author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 37671  fa53d267dab3 
child 55640  abc140f21caa 
permissions  rwrr 
33026  1 
(* Title: HOL/Isar_Examples/Cantor.thy 
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

2 
Author: Markus Wenzel, TU Muenchen 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

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

4 

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

6 

31758  7 
theory Cantor 
8 
imports Main 

9 
begin 

7955  10 

37671  11 
text_raw {* \footnote{This is an Isar version of the final example of 
12 
the Isabelle/HOL manual \cite{isabelleHOL}.} *} 

7819  13 

37671  14 
text {* Cantor's Theorem states that every set has more subsets than 
15 
it has elements. It has become a favorite basic example in pure 

12388  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\] 

19 

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

21 
powerset of $\alpha$. This version of the theorem states that for 

22 
every function from $\alpha$ to its powerset, some subset is outside 

23 
its range. The Isabelle/Isar proofs below uses HOL's set theory, 

24 
with the type $\alpha \ap \idt{set}$ and the operator 

37671  25 
$\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$. *} 
6505  26 

10007  27 
theorem "EX S. S ~: range (f :: 'a => 'a set)" 
28 
proof 

29 
let ?S = "{x. x ~: f x}" 

30 
show "?S ~: range f" 

31 
proof 

32 
assume "?S : range f" 

12388  33 
then obtain y where "?S = f y" .. 
23373  34 
then show False 
12388  35 
proof (rule equalityCE) 
36 
assume "y : f y" 

23373  37 
assume "y : ?S" then have "y ~: f y" .. 
38 
with `y : f y` show ?thesis by contradiction 

12388  39 
next 
40 
assume "y ~: ?S" 

23373  41 
assume "y ~: f y" then have "y : ?S" .. 
42 
with `y ~: ?S` show ?thesis by contradiction 

10007  43 
qed 
44 
qed 

45 
qed 

6494  46 

37671  47 
text {* How much creativity is required? As it happens, Isabelle can 
48 
prove this theorem automatically using bestfirst search. 

49 
Depthfirst search would diverge, but bestfirst search successfully 

50 
navigates through the large search space. The context of Isabelle's 

51 
classical prover contains rules for the relevant constructs of HOL's 

52 
set theory. *} 

6505  53 

10007  54 
theorem "EX S. S ~: range (f :: 'a => 'a set)" 
55 
by best 

6494  56 

37671  57 
text {* While this establishes the same theorem internally, we do not 
58 
get any idea of how the proof actually works. There is currently no 

59 
way to transform internal systemlevel representations of Isabelle 

12388  60 
proofs back into Isar text. Writing intelligible proof documents 
37671  61 
really is a creative process, after all. *} 
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

62 

10007  63 
end 