author  wenzelm 
Sat, 04 Sep 1999 21:13:01 +0200  
changeset 7480  0a0e0dbe1269 
parent 6746  cf6ad8d22793 
child 7748  5b9c45b21782 
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 

6505  5 
Cantor's theorem  Isar'ized version of the final section of the HOL 
6507  6 
chapter of "Isabelle's ObjectLogics" (Larry Paulson). 
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

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

8 

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

9 
theory Cantor = Main:; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

10 

6494  11 

6746  12 
section {* Example: Cantor's Theorem *}; 
6505  13 

6744  14 
text {* 
6505  15 
Cantor's Theorem states that every set has more subsets than it has 
16 
elements. It has become a favourite example in higherorder logic 

17 
since it is so easily expressed: @{display term[show_types] "ALL f 

18 
:: 'a => 'a => bool. EX S :: 'a => bool. ALL x::'a. f x ~= S"} 

19 

20 
Viewing types as sets, @{type "'a => bool"} represents the powerset 

21 
of @{type 'a}. This version states that for every function from 

22 
@{type 'a} to its powerset, some subset is outside its range. 

23 

24 
The Isabelle/Isar proofs below use HOL's set theory, with the type 

25 
@{type "'a set"} and the operator @{term range}. 

6744  26 
*}; 
6505  27 

6506  28 

6744  29 
text {* 
6505  30 
We first consider a rather verbose version of the proof, with the 
31 
reasoning expressed quite naively. We only make use of the pure 

32 
core of the Isar proof language. 

6744  33 
*}; 
6505  34 

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

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

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

43 
fix y; 

7480  44 
assume "?S = f y"; 
45 
then; show ?thesis; 

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

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

7480  55 
from y_notin_fy y_in_fy; show ?thesis; by contradiction; 
6494  56 
qed; 
57 
qed; 

58 
qed; 

59 
qed; 

60 

6506  61 

6744  62 
text {* 
6505  63 
The following version essentially does the same reasoning, only that 
64 
it is expressed more neatly, with some derived Isar language 

65 
elements involved. 

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 

92 

6744  93 
text {* 
6505  94 
How much creativity is required? As it happens, Isabelle can prove 
95 
this theorem automatically. The default classical set contains 

96 
rules for most of the constructs of HOL's set theory. We must 

97 
augment it with @{thm equalityCE} to break up set equalities, and 

98 
then apply bestfirst search. Depthfirst search would diverge, but 

99 
bestfirst search successfully navigates through the large search 

100 
space. 

6744  101 
*}; 
6505  102 

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

105 

6744  106 
text {* 
6505  107 
While this establishes the same theorem internally, we do not get 
6506  108 
any idea of how the proof actually works. There is currently no way 
109 
to transform internal systemlevel representations of Isabelle 

110 
proofs back into Isar documents. Writing Isabelle/Isar proof 

6507  111 
documents actually \emph{is} a creative process. 
6744  112 
*}; 
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

113 

6506  114 

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

115 
end; 