acons - ACL2 Book

other

(in-package "ACL2")

in-theory

(in-theory (disable acons))

alistp-of-aconstheorem

(defthm alistp-of-acons
  (equal (alistp (acons key datum alist)) (alistp alist))
  :hints (("Goal" :in-theory (enable acons))))

car-of-aconstheorem

(defthm car-of-acons
  (equal (car (acons key datum alist)) (cons key datum))
  :hints (("Goal" :in-theory (enable acons))))

cdr-of-aconstheorem

(defthm cdr-of-acons
  (equal (cdr (acons key datum alist)) alist)
  :hints (("Goal" :in-theory (enable acons))))

strip-cars-of-aconstheorem

(defthm strip-cars-of-acons
  (equal (strip-cars (acons key datum alist))
    (cons key (strip-cars alist)))
  :hints (("Goal" :in-theory (enable acons))))

strip-cdrs-of-aconstheorem

(defthm strip-cdrs-of-acons
  (equal (strip-cdrs (acons key datum alist))
    (cons datum (strip-cdrs alist)))
  :hints (("Goal" :in-theory (enable acons))))

len-of-aconstheorem

(defthm len-of-acons
  (equal (len (acons key datum alist)) (+ 1 (len alist)))
  :hints (("Goal" :in-theory (enable acons))))

equal-of-acons-and-aconstheorem

(defthm equal-of-acons-and-acons
  (equal (equal (acons key1 datum1 alist1)
      (acons key2 datum2 alist2))
    (and (equal key1 key2)
      (equal datum1 datum2)
      (equal alist1 alist2)))
  :hints (("Goal" :in-theory (enable acons))))

true-listp-of-aconstheorem

(defthm true-listp-of-acons
  (equal (true-listp (acons key datum alist))
    (true-listp alist))
  :hints (("Goal" :in-theory (enable acons))))