Built-in axioms and theorems about alists.
Theorem:
(defthm alistp-forward-to-true-listp (implies (alistp x) (true-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm eqlable-alistp-forward-to-alistp (implies (eqlable-alistp x) (alistp x)) :rule-classes :forward-chaining)
Theorem:
(defthm symbol-alistp-forward-to-eqlable-alistp (implies (symbol-alistp x) (eqlable-alistp x)) :rule-classes :forward-chaining)
Theorem:
(defthm character-alistp-forward-to-eqlable-alistp (implies (character-alistp x) (eqlable-alistp x)) :rule-classes :forward-chaining)
Theorem:
(defthm nat-alistp-forward-to-eqlable-alistp (implies (nat-alistp x) (eqlable-alistp x)) :rule-classes :forward-chaining)
Theorem:
(defthm fixnat-alistp-forward-to-nat-alistp (implies (fixnat-alistp x) (nat-alistp x)) :rule-classes :forward-chaining)
Theorem:
(defthm string-alistp-forward-to-alistp (implies (string-alistp x) (alistp x)) :rule-classes :forward-chaining)
Theorem:
(defthm consp-assoc-equal (implies (alistp l) (or (consp (assoc-equal name l)) (equal (assoc-equal name l) nil))) :rule-classes (:type-prescription (:forward-chaining :trigger-terms ((assoc-equal name l)))))
Theorem:
(defthm known-package-alistp-forward-to-true-list-listp-and-alistp (implies (known-package-alistp x) (and (true-list-listp x) (alistp x))) :rule-classes :forward-chaining)
Theorem:
(defthm true-list-listp-forward-to-true-listp-assoc-equal (implies (true-list-listp l) (true-listp (assoc-equal key l))) :rule-classes (:type-prescription (:forward-chaining :trigger-terms ((assoc-equal key l)))))
Theorem:
(defthm ordered-symbol-alistp-forward-to-symbol-alistp (implies (ordered-symbol-alistp x) (symbol-alistp x)) :rule-classes :forward-chaining)
Theorem:
(defthm ordered-symbol-alistp-remove1-assoc-eq (implies (ordered-symbol-alistp l) (ordered-symbol-alistp (remove1-assoc-eq key l))))
Theorem:
(defthm ordered-symbol-alistp-add-pair (implies (and (ordered-symbol-alistp gs) (symbolp w5)) (ordered-symbol-alistp (add-pair w5 w6 gs))))
Theorem:
(defthm ordered-symbol-alistp-add-pair-forward (implies (and (symbolp key) (ordered-symbol-alistp l)) (ordered-symbol-alistp (add-pair key value l))) :rule-classes ((:forward-chaining :trigger-terms ((add-pair key value l)))))
Theorem:
(defthm assoc-add-pair (equal (assoc sym1 (add-pair sym2 val alist)) (if (equal sym1 sym2) (cons sym1 val) (assoc sym1 alist))))
Theorem:
(defthm add-pair-preserves-all-boundp (implies (all-boundp alist1 alist2) (all-boundp alist1 (add-pair sym val alist2))))
Theorem:
(defthm bounded-integer-alistp-forward-to-eqlable-alistp (implies (bounded-integer-alistp x n) (eqlable-alistp x)) :rule-classes :forward-chaining)
Theorem:
(defthm assoc-eq-exec-is-assoc-equal (equal (assoc-eq-exec x l) (assoc-equal x l)))
Theorem:
(defthm assoc-eql-exec-is-assoc-equal (equal (assoc-eql-exec x l) (assoc-equal x l)))
Theorem:
(defthm rassoc-eq-exec-is-rassoc-equal (equal (rassoc-eq-exec x alist) (rassoc-equal x alist)))
Theorem:
(defthm rassoc-eql-exec-is-rassoc-equal (equal (rassoc-eql-exec x alist) (rassoc-equal x alist)))
Theorem:
(defthm remove1-assoc-eq-exec-is-remove1-assoc-equal (equal (remove1-assoc-eq-exec key lst) (remove1-assoc-equal key lst)))
Theorem:
(defthm remove1-assoc-eql-exec-is-remove1-assoc-equal (equal (remove1-assoc-eql-exec key lst) (remove1-assoc-equal key lst)))
Theorem:
(defthm remove-assoc-eq-exec-is-remove-assoc-equal (equal (remove-assoc-eq-exec x l) (remove-assoc-equal x l)))
Theorem:
(defthm remove-assoc-eql-exec-is-remove-assoc-equal (equal (remove-assoc-eql-exec x l) (remove-assoc-equal x l)))
Theorem:
(defthm put-assoc-eq-exec-is-put-assoc-equal (equal (put-assoc-eq-exec name val alist) (put-assoc-equal name val alist)))
Theorem:
(defthm put-assoc-eql-exec-is-put-assoc-equal (equal (put-assoc-eql-exec name val alist) (put-assoc-equal name val alist)))
Theorem:
(defthm timer-alistp-forward-to-true-list-listp-and-symbol-alistp (implies (timer-alistp x) (and (true-list-listp x) (symbol-alistp x))) :rule-classes :forward-chaining)
Theorem:
(defthm all-boundp-preserves-assoc-equal (implies (and (all-boundp tbl1 tbl2) (assoc-equal x tbl1)) (assoc-equal x tbl2)) :rule-classes nil)