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