author  wenzelm 
Thu, 14 Oct 1999 16:02:39 +0200  
changeset 7869  c007f801cd59 
parent 7860  7819547df4d8 
child 7874  180364256231 
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 

7869  8 
theory Cantor = Main:;text_raw {* \footnote{This is an Isar version of 
7833  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 

7860  22 
its range. The Isabelle/Isar proofs below uses HOL's set theory, 
23 
with the type $\alpha \ap \idt{set}$ and the operator $\idt{range}$. 

7748  24 

7860  25 
\bigskip We first consider a slightly awkward version of the proof, 
26 
with the reasoning expressed quite naively. 

6744  27 
*}; 
6505  28 

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

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

6494  33 
proof; 
7480  34 
assume "?S : range f"; 
7860  35 
thus False; 
6494  36 
proof; 
37 
fix y; 

7480  38 
assume "?S = f y"; 
7860  39 
thus ?thesis; 
6494  40 
proof (rule equalityCE); 
7860  41 
assume in_S: "y : ?S"; 
42 
assume in_fy: "y : f y"; 

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

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

6494  45 
next; 
7860  46 
assume notin_S: "y ~: ?S"; 
47 
assume notin_fy: "y ~: f y"; 

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

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

6494  50 
qed; 
51 
qed; 

52 
qed; 

53 
qed; 

54 

6744  55 
text {* 
7819  56 
The following version of the proof essentially does the same 
7860  57 
reasoning, only that it is expressed more neatly. In particular, we 
58 
change the order of assumptions introduced in the two cases of rule 

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

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

61 
assumptions as introduced \isacommand{assume}, nor the order of goals 

62 
as solved by \isacommand{show} matters. The basic logical structure 

63 
has to be left intact, though. In particular, assumptions 

64 
``belonging'' to some goal have to be introduced \emph{before} its 

65 
corresponding \isacommand{show}.} 

6744  66 
*}; 
6494  67 

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

69 
proof; 

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

6494  72 
proof; 
7480  73 
assume "?S : range f"; 
6505  74 
thus False; 
6494  75 
proof; 
76 
fix y; 

7480  77 
assume "?S = f y"; 
78 
thus ?thesis; 

6494  79 
proof (rule equalityCE); 
80 
assume "y : f y"; 

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

6494  83 
next; 
84 
assume "y ~: f y"; 

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

6494  87 
qed; 
88 
qed; 

89 
qed; 

90 
qed; 

91 

6744  92 
text {* 
7819  93 
How much creativity is required? As it happens, Isabelle can prove 
7860  94 
this theorem automatically. The default context of the classical 
95 
proof tools contains rules for most of the constructs of HOL's set 

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

97 
equalities, and then apply bestfirst search. Depthfirst search 

98 
would diverge, but bestfirst search successfully navigates through 

99 
the large search space. 

6744  100 
*}; 
6505  101 

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

104 

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

108 
transform internal systemlevel representations of Isabelle proofs 

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

7860  110 
creative process, after all. 
6744  111 
*}; 
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

112 

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

113 
end; 