SUBGOAL_THEN : term -> thm_tactic -> tactic

SYNOPSIS

Introduces a lemma as a new subgoal.

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 apply to the goal. That is, if

    A1 ?- t1
   ==========  ttac (t |- t)
    A2 ?- t2

then

         A1 ?- t1
   ====================  SUBGOAL_THEN `t` ttac
    A1 ?- t   A2 ?- t2

In the quite common special case where ttac is ASSUME_TAC, the net behaviour is simply to present the user with two subgoals, one in which the lemma is to be proved and one in which it may be assumed:

         A1 ?- t1
   ============================  SUBGOAL_THEN `t` ASSUME_TAC
    A1 ?- t   A1 u {t} ?- t2

FAILURE CONDITIONS

SUBGOAL_THEN will fail if an attempt is made to use a non-boolean term as a lemma.

USES

Introducing lemmas into the same basic proof script without separately binding them to names. This is often a good structuring technique for large tactic proofs, where separate lemmas might look artificial because of all the ad-hoc context in which they occur.

EXAMPLE

Consider the proof of the Knaster-Tarski fixpoint theorem, to be found in Library/card.ml. This (in its set-lattice context) states that every monotonic function has a fixpoint. After setting the initial goal:

  # g `!f. (!s t. s SUBSET t ==> f(s) SUBSET f(t)) ==> ?s:A->bool. f(s) = s`;;

we start off the proof, already proceeding via a series of lemmas with SUBGOAL_THEN, though we will focus our attention on a later one:

  # e(REPEAT STRIP_TAC THEN MAP_EVERY ABBREV_TAC
       [`Y = {b:A->bool | f(b) SUBSET b}`; `a:A->bool = INTERS Y`] THEN
      SUBGOAL_THEN `!b:A->bool. b IN Y <=> f(b) SUBSET b` ASSUME_TAC THENL
       [EXPAND_TAC "Y" THEN REWRITE_TAC[IN_ELIM_THM]; ALL_TAC] THEN
      SUBGOAL_THEN `!b:A->bool. b IN Y ==> f(a:A->bool) SUBSET b`
      ASSUME_TAC THENL
       [ASM_MESON_TAC[SUBSET_TRANS; IN_INTERS; SUBSET]; ALL_TAC]);;
  ...
  val it : goalstack = 1 subgoal (1 total)

   0 [`!s t. s SUBSET t ==> f s SUBSET f t`]
   1 [`{b | f b SUBSET b} = Y`]
   2 [`INTERS Y = a`]
   3 [`!b. b IN Y <=> f b SUBSET b`]
   4 [`!b. b IN Y ==> f a SUBSET b`]

  `?s. f s = s`

Now we select a particularly interesting lemma:

  # e(SUBGOAL_THEN `f(a:A->bool) SUBSET a` ASSUME_TAC);;
  val it : goalstack = 2 subgoals (2 total)

   0 [`!s t. s SUBSET t ==> f s SUBSET f t`]
   1 [`{b | f b SUBSET b} = Y`]
   2 [`INTERS Y = a`]
   3 [`!b. b IN Y <=> f b SUBSET b`]
   4 [`!b. b IN Y ==> f a SUBSET b`]
   5 [`f a SUBSET a`]

  `?s. f s = s`

   0 [`!s t. s SUBSET t ==> f s SUBSET f t`]
   1 [`{b | f b SUBSET b} = Y`]
   2 [`INTERS Y = a`]
   3 [`!b. b IN Y <=> f b SUBSET b`]
   4 [`!b. b IN Y ==> f a SUBSET b`]

  `f a SUBSET a`

The lemma is relatively easy to prove by giving MESON_TAC the right lemmas:

  # e(ASM_MESON_TAC[IN_INTERS; SUBSET]);;
  ...
  val it : goalstack = 1 subgoal (1 total)

   0 [`!s t. s SUBSET t ==> f s SUBSET f t`]
   1 [`{b | f b SUBSET b} = Y`]
   2 [`INTERS Y = a`]
   3 [`!b. b IN Y <=> f b SUBSET b`]
   4 [`!b. b IN Y ==> f a SUBSET b`]
   5 [`f a SUBSET a`]

  `?s. f s = s`

and the remaining subgoal is also quite easy for MESON_TAC:

  # e(ASM_MESON_TAC[SUBSET_ANTISYM; IN_INTERS]);;
  ...
  val it : goalstack = No subgoals

On the other hand, without splitting off the last lemmas, MESON_TAC finds the automated step rather large. If you step back three steps with

  # b(); b(); b();;

then although the following works, it takes half a minute:

  # e(ASM_MESON_TAC[IN_INTERS; SUBSET; SUBSET_ANTISYM]);;
  ....
  val it : goalstack = No subgoals