# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1502832135 -3600
# Node ID 1a93b480fec8386283db35283afeee0d4f684027
# Parent  bc76686f85a3390448112e7ffa65e06a1e46a017
fixed the previous commit (henstock_lemma)

diff -r bc76686f85a3 -r 1a93b480fec8 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Tue Aug 15 18:14:50 2017 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Tue Aug 15 22:22:15 2017 +0100
@@ -2089,40 +2089,35 @@
         qed
         finally show ?case .
       next
-        note f' = f_int[of a b, unfolded absolutely_integrable_on_def]
-        note f = f'[THEN conjunct1] f'[THEN conjunct2]
-        note * = this(2)[unfolded has_integral_integral has_integral[of "\<lambda>x. norm (f x)"],rule_format]
         have "e/2>0"
           using \<open>e > 0\<close> by auto
-        from * [OF this] obtain d1 where
-          d1: "gauge d1" "\<forall>p. p tagged_division_of (cbox a b) \<and> d1 fine p \<longrightarrow>
+        moreover
+        have f: "f integrable_on cbox a b" "(\<lambda>x. norm (f x)) integrable_on cbox a b"
+          using f_int by (auto simp: absolutely_integrable_on_def)
+        ultimately obtain d1 where "gauge d1"
+           and d1: "\<And>p. \<lbrakk>p tagged_division_of (cbox a b); d1 fine p\<rbrakk> \<Longrightarrow>
             norm ((\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm (f x))) < e/2"
-          by auto
-        from henstock_lemma [OF f(1) \<open>e/2>0\<close>] obtain d2 where
-          d2: "gauge d2" "\<forall>p. p tagged_partial_division_of (cbox a b) \<and> d2 fine p \<longrightarrow>
-            (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x - integral k f)) < e/2" .
-         obtain p where
+          unfolding has_integral_integral has_integral by meson
+        obtain d2 where "gauge d2" 
+          and d2: "\<And>p. \<lbrakk>p tagged_partial_division_of (cbox a b); d2 fine p\<rbrakk> \<Longrightarrow>
+            (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x - integral k f)) < e/2"
+          by (blast intro: henstock_lemma [OF f(1) \<open>e/2>0\<close>])
+        obtain p where
           p: "p tagged_division_of (cbox a b)" "d1 fine p" "d2 fine p"
-          by (rule fine_division_exists [OF gauge_Int [OF d1(1) d2(1)], of a b])
+          by (rule fine_division_exists [OF gauge_Int [OF \<open>gauge d1\<close> \<open>gauge d2\<close>], of a b])
             (auto simp add: fine_Int)
-        have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> ?S \<longrightarrow> \<bar>sf - si\<bar> < e/2 \<longrightarrow>
-          \<bar>sf' - di\<bar> < e/2 \<longrightarrow> di < ?S + e"
+        have *: "\<And>sf sf' si di. \<lbrakk>sf' = sf; si \<le> ?S; \<bar>sf - si\<bar> < e/2;
+                      \<bar>sf' - di\<bar> < e/2\<rbrakk> \<Longrightarrow> di < ?S + e"
           by arith
-        show "integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
-          apply (subst if_P)
-          apply rule
-        proof (rule *[rule_format])
+        have "integral (cbox a b) (\<lambda>x. norm (f x)) < ?S + e"
+        proof (rule *)
           show "\<bar>(\<Sum>(x,k)\<in>p. norm (content k *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p. norm (integral k f))\<bar> < e/2"
             unfolding split_def
             apply (rule absdiff_norm_less)
-            using d2(2)[rule_format,of p]
-            using p(1,3)
-            unfolding tagged_division_of_def split_def
-            apply auto
+            using d2[of p] p(1,3) apply (auto simp: tagged_division_of_def split_def)
             done
           show "\<bar>(\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm(f x))\<bar> < e/2"
-            using d1(2)[rule_format,OF conjI[OF p(1,2)]]
-            by (simp only: real_norm_def)
+            using d1[OF p(1,2)] by (simp only: real_norm_def)
           show "(\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) = (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x))"
             apply (rule sum.cong)
             apply (rule refl)
@@ -2133,10 +2128,12 @@
             using partial_division_of_tagged_division[of p "cbox a b"] p(1)
             apply (subst sum.over_tagged_division_lemma[OF p(1)])
             apply (simp add: content_eq_0_interior)
-            apply (intro cSUP_upper2[OF D(2), of "snd ` p"])
+            apply (intro cSUP_upper2 D)
             apply (auto simp: tagged_partial_division_of_def)
             done
         qed
+        then show "integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
+          by simp
       qed
     qed (insert K, auto)
   qed