		Search-engine friendly clone of the ACL2 documentation.

Array1

Defarray1type

Characterize 1-dimensional arrays with a fixed element type.

Example form:

(DEFARRAY1TYPE INTEGERP-ARRAY1P INTEGERP)

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

General form:

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

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.

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.

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

DEFARRAY1TYPE defines a recognizer:

(recognizer NAME L)

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

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)))

If :SIZE is specified then the first and third theorems become:

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)))

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.

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.

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.

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.