src/HOL/Library/ContNotDenum.thy
author wenzelm
Tue Apr 29 22:50:55 2014 +0200 (2014-04-29)
changeset 56796 9f84219715a7
parent 54797 be020ec8560c
child 57234 596a499318ab
permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      HOL/Library/ContNonDenum.thy
     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 @{text "f: \<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 @{text
    29 "f: \<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 
    33 subsection {* Closed Intervals *}
    34 
    35 subsection {* Nested Interval Property *}
    36 
    37 theorem NIP:
    38   fixes f :: "nat \<Rightarrow> real set"
    39   assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
    40     and closed: "\<forall>n. \<exists>a b. f n = {a..b} \<and> a \<le> b"
    41   shows "(\<Inter>n. f n) \<noteq> {}"
    42 proof -
    43   let ?I = "\<lambda>n. {Inf (f n) .. Sup (f n)}"
    44   {
    45     fix n
    46     from closed[rule_format, of n] obtain a b where "f n = {a .. b}" "a \<le> b"
    47       by auto
    48     then have "f n = {Inf (f n) .. Sup (f n)}" and "Inf (f n) \<le> Sup (f n)"
    49       by auto
    50   }
    51   note f_eq = this
    52   {
    53     fix n m :: nat
    54     assume "n \<le> m"
    55     then have "f m \<subseteq> f n"
    56       by (induct rule: dec_induct) (metis order_refl, metis order_trans subset)
    57   }
    58   note subset' = this
    59 
    60   have "compact (f 0)"
    61     by (subst f_eq) (rule compact_Icc)
    62   then have "f 0 \<inter> (\<Inter>i. f i) \<noteq> {}"
    63   proof (rule compact_imp_fip_image)
    64     fix I :: "nat set"
    65     assume I: "finite I"
    66     have "{} \<subset> f (Max (insert 0 I))"
    67       using f_eq[of "Max (insert 0 I)"] by auto
    68     also have "\<dots> \<subseteq> (\<Inter>i\<in>insert 0 I. f i)"
    69     proof (rule INF_greatest)
    70       fix i
    71       assume "i \<in> insert 0 I"
    72       with I show "f (Max (insert 0 I)) \<subseteq> f i"
    73         by (intro subset') auto
    74     qed
    75     finally show "f 0 \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
    76       by auto
    77   qed (subst f_eq, auto)
    78   then show "(\<Inter>n. f n) \<noteq> {}"
    79     by auto
    80 qed
    81 
    82 
    83 subsection {* Generating the intervals *}
    84 
    85 subsubsection {* Existence of non-singleton closed intervals *}
    86 
    87 text {* This lemma asserts that given any non-singleton closed
    88 interval (a,b) and any element c, there exists a closed interval that
    89 is a subset of (a,b) and that does not contain c and is a
    90 non-singleton itself. *}
    91 
    92 lemma closed_subset_ex:
    93   fixes c :: real
    94   assumes "a < b"
    95   shows "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb}"
    96 proof (cases "c < b")
    97   case True
    98   show ?thesis
    99   proof (cases "c < a")
   100     case True
   101     with `a < b` `c < b` have "c \<notin> {a..b}"
   102       by auto
   103     with `a < b` show ?thesis
   104       by auto
   105   next
   106     case False
   107     then have "a \<le> c" by simp
   108     def ka \<equiv> "(c + b)/2"
   109     from ka_def `c < b` have "ka < b"
   110       by auto
   111     moreover from ka_def `c < b` have "ka > c"
   112       by simp
   113     ultimately have "c \<notin> {ka..b}"
   114       by auto
   115     moreover from `a \<le> c` `ka > c` have "ka \<ge> a"
   116       by simp
   117     then have "{ka..b} \<subseteq> {a..b}"
   118       by auto
   119     ultimately have "ka < b  \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}"
   120       using `ka < b` by auto
   121     then show ?thesis
   122       by auto
   123   qed
   124 next
   125   case False
   126   then have "c \<ge> b" by simp
   127   def kb \<equiv> "(a + b)/2"
   128   with `a < b` have "kb < b" by auto
   129   with kb_def `c \<ge> b` have "a < kb" "kb < c"
   130     by auto
   131   from `kb < c` have c: "c \<notin> {a..kb}"
   132     by auto
   133   with `kb < b` have "{a..kb} \<subseteq> {a..b}"
   134     by auto
   135   with `a < kb` c have "a < kb \<and> {a..kb} \<subseteq> {a..b} \<and> c \<notin> {a..kb}"
   136     by simp
   137   then show ?thesis
   138     by auto
   139 qed
   140 
   141 
   142 subsection {* newInt: Interval generation *}
   143 
   144 text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
   145 closed interval such that @{text "newInt (Suc n) f \<subseteq> newInt n f"} and
   146 does not contain @{text "f (Suc n)"}. With the base case defined such
   147 that @{text "(f 0)\<notin>newInt 0 f"}. *}
   148 
   149 
   150 subsubsection {* Definition *}
   151 
   152 primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)"
   153 where
   154   "newInt 0 f = {f 0 + 1..f 0 + 2}"
   155 | "newInt (Suc n) f =
   156     (SOME e.
   157       (\<exists>e1 e2.
   158          e1 < e2 \<and>
   159          e = {e1..e2} \<and>
   160          e \<subseteq> newInt n f \<and>
   161          f (Suc n) \<notin> e))"
   162 
   163 
   164 subsubsection {* Properties *}
   165 
   166 text {* We now show that every application of newInt returns an
   167 appropriate interval. *}
   168 
   169 lemma newInt_ex:
   170   "\<exists>a b. a < b \<and>
   171     newInt (Suc n) f = {a..b} \<and>
   172     newInt (Suc n) f \<subseteq> newInt n f \<and>
   173     f (Suc n) \<notin> newInt (Suc n) f"
   174 proof (induct n)
   175   case 0
   176   let ?e = "SOME e. \<exists>e1 e2.
   177     e1 < e2 \<and>
   178     e = {e1..e2} \<and>
   179     e \<subseteq> {f 0 + 1..f 0 + 2} \<and>
   180     f (Suc 0) \<notin> e"
   181 
   182   have "newInt (Suc 0) f = ?e" by auto
   183   moreover
   184   have "f 0 + 1 < f 0 + 2" by simp
   185   with closed_subset_ex
   186   have "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> {ka..kb}" .
   187   then have "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and> e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> e"
   188     by simp
   189   then have "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> ?e"
   190     by (rule someI_ex)
   191   ultimately have "\<exists>e1 e2. e1 < e2 \<and>
   192       newInt (Suc 0) f = {e1..e2} \<and>
   193       newInt (Suc 0) f \<subseteq> {f 0 + 1..f 0 + 2} \<and>
   194       f (Suc 0) \<notin> newInt (Suc 0) f"
   195     by simp
   196   then show "\<exists>a b. a < b \<and> newInt (Suc 0) f = {a..b} \<and>
   197       newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
   198     by simp
   199 next
   200   case (Suc n)
   201   then have "\<exists>a b.
   202       a < b \<and>
   203       newInt (Suc n) f = {a..b} \<and>
   204       newInt (Suc n) f \<subseteq> newInt n f \<and>
   205       f (Suc n) \<notin> newInt (Suc n) f"
   206     by simp
   207   then obtain a and b where ab: "a < b \<and>
   208       newInt (Suc n) f = {a..b} \<and>
   209       newInt (Suc n) f \<subseteq> newInt n f \<and>
   210       f (Suc n) \<notin> newInt (Suc n) f"
   211     by auto
   212   then have cab: "{a..b} = newInt (Suc n) f"
   213     by simp
   214 
   215   let ?e = "SOME e. \<exists>e1 e2.
   216       e1 < e2 \<and>
   217       e = {e1..e2} \<and>
   218       e \<subseteq> {a..b} \<and>
   219       f (Suc (Suc n)) \<notin> e"
   220   from cab have ni: "newInt (Suc (Suc n)) f = ?e"
   221     by auto
   222 
   223   from ab have "a < b" by simp
   224   with closed_subset_ex have "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and>
   225     f (Suc (Suc n)) \<notin> {ka..kb}" .
   226   then have "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
   227       {ka..kb} \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> {ka..kb}"
   228     by simp
   229   then have "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and> e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> e"
   230     by simp
   231   then have "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> ?e"
   232     by (rule someI_ex)
   233   with ab ni show "\<exists>ka kb. ka < kb \<and>
   234       newInt (Suc (Suc n)) f = {ka..kb} \<and>
   235       newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
   236       f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f"
   237     by auto
   238 qed
   239 
   240 lemma newInt_subset: "newInt (Suc n) f \<subseteq> newInt n f"
   241   using newInt_ex by auto
   242 
   243 
   244 text {* Another fundamental property is that no element in the range
   245 of f is in the intersection of all closed intervals generated by
   246 newInt. *}
   247 
   248 lemma newInt_inter: "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
   249 proof
   250   fix n :: nat
   251   have "f n \<notin> newInt n f"
   252   proof (cases n)
   253     case 0
   254     moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}"
   255       by simp
   256     ultimately show ?thesis by simp
   257   next
   258     case (Suc m)
   259     from newInt_ex have "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
   260       newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
   261     then have "f (Suc m) \<notin> newInt (Suc m) f"
   262       by auto
   263     with Suc show ?thesis by simp
   264   qed
   265   then show "f n \<notin> (\<Inter>n. newInt n f)" by auto
   266 qed
   267 
   268 lemma newInt_notempty: "(\<Inter>n. newInt n f) \<noteq> {}"
   269 proof -
   270   let ?g = "\<lambda>n. newInt n f"
   271   have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
   272   proof
   273     fix n
   274     show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)
   275   qed
   276   moreover have "\<forall>n. \<exists>a b. ?g n = {a..b} \<and> a \<le> b"
   277   proof
   278     fix n :: nat
   279     show "\<exists>a b. ?g n = {a..b} \<and> a \<le> b"
   280     proof (cases n)
   281       case 0
   282       then have "?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)"
   283         by simp
   284       then show ?thesis
   285         by blast
   286     next
   287       case (Suc m)
   288       have "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
   289         (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
   290         by (rule newInt_ex)
   291       then obtain a and b where "a < b \<and> (newInt (Suc m) f) = {a..b}"
   292         by auto
   293       with Suc have "?g n = {a..b} \<and> a \<le> b"
   294         by auto
   295       then show ?thesis
   296         by blast
   297     qed
   298   qed
   299   ultimately show ?thesis by (rule NIP)
   300 qed
   301 
   302 
   303 subsection {* Final Theorem *}
   304 
   305 theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)"
   306 proof
   307   assume "\<exists>f :: nat \<Rightarrow> real. surj f"
   308   then obtain f :: "nat \<Rightarrow> real" where "surj f"
   309     by auto
   310   txt "We now produce a real number x that is not in the range of f, using the properties of newInt."
   311   have "\<exists>x. x \<in> (\<Inter>n. newInt n f)"
   312     using newInt_notempty by blast
   313   moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
   314     by (rule newInt_inter)
   315   ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x"
   316     by blast
   317   moreover from `surj f` have "x \<in> range f"
   318     by simp
   319   ultimately show False
   320     by blast
   321 qed
   322 
   323 end
   324