		Search-engine friendly clone of the ACL2 documentation.

Integer-operations

Le-integer-values

Apply <= to integer values [C:6.5.8/6].

Signature
(le-integer-values val1 val2) → resval
Arguments: val1 — Guard (valuep val1).; val2 — Guard (valuep val2).
Returns: resval — Type (valuep 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 always int. This operation is always well-defined, so it always returns a value (never an error).

Definitions and Theorems

Function: le-integer-values

(defun le-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__ 'le-integer-values))
    (declare (ignorable __function__))
    (b* ((mathint1 (value-integer->get val1))
         (mathint2 (value-integer->get val2)))
      (if (<= mathint1 mathint2)
          (value-sint 1)
        (value-sint 0)))))

Theorem: valuep-of-le-integer-values

(defthm valuep-of-le-integer-values
  (b* ((resval (le-integer-values val1 val2)))
    (valuep resval))
  :rule-classes :rewrite)

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

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

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

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

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

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

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

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