author  wenzelm 
Fri, 08 Oct 1999 15:09:14 +0200  
changeset 7800  8ee919e42174 
parent 7748  5b9c45b21782 
child 7819  6dd018b6cf3f 
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 

7800  9 
header {* Cantor's Theorem *}; 
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

10 

7748  11 
theory Cantor = Main:; 
6505  12 

6744  13 
text {* 
6505  14 
Cantor's Theorem states that every set has more subsets than it has 
7800  15 
elements. It has become a favorite basic example in pure 
16 
higherorder logic since it is so easily expressed: \[\all{f::\alpha 

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

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

7748  19 

20 
Viewing types as sets, $\alpha \To \idt{bool}$ represents the powerset of 

21 
$\alpha$. This version of the theorem states that for every function from 

22 
$\alpha$ to its powerset, some subset is outside its range. The 

23 
Isabelle/Isar proofs below use HOL's set theory, with the type $\alpha \ap 

24 
\idt{set}$ and the operator $\idt{range}$. 

25 

26 
\bigskip We first consider a rather verbose version of the proof, with the 

27 
reasoning expressed quite naively. We only make use of the pure core of the 

28 
Isar proof language. 

6744  29 
*}; 
6505  30 

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

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

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

39 
fix y; 

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

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

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

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

54 
qed; 

55 
qed; 

56 

6744  57 
text {* 
7748  58 
The following version of the proof essentially does the same reasoning, only 
59 
that it is expressed more neatly, with some derived Isar language elements 

60 
involved. 

6744  61 
*}; 
6494  62 

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

64 
proof; 

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

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

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

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

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

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

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

6494  82 
qed; 
83 
qed; 

84 
qed; 

85 
qed; 

86 

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

90 
the constructs of HOL's set theory. We must augment it with 

91 
\name{equalityCE} to break up set equalities, and then apply bestfirst 

92 
search. Depthfirst search would diverge, but bestfirst search 

93 
successfully navigates through the large search space. 

6744  94 
*}; 
6505  95 

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

98 

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

102 
internal systemlevel representations of Isabelle proofs back into Isar 

103 
documents. Note that writing Isabelle/Isar proof documents actually 

104 
\emph{is} a creative process. 

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

106 

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

107 
end; 