		Search-engine friendly clone of the ACL2 documentation.

Integer-ranges

Integer-type-rangep

Check if a mathematical integer is in the range of an integer type.

Signature
(integer-type-rangep mathint type) → yes/no
Arguments: mathint — Guard (integerp mathint).; type — Guard (typep type).
Returns: yes/no — Type (booleanp yes/no).

Fot now we exclude the plain char type, via the guard. However, we prefer to keep the name of this function more general, in anticipation for extending it to those two types.

Definitions and Theorems

Function: integer-type-rangep

(defun integer-type-rangep (mathint type)
  (declare (xargs :guard (and (integerp mathint) (typep type))))
  (declare (xargs :guard (type-nonchar-integerp type)))
  (let ((__function__ 'integer-type-rangep))
    (declare (ignorable __function__))
    (and (<= (integer-type-min type)
             (ifix mathint))
         (<= (ifix mathint)
             (integer-type-max type)))))

Theorem: booleanp-of-integer-type-rangep

(defthm booleanp-of-integer-type-rangep
  (b* ((yes/no (integer-type-rangep mathint type)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: integer-type-rangep-to-signed-byte-p

(defthm integer-type-rangep-to-signed-byte-p
  (implies (and (type-signed-integerp type)
                (integerp int))
           (equal (integer-type-rangep int type)
                  (signed-byte-p (integer-type-bits type)
                                 int))))

Theorem: integer-type-rangep-to-unsigned-byte-p

(defthm integer-type-rangep-to-unsigned-byte-p
  (implies (and (type-unsigned-integerp type)
                (integerp int))
           (equal (integer-type-rangep int type)
                  (unsigned-byte-p (integer-type-bits type)
                                   int))))

Theorem: integer-type-rangep-of-ifix-mathint

(defthm integer-type-rangep-of-ifix-mathint
  (equal (integer-type-rangep (ifix mathint)
                              type)
         (integer-type-rangep mathint type)))

Theorem: integer-type-rangep-int-equiv-congruence-on-mathint

(defthm integer-type-rangep-int-equiv-congruence-on-mathint
  (implies (acl2::int-equiv mathint mathint-equiv)
           (equal (integer-type-rangep mathint type)
                  (integer-type-rangep mathint-equiv type)))
  :rule-classes :congruence)

Theorem: integer-type-rangep-of-type-fix-type

(defthm integer-type-rangep-of-type-fix-type
  (equal (integer-type-rangep mathint (type-fix type))
         (integer-type-rangep mathint type)))

Theorem: integer-type-rangep-type-equiv-congruence-on-type

(defthm integer-type-rangep-type-equiv-congruence-on-type
  (implies (type-equiv type type-equiv)
           (equal (integer-type-rangep mathint type)
                  (integer-type-rangep mathint type-equiv)))
  :rule-classes :congruence)