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

src/HOL/Library/ContNotDenum.thy

author | blanchet |

Wed Sep 24 15:45:55 2014 +0200 (2014-09-24) | |

changeset 58425 | 246985c6b20b |

parent 57234 | 596a499318ab |

child 58881 | b9556a055632 |

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

simpler proof

1 (* Title: HOL/Library/ContNonDenum.thy

2 Author: Benjamin Porter, Monash University, NICTA, 2005

3 Author: Johannes Hölzl, TU München

4 *)

6 header {* 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