		Search-engine friendly clone of the ACL2 documentation.

Bitops/integer-length

Basic theorems about integer-length.

Definitions and Theorems

Theorem: integer-length-type-prescription-strong

(defthm integer-length-type-prescription-strong
  (implies (and (integerp n) (< 0 n))
           (and (integerp (integer-length n))
                (< 0 (integer-length n))))
  :rule-classes :type-prescription)

Theorem: integer-length-type-prescription-strong-negative

(defthm integer-length-type-prescription-strong-negative
  (implies (and (integerp n) (< n -1))
           (and (integerp (integer-length n))
                (< 0 (integer-length n))))
  :rule-classes :type-prescription)

Theorem: integer-length-expt-upper-bound-n

(defthm integer-length-expt-upper-bound-n
  (implies (integerp n)
           (< n (expt 2 (integer-length n))))
  :rule-classes :linear)

Theorem: integer-length-expt-upper-bound-n-1

(defthm integer-length-expt-upper-bound-n-1
  (implies (integerp n)
           (<= n (expt 2 (integer-length (1- n)))))
  :rule-classes :linear)

Theorem: integer-length-monotonic

(defthm integer-length-monotonic
  (implies (and (<= i j) (natp i) (natp j))
           (<= (integer-length i)
               (integer-length j)))
  :rule-classes :linear)

Theorem: integer-length-less

(defthm integer-length-less
  (implies (natp n)
           (<= (integer-length n) n))
  :rule-classes :linear)

Theorem: (integer-length (expt 2 n))

(defthm |(integer-length (expt 2 n))|
  (implies (natp n)
           (equal (integer-length (expt 2 n))
                  (+ 1 n))))

Theorem: (integer-length (1- (expt 2 n)))

(defthm |(integer-length (1- (expt 2 n)))|
  (implies (natp n)
           (equal (integer-length (+ -1 (expt 2 n)))
                  n)))

Theorem: (integer-length (floor n 2))

(defthm |(integer-length (floor n 2))|
  (implies (natp n)
           (equal (integer-length (floor n 2))
                  (if (zp n)
                      0
                    (- (integer-length n) 1)))))

Theorem: 2^{(integer-length n) - 1} <= n

(defthm |2^{(integer-length n) - 1} <= n|
  (implies (posp n)
           (<= (expt 2 (1- (integer-length n))) n))
  :rule-classes ((:rewrite) (:linear)))

Theorem: integer-length-of-logcdr-strong

(defthm integer-length-of-logcdr-strong
  (implies (posp (integer-length a))
           (< (integer-length (logcdr a))
              (integer-length a)))
  :rule-classes ((:rewrite) (:linear)))

Theorem: integer-length-of-logcdr-weak

(defthm integer-length-of-logcdr-weak
  (<= (integer-length (logcdr a))
      (integer-length a))
  :rule-classes ((:rewrite) (:linear)))

Theorem: integer-length-bounded-by-expt

(defthm integer-length-bounded-by-expt
 (implies (and (< a (expt 2 n)) (natp a) (natp n))
          (< (integer-length a) (+ 1 n)))
 :rule-classes
 ((:rewrite
     :corollary
     (implies (and (syntaxp (or (not (quotep n)) (< (cadr n) 1000)))
                   (< a (expt 2 n))
                   (natp a)
                   (natp n))
              (< (integer-length a) (+ 1 n))))
  (:linear)))

Theorem: (integer-length (mod a (expt 2 n)))

(defthm |(integer-length (mod a (expt 2 n)))|
  (implies (and (natp a) (natp n))
           (< (integer-length (mod a (expt 2 n)))
              (+ 1 n)))
  :rule-classes ((:rewrite) (:linear)))

Theorem: integer-length-expt-lower-bound

(defthm integer-length-expt-lower-bound
  (implies (posp n)
           (<= (expt 2 (+ -1 (integer-length n)))
               n))
  :rule-classes :linear)

Theorem: integer-length-when-less-than-exp

(defthm integer-length-when-less-than-exp
  (implies (and (< x (expt 2 y)) (natp x) (natp y))
           (<= (integer-length x) y))
  :rule-classes :linear)

Theorem: integer-length-when-greater-than-exp

(defthm integer-length-when-greater-than-exp
  (implies (and (<= (expt 2 y) x)
                (natp x)
                (integerp y))
           (< y (integer-length x)))
  :rule-classes :linear)

Theorem: integer-length-unique

(defthm integer-length-unique
  (implies (and (<= (expt 2 (1- y)) x)
                (< x (expt 2 y))
                (posp x)
                (posp y))
           (equal (integer-length x) y)))