Bit Extraction
Function:
(defun bitn (x n) (declare (xargs :guard (and (integerp x) (integerp n)))) (mbe :logic (bits x n n) :exec (if (evenp (ash x (- n))) 0 1)))
Theorem:
(defthm bitn-nonnegative-integer (and (integerp (bitn x n)) (<= 0 (bitn x n))) :rule-classes (:type-prescription))
Theorem:
(defthm bits-n-n-rewrite (equal (bits x n n) (bitn x n)))
Theorem:
(defthm bitn-def (implies (case-split (integerp n)) (equal (bitn x n) (mod (fl (/ x (expt 2 n))) 2))))
Theorem:
(defthm bitn-rec-0 (implies (integerp x) (equal (bitn x 0) (mod x 2))))
Theorem:
(defthm bitn-rec-pos (implies (< 0 n) (equal (bitn x n) (bitn (fl (/ x 2)) (1- n)))) :rule-classes ((:definition :controller-alist ((bitn t t)))))
Theorem:
(defthm bitn-0-1 (or (equal (bitn x n) 0) (equal (bitn x n) 1)) :rule-classes nil)
Theorem:
(defthm bitn-bvecp (implies (and (<= 1 k) (case-split (integerp k))) (bvecp (bitn x n) k)))
Theorem:
(defthm bitn-bvecp-forward (bvecp (bitn x n) 1) :rule-classes ((:forward-chaining :trigger-terms ((bitn x n)))))
Theorem:
(defthm bitn-neg (implies (and (< n 0) (integerp x)) (equal (bitn x n) 0)))
Theorem:
(defthm bitn-0 (equal (bitn 0 k) 0))
Theorem:
(defthm bitn-bvecp-1 (implies (bvecp x 1) (equal (bitn x 0) x)))
Theorem:
(defthm bitn-bitn-0 (equal (bitn (bitn x n) 0) (bitn x n)))
Theorem:
(defthm bitn-mod (implies (and (< k n) (integerp n) (integerp k)) (equal (bitn (mod x (expt 2 n)) k) (bitn x k))))
Theorem:
(defthm bvecp-bitn-0 (implies (bvecp x n) (equal (bitn x n) 0)))
Theorem:
(defthm neg-bitn-1 (implies (and (integerp x) (integerp n) (< x 0) (>= x (- (expt 2 n)))) (equal (bitn x n) 1)))
Theorem:
(defthm bitn-minus-1 (implies (natp i) (equal (bitn -1 i) 1)))
Theorem:
(defthm neg-bitn-2 (implies (and (integerp x) (integerp n) (integerp k) (< k n) (< x (- (expt 2 k) (expt 2 n))) (>= x (- (expt 2 n)))) (equal (bitn x k) 0)))
Theorem:
(defthm neg-bitn-0 (implies (and (integerp x) (natp n) (< x (- (expt 2 n))) (>= x (- (expt 2 (1+ n))))) (equal (bitn x n) 0)))
Theorem:
(defthm bitn-shift-up (implies (and (integerp n) (integerp k)) (equal (bitn (* x (expt 2 k)) (+ n k)) (bitn x n))))
Theorem:
(defthm bitn-shift-down (implies (and (natp i) (integerp k)) (equal (bitn (fl (/ x (expt 2 k))) i) (bitn x (+ i k)))))
Theorem:
(defthm bitn-bits (implies (and (<= k (- i j)) (case-split (<= 0 k)) (case-split (integerp i)) (case-split (integerp j)) (case-split (integerp k))) (equal (bitn (bits x i j) k) (bitn x (+ j k)))))
Theorem:
(defthm bitn-plus-bits (implies (and (<= m n) (integerp m) (integerp n)) (= (bits x n m) (+ (* (bitn x n) (expt 2 (- n m))) (bits x (1- n) m)))) :rule-classes nil)
Theorem:
(defthm bits-plus-bitn (implies (and (<= m n) (integerp m) (integerp n)) (= (bits x n m) (+ (bitn x m) (* 2 (bits x n (1+ m)))))) :rule-classes nil)
Function:
(defun sumbits (x n) (declare (xargs :guard (and (integerp x) (natp n)))) (if (zp n) 0 (+ (* (expt 2 (1- n)) (bitn x (1- n))) (sumbits x (1- n)))))
Theorem:
(defthm sumbits-bits (implies (and (integerp x) (natp n) (> n 0)) (equal (sumbits x n) (bits x (1- n) 0))))
Theorem:
(defthm sumbits-thm (implies (and (bvecp x n) (natp n) (> n 0)) (equal (sumbits x n) x)))
Function:
(defun all-bits-p (b k) (declare (xargs :guard t)) (if (posp k) (and (consp b) (all-bits-p (cdr b) (1- k)) (or (equal (car b) 0) (equal (car b) 1))) (and (true-listp b) (equal k 0))))
Function:
(defun sum-b (b k) (declare (xargs :guard (all-bits-p b k))) (if (zp k) 0 (+ (* (expt 2 (1- k)) (nth (1- k) b)) (sum-b b (1- k)))))
Theorem:
(defthm sum-bitn (implies (and (all-bits-p b n) (natp k) (< k n)) (equal (bitn (sum-b b n) k) (nth k b))))
Function:
(defun bit-diff (x y) (declare (xargs :guard t)) (if (or (not (integerp x)) (not (integerp y)) (= x y)) nil (if (= (bitn x 0) (bitn y 0)) (1+ (bit-diff (fl (/ x 2)) (fl (/ y 2)))) 0)))
Theorem:
(defthm bit-diff-diff (implies (and (integerp x) (integerp y) (not (= x y))) (let ((n (bit-diff x y))) (and (natp n) (not (= (bitn x n) (bitn y n)))))) :rule-classes nil)
Theorem:
(defthm bvecp-bitn-1 (implies (and (bvecp x (1+ n)) (<= (expt 2 n) x) (natp n)) (equal (bitn x n) 1)))
Theorem:
(defthm bvecp-bitn-2 (implies (and (bvecp x n) (< k n) (<= (- (expt 2 n) (expt 2 k)) x) (integerp n) (integerp k)) (equal (bitn x k) 1)) :rule-classes ((:rewrite :match-free :all)))
Theorem:
(defthm bitn-expt (implies (case-split (integerp n)) (equal (bitn (expt 2 n) n) 1)))
Theorem:
(defthm bitn-expt-0 (implies (and (not (equal i n)) (case-split (integerp i))) (equal (bitn (expt 2 i) n) 0)))
Theorem:
(defthm bitn-plus-expt-1 (implies (and (rationalp x) (integerp n)) (not (equal (bitn (+ x (expt 2 n)) n) (bitn x n)))) :rule-classes nil)
Theorem:
(defthm bitn-plus-mult (implies (and (< n m) (integerp m) (integerp k)) (equal (bitn (+ x (* k (expt 2 m))) n) (bitn x n))))
Theorem:
(defthm bitn-plus-mult-rewrite (implies (and (syntaxp (quotep c)) (equal (mod c (expt 2 (1+ n))) 0)) (equal (bitn (+ c x) n) (bitn x n))))