# HG changeset patch
# User wenzelm
# Date 1378765332 -7200
# Node ID cd25f20a797f44ceb409f511438968ee5eaad30c
# Parent  9770b0627de4c3714c9ba8ceb31bff8edea5ccc0# Parent  fd977a1574dc75b19df0aad378aa4ec90a9b4bbe
merged

diff -r 9770b0627de4 -r cd25f20a797f src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Sep 09 23:55:35 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Sep 10 00:22:12 2013 +0200
@@ -2999,7 +2999,7 @@
   done
 
 lemma integrable_setsum:
-  "finite t \<Longrightarrow> \<forall>a \<in> t.(f a) integrable_on s \<Longrightarrow> (\<lambda>x. setsum (\<lambda>a. f a x) t) integrable_on s"
+  "finite t \<Longrightarrow> \<forall>a \<in> t. (f a) integrable_on s \<Longrightarrow> (\<lambda>x. setsum (\<lambda>a. f a x) t) integrable_on s"
   unfolding integrable_on_def
   apply (drule bchoice)
   using has_integral_setsum[of t]
@@ -3141,7 +3141,12 @@
   proof (rule, rule)
     case goal1
     then have "e/2 > 0" by auto
-    then guess d apply- apply(drule y[rule_format]) by(erule exE,erule conjE) note d=this[rule_format]
+    then guess d
+      apply -
+      apply (drule y[rule_format])
+      apply (elim exE conjE)
+      done
+    note d=this[rule_format]
     show ?case
       apply (rule_tac x=d in exI)
       apply rule
@@ -3215,7 +3220,8 @@
       by auto
     guess N2 using y[OF *] .. note N2=this
     show "\<exists>d. gauge d \<and>
-      (\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - y) < e)"
+      (\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow>
+        norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - y) < e)"
       apply (rule_tac x="d (N1 + N2)" in exI)
       apply rule
       defer
@@ -3315,7 +3321,8 @@
   shows "content(k1 \<inter> {x. x\<bullet>k \<le> c}) = 0"
 proof -
   note d=division_ofD[OF assms(1)]
-  have *: "\<And>a b::'a. \<And> c. (content({a..b} \<inter> {x. x\<bullet>k \<le> c}) = 0 \<longleftrightarrow> interior({a..b} \<inter> {x. x\<bullet>k \<le> c}) = {})"
+  have *: "\<And>(a::'a) b c. content ({a..b} \<inter> {x. x\<bullet>k \<le> c}) = 0 \<longleftrightarrow>
+    interior({a..b} \<inter> {x. x\<bullet>k \<le> c}) = {}"
     unfolding  interval_split[OF k] content_eq_0_interior by auto
   guess u1 v1 using d(4)[OF assms(2)] apply-by(erule exE)+ note uv1=this
   guess u2 v2 using d(4)[OF assms(3)] apply-by(erule exE)+ note uv2=this
@@ -3344,8 +3351,8 @@
   have *: "\<And>a b::'a. \<And>c. content({a..b} \<inter> {x. x\<bullet>k \<ge> c}) = 0 \<longleftrightarrow>
     interior({a..b} \<inter> {x. x\<bullet>k \<ge> c}) = {}"
     unfolding interval_split[OF k] content_eq_0_interior by auto
-  guess u1 v1 using d(4)[OF assms(2)] apply-by(erule exE)+ note uv1=this
-  guess u2 v2 using d(4)[OF assms(3)] apply-by(erule exE)+ note uv2=this
+  guess u1 v1 using d(4)[OF assms(2)] by (elim exE) note uv1=this
+  guess u2 v2 using d(4)[OF assms(3)] by (elim exE) note uv2=this
   have **: "\<And>s t u. s \<inter> t = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<subseteq> t \<Longrightarrow> u = {}"
     by auto
   show ?thesis
@@ -3361,7 +3368,7 @@
 lemma tagged_division_split_left_inj:
   fixes x1 :: "'a::ordered_euclidean_space"
   assumes "d tagged_division_of i"
-    and "(x1,k1) \<in> d"
+    and "(x1, k1) \<in> d"
     and "(x2, k2) \<in> d"
     and "k1 \<noteq> k2"
     and "k1 \<inter> {x. x\<bullet>k \<le> c} = k2 \<inter> {x. x\<bullet>k \<le> c}"
@@ -3389,7 +3396,7 @@
     and "k1 \<noteq> k2"
     and "k1 \<inter> {x. x\<bullet>k \<ge> c} = k2 \<inter> {x. x\<bullet>k \<ge> c}"
   and k: "k \<in> Basis"
-  shows "content(k1 \<inter> {x. x\<bullet>k \<ge> c}) = 0"
+  shows "content (k1 \<inter> {x. x\<bullet>k \<ge> c}) = 0"
 proof -
   have *: "\<And>a b c. (a,b) \<in> c \<Longrightarrow> b \<in> snd ` c"
     unfolding image_iff
@@ -3472,8 +3479,10 @@
   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]]
+  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)
@@ -3486,7 +3495,8 @@
     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)]
+    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"
@@ -3701,7 +3711,8 @@
       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 \<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 -
@@ -3728,170 +3739,296 @@
 
 subsection {* A sort of converse, integrability on subintervals. *}
 
-lemma tagged_division_union_interval: fixes a::"'a::ordered_euclidean_space"
-  assumes "p1 tagged_division_of ({a..b} \<inter> {x. x\<bullet>k \<le> (c::real)})"  "p2 tagged_division_of ({a..b} \<inter> {x. x\<bullet>k \<ge> c})"
-  and k:"k\<in>Basis"
+lemma tagged_division_union_interval:
+  fixes a :: "'a::ordered_euclidean_space"
+  assumes "p1 tagged_division_of ({a..b} \<inter> {x. x\<bullet>k \<le> (c::real)})"
+    and "p2 tagged_division_of ({a..b} \<inter> {x. x\<bullet>k \<ge> c})"
+    and k: "k \<in> Basis"
   shows "(p1 \<union> p2) tagged_division_of ({a..b})"
-proof- have *:"{a..b} = ({a..b} \<inter> {x. x\<bullet>k \<le> c}) \<union> ({a..b} \<inter> {x. x\<bullet>k \<ge> c})" by auto
-  show ?thesis apply(subst *) apply(rule tagged_division_union[OF assms(1-2)])
-    unfolding interval_split[OF k] interior_closed_interval using k
-    by(auto simp add: eucl_less[where 'a='a] elim!: ballE[where x=k]) qed
-
-lemma has_integral_separate_sides: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
-  assumes "(f has_integral i) ({a..b})" "e>0" and k:"k\<in>Basis"
-  obtains d where "gauge d" "(\<forall>p1 p2. p1 tagged_division_of ({a..b} \<inter> {x. x\<bullet>k \<le> c}) \<and> d fine p1 \<and>
-                                p2 tagged_division_of ({a..b} \<inter> {x. x\<bullet>k \<ge> c}) \<and> d fine p2
-                                \<longrightarrow> norm((setsum (\<lambda>(x,k). content k *\<^sub>R f x) p1 +
-                                          setsum (\<lambda>(x,k). content k *\<^sub>R f x) p2) - i) < e)"
-proof- guess d using has_integralD[OF assms(1-2)] . note d=this
-  show ?thesis apply(rule that[of d]) apply(rule d) apply(rule,rule,rule,(erule conjE)+)
-  proof- fix p1 p2 assume "p1 tagged_division_of {a..b} \<inter> {x. x \<bullet> k \<le> c}" "d fine p1" note p1=tagged_division_ofD[OF this(1)] this
-                   assume "p2 tagged_division_of {a..b} \<inter> {x. c \<le> x \<bullet> k}" "d fine p2" note p2=tagged_division_ofD[OF this(1)] this
+proof -
+  have *: "{a..b} = ({a..b} \<inter> {x. x\<bullet>k \<le> c}) \<union> ({a..b} \<inter> {x. x\<bullet>k \<ge> c})"
+    by auto
+  show ?thesis
+    apply (subst *)
+    apply (rule tagged_division_union[OF assms(1-2)])
+    unfolding interval_split[OF k] interior_closed_interval
+    using k
+    apply (auto simp add: eucl_less[where 'a='a] elim!: ballE[where x=k])
+    done
+qed
+
+lemma has_integral_separate_sides:
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
+  assumes "(f has_integral i) ({a..b})"
+    and "e > 0"
+    and k: "k \<in> Basis"
+  obtains d where "gauge d"
+    "\<forall>p1 p2. p1 tagged_division_of ({a..b} \<inter> {x. x\<bullet>k \<le> c}) \<and> d fine p1 \<and>
+        p2 tagged_division_of ({a..b} \<inter> {x. x\<bullet>k \<ge> c}) \<and> d fine p2 \<longrightarrow>
+        norm ((setsum (\<lambda>(x,k). content k *\<^sub>R f x) p1 + setsum (\<lambda>(x,k). content k *\<^sub>R f x) p2) - i) < e"
+proof -
+  guess d using has_integralD[OF assms(1-2)] . note d=this
+  show ?thesis
+    apply (rule that[of d])
+    apply (rule d)
+    apply rule
+    apply rule
+    apply rule
+    apply (elim conjE)
+  proof -
+    fix p1 p2
+    assume "p1 tagged_division_of {a..b} \<inter> {x. x \<bullet> k \<le> c}" "d fine p1"
+    note p1=tagged_division_ofD[OF this(1)] this
+    assume "p2 tagged_division_of {a..b} \<inter> {x. c \<le> x \<bullet> k}" "d fine p2"
+    note p2=tagged_division_ofD[OF this(1)] this
     note tagged_division_union_interval[OF p1(7) p2(7)] note p12 = tagged_division_ofD[OF this] this
-    have "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - i) = norm ((\<Sum>(x, k)\<in>p1 \<union> p2. content k *\<^sub>R f x) - i)"
-      apply(subst setsum_Un_zero) apply(rule p1 p2)+ apply(rule) unfolding split_paired_all split_conv
-    proof- fix a b assume ab:"(a,b) \<in> p1 \<inter> p2"
-      have "(a,b) \<in> p1" using ab by auto from p1(4)[OF this] guess u v apply-by(erule exE)+ note uv =this
-      have "b \<subseteq> {x. x\<bullet>k = c}" using ab p1(3)[of a b] p2(3)[of a b] by fastforce
-      moreover have "interior {x::'a. x \<bullet> k = c} = {}"
-      proof(rule ccontr) case goal1 then obtain x where x:"x\<in>interior {x::'a. x\<bullet>k = c}" by auto
+    have "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - i) =
+      norm ((\<Sum>(x, k)\<in>p1 \<union> p2. content k *\<^sub>R f x) - i)"
+      apply (subst setsum_Un_zero)
+      apply (rule p1 p2)+
+      apply rule
+      unfolding split_paired_all split_conv
+    proof -
+      fix a b
+      assume ab: "(a, b) \<in> p1 \<inter> p2"
+      have "(a, b) \<in> p1"
+        using ab by auto
+      from p1(4)[OF this] guess u v by (elim exE) note uv = this
+      have "b \<subseteq> {x. x\<bullet>k = c}"
+        using ab p1(3)[of a b] p2(3)[of a b] by fastforce
+      moreover
+      have "interior {x::'a. x \<bullet> k = c} = {}"
+      proof (rule ccontr)
+        assume "\<not> ?thesis"
+        then obtain x where x: "x \<in> interior {x::'a. x\<bullet>k = c}"
+          by auto
         then guess e unfolding mem_interior .. note e=this
-        have x:"x\<bullet>k = c" using x interior_subset by fastforce
-        have *:"\<And>i. i\<in>Basis \<Longrightarrow> \<bar>(x - (x + (e / 2) *\<^sub>R k)) \<bullet> i\<bar>
-          = (if i = k then e/2 else 0)" using e k by (auto simp: inner_simps inner_not_same_Basis)
+        have x: "x\<bullet>k = c"
+          using x interior_subset by fastforce
+        have *: "\<And>i. i \<in> Basis \<Longrightarrow> \<bar>(x - (x + (e / 2) *\<^sub>R k)) \<bullet> i\<bar> = (if i = k then e/2 else 0)"
+          using e k by (auto simp: inner_simps inner_not_same_Basis)
         have "(\<Sum>i\<in>Basis. \<bar>(x - (x + (e / 2 ) *\<^sub>R k)) \<bullet> i\<bar>) =
-          (\<Sum>i\<in>Basis. (if i = k then e / 2 else 0))" apply(rule setsum_cong2) apply(subst *) by auto
-        also have "... < e" apply(subst setsum_delta) using e by auto
+          (\<Sum>i\<in>Basis. (if i = k then e / 2 else 0))"
+          apply (rule setsum_cong2)
+          apply (subst *)
+          apply auto
+          done
+        also have "\<dots> < e"
+          apply (subst setsum_delta)
+          using e
+          apply auto
+          done
         finally have "x + (e/2) *\<^sub>R k \<in> ball x e"
           unfolding mem_ball dist_norm by(rule le_less_trans[OF norm_le_l1])
-        hence "x + (e/2) *\<^sub>R k \<in> {x. x\<bullet>k = c}" using e by auto
-        thus False unfolding mem_Collect_eq using e x k by (auto simp: inner_simps)
-      qed ultimately have "content b = 0" unfolding uv content_eq_0_interior apply-apply(drule interior_mono) by auto
-      thus "content b *\<^sub>R f a = 0" by auto
+        then have "x + (e/2) *\<^sub>R k \<in> {x. x\<bullet>k = c}"
+          using e by auto
+        then show False
+          unfolding mem_Collect_eq using e x k by (auto simp: inner_simps)
+      qed
+      ultimately have "content b = 0"
+        unfolding uv content_eq_0_interior
+        apply -
+        apply (drule interior_mono)
+        apply auto
+        done
+      then show "content b *\<^sub>R f a = 0"
+        by auto
     qed auto
-    also have "\<dots> < e" by(rule k d(2) p12 fine_union p1 p2)+
-    finally show "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - i) < e" . qed qed
+    also have "\<dots> < e"
+      by (rule k d(2) p12 fine_union p1 p2)+
+    finally show "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - i) < e" .
+  qed
+qed
 
 lemma integrable_split[intro]:
-  fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::{real_normed_vector,complete_space}"
-  assumes "f integrable_on {a..b}" and k:"k\<in>Basis"
-  shows "f integrable_on ({a..b} \<inter> {x. x\<bullet>k \<le> c})" (is ?t1) and "f integrable_on ({a..b} \<inter> {x. x\<bullet>k \<ge> c})" (is ?t2)
-proof- guess y using assms(1) unfolding integrable_on_def .. note y=this
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::{real_normed_vector,complete_space}"
+  assumes "f integrable_on {a..b}"
+    and k: "k \<in> Basis"
+  shows "f integrable_on ({a..b} \<inter> {x. x\<bullet>k \<le> c})" (is ?t1)
+    and "f integrable_on ({a..b} \<inter> {x. x\<bullet>k \<ge> c})" (is ?t2)
+proof -
+  guess y using assms(1) unfolding integrable_on_def .. note y=this
   def b' \<equiv> "\<Sum>i\<in>Basis. (if i = k then min (b\<bullet>k) c else b\<bullet>i)*\<^sub>R i::'a"
   def a' \<equiv> "\<Sum>i\<in>Basis. (if i = k then max (a\<bullet>k) c else a\<bullet>i)*\<^sub>R i::'a"
-  show ?t1 ?t2 unfolding interval_split[OF k] integrable_cauchy unfolding interval_split[symmetric,OF k]
-  proof(rule_tac[!] allI impI)+ fix e::real assume "e>0" hence "e/2>0" by auto
+  show ?t1 ?t2
+    unfolding interval_split[OF k] integrable_cauchy
+    unfolding interval_split[symmetric,OF k]
+  proof (rule_tac[!] allI impI)+
+    fix e :: real
+    assume "e > 0"
+    then have "e/2>0"
+      by auto
     from has_integral_separate_sides[OF y this k,of c] guess d . note d=this[rule_format]
-    let ?P = "\<lambda>A. \<exists>d. gauge d \<and> (\<forall>p1 p2. p1 tagged_division_of {a..b} \<inter> A \<and> d fine p1
-      \<and> p2 tagged_division_of {a..b} \<inter> A \<and> d fine p2 \<longrightarrow>
+    let ?P = "\<lambda>A. \<exists>d. gauge d \<and> (\<forall>p1 p2. p1 tagged_division_of {a..b} \<inter> A \<and> d fine p1 \<and>
+      p2 tagged_division_of {a..b} \<inter> A \<and> d fine p2 \<longrightarrow>
       norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)) < e)"
-    show "?P {x. x \<bullet> k \<le> c}" apply(rule_tac x=d in exI) apply(rule,rule d) apply(rule,rule,rule)
-    proof- fix p1 p2 assume as:"p1 tagged_division_of {a..b} \<inter> {x. x \<bullet> k \<le> c} \<and> d fine p1
-        \<and> p2 tagged_division_of {a..b} \<inter> {x. x \<bullet> k \<le> c} \<and> d fine p2"
+    show "?P {x. x \<bullet> k \<le> c}"
+      apply (rule_tac x=d in exI)
+      apply rule
+      apply (rule d)
+      apply rule
+      apply rule
+      apply rule
+    proof -
+      fix p1 p2
+      assume as: "p1 tagged_division_of {a..b} \<inter> {x. x \<bullet> k \<le> c} \<and> d fine p1 \<and>
+        p2 tagged_division_of {a..b} \<inter> {x. x \<bullet> k \<le> c} \<and> d fine p2"
       show "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)) < e"
-      proof- guess p using fine_division_exists[OF d(1), of a' b] . note p=this
-        show ?thesis using norm_triangle_half_l[OF d(2)[of p1 p] d(2)[of p2 p]]
+      proof -
+        guess p using fine_division_exists[OF d(1), of a' b] . note p=this
+        show ?thesis
+          using norm_triangle_half_l[OF d(2)[of p1 p] d(2)[of p2 p]]
           using as unfolding interval_split[OF k] b'_def[symmetric] a'_def[symmetric]
-          using p using assms by(auto simp add:algebra_simps)
-      qed qed
-    show "?P {x. x \<bullet> k \<ge> c}" apply(rule_tac x=d in exI) apply(rule,rule d) apply(rule,rule,rule)
-    proof- fix p1 p2 assume as:"p1 tagged_division_of {a..b} \<inter> {x. x \<bullet> k \<ge> c} \<and> d fine p1
-        \<and> p2 tagged_division_of {a..b} \<inter> {x. x \<bullet> k \<ge> c} \<and> d fine p2"
+          using p using assms
+          by (auto simp add: algebra_simps)
+      qed
+    qed
+    show "?P {x. x \<bullet> k \<ge> c}"
+      apply (rule_tac x=d in exI)
+      apply rule
+      apply (rule d)
+      apply rule
+      apply rule
+      apply rule
+    proof -
+      fix p1 p2
+      assume as: "p1 tagged_division_of {a..b} \<inter> {x. x \<bullet> k \<ge> c} \<and> d fine p1 \<and>
+        p2 tagged_division_of {a..b} \<inter> {x. x \<bullet> k \<ge> c} \<and> d fine p2"
       show "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)) < e"
-      proof- guess p using fine_division_exists[OF d(1), of a b'] . note p=this
-        show ?thesis using norm_triangle_half_l[OF d(2)[of p p1] d(2)[of p p2]]
-          using as unfolding interval_split[OF k] b'_def[symmetric] a'_def[symmetric]
-          using p using assms by(auto simp add:algebra_simps) qed qed qed qed
+      proof -
+        guess p using fine_division_exists[OF d(1), of a b'] . note p=this
+        show ?thesis
+          using norm_triangle_half_l[OF d(2)[of p p1] d(2)[of p p2]]
+          using as
+          unfolding interval_split[OF k] b'_def[symmetric] a'_def[symmetric]
+          using p
+          using assms
+          by (auto simp add:algebra_simps)
+      qed
+    qed
+  qed
+qed
+
 
 subsection {* Generalized notion of additivity. *}
 
 definition "neutral opp = (SOME x. \<forall>y. opp x y = y \<and> opp y x = y)"
 
-definition operative :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (('b::ordered_euclidean_space) set \<Rightarrow> 'a) \<Rightarrow> bool" where
-  "operative opp f \<equiv>
-    (\<forall>a b. content {a..b} = 0 \<longrightarrow> f {a..b} = neutral(opp)) \<and>
-    (\<forall>a b c. \<forall>k\<in>Basis. f({a..b}) =
-                   opp (f({a..b} \<inter> {x. x\<bullet>k \<le> c}))
-                       (f({a..b} \<inter> {x. x\<bullet>k \<ge> c})))"
-
-lemma operativeD[dest]: fixes type::"'a::ordered_euclidean_space"  assumes "operative opp f"
-  shows "\<And>a b. content {a..b} = 0 \<Longrightarrow> f {a..b::'a} = neutral(opp)"
-  "\<And>a b c k. k\<in>Basis \<Longrightarrow> f({a..b}) = opp (f({a..b} \<inter> {x. x\<bullet>k \<le> c})) (f({a..b} \<inter> {x. x\<bullet>k \<ge> c}))"
+definition operative :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (('b::ordered_euclidean_space) set \<Rightarrow> 'a) \<Rightarrow> bool"
+  where "operative opp f \<longleftrightarrow>
+    (\<forall>a b. content {a..b} = 0 \<longrightarrow> f {a..b} = neutral opp) \<and>
+    (\<forall>a b c. \<forall>k\<in>Basis. f {a..b} = opp (f({a..b} \<inter> {x. x\<bullet>k \<le> c})) (f ({a..b} \<inter> {x. x\<bullet>k \<ge> c})))"
+
+lemma operativeD[dest]:
+  fixes type :: "'a::ordered_euclidean_space"
+  assumes "operative opp f"
+  shows "\<And>a b::'a. content {a..b} = 0 \<Longrightarrow> f {a..b} = neutral opp"
+    and "\<And>a b c k. k \<in> Basis \<Longrightarrow> f {a..b} =
+      opp (f ({a..b} \<inter> {x. x\<bullet>k \<le> c})) (f ({a..b} \<inter> {x. x\<bullet>k \<ge> c}))"
   using assms unfolding operative_def by auto
 
-lemma operative_trivial:
- "operative opp f \<Longrightarrow> content({a..b}) = 0 \<Longrightarrow> f({a..b}) = neutral opp"
+lemma operative_trivial: "operative opp f \<Longrightarrow> content({a..b}) = 0 \<Longrightarrow> f({a..b}) = neutral opp"
   unfolding operative_def by auto
 
-lemma property_empty_interval:
- "(\<forall>a b. content({a..b}) = 0 \<longrightarrow> P({a..b})) \<Longrightarrow> P {}"
+lemma property_empty_interval: "\<forall>a b. content {a..b} = 0 \<longrightarrow> P {a..b} \<Longrightarrow> P {}"
   using content_empty unfolding empty_as_interval by auto
 
 lemma operative_empty: "operative opp f \<Longrightarrow> f {} = neutral opp"
-  unfolding operative_def apply(rule property_empty_interval) by auto
+  unfolding operative_def by (rule property_empty_interval) auto
+
 
 subsection {* Using additivity of lifted function to encode definedness. *}
 
-lemma forall_option: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P(Some x))"
-  by (metis option.nchotomy)
-
-lemma exists_option: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P(Some x))"
+lemma forall_option: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P (Some x))"
   by (metis option.nchotomy)
 
-fun lifted
-where
-  "lifted (opp::'a\<Rightarrow>'a\<Rightarrow>'b) (Some x) (Some y) = Some (opp x y)"
+lemma exists_option: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))"
+  by (metis option.nchotomy)
+
+fun lifted where
+  "lifted (opp :: 'a \<Rightarrow> 'a \<Rightarrow> 'b) (Some x) (Some y) = Some (opp x y)"
 | "lifted opp None _ = (None::'b option)"
 | "lifted opp _ None = None"
 
 lemma lifted_simp_1[simp]: "lifted opp v None = None"
   by (induct v) auto
 
-definition "monoidal opp \<equiv>  (\<forall>x y. opp x y = opp y x) \<and>
-                   (\<forall>x y z. opp x (opp y z) = opp (opp x y) z) \<and>
-                   (\<forall>x. opp (neutral opp) x = x)"
+definition "monoidal opp \<longleftrightarrow>
+  (\<forall>x y. opp x y = opp y x) \<and>
+  (\<forall>x y z. opp x (opp y z) = opp (opp x y) z) \<and>
+  (\<forall>x. opp (neutral opp) x = x)"
 
 lemma monoidalI:
   assumes "\<And>x y. opp x y = opp y x"
-  "\<And>x y z. opp x (opp y z) = opp (opp x y) z"
-  "\<And>x. opp (neutral opp) x = x" shows "monoidal opp"
+    and "\<And>x y z. opp x (opp y z) = opp (opp x y) z"
+    and "\<And>x. opp (neutral opp) x = x"
+  shows "monoidal opp"
   unfolding monoidal_def using assms by fastforce
 
 lemma monoidal_ac:
   assumes "monoidal opp"
-  shows "opp (neutral opp) a = a" "opp a (neutral opp) = a" "opp a b = opp b a"
-  "opp (opp a b) c = opp a (opp b c)"  "opp a (opp b c) = opp b (opp a c)"
+  shows "opp (neutral opp) a = a"
+    and "opp a (neutral opp) = a"
+    and "opp a b = opp b a"
+    and "opp (opp a b) c = opp a (opp b c)"
+    and "opp a (opp b c) = opp b (opp a c)"
   using assms unfolding monoidal_def by metis+
 
-lemma monoidal_simps[simp]: assumes "monoidal opp"
-  shows "opp (neutral opp) a = a" "opp a (neutral opp) = a"
+lemma monoidal_simps[simp]:
+  assumes "monoidal opp"
+  shows "opp (neutral opp) a = a"
+    and "opp a (neutral opp) = a"
   using monoidal_ac[OF assms] by auto
 
-lemma neutral_lifted[cong]: assumes "monoidal opp"
-  shows "neutral (lifted opp) = Some(neutral opp)"
-  apply(subst neutral_def) apply(rule some_equality) apply(rule,induct_tac y) prefer 3
+lemma neutral_lifted[cong]:
+  assumes "monoidal opp"
+  shows "neutral (lifted opp) = Some (neutral opp)"
+  apply (subst neutral_def)
+  apply (rule some_equality)
+  apply rule
+  apply (induct_tac y)
+  prefer 3
 proof -
-  fix x assume "\<forall>y. lifted opp x y = y \<and> lifted opp y x = y"
-  thus "x = Some (neutral opp)"
-    apply(induct x) defer
-    apply rule apply(subst neutral_def) apply(subst eq_commute,rule some_equality)
-    apply(rule,erule_tac x="Some y" in allE) defer apply(erule_tac x="Some x" in allE)
+  fix x
+  assume "\<forall>y. lifted opp x y = y \<and> lifted opp y x = y"
+  then show "x = Some (neutral opp)"
+    apply (induct x)
+    defer
+    apply rule
+    apply (subst neutral_def)
+    apply (subst eq_commute)
+    apply(rule some_equality)
+    apply rule
+    apply (erule_tac x="Some y" in allE)
+    defer
+    apply (erule_tac x="Some x" in allE)
     apply auto
     done
-qed(auto simp add:monoidal_ac[OF assms])
-
-lemma monoidal_lifted[intro]: assumes "monoidal opp" shows "monoidal(lifted opp)"
-  unfolding monoidal_def forall_option neutral_lifted[OF assms] using monoidal_ac[OF assms] by auto
+qed (auto simp add:monoidal_ac[OF assms])
+
+lemma monoidal_lifted[intro]:
+  assumes "monoidal opp"
+  shows "monoidal (lifted opp)"
+  unfolding monoidal_def forall_option neutral_lifted[OF assms]
+  using monoidal_ac[OF assms]
+  by auto
 
 definition "support opp f s = {x. x\<in>s \<and> f x \<noteq> neutral opp}"
-definition "fold' opp e s \<equiv> (if finite s then Finite_Set.fold opp e s else e)"
-definition "iterate opp s f \<equiv> fold' (\<lambda>x a. opp (f x) a) (neutral opp) (support opp f s)"
-
-lemma support_subset[intro]:"support opp f s \<subseteq> s" unfolding support_def by auto
-lemma support_empty[simp]:"support opp f {} = {}" using support_subset[of opp f "{}"] by auto
-
-lemma comp_fun_commute_monoidal[intro]: assumes "monoidal opp" shows "comp_fun_commute opp"
-  unfolding comp_fun_commute_def using monoidal_ac[OF assms] by auto
+definition "fold' opp e s = (if finite s then Finite_Set.fold opp e s else e)"
+definition "iterate opp s f = fold' (\<lambda>x a. opp (f x) a) (neutral opp) (support opp f s)"
+
+lemma support_subset[intro]: "support opp f s \<subseteq> s"
+  unfolding support_def by auto
+
+lemma support_empty[simp]: "support opp f {} = {}"
+  using support_subset[of opp f "{}"] by auto
+
+lemma comp_fun_commute_monoidal[intro]:
+  assumes "monoidal opp"
+  shows "comp_fun_commute opp"
+  unfolding comp_fun_commute_def
+  using monoidal_ac[OF assms]
+  by auto
 
 lemma support_clauses:
   "\<And>f g s. support opp f {} = {}"
@@ -3902,98 +4039,190 @@
   "\<And>f g s. support opp f (s \<inter> t) = (support opp f s) \<inter> (support opp f t)"
   "\<And>f g s. support opp f (s - t) = (support opp f s) - (support opp f t)"
   "\<And>f g s. support opp g (f ` s) = f ` (support opp (g o f) s)"
-unfolding support_def by auto
-
-lemma finite_support[intro]:"finite s \<Longrightarrow> finite (support opp f s)"
   unfolding support_def by auto
 
-lemma iterate_empty[simp]:"iterate opp {} f = neutral opp"
+lemma finite_support[intro]: "finite s \<Longrightarrow> finite (support opp f s)"
+  unfolding support_def by auto
+
+lemma iterate_empty[simp]: "iterate opp {} f = neutral opp"
   unfolding iterate_def fold'_def by auto
 
-lemma iterate_insert[simp]: assumes "monoidal opp" "finite s"
-  shows "iterate opp (insert x s) f = (if x \<in> s then iterate opp s f else opp (f x) (iterate opp s f))"
-proof(cases "x\<in>s") case True hence *:"insert x s = s" by auto
+lemma iterate_insert[simp]:
+  assumes "monoidal opp"
+    and "finite s"
+  shows "iterate opp (insert x s) f =
+    (if x \<in> s then iterate opp s f else opp (f x) (iterate opp s f))"
+proof (cases "x \<in> s")
+  case True
+  then have *: "insert x s = s"
+    by auto
   show ?thesis unfolding iterate_def if_P[OF True] * by auto
-next case False note x=this
+next
+  case False
+  note x = this
   note * = comp_fun_commute.comp_comp_fun_commute [OF comp_fun_commute_monoidal[OF assms(1)]]
-  show ?thesis proof(cases "f x = neutral opp")
-    case True show ?thesis unfolding iterate_def if_not_P[OF x] support_clauses if_P[OF True]
-      unfolding True monoidal_simps[OF assms(1)] by auto
-  next case False show ?thesis unfolding iterate_def fold'_def  if_not_P[OF x] support_clauses if_not_P[OF False]
-      apply(subst comp_fun_commute.fold_insert[OF * finite_support, simplified comp_def])
-      using `finite s` unfolding support_def using False x by auto qed qed
+  show ?thesis
+  proof (cases "f x = neutral opp")
+    case True
+    show ?thesis
+      unfolding iterate_def if_not_P[OF x] support_clauses if_P[OF True]
+      unfolding True monoidal_simps[OF assms(1)]
+      by auto
+  next
+    case False
+    show ?thesis
+      unfolding iterate_def fold'_def  if_not_P[OF x] support_clauses if_not_P[OF False]
+      apply (subst comp_fun_commute.fold_insert[OF * finite_support, simplified comp_def])
+      using `finite s`
+      unfolding support_def
+      using False x
+      apply auto
+      done
+  qed
+qed
 
 lemma iterate_some:
-  assumes "monoidal opp"  "finite s"
-  shows "iterate (lifted opp) s (\<lambda>x. Some(f x)) = Some (iterate opp s f)" using assms(2)
-proof(induct s) case empty thus ?case using assms by auto
-next case (insert x F) show ?case apply(subst iterate_insert) prefer 3 apply(subst if_not_P)
-    defer unfolding insert(3) lifted.simps apply rule using assms insert by auto qed
+  assumes "monoidal opp"
+    and "finite s"
+  shows "iterate (lifted opp) s (\<lambda>x. Some(f x)) = Some (iterate opp s f)"
+  using assms(2)
+proof (induct s)
+  case empty
+  then show ?case
+    using assms by auto
+next
+  case (insert x F)
+  show ?case
+    apply (subst iterate_insert)
+    prefer 3
+    apply (subst if_not_P)
+    defer
+    unfolding insert(3) lifted.simps
+    apply rule
+    using assms insert
+    apply auto
+    done
+qed
+
+
 subsection {* Two key instances of additivity. *}
 
-lemma neutral_add[simp]:
-  "neutral op + = (0::_::comm_monoid_add)" unfolding neutral_def
-  apply(rule some_equality) defer apply(erule_tac x=0 in allE) by auto
+lemma neutral_add[simp]: "neutral op + = (0::'a::comm_monoid_add)"
+  unfolding neutral_def
+  apply (rule some_equality)
+  defer
+  apply (erule_tac x=0 in allE)
+  apply auto
+  done
 
 lemma operative_content[intro]: "operative (op +) content"
-  unfolding operative_def neutral_add apply safe
-  unfolding content_split[symmetric] ..
+  unfolding operative_def neutral_add
+  apply safe
+  unfolding content_split[symmetric]
+  apply rule
+  done
 
 lemma neutral_monoid: "neutral ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a) = 0"
   by (rule neutral_add) (* FIXME: duplicate *)
 
-lemma monoidal_monoid[intro]:
-  shows "monoidal ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a)"
-  unfolding monoidal_def neutral_monoid by(auto simp add: algebra_simps)
-
-lemma operative_integral: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::banach"
+lemma monoidal_monoid[intro]: "monoidal ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a)"
+  unfolding monoidal_def neutral_monoid
+  by (auto simp add: algebra_simps)
+
+lemma operative_integral:
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::banach"
   shows "operative (lifted(op +)) (\<lambda>i. if f integrable_on i then Some(integral i f) else None)"
-  unfolding operative_def unfolding neutral_lifted[OF monoidal_monoid] neutral_add
-  apply(rule,rule,rule,rule) defer apply(rule allI ballI)+
-proof-
-  fix a b c and k :: 'a assume k:"k\<in>Basis"
+  unfolding operative_def
+  unfolding neutral_lifted[OF monoidal_monoid] neutral_add
+  apply rule
+  apply rule
+  apply rule
+  apply rule
+  defer
+  apply (rule allI ballI)+
+proof -
+  fix a b c
+  fix k :: 'a
+  assume k: "k \<in> Basis"
   show "(if f integrable_on {a..b} then Some (integral {a..b} f) else None) =
     lifted op + (if f integrable_on {a..b} \<inter> {x. x \<bullet> k \<le> c} then Some (integral ({a..b} \<inter> {x. x \<bullet> k \<le> c}) f) else None)
     (if f integrable_on {a..b} \<inter> {x. c \<le> x \<bullet> k} then Some (integral ({a..b} \<inter> {x. c \<le> x \<bullet> k}) f) else None)"
-  proof(cases "f integrable_on {a..b}")
-    case True show ?thesis unfolding if_P[OF True] using k apply-
-      unfolding if_P[OF integrable_split(1)[OF True]] unfolding if_P[OF integrable_split(2)[OF True]]
-      unfolding lifted.simps option.inject apply(rule integral_unique) apply(rule has_integral_split[OF _ _ k])
-      apply(rule_tac[!] integrable_integral integrable_split)+ using True k by auto
-  next case False have "(\<not> (f integrable_on {a..b} \<inter> {x. x \<bullet> k \<le> c})) \<or> (\<not> ( f integrable_on {a..b} \<inter> {x. c \<le> x \<bullet> k}))"
-    proof(rule ccontr) case goal1 hence "f integrable_on {a..b}" apply- unfolding integrable_on_def
-        apply(rule_tac x="integral ({a..b} \<inter> {x. x \<bullet> k \<le> c}) f + integral ({a..b} \<inter> {x. x \<bullet> k \<ge> c}) f" in exI)
-        apply(rule has_integral_split[OF _ _ k]) apply(rule_tac[!] integrable_integral) by auto
-      thus False using False by auto
-    qed thus ?thesis using False by auto
-  qed next
-  fix a b assume as:"content {a..b::'a} = 0"
-  thus "(if f integrable_on {a..b} then Some (integral {a..b} f) else None) = Some 0"
-    unfolding if_P[OF integrable_on_null[OF as]] using has_integral_null_eq[OF as] by auto qed
+  proof (cases "f integrable_on {a..b}")
+    case True
+    show ?thesis
+      unfolding if_P[OF True]
+      using k
+      apply -
+      unfolding if_P[OF integrable_split(1)[OF True]]
+      unfolding if_P[OF integrable_split(2)[OF True]]
+      unfolding lifted.simps option.inject
+      apply (rule integral_unique)
+      apply (rule has_integral_split[OF _ _ k])
+      apply (rule_tac[!] integrable_integral integrable_split)+
+      using True k
+      apply auto
+      done
+  next
+    case False
+    have "\<not> (f integrable_on {a..b} \<inter> {x. x \<bullet> k \<le> c}) \<or> \<not> ( f integrable_on {a..b} \<inter> {x. c \<le> x \<bullet> k})"
+    proof (rule ccontr)
+      assume "\<not> ?thesis"
+      then have "f integrable_on {a..b}"
+        apply -
+        unfolding integrable_on_def
+        apply (rule_tac x="integral ({a..b} \<inter> {x. x \<bullet> k \<le> c}) f + integral ({a..b} \<inter> {x. x \<bullet> k \<ge> c}) f" in exI)
+        apply (rule has_integral_split[OF _ _ k])
+        apply (rule_tac[!] integrable_integral)
+        apply auto
+        done
+      then show False
+        using False by auto
+    qed
+    then show ?thesis
+      using False by auto
+  qed
+next
+  fix a b :: 'a
+  assume as: "content {a..b} = 0"
+  then show "(if f integrable_on {a..b} then Some (integral {a..b} f) else None) = Some 0"
+    unfolding if_P[OF integrable_on_null[OF as]]
+    using has_integral_null_eq[OF as]
+    by auto
+qed
+
 
 subsection {* Points of division of a partition. *}
 
 definition "division_points (k::('a::ordered_euclidean_space) set) d =
-    {(j,x). j\<in>Basis \<and> (interval_lowerbound k)\<bullet>j < x \<and> x < (interval_upperbound k)\<bullet>j \<and>
-           (\<exists>i\<in>d. (interval_lowerbound i)\<bullet>j = x \<or> (interval_upperbound i)\<bullet>j = x)}"
-
-lemma division_points_finite: fixes i::"('a::ordered_euclidean_space) set"
-  assumes "d division_of i" shows "finite (division_points i d)"
-proof- note assm = division_ofD[OF assms]
+  {(j,x). j \<in> Basis \<and> (interval_lowerbound k)\<bullet>j < x \<and> x < (interval_upperbound k)\<bullet>j \<and>
+    (\<exists>i\<in>d. (interval_lowerbound i)\<bullet>j = x \<or> (interval_upperbound i)\<bullet>j = x)}"
+
+lemma division_points_finite:
+  fixes i :: "'a::ordered_euclidean_space set"
+  assumes "d division_of i"
+  shows "finite (division_points i d)"
+proof -
+  note assm = division_ofD[OF assms]
   let ?M = "\<lambda>j. {(j,x)|x. (interval_lowerbound i)\<bullet>j < x \<and> x < (interval_upperbound i)\<bullet>j \<and>
-           (\<exists>i\<in>d. (interval_lowerbound i)\<bullet>j = x \<or> (interval_upperbound i)\<bullet>j = x)}"
-  have *:"division_points i d = \<Union>(?M ` Basis)"
+    (\<exists>i\<in>d. (interval_lowerbound i)\<bullet>j = x \<or> (interval_upperbound i)\<bullet>j = x)}"
+  have *: "division_points i d = \<Union>(?M ` Basis)"
     unfolding division_points_def by auto
-  show ?thesis unfolding * using assm by auto qed
-
-lemma division_points_subset: fixes a::"'a::ordered_euclidean_space"
-  assumes "d division_of {a..b}" "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"  "a\<bullet>k < c" "c < b\<bullet>k" and k:"k\<in>Basis"
-  shows "division_points ({a..b} \<inter> {x. x\<bullet>k \<le> c}) {l \<inter> {x. x\<bullet>k \<le> c} | l . l \<in> d \<and> ~(l \<inter> {x. x\<bullet>k \<le> c} = {})}
-                  \<subseteq> division_points ({a..b}) d" (is ?t1) and
-        "division_points ({a..b} \<inter> {x. x\<bullet>k \<ge> c}) {l \<inter> {x. x\<bullet>k \<ge> c} | l . l \<in> d \<and> ~(l \<inter> {x. x\<bullet>k \<ge> c} = {})}
-                  \<subseteq> division_points ({a..b}) d" (is ?t2)
-proof- note assm = division_ofD[OF assms(1)]
-  have *:"\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
+  show ?thesis
+    unfolding * using assm by auto
+qed
+
+lemma division_points_subset:
+  fixes a :: "'a::ordered_euclidean_space"
+  assumes "d division_of {a..b}"
+    and "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"  "a\<bullet>k < c" "c < b\<bullet>k"
+    and k: "k \<in> Basis"
+  shows "division_points ({a..b} \<inter> {x. x\<bullet>k \<le> c}) {l \<inter> {x. x\<bullet>k \<le> c} | l . l \<in> d \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}} \<subseteq>
+      division_points ({a..b}) d" (is ?t1)
+    and "division_points ({a..b} \<inter> {x. x\<bullet>k \<ge> c}) {l \<inter> {x. x\<bullet>k \<ge> c} | l . l \<in> d \<and> ~(l \<inter> {x. x\<bullet>k \<ge> c} = {})} \<subseteq>
+      division_points ({a..b}) d" (is ?t2)
+proof -
+  note assm = division_ofD[OF assms(1)]
+  have *: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
     "\<forall>i\<in>Basis. a\<bullet>i \<le> (\<Sum>i\<in>Basis. (if i = k then min (b \<bullet> k) c else b \<bullet> i) *\<^sub>R i) \<bullet> i"
     "\<forall>i\<in>Basis. (\<Sum>i\<in>Basis. (if i = k then max (a \<bullet> k) c else a \<bullet> i) *\<^sub>R i) \<bullet> i \<le> b\<bullet>i"
     "min (b \<bullet> k) c = c" "max (a \<bullet> k) c = c"
@@ -4003,83 +4232,148 @@
     unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)]
     unfolding *
     unfolding subset_eq
-    apply(rule)
+    apply rule
     unfolding mem_Collect_eq split_beta
-    apply(erule bexE conjE)+
-    apply(simp only: mem_Collect_eq inner_setsum_left_Basis simp_thms)
-    apply(erule exE conjE)+
+    apply (erule bexE conjE)+
+    apply (simp only: mem_Collect_eq inner_setsum_left_Basis simp_thms)
+    apply (erule exE conjE)+
   proof
-    fix i l x assume as:"a \<bullet> fst x < snd x" "snd x < (if fst x = k then c else b \<bullet> fst x)"
+    fix i l x
+    assume as:
+      "a \<bullet> fst x < snd x" "snd x < (if fst x = k then c else b \<bullet> fst x)"
       "interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x"
-      "i = l \<inter> {x. x \<bullet> k \<le> c}" "l \<in> d" "l \<inter> {x. x \<bullet> k \<le> c} \<noteq> {}" and fstx:"fst x \<in>Basis"
+      "i = l \<inter> {x. x \<bullet> k \<le> c}" "l \<in> d" "l \<inter> {x. x \<bullet> k \<le> c} \<noteq> {}"
+      and fstx: "fst x \<in> Basis"
     from assm(4)[OF this(5)] guess u v apply-by(erule exE)+ note l=this
-    have *:"\<forall>i\<in>Basis. u \<bullet> i \<le> (\<Sum>i\<in>Basis. (if i = k then min (v \<bullet> k) c else v \<bullet> i) *\<^sub>R i) \<bullet> i"
+    have *: "\<forall>i\<in>Basis. u \<bullet> i \<le> (\<Sum>i\<in>Basis. (if i = k then min (v \<bullet> k) c else v \<bullet> i) *\<^sub>R i) \<bullet> i"
       using as(6) unfolding l interval_split[OF k] interval_ne_empty as .
-    have **:"\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i" using l using as(6) unfolding interval_ne_empty[symmetric] by auto
+    have **: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i"
+      using l using as(6) unfolding interval_ne_empty[symmetric] by auto
     show "\<exists>i\<in>d. interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x"
       apply (rule bexI[OF _ `l \<in> d`])
       using as(1-3,5) fstx
       unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] as
-      by (auto split: split_if_asm)
+      apply (auto split: split_if_asm)
+      done
     show "snd x < b \<bullet> fst x"
       using as(2) `c < b\<bullet>k` by (auto split: split_if_asm)
   qed
   show ?t2
     unfolding division_points_def interval_split[OF k, of a b]
-    unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)] unfolding *
-    unfolding subset_eq apply(rule) unfolding mem_Collect_eq split_beta
-    apply(erule bexE conjE)+
-    apply(simp only: mem_Collect_eq inner_setsum_left_Basis simp_thms)
-    apply(erule exE conjE)+
+    unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)]
+    unfolding *
+    unfolding subset_eq
+    apply rule
+    unfolding mem_Collect_eq split_beta
+    apply (erule bexE conjE)+
+    apply (simp only: mem_Collect_eq inner_setsum_left_Basis simp_thms)
+    apply (erule exE conjE)+
   proof
-    fix i l x assume as:"(if fst x = k then c else a \<bullet> fst x) < snd x" "snd x < b \<bullet> fst x"
+    fix i l x
+    assume as:
+      "(if fst x = k then c else a \<bullet> fst x) < snd x" "snd x < b \<bullet> fst x"
       "interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x"
-      "i = l \<inter> {x. c \<le> x \<bullet> k}" "l \<in> d" "l \<inter> {x. c \<le> x \<bullet> k} \<noteq> {}" and fstx:"fst x \<in> Basis"
-    from assm(4)[OF this(5)] guess u v apply-by(erule exE)+ note l=this
-    have *:"\<forall>i\<in>Basis. (\<Sum>i\<in>Basis. (if i = k then max (u \<bullet> k) c else u \<bullet> i) *\<^sub>R i) \<bullet> i \<le> v \<bullet> i"
+      "i = l \<inter> {x. c \<le> x \<bullet> k}" "l \<in> d" "l \<inter> {x. c \<le> x \<bullet> k} \<noteq> {}"
+      and fstx: "fst x \<in> Basis"
+    from assm(4)[OF this(5)] guess u v by (elim exE) note l=this
+    have *: "\<forall>i\<in>Basis. (\<Sum>i\<in>Basis. (if i = k then max (u \<bullet> k) c else u \<bullet> i) *\<^sub>R i) \<bullet> i \<le> v \<bullet> i"
       using as(6) unfolding l interval_split[OF k] interval_ne_empty as .
-    have **:"\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i" using l using as(6) unfolding interval_ne_empty[symmetric] by auto
+    have **: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i"
+      using l using as(6) unfolding interval_ne_empty[symmetric] by auto
     show "\<exists>i\<in>d. interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x"
       apply (rule bexI[OF _ `l \<in> d`])
       using as(1-3,5) fstx
       unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] as
-      by (auto split: split_if_asm)
+      apply (auto split: split_if_asm)
+      done
     show "a \<bullet> fst x < snd x"
       using as(1) `a\<bullet>k < c` by (auto split: split_if_asm)
    qed
 qed
 
-lemma division_points_psubset: fixes a::"'a::ordered_euclidean_space"
-  assumes "d division_of {a..b}"  "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"  "a\<bullet>k < c" "c < b\<bullet>k"
-  "l \<in> d" "interval_lowerbound l\<bullet>k = c \<or> interval_upperbound l\<bullet>k = c" and k:"k\<in>Basis"
-  shows "division_points ({a..b} \<inter> {x. x\<bullet>k \<le> c}) {l \<inter> {x. x\<bullet>k \<le> c} | l. l\<in>d \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}}
-              \<subset> division_points ({a..b}) d" (is "?D1 \<subset> ?D")
-        "division_points ({a..b} \<inter> {x. x\<bullet>k \<ge> c}) {l \<inter> {x. x\<bullet>k \<ge> c} | l. l\<in>d \<and> l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}}
-              \<subset> division_points ({a..b}) d" (is "?D2 \<subset> ?D")
-proof- have ab:"\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i" using assms(2) by(auto intro!:less_imp_le)
-  guess u v using division_ofD(4)[OF assms(1,5)] apply-by(erule exE)+ note l=this
-  have uv:"\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i" "\<forall>i\<in>Basis. a\<bullet>i \<le> u\<bullet>i \<and> v\<bullet>i \<le> b\<bullet>i"
+lemma division_points_psubset:
+  fixes a :: "'a::ordered_euclidean_space"
+  assumes "d division_of {a..b}"
+    and "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"  "a\<bullet>k < c" "c < b\<bullet>k"
+    and "l \<in> d"
+    and "interval_lowerbound l\<bullet>k = c \<or> interval_upperbound l\<bullet>k = c"
+    and k: "k \<in> Basis"
+  shows "division_points ({a..b} \<inter> {x. x\<bullet>k \<le> c}) {l \<inter> {x. x\<bullet>k \<le> c} | l. l\<in>d \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}} \<subset>
+      division_points ({a..b}) d" (is "?D1 \<subset> ?D")
+    and "division_points ({a..b} \<inter> {x. x\<bullet>k \<ge> c}) {l \<inter> {x. x\<bullet>k \<ge> c} | l. l\<in>d \<and> l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}} \<subset>
+      division_points ({a..b}) d" (is "?D2 \<subset> ?D")
+proof -
+  have ab: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
+    using assms(2) by (auto intro!:less_imp_le)
+  guess u v using division_ofD(4)[OF assms(1,5)] by (elim exE) note l=this
+  have uv: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i" "\<forall>i\<in>Basis. a\<bullet>i \<le> u\<bullet>i \<and> v\<bullet>i \<le> b\<bullet>i"
     using division_ofD(2,2,3)[OF assms(1,5)] unfolding l interval_ne_empty
-    unfolding subset_eq apply- defer apply(erule_tac x=u in ballE, erule_tac x=v in ballE) unfolding mem_interval by auto
-  have *:"interval_upperbound ({a..b} \<inter> {x. x \<bullet> k \<le> interval_upperbound l \<bullet> k}) \<bullet> k = interval_upperbound l \<bullet> k"
-         "interval_upperbound ({a..b} \<inter> {x. x \<bullet> k \<le> interval_lowerbound l \<bullet> k}) \<bullet> k = interval_lowerbound l \<bullet> k"
-    unfolding interval_split[OF k] apply(subst interval_bounds) prefer 3 apply(subst interval_bounds)
-    unfolding l interval_bounds[OF uv(1)] using uv[rule_format,of k] ab k by auto
-  have "\<exists>x. x \<in> ?D - ?D1" using assms(2-) apply-apply(erule disjE)
-    apply(rule_tac x="(k,(interval_lowerbound l)\<bullet>k)" in exI) defer
-    apply(rule_tac x="(k,(interval_upperbound l)\<bullet>k)" in exI)
-    unfolding division_points_def unfolding interval_bounds[OF ab] by(auto simp add:*)
-  thus "?D1 \<subset> ?D" apply-apply(rule,rule division_points_subset[OF assms(1-4)]) using k by auto
-
-  have *:"interval_lowerbound ({a..b} \<inter> {x. x \<bullet> k \<ge> interval_lowerbound l \<bullet> k}) \<bullet> k = interval_lowerbound l \<bullet> k"
-         "interval_lowerbound ({a..b} \<inter> {x. x \<bullet> k \<ge> interval_upperbound l \<bullet> k}) \<bullet> k = interval_upperbound l \<bullet> k"
-    unfolding interval_split[OF k] apply(subst interval_bounds) prefer 3 apply(subst interval_bounds)
-    unfolding l interval_bounds[OF uv(1)] using uv[rule_format,of k] ab k by auto
-  have "\<exists>x. x \<in> ?D - ?D2" using assms(2-) apply-apply(erule disjE)
-    apply(rule_tac x="(k,(interval_lowerbound l)\<bullet>k)" in exI) defer
-    apply(rule_tac x="(k,(interval_upperbound l)\<bullet>k)" in exI)
-    unfolding division_points_def unfolding interval_bounds[OF ab] by(auto simp add:*)
-  thus "?D2 \<subset> ?D" apply-apply(rule,rule division_points_subset[OF assms(1-4) k]) by auto qed
+    unfolding subset_eq
+    apply -
+    defer
+    apply (erule_tac x=u in ballE)
+    apply (erule_tac x=v in ballE)
+    unfolding mem_interval
+    apply auto
+    done
+  have *: "interval_upperbound ({a..b} \<inter> {x. x \<bullet> k \<le> interval_upperbound l \<bullet> k}) \<bullet> k = interval_upperbound l \<bullet> k"
+    "interval_upperbound ({a..b} \<inter> {x. x \<bullet> k \<le> interval_lowerbound l \<bullet> k}) \<bullet> k = interval_lowerbound l \<bullet> k"
+    unfolding interval_split[OF k]
+    apply (subst interval_bounds)
+    prefer 3
+    apply (subst interval_bounds)
+    unfolding l interval_bounds[OF uv(1)]
+    using uv[rule_format,of k] ab k
+    apply auto
+    done
+  have "\<exists>x. x \<in> ?D - ?D1"
+    using assms(2-)
+    apply -
+    apply (erule disjE)
+    apply (rule_tac x="(k,(interval_lowerbound l)\<bullet>k)" in exI)
+    defer
+    apply (rule_tac x="(k,(interval_upperbound l)\<bullet>k)" in exI)
+    unfolding division_points_def
+    unfolding interval_bounds[OF ab]
+    apply (auto simp add:*)
+    done
+  then show "?D1 \<subset> ?D"
+    apply -
+    apply rule
+    apply (rule division_points_subset[OF assms(1-4)])
+    using k
+    apply auto
+    done
+
+  have *: "interval_lowerbound ({a..b} \<inter> {x. x \<bullet> k \<ge> interval_lowerbound l \<bullet> k}) \<bullet> k = interval_lowerbound l \<bullet> k"
+    "interval_lowerbound ({a..b} \<inter> {x. x \<bullet> k \<ge> interval_upperbound l \<bullet> k}) \<bullet> k = interval_upperbound l \<bullet> k"
+    unfolding interval_split[OF k]
+    apply (subst interval_bounds)
+    prefer 3
+    apply (subst interval_bounds)
+    unfolding l interval_bounds[OF uv(1)]
+    using uv[rule_format,of k] ab k
+    apply auto
+    done
+  have "\<exists>x. x \<in> ?D - ?D2"
+    using assms(2-)
+    apply -
+    apply (erule disjE)
+    apply (rule_tac x="(k,(interval_lowerbound l)\<bullet>k)" in exI)
+    defer
+    apply (rule_tac x="(k,(interval_upperbound l)\<bullet>k)" in exI)
+    unfolding division_points_def
+    unfolding interval_bounds[OF ab]
+    apply (auto simp add:*)
+    done
+  then show "?D2 \<subset> ?D"
+    apply -
+    apply rule
+    apply (rule division_points_subset[OF assms(1-4) k])
+    apply auto
+    done
+qed
+
 
 subsection {* Preservation by divisions and tagged divisions. *}
 
@@ -4091,138 +4385,308 @@
 
 lemma iterate_expand_cases:
   "iterate opp s f = (if finite(support opp f s) then iterate opp (support opp f s) f else neutral opp)"
-  apply(cases) apply(subst if_P,assumption) unfolding iterate_def support_support fold'_def by auto
-
-lemma iterate_image: assumes "monoidal opp"  "inj_on f s"
+  apply cases
+  apply (subst if_P, assumption)
+  unfolding iterate_def support_support fold'_def
+  apply auto
+  done
+
+lemma iterate_image:
+  assumes "monoidal opp"
+    and "inj_on f s"
   shows "iterate opp (f ` s) g = iterate opp s (g \<circ> f)"
-proof- have *:"\<And>s. finite s \<Longrightarrow>  \<forall>x\<in>s. \<forall>y\<in>s. f x = f y \<longrightarrow> x = y \<Longrightarrow>
-     iterate opp (f ` s) g = iterate opp s (g \<circ> f)"
-  proof- case goal1 show ?case using goal1
-    proof(induct s) case empty thus ?case using assms(1) by auto
-    next case (insert x s) show ?case unfolding iterate_insert[OF assms(1) insert(1)]
-        unfolding if_not_P[OF insert(2)] apply(subst insert(3)[symmetric])
-        unfolding image_insert defer apply(subst iterate_insert[OF assms(1)])
-        apply(rule finite_imageI insert)+ apply(subst if_not_P)
-        unfolding image_iff o_def using insert(2,4) by auto
-    qed qed
+proof -
+  have *: "\<And>s. finite s \<Longrightarrow>  \<forall>x\<in>s. \<forall>y\<in>s. f x = f y \<longrightarrow> x = y \<Longrightarrow>
+    iterate opp (f ` s) g = iterate opp s (g \<circ> f)"
+  proof -
+    case goal1
+    then show ?case
+    proof (induct s)
+      case empty
+      then show ?case
+        using assms(1) by auto
+    next
+      case (insert x s)
+      show ?case
+        unfolding iterate_insert[OF assms(1) insert(1)]
+        unfolding if_not_P[OF insert(2)]
+        apply (subst insert(3)[symmetric])
+        unfolding image_insert
+        defer
+        apply (subst iterate_insert[OF assms(1)])
+        apply (rule finite_imageI insert)+
+        apply (subst if_not_P)
+        unfolding image_iff o_def
+        using insert(2,4)
+        apply auto
+        done
+    qed
+  qed
   show ?thesis
-    apply(cases "finite (support opp g (f ` s))")
-    apply(subst (1) iterate_support[symmetric],subst (2) iterate_support[symmetric])
-    unfolding support_clauses apply(rule *)apply(rule finite_imageD,assumption) unfolding inj_on_def[symmetric]
-    apply(rule subset_inj_on[OF assms(2) support_subset])+
-    apply(subst iterate_expand_cases) unfolding support_clauses apply(simp only: if_False)
-    apply(subst iterate_expand_cases) apply(subst if_not_P) by auto qed
-
-
-(* This lemma about iterations comes up in a few places.                     *)
+    apply (cases "finite (support opp g (f ` s))")
+    apply (subst (1) iterate_support[symmetric],subst (2) iterate_support[symmetric])
+    unfolding support_clauses
+    apply (rule *)
+    apply (rule finite_imageD,assumption)
+    unfolding inj_on_def[symmetric]
+    apply (rule subset_inj_on[OF assms(2) support_subset])+
+    apply (subst iterate_expand_cases)
+    unfolding support_clauses
+    apply (simp only: if_False)
+    apply (subst iterate_expand_cases)
+    apply (subst if_not_P)
+    apply auto
+    done
+qed
+
+
+(* This lemma about iterations comes up in a few places. *)
 lemma iterate_nonzero_image_lemma:
-  assumes "monoidal opp" "finite s" "g(a) = neutral opp"
-  "\<forall>x\<in>s. \<forall>y\<in>s. f x = f y \<and> x \<noteq> y \<longrightarrow> g(f x) = neutral opp"
+  assumes "monoidal opp"
+    and "finite s" "g(a) = neutral opp"
+    and "\<forall>x\<in>s. \<forall>y\<in>s. f x = f y \<and> x \<noteq> y \<longrightarrow> g(f x) = neutral opp"
   shows "iterate opp {f x | x. x \<in> s \<and> f x \<noteq> a} g = iterate opp s (g \<circ> f)"
-proof- have *:"{f x |x. x \<in> s \<and> ~(f x = a)} = f ` {x. x \<in> s \<and> ~(f x = a)}" by auto
-  have **:"support opp (g \<circ> f) {x \<in> s. f x \<noteq> a} = support opp (g \<circ> f) s"
+proof -
+  have *: "{f x |x. x \<in> s \<and> f x \<noteq> a} = f ` {x. x \<in> s \<and> f x \<noteq> a}"
+    by auto
+  have **: "support opp (g \<circ> f) {x \<in> s. f x \<noteq> a} = support opp (g \<circ> f) s"
     unfolding support_def using assms(3) by auto
-  show ?thesis unfolding *
-    apply(subst iterate_support[symmetric]) unfolding support_clauses
-    apply(subst iterate_image[OF assms(1)]) defer
-    apply(subst(2) iterate_support[symmetric]) apply(subst **)
-    unfolding inj_on_def using assms(3,4) unfolding support_def by auto qed
+  show ?thesis
+    unfolding *
+    apply (subst iterate_support[symmetric])
+    unfolding support_clauses
+    apply (subst iterate_image[OF assms(1)])
+    defer
+    apply (subst(2) iterate_support[symmetric])
+    apply (subst **)
+    unfolding inj_on_def
+    using assms(3,4)
+    unfolding support_def
+    apply auto
+    done
+qed
 
 lemma iterate_eq_neutral:
-  assumes "monoidal opp"  "\<forall>x \<in> s. (f(x) = neutral opp)"
-  shows "(iterate opp s f = neutral opp)"
-proof- have *:"support opp f s = {}" unfolding support_def using assms(2) by auto
-  show ?thesis apply(subst iterate_support[symmetric])
-    unfolding * using assms(1) by auto qed
-
-lemma iterate_op: assumes "monoidal opp" "finite s"
-  shows "iterate opp s (\<lambda>x. opp (f x) (g x)) = opp (iterate opp s f) (iterate opp s g)" using assms(2)
-proof(induct s) case empty thus ?case unfolding iterate_insert[OF assms(1)] using assms(1) by auto
-next case (insert x F) show ?case unfolding iterate_insert[OF assms(1) insert(1)] if_not_P[OF insert(2)] insert(3)
-    unfolding monoidal_ac[OF assms(1)] by(rule refl) qed
-
-lemma iterate_eq: assumes "monoidal opp" "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
+  assumes "monoidal opp"
+    and "\<forall>x \<in> s. f x = neutral opp"
+  shows "iterate opp s f = neutral opp"
+proof -
+  have *: "support opp f s = {}"
+    unfolding support_def using assms(2) by auto
+  show ?thesis
+    apply (subst iterate_support[symmetric])
+    unfolding *
+    using assms(1)
+    apply auto
+    done
+qed
+
+lemma iterate_op:
+  assumes "monoidal opp"
+    and "finite s"
+  shows "iterate opp s (\<lambda>x. opp (f x) (g x)) = opp (iterate opp s f) (iterate opp s g)"
+  using assms(2)
+proof (induct s)
+  case empty
+  then show ?case
+    unfolding iterate_insert[OF assms(1)] using assms(1) by auto
+next
+  case (insert x F)
+  show ?case
+    unfolding iterate_insert[OF assms(1) insert(1)] if_not_P[OF insert(2)] insert(3)
+    by (simp add: monoidal_ac[OF assms(1)])
+qed
+
+lemma iterate_eq:
+  assumes "monoidal opp"
+    and "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
   shows "iterate opp s f = iterate opp s g"
-proof- have *:"support opp g s = support opp f s"
+proof -
+  have *: "support opp g s = support opp f s"
     unfolding support_def using assms(2) by auto
   show ?thesis
-  proof(cases "finite (support opp f s)")
-    case False thus ?thesis apply(subst iterate_expand_cases,subst(2) iterate_expand_cases)
-      unfolding * by auto
-  next def su \<equiv> "support opp f s"
+  proof (cases "finite (support opp f s)")
+    case False
+    then show ?thesis
+      apply (subst iterate_expand_cases)
+      apply (subst(2) iterate_expand_cases)
+      unfolding *
+      apply auto
+      done
+  next
+    def su \<equiv> "support opp f s"
     case True note support_subset[of opp f s]
-    thus ?thesis apply- apply(subst iterate_support[symmetric],subst(2) iterate_support[symmetric]) unfolding * using True
+    then show ?thesis
+      apply -
+      apply (subst iterate_support[symmetric])
+      apply (subst(2) iterate_support[symmetric])
+      unfolding *
+      using True
       unfolding su_def[symmetric]
-    proof(induct su) case empty show ?case by auto
-    next case (insert x s) show ?case unfolding iterate_insert[OF assms(1) insert(1)]
-        unfolding if_not_P[OF insert(2)] apply(subst insert(3))
-        defer apply(subst assms(2)[of x]) using insert by auto qed qed qed
-
-lemma nonempty_witness: assumes "s \<noteq> {}" obtains x where "x \<in> s" using assms by auto
-
-lemma operative_division: fixes f::"('a::ordered_euclidean_space) set \<Rightarrow> 'b"
-  assumes "monoidal opp" "operative opp f" "d division_of {a..b}"
+    proof (induct su)
+      case empty
+      show ?case by auto
+    next
+      case (insert x s)
+      show ?case
+        unfolding iterate_insert[OF assms(1) insert(1)]
+        unfolding if_not_P[OF insert(2)]
+        apply (subst insert(3))
+        defer
+        apply (subst assms(2)[of x])
+        using insert
+        apply auto
+        done
+    qed
+  qed
+qed
+
+lemma nonempty_witness:
+  assumes "s \<noteq> {}"
+  obtains x where "x \<in> s"
+  using assms by auto
+
+lemma operative_division:
+  fixes f :: "'a::ordered_euclidean_space set \<Rightarrow> 'b"
+  assumes "monoidal opp"
+    and "operative opp f"
+    and "d division_of {a..b}"
   shows "iterate opp d f = f {a..b}"
-proof- def C \<equiv> "card (division_points {a..b} d)" thus ?thesis using assms
-  proof(induct C arbitrary:a b d rule:full_nat_induct)
+proof -
+  def C \<equiv> "card (division_points {a..b} d)"
+  then show ?thesis
+    using assms
+  proof (induct C arbitrary: a b d rule: full_nat_induct)
     case goal1
-    { presume *:"content {a..b} \<noteq> 0 \<Longrightarrow> ?case"
-      thus ?case apply-apply(cases) defer apply assumption
-      proof- assume as:"content {a..b} = 0"
-        show ?case unfolding operativeD(1)[OF assms(2) as] apply(rule iterate_eq_neutral[OF goal1(2)])
-        proof fix x assume x:"x\<in>d"
-          then guess u v apply(drule_tac division_ofD(4)[OF goal1(4)]) by(erule exE)+
-          thus "f x = neutral opp" using division_of_content_0[OF as goal1(4)]
-            using operativeD(1)[OF assms(2)] x by auto
-        qed qed }
+    { presume *: "content {a..b} \<noteq> 0 \<Longrightarrow> ?case"
+      then show ?case
+        apply -
+        apply cases
+        defer
+        apply assumption
+      proof -
+        assume as: "content {a..b} = 0"
+        show ?case
+          unfolding operativeD(1)[OF assms(2) as]
+          apply(rule iterate_eq_neutral[OF goal1(2)])
+        proof
+          fix x
+          assume x: "x \<in> d"
+          then guess u v
+            apply (drule_tac division_ofD(4)[OF goal1(4)])
+            apply (elim exE)
+            done
+          then show "f x = neutral opp"
+            using division_of_content_0[OF as goal1(4)]
+            using operativeD(1)[OF assms(2)] x
+            by auto
+        qed
+      qed
+    }
     assume "content {a..b} \<noteq> 0" note ab = this[unfolded content_lt_nz[symmetric] content_pos_lt_eq]
-    hence ab':"\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i" by (auto intro!: less_imp_le) show ?case
-    proof(cases "division_points {a..b} d = {}")
-      case True have d':"\<forall>i\<in>d. \<exists>u v. i = {u..v} \<and>
+    then have ab': "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
+      by (auto intro!: less_imp_le)
+    show ?case
+    proof (cases "division_points {a..b} d = {}")
+      case True
+      have d': "\<forall>i\<in>d. \<exists>u v. i = {u..v} \<and>
         (\<forall>j\<in>Basis. u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = a\<bullet>j \<or> u\<bullet>j = b\<bullet>j \<and> v\<bullet>j = b\<bullet>j \<or> u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = b\<bullet>j)"
-        unfolding forall_in_division[OF goal1(4)] apply(rule,rule,rule)
-        apply(rule_tac x=a in exI,rule_tac x=b in exI) apply(rule,rule refl)
+        unfolding forall_in_division[OF goal1(4)]
+        apply rule
+        apply rule
+        apply rule
+        apply (rule_tac x=a in exI)
+        apply (rule_tac x=b in exI)
+        apply rule
+        apply (rule refl)
       proof
-        fix u v and j :: 'a assume j:"j\<in>Basis" assume as:"{u..v} \<in> d" note division_ofD(3)[OF goal1(4) this]
-        hence uv:"\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i" "u\<bullet>j \<le> v\<bullet>j" using j unfolding interval_ne_empty by auto
-        have *:"\<And>p r Q. \<not> j\<in>Basis \<or> p \<or> r \<or> (\<forall>x\<in>d. Q x) \<Longrightarrow> p \<or> r \<or> (Q {u..v})" using as j by auto
+        fix u v
+        fix j :: 'a
+        assume j: "j \<in> Basis"
+        assume as: "{u..v} \<in> d"
+        note division_ofD(3)[OF goal1(4) this]
+        then have uv: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i" "u\<bullet>j \<le> v\<bullet>j"
+          using j unfolding interval_ne_empty by auto
+        have *: "\<And>p r Q. \<not> j\<in>Basis \<or> p \<or> r \<or> (\<forall>x\<in>d. Q x) \<Longrightarrow> p \<or> r \<or> Q {u..v}"
+          using as j by auto
         have "(j, u\<bullet>j) \<notin> division_points {a..b} d"
           "(j, v\<bullet>j) \<notin> division_points {a..b} d" using True by auto
         note this[unfolded de_Morgan_conj division_points_def mem_Collect_eq split_conv interval_bounds[OF ab'] bex_simps]
         note *[OF this(1)] *[OF this(2)] note this[unfolded interval_bounds[OF uv(1)]]
-        moreover have "a\<bullet>j \<le> u\<bullet>j" "v\<bullet>j \<le> b\<bullet>j" using division_ofD(2,2,3)[OF goal1(4) as]
-          unfolding subset_eq apply- apply(erule_tac x=u in ballE,erule_tac[3] x=v in ballE)
-          unfolding interval_ne_empty mem_interval using j by auto
+        moreover
+        have "a\<bullet>j \<le> u\<bullet>j" "v\<bullet>j \<le> b\<bullet>j"
+          using division_ofD(2,2,3)[OF goal1(4) as]
+          unfolding subset_eq
+          apply -
+          apply (erule_tac x=u in ballE,erule_tac[3] x=v in ballE)
+          unfolding interval_ne_empty mem_interval
+          using j
+          apply auto
+          done
         ultimately show "u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = a\<bullet>j \<or> u\<bullet>j = b\<bullet>j \<and> v\<bullet>j = b\<bullet>j \<or> u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = b\<bullet>j"
           unfolding not_less de_Morgan_disj using ab[rule_format,of j] uv(2) j by auto
       qed
       have "(1/2) *\<^sub>R (a+b) \<in> {a..b}"
         unfolding mem_interval using ab by(auto intro!: less_imp_le simp: inner_simps)
       note this[unfolded division_ofD(6)[OF goal1(4),symmetric] Union_iff]
-      then guess i .. note i=this guess u v using d'[rule_format,OF i(1)] apply-by(erule exE conjE)+ note uv=this
+      then guess i .. note i=this
+      guess u v using d'[rule_format,OF i(1)] by (elim exE conjE) note uv=this
       have "{a..b} \<in> d"
-      proof- { presume "i = {a..b}" thus ?thesis using i by auto }
-        { presume "u = a" "v = b" thus "i = {a..b}" using uv by auto }
-        show "u = a" "v = b" unfolding euclidean_eq_iff[where 'a='a]
-        proof(safe)
-          fix j :: 'a assume j:"j\<in>Basis"
+      proof -
+        { presume "i = {a..b}" then show ?thesis using i by auto }
+        { presume "u = a" "v = b" then show "i = {a..b}" using uv by auto }
+        show "u = a" "v = b"
+          unfolding euclidean_eq_iff[where 'a='a]
+        proof safe
+          fix j :: 'a
+          assume j: "j \<in> Basis"
           note i(2)[unfolded uv mem_interval,rule_format,of j]
-          thus "u \<bullet> j = a \<bullet> j" "v \<bullet> j = b \<bullet> j" using uv(2)[rule_format,of j] j by (auto simp: inner_simps)
-        qed qed
-      hence *:"d = insert {a..b} (d - {{a..b}})" by auto
-      have "iterate opp (d - {{a..b}}) f = neutral opp" apply(rule iterate_eq_neutral[OF goal1(2)])
-      proof fix x assume x:"x \<in> d - {{a..b}}" hence "x\<in>d" by auto note d'[rule_format,OF this]
-        then guess u v apply-by(erule exE conjE)+ note uv=this
-        have "u\<noteq>a \<or> v\<noteq>b" using x[unfolded uv] by auto
-        then obtain j where "u\<bullet>j \<noteq> a\<bullet>j \<or> v\<bullet>j \<noteq> b\<bullet>j" and j:"j\<in>Basis" unfolding euclidean_eq_iff[where 'a='a] by auto
-        hence "u\<bullet>j = v\<bullet>j" using uv(2)[rule_format,OF j] by auto
-        hence "content {u..v} = 0"  unfolding content_eq_0 apply(rule_tac x=j in bexI) using j by auto
-        thus "f x = neutral opp" unfolding uv(1) by(rule operativeD(1)[OF goal1(3)])
-      qed thus "iterate opp d f = f {a..b}" apply-apply(subst *)
-        apply(subst iterate_insert[OF goal1(2)]) using goal1(2,4) by auto
-    next case False hence "\<exists>x. x\<in>division_points {a..b} d" by auto
-      then guess k c unfolding split_paired_Ex apply- unfolding division_points_def mem_Collect_eq split_conv
-        by(erule exE conjE)+ note this(2-4,1) note kc=this[unfolded interval_bounds[OF ab']]
+          then show "u \<bullet> j = a \<bullet> j" and "v \<bullet> j = b \<bullet> j"
+            using uv(2)[rule_format,of j] j by (auto simp: inner_simps)
+        qed
+      qed
+      then have *: "d = insert {a..b} (d - {{a..b}})"
+        by auto
+      have "iterate opp (d - {{a..b}}) f = neutral opp"
+        apply (rule iterate_eq_neutral[OF goal1(2)])
+      proof
+        fix x
+        assume x: "x \<in> d - {{a..b}}"
+        then have "x\<in>d"
+          by auto note d'[rule_format,OF this]
+        then guess u v by (elim exE conjE) note uv=this
+        have "u \<noteq> a \<or> v \<noteq> b"
+          using x[unfolded uv] by auto
+        then obtain j where "u\<bullet>j \<noteq> a\<bullet>j \<or> v\<bullet>j \<noteq> b\<bullet>j" and j: "j \<in> Basis"
+          unfolding euclidean_eq_iff[where 'a='a] by auto
+        then have "u\<bullet>j = v\<bullet>j"
+          using uv(2)[rule_format,OF j] by auto
+        then have "content {u..v} = 0"
+          unfolding content_eq_0
+          apply (rule_tac x=j in bexI)
+          using j
+          apply auto
+          done
+        then show "f x = neutral opp"
+          unfolding uv(1) by (rule operativeD(1)[OF goal1(3)])
+      qed
+      then show "iterate opp d f = f {a..b}"
+        apply -
+        apply (subst *)
+        apply (subst iterate_insert[OF goal1(2)])
+        using goal1(2,4)
+        apply auto
+        done
+    next
+      case False
+      then have "\<exists>x. x \<in> division_points {a..b} d"
+        by auto
+      then guess k c
+        unfolding split_paired_Ex
+        unfolding division_points_def mem_Collect_eq split_conv
+        apply (elim exE conjE)
+        done
+      note this(2-4,1) note kc=this[unfolded interval_bounds[OF ab']]
       from this(3) guess j .. note j=this
       def d1 \<equiv> "{l \<inter> {x. x\<bullet>k \<le> c} | l. l \<in> d \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}}"
       def d2 \<equiv> "{l \<inter> {x. x\<bullet>k \<ge> c} | l. l \<in> d \<and> l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}}"
@@ -4230,392 +4694,839 @@
       def ca \<equiv> "(\<Sum>i\<in>Basis. (if i = k then c else a\<bullet>i) *\<^sub>R i)::'a"
       note division_points_psubset[OF goal1(4) ab kc(1-2) j]
       note psubset_card_mono[OF _ this(1)] psubset_card_mono[OF _ this(2)]
-      hence *:"(iterate opp d1 f) = f ({a..b} \<inter> {x. x\<bullet>k \<le> c})" "(iterate opp d2 f) = f ({a..b} \<inter> {x. x\<bullet>k \<ge> c})"
-        apply- unfolding interval_split[OF kc(4)] apply(rule_tac[!] goal1(1)[rule_format])
+      then have *: "(iterate opp d1 f) = f ({a..b} \<inter> {x. x\<bullet>k \<le> c})"
+        "(iterate opp d2 f) = f ({a..b} \<inter> {x. x\<bullet>k \<ge> c})"
+        unfolding interval_split[OF kc(4)]
+        apply (rule_tac[!] goal1(1)[rule_format])
         using division_split[OF goal1(4), where k=k and c=c]
-        unfolding interval_split[OF kc(4)] d1_def[symmetric] d2_def[symmetric] unfolding goal1(2) Suc_le_mono
-        using goal1(2-3) using division_points_finite[OF goal1(4)] using kc(4) by auto
+        unfolding interval_split[OF kc(4)] d1_def[symmetric] d2_def[symmetric]
+        unfolding goal1(2) Suc_le_mono
+        using goal1(2-3)
+        using division_points_finite[OF goal1(4)]
+        using kc(4)
+        apply auto
+        done
       have "f {a..b} = opp (iterate opp d1 f) (iterate opp d2 f)" (is "_ = ?prev")
-        unfolding * apply(rule operativeD(2)) using goal1(3) using kc(4) by auto
+        unfolding *
+        apply (rule operativeD(2))
+        using goal1(3)
+        using kc(4)
+        apply auto
+        done
       also have "iterate opp d1 f = iterate opp d (\<lambda>l. f(l \<inter> {x. x\<bullet>k \<le> c}))"
-        unfolding d1_def apply(rule iterate_nonzero_image_lemma[unfolded o_def])
-        unfolding empty_as_interval apply(rule goal1 division_of_finite operativeD[OF goal1(3)])+
-        unfolding empty_as_interval[symmetric] apply(rule content_empty)
-      proof(rule,rule,rule,erule conjE) fix l y assume as:"l \<in> d" "y \<in> d" "l \<inter> {x. x \<bullet> k \<le> c} = y \<inter> {x. x \<bullet> k \<le> c}" "l \<noteq> y"
-        from division_ofD(4)[OF goal1(4) this(1)] guess u v apply-by(erule exE)+ note l=this
-        show "f (l \<inter> {x. x \<bullet> k \<le> c}) = neutral opp" unfolding l interval_split[OF kc(4)]
-          apply(rule operativeD(1) goal1)+ unfolding interval_split[symmetric,OF kc(4)] apply(rule division_split_left_inj)
-          apply(rule goal1) unfolding l[symmetric] apply(rule as(1),rule as(2)) by(rule kc(4) as)+
-      qed also have "iterate opp d2 f = iterate opp d (\<lambda>l. f(l \<inter> {x. x\<bullet>k \<ge> c}))"
-        unfolding d2_def apply(rule iterate_nonzero_image_lemma[unfolded o_def])
-        unfolding empty_as_interval apply(rule goal1 division_of_finite operativeD[OF goal1(3)])+
-        unfolding empty_as_interval[symmetric] apply(rule content_empty)
-      proof(rule,rule,rule,erule conjE) fix l y assume as:"l \<in> d" "y \<in> d" "l \<inter> {x. c \<le> x \<bullet> k} = y \<inter> {x. c \<le> x \<bullet> k}" "l \<noteq> y"
-        from division_ofD(4)[OF goal1(4) this(1)] guess u v apply-by(erule exE)+ note l=this
-        show "f (l \<inter> {x. x \<bullet> k \<ge> c}) = neutral opp" unfolding l interval_split[OF kc(4)]
-          apply(rule operativeD(1) goal1)+ unfolding interval_split[symmetric,OF kc(4)] apply(rule division_split_right_inj)
-          apply(rule goal1) unfolding l[symmetric] apply(rule as(1),rule as(2)) by(rule as kc(4))+
-      qed also have *:"\<forall>x\<in>d. f x = opp (f (x \<inter> {x. x \<bullet> k \<le> c})) (f (x \<inter> {x. c \<le> x \<bullet> k}))"
-        unfolding forall_in_division[OF goal1(4)] apply(rule,rule,rule,rule operativeD(2)) using goal1(3) kc by auto
-      have "opp (iterate opp d (\<lambda>l. f (l \<inter> {x. x \<bullet> k \<le> c}))) (iterate opp d (\<lambda>l. f (l \<inter> {x. c \<le> x \<bullet> k})))
-        = iterate opp d f" apply(subst(3) iterate_eq[OF _ *[rule_format]]) prefer 3
-        apply(rule iterate_op[symmetric]) using goal1 by auto
+        unfolding d1_def
+        apply (rule iterate_nonzero_image_lemma[unfolded o_def])
+        unfolding empty_as_interval
+        apply (rule goal1 division_of_finite operativeD[OF goal1(3)])+
+        unfolding empty_as_interval[symmetric]
+        apply (rule content_empty)
+      proof (rule, rule, rule, erule conjE)
+        fix l y
+        assume as: "l \<in> d" "y \<in> d" "l \<inter> {x. x \<bullet> k \<le> c} = y \<inter> {x. x \<bullet> k \<le> c}" "l \<noteq> y"
+        from division_ofD(4)[OF goal1(4) this(1)] guess u v by (elim exE) note l=this
+        show "f (l \<inter> {x. x \<bullet> k \<le> c}) = neutral opp"
+          unfolding l interval_split[OF kc(4)]
+          apply (rule operativeD(1) goal1)+
+          unfolding interval_split[symmetric,OF kc(4)]
+          apply (rule division_split_left_inj)
+          apply (rule goal1)
+          unfolding l[symmetric]
+          apply (rule as(1), rule as(2))
+          apply (rule kc(4) as)+
+          done
+      qed
+      also have "iterate opp d2 f = iterate opp d (\<lambda>l. f(l \<inter> {x. x\<bullet>k \<ge> c}))"
+        unfolding d2_def
+        apply (rule iterate_nonzero_image_lemma[unfolded o_def])
+        unfolding empty_as_interval
+        apply (rule goal1 division_of_finite operativeD[OF goal1(3)])+
+        unfolding empty_as_interval[symmetric]
+        apply (rule content_empty)
+      proof (rule, rule, rule, erule conjE)
+        fix l y
+        assume as: "l \<in> d" "y \<in> d" "l \<inter> {x. c \<le> x \<bullet> k} = y \<inter> {x. c \<le> x \<bullet> k}" "l \<noteq> y"
+        from division_ofD(4)[OF goal1(4) this(1)] guess u v by (elim exE) note l=this
+        show "f (l \<inter> {x. x \<bullet> k \<ge> c}) = neutral opp"
+        unfolding l interval_split[OF kc(4)]
+          apply (rule operativeD(1) goal1)+
+          unfolding interval_split[symmetric,OF kc(4)]
+          apply (rule division_split_right_inj)
+          apply (rule goal1)
+          unfolding l[symmetric]
+          apply (rule as(1))
+          apply (rule as(2))
+          apply (rule as kc(4))+
+          done
+      qed also have *: "\<forall>x\<in>d. f x = opp (f (x \<inter> {x. x \<bullet> k \<le> c})) (f (x \<inter> {x. c \<le> x \<bullet> k}))"
+        unfolding forall_in_division[OF goal1(4)]
+        apply (rule, rule, rule, rule operativeD(2))
+        using goal1(3) kc
+        by auto
+      have "opp (iterate opp d (\<lambda>l. f (l \<inter> {x. x \<bullet> k \<le> c}))) (iterate opp d (\<lambda>l. f (l \<inter> {x. c \<le> x \<bullet> k}))) =
+        iterate opp d f"
+        apply (subst(3) iterate_eq[OF _ *[rule_format]])
+        prefer 3
+        apply (rule iterate_op[symmetric])
+        using goal1
+        apply auto
+        done
       finally show ?thesis by auto
-    qed qed qed
-
-lemma iterate_image_nonzero: assumes "monoidal opp"
-  "finite s" "\<forall>x\<in>s. \<forall>y\<in>s. ~(x = y) \<and> f x = f y \<longrightarrow> g(f x) = neutral opp"
-  shows "iterate opp (f ` s) g = iterate opp s (g \<circ> f)" using assms
-proof(induct rule:finite_subset_induct[OF assms(2) subset_refl])
-  case goal1 show ?case using assms(1) by auto
-next case goal2 have *:"\<And>x y. y = neutral opp \<Longrightarrow> x = opp y x" using assms(1) by auto
-  show ?case unfolding image_insert apply(subst iterate_insert[OF assms(1)])
-    apply(rule finite_imageI goal2)+
-    apply(cases "f a \<in> f ` F") unfolding if_P if_not_P apply(subst goal2(4)[OF assms(1) goal2(1)]) defer
-    apply(subst iterate_insert[OF assms(1) goal2(1)]) defer
-    apply(subst iterate_insert[OF assms(1) goal2(1)])
-    unfolding if_not_P[OF goal2(3)] defer unfolding image_iff defer apply(erule bexE)
-    apply(rule *) unfolding o_def apply(rule_tac y=x in goal2(7)[rule_format])
-    using goal2 unfolding o_def by auto qed
-
-lemma operative_tagged_division: assumes "monoidal opp" "operative opp f" "d tagged_division_of {a..b}"
-  shows "iterate(opp) d (\<lambda>(x,l). f l) = f {a..b}"
-proof- have *:"(\<lambda>(x,l). f l) = (f o snd)" unfolding o_def by(rule,auto) note assm = tagged_division_ofD[OF assms(3)]
-  have "iterate(opp) d (\<lambda>(x,l). f l) = iterate opp (snd ` d) f" unfolding *
-    apply(rule iterate_image_nonzero[symmetric,OF assms(1)]) apply(rule tagged_division_of_finite assms)+
-    unfolding Ball_def split_paired_All snd_conv apply(rule,rule,rule,rule,rule,rule,rule,erule conjE)
-  proof- fix a b aa ba assume as:"(a, b) \<in> d" "(aa, ba) \<in> d" "(a, b) \<noteq> (aa, ba)" "b = ba"
-    guess u v using assm(4)[OF as(1)] apply-by(erule exE)+ note uv=this
-    show "f b = neutral opp" unfolding uv apply(rule operativeD(1)[OF assms(2)])
-      unfolding content_eq_0_interior using tagged_division_ofD(5)[OF assms(3) as(1-3)]
-      unfolding as(4)[symmetric] uv by auto
-  qed also have "\<dots> = f {a..b}"
+    qed
+  qed
+qed
+
+lemma iterate_image_nonzero:
+  assumes "monoidal opp"
+    and "finite s"
+    and "\<forall>x\<in>s. \<forall>y\<in>s. x \<noteq> y \<and> f x = f y \<longrightarrow> g (f x) = neutral opp"
+  shows "iterate opp (f ` s) g = iterate opp s (g \<circ> f)"
+  using assms
+proof (induct rule: finite_subset_induct[OF assms(2) subset_refl])
+  case goal1
+  show ?case
+    using assms(1) by auto
+next
+  case goal2
+  have *: "\<And>x y. y = neutral opp \<Longrightarrow> x = opp y x"
+    using assms(1) by auto
+  show ?case
+    unfolding image_insert
+    apply (subst iterate_insert[OF assms(1)])
+    apply (rule finite_imageI goal2)+
+    apply (cases "f a \<in> f ` F")
+    unfolding if_P if_not_P
+    apply (subst goal2(4)[OF assms(1) goal2(1)])
+    defer
+    apply (subst iterate_insert[OF assms(1) goal2(1)])
+    defer
+    apply (subst iterate_insert[OF assms(1) goal2(1)])
+    unfolding if_not_P[OF goal2(3)]
+    defer unfolding image_iff
+    defer
+    apply (erule bexE)
+    apply (rule *)
+    unfolding o_def
+    apply (rule_tac y=x in goal2(7)[rule_format])
+    using goal2
+    unfolding o_def
+    apply auto
+    done
+qed
+
+lemma operative_tagged_division:
+  assumes "monoidal opp"
+    and "operative opp f"
+    and "d tagged_division_of {a..b}"
+  shows "iterate opp d (\<lambda>(x,l). f l) = f {a..b}"
+proof -
+  have *: "(\<lambda>(x,l). f l) = f \<circ> snd"
+    unfolding o_def by rule auto note assm = tagged_division_ofD[OF assms(3)]
+  have "iterate opp d (\<lambda>(x,l). f l) = iterate opp (snd ` d) f"
+    unfolding *
+    apply (rule iterate_image_nonzero[symmetric,OF assms(1)])
+    apply (rule tagged_division_of_finite assms)+
+    unfolding Ball_def split_paired_All snd_conv
+    apply (rule, rule, rule, rule, rule, rule, rule, erule conjE)
+  proof -
+    fix a b aa ba
+    assume as: "(a, b) \<in> d" "(aa, ba) \<in> d" "(a, b) \<noteq> (aa, ba)" "b = ba"
+    guess u v using assm(4)[OF as(1)] by (elim exE) note uv=this
+    show "f b = neutral opp"
+      unfolding uv
+      apply (rule operativeD(1)[OF assms(2)])
+      unfolding content_eq_0_interior
+      using tagged_division_ofD(5)[OF assms(3) as(1-3)]
+      unfolding as(4)[symmetric] uv
+      apply auto
+      done
+  qed
+  also have "\<dots> = f {a..b}"
     using operative_division[OF assms(1-2) division_of_tagged_division[OF assms(3)]] .
-  finally show ?thesis . qed
+  finally show ?thesis .
+qed
+
 
 subsection {* Additivity of content. *}
 
 lemma setsum_iterate:
-  assumes "finite s" shows "setsum f s = iterate op + s f"
+  assumes "finite s"
+  shows "setsum f s = iterate op + s f"
 proof -
   have *: "setsum f s = setsum f (support op + f s)"
     apply (rule setsum_mono_zero_right)
-    unfolding support_def neutral_monoid using assms by auto
+    unfolding support_def neutral_monoid
+    using assms
+    apply auto
+    done
   then show ?thesis unfolding * iterate_def fold'_def setsum.eq_fold
     unfolding neutral_monoid by (simp add: comp_def)
 qed
 
-lemma additive_content_division: assumes "d division_of {a..b}"
-  shows "setsum content d = content({a..b})"
+lemma additive_content_division:
+  assumes "d division_of {a..b}"
+  shows "setsum content d = content {a..b}"
   unfolding operative_division[OF monoidal_monoid operative_content assms,symmetric]
-  apply(subst setsum_iterate) using assms by auto
+  apply (subst setsum_iterate)
+  using assms
+  apply auto
+  done
 
 lemma additive_content_tagged_division:
   assumes "d tagged_division_of {a..b}"
-  shows "setsum (\<lambda>(x,l). content l) d = content({a..b})"
+  shows "setsum (\<lambda>(x,l). content l) d = content {a..b}"
   unfolding operative_tagged_division[OF monoidal_monoid operative_content assms,symmetric]
-  apply(subst setsum_iterate) using assms by auto
+  apply (subst setsum_iterate)
+  using assms
+  apply auto
+  done
+
 
 subsection {* Finally, the integral of a constant *}
 
 lemma has_integral_const[intro]:
-  "((\<lambda>x. c) has_integral (content({a..b::'a::ordered_euclidean_space}) *\<^sub>R c)) ({a..b})"
-  unfolding has_integral apply(rule,rule,rule_tac x="\<lambda>x. ball x 1" in exI)
-  apply(rule,rule gauge_trivial)apply(rule,rule,erule conjE)
-  unfolding split_def apply(subst scaleR_left.setsum[symmetric, unfolded o_def])
-  defer apply(subst additive_content_tagged_division[unfolded split_def]) apply assumption by auto
+  fixes a b :: "'a::ordered_euclidean_space"
+  shows "((\<lambda>x. c) has_integral (content {a..b} *\<^sub>R c)) {a..b}"
+  unfolding has_integral
+  apply rule
+  apply rule
+  apply (rule_tac x="\<lambda>x. ball x 1" in exI)
+  apply rule
+  apply (rule gauge_trivial)
+  apply rule
+  apply rule
+  apply (erule conjE)
+  unfolding split_def
+  apply (subst scaleR_left.setsum[symmetric, unfolded o_def])
+  defer
+  apply (subst additive_content_tagged_division[unfolded split_def])
+  apply assumption
+  apply auto
+  done
 
 lemma integral_const[simp]:
   fixes a b :: "'a::ordered_euclidean_space"
   shows "integral {a .. b} (\<lambda>x. c) = content {a .. b} *\<^sub>R c"
   by (rule integral_unique) (rule has_integral_const)
 
+
 subsection {* Bounds on the norm of Riemann sums and the integral itself. *}
 
-lemma dsum_bound: assumes "p division_of {a..b}" "norm(c) \<le> e"
-  shows "norm(setsum (\<lambda>l. content l *\<^sub>R c) p) \<le> e * content({a..b})" (is "?l \<le> ?r")
-  apply(rule order_trans,rule norm_setsum) unfolding norm_scaleR setsum_left_distrib[symmetric]
-  apply(rule order_trans[OF mult_left_mono],rule assms,rule setsum_abs_ge_zero)
-  apply(subst mult_commute) apply(rule mult_left_mono)
-  apply(rule order_trans[of _ "setsum content p"]) apply(rule eq_refl,rule setsum_cong2)
-  apply(subst abs_of_nonneg) unfolding additive_content_division[OF assms(1)]
-proof- from order_trans[OF norm_ge_zero[of c] assms(2)] show "0 \<le> e" .
-  fix x assume "x\<in>p" from division_ofD(4)[OF assms(1) this] guess u v apply-by(erule exE)+
-  thus "0 \<le> content x" using content_pos_le by auto
-qed(insert assms,auto)
-
-lemma rsum_bound: assumes "p tagged_division_of {a..b}" "\<forall>x\<in>{a..b}. norm(f x) \<le> e"
-  shows "norm(setsum (\<lambda>(x,k). content k *\<^sub>R f x) p) \<le> e * content({a..b})"
-proof(cases "{a..b} = {}") case True
-  show ?thesis using assms(1) unfolding True tagged_division_of_trivial by auto
-next case False show ?thesis
-    apply(rule order_trans,rule norm_setsum) unfolding split_def norm_scaleR
-    apply(rule order_trans[OF setsum_mono]) apply(rule mult_left_mono[OF _ abs_ge_zero, of _ e]) defer
-    unfolding setsum_left_distrib[symmetric] apply(subst mult_commute) apply(rule mult_left_mono)
-    apply(rule order_trans[of _ "setsum (content \<circ> snd) p"]) apply(rule eq_refl,rule setsum_cong2)
-    apply(subst o_def, rule abs_of_nonneg)
-  proof- show "setsum (content \<circ> snd) p \<le> content {a..b}" apply(rule eq_refl)
-      unfolding additive_content_tagged_division[OF assms(1),symmetric] split_def by auto
+lemma dsum_bound:
+  assumes "p division_of {a..b}"
+    and "norm c \<le> e"
+  shows "norm (setsum (\<lambda>l. content l *\<^sub>R c) p) \<le> e * content({a..b})"
+  apply (rule order_trans)
+  apply (rule norm_setsum)
+  unfolding norm_scaleR setsum_left_distrib[symmetric]
+  apply (rule order_trans[OF mult_left_mono])
+  apply (rule assms)
+  apply (rule setsum_abs_ge_zero)
+  apply (subst mult_commute)
+  apply (rule mult_left_mono)
+  apply (rule order_trans[of _ "setsum content p"])
+  apply (rule eq_refl)
+  apply (rule setsum_cong2)
+  apply (subst abs_of_nonneg)
+  unfolding additive_content_division[OF assms(1)]
+proof -
+  from order_trans[OF norm_ge_zero[of c] assms(2)]
+  show "0 \<le> e" .
+  fix x assume "x \<in> p"
+  from division_ofD(4)[OF assms(1) this] guess u v by (elim exE)
+  then show "0 \<le> content x"
+    using content_pos_le by auto
+qed (insert assms, auto)
+
+lemma rsum_bound:
+  assumes "p tagged_division_of {a..b}"
+    and "\<forall>x\<in>{a..b}. norm (f x) \<le> e"
+  shows "norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p) \<le> e * content {a..b}"
+proof (cases "{a..b} = {}")
+  case True
+  show ?thesis
+    using assms(1) unfolding True tagged_division_of_trivial by auto
+next
+  case False
+  show ?thesis
+    apply (rule order_trans)
+    apply (rule norm_setsum)
+    unfolding split_def norm_scaleR
+    apply (rule order_trans[OF setsum_mono])
+    apply (rule mult_left_mono[OF _ abs_ge_zero, of _ e])
+    defer
+    unfolding setsum_left_distrib[symmetric]
+    apply (subst mult_commute)
+    apply (rule mult_left_mono)
+    apply (rule order_trans[of _ "setsum (content \<circ> snd) p"])
+    apply (rule eq_refl)
+    apply (rule setsum_cong2)
+    apply (subst o_def)
+    apply (rule abs_of_nonneg)
+  proof -
+    show "setsum (content \<circ> snd) p \<le> content {a..b}"
+      apply (rule eq_refl)
+      unfolding additive_content_tagged_division[OF assms(1),symmetric] split_def
+      apply auto
+      done
     guess w using nonempty_witness[OF False] .
-    thus "e\<ge>0" apply-apply(rule order_trans) defer apply(rule assms(2)[rule_format],assumption) by auto
-    fix xk assume *:"xk\<in>p" guess x k  using surj_pair[of xk] apply-by(erule exE)+ note xk = this *[unfolded this]
-    from tagged_division_ofD(4)[OF assms(1) xk(2)] guess u v apply-by(erule exE)+ note uv=this
-    show "0\<le> content (snd xk)" unfolding xk snd_conv uv by(rule content_pos_le)
-    show "norm (f (fst xk)) \<le> e" unfolding xk fst_conv using tagged_division_ofD(2,3)[OF assms(1) xk(2)] assms(2) by auto
-  qed qed
+    then show "e \<ge> 0"
+      apply -
+      apply (rule order_trans)
+      defer
+      apply (rule assms(2)[rule_format])
+      apply assumption
+      apply auto
+      done
+    fix xk
+    assume *: "xk \<in> p"
+    guess x k using surj_pair[of xk] by (elim exE) note xk = this *[unfolded this]
+    from tagged_division_ofD(4)[OF assms(1) xk(2)] guess u v by (elim exE) note uv=this
+    show "0 \<le> content (snd xk)"
+      unfolding xk snd_conv uv by(rule content_pos_le)
+    show "norm (f (fst xk)) \<le> e"
+      unfolding xk fst_conv using tagged_division_ofD(2,3)[OF assms(1) xk(2)] assms(2) by auto
+  qed
+qed
 
 lemma rsum_diff_bound:
-  assumes "p tagged_division_of {a..b}"  "\<forall>x\<in>{a..b}. norm(f x - g x) \<le> e"
-  shows "norm(setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - setsum (\<lambda>(x,k). content k *\<^sub>R g x) p) \<le> e * content({a..b})"
-  apply(rule order_trans[OF _ rsum_bound[OF assms]]) apply(rule eq_refl) apply(rule arg_cong[where f=norm])
-  unfolding setsum_subtractf[symmetric] apply(rule setsum_cong2) unfolding scaleR_diff_right by auto
-
-lemma has_integral_bound: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
-  assumes "0 \<le> B" "(f has_integral i) ({a..b})" "\<forall>x\<in>{a..b}. norm(f x) \<le> B"
+  assumes "p tagged_division_of {a..b}"
+    and "\<forall>x\<in>{a..b}. norm (f x - g x) \<le> e"
+  shows "norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - setsum (\<lambda>(x,k). content k *\<^sub>R g x) p) \<le>
+    e * content {a..b}"
+  apply (rule order_trans[OF _ rsum_bound[OF assms]])
+  apply (rule eq_refl)
+  apply (rule arg_cong[where f=norm])
+  unfolding setsum_subtractf[symmetric]
+  apply (rule setsum_cong2)
+  unfolding scaleR_diff_right
+  apply auto
+  done
+
+lemma has_integral_bound:
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
+  assumes "0 \<le> B"
+    and "(f has_integral i) {a..b}"
+    and "\<forall>x\<in>{a..b}. norm (f x) \<le> B"
   shows "norm i \<le> B * content {a..b}"
-proof- let ?P = "content {a..b} > 0" { presume "?P \<Longrightarrow> ?thesis"
-    thus ?thesis proof(cases ?P) case False
-      hence *:"content {a..b} = 0" using content_lt_nz by auto
-      hence **:"i = 0" using assms(2) apply(subst has_integral_null_eq[symmetric]) by auto
-      show ?thesis unfolding * ** using assms(1) by auto
-    qed auto } assume ab:?P
-  { presume "\<not> ?thesis \<Longrightarrow> False" thus ?thesis by auto }
-  assume "\<not> ?thesis" hence *:"norm i - B * content {a..b} > 0" by auto
-  from assms(2)[unfolded has_integral,rule_format,OF *] guess d apply-by(erule exE conjE)+ note d=this[rule_format]
+proof -
+  let ?P = "content {a..b} > 0"
+  {
+    presume "?P \<Longrightarrow> ?thesis"
+    then show ?thesis
+    proof (cases ?P)
+      case False
+      then have *: "content {a..b} = 0"
+        using content_lt_nz by auto
+      hence **: "i = 0"
+        using assms(2)
+        apply (subst has_integral_null_eq[symmetric])
+        apply auto
+        done
+      show ?thesis
+        unfolding * ** using assms(1) by auto
+    qed auto
+  }
+  assume ab: ?P
+  { presume "\<not> ?thesis \<Longrightarrow> False" then show ?thesis by auto }
+  assume "\<not> ?thesis"
+  then have *: "norm i - B * content {a..b} > 0"
+    by auto
+  from assms(2)[unfolded has_integral,rule_format,OF *]
+  guess d by (elim exE conjE) note d=this[rule_format]
   from fine_division_exists[OF this(1), of a b] guess p . note p=this
-  have *:"\<And>s B. norm s \<le> B \<Longrightarrow> \<not> (norm (s - i) < norm i - B)"
-  proof- case goal1 thus ?case unfolding not_less
-    using norm_triangle_sub[of i s] unfolding norm_minus_commute by auto
-  qed show False using d(2)[OF conjI[OF p]] *[OF rsum_bound[OF p(1) assms(3)]] by auto qed
+  have *: "\<And>s B. norm s \<le> B \<Longrightarrow> \<not> norm (s - i) < norm i - B"
+  proof -
+    case goal1
+    then show ?case
+      unfolding not_less
+      using norm_triangle_sub[of i s]
+      unfolding norm_minus_commute
+      by auto
+  qed
+  show False
+    using d(2)[OF conjI[OF p]] *[OF rsum_bound[OF p(1) assms(3)]] by auto
+qed
+
 
 subsection {* Similar theorems about relationship among components. *}
 
-lemma rsum_component_le: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes "p tagged_division_of {a..b}"  "\<forall>x\<in>{a..b}. (f x)\<bullet>i \<le> (g x)\<bullet>i"
+lemma rsum_component_le:
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "p tagged_division_of {a..b}"
+    and "\<forall>x\<in>{a..b}. (f x)\<bullet>i \<le> (g x)\<bullet>i"
   shows "(setsum (\<lambda>(x,k). content k *\<^sub>R f x) p)\<bullet>i \<le> (setsum (\<lambda>(x,k). content k *\<^sub>R g x) p)\<bullet>i"
-  unfolding inner_setsum_left apply(rule setsum_mono) apply safe
-proof- fix a b assume ab:"(a,b) \<in> p" note assm = tagged_division_ofD(2-4)[OF assms(1) ab]
-  from this(3) guess u v apply-by(erule exE)+ note b=this
-  show "(content b *\<^sub>R f a) \<bullet> i \<le> (content b *\<^sub>R g a) \<bullet> i" unfolding b
-    unfolding inner_simps real_scaleR_def apply(rule mult_left_mono)
-    defer apply(rule content_pos_le,rule assms(2)[rule_format]) using assm by auto qed
+  unfolding inner_setsum_left
+  apply (rule setsum_mono)
+  apply safe
+proof -
+  fix a b
+  assume ab: "(a, b) \<in> p"
+  note assm = tagged_division_ofD(2-4)[OF assms(1) ab]
+  from this(3) guess u v by (elim exE) note b=this
+  show "(content b *\<^sub>R f a) \<bullet> i \<le> (content b *\<^sub>R g a) \<bullet> i"
+    unfolding b
+    unfolding inner_simps real_scaleR_def
+    apply (rule mult_left_mono)
+    defer
+    apply (rule content_pos_le,rule assms(2)[rule_format])
+    using assm
+    apply auto
+    done
+qed
 
 lemma has_integral_component_le:
-  fixes f g::"'a::ordered_euclidean_space \<Rightarrow> 'b::euclidean_space"
+  fixes f g :: "'a::ordered_euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes k: "k \<in> Basis"
-  assumes "(f has_integral i) s" "(g has_integral j) s"  "\<forall>x\<in>s. (f x)\<bullet>k \<le> (g x)\<bullet>k"
+  assumes "(f has_integral i) s" "(g has_integral j) s"
+    and "\<forall>x\<in>s. (f x)\<bullet>k \<le> (g x)\<bullet>k"
   shows "i\<bullet>k \<le> j\<bullet>k"
 proof -
   have lem:"\<And>a b i (j::'b). \<And>g f::'a \<Rightarrow> 'b. (f has_integral i) ({a..b}) \<Longrightarrow>
     (g has_integral j) ({a..b}) \<Longrightarrow> \<forall>x\<in>{a..b}. (f x)\<bullet>k \<le> (g x)\<bullet>k \<Longrightarrow> i\<bullet>k \<le> j\<bullet>k"
   proof (rule ccontr)
     case goal1
-    then have *: "0 < (i\<bullet>k - j\<bullet>k) / 3" by auto
-    guess d1 using goal1(1)[unfolded has_integral,rule_format,OF *] apply-by(erule exE conjE)+ note d1=this[rule_format]
-    guess d2 using goal1(2)[unfolded has_integral,rule_format,OF *] apply-by(erule exE conjE)+ note d2=this[rule_format]
+    then have *: "0 < (i\<bullet>k - j\<bullet>k) / 3"
+      by auto
+    guess d1 using goal1(1)[unfolded has_integral,rule_format,OF *] by (elim exE conjE) note d1=this[rule_format]
+    guess d2 using goal1(2)[unfolded has_integral,rule_format,OF *] by (elim exE conjE) note d2=this[rule_format]
     guess p using fine_division_exists[OF gauge_inter[OF d1(1) d2(1)], of a b] unfolding fine_inter .
     note p = this(1) conjunctD2[OF this(2)]
     note le_less_trans[OF Basis_le_norm[OF k]]
     note this[OF d1(2)[OF conjI[OF p(1,2)]]] this[OF d2(2)[OF conjI[OF p(1,3)]]]
-    thus False
+    then show False
       unfolding inner_simps
       using rsum_component_le[OF p(1) goal1(3)]
       by (simp add: abs_real_def split: split_if_asm)
-  qed let ?P = "\<exists>a b. s = {a..b}"
-  { presume "\<not> ?P \<Longrightarrow> ?thesis" thus ?thesis proof(cases ?P)
-      case True then guess a b apply-by(erule exE)+ note s=this
-      show ?thesis apply(rule lem) using assms[unfolded s] by auto
-    qed auto } assume as:"\<not> ?P"
-  { presume "\<not> ?thesis \<Longrightarrow> False" thus ?thesis by auto }
-  assume "\<not> i\<bullet>k \<le> j\<bullet>k" hence ij:"(i\<bullet>k - j\<bullet>k) / 3 > 0" by auto
+  qed
+  let ?P = "\<exists>a b. s = {a..b}"
+  {
+    presume "\<not> ?P \<Longrightarrow> ?thesis"
+    then show ?thesis
+    proof (cases ?P)
+      case True
+      then guess a b by (elim exE) note s=this
+      show ?thesis
+        apply (rule lem)
+        using assms[unfolded s]
+        apply auto
+        done
+    qed auto
+  }
+  assume as: "\<not> ?P"
+  { presume "\<not> ?thesis \<Longrightarrow> False" then show ?thesis by auto }
+  assume "\<not> i\<bullet>k \<le> j\<bullet>k"
+  then have ij: "(i\<bullet>k - j\<bullet>k) / 3 > 0"
+    by auto
   note has_integral_altD[OF _ as this]
   from this[OF assms(2)] this[OF assms(3)] guess B1 B2 . note B=this[rule_format]
-  have "bounded (ball 0 B1 \<union> ball (0::'a) B2)" unfolding bounded_Un by(rule conjI bounded_ball)+
-  from bounded_subset_closed_interval[OF this] guess a b apply- by(erule exE)+
+  have "bounded (ball 0 B1 \<union> ball (0::'a) B2)"
+    unfolding bounded_Un by(rule conjI bounded_ball)+
+  from bounded_subset_closed_interval[OF this] guess a b by (elim exE)
   note ab = conjunctD2[OF this[unfolded Un_subset_iff]]
   guess w1 using B(2)[OF ab(1)] .. note w1=conjunctD2[OF this]
   guess w2 using B(4)[OF ab(2)] .. note w2=conjunctD2[OF this]
-  have *:"\<And>w1 w2 j i::real .\<bar>w1 - i\<bar> < (i - j) / 3 \<Longrightarrow> \<bar>w2 - j\<bar> < (i - j) / 3 \<Longrightarrow> w1 \<le> w2 \<Longrightarrow> False"
+  have *: "\<And>w1 w2 j i::real .\<bar>w1 - i\<bar> < (i - j) / 3 \<Longrightarrow> \<bar>w2 - j\<bar> < (i - j) / 3 \<Longrightarrow> w1 \<le> w2 \<Longrightarrow> False"
     by (simp add: abs_real_def split: split_if_asm)
-  note le_less_trans[OF Basis_le_norm[OF k]] note this[OF w1(2)] this[OF w2(2)] moreover
-  have "w1\<bullet>k \<le> w2\<bullet>k" apply(rule lem[OF w1(1) w2(1)]) using assms by auto ultimately
-  show False unfolding inner_simps by(rule *)
+  note le_less_trans[OF Basis_le_norm[OF k]]
+  note this[OF w1(2)] this[OF w2(2)]
+  moreover
+  have "w1\<bullet>k \<le> w2\<bullet>k"
+    apply (rule lem[OF w1(1) w2(1)])
+    using assms
+    apply auto
+    done
+  ultimately show False
+    unfolding inner_simps by(rule *)
 qed
 
-lemma integral_component_le: fixes g f::"'a::ordered_euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes "k\<in>Basis" "f integrable_on s" "g integrable_on s"  "\<forall>x\<in>s. (f x)\<bullet>k \<le> (g x)\<bullet>k"
+lemma integral_component_le:
+  fixes g f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "k \<in> Basis"
+    and "f integrable_on s" "g integrable_on s"
+    and "\<forall>x\<in>s. (f x)\<bullet>k \<le> (g x)\<bullet>k"
   shows "(integral s f)\<bullet>k \<le> (integral s g)\<bullet>k"
-  apply(rule has_integral_component_le) using integrable_integral assms by auto
-
-lemma has_integral_component_nonneg: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes "k\<in>Basis" "(f has_integral i) s" "\<forall>x\<in>s. 0 \<le> (f x)\<bullet>k" shows "0 \<le> i\<bullet>k"
-  using has_integral_component_le[OF assms(1) has_integral_0 assms(2)] using assms(3-) by auto
-
-lemma integral_component_nonneg: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes "k\<in>Basis" "f integrable_on s" "\<forall>x\<in>s. 0 \<le> (f x)\<bullet>k" shows "0 \<le> (integral s f)\<bullet>k"
-  apply(rule has_integral_component_nonneg) using assms by auto
-
-lemma has_integral_component_neg: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::ordered_euclidean_space"
-  assumes "k\<in>Basis" "(f has_integral i) s" "\<forall>x\<in>s. (f x)\<bullet>k \<le> 0"shows "i\<bullet>k \<le> 0"
-  using has_integral_component_le[OF assms(1,2) has_integral_0] assms(2-) by auto
+  apply (rule has_integral_component_le)
+  using integrable_integral assms
+  apply auto
+  done
+
+lemma has_integral_component_nonneg:
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "k \<in> Basis"
+    and "(f has_integral i) s"
+    and "\<forall>x\<in>s. 0 \<le> (f x)\<bullet>k"
+  shows "0 \<le> i\<bullet>k"
+  using has_integral_component_le[OF assms(1) has_integral_0 assms(2)]
+  using assms(3-)
+  by auto
+
+lemma integral_component_nonneg:
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "k \<in> Basis"
+    and "f integrable_on s" "\<forall>x\<in>s. 0 \<le> (f x)\<bullet>k"
+  shows "0 \<le> (integral s f)\<bullet>k"
+  apply (rule has_integral_component_nonneg)
+  using assms
+  apply auto
+  done
+
+lemma has_integral_component_neg:
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::ordered_euclidean_space"
+  assumes "k \<in> Basis"
+    and "(f has_integral i) s"
+    and "\<forall>x\<in>s. (f x)\<bullet>k \<le> 0"
+  shows "i\<bullet>k \<le> 0"
+  using has_integral_component_le[OF assms(1,2) has_integral_0] assms(2-)
+  by auto
 
 lemma has_integral_component_lbound:
-  fixes f::"'a::ordered_euclidean_space => 'b::ordered_euclidean_space"
-  assumes "(f has_integral i) {a..b}"  "\<forall>x\<in>{a..b}. B \<le> f(x)\<bullet>k" "k\<in>Basis"
+  fixes f :: "'a::ordered_euclidean_space => 'b::ordered_euclidean_space"
+  assumes "(f has_integral i) {a..b}"
+    and "\<forall>x\<in>{a..b}. B \<le> f(x)\<bullet>k"
+    and "k \<in> Basis"
   shows "B * content {a..b} \<le> i\<bullet>k"
   using has_integral_component_le[OF assms(3) has_integral_const assms(1),of "(\<Sum>i\<in>Basis. B *\<^sub>R i)::'b"] assms(2-)
-  by (auto simp add:field_simps)
+  by (auto simp add: field_simps)
 
 lemma has_integral_component_ubound:
   fixes f::"'a::ordered_euclidean_space => 'b::ordered_euclidean_space"
-  assumes "(f has_integral i) {a..b}" "\<forall>x\<in>{a..b}. f x\<bullet>k \<le> B" "k\<in>Basis"
-  shows "i\<bullet>k \<le> B * content({a..b})"
-  using has_integral_component_le[OF assms(3,1) has_integral_const, of "\<Sum>i\<in>Basis. B *\<^sub>R i"]  assms(2-)
-  by(auto simp add:field_simps)
-
-lemma integral_component_lbound: fixes f::"'a::ordered_euclidean_space => 'b::ordered_euclidean_space"
-  assumes "f integrable_on {a..b}" "\<forall>x\<in>{a..b}. B \<le> f(x)\<bullet>k" "k\<in>Basis"
-  shows "B * content({a..b}) \<le> (integral({a..b}) f)\<bullet>k"
-  apply(rule has_integral_component_lbound) using assms unfolding has_integral_integral by auto
-
-lemma integral_component_ubound: fixes f::"'a::ordered_euclidean_space => 'b::ordered_euclidean_space"
-  assumes "f integrable_on {a..b}" "\<forall>x\<in>{a..b}. f(x)\<bullet>k \<le> B" "k\<in>Basis"
-  shows "(integral({a..b}) f)\<bullet>k \<le> B * content({a..b})"
-  apply(rule has_integral_component_ubound) using assms unfolding has_integral_integral by auto
+  assumes "(f has_integral i) {a..b}"
+    and "\<forall>x\<in>{a..b}. f x\<bullet>k \<le> B"
+    and "k \<in> Basis"
+  shows "i\<bullet>k \<le> B * content {a..b}"
+  using has_integral_component_le[OF assms(3,1) has_integral_const, of "\<Sum>i\<in>Basis. B *\<^sub>R i"] assms(2-)
+  by (auto simp add: field_simps)
+
+lemma integral_component_lbound:
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::ordered_euclidean_space"
+  assumes "f integrable_on {a..b}"
+    and "\<forall>x\<in>{a..b}. B \<le> f(x)\<bullet>k"
+    and "k \<in> Basis"
+  shows "B * content {a..b} \<le> (integral({a..b}) f)\<bullet>k"
+  apply (rule has_integral_component_lbound)
+  using assms
+  unfolding has_integral_integral
+  apply auto
+  done
+
+lemma integral_component_ubound:
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::ordered_euclidean_space"
+  assumes "f integrable_on {a..b}"
+    and "\<forall>x\<in>{a..b}. f x\<bullet>k \<le> B"
+    and "k \<in> Basis"
+  shows "(integral {a..b} f)\<bullet>k \<le> B * content {a..b}"
+  apply (rule has_integral_component_ubound)
+  using assms
+  unfolding has_integral_integral
+  apply auto
+  done
+
 
 subsection {* Uniform limit of integrable functions is integrable. *}
 
-lemma integrable_uniform_limit: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::banach"
-  assumes "\<forall>e>0. \<exists>g. (\<forall>x\<in>{a..b}. norm(f x - g x) \<le> e) \<and> g integrable_on {a..b}"
+lemma integrable_uniform_limit:
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::banach"
+  assumes "\<forall>e>0. \<exists>g. (\<forall>x\<in>{a..b}. norm (f x - g x) \<le> e) \<and> g integrable_on {a..b}"
   shows "f integrable_on {a..b}"
-proof- { presume *:"content {a..b} > 0 \<Longrightarrow> ?thesis"
-    show ?thesis apply cases apply(rule *,assumption)
-      unfolding content_lt_nz integrable_on_def using has_integral_null by auto }
-  assume as:"content {a..b} > 0"
-  have *:"\<And>P. \<forall>e>(0::real). P e \<Longrightarrow> \<forall>n::nat. P (inverse (real n+1))" by auto
+proof -
+  {
+    presume *: "content {a..b} > 0 \<Longrightarrow> ?thesis"
+    show ?thesis
+      apply cases
+      apply (rule *)
+      apply assumption
+      unfolding content_lt_nz integrable_on_def
+      using has_integral_null
+      apply auto
+      done
+  }
+  assume as: "content {a..b} > 0"
+  have *: "\<And>P. \<forall>e>(0::real). P e \<Longrightarrow> \<forall>n::nat. P (inverse (real n + 1))"
+    by auto
   from choice[OF *[OF assms]] guess g .. note g=conjunctD2[OF this[rule_format],rule_format]
   from choice[OF allI[OF g(2)[unfolded integrable_on_def], of "\<lambda>x. x"]] guess i .. note i=this[rule_format]
 
-  have "Cauchy i" unfolding Cauchy_def
-  proof(rule,rule) fix e::real assume "e>0"
-    hence "e / 4 / content {a..b} > 0" using as by(auto simp add:field_simps)
-    then guess M apply-apply(subst(asm) real_arch_inv) by(erule exE conjE)+ note M=this
-    show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (i m) (i n) < e" apply(rule_tac x=M in exI,rule,rule,rule,rule)
-    proof- case goal1 have "e/4>0" using `e>0` by auto note * = i[unfolded has_integral,rule_format,OF this]
-      from *[of m] guess gm apply-by(erule conjE exE)+ note gm=this[rule_format]
-      from *[of n] guess gn apply-by(erule conjE exE)+ note gn=this[rule_format]
+  have "Cauchy i"
+    unfolding Cauchy_def
+  proof (rule, rule)
+    fix e :: real
+    assume "e>0"
+    then have "e / 4 / content {a..b} > 0"
+      using as by (auto simp add: field_simps)
+    then guess M
+      apply -
+      apply (subst(asm) real_arch_inv)
+      apply (elim exE conjE)
+      done
+    note M=this
+    show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (i m) (i n) < e"
+      apply (rule_tac x=M in exI,rule,rule,rule,rule)
+    proof -
+      case goal1
+      have "e/4>0" using `e>0` by auto
+      note * = i[unfolded has_integral,rule_format,OF this]
+      from *[of m] guess gm by (elim conjE exE) note gm=this[rule_format]
+      from *[of n] guess gn by (elim conjE exE) note gn=this[rule_format]
       from fine_division_exists[OF gauge_inter[OF gm(1) gn(1)], of a b] guess p . note p=this
-      have lem2:"\<And>s1 s2 i1 i2. norm(s2 - s1) \<le> e/2 \<Longrightarrow> norm(s1 - i1) < e / 4 \<Longrightarrow> norm(s2 - i2) < e / 4 \<Longrightarrow>norm(i1 - i2) < e"
-      proof- case goal1 have "norm (i1 - i2) \<le> norm (i1 - s1) + norm (s1 - s2) + norm (s2 - i2)"
+      have lem2: "\<And>s1 s2 i1 i2. norm(s2 - s1) \<le> e/2 \<Longrightarrow> norm (s1 - i1) < e / 4 \<Longrightarrow>
+        norm (s2 - i2) < e / 4 \<Longrightarrow> norm (i1 - i2) < e"
+      proof -
+        case goal1
+        have "norm (i1 - i2) \<le> norm (i1 - s1) + norm (s1 - s2) + norm (s2 - i2)"
           using norm_triangle_ineq[of "i1 - s1" "s1 - i2"]
-          using norm_triangle_ineq[of "s1 - s2" "s2 - i2"] by(auto simp add:algebra_simps)
-        also have "\<dots> < e" using goal1 unfolding norm_minus_commute by(auto simp add:algebra_simps)
+          using norm_triangle_ineq[of "s1 - s2" "s2 - i2"]
+          by (auto simp add: algebra_simps)
+        also have "\<dots> < e"
+          using goal1
+          unfolding norm_minus_commute
+          by (auto simp add: algebra_simps)
         finally show ?case .
       qed
-      show ?case unfolding dist_norm apply(rule lem2) defer
-        apply(rule gm(2)[OF conjI[OF p(1)]],rule_tac[2] gn(2)[OF conjI[OF p(1)]])
-        using conjunctD2[OF p(2)[unfolded fine_inter]] apply- apply assumption+ apply(rule order_trans)
-        apply(rule rsum_diff_bound[OF p(1), where e="2 / real M"])
-      proof show "2 / real M * content {a..b} \<le> e / 2" unfolding divide_inverse
-          using M as by(auto simp add:field_simps)
-        fix x assume x:"x \<in> {a..b}"
+      show ?case
+        unfolding dist_norm
+        apply (rule lem2)
+        defer
+        apply (rule gm(2)[OF conjI[OF p(1)]],rule_tac[2] gn(2)[OF conjI[OF p(1)]])
+        using conjunctD2[OF p(2)[unfolded fine_inter]]
+        apply -
+        apply assumption+
+        apply (rule order_trans)
+        apply (rule rsum_diff_bound[OF p(1), where e="2 / real M"])
+      proof
+        show "2 / real M * content {a..b} \<le> e / 2"
+          unfolding divide_inverse
+          using M as
+          by (auto simp add: field_simps)
+        fix x
+        assume x: "x \<in> {a..b}"
         have "norm (f x - g n x) + norm (f x - g m x) \<le> inverse (real n + 1) + inverse (real m + 1)"
-            using g(1)[OF x, of n] g(1)[OF x, of m] by auto
-        also have "\<dots> \<le> inverse (real M) + inverse (real M)" apply(rule add_mono)
-          apply(rule_tac[!] le_imp_inverse_le) using goal1 M by auto
-        also have "\<dots> = 2 / real M" unfolding divide_inverse by auto
+          using g(1)[OF x, of n] g(1)[OF x, of m] by auto
+        also have "\<dots> \<le> inverse (real M) + inverse (real M)"
+          apply (rule add_mono)
+          apply (rule_tac[!] le_imp_inverse_le)
+          using goal1 M
+          apply auto
+          done
+        also have "\<dots> = 2 / real M"
+          unfolding divide_inverse by auto
         finally show "norm (g n x - g m x) \<le> 2 / real M"
           using norm_triangle_le[of "g n x - f x" "f x - g m x" "2 / real M"]
-          by(auto simp add:algebra_simps simp add:norm_minus_commute)
-      qed qed qed
+          by (auto simp add: algebra_simps simp add: norm_minus_commute)
+      qed
+    qed
+  qed
   from this[unfolded convergent_eq_cauchy[symmetric]] guess s .. note s=this
 
-  show ?thesis unfolding integrable_on_def apply(rule_tac x=s in exI) unfolding has_integral
-  proof(rule,rule)
-    case goal1 hence *:"e/3 > 0" by auto
+  show ?thesis
+    unfolding integrable_on_def
+    apply (rule_tac x=s in exI)
+    unfolding has_integral
+  proof (rule, rule)
+    case goal1
+    then have *: "e/3 > 0" by auto
     from LIMSEQ_D [OF s this] guess N1 .. note N1=this
-    from goal1 as have "e / 3 / content {a..b} > 0" by(auto simp add:field_simps)
-    from real_arch_invD[OF this] guess N2 apply-by(erule exE conjE)+ note N2=this
+    from goal1 as have "e / 3 / content {a..b} > 0"
+      by (auto simp add: field_simps)
+    from real_arch_invD[OF this] guess N2 by (elim exE conjE) note N2=this
     from i[of "N1 + N2",unfolded has_integral,rule_format,OF *] guess g' .. note g'=conjunctD2[OF this,rule_format]
-    have lem:"\<And>sf sg i. norm(sf - sg) \<le> e / 3 \<Longrightarrow> norm(i - s) < e / 3 \<Longrightarrow> norm(sg - i) < e / 3 \<Longrightarrow> norm(sf - s) < e"
-    proof- case goal1 have "norm (sf - s) \<le> norm (sf - sg) + norm (sg - i) + norm (i - s)"
+    have lem: "\<And>sf sg i. norm (sf - sg) \<le> e / 3 \<Longrightarrow>
+      norm(i - s) < e / 3 \<Longrightarrow> norm (sg - i) < e / 3 \<Longrightarrow> norm (sf - s) < e"
+    proof -
+      case goal1
+      have "norm (sf - s) \<le> norm (sf - sg) + norm (sg - i) + norm (i - s)"
         using norm_triangle_ineq[of "sf - sg" "sg - s"]
-        using norm_triangle_ineq[of "sg -  i" " i - s"] by(auto simp add:algebra_simps)
-      also have "\<dots> < e" using goal1 unfolding norm_minus_commute by(auto simp add:algebra_simps)
+        using norm_triangle_ineq[of "sg -  i" " i - s"]
+        by (auto simp add: algebra_simps)
+      also have "\<dots> < e"
+        using goal1
+        unfolding norm_minus_commute
+        by (auto simp add: algebra_simps)
       finally show ?case .
     qed
-    show ?case apply(rule_tac x=g' in exI) apply(rule,rule g')
-    proof(rule,rule) fix p assume p:"p tagged_division_of {a..b} \<and> g' fine p" note * = g'(2)[OF this]
-      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - s) < e" apply-apply(rule lem[OF _ _ *])
-        apply(rule order_trans,rule rsum_diff_bound[OF p[THEN conjunct1]]) apply(rule,rule g,assumption)
-      proof- have "content {a..b} < e / 3 * (real N2)"
-          using N2 unfolding inverse_eq_divide using as by(auto simp add:field_simps)
-        hence "content {a..b} < e / 3 * (real (N1 + N2) + 1)"
-          apply-apply(rule less_le_trans,assumption) using `e>0` by auto
-        thus "inverse (real (N1 + N2) + 1) * content {a..b} \<le> e / 3"
-          unfolding inverse_eq_divide by(auto simp add:field_simps)
-        show "norm (i (N1 + N2) - s) < e / 3" by(rule N1[rule_format],auto)
-      qed qed qed qed
+    show ?case
+      apply (rule_tac x=g' in exI)
+      apply rule
+      apply (rule g')
+    proof (rule, rule)
+      fix p
+      assume p: "p tagged_division_of {a..b} \<and> g' fine p"
+      note * = g'(2)[OF this]
+      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - s) < e"
+        apply -
+        apply (rule lem[OF _ _ *])
+        apply (rule order_trans)
+        apply (rule rsum_diff_bound[OF p[THEN conjunct1]])
+        apply rule
+        apply (rule g)
+        apply assumption
+      proof -
+        have "content {a..b} < e / 3 * (real N2)"
+          using N2 unfolding inverse_eq_divide using as by (auto simp add: field_simps)
+        then have "content {a..b} < e / 3 * (real (N1 + N2) + 1)"
+          apply -
+          apply (rule less_le_trans,assumption)
+          using `e>0`
+          apply auto
+          done
+        then show "inverse (real (N1 + N2) + 1) * content {a..b} \<le> e / 3"
+          unfolding inverse_eq_divide
+          by (auto simp add: field_simps)
+        show "norm (i (N1 + N2) - s) < e / 3"
+          by (rule N1[rule_format]) auto
+      qed
+    qed
+  qed
+qed
+
 
 subsection {* Negligible sets. *}
 
-definition "negligible (s::('a::ordered_euclidean_space) set) \<equiv> (\<forall>a b. ((indicator s :: 'a\<Rightarrow>real) has_integral 0) {a..b})"
+definition "negligible (s:: 'a::ordered_euclidean_space set) \<longleftrightarrow>
+  (\<forall>a b. ((indicator s :: 'a\<Rightarrow>real) has_integral 0) {a..b})"
+
 
 subsection {* Negligibility of hyperplane. *}
 
 lemma vsum_nonzero_image_lemma:
-  assumes "finite s" "g(a) = 0"
-  "\<forall>x\<in>s. \<forall>y\<in>s. f x = f y \<and> x \<noteq> y \<longrightarrow> g(f x) = 0"
+  assumes "finite s"
+    and "g a = 0"
+    and "\<forall>x\<in>s. \<forall>y\<in>s. f x = f y \<and> x \<noteq> y \<longrightarrow> g (f x) = 0"
   shows "setsum g {f x |x. x \<in> s \<and> f x \<noteq> a} = setsum (g o f) s"
-  unfolding setsum_iterate[OF assms(1)] apply(subst setsum_iterate) defer
-  apply(rule iterate_nonzero_image_lemma) apply(rule assms monoidal_monoid)+
-  unfolding assms using neutral_add unfolding neutral_add using assms by auto
-
-lemma interval_doublesplit:  fixes a::"'a::ordered_euclidean_space" assumes "k\<in>Basis"
+  unfolding setsum_iterate[OF assms(1)]
+  apply (subst setsum_iterate)
+  defer
+  apply (rule iterate_nonzero_image_lemma)
+  apply (rule assms monoidal_monoid)+
+  unfolding assms
+  using neutral_add
+  unfolding neutral_add
+  using assms
+  apply auto
+  done
+
+lemma interval_doublesplit:
+  fixes a :: "'a::ordered_euclidean_space"
+  assumes "k \<in> Basis"
   shows "{a..b} \<inter> {x . abs(x\<bullet>k - c) \<le> (e::real)} =
-  {(\<Sum>i\<in>Basis. (if i = k then max (a\<bullet>k) (c - e) else a\<bullet>i) *\<^sub>R i) ..
-   (\<Sum>i\<in>Basis. (if i = k then min (b\<bullet>k) (c + e) else b\<bullet>i) *\<^sub>R i)}"
-proof- have *:"\<And>x c e::real. abs(x - c) \<le> e \<longleftrightarrow> x \<ge> c - e \<and> x \<le> c + e" by auto
-  have **:"\<And>s P Q. s \<inter> {x. P x \<and> Q x} = (s \<inter> {x. Q x}) \<inter> {x. P x}" by blast
-  show ?thesis unfolding * ** interval_split[OF assms] by(rule refl) qed
-
-lemma division_doublesplit: fixes a::"'a::ordered_euclidean_space" assumes "p division_of {a..b}" and k:"k\<in>Basis"
+    {(\<Sum>i\<in>Basis. (if i = k then max (a\<bullet>k) (c - e) else a\<bullet>i) *\<^sub>R i) ..
+     (\<Sum>i\<in>Basis. (if i = k then min (b\<bullet>k) (c + e) else b\<bullet>i) *\<^sub>R i)}"
+proof -
+  have *: "\<And>x c e::real. abs(x - c) \<le> e \<longleftrightarrow> x \<ge> c - e \<and> x \<le> c + e"
+    by auto
+  have **: "\<And>s P Q. s \<inter> {x. P x \<and> Q x} = (s \<inter> {x. Q x}) \<inter> {x. P x}"
+    by blast
+  show ?thesis
+    unfolding * ** interval_split[OF assms] by (rule refl)
+qed
+
+lemma division_doublesplit:
+  fixes a :: "'a::ordered_euclidean_space"
+  assumes "p division_of {a..b}"
+    and k: "k \<in> Basis"
   shows "{l \<inter> {x. abs(x\<bullet>k - c) \<le> e} |l. l \<in> p \<and> l \<inter> {x. abs(x\<bullet>k - c) \<le> e} \<noteq> {}} division_of ({a..b} \<inter> {x. abs(x\<bullet>k - c) \<le> e})"
-proof- have *:"\<And>x c. abs(x - c) \<le> e \<longleftrightarrow> x \<ge> c - e \<and> x \<le> c + e" by auto
-  have **:"\<And>p q p' q'. p division_of q \<Longrightarrow> p = p' \<Longrightarrow> q = q' \<Longrightarrow> p' division_of q'" by auto
+proof -
+  have *: "\<And>x c. abs (x - c) \<le> e \<longleftrightarrow> x \<ge> c - e \<and> x \<le> c + e"
+    by auto
+  have **: "\<And>p q p' q'. p division_of q \<Longrightarrow> p = p' \<Longrightarrow> q = q' \<Longrightarrow> p' division_of q'"
+    by auto
   note division_split(1)[OF assms, where c="c+e",unfolded interval_split[OF k]]
   note division_split(2)[OF this, where c="c-e" and k=k,OF k]
-  thus ?thesis apply(rule **) using k apply- unfolding interval_doublesplit unfolding * unfolding interval_split interval_doublesplit
-    apply(rule set_eqI) unfolding mem_Collect_eq apply rule apply(erule conjE exE)+ apply(rule_tac x=la in exI) defer
-    apply(erule conjE exE)+ apply(rule_tac x="l \<inter> {x. c + e \<ge> x \<bullet> k}" in exI) apply rule defer apply rule
-    apply(rule_tac x=l in exI) by blast+ qed
-
-lemma content_doublesplit: fixes a::"'a::ordered_euclidean_space" assumes "0 < e" and k:"k\<in>Basis"
-  obtains d where "0 < d" "content({a..b} \<inter> {x. abs(x\<bullet>k - c) \<le> d}) < e"
-proof(cases "content {a..b} = 0")
-  case True show ?thesis apply(rule that[of 1]) defer unfolding interval_doublesplit[OF k]
-    apply(rule le_less_trans[OF content_subset]) defer apply(subst True)
-    unfolding interval_doublesplit[symmetric,OF k] using assms by auto
-next case False def d \<equiv> "e / 3 / setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) (Basis - {k})"
+  then show ?thesis
+    apply (rule **)
+    using k
+    apply -
+    unfolding interval_doublesplit
+    unfolding *
+    unfolding interval_split interval_doublesplit
+    apply (rule set_eqI)
+    unfolding mem_Collect_eq
+    apply rule
+    apply (erule conjE exE)+
+    apply (rule_tac x=la in exI)
+    defer
+    apply (erule conjE exE)+
+    apply (rule_tac x="l \<inter> {x. c + e \<ge> x \<bullet> k}" in exI)
+    apply rule
+    defer
+    apply rule
+    apply (rule_tac x=l in exI)
+    apply blast+
+    done
+qed
+
+lemma content_doublesplit:
+  fixes a :: "'a::ordered_euclidean_space"
+  assumes "0 < e"
+    and k: "k \<in> Basis"
+  obtains d where "0 < d" and "content ({a..b} \<inter> {x. abs(x\<bullet>k - c) \<le> d}) < e"
+proof (cases "content {a..b} = 0")
+  case True
+  show ?thesis
+    apply (rule that[of 1])
+    defer
+    unfolding interval_doublesplit[OF k]
+    apply (rule le_less_trans[OF content_subset])
+    defer
+    apply (subst True)
+    unfolding interval_doublesplit[symmetric,OF k]
+    using assms
+    apply auto
+    done
+next
+  case False
+  def d \<equiv> "e / 3 / setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) (Basis - {k})"
   note False[unfolded content_eq_0 not_ex not_le, rule_format]
-  hence "\<And>x. x\<in>Basis \<Longrightarrow> b\<bullet>x > a\<bullet>x" by(auto simp add:not_le)
-  hence prod0:"0 < setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) (Basis - {k})" apply-apply(rule setprod_pos) by(auto simp add:field_simps)
-  hence "d > 0" unfolding d_def using assms by(auto simp add:field_simps) thus ?thesis
-  proof(rule that[of d]) have *:"Basis = insert k (Basis - {k})" using k by auto
-    have **:"{a..b} \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {} \<Longrightarrow>
-      (\<Prod>i\<in>Basis - {k}. interval_upperbound ({a..b} \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<bullet> i
-      - interval_lowerbound ({a..b} \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<bullet> i)
-      = (\<Prod>i\<in>Basis - {k}. b\<bullet>i - a\<bullet>i)" apply(rule setprod_cong,rule refl)
-      unfolding interval_doublesplit[OF k] apply(subst interval_bounds) defer apply(subst interval_bounds)
-      unfolding interval_eq_empty not_ex not_less by auto
-    show "content ({a..b} \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) < e" apply(cases) unfolding content_def apply(subst if_P,assumption,rule assms)
-      unfolding if_not_P apply(subst *) apply(subst setprod_insert) unfolding **
-      unfolding interval_doublesplit[OF k] interval_eq_empty not_ex not_less prefer 3
-      apply(subst interval_bounds) defer apply(subst interval_bounds)
+  then have "\<And>x. x \<in> Basis \<Longrightarrow> b\<bullet>x > a\<bullet>x"
+    by (auto simp add:not_le)
+  then have prod0: "0 < setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) (Basis - {k})"
+    apply -
+    apply (rule setprod_pos)
+    apply (auto simp add: field_simps)
+    done
+  then have "d > 0"
+    unfolding d_def
+    using assms
+    by (auto simp add:field_simps)
+  then show ?thesis
+  proof (rule that[of d])
+    have *: "Basis = insert k (Basis - {k})"
+      using k by auto
+    have **: "{a..b} \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {} \<Longrightarrow>
+      (\<Prod>i\<in>Basis - {k}. interval_upperbound ({a..b} \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<bullet> i -
+        interval_lowerbound ({a..b} \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<bullet> i) =
+      (\<Prod>i\<in>Basis - {k}. b\<bullet>i - a\<bullet>i)"
+      apply (rule setprod_cong)
+      apply (rule refl)
+      unfolding interval_doublesplit[OF k]
+      apply (subst interval_bounds)
+      defer
+      apply (subst interval_bounds)
+      unfolding interval_eq_empty not_ex not_less
+      apply auto
+      done
+    show "content ({a..b} \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) < e"
+      apply cases
+      unfolding content_def
+      apply (subst if_P)
+      apply assumption
+      apply (rule assms)
+      unfolding if_not_P
+      apply (subst *)
+      apply (subst setprod_insert)
+      unfolding **
+      unfolding interval_doublesplit[OF k] interval_eq_empty not_ex not_less
+      prefer 3
+      apply (subst interval_bounds)
+      defer
+      apply (subst interval_bounds)
       apply (simp_all only: k inner_setsum_left_Basis simp_thms if_P cong: bex_cong ball_cong)
     proof -
-      have "(min (b \<bullet> k) (c + d) - max (a \<bullet> k) (c - d)) \<le> 2 * d" by auto
-      also have "... < e / (\<Prod>i\<in>Basis - {k}. b \<bullet> i - a \<bullet> i)" unfolding d_def using assms prod0 by(auto simp add:field_simps)
+      have "(min (b \<bullet> k) (c + d) - max (a \<bullet> k) (c - d)) \<le> 2 * d"
+        by auto
+      also have "\<dots> < e / (\<Prod>i\<in>Basis - {k}. b \<bullet> i - a \<bullet> i)"
+        unfolding d_def
+        using assms prod0
+        by (auto simp add: field_simps)
       finally show "(min (b \<bullet> k) (c + d) - max (a \<bullet> k) (c - d)) * (\<Prod>i\<in>Basis - {k}. b \<bullet> i - a \<bullet> i) < e"
         unfolding pos_less_divide_eq[OF prod0] .
     qed auto
@@ -4626,261 +5537,707 @@
   fixes k :: "'a::ordered_euclidean_space"
   assumes k: "k \<in> Basis"
   shows "negligible {x. x\<bullet>k = c}"
-  unfolding negligible_def has_integral apply(rule,rule,rule,rule)
-proof-
-  case goal1 from content_doublesplit[OF this k,of a b c] guess d . note d=this
+  unfolding negligible_def has_integral
+  apply (rule, rule, rule, rule)
+proof -
+  case goal1
+  from content_doublesplit[OF this k,of a b c] guess d . note d=this
   let ?i = "indicator {x::'a. x\<bullet>k = c} :: 'a\<Rightarrow>real"
-  show ?case apply(rule_tac x="\<lambda>x. ball x d" in exI) apply(rule,rule gauge_ball,rule d)
-  proof(rule,rule) fix p assume p:"p tagged_division_of {a..b} \<and> (\<lambda>x. ball x d) fine p"
-    have *:"(\<Sum>(x, ka)\<in>p. content ka *\<^sub>R ?i x) = (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. abs(x\<bullet>k - c) \<le> d}) *\<^sub>R ?i x)"
-      apply(rule setsum_cong2) unfolding split_paired_all real_scaleR_def mult_cancel_right split_conv
-      apply(cases,rule disjI1,assumption,rule disjI2)
-    proof- fix x l assume as:"(x,l)\<in>p" "?i x \<noteq> 0" hence xk:"x\<bullet>k = c" unfolding indicator_def apply-by(rule ccontr,auto)
-      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,rule,rule) unfolding mem_Collect_eq
-      proof- fix y assume y:"y\<in>l" note p[THEN conjunct2,unfolded fine_def,rule_format,OF as(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]
-        thus "\<bar>y \<bullet> k - c\<bar> \<le> d" unfolding inner_simps xk by auto
-      qed auto qed
+  show ?case
+    apply (rule_tac x="\<lambda>x. ball x d" in exI)
+    apply rule
+    apply (rule gauge_ball)
+    apply (rule d)
+  proof (rule, rule)
+    fix p
+    assume p: "p tagged_division_of {a..b} \<and> (\<lambda>x. ball x d) fine p"
+    have *: "(\<Sum>(x, ka)\<in>p. content ka *\<^sub>R ?i x) =
+      (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. abs(x\<bullet>k - c) \<le> d}) *\<^sub>R ?i x)"
+      apply (rule setsum_cong2)
+      unfolding split_paired_all real_scaleR_def mult_cancel_right split_conv
+      apply cases
+      apply (rule disjI1)
+      apply assumption
+      apply (rule disjI2)
+    proof -
+      fix x l
+      assume as: "(x, l) \<in> p" "?i x \<noteq> 0"
+      then have xk: "x\<bullet>k = c"
+        unfolding indicator_def
+        apply -
+        apply (rule ccontr)
+        apply auto
+        done
+      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)
+        apply rule
+        apply rule
+        unfolding mem_Collect_eq
+      proof -
+        fix y
+        assume y: "y \<in> l"
+        note p[THEN conjunct2,unfolded fine_def,rule_format,OF as(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
     note p'= tagged_division_ofD[OF p[THEN conjunct1]] and p''=division_of_tagged_division[OF p[THEN conjunct1]]
-    show "norm ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R ?i x) - 0) < e" unfolding diff_0_right * unfolding real_scaleR_def real_norm_def
-      apply(subst abs_of_nonneg) apply(rule setsum_nonneg,rule) unfolding split_paired_all split_conv
-      apply(rule mult_nonneg_nonneg) apply(drule p'(4)) apply(erule exE)+ apply(rule_tac b=b in back_subst)
-      prefer 2 apply(subst(asm) eq_commute) apply assumption
-      apply(subst interval_doublesplit[OF k]) apply(rule content_pos_le) apply(rule indicator_pos_le)
-    proof- have "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) \<le> (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}))"
-        apply(rule setsum_mono) unfolding split_paired_all split_conv
-        apply(rule mult_right_le_one_le) apply(drule p'(4)) by(auto simp add:interval_doublesplit[OF k])
-      also have "... < e" apply(subst setsum_over_tagged_division_lemma[OF p[THEN conjunct1]])
-      proof- case goal1 have "content ({u..v} \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<le> content {u..v}"
-          unfolding interval_doublesplit[OF k] apply(rule content_subset) unfolding interval_doublesplit[symmetric,OF k] by auto
-        thus ?case unfolding goal1 unfolding interval_doublesplit[OF k]
+    show "norm ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R ?i x) - 0) < e"
+      unfolding diff_0_right *
+      unfolding real_scaleR_def real_norm_def
+      apply (subst abs_of_nonneg)
+      apply (rule setsum_nonneg)
+      apply rule
+      unfolding split_paired_all split_conv
+      apply (rule mult_nonneg_nonneg)
+      apply (drule p'(4))
+      apply (erule exE)+
+      apply(rule_tac b=b in back_subst)
+      prefer 2
+      apply (subst(asm) eq_commute)
+      apply assumption
+      apply (subst interval_doublesplit[OF k])
+      apply (rule content_pos_le)
+      apply (rule indicator_pos_le)
+    proof -
+      have "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) \<le>
+        (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}))"
+        apply (rule setsum_mono)
+        unfolding split_paired_all split_conv
+        apply (rule mult_right_le_one_le)
+        apply (drule p'(4))
+        apply (auto simp add:interval_doublesplit[OF k])
+        done
+      also have "\<dots> < e"
+        apply (subst setsum_over_tagged_division_lemma[OF p[THEN conjunct1]])
+      proof -
+        case goal1
+        have "content ({u..v} \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<le> content {u..v}"
+          unfolding interval_doublesplit[OF k]
+          apply (rule content_subset)
+          unfolding interval_doublesplit[symmetric,OF k]
+          apply auto
+          done
+        then show ?case
+          unfolding goal1
+          unfolding interval_doublesplit[OF k]
           by (blast intro: antisym)
-      next have *:"setsum content {l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} |l. l \<in> snd ` p \<and> l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}} \<ge> 0"
-          apply(rule setsum_nonneg,rule) unfolding mem_Collect_eq image_iff apply(erule exE bexE conjE)+ unfolding split_paired_all
-        proof- fix x l a b assume as:"x = l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}" "(a, b) \<in> p" "l = snd (a, b)"
-          guess u v using p'(4)[OF as(2)] apply-by(erule exE)+ note * = this
-          show "content x \<ge> 0" unfolding as snd_conv * interval_doublesplit[OF k] by(rule content_pos_le)
-        qed have **:"norm (1::real) \<le> 1" by auto note division_doublesplit[OF p'' k,unfolded interval_doublesplit[OF k]]
+      next
+        have *: "setsum content {l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} |l. l \<in> snd ` p \<and> l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}} \<ge> 0"
+          apply (rule setsum_nonneg)
+          apply rule
+          unfolding mem_Collect_eq image_iff
+          apply (erule exE bexE conjE)+
+          unfolding split_paired_all
+        proof -
+          fix x l a b
+          assume as: "x = l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}" "(a, b) \<in> p" "l = snd (a, b)"
+          guess u v using p'(4)[OF as(2)] by (elim exE) note * = this
+          show "content x \<ge> 0"
+            unfolding as snd_conv * interval_doublesplit[OF k]
+            by (rule content_pos_le)
+        qed
+        have **: "norm (1::real) \<le> 1"
+          by auto
+        note division_doublesplit[OF p'' k,unfolded interval_doublesplit[OF k]]
         note dsum_bound[OF this **,unfolded interval_doublesplit[symmetric,OF k]]
-        note this[unfolded real_scaleR_def real_norm_def mult_1_right mult_1, of c d] note le_less_trans[OF this d(2)]
-        from this[unfolded abs_of_nonneg[OF *]] show "(\<Sum>ka\<in>snd ` p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) < e"
-          apply(subst vsum_nonzero_image_lemma[of "snd ` p" content "{}", unfolded o_def,symmetric])
-          apply(rule finite_imageI p' content_empty)+ unfolding forall_in_division[OF p'']
-        proof(rule,rule,rule,rule,rule,rule,rule,erule conjE) fix m n u v
-          assume as:"{m..n} \<in> snd ` p" "{u..v} \<in> snd ` p" "{m..n} \<noteq> {u..v}"  "{m..n} \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} = {u..v} \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}"
-          have "({m..n} \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<inter> ({u..v} \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<subseteq> {m..n} \<inter> {u..v}" by blast
+        note this[unfolded real_scaleR_def real_norm_def mult_1_right mult_1, of c d]
+        note le_less_trans[OF this d(2)]
+        from this[unfolded abs_of_nonneg[OF *]]
+        show "(\<Sum>ka\<in>snd ` p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) < e"
+          apply (subst vsum_nonzero_image_lemma[of "snd ` p" content "{}", unfolded o_def,symmetric])
+          apply (rule finite_imageI p' content_empty)+
+          unfolding forall_in_division[OF p'']
+        proof (rule,rule,rule,rule,rule,rule,rule,erule conjE)
+          fix m n u v
+          assume as:
+            "{m..n} \<in> snd ` p" "{u..v} \<in> snd ` p"
+            "{m..n} \<noteq> {u..v}"
+            "{m..n} \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} = {u..v} \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}"
+          have "({m..n} \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<inter> ({u..v} \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<subseteq> {m..n} \<inter> {u..v}"
+            by blast
           note interior_mono[OF this, unfolded division_ofD(5)[OF p'' as(1-3)] interior_inter[of "{m..n}"]]
-          hence "interior ({m..n} \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = {}" unfolding as Int_absorb by auto
-          thus "content ({m..n} \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = 0" unfolding interval_doublesplit[OF k] content_eq_0_interior[symmetric] .
-        qed qed
+          then have "interior ({m..n} \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = {}"
+            unfolding as Int_absorb by auto
+          then show "content ({m..n} \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = 0"
+            unfolding interval_doublesplit[OF k] content_eq_0_interior[symmetric] .
+        qed
+      qed
       finally show "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) < e" .
-    qed qed qed
+    qed
+  qed
+qed
+
 
 subsection {* A technical lemma about "refinement" of division. *}
 
-lemma tagged_division_finer: fixes p::"(('a::ordered_euclidean_space) \<times> (('a::ordered_euclidean_space) set)) set"
-  assumes "p tagged_division_of {a..b}" "gauge d"
-  obtains q where "q tagged_division_of {a..b}" "d fine q" "\<forall>(x,k) \<in> p. k \<subseteq> d(x) \<longrightarrow> (x,k) \<in> q"
-proof-
+lemma tagged_division_finer:
+  fixes p :: "('a::ordered_euclidean_space \<times> ('a::ordered_euclidean_space set)) set"
+  assumes "p tagged_division_of {a..b}"
+    and "gauge d"
+  obtains q where "q tagged_division_of {a..b}"
+    and "d fine q"
+    and "\<forall>(x,k) \<in> p. k \<subseteq> d(x) \<longrightarrow> (x,k) \<in> q"
+proof -
   let ?P = "\<lambda>p. p tagged_partial_division_of {a..b} \<longrightarrow> gauge d \<longrightarrow>
     (\<exists>q. q tagged_division_of (\<Union>{k. \<exists>x. (x,k) \<in> p}) \<and> d fine q \<and>
-                   (\<forall>(x,k) \<in> p. k \<subseteq> d(x) \<longrightarrow> (x,k) \<in> q))"
-  { have *:"finite p" "p tagged_partial_division_of {a..b}" using assms(1) unfolding tagged_division_of_def by auto
-    presume "\<And>p. finite p \<Longrightarrow> ?P p" from this[rule_format,OF * assms(2)] guess q .. note q=this
-    thus ?thesis apply-apply(rule that[of q]) unfolding tagged_division_ofD[OF assms(1)] by auto
-  } fix p::"(('a::ordered_euclidean_space) \<times> (('a::ordered_euclidean_space) set)) set" assume as:"finite p"
-  show "?P p" apply(rule,rule) using as proof(induct p)
-    case empty show ?case apply(rule_tac x="{}" in exI) unfolding fine_def by auto
-  next case (insert xk p) guess x k using surj_pair[of xk] apply- by(erule exE)+ note xk=this
+      (\<forall>(x,k) \<in> p. k \<subseteq> d(x) \<longrightarrow> (x,k) \<in> q))"
+  {
+    have *: "finite p" "p tagged_partial_division_of {a..b}"
+      using assms(1)
+      unfolding tagged_division_of_def
+      by auto
+    presume "\<And>p. finite p \<Longrightarrow> ?P p"
+    from this[rule_format,OF * assms(2)] guess q .. note q=this
+    then show ?thesis
+      apply -
+      apply (rule that[of q])
+      unfolding tagged_division_ofD[OF assms(1)]
+      apply auto
+      done
+  }
+  fix p :: "('a::ordered_euclidean_space \<times> ('a::ordered_euclidean_space set)) set"
+  assume as: "finite p"
+  show "?P p"
+    apply rule
+    apply rule
+    using as
+  proof (induct p)
+    case empty
+    show ?case
+      apply (rule_tac x="{}" in exI)
+      unfolding fine_def
+      apply auto
+      done
+  next
+    case (insert xk p)
+    guess x k using surj_pair[of xk] by (elim exE) note xk=this
     note tagged_partial_division_subset[OF insert(4) subset_insertI]
     from insert(3)[OF this insert(5)] guess q1 .. note q1 = conjunctD3[OF this]
-    have *:"\<Union>{l. \<exists>y. (y,l) \<in> insert xk p} = k \<union> \<Union>{l. \<exists>y. (y,l) \<in> p}" unfolding xk by auto
+    have *: "\<Union>{l. \<exists>y. (y,l) \<in> insert xk p} = k \<union> \<Union>{l. \<exists>y. (y,l) \<in> p}"
+      unfolding xk by auto
     note p = tagged_partial_division_ofD[OF insert(4)]
-    from p(4)[unfolded xk, OF insertI1] guess u v apply-by(erule exE)+ note uv=this
+    from p(4)[unfolded xk, OF insertI1] guess u v by (elim exE) note uv=this
 
     have "finite {k. \<exists>x. (x, k) \<in> p}"
-      apply(rule finite_subset[of _ "snd ` p"],rule) unfolding subset_eq image_iff mem_Collect_eq
-      apply(erule exE,rule_tac x="(xa,x)" in bexI) using p by auto
-    hence int:"interior {u..v} \<inter> interior (\<Union>{k. \<exists>x. (x, k) \<in> p}) = {}"
-      apply(rule inter_interior_unions_intervals) apply(rule open_interior) apply(rule_tac[!] ballI)
-      unfolding mem_Collect_eq apply(erule_tac[!] exE) apply(drule p(4)[OF insertI2],assumption)
-      apply(rule p(5))  unfolding uv xk apply(rule insertI1,rule insertI2) apply assumption
-      using insert(2) unfolding uv xk by auto
-
-    show ?case proof(cases "{u..v} \<subseteq> d x")
-      case True thus ?thesis apply(rule_tac x="{(x,{u..v})} \<union> q1" in exI) apply rule
-        unfolding * uv apply(rule tagged_division_union,rule tagged_division_of_self)
-        apply(rule p[unfolded xk uv] insertI1)+  apply(rule q1,rule int)
-        apply(rule,rule fine_union,subst fine_def) defer apply(rule q1)
-        unfolding Ball_def split_paired_All split_conv apply(rule,rule,rule,rule)
-        apply(erule insertE) defer apply(rule UnI2) apply(drule q1(3)[rule_format]) unfolding xk uv by auto
-    next case False from fine_division_exists[OF assms(2), of u v] guess q2 . note q2=this
-      show ?thesis apply(rule_tac x="q2 \<union> q1" in exI)
-        apply rule unfolding * uv apply(rule tagged_division_union q2 q1 int fine_union)+
-        unfolding Ball_def split_paired_All split_conv apply rule apply(rule fine_union)
-        apply(rule q1 q2)+ apply(rule,rule,rule,rule) apply(erule insertE)
-        apply(rule UnI2) defer apply(drule q1(3)[rule_format])using False unfolding xk uv by auto
-    qed qed qed
+      apply (rule finite_subset[of _ "snd ` p"],rule)
+      unfolding subset_eq image_iff mem_Collect_eq
+      apply (erule exE)
+      apply (rule_tac x="(xa,x)" in bexI)
+      using p
+      apply auto
+      done
+    then have int: "interior {u..v} \<inter> interior (\<Union>{k. \<exists>x. (x, k) \<in> p}) = {}"
+      apply (rule inter_interior_unions_intervals)
+      apply (rule open_interior)
+      apply (rule_tac[!] ballI)
+      unfolding mem_Collect_eq
+      apply (erule_tac[!] exE)
+      apply (drule p(4)[OF insertI2])
+      apply assumption
+      apply (rule p(5))
+      unfolding uv xk
+      apply (rule insertI1)
+      apply (rule insertI2)
+      apply assumption
+      using insert(2)
+      unfolding uv xk
+      apply auto
+      done
+    show ?case
+    proof (cases "{u..v} \<subseteq> d x")
+      case True
+      then show ?thesis
+        apply (rule_tac x="{(x,{u..v})} \<union> q1" in exI)
+        apply rule
+        unfolding * uv
+        apply (rule tagged_division_union)
+        apply (rule tagged_division_of_self)
+        apply (rule p[unfolded xk uv] insertI1)+
+        apply (rule q1)
+        apply (rule int)
+        apply rule
+        apply (rule fine_union)
+        apply (subst fine_def)
+        defer
+        apply (rule q1)
+        unfolding Ball_def split_paired_All split_conv
+        apply rule
+        apply rule
+        apply rule
+        apply rule
+        apply (erule insertE)
+        defer
+        apply (rule UnI2)
+        apply (drule q1(3)[rule_format])
+        unfolding xk uv
+        apply auto
+        done
+    next
+      case False
+      from fine_division_exists[OF assms(2), of u v] guess q2 . note q2=this
+      show ?thesis
+        apply (rule_tac x="q2 \<union> q1" in exI)
+        apply rule
+        unfolding * uv
+        apply (rule tagged_division_union q2 q1 int fine_union)+
+        unfolding Ball_def split_paired_All split_conv
+        apply rule
+        apply (rule fine_union)
+        apply (rule q1 q2)+
+        apply rule
+        apply rule
+        apply rule
+        apply rule
+        apply (erule insertE)
+        apply (rule UnI2)
+        defer
+        apply (drule q1(3)[rule_format])
+        using False
+        unfolding xk uv
+        apply auto
+        done
+    qed
+  qed
+qed
+
 
 subsection {* Hence the main theorem about negligible sets. *}
 
-lemma finite_product_dependent: assumes "finite s" "\<And>x. x\<in>s\<Longrightarrow> finite (t x)"
-  shows "finite {(i, j) |i j. i \<in> s \<and> j \<in> t i}" using assms
-proof(induct) case (insert x s)
-  have *:"{(i, j) |i j. i \<in> insert x s \<and> j \<in> t i} = (\<lambda>y. (x,y)) ` (t x) \<union> {(i, j) |i j. i \<in> s \<and> j \<in> t i}" by auto
-  show ?case unfolding * apply(rule finite_UnI) using insert by auto qed auto
-
-lemma sum_sum_product: assumes "finite s" "\<forall>i\<in>s. finite (t i)"
-  shows "setsum (\<lambda>i. setsum (x i) (t i)::real) s = setsum (\<lambda>(i,j). x i j) {(i,j) | i j. i \<in> s \<and> j \<in> t i}" using assms
-proof(induct) case (insert a s)
-  have *:"{(i, j) |i j. i \<in> insert a s \<and> j \<in> t i} = (\<lambda>y. (a,y)) ` (t a) \<union> {(i, j) |i j. i \<in> s \<and> j \<in> t i}" by auto
-  show ?case unfolding * apply(subst setsum_Un_disjoint) unfolding setsum_insert[OF insert(1-2)]
-    prefer 4 apply(subst insert(3)) unfolding add_right_cancel
-  proof- show "setsum (x a) (t a) = (\<Sum>(xa, y)\<in>Pair a ` t a. x xa y)" apply(subst setsum_reindex) unfolding inj_on_def by auto
-    show "finite {(i, j) |i j. i \<in> s \<and> j \<in> t i}" apply(rule finite_product_dependent) using insert by auto
-  qed(insert insert, auto) qed auto
-
-lemma has_integral_negligible: fixes f::"'b::ordered_euclidean_space \<Rightarrow> 'a::real_normed_vector"
-  assumes "negligible s" "\<forall>x\<in>(t - s). f x = 0"
+lemma finite_product_dependent:
+  assumes "finite s"
+    and "\<And>x. x \<in> s \<Longrightarrow> finite (t x)"
+  shows "finite {(i, j) |i j. i \<in> s \<and> j \<in> t i}"
+  using assms
+proof induct
+  case (insert x s)
+  have *: "{(i, j) |i j. i \<in> insert x s \<and> j \<in> t i} =
+    (\<lambda>y. (x,y)) ` (t x) \<union> {(i, j) |i j. i \<in> s \<and> j \<in> t i}" by auto
+  show ?case
+    unfolding *
+    apply (rule finite_UnI)
+    using insert
+    apply auto
+    done
+qed auto
+
+lemma sum_sum_product:
+  assumes "finite s"
+    and "\<forall>i\<in>s. finite (t i)"
+  shows "setsum (\<lambda>i. setsum (x i) (t i)::real) s =
+    setsum (\<lambda>(i,j). x i j) {(i,j) | i j. i \<in> s \<and> j \<in> t i}"
+  using assms
+proof induct
+  case (insert a s)
+  have *: "{(i, j) |i j. i \<in> insert a s \<and> j \<in> t i} =
+    (\<lambda>y. (a,y)) ` (t a) \<union> {(i, j) |i j. i \<in> s \<and> j \<in> t i}" by auto
+  show ?case
+    unfolding *
+    apply (subst setsum_Un_disjoint)
+    unfolding setsum_insert[OF insert(1-2)]
+    prefer 4
+    apply (subst insert(3))
+    unfolding add_right_cancel
+  proof -
+    show "setsum (x a) (t a) = (\<Sum>(xa, y)\<in> Pair a ` t a. x xa y)"
+      apply (subst setsum_reindex)
+      unfolding inj_on_def
+      apply auto
+      done
+    show "finite {(i, j) |i j. i \<in> s \<and> j \<in> t i}"
+      apply (rule finite_product_dependent)
+      using insert
+      apply auto
+      done
+  qed (insert insert, auto)
+qed auto
+
+lemma has_integral_negligible:
+  fixes f :: "'b::ordered_euclidean_space \<Rightarrow> 'a::real_normed_vector"
+  assumes "negligible s"
+    and "\<forall>x\<in>(t - s). f x = 0"
   shows "(f has_integral 0) t"
-proof- presume P:"\<And>f::'b::ordered_euclidean_space \<Rightarrow> 'a. \<And>a b. (\<forall>x. ~(x \<in> s) \<longrightarrow> f x = 0) \<Longrightarrow> (f has_integral 0) ({a..b})"
+proof -
+  presume P: "\<And>f::'b::ordered_euclidean_space \<Rightarrow> 'a.
+    \<And>a b. \<forall>x. x \<notin> s \<longrightarrow> f x = 0 \<Longrightarrow> (f has_integral 0) {a..b}"
   let ?f = "(\<lambda>x. if x \<in> t then f x else 0)"
-  show ?thesis apply(rule_tac f="?f" in has_integral_eq) apply(rule) unfolding if_P apply(rule refl)
-    apply(subst has_integral_alt) apply(cases,subst if_P,assumption) unfolding if_not_P
-  proof- assume "\<exists>a b. t = {a..b}" then guess a b apply-by(erule exE)+ note t = this
-    show "(?f has_integral 0) t" unfolding t apply(rule P) using assms(2) unfolding t by auto
-  next show "\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b} \<longrightarrow> (\<exists>z. ((\<lambda>x. if x \<in> t then ?f x else 0) has_integral z) {a..b} \<and> norm (z - 0) < e)"
-      apply(safe,rule_tac x=1 in exI,rule) apply(rule zero_less_one,safe) apply(rule_tac x=0 in exI)
-      apply(rule,rule P) using assms(2) by auto
+  show ?thesis
+    apply (rule_tac f="?f" in has_integral_eq)
+    apply rule
+    unfolding if_P
+    apply (rule refl)
+    apply (subst has_integral_alt)
+    apply cases
+    apply (subst if_P, assumption)
+    unfolding if_not_P
+  proof -
+    assume "\<exists>a b. t = {a..b}"
+    then guess a b apply - by (erule exE)+ note t = this
+    show "(?f has_integral 0) t"
+      unfolding t
+      apply (rule P)
+      using assms(2)
+      unfolding t
+      apply auto
+      done
+  next
+    show "\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b} \<longrightarrow>
+      (\<exists>z. ((\<lambda>x. if x \<in> t then ?f x else 0) has_integral z) {a..b} \<and> norm (z - 0) < e)"
+      apply safe
+      apply (rule_tac x=1 in exI)
+      apply rule
+      apply (rule zero_less_one)
+      apply safe
+      apply (rule_tac x=0 in exI)
+      apply rule
+      apply (rule P)
+      using assms(2)
+      apply auto
+      done
   qed
-next fix f::"'b \<Rightarrow> 'a" and a b::"'b" assume assm:"\<forall>x. x \<notin> s \<longrightarrow> f x = 0"
-  show "(f has_integral 0) {a..b}" unfolding has_integral
-  proof(safe) case goal1
-    hence "\<And>n. e / 2 / ((real n+1) * (2 ^ n)) > 0"
-      apply-apply(rule divide_pos_pos) defer apply(rule mult_pos_pos) by(auto simp add:field_simps)
-    note assms(1)[unfolded negligible_def has_integral,rule_format,OF this,of a b] note allI[OF this,of "\<lambda>x. x"]
+next
+  fix f :: "'b \<Rightarrow> 'a"
+  fix a b :: 'b
+  assume assm: "\<forall>x. x \<notin> s \<longrightarrow> f x = 0"
+  show "(f has_integral 0) {a..b}"
+    unfolding has_integral
+  proof safe
+    case goal1
+    then have "\<And>n. e / 2 / ((real n+1) * (2 ^ n)) > 0"
+      apply -
+      apply (rule divide_pos_pos)
+      defer
+      apply (rule mult_pos_pos)
+      apply (auto simp add:field_simps)
+      done
+    note assms(1)[unfolded negligible_def has_integral,rule_format,OF this,of a b]
+    note allI[OF this,of "\<lambda>x. x"]
     from choice[OF this] guess d .. note d=conjunctD2[OF this[rule_format]]
-    show ?case apply(rule_tac x="\<lambda>x. d (nat \<lfloor>norm (f x)\<rfloor>) x" in exI)
-    proof safe show "gauge (\<lambda>x. d (nat \<lfloor>norm (f x)\<rfloor>) x)" using d(1) unfolding gauge_def by auto
-      fix p assume as:"p tagged_division_of {a..b}" "(\<lambda>x. d (nat \<lfloor>norm (f x)\<rfloor>) x) fine p"
+    show ?case
+      apply (rule_tac x="\<lambda>x. d (nat \<lfloor>norm (f x)\<rfloor>) x" in exI)
+    proof safe
+      show "gauge (\<lambda>x. d (nat \<lfloor>norm (f x)\<rfloor>) x)"
+        using d(1) unfolding gauge_def by auto
+      fix p
+      assume as: "p tagged_division_of {a..b}" "(\<lambda>x. d (nat \<lfloor>norm (f x)\<rfloor>) x) fine p"
       let ?goal = "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) < e"
-      { presume "p\<noteq>{} \<Longrightarrow> ?goal" thus ?goal apply(cases "p={}") using goal1 by auto  }
-      assume as':"p \<noteq> {}" from real_arch_simple[of "Sup((\<lambda>(x,k). norm(f x)) ` p)"] guess N ..
-      hence N:"\<forall>x\<in>(\<lambda>(x, k). norm (f x)) ` p. x \<le> real N" apply(subst(asm) cSup_finite_le_iff) using as as' by auto
+      {
+        presume "p \<noteq> {} \<Longrightarrow> ?goal"
+        then show ?goal
+          apply (cases "p = {}")
+          using goal1
+          apply auto
+          done
+      }
+      assume as': "p \<noteq> {}"
+      from real_arch_simple[of "Sup((\<lambda>(x,k). norm(f x)) ` p)"] guess N ..
+      then have N: "\<forall>x\<in>(\<lambda>(x, k). norm (f x)) ` p. x \<le> real N"
+        apply (subst(asm) cSup_finite_le_iff)
+        using as as'
+        apply auto
+        done
       have "\<forall>i. \<exists>q. q tagged_division_of {a..b} \<and> (d i) fine q \<and> (\<forall>(x, k)\<in>p. k \<subseteq> (d i) x \<longrightarrow> (x, k) \<in> q)"
-        apply(rule,rule tagged_division_finer[OF as(1) d(1)]) by auto
+        apply rule
+        apply (rule tagged_division_finer[OF as(1) d(1)])
+        apply auto
+        done
       from choice[OF this] guess q .. note q=conjunctD3[OF this[rule_format]]
-      have *:"\<And>i. (\<Sum>(x, k)\<in>q i. content k *\<^sub>R indicator s x) \<ge> (0::real)" apply(rule setsum_nonneg,safe)
-        unfolding real_scaleR_def apply(rule mult_nonneg_nonneg) apply(drule tagged_division_ofD(4)[OF q(1)]) by auto
-      have **:"\<And>f g s t. finite s \<Longrightarrow> finite t \<Longrightarrow> (\<forall>(x,y) \<in> t. (0::real) \<le> g(x,y)) \<Longrightarrow> (\<forall>y\<in>s. \<exists>x. (x,y) \<in> t \<and> f(y) \<le> g(x,y)) \<Longrightarrow> setsum f s \<le> setsum g t"
-      proof- case goal1 thus ?case apply-apply(rule setsum_le_included[of s t g snd f]) prefer 4
-          apply safe apply(erule_tac x=x in ballE) apply(erule exE) apply(rule_tac x="(xa,x)" in bexI) by auto qed
+      have *: "\<And>i. (\<Sum>(x, k)\<in>q i. content k *\<^sub>R indicator s x) \<ge> (0::real)"
+        apply (rule setsum_nonneg)
+        apply safe
+        unfolding real_scaleR_def
+        apply (rule mult_nonneg_nonneg)
+        apply (drule tagged_division_ofD(4)[OF q(1)])
+        apply auto
+        done
+      have **: "\<And>f g s t. finite s \<Longrightarrow> finite t \<Longrightarrow> (\<forall>(x,y) \<in> t. (0::real) \<le> g(x,y)) \<Longrightarrow>
+        (\<forall>y\<in>s. \<exists>x. (x,y) \<in> t \<and> f(y) \<le> g(x,y)) \<Longrightarrow> setsum f s \<le> setsum g t"
+      proof -
+        case goal1
+        then show ?case
+          apply -
+          apply (rule setsum_le_included[of s t g snd f])
+          prefer 4
+          apply safe
+          apply (erule_tac x=x in ballE)
+          apply (erule exE)
+          apply (rule_tac x="(xa,x)" in bexI)
+          apply auto  
+          done
+      qed
       have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) \<le> setsum (\<lambda>i. (real i + 1) *
-                     norm(setsum (\<lambda>(x,k). content k *\<^sub>R indicator s x :: real) (q i))) {0..N+1}"
+        norm (setsum (\<lambda>(x,k). content k *\<^sub>R indicator s x :: real) (q i))) {0..N+1}"
         unfolding real_norm_def setsum_right_distrib abs_of_nonneg[OF *] diff_0_right
-        apply(rule order_trans,rule norm_setsum) apply(subst sum_sum_product) prefer 3
-      proof(rule **,safe) show "finite {(i, j) |i j. i \<in> {0..N + 1} \<and> j \<in> q i}" apply(rule finite_product_dependent) using q by auto
-        fix i a b assume as'':"(a,b) \<in> q i" show "0 \<le> (real i + 1) * (content b *\<^sub>R indicator s a)"
-          unfolding real_scaleR_def apply(rule mult_nonneg_nonneg) defer apply(rule mult_nonneg_nonneg)
-          using tagged_division_ofD(4)[OF q(1) as''] by auto
-      next fix i::nat show "finite (q i)" using q by auto
-      next fix x k assume xk:"(x,k) \<in> p" def n \<equiv> "nat \<lfloor>norm (f x)\<rfloor>"
-        have *:"norm (f x) \<in> (\<lambda>(x, k). norm (f x)) ` p" using xk by auto
-        have nfx:"real n \<le> norm(f x)" "norm(f x) \<le> real n + 1" unfolding n_def by auto
-        hence "n \<in> {0..N + 1}" using N[rule_format,OF *] by auto
-        moreover  note as(2)[unfolded fine_def,rule_format,OF xk,unfolded split_conv]
-        note q(3)[rule_format,OF xk,unfolded split_conv,rule_format,OF this] note this[unfolded n_def[symmetric]]
-        moreover have "norm (content k *\<^sub>R f x) \<le> (real n + 1) * (content k * indicator s x)"
-        proof(cases "x\<in>s") case False thus ?thesis using assm by auto
-        next case True have *:"content k \<ge> 0" using tagged_division_ofD(4)[OF as(1) xk] by auto
-          moreover have "content k * norm (f x) \<le> content k * (real n + 1)" apply(rule mult_mono) using nfx * by auto
-          ultimately show ?thesis unfolding abs_mult using nfx True by(auto simp add:field_simps)
-        qed ultimately show "\<exists>y. (y, x, k) \<in> {(i, j) |i j. i \<in> {0..N + 1} \<and> j \<in> q i} \<and> norm (content k *\<^sub>R f x) \<le> (real y + 1) * (content k *\<^sub>R indicator s x)"
-          apply(rule_tac x=n in exI,safe) apply(rule_tac x=n in exI,rule_tac x="(x,k)" in exI,safe) by auto
-      qed(insert as, auto)
-      also have "... \<le> setsum (\<lambda>i. e / 2 / 2 ^ i) {0..N+1}" apply(rule setsum_mono)
-      proof- case goal1 thus ?case apply(subst mult_commute, subst pos_le_divide_eq[symmetric])
-          using d(2)[rule_format,of "q i" i] using q[rule_format] by(auto simp add:field_simps)
-      qed also have "... < e * inverse 2 * 2" unfolding divide_inverse setsum_right_distrib[symmetric]
-        apply(rule mult_strict_left_mono) unfolding power_inverse atLeastLessThanSuc_atLeastAtMost[symmetric]
-        apply(subst sumr_geometric) using goal1 by auto
-      finally show "?goal" by auto qed qed qed
-
-lemma has_integral_spike: fixes f::"'b::ordered_euclidean_space \<Rightarrow> 'a::real_normed_vector"
-  assumes "negligible s" "(\<forall>x\<in>(t - s). g x = f x)" "(f has_integral y) t"
+        apply (rule order_trans)
+        apply (rule norm_setsum)
+        apply (subst sum_sum_product)
+        prefer 3
+      proof (rule **, safe)
+        show "finite {(i, j) |i j. i \<in> {0..N + 1} \<and> j \<in> q i}"
+          apply (rule finite_product_dependent)
+          using q
+          apply auto
+          done
+        fix i a b
+        assume as'': "(a, b) \<in> q i"
+        show "0 \<le> (real i + 1) * (content b *\<^sub>R indicator s a)"
+          unfolding real_scaleR_def
+          apply (rule mult_nonneg_nonneg)
+          defer
+          apply (rule mult_nonneg_nonneg)
+          using tagged_division_ofD(4)[OF q(1) as'']
+          apply auto
+          done
+      next
+        fix i :: nat
+        show "finite (q i)"
+          using q by auto
+      next
+        fix x k
+        assume xk: "(x, k) \<in> p"
+        def n \<equiv> "nat \<lfloor>norm (f x)\<rfloor>"
+        have *: "norm (f x) \<in> (\<lambda>(x, k). norm (f x)) ` p"
+          using xk by auto
+        have nfx: "real n \<le> norm (f x)" "norm (f x) \<le> real n + 1"
+          unfolding n_def by auto
+        then have "n \<in> {0..N + 1}"
+          using N[rule_format,OF *] by auto
+        moreover
+        note as(2)[unfolded fine_def,rule_format,OF xk,unfolded split_conv]
+        note q(3)[rule_format,OF xk,unfolded split_conv,rule_format,OF this]
+        note this[unfolded n_def[symmetric]]
+        moreover
+        have "norm (content k *\<^sub>R f x) \<le> (real n + 1) * (content k * indicator s x)"
+        proof (cases "x \<in> s")
+          case False
+          then show ?thesis
+            using assm by auto
+        next
+          case True
+          have *: "content k \<ge> 0"
+            using tagged_division_ofD(4)[OF as(1) xk] by auto
+          moreover
+          have "content k * norm (f x) \<le> content k * (real n + 1)"
+            apply (rule mult_mono)
+            using nfx *
+            apply auto
+            done
+          ultimately
+          show ?thesis
+            unfolding abs_mult
+            using nfx True
+            by (auto simp add: field_simps)
+        qed
+        ultimately show "\<exists>y. (y, x, k) \<in> {(i, j) |i j. i \<in> {0..N + 1} \<and> j \<in> q i} \<and> norm (content k *\<^sub>R f x) \<le>
+          (real y + 1) * (content k *\<^sub>R indicator s x)"
+          apply (rule_tac x=n in exI)
+          apply safe
+          apply (rule_tac x=n in exI)
+          apply (rule_tac x="(x,k)" in exI)
+          apply safe
+          apply auto
+          done
+      qed (insert as, auto)
+      also have "\<dots> \<le> setsum (\<lambda>i. e / 2 / 2 ^ i) {0..N+1}"
+        apply (rule setsum_mono)
+      proof -
+        case goal1
+        then show ?case
+          apply (subst mult_commute, subst pos_le_divide_eq[symmetric])
+          using d(2)[rule_format,of "q i" i]
+          using q[rule_format]
+          apply (auto simp add: field_simps)
+          done
+      qed
+      also have "\<dots> < e * inverse 2 * 2"
+        unfolding divide_inverse setsum_right_distrib[symmetric]
+        apply (rule mult_strict_left_mono)
+        unfolding power_inverse atLeastLessThanSuc_atLeastAtMost[symmetric]
+        apply (subst sumr_geometric)
+        using goal1
+        apply auto
+        done
+      finally show "?goal" by auto
+    qed
+  qed
+qed
+
+lemma has_integral_spike:
+  fixes f :: "'b::ordered_euclidean_space \<Rightarrow> 'a::real_normed_vector"
+  assumes "negligible s"
+    and "(\<forall>x\<in>(t - s). g x = f x)"
+    and "(f has_integral y) t"
   shows "(g has_integral y) t"
-proof- { fix a b::"'b" and f g ::"'b \<Rightarrow> 'a" and y::'a
-    assume as:"\<forall>x \<in> {a..b} - s. g x = f x" "(f has_integral y) {a..b}"
-    have "((\<lambda>x. f x + (g x - f x)) has_integral (y + 0)) {a..b}" apply(rule has_integral_add[OF as(2)])
-      apply(rule has_integral_negligible[OF assms(1)]) using as by auto
-    hence "(g has_integral y) {a..b}" by auto } note * = this
-  show ?thesis apply(subst has_integral_alt) using assms(2-) apply-apply(rule cond_cases,safe)
-    apply(rule *, assumption+) apply(subst(asm) has_integral_alt) unfolding if_not_P
-    apply(erule_tac x=e in allE,safe,rule_tac x=B in exI,safe) apply(erule_tac x=a in allE,erule_tac x=b in allE,safe)
-    apply(rule_tac x=z in exI,safe) apply(rule *[where fa2="\<lambda>x. if x\<in>t then f x else 0"]) by auto qed
+proof -
+  {
+    fix a b :: 'b
+    fix f g :: "'b \<Rightarrow> 'a"
+    fix y :: 'a
+    assume as: "\<forall>x \<in> {a..b} - s. g x = f x" "(f has_integral y) {a..b}"
+    have "((\<lambda>x. f x + (g x - f x)) has_integral (y + 0)) {a..b}"
+      apply (rule has_integral_add[OF as(2)])
+      apply (rule has_integral_negligible[OF assms(1)])
+      using as
+      apply auto
+      done
+    then have "(g has_integral y) {a..b}"
+      by auto
+  } note * = this
+  show ?thesis
+    apply (subst has_integral_alt)
+    using assms(2-)
+    apply -
+    apply (rule cond_cases)
+    apply safe
+    apply (rule *)
+    apply assumption+
+    apply (subst(asm) has_integral_alt)
+    unfolding if_not_P
+    apply (erule_tac x=e in allE)
+    apply safe
+    apply (rule_tac x=B in exI)
+    apply safe
+    apply (erule_tac x=a in allE)
+    apply (erule_tac x=b in allE)
+    apply safe
+    apply (rule_tac x=z in exI)
+    apply safe
+    apply (rule *[where fa2="\<lambda>x. if x\<in>t then f x else 0"])
+    apply auto
+    done
+qed
 
 lemma has_integral_spike_eq:
-  assumes "negligible s" "\<forall>x\<in>(t - s). g x = f x"
+  assumes "negligible s"
+    and "\<forall>x\<in>(t - s). g x = f x"
   shows "((f has_integral y) t \<longleftrightarrow> (g has_integral y) t)"
-  apply rule apply(rule_tac[!] has_integral_spike[OF assms(1)]) using assms(2) by auto
-
-lemma integrable_spike: assumes "negligible s" "\<forall>x\<in>(t - s). g x = f x" "f integrable_on t"
+  apply rule
+  apply (rule_tac[!] has_integral_spike[OF assms(1)])
+  using assms(2)
+  apply auto
+  done
+
+lemma integrable_spike:
+  assumes "negligible s"
+    and "\<forall>x\<in>(t - s). g x = f x"
+    and "f integrable_on t"
   shows "g integrable_on  t"
-  using assms unfolding integrable_on_def apply-apply(erule exE)
-  apply(rule,rule has_integral_spike) by fastforce+
-
-lemma integral_spike: assumes "negligible s" "\<forall>x\<in>(t - s). g x = f x"
+  using assms
+  unfolding integrable_on_def
+  apply -
+  apply (erule exE)
+  apply rule
+  apply (rule has_integral_spike)
+  apply fastforce+
+  done
+
+lemma integral_spike:
+  assumes "negligible s"
+    and "\<forall>x\<in>(t - s). g x = f x"
   shows "integral t f = integral t g"
-  unfolding integral_def using has_integral_spike_eq[OF assms] by auto
+  unfolding integral_def
+  using has_integral_spike_eq[OF assms]
+  by auto
+
 
 subsection {* Some other trivialities about negligible sets. *}
 
-lemma negligible_subset[intro]: assumes "negligible s" "t \<subseteq> s" shows "negligible t" unfolding negligible_def
-proof(safe) case goal1 show ?case using assms(1)[unfolded negligible_def,rule_format,of a b]
-    apply-apply(rule has_integral_spike[OF assms(1)]) defer apply assumption
-    using assms(2) unfolding indicator_def by auto qed
-
-lemma negligible_diff[intro?]: assumes "negligible s" shows "negligible(s - t)" using assms by auto
-
-lemma negligible_inter: assumes "negligible s \<or> negligible t" shows "negligible(s \<inter> t)" using assms by auto
-
-lemma negligible_union: assumes "negligible s" "negligible t" shows "negligible (s \<union> t)" unfolding negligible_def
-proof safe case goal1 note assm = assms[unfolded negligible_def,rule_format,of a b]
-  thus ?case apply(subst has_integral_spike_eq[OF assms(2)])
-    defer apply assumption unfolding indicator_def by auto qed
-
-lemma negligible_union_eq[simp]: "negligible (s \<union> t) \<longleftrightarrow> (negligible s \<and> negligible t)"
+lemma negligible_subset[intro]:
+  assumes "negligible s"
+    and "t \<subseteq> s"
+  shows "negligible t"
+  unfolding negligible_def
+proof safe
+  case goal1
+  show ?case
+    using assms(1)[unfolded negligible_def,rule_format,of a b]
+    apply -
+    apply (rule has_integral_spike[OF assms(1)])
+    defer
+    apply assumption
+    using assms(2)
+    unfolding indicator_def
+    apply auto
+    done
+qed
+
+lemma negligible_diff[intro?]:
+  assumes "negligible s"
+  shows "negligible (s - t)"
+  using assms by auto
+
+lemma negligible_inter:
+  assumes "negligible s \<or> negligible t"
+  shows "negligible (s \<inter> t)"
+  using assms by auto
+
+lemma negligible_union:
+  assumes "negligible s"
+    and "negligible t"
+  shows "negligible (s \<union> t)"
+  unfolding negligible_def
+proof safe
+  case goal1
+  note assm = assms[unfolded negligible_def,rule_format,of a b]
+  then show ?case
+    apply (subst has_integral_spike_eq[OF assms(2)])
+    defer
+    apply assumption
+    unfolding indicator_def
+    apply auto
+    done
+qed
+
+lemma negligible_union_eq[simp]: "negligible (s \<union> t) \<longleftrightarrow> negligible s \<and> negligible t"
   using negligible_union by auto
 
-lemma negligible_sing[intro]: "negligible {a::_::ordered_euclidean_space}"
+lemma negligible_sing[intro]: "negligible {a::'a::ordered_euclidean_space}"
   using negligible_standard_hyperplane[OF SOME_Basis, of "a \<bullet> (SOME i. i \<in> Basis)"] by auto
 
-lemma negligible_insert[simp]: "negligible(insert a s) \<longleftrightarrow> negligible s"
-  apply(subst insert_is_Un) unfolding negligible_union_eq by auto
-
-lemma negligible_empty[intro]: "negligible {}" by auto
-
-lemma negligible_finite[intro]: assumes "finite s" shows "negligible s"
-  using assms apply(induct s) by auto
-
-lemma negligible_unions[intro]: assumes "finite s" "\<forall>t\<in>s. negligible t" shows "negligible(\<Union>s)"
-  using assms by(induct,auto)
-
-lemma negligible:  "negligible s \<longleftrightarrow> (\<forall>t::('a::ordered_euclidean_space) set. ((indicator s::'a\<Rightarrow>real) has_integral 0) t)"
-  apply safe defer apply(subst negligible_def)
+lemma negligible_insert[simp]: "negligible (insert a s) \<longleftrightarrow> negligible s"
+  apply (subst insert_is_Un)
+  unfolding negligible_union_eq
+  apply auto
+  done
+
+lemma negligible_empty[intro]: "negligible {}"
+  by auto
+
+lemma negligible_finite[intro]:
+  assumes "finite s"
+  shows "negligible s"
+  using assms by (induct s) auto
+
+lemma negligible_unions[intro]:
+  assumes "finite s"
+    and "\<forall>t\<in>s. negligible t"
+  shows "negligible(\<Union>s)"
+  using assms by induct auto
+
+lemma negligible:
+  "negligible s \<longleftrightarrow> (\<forall>t::('a::ordered_euclidean_space) set. ((indicator s::'a\<Rightarrow>real) has_integral 0) t)"
+  apply safe
+  defer
+  apply (subst negligible_def)
 proof -
-  fix t::"'a set" assume as:"negligible s"
-  have *:"(\<lambda>x. if x \<in> s \<inter> t then 1 else 0) = (\<lambda>x. if x\<in>t then if x\<in>s then 1 else 0 else 0)"
+  fix t :: "'a set"
+  assume as: "negligible s"
+  have *: "(\<lambda>x. if x \<in> s \<inter> t then 1 else 0) = (\<lambda>x. if x\<in>t then if x\<in>s then 1 else 0 else 0)"
     by auto
   show "((indicator s::'a\<Rightarrow>real) has_integral 0) t"
-    apply(subst has_integral_alt)
-    apply(cases,subst if_P,assumption)
+    apply (subst has_integral_alt)
+    apply cases
+    apply (subst if_P,assumption)
     unfolding if_not_P
-    apply(safe,rule as[unfolded negligible_def,rule_format])
-    apply(rule_tac x=1 in exI)
-    apply(safe,rule zero_less_one)
-    apply(rule_tac x=0 in exI)
+    apply safe
+    apply (rule as[unfolded negligible_def,rule_format])
+    apply (rule_tac x=1 in exI)
+    apply safe
+    apply (rule zero_less_one)
+    apply (rule_tac x=0 in exI)
     using negligible_subset[OF as,of "s \<inter> t"]
     unfolding negligible_def indicator_def [abs_def]
     unfolding *
@@ -4888,63 +6245,114 @@
     done
 qed auto
 
+
 subsection {* Finite case of the spike theorem is quite commonly needed. *}
 
-lemma has_integral_spike_finite: assumes "finite s" "\<forall>x\<in>t-s. g x = f x"
-  "(f has_integral y) t" shows "(g has_integral y) t"
-  apply(rule has_integral_spike) using assms by auto
-
-lemma has_integral_spike_finite_eq: assumes "finite s" "\<forall>x\<in>t-s. g x = f x"
+lemma has_integral_spike_finite:
+  assumes "finite s"
+    and "\<forall>x\<in>t-s. g x = f x"
+    and "(f has_integral y) t"
+  shows "(g has_integral y) t"
+  apply (rule has_integral_spike)
+  using assms
+  apply auto
+  done
+
+lemma has_integral_spike_finite_eq:
+  assumes "finite s"
+    and "\<forall>x\<in>t-s. g x = f x"
   shows "((f has_integral y) t \<longleftrightarrow> (g has_integral y) t)"
-  apply rule apply(rule_tac[!] has_integral_spike_finite) using assms by auto
+  apply rule
+  apply (rule_tac[!] has_integral_spike_finite)
+  using assms
+  apply auto
+  done
 
 lemma integrable_spike_finite:
-  assumes "finite s" "\<forall>x\<in>t-s. g x = f x" "f integrable_on t" shows "g integrable_on  t"
-  using assms unfolding integrable_on_def apply safe apply(rule_tac x=y in exI)
-  apply(rule has_integral_spike_finite) by auto
+  assumes "finite s"
+    and "\<forall>x\<in>t-s. g x = f x"
+    and "f integrable_on t"
+  shows "g integrable_on  t"
+  using assms
+  unfolding integrable_on_def
+  apply safe
+  apply (rule_tac x=y in exI)
+  apply (rule has_integral_spike_finite)
+  apply auto
+  done
+
 
 subsection {* In particular, the boundary of an interval is negligible. *}
 
 lemma negligible_frontier_interval: "negligible({a::'a::ordered_euclidean_space..b} - {a<..<b})"
-proof-
+proof -
   let ?A = "\<Union>((\<lambda>k. {x. x\<bullet>k = a\<bullet>k} \<union> {x::'a. x\<bullet>k = b\<bullet>k}) ` Basis)"
   have "{a..b} - {a<..<b} \<subseteq> ?A"
     apply rule unfolding Diff_iff mem_interval
     apply simp
     apply(erule conjE bexE)+
     apply(rule_tac x=i in bexI)
-    by auto
-  thus ?thesis
-    apply-
-    apply(rule negligible_subset[of ?A])
-    apply(rule negligible_unions[OF finite_imageI])
-    by auto
+    apply auto
+    done
+  then show ?thesis
+    apply -
+    apply (rule negligible_subset[of ?A])
+    apply (rule negligible_unions[OF finite_imageI])
+    apply auto
+    done
 qed
 
 lemma has_integral_spike_interior:
-  assumes "\<forall>x\<in>{a<..<b}. g x = f x" "(f has_integral y) ({a..b})" shows "(g has_integral y) ({a..b})"
-  apply(rule has_integral_spike[OF negligible_frontier_interval _ assms(2)]) using assms(1) by auto
+  assumes "\<forall>x\<in>{a<..<b}. g x = f x"
+    and "(f has_integral y) ({a..b})"
+  shows "(g has_integral y) {a..b}"
+  apply (rule has_integral_spike[OF negligible_frontier_interval _ assms(2)])
+  using assms(1)
+  apply auto
+  done
 
 lemma has_integral_spike_interior_eq:
-  assumes "\<forall>x\<in>{a<..<b}. g x = f x" shows "((f has_integral y) ({a..b}) \<longleftrightarrow> (g has_integral y) ({a..b}))"
-  apply rule apply(rule_tac[!] has_integral_spike_interior) using assms by auto
-
-lemma integrable_spike_interior: assumes "\<forall>x\<in>{a<..<b}. g x = f x" "f integrable_on {a..b}" shows "g integrable_on {a..b}"
-  using  assms unfolding integrable_on_def using has_integral_spike_interior[OF assms(1)] by auto
+  assumes "\<forall>x\<in>{a<..<b}. g x = f x"
+  shows "(f has_integral y) {a..b} \<longleftrightarrow> (g has_integral y) {a..b}"
+  apply rule
+  apply (rule_tac[!] has_integral_spike_interior)
+  using assms
+  apply auto
+  done
+
+lemma integrable_spike_interior:
+  assumes "\<forall>x\<in>{a<..<b}. g x = f x"
+    and "f integrable_on {a..b}"
+  shows "g integrable_on {a..b}"
+  using assms
+  unfolding integrable_on_def
+  using has_integral_spike_interior[OF assms(1)]
+  by auto
+
 
 subsection {* Integrability of continuous functions. *}
 
 lemma neutral_and[simp]: "neutral op \<and> = True"
-  unfolding neutral_def apply(rule some_equality) by auto
-
-lemma monoidal_and[intro]: "monoidal op \<and>" unfolding monoidal_def by auto
-
-lemma iterate_and[simp]: assumes "finite s" shows "(iterate op \<and>) s p \<longleftrightarrow> (\<forall>x\<in>s. p x)" using assms
-apply induct unfolding iterate_insert[OF monoidal_and] by auto
-
-lemma operative_division_and: assumes "operative op \<and> P" "d division_of {a..b}"
+  unfolding neutral_def by (rule some_equality) auto
+
+lemma monoidal_and[intro]: "monoidal op \<and>"
+  unfolding monoidal_def by auto
+
+lemma iterate_and[simp]:
+  assumes "finite s"
+  shows "(iterate op \<and>) s p \<longleftrightarrow> (\<forall>x\<in>s. p x)"
+  using assms
+  apply induct
+  unfolding iterate_insert[OF monoidal_and]
+  apply auto
+  done
+
+lemma operative_division_and:
+  assumes "operative op \<and> P"
+    and "d division_of {a..b}"
   shows "(\<forall>i\<in>d. P i) \<longleftrightarrow> P {a..b}"
-  using operative_division[OF monoidal_and assms] division_of_finite[OF assms(2)] by auto
+  using operative_division[OF monoidal_and assms] division_of_finite[OF assms(2)]
+  by auto
 
 lemma operative_approximable: assumes "0 \<le> e" fixes f::"'b::ordered_euclidean_space \<Rightarrow> 'a::banach"
   shows "operative op \<and> (\<lambda>i. \<exists>g. (\<forall>x\<in>i. norm (f x - g (x::'b)) \<le> e) \<and> g integrable_on i)" unfolding operative_def neutral_and