		Search-engine friendly clone of the ACL2 documentation.

Fgl-syntactic-checker-binders

Integer-length-bound

FGL binder that finds a bound for the integer-length of X if possible.

Signature
(integer-length-bound ans x) → bound
Arguments: ans — Guard (acl2::maybe-natp ans).; x — Guard (integerp x).
Returns: bound — Type (acl2::maybe-natp bound).

Logically, this function returns either NIL or a natural number greater than or equal to the integer length of x. Its FGL binder meta rule checks whether x is a symbolic integer and if so returns the count of its symbolic bits.

Definitions and Theorems

Function: integer-length-bound

(defun integer-length-bound (ans x)
  (declare (xargs :guard (and (acl2::maybe-natp ans)
                              (integerp x))))
  (let ((__function__ 'integer-length-bound))
    (declare (ignorable __function__))
    (and (natp ans)
         (<= (integer-length x) ans)
         ans)))

Theorem: maybe-natp-of-integer-length-bound

(defthm maybe-natp-of-integer-length-bound
  (b* ((bound (integer-length-bound ans x)))
    (acl2::maybe-natp bound))
  :rule-classes :type-prescription)

Theorem: integer-length-bound-implies-integer-length

(defthm integer-length-bound-implies-integer-length
  (implies (integer-length-bound ans x)
           (<= (integer-length x)
               (integer-length-bound ans x)))
  :rule-classes :linear)