moved ContNotDenum into Library
authornipkow
Wed Dec 10 10:23:47 2008 +0100 (2008-12-10)
changeset 290265fbaa05f637f
parent 28964 f0044cdeb945
child 29027 501780b0bcae
moved ContNotDenum into Library
src/HOL/Complex_Main.thy
src/HOL/ContNotDenum.thy
src/HOL/IsaMakefile
src/HOL/Library/ContNotDenum.thy
src/HOL/Library/Library.thy
src/HOL/Real.thy
     1.1 --- a/src/HOL/Complex_Main.thy	Thu Dec 04 14:17:36 2008 +0100
     1.2 +++ b/src/HOL/Complex_Main.thy	Wed Dec 10 10:23:47 2008 +0100
     1.3 @@ -8,7 +8,6 @@
     1.4  theory Complex_Main
     1.5  imports
     1.6    Main
     1.7 -  ContNotDenum
     1.8    Real
     1.9    "~~/src/HOL/Complex/Fundamental_Theorem_Algebra"
    1.10    Log
     2.1 --- a/src/HOL/ContNotDenum.thy	Thu Dec 04 14:17:36 2008 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,579 +0,0 @@
     2.4 -(*  Title       : HOL/ContNonDenum
     2.5 -    Author      : Benjamin Porter, Monash University, NICTA, 2005
     2.6 -*)
     2.7 -
     2.8 -header {* Non-denumerability of the Continuum. *}
     2.9 -
    2.10 -theory ContNotDenum
    2.11 -imports RComplete Hilbert_Choice
    2.12 -begin
    2.13 -
    2.14 -subsection {* Abstract *}
    2.15 -
    2.16 -text {* The following document presents a proof that the Continuum is
    2.17 -uncountable. It is formalised in the Isabelle/Isar theorem proving
    2.18 -system.
    2.19 -
    2.20 -{\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other
    2.21 -words, there does not exist a function f:@{text "\<nat>\<Rightarrow>\<real>"} such that f is
    2.22 -surjective.
    2.23 -
    2.24 -{\em Outline:} An elegant informal proof of this result uses Cantor's
    2.25 -Diagonalisation argument. The proof presented here is not this
    2.26 -one. First we formalise some properties of closed intervals, then we
    2.27 -prove the Nested Interval Property. This property relies on the
    2.28 -completeness of the Real numbers and is the foundation for our
    2.29 -argument. Informally it states that an intersection of countable
    2.30 -closed intervals (where each successive interval is a subset of the
    2.31 -last) is non-empty. We then assume a surjective function f:@{text
    2.32 -"\<nat>\<Rightarrow>\<real>"} exists and find a real x such that x is not in the range of f
    2.33 -by generating a sequence of closed intervals then using the NIP. *}
    2.34 -
    2.35 -subsection {* Closed Intervals *}
    2.36 -
    2.37 -text {* This section formalises some properties of closed intervals. *}
    2.38 -
    2.39 -subsubsection {* Definition *}
    2.40 -
    2.41 -definition
    2.42 -  closed_int :: "real \<Rightarrow> real \<Rightarrow> real set" where
    2.43 -  "closed_int x y = {z. x \<le> z \<and> z \<le> y}"
    2.44 -
    2.45 -subsubsection {* Properties *}
    2.46 -
    2.47 -lemma closed_int_subset:
    2.48 -  assumes xy: "x1 \<ge> x0" "y1 \<le> y0"
    2.49 -  shows "closed_int x1 y1 \<subseteq> closed_int x0 y0"
    2.50 -proof -
    2.51 -  {
    2.52 -    fix x::real
    2.53 -    assume "x \<in> closed_int x1 y1"
    2.54 -    hence "x \<ge> x1 \<and> x \<le> y1" by (simp add: closed_int_def)
    2.55 -    with xy have "x \<ge> x0 \<and> x \<le> y0" by auto
    2.56 -    hence "x \<in> closed_int x0 y0" by (simp add: closed_int_def)
    2.57 -  }
    2.58 -  thus ?thesis by auto
    2.59 -qed
    2.60 -
    2.61 -lemma closed_int_least:
    2.62 -  assumes a: "a \<le> b"
    2.63 -  shows "a \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. a \<le> x)"
    2.64 -proof
    2.65 -  from a have "a\<in>{x. a\<le>x \<and> x\<le>b}" by simp
    2.66 -  thus "a \<in> closed_int a b" by (unfold closed_int_def)
    2.67 -next
    2.68 -  have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. a\<le>x" by simp
    2.69 -  thus "\<forall>x \<in> closed_int a b. a \<le> x" by (unfold closed_int_def)
    2.70 -qed
    2.71 -
    2.72 -lemma closed_int_most:
    2.73 -  assumes a: "a \<le> b"
    2.74 -  shows "b \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. x \<le> b)"
    2.75 -proof
    2.76 -  from a have "b\<in>{x. a\<le>x \<and> x\<le>b}" by simp
    2.77 -  thus "b \<in> closed_int a b" by (unfold closed_int_def)
    2.78 -next
    2.79 -  have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. x\<le>b" by simp
    2.80 -  thus "\<forall>x \<in> closed_int a b. x\<le>b" by (unfold closed_int_def)
    2.81 -qed
    2.82 -
    2.83 -lemma closed_not_empty:
    2.84 -  shows "a \<le> b \<Longrightarrow> \<exists>x. x \<in> closed_int a b" 
    2.85 -  by (auto dest: closed_int_least)
    2.86 -
    2.87 -lemma closed_mem:
    2.88 -  assumes "a \<le> c" and "c \<le> b"
    2.89 -  shows "c \<in> closed_int a b"
    2.90 -  using assms unfolding closed_int_def by auto
    2.91 -
    2.92 -lemma closed_subset:
    2.93 -  assumes ac: "a \<le> b"  "c \<le> d" 
    2.94 -  assumes closed: "closed_int a b \<subseteq> closed_int c d"
    2.95 -  shows "b \<ge> c"
    2.96 -proof -
    2.97 -  from closed have "\<forall>x\<in>closed_int a b. x\<in>closed_int c d" by auto
    2.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)
    2.99 -  with ac have "c\<le>b \<and> b\<le>d" by simp
   2.100 -  thus ?thesis by auto
   2.101 -qed
   2.102 -
   2.103 -
   2.104 -subsection {* Nested Interval Property *}
   2.105 -
   2.106 -theorem NIP:
   2.107 -  fixes f::"nat \<Rightarrow> real set"
   2.108 -  assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
   2.109 -  and closed: "\<forall>n. \<exists>a b. f n = closed_int a b \<and> a \<le> b"
   2.110 -  shows "(\<Inter>n. f n) \<noteq> {}"
   2.111 -proof -
   2.112 -  let ?g = "\<lambda>n. (SOME c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x))"
   2.113 -  have ne: "\<forall>n. \<exists>x. x\<in>(f n)"
   2.114 -  proof
   2.115 -    fix n
   2.116 -    from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" by simp
   2.117 -    then obtain a and b where fn: "f n = closed_int a b \<and> a \<le> b" by auto
   2.118 -    hence "a \<le> b" ..
   2.119 -    with closed_not_empty have "\<exists>x. x\<in>closed_int a b" by simp
   2.120 -    with fn show "\<exists>x. x\<in>(f n)" by simp
   2.121 -  qed
   2.122 -
   2.123 -  have gdef: "\<forall>n. (?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)"
   2.124 -  proof
   2.125 -    fix n
   2.126 -    from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
   2.127 -    then obtain a and b where ff: "f n = closed_int a b" and "a \<le> b" by auto
   2.128 -    hence "a \<le> b" by simp
   2.129 -    hence "a\<in>closed_int a b \<and> (\<forall>x\<in>closed_int a b. a \<le> x)" by (rule closed_int_least)
   2.130 -    with ff have "a\<in>(f n) \<and> (\<forall>x\<in>(f n). a \<le> x)" by simp
   2.131 -    hence "\<exists>c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x)" ..
   2.132 -    thus "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by (rule someI_ex)
   2.133 -  qed
   2.134 -
   2.135 -  -- "A denotes the set of all left-most points of all the intervals ..."
   2.136 -  moreover obtain A where Adef: "A = ?g ` \<nat>" by simp
   2.137 -  ultimately have "\<exists>x. x\<in>A"
   2.138 -  proof -
   2.139 -    have "(0::nat) \<in> \<nat>" by simp
   2.140 -    moreover have "?g 0 = ?g 0" by simp
   2.141 -    ultimately have "?g 0 \<in> ?g ` \<nat>" by (rule  rev_image_eqI)
   2.142 -    with Adef have "?g 0 \<in> A" by simp
   2.143 -    thus ?thesis ..
   2.144 -  qed
   2.145 -
   2.146 -  -- "Now show that A is bounded above ..."
   2.147 -  moreover have "\<exists>y. isUb (UNIV::real set) A y"
   2.148 -  proof -
   2.149 -    {
   2.150 -      fix n
   2.151 -      from ne have ex: "\<exists>x. x\<in>(f n)" ..
   2.152 -      from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
   2.153 -      moreover
   2.154 -      from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
   2.155 -      then obtain a and b where "f n = closed_int a b \<and> a \<le> b" by auto
   2.156 -      hence "b\<in>(f n) \<and> (\<forall>x\<in>(f n). x \<le> b)" using closed_int_most by blast
   2.157 -      ultimately have "\<forall>x\<in>(f n). (?g n) \<le> b" by simp
   2.158 -      with ex have "(?g n) \<le> b" by auto
   2.159 -      hence "\<exists>b. (?g n) \<le> b" by auto
   2.160 -    }
   2.161 -    hence aux: "\<forall>n. \<exists>b. (?g n) \<le> b" ..
   2.162 -
   2.163 -    have fs: "\<forall>n::nat. f n \<subseteq> f 0"
   2.164 -    proof (rule allI, induct_tac n)
   2.165 -      show "f 0 \<subseteq> f 0" by simp
   2.166 -    next
   2.167 -      fix n
   2.168 -      assume "f n \<subseteq> f 0"
   2.169 -      moreover from subset have "f (Suc n) \<subseteq> f n" ..
   2.170 -      ultimately show "f (Suc n) \<subseteq> f 0" by simp
   2.171 -    qed
   2.172 -    have "\<forall>n. (?g n)\<in>(f 0)"
   2.173 -    proof
   2.174 -      fix n
   2.175 -      from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
   2.176 -      hence "?g n \<in> f n" ..
   2.177 -      with fs show "?g n \<in> f 0" by auto
   2.178 -    qed
   2.179 -    moreover from closed
   2.180 -      obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast
   2.181 -    ultimately have "\<forall>n. ?g n \<in> closed_int a b" by auto
   2.182 -    with alb have "\<forall>n. ?g n \<le> b" using closed_int_most by blast
   2.183 -    with Adef have "\<forall>y\<in>A. y\<le>b" by auto
   2.184 -    hence "A *<= b" by (unfold setle_def)
   2.185 -    moreover have "b \<in> (UNIV::real set)" by simp
   2.186 -    ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
   2.187 -    hence "isUb (UNIV::real set) A b" by (unfold isUb_def)
   2.188 -    thus ?thesis by auto
   2.189 -  qed
   2.190 -  -- "by the Axiom Of Completeness, A has a least upper bound ..."
   2.191 -  ultimately have "\<exists>t. isLub UNIV A t" by (rule reals_complete)
   2.192 -
   2.193 -  -- "denote this least upper bound as t ..."
   2.194 -  then obtain t where tdef: "isLub UNIV A t" ..
   2.195 -
   2.196 -  -- "and finally show that this least upper bound is in all the intervals..."
   2.197 -  have "\<forall>n. t \<in> f n"
   2.198 -  proof
   2.199 -    fix n::nat
   2.200 -    from closed obtain a and b where
   2.201 -      int: "f n = closed_int a b" and alb: "a \<le> b" by blast
   2.202 -
   2.203 -    have "t \<ge> a"
   2.204 -    proof -
   2.205 -      have "a \<in> A"
   2.206 -      proof -
   2.207 -          (* by construction *)
   2.208 -        from alb int have ain: "a\<in>f n \<and> (\<forall>x\<in>f n. a \<le> x)"
   2.209 -          using closed_int_least by blast
   2.210 -        moreover have "\<forall>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<longrightarrow> e = a"
   2.211 -        proof clarsimp
   2.212 -          fix e
   2.213 -          assume ein: "e \<in> f n" and lt: "\<forall>x\<in>f n. e \<le> x"
   2.214 -          from lt ain have aux: "\<forall>x\<in>f n. a \<le> x \<and> e \<le> x" by auto
   2.215 -  
   2.216 -          from ein aux have "a \<le> e \<and> e \<le> e" by auto
   2.217 -          moreover from ain aux have "a \<le> a \<and> e \<le> a" by auto
   2.218 -          ultimately show "e = a" by simp
   2.219 -        qed
   2.220 -        hence "\<And>e.  e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<Longrightarrow> e = a" by simp
   2.221 -        ultimately have "(?g n) = a" by (rule some_equality)
   2.222 -        moreover
   2.223 -        {
   2.224 -          have "n = of_nat n" by simp
   2.225 -          moreover have "of_nat n \<in> \<nat>" by simp
   2.226 -          ultimately have "n \<in> \<nat>"
   2.227 -            apply -
   2.228 -            apply (subst(asm) eq_sym_conv)
   2.229 -            apply (erule subst)
   2.230 -            .
   2.231 -        }
   2.232 -        with Adef have "(?g n) \<in> A" by auto
   2.233 -        ultimately show ?thesis by simp
   2.234 -      qed 
   2.235 -      with tdef show "a \<le> t" by (rule isLubD2)
   2.236 -    qed
   2.237 -    moreover have "t \<le> b"
   2.238 -    proof -
   2.239 -      have "isUb UNIV A b"
   2.240 -      proof -
   2.241 -        {
   2.242 -          from alb int have
   2.243 -            ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
   2.244 -          
   2.245 -          have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
   2.246 -          proof (rule allI, induct_tac m)
   2.247 -            show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
   2.248 -          next
   2.249 -            fix m n
   2.250 -            assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
   2.251 -            {
   2.252 -              fix p
   2.253 -              from pp have "f (p + n) \<subseteq> f p" by simp
   2.254 -              moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
   2.255 -              hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
   2.256 -              ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
   2.257 -            }
   2.258 -            thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
   2.259 -          qed 
   2.260 -          have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
   2.261 -          proof ((rule allI)+, rule impI)
   2.262 -            fix \<alpha>::nat and \<beta>::nat
   2.263 -            assume "\<beta> \<le> \<alpha>"
   2.264 -            hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
   2.265 -            then obtain k where "\<alpha> = \<beta> + k" ..
   2.266 -            moreover
   2.267 -            from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
   2.268 -            ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
   2.269 -          qed 
   2.270 -          
   2.271 -          fix m   
   2.272 -          {
   2.273 -            assume "m \<ge> n"
   2.274 -            with subsetm have "f m \<subseteq> f n" by simp
   2.275 -            with ain have "\<forall>x\<in>f m. x \<le> b" by auto
   2.276 -            moreover
   2.277 -            from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
   2.278 -            ultimately have "?g m \<le> b" by auto
   2.279 -          }
   2.280 -          moreover
   2.281 -          {
   2.282 -            assume "\<not>(m \<ge> n)"
   2.283 -            hence "m < n" by simp
   2.284 -            with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
   2.285 -            from closed obtain ma and mb where
   2.286 -              "f m = closed_int ma mb \<and> ma \<le> mb" by blast
   2.287 -            hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto 
   2.288 -            from one alb sub fm int have "ma \<le> b" using closed_subset by blast
   2.289 -            moreover have "(?g m) = ma"
   2.290 -            proof -
   2.291 -              from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
   2.292 -              moreover from one have
   2.293 -                "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
   2.294 -                by (rule closed_int_least)
   2.295 -              with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
   2.296 -              ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
   2.297 -              thus "?g m = ma" by auto
   2.298 -            qed
   2.299 -            ultimately have "?g m \<le> b" by simp
   2.300 -          } 
   2.301 -          ultimately have "?g m \<le> b" by (rule case_split)
   2.302 -        }
   2.303 -        with Adef have "\<forall>y\<in>A. y\<le>b" by auto
   2.304 -        hence "A *<= b" by (unfold setle_def)
   2.305 -        moreover have "b \<in> (UNIV::real set)" by simp
   2.306 -        ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
   2.307 -        thus "isUb (UNIV::real set) A b" by (unfold isUb_def)
   2.308 -      qed
   2.309 -      with tdef show "t \<le> b" by (rule isLub_le_isUb)
   2.310 -    qed
   2.311 -    ultimately have "t \<in> closed_int a b" by (rule closed_mem)
   2.312 -    with int show "t \<in> f n" by simp
   2.313 -  qed
   2.314 -  hence "t \<in> (\<Inter>n. f n)" by auto
   2.315 -  thus ?thesis by auto
   2.316 -qed
   2.317 -
   2.318 -subsection {* Generating the intervals *}
   2.319 -
   2.320 -subsubsection {* Existence of non-singleton closed intervals *}
   2.321 -
   2.322 -text {* This lemma asserts that given any non-singleton closed
   2.323 -interval (a,b) and any element c, there exists a closed interval that
   2.324 -is a subset of (a,b) and that does not contain c and is a
   2.325 -non-singleton itself. *}
   2.326 -
   2.327 -lemma closed_subset_ex:
   2.328 -  fixes c::real
   2.329 -  assumes alb: "a < b"
   2.330 -  shows
   2.331 -    "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
   2.332 -proof -
   2.333 -  {
   2.334 -    assume clb: "c < b"
   2.335 -    {
   2.336 -      assume cla: "c < a"
   2.337 -      from alb cla clb have "c \<notin> closed_int a b" by (unfold closed_int_def, auto)
   2.338 -      with alb have
   2.339 -        "a < b \<and> closed_int a b \<subseteq> closed_int a b \<and> c \<notin> closed_int a b"
   2.340 -        by auto
   2.341 -      hence
   2.342 -        "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
   2.343 -        by auto
   2.344 -    }
   2.345 -    moreover
   2.346 -    {
   2.347 -      assume ncla: "\<not>(c < a)"
   2.348 -      with clb have cdef: "a \<le> c \<and> c < b" by simp
   2.349 -      obtain ka where kadef: "ka = (c + b)/2" by blast
   2.350 -
   2.351 -      from kadef clb have kalb: "ka < b" by auto
   2.352 -      moreover from kadef cdef have kagc: "ka > c" by simp
   2.353 -      ultimately have "c\<notin>(closed_int ka b)" by (unfold closed_int_def, auto)
   2.354 -      moreover from cdef kagc have "ka \<ge> a" by simp
   2.355 -      hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
   2.356 -      ultimately have
   2.357 -        "ka < b  \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b"
   2.358 -        using kalb by auto
   2.359 -      hence
   2.360 -        "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
   2.361 -        by auto
   2.362 -
   2.363 -    }
   2.364 -    ultimately have
   2.365 -      "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
   2.366 -      by (rule case_split)
   2.367 -  }
   2.368 -  moreover
   2.369 -  {
   2.370 -    assume "\<not> (c < b)"
   2.371 -    hence cgeb: "c \<ge> b" by simp
   2.372 -
   2.373 -    obtain kb where kbdef: "kb = (a + b)/2" by blast
   2.374 -    with alb have kblb: "kb < b" by auto
   2.375 -    with kbdef cgeb have "a < kb \<and> kb < c" by auto
   2.376 -    moreover hence "c \<notin> (closed_int a kb)" by (unfold closed_int_def, auto)
   2.377 -    moreover from kblb have
   2.378 -      "closed_int a kb \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
   2.379 -    ultimately have
   2.380 -      "a < kb \<and>  closed_int a kb \<subseteq> closed_int a b \<and> c\<notin>closed_int a kb"
   2.381 -      by simp
   2.382 -    hence
   2.383 -      "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
   2.384 -      by auto
   2.385 -  }
   2.386 -  ultimately show ?thesis by (rule case_split)
   2.387 -qed
   2.388 -
   2.389 -subsection {* newInt: Interval generation *}
   2.390 -
   2.391 -text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
   2.392 -closed interval such that @{text "newInt (Suc n) f \<subseteq> newInt n f"} and
   2.393 -does not contain @{text "f (Suc n)"}. With the base case defined such
   2.394 -that @{text "(f 0)\<notin>newInt 0 f"}. *}
   2.395 -
   2.396 -subsubsection {* Definition *}
   2.397 -
   2.398 -primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
   2.399 -  "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"
   2.400 -  | "newInt (Suc n) f =
   2.401 -      (SOME e. (\<exists>e1 e2.
   2.402 -       e1 < e2 \<and>
   2.403 -       e = closed_int e1 e2 \<and>
   2.404 -       e \<subseteq> (newInt n f) \<and>
   2.405 -       (f (Suc n)) \<notin> e)
   2.406 -      )"
   2.407 -
   2.408 -declare newInt.simps [code del]
   2.409 -
   2.410 -subsubsection {* Properties *}
   2.411 -
   2.412 -text {* We now show that every application of newInt returns an
   2.413 -appropriate interval. *}
   2.414 -
   2.415 -lemma newInt_ex:
   2.416 -  "\<exists>a b. a < b \<and>
   2.417 -   newInt (Suc n) f = closed_int a b \<and>
   2.418 -   newInt (Suc n) f \<subseteq> newInt n f \<and>
   2.419 -   f (Suc n) \<notin> newInt (Suc n) f"
   2.420 -proof (induct n)
   2.421 -  case 0
   2.422 -
   2.423 -  let ?e = "SOME e. \<exists>e1 e2.
   2.424 -   e1 < e2 \<and>
   2.425 -   e = closed_int e1 e2 \<and>
   2.426 -   e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
   2.427 -   f (Suc 0) \<notin> e"
   2.428 -
   2.429 -  have "newInt (Suc 0) f = ?e" by auto
   2.430 -  moreover
   2.431 -  have "f 0 + 1 < f 0 + 2" by simp
   2.432 -  with closed_subset_ex have
   2.433 -    "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
   2.434 -     f (Suc 0) \<notin> (closed_int ka kb)" .
   2.435 -  hence
   2.436 -    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
   2.437 -     e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> e" by simp
   2.438 -  hence
   2.439 -    "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
   2.440 -     ?e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> ?e"
   2.441 -    by (rule someI_ex)
   2.442 -  ultimately have "\<exists>e1 e2. e1 < e2 \<and>
   2.443 -   newInt (Suc 0) f = closed_int e1 e2 \<and>
   2.444 -   newInt (Suc 0) f \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
   2.445 -   f (Suc 0) \<notin> newInt (Suc 0) f" by simp
   2.446 -  thus
   2.447 -    "\<exists>a b. a < b \<and> newInt (Suc 0) f = closed_int a b \<and>
   2.448 -     newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
   2.449 -    by simp
   2.450 -next
   2.451 -  case (Suc n)
   2.452 -  hence "\<exists>a b.
   2.453 -   a < b \<and>
   2.454 -   newInt (Suc n) f = closed_int a b \<and>
   2.455 -   newInt (Suc n) f \<subseteq> newInt n f \<and>
   2.456 -   f (Suc n) \<notin> newInt (Suc n) f" by simp
   2.457 -  then obtain a and b where ab: "a < b \<and>
   2.458 -   newInt (Suc n) f = closed_int a b \<and>
   2.459 -   newInt (Suc n) f \<subseteq> newInt n f \<and>
   2.460 -   f (Suc n) \<notin> newInt (Suc n) f" by auto
   2.461 -  hence cab: "closed_int a b = newInt (Suc n) f" by simp
   2.462 -
   2.463 -  let ?e = "SOME e. \<exists>e1 e2.
   2.464 -    e1 < e2 \<and>
   2.465 -    e = closed_int e1 e2 \<and>
   2.466 -    e \<subseteq> closed_int a b \<and>
   2.467 -    f (Suc (Suc n)) \<notin> e"
   2.468 -  from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto
   2.469 -
   2.470 -  from ab have "a < b" by simp
   2.471 -  with closed_subset_ex have
   2.472 -    "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and>
   2.473 -     f (Suc (Suc n)) \<notin> closed_int ka kb" .
   2.474 -  hence
   2.475 -    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
   2.476 -     closed_int ka kb \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> closed_int ka kb"
   2.477 -    by simp
   2.478 -  hence
   2.479 -    "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
   2.480 -     e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> e" by simp
   2.481 -  hence
   2.482 -    "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
   2.483 -     ?e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
   2.484 -  with ab ni show
   2.485 -    "\<exists>ka kb. ka < kb \<and>
   2.486 -     newInt (Suc (Suc n)) f = closed_int ka kb \<and>
   2.487 -     newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
   2.488 -     f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto
   2.489 -qed
   2.490 -
   2.491 -lemma newInt_subset:
   2.492 -  "newInt (Suc n) f \<subseteq> newInt n f"
   2.493 -  using newInt_ex by auto
   2.494 -
   2.495 -
   2.496 -text {* Another fundamental property is that no element in the range
   2.497 -of f is in the intersection of all closed intervals generated by
   2.498 -newInt. *}
   2.499 -
   2.500 -lemma newInt_inter:
   2.501 -  "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
   2.502 -proof
   2.503 -  fix n::nat
   2.504 -  {
   2.505 -    assume n0: "n = 0"
   2.506 -    moreover have "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)" by simp
   2.507 -    ultimately have "f n \<notin> newInt n f" by (unfold closed_int_def, simp)
   2.508 -  }
   2.509 -  moreover
   2.510 -  {
   2.511 -    assume "\<not> n = 0"
   2.512 -    hence "n > 0" by simp
   2.513 -    then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc)
   2.514 -
   2.515 -    from newInt_ex have
   2.516 -      "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
   2.517 -       newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
   2.518 -    then have "f (Suc m) \<notin> newInt (Suc m) f" by auto
   2.519 -    with ndef have "f n \<notin> newInt n f" by simp
   2.520 -  }
   2.521 -  ultimately have "f n \<notin> newInt n f" by (rule case_split)
   2.522 -  thus "f n \<notin> (\<Inter>n. newInt n f)" by auto
   2.523 -qed
   2.524 -
   2.525 -
   2.526 -lemma newInt_notempty:
   2.527 -  "(\<Inter>n. newInt n f) \<noteq> {}"
   2.528 -proof -
   2.529 -  let ?g = "\<lambda>n. newInt n f"
   2.530 -  have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
   2.531 -  proof
   2.532 -    fix n
   2.533 -    show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)
   2.534 -  qed
   2.535 -  moreover have "\<forall>n. \<exists>a b. ?g n = closed_int a b \<and> a \<le> b"
   2.536 -  proof
   2.537 -    fix n::nat
   2.538 -    {
   2.539 -      assume "n = 0"
   2.540 -      then have
   2.541 -        "?g n = closed_int (f 0 + 1) (f 0 + 2) \<and> (f 0 + 1 \<le> f 0 + 2)"
   2.542 -        by simp
   2.543 -      hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
   2.544 -    }
   2.545 -    moreover
   2.546 -    {
   2.547 -      assume "\<not> n = 0"
   2.548 -      then have "n > 0" by simp
   2.549 -      then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)
   2.550 -
   2.551 -      have
   2.552 -        "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
   2.553 -        (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
   2.554 -        by (rule newInt_ex)
   2.555 -      then obtain a and b where
   2.556 -        "a < b \<and> (newInt (Suc m) f) = closed_int a b" by auto
   2.557 -      with nd have "?g n = closed_int a b \<and> a \<le> b" by auto
   2.558 -      hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
   2.559 -    }
   2.560 -    ultimately show "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by (rule case_split)
   2.561 -  qed
   2.562 -  ultimately show ?thesis by (rule NIP)
   2.563 -qed
   2.564 -
   2.565 -
   2.566 -subsection {* Final Theorem *}
   2.567 -
   2.568 -theorem real_non_denum:
   2.569 -  shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
   2.570 -proof -- "by contradiction"
   2.571 -  assume "\<exists>f::nat\<Rightarrow>real. surj f"
   2.572 -  then obtain f::"nat\<Rightarrow>real" where "surj f" by auto
   2.573 -  hence rangeF: "range f = UNIV" by (rule surj_range)
   2.574 -  -- "We now produce a real number x that is not in the range of f, using the properties of newInt. "
   2.575 -  have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
   2.576 -  moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
   2.577 -  ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast
   2.578 -  moreover from rangeF have "x \<in> range f" by simp
   2.579 -  ultimately show False by blast
   2.580 -qed
   2.581 -
   2.582 -end
     3.1 --- a/src/HOL/IsaMakefile	Thu Dec 04 14:17:36 2008 +0100
     3.2 +++ b/src/HOL/IsaMakefile	Wed Dec 10 10:23:47 2008 +0100
     3.3 @@ -274,7 +274,6 @@
     3.4    Order_Relation.thy \
     3.5    Parity.thy \
     3.6    Univ_Poly.thy \
     3.7 -  ContNotDenum.thy \
     3.8    Lubs.thy \
     3.9    PReal.thy \
    3.10    Rational.thy \
    3.11 @@ -299,7 +298,7 @@
    3.12  
    3.13  $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/SetsAndFunctions.thy		\
    3.14    Library/Abstract_Rat.thy \
    3.15 -  Library/BigO.thy Library/Ramsey.thy Library/Efficient_Nat.thy		\
    3.16 +  Library/BigO.thy Library/ContNotDenum.thy Library/Efficient_Nat.thy	\
    3.17    Library/Executable_Set.thy Library/Infinite_Set.thy			\
    3.18    Library/FuncSet.thy			\
    3.19    Library/Library.thy Library/List_Prefix.thy Library/State_Monad.thy	\
    3.20 @@ -307,7 +306,7 @@
    3.21    Library/Primes.thy Library/Pocklington.thy Library/Quotient.thy	\
    3.22    Library/Quicksort.thy Library/Nat_Infinity.thy Library/Word.thy	\
    3.23    Library/README.html Library/Continuity.thy				\
    3.24 -  Library/Nested_Environment.thy Library/Zorn.thy			\
    3.25 +  Library/Nested_Environment.thy Library/Ramsey.thy Library/Zorn.thy	\
    3.26    Library/Library/ROOT.ML Library/Library/document/root.tex		\
    3.27    Library/Library/document/root.bib Library/While_Combinator.thy	\
    3.28    Library/Product_ord.thy Library/Char_nat.thy Library/Char_ord.thy	\
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/ContNotDenum.thy	Wed Dec 10 10:23:47 2008 +0100
     4.3 @@ -0,0 +1,579 @@
     4.4 +(*  Title       : HOL/ContNonDenum
     4.5 +    Author      : Benjamin Porter, Monash University, NICTA, 2005
     4.6 +*)
     4.7 +
     4.8 +header {* Non-denumerability of the Continuum. *}
     4.9 +
    4.10 +theory ContNotDenum
    4.11 +imports RComplete Hilbert_Choice
    4.12 +begin
    4.13 +
    4.14 +subsection {* Abstract *}
    4.15 +
    4.16 +text {* The following document presents a proof that the Continuum is
    4.17 +uncountable. It is formalised in the Isabelle/Isar theorem proving
    4.18 +system.
    4.19 +
    4.20 +{\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other
    4.21 +words, there does not exist a function f:@{text "\<nat>\<Rightarrow>\<real>"} such that f is
    4.22 +surjective.
    4.23 +
    4.24 +{\em Outline:} An elegant informal proof of this result uses Cantor's
    4.25 +Diagonalisation argument. The proof presented here is not this
    4.26 +one. First we formalise some properties of closed intervals, then we
    4.27 +prove the Nested Interval Property. This property relies on the
    4.28 +completeness of the Real numbers and is the foundation for our
    4.29 +argument. Informally it states that an intersection of countable
    4.30 +closed intervals (where each successive interval is a subset of the
    4.31 +last) is non-empty. We then assume a surjective function f:@{text
    4.32 +"\<nat>\<Rightarrow>\<real>"} exists and find a real x such that x is not in the range of f
    4.33 +by generating a sequence of closed intervals then using the NIP. *}
    4.34 +
    4.35 +subsection {* Closed Intervals *}
    4.36 +
    4.37 +text {* This section formalises some properties of closed intervals. *}
    4.38 +
    4.39 +subsubsection {* Definition *}
    4.40 +
    4.41 +definition
    4.42 +  closed_int :: "real \<Rightarrow> real \<Rightarrow> real set" where
    4.43 +  "closed_int x y = {z. x \<le> z \<and> z \<le> y}"
    4.44 +
    4.45 +subsubsection {* Properties *}
    4.46 +
    4.47 +lemma closed_int_subset:
    4.48 +  assumes xy: "x1 \<ge> x0" "y1 \<le> y0"
    4.49 +  shows "closed_int x1 y1 \<subseteq> closed_int x0 y0"
    4.50 +proof -
    4.51 +  {
    4.52 +    fix x::real
    4.53 +    assume "x \<in> closed_int x1 y1"
    4.54 +    hence "x \<ge> x1 \<and> x \<le> y1" by (simp add: closed_int_def)
    4.55 +    with xy have "x \<ge> x0 \<and> x \<le> y0" by auto
    4.56 +    hence "x \<in> closed_int x0 y0" by (simp add: closed_int_def)
    4.57 +  }
    4.58 +  thus ?thesis by auto
    4.59 +qed
    4.60 +
    4.61 +lemma closed_int_least:
    4.62 +  assumes a: "a \<le> b"
    4.63 +  shows "a \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. a \<le> x)"
    4.64 +proof
    4.65 +  from a have "a\<in>{x. a\<le>x \<and> x\<le>b}" by simp
    4.66 +  thus "a \<in> closed_int a b" by (unfold closed_int_def)
    4.67 +next
    4.68 +  have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. a\<le>x" by simp
    4.69 +  thus "\<forall>x \<in> closed_int a b. a \<le> x" by (unfold closed_int_def)
    4.70 +qed
    4.71 +
    4.72 +lemma closed_int_most:
    4.73 +  assumes a: "a \<le> b"
    4.74 +  shows "b \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. x \<le> b)"
    4.75 +proof
    4.76 +  from a have "b\<in>{x. a\<le>x \<and> x\<le>b}" by simp
    4.77 +  thus "b \<in> closed_int a b" by (unfold closed_int_def)
    4.78 +next
    4.79 +  have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. x\<le>b" by simp
    4.80 +  thus "\<forall>x \<in> closed_int a b. x\<le>b" by (unfold closed_int_def)
    4.81 +qed
    4.82 +
    4.83 +lemma closed_not_empty:
    4.84 +  shows "a \<le> b \<Longrightarrow> \<exists>x. x \<in> closed_int a b" 
    4.85 +  by (auto dest: closed_int_least)
    4.86 +
    4.87 +lemma closed_mem:
    4.88 +  assumes "a \<le> c" and "c \<le> b"
    4.89 +  shows "c \<in> closed_int a b"
    4.90 +  using assms unfolding closed_int_def by auto
    4.91 +
    4.92 +lemma closed_subset:
    4.93 +  assumes ac: "a \<le> b"  "c \<le> d" 
    4.94 +  assumes closed: "closed_int a b \<subseteq> closed_int c d"
    4.95 +  shows "b \<ge> c"
    4.96 +proof -
    4.97 +  from closed have "\<forall>x\<in>closed_int a b. x\<in>closed_int c d" by auto
    4.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)
    4.99 +  with ac have "c\<le>b \<and> b\<le>d" by simp
   4.100 +  thus ?thesis by auto
   4.101 +qed
   4.102 +
   4.103 +
   4.104 +subsection {* Nested Interval Property *}
   4.105 +
   4.106 +theorem NIP:
   4.107 +  fixes f::"nat \<Rightarrow> real set"
   4.108 +  assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
   4.109 +  and closed: "\<forall>n. \<exists>a b. f n = closed_int a b \<and> a \<le> b"
   4.110 +  shows "(\<Inter>n. f n) \<noteq> {}"
   4.111 +proof -
   4.112 +  let ?g = "\<lambda>n. (SOME c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x))"
   4.113 +  have ne: "\<forall>n. \<exists>x. x\<in>(f n)"
   4.114 +  proof
   4.115 +    fix n
   4.116 +    from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" by simp
   4.117 +    then obtain a and b where fn: "f n = closed_int a b \<and> a \<le> b" by auto
   4.118 +    hence "a \<le> b" ..
   4.119 +    with closed_not_empty have "\<exists>x. x\<in>closed_int a b" by simp
   4.120 +    with fn show "\<exists>x. x\<in>(f n)" by simp
   4.121 +  qed
   4.122 +
   4.123 +  have gdef: "\<forall>n. (?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)"
   4.124 +  proof
   4.125 +    fix n
   4.126 +    from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
   4.127 +    then obtain a and b where ff: "f n = closed_int a b" and "a \<le> b" by auto
   4.128 +    hence "a \<le> b" by simp
   4.129 +    hence "a\<in>closed_int a b \<and> (\<forall>x\<in>closed_int a b. a \<le> x)" by (rule closed_int_least)
   4.130 +    with ff have "a\<in>(f n) \<and> (\<forall>x\<in>(f n). a \<le> x)" by simp
   4.131 +    hence "\<exists>c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x)" ..
   4.132 +    thus "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by (rule someI_ex)
   4.133 +  qed
   4.134 +
   4.135 +  -- "A denotes the set of all left-most points of all the intervals ..."
   4.136 +  moreover obtain A where Adef: "A = ?g ` \<nat>" by simp
   4.137 +  ultimately have "\<exists>x. x\<in>A"
   4.138 +  proof -
   4.139 +    have "(0::nat) \<in> \<nat>" by simp
   4.140 +    moreover have "?g 0 = ?g 0" by simp
   4.141 +    ultimately have "?g 0 \<in> ?g ` \<nat>" by (rule  rev_image_eqI)
   4.142 +    with Adef have "?g 0 \<in> A" by simp
   4.143 +    thus ?thesis ..
   4.144 +  qed
   4.145 +
   4.146 +  -- "Now show that A is bounded above ..."
   4.147 +  moreover have "\<exists>y. isUb (UNIV::real set) A y"
   4.148 +  proof -
   4.149 +    {
   4.150 +      fix n
   4.151 +      from ne have ex: "\<exists>x. x\<in>(f n)" ..
   4.152 +      from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
   4.153 +      moreover
   4.154 +      from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
   4.155 +      then obtain a and b where "f n = closed_int a b \<and> a \<le> b" by auto
   4.156 +      hence "b\<in>(f n) \<and> (\<forall>x\<in>(f n). x \<le> b)" using closed_int_most by blast
   4.157 +      ultimately have "\<forall>x\<in>(f n). (?g n) \<le> b" by simp
   4.158 +      with ex have "(?g n) \<le> b" by auto
   4.159 +      hence "\<exists>b. (?g n) \<le> b" by auto
   4.160 +    }
   4.161 +    hence aux: "\<forall>n. \<exists>b. (?g n) \<le> b" ..
   4.162 +
   4.163 +    have fs: "\<forall>n::nat. f n \<subseteq> f 0"
   4.164 +    proof (rule allI, induct_tac n)
   4.165 +      show "f 0 \<subseteq> f 0" by simp
   4.166 +    next
   4.167 +      fix n
   4.168 +      assume "f n \<subseteq> f 0"
   4.169 +      moreover from subset have "f (Suc n) \<subseteq> f n" ..
   4.170 +      ultimately show "f (Suc n) \<subseteq> f 0" by simp
   4.171 +    qed
   4.172 +    have "\<forall>n. (?g n)\<in>(f 0)"
   4.173 +    proof
   4.174 +      fix n
   4.175 +      from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
   4.176 +      hence "?g n \<in> f n" ..
   4.177 +      with fs show "?g n \<in> f 0" by auto
   4.178 +    qed
   4.179 +    moreover from closed
   4.180 +      obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast
   4.181 +    ultimately have "\<forall>n. ?g n \<in> closed_int a b" by auto
   4.182 +    with alb have "\<forall>n. ?g n \<le> b" using closed_int_most by blast
   4.183 +    with Adef have "\<forall>y\<in>A. y\<le>b" by auto
   4.184 +    hence "A *<= b" by (unfold setle_def)
   4.185 +    moreover have "b \<in> (UNIV::real set)" by simp
   4.186 +    ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
   4.187 +    hence "isUb (UNIV::real set) A b" by (unfold isUb_def)
   4.188 +    thus ?thesis by auto
   4.189 +  qed
   4.190 +  -- "by the Axiom Of Completeness, A has a least upper bound ..."
   4.191 +  ultimately have "\<exists>t. isLub UNIV A t" by (rule reals_complete)
   4.192 +
   4.193 +  -- "denote this least upper bound as t ..."
   4.194 +  then obtain t where tdef: "isLub UNIV A t" ..
   4.195 +
   4.196 +  -- "and finally show that this least upper bound is in all the intervals..."
   4.197 +  have "\<forall>n. t \<in> f n"
   4.198 +  proof
   4.199 +    fix n::nat
   4.200 +    from closed obtain a and b where
   4.201 +      int: "f n = closed_int a b" and alb: "a \<le> b" by blast
   4.202 +
   4.203 +    have "t \<ge> a"
   4.204 +    proof -
   4.205 +      have "a \<in> A"
   4.206 +      proof -
   4.207 +          (* by construction *)
   4.208 +        from alb int have ain: "a\<in>f n \<and> (\<forall>x\<in>f n. a \<le> x)"
   4.209 +          using closed_int_least by blast
   4.210 +        moreover have "\<forall>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<longrightarrow> e = a"
   4.211 +        proof clarsimp
   4.212 +          fix e
   4.213 +          assume ein: "e \<in> f n" and lt: "\<forall>x\<in>f n. e \<le> x"
   4.214 +          from lt ain have aux: "\<forall>x\<in>f n. a \<le> x \<and> e \<le> x" by auto
   4.215 +  
   4.216 +          from ein aux have "a \<le> e \<and> e \<le> e" by auto
   4.217 +          moreover from ain aux have "a \<le> a \<and> e \<le> a" by auto
   4.218 +          ultimately show "e = a" by simp
   4.219 +        qed
   4.220 +        hence "\<And>e.  e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<Longrightarrow> e = a" by simp
   4.221 +        ultimately have "(?g n) = a" by (rule some_equality)
   4.222 +        moreover
   4.223 +        {
   4.224 +          have "n = of_nat n" by simp
   4.225 +          moreover have "of_nat n \<in> \<nat>" by simp
   4.226 +          ultimately have "n \<in> \<nat>"
   4.227 +            apply -
   4.228 +            apply (subst(asm) eq_sym_conv)
   4.229 +            apply (erule subst)
   4.230 +            .
   4.231 +        }
   4.232 +        with Adef have "(?g n) \<in> A" by auto
   4.233 +        ultimately show ?thesis by simp
   4.234 +      qed 
   4.235 +      with tdef show "a \<le> t" by (rule isLubD2)
   4.236 +    qed
   4.237 +    moreover have "t \<le> b"
   4.238 +    proof -
   4.239 +      have "isUb UNIV A b"
   4.240 +      proof -
   4.241 +        {
   4.242 +          from alb int have
   4.243 +            ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
   4.244 +          
   4.245 +          have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
   4.246 +          proof (rule allI, induct_tac m)
   4.247 +            show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
   4.248 +          next
   4.249 +            fix m n
   4.250 +            assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
   4.251 +            {
   4.252 +              fix p
   4.253 +              from pp have "f (p + n) \<subseteq> f p" by simp
   4.254 +              moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
   4.255 +              hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
   4.256 +              ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
   4.257 +            }
   4.258 +            thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
   4.259 +          qed 
   4.260 +          have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
   4.261 +          proof ((rule allI)+, rule impI)
   4.262 +            fix \<alpha>::nat and \<beta>::nat
   4.263 +            assume "\<beta> \<le> \<alpha>"
   4.264 +            hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
   4.265 +            then obtain k where "\<alpha> = \<beta> + k" ..
   4.266 +            moreover
   4.267 +            from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
   4.268 +            ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
   4.269 +          qed 
   4.270 +          
   4.271 +          fix m   
   4.272 +          {
   4.273 +            assume "m \<ge> n"
   4.274 +            with subsetm have "f m \<subseteq> f n" by simp
   4.275 +            with ain have "\<forall>x\<in>f m. x \<le> b" by auto
   4.276 +            moreover
   4.277 +            from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
   4.278 +            ultimately have "?g m \<le> b" by auto
   4.279 +          }
   4.280 +          moreover
   4.281 +          {
   4.282 +            assume "\<not>(m \<ge> n)"
   4.283 +            hence "m < n" by simp
   4.284 +            with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
   4.285 +            from closed obtain ma and mb where
   4.286 +              "f m = closed_int ma mb \<and> ma \<le> mb" by blast
   4.287 +            hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto 
   4.288 +            from one alb sub fm int have "ma \<le> b" using closed_subset by blast
   4.289 +            moreover have "(?g m) = ma"
   4.290 +            proof -
   4.291 +              from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
   4.292 +              moreover from one have
   4.293 +                "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
   4.294 +                by (rule closed_int_least)
   4.295 +              with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
   4.296 +              ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
   4.297 +              thus "?g m = ma" by auto
   4.298 +            qed
   4.299 +            ultimately have "?g m \<le> b" by simp
   4.300 +          } 
   4.301 +          ultimately have "?g m \<le> b" by (rule case_split)
   4.302 +        }
   4.303 +        with Adef have "\<forall>y\<in>A. y\<le>b" by auto
   4.304 +        hence "A *<= b" by (unfold setle_def)
   4.305 +        moreover have "b \<in> (UNIV::real set)" by simp
   4.306 +        ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
   4.307 +        thus "isUb (UNIV::real set) A b" by (unfold isUb_def)
   4.308 +      qed
   4.309 +      with tdef show "t \<le> b" by (rule isLub_le_isUb)
   4.310 +    qed
   4.311 +    ultimately have "t \<in> closed_int a b" by (rule closed_mem)
   4.312 +    with int show "t \<in> f n" by simp
   4.313 +  qed
   4.314 +  hence "t \<in> (\<Inter>n. f n)" by auto
   4.315 +  thus ?thesis by auto
   4.316 +qed
   4.317 +
   4.318 +subsection {* Generating the intervals *}
   4.319 +
   4.320 +subsubsection {* Existence of non-singleton closed intervals *}
   4.321 +
   4.322 +text {* This lemma asserts that given any non-singleton closed
   4.323 +interval (a,b) and any element c, there exists a closed interval that
   4.324 +is a subset of (a,b) and that does not contain c and is a
   4.325 +non-singleton itself. *}
   4.326 +
   4.327 +lemma closed_subset_ex:
   4.328 +  fixes c::real
   4.329 +  assumes alb: "a < b"
   4.330 +  shows
   4.331 +    "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
   4.332 +proof -
   4.333 +  {
   4.334 +    assume clb: "c < b"
   4.335 +    {
   4.336 +      assume cla: "c < a"
   4.337 +      from alb cla clb have "c \<notin> closed_int a b" by (unfold closed_int_def, auto)
   4.338 +      with alb have
   4.339 +        "a < b \<and> closed_int a b \<subseteq> closed_int a b \<and> c \<notin> closed_int a b"
   4.340 +        by auto
   4.341 +      hence
   4.342 +        "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
   4.343 +        by auto
   4.344 +    }
   4.345 +    moreover
   4.346 +    {
   4.347 +      assume ncla: "\<not>(c < a)"
   4.348 +      with clb have cdef: "a \<le> c \<and> c < b" by simp
   4.349 +      obtain ka where kadef: "ka = (c + b)/2" by blast
   4.350 +
   4.351 +      from kadef clb have kalb: "ka < b" by auto
   4.352 +      moreover from kadef cdef have kagc: "ka > c" by simp
   4.353 +      ultimately have "c\<notin>(closed_int ka b)" by (unfold closed_int_def, auto)
   4.354 +      moreover from cdef kagc have "ka \<ge> a" by simp
   4.355 +      hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
   4.356 +      ultimately have
   4.357 +        "ka < b  \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b"
   4.358 +        using kalb by auto
   4.359 +      hence
   4.360 +        "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
   4.361 +        by auto
   4.362 +
   4.363 +    }
   4.364 +    ultimately have
   4.365 +      "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
   4.366 +      by (rule case_split)
   4.367 +  }
   4.368 +  moreover
   4.369 +  {
   4.370 +    assume "\<not> (c < b)"
   4.371 +    hence cgeb: "c \<ge> b" by simp
   4.372 +
   4.373 +    obtain kb where kbdef: "kb = (a + b)/2" by blast
   4.374 +    with alb have kblb: "kb < b" by auto
   4.375 +    with kbdef cgeb have "a < kb \<and> kb < c" by auto
   4.376 +    moreover hence "c \<notin> (closed_int a kb)" by (unfold closed_int_def, auto)
   4.377 +    moreover from kblb have
   4.378 +      "closed_int a kb \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
   4.379 +    ultimately have
   4.380 +      "a < kb \<and>  closed_int a kb \<subseteq> closed_int a b \<and> c\<notin>closed_int a kb"
   4.381 +      by simp
   4.382 +    hence
   4.383 +      "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
   4.384 +      by auto
   4.385 +  }
   4.386 +  ultimately show ?thesis by (rule case_split)
   4.387 +qed
   4.388 +
   4.389 +subsection {* newInt: Interval generation *}
   4.390 +
   4.391 +text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
   4.392 +closed interval such that @{text "newInt (Suc n) f \<subseteq> newInt n f"} and
   4.393 +does not contain @{text "f (Suc n)"}. With the base case defined such
   4.394 +that @{text "(f 0)\<notin>newInt 0 f"}. *}
   4.395 +
   4.396 +subsubsection {* Definition *}
   4.397 +
   4.398 +primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
   4.399 +  "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"
   4.400 +  | "newInt (Suc n) f =
   4.401 +      (SOME e. (\<exists>e1 e2.
   4.402 +       e1 < e2 \<and>
   4.403 +       e = closed_int e1 e2 \<and>
   4.404 +       e \<subseteq> (newInt n f) \<and>
   4.405 +       (f (Suc n)) \<notin> e)
   4.406 +      )"
   4.407 +
   4.408 +declare newInt.simps [code del]
   4.409 +
   4.410 +subsubsection {* Properties *}
   4.411 +
   4.412 +text {* We now show that every application of newInt returns an
   4.413 +appropriate interval. *}
   4.414 +
   4.415 +lemma newInt_ex:
   4.416 +  "\<exists>a b. a < b \<and>
   4.417 +   newInt (Suc n) f = closed_int a b \<and>
   4.418 +   newInt (Suc n) f \<subseteq> newInt n f \<and>
   4.419 +   f (Suc n) \<notin> newInt (Suc n) f"
   4.420 +proof (induct n)
   4.421 +  case 0
   4.422 +
   4.423 +  let ?e = "SOME e. \<exists>e1 e2.
   4.424 +   e1 < e2 \<and>
   4.425 +   e = closed_int e1 e2 \<and>
   4.426 +   e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
   4.427 +   f (Suc 0) \<notin> e"
   4.428 +
   4.429 +  have "newInt (Suc 0) f = ?e" by auto
   4.430 +  moreover
   4.431 +  have "f 0 + 1 < f 0 + 2" by simp
   4.432 +  with closed_subset_ex have
   4.433 +    "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
   4.434 +     f (Suc 0) \<notin> (closed_int ka kb)" .
   4.435 +  hence
   4.436 +    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
   4.437 +     e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> e" by simp
   4.438 +  hence
   4.439 +    "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
   4.440 +     ?e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> ?e"
   4.441 +    by (rule someI_ex)
   4.442 +  ultimately have "\<exists>e1 e2. e1 < e2 \<and>
   4.443 +   newInt (Suc 0) f = closed_int e1 e2 \<and>
   4.444 +   newInt (Suc 0) f \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
   4.445 +   f (Suc 0) \<notin> newInt (Suc 0) f" by simp
   4.446 +  thus
   4.447 +    "\<exists>a b. a < b \<and> newInt (Suc 0) f = closed_int a b \<and>
   4.448 +     newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
   4.449 +    by simp
   4.450 +next
   4.451 +  case (Suc n)
   4.452 +  hence "\<exists>a b.
   4.453 +   a < b \<and>
   4.454 +   newInt (Suc n) f = closed_int a b \<and>
   4.455 +   newInt (Suc n) f \<subseteq> newInt n f \<and>
   4.456 +   f (Suc n) \<notin> newInt (Suc n) f" by simp
   4.457 +  then obtain a and b where ab: "a < b \<and>
   4.458 +   newInt (Suc n) f = closed_int a b \<and>
   4.459 +   newInt (Suc n) f \<subseteq> newInt n f \<and>
   4.460 +   f (Suc n) \<notin> newInt (Suc n) f" by auto
   4.461 +  hence cab: "closed_int a b = newInt (Suc n) f" by simp
   4.462 +
   4.463 +  let ?e = "SOME e. \<exists>e1 e2.
   4.464 +    e1 < e2 \<and>
   4.465 +    e = closed_int e1 e2 \<and>
   4.466 +    e \<subseteq> closed_int a b \<and>
   4.467 +    f (Suc (Suc n)) \<notin> e"
   4.468 +  from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto
   4.469 +
   4.470 +  from ab have "a < b" by simp
   4.471 +  with closed_subset_ex have
   4.472 +    "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and>
   4.473 +     f (Suc (Suc n)) \<notin> closed_int ka kb" .
   4.474 +  hence
   4.475 +    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
   4.476 +     closed_int ka kb \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> closed_int ka kb"
   4.477 +    by simp
   4.478 +  hence
   4.479 +    "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
   4.480 +     e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> e" by simp
   4.481 +  hence
   4.482 +    "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
   4.483 +     ?e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
   4.484 +  with ab ni show
   4.485 +    "\<exists>ka kb. ka < kb \<and>
   4.486 +     newInt (Suc (Suc n)) f = closed_int ka kb \<and>
   4.487 +     newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
   4.488 +     f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto
   4.489 +qed
   4.490 +
   4.491 +lemma newInt_subset:
   4.492 +  "newInt (Suc n) f \<subseteq> newInt n f"
   4.493 +  using newInt_ex by auto
   4.494 +
   4.495 +
   4.496 +text {* Another fundamental property is that no element in the range
   4.497 +of f is in the intersection of all closed intervals generated by
   4.498 +newInt. *}
   4.499 +
   4.500 +lemma newInt_inter:
   4.501 +  "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
   4.502 +proof
   4.503 +  fix n::nat
   4.504 +  {
   4.505 +    assume n0: "n = 0"
   4.506 +    moreover have "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)" by simp
   4.507 +    ultimately have "f n \<notin> newInt n f" by (unfold closed_int_def, simp)
   4.508 +  }
   4.509 +  moreover
   4.510 +  {
   4.511 +    assume "\<not> n = 0"
   4.512 +    hence "n > 0" by simp
   4.513 +    then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc)
   4.514 +
   4.515 +    from newInt_ex have
   4.516 +      "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
   4.517 +       newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
   4.518 +    then have "f (Suc m) \<notin> newInt (Suc m) f" by auto
   4.519 +    with ndef have "f n \<notin> newInt n f" by simp
   4.520 +  }
   4.521 +  ultimately have "f n \<notin> newInt n f" by (rule case_split)
   4.522 +  thus "f n \<notin> (\<Inter>n. newInt n f)" by auto
   4.523 +qed
   4.524 +
   4.525 +
   4.526 +lemma newInt_notempty:
   4.527 +  "(\<Inter>n. newInt n f) \<noteq> {}"
   4.528 +proof -
   4.529 +  let ?g = "\<lambda>n. newInt n f"
   4.530 +  have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
   4.531 +  proof
   4.532 +    fix n
   4.533 +    show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)
   4.534 +  qed
   4.535 +  moreover have "\<forall>n. \<exists>a b. ?g n = closed_int a b \<and> a \<le> b"
   4.536 +  proof
   4.537 +    fix n::nat
   4.538 +    {
   4.539 +      assume "n = 0"
   4.540 +      then have
   4.541 +        "?g n = closed_int (f 0 + 1) (f 0 + 2) \<and> (f 0 + 1 \<le> f 0 + 2)"
   4.542 +        by simp
   4.543 +      hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
   4.544 +    }
   4.545 +    moreover
   4.546 +    {
   4.547 +      assume "\<not> n = 0"
   4.548 +      then have "n > 0" by simp
   4.549 +      then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)
   4.550 +
   4.551 +      have
   4.552 +        "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
   4.553 +        (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
   4.554 +        by (rule newInt_ex)
   4.555 +      then obtain a and b where
   4.556 +        "a < b \<and> (newInt (Suc m) f) = closed_int a b" by auto
   4.557 +      with nd have "?g n = closed_int a b \<and> a \<le> b" by auto
   4.558 +      hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
   4.559 +    }
   4.560 +    ultimately show "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by (rule case_split)
   4.561 +  qed
   4.562 +  ultimately show ?thesis by (rule NIP)
   4.563 +qed
   4.564 +
   4.565 +
   4.566 +subsection {* Final Theorem *}
   4.567 +
   4.568 +theorem real_non_denum:
   4.569 +  shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
   4.570 +proof -- "by contradiction"
   4.571 +  assume "\<exists>f::nat\<Rightarrow>real. surj f"
   4.572 +  then obtain f::"nat\<Rightarrow>real" where "surj f" by auto
   4.573 +  hence rangeF: "range f = UNIV" by (rule surj_range)
   4.574 +  -- "We now produce a real number x that is not in the range of f, using the properties of newInt. "
   4.575 +  have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
   4.576 +  moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
   4.577 +  ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast
   4.578 +  moreover from rangeF have "x \<in> range f" by simp
   4.579 +  ultimately show False by blast
   4.580 +qed
   4.581 +
   4.582 +end
     5.1 --- a/src/HOL/Library/Library.thy	Thu Dec 04 14:17:36 2008 +0100
     5.2 +++ b/src/HOL/Library/Library.thy	Wed Dec 10 10:23:47 2008 +0100
     5.3 @@ -14,6 +14,7 @@
     5.4    Coinductive_List
     5.5    Commutative_Ring
     5.6    Continuity
     5.7 +  ContNotDenum
     5.8    Countable
     5.9    Dense_Linear_Order
    5.10    Efficient_Nat
     6.1 --- a/src/HOL/Real.thy	Thu Dec 04 14:17:36 2008 +0100
     6.2 +++ b/src/HOL/Real.thy	Wed Dec 10 10:23:47 2008 +0100
     6.3 @@ -1,5 +1,5 @@
     6.4  theory Real
     6.5 -imports ContNotDenum "~~/src/HOL/Real/RealVector"
     6.6 +imports "~~/src/HOL/Real/RealVector"
     6.7  begin
     6.8  
     6.9  end