Binary Operations
Theorem:
(defthm logand-def (equal (logand x y) (if (or (zip x) (zip y)) 0 (if (= x y) x (+ (* 2 (logand (fl (/ x 2)) (fl (/ y 2)))) (logand (mod x 2) (mod y 2)))))) :rule-classes ((:definition :controller-alist ((binary-logand t t)))))
Theorem:
(defthm logior-def (implies (and (integerp x) (integerp y)) (equal (logior x y) (if (or (zip x) (= x y)) y (if (zip y) x (+ (* 2 (logior (fl (/ x 2)) (fl (/ y 2)))) (logior (mod x 2) (mod y 2))))))) :rule-classes ((:definition :controller-alist ((binary-logior t t)))))
Theorem:
(defthm logxor-def (implies (and (integerp x) (integerp y)) (equal (logxor x y) (if (zip x) y (if (zip y) x (if (= x y) 0 (+ (* 2 (logxor (fl (/ x 2)) (fl (/ y 2)))) (logxor (mod x 2) (mod y 2)))))))) :rule-classes ((:definition :controller-alist ((binary-logxor t t)))))
Function:
(defun log-induct (x y) (if (or (not (integerp x)) (not (integerp y)) (= x 0) (= y 0) (= x y)) (+ x y) (log-induct (fl (/ x 2)) (fl (/ y 2)))))
Theorem:
(defthm logand-bvecp (implies (and (natp n) (bvecp x n) (integerp y)) (bvecp (logand x y) n)))
Theorem:
(defthm logior-bvecp (implies (and (bvecp x n) (bvecp y n)) (bvecp (logior x y) n)))
Theorem:
(defthm logxor-bvecp (implies (and (bvecp x n) (bvecp y n) (natp n)) (bvecp (logxor x y) n)))
Theorem:
(defthm logand-plus-logxor (implies (and (integerp x) (integerp y)) (equal (+ (logand x y) (logxor x y)) (logior x y))))
Theorem:
(defthm logand-mod (implies (and (integerp x) (integerp y) (integerp n)) (equal (mod (logand x y) (expt 2 n)) (logand (mod x (expt 2 n)) (mod y (expt 2 n))))))
Theorem:
(defthm logior-mod (implies (and (integerp x) (integerp y) (integerp n)) (equal (mod (logior x y) (expt 2 n)) (logior (mod x (expt 2 n)) (mod y (expt 2 n))))))
Theorem:
(defthm logxor-mod (implies (and (integerp x) (integerp y) (integerp n)) (equal (mod (logxor x y) (expt 2 n)) (logxor (mod x (expt 2 n)) (mod y (expt 2 n))))))
Theorem:
(defthm fl-logand (implies (and (integerp x) (integerp y) (natp n)) (equal (fl (* (expt 2 (- n)) (logand x y))) (logand (fl (* (expt 2 (- n)) x)) (fl (* (expt 2 (- n)) y))))))
Theorem:
(defthm fl-logior (implies (and (integerp x) (integerp y) (natp n)) (equal (fl (* (expt 2 (- n)) (logior x y))) (logior (fl (* (expt 2 (- n)) x)) (fl (* (expt 2 (- n)) y))))))
Theorem:
(defthm fl-logxor (implies (and (integerp x) (integerp y) (natp n)) (equal (fl (* (expt 2 (- n)) (logxor x y))) (logxor (fl (* (expt 2 (- n)) x)) (fl (* (expt 2 (- n)) y))))))
Theorem:
(defthm logand-cat (implies (and (case-split (integerp x1)) (case-split (integerp y1)) (case-split (integerp x2)) (case-split (integerp y2)) (case-split (natp n)) (case-split (natp m))) (equal (logand (cat x1 m y1 n) (cat x2 m y2 n)) (cat (logand x1 x2) m (logand y1 y2) n))))
Theorem:
(defthm logior-cat (implies (and (case-split (integerp x1)) (case-split (integerp y1)) (case-split (integerp x2)) (case-split (integerp y2)) (case-split (natp n)) (case-split (natp m))) (equal (logior (cat x1 m y1 n) (cat x2 m y2 n)) (cat (logior x1 x2) m (logior y1 y2) n))))
Theorem:
(defthm logxor-cat (implies (and (case-split (integerp x1)) (case-split (integerp y1)) (case-split (integerp x2)) (case-split (integerp y2)) (case-split (natp n)) (case-split (natp m))) (equal (logxor (cat x1 m y1 n) (cat x2 m y2 n)) (cat (logxor x1 x2) m (logxor y1 y2) n))))
Theorem:
(defthm logand-shift (implies (and (integerp x) (integerp y) (natp k)) (equal (logand (* (expt 2 k) x) (* (expt 2 k) y)) (* (expt 2 k) (logand x y)))))
Theorem:
(defthm logior-shift (implies (and (integerp x) (integerp y) (natp k)) (equal (logior (* (expt 2 k) x) (* (expt 2 k) y)) (* (expt 2 k) (logior x y)))))
Theorem:
(defthm logxor-shift (implies (and (integerp x) (integerp y) (natp k)) (equal (logxor (* (expt 2 k) x) (* (expt 2 k) y)) (* (expt 2 k) (logxor x y)))))
Theorem:
(defthm logand-expt (implies (and (integerp x) (integerp y) (natp n)) (equal (logand (* (expt 2 n) x) y) (* (expt 2 n) (logand x (fl (/ y (expt 2 n))))))))
Theorem:
(defthm logior-expt (implies (and (integerp x) (integerp y) (natp n)) (equal (logior (* (expt 2 n) x) y) (+ (* (expt 2 n) (logior x (fl (/ y (expt 2 n))))) (mod y (expt 2 n))))))
Theorem:
(defthm logxor-expt (implies (and (integerp x) (integerp y) (natp n)) (equal (logxor (* (expt 2 n) x) y) (+ (* (expt 2 n) (logxor x (fl (/ y (expt 2 n))))) (mod y (expt 2 n))))))
Theorem:
(defthm logior-expt-cor (implies (and (natp n) (integerp x) (bvecp y n)) (equal (logior (* (expt 2 n) x) y) (+ (* (expt 2 n) x) y))))
Theorem:
(defthm logior-2**n (implies (and (natp n) (integerp x)) (equal (logior (expt 2 n) x) (if (= (bitn x n) 1) x (+ x (expt 2 n))))))
Theorem:
(defthm logand-bits (implies (and (integerp x) (natp n) (natp k) (< k n)) (equal (logand x (- (expt 2 n) (expt 2 k))) (* (expt 2 k) (bits x (1- n) k)))))
Theorem:
(defthm logand-bit (implies (and (integerp x) (natp n)) (equal (logand x (expt 2 n)) (* (expt 2 n) (bitn x n)))))
Theorem:
(defthm bits-logand (implies (and (integerp x) (integerp y) (integerp i) (integerp j)) (equal (bits (logand x y) i j) (logand (bits x i j) (bits y i j)))))
Theorem:
(defthm bits-logior (implies (and (integerp x) (integerp y) (integerp i) (integerp j)) (equal (bits (logior x y) i j) (logior (bits x i j) (bits y i j)))))
Theorem:
(defthm bits-logxor (implies (and (integerp x) (integerp y) (integerp i) (integerp j)) (equal (bits (logxor x y) i j) (logxor (bits x i j) (bits y i j)))))
Theorem:
(defthm bitn-logand (implies (and (integerp x) (integerp y) (integerp n)) (equal (bitn (logand x y) n) (logand (bitn x n) (bitn y n)))))
Theorem:
(defthm bitn-logior (implies (and (integerp x) (integerp y) (integerp n)) (equal (bitn (logior x y) n) (logior (bitn x n) (bitn y n)))))
Theorem:
(defthm bitn-logxor (implies (and (case-split (integerp x)) (case-split (integerp y)) (case-split (integerp n))) (equal (bitn (logxor x y) n) (logxor (bitn x n) (bitn y n)))))