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
|
\DOC DISJ_CASES
\TYPE {DISJ_CASES : (thm -> thm -> thm -> thm)}
\SYNOPSIS
Eliminates disjunction by cases.
\KEYWORDS
rule, disjunction, cases.
\DESCRIBE
The rule {DISJ_CASES} takes a disjunctive theorem, and two `case'
theorems, each with one of the disjuncts as a hypothesis while sharing
alpha-equivalent conclusions. A new theorem is returned with the same
conclusion as the `case' theorems, and the union of all assumptions
excepting the disjuncts.
{
A |- t1 \/ t2 A1 u {{t1}} |- t A2 u {{t2}} |- t
------------------------------------------------------ DISJ_CASES
A u A1 u A2 |- t
}
\FAILURE
Fails if the first argument is not a disjunctive theorem, or if the
conclusions of the other two theorems are not alpha-convertible.
\EXAMPLE
Specializing the built-in theorem {num_CASES} gives the theorem:
{
th = |- (m = 0) \/ (?n. m = SUC n)
}
\noindent Using two additional theorems, each having one disjunct as a
hypothesis:
{
th1 = (m = 0 |- (PRE m = m) = (m = 0))
th2 = (?n. m = SUC n" |- (PRE m = m) = (m = 0))
}
\noindent a new theorem can be derived:
{
#DISJ_CASES th th1 th2;;
|- (PRE m = m) = (m = 0)
}
\COMMENTS
Neither of the `case' theorems is required to have either disjunct as a
hypothesis, but otherwise {DISJ_CASES} is pointless.
\SEEALSO
DISJ_CASES_TAC, DISJ_CASES_THEN, DISJ_CASES_THEN2, DISJ_CASES_UNION,
DISJ1, DISJ2.
\ENDDOC
|
