Recognizing Bit Vectors
Function:
(defun bvecp (x k) (declare (xargs :guard (integerp k))) (and (integerp x) (<= 0 x) (< x (expt 2 k))))
Theorem:
(defthm bvecp-forward (implies (bvecp x k) (and (integerp x) (<= 0 x) (< x (expt 2 k)))) :rule-classes :forward-chaining)
Function:
(defun nats (n) (declare (xargs :guard (natp n))) (if (zp n) nil (cons (1- n) (nats (1- n)))))
Theorem:
(defthm bvecp-member (implies (and (natp n) (bvecp x n)) (member x (nats (expt 2 n)))) :rule-classes nil)
Theorem:
(defthm bvecp-monotone (implies (and (bvecp x n) (<= n m) (case-split (integerp m))) (bvecp x m)))
Theorem:
(defthm bvecp-shift-down (implies (and (bvecp x n) (natp n) (natp k)) (bvecp (fl (/ x (expt 2 k))) (- n k))))
Theorem:
(defthm bvecp-shift-up (implies (and (bvecp x (- n k)) (natp k) (integerp n)) (bvecp (* x (expt 2 k)) n)))
Theorem:
(defthm bvecp-product (implies (and (bvecp x m) (bvecp y n)) (bvecp (* x y) (+ m n))) :rule-classes nil)
Theorem:
(defthm bvecp-1-0 (implies (and (bvecp x 1) (not (equal x 1))) (equal x 0)) :rule-classes :forward-chaining)
Theorem:
(defthm bvecp-0-1 (implies (and (bvecp x 1) (not (equal x 0))) (equal x 1)) :rule-classes :forward-chaining)