# HG changeset patch
# User paulson
# Date 1502832154 -3600
# Node ID a6ec6c806a6c3a296bb0b7dd71ca4628a6dfa79b
# Parent  36a01c02d0ca4dab8ba409aef80d950174aac299# Parent  1a93b480fec8386283db35283afeee0d4f684027
merged

diff -r 36a01c02d0ca -r a6ec6c806a6c src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Tue Aug 15 22:23:28 2017 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Tue Aug 15 22:22:34 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
diff -r 36a01c02d0ca -r a6ec6c806a6c src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Aug 15 22:23:28 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Aug 15 22:22:34 2017 +0100
@@ -5670,10 +5670,10 @@
   assumes "f integrable_on cbox a b"
     and "e > 0"
     and "gauge d"
-    and "(\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
-      norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p - integral(cbox a b) f) < e)"
+    and less_e: "\<And>p. \<lbrakk>p tagged_division_of (cbox a b); d fine p\<rbrakk> \<Longrightarrow>
+                     norm (sum (\<lambda>(x,K). content K *\<^sub>R f x) p - integral(cbox a b) f) < e"
     and p: "p tagged_partial_division_of (cbox a b)" "d fine p"
-  shows "norm (sum (\<lambda>(x,k). content k *\<^sub>R f x - integral k f) p) \<le> e"
+  shows "norm (sum (\<lambda>(x,K). content K *\<^sub>R f x - integral K f) p) \<le> e"
   (is "?x \<le> e")
 proof -
   { presume "\<And>k. 0<k \<Longrightarrow> ?x \<le> e + k" then show ?thesis by (blast intro: field_le_epsilon) }
@@ -5720,15 +5720,9 @@
 
   let ?p = "p \<union> \<Union>(qq ` r)"
   have "norm ((\<Sum>(x, k)\<in>?p. content k *\<^sub>R f x) - integral (cbox a b) f) < e"
-    apply (rule assms(4)[rule_format])
-  proof
+  proof (rule less_e)
     show "d fine ?p"
-      apply (rule fine_Un)
-      apply (rule p)
-      apply (rule fine_Union)
-      using qq
-      apply auto
-      done
+      by (metis (mono_tags, hide_lams) qq fine_Un fine_Union imageE p(2))
     note * = tagged_partial_division_of_union_self[OF p(1)]
     have "p \<union> \<Union>(qq ` r) tagged_division_of \<Union>(snd ` p) \<union> \<Union>r"
       using r
@@ -5902,53 +5896,55 @@
 
 lemma henstock_lemma_part2:
   fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
-  assumes "f integrable_on cbox a b"
-    and "e > 0"
-    and "gauge d"
-    and "\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
-      norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p - integral (cbox a b) f) < e"
-    and "p tagged_partial_division_of (cbox a b)"
+  assumes fed: "f integrable_on cbox a b" "e > 0" "gauge d"
+    and less_e: "\<And>p. \<lbrakk>p tagged_division_of (cbox a b); d fine p\<rbrakk> \<Longrightarrow>
+                     norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p - integral (cbox a b) f) < e"
+    and tag: "p tagged_partial_division_of (cbox a b)"
     and "d fine p"
   shows "sum (\<lambda>(x,k). norm (content k *\<^sub>R f x - integral k f)) p \<le> 2 * real (DIM('n)) * e"
-  unfolding split_def
-  apply (rule sum_norm_allsubsets_bound)
-  defer
-  apply (rule henstock_lemma_part1[unfolded split_def,OF assms(1-3)])
-  apply safe
-  apply (rule assms[rule_format,unfolded split_def])
-  defer
-  apply (rule tagged_partial_division_subset)
-  apply (rule assms)
-  apply assumption
-  apply (rule fine_subset)
-  apply assumption
-  apply (rule assms)
-  using assms(5)
-  apply auto
-  done
+proof -
+  have "finite p"
+    using tag by blast
+  then show ?thesis
+    unfolding split_def
+  proof (rule sum_norm_allsubsets_bound)
+    fix Q
+    assume Q: "Q \<subseteq> p"
+    then have fine: "d fine Q"
+      by (simp add: \<open>d fine p\<close> fine_subset)
+    show "norm (\<Sum>x\<in>Q. content (snd x) *\<^sub>R f (fst x) - integral (snd x) f) \<le> e"
+      apply (rule henstock_lemma_part1[OF fed less_e, unfolded split_def])
+      using Q tag tagged_partial_division_subset apply (force simp add: fine)+
+      done
+  qed
+qed
 
 lemma henstock_lemma:
   fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
-  assumes "f integrable_on cbox a b"
+  assumes intf: "f integrable_on cbox a b"
     and "e > 0"
-  obtains d where "gauge d"
-    and "\<forall>p. p tagged_partial_division_of (cbox a b) \<and> d fine p \<longrightarrow>
-      sum (\<lambda>(x,k). norm(content k *\<^sub>R f x - integral k f)) p < e"
+  obtains \<gamma> where "gauge \<gamma>"
+    and "\<And>p. \<lbrakk>p tagged_partial_division_of (cbox a b); \<gamma> fine p\<rbrakk> \<Longrightarrow>
+             sum (\<lambda>(x,k). norm(content k *\<^sub>R f x - integral k f)) p < e"
 proof -
-  have *: "e / (2 * (real DIM('n) + 1)) > 0" using assms(2) by simp
-  from integrable_integral[OF assms(1),unfolded has_integral[of f],rule_format,OF this]
-  guess d..note d = conjunctD2[OF this]
+  have *: "e / (2 * (real DIM('n) + 1)) > 0" using \<open>e > 0\<close> by simp
+  with integrable_integral[OF intf, unfolded has_integral]
+  obtain \<gamma> where "gauge \<gamma>"
+    and \<gamma>: "\<And>p. \<lbrakk>p tagged_division_of cbox a b; \<gamma> fine p\<rbrakk> \<Longrightarrow>
+         norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f x) - integral (cbox a b) f)
+         < e / (2 * (real DIM('n) + 1))"
+    by metis
   show thesis
-    apply (rule that)
-    apply (rule d)
-  proof (safe, goal_cases)
-    case (1 p)
-    note * = henstock_lemma_part2[OF assms(1) * d this]
-    show ?case
-      apply (rule le_less_trans[OF *])
-      using \<open>e > 0\<close>
-      apply (auto simp add: field_simps)
-      done
+  proof (rule that [OF \<open>gauge \<gamma>\<close>])
+    fix p
+    assume p: "p tagged_partial_division_of cbox a b" "\<gamma> fine p"
+    have "(\<Sum>(x,K)\<in>p. norm (content K *\<^sub>R f x - integral K f)) 
+          \<le> 2 * real DIM('n) * (e / (2 * (real DIM('n) + 1)))"
+      using henstock_lemma_part2[OF intf * \<open>gauge \<gamma>\<close> \<gamma> p] by metis
+    also have "... < e"
+      using \<open>e > 0\<close> by (auto simp add: field_simps)
+    finally
+    show "(\<Sum>(x,K)\<in>p. norm (content K *\<^sub>R f x - integral K f)) < e" .
   qed
 qed
 
@@ -6118,30 +6114,19 @@
               done
             fix t
             assume "t \<in> {0..s}"
-            show "norm (\<Sum>(x, k)\<in>{xk \<in> p. m (fst xk) = t}. content k *\<^sub>R f (m x) x -
-              integral k (f (m x))) \<le> e/2 ^ (t + 2)"
-              apply (rule order_trans
-                [of _ "norm (sum (\<lambda>(x,k). content k *\<^sub>R f t x - integral k (f t)) {xk \<in> p. m (fst xk) = t})"])
-              apply (rule eq_refl)
-              apply (rule arg_cong[where f=norm])
-              apply (rule sum.cong)
-              apply (rule refl)
-              defer
-              apply (rule henstock_lemma_part1)
-              apply (rule assms(1)[rule_format])
-              apply (simp add: e)
-              apply safe
-              apply (rule c)+
-              apply assumption+
-              apply (rule tagged_partial_division_subset[of p])
-              apply (rule p(1)[unfolded tagged_division_of_def,THEN conjunct1])
-              defer
-              unfolding fine_def
-              apply safe
-              apply (drule p(2)[unfolded fine_def,rule_format])
-              unfolding d_def
-              apply auto
-              done
+            have "norm (\<Sum>(x,k)\<in>{xk \<in> p. m (fst xk) = t}. content k *\<^sub>R f (m x) x - integral k (f (m x))) =
+                  norm (\<Sum>(x,k)\<in>{xk \<in> p. m (fst xk) = t}. content k *\<^sub>R f t x - integral k (f t))"
+              by (force intro!: sum.cong arg_cong[where f=norm])
+            also have "... \<le> e/2 ^ (t + 2)"
+            proof (rule henstock_lemma_part1 [OF intf _ c])
+              show "{xk \<in> p. m (fst xk) = t} tagged_partial_division_of cbox a b"
+                apply (rule tagged_partial_division_subset[of p])
+                using p by (auto simp: tagged_division_of_def)
+              show "c t fine {xk \<in> p. m (fst xk) = t}"
+                using p(2) by (auto simp: fine_def d_def)
+            qed (auto simp: e)
+            finally show "norm (\<Sum>(x, k)\<in>{xk \<in> p. m (fst xk) = t}. content k *\<^sub>R f (m x) x -
+              integral k (f (m x))) \<le> e/2 ^ (t + 2)" .
           qed
         qed (insert s, auto)
       next