We end this section with a somewhat larger example; `
backchain_with` is a tactic that
implements * backchaining*, a restricted form of resolution. It
tries to prove the goal by ``backing through'' hypotheses, i.e., by
finding a hypothesis that is an implication whose consequent matches
the conclusion of the goal, and then recursively calling itself to prove
the antecedents of the implication.

The main component is ` back_thru_hyp`, which, given i, proceeds as
follows. First, it uses ` match_part` to match the conclusion
against part of hypothesis ` i`; if the hypothesis has the form `
: -> -> : -> ( & &
)` (where some of the variables may not be present), and if terms can be
obtained that, when substituted for the in one of the , yield
the conclusion, then ` match_part` succeeds and returns those terms.
The terms are used to obtain instances of the (`
antecedents`). If **m=0** then the goal can be proved immediately; otherwise,
a tactic based on the ` seq` rule is used to obtain the subgoals that the
` seq` rule would produce, except that all but the last of the subgoals
have no extra hypotheses. The last of these subgoals is completely
proved using repeated eliminations; of the rest, the ones
which have conclusions of the form
` a in A` are
left for the membership tactic , and

When invoked, ` backchain_with` first breaks down the conclusion
and then tries to back through each
hypothesis in turn until it succeeds; if it does not, the tactic
` tactic` is applied. If ` tactic` is `
\p.fail` then

letrec backchain_with tactic =

let atomize_concl = REPEAT (\ p . let c = concl p in if is_function_term c or is_and_term c then intro p else fail ) in

let back_thru_hyp i p = let t = type_of_hyp i p and c = conclusion p in let inst_list = match_part c t in let antecedents = antecedents t inst_list in ( if null antecedents then repeat_and_elim i THEN hypothesis else parallel_seq antecedents THEN (\ p . (if conclusion p = c then repeat_function_elim i inst_list THEN ( hypothesis ORELSE ( apply_to_last_hyp repeat_and_elim THEN hypothesis ) ) else if_not_membership_goal (backchain_with tactic) ) p ) ) p in

atomize_concl THEN if_not_membership_goal (apply_to_a_hyp back_thru_hyp ORELSE tactic) ;;

Thu Sep 14 08:45:18 EDT 1995