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
75
76
77
78
79
80
81
82
|
\DOC FILTER_STRIP_TAC
\TYPE {FILTER_STRIP_TAC : (term -> tactic)}
\SYNOPSIS
Conditionally strips apart a goal by eliminating the outermost connective.
\KEYWORDS
tactic, selective.
\DESCRIBE
Stripping apart a goal in a more careful way than is done by {STRIP_TAC} may be
necessary when dealing with quantified terms and implications.
{FILTER_STRIP_TAC} behaves like {STRIP_TAC}, but it does not strip apart a goal
if it contains a given term.
If {u} is a term, then {FILTER_STRIP_TAC u} is a tactic that removes one
outermost occurrence of one of the connectives {!}, {==>}, {~} or {/\} from the
conclusion of the goal {t}, provided the term being stripped does not contain
{u}. A negation {~t} is treated as the implication {t ==> F}.
{FILTER_STRIP_TAC u} also breaks apart conjunctions without applying any
filtering.
If {t} is a universally quantified term, {FILTER_STRIP_TAC u}
strips off the quantifier:
{
A ?- !x.v
================ FILTER_STRIP_TAC "u" [where x is not u]
A ?- v[x'/x]
}
\noindent where {x'} is a primed variant that does not appear free in the
assumptions {A}. If {t} is a conjunction, no filtering is done and
{FILTER_STRIP_TAC u} simply splits the conjunction:
{
A ?- v /\ w
================= FILTER_STRIP_TAC "u"
A ?- v A ?- w
}
\noindent If {t} is an implication and the antecedent does not contain
a free instance of {u}, then {FILTER_STRIP_TAC u} moves the antecedent into the
assumptions and recursively splits the antecedent according to the following
rules (see {STRIP_ASSUME_TAC}):
{
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 variant of {x}.
\FAILURE
{FILTER_STRIP_TAC u (A,t)} fails if {t} is not a universally quantified term,
an implication, a negation or a conjunction; or if the term being
stripped contains {u} in the sense described above (conjunction excluded).
\EXAMPLE
When trying to solve the goal
{
?- !n. m <= n /\ n <= m ==> (m = n)
}
\noindent the universally quantified variable {n} can be stripped off by using
{
FILTER_STRIP_TAC "m:num"
}
\noindent and then the implication can be stripped apart by using
{
FILTER_STRIP_TAC "m:num = n"
}
\USES
{FILTER_STRIP_TAC} is used when stripping outer connectives from a goal in a
more delicate way than {STRIP_TAC}. A typical application is to keep
stripping by using the tactic {REPEAT (FILTER_STRIP_TAC u)}
until one hits the term {u} at which stripping is to stop.
\SEEALSO
CONJ_TAC, FILTER_DISCH_TAC, FILTER_DISCH_THEN, FILTER_GEN_TAC,
STRIP_ASSUME_TAC, STRIP_TAC.
\ENDDOC
|
