		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-binop

Map a binary operator to a binary operator in the language definition.

Signature
(ldm-binop binop) → binop1
Arguments: binop — Guard (binopp binop).
Returns: binop1 — Type (c::binopp binop1).

Definitions and Theorems

Function: ldm-binop

(defun ldm-binop (binop)
  (declare (xargs :guard (binopp binop)))
  (let ((__function__ 'ldm-binop))
    (declare (ignorable __function__))
    (binop-case binop
                :mul (c::binop-mul)
                :div (c::binop-div)
                :rem (c::binop-rem)
                :add (c::binop-add)
                :sub (c::binop-sub)
                :shl (c::binop-shl)
                :shr (c::binop-shr)
                :lt (c::binop-lt)
                :gt (c::binop-gt)
                :le (c::binop-le)
                :ge (c::binop-ge)
                :eq (c::binop-eq)
                :ne (c::binop-ne)
                :bitand (c::binop-bitand)
                :bitxor (c::binop-bitxor)
                :bitior (c::binop-bitior)
                :logand (c::binop-logand)
                :logor (c::binop-logor)
                :asg (c::binop-asg)
                :asg-mul (c::binop-asg-mul)
                :asg-div (c::binop-asg-div)
                :asg-rem (c::binop-asg-rem)
                :asg-add (c::binop-asg-add)
                :asg-sub (c::binop-asg-sub)
                :asg-shl (c::binop-asg-shl)
                :asg-shr (c::binop-asg-shr)
                :asg-and (c::binop-asg-and)
                :asg-xor (c::binop-asg-xor)
                :asg-ior (c::binop-asg-ior))))

Theorem: binopp-of-ldm-binop

(defthm binopp-of-ldm-binop
  (b* ((binop1 (ldm-binop binop)))
    (c::binopp binop1))
  :rule-classes :rewrite)

Theorem: ldm-binop-of-binop-fix-binop

(defthm ldm-binop-of-binop-fix-binop
  (equal (ldm-binop (binop-fix binop))
         (ldm-binop binop)))

Theorem: ldm-binop-binop-equiv-congruence-on-binop

(defthm ldm-binop-binop-equiv-congruence-on-binop
  (implies (binop-equiv binop binop-equiv)
           (equal (ldm-binop binop)
                  (ldm-binop binop-equiv)))
  :rule-classes :congruence)