Concatenation
Function:
(defun binary-cat (x m y n) (declare (xargs :guard (and (integerp x) (integerp y) (natp m) (natp n)))) (if (and (natp m) (natp n)) (+ (* (expt 2 n) (bits x (1- m) 0)) (bits y (1- n) 0)) 0))
Function:
(defun formal-+ (x y) (declare (xargs :guard t)) (if (and (acl2-numberp x) (acl2-numberp y)) (+ x y) (list '+ x y)))
Function:
(defun cat-size (x) (declare (xargs :guard (and (true-listp x) (evenp (length x))))) (if (endp (cddr x)) (cadr x) (formal-+ (cadr x) (cat-size (cddr x)))))
Macro:
(defmacro cat (&rest x) (declare (xargs :guard (and x (true-listp x) (evenp (length x))))) (cond ((endp (cddr x)) (cons 'bits (cons (car x) (cons (formal-+ -1 (cadr x)) '(0))))) ((endp (cddddr x)) (cons 'binary-cat x)) (t (cons 'binary-cat (cons (car x) (cons (cadr x) (cons (cons 'cat (cddr x)) (cons (cat-size (cddr x)) 'nil))))))))
Theorem:
(defthm cat-nonnegative-integer-type (and (integerp (cat x m y n)) (<= 0 (cat x m y n))) :rule-classes (:type-prescription))
Theorem:
(defthm cat-bvecp (implies (and (<= (+ m n) k) (case-split (integerp k))) (bvecp (cat x m y n) k)))
Theorem:
(defthm cat-with-n-0 (equal (binary-cat x m y 0) (bits x (1- m) 0)))
Theorem:
(defthm cat-with-m-0 (equal (binary-cat x 0 y n) (bits y (1- n) 0)))
Theorem:
(defthm cat-0 (implies (and (case-split (bvecp y n)) (case-split (integerp n)) (case-split (integerp m)) (case-split (<= 0 m))) (equal (cat 0 m y n) y)))
Theorem:
(defthm cat-bits-1 (equal (cat (bits x (1- m) 0) m y n) (cat x m y n)))
Theorem:
(defthm cat-bits-2 (equal (cat x m (bits y (1- n) 0) n) (cat x m y n)))
Theorem:
(defthm cat-bits-3 (implies (and (integerp i) (integerp m) (>= i (1- m))) (equal (cat (bits x i 0) m y n) (cat x m y n))))
Theorem:
(defthm cat-bits-4 (implies (and (integerp i) (integerp n) (>= i (1- n))) (equal (cat x m (bits y i 0) n) (cat x m y n))))
Theorem:
(defthm cat-associative (implies (and (case-split (<= (+ m n) p)) (case-split (<= 0 m)) (case-split (<= 0 n)) (case-split (<= 0 q)) (case-split (integerp m)) (case-split (integerp n)) (case-split (integerp p)) (case-split (integerp q))) (equal (cat (cat x m y n) p z q) (cat x m (cat y n z q) (+ n q)))))
Theorem:
(defthm cat-equal-constant (implies (and (syntaxp (and (quotep k) (quotep m) (quotep n))) (case-split (bvecp y n)) (case-split (bvecp x m)) (case-split (< k (expt 2 (+ m n)))) (case-split (integerp k)) (case-split (<= 0 k)) (case-split (integerp m)) (case-split (<= 0 m)) (case-split (integerp n)) (case-split (<= 0 n))) (equal (equal k (cat x m y n)) (and (equal y (bits k (1- n) 0)) (equal x (bits k (+ -1 m n) n))))))
Theorem:
(defthm cat-equal-rewrite (implies (and (case-split (bvecp x1 m)) (case-split (bvecp y1 n)) (case-split (bvecp x2 m)) (case-split (bvecp y2 n)) (case-split (integerp n)) (case-split (<= 0 n)) (case-split (integerp m)) (case-split (<= 0 m))) (equal (equal (cat x1 m y1 n) (cat x2 m y2 n)) (and (equal x1 x2) (equal y1 y2)))))
Theorem:
(defthm cat-bits-bits (implies (and (equal j (1+ k)) (equal n (+ 1 (- l) k)) (case-split (<= (+ 1 (- j) i) m)) (case-split (<= j i)) (case-split (<= l k)) (case-split (integerp i)) (case-split (integerp k)) (case-split (integerp l)) (case-split (integerp m))) (equal (cat (bits x i j) m (bits x k l) n) (bits x i l))))
Theorem:
(defthm cat-bitn-bits (implies (and (equal j (1+ k)) (equal n (+ 1 (- l) k)) (case-split (<= 1 m)) (case-split (<= l k)) (case-split (integerp j)) (case-split (integerp k)) (case-split (integerp l)) (case-split (integerp m))) (equal (cat (bitn x j) m (bits x k l) n) (bits x j l))))
Theorem:
(defthm cat-bits-bitn (implies (and (equal j (1+ k)) (case-split (<= (+ 1 (- j) i) m)) (case-split (<= j i)) (case-split (integerp i)) (case-split (integerp j)) (case-split (integerp k)) (case-split (integerp m))) (equal (cat (bits x i j) m (bitn x k) 1) (bits x i k))))
Theorem:
(defthm cat-bitn-bitn (implies (and (equal i (1+ j)) (case-split (integerp i)) (case-split (integerp j))) (equal (cat (bitn x i) 1 (bitn x j) 1) (bits x i j))))
Theorem:
(defthm bits-cat (implies (and (case-split (natp n)) (case-split (natp m)) (case-split (natp i)) (case-split (natp j))) (equal (bits (cat x m y n) i j) (if (< i n) (bits y i j) (if (>= j n) (bits x (if (< i (+ m n)) (- i n) (1- m)) (- j n)) (cat (bits x (if (< i (+ m n)) (- i n) (1- m)) 0) (1+ (- i n)) (bits y (1- n) j) (- n j)))))))
Theorem:
(defthm bits-cat-constants (implies (and (syntaxp (quotep n)) (syntaxp (quotep m)) (syntaxp (quotep i)) (syntaxp (quotep j)) (natp n) (natp m) (natp i) (natp j)) (equal (bits (cat x m y n) i j) (if (< i n) (bits y i j) (if (>= j n) (bits x (if (< i (+ m n)) (- i n) (1- m)) (- j n)) (cat (bits x (if (< i (+ m n)) (- i n) (1- m)) 0) (1+ (- i n)) (bits y (1- n) j) (- n j)))))))
Theorem:
(defthm bitn-cat (implies (and (case-split (natp n)) (case-split (natp m)) (case-split (natp i))) (equal (bitn (cat x m y n) i) (if (< i n) (bitn y i) (if (< i (+ m n)) (bitn x (- i n)) 0)))))
Theorem:
(defthm bitn-cat-constants (implies (and (syntaxp (quotep n)) (syntaxp (quotep m)) (syntaxp (quotep i)) (natp n) (natp m) (natp i)) (equal (bitn (cat x m y n) i) (if (< i n) (bitn y i) (if (< i (+ m n)) (bitn x (- i n)) 0)))))
Function:
(defun mulcat (l n x) (declare (xargs :guard (and (natp l) (natp n) (natp x)))) (if (and (integerp n) (> n 0)) (cat (mulcat l (1- n) x) (* l (1- n)) x l) 0))
Theorem:
(defthm mulcat-nonnegative-integer-type (and (integerp (mulcat l n x)) (<= 0 (mulcat l n x))) :rule-classes (:type-prescription))
Theorem:
(defthm mulcat-bits (implies (and (integerp l) (integerp x)) (equal (mulcat l n (bits x (1- l) 0)) (mulcat l n x))))
Theorem:
(defthm mulcat-bvecp (implies (and (>= p (* l n)) (case-split (integerp p)) (case-split (natp l))) (bvecp (mulcat l n x) p)))
Theorem:
(defthm mulcat-1 (implies (natp l) (equal (mulcat l 1 x) (bits x (1- l) 0))))
Theorem:
(defthm mulcat-0 (equal (mulcat l n 0) 0))
Theorem:
(defthm mulcat-n-1 (implies (case-split (<= 0 n)) (equal (mulcat 1 n 1) (1- (expt 2 n)))))
Theorem:
(defthm bitn-mulcat-1 (implies (and (< m n) (case-split (bvecp x 1)) (case-split (natp m)) (case-split (integerp n))) (equal (bitn (mulcat 1 n x) m) x)))