• 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
          • Reset-array1*
        • Array1-functions
        • Array1-disabled-lemmas
      • Utilities
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Array1

Reset-array1

Clear an 1-dimensional array.

The function (RESET-ARRAY1 name l) returns a 1-dimensional array whose alist is simply the HEADER of l. This has the effect of resetting the array, i.e., reading the new array at any address will return the default value. The implementation is simply to redefine the array as the HEADER of the old array. Thus all of the HEADER information is carried over to the new array.

Note that an alternate definition is available as the lemma RESET-ARRAY1*.

Definitions and Theorems

Function: reset-array1

(defun reset-array1 (name l)
  (declare (xargs :guard (array1p name l)))
  (compress1 name (list (header name l))))

Theorem: array1p-reset-array1

(defthm array1p-reset-array1
  (implies (array1p name l)
           (array1p name (reset-array1 name l))))

Theorem: array1p-reset-array1-properties

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

Theorem: aref1-reset-array1

(defthm aref1-reset-array1
  (implies (and (array1p name l) (integerp index))
           (equal (aref1 name (reset-array1 name l) index)
                  (default name l))))

Subtopics

Reset-array1*

Rewrite: (RESET-ARRAY1 name l) = (LIST (HEADER name l)).