		Search-engine friendly clone of the ACL2 documentation.

Arithmetic-operations

Eq-arithmetic-values

Apply == to arithmetic values [C:6.5.9/3] [C:6.5.9/4].

Signature
(eq-arithmetic-values val1 val2) → resval
Arguments: val1 — Guard (valuep val1).; val2 — Guard (valuep val2).
Returns: resval — Type (value-resultp resval).

We perform the usual arithmetic conversions and then we apply the operation on the integers. In our current formalization, integers are the only arithmetic values. This ACL2 function will be extended with more cases if/when we extend our model with non-integer arithmetic values.

Definitions and Theorems

Function: eq-arithmetic-values

(defun eq-arithmetic-values (val1 val2)
  (declare (xargs :guard (and (valuep val1) (valuep val2))))
  (declare (xargs :guard (and (value-arithmeticp val1)
                              (value-arithmeticp val2))))
  (let ((__function__ 'eq-arithmetic-values))
    (declare (ignorable __function__))
    (b* (((mv val1 val2)
          (uaconvert-values val1 val2)))
      (eq-integer-values val1 val2))))

Theorem: value-resultp-of-eq-arithmetic-values

(defthm value-resultp-of-eq-arithmetic-values
  (b* ((resval (eq-arithmetic-values val1 val2)))
    (value-resultp resval))
  :rule-classes :rewrite)

Theorem: eq-arithmetic-values-of-value-fix-val1

(defthm eq-arithmetic-values-of-value-fix-val1
  (equal (eq-arithmetic-values (value-fix val1)
                               val2)
         (eq-arithmetic-values val1 val2)))

Theorem: eq-arithmetic-values-value-equiv-congruence-on-val1

(defthm eq-arithmetic-values-value-equiv-congruence-on-val1
  (implies (value-equiv val1 val1-equiv)
           (equal (eq-arithmetic-values val1 val2)
                  (eq-arithmetic-values val1-equiv val2)))
  :rule-classes :congruence)

Theorem: eq-arithmetic-values-of-value-fix-val2

(defthm eq-arithmetic-values-of-value-fix-val2
  (equal (eq-arithmetic-values val1 (value-fix val2))
         (eq-arithmetic-values val1 val2)))

Theorem: eq-arithmetic-values-value-equiv-congruence-on-val2

(defthm eq-arithmetic-values-value-equiv-congruence-on-val2
  (implies (value-equiv val2 val2-equiv)
           (equal (eq-arithmetic-values val1 val2)
                  (eq-arithmetic-values val1 val2-equiv)))
  :rule-classes :congruence)