author  wenzelm 
Mon, 11 Oct 1999 20:44:23 +0200  
changeset 7833  f5288e4b95d1 
parent 7819  6dd018b6cf3f 
child 7860  7819547df4d8 
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 

7833  8 
theory Cantor = Main:;verbatim {* \footnote{This is an Isar version of 
9 
the final example of the Isabelle/HOL manual \cite{isabelleHOL}.} 

7819  10 
*}; 
11 

12 
text {* 

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

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

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

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

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

7748  18 

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

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

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

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

7748  24 

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

27 
pure core of the Isar proof language. 

6744  28 
*}; 
6505  29 

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

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

6494  34 
proof; 
7480  35 
assume "?S : range f"; 
6494  36 
then; show False; 
37 
proof; 

38 
fix y; 

7480  39 
assume "?S = f y"; 
40 
then; show ?thesis; 

6494  41 
proof (rule equalityCE); 
7480  42 
assume y_in_S: "y : ?S"; 
6494  43 
assume y_in_fy: "y : f y"; 
44 
from y_in_S; have y_notin_fy: "y ~: f y"; ..; 

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

7480  50 
from y_notin_fy y_in_fy; show ?thesis; by contradiction; 
6494  51 
qed; 
52 
qed; 

53 
qed; 

54 
qed; 

55 

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

59 
Isar language elements involved. 

6744  60 
*}; 
6494  61 

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

63 
proof; 

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

6494  66 
proof; 
7480  67 
assume "?S : range f"; 
6505  68 
thus False; 
6494  69 
proof; 
70 
fix y; 

7480  71 
assume "?S = f y"; 
72 
thus ?thesis; 

6494  73 
proof (rule equalityCE); 
74 
assume "y : f y"; 

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

6494  77 
next; 
78 
assume "y ~: f y"; 

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

6494  81 
qed; 
82 
qed; 

83 
qed; 

84 
qed; 

85 

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

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

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

91 
bestfirst search. Depthfirst search would diverge, but bestfirst 

92 
search successfully navigates through the large search space. 

6744  93 
*}; 
6505  94 

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

97 

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

101 
transform internal systemlevel representations of Isabelle proofs 

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

103 
creative process. 

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

105 

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

106 
end; 