* include generalised MVT in HyperReal (contributed by Benjamin Porter)
authorkleing
Sun Feb 12 12:29:01 2006 +0100 (2006-02-12)
changeset 190235652a536b7e8
parent 19022 0e6ec4fd204c
child 19024 80eb6640f3d5
* include generalised MVT in HyperReal (contributed by Benjamin Porter)

* add non-denumerability of continuum in Real, includes closed intervals on real
(contributed by Benjamin Porter, #22 in http://www.cs.ru.nl/~freek/100/)
src/HOL/Hyperreal/Lim.thy
src/HOL/Real/ContNotDenum.thy
src/HOL/Real/Real.thy
src/HOL/Real/RealDef.thy
     1.1 --- a/src/HOL/Hyperreal/Lim.thy	Sun Feb 12 10:42:19 2006 +0100
     1.2 +++ b/src/HOL/Hyperreal/Lim.thy	Sun Feb 12 12:29:01 2006 +0100
     1.3 @@ -3,6 +3,7 @@
     1.4      Author      : Jacques D. Fleuriot
     1.5      Copyright   : 1998  University of Cambridge
     1.6      Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     1.7 +    GMVT by Benjamin Porter, 2005
     1.8  *)
     1.9  
    1.10  header{*Limits, Continuity and Differentiation*}
    1.11 @@ -15,16 +16,16 @@
    1.12  
    1.13  constdefs
    1.14    LIM :: "[real=>real,real,real] => bool"
    1.15 -				("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
    1.16 +        ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
    1.17    "f -- a --> L ==
    1.18       \<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s
    1.19 -			  --> \<bar>f x + -L\<bar> < r"
    1.20 +        --> \<bar>f x + -L\<bar> < r"
    1.21  
    1.22    NSLIM :: "[real=>real,real,real] => bool"
    1.23 -			      ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
    1.24 +            ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
    1.25    "f -- a --NS> L == (\<forall>x. (x \<noteq> hypreal_of_real a &
    1.26 -		      x @= hypreal_of_real a -->
    1.27 -		      ( *f* f) x @= hypreal_of_real L))"
    1.28 +          x @= hypreal_of_real a -->
    1.29 +          ( *f* f) x @= hypreal_of_real L))"
    1.30  
    1.31    isCont :: "[real=>real,real] => bool"
    1.32    "isCont f a == (f -- a --> (f a))"
    1.33 @@ -32,29 +33,29 @@
    1.34    isNSCont :: "[real=>real,real] => bool"
    1.35      --{*NS definition dispenses with limit notions*}
    1.36    "isNSCont f a == (\<forall>y. y @= hypreal_of_real a -->
    1.37 -			   ( *f* f) y @= hypreal_of_real (f a))"
    1.38 +         ( *f* f) y @= hypreal_of_real (f a))"
    1.39  
    1.40    deriv:: "[real=>real,real,real] => bool"
    1.41      --{*Differentiation: D is derivative of function f at x*}
    1.42 -			    ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
    1.43 +          ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
    1.44    "DERIV f x :> D == ((%h. (f(x + h) + -f x)/h) -- 0 --> D)"
    1.45  
    1.46    nsderiv :: "[real=>real,real,real] => bool"
    1.47 -			    ("(NSDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
    1.48 +          ("(NSDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
    1.49    "NSDERIV f x :> D == (\<forall>h \<in> Infinitesimal - {0}.
    1.50 -			(( *f* f)(hypreal_of_real x + h) +
    1.51 -			 - hypreal_of_real (f x))/h @= hypreal_of_real D)"
    1.52 +      (( *f* f)(hypreal_of_real x + h) +
    1.53 +       - hypreal_of_real (f x))/h @= hypreal_of_real D)"
    1.54  
    1.55    differentiable :: "[real=>real,real] => bool"   (infixl "differentiable" 60)
    1.56    "f differentiable x == (\<exists>D. DERIV f x :> D)"
    1.57  
    1.58 -  NSdifferentiable :: "[real=>real,real] => bool"   
    1.59 +  NSdifferentiable :: "[real=>real,real] => bool"
    1.60                         (infixl "NSdifferentiable" 60)
    1.61    "f NSdifferentiable x == (\<exists>D. NSDERIV f x :> D)"
    1.62  
    1.63    increment :: "[real=>real,real,hypreal] => hypreal"
    1.64    "increment f x h == (@inc. f NSdifferentiable x &
    1.65 -		       inc = ( *f* f)(hypreal_of_real x + h) + -hypreal_of_real (f x))"
    1.66 +           inc = ( *f* f)(hypreal_of_real x + h) + -hypreal_of_real (f x))"
    1.67  
    1.68    isUCont :: "(real=>real) => bool"
    1.69    "isUCont f ==  \<forall>r > 0. \<exists>s > 0. \<forall>x y. \<bar>x + -y\<bar> < s --> \<bar>f x + -f y\<bar> < r"
    1.70 @@ -133,7 +134,7 @@
    1.71  
    1.72  lemma LIM_diff:
    1.73      "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) - g(x)) -- x --> l-m"
    1.74 -by (simp add: diff_minus LIM_add_minus) 
    1.75 +by (simp add: diff_minus LIM_add_minus)
    1.76  
    1.77  
    1.78  lemma LIM_const_not_eq: "k \<noteq> L ==> ~ ((%x. k) -- a --> L)"
    1.79 @@ -146,7 +147,7 @@
    1.80      assume s: "0<s"
    1.81      { from s show "s/2 + a < a \<or> a < s/2 + a" by arith
    1.82       next
    1.83 -      from s show "\<bar>s / 2 + a - a\<bar> < s" by (simp add: abs_if) 
    1.84 +      from s show "\<bar>s / 2 + a - a\<bar> < s" by (simp add: abs_if)
    1.85       next
    1.86        from s show "~ \<bar>k-L\<bar> < L-k" by (simp add: abs_if) }
    1.87    qed
    1.88 @@ -159,7 +160,7 @@
    1.89      assume s: "0<s"
    1.90      { from s show "s/2 + a < a \<or> a < s/2 + a" by arith
    1.91       next
    1.92 -      from s show "\<bar>s / 2 + a - a\<bar> < s" by (simp add: abs_if) 
    1.93 +      from s show "\<bar>s / 2 + a - a\<bar> < s" by (simp add: abs_if)
    1.94       next
    1.95        from s show "~ \<bar>k-L\<bar> < k-L" by (simp add: abs_if) }
    1.96    qed
    1.97 @@ -167,11 +168,11 @@
    1.98  
    1.99  lemma LIM_const_eq: "(%x. k) -- x --> L ==> k = L"
   1.100  apply (rule ccontr)
   1.101 -apply (blast dest: LIM_const_not_eq) 
   1.102 +apply (blast dest: LIM_const_not_eq)
   1.103  done
   1.104  
   1.105  lemma LIM_unique: "[| f -- a --> L; f -- a --> M |] ==> L = M"
   1.106 -apply (drule LIM_diff, assumption) 
   1.107 +apply (drule LIM_diff, assumption)
   1.108  apply (auto dest!: LIM_const_eq)
   1.109  done
   1.110  
   1.111 @@ -198,7 +199,7 @@
   1.112      assume "x \<noteq> a \<and> \<bar>x-a\<bar> < min fs gs"
   1.113      with fs_lt gs_lt
   1.114      have "\<bar>f x\<bar> < 1" and "\<bar>g x\<bar> < r" by (auto simp add: fs_lt)
   1.115 -    hence "\<bar>f x\<bar> * \<bar>g x\<bar> < 1*r" by (rule abs_mult_less) 
   1.116 +    hence "\<bar>f x\<bar> * \<bar>g x\<bar> < 1*r" by (rule abs_mult_less)
   1.117      thus "\<bar>f x\<bar> * \<bar>g x\<bar> < r" by simp
   1.118    qed
   1.119  qed
   1.120 @@ -228,7 +229,7 @@
   1.121  apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
   1.122  apply (rule_tac x = xa in star_cases)
   1.123  apply (auto simp add: real_add_minus_iff starfun star_n_minus star_of_def star_n_add star_n_eq_iff)
   1.124 -apply (rule bexI [OF _ Rep_star_star_n], clarify) 
   1.125 +apply (rule bexI [OF _ Rep_star_star_n], clarify)
   1.126  apply (drule_tac x = u in spec, clarify)
   1.127  apply (drule_tac x = s in spec, clarify)
   1.128  apply (subgoal_tac "\<forall>n::nat. (Xa n) \<noteq> x & \<bar>(Xa n) + - x\<bar> < s --> \<bar>f (Xa n) + - L\<bar> < u")
   1.129 @@ -594,7 +595,7 @@
   1.130  lemma lemma_LIMu: "\<forall>s>0.\<exists>z y. \<bar>z + - y\<bar> < s & r \<le> \<bar>f z + -f y\<bar>
   1.131        ==> \<forall>n::nat. \<exists>z y. \<bar>z + -y\<bar> < inverse(real(Suc n)) & r \<le> \<bar>f z + -f y\<bar>"
   1.132  apply clarify
   1.133 -apply (cut_tac n1 = n 
   1.134 +apply (cut_tac n1 = n
   1.135         in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto)
   1.136  done
   1.137  
   1.138 @@ -772,8 +773,8 @@
   1.139  apply (drule_tac [!] hypreal_not_eq_minus_iff [THEN iffD1])
   1.140  apply (subgoal_tac [2] "( *f* (%z. z-x)) u \<noteq> (0::hypreal) ")
   1.141  apply (auto simp add: diff_minus
   1.142 -	       approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]]
   1.143 -		     Infinitesimal_subset_HFinite [THEN subsetD])
   1.144 +         approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]]
   1.145 +         Infinitesimal_subset_HFinite [THEN subsetD])
   1.146  done
   1.147  
   1.148  lemma NSDERIVD4:
   1.149 @@ -881,7 +882,7 @@
   1.150        ==> NSDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"
   1.151  apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
   1.152  apply (auto dest!: spec
   1.153 -	    simp add: starfun_lambda_cancel lemma_nsderiv1)
   1.154 +      simp add: starfun_lambda_cancel lemma_nsderiv1)
   1.155  apply (simp (no_asm) add: add_divide_distrib)
   1.156  apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
   1.157  apply (auto simp add: times_divide_eq_right [symmetric]
   1.158 @@ -1330,7 +1331,7 @@
   1.159  apply (auto simp add: Bolzano_bisect_le Let_def split_def)
   1.160  done
   1.161  
   1.162 -lemma eq_divide_2_times_iff: "((x::real) = y / (2 * z)) = (2 * x = y/z)" 
   1.163 +lemma eq_divide_2_times_iff: "((x::real) = y / (2 * z)) = (2 * x = y/z)"
   1.164  apply (auto)
   1.165  apply (drule_tac f = "%u. (1/2) *u" in arg_cong)
   1.166  apply (simp)
   1.167 @@ -1498,7 +1499,7 @@
   1.168  lemma isCont_has_Ub: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
   1.169           ==> \<exists>M. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) &
   1.170                     (\<forall>N. N < M --> (\<exists>x. a \<le> x & x \<le> b & N < f(x)))"
   1.171 -apply (cut_tac S = "Collect (%y. \<exists>x. a \<le> x & x \<le> b & y = f x)" 
   1.172 +apply (cut_tac S = "Collect (%y. \<exists>x. a \<le> x & x \<le> b & y = f x)"
   1.173          in lemma_reals_complete)
   1.174  apply auto
   1.175  apply (drule isCont_bounded, assumption)
   1.176 @@ -1601,12 +1602,12 @@
   1.177      assume "0 < h" "h < s"
   1.178      with all [of h] show "f x < f (x+h)"
   1.179      proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric]
   1.180 -		split add: split_if_asm)
   1.181 +    split add: split_if_asm)
   1.182        assume "~ (f (x+h) - f x) / h < l" and h: "0 < h"
   1.183        with l
   1.184        have "0 < (f (x+h) - f x) / h" by arith
   1.185        thus "f x < f (x+h)"
   1.186 -	by (simp add: pos_less_divide_eq h)
   1.187 +  by (simp add: pos_less_divide_eq h)
   1.188      qed
   1.189    qed
   1.190  qed
   1.191 @@ -1630,12 +1631,12 @@
   1.192      assume "0 < h" "h < s"
   1.193      with all [of "-h"] show "f x < f (x-h)"
   1.194      proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric]
   1.195 -		split add: split_if_asm)
   1.196 +    split add: split_if_asm)
   1.197        assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h"
   1.198        with l
   1.199        have "0 < (f (x-h) - f x) / h" by arith
   1.200        thus "f x < f (x-h)"
   1.201 -	by (simp add: pos_less_divide_eq h)
   1.202 +  by (simp add: pos_less_divide_eq h)
   1.203      qed
   1.204    qed
   1.205  qed
   1.206 @@ -1742,9 +1743,9 @@
   1.207        hence ax': "a<x'" and x'b: "x'<b" by auto
   1.208        from lemma_interval [OF ax' x'b]
   1.209        obtain d where d: "0<d" and bound: "\<forall>y. \<bar>x'-y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b"
   1.210 -	by blast
   1.211 +  by blast
   1.212        hence bound': "\<forall>y. \<bar>x'-y\<bar> < d \<longrightarrow> f x' \<le> f y" using x'_min
   1.213 -	by blast
   1.214 +  by blast
   1.215        from differentiableD [OF dif [OF ax'b]]
   1.216        obtain l where der: "DERIV f x' :> l" ..
   1.217        have "l=0" by (rule DERIV_local_min [OF der d bound'])
   1.218 @@ -1759,7 +1760,7 @@
   1.219        obtain r where ar: "a < r" and rb: "r < b" by blast
   1.220        from lemma_interval [OF ar rb]
   1.221        obtain d where d: "0<d" and bound: "\<forall>y. \<bar>r-y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b"
   1.222 -	by blast
   1.223 +  by blast
   1.224        have eq_fb: "\<forall>z. a \<le> z --> z \<le> b --> f z = f b"
   1.225        proof (clarify)
   1.226          fix z::real
   1.227 @@ -1798,7 +1799,7 @@
   1.228    hence ba: "b-a \<noteq> 0" by arith
   1.229    show ?thesis
   1.230      by (rule real_mult_left_cancel [OF ba, THEN iffD1],
   1.231 -        simp add: right_diff_distrib, 
   1.232 +        simp add: right_diff_distrib,
   1.233          simp add: left_diff_distrib)
   1.234  qed
   1.235  
   1.236 @@ -1888,10 +1889,10 @@
   1.237  done
   1.238  
   1.239  lemma real_average_minus_first [simp]: "((a + b) /2 - a) = (b-a)/(2::real)"
   1.240 -by (simp) 
   1.241 +by (simp)
   1.242  
   1.243  lemma real_average_minus_second [simp]: "((b + a)/2 - a) = (b-a)/(2::real)"
   1.244 -by (simp) 
   1.245 +by (simp)
   1.246  
   1.247  text{*Gallileo's "trick": average velocity = av. of end velocities*}
   1.248  
   1.249 @@ -2060,6 +2061,319 @@
   1.250    qed
   1.251  qed
   1.252  
   1.253 +
   1.254 +lemma differentiable_const: "(\<lambda>z. a) differentiable x"
   1.255 +  apply (unfold differentiable_def)
   1.256 +  apply (rule_tac x=0 in exI)
   1.257 +  apply simp
   1.258 +  done
   1.259 +
   1.260 +lemma differentiable_sum:
   1.261 +  assumes "f differentiable x"
   1.262 +  and "g differentiable x"
   1.263 +  shows "(\<lambda>x. f x + g x) differentiable x"
   1.264 +proof -
   1.265 +  from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def)
   1.266 +  then obtain df where "DERIV f x :> df" ..
   1.267 +  moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
   1.268 +  then obtain dg where "DERIV g x :> dg" ..
   1.269 +  ultimately have "DERIV (\<lambda>x. f x + g x) x :> df + dg" by (rule DERIV_add)
   1.270 +  hence "\<exists>D. DERIV (\<lambda>x. f x + g x) x :> D" by auto
   1.271 +  thus ?thesis by (fold differentiable_def)
   1.272 +qed
   1.273 +
   1.274 +lemma differentiable_diff:
   1.275 +  assumes "f differentiable x"
   1.276 +  and "g differentiable x"
   1.277 +  shows "(\<lambda>x. f x - g x) differentiable x"
   1.278 +proof -
   1.279 +  from prems have "f differentiable x" by simp
   1.280 +  moreover
   1.281 +  from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
   1.282 +  then obtain dg where "DERIV g x :> dg" ..
   1.283 +  then have "DERIV (\<lambda>x. - g x) x :> -dg" by (rule DERIV_minus)
   1.284 +  hence "\<exists>D. DERIV (\<lambda>x. - g x) x :> D" by auto
   1.285 +  hence "(\<lambda>x. - g x) differentiable x" by (fold differentiable_def)
   1.286 +  ultimately 
   1.287 +  show ?thesis
   1.288 +    by (auto simp: real_diff_def dest: differentiable_sum)
   1.289 +qed
   1.290 +
   1.291 +lemma differentiable_mult:
   1.292 +  assumes "f differentiable x"
   1.293 +  and "g differentiable x"
   1.294 +  shows "(\<lambda>x. f x * g x) differentiable x"
   1.295 +proof -
   1.296 +  from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def)
   1.297 +  then obtain df where "DERIV f x :> df" ..
   1.298 +  moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
   1.299 +  then obtain dg where "DERIV g x :> dg" ..
   1.300 +  ultimately have "DERIV (\<lambda>x. f x * g x) x :> df * g x + dg * f x" by (simp add: DERIV_mult)
   1.301 +  hence "\<exists>D. DERIV (\<lambda>x. f x * g x) x :> D" by auto
   1.302 +  thus ?thesis by (fold differentiable_def)
   1.303 +qed
   1.304 +
   1.305 +
   1.306 +theorem GMVT:
   1.307 +  assumes alb: "a < b"
   1.308 +  and fc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"
   1.309 +  and fd: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable x"
   1.310 +  and gc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont g x"
   1.311 +  and gd: "\<forall>x. a < x \<and> x < b \<longrightarrow> g differentiable x"
   1.312 +  shows "\<exists>g'c f'c c. DERIV g c :> g'c \<and> DERIV f c :> f'c \<and> a < c \<and> c < b \<and> ((f b - f a) * g'c) = ((g b - g a) * f'c)"
   1.313 +proof -
   1.314 +  let ?h = "\<lambda>x. (f b - f a)*(g x) - (g b - g a)*(f x)"
   1.315 +  from prems have "a < b" by simp
   1.316 +  moreover have "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?h x"
   1.317 +  proof -
   1.318 +    have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. f b - f a) x" by simp
   1.319 +    with gc have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. (f b - f a) * g x) x"
   1.320 +      by (auto intro: isCont_mult)
   1.321 +    moreover
   1.322 +    have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. g b - g a) x" by simp
   1.323 +    with fc have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. (g b - g a) * f x) x"
   1.324 +      by (auto intro: isCont_mult)
   1.325 +    ultimately show ?thesis
   1.326 +      by (fastsimp intro: isCont_diff)
   1.327 +  qed
   1.328 +  moreover
   1.329 +  have "\<forall>x. a < x \<and> x < b \<longrightarrow> ?h differentiable x"
   1.330 +  proof -
   1.331 +    have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. f b - f a) differentiable x" by (simp add: differentiable_const)
   1.332 +    with gd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (f b - f a) * g x) differentiable x" by (simp add: differentiable_mult)
   1.333 +    moreover
   1.334 +    have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. g b - g a) differentiable x" by (simp add: differentiable_const)
   1.335 +    with fd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (g b - g a) * f x) differentiable x" by (simp add: differentiable_mult)
   1.336 +    ultimately show ?thesis by (simp add: differentiable_diff)
   1.337 +  qed
   1.338 +  ultimately have "\<exists>l z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" by (rule MVT)
   1.339 +  then obtain l where ldef: "\<exists>z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" ..
   1.340 +  then obtain c where cdef: "a < c \<and> c < b \<and> DERIV ?h c :> l \<and> ?h b - ?h a = (b - a) * l" ..
   1.341 +
   1.342 +  from cdef have cint: "a < c \<and> c < b" by auto
   1.343 +  with gd have "g differentiable c" by simp
   1.344 +  hence "\<exists>D. DERIV g c :> D" by (rule differentiableD)
   1.345 +  then obtain g'c where g'cdef: "DERIV g c :> g'c" ..
   1.346 +
   1.347 +  from cdef have "a < c \<and> c < b" by auto
   1.348 +  with fd have "f differentiable c" by simp
   1.349 +  hence "\<exists>D. DERIV f c :> D" by (rule differentiableD)
   1.350 +  then obtain f'c where f'cdef: "DERIV f c :> f'c" ..
   1.351 +
   1.352 +  from cdef have "DERIV ?h c :> l" by auto
   1.353 +  moreover
   1.354 +  {
   1.355 +    from g'cdef have "DERIV (\<lambda>x. (f b - f a) * g x) c :> g'c * (f b - f a)"
   1.356 +      apply (insert DERIV_const [where k="f b - f a"])
   1.357 +      apply (drule meta_spec [of _ c])
   1.358 +      apply (drule DERIV_mult [where f="(\<lambda>x. f b - f a)" and g=g])
   1.359 +      by simp_all
   1.360 +    moreover from f'cdef have "DERIV (\<lambda>x. (g b - g a) * f x) c :> f'c * (g b - g a)"
   1.361 +      apply (insert DERIV_const [where k="g b - g a"])
   1.362 +      apply (drule meta_spec [of _ c])
   1.363 +      apply (drule DERIV_mult [where f="(\<lambda>x. g b - g a)" and g=f])
   1.364 +      by simp_all
   1.365 +    ultimately have "DERIV ?h c :>  g'c * (f b - f a) - f'c * (g b - g a)"
   1.366 +      by (simp add: DERIV_diff)
   1.367 +  }
   1.368 +  ultimately have leq: "l =  g'c * (f b - f a) - f'c * (g b - g a)" by (rule DERIV_unique)
   1.369 +
   1.370 +  {
   1.371 +    from cdef have "?h b - ?h a = (b - a) * l" by auto
   1.372 +    also with leq have "\<dots> = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp
   1.373 +    finally have "?h b - ?h a = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp
   1.374 +  }
   1.375 +  moreover
   1.376 +  {
   1.377 +    have "?h b - ?h a =
   1.378 +         ((f b)*(g b) - (f a)*(g b) - (g b)*(f b) + (g a)*(f b)) -
   1.379 +          ((f b)*(g a) - (f a)*(g a) - (g b)*(f a) + (g a)*(f a))"
   1.380 +      by (simp add: mult_ac add_ac real_diff_mult_distrib)
   1.381 +    hence "?h b - ?h a = 0" by auto
   1.382 +  }
   1.383 +  ultimately have "(b - a) * (g'c * (f b - f a) - f'c * (g b - g a)) = 0" by auto
   1.384 +  with alb have "g'c * (f b - f a) - f'c * (g b - g a) = 0" by simp
   1.385 +  hence "g'c * (f b - f a) = f'c * (g b - g a)" by simp
   1.386 +  hence "(f b - f a) * g'c = (g b - g a) * f'c" by (simp add: mult_ac)
   1.387 +
   1.388 +  with g'cdef f'cdef cint show ?thesis by auto
   1.389 +qed
   1.390 +
   1.391 +
   1.392 +lemma LIMSEQ_SEQ_conv1:
   1.393 +  assumes "X -- a --> L"
   1.394 +  shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
   1.395 +proof -
   1.396 +  {
   1.397 +    from prems have Xdef: "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s --> \<bar>X x + -L\<bar> < r" by (unfold LIM_def)
   1.398 +    
   1.399 +    fix S
   1.400 +    assume as: "(\<forall>n. S n \<noteq> a) \<and> S ----> a"
   1.401 +    then have "S ----> a" by auto
   1.402 +    then have Sdef: "(\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>S n + -a\<bar> < r))" by (unfold LIMSEQ_def)
   1.403 +    {
   1.404 +      fix r
   1.405 +      from Xdef have Xdef2: "0 < r --> (\<exists>s > 0. \<forall>x. x \<noteq> a \<and> \<bar>x + -a\<bar> < s --> \<bar>X x + -L\<bar> < r)" by simp
   1.406 +      {
   1.407 +        assume rgz: "0 < r"
   1.408 +
   1.409 +        from Xdef2 rgz have "\<exists>s > 0. \<forall>x. x \<noteq> a \<and> \<bar>x + -a\<bar> < s --> \<bar>X x + -L\<bar> < r" by simp 
   1.410 +        then obtain s where sdef: "s > 0 \<and> (\<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s \<longrightarrow> \<bar>X x + -L\<bar> < r)" by auto
   1.411 +        then have aux: "\<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s \<longrightarrow> \<bar>X x + -L\<bar> < r" by auto
   1.412 +        {
   1.413 +          fix n
   1.414 +          from aux have "S n \<noteq> a \<and> \<bar>S n + -a\<bar> < s \<longrightarrow> \<bar>X (S n) + -L\<bar> < r" by simp
   1.415 +          with as have imp2: "\<bar>S n + -a\<bar> < s --> \<bar>X (S n) + -L\<bar> < r" by auto
   1.416 +        }
   1.417 +        hence "\<forall>n. \<bar>S n + -a\<bar> < s --> \<bar>X (S n) + -L\<bar> < r" ..
   1.418 +        moreover
   1.419 +        from Sdef sdef have imp1: "\<exists>no. \<forall>n. no \<le> n --> \<bar>S n + -a\<bar> < s" by auto  
   1.420 +        then obtain no where "\<forall>n. no \<le> n --> \<bar>S n + -a\<bar> < s" by auto
   1.421 +        ultimately have "\<forall>n. no \<le> n \<longrightarrow> \<bar>X (S n) + -L\<bar> < r" by simp
   1.422 +        hence "\<exists>no. \<forall>n. no \<le> n \<longrightarrow> \<bar>X (S n) + -L\<bar> < r" by auto
   1.423 +      }
   1.424 +    }
   1.425 +    hence "(\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>X (S n) + -L\<bar> < r))" by simp
   1.426 +    hence "(\<lambda>n. X (S n)) ----> L" by (fold LIMSEQ_def)
   1.427 +  }
   1.428 +  thus ?thesis by simp
   1.429 +qed
   1.430 +
   1.431 +lemma LIMSEQ_SEQ_conv2:
   1.432 +  assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
   1.433 +  shows "X -- a --> L"
   1.434 +proof (rule ccontr)
   1.435 +  assume "\<not> (X -- a --> L)"
   1.436 +  hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s --> \<bar>X x + -L\<bar> < r)" by (unfold LIM_def)
   1.437 +  hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. \<not>(x \<noteq> a \<and> \<bar>x + -a\<bar> < s --> \<bar>X x + -L\<bar> < r)" by simp
   1.438 +  hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> \<bar>X x + -L\<bar> \<ge> r)" by (simp add: linorder_not_less)
   1.439 +  then obtain r where rdef: "r > 0 \<and> (\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> \<bar>X x + -L\<bar> \<ge> r))" by auto
   1.440 +
   1.441 +  let ?F = "\<lambda>n::nat. SOME x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> \<bar>X x + -L\<bar> \<ge> r"
   1.442 +  have "?F ----> a"
   1.443 +  proof -
   1.444 +    {
   1.445 +      fix e::real
   1.446 +      assume "0 < e"
   1.447 +        (* choose no such that inverse (real (Suc n)) < e *)
   1.448 +      have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean)
   1.449 +      then obtain m where nodef: "inverse (real (Suc m)) < e" by auto
   1.450 +      {
   1.451 +        fix n
   1.452 +        assume mlen: "m \<le> n"
   1.453 +        then have
   1.454 +          "inverse (real (Suc n)) \<le> inverse (real (Suc m))"
   1.455 +          by auto
   1.456 +        moreover have
   1.457 +          "\<bar>?F n + -a\<bar> < inverse (real (Suc n))"
   1.458 +        proof -
   1.459 +          from rdef have
   1.460 +            "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> \<bar>X x + -L\<bar> \<ge> r"
   1.461 +            by simp
   1.462 +          hence
   1.463 +            "(?F n)\<noteq>a \<and> \<bar>(?F n) + -a\<bar> < inverse (real (Suc n)) \<and> \<bar>X (?F n) + -L\<bar> \<ge> r"
   1.464 +            by (simp add: some_eq_ex [symmetric])
   1.465 +          thus ?thesis by simp
   1.466 +        qed
   1.467 +        moreover from nodef have
   1.468 +          "inverse (real (Suc m)) < e" .
   1.469 +        ultimately have "\<bar>?F n + -a\<bar> < e" by arith
   1.470 +      }
   1.471 +      then have "\<exists>no. \<forall>n. no \<le> n --> \<bar>?F n + -a\<bar> < e" by auto
   1.472 +    }
   1.473 +    thus ?thesis by (unfold LIMSEQ_def, simp)
   1.474 +  qed
   1.475 +  
   1.476 +  moreover have "\<forall>n. ?F n \<noteq> a"
   1.477 +  proof -
   1.478 +    {
   1.479 +      fix n
   1.480 +      from rdef have
   1.481 +        "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> \<bar>X x + -L\<bar> \<ge> r"
   1.482 +        by simp
   1.483 +      hence "?F n \<noteq> a" by (simp add: some_eq_ex [symmetric])
   1.484 +    }
   1.485 +    thus ?thesis ..
   1.486 +  qed
   1.487 +  moreover from prems have "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" by simp
   1.488 +  ultimately have "(\<lambda>n. X (?F n)) ----> L" by simp
   1.489 +  
   1.490 +  moreover have "\<not> ((\<lambda>n. X (?F n)) ----> L)"
   1.491 +  proof -
   1.492 +    {
   1.493 +      fix no::nat
   1.494 +      obtain n where "n = no + 1" by simp
   1.495 +      then have nolen: "no \<le> n" by simp
   1.496 +        (* We prove this by showing that for any m there is an n\<ge>m such that |X (?F n) - L| \<ge> r *)
   1.497 +      from rdef have "\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> \<bar>X x + -L\<bar> \<ge> r)" ..
   1.498 +
   1.499 +      then have "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> \<bar>X x + -L\<bar> \<ge> r" by simp
   1.500 +      
   1.501 +      hence "\<bar>X (?F n) + -L\<bar> \<ge> r" by (simp add: some_eq_ex [symmetric])
   1.502 +      with nolen have "\<exists>n. no \<le> n \<and> \<bar>X (?F n) + -L\<bar> \<ge> r" by auto
   1.503 +    }
   1.504 +    then have "(\<forall>no. \<exists>n. no \<le> n \<and> \<bar>X (?F n) + -L\<bar> \<ge> r)" by simp
   1.505 +    with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> \<bar>X (?F n) + -L\<bar> \<ge> e)" by auto
   1.506 +    thus ?thesis by (unfold LIMSEQ_def, auto simp add: linorder_not_less)
   1.507 +  qed
   1.508 +  ultimately show False by simp
   1.509 +qed
   1.510 +
   1.511 +
   1.512 +lemma LIMSEQ_SEQ_conv:
   1.513 +  "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L) = (X -- a --> L)"
   1.514 +proof
   1.515 +  assume "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
   1.516 +  show "X -- a --> L" by (rule LIMSEQ_SEQ_conv2)
   1.517 +next
   1.518 +  assume "(X -- a --> L)"
   1.519 +  show "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" by (rule LIMSEQ_SEQ_conv1)
   1.520 +qed
   1.521 +
   1.522 +lemma real_sqz:
   1.523 +  fixes a::real
   1.524 +  assumes "a < c"
   1.525 +  shows "\<exists>b. a < b \<and> b < c"
   1.526 +proof
   1.527 +  let ?b = "(a + c) / 2"
   1.528 +  have "a < ?b" by simp
   1.529 +  moreover
   1.530 +  have "?b < c" by simp
   1.531 +  ultimately
   1.532 +  show "a < ?b \<and> ?b < c" by simp
   1.533 +qed
   1.534 +
   1.535 +lemma LIM_offset:
   1.536 +  assumes "(\<lambda>x. f x) -- a --> L"
   1.537 +  shows "(\<lambda>x. f (x+c)) -- (a-c) --> L"
   1.538 +proof -
   1.539 +  have "f -- a --> L" .
   1.540 +  hence
   1.541 +    fd: "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s --> \<bar>f x + -L\<bar> < r"
   1.542 +    by (unfold LIM_def)
   1.543 +  {
   1.544 +    fix r::real
   1.545 +    assume rgz: "0 < r"
   1.546 +    with fd have "\<exists>s > 0. \<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s --> \<bar>f x + -L\<bar> < r" by simp
   1.547 +    then obtain s where sgz: "s > 0" and ax: "\<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s \<longrightarrow> \<bar>f x + -L\<bar> < r" by auto
   1.548 +    from ax have ax2: "\<forall>x. (x+c)\<noteq>a \<and> \<bar>(x+c) + -a\<bar> < s \<longrightarrow> \<bar>f (x+c) + -L\<bar> < r" by auto
   1.549 +    {
   1.550 +      fix x::real
   1.551 +      from ax2 have nt: "(x+c)\<noteq>a \<and> \<bar>(x+c) + -a\<bar> < s \<longrightarrow> \<bar>f (x+c) + -L\<bar> < r" ..
   1.552 +      moreover have "((x+c)\<noteq>a) = (x\<noteq>(a-c))" by auto
   1.553 +      moreover have "((x+c) + -a) = (x + -(a-c))" by simp
   1.554 +      ultimately have "x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> \<bar>f (x+c) + -L\<bar> < r" by simp
   1.555 +    }
   1.556 +    then have "\<forall>x. x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> \<bar>f (x+c) + -L\<bar> < r" ..
   1.557 +    with sgz have "\<exists>s > 0. \<forall>x. x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> \<bar>f (x+c) + -L\<bar> < r" by auto
   1.558 +  }
   1.559 +  then have
   1.560 +    "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> (a-c) & \<bar>x + -(a-c)\<bar> < s --> \<bar>f (x+c) + -L\<bar> < r" by simp
   1.561 +  thus ?thesis by (fold LIM_def)
   1.562 +qed
   1.563 +
   1.564 +
   1.565 +
   1.566  ML
   1.567  {*
   1.568  val LIM_def = thm"LIM_def";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Real/ContNotDenum.thy	Sun Feb 12 12:29:01 2006 +0100
     2.3 @@ -0,0 +1,578 @@
     2.4 +(*  Title       : HOL/Real/ContNonDenum
     2.5 +    ID          : $Id$
     2.6 +    Author      : Benjamin Porter, Monash University, NICTA, 2005
     2.7 +*)
     2.8 +
     2.9 +header {* Non-denumerability of the Continuum. *}
    2.10 +
    2.11 +theory ContNotDenum
    2.12 +imports RComplete
    2.13 +begin
    2.14 +
    2.15 +section {* Abstract *}
    2.16 +
    2.17 +text {* The following document presents a proof that the Continuum is
    2.18 +uncountable. It is formalised in the Isabelle/Isar theorem proving
    2.19 +system.
    2.20 +
    2.21 +{\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other
    2.22 +words, there does not exist a function f:@{text "\<nat>\<Rightarrow>\<real>"} such that f is
    2.23 +surjective.
    2.24 +
    2.25 +{\em Outline:} An elegant informal proof of this result uses Cantor's
    2.26 +Diagonalisation argument. The proof presented here is not this
    2.27 +one. First we formalise some properties of closed intervals, then we
    2.28 +prove the Nested Interval Property. This property relies on the
    2.29 +completeness of the Real numbers and is the foundation for our
    2.30 +argument. Informally it states that an intersection of countable
    2.31 +closed intervals (where each successive interval is a subset of the
    2.32 +last) is non-empty. We then assume a surjective function f:@{text
    2.33 +"\<nat>\<Rightarrow>\<real>"} exists and find a real x such that x is not in the range of f
    2.34 +by generating a sequence of closed intervals then using the NIP. *}
    2.35 +
    2.36 +section {* Closed Intervals *}
    2.37 +
    2.38 +text {* This section formalises some properties of closed intervals. *}
    2.39 +
    2.40 +subsection {* Definition *}
    2.41 +
    2.42 +constdefs closed_int :: "real \<Rightarrow> real \<Rightarrow> real set"
    2.43 +  "closed_int x y \<equiv> {z. x \<le> z \<and> z \<le> y}"
    2.44 +
    2.45 +subsection {* 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 (unfold closed_int_def, simp)
    2.55 +    with xy have "x \<ge> x0 \<and> x \<le> y0" by auto
    2.56 +    hence "x \<in> closed_int x0 y0" by (unfold closed_int_def, simp)
    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 +  by (unfold closed_int_def) 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 +section {* 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 +section {* 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 +consts newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)"
   2.399 +primrec
   2.400 +"newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"
   2.401 +"newInt (Suc n) f =
   2.402 +  (SOME e. (\<exists>e1 e2.
   2.403 +   e1 < e2 \<and>
   2.404 +   e = closed_int e1 e2 \<and>
   2.405 +   e \<subseteq> (newInt n f) \<and>
   2.406 +   (f (Suc n)) \<notin> e)
   2.407 +  )"
   2.408 +
   2.409 +subsubsection {* Properties *}
   2.410 +
   2.411 +text {* We now show that every application of newInt returns an
   2.412 +appropriate interval. *}
   2.413 +
   2.414 +lemma newInt_ex:
   2.415 +  "\<exists>a b. a < b \<and>
   2.416 +   newInt (Suc n) f = closed_int a b \<and>
   2.417 +   newInt (Suc n) f \<subseteq> newInt n f \<and>
   2.418 +   f (Suc n) \<notin> newInt (Suc n) f"
   2.419 +proof (induct n)
   2.420 +  case 0
   2.421 +
   2.422 +  let ?e = "SOME e. \<exists>e1 e2.
   2.423 +   e1 < e2 \<and>
   2.424 +   e = closed_int e1 e2 \<and>
   2.425 +   e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
   2.426 +   f (Suc 0) \<notin> e"
   2.427 +
   2.428 +  have "newInt (Suc 0) f = ?e" by auto
   2.429 +  moreover
   2.430 +  have "f 0 + 1 < f 0 + 2" by simp
   2.431 +  with closed_subset_ex have
   2.432 +    "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
   2.433 +     f (Suc 0) \<notin> (closed_int ka kb)" .
   2.434 +  hence
   2.435 +    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
   2.436 +     e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> e" by simp
   2.437 +  hence
   2.438 +    "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
   2.439 +     ?e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> ?e"
   2.440 +    by (rule someI_ex)
   2.441 +  ultimately have "\<exists>e1 e2. e1 < e2 \<and>
   2.442 +   newInt (Suc 0) f = closed_int e1 e2 \<and>
   2.443 +   newInt (Suc 0) f \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
   2.444 +   f (Suc 0) \<notin> newInt (Suc 0) f" by simp
   2.445 +  thus
   2.446 +    "\<exists>a b. a < b \<and> newInt (Suc 0) f = closed_int a b \<and>
   2.447 +     newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
   2.448 +    by simp
   2.449 +next
   2.450 +  case (Suc n)
   2.451 +  hence "\<exists>a b.
   2.452 +   a < b \<and>
   2.453 +   newInt (Suc n) f = closed_int a b \<and>
   2.454 +   newInt (Suc n) f \<subseteq> newInt n f \<and>
   2.455 +   f (Suc n) \<notin> newInt (Suc n) f" by simp
   2.456 +  then obtain a and b where ab: "a < b \<and>
   2.457 +   newInt (Suc n) f = closed_int a b \<and>
   2.458 +   newInt (Suc n) f \<subseteq> newInt n f \<and>
   2.459 +   f (Suc n) \<notin> newInt (Suc n) f" by auto
   2.460 +  hence cab: "closed_int a b = newInt (Suc n) f" by simp
   2.461 +
   2.462 +  let ?e = "SOME e. \<exists>e1 e2.
   2.463 +    e1 < e2 \<and>
   2.464 +    e = closed_int e1 e2 \<and>
   2.465 +    e \<subseteq> closed_int a b \<and>
   2.466 +    f (Suc (Suc n)) \<notin> e"
   2.467 +  from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto
   2.468 +
   2.469 +  from ab have "a < b" by simp
   2.470 +  with closed_subset_ex have
   2.471 +    "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and>
   2.472 +     f (Suc (Suc n)) \<notin> closed_int ka kb" .
   2.473 +  hence
   2.474 +    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
   2.475 +     closed_int ka kb \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> closed_int ka kb"
   2.476 +    by simp
   2.477 +  hence
   2.478 +    "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
   2.479 +     e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> e" by simp
   2.480 +  hence
   2.481 +    "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
   2.482 +     ?e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
   2.483 +  with ab ni show
   2.484 +    "\<exists>ka kb. ka < kb \<and>
   2.485 +     newInt (Suc (Suc n)) f = closed_int ka kb \<and>
   2.486 +     newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
   2.487 +     f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto
   2.488 +qed
   2.489 +
   2.490 +lemma newInt_subset:
   2.491 +  "newInt (Suc n) f \<subseteq> newInt n f"
   2.492 +  using newInt_ex by auto
   2.493 +
   2.494 +
   2.495 +text {* Another fundamental property is that no element in the range
   2.496 +of f is in the intersection of all closed intervals generated by
   2.497 +newInt. *}
   2.498 +
   2.499 +lemma newInt_inter:
   2.500 +  "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
   2.501 +proof
   2.502 +  fix n::nat
   2.503 +  {
   2.504 +    assume n0: "n = 0"
   2.505 +    moreover have "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)" by simp
   2.506 +    ultimately have "f n \<notin> newInt n f" by (unfold closed_int_def, simp)
   2.507 +  }
   2.508 +  moreover
   2.509 +  {
   2.510 +    assume "\<not> n = 0"
   2.511 +    hence "n > 0" by simp
   2.512 +    then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc)
   2.513 +
   2.514 +    from newInt_ex have
   2.515 +      "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
   2.516 +       newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
   2.517 +    then have "f (Suc m) \<notin> newInt (Suc m) f" by auto
   2.518 +    with ndef have "f n \<notin> newInt n f" by simp
   2.519 +  }
   2.520 +  ultimately have "f n \<notin> newInt n f" by (rule case_split)
   2.521 +  thus "f n \<notin> (\<Inter>n. newInt n f)" by auto
   2.522 +qed
   2.523 +
   2.524 +
   2.525 +lemma newInt_notempty:
   2.526 +  "(\<Inter>n. newInt n f) \<noteq> {}"
   2.527 +proof -
   2.528 +  let ?g = "\<lambda>n. newInt n f"
   2.529 +  have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
   2.530 +  proof
   2.531 +    fix n
   2.532 +    show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)
   2.533 +  qed
   2.534 +  moreover have "\<forall>n. \<exists>a b. ?g n = closed_int a b \<and> a \<le> b"
   2.535 +  proof
   2.536 +    fix n::nat
   2.537 +    {
   2.538 +      assume "n = 0"
   2.539 +      then have
   2.540 +        "?g n = closed_int (f 0 + 1) (f 0 + 2) \<and> (f 0 + 1 \<le> f 0 + 2)"
   2.541 +        by simp
   2.542 +      hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
   2.543 +    }
   2.544 +    moreover
   2.545 +    {
   2.546 +      assume "\<not> n = 0"
   2.547 +      then have "n > 0" by simp
   2.548 +      then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)
   2.549 +
   2.550 +      have
   2.551 +        "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
   2.552 +        (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
   2.553 +        by (rule newInt_ex)
   2.554 +      then obtain a and b where
   2.555 +        "a < b \<and> (newInt (Suc m) f) = closed_int a b" by auto
   2.556 +      with nd have "?g n = closed_int a b \<and> a \<le> b" by auto
   2.557 +      hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
   2.558 +    }
   2.559 +    ultimately show "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by (rule case_split)
   2.560 +  qed
   2.561 +  ultimately show ?thesis by (rule NIP)
   2.562 +qed
   2.563 +
   2.564 +
   2.565 +section {* Final Theorem *}
   2.566 +
   2.567 +theorem real_non_denum:
   2.568 +  shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
   2.569 +proof -- "by contradiction"
   2.570 +  assume "\<exists>f::nat\<Rightarrow>real. surj f"
   2.571 +  then obtain f::"nat\<Rightarrow>real" where "surj f" by auto
   2.572 +  hence rangeF: "range f = UNIV" by (rule surj_range)
   2.573 +  -- "We now produce a real number x that is not in the range of f, using the properties of newInt. "
   2.574 +  have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
   2.575 +  moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
   2.576 +  ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast
   2.577 +  moreover from rangeF have "x \<in> range f" by simp
   2.578 +  ultimately show False by blast
   2.579 +qed
   2.580 +
   2.581 +end
   2.582 \ No newline at end of file
     3.1 --- a/src/HOL/Real/Real.thy	Sun Feb 12 10:42:19 2006 +0100
     3.2 +++ b/src/HOL/Real/Real.thy	Sun Feb 12 12:29:01 2006 +0100
     3.3 @@ -1,4 +1,4 @@
     3.4  theory Real
     3.5 -imports RComplete RealPow
     3.6 +imports ContNotDenum RealPow
     3.7  begin
     3.8  end
     3.9 \ No newline at end of file
     4.1 --- a/src/HOL/Real/RealDef.thy	Sun Feb 12 10:42:19 2006 +0100
     4.2 +++ b/src/HOL/Real/RealDef.thy	Sun Feb 12 12:29:01 2006 +0100
     4.3 @@ -929,7 +929,6 @@
     4.4  instance real :: number_ring
     4.5  by (intro_classes, simp add: real_number_of_def) 
     4.6  
     4.7 -
     4.8  text{*Collapse applications of @{term real} to @{term number_of}*}
     4.9  lemma real_number_of [simp]: "real (number_of v :: int) = number_of v"
    4.10  by (simp add:  real_of_int_def of_int_number_of_eq)
    4.11 @@ -945,6 +944,19 @@
    4.12  
    4.13  setup real_arith_setup
    4.14  
    4.15 +
    4.16 +lemma real_diff_mult_distrib:
    4.17 +  fixes a::real
    4.18 +  shows "a * (b - c) = a * b - a * c" 
    4.19 +proof -
    4.20 +  have "a * (b - c) = a * (b + -c)" by simp
    4.21 +  also have "\<dots> = (b + -c) * a" by simp
    4.22 +  also have "\<dots> = b*a + (-c)*a" by (rule real_add_mult_distrib)
    4.23 +  also have "\<dots> = a*b - a*c" by simp
    4.24 +  finally show ?thesis .
    4.25 +qed
    4.26 +
    4.27 +
    4.28  subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}
    4.29  
    4.30  text{*Needed in this non-standard form by Hyperreal/Transcendental*}
    4.31 @@ -1027,7 +1039,6 @@
    4.32  done
    4.33  
    4.34  
    4.35 -
    4.36  ML
    4.37  {*
    4.38  val real_lbound_gt_zero = thm"real_lbound_gt_zero";