ADD_SGS_TAC : term list -> tactic -> tactic
STRUCTURE
SYNOPSIS
Adds extra sub-goals to the outcome of a tactic, as may be required to make an invalid tactic valid.
DESCRIPTION
Suppose tac applied to the goal (asl,w) produces new goal list gl. Then ADD_SGS_TAC tml tac (asl,w) produces, as new goals, gl and, additionally, (asl,tm) for each tm in tml.

Then, if the justification returned by tac, when applied to the proved goals gl, gives a theorem which uses some additional assumption tm in tml, then the proved goal (asl,tm) is used to remove tm from the assumption list of that theorem.

FAILURE
ADD_SGS_TAC tml tac (asl,w) fails if tac (asl,w) fails.
USES
Where a tactic tac requires certain assumptions tml to be present in the goal, which are not present but are capable of being proved, ADD_SGS_TAC tml tac will conveniently set up new subgoals to prove the missing assumptions.
COMMENTS
VALIDATE tac is similar and will usually be easier to use, but its extra new subgoals may occur in an unpredictable order.
EXAMPLE
Given a goal with an implication in the assumptions, one can split it into two subgoals, defining an auxiliary function
fun split_imp_asm th =
  let val (tm, thu) = UNDISCH_TM th ;
  in ADD_SGS_TAC [tm] (ASSUME_TAC thu) end ;
This can be used as follows:
1 subgoal:
val it =

r
------------------------------------
  p ==> q
:
   proof

> e (FIRST_X_ASSUM split_imp_asm) ;

OK..
2 subgoals:
val it =

r
------------------------------------
  q

p

2 subgoals
:
   proof

To propose a term, prove it as a subgoal and then use it to prove the goal, as is done using SUBGOAL_THEN tm ASSUME_TAC, can also be done by ADD_SGS_TAC [tm] (ASSUME_TAC (ASSUME tm))

SEEALSO
HOL  Kananaskis-14