# HG changeset patch
# User paulson
# Date 1523635257 -3600
# Node ID 06bce659d41bdbe05f5ec799f32969d347c12931
# Parent  9ecc78bcf1efa72c17408640efb6de213b8ad02f# Parent  557ea2740125b35d5fbcf6cc4ad7419134b789f1
merged

diff -r 9ecc78bcf1ef -r 06bce659d41b src/HOL/Analysis/Ball_Volume.thy
--- a/src/HOL/Analysis/Ball_Volume.thy	Fri Apr 13 17:25:02 2018 +0200
+++ b/src/HOL/Analysis/Ball_Volume.thy	Fri Apr 13 17:00:57 2018 +0100
@@ -43,7 +43,7 @@
   also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (x\<^sup>2 powr - (1 / 2) * (1 - x\<^sup>2) powr (real n / 2) * (2 * x) *
                           indicator {0..1} x) \<partial>lborel)"
     by (subst nn_integral_substitution[where g = "\<lambda>x. x ^ 2" and g' = "\<lambda>x. 2 * x"])
-       (auto intro!: derivative_eq_intros continuous_intros)
+       (auto intro!: derivative_eq_intros continuous_intros simp: set_borel_measurable_def)
   also have "\<dots> = (\<integral>\<^sup>+ x. 2 * ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel)"
     by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"]) 
        (auto simp: indicator_def powr_minus powr_half_sqrt divide_simps ennreal_mult' mult_ac)
diff -r 9ecc78bcf1ef -r 06bce659d41b src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Fri Apr 13 17:25:02 2018 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Fri Apr 13 17:00:57 2018 +0100
@@ -1545,7 +1545,7 @@
     using that by (subst Ln_minus) (auto simp: Ln_of_real)
   have **: "Ln (of_real x) = of_real (ln (-x)) + \<i> * pi" if "x < 0" for x
     using *[of "-x"] that by simp
-  have cont: "set_borel_measurable borel (- \<real>\<^sub>\<le>\<^sub>0) Ln"
+  have cont: "(\<lambda>x. indicat_real (- \<real>\<^sub>\<le>\<^sub>0) x *\<^sub>R Ln x) \<in> borel_measurable borel"
     by (intro borel_measurable_continuous_on_indicator continuous_intros) auto
   have "(\<lambda>x. if x \<in> \<real>\<^sub>\<le>\<^sub>0 then ln (-Re x) + \<i> * pi else indicator (-\<real>\<^sub>\<le>\<^sub>0) x *\<^sub>R Ln x) \<in> borel \<rightarrow>\<^sub>M borel"
     (is "?f \<in> _") by (rule measurable_If_set[OF _ cont]) auto
diff -r 9ecc78bcf1ef -r 06bce659d41b src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Apr 13 17:25:02 2018 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Apr 13 17:00:57 2018 +0100
@@ -839,13 +839,15 @@
 lemma set_integral_reflect:
   fixes S and f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
   shows "(LBINT x : S. f x) = (LBINT x : {x. - x \<in> S}. f (- x))"
+  unfolding set_lebesgue_integral_def
   by (subst lborel_integral_real_affine[where c="-1" and t=0])
      (auto intro!: Bochner_Integration.integral_cong split: split_indicator)
 
 lemma borel_integrable_atLeastAtMost':
   fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
   assumes f: "continuous_on {a..b} f"
-  shows "set_integrable lborel {a..b} f" (is "integrable _ ?f")
+  shows "set_integrable lborel {a..b} f" 
+  unfolding set_integrable_def
   by (intro borel_integrable_compact compact_Icc f)
 
 lemma integral_FTC_atLeastAtMost:
@@ -857,7 +859,8 @@
 proof -
   let ?f = "\<lambda>x. indicator {a .. b} x *\<^sub>R f x"
   have "(?f has_integral (\<integral>x. ?f x \<partial>lborel)) UNIV"
-    using borel_integrable_atLeastAtMost'[OF f] by (rule has_integral_integral_lborel)
+    using borel_integrable_atLeastAtMost'[OF f]
+    unfolding set_integrable_def by (rule has_integral_integral_lborel)
   moreover
   have "(f has_integral F b - F a) {a .. b}"
     by (intro fundamental_theorem_of_calculus ballI assms) auto
@@ -876,7 +879,8 @@
 proof -
   let ?f = "\<lambda>x. indicator S x *\<^sub>R f x"
   have "(?f has_integral LINT x : S | lborel. f x) UNIV"
-    by (rule has_integral_integral_lborel) fact
+    using assms has_integral_integral_lborel 
+    unfolding set_integrable_def set_lebesgue_integral_def by blast
   hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
     apply (subst has_integral_restrict_UNIV [symmetric])
     apply (rule has_integral_eq)
@@ -893,8 +897,8 @@
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes f: "set_integrable lebesgue S f"
   shows "(f has_integral (LINT x:S|lebesgue. f x)) S"
-  using has_integral_integral_lebesgue[OF f]
-  by (simp_all add: indicator_def if_distrib[of "\<lambda>x. x *\<^sub>R f _"] has_integral_restrict_UNIV cong: if_cong)
+  using has_integral_integral_lebesgue f 
+  by (fastforce simp add: set_integrable_def set_lebesgue_integral_def indicator_def if_distrib[of "\<lambda>x. x *\<^sub>R f _"] cong: if_cong)
 
 lemma set_lebesgue_integral_eq_integral:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -915,26 +919,26 @@
 
 lemma absolutely_integrable_on_def:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  shows "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s \<and> (\<lambda>x. norm (f x)) integrable_on s"
+  shows "f absolutely_integrable_on S \<longleftrightarrow> f integrable_on S \<and> (\<lambda>x. norm (f x)) integrable_on S"
 proof safe
-  assume f: "f absolutely_integrable_on s"
-  then have nf: "integrable lebesgue (\<lambda>x. norm (indicator s x *\<^sub>R f x))"
-    by (intro integrable_norm)
-  note integrable_on_lebesgue[OF f] integrable_on_lebesgue[OF nf]
-  moreover have
-    "(\<lambda>x. indicator s x *\<^sub>R f x) = (\<lambda>x. if x \<in> s then f x else 0)"
-    "(\<lambda>x. norm (indicator s x *\<^sub>R f x)) = (\<lambda>x. if x \<in> s then norm (f x) else 0)"
+  assume f: "f absolutely_integrable_on S"
+  then have nf: "integrable lebesgue (\<lambda>x. norm (indicator S x *\<^sub>R f x))"
+    using integrable_norm set_integrable_def by blast
+  show "f integrable_on S"
+    by (rule set_lebesgue_integral_eq_integral[OF f])
+  have "(\<lambda>x. norm (indicator S x *\<^sub>R f x)) = (\<lambda>x. if x \<in> S then norm (f x) else 0)"
     by auto
-  ultimately show "f integrable_on s" "(\<lambda>x. norm (f x)) integrable_on s"
-    by (simp_all add: integrable_restrict_UNIV)
+  with integrable_on_lebesgue[OF nf] show "(\<lambda>x. norm (f x)) integrable_on S"
+    by (simp add: integrable_restrict_UNIV)
 next
-  assume f: "f integrable_on s" and nf: "(\<lambda>x. norm (f x)) integrable_on s"
-  show "f absolutely_integrable_on s"
+  assume f: "f integrable_on S" and nf: "(\<lambda>x. norm (f x)) integrable_on S"
+  show "f absolutely_integrable_on S"
+    unfolding set_integrable_def
   proof (rule integrableI_bounded)
-    show "(\<lambda>x. indicator s x *\<^sub>R f x) \<in> borel_measurable lebesgue"
-      using f has_integral_implies_lebesgue_measurable[of f _ s] by (auto simp: integrable_on_def)
-    show "(\<integral>\<^sup>+ x. ennreal (norm (indicator s x *\<^sub>R f x)) \<partial>lebesgue) < \<infinity>"
-      using nf nn_integral_has_integral_lebesgue[of "\<lambda>x. norm (f x)" _ s]
+    show "(\<lambda>x. indicator S x *\<^sub>R f x) \<in> borel_measurable lebesgue"
+      using f has_integral_implies_lebesgue_measurable[of f _ S] by (auto simp: integrable_on_def)
+    show "(\<integral>\<^sup>+ x. ennreal (norm (indicator S x *\<^sub>R f x)) \<partial>lebesgue) < \<infinity>"
+      using nf nn_integral_has_integral_lebesgue[of "\<lambda>x. norm (f x)" _ S]
       by (auto simp: integrable_on_def nn_integral_completion)
   qed
 qed
@@ -951,12 +955,13 @@
   by (auto simp: integrable_on_open_interval absolutely_integrable_on_def)
 
 lemma absolutely_integrable_restrict_UNIV:
-  "(\<lambda>x. if x \<in> s then f x else 0) absolutely_integrable_on UNIV \<longleftrightarrow> f absolutely_integrable_on s"
+  "(\<lambda>x. if x \<in> S then f x else 0) absolutely_integrable_on UNIV \<longleftrightarrow> f absolutely_integrable_on S"
+    unfolding set_integrable_def
   by (intro arg_cong2[where f=integrable]) auto
 
 lemma absolutely_integrable_onI:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  shows "f integrable_on s \<Longrightarrow> (\<lambda>x. norm (f x)) integrable_on s \<Longrightarrow> f absolutely_integrable_on s"
+  shows "f integrable_on S \<Longrightarrow> (\<lambda>x. norm (f x)) integrable_on S \<Longrightarrow> f absolutely_integrable_on S"
   unfolding absolutely_integrable_on_def by auto
 
 lemma nonnegative_absolutely_integrable_1:
@@ -984,7 +989,7 @@
 
 lemma lmeasurable_iff_integrable_on: "S \<in> lmeasurable \<longleftrightarrow> (\<lambda>x. 1::real) integrable_on S"
   by (subst absolutely_integrable_on_iff_nonneg[symmetric])
-     (simp_all add: lmeasurable_iff_integrable)
+     (simp_all add: lmeasurable_iff_integrable set_integrable_def)
 
 lemma lmeasure_integral_UNIV: "S \<in> lmeasurable \<Longrightarrow> measure lebesgue S = integral UNIV (indicator S)"
   by (simp add: lmeasurable_iff_has_integral integral_unique)
@@ -1532,7 +1537,8 @@
 lemma set_integral_norm_bound:
   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   shows "set_integrable M k f \<Longrightarrow> norm (LINT x:k|M. f x) \<le> LINT x:k|M. norm (f x)"
-  using integral_norm_bound[of M "\<lambda>x. indicator k x *\<^sub>R f x"] by simp
+  using integral_norm_bound[of M "\<lambda>x. indicator k x *\<^sub>R f x"] by (simp add: set_lebesgue_integral_def)
+
 
 lemma set_integral_finite_UN_AE:
   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
@@ -1557,13 +1563,13 @@
   with insert.hyps insert.IH[symmetric]
   show ?case
     by (auto intro!: set_integral_Un_AE sets.finite_UN f set_integrable_UN)
-qed simp
+qed (simp add: set_lebesgue_integral_def)
 
 lemma set_integrable_norm:
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   assumes f: "set_integrable M k f" shows "set_integrable M k (\<lambda>x. norm (f x))"
-  using integrable_norm[OF f] by simp
-
+  using integrable_norm f by (force simp add: set_integrable_def)
+ 
 lemma absolutely_integrable_bounded_variation:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes f: "f absolutely_integrable_on UNIV"
@@ -2120,30 +2126,36 @@
     and h :: "'n::euclidean_space \<Rightarrow> 'p::euclidean_space"
   shows "f absolutely_integrable_on s \<Longrightarrow> bounded_linear h \<Longrightarrow> (h \<circ> f) absolutely_integrable_on s"
   using integrable_bounded_linear[of h lebesgue "\<lambda>x. indicator s x *\<^sub>R f x"]
-  by (simp add: linear_simps[of h])
+  by (simp add: linear_simps[of h] set_integrable_def)
+
+lemma absolutely_integrable_zero [simp]: "(\<lambda>x. 0) absolutely_integrable_on S"
+    by (simp add: set_integrable_def)
 
 lemma absolutely_integrable_sum:
   fixes f :: "'a \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  assumes "finite t" and "\<And>a. a \<in> t \<Longrightarrow> (f a) absolutely_integrable_on s"
-  shows "(\<lambda>x. sum (\<lambda>a. f a x) t) absolutely_integrable_on s"
-  using assms(1,2) by induct auto
+  assumes "finite T" and "\<And>a. a \<in> T \<Longrightarrow> (f a) absolutely_integrable_on S"
+  shows "(\<lambda>x. sum (\<lambda>a. f a x) T) absolutely_integrable_on S"
+  using assms by induction auto
 
 lemma absolutely_integrable_integrable_bound:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  assumes le: "\<forall>x\<in>s. norm (f x) \<le> g x" and f: "f integrable_on s" and g: "g integrable_on s"
-  shows "f absolutely_integrable_on s"
+  assumes le: "\<And>x. x\<in>S \<Longrightarrow> norm (f x) \<le> g x" and f: "f integrable_on S" and g: "g integrable_on S"
+  shows "f absolutely_integrable_on S"
+    unfolding set_integrable_def
 proof (rule Bochner_Integration.integrable_bound)
-  show "g absolutely_integrable_on s"
+  have "g absolutely_integrable_on S"
     unfolding absolutely_integrable_on_def
   proof
-    show "(\<lambda>x. norm (g x)) integrable_on s"
+    show "(\<lambda>x. norm (g x)) integrable_on S"
       using le norm_ge_zero[of "f _"]
       by (intro integrable_spike_finite[OF _ _ g, of "{}"])
          (auto intro!: abs_of_nonneg intro: order_trans simp del: norm_ge_zero)
   qed fact
-  show "set_borel_measurable lebesgue s f"
+  then show "integrable lebesgue (\<lambda>x. indicat_real S x *\<^sub>R g x)"
+    by (simp add: set_integrable_def)
+  show "(\<lambda>x. indicat_real S x *\<^sub>R f x) \<in> borel_measurable lebesgue"
     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>)
+qed (use le in \<open>force intro!: always_eventually split: split_indicator\<close>)
 
 subsection \<open>Componentwise\<close>
 
@@ -2175,7 +2187,7 @@
 
 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"
-  by (simp add: absolutely_integrable_componentwise_iff)
+  using absolutely_integrable_componentwise_iff by blast
 
 lemma absolutely_integrable_component:
   "f absolutely_integrable_on A \<Longrightarrow> (\<lambda>x. f x \<bullet> (b :: 'b :: euclidean_space)) absolutely_integrable_on A"
@@ -2190,7 +2202,8 @@
   have "(\<lambda>x. c *\<^sub>R x) o f absolutely_integrable_on S"
     apply (rule absolutely_integrable_linear [OF assms])
     by (simp add: bounded_linear_scaleR_right)
-  then show ?thesis by simp
+  then show ?thesis
+    using assms by blast
 qed
 
 lemma absolutely_integrable_scaleR_right:
@@ -2202,7 +2215,7 @@
   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
+  using assms by (simp add: absolutely_integrable_on_def o_def)
     
 lemma absolutely_integrable_abs:
   fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
@@ -2405,56 +2418,60 @@
 
 lemma dominated_convergence:
   fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  assumes f: "\<And>k. (f k) integrable_on s" and h: "h integrable_on s"
-    and le: "\<And>k. \<forall>x \<in> s. norm (f k x) \<le> h x"
-    and conv: "\<forall>x \<in> s. (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
-  shows "g integrable_on s" "(\<lambda>k. integral s (f k)) \<longlonglongrightarrow> integral s g"
+  assumes f: "\<And>k. (f k) integrable_on S" and h: "h integrable_on S"
+    and le: "\<And>k x. x \<in> S \<Longrightarrow> norm (f k x) \<le> h x"
+    and conv: "\<forall>x \<in> S. (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
+  shows "g integrable_on S" "(\<lambda>k. integral S (f k)) \<longlonglongrightarrow> integral S g"
 proof -
-  have 3: "h absolutely_integrable_on s"
+  have 3: "h absolutely_integrable_on S"
     unfolding absolutely_integrable_on_def
   proof
-    show "(\<lambda>x. norm (h x)) integrable_on s"
+    show "(\<lambda>x. norm (h x)) integrable_on S"
     proof (intro integrable_spike_finite[OF _ _ h, of "{}"] ballI)
-      fix x assume "x \<in> s - {}" then show "norm (h x) = h x"
+      fix x assume "x \<in> S - {}" then show "norm (h x) = h x"
         by (metis Diff_empty abs_of_nonneg bot_set_def le norm_ge_zero order_trans real_norm_def)
     qed auto
   qed fact
-  have 2: "set_borel_measurable lebesgue s (f k)" for k
+  have 2: "set_borel_measurable lebesgue S (f k)" for k
+    unfolding set_borel_measurable_def
     using f by (auto intro: has_integral_implies_lebesgue_measurable simp: integrable_on_def)
-  then have 1: "set_borel_measurable lebesgue s g"
+  then have 1: "set_borel_measurable lebesgue S g"
+    unfolding set_borel_measurable_def
     by (rule borel_measurable_LIMSEQ_metric) (use conv in \<open>auto split: split_indicator\<close>)
-  have 4: "AE x in lebesgue. (\<lambda>i. indicator s x *\<^sub>R f i x) \<longlonglongrightarrow> indicator s x *\<^sub>R g x"
-    "AE x in lebesgue. norm (indicator s x *\<^sub>R f k x) \<le> indicator s x *\<^sub>R h x" for k
+  have 4: "AE x in lebesgue. (\<lambda>i. indicator S x *\<^sub>R f i x) \<longlonglongrightarrow> indicator S x *\<^sub>R g x"
+    "AE x in lebesgue. norm (indicator S x *\<^sub>R f k x) \<le> indicator S x *\<^sub>R h x" for k
     using conv le by (auto intro!: always_eventually split: split_indicator)
-
-  have g: "g absolutely_integrable_on s"
-    using 1 2 3 4 by (rule integrable_dominated_convergence)
-  then show "g integrable_on s"
+  have g: "g absolutely_integrable_on S"
+    using 1 2 3 4 unfolding set_borel_measurable_def set_integrable_def    
+    by (rule integrable_dominated_convergence)
+  then show "g integrable_on S"
     by (auto simp: absolutely_integrable_on_def)
-  have "(\<lambda>k. (LINT x:s|lebesgue. f k x)) \<longlonglongrightarrow> (LINT x:s|lebesgue. g x)"
-    using 1 2 3 4 by (rule integral_dominated_convergence)
-  then show "(\<lambda>k. integral s (f k)) \<longlonglongrightarrow> integral s g"
+  have "(\<lambda>k. (LINT x:S|lebesgue. f k x)) \<longlonglongrightarrow> (LINT x:S|lebesgue. g x)"
+    unfolding set_borel_measurable_def set_lebesgue_integral_def
+    using 1 2 3 4 unfolding set_borel_measurable_def set_lebesgue_integral_def set_integrable_def
+    by (rule integral_dominated_convergence)
+  then show "(\<lambda>k. integral S (f k)) \<longlonglongrightarrow> integral S g"
     using g absolutely_integrable_integrable_bound[OF le f h]
     by (subst (asm) (1 2) set_lebesgue_integral_eq_integral) auto
 qed
 
 lemma has_integral_dominated_convergence:
   fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  assumes "\<And>k. (f k has_integral y k) s" "h integrable_on s"
-    "\<And>k. \<forall>x\<in>s. norm (f k x) \<le> h x" "\<forall>x\<in>s. (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
+  assumes "\<And>k. (f k has_integral y k) S" "h integrable_on S"
+    "\<And>k. \<forall>x\<in>S. norm (f k x) \<le> h x" "\<forall>x\<in>S. (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
     and x: "y \<longlonglongrightarrow> x"
-  shows "(g has_integral x) s"
+  shows "(g has_integral x) S"
 proof -
-  have int_f: "\<And>k. (f k) integrable_on s"
+  have int_f: "\<And>k. (f k) integrable_on S"
     using assms by (auto simp: integrable_on_def)
-  have "(g has_integral (integral s g)) s"
-    by (intro integrable_integral dominated_convergence[OF int_f assms(2)]) fact+
-  moreover have "integral s g = x"
+  have "(g has_integral (integral S g)) S"
+    by (metis assms(2-4) dominated_convergence(1) has_integral_integral int_f)
+  moreover have "integral S g = x"
   proof (rule LIMSEQ_unique)
-    show "(\<lambda>i. integral s (f i)) \<longlonglongrightarrow> x"
+    show "(\<lambda>i. integral S (f i)) \<longlonglongrightarrow> x"
       using integral_unique[OF assms(1)] x by simp
-    show "(\<lambda>i. integral s (f i)) \<longlonglongrightarrow> integral s g"
-      by (intro dominated_convergence[OF int_f assms(2)]) fact+
+    show "(\<lambda>i. integral S (f i)) \<longlonglongrightarrow> integral S g"
+      by (metis assms(2) assms(3) assms(4) dominated_convergence(2) int_f)
   qed
   ultimately show ?thesis
     by simp
@@ -2720,7 +2737,11 @@
   then have "integral (closure S) f = set_lebesgue_integral lebesgue (closure S) f"
     by (intro set_lebesgue_integral_eq_integral(2)[symmetric])
   also have "\<dots> = 0 \<longleftrightarrow> (AE x in lebesgue. indicator (closure S) x *\<^sub>R f x = 0)"
-    by (rule integral_nonneg_eq_0_iff_AE[OF af]) (use nonneg in \<open>auto simp: indicator_def\<close>)
+    unfolding set_lebesgue_integral_def
+  proof (rule integral_nonneg_eq_0_iff_AE)
+    show "integrable lebesgue (\<lambda>x. indicat_real (closure S) x *\<^sub>R f x)"
+      by (metis af set_integrable_def)
+  qed (use nonneg in \<open>auto simp: indicator_def\<close>)
   also have "\<dots> \<longleftrightarrow> (AE x in lebesgue. x \<in> {x. x \<in> closure S \<longrightarrow> f x = 0})"
     by (auto simp: indicator_def)
   finally have "(AE x in lebesgue. x \<in> {x. x \<in> closure S \<longrightarrow> f x = 0})" by simp
diff -r 9ecc78bcf1ef -r 06bce659d41b src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Fri Apr 13 17:25:02 2018 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy	Fri Apr 13 17:00:57 2018 +0100
@@ -876,9 +876,9 @@
      using of_nat_neq_0[of "2*n"] by (simp only: of_nat_Suc) (simp add: add_ac)
   hence nz': "of_nat n + (1/2::'a) \<noteq> 0" by (simp add: field_simps)
   have "Digamma (of_nat (Suc n) + 1/2 :: 'a) = Digamma (of_nat n + 1/2 + 1)" by simp
-  also from nz' have "\<dots> = Digamma (of_nat n + 1 / 2) + 1 / (of_nat n + 1 / 2)"
+  also from nz' have "\<dots> = Digamma (of_nat n + 1/2) + 1 / (of_nat n + 1/2)"
     by (rule Digamma_plus1)
-  also from nz nz' have "1 / (of_nat n + 1 / 2 :: 'a) = 2 / (2 * of_nat n + 1)"
+  also from nz nz' have "1 / (of_nat n + 1/2 :: 'a) = 2 / (2 * of_nat n + 1)"
     by (subst divide_eq_eq) simp_all
   also note Suc
   finally show ?case by (simp add: add_ac)
@@ -2048,7 +2048,7 @@
   from assms double_in_nonpos_Ints_imp[of z] have z': "2 * z \<notin> \<int>\<^sub>\<le>\<^sub>0" by auto
   from fraction_not_in_ints[of 2 1] have "(1/2 :: 'a) \<notin> \<int>\<^sub>\<le>\<^sub>0"
     by (intro not_in_Ints_imp_not_in_nonpos_Ints) simp_all
-  with lim[of "1/2 :: 'a"] have "?h \<longlonglongrightarrow> 2 * Gamma (1 / 2 :: 'a)" by (simp add: exp_of_real)
+  with lim[of "1/2 :: 'a"] have "?h \<longlonglongrightarrow> 2 * Gamma (1/2 :: 'a)" by (simp add: exp_of_real)
   from LIMSEQ_unique[OF this lim[OF assms]] z' show ?thesis
     by (simp add: divide_simps Gamma_eq_zero_iff ring_distribs exp_diff exp_of_real ac_simps)
 qed
@@ -2735,11 +2735,12 @@
   have "?f absolutely_integrable_on ({0<..x0} \<union> {x0..})"
   proof (rule set_integrable_Un)
     show "?f absolutely_integrable_on {0<..x0}"
+      unfolding set_integrable_def
     proof (rule Bochner_Integration.integrable_bound [OF _ _ AE_I2])
-      show "set_integrable lebesgue {0<..x0} (\<lambda>x. x powr (Re z - 1))" using x0(1) assms
-        by (intro nonnegative_absolutely_integrable_1 integrable_on_powr_from_0') auto
-      show "set_borel_measurable lebesgue {0<..x0}
-              (\<lambda>x. complex_of_real x powr (z - 1) / complex_of_real (exp (a * x)))"
+      show "integrable lebesgue (\<lambda>x. indicat_real {0<..x0} x *\<^sub>R x powr (Re z - 1))"         
+        using x0(1) assms
+        by (intro nonnegative_absolutely_integrable_1 [unfolded set_integrable_def] integrable_on_powr_from_0') auto
+      show "(\<lambda>x. indicat_real {0<..x0} x *\<^sub>R (x powr (z - 1) / exp (a * x))) \<in> borel_measurable lebesgue"
         by (intro measurable_completion)
            (auto intro!: borel_measurable_continuous_on_indicator continuous_intros)
       fix x :: real 
@@ -2751,11 +2752,11 @@
     qed
   next
     show "?f absolutely_integrable_on {x0..}"
+      unfolding set_integrable_def
     proof (rule Bochner_Integration.integrable_bound [OF _ _ AE_I2])
-      show "set_integrable lebesgue {x0..} (\<lambda>x. exp (-(a/2) * x))" using assms
-        by (intro nonnegative_absolutely_integrable_1 integrable_on_exp_minus_to_infinity) auto
-      show "set_borel_measurable lebesgue {x0..}
-              (\<lambda>x. complex_of_real x powr (z - 1) / complex_of_real (exp (a * x)))" using x0(1)
+      show "integrable lebesgue (\<lambda>x. indicat_real {x0..} x *\<^sub>R exp (- (a / 2) * x))" using assms
+        by (intro nonnegative_absolutely_integrable_1 [unfolded set_integrable_def] integrable_on_exp_minus_to_infinity) auto
+      show "(\<lambda>x. indicat_real {x0..} x *\<^sub>R (x powr (z - 1) / exp (a * x))) \<in> borel_measurable lebesgue" using x0(1)
         by (intro measurable_completion)
            (auto intro!: borel_measurable_continuous_on_indicator continuous_intros)
       fix x :: real 
@@ -3015,14 +3016,15 @@
   qed (insert that, auto simp: max.coboundedI1 max.coboundedI2 powr_mono2' powr_mono2 D_def)
   have [simp]: "C \<ge> 0" "D \<ge> 0" by (simp_all add: C_def D_def)
 
-  have I1: "set_integrable lborel {0..1 / 2} (\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1))"
+  have I1: "set_integrable lborel {0..1/2} (\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1))"
+    unfolding set_integrable_def
   proof (rule Bochner_Integration.integrable_bound[OF _ _ AE_I2])
-    have "(\<lambda>t. t powr (a - 1)) integrable_on {0..1 / 2}"
+    have "(\<lambda>t. t powr (a - 1)) integrable_on {0..1/2}"
       by (rule integrable_on_powr_from_0) (use assms in auto)
-    hence "(\<lambda>t. t powr (a - 1)) absolutely_integrable_on {0..1 / 2}"
+    hence "(\<lambda>t. t powr (a - 1)) absolutely_integrable_on {0..1/2}"
       by (subst absolutely_integrable_on_iff_nonneg) auto
-    from integrable_mult_right[OF this, of C]
-      show "set_integrable lborel {0..1 / 2} (\<lambda>t. C * t powr (a - 1))"
+    from integrable_mult_right[OF this [unfolded set_integrable_def], of C]
+    show "integrable lborel (\<lambda>x. indicat_real {0..1/2} x *\<^sub>R (C * x powr (a - 1)))"
       by (subst (asm) integrable_completion) (auto simp: mult_ac)
   next
     fix x :: real
@@ -3033,7 +3035,8 @@
       by (auto simp: indicator_def abs_mult mult_ac)
   qed (auto intro!: AE_I2 simp: indicator_def)
 
-  have I2: "set_integrable lborel {1 / 2..1} (\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1))"
+  have I2: "set_integrable lborel {1/2..1} (\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1))"
+    unfolding set_integrable_def
   proof (rule Bochner_Integration.integrable_bound[OF _ _ AE_I2])
     have "(\<lambda>t. t powr (b - 1)) integrable_on {0..1/2}"
       by (rule integrable_on_powr_from_0) (use assms in auto)
@@ -3042,8 +3045,8 @@
       have "(\<lambda>t. (1 - t) powr (b - 1)) integrable_on {1/2..1}" by simp
     hence "(\<lambda>t. (1 - t) powr (b - 1)) absolutely_integrable_on {1/2..1}"
       by (subst absolutely_integrable_on_iff_nonneg) auto
-    from integrable_mult_right[OF this, of D]
-      show "set_integrable lborel {1 / 2..1} (\<lambda>t. D * (1 - t) powr (b - 1))"
+    from integrable_mult_right[OF this [unfolded set_integrable_def], of D]
+    show "integrable lborel (\<lambda>x. indicat_real {1/2..1} x *\<^sub>R (D * (1 - x) powr (b - 1)))"
       by (subst (asm) integrable_completion) (auto simp: mult_ac)
   next
     fix x :: real
@@ -3204,9 +3207,9 @@
 proof -
   from tendsto_inverse[OF tendsto_mult[OF
          sin_product_formula_real[of "1/2"] tendsto_const[of "2/pi"]]]
-    have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1 / 2)\<^sup>2 / (real k)\<^sup>2))) \<longlonglongrightarrow> pi/2"
+    have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1/2)\<^sup>2 / (real k)\<^sup>2))) \<longlonglongrightarrow> pi/2"
     by (simp add: prod_inversef [symmetric])
-  also have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1 / 2)\<^sup>2 / (real k)\<^sup>2))) =
+  also have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1/2)\<^sup>2 / (real k)\<^sup>2))) =
                (\<lambda>n. (\<Prod>k=1..n. (4*real k^2)/(4*real k^2 - 1)))"
     by (intro ext prod.cong refl) (simp add: divide_simps)
   finally show ?thesis .
diff -r 9ecc78bcf1ef -r 06bce659d41b src/HOL/Analysis/Infinite_Set_Sum.thy
--- a/src/HOL/Analysis/Infinite_Set_Sum.thy	Fri Apr 13 17:25:02 2018 +0200
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy	Fri Apr 13 17:00:57 2018 +0100
@@ -142,8 +142,6 @@
 \<close>
 
 
-
-
 lemma restrict_count_space_subset:
   "A \<subseteq> B \<Longrightarrow> restrict_space (count_space B) A = count_space A"
   by (subst restrict_count_space) (simp_all add: Int_absorb2)
@@ -156,17 +154,19 @@
   have "count_space A = restrict_space (count_space B) A"
     by (rule restrict_count_space_subset [symmetric]) fact+
   also have "integrable \<dots> f \<longleftrightarrow> set_integrable (count_space B) A f"
-    by (subst integrable_restrict_space) auto
+    by (simp add: integrable_restrict_space set_integrable_def)
   finally show ?thesis 
-    unfolding abs_summable_on_def .
+    unfolding abs_summable_on_def set_integrable_def .
 qed
 
 lemma abs_summable_on_altdef: "f abs_summable_on A \<longleftrightarrow> set_integrable (count_space UNIV) A f"
-  by (subst abs_summable_on_restrict[of _ UNIV]) (auto simp: abs_summable_on_def)
+  unfolding abs_summable_on_def set_integrable_def
+  by (metis (no_types) inf_top.right_neutral integrable_restrict_space restrict_count_space sets_UNIV)
 
 lemma abs_summable_on_altdef': 
   "A \<subseteq> B \<Longrightarrow> f abs_summable_on A \<longleftrightarrow> set_integrable (count_space B) A f"
-  by (subst abs_summable_on_restrict[of _ B]) (auto simp: abs_summable_on_def)
+  unfolding abs_summable_on_def set_integrable_def
+  by (metis (no_types) Pow_iff abs_summable_on_def inf.orderE integrable_restrict_space restrict_count_space_subset set_integrable_def sets_count_space space_count_space)
 
 lemma abs_summable_on_norm_iff [simp]: 
   "(\<lambda>x. norm (f x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on A"
@@ -205,7 +205,7 @@
   assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x = 0"
   assumes "\<And>x. x \<in> A \<inter> B \<Longrightarrow> f x = g x"
   shows   "f abs_summable_on A \<longleftrightarrow> g abs_summable_on B"
-  unfolding abs_summable_on_altdef using assms
+  unfolding abs_summable_on_altdef set_integrable_def using assms
   by (intro Bochner_Integration.integrable_cong refl)
      (auto simp: indicator_def split: if_splits)
 
@@ -418,11 +418,13 @@
 
 lemma infsetsum_altdef:
   "infsetsum f A = set_lebesgue_integral (count_space UNIV) A f"
+  unfolding set_lebesgue_integral_def
   by (subst integral_restrict_space [symmetric])
      (auto simp: restrict_count_space_subset infsetsum_def)
 
 lemma infsetsum_altdef':
   "A \<subseteq> B \<Longrightarrow> infsetsum f A = set_lebesgue_integral (count_space B) A f"
+  unfolding set_lebesgue_integral_def
   by (subst integral_restrict_space [symmetric])
      (auto simp: restrict_count_space_subset infsetsum_def)
 
@@ -477,7 +479,8 @@
   shows   "infsetsum f A = (\<Sum>n. if n \<in> A then f n else 0)"
 proof -
   from assms have "infsetsum f A = (\<Sum>n. indicator A n *\<^sub>R f n)"
-    unfolding infsetsum_altdef abs_summable_on_altdef by (subst integral_count_space_nat) auto
+    unfolding infsetsum_altdef abs_summable_on_altdef set_lebesgue_integral_def set_integrable_def
+ by (subst integral_count_space_nat) auto
   also have "(\<lambda>n. indicator A n *\<^sub>R f n) = (\<lambda>n. if n \<in> A then f n else 0)"
     by auto
   finally show ?thesis .
@@ -560,7 +563,7 @@
   assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x = 0"
   assumes "\<And>x. x \<in> A \<inter> B \<Longrightarrow> f x = g x"
   shows   "infsetsum f A = infsetsum g B"
-  unfolding infsetsum_altdef using assms
+  unfolding infsetsum_altdef set_lebesgue_integral_def using assms
   by (intro Bochner_Integration.integral_cong refl)
      (auto simp: indicator_def split: if_splits)
 
@@ -571,7 +574,7 @@
   assumes "\<And>x. x \<in> A - B \<Longrightarrow> f x \<le> 0"
   assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x \<ge> 0"
   shows   "infsetsum f A \<le> infsetsum g B"
-  using assms unfolding infsetsum_altdef abs_summable_on_altdef
+  using assms unfolding infsetsum_altdef set_lebesgue_integral_def abs_summable_on_altdef set_integrable_def
   by (intro Bochner_Integration.integral_mono) (auto simp: indicator_def)
 
 lemma infsetsum_mono_neutral_left:
@@ -617,7 +620,8 @@
     by (intro pair_sigma_finite.intro sigma_finite_measure_count_space_countable) fact+
 
   have "integrable (count_space (A \<times> B')) (\<lambda>z. indicator (Sigma A B) z *\<^sub>R f z)"
-    using summable by (subst abs_summable_on_altdef' [symmetric]) (auto simp: B'_def)
+    using summable
+    by (metis (mono_tags, lifting) abs_summable_on_altdef abs_summable_on_def integrable_cong integrable_mult_indicator set_integrable_def sets_UNIV)
   also have "?this \<longleftrightarrow> integrable (count_space A \<Otimes>\<^sub>M count_space B') (\<lambda>(x, y). indicator (B x) y *\<^sub>R f (x, y))"
     by (intro Bochner_Integration.integrable_cong)
        (auto simp: pair_measure_countable indicator_def split: if_splits)
@@ -627,14 +631,20 @@
           (\<integral>x. infsetsum (\<lambda>y. f (x, y)) (B x) \<partial>count_space A)"
     unfolding infsetsum_def by simp
   also have "\<dots> = (\<integral>x. \<integral>y. indicator (B x) y *\<^sub>R f (x, y) \<partial>count_space B' \<partial>count_space A)"
-    by (intro Bochner_Integration.integral_cong infsetsum_altdef'[of _ B'] refl)
-       (auto simp: B'_def)
+  proof (rule Bochner_Integration.integral_cong [OF refl])
+    show "\<And>x. x \<in> space (count_space A) \<Longrightarrow>
+         (\<Sum>\<^sub>ay\<in>B x. f (x, y)) = LINT y|count_space B'. indicat_real (B x) y *\<^sub>R f (x, y)"
+      using infsetsum_altdef'[of _ B'] 
+      unfolding set_lebesgue_integral_def B'_def
+      by auto 
+  qed
   also have "\<dots> = (\<integral>(x,y). indicator (B x) y *\<^sub>R f (x, y) \<partial>(count_space A \<Otimes>\<^sub>M count_space B'))"
     by (subst integral_fst [OF integrable]) auto
   also have "\<dots> = (\<integral>z. indicator (Sigma A B) z *\<^sub>R f z \<partial>count_space (A \<times> B'))"
     by (intro Bochner_Integration.integral_cong)
        (auto simp: pair_measure_countable indicator_def split: if_splits)
   also have "\<dots> = infsetsum f (Sigma A B)"
+    unfolding set_lebesgue_integral_def [symmetric]
     by (rule infsetsum_altdef' [symmetric]) (auto simp: B'_def)
   finally show ?thesis ..
 qed
@@ -693,7 +703,6 @@
     unfolding B'_def using assms by auto
   interpret pair_sigma_finite "count_space A" "count_space B'"
     by (intro pair_sigma_finite.intro sigma_finite_measure_count_space_countable) fact+
-
   {
     assume *: "f abs_summable_on Sigma A B"
     thus "(\<lambda>y. f (x, y)) abs_summable_on B x" if "x \<in> A" for x
@@ -707,18 +716,18 @@
     finally have "integrable (count_space A) 
                     (\<lambda>x. lebesgue_integral (count_space B') 
                       (\<lambda>y. indicator (Sigma A B) (x, y) *\<^sub>R norm (f (x, y))))"
-      by (rule integrable_fst')
+      unfolding set_integrable_def by (rule integrable_fst')
     also have "?this \<longleftrightarrow> integrable (count_space A)
                     (\<lambda>x. lebesgue_integral (count_space B') 
                       (\<lambda>y. indicator (B x) y *\<^sub>R norm (f (x, y))))"
       by (intro integrable_cong refl) (simp_all add: indicator_def)
     also have "\<dots> \<longleftrightarrow> integrable (count_space A) (\<lambda>x. infsetsum (\<lambda>y. norm (f (x, y))) (B x))"
+      unfolding set_lebesgue_integral_def [symmetric]
       by (intro integrable_cong refl infsetsum_altdef' [symmetric]) (auto simp: B'_def)
     also have "\<dots> \<longleftrightarrow> (\<lambda>x. infsetsum (\<lambda>y. norm (f (x, y))) (B x)) abs_summable_on A"
       by (simp add: abs_summable_on_def)
     finally show \<dots> .
   }
-
   {
     assume *: "\<forall>x\<in>A. (\<lambda>y. f (x, y)) abs_summable_on B x"
     assume "(\<lambda>x. \<Sum>\<^sub>ay\<in>B x. norm (f (x, y))) abs_summable_on A"
@@ -726,6 +735,7 @@
       by (intro abs_summable_on_cong refl infsetsum_altdef') (auto simp: B'_def)
     also have "\<dots> \<longleftrightarrow> (\<lambda>x. \<integral>y. indicator (Sigma A B) (x, y) *\<^sub>R norm (f (x, y)) \<partial>count_space B')
                         abs_summable_on A" (is "_ \<longleftrightarrow> ?h abs_summable_on _")
+      unfolding set_lebesgue_integral_def
       by (intro abs_summable_on_cong) (auto simp: indicator_def)
     also have "\<dots> \<longleftrightarrow> integrable (count_space A) ?h"
       by (simp add: abs_summable_on_def)
@@ -740,7 +750,8 @@
           by blast
         also have "?this \<longleftrightarrow> integrable (count_space B') 
                       (\<lambda>y. indicator (B x) y *\<^sub>R f (x, y))"
-          using x by (intro abs_summable_on_altdef') (auto simp: B'_def)
+          unfolding set_integrable_def [symmetric]
+         using x by (intro abs_summable_on_altdef') (auto simp: B'_def)
         also have "(\<lambda>y. indicator (B x) y *\<^sub>R f (x, y)) = 
                      (\<lambda>y. indicator (Sigma A B) (x, y) *\<^sub>R f (x, y))"
           using x by (auto simp: indicator_def)
@@ -749,12 +760,13 @@
       }
       thus ?case by (auto simp: AE_count_space)
     qed (insert **, auto simp: pair_measure_countable)
-    also have "count_space A \<Otimes>\<^sub>M count_space B' = count_space (A \<times> B')"
+    moreover have "count_space A \<Otimes>\<^sub>M count_space B' = count_space (A \<times> B')"
       by (simp add: pair_measure_countable)
-    also have "set_integrable (count_space (A \<times> B')) (Sigma A B) f \<longleftrightarrow>
+    moreover have "set_integrable (count_space (A \<times> B')) (Sigma A B) f \<longleftrightarrow>
                  f abs_summable_on Sigma A B"
       by (rule abs_summable_on_altdef' [symmetric]) (auto simp: B'_def)
-    finally show \<dots> .
+    ultimately show "f abs_summable_on Sigma A B"
+      by (simp add: set_integrable_def)
   }
 qed
 
diff -r 9ecc78bcf1ef -r 06bce659d41b src/HOL/Analysis/Interval_Integral.thy
--- a/src/HOL/Analysis/Interval_Integral.thy	Fri Apr 13 17:25:02 2018 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy	Fri Apr 13 17:00:57 2018 +0100
@@ -51,9 +51,7 @@
 lemma borel_einterval[measurable]: "einterval a b \<in> sets borel"
   unfolding einterval_def by measurable
 
-(*
-    Approximating a (possibly infinite) interval
-*)
+subsection\<open>Approximating a (possibly infinite) interval\<close>
 
 lemma filterlim_sup1: "(LIM x F. f x :> G1) \<Longrightarrow> (LIM x F. f x :> (sup G1 G2))"
  unfolding filterlim_def by (auto intro: le_supI1)
@@ -175,9 +173,7 @@
 translations
   "LBINT x=a..b. f" == "CONST interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"
 
-(*
-    Basic properties of integration over an interval.
-*)
+subsection\<open>Basic properties of integration over an interval\<close>
 
 lemma interval_lebesgue_integral_cong:
   "a \<le> b \<Longrightarrow> (\<And>x. x \<in> einterval a b \<Longrightarrow> f x = g x) \<Longrightarrow> einterval a b \<in> sets M \<Longrightarrow>
@@ -200,7 +196,7 @@
   show ?thesis
     unfolding interval_lebesgue_integrable_def
     using lborel_integrable_real_affine_iff[symmetric, of "-1" "\<lambda>x. indicator (einterval _ _) x *\<^sub>R f x" 0]
-    by (simp add: *)
+    by (simp add: * set_integrable_def)
 qed
 
 lemma interval_lebesgue_integral_add [intro, simp]:
@@ -260,7 +256,7 @@
 
 lemma interval_lebesgue_integral_uminus:
   "interval_lebesgue_integral M a b (\<lambda>x. - f x) = - interval_lebesgue_integral M a b f"
-  by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def)
+  by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def)
 
 lemma interval_lebesgue_integral_of_real:
   "interval_lebesgue_integral M a b (\<lambda>x. complex_of_real (f x)) =
@@ -287,10 +283,10 @@
 using assms by (auto simp add: interval_lebesgue_integral_def less_imp_le einterval_def)
 
 lemma interval_integral_endpoints_same [simp]: "(LBINT x=a..a. f x) = 0"
-  by (simp add: interval_lebesgue_integral_def einterval_same)
+  by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_def einterval_same)
 
 lemma interval_integral_endpoints_reverse: "(LBINT x=a..b. f x) = -(LBINT x=b..a. f x)"
-  by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integral_def einterval_same)
+  by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integral_def set_lebesgue_integral_def einterval_same)
 
 lemma interval_integrable_endpoints_reverse:
   "interval_lebesgue_integrable lborel a b f \<longleftrightarrow>
@@ -304,15 +300,16 @@
     by (auto simp add: interval_lebesgue_integral_def interval_integrable_endpoints_reverse
              split: if_split_asm)
 next
-  case (le a b) then show ?case
-    unfolding interval_lebesgue_integral_def
-    by (subst set_integral_reflect)
-       (auto simp: interval_lebesgue_integrable_def einterval_iff
-                   ereal_uminus_le_reorder ereal_uminus_less_reorder not_less
-                   uminus_ereal.simps[symmetric]
+  case (le a b) 
+  have "LBINT x:{x. - x \<in> einterval a b}. f (- x) = LBINT x:einterval (- b) (- a). f (- x)"
+    unfolding interval_lebesgue_integrable_def set_lebesgue_integral_def
+    apply (rule Bochner_Integration.integral_cong [OF refl])
+    by (auto simp: einterval_iff ereal_uminus_le_reorder ereal_uminus_less_reorder not_less uminus_ereal.simps[symmetric]
              simp del: uminus_ereal.simps
-             intro!: Bochner_Integration.integral_cong
              split: split_indicator)
+  then show ?case
+    unfolding interval_lebesgue_integral_def 
+    by (subst set_integral_reflect) (simp add: le)
 qed
 
 lemma interval_lebesgue_integral_0_infty:
@@ -328,21 +325,19 @@
   (set_integrable M {a<..} f)"
   unfolding interval_lebesgue_integrable_def by auto
 
-(*
-    Basic properties of integration over an interval wrt lebesgue measure.
-*)
+subsection\<open>Basic properties of integration over an interval wrt lebesgue measure\<close>
 
 lemma interval_integral_zero [simp]:
   fixes a b :: ereal
   shows"LBINT x=a..b. 0 = 0"
-unfolding interval_lebesgue_integral_def einterval_eq
+unfolding interval_lebesgue_integral_def set_lebesgue_integral_def einterval_eq
 by simp
 
 lemma interval_integral_const [intro, simp]:
   fixes a b c :: real
   shows "interval_lebesgue_integrable lborel a b (\<lambda>x. c)" and "LBINT x=a..b. c = c * (b - a)"
-unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq
-by (auto simp add:  less_imp_le field_simps measure_def)
+  unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq
+  by (auto simp add: less_imp_le field_simps measure_def set_integrable_def set_lebesgue_integral_def)
 
 lemma interval_integral_cong_AE:
   assumes [measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel"
@@ -429,7 +424,7 @@
   and anti_eq: "\<And>x. b \<le> a \<Longrightarrow> b < x \<Longrightarrow> x < a \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
   assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
   shows "interval_lebesgue_integral M a b f = interval_lebesgue_integral M a b g"
-  unfolding interval_lebesgue_integral_def
+  unfolding interval_lebesgue_integral_def set_lebesgue_integral_def
   apply (intro if_cong refl arg_cong[where f="\<lambda>x. - x"] integral_discrete_difference[of X] assms)
   apply (auto simp: eq anti_eq einterval_iff split: split_indicator)
   done
@@ -444,13 +439,17 @@
     then have ord: "a \<le> b" "b \<le> c" "a \<le> c" and f': "set_integrable lborel (einterval a c) f"
       by (auto simp: interval_lebesgue_integrable_def)
     then have f: "set_borel_measurable borel (einterval a c) f"
+      unfolding set_integrable_def set_borel_measurable_def
       by (drule_tac borel_measurable_integrable) simp
     have "(LBINT x:einterval a c. f x) = (LBINT x:einterval a b \<union> einterval b c. f x)"
     proof (rule set_integral_cong_set)
       show "AE x in lborel. (x \<in> einterval a b \<union> einterval b c) = (x \<in> einterval a c)"
         using AE_lborel_singleton[of "real_of_ereal b"] ord
         by (cases a b c rule: ereal3_cases) (auto simp: einterval_iff)
-    qed (insert ord, auto intro!: set_borel_measurable_subset[OF f] simp: einterval_iff)
+      show "set_borel_measurable lborel (einterval a c) f" "set_borel_measurable lborel (einterval a b \<union> einterval b c) f"
+        unfolding set_borel_measurable_def
+        using ord by (auto simp: einterval_iff intro!: set_borel_measurable_subset[OF f, unfolded set_borel_measurable_def])
+    qed
     also have "\<dots> = (LBINT x:einterval a b. f x) + (LBINT x:einterval b c. f x)"
       using ord
       by (intro set_integral_Un_AE) (auto intro!: set_integrable_subset[OF f'] simp: einterval_iff not_less)
@@ -475,9 +474,10 @@
     interval_lebesgue_integrable lborel a b f"
 proof (induct a b rule: linorder_wlog)
   case (le a b) then show ?case
+    unfolding interval_lebesgue_integrable_def set_integrable_def
     by (auto simp: interval_lebesgue_integrable_def
-             intro!: set_integrable_subset[OF borel_integrable_compact[of "{a .. b}"]]
-                     continuous_at_imp_continuous_on)
+        intro!: set_integrable_subset[unfolded set_integrable_def, OF borel_integrable_compact[of "{a .. b}"]]
+        continuous_at_imp_continuous_on)
 qed (auto intro: interval_integrable_endpoints_reverse[THEN iffD1])
 
 lemma interval_integrable_continuous_on:
@@ -497,9 +497,8 @@
   shows "a \<le> b \<Longrightarrow> set_integrable lborel (einterval a b) f \<Longrightarrow> LBINT x=a..b. f x = integral (einterval a b) f"
   by (subst interval_lebesgue_integral_le_eq, simp) (rule set_borel_integral_eq_integral)
 
-(*
-    General limit approximation arguments
-*)
+
+subsection\<open>General limit approximation arguments\<close>
 
 lemma interval_integral_Icc_approx_nonneg:
   fixes a b :: ereal
@@ -517,7 +516,7 @@
     "set_integrable lborel (einterval a b) f"
     "(LBINT x=a..b. f x) = C"
 proof -
-  have 1: "\<And>i. set_integrable lborel {l i..u i} f" by (rule f_integrable)
+  have 1 [unfolded set_integrable_def]: "\<And>i. set_integrable lborel {l i..u i} f" by (rule f_integrable)
   have 2: "AE x in lborel. mono (\<lambda>n. indicator {l n..u n} x *\<^sub>R f x)"
   proof -
      from f_nonneg have "AE x in lborel. \<forall>i. l i \<le> x \<longrightarrow> x \<le> u i \<longrightarrow> 0 \<le> f x"
@@ -544,14 +543,16 @@
       unfolding approx(1) by (auto intro!: AE_I2 Lim_eventually split: split_indicator)
   qed
   have 4: "(\<lambda>i. \<integral> x. indicator {l i..u i} x *\<^sub>R f x \<partial>lborel) \<longlonglongrightarrow> C"
-    using lbint_lim by (simp add: interval_integral_Icc approx less_imp_le)
-  have 5: "set_borel_measurable lborel (einterval a b) f" by (rule assms)
+    using lbint_lim by (simp add: interval_integral_Icc [unfolded set_lebesgue_integral_def] approx less_imp_le)
+  have 5: "(\<lambda>x. indicat_real (einterval a b) x *\<^sub>R f x) \<in> borel_measurable lborel"
+    using f_measurable set_borel_measurable_def by blast
   have "(LBINT x=a..b. f x) = lebesgue_integral lborel (\<lambda>x. indicator (einterval a b) x *\<^sub>R f x)"
-    using assms by (simp add: interval_lebesgue_integral_def less_imp_le)
-  also have "... = C" by (rule integral_monotone_convergence [OF 1 2 3 4 5])
+    using assms by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_def less_imp_le)
+  also have "... = C"
+    by (rule integral_monotone_convergence [OF 1 2 3 4 5])
   finally show "(LBINT x=a..b. f x) = C" .
-
   show "set_integrable lborel (einterval a b) f"
+    unfolding set_integrable_def
     by (rule integrable_monotone_convergence[OF 1 2 3 4 5])
 qed
 
@@ -566,13 +567,14 @@
   shows "(\<lambda>i. LBINT x=l i.. u i. f x) \<longlonglongrightarrow> (LBINT x=a..b. f x)"
 proof -
   have "(\<lambda>i. LBINT x:{l i.. u i}. f x) \<longlonglongrightarrow> (LBINT x:einterval a b. f x)"
+    unfolding set_lebesgue_integral_def
   proof (rule integral_dominated_convergence)
     show "integrable lborel (\<lambda>x. norm (indicator (einterval a b) x *\<^sub>R f x))"
-      by (rule integrable_norm) fact
-    show "set_borel_measurable lborel (einterval a b) f"
-      using f_integrable by (rule borel_measurable_integrable)
-    then show "\<And>i. set_borel_measurable lborel {l i..u i} f"
-      by (rule set_borel_measurable_subset) (auto simp: approx)
+      using f_integrable integrable_norm set_integrable_def by blast
+    show "(\<lambda>x. indicat_real (einterval a b) x *\<^sub>R f x) \<in> borel_measurable lborel"
+      using f_integrable by (simp add: set_integrable_def)
+    then show "\<And>i. (\<lambda>x. indicat_real {l i..u i} x *\<^sub>R f x) \<in> borel_measurable lborel"
+      by (rule set_borel_measurable_subset [unfolded set_borel_measurable_def]) (auto simp: approx)
     show "\<And>i. AE x in lborel. norm (indicator {l i..u i} x *\<^sub>R f x) \<le> norm (indicator (einterval a b) x *\<^sub>R f x)"
       by (intro AE_I2) (auto simp: approx split: split_indicator)
     show "AE x in lborel. (\<lambda>i. indicator {l i..u i} x *\<^sub>R f x) \<longlonglongrightarrow> indicator (einterval a b) x *\<^sub>R f x"
@@ -591,10 +593,12 @@
     by (simp add: interval_lebesgue_integral_le_eq[symmetric] interval_integral_Icc less_imp_le)
 qed
 
+subsection\<open>A slightly stronger Fundamental Theorem of Calculus\<close>
+
+text\<open>Three versions: first, for finite intervals, and then two versions for
+    arbitrary intervals.\<close>
+
 (*
-  A slightly stronger version of integral_FTC_atLeastAtMost and related facts,
-  with continuous_on instead of isCont
-
   TODO: make the older versions corollaries of these (using continuous_at_imp_continuous_on, etc.)
 *)
 
@@ -606,28 +610,43 @@
 where x and y are real. These should be better automated.
 *)
 
-(*
-    The first Fundamental Theorem of Calculus
-
-    First, for finite intervals, and then two versions for arbitrary intervals.
-*)
-
 lemma interval_integral_FTC_finite:
   fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: real
   assumes f: "continuous_on {min a b..max a b} f"
   assumes F: "\<And>x. min a b \<le> x \<Longrightarrow> x \<le> max a b \<Longrightarrow> (F has_vector_derivative (f x)) (at x within
     {min a b..max a b})"
   shows "(LBINT x=a..b. f x) = F b - F a"
-  apply (case_tac "a \<le> b")
-  apply (subst interval_integral_Icc, simp)
-  apply (rule integral_FTC_atLeastAtMost, assumption)
-  apply (metis F max_def min_def)
-  using f apply (simp add: min_absorb1 max_absorb2)
-  apply (subst interval_integral_endpoints_reverse)
-  apply (subst interval_integral_Icc, simp)
-  apply (subst integral_FTC_atLeastAtMost, auto)
-  apply (metis F max_def min_def)
-using f by (simp add: min_absorb2 max_absorb1)
+proof (cases "a \<le> b")
+  case True
+  have "(LBINT x=a..b. f x) = (LBINT x. indicat_real {a..b} x *\<^sub>R f x)"
+    by (simp add: True interval_integral_Icc set_lebesgue_integral_def)
+  also have "... = F b - F a"
+  proof (rule integral_FTC_atLeastAtMost [OF True])
+    show "continuous_on {a..b} f"
+      using True f by linarith
+    show "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (F has_vector_derivative f x) (at x within {a..b})"
+      by (metis F True max.commute max_absorb1 min_def)
+  qed
+  finally show ?thesis .
+next
+  case False
+  then have "b \<le> a"
+    by simp
+  have "- interval_lebesgue_integral lborel (ereal b) (ereal a) f = - (LBINT x. indicat_real {b..a} x *\<^sub>R f x)"
+    by (simp add: \<open>b \<le> a\<close> interval_integral_Icc set_lebesgue_integral_def)
+  also have "... = F b - F a"
+  proof (subst integral_FTC_atLeastAtMost [OF \<open>b \<le> a\<close>])
+    show "continuous_on {b..a} f"
+      using False f by linarith
+    show "\<And>x. \<lbrakk>b \<le> x; x \<le> a\<rbrakk>
+         \<Longrightarrow> (F has_vector_derivative f x) (at x within {b..a})"
+      by (metis F False max_def min_def)
+  qed auto
+  finally show ?thesis
+    by (metis interval_integral_endpoints_reverse)
+qed
+
+
 
 lemma interval_integral_FTC_nonneg:
   fixes f F :: "real \<Rightarrow> real" and a b :: ereal
@@ -655,11 +674,12 @@
   have 1: "\<And>i. set_integrable lborel {l i..u i} f"
   proof -
     fix i show "set_integrable lborel {l i .. u i} f"
-      using \<open>a < l i\<close> \<open>u i < b\<close>
+      using \<open>a < l i\<close> \<open>u i < b\<close> unfolding set_integrable_def
       by (intro borel_integrable_compact f continuous_at_imp_continuous_on compact_Icc ballI)
          (auto simp del: ereal_less_eq simp add: ereal_less_eq(3)[symmetric])
   qed
   have 2: "set_borel_measurable lborel (einterval a b) f"
+    unfolding set_borel_measurable_def
     by (auto simp del: real_scaleR_def intro!: borel_measurable_continuous_on_indicator
              simp: continuous_on_eq_continuous_at einterval_iff f)
   have 3: "(\<lambda>i. LBINT x=l i..u i. f x) \<longlonglongrightarrow> B - A"
@@ -779,12 +799,10 @@
   qed
 qed
 
-(*
-    The substitution theorem
+subsection\<open>The substitution theorem\<close>
 
-    Once again, three versions: first, for finite intervals, and then two versions for
-    arbitrary intervals.
-*)
+text\<open>Once again, three versions: first, for finite intervals, and then two versions for
+    arbitrary intervals.\<close>
 
 lemma interval_integral_substitution_finite:
   fixes a b :: real and f :: "real \<Rightarrow> 'a::euclidean_space"
@@ -824,6 +842,7 @@
     by (blast intro: continuous_on_compose2 contf contg)
   have "LBINT x=a..b. g' x *\<^sub>R f (g x) = F (g b) - F (g a)"
     apply (subst interval_integral_Icc, simp add: assms)
+    unfolding set_lebesgue_integral_def
     apply (rule integral_FTC_atLeastAtMost[of a b "\<lambda>x. F (g x)", OF \<open>a \<le> b\<close>])
     apply (rule vector_diff_chain_within[OF v_derivg derivF, unfolded comp_def])
     apply (auto intro!: continuous_on_scaleR contg' contfg)
@@ -1093,7 +1112,7 @@
   shows "interval_lebesgue_integrable lborel a b f \<Longrightarrow> a \<le> b \<Longrightarrow>
     norm (LBINT t=a..b. f t) \<le> LBINT t=a..b. norm (f t)"
   using integral_norm_bound[of lborel "\<lambda>x. indicator (einterval a b) x *\<^sub>R f x"]
-  by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def)
+  by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def)
 
 lemma interval_integral_norm2:
   "interval_lebesgue_integrable lborel a b f \<Longrightarrow>
@@ -1105,7 +1124,7 @@
   case (le a b)
   then have "\<bar>LBINT t=a..b. norm (f t)\<bar> = LBINT t=a..b. norm (f t)"
     using integrable_norm[of lborel "\<lambda>x. indicator (einterval a b) x *\<^sub>R f x"]
-    by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def
+    by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def
              intro!: integral_nonneg_AE abs_of_nonneg)
   then show ?case
     using le by (simp add: interval_integral_norm)
diff -r 9ecc78bcf1ef -r 06bce659d41b src/HOL/Analysis/Lebesgue_Integral_Substitution.thy
--- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Fri Apr 13 17:25:02 2018 +0200
+++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Fri Apr 13 17:00:57 2018 +0100
@@ -74,10 +74,12 @@
                       (g has_vector_derivative g' x) (at x within {min u' v'..max u' v'})"
             by (simp only: u'v' max_absorb2 min_absorb1)
                (auto simp: has_field_derivative_iff_has_vector_derivative)
-        have "integrable lborel (\<lambda>x. indicator ({a..b} \<inter> g -` {u..v}) x *\<^sub>R g' x)"
-          by (rule set_integrable_subset[OF borel_integrable_atLeastAtMost'[OF contg']]) simp_all
+          have "integrable lborel (\<lambda>x. indicator ({a..b} \<inter> g -` {u..v}) x *\<^sub>R g' x)"
+            using set_integrable_subset borel_integrable_atLeastAtMost'[OF contg']
+            by (metis \<open>{u'..v'} \<subseteq> {a..b}\<close> eucl_ivals(5) set_integrable_def sets_lborel u'v'(1))
         hence "(\<integral>\<^sup>+x. ennreal (g' x) * indicator ({a..b} \<inter> g-` {u..v}) x \<partial>lborel) =
                    LBINT x:{a..b} \<inter> g-`{u..v}. g' x"
+          unfolding set_lebesgue_integral_def
           by (subst nn_integral_eq_integral[symmetric])
              (auto intro!: derivg_nonneg nn_integral_cong split: split_indicator)
         also from interval_integral_FTC_finite[OF A B]
@@ -129,28 +131,29 @@
       also have "... = \<integral>\<^sup>+ x. indicator (g-`A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x) \<partial>lborel" (is "_ = ?I")
         by (subst compl.IH, intro nn_integral_cong) (simp split: split_indicator)
       also have "g b - g a = LBINT x:{a..b}. g' x" using derivg'
+        unfolding set_lebesgue_integral_def
         by (intro integral_FTC_atLeastAtMost[symmetric])
            (auto intro: continuous_on_subset[OF contg'] has_field_derivative_subset[OF derivg]
                  has_vector_derivative_at_within)
       also have "ennreal ... = \<integral>\<^sup>+ x. g' x * indicator {a..b} x \<partial>lborel"
-        using borel_integrable_atLeastAtMost'[OF contg']
+        using borel_integrable_atLeastAtMost'[OF contg'] unfolding set_lebesgue_integral_def
         by (subst nn_integral_eq_integral)
-           (simp_all add: mult.commute derivg_nonneg split: split_indicator)
+           (simp_all add: mult.commute derivg_nonneg set_integrable_def split: split_indicator)
       also have Mg'': "(\<lambda>x. indicator (g -` A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x))
                             \<in> borel_measurable borel" using Mg'
         by (intro borel_measurable_times_ennreal borel_measurable_indicator)
-           (simp_all add: mult.commute)
+           (simp_all add: mult.commute set_borel_measurable_def)
       have le: "(\<integral>\<^sup>+x. indicator (g-`A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x) \<partial>lborel) \<le>
                         (\<integral>\<^sup>+x. ennreal (g' x) * indicator {a..b} x \<partial>lborel)"
          by (intro nn_integral_mono) (simp split: split_indicator add: derivg_nonneg)
       note integrable = borel_integrable_atLeastAtMost'[OF contg']
       with le have notinf: "(\<integral>\<^sup>+x. indicator (g-`A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x) \<partial>lborel) \<noteq> top"
-          by (auto simp: real_integrable_def nn_integral_set_ennreal mult.commute top_unique)
+          by (auto simp: real_integrable_def nn_integral_set_ennreal mult.commute top_unique set_integrable_def)
       have "(\<integral>\<^sup>+ x. g' x * indicator {a..b} x \<partial>lborel) - ?I =
                   \<integral>\<^sup>+ x. ennreal (g' x * indicator {a..b} x) -
                         indicator (g -` A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x) \<partial>lborel"
         apply (intro nn_integral_diff[symmetric])
-        apply (insert Mg', simp add: mult.commute) []
+        apply (insert Mg', simp add: mult.commute set_borel_measurable_def) []
         apply (insert Mg'', simp) []
         apply (simp split: split_indicator add: derivg_nonneg)
         apply (rule notinf)
@@ -185,7 +188,7 @@
       also have "(\<Sum>i. ... i) = \<integral>\<^sup>+ x. (\<Sum>i. ennreal (g' x * indicator {a..b} x) * indicator ({a..b} \<inter> g -` f i) x) \<partial>lborel"
         using Mg'
         apply (intro nn_integral_suminf[symmetric])
-        apply (rule borel_measurable_times_ennreal, simp add: mult.commute)
+        apply (rule borel_measurable_times_ennreal, simp add: mult.commute set_borel_measurable_def)
         apply (rule borel_measurable_indicator, subst sets_lborel)
         apply (simp_all split: split_indicator add: derivg_nonneg)
         done
@@ -209,7 +212,7 @@
     let ?I = "indicator {a..b}"
     have "(\<lambda>x. f (g x * ?I x) * ennreal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg'
       by (intro borel_measurable_times_ennreal measurable_compose[OF _ Mf])
-         (simp_all add: mult.commute)
+         (simp_all add: mult.commute set_borel_measurable_def)
     also have "(\<lambda>x. f (g x * ?I x) * ennreal (g' x * ?I x)) = (\<lambda>x. f (g x) * ennreal (g' x) * ?I x)"
       by (intro ext) (simp split: split_indicator)
     finally have Mf': "(\<lambda>x. f (g x) * ennreal (g' x) * ?I x) \<in> borel_measurable borel" .
@@ -223,7 +226,7 @@
       fix f :: "real \<Rightarrow> ennreal" assume Mf: "f \<in> borel_measurable borel"
       have "(\<lambda>x. f (g x * ?I x) * ennreal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg'
         by (intro borel_measurable_times_ennreal measurable_compose[OF _ Mf])
-           (simp_all add:  mult.commute)
+           (simp_all add:  mult.commute set_borel_measurable_def)
       also have "(\<lambda>x. f (g x * ?I x) * ennreal (g' x * ?I x)) = (\<lambda>x. f (g x) * ennreal (g' x) * ?I x)"
         by (intro ext) (simp split: split_indicator)
       finally have "(\<lambda>x. f (g x) * ennreal (g' x) * ?I x) \<in> borel_measurable borel" .
@@ -250,7 +253,7 @@
     let ?I = "indicator {a..b}"
     have "(\<lambda>x. F i (g x * ?I x) * ennreal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg'
       by (rule_tac borel_measurable_times_ennreal, rule_tac measurable_compose[OF _ sup.hyps(1)])
-         (simp_all add: mult.commute)
+         (simp_all add: mult.commute set_borel_measurable_def)
     also have "(\<lambda>x. F i (g x * ?I x) * ennreal (g' x * ?I x)) = (\<lambda>x. F i (g x) * ennreal (g' x) * ?I x)"
       by (intro ext) (simp split: split_indicator)
      finally have "... \<in> borel_measurable borel" .
@@ -306,7 +309,7 @@
        (auto split: split_indicator split_max simp: zero_ennreal.rep_eq ennreal_neg)
   also have "... = \<integral>\<^sup>+ x. ?f' (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel" using Mf
     by (subst nn_integral_substitution_aux[OF _ _ derivg contg' derivg_nonneg \<open>a < b\<close>])
-       (auto simp add: mult.commute)
+       (auto simp add: mult.commute set_borel_measurable_def)
   also have "... = \<integral>\<^sup>+ x. f (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel"
     by (intro nn_integral_cong) (auto split: split_indicator simp: max_def dest: bounds)
   also have "... = \<integral>\<^sup>+x. ennreal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel"
@@ -334,13 +337,14 @@
            (\<lambda>x. ennreal (f x * indicator {g a..g b} x))"
     by (intro ext) (simp split: split_indicator)
   with integrable have M1: "(\<lambda>x. f x * indicator {g a..g b} x) \<in> borel_measurable borel"
-    unfolding real_integrable_def by (force simp: mult.commute)
+    by (force simp: mult.commute set_integrable_def)
   from integrable have M2: "(\<lambda>x. -f x * indicator {g a..g b} x) \<in> borel_measurable borel"
-    unfolding real_integrable_def by (force simp: mult.commute)
+    by (force simp: mult.commute set_integrable_def)
 
   have "LBINT x. (f x :: real) * indicator {g a..g b} x =
           enn2real (\<integral>\<^sup>+ x. ennreal (f x) * indicator {g a..g b} x \<partial>lborel) -
           enn2real (\<integral>\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \<partial>lborel)" using integrable
+    unfolding set_integrable_def
     by (subst real_lebesgue_integral_def) (simp_all add: nn_integral_set_ennreal mult.commute)
   also have *: "(\<integral>\<^sup>+x. ennreal (f x) * indicator {g a..g b} x \<partial>lborel) =
       (\<integral>\<^sup>+x. ennreal (f x * indicator {g a..g b} x) \<partial>lborel)"
@@ -348,32 +352,33 @@
   also from M1 * have A: "(\<integral>\<^sup>+ x. ennreal (f x * indicator {g a..g b} x) \<partial>lborel) =
                             (\<integral>\<^sup>+ x. ennreal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel)"
     by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg \<open>a \<le> b\<close>])
-       (auto simp: nn_integral_set_ennreal mult.commute)
+       (auto simp: nn_integral_set_ennreal mult.commute set_borel_measurable_def)
   also have **: "(\<integral>\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \<partial>lborel) =
       (\<integral>\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \<partial>lborel)"
     by (intro nn_integral_cong) (simp split: split_indicator)
   also from M2 ** have B: "(\<integral>\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \<partial>lborel) =
         (\<integral>\<^sup>+ x. ennreal (- (f (g x)) * g' x * indicator {a..b} x) \<partial>lborel)"
     by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg \<open>a \<le> b\<close>])
-       (auto simp: nn_integral_set_ennreal mult.commute)
+       (auto simp: nn_integral_set_ennreal mult.commute set_borel_measurable_def)
 
   also {
     from integrable have Mf: "set_borel_measurable borel {g a..g b} f"
-      unfolding real_integrable_def by simp
-    from borel_measurable_times[OF measurable_compose[OF Mg Mf] Mg']
-      have "(\<lambda>x. f (g x * indicator {a..b} x) * indicator {g a..g b} (g x * indicator {a..b} x) *
+      unfolding set_borel_measurable_def set_integrable_def by simp
+    from measurable_compose Mg Mf Mg' borel_measurable_times
+    have "(\<lambda>x. f (g x * indicator {a..b} x) * indicator {g a..g b} (g x * indicator {a..b} x) *
                      (g' x * indicator {a..b} x)) \<in> borel_measurable borel"  (is "?f \<in> _")
-      by (simp add: mult.commute)
+      by (simp add: mult.commute set_borel_measurable_def)
     also have "?f = (\<lambda>x. f (g x) * g' x * indicator {a..b} x)"
       using monog by (intro ext) (auto split: split_indicator)
     finally show "set_integrable lborel {a..b} (\<lambda>x. f (g x) * g' x)"
-      using A B integrable unfolding real_integrable_def
+      using A B integrable unfolding real_integrable_def set_integrable_def
       by (simp_all add: nn_integral_set_ennreal mult.commute)
   } note integrable' = this
 
   have "enn2real (\<integral>\<^sup>+ x. ennreal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel) -
                   enn2real (\<integral>\<^sup>+ x. ennreal (-f (g x) * g' x * indicator {a..b} x) \<partial>lborel) =
-                (LBINT x. f (g x) * g' x * indicator {a..b} x)" using integrable'
+                (LBINT x. f (g x) * g' x * indicator {a..b} x)" 
+    using integrable' unfolding set_integrable_def
     by (subst real_lebesgue_integral_def) (simp_all add: field_simps)
   finally show "(LBINT x. f x * indicator {g a..g b} x) =
                      (LBINT x. f (g x) * g' x * indicator {a..b} x)" .
@@ -391,11 +396,11 @@
   apply (subst (1 2) interval_integral_Icc, fact)
   apply (rule deriv_nonneg_imp_mono[OF derivg derivg_nonneg], simp, simp, fact)
   using integral_substitution(2)[OF assms]
-  apply (simp add: mult.commute)
+  apply (simp add: mult.commute set_lebesgue_integral_def)
   done
 
-lemma set_borel_integrable_singleton[simp]:
-  "set_integrable lborel {x} (f :: real \<Rightarrow> real)"
+lemma set_borel_integrable_singleton[simp]: "set_integrable lborel {x} (f :: real \<Rightarrow> real)"
+  unfolding set_integrable_def
   by (subst integrable_discrete_difference[where X="{x}" and g="\<lambda>_. 0"]) auto
 
 end
diff -r 9ecc78bcf1ef -r 06bce659d41b src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Fri Apr 13 17:25:02 2018 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy	Fri Apr 13 17:00:57 2018 +0100
@@ -15,18 +15,18 @@
     Notation
 *)
 
-abbreviation "set_borel_measurable M A f \<equiv> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable M"
+definition "set_borel_measurable M A f \<equiv> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable M"
 
-abbreviation "set_integrable M A f \<equiv> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
+definition "set_integrable M A f \<equiv> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
 
-abbreviation "set_lebesgue_integral M A f \<equiv> lebesgue_integral M (\<lambda>x. indicator A x *\<^sub>R f x)"
+definition "set_lebesgue_integral M A f \<equiv> lebesgue_integral M (\<lambda>x. indicator A x *\<^sub>R f x)"
 
 syntax
-"_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
-("(4LINT (_):(_)/|(_)./ _)" [0,60,110,61] 60)
+  "_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
+  ("(4LINT (_):(_)/|(_)./ _)" [0,60,110,61] 60)
 
 translations
-"LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
+  "LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
 
 (*
     Notation for integration wrt lebesgue measure on the reals:
@@ -38,12 +38,12 @@
 *)
 
 syntax
-"_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
-("(2LBINT _./ _)" [0,60] 60)
+  "_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
+  ("(2LBINT _./ _)" [0,60] 60)
 
 syntax
-"_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
-("(3LBINT _:_./ _)" [0,60,61] 60)
+  "_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
+  ("(3LBINT _:_./ _)" [0,60,61] 60)
 
 (*
     Basic properties
@@ -60,17 +60,22 @@
   shows "f -` B \<inter> X \<in> sets M"
 proof -
   have "f \<in> borel_measurable (restrict_space M X)"
-    using assms by (subst borel_measurable_restrict_space_iff) auto
+    using assms unfolding set_borel_measurable_def by (subst borel_measurable_restrict_space_iff) auto
   then have "f -` B \<inter> space (restrict_space M X) \<in> sets (restrict_space M X)"
     by (rule measurable_sets) fact
   with \<open>X \<in> sets M\<close> show ?thesis
     by (subst (asm) sets_restrict_space_iff) (auto simp: space_restrict_space)
 qed
 
+lemma set_lebesgue_integral_zero [simp]: "set_lebesgue_integral M A (\<lambda>x. 0) = 0"
+  by (auto simp: set_lebesgue_integral_def)
+
 lemma set_lebesgue_integral_cong:
   assumes "A \<in> sets M" and "\<forall>x. x \<in> A \<longrightarrow> f x = g x"
   shows "(LINT x:A|M. f x) = (LINT x:A|M. g x)"
-  using assms by (auto intro!: Bochner_Integration.integral_cong split: split_indicator simp add: sets.sets_into_space)
+  unfolding set_lebesgue_integral_def
+  using assms
+  by (metis indicator_simps(2) real_vector.scale_zero_left)
 
 lemma set_lebesgue_integral_cong_AE:
   assumes [measurable]: "A \<in> sets M" "f \<in> borel_measurable M" "g \<in> borel_measurable M"
@@ -79,13 +84,15 @@
 proof-
   have "AE x in M. indicator A x *\<^sub>R f x = indicator A x *\<^sub>R g x"
     using assms by auto
-  thus ?thesis by (intro integral_cong_AE) auto
+  thus ?thesis
+  unfolding set_lebesgue_integral_def by (intro integral_cong_AE) auto
 qed
 
 lemma set_integrable_cong_AE:
     "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow>
     AE x \<in> A in M. f x = g x \<Longrightarrow> A \<in> sets M \<Longrightarrow>
     set_integrable M A f = set_integrable M A g"
+  unfolding set_integrable_def
   by (rule integrable_cong_AE) auto
 
 lemma set_integrable_subset:
@@ -94,8 +101,9 @@
   shows "set_integrable M B f"
 proof -
   have "set_integrable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
-    by (rule integrable_mult_indicator) fact+
+    using assms integrable_mult_indicator set_integrable_def by blast
   with \<open>B \<subseteq> A\<close> show ?thesis
+    unfolding set_integrable_def
     by (simp add: indicator_inter_arith[symmetric] Int_absorb2)
 qed
 
@@ -104,11 +112,12 @@
   assumes f: "set_integrable M S f" and T: "T \<in> sets (restrict_space M S)"
   shows "set_integrable M T f"
 proof -
-  obtain T' where T_eq: "T = S \<inter> T'" and "T' \<in> sets M" using T by (auto simp: sets_restrict_space)
-
+  obtain T' where T_eq: "T = S \<inter> T'" and "T' \<in> sets M" 
+    using T by (auto simp: sets_restrict_space)
   have \<open>integrable M (\<lambda>x. indicator T' x *\<^sub>R (indicator S x *\<^sub>R f x))\<close>
-    by (rule integrable_mult_indicator; fact)
+    using \<open>T' \<in> sets M\<close> f integrable_mult_indicator set_integrable_def by blast
   then show ?thesis
+    unfolding set_integrable_def
     unfolding T_eq indicator_inter_arith by (simp add: ac_simps)
 qed
 
@@ -116,41 +125,49 @@
 (* TODO: borel_integrable_atLeastAtMost should be named something like set_integrable_Icc_isCont *)
 
 lemma set_integral_scaleR_right [simp]: "LINT t:A|M. a *\<^sub>R f t = a *\<^sub>R (LINT t:A|M. f t)"
+  unfolding set_lebesgue_integral_def
   by (subst integral_scaleR_right[symmetric]) (auto intro!: Bochner_Integration.integral_cong)
 
 lemma set_integral_mult_right [simp]:
   fixes a :: "'a::{real_normed_field, second_countable_topology}"
   shows "LINT t:A|M. a * f t = a * (LINT t:A|M. f t)"
+  unfolding set_lebesgue_integral_def
   by (subst integral_mult_right_zero[symmetric]) auto
 
 lemma set_integral_mult_left [simp]:
   fixes a :: "'a::{real_normed_field, second_countable_topology}"
   shows "LINT t:A|M. f t * a = (LINT t:A|M. f t) * a"
+  unfolding set_lebesgue_integral_def
   by (subst integral_mult_left_zero[symmetric]) auto
 
 lemma set_integral_divide_zero [simp]:
   fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
   shows "LINT t:A|M. f t / a = (LINT t:A|M. f t) / a"
+  unfolding set_lebesgue_integral_def
   by (subst integral_divide_zero[symmetric], intro Bochner_Integration.integral_cong)
      (auto split: split_indicator)
 
 lemma set_integrable_scaleR_right [simp, intro]:
   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. a *\<^sub>R f t)"
+  unfolding set_integrable_def
   unfolding scaleR_left_commute by (rule integrable_scaleR_right)
 
 lemma set_integrable_scaleR_left [simp, intro]:
   fixes a :: "_ :: {banach, second_countable_topology}"
   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t *\<^sub>R a)"
+  unfolding set_integrable_def
   using integrable_scaleR_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
 
 lemma set_integrable_mult_right [simp, intro]:
   fixes a :: "'a::{real_normed_field, second_countable_topology}"
   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. a * f t)"
+  unfolding set_integrable_def
   using integrable_mult_right[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
 
 lemma set_integrable_mult_left [simp, intro]:
   fixes a :: "'a::{real_normed_field, second_countable_topology}"
   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t * a)"
+  unfolding set_integrable_def
   using integrable_mult_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
 
 lemma set_integrable_divide [simp, intro]:
@@ -159,10 +176,11 @@
   shows "set_integrable M A (\<lambda>t. f t / a)"
 proof -
   have "integrable M (\<lambda>x. indicator A x *\<^sub>R f x / a)"
-    using assms by (rule integrable_divide_zero)
+    using assms unfolding set_integrable_def by (rule integrable_divide_zero)
   also have "(\<lambda>x. indicator A x *\<^sub>R f x / a) = (\<lambda>x. indicator A x *\<^sub>R (f x / a))"
     by (auto split: split_indicator)
-  finally show ?thesis .
+  finally show ?thesis 
+    unfolding set_integrable_def .
 qed
 
 lemma set_integral_add [simp, intro]:
@@ -170,21 +188,23 @@
   assumes "set_integrable M A f" "set_integrable M A g"
   shows "set_integrable M A (\<lambda>x. f x + g x)"
     and "LINT x:A|M. f x + g x = (LINT x:A|M. f x) + (LINT x:A|M. g x)"
-  using assms by (simp_all add: scaleR_add_right)
+  using assms unfolding set_integrable_def set_lebesgue_integral_def by (simp_all add: scaleR_add_right)
 
 lemma set_integral_diff [simp, intro]:
   assumes "set_integrable M A f" "set_integrable M A g"
   shows "set_integrable M A (\<lambda>x. f x - g x)" and "LINT x:A|M. f x - g x =
     (LINT x:A|M. f x) - (LINT x:A|M. g x)"
-  using assms by (simp_all add: scaleR_diff_right)
+  using assms unfolding set_integrable_def set_lebesgue_integral_def by (simp_all add: scaleR_diff_right)
 
 (* question: why do we have this for negation, but multiplication by a constant
    requires an integrability assumption? *)
 lemma set_integral_uminus: "set_integrable M A f \<Longrightarrow> LINT x:A|M. - f x = - (LINT x:A|M. f x)"
+  unfolding set_integrable_def set_lebesgue_integral_def
   by (subst integral_minus[symmetric]) simp_all
 
 lemma set_integral_complex_of_real:
   "LINT x:A|M. complex_of_real (f x) = of_real (LINT x:A|M. f x)"
+  unfolding set_lebesgue_integral_def
   by (subst integral_complex_of_real[symmetric])
      (auto intro!: Bochner_Integration.integral_cong split: split_indicator)
 
@@ -193,28 +213,31 @@
   assumes "set_integrable M A f" "set_integrable M A g"
     "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
   shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)"
-using assms by (auto intro: integral_mono split: split_indicator)
+  using assms unfolding set_integrable_def set_lebesgue_integral_def
+  by (auto intro: integral_mono split: split_indicator)
 
 lemma set_integral_mono_AE:
   fixes f g :: "_ \<Rightarrow> real"
   assumes "set_integrable M A f" "set_integrable M A g"
     "AE x \<in> A in M. f x \<le> g x"
   shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)"
-using assms by (auto intro: integral_mono_AE split: split_indicator)
+  using assms unfolding set_integrable_def set_lebesgue_integral_def
+  by (auto intro: integral_mono_AE split: split_indicator)
 
 lemma set_integrable_abs: "set_integrable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar> :: real)"
-  using integrable_abs[of M "\<lambda>x. f x * indicator A x"] by (simp add: abs_mult ac_simps)
+  using integrable_abs[of M "\<lambda>x. f x * indicator A x"]unfolding set_integrable_def by (simp add: abs_mult ac_simps)
 
 lemma set_integrable_abs_iff:
   fixes f :: "_ \<Rightarrow> real"
   shows "set_borel_measurable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f"
+  unfolding set_integrable_def set_borel_measurable_def
   by (subst (2) integrable_abs_iff[symmetric]) (simp_all add: abs_mult ac_simps)
 
 lemma set_integrable_abs_iff':
   fixes f :: "_ \<Rightarrow> real"
   shows "f \<in> borel_measurable M \<Longrightarrow> A \<in> sets M \<Longrightarrow>
     set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f"
-by (intro set_integrable_abs_iff) auto
+  by (simp add: set_borel_measurable_def set_integrable_abs_iff)
 
 lemma set_integrable_discrete_difference:
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
@@ -222,6 +245,7 @@
   assumes diff: "(A - B) \<union> (B - A) \<subseteq> X"
   assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
   shows "set_integrable M A f \<longleftrightarrow> set_integrable M B f"
+  unfolding set_integrable_def
 proof (rule integrable_discrete_difference[where X=X])
   show "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> indicator A x *\<^sub>R f x = indicator B x *\<^sub>R f x"
     using diff by (auto split: split_indicator)
@@ -233,6 +257,7 @@
   assumes diff: "(A - B) \<union> (B - A) \<subseteq> X"
   assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
   shows "set_lebesgue_integral M A f = set_lebesgue_integral M B f"
+  unfolding set_lebesgue_integral_def
 proof (rule integral_discrete_difference[where X=X])
   show "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> indicator A x *\<^sub>R f x = indicator B x *\<^sub>R f x"
     using diff by (auto split: split_indicator)
@@ -246,35 +271,44 @@
 proof -
   have "set_integrable M (A - B) f"
     using f_A by (rule set_integrable_subset) auto
-  from Bochner_Integration.integrable_add[OF this f_B] show ?thesis
+  with f_B have "integrable M (\<lambda>x. indicator (A - B) x *\<^sub>R f x + indicator B x *\<^sub>R f x)"
+    unfolding set_integrable_def using integrable_add by blast
+  then show ?thesis
+    unfolding set_integrable_def
     by (rule integrable_cong[THEN iffD1, rotated 2]) (auto split: split_indicator)
 qed
 
+lemma set_integrable_empty [simp]: "set_integrable M {} f"
+  by (auto simp: set_integrable_def)
+
 lemma set_integrable_UN:
   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   assumes "finite I" "\<And>i. i\<in>I \<Longrightarrow> set_integrable M (A i) f"
     "\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets M"
   shows "set_integrable M (\<Union>i\<in>I. A i) f"
-using assms by (induct I) (auto intro!: set_integrable_Un)
+  using assms
+  by (induct I) (auto simp: set_integrable_Un sets.finite_UN)
 
 lemma set_integral_Un:
   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   assumes "A \<inter> B = {}"
   and "set_integrable M A f"
   and "set_integrable M B f"
-  shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
-by (auto simp add: indicator_union_arith indicator_inter_arith[symmetric]
-      scaleR_add_left assms)
+shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
+  using assms
+  unfolding set_integrable_def set_lebesgue_integral_def
+  by (auto simp add: indicator_union_arith indicator_inter_arith[symmetric] scaleR_add_left)
 
 lemma set_integral_cong_set:
   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
-  assumes [measurable]: "set_borel_measurable M A f" "set_borel_measurable M B f"
+  assumes "set_borel_measurable M A f" "set_borel_measurable M B f"
     and ae: "AE x in M. x \<in> A \<longleftrightarrow> x \<in> B"
   shows "LINT x:B|M. f x = LINT x:A|M. f x"
+  unfolding set_lebesgue_integral_def
 proof (rule integral_cong_AE)
   show "AE x in M. indicator B x *\<^sub>R f x = indicator A x *\<^sub>R f x"
     using ae by (auto simp: subset_eq split: split_indicator)
-qed fact+
+qed (use assms in \<open>auto simp: set_borel_measurable_def\<close>)
 
 lemma set_borel_measurable_subset:
   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
@@ -282,10 +316,12 @@
   shows "set_borel_measurable M B f"
 proof -
   have "set_borel_measurable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
-    by measurable
-  also have "(\<lambda>x. indicator B x *\<^sub>R indicator A x *\<^sub>R f x) = (\<lambda>x. indicator B x *\<^sub>R f x)"
+    using assms unfolding set_borel_measurable_def
+    using borel_measurable_indicator borel_measurable_scaleR by blast 
+  moreover have "(\<lambda>x. indicator B x *\<^sub>R indicator A x *\<^sub>R f x) = (\<lambda>x. indicator B x *\<^sub>R f x)"
     using \<open>B \<subseteq> A\<close> by (auto simp: fun_eq_iff split: split_indicator)
-  finally show ?thesis .
+  ultimately show ?thesis 
+    unfolding set_borel_measurable_def by simp
 qed
 
 lemma set_integral_Un_AE:
@@ -298,7 +334,7 @@
   have f: "set_integrable M (A \<union> B) f"
     by (intro set_integrable_Un assms)
   then have f': "set_borel_measurable M (A \<union> B) f"
-    by (rule borel_measurable_integrable)
+    using integrable_iff_bounded set_borel_measurable_def set_integrable_def by blast
   have "LINT x:A\<union>B|M. f x = LINT x:(A - A \<inter> B) \<union> (B - A \<inter> B)|M. f x"
   proof (rule set_integral_cong_set)
     show "AE x in M. (x \<in> A - A \<inter> B \<union> (B - A \<inter> B)) = (x \<in> A \<union> B)"
@@ -321,9 +357,13 @@
     and "\<And>i. i \<in> I \<Longrightarrow> set_integrable M (A i) f" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
   shows "(LINT x:(\<Union>i\<in>I. A i)|M. f x) = (\<Sum>i\<in>I. LINT x:A i|M. f x)"
   using assms
-  apply induct
-  apply (auto intro!: set_integral_Un set_integrable_Un set_integrable_UN simp: disjoint_family_on_def)
-by (subst set_integral_Un, auto intro: set_integrable_UN)
+proof induction
+  case (insert x F)
+  then have "A x \<inter> UNION F A = {}"
+    by (meson disjoint_family_on_insert)
+  with insert show ?case
+    by (simp add: set_integral_Un set_integrable_Un set_integrable_UN disjoint_family_on_insert)
+qed (simp add: set_lebesgue_integral_def)
 
 (* TODO: find a better name? *)
 lemma pos_integrable_to_top:
@@ -332,10 +372,11 @@
   assumes nneg: "\<And>x i. x \<in> A i \<Longrightarrow> 0 \<le> f x"
   and intgbl: "\<And>i::nat. set_integrable M (A i) f"
   and lim: "(\<lambda>i::nat. LINT x:A i|M. f x) \<longlonglongrightarrow> l"
-  shows "set_integrable M (\<Union>i. A i) f"
+shows "set_integrable M (\<Union>i. A i) f"
+    unfolding set_integrable_def
   apply (rule integrable_monotone_convergence[where f = "\<lambda>i::nat. \<lambda>x. indicator (A i) x *\<^sub>R f x" and x = l])
-  apply (rule intgbl)
-  prefer 3 apply (rule lim)
+  apply (rule intgbl [unfolded set_integrable_def])
+  prefer 3 apply (rule lim [unfolded set_lebesgue_integral_def])
   apply (rule AE_I2)
   using \<open>mono A\<close> apply (auto simp: mono_def nneg split: split_indicator) []
 proof (rule AE_I2)
@@ -356,8 +397,7 @@
   then show "(\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R f x) \<in> borel_measurable M"
     apply (rule borel_measurable_LIMSEQ_real)
     apply assumption
-    apply (intro borel_measurable_integrable intgbl)
-    done
+    using intgbl set_integrable_def by blast
 qed
 
 (* Proof from Royden Real Analysis, p. 91. *)
@@ -367,16 +407,18 @@
     and disj: "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
     and intgbl: "set_integrable M (\<Union>i. A i) f"
   shows "LINT x:(\<Union>i. A i)|M. f x = (\<Sum>i. (LINT x:(A i)|M. f x))"
+    unfolding set_lebesgue_integral_def
 proof (subst integral_suminf[symmetric])
-  show int_A: "\<And>i. set_integrable M (A i) f"
-    using intgbl by (rule set_integrable_subset) auto
+  show int_A: "integrable M (\<lambda>x. indicat_real (A i) x *\<^sub>R f x)" for i
+    using intgbl unfolding set_integrable_def [symmetric]
+    by (rule set_integrable_subset) auto
   { fix x assume "x \<in> space M"
     have "(\<lambda>i. indicator (A i) x *\<^sub>R f x) sums (indicator (\<Union>i. A i) x *\<^sub>R f x)"
       by (intro sums_scaleR_left indicator_sums) fact }
   note sums = this
 
   have norm_f: "\<And>i. set_integrable M (A i) (\<lambda>x. norm (f x))"
-    using int_A[THEN integrable_norm] by auto
+    using int_A[THEN integrable_norm] unfolding set_integrable_def by auto
 
   show "AE x in M. summable (\<lambda>i. norm (indicator (A i) x *\<^sub>R f x))"
     using disj by (intro AE_I2) (auto intro!: summable_mult2 sums_summable[OF indicator_sums])
@@ -387,21 +429,22 @@
     show "0 \<le> LINT x|M. norm (indicator (A n) x *\<^sub>R f x)"
       using norm_f by (auto intro!: integral_nonneg_AE)
 
-    have "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) =
-      (\<Sum>i<n. set_lebesgue_integral M (A i) (\<lambda>x. norm (f x)))"
-      by (simp add: abs_mult)
+    have "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) = (\<Sum>i<n. LINT x:A i|M. norm (f x))"
+      by (simp add: abs_mult set_lebesgue_integral_def)
     also have "\<dots> = set_lebesgue_integral M (\<Union>i<n. A i) (\<lambda>x. norm (f x))"
       using norm_f
       by (subst set_integral_finite_Union) (auto simp: disjoint_family_on_def disj)
     also have "\<dots> \<le> set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
-      using intgbl[THEN integrable_norm]
-      by (intro integral_mono set_integrable_UN[of "{..<n}"] norm_f)
-         (auto split: split_indicator)
+      using intgbl[unfolded set_integrable_def, THEN integrable_norm] norm_f
+      unfolding set_lebesgue_integral_def set_integrable_def
+      apply (intro integral_mono set_integrable_UN[of "{..<n}", unfolded set_integrable_def])
+          apply (auto split: split_indicator)
+      done
     finally show "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) \<le>
       set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
       by simp
   qed
-  show "set_lebesgue_integral M (UNION UNIV A) f = LINT x|M. (\<Sum>i. indicator (A i) x *\<^sub>R f x)"
+  show "LINT x|M. indicator (UNION UNIV A) x *\<^sub>R f x = LINT x|M. (\<Sum>i. indicator (A i) x *\<^sub>R f x)"
     apply (rule Bochner_Integration.integral_cong[OF refl])
     apply (subst suminf_scaleR_left[OF sums_summable[OF indicator_sums, OF disj], symmetric])
     using sums_unique[OF indicator_sums[OF disj]]
@@ -413,14 +456,18 @@
   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "incseq A"
   and intgbl: "set_integrable M (\<Union>i. A i) f"
-  shows "(\<lambda>i. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Union>i. A i)|M. f x"
+shows "(\<lambda>i. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Union>i. A i)|M. f x"
+  unfolding set_lebesgue_integral_def
 proof (intro integral_dominated_convergence[where w="\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R norm (f x)"])
   have int_A: "\<And>i. set_integrable M (A i) f"
     using intgbl by (rule set_integrable_subset) auto
-  then show "\<And>i. set_borel_measurable M (A i) f" "set_borel_measurable M (\<Union>i. A i) f"
-    "set_integrable M (\<Union>i. A i) (\<lambda>x. norm (f x))"
-    using intgbl integrable_norm[OF intgbl] by auto
-
+  show "\<And>i. (\<lambda>x. indicator (A i) x *\<^sub>R f x) \<in> borel_measurable M"
+    using int_A integrable_iff_bounded set_integrable_def by blast
+  show "(\<lambda>x. indicator (UNION UNIV A) x *\<^sub>R f x) \<in> borel_measurable M"
+    using integrable_iff_bounded intgbl set_integrable_def by blast
+  show "integrable M (\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R norm (f x))"
+    using int_A intgbl integrable_norm unfolding set_integrable_def 
+    by fastforce
   { fix x i assume "x \<in> A i"
     with A have "(\<lambda>xa. indicator (A xa) x::real) \<longlonglongrightarrow> 1 \<longleftrightarrow> (\<lambda>xa. 1::real) \<longlonglongrightarrow> 1"
       by (intro filterlim_cong refl)
@@ -435,15 +482,19 @@
   assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "decseq A"
   and int0: "set_integrable M (A 0) f"
   shows "(\<lambda>i::nat. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Inter>i. A i)|M. f x"
+  unfolding set_lebesgue_integral_def
 proof (rule integral_dominated_convergence)
   have int_A: "\<And>i. set_integrable M (A i) f"
     using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
-  show "set_integrable M (A 0) (\<lambda>x. norm (f x))"
-    using int0[THEN integrable_norm] by simp
+  have "integrable M (\<lambda>c. norm (indicat_real (A 0) c *\<^sub>R f c))"
+    by (metis (no_types) int0 integrable_norm set_integrable_def)
+  then show "integrable M (\<lambda>x. indicator (A 0) x *\<^sub>R norm (f x))"
+    by force
   have "set_integrable M (\<Inter>i. A i) f"
     using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
-  with int_A show "set_borel_measurable M (\<Inter>i. A i) f" "\<And>i. set_borel_measurable M (A i) f"
-    by auto
+  with int_A show "(\<lambda>x. indicat_real (INTER UNIV A) x *\<^sub>R f x) \<in> borel_measurable M"
+                  "\<And>i. (\<lambda>x. indicat_real (A i) x *\<^sub>R f x) \<in> borel_measurable M"
+    by (auto simp: set_integrable_def)
   show "\<And>i. AE x in M. norm (indicator (A i) x *\<^sub>R f x) \<le> indicator (A 0) x *\<^sub>R norm (f x)"
     using A by (auto split: split_indicator simp: decseq_def)
   { fix x i assume "x \<in> space M" "x \<notin> A i"
@@ -462,7 +513,8 @@
 proof-
   have "set_lebesgue_integral M {a} f = set_lebesgue_integral M {a} (%x. f a)"
     by (intro set_lebesgue_integral_cong) simp_all
-  then show ?thesis using assms by simp
+  then show ?thesis using assms
+    unfolding set_lebesgue_integral_def by simp
 qed
 
 
@@ -523,6 +575,7 @@
 lemma set_measurable_continuous_on_ivl:
   assumes "continuous_on {a..b} (f :: real \<Rightarrow> real)"
   shows "set_borel_measurable borel {a..b} f"
+  unfolding set_borel_measurable_def
   by (rule borel_measurable_continuous_on_indicator[OF _ assms]) simp
 
 
@@ -670,19 +723,19 @@
 lemma set_integral_null_delta:
   fixes f::"_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   assumes [measurable]: "integrable M f" "A \<in> sets M" "B \<in> sets M"
-    and "(A - B) \<union> (B - A) \<in> null_sets M"
+    and null: "(A - B) \<union> (B - A) \<in> null_sets M"
   shows "(\<integral>x \<in> A. f x \<partial>M) = (\<integral>x \<in> B. f x \<partial>M)"
-proof (rule set_integral_cong_set, auto)
+proof (rule set_integral_cong_set)
   have *: "AE a in M. a \<notin> (A - B) \<union> (B - A)"
-    using assms(4) AE_not_in by blast
+    using null AE_not_in by blast
   then show "AE x in M. (x \<in> B) = (x \<in> A)"
     by auto
-qed
+qed (simp_all add: set_borel_measurable_def)
 
 lemma set_integral_space:
   assumes "integrable M f"
   shows "(\<integral>x \<in> space M. f x \<partial>M) = (\<integral>x. f x \<partial>M)"
-by (metis (mono_tags, lifting) indicator_simps(1) Bochner_Integration.integral_cong real_vector.scale_one)
+  by (metis (no_types, lifting) indicator_simps(1) integral_cong scaleR_one set_lebesgue_integral_def)
 
 lemma null_if_pos_func_has_zero_nn_int:
   fixes f::"'a \<Rightarrow> ennreal"
@@ -703,7 +756,8 @@
 proof -
   have "AE x in M. indicator A x * f x = 0"
     apply (subst integral_nonneg_eq_0_iff_AE[symmetric])
-    using assms integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)] by auto
+    using assms integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)]
+    by (auto simp: set_lebesgue_integral_def)
   then have "AE x\<in>A in M. f x = 0" by auto
   then have "AE x\<in>A in M. False" using assms(3) by auto
   then show "A \<in> null_sets M" using assms(2) by (simp add: AE_iff_null_sets)
@@ -728,31 +782,29 @@
 
 lemma density_unique_real:
   fixes f f'::"_ \<Rightarrow> real"
-  assumes [measurable]: "integrable M f" "integrable M f'"
+  assumes M[measurable]: "integrable M f" "integrable M f'"
   assumes density_eq: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>x \<in> A. f x \<partial>M) = (\<integral>x \<in> A. f' x \<partial>M)"
   shows "AE x in M. f x = f' x"
 proof -
   define A where "A = {x \<in> space M. f x < f' x}"
   then have [measurable]: "A \<in> sets M" by simp
   have "(\<integral>x \<in> A. (f' x - f x) \<partial>M) = (\<integral>x \<in> A. f' x \<partial>M) - (\<integral>x \<in> A. f x \<partial>M)"
-    using \<open>A \<in> sets M\<close> assms(1) assms(2) integrable_mult_indicator by blast
+    using \<open>A \<in> sets M\<close> M integrable_mult_indicator set_integrable_def by blast
   then have "(\<integral>x \<in> A. (f' x - f x) \<partial>M) = 0" using assms(3) by simp
   then have "A \<in> null_sets M"
     using A_def null_if_pos_func_has_zero_int[where ?f = "\<lambda>x. f' x - f x" and ?A = A] assms by auto
   then have "AE x in M. x \<notin> A" by (simp add: AE_not_in)
   then have *: "AE x in M. f' x \<le> f x" unfolding A_def by auto
 
-
   define B where "B = {x \<in> space M. f' x < f x}"
   then have [measurable]: "B \<in> sets M" by simp
   have "(\<integral>x \<in> B. (f x - f' x) \<partial>M) = (\<integral>x \<in> B. f x \<partial>M) - (\<integral>x \<in> B. f' x \<partial>M)"
-    using \<open>B \<in> sets M\<close> assms(1) assms(2) integrable_mult_indicator by blast
+    using \<open>B \<in> sets M\<close> M integrable_mult_indicator set_integrable_def by blast
   then have "(\<integral>x \<in> B. (f x - f' x) \<partial>M) = 0" using assms(3) by simp
   then have "B \<in> null_sets M"
     using B_def null_if_pos_func_has_zero_int[where ?f = "\<lambda>x. f x - f' x" and ?A = B] assms by auto
   then have "AE x in M. x \<notin> B" by (simp add: AE_not_in)
   then have "AE x in M. f' x \<ge> f x" unfolding B_def by auto
-
   then show ?thesis using * by auto
 qed
 
diff -r 9ecc78bcf1ef -r 06bce659d41b src/HOL/Probability/Characteristic_Functions.thy
--- a/src/HOL/Probability/Characteristic_Functions.thy	Fri Apr 13 17:25:02 2018 +0200
+++ b/src/HOL/Probability/Characteristic_Functions.thy	Fri Apr 13 17:00:57 2018 +0100
@@ -274,7 +274,8 @@
   have *: "\<And>a b. interval_lebesgue_integrable lborel a b f \<Longrightarrow> interval_lebesgue_integrable lborel a b g \<Longrightarrow>
       \<bar>LBINT s=a..b. f s\<bar> \<le> \<bar>LBINT s=a..b. g s\<bar>"
     if f: "\<And>s. 0 \<le> f s" and g: "\<And>s. f s \<le> g s" for f g :: "_ \<Rightarrow> real"
-    using order_trans[OF f g] f g unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def
+    using order_trans[OF f g] f g 
+    unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def set_integrable_def
     by (auto simp: integral_nonneg_AE[OF AE_I2] intro!: integral_mono mult_mono)
 
   have "iexp x - (\<Sum>k \<le> Suc n. (\<i> * x)^k / fact k) =
diff -r 9ecc78bcf1ef -r 06bce659d41b src/HOL/Probability/Conditional_Expectation.thy
--- a/src/HOL/Probability/Conditional_Expectation.thy	Fri Apr 13 17:25:02 2018 +0200
+++ b/src/HOL/Probability/Conditional_Expectation.thy	Fri Apr 13 17:00:57 2018 +0100
@@ -739,7 +739,8 @@
 proof -
   have "A \<in> sets M" by (meson assms(2) subalg subalgebra_def subsetD)
   have "integrable M (\<lambda>x. indicator A x * f x)" using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)] by auto
-  then show ?thesis using real_cond_exp_intg(2)[where ?f = "indicator A" and ?g = f, symmetric] by auto
+  then show ?thesis using real_cond_exp_intg(2)[where ?f = "indicator A" and ?g = f, symmetric]
+    unfolding set_lebesgue_integral_def by auto
 qed
 
 lemma real_cond_exp_int [intro]:
@@ -760,14 +761,14 @@
     then have [measurable]: "A \<in> sets F" using sets_restr_to_subalg[OF subalg] by simp
     then have a [measurable]: "A \<in> sets M" by (meson subalg subalgebra_def subsetD)
     have "(\<integral>x \<in> A. g x \<partial> ?MF) = (\<integral>x \<in> A. g x \<partial>M)"
-      by (simp add: integral_subalgebra2 subalg)
+      unfolding set_lebesgue_integral_def  by (simp add: integral_subalgebra2 subalg)
     also have "... = (\<integral>x \<in> A. f x \<partial>M)" using assms(1) by simp
-    also have "... = (\<integral>x. indicator A x * f x \<partial>M)" by (simp add: mult.commute)
+    also have "... = (\<integral>x. indicator A x * f x \<partial>M)" by (simp add: mult.commute set_lebesgue_integral_def)
     also have "... = (\<integral>x. indicator A x * real_cond_exp M F f x \<partial>M)"
       apply (rule real_cond_exp_intg(2)[symmetric]) using integrable_mult_indicator[OF a assms(2)] by (auto simp add: assms)
-    also have "... = (\<integral>x \<in> A. real_cond_exp M F f x \<partial>M)" by (simp add: mult.commute)
+    also have "... = (\<integral>x \<in> A. real_cond_exp M F f x \<partial>M)" by (simp add: mult.commute set_lebesgue_integral_def)
     also have "... = (\<integral>x \<in> A. real_cond_exp M F f x \<partial> ?MF)"
-      by (simp add: integral_subalgebra2 subalg)
+      by (simp add: integral_subalgebra2 subalg set_lebesgue_integral_def)
     finally show "(\<integral>x \<in> A. g x \<partial> ?MF) = (\<integral>x \<in> A. real_cond_exp M F f x \<partial> ?MF)" by simp
   next
     have "integrable M (real_cond_exp M F f)" by (rule real_cond_exp_int(1)[OF assms(2)])
@@ -791,12 +792,12 @@
   then have [measurable]: "(\<lambda>x. f x * indicator A x) \<in> borel_measurable F" by measurable
   have [measurable]: "A \<in> sets M" using subalg by (meson \<open>A \<in> sets F\<close> subalgebra_def subsetD)
   have "\<integral>x\<in>A. (f x * g x) \<partial>M = \<integral>x. (f x * indicator A x) * g x \<partial>M"
-    by (simp add: mult.commute mult.left_commute)
+    by (simp add: mult.commute mult.left_commute set_lebesgue_integral_def)
   also have "... = \<integral>x. (f x * indicator A x) * real_cond_exp M F g x \<partial>M"
     apply (rule real_cond_exp_intg(2)[symmetric], auto simp add: assms)
     using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(3)] by (simp add: mult.commute mult.left_commute)
   also have "... = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M"
-    by (simp add: mult.commute mult.left_commute)
+    by (simp add: mult.commute mult.left_commute set_lebesgue_integral_def)
   finally show "\<integral>x\<in>A. (f x * g x) \<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M" by simp
 qed (auto simp add: real_cond_exp_intg(1) assms)
 
@@ -817,17 +818,17 @@
     using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(2)] by auto
 
   have "\<integral>x\<in>A. (real_cond_exp M F f x + real_cond_exp M F g x)\<partial>M = (\<integral>x\<in>A. real_cond_exp M F f x \<partial>M) + (\<integral>x\<in>A. real_cond_exp M F g x \<partial>M)"
-    apply (rule set_integral_add, auto simp add: assms)
+    apply (rule set_integral_add, auto simp add: assms set_integrable_def)
     using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> real_cond_exp_int(1)[OF assms(1)]]
           integrable_mult_indicator[OF \<open>A \<in> sets M\<close> real_cond_exp_int(1)[OF assms(2)]] by simp_all
   also have "... = (\<integral>x. indicator A x * real_cond_exp M F f x \<partial>M) + (\<integral>x. indicator A x * real_cond_exp M F g x \<partial>M)"
-    by auto
+    unfolding set_lebesgue_integral_def by auto
   also have "... = (\<integral>x. indicator A x * f x \<partial>M) + (\<integral>x. indicator A x * g x \<partial>M)"
     using real_cond_exp_intg(2) assms \<open>A \<in> sets F\<close> intAf intAg by auto
   also have "... = (\<integral>x\<in>A. f x \<partial>M) + (\<integral>x\<in>A. g x \<partial>M)"
-    by auto
+    unfolding set_lebesgue_integral_def by auto
   also have "... = \<integral>x\<in>A. (f x + g x)\<partial>M"
-    by (rule set_integral_add(2)[symmetric]) (auto simp add: assms \<open>A \<in> sets M\<close> intAf intAg)
+    by (rule set_integral_add(2)[symmetric]) (auto simp add: assms set_integrable_def \<open>A \<in> sets M\<close> intAf intAg)
   finally show "\<integral>x\<in>A. (f x + g x)\<partial>M = \<integral>x\<in>A. (real_cond_exp M F f x + real_cond_exp M F g x)\<partial>M"
     by simp
 qed (auto simp add: assms)
@@ -911,7 +912,7 @@
 
 lemma real_cond_exp_gr_c:
   assumes [measurable]: "integrable M f"
-      and "AE x in M. f x > c"
+      and AE: "AE x in M. f x > c"
   shows "AE x in M. real_cond_exp M F f x > c"
 proof -
   define X where "X = {x \<in> space M. real_cond_exp M F f x \<le> c}"
@@ -931,24 +932,33 @@
     then have [measurable]: "A \<in> sets F" using subalg sets_restr_to_subalg by blast
     then have [measurable]: "A \<in> sets M" using sets_restr_to_subalg subalg subalgebra_def by blast
     have Ic: "set_integrable M A (\<lambda>x. c)"
+      unfolding set_integrable_def
       using \<open>emeasure (restr_to_subalg M F) A < \<infinity>\<close> emeasure_restr_to_subalg subalg by fastforce
     have If: "set_integrable M A f"
+      unfolding set_integrable_def
       by (rule integrable_mult_indicator, auto simp add: \<open>integrable M f\<close>)
-    have *: "(\<integral>x\<in>A. c \<partial>M) = (\<integral>x\<in>A. f x \<partial>M)"
-    proof (rule antisym)
-      show "(\<integral>x\<in>A. c \<partial>M) \<le> (\<integral>x\<in>A. f x \<partial>M)"
-        apply (rule set_integral_mono_AE) using Ic If assms(2) by auto
-      have "(\<integral>x\<in>A. f x \<partial>M) = (\<integral>x\<in>A. real_cond_exp M F f x \<partial>M)"
-        by (rule real_cond_exp_intA, auto simp add: \<open>integrable M f\<close>)
-      also have "... \<le> (\<integral>x\<in>A. c \<partial>M)"
-        apply (rule set_integral_mono)
-        apply (rule integrable_mult_indicator, simp, simp add: real_cond_exp_int(1)[OF \<open>integrable M f\<close>])
-        using Ic X_def \<open>A \<subseteq> X\<close> by auto
-      finally show "(\<integral>x\<in>A. f x \<partial>M) \<le> (\<integral>x\<in>A. c \<partial>M)" by simp
-    qed
     have "AE x in M. indicator A x * c = indicator A x * f x"
-      apply (rule integral_ineq_eq_0_then_AE) using Ic If * apply auto
-      using assms(2) unfolding indicator_def by auto
+    proof (rule integral_ineq_eq_0_then_AE)
+      have "(\<integral>x\<in>A. c \<partial>M) = (\<integral>x\<in>A. f x \<partial>M)"
+      proof (rule antisym)
+        show "(\<integral>x\<in>A. c \<partial>M) \<le> (\<integral>x\<in>A. f x \<partial>M)"
+          apply (rule set_integral_mono_AE) using Ic If assms(2) by auto
+        have "(\<integral>x\<in>A. f x \<partial>M) = (\<integral>x\<in>A. real_cond_exp M F f x \<partial>M)"
+          by (rule real_cond_exp_intA, auto simp add: \<open>integrable M f\<close>)
+        also have "... \<le> (\<integral>x\<in>A. c \<partial>M)"
+          apply (rule set_integral_mono)
+          unfolding set_integrable_def
+            apply (rule integrable_mult_indicator, simp, simp add: real_cond_exp_int(1)[OF \<open>integrable M f\<close>])
+          using Ic X_def \<open>A \<subseteq> X\<close> by (auto simp: set_integrable_def)
+        finally show "(\<integral>x\<in>A. f x \<partial>M) \<le> (\<integral>x\<in>A. c \<partial>M)" by simp
+      qed
+      then have "measure M A * c = LINT x|M. indicat_real A x * f x"
+        by (auto simp: set_lebesgue_integral_def)
+      then show "LINT x|M. indicat_real A x * c = LINT x|M. indicat_real A x * f x"
+        by auto
+      show "AE x in M. indicat_real A x * c \<le> indicat_real A x * f x"
+      using AE unfolding indicator_def by auto
+    qed (use Ic If  in \<open>auto simp: set_integrable_def\<close>)
     then have "AE x\<in>A in M. c = f x" by auto
     then have "AE x\<in>A in M. False" using assms(2) by auto
     have "A \<in> null_sets M" unfolding ae_filter_def by (meson AE_iff_null_sets \<open>A \<in> sets M\<close> \<open>AE x\<in>A in M. False\<close>)
@@ -1045,7 +1055,7 @@
     by (rule real_cond_exp_intg(2)[symmetric], auto simp add: *)
 
   have "(\<integral>x\<in>A. (\<Sum>i\<in>I. f i x)\<partial>M) = (\<integral>x. (\<Sum>i\<in>I. indicator A x * f i x)\<partial>M)"
-    by (simp add: sum_distrib_left)
+    by (simp add: sum_distrib_left set_lebesgue_integral_def)
   also have "... = (\<Sum>i\<in>I. (\<integral>x. indicator A x * f i x \<partial>M))"
     by (rule Bochner_Integration.integral_sum, simp add: *)
   also have "... = (\<Sum>i\<in>I. (\<integral>x. indicator A x * real_cond_exp M F (f i) x \<partial>M))"
@@ -1053,7 +1063,7 @@
   also have "... = (\<integral>x. (\<Sum>i\<in>I. indicator A x * real_cond_exp M F (f i) x)\<partial>M)"
     by (rule Bochner_Integration.integral_sum[symmetric], simp add: **)
   also have "... = (\<integral>x\<in>A. (\<Sum>i\<in>I. real_cond_exp M F (f i) x)\<partial>M)"
-    by (simp add: sum_distrib_left)
+    by (simp add: sum_distrib_left set_lebesgue_integral_def)
   finally show "(\<integral>x\<in>A. (\<Sum>i\<in>I. f i x)\<partial>M) = (\<integral>x\<in>A. (\<Sum>i\<in>I. real_cond_exp M F (f i) x)\<partial>M)" by auto
 qed (auto simp add: assms real_cond_exp_int(1)[OF assms(1)])
 
diff -r 9ecc78bcf1ef -r 06bce659d41b src/HOL/Probability/Distributions.thy
--- a/src/HOL/Probability/Distributions.thy	Fri Apr 13 17:25:02 2018 +0200
+++ b/src/HOL/Probability/Distributions.thy	Fri Apr 13 17:00:57 2018 +0100
@@ -955,12 +955,13 @@
         by (rule integral_by_parts')
            (auto intro!: derivative_eq_intros b
                  simp: diff_Suc of_nat_Suc field_simps split: nat.split)
-      also have "(\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * x * exp (- x\<^sup>2) * x ^ (Suc k)) \<partial>lborel) =
-        (\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * (exp (- x\<^sup>2) * x ^ (k + 2))) \<partial>lborel)"
-        by (intro Bochner_Integration.integral_cong) auto
+      also have "... = exp (- b\<^sup>2) * b ^ (Suc k) - (\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * (exp (- x\<^sup>2) * x ^ (k + 2))) \<partial>lborel)"
+        by (auto simp: intro!: Bochner_Integration.integral_cong)
+      also have "... = exp (- b\<^sup>2) * b ^ (Suc k) + 2 * (\<integral>x. indicator {0..b} x *\<^sub>R ?M (k + 2) x \<partial>lborel)"
+        unfolding Bochner_Integration.integral_mult_right_zero [symmetric]
+        by (simp del: real_scaleR_def)
       finally have "Suc k * (\<integral>x. indicator {0..b} x *\<^sub>R ?M k x \<partial>lborel) =
-        exp (- b\<^sup>2) * b ^ (Suc k) + 2 * (\<integral>x. indicator {0..b} x *\<^sub>R ?M (k + 2) x \<partial>lborel)"
-        by (simp del: real_scaleR_def integral_mult_right add: integral_mult_right[symmetric])
+        exp (- b\<^sup>2) * b ^ (Suc k) + 2 * (\<integral>x. indicator {0..b} x *\<^sub>R ?M (k + 2) x \<partial>lborel)" .
       then show "(k + 1) / 2 * (\<integral>x. indicator {..b} x *\<^sub>R (indicator {0..} x *\<^sub>R ?M k x)\<partial>lborel) - exp (- b\<^sup>2) * b ^ (k + 1) / 2 = ?f b"
         by (simp add: field_simps atLeastAtMost_def indicator_inter_arith)
     qed
diff -r 9ecc78bcf1ef -r 06bce659d41b src/HOL/Probability/Levy.thy
--- a/src/HOL/Probability/Levy.thy	Fri Apr 13 17:25:02 2018 +0200
+++ b/src/HOL/Probability/Levy.thy	Fri Apr 13 17:00:57 2018 +0100
@@ -90,12 +90,12 @@
     { fix x
       have 1: "complex_interval_lebesgue_integrable lborel u v (\<lambda>t. ?f t x)" for u v :: real
         using Levy_Inversion_aux2[of "x - b" "x - a"]
-        apply (simp add: interval_lebesgue_integrable_def del: times_divide_eq_left)
+        apply (simp add: interval_lebesgue_integrable_def set_integrable_def del: times_divide_eq_left)
         apply (intro integrableI_bounded_set_indicator[where B="b - a"] conjI impI)
         apply (auto intro!: AE_I [of _ _ "{0}"] simp: assms)
         done
       have "(CLBINT t. ?f' (t, x)) = (CLBINT t=-T..T. ?f t x)"
-        using \<open>T \<ge> 0\<close> by (simp add: interval_lebesgue_integral_def)
+        using \<open>T \<ge> 0\<close> by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_def)
       also have "\<dots> = (CLBINT t=-T..(0 :: real). ?f t x) + (CLBINT t=(0 :: real)..T. ?f t x)"
           (is "_ = _ + ?t")
         using 1 by (intro interval_integral_sum[symmetric]) (simp add: min_absorb1 max_absorb2 \<open>T \<ge> 0\<close>)
@@ -130,7 +130,7 @@
     } note main_eq = this
     have "(CLBINT t=-T..T. ?F t * \<phi> t) =
       (CLBINT t. (CLINT x | M. ?F t * iexp (t * x) * indicator {-T<..<T} t))"
-      using \<open>T \<ge> 0\<close> unfolding \<phi>_def char_def interval_lebesgue_integral_def
+      using \<open>T \<ge> 0\<close> unfolding \<phi>_def char_def interval_lebesgue_integral_def set_lebesgue_integral_def
       by (auto split: split_indicator intro!: Bochner_Integration.integral_cong)
     also have "\<dots> = (CLBINT t. (CLINT x | M. ?f' (t, x)))"
       by (auto intro!: Bochner_Integration.integral_cong simp: field_simps exp_diff exp_minus split: split_indicator)
@@ -323,6 +323,7 @@
       by (rule Mn.integrable_const_bound [where B = 1], auto)
     have Mn3: "set_integrable (M n \<Otimes>\<^sub>M lborel) (UNIV \<times> {- u..u}) (\<lambda>a. 1 - exp (\<i> * complex_of_real (snd a * fst a)))"
       using \<open>0 < u\<close>
+      unfolding set_integrable_def
       by (intro integrableI_bounded_set_indicator [where B="2"])
          (auto simp: lborel.emeasure_pair_measure_Times ennreal_mult_less_top not_less top_unique
                split: split_indicator
@@ -331,9 +332,10 @@
         (CLBINT t:{-u..u}. (CLINT x | M n. 1 - iexp (t * x)))"
       unfolding char_def by (rule set_lebesgue_integral_cong, auto simp del: of_real_mult)
     also have "\<dots> = (CLBINT t. (CLINT x | M n. indicator {-u..u} t *\<^sub>R (1 - iexp (t * x))))"
+      unfolding set_lebesgue_integral_def
       by (rule Bochner_Integration.integral_cong) (auto split: split_indicator)
     also have "\<dots> = (CLINT x | M n. (CLBINT t:{-u..u}. 1 - iexp (t * x)))"
-      using Mn3 by (subst P.Fubini_integral) (auto simp: indicator_times split_beta')
+      using Mn3 by (subst P.Fubini_integral) (auto simp: indicator_times split_beta' set_integrable_def set_lebesgue_integral_def)
     also have "\<dots> = (CLINT x | M n. (if x = 0 then 0 else 2 * (u  - sin (u * x) / x)))"
       using \<open>u > 0\<close> by (intro Bochner_Integration.integral_cong, auto simp add: * simp del: of_real_mult)
     also have "\<dots> = (LINT x | M n. (if x = 0 then 0 else 2 * (u  - sin (u * x) / x)))"
@@ -343,9 +345,12 @@
     also have "\<dots> \<ge> (LINT x : {x. abs x \<ge> 2 / u} | M n. u)"
     proof -
       have "complex_integrable (M n) (\<lambda>x. CLBINT t:{-u..u}. 1 - iexp (snd (x, t) * fst (x, t)))"
-        using Mn3 by (intro P.integrable_fst) (simp add: indicator_times split_beta')
+        using Mn3 unfolding set_integrable_def set_lebesgue_integral_def
+        by (intro P.integrable_fst) (simp add: indicator_times split_beta')
       hence "complex_integrable (M n) (\<lambda>x. if x = 0 then 0 else 2 * (u  - sin (u * x) / x))"
-        using \<open>u > 0\<close> by (subst integrable_cong) (auto simp add: * simp del: of_real_mult)
+        using \<open>u > 0\<close>
+        unfolding set_integrable_def
+        by (subst integrable_cong) (auto simp add: * simp del: of_real_mult)
       hence **: "integrable (M n) (\<lambda>x. if x = 0 then 0 else 2 * (u  - sin (u * x) / x))"
         unfolding complex_of_real_integrable_eq .
       have "2 * sin x \<le> x" if "2 \<le> x" for x :: real
@@ -355,13 +360,13 @@
       moreover have "x < 0 \<Longrightarrow> x \<le> sin x" for x :: real
         using sin_x_le_x[of "-x"] by simp
       ultimately show ?thesis
-        using \<open>u > 0\<close>
+        using \<open>u > 0\<close> unfolding set_lebesgue_integral_def
         by (intro integral_mono [OF _ **])
            (auto simp: divide_simps sin_x_le_x mult.commute[of u] mult_neg_pos top_unique less_top[symmetric]
                  split: split_indicator)
     qed
-    also (xtrans) have "(LINT x : {x. abs x \<ge> 2 / u} | M n. u) =
-        u * measure (M n) {x. abs x \<ge> 2 / u}"
+    also (xtrans) have "(LINT x : {x. abs x \<ge> 2 / u} | M n. u) = u * measure (M n) {x. abs x \<ge> 2 / u}"
+      unfolding set_lebesgue_integral_def
       by (simp add: Mn.emeasure_eq_measure)
     finally show "Re (CLBINT t:{-u..u}. 1 - char (M n) t) \<ge> u * measure (M n) {x. abs x \<ge> 2 / u}" .
   qed
@@ -380,13 +385,16 @@
     have 1: "\<And>x. cmod (1 - char M' x) \<le> 2"
       by (rule order_trans [OF norm_triangle_ineq4], auto simp add: M'.cmod_char_le_1)
     then have 2: "\<And>u v. complex_set_integrable lborel {u..v} (\<lambda>x. 1 - char M' x)"
+      unfolding set_integrable_def
       by (intro integrableI_bounded_set_indicator[where B=2]) (auto simp: emeasure_lborel_Icc_eq)
-    have 3: "\<And>u v. set_integrable lborel {u..v} (\<lambda>x. cmod (1 - char M' x))"
+    have 3: "\<And>u v. integrable lborel (\<lambda>x. indicat_real {u..v} x *\<^sub>R cmod (1 - char M' x))"
       by (intro borel_integrable_compact[OF compact_Icc] continuous_at_imp_continuous_on
                 continuous_intros ballI M'.isCont_char continuous_intros)
     have "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> LBINT t:{-d/2..d/2}. cmod (1 - char M' t)"
+      unfolding set_lebesgue_integral_def
       using integral_norm_bound[of _ "\<lambda>x. indicator {u..v} x *\<^sub>R (1 - char M' x)" for u v] by simp
     also have 4: "\<dots> \<le> LBINT t:{-d/2..d/2}. \<epsilon> / 4"
+      unfolding set_lebesgue_integral_def
       apply (rule integral_mono [OF 3])
        apply (simp add: emeasure_lborel_Icc_eq)
       apply (case_tac "x \<in> {-d/2..d/2}")
@@ -397,11 +405,12 @@
       using d0 apply auto
       done
     also from d0 4 have "\<dots> = d * \<epsilon> / 4"
-      by simp
+      unfolding set_lebesgue_integral_def by simp
     finally have bound: "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> d * \<epsilon> / 4" .
     have "cmod (1 - char (M n) x) \<le> 2" for n x
       by (rule order_trans [OF norm_triangle_ineq4], auto simp add: Mn.cmod_char_le_1)
     then have "(\<lambda>n. CLBINT t:{-d/2..d/2}. 1 - char (M n) t) \<longlonglongrightarrow> (CLBINT t:{-d/2..d/2}. 1 - char M' t)"
+      unfolding set_lebesgue_integral_def
       apply (intro integral_dominated_convergence[where w="\<lambda>x. indicator {-d/2..d/2} x *\<^sub>R 2"])
       apply (auto intro!: char_conv tendsto_intros
                   simp: emeasure_lborel_Icc_eq
diff -r 9ecc78bcf1ef -r 06bce659d41b src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Apr 13 17:25:02 2018 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Apr 13 17:00:57 2018 +0100
@@ -541,7 +541,7 @@
   shows   "infsetsum (pmf p) A = 1"
 proof -
   have "infsetsum (pmf p) A = lebesgue_integral (count_space UNIV) (pmf p)"
-    using assms unfolding infsetsum_altdef
+    using assms unfolding infsetsum_altdef set_lebesgue_integral_def
     by (intro Bochner_Integration.integral_cong) (auto simp: indicator_def set_pmf_eq)
   also have "\<dots> = 1"
     by (subst integral_eq_nn_integral) (auto simp: nn_integral_pmf)
diff -r 9ecc78bcf1ef -r 06bce659d41b src/HOL/Probability/Sinc_Integral.thy
--- a/src/HOL/Probability/Sinc_Integral.thy	Fri Apr 13 17:25:02 2018 +0200
+++ b/src/HOL/Probability/Sinc_Integral.thy	Fri Apr 13 17:00:57 2018 +0100
@@ -33,12 +33,12 @@
 lemma integrable_I0i_exp_mscale: "0 < (u::real) \<Longrightarrow> set_integrable lborel {0 <..} (\<lambda>x. exp (-(x * u)))"
   using lborel_integrable_real_affine_iff[of u "\<lambda>x. indicator {0 <..} x *\<^sub>R exp (- x)" 0]
         has_bochner_integral_I0i_power_exp_m[of 0]
-  by (simp add: indicator_def zero_less_mult_iff mult_ac integrable.intros)
+  by (simp add: indicator_def zero_less_mult_iff mult_ac integrable.intros set_integrable_def)
 
 lemma LBINT_I0i_exp_mscale: "0 < (u::real) \<Longrightarrow> LBINT x=0..\<infinity>. exp (-(x * u)) = 1 / u"
   using lborel_integral_real_affine[of u "\<lambda>x. indicator {0<..} x *\<^sub>R exp (- x)" 0]
         has_bochner_integral_I0i_power_exp_m[of 0]
-  by (auto simp: indicator_def zero_less_mult_iff interval_lebesgue_integral_0_infty field_simps
+  by (auto simp: indicator_def zero_less_mult_iff interval_lebesgue_integral_0_infty set_lebesgue_integral_def field_simps
            dest!: has_bochner_integral_integral_eq)
 
 lemma LBINT_I0c_exp_mscale_sin:
@@ -83,11 +83,11 @@
   show "LBINT x=-\<infinity>..\<infinity>. inverse (1 + x^2) = pi"
     by (subst interval_integral_substitution_nonneg[of "-pi/2" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"])
        (auto intro: derivative_eq_intros 1 2 filterlim_tan_at_right
-             simp add: ereal_tendsto_simps filterlim_tan_at_left add_nonneg_eq_0_iff)
+             simp add: ereal_tendsto_simps filterlim_tan_at_left add_nonneg_eq_0_iff set_integrable_def)
   show "set_integrable lborel (einterval (-\<infinity>) \<infinity>) (\<lambda>x. inverse (1 + x^2))"
     by (subst interval_integral_substitution_nonneg[of "-pi/2" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"])
        (auto intro: derivative_eq_intros 1 2 filterlim_tan_at_right
-             simp add: ereal_tendsto_simps filterlim_tan_at_left add_nonneg_eq_0_iff)
+             simp add: ereal_tendsto_simps filterlim_tan_at_left add_nonneg_eq_0_iff set_integrable_def)
 qed
 
 lemma
@@ -103,12 +103,12 @@
   show "LBINT x=0..\<infinity>. 1 / (1 + x^2) = pi / 2"
     by (subst interval_integral_substitution_nonneg[of "0" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"])
        (auto intro: derivative_eq_intros 1 2 tendsto_eq_intros
-             simp add: ereal_tendsto_simps filterlim_tan_at_left zero_ereal_def add_nonneg_eq_0_iff)
+             simp add: ereal_tendsto_simps filterlim_tan_at_left zero_ereal_def add_nonneg_eq_0_iff set_integrable_def)
   show "interval_lebesgue_integrable lborel 0 \<infinity> (\<lambda>x. 1 / (1 + x^2))"
     unfolding interval_lebesgue_integrable_def
     by (subst interval_integral_substitution_nonneg[of "0" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"])
        (auto intro: derivative_eq_intros 1 2 tendsto_eq_intros
-             simp add: ereal_tendsto_simps filterlim_tan_at_left zero_ereal_def add_nonneg_eq_0_iff)
+             simp add: ereal_tendsto_simps filterlim_tan_at_left zero_ereal_def add_nonneg_eq_0_iff set_integrable_def)
 qed
 
 section \<open>The sinc function, and the sine integral (Si)\<close>
@@ -212,10 +212,12 @@
   have int: "set_integrable lborel {0<..} (\<lambda>x. exp (- x) * (x + 1) :: real)"
     unfolding distrib_left
     using has_bochner_integral_I0i_power_exp_m[of 0] has_bochner_integral_I0i_power_exp_m[of 1]
-    by (intro set_integral_add) (auto dest!: integrable.intros simp: ac_simps)
+    by (intro set_integral_add) (auto dest!: integrable.intros simp: ac_simps set_integrable_def)
 
   have "((\<lambda>t::real. LBINT x:{0<..}. ?F x t) \<longlongrightarrow> LBINT x::real:{0<..}. 0) at_top"
-  proof (rule integral_dominated_convergence_at_top[OF _ _ int], simp_all del: abs_divide split: split_indicator)
+    unfolding set_lebesgue_integral_def
+  proof (rule integral_dominated_convergence_at_top[OF _ _ int [unfolded set_integrable_def]], 
+         simp_all del: abs_divide split: split_indicator)
     have *: "0 < x \<Longrightarrow> \<bar>x * sin t + cos t\<bar> / (1 + x\<^sup>2) \<le> (x * 1 + 1) / 1" for x t :: real
       by (intro frac_le abs_triangle_ineq[THEN order_trans] add_mono)
          (auto simp add: abs_mult simp del: mult_1_right intro!: mult_mono)
@@ -241,7 +243,7 @@
     qed
   qed
   then show "((\<lambda>t. (LBINT x=0..\<infinity>. exp (-(x * t)) * (x * sin t + cos t) / (1 + x^2))) \<longlongrightarrow> 0) at_top"
-    by (simp add: interval_lebesgue_integral_0_infty)
+    by (simp add: interval_lebesgue_integral_0_infty set_lebesgue_integral_def)
 qed
 
 lemma Si_at_top_integrable:
@@ -258,10 +260,10 @@
   have "set_integrable lborel {0<..} (\<lambda>x. (exp (- x) * x) * (sin t/t) + exp (- x) * cos t)"
     using has_bochner_integral_I0i_power_exp_m[of 0] has_bochner_integral_I0i_power_exp_m[of 1]
     by (intro set_integral_add set_integrable_mult_left)
-       (auto dest!: integrable.intros simp: ac_simps)
-  from lborel_integrable_real_affine[OF this, of t 0]
+       (auto dest!: integrable.intros simp: ac_simps set_integrable_def)
+  from lborel_integrable_real_affine[OF this [unfolded set_integrable_def], of t 0]
   show ?thesis
-    unfolding interval_lebesgue_integral_0_infty
+    unfolding interval_lebesgue_integral_0_infty set_integrable_def
     by (rule Bochner_Integration.integrable_bound) (auto simp: field_simps * split: split_indicator)
 qed
 
@@ -275,9 +277,10 @@
       unfolding Si_def using \<open>0 \<le> t\<close>
       by (intro interval_integral_discrete_difference[where X="{0}"]) (auto simp: LBINT_I0i_exp_mscale)
     also have "\<dots> = LBINT x. (LBINT u=ereal 0..\<infinity>. indicator {0 <..< t} x *\<^sub>R sin x * exp (-(u * x)))"
-      using \<open>0\<le>t\<close> by (simp add: zero_ereal_def interval_lebesgue_integral_le_eq mult_ac)
+      using \<open>0\<le>t\<close> by (simp add: zero_ereal_def interval_lebesgue_integral_le_eq mult_ac set_lebesgue_integral_def)
     also have "\<dots> = LBINT x. (LBINT u. indicator ({0<..} \<times> {0 <..< t}) (u, x) *\<^sub>R (sin x * exp (-(u * x))))"
-      by (subst interval_integral_Ioi) (simp_all add: indicator_times ac_simps)
+      apply (subst interval_integral_Ioi)
+      unfolding set_lebesgue_integral_def  by(simp_all add: indicator_times ac_simps )
     also have "\<dots> = LBINT u. (LBINT x. indicator ({0<..} \<times> {0 <..< t}) (u, x) *\<^sub>R (sin x * exp (-(u * x))))"
     proof (intro lborel_pair.Fubini_integral[symmetric] lborel_pair.Fubini_integrable)
       show "(\<lambda>(x, y). indicator ({0<..} \<times> {0<..<t}) (y, x) *\<^sub>R (sin x * exp (- (y * x))))
@@ -293,7 +296,7 @@
           by (intro Bochner_Integration.integral_cong) (auto split: split_indicator simp: abs_mult)
         also have "\<dots> = \<bar>sin x\<bar> * indicator {0<..<t} x * (LBINT y=0..\<infinity>.  exp (- (y * x)))"
           by (cases "x > 0")
-             (auto simp: field_simps interval_lebesgue_integral_0_infty split: split_indicator)
+             (auto simp: field_simps interval_lebesgue_integral_0_infty set_lebesgue_integral_def split: split_indicator)
         also have "\<dots> = \<bar>sin x\<bar> * indicator {0<..<t} x * (1 / x)"
           by (cases "x > 0") (auto simp add: LBINT_I0i_exp_mscale)
         also have "\<dots> = indicator {0..t} x *\<^sub>R \<bar>sinc x\<bar>"
@@ -301,7 +304,7 @@
         finally show "indicator {0..t} x *\<^sub>R abs (sinc x) = LBINT y. norm (?f (x, y))"
           by simp
       qed
-      moreover have "set_integrable lborel {0 .. t} (\<lambda>x. abs (sinc x))"
+      moreover have "integrable lborel (\<lambda>x. indicat_real {0..t} x *\<^sub>R \<bar>sinc x\<bar>)"
         by (auto intro!: borel_integrable_compact continuous_intros simp del: real_scaleR_def)
       ultimately show "integrable lborel (\<lambda>x. LBINT y. norm (?f (x, y)))"
         by (rule integrable_cong_AE_imp[rotated 2]) simp
@@ -309,11 +312,11 @@
       have "0 < x \<Longrightarrow> set_integrable lborel {0<..} (\<lambda>y. sin x * exp (- (y * x)))" for x :: real
           by (intro set_integrable_mult_right integrable_I0i_exp_mscale)
       then show "AE x in lborel. integrable lborel (\<lambda>y. ?f (x, y))"
-        by (intro AE_I2) (auto simp: indicator_times split: split_indicator)
+        by (intro AE_I2) (auto simp: indicator_times set_integrable_def split: split_indicator)
     qed
     also have "... = LBINT u=0..\<infinity>. (LBINT x=0..t. exp (-(u * x)) * sin x)"
       using \<open>0\<le>t\<close>
-      by (auto simp: interval_lebesgue_integral_def zero_ereal_def ac_simps
+      by (auto simp: interval_lebesgue_integral_def set_lebesgue_integral_def zero_ereal_def ac_simps
                split: split_indicator intro!: Bochner_Integration.integral_cong)
     also have "\<dots> = LBINT u=0..\<infinity>. 1 / (1 + u\<^sup>2) - 1 / (1 + u\<^sup>2) * (exp (- (u * t)) * (u * sin t + cos t))"
       by (auto simp: divide_simps LBINT_I0c_exp_mscale_sin intro!: interval_integral_cong)
@@ -369,12 +372,12 @@
     hence "LBINT x. indicator {0<..<T} x * sin (x * \<theta>) / x =
         LBINT x. indicator {0<..<T * \<theta>} x * sin x / x"
       using assms \<open>0 < \<theta>\<close> unfolding interval_lebesgue_integral_def einterval_eq zero_ereal_def
-        by (auto simp: ac_simps)
+        by (auto simp: ac_simps set_lebesgue_integral_def)
   } note aux1 = this
   { assume "0 > \<theta>"
     have [simp]: "integrable lborel (\<lambda>x. sin (x * \<theta>) * indicator {0<..<T} x / x)"
       using integrable_sinc' [of T \<theta>] assms
-      by (simp add: interval_lebesgue_integrable_def ac_simps)
+      by (simp add: interval_lebesgue_integrable_def set_integrable_def ac_simps)
     have "(LBINT t=ereal 0..T. sin (t * -\<theta>) / t) = (LBINT t=ereal 0..T. -\<theta> *\<^sub>R sinc (t * -\<theta>))"
       by (rule interval_integral_discrete_difference[of "{0}"]) auto
     also have "\<dots> = (LBINT t=ereal (0 * -\<theta>)..T * -\<theta>. sinc t)"
@@ -388,10 +391,10 @@
     hence "LBINT x. indicator {0<..<T} x * sin (x * \<theta>) / x =
        - (LBINT x. indicator {0<..<- (T * \<theta>)} x * sin x / x)"
       using assms \<open>0 > \<theta>\<close> unfolding interval_lebesgue_integral_def einterval_eq zero_ereal_def
-        by (auto simp add: field_simps mult_le_0_iff split: if_split_asm)
+        by (auto simp add: field_simps mult_le_0_iff set_lebesgue_integral_def split: if_split_asm)
   } note aux2 = this
   show ?thesis
-    using assms unfolding Si_def interval_lebesgue_integral_def sgn_real_def einterval_eq zero_ereal_def
+    using assms unfolding Si_def interval_lebesgue_integral_def set_lebesgue_integral_def sgn_real_def einterval_eq zero_ereal_def
     apply auto
     apply (erule aux1)
     apply (rule aux2)