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