# HG changeset patch # User hoelzl # Date 1266944100 -3600 # Node ID cac5a37fb638c0afbec149b4631746bae893a4e2 # Parent c76b7dcd77ce0e874d74f01d94265cfd579f1142# Parent e8888458dce304af91340df065bc3c5cac007c3d merged diff -r c76b7dcd77ce -r cac5a37fb638 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Feb 23 16:58:21 2010 +0100 +++ b/src/HOL/IsaMakefile Tue Feb 23 17:55:00 2010 +0100 @@ -955,11 +955,12 @@ ex/Codegenerator_Pretty.thy ex/Codegenerator_Pretty_Test.thy \ ex/Codegenerator_Test.thy ex/Coherent.thy \ ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy \ - ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \ - ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \ - ex/Hilbert_Classical.thy ex/Induction_Schema.thy \ - ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \ - ex/Intuitionistic.thy ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy \ + ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy \ + ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy \ + ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy \ + ex/Induction_Schema.thy ex/InductiveInvariant.thy \ + ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy \ + ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy \ ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \ ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy \ ex/Predicate_Compile_ex.thy ex/Predicate_Compile_Quickcheck.thy \ diff -r c76b7dcd77ce -r cac5a37fb638 src/HOL/ex/Gauge_Integration.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Gauge_Integration.thy Tue Feb 23 17:55:00 2010 +0100 @@ -0,0 +1,573 @@ +(* Author: Jacques D. Fleuriot, University of Edinburgh + Conversion to Isar and new proofs by Lawrence C Paulson, 2004 + + Replaced by ~~/src/HOL/Multivariate_Analysis/Real_Integral.thy . +*) + +header{*Theory of Integration on real intervals*} + +theory Gauge_Integration +imports Complex_Main +begin + +text {* + +\textbf{Attention}: This theory defines the Integration on real +intervals. This is just a example theory for historical / expository interests. +A better replacement is found in the Multivariate Analysis library. This defines +the gauge integral on real vector spaces and in the Real Integral theory +is a specialization to the integral on arbitrary real intervals. The +Multivariate Analysis package also provides a better support for analysis on +integrals. + +*} + +text{*We follow John Harrison in formalizing the Gauge integral.*} + +subsection {* Gauges *} + +definition + gauge :: "[real set, real => real] => bool" where + [code del]:"gauge E g = (\x\E. 0 < g(x))" + + +subsection {* Gauge-fine divisions *} + +inductive + fine :: "[real \ real, real \ real, (real \ real \ real) list] \ bool" +for + \ :: "real \ real" +where + fine_Nil: + "fine \ (a, a) []" +| fine_Cons: + "\fine \ (b, c) D; a < b; a \ x; x \ b; b - a < \ x\ + \ fine \ (a, c) ((a, x, b) # D)" + +lemmas fine_induct [induct set: fine] = + fine.induct [of "\" "(a,b)" "D" "split P", unfolded split_conv, standard] + +lemma fine_single: + "\a < b; a \ x; x \ b; b - a < \ x\ \ fine \ (a, b) [(a, x, b)]" +by (rule fine_Cons [OF fine_Nil]) + +lemma fine_append: + "\fine \ (a, b) D; fine \ (b, c) D'\ \ fine \ (a, c) (D @ D')" +by (induct set: fine, simp, simp add: fine_Cons) + +lemma fine_imp_le: "fine \ (a, b) D \ a \ b" +by (induct set: fine, simp_all) + +lemma nonempty_fine_imp_less: "\fine \ (a, b) D; D \ []\ \ a < b" +apply (induct set: fine, simp) +apply (drule fine_imp_le, simp) +done + +lemma empty_fine_imp_eq: "\fine \ (a, b) D; D = []\ \ a = b" +by (induct set: fine, simp_all) + +lemma fine_eq: "fine \ (a, b) D \ a = b \ D = []" +apply (cases "D = []") +apply (drule (1) empty_fine_imp_eq, simp) +apply (drule (1) nonempty_fine_imp_less, simp) +done + +lemma mem_fine: + "\fine \ (a, b) D; (u, x, v) \ set D\ \ u < v \ u \ x \ x \ v" +by (induct set: fine, simp, force) + +lemma mem_fine2: "\fine \ (a, b) D; (u, z, v) \ set D\ \ a \ u \ v \ b" +apply (induct arbitrary: z u v set: fine, auto) +apply (simp add: fine_imp_le) +apply (erule order_trans [OF less_imp_le], simp) +done + +lemma mem_fine3: "\fine \ (a, b) D; (u, z, v) \ set D\ \ v - u < \ z" +by (induct arbitrary: z u v set: fine) auto + +lemma BOLZANO: + fixes P :: "real \ real \ bool" + assumes 1: "a \ b" + assumes 2: "\a b c. \P a b; P b c; a \ b; b \ c\ \ P a c" + assumes 3: "\x. \d>0. \a b. a \ x & x \ b & (b-a) < d \ P a b" + shows "P a b" +apply (subgoal_tac "split P (a,b)", simp) +apply (rule lemma_BOLZANO [OF _ _ 1]) +apply (clarify, erule (3) 2) +apply (clarify, rule 3) +done + +text{*We can always find a division that is fine wrt any gauge*} + +lemma fine_exists: + assumes "a \ b" and "gauge {a..b} \" shows "\D. fine \ (a, b) D" +proof - + { + fix u v :: real assume "u \ v" + have "a \ u \ v \ b \ \D. fine \ (u, v) D" + apply (induct u v rule: BOLZANO, rule `u \ v`) + apply (simp, fast intro: fine_append) + apply (case_tac "a \ x \ x \ b") + apply (rule_tac x="\ x" in exI) + apply (rule conjI) + apply (simp add: `gauge {a..b} \` [unfolded gauge_def]) + apply (clarify, rename_tac u v) + apply (case_tac "u = v") + apply (fast intro: fine_Nil) + apply (subgoal_tac "u < v", fast intro: fine_single, simp) + apply (rule_tac x="1" in exI, clarsimp) + done + } + with `a \ b` show ?thesis by auto +qed + +lemma fine_covers_all: + assumes "fine \ (a, c) D" and "a < x" and "x \ c" + shows "\ N < length D. \ d t e. D ! N = (d,t,e) \ d < x \ x \ e" + using assms +proof (induct set: fine) + case (2 b c D a t) + thus ?case + proof (cases "b < x") + case True + with 2 obtain N where *: "N < length D" + and **: "\ d t e. D ! N = (d,t,e) \ d < x \ x \ e" by auto + hence "Suc N < length ((a,t,b)#D) \ + (\ d t' e. ((a,t,b)#D) ! Suc N = (d,t',e) \ d < x \ x \ e)" by auto + thus ?thesis by auto + next + case False with 2 + have "0 < length ((a,t,b)#D) \ + (\ d t' e. ((a,t,b)#D) ! 0 = (d,t',e) \ d < x \ x \ e)" by auto + thus ?thesis by auto + qed +qed auto + +lemma fine_append_split: + assumes "fine \ (a,b) D" and "D2 \ []" and "D = D1 @ D2" + shows "fine \ (a,fst (hd D2)) D1" (is "?fine1") + and "fine \ (fst (hd D2), b) D2" (is "?fine2") +proof - + from assms + have "?fine1 \ ?fine2" + proof (induct arbitrary: D1 D2) + case (2 b c D a' x D1 D2) + note induct = this + + thus ?case + proof (cases D1) + case Nil + hence "fst (hd D2) = a'" using 2 by auto + with fine_Cons[OF `fine \ (b,c) D` induct(3,4,5)] Nil induct + show ?thesis by (auto intro: fine_Nil) + next + case (Cons d1 D1') + with induct(2)[OF `D2 \ []`, of D1'] induct(8) + have "fine \ (b, fst (hd D2)) D1'" and "fine \ (fst (hd D2), c) D2" and + "d1 = (a', x, b)" by auto + with fine_Cons[OF this(1) induct(3,4,5), OF induct(6)] Cons + show ?thesis by auto + qed + qed auto + thus ?fine1 and ?fine2 by auto +qed + +lemma fine_\_expand: + assumes "fine \ (a,b) D" + and "\ x. \ a \ x ; x \ b \ \ \ x \ \' x" + shows "fine \' (a,b) D" +using assms proof induct + case 1 show ?case by (rule fine_Nil) +next + case (2 b c D a x) + show ?case + proof (rule fine_Cons) + show "fine \' (b,c) D" using 2 by auto + from fine_imp_le[OF 2(1)] 2(6) `x \ b` + show "b - a < \' x" + using 2(7)[OF `a \ x`] by auto + qed (auto simp add: 2) +qed + +lemma fine_single_boundaries: + assumes "fine \ (a,b) D" and "D = [(d, t, e)]" + shows "a = d \ b = e" +using assms proof induct + case (2 b c D a x) + hence "D = []" and "a = d" and "b = e" by auto + moreover + from `fine \ (b,c) D` `D = []` have "b = c" + by (rule empty_fine_imp_eq) + ultimately show ?case by simp +qed auto + +lemma fine_listsum_eq_diff: + fixes f :: "real \ real" + shows "fine \ (a, b) D \ (\(u, x, v)\D. f v - f u) = f b - f a" +by (induct set: fine) simp_all + +text{*Lemmas about combining gauges*} + +lemma gauge_min: + "[| gauge(E) g1; gauge(E) g2 |] + ==> gauge(E) (%x. min (g1(x)) (g2(x)))" +by (simp add: gauge_def) + +lemma fine_min: + "fine (%x. min (g1(x)) (g2(x))) (a,b) D + ==> fine(g1) (a,b) D & fine(g2) (a,b) D" +apply (erule fine.induct) +apply (simp add: fine_Nil) +apply (simp add: fine_Cons) +done + +subsection {* Riemann sum *} + +definition + rsum :: "[(real \ real \ real) list, real \ real] \ real" where + "rsum D f = (\(u, x, v)\D. f x * (v - u))" + +lemma rsum_Nil [simp]: "rsum [] f = 0" +unfolding rsum_def by simp + +lemma rsum_Cons [simp]: "rsum ((u, x, v) # D) f = f x * (v - u) + rsum D f" +unfolding rsum_def by simp + +lemma rsum_zero [simp]: "rsum D (\x. 0) = 0" +by (induct D, auto) + +lemma rsum_left_distrib: "rsum D f * c = rsum D (\x. f x * c)" +by (induct D, auto simp add: algebra_simps) + +lemma rsum_right_distrib: "c * rsum D f = rsum D (\x. c * f x)" +by (induct D, auto simp add: algebra_simps) + +lemma rsum_add: "rsum D (\x. f x + g x) = rsum D f + rsum D g" +by (induct D, auto simp add: algebra_simps) + +lemma rsum_append: "rsum (D1 @ D2) f = rsum D1 f + rsum D2 f" +unfolding rsum_def map_append listsum_append .. + + +subsection {* Gauge integrability (definite) *} + +definition + Integral :: "[(real*real),real=>real,real] => bool" where + [code del]: "Integral = (%(a,b) f k. \e > 0. + (\\. gauge {a .. b} \ & + (\D. fine \ (a,b) D --> + \rsum D f - k\ < e)))" + +lemma Integral_def2: + "Integral = (%(a,b) f k. \e>0. (\\. gauge {a..b} \ & + (\D. fine \ (a,b) D --> + \rsum D f - k\ \ e)))" +unfolding Integral_def +apply (safe intro!: ext) +apply (fast intro: less_imp_le) +apply (drule_tac x="e/2" in spec) +apply force +done + +text{*The integral is unique if it exists*} + +lemma Integral_unique: + "[| a \ b; Integral(a,b) f k1; Integral(a,b) f k2 |] ==> k1 = k2" +apply (simp add: Integral_def) +apply (drule_tac x = "\k1 - k2\ /2" in spec)+ +apply auto +apply (drule gauge_min, assumption) +apply (drule_tac \ = "%x. min (\ x) (\' x)" + in fine_exists, assumption, auto) +apply (drule fine_min) +apply (drule spec)+ +apply auto +apply (subgoal_tac "\(rsum D f - k2) - (rsum D f - k1)\ < \k1 - k2\") +apply arith +apply (drule add_strict_mono, assumption) +apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] + mult_less_cancel_right) +done + +lemma Integral_zero [simp]: "Integral(a,a) f 0" +apply (auto simp add: Integral_def) +apply (rule_tac x = "%x. 1" in exI) +apply (auto dest: fine_eq simp add: gauge_def rsum_def) +done + +lemma fine_rsum_const: "fine \ (a,b) D \ rsum D (\x. c) = (c * (b - a))" +unfolding rsum_def +by (induct set: fine, auto simp add: algebra_simps) + +lemma Integral_eq_diff_bounds: "a \ b ==> Integral(a,b) (%x. 1) (b - a)" +apply (cases "a = b", simp) +apply (simp add: Integral_def, clarify) +apply (rule_tac x = "%x. b - a" in exI) +apply (rule conjI, simp add: gauge_def) +apply (clarify) +apply (subst fine_rsum_const, assumption, simp) +done + +lemma Integral_mult_const: "a \ b ==> Integral(a,b) (%x. c) (c*(b - a))" +apply (cases "a = b", simp) +apply (simp add: Integral_def, clarify) +apply (rule_tac x = "%x. b - a" in exI) +apply (rule conjI, simp add: gauge_def) +apply (clarify) +apply (subst fine_rsum_const, assumption, simp) +done + +lemma Integral_mult: + "[| a \ b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)" +apply (auto simp add: order_le_less + dest: Integral_unique [OF order_refl Integral_zero]) +apply (auto simp add: Integral_def setsum_right_distrib[symmetric] mult_assoc) +apply (case_tac "c = 0", force) +apply (drule_tac x = "e/abs c" in spec) +apply (simp add: divide_pos_pos) +apply clarify +apply (rule_tac x="\" in exI, clarify) +apply (drule_tac x="D" in spec, clarify) +apply (simp add: pos_less_divide_eq abs_mult [symmetric] + algebra_simps rsum_right_distrib) +done + +lemma Integral_add: + assumes "Integral (a, b) f x1" + assumes "Integral (b, c) f x2" + assumes "a \ b" and "b \ c" + shows "Integral (a, c) f (x1 + x2)" +proof (cases "a < b \ b < c", simp only: Integral_def split_conv, rule allI, rule impI) + fix \ :: real assume "0 < \" + hence "0 < \ / 2" by auto + + assume "a < b \ b < c" + hence "a < b" and "b < c" by auto + + from `Integral (a, b) f x1`[simplified Integral_def split_conv, + rule_format, OF `0 < \/2`] + obtain \1 where \1_gauge: "gauge {a..b} \1" + and I1: "\ D. fine \1 (a,b) D \ \ rsum D f - x1 \ < (\ / 2)" by auto + + from `Integral (b, c) f x2`[simplified Integral_def split_conv, + rule_format, OF `0 < \/2`] + obtain \2 where \2_gauge: "gauge {b..c} \2" + and I2: "\ D. fine \2 (b,c) D \ \ rsum D f - x2 \ < (\ / 2)" by auto + + def \ \ "\ x. if x < b then min (\1 x) (b - x) + else if x = b then min (\1 b) (\2 b) + else min (\2 x) (x - b)" + + have "gauge {a..c} \" + using \1_gauge \2_gauge unfolding \_def gauge_def by auto + moreover { + fix D :: "(real \ real \ real) list" + assume fine: "fine \ (a,c) D" + from fine_covers_all[OF this `a < b` `b \ c`] + obtain N where "N < length D" + and *: "\ d t e. D ! N = (d, t, e) \ d < b \ b \ e" + by auto + obtain d t e where D_eq: "D ! N = (d, t, e)" by (cases "D!N", auto) + with * have "d < b" and "b \ e" by auto + have in_D: "(d, t, e) \ set D" + using D_eq[symmetric] using `N < length D` by auto + + from mem_fine[OF fine in_D] + have "d < e" and "d \ t" and "t \ e" by auto + + have "t = b" + proof (rule ccontr) + assume "t \ b" + with mem_fine3[OF fine in_D] `b \ e` `d \ t` `t \ e` `d < b` \_def + show False by (cases "t < b") auto + qed + + let ?D1 = "take N D" + let ?D2 = "drop N D" + def D1 \ "take N D @ [(d, t, b)]" + def D2 \ "(if b = e then [] else [(b, t, e)]) @ drop (Suc N) D" + + have "D \ []" using `N < length D` by auto + from hd_drop_conv_nth[OF this `N < length D`] + have "fst (hd ?D2) = d" using `D ! N = (d, t, e)` by auto + with fine_append_split[OF _ _ append_take_drop_id[symmetric]] + have fine1: "fine \ (a,d) ?D1" and fine2: "fine \ (d,c) ?D2" + using `N < length D` fine by auto + + have "fine \1 (a,b) D1" unfolding D1_def + proof (rule fine_append) + show "fine \1 (a, d) ?D1" + proof (rule fine1[THEN fine_\_expand]) + fix x assume "a \ x" "x \ d" + hence "x \ b" using `d < b` `x \ d` by auto + thus "\ x \ \1 x" unfolding \_def by auto + qed + + have "b - d < \1 t" + using mem_fine3[OF fine in_D] \_def `b \ e` `t = b` by auto + from `d < b` `d \ t` `t = b` this + show "fine \1 (d, b) [(d, t, b)]" using fine_single by auto + qed + note rsum1 = I1[OF this] + + have drop_split: "drop N D = [D ! N] @ drop (Suc N) D" + using nth_drop'[OF `N < length D`] by simp + + have fine2: "fine \2 (e,c) (drop (Suc N) D)" + proof (cases "drop (Suc N) D = []") + case True + note * = fine2[simplified drop_split True D_eq append_Nil2] + have "e = c" using fine_single_boundaries[OF * refl] by auto + thus ?thesis unfolding True using fine_Nil by auto + next + case False + note * = fine_append_split[OF fine2 False drop_split] + from fine_single_boundaries[OF *(1)] + have "fst (hd (drop (Suc N) D)) = e" using D_eq by auto + with *(2) have "fine \ (e,c) (drop (Suc N) D)" by auto + thus ?thesis + proof (rule fine_\_expand) + fix x assume "e \ x" and "x \ c" + thus "\ x \ \2 x" using `b \ e` unfolding \_def by auto + qed + qed + + have "fine \2 (b, c) D2" + proof (cases "e = b") + case True thus ?thesis using fine2 by (simp add: D1_def D2_def) + next + case False + have "e - b < \2 b" + using mem_fine3[OF fine in_D] \_def `d < b` `t = b` by auto + with False `t = b` `b \ e` + show ?thesis using D2_def + by (auto intro!: fine_append[OF _ fine2] fine_single + simp del: append_Cons) + qed + note rsum2 = I2[OF this] + + have "rsum D f = rsum (take N D) f + rsum [D ! N] f + rsum (drop (Suc N) D) f" + using rsum_append[symmetric] nth_drop'[OF `N < length D`] by auto + also have "\ = rsum D1 f + rsum D2 f" + by (cases "b = e", auto simp add: D1_def D2_def D_eq rsum_append algebra_simps) + finally have "\rsum D f - (x1 + x2)\ < \" + using add_strict_mono[OF rsum1 rsum2] by simp + } + ultimately show "\ \. gauge {a .. c} \ \ + (\D. fine \ (a,c) D \ \rsum D f - (x1 + x2)\ < \)" + by blast +next + case False + hence "a = b \ b = c" using `a \ b` and `b \ c` by auto + thus ?thesis + proof (rule disjE) + assume "a = b" hence "x1 = 0" + using `Integral (a, b) f x1` Integral_zero Integral_unique[of a b] by auto + thus ?thesis using `a = b` `Integral (b, c) f x2` by auto + next + assume "b = c" hence "x2 = 0" + using `Integral (b, c) f x2` Integral_zero Integral_unique[of b c] by auto + thus ?thesis using `b = c` `Integral (a, b) f x1` by auto + qed +qed + +text{*Fundamental theorem of calculus (Part I)*} + +text{*"Straddle Lemma" : Swartz and Thompson: AMM 95(7) 1988 *} + +lemma strad1: + "\\z::real. z \ x \ \z - x\ < s \ + \(f z - f x) / (z - x) - f' x\ < e/2; + 0 < s; 0 < e; a \ x; x \ b\ + \ \z. \z - x\ < s -->\f z - f x - f' x * (z - x)\ \ e/2 * \z - x\" +apply clarify +apply (case_tac "z = x", simp) +apply (drule_tac x = z in spec) +apply (rule_tac z1 = "\inverse (z - x)\" + in real_mult_le_cancel_iff2 [THEN iffD1]) + apply simp +apply (simp del: abs_inverse abs_mult add: abs_mult [symmetric] + mult_assoc [symmetric]) +apply (subgoal_tac "inverse (z - x) * (f z - f x - f' x * (z - x)) + = (f z - f x) / (z - x) - f' x") + apply (simp add: abs_mult [symmetric] mult_ac diff_minus) +apply (subst mult_commute) +apply (simp add: left_distrib diff_minus) +apply (simp add: mult_assoc divide_inverse) +apply (simp add: left_distrib) +done + +lemma lemma_straddle: + assumes f': "\x. a \ x & x \ b --> DERIV f x :> f'(x)" and "0 < e" + shows "\g. gauge {a..b} g & + (\x u v. a \ u & u \ x & x \ v & v \ b & (v - u) < g(x) + --> \(f(v) - f(u)) - (f'(x) * (v - u))\ \ e * (v - u))" +proof - + have "\x\{a..b}. + (\d > 0. \u v. u \ x & x \ v & (v - u) < d --> + \(f(v) - f(u)) - (f'(x) * (v - u))\ \ e * (v - u))" + proof (clarsimp) + fix x :: real assume "a \ x" and "x \ b" + with f' have "DERIV f x :> f'(x)" by simp + then have "\r>0. \s>0. \z. z \ x \ \z - x\ < s \ \(f z - f x) / (z - x) - f' x\ < r" + by (simp add: DERIV_iff2 LIM_eq) + with `0 < e` obtain s + where "\z. z \ x \ \z - x\ < s \ \(f z - f x) / (z - x) - f' x\ < e/2" and "0 < s" + by (drule_tac x="e/2" in spec, auto) + then have strad [rule_format]: + "\z. \z - x\ < s --> \f z - f x - f' x * (z - x)\ \ e/2 * \z - x\" + using `0 < e` `a \ x` `x \ b` by (rule strad1) + show "\d>0. \u v. u \ x \ x \ v \ v - u < d \ \f v - f u - f' x * (v - u)\ \ e * (v - u)" + proof (safe intro!: exI) + show "0 < s" by fact + next + fix u v :: real assume "u \ x" and "x \ v" and "v - u < s" + have "\f v - f u - f' x * (v - u)\ = + \(f v - f x - f' x * (v - x)) + (f x - f u - f' x * (x - u))\" + by (simp add: right_diff_distrib) + also have "\ \ \f v - f x - f' x * (v - x)\ + \f x - f u - f' x * (x - u)\" + by (rule abs_triangle_ineq) + also have "\ = \f v - f x - f' x * (v - x)\ + \f u - f x - f' x * (u - x)\" + by (simp add: right_diff_distrib) + also have "\ \ (e/2) * \v - x\ + (e/2) * \u - x\" + using `u \ x` `x \ v` `v - u < s` by (intro add_mono strad, simp_all) + also have "\ \ e * (v - u) / 2 + e * (v - u) / 2" + using `u \ x` `x \ v` `0 < e` by (intro add_mono, simp_all) + also have "\ = e * (v - u)" + by simp + finally show "\f v - f u - f' x * (v - u)\ \ e * (v - u)" . + qed + qed + thus ?thesis + by (simp add: gauge_def) (drule bchoice, auto) +qed + +lemma fundamental_theorem_of_calculus: + "\ a \ b; \x. a \ x & x \ b --> DERIV f x :> f'(x) \ + \ Integral(a,b) f' (f(b) - f(a))" + apply (drule order_le_imp_less_or_eq, auto) + apply (auto simp add: Integral_def2) + apply (drule_tac e = "e / (b - a)" in lemma_straddle) + apply (simp add: divide_pos_pos) + apply clarify + apply (rule_tac x="g" in exI, clarify) + apply (clarsimp simp add: rsum_def) + apply (frule fine_listsum_eq_diff [where f=f]) + apply (erule subst) + apply (subst listsum_subtractf [symmetric]) + apply (rule listsum_abs [THEN order_trans]) + apply (subst map_map [unfolded o_def]) + apply (subgoal_tac "e = (\(u, x, v)\D. (e / (b - a)) * (v - u))") + apply (erule ssubst) + apply (simp add: abs_minus_commute) + apply (rule listsum_mono) + apply (clarify, rename_tac u x v) + apply ((drule spec)+, erule mp) + apply (simp add: mem_fine mem_fine2 mem_fine3) + apply (frule fine_listsum_eq_diff [where f="\x. x"]) + apply (simp only: split_def) + apply (subst listsum_const_mult) + apply simp +done + +end diff -r c76b7dcd77ce -r cac5a37fb638 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Tue Feb 23 16:58:21 2010 +0100 +++ b/src/HOL/ex/ROOT.ML Tue Feb 23 17:55:00 2010 +0100 @@ -67,7 +67,8 @@ "Quickcheck_Examples", "Landau", "Execute_Choice", - "Summation" + "Summation", + "Gauge_Integration" ]; HTML.with_charset "utf-8" (no_document use_thys)