array1

(in-package "ACL2")

(defxdoc array1
  :parents (data-structures)
  :short "A book of lemmas that characterize 1-dimensional arrays."
  :long "<p>Because many of the functions characterized by this book are
non-recursive, one should always @(see DISABLE) the theory
@('ARRAY1-FUNCTIONS') after including this book, or the lemmas will not be
applicable.</p>

<p>The lemmas exported by this book should completely characterize
1-dimensional arrays for most purposes.  Given the lemmas exported by this
book, it should not be necessary to @(see ENABLE) any of the 1-dimensional
array functions except under special circumstances.</p>

<p>This book defines a function @(see RESET-ARRAY1) that clears an array,
effectively resetting each element of the array to the default value.  This
book also includes a macro, @(see DEFARRAY1TYPE), which defines recognizers and
supporting lemmas for 1-dimensional arrays whose elements are all of a fixed
type.</p>")

(defsection array1-lemmas
  :parents (array1)
  :short "A @(see theory) of all @(see enable)d rules exported by the @(see
array1) book."
  :long "<p>Note that in order for these rules to be applicable you will first
need to @(see DISABLE) the theory @(see ARRAY1-FUNCTIONS).</p>"
  (defthm array1p-compress1
    (implies (array1p name l) (array1p name (compress1 name l)))
    :hints (("Goal" :in-theory (enable array1p)
       :use array1p-header-exists)))
  (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)))))
  (local (in-theory (disable compress1)))
  (defthm array1p-aset1
    (implies (and (array1p name l)
        (integerp n)
        (>= n 0)
        (< n (car (dimensions name l))))
      (array1p name (aset1 name l n val))))
  (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)))))
  (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))))
  (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)))))
  (defthm array1p-consp-header
    (implies (array1p name l) (consp (header name l)))
    :rule-classes :type-prescription)
  (defthm array1p-car-header
    (implies (array1p name l)
      (equal (car (header name l)) :header)))
  (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)))
  (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))))
  (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))))
    :hints (("Goal" :in-theory (disable aref1 aset1))))
  (in-theory (disable aref1-aset1-equal aref1-aset1-not-equal))
  (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 :hints (("Goal" :in-theory (disable length)))))

(defsection reset-array1
  :parents (array1)
  :short "Clear an 1-dimensional array."
  :long "<p>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.</p>

<p>Note that an alternate definition is available as the lemma
RESET-ARRAY1*.</p>"
  (defun reset-array1
    (name l)
    (declare (xargs :guard (array1p name l)))
    (compress1 name (list (header name l)))))

(defsection reset-array1*
  :parents (reset-array1)
  :short "Rewrite: (RESET-ARRAY1 name l) = (LIST (HEADER name l))."
  :long "<p>This definition of RESET-ARRAY1 is logically equivalent to the
actual definition. The actual definition, which includes a COMPRESS1 call, has
the run-time side-effect of re-installing the new array.  The COMPRESS1 is
logically redundant, however.</p>

<p>This lemma is exported DISABLED, however this is the preferred definition to
use to reason about RESET-ARRAY1.</p>"
  (defthm reset-array1*
    (implies (array1p name l)
      (equal (reset-array1 name l) (list (header name l))))
    :hints (("Goal" :in-theory (enable compress1 compress11)))))

(defsection-progn reset-array1-lemmas
  :extension reset-array1
  (defthm array1p-reset-array1
    (implies (array1p name l)
      (array1p name (reset-array1 name l))))
  (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)))))
  (defthm aref1-reset-array1
    (implies (and (array1p name l) (integerp index))
      (equal (aref1 name (reset-array1 name l) index)
        (default name l)))))

(defsection array1-functions
  :parents (array1)
  :short "A theory of all functions specific to 1-dimensional arrays."
  :long "<p>This theory must be DISABLEd in order for the lemmas exported by
the "array1" book to be applicable.</p>"
  (deftheory array1-functions
    '(array1p aset1
      aref1
      compress1
      header
      dimensions
      maximum-length
      default
      reset-array1)))

(deftheory array1-lemmas
  '(array1p-compress1 array1p-compress1-properties
    array1p-aset1
    array1p-aset1-properties
    aref1-compress1
    array1p-acons-properties
    array1p-consp-header
    array1p-car-header
    aref1-aset1
    array1p-forward-modular
    array1p-reset-array1
    array1p-reset-array1-properties
    aref1-reset-array1))

(defsection array1-disabled-lemmas
  :parents (array1)
  :short "A theory of all rules exported DISABLEd by the "array1" book."
  :long "<p>Note that in order for these rules to be applicable you will first
need to disable @(see array1-functions).  Look at the :DOC for each lemma for
an explanation of why the lemma is exported DISABLEd.</p>"
  (deftheory array1-disabled-lemmas
    '(aref1-aset1-equal aref1-aset1-not-equal reset-array1*)))

(defsection defarray1type
  :parents (array1)
  :short "Characterize 1-dimensional arrays with a fixed element type."
  :long "<p>Example form:</p>

@({
  (DEFARRAY1TYPE INTEGERP-ARRAY1P INTEGERP)
})

<p>The above example defines a recognizer, INTEGERP-ARRAYP, for 1-dimensional
arrays whose elements are all INTEGERP.</p>

<p>General form:</p>

@({
  (DEF1ARRAYTYPE recognizer predicate
                 &key size doc
                      (aref1-lemma-rule-classes ':REWRITE)
                      (aset1-lemma-rule-classes ':REWRITE))
})

<p>DEFARRAY1TYPE defines a recognizer for 1-dimensional arrays whose elements
are all of a single type.  The recognizer argument is a symbol that is used as
the name of the recognizer.  The predicate argument should be a 1-argument,
unguarded Boolean function that recognizes objects of the desired type.  The
predicate may either be a symbol (the name of the predicate), or a LAMBDA
expression.</p>

<p>If :SIZE is specified it should be a variable-free term that will evaluate
to a positive integer.  If specified, then the recognizer will only recognize
1-dimensional arrays of the given type and of a fixed size.</p>

<p>If :DOC is specified it should be a string, and it will be inserted as the
documentation string in the recognizer.</p>

<p>DEFARRAY1TYPE defines a recognizer:</p>

@({ (recognizer NAME L) })

<p>and proves 4 useful theorems about it.  If the :SIZE is not specified then
the three theorems will be:</p>

@({
  1. (IMPLIES (recognizer NAME L)
              (ARRAY1P NAME L))

  2. (IMPLIES (AND (recognizer NAME L)
                   (INTEGERP N))
              (predicate (AREF1 NAME L N)))

  3. (IMPLIES (AND (recognizer NAME L)
                   (< N (CAR (DIMENSIONS NAME L)))
                   (INTEGERP N)
                   (>= N 0)
                   (predicate VAL))
              (recognizer NAME (ASET1 NAME L N VAL)))

  4. (IMPLIES (recognizer NAME l)
              (recognizer NAME (RESET-ARRAY1 name l)))
})

<p>If :SIZE is specified then the first and third theorems become:</p>

@({
  1. (IMPLIES (recognizer NAME L)
              (AND (ARRAY1P NAME L)
                   (EQUAL (CAR (DIMENSIONS name l))
                          size)))

  3. (IMPLIES (AND (recognizer NAME L)
                   (< N size)
                   (INTEGERP N)
                   (>= N 0)
                   (predicate VAL))
              (recognizer NAME (ASET1 NAME L N VAL)))
})

<p>The first theorem is stored as both :REWRITE and :FORWARD-CHAINING rules.
The :RULE-CLASSES of the second and third lemmas default to :REWRITE, but are
selectable by the user by means of the :AREF1-LEMMA-RULE-CLASSES and
:ASET1-LEMMA-RULE-CLASSSES arguments to DEFARRAY1TYPE (respectively).  If
using :RULE-CLASSES other than :REWRITE the user should bear in mind the
documented restrictions on the applicability of :TYPE-PRESCRIPTION and
:FORWARD-CHAINING rules.  The fourth rule is always a :REWRITE rule.</p>

<p>Note the the recognizer is a very strong recognizer that specifies that the
array alist is a BOUNDED-INTEGER-ALISTP whose elements all satisfy the type
predicate.  The recognizer also specifies that the default element of the array
satisfies the predicate as well.</p>

<p>WARNING: The recognizer is defined in terms of a recursive recognizer, named
@('<recognizer>-FN').  THE RECURSIVE RECOGNIZER SHOULD BE COMPILED BEFORE YOU
TRY TO EXECUTE IT, OR IT MAY CAUSE A STACK OVERFLOW.  Also note that the
recognizer will be DISABLEd after execution of this macro.  The user must
insure that the recognizer remains DISABLEd, otherwise the above lemmas will
never be applied.</p>

<p>DEFARRAY1TYPE proves the generated lemmas in a minimal, ENCAPSULATEd theory
that should guarantee that the proofs always succeed.  If one should encounter
a case where a proof fails (as opposed to a translation or other syntax
failure), please notify the author.</p>")