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 backchain_with is recursively applied to the remainder.
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 backchain_with behaves like a primitive Prolog
interpreter, where the hypotheses are the clauses and the conclusion is
the query. The fact that backchain_with
takes a tactic as an argument
allows one to make this basic search method more powerful, since it
means that one can specify what actions to take at the ``leaves''
of the search.
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) ;;