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
|
\DOC STRIP_THM_THEN
\TYPE {STRIP_THM_THEN : thm_tactical}
\SYNOPSIS
{STRIP_THM_THEN} applies the given theorem-tactic using the result of
stripping off one outer connective from the given theorem.
\KEYWORDS
theorem-tactic.
\DESCRIBE
Given a theorem-tactic {ttac}, a theorem {th} whose conclusion is a
conjunction, a disjunction or an existentially quantified term, and a goal
{(A,t)}, {STRIP_THM_THEN ttac th} first strips apart the conclusion of {th},
next applies {ttac} to the theorem(s) resulting from the stripping and then
applies the resulting tactic to the goal.
In particular, when stripping a conjunctive theorem {A'|- u /\ v}, the tactic
{
ttac(u|-u) THEN ttac(v|-v)
}
\noindent resulting from applying {ttac} to the conjuncts, is applied to the
goal. When stripping a disjunctive theorem {A'|- u \/ v}, the tactics
resulting from applying {ttac} to the disjuncts, are applied to split the goal
into two cases. That is, if
{
A ?- t A ?- t
========= ttac (u|-u) and ========= ttac (v|-v)
A ?- t1 A ?- t2
}
\noindent then:
{
A ?- t
================== STRIP_THM_THEN ttac (A'|- u \/ v)
A ?- t1 A ?- t2
}
\noindent When stripping an existentially quantified theorem {A'|- ?x.u}, the
tactic {ttac(u|-u)}, resulting from applying {ttac} to the body of the
existential quantification, is applied to the goal. That is, if:
{
A ?- t
========= ttac (u|-u)
A ?- t1
}
\noindent then:
{
A ?- t
============= STRIP_THM_THEN ttac (A'|- ?x. u)
A ?- t1
}
The assumptions of the theorem being split are not added to the assumptions of
the goal(s) but are recorded in the proof. If {A'} is not a subset of the
assumptions {A} of the goal (up to alpha-conversion), {STRIP_THM_THEN ttac th}
results in an invalid tactic.
\FAILURE
{STRIP_THM_THEN ttac th} fails if the conclusion of {th} is not a conjunction,
a disjunction or an existentially quantified term. Failure also occurs if the
application of {ttac} fails, after stripping the outer connective from the
conclusion of {th}.
\USES
{STRIP_THM_THEN} is used enrich the assumptions of a goal with a stripped
version of a previously-proved theorem.
\SEEALSO
CHOOSE_THEN, CONJUNCTS_THEN, DISJ_CASES_THEN, STRIP_ASSUME_TAC.
\ENDDOC
|
