Forward and Backward Chaining

Forward  and backward chaining  involves treating a component of a universal formula (see Section ) as a derived rule of inference. Backward chaining involves matching the conclusion of a sequent against the consequent of a universal formula. The antecedents of the universal formula, instantiated using the substitution resulting from the match, then become new subgoals. Forward chaining involves matching hypotheses of a sequent against antecedents of a universal formula. The consequent of the universal formula, instantiated using the substitution resulting from the match, then becomes a new hypothesis.

BackThruLemma name
BackThruHyp i

The name ( i) argument selects the lemma (hypothesis) to back-chain through. Subgoals corresponding to antecents of the lemma (hyp) are labelled with antecedent. The rest are labelled wf. Aliases are BLemma  and BHyp .

FwdThruLemma name is
FwdThruHyp i is

The name ( i) argument selects the lemma (hypothesis) to forward chain through. is selects the hypotheses which are to be matched against antecedents of the chaining formula. The order of the is is immaterial; the tactics try all possible pairings of hypotheses with antecedents. If there are more antecedents that hyps listed in the is, the antecedents not matched will manifest themselves as new subgoals to be proved. The main subgoal with the consequent of the lemma (hyp) asserted is labelled main. Unmatched antecedents are labelled antecedent and the rest are labelled wf. Aliases are FLemma  and FHyp .

Chaining tactics take a number of optional arguments .

• An explicit list of variable bindings as a sub argument. This argument is necessary when all variable bindings cannot be inferred from matching. The sub argument is supplied using the Using tactical. For example:

  Using [`n`.'3'] (BackThruLemma `int_upper_induction`)  

  would bind the variable n in the lemma int_upper_induction to the value 3.

• A specific simple component of a general formula can be selected using an `n` argument, supplied by using the Sel tactical. For example

  Sel 2 (FwdThruLemma `add_mono_wrt_eq`)

  An `n` argument of -1 forces the tactic to treat the formula as a simple formula.

Backchain bc_names
CompleteBackchain bc_names

Repeatedly try BackThruLemma using lemmas named in bc_names in order given. Backchain leaves alone any subgoals which don't match the consequent of any of the lemmas. CompleteBackchain backtracks in the event of any such subgoal coming up.  
In addition to lemma names, a few special names are recognized:
• An integer i. Use hypothesis i. (i must be a positive integer. Negative integers can't be used to refer to hypotheses here.)
• hyps: hyps where n is the number of hyps. Skips hyps which declare variables.
• rev_hyps: As hyps but in order .
• new_hyps: new hyps introduced by backchaining, least recent first.
• rev_new_hyps: As new_hyps but in opposite order.

HypBackchain Backchain ``rev_new_hyps rev_hyps``
  CompleteHypBackchain CompleteBackchain ``rev_new_hyps rev_hyps``
 

InstLemma name [t1;...;tn]

Instantiate lemma name with terms t1 through tn.   If the lemma has m distinct level expressions, the first m terms should be level expressions to substitute for the lemma's level expressions. (Inject level expression le into the term type using the special term parameterle:l . In the term editor you select this term by the name parameter.)

InstHyp [t1;...;tn] i

Instantiate universal formula in hyp i with terms t1 through tn.

Instantiate existential quantifiers in conclusion with terms t1 through tn.