signed-byte-listp

(in-package "ACL2")

(set-verify-guards-eagerness 2)

(defsection signed-byte-listp
  :parents (std/typed-lists signed-byte-p)
  :short "Recognizer for lists of @(see signed-byte-p)'s."
  :long "<p>BOZO consider switching this book to use deflist.</p>"
  (defund signed-byte-listp
    (n x)
    (if (atom x)
      (null x)
      (and (signed-byte-p n (car x))
        (signed-byte-listp n (cdr x)))))
  (defthm signed-byte-listp-when-atom
    (implies (atom x) (equal (signed-byte-listp n x) (not x)))
    :hints (("Goal" :in-theory (enable signed-byte-listp))))
  (defthm signed-byte-listp-of-cons
    (equal (signed-byte-listp n (cons a x))
      (and (signed-byte-p n a) (signed-byte-listp n x)))
    :hints (("Goal" :in-theory (enable signed-byte-listp))))
  (defthm true-listp-when-signed-byte-listp
    (implies (signed-byte-listp width x) (true-listp x))
    :hints (("Goal" :induct (len x)))))