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
|
\DOC DISJ_CASES_TAC
\TYPE {DISJ_CASES_TAC : thm_tactic}
\SYNOPSIS
Produces a case split based on a disjunctive theorem.
\KEYWORDS
tactic, disjunction, cases.
\DESCRIBE
Given a theorem {th} of the form {A |- u \/ v}, {DISJ_CASES_TAC th}
applied to a goal
produces two subgoals, one with {u} as an assumption and one with {v}:
{
A ?- t
================================= DISJ_CASES_TAC (A |- u \/ v)
A u {{u}} ?- t A u {{v}}?- t
}
\FAILURE
Fails if the given theorem does not have a disjunctive conclusion.
\EXAMPLE
Given the simple fact about arithmetic {th}, {|- m = 0 \/ (?n. m = SUC n)},
the tactic {DISJ_CASES_TAC th} can be used to produce a case split:
{
# let th = SPEC `m:num` num_CASES;;
val th : thm = |- m = 0 \/ (?n. m = SUC n)
# g `(P:num -> bool) m`;;
Warning: Free variables in goal: P, m
val it : goalstack = 1 subgoal (1 total)
`P m`
# e(DISJ_CASES_TAC th);;
val it : goalstack = 2 subgoals (2 total)
0 [`?n. m = SUC n`]
`P m`
0 [`m = 0`]
`P m`
}
\USES
Performing a case analysis according to a disjunctive theorem.
\SEEALSO
ASSUME_TAC, ASM_CASES_TAC, COND_CASES_TAC, DISJ_CASES_THEN, STRUCT_CASES_TAC.
\ENDDOC
|
