SUBGOAL_THEN

Tactical.SUBGOAL_THEN : term -> thm_tactic -> tactic

Allows the user to introduce a lemma.

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.

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