author | wenzelm |
Sat, 14 Jan 2012 12:36:43 +0100 | |
changeset 46204 | df1369a42393 |
parent 37671 | fa53d267dab3 |
child 55640 | abc140f21caa |
permissions | -rw-r--r-- |
33026 | 1 |
(* Title: HOL/Isar_Examples/Cantor.thy |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
2 |
Author: Markus Wenzel, TU Muenchen |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
3 |
*) |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
4 |
|
10007 | 5 |
header {* Cantor's Theorem *} |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order 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{isabelle-HOL}.} *} |
|
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 |
higher-order 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 best-first search. |
|
49 |
Depth-first search would diverge, but best-first 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 system-level 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 Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
62 |
|
10007 | 63 |
end |