		Search-engine friendly clone of the ACL2 documentation.

Unsigned-byte-listp

Recognizer for lists of unsigned-byte-p's.

BOZO consider switching this book to use deflist.

Definitions and Theorems

Function: unsigned-byte-listp

(defun unsigned-byte-listp (n x)
  (if (atom x)
      (null x)
    (and (unsigned-byte-p n (car x))
         (unsigned-byte-listp n (cdr x)))))

Theorem: unsigned-byte-listp-when-not-consp

(defthm unsigned-byte-listp-when-not-consp
  (implies (not (consp x))
           (equal (unsigned-byte-listp n x)
                  (not x))))

Theorem: unsigned-byte-listp-of-cons

(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))))

Theorem: unsigned-byte-p-of-car-when-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))

Theorem: nat-listp-when-unsigned-byte-listp

(defthm nat-listp-when-unsigned-byte-listp
  (implies (unsigned-byte-listp width x)
           (nat-listp x)))

Theorem: true-listp-when-unsigned-byte-listp

(defthm true-listp-when-unsigned-byte-listp
  (implies (unsigned-byte-listp width x)
           (true-listp x)))

Theorem: unsigned-byte-listp-of-append

(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))))

Theorem: unsigned-byte-listp-of-list-fix-when-unsigned-byte-listp

(defthm unsigned-byte-listp-of-list-fix-when-unsigned-byte-listp
  (implies (unsigned-byte-listp width x)
           (unsigned-byte-listp width (list-fix x))))

Theorem: unsigned-byte-listp-of-repeat

(defthm unsigned-byte-listp-of-repeat
  (equal (unsigned-byte-listp width (repeat n x))
         (or (zp n) (unsigned-byte-p width x))))

Theorem: unsigned-byte-listp-of-take

(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))))))

Theorem: unsigned-byte-listp-of-take-past-length

(defthm unsigned-byte-listp-of-take-past-length
  (implies (and (natp k) (< (len x) k))
           (not (unsigned-byte-listp width (take k x)))))

Theorem: unsigned-byte-listp-of-nthcdr

(defthm unsigned-byte-listp-of-nthcdr
  (implies (unsigned-byte-listp width x)
           (unsigned-byte-listp width (nthcdr n x))))

Theorem: unsigned-byte-listp-when-take-and-nthcdr

(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)))

Theorem: unsigned-byte-listp-of-update-nth

(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))))

Theorem: unsigned-byte-listp-of-rev

(defthm unsigned-byte-listp-of-rev
  (equal (unsigned-byte-listp n (rev bytes))
         (unsigned-byte-listp n (list-fix bytes))))

Theorem: unsigned-byte-p-of-nth-when-unsigned-byte-listp

(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)))))

Theorem: unsigned-byte-listp-of-make-list-ac

(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)))))

Theorem: unsigned-byte-listp-of-revappend

(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))))

Subtopics

Defbytelist: Introduce a fixtype of true lists of unsigned or signed bytes of a specified size.
Unsigned-byte-list-fix: Fixing function for unsigned-byte-listp.