		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Eval-binary-strict-pure

Evaluate a binary expression with a strict pure operator, on two values, returning a value.

Signature
(eval-binary-strict-pure op arg1 arg2) → val
Arguments: op — Guard (binopp op).; arg1 — Guard (valuep arg1).; arg2 — Guard (valuep arg2).
Returns: val — Type (value-resultp val).

Definitions and Theorems

Function: eval-binary-strict-pure

(defun eval-binary-strict-pure (op arg1 arg2)
  (declare (xargs :guard (and (binopp op)
                              (valuep arg1)
                              (valuep arg2))))
  (declare (xargs :guard (and (binop-strictp op)
                              (binop-purep op))))
  (let ((__function__ 'eval-binary-strict-pure))
    (declare (ignorable __function__))
    (case (binop-kind op)
      (:mul (mul-values arg1 arg2))
      (:div (div-values arg1 arg2))
      (:rem (rem-values arg1 arg2))
      (:add (add-values arg1 arg2))
      (:sub (sub-values arg1 arg2))
      (:shl (shl-values arg1 arg2))
      (:shr (shr-values arg1 arg2))
      (:lt (lt-values arg1 arg2))
      (:gt (gt-values arg1 arg2))
      (:le (le-values arg1 arg2))
      (:ge (ge-values arg1 arg2))
      (:eq (eq-values arg1 arg2))
      (:ne (ne-values arg1 arg2))
      (:bitand (bitand-values arg1 arg2))
      (:bitxor (bitxor-values arg1 arg2))
      (:bitior (bitior-values arg1 arg2))
      (t (error (impossible))))))

Theorem: value-resultp-of-eval-binary-strict-pure

(defthm value-resultp-of-eval-binary-strict-pure
  (b* ((val (eval-binary-strict-pure op arg1 arg2)))
    (value-resultp val))
  :rule-classes :rewrite)

Theorem: eval-binary-strict-pure-of-binop-fix-op

(defthm eval-binary-strict-pure-of-binop-fix-op
  (equal (eval-binary-strict-pure (binop-fix op)
                                  arg1 arg2)
         (eval-binary-strict-pure op arg1 arg2)))

Theorem: eval-binary-strict-pure-binop-equiv-congruence-on-op

(defthm eval-binary-strict-pure-binop-equiv-congruence-on-op
  (implies (binop-equiv op op-equiv)
           (equal (eval-binary-strict-pure op arg1 arg2)
                  (eval-binary-strict-pure op-equiv arg1 arg2)))
  :rule-classes :congruence)

Theorem: eval-binary-strict-pure-of-value-fix-arg1

(defthm eval-binary-strict-pure-of-value-fix-arg1
  (equal (eval-binary-strict-pure op (value-fix arg1)
                                  arg2)
         (eval-binary-strict-pure op arg1 arg2)))

Theorem: eval-binary-strict-pure-value-equiv-congruence-on-arg1

(defthm eval-binary-strict-pure-value-equiv-congruence-on-arg1
  (implies (value-equiv arg1 arg1-equiv)
           (equal (eval-binary-strict-pure op arg1 arg2)
                  (eval-binary-strict-pure op arg1-equiv arg2)))
  :rule-classes :congruence)

Theorem: eval-binary-strict-pure-of-value-fix-arg2

(defthm eval-binary-strict-pure-of-value-fix-arg2
  (equal (eval-binary-strict-pure op arg1 (value-fix arg2))
         (eval-binary-strict-pure op arg1 arg2)))

Theorem: eval-binary-strict-pure-value-equiv-congruence-on-arg2

(defthm eval-binary-strict-pure-value-equiv-congruence-on-arg2
  (implies (value-equiv arg2 arg2-equiv)
           (equal (eval-binary-strict-pure op arg1 arg2)
                  (eval-binary-strict-pure op arg1 arg2-equiv)))
  :rule-classes :congruence)