src/HOL/Library/ContNotDenum.thy
author hoelzl
Wed Dec 18 11:53:40 2013 +0100 (2013-12-18)
changeset 54797 be020ec8560c
parent 54263 c4159fe6fa46
child 56796 9f84219715a7
permissions -rw-r--r--
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
     1 (*  Title       : HOL/ContNonDenum
     2     Author      : Benjamin Porter, Monash University, NICTA, 2005
     3 *)
     4 
     5 header {* Non-denumerability of the Continuum. *}
     6 
     7 theory ContNotDenum
     8 imports Complex_Main
     9 begin
    10 
    11 subsection {* Abstract *}
    12 
    13 text {* The following document presents a proof that the Continuum is
    14 uncountable. It is formalised in the Isabelle/Isar theorem proving
    15 system.
    16 
    17 {\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other
    18 words, there does not exist a function f:@{text "\<nat>\<Rightarrow>\<real>"} such that f is
    19 surjective.
    20 
    21 {\em Outline:} An elegant informal proof of this result uses Cantor's
    22 Diagonalisation argument. The proof presented here is not this
    23 one. First we formalise some properties of closed intervals, then we
    24 prove the Nested Interval Property. This property relies on the
    25 completeness of the Real numbers and is the foundation for our
    26 argument. Informally it states that an intersection of countable
    27 closed intervals (where each successive interval is a subset of the
    28 last) is non-empty. We then assume a surjective function f:@{text
    29 "\<nat>\<Rightarrow>\<real>"} 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. *}
    31 
    32 subsection {* Closed Intervals *}
    33 
    34 subsection {* Nested Interval Property *}
    35 
    36 theorem NIP:
    37   fixes f::"nat \<Rightarrow> real set"
    38   assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
    39   and closed: "\<forall>n. \<exists>a b. f n = {a..b} \<and> a \<le> b"
    40   shows "(\<Inter>n. f n) \<noteq> {}"
    41 proof -
    42   let ?I = "\<lambda>n. {Inf (f n) .. Sup (f n)}"
    43   { fix n 
    44     from closed[rule_format, of n] obtain a b where "f n = {a .. b}" "a \<le> b"
    45       by auto
    46     then have "f n = {Inf (f n) .. Sup (f n)}" and "Inf (f n) \<le> Sup (f n)"
    47       by auto }
    48   note f_eq = this
    49   { fix n m :: nat assume "n \<le> m" then have "f m \<subseteq> f n"
    50       by (induct rule: dec_induct) (metis order_refl, metis order_trans subset) }
    51   note subset' = this
    52 
    53   have "compact (f 0)"
    54     by (subst f_eq) (rule compact_Icc)
    55   then have "f 0 \<inter> (\<Inter>i. f i) \<noteq> {}"
    56   proof (rule compact_imp_fip_image)
    57     fix I :: "nat set" assume I: "finite I"
    58     have "{} \<subset> f (Max (insert 0 I))"
    59       using f_eq[of "Max (insert 0 I)"] by auto
    60     also have "\<dots> \<subseteq> (\<Inter>i\<in>insert 0 I. f i)"
    61     proof (rule INF_greatest)
    62       fix i assume "i \<in> insert 0 I"
    63       with I show "f (Max (insert 0 I)) \<subseteq> f i"
    64         by (intro subset') auto
    65     qed
    66     finally show "f 0 \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
    67       by auto
    68   qed (subst f_eq, auto)
    69   then show "(\<Inter>n. f n) \<noteq> {}"
    70     by auto
    71 qed
    72 
    73 subsection {* Generating the intervals *}
    74 
    75 subsubsection {* Existence of non-singleton closed intervals *}
    76 
    77 text {* This lemma asserts that given any non-singleton closed
    78 interval (a,b) and any element c, there exists a closed interval that
    79 is a subset of (a,b) and that does not contain c and is a
    80 non-singleton itself. *}
    81 
    82 lemma closed_subset_ex:
    83   fixes c::real
    84   assumes "a < b"
    85   shows "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb}"
    86 proof (cases "c < b")
    87   case True
    88   show ?thesis
    89   proof (cases "c < a")
    90     case True
    91     with `a < b` `c < b` have "c \<notin> {a..b}"
    92       by auto
    93     with `a < b` show ?thesis by auto
    94   next
    95     case False
    96     then have "a \<le> c" by simp
    97     def ka \<equiv> "(c + b)/2"
    98 
    99     from ka_def `c < b` have kalb: "ka < b" by auto
   100     moreover from ka_def `c < b` have kagc: "ka > c" by simp
   101     ultimately have "c\<notin>{ka..b}" by auto
   102     moreover from `a \<le> c` kagc have "ka \<ge> a" by simp
   103     hence "{ka..b} \<subseteq> {a..b}" by auto
   104     ultimately have
   105       "ka < b  \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}"
   106       using kalb by auto
   107     then show ?thesis
   108       by auto
   109   qed
   110 next
   111   case False
   112   then have "c \<ge> b" by simp
   113 
   114   def kb \<equiv> "(a + b)/2"
   115   with `a < b` have "kb < b" by auto
   116   with kb_def `c \<ge> b` have "a < kb" "kb < c" by auto
   117   from `kb < c` have c: "c \<notin> {a..kb}"
   118     by auto
   119   with `kb < b` have "{a..kb} \<subseteq> {a..b}"
   120     by auto
   121   with `a < kb` c have "a < kb \<and> {a..kb} \<subseteq> {a..b} \<and> c \<notin> {a..kb}"
   122     by simp
   123   then show ?thesis by auto
   124 qed
   125 
   126 subsection {* newInt: Interval generation *}
   127 
   128 text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
   129 closed interval such that @{text "newInt (Suc n) f \<subseteq> newInt n f"} and
   130 does not contain @{text "f (Suc n)"}. With the base case defined such
   131 that @{text "(f 0)\<notin>newInt 0 f"}. *}
   132 
   133 subsubsection {* Definition *}
   134 
   135 primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
   136   "newInt 0 f = {f 0 + 1..f 0 + 2}"
   137   | "newInt (Suc n) f =
   138       (SOME e. (\<exists>e1 e2.
   139        e1 < e2 \<and>
   140        e = {e1..e2} \<and>
   141        e \<subseteq> newInt n f \<and>
   142        f (Suc n) \<notin> e)
   143       )"
   144 
   145 
   146 subsubsection {* Properties *}
   147 
   148 text {* We now show that every application of newInt returns an
   149 appropriate interval. *}
   150 
   151 lemma newInt_ex:
   152   "\<exists>a b. a < b \<and>
   153    newInt (Suc n) f = {a..b} \<and>
   154    newInt (Suc n) f \<subseteq> newInt n f \<and>
   155    f (Suc n) \<notin> newInt (Suc n) f"
   156 proof (induct n)
   157   case 0
   158 
   159   let ?e = "SOME e. \<exists>e1 e2.
   160    e1 < e2 \<and>
   161    e = {e1..e2} \<and>
   162    e \<subseteq> {f 0 + 1..f 0 + 2} \<and>
   163    f (Suc 0) \<notin> e"
   164 
   165   have "newInt (Suc 0) f = ?e" by auto
   166   moreover
   167   have "f 0 + 1 < f 0 + 2" by simp
   168   with closed_subset_ex have
   169     "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {f 0 + 1..f 0 + 2} \<and>
   170      f (Suc 0) \<notin> {ka..kb}" .
   171   hence
   172     "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
   173      e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> e" by simp
   174   hence
   175     "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> ?e"
   176     by (rule someI_ex)
   177   ultimately have "\<exists>e1 e2. e1 < e2 \<and>
   178    newInt (Suc 0) f = {e1..e2} \<and>
   179    newInt (Suc 0) f \<subseteq> {f 0 + 1..f 0 + 2} \<and>
   180    f (Suc 0) \<notin> newInt (Suc 0) f" by simp
   181   thus
   182     "\<exists>a b. a < b \<and> newInt (Suc 0) f = {a..b} \<and>
   183      newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
   184     by simp
   185 next
   186   case (Suc n)
   187   hence "\<exists>a b.
   188    a < b \<and>
   189    newInt (Suc n) f = {a..b} \<and>
   190    newInt (Suc n) f \<subseteq> newInt n f \<and>
   191    f (Suc n) \<notin> newInt (Suc n) f" by simp
   192   then obtain a and b where ab: "a < b \<and>
   193    newInt (Suc n) f = {a..b} \<and>
   194    newInt (Suc n) f \<subseteq> newInt n f \<and>
   195    f (Suc n) \<notin> newInt (Suc n) f" by auto
   196   hence cab: "{a..b} = newInt (Suc n) f" by simp
   197 
   198   let ?e = "SOME e. \<exists>e1 e2.
   199     e1 < e2 \<and>
   200     e = {e1..e2} \<and>
   201     e \<subseteq> {a..b} \<and>
   202     f (Suc (Suc n)) \<notin> e"
   203   from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto
   204 
   205   from ab have "a < b" by simp
   206   with closed_subset_ex have
   207     "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and>
   208      f (Suc (Suc n)) \<notin> {ka..kb}" .
   209   hence
   210     "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
   211      {ka..kb} \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> {ka..kb}"
   212     by simp
   213   hence
   214     "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
   215      e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> e" by simp
   216   hence
   217     "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and>
   218      ?e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
   219   with ab ni show
   220     "\<exists>ka kb. ka < kb \<and>
   221      newInt (Suc (Suc n)) f = {ka..kb} \<and>
   222      newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
   223      f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto
   224 qed
   225 
   226 lemma newInt_subset:
   227   "newInt (Suc n) f \<subseteq> newInt n f"
   228   using newInt_ex by auto
   229 
   230 
   231 text {* Another fundamental property is that no element in the range
   232 of f is in the intersection of all closed intervals generated by
   233 newInt. *}
   234 
   235 lemma newInt_inter:
   236   "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
   237 proof
   238   fix n::nat
   239   {
   240     assume n0: "n = 0"
   241     moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}" by simp
   242     ultimately have "f n \<notin> newInt n f" by simp
   243   }
   244   moreover
   245   {
   246     assume "\<not> n = 0"
   247     hence "n > 0" by simp
   248     then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc)
   249 
   250     from newInt_ex have
   251       "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
   252        newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
   253     then have "f (Suc m) \<notin> newInt (Suc m) f" by auto
   254     with ndef have "f n \<notin> newInt n f" by simp
   255   }
   256   ultimately have "f n \<notin> newInt n f" by (rule case_split)
   257   thus "f n \<notin> (\<Inter>n. newInt n f)" by auto
   258 qed
   259 
   260 
   261 lemma newInt_notempty:
   262   "(\<Inter>n. newInt n f) \<noteq> {}"
   263 proof -
   264   let ?g = "\<lambda>n. newInt n f"
   265   have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
   266   proof
   267     fix n
   268     show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)
   269   qed
   270   moreover have "\<forall>n. \<exists>a b. ?g n = {a..b} \<and> a \<le> b"
   271   proof
   272     fix n::nat
   273     {
   274       assume "n = 0"
   275       then have
   276         "?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)"
   277         by simp
   278       hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast
   279     }
   280     moreover
   281     {
   282       assume "\<not> n = 0"
   283       then have "n > 0" by simp
   284       then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)
   285 
   286       have
   287         "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
   288         (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
   289         by (rule newInt_ex)
   290       then obtain a and b where
   291         "a < b \<and> (newInt (Suc m) f) = {a..b}" by auto
   292       with nd have "?g n = {a..b} \<and> a \<le> b" by auto
   293       hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast
   294     }
   295     ultimately show "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by (rule case_split)
   296   qed
   297   ultimately show ?thesis by (rule NIP)
   298 qed
   299 
   300 
   301 subsection {* Final Theorem *}
   302 
   303 theorem real_non_denum:
   304   shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
   305 proof -- "by contradiction"
   306   assume "\<exists>f::nat\<Rightarrow>real. surj f"
   307   then obtain f::"nat\<Rightarrow>real" where rangeF: "surj f" by auto
   308   -- "We now produce a real number x that is not in the range of f, using the properties of newInt. "
   309   have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
   310   moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
   311   ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast
   312   moreover from rangeF have "x \<in> range f" by simp
   313   ultimately show False by blast
   314 qed
   315 
   316 end
   317