unsigned-byte-listp

(in-package "ACL2")

(set-verify-guards-eagerness 2)

(defsection unsigned-byte-listp
  :parents (std/typed-lists unsigned-byte-p)
  :short "Recognizer for lists of @(see unsigned-byte-p)'s."
  :long "<p>BOZO consider switching this book to use deflist.</p>"
  (local (in-theory (disable unsigned-byte-p)))
  (defund unsigned-byte-listp
    (n x)
    (if (atom x)
      (null x)
      (and (unsigned-byte-p n (car x))
        (unsigned-byte-listp n (cdr x)))))
  (defthm unsigned-byte-listp-when-not-consp
    (implies (not (consp x))
      (equal (unsigned-byte-listp n x) (not x)))
    :hints (("Goal" :in-theory (enable unsigned-byte-listp))))
  (defthm unsigned-byte-listp-of-cons
    (equal (unsigned-byte-listp n (cons a x))
      (and (unsigned-byte-p n a) (unsigned-byte-listp n x)))
    :hints (("Goal" :in-theory (enable unsigned-byte-listp))))
  (defthm unsigned-byte-p-of-car-when-unsigned-byte-listp
    (implies (unsigned-byte-listp width x)
      (equal (unsigned-byte-p width (car x)) (consp x)))
    :rule-classes (:rewrite :forward-chaining))
  (defthm nat-listp-when-unsigned-byte-listp
    (implies (unsigned-byte-listp width x) (nat-listp x))
    :hints (("Goal" :induct (len x))))
  (defthm true-listp-when-unsigned-byte-listp
    (implies (unsigned-byte-listp width x) (true-listp x))
    :hints (("Goal" :induct (len x))))
  (defthm unsigned-byte-listp-of-append
    (equal (unsigned-byte-listp width (append x y))
      (and (unsigned-byte-listp width (list-fix x))
        (unsigned-byte-listp width y)))
    :hints (("Goal" :induct (len x))))
  (defthm unsigned-byte-listp-of-list-fix-when-unsigned-byte-listp
    (implies (unsigned-byte-listp width x)
      (unsigned-byte-listp width (list-fix x))))
  (defthm unsigned-byte-listp-of-repeat
    (equal (unsigned-byte-listp width (repeat n x))
      (or (zp n) (unsigned-byte-p width x)))
    :hints (("Goal" :in-theory (enable repeat))))
  (defthm unsigned-byte-listp-of-take
    (implies (unsigned-byte-listp width x)
      (equal (unsigned-byte-listp width (take n x))
        (or (zp n) (<= n (len x))))))
  (defthm unsigned-byte-listp-of-take-past-length
    (implies (and (natp k) (< (len x) k))
      (not (unsigned-byte-listp width (take k x)))))
  (defthm unsigned-byte-listp-of-nthcdr
    (implies (unsigned-byte-listp width x)
      (unsigned-byte-listp width (nthcdr n x))))
  (defthm unsigned-byte-listp-when-take-and-nthcdr
    (implies (and (unsigned-byte-listp width (take n x))
        (unsigned-byte-listp width (nthcdr n x)))
      (unsigned-byte-listp width x)))
  (defthm unsigned-byte-listp-of-update-nth
    (implies (and (unsigned-byte-listp n l) (< key (len l)))
      (equal (unsigned-byte-listp n (update-nth key val l))
        (unsigned-byte-p n val))))
  (defthm unsigned-byte-listp-of-rev
    (equal (unsigned-byte-listp n (rev bytes))
      (unsigned-byte-listp n (list-fix bytes)))
    :hints (("goal" :in-theory (enable rev))))
  (defthm unsigned-byte-p-of-nth-when-unsigned-byte-listp
    (implies (unsigned-byte-listp bits l)
      (iff (unsigned-byte-p bits (nth n l)) (< (nfix n) (len l)))))
  (defthm unsigned-byte-listp-of-make-list-ac
    (equal (unsigned-byte-listp n1 (make-list-ac n2 val ac))
      (and (unsigned-byte-listp n1 ac)
        (or (zp n2) (unsigned-byte-p n1 val)))))
  (defthm unsigned-byte-listp-of-revappend
    (equal (unsigned-byte-listp width (revappend x y))
      (and (unsigned-byte-listp width (list-fix x))
        (unsigned-byte-listp width y)))
    :hints (("goal" :induct (revappend x y)))))