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