merged
authorpaulson
Mon Aug 28 22:32:22 2017 +0100 (22 months ago)
changeset 665401f955cdd9e59
parent 66531 d9641709f2df
parent 66539 0ad3fc48c9ec
child 66541 4d9c4cb9e9a5
child 66552 507a42c0a0ff
merged
     1.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Aug 28 21:18:47 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Aug 28 22:32:22 2017 +0100
     1.3 @@ -3617,22 +3617,24 @@
     1.4        and ge: "\<And>x. \<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> 0 \<le> Im (vector_derivative \<gamma> (at x) * cnj(\<gamma> x - z))"
     1.5      shows "0 \<le> Re(winding_number \<gamma> z)"
     1.6  proof -
     1.7 -  have *: "0 \<le> Im (vector_derivative \<gamma> (at x) / (\<gamma> x - z))" if x: "0 < x" "x < 1" for x
     1.8 +  have ge0: "0 \<le> Im (vector_derivative \<gamma> (at x) / (\<gamma> x - z))" if x: "0 < x" "x < 1" for x
     1.9      using ge by (simp add: Complex.Im_divide algebra_simps x)
    1.10 -  show ?thesis
    1.11 -    apply (simp add: Re_winding_number [OF \<gamma>] field_simps)
    1.12 +  have hi: "((\<lambda>x. 1 / (\<gamma> x - z) * vector_derivative \<gamma> (at x)) has_integral contour_integral \<gamma> (\<lambda>w. 1 / (w - z)))
    1.13 +            (cbox 0 1)"
    1.14 +    unfolding box_real
    1.15 +    apply (subst has_contour_integral [symmetric])
    1.16 +    using \<gamma> by (simp add: contour_integrable_inversediff has_contour_integral_integral)
    1.17 +  have "0 \<le> Im (contour_integral \<gamma> (\<lambda>w. 1 / (w - z)))"
    1.18      apply (rule has_integral_component_nonneg
    1.19               [of \<i> "\<lambda>x. if x \<in> {0<..<1}
    1.20                           then 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x) else 0", simplified])
    1.21 -      prefer 3 apply (force simp: *)
    1.22 +      prefer 3 apply (force simp: ge0)
    1.23       apply (simp add: Basis_complex_def)
    1.24 -    apply (rule has_integral_spike_interior [of 0 1 _ "\<lambda>x. 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x)"])
    1.25 +    apply (rule has_integral_spike_interior [OF hi])
    1.26      apply simp
    1.27 -    apply (simp only: box_real)
    1.28 -    apply (subst has_contour_integral [symmetric])
    1.29 -    using \<gamma>
    1.30 -    apply (simp add: contour_integrable_inversediff has_contour_integral_integral)
    1.31      done
    1.32 +  then show ?thesis
    1.33 +    by (simp add: Re_winding_number [OF \<gamma>] field_simps)
    1.34  qed
    1.35  
    1.36  lemma winding_number_pos_lt_lemma:
    1.37 @@ -3641,19 +3643,20 @@
    1.38        and ge: "\<And>x. \<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> e \<le> Im (vector_derivative \<gamma> (at x) / (\<gamma> x - z))"
    1.39      shows "0 < Re(winding_number \<gamma> z)"
    1.40  proof -
    1.41 +  have hi: "((\<lambda>x. 1 / (\<gamma> x - z) * vector_derivative \<gamma> (at x)) has_integral contour_integral \<gamma> (\<lambda>w. 1 / (w - z)))
    1.42 +            (cbox 0 1)"
    1.43 +    unfolding box_real
    1.44 +    apply (subst has_contour_integral [symmetric])
    1.45 +    using \<gamma> by (simp add: contour_integrable_inversediff has_contour_integral_integral)
    1.46    have "e \<le> Im (contour_integral \<gamma> (\<lambda>w. 1 / (w - z)))"
    1.47      apply (rule has_integral_component_le
    1.48               [of \<i> "\<lambda>x. \<i>*e" "\<i>*e" "{0..1}"
    1.49                      "\<lambda>x. if x \<in> {0<..<1} then 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x) else \<i>*e"
    1.50                      "contour_integral \<gamma> (\<lambda>w. 1/(w - z))", simplified])
    1.51 -    using e
    1.52 -    apply (simp_all add: Basis_complex_def)
    1.53 +    using e apply (simp_all add: Basis_complex_def)
    1.54      using has_integral_const_real [of _ 0 1] apply force
    1.55 -    apply (rule has_integral_spike_interior [of 0 1 _ "\<lambda>x. 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x)", simplified box_real])
    1.56 -    apply simp
    1.57 -    apply (subst has_contour_integral [symmetric])
    1.58 -    using \<gamma>
    1.59 -    apply (simp_all add: contour_integrable_inversediff has_contour_integral_integral ge)
    1.60 +     apply (rule has_integral_spike_interior [OF hi, simplified box_real])
    1.61 +    apply (simp_all add: ge)
    1.62      done
    1.63    with e show ?thesis
    1.64      by (simp add: Re_winding_number [OF \<gamma>] field_simps)
     2.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Aug 28 21:18:47 2017 +0200
     2.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Aug 28 22:32:22 2017 +0100
     2.3 @@ -324,7 +324,7 @@
     2.4    assumes "(f has_integral k1) i" "(f has_integral k2) i"
     2.5    shows "k1 = k2"
     2.6  proof (rule ccontr)
     2.7 -  let ?e = "norm (k1 - k2) / 2"
     2.8 +  let ?e = "norm (k1 - k2)/2"
     2.9    let ?F = "(\<lambda>x. if x \<in> i then f x else 0)"
    2.10    assume "k1 \<noteq> k2"
    2.11    then have e: "?e > 0"
    2.12 @@ -334,25 +334,25 @@
    2.13    obtain B1 where B1:
    2.14        "0 < B1"
    2.15        "\<And>a b. ball 0 B1 \<subseteq> cbox a b \<Longrightarrow>
    2.16 -        \<exists>z. (?F has_integral z) (cbox a b) \<and> norm (z - k1) < norm (k1 - k2) / 2"
    2.17 +        \<exists>z. (?F has_integral z) (cbox a b) \<and> norm (z - k1) < norm (k1 - k2)/2"
    2.18      by (rule has_integral_altD[OF assms(1) nonbox,OF e]) blast
    2.19    obtain B2 where B2:
    2.20        "0 < B2"
    2.21        "\<And>a b. ball 0 B2 \<subseteq> cbox a b \<Longrightarrow>
    2.22 -        \<exists>z. (?F has_integral z) (cbox a b) \<and> norm (z - k2) < norm (k1 - k2) / 2"
    2.23 +        \<exists>z. (?F has_integral z) (cbox a b) \<and> norm (z - k2) < norm (k1 - k2)/2"
    2.24      by (rule has_integral_altD[OF assms(2) nonbox,OF e]) blast
    2.25    obtain a b :: 'n where ab: "ball 0 B1 \<subseteq> cbox a b" "ball 0 B2 \<subseteq> cbox a b"
    2.26      by (metis Un_subset_iff bounded_Un bounded_ball bounded_subset_cbox)
    2.27 -  obtain w where w: "(?F has_integral w) (cbox a b)" "norm (w - k1) < norm (k1 - k2) / 2"
    2.28 +  obtain w where w: "(?F has_integral w) (cbox a b)" "norm (w - k1) < norm (k1 - k2)/2"
    2.29      using B1(2)[OF ab(1)] by blast
    2.30 -  obtain z where z: "(?F has_integral z) (cbox a b)" "norm (z - k2) < norm (k1 - k2) / 2"
    2.31 +  obtain z where z: "(?F has_integral z) (cbox a b)" "norm (z - k2) < norm (k1 - k2)/2"
    2.32      using B2(2)[OF ab(2)] by blast
    2.33    have "z = w"
    2.34      using has_integral_unique_cbox[OF w(1) z(1)] by auto
    2.35    then have "norm (k1 - k2) \<le> norm (z - k2) + norm (w - k1)"
    2.36      using norm_triangle_ineq4 [of "k1 - w" "k2 - z"]
    2.37      by (auto simp add: norm_minus_commute)
    2.38 -  also have "\<dots> < norm (k1 - k2) / 2 + norm (k1 - k2) / 2"
    2.39 +  also have "\<dots> < norm (k1 - k2)/2 + norm (k1 - k2)/2"
    2.40      by (metis add_strict_mono z(2) w(2))
    2.41    finally show False by auto
    2.42  qed
    2.43 @@ -1290,10 +1290,10 @@
    2.44            using mem_interior by metis
    2.45          have x: "x\<bullet>k = c"
    2.46            using x interior_subset by fastforce
    2.47 -        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)"
    2.48 +        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)"
    2.49            using \<open>0 < \<epsilon>\<close> k by (auto simp: inner_simps inner_not_same_Basis)
    2.50 -        have "(\<Sum>i\<in>Basis. \<bar>(x - (x + (\<epsilon> / 2 ) *\<^sub>R k)) \<bullet> i\<bar>) =
    2.51 -              (\<Sum>i\<in>Basis. (if i = k then \<epsilon> / 2 else 0))"
    2.52 +        have "(\<Sum>i\<in>Basis. \<bar>(x - (x + (\<epsilon>/2 ) *\<^sub>R k)) \<bullet> i\<bar>) =
    2.53 +              (\<Sum>i\<in>Basis. (if i = k then \<epsilon>/2 else 0))"
    2.54            using "*" by (blast intro: sum.cong)
    2.55          also have "\<dots> < \<epsilon>"
    2.56            by (subst sum.delta) (use \<open>0 < \<epsilon>\<close> in auto)
    2.57 @@ -1964,132 +1964,116 @@
    2.58        assume c: "c < a \<bullet> k"
    2.59        moreover have "x \<in> cbox a b \<Longrightarrow> c \<le> x \<bullet> k" for x
    2.60          using k c by (auto simp: cbox_def)
    2.61 -      ultimately have "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> (a \<bullet> k - c) / 2} = {}"
    2.62 +      ultimately have "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> (a \<bullet> k - c)/2} = {}"
    2.63          using k by (auto simp: cbox_def)
    2.64 -      with \<open>0<e\<close> c that[of "(a \<bullet> k - c) / 2"] show ?thesis
    2.65 +      with \<open>0<e\<close> c that[of "(a \<bullet> k - c)/2"] show ?thesis
    2.66          by auto
    2.67      next
    2.68        assume c: "b \<bullet> k < c"
    2.69        moreover have "x \<in> cbox a b \<Longrightarrow> x \<bullet> k \<le> c" for x
    2.70          using k c by (auto simp: cbox_def)
    2.71 -      ultimately have "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> (c - b \<bullet> k) / 2} = {}"
    2.72 +      ultimately have "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> (c - b \<bullet> k)/2} = {}"
    2.73          using k by (auto simp: cbox_def)
    2.74 -      with \<open>0<e\<close> c that[of "(c - b \<bullet> k) / 2"] show ?thesis
    2.75 +      with \<open>0<e\<close> c that[of "(c - b \<bullet> k)/2"] show ?thesis
    2.76          by auto
    2.77      qed
    2.78    qed
    2.79  qed
    2.80  
    2.81  
    2.82 -lemma negligible_standard_hyperplane[intro]:
    2.83 +proposition negligible_standard_hyperplane[intro]:
    2.84    fixes k :: "'a::euclidean_space"
    2.85    assumes k: "k \<in> Basis"
    2.86    shows "negligible {x. x\<bullet>k = c}"
    2.87    unfolding negligible_def has_integral
    2.88 -proof (clarify, goal_cases)
    2.89 -  case (1 a b e)
    2.90 -  from this and k obtain d where d: "0 < d" "content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) < e"
    2.91 -    by (rule content_doublesplit)
    2.92 +proof clarsimp
    2.93 +  fix a b and e::real assume "e > 0"
    2.94 +  with k obtain d where "0 < d" and d: "content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) < e"
    2.95 +    by (metis content_doublesplit)
    2.96    let ?i = "indicator {x::'a. x\<bullet>k = c} :: 'a\<Rightarrow>real"
    2.97 -  show ?case
    2.98 -    apply (rule_tac x="\<lambda>x. ball x d" in exI)
    2.99 -    apply rule
   2.100 -    apply (rule gauge_ball)
   2.101 -    apply (rule d)
   2.102 -  proof (rule, rule)
   2.103 -    fix p
   2.104 -    assume p: "p tagged_division_of (cbox a b) \<and> (\<lambda>x. ball x d) fine p"
   2.105 -    have *: "(\<Sum>(x, ka)\<in>p. content ka *\<^sub>R ?i x) =
   2.106 -      (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d}) *\<^sub>R ?i x)"
   2.107 -      apply (rule sum.cong)
   2.108 -      apply (rule refl)
   2.109 -      unfolding split_paired_all real_scaleR_def mult_cancel_right split_conv
   2.110 -      apply cases
   2.111 -      apply (rule disjI1)
   2.112 -      apply assumption
   2.113 -      apply (rule disjI2)
   2.114 +  show "\<exists>\<gamma>. gauge \<gamma> \<and>
   2.115 +           (\<forall>\<D>. \<D> tagged_division_of cbox a b \<and> \<gamma> fine \<D> \<longrightarrow>
   2.116 +                 \<bar>\<Sum>(x,K) \<in> \<D>. content K * ?i x\<bar> < e)"
   2.117 +  proof (intro exI, safe)
   2.118 +    show "gauge (\<lambda>x. ball x d)"
   2.119 +      using \<open>0 < d\<close> by blast
   2.120 +  next
   2.121 +    fix \<D>
   2.122 +    assume p: "\<D> tagged_division_of (cbox a b)" "(\<lambda>x. ball x d) fine \<D>"
   2.123 +    have "content L = content (L \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})" 
   2.124 +      if "(x, L) \<in> \<D>" "?i x \<noteq> 0" for x L
   2.125      proof -
   2.126 -      fix x l
   2.127 -      assume as: "(x, l) \<in> p" "?i x \<noteq> 0"
   2.128 -      then have xk: "x\<bullet>k = c"
   2.129 -        unfolding indicator_def
   2.130 -        apply -
   2.131 -        apply (rule ccontr)
   2.132 -        apply auto
   2.133 -        done
   2.134 -      show "content l = content (l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})"
   2.135 -        apply (rule arg_cong[where f=content])
   2.136 -        apply (rule set_eqI)
   2.137 -        apply rule
   2.138 -        apply rule
   2.139 -        unfolding mem_Collect_eq
   2.140 -      proof -
   2.141 +      have xk: "x\<bullet>k = c"
   2.142 +        using that by (simp add: indicator_def split: if_split_asm)
   2.143 +      have "L \<subseteq> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}"
   2.144 +      proof 
   2.145          fix y
   2.146 -        assume y: "y \<in> l"
   2.147 -        note p[THEN conjunct2,unfolded fine_def,rule_format,OF as(1),unfolded split_conv]
   2.148 -        note this[unfolded subset_eq mem_ball dist_norm,rule_format,OF y]
   2.149 -        note le_less_trans[OF Basis_le_norm[OF k] this]
   2.150 -        then show "\<bar>y \<bullet> k - c\<bar> \<le> d"
   2.151 +        assume y: "y \<in> L"
   2.152 +        have "L \<subseteq> ball x d"
   2.153 +          using p(2) that(1) by auto
   2.154 +        then have "norm (x - y) < d"
   2.155 +          by (simp add: dist_norm subset_iff y)
   2.156 +        then have "\<bar>(x - y) \<bullet> k\<bar> < d"
   2.157 +          using k norm_bound_Basis_lt by blast
   2.158 +        then show "y \<in> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}"
   2.159            unfolding inner_simps xk by auto
   2.160 -      qed auto
   2.161 +      qed 
   2.162 +      then show "content L = content (L \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})"
   2.163 +        by (metis inf.orderE)
   2.164      qed
   2.165 -    note p'= tagged_division_ofD[OF p[THEN conjunct1]] and p''=division_of_tagged_division[OF p[THEN conjunct1]]
   2.166 -    have "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * indicator {x. x \<bullet> k = c} x) < e"
   2.167 +    then have *: "(\<Sum>(x,K)\<in>\<D>. content K * ?i x) = (\<Sum>(x,K)\<in>\<D>. content (K \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d}) *\<^sub>R ?i x)"
   2.168 +      by (force simp add: split_paired_all intro!: sum.cong [OF refl])
   2.169 +    note p'= tagged_division_ofD[OF p(1)] and p''=division_of_tagged_division[OF p(1)]
   2.170 +    have "(\<Sum>(x,K)\<in>\<D>. content (K \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * indicator {x. x \<bullet> k = c} x) < e"
   2.171      proof -
   2.172 -      have "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) \<le>
   2.173 -        (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}))"
   2.174 -        apply (rule sum_mono)
   2.175 -        unfolding split_paired_all split_conv
   2.176 -        apply (rule mult_right_le_one_le)
   2.177 -        apply (drule p'(4))
   2.178 -        apply (auto simp add:interval_doublesplit[OF k])
   2.179 -        done
   2.180 +      have "(\<Sum>(x,K)\<in>\<D>. content (K \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) \<le> (\<Sum>(x,K)\<in>\<D>. content (K \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}))"
   2.181 +        by (force simp add: indicator_def intro!: sum_mono)
   2.182        also have "\<dots> < e"
   2.183 -      proof (subst sum.over_tagged_division_lemma[OF p[THEN conjunct1]], goal_cases)
   2.184 -        case prems: (1 u v)
   2.185 +      proof (subst sum.over_tagged_division_lemma[OF p(1)])
   2.186 +        fix u v::'a
   2.187 +        assume "box u v = {}"
   2.188          then have *: "content (cbox u v) = 0"
   2.189            unfolding content_eq_0_interior by simp
   2.190 -        have "content (cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<le> content (cbox u v)"
   2.191 -          unfolding interval_doublesplit[OF k]
   2.192 -          apply (rule content_subset)
   2.193 -          unfolding interval_doublesplit[symmetric,OF k]
   2.194 -          apply auto
   2.195 -          done
   2.196 -        then show ?case
   2.197 +        have "cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<subseteq> cbox u v"
   2.198 +          by auto
   2.199 +        then have "content (cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<le> content (cbox u v)"
   2.200 +          unfolding interval_doublesplit[OF k] by (rule content_subset)
   2.201 +        then show "content (cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = 0"
   2.202            unfolding * interval_doublesplit[OF k]
   2.203            by (blast intro: antisym)
   2.204        next
   2.205 -        have "(\<Sum>l\<in>snd ` p. content (l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) =
   2.206 -          sum content ((\<lambda>l. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})`{l\<in>snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}})"
   2.207 +        have "(\<Sum>l\<in>snd ` \<D>. content (l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) =
   2.208 +          sum content ((\<lambda>l. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})`{l\<in>snd ` \<D>. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}})"
   2.209          proof (subst (2) sum.reindex_nontrivial)
   2.210 -          fix x y assume "x \<in> {l \<in> snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}" "y \<in> {l \<in> snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}"
   2.211 +          fix x y assume "x \<in> {l \<in> snd ` \<D>. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}" "y \<in> {l \<in> snd ` \<D>. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}"
   2.212              "x \<noteq> y" and eq: "x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} = y \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}"
   2.213 -          then obtain x' y' where "(x', x) \<in> p" "x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}" "(y', y) \<in> p" "y \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}"
   2.214 +          then obtain x' y' where "(x', x) \<in> \<D>" "x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}" "(y', y) \<in> \<D>" "y \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}"
   2.215              by (auto)
   2.216 -          from p'(5)[OF \<open>(x', x) \<in> p\<close> \<open>(y', y) \<in> p\<close>] \<open>x \<noteq> y\<close> have "interior (x \<inter> y) = {}"
   2.217 +          from p'(5)[OF \<open>(x', x) \<in> \<D>\<close> \<open>(y', y) \<in> \<D>\<close>] \<open>x \<noteq> y\<close> have "interior (x \<inter> y) = {}"
   2.218              by auto
   2.219            moreover have "interior ((x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<inter> (y \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) \<subseteq> interior (x \<inter> y)"
   2.220              by (auto intro: interior_mono)
   2.221            ultimately have "interior (x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = {}"
   2.222              by (auto simp: eq)
   2.223            then show "content (x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = 0"
   2.224 -            using p'(4)[OF \<open>(x', x) \<in> p\<close>] by (auto simp: interval_doublesplit[OF k] content_eq_0_interior simp del: interior_Int)
   2.225 +            using p'(4)[OF \<open>(x', x) \<in> \<D>\<close>] by (auto simp: interval_doublesplit[OF k] content_eq_0_interior simp del: interior_Int)
   2.226          qed (insert p'(1), auto intro!: sum.mono_neutral_right)
   2.227 -        also have "\<dots> \<le> norm (\<Sum>l\<in>(\<lambda>l. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})`{l\<in>snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}. content l *\<^sub>R 1::real)"
   2.228 +        also have "\<dots> \<le> norm (\<Sum>l\<in>(\<lambda>l. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})`{l\<in>snd ` \<D>. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}. content l *\<^sub>R 1::real)"
   2.229            by simp
   2.230          also have "\<dots> \<le> 1 * content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})"
   2.231            using division_doublesplit[OF p'' k, unfolded interval_doublesplit[OF k]]
   2.232            unfolding interval_doublesplit[OF k] by (intro dsum_bound) auto
   2.233          also have "\<dots> < e"
   2.234 -          using d(2) by simp
   2.235 -        finally show "(\<Sum>ka\<in>snd ` p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) < e" .
   2.236 +          using d by simp
   2.237 +        finally show "(\<Sum>K\<in>snd ` \<D>. content (K \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) < e" .
   2.238        qed
   2.239 -      finally show "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) < e" .
   2.240 +      finally show "(\<Sum>(x, K)\<in>\<D>. content (K \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) < e" .
   2.241      qed
   2.242 -    then show "norm ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R ?i x) - 0) < e"
   2.243 -      unfolding * real_norm_def
   2.244 +    then show "\<bar>\<Sum>(x, K)\<in>\<D>. content K * ?i x\<bar> < e"
   2.245 +      unfolding * 
   2.246        apply (subst abs_of_nonneg)
   2.247 -      using measure_nonneg  by (force simp add: indicator_def intro: sum_nonneg)+
   2.248 +      using measure_nonneg       
   2.249 +      by (force simp add: indicator_def intro: sum_nonneg)+
   2.250    qed
   2.251  qed
   2.252  
   2.253 @@ -2194,21 +2178,21 @@
   2.254          done
   2.255        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>)"
   2.256          by (rule sum_mono) (simp add: sum_distrib_left [symmetric])
   2.257 -      also have "... \<le> (\<Sum>i\<le>N + 1. e/2 / 2 ^ i)"
   2.258 +      also have "... \<le> (\<Sum>i\<le>N + 1. e/2/2 ^ i)"
   2.259        proof (rule sum_mono)
   2.260 -        show "(real i + 1) * \<bar>\<Sum>(x,K) \<in> q i. content K *\<^sub>R indicator S x\<bar> \<le> e/2 / 2 ^ i"
   2.261 +        show "(real i + 1) * \<bar>\<Sum>(x,K) \<in> q i. content K *\<^sub>R indicator S x\<bar> \<le> e/2/2 ^ i"
   2.262            if "i \<in> {..N + 1}" for i
   2.263            using \<gamma>[of "q i" i] q by (simp add: divide_simps mult.left_commute)
   2.264        qed
   2.265 -      also have "... = e/2 * (\<Sum>i\<le>N + 1. (1 / 2) ^ i)"
   2.266 +      also have "... = e/2 * (\<Sum>i\<le>N + 1. (1/2) ^ i)"
   2.267          unfolding sum_distrib_left by (metis divide_inverse inverse_eq_divide power_one_over)
   2.268        also have "\<dots> < e/2 * 2"
   2.269        proof (rule mult_strict_left_mono)
   2.270 -        have "sum (op ^ (1 / 2)) {..N + 1} = sum (op ^ (1 / 2::real)) {..<N + 2}"
   2.271 +        have "sum (op ^ (1/2)) {..N + 1} = sum (op ^ (1/2::real)) {..<N + 2}"
   2.272            using lessThan_Suc_atMost by auto
   2.273          also have "... < 2"
   2.274            by (auto simp: geometric_sum)
   2.275 -        finally show "sum (op ^ (1 / 2::real)) {..N + 1} < 2" .
   2.276 +        finally show "sum (op ^ (1/2::real)) {..N + 1} < 2" .
   2.277        qed (use \<open>0 < e\<close> in auto)
   2.278        finally  show ?thesis by auto
   2.279      qed
   2.280 @@ -2406,47 +2390,30 @@
   2.281  lemma negligible_frontier_interval: "negligible(cbox (a::'a::euclidean_space) b - box a b)"
   2.282  proof -
   2.283    let ?A = "\<Union>((\<lambda>k. {x. x\<bullet>k = a\<bullet>k} \<union> {x::'a. x\<bullet>k = b\<bullet>k}) ` Basis)"
   2.284 -  have "cbox a b - box a b \<subseteq> ?A"
   2.285 -    apply rule unfolding Diff_iff mem_box
   2.286 -    apply simp
   2.287 -    apply(erule conjE bexE)+
   2.288 -    apply(rule_tac x=i in bexI)
   2.289 -    apply auto
   2.290 -    done
   2.291 -  then show ?thesis
   2.292 -    apply -
   2.293 -    apply (rule negligible_subset[of ?A])
   2.294 -    apply (rule negligible_Union[OF finite_imageI])
   2.295 -    apply auto
   2.296 -    done
   2.297 +  have "negligible ?A"
   2.298 +    by (force simp add: negligible_Union[OF finite_imageI])
   2.299 +  moreover have "cbox a b - box a b \<subseteq> ?A"
   2.300 +    by (force simp add: mem_box)
   2.301 +  ultimately show ?thesis
   2.302 +    by (rule negligible_subset)
   2.303  qed
   2.304  
   2.305  lemma has_integral_spike_interior:
   2.306 -  assumes "\<forall>x\<in>box a b. g x = f x"
   2.307 -    and "(f has_integral y) (cbox a b)"
   2.308 +  assumes f: "(f has_integral y) (cbox a b)" and gf: "\<And>x. x \<in> box a b \<Longrightarrow> g x = f x"
   2.309    shows "(g has_integral y) (cbox a b)"
   2.310 -  apply (rule has_integral_spike[OF negligible_frontier_interval _ assms(2)])
   2.311 -  using assms(1)
   2.312 -  apply auto
   2.313 -  done
   2.314 +  apply (rule has_integral_spike[OF negligible_frontier_interval _ f])
   2.315 +  using gf by auto
   2.316  
   2.317  lemma has_integral_spike_interior_eq:
   2.318 -  assumes "\<forall>x\<in>box a b. g x = f x"
   2.319 +  assumes "\<And>x. x \<in> box a b \<Longrightarrow> g x = f x"
   2.320    shows "(f has_integral y) (cbox a b) \<longleftrightarrow> (g has_integral y) (cbox a b)"
   2.321 -  apply rule
   2.322 -  apply (rule_tac[!] has_integral_spike_interior)
   2.323 -  using assms
   2.324 -  apply auto
   2.325 -  done
   2.326 +  by (metis assms has_integral_spike_interior)
   2.327  
   2.328  lemma integrable_spike_interior:
   2.329 -  assumes "\<forall>x\<in>box a b. g x = f x"
   2.330 +  assumes "\<And>x. x \<in> box a b \<Longrightarrow> g x = f x"
   2.331      and "f integrable_on cbox a b"
   2.332    shows "g integrable_on cbox a b"
   2.333 -  using assms
   2.334 -  unfolding integrable_on_def
   2.335 -  using has_integral_spike_interior[OF assms(1)]
   2.336 -  by auto
   2.337 +  using assms has_integral_spike_interior_eq by blast
   2.338  
   2.339  
   2.340  subsection \<open>Integrability of continuous functions.\<close>
   2.341 @@ -2727,7 +2694,7 @@
   2.342  lemma ident_has_integral:
   2.343    fixes a::real
   2.344    assumes "a \<le> b"
   2.345 -  shows "((\<lambda>x. x) has_integral (b\<^sup>2 - a\<^sup>2) / 2) {a..b}"
   2.346 +  shows "((\<lambda>x. x) has_integral (b\<^sup>2 - a\<^sup>2)/2) {a..b}"
   2.347  proof -
   2.348    have "((\<lambda>x. x) has_integral inverse 2 * b\<^sup>2 - inverse 2 * a\<^sup>2) {a..b}"
   2.349      apply (rule fundamental_theorem_of_calculus [OF assms], clarify)
   2.350 @@ -2740,7 +2707,7 @@
   2.351  lemma integral_ident [simp]:
   2.352    fixes a::real
   2.353    assumes "a \<le> b"
   2.354 -  shows "integral {a..b} (\<lambda>x. x) = (if a \<le> b then (b\<^sup>2 - a\<^sup>2) / 2 else 0)"
   2.355 +  shows "integral {a..b} (\<lambda>x. x) = (if a \<le> b then (b\<^sup>2 - a\<^sup>2)/2 else 0)"
   2.356    by (metis assms ident_has_integral integral_unique)
   2.357  
   2.358  lemma ident_integrable_on:
   2.359 @@ -2798,9 +2765,9 @@
   2.360    and ivl: "a \<le> b"
   2.361    defines "i \<equiv> \<lambda>x. ((b - x) ^ (p - 1) / fact (p - 1)) *\<^sub>R Df p x"
   2.362    shows taylor_has_integral:
   2.363 -    "(i has_integral f b - (\<Sum>i<p. ((b - a) ^ i / fact i) *\<^sub>R Df i a)) {a..b}"
   2.364 +    "(i has_integral f b - (\<Sum>i<p. ((b-a) ^ i / fact i) *\<^sub>R Df i a)) {a..b}"
   2.365    and taylor_integral:
   2.366 -    "f b = (\<Sum>i<p. ((b - a) ^ i / fact i) *\<^sub>R Df i a) + integral {a..b} i"
   2.367 +    "f b = (\<Sum>i<p. ((b-a) ^ i / fact i) *\<^sub>R Df i a) + integral {a..b} i"
   2.368    and taylor_integrable:
   2.369      "i integrable_on {a..b}"
   2.370  proof goal_cases
   2.371 @@ -2855,7 +2822,7 @@
   2.372        by (auto intro!: image_eqI[where x = "p - x - 1"])
   2.373    qed simp
   2.374    from _ this
   2.375 -  have "?sum a = (\<Sum>i<p. ((b - a) ^ i / fact i) *\<^sub>R Df i a)"
   2.376 +  have "?sum a = (\<Sum>i<p. ((b-a) ^ i / fact i) *\<^sub>R Df i a)"
   2.377      by (rule sum.reindex_cong) (auto simp add: inj_on_def Dg_def one)
   2.378    finally show c: ?case .
   2.379    case 2 show ?case using c integral_unique
   2.380 @@ -2900,8 +2867,8 @@
   2.381        by (meson content_eq_0 dual_order.antisym)
   2.382      then have xi: "x\<bullet>i = d\<bullet>i"
   2.383        using \<open>x \<in> K\<close> unfolding keq mem_box by (metis antisym)
   2.384 -    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 +
   2.385 -      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)"
   2.386 +    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 +
   2.387 +      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)"
   2.388      show "\<exists>x'\<in>\<Union>(\<D> - {K}). x' \<noteq> x \<and> dist x' x < e"
   2.389      proof (intro bexI conjI)
   2.390        have "d \<in> cbox c d"
   2.391 @@ -2960,18 +2927,17 @@
   2.392  proof -
   2.393    interpret comm_monoid conj True
   2.394      by standard auto
   2.395 +  have 1: "\<And>a b. box a b = {} \<Longrightarrow> f integrable_on cbox a b"
   2.396 +    by (simp add: content_eq_0_interior integrable_on_null)
   2.397 +  have 2: "\<And>a b c k.
   2.398 +       \<lbrakk>k \<in> Basis;
   2.399 +        f integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c};
   2.400 +        f integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}\<rbrakk>
   2.401 +       \<Longrightarrow> f integrable_on cbox a b"
   2.402 +    unfolding integrable_on_def by (auto intro!: has_integral_split)
   2.403    show ?thesis
   2.404      apply standard
   2.405 -    apply safe
   2.406 -       apply (subst integrable_on_def)
   2.407 -       apply rule
   2.408 -       apply (rule has_integral_null_eq[where i=0, THEN iffD2])
   2.409 -        apply (simp add: content_eq_0_interior)
   2.410 -       apply rule
   2.411 -      apply (rule, assumption, assumption)+
   2.412 -    unfolding integrable_on_def
   2.413 -    apply (auto intro!: has_integral_split)
   2.414 -    done
   2.415 +    using 1 2 by blast+
   2.416  qed
   2.417  
   2.418  lemma integrable_subinterval:
   2.419 @@ -3162,12 +3128,8 @@
   2.420  lemma antiderivative_continuous:
   2.421    fixes q b :: real
   2.422    assumes "continuous_on {a..b} f"
   2.423 -  obtains g where "\<forall>x\<in>{a..b}. (g has_vector_derivative (f x::_::banach)) (at x within {a..b})"
   2.424 -  apply (rule that)
   2.425 -  apply rule
   2.426 -  using integral_has_vector_derivative[OF assms]
   2.427 -  apply auto
   2.428 -  done
   2.429 +  obtains g where "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_vector_derivative (f x::_::banach)) (at x within {a..b})"
   2.430 +  using integral_has_vector_derivative[OF assms] by auto
   2.431  
   2.432  
   2.433  subsection \<open>Combined fundamental theorem of calculus.\<close>
   2.434 @@ -3414,7 +3376,7 @@
   2.435        apply (erule_tac x=i in ballE)
   2.436        apply (auto simp: inner_simps mult_left_mono)
   2.437        done
   2.438 -    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"
   2.439 +    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"
   2.440        by (simp add: inner_simps field_simps)
   2.441      ultimately show ?thesis
   2.442        by (simp add: image_affinity_cbox True content_cbox'
   2.443 @@ -3427,7 +3389,7 @@
   2.444        apply (erule_tac x=i in ballE)
   2.445        apply (auto simp: inner_simps mult_left_mono)
   2.446        done
   2.447 -    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"
   2.448 +    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"
   2.449        by (simp add: inner_simps field_simps)
   2.450      ultimately show ?thesis using False
   2.451        by (simp add: image_affinity_cbox content_cbox'
   2.452 @@ -3491,12 +3453,10 @@
   2.453  lemma uminus_interval_vector[simp]:
   2.454    fixes a b :: "'a::euclidean_space"
   2.455    shows "uminus ` cbox a b = cbox (-b) (-a)"
   2.456 -  apply (rule set_eqI)
   2.457 -  apply rule
   2.458 -  defer
   2.459 -  unfolding image_iff
   2.460 -  apply (rule_tac x="-x" in bexI)
   2.461 -  apply (auto simp add:minus_le_iff le_minus_iff mem_box)
   2.462 +  apply safe
   2.463 +   apply (simp add: mem_box(2))
   2.464 +  apply (rule_tac x="-x" in image_eqI)
   2.465 +   apply (auto simp add: mem_box)
   2.466    done
   2.467  
   2.468  lemma has_integral_reflect_lemma[intro]:
   2.469 @@ -3514,10 +3474,7 @@
   2.470  
   2.471  lemma has_integral_reflect[simp]:
   2.472    "((\<lambda>x. f (-x)) has_integral i) (cbox (-b) (-a)) \<longleftrightarrow> (f has_integral i) (cbox a b)"
   2.473 -  apply rule
   2.474 -  apply (drule_tac[!] has_integral_reflect_lemma)
   2.475 -  apply auto
   2.476 -  done
   2.477 +  by (auto dest: has_integral_reflect_lemma)
   2.478  
   2.479  lemma integrable_reflect[simp]: "(\<lambda>x. f(-x)) integrable_on cbox (-b) (-a) \<longleftrightarrow> f integrable_on cbox a b"
   2.480    unfolding integrable_on_def by auto
   2.481 @@ -3543,7 +3500,7 @@
   2.482    fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
   2.483    assumes "a \<le> b"
   2.484      and contf: "continuous_on {a..b} f"
   2.485 -    and derf: "\<And>x. x \<in> {a <..< b} \<Longrightarrow> (f has_vector_derivative f'(x)) (at x)"
   2.486 +    and derf: "\<And>x. x \<in> {a <..< b} \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
   2.487    shows "(f' has_integral (f b - f a)) {a..b}"
   2.488  proof (cases "a = b")
   2.489    case True
   2.490 @@ -3553,165 +3510,163 @@
   2.491  next
   2.492    case False
   2.493    with \<open>a \<le> b\<close> have ab: "a < b" by arith
   2.494 -  let ?P = "\<lambda>e. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a..b} \<longrightarrow> d fine p \<longrightarrow>
   2.495 -    norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content {a..b})"
   2.496 -  { presume "\<And>e. e > 0 \<Longrightarrow> ?P e" then show ?thesis unfolding has_integral_factor_content_real by force }
   2.497 -  fix e :: real
   2.498 -  assume e: "e > 0"
   2.499 -  then have eba8: "(e * (b - a)) / 8 > 0"
   2.500 -    using ab by (auto simp add: field_simps)
   2.501 -  note derf_exp = derf[unfolded has_vector_derivative_def has_derivative_at_alt]
   2.502 -  have bounded: "\<And>x. x \<in> {a<..<b} \<Longrightarrow> bounded_linear (\<lambda>u. u *\<^sub>R f' x)"
   2.503 -    using derf_exp by simp
   2.504 -  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)"
   2.505 -    (is "\<forall>x \<in> box a b. ?Q x")
   2.506 -  proof
   2.507 -    fix x assume x: "x \<in> box a b"
   2.508 -    show "?Q x"
   2.509 -      apply (rule allE [where x="e/2", OF derf_exp [THEN conjunct2, of x]])
   2.510 -      using x e by auto
   2.511 -  qed
   2.512 -  from this [unfolded bgauge_existence_lemma]
   2.513 -  obtain d where d: "\<And>x. 0 < d x"
   2.514 -    "\<And>x y. \<lbrakk>x \<in> box a b; norm (y-x) < d x\<rbrakk>
   2.515 +  show ?thesis
   2.516 +    unfolding has_integral_factor_content_real
   2.517 +  proof (intro allI impI)
   2.518 +    fix e :: real
   2.519 +    assume e: "e > 0"
   2.520 +    then have eba8: "(e * (b-a)) / 8 > 0"
   2.521 +      using ab by (auto simp add: field_simps)
   2.522 +    note derf_exp = derf[unfolded has_vector_derivative_def has_derivative_at_alt]
   2.523 +    have bounded: "\<And>x. x \<in> {a<..<b} \<Longrightarrow> bounded_linear (\<lambda>u. u *\<^sub>R f' x)"
   2.524 +      using derf_exp by simp
   2.525 +    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)"
   2.526 +      (is "\<forall>x \<in> box a b. ?Q x")
   2.527 +    proof
   2.528 +      fix x assume x: "x \<in> box a b"
   2.529 +      show "?Q x"
   2.530 +        apply (rule allE [where x="e/2", OF derf_exp [THEN conjunct2, of x]])
   2.531 +        using x e by auto
   2.532 +    qed
   2.533 +    from this [unfolded bgauge_existence_lemma]
   2.534 +    obtain d where d: "\<And>x. 0 < d x"
   2.535 +      "\<And>x y. \<lbrakk>x \<in> box a b; norm (y-x) < d x\<rbrakk>
   2.536                 \<Longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e/2 * norm (y-x)"
   2.537 -    by metis
   2.538 -  have "bounded (f ` cbox a b)"
   2.539 -    apply (rule compact_imp_bounded compact_continuous_image)+
   2.540 -    using compact_cbox assms by auto
   2.541 -  then obtain B 
   2.542 -    where "0 < B" and B: "\<And>x. x \<in> f ` cbox a b \<Longrightarrow> norm x \<le> B"
   2.543 -    unfolding bounded_pos by metis
   2.544 -  obtain da where "0 < da"
   2.545 -    and da: "\<And>c. \<lbrakk>a \<le> c; {a..c} \<subseteq> {a..b}; {a..c} \<subseteq> ball a da\<rbrakk>
   2.546 -                          \<Longrightarrow> norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \<le> (e * (b - a)) / 4"
   2.547 -  proof -
   2.548 -    have "continuous (at a within {a..b}) f"
   2.549 -      using contf continuous_on_eq_continuous_within by force
   2.550 -    with eba8 obtain k where "0 < k"
   2.551 -      and k: "\<And>x. \<lbrakk>x \<in> {a..b}; 0 < norm (x-a); norm (x-a) < k\<rbrakk>
   2.552 -                          \<Longrightarrow> norm (f x - f a) < e * (b - a) / 8"
   2.553 -      unfolding continuous_within Lim_within dist_norm by metis
   2.554 -    obtain l where l: "0 < l" "norm (l *\<^sub>R f' a) \<le> e * (b - a) / 8" 
   2.555 -    proof (cases "f' a = 0")
   2.556 -      case True with ab e that show ?thesis by auto
   2.557 -    next
   2.558 -      case False
   2.559 -      then show ?thesis
   2.560 -        apply (rule_tac l="(e * (b - a)) / 8 / norm (f' a)" in that)
   2.561 -        using ab e apply (auto simp add: field_simps)
   2.562 -        done
   2.563 -    qed
   2.564 -    have "norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \<le> e * (b - a) / 4"
   2.565 -      if "a \<le> c" "{a..c} \<subseteq> {a..b}" and bmin: "{a..c} \<subseteq> ball a (min k l)" for c
   2.566 +      by metis
   2.567 +    have "bounded (f ` cbox a b)"
   2.568 +      using compact_cbox assms by (auto simp: compact_imp_bounded compact_continuous_image)
   2.569 +    then obtain B 
   2.570 +      where "0 < B" and B: "\<And>x. x \<in> f ` cbox a b \<Longrightarrow> norm x \<le> B"
   2.571 +      unfolding bounded_pos by metis
   2.572 +    obtain da where "0 < da"
   2.573 +      and da: "\<And>c. \<lbrakk>a \<le> c; {a..c} \<subseteq> {a..b}; {a..c} \<subseteq> ball a da\<rbrakk>
   2.574 +                          \<Longrightarrow> norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \<le> (e * (b-a)) / 4"
   2.575      proof -
   2.576 -      have minkl: "\<bar>a - x\<bar> < min k l" if "x \<in> {a..c}" for x
   2.577 -        using bmin dist_real_def that by auto
   2.578 -      then have lel: "\<bar>c - a\<bar> \<le> \<bar>l\<bar>"
   2.579 -        using that by force
   2.580 -      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)"
   2.581 -        by (rule norm_triangle_ineq4)
   2.582 -      also have "\<dots> \<le> e * (b - a) / 8 + e * (b - a) / 8"
   2.583 -      proof (rule add_mono)
   2.584 -        have "norm ((c - a) *\<^sub>R f' a) \<le> norm (l *\<^sub>R f' a)"
   2.585 -          by (auto intro: mult_right_mono [OF lel])
   2.586 -        also have "... \<le> e * (b - a) / 8"
   2.587 -          by (rule l)
   2.588 -        finally show "norm ((c - a) *\<^sub>R f' a) \<le> e * (b - a) / 8" .
   2.589 +      have "continuous (at a within {a..b}) f"
   2.590 +        using contf continuous_on_eq_continuous_within by force
   2.591 +      with eba8 obtain k where "0 < k"
   2.592 +        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"
   2.593 +        unfolding continuous_within Lim_within dist_norm by metis
   2.594 +      obtain l where l: "0 < l" "norm (l *\<^sub>R f' a) \<le> e * (b-a) / 8" 
   2.595 +      proof (cases "f' a = 0")
   2.596 +        case True with ab e that show ?thesis by auto
   2.597        next
   2.598 -        have "norm (f c - f a) < e * (b - a) / 8"
   2.599 -        proof (cases "a = c")
   2.600 -          case True then show ?thesis
   2.601 -            using eba8 by auto
   2.602 -        next
   2.603 -          case False show ?thesis
   2.604 -            by (rule k) (use minkl \<open>a \<le> c\<close> that False in auto)
   2.605 -        qed
   2.606 -        then show "norm (f c - f a) \<le> e * (b - a) / 8" by simp
   2.607 +        case False
   2.608 +        then show ?thesis
   2.609 +          apply (rule_tac l="(e * (b-a)) / 8 / norm (f' a)" in that)
   2.610 +          using ab e apply (auto simp add: field_simps)
   2.611 +          done
   2.612        qed
   2.613 -      finally show "norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \<le> e * (b - a) / 4"
   2.614 -        unfolding content_real[OF \<open>a \<le> c\<close>] by auto
   2.615 +      have "norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \<le> e * (b-a) / 4"
   2.616 +        if "a \<le> c" "{a..c} \<subseteq> {a..b}" and bmin: "{a..c} \<subseteq> ball a (min k l)" for c
   2.617 +      proof -
   2.618 +        have minkl: "\<bar>a - x\<bar> < min k l" if "x \<in> {a..c}" for x
   2.619 +          using bmin dist_real_def that by auto
   2.620 +        then have lel: "\<bar>c - a\<bar> \<le> \<bar>l\<bar>"
   2.621 +          using that by force
   2.622 +        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)"
   2.623 +          by (rule norm_triangle_ineq4)
   2.624 +        also have "\<dots> \<le> e * (b-a) / 8 + e * (b-a) / 8"
   2.625 +        proof (rule add_mono)
   2.626 +          have "norm ((c - a) *\<^sub>R f' a) \<le> norm (l *\<^sub>R f' a)"
   2.627 +            by (auto intro: mult_right_mono [OF lel])
   2.628 +          also have "... \<le> e * (b-a) / 8"
   2.629 +            by (rule l)
   2.630 +          finally show "norm ((c - a) *\<^sub>R f' a) \<le> e * (b-a) / 8" .
   2.631 +        next
   2.632 +          have "norm (f c - f a) < e * (b-a) / 8"
   2.633 +          proof (cases "a = c")
   2.634 +            case True then show ?thesis
   2.635 +              using eba8 by auto
   2.636 +          next
   2.637 +            case False show ?thesis
   2.638 +              by (rule k) (use minkl \<open>a \<le> c\<close> that False in auto)
   2.639 +          qed
   2.640 +          then show "norm (f c - f a) \<le> e * (b-a) / 8" by simp
   2.641 +        qed
   2.642 +        finally show "norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \<le> e * (b-a) / 4"
   2.643 +          unfolding content_real[OF \<open>a \<le> c\<close>] by auto
   2.644 +      qed
   2.645 +      then show ?thesis
   2.646 +        by (rule_tac da="min k l" in that) (auto simp: l \<open>0 < k\<close>)
   2.647      qed
   2.648 -    then show ?thesis
   2.649 -      by (rule_tac da="min k l" in that) (auto simp: l \<open>0 < k\<close>)
   2.650 -  qed
   2.651 -  obtain db where "0 < db"
   2.652 -            and db: "\<And>c. \<lbrakk>c \<le> b; {c..b} \<subseteq> {a..b}; {c..b} \<subseteq> ball b db\<rbrakk>
   2.653 -                          \<Longrightarrow> norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> (e * (b - a)) / 4"
   2.654 -  proof -
   2.655 -    have "continuous (at b within {a..b}) f"
   2.656 -      using contf continuous_on_eq_continuous_within by force
   2.657 -    with eba8 obtain k
   2.658 -      where "0 < k"
   2.659 -        and k: "\<And>x. \<lbrakk>x \<in> {a..b}; 0 < norm(x-b); norm(x-b) < k\<rbrakk>
   2.660 -                     \<Longrightarrow> norm (f b - f x) < e * (b - a) / 8"
   2.661 -      unfolding continuous_within Lim_within dist_norm norm_minus_commute by metis
   2.662 -    obtain l where l: "0 < l" "norm (l *\<^sub>R f' b) \<le> (e * (b - a)) / 8"
   2.663 -    proof (cases "f' b = 0")
   2.664 -      case True thus ?thesis 
   2.665 -        using ab e that by auto
   2.666 -    next
   2.667 -      case False then show ?thesis
   2.668 -        apply (rule_tac l="(e * (b - a)) / 8 / norm (f' b)" in that)
   2.669 -        using ab e by (auto simp add: field_simps)
   2.670 -    qed
   2.671 -    have "norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> e * (b - a) / 4" 
   2.672 -      if "c \<le> b" "{c..b} \<subseteq> {a..b}" and bmin: "{c..b} \<subseteq> ball b (min k l)" for c
   2.673 +    obtain db where "0 < db"
   2.674 +      and db: "\<And>c. \<lbrakk>c \<le> b; {c..b} \<subseteq> {a..b}; {c..b} \<subseteq> ball b db\<rbrakk>
   2.675 +                          \<Longrightarrow> norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> (e * (b-a)) / 4"
   2.676      proof -
   2.677 -      have minkl: "\<bar>b - x\<bar> < min k l" if "x \<in> {c..b}" for x
   2.678 -        using bmin dist_real_def that by auto
   2.679 -      then have lel: "\<bar>b - c\<bar> \<le> \<bar>l\<bar>"
   2.680 -        using that by force
   2.681 -      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)"
   2.682 -        by (rule norm_triangle_ineq4)
   2.683 -      also have "\<dots> \<le> e * (b - a) / 8 + e * (b - a) / 8"
   2.684 -      proof (rule add_mono)
   2.685 -        have "norm ((b - c) *\<^sub>R f' b) \<le> norm (l *\<^sub>R f' b)"
   2.686 -          by (auto intro: mult_right_mono [OF lel])
   2.687 -        also have "... \<le> e * (b - a) / 8"
   2.688 -          by (rule l)
   2.689 -        finally show "norm ((b - c) *\<^sub>R f' b) \<le> e * (b - a) / 8" .
   2.690 +      have "continuous (at b within {a..b}) f"
   2.691 +        using contf continuous_on_eq_continuous_within by force
   2.692 +      with eba8 obtain k
   2.693 +        where "0 < k"
   2.694 +          and k: "\<And>x. \<lbrakk>x \<in> {a..b}; 0 < norm(x-b); norm(x-b) < k\<rbrakk>
   2.695 +                     \<Longrightarrow> norm (f b - f x) < e * (b-a) / 8"
   2.696 +        unfolding continuous_within Lim_within dist_norm norm_minus_commute by metis
   2.697 +      obtain l where l: "0 < l" "norm (l *\<^sub>R f' b) \<le> (e * (b-a)) / 8"
   2.698 +      proof (cases "f' b = 0")
   2.699 +        case True thus ?thesis 
   2.700 +          using ab e that by auto
   2.701        next
   2.702 -        have "norm (f b - f c) < e * (b - a) / 8"
   2.703 -        proof (cases "b = c")
   2.704 -          case True with eba8 show ?thesis
   2.705 -            by auto
   2.706 -        next
   2.707 -          case False show ?thesis
   2.708 -            by (rule k) (use minkl \<open>c \<le> b\<close> that False in auto)
   2.709 -        qed
   2.710 -        then show "norm (f b - f c) \<le> e * (b - a) / 8" by simp
   2.711 +        case False then show ?thesis
   2.712 +          apply (rule_tac l="(e * (b-a)) / 8 / norm (f' b)" in that)
   2.713 +          using ab e by (auto simp add: field_simps)
   2.714        qed
   2.715 -      finally show "norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> e * (b - a) / 4"
   2.716 -        unfolding content_real[OF \<open>c \<le> b\<close>] by auto
   2.717 +      have "norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> e * (b-a) / 4" 
   2.718 +        if "c \<le> b" "{c..b} \<subseteq> {a..b}" and bmin: "{c..b} \<subseteq> ball b (min k l)" for c
   2.719 +      proof -
   2.720 +        have minkl: "\<bar>b - x\<bar> < min k l" if "x \<in> {c..b}" for x
   2.721 +          using bmin dist_real_def that by auto
   2.722 +        then have lel: "\<bar>b - c\<bar> \<le> \<bar>l\<bar>"
   2.723 +          using that by force
   2.724 +        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)"
   2.725 +          by (rule norm_triangle_ineq4)
   2.726 +        also have "\<dots> \<le> e * (b-a) / 8 + e * (b-a) / 8"
   2.727 +        proof (rule add_mono)
   2.728 +          have "norm ((b - c) *\<^sub>R f' b) \<le> norm (l *\<^sub>R f' b)"
   2.729 +            by (auto intro: mult_right_mono [OF lel])
   2.730 +          also have "... \<le> e * (b-a) / 8"
   2.731 +            by (rule l)
   2.732 +          finally show "norm ((b - c) *\<^sub>R f' b) \<le> e * (b-a) / 8" .
   2.733 +        next
   2.734 +          have "norm (f b - f c) < e * (b-a) / 8"
   2.735 +          proof (cases "b = c")
   2.736 +            case True with eba8 show ?thesis
   2.737 +              by auto
   2.738 +          next
   2.739 +            case False show ?thesis
   2.740 +              by (rule k) (use minkl \<open>c \<le> b\<close> that False in auto)
   2.741 +          qed
   2.742 +          then show "norm (f b - f c) \<le> e * (b-a) / 8" by simp
   2.743 +        qed
   2.744 +        finally show "norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> e * (b-a) / 4"
   2.745 +          unfolding content_real[OF \<open>c \<le> b\<close>] by auto
   2.746 +      qed
   2.747 +      then show ?thesis
   2.748 +        by (rule_tac db="min k l" in that) (auto simp: l \<open>0 < k\<close>)
   2.749      qed
   2.750 -    then show ?thesis
   2.751 -      by (rule_tac db="min k l" in that) (auto simp: l \<open>0 < k\<close>)
   2.752 -  qed
   2.753 -  let ?d = "(\<lambda>x. ball x (if x=a then da else if x=b then db else d x))"
   2.754 -  show "?P e"
   2.755 -  proof (intro exI conjI allI impI)
   2.756 -    show "gauge ?d"
   2.757 -      using ab \<open>db > 0\<close> \<open>da > 0\<close> d(1) by (auto intro: gauge_ball_dependent)
   2.758 -  next
   2.759 -    fix p
   2.760 -    assume ptag: "p tagged_division_of {a..b}" and fine: "?d fine p"
   2.761 -    let ?A = "{t. fst t \<in> {a, b}}"
   2.762 -    note p = tagged_division_ofD[OF ptag]
   2.763 -    have pA: "p = (p \<inter> ?A) \<union> (p - ?A)" "finite (p \<inter> ?A)" "finite (p - ?A)" "(p \<inter> ?A) \<inter> (p - ?A) = {}"
   2.764 -      using ptag fine by auto
   2.765 -    note * = additive_tagged_division_1[OF assms(1) ptag, symmetric]
   2.766 -    have **: "\<And>n1 s1 n2 s2::real. n2 \<le> s2 / 2 \<Longrightarrow> n1 - s1 \<le> s2 / 2 \<Longrightarrow> n1 + n2 \<le> s1 + s2"
   2.767 -      by arith
   2.768 -    have non: False if xk: "(x,K) \<in> p" and "x \<noteq> a" "x \<noteq> b"
   2.769 -         and less: "e * (Sup K - Inf K) / 2 < norm (content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))"
   2.770 -         for x K
   2.771 +    let ?d = "(\<lambda>x. ball x (if x=a then da else if x=b then db else d x))"
   2.772 +    show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow>
   2.773 +              norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f' x) - (f b - f a)) \<le> e * content {a..b})"
   2.774 +    proof (rule exI, safe)
   2.775 +      show "gauge ?d"
   2.776 +        using ab \<open>db > 0\<close> \<open>da > 0\<close> d(1) by (auto intro: gauge_ball_dependent)
   2.777 +    next
   2.778 +      fix p
   2.779 +      assume ptag: "p tagged_division_of {a..b}" and fine: "?d fine p"
   2.780 +      let ?A = "{t. fst t \<in> {a, b}}"
   2.781 +      note p = tagged_division_ofD[OF ptag]
   2.782 +      have pA: "p = (p \<inter> ?A) \<union> (p - ?A)" "finite (p \<inter> ?A)" "finite (p - ?A)" "(p \<inter> ?A) \<inter> (p - ?A) = {}"
   2.783 +        using ptag fine by auto
   2.784 +      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"
   2.785 +        by arith
   2.786 +      have non: False if xk: "(x,K) \<in> p" and "x \<noteq> a" "x \<noteq> b"
   2.787 +        and less: "e * (Sup K - Inf K)/2 < norm (content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))"
   2.788 +      for x K
   2.789        proof -
   2.790          obtain u v where k: "K = cbox u v"
   2.791            using p(4) xk by blast
   2.792          then have "u \<le> v" and uv: "{u, v} \<subseteq> cbox u v"
   2.793            using p(2)[OF xk] by auto
   2.794 -        then have result: "e * (v - u) / 2 < norm ((v - u) *\<^sub>R f' x - (f v - f u))"
   2.795 +        then have result: "e * (v - u)/2 < norm ((v - u) *\<^sub>R f' x - (f v - f u))"
   2.796            using less[unfolded k box_real interval_bounds_real content_real] by auto
   2.797          then have "x \<in> box a b"
   2.798            using p(2) p(3) \<open>x \<noteq> a\<close> \<open>x \<noteq> b\<close> xk by fastforce
   2.799 @@ -3721,8 +3676,8 @@
   2.800          have xd: "norm (u - x) < d x" "norm (v - x) < d x"
   2.801            using fineD[OF fine xk] \<open>x \<noteq> a\<close> \<open>x \<noteq> b\<close> uv 
   2.802            by (auto simp add: k subset_eq dist_commute dist_real_def)
   2.803 -        have "norm ((v - u) *\<^sub>R f' (x) - (f (v) - f (u))) =
   2.804 -              norm ((f (u) - f (x) - (u - x) *\<^sub>R f' (x)) - (f (v) - f (x) - (v - x) *\<^sub>R f' (x)))"
   2.805 +        have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) =
   2.806 +              norm ((f u - f x - (u - x) *\<^sub>R f' x) - (f v - f x - (v - x) *\<^sub>R f' x))"
   2.807            by (rule arg_cong[where f=norm]) (auto simp: scaleR_left.diff)
   2.808          also have "\<dots> \<le> e/2 * norm (u - x) + e/2 * norm (v - x)"
   2.809            by (metis norm_triangle_le_diff add_mono * xd)
   2.810 @@ -3730,211 +3685,184 @@
   2.811            using p(2)[OF xk] by (auto simp add: field_simps k)
   2.812          also have "\<dots> < norm ((v - u) *\<^sub>R f' x - (f v - f u))"
   2.813            using result by (simp add: \<open>u \<le> v\<close>)
   2.814 -        finally have "e * (v - u) / 2 < e * (v - u) / 2"
   2.815 +        finally have "e * (v - u)/2 < e * (v - u)/2"
   2.816            using uv by auto
   2.817          then show False by auto
   2.818        qed
   2.819 -    have "norm (\<Sum>(x, K)\<in>p - ?A. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))
   2.820 +      have "norm (\<Sum>(x, K)\<in>p - ?A. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))
   2.821            \<le> (\<Sum>(x, K)\<in>p - ?A. norm (content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))))"
   2.822 -      by (auto intro: sum_norm_le)
   2.823 -    also have "... \<le> (\<Sum>n\<in>p - ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k) / 2)"
   2.824 -      using non by (force intro: sum_mono)
   2.825 -    finally have I: "norm (\<Sum>(x, k)\<in>p - ?A.
   2.826 +        by (auto intro: sum_norm_le)
   2.827 +      also have "... \<le> (\<Sum>n\<in>p - ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k)/2)"
   2.828 +        using non by (fastforce intro: sum_mono)
   2.829 +      finally have I: "norm (\<Sum>(x, k)\<in>p - ?A.
   2.830                    content k *\<^sub>R f' x - (f (Sup k) - f (Inf k)))
   2.831 -             \<le> (\<Sum>n\<in>p - ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k)) / 2"
   2.832 -      by (simp add: sum_divide_distrib)
   2.833 -    have II: "norm (\<Sum>(x, k)\<in>p \<inter> ?A. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) -
   2.834 +             \<le> (\<Sum>n\<in>p - ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k))/2"
   2.835 +        by (simp add: sum_divide_distrib)
   2.836 +      have II: "norm (\<Sum>(x, k)\<in>p \<inter> ?A. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) -
   2.837               (\<Sum>n\<in>p \<inter> ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k))
   2.838 -             \<le> (\<Sum>n\<in>p - ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k)) / 2"
   2.839 -    proof -
   2.840 -      have ge0: "0 \<le> e * (Sup k - Inf k)" if xkp: "(x, k) \<in> p \<inter> ?A" for x k
   2.841 +             \<le> (\<Sum>n\<in>p - ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k))/2"
   2.842        proof -
   2.843 -        obtain u v where uv: "k = cbox u v"
   2.844 -          by (meson Int_iff xkp p(4))
   2.845 -        with p(2) that uv have "cbox u v \<noteq> {}"
   2.846 -          by blast
   2.847 -        then show "0 \<le> e * ((Sup k) - (Inf k))"
   2.848 -          unfolding uv using e by (auto simp add: field_simps)
   2.849 -      qed
   2.850 -      let ?B = "\<lambda>x. {t \<in> p. fst t = x \<and> content (snd t) \<noteq> 0}"
   2.851 -      let ?C = "{t \<in> p. fst t \<in> {a, b} \<and> content (snd t) \<noteq> 0}"
   2.852 -      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"
   2.853 -      proof -
   2.854 -        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"
   2.855 -          by auto
   2.856 -        have 1: "content K *\<^sub>R (f' (x)) - (f ((Sup K)) - f ((Inf K))) = 0"
   2.857 -                if "(x,K) \<in> p \<inter> {t. fst t \<in> {a, b}} - p \<inter> ?C" for x K
   2.858 +        have ge0: "0 \<le> e * (Sup k - Inf k)" if xkp: "(x, k) \<in> p \<inter> ?A" for x k
   2.859          proof -
   2.860 -          have xk: "(x, K) \<in> p" and k0: "content K = 0"
   2.861 -            using that by auto
   2.862 -          then obtain u v where uv: "K = cbox u v"
   2.863 -            using p(4) by blast
   2.864 -          then have "u = v"
   2.865 -            using xk k0 p(2) by force
   2.866 -          then show "content K *\<^sub>R (f' (x)) - (f ((Sup K)) - f ((Inf K))) = 0"
   2.867 -            using xk unfolding uv by auto
   2.868 -        qed
   2.869 -        have 2: "norm(\<Sum>(x,k)\<in>p \<inter> ?C. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) 
   2.870 -                 \<le> e * (b - a) / 2"
   2.871 -        proof -
   2.872 -          have *: "p \<inter> ?C = ?B a \<union> ?B b"
   2.873 +          obtain u v where uv: "k = cbox u v"
   2.874 +            by (meson Int_iff xkp p(4))
   2.875 +          with p(2) that uv have "cbox u v \<noteq> {}"
   2.876              by blast
   2.877 -          have **: "norm (sum f s) \<le> e"
   2.878 -            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"
   2.879 -            for s f and e :: real
   2.880 -          proof (cases "s = {}")
   2.881 -            case True
   2.882 -            with that show ?thesis by auto
   2.883 -          next
   2.884 -            case False
   2.885 -            then obtain x where "x \<in> s"
   2.886 -              by auto
   2.887 -            then have "s = {x}"
   2.888 -              using that(1) by auto
   2.889 -            then show ?thesis
   2.890 -              using \<open>x \<in> s\<close> that(2) by auto
   2.891 +          then show "0 \<le> e * ((Sup k) - (Inf k))"
   2.892 +            unfolding uv using e by (auto simp add: field_simps)
   2.893 +        qed
   2.894 +        let ?B = "\<lambda>x. {t \<in> p. fst t = x \<and> content (snd t) \<noteq> 0}"
   2.895 +        let ?C = "{t \<in> p. fst t \<in> {a, b} \<and> content (snd t) \<noteq> 0}"
   2.896 +        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"
   2.897 +        proof -
   2.898 +          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"
   2.899 +            by auto
   2.900 +          have 1: "content K *\<^sub>R (f' x) - (f ((Sup K)) - f ((Inf K))) = 0"
   2.901 +            if "(x,K) \<in> p \<inter> {t. fst t \<in> {a, b}} - p \<inter> ?C" for x K
   2.902 +          proof -
   2.903 +            have xk: "(x,K) \<in> p" and k0: "content K = 0"
   2.904 +              using that by auto
   2.905 +            then obtain u v where uv: "K = cbox u v"
   2.906 +              using p(4) by blast
   2.907 +            then have "u = v"
   2.908 +              using xk k0 p(2) by force
   2.909 +            then show "content K *\<^sub>R (f' x) - (f ((Sup K)) - f ((Inf K))) = 0"
   2.910 +              using xk unfolding uv by auto
   2.911            qed
   2.912 -          show "norm (\<Sum>(x,k)\<in>p \<inter> ?C.
   2.913 -                        content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \<le> e * (b - a) / 2"
   2.914 -            apply (subst *)
   2.915 -            apply (subst sum.union_disjoint)
   2.916 -               prefer 4
   2.917 -               apply (rule order_trans[of _ "e * (b - a)/4 + e * (b - a)/4"])
   2.918 -                apply (rule norm_triangle_le,rule add_mono)
   2.919 -                 apply (rule_tac[1-2] **)
   2.920 -
   2.921 +          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"
   2.922            proof -
   2.923 -            have pa: "\<exists>v. k = cbox a v \<and> a \<le> v" if "(a, k) \<in> p" for k
   2.924 -            proof -
   2.925 -              obtain u v where uv: "k = cbox u v"
   2.926 -                using \<open>(a, k) \<in> p\<close> p(4) by blast
   2.927 -              moreover have "u \<le> v"
   2.928 -                using uv p(2)[OF that] by auto
   2.929 -              moreover have "u = a"
   2.930 -                using p(2) p(3) that uv by force
   2.931 -              ultimately show ?thesis
   2.932 -                by blast
   2.933 -            qed
   2.934 -            have pb: "\<exists>v. k = cbox v b \<and> b \<ge> v" if "(b, k) \<in> p" for k
   2.935 -            proof -
   2.936 -              obtain u v where uv: "k = cbox u v"
   2.937 -                using \<open>(b, k) \<in> p\<close> p(4) by blast
   2.938 -              moreover have "u \<le> v"
   2.939 -                using p(2)[OF that] unfolding uv by auto
   2.940 -              moreover have "v = b"
   2.941 -                using p(2) p(3) that uv by force
   2.942 -              ultimately show ?thesis
   2.943 -                by blast
   2.944 +            have norm_le: "norm (sum f S) \<le> e"
   2.945 +              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"
   2.946 +              for S f and e :: real
   2.947 +            proof (cases "S = {}")
   2.948 +              case True
   2.949 +              with that show ?thesis by auto
   2.950 +            next
   2.951 +              case False then obtain x where "x \<in> S"
   2.952 +                by auto
   2.953 +              then have "S = {x}"
   2.954 +                using that(1) by auto
   2.955 +              then show ?thesis
   2.956 +                using \<open>x \<in> S\<close> that(2) by auto
   2.957              qed
   2.958 -            show "\<forall>x y. x \<in> ?B a \<and> y \<in> ?B a \<longrightarrow> x = y"
   2.959 -            proof (safe; clarsimp)
   2.960 -              fix x k k'
   2.961 -              assume k: "(a, k) \<in> p" "(a, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
   2.962 -              obtain v where v: "k = cbox a v" "a \<le> v"
   2.963 -                using pa[OF k(1)] by blast
   2.964 -              obtain v' where v': "k' = cbox a v'" "a \<le> v'"
   2.965 -                using pa[OF k(2)] by blast              
   2.966 -              let ?v = "min v v'"
   2.967 -              have "box a ?v \<subseteq> k \<inter> k'"
   2.968 -                unfolding v v' by (auto simp add: mem_box)
   2.969 -              then have "interior (box a (min v v')) \<subseteq> interior k \<inter> interior k'"
   2.970 -                using interior_Int interior_mono by blast
   2.971 -              moreover have "(a + ?v)/2 \<in> box a ?v"
   2.972 -                using k(3-)
   2.973 -                unfolding v v' content_eq_0 not_le
   2.974 -                by (auto simp add: mem_box)
   2.975 -              ultimately have "(a + ?v)/2 \<in> interior k \<inter> interior k'"
   2.976 -                unfolding interior_open[OF open_box] by auto
   2.977 -              then have eq: "k = k'"
   2.978 -                using p(5)[OF k(1-2)] by auto
   2.979 -              { assume "x \<in> k" then show "x \<in> k'" unfolding eq . }
   2.980 -              { assume "x \<in> k'" then show "x \<in> k" unfolding eq . }
   2.981 -            qed
   2.982 -
   2.983 -            show "\<forall>x y. x \<in> ?B b \<and> y \<in> ?B b \<longrightarrow> x = y"
   2.984 -            proof (safe; clarsimp)
   2.985 -              fix x K K'
   2.986 -              assume k: "(b, K) \<in> p" "(b, K') \<in> p" "content K \<noteq> 0" "content K' \<noteq> 0"
   2.987 -              obtain v where v: "K = cbox v b" "v \<le> b"
   2.988 -                using pb[OF k(1)] by blast
   2.989 -              obtain v' where v': "K' = cbox v' b" "v' \<le> b"
   2.990 -                using pb[OF k(2)] by blast 
   2.991 -              let ?v = "max v v'"
   2.992 -              have "box ?v b \<subseteq> K \<inter> K'"
   2.993 -                unfolding v v' by (auto simp: mem_box)
   2.994 -              then have "interior (box (max v v') b) \<subseteq> interior K \<inter> interior K'"
   2.995 -                using interior_Int interior_mono by blast
   2.996 -              moreover have " ((b + ?v)/2) \<in> box ?v b"
   2.997 -                using k(3-) unfolding v v' content_eq_0 not_le by (auto simp: mem_box)
   2.998 -              ultimately have " ((b + ?v)/2) \<in> interior K \<inter> interior K'"
   2.999 -                unfolding interior_open[OF open_box] by auto
  2.1000 -              then have eq: "K = K'"
  2.1001 -                using p(5)[OF k(1-2)] by auto
  2.1002 -              { assume "x \<in> K" then show "x \<in> K'" unfolding eq . }
  2.1003 -              { assume "x \<in> K'" then show "x \<in> K" unfolding eq . }
  2.1004 +            have *: "p \<inter> ?C = ?B a \<union> ?B b"
  2.1005 +              by blast
  2.1006 +            then have "norm (\<Sum>(x,K)\<in>p \<inter> ?C. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))) =
  2.1007 +                       norm (\<Sum>(x,K) \<in> ?B a \<union> ?B b. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))"
  2.1008 +              by simp
  2.1009 +            also have "... = norm ((\<Sum>(x,K) \<in> ?B a. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))) + 
  2.1010 +                                   (\<Sum>(x,K) \<in> ?B b. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))))"
  2.1011 +              apply (subst sum.union_disjoint)
  2.1012 +              using p(1) ab e by auto
  2.1013 +            also have "... \<le> e * (b - a) / 4 + e * (b - a) / 4"
  2.1014 +            proof (rule norm_triangle_le [OF add_mono])
  2.1015 +              have pa: "\<exists>v. k = cbox a v \<and> a \<le> v" if "(a, k) \<in> p" for k
  2.1016 +                using p(2) p(3) p(4) that by fastforce
  2.1017 +              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"
  2.1018 +              proof (intro norm_le; clarsimp)
  2.1019 +                fix K K'
  2.1020 +                assume K: "(a, K) \<in> p" "(a, K') \<in> p" and ne0: "content K \<noteq> 0" "content K' \<noteq> 0"
  2.1021 +                with pa obtain v v' where v: "K = cbox a v" "a \<le> v" and v': "K' = cbox a v'" "a \<le> v'"
  2.1022 +                  by blast
  2.1023 +                let ?v = "min v v'"
  2.1024 +                have "box a ?v \<subseteq> K \<inter> K'"
  2.1025 +                  unfolding v v' by (auto simp add: mem_box)
  2.1026 +                then have "interior (box a (min v v')) \<subseteq> interior K \<inter> interior K'"
  2.1027 +                  using interior_Int interior_mono by blast
  2.1028 +                moreover have "(a + ?v)/2 \<in> box a ?v"
  2.1029 +                  using ne0  unfolding v v' content_eq_0 not_le
  2.1030 +                  by (auto simp add: mem_box)
  2.1031 +                ultimately have "(a + ?v)/2 \<in> interior K \<inter> interior K'"
  2.1032 +                  unfolding interior_open[OF open_box] by auto
  2.1033 +                then show "K = K'"
  2.1034 +                  using p(5)[OF K] by auto
  2.1035 +              next
  2.1036 +                fix K 
  2.1037 +                assume K: "(a, K) \<in> p" and ne0: "content K \<noteq> 0"
  2.1038 +                show "norm (content c *\<^sub>R f' a - (f (Sup c) - f (Inf c))) * 4 \<le> e * (b-a)"
  2.1039 +                  if "(a, c) \<in> p" and ne0: "content c \<noteq> 0" for c
  2.1040 +                proof -
  2.1041 +                  obtain v where v: "c = cbox a v" and "a \<le> v"
  2.1042 +                    using pa[OF \<open>(a, c) \<in> p\<close>] by metis 
  2.1043 +                  then have "a \<in> {a..v}" "v \<le> b"
  2.1044 +                    using p(3)[OF \<open>(a, c) \<in> p\<close>] by auto
  2.1045 +                  moreover have "{a..v} \<subseteq> ball a da"
  2.1046 +                    using fineD[OF \<open>?d fine p\<close> \<open>(a, c) \<in> p\<close>] by (simp add: v split: if_split_asm)
  2.1047 +                  ultimately show ?thesis
  2.1048 +                    unfolding v interval_bounds_real[OF \<open>a \<le> v\<close>] box_real
  2.1049 +                    using da \<open>a \<le> v\<close> by auto
  2.1050 +                qed
  2.1051 +              qed (use ab e in auto)
  2.1052 +            next
  2.1053 +              have pb: "\<exists>v. k = cbox v b \<and> b \<ge> v" if "(b, k) \<in> p" for k
  2.1054 +                using p(2) p(3) p(4) that by fastforce
  2.1055 +              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"
  2.1056 +              proof (intro norm_le; clarsimp)
  2.1057 +                fix K K'
  2.1058 +                assume K: "(b, K) \<in> p" "(b, K') \<in> p" and ne0: "content K \<noteq> 0" "content K' \<noteq> 0"
  2.1059 +                with pb obtain v v' where v: "K = cbox v b" "v \<le> b" and v': "K' = cbox v' b" "v' \<le> b"
  2.1060 +                  by blast
  2.1061 +                let ?v = "max v v'"
  2.1062 +                have "box ?v b \<subseteq> K \<inter> K'"
  2.1063 +                  unfolding v v' by (auto simp: mem_box)
  2.1064 +                then have "interior (box (max v v') b) \<subseteq> interior K \<inter> interior K'"
  2.1065 +                  using interior_Int interior_mono by blast
  2.1066 +                moreover have " ((b + ?v)/2) \<in> box ?v b"
  2.1067 +                  using ne0 unfolding v v' content_eq_0 not_le by (auto simp: mem_box)
  2.1068 +                ultimately have "((b + ?v)/2) \<in> interior K \<inter> interior K'"
  2.1069 +                  unfolding interior_open[OF open_box] by auto
  2.1070 +                then show "K = K'"
  2.1071 +                  using p(5)[OF K] by auto
  2.1072 +              next
  2.1073 +                fix K 
  2.1074 +                assume K: "(b, K) \<in> p" and ne0: "content K \<noteq> 0"
  2.1075 +                show "norm (content c *\<^sub>R f' b - (f (Sup c) - f (Inf c))) * 4 \<le> e * (b-a)"
  2.1076 +                  if "(b, c) \<in> p" and ne0: "content c \<noteq> 0" for c
  2.1077 +                proof -
  2.1078 +                obtain v where v: "c = cbox v b" and "v \<le> b"
  2.1079 +                  using \<open>(b, c) \<in> p\<close> pb by blast
  2.1080 +                then have "v \<ge> a""b \<in> {v.. b}"  
  2.1081 +                  using p(3)[OF \<open>(b, c) \<in> p\<close>] by auto
  2.1082 +                moreover have "{v..b} \<subseteq> ball b db"
  2.1083 +                  using fineD[OF \<open>?d fine p\<close> \<open>(b, c) \<in> p\<close>] box_real(2) v False by force
  2.1084 +                ultimately show ?thesis
  2.1085 +                  using db v by auto
  2.1086 +                qed
  2.1087 +              qed (use ab e in auto)
  2.1088              qed
  2.1089 -
  2.1090 -            have "norm (content c *\<^sub>R f' a - (f (Sup c) - f (Inf c))) \<le> e * (b - a) / 4"
  2.1091 -              if "(a, c) \<in> p" and ne0: "content c \<noteq> 0" for c
  2.1092 -            proof -
  2.1093 -              obtain v where v: "c = cbox a v" and "a \<le> v"
  2.1094 -                using pa[OF \<open>(a, c) \<in> p\<close>] by metis 
  2.1095 -              then have "a \<in> {a..v}" "v \<le> b"
  2.1096 -                using p(3)[OF \<open>(a, c) \<in> p\<close>] by auto
  2.1097 -              moreover have "{a..v} \<subseteq> ball a da"
  2.1098 -                using fineD[OF \<open>?d fine p\<close> \<open>(a, c) \<in> p\<close>] by (simp add: v split: if_split_asm)
  2.1099 -              ultimately show ?thesis
  2.1100 -                unfolding v interval_bounds_real[OF \<open>a \<le> v\<close>] box_real
  2.1101 -                using da \<open>a \<le> v\<close> by auto
  2.1102 -            qed
  2.1103 -            then show "\<forall>x. x \<in> ?B a \<longrightarrow> norm ((\<lambda>(x, k). content k *\<^sub>R f' x - (f (Sup k) -
  2.1104 -              f (Inf k))) x) \<le> e * (b - a) / 4"
  2.1105 -              by auto
  2.1106 -
  2.1107 -            have "norm (content c *\<^sub>R f' b - (f (Sup c) - f (Inf c))) \<le> e * (b - a) / 4"
  2.1108 -              if "(b, c) \<in> p" and ne0: "content c \<noteq> 0" for c
  2.1109 -            proof -
  2.1110 -              obtain v where v: "c = cbox v b" and "v \<le> b"
  2.1111 -                using \<open>(b, c) \<in> p\<close> pb by blast
  2.1112 -              then have "v \<ge> a""b \<in> {v.. b}"  
  2.1113 -                using p(3)[OF \<open>(b, c) \<in> p\<close>] by auto
  2.1114 -              moreover have "{v..b} \<subseteq> ball b db"
  2.1115 -                using fineD[OF \<open>?d fine p\<close> \<open>(b, c) \<in> p\<close>] box_real(2) v False by force
  2.1116 -              ultimately show ?thesis
  2.1117 -                using db v by auto
  2.1118 -            qed
  2.1119 -            then show "\<forall>x. x \<in> ?B b \<longrightarrow> 
  2.1120 -                           norm ((\<lambda>(x, k). content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) x) 
  2.1121 -                           \<le> e * (b - a) / 4"
  2.1122 -              by auto
  2.1123 -          qed (insert p(1) ab e, auto simp add: field_simps)
  2.1124 +            also have "... = e * (b-a)/2"
  2.1125 +              by simp
  2.1126 +            finally show "norm (\<Sum>(x,k)\<in>p \<inter> ?C.
  2.1127 +                        content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \<le> e * (b-a)/2" .
  2.1128 +          qed
  2.1129 +          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"
  2.1130 +            apply (rule * [OF sum.mono_neutral_right[OF pA(2)]])
  2.1131 +            using 1 2 by (auto simp: split_paired_all)
  2.1132          qed
  2.1133 -        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"
  2.1134 -          apply (rule * [OF sum.mono_neutral_right[OF pA(2)]])
  2.1135 -          using 1 2 by (auto simp: split_paired_all)
  2.1136 +        also have "... = (\<Sum>n\<in>p. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k))/2"
  2.1137 +          unfolding sum_distrib_left[symmetric]
  2.1138 +          apply (subst additive_tagged_division_1[OF \<open>a \<le> b\<close> ptag])
  2.1139 +          by auto
  2.1140 +        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)))
  2.1141 +                \<le> (\<Sum>n\<in>p. e * (case n of (x, K) \<Rightarrow> Sup K - Inf K))/2" .
  2.1142 +        have le2: "\<And>x s1 s2::real. 0 \<le> s1 \<Longrightarrow> x \<le> (s1 + s2)/2 \<Longrightarrow> x - s1 \<le> s2/2"
  2.1143 +          by auto
  2.1144 +        show ?thesis
  2.1145 +          apply (rule le2 [OF sum_nonneg])
  2.1146 +          using ge0 apply force
  2.1147 +          unfolding sum.union_disjoint[OF pA(2-), symmetric] pA(1)[symmetric]
  2.1148 +          by (metis norm_le)
  2.1149        qed
  2.1150 -      also have "... = (\<Sum>n\<in>p. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k)) / 2"
  2.1151 -        unfolding sum_distrib_left[symmetric]
  2.1152 -        apply (subst additive_tagged_division_1[OF \<open>a \<le> b\<close> ptag])
  2.1153 -        by auto
  2.1154 -      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)))
  2.1155 -                \<le> (\<Sum>n\<in>p. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k)) / 2" .
  2.1156 -      have *: "\<And>x s1 s2::real. 0 \<le> s1 \<Longrightarrow> x \<le> (s1 + s2) / 2 \<Longrightarrow> x - s1 \<le> s2 / 2"
  2.1157 -        by auto
  2.1158 -      show ?thesis
  2.1159 -        apply (rule * [OF sum_nonneg])
  2.1160 -        using ge0 apply force
  2.1161 -        unfolding sum.union_disjoint[OF pA(2-), symmetric] pA(1)[symmetric]
  2.1162 -        by (metis norm_le)
  2.1163 +      note * = additive_tagged_division_1[OF assms(1) ptag, symmetric]
  2.1164 +      have "norm (\<Sum>(x,K)\<in>p \<inter> ?A \<union> (p - ?A). content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))
  2.1165 +               \<le> e * (\<Sum>(x,K)\<in>p \<inter> ?A \<union> (p - ?A). Sup K - Inf K)"
  2.1166 +        unfolding sum_distrib_left
  2.1167 +        unfolding sum.union_disjoint[OF pA(2-)]
  2.1168 +        using le_xz norm_triangle_le I II by blast
  2.1169 +      then
  2.1170 +      show "norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f' x) - (f b - f a)) \<le> e * content {a..b}"
  2.1171 +        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])
  2.1172      qed
  2.1173 -    have "norm (\<Sum>(x,K)\<in>p \<inter> ?A \<union> (p - ?A). content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))
  2.1174 -               \<le> e * (\<Sum>(x,K)\<in>p \<inter> ?A \<union> (p - ?A). Sup K - Inf K)"
  2.1175 -      unfolding sum_distrib_left
  2.1176 -      unfolding sum.union_disjoint[OF pA(2-)]
  2.1177 -      using ** norm_triangle_le I II by blast
  2.1178 -    then
  2.1179 -    show "norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f' x) - (f b - f a)) \<le> e * content {a..b}"
  2.1180 -      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])
  2.1181    qed
  2.1182  qed
  2.1183  
  2.1184 @@ -3992,12 +3920,9 @@
  2.1185    using vec apply (auto simp: mem_box)
  2.1186    done
  2.1187  
  2.1188 -lemma indefinite_integral_continuous_left:
  2.1189 +proposition indefinite_integral_continuous_left:
  2.1190    fixes f:: "real \<Rightarrow> 'a::banach"
  2.1191 -  assumes intf: "f integrable_on {a..b}"
  2.1192 -    and "a < c"
  2.1193 -    and "c \<le> b"
  2.1194 -    and "e > 0"
  2.1195 +  assumes intf: "f integrable_on {a..b}" and "a < c" "c \<le> b" "e > 0"
  2.1196    obtains d where "d > 0"
  2.1197      and "\<forall>t. c - d < t \<and> t \<le> c \<longrightarrow> norm (integral {a..c} f - integral {a..t} f) < e"
  2.1198  proof -
  2.1199 @@ -4020,14 +3945,14 @@
  2.1200        using \<open>e > 0\<close> that by auto
  2.1201    qed
  2.1202  
  2.1203 +  let ?SUM = "\<lambda>p. (\<Sum>(x,K) \<in> p. content K *\<^sub>R f x)"
  2.1204    have e3: "e/3 > 0"
  2.1205      using \<open>e > 0\<close> by auto
  2.1206    have "f integrable_on {a..c}"
  2.1207      apply (rule integrable_subinterval_real[OF intf])
  2.1208      using \<open>a < c\<close> \<open>c \<le> b\<close> by auto
  2.1209    then obtain d1 where "gauge d1" and d1:
  2.1210 -    "\<And>p. \<lbrakk>p tagged_division_of {a..c}; d1 fine p\<rbrakk> \<Longrightarrow>
  2.1211 -            norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f x) - integral {a..c} f) < e/3"
  2.1212 +    "\<And>p. \<lbrakk>p tagged_division_of {a..c}; d1 fine p\<rbrakk> \<Longrightarrow> norm (?SUM p - integral {a..c} f) < e/3"
  2.1213      using integrable_integral has_integral_real e3 by metis
  2.1214    define d where [abs_def]: "d x = ball x w \<inter> d1 x" for x
  2.1215    have "gauge d"
  2.1216 @@ -4035,132 +3960,102 @@
  2.1217    then obtain k where "0 < k" and k: "ball c k \<subseteq> d c"
  2.1218      by (meson gauge_def open_contains_ball)
  2.1219  
  2.1220 -  let ?d = "min k (c - a) / 2"
  2.1221 -  show ?thesis
  2.1222 -    apply (rule that[of ?d])
  2.1223 -    apply safe
  2.1224 -  proof -
  2.1225 +  let ?d = "min k (c - a)/2"
  2.1226 +  show thesis
  2.1227 +  proof (intro that[of ?d] allI impI, safe)
  2.1228      show "?d > 0"
  2.1229 -      using \<open>0 < k\<close> using assms(2) by auto
  2.1230 +      using \<open>0 < k\<close> \<open>a < c\<close> by auto
  2.1231 +  next
  2.1232      fix t
  2.1233 -    assume as: "c - ?d < t" "t \<le> c"
  2.1234 -    let ?thesis = "norm (integral ({a..c}) f - integral ({a..t}) f) < e"
  2.1235 -    {
  2.1236 -      presume *: "t < c \<Longrightarrow> ?thesis"
  2.1237 -      show ?thesis
  2.1238 -      proof (cases "t = c")
  2.1239 -        case True
  2.1240 -        then show ?thesis
  2.1241 -          by (simp add: \<open>e > 0\<close>)
  2.1242 -      next
  2.1243 -        case False
  2.1244 -        then show ?thesis
  2.1245 -          using "*" \<open>t \<le> c\<close> by linarith
  2.1246 -      qed
  2.1247 -    }
  2.1248 -    assume "t < c"
  2.1249 -
  2.1250 -    have "f integrable_on {a..t}"
  2.1251 -      apply (rule integrable_subinterval_real[OF intf])
  2.1252 -      using \<open>t < c\<close> \<open>c \<le> b\<close> by auto
  2.1253 -    then obtain d2 where d2: "gauge d2"
  2.1254 -      "\<And>p. p tagged_division_of {a..t} \<and> d2 fine p \<Longrightarrow>
  2.1255 -            norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f x) - integral {a..t} f) < e/3"
  2.1256 -      using integrable_integral has_integral_real e3 by metis
  2.1257 -    define d3 where "d3 x = (if x \<le> t then d1 x \<inter> d2 x else d1 x)" for x
  2.1258 -    have "gauge d3"
  2.1259 -      using \<open>gauge d1\<close> \<open>gauge d2\<close> unfolding d3_def gauge_def by auto
  2.1260 -    then obtain p where ptag: "p tagged_division_of {a..t}" and pfine: "d3 fine p"
  2.1261 -      by (metis box_real(2) fine_division_exists)
  2.1262 -    note p'=tagged_division_ofD[OF ptag]
  2.1263 -    have pt: "(x,k)\<in>p \<Longrightarrow> x \<le> t" for x k
  2.1264 -      by (meson atLeastAtMost_iff p'(2) p'(3) subsetCE)
  2.1265 -    with pfine have "d2 fine p"
  2.1266 -      unfolding fine_def d3_def by fastforce
  2.1267 -    then have d2_fin: "norm ((\<Sum>(x, K)\<in>p. content K *\<^sub>R f x) - integral {a..t} f) < e/3"
  2.1268 -      using d2(2) ptag by auto
  2.1269 -    have *: "{a..c} \<inter> {x. x \<le> t} = {a..t}" "{a..c} \<inter> {x. x \<ge> t} = {t..c}"
  2.1270 -      using as by (auto simp add: field_simps)
  2.1271 -
  2.1272 -    have "p \<union> {(c, {t..c})} tagged_division_of {a..c}"
  2.1273 -      apply (rule tagged_division_Un_interval_real[of _ _ _ 1 "t"])
  2.1274 -      using  \<open>t \<le> c\<close> by (auto simp: * ptag tagged_division_of_self_real)
  2.1275 -    moreover
  2.1276 -    have "d1 fine p \<union> {(c, {t..c})}"
  2.1277 -      unfolding fine_def
  2.1278 -    proof safe
  2.1279 -      fix x K y
  2.1280 -      assume "(x,K) \<in> p" and "y \<in> K" then show "y \<in> d1 x"
  2.1281 -        by (metis Int_iff d3_def subsetD fineD pfine)
  2.1282 +    assume t: "c - ?d < t" "t \<le> c"
  2.1283 +    show "norm (integral ({a..c}) f - integral ({a..t}) f) < e"
  2.1284 +    proof (cases "t < c")
  2.1285 +      case False with \<open>t \<le> c\<close> show ?thesis
  2.1286 +        by (simp add: \<open>e > 0\<close>)
  2.1287      next
  2.1288 -      fix x assume "x \<in> {t..c}"
  2.1289 -      then have "dist c x < k"
  2.1290 -        using as(1)
  2.1291 -        by (auto simp add: field_simps dist_real_def)
  2.1292 -      with k show "x \<in> d1 c"
  2.1293 -        unfolding d_def by auto
  2.1294 -    qed  
  2.1295 -    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"
  2.1296 -      using d1 by metis
  2.1297 -
  2.1298 -    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)) -
  2.1299 -      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"
  2.1300 -      "e = (e/3 + e/3) + e/3"
  2.1301 -      by auto
  2.1302 -    have **: "(\<Sum>(x, k)\<in>p \<union> {(c, {t..c})}. content k *\<^sub>R f x) =
  2.1303 -      (c - t) *\<^sub>R f c + (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)"
  2.1304 -    proof -
  2.1305 -      have **: "\<And>x F. F \<union> {x} = insert x F"
  2.1306 -        by auto
  2.1307 -      have "(c, cbox t c) \<notin> p"
  2.1308 -      proof (safe, goal_cases)
  2.1309 -        case prems: 1
  2.1310 -        from p'(2-3)[OF prems] have "c \<in> cbox a t"
  2.1311 -          by auto
  2.1312 -        then show False using \<open>t < c\<close>
  2.1313 -          by auto
  2.1314 +      case True
  2.1315 +      have "f integrable_on {a..t}"
  2.1316 +        apply (rule integrable_subinterval_real[OF intf])
  2.1317 +        using \<open>t < c\<close> \<open>c \<le> b\<close> by auto
  2.1318 +      then obtain d2 where d2: "gauge d2"
  2.1319 +        "\<And>p. p tagged_division_of {a..t} \<and> d2 fine p \<Longrightarrow> norm (?SUM p - integral {a..t} f) < e/3"
  2.1320 +        using integrable_integral has_integral_real e3 by metis
  2.1321 +      define d3 where "d3 x = (if x \<le> t then d1 x \<inter> d2 x else d1 x)" for x
  2.1322 +      have "gauge d3"
  2.1323 +        using \<open>gauge d1\<close> \<open>gauge d2\<close> unfolding d3_def gauge_def by auto
  2.1324 +      then obtain p where ptag: "p tagged_division_of {a..t}" and pfine: "d3 fine p"
  2.1325 +        by (metis box_real(2) fine_division_exists)
  2.1326 +      note p' = tagged_division_ofD[OF ptag]
  2.1327 +      have pt: "(x,K)\<in>p \<Longrightarrow> x \<le> t" for x K
  2.1328 +        by (meson atLeastAtMost_iff p'(2) p'(3) subsetCE)
  2.1329 +      with pfine have "d2 fine p"
  2.1330 +        unfolding fine_def d3_def by fastforce
  2.1331 +      then have d2_fin: "norm (?SUM p - integral {a..t} f) < e/3"
  2.1332 +        using d2(2) ptag by auto
  2.1333 +      have eqs: "{a..c} \<inter> {x. x \<le> t} = {a..t}" "{a..c} \<inter> {x. x \<ge> t} = {t..c}"
  2.1334 +        using t by (auto simp add: field_simps)
  2.1335 +      have "p \<union> {(c, {t..c})} tagged_division_of {a..c}"
  2.1336 +        apply (rule tagged_division_Un_interval_real[of _ _ _ 1 "t"])
  2.1337 +        using  \<open>t \<le> c\<close> by (auto simp: eqs ptag tagged_division_of_self_real)
  2.1338 +      moreover
  2.1339 +      have "d1 fine p \<union> {(c, {t..c})}"
  2.1340 +        unfolding fine_def
  2.1341 +      proof safe
  2.1342 +        fix x K y
  2.1343 +        assume "(x,K) \<in> p" and "y \<in> K" then show "y \<in> d1 x"
  2.1344 +          by (metis Int_iff d3_def subsetD fineD pfine)
  2.1345 +      next
  2.1346 +        fix x assume "x \<in> {t..c}"
  2.1347 +        then have "dist c x < k"
  2.1348 +          using t(1) by (auto simp add: field_simps dist_real_def)
  2.1349 +        with k show "x \<in> d1 c"
  2.1350 +          unfolding d_def by auto
  2.1351 +      qed  
  2.1352 +      ultimately have d1_fin: "norm (?SUM(p \<union> {(c, {t..c})}) - integral {a..c} f) < e/3"
  2.1353 +        using d1 by metis
  2.1354 +      have SUMEQ: "?SUM(p \<union> {(c, {t..c})}) = (c - t) *\<^sub>R f c + ?SUM p"
  2.1355 +      proof -
  2.1356 +        have "?SUM(p \<union> {(c, {t..c})}) = (content{t..c} *\<^sub>R f c) + ?SUM p"
  2.1357 +        proof (subst sum.union_disjoint)
  2.1358 +          show "p \<inter> {(c, {t..c})} = {}"
  2.1359 +            using \<open>t < c\<close> pt by force
  2.1360 +        qed (use p'(1) in auto)
  2.1361 +        also have "... = (c - t) *\<^sub>R f c + ?SUM p"
  2.1362 +          using \<open>t \<le> c\<close> by auto
  2.1363 +        finally show ?thesis .
  2.1364        qed
  2.1365 -      then show ?thesis
  2.1366 -        unfolding ** box_real
  2.1367 -        apply -
  2.1368 -        apply (subst sum.insert)
  2.1369 -        apply (rule p')
  2.1370 -        unfolding split_conv
  2.1371 -        defer
  2.1372 -        apply (subst content_real)
  2.1373 -        using as(2)
  2.1374 -        apply auto
  2.1375 -        done
  2.1376 -    qed
  2.1377 -    have ***: "c - w < t \<and> t < c"
  2.1378 -    proof -
  2.1379        have "c - k < t"
  2.1380 -        using \<open>k>0\<close> as(1) by (auto simp add: field_simps)
  2.1381 +        using \<open>k>0\<close> t(1) by (auto simp add: field_simps)
  2.1382        moreover have "k \<le> w"
  2.1383 -        apply (rule ccontr)
  2.1384 -        using k
  2.1385 -        unfolding subset_eq
  2.1386 -        apply (erule_tac x="c + ((k + w)/2)" in ballE)
  2.1387 -        unfolding d_def
  2.1388 -        using \<open>k > 0\<close> \<open>w > 0\<close>
  2.1389 -        apply (auto simp add: field_simps not_le not_less dist_real_def)
  2.1390 -        done
  2.1391 -      ultimately show ?thesis using \<open>t < c\<close>
  2.1392 +      proof (rule ccontr)
  2.1393 +        assume "\<not> k \<le> w"
  2.1394 +        then have "c + (k + w) / 2 \<notin> d c"
  2.1395 +          by (auto simp add: field_simps not_le not_less dist_real_def d_def)
  2.1396 +        then have "c + (k + w) / 2 \<notin> ball c k"
  2.1397 +          using k by blast
  2.1398 +        then show False
  2.1399 +          using \<open>0 < w\<close> \<open>\<not> k \<le> w\<close> dist_real_def by auto
  2.1400 +      qed
  2.1401 +      ultimately have cwt: "c - w < t"
  2.1402          by (auto simp add: field_simps)
  2.1403 +      have eq: "integral {a..c} f - integral {a..t} f = -(((c - t) *\<^sub>R f c + ?SUM p) -
  2.1404 +             integral {a..c} f) + (?SUM p - integral {a..t} f) + (c - t) *\<^sub>R f c"
  2.1405 +        by auto
  2.1406 +      have "norm (integral {a..c} f - integral {a..t} f) < e/3 + e/3 + e/3"
  2.1407 +        unfolding eq
  2.1408 +      proof (intro norm_triangle_lt add_strict_mono)
  2.1409 +        show "norm (- ((c - t) *\<^sub>R f c + ?SUM p - integral {a..c} f)) < e/3"
  2.1410 +          by (metis SUMEQ d1_fin norm_minus_cancel)
  2.1411 +        show "norm (?SUM p - integral {a..t} f) < e/3"
  2.1412 +          using d2_fin by blast
  2.1413 +        show "norm ((c - t) *\<^sub>R f c) < e/3"
  2.1414 +          using w cwt \<open>t < c\<close> by (auto simp add: field_simps)
  2.1415 +      qed
  2.1416 +      then show ?thesis by simp
  2.1417      qed
  2.1418 -    show ?thesis
  2.1419 -      unfolding *(1)
  2.1420 -      apply (subst *(2))
  2.1421 -      apply (rule norm_triangle_lt add_strict_mono)+
  2.1422 -      apply (metis "**" d1_fin norm_minus_cancel)
  2.1423 -      using d2_fin apply blast
  2.1424 -      using w ***
  2.1425 -      apply (auto simp add: field_simps)
  2.1426 -      done
  2.1427    qed
  2.1428  qed
  2.1429  
  2.1430 -
  2.1431  lemma indefinite_integral_continuous_right:
  2.1432    fixes f :: "real \<Rightarrow> 'a::banach"
  2.1433    assumes "f integrable_on {a..b}"
  2.1434 @@ -4424,97 +4319,66 @@
  2.1435    assumes intf: "(f has_integral i) (cbox c d)"
  2.1436      and cb: "cbox c d \<subseteq> cbox a b"
  2.1437    shows "((\<lambda>x. if x \<in> box c d then f x else 0) has_integral i) (cbox a b)"
  2.1438 -proof -
  2.1439 +proof (cases "cbox c d = {}")
  2.1440 +  case True
  2.1441 +  then have "box c d = {}"
  2.1442 +    by (metis bot.extremum_uniqueI box_subset_cbox)
  2.1443 +  then show ?thesis
  2.1444 +    using True intf by auto
  2.1445 +next
  2.1446 +  case False
  2.1447 +  then obtain p where pdiv: "p division_of cbox a b" and inp: "cbox c d \<in> p"
  2.1448 +    using cb partial_division_extend_1 by blast
  2.1449    define g where [abs_def]: "g x = (if x \<in>box c d then f x else 0)" for x
  2.1450 -  {
  2.1451 -    presume *: "cbox c d \<noteq> {} \<Longrightarrow> ?thesis"
  2.1452 -    show ?thesis
  2.1453 -      apply cases
  2.1454 -      apply (rule *)
  2.1455 -      apply assumption
  2.1456 -    proof goal_cases
  2.1457 -      case prems: 1
  2.1458 -      then have *: "box c d = {}"
  2.1459 -        by (metis bot.extremum_uniqueI box_subset_cbox)
  2.1460 -      show ?thesis
  2.1461 -        using assms(1)
  2.1462 -        unfolding *
  2.1463 -        using prems
  2.1464 -        by auto
  2.1465 -    qed
  2.1466 -  }
  2.1467 -  assume "cbox c d \<noteq> {}"
  2.1468 -  then obtain p where p: "p division_of cbox a b" "cbox c d \<in> p"
  2.1469 -    using cb partial_division_extend_1 by blast
  2.1470    interpret operative "lift_option plus" "Some (0 :: 'b)"
  2.1471      "\<lambda>i. if g integrable_on i then Some (integral i g) else None"
  2.1472      by (fact operative_integralI)
  2.1473 -  note operat = division
  2.1474 -    [OF p(1), symmetric]
  2.1475 -  let ?P = "(if g integrable_on cbox a b then Some (integral (cbox a b) g) else None) = Some i"
  2.1476 -  {
  2.1477 -    presume "?P"
  2.1478 -    then have "g integrable_on cbox a b \<and> integral (cbox a b) g = i"
  2.1479 -      apply -
  2.1480 -      apply cases
  2.1481 -      apply (subst(asm) if_P)
  2.1482 -      apply assumption
  2.1483 -      apply auto
  2.1484 -      done
  2.1485 -    then show ?thesis
  2.1486 -      using integrable_integral
  2.1487 -      unfolding g_def
  2.1488 -      by auto
  2.1489 -  }
  2.1490 -  let ?F = F
  2.1491 -  have iterate:"?F (\<lambda>i. if g integrable_on i then Some (integral i g) else None) (p - {cbox c d}) = Some 0"
  2.1492 -  proof (intro neutral ballI)
  2.1493 -    fix x
  2.1494 -    assume x: "x \<in> p - {cbox c d}"
  2.1495 -    then have "x \<in> p"
  2.1496 -      by auto
  2.1497 -    note div = division_ofD(2-5)[OF p(1) this]
  2.1498 -    then obtain u v where uv: "x = cbox u v" by blast
  2.1499 -    have "interior x \<inter> interior (cbox c d) = {}"
  2.1500 -      using div(4)[OF p(2)] x by auto
  2.1501 -    then have "(g has_integral 0) x"
  2.1502 -      unfolding uv
  2.1503 -      using has_integral_spike_interior[where f="\<lambda>x. 0"]
  2.1504 -      by (metis (no_types, lifting) disjoint_iff_not_equal g_def has_integral_0_eq interior_cbox)
  2.1505 -    then show "(if g integrable_on x then Some (integral x g) else None) = Some 0"
  2.1506 -      by auto
  2.1507 +  note operat = division [OF pdiv, symmetric]
  2.1508 +  show ?thesis
  2.1509 +  proof (cases "(g has_integral i) (cbox a b)")
  2.1510 +    case True then show ?thesis
  2.1511 +      by (simp add: g_def)
  2.1512 +  next
  2.1513 +    case False
  2.1514 +    have iterate:"F (\<lambda>i. if g integrable_on i then Some (integral i g) else None) (p - {cbox c d}) = Some 0"
  2.1515 +    proof (intro neutral ballI)
  2.1516 +      fix x
  2.1517 +      assume x: "x \<in> p - {cbox c d}"
  2.1518 +      then have "x \<in> p"
  2.1519 +        by auto
  2.1520 +      then obtain u v where uv: "x = cbox u v"
  2.1521 +        using pdiv by blast
  2.1522 +      have "interior x \<inter> interior (cbox c d) = {}"
  2.1523 +        using pdiv inp x by blast 
  2.1524 +      then have "(g has_integral 0) x"
  2.1525 +        unfolding uv using has_integral_spike_interior[where f="\<lambda>x. 0"]
  2.1526 +        by (metis (no_types, lifting) disjoint_iff_not_equal g_def has_integral_0_eq interior_cbox)
  2.1527 +      then show "(if g integrable_on x then Some (integral x g) else None) = Some 0"
  2.1528 +        by auto
  2.1529 +    qed
  2.1530 +    interpret comm_monoid_set "lift_option plus" "Some (0 :: 'b)"
  2.1531 +      by (intro comm_monoid_set.intro comm_monoid_lift_option add.comm_monoid_axioms)
  2.1532 +    have intg: "g integrable_on cbox c d"
  2.1533 +      using integrable_spike_interior[where f=f]
  2.1534 +      by (meson g_def has_integral_integrable intf)
  2.1535 +    moreover have "integral (cbox c d) g = i"
  2.1536 +    proof (rule has_integral_unique[OF has_integral_spike_interior intf])
  2.1537 +      show "\<And>x. x \<in> box c d \<Longrightarrow> f x = g x"
  2.1538 +        by (auto simp: g_def)
  2.1539 +      show "(g has_integral integral (cbox c d) g) (cbox c d)"
  2.1540 +        by (rule integrable_integral[OF intg])
  2.1541 +    qed
  2.1542 +    ultimately have "F (\<lambda>A. if g integrable_on A then Some (integral A g) else None) p = Some i"
  2.1543 +      by (metis (full_types, lifting) division_of_finite inp iterate pdiv remove right_neutral)
  2.1544 +    then
  2.1545 +    have "(g has_integral i) (cbox a b)"
  2.1546 +      by (metis integrable_on_def integral_unique operat option.inject option.simps(3))
  2.1547 +    with False show ?thesis
  2.1548 +      by blast
  2.1549    qed
  2.1550 -
  2.1551 -  have *: "p = insert (cbox c d) (p - {cbox c d})"
  2.1552 -    using p by auto
  2.1553 -  interpret comm_monoid_set "lift_option plus" "Some (0 :: 'b)"
  2.1554 -    apply (rule comm_monoid_set.intro)
  2.1555 -    apply (rule comm_monoid_lift_option)
  2.1556 -    apply (rule add.comm_monoid_axioms)
  2.1557 -    done
  2.1558 -  have **: "g integrable_on cbox c d"
  2.1559 -    apply (rule integrable_spike_interior[where f=f])
  2.1560 -    unfolding g_def  using assms(1)
  2.1561 -    apply auto
  2.1562 -    done
  2.1563 -  moreover
  2.1564 -  have "integral (cbox c d) g = i"
  2.1565 -    apply (rule has_integral_unique[OF _ assms(1)])
  2.1566 -    apply (rule has_integral_spike_interior[where f=g])
  2.1567 -    defer
  2.1568 -    apply (rule integrable_integral[OF **])
  2.1569 -    unfolding g_def
  2.1570 -    apply auto
  2.1571 -    done
  2.1572 -  ultimately show ?P
  2.1573 -    unfolding operat
  2.1574 -    using p
  2.1575 -    apply (subst *)
  2.1576 -    apply (subst insert)
  2.1577 -    apply (simp_all add: division_of_finite iterate)
  2.1578 -    done
  2.1579  qed
  2.1580  
  2.1581 +
  2.1582  lemma has_integral_restrict_closed_subinterval:
  2.1583    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
  2.1584    assumes "(f has_integral i) (cbox c d)"
  2.1585 @@ -4539,28 +4403,21 @@
  2.1586    case False
  2.1587    let ?g = "\<lambda>x. if x \<in> cbox c d then f x else 0"
  2.1588    show ?thesis
  2.1589 -    apply rule
  2.1590 -    defer
  2.1591 -    apply (rule has_integral_restrict_closed_subinterval[OF _ assms])
  2.1592 -    apply assumption
  2.1593 -  proof -
  2.1594 +  proof 
  2.1595      assume ?l
  2.1596      then have "?g integrable_on cbox c d"
  2.1597        using assms has_integral_integrable integrable_subinterval by blast
  2.1598 -    then have *: "f integrable_on cbox c d"
  2.1599 +    then have "f integrable_on cbox c d"
  2.1600        apply -
  2.1601        apply (rule integrable_eq)
  2.1602        apply auto
  2.1603        done
  2.1604 -    then have "i = integral (cbox c d) f"
  2.1605 -      apply -
  2.1606 -      apply (rule has_integral_unique)
  2.1607 -      apply (rule \<open>?l\<close>)
  2.1608 -      apply (rule has_integral_restrict_closed_subinterval[OF _ assms])
  2.1609 -      apply auto
  2.1610 -      done
  2.1611 -    then show ?r
  2.1612 -      using * by auto
  2.1613 +    moreover then have "i = integral (cbox c d) f"
  2.1614 +      by (meson \<open>((\<lambda>x. if x \<in> cbox c d then f x else 0) has_integral i) (cbox a b)\<close> assms has_integral_restrict_closed_subinterval has_integral_unique integrable_integral)
  2.1615 +    ultimately show ?r by auto
  2.1616 +  next
  2.1617 +    assume ?r then show ?l
  2.1618 +      by (rule has_integral_restrict_closed_subinterval[OF _ assms])
  2.1619    qed
  2.1620  qed auto
  2.1621  
  2.1622 @@ -4672,10 +4529,9 @@
  2.1623  
  2.1624  lemma integral_nonneg:
  2.1625    fixes f :: "'n::euclidean_space \<Rightarrow> real"
  2.1626 -  assumes "f integrable_on S"
  2.1627 -    and "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f x"
  2.1628 +  assumes f: "f integrable_on S" and 0: "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f x"
  2.1629    shows "0 \<le> integral S f"
  2.1630 -  by (rule has_integral_nonneg[OF assms(1)[unfolded has_integral_integral] assms(2)])
  2.1631 +  by (rule has_integral_nonneg[OF f[unfolded has_integral_integral] 0])
  2.1632  
  2.1633  
  2.1634  text \<open>Hence a general restriction property.\<close>
  2.1635 @@ -5033,11 +4889,11 @@
  2.1636      if "e > 0" for e
  2.1637    proof -
  2.1638      have *: "e/2 > 0" using that by auto
  2.1639 -    then obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> norm (i - integral (?cube n) ?F) < e / 2"
  2.1640 +    then obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> norm (i - integral (?cube n) ?F) < e/2"
  2.1641        using i[THEN LIMSEQ_D, simplified norm_minus_commute] by meson
  2.1642      obtain B where "0 < B" 
  2.1643        and B: "\<And>a b c d. \<lbrakk>ball 0 B \<subseteq> cbox a b; ball 0 B \<subseteq> cbox c d\<rbrakk> \<Longrightarrow>
  2.1644 -                  norm (integral (cbox a b) ?F - integral (cbox c d) ?F) < e / 2"
  2.1645 +                  norm (integral (cbox a b) ?F - integral (cbox c d) ?F) < e/2"
  2.1646        using rhs * by meson
  2.1647      let ?B = "max (real N) B"
  2.1648      show ?thesis
  2.1649 @@ -6017,9 +5873,9 @@
  2.1650          proof (rule *)
  2.1651            show "\<bar>integral (cbox a b) (?f N) - i\<bar> < e/2"
  2.1652            proof (rule abs_triangle_half_l)
  2.1653 -            show "\<bar>integral (cbox a b) (?f N) - integral S (f N)\<bar> < e/2 / 2"
  2.1654 +            show "\<bar>integral (cbox a b) (?f N) - integral S (f N)\<bar> < e/2/2"
  2.1655                using B[OF ab] by simp
  2.1656 -            show "abs (i - integral S (f N)) < e/2 / 2"
  2.1657 +            show "abs (i - integral S (f N)) < e/2/2"
  2.1658                using N by (simp add: abs_minus_commute)
  2.1659            qed
  2.1660            show "\<bar>integral (cbox a b) (?f (M + N)) - integral (cbox a b) ?g\<bar> < e/2"
  2.1661 @@ -6953,7 +6809,7 @@
  2.1662          also have "norm (t1 - x1, t2 - x2) < k"
  2.1663            using xuvwz ls uwvz_sub unfolding ball_def
  2.1664            by (force simp add: cbox_Pair_eq dist_norm )
  2.1665 -        finally have "norm (f (x1,x2) - f (t1,t2)) \<le> e/content ?CBOX / 2"
  2.1666 +        finally have "norm (f (x1,x2) - f (t1,t2)) \<le> e/content ?CBOX/2"
  2.1667            using nf [OF t x]  by simp
  2.1668        } note nf' = this
  2.1669        have f_int_uwvz: "f integrable_on cbox (u,w) (v,z)"
  2.1670 @@ -6962,9 +6818,9 @@
  2.1671          using assms continuous_on_subset uwvz_sub
  2.1672          by (blast intro: continuous_on_imp_integrable_on_Pair1)
  2.1673        have 1: "norm (integral (cbox (u,w) (v,z)) f - integral (cbox (u,w) (v,z)) (\<lambda>x. f (t1,t2)))
  2.1674 -         \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
  2.1675 +         \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX/2"
  2.1676          apply (simp only: integral_diff [symmetric] f_int_uwvz integrable_const)
  2.1677 -        apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX / 2"]])
  2.1678 +        apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX/2"]])
  2.1679          using cbp \<open>0 < e/content ?CBOX\<close> nf'
  2.1680          apply (auto simp: integrable_diff f_int_uwvz integrable_const)
  2.1681          done
  2.1682 @@ -6973,24 +6829,24 @@
  2.1683        have normint_wz:
  2.1684           "\<And>x. x \<in> cbox u v \<Longrightarrow>
  2.1685                 norm (integral (cbox w z) (\<lambda>y. f (x, y)) - integral (cbox w z) (\<lambda>y. f (t1, t2)))
  2.1686 -               \<le> e * content (cbox w z) / content (cbox (a, c) (b, d)) / 2"
  2.1687 +               \<le> e * content (cbox w z) / content (cbox (a, c) (b, d))/2"
  2.1688          apply (simp only: integral_diff [symmetric] f_int_uv integrable_const)
  2.1689 -        apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX / 2"]])
  2.1690 +        apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX/2"]])
  2.1691          using cbp \<open>0 < e/content ?CBOX\<close> nf'
  2.1692          apply (auto simp: integrable_diff f_int_uv integrable_const)
  2.1693          done
  2.1694        have "norm (integral (cbox u v)
  2.1695                 (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y)) - integral (cbox w z) (\<lambda>y. f (t1,t2))))
  2.1696 -            \<le> e * content (cbox w z) / content ?CBOX / 2 * content (cbox u v)"
  2.1697 +            \<le> e * content (cbox w z) / content ?CBOX/2 * content (cbox u v)"
  2.1698          apply (rule integrable_bound [OF _ _ normint_wz])
  2.1699          using cbp \<open>0 < e/content ?CBOX\<close>
  2.1700          apply (auto simp: divide_simps content_pos_le integrable_diff int_integrable integrable_const)
  2.1701          done
  2.1702 -      also have "... \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
  2.1703 +      also have "... \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX/2"
  2.1704          by (simp add: content_Pair divide_simps)
  2.1705        finally have 2: "norm (integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y))) -
  2.1706                        integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (t1,t2))))
  2.1707 -                \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
  2.1708 +                \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX/2"
  2.1709          by (simp only: integral_diff [symmetric] int_integrable integrable_const)
  2.1710        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
  2.1711          using norm_triangle_mono [of "x-y'" "e/2" "y'-y" "e/2"] real_sum_of_halves