# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1503445133 -3600
# Node ID 307c19f24d5cf183e4a3ddcc1efde81cc59e30b7
# Parent  ffaaa83543b2b753eceb25636d9853ac415ee00f
more on the dreadful monotone_convergence_interval

diff -r ffaaa83543b2 -r 307c19f24d5c src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Aug 22 21:36:48 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Aug 23 00:38:53 2017 +0100
@@ -458,7 +458,7 @@
     obtain M where M:
       "M > 0"
       "\<And>a b. ball 0 M \<subseteq> cbox a b \<Longrightarrow>
-        \<exists>z. ((\<lambda>x. if x \<in> S then f x else 0) has_integral z) (cbox a b) \<and> norm (z - y) < e / B"
+        \<exists>z. ((\<lambda>x. if x \<in> S then f x else 0) has_integral z) (cbox a b) \<and> norm (z - y) < e/B"
       using has_integral_altD[OF assms(1) as *] by blast
     show "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
       (\<exists>z. ((\<lambda>x. if x \<in> S then (h \<circ> f) x else 0) has_integral z) (cbox a b) \<and> norm (z - h y) < e)"
@@ -466,7 +466,7 @@
       case prems: (1 a b)
       obtain z where z:
         "((\<lambda>x. if x \<in> S then f x else 0) has_integral z) (cbox a b)"
-        "norm (z - y) < e / B"
+        "norm (z - y) < e/B"
         using M(2)[OF prems(1)] by blast
       have *: "(\<lambda>x. if x \<in> S then (h \<circ> f) x else 0) = h \<circ> (\<lambda>x. if x \<in> S then f x else 0)"
         using zero by auto
@@ -5927,19 +5927,19 @@
     and "\<And>p. \<lbrakk>p tagged_partial_division_of (cbox a b); \<gamma> fine p\<rbrakk> \<Longrightarrow>
              sum (\<lambda>(x,k). norm(content k *\<^sub>R f x - integral k f)) p < e"
 proof -
-  have *: "e / (2 * (real DIM('n) + 1)) > 0" using \<open>e > 0\<close> by simp
+  have *: "e/(2 * (real DIM('n) + 1)) > 0" using \<open>e > 0\<close> by simp
   with integrable_integral[OF intf, unfolded has_integral]
   obtain \<gamma> where "gauge \<gamma>"
     and \<gamma>: "\<And>p. \<lbrakk>p tagged_division_of cbox a b; \<gamma> fine p\<rbrakk> \<Longrightarrow>
          norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f x) - integral (cbox a b) f)
-         < e / (2 * (real DIM('n) + 1))"
+         < e/(2 * (real DIM('n) + 1))"
     by metis
   show thesis
   proof (rule that [OF \<open>gauge \<gamma>\<close>])
     fix p
     assume p: "p tagged_partial_division_of cbox a b" "\<gamma> fine p"
     have "(\<Sum>(x,K)\<in>p. norm (content K *\<^sub>R f x - integral K f)) 
-          \<le> 2 * real DIM('n) * (e / (2 * (real DIM('n) + 1)))"
+          \<le> 2 * real DIM('n) * (e/(2 * (real DIM('n) + 1)))"
       using henstock_lemma_part2[OF intf * \<open>gauge \<gamma>\<close> \<gamma> p] by metis
     also have "... < e"
       using \<open>e > 0\<close> by (auto simp add: field_simps)
@@ -5993,21 +5993,21 @@
   then have i': "\<And>k. (integral(cbox a b) (f k)) \<le> i\<bullet>1"
     using Lim_component_ge [OF i] trivial_limit_sequentially by blast
   have "(g has_integral i) (cbox a b)"
-    unfolding has_integral
+    unfolding has_integral real_norm_def
   proof clarify
     fix e::real
     assume e: "e > 0"
     have "\<And>k. (\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
-      norm ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R f k x) - integral (cbox a b) (f k)) < e/2 ^ (k + 2)))"
+      abs ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R f k x) - integral (cbox a b) (f k)) < e/2 ^ (k + 2)))"
       using intf e by (auto simp: has_integral_integral has_integral)
     then obtain c where c:
           "\<And>x. gauge (c x)"
           "\<And>x p. \<lbrakk>p tagged_division_of cbox a b; c x fine p\<rbrakk> \<Longrightarrow>
-              norm ((\<Sum>(u, ka)\<in>p. content ka *\<^sub>R f x u) - integral (cbox a b) (f x))
-              < e / 2 ^ (x + 2)"
+              abs ((\<Sum>(u, ka)\<in>p. content ka *\<^sub>R f x u) - integral (cbox a b) (f x))
+              < e/2 ^ (x + 2)"
       by metis
 
-    have "\<exists>r. \<forall>k\<ge>r. 0 \<le> i\<bullet>1 - (integral (cbox a b) (f k)) \<and> i\<bullet>1 - (integral (cbox a b) (f k)) < e / 4"
+    have "\<exists>r. \<forall>k\<ge>r. 0 \<le> i\<bullet>1 - (integral (cbox a b) (f k)) \<and> i\<bullet>1 - (integral (cbox a b) (f k)) < e/4"
     proof -
       have "e/4 > 0"
         using e by auto
@@ -6015,33 +6015,33 @@
         using LIMSEQ_D [OF i \<open>e/4 > 0\<close>] i' by auto
     qed
     then obtain r where r: "\<And>k. r \<le> k \<Longrightarrow> 0 \<le> i \<bullet> 1 - integral (cbox a b) (f k)"
-                       "\<And>k. r \<le> k \<Longrightarrow> i \<bullet> 1 - integral (cbox a b) (f k) < e / 4" 
+                       "\<And>k. r \<le> k \<Longrightarrow> i \<bullet> 1 - integral (cbox a b) (f k) < e/4" 
       by metis
-    have "\<exists>n\<ge>r. \<forall>k\<ge>n. 0 \<le> (g x)\<bullet>1 - (f k x)\<bullet>1 \<and> (g x)\<bullet>1 - (f k x)\<bullet>1 < e / (4 * content(cbox a b))"
+    have "\<exists>n\<ge>r. \<forall>k\<ge>n. 0 \<le> (g x)\<bullet>1 - (f k x)\<bullet>1 \<and> (g x)\<bullet>1 - (f k x)\<bullet>1 < e/(4 * content(cbox a b))"
       if "x \<in> cbox a b" for x
     proof -
-      have "e / (4 * content (cbox a b)) > 0"
+      have "e/(4 * content (cbox a b)) > 0"
         by (simp add: False content_lt_nz e)
       with fg that LIMSEQ_D
-      obtain N where "\<forall>n\<ge>N. norm (f n x - g x) < e / (4 * content (cbox a b))"
+      obtain N where "\<forall>n\<ge>N. norm (f n x - g x) < e/(4 * content (cbox a b))"
         by metis
       then show "\<exists>n\<ge>r.
             \<forall>k\<ge>n.
                0 \<le> g x \<bullet> 1 - f k x \<bullet> 1 \<and>
                g x \<bullet> 1 - f k x \<bullet> 1
-               < e / (4 * content (cbox a b))"
+               < e/(4 * content (cbox a b))"
         apply (rule_tac x="N + r" in exI)
         using fg1[OF that] apply (auto simp add: field_simps)
         done
     qed
     then obtain m where r_le_m: "\<And>x. x \<in> cbox a b \<Longrightarrow> r \<le> m x"
        and m: "\<And>x k. \<lbrakk>x \<in> cbox a b; m x \<le> k\<rbrakk>
-                     \<Longrightarrow> 0 \<le> g x \<bullet> 1 - f k x \<bullet> 1 \<and> g x \<bullet> 1 - f k x \<bullet> 1 < e / (4 * content (cbox a b))"
+                     \<Longrightarrow> 0 \<le> g x \<bullet> 1 - f k x \<bullet> 1 \<and> g x \<bullet> 1 - f k x \<bullet> 1 < e/(4 * content (cbox a b))"
       by metis
     define d where "d x = c (m x) x" for x
     show "\<exists>\<gamma>. gauge \<gamma> \<and>
              (\<forall>p. p tagged_division_of cbox a b \<and>
-                  \<gamma> fine p \<longrightarrow> norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R g x) - i) < e)"
+                  \<gamma> fine p \<longrightarrow> abs ((\<Sum>(x,K)\<in>p. content K *\<^sub>R g x) - i) < e)"
     proof (rule exI, safe)
       show "gauge d"
         using c(1) unfolding gauge_def d_def by auto
@@ -6051,26 +6051,18 @@
       note p'=tagged_division_ofD[OF p(1)]
       obtain s where s: "\<And>x. x \<in> p \<Longrightarrow> m (fst x) \<le> s"
         by (metis finite_imageI finite_nat_set_iff_bounded_le p'(1) rev_image_eqI)
-      have *: "\<forall>a b c d. norm(a - b) \<le> e / 4 \<and> norm(b - c) < e/2 \<and>
-        norm (c - d) < e / 4 \<longrightarrow> norm (a - d) < e"
-      proof (safe, goal_cases)
-        case (1 a b c d)
-        then show ?case
-          using norm_triangle_lt[of "a - b" "b - c" "3* e/4"]
-            norm_triangle_lt[of "a - b + (b - c)" "c - d" e]
-          unfolding norm_minus_cancel
-          by (auto simp add: algebra_simps)
-      qed
-      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - i) < e"
-        apply (rule *[rule_format,where
-          b="\<Sum>(x, k)\<in>p. content k *\<^sub>R f (m x) x" and c="\<Sum>(x, k)\<in>p. integral k (f (m x))"])
-      proof (safe, goal_cases)
-        case 1
-        show ?case
-          apply (rule order_trans[of _ "\<Sum>(x, k)\<in>p. content k * (e / (4 * content (cbox a b)))"])
+      have *: "\<bar>a - d\<bar> < e" if "\<bar>a - b\<bar> \<le> e/4" "\<bar>b - c\<bar> < e/2" "\<bar>c - d\<bar> < e/4" for a b c d
+        using that norm_triangle_lt[of "a - b" "b - c" "3* e/4"]
+          norm_triangle_lt[of "a - b + (b - c)" "c - d" e]
+        by (auto simp add: algebra_simps)
+      show "abs ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - i) < e"
+      proof (rule *)
+        show "\<bar>(\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - (\<Sum>(x, K)\<in>p. content K *\<^sub>R f (m x) x)\<bar>
+              \<le> e/4"
+          apply (rule order_trans[of _ "\<Sum>(x, k)\<in>p. content k * (e/(4 * content (cbox a b)))"])
           unfolding sum_subtractf[symmetric]
           apply (rule order_trans)
-          apply (rule norm_sum)
+          apply (rule sum_abs)
           apply (rule sum_mono)
           unfolding split_paired_all split_conv
           unfolding split_def sum_distrib_right[symmetric] scaleR_diff_right[symmetric]
@@ -6081,64 +6073,57 @@
           then have x: "x \<in> cbox a b"
             using p'(2-3)[OF xk] by auto
           with p'(4)[OF xk] obtain u v where "K = cbox u v" by metis
-          then show "norm (content K *\<^sub>R (g x - f (m x) x)) \<le> content K * (e / (4 * content (cbox a b)))"
-            unfolding norm_scaleR using m[OF x]
-            by (metis abs_of_nonneg inner_real_def less_eq_real_def measure_nonneg mult.right_neutral mult_left_mono order_refl real_norm_def)
+          then show "abs (content K *\<^sub>R (g x - f (m x) x)) \<le> content K * (e/(4 * content (cbox a b)))"
+            unfolding abs_scaleR using m[OF x]
+            by (metis real_inner_1_right real_scaleR_def abs_of_nonneg inner_real_def less_eq_real_def measure_nonneg mult_left_mono order_refl)
         qed (insert False, auto)
 
       next
-        case 2
-        show ?case
-          apply (rule le_less_trans[of _ "norm (\<Sum>j = 0..s.
-            \<Sum>(x, K)\<in>{xk\<in>p. m (fst xk) = j}. content K *\<^sub>R f (m x) x - integral K (f (m x)))"])
+        have "norm ((\<Sum>(x, K)\<in>p. content K *\<^sub>R f (m x) x) - (\<Sum>(x, k)\<in>p. integral k (f (m x))))
+              \<le> norm
+                  (\<Sum>j = 0..s.
+                      \<Sum>(x, K)\<in>{xk \<in> p. m (fst xk) = j}.
+                        content K *\<^sub>R f (m x) x - integral K (f (m x)))"
           apply (subst sum_group)
-          apply fact
-          apply (rule finite_atLeastAtMost)
-          defer
-          apply (subst split_def)+
-          unfolding sum_subtractf
-          apply rule
+          using s by (auto simp: sum_subtractf split_def p'(1))
+        also have "\<dots> < e/2"
         proof -
-          show "norm (\<Sum>j = 0..s. \<Sum>(x, k)\<in>{xk \<in> p.
-            m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x))) < e/2"
-            apply (rule le_less_trans[of _ "sum (\<lambda>i. e/2^(i+2)) {0..s}"])
-            apply (rule sum_norm_le)
-          proof -
-            show "(\<Sum>i = 0..s. e/2 ^ (i + 2)) < e/2"
-              unfolding power_add divide_inverse inverse_mult_distrib
-              unfolding sum_distrib_left[symmetric] sum_distrib_right[symmetric]
-              unfolding power_inverse [symmetric] sum_gp
-              apply(rule mult_strict_left_mono[OF _ e])
-              unfolding power2_eq_square
-              apply auto
-              done
+          have "norm (\<Sum>j = 0..s. \<Sum>(x, k)\<in>{xk \<in> p. m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x)))
+                \<le> (\<Sum>i = 0..s. e/2 ^ (i + 2))"
+          proof (rule sum_norm_le)
             fix t
             assume "t \<in> {0..s}"
             have "norm (\<Sum>(x,k)\<in>{xk \<in> p. m (fst xk) = t}. content k *\<^sub>R f (m x) x - integral k (f (m x))) =
                   norm (\<Sum>(x,k)\<in>{xk \<in> p. m (fst xk) = t}. content k *\<^sub>R f t x - integral k (f t))"
               by (force intro!: sum.cong arg_cong[where f=norm])
             also have "... \<le> e/2 ^ (t + 2)"
-            proof (rule henstock_lemma_part1 [OF intf _ c])
+            proof (rule henstock_lemma_part1 [OF intf])
               show "{xk \<in> p. m (fst xk) = t} tagged_partial_division_of cbox a b"
                 apply (rule tagged_partial_division_subset[of p])
                 using p by (auto simp: tagged_division_of_def)
               show "c t fine {xk \<in> p. m (fst xk) = t}"
                 using p(2) by (auto simp: fine_def d_def)
-            qed (auto simp: e)
-            finally show "norm (\<Sum>(x, k)\<in>{xk \<in> p. m (fst xk) = t}. content k *\<^sub>R f (m x) x -
-              integral k (f (m x))) \<le> e/2 ^ (t + 2)" .
+            qed (use c e in auto)
+            finally show "norm (\<Sum>(x,K)\<in>{xk \<in> p. m (fst xk) = t}. content K *\<^sub>R f (m x) x -
+                                integral K (f (m x))) \<le> e/2 ^ (t + 2)" .
           qed
-        qed (insert s, auto)
+          also have "... = (e/2/2) * (\<Sum>i = 0..s. (1/2) ^ i)"
+            by (simp add: sum_distrib_left field_simps)
+          also have "\<dots> < e/2"
+            by (simp add: sum_gp mult_strict_left_mono[OF _ e])
+          finally show "norm (\<Sum>j = 0..s. \<Sum>(x, k)\<in>{xk \<in> p.
+            m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x))) < e/2" .
+        qed 
+        finally show "\<bar>(\<Sum>(x,K)\<in>p. content K *\<^sub>R f (m x) x) - (\<Sum>(x,K)\<in>p. integral K (f (m x)))\<bar> < e/2"
+          by simp
       next
-        case 3
         note comb = integral_combine_tagged_division_topdown[OF assms(1)[rule_format] p(1)]
-        have *: "\<And>sr sx ss ks kr::real. kr = sr \<longrightarrow> ks = ss \<longrightarrow>
-          ks \<le> i \<and> sr \<le> sx \<and> sx \<le> ss \<and> 0 \<le> i\<bullet>1 - kr\<bullet>1 \<and> i\<bullet>1 - kr\<bullet>1 < e/4 \<longrightarrow> \<bar>sx - i\<bar> < e/4"
+        have *: "\<And>sr sx ss ks kr. \<lbrakk>kr = sr; ks = ss;
+          ks \<le> i; sr \<le> sx; sx \<le> ss; 0 \<le> i\<bullet>1 - kr\<bullet>1; i\<bullet>1 - kr\<bullet>1 < e/4\<rbrakk> \<Longrightarrow> \<bar>sx - i\<bar> < e/4"
           by auto
-        show ?case
+        show "\<bar>(\<Sum>(x, k)\<in>p. integral k (f (m x))) - i\<bar> < e/4"
           unfolding real_norm_def
-          apply (rule *[rule_format])
-          apply safe
+          apply (rule *)
           apply (rule comb[of r])
           apply (rule comb[of s])
           apply (rule i'[unfolded real_inner_1_right])
@@ -6146,15 +6131,15 @@
           unfolding split_paired_all split_conv
           apply (rule_tac[1-2] integral_le[OF ])
         proof safe
-          show "0 \<le> i\<bullet>1 - (integral (cbox a b) (f r))\<bullet>1" "i\<bullet>1 - (integral (cbox a b) (f r))\<bullet>1 < e / 4"
+          show "0 \<le> i\<bullet>1 - (integral (cbox a b) (f r))\<bullet>1" "i\<bullet>1 - (integral (cbox a b) (f r))\<bullet>1 < e/4"
             using r by auto
-          fix x k
-          assume xk: "(x, k) \<in> p"
+          fix x K
+          assume xk: "(x, K) \<in> p"
           from p'(4)[OF this] guess u v by (elim exE) note uv=this
-          show "f r integrable_on k"
-            and "f s integrable_on k"
-            and "f (m x) integrable_on k"
-            and "f (m x) integrable_on k"
+          show "f r integrable_on K"
+            and "f s integrable_on K"
+            and "f (m x) integrable_on K"
+            and "f (m x) integrable_on K"
             unfolding uv
             apply (rule_tac[!] integrable_on_subcbox[OF assms(1)[rule_format]])
             using p'(3)[OF xk]
@@ -6162,15 +6147,14 @@
             apply auto
             done
           fix y
-          assume "y \<in> k"
+          assume "y \<in> K"
           then have "y \<in> cbox a b"
             using p'(3)[OF xk] by auto
           then have *: "\<And>m n. n\<ge>m \<Longrightarrow> f m y \<le> f n y"
             using assms(2) by (auto intro: transitive_stepwise_le)
-          show "f r y \<le> f (m x) y" and "f (m x) y \<le> f s y"
-            apply (rule_tac[!] *)
+          show "f r y \<le> f (m x) y" "f (m x) y \<le> f s y"
             using s[rule_format,OF xk] r_le_m[of x] p'(2-3)[OF xk]
-            apply auto
+            apply (auto intro!: *)
             done
         qed
       qed
@@ -6249,11 +6233,11 @@
         by metis
       with int_f[of N, unfolded has_integral_integral has_integral_alt'[of "f N"]] 
       obtain B where "0 < B" and B: 
-        "\<And>a b. ball 0 B \<subseteq> cbox a b \<Longrightarrow> norm (integral (cbox a b) (?f N) - integral S (f N)) < e / 4"
-        by (meson \<open>0 < e / 4\<close>)
+        "\<And>a b. ball 0 B \<subseteq> cbox a b \<Longrightarrow> norm (integral (cbox a b) (?f N) - integral S (f N)) < e/4"
+        by (meson \<open>0 < e/4\<close>)
       have "norm (integral (cbox a b) ?g - i) < e" if  ab: "ball 0 B \<subseteq> cbox a b" for a b
       proof -
-        obtain M where M: "\<And>n. n \<ge> M \<Longrightarrow> abs (integral (cbox a b) (?f n) - integral (cbox a b) ?g) < e / 2"
+        obtain M where M: "\<And>n. n \<ge> M \<Longrightarrow> abs (integral (cbox a b) (?f n) - integral (cbox a b) ?g) < e/2"
           using \<open>e > 0\<close> g by (fastforce simp add: dest!: LIMSEQ_D [where r = "e/2"])
         have *: "\<And>\<alpha> \<beta> g. \<lbrakk>\<bar>\<alpha> - i\<bar> < e/2; \<bar>\<beta> - g\<bar> < e/2; \<alpha> \<le> \<beta>; \<beta> \<le> i\<rbrakk> \<Longrightarrow> \<bar>g - i\<bar> < e"
           unfolding real_inner_1_right by arith
@@ -6262,12 +6246,12 @@
         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"
+          show "\<bar>integral (cbox a b) (?f (M + N)) - integral (cbox a b) ?g\<bar> < e/2"
             by (metis le_add1 M[of "M + N"])
           show "integral (cbox a b) (?f N) \<le> integral (cbox a b) (?f (M + N))"
           proof (intro ballI integral_le[OF int int])
@@ -6998,8 +6982,8 @@
       by (auto simp: False content_lt_nz e)
     then obtain dd
     where dd: "\<And>x x'. \<lbrakk>x\<in>cbox (a, c) (b, d); x'\<in>cbox (a, c) (b, d); norm (x' - x) < dd\<rbrakk>
-                       \<Longrightarrow> norm (f x' - f x) \<le> e / (2 * content (cbox c d))"  "dd>0"
-      using uc [unfolded uniformly_continuous_on_def, THEN spec, of "e / (2 * content (cbox c d))"]
+                       \<Longrightarrow> norm (f x' - f x) \<le> e/(2 * content (cbox c d))"  "dd>0"
+      using uc [unfolded uniformly_continuous_on_def, THEN spec, of "e/(2 * content (cbox c d))"]
       by (auto simp: dist_norm intro: less_imp_le)
     have "\<exists>delta>0. \<forall>x'\<in>cbox a b. norm (x' - x) < delta \<longrightarrow> norm (integral (cbox c d) (\<lambda>u. f (x', u) - f (x, u))) < e"
       apply (rule_tac x=dd in exI)
@@ -7144,7 +7128,7 @@
   have "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) = 0"
   proof (rule dense_eq0_I, simp)
     fix e::real  assume "0 < e"
-    with cbp have e': "0 < e / content ?CBOX"
+    with cbp have e': "0 < e/content ?CBOX"
       by simp
     have f_int_acbd: "f integrable_on cbox (a,c) (b,d)"
       by (rule integrable_continuous [OF assms])
@@ -7164,7 +7148,7 @@
       assume k: "0 < k"
          and nf: "\<And>x y u v.
                   \<lbrakk>x \<in> cbox a b; y \<in> cbox c d; u \<in> cbox a b; v\<in>cbox c d; norm (u-x, v-y) < k\<rbrakk>
-                  \<Longrightarrow> norm (f(u,v) - f(x,y)) < e / (2 * (content ?CBOX))"
+                  \<Longrightarrow> norm (f(u,v) - f(x,y)) < e/(2 * (content ?CBOX))"
          and p_acbd: "p tagged_division_of cbox (a,c) (b,d)"
          and fine: "(\<lambda>x. ball x k) fine p"  "((t1,t2), l) \<in> p"
          and uwvz_sub: "cbox (u,w) (v,z) \<subseteq> l" "cbox (u,w) (v,z) \<subseteq> cbox (a,c) (b,d)"
@@ -7181,7 +7165,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)"
@@ -7192,7 +7176,7 @@
       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"
         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 e' nf'
         apply (auto simp: integrable_diff f_int_uwvz integrable_const)
         done
@@ -7203,7 +7187,7 @@
                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"
         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 e' nf'
         apply (auto simp: integrable_diff f_int_uv integrable_const)
         done