Lemmas about integer-length from the logops-lemmas book.
Theorem:
(defthm equal-integer-length-0 (equal (equal (integer-length i) 0) (or (zip i) (equal i -1))))
Theorem:
(defthm unsigned-byte-p-integer-length (implies (and (integerp i) (>= i 0) (equal size (integer-length i))) (unsigned-byte-p size i)) :rule-classes nil)
Theorem:
(defthm integer-length-unsigned-byte (implies (unsigned-byte-p size i) (<= (integer-length i) size)) :rule-classes nil)
Theorem:
(defthm signed-byte-p-integer-length (implies (and (integerp i) (integerp size) (> size 0) (equal size (+ (integer-length i) 1))) (signed-byte-p size i)) :rule-classes nil)
Theorem:
(defthm integer-length-signed-byte (implies (signed-byte-p size i) (<= (+ (integer-length i) 1) size)) :rule-classes nil)