• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
    • Real
    • ACL2-tutorial
    • Debugging
    • Miscellaneous
    • Prover-output
    • Built-in-theorems
      • Built-in-theorems-about-arithmetic
      • Built-in-theorems-about-symbols
      • Built-in-theorems-about-characters
      • Built-in-theorems-about-lists
      • Built-in-theorems-about-arrays
      • Built-in-theorems-about-strings
      • Built-in-theorems-about-alists
      • Built-in-theorems-about-total-order
      • Built-in-theorems-about-system-utilities
      • Built-in-theorems-about-cons-pairs
      • Built-in-theorems-for-tau
      • Built-in-theorems-about-bad-atoms
      • Built-in-theorems-about-logical-connectives
      • Built-in-theorems-about-booleans
      • Built-in-theorems-about-random$
      • Built-in-theorems-about-eqlables
    • Macros
    • Interfacing-tools
    • About-ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Built-in-theorems

Built-in-theorems-about-arrays

Built-in theorems about arrays.

Theorem: array1p-forward

(defthm
 array1p-forward
 (implies
  (array1p name l)
  (and
   (symbolp name)
   (alistp l)
   (keyword-value-listp (cdr (assoc-eq :header l)))
   (true-listp
      (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))
   (equal
    (length
      (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))
    1)
   (integerp
    (car
     (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))))
   (integerp
    (cadr
        (assoc-keyword :maximum-length (cdr (assoc-eq :header l)))))
   (<
    0
    (car
     (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))))
   (<
    (car
      (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))
    (cadr
        (assoc-keyword :maximum-length (cdr (assoc-eq :header l)))))
   (<=
    (cadr
         (assoc-keyword :maximum-length (cdr (assoc-eq :header l))))
    *maximum-positive-32-bit-integer*)
   (bounded-integer-alistp
    l
    (car
     (cadr
         (assoc-keyword :dimensions (cdr (assoc-eq :header l))))))))
 :rule-classes :forward-chaining)

Theorem: array1p-linear

(defthm
 array1p-linear
 (implies
  (array1p name l)
  (and
   (<
    0
    (car
     (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))))
   (<
    (car
      (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))
    (cadr
        (assoc-keyword :maximum-length (cdr (assoc-eq :header l)))))
   (<=
    (cadr
         (assoc-keyword :maximum-length (cdr (assoc-eq :header l))))
    *maximum-positive-32-bit-integer*)))
 :rule-classes ((:linear :match-free :all)))

Theorem: array2p-forward

(defthm
 array2p-forward
 (implies
  (array2p name l)
  (and
   (symbolp name)
   (alistp l)
   (keyword-value-listp (cdr (assoc-eq :header l)))
   (true-listp
      (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))
   (equal
    (length
      (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))
    2)
   (integerp
    (car
     (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))))
   (integerp
    (cadr
     (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))))
   (integerp
    (cadr
        (assoc-keyword :maximum-length (cdr (assoc-eq :header l)))))
   (<
    0
    (car
     (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))))
   (<
    0
    (cadr
     (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))))
   (<
    (*
     (car
      (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))
     (cadr
      (cadr
           (assoc-keyword :dimensions (cdr (assoc-eq :header l))))))
    (cadr
        (assoc-keyword :maximum-length (cdr (assoc-eq :header l)))))
   (<=
    (cadr
         (assoc-keyword :maximum-length (cdr (assoc-eq :header l))))
    *maximum-positive-32-bit-integer*)
   (bounded-integer-alistp2
    l
    (car
      (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))
    (cadr
     (cadr
         (assoc-keyword :dimensions (cdr (assoc-eq :header l))))))))
 :rule-classes :forward-chaining)

Theorem: array2p-linear

(defthm
 array2p-linear
 (implies
  (array2p name l)
  (and
   (<
    0
    (car
     (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))))
   (<
    0
    (cadr
     (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))))
   (<
    (*
     (car
      (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))
     (cadr
      (cadr
           (assoc-keyword :dimensions (cdr (assoc-eq :header l))))))
    (cadr
        (assoc-keyword :maximum-length (cdr (assoc-eq :header l)))))
   (<=
    (cadr
         (assoc-keyword :maximum-length (cdr (assoc-eq :header l))))
    *maximum-positive-32-bit-integer*)))
 :rule-classes ((:linear :match-free :all)))

Theorem: array1p-cons

(defthm
 array1p-cons
 (implies
  (and
   (<
     n
     (caadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))
   (not (< n 0))
   (integerp n)
   (array1p name l))
  (array1p name (cons (cons n val) l))))

Theorem: array2p-cons

(defthm array2p-cons
        (implies (and (< j (cadr (dimensions name l)))
                      (not (< j 0))
                      (integerp j)
                      (< i (car (dimensions name l)))
                      (not (< i 0))
                      (integerp i)
                      (array2p name l))
                 (array2p name (cons (cons (cons i j) val) l))))