• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
    • Bit-vectors
      • Sparseint
      • Bitops
        • Bitops/merge
        • Bitops-compatibility
        • Bitops-books
        • Logbitp-reasoning
        • Bitops/signed-byte-p
        • Fast-part-select
        • Bitops/integer-length
        • Bitops/extra-defs
        • Install-bit
        • Trailing-0-count
        • Bitops/defaults
        • Logbitp-mismatch
        • Trailing-1-count
        • Bitops/rotate
        • Bitops/equal-by-logbitp
        • Bitops/ash-bounds
        • Bitops/fast-logrev
        • Limited-shifts
        • Bitops/part-select
        • Bitops/parity
        • Bitops/saturate
        • Bitops/part-install
        • Bitops/logbitp-bounds
        • Bitops/ihsext-basics
        • Bitops/fast-rotate
        • Bitops/fast-logext
        • Bitops/ihs-extensions
      • Bv
      • Ihs
      • Rtl
    • Algebra
  • Testing-utilities

• Bitops
• Integer-length

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)))