		Search-engine friendly clone of the ACL2 documentation.

Integer-range-fix

Fixing function for integer-range-p.

Signature
(integer-range-fix lower upper x) → fixed-x
Arguments: lower — Guard (integerp lower).; upper — Guard (integerp upper).; x — Guard (integer-range-p lower upper x).
Returns: fixed-x — Type (integer-range-p lower upper fixed-x), given (and (integerp lower) (integerp upper) (< lower upper)).

Since the set denoted by integer-range-p is empty for some values of lower and upper, this fixing function cannot always return a value satisfying the predicate. Even though integer-range-p does not fix its lower and upper arguments to integerp, this fixing function does, i.e. it treats lower and upper as integers. Thus, the set (range) denoted by integer-range-p is empty iff lower is not below upper. If the range is empty, this fixing function returns 0. If the range is not empty but x is below lower, we return lower, i.e. the closest value to x in range. If the range is not empty and x is not below upper, we return one below upper, i.e. the closest value to x in range.

Since integer-range-p is enabled by default, this fixing function is also enabled by default. When these functions are enabled, they are meant as abbreviations, and theorems triggered by them may not fire during proofs.

Definitions and Theorems

Function: integer-range-fix

(defun integer-range-fix (lower upper x)
  (declare (xargs :guard (and (integerp lower)
                              (integerp upper)
                              (integer-range-p lower upper x))))
  (let ((__function__ 'integer-range-fix))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((lower (ifix lower))
              (upper (ifix upper))
              (x (ifix x)))
           (if (< lower upper)
               (cond ((< x lower) lower)
                     ((>= x upper) (1- upper))
                     (t x))
             0))
         :exec x)))

Theorem: return-type-of-integer-range-fix

(defthm return-type-of-integer-range-fix
  (implies (and (integerp lower)
                (integerp upper)
                (< lower upper))
           (b* ((fixed-x (integer-range-fix lower upper x)))
             (integer-range-p lower upper fixed-x)))
  :rule-classes :rewrite)

Theorem: integer-range-fix-when-integer-range-p

(defthm integer-range-fix-when-integer-range-p
  (implies (and (integer-range-p (ifix lower)
                                 (ifix upper)
                                 x)
                (< (ifix lower) (ifix upper)))
           (equal (integer-range-fix lower upper x)
                  x)))

Theorem: integer-range-fix-of-ifix-lower

(defthm integer-range-fix-of-ifix-lower
  (equal (integer-range-fix (ifix lower) upper x)
         (integer-range-fix lower upper x)))

Theorem: integer-range-fix-int-equiv-congruence-on-lower

(defthm integer-range-fix-int-equiv-congruence-on-lower
  (implies (int-equiv lower lower-equiv)
           (equal (integer-range-fix lower upper x)
                  (integer-range-fix lower-equiv upper x)))
  :rule-classes :congruence)

Theorem: integer-range-fix-of-ifix-upper

(defthm integer-range-fix-of-ifix-upper
  (equal (integer-range-fix lower (ifix upper) x)
         (integer-range-fix lower upper x)))

Theorem: integer-range-fix-int-equiv-congruence-on-upper

(defthm integer-range-fix-int-equiv-congruence-on-upper
  (implies (int-equiv upper upper-equiv)
           (equal (integer-range-fix lower upper x)
                  (integer-range-fix lower upper-equiv x)))
  :rule-classes :congruence)