alistp

other

(in-package "ACL2")

local

(local (include-book "kestrel/utilities/equal-of-booleans" :dir :system))

in-theory

(in-theory (disable alistp))

alistp-of-constheorem

(defthm alistp-of-cons
  (equal (alistp (cons a x)) (and (consp a) (alistp x)))
  :hints (("Goal" :in-theory (enable alistp))))

alistp-of-aconstheorem

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

alistp-of-appendtheorem

(defthm alistp-of-append
  (equal (alistp (append x y))
    (and (alistp (true-list-fix x)) (alistp y)))
  :hints (("Goal" :in-theory (enable append))))

alistp-true-list-fixtheorem

(defthm alistp-true-list-fix
  (implies (alistp x) (alistp (true-list-fix x)))
  :hints (("Goal" :in-theory (enable true-list-fix))))

alistp-of-union-equaltheorem

(defthm alistp-of-union-equal
  (equal (alistp (union-equal x y))
    (and (alistp (true-list-fix x)) (alistp y)))
  :hints (("Goal" :in-theory (enable union-equal))))

alistp-of-revappend-2theorem

(defthm alistp-of-revappend-2
  (equal (alistp (revappend x y))
    (and (alistp (true-list-fix x)) (alistp y)))
  :hints (("Goal" :in-theory (enable alistp revappend))))

alistp-of-reverse-2theorem

(defthm alistp-of-reverse-2
  (equal (alistp (reverse x))
    (if (stringp x)
      nil
      (alistp (true-list-fix x))))
  :hints (("Goal" :in-theory (enable alistp))))

consp-of-nth-when-alistptheorem

(defthmd consp-of-nth-when-alistp
  (implies (alistp alist)
    (equal (consp (nth n alist)) (< (nfix n) (len alist))))
  :hints (("Goal" :in-theory (enable nth len))))

consp-of-nth-when-alistp-cheaptheorem

(defthmd consp-of-nth-when-alistp-cheap
  (implies (alistp alist)
    (equal (consp (nth n alist)) (< (nfix n) (len alist))))
  :rule-classes ((:rewrite :backchain-limit-lst (0)))
  :hints (("Goal" :in-theory (enable nth len))))

alistp-of-cdrtheorem

(defthm alistp-of-cdr
  (implies (alistp x) (alistp (cdr x)))
  :hints (("Goal" :in-theory (enable alistp))))

consp-of-car-when-alistp-alttheorem

(defthmd consp-of-car-when-alistp-alt
  (implies (alistp x) (equal (consp (car x)) (consp x)))
  :hints (("Goal" :in-theory (enable alistp))))

consp-of-car-when-alistp-cheaptheorem

(defthm consp-of-car-when-alistp-cheap
  (implies (alistp x) (equal (consp (car x)) (consp x)))
  :rule-classes ((:rewrite :backchain-limit-lst (0)))
  :hints (("Goal" :in-theory (enable alistp))))

car-when-alistp-ifftheorem

(defthmd car-when-alistp-iff
  (implies (alistp x) (iff (car x) (consp x)))
  :hints (("Goal" :in-theory (enable alistp))))

car-when-alistp-iff-cheaptheorem

(defthm car-when-alistp-iff-cheap
  (implies (alistp x) (iff (car x) (consp x)))
  :rule-classes ((:rewrite :backchain-limit-lst (0)))
  :hints (("Goal" :in-theory (enable alistp))))

alistp-of-remove1-equaltheorem

(defthm alistp-of-remove1-equal
  (implies (alistp alist) (alistp (remove1-equal pair alist)))
  :hints (("Goal" :in-theory (enable remove1-equal))))

Included Books