author  wenzelm 
Wed, 27 Oct 1999 18:11:54 +0200  
changeset 7955  f30e08579481 
parent 7874  180364256231 
child 7982  d534b897ce39 
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 

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"; 
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 

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

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 
7874  98 
this theorem automatically. The default context of the Isabelle's 
99 
classical prover contains rules for most of the constructs of HOL's 

100 
set theory. We must augment it with \name{equalityCE} to break up 

101 
set equalities, and then apply bestfirst search. Depthfirst search 

7860  102 
would diverge, but bestfirst search successfully navigates through 
103 
the large search space. 

6744  104 
*}; 
6505  105 

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

108 

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

112 
transform internal systemlevel representations of Isabelle proofs 

7874  113 
back into Isar documents. Writing intelligible proof documents 
114 
really is a creative process, after all. 

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

116 

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

117 
end; 