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