		Search-engine friendly clone of the ACL2 documentation.

Arithmetic-operations

Plus-arithmetic-value

Apply unary + to an arithmetic value [C:6.5.3.3/2].

Signature
(plus-arithmetic-value val) → resval
Arguments: val — Guard (valuep val).
Returns: resval — Type (value-resultp resval).

We promote the operand and then we apply the operation on the integer. 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: plus-arithmetic-value

(defun plus-arithmetic-value (val)
  (declare (xargs :guard (valuep val)))
  (declare (xargs :guard (value-arithmeticp val)))
  (let ((__function__ 'plus-arithmetic-value))
    (declare (ignorable __function__))
    (b* ((val (promote-value val)))
      (plus-integer-value val))))

Theorem: value-resultp-of-plus-arithmetic-value

(defthm value-resultp-of-plus-arithmetic-value
  (b* ((resval (plus-arithmetic-value val)))
    (value-resultp resval))
  :rule-classes :rewrite)

Theorem: plus-arithmetic-value-of-value-fix-val

(defthm plus-arithmetic-value-of-value-fix-val
  (equal (plus-arithmetic-value (value-fix val))
         (plus-arithmetic-value val)))

Theorem: plus-arithmetic-value-value-equiv-congruence-on-val

(defthm plus-arithmetic-value-value-equiv-congruence-on-val
  (implies (value-equiv val val-equiv)
           (equal (plus-arithmetic-value val)
                  (plus-arithmetic-value val-equiv)))
  :rule-classes :congruence)