ANTE_RES_THEN

Thm_cont.ANTE_RES_THEN : thm_tactical

Resolves implicative assumptions with an antecedent.

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. Any negation ~v that appears among the assumptions of the goal is treated as an implication v ==> F. The sequence in which the theorems Ai u A |- vi are generated and the corresponding tactics applied is unspecified.

Failure

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.

Painfully detailed proof hacking.

See also

Tactic.IMP_RES_TAC, Thm_cont.IMP_RES_THEN, Drule.MATCH_MP, Tactic.RES_TAC, Thm_cont.RES_THEN