alistp

(in-package "ACL2")

(defsection std/alists/alistp
  :parents (std/alists alistp)
  :short "Lemmas about @(see alistp) available in the @(see std/alists)
library."
  :long "<p>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.</p>"
  (defthm alistp-when-atom
    (implies (atom x) (equal (alistp x) (not x))))
  (defthm alistp-of-cons
    (equal (alistp (cons a x)) (and (consp a) (alistp x))))
  (defthm true-listp-when-alistp
    (implies (alistp x) (true-listp x))
    :rule-classes :compound-recognizer)
  (defthmd true-listp-when-alistp-rewrite
    (implies (alistp x) (true-listp x)))
  (defthm alistp-of-append
    (equal (alistp (append x y))
      (and (alistp (list-fix x)) (alistp y)))
    :hints (("Goal" :in-theory (enable list-fix))))
  (defthm alistp-of-revappend
    (equal (alistp (revappend x y))
      (and (alistp (list-fix x)) (alistp y)))
    :hints (("Goal" :in-theory (enable list-fix))))
  (local (defthm list-fix-when-true-listp
      (implies (true-listp x) (equal (list-fix x) x))
      :hints (("Goal" :in-theory (enable list-fix)))))
  (defthm alistp-of-rev
    (equal (alistp (rev x)) (alistp (list-fix x)))
    :hints (("Goal" :in-theory (enable rev list-fix) :induct (len x))))
  (defthm alistp-of-reverse
    (equal (alistp (reverse x))
      (and (not (stringp x)) (alistp (list-fix x))))
    :hints (("Goal" :in-theory (enable list-fix) :induct (len x))))
  (defthm alistp-of-cdr (implies (alistp x) (alistp (cdr x))))
  (defthm consp-of-car-when-alistp
    (implies (alistp x)
      (equal (consp (car x))
        (if x
          t
          nil))))
  (defthm alistp-of-member
    (implies (alistp x) (alistp (member a x))))
  (defthm alistp-of-repeat
    (equal (alistp (repeat n x)) (or (zp n) (consp x)))
    :hints (("Goal" :in-theory (enable repeat))))
  (defthm alistp-of-take
    (implies (alistp x)
      (equal (alistp (take n x)) (<= (nfix n) (len x))))
    :hints (("Goal" :in-theory (enable take))))
  (defthm alistp-of-nthcdr
    (implies (alistp x) (alistp (nthcdr n x))))
  (defthm alistp-of-remove1-assoc-equal
    (implies (alistp x) (alistp (remove1-assoc-equal key x))))
  (defthm alistp-of-pairlis$ (alistp (pairlis$ x y))))