		Search-engine friendly clone of the ACL2 documentation.

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)