• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
      • Std/strings
      • Std/osets
      • Std/io
      • Std/basic
      • Std/system
      • Std/typed-lists
        • Std/typed-lists/character-listp
        • Std/typed-lists/symbol-listp
        • Std/typed-lists/boolean-listp
        • Std/typed-lists/string-listp
        • Std/typed-lists/eqlable-listp
        • Theorems-about-true-list-lists
        • Std/typed-lists/atom-listp
        • Unsigned-byte-listp
          • Defbytelist
          • Unsigned-byte-list-fix
        • Cons-listp
        • Cons-list-listp
        • Signed-byte-listp
        • String-or-symbol-listp
      • Std/bitsets
      • Std/testing
      • Std/typed-alists
      • Std/stobjs
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Std/typed-lists
  • Unsigned-byte-p

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.