src/HOL/Library/ContNotDenum.thy
 author wenzelm Mon Mar 16 16:59:59 2015 +0100 (2015-03-16) changeset 59720 f893472fff31 parent 58881 b9556a055632 child 59872 db4000b71fdb permissions -rw-r--r--
1 (*  Title:      HOL/Library/ContNotDenum.thy
2     Author:     Benjamin Porter, Monash University, NICTA, 2005
3     Author:     Johannes Hölzl, TU München
4 *)
6 section {* Non-denumerability of the Continuum. *}
8 theory ContNotDenum
9 imports Complex_Main Countable_Set
10 begin
12 subsection {* Abstract *}
14 text {* The following document presents a proof that the Continuum is
15 uncountable. It is formalised in the Isabelle/Isar theorem proving
16 system.
18 {\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other
19 words, there does not exist a function @{text "f: \<nat> \<Rightarrow> \<real>"} such that f is
20 surjective.
22 {\em Outline:} An elegant informal proof of this result uses Cantor's
23 Diagonalisation argument. The proof presented here is not this
24 one. First we formalise some properties of closed intervals, then we
25 prove the Nested Interval Property. This property relies on the
26 completeness of the Real numbers and is the foundation for our
27 argument. Informally it states that an intersection of countable
28 closed intervals (where each successive interval is a subset of the
29 last) is non-empty. We then assume a surjective function @{text
30 "f: \<nat> \<Rightarrow> \<real>"} exists and find a real x such that x is not in the range of f
31 by generating a sequence of closed intervals then using the NIP. *}
33 theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)"
34 proof
35   assume "\<exists>f::nat \<Rightarrow> real. surj f"
36   then obtain f :: "nat \<Rightarrow> real" where "surj f" ..
38   txt {* First we construct a sequence of nested intervals, ignoring @{term "range f"}. *}
40   have "\<forall>a b c::real. a < b \<longrightarrow> (\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb})"
41     using assms
42     by (auto simp add: not_le cong: conj_cong)
43        (metis dense le_less_linear less_linear less_trans order_refl)
44   then obtain i j where ij:
45     "\<And>a b c::real. a < b \<Longrightarrow> i a b c < j a b c"
46     "\<And>a b c. a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}"
47     "\<And>a b c. a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}"
48     by metis
50   def ivl \<equiv> "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)))"
51   def I \<equiv> "\<lambda>n. {fst (ivl n) .. snd (ivl n)}"
53   have ivl[simp]:
54     "ivl 0 = (f 0 + 1, f 0 + 2)"
55     "\<And>n. ivl (Suc n) = (i (fst (ivl n)) (snd (ivl n)) (f n), j (fst (ivl n)) (snd (ivl n)) (f n))"
56     unfolding ivl_def by simp_all
58   txt {* This is a decreasing sequence of non-empty intervals. *}
60   { fix n have "fst (ivl n) < snd (ivl n)"
61       by (induct n) (auto intro!: ij) }
62   note less = this
64   have "decseq I"
65     unfolding I_def decseq_Suc_iff ivl fst_conv snd_conv by (intro ij allI less)
67   txt {* Now we apply the finite intersection property of compact sets. *}
69   have "I 0 \<inter> (\<Inter>i. I i) \<noteq> {}"
70   proof (rule compact_imp_fip_image)
71     fix S :: "nat set" assume fin: "finite S"
72     have "{} \<subset> I (Max (insert 0 S))"
73       unfolding I_def using less[of "Max (insert 0 S)"] by auto
74     also have "I (Max (insert 0 S)) \<subseteq> (\<Inter>i\<in>insert 0 S. I i)"
75       using fin decseqD[OF decseq I, of _ "Max (insert 0 S)"] by (auto simp: Max_ge_iff)
76     also have "(\<Inter>i\<in>insert 0 S. I i) = I 0 \<inter> (\<Inter>i\<in>S. I i)"
77       by auto
78     finally show "I 0 \<inter> (\<Inter>i\<in>S. I i) \<noteq> {}"
79       by auto
80   qed (auto simp: I_def)
81   then obtain x where "\<And>n. x \<in> I n"
82     by blast
83   moreover from surj f obtain j where "x = f j"
84     by blast
85   ultimately have "f j \<in> I (Suc j)"
86     by blast
87   with ij(3)[OF less] show False
88     unfolding I_def ivl fst_conv snd_conv by auto
89 qed
91 lemma uncountable_UNIV_real: "uncountable (UNIV::real set)"
92   using real_non_denum unfolding uncountable_def by auto
94 lemma bij_betw_open_intervals:
95   fixes a b c d :: real
96   assumes "a < b" "c < d"
97   shows "\<exists>f. bij_betw f {a<..<b} {c<..<d}"
98 proof -
99   def f \<equiv> "\<lambda>a b c d x::real. (d - c)/(b - a) * (x - a) + c"
100   { fix a b c d x :: real assume *: "a < b" "c < d" "a < x" "x < b"
101     moreover from * have "(d - c) * (x - a) < (d - c) * (b - a)"
102       by (intro mult_strict_left_mono) simp_all
103     moreover from * have "0 < (d - c) * (x - a) / (b - a)"
104       by simp
105     ultimately have "f a b c d x < d" "c < f a b c d x"
106       by (simp_all add: f_def field_simps) }
107   with assms have "bij_betw (f a b c d) {a<..<b} {c<..<d}"
108     by (intro bij_betw_byWitness[where f'="f c d a b"]) (auto simp: f_def)
109   thus ?thesis by auto
110 qed
112 lemma bij_betw_tan: "bij_betw tan {-pi/2<..<pi/2} UNIV"
113   using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan_tan)
115 lemma uncountable_open_interval:
116   fixes a b :: real assumes ab: "a < b"
117   shows "uncountable {a<..<b}"
118 proof -
119   obtain f where "bij_betw f {a <..< b} {-pi/2<..<pi/2}"
120     using bij_betw_open_intervals[OF a < b, of "-pi/2" "pi/2"] by auto
121   then show ?thesis
122     by (metis bij_betw_tan uncountable_bij_betw uncountable_UNIV_real)
123 qed
125 end