atom-listp

(in-package "ACL2")

(defsection std/typed-lists/atom-listp
  :parents (std/typed-lists atom-listp)
  :short "Lemmas about @(see atom-listp) available in the @(see
std/typed-lists) library."
  :long "<p>Most of these are generated automatically with @(see
std::deflist).</p>"
  (in-theory (disable atom-listp))
  (deflist atom-listp
    (x)
    (consp x)
    :negatedp t
    :cheap t
    :true-listp t
    :elementp-of-nil nil
    :already-definedp t
    :parents nil)
  (defthm atom-listp-of-remove-equal
    (implies (atom-listp x) (atom-listp (remove-equal a x)))
    :hints (("Goal" :in-theory (enable remove-equal))))
  (defthm atom-listp-of-make-list-ac
    (equal (atom-listp (make-list-ac n x ac))
      (and (atom-listp ac) (or (atom x) (zp n))))
    :hints (("Goal" :in-theory (enable make-list-ac zp))))
  (defthm atom-listp-of-rev
    (equal (atom-listp (rev x)) (atom-listp (list-fix x)))
    :hints (("Goal" :induct (len x)))))