Thm_cont.ANTE_RES

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.