----------------------------------------------------------------------
STRIP_GOAL_THEN                                               (Tactic)
----------------------------------------------------------------------
STRIP_GOAL_THEN : thm_tactic -> tactic

SYNOPSIS
Splits a goal by eliminating one outermost connective, applying the
given theorem-tactic to the antecedents of implications.

KEYWORDS
theorem-tactic.

DESCRIBE
Given a theorem-tactic {ttac} and a goal {(A,t)}, {STRIP_GOAL_THEN} removes one
outermost occurrence of one of the connectives {!}, {==>}, {~} or {/\} from the
conclusion of the goal {t}.  If {t} is a universally quantified term, then
{STRIP_GOAL_THEN} strips off the quantifier:

      A ?- !x.u
   ==============  STRIP_GOAL_THEN ttac
     A ?- u[x'/x]

where {x'} is a primed variant that does not appear free in the
assumptions {A}.  If {t} is a conjunction, then {STRIP_GOAL_THEN} simply splits
the conjunction into two subgoals:

      A ?- v /\ w
   =================  STRIP_GOAL_THEN ttac
    A ?- v   A ?- w

If {t} is an implication {u ==> v} and if:

      A ?- v
  ===============  ttac (u |- u)
     A' ?- v'

then:

      A ?- u ==> v
  ====================  STRIP_GOAL_THEN ttac
        A' ?- v'

Finally, a negation {~t} is treated as the implication {t ==> F}.

FAILURE
{STRIP_GOAL_THEN ttac (A,t)} fails if {t} is not a universally quantified term,
an implication, a negation or a conjunction.  Failure also occurs if the
application of {ttac} fails, after stripping the goal.

EXAMPLE
When solving the goal

   ?- (n = 1) ==> (n * n = n)

a possible initial step is to apply

   STRIP_GOAL_THEN SUBST1_TAC

thus obtaining the goal

   ?- 1 * 1 = 1




USES
{STRIP_GOAL_THEN} is used when manipulating intermediate results (obtained by
stripping outer connectives from a goal) directly, rather than as assumptions.

SEEALSO
Tactic.CONJ_TAC, Thm_cont.DISCH_THEN, Tactic.FILTER_STRIP_THEN,
Tactic.GEN_TAC, Tactic.STRIP_ASSUME_TAC, Tactic.STRIP_TAC.

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