1 (* Title: HOL/Isar_examples/Cantor.thy |
1 (* Title: HOL/Isar_examples/Cantor.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header {* Cantor's Theorem *}; |
6 header {* Cantor's Theorem *} |
7 |
7 |
8 theory Cantor = Main:; |
8 theory Cantor = Main: |
9 |
9 |
10 text_raw {* |
10 text_raw {* |
11 \footnote{This is an Isar version of the final example of the |
11 \footnote{This is an Isar version of the final example of the |
12 Isabelle/HOL manual \cite{isabelle-HOL}.} |
12 Isabelle/HOL manual \cite{isabelle-HOL}.} |
13 *}; |
13 *} |
14 |
14 |
15 text {* |
15 text {* |
16 Cantor's Theorem states that every set has more subsets than it has |
16 Cantor's Theorem states that every set has more subsets than it has |
17 elements. It has become a favorite basic example in pure |
17 elements. It has become a favorite basic example in pure |
18 higher-order logic since it is so easily expressed: \[\all{f::\alpha |
18 higher-order logic since it is so easily expressed: \[\all{f::\alpha |
26 with the type $\alpha \ap \idt{set}$ and the operator |
26 with the type $\alpha \ap \idt{set}$ and the operator |
27 $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$. |
27 $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$. |
28 |
28 |
29 \bigskip We first consider a slightly awkward version of the proof, |
29 \bigskip We first consider a slightly awkward version of the proof, |
30 with the innermost reasoning expressed quite naively. |
30 with the innermost reasoning expressed quite naively. |
31 *}; |
31 *} |
32 |
32 |
33 theorem "EX S. S ~: range (f :: 'a => 'a set)"; |
33 theorem "EX S. S ~: range (f :: 'a => 'a set)" |
34 proof; |
34 proof |
35 let ?S = "{x. x ~: f x}"; |
35 let ?S = "{x. x ~: f x}" |
36 show "?S ~: range f"; |
36 show "?S ~: range f" |
37 proof; |
37 proof |
38 assume "?S : range f"; |
38 assume "?S : range f" |
39 thus False; |
39 thus False |
40 proof; |
40 proof |
41 fix y; |
41 fix y |
42 assume "?S = f y"; |
42 assume "?S = f y" |
43 thus ?thesis; |
43 thus ?thesis |
44 proof (rule equalityCE); |
44 proof (rule equalityCE) |
45 assume in_S: "y : ?S"; |
45 assume in_S: "y : ?S" |
46 assume in_fy: "y : f y"; |
46 assume in_fy: "y : f y" |
47 from in_S; have notin_fy: "y ~: f y"; ..; |
47 from in_S have notin_fy: "y ~: f y" .. |
48 from notin_fy in_fy; show ?thesis; by contradiction; |
48 from notin_fy in_fy show ?thesis by contradiction |
49 next; |
49 next |
50 assume notin_S: "y ~: ?S"; |
50 assume notin_S: "y ~: ?S" |
51 assume notin_fy: "y ~: f y"; |
51 assume notin_fy: "y ~: f y" |
52 from notin_S; have in_fy: "y : f y"; ..; |
52 from notin_S have in_fy: "y : f y" .. |
53 from notin_fy in_fy; show ?thesis; by contradiction; |
53 from notin_fy in_fy show ?thesis by contradiction |
54 qed; |
54 qed |
55 qed; |
55 qed |
56 qed; |
56 qed |
57 qed; |
57 qed |
58 |
58 |
59 text {* |
59 text {* |
60 The following version of the proof essentially does the same |
60 The following version of the proof essentially does the same |
61 reasoning, only that it is expressed more neatly. In particular, we |
61 reasoning, only that it is expressed more neatly. In particular, we |
62 change the order of assumptions introduced in the two cases of rule |
62 change the order of assumptions introduced in the two cases of rule |
65 assumptions as introduced by \isacommand{assume}, nor the order of |
65 assumptions as introduced by \isacommand{assume}, nor the order of |
66 goals as solved by \isacommand{show} is of any significance. The |
66 goals as solved by \isacommand{show} is of any significance. The |
67 basic logical structure has to be left intact, though. In |
67 basic logical structure has to be left intact, though. In |
68 particular, assumptions ``belonging'' to some goal have to be |
68 particular, assumptions ``belonging'' to some goal have to be |
69 introduced \emph{before} its corresponding \isacommand{show}.} |
69 introduced \emph{before} its corresponding \isacommand{show}.} |
70 *}; |
70 *} |
71 |
71 |
72 theorem "EX S. S ~: range (f :: 'a => 'a set)"; |
72 theorem "EX S. S ~: range (f :: 'a => 'a set)" |
73 proof; |
73 proof |
74 let ?S = "{x. x ~: f x}"; |
74 let ?S = "{x. x ~: f x}" |
75 show "?S ~: range f"; |
75 show "?S ~: range f" |
76 proof; |
76 proof |
77 assume "?S : range f"; |
77 assume "?S : range f" |
78 thus False; |
78 thus False |
79 proof; |
79 proof |
80 fix y; |
80 fix y |
81 assume "?S = f y"; |
81 assume "?S = f y" |
82 thus ?thesis; |
82 thus ?thesis |
83 proof (rule equalityCE); |
83 proof (rule equalityCE) |
84 assume "y : f y"; |
84 assume "y : f y" |
85 assume "y : ?S"; hence "y ~: f y"; ..; |
85 assume "y : ?S" hence "y ~: f y" .. |
86 thus ?thesis; by contradiction; |
86 thus ?thesis by contradiction |
87 next; |
87 next |
88 assume "y ~: f y"; |
88 assume "y ~: f y" |
89 assume "y ~: ?S"; hence "y : f y"; ..; |
89 assume "y ~: ?S" hence "y : f y" .. |
90 thus ?thesis; by contradiction; |
90 thus ?thesis by contradiction |
91 qed; |
91 qed |
92 qed; |
92 qed |
93 qed; |
93 qed |
94 qed; |
94 qed |
95 |
95 |
96 text {* |
96 text {* |
97 How much creativity is required? As it happens, Isabelle can prove |
97 How much creativity is required? As it happens, Isabelle can prove |
98 this theorem automatically using best-first search. Depth-first |
98 this theorem automatically using best-first search. Depth-first |
99 search would diverge, but best-first search successfully navigates |
99 search would diverge, but best-first search successfully navigates |
100 through the large search space. The context of Isabelle's classical |
100 through the large search space. The context of Isabelle's classical |
101 prover contains rules for the relevant constructs of HOL's set |
101 prover contains rules for the relevant constructs of HOL's set |
102 theory. |
102 theory. |
103 *}; |
103 *} |
104 |
104 |
105 theorem "EX S. S ~: range (f :: 'a => 'a set)"; |
105 theorem "EX S. S ~: range (f :: 'a => 'a set)" |
106 by best; |
106 by best |
107 |
107 |
108 text {* |
108 text {* |
109 While this establishes the same theorem internally, we do not get any |
109 While this establishes the same theorem internally, we do not get any |
110 idea of how the proof actually works. There is currently no way to |
110 idea of how the proof actually works. There is currently no way to |
111 transform internal system-level representations of Isabelle proofs |
111 transform internal system-level representations of Isabelle proofs |
112 back into Isar text. Writing intelligible proof documents |
112 back into Isar text. Writing intelligible proof documents |
113 really is a creative process, after all. |
113 really is a creative process, after all. |
114 *}; |
114 *} |
115 |
115 |
116 end; |
116 end |