src/HOL/Library/ContNotDenum.thy
changeset 29026 5fbaa05f637f
parent 28952 15a4b2cf8c34
child 30663 0b6aff7451b2
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/ContNotDenum.thy	Wed Dec 10 10:23:47 2008 +0100
     1.3 @@ -0,0 +1,579 @@
     1.4 +(*  Title       : HOL/ContNonDenum
     1.5 +    Author      : Benjamin Porter, Monash University, NICTA, 2005
     1.6 +*)
     1.7 +
     1.8 +header {* Non-denumerability of the Continuum. *}
     1.9 +
    1.10 +theory ContNotDenum
    1.11 +imports RComplete Hilbert_Choice
    1.12 +begin
    1.13 +
    1.14 +subsection {* Abstract *}
    1.15 +
    1.16 +text {* The following document presents a proof that the Continuum is
    1.17 +uncountable. It is formalised in the Isabelle/Isar theorem proving
    1.18 +system.
    1.19 +
    1.20 +{\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other
    1.21 +words, there does not exist a function f:@{text "\<nat>\<Rightarrow>\<real>"} such that f is
    1.22 +surjective.
    1.23 +
    1.24 +{\em Outline:} An elegant informal proof of this result uses Cantor's
    1.25 +Diagonalisation argument. The proof presented here is not this
    1.26 +one. First we formalise some properties of closed intervals, then we
    1.27 +prove the Nested Interval Property. This property relies on the
    1.28 +completeness of the Real numbers and is the foundation for our
    1.29 +argument. Informally it states that an intersection of countable
    1.30 +closed intervals (where each successive interval is a subset of the
    1.31 +last) is non-empty. We then assume a surjective function f:@{text
    1.32 +"\<nat>\<Rightarrow>\<real>"} exists and find a real x such that x is not in the range of f
    1.33 +by generating a sequence of closed intervals then using the NIP. *}
    1.34 +
    1.35 +subsection {* Closed Intervals *}
    1.36 +
    1.37 +text {* This section formalises some properties of closed intervals. *}
    1.38 +
    1.39 +subsubsection {* Definition *}
    1.40 +
    1.41 +definition
    1.42 +  closed_int :: "real \<Rightarrow> real \<Rightarrow> real set" where
    1.43 +  "closed_int x y = {z. x \<le> z \<and> z \<le> y}"
    1.44 +
    1.45 +subsubsection {* Properties *}
    1.46 +
    1.47 +lemma closed_int_subset:
    1.48 +  assumes xy: "x1 \<ge> x0" "y1 \<le> y0"
    1.49 +  shows "closed_int x1 y1 \<subseteq> closed_int x0 y0"
    1.50 +proof -
    1.51 +  {
    1.52 +    fix x::real
    1.53 +    assume "x \<in> closed_int x1 y1"
    1.54 +    hence "x \<ge> x1 \<and> x \<le> y1" by (simp add: closed_int_def)
    1.55 +    with xy have "x \<ge> x0 \<and> x \<le> y0" by auto
    1.56 +    hence "x \<in> closed_int x0 y0" by (simp add: closed_int_def)
    1.57 +  }
    1.58 +  thus ?thesis by auto
    1.59 +qed
    1.60 +
    1.61 +lemma closed_int_least:
    1.62 +  assumes a: "a \<le> b"
    1.63 +  shows "a \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. a \<le> x)"
    1.64 +proof
    1.65 +  from a have "a\<in>{x. a\<le>x \<and> x\<le>b}" by simp
    1.66 +  thus "a \<in> closed_int a b" by (unfold closed_int_def)
    1.67 +next
    1.68 +  have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. a\<le>x" by simp
    1.69 +  thus "\<forall>x \<in> closed_int a b. a \<le> x" by (unfold closed_int_def)
    1.70 +qed
    1.71 +
    1.72 +lemma closed_int_most:
    1.73 +  assumes a: "a \<le> b"
    1.74 +  shows "b \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. x \<le> b)"
    1.75 +proof
    1.76 +  from a have "b\<in>{x. a\<le>x \<and> x\<le>b}" by simp
    1.77 +  thus "b \<in> closed_int a b" by (unfold closed_int_def)
    1.78 +next
    1.79 +  have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. x\<le>b" by simp
    1.80 +  thus "\<forall>x \<in> closed_int a b. x\<le>b" by (unfold closed_int_def)
    1.81 +qed
    1.82 +
    1.83 +lemma closed_not_empty:
    1.84 +  shows "a \<le> b \<Longrightarrow> \<exists>x. x \<in> closed_int a b" 
    1.85 +  by (auto dest: closed_int_least)
    1.86 +
    1.87 +lemma closed_mem:
    1.88 +  assumes "a \<le> c" and "c \<le> b"
    1.89 +  shows "c \<in> closed_int a b"
    1.90 +  using assms unfolding closed_int_def by auto
    1.91 +
    1.92 +lemma closed_subset:
    1.93 +  assumes ac: "a \<le> b"  "c \<le> d" 
    1.94 +  assumes closed: "closed_int a b \<subseteq> closed_int c d"
    1.95 +  shows "b \<ge> c"
    1.96 +proof -
    1.97 +  from closed have "\<forall>x\<in>closed_int a b. x\<in>closed_int c d" by auto
    1.98 +  hence "\<forall>x. a\<le>x \<and> x\<le>b \<longrightarrow> c\<le>x \<and> x\<le>d" by (unfold closed_int_def, auto)
    1.99 +  with ac have "c\<le>b \<and> b\<le>d" by simp
   1.100 +  thus ?thesis by auto
   1.101 +qed
   1.102 +
   1.103 +
   1.104 +subsection {* Nested Interval Property *}
   1.105 +
   1.106 +theorem NIP:
   1.107 +  fixes f::"nat \<Rightarrow> real set"
   1.108 +  assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
   1.109 +  and closed: "\<forall>n. \<exists>a b. f n = closed_int a b \<and> a \<le> b"
   1.110 +  shows "(\<Inter>n. f n) \<noteq> {}"
   1.111 +proof -
   1.112 +  let ?g = "\<lambda>n. (SOME c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x))"
   1.113 +  have ne: "\<forall>n. \<exists>x. x\<in>(f n)"
   1.114 +  proof
   1.115 +    fix n
   1.116 +    from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" by simp
   1.117 +    then obtain a and b where fn: "f n = closed_int a b \<and> a \<le> b" by auto
   1.118 +    hence "a \<le> b" ..
   1.119 +    with closed_not_empty have "\<exists>x. x\<in>closed_int a b" by simp
   1.120 +    with fn show "\<exists>x. x\<in>(f n)" by simp
   1.121 +  qed
   1.122 +
   1.123 +  have gdef: "\<forall>n. (?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)"
   1.124 +  proof
   1.125 +    fix n
   1.126 +    from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
   1.127 +    then obtain a and b where ff: "f n = closed_int a b" and "a \<le> b" by auto
   1.128 +    hence "a \<le> b" by simp
   1.129 +    hence "a\<in>closed_int a b \<and> (\<forall>x\<in>closed_int a b. a \<le> x)" by (rule closed_int_least)
   1.130 +    with ff have "a\<in>(f n) \<and> (\<forall>x\<in>(f n). a \<le> x)" by simp
   1.131 +    hence "\<exists>c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x)" ..
   1.132 +    thus "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by (rule someI_ex)
   1.133 +  qed
   1.134 +
   1.135 +  -- "A denotes the set of all left-most points of all the intervals ..."
   1.136 +  moreover obtain A where Adef: "A = ?g ` \<nat>" by simp
   1.137 +  ultimately have "\<exists>x. x\<in>A"
   1.138 +  proof -
   1.139 +    have "(0::nat) \<in> \<nat>" by simp
   1.140 +    moreover have "?g 0 = ?g 0" by simp
   1.141 +    ultimately have "?g 0 \<in> ?g ` \<nat>" by (rule  rev_image_eqI)
   1.142 +    with Adef have "?g 0 \<in> A" by simp
   1.143 +    thus ?thesis ..
   1.144 +  qed
   1.145 +
   1.146 +  -- "Now show that A is bounded above ..."
   1.147 +  moreover have "\<exists>y. isUb (UNIV::real set) A y"
   1.148 +  proof -
   1.149 +    {
   1.150 +      fix n
   1.151 +      from ne have ex: "\<exists>x. x\<in>(f n)" ..
   1.152 +      from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
   1.153 +      moreover
   1.154 +      from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
   1.155 +      then obtain a and b where "f n = closed_int a b \<and> a \<le> b" by auto
   1.156 +      hence "b\<in>(f n) \<and> (\<forall>x\<in>(f n). x \<le> b)" using closed_int_most by blast
   1.157 +      ultimately have "\<forall>x\<in>(f n). (?g n) \<le> b" by simp
   1.158 +      with ex have "(?g n) \<le> b" by auto
   1.159 +      hence "\<exists>b. (?g n) \<le> b" by auto
   1.160 +    }
   1.161 +    hence aux: "\<forall>n. \<exists>b. (?g n) \<le> b" ..
   1.162 +
   1.163 +    have fs: "\<forall>n::nat. f n \<subseteq> f 0"
   1.164 +    proof (rule allI, induct_tac n)
   1.165 +      show "f 0 \<subseteq> f 0" by simp
   1.166 +    next
   1.167 +      fix n
   1.168 +      assume "f n \<subseteq> f 0"
   1.169 +      moreover from subset have "f (Suc n) \<subseteq> f n" ..
   1.170 +      ultimately show "f (Suc n) \<subseteq> f 0" by simp
   1.171 +    qed
   1.172 +    have "\<forall>n. (?g n)\<in>(f 0)"
   1.173 +    proof
   1.174 +      fix n
   1.175 +      from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
   1.176 +      hence "?g n \<in> f n" ..
   1.177 +      with fs show "?g n \<in> f 0" by auto
   1.178 +    qed
   1.179 +    moreover from closed
   1.180 +      obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast
   1.181 +    ultimately have "\<forall>n. ?g n \<in> closed_int a b" by auto
   1.182 +    with alb have "\<forall>n. ?g n \<le> b" using closed_int_most by blast
   1.183 +    with Adef have "\<forall>y\<in>A. y\<le>b" by auto
   1.184 +    hence "A *<= b" by (unfold setle_def)
   1.185 +    moreover have "b \<in> (UNIV::real set)" by simp
   1.186 +    ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
   1.187 +    hence "isUb (UNIV::real set) A b" by (unfold isUb_def)
   1.188 +    thus ?thesis by auto
   1.189 +  qed
   1.190 +  -- "by the Axiom Of Completeness, A has a least upper bound ..."
   1.191 +  ultimately have "\<exists>t. isLub UNIV A t" by (rule reals_complete)
   1.192 +
   1.193 +  -- "denote this least upper bound as t ..."
   1.194 +  then obtain t where tdef: "isLub UNIV A t" ..
   1.195 +
   1.196 +  -- "and finally show that this least upper bound is in all the intervals..."
   1.197 +  have "\<forall>n. t \<in> f n"
   1.198 +  proof
   1.199 +    fix n::nat
   1.200 +    from closed obtain a and b where
   1.201 +      int: "f n = closed_int a b" and alb: "a \<le> b" by blast
   1.202 +
   1.203 +    have "t \<ge> a"
   1.204 +    proof -
   1.205 +      have "a \<in> A"
   1.206 +      proof -
   1.207 +          (* by construction *)
   1.208 +        from alb int have ain: "a\<in>f n \<and> (\<forall>x\<in>f n. a \<le> x)"
   1.209 +          using closed_int_least by blast
   1.210 +        moreover have "\<forall>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<longrightarrow> e = a"
   1.211 +        proof clarsimp
   1.212 +          fix e
   1.213 +          assume ein: "e \<in> f n" and lt: "\<forall>x\<in>f n. e \<le> x"
   1.214 +          from lt ain have aux: "\<forall>x\<in>f n. a \<le> x \<and> e \<le> x" by auto
   1.215 +  
   1.216 +          from ein aux have "a \<le> e \<and> e \<le> e" by auto
   1.217 +          moreover from ain aux have "a \<le> a \<and> e \<le> a" by auto
   1.218 +          ultimately show "e = a" by simp
   1.219 +        qed
   1.220 +        hence "\<And>e.  e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<Longrightarrow> e = a" by simp
   1.221 +        ultimately have "(?g n) = a" by (rule some_equality)
   1.222 +        moreover
   1.223 +        {
   1.224 +          have "n = of_nat n" by simp
   1.225 +          moreover have "of_nat n \<in> \<nat>" by simp
   1.226 +          ultimately have "n \<in> \<nat>"
   1.227 +            apply -
   1.228 +            apply (subst(asm) eq_sym_conv)
   1.229 +            apply (erule subst)
   1.230 +            .
   1.231 +        }
   1.232 +        with Adef have "(?g n) \<in> A" by auto
   1.233 +        ultimately show ?thesis by simp
   1.234 +      qed 
   1.235 +      with tdef show "a \<le> t" by (rule isLubD2)
   1.236 +    qed
   1.237 +    moreover have "t \<le> b"
   1.238 +    proof -
   1.239 +      have "isUb UNIV A b"
   1.240 +      proof -
   1.241 +        {
   1.242 +          from alb int have
   1.243 +            ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
   1.244 +          
   1.245 +          have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
   1.246 +          proof (rule allI, induct_tac m)
   1.247 +            show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
   1.248 +          next
   1.249 +            fix m n
   1.250 +            assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
   1.251 +            {
   1.252 +              fix p
   1.253 +              from pp have "f (p + n) \<subseteq> f p" by simp
   1.254 +              moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
   1.255 +              hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
   1.256 +              ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
   1.257 +            }
   1.258 +            thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
   1.259 +          qed 
   1.260 +          have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
   1.261 +          proof ((rule allI)+, rule impI)
   1.262 +            fix \<alpha>::nat and \<beta>::nat
   1.263 +            assume "\<beta> \<le> \<alpha>"
   1.264 +            hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
   1.265 +            then obtain k where "\<alpha> = \<beta> + k" ..
   1.266 +            moreover
   1.267 +            from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
   1.268 +            ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
   1.269 +          qed 
   1.270 +          
   1.271 +          fix m   
   1.272 +          {
   1.273 +            assume "m \<ge> n"
   1.274 +            with subsetm have "f m \<subseteq> f n" by simp
   1.275 +            with ain have "\<forall>x\<in>f m. x \<le> b" by auto
   1.276 +            moreover
   1.277 +            from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
   1.278 +            ultimately have "?g m \<le> b" by auto
   1.279 +          }
   1.280 +          moreover
   1.281 +          {
   1.282 +            assume "\<not>(m \<ge> n)"
   1.283 +            hence "m < n" by simp
   1.284 +            with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
   1.285 +            from closed obtain ma and mb where
   1.286 +              "f m = closed_int ma mb \<and> ma \<le> mb" by blast
   1.287 +            hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto 
   1.288 +            from one alb sub fm int have "ma \<le> b" using closed_subset by blast
   1.289 +            moreover have "(?g m) = ma"
   1.290 +            proof -
   1.291 +              from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
   1.292 +              moreover from one have
   1.293 +                "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
   1.294 +                by (rule closed_int_least)
   1.295 +              with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
   1.296 +              ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
   1.297 +              thus "?g m = ma" by auto
   1.298 +            qed
   1.299 +            ultimately have "?g m \<le> b" by simp
   1.300 +          } 
   1.301 +          ultimately have "?g m \<le> b" by (rule case_split)
   1.302 +        }
   1.303 +        with Adef have "\<forall>y\<in>A. y\<le>b" by auto
   1.304 +        hence "A *<= b" by (unfold setle_def)
   1.305 +        moreover have "b \<in> (UNIV::real set)" by simp
   1.306 +        ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
   1.307 +        thus "isUb (UNIV::real set) A b" by (unfold isUb_def)
   1.308 +      qed
   1.309 +      with tdef show "t \<le> b" by (rule isLub_le_isUb)
   1.310 +    qed
   1.311 +    ultimately have "t \<in> closed_int a b" by (rule closed_mem)
   1.312 +    with int show "t \<in> f n" by simp
   1.313 +  qed
   1.314 +  hence "t \<in> (\<Inter>n. f n)" by auto
   1.315 +  thus ?thesis by auto
   1.316 +qed
   1.317 +
   1.318 +subsection {* Generating the intervals *}
   1.319 +
   1.320 +subsubsection {* Existence of non-singleton closed intervals *}
   1.321 +
   1.322 +text {* This lemma asserts that given any non-singleton closed
   1.323 +interval (a,b) and any element c, there exists a closed interval that
   1.324 +is a subset of (a,b) and that does not contain c and is a
   1.325 +non-singleton itself. *}
   1.326 +
   1.327 +lemma closed_subset_ex:
   1.328 +  fixes c::real
   1.329 +  assumes alb: "a < b"
   1.330 +  shows
   1.331 +    "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
   1.332 +proof -
   1.333 +  {
   1.334 +    assume clb: "c < b"
   1.335 +    {
   1.336 +      assume cla: "c < a"
   1.337 +      from alb cla clb have "c \<notin> closed_int a b" by (unfold closed_int_def, auto)
   1.338 +      with alb have
   1.339 +        "a < b \<and> closed_int a b \<subseteq> closed_int a b \<and> c \<notin> closed_int a b"
   1.340 +        by auto
   1.341 +      hence
   1.342 +        "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
   1.343 +        by auto
   1.344 +    }
   1.345 +    moreover
   1.346 +    {
   1.347 +      assume ncla: "\<not>(c < a)"
   1.348 +      with clb have cdef: "a \<le> c \<and> c < b" by simp
   1.349 +      obtain ka where kadef: "ka = (c + b)/2" by blast
   1.350 +
   1.351 +      from kadef clb have kalb: "ka < b" by auto
   1.352 +      moreover from kadef cdef have kagc: "ka > c" by simp
   1.353 +      ultimately have "c\<notin>(closed_int ka b)" by (unfold closed_int_def, auto)
   1.354 +      moreover from cdef kagc have "ka \<ge> a" by simp
   1.355 +      hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
   1.356 +      ultimately have
   1.357 +        "ka < b  \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b"
   1.358 +        using kalb by auto
   1.359 +      hence
   1.360 +        "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
   1.361 +        by auto
   1.362 +
   1.363 +    }
   1.364 +    ultimately have
   1.365 +      "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
   1.366 +      by (rule case_split)
   1.367 +  }
   1.368 +  moreover
   1.369 +  {
   1.370 +    assume "\<not> (c < b)"
   1.371 +    hence cgeb: "c \<ge> b" by simp
   1.372 +
   1.373 +    obtain kb where kbdef: "kb = (a + b)/2" by blast
   1.374 +    with alb have kblb: "kb < b" by auto
   1.375 +    with kbdef cgeb have "a < kb \<and> kb < c" by auto
   1.376 +    moreover hence "c \<notin> (closed_int a kb)" by (unfold closed_int_def, auto)
   1.377 +    moreover from kblb have
   1.378 +      "closed_int a kb \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
   1.379 +    ultimately have
   1.380 +      "a < kb \<and>  closed_int a kb \<subseteq> closed_int a b \<and> c\<notin>closed_int a kb"
   1.381 +      by simp
   1.382 +    hence
   1.383 +      "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
   1.384 +      by auto
   1.385 +  }
   1.386 +  ultimately show ?thesis by (rule case_split)
   1.387 +qed
   1.388 +
   1.389 +subsection {* newInt: Interval generation *}
   1.390 +
   1.391 +text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
   1.392 +closed interval such that @{text "newInt (Suc n) f \<subseteq> newInt n f"} and
   1.393 +does not contain @{text "f (Suc n)"}. With the base case defined such
   1.394 +that @{text "(f 0)\<notin>newInt 0 f"}. *}
   1.395 +
   1.396 +subsubsection {* Definition *}
   1.397 +
   1.398 +primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
   1.399 +  "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"
   1.400 +  | "newInt (Suc n) f =
   1.401 +      (SOME e. (\<exists>e1 e2.
   1.402 +       e1 < e2 \<and>
   1.403 +       e = closed_int e1 e2 \<and>
   1.404 +       e \<subseteq> (newInt n f) \<and>
   1.405 +       (f (Suc n)) \<notin> e)
   1.406 +      )"
   1.407 +
   1.408 +declare newInt.simps [code del]
   1.409 +
   1.410 +subsubsection {* Properties *}
   1.411 +
   1.412 +text {* We now show that every application of newInt returns an
   1.413 +appropriate interval. *}
   1.414 +
   1.415 +lemma newInt_ex:
   1.416 +  "\<exists>a b. a < b \<and>
   1.417 +   newInt (Suc n) f = closed_int a b \<and>
   1.418 +   newInt (Suc n) f \<subseteq> newInt n f \<and>
   1.419 +   f (Suc n) \<notin> newInt (Suc n) f"
   1.420 +proof (induct n)
   1.421 +  case 0
   1.422 +
   1.423 +  let ?e = "SOME e. \<exists>e1 e2.
   1.424 +   e1 < e2 \<and>
   1.425 +   e = closed_int e1 e2 \<and>
   1.426 +   e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
   1.427 +   f (Suc 0) \<notin> e"
   1.428 +
   1.429 +  have "newInt (Suc 0) f = ?e" by auto
   1.430 +  moreover
   1.431 +  have "f 0 + 1 < f 0 + 2" by simp
   1.432 +  with closed_subset_ex have
   1.433 +    "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
   1.434 +     f (Suc 0) \<notin> (closed_int ka kb)" .
   1.435 +  hence
   1.436 +    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
   1.437 +     e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> e" by simp
   1.438 +  hence
   1.439 +    "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
   1.440 +     ?e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> ?e"
   1.441 +    by (rule someI_ex)
   1.442 +  ultimately have "\<exists>e1 e2. e1 < e2 \<and>
   1.443 +   newInt (Suc 0) f = closed_int e1 e2 \<and>
   1.444 +   newInt (Suc 0) f \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
   1.445 +   f (Suc 0) \<notin> newInt (Suc 0) f" by simp
   1.446 +  thus
   1.447 +    "\<exists>a b. a < b \<and> newInt (Suc 0) f = closed_int a b \<and>
   1.448 +     newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
   1.449 +    by simp
   1.450 +next
   1.451 +  case (Suc n)
   1.452 +  hence "\<exists>a b.
   1.453 +   a < b \<and>
   1.454 +   newInt (Suc n) f = closed_int a b \<and>
   1.455 +   newInt (Suc n) f \<subseteq> newInt n f \<and>
   1.456 +   f (Suc n) \<notin> newInt (Suc n) f" by simp
   1.457 +  then obtain a and b where ab: "a < b \<and>
   1.458 +   newInt (Suc n) f = closed_int a b \<and>
   1.459 +   newInt (Suc n) f \<subseteq> newInt n f \<and>
   1.460 +   f (Suc n) \<notin> newInt (Suc n) f" by auto
   1.461 +  hence cab: "closed_int a b = newInt (Suc n) f" by simp
   1.462 +
   1.463 +  let ?e = "SOME e. \<exists>e1 e2.
   1.464 +    e1 < e2 \<and>
   1.465 +    e = closed_int e1 e2 \<and>
   1.466 +    e \<subseteq> closed_int a b \<and>
   1.467 +    f (Suc (Suc n)) \<notin> e"
   1.468 +  from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto
   1.469 +
   1.470 +  from ab have "a < b" by simp
   1.471 +  with closed_subset_ex have
   1.472 +    "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and>
   1.473 +     f (Suc (Suc n)) \<notin> closed_int ka kb" .
   1.474 +  hence
   1.475 +    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
   1.476 +     closed_int ka kb \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> closed_int ka kb"
   1.477 +    by simp
   1.478 +  hence
   1.479 +    "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
   1.480 +     e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> e" by simp
   1.481 +  hence
   1.482 +    "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
   1.483 +     ?e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
   1.484 +  with ab ni show
   1.485 +    "\<exists>ka kb. ka < kb \<and>
   1.486 +     newInt (Suc (Suc n)) f = closed_int ka kb \<and>
   1.487 +     newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
   1.488 +     f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto
   1.489 +qed
   1.490 +
   1.491 +lemma newInt_subset:
   1.492 +  "newInt (Suc n) f \<subseteq> newInt n f"
   1.493 +  using newInt_ex by auto
   1.494 +
   1.495 +
   1.496 +text {* Another fundamental property is that no element in the range
   1.497 +of f is in the intersection of all closed intervals generated by
   1.498 +newInt. *}
   1.499 +
   1.500 +lemma newInt_inter:
   1.501 +  "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
   1.502 +proof
   1.503 +  fix n::nat
   1.504 +  {
   1.505 +    assume n0: "n = 0"
   1.506 +    moreover have "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)" by simp
   1.507 +    ultimately have "f n \<notin> newInt n f" by (unfold closed_int_def, simp)
   1.508 +  }
   1.509 +  moreover
   1.510 +  {
   1.511 +    assume "\<not> n = 0"
   1.512 +    hence "n > 0" by simp
   1.513 +    then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc)
   1.514 +
   1.515 +    from newInt_ex have
   1.516 +      "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
   1.517 +       newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
   1.518 +    then have "f (Suc m) \<notin> newInt (Suc m) f" by auto
   1.519 +    with ndef have "f n \<notin> newInt n f" by simp
   1.520 +  }
   1.521 +  ultimately have "f n \<notin> newInt n f" by (rule case_split)
   1.522 +  thus "f n \<notin> (\<Inter>n. newInt n f)" by auto
   1.523 +qed
   1.524 +
   1.525 +
   1.526 +lemma newInt_notempty:
   1.527 +  "(\<Inter>n. newInt n f) \<noteq> {}"
   1.528 +proof -
   1.529 +  let ?g = "\<lambda>n. newInt n f"
   1.530 +  have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
   1.531 +  proof
   1.532 +    fix n
   1.533 +    show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)
   1.534 +  qed
   1.535 +  moreover have "\<forall>n. \<exists>a b. ?g n = closed_int a b \<and> a \<le> b"
   1.536 +  proof
   1.537 +    fix n::nat
   1.538 +    {
   1.539 +      assume "n = 0"
   1.540 +      then have
   1.541 +        "?g n = closed_int (f 0 + 1) (f 0 + 2) \<and> (f 0 + 1 \<le> f 0 + 2)"
   1.542 +        by simp
   1.543 +      hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
   1.544 +    }
   1.545 +    moreover
   1.546 +    {
   1.547 +      assume "\<not> n = 0"
   1.548 +      then have "n > 0" by simp
   1.549 +      then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)
   1.550 +
   1.551 +      have
   1.552 +        "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
   1.553 +        (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
   1.554 +        by (rule newInt_ex)
   1.555 +      then obtain a and b where
   1.556 +        "a < b \<and> (newInt (Suc m) f) = closed_int a b" by auto
   1.557 +      with nd have "?g n = closed_int a b \<and> a \<le> b" by auto
   1.558 +      hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
   1.559 +    }
   1.560 +    ultimately show "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by (rule case_split)
   1.561 +  qed
   1.562 +  ultimately show ?thesis by (rule NIP)
   1.563 +qed
   1.564 +
   1.565 +
   1.566 +subsection {* Final Theorem *}
   1.567 +
   1.568 +theorem real_non_denum:
   1.569 +  shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
   1.570 +proof -- "by contradiction"
   1.571 +  assume "\<exists>f::nat\<Rightarrow>real. surj f"
   1.572 +  then obtain f::"nat\<Rightarrow>real" where "surj f" by auto
   1.573 +  hence rangeF: "range f = UNIV" by (rule surj_range)
   1.574 +  -- "We now produce a real number x that is not in the range of f, using the properties of newInt. "
   1.575 +  have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
   1.576 +  moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
   1.577 +  ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast
   1.578 +  moreover from rangeF have "x \<in> range f" by simp
   1.579 +  ultimately show False by blast
   1.580 +qed
   1.581 +
   1.582 +end