summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/ContNotDenum.thy

author | hoelzl |

Thu Dec 17 16:43:36 2015 +0100 (2015-12-17) | |

changeset 61880 | ff4d33058566 |

parent 61585 | a9599d3d7610 |

child 61975 | b4b11391c676 |

permissions | -rw-r--r-- |

moved some theorems from the CLT proof; reordered some theorems / notation

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 \<open>Non-denumerability of the Continuum.\<close>

8 theory ContNotDenum

9 imports Complex_Main Countable_Set

10 begin

12 subsection \<open>Abstract\<close>

14 text \<open>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 \<open>\<real>\<close> is not denumerable. In other

19 words, there does not exist a function \<open>f: \<nat> \<Rightarrow> \<real>\<close> 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 \<open>f: \<nat> \<Rightarrow> \<real>\<close> exists and find a real x such that x is not in the range of f

30 by generating a sequence of closed intervals then using the NIP.\<close>

32 theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)"

33 proof

34 assume "\<exists>f::nat \<Rightarrow> real. surj f"

35 then obtain f :: "nat \<Rightarrow> real" where "surj f" ..

37 txt \<open>First we construct a sequence of nested intervals, ignoring @{term "range f"}.\<close>

39 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})"

40 using assms

41 by (auto simp add: not_le cong: conj_cong)

42 (metis dense le_less_linear less_linear less_trans order_refl)

43 then obtain i j where ij:

44 "\<And>a b c::real. a < b \<Longrightarrow> i a b c < j a b c"

45 "\<And>a b c. a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}"

46 "\<And>a b c. a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}"

47 by metis

49 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)))"

50 def I \<equiv> "\<lambda>n. {fst (ivl n) .. snd (ivl n)}"

52 have ivl[simp]:

53 "ivl 0 = (f 0 + 1, f 0 + 2)"

54 "\<And>n. ivl (Suc n) = (i (fst (ivl n)) (snd (ivl n)) (f n), j (fst (ivl n)) (snd (ivl n)) (f n))"

55 unfolding ivl_def by simp_all

57 txt \<open>This is a decreasing sequence of non-empty intervals.\<close>

59 { fix n have "fst (ivl n) < snd (ivl n)"

60 by (induct n) (auto intro!: ij) }

61 note less = this

63 have "decseq I"

64 unfolding I_def decseq_Suc_iff ivl fst_conv snd_conv by (intro ij allI less)

66 txt \<open>Now we apply the finite intersection property of compact sets.\<close>

68 have "I 0 \<inter> (\<Inter>i. I i) \<noteq> {}"

69 proof (rule compact_imp_fip_image)

70 fix S :: "nat set" assume fin: "finite S"

71 have "{} \<subset> I (Max (insert 0 S))"

72 unfolding I_def using less[of "Max (insert 0 S)"] by auto

73 also have "I (Max (insert 0 S)) \<subseteq> (\<Inter>i\<in>insert 0 S. I i)"

74 using fin decseqD[OF \<open>decseq I\<close>, of _ "Max (insert 0 S)"] by (auto simp: Max_ge_iff)

75 also have "(\<Inter>i\<in>insert 0 S. I i) = I 0 \<inter> (\<Inter>i\<in>S. I i)"

76 by auto

77 finally show "I 0 \<inter> (\<Inter>i\<in>S. I i) \<noteq> {}"

78 by auto

79 qed (auto simp: I_def)

80 then obtain x where "\<And>n. x \<in> I n"

81 by blast

82 moreover from \<open>surj f\<close> obtain j where "x = f j"

83 by blast

84 ultimately have "f j \<in> I (Suc j)"

85 by blast

86 with ij(3)[OF less] show False

87 unfolding I_def ivl fst_conv snd_conv by auto

88 qed

90 lemma uncountable_UNIV_real: "uncountable (UNIV::real set)"

91 using real_non_denum unfolding uncountable_def by auto

93 lemma bij_betw_open_intervals:

94 fixes a b c d :: real

95 assumes "a < b" "c < d"

96 shows "\<exists>f. bij_betw f {a<..<b} {c<..<d}"

97 proof -

98 def f \<equiv> "\<lambda>a b c d x::real. (d - c)/(b - a) * (x - a) + c"

99 { fix a b c d x :: real assume *: "a < b" "c < d" "a < x" "x < b"

100 moreover from * have "(d - c) * (x - a) < (d - c) * (b - a)"

101 by (intro mult_strict_left_mono) simp_all

102 moreover from * have "0 < (d - c) * (x - a) / (b - a)"

103 by simp

104 ultimately have "f a b c d x < d" "c < f a b c d x"

105 by (simp_all add: f_def field_simps) }

106 with assms have "bij_betw (f a b c d) {a<..<b} {c<..<d}"

107 by (intro bij_betw_byWitness[where f'="f c d a b"]) (auto simp: f_def)

108 thus ?thesis by auto

109 qed

111 lemma bij_betw_tan: "bij_betw tan {-pi/2<..<pi/2} UNIV"

112 using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan arctan_tan)

114 lemma uncountable_open_interval:

115 fixes a b :: real

116 shows "uncountable {a<..<b} \<longleftrightarrow> a < b"

117 proof

118 assume "uncountable {a<..<b}"

119 then show "a < b"

120 using uncountable_def by force

121 next

122 assume "a < b"

123 show "uncountable {a<..<b}"

124 proof -

125 obtain f where "bij_betw f {a <..< b} {-pi/2<..<pi/2}"

126 using bij_betw_open_intervals[OF \<open>a < b\<close>, of "-pi/2" "pi/2"] by auto

127 then show ?thesis

128 by (metis bij_betw_tan uncountable_bij_betw uncountable_UNIV_real)

129 qed

130 qed

132 lemma uncountable_half_open_interval_1:

133 fixes a :: real shows "uncountable {a..<b} \<longleftrightarrow> a<b"

134 apply auto

135 using atLeastLessThan_empty_iff apply fastforce

136 using uncountable_open_interval [of a b]

137 by (metis countable_Un_iff ivl_disj_un_singleton(3))

139 lemma uncountable_half_open_interval_2:

140 fixes a :: real shows "uncountable {a<..b} \<longleftrightarrow> a<b"

141 apply auto

142 using atLeastLessThan_empty_iff apply fastforce

143 using uncountable_open_interval [of a b]

144 by (metis countable_Un_iff ivl_disj_un_singleton(4))

146 lemma real_interval_avoid_countable_set:

147 fixes a b :: real and A :: "real set"

148 assumes "a < b" and "countable A"

149 shows "\<exists>x\<in>{a<..<b}. x \<notin> A"

150 proof -

151 from `countable A` have "countable (A \<inter> {a<..<b})" by auto

152 moreover with `a < b` have "\<not> countable {a<..<b}"

153 by (simp add: uncountable_open_interval)

154 ultimately have "A \<inter> {a<..<b} \<noteq> {a<..<b}" by auto

155 hence "A \<inter> {a<..<b} \<subset> {a<..<b}"

156 by (intro psubsetI, auto)

157 hence "\<exists>x. x \<in> {a<..<b} - A \<inter> {a<..<b}"

158 by (rule psubset_imp_ex_mem)

159 thus ?thesis by auto

160 qed

162 end