STRIP_GOAL_THEN : thm_tactic -> tactic

- STRUCTURE
- SYNOPSIS
- Splits a goal by eliminating one outermost connective, applying the given theorem-tactic to the antecedents of implications.
- DESCRIPTION
- 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: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 ?- !x.u ============== STRIP_GOAL_THEN ttac A ?- u[x'/x]

If t is an implication u ==> v and if:A ?- v /\ w ================= STRIP_GOAL_THEN ttac A ?- v A ?- w

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

Finally, a negation ~t is treated as the implication t ==> F.A ?- u ==> v ==================== STRIP_GOAL_THEN ttac A' ?- v'

- 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 goala possible initial step is to apply
?- (n = 1) ==> (n * n = n)

thus obtaining the goalSTRIP_GOAL_THEN SUBST1_TAC

?- 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

HOL Kananaskis-14