PROVEHYP_THEN
Thm_cont.PROVEHYP_THEN : (thm -> thm -> tactic) -> thm -> tactic
Makes antecedent of theorem as subgoal, continues with both parts as theorems.
An application of the tactic PROVEHYP_THEN th2tac th to a goal g
requires that th be an (universally quantified) implication (or a
negation, in which case ~p is treated as p ==> F). Given an
implication |- !x1..xn. l ==> r x1..xn, the result is a new sub-goal
requiring the user to prove l, and the application of th2tac to the
theorems with conclusion l and !x1..xn. r x1..xn.
Diagrammatically, one might see this as
A ?- g
============================================== PROVEHYP_THEN th2tac th
A ?- l ... th2tac (A |- l) (A |- r) (A ?- g)
Failure
Fails if the theorem argument is not an implication or negation.
Example
> FIRST_X_ASSUM (PROVEHYP_THEN (K MP_TAC)) ([“p”, “p ==> q”], “r”)
val it = ([([“p”], “p”), ([“p”], “q ==> r”)], fn):
goal list * validation
The use of FIRST_X_ASSUM pulls out the first implicational theorem,
and gives the user the requirement to prove p as a subgoal. In the
other subgoal, q has become a new antecedent in the goal (thanks to
the action of MP_TAC).
Comments
This function is also available under the name provehyp_then.