Major Section: ACL2 Documentation

General Form: a true list of rule class objects as defined belowACL2 provides users with the ability to create a number of different kinds of rules, including (conditional) rewrite rules but also including others. Don't be put off by the long description to follow; usually, you'll probably want to use rewrite rules. More on this below.Special Cases: a symbol abbreviating a single rule class object

A rule class object is either one of the `:class`

keywords or else is
a list of the form shown below. Those fields marked with ``(!)''
are required when the `:class`

is as indicated.

(:class :COROLLARY term :TRIGGER-FNS (fn1 ... fnk) ; provided :class = :META (!) :TRIGGER-TERMS (t1 ... tk) ; provided :class = :FORWARD-CHAINING ; or :class = :LINEAR :TYPE-SET n ; provided :class = :TYPE-SET-INVERTER :TYPED-TERM term ; provided :class = :TYPE-PRESCRIPTION :CLIQUE (fn1 ... fnk) ; provided :class = :DEFINITION (!) :CONTROLLER-ALIST alist ; provided :class = :DEFINITION (!) :LOOP-STOPPER alist ; provided :class = :REWRITE :PATTERN term ; provided :class = :INDUCTION (!) :CONDITION term ; provided :class = :INDUCTION :SCHEME term ; provided :class = :INDUCTION (!) :MATCH-FREE all-or-once ; provided :class = :REWRITE or :class = :LINEAR or :class = :FORWARD-CHAINING :BACKCHAIN-LIMIT-LST limit ; provided :class = :REWRITE or :class = :META or :class = :LINEAR :HINTS hints ; provided instrs = nil :INSTRUCTIONS instrs ; provided hints = nil :OTF-FLG flg)When rule class objects are provided by the user, most of the fields are optional and their values are computed in a context sensitive way. When a

`:class`

keyword is used as a rule class
object, all relevant fields are determined contextually. Each rule
class object in `:rule-classes`

causes one or more rules to be added
to the data base. The `:class`

keywords are documented individually
under the following names. Note that when one of these names is used
as a `:class`

, it is expected to be in the keyword package (i.e., the
names below should be preceded by a colon but the ACL2 documentation
facilities do not permit us to use keywords below).

### BUILT-IN-CLAUSES -- to build a clause into the simplifier

### COMPOUND-RECOGNIZER -- make a rule used by the typing mechanism

### CONGRUENCE -- the relations to maintain while simplifying arguments

### DEFINITION -- make a rule that acts like a function definition

### ELIM -- make a destructor elimination rule

### EQUIVALENCE -- mark a relation as an equivalence relation

### FORWARD-CHAINING -- make a rule to forward chain when a certain trigger arises

### FREE-VARIABLES -- free variables in rules

### GENERALIZE -- make a rule to restrict generalizations

### INDUCTION -- make a rule that suggests a certain induction

### LINEAR -- make some arithmetic inequality rules

### META -- make a

`:meta`

rule (a hand-written simplifier)### REFINEMENT -- record that one equivalence relation refines another

### REWRITE -- make some

`:rewrite`

rules (possibly conditional ones)### TYPE-PRESCRIPTION -- make a rule that specifies the type of a term

### TYPE-SET-INVERTER -- exhibit a new decoding for an ACL2 type-set

### WELL-FOUNDED-RELATION -- show that a relation is well-founded on a set

`:`

`type-prescription`

and
`:`

`forward-chaining`

rules for ``type-theoretic'' rules, especially
ones whose top-level function symbol is a common one like
`true-listp`

or `consp`

; see type-prescription and
see forward-chaining. However, the rest of the rule classes
are really not intended for widespread use, but rather are mainly
for experts.
We expect that we will write more about the question of which kind
of rule to use. For now: when in doubt, use a `:`

`rewrite`

rule.

`:Rule-classes`

is an optional keyword argument of the `defthm`

(and
`defaxiom`

) event. In the following, let `name`

be the name of the
event and let `thm`

be the formula to be proved or added as an axiom.

If `:rule-classes`

is not specified in a `defthm`

(or `defaxiom`

) event,
it is as though `:rule-classes`

`((:rewrite))`

had been used. Use
`:rule-classes`

`nil`

to specify that no rules are to be generated.

If `:rule-classes`

class is specified, where class is a non-`nil`

symbol, it is as though `:rule-classes`

`((class))`

had been used.
Thus, `:rule-classes`

`:`

`forward-chaining`

is equivalent to `:rule-classes`

`((:forward-chaining))`

.

We therefore now consider `:rule-classes`

as a true list. If any
element of that list is a keyword, replace it by the singleton list
containing that keyword. Thus, `:rule-classes`

`(:rewrite :elim)`

is
the same as `:rule-classes`

`((:rewrite) (:elim))`

.

Each element of the expanded value of `:rule-classes`

must be a true
list whose `car`

is one of the rule class keyword tokens listed above,
e.g., `:`

`rewrite`

, `:`

`elim`

, etc., and whose `cdr`

is a ``keyword alist''
alternately listing keywords and values. The keywords in this alist
must be taken from those shown below. They may be listed in any
order and most may be omitted, as specified below.

Once

`:`

`Corollary`

-- its value,`term`

, must be a term. If omitted, this field defaults to`thm`

. The`:`

`corollary`

of a rule class object is the formula actually used to justify the rule created and thus determines the form of the rule. Nqthm provided no similar capability: each rule was determined by`thm`

, the theorem or axiom added. ACL2 permits`thm`

to be stated ``elegantly'' and then allows the`:`

`corollary`

of a rule class object to specify how that elegant statement is to be interpreted as a rule. For the rule class object to be well-formed, its (defaulted)`:`

`corollary`

,`term`

, must follow from`thm`

. Unless`term`

is trivially implied by`thm`

, using little more than propositional logic, the formula`(implies thm term)`

is submitted to the theorem prover and the proof attempt must be successful. During that proof attempt the values of`:`

`hints`

,`:`

`instructions`

, and`:`

`otf-flg`

, as provided in the rule class object, are provided as arguments to the prover. Such auxiliary proofs give the sort of output that one expects from the prover. However, as noted above, corollaries that follow trivially are not submitted to the prover; thus, such corollaries cause no prover output.Note that before

`term`

is stored, all calls of macros in it are expanded away. See trans.

`:`

`Hints`

,`:`

`instructions`

,`:`

`otf-flg`

-- the values of these fields must satisfy the same restrictions placed on the fields of the same names in`defthm`

. These values are passed to the recursive call of the prover used to establish that the`:`

`corollary`

of the rule class object follows from the theorem or axiom`thm`

.

`:`

`Type-set`

-- this field may be supplied only if the`:class`

is`:`

`type-set-inverter`

. When provided, the value must be a type-set, an integer in a certain range. If not provided, an attempt is made to compute it from the corollary. See type-set-inverter.

`:Typed-term`

-- this field may be supplied only if the`:class`

is`:`

`type-prescription`

. When provided, the value is the term for which the`:`

`corollary`

is a type-prescription lemma. If no`:typed-term`

is provided in a`:`

`type-prescription`

rule class object, we try to compute heuristically an acceptable term. See type-prescription.

`:Trigger-terms`

-- this field may be supplied only if the`:class`

is`:`

`forward-chaining`

or`:`

`linear`

. When provided, the value is a list of terms, each of which is to trigger the attempted application of the rule. If no`:trigger-terms`

is provided, we attempt to compute heuristically an appropriate set of triggers. See forward-chaining or see linear.

`:Trigger-fns`

-- this field must (and may only) be supplied if the`:class`

is`:`

`meta`

. Its value must be a list of function symbols. Terms with these symbols trigger the application of the rule. See meta.

`:Clique`

and`:controller-alist`

-- these two fields may only be supplied if the`:class`

is`:`

`definition`

. If they are omitted, then ACL2 will attempt to guess them. Suppose the`:`

`corollary`

of the rule is`(implies hyp (equiv (fn a1 ... an) body))`

. The value of the`:clique`

field should be a true list of function symbols, and if non-`nil`

must include`fn`

. These symbols are all the members of the mutually recursive clique containing this definition of`fn`

. That is, a call of any function in`:clique`

is considered a ``recursive call'' for purposes of the expansion heuristics. The value of the`:controller-alist`

field should be an alist that maps each function symbol in the`:clique`

to a list of`t`

's and`nil`

's of length equal to the arity of the function. For example, if`:clique`

consists of just two symbols,`fn1`

and`fn2`

, of arities`2`

and`3`

respectively, then`((fn1 t nil) (fn2 nil t t))`

is a legal value of`:controller-alist`

. The value associated with a function symbol in this alist is a ``mask'' specifying which argument slots of the function ``control'' the recursion for heuristic purposes. Sloppy choice of`:clique`

or`:controller-alist`

can result in infinite expansion and stack overflow.

`:`

`loop-stopper`

-- this field may only be supplied if the class is`:`

`rewrite`

. Its value must be a list of entries each consisting of two variables followed by a (possibly empty) list of functions, for example`((x y binary-+) (u v foo bar))`

. It will be used to restrict application of rewrite rules by requiring that the list of instances of the second variables must be ``smaller'' than the list of instances of the first variables in a sense related to the corresponding functions listed; see loop-stopper. The list as a whole is allowed to be`nil`

, indicating that no such restriction shall be made. Note that any such entry that contains a variable not being instantiated, i.e., not occurring on the left side of the rewrite rule, will be ignored. However, for simplicity we merely require that every variable mentioned should appear somewhere in the corresponding`:`

`corollary`

formula.

`:pattern`

,`:condition`

,`:scheme`

-- the first and last of these fields must (and may only) be supplied if the class is`:`

`induction`

.`:Condition`

is optional but may only be supplied if the class is`:`

`induction`

. The values must all be terms and indicate, respectively, the pattern to which a new induction scheme is to be attached, the condition under which the suggestion is to be made, and a term which suggests the new scheme. See induction.

`match-free`

-- this field must be`:all`

or`:once`

and may be supplied only if the`:class`

is either`:`

`rewrite`

,`:`

`linear`

, or`:`

`forward-chaining`

. See free-variables for a description of this field. Note: Although this field is intended to be used for controlling retries of matching free variables in hypotheses, it is legal to supply it even if there are no such free variables. This can simplify the automated generation of rules, but note that when`:match-free`

is supplied, the warning otherwise provided for the presence of free variables in hypotheses will be suppressed.

`backchain-limit-lst`

-- this field may be supplied only if the`:class`

is either`:`

`rewrite`

,`:`

`meta`

, or`:`

`linear`

and only one rule is generated from the formula. Its value must be`nil`

; a non-negative integer; or, except in the case of`:`

`meta`

rules, a true list each element of which is either`nil`

or a non-negative integer. If it is a list, its length must be equal to the number of hypotheses of the rule and each item in the list is the ``backchain limit'' associated with the corresponding hypothesis. If`backchain-limit-lst`

is a non-negative integer, it is defaulted to a list of the appropriate number of repetions of that integer. The backchain limit of a hypothesis is used to limit the effort that ACL2 will expend when relieving the hypothesis. If it is`NIL`

, no new limits are imposed; if it is an integer, the hypothesis will be limited to backchaining at most that many times. Note that backchaining may be further limited by a global`backchain-limit`

; see backchain-limit for details. For a different way to reign in the rewriter, see rewrite-stack-limit. Jared Davis has pointed out that you can set this field to 0 to avoid any attempt to relieve`force`

d hypotheses, which can lead to a significant speed-up in some cases.

`thm`

has been proved (in the case of `defthm`

) and each rule
class object has been checked for well-formedness (which might
require additional proofs), we consider each rule class object in
turn to generate and add rules. Let `:class`

be the class keyword
token of the `i`

th class object (counting from left to right).
Generate the rune `(:class name . x)`

, where `x`

is `nil`

if there is only
one class and otherwise `x`

is `i`

. Then, from the `:`

`corollary`

of that
object, generate one or more rules, each of which has the name
`(:class name . x)`

. See the `:`

`doc`

entry for each rule class to see
how formulas determine rules. Note that it is in principle possible
for several rules to share the same name; it happens whenever a
`:`

`corollary`

determines more than one rule. This in fact only occurs
for `:`

`rewrite`

, `:`

`linear`

, and `:`

`forward-chaining`

class rules and only
then if the `:`

`corollary`

is essentially a conjunction. (See the
documentation for rewrite, linear, or
forward-chaining for details.)