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