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. If that term has the form

`(implies hyp concl)`

, then the
`let`

expressions in `concl`

(formally, lambda expressions) are expanded
away, and the result 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`

-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 *not* further simplified.
If `f`

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

may be expanded
away.

Another common misconception is this: Suppose that you forward
chain and put `(< (f x) (g x))`

into the context. Then does it go
into the linear arithmetic data base? Answer: no. Alternative
question: do we go looking for linear lemmas about `(g x)`

? Answer:
no. The linear arithmetic data base is built up by a process very
similar to but independent of forward chaining.