src/HOL/ex/Gauge_Integration.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 37765 26bdfb7b680b
child 45605 a89b4bc311a5
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     1 (*  Author:     Jacques D. Fleuriot, University of Edinburgh
     2     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     3 
     4     Replaced by ~~/src/HOL/Multivariate_Analysis/Real_Integral.thy .
     5 *)
     6 
     7 header{*Theory of Integration on real intervals*}
     8 
     9 theory Gauge_Integration
    10 imports Complex_Main
    11 begin
    12 
    13 text {*
    14 
    15 \textbf{Attention}: This theory defines the Integration on real
    16 intervals.  This is just a example theory for historical / expository interests.
    17 A better replacement is found in the Multivariate Analysis library. This defines
    18 the gauge integral on real vector spaces and in the Real Integral theory
    19 is a specialization to the integral on arbitrary real intervals.  The
    20 Multivariate Analysis package also provides a better support for analysis on
    21 integrals.
    22 
    23 *}
    24 
    25 text{*We follow John Harrison in formalizing the Gauge integral.*}
    26 
    27 subsection {* Gauges *}
    28 
    29 definition
    30   gauge :: "[real set, real => real] => bool" where
    31   "gauge E g = (\<forall>x\<in>E. 0 < g(x))"
    32 
    33 
    34 subsection {* Gauge-fine divisions *}
    35 
    36 inductive
    37   fine :: "[real \<Rightarrow> real, real \<times> real, (real \<times> real \<times> real) list] \<Rightarrow> bool"
    38 for
    39   \<delta> :: "real \<Rightarrow> real"
    40 where
    41   fine_Nil:
    42     "fine \<delta> (a, a) []"
    43 | fine_Cons:
    44     "\<lbrakk>fine \<delta> (b, c) D; a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk>
    45       \<Longrightarrow> fine \<delta> (a, c) ((a, x, b) # D)"
    46 
    47 lemmas fine_induct [induct set: fine] =
    48   fine.induct [of "\<delta>" "(a,b)" "D" "split P", unfolded split_conv, standard]
    49 
    50 lemma fine_single:
    51   "\<lbrakk>a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk> \<Longrightarrow> fine \<delta> (a, b) [(a, x, b)]"
    52 by (rule fine_Cons [OF fine_Nil])
    53 
    54 lemma fine_append:
    55   "\<lbrakk>fine \<delta> (a, b) D; fine \<delta> (b, c) D'\<rbrakk> \<Longrightarrow> fine \<delta> (a, c) (D @ D')"
    56 by (induct set: fine, simp, simp add: fine_Cons)
    57 
    58 lemma fine_imp_le: "fine \<delta> (a, b) D \<Longrightarrow> a \<le> b"
    59 by (induct set: fine, simp_all)
    60 
    61 lemma nonempty_fine_imp_less: "\<lbrakk>fine \<delta> (a, b) D; D \<noteq> []\<rbrakk> \<Longrightarrow> a < b"
    62 apply (induct set: fine, simp)
    63 apply (drule fine_imp_le, simp)
    64 done
    65 
    66 lemma fine_Nil_iff: "fine \<delta> (a, b) [] \<longleftrightarrow> a = b"
    67 by (auto elim: fine.cases intro: fine.intros)
    68 
    69 lemma fine_same_iff: "fine \<delta> (a, a) D \<longleftrightarrow> D = []"
    70 proof
    71   assume "fine \<delta> (a, a) D" thus "D = []"
    72     by (metis nonempty_fine_imp_less less_irrefl)
    73 next
    74   assume "D = []" thus "fine \<delta> (a, a) D"
    75     by (simp add: fine_Nil)
    76 qed
    77 
    78 lemma empty_fine_imp_eq: "\<lbrakk>fine \<delta> (a, b) D; D = []\<rbrakk> \<Longrightarrow> a = b"
    79 by (simp add: fine_Nil_iff)
    80 
    81 lemma mem_fine:
    82   "\<lbrakk>fine \<delta> (a, b) D; (u, x, v) \<in> set D\<rbrakk> \<Longrightarrow> u < v \<and> u \<le> x \<and> x \<le> v"
    83 by (induct set: fine, simp, force)
    84 
    85 lemma mem_fine2: "\<lbrakk>fine \<delta> (a, b) D; (u, z, v) \<in> set D\<rbrakk> \<Longrightarrow> a \<le> u \<and> v \<le> b"
    86 apply (induct arbitrary: z u v set: fine, auto)
    87 apply (simp add: fine_imp_le)
    88 apply (erule order_trans [OF less_imp_le], simp)
    89 done
    90 
    91 lemma mem_fine3: "\<lbrakk>fine \<delta> (a, b) D; (u, z, v) \<in> set D\<rbrakk> \<Longrightarrow> v - u < \<delta> z"
    92 by (induct arbitrary: z u v set: fine) auto
    93 
    94 lemma BOLZANO:
    95   fixes P :: "real \<Rightarrow> real \<Rightarrow> bool"
    96   assumes 1: "a \<le> b"
    97   assumes 2: "\<And>a b c. \<lbrakk>P a b; P b c; a \<le> b; b \<le> c\<rbrakk> \<Longrightarrow> P a c"
    98   assumes 3: "\<And>x. \<exists>d>0. \<forall>a b. a \<le> x & x \<le> b & (b-a) < d \<longrightarrow> P a b"
    99   shows "P a b"
   100 apply (subgoal_tac "split P (a,b)", simp)
   101 apply (rule lemma_BOLZANO [OF _ _ 1])
   102 apply (clarify, erule (3) 2)
   103 apply (clarify, rule 3)
   104 done
   105 
   106 text{*We can always find a division that is fine wrt any gauge*}
   107 
   108 lemma fine_exists:
   109   assumes "a \<le> b" and "gauge {a..b} \<delta>" shows "\<exists>D. fine \<delta> (a, b) D"
   110 proof -
   111   {
   112     fix u v :: real assume "u \<le> v"
   113     have "a \<le> u \<Longrightarrow> v \<le> b \<Longrightarrow> \<exists>D. fine \<delta> (u, v) D"
   114       apply (induct u v rule: BOLZANO, rule `u \<le> v`)
   115        apply (simp, fast intro: fine_append)
   116       apply (case_tac "a \<le> x \<and> x \<le> b")
   117        apply (rule_tac x="\<delta> x" in exI)
   118        apply (rule conjI)
   119         apply (simp add: `gauge {a..b} \<delta>` [unfolded gauge_def])
   120        apply (clarify, rename_tac u v)
   121        apply (case_tac "u = v")
   122         apply (fast intro: fine_Nil)
   123        apply (subgoal_tac "u < v", fast intro: fine_single, simp)
   124       apply (rule_tac x="1" in exI, clarsimp)
   125       done
   126   }
   127   with `a \<le> b` show ?thesis by auto
   128 qed
   129 
   130 lemma fine_covers_all:
   131   assumes "fine \<delta> (a, c) D" and "a < x" and "x \<le> c"
   132   shows "\<exists> N < length D. \<forall> d t e. D ! N = (d,t,e) \<longrightarrow> d < x \<and> x \<le> e"
   133   using assms
   134 proof (induct set: fine)
   135   case (2 b c D a t)
   136   thus ?case
   137   proof (cases "b < x")
   138     case True
   139     with 2 obtain N where *: "N < length D"
   140       and **: "\<And> d t e. D ! N = (d,t,e) \<Longrightarrow> d < x \<and> x \<le> e" by auto
   141     hence "Suc N < length ((a,t,b)#D) \<and>
   142            (\<forall> d t' e. ((a,t,b)#D) ! Suc N = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
   143     thus ?thesis by auto
   144   next
   145     case False with 2
   146     have "0 < length ((a,t,b)#D) \<and>
   147            (\<forall> d t' e. ((a,t,b)#D) ! 0 = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
   148     thus ?thesis by auto
   149   qed
   150 qed auto
   151 
   152 lemma fine_append_split:
   153   assumes "fine \<delta> (a,b) D" and "D2 \<noteq> []" and "D = D1 @ D2"
   154   shows "fine \<delta> (a,fst (hd D2)) D1" (is "?fine1")
   155   and "fine \<delta> (fst (hd D2), b) D2" (is "?fine2")
   156 proof -
   157   from assms
   158   have "?fine1 \<and> ?fine2"
   159   proof (induct arbitrary: D1 D2)
   160     case (2 b c D a' x D1 D2)
   161     note induct = this
   162 
   163     thus ?case
   164     proof (cases D1)
   165       case Nil
   166       hence "fst (hd D2) = a'" using 2 by auto
   167       with fine_Cons[OF `fine \<delta> (b,c) D` induct(3,4,5)] Nil induct
   168       show ?thesis by (auto intro: fine_Nil)
   169     next
   170       case (Cons d1 D1')
   171       with induct(2)[OF `D2 \<noteq> []`, of D1'] induct(8)
   172       have "fine \<delta> (b, fst (hd D2)) D1'" and "fine \<delta> (fst (hd D2), c) D2" and
   173         "d1 = (a', x, b)" by auto
   174       with fine_Cons[OF this(1) induct(3,4,5), OF induct(6)] Cons
   175       show ?thesis by auto
   176     qed
   177   qed auto
   178   thus ?fine1 and ?fine2 by auto
   179 qed
   180 
   181 lemma fine_\<delta>_expand:
   182   assumes "fine \<delta> (a,b) D"
   183   and "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> \<delta> x \<le> \<delta>' x"
   184   shows "fine \<delta>' (a,b) D"
   185 using assms proof induct
   186   case 1 show ?case by (rule fine_Nil)
   187 next
   188   case (2 b c D a x)
   189   show ?case
   190   proof (rule fine_Cons)
   191     show "fine \<delta>' (b,c) D" using 2 by auto
   192     from fine_imp_le[OF 2(1)] 2(6) `x \<le> b`
   193     show "b - a < \<delta>' x"
   194       using 2(7)[OF `a \<le> x`] by auto
   195   qed (auto simp add: 2)
   196 qed
   197 
   198 lemma fine_single_boundaries:
   199   assumes "fine \<delta> (a,b) D" and "D = [(d, t, e)]"
   200   shows "a = d \<and> b = e"
   201 using assms proof induct
   202   case (2 b c  D a x)
   203   hence "D = []" and "a = d" and "b = e" by auto
   204   moreover
   205   from `fine \<delta> (b,c) D` `D = []` have "b = c"
   206     by (rule empty_fine_imp_eq)
   207   ultimately show ?case by simp
   208 qed auto
   209 
   210 lemma fine_listsum_eq_diff:
   211   fixes f :: "real \<Rightarrow> real"
   212   shows "fine \<delta> (a, b) D \<Longrightarrow> (\<Sum>(u, x, v)\<leftarrow>D. f v - f u) = f b - f a"
   213 by (induct set: fine) simp_all
   214 
   215 text{*Lemmas about combining gauges*}
   216 
   217 lemma gauge_min:
   218      "[| gauge(E) g1; gauge(E) g2 |]
   219       ==> gauge(E) (%x. min (g1(x)) (g2(x)))"
   220 by (simp add: gauge_def)
   221 
   222 lemma fine_min:
   223       "fine (%x. min (g1(x)) (g2(x))) (a,b) D
   224        ==> fine(g1) (a,b) D & fine(g2) (a,b) D"
   225 apply (erule fine.induct)
   226 apply (simp add: fine_Nil)
   227 apply (simp add: fine_Cons)
   228 done
   229 
   230 subsection {* Riemann sum *}
   231 
   232 definition
   233   rsum :: "[(real \<times> real \<times> real) list, real \<Rightarrow> real] \<Rightarrow> real" where
   234   "rsum D f = (\<Sum>(u, x, v)\<leftarrow>D. f x * (v - u))"
   235 
   236 lemma rsum_Nil [simp]: "rsum [] f = 0"
   237 unfolding rsum_def by simp
   238 
   239 lemma rsum_Cons [simp]: "rsum ((u, x, v) # D) f = f x * (v - u) + rsum D f"
   240 unfolding rsum_def by simp
   241 
   242 lemma rsum_zero [simp]: "rsum D (\<lambda>x. 0) = 0"
   243 by (induct D, auto)
   244 
   245 lemma rsum_left_distrib: "rsum D f * c = rsum D (\<lambda>x. f x * c)"
   246 by (induct D, auto simp add: algebra_simps)
   247 
   248 lemma rsum_right_distrib: "c * rsum D f = rsum D (\<lambda>x. c * f x)"
   249 by (induct D, auto simp add: algebra_simps)
   250 
   251 lemma rsum_add: "rsum D (\<lambda>x. f x + g x) =  rsum D f + rsum D g"
   252 by (induct D, auto simp add: algebra_simps)
   253 
   254 lemma rsum_append: "rsum (D1 @ D2) f = rsum D1 f + rsum D2 f"
   255 unfolding rsum_def map_append listsum_append ..
   256 
   257 
   258 subsection {* Gauge integrability (definite) *}
   259 
   260 definition
   261   Integral :: "[(real*real),real=>real,real] => bool" where
   262   "Integral = (%(a,b) f k. \<forall>e > 0.
   263                                (\<exists>\<delta>. gauge {a .. b} \<delta> &
   264                                (\<forall>D. fine \<delta> (a,b) D -->
   265                                          \<bar>rsum D f - k\<bar> < e)))"
   266 
   267 lemma Integral_eq:
   268   "Integral (a, b) f k \<longleftrightarrow>
   269     (\<forall>e>0. \<exists>\<delta>. gauge {a..b} \<delta> \<and> (\<forall>D. fine \<delta> (a,b) D \<longrightarrow> \<bar>rsum D f - k\<bar> < e))"
   270 unfolding Integral_def by simp
   271 
   272 lemma IntegralI:
   273   assumes "\<And>e. 0 < e \<Longrightarrow>
   274     \<exists>\<delta>. gauge {a..b} \<delta> \<and> (\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f - k\<bar> < e)"
   275   shows "Integral (a, b) f k"
   276 using assms unfolding Integral_def by auto
   277 
   278 lemma IntegralE:
   279   assumes "Integral (a, b) f k" and "0 < e"
   280   obtains \<delta> where "gauge {a..b} \<delta>" and "\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f - k\<bar> < e"
   281 using assms unfolding Integral_def by auto
   282 
   283 lemma Integral_def2:
   284   "Integral = (%(a,b) f k. \<forall>e>0. (\<exists>\<delta>. gauge {a..b} \<delta> &
   285                                (\<forall>D. fine \<delta> (a,b) D -->
   286                                          \<bar>rsum D f - k\<bar> \<le> e)))"
   287 unfolding Integral_def
   288 apply (safe intro!: ext)
   289 apply (fast intro: less_imp_le)
   290 apply (drule_tac x="e/2" in spec)
   291 apply force
   292 done
   293 
   294 text{*The integral is unique if it exists*}
   295 
   296 lemma Integral_unique:
   297   assumes le: "a \<le> b"
   298   assumes 1: "Integral (a, b) f k1"
   299   assumes 2: "Integral (a, b) f k2"
   300   shows "k1 = k2"
   301 proof (rule ccontr)
   302   assume "k1 \<noteq> k2"
   303   hence e: "0 < \<bar>k1 - k2\<bar> / 2" by simp
   304   obtain d1 where "gauge {a..b} d1" and
   305     d1: "\<forall>D. fine d1 (a, b) D \<longrightarrow> \<bar>rsum D f - k1\<bar> < \<bar>k1 - k2\<bar> / 2"
   306     using 1 e by (rule IntegralE)
   307   obtain d2 where "gauge {a..b} d2" and
   308     d2: "\<forall>D. fine d2 (a, b) D \<longrightarrow> \<bar>rsum D f - k2\<bar> < \<bar>k1 - k2\<bar> / 2"
   309     using 2 e by (rule IntegralE)
   310   have "gauge {a..b} (\<lambda>x. min (d1 x) (d2 x))"
   311     using `gauge {a..b} d1` and `gauge {a..b} d2`
   312     by (rule gauge_min)
   313   then obtain D where "fine (\<lambda>x. min (d1 x) (d2 x)) (a, b) D"
   314     using fine_exists [OF le] by fast
   315   hence "fine d1 (a, b) D" and "fine d2 (a, b) D"
   316     by (auto dest: fine_min)
   317   hence "\<bar>rsum D f - k1\<bar> < \<bar>k1 - k2\<bar> / 2" and "\<bar>rsum D f - k2\<bar> < \<bar>k1 - k2\<bar> / 2"
   318     using d1 d2 by simp_all
   319   hence "\<bar>rsum D f - k1\<bar> + \<bar>rsum D f - k2\<bar> < \<bar>k1 - k2\<bar> / 2 + \<bar>k1 - k2\<bar> / 2"
   320     by (rule add_strict_mono)
   321   thus False by auto
   322 qed
   323 
   324 lemma Integral_zero: "Integral(a,a) f 0"
   325 apply (rule IntegralI)
   326 apply (rule_tac x = "\<lambda>x. 1" in exI)
   327 apply (simp add: fine_same_iff gauge_def)
   328 done
   329 
   330 lemma Integral_same_iff [simp]: "Integral (a, a) f k \<longleftrightarrow> k = 0"
   331   by (auto intro: Integral_zero Integral_unique)
   332 
   333 lemma Integral_zero_fun: "Integral (a,b) (\<lambda>x. 0) 0"
   334 apply (rule IntegralI)
   335 apply (rule_tac x="\<lambda>x. 1" in exI, simp add: gauge_def)
   336 done
   337 
   338 lemma fine_rsum_const: "fine \<delta> (a,b) D \<Longrightarrow> rsum D (\<lambda>x. c) = (c * (b - a))"
   339 unfolding rsum_def
   340 by (induct set: fine, auto simp add: algebra_simps)
   341 
   342 lemma Integral_mult_const: "a \<le> b \<Longrightarrow> Integral(a,b) (\<lambda>x. c) (c * (b - a))"
   343 apply (cases "a = b", simp)
   344 apply (rule IntegralI)
   345 apply (rule_tac x = "\<lambda>x. b - a" in exI)
   346 apply (rule conjI, simp add: gauge_def)
   347 apply (clarify)
   348 apply (subst fine_rsum_const, assumption, simp)
   349 done
   350 
   351 lemma Integral_eq_diff_bounds: "a \<le> b \<Longrightarrow> Integral(a,b) (\<lambda>x. 1) (b - a)"
   352   using Integral_mult_const [of a b 1] by simp
   353 
   354 lemma Integral_mult:
   355      "[| a \<le> b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)"
   356 apply (auto simp add: order_le_less)
   357 apply (cases "c = 0", simp add: Integral_zero_fun)
   358 apply (rule IntegralI)
   359 apply (erule_tac e="e / \<bar>c\<bar>" in IntegralE, simp add: divide_pos_pos)
   360 apply (rule_tac x="\<delta>" in exI, clarify)
   361 apply (drule_tac x="D" in spec, clarify)
   362 apply (simp add: pos_less_divide_eq abs_mult [symmetric]
   363                  algebra_simps rsum_right_distrib)
   364 done
   365 
   366 lemma Integral_add:
   367   assumes "Integral (a, b) f x1"
   368   assumes "Integral (b, c) f x2"
   369   assumes "a \<le> b" and "b \<le> c"
   370   shows "Integral (a, c) f (x1 + x2)"
   371 proof (cases "a < b \<and> b < c", rule IntegralI)
   372   fix \<epsilon> :: real assume "0 < \<epsilon>"
   373   hence "0 < \<epsilon> / 2" by auto
   374 
   375   assume "a < b \<and> b < c"
   376   hence "a < b" and "b < c" by auto
   377 
   378   obtain \<delta>1 where \<delta>1_gauge: "gauge {a..b} \<delta>1"
   379     and I1: "\<And> D. fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f - x1 \<bar> < (\<epsilon> / 2)"
   380     using IntegralE [OF `Integral (a, b) f x1` `0 < \<epsilon>/2`] by auto
   381 
   382   obtain \<delta>2 where \<delta>2_gauge: "gauge {b..c} \<delta>2"
   383     and I2: "\<And> D. fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)"
   384     using IntegralE [OF `Integral (b, c) f x2` `0 < \<epsilon>/2`] by auto
   385 
   386   def \<delta> \<equiv> "\<lambda> x. if x < b then min (\<delta>1 x) (b - x)
   387            else if x = b then min (\<delta>1 b) (\<delta>2 b)
   388                          else min (\<delta>2 x) (x - b)"
   389 
   390   have "gauge {a..c} \<delta>"
   391     using \<delta>1_gauge \<delta>2_gauge unfolding \<delta>_def gauge_def by auto
   392 
   393   moreover {
   394     fix D :: "(real \<times> real \<times> real) list"
   395     assume fine: "fine \<delta> (a,c) D"
   396     from fine_covers_all[OF this `a < b` `b \<le> c`]
   397     obtain N where "N < length D"
   398       and *: "\<forall> d t e. D ! N = (d, t, e) \<longrightarrow> d < b \<and> b \<le> e"
   399       by auto
   400     obtain d t e where D_eq: "D ! N = (d, t, e)" by (cases "D!N", auto)
   401     with * have "d < b" and "b \<le> e" by auto
   402     have in_D: "(d, t, e) \<in> set D"
   403       using D_eq[symmetric] using `N < length D` by auto
   404 
   405     from mem_fine[OF fine in_D]
   406     have "d < e" and "d \<le> t" and "t \<le> e" by auto
   407 
   408     have "t = b"
   409     proof (rule ccontr)
   410       assume "t \<noteq> b"
   411       with mem_fine3[OF fine in_D] `b \<le> e` `d \<le> t` `t \<le> e` `d < b` \<delta>_def
   412       show False by (cases "t < b") auto
   413     qed
   414 
   415     let ?D1 = "take N D"
   416     let ?D2 = "drop N D"
   417     def D1 \<equiv> "take N D @ [(d, t, b)]"
   418     def D2 \<equiv> "(if b = e then [] else [(b, t, e)]) @ drop (Suc N) D"
   419 
   420     have "D \<noteq> []" using `N < length D` by auto
   421     from hd_drop_conv_nth[OF this `N < length D`]
   422     have "fst (hd ?D2) = d" using `D ! N = (d, t, e)` by auto
   423     with fine_append_split[OF _ _ append_take_drop_id[symmetric]]
   424     have fine1: "fine \<delta> (a,d) ?D1" and fine2: "fine \<delta> (d,c) ?D2"
   425       using `N < length D` fine by auto
   426 
   427     have "fine \<delta>1 (a,b) D1" unfolding D1_def
   428     proof (rule fine_append)
   429       show "fine \<delta>1 (a, d) ?D1"
   430       proof (rule fine1[THEN fine_\<delta>_expand])
   431         fix x assume "a \<le> x" "x \<le> d"
   432         hence "x \<le> b" using `d < b` `x \<le> d` by auto
   433         thus "\<delta> x \<le> \<delta>1 x" unfolding \<delta>_def by auto
   434       qed
   435 
   436       have "b - d < \<delta>1 t"
   437         using mem_fine3[OF fine in_D] \<delta>_def `b \<le> e` `t = b` by auto
   438       from `d < b` `d \<le> t` `t = b` this
   439       show "fine \<delta>1 (d, b) [(d, t, b)]" using fine_single by auto
   440     qed
   441     note rsum1 = I1[OF this]
   442 
   443     have drop_split: "drop N D = [D ! N] @ drop (Suc N) D"
   444       using nth_drop'[OF `N < length D`] by simp
   445 
   446     have fine2: "fine \<delta>2 (e,c) (drop (Suc N) D)"
   447     proof (cases "drop (Suc N) D = []")
   448       case True
   449       note * = fine2[simplified drop_split True D_eq append_Nil2]
   450       have "e = c" using fine_single_boundaries[OF * refl] by auto
   451       thus ?thesis unfolding True using fine_Nil by auto
   452     next
   453       case False
   454       note * = fine_append_split[OF fine2 False drop_split]
   455       from fine_single_boundaries[OF *(1)]
   456       have "fst (hd (drop (Suc N) D)) = e" using D_eq by auto
   457       with *(2) have "fine \<delta> (e,c) (drop (Suc N) D)" by auto
   458       thus ?thesis
   459       proof (rule fine_\<delta>_expand)
   460         fix x assume "e \<le> x" and "x \<le> c"
   461         thus "\<delta> x \<le> \<delta>2 x" using `b \<le> e` unfolding \<delta>_def by auto
   462       qed
   463     qed
   464 
   465     have "fine \<delta>2 (b, c) D2"
   466     proof (cases "e = b")
   467       case True thus ?thesis using fine2 by (simp add: D1_def D2_def)
   468     next
   469       case False
   470       have "e - b < \<delta>2 b"
   471         using mem_fine3[OF fine in_D] \<delta>_def `d < b` `t = b` by auto
   472       with False `t = b` `b \<le> e`
   473       show ?thesis using D2_def
   474         by (auto intro!: fine_append[OF _ fine2] fine_single
   475                simp del: append_Cons)
   476     qed
   477     note rsum2 = I2[OF this]
   478 
   479     have "rsum D f = rsum (take N D) f + rsum [D ! N] f + rsum (drop (Suc N) D) f"
   480       using rsum_append[symmetric] nth_drop'[OF `N < length D`] by auto
   481     also have "\<dots> = rsum D1 f + rsum D2 f"
   482       by (cases "b = e", auto simp add: D1_def D2_def D_eq rsum_append algebra_simps)
   483     finally have "\<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>"
   484       using add_strict_mono[OF rsum1 rsum2] by simp
   485   }
   486   ultimately show "\<exists> \<delta>. gauge {a .. c} \<delta> \<and>
   487     (\<forall>D. fine \<delta> (a,c) D \<longrightarrow> \<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>)"
   488     by blast
   489 next
   490   case False
   491   hence "a = b \<or> b = c" using `a \<le> b` and `b \<le> c` by auto
   492   thus ?thesis
   493   proof (rule disjE)
   494     assume "a = b" hence "x1 = 0"
   495       using `Integral (a, b) f x1` by simp
   496     thus ?thesis using `a = b` `Integral (b, c) f x2` by simp
   497   next
   498     assume "b = c" hence "x2 = 0"
   499       using `Integral (b, c) f x2` by simp
   500     thus ?thesis using `b = c` `Integral (a, b) f x1` by simp
   501   qed
   502 qed
   503 
   504 text{*Fundamental theorem of calculus (Part I)*}
   505 
   506 text{*"Straddle Lemma" : Swartz and Thompson: AMM 95(7) 1988 *}
   507 
   508 lemma strad1:
   509        "\<lbrakk>\<forall>z::real. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow>
   510              \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2;
   511         0 < s; 0 < e; a \<le> x; x \<le> b\<rbrakk>
   512        \<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>"
   513 apply clarify
   514 apply (case_tac "z = x", simp)
   515 apply (drule_tac x = z in spec)
   516 apply (rule_tac z1 = "\<bar>inverse (z - x)\<bar>" 
   517        in real_mult_le_cancel_iff2 [THEN iffD1])
   518  apply simp
   519 apply (simp del: abs_inverse add: abs_mult [symmetric]
   520           mult_assoc [symmetric])
   521 apply (subgoal_tac "inverse (z - x) * (f z - f x - f' x * (z - x)) 
   522                     = (f z - f x) / (z - x) - f' x")
   523  apply (simp add: abs_mult [symmetric] mult_ac diff_minus)
   524 apply (subst mult_commute)
   525 apply (simp add: left_distrib diff_minus)
   526 apply (simp add: mult_assoc divide_inverse)
   527 apply (simp add: left_distrib)
   528 done
   529 
   530 lemma lemma_straddle:
   531   assumes f': "\<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x)" and "0 < e"
   532   shows "\<exists>g. gauge {a..b} g &
   533                 (\<forall>x u v. a \<le> u & u \<le> x & x \<le> v & v \<le> b & (v - u) < g(x)
   534                   --> \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))"
   535 proof -
   536   have "\<forall>x\<in>{a..b}.
   537         (\<exists>d > 0. \<forall>u v. u \<le> x & x \<le> v & (v - u) < d --> 
   538                        \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))"
   539   proof (clarsimp)
   540     fix x :: real assume "a \<le> x" and "x \<le> b"
   541     with f' have "DERIV f x :> f'(x)" by simp
   542     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"
   543       by (simp add: DERIV_iff2 LIM_eq)
   544     with `0 < e` obtain s
   545     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"
   546       by (drule_tac x="e/2" in spec, auto)
   547     then have strad [rule_format]:
   548         "\<forall>z. \<bar>z - x\<bar> < s --> \<bar>f z - f x - f' x * (z - x)\<bar> \<le> e/2 * \<bar>z - x\<bar>"
   549       using `0 < e` `a \<le> x` `x \<le> b` by (rule strad1)
   550     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)"
   551     proof (safe intro!: exI)
   552       show "0 < s" by fact
   553     next
   554       fix u v :: real assume "u \<le> x" and "x \<le> v" and "v - u < s"
   555       have "\<bar>f v - f u - f' x * (v - u)\<bar> =
   556             \<bar>(f v - f x - f' x * (v - x)) + (f x - f u - f' x * (x - u))\<bar>"
   557         by (simp add: right_diff_distrib)
   558       also have "\<dots> \<le> \<bar>f v - f x - f' x * (v - x)\<bar> + \<bar>f x - f u - f' x * (x - u)\<bar>"
   559         by (rule abs_triangle_ineq)
   560       also have "\<dots> = \<bar>f v - f x - f' x * (v - x)\<bar> + \<bar>f u - f x - f' x * (u - x)\<bar>"
   561         by (simp add: right_diff_distrib)
   562       also have "\<dots> \<le> (e/2) * \<bar>v - x\<bar> + (e/2) * \<bar>u - x\<bar>"
   563         using `u \<le> x` `x \<le> v` `v - u < s` by (intro add_mono strad, simp_all)
   564       also have "\<dots> \<le> e * (v - u) / 2 + e * (v - u) / 2"
   565         using `u \<le> x` `x \<le> v` `0 < e` by (intro add_mono, simp_all)
   566       also have "\<dots> = e * (v - u)"
   567         by simp
   568       finally show "\<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u)" .
   569     qed
   570   qed
   571   thus ?thesis
   572     by (simp add: gauge_def) (drule bchoice, auto)
   573 qed
   574 
   575 lemma fundamental_theorem_of_calculus:
   576   assumes "a \<le> b"
   577   assumes f': "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> DERIV f x :> f'(x)"
   578   shows "Integral (a, b) f' (f(b) - f(a))"
   579 proof (cases "a = b")
   580   assume "a = b" thus ?thesis by simp
   581 next
   582   assume "a \<noteq> b" with `a \<le> b` have "a < b" by simp
   583   show ?thesis
   584   proof (simp add: Integral_def2, clarify)
   585     fix e :: real assume "0 < e"
   586     with `a < b` have "0 < e / (b - a)" by (simp add: divide_pos_pos)
   587 
   588     from lemma_straddle [OF f' this]
   589     obtain \<delta> where "gauge {a..b} \<delta>"
   590       and \<delta>: "\<And>x u v. \<lbrakk>a \<le> u; u \<le> x; x \<le> v; v \<le> b; v - u < \<delta> x\<rbrakk> \<Longrightarrow>
   591            \<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u) / (b - a)" by auto
   592 
   593     have "\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f' - (f b - f a)\<bar> \<le> e"
   594     proof (clarify)
   595       fix D assume D: "fine \<delta> (a, b) D"
   596       hence "(\<Sum>(u, x, v)\<leftarrow>D. f v - f u) = f b - f a"
   597         by (rule fine_listsum_eq_diff)
   598       hence "\<bar>rsum D f' - (f b - f a)\<bar> = \<bar>rsum D f' - (\<Sum>(u, x, v)\<leftarrow>D. f v - f u)\<bar>"
   599         by simp
   600       also have "\<dots> = \<bar>(\<Sum>(u, x, v)\<leftarrow>D. f v - f u) - rsum D f'\<bar>"
   601         by (rule abs_minus_commute)
   602       also have "\<dots> = \<bar>\<Sum>(u, x, v)\<leftarrow>D. (f v - f u) - f' x * (v - u)\<bar>"
   603         by (simp only: rsum_def listsum_subtractf split_def)
   604       also have "\<dots> \<le> (\<Sum>(u, x, v)\<leftarrow>D. \<bar>(f v - f u) - f' x * (v - u)\<bar>)"
   605         by (rule ord_le_eq_trans [OF listsum_abs], simp add: o_def split_def)
   606       also have "\<dots> \<le> (\<Sum>(u, x, v)\<leftarrow>D. (e / (b - a)) * (v - u))"
   607         apply (rule listsum_mono, clarify, rename_tac u x v)
   608         using D apply (simp add: \<delta> mem_fine mem_fine2 mem_fine3)
   609         done
   610       also have "\<dots> = e"
   611         using fine_listsum_eq_diff [OF D, where f="\<lambda>x. x"]
   612         unfolding split_def listsum_const_mult
   613         using `a < b` by simp
   614       finally show "\<bar>rsum D f' - (f b - f a)\<bar> \<le> e" .
   615     qed
   616 
   617     with `gauge {a..b} \<delta>`
   618     show "\<exists>\<delta>. gauge {a..b} \<delta> \<and> (\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f' - (f b - f a)\<bar> \<le> e)"
   619       by auto
   620   qed
   621 qed
   622 
   623 end