# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1503948788 -3600
# Node ID e2249cd6df67db38e45945f5abd55ea7286de5a0
# Parent  9c95b2b54337eec4720760440d97fc974371b4e6
sorted out cases in negligible_standard_hyperplane

diff -r 9c95b2b54337 -r e2249cd6df67 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Aug 28 20:02:43 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Aug 28 20:33:08 2017 +0100
@@ -1988,7 +1988,7 @@
   unfolding negligible_def has_integral
 proof clarsimp
   fix a b and e::real assume "e > 0"
-  with k obtain d where d: "0 < d" "content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) < e"
+  with k obtain d where "0 < d" and d: "content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) < e"
     by (metis content_doublesplit)
   let ?i = "indicator {x::'a. x\<bullet>k = c} :: 'a\<Rightarrow>real"
   show "\<exists>\<gamma>. gauge \<gamma> \<and>
@@ -1996,22 +1996,15 @@
                  \<bar>\<Sum>(x,K) \<in> \<D>. content K * ?i x\<bar> < e)"
   proof (intro exI, safe)
     show "gauge (\<lambda>x. ball x d)"
-      using d(1) by blast
+      using \<open>0 < d\<close> by blast
   next
     fix \<D>
     assume p: "\<D> tagged_division_of (cbox a b)" "(\<lambda>x. ball x d) fine \<D>"
-    have *: "(\<Sum>(x,K)\<in>\<D>. content K * ?i x) = (\<Sum>(x,K)\<in>\<D>. content (K \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d}) *\<^sub>R ?i x)"
-      apply (rule sum.cong [OF refl])
-      unfolding split_paired_all real_scaleR_def mult_cancel_right split_conv
-      apply cases
-       apply (rule disjI1)
-       apply assumption
-      apply (rule disjI2)
+    have "content l = content (l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})" 
+      if "(x, l) \<in> \<D>" "?i x \<noteq> 0" for x l
     proof -
-      fix x l
-      assume as: "(x, l) \<in> \<D>" "?i x \<noteq> 0"
-      then have xk: "x\<bullet>k = c"
-        by (simp add: indicator_def split: if_split_asm)
+      have xk: "x\<bullet>k = c"
+        using that by (simp add: indicator_def split: if_split_asm)
       show "content l = content (l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})"
         apply (rule arg_cong[where f=content])
         apply (rule set_eqI)
@@ -2021,13 +2014,15 @@
       proof -
         fix y
         assume y: "y \<in> l"
-        note p(2)[unfolded fine_def,rule_format,OF as(1),unfolded split_conv]
+        note p(2)[unfolded fine_def,rule_format,OF that(1),unfolded split_conv]
         note this[unfolded subset_eq mem_ball dist_norm,rule_format,OF y]
         note le_less_trans[OF Basis_le_norm[OF k] this]
         then show "\<bar>y \<bullet> k - c\<bar> \<le> d"
           unfolding inner_simps xk by auto
       qed auto
     qed
+    then have *: "(\<Sum>(x,K)\<in>\<D>. content K * ?i x) = (\<Sum>(x,K)\<in>\<D>. content (K \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d}) *\<^sub>R ?i x)"
+      by (force simp add: split_paired_all intro!: sum.cong [OF refl])
     note p'= tagged_division_ofD[OF p(1)] and p''=division_of_tagged_division[OF p(1)]
     have "(\<Sum>(x,K)\<in>\<D>. content (K \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * indicator {x. x \<bullet> k = c} x) < e"
     proof -
@@ -2044,12 +2039,10 @@
         case prems: (1 u v)
         then have *: "content (cbox u v) = 0"
           unfolding content_eq_0_interior by simp
-        have "content (cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<le> content (cbox u v)"
-          unfolding interval_doublesplit[OF k]
-          apply (rule content_subset)
-          unfolding interval_doublesplit[symmetric,OF k]
-          apply auto
-          done
+        have "cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<subseteq> cbox u v"
+          by auto
+        then have "content (cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<le> content (cbox u v)"
+          unfolding interval_doublesplit[OF k] by (rule content_subset)
         then show ?case
           unfolding * interval_doublesplit[OF k]
           by (blast intro: antisym)
@@ -2076,7 +2069,7 @@
           using division_doublesplit[OF p'' k, unfolded interval_doublesplit[OF k]]
           unfolding interval_doublesplit[OF k] by (intro dsum_bound) auto
         also have "\<dots> < e"
-          using d(2) by simp
+          using d by simp
         finally show "(\<Sum>K\<in>snd ` \<D>. content (K \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) < e" .
       qed
       finally show "(\<Sum>(x, K)\<in>\<D>. content (K \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) < e" .