		Search-engine friendly clone of the ACL2 documentation.

Defaggregate

Prod-cons

Special constructor for products that collapses (nil . nil) into nil.

Definitions and Theorems

Function: prod-cons$inline

(defun prod-cons$inline (x y)
  (declare (xargs :guard t))
  (and (or x y) (cons x y)))

Theorem: prod-consp-of-prod-cons

(defthm prod-consp-of-prod-cons
  (prod-consp (prod-cons x y))
  :rule-classes (:rewrite :type-prescription))

Theorem: car-of-prod-cons

(defthm car-of-prod-cons
  (equal (car (prod-cons x y)) x))

Theorem: cdr-of-prod-cons

(defthm cdr-of-prod-cons
  (equal (cdr (prod-cons x y)) y))

Theorem: prod-cons-of-car/cdr

(defthm prod-cons-of-car/cdr
  (implies (prod-consp x)
           (equal (prod-cons (car x) (cdr x)) x)))

Theorem: equal-of-prod-cons

(defthm equal-of-prod-cons
  (implies (prod-consp x)
           (equal (equal x (prod-cons a b))
                  (and (equal (car x) a)
                       (equal (cdr x) b)))))

Theorem: acl2-count-of-prod-cons

(defthm acl2-count-of-prod-cons
  (and (>= (acl2-count (prod-cons x y))
           (acl2-count x))
       (>= (acl2-count (prod-cons x y))
           (acl2-count y)))
  :rule-classes :linear)

Theorem: prod-cons-equal-cons

(defthm prod-cons-equal-cons
  (implies (or a b)
           (equal (equal (prod-cons a b) (cons c d))
                  (and (equal a c) (equal b d)))))

Theorem: prod-cons-when-either

(defthm prod-cons-when-either
 (implies (or a b)
          (and (prod-cons a b)
               (consp (prod-cons a b))))
 :rule-classes ((:rewrite)
                (:type-prescription
                     :corollary (implies (or a b)
                                         (consp (prod-cons a b))))))

Theorem: prod-cons-not-consp-forward

(defthm prod-cons-not-consp-forward
  (implies (not (consp (prod-cons a b)))
           (and (not a) (not b)))
  :rule-classes
  ((:forward-chaining :trigger-terms ((prod-cons a b)))))

Subtopics

Prod-consp: Special recognizer for conses, except that to save space we require that (nil . nil) be represented just as nil.
Prod-cons-with-hint: Same as prod-cons, but avoids reconsing like cons-with-hint.
Prod-hons: Same as prod-cons but uses hons.
Prod-cdr: Same as cdr, but guarded with prod-consp.
Prod-car: Same as car, but guarded with prod-consp.