Define a new alist type, and a theory of the alist type.

Examples:(defalist symbol-to-integer-alistp (l) "Recognizes an alist mapping symbols to integers." (symbolp . integerp)) (defalist symbol-to-bnatural-alistp (l lub) "Recognizes an alists mapping symbols to naturals bounded by lub." (symbolp . (lambda (x) (bnaturalp x lub)))) (defalist symbol-alistp (l) "Define an alist theory alists from an unspecified domain type to symbols." ((lambda (x) t) . symbolp) (:options :omit-defun (:range-type symbol-listp))) (defalist string-to-integer-alistp (l) "Recognizes an alist mapping strings to integers. Produce a minimal theory, and store the BINDING-EQUAL lemma as a :TYPE-PRESCRIPTION." (stringp . integerp) (:options (:theory nth put) (:binding-equal-rule-classes :type-prescription) (:domain-type string-listp) (:range-type integer-listp)))

Syntax:

DEFALIST name arglist [documentation] {declaration}* type-pair [option-list] option-list ::= (:OPTIONS <<!options>>) options ::= !binding-equal-rule-classes-option | !omit-defun-option | !theory-option | !domain-type-option | !range-type-option | !theory-name-option theory-option ::= (:THEORY <<!alist-functions>>) theory-name-option ::= (:THEORY-NAME theory-name) alist-functions ::= acons | alistp | all-bindings-equal| all-bound?-equal | append | assoc-equal | bind-all-equal | bind-equal | bind-pairs-equal | binding-equal | bound?-equal | collect-bound-equal | domain | domain-restrict-equal | pairlis$ | range | rembind-all-equal | rembind-equal binding-equal-rule-classes-option ::= (:BINDING-EQUAL-RULE-CLASSES rule-classes) omit-defun-option ::= :OMIT-DEFUN

Arguments and Values:

arglist -- an argument list satisfying ACL2::ARGLISTP, and containing exactly one symbol whose `print-name' is "L". declaration -- any valid declaration. documentation -- a string; not evaluated. name -- a symbol. theory-name -- any symbol that is a legal name for a deftheory event. type-pair -- A pair (d . r) where d and r are either a function symbol or a one argument LAMBDA function or the constant T. d designates a predicate to be applied to each element of the domain of the alist, and r designates a predicate to be applied to each element of the range of the alist. T means no type restriction. rule-classes -- any form legal as an argument to the :RULE-CLASSES keyword of DEFTHM. Acl2-theory-expression -- Any legal Acl2 theory expression

DEFALIST defines a recognizer for association lists whose pairs map keys of a given type to values of a given type, and by default creates an extensive theory for alists of the newly defined type.

To define an alist type with DEFALIST you must supply a name for the alist recognizer, an argument list for the recognizer, and predicate designator for elements of the alist's range. The name may be any symbol. The argument list must be valid as a functional argument list, and must contain exactly one symbol whose `print-name'is "L". By convention this is the alist argument recognized by the function defined by DEFALIST.

The type of the domain and range of the alist is given by a pair (d . r) where d identifies the type of an element of the alist's domain, and r specifies the type of an element of the alist's range. Either of these may be specified by a symbol which names a one-argument function (or macro) which tests the elements of the domain and range of L. Either of d and r may also be specified as a single-argument LAMBDA function. Finally, either of d and r may be specified as the constant t, indicating no type constraint.

Any number of other arguments to the alist functions may be supplied, but only the L argument will change in the recursive structure of the recognizer.

Note that DEFALIST does not create any guards for L or any other argument. Guards may be specified in the usual way since any number of DECLARE forms may preceed the predicate specification in the DEFALIST form. Bear in mind that if you are defining a function to be used as a guard, then you are advised to consider what impact guarding the arguments of the function may have on its utility. In general the most useful guard functions are those that are guard-free.

By default, DEFALIST creates an extensive theory for the recognized alists. This theory contains appropriate lemmas for all of the alist functions appearing in the `alist-functions' syntax description above. One can select a subset of this theory to be generated by using the :THEORY option (see below). DEFALIST always creates a :FORWARD-CHAINING rule from the recognizer to ALISTP.

DEFALIST also creates a DEFTHEORY event that lists all of the lemmas created by the DEFALIST. The name of the theory is formed by concatenating the function name and the string "-THEORY", and INTERNing the resulting string in the package of the function name.

DEFALIST options are specified with a special :OPTIONS list systax. If present, the :OPTIONS list must appear as the last form in the body of the DEFALIST.

- :OMIT-DEFUN
- If the :OMIT-DEFUN keyword is present then the definition will not be created. Instead, only the list theory for the function is generated. Use this option to create a list theory for recognizers defined elsewhere.
- :THEORY
- This option is used to specify that only a subset of the list theory be created. In the STRINGP-LISTP example above we specify that only lemmas about STRINGP-LISTP viz-a-viz NTH and PUT are to be generated. By default the complete list theory for the recognizer is created. If the option is given as (:THEORY) then the entire theory will be suppressed, except for the :FORWARD-CHAINING rule from the recognizer to TRUE-LISTP.
- :BINDING-EQUAL-RULE-CLASSES
- This option specifies a value for the :RULE-CLASSES keyword for the DEFTHM generated for the BINDING-EQUAL function (and for CDRASSOC) applied to an alist recognized by the DEFALIST recognizer. The default is :REWRITE.
- :DOMAIN-TYPE
- This option specifies a predicate that recognizes a list of domain elements. It may be either a symbol or LAMBDA form. If present, and when not prevented by a :THEORY specification, a rewrite rule for the type of the domain will be generated. A lemma will be generated to check the compatibility of the specified domain type and domain element type.
- :RANGE-TYPE
- This option specifies a predicate that recognizes a list of range elements. It may be either a symbol or LAMBDA form. If present, and when not prevented by a :THEORY specification, a rewrite rule for the type of the range will be generated. A lemma will be generated to check the compatibility of the specified range type and domain element type.
- :THEORY-NAME
- This option allows the user to define the name of the deftheory event that is automatically generated, and which includes the defthms that are generated.