Built-in axioms and theorems about lists.
Theorem:
(defthm symbol-listp-forward-to-eqlable-listp (implies (symbol-listp x) (eqlable-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm eqlable-listp-forward-to-atom-listp (implies (eqlable-listp x) (atom-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm atom-listp-forward-to-true-listp (implies (atom-listp x) (true-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm true-listp-append (implies (true-listp b) (true-listp (append a b))) :rule-classes :type-prescription)
Theorem:
(defthm append-to-nil (implies (true-listp x) (equal (append x nil) x)))
Theorem:
(defthm character-listp-forward-to-eqlable-listp (implies (character-listp x) (eqlable-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm standard-char-listp-forward-to-character-listp (implies (standard-char-listp x) (character-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm atom-listp-forward-to-true-listp (implies (atom-listp x) (true-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm eqlable-listp-forward-to-atom-listp (implies (eqlable-listp x) (atom-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm true-listp-revappend-type-prescription (implies (true-listp y) (true-listp (revappend x y))) :rule-classes :type-prescription)
Theorem:
(defthm keyword-value-listp-forward-to-true-listp (implies (keyword-value-listp x) (true-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm true-list-listp-forward-to-true-listp (implies (true-list-listp x) (true-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm true-listp-nthcdr-type-prescription (implies (true-listp x) (true-listp (nthcdr n x))) :rule-classes :type-prescription)
Theorem:
(defthm keyword-value-listp-assoc-keyword (implies (keyword-value-listp l) (keyword-value-listp (assoc-keyword key l))) :rule-classes ((:forward-chaining :trigger-terms ((assoc-keyword key l)))))
Theorem:
(defthm acl2-number-listp-forward-to-true-listp (implies (acl2-number-listp x) (true-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm rational-listp-forward-to-acl2-number-listp (implies (rational-listp x) (acl2-number-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm integer-listp-forward-to-rational-listp (implies (integer-listp x) (rational-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm nat-listp-forward-to-integer-listp (implies (nat-listp x) (integer-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm nth-update-nth (equal (nth m (update-nth n val l)) (if (equal (nfix m) (nfix n)) val (nth m l))))
Theorem:
(defthm true-listp-update-nth (implies (true-listp l) (true-listp (update-nth key val l))) :rule-classes :type-prescription)
Theorem:
(defthm nth-update-nth-array (equal (nth m (update-nth-array n i val l)) (if (equal (nfix m) (nfix n)) (update-nth i val (nth m l)) (nth m l))))
Theorem:
(defthm len-update-nth (equal (len (update-nth n val x)) (max (1+ (nfix n)) (len x))))
Theorem:
(defthm nth-0-cons (equal (nth 0 (cons a l)) a))
Theorem:
(defthm nth-add1 (implies (and (integerp n) (>= n 0)) (equal (nth (+ 1 n) (cons a l)) (nth n l))))
Theorem:
(defthm last-cdr-is-nil (implies (true-listp x) (equal (last-cdr x) nil)))
Theorem:
(defthm pairlis$-true-list-fix (equal (pairlis$ x (true-list-fix y)) (pairlis$ x y)))
Theorem:
(defthm true-listp-first-n-ac-type-prescription (true-listp (first-n-ac i l ac)) :rule-classes :type-prescription)
Theorem:
(defthm natp-position-ac-eq-exec (implies (natp acc) (or (natp (position-ac-eq-exec item lst acc)) (equal (position-ac-eq-exec item lst acc) nil))) :rule-classes :type-prescription)
Theorem:
(defthm natp-position-ac-eql-exec (implies (natp acc) (or (natp (position-ac-eql-exec item lst acc)) (equal (position-ac-eql-exec item lst acc) nil))) :rule-classes :type-prescription)
Theorem:
(defthm natp-position-equal-ac (implies (natp acc) (or (natp (position-equal-ac item lst acc)) (equal (position-equal-ac item lst acc) nil))) :rule-classes :type-prescription)
Theorem:
(defthm natp-position-ac (implies (and (integerp acc) (<= 0 acc)) (or (equal (position-ac item lst acc) nil) (and (integerp (position-ac item lst acc)) (<= 0 (position-ac item lst acc))))) :rule-classes :type-prescription)
Theorem:
(defthm position-ac-eq-exec-is-position-equal-ac (equal (position-ac-eq-exec item lst acc) (position-equal-ac item lst acc)))
Theorem:
(defthm position-ac-eql-exec-is-position-equal-ac (equal (position-ac-eql-exec item lst acc) (position-equal-ac item lst acc)))
Theorem:
(defthm position-eq-exec-is-position-equal (implies (not (stringp lst)) (equal (position-eq-exec item lst) (position-equal item lst))))
Theorem:
(defthm position-eql-exec-is-position-equal (equal (position-eql-exec item lst) (position-equal item lst)))
Theorem:
(defthm member-eq-exec-is-member-equal (equal (member-eq-exec x l) (member-equal x l)))
Theorem:
(defthm member-eql-exec-is-member-equal (equal (member-eql-exec x l) (member-equal x l)))
Theorem:
(defthm subsetp-eq-exec-is-subsetp-equal (equal (subsetp-eq-exec x y) (subsetp-equal x y)))
Theorem:
(defthm subsetp-eql-exec-is-subsetp-equal (equal (subsetp-eql-exec x y) (subsetp-equal x y)))
Theorem:
(defthm no-duplicatesp-eq-exec-is-no-duplicatesp-equal (equal (no-duplicatesp-eq-exec x) (no-duplicatesp-equal x)))
Theorem:
(defthm no-duplicatesp-eql-exec-is-no-duplicatesp-equal (equal (no-duplicatesp-eql-exec x) (no-duplicatesp-equal x)))
Theorem:
(defthm remove-eq-exec-is-remove-equal (equal (remove-eq-exec x l) (remove-equal x l)))
Theorem:
(defthm remove-eql-exec-is-remove-equal (equal (remove-eql-exec x l) (remove-equal x l)))
Theorem:
(defthm remove1-eq-exec-is-remove1-equal (equal (remove1-eq-exec x l) (remove1-equal x l)))
Theorem:
(defthm remove1-eql-exec-is-remove1-equal (equal (remove1-eql-exec x l) (remove1-equal x l)))
Theorem:
(defthm remove-duplicates-eq-exec-is-remove-duplicates-equal (equal (remove-duplicates-eq-exec x) (remove-duplicates-equal x)))
Theorem:
(defthm remove-duplicates-eql-exec-is-remove-duplicates-equal (equal (remove-duplicates-eql-exec x) (remove-duplicates-equal x)))
Theorem:
(defthm set-difference-eq-exec-is-set-difference-equal (equal (set-difference-eq-exec l1 l2) (set-difference-equal l1 l2)))
Theorem:
(defthm set-difference-eql-exec-is-set-difference-equal (equal (set-difference-eql-exec l1 l2) (set-difference-equal l1 l2)))
Theorem:
(defthm add-to-set-eq-exec-is-add-to-set-equal (equal (add-to-set-eq-exec x lst) (add-to-set-equal x lst)))
Theorem:
(defthm add-to-set-eql-exec-is-add-to-set-equal (equal (add-to-set-eql-exec x lst) (add-to-set-equal x lst)))
Theorem:
(defthm union-eq-exec-is-union-equal (equal (union-eq-exec l1 l2) (union-equal l1 l2)))
Theorem:
(defthm union-eql-exec-is-union-equal (equal (union-eql-exec l1 l2) (union-equal l1 l2)))
Theorem:
(defthm intersectp-eq-exec-is-intersectp-equal (equal (intersectp-eq-exec x y) (intersectp-equal x y)))
Theorem:
(defthm intersectp-eql-exec-is-intersectp-equal (equal (intersectp-eql-exec x y) (intersectp-equal x y)))
Theorem:
(defthm intersection-eq-exec-is-intersection-equal (equal (intersection-eq-exec l1 l2) (intersection-equal l1 l2)))
Theorem:
(defthm intersection-eql-exec-is-intersection-equal (equal (intersection-eql-exec l1 l2) (intersection-equal l1 l2)))
Theorem:
(defthm pairlis$-tailrec-is-pairlis$ (implies (true-listp acc) (equal (pairlis$-tailrec x y acc) (revappend acc (pairlis$ x y)))))
Theorem:
(defthm resize-list-exec-is-resize-list (implies (true-listp acc) (equal (resize-list-exec lst n default-value acc) (revappend acc (resize-list lst n default-value)))))
Theorem:
(defthm typed-io-listp-forward-to-true-listp (implies (typed-io-listp x typ) (true-listp x)) :rule-classes :forward-chaining)