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 DISJ_CASES_THEN
\TYPE {DISJ_CASES_THEN : thm_tactical}
\SYNOPSIS
Applies a theorem-tactic to each disjunct of a disjunctive theorem.
\KEYWORDS
theorem-tactic, disjunction, cases.
\DESCRIBE
If the theorem-tactic {f:thm->tactic} applied to either
{ASSUME}d disjunct produces results as follows when applied to a goal
{(A ?- t)}:
{
A ?- t A ?- t
========= f (u |- u) and ========= f (v |- v)
A ?- t1 A ?- t2
}
\noindent then applying {DISJ_CASES_THEN f (|- u \/ v)}
to the goal {(A ?- t)} produces two subgoals.
{
A ?- t
====================== DISJ_CASES_THEN f (|- u \/ v)
A ?- t1 A ?- t2
}
\FAILURE
Fails if the theorem is not a disjunction. An invalid tactic is
produced if the theorem has any hypothesis which is not
alpha-convertible to an assumption of the goal.
\EXAMPLE
Given the theorem
{
th = |- (m = 0) \/ (?n. m = SUC n)
}
\noindent and a goal of the form {?- (PRE m = m) = (m = 0)},
applying the tactic
{
DISJ_CASES_THEN MP_TAC th
}
\noindent produces two subgoals, each with one disjunct as an added
antecedent
{
# let th = SPEC `m:num` num_CASES;;
val th : thm = |- m = 0 \/ (?n. m = SUC n)
# g `PRE m = m <=> m = 0`;;
Warning: Free variables in goal: m
val it : goalstack = 1 subgoal (1 total)
`PRE m = m <=> m = 0`
# e(DISJ_CASES_THEN MP_TAC th);;
val it : goalstack = 2 subgoals (2 total)
`(?n. m = SUC n) ==> (PRE m = m <=> m = 0)`
`m = 0 ==> (PRE m = m <=> m = 0)`
}
\USES
Building cases tactics. For example, {DISJ_CASES_TAC} could be defined by:
{
let DISJ_CASES_TAC = DISJ_CASES_THEN ASSUME_TAC
}
\COMMENTS
Use {DISJ_CASES_THEN2} to apply different tactic generating functions
to each case.
\SEEALSO
STRIP_THM_THEN, CHOOSE_THEN, CONJUNCTS_THEN, CONJUNCTS_THEN2,
DISJ_CASES_TAC, DISJ_CASES_THEN2.
\ENDDOC
|
