		Search-engine friendly clone of the ACL2 documentation.

Integer-operations

Rem-integer-values

Apply % to integer values [C:6.5.5/5] [C:6.5.5/6].

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

By the time we reach this ACL2 function, the values have already been subjected to the usual arithmetic conversions, so they are promoted arithmetic value with the same type. We put this condition in the guard.

The type of the result is the same as the operands [C:6.3.1.8/1]. We use result-integer-value to return the resulting value, or an error, as documented in that function.

It is an error if the divisor is 0 [C:6.5.5/5].

We use rem because it matches the use of truncate, in terms of the relationship between quotient and remainder [C:6.5.5/6], in the definition of / in rem-integer-values.

Definitions and Theorems

Function: rem-integer-values

(defun rem-integer-values (val1 val2)
  (declare (xargs :guard (and (valuep val1) (valuep val2))))
  (declare (xargs :guard (and (value-integerp val1)
                              (value-integerp val2)
                              (value-promoted-arithmeticp val1)
                              (value-promoted-arithmeticp val2)
                              (equal (type-of-value val1)
                                     (type-of-value val2)))))
  (let ((__function__ 'rem-integer-values))
    (declare (ignorable __function__))
    (b* ((mathint1 (value-integer->get val1))
         (mathint2 (value-integer->get val2))
         ((when (equal mathint2 0))
          (error :division-by-zero))
         (result (rem mathint1 mathint2))
         (resval (result-integer-value result (type-of-value val1)))
         ((when (errorp resval))
          (error (list :undefined-rem (value-fix val1)
                       (value-fix val2)))))
      resval)))

Theorem: value-resultp-of-rem-integer-values

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

Theorem: rem-integer-values-of-value-fix-val1

(defthm rem-integer-values-of-value-fix-val1
  (equal (rem-integer-values (value-fix val1)
                             val2)
         (rem-integer-values val1 val2)))

Theorem: rem-integer-values-value-equiv-congruence-on-val1

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

Theorem: rem-integer-values-of-value-fix-val2

(defthm rem-integer-values-of-value-fix-val2
  (equal (rem-integer-values val1 (value-fix val2))
         (rem-integer-values val1 val2)))

Theorem: rem-integer-values-value-equiv-congruence-on-val2

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