• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
      • Deflist
      • Defalist
      • Memory
      • Defstructure
      • Array1
        • Defarray1type
        • Array1-lemmas
        • Reset-array1
        • Array1-functions
        • Array1-disabled-lemmas
      • Utilities
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Array1

Array1-lemmas

A theory of all enabled rules exported by the array1 book.

Note that in order for these rules to be applicable you will first need to disable the theory array1-functions.

Definitions and Theorems

Theorem: array1p-compress1

(defthm array1p-compress1
  (implies (array1p name l)
           (array1p name (compress1 name l))))

Theorem: array1p-compress1-properties

(defthm array1p-compress1-properties
  (implies (array1p name l)
           (and (equal (header name (compress1 name l))
                       (header name l))
                (equal (dimensions name (compress1 name l))
                       (dimensions name l))
                (equal (maximum-length name (compress1 name l))
                       (maximum-length name l))
                (equal (default name (compress1 name l))
                       (default name l)))))

Theorem: array1p-aset1

(defthm array1p-aset1
  (implies (and (array1p name l)
                (integerp n)
                (>= n 0)
                (< n (car (dimensions name l))))
           (array1p name (aset1 name l n val))))

Theorem: array1p-aset1-properties

(defthm array1p-aset1-properties
  (implies (and (array1p name l)
                (integerp n)
                (>= n 0)
                (< n (car (dimensions name l))))
           (and (equal (header name (aset1 name l n val))
                       (header name l))
                (equal (dimensions name (aset1 name l n val))
                       (dimensions name l))
                (equal (maximum-length name (aset1 name l n val))
                       (maximum-length name l))
                (equal (default name (aset1 name l n val))
                       (default name l)))))

Theorem: aref1-compress1

(defthm aref1-compress1
  (implies (and (array1p name l)
                (integerp n)
                (>= n 0)
                (< n (car (dimensions name l))))
           (equal (aref1 name (compress1 name l) n)
                  (aref1 name l n))))

Theorem: array1p-acons-properties

(defthm array1p-acons-properties
  (implies (integerp n)
           (and (equal (header name (cons (cons n val) l))
                       (header name l))
                (equal (dimensions name (cons (cons n val) l))
                       (dimensions name l))
                (equal (maximum-length name (cons (cons n val) l))
                       (maximum-length name l))
                (equal (default name (cons (cons n val) l))
                       (default name l)))))

Theorem: array1p-consp-header

(defthm array1p-consp-header
  (implies (array1p name l)
           (consp (header name l)))
  :rule-classes :type-prescription)

Theorem: array1p-car-header

(defthm array1p-car-header
  (implies (array1p name l)
           (equal (car (header name l)) :header)))

Theorem: aref1-aset1-equal

(defthm aref1-aset1-equal
  (implies (and (array1p name l)
                (integerp n)
                (>= n 0)
                (< n (car (dimensions name l))))
           (equal (aref1 name (aset1 name l n val) n)
                  val)))

Theorem: aref1-aset1-not-equal

(defthm aref1-aset1-not-equal
  (implies (and (array1p name l)
                (integerp n1)
                (>= n1 0)
                (< n1 (car (dimensions name l)))
                (integerp n2)
                (>= n2 0)
                (< n2 (car (dimensions name l)))
                (not (equal n1 n2)))
           (equal (aref1 name (aset1 name l n1 val) n2)
                  (aref1 name l n2))))

Theorem: aref1-aset1

(defthm aref1-aset1
  (implies (and (array1p name l)
                (integerp n1)
                (>= n1 0)
                (< n1 (car (dimensions name l)))
                (integerp n2)
                (>= n2 0)
                (< n2 (car (dimensions name l))))
           (equal (aref1 name (aset1 name l n1 val) n2)
                  (if (equal n1 n2)
                      val
                    (aref1 name l n2)))))

Theorem: array1p-forward-modular

(defthm array1p-forward-modular
  (implies
       (array1p name l)
       (and (symbolp name)
            (alistp l)
            (keyword-value-listp (cdr (header name l)))
            (true-listp (dimensions name l))
            (equal (length (dimensions name l)) 1)
            (integerp (car (dimensions name l)))
            (integerp (maximum-length name l))
            (< 0 (car (dimensions name l)))
            (<= (car (dimensions name l))
                (maximum-length name l))
            (<= (maximum-length name l)
                (array-maximum-length-bound))
            (bounded-integer-alistp l (car (dimensions name l)))))
  :rule-classes :forward-chaining)