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
|
\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 |- t A2 |- t
-------------------------------------------------- DISJ_CASES
A u (A1 - {{t1}}) u (A2 - {{t2}}) |- 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
Let us create several theorems. Note that {th1} and {th2} draw the same
conclusion from different hypotheses, while {th} proves the disjunction of the
two hypotheses:
{
# let [th; th1; th2] = map (UNDISCH_ALL o REAL_FIELD)
[`~(x = &0) \/ x = &0`;
`~(x = &0) ==> x * (inv(x) * x - &1) = &0`;
`x = &0 ==> x * (inv(x) * x - &1) = &0`];;
...
val th : thm = |- ~(x = &0) \/ x = &0
val th1 : thm = ~(x = &0) |- x * (inv x * x - &1) = &0
val th2 : thm = x = &0 |- x * (inv x * x - &1) = &0
}
\noindent so we can apply {DISJ_CASES}:
{
# DISJ_CASES th th1 th2;;
val it : thm = |- x * (inv x * x - &1) = &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, DISJ1, DISJ2,
SIMPLE_DISJ_CASES.
\ENDDOC
|
