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
|
\DOC STRIP_GOAL_THEN
\TYPE {STRIP_GOAL_THEN : (thm_tactic -> tactic)}
\SYNOPSIS
Splits a goal by eliminating one outermost connective, applying the
given theorem-tactic to the antecedents of implications.
\KEYWORDS
theorem-tactic.
\DESCRIBE
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:
{
A ?- !x.u
============== STRIP_GOAL_THEN ttac
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_GOAL_THEN} simply splits
the conjunction into two subgoals:
{
A ?- v /\ w
================= STRIP_GOAL_THEN ttac
A ?- v A ?- w
}
\noindent If {t} is an implication {"u ==> v"} and if:
{
A ?- v
=============== ttac (u |- u)
A' ?- v'
}
\noindent then:
{
A ?- u ==> v
==================== STRIP_GOAL_THEN ttac
A' ?- v'
}
\noindent Finally, a negation {~t} is treated as the implication {t ==> F}.
\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 goal
{
?- (n = 1) ==> (n * n = n)
}
\noindent a possible initial step is to apply
{
STRIP_GOAL_THEN SUBST1_TAC
}
\noindent thus obtaining the goal
{
?- 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
CONJ_TAC, DISCH_THEN, FILTER_STRIP_THEN, GEN_TAC, STRIP_ASSUME_TAC, STRIP_TAC.
\ENDDOC
|
