Adding rules to the database

For an introduction to rule-classes, see rule-classes-introduction.

Example Form (from community book finite-set-theory/total-ordering.lisp): (defthm <<-trichotomy (implies (and (ordinaryp x) (ordinaryp y)) (or (<< x y) (equal x y) (<< y x))) :rule-classes ((:rewrite :corollary (implies (and (ordinaryp x) (ordinaryp y) (not (<< x y)) (not (equal x y))) (<< y x))))) General Form: a true list of rule class objects as defined below Special Cases: a symbol abbreviating a single rule class object

When `defthm` is used to prove a named theorem, rules may be derived
from the proved formula and stored in the database. The user specifies which
kinds of rules are to be built, by providing a list of rule class *names*
or, more generally, rule class *objects*, which name the kind of rule to
build and optionally specify various attributes of the desired rule. The rule
class names are `rewrite`, `rewrite-quoted-constant`,
`built-in-clause`, `clause-processor`, `compound-recognizer`, `congruence`, `definition`,
`elim`, `equivalence`, `forward-chaining`,
`generalize`, `induction`, `linear`,
`meta`, `refinement`, `tau-system`,
`type-prescription`, `type-set-inverter`, and
*require* the user-specification of certain class-specific
attributes. Each class of rule affects the theorem prover's behavior in a
different way, as discussed in the corresponding documentation topic. In this
topic we discuss the various attributes that may be attached to rule
classes.

Note that not all events generate rules. For example, a `defthm` event that specifies `defchoose` event generates an axiom that can be referenced
by name in

A rule class object is either one of the

(:class :COROLLARY term :TRIGGER-FNS (fn1 ... fnk) ; provided :class = :META (!) :WELL-FORMEDNESS-GUARANTEE x ; provided :class = :META or :class = :CLAUSE-PROCESSOR :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 :INSTALL-BODY directive ; provided :class = :DEFINITION :LOOP-STOPPER alist ; provided :class = :REWRITE or :class = :REWRITE-QUOTED-CONSTANT :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 ; or :class = :TYPE-PRESCRIPTION :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

See also `force`, case-split, `syntaxp`, and `bind-free` for ``pragmas'' one can wrap around individual hypotheses of
certain classes of rules to affect how the hypothesis is relieved.

Before we get into the discussion of rule classes, let us return to an
important point. In spite of the large variety of rule classes available, at
present we recommend that new ACL2 users rely almost exclusively on
(conditional) rewrite rules. A reasonable but slightly bolder approach is to
use `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.

When in doubt, create a `rewrite` rule, which is the default.
See rule-classes-introduction.

`defthm`
(and `defaxiom`) event. In the following, let

If `defthm` (or `defaxiom`) event, it is as though what was specified was to make one or more
`rewrite` rules, i.e., as though

If `forward-chaining` is equivalent to

We therefore now consider

Each element of the expanded value of `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.

: Corollary— its value,term , must be a term. If omitted, this field defaults tothm . The: corollaryof 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 bythm , the theorem or axiom added. ACL2 permitsthm to be stated ``elegantly'' and then allows the: corollaryof 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 fromthm . Unlessterm follows trivially fromthm 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 no rule is stored for the theorem until all corollaries have been proved.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 indefthm. These values are passed to the recursive call of the prover used to establish that the: corollaryof the rule class object follows from the theorem or axiomthm .

: 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: corollaryis a type-prescription lemma. If no:typed-term is provided in a: type-prescriptionrule 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-chainingor: 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 (except that a macro alias can stand in for a function symbol; see add-macro-alias). Terms with these symbols trigger the application of the rule. See meta.

:Well-formedness-guarantee — this field may be supplied only if the:class is: metaor: clause-processor. Its value must be of one of the following forms:[1] thm-name1 ; :META or :CLAUSE-PROCESSOR rules [2] (thm-name1) ; :META rules [3] (thm-name1 thm-name2) ; :META ruleswhere

thm-name1 andthm-name2 are the names of previously proved theorems establishing that the results of applying the metafunction(s) or clause-processor will be syntactically well-formed. See: meta and: clause-processor for details of the required forms of these well-formedness theorems. Forms [1] and [2] may be used for:meta rules where no hypothesis metafunction is involved. Form [3] must be used for:meta rules with hypothesis metafunctions; that is, if you provide a well-formedness guarantee for a metatheorem with a hypothesis metafunction you must guarantee the well-formedness of both the metafunction (withthm-name1 ) and the hypothesis metafunction (withthm-name2 ). Form [1] must be used for:clause-processor rules. In the absence of a proper:well-formedness-guarantee the well-formedness of the output of a both kinds of rules is checked every time the rule is fired. These checks are skipped when a proper:well-formedness-guarantee is provided or when overridden as described inset-skip-meta-termp-checks.

: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: corollaryof 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 includefn . These symbols are all the members of the mutually recursive clique containing this definition offn . 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 oft 's andnil 's of length equal to the arity of the function. For example, if:clique consists of just two symbols,fn1 andfn2 , of arities2 and3 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.

:Install-body — this field may only be supplied if the:class is: definition. Its value must bet ,nil , or the default,:normalize . A value oft or:normalize will cause ACL2 to install this rule as the new body of the function being ``defined'' (fn in the paragraph just above); hence this definition will be installed for future:expand hints. Furthermore, if this field is omitted or the value is:normalize , then this definition will be simplified with the normalization procedure that is used by default when processing definitions made withdefun. You must explicitly specify:install-body nil in the following cases: the arguments are not a list of distinct variables,equiv (as above) is notequal, or there are free variables in the hypotheses or right-hand side (see free-variables). However, supplying:install-body nil will not affect the rewriter's application of the:definition rule, other than to avoid using the rule to apply:expand hints. If a definition rule equates(f a1 ... ak) withbody but there are hypotheses,hyps , then:expand hints will replace terms(f term1 ... termk) by corresponding terms(if hyps body (hide (f term1 ... termk))) .

: Loop-stopper— this field may only be supplied if the class is: rewriteor: rewrite-quoted-constant. Its value must be a list of entries each consisting of two variables followed by a (possibly empty) list of function symbols, 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 benil , 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: corollaryformula.

: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. (This field is not implemented for other rule classes, including the: type-prescriptionrule class.) 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,: linear, or: type-prescription. It is further required that either only one rule is generated from the formula or, at least, every such rule has the same list of hypotheses. The value for:backchain-limit-lst must benil ; a non-negative integer; or, except in the case of: metarules, a true list each element of which is eithernil 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. Ifbackchain-limit-lst is a non-negative integer, it is defaulted to a list of the appropriate number of repetitions 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 isNIL , 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 globalbackchain-limit ; see backchain-limit for details. For different ways to reign in the rewriter, see rewrite-stack-limit and see set-prover-step-limit. Jared Davis has pointed out that you can set the:backchain-limit-lst to 0 to avoid any attempt to relieveforced hypotheses, which can lead to a significant speed-up in some cases.

Once `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 `corollary` of that object,
generate one or more rules, each of which has the name `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.)

- Type-prescription
- Make a rule that specifies the type of a term
- Rewrite
- Make some
:rewrite rules (possibly conditional ones) - Meta
- Make a
:meta rule (a hand-written simplifier) - Linear
- Make some arithmetic inequality rules
- Definition
- Make a rule that acts like a function definition
- Clause-processor
- Make or apply a
:clause-processor rule (goal-level simplifier) - Tau-system
- Make a rule for the ACL2 ``type checker''
- Forward-chaining
- Make a rule to forward chain when a certain trigger arises
- Equivalence
- Mark a relation as an equivalence relation
- Free-variables
- Free variables in rules
- Congruence
- The relations to maintain while simplifying arguments
- Executable-counterpart
- A rule for computing the value of a function
- Induction
- Make a rule that suggests a certain induction
- Type-reasoning
- ACL2 reasoning with “types”
- Compound-recognizer
- Make a rule used by the typing mechanism
- Rewrite-quoted-constant
- Make a rule to rewrite a quoted constant
- Elim
- Make a destructor elimination rule
- Well-founded-relation-rule
- Show that a relation is well-founded on a set
- Built-in-clause
- To build a clause into the simplifier
- Well-formedness-guarantee
- Guarantee that a metafunction or clause-processor returns a well-formed answer
- Patterned-congruence
- Removing restrictions on classic congruence rules
- Rule-classes-introduction
- Selecting which kind of rule to create
- Guard-holders
- Remove trivial calls from a term
- Refinement
- Record that one equivalence relation refines another
- Type-set-inverter
- Exhibit a new decoding for an ACL2 type-set
- Generalize
- Make a rule to restrict generalizations
- Corollary
- The corollary formula of a rune
- Induction-heuristics
- How ACL2 selects induction schemes
- Backchaining
- Attempting to relieve the hypotheses of a rule
- Default-backchain-limit
- Specifying the backchain limit for a rule