1\DOC STRIP_TAC
2
3\TYPE {STRIP_TAC : tactic}
4
5\SYNOPSIS
6Splits a goal by eliminating one outermost connective.
7
8\KEYWORDS
9tactic.
10
11\DESCRIBE
12Given a goal {(A,t)}, {STRIP_TAC} removes one outermost occurrence of
13one of the connectives {!}, {==>}, {~} or {/\} from the conclusion of
14the goal {t}.  If {t} is a universally quantified term, then {STRIP_TAC}
15strips off the quantifier:
16{
17      A ?- !x.u
18   ==============  STRIP_TAC
19     A ?- u[x'/x]
20}
21where {x'} is a primed variant that does not appear free in the
22assumptions {A}.  If {t} is a conjunction, then {STRIP_TAC} simply splits
23the conjunction into two subgoals:
24{
25      A ?- v /\ w
26   =================  STRIP_TAC
27    A ?- v   A ?- w
28}
29If {t} is an implication, {STRIP_TAC} moves the antecedent into the
30assumptions, stripping conjunctions, disjunctions and existential
31quantifiers according to the following rules:
32{
33    A ?- v1 /\ ... /\ vn ==> v            A ?- v1 \/ ... \/ vn ==> v
34   ============================        =================================
35       A u {v1,...,vn} ?- v             A u {v1} ?- v ... A u {vn} ?- v
36
37     A ?- ?x.w ==> v
38   ====================
39    A u {w[x'/x]} ?- v
40}
41where {x'} is a primed variant of {x} that does not appear free in
42{A}. Finally, a negation {~t} is treated as the implication {t ==> F}.
43
44\FAILURE
45{STRIP_TAC (A,t)} fails if {t} is not a universally quantified term,
46an implication, a negation or a conjunction.
47
48\EXAMPLE
49Applying {STRIP_TAC} twice to the goal:
50{
51    ?- !n. m <= n /\ n <= m ==> (m = n)
52}
53results in the subgoal:
54{
55   {n <= m, m <= n} ?- m = n
56}
57
58
59\USES
60When trying to solve a goal, often the best thing to do first
61is {REPEAT STRIP_TAC} to split the goal up into manageable pieces.
62
63\SEEALSO
64Tactic.CONJ_TAC, Tactic.DISCH_TAC, Thm_cont.DISCH_THEN, Tactic.GEN_TAC,
65Tactic.STRIP_ASSUME_TAC, Tactic.STRIP_GOAL_THEN.
66\ENDDOC
67