1.1 --- a/src/HOL/Integration.thy Mon Feb 22 20:08:10 2010 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,658 +0,0 @@
1.4 -(* Author: Jacques D. Fleuriot, University of Edinburgh
1.5 - Conversion to Isar and new proofs by Lawrence C Paulson, 2004
1.6 -*)
1.7 -
1.8 -header{*Theory of Integration*}
1.9 -
1.10 -theory Integration
1.11 -imports Deriv ATP_Linkup
1.12 -begin
1.13 -
1.14 -text{*We follow John Harrison in formalizing the Gauge integral.*}
1.15 -
1.16 -subsection {* Gauges *}
1.17 -
1.18 -definition
1.19 - gauge :: "[real set, real => real] => bool" where
1.20 - [code del]:"gauge E g = (\<forall>x\<in>E. 0 < g(x))"
1.21 -
1.22 -
1.23 -subsection {* Gauge-fine divisions *}
1.24 -
1.25 -inductive
1.26 - fine :: "[real \<Rightarrow> real, real \<times> real, (real \<times> real \<times> real) list] \<Rightarrow> bool"
1.27 -for
1.28 - \<delta> :: "real \<Rightarrow> real"
1.29 -where
1.30 - fine_Nil:
1.31 - "fine \<delta> (a, a) []"
1.32 -| fine_Cons:
1.33 - "\<lbrakk>fine \<delta> (b, c) D; a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk>
1.34 - \<Longrightarrow> fine \<delta> (a, c) ((a, x, b) # D)"
1.35 -
1.36 -lemmas fine_induct [induct set: fine] =
1.37 - fine.induct [of "\<delta>" "(a,b)" "D" "split P", unfolded split_conv, standard]
1.38 -
1.39 -lemma fine_single:
1.40 - "\<lbrakk>a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk> \<Longrightarrow> fine \<delta> (a, b) [(a, x, b)]"
1.41 -by (rule fine_Cons [OF fine_Nil])
1.42 -
1.43 -lemma fine_append:
1.44 - "\<lbrakk>fine \<delta> (a, b) D; fine \<delta> (b, c) D'\<rbrakk> \<Longrightarrow> fine \<delta> (a, c) (D @ D')"
1.45 -by (induct set: fine, simp, simp add: fine_Cons)
1.46 -
1.47 -lemma fine_imp_le: "fine \<delta> (a, b) D \<Longrightarrow> a \<le> b"
1.48 -by (induct set: fine, simp_all)
1.49 -
1.50 -lemma nonempty_fine_imp_less: "\<lbrakk>fine \<delta> (a, b) D; D \<noteq> []\<rbrakk> \<Longrightarrow> a < b"
1.51 -apply (induct set: fine, simp)
1.52 -apply (drule fine_imp_le, simp)
1.53 -done
1.54 -
1.55 -lemma empty_fine_imp_eq: "\<lbrakk>fine \<delta> (a, b) D; D = []\<rbrakk> \<Longrightarrow> a = b"
1.56 -by (induct set: fine, simp_all)
1.57 -
1.58 -lemma fine_eq: "fine \<delta> (a, b) D \<Longrightarrow> a = b \<longleftrightarrow> D = []"
1.59 -apply (cases "D = []")
1.60 -apply (drule (1) empty_fine_imp_eq, simp)
1.61 -apply (drule (1) nonempty_fine_imp_less, simp)
1.62 -done
1.63 -
1.64 -lemma mem_fine:
1.65 - "\<lbrakk>fine \<delta> (a, b) D; (u, x, v) \<in> set D\<rbrakk> \<Longrightarrow> u < v \<and> u \<le> x \<and> x \<le> v"
1.66 -by (induct set: fine, simp, force)
1.67 -
1.68 -lemma mem_fine2: "\<lbrakk>fine \<delta> (a, b) D; (u, z, v) \<in> set D\<rbrakk> \<Longrightarrow> a \<le> u \<and> v \<le> b"
1.69 -apply (induct arbitrary: z u v set: fine, auto)
1.70 -apply (simp add: fine_imp_le)
1.71 -apply (erule order_trans [OF less_imp_le], simp)
1.72 -done
1.73 -
1.74 -lemma mem_fine3: "\<lbrakk>fine \<delta> (a, b) D; (u, z, v) \<in> set D\<rbrakk> \<Longrightarrow> v - u < \<delta> z"
1.75 -by (induct arbitrary: z u v set: fine) auto
1.76 -
1.77 -lemma BOLZANO:
1.78 - fixes P :: "real \<Rightarrow> real \<Rightarrow> bool"
1.79 - assumes 1: "a \<le> b"
1.80 - assumes 2: "\<And>a b c. \<lbrakk>P a b; P b c; a \<le> b; b \<le> c\<rbrakk> \<Longrightarrow> P a c"
1.81 - assumes 3: "\<And>x. \<exists>d>0. \<forall>a b. a \<le> x & x \<le> b & (b-a) < d \<longrightarrow> P a b"
1.82 - shows "P a b"
1.83 -apply (subgoal_tac "split P (a,b)", simp)
1.84 -apply (rule lemma_BOLZANO [OF _ _ 1])
1.85 -apply (clarify, erule (3) 2)
1.86 -apply (clarify, rule 3)
1.87 -done
1.88 -
1.89 -text{*We can always find a division that is fine wrt any gauge*}
1.90 -
1.91 -lemma fine_exists:
1.92 - assumes "a \<le> b" and "gauge {a..b} \<delta>" shows "\<exists>D. fine \<delta> (a, b) D"
1.93 -proof -
1.94 - {
1.95 - fix u v :: real assume "u \<le> v"
1.96 - have "a \<le> u \<Longrightarrow> v \<le> b \<Longrightarrow> \<exists>D. fine \<delta> (u, v) D"
1.97 - apply (induct u v rule: BOLZANO, rule `u \<le> v`)
1.98 - apply (simp, fast intro: fine_append)
1.99 - apply (case_tac "a \<le> x \<and> x \<le> b")
1.100 - apply (rule_tac x="\<delta> x" in exI)
1.101 - apply (rule conjI)
1.102 - apply (simp add: `gauge {a..b} \<delta>` [unfolded gauge_def])
1.103 - apply (clarify, rename_tac u v)
1.104 - apply (case_tac "u = v")
1.105 - apply (fast intro: fine_Nil)
1.106 - apply (subgoal_tac "u < v", fast intro: fine_single, simp)
1.107 - apply (rule_tac x="1" in exI, clarsimp)
1.108 - done
1.109 - }
1.110 - with `a \<le> b` show ?thesis by auto
1.111 -qed
1.112 -
1.113 -lemma fine_covers_all:
1.114 - assumes "fine \<delta> (a, c) D" and "a < x" and "x \<le> c"
1.115 - shows "\<exists> N < length D. \<forall> d t e. D ! N = (d,t,e) \<longrightarrow> d < x \<and> x \<le> e"
1.116 - using assms
1.117 -proof (induct set: fine)
1.118 - case (2 b c D a t)
1.119 - thus ?case
1.120 - proof (cases "b < x")
1.121 - case True
1.122 - with 2 obtain N where *: "N < length D"
1.123 - and **: "\<And> d t e. D ! N = (d,t,e) \<Longrightarrow> d < x \<and> x \<le> e" by auto
1.124 - hence "Suc N < length ((a,t,b)#D) \<and>
1.125 - (\<forall> d t' e. ((a,t,b)#D) ! Suc N = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
1.126 - thus ?thesis by auto
1.127 - next
1.128 - case False with 2
1.129 - have "0 < length ((a,t,b)#D) \<and>
1.130 - (\<forall> d t' e. ((a,t,b)#D) ! 0 = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
1.131 - thus ?thesis by auto
1.132 - qed
1.133 -qed auto
1.134 -
1.135 -lemma fine_append_split:
1.136 - assumes "fine \<delta> (a,b) D" and "D2 \<noteq> []" and "D = D1 @ D2"
1.137 - shows "fine \<delta> (a,fst (hd D2)) D1" (is "?fine1")
1.138 - and "fine \<delta> (fst (hd D2), b) D2" (is "?fine2")
1.139 -proof -
1.140 - from assms
1.141 - have "?fine1 \<and> ?fine2"
1.142 - proof (induct arbitrary: D1 D2)
1.143 - case (2 b c D a' x D1 D2)
1.144 - note induct = this
1.145 -
1.146 - thus ?case
1.147 - proof (cases D1)
1.148 - case Nil
1.149 - hence "fst (hd D2) = a'" using 2 by auto
1.150 - with fine_Cons[OF `fine \<delta> (b,c) D` induct(3,4,5)] Nil induct
1.151 - show ?thesis by (auto intro: fine_Nil)
1.152 - next
1.153 - case (Cons d1 D1')
1.154 - with induct(2)[OF `D2 \<noteq> []`, of D1'] induct(8)
1.155 - have "fine \<delta> (b, fst (hd D2)) D1'" and "fine \<delta> (fst (hd D2), c) D2" and
1.156 - "d1 = (a', x, b)" by auto
1.157 - with fine_Cons[OF this(1) induct(3,4,5), OF induct(6)] Cons
1.158 - show ?thesis by auto
1.159 - qed
1.160 - qed auto
1.161 - thus ?fine1 and ?fine2 by auto
1.162 -qed
1.163 -
1.164 -lemma fine_\<delta>_expand:
1.165 - assumes "fine \<delta> (a,b) D"
1.166 - and "\<And> x. \<lbrakk> a \<le> x ; x \<le> b \<rbrakk> \<Longrightarrow> \<delta> x \<le> \<delta>' x"
1.167 - shows "fine \<delta>' (a,b) D"
1.168 -using assms proof induct
1.169 - case 1 show ?case by (rule fine_Nil)
1.170 -next
1.171 - case (2 b c D a x)
1.172 - show ?case
1.173 - proof (rule fine_Cons)
1.174 - show "fine \<delta>' (b,c) D" using 2 by auto
1.175 - from fine_imp_le[OF 2(1)] 2(6) `x \<le> b`
1.176 - show "b - a < \<delta>' x"
1.177 - using 2(7)[OF `a \<le> x`] by auto
1.178 - qed (auto simp add: 2)
1.179 -qed
1.180 -
1.181 -lemma fine_single_boundaries:
1.182 - assumes "fine \<delta> (a,b) D" and "D = [(d, t, e)]"
1.183 - shows "a = d \<and> b = e"
1.184 -using assms proof induct
1.185 - case (2 b c D a x)
1.186 - hence "D = []" and "a = d" and "b = e" by auto
1.187 - moreover
1.188 - from `fine \<delta> (b,c) D` `D = []` have "b = c"
1.189 - by (rule empty_fine_imp_eq)
1.190 - ultimately show ?case by simp
1.191 -qed auto
1.192 -
1.193 -
1.194 -subsection {* Riemann sum *}
1.195 -
1.196 -definition
1.197 - rsum :: "[(real \<times> real \<times> real) list, real \<Rightarrow> real] \<Rightarrow> real" where
1.198 - "rsum D f = (\<Sum>(u, x, v)\<leftarrow>D. f x * (v - u))"
1.199 -
1.200 -lemma rsum_Nil [simp]: "rsum [] f = 0"
1.201 -unfolding rsum_def by simp
1.202 -
1.203 -lemma rsum_Cons [simp]: "rsum ((u, x, v) # D) f = f x * (v - u) + rsum D f"
1.204 -unfolding rsum_def by simp
1.205 -
1.206 -lemma rsum_zero [simp]: "rsum D (\<lambda>x. 0) = 0"
1.207 -by (induct D, auto)
1.208 -
1.209 -lemma rsum_left_distrib: "rsum D f * c = rsum D (\<lambda>x. f x * c)"
1.210 -by (induct D, auto simp add: algebra_simps)
1.211 -
1.212 -lemma rsum_right_distrib: "c * rsum D f = rsum D (\<lambda>x. c * f x)"
1.213 -by (induct D, auto simp add: algebra_simps)
1.214 -
1.215 -lemma rsum_add: "rsum D (\<lambda>x. f x + g x) = rsum D f + rsum D g"
1.216 -by (induct D, auto simp add: algebra_simps)
1.217 -
1.218 -lemma rsum_append: "rsum (D1 @ D2) f = rsum D1 f + rsum D2 f"
1.219 -unfolding rsum_def map_append listsum_append ..
1.220 -
1.221 -
1.222 -subsection {* Gauge integrability (definite) *}
1.223 -
1.224 -definition
1.225 - Integral :: "[(real*real),real=>real,real] => bool" where
1.226 - [code del]: "Integral = (%(a,b) f k. \<forall>e > 0.
1.227 - (\<exists>\<delta>. gauge {a .. b} \<delta> &
1.228 - (\<forall>D. fine \<delta> (a,b) D -->
1.229 - \<bar>rsum D f - k\<bar> < e)))"
1.230 -
1.231 -lemma Integral_def2:
1.232 - "Integral = (%(a,b) f k. \<forall>e>0. (\<exists>\<delta>. gauge {a..b} \<delta> &
1.233 - (\<forall>D. fine \<delta> (a,b) D -->
1.234 - \<bar>rsum D f - k\<bar> \<le> e)))"
1.235 -unfolding Integral_def
1.236 -apply (safe intro!: ext)
1.237 -apply (fast intro: less_imp_le)
1.238 -apply (drule_tac x="e/2" in spec)
1.239 -apply force
1.240 -done
1.241 -
1.242 -text{*Lemmas about combining gauges*}
1.243 -
1.244 -lemma gauge_min:
1.245 - "[| gauge(E) g1; gauge(E) g2 |]
1.246 - ==> gauge(E) (%x. min (g1(x)) (g2(x)))"
1.247 -by (simp add: gauge_def)
1.248 -
1.249 -lemma fine_min:
1.250 - "fine (%x. min (g1(x)) (g2(x))) (a,b) D
1.251 - ==> fine(g1) (a,b) D & fine(g2) (a,b) D"
1.252 -apply (erule fine.induct)
1.253 -apply (simp add: fine_Nil)
1.254 -apply (simp add: fine_Cons)
1.255 -done
1.256 -
1.257 -text{*The integral is unique if it exists*}
1.258 -
1.259 -lemma Integral_unique:
1.260 - "[| a \<le> b; Integral(a,b) f k1; Integral(a,b) f k2 |] ==> k1 = k2"
1.261 -apply (simp add: Integral_def)
1.262 -apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec)+
1.263 -apply auto
1.264 -apply (drule gauge_min, assumption)
1.265 -apply (drule_tac \<delta> = "%x. min (\<delta> x) (\<delta>' x)"
1.266 - in fine_exists, assumption, auto)
1.267 -apply (drule fine_min)
1.268 -apply (drule spec)+
1.269 -apply auto
1.270 -apply (subgoal_tac "\<bar>(rsum D f - k2) - (rsum D f - k1)\<bar> < \<bar>k1 - k2\<bar>")
1.271 -apply arith
1.272 -apply (drule add_strict_mono, assumption)
1.273 -apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
1.274 - mult_less_cancel_right)
1.275 -done
1.276 -
1.277 -lemma Integral_zero [simp]: "Integral(a,a) f 0"
1.278 -apply (auto simp add: Integral_def)
1.279 -apply (rule_tac x = "%x. 1" in exI)
1.280 -apply (auto dest: fine_eq simp add: gauge_def rsum_def)
1.281 -done
1.282 -
1.283 -lemma fine_rsum_const: "fine \<delta> (a,b) D \<Longrightarrow> rsum D (\<lambda>x. c) = (c * (b - a))"
1.284 -unfolding rsum_def
1.285 -by (induct set: fine, auto simp add: algebra_simps)
1.286 -
1.287 -lemma Integral_eq_diff_bounds: "a \<le> b ==> Integral(a,b) (%x. 1) (b - a)"
1.288 -apply (cases "a = b", simp)
1.289 -apply (simp add: Integral_def, clarify)
1.290 -apply (rule_tac x = "%x. b - a" in exI)
1.291 -apply (rule conjI, simp add: gauge_def)
1.292 -apply (clarify)
1.293 -apply (subst fine_rsum_const, assumption, simp)
1.294 -done
1.295 -
1.296 -lemma Integral_mult_const: "a \<le> b ==> Integral(a,b) (%x. c) (c*(b - a))"
1.297 -apply (cases "a = b", simp)
1.298 -apply (simp add: Integral_def, clarify)
1.299 -apply (rule_tac x = "%x. b - a" in exI)
1.300 -apply (rule conjI, simp add: gauge_def)
1.301 -apply (clarify)
1.302 -apply (subst fine_rsum_const, assumption, simp)
1.303 -done
1.304 -
1.305 -lemma Integral_mult:
1.306 - "[| a \<le> b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)"
1.307 -apply (auto simp add: order_le_less
1.308 - dest: Integral_unique [OF order_refl Integral_zero])
1.309 -apply (auto simp add: Integral_def setsum_right_distrib[symmetric] mult_assoc)
1.310 -apply (case_tac "c = 0", force)
1.311 -apply (drule_tac x = "e/abs c" in spec)
1.312 -apply (simp add: divide_pos_pos)
1.313 -apply clarify
1.314 -apply (rule_tac x="\<delta>" in exI, clarify)
1.315 -apply (drule_tac x="D" in spec, clarify)
1.316 -apply (simp add: pos_less_divide_eq abs_mult [symmetric]
1.317 - algebra_simps rsum_right_distrib)
1.318 -done
1.319 -
1.320 -lemma Integral_add:
1.321 - assumes "Integral (a, b) f x1"
1.322 - assumes "Integral (b, c) f x2"
1.323 - assumes "a \<le> b" and "b \<le> c"
1.324 - shows "Integral (a, c) f (x1 + x2)"
1.325 -proof (cases "a < b \<and> b < c", simp only: Integral_def split_conv, rule allI, rule impI)
1.326 - fix \<epsilon> :: real assume "0 < \<epsilon>"
1.327 - hence "0 < \<epsilon> / 2" by auto
1.328 -
1.329 - assume "a < b \<and> b < c"
1.330 - hence "a < b" and "b < c" by auto
1.331 -
1.332 - from `Integral (a, b) f x1`[simplified Integral_def split_conv,
1.333 - rule_format, OF `0 < \<epsilon>/2`]
1.334 - obtain \<delta>1 where \<delta>1_gauge: "gauge {a..b} \<delta>1"
1.335 - and I1: "\<And> D. fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f - x1 \<bar> < (\<epsilon> / 2)" by auto
1.336 -
1.337 - from `Integral (b, c) f x2`[simplified Integral_def split_conv,
1.338 - rule_format, OF `0 < \<epsilon>/2`]
1.339 - obtain \<delta>2 where \<delta>2_gauge: "gauge {b..c} \<delta>2"
1.340 - and I2: "\<And> D. fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)" by auto
1.341 -
1.342 - def \<delta> \<equiv> "\<lambda> x. if x < b then min (\<delta>1 x) (b - x)
1.343 - else if x = b then min (\<delta>1 b) (\<delta>2 b)
1.344 - else min (\<delta>2 x) (x - b)"
1.345 -
1.346 - have "gauge {a..c} \<delta>"
1.347 - using \<delta>1_gauge \<delta>2_gauge unfolding \<delta>_def gauge_def by auto
1.348 - moreover {
1.349 - fix D :: "(real \<times> real \<times> real) list"
1.350 - assume fine: "fine \<delta> (a,c) D"
1.351 - from fine_covers_all[OF this `a < b` `b \<le> c`]
1.352 - obtain N where "N < length D"
1.353 - and *: "\<forall> d t e. D ! N = (d, t, e) \<longrightarrow> d < b \<and> b \<le> e"
1.354 - by auto
1.355 - obtain d t e where D_eq: "D ! N = (d, t, e)" by (cases "D!N", auto)
1.356 - with * have "d < b" and "b \<le> e" by auto
1.357 - have in_D: "(d, t, e) \<in> set D"
1.358 - using D_eq[symmetric] using `N < length D` by auto
1.359 -
1.360 - from mem_fine[OF fine in_D]
1.361 - have "d < e" and "d \<le> t" and "t \<le> e" by auto
1.362 -
1.363 - have "t = b"
1.364 - proof (rule ccontr)
1.365 - assume "t \<noteq> b"
1.366 - with mem_fine3[OF fine in_D] `b \<le> e` `d \<le> t` `t \<le> e` `d < b` \<delta>_def
1.367 - show False by (cases "t < b") auto
1.368 - qed
1.369 -
1.370 - let ?D1 = "take N D"
1.371 - let ?D2 = "drop N D"
1.372 - def D1 \<equiv> "take N D @ [(d, t, b)]"
1.373 - def D2 \<equiv> "(if b = e then [] else [(b, t, e)]) @ drop (Suc N) D"
1.374 -
1.375 - have "D \<noteq> []" using `N < length D` by auto
1.376 - from hd_drop_conv_nth[OF this `N < length D`]
1.377 - have "fst (hd ?D2) = d" using `D ! N = (d, t, e)` by auto
1.378 - with fine_append_split[OF _ _ append_take_drop_id[symmetric]]
1.379 - have fine1: "fine \<delta> (a,d) ?D1" and fine2: "fine \<delta> (d,c) ?D2"
1.380 - using `N < length D` fine by auto
1.381 -
1.382 - have "fine \<delta>1 (a,b) D1" unfolding D1_def
1.383 - proof (rule fine_append)
1.384 - show "fine \<delta>1 (a, d) ?D1"
1.385 - proof (rule fine1[THEN fine_\<delta>_expand])
1.386 - fix x assume "a \<le> x" "x \<le> d"
1.387 - hence "x \<le> b" using `d < b` `x \<le> d` by auto
1.388 - thus "\<delta> x \<le> \<delta>1 x" unfolding \<delta>_def by auto
1.389 - qed
1.390 -
1.391 - have "b - d < \<delta>1 t"
1.392 - using mem_fine3[OF fine in_D] \<delta>_def `b \<le> e` `t = b` by auto
1.393 - from `d < b` `d \<le> t` `t = b` this
1.394 - show "fine \<delta>1 (d, b) [(d, t, b)]" using fine_single by auto
1.395 - qed
1.396 - note rsum1 = I1[OF this]
1.397 -
1.398 - have drop_split: "drop N D = [D ! N] @ drop (Suc N) D"
1.399 - using nth_drop'[OF `N < length D`] by simp
1.400 -
1.401 - have fine2: "fine \<delta>2 (e,c) (drop (Suc N) D)"
1.402 - proof (cases "drop (Suc N) D = []")
1.403 - case True
1.404 - note * = fine2[simplified drop_split True D_eq append_Nil2]
1.405 - have "e = c" using fine_single_boundaries[OF * refl] by auto
1.406 - thus ?thesis unfolding True using fine_Nil by auto
1.407 - next
1.408 - case False
1.409 - note * = fine_append_split[OF fine2 False drop_split]
1.410 - from fine_single_boundaries[OF *(1)]
1.411 - have "fst (hd (drop (Suc N) D)) = e" using D_eq by auto
1.412 - with *(2) have "fine \<delta> (e,c) (drop (Suc N) D)" by auto
1.413 - thus ?thesis
1.414 - proof (rule fine_\<delta>_expand)
1.415 - fix x assume "e \<le> x" and "x \<le> c"
1.416 - thus "\<delta> x \<le> \<delta>2 x" using `b \<le> e` unfolding \<delta>_def by auto
1.417 - qed
1.418 - qed
1.419 -
1.420 - have "fine \<delta>2 (b, c) D2"
1.421 - proof (cases "e = b")
1.422 - case True thus ?thesis using fine2 by (simp add: D1_def D2_def)
1.423 - next
1.424 - case False
1.425 - have "e - b < \<delta>2 b"
1.426 - using mem_fine3[OF fine in_D] \<delta>_def `d < b` `t = b` by auto
1.427 - with False `t = b` `b \<le> e`
1.428 - show ?thesis using D2_def
1.429 - by (auto intro!: fine_append[OF _ fine2] fine_single
1.430 - simp del: append_Cons)
1.431 - qed
1.432 - note rsum2 = I2[OF this]
1.433 -
1.434 - have "rsum D f = rsum (take N D) f + rsum [D ! N] f + rsum (drop (Suc N) D) f"
1.435 - using rsum_append[symmetric] nth_drop'[OF `N < length D`] by auto
1.436 - also have "\<dots> = rsum D1 f + rsum D2 f"
1.437 - by (cases "b = e", auto simp add: D1_def D2_def D_eq rsum_append algebra_simps)
1.438 - finally have "\<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>"
1.439 - using add_strict_mono[OF rsum1 rsum2] by simp
1.440 - }
1.441 - ultimately show "\<exists> \<delta>. gauge {a .. c} \<delta> \<and>
1.442 - (\<forall>D. fine \<delta> (a,c) D \<longrightarrow> \<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>)"
1.443 - by blast
1.444 -next
1.445 - case False
1.446 - hence "a = b \<or> b = c" using `a \<le> b` and `b \<le> c` by auto
1.447 - thus ?thesis
1.448 - proof (rule disjE)
1.449 - assume "a = b" hence "x1 = 0"
1.450 - using `Integral (a, b) f x1` Integral_zero Integral_unique[of a b] by auto
1.451 - thus ?thesis using `a = b` `Integral (b, c) f x2` by auto
1.452 - next
1.453 - assume "b = c" hence "x2 = 0"
1.454 - using `Integral (b, c) f x2` Integral_zero Integral_unique[of b c] by auto
1.455 - thus ?thesis using `b = c` `Integral (a, b) f x1` by auto
1.456 - qed
1.457 -qed
1.458 -
1.459 -text{*Fundamental theorem of calculus (Part I)*}
1.460 -
1.461 -text{*"Straddle Lemma" : Swartz and Thompson: AMM 95(7) 1988 *}
1.462 -
1.463 -lemma strad1:
1.464 - "\<lbrakk>\<forall>z::real. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow>
1.465 - \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2;
1.466 - 0 < s; 0 < e; a \<le> x; x \<le> b\<rbrakk>
1.467 - \<Longrightarrow> \<forall>z. \<bar>z - x\<bar> < s -->\<bar>f z - f x - f' x * (z - x)\<bar> \<le> e/2 * \<bar>z - x\<bar>"
1.468 -apply clarify
1.469 -apply (case_tac "z = x", simp)
1.470 -apply (drule_tac x = z in spec)
1.471 -apply (rule_tac z1 = "\<bar>inverse (z - x)\<bar>"
1.472 - in real_mult_le_cancel_iff2 [THEN iffD1])
1.473 - apply simp
1.474 -apply (simp del: abs_inverse abs_mult add: abs_mult [symmetric]
1.475 - mult_assoc [symmetric])
1.476 -apply (subgoal_tac "inverse (z - x) * (f z - f x - f' x * (z - x))
1.477 - = (f z - f x) / (z - x) - f' x")
1.478 - apply (simp add: abs_mult [symmetric] mult_ac diff_minus)
1.479 -apply (subst mult_commute)
1.480 -apply (simp add: left_distrib diff_minus)
1.481 -apply (simp add: mult_assoc divide_inverse)
1.482 -apply (simp add: left_distrib)
1.483 -done
1.484 -
1.485 -lemma lemma_straddle:
1.486 - assumes f': "\<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x)" and "0 < e"
1.487 - shows "\<exists>g. gauge {a..b} g &
1.488 - (\<forall>x u v. a \<le> u & u \<le> x & x \<le> v & v \<le> b & (v - u) < g(x)
1.489 - --> \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))"
1.490 -proof -
1.491 - have "\<forall>x\<in>{a..b}.
1.492 - (\<exists>d > 0. \<forall>u v. u \<le> x & x \<le> v & (v - u) < d -->
1.493 - \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))"
1.494 - proof (clarsimp)
1.495 - fix x :: real assume "a \<le> x" and "x \<le> b"
1.496 - with f' have "DERIV f x :> f'(x)" by simp
1.497 - then have "\<forall>r>0. \<exists>s>0. \<forall>z. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < r"
1.498 - by (simp add: DERIV_iff2 LIM_eq)
1.499 - with `0 < e` obtain s
1.500 - where "\<forall>z. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2" and "0 < s"
1.501 - by (drule_tac x="e/2" in spec, auto)
1.502 - then have strad [rule_format]:
1.503 - "\<forall>z. \<bar>z - x\<bar> < s --> \<bar>f z - f x - f' x * (z - x)\<bar> \<le> e/2 * \<bar>z - x\<bar>"
1.504 - using `0 < e` `a \<le> x` `x \<le> b` by (rule strad1)
1.505 - show "\<exists>d>0. \<forall>u v. u \<le> x \<and> x \<le> v \<and> v - u < d \<longrightarrow> \<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u)"
1.506 - proof (safe intro!: exI)
1.507 - show "0 < s" by fact
1.508 - next
1.509 - fix u v :: real assume "u \<le> x" and "x \<le> v" and "v - u < s"
1.510 - have "\<bar>f v - f u - f' x * (v - u)\<bar> =
1.511 - \<bar>(f v - f x - f' x * (v - x)) + (f x - f u - f' x * (x - u))\<bar>"
1.512 - by (simp add: right_diff_distrib)
1.513 - also have "\<dots> \<le> \<bar>f v - f x - f' x * (v - x)\<bar> + \<bar>f x - f u - f' x * (x - u)\<bar>"
1.514 - by (rule abs_triangle_ineq)
1.515 - also have "\<dots> = \<bar>f v - f x - f' x * (v - x)\<bar> + \<bar>f u - f x - f' x * (u - x)\<bar>"
1.516 - by (simp add: right_diff_distrib)
1.517 - also have "\<dots> \<le> (e/2) * \<bar>v - x\<bar> + (e/2) * \<bar>u - x\<bar>"
1.518 - using `u \<le> x` `x \<le> v` `v - u < s` by (intro add_mono strad, simp_all)
1.519 - also have "\<dots> \<le> e * (v - u) / 2 + e * (v - u) / 2"
1.520 - using `u \<le> x` `x \<le> v` `0 < e` by (intro add_mono, simp_all)
1.521 - also have "\<dots> = e * (v - u)"
1.522 - by simp
1.523 - finally show "\<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u)" .
1.524 - qed
1.525 - qed
1.526 - thus ?thesis
1.527 - by (simp add: gauge_def) (drule bchoice, auto)
1.528 -qed
1.529 -
1.530 -lemma fine_listsum_eq_diff:
1.531 - fixes f :: "real \<Rightarrow> real"
1.532 - shows "fine \<delta> (a, b) D \<Longrightarrow> (\<Sum>(u, x, v)\<leftarrow>D. f v - f u) = f b - f a"
1.533 -by (induct set: fine) simp_all
1.534 -
1.535 -lemma FTC1: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
1.536 - ==> Integral(a,b) f' (f(b) - f(a))"
1.537 - apply (drule order_le_imp_less_or_eq, auto)
1.538 - apply (auto simp add: Integral_def2)
1.539 - apply (drule_tac e = "e / (b - a)" in lemma_straddle)
1.540 - apply (simp add: divide_pos_pos)
1.541 - apply clarify
1.542 - apply (rule_tac x="g" in exI, clarify)
1.543 - apply (clarsimp simp add: rsum_def)
1.544 - apply (frule fine_listsum_eq_diff [where f=f])
1.545 - apply (erule subst)
1.546 - apply (subst listsum_subtractf [symmetric])
1.547 - apply (rule listsum_abs [THEN order_trans])
1.548 - apply (subst map_map [unfolded o_def])
1.549 - apply (subgoal_tac "e = (\<Sum>(u, x, v)\<leftarrow>D. (e / (b - a)) * (v - u))")
1.550 - apply (erule ssubst)
1.551 - apply (simp add: abs_minus_commute)
1.552 - apply (rule listsum_mono)
1.553 - apply (clarify, rename_tac u x v)
1.554 - apply ((drule spec)+, erule mp)
1.555 - apply (simp add: mem_fine mem_fine2 mem_fine3)
1.556 - apply (frule fine_listsum_eq_diff [where f="\<lambda>x. x"])
1.557 - apply (simp only: split_def)
1.558 - apply (subst listsum_const_mult)
1.559 - apply simp
1.560 -done
1.561 -
1.562 -lemma Integral_subst: "[| Integral(a,b) f k1; k2=k1 |] ==> Integral(a,b) f k2"
1.563 -by simp
1.564 -
1.565 -subsection {* Additivity Theorem of Gauge Integral *}
1.566 -
1.567 -text{* Bartle/Sherbert: Theorem 10.1.5 p. 278 *}
1.568 -lemma Integral_add_fun:
1.569 - "[| a \<le> b; Integral(a,b) f k1; Integral(a,b) g k2 |]
1.570 - ==> Integral(a,b) (%x. f x + g x) (k1 + k2)"
1.571 -unfolding Integral_def
1.572 -apply clarify
1.573 -apply (drule_tac x = "e/2" in spec)+
1.574 -apply clarsimp
1.575 -apply (rule_tac x = "\<lambda>x. min (\<delta> x) (\<delta>' x)" in exI)
1.576 -apply (rule conjI, erule (1) gauge_min)
1.577 -apply clarify
1.578 -apply (drule fine_min)
1.579 -apply (drule_tac x=D in spec, simp)+
1.580 -apply (drule_tac a = "\<bar>rsum D f - k1\<bar> * 2" and c = "\<bar>rsum D g - k2\<bar> * 2" in add_strict_mono, assumption)
1.581 -apply (auto simp only: rsum_add left_distrib [symmetric]
1.582 - mult_2_right [symmetric] real_mult_less_iff1)
1.583 -done
1.584 -
1.585 -lemma lemma_Integral_rsum_le:
1.586 - "[| \<forall>x. a \<le> x & x \<le> b --> f x \<le> g x;
1.587 - fine \<delta> (a,b) D
1.588 - |] ==> rsum D f \<le> rsum D g"
1.589 -unfolding rsum_def
1.590 -apply (rule listsum_mono)
1.591 -apply clarify
1.592 -apply (rule mult_right_mono)
1.593 -apply (drule spec, erule mp)
1.594 -apply (frule (1) mem_fine)
1.595 -apply (frule (1) mem_fine2)
1.596 -apply simp
1.597 -apply (frule (1) mem_fine)
1.598 -apply simp
1.599 -done
1.600 -
1.601 -lemma Integral_le:
1.602 - "[| a \<le> b;
1.603 - \<forall>x. a \<le> x & x \<le> b --> f(x) \<le> g(x);
1.604 - Integral(a,b) f k1; Integral(a,b) g k2
1.605 - |] ==> k1 \<le> k2"
1.606 -apply (simp add: Integral_def)
1.607 -apply (rotate_tac 2)
1.608 -apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec)
1.609 -apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec, auto)
1.610 -apply (drule gauge_min, assumption)
1.611 -apply (drule_tac \<delta> = "\<lambda>x. min (\<delta> x) (\<delta>' x)" in fine_exists, assumption, clarify)
1.612 -apply (drule fine_min)
1.613 -apply (drule_tac x = D in spec, drule_tac x = D in spec, clarsimp)
1.614 -apply (frule lemma_Integral_rsum_le, assumption)
1.615 -apply (subgoal_tac "\<bar>(rsum D f - k1) - (rsum D g - k2)\<bar> < \<bar>k1 - k2\<bar>")
1.616 -apply arith
1.617 -apply (drule add_strict_mono, assumption)
1.618 -apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
1.619 - real_mult_less_iff1)
1.620 -done
1.621 -
1.622 -lemma Integral_imp_Cauchy:
1.623 - "(\<exists>k. Integral(a,b) f k) ==>
1.624 - (\<forall>e > 0. \<exists>\<delta>. gauge {a..b} \<delta> &
1.625 - (\<forall>D1 D2.
1.626 - fine \<delta> (a,b) D1 &
1.627 - fine \<delta> (a,b) D2 -->
1.628 - \<bar>rsum D1 f - rsum D2 f\<bar> < e))"
1.629 -apply (simp add: Integral_def, auto)
1.630 -apply (drule_tac x = "e/2" in spec, auto)
1.631 -apply (rule exI, auto)
1.632 -apply (frule_tac x = D1 in spec)
1.633 -apply (drule_tac x = D2 in spec)
1.634 -apply simp
1.635 -apply (thin_tac "0 < e")
1.636 -apply (drule add_strict_mono, assumption)
1.637 -apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
1.638 - real_mult_less_iff1)
1.639 -done
1.640 -
1.641 -lemma Cauchy_iff2:
1.642 - "Cauchy X =
1.643 - (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))"
1.644 -apply (simp add: Cauchy_iff, auto)
1.645 -apply (drule reals_Archimedean, safe)
1.646 -apply (drule_tac x = n in spec, auto)
1.647 -apply (rule_tac x = M in exI, auto)
1.648 -apply (drule_tac x = m in spec, simp)
1.649 -apply (drule_tac x = na in spec, auto)
1.650 -done
1.651 -
1.652 -lemma monotonic_anti_derivative:
1.653 - fixes f g :: "real => real" shows
1.654 - "[| a \<le> b; \<forall>c. a \<le> c & c \<le> b --> f' c \<le> g' c;
1.655 - \<forall>x. DERIV f x :> f' x; \<forall>x. DERIV g x :> g' x |]
1.656 - ==> f b - f a \<le> g b - g a"
1.657 -apply (rule Integral_le, assumption)
1.658 -apply (auto intro: FTC1)
1.659 -done
1.660 -
1.661 -end
2.1 --- a/src/HOL/IsaMakefile Mon Feb 22 20:08:10 2010 +0100
2.2 +++ b/src/HOL/IsaMakefile Tue Feb 23 17:33:03 2010 +0100
2.3 @@ -965,11 +965,12 @@
2.4 ex/Codegenerator_Pretty.thy ex/Codegenerator_Pretty_Test.thy \
2.5 ex/Codegenerator_Test.thy ex/Coherent.thy \
2.6 ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy \
2.7 - ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \
2.8 - ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \
2.9 - ex/Hilbert_Classical.thy ex/Induction_Schema.thy \
2.10 - ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \
2.11 - ex/Intuitionistic.thy ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy \
2.12 + ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy \
2.13 + ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy \
2.14 + ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy \
2.15 + ex/Induction_Schema.thy ex/InductiveInvariant.thy \
2.16 + ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy \
2.17 + ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy \
2.18 ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \
2.19 ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy \
2.20 ex/Predicate_Compile_ex.thy ex/Predicate_Compile_Quickcheck.thy \
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/ex/Gauge_Integration.thy Tue Feb 23 17:33:03 2010 +0100
3.3 @@ -0,0 +1,573 @@
3.4 +(* Author: Jacques D. Fleuriot, University of Edinburgh
3.5 + Conversion to Isar and new proofs by Lawrence C Paulson, 2004
3.6 +
3.7 + Replaced by ~~/src/HOL/Multivariate_Analysis/Real_Integral.thy .
3.8 +*)
3.9 +
3.10 +header{*Theory of Integration on real intervals*}
3.11 +
3.12 +theory Gauge_Integration
3.13 +imports Complex_Main
3.14 +begin
3.15 +
3.16 +text {*
3.17 +
3.18 +\textbf{Attention}: This theory defines the Integration on real
3.19 +intervals. This is just a example theory for historical / expository interests.
3.20 +A better replacement is found in the Multivariate Analysis library. This defines
3.21 +the gauge integral on real vector spaces and in the Real Integral theory
3.22 +is a specialization to the integral on arbitrary real intervals. The
3.23 +Multivariate Analysis package also provides a better support for analysis on
3.24 +integrals.
3.25 +
3.26 +*}
3.27 +
3.28 +text{*We follow John Harrison in formalizing the Gauge integral.*}
3.29 +
3.30 +subsection {* Gauges *}
3.31 +
3.32 +definition
3.33 + gauge :: "[real set, real => real] => bool" where
3.34 + [code del]:"gauge E g = (\<forall>x\<in>E. 0 < g(x))"
3.35 +
3.36 +
3.37 +subsection {* Gauge-fine divisions *}
3.38 +
3.39 +inductive
3.40 + fine :: "[real \<Rightarrow> real, real \<times> real, (real \<times> real \<times> real) list] \<Rightarrow> bool"
3.41 +for
3.42 + \<delta> :: "real \<Rightarrow> real"
3.43 +where
3.44 + fine_Nil:
3.45 + "fine \<delta> (a, a) []"
3.46 +| fine_Cons:
3.47 + "\<lbrakk>fine \<delta> (b, c) D; a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk>
3.48 + \<Longrightarrow> fine \<delta> (a, c) ((a, x, b) # D)"
3.49 +
3.50 +lemmas fine_induct [induct set: fine] =
3.51 + fine.induct [of "\<delta>" "(a,b)" "D" "split P", unfolded split_conv, standard]
3.52 +
3.53 +lemma fine_single:
3.54 + "\<lbrakk>a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk> \<Longrightarrow> fine \<delta> (a, b) [(a, x, b)]"
3.55 +by (rule fine_Cons [OF fine_Nil])
3.56 +
3.57 +lemma fine_append:
3.58 + "\<lbrakk>fine \<delta> (a, b) D; fine \<delta> (b, c) D'\<rbrakk> \<Longrightarrow> fine \<delta> (a, c) (D @ D')"
3.59 +by (induct set: fine, simp, simp add: fine_Cons)
3.60 +
3.61 +lemma fine_imp_le: "fine \<delta> (a, b) D \<Longrightarrow> a \<le> b"
3.62 +by (induct set: fine, simp_all)
3.63 +
3.64 +lemma nonempty_fine_imp_less: "\<lbrakk>fine \<delta> (a, b) D; D \<noteq> []\<rbrakk> \<Longrightarrow> a < b"
3.65 +apply (induct set: fine, simp)
3.66 +apply (drule fine_imp_le, simp)
3.67 +done
3.68 +
3.69 +lemma empty_fine_imp_eq: "\<lbrakk>fine \<delta> (a, b) D; D = []\<rbrakk> \<Longrightarrow> a = b"
3.70 +by (induct set: fine, simp_all)
3.71 +
3.72 +lemma fine_eq: "fine \<delta> (a, b) D \<Longrightarrow> a = b \<longleftrightarrow> D = []"
3.73 +apply (cases "D = []")
3.74 +apply (drule (1) empty_fine_imp_eq, simp)
3.75 +apply (drule (1) nonempty_fine_imp_less, simp)
3.76 +done
3.77 +
3.78 +lemma mem_fine:
3.79 + "\<lbrakk>fine \<delta> (a, b) D; (u, x, v) \<in> set D\<rbrakk> \<Longrightarrow> u < v \<and> u \<le> x \<and> x \<le> v"
3.80 +by (induct set: fine, simp, force)
3.81 +
3.82 +lemma mem_fine2: "\<lbrakk>fine \<delta> (a, b) D; (u, z, v) \<in> set D\<rbrakk> \<Longrightarrow> a \<le> u \<and> v \<le> b"
3.83 +apply (induct arbitrary: z u v set: fine, auto)
3.84 +apply (simp add: fine_imp_le)
3.85 +apply (erule order_trans [OF less_imp_le], simp)
3.86 +done
3.87 +
3.88 +lemma mem_fine3: "\<lbrakk>fine \<delta> (a, b) D; (u, z, v) \<in> set D\<rbrakk> \<Longrightarrow> v - u < \<delta> z"
3.89 +by (induct arbitrary: z u v set: fine) auto
3.90 +
3.91 +lemma BOLZANO:
3.92 + fixes P :: "real \<Rightarrow> real \<Rightarrow> bool"
3.93 + assumes 1: "a \<le> b"
3.94 + assumes 2: "\<And>a b c. \<lbrakk>P a b; P b c; a \<le> b; b \<le> c\<rbrakk> \<Longrightarrow> P a c"
3.95 + assumes 3: "\<And>x. \<exists>d>0. \<forall>a b. a \<le> x & x \<le> b & (b-a) < d \<longrightarrow> P a b"
3.96 + shows "P a b"
3.97 +apply (subgoal_tac "split P (a,b)", simp)
3.98 +apply (rule lemma_BOLZANO [OF _ _ 1])
3.99 +apply (clarify, erule (3) 2)
3.100 +apply (clarify, rule 3)
3.101 +done
3.102 +
3.103 +text{*We can always find a division that is fine wrt any gauge*}
3.104 +
3.105 +lemma fine_exists:
3.106 + assumes "a \<le> b" and "gauge {a..b} \<delta>" shows "\<exists>D. fine \<delta> (a, b) D"
3.107 +proof -
3.108 + {
3.109 + fix u v :: real assume "u \<le> v"
3.110 + have "a \<le> u \<Longrightarrow> v \<le> b \<Longrightarrow> \<exists>D. fine \<delta> (u, v) D"
3.111 + apply (induct u v rule: BOLZANO, rule `u \<le> v`)
3.112 + apply (simp, fast intro: fine_append)
3.113 + apply (case_tac "a \<le> x \<and> x \<le> b")
3.114 + apply (rule_tac x="\<delta> x" in exI)
3.115 + apply (rule conjI)
3.116 + apply (simp add: `gauge {a..b} \<delta>` [unfolded gauge_def])
3.117 + apply (clarify, rename_tac u v)
3.118 + apply (case_tac "u = v")
3.119 + apply (fast intro: fine_Nil)
3.120 + apply (subgoal_tac "u < v", fast intro: fine_single, simp)
3.121 + apply (rule_tac x="1" in exI, clarsimp)
3.122 + done
3.123 + }
3.124 + with `a \<le> b` show ?thesis by auto
3.125 +qed
3.126 +
3.127 +lemma fine_covers_all:
3.128 + assumes "fine \<delta> (a, c) D" and "a < x" and "x \<le> c"
3.129 + shows "\<exists> N < length D. \<forall> d t e. D ! N = (d,t,e) \<longrightarrow> d < x \<and> x \<le> e"
3.130 + using assms
3.131 +proof (induct set: fine)
3.132 + case (2 b c D a t)
3.133 + thus ?case
3.134 + proof (cases "b < x")
3.135 + case True
3.136 + with 2 obtain N where *: "N < length D"
3.137 + and **: "\<And> d t e. D ! N = (d,t,e) \<Longrightarrow> d < x \<and> x \<le> e" by auto
3.138 + hence "Suc N < length ((a,t,b)#D) \<and>
3.139 + (\<forall> d t' e. ((a,t,b)#D) ! Suc N = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
3.140 + thus ?thesis by auto
3.141 + next
3.142 + case False with 2
3.143 + have "0 < length ((a,t,b)#D) \<and>
3.144 + (\<forall> d t' e. ((a,t,b)#D) ! 0 = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
3.145 + thus ?thesis by auto
3.146 + qed
3.147 +qed auto
3.148 +
3.149 +lemma fine_append_split:
3.150 + assumes "fine \<delta> (a,b) D" and "D2 \<noteq> []" and "D = D1 @ D2"
3.151 + shows "fine \<delta> (a,fst (hd D2)) D1" (is "?fine1")
3.152 + and "fine \<delta> (fst (hd D2), b) D2" (is "?fine2")
3.153 +proof -
3.154 + from assms
3.155 + have "?fine1 \<and> ?fine2"
3.156 + proof (induct arbitrary: D1 D2)
3.157 + case (2 b c D a' x D1 D2)
3.158 + note induct = this
3.159 +
3.160 + thus ?case
3.161 + proof (cases D1)
3.162 + case Nil
3.163 + hence "fst (hd D2) = a'" using 2 by auto
3.164 + with fine_Cons[OF `fine \<delta> (b,c) D` induct(3,4,5)] Nil induct
3.165 + show ?thesis by (auto intro: fine_Nil)
3.166 + next
3.167 + case (Cons d1 D1')
3.168 + with induct(2)[OF `D2 \<noteq> []`, of D1'] induct(8)
3.169 + have "fine \<delta> (b, fst (hd D2)) D1'" and "fine \<delta> (fst (hd D2), c) D2" and
3.170 + "d1 = (a', x, b)" by auto
3.171 + with fine_Cons[OF this(1) induct(3,4,5), OF induct(6)] Cons
3.172 + show ?thesis by auto
3.173 + qed
3.174 + qed auto
3.175 + thus ?fine1 and ?fine2 by auto
3.176 +qed
3.177 +
3.178 +lemma fine_\<delta>_expand:
3.179 + assumes "fine \<delta> (a,b) D"
3.180 + and "\<And> x. \<lbrakk> a \<le> x ; x \<le> b \<rbrakk> \<Longrightarrow> \<delta> x \<le> \<delta>' x"
3.181 + shows "fine \<delta>' (a,b) D"
3.182 +using assms proof induct
3.183 + case 1 show ?case by (rule fine_Nil)
3.184 +next
3.185 + case (2 b c D a x)
3.186 + show ?case
3.187 + proof (rule fine_Cons)
3.188 + show "fine \<delta>' (b,c) D" using 2 by auto
3.189 + from fine_imp_le[OF 2(1)] 2(6) `x \<le> b`
3.190 + show "b - a < \<delta>' x"
3.191 + using 2(7)[OF `a \<le> x`] by auto
3.192 + qed (auto simp add: 2)
3.193 +qed
3.194 +
3.195 +lemma fine_single_boundaries:
3.196 + assumes "fine \<delta> (a,b) D" and "D = [(d, t, e)]"
3.197 + shows "a = d \<and> b = e"
3.198 +using assms proof induct
3.199 + case (2 b c D a x)
3.200 + hence "D = []" and "a = d" and "b = e" by auto
3.201 + moreover
3.202 + from `fine \<delta> (b,c) D` `D = []` have "b = c"
3.203 + by (rule empty_fine_imp_eq)
3.204 + ultimately show ?case by simp
3.205 +qed auto
3.206 +
3.207 +lemma fine_listsum_eq_diff:
3.208 + fixes f :: "real \<Rightarrow> real"
3.209 + shows "fine \<delta> (a, b) D \<Longrightarrow> (\<Sum>(u, x, v)\<leftarrow>D. f v - f u) = f b - f a"
3.210 +by (induct set: fine) simp_all
3.211 +
3.212 +text{*Lemmas about combining gauges*}
3.213 +
3.214 +lemma gauge_min:
3.215 + "[| gauge(E) g1; gauge(E) g2 |]
3.216 + ==> gauge(E) (%x. min (g1(x)) (g2(x)))"
3.217 +by (simp add: gauge_def)
3.218 +
3.219 +lemma fine_min:
3.220 + "fine (%x. min (g1(x)) (g2(x))) (a,b) D
3.221 + ==> fine(g1) (a,b) D & fine(g2) (a,b) D"
3.222 +apply (erule fine.induct)
3.223 +apply (simp add: fine_Nil)
3.224 +apply (simp add: fine_Cons)
3.225 +done
3.226 +
3.227 +subsection {* Riemann sum *}
3.228 +
3.229 +definition
3.230 + rsum :: "[(real \<times> real \<times> real) list, real \<Rightarrow> real] \<Rightarrow> real" where
3.231 + "rsum D f = (\<Sum>(u, x, v)\<leftarrow>D. f x * (v - u))"
3.232 +
3.233 +lemma rsum_Nil [simp]: "rsum [] f = 0"
3.234 +unfolding rsum_def by simp
3.235 +
3.236 +lemma rsum_Cons [simp]: "rsum ((u, x, v) # D) f = f x * (v - u) + rsum D f"
3.237 +unfolding rsum_def by simp
3.238 +
3.239 +lemma rsum_zero [simp]: "rsum D (\<lambda>x. 0) = 0"
3.240 +by (induct D, auto)
3.241 +
3.242 +lemma rsum_left_distrib: "rsum D f * c = rsum D (\<lambda>x. f x * c)"
3.243 +by (induct D, auto simp add: algebra_simps)
3.244 +
3.245 +lemma rsum_right_distrib: "c * rsum D f = rsum D (\<lambda>x. c * f x)"
3.246 +by (induct D, auto simp add: algebra_simps)
3.247 +
3.248 +lemma rsum_add: "rsum D (\<lambda>x. f x + g x) = rsum D f + rsum D g"
3.249 +by (induct D, auto simp add: algebra_simps)
3.250 +
3.251 +lemma rsum_append: "rsum (D1 @ D2) f = rsum D1 f + rsum D2 f"
3.252 +unfolding rsum_def map_append listsum_append ..
3.253 +
3.254 +
3.255 +subsection {* Gauge integrability (definite) *}
3.256 +
3.257 +definition
3.258 + Integral :: "[(real*real),real=>real,real] => bool" where
3.259 + [code del]: "Integral = (%(a,b) f k. \<forall>e > 0.
3.260 + (\<exists>\<delta>. gauge {a .. b} \<delta> &
3.261 + (\<forall>D. fine \<delta> (a,b) D -->
3.262 + \<bar>rsum D f - k\<bar> < e)))"
3.263 +
3.264 +lemma Integral_def2:
3.265 + "Integral = (%(a,b) f k. \<forall>e>0. (\<exists>\<delta>. gauge {a..b} \<delta> &
3.266 + (\<forall>D. fine \<delta> (a,b) D -->
3.267 + \<bar>rsum D f - k\<bar> \<le> e)))"
3.268 +unfolding Integral_def
3.269 +apply (safe intro!: ext)
3.270 +apply (fast intro: less_imp_le)
3.271 +apply (drule_tac x="e/2" in spec)
3.272 +apply force
3.273 +done
3.274 +
3.275 +text{*The integral is unique if it exists*}
3.276 +
3.277 +lemma Integral_unique:
3.278 + "[| a \<le> b; Integral(a,b) f k1; Integral(a,b) f k2 |] ==> k1 = k2"
3.279 +apply (simp add: Integral_def)
3.280 +apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec)+
3.281 +apply auto
3.282 +apply (drule gauge_min, assumption)
3.283 +apply (drule_tac \<delta> = "%x. min (\<delta> x) (\<delta>' x)"
3.284 + in fine_exists, assumption, auto)
3.285 +apply (drule fine_min)
3.286 +apply (drule spec)+
3.287 +apply auto
3.288 +apply (subgoal_tac "\<bar>(rsum D f - k2) - (rsum D f - k1)\<bar> < \<bar>k1 - k2\<bar>")
3.289 +apply arith
3.290 +apply (drule add_strict_mono, assumption)
3.291 +apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
3.292 + mult_less_cancel_right)
3.293 +done
3.294 +
3.295 +lemma Integral_zero [simp]: "Integral(a,a) f 0"
3.296 +apply (auto simp add: Integral_def)
3.297 +apply (rule_tac x = "%x. 1" in exI)
3.298 +apply (auto dest: fine_eq simp add: gauge_def rsum_def)
3.299 +done
3.300 +
3.301 +lemma fine_rsum_const: "fine \<delta> (a,b) D \<Longrightarrow> rsum D (\<lambda>x. c) = (c * (b - a))"
3.302 +unfolding rsum_def
3.303 +by (induct set: fine, auto simp add: algebra_simps)
3.304 +
3.305 +lemma Integral_eq_diff_bounds: "a \<le> b ==> Integral(a,b) (%x. 1) (b - a)"
3.306 +apply (cases "a = b", simp)
3.307 +apply (simp add: Integral_def, clarify)
3.308 +apply (rule_tac x = "%x. b - a" in exI)
3.309 +apply (rule conjI, simp add: gauge_def)
3.310 +apply (clarify)
3.311 +apply (subst fine_rsum_const, assumption, simp)
3.312 +done
3.313 +
3.314 +lemma Integral_mult_const: "a \<le> b ==> Integral(a,b) (%x. c) (c*(b - a))"
3.315 +apply (cases "a = b", simp)
3.316 +apply (simp add: Integral_def, clarify)
3.317 +apply (rule_tac x = "%x. b - a" in exI)
3.318 +apply (rule conjI, simp add: gauge_def)
3.319 +apply (clarify)
3.320 +apply (subst fine_rsum_const, assumption, simp)
3.321 +done
3.322 +
3.323 +lemma Integral_mult:
3.324 + "[| a \<le> b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)"
3.325 +apply (auto simp add: order_le_less
3.326 + dest: Integral_unique [OF order_refl Integral_zero])
3.327 +apply (auto simp add: Integral_def setsum_right_distrib[symmetric] mult_assoc)
3.328 +apply (case_tac "c = 0", force)
3.329 +apply (drule_tac x = "e/abs c" in spec)
3.330 +apply (simp add: divide_pos_pos)
3.331 +apply clarify
3.332 +apply (rule_tac x="\<delta>" in exI, clarify)
3.333 +apply (drule_tac x="D" in spec, clarify)
3.334 +apply (simp add: pos_less_divide_eq abs_mult [symmetric]
3.335 + algebra_simps rsum_right_distrib)
3.336 +done
3.337 +
3.338 +lemma Integral_add:
3.339 + assumes "Integral (a, b) f x1"
3.340 + assumes "Integral (b, c) f x2"
3.341 + assumes "a \<le> b" and "b \<le> c"
3.342 + shows "Integral (a, c) f (x1 + x2)"
3.343 +proof (cases "a < b \<and> b < c", simp only: Integral_def split_conv, rule allI, rule impI)
3.344 + fix \<epsilon> :: real assume "0 < \<epsilon>"
3.345 + hence "0 < \<epsilon> / 2" by auto
3.346 +
3.347 + assume "a < b \<and> b < c"
3.348 + hence "a < b" and "b < c" by auto
3.349 +
3.350 + from `Integral (a, b) f x1`[simplified Integral_def split_conv,
3.351 + rule_format, OF `0 < \<epsilon>/2`]
3.352 + obtain \<delta>1 where \<delta>1_gauge: "gauge {a..b} \<delta>1"
3.353 + and I1: "\<And> D. fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f - x1 \<bar> < (\<epsilon> / 2)" by auto
3.354 +
3.355 + from `Integral (b, c) f x2`[simplified Integral_def split_conv,
3.356 + rule_format, OF `0 < \<epsilon>/2`]
3.357 + obtain \<delta>2 where \<delta>2_gauge: "gauge {b..c} \<delta>2"
3.358 + and I2: "\<And> D. fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)" by auto
3.359 +
3.360 + def \<delta> \<equiv> "\<lambda> x. if x < b then min (\<delta>1 x) (b - x)
3.361 + else if x = b then min (\<delta>1 b) (\<delta>2 b)
3.362 + else min (\<delta>2 x) (x - b)"
3.363 +
3.364 + have "gauge {a..c} \<delta>"
3.365 + using \<delta>1_gauge \<delta>2_gauge unfolding \<delta>_def gauge_def by auto
3.366 + moreover {
3.367 + fix D :: "(real \<times> real \<times> real) list"
3.368 + assume fine: "fine \<delta> (a,c) D"
3.369 + from fine_covers_all[OF this `a < b` `b \<le> c`]
3.370 + obtain N where "N < length D"
3.371 + and *: "\<forall> d t e. D ! N = (d, t, e) \<longrightarrow> d < b \<and> b \<le> e"
3.372 + by auto
3.373 + obtain d t e where D_eq: "D ! N = (d, t, e)" by (cases "D!N", auto)
3.374 + with * have "d < b" and "b \<le> e" by auto
3.375 + have in_D: "(d, t, e) \<in> set D"
3.376 + using D_eq[symmetric] using `N < length D` by auto
3.377 +
3.378 + from mem_fine[OF fine in_D]
3.379 + have "d < e" and "d \<le> t" and "t \<le> e" by auto
3.380 +
3.381 + have "t = b"
3.382 + proof (rule ccontr)
3.383 + assume "t \<noteq> b"
3.384 + with mem_fine3[OF fine in_D] `b \<le> e` `d \<le> t` `t \<le> e` `d < b` \<delta>_def
3.385 + show False by (cases "t < b") auto
3.386 + qed
3.387 +
3.388 + let ?D1 = "take N D"
3.389 + let ?D2 = "drop N D"
3.390 + def D1 \<equiv> "take N D @ [(d, t, b)]"
3.391 + def D2 \<equiv> "(if b = e then [] else [(b, t, e)]) @ drop (Suc N) D"
3.392 +
3.393 + have "D \<noteq> []" using `N < length D` by auto
3.394 + from hd_drop_conv_nth[OF this `N < length D`]
3.395 + have "fst (hd ?D2) = d" using `D ! N = (d, t, e)` by auto
3.396 + with fine_append_split[OF _ _ append_take_drop_id[symmetric]]
3.397 + have fine1: "fine \<delta> (a,d) ?D1" and fine2: "fine \<delta> (d,c) ?D2"
3.398 + using `N < length D` fine by auto
3.399 +
3.400 + have "fine \<delta>1 (a,b) D1" unfolding D1_def
3.401 + proof (rule fine_append)
3.402 + show "fine \<delta>1 (a, d) ?D1"
3.403 + proof (rule fine1[THEN fine_\<delta>_expand])
3.404 + fix x assume "a \<le> x" "x \<le> d"
3.405 + hence "x \<le> b" using `d < b` `x \<le> d` by auto
3.406 + thus "\<delta> x \<le> \<delta>1 x" unfolding \<delta>_def by auto
3.407 + qed
3.408 +
3.409 + have "b - d < \<delta>1 t"
3.410 + using mem_fine3[OF fine in_D] \<delta>_def `b \<le> e` `t = b` by auto
3.411 + from `d < b` `d \<le> t` `t = b` this
3.412 + show "fine \<delta>1 (d, b) [(d, t, b)]" using fine_single by auto
3.413 + qed
3.414 + note rsum1 = I1[OF this]
3.415 +
3.416 + have drop_split: "drop N D = [D ! N] @ drop (Suc N) D"
3.417 + using nth_drop'[OF `N < length D`] by simp
3.418 +
3.419 + have fine2: "fine \<delta>2 (e,c) (drop (Suc N) D)"
3.420 + proof (cases "drop (Suc N) D = []")
3.421 + case True
3.422 + note * = fine2[simplified drop_split True D_eq append_Nil2]
3.423 + have "e = c" using fine_single_boundaries[OF * refl] by auto
3.424 + thus ?thesis unfolding True using fine_Nil by auto
3.425 + next
3.426 + case False
3.427 + note * = fine_append_split[OF fine2 False drop_split]
3.428 + from fine_single_boundaries[OF *(1)]
3.429 + have "fst (hd (drop (Suc N) D)) = e" using D_eq by auto
3.430 + with *(2) have "fine \<delta> (e,c) (drop (Suc N) D)" by auto
3.431 + thus ?thesis
3.432 + proof (rule fine_\<delta>_expand)
3.433 + fix x assume "e \<le> x" and "x \<le> c"
3.434 + thus "\<delta> x \<le> \<delta>2 x" using `b \<le> e` unfolding \<delta>_def by auto
3.435 + qed
3.436 + qed
3.437 +
3.438 + have "fine \<delta>2 (b, c) D2"
3.439 + proof (cases "e = b")
3.440 + case True thus ?thesis using fine2 by (simp add: D1_def D2_def)
3.441 + next
3.442 + case False
3.443 + have "e - b < \<delta>2 b"
3.444 + using mem_fine3[OF fine in_D] \<delta>_def `d < b` `t = b` by auto
3.445 + with False `t = b` `b \<le> e`
3.446 + show ?thesis using D2_def
3.447 + by (auto intro!: fine_append[OF _ fine2] fine_single
3.448 + simp del: append_Cons)
3.449 + qed
3.450 + note rsum2 = I2[OF this]
3.451 +
3.452 + have "rsum D f = rsum (take N D) f + rsum [D ! N] f + rsum (drop (Suc N) D) f"
3.453 + using rsum_append[symmetric] nth_drop'[OF `N < length D`] by auto
3.454 + also have "\<dots> = rsum D1 f + rsum D2 f"
3.455 + by (cases "b = e", auto simp add: D1_def D2_def D_eq rsum_append algebra_simps)
3.456 + finally have "\<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>"
3.457 + using add_strict_mono[OF rsum1 rsum2] by simp
3.458 + }
3.459 + ultimately show "\<exists> \<delta>. gauge {a .. c} \<delta> \<and>
3.460 + (\<forall>D. fine \<delta> (a,c) D \<longrightarrow> \<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>)"
3.461 + by blast
3.462 +next
3.463 + case False
3.464 + hence "a = b \<or> b = c" using `a \<le> b` and `b \<le> c` by auto
3.465 + thus ?thesis
3.466 + proof (rule disjE)
3.467 + assume "a = b" hence "x1 = 0"
3.468 + using `Integral (a, b) f x1` Integral_zero Integral_unique[of a b] by auto
3.469 + thus ?thesis using `a = b` `Integral (b, c) f x2` by auto
3.470 + next
3.471 + assume "b = c" hence "x2 = 0"
3.472 + using `Integral (b, c) f x2` Integral_zero Integral_unique[of b c] by auto
3.473 + thus ?thesis using `b = c` `Integral (a, b) f x1` by auto
3.474 + qed
3.475 +qed
3.476 +
3.477 +text{*Fundamental theorem of calculus (Part I)*}
3.478 +
3.479 +text{*"Straddle Lemma" : Swartz and Thompson: AMM 95(7) 1988 *}
3.480 +
3.481 +lemma strad1:
3.482 + "\<lbrakk>\<forall>z::real. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow>
3.483 + \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2;
3.484 + 0 < s; 0 < e; a \<le> x; x \<le> b\<rbrakk>
3.485 + \<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>"
3.486 +apply clarify
3.487 +apply (case_tac "z = x", simp)
3.488 +apply (drule_tac x = z in spec)
3.489 +apply (rule_tac z1 = "\<bar>inverse (z - x)\<bar>"
3.490 + in real_mult_le_cancel_iff2 [THEN iffD1])
3.491 + apply simp
3.492 +apply (simp del: abs_inverse abs_mult add: abs_mult [symmetric]
3.493 + mult_assoc [symmetric])
3.494 +apply (subgoal_tac "inverse (z - x) * (f z - f x - f' x * (z - x))
3.495 + = (f z - f x) / (z - x) - f' x")
3.496 + apply (simp add: abs_mult [symmetric] mult_ac diff_minus)
3.497 +apply (subst mult_commute)
3.498 +apply (simp add: left_distrib diff_minus)
3.499 +apply (simp add: mult_assoc divide_inverse)
3.500 +apply (simp add: left_distrib)
3.501 +done
3.502 +
3.503 +lemma lemma_straddle:
3.504 + assumes f': "\<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x)" and "0 < e"
3.505 + shows "\<exists>g. gauge {a..b} g &
3.506 + (\<forall>x u v. a \<le> u & u \<le> x & x \<le> v & v \<le> b & (v - u) < g(x)
3.507 + --> \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))"
3.508 +proof -
3.509 + have "\<forall>x\<in>{a..b}.
3.510 + (\<exists>d > 0. \<forall>u v. u \<le> x & x \<le> v & (v - u) < d -->
3.511 + \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))"
3.512 + proof (clarsimp)
3.513 + fix x :: real assume "a \<le> x" and "x \<le> b"
3.514 + with f' have "DERIV f x :> f'(x)" by simp
3.515 + 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"
3.516 + by (simp add: DERIV_iff2 LIM_eq)
3.517 + with `0 < e` obtain s
3.518 + 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"
3.519 + by (drule_tac x="e/2" in spec, auto)
3.520 + then have strad [rule_format]:
3.521 + "\<forall>z. \<bar>z - x\<bar> < s --> \<bar>f z - f x - f' x * (z - x)\<bar> \<le> e/2 * \<bar>z - x\<bar>"
3.522 + using `0 < e` `a \<le> x` `x \<le> b` by (rule strad1)
3.523 + 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)"
3.524 + proof (safe intro!: exI)
3.525 + show "0 < s" by fact
3.526 + next
3.527 + fix u v :: real assume "u \<le> x" and "x \<le> v" and "v - u < s"
3.528 + have "\<bar>f v - f u - f' x * (v - u)\<bar> =
3.529 + \<bar>(f v - f x - f' x * (v - x)) + (f x - f u - f' x * (x - u))\<bar>"
3.530 + by (simp add: right_diff_distrib)
3.531 + also have "\<dots> \<le> \<bar>f v - f x - f' x * (v - x)\<bar> + \<bar>f x - f u - f' x * (x - u)\<bar>"
3.532 + by (rule abs_triangle_ineq)
3.533 + also have "\<dots> = \<bar>f v - f x - f' x * (v - x)\<bar> + \<bar>f u - f x - f' x * (u - x)\<bar>"
3.534 + by (simp add: right_diff_distrib)
3.535 + also have "\<dots> \<le> (e/2) * \<bar>v - x\<bar> + (e/2) * \<bar>u - x\<bar>"
3.536 + using `u \<le> x` `x \<le> v` `v - u < s` by (intro add_mono strad, simp_all)
3.537 + also have "\<dots> \<le> e * (v - u) / 2 + e * (v - u) / 2"
3.538 + using `u \<le> x` `x \<le> v` `0 < e` by (intro add_mono, simp_all)
3.539 + also have "\<dots> = e * (v - u)"
3.540 + by simp
3.541 + finally show "\<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u)" .
3.542 + qed
3.543 + qed
3.544 + thus ?thesis
3.545 + by (simp add: gauge_def) (drule bchoice, auto)
3.546 +qed
3.547 +
3.548 +lemma fundamental_theorem_of_calculus:
3.549 + "\<lbrakk> a \<le> b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) \<rbrakk>
3.550 + \<Longrightarrow> Integral(a,b) f' (f(b) - f(a))"
3.551 + apply (drule order_le_imp_less_or_eq, auto)
3.552 + apply (auto simp add: Integral_def2)
3.553 + apply (drule_tac e = "e / (b - a)" in lemma_straddle)
3.554 + apply (simp add: divide_pos_pos)
3.555 + apply clarify
3.556 + apply (rule_tac x="g" in exI, clarify)
3.557 + apply (clarsimp simp add: rsum_def)
3.558 + apply (frule fine_listsum_eq_diff [where f=f])
3.559 + apply (erule subst)
3.560 + apply (subst listsum_subtractf [symmetric])
3.561 + apply (rule listsum_abs [THEN order_trans])
3.562 + apply (subst map_map [unfolded o_def])
3.563 + apply (subgoal_tac "e = (\<Sum>(u, x, v)\<leftarrow>D. (e / (b - a)) * (v - u))")
3.564 + apply (erule ssubst)
3.565 + apply (simp add: abs_minus_commute)
3.566 + apply (rule listsum_mono)
3.567 + apply (clarify, rename_tac u x v)
3.568 + apply ((drule spec)+, erule mp)
3.569 + apply (simp add: mem_fine mem_fine2 mem_fine3)
3.570 + apply (frule fine_listsum_eq_diff [where f="\<lambda>x. x"])
3.571 + apply (simp only: split_def)
3.572 + apply (subst listsum_const_mult)
3.573 + apply simp
3.574 +done
3.575 +
3.576 +end
4.1 --- a/src/HOL/ex/ROOT.ML Mon Feb 22 20:08:10 2010 +0100
4.2 +++ b/src/HOL/ex/ROOT.ML Tue Feb 23 17:33:03 2010 +0100
4.3 @@ -67,7 +67,8 @@
4.4 "Quickcheck_Examples",
4.5 "Landau",
4.6 "Execute_Choice",
4.7 - "Summation"
4.8 + "Summation",
4.9 + "Gauge_Integration"
4.10 ];
4.11
4.12 HTML.with_charset "utf-8" (no_document use_thys)