SUBGOAL_THEN : term -> thm_tactic -> tactic

- STRUCTURE
- SYNOPSIS
- Allows the user to introduce a lemma.
- DESCRIPTION
- 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, ifthen
A1 ?- t1 ========== f (u |- u) A2 ?- t2

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 goalUsing SUBGOAL_THEN to focus on the case in which ~(n = 0), rewriting establishes it truth, leaving only the proof that ~(n = 0). That is,
{n = SUC m} ?- (0 = n) ==> t

generates the following subgoals:SUBGOAL_THEN (Term `~(0 = n)`) (fn th => REWRITE_TAC [th])

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

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

HOL Kananaskis-13