# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1503704606 -3600
# Node ID ca8b18baf0e03db4231ad0cb879d486de1fa8e34
# Parent  89b6455b63b6f1bd20c369cac17681f9d8f6a7b8
unscrambling esp of Henstock_lemma_part1

diff -r 89b6455b63b6 -r ca8b18baf0e0 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Aug 25 23:30:36 2017 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sat Aug 26 00:43:26 2017 +0100
@@ -1732,31 +1732,27 @@
       then have sum_less_e2: "(\<Sum>(x,K) \<in> p'. norm (content K *\<^sub>R f x - integral K f)) < e/2"
         using g(2) gp' tagged_division_of_def by blast
 
-      have XX: "(x, I \<inter> L) \<in> p'" if "(x, L) \<in> p" "I \<in> d" "y \<in> I" "y \<in> L"
+      have "(x, I \<inter> L) \<in> p'" if x: "(x, L) \<in> p" "I \<in> d" and y: "y \<in> I" "y \<in> L"
         for x I L y
       proof -
         have "x \<in> I"
-          using fineD[OF p(3) that(1)] k(2)[OF that(2), of x] that(3-) by auto
-        then have "(\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> I \<inter> L = i \<inter> l)"
-          using that(1) that(2) by blast
+          using fineD[OF p(3) that(1)] k(2)[OF \<open>I \<in> d\<close>] y by auto
+        with x have "(\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> I \<inter> L = i \<inter> l)"
+          by blast
         then have "(x, I \<inter> L) \<in> p'"
           by (simp add: p'_def)
-        then show ?thesis
-          using that(3) by auto
+        with y show ?thesis by auto
       qed
-  have p'alt: "p' = {(x, I \<inter> L) | x I L. (x,L) \<in> p \<and> I \<in> d \<and> I \<inter> L \<noteq> {}}"
-      proof (safe, goal_cases)
-        case prems: (2 _ _ x i l)
-        then show ?case
-          using XX by auto
-      next
-        fix x K
-        assume "(x, K) \<in> p'"
-        then obtain i l where il: "x \<in> i" "i \<in> d" "(x, l) \<in> p" "K = i \<inter> l" 
-          unfolding p'_def by auto
-        then show "\<exists>y i l. (x, K) = (y, i \<inter> l) \<and> (y, l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}"
+      moreover have "\<exists>y i l. (x, K) = (y, i \<inter> l) \<and> (y, l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}"
+        if xK: "(x,K) \<in> p'" for x K
+      proof -
+        obtain i l where il: "x \<in> i" "i \<in> d" "(x, l) \<in> p" "K = i \<inter> l" 
+          using xK unfolding p'_def by auto
+        then show ?thesis
           using p'(2) by fastforce
       qed
+      ultimately have p'alt: "p' = {(x, I \<inter> L) | x I L. (x,L) \<in> p \<and> I \<in> d \<and> I \<inter> L \<noteq> {}}"
+        by auto
       have sum_p': "(\<Sum>(x,K) \<in> p'. norm (integral K f)) = (\<Sum>k\<in>snd ` p'. norm (integral k f))"
         apply (subst sum.over_tagged_division_lemma[OF p'',of "\<lambda>k. norm (integral k f)"])
          apply (auto intro: integral_null simp: content_eq_0_interior)
@@ -2034,26 +2030,20 @@
     from this[unfolded bounded_pos] obtain K where
        K: "0 < K" "\<forall>x\<in>\<Union>d. norm x \<le> K" by auto
     show ?case
-      apply (rule_tac x="K + 1" in exI)
-      apply safe
-    proof -
+    proof (intro conjI impI allI exI)
       fix a b :: 'n
       assume ab: "ball 0 (K + 1) \<subseteq> cbox a b"
-      have *: "\<forall>s s1. ?S - e < s1 \<and> s1 \<le> s \<and> s < ?S + e \<longrightarrow> \<bar>s - ?S\<bar> < e"
+      have *: "\<And>s s1. \<lbrakk>?S - e < s1; s1 \<le> s; s < ?S + e\<rbrakk> \<Longrightarrow> \<bar>s - ?S\<bar> < e"
         by arith
       show "norm (integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - ?S) < e"
         unfolding real_norm_def
-        apply (rule *[rule_format])
-        apply safe
-        apply (rule d)
-      proof goal_cases
-        case 1
+      proof (rule * [OF d])
         have "(\<Sum>k\<in>d. norm (integral k f)) \<le> sum (\<lambda>k. integral k (\<lambda>x. norm (f x))) d"
-          apply (intro sum_mono)
-          subgoal for k
-            using d'(4)[of k] f_int
-            by (auto simp: absolutely_integrable_on_def integral_norm_bound_integral)
-          done
+        proof (intro sum_mono)
+          fix k assume "k \<in> d"
+          with d'(4) f_int show "norm (integral k f) \<le> integral k (\<lambda>x. norm (f x))"
+            by (force simp: absolutely_integrable_on_def integral_norm_bound_integral)
+        qed
         also have "\<dots> = integral (\<Union>d) (\<lambda>x. norm (f x))"
           apply (rule integral_combine_division_bottomup[OF ddiv, symmetric])
           using absolutely_integrable_on_def d'(4) f_int by blast
@@ -2065,7 +2055,8 @@
             using integrable_on_subdivision[OF ddiv] f_int[of a b] unfolding absolutely_integrable_on_def
             by (auto intro!: integral_subset_le)
         qed
-        finally show ?case .
+        finally show "(\<Sum>k\<in>d. norm (integral k f))
+                      \<le> integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0)" .
       next
         have "e/2>0"
           using \<open>e > 0\<close> by auto
@@ -2101,9 +2092,7 @@
           show "(\<Sum>(x,k) \<in> p. norm (integral k f)) \<le> ?S"
             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 D)
-            apply (auto simp: tagged_partial_division_of_def)
+            apply (auto simp: content_eq_0_interior tagged_partial_division_of_def intro!: cSUP_upper2 D)
             done
         qed
         then show "integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
diff -r 89b6455b63b6 -r ca8b18baf0e0 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Aug 25 23:30:36 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Aug 26 00:43:26 2017 +0100
@@ -5610,7 +5610,8 @@
     note integrable_integral[OF this, unfolded has_integral[of f]]
     from this[rule_format,OF *] guess dd..note dd=conjunctD2[OF this,rule_format]
     note gauge_Int[OF \<open>gauge d\<close> dd(1)]
-    from fine_division_exists[OF this,of u v] guess qq .
+    then obtain qq where qq: "qq tagged_division_of cbox u v" "(\<lambda>x. d x \<inter> dd x) fine qq"
+      using fine_division_exists by blast
     then show ?thesis
       apply (rule_tac x=qq in exI)
       using dd(2)[of qq]
@@ -5674,14 +5675,15 @@
   proof -
     fix x l k
     assume as: "(x, l) \<in> p" "(x, l) \<in> qq k" "k \<in> r"
-    note qq[OF this(3)]
-    note tagged_division_ofD(3,4)[OF conjunct1[OF this] as(2)]
-    from this(2) guess u v by (elim exE) note uv=this
-    have "l\<in>snd ` p" unfolding image_iff apply(rule_tac x="(x,l)" in bexI) using as by auto
+    then obtain u v where uv: "l = cbox u v"
+      using p'(4) by blast
+    have "l \<subseteq> k"
+      using  qq[OF as(3)] tagged_division_ofD(3) \<open>(x, l) \<in> qq k\<close> by metis
+    have "l \<in> snd ` p" 
+      using \<open>(x, l) \<in> p\<close> image_iff by fastforce 
     then have "l \<in> q" "k \<in> q" "l \<noteq> k"
       using as(1,3) q(1) unfolding r_def by auto
-    note q'(5)[OF this]
-    then have "interior l = {}"
+    with q'(5) have "interior l = {}"
       using interior_mono[OF \<open>l \<subseteq> k\<close>] by blast
     then show "content l *\<^sub>R f x = 0"
       unfolding uv content_eq_0_interior[symmetric] by auto
@@ -5745,45 +5747,33 @@
   have "?x =  norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p. integral k f))"
     unfolding split_def sum_subtractf ..
   also have "\<dots> \<le> e + k"
-    apply (rule *[OF **, where ir1="sum (\<lambda>k. integral k f) r"])
-  proof goal_cases
-    case 1
+  proof (rule *[OF **])
     have *: "k * real (card r) / (1 + real (card r)) < k"
       using k by (auto simp add: field_simps)
-    show ?case
-      apply (rule le_less_trans[of _ "sum (\<lambda>x. k / (real (card r) + 1)) r"])
-      unfolding sum_subtractf[symmetric]
-      apply (rule sum_norm_le)
-      apply (drule qq)
-      defer
-      unfolding divide_inverse sum_distrib_right[symmetric]
-      unfolding divide_inverse[symmetric]
-      using * apply (auto simp add: field_simps)
-      done
+    have "norm (sum (sum (\<lambda>(x, k). content k *\<^sub>R f x) \<circ> qq) r - (\<Sum>k\<in>r. integral k f))
+          \<le> (\<Sum>x\<in>r. k / (real (card r) + 1))"
+      unfolding sum_subtractf[symmetric] by (force dest: qq intro!: sum_norm_le)
+    also have "... < k"
+      by (simp add: "*" add.commute mult.commute)
+    finally show "norm (sum (sum (\<lambda>(x, k). content k *\<^sub>R f x) \<circ> qq) r - (\<Sum>k\<in>r. integral k f)) < k" .
   next
-    case 2
-    have *: "(\<Sum>(x, k)\<in>p. integral k f) = (\<Sum>k\<in>snd ` p. integral k f)"
-      apply (subst sum.reindex_nontrivial)
-      apply fact
-      unfolding split_paired_all snd_conv split_def o_def
+    from q(1) have [simp]: "snd ` p \<union> q = q" by auto
+    have "integral l f = 0"
+      if inp: "(x, l) \<in> p" "(y, m) \<in> p" and ne: "(x, l) \<noteq> (y, m)" and "l = m" for x l y m
     proof -
-      fix x l y m
-      assume as: "(x, l) \<in> p" "(y, m) \<in> p" "(x, l) \<noteq> (y, m)" "l = m"
-      from p'(4)[OF as(1)] guess u v by (elim exE) note uv=this
-      show "integral l f = 0"
-        unfolding uv
-        apply (rule integral_unique)
-        apply (rule has_integral_null)
-        unfolding content_eq_0_interior
-        using p'(5)[OF as(1-3)]
-        unfolding uv as(4)[symmetric]
-        apply auto
-        done
-    qed auto
-    from q(1) have **: "snd ` p \<union> q = q" by auto
-    show ?case
-      unfolding integral_combine_division_topdown[OF assms(1) q(2)] * r_def
-      using ** q'(1) p'(1) sum.union_disjoint [of "snd ` p" "q - snd ` p" "\<lambda>k. integral k f", symmetric]
+      obtain u v where uv: "l = cbox u v"
+        using inp p'(4) by blast
+      have "content (cbox u v) = 0"
+        unfolding content_eq_0_interior using that p(1) uv by auto
+      then show ?thesis
+        using uv by blast
+    qed
+    then have "(\<Sum>(x, k)\<in>p. integral k f) = (\<Sum>k\<in>snd ` p. integral k f)"
+      apply (subst sum.reindex_nontrivial [OF \<open>finite p\<close>])
+      unfolding split_paired_all split_def by auto
+    then show "(\<Sum>(x, k)\<in>p. integral k f) + (\<Sum>k\<in>r. integral k f) = integral (cbox a b) f"
+      unfolding integral_combine_division_topdown[OF assms(1) q(2)] r_def
+      using q'(1) p'(1) sum.union_disjoint [of "snd ` p" "q - snd ` p", symmetric]
         by simp
   qed
   finally show "?x \<le> e + k" .