author  wenzelm 
Sat, 09 Oct 1999 23:20:02 +0200  
changeset 7819  6dd018b6cf3f 
parent 7800  8ee919e42174 
child 7833  f5288e4b95d1 
permissions  rwrr 
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

1 
(* Title: HOL/Isar_examples/Cantor.thy 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

3 
Author: Markus Wenzel, TU Muenchen 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

4 
*) 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

5 

7800  6 
header {* Cantor's Theorem *}; 
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

7 

7748  8 
theory Cantor = Main:; 
6505  9 

6744  10 
text {* 
7819  11 
This is an Isar'ized version of the final example of the Isabelle/HOL 
12 
manual \cite{isabelleHOL}. 

13 
*}; 

14 

15 
text {* 

16 
Cantor's Theorem states that every set has more subsets than it has 

17 
elements. It has become a favorite basic example in pure 

18 
higherorder logic since it is so easily expressed: \[\all{f::\alpha 

19 
\To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}} 

20 
\all{x::\alpha}. f \ap x \not= S\] 

7748  21 

7819  22 
Viewing types as sets, $\alpha \To \idt{bool}$ represents the 
23 
powerset of $\alpha$. This version of the theorem states that for 

24 
every function from $\alpha$ to its powerset, some subset is outside 

25 
its range. The Isabelle/Isar proofs below use HOL's set theory, with 

26 
the type $\alpha \ap \idt{set}$ and the operator $\idt{range}$. 

7748  27 

7819  28 
\bigskip We first consider a rather verbose version of the proof, 
29 
with the reasoning expressed quite naively. We only make use of the 

30 
pure core of the Isar proof language. 

6744  31 
*}; 
6505  32 

6494  33 
theorem "EX S. S ~: range(f :: 'a => 'a set)"; 
34 
proof; 

7480  35 
let ?S = "{x. x ~: f x}"; 
36 
show "?S ~: range f"; 

6494  37 
proof; 
7480  38 
assume "?S : range f"; 
6494  39 
then; show False; 
40 
proof; 

41 
fix y; 

7480  42 
assume "?S = f y"; 
43 
then; show ?thesis; 

6494  44 
proof (rule equalityCE); 
7480  45 
assume y_in_S: "y : ?S"; 
6494  46 
assume y_in_fy: "y : f y"; 
47 
from y_in_S; have y_notin_fy: "y ~: f y"; ..; 

7480  48 
from y_notin_fy y_in_fy; show ?thesis; by contradiction; 
6494  49 
next; 
7480  50 
assume y_notin_S: "y ~: ?S"; 
6494  51 
assume y_notin_fy: "y ~: f y"; 
52 
from y_notin_S; have y_in_fy: "y : f y"; ..; 

7480  53 
from y_notin_fy y_in_fy; show ?thesis; by contradiction; 
6494  54 
qed; 
55 
qed; 

56 
qed; 

57 
qed; 

58 

6744  59 
text {* 
7819  60 
The following version of the proof essentially does the same 
61 
reasoning, only that it is expressed more neatly, with some derived 

62 
Isar language elements involved. 

6744  63 
*}; 
6494  64 

65 
theorem "EX S. S ~: range(f :: 'a => 'a set)"; 

66 
proof; 

7480  67 
let ?S = "{x. x ~: f x}"; 
68 
show "?S ~: range f"; 

6494  69 
proof; 
7480  70 
assume "?S : range f"; 
6505  71 
thus False; 
6494  72 
proof; 
73 
fix y; 

7480  74 
assume "?S = f y"; 
75 
thus ?thesis; 

6494  76 
proof (rule equalityCE); 
77 
assume "y : f y"; 

7480  78 
assume "y : ?S"; hence "y ~: f y"; ..; 
79 
thus ?thesis; by contradiction; 

6494  80 
next; 
81 
assume "y ~: f y"; 

7480  82 
assume "y ~: ?S"; hence "y : f y"; ..; 
83 
thus ?thesis; by contradiction; 

6494  84 
qed; 
85 
qed; 

86 
qed; 

87 
qed; 

88 

6744  89 
text {* 
7819  90 
How much creativity is required? As it happens, Isabelle can prove 
91 
this theorem automatically. The default classical set contains rules 

92 
for most of the constructs of HOL's set theory. We must augment it 

93 
with \name{equalityCE} to break up set equalities, and then apply 

94 
bestfirst search. Depthfirst search would diverge, but bestfirst 

95 
search successfully navigates through the large search space. 

6744  96 
*}; 
6505  97 

6494  98 
theorem "EX S. S ~: range(f :: 'a => 'a set)"; 
99 
by (best elim: equalityCE); 

100 

6744  101 
text {* 
7819  102 
While this establishes the same theorem internally, we do not get any 
103 
idea of how the proof actually works. There is currently no way to 

104 
transform internal systemlevel representations of Isabelle proofs 

105 
back into Isar documents. Writing proof documents really is a 

106 
creative process. 

6744  107 
*}; 
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

108 

2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

109 
end; 