author | wenzelm |
Fri, 23 Apr 1999 11:50:35 +0200 | |
changeset 6494 | ab1442d2e4e1 |
parent 6444 | 2ebe9e630cab |
child 6505 | 2863855a6902 |
permissions | -rw-r--r-- |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Isar_examples/Cantor.thy |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel, TU Muenchen |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
4 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
5 |
Cantor's theorem (see also 'Isabelle's Object-Logics'). |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
6 |
*) |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
7 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
8 |
theory Cantor = Main:; |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
9 |
|
6494 | 10 |
|
11 |
theorem "EX S. S ~: range(f :: 'a => 'a set)"; |
|
12 |
proof; |
|
13 |
let ??S = "{x. x ~: f x}"; |
|
14 |
show "??S ~: range f"; |
|
15 |
proof; |
|
16 |
assume "??S : range f"; |
|
17 |
then; show False; |
|
18 |
proof; |
|
19 |
fix y; |
|
20 |
assume "??S = f y"; |
|
21 |
then; show ??thesis; |
|
22 |
proof (rule equalityCE); |
|
23 |
assume y_in_S: "y : ??S"; |
|
24 |
assume y_in_fy: "y : f y"; |
|
25 |
from y_in_S; have y_notin_fy: "y ~: f y"; ..; |
|
26 |
from y_notin_fy y_in_fy; show ??thesis; ..; |
|
27 |
next; |
|
28 |
assume y_notin_S: "y ~: ??S"; |
|
29 |
assume y_notin_fy: "y ~: f y"; |
|
30 |
from y_notin_S; have y_in_fy: "y : f y"; ..; |
|
31 |
from y_notin_fy y_in_fy; show ??thesis; ..; |
|
32 |
qed; |
|
33 |
qed; |
|
34 |
qed; |
|
35 |
qed; |
|
36 |
||
37 |
||
38 |
theorem "EX S. S ~: range(f :: 'a => 'a set)"; |
|
39 |
proof; |
|
40 |
let ??S = "{x. x ~: f x}"; |
|
41 |
show "??S ~: range f"; |
|
42 |
proof; |
|
43 |
assume "??S : range f"; |
|
44 |
then; show False; |
|
45 |
proof; |
|
46 |
fix y; |
|
47 |
assume "??S = f y"; |
|
48 |
then; show ??thesis; |
|
49 |
proof (rule equalityCE); |
|
50 |
assume "y : ??S"; then; have y_notin_fy: "y ~: f y"; ..; |
|
51 |
assume "y : f y"; |
|
52 |
from y_notin_fy it; show ??thesis; ..; |
|
53 |
next; |
|
54 |
assume "y ~: ??S"; then; have y_in_fy: "y : f y"; ..; |
|
55 |
assume "y ~: f y"; |
|
56 |
from it y_in_fy; show ??thesis; ..; |
|
57 |
qed; |
|
58 |
qed; |
|
59 |
qed; |
|
60 |
qed; |
|
61 |
||
62 |
||
63 |
theorem "EX S. S ~: range(f :: 'a => 'a set)"; |
|
64 |
by (best elim: equalityCE); |
|
65 |
||
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
66 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
67 |
end; |