cons - ACL2 Book

other

(in-package "ACL2")

equal-of-constheorem

(defthm equal-of-cons
  (implies (syntaxp (not (and (quotep x) (quotep y))))
    (equal (equal (cons x y) z)
      (and (consp z) (equal x (car z)) (equal y (cdr z))))))

equal-of-cons-when-constanttheorem

(defthmd equal-of-cons-when-constant
  (implies (syntaxp (and (quotep x) (quotep y)))
    (equal (equal (cons x y) z)
      (and (consp z) (equal x (car z)) (equal y (cdr z))))))

equal-of-cons-and-constheorem

(defthm equal-of-cons-and-cons
  (equal (equal (cons a x) (cons b y))
    (and (equal a b) (equal x y))))

true-listp-of-constheorem

(defthm true-listp-of-cons
  (equal (true-listp (cons a x)) (true-listp x))
  :hints (("Goal" :cases ((true-listp x)))))

equal-cons-cases2theorem

(defthmd equal-cons-cases2
  (equal (equal (cons a b) c)
    (and (consp c) (equal a (car c)) (equal b (cdr c)))))

equal-cons-cases2-alttheorem

(defthmd equal-cons-cases2-alt
  (equal (equal c (cons a b))
    (and (consp c) (equal a (car c)) (equal b (cdr c)))))

equal-of-cons-and-cons-same-arg2theorem

(defthm equal-of-cons-and-cons-same-arg2
  (equal (equal (cons x y) (cons z y)) (equal x z)))