src/HOL/Library/ContNotDenum.thy
 author paulson Mon Feb 22 14:37:56 2016 +0000 (2016-02-22) changeset 62379 340738057c8c parent 62083 7582b39f51ed child 63040 eb4ddd18d635 permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
     1 (*  Title:      HOL/Library/ContNotDenum.thy

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

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

     4 *)

     5

     6 section \<open>Non-denumerability of the Continuum.\<close>

     7

     8 theory ContNotDenum

     9 imports Complex_Main Countable_Set

    10 begin

    11

    12 subsection \<open>Abstract\<close>

    13

    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.

    17

    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.

    21

    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>

    31

    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" ..

    36

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

    38

    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

    48

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

    51

    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

    56

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

    58

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

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

    61   note less = this

    62

    63   have "decseq I"

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

    65

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

    67

    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

    89

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

    91   using real_non_denum unfolding uncountable_def by auto

    92

    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

   110

   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)

   113

   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

   131

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

   138

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

   145

   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 \<open>countable A\<close> have "countable (A \<inter> {a<..<b})" by auto

   152   moreover with \<open>a < b\<close> 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

   161

   162 lemma open_minus_countable:

   163   fixes S A :: "real set" assumes "countable A" "S \<noteq> {}" "open S"

   164   shows "\<exists>x\<in>S. x \<notin> A"

   165 proof -

   166   obtain x where "x \<in> S"

   167     using \<open>S \<noteq> {}\<close> by auto

   168   then obtain e where "0 < e" "{y. dist y x < e} \<subseteq> S"

   169     using \<open>open S\<close> by (auto simp: open_dist subset_eq)

   170   moreover have "{y. dist y x < e} = {x - e <..< x + e}"

   171     by (auto simp: dist_real_def)

   172   ultimately have "uncountable (S - A)"

   173     using uncountable_open_interval[of "x - e" "x + e"] \<open>countable A\<close>

   174     by (intro uncountable_minus_countable) (auto dest: countable_subset)

   175   then show ?thesis

   176     unfolding uncountable_def by auto

   177 qed

   178

   179 end