		Search-engine friendly clone of the ACL2 documentation.

Arithmetic-operations

Plus-arithmetic-value

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

Signature
(plus-arithmetic-value val) → resval
Arguments: val — Guard (valuep val).
Returns: resval — Type (valuep 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: valuep-of-plus-arithmetic-value

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

Theorem: type-of-value-of-plus-arithmetic-value

(defthm type-of-value-of-plus-arithmetic-value
  (b* ((?resval (plus-arithmetic-value val)))
    (equal (type-of-value resval)
           (promote-type (type-of-value val)))))

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)