last-minute integration unscrambling
authorpaulson <lp15@cam.ac.uk>
Tue Aug 29 17:41:11 2017 +0100 (23 months ago)
changeset 66552507a42c0a0ff
parent 66540 1f955cdd9e59
child 66553 6ab32ffb2bdd
last-minute integration unscrambling
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Improper_Integral.thy
     1.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Aug 28 22:32:22 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Tue Aug 29 17:41:11 2017 +0100
     1.3 @@ -314,7 +314,7 @@
     1.4      then have "(\<lambda>x. f x * indicator \<Omega> x) integrable_on \<Omega>"
     1.5        by (auto simp: integrable_on_def cong: has_integral_cong)
     1.6      then have "(\<lambda>x. f x * indicator \<Omega> x) integrable_on (\<Omega> \<union> B n)"
     1.7 -      by (rule integrable_on_superset[rotated 2]) auto
     1.8 +      by (rule integrable_on_superset) auto
     1.9      then have "(\<lambda>x. f x * indicator \<Omega> x) integrable_on B n"
    1.10        unfolding B_def by (rule integrable_on_subcbox) auto
    1.11      then show "(\<lambda>x. f x * indicator \<Omega> x) \<in> lebesgue_on \<Omega>' \<rightarrow>\<^sub>M borel"
    1.12 @@ -2717,7 +2717,7 @@
    1.13    note intl = has_integral_integrable[OF int]
    1.14    have af: "f absolutely_integrable_on (closure S)"
    1.15      using nonneg
    1.16 -    by (intro absolutely_integrable_onI intl integrable_eq[OF _ intl]) simp
    1.17 +    by (intro absolutely_integrable_onI intl integrable_eq[OF intl]) simp
    1.18    then have "integral (closure S) f = set_lebesgue_integral lebesgue (closure S) f"
    1.19      by (intro set_lebesgue_integral_eq_integral(2)[symmetric])
    1.20    also have "\<dots> = 0 \<longleftrightarrow> (AE x in lebesgue. indicator (closure S) x *\<^sub>R f x = 0)"
     2.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Aug 28 22:32:22 2017 +0100
     2.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Aug 29 17:41:11 2017 +0100
     2.3 @@ -716,7 +716,7 @@
     2.4    using assms(1)
     2.5    by auto
     2.6  
     2.7 -lemma integrable_eq: "(\<And>x. x \<in> s \<Longrightarrow> f x = g x) \<Longrightarrow> f integrable_on s \<Longrightarrow> g integrable_on s"
     2.8 +lemma integrable_eq: "\<lbrakk>f integrable_on s; \<And>x. x \<in> s \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> g integrable_on s"
     2.9    unfolding integrable_on_def
    2.10    using has_integral_eq[of s f g] has_integral_eq by blast
    2.11  
    2.12 @@ -2615,79 +2615,70 @@
    2.13      and "Inf {a..b} = a"
    2.14    using assms by auto
    2.15  
    2.16 -lemma fundamental_theorem_of_calculus:
    2.17 +theorem fundamental_theorem_of_calculus:
    2.18    fixes f :: "real \<Rightarrow> 'a::banach"
    2.19 -  assumes "a \<le> b"
    2.20 -    and vecd: "\<forall>x\<in>{a..b}. (f has_vector_derivative f' x) (at x within {a..b})"
    2.21 +  assumes "a \<le> b" 
    2.22 +      and vecd: "\<And>x. x \<in> {a..b} \<Longrightarrow> (f has_vector_derivative f' x) (at x within {a..b})"
    2.23    shows "(f' has_integral (f b - f a)) {a..b}"
    2.24    unfolding has_integral_factor_content box_real[symmetric]
    2.25  proof safe
    2.26    fix e :: real
    2.27    assume "e > 0"
    2.28 -  then have "\<forall>x. \<exists>d>0.
    2.29 -         x \<in> {a..b} \<longrightarrow>
    2.30 -         (\<forall>y\<in>{a..b}.
    2.31 -             norm (y-x) < d \<longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e * norm (y-x))"
    2.32 +  then have "\<forall>x. \<exists>d>0. x \<in> {a..b} \<longrightarrow>
    2.33 +         (\<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))"
    2.34      using vecd[unfolded has_vector_derivative_def has_derivative_within_alt] by blast
    2.35    then obtain d where d: "\<And>x. 0 < d x"
    2.36                   "\<And>x y. \<lbrakk>x \<in> {a..b}; y \<in> {a..b}; norm (y-x) < d x\<rbrakk>
    2.37                          \<Longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e * norm (y-x)"
    2.38 -    by metis
    2.39 -  
    2.40 +    by metis  
    2.41    show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
    2.42      norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content (cbox a b))"
    2.43 -    apply (rule_tac x="\<lambda>x. ball x (d x)" in exI)
    2.44 -    apply safe
    2.45 -    apply (rule gauge_ball_dependent)
    2.46 -    apply rule
    2.47 -    apply (rule d(1))
    2.48 -  proof -
    2.49 +  proof (rule exI, safe)
    2.50 +    show "gauge (\<lambda>x. ball x (d x))"
    2.51 +      using d(1) gauge_ball_dependent by blast
    2.52 +  next
    2.53      fix p
    2.54 -    assume as: "p tagged_division_of cbox a b" "(\<lambda>x. ball x (d x)) fine p"
    2.55 -    show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content (cbox a b)"
    2.56 -      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]
    2.57 -      unfolding additive_tagged_division_1[OF assms(1) as(1)[simplified box_real],of "\<lambda>x. x",symmetric]
    2.58 -      unfolding sum_distrib_left
    2.59 -      defer
    2.60 -      unfolding sum_subtractf[symmetric]
    2.61 +    assume ptag: "p tagged_division_of cbox a b" and finep: "(\<lambda>x. ball x (d x)) fine p"
    2.62 +    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))"
    2.63 +      using additive_tagged_division_1[where f= "\<lambda>x. x"] additive_tagged_division_1[where f= f]
    2.64 +            \<open>a \<le> b\<close> ptag by auto
    2.65 +    have "norm (\<Sum>(x, K) \<in> p. (content K *\<^sub>R f' x) - (f (Sup K) - f (Inf K)))
    2.66 +          \<le> (\<Sum>n\<in>p. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k))"
    2.67      proof (rule sum_norm_le,safe)
    2.68 -      fix x k
    2.69 -      assume "(x, k) \<in> p"
    2.70 -      note xk = tagged_division_ofD(2-4)[OF as(1) this]
    2.71 -      then obtain u v where k: "k = cbox u v" by blast
    2.72 -      have *: "u \<le> v"
    2.73 -        using xk unfolding k by auto
    2.74 -      have ball: "\<forall>xa\<in>k. xa \<in> ball x (d x)"
    2.75 -        using as(2)[unfolded fine_def,rule_format,OF \<open>(x,k)\<in>p\<close>,unfolded split_conv subset_eq] .
    2.76 -      have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) \<le>
    2.77 -        norm (f u - f x - (u - x) *\<^sub>R f' x) + norm (f v - f x - (v - x) *\<^sub>R f' x)"
    2.78 -        apply (rule order_trans[OF _ norm_triangle_ineq4])
    2.79 -        apply (rule eq_refl)
    2.80 -        apply (rule arg_cong[where f=norm])
    2.81 -        unfolding scaleR_diff_left
    2.82 -        apply (auto simp add:algebra_simps)
    2.83 -        done
    2.84 +      fix x K
    2.85 +      assume "(x, K) \<in> p"
    2.86 +      then have "x \<in> K" and kab: "K \<subseteq> cbox a b"
    2.87 +        using ptag by blast+
    2.88 +      then obtain u v where k: "K = cbox u v" and "x \<in> K" and kab: "K \<subseteq> cbox a b"
    2.89 +        using ptag \<open>(x, K) \<in> p\<close> by auto 
    2.90 +      have "u \<le> v"
    2.91 +        using \<open>x \<in> K\<close> unfolding k by auto
    2.92 +      have ball: "\<forall>y\<in>K. y \<in> ball x (d x)"
    2.93 +        using finep \<open>(x, K) \<in> p\<close> by blast
    2.94 +      have "u \<in> K" "v \<in> K"
    2.95 +        by (simp_all add: \<open>u \<le> v\<close> k)
    2.96 +      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))"
    2.97 +        by (auto simp add: algebra_simps)
    2.98 +      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)"
    2.99 +        by (rule norm_triangle_ineq4)
   2.100 +      finally have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) \<le>
   2.101 +        norm (f u - f x - (u - x) *\<^sub>R f' x) + norm (f v - f x - (v - x) *\<^sub>R f' x)" .
   2.102        also have "\<dots> \<le> e * norm (u - x) + e * norm (v - x)"
   2.103 -        apply (rule add_mono)
   2.104 -        apply (rule d(2)[of "x" "u",unfolded o_def])
   2.105 -        prefer 4
   2.106 -        apply (rule d(2)[of "x" "v",unfolded o_def])
   2.107 -        using ball[rule_format,of u] ball[rule_format,of v]
   2.108 -        using xk(1-2)
   2.109 -        unfolding k subset_eq
   2.110 -        apply (auto simp add:dist_real_def)
   2.111 -        done
   2.112 -      also have "\<dots> \<le> e * (Sup k - Inf k)"
   2.113 -        unfolding k interval_bounds_real[OF *]
   2.114 -        using xk(1)
   2.115 -        unfolding k
   2.116 -        by (auto simp add: dist_real_def field_simps)
   2.117 -      finally show "norm (content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \<le>
   2.118 -        e * (Sup k - Inf k)"
   2.119 -        unfolding box_real k interval_bounds_real[OF *] content_real[OF *]
   2.120 -          interval_upperbound_real interval_lowerbound_real
   2.121 -          .
   2.122 +      proof (rule add_mono)
   2.123 +        show "norm (f u - f x - (u - x) *\<^sub>R f' x) \<le> e * norm (u - x)"
   2.124 +          apply (rule d(2)[of x u])
   2.125 +          using \<open>x \<in> K\<close> kab \<open>u \<in> K\<close> ball dist_real_def by (auto simp add:dist_real_def)
   2.126 +        show "norm (f v - f x - (v - x) *\<^sub>R f' x) \<le> e * norm (v - x)"
   2.127 +          apply (rule d(2)[of x v])
   2.128 +          using \<open>x \<in> K\<close> kab \<open>v \<in> K\<close> ball dist_real_def by (auto simp add:dist_real_def)
   2.129 +      qed
   2.130 +      also have "\<dots> \<le> e * (Sup K - Inf K)"
   2.131 +        using \<open>x \<in> K\<close> by (auto simp: k interval_bounds_real[OF \<open>u \<le> v\<close>] field_simps)
   2.132 +      finally show "norm (content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))) \<le> e * (Sup K - Inf K)"
   2.133 +        using \<open>u \<le> v\<close> by (simp add: k)
   2.134      qed
   2.135 +    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)"
   2.136 +      by (auto simp: ba split_def sum_subtractf [symmetric] sum_distrib_left)
   2.137    qed
   2.138  qed
   2.139  
   2.140 @@ -2697,7 +2688,7 @@
   2.141    shows "((\<lambda>x. x) has_integral (b\<^sup>2 - a\<^sup>2)/2) {a..b}"
   2.142  proof -
   2.143    have "((\<lambda>x. x) has_integral inverse 2 * b\<^sup>2 - inverse 2 * a\<^sup>2) {a..b}"
   2.144 -    apply (rule fundamental_theorem_of_calculus [OF assms], clarify)
   2.145 +    apply (rule fundamental_theorem_of_calculus [OF assms])
   2.146      unfolding power2_eq_square
   2.147      by (rule derivative_eq_intros | simp)+
   2.148    then show ?thesis
   2.149 @@ -3144,10 +3135,10 @@
   2.150      using  antiderivative_continuous[OF assms] by metis
   2.151    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
   2.152    proof -
   2.153 -    have "\<forall>x\<in>cbox u v. (g has_vector_derivative f x) (at x within cbox u v)"
   2.154 +    have "\<And>x. x \<in> cbox u v \<Longrightarrow> (g has_vector_derivative f x) (at x within cbox u v)"
   2.155        by (meson g has_vector_derivative_within_subset interval_subset_is_interval is_interval_closed_interval subsetCE that(1) that(2))
   2.156      then show ?thesis
   2.157 -      by (simp add: fundamental_theorem_of_calculus that(3))
   2.158 +      by (metis box_real(2) that(3) fundamental_theorem_of_calculus)
   2.159    qed
   2.160    then show ?thesis
   2.161      using that by blast
   2.162 @@ -3158,39 +3149,30 @@
   2.163  
   2.164  lemma has_integral_twiddle:
   2.165    assumes "0 < r"
   2.166 -    and "\<forall>x. h(g x) = x"
   2.167 -    and "\<forall>x. g(h x) = x"
   2.168 +    and hg: "\<And>x. h(g x) = x"
   2.169 +    and gh: "\<And>x. g(h x) = x"
   2.170      and contg: "\<And>x. continuous (at x) g"
   2.171 -    and "\<forall>u v. \<exists>w z. g ` cbox u v = cbox w z"
   2.172 -    and h: "\<forall>u v. \<exists>w z. h ` cbox u v = cbox w z"
   2.173 -    and "\<forall>u v. content(g ` cbox u v) = r * content (cbox u v)"
   2.174 +    and g: "\<And>u v. \<exists>w z. g ` cbox u v = cbox w z"
   2.175 +    and h: "\<And>u v. \<exists>w z. h ` cbox u v = cbox w z"
   2.176 +    and r: "\<And>u v. content(g ` cbox u v) = r * content (cbox u v)"
   2.177      and intfi: "(f has_integral i) (cbox a b)"
   2.178    shows "((\<lambda>x. f(g x)) has_integral (1 / r) *\<^sub>R i) (h ` cbox a b)"
   2.179 -proof -
   2.180 -  show ?thesis when *: "cbox a b \<noteq> {} \<Longrightarrow> ?thesis"
   2.181 -    apply cases
   2.182 -    defer
   2.183 -    apply (rule *)
   2.184 -    apply assumption
   2.185 -  proof goal_cases
   2.186 -    case prems: 1
   2.187 -    then show ?thesis
   2.188 -      unfolding prems assms(8)[unfolded prems has_integral_empty_eq] by auto
   2.189 -  qed
   2.190 -  assume "cbox a b \<noteq> {}"
   2.191 +proof (cases "cbox a b = {}")
   2.192 +  case True
   2.193 +  then show ?thesis 
   2.194 +    using intfi by auto
   2.195 +next
   2.196 +  case False
   2.197    obtain w z where wz: "h ` cbox a b = cbox w z"
   2.198      using h by blast
   2.199    have inj: "inj g" "inj h"
   2.200 -    apply (metis assms(2) injI)
   2.201 -    by (metis assms(3) injI)
   2.202 +    using hg gh injI by metis+
   2.203    from h obtain ha hb where h_eq: "h ` cbox a b = cbox ha hb" by blast
   2.204 -  show ?thesis
   2.205 -    unfolding h_eq has_integral
   2.206 -    unfolding h_eq[symmetric]
   2.207 -  proof safe
   2.208 -    fix e :: real
   2.209 -    assume e: "e > 0"
   2.210 -    with \<open>0 < r\<close> have "e * r > 0" by simp
   2.211 +  have "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of h ` cbox a b \<and> d fine p 
   2.212 +              \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e)"
   2.213 +    if "e > 0" for e
   2.214 +  proof -
   2.215 +    have "e * r > 0" using that \<open>0 < r\<close> by simp
   2.216      with intfi[unfolded has_integral]
   2.217      obtain d where d: "gauge d"
   2.218                     "\<And>p. p tagged_division_of cbox a b \<and> d fine p 
   2.219 @@ -3199,69 +3181,49 @@
   2.220      define d' where "d' x = {y. g y \<in> d (g x)}" for x
   2.221      have d': "\<And>x. d' x = {y. g y \<in> (d (g x))}"
   2.222        unfolding d'_def ..
   2.223 -    show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of h ` cbox a b \<and> d fine p 
   2.224 -              \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e)"
   2.225 +    show ?thesis
   2.226      proof (rule_tac x=d' in exI, safe)
   2.227        show "gauge d'"
   2.228 -        using d(1)
   2.229 -        unfolding gauge_def d'
   2.230 -        using continuous_open_preimage_univ[OF _ contg]
   2.231 -        by auto
   2.232 +        using d(1) continuous_open_preimage_univ[OF _ contg] by (auto simp: gauge_def d')
   2.233 +    next
   2.234        fix p
   2.235 -      assume as: "p tagged_division_of h ` cbox a b" "d' fine p"
   2.236 -      note p = tagged_division_ofD[OF as(1)]
   2.237 -      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"
   2.238 +      assume ptag: "p tagged_division_of h ` cbox a b" and finep: "d' fine p"
   2.239 +      note p = tagged_division_ofD[OF ptag]
   2.240 +      have gab: "g y \<in> cbox a b" if "y \<in> K" "(x, K) \<in> p" for x y K
   2.241 +        by (metis hg inj(2) inj_image_mem_iff p(3) subsetCE that that)
   2.242 +      have gimp: "(\<lambda>(x,K). (g x, g ` K)) ` p tagged_division_of (cbox a b) \<and> 
   2.243 +                  d fine (\<lambda>(x, k). (g x, g ` k)) ` p"
   2.244          unfolding tagged_division_of
   2.245        proof safe
   2.246          show "finite ((\<lambda>(x, k). (g x, g ` k)) ` p)"
   2.247 -          using as by auto
   2.248 +          using ptag by auto
   2.249          show "d fine (\<lambda>(x, k). (g x, g ` k)) ` p"
   2.250 -          using as(2) unfolding fine_def d' by auto
   2.251 +          using finep unfolding fine_def d' by auto
   2.252 +      next
   2.253          fix x k
   2.254 -        assume xk[intro]: "(x, k) \<in> p"
   2.255 +        assume xk: "(x, k) \<in> p"
   2.256          show "g x \<in> g ` k"
   2.257            using p(2)[OF xk] by auto
   2.258          show "\<exists>u v. g ` k = cbox u v"
   2.259            using p(4)[OF xk] using assms(5-6) by auto
   2.260 -        {
   2.261 -          fix y
   2.262 -          assume "y \<in> k"
   2.263 -          then show "g y \<in> cbox a b" "g y \<in> cbox a b"
   2.264 -            using p(3)[OF xk,unfolded subset_eq,rule_format,of "h (g y)"]
   2.265 -            using assms(2)[rule_format,of y]
   2.266 -            unfolding inj_image_mem_iff[OF inj(2)]
   2.267 -            by auto
   2.268 -        }
   2.269 -        fix x' k'
   2.270 -        assume xk': "(x', k') \<in> p"
   2.271 -        fix z
   2.272 -        assume z: "z \<in> interior (g ` k)" "z \<in> interior (g ` k')"
   2.273 -        have same: "(x, k) = (x', k')"
   2.274 -          apply -
   2.275 -          apply (rule ccontr)
   2.276 -          apply (drule p(5)[OF xk xk'])
   2.277 -        proof -
   2.278 -          assume as: "interior k \<inter> interior k' = {}"
   2.279 -          have "z \<in> g ` (interior k \<inter> interior k')"
   2.280 -            using interior_image_subset[OF \<open>inj g\<close> contg] z
   2.281 +        fix x' K' u
   2.282 +        assume xk': "(x', K') \<in> p" and u: "u \<in> interior (g ` k)" "u \<in> interior (g ` K')"
   2.283 +        have "interior k \<inter> interior K' \<noteq> {}"
   2.284 +        proof 
   2.285 +          assume "interior k \<inter> interior K' = {}"
   2.286 +          moreover have "u \<in> g ` (interior k \<inter> interior K')"
   2.287 +            using interior_image_subset[OF \<open>inj g\<close> contg] u
   2.288              unfolding image_Int[OF inj(1)] by blast
   2.289 -          then show False
   2.290 -            using as by blast
   2.291 +          ultimately show False by blast
   2.292          qed
   2.293 +        then have same: "(x, k) = (x', K')"
   2.294 +          using ptag xk' xk by blast
   2.295          then show "g x = g x'"
   2.296            by auto
   2.297 -        {
   2.298 -          fix z
   2.299 -          assume "z \<in> k"
   2.300 -          then show "g z \<in> g ` k'"
   2.301 -            using same by auto
   2.302 -        }
   2.303 -        {
   2.304 -          fix z
   2.305 -          assume "z \<in> k'"
   2.306 -          then show "g z \<in> g ` k"
   2.307 -            using same by auto
   2.308 -        }
   2.309 +        show "g u \<in> g ` K'"if "u \<in> k" for u
   2.310 +          using that same by auto
   2.311 +        show "g u \<in> g ` k"if "u \<in> K'" for u
   2.312 +          using that same by auto
   2.313        next
   2.314          fix x
   2.315          assume "x \<in> cbox a b"
   2.316 @@ -3269,31 +3231,26 @@
   2.317            using p(6) by auto
   2.318          then obtain X y where "h x \<in> X" "(y, X) \<in> p" by blast
   2.319          then show "x \<in> \<Union>{k. \<exists>x. (x, k) \<in> (\<lambda>(x, k). (g x, g ` k)) ` p}"
   2.320 -          apply (clarsimp simp: )
   2.321 +          apply clarsimp
   2.322            by (metis (no_types, lifting) assms(3) image_eqI pair_imageI)
   2.323 -      qed
   2.324 -        note ** = d(2)[OF this]
   2.325 -        have *: "inj_on (\<lambda>(x, k). (g x, g ` k)) p"
   2.326 -          using inj(1) unfolding inj_on_def by fastforce
   2.327 -        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 = _")
   2.328 -          using assms(7)
   2.329 -          apply (simp only: algebra_simps add_left_cancel scaleR_right.sum)
   2.330 -          apply (subst sum.reindex_bij_betw[symmetric, where h="\<lambda>(x, k). (g x, g ` k)" and S=p])
   2.331 -          apply (auto intro!: * sum.cong simp: bij_betw_def dest!: p(4))
   2.332 -          done
   2.333 +      qed (use gab in auto)
   2.334 +      have *: "inj_on (\<lambda>(x, k). (g x, g ` k)) p"
   2.335 +        using inj(1) unfolding inj_on_def by fastforce
   2.336 +      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 = _")
   2.337 +        using r
   2.338 +        apply (simp only: algebra_simps add_left_cancel scaleR_right.sum)
   2.339 +        apply (subst sum.reindex_bij_betw[symmetric, where h="\<lambda>(x, k). (g x, g ` k)" and S=p])
   2.340 +         apply (auto intro!: * sum.cong simp: bij_betw_def dest!: p(4))
   2.341 +        done
   2.342        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")
   2.343 -        unfolding scaleR_diff_right scaleR_scaleR
   2.344 -        using assms(1)
   2.345 -        by auto
   2.346 -      finally have *: "?l = ?r" .
   2.347 -      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e"
   2.348 -        using **
   2.349 -        unfolding *
   2.350 -        unfolding norm_scaleR
   2.351 -        using assms(1)
   2.352 -        by (auto simp add:field_simps)
   2.353 +        using \<open>0 < r\<close> by (auto simp: scaleR_diff_right)
   2.354 +      finally have eq: "?l = ?r" .
   2.355 +      show "norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e"
   2.356 +        using d(2)[OF gimp] \<open>0 < r\<close> by (auto simp add: eq)
   2.357      qed
   2.358    qed
   2.359 +  then show ?thesis
   2.360 +    by (auto simp: h_eq has_integral)
   2.361  qed
   2.362  
   2.363  
   2.364 @@ -4408,10 +4365,7 @@
   2.365      then have "?g integrable_on cbox c d"
   2.366        using assms has_integral_integrable integrable_subinterval by blast
   2.367      then have "f integrable_on cbox c d"
   2.368 -      apply -
   2.369 -      apply (rule integrable_eq)
   2.370 -      apply auto
   2.371 -      done
   2.372 +      by (rule integrable_eq) auto
   2.373      moreover then have "i = integral (cbox c d) f"
   2.374        by (meson \<open>((\<lambda>x. if x \<in> cbox c d then f x else 0) has_integral i) (cbox a b)\<close> assms has_integral_restrict_closed_subinterval has_integral_unique integrable_integral)
   2.375      ultimately show ?r by auto
   2.376 @@ -4591,9 +4545,9 @@
   2.377  
   2.378  lemma integrable_on_superset:
   2.379    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   2.380 -  assumes "\<forall>x. x \<notin> s \<longrightarrow> f x = 0"
   2.381 -    and "s \<subseteq> t"
   2.382 -    and "f integrable_on s"
   2.383 +  assumes "f integrable_on S"
   2.384 +    and "\<And>x. x \<notin> S \<Longrightarrow> f x = 0"
   2.385 +    and "S \<subseteq> t"
   2.386    shows "f integrable_on t"
   2.387    using assms
   2.388    unfolding integrable_on_def
   2.389 @@ -4601,7 +4555,7 @@
   2.390  
   2.391  lemma integral_restrict_UNIV [intro]:
   2.392    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   2.393 -  shows "f integrable_on s \<Longrightarrow> integral UNIV (\<lambda>x. if x \<in> s then f x else 0) = integral s f"
   2.394 +  shows "f integrable_on S \<Longrightarrow> integral UNIV (\<lambda>x. if x \<in> S then f x else 0) = integral S f"
   2.395    apply (rule integral_unique)
   2.396    unfolding has_integral_restrict_UNIV
   2.397    apply auto
   2.398 @@ -6881,7 +6835,7 @@
   2.399  proof -
   2.400    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)))"
   2.401      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])
   2.402 -    apply (auto simp: isCont_swap content_Pair has_integral_integral [symmetric] integrable_continuous swap_continuous assms)
   2.403 +    apply (force simp: isCont_swap content_Pair has_integral_integral [symmetric] integrable_continuous swap_continuous assms)+
   2.404      done
   2.405   then show ?thesis
   2.406     by force
   2.407 @@ -6934,10 +6888,10 @@
   2.408      fix k ::nat
   2.409      have "(\<lambda>x. exp (-a*x)) integrable_on {c..of_real k}" (is ?P)
   2.410        unfolding f_def by (auto intro!: continuous_intros integrable_continuous_real)
   2.411 -    hence int: "(f k) integrable_on {c..of_real k}"
   2.412 -      by (rule integrable_eq[rotated]) (simp add: f_def)
   2.413 -    show "f k integrable_on {c..}"
   2.414 -      by (rule integrable_on_superset[OF _ _ int]) (auto simp: f_def)
   2.415 +    hence  "(f k) integrable_on {c..of_real k}"
   2.416 +      by (rule integrable_eq) (simp add: f_def)
   2.417 +    then show "f k integrable_on {c..}"
   2.418 +      by (rule integrable_on_superset) (auto simp: f_def)
   2.419    next
   2.420      fix x assume x: "x \<in> {c..}"
   2.421      have "sequentially \<le> principal {nat \<lceil>x\<rceil>..}" unfolding at_top_def by (simp add: Inf_lower)
   2.422 @@ -7118,9 +7072,9 @@
   2.423      from assms have "(\<lambda>x. x powr e) integrable_on {a..n}"
   2.424        by (auto intro!: integrable_continuous_real continuous_intros)
   2.425      hence "f n integrable_on {a..n}"
   2.426 -      by (rule integrable_eq [rotated]) (auto simp: f_def)
   2.427 +      by (rule integrable_eq) (auto simp: f_def)
   2.428      thus "f n integrable_on {a..}"
   2.429 -      by (rule integrable_on_superset [rotated 2]) (auto simp: f_def)
   2.430 +      by (rule integrable_on_superset) (auto simp: f_def)
   2.431    next
   2.432      fix n :: nat and x :: real
   2.433      show "f n x \<le> f (Suc n) x" by (auto simp: f_def)
     3.1 --- a/src/HOL/Analysis/Improper_Integral.thy	Mon Aug 28 22:32:22 2017 +0100
     3.2 +++ b/src/HOL/Analysis/Improper_Integral.thy	Tue Aug 29 17:41:11 2017 +0100
     3.3 @@ -220,7 +220,10 @@
     3.4      qed
     3.5    qed
     3.6    then show ?thesis
     3.7 -    using assms by (auto simp: equiintegrable_on_def integrable_eq)
     3.8 +    using assms
     3.9 +    apply (auto simp: equiintegrable_on_def)
    3.10 +    apply (rule integrable_eq)
    3.11 +    by auto 
    3.12  qed
    3.13  
    3.14  subsection\<open>Subinterval restrictions for equiintegrable families\<close>