author  wenzelm 
Sun, 30 Jul 2000 13:02:56 +0200  
changeset 9474  b0ce3b7c9c26 
parent 7982  d534b897ce39 
child 10007  64bf7da1994a 
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 

7955  8 
theory Cantor = Main:; 
9 

10 
text_raw {* 

11 
\footnote{This is an Isar version of the final example of the 

12 
Isabelle/HOL manual \cite{isabelleHOL}.} 

7819  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}} 

7874  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 

7860  25 
its range. The Isabelle/Isar proofs below uses HOL's set theory, 
7874  26 
with the type $\alpha \ap \idt{set}$ and the operator 
27 
$\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$. 

7748  28 

7860  29 
\bigskip We first consider a slightly awkward version of the proof, 
7874  30 
with the innermost reasoning expressed quite naively. 
6744  31 
*}; 
6505  32 

7982  33 
theorem "EX S. S ~: range (f :: 'a => 'a set)"; 
6494  34 
proof; 
7480  35 
let ?S = "{x. x ~: f x}"; 
36 
show "?S ~: range f"; 

6494  37 
proof; 
7480  38 
assume "?S : range f"; 
7860  39 
thus False; 
6494  40 
proof; 
41 
fix y; 

7480  42 
assume "?S = f y"; 
7860  43 
thus ?thesis; 
6494  44 
proof (rule equalityCE); 
7860  45 
assume in_S: "y : ?S"; 
46 
assume in_fy: "y : f y"; 

47 
from in_S; have notin_fy: "y ~: f y"; ..; 

48 
from notin_fy in_fy; show ?thesis; by contradiction; 

6494  49 
next; 
7860  50 
assume notin_S: "y ~: ?S"; 
51 
assume notin_fy: "y ~: f y"; 

52 
from notin_S; have in_fy: "y : f y"; ..; 

53 
from notin_fy 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 
7860  61 
reasoning, only that it is expressed more neatly. In particular, we 
62 
change the order of assumptions introduced in the two cases of rule 

63 
\name{equalityCE}, streamlining the flow of intermediate facts and 

64 
avoiding explicit naming.\footnote{In general, neither the order of 

7874  65 
assumptions as introduced by \isacommand{assume}, nor the order of 
66 
goals as solved by \isacommand{show} is of any significance. The 

67 
basic logical structure has to be left intact, though. In 

68 
particular, assumptions ``belonging'' to some goal have to be 

69 
introduced \emph{before} its corresponding \isacommand{show}.} 

6744  70 
*}; 
6494  71 

7982  72 
theorem "EX S. S ~: range (f :: 'a => 'a set)"; 
6494  73 
proof; 
7480  74 
let ?S = "{x. x ~: f x}"; 
75 
show "?S ~: range f"; 

6494  76 
proof; 
7480  77 
assume "?S : range f"; 
6505  78 
thus False; 
6494  79 
proof; 
80 
fix y; 

7480  81 
assume "?S = f y"; 
82 
thus ?thesis; 

6494  83 
proof (rule equalityCE); 
84 
assume "y : f y"; 

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

6494  87 
next; 
88 
assume "y ~: f y"; 

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

6494  91 
qed; 
92 
qed; 

93 
qed; 

94 
qed; 

95 

6744  96 
text {* 
7819  97 
How much creativity is required? As it happens, Isabelle can prove 
9474  98 
this theorem automatically using bestfirst search. Depthfirst 
99 
search would diverge, but bestfirst search successfully navigates 

100 
through the large search space. The context of Isabelle's classical 

101 
prover contains rules for the relevant constructs of HOL's set 

102 
theory. 

6744  103 
*}; 
6505  104 

7982  105 
theorem "EX S. S ~: range (f :: 'a => 'a set)"; 
9474  106 
by best; 
6494  107 

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

111 
transform internal systemlevel representations of Isabelle proofs 

7982  112 
back into Isar text. Writing intelligible proof documents 
7874  113 
really is a creative process, after all. 
6744  114 
*}; 
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

115 

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

116 
end; 