----------------------------------------------------------------------
SUBGOAL_THEN                                                (Tactical)
----------------------------------------------------------------------
SUBGOAL_THEN : term -> thm_tactic -> tactic

SYNOPSIS
Allows the user to introduce a lemma.

KEYWORDS
theorem-tactic, lemma.

DESCRIBE
The user proposes a lemma and is then invited to prove it under the
current assumptions.  The lemma is then used with the {thm_tactic} to
simplify the goal.  That is, if

    A1 ?- t1
   ==========  f (u |- u)
    A2 ?- t2

then

         A1 ?- t1
   ====================  SUBGOAL_THEN u f
    A1 ?- u   A2 ?- t2


Typically {f (u |- u)} will be an invalid tactic because it would
return a validation function which generated the theorem {A1,u |- t1}
from the theorem {A2 |- t2}.  Nonetheless, the tactic
{SUBGOAL_THEN u f} is valid because of the extra sub-goal where {u}
must be proved.

FAILURE
{SUBGOAL_THEN} will fail if an attempt is made to use a
nonboolean term as a lemma.

USES
When combined with {rotate}, {SUBGOAL_THEN} allows the user to defer
some part of a proof and to continue with another part.
{SUBGOAL_THEN} is most convenient when the tactic solves the original
goal, leaving only the subgoal.  For example, suppose the user wishes
to prove the goal

   {n = SUC m} ?- (0 = n) ==> t

Using {SUBGOAL_THEN} to focus on the case in which {~(n = 0)},
rewriting establishes it truth, leaving only the proof that {~(n = 0)}.
That is,

   SUBGOAL_THEN (Term `~(0 = n)`) (fn th => REWRITE_TAC [th])

generates the following subgoals:

   {n = SUC m} ?-  ~(0 = n)
   ?- T


COMMENTS
Some users may expect the generated tactic to be {f (A1 |- u)}, rather
than {f (u |- u)}.

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