Apply unary
(minus-arithmetic-value val) → 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 value.
Function:
(defun minus-arithmetic-value (val) (declare (xargs :guard (valuep val))) (declare (xargs :guard (value-arithmeticp val))) (let ((__function__ 'minus-arithmetic-value)) (declare (ignorable __function__)) (b* ((val (promote-value val))) (minus-integer-value val))))
Theorem:
(defthm value-resultp-of-minus-arithmetic-value (b* ((resval (minus-arithmetic-value val))) (value-resultp resval)) :rule-classes :rewrite)
Theorem:
(defthm minus-arithmetic-value-of-value-fix-val (equal (minus-arithmetic-value (value-fix val)) (minus-arithmetic-value val)))
Theorem:
(defthm minus-arithmetic-value-value-equiv-congruence-on-val (implies (value-equiv val val-equiv) (equal (minus-arithmetic-value val) (minus-arithmetic-value val-equiv))) :rule-classes :congruence)