# HG changeset patch
# User paulson
# Date 1503924063 -3600
# Node ID 9cbe0084b94174a4cf23f199b3248ce786a42c42
# Parent  322120e880c592b244e4b152f7b36e5801a2ea2c# Parent  c485474cd91dff8915d6d4a83fb55777bf842865
merged

diff -r 322120e880c5 -r 9cbe0084b941 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Aug 26 18:58:40 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Aug 28 13:41:03 2017 +0100
@@ -324,7 +324,7 @@
   assumes "(f has_integral k1) i" "(f has_integral k2) i"
   shows "k1 = k2"
 proof (rule ccontr)
-  let ?e = "norm (k1 - k2) / 2"
+  let ?e = "norm (k1 - k2)/2"
   let ?F = "(\<lambda>x. if x \<in> i then f x else 0)"
   assume "k1 \<noteq> k2"
   then have e: "?e > 0"
@@ -334,25 +334,25 @@
   obtain B1 where B1:
       "0 < B1"
       "\<And>a b. ball 0 B1 \<subseteq> cbox a b \<Longrightarrow>
-        \<exists>z. (?F has_integral z) (cbox a b) \<and> norm (z - k1) < norm (k1 - k2) / 2"
+        \<exists>z. (?F has_integral z) (cbox a b) \<and> norm (z - k1) < norm (k1 - k2)/2"
     by (rule has_integral_altD[OF assms(1) nonbox,OF e]) blast
   obtain B2 where B2:
       "0 < B2"
       "\<And>a b. ball 0 B2 \<subseteq> cbox a b \<Longrightarrow>
-        \<exists>z. (?F has_integral z) (cbox a b) \<and> norm (z - k2) < norm (k1 - k2) / 2"
+        \<exists>z. (?F has_integral z) (cbox a b) \<and> norm (z - k2) < norm (k1 - k2)/2"
     by (rule has_integral_altD[OF assms(2) nonbox,OF e]) blast
   obtain a b :: 'n where ab: "ball 0 B1 \<subseteq> cbox a b" "ball 0 B2 \<subseteq> cbox a b"
     by (metis Un_subset_iff bounded_Un bounded_ball bounded_subset_cbox)
-  obtain w where w: "(?F has_integral w) (cbox a b)" "norm (w - k1) < norm (k1 - k2) / 2"
+  obtain w where w: "(?F has_integral w) (cbox a b)" "norm (w - k1) < norm (k1 - k2)/2"
     using B1(2)[OF ab(1)] by blast
-  obtain z where z: "(?F has_integral z) (cbox a b)" "norm (z - k2) < norm (k1 - k2) / 2"
+  obtain z where z: "(?F has_integral z) (cbox a b)" "norm (z - k2) < norm (k1 - k2)/2"
     using B2(2)[OF ab(2)] by blast
   have "z = w"
     using has_integral_unique_cbox[OF w(1) z(1)] by auto
   then have "norm (k1 - k2) \<le> norm (z - k2) + norm (w - k1)"
     using norm_triangle_ineq4 [of "k1 - w" "k2 - z"]
     by (auto simp add: norm_minus_commute)
-  also have "\<dots> < norm (k1 - k2) / 2 + norm (k1 - k2) / 2"
+  also have "\<dots> < norm (k1 - k2)/2 + norm (k1 - k2)/2"
     by (metis add_strict_mono z(2) w(2))
   finally show False by auto
 qed
@@ -1290,10 +1290,10 @@
           using mem_interior by metis
         have x: "x\<bullet>k = c"
           using x interior_subset by fastforce
-        have *: "\<And>i. i \<in> Basis \<Longrightarrow> \<bar>(x - (x + (\<epsilon> / 2) *\<^sub>R k)) \<bullet> i\<bar> = (if i = k then \<epsilon>/2 else 0)"
+        have *: "\<And>i. i \<in> Basis \<Longrightarrow> \<bar>(x - (x + (\<epsilon>/2) *\<^sub>R k)) \<bullet> i\<bar> = (if i = k then \<epsilon>/2 else 0)"
           using \<open>0 < \<epsilon>\<close> k by (auto simp: inner_simps inner_not_same_Basis)
-        have "(\<Sum>i\<in>Basis. \<bar>(x - (x + (\<epsilon> / 2 ) *\<^sub>R k)) \<bullet> i\<bar>) =
-              (\<Sum>i\<in>Basis. (if i = k then \<epsilon> / 2 else 0))"
+        have "(\<Sum>i\<in>Basis. \<bar>(x - (x + (\<epsilon>/2 ) *\<^sub>R k)) \<bullet> i\<bar>) =
+              (\<Sum>i\<in>Basis. (if i = k then \<epsilon>/2 else 0))"
           using "*" by (blast intro: sum.cong)
         also have "\<dots> < \<epsilon>"
           by (subst sum.delta) (use \<open>0 < \<epsilon>\<close> in auto)
@@ -1964,17 +1964,17 @@
       assume c: "c < a \<bullet> k"
       moreover have "x \<in> cbox a b \<Longrightarrow> c \<le> x \<bullet> k" for x
         using k c by (auto simp: cbox_def)
-      ultimately have "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> (a \<bullet> k - c) / 2} = {}"
+      ultimately have "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> (a \<bullet> k - c)/2} = {}"
         using k by (auto simp: cbox_def)
-      with \<open>0<e\<close> c that[of "(a \<bullet> k - c) / 2"] show ?thesis
+      with \<open>0<e\<close> c that[of "(a \<bullet> k - c)/2"] show ?thesis
         by auto
     next
       assume c: "b \<bullet> k < c"
       moreover have "x \<in> cbox a b \<Longrightarrow> x \<bullet> k \<le> c" for x
         using k c by (auto simp: cbox_def)
-      ultimately have "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> (c - b \<bullet> k) / 2} = {}"
+      ultimately have "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> (c - b \<bullet> k)/2} = {}"
         using k by (auto simp: cbox_def)
-      with \<open>0<e\<close> c that[of "(c - b \<bullet> k) / 2"] show ?thesis
+      with \<open>0<e\<close> c that[of "(c - b \<bullet> k)/2"] show ?thesis
         by auto
     qed
   qed
@@ -2194,21 +2194,21 @@
         done
       also have "... \<le> (\<Sum>i\<le>N + 1. (real i + 1) * \<bar>\<Sum>(x,K) \<in> q i. content K *\<^sub>R indicator S x\<bar>)"
         by (rule sum_mono) (simp add: sum_distrib_left [symmetric])
-      also have "... \<le> (\<Sum>i\<le>N + 1. e/2 / 2 ^ i)"
+      also have "... \<le> (\<Sum>i\<le>N + 1. e/2/2 ^ i)"
       proof (rule sum_mono)
-        show "(real i + 1) * \<bar>\<Sum>(x,K) \<in> q i. content K *\<^sub>R indicator S x\<bar> \<le> e/2 / 2 ^ i"
+        show "(real i + 1) * \<bar>\<Sum>(x,K) \<in> q i. content K *\<^sub>R indicator S x\<bar> \<le> e/2/2 ^ i"
           if "i \<in> {..N + 1}" for i
           using \<gamma>[of "q i" i] q by (simp add: divide_simps mult.left_commute)
       qed
-      also have "... = e/2 * (\<Sum>i\<le>N + 1. (1 / 2) ^ i)"
+      also have "... = e/2 * (\<Sum>i\<le>N + 1. (1/2) ^ i)"
         unfolding sum_distrib_left by (metis divide_inverse inverse_eq_divide power_one_over)
       also have "\<dots> < e/2 * 2"
       proof (rule mult_strict_left_mono)
-        have "sum (op ^ (1 / 2)) {..N + 1} = sum (op ^ (1 / 2::real)) {..<N + 2}"
+        have "sum (op ^ (1/2)) {..N + 1} = sum (op ^ (1/2::real)) {..<N + 2}"
           using lessThan_Suc_atMost by auto
         also have "... < 2"
           by (auto simp: geometric_sum)
-        finally show "sum (op ^ (1 / 2::real)) {..N + 1} < 2" .
+        finally show "sum (op ^ (1/2::real)) {..N + 1} < 2" .
       qed (use \<open>0 < e\<close> in auto)
       finally  show ?thesis by auto
     qed
@@ -2727,7 +2727,7 @@
 lemma ident_has_integral:
   fixes a::real
   assumes "a \<le> b"
-  shows "((\<lambda>x. x) has_integral (b\<^sup>2 - a\<^sup>2) / 2) {a..b}"
+  shows "((\<lambda>x. x) has_integral (b\<^sup>2 - a\<^sup>2)/2) {a..b}"
 proof -
   have "((\<lambda>x. x) has_integral inverse 2 * b\<^sup>2 - inverse 2 * a\<^sup>2) {a..b}"
     apply (rule fundamental_theorem_of_calculus [OF assms], clarify)
@@ -2740,7 +2740,7 @@
 lemma integral_ident [simp]:
   fixes a::real
   assumes "a \<le> b"
-  shows "integral {a..b} (\<lambda>x. x) = (if a \<le> b then (b\<^sup>2 - a\<^sup>2) / 2 else 0)"
+  shows "integral {a..b} (\<lambda>x. x) = (if a \<le> b then (b\<^sup>2 - a\<^sup>2)/2 else 0)"
   by (metis assms ident_has_integral integral_unique)
 
 lemma ident_integrable_on:
@@ -2798,9 +2798,9 @@
   and ivl: "a \<le> b"
   defines "i \<equiv> \<lambda>x. ((b - x) ^ (p - 1) / fact (p - 1)) *\<^sub>R Df p x"
   shows taylor_has_integral:
-    "(i has_integral f b - (\<Sum>i<p. ((b - a) ^ i / fact i) *\<^sub>R Df i a)) {a..b}"
+    "(i has_integral f b - (\<Sum>i<p. ((b-a) ^ i / fact i) *\<^sub>R Df i a)) {a..b}"
   and taylor_integral:
-    "f b = (\<Sum>i<p. ((b - a) ^ i / fact i) *\<^sub>R Df i a) + integral {a..b} i"
+    "f b = (\<Sum>i<p. ((b-a) ^ i / fact i) *\<^sub>R Df i a) + integral {a..b} i"
   and taylor_integrable:
     "i integrable_on {a..b}"
 proof goal_cases
@@ -2855,7 +2855,7 @@
       by (auto intro!: image_eqI[where x = "p - x - 1"])
   qed simp
   from _ this
-  have "?sum a = (\<Sum>i<p. ((b - a) ^ i / fact i) *\<^sub>R Df i a)"
+  have "?sum a = (\<Sum>i<p. ((b-a) ^ i / fact i) *\<^sub>R Df i a)"
     by (rule sum.reindex_cong) (auto simp add: inj_on_def Dg_def one)
   finally show c: ?case .
   case 2 show ?case using c integral_unique
@@ -2900,8 +2900,8 @@
       by (meson content_eq_0 dual_order.antisym)
     then have xi: "x\<bullet>i = d\<bullet>i"
       using \<open>x \<in> K\<close> unfolding keq mem_box by (metis antisym)
-    define y where "y = (\<Sum>j\<in>Basis. (if j = i then if c\<bullet>i \<le> (a\<bullet>i + b\<bullet>i) / 2 then c\<bullet>i +
-      min e (b\<bullet>i - c\<bullet>i) / 2 else c\<bullet>i - min e (c\<bullet>i - a\<bullet>i) / 2 else x\<bullet>j) *\<^sub>R j)"
+    define y where "y = (\<Sum>j\<in>Basis. (if j = i then if c\<bullet>i \<le> (a\<bullet>i + b\<bullet>i)/2 then c\<bullet>i +
+      min e (b\<bullet>i - c\<bullet>i)/2 else c\<bullet>i - min e (c\<bullet>i - a\<bullet>i)/2 else x\<bullet>j) *\<^sub>R j)"
     show "\<exists>x'\<in>\<Union>(\<D> - {K}). x' \<noteq> x \<and> dist x' x < e"
     proof (intro bexI conjI)
       have "d \<in> cbox c d"
@@ -3414,7 +3414,7 @@
       apply (erule_tac x=i in ballE)
       apply (auto simp: inner_simps mult_left_mono)
       done
-    moreover from True have *: "\<And>i. (m *\<^sub>R b + c) \<bullet> i - (m *\<^sub>R a + c) \<bullet> i = m *\<^sub>R (b - a) \<bullet> i"
+    moreover from True have *: "\<And>i. (m *\<^sub>R b + c) \<bullet> i - (m *\<^sub>R a + c) \<bullet> i = m *\<^sub>R (b-a) \<bullet> i"
       by (simp add: inner_simps field_simps)
     ultimately show ?thesis
       by (simp add: image_affinity_cbox True content_cbox'
@@ -3427,7 +3427,7 @@
       apply (erule_tac x=i in ballE)
       apply (auto simp: inner_simps mult_left_mono)
       done
-    moreover from False have *: "\<And>i. (m *\<^sub>R a + c) \<bullet> i - (m *\<^sub>R b + c) \<bullet> i = (-m) *\<^sub>R (b - a) \<bullet> i"
+    moreover from False have *: "\<And>i. (m *\<^sub>R a + c) \<bullet> i - (m *\<^sub>R b + c) \<bullet> i = (-m) *\<^sub>R (b-a) \<bullet> i"
       by (simp add: inner_simps field_simps)
     ultimately show ?thesis using False
       by (simp add: image_affinity_cbox content_cbox'
@@ -3543,7 +3543,7 @@
   fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
   assumes "a \<le> b"
     and contf: "continuous_on {a..b} f"
-    and derf: "\<And>x. x \<in> {a <..< b} \<Longrightarrow> (f has_vector_derivative f'(x)) (at x)"
+    and derf: "\<And>x. x \<in> {a <..< b} \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
   shows "(f' has_integral (f b - f a)) {a..b}"
 proof (cases "a = b")
   case True
@@ -3553,165 +3553,163 @@
 next
   case False
   with \<open>a \<le> b\<close> have ab: "a < b" by arith
-  let ?P = "\<lambda>e. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a..b} \<longrightarrow> 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" then show ?thesis unfolding has_integral_factor_content_real by force }
-  fix e :: real
-  assume e: "e > 0"
-  then have eba8: "(e * (b - a)) / 8 > 0"
-    using ab by (auto simp add: field_simps)
-  note derf_exp = derf[unfolded has_vector_derivative_def has_derivative_at_alt]
-  have bounded: "\<And>x. x \<in> {a<..<b} \<Longrightarrow> bounded_linear (\<lambda>u. u *\<^sub>R f' x)"
-    using derf_exp by simp
-  have "\<forall>x \<in> box 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)"
-    (is "\<forall>x \<in> box a b. ?Q x")
-  proof
-    fix x assume x: "x \<in> box a b"
-    show "?Q x"
-      apply (rule allE [where x="e/2", OF derf_exp [THEN conjunct2, of x]])
-      using x e by auto
-  qed
-  from this [unfolded bgauge_existence_lemma]
-  obtain d where d: "\<And>x. 0 < d x"
-    "\<And>x y. \<lbrakk>x \<in> box a b; norm (y-x) < d x\<rbrakk>
+  show ?thesis
+    unfolding has_integral_factor_content_real
+  proof (intro allI impI)
+    fix e :: real
+    assume e: "e > 0"
+    then have eba8: "(e * (b-a)) / 8 > 0"
+      using ab by (auto simp add: field_simps)
+    note derf_exp = derf[unfolded has_vector_derivative_def has_derivative_at_alt]
+    have bounded: "\<And>x. x \<in> {a<..<b} \<Longrightarrow> bounded_linear (\<lambda>u. u *\<^sub>R f' x)"
+      using derf_exp by simp
+    have "\<forall>x \<in> box 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)"
+      (is "\<forall>x \<in> box a b. ?Q x")
+    proof
+      fix x assume x: "x \<in> box a b"
+      show "?Q x"
+        apply (rule allE [where x="e/2", OF derf_exp [THEN conjunct2, of x]])
+        using x e by auto
+    qed
+    from this [unfolded bgauge_existence_lemma]
+    obtain d where d: "\<And>x. 0 < d x"
+      "\<And>x y. \<lbrakk>x \<in> box a b; norm (y-x) < d x\<rbrakk>
                \<Longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e/2 * norm (y-x)"
-    by metis
-  have "bounded (f ` cbox a b)"
-    apply (rule compact_imp_bounded compact_continuous_image)+
-    using compact_cbox assms by auto
-  then obtain B 
-    where "0 < B" and B: "\<And>x. x \<in> f ` cbox a b \<Longrightarrow> norm x \<le> B"
-    unfolding bounded_pos by metis
-  obtain da where "0 < da"
-    and da: "\<And>c. \<lbrakk>a \<le> c; {a..c} \<subseteq> {a..b}; {a..c} \<subseteq> ball a da\<rbrakk>
-                          \<Longrightarrow> norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \<le> (e * (b - a)) / 4"
-  proof -
-    have "continuous (at a within {a..b}) f"
-      using contf continuous_on_eq_continuous_within by force
-    with eba8 obtain k where "0 < k"
-      and k: "\<And>x. \<lbrakk>x \<in> {a..b}; 0 < norm (x-a); norm (x-a) < k\<rbrakk>
-                          \<Longrightarrow> norm (f x - f a) < e * (b - a) / 8"
-      unfolding continuous_within Lim_within dist_norm by metis
-    obtain l where l: "0 < l" "norm (l *\<^sub>R f' a) \<le> e * (b - a) / 8" 
-    proof (cases "f' a = 0")
-      case True with ab e that show ?thesis by auto
-    next
-      case False
-      then show ?thesis
-        apply (rule_tac l="(e * (b - a)) / 8 / norm (f' a)" in that)
-        using ab e apply (auto simp add: field_simps)
-        done
-    qed
-    have "norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \<le> e * (b - a) / 4"
-      if "a \<le> c" "{a..c} \<subseteq> {a..b}" and bmin: "{a..c} \<subseteq> ball a (min k l)" for c
+      by metis
+    have "bounded (f ` cbox a b)"
+      using compact_cbox assms by (auto simp: compact_imp_bounded compact_continuous_image)
+    then obtain B 
+      where "0 < B" and B: "\<And>x. x \<in> f ` cbox a b \<Longrightarrow> norm x \<le> B"
+      unfolding bounded_pos by metis
+    obtain da where "0 < da"
+      and da: "\<And>c. \<lbrakk>a \<le> c; {a..c} \<subseteq> {a..b}; {a..c} \<subseteq> ball a da\<rbrakk>
+                          \<Longrightarrow> norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \<le> (e * (b-a)) / 4"
     proof -
-      have minkl: "\<bar>a - x\<bar> < min k l" if "x \<in> {a..c}" for x
-        using bmin dist_real_def that by auto
-      then have lel: "\<bar>c - a\<bar> \<le> \<bar>l\<bar>"
-        using that by force
-      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)
-        have "norm ((c - a) *\<^sub>R f' a) \<le> norm (l *\<^sub>R f' a)"
-          by (auto intro: mult_right_mono [OF lel])
-        also have "... \<le> e * (b - a) / 8"
-          by (rule l)
-        finally show "norm ((c - a) *\<^sub>R f' a) \<le> e * (b - a) / 8" .
+      have "continuous (at a within {a..b}) f"
+        using contf continuous_on_eq_continuous_within by force
+      with eba8 obtain k where "0 < k"
+        and k: "\<And>x. \<lbrakk>x \<in> {a..b}; 0 < norm (x-a); norm (x-a) < k\<rbrakk> \<Longrightarrow> norm (f x - f a) < e * (b-a) / 8"
+        unfolding continuous_within Lim_within dist_norm by metis
+      obtain l where l: "0 < l" "norm (l *\<^sub>R f' a) \<le> e * (b-a) / 8" 
+      proof (cases "f' a = 0")
+        case True with ab e that show ?thesis by auto
       next
-        have "norm (f c - f a) < e * (b - a) / 8"
-        proof (cases "a = c")
-          case True then show ?thesis
-            using eba8 by auto
-        next
-          case False show ?thesis
-            by (rule k) (use minkl \<open>a \<le> c\<close> that False in auto)
-        qed
-        then show "norm (f c - f a) \<le> e * (b - a) / 8" by simp
+        case False
+        then show ?thesis
+          apply (rule_tac l="(e * (b-a)) / 8 / norm (f' a)" in that)
+          using ab e 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 \<open>a \<le> c\<close>] by auto
+      have "norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \<le> e * (b-a) / 4"
+        if "a \<le> c" "{a..c} \<subseteq> {a..b}" and bmin: "{a..c} \<subseteq> ball a (min k l)" for c
+      proof -
+        have minkl: "\<bar>a - x\<bar> < min k l" if "x \<in> {a..c}" for x
+          using bmin dist_real_def that by auto
+        then have lel: "\<bar>c - a\<bar> \<le> \<bar>l\<bar>"
+          using that by force
+        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)
+          have "norm ((c - a) *\<^sub>R f' a) \<le> norm (l *\<^sub>R f' a)"
+            by (auto intro: mult_right_mono [OF lel])
+          also have "... \<le> e * (b-a) / 8"
+            by (rule l)
+          finally show "norm ((c - a) *\<^sub>R f' a) \<le> e * (b-a) / 8" .
+        next
+          have "norm (f c - f a) < e * (b-a) / 8"
+          proof (cases "a = c")
+            case True then show ?thesis
+              using eba8 by auto
+          next
+            case False show ?thesis
+              by (rule k) (use minkl \<open>a \<le> c\<close> that False in auto)
+          qed
+          then show "norm (f c - f a) \<le> e * (b-a) / 8" by simp
+        qed
+        finally show "norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \<le> e * (b-a) / 4"
+          unfolding content_real[OF \<open>a \<le> c\<close>] by auto
+      qed
+      then show ?thesis
+        by (rule_tac da="min k l" in that) (auto simp: l \<open>0 < k\<close>)
     qed
-    then show ?thesis
-      by (rule_tac da="min k l" in that) (auto simp: l \<open>0 < k\<close>)
-  qed
-  obtain db where "0 < db"
-            and db: "\<And>c. \<lbrakk>c \<le> b; {c..b} \<subseteq> {a..b}; {c..b} \<subseteq> ball b db\<rbrakk>
-                          \<Longrightarrow> norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> (e * (b - a)) / 4"
-  proof -
-    have "continuous (at b within {a..b}) f"
-      using contf continuous_on_eq_continuous_within by force
-    with eba8 obtain k
-      where "0 < k"
-        and k: "\<And>x. \<lbrakk>x \<in> {a..b}; 0 < norm(x-b); norm(x-b) < k\<rbrakk>
-                     \<Longrightarrow> norm (f b - f x) < e * (b - a) / 8"
-      unfolding continuous_within Lim_within dist_norm norm_minus_commute by metis
-    obtain l where l: "0 < l" "norm (l *\<^sub>R f' b) \<le> (e * (b - a)) / 8"
-    proof (cases "f' b = 0")
-      case True thus ?thesis 
-        using ab e that by auto
-    next
-      case False then show ?thesis
-        apply (rule_tac l="(e * (b - a)) / 8 / norm (f' b)" in that)
-        using ab e by (auto simp add: field_simps)
-    qed
-    have "norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> e * (b - a) / 4" 
-      if "c \<le> b" "{c..b} \<subseteq> {a..b}" and bmin: "{c..b} \<subseteq> ball b (min k l)" for c
+    obtain db where "0 < db"
+      and db: "\<And>c. \<lbrakk>c \<le> b; {c..b} \<subseteq> {a..b}; {c..b} \<subseteq> ball b db\<rbrakk>
+                          \<Longrightarrow> norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> (e * (b-a)) / 4"
     proof -
-      have minkl: "\<bar>b - x\<bar> < min k l" if "x \<in> {c..b}" for x
-        using bmin dist_real_def that by auto
-      then have lel: "\<bar>b - c\<bar> \<le> \<bar>l\<bar>"
-        using that by force
-      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)
-        have "norm ((b - c) *\<^sub>R f' b) \<le> norm (l *\<^sub>R f' b)"
-          by (auto intro: mult_right_mono [OF lel])
-        also have "... \<le> e * (b - a) / 8"
-          by (rule l)
-        finally show "norm ((b - c) *\<^sub>R f' b) \<le> e * (b - a) / 8" .
+      have "continuous (at b within {a..b}) f"
+        using contf continuous_on_eq_continuous_within by force
+      with eba8 obtain k
+        where "0 < k"
+          and k: "\<And>x. \<lbrakk>x \<in> {a..b}; 0 < norm(x-b); norm(x-b) < k\<rbrakk>
+                     \<Longrightarrow> norm (f b - f x) < e * (b-a) / 8"
+        unfolding continuous_within Lim_within dist_norm norm_minus_commute by metis
+      obtain l where l: "0 < l" "norm (l *\<^sub>R f' b) \<le> (e * (b-a)) / 8"
+      proof (cases "f' b = 0")
+        case True thus ?thesis 
+          using ab e that by auto
       next
-        have "norm (f b - f c) < e * (b - a) / 8"
-        proof (cases "b = c")
-          case True with eba8 show ?thesis
-            by auto
-        next
-          case False show ?thesis
-            by (rule k) (use minkl \<open>c \<le> b\<close> that False in auto)
-        qed
-        then show "norm (f b - f c) \<le> e * (b - a) / 8" by simp
+        case False then show ?thesis
+          apply (rule_tac l="(e * (b-a)) / 8 / norm (f' b)" in that)
+          using ab e 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"
-        unfolding content_real[OF \<open>c \<le> b\<close>] by auto
+      have "norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> e * (b-a) / 4" 
+        if "c \<le> b" "{c..b} \<subseteq> {a..b}" and bmin: "{c..b} \<subseteq> ball b (min k l)" for c
+      proof -
+        have minkl: "\<bar>b - x\<bar> < min k l" if "x \<in> {c..b}" for x
+          using bmin dist_real_def that by auto
+        then have lel: "\<bar>b - c\<bar> \<le> \<bar>l\<bar>"
+          using that by force
+        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)
+          have "norm ((b - c) *\<^sub>R f' b) \<le> norm (l *\<^sub>R f' b)"
+            by (auto intro: mult_right_mono [OF lel])
+          also have "... \<le> e * (b-a) / 8"
+            by (rule l)
+          finally show "norm ((b - c) *\<^sub>R f' b) \<le> e * (b-a) / 8" .
+        next
+          have "norm (f b - f c) < e * (b-a) / 8"
+          proof (cases "b = c")
+            case True with eba8 show ?thesis
+              by auto
+          next
+            case False show ?thesis
+              by (rule k) (use minkl \<open>c \<le> b\<close> that False in auto)
+          qed
+          then show "norm (f b - f c) \<le> e * (b-a) / 8" by simp
+        qed
+        finally show "norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> e * (b-a) / 4"
+          unfolding content_real[OF \<open>c \<le> b\<close>] by auto
+      qed
+      then show ?thesis
+        by (rule_tac db="min k l" in that) (auto simp: l \<open>0 < k\<close>)
     qed
-    then show ?thesis
-      by (rule_tac db="min k l" in that) (auto simp: l \<open>0 < k\<close>)
-  qed
-  let ?d = "(\<lambda>x. ball x (if x=a then da else if x=b then db else d x))"
-  show "?P e"
-  proof (intro exI conjI allI impI)
-    show "gauge ?d"
-      using ab \<open>db > 0\<close> \<open>da > 0\<close> d(1) by (auto intro: gauge_ball_dependent)
-  next
-    fix p
-    assume ptag: "p tagged_division_of {a..b}" and fine: "?d fine p"
-    let ?A = "{t. fst t \<in> {a, b}}"
-    note p = tagged_division_ofD[OF ptag]
-    have pA: "p = (p \<inter> ?A) \<union> (p - ?A)" "finite (p \<inter> ?A)" "finite (p - ?A)" "(p \<inter> ?A) \<inter> (p - ?A) = {}"
-      using ptag fine by auto
-    note * = additive_tagged_division_1[OF assms(1) ptag, 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
-    have non: False if xk: "(x,K) \<in> p" and "x \<noteq> a" "x \<noteq> b"
-         and less: "e * (Sup K - Inf K) / 2 < norm (content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))"
-         for x K
+    let ?d = "(\<lambda>x. ball x (if x=a then da else if x=b then db else d x))"
+    show "\<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})"
+    proof (rule exI, safe)
+      show "gauge ?d"
+        using ab \<open>db > 0\<close> \<open>da > 0\<close> d(1) by (auto intro: gauge_ball_dependent)
+    next
+      fix p
+      assume ptag: "p tagged_division_of {a..b}" and fine: "?d fine p"
+      let ?A = "{t. fst t \<in> {a, b}}"
+      note p = tagged_division_ofD[OF ptag]
+      have pA: "p = (p \<inter> ?A) \<union> (p - ?A)" "finite (p \<inter> ?A)" "finite (p - ?A)" "(p \<inter> ?A) \<inter> (p - ?A) = {}"
+        using ptag fine by auto
+      have le_xz: "\<And>w x y z::real. y \<le> z/2 \<Longrightarrow> w - x \<le> z/2 \<Longrightarrow> w + y \<le> x + z"
+        by arith
+      have non: False if xk: "(x,K) \<in> p" and "x \<noteq> a" "x \<noteq> b"
+        and less: "e * (Sup K - Inf K)/2 < norm (content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))"
+      for x K
       proof -
         obtain u v where k: "K = cbox u v"
           using p(4) xk by blast
         then have "u \<le> v" and uv: "{u, v} \<subseteq> cbox u v"
           using p(2)[OF xk] by auto
-        then have result: "e * (v - u) / 2 < norm ((v - u) *\<^sub>R f' x - (f v - f u))"
+        then have result: "e * (v - u)/2 < norm ((v - u) *\<^sub>R f' x - (f v - f u))"
           using less[unfolded k box_real interval_bounds_real content_real] by auto
         then have "x \<in> box a b"
           using p(2) p(3) \<open>x \<noteq> a\<close> \<open>x \<noteq> b\<close> xk by fastforce
@@ -3721,8 +3719,8 @@
         have xd: "norm (u - x) < d x" "norm (v - x) < d x"
           using fineD[OF fine xk] \<open>x \<noteq> a\<close> \<open>x \<noteq> b\<close> uv 
           by (auto simp add: k subset_eq dist_commute dist_real_def)
-        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)))"
+        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))"
           by (rule arg_cong[where f=norm]) (auto simp: scaleR_left.diff)
         also have "\<dots> \<le> e/2 * norm (u - x) + e/2 * norm (v - x)"
           by (metis norm_triangle_le_diff add_mono * xd)
@@ -3730,211 +3728,184 @@
           using p(2)[OF xk] by (auto simp add: field_simps k)
         also have "\<dots> < norm ((v - u) *\<^sub>R f' x - (f v - f u))"
           using result by (simp add: \<open>u \<le> v\<close>)
-        finally have "e * (v - u) / 2 < e * (v - u) / 2"
+        finally have "e * (v - u)/2 < e * (v - u)/2"
           using uv by auto
         then show False by auto
       qed
-    have "norm (\<Sum>(x, K)\<in>p - ?A. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))
+      have "norm (\<Sum>(x, K)\<in>p - ?A. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))
           \<le> (\<Sum>(x, K)\<in>p - ?A. norm (content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))))"
-      by (auto intro: sum_norm_le)
-    also have "... \<le> (\<Sum>n\<in>p - ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k) / 2)"
-      using non by (force intro: sum_mono)
-    finally have I: "norm (\<Sum>(x, k)\<in>p - ?A.
+        by (auto intro: sum_norm_le)
+      also have "... \<le> (\<Sum>n\<in>p - ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k)/2)"
+        using non by (fastforce intro: sum_mono)
+      finally have I: "norm (\<Sum>(x, k)\<in>p - ?A.
                   content k *\<^sub>R f' x - (f (Sup k) - f (Inf k)))
-             \<le> (\<Sum>n\<in>p - ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k)) / 2"
-      by (simp add: sum_divide_distrib)
-    have II: "norm (\<Sum>(x, k)\<in>p \<inter> ?A. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) -
+             \<le> (\<Sum>n\<in>p - ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k))/2"
+        by (simp add: sum_divide_distrib)
+      have II: "norm (\<Sum>(x, k)\<in>p \<inter> ?A. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) -
              (\<Sum>n\<in>p \<inter> ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k))
-             \<le> (\<Sum>n\<in>p - ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k)) / 2"
-    proof -
-      have ge0: "0 \<le> e * (Sup k - Inf k)" if xkp: "(x, k) \<in> p \<inter> ?A" for x k
+             \<le> (\<Sum>n\<in>p - ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k))/2"
       proof -
-        obtain u v where uv: "k = cbox u v"
-          by (meson Int_iff xkp p(4))
-        with p(2) that uv have "cbox u v \<noteq> {}"
-          by blast
-        then show "0 \<le> e * ((Sup k) - (Inf k))"
-          unfolding uv using e by (auto simp add: field_simps)
-      qed
-      let ?B = "\<lambda>x. {t \<in> p. fst t = x \<and> content (snd t) \<noteq> 0}"
-      let ?C = "{t \<in> p. fst t \<in> {a, b} \<and> content (snd t) \<noteq> 0}"
-      have "norm (\<Sum>(x, k)\<in>p \<inter> {t. fst t \<in> {a, b}}. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \<le> e * (b-a) / 2"
-      proof -
-        have *: "\<And>s f e. sum f s = sum f (p \<inter> ?C) \<Longrightarrow> norm (sum f (p \<inter> ?C)) \<le> e \<Longrightarrow> norm (sum f s) \<le> e"
-          by auto
-        have 1: "content K *\<^sub>R (f' (x)) - (f ((Sup K)) - f ((Inf K))) = 0"
-                if "(x,K) \<in> p \<inter> {t. fst t \<in> {a, b}} - p \<inter> ?C" for x K
+        have ge0: "0 \<le> e * (Sup k - Inf k)" if xkp: "(x, k) \<in> p \<inter> ?A" for x k
         proof -
-          have xk: "(x, K) \<in> p" and k0: "content K = 0"
-            using that by auto
-          then obtain u v where uv: "K = cbox u v"
-            using p(4) by blast
-          then have "u = v"
-            using xk k0 p(2) by force
-          then show "content K *\<^sub>R (f' (x)) - (f ((Sup K)) - f ((Inf K))) = 0"
-            using xk unfolding uv by auto
-        qed
-        have 2: "norm(\<Sum>(x,k)\<in>p \<inter> ?C. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) 
-                 \<le> e * (b - a) / 2"
-        proof -
-          have *: "p \<inter> ?C = ?B a \<union> ?B b"
+          obtain u v where uv: "k = cbox u v"
+            by (meson Int_iff xkp p(4))
+          with p(2) that uv have "cbox u v \<noteq> {}"
             by blast
-          have **: "norm (sum f s) \<le> e"
-            if "\<forall>x y. x \<in> s \<and> y \<in> s \<longrightarrow> x = y" "\<forall>x. x \<in> s \<longrightarrow> norm (f x) \<le> e" "e > 0"
-            for s f and e :: real
-          proof (cases "s = {}")
-            case True
-            with that show ?thesis by auto
-          next
-            case False
-            then obtain x where "x \<in> s"
-              by auto
-            then have "s = {x}"
-              using that(1) by auto
-            then show ?thesis
-              using \<open>x \<in> s\<close> that(2) by auto
+          then show "0 \<le> e * ((Sup k) - (Inf k))"
+            unfolding uv using e by (auto simp add: field_simps)
+        qed
+        let ?B = "\<lambda>x. {t \<in> p. fst t = x \<and> content (snd t) \<noteq> 0}"
+        let ?C = "{t \<in> p. fst t \<in> {a, b} \<and> content (snd t) \<noteq> 0}"
+        have "norm (\<Sum>(x, k)\<in>p \<inter> {t. fst t \<in> {a, b}}. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \<le> e * (b-a)/2"
+        proof -
+          have *: "\<And>S f e. sum f S = sum f (p \<inter> ?C) \<Longrightarrow> norm (sum f (p \<inter> ?C)) \<le> e \<Longrightarrow> norm (sum f S) \<le> e"
+            by auto
+          have 1: "content K *\<^sub>R (f' x) - (f ((Sup K)) - f ((Inf K))) = 0"
+            if "(x,K) \<in> p \<inter> {t. fst t \<in> {a, b}} - p \<inter> ?C" for x K
+          proof -
+            have xk: "(x,K) \<in> p" and k0: "content K = 0"
+              using that by auto
+            then obtain u v where uv: "K = cbox u v"
+              using p(4) by blast
+            then have "u = v"
+              using xk k0 p(2) by force
+            then show "content K *\<^sub>R (f' x) - (f ((Sup K)) - f ((Inf K))) = 0"
+              using xk unfolding uv by auto
           qed
-          show "norm (\<Sum>(x,k)\<in>p \<inter> ?C.
-                        content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \<le> e * (b - a) / 2"
-            apply (subst *)
-            apply (subst sum.union_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] **)
-
+          have 2: "norm(\<Sum>(x,K)\<in>p \<inter> ?C. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))  \<le> e * (b-a)/2"
           proof -
-            have pa: "\<exists>v. k = cbox a v \<and> a \<le> v" if "(a, k) \<in> p" for k
-            proof -
-              obtain u v where uv: "k = cbox u v"
-                using \<open>(a, k) \<in> p\<close> p(4) by blast
-              moreover have "u \<le> v"
-                using uv p(2)[OF that] by auto
-              moreover have "u = a"
-                using p(2) p(3) that uv by force
-              ultimately show ?thesis
-                by blast
-            qed
-            have pb: "\<exists>v. k = cbox v b \<and> b \<ge> v" if "(b, k) \<in> p" for k
-            proof -
-              obtain u v where uv: "k = cbox u v"
-                using \<open>(b, k) \<in> p\<close> p(4) by blast
-              moreover have "u \<le> v"
-                using p(2)[OF that] unfolding uv by auto
-              moreover have "v = b"
-                using p(2) p(3) that uv by force
-              ultimately show ?thesis
-                by blast
+            have norm_le: "norm (sum f S) \<le> e"
+              if "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x = y" "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> e" "e > 0"
+              for S f and e :: real
+            proof (cases "S = {}")
+              case True
+              with that show ?thesis by auto
+            next
+              case False then obtain x where "x \<in> S"
+                by auto
+              then have "S = {x}"
+                using that(1) by auto
+              then show ?thesis
+                using \<open>x \<in> S\<close> that(2) by auto
             qed
-            show "\<forall>x y. x \<in> ?B a \<and> y \<in> ?B a \<longrightarrow> x = y"
-            proof (safe; clarsimp)
-              fix x k k'
-              assume k: "(a, k) \<in> p" "(a, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
-              obtain v where v: "k = cbox a v" "a \<le> v"
-                using pa[OF k(1)] by blast
-              obtain v' where v': "k' = cbox a v'" "a \<le> v'"
-                using pa[OF k(2)] by blast              
-              let ?v = "min v v'"
-              have "box a ?v \<subseteq> k \<inter> k'"
-                unfolding v v' by (auto simp add: mem_box)
-              then have "interior (box a (min v v')) \<subseteq> interior k \<inter> interior k'"
-                using interior_Int interior_mono by blast
-              moreover have "(a + ?v)/2 \<in> box a ?v"
-                using k(3-)
-                unfolding v v' content_eq_0 not_le
-                by (auto simp add: mem_box)
-              ultimately have "(a + ?v)/2 \<in> interior k \<inter> interior k'"
-                unfolding interior_open[OF open_box] by auto
-              then have eq: "k = k'"
-                using p(5)[OF k(1-2)] by auto
-              { assume "x \<in> k" then show "x \<in> k'" unfolding eq . }
-              { assume "x \<in> k'" then show "x \<in> k" unfolding eq . }
-            qed
-
-            show "\<forall>x y. x \<in> ?B b \<and> y \<in> ?B b \<longrightarrow> x = y"
-            proof (safe; clarsimp)
-              fix x K K'
-              assume k: "(b, K) \<in> p" "(b, K') \<in> p" "content K \<noteq> 0" "content K' \<noteq> 0"
-              obtain v where v: "K = cbox v b" "v \<le> b"
-                using pb[OF k(1)] by blast
-              obtain v' where v': "K' = cbox v' b" "v' \<le> b"
-                using pb[OF k(2)] by blast 
-              let ?v = "max v v'"
-              have "box ?v b \<subseteq> K \<inter> K'"
-                unfolding v v' by (auto simp: mem_box)
-              then have "interior (box (max v v') b) \<subseteq> interior K \<inter> interior K'"
-                using interior_Int interior_mono by blast
-              moreover have " ((b + ?v)/2) \<in> box ?v b"
-                using k(3-) unfolding v v' content_eq_0 not_le by (auto simp: mem_box)
-              ultimately have " ((b + ?v)/2) \<in> interior K \<inter> interior K'"
-                unfolding interior_open[OF open_box] by auto
-              then have eq: "K = K'"
-                using p(5)[OF k(1-2)] by auto
-              { assume "x \<in> K" then show "x \<in> K'" unfolding eq . }
-              { assume "x \<in> K'" then show "x \<in> K" unfolding eq . }
+            have *: "p \<inter> ?C = ?B a \<union> ?B b"
+              by blast
+            then have "norm (\<Sum>(x,K)\<in>p \<inter> ?C. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))) =
+                       norm (\<Sum>(x,K) \<in> ?B a \<union> ?B b. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))"
+              by simp
+            also have "... = norm ((\<Sum>(x,K) \<in> ?B a. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))) + 
+                                   (\<Sum>(x,K) \<in> ?B b. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))))"
+              apply (subst sum.union_disjoint)
+              using p(1) ab e by auto
+            also have "... \<le> e * (b - a) / 4 + e * (b - a) / 4"
+            proof (rule norm_triangle_le [OF add_mono])
+              have pa: "\<exists>v. k = cbox a v \<and> a \<le> v" if "(a, k) \<in> p" for k
+                using p(2) p(3) p(4) that by fastforce
+              show "norm (\<Sum>(x,K) \<in> ?B a. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))) \<le> e * (b - a) / 4"
+              proof (intro norm_le; clarsimp)
+                fix K K'
+                assume K: "(a, K) \<in> p" "(a, K') \<in> p" and ne0: "content K \<noteq> 0" "content K' \<noteq> 0"
+                with pa obtain v v' where v: "K = cbox a v" "a \<le> v" and v': "K' = cbox a v'" "a \<le> v'"
+                  by blast
+                let ?v = "min v v'"
+                have "box a ?v \<subseteq> K \<inter> K'"
+                  unfolding v v' by (auto simp add: mem_box)
+                then have "interior (box a (min v v')) \<subseteq> interior K \<inter> interior K'"
+                  using interior_Int interior_mono by blast
+                moreover have "(a + ?v)/2 \<in> box a ?v"
+                  using ne0  unfolding v v' content_eq_0 not_le
+                  by (auto simp add: mem_box)
+                ultimately have "(a + ?v)/2 \<in> interior K \<inter> interior K'"
+                  unfolding interior_open[OF open_box] by auto
+                then show "K = K'"
+                  using p(5)[OF K] by auto
+              next
+                fix K 
+                assume K: "(a, K) \<in> p" and ne0: "content K \<noteq> 0"
+                show "norm (content c *\<^sub>R f' a - (f (Sup c) - f (Inf c))) * 4 \<le> e * (b-a)"
+                  if "(a, c) \<in> p" and ne0: "content c \<noteq> 0" for c
+                proof -
+                  obtain v where v: "c = cbox a v" and "a \<le> v"
+                    using pa[OF \<open>(a, c) \<in> p\<close>] by metis 
+                  then have "a \<in> {a..v}" "v \<le> b"
+                    using p(3)[OF \<open>(a, c) \<in> p\<close>] by auto
+                  moreover have "{a..v} \<subseteq> ball a da"
+                    using fineD[OF \<open>?d fine p\<close> \<open>(a, c) \<in> p\<close>] by (simp add: v split: if_split_asm)
+                  ultimately show ?thesis
+                    unfolding v interval_bounds_real[OF \<open>a \<le> v\<close>] box_real
+                    using da \<open>a \<le> v\<close> by auto
+                qed
+              qed (use ab e in auto)
+            next
+              have pb: "\<exists>v. k = cbox v b \<and> b \<ge> v" if "(b, k) \<in> p" for k
+                using p(2) p(3) p(4) that by fastforce
+              show "norm (\<Sum>(x,K) \<in> ?B b. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))) \<le> e * (b - a) / 4"
+              proof (intro norm_le; clarsimp)
+                fix K K'
+                assume K: "(b, K) \<in> p" "(b, K') \<in> p" and ne0: "content K \<noteq> 0" "content K' \<noteq> 0"
+                with pb obtain v v' where v: "K = cbox v b" "v \<le> b" and v': "K' = cbox v' b" "v' \<le> b"
+                  by blast
+                let ?v = "max v v'"
+                have "box ?v b \<subseteq> K \<inter> K'"
+                  unfolding v v' by (auto simp: mem_box)
+                then have "interior (box (max v v') b) \<subseteq> interior K \<inter> interior K'"
+                  using interior_Int interior_mono by blast
+                moreover have " ((b + ?v)/2) \<in> box ?v b"
+                  using ne0 unfolding v v' content_eq_0 not_le by (auto simp: mem_box)
+                ultimately have "((b + ?v)/2) \<in> interior K \<inter> interior K'"
+                  unfolding interior_open[OF open_box] by auto
+                then show "K = K'"
+                  using p(5)[OF K] by auto
+              next
+                fix K 
+                assume K: "(b, K) \<in> p" and ne0: "content K \<noteq> 0"
+                show "norm (content c *\<^sub>R f' b - (f (Sup c) - f (Inf c))) * 4 \<le> e * (b-a)"
+                  if "(b, c) \<in> p" and ne0: "content c \<noteq> 0" for c
+                proof -
+                obtain v where v: "c = cbox v b" and "v \<le> b"
+                  using \<open>(b, c) \<in> p\<close> pb by blast
+                then have "v \<ge> a""b \<in> {v.. b}"  
+                  using p(3)[OF \<open>(b, c) \<in> p\<close>] by auto
+                moreover have "{v..b} \<subseteq> ball b db"
+                  using fineD[OF \<open>?d fine p\<close> \<open>(b, c) \<in> p\<close>] box_real(2) v False by force
+                ultimately show ?thesis
+                  using db v by auto
+                qed
+              qed (use ab e in auto)
             qed
-
-            have "norm (content c *\<^sub>R f' a - (f (Sup c) - f (Inf c))) \<le> e * (b - a) / 4"
-              if "(a, c) \<in> p" and ne0: "content c \<noteq> 0" for c
-            proof -
-              obtain v where v: "c = cbox a v" and "a \<le> v"
-                using pa[OF \<open>(a, c) \<in> p\<close>] by metis 
-              then have "a \<in> {a..v}" "v \<le> b"
-                using p(3)[OF \<open>(a, c) \<in> p\<close>] by auto
-              moreover have "{a..v} \<subseteq> ball a da"
-                using fineD[OF \<open>?d fine p\<close> \<open>(a, c) \<in> p\<close>] by (simp add: v split: if_split_asm)
-              ultimately show ?thesis
-                unfolding v interval_bounds_real[OF \<open>a \<le> v\<close>] box_real
-                using da \<open>a \<le> v\<close> by auto
-            qed
-            then show "\<forall>x. x \<in> ?B a \<longrightarrow> norm ((\<lambda>(x, k). content k *\<^sub>R f' x - (f (Sup k) -
-              f (Inf k))) x) \<le> e * (b - a) / 4"
-              by auto
-
-            have "norm (content c *\<^sub>R f' b - (f (Sup c) - f (Inf c))) \<le> e * (b - a) / 4"
-              if "(b, c) \<in> p" and ne0: "content c \<noteq> 0" for c
-            proof -
-              obtain v where v: "c = cbox v b" and "v \<le> b"
-                using \<open>(b, c) \<in> p\<close> pb by blast
-              then have "v \<ge> a""b \<in> {v.. b}"  
-                using p(3)[OF \<open>(b, c) \<in> p\<close>] by auto
-              moreover have "{v..b} \<subseteq> ball b db"
-                using fineD[OF \<open>?d fine p\<close> \<open>(b, c) \<in> p\<close>] box_real(2) v False by force
-              ultimately show ?thesis
-                using db v by auto
-            qed
-            then show "\<forall>x. x \<in> ?B b \<longrightarrow> 
-                           norm ((\<lambda>(x, k). content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) x) 
-                           \<le> e * (b - a) / 4"
-              by auto
-          qed (insert p(1) ab e, auto simp add: field_simps)
+            also have "... = e * (b-a)/2"
+              by simp
+            finally show "norm (\<Sum>(x,k)\<in>p \<inter> ?C.
+                        content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \<le> e * (b-a)/2" .
+          qed
+          show "norm (\<Sum>(x, k)\<in>p \<inter> ?A. content k *\<^sub>R f' x - (f ((Sup k)) - f ((Inf k)))) \<le> e * (b-a)/2"
+            apply (rule * [OF sum.mono_neutral_right[OF pA(2)]])
+            using 1 2 by (auto simp: split_paired_all)
         qed
-        show "norm (\<Sum>(x, k)\<in>p \<inter> ?A. content k *\<^sub>R f' x - (f ((Sup k)) - f ((Inf k)))) \<le> e * (b - a) / 2"
-          apply (rule * [OF sum.mono_neutral_right[OF pA(2)]])
-          using 1 2 by (auto simp: split_paired_all)
+        also have "... = (\<Sum>n\<in>p. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k))/2"
+          unfolding sum_distrib_left[symmetric]
+          apply (subst additive_tagged_division_1[OF \<open>a \<le> b\<close> ptag])
+          by auto
+        finally have norm_le: "norm (\<Sum>(x,K)\<in>p \<inter> {t. fst t \<in> {a, b}}. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))
+                \<le> (\<Sum>n\<in>p. e * (case n of (x, K) \<Rightarrow> Sup K - Inf K))/2" .
+        have le2: "\<And>x s1 s2::real. 0 \<le> s1 \<Longrightarrow> x \<le> (s1 + s2)/2 \<Longrightarrow> x - s1 \<le> s2/2"
+          by auto
+        show ?thesis
+          apply (rule le2 [OF sum_nonneg])
+          using ge0 apply force
+          unfolding sum.union_disjoint[OF pA(2-), symmetric] pA(1)[symmetric]
+          by (metis norm_le)
       qed
-      also have "... = (\<Sum>n\<in>p. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k)) / 2"
-        unfolding sum_distrib_left[symmetric]
-        apply (subst additive_tagged_division_1[OF \<open>a \<le> b\<close> ptag])
-        by auto
-      finally have norm_le: "norm (\<Sum>(x, k)\<in>p \<inter> {t. fst t \<in> {a, b}}. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k)))
-                \<le> (\<Sum>n\<in>p. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k)) / 2" .
-      have *: "\<And>x s1 s2::real. 0 \<le> s1 \<Longrightarrow> x \<le> (s1 + s2) / 2 \<Longrightarrow> x - s1 \<le> s2 / 2"
-        by auto
-      show ?thesis
-        apply (rule * [OF sum_nonneg])
-        using ge0 apply force
-        unfolding sum.union_disjoint[OF pA(2-), symmetric] pA(1)[symmetric]
-        by (metis norm_le)
+      note * = additive_tagged_division_1[OF assms(1) ptag, symmetric]
+      have "norm (\<Sum>(x,K)\<in>p \<inter> ?A \<union> (p - ?A). content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))
+               \<le> e * (\<Sum>(x,K)\<in>p \<inter> ?A \<union> (p - ?A). Sup K - Inf K)"
+        unfolding sum_distrib_left
+        unfolding sum.union_disjoint[OF pA(2-)]
+        using le_xz norm_triangle_le I II by blast
+      then
+      show "norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f' x) - (f b - f a)) \<le> e * content {a..b}"
+        by (simp only: content_real[OF \<open>a \<le> b\<close>] *[of "\<lambda>x. x"] *[of f] sum_subtractf[symmetric] split_minus pA(1) [symmetric])
     qed
-    have "norm (\<Sum>(x,K)\<in>p \<inter> ?A \<union> (p - ?A). content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))
-               \<le> e * (\<Sum>(x,K)\<in>p \<inter> ?A \<union> (p - ?A). Sup K - Inf K)"
-      unfolding sum_distrib_left
-      unfolding sum.union_disjoint[OF pA(2-)]
-      using ** norm_triangle_le I II by blast
-    then
-    show "norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f' x) - (f b - f a)) \<le> e * content {a..b}"
-      by (simp only: content_real[OF \<open>a \<le> b\<close>] *[of "\<lambda>x. x"] *[of f] sum_subtractf[symmetric] split_minus pA(1) [symmetric])
   qed
 qed
 
@@ -3992,12 +3963,9 @@
   using vec apply (auto simp: mem_box)
   done
 
-lemma indefinite_integral_continuous_left:
+proposition indefinite_integral_continuous_left:
   fixes f:: "real \<Rightarrow> 'a::banach"
-  assumes intf: "f integrable_on {a..b}"
-    and "a < c"
-    and "c \<le> b"
-    and "e > 0"
+  assumes intf: "f integrable_on {a..b}" and "a < c" "c \<le> b" "e > 0"
   obtains d where "d > 0"
     and "\<forall>t. c - d < t \<and> t \<le> c \<longrightarrow> norm (integral {a..c} f - integral {a..t} f) < e"
 proof -
@@ -4020,14 +3988,14 @@
       using \<open>e > 0\<close> that by auto
   qed
 
+  let ?SUM = "\<lambda>p. (\<Sum>(x,K) \<in> p. content K *\<^sub>R f x)"
   have e3: "e/3 > 0"
     using \<open>e > 0\<close> by auto
   have "f integrable_on {a..c}"
     apply (rule integrable_subinterval_real[OF intf])
     using \<open>a < c\<close> \<open>c \<le> b\<close> by auto
   then obtain d1 where "gauge d1" and d1:
-    "\<And>p. \<lbrakk>p tagged_division_of {a..c}; d1 fine p\<rbrakk> \<Longrightarrow>
-            norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f x) - integral {a..c} f) < e/3"
+    "\<And>p. \<lbrakk>p tagged_division_of {a..c}; d1 fine p\<rbrakk> \<Longrightarrow> norm (?SUM p - integral {a..c} f) < e/3"
     using integrable_integral has_integral_real e3 by metis
   define d where [abs_def]: "d x = ball x w \<inter> d1 x" for x
   have "gauge d"
@@ -4035,132 +4003,102 @@
   then obtain k where "0 < k" and k: "ball c k \<subseteq> d c"
     by (meson gauge_def open_contains_ball)
 
-  let ?d = "min k (c - a) / 2"
-  show ?thesis
-    apply (rule that[of ?d])
-    apply safe
-  proof -
+  let ?d = "min k (c - a)/2"
+  show thesis
+  proof (intro that[of ?d] allI impI, safe)
     show "?d > 0"
-      using \<open>0 < k\<close> using assms(2) by auto
+      using \<open>0 < k\<close> \<open>a < c\<close> by auto
+  next
     fix t
-    assume as: "c - ?d < t" "t \<le> c"
-    let ?thesis = "norm (integral ({a..c}) f - integral ({a..t}) f) < e"
-    {
-      presume *: "t < c \<Longrightarrow> ?thesis"
-      show ?thesis
-      proof (cases "t = c")
-        case True
-        then show ?thesis
-          by (simp add: \<open>e > 0\<close>)
-      next
-        case False
-        then show ?thesis
-          using "*" \<open>t \<le> c\<close> by linarith
-      qed
-    }
-    assume "t < c"
-
-    have "f integrable_on {a..t}"
-      apply (rule integrable_subinterval_real[OF intf])
-      using \<open>t < c\<close> \<open>c \<le> b\<close> by auto
-    then obtain d2 where d2: "gauge d2"
-      "\<And>p. p tagged_division_of {a..t} \<and> d2 fine p \<Longrightarrow>
-            norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f x) - integral {a..t} f) < e/3"
-      using integrable_integral has_integral_real e3 by metis
-    define d3 where "d3 x = (if x \<le> t then d1 x \<inter> d2 x else d1 x)" for x
-    have "gauge d3"
-      using \<open>gauge d1\<close> \<open>gauge d2\<close> unfolding d3_def gauge_def by auto
-    then obtain p where ptag: "p tagged_division_of {a..t}" and pfine: "d3 fine p"
-      by (metis box_real(2) fine_division_exists)
-    note p'=tagged_division_ofD[OF ptag]
-    have pt: "(x,k)\<in>p \<Longrightarrow> x \<le> t" for x k
-      by (meson atLeastAtMost_iff p'(2) p'(3) subsetCE)
-    with pfine have "d2 fine p"
-      unfolding fine_def d3_def by fastforce
-    then have d2_fin: "norm ((\<Sum>(x, K)\<in>p. content K *\<^sub>R f x) - integral {a..t} f) < e/3"
-      using d2(2) ptag by auto
-    have *: "{a..c} \<inter> {x. x \<le> t} = {a..t}" "{a..c} \<inter> {x. x \<ge> t} = {t..c}"
-      using as by (auto simp add: field_simps)
-
-    have "p \<union> {(c, {t..c})} tagged_division_of {a..c}"
-      apply (rule tagged_division_Un_interval_real[of _ _ _ 1 "t"])
-      using  \<open>t \<le> c\<close> by (auto simp: * ptag tagged_division_of_self_real)
-    moreover
-    have "d1 fine p \<union> {(c, {t..c})}"
-      unfolding fine_def
-    proof safe
-      fix x K y
-      assume "(x,K) \<in> p" and "y \<in> K" then show "y \<in> d1 x"
-        by (metis Int_iff d3_def subsetD fineD pfine)
+    assume t: "c - ?d < t" "t \<le> c"
+    show "norm (integral ({a..c}) f - integral ({a..t}) f) < e"
+    proof (cases "t < c")
+      case False with \<open>t \<le> c\<close> show ?thesis
+        by (simp add: \<open>e > 0\<close>)
     next
-      fix x assume "x \<in> {t..c}"
-      then have "dist c x < k"
-        using as(1)
-        by (auto simp add: field_simps dist_real_def)
-      with k show "x \<in> d1 c"
-        unfolding d_def by auto
-    qed  
-    ultimately have d1_fin: "norm ((\<Sum>(x,K) \<in> p \<union> {(c, {t..c})}. content K *\<^sub>R f x) - integral {a..c} f) < e/3"
-      using d1 by metis
-
-    have *: "integral {a..c} f - integral {a..t} f = -(((c - t) *\<^sub>R f c + (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)) -
-      integral {a..c} f) + ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - integral {a..t} f) + (c - t) *\<^sub>R f c"
-      "e = (e/3 + e/3) + e/3"
-      by auto
-    have **: "(\<Sum>(x, k)\<in>p \<union> {(c, {t..c})}. content k *\<^sub>R f x) =
-      (c - t) *\<^sub>R f c + (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)"
-    proof -
-      have **: "\<And>x F. F \<union> {x} = insert x F"
-        by auto
-      have "(c, cbox t c) \<notin> p"
-      proof (safe, goal_cases)
-        case prems: 1
-        from p'(2-3)[OF prems] have "c \<in> cbox a t"
-          by auto
-        then show False using \<open>t < c\<close>
-          by auto
+      case True
+      have "f integrable_on {a..t}"
+        apply (rule integrable_subinterval_real[OF intf])
+        using \<open>t < c\<close> \<open>c \<le> b\<close> by auto
+      then obtain d2 where d2: "gauge d2"
+        "\<And>p. p tagged_division_of {a..t} \<and> d2 fine p \<Longrightarrow> norm (?SUM p - integral {a..t} f) < e/3"
+        using integrable_integral has_integral_real e3 by metis
+      define d3 where "d3 x = (if x \<le> t then d1 x \<inter> d2 x else d1 x)" for x
+      have "gauge d3"
+        using \<open>gauge d1\<close> \<open>gauge d2\<close> unfolding d3_def gauge_def by auto
+      then obtain p where ptag: "p tagged_division_of {a..t}" and pfine: "d3 fine p"
+        by (metis box_real(2) fine_division_exists)
+      note p' = tagged_division_ofD[OF ptag]
+      have pt: "(x,K)\<in>p \<Longrightarrow> x \<le> t" for x K
+        by (meson atLeastAtMost_iff p'(2) p'(3) subsetCE)
+      with pfine have "d2 fine p"
+        unfolding fine_def d3_def by fastforce
+      then have d2_fin: "norm (?SUM p - integral {a..t} f) < e/3"
+        using d2(2) ptag by auto
+      have eqs: "{a..c} \<inter> {x. x \<le> t} = {a..t}" "{a..c} \<inter> {x. x \<ge> t} = {t..c}"
+        using t by (auto simp add: field_simps)
+      have "p \<union> {(c, {t..c})} tagged_division_of {a..c}"
+        apply (rule tagged_division_Un_interval_real[of _ _ _ 1 "t"])
+        using  \<open>t \<le> c\<close> by (auto simp: eqs ptag tagged_division_of_self_real)
+      moreover
+      have "d1 fine p \<union> {(c, {t..c})}"
+        unfolding fine_def
+      proof safe
+        fix x K y
+        assume "(x,K) \<in> p" and "y \<in> K" then show "y \<in> d1 x"
+          by (metis Int_iff d3_def subsetD fineD pfine)
+      next
+        fix x assume "x \<in> {t..c}"
+        then have "dist c x < k"
+          using t(1) by (auto simp add: field_simps dist_real_def)
+        with k show "x \<in> d1 c"
+          unfolding d_def by auto
+      qed  
+      ultimately have d1_fin: "norm (?SUM(p \<union> {(c, {t..c})}) - integral {a..c} f) < e/3"
+        using d1 by metis
+      have SUMEQ: "?SUM(p \<union> {(c, {t..c})}) = (c - t) *\<^sub>R f c + ?SUM p"
+      proof -
+        have "?SUM(p \<union> {(c, {t..c})}) = (content{t..c} *\<^sub>R f c) + ?SUM p"
+        proof (subst sum.union_disjoint)
+          show "p \<inter> {(c, {t..c})} = {}"
+            using \<open>t < c\<close> pt by force
+        qed (use p'(1) in auto)
+        also have "... = (c - t) *\<^sub>R f c + ?SUM p"
+          using \<open>t \<le> c\<close> by auto
+        finally show ?thesis .
       qed
-      then show ?thesis
-        unfolding ** box_real
-        apply -
-        apply (subst sum.insert)
-        apply (rule p')
-        unfolding split_conv
-        defer
-        apply (subst content_real)
-        using as(2)
-        apply auto
-        done
-    qed
-    have ***: "c - w < t \<and> t < c"
-    proof -
       have "c - k < t"
-        using \<open>k>0\<close> as(1) by (auto simp add: field_simps)
+        using \<open>k>0\<close> t(1) by (auto simp add: field_simps)
       moreover have "k \<le> w"
-        apply (rule ccontr)
-        using k
-        unfolding subset_eq
-        apply (erule_tac x="c + ((k + w)/2)" in ballE)
-        unfolding d_def
-        using \<open>k > 0\<close> \<open>w > 0\<close>
-        apply (auto simp add: field_simps not_le not_less dist_real_def)
-        done
-      ultimately show ?thesis using \<open>t < c\<close>
+      proof (rule ccontr)
+        assume "\<not> k \<le> w"
+        then have "c + (k + w) / 2 \<notin> d c"
+          by (auto simp add: field_simps not_le not_less dist_real_def d_def)
+        then have "c + (k + w) / 2 \<notin> ball c k"
+          using k by blast
+        then show False
+          using \<open>0 < w\<close> \<open>\<not> k \<le> w\<close> dist_real_def by auto
+      qed
+      ultimately have cwt: "c - w < t"
         by (auto simp add: field_simps)
+      have eq: "integral {a..c} f - integral {a..t} f = -(((c - t) *\<^sub>R f c + ?SUM p) -
+             integral {a..c} f) + (?SUM p - integral {a..t} f) + (c - t) *\<^sub>R f c"
+        by auto
+      have "norm (integral {a..c} f - integral {a..t} f) < e/3 + e/3 + e/3"
+        unfolding eq
+      proof (intro norm_triangle_lt add_strict_mono)
+        show "norm (- ((c - t) *\<^sub>R f c + ?SUM p - integral {a..c} f)) < e/3"
+          by (metis SUMEQ d1_fin norm_minus_cancel)
+        show "norm (?SUM p - integral {a..t} f) < e/3"
+          using d2_fin by blast
+        show "norm ((c - t) *\<^sub>R f c) < e/3"
+          using w cwt \<open>t < c\<close> by (auto simp add: field_simps)
+      qed
+      then show ?thesis by simp
     qed
-    show ?thesis
-      unfolding *(1)
-      apply (subst *(2))
-      apply (rule norm_triangle_lt add_strict_mono)+
-      apply (metis "**" d1_fin norm_minus_cancel)
-      using d2_fin apply blast
-      using w ***
-      apply (auto simp add: field_simps)
-      done
   qed
 qed
 
-
 lemma indefinite_integral_continuous_right:
   fixes f :: "real \<Rightarrow> 'a::banach"
   assumes "f integrable_on {a..b}"
@@ -4672,10 +4610,9 @@
 
 lemma integral_nonneg:
   fixes f :: "'n::euclidean_space \<Rightarrow> real"
-  assumes "f integrable_on S"
-    and "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f x"
+  assumes f: "f integrable_on S" and 0: "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f x"
   shows "0 \<le> integral S f"
-  by (rule has_integral_nonneg[OF assms(1)[unfolded has_integral_integral] assms(2)])
+  by (rule has_integral_nonneg[OF f[unfolded has_integral_integral] 0])
 
 
 text \<open>Hence a general restriction property.\<close>
@@ -5033,11 +4970,11 @@
     if "e > 0" for e
   proof -
     have *: "e/2 > 0" using that by auto
-    then obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> norm (i - integral (?cube n) ?F) < e / 2"
+    then obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> norm (i - integral (?cube n) ?F) < e/2"
       using i[THEN LIMSEQ_D, simplified norm_minus_commute] by meson
     obtain B where "0 < B" 
       and B: "\<And>a b c d. \<lbrakk>ball 0 B \<subseteq> cbox a b; ball 0 B \<subseteq> cbox c d\<rbrakk> \<Longrightarrow>
-                  norm (integral (cbox a b) ?F - integral (cbox c d) ?F) < e / 2"
+                  norm (integral (cbox a b) ?F - integral (cbox c d) ?F) < e/2"
       using rhs * by meson
     let ?B = "max (real N) B"
     show ?thesis
@@ -6017,9 +5954,9 @@
         proof (rule *)
           show "\<bar>integral (cbox a b) (?f N) - i\<bar> < e/2"
           proof (rule abs_triangle_half_l)
-            show "\<bar>integral (cbox a b) (?f N) - integral S (f N)\<bar> < e/2 / 2"
+            show "\<bar>integral (cbox a b) (?f N) - integral S (f N)\<bar> < e/2/2"
               using B[OF ab] by simp
-            show "abs (i - integral S (f N)) < e/2 / 2"
+            show "abs (i - integral S (f N)) < e/2/2"
               using N by (simp add: abs_minus_commute)
           qed
           show "\<bar>integral (cbox a b) (?f (M + N)) - integral (cbox a b) ?g\<bar> < e/2"
@@ -6953,7 +6890,7 @@
         also have "norm (t1 - x1, t2 - x2) < k"
           using xuvwz ls uwvz_sub unfolding ball_def
           by (force simp add: cbox_Pair_eq dist_norm )
-        finally have "norm (f (x1,x2) - f (t1,t2)) \<le> e/content ?CBOX / 2"
+        finally have "norm (f (x1,x2) - f (t1,t2)) \<le> e/content ?CBOX/2"
           using nf [OF t x]  by simp
       } note nf' = this
       have f_int_uwvz: "f integrable_on cbox (u,w) (v,z)"
@@ -6962,9 +6899,9 @@
         using assms continuous_on_subset uwvz_sub
         by (blast intro: continuous_on_imp_integrable_on_Pair1)
       have 1: "norm (integral (cbox (u,w) (v,z)) f - integral (cbox (u,w) (v,z)) (\<lambda>x. f (t1,t2)))
-         \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
+         \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX/2"
         apply (simp only: integral_diff [symmetric] f_int_uwvz integrable_const)
-        apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX / 2"]])
+        apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX/2"]])
         using cbp \<open>0 < e/content ?CBOX\<close> nf'
         apply (auto simp: integrable_diff f_int_uwvz integrable_const)
         done
@@ -6973,24 +6910,24 @@
       have normint_wz:
          "\<And>x. x \<in> cbox u v \<Longrightarrow>
                norm (integral (cbox w z) (\<lambda>y. f (x, y)) - integral (cbox w z) (\<lambda>y. f (t1, t2)))
-               \<le> e * content (cbox w z) / content (cbox (a, c) (b, d)) / 2"
+               \<le> e * content (cbox w z) / content (cbox (a, c) (b, d))/2"
         apply (simp only: integral_diff [symmetric] f_int_uv integrable_const)
-        apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX / 2"]])
+        apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX/2"]])
         using cbp \<open>0 < e/content ?CBOX\<close> nf'
         apply (auto simp: integrable_diff f_int_uv integrable_const)
         done
       have "norm (integral (cbox u v)
                (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y)) - integral (cbox w z) (\<lambda>y. f (t1,t2))))
-            \<le> e * content (cbox w z) / content ?CBOX / 2 * content (cbox u v)"
+            \<le> e * content (cbox w z) / content ?CBOX/2 * content (cbox u v)"
         apply (rule integrable_bound [OF _ _ normint_wz])
         using cbp \<open>0 < e/content ?CBOX\<close>
         apply (auto simp: divide_simps content_pos_le integrable_diff int_integrable integrable_const)
         done
-      also have "... \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
+      also have "... \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX/2"
         by (simp add: content_Pair divide_simps)
       finally have 2: "norm (integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y))) -
                       integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (t1,t2))))
-                \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
+                \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX/2"
         by (simp only: integral_diff [symmetric] int_integrable integrable_const)
       have norm_xx: "\<lbrakk>x' = y'; norm(x - x') \<le> e/2; norm(y - y') \<le> e/2\<rbrakk> \<Longrightarrow> norm(x - y) \<le> e" for x::'c and y x' y' e
         using norm_triangle_mono [of "x-y'" "e/2" "y'-y" "e/2"] real_sum_of_halves