Make a rule to forward chain when a certain trigger arises

See rule-classes for a general discussion of rule classes, including how they are used to build rules from formulas and a discussion of the various keywords in a rule class description.

Examples: (defthm p-and-r-forward ; When (p a) appears in a formula to be (implies (and (p x) (r x)) ; simplified, try to establish (p a) and (q (f x))) ; (r a) and, if successful, add (q (f a)) :rule-classes :forward-chaining) ; to the known assumptions. (defthm p-and-r-forward ; as above with most defaults filled in (implies (and (p x) (r x)) (q (f x))) :rule-classes ((:forward-chaining :trigger-terms ((p x)) :corollary (implies (and (p x) (r x)) (q (f x))) :match-free :all)))

To specify the triggering terms provide a non-empty list of terms as the
value of the

General Form: Any theorem, provided an acceptable triggering term exists.

The structure of this documentation is as follows. First we give a brief
overview of forward chaining and contrast it to backchaining (rewriting).
Then we lay out the syntactic restrictions on

*Overview and When to Use Forward Chaining*

Forward chaining is performed as part of the simplification process: before
the goal is rewritten a *context* is established. The context tells the
theorem prover what may be assumed during rewriting, in particular, to
establish hypotheses of rewrite rules. Forward chaining is used to extend the
context before rewriting begins. For example, the

Forward chaining and backchaining are duals. If a rewrite rule requires
that

As a rule of thumb, if a conclusion like

The following example illustrates that forward chaining may be indispensable in a scenario with free-variables, whose handling is quite weak with rewrite rules.

(defstub p0 (x) t) (defstub p1 (x) t) (defstub p2 (y) t) (defaxiom p0-implies-p1 (implies (p0 x) (p1 x)) :rule-classes :forward-chaining) (defaxiom p1-implies-p2 (implies (p1 x) (p2 y))) ; ACL2 proves the following, but only because p0-implies-p1 is a ; :forward-chaining rule. If p0-implies-p1 is instead a :rewrite ; rule, then the proof fails for the following event. (thm (implies (p0 x) (p2 y)))

*Syntactic Restrictions*

Forward chaining rules are generated from the corollary term (see rule-classes) as follows. First, every `let` expression is expanded
away (hence, so is every `let*` and `lambda` expression), and
trivial ``guard holders'' are removed; see guard-holders. If the
resulting term has the form `implies`, we process it as we process the conclusion in
the first case.

Note that unlike rewrite rules, a nested implication is not folded into a single implication. Consider for example the following term.

(implies (p1 x) (implies (p2 x) (p3 x)))

Although this term is parsed for a rewrite rule as

The

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.

*More Details about Forward Chaining*

*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, and certain heuristics approve of the newly
derived conclusion, we add the instantiated conclusion to our known
assumptions. Since this might introduce new terms into the assumptions,
forward chaining is repeated. Heuristic approval of each new addition is
necessary to avoid infinite looping as would happen with the rule

*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. (For insiders: forward chaining
extends the `type-alist`.) The context starts out with ``obvious''
consequences of the negation of the goal. For example, if the goal is

(implies (and (p A) (q (f A))) (c A))

then the context notes that

However, forward-chaining does support the linear arithmetic reasoning
package. For example, suppose that forward-chaining puts

Debugging

- Forward-chaining-reports
- To see reports about the forward chaining process
- Case-split
- Like force but immediately splits the top-level goal on the hypothesis