diff -r 0df9c8a37f64 -r ae742caa0c5b src/HOL/ex/Gauge_Integration.thy
--- a/src/HOL/ex/Gauge_Integration.thy	Wed Feb 24 07:06:39 2010 -0800
+++ b/src/HOL/ex/Gauge_Integration.thy	Wed Feb 24 10:36:17 2010 -0800
@@ -28,7 +28,7 @@
 
 definition
   gauge :: "[real set, real => real] => bool" where
-  [code del]:"gauge E g = (\<forall>x\<in>E. 0 < g(x))"
+  [code del]: "gauge E g = (\<forall>x\<in>E. 0 < g(x))"
 
 
 subsection {* Gauge-fine divisions *}
@@ -63,14 +63,20 @@
 apply (drule fine_imp_le, simp)
 done
 
-lemma empty_fine_imp_eq: "\<lbrakk>fine \<delta> (a, b) D; D = []\<rbrakk> \<Longrightarrow> a = b"
-by (induct set: fine, simp_all)
+lemma fine_Nil_iff: "fine \<delta> (a, b) [] \<longleftrightarrow> a = b"
+by (auto elim: fine.cases intro: fine.intros)
 
-lemma fine_eq: "fine \<delta> (a, b) D \<Longrightarrow> a = b \<longleftrightarrow> D = []"
-apply (cases "D = []")
-apply (drule (1) empty_fine_imp_eq, simp)
-apply (drule (1) nonempty_fine_imp_less, simp)
-done
+lemma fine_same_iff: "fine \<delta> (a, a) D \<longleftrightarrow> D = []"
+proof
+  assume "fine \<delta> (a, a) D" thus "D = []"
+    by (metis nonempty_fine_imp_less less_irrefl)
+next
+  assume "D = []" thus "fine \<delta> (a, a) D"
+    by (simp add: fine_Nil)
+qed
+
+lemma empty_fine_imp_eq: "\<lbrakk>fine \<delta> (a, b) D; D = []\<rbrakk> \<Longrightarrow> a = b"
+by (simp add: fine_Nil_iff)
 
 lemma mem_fine:
   "\<lbrakk>fine \<delta> (a, b) D; (u, x, v) \<in> set D\<rbrakk> \<Longrightarrow> u < v \<and> u \<le> x \<and> x \<le> v"
@@ -174,7 +180,7 @@
 
 lemma fine_\<delta>_expand:
   assumes "fine \<delta> (a,b) D"
-  and "\<And> x. \<lbrakk> a \<le> x ; x \<le> b \<rbrakk> \<Longrightarrow> \<delta> x \<le> \<delta>' x"
+  and "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> \<delta> x \<le> \<delta>' x"
   shows "fine \<delta>' (a,b) D"
 using assms proof induct
   case 1 show ?case by (rule fine_Nil)
@@ -258,6 +264,22 @@
                                (\<forall>D. fine \<delta> (a,b) D -->
                                          \<bar>rsum D f - k\<bar> < e)))"
 
+lemma Integral_eq:
+  "Integral (a, b) f k \<longleftrightarrow>
+    (\<forall>e>0. \<exists>\<delta>. gauge {a..b} \<delta> \<and> (\<forall>D. fine \<delta> (a,b) D \<longrightarrow> \<bar>rsum D f - k\<bar> < e))"
+unfolding Integral_def by simp
+
+lemma IntegralI:
+  assumes "\<And>e. 0 < e \<Longrightarrow>
+    \<exists>\<delta>. gauge {a..b} \<delta> \<and> (\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f - k\<bar> < e)"
+  shows "Integral (a, b) f k"
+using assms unfolding Integral_def by auto
+
+lemma IntegralE:
+  assumes "Integral (a, b) f k" and "0 < e"
+  obtains \<delta> where "gauge {a..b} \<delta>" and "\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f - k\<bar> < e"
+using assms unfolding Integral_def by auto
+
 lemma Integral_def2:
   "Integral = (%(a,b) f k. \<forall>e>0. (\<exists>\<delta>. gauge {a..b} \<delta> &
                                (\<forall>D. fine \<delta> (a,b) D -->
@@ -272,60 +294,69 @@
 text{*The integral is unique if it exists*}
 
 lemma Integral_unique:
-    "[| a \<le> b; Integral(a,b) f k1; Integral(a,b) f k2 |] ==> k1 = k2"
-apply (simp add: Integral_def)
-apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec)+
-apply auto
-apply (drule gauge_min, assumption)
-apply (drule_tac \<delta> = "%x. min (\<delta> x) (\<delta>' x)"
-       in fine_exists, assumption, auto)
-apply (drule fine_min)
-apply (drule spec)+
-apply auto
-apply (subgoal_tac "\<bar>(rsum D f - k2) - (rsum D f - k1)\<bar> < \<bar>k1 - k2\<bar>")
-apply arith
-apply (drule add_strict_mono, assumption)
-apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] 
-                mult_less_cancel_right)
+  assumes le: "a \<le> b"
+  assumes 1: "Integral (a, b) f k1"
+  assumes 2: "Integral (a, b) f k2"
+  shows "k1 = k2"
+proof (rule ccontr)
+  assume "k1 \<noteq> k2"
+  hence e: "0 < \<bar>k1 - k2\<bar> / 2" by simp
+  obtain d1 where "gauge {a..b} d1" and
+    d1: "\<forall>D. fine d1 (a, b) D \<longrightarrow> \<bar>rsum D f - k1\<bar> < \<bar>k1 - k2\<bar> / 2"
+    using 1 e by (rule IntegralE)
+  obtain d2 where "gauge {a..b} d2" and
+    d2: "\<forall>D. fine d2 (a, b) D \<longrightarrow> \<bar>rsum D f - k2\<bar> < \<bar>k1 - k2\<bar> / 2"
+    using 2 e by (rule IntegralE)
+  have "gauge {a..b} (\<lambda>x. min (d1 x) (d2 x))"
+    using `gauge {a..b} d1` and `gauge {a..b} d2`
+    by (rule gauge_min)
+  then obtain D where "fine (\<lambda>x. min (d1 x) (d2 x)) (a, b) D"
+    using fine_exists [OF le] by fast
+  hence "fine d1 (a, b) D" and "fine d2 (a, b) D"
+    by (auto dest: fine_min)
+  hence "\<bar>rsum D f - k1\<bar> < \<bar>k1 - k2\<bar> / 2" and "\<bar>rsum D f - k2\<bar> < \<bar>k1 - k2\<bar> / 2"
+    using d1 d2 by simp_all
+  hence "\<bar>rsum D f - k1\<bar> + \<bar>rsum D f - k2\<bar> < \<bar>k1 - k2\<bar> / 2 + \<bar>k1 - k2\<bar> / 2"
+    by (rule add_strict_mono)
+  thus False by auto
+qed
+
+lemma Integral_zero: "Integral(a,a) f 0"
+apply (rule IntegralI)
+apply (rule_tac x = "\<lambda>x. 1" in exI)
+apply (simp add: fine_same_iff gauge_def)
 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)
+lemma Integral_same_iff [simp]: "Integral (a, a) f k \<longleftrightarrow> k = 0"
+  by (auto intro: Integral_zero Integral_unique)
+
+lemma Integral_zero_fun: "Integral (a,b) (\<lambda>x. 0) 0"
+apply (rule IntegralI)
+apply (rule_tac x="\<lambda>x. 1" in exI, simp add: gauge_def)
 done
 
 lemma fine_rsum_const: "fine \<delta> (a,b) D \<Longrightarrow> rsum D (\<lambda>x. c) = (c * (b - a))"
 unfolding rsum_def
 by (induct set: fine, auto simp add: algebra_simps)
 
-lemma Integral_eq_diff_bounds: "a \<le> b ==> Integral(a,b) (%x. 1) (b - a)"
+lemma Integral_mult_const: "a \<le> b \<Longrightarrow> Integral(a,b) (\<lambda>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 IntegralI)
+apply (rule_tac x = "\<lambda>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 \<le> 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_eq_diff_bounds: "a \<le> b \<Longrightarrow> Integral(a,b) (\<lambda>x. 1) (b - a)"
+  using Integral_mult_const [of a b 1] by simp
 
 lemma Integral_mult:
      "[| a \<le> 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 (auto simp add: order_le_less)
+apply (cases "c = 0", simp add: Integral_zero_fun)
+apply (rule IntegralI)
+apply (erule_tac e="e / \<bar>c\<bar>" in IntegralE, simp add: divide_pos_pos)
 apply (rule_tac x="\<delta>" in exI, clarify)
 apply (drule_tac x="D" in spec, clarify)
 apply (simp add: pos_less_divide_eq abs_mult [symmetric]
@@ -337,22 +368,20 @@
   assumes "Integral (b, c) f x2"
   assumes "a \<le> b" and "b \<le> c"
   shows "Integral (a, c) f (x1 + x2)"
-proof (cases "a < b \<and> b < c", simp only: Integral_def split_conv, rule allI, rule impI)
+proof (cases "a < b \<and> b < c", rule IntegralI)
   fix \<epsilon> :: real assume "0 < \<epsilon>"
   hence "0 < \<epsilon> / 2" by auto
 
   assume "a < b \<and> 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 < \<epsilon>/2`]
   obtain \<delta>1 where \<delta>1_gauge: "gauge {a..b} \<delta>1"
-    and I1: "\<And> D. fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f - x1 \<bar> < (\<epsilon> / 2)" by auto
+    and I1: "\<And> D. fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f - x1 \<bar> < (\<epsilon> / 2)"
+    using IntegralE [OF `Integral (a, b) f x1` `0 < \<epsilon>/2`] by auto
 
-  from `Integral (b, c) f x2`[simplified Integral_def split_conv,
-                              rule_format, OF `0 < \<epsilon>/2`]
   obtain \<delta>2 where \<delta>2_gauge: "gauge {b..c} \<delta>2"
-    and I2: "\<And> D. fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)" by auto
+    and I2: "\<And> D. fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)"
+    using IntegralE [OF `Integral (b, c) f x2` `0 < \<epsilon>/2`] by auto
 
   def \<delta> \<equiv> "\<lambda> x. if x < b then min (\<delta>1 x) (b - x)
            else if x = b then min (\<delta>1 b) (\<delta>2 b)
@@ -360,6 +389,7 @@
 
   have "gauge {a..c} \<delta>"
     using \<delta>1_gauge \<delta>2_gauge unfolding \<delta>_def gauge_def by auto
+
   moreover {
     fix D :: "(real \<times> real \<times> real) list"
     assume fine: "fine \<delta> (a,c) D"
@@ -462,12 +492,12 @@
   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
+      using `Integral (a, b) f x1` by simp
+    thus ?thesis using `a = b` `Integral (b, c) f x2` by simp
   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
+      using `Integral (b, c) f x2` by simp
+    thus ?thesis using `b = c` `Integral (a, b) f x1` by simp
   qed
 qed
 
@@ -486,7 +516,7 @@
 apply (rule_tac z1 = "\<bar>inverse (z - x)\<bar>" 
        in real_mult_le_cancel_iff2 [THEN iffD1])
  apply simp
-apply (simp del: abs_inverse abs_mult add: abs_mult [symmetric]
+apply (simp del: abs_inverse 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")
@@ -543,31 +573,51 @@
 qed
 
 lemma fundamental_theorem_of_calculus:
-  "\<lbrakk> a \<le> b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) \<rbrakk>
-             \<Longrightarrow> 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 = (\<Sum>(u, x, v)\<leftarrow>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="\<lambda>x. x"])
- apply (simp only: split_def)
- apply (subst listsum_const_mult)
- apply simp
-done
+  assumes "a \<le> b"
+  assumes f': "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> DERIV f x :> f'(x)"
+  shows "Integral (a, b) f' (f(b) - f(a))"
+proof (cases "a = b")
+  assume "a = b" thus ?thesis by simp
+next
+  assume "a \<noteq> b" with `a \<le> b` have "a < b" by simp
+  show ?thesis
+  proof (simp add: Integral_def2, clarify)
+    fix e :: real assume "0 < e"
+    with `a < b` have "0 < e / (b - a)" by (simp add: divide_pos_pos)
+
+    from lemma_straddle [OF f' this]
+    obtain \<delta> where "gauge {a..b} \<delta>"
+      and \<delta>: "\<And>x u v. \<lbrakk>a \<le> u; u \<le> x; x \<le> v; v \<le> b; v - u < \<delta> x\<rbrakk> \<Longrightarrow>
+           \<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u) / (b - a)" by auto
+
+    have "\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f' - (f b - f a)\<bar> \<le> e"
+    proof (clarify)
+      fix D assume D: "fine \<delta> (a, b) D"
+      hence "(\<Sum>(u, x, v)\<leftarrow>D. f v - f u) = f b - f a"
+        by (rule fine_listsum_eq_diff)
+      hence "\<bar>rsum D f' - (f b - f a)\<bar> = \<bar>rsum D f' - (\<Sum>(u, x, v)\<leftarrow>D. f v - f u)\<bar>"
+        by simp
+      also have "\<dots> = \<bar>(\<Sum>(u, x, v)\<leftarrow>D. f v - f u) - rsum D f'\<bar>"
+        by (rule abs_minus_commute)
+      also have "\<dots> = \<bar>\<Sum>(u, x, v)\<leftarrow>D. (f v - f u) - f' x * (v - u)\<bar>"
+        by (simp only: rsum_def listsum_subtractf split_def)
+      also have "\<dots> \<le> (\<Sum>(u, x, v)\<leftarrow>D. \<bar>(f v - f u) - f' x * (v - u)\<bar>)"
+        by (rule ord_le_eq_trans [OF listsum_abs], simp add: o_def split_def)
+      also have "\<dots> \<le> (\<Sum>(u, x, v)\<leftarrow>D. (e / (b - a)) * (v - u))"
+        apply (rule listsum_mono, clarify, rename_tac u x v)
+        using D apply (simp add: \<delta> mem_fine mem_fine2 mem_fine3)
+        done
+      also have "\<dots> = e"
+        using fine_listsum_eq_diff [OF D, where f="\<lambda>x. x"]
+        unfolding split_def listsum_const_mult
+        using `a < b` by simp
+      finally show "\<bar>rsum D f' - (f b - f a)\<bar> \<le> e" .
+    qed
+
+    with `gauge {a..b} \<delta>`
+    show "\<exists>\<delta>. gauge {a..b} \<delta> \<and> (\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f' - (f b - f a)\<bar> \<le> e)"
+      by auto
+  qed
+qed
 
 end