Built-in axioms and theorems about arrays.
Theorem:
(defthm array1p-forward (implies (array1p name l) (and (symbolp name) (alistp l) (keyword-value-listp (cdr (assoc-eq :header l))) (true-listp (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))) (equal (length (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))) 1) (integerp (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))) (integerp (cadr (assoc-keyword :maximum-length (cdr (assoc-eq :header l))))) (< 0 (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))) (< (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))) (cadr (assoc-keyword :maximum-length (cdr (assoc-eq :header l))))) (<= (cadr (assoc-keyword :maximum-length (cdr (assoc-eq :header l)))) (array-maximum-length-bound)) (bounded-integer-alistp l (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))))) :rule-classes :forward-chaining)
Theorem:
(defthm array1p-linear (implies (array1p name l) (and (< 0 (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))) (< (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))) (cadr (assoc-keyword :maximum-length (cdr (assoc-eq :header l))))) (<= (cadr (assoc-keyword :maximum-length (cdr (assoc-eq :header l)))) (array-maximum-length-bound)))) :rule-classes ((:linear :match-free :all)))
Theorem:
(defthm array2p-forward (implies (array2p name l) (and (symbolp name) (alistp l) (keyword-value-listp (cdr (assoc-eq :header l))) (true-listp (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))) (equal (length (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))) 2) (integerp (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))) (integerp (cadr (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))) (integerp (cadr (assoc-keyword :maximum-length (cdr (assoc-eq :header l))))) (< 0 (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))) (< 0 (cadr (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))) (< (* (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))) (cadr (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))) (cadr (assoc-keyword :maximum-length (cdr (assoc-eq :header l))))) (<= (cadr (assoc-keyword :maximum-length (cdr (assoc-eq :header l)))) (array-maximum-length-bound)) (bounded-integer-alistp2 l (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))) (cadr (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))))) :rule-classes :forward-chaining)
Theorem:
(defthm array2p-linear (implies (array2p name l) (and (< 0 (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))) (< 0 (cadr (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))) (< (* (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))) (cadr (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))) (cadr (assoc-keyword :maximum-length (cdr (assoc-eq :header l))))) (<= (cadr (assoc-keyword :maximum-length (cdr (assoc-eq :header l)))) (array-maximum-length-bound)))) :rule-classes ((:linear :match-free :all)))
Theorem:
(defthm array1p-cons (implies (and (< n (caadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))) (not (< n 0)) (integerp n) (array1p name l)) (array1p name (cons (cons n val) l))))
Theorem:
(defthm array2p-cons (implies (and (< j (cadr (dimensions name l))) (not (< j 0)) (integerp j) (< i (car (dimensions name l))) (not (< i 0)) (integerp i) (array2p name l)) (array2p name (cons (cons (cons i j) val) l))))