Built-in axioms and theorems about cons pairs.
Definition:
(defaxiom car-cdr-elim (implies (consp x) (equal (cons (car x) (cdr x)) x)) :rule-classes :elim)
Definition:
(defaxiom car-cons (equal (car (cons x y)) x))
Definition:
(defaxiom cdr-cons (equal (cdr (cons x y)) y))
Definition:
(defaxiom cons-equal (equal (equal (cons x1 y1) (cons x2 y2)) (and (equal x1 x2) (equal y1 y2))))
Definition:
(defaxiom completion-of-car (equal (car x) (cond ((consp x) (car x)) (t nil))) :rule-classes nil)
Definition:
(defaxiom completion-of-cdr (equal (cdr x) (cond ((consp x) (cdr x)) (t nil))) :rule-classes nil)
Theorem:
(defthm default-car (implies (not (consp x)) (equal (car x) nil)))
Theorem:
(defthm default-cdr (implies (not (consp x)) (equal (cdr x) nil)))
Theorem:
(defthm cons-car-cdr (equal (cons (car x) (cdr x)) (if (consp x) x (cons nil nil))))