nat-listp

(in-package "ACL2")

(defsection arithmetic/nat-listp
  :parents (nat-listp)
  :short "Lemmas about @(see nat-listp) available in the @('arithmetic/nat-listp')
book."
  :long "<p>Note: this book is extremely minimal.  You should generally instead
see @(see std/typed-lists/nat-listp).  Note however that this book is part
of a widely-used library of basic arithmetic facts: @('(include-book
"arithmetic/top" :dir :system)').</p>"
  (local (in-theory (enable nat-listp)))
  (defthm nat-listp-implies-true-listp
    (implies (nat-listp x) (true-listp x))
    :rule-classes (:rewrite :compound-recognizer))
  (in-theory (disable (:rewrite nat-listp-implies-true-listp)))
  (defthm nat-listp-when-not-consp
    (implies (not (consp x)) (equal (nat-listp x) (not x)))
    :hints (("Goal" :in-theory (enable nat-listp))))
  (defthm nat-listp-of-cons
    (equal (nat-listp (cons a x)) (and (natp a) (nat-listp x)))
    :hints (("Goal" :in-theory (enable nat-listp))))
  (defthm nat-listp-of-append-weak
    (implies (true-listp x)
      (equal (nat-listp (append x y))
        (and (nat-listp x) (nat-listp y)))))
  (defthm car-nat-listp
    (implies (and (nat-listp x) x) (natp (car x)))
    :rule-classes :forward-chaining)
  (defthm nat-listp-of-cdr-when-nat-listp
    (implies (nat-listp (double-rewrite x)) (nat-listp (cdr x)))))