# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1504024871 -3600
# Node ID 507a42c0a0ffc599c9d35ec0e372af13e324bbac
# Parent  1f955cdd9e5901606444ce84f58a70e53ea75005
last-minute integration unscrambling

diff -r 1f955cdd9e59 -r 507a42c0a0ff src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Aug 28 22:32:22 2017 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Tue Aug 29 17:41:11 2017 +0100
@@ -314,7 +314,7 @@
     then have "(\<lambda>x. f x * indicator \<Omega> x) integrable_on \<Omega>"
       by (auto simp: integrable_on_def cong: has_integral_cong)
     then have "(\<lambda>x. f x * indicator \<Omega> x) integrable_on (\<Omega> \<union> B n)"
-      by (rule integrable_on_superset[rotated 2]) auto
+      by (rule integrable_on_superset) auto
     then have "(\<lambda>x. f x * indicator \<Omega> x) integrable_on B n"
       unfolding B_def by (rule integrable_on_subcbox) auto
     then show "(\<lambda>x. f x * indicator \<Omega> x) \<in> lebesgue_on \<Omega>' \<rightarrow>\<^sub>M borel"
@@ -2717,7 +2717,7 @@
   note intl = has_integral_integrable[OF int]
   have af: "f absolutely_integrable_on (closure S)"
     using nonneg
-    by (intro absolutely_integrable_onI intl integrable_eq[OF _ intl]) simp
+    by (intro absolutely_integrable_onI intl integrable_eq[OF intl]) simp
   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)"
diff -r 1f955cdd9e59 -r 507a42c0a0ff src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Aug 28 22:32:22 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Aug 29 17:41:11 2017 +0100
@@ -716,7 +716,7 @@
   using assms(1)
   by auto
 
-lemma integrable_eq: "(\<And>x. x \<in> s \<Longrightarrow> f x = g x) \<Longrightarrow> f integrable_on s \<Longrightarrow> g integrable_on s"
+lemma integrable_eq: "\<lbrakk>f integrable_on s; \<And>x. x \<in> s \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> g integrable_on s"
   unfolding integrable_on_def
   using has_integral_eq[of s f g] has_integral_eq by blast
 
@@ -2615,79 +2615,70 @@
     and "Inf {a..b} = a"
   using assms by auto
 
-lemma fundamental_theorem_of_calculus:
+theorem fundamental_theorem_of_calculus:
   fixes f :: "real \<Rightarrow> 'a::banach"
-  assumes "a \<le> b"
-    and vecd: "\<forall>x\<in>{a..b}. (f has_vector_derivative f' x) (at x within {a..b})"
+  assumes "a \<le> b" 
+      and vecd: "\<And>x. x \<in> {a..b} \<Longrightarrow> (f has_vector_derivative f' x) (at x within {a..b})"
   shows "(f' has_integral (f b - f a)) {a..b}"
   unfolding has_integral_factor_content box_real[symmetric]
 proof safe
   fix e :: real
   assume "e > 0"
-  then have "\<forall>x. \<exists>d>0.
-         x \<in> {a..b} \<longrightarrow>
-         (\<forall>y\<in>{a..b}.
-             norm (y-x) < d \<longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e * norm (y-x))"
+  then have "\<forall>x. \<exists>d>0. x \<in> {a..b} \<longrightarrow>
+         (\<forall>y\<in>{a..b}. norm (y-x) < d \<longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e * norm (y-x))"
     using vecd[unfolded has_vector_derivative_def has_derivative_within_alt] by blast
   then obtain d where d: "\<And>x. 0 < d x"
                  "\<And>x y. \<lbrakk>x \<in> {a..b}; y \<in> {a..b}; norm (y-x) < d x\<rbrakk>
                         \<Longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e * norm (y-x)"
-    by metis
-  
+    by metis  
   show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
     norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content (cbox a b))"
-    apply (rule_tac x="\<lambda>x. ball x (d x)" in exI)
-    apply safe
-    apply (rule gauge_ball_dependent)
-    apply rule
-    apply (rule d(1))
-  proof -
+  proof (rule exI, safe)
+    show "gauge (\<lambda>x. ball x (d x))"
+      using d(1) gauge_ball_dependent by blast
+  next
     fix p
-    assume as: "p tagged_division_of cbox a b" "(\<lambda>x. ball x (d x)) fine p"
-    show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content (cbox a b)"
-      unfolding content_real[OF assms(1), simplified box_real[symmetric]] additive_tagged_division_1[OF assms(1) as(1)[simplified box_real],of f,symmetric]
-      unfolding additive_tagged_division_1[OF assms(1) as(1)[simplified box_real],of "\<lambda>x. x",symmetric]
-      unfolding sum_distrib_left
-      defer
-      unfolding sum_subtractf[symmetric]
+    assume ptag: "p tagged_division_of cbox a b" and finep: "(\<lambda>x. ball x (d x)) fine p"
+    have ba: "b - a = (\<Sum>(x,K)\<in>p. Sup K - Inf K)" "f b - f a = (\<Sum>(x,K)\<in>p. f(Sup K) - f(Inf K))"
+      using additive_tagged_division_1[where f= "\<lambda>x. x"] additive_tagged_division_1[where f= f]
+            \<open>a \<le> b\<close> ptag by auto
+    have "norm (\<Sum>(x, K) \<in> p. (content K *\<^sub>R f' x) - (f (Sup K) - f (Inf K)))
+          \<le> (\<Sum>n\<in>p. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k))"
     proof (rule sum_norm_le,safe)
-      fix x k
-      assume "(x, k) \<in> p"
-      note xk = tagged_division_ofD(2-4)[OF as(1) this]
-      then obtain u v where k: "k = cbox u v" by blast
-      have *: "u \<le> v"
-        using xk unfolding k by auto
-      have ball: "\<forall>xa\<in>k. xa \<in> ball x (d x)"
-        using as(2)[unfolded fine_def,rule_format,OF \<open>(x,k)\<in>p\<close>,unfolded split_conv subset_eq] .
-      have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) \<le>
-        norm (f u - f x - (u - x) *\<^sub>R f' x) + norm (f v - f x - (v - x) *\<^sub>R f' x)"
-        apply (rule order_trans[OF _ norm_triangle_ineq4])
-        apply (rule eq_refl)
-        apply (rule arg_cong[where f=norm])
-        unfolding scaleR_diff_left
-        apply (auto simp add:algebra_simps)
-        done
+      fix x K
+      assume "(x, K) \<in> p"
+      then have "x \<in> K" and kab: "K \<subseteq> cbox a b"
+        using ptag by blast+
+      then obtain u v where k: "K = cbox u v" and "x \<in> K" and kab: "K \<subseteq> cbox a b"
+        using ptag \<open>(x, K) \<in> p\<close> by auto 
+      have "u \<le> v"
+        using \<open>x \<in> K\<close> unfolding k by auto
+      have ball: "\<forall>y\<in>K. y \<in> ball x (d x)"
+        using finep \<open>(x, K) \<in> p\<close> by blast
+      have "u \<in> K" "v \<in> K"
+        by (simp_all add: \<open>u \<le> v\<close> k)
+      have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) = norm (f u - f x - (u - x) *\<^sub>R f' x - (f v - f x - (v - x) *\<^sub>R f' x))"
+        by (auto simp add: algebra_simps)
+      also have "... \<le> norm (f u - f x - (u - x) *\<^sub>R f' x) + norm (f v - f x - (v - x) *\<^sub>R f' x)"
+        by (rule norm_triangle_ineq4)
+      finally have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) \<le>
+        norm (f u - f x - (u - x) *\<^sub>R f' x) + norm (f v - f x - (v - x) *\<^sub>R f' x)" .
       also have "\<dots> \<le> e * norm (u - x) + e * norm (v - x)"
-        apply (rule add_mono)
-        apply (rule d(2)[of "x" "u",unfolded o_def])
-        prefer 4
-        apply (rule d(2)[of "x" "v",unfolded o_def])
-        using ball[rule_format,of u] ball[rule_format,of v]
-        using xk(1-2)
-        unfolding k subset_eq
-        apply (auto simp add:dist_real_def)
-        done
-      also have "\<dots> \<le> e * (Sup k - Inf k)"
-        unfolding k interval_bounds_real[OF *]
-        using xk(1)
-        unfolding k
-        by (auto simp add: dist_real_def field_simps)
-      finally show "norm (content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \<le>
-        e * (Sup k - Inf k)"
-        unfolding box_real k interval_bounds_real[OF *] content_real[OF *]
-          interval_upperbound_real interval_lowerbound_real
-          .
+      proof (rule add_mono)
+        show "norm (f u - f x - (u - x) *\<^sub>R f' x) \<le> e * norm (u - x)"
+          apply (rule d(2)[of x u])
+          using \<open>x \<in> K\<close> kab \<open>u \<in> K\<close> ball dist_real_def by (auto simp add:dist_real_def)
+        show "norm (f v - f x - (v - x) *\<^sub>R f' x) \<le> e * norm (v - x)"
+          apply (rule d(2)[of x v])
+          using \<open>x \<in> K\<close> kab \<open>v \<in> K\<close> ball dist_real_def by (auto simp add:dist_real_def)
+      qed
+      also have "\<dots> \<le> e * (Sup K - Inf K)"
+        using \<open>x \<in> K\<close> by (auto simp: k interval_bounds_real[OF \<open>u \<le> v\<close>] field_simps)
+      finally show "norm (content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))) \<le> e * (Sup K - Inf K)"
+        using \<open>u \<le> v\<close> by (simp add: k)
     qed
+    with \<open>a \<le> b\<close> show "norm ((\<Sum>(x, K)\<in>p. content K *\<^sub>R f' x) - (f b - f a)) \<le> e * content (cbox a b)"
+      by (auto simp: ba split_def sum_subtractf [symmetric] sum_distrib_left)
   qed
 qed
 
@@ -2697,7 +2688,7 @@
   shows "((\<lambda>x. x) has_integral (b\<^sup>2 - a\<^sup>2)/2) {a..b}"
 proof -
   have "((\<lambda>x. x) has_integral inverse 2 * b\<^sup>2 - inverse 2 * a\<^sup>2) {a..b}"
-    apply (rule fundamental_theorem_of_calculus [OF assms], clarify)
+    apply (rule fundamental_theorem_of_calculus [OF assms])
     unfolding power2_eq_square
     by (rule derivative_eq_intros | simp)+
   then show ?thesis
@@ -3144,10 +3135,10 @@
     using  antiderivative_continuous[OF assms] by metis
   have "(f has_integral g v - g u) {u..v}" if "u \<in> {a..b}" "v \<in> {a..b}" "u \<le> v" for u v
   proof -
-    have "\<forall>x\<in>cbox u v. (g has_vector_derivative f x) (at x within cbox u v)"
+    have "\<And>x. x \<in> cbox u v \<Longrightarrow> (g has_vector_derivative f x) (at x within cbox u v)"
       by (meson g has_vector_derivative_within_subset interval_subset_is_interval is_interval_closed_interval subsetCE that(1) that(2))
     then show ?thesis
-      by (simp add: fundamental_theorem_of_calculus that(3))
+      by (metis box_real(2) that(3) fundamental_theorem_of_calculus)
   qed
   then show ?thesis
     using that by blast
@@ -3158,39 +3149,30 @@
 
 lemma has_integral_twiddle:
   assumes "0 < r"
-    and "\<forall>x. h(g x) = x"
-    and "\<forall>x. g(h x) = x"
+    and hg: "\<And>x. h(g x) = x"
+    and gh: "\<And>x. g(h x) = x"
     and contg: "\<And>x. continuous (at x) g"
-    and "\<forall>u v. \<exists>w z. g ` cbox u v = cbox w z"
-    and h: "\<forall>u v. \<exists>w z. h ` cbox u v = cbox w z"
-    and "\<forall>u v. content(g ` cbox u v) = r * content (cbox u v)"
+    and g: "\<And>u v. \<exists>w z. g ` cbox u v = cbox w z"
+    and h: "\<And>u v. \<exists>w z. h ` cbox u v = cbox w z"
+    and r: "\<And>u v. content(g ` cbox u v) = r * content (cbox u v)"
     and intfi: "(f has_integral i) (cbox a b)"
   shows "((\<lambda>x. f(g x)) has_integral (1 / r) *\<^sub>R i) (h ` cbox a b)"
-proof -
-  show ?thesis when *: "cbox a b \<noteq> {} \<Longrightarrow> ?thesis"
-    apply cases
-    defer
-    apply (rule *)
-    apply assumption
-  proof goal_cases
-    case prems: 1
-    then show ?thesis
-      unfolding prems assms(8)[unfolded prems has_integral_empty_eq] by auto
-  qed
-  assume "cbox a b \<noteq> {}"
+proof (cases "cbox a b = {}")
+  case True
+  then show ?thesis 
+    using intfi by auto
+next
+  case False
   obtain w z where wz: "h ` cbox a b = cbox w z"
     using h by blast
   have inj: "inj g" "inj h"
-    apply (metis assms(2) injI)
-    by (metis assms(3) injI)
+    using hg gh injI by metis+
   from h obtain ha hb where h_eq: "h ` cbox a b = cbox ha hb" by blast
-  show ?thesis
-    unfolding h_eq has_integral
-    unfolding h_eq[symmetric]
-  proof safe
-    fix e :: real
-    assume e: "e > 0"
-    with \<open>0 < r\<close> have "e * r > 0" by simp
+  have "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of h ` cbox a b \<and> d fine p 
+              \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e)"
+    if "e > 0" for e
+  proof -
+    have "e * r > 0" using that \<open>0 < r\<close> by simp
     with intfi[unfolded has_integral]
     obtain d where d: "gauge d"
                    "\<And>p. p tagged_division_of cbox a b \<and> d fine p 
@@ -3199,69 +3181,49 @@
     define d' where "d' x = {y. g y \<in> d (g x)}" for x
     have d': "\<And>x. d' x = {y. g y \<in> (d (g x))}"
       unfolding d'_def ..
-    show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of h ` cbox a b \<and> d fine p 
-              \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e)"
+    show ?thesis
     proof (rule_tac x=d' in exI, safe)
       show "gauge d'"
-        using d(1)
-        unfolding gauge_def d'
-        using continuous_open_preimage_univ[OF _ contg]
-        by auto
+        using d(1) continuous_open_preimage_univ[OF _ contg] by (auto simp: gauge_def d')
+    next
       fix p
-      assume as: "p tagged_division_of h ` cbox a b" "d' fine p"
-      note p = tagged_division_ofD[OF as(1)]
-      have "(\<lambda>(x, k). (g x, g ` k)) ` p tagged_division_of (cbox a b) \<and> d fine (\<lambda>(x, k). (g x, g ` k)) ` p"
+      assume ptag: "p tagged_division_of h ` cbox a b" and finep: "d' fine p"
+      note p = tagged_division_ofD[OF ptag]
+      have gab: "g y \<in> cbox a b" if "y \<in> K" "(x, K) \<in> p" for x y K
+        by (metis hg inj(2) inj_image_mem_iff p(3) subsetCE that that)
+      have gimp: "(\<lambda>(x,K). (g x, g ` K)) ` p tagged_division_of (cbox a b) \<and> 
+                  d fine (\<lambda>(x, k). (g x, g ` k)) ` p"
         unfolding tagged_division_of
       proof safe
         show "finite ((\<lambda>(x, k). (g x, g ` k)) ` p)"
-          using as by auto
+          using ptag by auto
         show "d fine (\<lambda>(x, k). (g x, g ` k)) ` p"
-          using as(2) unfolding fine_def d' by auto
+          using finep unfolding fine_def d' by auto
+      next
         fix x k
-        assume xk[intro]: "(x, k) \<in> p"
+        assume xk: "(x, k) \<in> p"
         show "g x \<in> g ` k"
           using p(2)[OF xk] by auto
         show "\<exists>u v. g ` k = cbox u v"
           using p(4)[OF xk] using assms(5-6) by auto
-        {
-          fix y
-          assume "y \<in> k"
-          then show "g y \<in> cbox a b" "g y \<in> cbox a b"
-            using p(3)[OF xk,unfolded subset_eq,rule_format,of "h (g y)"]
-            using assms(2)[rule_format,of y]
-            unfolding inj_image_mem_iff[OF inj(2)]
-            by auto
-        }
-        fix x' k'
-        assume xk': "(x', k') \<in> p"
-        fix z
-        assume z: "z \<in> interior (g ` k)" "z \<in> interior (g ` k')"
-        have same: "(x, k) = (x', k')"
-          apply -
-          apply (rule ccontr)
-          apply (drule p(5)[OF xk xk'])
-        proof -
-          assume as: "interior k \<inter> interior k' = {}"
-          have "z \<in> g ` (interior k \<inter> interior k')"
-            using interior_image_subset[OF \<open>inj g\<close> contg] z
+        fix x' K' u
+        assume xk': "(x', K') \<in> p" and u: "u \<in> interior (g ` k)" "u \<in> interior (g ` K')"
+        have "interior k \<inter> interior K' \<noteq> {}"
+        proof 
+          assume "interior k \<inter> interior K' = {}"
+          moreover have "u \<in> g ` (interior k \<inter> interior K')"
+            using interior_image_subset[OF \<open>inj g\<close> contg] u
             unfolding image_Int[OF inj(1)] by blast
-          then show False
-            using as by blast
+          ultimately show False by blast
         qed
+        then have same: "(x, k) = (x', K')"
+          using ptag xk' xk by blast
         then show "g x = g x'"
           by auto
-        {
-          fix z
-          assume "z \<in> k"
-          then show "g z \<in> g ` k'"
-            using same by auto
-        }
-        {
-          fix z
-          assume "z \<in> k'"
-          then show "g z \<in> g ` k"
-            using same by auto
-        }
+        show "g u \<in> g ` K'"if "u \<in> k" for u
+          using that same by auto
+        show "g u \<in> g ` k"if "u \<in> K'" for u
+          using that same by auto
       next
         fix x
         assume "x \<in> cbox a b"
@@ -3269,31 +3231,26 @@
           using p(6) by auto
         then obtain X y where "h x \<in> X" "(y, X) \<in> p" by blast
         then show "x \<in> \<Union>{k. \<exists>x. (x, k) \<in> (\<lambda>(x, k). (g x, g ` k)) ` p}"
-          apply (clarsimp simp: )
+          apply clarsimp
           by (metis (no_types, lifting) assms(3) image_eqI pair_imageI)
-      qed
-        note ** = d(2)[OF this]
-        have *: "inj_on (\<lambda>(x, k). (g x, g ` k)) p"
-          using inj(1) unfolding inj_on_def by fastforce
-        have "(\<Sum>(x, k)\<in>(\<lambda>(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - i" (is "?l = _")
-          using assms(7)
-          apply (simp only: algebra_simps add_left_cancel scaleR_right.sum)
-          apply (subst sum.reindex_bij_betw[symmetric, where h="\<lambda>(x, k). (g x, g ` k)" and S=p])
-          apply (auto intro!: * sum.cong simp: bij_betw_def dest!: p(4))
-          done
+      qed (use gab in auto)
+      have *: "inj_on (\<lambda>(x, k). (g x, g ` k)) p"
+        using inj(1) unfolding inj_on_def by fastforce
+      have "(\<Sum>(x, k)\<in>(\<lambda>(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - i" (is "?l = _")
+        using r
+        apply (simp only: algebra_simps add_left_cancel scaleR_right.sum)
+        apply (subst sum.reindex_bij_betw[symmetric, where h="\<lambda>(x, k). (g x, g ` k)" and S=p])
+         apply (auto intro!: * sum.cong simp: bij_betw_def dest!: p(4))
+        done
       also have "\<dots> = r *\<^sub>R ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r")
-        unfolding scaleR_diff_right scaleR_scaleR
-        using assms(1)
-        by auto
-      finally have *: "?l = ?r" .
-      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e"
-        using **
-        unfolding *
-        unfolding norm_scaleR
-        using assms(1)
-        by (auto simp add:field_simps)
+        using \<open>0 < r\<close> by (auto simp: scaleR_diff_right)
+      finally have eq: "?l = ?r" .
+      show "norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e"
+        using d(2)[OF gimp] \<open>0 < r\<close> by (auto simp add: eq)
     qed
   qed
+  then show ?thesis
+    by (auto simp: h_eq has_integral)
 qed
 
 
@@ -4408,10 +4365,7 @@
     then have "?g integrable_on cbox c d"
       using assms has_integral_integrable integrable_subinterval by blast
     then have "f integrable_on cbox c d"
-      apply -
-      apply (rule integrable_eq)
-      apply auto
-      done
+      by (rule integrable_eq) auto
     moreover then have "i = integral (cbox c d) f"
       by (meson \<open>((\<lambda>x. if x \<in> cbox c d then f x else 0) has_integral i) (cbox a b)\<close> assms has_integral_restrict_closed_subinterval has_integral_unique integrable_integral)
     ultimately show ?r by auto
@@ -4591,9 +4545,9 @@
 
 lemma integrable_on_superset:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "\<forall>x. x \<notin> s \<longrightarrow> f x = 0"
-    and "s \<subseteq> t"
-    and "f integrable_on s"
+  assumes "f integrable_on S"
+    and "\<And>x. x \<notin> S \<Longrightarrow> f x = 0"
+    and "S \<subseteq> t"
   shows "f integrable_on t"
   using assms
   unfolding integrable_on_def
@@ -4601,7 +4555,7 @@
 
 lemma integral_restrict_UNIV [intro]:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  shows "f integrable_on s \<Longrightarrow> integral UNIV (\<lambda>x. if x \<in> s then f x else 0) = integral s f"
+  shows "f integrable_on S \<Longrightarrow> integral UNIV (\<lambda>x. if x \<in> S then f x else 0) = integral S f"
   apply (rule integral_unique)
   unfolding has_integral_restrict_UNIV
   apply auto
@@ -6881,7 +6835,7 @@
 proof -
   have "((\<lambda>(x, y). f x y) has_integral integral (cbox (c, a) (d, b)) (\<lambda>(x, y). f y x)) (prod.swap ` (cbox (c, a) (d, b)))"
     apply (rule has_integral_twiddle [of 1 prod.swap prod.swap "\<lambda>(x,y). f y x" "integral (cbox (c, a) (d, b)) (\<lambda>(x, y). f y x)", simplified])
-    apply (auto simp: isCont_swap content_Pair has_integral_integral [symmetric] integrable_continuous swap_continuous assms)
+    apply (force simp: isCont_swap content_Pair has_integral_integral [symmetric] integrable_continuous swap_continuous assms)+
     done
  then show ?thesis
    by force
@@ -6934,10 +6888,10 @@
     fix k ::nat
     have "(\<lambda>x. exp (-a*x)) integrable_on {c..of_real k}" (is ?P)
       unfolding f_def by (auto intro!: continuous_intros integrable_continuous_real)
-    hence int: "(f k) integrable_on {c..of_real k}"
-      by (rule integrable_eq[rotated]) (simp add: f_def)
-    show "f k integrable_on {c..}"
-      by (rule integrable_on_superset[OF _ _ int]) (auto simp: f_def)
+    hence  "(f k) integrable_on {c..of_real k}"
+      by (rule integrable_eq) (simp add: f_def)
+    then show "f k integrable_on {c..}"
+      by (rule integrable_on_superset) (auto simp: f_def)
   next
     fix x assume x: "x \<in> {c..}"
     have "sequentially \<le> principal {nat \<lceil>x\<rceil>..}" unfolding at_top_def by (simp add: Inf_lower)
@@ -7118,9 +7072,9 @@
     from assms have "(\<lambda>x. x powr e) integrable_on {a..n}"
       by (auto intro!: integrable_continuous_real continuous_intros)
     hence "f n integrable_on {a..n}"
-      by (rule integrable_eq [rotated]) (auto simp: f_def)
+      by (rule integrable_eq) (auto simp: f_def)
     thus "f n integrable_on {a..}"
-      by (rule integrable_on_superset [rotated 2]) (auto simp: f_def)
+      by (rule integrable_on_superset) (auto simp: f_def)
   next
     fix n :: nat and x :: real
     show "f n x \<le> f (Suc n) x" by (auto simp: f_def)
diff -r 1f955cdd9e59 -r 507a42c0a0ff src/HOL/Analysis/Improper_Integral.thy
--- a/src/HOL/Analysis/Improper_Integral.thy	Mon Aug 28 22:32:22 2017 +0100
+++ b/src/HOL/Analysis/Improper_Integral.thy	Tue Aug 29 17:41:11 2017 +0100
@@ -220,7 +220,10 @@
     qed
   qed
   then show ?thesis
-    using assms by (auto simp: equiintegrable_on_def integrable_eq)
+    using assms
+    apply (auto simp: equiintegrable_on_def)
+    apply (rule integrable_eq)
+    by auto 
 qed
 
 subsection\<open>Subinterval restrictions for equiintegrable families\<close>