Lemmas about nat-listp available in the
Note: this book is extremely minimal. You should generally instead
see std/typed-lists/nat-listp. Note however that this book is part
of a widely-used library of basic arithmetic facts:
Theorem:
(defthm nat-listp-implies-true-listp (implies (nat-listp x) (true-listp x)) :rule-classes (:rewrite :compound-recognizer))
Theorem:
(defthm nat-listp-when-not-consp (implies (not (consp x)) (equal (nat-listp x) (not x))))
Theorem:
(defthm nat-listp-of-cons (equal (nat-listp (cons a x)) (and (natp a) (nat-listp x))))
Theorem:
(defthm nat-listp-of-append-weak (implies (true-listp x) (equal (nat-listp (append x y)) (and (nat-listp x) (nat-listp y)))))
Theorem:
(defthm car-nat-listp (implies (and (nat-listp x) x) (natp (car x))) :rule-classes :forward-chaining)
Theorem:
(defthm nat-listp-of-cdr-when-nat-listp (implies (nat-listp (double-rewrite x)) (nat-listp (cdr x))))