RES_THEN
Thm_cont.RES_THEN : (thm_tactic -> tactic)
Resolves all implicative assumptions against the rest.
Like the basic resolution function IMP_RES_THEN, the resolution tactic
RES_THEN performs a single-step resolution of an implication and the
assumptions of a goal. RES_THEN differs from IMP_RES_THEN only in
that the implications used for resolution are taken from the assumptions
of the goal itself, rather than supplied as an argument.
When applied to a goal A ?- g, the tactic RES_THEN ttac uses
RES_CANON to obtain a set of implicative theorems in canonical form
from the assumptions A of the goal. Each of the resulting theorems (if
there are any) will have the form:
ai |- !x1...xn. ui ==> vi
where ai is one of the assumptions of the goal. Having obtained these
implications, RES_THEN then attempts to match each antecedent ui to
each assumption aj |- aj in the assumptions A. If the antecedent
ui of any implication matches the conclusion aj of any assumption,
then an instance of the theorem ai, aj |- vi, called a 'resolvent', is
obtained by specialization of the variables x1, ..., xn and type
instantiation, followed by an application of modus ponens. There may be
more than one canonical implication derivable from the assumptions of
the goal and each such implication is tried against every assumption, so
there may be several resolvents (or, indeed, none).
Tactics are produced using the theorem-tactic ttac from all these
resolvents (failures of ttac at this stage are filtered out) and these
tactics are then applied in an unspecified sequence to the goal. That
is,
RES_THEN ttac (A ?- g)
has the effect of:
MAP_EVERY (mapfilter ttac [... ; (ai,aj |- vi) ; ...]) (A ?- g)
where the theorems ai,aj |- vi are all the consequences that can be
drawn by a (single) matching modus-ponens inference from the assumptions
A and the implications derived using RES_CANON from the assumptions.
The sequence in which the theorems ai,aj |- vi are generated and the
corresponding tactics applied is unspecified.
Failure
Evaluating RES_THEN ttac th fails with 'no implication' if no
implication(s) can be derived from the assumptions of the goal by the
transformation process described under the entry for RES_CANON.
Evaluating RES_THEN ttac (A ?- g) fails with 'no resolvents' if no
assumption of the goal A ?- g can be resolved with the derived
implication or implications. Evaluation also fails, with 'no tactics',
if there are resolvents, but for every resolvent ai,aj |- vi
evaluating the application ttac (ai,aj |- vi) fails---that is, if for
every resolvent ttac fails to produce a tactic. Finally, failure is
propagated if any of the tactics that are produced from the resolvents
by ttac fails when applied in sequence to the goal.
See also
Tactic.IMP_RES_TAC,
Thm_cont.IMP_RES_THEN,
Drule.MATCH_MP,
Drule.RES_CANON,
Tactic.RES_TAC