src/HOL/Library/ContNotDenum.thy
changeset 57234 596a499318ab
parent 56796 9f84219715a7
child 58881 b9556a055632
equal deleted inserted replaced
57233:8fcbfce2a2a9 57234:596a499318ab
     1 (*  Title:      HOL/Library/ContNonDenum.thy
     1 (*  Title:      HOL/Library/ContNonDenum.thy
     2     Author:     Benjamin Porter, Monash University, NICTA, 2005
     2     Author:     Benjamin Porter, Monash University, NICTA, 2005
       
     3     Author:     Johannes Hölzl, TU München
     3 *)
     4 *)
     4 
     5 
     5 header {* Non-denumerability of the Continuum. *}
     6 header {* Non-denumerability of the Continuum. *}
     6 
     7 
     7 theory ContNotDenum
     8 theory ContNotDenum
     8 imports Complex_Main
     9 imports Complex_Main Countable_Set
     9 begin
    10 begin
    10 
    11 
    11 subsection {* Abstract *}
    12 subsection {* Abstract *}
    12 
    13 
    13 text {* The following document presents a proof that the Continuum is
    14 text {* The following document presents a proof that the Continuum is
    27 closed intervals (where each successive interval is a subset of the
    28 closed intervals (where each successive interval is a subset of the
    28 last) is non-empty. We then assume a surjective function @{text
    29 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 "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 by generating a sequence of closed intervals then using the NIP. *}
    31 
    32 
       
    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" ..
    32 
    37 
    33 subsection {* Closed Intervals *}
    38   txt {* First we construct a sequence of nested intervals, ignoring @{term "range f"}. *}
    34 
    39 
    35 subsection {* Nested Interval Property *}
    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
    36 
    49 
    37 theorem NIP:
    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)))"
    38   fixes f :: "nat \<Rightarrow> real set"
    51   def I \<equiv> "\<lambda>n. {fst (ivl n) .. snd (ivl n)}"
    39   assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
    52 
    40     and closed: "\<forall>n. \<exists>a b. f n = {a..b} \<and> a \<le> b"
    53   have ivl[simp]:
    41   shows "(\<Inter>n. f n) \<noteq> {}"
    54     "ivl 0 = (f 0 + 1, f 0 + 2)"
    42 proof -
    55     "\<And>n. ivl (Suc n) = (i (fst (ivl n)) (snd (ivl n)) (f n), j (fst (ivl n)) (snd (ivl n)) (f n))"
    43   let ?I = "\<lambda>n. {Inf (f n) .. Sup (f n)}"
    56     unfolding ivl_def by simp_all
    44   {
    57 
    45     fix n
    58   txt {* This is a decreasing sequence of non-empty intervals. *}
    46     from closed[rule_format, of n] obtain a b where "f n = {a .. b}" "a \<le> b"
    59 
       
    60   { fix n have "fst (ivl n) < snd (ivl n)"
       
    61       by (induct n) (auto intro!: ij) }
       
    62   note less = this
       
    63 
       
    64   have "decseq I"
       
    65     unfolding I_def decseq_Suc_iff ivl fst_conv snd_conv by (intro ij allI less)
       
    66 
       
    67   txt {* Now we apply the finite intersection property of compact sets. *}
       
    68 
       
    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)"
    47       by auto
    77       by auto
    48     then have "f n = {Inf (f n) .. Sup (f n)}" and "Inf (f n) \<le> Sup (f n)"
    78     finally show "I 0 \<inter> (\<Inter>i\<in>S. I i) \<noteq> {}"
    49       by auto
    79       by auto
    50   }
    80   qed (auto simp: I_def)
    51   note f_eq = this
    81   then obtain x where "\<And>n. x \<in> I n"
    52   {
    82     by blast
    53     fix n m :: nat
    83   moreover from `surj f` obtain j where "x = f j"
    54     assume "n \<le> m"
    84     by blast
    55     then have "f m \<subseteq> f n"
    85   ultimately have "f j \<in> I (Suc j)"
    56       by (induct rule: dec_induct) (metis order_refl, metis order_trans subset)
    86     by blast
    57   }
    87   with ij(3)[OF less] show False
    58   note subset' = this
    88     unfolding I_def ivl fst_conv snd_conv by auto
    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
    89 qed
    81 
    90 
       
    91 lemma uncountable_UNIV_real: "uncountable (UNIV::real set)"
       
    92   using real_non_denum unfolding uncountable_def by auto
    82 
    93 
    83 subsection {* Generating the intervals *}
    94 lemma bij_betw_open_intervals:
    84 
    95   fixes a b c d :: real
    85 subsubsection {* Existence of non-singleton closed intervals *}
    96   assumes "a < b" "c < d"
    86 
    97   shows "\<exists>f. bij_betw f {a<..<b} {c<..<d}"
    87 text {* This lemma asserts that given any non-singleton closed
    98 proof -
    88 interval (a,b) and any element c, there exists a closed interval that
    99   def f \<equiv> "\<lambda>a b c d x::real. (d - c)/(b - a) * (x - a) + c"
    89 is a subset of (a,b) and that does not contain c and is a
   100   { fix a b c d x :: real assume *: "a < b" "c < d" "a < x" "x < b"
    90 non-singleton itself. *}
   101     moreover from * have "(d - c) * (x - a) < (d - c) * (b - a)"
    91 
   102       by (intro mult_strict_left_mono) simp_all
    92 lemma closed_subset_ex:
   103     moreover from * have "0 < (d - c) * (x - a) / (b - a)"
    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
   104       by simp
   113     ultimately have "c \<notin> {ka..b}"
   105     ultimately have "f a b c d x < d" "c < f a b c d x"
   114       by auto
   106       by (simp_all add: f_def field_simps) }
   115     moreover from `a \<le> c` `ka > c` have "ka \<ge> a"
   107   with assms have "bij_betw (f a b c d) {a<..<b} {c<..<d}"
   116       by simp
   108     by (intro bij_betw_byWitness[where f'="f c d a b"]) (auto simp: f_def)
   117     then have "{ka..b} \<subseteq> {a..b}"
   109   thus ?thesis by auto
   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
   110 qed
   140 
   111 
       
   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)
   141 
   114 
   142 subsection {* newInt: Interval generation *}
   115 lemma uncountable_open_interval:
   143 
   116   fixes a b :: real assumes ab: "a < b"
   144 text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
   117   shows "uncountable {a<..<b}"
   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 -
   118 proof -
   270   let ?g = "\<lambda>n. newInt n f"
   119   obtain f where "bij_betw f {a <..< b} {-pi/2<..<pi/2}"
   271   have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
   120     using bij_betw_open_intervals[OF `a < b`, of "-pi/2" "pi/2"] by auto
   272   proof
   121   then show ?thesis
   273     fix n
   122     by (metis bij_betw_tan uncountable_bij_betw uncountable_UNIV_real)
   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
   123 qed
   322 
   124 
   323 end
   125 end
   324 
   126