• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • 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
  • 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.