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

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.