Resolves implicative assumptions with an antecedent.
DESCRIPTION
Given a theorem-tactic ttac and a theorem A |- t, the function
ANTE_RES_THEN produces a tactic that attempts to match t to the antecedent
of each implication
Ai |- !x1...xn. ui ==> vi
(where Ai is just !x1...xn. ui ==> vi) that occurs among the
assumptions of a goal. If the antecedent ui of any implication matches t,
then an instance of Ai u A |- vi is obtained by specialization of the
variables x1, ..., xn and type instantiation, followed by an application of
modus ponens. Because all implicative assumptions are tried, this may result
in several modus-ponens consequences of the supplied theorem and the
assumptions. Tactics are produced using ttac from all these theorems, and
these tactics are applied in sequence to the goal. That is,
ANTE_RES_THEN ttac (A |- t) g
has the effect of:
MAP_EVERY ttac [A1 u A |- v1; ...; Am u A |- vm] g
where the theorems Ai u A |- vi are all the consequences that can
be drawn by a (single) matching modus-ponens inference from the implications
that occur among the assumptions of the goal g and the supplied theorem
A |- t.
FAILURE CONDITIONS
ANTE_RES_THEN ttac (A |- t) fails when applied to a goal g if any of the
tactics produced by ttac (Ai u A |- vi), where Ai u A |- vi is the ith
resolvent obtained from the theorem A |- t and the assumptions of g, fails
when applied in sequence to g.