nat-listp

(in-package "ACL2")

(defsection std/typed-lists/nat-listp
  :parents (nat-listp)
  :short "Lemmas about @(see nat-listp) available in the @(see std/typed-lists)
library."
  :long "<p>Most of these are generated automatically with @(see
std::deflist).</p>

<p>BOZO some additional lemmas are found in @('arithmetic/nat-listp').</p>"
  (deflist nat-listp
    (x)
    (natp x)
    :true-listp t
    :elementp-of-nil nil
    :already-definedp t
    :parents nil)
  (defthm integerp-of-car-when-nat-listp
    (implies (nat-listp x) (equal (integerp (car x)) (consp x))))
  (defthm lower-bound-of-car-when-nat-listp
    (implies (nat-listp x) (<= 0 (car x)))
    :rule-classes ((:rewrite) (:linear))
    :hints (("Goal" :induct (len x))))
  (defthm nat-listp-of-remove-equal
    (implies (nat-listp x) (nat-listp (remove-equal a x)))
    :hints (("Goal" :in-theory (enable remove))))
  (defthm nat-listp-of-make-list-ac
    (equal (nat-listp (make-list-ac n x ac))
      (and (nat-listp ac) (or (natp x) (zp n))))
    :hints (("Goal" :in-theory (enable make-list-ac))))
  (defthm eqlable-listp-when-nat-listp
    (implies (nat-listp x) (eqlable-listp x))
    :hints (("Goal" :in-theory (enable eqlable-listp eqlablep)))))