# HG changeset patch
# User wenzelm
# Date 1378849803 -7200
# Node ID 706f7edea3d402abe8725535499b84898df84f1f
# Parent  c5d2ef007d81d23280ac149eca245f7d597cc760
tuned proofs;

diff -r c5d2ef007d81 -r 706f7edea3d4 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Sep 10 23:08:48 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Sep 10 23:50:03 2013 +0200
@@ -7551,278 +7551,658 @@
 qed simp
 
 lemma interval_image_stretch_interval:
-    "\<exists>u v. (\<lambda>x. \<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k) ` {a..b::'a::ordered_euclidean_space} = {u..v::'a}"
+  "\<exists>u v. (\<lambda>x. \<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k) ` {a..b::'a::ordered_euclidean_space} = {u..v::'a}"
   unfolding image_stretch_interval by auto
 
 lemma content_image_stretch_interval:
-  "content((\<lambda>x::'a::ordered_euclidean_space. (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)::'a) ` {a..b}) = abs(setprod m Basis) * content({a..b})"
-proof(cases "{a..b} = {}") case True thus ?thesis
+  "content ((\<lambda>x::'a::ordered_euclidean_space. (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)::'a) ` {a..b}) =
+    abs (setprod m Basis) * content {a..b}"
+proof (cases "{a..b} = {}")
+  case True
+  then show ?thesis
     unfolding content_def image_is_empty image_stretch_interval if_P[OF True] by auto
-next case False hence "(\<lambda>x. (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)::'a) ` {a..b} \<noteq> {}" by auto
-  thus ?thesis using False unfolding content_def image_stretch_interval apply- unfolding interval_bounds' if_not_P
-    unfolding abs_setprod setprod_timesf[symmetric] apply(rule setprod_cong2) unfolding lessThan_iff
-  proof (simp only: inner_setsum_left_Basis)
-    fix i :: 'a assume i:"i\<in>Basis" have "(m i < 0 \<or> m i > 0) \<or> m i = 0" by auto
-    thus "max (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) - min (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) =
-        \<bar>m i\<bar> * (b \<bullet> i - a \<bullet> i)"
-      apply-apply(erule disjE)+ unfolding min_def max_def using False[unfolded interval_ne_empty,rule_format,of i] i
-      by(auto simp add:field_simps not_le mult_le_cancel_left_neg mult_le_cancel_left_pos) qed qed
-
-lemma has_integral_stretch: fixes f::"'a::ordered_euclidean_space => 'b::real_normed_vector"
-  assumes "(f has_integral i) {a..b}" "\<forall>k\<in>Basis. ~(m k = 0)"
+next
+  case False
+  then have "(\<lambda>x. (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) ` {a..b} \<noteq> {}"
+    by auto
+  then show ?thesis
+    using False
+    unfolding content_def image_stretch_interval
+    apply -
+    unfolding interval_bounds' if_not_P
+    unfolding abs_setprod setprod_timesf[symmetric]
+    apply (rule setprod_cong2)
+    unfolding lessThan_iff
+    apply (simp only: inner_setsum_left_Basis)
+  proof -
+    fix i :: 'a
+    assume i: "i \<in> Basis"
+    have "(m i < 0 \<or> m i > 0) \<or> m i = 0"
+      by auto
+    then show "max (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) - min (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) =
+      \<bar>m i\<bar> * (b \<bullet> i - a \<bullet> i)"
+      apply -
+      apply (erule disjE)+
+      unfolding min_def max_def
+      using False[unfolded interval_ne_empty,rule_format,of i] i
+      apply (auto simp add:field_simps not_le mult_le_cancel_left_neg mult_le_cancel_left_pos)
+      done
+  qed
+qed
+
+lemma has_integral_stretch:
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
+  assumes "(f has_integral i) {a..b}"
+    and "\<forall>k\<in>Basis. m k \<noteq> 0"
   shows "((\<lambda>x. f (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) has_integral
-             ((1/(abs(setprod m Basis))) *\<^sub>R i)) ((\<lambda>x. (\<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k)) ` {a..b})"
-  apply(rule has_integral_twiddle[where f=f]) unfolding zero_less_abs_iff content_image_stretch_interval
-  unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a] using assms
-proof- show "\<forall>y::'a. continuous (at y) (\<lambda>x. (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k))"
-   apply(rule,rule linear_continuous_at) unfolding linear_linear
-   unfolding linear_def inner_simps euclidean_eq_iff[where 'a='a] by(auto simp add:field_simps)
+    ((1/(abs(setprod m Basis))) *\<^sub>R i)) ((\<lambda>x. (\<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k)) ` {a..b})"
+  apply (rule has_integral_twiddle[where f=f])
+  unfolding zero_less_abs_iff content_image_stretch_interval
+  unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a]
+  using assms
+proof -
+  show "\<forall>y::'a. continuous (at y) (\<lambda>x. (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k))"
+    apply rule
+    apply (rule linear_continuous_at)
+    unfolding linear_linear
+    unfolding linear_def inner_simps euclidean_eq_iff[where 'a='a]
+    apply (auto simp add: field_simps)
+    done
 qed auto
 
-lemma integrable_stretch:  fixes f::"'a::ordered_euclidean_space => 'b::real_normed_vector"
-  assumes "f integrable_on {a..b}" "\<forall>k\<in>Basis. ~(m k = 0)"
-  shows "(\<lambda>x::'a. f (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) integrable_on ((\<lambda>x. \<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k) ` {a..b})"
-  using assms unfolding integrable_on_def apply-apply(erule exE)
-  apply(drule has_integral_stretch,assumption) by auto
+lemma integrable_stretch:
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
+  assumes "f integrable_on {a..b}"
+    and "\<forall>k\<in>Basis. m k \<noteq> 0"
+  shows "(\<lambda>x::'a. f (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) integrable_on
+    ((\<lambda>x. \<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k) ` {a..b})"
+  using assms
+  unfolding integrable_on_def
+  apply -
+  apply (erule exE)
+  apply (drule has_integral_stretch)
+  apply assumption
+  apply auto
+  done
+
 
 subsection {* even more special cases. *}
 
-lemma uminus_interval_vector[simp]:"uminus ` {a..b} = {-b .. -a::'a::ordered_euclidean_space}"
-  apply(rule set_eqI,rule) defer unfolding image_iff
-  apply(rule_tac x="-x" in bexI) by(auto simp add:minus_le_iff le_minus_iff eucl_le[where 'a='a])
-
-lemma has_integral_reflect_lemma[intro]: assumes "(f has_integral i) {a..b}"
-  shows "((\<lambda>x. f(-x)) has_integral i) {-b .. -a}"
-  using has_integral_affinity[OF assms, of "-1" 0] by auto
-
-lemma has_integral_reflect[simp]: "((\<lambda>x. f(-x)) has_integral i) {-b..-a} \<longleftrightarrow> (f has_integral i) ({a..b})"
-  apply rule apply(drule_tac[!] has_integral_reflect_lemma) by auto
+lemma uminus_interval_vector[simp]:
+  fixes a b :: "'a::ordered_euclidean_space"
+  shows "uminus ` {a..b} = {-b..-a}"
+  apply (rule set_eqI)
+  apply rule
+  defer
+  unfolding image_iff
+  apply (rule_tac x="-x" in bexI)
+  apply (auto simp add:minus_le_iff le_minus_iff eucl_le[where 'a='a])
+  done
+
+lemma has_integral_reflect_lemma[intro]:
+  assumes "(f has_integral i) {a..b}"
+  shows "((\<lambda>x. f(-x)) has_integral i) {-b..-a}"
+  using has_integral_affinity[OF assms, of "-1" 0]
+  by auto
+
+lemma has_integral_reflect[simp]:
+  "((\<lambda>x. f (-x)) has_integral i) {-b..-a} \<longleftrightarrow> (f has_integral i) {a..b}"
+  apply rule
+  apply (drule_tac[!] has_integral_reflect_lemma)
+  apply auto
+  done
 
 lemma integrable_reflect[simp]: "(\<lambda>x. f(-x)) integrable_on {-b..-a} \<longleftrightarrow> f integrable_on {a..b}"
   unfolding integrable_on_def by auto
 
-lemma integral_reflect[simp]: "integral {-b..-a} (\<lambda>x. f(-x)) = integral ({a..b}) f"
+lemma integral_reflect[simp]: "integral {-b..-a} (\<lambda>x. f (-x)) = integral {a..b} f"
   unfolding integral_def by auto
 
+
 subsection {* Stronger form of FCT; quite a tedious proof. *}
 
-lemma bgauge_existence_lemma: "(\<forall>x\<in>s. \<exists>d::real. 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. x\<in>s \<longrightarrow> q d x)" by(meson zero_less_one)
-
-lemma additive_tagged_division_1': fixes f::"real \<Rightarrow> 'a::real_normed_vector"
-  assumes "a \<le> b" "p tagged_division_of {a..b}"
+lemma bgauge_existence_lemma: "(\<forall>x\<in>s. \<exists>d::real. 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. x\<in>s \<longrightarrow> q d x)"
+  by (meson zero_less_one)
+
+lemma additive_tagged_division_1':
+  fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
+  assumes "a \<le> b"
+    and "p tagged_division_of {a..b}"
   shows "setsum (\<lambda>(x,k). f (interval_upperbound k) - f(interval_lowerbound k)) p = f b - f a"
-  using additive_tagged_division_1[OF _ assms(2), of f] using assms(1) by auto
-
-lemma split_minus[simp]:"(\<lambda>(x, k). f x k) x - (\<lambda>(x, k). g x k) x = (\<lambda>(x, k). f x k - g x k) x"
-  unfolding split_def by(rule refl)
+  using additive_tagged_division_1[OF _ assms(2), of f]
+  using assms(1)
+  by auto
+
+lemma split_minus[simp]: "(\<lambda>(x, k). f x k) x - (\<lambda>(x, k). g x k) x = (\<lambda>(x, k). f x k - g x k) x"
+  by (simp add: split_def)
 
 lemma norm_triangle_le_sub: "norm x + norm y \<le> e \<Longrightarrow> norm (x - y) \<le> e"
-  apply(subst(asm)(2) norm_minus_cancel[symmetric])
-  apply(drule norm_triangle_le) by(auto simp add:algebra_simps)
-
-lemma fundamental_theorem_of_calculus_interior: fixes f::"real => 'a::real_normed_vector"
-  assumes"a \<le> b" "continuous_on {a..b} f" "\<forall>x\<in>{a<..<b}. (f has_vector_derivative f'(x)) (at x)"
+  apply (subst(asm)(2) norm_minus_cancel[symmetric])
+  apply (drule norm_triangle_le)
+  apply (auto simp add: algebra_simps)
+  done
+
+lemma fundamental_theorem_of_calculus_interior:
+  fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
+  assumes "a \<le> b"
+    and "continuous_on {a..b} f"
+    and "\<forall>x\<in>{a<..<b}. (f has_vector_derivative f'(x)) (at x)"
   shows "(f' has_integral (f b - f a)) {a..b}"
-proof- { presume *:"a < b \<Longrightarrow> ?thesis"
-    show ?thesis proof(cases,rule *,assumption)
-      assume "\<not> a < b" hence "a = b" using assms(1) by auto
-      hence *:"{a .. b} = {b}" "f b - f a = 0" by(auto simp add:  order_antisym)
-      show ?thesis unfolding *(2) apply(rule has_integral_null) unfolding content_eq_0 using * `a=b`
+proof -
+  {
+    presume *: "a < b \<Longrightarrow> ?thesis"
+    show ?thesis
+    proof (cases "a < b")
+      case True
+      then show ?thesis by (rule *)
+    next
+      case False
+      then have "a = b"
+        using assms(1) by auto
+      then have *: "{a .. b} = {b}" "f b - f a = 0"
+        by (auto simp add:  order_antisym)
+      show ?thesis
+        unfolding *(2)
+        apply (rule has_integral_null)
+        unfolding content_eq_0
+        using * `a = b`
         by (auto simp: ex_in_conv)
-    qed } assume ab:"a < b"
+    qed
+  }
+  assume ab: "a < b"
   let ?P = "\<lambda>e. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow>
-                   norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content {a..b})"
-  { presume "\<And>e. e>0 \<Longrightarrow> ?P e" thus ?thesis unfolding has_integral_factor_content by auto }
-  fix e::real assume e:"e>0"
+    norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content {a..b})"
+  { presume "\<And>e. e > 0 \<Longrightarrow> ?P e" then show ?thesis unfolding has_integral_factor_content by auto }
+  fix e :: real
+  assume e: "e > 0"
   note assms(3)[unfolded has_vector_derivative_def has_derivative_at_alt ball_conj_distrib]
-  note conjunctD2[OF this] note bounded=this(1) and this(2)
-  from this(2) have "\<forall>x\<in>{a<..<b}. \<exists>d>0. \<forall>y. norm (y - x) < d \<longrightarrow> norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e/2 * norm (y - x)"
-    apply-apply safe apply(erule_tac x=x in ballE,erule_tac x="e/2" in allE) using e by auto note this[unfolded bgauge_existence_lemma]
-  from choice[OF this] guess d .. note conjunctD2[OF this[rule_format]] note d = this[rule_format]
-  have "bounded (f ` {a..b})" apply(rule compact_imp_bounded compact_continuous_image)+ using compact_interval assms by auto
+  note conjunctD2[OF this]
+  note bounded=this(1) and this(2)
+  from this(2) have "\<forall>x\<in>{a<..<b}. \<exists>d>0. \<forall>y. norm (y - x) < d \<longrightarrow>
+    norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e/2 * norm (y - x)"
+    apply -
+    apply safe
+    apply (erule_tac x=x in ballE)
+    apply (erule_tac x="e/2" in allE)
+    using e
+    apply auto
+    done
+  note this[unfolded bgauge_existence_lemma]
+  from choice[OF this] guess d ..
+  note conjunctD2[OF this[rule_format]]
+  note d = this[rule_format]
+  have "bounded (f ` {a..b})"
+    apply (rule compact_imp_bounded compact_continuous_image)+
+    using compact_interval assms
+    apply auto
+    done
   from this[unfolded bounded_pos] guess B .. note B = this[rule_format]
 
-  have "\<exists>da. 0 < da \<and> (\<forall>c. a \<le> c \<and> {a..c} \<subseteq> {a..b} \<and> {a..c} \<subseteq> ball a da
-    \<longrightarrow> norm(content {a..c} *\<^sub>R f' a - (f c - f a)) \<le> (e * (b - a)) / 4)"
-  proof- have "a\<in>{a..b}" using ab by auto
+  have "\<exists>da. 0 < da \<and> (\<forall>c. a \<le> c \<and> {a..c} \<subseteq> {a..b} \<and> {a..c} \<subseteq> ball a da \<longrightarrow>
+    norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \<le> (e * (b - a)) / 4)"
+  proof -
+    have "a \<in> {a..b}"
+      using ab by auto
     note assms(2)[unfolded continuous_on_eq_continuous_within,rule_format,OF this]
-    note * = this[unfolded continuous_within Lim_within,rule_format] have "(e * (b - a)) / 8 > 0" using e ab by(auto simp add:field_simps)
+    note * = this[unfolded continuous_within Lim_within,rule_format]
+    have "(e * (b - a)) / 8 > 0"
+      using e ab by (auto simp add: field_simps)
     from *[OF this] guess k .. note k = conjunctD2[OF this,rule_format]
     have "\<exists>l. 0 < l \<and> norm(l *\<^sub>R f' a) \<le> (e * (b - a)) / 8"
-    proof(cases "f' a = 0") case True
-      thus ?thesis apply(rule_tac x=1 in exI) using ab e by(auto intro!:mult_nonneg_nonneg)
-    next case False thus ?thesis
-        apply(rule_tac x="(e * (b - a)) / 8 / norm (f' a)" in exI) using ab e by(auto simp add:field_simps)
-    qed then guess l .. note l = conjunctD2[OF this]
-    show ?thesis apply(rule_tac x="min k l" in exI) apply safe unfolding min_less_iff_conj apply(rule,(rule l k)+)
-    proof- fix c assume as:"a \<le> c" "{a..c} \<subseteq> {a..b}" "{a..c} \<subseteq> ball a (min k l)"
+    proof (cases "f' a = 0")
+      case True
+      then show ?thesis
+        apply (rule_tac x=1 in exI)
+        using ab e
+        apply (auto intro!:mult_nonneg_nonneg)
+        done
+    next
+      case False
+      then show ?thesis
+        apply (rule_tac x="(e * (b - a)) / 8 / norm (f' a)" in exI)
+        using ab e
+        apply (auto simp add: field_simps)
+        done
+    qed
+    then guess l .. note l = conjunctD2[OF this]
+    show ?thesis
+      apply (rule_tac x="min k l" in exI)
+      apply safe
+      unfolding min_less_iff_conj
+      apply rule
+      apply (rule l k)+
+    proof -
+      fix c
+      assume as: "a \<le> c" "{a..c} \<subseteq> {a..b}" "{a..c} \<subseteq> ball a (min k l)"
       note as' = this[unfolded subset_eq Ball_def mem_ball dist_real_def mem_interval]
-      have "norm ((c - a) *\<^sub>R f' a - (f c - f a)) \<le> norm ((c - a) *\<^sub>R f' a) + norm (f c - f a)" by(rule norm_triangle_ineq4)
-      also have "... \<le> e * (b - a) / 8 + e * (b - a) / 8"
-      proof(rule add_mono) case goal1 have "\<bar>c - a\<bar> \<le> \<bar>l\<bar>" using as' by auto
-        thus ?case apply-apply(rule order_trans[OF _ l(2)]) unfolding norm_scaleR apply(rule mult_right_mono) by auto
-      next case goal2 show ?case apply(rule less_imp_le) apply(cases "a = c") defer
-          apply(rule k(2)[unfolded dist_norm]) using as' e ab by(auto simp add:field_simps)
-      qed finally show "norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \<le> e * (b - a) / 4"
+      have "norm ((c - a) *\<^sub>R f' a - (f c - f a)) \<le> norm ((c - a) *\<^sub>R f' a) + norm (f c - f a)"
+        by (rule norm_triangle_ineq4)
+      also have "\<dots> \<le> e * (b - a) / 8 + e * (b - a) / 8"
+      proof (rule add_mono)
+        case goal1
+        have "\<bar>c - a\<bar> \<le> \<bar>l\<bar>"
+          using as' by auto
+        then show ?case
+          apply -
+          apply (rule order_trans[OF _ l(2)])
+          unfolding norm_scaleR
+          apply (rule mult_right_mono)
+          apply auto
+          done
+      next
+        case goal2
+        show ?case
+          apply (rule less_imp_le)
+          apply (cases "a = c")
+          defer
+          apply (rule k(2)[unfolded dist_norm])
+          using as' e ab
+          apply (auto simp add: field_simps)
+          done
+      qed
+      finally show "norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \<le> e * (b - a) / 4"
         unfolding content_real[OF as(1)] by auto
-    qed qed then guess da .. note da=conjunctD2[OF this,rule_format]
+    qed
+  qed
+  then guess da .. note da=conjunctD2[OF this,rule_format]
 
   have "\<exists>db>0. \<forall>c\<le>b. {c..b} \<subseteq> {a..b} \<and> {c..b} \<subseteq> ball b db \<longrightarrow>
-    norm(content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> (e * (b - a)) / 4"
-  proof- have "b\<in>{a..b}" using ab by auto
+    norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> (e * (b - a)) / 4"
+  proof -
+    have "b \<in> {a..b}"
+      using ab by auto
     note assms(2)[unfolded continuous_on_eq_continuous_within,rule_format,OF this]
     note * = this[unfolded continuous_within Lim_within,rule_format] have "(e * (b - a)) / 8 > 0"
-      using e ab by(auto simp add:field_simps)
+      using e ab by (auto simp add: field_simps)
     from *[OF this] guess k .. note k = conjunctD2[OF this,rule_format]
-    have "\<exists>l. 0 < l \<and> norm(l *\<^sub>R f' b) \<le> (e * (b - a)) / 8"
-    proof(cases "f' b = 0") case True
-      thus ?thesis apply(rule_tac x=1 in exI) using ab e by(auto intro!:mult_nonneg_nonneg)
-    next case False thus ?thesis
-        apply(rule_tac x="(e * (b - a)) / 8 / norm (f' b)" in exI)
-        using ab e by(auto simp add:field_simps)
-    qed then guess l .. note l = conjunctD2[OF this]
-    show ?thesis apply(rule_tac x="min k l" in exI) apply safe unfolding min_less_iff_conj apply(rule,(rule l k)+)
-    proof- fix c assume as:"c \<le> b" "{c..b} \<subseteq> {a..b}" "{c..b} \<subseteq> ball b (min k l)"
+    have "\<exists>l. 0 < l \<and> norm (l *\<^sub>R f' b) \<le> (e * (b - a)) / 8"
+    proof (cases "f' b = 0")
+      case True
+      then show ?thesis
+        apply (rule_tac x=1 in exI)
+        using ab e
+        apply (auto intro!: mult_nonneg_nonneg)
+        done
+    next
+      case False
+      then show ?thesis
+        apply (rule_tac x="(e * (b - a)) / 8 / norm (f' b)" in exI)
+        using ab e
+        apply (auto simp add: field_simps)
+        done
+    qed
+    then guess l .. note l = conjunctD2[OF this]
+    show ?thesis
+      apply (rule_tac x="min k l" in exI)
+      apply safe
+      unfolding min_less_iff_conj
+      apply rule
+      apply (rule l k)+
+    proof -
+      fix c
+      assume as: "c \<le> b" "{c..b} \<subseteq> {a..b}" "{c..b} \<subseteq> ball b (min k l)"
       note as' = this[unfolded subset_eq Ball_def mem_ball dist_real_def mem_interval]
-      have "norm ((b - c) *\<^sub>R f' b - (f b - f c)) \<le> norm ((b - c) *\<^sub>R f' b) + norm (f b - f c)" by(rule norm_triangle_ineq4)
-      also have "... \<le> e * (b - a) / 8 + e * (b - a) / 8"
-      proof(rule add_mono) case goal1 have "\<bar>c - b\<bar> \<le> \<bar>l\<bar>" using as' by auto
-        thus ?case apply-apply(rule order_trans[OF _ l(2)]) unfolding norm_scaleR apply(rule mult_right_mono) by auto
-      next case goal2 show ?case apply(rule less_imp_le) apply(cases "b = c") defer apply(subst norm_minus_commute)
-          apply(rule k(2)[unfolded dist_norm]) using as' e ab by(auto simp add:field_simps)
-      qed finally show "norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> e * (b - a) / 4"
+      have "norm ((b - c) *\<^sub>R f' b - (f b - f c)) \<le> norm ((b - c) *\<^sub>R f' b) + norm (f b - f c)"
+        by (rule norm_triangle_ineq4)
+      also have "\<dots> \<le> e * (b - a) / 8 + e * (b - a) / 8"
+      proof (rule add_mono)
+        case goal1
+        have "\<bar>c - b\<bar> \<le> \<bar>l\<bar>"
+          using as' by auto
+        then show ?case
+          apply -
+          apply (rule order_trans[OF _ l(2)])
+          unfolding norm_scaleR
+          apply (rule mult_right_mono)
+          apply auto
+          done
+      next
+        case goal2
+        show ?case
+          apply (rule less_imp_le)
+          apply (cases "b = c")
+          defer
+          apply (subst norm_minus_commute)
+          apply (rule k(2)[unfolded dist_norm])
+          using as' e ab
+          apply (auto simp add: field_simps)
+          done
+      qed
+      finally show "norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> e * (b - a) / 4"
         unfolding content_real[OF as(1)] by auto
-    qed qed then guess db .. note db=conjunctD2[OF this,rule_format]
+    qed
+  qed
+  then guess db .. note db=conjunctD2[OF this,rule_format]
 
   let ?d = "(\<lambda>x. ball x (if x=a then da else if x=b then db else d x))"
-  show "?P e" apply(rule_tac x="?d" in exI)
-  proof safe case goal1 show ?case apply(rule gauge_ball_dependent) using ab db(1) da(1) d(1) by auto
-  next case goal2 note as=this let ?A = "{t. fst t \<in> {a, b}}" note p = tagged_division_ofD[OF goal2(1)]
-    have pA:"p = (p \<inter> ?A) \<union> (p - ?A)" "finite (p \<inter> ?A)" "finite (p - ?A)" "(p \<inter> ?A) \<inter> (p - ?A) = {}"  using goal2 by auto
+  show "?P e"
+    apply (rule_tac x="?d" in exI)
+  proof safe
+    case goal1
+    show ?case
+      apply (rule gauge_ball_dependent)
+      using ab db(1) da(1) d(1)
+      apply auto
+      done
+  next
+    case goal2
+    note as=this
+    let ?A = "{t. fst t \<in> {a, b}}"
+    note p = tagged_division_ofD[OF goal2(1)]
+    have pA: "p = (p \<inter> ?A) \<union> (p - ?A)" "finite (p \<inter> ?A)" "finite (p - ?A)" "(p \<inter> ?A) \<inter> (p - ?A) = {}"
+      using goal2 by auto
     note * = additive_tagged_division_1'[OF assms(1) goal2(1), symmetric]
-    have **:"\<And>n1 s1 n2 s2::real. n2 \<le> s2 / 2 \<Longrightarrow> n1 - s1 \<le> s2 / 2 \<Longrightarrow> n1 + n2 \<le> s1 + s2" by arith
-    show ?case unfolding content_real[OF assms(1)] and *[of "\<lambda>x. x"] *[of f] setsum_subtractf[symmetric] split_minus
-      unfolding setsum_right_distrib apply(subst(2) pA,subst pA) unfolding setsum_Un_disjoint[OF pA(2-)]
-    proof(rule norm_triangle_le,rule **)
-      case goal1 show ?case apply(rule order_trans,rule setsum_norm_le) defer apply(subst setsum_divide_distrib)
-      proof(rule order_refl,safe,unfold not_le o_def split_conv fst_conv,rule ccontr) fix x k assume as:"(x,k) \<in> p"
-          "e * (interval_upperbound k -  interval_lowerbound k) / 2
-          < norm (content k *\<^sub>R f' x - (f (interval_upperbound k) - f (interval_lowerbound k)))"
-        from p(4)[OF this(1)] guess u v apply-by(erule exE)+ note k=this
-        hence "u \<le> v" and uv:"{u,v}\<subseteq>{u..v}" using p(2)[OF as(1)] by auto
+    have **: "\<And>n1 s1 n2 s2::real. n2 \<le> s2 / 2 \<Longrightarrow> n1 - s1 \<le> s2 / 2 \<Longrightarrow> n1 + n2 \<le> s1 + s2"
+      by arith
+    show ?case
+      unfolding content_real[OF assms(1)] and *[of "\<lambda>x. x"] *[of f] setsum_subtractf[symmetric] split_minus
+      unfolding setsum_right_distrib
+      apply (subst(2) pA)
+      apply (subst pA)
+      unfolding setsum_Un_disjoint[OF pA(2-)]
+    proof (rule norm_triangle_le, rule **)
+      case goal1
+      show ?case
+        apply (rule order_trans)
+        apply (rule setsum_norm_le)
+        defer
+        apply (subst setsum_divide_distrib)
+        apply (rule order_refl)
+        apply safe
+        apply (unfold not_le o_def split_conv fst_conv)
+      proof (rule ccontr)
+        fix x k
+        assume as: "(x, k) \<in> p"
+          "e * (interval_upperbound k -  interval_lowerbound k) / 2 <
+            norm (content k *\<^sub>R f' x - (f (interval_upperbound k) - f (interval_lowerbound k)))"
+        from p(4)[OF this(1)] guess u v by (elim exE) note k=this
+        then have "u \<le> v" and uv: "{u, v} \<subseteq> {u..v}"
+          using p(2)[OF as(1)] by auto
         note result = as(2)[unfolded k interval_bounds_real[OF this(1)] content_real[OF this(1)]]
 
-        assume as':"x \<noteq> a" "x \<noteq> b" hence "x \<in> {a<..<b}" using p(2-3)[OF as(1)] by auto
+        assume as': "x \<noteq> a" "x \<noteq> b"
+        then have "x \<in> {a<..<b}"
+          using p(2-3)[OF as(1)] by auto
         note  * = d(2)[OF this]
         have "norm ((v - u) *\<^sub>R f' (x) - (f (v) - f (u))) =
           norm ((f (u) - f (x) - (u - x) *\<^sub>R f' (x)) - (f (v) - f (x) - (v - x) *\<^sub>R f' (x)))"
-          apply(rule arg_cong[of _ _ norm]) unfolding scaleR_left.diff by auto
-        also have "... \<le> e / 2 * norm (u - x) + e / 2 * norm (v - x)" apply(rule norm_triangle_le_sub)
-          apply(rule add_mono) apply(rule_tac[!] *) using fineD[OF goal2(2) as(1)] as' unfolding k subset_eq
-          apply- apply(erule_tac x=u in ballE,erule_tac[3] x=v in ballE) using uv by(auto simp:dist_real_def)
-        also have "... \<le> e / 2 * norm (v - u)" using p(2)[OF as(1)] unfolding k by(auto simp add:field_simps)
+          apply (rule arg_cong[of _ _ norm])
+          unfolding scaleR_left.diff
+          apply auto
+          done
+        also have "\<dots> \<le> e / 2 * norm (u - x) + e / 2 * norm (v - x)"
+          apply (rule norm_triangle_le_sub)
+          apply (rule add_mono)
+          apply (rule_tac[!] *)
+          using fineD[OF goal2(2) as(1)] as'
+          unfolding k subset_eq
+          apply -
+          apply (erule_tac x=u in ballE)
+          apply (erule_tac[3] x=v in ballE)
+          using uv
+          apply (auto simp:dist_real_def)
+          done
+        also have "\<dots> \<le> e / 2 * norm (v - u)"
+          using p(2)[OF as(1)]
+          unfolding k
+          by (auto simp add: field_simps)
         finally have "e * (v - u) / 2 < e * (v - u) / 2"
-          apply- apply(rule less_le_trans[OF result]) using uv by auto thus False by auto qed
-
-    next have *:"\<And>x s1 s2::real. 0 \<le> s1 \<Longrightarrow> x \<le> (s1 + s2) / 2 \<Longrightarrow> x - s1 \<le> s2 / 2" by auto
-      case goal2 show ?case apply(rule *) apply(rule setsum_nonneg) apply(rule,unfold split_paired_all split_conv)
-        defer unfolding setsum_Un_disjoint[OF pA(2-),symmetric] pA(1)[symmetric] unfolding setsum_right_distrib[symmetric]
-        apply(subst additive_tagged_division_1[OF _ as(1)]) apply(rule assms)
-      proof- fix x k assume "(x,k) \<in> p \<inter> {t. fst t \<in> {a, b}}" note xk=IntD1[OF this]
-        from p(4)[OF this] guess u v apply-by(erule exE)+ note uv=this
-        with p(2)[OF xk] have "{u..v} \<noteq> {}" by auto
-        thus "0 \<le> e * ((interval_upperbound k) - (interval_lowerbound k))"
-          unfolding uv using e by(auto simp add:field_simps)
-      next have *:"\<And>s f t e. setsum f s = setsum f t \<Longrightarrow> norm(setsum f t) \<le> e \<Longrightarrow> norm(setsum f s) \<le> e" by auto
+          apply -
+          apply (rule less_le_trans[OF result])
+          using uv
+          apply auto
+          done
+        then show False by auto
+      qed
+    next
+      have *: "\<And>x s1 s2::real. 0 \<le> s1 \<Longrightarrow> x \<le> (s1 + s2) / 2 \<Longrightarrow> x - s1 \<le> s2 / 2"
+        by auto
+      case goal2
+      show ?case
+        apply (rule *)
+        apply (rule setsum_nonneg)
+        apply rule
+        apply (unfold split_paired_all split_conv)
+        defer
+        unfolding setsum_Un_disjoint[OF pA(2-),symmetric] pA(1)[symmetric]
+        unfolding setsum_right_distrib[symmetric]
+        apply (subst additive_tagged_division_1[OF _ as(1)])
+        apply (rule assms)
+      proof -
+        fix x k
+        assume "(x, k) \<in> p \<inter> {t. fst t \<in> {a, b}}"
+        note xk=IntD1[OF this]
+        from p(4)[OF this] guess u v by (elim exE) note uv=this
+        with p(2)[OF xk] have "{u..v} \<noteq> {}"
+          by auto
+        then show "0 \<le> e * ((interval_upperbound k) - (interval_lowerbound k))"
+          unfolding uv using e by (auto simp add: field_simps)
+      next
+        have *: "\<And>s f t e. setsum f s = setsum f t \<Longrightarrow> norm (setsum f t) \<le> e \<Longrightarrow> norm (setsum f s) \<le> e"
+          by auto
         show "norm (\<Sum>(x, k)\<in>p \<inter> ?A. content k *\<^sub>R f' x -
           (f ((interval_upperbound k)) - f ((interval_lowerbound k)))) \<le> e * (b - a) / 2"
-          apply(rule *[where t="p \<inter> {t. fst t \<in> {a, b} \<and> content(snd t) \<noteq> 0}"])
-          apply(rule setsum_mono_zero_right[OF pA(2)]) defer apply(rule) unfolding split_paired_all split_conv o_def
-        proof- fix x k assume "(x,k) \<in> p \<inter> {t. fst t \<in> {a, b}} - p \<inter> {t. fst t \<in> {a, b} \<and> content (snd t) \<noteq> 0}"
-          hence xk:"(x,k)\<in>p" "content k = 0" by auto from p(4)[OF xk(1)] guess u v apply-by(erule exE)+ note uv=this
-          have "k\<noteq>{}" using p(2)[OF xk(1)] by auto hence *:"u = v" using xk
-            unfolding uv content_eq_0 interval_eq_empty by auto
-          thus "content k *\<^sub>R (f' (x)) - (f ((interval_upperbound k)) - f ((interval_lowerbound k))) = 0" using xk unfolding uv by auto
-        next have *:"p \<inter> {t. fst t \<in> {a, b} \<and> content(snd t) \<noteq> 0} =
-            {t. t\<in>p \<and> fst t = a \<and> content(snd t) \<noteq> 0} \<union> {t. t\<in>p \<and> fst t = b \<and> content(snd t) \<noteq> 0}" by blast
-          have **:"\<And>s f. \<And>e::real. (\<forall>x y. x \<in> s \<and> y \<in> s \<longrightarrow> x = y) \<Longrightarrow> (\<forall>x. x \<in> s \<longrightarrow> norm(f x) \<le> e)
-            \<Longrightarrow> e>0 \<Longrightarrow> norm(setsum f s) \<le> e"
-          proof(case_tac "s={}") case goal2 then obtain x where "x\<in>s" by auto hence *:"s = {x}" using goal2(1) by auto
-            thus ?case using `x\<in>s` goal2(2) by auto
+          apply (rule *[where t="p \<inter> {t. fst t \<in> {a, b} \<and> content(snd t) \<noteq> 0}"])
+          apply (rule setsum_mono_zero_right[OF pA(2)])
+          defer
+          apply rule
+          unfolding split_paired_all split_conv o_def
+        proof -
+          fix x k
+          assume "(x, k) \<in> p \<inter> {t. fst t \<in> {a, b}} - p \<inter> {t. fst t \<in> {a, b} \<and> content (snd t) \<noteq> 0}"
+          then have xk: "(x, k) \<in> p" "content k = 0"
+            by auto
+          from p(4)[OF xk(1)] guess u v by (elim exE) note uv=this
+          have "k \<noteq> {}"
+            using p(2)[OF xk(1)] by auto
+          then have *: "u = v"
+            using xk
+            unfolding uv content_eq_0 interval_eq_empty
+            by auto
+          then show "content k *\<^sub>R (f' (x)) - (f ((interval_upperbound k)) - f ((interval_lowerbound k))) = 0"
+            using xk unfolding uv by auto
+        next
+          have *: "p \<inter> {t. fst t \<in> {a, b} \<and> content(snd t) \<noteq> 0} =
+            {t. t\<in>p \<and> fst t = a \<and> content(snd t) \<noteq> 0} \<union> {t. t\<in>p \<and> fst t = b \<and> content(snd t) \<noteq> 0}"
+            by blast
+          have **: "\<And>s f. \<And>e::real. (\<forall>x y. x \<in> s \<and> y \<in> s \<longrightarrow> x = y) \<Longrightarrow>
+            (\<forall>x. x \<in> s \<longrightarrow> norm (f x) \<le> e) \<Longrightarrow> e > 0 \<Longrightarrow> norm (setsum f s) \<le> e"
+          proof (case_tac "s = {}")
+            case goal2
+            then obtain x where "x \<in> s"
+              by auto
+            then have *: "s = {x}"
+              using goal2(1) by auto
+            then show ?case
+              using `x \<in> s` goal2(2) by auto
           qed auto
-          case goal2 show ?case apply(subst *, subst setsum_Un_disjoint) prefer 4
-            apply(rule order_trans[of _ "e * (b - a)/4 + e * (b - a)/4"])
-            apply(rule norm_triangle_le,rule add_mono) apply(rule_tac[1-2] **)
-          proof- let ?B = "\<lambda>x. {t \<in> p. fst t = x \<and> content (snd t) \<noteq> 0}"
-            have pa:"\<And>k. (a, k) \<in> p \<Longrightarrow> \<exists>v. k = {a .. v} \<and> a \<le> v"
-            proof- case goal1 guess u v using p(4)[OF goal1] apply-by(erule exE)+ note uv=this
-              have *:"u \<le> v" using p(2)[OF goal1] unfolding uv by auto
-              have u:"u = a" proof(rule ccontr)  have "u \<in> {u..v}" using p(2-3)[OF goal1(1)] unfolding uv by auto
-                have "u \<ge> a" using p(2-3)[OF goal1(1)] unfolding uv subset_eq by auto moreover assume "u\<noteq>a" ultimately
-                have "u > a" by auto
-                thus False using p(2)[OF goal1(1)] unfolding uv by(auto simp add:)
-              qed thus ?case apply(rule_tac x=v in exI) unfolding uv using * by auto
+          case goal2
+          show ?case
+            apply (subst *)
+            apply (subst setsum_Un_disjoint)
+            prefer 4
+            apply (rule order_trans[of _ "e * (b - a)/4 + e * (b - a)/4"])
+            apply (rule norm_triangle_le,rule add_mono)
+            apply (rule_tac[1-2] **)
+          proof -
+            let ?B = "\<lambda>x. {t \<in> p. fst t = x \<and> content (snd t) \<noteq> 0}"
+            have pa: "\<And>k. (a, k) \<in> p \<Longrightarrow> \<exists>v. k = {a .. v} \<and> a \<le> v"
+            proof -
+              case goal1
+              guess u v using p(4)[OF goal1] by (elim exE) note uv=this
+              have *: "u \<le> v"
+                using p(2)[OF goal1] unfolding uv by auto
+              have u: "u = a"
+              proof (rule ccontr)
+                have "u \<in> {u..v}"
+                  using p(2-3)[OF goal1(1)] unfolding uv by auto
+                have "u \<ge> a"
+                  using p(2-3)[OF goal1(1)] unfolding uv subset_eq by auto
+                moreover assume "u \<noteq> a"
+                ultimately have "u > a" by auto
+                then show False
+                  using p(2)[OF goal1(1)] unfolding uv by (auto simp add:)
+              qed
+              then show ?case
+                apply (rule_tac x=v in exI)
+                unfolding uv
+                using *
+                apply auto
+                done
             qed
-            have pb:"\<And>k. (b, k) \<in> p \<Longrightarrow> \<exists>v. k = {v .. b} \<and> b \<ge> v"
-            proof- case goal1 guess u v using p(4)[OF goal1] apply-by(erule exE)+ note uv=this
-              have *:"u \<le> v" using p(2)[OF goal1] unfolding uv by auto
-              have u:"v =  b" proof(rule ccontr)  have "u \<in> {u..v}" using p(2-3)[OF goal1(1)] unfolding uv by auto
-                have "v \<le>  b" using p(2-3)[OF goal1(1)] unfolding uv subset_eq by auto moreover assume "v\<noteq> b" ultimately
-                have "v <  b" by auto
-                thus False using p(2)[OF goal1(1)] unfolding uv by(auto simp add:)
-              qed thus ?case apply(rule_tac x=u in exI) unfolding uv using * by auto
+            have pb: "\<And>k. (b, k) \<in> p \<Longrightarrow> \<exists>v. k = {v .. b} \<and> b \<ge> v"
+            proof -
+              case goal1
+              guess u v using p(4)[OF goal1] by (elim exE) note uv=this
+              have *: "u \<le> v"
+                using p(2)[OF goal1] unfolding uv by auto
+              have u: "v =  b"
+              proof (rule ccontr)
+                have "u \<in> {u..v}"
+                  using p(2-3)[OF goal1(1)] unfolding uv by auto
+                have "v \<le> b"
+                  using p(2-3)[OF goal1(1)] unfolding uv subset_eq by auto
+                moreover assume "v \<noteq> b"
+                ultimately have "v < b" by auto
+                then show False
+                  using p(2)[OF goal1(1)] unfolding uv by (auto simp add:)
+              qed
+              then show ?case
+                apply (rule_tac x=u in exI)
+                unfolding uv
+                using *
+                apply auto
+                done
             qed
-
-            show "\<forall>x y. x \<in> ?B a \<and> y \<in> ?B a \<longrightarrow> x = y" apply(rule,rule,rule,unfold split_paired_all)
-              unfolding mem_Collect_eq fst_conv snd_conv apply safe
-            proof- fix x k k' assume k:"( a, k) \<in> p" "( a, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
+            show "\<forall>x y. x \<in> ?B a \<and> y \<in> ?B a \<longrightarrow> x = y"
+              apply (rule,rule,rule,unfold split_paired_all)
+              unfolding mem_Collect_eq fst_conv snd_conv
+              apply safe
+            proof -
+              fix x k k'
+              assume k: "(a, k) \<in> p" "(a, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
               guess v using pa[OF k(1)] .. note v = conjunctD2[OF this]
-              guess v' using pa[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = " (min (v) (v'))"
-              have "{ a <..< ?v} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note interior_mono[OF this,unfolded interior_inter]
-              moreover have " ((a + ?v)/2) \<in> { a <..< ?v}" using k(3-)
-                unfolding v v' content_eq_0 not_le by(auto simp add:not_le)
-              ultimately have " ((a + ?v)/2) \<in> interior k \<inter> interior k'" unfolding interior_open[OF open_interval] by auto
-              hence *:"k = k'" apply- apply(rule ccontr) using p(5)[OF k(1-2)] by auto
-              { assume "x\<in>k" thus "x\<in>k'" unfolding * . } { assume "x\<in>k'" thus "x\<in>k" unfolding * . }
+              guess v' using pa[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = "min v v'"
+              have "{a <..< ?v} \<subseteq> k \<inter> k'"
+                unfolding v v' by (auto simp add:)
+              note interior_mono[OF this,unfolded interior_inter]
+              moreover have "(a + ?v)/2 \<in> { a <..< ?v}"
+                using k(3-)
+                unfolding v v' content_eq_0 not_le
+                by (auto simp add: not_le)
+              ultimately have "(a + ?v)/2 \<in> interior k \<inter> interior k'"
+                unfolding interior_open[OF open_interval] by auto
+              then have *: "k = k'"
+                apply -
+                apply (rule ccontr)
+                using p(5)[OF k(1-2)]
+                apply auto
+                done
+              { assume "x \<in> k" then show "x \<in> k'" unfolding * . }
+              { assume "x \<in> k'" then show "x\<in>k" unfolding * . }
             qed
-            show "\<forall>x y. x \<in> ?B b \<and> y \<in> ?B b \<longrightarrow> x = y" apply(rule,rule,rule,unfold split_paired_all)
-              unfolding mem_Collect_eq fst_conv snd_conv apply safe
-            proof- fix x k k' assume k:"( b, k) \<in> p" "( b, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
+            show "\<forall>x y. x \<in> ?B b \<and> y \<in> ?B b \<longrightarrow> x = y"
+              apply rule
+              apply rule
+              apply rule
+              apply (unfold split_paired_all)
+              unfolding mem_Collect_eq fst_conv snd_conv
+              apply safe
+            proof -
+              fix x k k'
+              assume k: "(b, k) \<in> p" "(b, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
               guess v using pb[OF k(1)] .. note v = conjunctD2[OF this]
-              guess v' using pb[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = " (max (v) (v'))"
-              have "{?v <..<  b} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note interior_mono[OF this,unfolded interior_inter]
-              moreover have " ((b + ?v)/2) \<in> {?v <..<  b}" using k(3-) unfolding v v' content_eq_0 not_le by auto
-              ultimately have " ((b + ?v)/2) \<in> interior k \<inter> interior k'" unfolding interior_open[OF open_interval] by auto
-              hence *:"k = k'" apply- apply(rule ccontr) using p(5)[OF k(1-2)] by auto
-              { assume "x\<in>k" thus "x\<in>k'" unfolding * . } { assume "x\<in>k'" thus "x\<in>k" unfolding * . }
+              guess v' using pb[OF k(2)] .. note v' = conjunctD2[OF this]
+              let ?v = "max v v'"
+              have "{?v <..< b} \<subseteq> k \<inter> k'"
+                unfolding v v' by auto
+                note interior_mono[OF this,unfolded interior_inter]
+              moreover have " ((b + ?v)/2) \<in> {?v <..<  b}"
+                using k(3-) unfolding v v' content_eq_0 not_le by auto
+              ultimately have " ((b + ?v)/2) \<in> interior k \<inter> interior k'"
+                unfolding interior_open[OF open_interval] by auto
+              then have *: "k = k'"
+                apply -
+                apply (rule ccontr)
+                using p(5)[OF k(1-2)]
+                apply auto
+                done
+              { assume "x \<in> k" then show "x \<in> k'" unfolding * . }
+              { assume "x \<in> k'" then show "x\<in>k" unfolding * . }
             qed
 
             let ?a = a and ?b = b (* a is something else while proofing the next theorem. *)
-            show "\<forall>x. x \<in> ?B a \<longrightarrow> norm ((\<lambda>(x, k). content k *\<^sub>R f' (x) - (f ((interval_upperbound k)) -
-              f ((interval_lowerbound k)))) x) \<le> e * (b - a) / 4" apply(rule,rule) unfolding mem_Collect_eq
+            show "\<forall>x. x \<in> ?B a \<longrightarrow> norm ((\<lambda>(x, k). content k *\<^sub>R f' x - (f (interval_upperbound k) -
+              f (interval_lowerbound k))) x) \<le> e * (b - a) / 4"
+              apply rule
+              apply rule
+              unfolding mem_Collect_eq
               unfolding split_paired_all fst_conv snd_conv
-            proof safe case goal1 guess v using pa[OF goal1(1)] .. note v = conjunctD2[OF this]
-              have " ?a\<in>{ ?a..v}" using v(2) by auto hence "v \<le> ?b" using p(3)[OF goal1(1)] unfolding subset_eq v by auto
-              moreover have "{?a..v} \<subseteq> ball ?a da" using fineD[OF as(2) goal1(1)]
-                apply-apply(subst(asm) if_P,rule refl) unfolding subset_eq apply safe apply(erule_tac x=" x" in ballE)
-                by(auto simp add:subset_eq dist_real_def v) ultimately
-              show ?case unfolding v interval_bounds_real[OF v(2)] apply- apply(rule da(2)[of "v"])
-                using goal1 fineD[OF as(2) goal1(1)] unfolding v content_eq_0 by auto
+            proof safe
+              case goal1
+              guess v using pa[OF goal1(1)] .. note v = conjunctD2[OF this]
+              have "?a \<in> {?a..v}"
+                using v(2) by auto
+              then have "v \<le> ?b"
+                using p(3)[OF goal1(1)] unfolding subset_eq v by auto
+              moreover have "{?a..v} \<subseteq> ball ?a da"
+                using fineD[OF as(2) goal1(1)]
+                apply -
+                apply (subst(asm) if_P)
+                apply (rule refl)
+                unfolding subset_eq
+                apply safe
+                apply (erule_tac x=" x" in ballE)
+                apply (auto simp add:subset_eq dist_real_def v)
+                done
+              ultimately show ?case
+                unfolding v interval_bounds_real[OF v(2)]
+                apply -
+                apply(rule da(2)[of "v"])
+                using goal1 fineD[OF as(2) goal1(1)]
+                unfolding v content_eq_0
+                apply auto
+                done
             qed
-            show "\<forall>x. x \<in> ?B b \<longrightarrow> norm ((\<lambda>(x, k). content k *\<^sub>R f' (x) -
-              (f ((interval_upperbound k)) - f ((interval_lowerbound k)))) x) \<le> e * (b - a) / 4"
-              apply(rule,rule) unfolding mem_Collect_eq unfolding split_paired_all fst_conv snd_conv
-            proof safe case goal1 guess v using pb[OF goal1(1)] .. note v = conjunctD2[OF this]
-              have " ?b\<in>{v.. ?b}" using v(2) by auto hence "v \<ge> ?a" using p(3)[OF goal1(1)]
+            show "\<forall>x. x \<in> ?B b \<longrightarrow> norm ((\<lambda>(x, k). content k *\<^sub>R f' x -
+              (f (interval_upperbound k) - f (interval_lowerbound k))) x) \<le> e * (b - a) / 4"
+              apply rule
+              apply rule
+              unfolding mem_Collect_eq
+              unfolding split_paired_all fst_conv snd_conv
+            proof safe
+              case goal1 guess v using pb[OF goal1(1)] .. note v = conjunctD2[OF this]
+              have "?b \<in> {v.. ?b}"
+                using v(2) by auto
+              then have "v \<ge> ?a" using p(3)[OF goal1(1)]
                 unfolding subset_eq v by auto
-              moreover have "{v..?b} \<subseteq> ball ?b db" using fineD[OF as(2) goal1(1)]
-                apply-apply(subst(asm) if_P,rule refl) unfolding subset_eq apply safe
-                apply(erule_tac x=" x" in ballE) using ab
-                by(auto simp add:subset_eq v dist_real_def) ultimately
-              show ?case unfolding v unfolding interval_bounds_real[OF v(2)] apply- apply(rule db(2)[of "v"])
-                using goal1 fineD[OF as(2) goal1(1)] unfolding v content_eq_0 by auto
+              moreover have "{v..?b} \<subseteq> ball ?b db"
+                using fineD[OF as(2) goal1(1)]
+                apply -
+                apply (subst(asm) if_P, rule refl)
+                unfolding subset_eq
+                apply safe
+                apply (erule_tac x=" x" in ballE)
+                using ab
+                apply (auto simp add:subset_eq v dist_real_def)
+                done
+              ultimately show ?case
+                unfolding v
+                unfolding interval_bounds_real[OF v(2)]
+                apply -
+                apply(rule db(2)[of "v"])
+                using goal1 fineD[OF as(2) goal1(1)]
+                unfolding v content_eq_0
+                apply auto
+                done
             qed
-          qed(insert p(1) ab e, auto simp add:field_simps) qed auto qed qed qed qed
+          qed (insert p(1) ab e, auto simp add: field_simps)
+        qed auto
+      qed
+    qed
+  qed
+qed
+
 
 subsection {* Stronger form with finite number of exceptional points. *}