author paulson Mon, 26 Jun 2017 14:26:03 +0100 changeset 66192 e5b84854baa4 parent 66191 d91108ba9474 child 66193 6e6eeef63589
A few renamings and several tidied-up proofs
```--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sat Jun 24 21:23:48 2017 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Jun 26 14:26:03 2017 +0100
@@ -3790,7 +3790,7 @@
have "exp (- (integral {a..t} (\<lambda>x. ?D\<gamma> x / (\<gamma> x - z)))) * (\<gamma> t - z) =\<gamma> a - z"
apply (rule has_derivative_zero_unique_strong_interval [of "{a,b} \<union> k" a b])
using t
-      apply (auto intro!: * continuous_intros fink cong indefinite_integral_continuous [OF vg_int]  simp add: ab)+
+      apply (auto intro!: * continuous_intros fink cong indefinite_integral_continuous_1 [OF vg_int]  simp add: ab)+
done
}
with ab show ?thesis2
@@ -3865,7 +3865,7 @@
apply (rule IVT')
-    apply (intro continuous_intros indefinite_integral_continuous winding_number_exp_integral [OF gpd]; simp)
+    apply (intro continuous_intros indefinite_integral_continuous_1 winding_number_exp_integral [OF gpd]; simp)
done
then obtain t where t:     "t \<in> {0..1}"
and eqArg: "Im (integral {0..t} (\<lambda>x. vector_derivative \<gamma> (at x)/(\<gamma> x - z))) = Arg r"
@@ -4271,7 +4271,7 @@
[where f = "\<lambda>x. 1 / (2*pi*\<i>) *
integral {0..x} (\<lambda>t. 1/(\<gamma> t - z) * vector_derivative \<gamma> (at t))"])
apply (rule continuous_intros)+
-    apply (rule indefinite_integral_continuous)
+    apply (rule indefinite_integral_continuous_1)
apply (rule contour_integrable_inversediff [OF assms, unfolded contour_integrable_on])
using assms
```--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sat Jun 24 21:23:48 2017 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Jun 26 14:26:03 2017 +0100
@@ -1648,7 +1648,7 @@
by auto
fix p
assume "p tagged_division_of (cbox a b)" and "?g fine p"
-      note p = this(1) conjunctD2[OF this(2)[unfolded fine_inter]]
+      note p = this(1) conjunctD2[OF this(2)[unfolded fine_Int]]
note p' = tagged_division_ofD[OF p(1)]
define p' where "p' = {(x,k) | x k. \<exists>i l. x \<in> i \<and> i \<in> d \<and> (x,l) \<in> p \<and> k = i \<inter> l}"
have gp': "g fine p'"
@@ -2197,7 +2197,7 @@
obtain p where
p: "p tagged_division_of (cbox a b)" "d1 fine p" "d2 fine p"
by (rule fine_division_exists [OF gauge_Int [OF d1(1) d2(1)], of a b])
have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> ?S \<longrightarrow> \<bar>sf - si\<bar> < e / 2 \<longrightarrow>
\<bar>sf' - di\<bar> < e / 2 \<longrightarrow> di < ?S + e"
by arith
@@ -2280,6 +2280,264 @@
using f by (auto intro: has_integral_implies_lebesgue_measurable simp: integrable_on_def)
qed (use le in \<open>auto intro!: always_eventually split: split_indicator\<close>)

+subsection \<open>Componentwise\<close>
+
+proposition absolutely_integrable_componentwise_iff:
+  shows "f absolutely_integrable_on A \<longleftrightarrow> (\<forall>b\<in>Basis. (\<lambda>x. f x \<bullet> b) absolutely_integrable_on A)"
+proof -
+  have *: "(\<lambda>x. norm (f x)) integrable_on A \<longleftrightarrow> (\<forall>b\<in>Basis. (\<lambda>x. norm (f x \<bullet> b)) integrable_on A)"
+          if "f integrable_on A"
+  proof -
+    have 1: "\<And>i. \<lbrakk>(\<lambda>x. norm (f x)) integrable_on A; i \<in> Basis\<rbrakk>
+                 \<Longrightarrow> (\<lambda>x. f x \<bullet> i) absolutely_integrable_on A"
+      apply (rule absolutely_integrable_integrable_bound [where g = "\<lambda>x. norm(f x)"])
+      using Basis_le_norm integrable_component that apply fastforce+
+      done
+    have 2: "\<forall>i\<in>Basis. (\<lambda>x. \<bar>f x \<bullet> i\<bar>) integrable_on A \<Longrightarrow> f absolutely_integrable_on A"
+      apply (rule absolutely_integrable_integrable_bound [where g = "\<lambda>x. \<Sum>i\<in>Basis. norm (f x \<bullet> i)"])
+      using norm_le_l1 that apply (force intro: integrable_sum)+
+      done
+    show ?thesis
+      apply auto
+       apply (metis (full_types) absolutely_integrable_on_def set_integrable_abs 1)
+      apply (metis (full_types) absolutely_integrable_on_def 2)
+      done
+  qed
+  show ?thesis
+    unfolding absolutely_integrable_on_def
+    by (simp add:  integrable_componentwise_iff [symmetric] ball_conj_distrib * cong: conj_cong)
+qed
+
+lemma absolutely_integrable_componentwise:
+  shows "(\<And>b. b \<in> Basis \<Longrightarrow> (\<lambda>x. f x \<bullet> b) absolutely_integrable_on A) \<Longrightarrow> f absolutely_integrable_on A"
+
+lemma absolutely_integrable_component:
+  "f absolutely_integrable_on A \<Longrightarrow> (\<lambda>x. f x \<bullet> (b :: 'b :: euclidean_space)) absolutely_integrable_on A"
+  by (drule absolutely_integrable_linear[OF _ bounded_linear_inner_left[of b]]) (simp add: o_def)
+
+
+lemma absolutely_integrable_scaleR_left:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+    assumes "f absolutely_integrable_on S"
+  shows "(\<lambda>x. c *\<^sub>R f x) absolutely_integrable_on S"
+proof -
+  have "(\<lambda>x. c *\<^sub>R x) o f absolutely_integrable_on S"
+    apply (rule absolutely_integrable_linear [OF assms])
+  then show ?thesis by simp
+qed
+
+lemma absolutely_integrable_scaleR_right:
+  assumes "f absolutely_integrable_on S"
+  shows "(\<lambda>x. f x *\<^sub>R c) absolutely_integrable_on S"
+  using assms by blast
+
+lemma absolutely_integrable_norm:
+  fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
+  assumes "f absolutely_integrable_on S"
+  shows "(norm o f) absolutely_integrable_on S"
+  using assms unfolding absolutely_integrable_on_def by auto
+
+lemma absolutely_integrable_abs:
+  fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
+  assumes "f absolutely_integrable_on S"
+  shows "(\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x \<bullet> i\<bar> *\<^sub>R i) absolutely_integrable_on S"
+        (is "?g absolutely_integrable_on S")
+proof -
+  have eq: "?g =
+        (\<lambda>x. \<Sum>i\<in>Basis. ((\<lambda>y. \<Sum>j\<in>Basis. if j = i then y *\<^sub>R j else 0) \<circ>
+               (\<lambda>x. norm(\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f) x)"
+  have *: "(\<lambda>y. \<Sum>j\<in>Basis. if j = i then y *\<^sub>R j else 0) \<circ>
+           (\<lambda>x. norm (\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f
+           absolutely_integrable_on S"
+        if "i \<in> Basis" for i
+  proof -
+    have "bounded_linear (\<lambda>y. \<Sum>j\<in>Basis. if j = i then y *\<^sub>R j else 0)"
+      by (simp add: linear_linear algebra_simps linearI)
+    moreover have "(\<lambda>x. norm (\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f
+                   absolutely_integrable_on S"
+      unfolding o_def
+      apply (rule absolutely_integrable_norm [unfolded o_def])
+      using assms \<open>i \<in> Basis\<close>
+      apply (auto simp: algebra_simps dest: absolutely_integrable_component[where b=i])
+      done
+    ultimately show ?thesis
+      by (subst comp_assoc) (blast intro: absolutely_integrable_linear)
+  qed
+  show ?thesis
+    apply (rule ssubst [OF eq])
+    apply (rule absolutely_integrable_sum)
+     apply (force simp: intro!: *)+
+    done
+qed
+
+lemma abs_absolutely_integrableI_1:
+  fixes f :: "'a :: euclidean_space \<Rightarrow> real"
+  assumes f: "f integrable_on A" and "(\<lambda>x. \<bar>f x\<bar>) integrable_on A"
+  shows "f absolutely_integrable_on A"
+  by (rule absolutely_integrable_integrable_bound [OF _ assms]) auto
+
+
+lemma abs_absolutely_integrableI:
+  assumes f: "f integrable_on S" and fcomp: "(\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x \<bullet> i\<bar> *\<^sub>R i) integrable_on S"
+  shows "f absolutely_integrable_on S"
+proof -
+  have "(\<lambda>x. (f x \<bullet> i) *\<^sub>R i) absolutely_integrable_on S" if "i \<in> Basis" for i
+  proof -
+    have "(\<lambda>x. \<bar>f x \<bullet> i\<bar>) integrable_on S"
+      using assms integrable_component [OF fcomp, where y=i] that by simp
+    then have "(\<lambda>x. f x \<bullet> i) absolutely_integrable_on S"
+      apply -
+      apply (rule abs_absolutely_integrableI_1, auto)
+      by (simp add: f integrable_component)
+    then show ?thesis
+      by (rule absolutely_integrable_scaleR_right)
+  qed
+  then have "(\<lambda>x. \<Sum>i\<in>Basis. (f x \<bullet> i) *\<^sub>R i) absolutely_integrable_on S"
+  then show ?thesis
+qed
+
+
+lemma absolutely_integrable_abs_iff:
+   "f absolutely_integrable_on S \<longleftrightarrow>
+    f integrable_on S \<and> (\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x \<bullet> i\<bar> *\<^sub>R i) integrable_on S"
+    (is "?lhs = ?rhs")
+proof
+  assume ?lhs then show ?rhs
+    using absolutely_integrable_abs absolutely_integrable_on_def by blast
+next
+  assume ?rhs
+  moreover
+  have "(\<lambda>x. if x \<in> S then \<Sum>i\<in>Basis. \<bar>f x \<bullet> i\<bar> *\<^sub>R i else 0) = (\<lambda>x. \<Sum>i\<in>Basis. \<bar>(if x \<in> S then f x else 0) \<bullet> i\<bar> *\<^sub>R i)"
+    by force
+  ultimately show ?lhs
+    by (simp only: absolutely_integrable_restrict_UNIV [of S, symmetric] integrable_restrict_UNIV [of S, symmetric] abs_absolutely_integrableI)
+qed
+
+lemma absolutely_integrable_max:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+  assumes "f absolutely_integrable_on S" "g absolutely_integrable_on S"
+   shows "(\<lambda>x. \<Sum>i\<in>Basis. max (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i)
+            absolutely_integrable_on S"
+proof -
+  have "(\<lambda>x. \<Sum>i\<in>Basis. max (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i) =
+        (\<lambda>x. (1/2) *\<^sub>R (f x + g x + (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))"
+  proof (rule ext)
+    fix x
+    have "(\<Sum>i\<in>Basis. max (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i) = (\<Sum>i\<in>Basis. ((f x \<bullet> i + g x \<bullet> i + \<bar>f x \<bullet> i - g x \<bullet> i\<bar>) / 2) *\<^sub>R i)"
+      by (force intro: sum.cong)
+    also have "... = (1 / 2) *\<^sub>R (\<Sum>i\<in>Basis. (f x \<bullet> i + g x \<bullet> i + \<bar>f x \<bullet> i - g x \<bullet> i\<bar>) *\<^sub>R i)"
+    also have "... = (1 / 2) *\<^sub>R (f x + g x + (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i))"
+      by (simp add: sum.distrib algebra_simps euclidean_representation)
+    finally
+    show "(\<Sum>i\<in>Basis. max (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i) =
+         (1 / 2) *\<^sub>R (f x + g x + (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i))" .
+  qed
+  moreover have "(\<lambda>x. (1 / 2) *\<^sub>R (f x + g x + (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))
+                 absolutely_integrable_on S"
+    apply (intro absolutely_integrable_add absolutely_integrable_scaleR_left assms)
+    using absolutely_integrable_abs [OF absolutely_integrable_diff [OF assms]]
+    done
+  ultimately show ?thesis by metis
+qed
+
+corollary absolutely_integrable_max_1:
+  fixes f :: "'n::euclidean_space \<Rightarrow> real"
+  assumes "f absolutely_integrable_on S" "g absolutely_integrable_on S"
+   shows "(\<lambda>x. max (f x) (g x)) absolutely_integrable_on S"
+  using absolutely_integrable_max [OF assms] by simp
+
+lemma absolutely_integrable_min:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+  assumes "f absolutely_integrable_on S" "g absolutely_integrable_on S"
+   shows "(\<lambda>x. \<Sum>i\<in>Basis. min (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i)
+            absolutely_integrable_on S"
+proof -
+  have "(\<lambda>x. \<Sum>i\<in>Basis. min (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i) =
+        (\<lambda>x. (1/2) *\<^sub>R (f x + g x - (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))"
+  proof (rule ext)
+    fix x
+    have "(\<Sum>i\<in>Basis. min (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i) = (\<Sum>i\<in>Basis. ((f x \<bullet> i + g x \<bullet> i - \<bar>f x \<bullet> i - g x \<bullet> i\<bar>) / 2) *\<^sub>R i)"
+      by (force intro: sum.cong)
+    also have "... = (1 / 2) *\<^sub>R (\<Sum>i\<in>Basis. (f x \<bullet> i + g x \<bullet> i - \<bar>f x \<bullet> i - g x \<bullet> i\<bar>) *\<^sub>R i)"
+    also have "... = (1 / 2) *\<^sub>R (f x + g x - (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i))"
+      by (simp add: sum.distrib sum_subtractf algebra_simps euclidean_representation)
+    finally
+    show "(\<Sum>i\<in>Basis. min (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i) =
+         (1 / 2) *\<^sub>R (f x + g x - (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i))" .
+  qed
+  moreover have "(\<lambda>x. (1 / 2) *\<^sub>R (f x + g x - (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))
+                 absolutely_integrable_on S"
+    apply (intro absolutely_integrable_add absolutely_integrable_diff absolutely_integrable_scaleR_left assms)
+    using absolutely_integrable_abs [OF absolutely_integrable_diff [OF assms]]
+    done
+  ultimately show ?thesis by metis
+qed
+
+corollary absolutely_integrable_min_1:
+  fixes f :: "'n::euclidean_space \<Rightarrow> real"
+  assumes "f absolutely_integrable_on S" "g absolutely_integrable_on S"
+   shows "(\<lambda>x. min (f x) (g x)) absolutely_integrable_on S"
+  using absolutely_integrable_min [OF assms] by simp
+
+lemma nonnegative_absolutely_integrable:
+  fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
+  assumes "f integrable_on A" and comp: "\<And>x b. \<lbrakk>x \<in> A; b \<in> Basis\<rbrakk> \<Longrightarrow> 0 \<le> f x \<bullet> b"
+  shows "f absolutely_integrable_on A"
+proof -
+  have "(\<lambda>x. (f x \<bullet> i) *\<^sub>R i) absolutely_integrable_on A" if "i \<in> Basis" for i
+  proof -
+    have "(\<lambda>x. f x \<bullet> i) integrable_on A"
+      by (simp add: assms(1) integrable_component)
+    then have "(\<lambda>x. f x \<bullet> i) absolutely_integrable_on A"
+      by (metis that comp nonnegative_absolutely_integrable_1)
+    then show ?thesis
+      by (rule absolutely_integrable_scaleR_right)
+  qed
+  then have "(\<lambda>x. \<Sum>i\<in>Basis. (f x \<bullet> i) *\<^sub>R i) absolutely_integrable_on A"
+  then show ?thesis
+qed
+
+
+lemma absolutely_integrable_component_ubound:
+  fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
+  assumes f: "f integrable_on A" and g: "g absolutely_integrable_on A"
+      and comp: "\<And>x b. \<lbrakk>x \<in> A; b \<in> Basis\<rbrakk> \<Longrightarrow> f x \<bullet> b \<le> g x \<bullet> b"
+  shows "f absolutely_integrable_on A"
+proof -
+  have "(\<lambda>x. g x - (g x - f x)) absolutely_integrable_on A"
+    apply (rule absolutely_integrable_diff [OF g nonnegative_absolutely_integrable])
+    using Henstock_Kurzweil_Integration.integrable_diff absolutely_integrable_on_def f g apply blast
+    by (simp add: comp inner_diff_left)
+  then show ?thesis
+    by simp
+qed
+
+
+lemma absolutely_integrable_component_lbound:
+  fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
+  assumes f: "f absolutely_integrable_on A" and g: "g integrable_on A"
+      and comp: "\<And>x b. \<lbrakk>x \<in> A; b \<in> Basis\<rbrakk> \<Longrightarrow> f x \<bullet> b \<le> g x \<bullet> b"
+  shows "g absolutely_integrable_on A"
+proof -
+  have "(\<lambda>x. f x + (g x - f x)) absolutely_integrable_on A"
+    apply (rule absolutely_integrable_add [OF f nonnegative_absolutely_integrable])
+    using Henstock_Kurzweil_Integration.integrable_diff absolutely_integrable_on_def f g apply blast
+    by (simp add: comp inner_diff_left)
+  then show ?thesis
+    by simp
+qed
+
subsection \<open>Dominated convergence\<close>

lemma dominated_convergence:
@@ -2347,7 +2605,7 @@

\<close>

-lemma
+lemma
fixes f :: "real \<Rightarrow> real"
assumes [measurable]: "f \<in> borel_measurable borel"
assumes f: "\<And>x. x \<in> {a..b} \<Longrightarrow> DERIV F x :> f x" "\<And>x. x \<in> {a..b} \<Longrightarrow> 0 \<le> f x" and "a \<le> b"```
```--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Jun 24 21:23:48 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Jun 26 14:26:03 2017 +0100
@@ -890,103 +890,103 @@

subsection \<open>Cauchy-type criterion for integrability.\<close>

-(* XXXXXXX *)
-lemma integrable_cauchy:
+lemma integrable_Cauchy:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::{real_normed_vector,complete_space}"
shows "f integrable_on cbox a b \<longleftrightarrow>
-    (\<forall>e>0. \<exists>d. gauge d \<and>
-      (\<forall>p1 p2. p1 tagged_division_of (cbox a b) \<and> d fine p1 \<and>
-        p2 tagged_division_of (cbox a b) \<and> d fine p2 \<longrightarrow>
-        norm ((\<Sum>(x,k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x,k)\<in>p2. content k *\<^sub>R f x)) < e))"
-  (is "?l = (\<forall>e>0. \<exists>d. ?P e d)")
-proof
+        (\<forall>e>0. \<exists>\<gamma>. gauge \<gamma> \<and>
+          (\<forall>p1 p2. p1 tagged_division_of (cbox a b) \<and> \<gamma> fine p1 \<and>
+            p2 tagged_division_of (cbox a b) \<and> \<gamma> fine p2 \<longrightarrow>
+            norm ((\<Sum>(x,K)\<in>p1. content K *\<^sub>R f x) - (\<Sum>(x,K)\<in>p2. content K *\<^sub>R f x)) < e))"
+  (is "?l = (\<forall>e>0. \<exists>\<gamma>. ?P e \<gamma>)")
+proof (intro iffI allI impI)
assume ?l
-  then guess y unfolding integrable_on_def has_integral .. note y=this
-  show "\<forall>e>0. \<exists>d. ?P e d"
-  proof (clarify, goal_cases)
-    case (1 e)
-    then have "e/2 > 0" by auto
-    then guess d
-      apply -
-      apply (drule y[rule_format])
-      apply (elim exE conjE)
-      done
-    note d=this[rule_format]
-    show ?case
-    proof (rule_tac x=d in exI, clarsimp simp: d)
-      fix p1 p2
-      assume as: "p1 tagged_division_of (cbox a b)" "d fine p1"
-                 "p2 tagged_division_of (cbox a b)" "d fine p2"
-      show "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)) < e"
-        apply (rule dist_triangle_half_l[where y=y,unfolded dist_norm])
-        using d(2)[OF conjI[OF as(1-2)]] d(2)[OF conjI[OF as(3-4)]] .
+  then obtain y
+    where y: "\<And>e. e > 0 \<Longrightarrow>
+        \<exists>\<gamma>. gauge \<gamma> \<and>
+            (\<forall>p. p tagged_division_of cbox a b \<and> \<gamma> fine p \<longrightarrow>
+                 norm ((\<Sum>(x,K) \<in> p. content K *\<^sub>R f x) - y) < e)"
+    by (auto simp: integrable_on_def has_integral)
+  show "\<exists>\<gamma>. ?P e \<gamma>" if "e > 0" for e
+  proof -
+    have "e/2 > 0" using that by auto
+    with y obtain \<gamma> where "gauge \<gamma>"
+      and \<gamma>: "\<And>p. p tagged_division_of cbox a b \<and> \<gamma> fine p \<Longrightarrow>
+                  norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f x) - y) < e / 2"
+      by meson
+    show ?thesis
+    apply (rule_tac x=\<gamma> in exI, clarsimp simp: \<open>gauge \<gamma>\<close>)
+        by (blast intro!: \<gamma> dist_triangle_half_l[where y=y,unfolded dist_norm])
+    qed
+next
+  assume "\<forall>e>0. \<exists>\<gamma>. ?P e \<gamma>"
+  then have "\<forall>n::nat. \<exists>\<gamma>. ?P (1 / (n + 1)) \<gamma>"
+    by auto
+  then obtain \<gamma> :: "nat \<Rightarrow> 'n \<Rightarrow> 'n set" where \<gamma>:
+    "\<And>m. gauge (\<gamma> m)"
+    "\<And>m p1 p2. \<lbrakk>p1 tagged_division_of cbox a b;
+              \<gamma> m fine p1; p2 tagged_division_of cbox a b; \<gamma> m fine p2\<rbrakk>
+              \<Longrightarrow> norm ((\<Sum>(x,K) \<in> p1. content K *\<^sub>R f x) - (\<Sum>(x,K) \<in> p2. content K *\<^sub>R f x))
+                  < 1 / (m + 1)"
+    by metis
+  have "\<And>n. gauge (\<lambda>x. \<Inter>{\<gamma> i x |i. i \<in> {0..n}})"
+    apply (rule gauge_Inter)
+    using \<gamma> by auto
+  then have "\<forall>n. \<exists>p. p tagged_division_of (cbox a b) \<and> (\<lambda>x. \<Inter>{\<gamma> i x |i. i \<in> {0..n}}) fine p"
+    by (meson fine_division_exists)
+  then obtain p where p: "\<And>z. p z tagged_division_of cbox a b"
+                         "\<And>z. (\<lambda>x. \<Inter>{\<gamma> i x |i. i \<in> {0..z}}) fine p z"
+    by meson
+  have dp: "\<And>i n. i\<le>n \<Longrightarrow> \<gamma> i fine p n"
+    using p unfolding fine_Inter
+    using atLeastAtMost_iff by blast
+  have "Cauchy (\<lambda>n. sum (\<lambda>(x,K). content K *\<^sub>R (f x)) (p n))"
+  proof (rule CauchyI)
+    fix e::real
+    assume "0 < e"
+    then obtain N where "N \<noteq> 0" and N: "inverse (real N) < e"
+      using real_arch_inverse[of e] by blast
+    show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm ((\<Sum>(x,K) \<in> p m. content K *\<^sub>R f x) - (\<Sum>(x,K) \<in> p n. content K *\<^sub>R f x)) < e"
+    proof (intro exI allI impI)
+      fix m n
+      assume mn: "N \<le> m" "N \<le> n"
+      have "norm ((\<Sum>(x,K) \<in> p m. content K *\<^sub>R f x) - (\<Sum>(x,K) \<in> p n. content K *\<^sub>R f x)) < 1 / (real N + 1)"
+        by (simp add: p(1) dp mn \<gamma>)
+      also have "... < e"
+        using  N \<open>N \<noteq> 0\<close> \<open>0 < e\<close> by (auto simp: field_simps)
+      finally show "norm ((\<Sum>(x,K) \<in> p m. content K *\<^sub>R f x) - (\<Sum>(x,K) \<in> p n. content K *\<^sub>R f x)) < e" .
qed
qed
-next
-  assume "\<forall>e>0. \<exists>d. ?P e d"
-  then have "\<forall>n::nat. \<exists>d. ?P (inverse(of_nat (n + 1))) d"
-    by auto
-  from choice[OF this] guess d .. note d=conjunctD2[OF this[rule_format],rule_format]
-  have "\<And>n. gauge (\<lambda>x. \<Inter>{d i x |i. i \<in> {0..n}})"
-    apply (rule gauge_Inter)
-    using d(1)
-    apply auto
-    done
-  then have "\<forall>n. \<exists>p. p tagged_division_of (cbox a b) \<and> (\<lambda>x. \<Inter>{d i x |i. i \<in> {0..n}}) fine p"
-    by (meson fine_division_exists)
-  from choice[OF this] guess p .. note p = conjunctD2[OF this[rule_format]]
-  have dp: "\<And>i n. i\<le>n \<Longrightarrow> d i fine p n"
-    using p(2) unfolding fine_inters by auto
-  have "Cauchy (\<lambda>n. sum (\<lambda>(x,k). content k *\<^sub>R (f x)) (p n))"
-  proof (rule CauchyI, goal_cases)
-    case (1 e)
-    then guess N unfolding real_arch_inverse[of e] .. note N=this
-    show ?case
-      apply (rule_tac x=N in exI)
-    proof clarify
-      fix m n
-      assume mn: "N \<le> m" "N \<le> n"
-      have *: "N = (N - 1) + 1" using N by auto
-      show "norm ((\<Sum>(x, k)\<in>p m. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p n. content k *\<^sub>R f x)) < e"
-        apply (rule less_trans[OF _ N[THEN conjunct2,THEN conjunct2]])
-        apply(subst *)
-        using dp p(1) mn d(2) by auto
-    qed
-  qed
-  then guess y unfolding convergent_eq_Cauchy[symmetric] .. note y=this[THEN LIMSEQ_D]
+  then obtain y where y: "\<exists>no. \<forall>n\<ge>no. norm ((\<Sum>(x,K) \<in> p n. content K *\<^sub>R f x) - y) < r" if "r > 0" for r
+    by (auto simp: convergent_eq_Cauchy[symmetric] dest: LIMSEQ_D)
show ?l
unfolding integrable_on_def has_integral
proof (rule_tac x=y in exI, clarify)
fix e :: real
assume "e>0"
-    then have *:"e/2 > 0" by auto
-    then guess N1 unfolding real_arch_inverse[of "e/2"] .. note N1=this
-    then have N1': "N1 = N1 - 1 + 1"
-      by auto
-    guess N2 using y[OF *] .. note N2=this
-    have "gauge (d (N1 + N2))"
-      using d by auto
-    moreover
-    {
-      fix q
-      assume as: "q tagged_division_of (cbox a b)" "d (N1 + N2) fine q"
-      have *: "inverse (of_nat (N1 + N2 + 1)) < e / 2"
-        apply (rule less_trans)
-        using N1
-        apply auto
-        done
-      have "norm ((\<Sum>(x, k)\<in>q. content k *\<^sub>R f x) - y) < e"
-        apply (rule norm_triangle_half_r)
-        apply (rule less_trans[OF _ *])
-        apply (subst N1', rule d(2)[of "p (N1+N2)"])
-        using N1' as(1) as(2) dp
-        apply (simp add: \<open>\<forall>x. p x tagged_division_of cbox a b \<and> (\<lambda>xa. \<Inter>{d i xa |i. i \<in> {0..x}}) fine p x\<close>)
-        using N2 le_add2 by blast
-    }
-    ultimately show "\<exists>d. gauge d \<and>
-      (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
-        norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - y) < e)"
-      by (rule_tac x="d (N1 + N2)" in exI) auto
+    then have e2: "e/2 > 0" by auto
+    then obtain N1::nat where N1: "N1 \<noteq> 0" "inverse (real N1) < e / 2"
+      using real_arch_inverse by blast
+    obtain N2::nat where N2: "\<And>n. n \<ge> N2 \<Longrightarrow> norm ((\<Sum>(x,K) \<in> p n. content K *\<^sub>R f x) - y) < e / 2"
+      using y[OF e2] by metis
+    show "\<exists>\<gamma>. gauge \<gamma> \<and>
+              (\<forall>p. p tagged_division_of (cbox a b) \<and> \<gamma> fine p \<longrightarrow>
+                norm ((\<Sum>(x,K) \<in> p. content K *\<^sub>R f x) - y) < e)"
+    proof (intro exI conjI allI impI)
+      show "gauge (\<gamma> (N1+N2))"
+        using \<gamma> by auto
+      show "norm ((\<Sum>(x,K) \<in> q. content K *\<^sub>R f x) - y) < e"
+           if "q tagged_division_of cbox a b \<and> \<gamma> (N1+N2) fine q" for q
+      proof (rule norm_triangle_half_r)
+        have "norm ((\<Sum>(x,K) \<in> p (N1+N2). content K *\<^sub>R f x) - (\<Sum>(x,K) \<in> q. content K *\<^sub>R f x))
+               < 1 / (real (N1+N2) + 1)"
+          by (rule \<gamma>; simp add: dp p that)
+        also have "... < e/2"
+          using N1 \<open>0 < e\<close> by (auto simp: field_simps intro: less_le_trans)
+        finally show "norm ((\<Sum>(x,K) \<in> p (N1+N2). content K *\<^sub>R f x) - (\<Sum>(x,K) \<in> q. content K *\<^sub>R f x)) < e / 2" .
+        show "norm ((\<Sum>(x,K) \<in> p (N1+N2). content K *\<^sub>R f x) - y) < e/2"
+          using N2 le_add_same_cancel2 by blast
+      qed
+    qed
qed
qed

@@ -1021,221 +1021,220 @@
qed

-lemma has_integral_split:
+proposition has_integral_split:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes fi: "(f has_integral i) (cbox a b \<inter> {x. x\<bullet>k \<le> c})"
and fj: "(f has_integral j) (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
and k: "k \<in> Basis"
-  shows "(f has_integral (i + j)) (cbox a b)"
-proof (unfold has_integral, rule, rule, goal_cases)
-  case (1 e)
+shows "(f has_integral (i + j)) (cbox a b)"
+  unfolding has_integral
+proof clarify
+  fix e::real
+  assume "0 < e"
then have e: "e/2 > 0"
by auto
-    obtain d1
-    where d1: "gauge d1"
-      and d1norm:
-        "\<And>p. \<lbrakk>p tagged_division_of cbox a b \<inter> {x. x \<bullet> k \<le> c};
-               d1 fine p\<rbrakk> \<Longrightarrow> norm ((\<Sum>(x, k) \<in> p. content k *\<^sub>R f x) - i) < e / 2"
+    obtain \<gamma>1 where \<gamma>1: "gauge \<gamma>1"
+      and \<gamma>1norm:
+        "\<And>p. \<lbrakk>p tagged_division_of cbox a b \<inter> {x. x \<bullet> k \<le> c}; \<gamma>1 fine p\<rbrakk>
+             \<Longrightarrow> norm ((\<Sum>(x,K) \<in> p. content K *\<^sub>R f x) - i) < e / 2"
apply (rule has_integralD[OF fi[unfolded interval_split[OF k]] e])
-       done
-    obtain d2
-    where d2: "gauge d2"
-      and d2norm:
-        "\<And>p. \<lbrakk>p tagged_division_of cbox a b \<inter> {x. c \<le> x \<bullet> k};
-               d2 fine p\<rbrakk> \<Longrightarrow> norm ((\<Sum>(x, k) \<in> p. content k *\<^sub>R f x) - j) < e / 2"
+      done
+    obtain \<gamma>2 where \<gamma>2: "gauge \<gamma>2"
+      and \<gamma>2norm:
+        "\<And>p. \<lbrakk>p tagged_division_of cbox a b \<inter> {x. c \<le> x \<bullet> k}; \<gamma>2 fine p\<rbrakk>
+             \<Longrightarrow> norm ((\<Sum>(x, k) \<in> p. content k *\<^sub>R f x) - j) < e / 2"
apply (rule has_integralD[OF fj[unfolded interval_split[OF k]] e])
done
-  let ?d = "\<lambda>x. if x\<bullet>k = c then (d1 x \<inter> d2 x) else ball x \<bar>x\<bullet>k - c\<bar> \<inter> d1 x \<inter> d2 x"
-  have "gauge ?d"
-    using d1 d2 unfolding gauge_def by auto
-  then show ?case
-  proof (rule_tac x="?d" in exI, safe)
+  let ?\<gamma> = "\<lambda>x. if x\<bullet>k = c then (\<gamma>1 x \<inter> \<gamma>2 x) else ball x \<bar>x\<bullet>k - c\<bar> \<inter> \<gamma>1 x \<inter> \<gamma>2 x"
+  have "gauge ?\<gamma>"
+    using \<gamma>1 \<gamma>2 unfolding gauge_def by auto
+  then show "\<exists>\<gamma>. gauge \<gamma> \<and>
+                 (\<forall>p. p tagged_division_of cbox a b \<and> \<gamma> fine p \<longrightarrow>
+                      norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - (i + j)) < e)"
+  proof (rule_tac x="?\<gamma>" in exI, safe)
fix p
-    assume "p tagged_division_of (cbox a b)" "?d fine p"
-    note p = this tagged_division_ofD[OF this(1)]
-    have xk_le_c: "\<And>x kk. (x, kk) \<in> p \<Longrightarrow> kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {} \<Longrightarrow> x\<bullet>k \<le> c"
-    proof -
-      fix x kk
-      assume as: "(x, kk) \<in> p" and kk: "kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}"
-      show "x\<bullet>k \<le> c"
-      proof (rule ccontr)
-        assume **: "\<not> ?thesis"
-        from this[unfolded not_le]
-        have "kk \<subseteq> ball x \<bar>x \<bullet> k - c\<bar>"
-          using p(2)[unfolded fine_def, rule_format,OF as] by auto
-        with kk obtain y where y: "y \<in> ball x \<bar>x \<bullet> k - c\<bar>" "y\<bullet>k \<le> c"
-          by blast
-        then have "\<bar>x \<bullet> k - y \<bullet> k\<bar> < \<bar>x \<bullet> k - c\<bar>"
-          using Basis_le_norm[OF k, of "x - y"]
-          by (auto simp add: dist_norm inner_diff_left intro: le_less_trans)
-        with y show False
-          using ** by (auto simp add: field_simps)
-      qed
+    assume p: "p tagged_division_of (cbox a b)" and "?\<gamma> fine p"
+    have ab_eqp: "cbox a b = \<Union>{K. \<exists>x. (x, K) \<in> p}"
+      using p by blast
+    have xk_le_c: "x\<bullet>k \<le> c" if as: "(x,K) \<in> p" and K: "K \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}" for x K
+    proof (rule ccontr)
+      assume **: "\<not> x \<bullet> k \<le> c"
+      then have "K \<subseteq> ball x \<bar>x \<bullet> k - c\<bar>"
+        using \<open>?\<gamma> fine p\<close> as by (fastforce simp: not_le algebra_simps)
+      with K obtain y where y: "y \<in> ball x \<bar>x \<bullet> k - c\<bar>" "y\<bullet>k \<le> c"
+        by blast
+      then have "\<bar>x \<bullet> k - y \<bullet> k\<bar> < \<bar>x \<bullet> k - c\<bar>"
+        using Basis_le_norm[OF k, of "x - y"]
+        by (auto simp add: dist_norm inner_diff_left intro: le_less_trans)
+      with y show False
+        using ** by (auto simp add: field_simps)
qed
-    have xk_ge_c: "\<And>x kk. (x, kk) \<in> p \<Longrightarrow> kk \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {} \<Longrightarrow> x\<bullet>k \<ge> c"
-    proof -
-      fix x kk
-      assume as: "(x, kk) \<in> p" and kk: "kk \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}"
-      show "x\<bullet>k \<ge> c"
-      proof (rule ccontr)
-        assume **: "\<not> ?thesis"
-        from this[unfolded not_le] have "kk \<subseteq> ball x \<bar>x \<bullet> k - c\<bar>"
-          using p(2)[unfolded fine_def,rule_format,OF as,unfolded split_conv] by auto
-        with kk obtain y where y: "y \<in> ball x \<bar>x \<bullet> k - c\<bar>" "y\<bullet>k \<ge> c"
-          by blast
-        then have "\<bar>x \<bullet> k - y \<bullet> k\<bar> < \<bar>x \<bullet> k - c\<bar>"
-          using Basis_le_norm[OF k, of "x - y"]
-          by (auto simp add: dist_norm inner_diff_left intro: le_less_trans)
-        with y show False
-          using ** by (auto simp add: field_simps)
-      qed
+    have xk_ge_c: "x\<bullet>k \<ge> c" if as: "(x,K) \<in> p" and K: "K \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}" for x K
+    proof (rule ccontr)
+      assume **: "\<not> x \<bullet> k \<ge> c"
+      then have "K \<subseteq> ball x \<bar>x \<bullet> k - c\<bar>"
+        using \<open>?\<gamma> fine p\<close> as by (fastforce simp: not_le algebra_simps)
+      with K obtain y where y: "y \<in> ball x \<bar>x \<bullet> k - c\<bar>" "y\<bullet>k \<ge> c"
+        by blast
+      then have "\<bar>x \<bullet> k - y \<bullet> k\<bar> < \<bar>x \<bullet> k - c\<bar>"
+        using Basis_le_norm[OF k, of "x - y"]
+        by (auto simp add: dist_norm inner_diff_left intro: le_less_trans)
+      with y show False
+        using ** by (auto simp add: field_simps)
qed
-
-    have lem1: "\<And>f P Q. (\<forall>x k. (x, k) \<in> {(x, f k) | x k. P x k} \<longrightarrow> Q x k) \<longleftrightarrow>
-                         (\<forall>x k. P x k \<longrightarrow> Q x (f k))"
-      by auto
-    have fin_finite: "finite {(x,f k) | x k. (x,k) \<in> s \<and> P x k}"
+    have fin_finite: "finite {(x,f K) | x K. (x,K) \<in> s \<and> P x K}"
if "finite s" for s and f :: "'a set \<Rightarrow> 'a set" and P :: "'a \<Rightarrow> 'a set \<Rightarrow> bool"
proof -
-      from that have "finite ((\<lambda>(x, k). (x, f k)) ` s)"
+      from that have "finite ((\<lambda>(x,K). (x, f K)) ` s)"
by auto
then show ?thesis
by (rule rev_finite_subset) auto
qed
-    { fix g :: "'a set \<Rightarrow> 'a set"
+    { fix \<G> :: "'a set \<Rightarrow> 'a set"
fix i :: "'a \<times> 'a set"
-      assume "i \<in> (\<lambda>(x, k). (x, g k)) ` p - {(x, g k) |x k. (x, k) \<in> p \<and> g k \<noteq> {}}"
-      then obtain x k where xk:
-              "i = (x, g k)"  "(x, k) \<in> p"
-              "(x, g k) \<notin> {(x, g k) |x k. (x, k) \<in> p \<and> g k \<noteq> {}}"
-          by auto
-      have "content (g k) = 0"
+      assume "i \<in> (\<lambda>(x, k). (x, \<G> k)) ` p - {(x, \<G> k) |x k. (x, k) \<in> p \<and> \<G> k \<noteq> {}}"
+      then obtain x K where xk: "i = (x, \<G> K)"  "(x,K) \<in> p"
+                                 "(x, \<G> K) \<notin> {(x, \<G> K) |x K. (x,K) \<in> p \<and> \<G> K \<noteq> {}}"
+        by auto
+      have "content (\<G> K) = 0"
using xk using content_empty by auto
-      then have "(\<lambda>(x, k). content k *\<^sub>R f x) i = 0"
+      then have "(\<lambda>(x,K). content K *\<^sub>R f x) i = 0"
unfolding xk split_conv by auto
} note [simp] = this
-    have lem3: "\<And>g :: 'a set \<Rightarrow> 'a set. finite p \<Longrightarrow>
-                  sum (\<lambda>(x, k). content k *\<^sub>R f x) {(x,g k) |x k. (x,k) \<in> p \<and> g k \<noteq> {}} =
-                  sum (\<lambda>(x, k). content k *\<^sub>R f x) ((\<lambda>(x, k). (x, g k)) ` p)"
-      by (rule sum.mono_neutral_left) auto
-    let ?M1 = "{(x, kk \<inter> {x. x\<bullet>k \<le> c}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}}"
-    have d1_fine: "d1 fine ?M1"
-      by (force intro: fineI dest: fineD[OF p(2)] simp add: split: if_split_asm)
+    have "finite p"
+      using p by blast
+    let ?M1 = "{(x, K \<inter> {x. x\<bullet>k \<le> c}) |x K. (x,K) \<in> p \<and> K \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}}"
+    have \<gamma>1_fine: "\<gamma>1 fine ?M1"
+      using \<open>?\<gamma> fine p\<close> by (fastforce simp: fine_def split: if_split_asm)
have "norm ((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) < e/2"
-    proof (rule d1norm [OF tagged_division_ofI d1_fine])
+    proof (rule \<gamma>1norm [OF tagged_division_ofI \<gamma>1_fine])
show "finite ?M1"
-        by (rule fin_finite p(3))+
+        by (rule fin_finite) (use p in blast)
show "\<Union>{k. \<exists>x. (x, k) \<in> ?M1} = cbox a b \<inter> {x. x\<bullet>k \<le> c}"
-        unfolding p(8)[symmetric] by auto
-      fix x l
-      assume xl: "(x, l) \<in> ?M1"
-      then guess x' l' unfolding mem_Collect_eq unfolding prod.inject by (elim exE conjE) note xl'=this
-      show "x \<in> l" "l \<subseteq> cbox a b \<inter> {x. x \<bullet> k \<le> c}"
-        unfolding xl'
-        using p(4-6)[OF xl'(3)] using xl'(4)
-        using xk_le_c[OF xl'(3-4)] by auto
-      show "\<exists>a b. l = cbox a b"
-        unfolding xl'
-        using p(6)[OF xl'(3)]
-        by (fastforce simp add: interval_split[OF k,where c=c])
-      fix y r
-      let ?goal = "interior l \<inter> interior r = {}"
-      assume yr: "(y, r) \<in> ?M1"
-      then guess y' r' unfolding mem_Collect_eq unfolding prod.inject by (elim exE conjE) note yr'=this
-      assume as: "(x, l) \<noteq> (y, r)"
-      show "interior l \<inter> interior r = {}"
-      proof (cases "l' = r' \<longrightarrow> x' = y'")
+        by (auto simp: ab_eqp)
+
+      fix x L
+      assume xL: "(x, L) \<in> ?M1"
+      then obtain x' L' where xL': "x = x'" "L = L' \<inter> {x. x \<bullet> k \<le> c}"
+                                   "(x', L') \<in> p" "L' \<inter> {x. x \<bullet> k \<le> c} \<noteq> {}"
+        by blast
+      then obtain a' b' where ab': "L' = cbox a' b'"
+        using p by blast
+      show "x \<in> L" "L \<subseteq> cbox a b \<inter> {x. x \<bullet> k \<le> c}"
+        using p xk_le_c xL' by auto
+      show "\<exists>a b. L = cbox a b"
+        using p xL' ab' by (auto simp add: interval_split[OF k,where c=c])
+
+      fix y R
+      assume yR: "(y, R) \<in> ?M1"
+      then obtain y' R' where yR': "y = y'" "R = R' \<inter> {x. x \<bullet> k \<le> c}"
+                                   "(y', R') \<in> p" "R' \<inter> {x. x \<bullet> k \<le> c} \<noteq> {}"
+        by blast
+      assume as: "(x, L) \<noteq> (y, R)"
+      show "interior L \<inter> interior R = {}"
+      proof (cases "L' = R' \<longrightarrow> x' = y'")
case False
+        have "interior R' = {}"
+          by (metis (no_types) False Pair_inject inf.idem tagged_division_ofD(5) [OF p] xL'(3) yR'(3))
then show ?thesis
-          using p(7)[OF xl'(3) yr'(3)] using as unfolding xl' yr' by auto
+          using yR' by simp
next
case True
-        then have "l' \<noteq> r'"
-          using as unfolding xl' yr' by auto
+        then have "L' \<noteq> R'"
+          using as unfolding xL' yR' by auto
+        have "interior L' \<inter> interior R' = {}"
+          by (metis (no_types) Pair_inject \<open>L' \<noteq> R'\<close> p tagged_division_ofD(5) xL'(3) yR'(3))
then show ?thesis
-          using p(7)[OF xl'(3) yr'(3)] using as unfolding xl' yr' by auto
+          using xL'(2) yR'(2) by auto
qed
qed
moreover
-    let ?M2 = "{(x,kk \<inter> {x. x\<bullet>k \<ge> c}) |x kk. (x,kk) \<in> p \<and> kk \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}}"
-    have d2_fine: "d2 fine ?M2"
-      by (force intro: fineI dest: fineD[OF p(2)] simp add: split: if_split_asm)
+    let ?M2 = "{(x,K \<inter> {x. x\<bullet>k \<ge> c}) |x K. (x,K) \<in> p \<and> K \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}}"
+    have \<gamma>2_fine: "\<gamma>2 fine ?M2"
+      using \<open>?\<gamma> fine p\<close> by (fastforce simp: fine_def split: if_split_asm)
have "norm ((\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - j) < e/2"
-    proof (rule d2norm [OF tagged_division_ofI d2_fine])
+    proof (rule \<gamma>2norm [OF tagged_division_ofI \<gamma>2_fine])
show "finite ?M2"
-        by (rule fin_finite p(3))+
+        by (rule fin_finite) (use p in blast)
show "\<Union>{k. \<exists>x. (x, k) \<in> ?M2} = cbox a b \<inter> {x. x\<bullet>k \<ge> c}"
-        unfolding p(8)[symmetric] by auto
-      fix x l
-      assume xl: "(x, l) \<in> ?M2"
-      then guess x' l' unfolding mem_Collect_eq unfolding prod.inject by (elim exE conjE) note xl'=this
-      show "x \<in> l" "l \<subseteq> cbox a b \<inter> {x. x \<bullet> k \<ge> c}"
-        unfolding xl'
-        using p(4-6)[OF xl'(3)] xl'(4) xk_ge_c[OF xl'(3-4)]
-        by auto
-      show "\<exists>a b. l = cbox a b"
-        unfolding xl'
-        using p(6)[OF xl'(3)]
-        by (fastforce simp add: interval_split[OF k, where c=c])
-      fix y r
-      let ?goal = "interior l \<inter> interior r = {}"
-      assume yr: "(y, r) \<in> ?M2"
-      then guess y' r' unfolding mem_Collect_eq unfolding prod.inject by (elim exE conjE) note yr'=this
-      assume as: "(x, l) \<noteq> (y, r)"
-      show "interior l \<inter> interior r = {}"
-      proof (cases "l' = r' \<longrightarrow> x' = y'")
+        by (auto simp: ab_eqp)
+
+      fix x L
+      assume xL: "(x, L) \<in> ?M2"
+      then obtain x' L' where xL': "x = x'" "L = L' \<inter> {x. x \<bullet> k \<ge> c}"
+                                   "(x', L') \<in> p" "L' \<inter> {x. x \<bullet> k \<ge> c} \<noteq> {}"
+        by blast
+      then obtain a' b' where ab': "L' = cbox a' b'"
+        using p by blast
+      show "x \<in> L" "L \<subseteq> cbox a b \<inter> {x. x \<bullet> k \<ge> c}"
+        using p xk_ge_c xL' by auto
+      show "\<exists>a b. L = cbox a b"
+        using p xL' ab' by (auto simp add: interval_split[OF k,where c=c])
+
+      fix y R
+      assume yR: "(y, R) \<in> ?M2"
+      then obtain y' R' where yR': "y = y'" "R = R' \<inter> {x. x \<bullet> k \<ge> c}"
+                                   "(y', R') \<in> p" "R' \<inter> {x. x \<bullet> k \<ge> c} \<noteq> {}"
+        by blast
+      assume as: "(x, L) \<noteq> (y, R)"
+      show "interior L \<inter> interior R = {}"
+      proof (cases "L' = R' \<longrightarrow> x' = y'")
case False
+        have "interior R' = {}"
+          by (metis (no_types) False Pair_inject inf.idem tagged_division_ofD(5) [OF p] xL'(3) yR'(3))
then show ?thesis
-          using p(7)[OF xl'(3) yr'(3)] using as unfolding xl' yr' by auto
+          using yR' by simp
next
case True
-        then have "l' \<noteq> r'"
-          using as unfolding xl' yr' by auto
+        then have "L' \<noteq> R'"
+          using as unfolding xL' yR' by auto
+        have "interior L' \<inter> interior R' = {}"
+          by (metis (no_types) Pair_inject \<open>L' \<noteq> R'\<close> p tagged_division_ofD(5) xL'(3) yR'(3))
then show ?thesis
-          using p(7)[OF xl'(3) yr'(3)] using as unfolding xl' yr' by auto
+          using xL'(2) yR'(2) by auto
qed
qed
ultimately
-    have "norm (((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) + ((\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - j)) < e/2 + e/2"
+    have "norm (((\<Sum>(x,K) \<in> ?M1. content K *\<^sub>R f x) - i) + ((\<Sum>(x,K) \<in> ?M2. content K *\<^sub>R f x) - j)) < e/2 + e/2"
-    also {
+    moreover have "((\<Sum>(x,K) \<in> ?M1. content K *\<^sub>R f x) - i) +
+                   ((\<Sum>(x,K) \<in> ?M2. content K *\<^sub>R f x) - j) =
+                   (\<Sum>(x, ka)\<in>p. content ka *\<^sub>R f x) - (i + j)"
+    proof -
have eq0: "\<And>x y. x = (0::real) \<Longrightarrow> x *\<^sub>R (y::'b) = 0"
-        using scaleR_zero_left by auto
+         by auto
have cont_eq: "\<And>g. (\<lambda>(x,l). content l *\<^sub>R f x) \<circ> (\<lambda>(x,l). (x,g l)) = (\<lambda>(x,l). content (g l) *\<^sub>R f x)"
by auto
+      have *: "\<And>\<G> :: 'a set \<Rightarrow> 'a set.
+                  (\<Sum>(x,K)\<in>{(x, \<G> K) |x K. (x,K) \<in> p \<and> \<G> K \<noteq> {}}. content K *\<^sub>R f x) =
+                  (\<Sum>(x,K)\<in>(\<lambda>(x,K). (x, \<G> K)) ` p. content K *\<^sub>R f x)"
+        by (rule sum.mono_neutral_left) (auto simp: \<open>finite p\<close>)
have "((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) + ((\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - j) =
(\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - (i + j)"
by auto
-      also have "\<dots> = (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f x) +
-        (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f x) - (i + j)"
-        unfolding lem3[OF p(3)]
-        by (subst (1 2) sum.reindex_nontrivial[OF p(3)])
-           (auto intro!: k eq0 tagged_division_split_left_inj_content[OF p(1)] tagged_division_split_right_inj_content[OF p(1)]
-                 simp: cont_eq)+
-      also note sum.distrib[symmetric]
-      also have "\<And>x. x \<in> p \<Longrightarrow>
-                    (\<lambda>(x,ka). content (ka \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f x) x +
-                    (\<lambda>(x,ka). content (ka \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f x) x =
-                    (\<lambda>(x,ka). content ka *\<^sub>R f x) x"
+      moreover have "\<dots> = (\<Sum>(x,K) \<in> p. content (K \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f x) +
+        (\<Sum>(x,K) \<in> p. content (K \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f x) - (i + j)"
+        unfolding *
+        apply (subst (1 2) sum.reindex_nontrivial)
+           apply (auto intro!: k p eq0 tagged_division_split_left_inj_content tagged_division_split_right_inj_content
+                       simp: cont_eq \<open>finite p\<close>)
+        done
+      moreover have "\<And>x. x \<in> p \<Longrightarrow> (\<lambda>(a,B). content (B \<inter> {a. a \<bullet> k \<le> c}) *\<^sub>R f a) x +
+                                (\<lambda>(a,B). content (B \<inter> {a. c \<le> a \<bullet> k}) *\<^sub>R f a) x =
+                                (\<lambda>(a,B). content B *\<^sub>R f a) x"
proof clarify
-        fix a b
-        assume "(a, b) \<in> p"
-        from p(6)[OF this] guess u v by (elim exE) note uv=this
-        then show "content (b \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f a + content (b \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f a =
-          content b *\<^sub>R f a"
-          unfolding scaleR_left_distrib[symmetric]
-          unfolding uv content_split[OF k,of u v c]
-          by auto
+        fix a B
+        assume "(a, B) \<in> p"
+        with p obtain u v where uv: "B = cbox u v" by blast
+        then show "content (B \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f a + content (B \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f a = content B *\<^sub>R f a"
+          by (auto simp: scaleR_left_distrib uv content_split[OF k,of u v c])
qed
-      note sum.cong [OF _ this]
-      finally have "(\<Sum>(x, k)\<in>{(x, kk \<inter> {x. x \<bullet> k \<le> c}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. x \<bullet> k \<le> c} \<noteq> {}}. content k *\<^sub>R f x) - i +
-        ((\<Sum>(x, k)\<in>{(x, kk \<inter> {x. c \<le> x \<bullet> k}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. c \<le> x \<bullet> k} \<noteq> {}}. content k *\<^sub>R f x) - j) =
-        (\<Sum>(x, ka)\<in>p. content ka *\<^sub>R f x) - (i + j)"
-        by auto
-    }
-    finally show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - (i + j)) < e"
+      ultimately show ?thesis
+        by (auto simp: sum.distrib[symmetric])
+      qed
+    ultimately show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - (i + j)) < e"
by auto
qed
qed
@@ -1303,7 +1302,7 @@
norm ((\<Sum>(x, k)\<in>p1 \<union> p2. content k *\<^sub>R f x) - i)"
by (subst sum.union_inter_neutral) (auto simp: p1 p2)
also have "\<dots> < e"
-      by (rule k d(2) p12 fine_union p1 p2)+
+      by (rule k d(2) p12 fine_Un p1 p2)+
finally have "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - i) < e" .
}
then show ?thesis
@@ -1352,7 +1351,7 @@
qed
qed
with f show ?thesis1
-    by (simp add: interval_split[OF k] integrable_cauchy)
+    by (simp add: interval_split[OF k] integrable_Cauchy)
have "\<exists>d. gauge d \<and>
(\<forall>p1 p2. p1 tagged_division_of cbox a b \<inter> {x. x \<bullet> k \<ge> c} \<and> d fine p1 \<and>
p2 tagged_division_of cbox a b \<inter> {x. x \<bullet> k \<ge> c} \<and> d fine p2 \<longrightarrow>
@@ -1384,7 +1383,7 @@
qed
qed
with f show ?thesis2
-    by (simp add: interval_split[OF k] integrable_cauchy)
+    by (simp add: interval_split[OF k] integrable_Cauchy)
qed

lemma operative_integral:
@@ -1509,21 +1508,25 @@
lemma has_integral_bound:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes "0 \<le> B"
-      and *: "(f has_integral i) (cbox a b)"
-      and "\<forall>x\<in>cbox a b. norm (f x) \<le> B"
+      and f: "(f has_integral i) (cbox a b)"
+      and "\<And>x. x\<in>cbox a b \<Longrightarrow> norm (f x) \<le> B"
shows "norm i \<le> B * content (cbox a b)"
proof (rule ccontr)
assume "\<not> ?thesis"
-  then have *: "norm i - B * content (cbox a b) > 0"
+  then have "norm i - B * content (cbox a b) > 0"
by auto
-  from assms(2)[unfolded has_integral,rule_format,OF *]
-  guess d by (elim exE conjE) note d=this[rule_format]
-  from fine_division_exists[OF this(1), of a b] guess p . note p=this
-  have *: "\<And>s B. norm s \<le> B \<Longrightarrow> \<not> norm (s - i) < norm i - B"
+  with f[unfolded has_integral]
+  obtain \<gamma> where "gauge \<gamma>" and \<gamma>:
+    "\<And>p. \<lbrakk>p tagged_division_of cbox a b; \<gamma> fine p\<rbrakk>
+          \<Longrightarrow> norm ((\<Sum>(x, K)\<in>p. content K *\<^sub>R f x) - i) < norm i - B * content (cbox a b)"
+    by metis
+  then obtain p where p: "p tagged_division_of cbox a b" and "\<gamma> fine p"
+    using fine_division_exists by blast
+  have "\<And>s B. norm s \<le> B \<Longrightarrow> \<not> norm (s - i) < norm i - B"
unfolding not_less
-    by (metis norm_triangle_sub[of i] add.commute le_less_trans less_diff_eq linorder_not_le norm_minus_commute)
-  show False
-    using d(2)[OF conjI[OF p]] *[OF rsum_bound[OF p(1) assms(3)]] by auto
+    by (metis diff_left_mono dist_commute dist_norm norm_triangle_ineq2 order_trans)
+  then show False
+    using \<gamma> [OF p \<open>\<gamma> fine p\<close>] rsum_bound[OF p] assms by metis
qed

corollary has_integral_bound_real:
@@ -1547,20 +1550,17 @@

lemma rsum_component_le:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes "p tagged_division_of (cbox a b)"
-      and "\<forall>x\<in>cbox a b. (f x)\<bullet>i \<le> (g x)\<bullet>i"
-    shows "(sum (\<lambda>(x,k). content k *\<^sub>R f x) p)\<bullet>i \<le> (sum (\<lambda>(x,k). content k *\<^sub>R g x) p)\<bullet>i"
+  assumes p: "p tagged_division_of (cbox a b)"
+      and "\<And>x. x \<in> cbox a b \<Longrightarrow> (f x)\<bullet>i \<le> (g x)\<bullet>i"
+    shows "(\<Sum>(x, K)\<in>p. content K *\<^sub>R f x) \<bullet> i \<le> (\<Sum>(x, K)\<in>p. content K *\<^sub>R g x) \<bullet> i"
unfolding inner_sum_left
proof (rule sum_mono, clarify)
-  fix a b
-  assume ab: "(a, b) \<in> p"
-  note tagged = tagged_division_ofD(2-4)[OF assms(1) ab]
-  from this(3) guess u v by (elim exE) note b=this
-  show "(content b *\<^sub>R f a) \<bullet> i \<le> (content b *\<^sub>R g a) \<bullet> i"
-    unfolding b inner_simps real_scaleR_def
-    apply (rule mult_left_mono)
-    using assms(2) tagged
-    by (auto simp add: content_pos_le)
+  fix x K
+  assume ab: "(x, K) \<in> p"
+  with p obtain u v where K: "K = cbox u v"
+    by blast
+  then show "(content K *\<^sub>R f x) \<bullet> i \<le> (content K *\<^sub>R g x) \<bullet> i"
+    by (metis ab assms inner_scaleR_left measure_nonneg mult_left_mono tag_in_interval)
qed

lemma has_integral_component_le:
@@ -1582,7 +1582,7 @@
guess d1 using f_i[unfolded has_integral,rule_format,OF *] by (elim exE conjE) note d1=this[rule_format]
guess d2 using g_j[unfolded has_integral,rule_format,OF *] by (elim exE conjE) note d2=this[rule_format]
obtain p where p: "p tagged_division_of cbox a b" "d1 fine p" "d2 fine p"
-       using fine_division_exists[OF gauge_Int[OF d1(1) d2(1)], of a b] unfolding fine_inter
+       using fine_division_exists[OF gauge_Int[OF d1(1) d2(1)], of a b] unfolding fine_Int
by metis
note le_less_trans[OF Basis_le_norm[OF k]]
then have "\<bar>((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - i) \<bullet> k\<bar> < (i \<bullet> k - j \<bullet> k) / 3"
@@ -1591,8 +1591,8 @@
by blast+
then show False
unfolding inner_simps
-      using rsum_component_le[OF p(1) le]
-      by (simp add: abs_real_def split: if_split_asm)
+      using rsum_component_le[OF p(1)] le
+      by (force simp add: abs_real_def split: if_split_asm)
qed
show ?thesis
proof (cases "\<exists>a b. s = cbox a b")
@@ -1787,7 +1787,7 @@
finally have "norm (i1 - i2) < e" .
} note triangle3 = this
have finep: "gm fine p" "gn fine p"
-        using fine_inter p  by auto
+        using fine_Int p  by auto
{ fix x
assume x: "x \<in> cbox a b"
have "norm (f x - g n x) + norm (f x - g m x) \<le> inverse (real n + 1) + inverse (real m + 1)"
@@ -4444,7 +4444,7 @@
have *: "(\<lambda>x. f (- x)) integrable_on {-b .. -a}" "- b < - c" "- c \<le> - a"
using assms by auto
from indefinite_integral_continuous_left[OF * \<open>e>0\<close>] guess d . note d = this
-  let ?d = "min d (b - c)"
+  let ?d = "min d (b - c)"
show ?thesis
apply (rule that[of "?d"])
apply safe
@@ -4471,92 +4471,62 @@
qed
qed

-lemma indefinite_integral_continuous:
+lemma indefinite_integral_continuous_1:
fixes f :: "real \<Rightarrow> 'a::banach"
assumes "f integrable_on {a .. b}"
shows "continuous_on {a .. b} (\<lambda>x. integral {a .. x} f)"
-proof (unfold continuous_on_iff, safe)
-  fix x e :: real
-  assume as: "x \<in> {a .. b}" "e > 0"
-  let ?thesis = "\<exists>d>0. \<forall>x'\<in>{a .. b}. dist x' x < d \<longrightarrow> dist (integral {a .. x'} f) (integral {a .. x} f) < e"
-  {
-    presume *: "a < b \<Longrightarrow> ?thesis"
-    show ?thesis
-      apply cases
-      apply (rule *)
-      apply assumption
-    proof goal_cases
-      case 1
-      then have "cbox a b = {x}"
-        using as(1)
-        apply -
-        apply (rule set_eqI)
-        apply auto
+proof -
+  have "\<exists>d>0. \<forall>x'\<in>{a..b}. dist x' x < d \<longrightarrow> dist (integral {a..x'} f) (integral {a..x} f) < e"
+       if x: "x \<in> {a..b}" and "e > 0" for x e :: real
+  proof (cases "a = b")
+    case True
+    with that show ?thesis by force
+  next
+    case False
+    with x have "a < b" by force
+    with x consider "x = a" | "x = b" | "a < x" "x < b"
+      by force
+    then show ?thesis
+    proof cases
+      case 1 show ?thesis
+        apply (rule indefinite_integral_continuous_right [OF assms _ \<open>a < b\<close> \<open>e > 0\<close>], force)
+        using \<open>x = a\<close> apply (force simp: dist_norm algebra_simps)
+        done
+    next
+      case 2 show ?thesis
+        apply (rule indefinite_integral_continuous_left [OF assms \<open>a < b\<close> _ \<open>e > 0\<close>], force)
+        using \<open>x = b\<close> apply (force simp: dist_norm norm_minus_commute algebra_simps)
done
-      then show ?case using \<open>e > 0\<close> by auto
-    qed
-  }
-  assume "a < b"
-  have "(x = a \<or> x = b) \<or> (a < x \<and> x < b)"
-    using as(1) by auto
-  then show ?thesis
-    apply (elim disjE)
-  proof -
-    assume "x = a"
-    have "a \<le> a" ..
-    from indefinite_integral_continuous_right[OF assms(1) this \<open>a<b\<close> \<open>e>0\<close>] guess d . note d=this
-    show ?thesis
-      apply rule
-      apply rule
-      apply (rule d)
-      apply safe
-      apply (subst dist_commute)
-      unfolding \<open>x = a\<close> dist_norm
-      apply (rule d(2)[rule_format])
-      apply auto
-      done
-  next
-    assume "x = b"
-    have "b \<le> b" ..
-    from indefinite_integral_continuous_left[OF assms(1) \<open>a<b\<close> this \<open>e>0\<close>] guess d . note d=this
-    show ?thesis
-      apply rule
-      apply rule
-      apply (rule d)
-      apply safe
-      apply (subst dist_commute)
-      unfolding \<open>x = b\<close> dist_norm
-      apply (rule d(2)[rule_format])
-      apply auto
-      done
-  next
-    assume "a < x \<and> x < b"
-    then have xl: "a < x" "x \<le> b" and xr: "a \<le> x" "x < b"
-      by auto
-    from indefinite_integral_continuous_left [OF assms(1) xl \<open>e>0\<close>] guess d1 . note d1=this
-    from indefinite_integral_continuous_right[OF assms(1) xr \<open>e>0\<close>] guess d2 . note d2=this
-    show ?thesis
-      apply (rule_tac x="min d1 d2" in exI)
-    proof safe
-      show "0 < min d1 d2"
-        using d1 d2 by auto
-      fix y
-      assume "y \<in> {a .. b}" and "dist y x < min d1 d2"
-      then show "dist (integral {a .. y} f) (integral {a .. x} f) < e"
-        apply (subst dist_commute)
-        apply (cases "y < x")
-        unfolding dist_norm
-        apply (rule d1(2)[rule_format])
-        defer
-        apply (rule d2(2)[rule_format])
-        unfolding not_less
-        apply (auto simp add: field_simps)
-        done
+    next
+      case 3
+      obtain d1 where "0 < d1"
+        and d1: "\<And>t. \<lbrakk>x - d1 < t; t \<le> x\<rbrakk> \<Longrightarrow> norm (integral {a..x} f - integral {a..t} f) < e"
+        using 3 by (auto intro: indefinite_integral_continuous_left [OF assms \<open>a < x\<close> _ \<open>e > 0\<close>])
+      obtain d2 where "0 < d2"
+        and d2: "\<And>t. \<lbrakk>x \<le> t; t < x + d2\<rbrakk> \<Longrightarrow> norm (integral {a..x} f - integral {a..t} f) < e"
+        using 3 by (auto intro: indefinite_integral_continuous_right [OF assms _ \<open>x < b\<close> \<open>e > 0\<close>])
+      show ?thesis
+      proof (intro exI ballI conjI impI)
+        show "0 < min d1 d2"
+          using \<open>0 < d1\<close> \<open>0 < d2\<close> by simp
+        show "dist (integral {a..y} f) (integral {a..x} f) < e"
+             if "y \<in> {a..b}" "dist y x < min d1 d2" for y
+        proof (cases "y < x")
+          case True
+          with that d1 show ?thesis by (auto simp: dist_commute dist_norm)
+        next
+          case False
+          with that d2 show ?thesis
+            by (auto simp: dist_commute dist_norm)
+        qed
+      qed
qed
qed
+  then show ?thesis
+    by (auto simp: continuous_on_iff)
qed

-lemma indefinite_integral_continuous':
+lemma indefinite_integral_continuous_1':
fixes f::"real \<Rightarrow> 'a::banach"
assumes "f integrable_on {a..b}"
shows "continuous_on {a..b} (\<lambda>x. integral {x..b} f)"
@@ -4565,7 +4535,7 @@
using integral_combine[OF _ _ assms, of x] that
by (auto simp: algebra_simps)
with _ show ?thesis
-    by (rule continuous_on_eq) (auto intro!: continuous_intros indefinite_integral_continuous assms)
+    by (rule continuous_on_eq) (auto intro!: continuous_intros indefinite_integral_continuous_1 assms)
qed

@@ -5248,7 +5218,7 @@
assumes "negligible ((S - T) \<union> (T - S))"
shows "f integrable_on S \<longleftrightarrow> f integrable_on T"
by (blast intro: integrable_spike_set assms negligible_subset)
-
+
lemma has_integral_interior:
fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
shows "negligible(frontier S) \<Longrightarrow> (f has_integral y) (interior S) \<longleftrightarrow> (f has_integral y) S"
@@ -5256,7 +5226,7 @@
apply (auto simp: frontier_def Un_Diff closure_def)
apply (metis Diff_eq_empty_iff interior_subset negligible_empty)
done
-
+
lemma has_integral_closure:
fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
shows "negligible(frontier S) \<Longrightarrow> (f has_integral y) (closure S) \<longleftrightarrow> (f has_integral y) S"
@@ -5593,10 +5563,10 @@
qed
then show ?thesis
by (rule_tac x="\<lambda>x. d1 x \<inter> d2 x" in exI)
-        (auto simp: fine_inter intro: \<open>gauge d1\<close> \<open>gauge d2\<close> d1 d2)
+        (auto simp: fine_Int intro: \<open>gauge d1\<close> \<open>gauge d2\<close> d1 d2)
qed
then show ?thesis
qed

@@ -5605,142 +5575,123 @@
\<bar>i - j\<bar> < e \<and> (\<forall>x\<in>s. g x \<le> f x \<and> f x \<le> h x)"
shows "f integrable_on s"
proof -
-  have "\<And>a b. (\<lambda>x. if x \<in> s then f x else 0) integrable_on cbox a b"
-    case (1 a b e)
+  let ?fs = "(\<lambda>x. if x \<in> s then f x else 0)"
+  have "?fs integrable_on cbox a b" for a b
+    fix e::real
+    assume "e > 0"
then have *: "e/4 > 0"
by auto
-    from assms[rule_format,OF this] guess g h i j by (elim exE conjE) note obt=this
-    note obt(1)[unfolded has_integral_alt'[of g]]
-    note conjunctD2[OF this, rule_format]
-    note g = this(1) and this(2)[OF *]
-    from this(2) guess B1 .. note B1 = conjunctD2[OF this,rule_format]
-    note obt(2)[unfolded has_integral_alt'[of h]]
-    note conjunctD2[OF this, rule_format]
-    note h = this(1) and this(2)[OF *]
-    from this(2) guess B2 .. note B2 = conjunctD2[OF this,rule_format]
-    define c :: 'n where "c = (\<Sum>i\<in>Basis. min (a\<bullet>i) (- (max B1 B2)) *\<^sub>R i)"
-    define d :: 'n where "d = (\<Sum>i\<in>Basis. max (b\<bullet>i) (max B1 B2) *\<^sub>R i)"
-    have *: "ball 0 B1 \<subseteq> cbox c d" "ball 0 B2 \<subseteq> cbox c d"
-      apply safe
-      unfolding mem_ball mem_box dist_norm
-      apply (rule_tac[!] ballI)
-    proof goal_cases
-      case (1 x i)
-      then show ?case using Basis_le_norm[of i x]
-        unfolding c_def d_def by auto
-    next
-      case (2 x i)
-      then show ?case using Basis_le_norm[of i x]
-        unfolding c_def d_def by auto
-    qed
-    have **: "\<And>ch cg ag ah::real. norm (ah - ag) \<le> norm (ch - cg) \<Longrightarrow> norm (cg - i) < e / 4 \<Longrightarrow>
-      norm (ch - j) < e / 4 \<Longrightarrow> abs (ag - ah) < e"
-      using obt(3)
-      unfolding real_norm_def
-      by arith
-    show ?case
-      apply (rule_tac x="\<lambda>x. if x \<in> s then g x else 0" in exI)
-      apply (rule_tac x="\<lambda>x. if x \<in> s then h x else 0" in exI)
-      apply (rule_tac x="integral (cbox a b) (\<lambda>x. if x \<in> s then g x else 0)" in exI)
-      apply (rule_tac x="integral (cbox a b) (\<lambda>x. if x \<in> s then h x else 0)" in exI)
-      apply safe
-      apply (rule_tac[1-2] integrable_integral,rule g)
-         apply (rule h)
-      apply (rule **[OF _ B1(2)[OF *(1)] B2(2)[OF *(2)]])
-    proof -
-      have *: "\<And>x f g. (if x \<in> s then f x else 0) - (if x \<in> s then g x else 0) =
-        (if x \<in> s then f x - g x else (0::real))"
+    with assms obtain g h i j where g: "(g has_integral i) s" and h: "(h has_integral j) s"
+                 and ij: "\<bar>i - j\<bar> < e/4"
+                 and fgh: "\<And>x. x \<in> s \<Longrightarrow> g x \<le> f x \<and> f x \<le> h x"
+      by metis
+    let ?gs = "(\<lambda>x. if x \<in> s then g x else 0)"
+    let ?hs = "(\<lambda>x. if x \<in> s then h x else 0)"
+    obtain Bg where Bg: "\<And>a b. ball 0 Bg \<subseteq> cbox a b \<Longrightarrow> \<bar>integral (cbox a b) ?gs - i\<bar> < e/4"
+              and int_g: "\<And>a b. ?gs integrable_on cbox a b"
+      using g * unfolding has_integral_alt' real_norm_def by meson
+    obtain Bh where
+          Bh: "\<And>a b. ball 0 Bh \<subseteq> cbox a b \<Longrightarrow> \<bar>integral (cbox a b) ?hs - j\<bar> < e/4"
+         and int_h: "\<And>a b. ?hs integrable_on cbox a b"
+      using h * unfolding has_integral_alt' real_norm_def by meson
+    define c where "c = (\<Sum>i\<in>Basis. min (a\<bullet>i) (- (max Bg Bh)) *\<^sub>R i)"
+    define d where "d = (\<Sum>i\<in>Basis. max (b\<bullet>i) (max Bg Bh) *\<^sub>R i)"
+    have "\<lbrakk>norm (0 - x) < Bg; i \<in> Basis\<rbrakk> \<Longrightarrow> c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i" for x i
+      using Basis_le_norm[of i x] unfolding c_def d_def by auto
+    then have ballBg: "ball 0 Bg \<subseteq> cbox c d"
+      by (auto simp: mem_box dist_norm)
+    have "\<lbrakk>norm (0 - x) < Bh; i \<in> Basis\<rbrakk> \<Longrightarrow> c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i" for x i
+      using Basis_le_norm[of i x] unfolding c_def d_def by auto
+    then have ballBh: "ball 0 Bh \<subseteq> cbox c d"
+      by (auto simp: mem_box dist_norm)
+    have ab_cd: "cbox a b \<subseteq> cbox c d"
+      by (auto simp: c_def d_def subset_box_imp)
+    have **: "\<And>ch cg ag ah::real. \<lbrakk>\<bar>ah - ag\<bar> \<le> \<bar>ch - cg\<bar>; \<bar>cg - i\<bar> < e/4; \<bar>ch - j\<bar> < e/4\<rbrakk>
+       \<Longrightarrow> \<bar>ag - ah\<bar> < e"
+      using ij by arith
+    show "\<exists>g h i j. (g has_integral i) (cbox a b) \<and> (h has_integral j) (cbox a b) \<and> \<bar>i - j\<bar> < e \<and>
+          (\<forall>x\<in>cbox a b. g x \<le> (if x \<in> s then f x else 0) \<and>
+                        (if x \<in> s then f x else 0) \<le> h x)"
+    proof (intro exI ballI conjI)
+      have eq: "\<And>x f g. (if x \<in> s then f x else 0) - (if x \<in> s then g x else 0) =
+                       (if x \<in> s then f x - g x else (0::real))"
by auto
-      note ** = abs_of_nonneg[OF integral_nonneg[OF integrable_diff, OF h g]]
-      show "norm (integral (cbox a b) (\<lambda>x. if x \<in> s then h x else 0) -
-          integral (cbox a b) (\<lambda>x. if x \<in> s then g x else 0)) \<le>
-        norm (integral (cbox c d) (\<lambda>x. if x \<in> s then h x else 0) -
-          integral (cbox c d) (\<lambda>x. if x \<in> s then g x else 0))"
-        unfolding integral_diff[OF h g,symmetric] real_norm_def
-        apply (subst **)
-        defer
-        apply (subst **)
-        defer
-        apply (rule has_integral_subset_le)
-        defer
-        apply (rule integrable_integral integrable_diff h g)+
-      proof safe
-        fix x
-        assume "x \<in> cbox a b"
-        then show "x \<in> cbox c d"
-          unfolding mem_box c_def d_def
-          apply -
-          apply rule
-          apply (erule_tac x=i in ballE)
-          apply auto
-          done
-      qed (insert obt(4), auto)
-    qed (insert obt(4), auto)
-  qed
-  note interv = this
-
-  show ?thesis
-    unfolding integrable_alt[of f]
-    apply safe
-    apply (rule interv)
-  proof goal_cases
-    case (1 e)
-    then have *: "e/3 > 0"
-      by auto
-    from assms[rule_format,OF this] guess g h i j by (elim exE conjE) note obt=this
-    note obt(1)[unfolded has_integral_alt'[of g]]
-    note conjunctD2[OF this, rule_format]
-    note g = this(1) and this(2)[OF *]
-    from this(2) guess B1 .. note B1 = conjunctD2[OF this,rule_format]
-    note obt(2)[unfolded has_integral_alt'[of h]]
-    note conjunctD2[OF this, rule_format]
-    note h = this(1) and this(2)[OF *]
-    from this(2) guess B2 .. note B2 = conjunctD2[OF this,rule_format]
-    show ?case
-      apply (rule_tac x="max B1 B2" in exI)
-      apply safe
-      apply (rule max.strict_coboundedI1)
-      apply (rule B1)
-    proof -
-      fix a b c d :: 'n
-      assume as: "ball 0 (max B1 B2) \<subseteq> cbox a b" "ball 0 (max B1 B2) \<subseteq> cbox c d"
-      have **: "ball 0 B1 \<subseteq> ball (0::'n) (max B1 B2)" "ball 0 B2 \<subseteq> ball (0::'n) (max B1 B2)"
-        by auto
-      have *: "\<And>ga gc ha hc fa fc::real.
-        \<bar>ga - i\<bar> < e / 3 \<and> \<bar>gc - i\<bar> < e / 3 \<and> \<bar>ha - j\<bar> < e / 3 \<and>
-        \<bar>hc - j\<bar> < e / 3 \<and> \<bar>i - j\<bar> < e / 3 \<and> ga \<le> fa \<and> fa \<le> ha \<and> gc \<le> fc \<and> fc \<le> hc \<Longrightarrow>
-        \<bar>fa - fc\<bar> < e"
-        by (simp add: abs_real_def split: if_split_asm)
-      show "norm (integral (cbox a b) (\<lambda>x. if x \<in> s then f x else 0) - integral (cbox c d)
-        (\<lambda>x. if x \<in> s then f x else 0)) < e"
-        unfolding real_norm_def
-        apply (rule *)
-        apply safe
-        unfolding real_norm_def[symmetric]
-        apply (rule B1(2))
-        apply (rule order_trans)
+      have int_hg: "(\<lambda>x. if x \<in> s then h x - g x else 0) integrable_on cbox a b"
+                   "(\<lambda>x. if x \<in> s then h x - g x else 0) integrable_on cbox c d"
+        by (metis (no_types) integrable_diff g h has_integral_integrable integrable_altD(1))+
+      show "(?gs has_integral integral (cbox a b) ?gs) (cbox a b)"
+           "(?hs has_integral integral (cbox a b) ?hs) (cbox a b)"
+        by (intro integrable_integral int_g int_h)+
+      then have "integral (cbox a b) ?gs \<le> integral (cbox a b) ?hs"
+        apply (rule has_integral_le)
+        using fgh by force
+      then have "0 \<le> integral (cbox a b) ?hs - integral (cbox a b) ?gs"
+        by simp
+      then have "\<bar>integral (cbox a b) ?hs - integral (cbox a b) ?gs\<bar>
+              \<le> \<bar>integral (cbox c d) ?hs - integral (cbox c d) ?gs\<bar>"
+        apply (simp add: integral_diff [symmetric] int_g int_h)
+        apply (subst abs_of_nonneg[OF integral_nonneg[OF integrable_diff, OF int_h int_g]])
+        using fgh apply (force simp: eq intro!: integral_subset_le [OF ab_cd int_hg])+
+        done
+      then show "\<bar>integral (cbox a b) ?gs - integral (cbox a b) ?hs\<bar> < e"
apply (rule **)
-        apply (rule as(1))
-        apply (rule B1(2))
-        apply (rule order_trans)
-        apply (rule **)
-        apply (rule as(2))
-        apply (rule B2(2))
-        apply (rule order_trans)
-        apply (rule **)
-        apply (rule as(1))
-        apply (rule B2(2))
-        apply (rule order_trans)
-        apply (rule **)
-        apply (rule as(2))
-        using obt(3) apply auto[1]
-        apply (rule_tac[!] integral_le)
-        using obt
-        apply (auto intro!: h g interv)
+         apply (rule Bg ballBg Bh ballBh)+
done
+      show "\<And>x. x \<in> cbox a b \<Longrightarrow> ?gs x \<le> ?fs x" "\<And>x. x \<in> cbox a b \<Longrightarrow> ?fs x \<le> ?hs x"
+        using fgh by auto
qed
qed
+  then have int_f: "?fs integrable_on cbox a b" for a b
+    by simp
+  have "\<exists>B>0. \<forall>a b c d.
+                  ball 0 B \<subseteq> cbox a b \<and> ball 0 B \<subseteq> cbox c d \<longrightarrow>
+                  abs (integral (cbox a b) ?fs - integral (cbox c d) ?fs) < e"
+      if "0 < e" for e
+  proof -
+    have *: "e/3 > 0"
+      using that by auto
+    with assms obtain g h i j where g: "(g has_integral i) s" and h: "(h has_integral j) s"
+                 and ij: "\<bar>i - j\<bar> < e/3"
+                 and fgh: "\<And>x. x \<in> s \<Longrightarrow> g x \<le> f x \<and> f x \<le> h x"
+      by metis
+    let ?gs = "(\<lambda>x. if x \<in> s then g x else 0)"
+    let ?hs = "(\<lambda>x. if x \<in> s then h x else 0)"
+    obtain Bg where "Bg > 0"
+              and Bg: "\<And>a b. ball 0 Bg \<subseteq> cbox a b \<Longrightarrow> \<bar>integral (cbox a b) ?gs - i\<bar> < e/3"
+              and int_g: "\<And>a b. ?gs integrable_on cbox a b"
+      using g * unfolding has_integral_alt' real_norm_def by meson
+    obtain Bh where "Bh > 0"
+              and Bh: "\<And>a b. ball 0 Bh \<subseteq> cbox a b \<Longrightarrow> \<bar>integral (cbox a b) ?hs - j\<bar> < e/3"
+              and int_h: "\<And>a b. ?hs integrable_on cbox a b"
+      using h * unfolding has_integral_alt' real_norm_def by meson
+    { fix a b c d :: 'n
+      assume as: "ball 0 (max Bg Bh) \<subseteq> cbox a b" "ball 0 (max Bg Bh) \<subseteq> cbox c d"
+      have **: "ball 0 Bg \<subseteq> ball (0::'n) (max Bg Bh)" "ball 0 Bh \<subseteq> ball (0::'n) (max Bg Bh)"
+        by auto
+      have *: "\<And>ga gc ha hc fa fc. \<lbrakk>\<bar>ga - i\<bar> < e/3; \<bar>gc - i\<bar> < e/3; \<bar>ha - j\<bar> < e/3;
+                     \<bar>hc - j\<bar> < e/3; ga \<le> fa; fa \<le> ha; gc \<le> fc; fc \<le> hc\<rbrakk> \<Longrightarrow>
+        \<bar>fa - fc\<bar> < e"
+        using ij by arith
+      have "abs (integral (cbox a b) (\<lambda>x. if x \<in> s then f x else 0) - integral (cbox c d)
+        (\<lambda>x. if x \<in> s then f x else 0)) < e"
+      proof (rule *)
+        show "\<bar>integral (cbox a b) ?gs - i\<bar> < e/3"
+          using "**" Bg as by blast
+        show "\<bar>integral (cbox c d) ?gs - i\<bar> < e/3"
+          using "**" Bg as by blast
+        show "\<bar>integral (cbox a b) ?hs - j\<bar> < e/3"
+          using "**" Bh as by blast
+        show "\<bar>integral (cbox c d) ?hs - j\<bar> < e/3"
+          using "**" Bh as by blast
+      qed (use int_f int_g int_h fgh in \<open>simp_all add: integral_le\<close>)
+    }
+    then show ?thesis
+      apply (rule_tac x="max Bg Bh" in exI)
+        using \<open>Bg > 0\<close> by auto
+  qed
+  then show ?thesis
+    unfolding integrable_alt[of f] real_norm_def by (blast intro: int_f)
qed

@@ -6043,7 +5994,7 @@
then show ?case
apply (rule_tac x=qq in exI)
using dd(2)[of qq]
-      unfolding fine_inter uv
+      unfolding fine_Int uv
apply auto
done
qed
@@ -6054,9 +6005,9 @@
apply (rule assms(4)[rule_format])
proof
show "d fine ?p"
-      apply (rule fine_union)
+      apply (rule fine_Un)
apply (rule p)
-      apply (rule fine_unions)
+      apply (rule fine_Union)
using qq
apply auto
done
@@ -6952,7 +6903,7 @@
using that(3) as
apply auto
done
-    qed (insert p[unfolded fine_inter], auto)
+    qed (insert p[unfolded fine_Int], auto)
qed

{ presume "\<And>e. 0 < e \<Longrightarrow> norm (integral s f) < integral s g + e"
@@ -7400,7 +7351,7 @@
proof -
let ?F = "\<lambda>x. integral {c..g x} f"
have cont_int: "continuous_on {a..b} ?F"
-    by (rule continuous_on_compose2[OF _ g subset] indefinite_integral_continuous
+    by (rule continuous_on_compose2[OF _ g subset] indefinite_integral_continuous_1
f integrable_continuous_real)+
have deriv: "(((\<lambda>x. integral {c..x} f) \<circ> g) has_vector_derivative g' x *\<^sub>R f (g x))
(at x within {a..b})" if "x \<in> {a..b} - s" for x```
```--- a/src/HOL/Analysis/Tagged_Division.thy	Sat Jun 24 21:23:48 2017 +0200
+++ b/src/HOL/Analysis/Tagged_Division.thy	Mon Jun 26 14:26:03 2017 +0100
@@ -1982,17 +1982,17 @@
shows "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> d x"
using assms unfolding fine_def by auto

-lemma fine_inter: "(\<lambda>x. d1 x \<inter> d2 x) fine p \<longleftrightarrow> d1 fine p \<and> d2 fine p"
+lemma fine_Int: "(\<lambda>x. d1 x \<inter> d2 x) fine p \<longleftrightarrow> d1 fine p \<and> d2 fine p"
unfolding fine_def by auto

-lemma fine_inters:
+lemma fine_Inter:
"(\<lambda>x. \<Inter>{f d x | d.  d \<in> s}) fine p \<longleftrightarrow> (\<forall>d\<in>s. (f d) fine p)"
unfolding fine_def by blast

-lemma fine_union: "d fine p1 \<Longrightarrow> d fine p2 \<Longrightarrow> d fine (p1 \<union> p2)"
+lemma fine_Un: "d fine p1 \<Longrightarrow> d fine p2 \<Longrightarrow> d fine (p1 \<union> p2)"
unfolding fine_def by blast

-lemma fine_unions: "(\<And>p. p \<in> ps \<Longrightarrow> d fine p) \<Longrightarrow> d fine (\<Union>ps)"
+lemma fine_Union: "(\<And>p. p \<in> ps \<Longrightarrow> d fine p) \<Longrightarrow> d fine (\<Union>ps)"
unfolding fine_def by auto

lemma fine_subset: "p \<subseteq> q \<Longrightarrow> d fine q \<Longrightarrow> d fine p"
@@ -2000,7 +2000,7 @@

subsection \<open>Some basic combining lemmas.\<close>

-lemma tagged_division_unions_exists:
+lemma tagged_division_Union_exists:
assumes "finite iset"
and "\<forall>i\<in>iset. \<exists>p. p tagged_division_of i \<and> d fine p"
and "\<forall>i1\<in>iset. \<forall>i2\<in>iset. i1 \<noteq> i2 \<longrightarrow> interior i1 \<inter> interior i2 = {}"
@@ -2014,7 +2014,7 @@
show thesis
apply (rule_tac p="\<Union>(pfn ` iset)" in that)
using assms(1) assms(3) assms(4) pfn(1) tagged_division_unions apply force
-    by (metis (mono_tags, lifting) fine_unions imageE pfn(2))
+    by (metis (mono_tags, lifting) fine_Union imageE pfn(2))
qed

@@ -2367,7 +2367,7 @@
\<not> (\<exists>p. p tagged_division_of cbox c d \<and> g fine p)"
apply (rule interval_bisection[of "\<lambda>s. \<exists>p. p tagged_division_of s \<and> g fine p", OF _ _ as])
-    apply (metis tagged_division_union fine_union)
+    apply (metis tagged_division_union fine_Un)
apply (auto simp: )
done
obtain e where e: "e > 0" "ball x e \<subseteq> g x"
@@ -2477,7 +2477,7 @@
apply (rule q1)
apply (rule int)
apply rule
-        apply (rule fine_union)
+        apply (rule fine_Un)
apply (subst fine_def)
defer
apply (rule q1)
@@ -2500,10 +2500,10 @@
apply (rule_tac x="q2 \<union> q1" in exI)
apply rule
unfolding * uv
-        apply (rule tagged_division_union q2 q1 int fine_union)+
+        apply (rule tagged_division_union q2 q1 int fine_Un)+
unfolding Ball_def split_paired_All split_conv
apply rule
-        apply (rule fine_union)
+        apply (rule fine_Un)
apply (rule q1 q2)+
apply rule
apply rule
@@ -2806,7 +2806,7 @@
fix g1 g2 :: "'a \<Rightarrow> 'a set" show "gauge g1 \<Longrightarrow> gauge g2 \<Longrightarrow> \<exists>x. gauge x \<and>
{p. p tagged_division_of s \<and> x fine p} \<subseteq> {p. p tagged_division_of s \<and> g1 fine p} \<and>
{p. p tagged_division_of s \<and> x fine p} \<subseteq> {p. p tagged_division_of s \<and> g2 fine p}"
-    by (intro exI[of _ "\<lambda>x. g1 x \<inter> g2 x"]) (auto simp: fine_inter)
+    by (intro exI[of _ "\<lambda>x. g1 x \<inter> g2 x"]) (auto simp: fine_Int)
qed (auto simp: eventually_principal)

lemma division_filter_not_empty: "division_filter (cbox a b) \<noteq> bot"```
```--- a/src/HOL/Probability/Probability_Mass_Function.thy	Sat Jun 24 21:23:48 2017 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Mon Jun 26 14:26:03 2017 +0100
@@ -850,7 +850,7 @@
proof (subst set_borel_integral_eq_integral)
{ fix b :: real assume "a \<le> b"
from f[OF this] have "continuous_on {a..b} (\<lambda>b. integral {a..b} f)"
-      by (intro indefinite_integral_continuous set_borel_integral_eq_integral) }
+      by (intro indefinite_integral_continuous_1 set_borel_integral_eq_integral) }
note * = this

have "continuous_on (\<Union>b\<in>{a..}. {a <..< b}) (\<lambda>b. integral {a..b} f)"```