Major Section: RULE-CLASSES

See rule-classes for a general discussion of rule classes and how they are
used to build rules from formulas. An example `:`

`corollary`

formula
from which a `:forward-chaining`

rule might be built is:

Example: (implies (and (p x) (r x)) when (p a) appears in a formula to be (q (f x))) simplified, try to establish (r a) and if successful, add (q (f a)) to the known assumptionsTo specify the triggering terms provide a non-empty list of terms as the value of the

`:trigger-terms`

field of the rule class object.

General Form: Any theorem, provided an acceptable triggering term exists.Forward chaining rules are generated from the corollary term as follows. First, every

`let`

expression is expanded away (hence, so is every
`let*`

and `lambda`

expression), as is every call of a so-called
``guard holder'' (`must-be-equal`

, `prog2$`

, `ec-call`

,
`mv-list`

, `the`

). If the resulting term has the form
`(implies hyp concl)`

, then `concl`

is treated as a conjunction, with one
forward chaining rule with hypothesis `hyp`

created for each conjunct. In
the other case, where the corollary term is not an `implies`

, we process
it as we process the conclusion in the first case.
The `:trigger-terms`

field of a `:forward-chaining`

rule class object
should be a non-empty list of terms, if provided, and should have certain
properties described below. If the `:trigger-terms`

field is not provided,
it defaults to the singleton list containing the ``atom'' of the first
hypothesis of the formula. (The atom of `(not x)`

is `x`

; the atom of
any other term is the term itself.) If there are no hypotheses and no
`:trigger-terms`

were provided, an error is caused.

A triggering term is acceptable if it is not a variable, a quoted constant, a
lambda application, a `let`

- (or `let*`

-) expression, or a
`not`

-expression, and every variable symbol in the conclusion of the
theorem either occurs in the hypotheses or occurs in the trigger.

`:Forward-chaining`

rules are used by the simplifier before it begins to
rewrite the literals of the goal. (Forward chaining is thus carried out from
scratch for each goal.) If any term in the goal is an instance of a trigger
of some forward chaining rule, we try to establish the hypotheses of that
forward chaining theorem (from the negation of the goal). To relieve a
hypothesis we only use type reasoning, evaluation of ground terms, and
presence among our known assumptions. We do not use rewriting. So-called
free variables in hypotheses are treated specially; see free-variables. If
all hypotheses are relieved, we add the instantiated conclusion to our known
assumptions.

*Caution*. Forward chaining does not actually add terms to the goals
displayed during proof attempts. Instead, it extends an associated
*context*, called ``assumptions'' in the preceding paragraph, that ACL2
builds from the goal currently being proved. The context starts out with
``obvious'' consequences of the negation of the goal. For example, if the
goal is

(implies (and (p x) (q (f x))) (c x))then the context notes that

`(p x)`

and `(q (f x))`

are non-`nil`

and
`(c x)`

is `nil`

. Forward chaining is then used to expand the context.
For example, if a forward chaining rule has `(f x)`

as a trigger term and
has body `(implies (p x) (r (f x)))`

, then the context is extended by
binding `(r (f x))`

to non-`nil`

. Note however that since `(r (f x))`

is put into the context, not the goal, it is `f`

is an enabled nonrecursive function symbol then this forward chaining
rule may well be useless, since calls of `f`

may be expanded away.
However, forward-chaining does support the linear arithmetic reasoning
package. For example, suppose that forward-chaining puts `(< (f x) (g x))`

into the context. Then this inequality also goes into the linear arithmetic
data base, together with suitable instances of linear lemmas whose trigger
term is a call of `g`

. See linear.