author | wenzelm |
Fri, 15 Oct 1999 16:44:37 +0200 | |
changeset 7874 | 180364256231 |
parent 7869 | c007f801cd59 |
child 7955 | f30e08579481 |
permissions | -rw-r--r-- |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Isar_examples/Cantor.thy |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel, TU Muenchen |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
4 |
*) |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
5 |
|
7800 | 6 |
header {* Cantor's Theorem *}; |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order 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{isabelle-HOL}.} |
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 |
higher-order logic since it is so easily expressed: \[\all{f::\alpha |
|
16 |
\To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}} |
|
7874 | 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, |
7874 | 23 |
with the type $\alpha \ap \idt{set}$ and the operator |
24 |
$\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$. |
|
7748 | 25 |
|
7860 | 26 |
\bigskip We first consider a slightly awkward version of the proof, |
7874 | 27 |
with the innermost reasoning expressed quite naively. |
6744 | 28 |
*}; |
6505 | 29 |
|
6494 | 30 |
theorem "EX S. S ~: range(f :: 'a => 'a set)"; |
31 |
proof; |
|
7480 | 32 |
let ?S = "{x. x ~: f x}"; |
33 |
show "?S ~: range f"; |
|
6494 | 34 |
proof; |
7480 | 35 |
assume "?S : range f"; |
7860 | 36 |
thus False; |
6494 | 37 |
proof; |
38 |
fix y; |
|
7480 | 39 |
assume "?S = f y"; |
7860 | 40 |
thus ?thesis; |
6494 | 41 |
proof (rule equalityCE); |
7860 | 42 |
assume in_S: "y : ?S"; |
43 |
assume in_fy: "y : f y"; |
|
44 |
from in_S; have notin_fy: "y ~: f y"; ..; |
|
45 |
from notin_fy in_fy; show ?thesis; by contradiction; |
|
6494 | 46 |
next; |
7860 | 47 |
assume notin_S: "y ~: ?S"; |
48 |
assume notin_fy: "y ~: f y"; |
|
49 |
from notin_S; have in_fy: "y : f y"; ..; |
|
50 |
from notin_fy in_fy; show ?thesis; by contradiction; |
|
6494 | 51 |
qed; |
52 |
qed; |
|
53 |
qed; |
|
54 |
qed; |
|
55 |
||
6744 | 56 |
text {* |
7819 | 57 |
The following version of the proof essentially does the same |
7860 | 58 |
reasoning, only that it is expressed more neatly. In particular, we |
59 |
change the order of assumptions introduced in the two cases of rule |
|
60 |
\name{equalityCE}, streamlining the flow of intermediate facts and |
|
61 |
avoiding explicit naming.\footnote{In general, neither the order of |
|
7874 | 62 |
assumptions as introduced by \isacommand{assume}, nor the order of |
63 |
goals as solved by \isacommand{show} is of any significance. The |
|
64 |
basic logical structure has to be left intact, though. In |
|
65 |
particular, assumptions ``belonging'' to some goal have to be |
|
66 |
introduced \emph{before} its corresponding \isacommand{show}.} |
|
6744 | 67 |
*}; |
6494 | 68 |
|
69 |
theorem "EX S. S ~: range(f :: 'a => 'a set)"; |
|
70 |
proof; |
|
7480 | 71 |
let ?S = "{x. x ~: f x}"; |
72 |
show "?S ~: range f"; |
|
6494 | 73 |
proof; |
7480 | 74 |
assume "?S : range f"; |
6505 | 75 |
thus False; |
6494 | 76 |
proof; |
77 |
fix y; |
|
7480 | 78 |
assume "?S = f y"; |
79 |
thus ?thesis; |
|
6494 | 80 |
proof (rule equalityCE); |
81 |
assume "y : f y"; |
|
7480 | 82 |
assume "y : ?S"; hence "y ~: f y"; ..; |
83 |
thus ?thesis; by contradiction; |
|
6494 | 84 |
next; |
85 |
assume "y ~: f y"; |
|
7480 | 86 |
assume "y ~: ?S"; hence "y : f y"; ..; |
87 |
thus ?thesis; by contradiction; |
|
6494 | 88 |
qed; |
89 |
qed; |
|
90 |
qed; |
|
91 |
qed; |
|
92 |
||
6744 | 93 |
text {* |
7819 | 94 |
How much creativity is required? As it happens, Isabelle can prove |
7874 | 95 |
this theorem automatically. The default context of the Isabelle's |
96 |
classical prover contains rules for most of the constructs of HOL's |
|
97 |
set theory. We must augment it with \name{equalityCE} to break up |
|
98 |
set equalities, and then apply best-first search. Depth-first search |
|
7860 | 99 |
would diverge, but best-first search successfully navigates through |
100 |
the large search 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 {* |
7819 | 107 |
While this establishes the same theorem internally, we do not get any |
108 |
idea of how the proof actually works. There is currently no way to |
|
109 |
transform internal system-level representations of Isabelle proofs |
|
7874 | 110 |
back into Isar documents. Writing intelligible proof documents |
111 |
really is a creative process, after all. |
|
6744 | 112 |
*}; |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
113 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
114 |
end; |