----------------------------------------------------------------------
PROVEHYP_THEN                                               (Thm_cont)
----------------------------------------------------------------------
PROVEHYP_THEN : (thm -> thm -> tactic) -> thm -> tactic

SYNOPSIS
Makes antecedent of theorem as subgoal, continues with both parts as theorems.

KEYWORDS
Theorem-tactical.

DESCRIBE
An application of the tactic {PROVEHYP_THEN th2tac th} to a goal {g} requires that {th} be an implication (or a negation, in which case {‘~p’} is treated as {‘p ==> F’}). Given an implication {|- l ==> r}, 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 {r}. (The former has just been proved by the user; the latter is the result of applying {MP} to {th} and {l}.)

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}.

SEEALSO
Tactic.impl_keep_tac, Tactic.impl_tac.

----------------------------------------------------------------------