author | wenzelm |
Tue, 19 Jul 2016 09:55:03 +0200 | |
changeset 63520 | 2803d2b8f85d |
parent 63465 | d7610beb98bc |
child 63540 | f8652d0534fa |
permissions | -rw-r--r-- |
63464 | 1 |
(* Title: HOL/Library/Continuum_Not_Denumerable.thy |
56796 | 2 |
Author: Benjamin Porter, Monash University, NICTA, 2005 |
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
3 |
Author: Johannes Hölzl, TU München |
23461 | 4 |
*) |
5 |
||
60500 | 6 |
section \<open>Non-denumerability of the Continuum.\<close> |
23461 | 7 |
|
63464 | 8 |
theory Continuum_Not_Denumerable |
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
9 |
imports Complex_Main Countable_Set |
23461 | 10 |
begin |
11 |
||
60500 | 12 |
subsection \<open>Abstract\<close> |
23461 | 13 |
|
63465 | 14 |
text \<open> |
15 |
The following document presents a proof that the Continuum is uncountable. |
|
16 |
It is formalised in the Isabelle/Isar theorem proving system. |
|
23461 | 17 |
|
63465 | 18 |
\<^bold>\<open>Theorem:\<close> The Continuum \<open>\<real>\<close> is not denumerable. In other words, there does |
19 |
not exist a function \<open>f: \<nat> \<Rightarrow> \<real>\<close> such that f is surjective. |
|
20 |
||
21 |
\<^bold>\<open>Outline:\<close> An elegant informal proof of this result uses Cantor's |
|
22 |
Diagonalisation argument. The proof presented here is not this one. |
|
23461 | 23 |
|
63465 | 24 |
First we formalise some properties of closed intervals, then we prove the |
25 |
Nested Interval Property. This property relies on the completeness of the |
|
26 |
Real numbers and is the foundation for our argument. Informally it states |
|
27 |
that an intersection of countable closed intervals (where each successive |
|
28 |
interval is a subset of the last) is non-empty. We then assume a surjective |
|
29 |
function \<open>f: \<nat> \<Rightarrow> \<real>\<close> exists and find a real \<open>x\<close> such that \<open>x\<close> is not in the |
|
30 |
range of \<open>f\<close> by generating a sequence of closed intervals then using the |
|
31 |
NIP. |
|
32 |
\<close> |
|
23461 | 33 |
|
63465 | 34 |
theorem real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f" |
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
35 |
proof |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
36 |
assume "\<exists>f::nat \<Rightarrow> real. surj f" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
37 |
then obtain f :: "nat \<Rightarrow> real" where "surj f" .. |
56796 | 38 |
|
60500 | 39 |
txt \<open>First we construct a sequence of nested intervals, ignoring @{term "range f"}.\<close> |
23461 | 40 |
|
63465 | 41 |
have "a < b \<Longrightarrow> \<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb}" for a b c :: real |
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
42 |
by (auto simp add: not_le cong: conj_cong) |
63465 | 43 |
(metis dense le_less_linear less_linear less_trans order_refl) |
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
44 |
then obtain i j where ij: |
63465 | 45 |
"a < b \<Longrightarrow> i a b c < j a b c" |
63060 | 46 |
"a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}" |
47 |
"a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}" |
|
48 |
for a b c :: real |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
49 |
by metis |
23461 | 50 |
|
63040 | 51 |
define ivl where "ivl = |
52 |
rec_nat (f 0 + 1, f 0 + 2) (\<lambda>n x. (i (fst x) (snd x) (f n), j (fst x) (snd x) (f n)))" |
|
53 |
define I where "I n = {fst (ivl n) .. snd (ivl n)}" for n |
|
23461 | 54 |
|
63465 | 55 |
have ivl [simp]: |
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
56 |
"ivl 0 = (f 0 + 1, f 0 + 2)" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
57 |
"\<And>n. ivl (Suc n) = (i (fst (ivl n)) (snd (ivl n)) (f n), j (fst (ivl n)) (snd (ivl n)) (f n))" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
58 |
unfolding ivl_def by simp_all |
56796 | 59 |
|
60500 | 60 |
txt \<open>This is a decreasing sequence of non-empty intervals.\<close> |
23461 | 61 |
|
63465 | 62 |
have less: "fst (ivl n) < snd (ivl n)" for n |
63 |
by (induct n) (auto intro!: ij) |
|
23461 | 64 |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
65 |
have "decseq I" |
63465 | 66 |
unfolding I_def decseq_Suc_iff ivl fst_conv snd_conv |
67 |
by (intro ij allI less) |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
68 |
|
60500 | 69 |
txt \<open>Now we apply the finite intersection property of compact sets.\<close> |
23461 | 70 |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
71 |
have "I 0 \<inter> (\<Inter>i. I i) \<noteq> {}" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
72 |
proof (rule compact_imp_fip_image) |
63465 | 73 |
fix S :: "nat set" |
74 |
assume fin: "finite S" |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
75 |
have "{} \<subset> I (Max (insert 0 S))" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
76 |
unfolding I_def using less[of "Max (insert 0 S)"] by auto |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
77 |
also have "I (Max (insert 0 S)) \<subseteq> (\<Inter>i\<in>insert 0 S. I i)" |
63465 | 78 |
using fin decseqD[OF \<open>decseq I\<close>, of _ "Max (insert 0 S)"] |
79 |
by (auto simp: Max_ge_iff) |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
80 |
also have "(\<Inter>i\<in>insert 0 S. I i) = I 0 \<inter> (\<Inter>i\<in>S. I i)" |
56796 | 81 |
by auto |
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
82 |
finally show "I 0 \<inter> (\<Inter>i\<in>S. I i) \<noteq> {}" |
53372 | 83 |
by auto |
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
84 |
qed (auto simp: I_def) |
63060 | 85 |
then obtain x where "x \<in> I n" for n |
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
86 |
by blast |
60500 | 87 |
moreover from \<open>surj f\<close> obtain j where "x = f j" |
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
88 |
by blast |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
89 |
ultimately have "f j \<in> I (Suc j)" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
90 |
by blast |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
91 |
with ij(3)[OF less] show False |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
92 |
unfolding I_def ivl fst_conv snd_conv by auto |
23461 | 93 |
qed |
94 |
||
63465 | 95 |
lemma uncountable_UNIV_real: "uncountable (UNIV :: real set)" |
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
96 |
using real_non_denum unfolding uncountable_def by auto |
23461 | 97 |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
98 |
lemma bij_betw_open_intervals: |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
99 |
fixes a b c d :: real |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
100 |
assumes "a < b" "c < d" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
101 |
shows "\<exists>f. bij_betw f {a<..<b} {c<..<d}" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
102 |
proof - |
63040 | 103 |
define f where "f a b c d x = (d - c)/(b - a) * (x - a) + c" for a b c d x :: real |
63465 | 104 |
{ |
105 |
fix a b c d x :: real |
|
106 |
assume *: "a < b" "c < d" "a < x" "x < b" |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
107 |
moreover from * have "(d - c) * (x - a) < (d - c) * (b - a)" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
108 |
by (intro mult_strict_left_mono) simp_all |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
109 |
moreover from * have "0 < (d - c) * (x - a) / (b - a)" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
110 |
by simp |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
111 |
ultimately have "f a b c d x < d" "c < f a b c d x" |
63465 | 112 |
by (simp_all add: f_def field_simps) |
113 |
} |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
114 |
with assms have "bij_betw (f a b c d) {a<..<b} {c<..<d}" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
115 |
by (intro bij_betw_byWitness[where f'="f c d a b"]) (auto simp: f_def) |
63465 | 116 |
then show ?thesis by auto |
23461 | 117 |
qed |
118 |
||
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
119 |
lemma bij_betw_tan: "bij_betw tan {-pi/2<..<pi/2} UNIV" |
59872
db4000b71fdb
Theorem "arctan" is no longer a default simprule
paulson <lp15@cam.ac.uk>
parents:
59720
diff
changeset
|
120 |
using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan arctan_tan) |
23461 | 121 |
|
63465 | 122 |
lemma uncountable_open_interval: "uncountable {a<..<b} \<longleftrightarrow> a < b" for a b :: real |
60308
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
123 |
proof |
63465 | 124 |
show "a < b" if "uncountable {a<..<b}" |
125 |
using uncountable_def that by force |
|
126 |
show "uncountable {a<..<b}" if "a < b" |
|
60308
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
127 |
proof - |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
128 |
obtain f where "bij_betw f {a <..< b} {-pi/2<..<pi/2}" |
60500 | 129 |
using bij_betw_open_intervals[OF \<open>a < b\<close>, of "-pi/2" "pi/2"] by auto |
60308
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
130 |
then show ?thesis |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
131 |
by (metis bij_betw_tan uncountable_bij_betw uncountable_UNIV_real) |
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
132 |
qed |
23461 | 133 |
qed |
134 |
||
63465 | 135 |
lemma uncountable_half_open_interval_1: "uncountable {a..<b} \<longleftrightarrow> a < b" for a b :: real |
60308
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
136 |
apply auto |
63465 | 137 |
using atLeastLessThan_empty_iff |
138 |
apply fastforce |
|
60308
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
139 |
using uncountable_open_interval [of a b] |
63465 | 140 |
apply (metis countable_Un_iff ivl_disj_un_singleton(3)) |
141 |
done |
|
60308
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
142 |
|
63465 | 143 |
lemma uncountable_half_open_interval_2: "uncountable {a<..b} \<longleftrightarrow> a < b" for a b :: real |
60308
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
144 |
apply auto |
63465 | 145 |
using atLeastLessThan_empty_iff |
146 |
apply fastforce |
|
60308
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
147 |
using uncountable_open_interval [of a b] |
63465 | 148 |
apply (metis countable_Un_iff ivl_disj_un_singleton(4)) |
149 |
done |
|
60308
f7e406aba90d
uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents:
59872
diff
changeset
|
150 |
|
61880
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61585
diff
changeset
|
151 |
lemma real_interval_avoid_countable_set: |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61585
diff
changeset
|
152 |
fixes a b :: real and A :: "real set" |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61585
diff
changeset
|
153 |
assumes "a < b" and "countable A" |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61585
diff
changeset
|
154 |
shows "\<exists>x\<in>{a<..<b}. x \<notin> A" |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61585
diff
changeset
|
155 |
proof - |
63465 | 156 |
from \<open>countable A\<close> have "countable (A \<inter> {a<..<b})" |
157 |
by auto |
|
158 |
moreover with \<open>a < b\<close> have "\<not> countable {a<..<b}" |
|
61880
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61585
diff
changeset
|
159 |
by (simp add: uncountable_open_interval) |
63465 | 160 |
ultimately have "A \<inter> {a<..<b} \<noteq> {a<..<b}" |
161 |
by auto |
|
162 |
then have "A \<inter> {a<..<b} \<subset> {a<..<b}" |
|
163 |
by (intro psubsetI) auto |
|
164 |
then have "\<exists>x. x \<in> {a<..<b} - A \<inter> {a<..<b}" |
|
61880
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61585
diff
changeset
|
165 |
by (rule psubset_imp_ex_mem) |
63465 | 166 |
then show ?thesis |
167 |
by auto |
|
61880
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61585
diff
changeset
|
168 |
qed |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61585
diff
changeset
|
169 |
|
62083 | 170 |
lemma open_minus_countable: |
63465 | 171 |
fixes S A :: "real set" |
172 |
assumes "countable A" "S \<noteq> {}" "open S" |
|
62083 | 173 |
shows "\<exists>x\<in>S. x \<notin> A" |
174 |
proof - |
|
175 |
obtain x where "x \<in> S" |
|
176 |
using \<open>S \<noteq> {}\<close> by auto |
|
177 |
then obtain e where "0 < e" "{y. dist y x < e} \<subseteq> S" |
|
178 |
using \<open>open S\<close> by (auto simp: open_dist subset_eq) |
|
179 |
moreover have "{y. dist y x < e} = {x - e <..< x + e}" |
|
180 |
by (auto simp: dist_real_def) |
|
181 |
ultimately have "uncountable (S - A)" |
|
182 |
using uncountable_open_interval[of "x - e" "x + e"] \<open>countable A\<close> |
|
183 |
by (intro uncountable_minus_countable) (auto dest: countable_subset) |
|
184 |
then show ?thesis |
|
185 |
unfolding uncountable_def by auto |
|
186 |
qed |
|
187 |
||
23461 | 188 |
end |