		Search-engine friendly clone of the ACL2 documentation.

Built-in-theorems-about-cons-pairs

Built-in theorems about cons pairs.

Definition: car-cdr-elim

(defaxiom car-cdr-elim
          (implies (consp x)
                   (equal (cons (car x) (cdr x)) x))
          :rule-classes :elim)

Definition: car-cons

(defaxiom car-cons (equal (car (cons x y)) x))

Definition: cdr-cons

(defaxiom cdr-cons (equal (cdr (cons x y)) y))

Definition: cons-equal

(defaxiom cons-equal
          (equal (equal (cons x1 y1) (cons x2 y2))
                 (and (equal x1 x2) (equal y1 y2))))

Definition: completion-of-car

(defaxiom completion-of-car
          (equal (car x)
                 (cond ((consp x) (car x)) (t nil)))
          :rule-classes nil)

Definition: completion-of-cdr

(defaxiom completion-of-cdr
          (equal (cdr x)
                 (cond ((consp x) (cdr x)) (t nil)))
          :rule-classes nil)

Theorem: default-car

(defthm default-car
        (implies (not (consp x))
                 (equal (car x) nil)))

Theorem: default-cdr

(defthm default-cdr
        (implies (not (consp x))
                 (equal (cdr x) nil)))

Theorem: cons-car-cdr

(defthm cons-car-cdr
        (equal (cons (car x) (cdr x))
               (if (consp x) x (cons nil nil))))