		Search-engine friendly clone of the ACL2 documentation.

Std/alists/alistp

Lemmas about alistp available in the std/alists library.

Note that "modern" alist functions do not have alistp guards and that theorems about them typically do not need any alistp hypotheses. Accordingly, you may not really need to reason about alistp at all.

Definitions and Theorems

Theorem: alistp-when-atom

(defthm alistp-when-atom
  (implies (atom x)
           (equal (alistp x) (not x))))

Theorem: alistp-of-cons

(defthm alistp-of-cons
  (equal (alistp (cons a x))
         (and (consp a) (alistp x))))

Theorem: true-listp-when-alistp

(defthm true-listp-when-alistp
  (implies (alistp x) (true-listp x))
  :rule-classes :compound-recognizer)

Theorem: true-listp-when-alistp-rewrite

(defthm true-listp-when-alistp-rewrite
  (implies (alistp x) (true-listp x)))

Theorem: alistp-of-append

(defthm alistp-of-append
  (equal (alistp (append x y))
         (and (alistp (list-fix x)) (alistp y))))

Theorem: alistp-of-revappend

(defthm alistp-of-revappend
  (equal (alistp (revappend x y))
         (and (alistp (list-fix x)) (alistp y))))

Theorem: alistp-of-rev

(defthm alistp-of-rev
  (equal (alistp (rev x))
         (alistp (list-fix x))))

Theorem: alistp-of-reverse

(defthm alistp-of-reverse
  (equal (alistp (reverse x))
         (and (not (stringp x))
              (alistp (list-fix x)))))

Theorem: alistp-of-cdr

(defthm alistp-of-cdr
  (implies (alistp x) (alistp (cdr x))))

Theorem: consp-of-car-when-alistp

(defthm consp-of-car-when-alistp
  (implies (alistp x)
           (equal (consp (car x)) (if x t nil))))

Theorem: alistp-of-member

(defthm alistp-of-member
  (implies (alistp x)
           (alistp (member a x))))

Theorem: alistp-of-repeat

(defthm alistp-of-repeat
  (equal (alistp (repeat n x))
         (or (zp n) (consp x))))

Theorem: alistp-of-take

(defthm alistp-of-take
  (implies (alistp x)
           (equal (alistp (take n x))
                  (<= (nfix n) (len x)))))

Theorem: alistp-of-nthcdr

(defthm alistp-of-nthcdr
  (implies (alistp x)
           (alistp (nthcdr n x))))

Theorem: alistp-of-remove1-assoc-equal

(defthm alistp-of-remove1-assoc-equal
  (implies (alistp x)
           (alistp (remove1-assoc-equal key x))))

Theorem: alistp-of-pairlis$

(defthm alistp-of-pairlis$
  (alistp (pairlis$ x y)))