# HG changeset patch
# User wenzelm
# Date 1378588166 -7200
# Node ID 0688928a41fdce1c20acf3af868e3efd4105d053
# Parent  8adcf1f0042d309da09a3a55d2b2f1419c676c6b
tuned proofs;

diff -r 8adcf1f0042d -r 0688928a41fd src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Sat Sep 07 20:12:38 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sat Sep 07 23:09:26 2013 +0200
@@ -3404,136 +3404,327 @@
     done
 qed
 
-lemma division_split: fixes a::"'a::ordered_euclidean_space"
-  assumes "p division_of {a..b}" and k:"k\<in>Basis"
-  shows "{l \<inter> {x. x\<bullet>k \<le> c} | l. l \<in> p \<and> ~(l \<inter> {x. x\<bullet>k \<le> c} = {})} division_of({a..b} \<inter> {x. x\<bullet>k \<le> c})" (is "?p1 division_of ?I1") and
-        "{l \<inter> {x. x\<bullet>k \<ge> c} | l. l \<in> p \<and> ~(l \<inter> {x. x\<bullet>k \<ge> c} = {})} division_of ({a..b} \<inter> {x. x\<bullet>k \<ge> c})" (is "?p2 division_of ?I2")
-proof(rule_tac[!] division_ofI) note p=division_ofD[OF assms(1)]
-  show "finite ?p1" "finite ?p2" using p(1) by auto show "\<Union>?p1 = ?I1" "\<Union>?p2 = ?I2" unfolding p(6)[symmetric] by auto
-  { fix k assume "k\<in>?p1" then guess l unfolding mem_Collect_eq apply-by(erule exE,(erule conjE)+) note l=this
-    guess u v using p(4)[OF l(2)] apply-by(erule exE)+ note uv=this
-    show "k\<subseteq>?I1" "k \<noteq> {}" "\<exists>a b. k = {a..b}" unfolding l
-      using p(2-3)[OF l(2)] l(3) unfolding uv apply- prefer 3 apply(subst interval_split[OF k]) by auto
-    fix k' assume "k'\<in>?p1" then guess l' unfolding mem_Collect_eq apply-by(erule exE,(erule conjE)+) note l'=this
-    assume "k\<noteq>k'" thus "interior k \<inter> interior k' = {}" unfolding l l' using p(5)[OF l(2) l'(2)] by auto }
-  { fix k assume "k\<in>?p2" then guess l unfolding mem_Collect_eq apply-by(erule exE,(erule conjE)+) note l=this
-    guess u v using p(4)[OF l(2)] apply-by(erule exE)+ note uv=this
-    show "k\<subseteq>?I2" "k \<noteq> {}" "\<exists>a b. k = {a..b}" unfolding l
-      using p(2-3)[OF l(2)] l(3) unfolding uv apply- prefer 3 apply(subst interval_split[OF k]) by auto
-    fix k' assume "k'\<in>?p2" then guess l' unfolding mem_Collect_eq apply-by(erule exE,(erule conjE)+) note l'=this
-    assume "k\<noteq>k'" thus "interior k \<inter> interior k' = {}" unfolding l l' using p(5)[OF l(2) l'(2)] by auto }
+lemma division_split:
+  fixes a :: "'a::ordered_euclidean_space"
+  assumes "p division_of {a..b}"
+    and k: "k\<in>Basis"
+  shows "{l \<inter> {x. x\<bullet>k \<le> c} | l. l \<in> p \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}} division_of({a..b} \<inter> {x. x\<bullet>k \<le> c})"
+      (is "?p1 division_of ?I1")
+    and "{l \<inter> {x. x\<bullet>k \<ge> c} | l. l \<in> p \<and> l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}} division_of ({a..b} \<inter> {x. x\<bullet>k \<ge> c})"
+      (is "?p2 division_of ?I2")
+proof (rule_tac[!] division_ofI)
+  note p = division_ofD[OF assms(1)]
+  show "finite ?p1" "finite ?p2"
+    using p(1) by auto
+  show "\<Union>?p1 = ?I1" "\<Union>?p2 = ?I2"
+    unfolding p(6)[symmetric] by auto
+  {
+    fix k
+    assume "k \<in> ?p1"
+    then guess l unfolding mem_Collect_eq by (elim exE conjE) note l=this
+    guess u v using p(4)[OF l(2)] by (elim exE) note uv=this
+    show "k \<subseteq> ?I1" "k \<noteq> {}" "\<exists>a b. k = {a..b}"
+      unfolding l
+      using p(2-3)[OF l(2)] l(3)
+      unfolding uv
+      apply -
+      prefer 3
+      apply (subst interval_split[OF k])
+      apply auto
+      done
+    fix k'
+    assume "k' \<in> ?p1"
+    then guess l' unfolding mem_Collect_eq by (elim exE conjE) note l'=this
+    assume "k \<noteq> k'"
+    then show "interior k \<inter> interior k' = {}"
+      unfolding l l' using p(5)[OF l(2) l'(2)] by auto
+  }
+  {
+    fix k
+    assume "k \<in> ?p2"
+    then guess l unfolding mem_Collect_eq by (elim exE conjE) note l=this
+    guess u v using p(4)[OF l(2)] by (elim exE) note uv=this
+    show "k \<subseteq> ?I2" "k \<noteq> {}" "\<exists>a b. k = {a..b}"
+      unfolding l
+      using p(2-3)[OF l(2)] l(3)
+      unfolding uv
+      apply -
+      prefer 3
+      apply (subst interval_split[OF k])
+      apply auto
+      done
+    fix k'
+    assume "k' \<in> ?p2"
+    then guess l' unfolding mem_Collect_eq by (elim exE conjE) note l'=this
+    assume "k \<noteq> k'"
+    then show "interior k \<inter> interior k' = {}"
+      unfolding l l' using p(5)[OF l(2) l'(2)] by auto
+  }
 qed
 
-lemma has_integral_split: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
-  assumes "(f has_integral i) ({a..b} \<inter> {x. x\<bullet>k \<le> c})"  "(f has_integral j) ({a..b} \<inter> {x. x\<bullet>k \<ge> c})" and k:"k\<in>Basis"
+lemma has_integral_split:
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
+  assumes "(f has_integral i) ({a..b} \<inter> {x. x\<bullet>k \<le> c})"
+    and "(f has_integral j) ({a..b} \<inter> {x. x\<bullet>k \<ge> c})"
+    and k: "k \<in> Basis"
   shows "(f has_integral (i + j)) ({a..b})"
-proof(unfold has_integral,rule,rule) case goal1 hence e:"e/2>0" by auto
+proof (unfold has_integral, rule, rule)
+  case goal1
+  then have e: "e/2 > 0"
+    by auto
   guess d1 using has_integralD[OF assms(1)[unfolded interval_split[OF k]] e] . note d1=this[unfolded interval_split[symmetric,OF k]]
   guess d2 using has_integralD[OF assms(2)[unfolded interval_split[OF k]] e] . note d2=this[unfolded interval_split[symmetric,OF k]]
   let ?d = "\<lambda>x. if x\<bullet>k = c then (d1 x \<inter> d2 x) else ball x (abs(x\<bullet>k - c)) \<inter> d1 x \<inter> d2 x"
-  show ?case apply(rule_tac x="?d" in exI,rule) defer apply(rule,rule,(erule conjE)+)
-  proof- show "gauge ?d" using d1(1) d2(1) unfolding gauge_def by auto
-    fix p assume "p tagged_division_of {a..b}" "?d fine p" note p = this tagged_division_ofD[OF this(1)]
-    have lem0:"\<And>x kk. (x,kk) \<in> p \<Longrightarrow> ~(kk \<inter> {x. x\<bullet>k \<le> c} = {}) \<Longrightarrow> x\<bullet>k \<le> c"
-         "\<And>x kk. (x,kk) \<in> p \<Longrightarrow> ~(kk \<inter> {x. x\<bullet>k \<ge> c} = {}) \<Longrightarrow> x\<bullet>k \<ge> c"
-    proof- fix x kk assume as:"(x,kk)\<in>p"
-      show "~(kk \<inter> {x. x\<bullet>k \<le> c} = {}) \<Longrightarrow> x\<bullet>k \<le> c"
-      proof(rule ccontr) case goal1
-        from this(2)[unfolded not_le] have "kk \<subseteq> ball x \<bar>x \<bullet> k - c\<bar>"
-          using p(2)[unfolded fine_def,rule_format,OF as,unfolded split_conv] by auto
-        hence "\<exists>y. y \<in> ball x \<bar>x \<bullet> k - c\<bar> \<inter> {x. x \<bullet> k \<le> c}" using goal1(1) by blast
-        then guess y .. hence "\<bar>x \<bullet> k - y \<bullet> k\<bar> < \<bar>x \<bullet> k - c\<bar>" "y\<bullet>k \<le> c" apply-apply(rule le_less_trans)
-          using Basis_le_norm[OF k, of "x - y"] by (auto simp add: dist_norm inner_diff_left)
-        thus False using goal1(2)[unfolded not_le] by(auto simp add:field_simps)
-      qed
-      show "~(kk \<inter> {x. x\<bullet>k \<ge> c} = {}) \<Longrightarrow> x\<bullet>k \<ge> c"
-      proof(rule ccontr) case goal1
-        from this(2)[unfolded not_le] have "kk \<subseteq> ball x \<bar>x \<bullet> k - c\<bar>"
-          using p(2)[unfolded fine_def,rule_format,OF as,unfolded split_conv] by auto
-        hence "\<exists>y. y \<in> ball x \<bar>x \<bullet> k - c\<bar> \<inter> {x. x \<bullet> k \<ge> c}" using goal1(1) by blast
-        then guess y .. hence "\<bar>x \<bullet> k - y \<bullet> k\<bar> < \<bar>x \<bullet> k - c\<bar>" "y\<bullet>k \<ge> c" apply-apply(rule le_less_trans)
-          using Basis_le_norm[OF k, of "x - y"] by (auto simp add: dist_norm inner_diff_left)
-        thus False using goal1(2)[unfolded not_le] by(auto simp add:field_simps)
+  show ?case
+    apply (rule_tac x="?d" in exI)
+    apply rule
+    defer
+    apply rule
+    apply rule
+    apply (elim conjE)
+  proof -
+    show "gauge ?d"
+      using d1(1) d2(1) unfolding gauge_def by auto
+    fix p
+    assume "p tagged_division_of {a..b}" "?d fine p" note p = this tagged_division_ofD[OF this(1)]
+    have lem0:
+      "\<And>x kk. (x, kk) \<in> p \<Longrightarrow> kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {} \<Longrightarrow> x\<bullet>k \<le> c"
+      "\<And>x kk. (x, kk) \<in> p \<Longrightarrow> kk \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {} \<Longrightarrow> x\<bullet>k \<ge> c"
+    proof -
+      fix x kk
+      assume as: "(x, kk) \<in> p"
+      {
+        assume *: "kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}"
+        show "x\<bullet>k \<le> c"
+        proof (rule ccontr)
+          assume **: "\<not> ?thesis"
+          from this[unfolded not_le]
+          have "kk \<subseteq> ball x \<bar>x \<bullet> k - c\<bar>"
+            using p(2)[unfolded fine_def, rule_format,OF as,unfolded split_conv] by auto
+          with * have "\<exists>y. y \<in> ball x \<bar>x \<bullet> k - c\<bar> \<inter> {x. x \<bullet> k \<le> c}"
+            by blast
+          then guess y ..
+          then have "\<bar>x \<bullet> k - y \<bullet> k\<bar> < \<bar>x \<bullet> k - c\<bar>" "y\<bullet>k \<le> c"
+            apply -
+            apply (rule le_less_trans)
+            using Basis_le_norm[OF k, of "x - y"]
+            apply (auto simp add: dist_norm inner_diff_left)
+            done
+          then show False
+            using **[unfolded not_le] by (auto simp add: field_simps)
+        qed
+      next
+        assume *: "kk \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}"
+        show "x\<bullet>k \<ge> c"
+        proof (rule ccontr)
+          assume **: "\<not> ?thesis"
+          from this[unfolded not_le] have "kk \<subseteq> ball x \<bar>x \<bullet> k - c\<bar>"
+            using p(2)[unfolded fine_def,rule_format,OF as,unfolded split_conv] by auto
+          with * have "\<exists>y. y \<in> ball x \<bar>x \<bullet> k - c\<bar> \<inter> {x. x \<bullet> k \<ge> c}"
+            by blast
+          then guess y ..
+          then have "\<bar>x \<bullet> k - y \<bullet> k\<bar> < \<bar>x \<bullet> k - c\<bar>" "y\<bullet>k \<ge> c"
+            apply -
+            apply (rule le_less_trans)
+            using Basis_le_norm[OF k, of "x - y"]
+            apply (auto simp add: dist_norm inner_diff_left)
+            done
+          then show False
+            using **[unfolded not_le] by (auto simp add: field_simps)
+        qed
+      }
+    qed
+
+    have lem1: "\<And>f P Q. (\<forall>x k. (x, k) \<in> {(x, f k) | x k. P x k} \<longrightarrow> Q x k) \<longleftrightarrow>
+      (\<forall>x k. P x k \<longrightarrow> Q x (f k))" by auto
+    have lem2: "\<And>f s P f. finite s \<Longrightarrow> finite {(x,f k) | x k. (x,k) \<in> s \<and> P x k}"
+    proof -
+      case goal1
+      then show ?case
+        apply -
+        apply (rule finite_subset[of _ "(\<lambda>(x,k). (x,f k)) ` s"])
+        apply auto
+        done
+    qed
+    have lem3: "\<And>g :: 'a set \<Rightarrow> 'a set. finite p \<Longrightarrow>
+      setsum (\<lambda>(x, k). content k *\<^sub>R f x) {(x,g k) |x k. (x,k) \<in> p \<and> g k \<noteq> {}} =
+      setsum (\<lambda>(x, k). content k *\<^sub>R f x) ((\<lambda>(x, k). (x, g k)) ` p)"
+      apply (rule setsum_mono_zero_left)
+      prefer 3
+    proof
+      fix g :: "'a set \<Rightarrow> 'a set"
+      fix i :: "'a \<times> 'a set"
+      assume "i \<in> (\<lambda>(x, k). (x, g k)) ` p - {(x, g k) |x k. (x, k) \<in> p \<and> g k \<noteq> {}}"
+      then obtain x k where xk:
+        "i = (x, g k)"
+        "(x, k) \<in> p"
+        "(x, g k) \<notin> {(x, g k) |x k. (x, k) \<in> p \<and> g k \<noteq> {}}"
+        by auto
+      have "content (g k) = 0"
+        using xk using content_empty by auto
+      then show "(\<lambda>(x, k). content k *\<^sub>R f x) i = 0"
+        unfolding xk split_conv by auto
+    qed auto
+    have lem4: "\<And>g. (\<lambda>(x,l). content (g l) *\<^sub>R f x) = (\<lambda>(x,l). content l *\<^sub>R f x) \<circ> (\<lambda>(x,l). (x,g l))"
+      by auto
+
+    let ?M1 = "{(x, kk \<inter> {x. x\<bullet>k \<le> c}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}}"
+    have "norm ((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) < e/2"
+      apply (rule d1(2),rule tagged_division_ofI)
+      apply (rule lem2 p(3))+
+      prefer 6
+      apply (rule fineI)
+    proof -
+      show "\<Union>{k. \<exists>x. (x, k) \<in> ?M1} = {a..b} \<inter> {x. x\<bullet>k \<le> c}"
+        unfolding p(8)[symmetric] by auto
+      fix x l
+      assume xl: "(x, l) \<in> ?M1"
+      then guess x' l' unfolding mem_Collect_eq unfolding Pair_eq by (elim exE conjE) note xl'=this
+      have "l' \<subseteq> d1 x'"
+        apply (rule order_trans[OF fineD[OF p(2) xl'(3)]])
+        apply auto
+        done
+      then show "l \<subseteq> d1 x"
+        unfolding xl' by auto
+      show "x \<in> l" "l \<subseteq> {a..b} \<inter> {x. x \<bullet> k \<le> c}"
+        unfolding xl'
+        using p(4-6)[OF xl'(3)] using xl'(4)
+        using lem0(1)[OF xl'(3-4)] by auto
+      show "\<exists>a b. l = {a..b}"
+        unfolding xl'
+        using p(6)[OF xl'(3)]
+        by (fastforce simp add: interval_split[OF k,where c=c])
+      fix y r
+      let ?goal = "interior l \<inter> interior r = {}"
+      assume yr: "(y, r) \<in> ?M1"
+      then guess y' r' unfolding mem_Collect_eq unfolding Pair_eq by (elim exE conjE) note yr'=this
+      assume as: "(x, l) \<noteq> (y, r)"
+      show "interior l \<inter> interior r = {}"
+      proof (cases "l' = r' \<longrightarrow> x' = y'")
+        case False
+        then show ?thesis
+          using p(7)[OF xl'(3) yr'(3)] using as unfolding xl' yr' by auto
+      next
+        case True
+        then have "l' \<noteq> r'"
+          using as unfolding xl' yr' by auto
+        then show ?thesis
+          using p(7)[OF xl'(3) yr'(3)] using as unfolding xl' yr' by auto
       qed
     qed
-
-    have lem1: "\<And>f P Q. (\<forall>x k. (x,k) \<in> {(x,f k) | x k. P x k} \<longrightarrow> Q x k) \<longleftrightarrow> (\<forall>x k. P x k \<longrightarrow> Q x (f k))" by auto
-    have lem2: "\<And>f s P f. finite s \<Longrightarrow> finite {(x,f k) | x k. (x,k) \<in> s \<and> P x k}"
-    proof- case goal1 thus ?case apply-apply(rule finite_subset[of _ "(\<lambda>(x,k). (x,f k)) ` s"]) by auto qed
-    have lem3: "\<And>g::'a set \<Rightarrow> 'a set. finite p \<Longrightarrow>
-      setsum (\<lambda>(x,k). content k *\<^sub>R f x) {(x,g k) |x k. (x,k) \<in> p \<and> ~(g k = {})}
-               = setsum (\<lambda>(x,k). content k *\<^sub>R f x) ((\<lambda>(x,k). (x,g k)) ` p)"
-      apply(rule setsum_mono_zero_left) prefer 3
-    proof fix g::"'a set \<Rightarrow> 'a set" and i::"('a) \<times> (('a) set)"
-      assume "i \<in> (\<lambda>(x, k). (x, g k)) ` p - {(x, g k) |x k. (x, k) \<in> p \<and> g k \<noteq> {}}"
-      then obtain x k where xk:"i=(x,g k)" "(x,k)\<in>p" "(x,g k) \<notin> {(x, g k) |x k. (x, k) \<in> p \<and> g k \<noteq> {}}" by auto
-      have "content (g k) = 0" using xk using content_empty by auto
-      thus "(\<lambda>(x, k). content k *\<^sub>R f x) i = 0" unfolding xk split_conv by auto
-    qed auto
-    have lem4:"\<And>g. (\<lambda>(x,l). content (g l) *\<^sub>R f x) = (\<lambda>(x,l). content l *\<^sub>R f x) o (\<lambda>(x,l). (x,g l))" apply(rule ext) by auto
-
-    let ?M1 = "{(x,kk \<inter> {x. x\<bullet>k \<le> c}) |x kk. (x,kk) \<in> p \<and> kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}}"
-    have "norm ((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) < e/2" apply(rule d1(2),rule tagged_division_ofI)
-      apply(rule lem2 p(3))+ prefer 6 apply(rule fineI)
-    proof- show "\<Union>{k. \<exists>x. (x, k) \<in> ?M1} = {a..b} \<inter> {x. x\<bullet>k \<le> c}" unfolding p(8)[symmetric] by auto
-      fix x l assume xl:"(x,l)\<in>?M1"
-      then guess x' l' unfolding mem_Collect_eq apply- unfolding Pair_eq apply((erule exE)+,(erule conjE)+) .  note xl'=this
-      have "l' \<subseteq> d1 x'" apply(rule order_trans[OF fineD[OF p(2) xl'(3)]]) by auto
-      thus "l \<subseteq> d1 x" unfolding xl' by auto
-      show "x\<in>l" "l \<subseteq> {a..b} \<inter> {x. x \<bullet> k \<le> c}" unfolding xl' using p(4-6)[OF xl'(3)] using xl'(4)
-        using lem0(1)[OF xl'(3-4)] by auto
-      show  "\<exists>a b. l = {a..b}" unfolding xl' using p(6)[OF xl'(3)] by(fastforce simp add: interval_split[OF k,where c=c])
-      fix y r let ?goal = "interior l \<inter> interior r = {}" assume yr:"(y,r)\<in>?M1"
-      then guess y' r' unfolding mem_Collect_eq apply- unfolding Pair_eq apply((erule exE)+,(erule conjE)+) .  note yr'=this
-      assume as:"(x,l) \<noteq> (y,r)" show "interior l \<inter> interior r = {}"
-      proof(cases "l' = r' \<longrightarrow> x' = y'")
-        case False thus ?thesis using p(7)[OF xl'(3) yr'(3)] using as unfolding xl' yr' by auto
-      next case True hence "l' \<noteq> r'" using as unfolding xl' yr' by auto
-        thus ?thesis using p(7)[OF xl'(3) yr'(3)] using as unfolding xl' yr' by auto
-      qed qed moreover
-
+    moreover
     let ?M2 = "{(x,kk \<inter> {x. x\<bullet>k \<ge> c}) |x kk. (x,kk) \<in> p \<and> kk \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}}"
-    have "norm ((\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - j) < e/2" apply(rule d2(2),rule tagged_division_ofI)
-      apply(rule lem2 p(3))+ prefer 6 apply(rule fineI)
-    proof- show "\<Union>{k. \<exists>x. (x, k) \<in> ?M2} = {a..b} \<inter> {x. x\<bullet>k \<ge> c}" unfolding p(8)[symmetric] by auto
-      fix x l assume xl:"(x,l)\<in>?M2"
-      then guess x' l' unfolding mem_Collect_eq apply- unfolding Pair_eq apply((erule exE)+,(erule conjE)+) .  note xl'=this
-      have "l' \<subseteq> d2 x'" apply(rule order_trans[OF fineD[OF p(2) xl'(3)]]) by auto
-      thus "l \<subseteq> d2 x" unfolding xl' by auto
-      show "x\<in>l" "l \<subseteq> {a..b} \<inter> {x. x \<bullet> k \<ge> c}" unfolding xl' using p(4-6)[OF xl'(3)] using xl'(4)
-        using lem0(2)[OF xl'(3-4)] by auto
-      show  "\<exists>a b. l = {a..b}" unfolding xl' using p(6)[OF xl'(3)] by(fastforce simp add: interval_split[OF k, where c=c])
-      fix y r let ?goal = "interior l \<inter> interior r = {}" assume yr:"(y,r)\<in>?M2"
-      then guess y' r' unfolding mem_Collect_eq apply- unfolding Pair_eq apply((erule exE)+,(erule conjE)+) .  note yr'=this
-      assume as:"(x,l) \<noteq> (y,r)" show "interior l \<inter> interior r = {}"
-      proof(cases "l' = r' \<longrightarrow> x' = y'")
-        case False thus ?thesis using p(7)[OF xl'(3) yr'(3)] using as unfolding xl' yr' by auto
-      next case True hence "l' \<noteq> r'" using as unfolding xl' yr' by auto
-        thus ?thesis using p(7)[OF xl'(3) yr'(3)] using as unfolding xl' yr' by auto
-      qed qed ultimately
-
+    have "norm ((\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - j) < e/2"
+      apply (rule d2(2),rule tagged_division_ofI)
+      apply (rule lem2 p(3))+
+      prefer 6
+      apply (rule fineI)
+    proof -
+      show "\<Union>{k. \<exists>x. (x, k) \<in> ?M2} = {a..b} \<inter> {x. x\<bullet>k \<ge> c}"
+        unfolding p(8)[symmetric] by auto
+      fix x l
+      assume xl: "(x, l) \<in> ?M2"
+      then guess x' l' unfolding mem_Collect_eq unfolding Pair_eq by (elim exE conjE) note xl'=this
+      have "l' \<subseteq> d2 x'"
+        apply (rule order_trans[OF fineD[OF p(2) xl'(3)]])
+        apply auto
+        done
+      then show "l \<subseteq> d2 x"
+        unfolding xl' by auto
+      show "x \<in> l" "l \<subseteq> {a..b} \<inter> {x. x \<bullet> k \<ge> c}"
+        unfolding xl'
+        using p(4-6)[OF xl'(3)]
+        using xl'(4)
+        using lem0(2)[OF xl'(3-4)]
+        by auto
+      show "\<exists>a b. l = {a..b}"
+        unfolding xl'
+        using p(6)[OF xl'(3)]
+        by (fastforce simp add: interval_split[OF k, where c=c])
+      fix y r
+      let ?goal = "interior l \<inter> interior r = {}"
+      assume yr: "(y, r) \<in> ?M2"
+      then guess y' r' unfolding mem_Collect_eq unfolding Pair_eq by (elim exE conjE) note yr'=this
+      assume as: "(x, l) \<noteq> (y, r)"
+      show "interior l \<inter> interior r = {}"
+      proof (cases "l' = r' \<longrightarrow> x' = y'")
+        case False
+        then show ?thesis
+          using p(7)[OF xl'(3) yr'(3)] using as unfolding xl' yr' by auto
+      next
+        case True
+        then have "l' \<noteq> r'"
+          using as unfolding xl' yr' by auto
+        then show ?thesis
+          using p(7)[OF xl'(3) yr'(3)] using as unfolding xl' yr' by auto
+      qed
+    qed
+    ultimately
     have "norm (((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) + ((\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - j)) < e/2 + e/2"
-      apply- apply(rule norm_triangle_lt) by auto
-    also { have *:"\<And>x y. x = (0::real) \<Longrightarrow> x *\<^sub>R (y::'b) = 0" using scaleR_zero_left by auto
-      have "((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) + ((\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - j)
-       = (\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - (i + j)" by auto
+      apply -
+      apply (rule norm_triangle_lt)
+      apply auto
+      done
+    also {
+      have *: "\<And>x y. x = (0::real) \<Longrightarrow> x *\<^sub>R (y::'b) = 0"
+        using scaleR_zero_left by auto
+      have "((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) + ((\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - j) =
+        (\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - (i + j)"
+        by auto
       also have "\<dots> = (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f x) +
         (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f x) - (i + j)"
-        unfolding lem3[OF p(3)] apply(subst setsum_reindex_nonzero[OF p(3)]) defer apply(subst setsum_reindex_nonzero[OF p(3)])
-        defer unfolding lem4[symmetric] apply(rule refl) unfolding split_paired_all split_conv apply(rule_tac[!] *)
-      proof- case goal1 thus ?case apply- apply(rule tagged_division_split_left_inj [OF p(1), of a b aa ba]) using k by auto
-      next case   goal2 thus ?case apply- apply(rule tagged_division_split_right_inj[OF p(1), of a b aa ba]) using k by auto
-      qed also note setsum_addf[symmetric]
-      also have *:"\<And>x. x\<in>p \<Longrightarrow> (\<lambda>(x, ka). content (ka \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f x) x + (\<lambda>(x, ka). content (ka \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f x) x
-        = (\<lambda>(x,ka). content ka *\<^sub>R f x) x" unfolding split_paired_all split_conv
-      proof- fix a b assume "(a,b) \<in> p" from p(6)[OF this] guess u v apply-by(erule exE)+ note uv=this
-        thus "content (b \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f a + content (b \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f a = content b *\<^sub>R f a"
-          unfolding scaleR_left_distrib[symmetric] unfolding uv content_split[OF k,of u v c] by auto
-      qed note setsum_cong2[OF this]
+        unfolding lem3[OF p(3)]
+        apply (subst setsum_reindex_nonzero[OF p(3)])
+        defer
+        apply(subst setsum_reindex_nonzero[OF p(3)])
+        defer
+        unfolding lem4[symmetric]
+        apply (rule refl)
+        unfolding split_paired_all split_conv
+        apply (rule_tac[!] *)
+      proof -
+        case goal1
+        then show ?case
+          apply -
+          apply (rule tagged_division_split_left_inj [OF p(1), of a b aa ba])
+          using k
+          apply auto
+          done
+      next
+        case goal2
+        then show ?case
+          apply -
+          apply (rule tagged_division_split_right_inj[OF p(1), of a b aa ba])
+          using k
+          apply auto
+          done
+      qed
+      also note setsum_addf[symmetric]
+      also have *: "\<And>x. x \<in> p \<Longrightarrow>
+        (\<lambda>(x,ka). content (ka \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f x) x + (\<lambda>(x,ka). content (ka \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f x) x =
+        (\<lambda>(x,ka). content ka *\<^sub>R f x) x"
+        unfolding split_paired_all split_conv
+      proof -
+        fix a b
+        assume "(a, b) \<in> p"
+        from p(6)[OF this] guess u v by (elim exE) note uv=this
+        then show "content (b \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f a + content (b \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f a =
+          content b *\<^sub>R f a"
+          unfolding scaleR_left_distrib[symmetric]
+          unfolding uv content_split[OF k,of u v c]
+          by auto
+      qed
+      note setsum_cong2[OF this]
       finally have "(\<Sum>(x, k)\<in>{(x, kk \<inter> {x. x \<bullet> k \<le> c}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. x \<bullet> k \<le> c} \<noteq> {}}. content k *\<^sub>R f x) - i +
         ((\<Sum>(x, k)\<in>{(x, kk \<inter> {x. c \<le> x \<bullet> k}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. c \<le> x \<bullet> k} \<noteq> {}}. content k *\<^sub>R f x) - j) =
-        (\<Sum>(x, ka)\<in>p. content ka *\<^sub>R f x) - (i + j)" by auto }
-    finally show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - (i + j)) < e" by auto qed qed
+        (\<Sum>(x, ka)\<in>p. content ka *\<^sub>R f x) - (i + j)"
+        by auto
+    }
+    finally show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - (i + j)) < e"
+      by auto
+  qed
+qed
+
 
 subsection {* A sort of converse, integrability on subintervals. *}