src/HOL/Integration.thy
changeset 35292 e4a431b6d9b7
parent 35291 ead7bfc30b26
child 35293 06a98796453e
     1.1 --- a/src/HOL/Integration.thy	Mon Feb 22 20:08:10 2010 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,658 +0,0 @@
     1.4 -(*  Author:     Jacques D. Fleuriot, University of Edinburgh
     1.5 -    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     1.6 -*)
     1.7 -
     1.8 -header{*Theory of Integration*}
     1.9 -
    1.10 -theory Integration
    1.11 -imports Deriv ATP_Linkup
    1.12 -begin
    1.13 -
    1.14 -text{*We follow John Harrison in formalizing the Gauge integral.*}
    1.15 -
    1.16 -subsection {* Gauges *}
    1.17 -
    1.18 -definition
    1.19 -  gauge :: "[real set, real => real] => bool" where
    1.20 -  [code del]:"gauge E g = (\<forall>x\<in>E. 0 < g(x))"
    1.21 -
    1.22 -
    1.23 -subsection {* Gauge-fine divisions *}
    1.24 -
    1.25 -inductive
    1.26 -  fine :: "[real \<Rightarrow> real, real \<times> real, (real \<times> real \<times> real) list] \<Rightarrow> bool"
    1.27 -for
    1.28 -  \<delta> :: "real \<Rightarrow> real"
    1.29 -where
    1.30 -  fine_Nil:
    1.31 -    "fine \<delta> (a, a) []"
    1.32 -| fine_Cons:
    1.33 -    "\<lbrakk>fine \<delta> (b, c) D; a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk>
    1.34 -      \<Longrightarrow> fine \<delta> (a, c) ((a, x, b) # D)"
    1.35 -
    1.36 -lemmas fine_induct [induct set: fine] =
    1.37 -  fine.induct [of "\<delta>" "(a,b)" "D" "split P", unfolded split_conv, standard]
    1.38 -
    1.39 -lemma fine_single:
    1.40 -  "\<lbrakk>a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk> \<Longrightarrow> fine \<delta> (a, b) [(a, x, b)]"
    1.41 -by (rule fine_Cons [OF fine_Nil])
    1.42 -
    1.43 -lemma fine_append:
    1.44 -  "\<lbrakk>fine \<delta> (a, b) D; fine \<delta> (b, c) D'\<rbrakk> \<Longrightarrow> fine \<delta> (a, c) (D @ D')"
    1.45 -by (induct set: fine, simp, simp add: fine_Cons)
    1.46 -
    1.47 -lemma fine_imp_le: "fine \<delta> (a, b) D \<Longrightarrow> a \<le> b"
    1.48 -by (induct set: fine, simp_all)
    1.49 -
    1.50 -lemma nonempty_fine_imp_less: "\<lbrakk>fine \<delta> (a, b) D; D \<noteq> []\<rbrakk> \<Longrightarrow> a < b"
    1.51 -apply (induct set: fine, simp)
    1.52 -apply (drule fine_imp_le, simp)
    1.53 -done
    1.54 -
    1.55 -lemma empty_fine_imp_eq: "\<lbrakk>fine \<delta> (a, b) D; D = []\<rbrakk> \<Longrightarrow> a = b"
    1.56 -by (induct set: fine, simp_all)
    1.57 -
    1.58 -lemma fine_eq: "fine \<delta> (a, b) D \<Longrightarrow> a = b \<longleftrightarrow> D = []"
    1.59 -apply (cases "D = []")
    1.60 -apply (drule (1) empty_fine_imp_eq, simp)
    1.61 -apply (drule (1) nonempty_fine_imp_less, simp)
    1.62 -done
    1.63 -
    1.64 -lemma mem_fine:
    1.65 -  "\<lbrakk>fine \<delta> (a, b) D; (u, x, v) \<in> set D\<rbrakk> \<Longrightarrow> u < v \<and> u \<le> x \<and> x \<le> v"
    1.66 -by (induct set: fine, simp, force)
    1.67 -
    1.68 -lemma mem_fine2: "\<lbrakk>fine \<delta> (a, b) D; (u, z, v) \<in> set D\<rbrakk> \<Longrightarrow> a \<le> u \<and> v \<le> b"
    1.69 -apply (induct arbitrary: z u v set: fine, auto)
    1.70 -apply (simp add: fine_imp_le)
    1.71 -apply (erule order_trans [OF less_imp_le], simp)
    1.72 -done
    1.73 -
    1.74 -lemma mem_fine3: "\<lbrakk>fine \<delta> (a, b) D; (u, z, v) \<in> set D\<rbrakk> \<Longrightarrow> v - u < \<delta> z"
    1.75 -by (induct arbitrary: z u v set: fine) auto
    1.76 -
    1.77 -lemma BOLZANO:
    1.78 -  fixes P :: "real \<Rightarrow> real \<Rightarrow> bool"
    1.79 -  assumes 1: "a \<le> b"
    1.80 -  assumes 2: "\<And>a b c. \<lbrakk>P a b; P b c; a \<le> b; b \<le> c\<rbrakk> \<Longrightarrow> P a c"
    1.81 -  assumes 3: "\<And>x. \<exists>d>0. \<forall>a b. a \<le> x & x \<le> b & (b-a) < d \<longrightarrow> P a b"
    1.82 -  shows "P a b"
    1.83 -apply (subgoal_tac "split P (a,b)", simp)
    1.84 -apply (rule lemma_BOLZANO [OF _ _ 1])
    1.85 -apply (clarify, erule (3) 2)
    1.86 -apply (clarify, rule 3)
    1.87 -done
    1.88 -
    1.89 -text{*We can always find a division that is fine wrt any gauge*}
    1.90 -
    1.91 -lemma fine_exists:
    1.92 -  assumes "a \<le> b" and "gauge {a..b} \<delta>" shows "\<exists>D. fine \<delta> (a, b) D"
    1.93 -proof -
    1.94 -  {
    1.95 -    fix u v :: real assume "u \<le> v"
    1.96 -    have "a \<le> u \<Longrightarrow> v \<le> b \<Longrightarrow> \<exists>D. fine \<delta> (u, v) D"
    1.97 -      apply (induct u v rule: BOLZANO, rule `u \<le> v`)
    1.98 -       apply (simp, fast intro: fine_append)
    1.99 -      apply (case_tac "a \<le> x \<and> x \<le> b")
   1.100 -       apply (rule_tac x="\<delta> x" in exI)
   1.101 -       apply (rule conjI)
   1.102 -        apply (simp add: `gauge {a..b} \<delta>` [unfolded gauge_def])
   1.103 -       apply (clarify, rename_tac u v)
   1.104 -       apply (case_tac "u = v")
   1.105 -        apply (fast intro: fine_Nil)
   1.106 -       apply (subgoal_tac "u < v", fast intro: fine_single, simp)
   1.107 -      apply (rule_tac x="1" in exI, clarsimp)
   1.108 -      done
   1.109 -  }
   1.110 -  with `a \<le> b` show ?thesis by auto
   1.111 -qed
   1.112 -
   1.113 -lemma fine_covers_all:
   1.114 -  assumes "fine \<delta> (a, c) D" and "a < x" and "x \<le> c"
   1.115 -  shows "\<exists> N < length D. \<forall> d t e. D ! N = (d,t,e) \<longrightarrow> d < x \<and> x \<le> e"
   1.116 -  using assms
   1.117 -proof (induct set: fine)
   1.118 -  case (2 b c D a t)
   1.119 -  thus ?case
   1.120 -  proof (cases "b < x")
   1.121 -    case True
   1.122 -    with 2 obtain N where *: "N < length D"
   1.123 -      and **: "\<And> d t e. D ! N = (d,t,e) \<Longrightarrow> d < x \<and> x \<le> e" by auto
   1.124 -    hence "Suc N < length ((a,t,b)#D) \<and>
   1.125 -           (\<forall> d t' e. ((a,t,b)#D) ! Suc N = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
   1.126 -    thus ?thesis by auto
   1.127 -  next
   1.128 -    case False with 2
   1.129 -    have "0 < length ((a,t,b)#D) \<and>
   1.130 -           (\<forall> d t' e. ((a,t,b)#D) ! 0 = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
   1.131 -    thus ?thesis by auto
   1.132 -  qed
   1.133 -qed auto
   1.134 -
   1.135 -lemma fine_append_split:
   1.136 -  assumes "fine \<delta> (a,b) D" and "D2 \<noteq> []" and "D = D1 @ D2"
   1.137 -  shows "fine \<delta> (a,fst (hd D2)) D1" (is "?fine1")
   1.138 -  and "fine \<delta> (fst (hd D2), b) D2" (is "?fine2")
   1.139 -proof -
   1.140 -  from assms
   1.141 -  have "?fine1 \<and> ?fine2"
   1.142 -  proof (induct arbitrary: D1 D2)
   1.143 -    case (2 b c D a' x D1 D2)
   1.144 -    note induct = this
   1.145 -
   1.146 -    thus ?case
   1.147 -    proof (cases D1)
   1.148 -      case Nil
   1.149 -      hence "fst (hd D2) = a'" using 2 by auto
   1.150 -      with fine_Cons[OF `fine \<delta> (b,c) D` induct(3,4,5)] Nil induct
   1.151 -      show ?thesis by (auto intro: fine_Nil)
   1.152 -    next
   1.153 -      case (Cons d1 D1')
   1.154 -      with induct(2)[OF `D2 \<noteq> []`, of D1'] induct(8)
   1.155 -      have "fine \<delta> (b, fst (hd D2)) D1'" and "fine \<delta> (fst (hd D2), c) D2" and
   1.156 -        "d1 = (a', x, b)" by auto
   1.157 -      with fine_Cons[OF this(1) induct(3,4,5), OF induct(6)] Cons
   1.158 -      show ?thesis by auto
   1.159 -    qed
   1.160 -  qed auto
   1.161 -  thus ?fine1 and ?fine2 by auto
   1.162 -qed
   1.163 -
   1.164 -lemma fine_\<delta>_expand:
   1.165 -  assumes "fine \<delta> (a,b) D"
   1.166 -  and "\<And> x. \<lbrakk> a \<le> x ; x \<le> b \<rbrakk> \<Longrightarrow> \<delta> x \<le> \<delta>' x"
   1.167 -  shows "fine \<delta>' (a,b) D"
   1.168 -using assms proof induct
   1.169 -  case 1 show ?case by (rule fine_Nil)
   1.170 -next
   1.171 -  case (2 b c D a x)
   1.172 -  show ?case
   1.173 -  proof (rule fine_Cons)
   1.174 -    show "fine \<delta>' (b,c) D" using 2 by auto
   1.175 -    from fine_imp_le[OF 2(1)] 2(6) `x \<le> b`
   1.176 -    show "b - a < \<delta>' x"
   1.177 -      using 2(7)[OF `a \<le> x`] by auto
   1.178 -  qed (auto simp add: 2)
   1.179 -qed
   1.180 -
   1.181 -lemma fine_single_boundaries:
   1.182 -  assumes "fine \<delta> (a,b) D" and "D = [(d, t, e)]"
   1.183 -  shows "a = d \<and> b = e"
   1.184 -using assms proof induct
   1.185 -  case (2 b c  D a x)
   1.186 -  hence "D = []" and "a = d" and "b = e" by auto
   1.187 -  moreover
   1.188 -  from `fine \<delta> (b,c) D` `D = []` have "b = c"
   1.189 -    by (rule empty_fine_imp_eq)
   1.190 -  ultimately show ?case by simp
   1.191 -qed auto
   1.192 -
   1.193 -
   1.194 -subsection {* Riemann sum *}
   1.195 -
   1.196 -definition
   1.197 -  rsum :: "[(real \<times> real \<times> real) list, real \<Rightarrow> real] \<Rightarrow> real" where
   1.198 -  "rsum D f = (\<Sum>(u, x, v)\<leftarrow>D. f x * (v - u))"
   1.199 -
   1.200 -lemma rsum_Nil [simp]: "rsum [] f = 0"
   1.201 -unfolding rsum_def by simp
   1.202 -
   1.203 -lemma rsum_Cons [simp]: "rsum ((u, x, v) # D) f = f x * (v - u) + rsum D f"
   1.204 -unfolding rsum_def by simp
   1.205 -
   1.206 -lemma rsum_zero [simp]: "rsum D (\<lambda>x. 0) = 0"
   1.207 -by (induct D, auto)
   1.208 -
   1.209 -lemma rsum_left_distrib: "rsum D f * c = rsum D (\<lambda>x. f x * c)"
   1.210 -by (induct D, auto simp add: algebra_simps)
   1.211 -
   1.212 -lemma rsum_right_distrib: "c * rsum D f = rsum D (\<lambda>x. c * f x)"
   1.213 -by (induct D, auto simp add: algebra_simps)
   1.214 -
   1.215 -lemma rsum_add: "rsum D (\<lambda>x. f x + g x) =  rsum D f + rsum D g"
   1.216 -by (induct D, auto simp add: algebra_simps)
   1.217 -
   1.218 -lemma rsum_append: "rsum (D1 @ D2) f = rsum D1 f + rsum D2 f"
   1.219 -unfolding rsum_def map_append listsum_append ..
   1.220 -
   1.221 -
   1.222 -subsection {* Gauge integrability (definite) *}
   1.223 -
   1.224 -definition
   1.225 -  Integral :: "[(real*real),real=>real,real] => bool" where
   1.226 -  [code del]: "Integral = (%(a,b) f k. \<forall>e > 0.
   1.227 -                               (\<exists>\<delta>. gauge {a .. b} \<delta> &
   1.228 -                               (\<forall>D. fine \<delta> (a,b) D -->
   1.229 -                                         \<bar>rsum D f - k\<bar> < e)))"
   1.230 -
   1.231 -lemma Integral_def2:
   1.232 -  "Integral = (%(a,b) f k. \<forall>e>0. (\<exists>\<delta>. gauge {a..b} \<delta> &
   1.233 -                               (\<forall>D. fine \<delta> (a,b) D -->
   1.234 -                                         \<bar>rsum D f - k\<bar> \<le> e)))"
   1.235 -unfolding Integral_def
   1.236 -apply (safe intro!: ext)
   1.237 -apply (fast intro: less_imp_le)
   1.238 -apply (drule_tac x="e/2" in spec)
   1.239 -apply force
   1.240 -done
   1.241 -
   1.242 -text{*Lemmas about combining gauges*}
   1.243 -
   1.244 -lemma gauge_min:
   1.245 -     "[| gauge(E) g1; gauge(E) g2 |]
   1.246 -      ==> gauge(E) (%x. min (g1(x)) (g2(x)))"
   1.247 -by (simp add: gauge_def)
   1.248 -
   1.249 -lemma fine_min:
   1.250 -      "fine (%x. min (g1(x)) (g2(x))) (a,b) D
   1.251 -       ==> fine(g1) (a,b) D & fine(g2) (a,b) D"
   1.252 -apply (erule fine.induct)
   1.253 -apply (simp add: fine_Nil)
   1.254 -apply (simp add: fine_Cons)
   1.255 -done
   1.256 -
   1.257 -text{*The integral is unique if it exists*}
   1.258 -
   1.259 -lemma Integral_unique:
   1.260 -    "[| a \<le> b; Integral(a,b) f k1; Integral(a,b) f k2 |] ==> k1 = k2"
   1.261 -apply (simp add: Integral_def)
   1.262 -apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec)+
   1.263 -apply auto
   1.264 -apply (drule gauge_min, assumption)
   1.265 -apply (drule_tac \<delta> = "%x. min (\<delta> x) (\<delta>' x)"
   1.266 -       in fine_exists, assumption, auto)
   1.267 -apply (drule fine_min)
   1.268 -apply (drule spec)+
   1.269 -apply auto
   1.270 -apply (subgoal_tac "\<bar>(rsum D f - k2) - (rsum D f - k1)\<bar> < \<bar>k1 - k2\<bar>")
   1.271 -apply arith
   1.272 -apply (drule add_strict_mono, assumption)
   1.273 -apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] 
   1.274 -                mult_less_cancel_right)
   1.275 -done
   1.276 -
   1.277 -lemma Integral_zero [simp]: "Integral(a,a) f 0"
   1.278 -apply (auto simp add: Integral_def)
   1.279 -apply (rule_tac x = "%x. 1" in exI)
   1.280 -apply (auto dest: fine_eq simp add: gauge_def rsum_def)
   1.281 -done
   1.282 -
   1.283 -lemma fine_rsum_const: "fine \<delta> (a,b) D \<Longrightarrow> rsum D (\<lambda>x. c) = (c * (b - a))"
   1.284 -unfolding rsum_def
   1.285 -by (induct set: fine, auto simp add: algebra_simps)
   1.286 -
   1.287 -lemma Integral_eq_diff_bounds: "a \<le> b ==> Integral(a,b) (%x. 1) (b - a)"
   1.288 -apply (cases "a = b", simp)
   1.289 -apply (simp add: Integral_def, clarify)
   1.290 -apply (rule_tac x = "%x. b - a" in exI)
   1.291 -apply (rule conjI, simp add: gauge_def)
   1.292 -apply (clarify)
   1.293 -apply (subst fine_rsum_const, assumption, simp)
   1.294 -done
   1.295 -
   1.296 -lemma Integral_mult_const: "a \<le> b ==> Integral(a,b) (%x. c)  (c*(b - a))"
   1.297 -apply (cases "a = b", simp)
   1.298 -apply (simp add: Integral_def, clarify)
   1.299 -apply (rule_tac x = "%x. b - a" in exI)
   1.300 -apply (rule conjI, simp add: gauge_def)
   1.301 -apply (clarify)
   1.302 -apply (subst fine_rsum_const, assumption, simp)
   1.303 -done
   1.304 -
   1.305 -lemma Integral_mult:
   1.306 -     "[| a \<le> b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)"
   1.307 -apply (auto simp add: order_le_less 
   1.308 -            dest: Integral_unique [OF order_refl Integral_zero])
   1.309 -apply (auto simp add: Integral_def setsum_right_distrib[symmetric] mult_assoc)
   1.310 -apply (case_tac "c = 0", force)
   1.311 -apply (drule_tac x = "e/abs c" in spec)
   1.312 -apply (simp add: divide_pos_pos)
   1.313 -apply clarify
   1.314 -apply (rule_tac x="\<delta>" in exI, clarify)
   1.315 -apply (drule_tac x="D" in spec, clarify)
   1.316 -apply (simp add: pos_less_divide_eq abs_mult [symmetric]
   1.317 -                 algebra_simps rsum_right_distrib)
   1.318 -done
   1.319 -
   1.320 -lemma Integral_add:
   1.321 -  assumes "Integral (a, b) f x1"
   1.322 -  assumes "Integral (b, c) f x2"
   1.323 -  assumes "a \<le> b" and "b \<le> c"
   1.324 -  shows "Integral (a, c) f (x1 + x2)"
   1.325 -proof (cases "a < b \<and> b < c", simp only: Integral_def split_conv, rule allI, rule impI)
   1.326 -  fix \<epsilon> :: real assume "0 < \<epsilon>"
   1.327 -  hence "0 < \<epsilon> / 2" by auto
   1.328 -
   1.329 -  assume "a < b \<and> b < c"
   1.330 -  hence "a < b" and "b < c" by auto
   1.331 -
   1.332 -  from `Integral (a, b) f x1`[simplified Integral_def split_conv,
   1.333 -                              rule_format, OF `0 < \<epsilon>/2`]
   1.334 -  obtain \<delta>1 where \<delta>1_gauge: "gauge {a..b} \<delta>1"
   1.335 -    and I1: "\<And> D. fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f - x1 \<bar> < (\<epsilon> / 2)" by auto
   1.336 -
   1.337 -  from `Integral (b, c) f x2`[simplified Integral_def split_conv,
   1.338 -                              rule_format, OF `0 < \<epsilon>/2`]
   1.339 -  obtain \<delta>2 where \<delta>2_gauge: "gauge {b..c} \<delta>2"
   1.340 -    and I2: "\<And> D. fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)" by auto
   1.341 -
   1.342 -  def \<delta> \<equiv> "\<lambda> x. if x < b then min (\<delta>1 x) (b - x)
   1.343 -           else if x = b then min (\<delta>1 b) (\<delta>2 b)
   1.344 -                         else min (\<delta>2 x) (x - b)"
   1.345 -
   1.346 -  have "gauge {a..c} \<delta>"
   1.347 -    using \<delta>1_gauge \<delta>2_gauge unfolding \<delta>_def gauge_def by auto
   1.348 -  moreover {
   1.349 -    fix D :: "(real \<times> real \<times> real) list"
   1.350 -    assume fine: "fine \<delta> (a,c) D"
   1.351 -    from fine_covers_all[OF this `a < b` `b \<le> c`]
   1.352 -    obtain N where "N < length D"
   1.353 -      and *: "\<forall> d t e. D ! N = (d, t, e) \<longrightarrow> d < b \<and> b \<le> e"
   1.354 -      by auto
   1.355 -    obtain d t e where D_eq: "D ! N = (d, t, e)" by (cases "D!N", auto)
   1.356 -    with * have "d < b" and "b \<le> e" by auto
   1.357 -    have in_D: "(d, t, e) \<in> set D"
   1.358 -      using D_eq[symmetric] using `N < length D` by auto
   1.359 -
   1.360 -    from mem_fine[OF fine in_D]
   1.361 -    have "d < e" and "d \<le> t" and "t \<le> e" by auto
   1.362 -
   1.363 -    have "t = b"
   1.364 -    proof (rule ccontr)
   1.365 -      assume "t \<noteq> b"
   1.366 -      with mem_fine3[OF fine in_D] `b \<le> e` `d \<le> t` `t \<le> e` `d < b` \<delta>_def
   1.367 -      show False by (cases "t < b") auto
   1.368 -    qed
   1.369 -
   1.370 -    let ?D1 = "take N D"
   1.371 -    let ?D2 = "drop N D"
   1.372 -    def D1 \<equiv> "take N D @ [(d, t, b)]"
   1.373 -    def D2 \<equiv> "(if b = e then [] else [(b, t, e)]) @ drop (Suc N) D"
   1.374 -
   1.375 -    have "D \<noteq> []" using `N < length D` by auto
   1.376 -    from hd_drop_conv_nth[OF this `N < length D`]
   1.377 -    have "fst (hd ?D2) = d" using `D ! N = (d, t, e)` by auto
   1.378 -    with fine_append_split[OF _ _ append_take_drop_id[symmetric]]
   1.379 -    have fine1: "fine \<delta> (a,d) ?D1" and fine2: "fine \<delta> (d,c) ?D2"
   1.380 -      using `N < length D` fine by auto
   1.381 -
   1.382 -    have "fine \<delta>1 (a,b) D1" unfolding D1_def
   1.383 -    proof (rule fine_append)
   1.384 -      show "fine \<delta>1 (a, d) ?D1"
   1.385 -      proof (rule fine1[THEN fine_\<delta>_expand])
   1.386 -        fix x assume "a \<le> x" "x \<le> d"
   1.387 -        hence "x \<le> b" using `d < b` `x \<le> d` by auto
   1.388 -        thus "\<delta> x \<le> \<delta>1 x" unfolding \<delta>_def by auto
   1.389 -      qed
   1.390 -
   1.391 -      have "b - d < \<delta>1 t"
   1.392 -        using mem_fine3[OF fine in_D] \<delta>_def `b \<le> e` `t = b` by auto
   1.393 -      from `d < b` `d \<le> t` `t = b` this
   1.394 -      show "fine \<delta>1 (d, b) [(d, t, b)]" using fine_single by auto
   1.395 -    qed
   1.396 -    note rsum1 = I1[OF this]
   1.397 -
   1.398 -    have drop_split: "drop N D = [D ! N] @ drop (Suc N) D"
   1.399 -      using nth_drop'[OF `N < length D`] by simp
   1.400 -
   1.401 -    have fine2: "fine \<delta>2 (e,c) (drop (Suc N) D)"
   1.402 -    proof (cases "drop (Suc N) D = []")
   1.403 -      case True
   1.404 -      note * = fine2[simplified drop_split True D_eq append_Nil2]
   1.405 -      have "e = c" using fine_single_boundaries[OF * refl] by auto
   1.406 -      thus ?thesis unfolding True using fine_Nil by auto
   1.407 -    next
   1.408 -      case False
   1.409 -      note * = fine_append_split[OF fine2 False drop_split]
   1.410 -      from fine_single_boundaries[OF *(1)]
   1.411 -      have "fst (hd (drop (Suc N) D)) = e" using D_eq by auto
   1.412 -      with *(2) have "fine \<delta> (e,c) (drop (Suc N) D)" by auto
   1.413 -      thus ?thesis
   1.414 -      proof (rule fine_\<delta>_expand)
   1.415 -        fix x assume "e \<le> x" and "x \<le> c"
   1.416 -        thus "\<delta> x \<le> \<delta>2 x" using `b \<le> e` unfolding \<delta>_def by auto
   1.417 -      qed
   1.418 -    qed
   1.419 -
   1.420 -    have "fine \<delta>2 (b, c) D2"
   1.421 -    proof (cases "e = b")
   1.422 -      case True thus ?thesis using fine2 by (simp add: D1_def D2_def)
   1.423 -    next
   1.424 -      case False
   1.425 -      have "e - b < \<delta>2 b"
   1.426 -        using mem_fine3[OF fine in_D] \<delta>_def `d < b` `t = b` by auto
   1.427 -      with False `t = b` `b \<le> e`
   1.428 -      show ?thesis using D2_def
   1.429 -        by (auto intro!: fine_append[OF _ fine2] fine_single
   1.430 -               simp del: append_Cons)
   1.431 -    qed
   1.432 -    note rsum2 = I2[OF this]
   1.433 -
   1.434 -    have "rsum D f = rsum (take N D) f + rsum [D ! N] f + rsum (drop (Suc N) D) f"
   1.435 -      using rsum_append[symmetric] nth_drop'[OF `N < length D`] by auto
   1.436 -    also have "\<dots> = rsum D1 f + rsum D2 f"
   1.437 -      by (cases "b = e", auto simp add: D1_def D2_def D_eq rsum_append algebra_simps)
   1.438 -    finally have "\<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>"
   1.439 -      using add_strict_mono[OF rsum1 rsum2] by simp
   1.440 -  }
   1.441 -  ultimately show "\<exists> \<delta>. gauge {a .. c} \<delta> \<and>
   1.442 -    (\<forall>D. fine \<delta> (a,c) D \<longrightarrow> \<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>)"
   1.443 -    by blast
   1.444 -next
   1.445 -  case False
   1.446 -  hence "a = b \<or> b = c" using `a \<le> b` and `b \<le> c` by auto
   1.447 -  thus ?thesis
   1.448 -  proof (rule disjE)
   1.449 -    assume "a = b" hence "x1 = 0"
   1.450 -      using `Integral (a, b) f x1` Integral_zero Integral_unique[of a b] by auto
   1.451 -    thus ?thesis using `a = b` `Integral (b, c) f x2` by auto
   1.452 -  next
   1.453 -    assume "b = c" hence "x2 = 0"
   1.454 -      using `Integral (b, c) f x2` Integral_zero Integral_unique[of b c] by auto
   1.455 -    thus ?thesis using `b = c` `Integral (a, b) f x1` by auto
   1.456 -  qed
   1.457 -qed
   1.458 -
   1.459 -text{*Fundamental theorem of calculus (Part I)*}
   1.460 -
   1.461 -text{*"Straddle Lemma" : Swartz and Thompson: AMM 95(7) 1988 *}
   1.462 -
   1.463 -lemma strad1:
   1.464 -       "\<lbrakk>\<forall>z::real. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow>
   1.465 -             \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2;
   1.466 -        0 < s; 0 < e; a \<le> x; x \<le> b\<rbrakk>
   1.467 -       \<Longrightarrow> \<forall>z. \<bar>z - x\<bar> < s -->\<bar>f z - f x - f' x * (z - x)\<bar> \<le> e/2 * \<bar>z - x\<bar>"
   1.468 -apply clarify
   1.469 -apply (case_tac "z = x", simp)
   1.470 -apply (drule_tac x = z in spec)
   1.471 -apply (rule_tac z1 = "\<bar>inverse (z - x)\<bar>" 
   1.472 -       in real_mult_le_cancel_iff2 [THEN iffD1])
   1.473 - apply simp
   1.474 -apply (simp del: abs_inverse abs_mult add: abs_mult [symmetric]
   1.475 -          mult_assoc [symmetric])
   1.476 -apply (subgoal_tac "inverse (z - x) * (f z - f x - f' x * (z - x)) 
   1.477 -                    = (f z - f x) / (z - x) - f' x")
   1.478 - apply (simp add: abs_mult [symmetric] mult_ac diff_minus)
   1.479 -apply (subst mult_commute)
   1.480 -apply (simp add: left_distrib diff_minus)
   1.481 -apply (simp add: mult_assoc divide_inverse)
   1.482 -apply (simp add: left_distrib)
   1.483 -done
   1.484 -
   1.485 -lemma lemma_straddle:
   1.486 -  assumes f': "\<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x)" and "0 < e"
   1.487 -  shows "\<exists>g. gauge {a..b} g &
   1.488 -                (\<forall>x u v. a \<le> u & u \<le> x & x \<le> v & v \<le> b & (v - u) < g(x)
   1.489 -                  --> \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))"
   1.490 -proof -
   1.491 -  have "\<forall>x\<in>{a..b}.
   1.492 -        (\<exists>d > 0. \<forall>u v. u \<le> x & x \<le> v & (v - u) < d --> 
   1.493 -                       \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))"
   1.494 -  proof (clarsimp)
   1.495 -    fix x :: real assume "a \<le> x" and "x \<le> b"
   1.496 -    with f' have "DERIV f x :> f'(x)" by simp
   1.497 -    then have "\<forall>r>0. \<exists>s>0. \<forall>z. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < r"
   1.498 -      by (simp add: DERIV_iff2 LIM_eq)
   1.499 -    with `0 < e` obtain s
   1.500 -    where "\<forall>z. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2" and "0 < s"
   1.501 -      by (drule_tac x="e/2" in spec, auto)
   1.502 -    then have strad [rule_format]:
   1.503 -        "\<forall>z. \<bar>z - x\<bar> < s --> \<bar>f z - f x - f' x * (z - x)\<bar> \<le> e/2 * \<bar>z - x\<bar>"
   1.504 -      using `0 < e` `a \<le> x` `x \<le> b` by (rule strad1)
   1.505 -    show "\<exists>d>0. \<forall>u v. u \<le> x \<and> x \<le> v \<and> v - u < d \<longrightarrow> \<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u)"
   1.506 -    proof (safe intro!: exI)
   1.507 -      show "0 < s" by fact
   1.508 -    next
   1.509 -      fix u v :: real assume "u \<le> x" and "x \<le> v" and "v - u < s"
   1.510 -      have "\<bar>f v - f u - f' x * (v - u)\<bar> =
   1.511 -            \<bar>(f v - f x - f' x * (v - x)) + (f x - f u - f' x * (x - u))\<bar>"
   1.512 -        by (simp add: right_diff_distrib)
   1.513 -      also have "\<dots> \<le> \<bar>f v - f x - f' x * (v - x)\<bar> + \<bar>f x - f u - f' x * (x - u)\<bar>"
   1.514 -        by (rule abs_triangle_ineq)
   1.515 -      also have "\<dots> = \<bar>f v - f x - f' x * (v - x)\<bar> + \<bar>f u - f x - f' x * (u - x)\<bar>"
   1.516 -        by (simp add: right_diff_distrib)
   1.517 -      also have "\<dots> \<le> (e/2) * \<bar>v - x\<bar> + (e/2) * \<bar>u - x\<bar>"
   1.518 -        using `u \<le> x` `x \<le> v` `v - u < s` by (intro add_mono strad, simp_all)
   1.519 -      also have "\<dots> \<le> e * (v - u) / 2 + e * (v - u) / 2"
   1.520 -        using `u \<le> x` `x \<le> v` `0 < e` by (intro add_mono, simp_all)
   1.521 -      also have "\<dots> = e * (v - u)"
   1.522 -        by simp
   1.523 -      finally show "\<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u)" .
   1.524 -    qed
   1.525 -  qed
   1.526 -  thus ?thesis
   1.527 -    by (simp add: gauge_def) (drule bchoice, auto)
   1.528 -qed
   1.529 -
   1.530 -lemma fine_listsum_eq_diff:
   1.531 -  fixes f :: "real \<Rightarrow> real"
   1.532 -  shows "fine \<delta> (a, b) D \<Longrightarrow> (\<Sum>(u, x, v)\<leftarrow>D. f v - f u) = f b - f a"
   1.533 -by (induct set: fine) simp_all
   1.534 -
   1.535 -lemma FTC1: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
   1.536 -             ==> Integral(a,b) f' (f(b) - f(a))"
   1.537 - apply (drule order_le_imp_less_or_eq, auto)
   1.538 - apply (auto simp add: Integral_def2)
   1.539 - apply (drule_tac e = "e / (b - a)" in lemma_straddle)
   1.540 -  apply (simp add: divide_pos_pos)
   1.541 - apply clarify
   1.542 - apply (rule_tac x="g" in exI, clarify)
   1.543 - apply (clarsimp simp add: rsum_def)
   1.544 - apply (frule fine_listsum_eq_diff [where f=f])
   1.545 - apply (erule subst)
   1.546 - apply (subst listsum_subtractf [symmetric])
   1.547 - apply (rule listsum_abs [THEN order_trans])
   1.548 - apply (subst map_map [unfolded o_def])
   1.549 - apply (subgoal_tac "e = (\<Sum>(u, x, v)\<leftarrow>D. (e / (b - a)) * (v - u))")
   1.550 -  apply (erule ssubst)
   1.551 -  apply (simp add: abs_minus_commute)
   1.552 -  apply (rule listsum_mono)
   1.553 -  apply (clarify, rename_tac u x v)
   1.554 -  apply ((drule spec)+, erule mp)
   1.555 -  apply (simp add: mem_fine mem_fine2 mem_fine3)
   1.556 - apply (frule fine_listsum_eq_diff [where f="\<lambda>x. x"])
   1.557 - apply (simp only: split_def)
   1.558 - apply (subst listsum_const_mult)
   1.559 - apply simp
   1.560 -done
   1.561 -
   1.562 -lemma Integral_subst: "[| Integral(a,b) f k1; k2=k1 |] ==> Integral(a,b) f k2"
   1.563 -by simp
   1.564 -
   1.565 -subsection {* Additivity Theorem of Gauge Integral *}
   1.566 -
   1.567 -text{* Bartle/Sherbert: Theorem 10.1.5 p. 278 *}
   1.568 -lemma Integral_add_fun:
   1.569 -    "[| a \<le> b; Integral(a,b) f k1; Integral(a,b) g k2 |]
   1.570 -     ==> Integral(a,b) (%x. f x + g x) (k1 + k2)"
   1.571 -unfolding Integral_def
   1.572 -apply clarify
   1.573 -apply (drule_tac x = "e/2" in spec)+
   1.574 -apply clarsimp
   1.575 -apply (rule_tac x = "\<lambda>x. min (\<delta> x) (\<delta>' x)" in exI)
   1.576 -apply (rule conjI, erule (1) gauge_min)
   1.577 -apply clarify
   1.578 -apply (drule fine_min)
   1.579 -apply (drule_tac x=D in spec, simp)+
   1.580 -apply (drule_tac a = "\<bar>rsum D f - k1\<bar> * 2" and c = "\<bar>rsum D g - k2\<bar> * 2" in add_strict_mono, assumption)
   1.581 -apply (auto simp only: rsum_add left_distrib [symmetric]
   1.582 -                mult_2_right [symmetric] real_mult_less_iff1)
   1.583 -done
   1.584 -
   1.585 -lemma lemma_Integral_rsum_le:
   1.586 -     "[| \<forall>x. a \<le> x & x \<le> b --> f x \<le> g x;
   1.587 -         fine \<delta> (a,b) D
   1.588 -      |] ==> rsum D f \<le> rsum D g"
   1.589 -unfolding rsum_def
   1.590 -apply (rule listsum_mono)
   1.591 -apply clarify
   1.592 -apply (rule mult_right_mono)
   1.593 -apply (drule spec, erule mp)
   1.594 -apply (frule (1) mem_fine)
   1.595 -apply (frule (1) mem_fine2)
   1.596 -apply simp
   1.597 -apply (frule (1) mem_fine)
   1.598 -apply simp
   1.599 -done
   1.600 -
   1.601 -lemma Integral_le:
   1.602 -    "[| a \<le> b;
   1.603 -        \<forall>x. a \<le> x & x \<le> b --> f(x) \<le> g(x);
   1.604 -        Integral(a,b) f k1; Integral(a,b) g k2
   1.605 -     |] ==> k1 \<le> k2"
   1.606 -apply (simp add: Integral_def)
   1.607 -apply (rotate_tac 2)
   1.608 -apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec)
   1.609 -apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec, auto)
   1.610 -apply (drule gauge_min, assumption)
   1.611 -apply (drule_tac \<delta> = "\<lambda>x. min (\<delta> x) (\<delta>' x)" in fine_exists, assumption, clarify)
   1.612 -apply (drule fine_min)
   1.613 -apply (drule_tac x = D in spec, drule_tac x = D in spec, clarsimp)
   1.614 -apply (frule lemma_Integral_rsum_le, assumption)
   1.615 -apply (subgoal_tac "\<bar>(rsum D f - k1) - (rsum D g - k2)\<bar> < \<bar>k1 - k2\<bar>")
   1.616 -apply arith
   1.617 -apply (drule add_strict_mono, assumption)
   1.618 -apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
   1.619 -                       real_mult_less_iff1)
   1.620 -done
   1.621 -
   1.622 -lemma Integral_imp_Cauchy:
   1.623 -     "(\<exists>k. Integral(a,b) f k) ==>
   1.624 -      (\<forall>e > 0. \<exists>\<delta>. gauge {a..b} \<delta> &
   1.625 -                       (\<forall>D1 D2.
   1.626 -                            fine \<delta> (a,b) D1 &
   1.627 -                            fine \<delta> (a,b) D2 -->
   1.628 -                            \<bar>rsum D1 f - rsum D2 f\<bar> < e))"
   1.629 -apply (simp add: Integral_def, auto)
   1.630 -apply (drule_tac x = "e/2" in spec, auto)
   1.631 -apply (rule exI, auto)
   1.632 -apply (frule_tac x = D1 in spec)
   1.633 -apply (drule_tac x = D2 in spec)
   1.634 -apply simp
   1.635 -apply (thin_tac "0 < e")
   1.636 -apply (drule add_strict_mono, assumption)
   1.637 -apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
   1.638 -                       real_mult_less_iff1)
   1.639 -done
   1.640 -
   1.641 -lemma Cauchy_iff2:
   1.642 -     "Cauchy X =
   1.643 -      (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))"
   1.644 -apply (simp add: Cauchy_iff, auto)
   1.645 -apply (drule reals_Archimedean, safe)
   1.646 -apply (drule_tac x = n in spec, auto)
   1.647 -apply (rule_tac x = M in exI, auto)
   1.648 -apply (drule_tac x = m in spec, simp)
   1.649 -apply (drule_tac x = na in spec, auto)
   1.650 -done
   1.651 -
   1.652 -lemma monotonic_anti_derivative:
   1.653 -  fixes f g :: "real => real" shows
   1.654 -     "[| a \<le> b; \<forall>c. a \<le> c & c \<le> b --> f' c \<le> g' c;
   1.655 -         \<forall>x. DERIV f x :> f' x; \<forall>x. DERIV g x :> g' x |]
   1.656 -      ==> f b - f a \<le> g b - g a"
   1.657 -apply (rule Integral_le, assumption)
   1.658 -apply (auto intro: FTC1) 
   1.659 -done
   1.660 -
   1.661 -end