• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/system
    • Std/basic
    • 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
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• 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.