author | wenzelm |
Wed, 06 Oct 1999 00:31:40 +0200 | |
changeset 7748 | 5b9c45b21782 |
parent 7480 | 0a0e0dbe1269 |
child 7800 | 8ee919e42174 |
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 |
|
6505 | 5 |
Cantor's theorem -- Isar'ized version of the final section of the HOL |
6507 | 6 |
chapter of "Isabelle's Object-Logics" (Larry Paulson). |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
7 |
*) |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
8 |
|
7748 | 9 |
header {* More classical proofs: Cantor's Theorem *}; |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order 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 |
7748 | 15 |
elements. It has become a favourite basic example in higher-order logic |
16 |
since it is so easily expressed: \[\all{f::\alpha \To \alpha \To \idt{bool}} |
|
17 |
\ex{S::\alpha \To \idt{bool}} \all{x::\alpha}. f \ap x \not= S\] |
|
18 |
||
19 |
Viewing types as sets, $\alpha \To \idt{bool}$ represents the powerset of |
|
20 |
$\alpha$. This version of the theorem states that for every function from |
|
21 |
$\alpha$ to its powerset, some subset is outside its range. The |
|
22 |
Isabelle/Isar proofs below use HOL's set theory, with the type $\alpha \ap |
|
23 |
\idt{set}$ and the operator $\idt{range}$. |
|
24 |
||
25 |
\bigskip We first consider a rather verbose version of the proof, with the |
|
26 |
reasoning expressed quite naively. We only make use of the pure core of the |
|
27 |
Isar proof language. |
|
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"; |
6494 | 36 |
then; show False; |
37 |
proof; |
|
38 |
fix y; |
|
7480 | 39 |
assume "?S = f y"; |
40 |
then; show ?thesis; |
|
6494 | 41 |
proof (rule equalityCE); |
7480 | 42 |
assume y_in_S: "y : ?S"; |
6494 | 43 |
assume y_in_fy: "y : f y"; |
44 |
from y_in_S; have y_notin_fy: "y ~: f y"; ..; |
|
7480 | 45 |
from y_notin_fy y_in_fy; show ?thesis; by contradiction; |
6494 | 46 |
next; |
7480 | 47 |
assume y_notin_S: "y ~: ?S"; |
6494 | 48 |
assume y_notin_fy: "y ~: f y"; |
49 |
from y_notin_S; have y_in_fy: "y : f y"; ..; |
|
7480 | 50 |
from y_notin_fy y_in_fy; show ?thesis; by contradiction; |
6494 | 51 |
qed; |
52 |
qed; |
|
53 |
qed; |
|
54 |
qed; |
|
55 |
||
6744 | 56 |
text {* |
7748 | 57 |
The following version of the proof essentially does the same reasoning, only |
58 |
that it is expressed more neatly, with some derived Isar language elements |
|
59 |
involved. |
|
6744 | 60 |
*}; |
6494 | 61 |
|
62 |
theorem "EX S. S ~: range(f :: 'a => 'a set)"; |
|
63 |
proof; |
|
7480 | 64 |
let ?S = "{x. x ~: f x}"; |
65 |
show "?S ~: range f"; |
|
6494 | 66 |
proof; |
7480 | 67 |
assume "?S : range f"; |
6505 | 68 |
thus False; |
6494 | 69 |
proof; |
70 |
fix y; |
|
7480 | 71 |
assume "?S = f y"; |
72 |
thus ?thesis; |
|
6494 | 73 |
proof (rule equalityCE); |
74 |
assume "y : f y"; |
|
7480 | 75 |
assume "y : ?S"; hence "y ~: f y"; ..; |
76 |
thus ?thesis; by contradiction; |
|
6494 | 77 |
next; |
78 |
assume "y ~: f y"; |
|
7480 | 79 |
assume "y ~: ?S"; hence "y : f y"; ..; |
80 |
thus ?thesis; by contradiction; |
|
6494 | 81 |
qed; |
82 |
qed; |
|
83 |
qed; |
|
84 |
qed; |
|
85 |
||
6744 | 86 |
text {* |
7748 | 87 |
How much creativity is required? As it happens, Isabelle can prove this |
88 |
theorem automatically. The default classical set contains rules for most of |
|
89 |
the constructs of HOL's set theory. We must augment it with |
|
90 |
\name{equalityCE} to break up set equalities, and then apply best-first |
|
91 |
search. Depth-first search would diverge, but best-first search |
|
92 |
successfully navigates through the large search space. |
|
6744 | 93 |
*}; |
6505 | 94 |
|
6494 | 95 |
theorem "EX S. S ~: range(f :: 'a => 'a set)"; |
96 |
by (best elim: equalityCE); |
|
97 |
||
6744 | 98 |
text {* |
7748 | 99 |
While this establishes the same theorem internally, we do not get any idea |
100 |
of how the proof actually works. There is currently no way to transform |
|
101 |
internal system-level representations of Isabelle proofs back into Isar |
|
102 |
documents. Note that writing Isabelle/Isar proof documents actually |
|
103 |
\emph{is} a creative process. |
|
6744 | 104 |
*}; |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
105 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
106 |
end; |