		Search-engine friendly clone of the ACL2 documentation.

Arithmetic-operations

Sub-arithmetic-values

Apply binary - to arithmetic values [C17:6.5.6/4] [C17:6.5.6/6].

Signature
(sub-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: sub-arithmetic-values

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

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

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

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

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

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

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

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

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

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

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