|
|
|---|
|
|
|
|---|
Define a new list type, and a theory of the list type.
Examples
(deflist integer-listp (l) "Recognizes true-lists of integers." integerp) (deflist bnatural-listp (l lub) "Recognizes lists of naturals bounded by lub." (lambda (x) (bnaturalp x lub))) (deflist symbol-listp (l) "Define a list theory for this function which is already defined by Acl2." symbolp (:options :omit-defun)) (deflist stringp-listp (l) "Recognizes lists of strings; produce a minimal theory, and store the NTH lemma as a :TYPE-PRESCRIPTION." stringp (:options (:theory nth put-nth) (:nth-rule-classes :type-prescription)))
Syntax:
DEFLIST name arglist [documentation] {declaration}* predicate [option-list]
option-list ::= (:OPTIONS <<!options>>)
options ::= !car-rule-classes-option |
!nth-rule-classes-option |
!omit-defun-option |
!theory-option |
!theory-name-option
theory-name-option ::= (:THEORY-NAME theory-name)
theory-option ::= (:THEORY <<!list-functions>>)
list-functions ::= APPEND | BUTLAST | CONS | CAR | CDR |
FIRSTN | INITIAL-SUBLISTP-EQUAL | LAST |
MAKE-LIST | MEMBER-EQUAL | MEMBERP-EQUAL |
NTH | NTH-SEG | NTHCDR | PUT-NTH | PUT-SEG |
REMOVE-DUPLICATES-EQUAL | REMOVE-EQUAL |
REVERSE | SUBSEQ | UPDATE-NTH
car-rule-classes-option ::= (:CAR-RULE-CLASSES rule-classes)
nth-rule-classes-option ::= (:NTH-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. predicate -- Either a symbol or a one argument LAMBDA function; designates a predicate to be applied to each element of the list. rule-classes -- any form legal as an argument to the :RULE-CLASSES keyword of DEFTHM. theory-name -- any symbol that is a legal name for a deftheory event.
DEFLIST defines a recognizer for true lists whose elements all satisfy a given predicate, and by default creates an extensive theory for lists of the newly defined type.
To define a list type with DEFLIST you must supply a name for the recognizer, an argument list, and predicate designator. The name may be any symbol. The argument list must be valid as a functional argument list, and must contain exactly 1 symbol whose `print-name'is "L". By convention this is the list argument recognized by the function defined by DEFLIST.
The DEFLIST recognizer will return T only if each element of L satisfies (returns a non-NIL value) the given predicate, otherwise NIL. If the predicate is specified as a symbol, then this is assumed to be the function symbol of a one argument function (or macro) with which to test the elements of L. If the predicate is specified as a single-argument LAMBDA function, then the given LAMBDA function will be applied to test successive elements of L.
Any number of other arguments to the function may be supplied, but only the L argument will change in the recursive structure of the recognizer.
Note that DEFLIST 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 precede the predicate specification in the DEFLIST form. DO NOT DECLARE GUARDS FOR THE LIST ARGUMENT L, as this may cause DEFLIST to blindly generate unprovable conjectures and unusable theorems. 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.
Theory:
By default, DEFLIST creates an extensive theory for the recognized lists. This theory contains appropriate lemmas for all of the list functions appearing in the `list-functions' syntax description above. This list of function symbols is also available as the Acl2 constant *DEFLIST-THEORY-OPTIONS*.
One can select a subset of this theory to be generated by using the :THEORY option (see below). DEFLIST always creates a :FORWARD-CHAINING rule from the recognizer to TRUE-LISTP. DEFLIST also creates a DEFTHEORY event that lists all of the lemmas created by the DEFLIST. 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.
Options:
DEFLIST 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 DEFLIST.