# HG changeset patch
# User wenzelm
# Date 1379159997 -7200
# Node ID ab5d01b69a07bf9e9177dfbd1a8cbd748be1df1a
# Parent  e68732cd842e024e4a63730a33608f970332b138
tuned proofs;

diff -r e68732cd842e -r ab5d01b69a07 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Sep 13 23:52:01 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sat Sep 14 13:59:57 2013 +0200
@@ -8287,386 +8287,953 @@
   done
 
 lemma indefinite_integral_continuous_left:
-  fixes f::"real \<Rightarrow> 'a::banach"
-  assumes "f integrable_on {a..b}" "a < c" "c \<le> b" "0 < e"
-  obtains d where "0 < d" "\<forall>t. c - d < t \<and> t \<le> c \<longrightarrow> norm(integral {a..c} f - integral {a..t} f) < e"
-proof- have "\<exists>w>0. \<forall>t. c - w < t \<and> t < c \<longrightarrow> norm(f c) * norm(c - t) < e / 3"
-  proof(cases "f c = 0") case False hence "0 < e / 3 / norm (f c)"
-      apply-apply(rule divide_pos_pos) using `e>0` by auto
-    thus ?thesis apply-apply(rule,rule,assumption,safe)
-    proof- fix t assume as:"t < c" and "c - e / 3 / norm (f c) < t"
-      hence "c - t < e / 3 / norm (f c)" by auto
-      hence "norm (c - t) < e / 3 / norm (f c)" using as by auto
-      thus "norm (f c) * norm (c - t) < e / 3" using False apply-
-        apply(subst mult_commute) apply(subst pos_less_divide_eq[symmetric]) by auto
-    qed next case True show ?thesis apply(rule_tac x=1 in exI) unfolding True using `e>0` by auto
-  qed then guess w .. note w = conjunctD2[OF this,rule_format]
-
-  have *:"e / 3 > 0" using assms by auto
-  have "f integrable_on {a..c}" apply(rule integrable_subinterval[OF assms(1)]) using assms(2-3) by auto
+  fixes f:: "real \<Rightarrow> 'a::banach"
+  assumes "f integrable_on {a..b}"
+    and "a < c"
+    and "c \<le> b"
+    and "e > 0"
+  obtains d where "d > 0"
+    and "\<forall>t. c - d < t \<and> t \<le> c \<longrightarrow> norm (integral {a..c} f - integral {a..t} f) < e"
+proof -
+  have "\<exists>w>0. \<forall>t. c - w < t \<and> t < c \<longrightarrow> norm (f c) * norm(c - t) < e / 3"
+  proof (cases "f c = 0")
+    case False
+    then have "0 < e / 3 / norm (f c)"
+      apply -
+      apply (rule divide_pos_pos)
+      using `e>0`
+      apply auto
+      done
+    then show ?thesis
+      apply -
+      apply rule
+      apply rule
+      apply assumption
+      apply safe
+    proof -
+      fix t
+      assume as: "t < c" and "c - e / 3 / norm (f c) < t"
+      then have "c - t < e / 3 / norm (f c)"
+        by auto
+      then have "norm (c - t) < e / 3 / norm (f c)"
+        using as by auto
+      then show "norm (f c) * norm (c - t) < e / 3"
+        using False
+        apply -
+        apply (subst mult_commute)
+        apply (subst pos_less_divide_eq[symmetric])
+        apply auto
+        done
+    qed
+  next
+    case True
+    show ?thesis
+      apply (rule_tac x=1 in exI)
+      unfolding True
+      using `e > 0`
+      apply auto
+      done
+  qed
+  then guess w .. note w = conjunctD2[OF this,rule_format]
+
+  have *: "e / 3 > 0"
+    using assms by auto
+  have "f integrable_on {a..c}"
+    apply (rule integrable_subinterval[OF assms(1)])
+    using assms(2-3)
+    apply auto
+    done
   from integrable_integral[OF this,unfolded has_integral,rule_format,OF *] guess d1 ..
-  note d1 = conjunctD2[OF this,rule_format] def d \<equiv> "\<lambda>x. ball x w \<inter> d1 x"
-  have "gauge d" unfolding d_def using w(1) d1 by auto
-  note this[unfolded gauge_def,rule_format,of c] note conjunctD2[OF this]
-  from this(2)[unfolded open_contains_ball,rule_format,OF this(1)] guess k .. note k=conjunctD2[OF this]
-
-  let ?d = "min k (c - a)/2" show ?thesis apply(rule that[of ?d])
-  proof safe
-    show "?d > 0" using k(1) using assms(2) by auto
-    fix t assume as:"c - ?d < t" "t \<le> c"
+  note d1 = conjunctD2[OF this,rule_format]
+  def d \<equiv> "\<lambda>x. ball x w \<inter> d1 x"
+  have "gauge d"
+    unfolding d_def using w(1) d1 by auto
+  note this[unfolded gauge_def,rule_format,of c]
+  note conjunctD2[OF this]
+  from this(2)[unfolded open_contains_ball,rule_format,OF this(1)] guess k ..
+  note k=conjunctD2[OF this]
+
+  let ?d = "min k (c - a) / 2"
+  show ?thesis
+    apply (rule that[of ?d])
+    apply safe
+  proof -
+    show "?d > 0"
+      using k(1) using assms(2) by auto
+    fix t
+    assume as: "c - ?d < t" "t \<le> c"
     let ?thesis = "norm (integral {a..c} f - integral {a..t} f) < e"
-    { presume *:"t < c \<Longrightarrow> ?thesis"
-      show ?thesis apply(cases "t = c") defer apply(rule *)
-        apply(subst less_le) using `e>0` as(2) by auto }
+    {
+      presume *: "t < c \<Longrightarrow> ?thesis"
+      show ?thesis
+        apply (cases "t = c")
+        defer
+        apply (rule *)
+        apply (subst less_le)
+        using `e > 0` as(2)
+        apply auto
+        done
+    }
     assume "t < c"
 
-    have "f integrable_on {a..t}" apply(rule integrable_subinterval[OF assms(1)]) using assms(2-3) as(2) by auto
+    have "f integrable_on {a..t}"
+      apply (rule integrable_subinterval[OF assms(1)])
+      using assms(2-3) as(2)
+      apply auto
+      done
     from integrable_integral[OF this,unfolded has_integral,rule_format,OF *] guess d2 ..
     note d2 = conjunctD2[OF this,rule_format]
     def d3 \<equiv> "\<lambda>x. if x \<le> t then d1 x \<inter> d2 x else d1 x"
-    have "gauge d3" using d2(1) d1(1) unfolding d3_def gauge_def by auto
+    have "gauge d3"
+      using d2(1) d1(1) unfolding d3_def gauge_def by auto
     from fine_division_exists[OF this, of a t] guess p . note p=this
     note p'=tagged_division_ofD[OF this(1)]
-    have pt:"\<forall>(x,k)\<in>p. x \<le> t" proof safe case goal1 from p'(2,3)[OF this] show ?case by auto qed
-    with p(2) have "d2 fine p" unfolding fine_def d3_def apply safe apply(erule_tac x="(a,b)" in ballE)+ by auto
+    have pt: "\<forall>(x,k)\<in>p. x \<le> t"
+    proof safe
+      case goal1
+      from p'(2,3)[OF this] show ?case
+        by auto
+    qed
+    with p(2) have "d2 fine p"
+      unfolding fine_def d3_def
+      apply safe
+      apply (erule_tac x="(a,b)" in ballE)+
+      apply auto
+      done
     note d2_fin = d2(2)[OF conjI[OF p(1) this]]
 
-    have *:"{a..c} \<inter> {x. x \<bullet> 1 \<le> t} = {a..t}" "{a..c} \<inter> {x. x \<bullet> 1 \<ge> t} = {t..c}"
-      using assms(2-3) as by(auto simp add:field_simps)
-    have "p \<union> {(c, {t..c})} tagged_division_of {a..c} \<and> d1 fine p \<union> {(c, {t..c})}" apply rule
-      apply(rule tagged_division_union_interval[of _ _ _ 1 "t"]) unfolding * apply(rule p)
-      apply(rule tagged_division_of_self) unfolding fine_def
-    proof safe fix x k y assume "(x,k)\<in>p" "y\<in>k" thus "y\<in>d1 x"
-        using p(2) pt unfolding fine_def d3_def apply- apply(erule_tac x="(x,k)" in ballE)+ by auto
-    next fix x assume "x\<in>{t..c}" hence "dist c x < k" unfolding dist_real_def
-        using as(1) by(auto simp add:field_simps)
-      thus "x \<in> d1 c" using k(2) unfolding d_def by auto
-    qed(insert as(2), auto) note d1_fin = d1(2)[OF this]
-
-    have *:"integral{a..c} f - integral {a..t} f = -(((c - t) *\<^sub>R f c + (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)) -
-        integral {a..c} f) + ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - integral {a..t} f) + (c - t) *\<^sub>R f c"
-      "e = (e/3 + e/3) + e/3" by auto
-    have **:"(\<Sum>(x, k)\<in>p \<union> {(c, {t..c})}. content k *\<^sub>R f x) = (c - t) *\<^sub>R f c + (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)"
-    proof- have **:"\<And>x F. F \<union> {x} = insert x F" by auto
-      have "(c, {t..c}) \<notin> p" proof safe case goal1 from p'(2-3)[OF this]
-        have "c \<in> {a..t}" by auto thus False using `t<c` by auto
-      qed thus ?thesis unfolding ** apply- apply(subst setsum_insert) apply(rule p')
-        unfolding split_conv defer apply(subst content_real) using as(2) by auto qed
-
-    have ***:"c - w < t \<and> t < c"
-    proof- have "c - k < t" using `k>0` as(1) by(auto simp add:field_simps)
-      moreover have "k \<le> w" apply(rule ccontr) using k(2)
-        unfolding subset_eq apply(erule_tac x="c + ((k + w)/2)" in ballE)
-        unfolding d_def using `k>0` `w>0` by(auto simp add:field_simps not_le not_less dist_real_def)
-      ultimately show  ?thesis using `t<c` by(auto simp add:field_simps) qed
-
-    show ?thesis unfolding *(1) apply(subst *(2)) apply(rule norm_triangle_lt add_strict_mono)+
-      unfolding norm_minus_cancel apply(rule d1_fin[unfolded **]) apply(rule d2_fin)
-      using w(2)[OF ***] unfolding norm_scaleR by(auto simp add:field_simps) qed qed
-
-lemma indefinite_integral_continuous_right: fixes f::"real \<Rightarrow> 'a::banach"
-  assumes "f integrable_on {a..b}" "a \<le> c" "c < b" "0 < e"
-  obtains d where "0 < d" "\<forall>t. c \<le> t \<and> t < c + d \<longrightarrow> norm(integral{a..c} f - integral{a..t} f) < e"
-proof- have *:"(\<lambda>x. f (- x)) integrable_on {- b..- a}" "- b < - c" "- c \<le> - a" using assms by auto
-  from indefinite_integral_continuous_left[OF * `e>0`] guess d . note d = this let ?d = "min d (b - c)"
-  show ?thesis apply(rule that[of "?d"])
-  proof safe show "0 < ?d" using d(1) assms(3) by auto
-    fix t::"real" assume as:"c \<le> t" "t < c + ?d"
-    have *:"integral{a..c} f = integral{a..b} f - integral{c..b} f"
-      "integral{a..t} f = integral{a..b} f - integral{t..b} f" unfolding algebra_simps
-      apply(rule_tac[!] integral_combine) using assms as by auto
-    have "(- c) - d < (- t) \<and> - t \<le> - c" using as by auto note d(2)[rule_format,OF this]
-    thus "norm (integral {a..c} f - integral {a..t} f) < e" unfolding *
-      unfolding integral_reflect apply-apply(subst norm_minus_commute) by(auto simp add:algebra_simps) qed qed
-
-lemma indefinite_integral_continuous: fixes f::"real \<Rightarrow> 'a::banach"
-  assumes "f integrable_on {a..b}" shows  "continuous_on {a..b} (\<lambda>x. integral {a..x} f)"
-proof(unfold continuous_on_iff, safe)  fix x e assume as:"x\<in>{a..b}" "0<(e::real)"
+    have *: "{a..c} \<inter> {x. x \<bullet> 1 \<le> t} = {a..t}" "{a..c} \<inter> {x. x \<bullet> 1 \<ge> t} = {t..c}"
+      using assms(2-3) as by (auto simp add: field_simps)
+    have "p \<union> {(c, {t..c})} tagged_division_of {a..c} \<and> d1 fine p \<union> {(c, {t..c})}"
+      apply rule
+      apply (rule tagged_division_union_interval[of _ _ _ 1 "t"])
+      unfolding *
+      apply (rule p)
+      apply (rule tagged_division_of_self)
+      unfolding fine_def
+      apply safe
+    proof -
+      fix x k y
+      assume "(x,k) \<in> p" and "y \<in> k"
+      then show "y \<in> d1 x"
+        using p(2) pt
+        unfolding fine_def d3_def
+        apply -
+        apply (erule_tac x="(x,k)" in ballE)+
+        apply auto
+        done
+    next
+      fix x assume "x \<in> {t..c}"
+      then have "dist c x < k"
+        unfolding dist_real_def
+        using as(1)
+        by (auto simp add: field_simps)
+      then show "x \<in> d1 c"
+        using k(2)
+        unfolding d_def
+        by auto
+    qed (insert as(2), auto) note d1_fin = d1(2)[OF this]
+
+    have *: "integral{a..c} f - integral {a..t} f = -(((c - t) *\<^sub>R f c + (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)) -
+      integral {a..c} f) + ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - integral {a..t} f) + (c - t) *\<^sub>R f c"
+      "e = (e/3 + e/3) + e/3"
+      by auto
+    have **: "(\<Sum>(x, k)\<in>p \<union> {(c, {t..c})}. content k *\<^sub>R f x) =
+      (c - t) *\<^sub>R f c + (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)"
+    proof -
+      have **: "\<And>x F. F \<union> {x} = insert x F"
+        by auto
+      have "(c, {t..c}) \<notin> p"
+      proof safe
+        case goal1
+        from p'(2-3)[OF this] have "c \<in> {a..t}"
+          by auto
+        then show False using `t < c`
+          by auto
+      qed
+      then show ?thesis
+        unfolding **
+        apply -
+        apply (subst setsum_insert)
+        apply (rule p')
+        unfolding split_conv
+        defer
+        apply (subst content_real)
+        using as(2)
+        apply auto
+        done
+    qed
+    have ***: "c - w < t \<and> t < c"
+    proof -
+      have "c - k < t"
+        using `k>0` as(1) by (auto simp add: field_simps)
+      moreover have "k \<le> w"
+        apply (rule ccontr)
+        using k(2)
+        unfolding subset_eq
+        apply (erule_tac x="c + ((k + w)/2)" in ballE)
+        unfolding d_def
+        using `k>0` `w>0`
+        apply (auto simp add: field_simps not_le not_less dist_real_def)
+        done
+      ultimately show ?thesis using `t < c`
+        by (auto simp add: field_simps)
+    qed
+    show ?thesis
+      unfolding *(1)
+      apply (subst *(2))
+      apply (rule norm_triangle_lt add_strict_mono)+
+      unfolding norm_minus_cancel
+      apply (rule d1_fin[unfolded **])
+      apply (rule d2_fin)
+      using w(2)[OF ***]
+      unfolding norm_scaleR
+      apply (auto simp add: field_simps)
+      done
+  qed
+qed
+
+lemma indefinite_integral_continuous_right:
+  fixes f :: "real \<Rightarrow> 'a::banach"
+  assumes "f integrable_on {a..b}"
+    and "a \<le> c"
+    and "c < b"
+    and "e > 0"
+  obtains d where "0 < d"
+    and "\<forall>t. c \<le> t \<and> t < c + d \<longrightarrow> norm (integral {a..c} f - integral {a..t} f) < e"
+proof -
+  have *: "(\<lambda>x. f (- x)) integrable_on {- b..- a}" "- b < - c" "- c \<le> - a"
+    using assms by auto
+  from indefinite_integral_continuous_left[OF * `e>0`] guess d . note d = this
+  let ?d = "min d (b - c)"
+  show ?thesis
+    apply (rule that[of "?d"])
+    apply safe
+  proof -
+    show "0 < ?d"
+      using d(1) assms(3) by auto
+    fix t :: real
+    assume as: "c \<le> t" "t < c + ?d"
+    have *: "integral {a..c} f = integral {a..b} f - integral {c..b} f"
+      "integral {a..t} f = integral {a..b} f - integral {t..b} f"
+      unfolding algebra_simps
+      apply (rule_tac[!] integral_combine)
+      using assms as
+      apply auto
+      done
+    have "(- c) - d < (- t) \<and> - t \<le> - c"
+      using as by auto note d(2)[rule_format,OF this]
+    then show "norm (integral {a..c} f - integral {a..t} f) < e"
+      unfolding *
+      unfolding integral_reflect
+      apply (subst norm_minus_commute)
+      apply (auto simp add: algebra_simps)
+      done
+  qed
+qed
+
+lemma indefinite_integral_continuous:
+  fixes f :: "real \<Rightarrow> 'a::banach"
+  assumes "f integrable_on {a..b}"
+  shows "continuous_on {a..b} (\<lambda>x. integral {a..x} f)"
+proof (unfold continuous_on_iff, safe)
+  fix x e :: real
+  assume as: "x \<in> {a..b}" "e > 0"
   let ?thesis = "\<exists>d>0. \<forall>x'\<in>{a..b}. dist x' x < d \<longrightarrow> dist (integral {a..x'} f) (integral {a..x} f) < e"
-  { presume *:"a<b \<Longrightarrow> ?thesis"
-    show ?thesis apply(cases,rule *,assumption)
-    proof- case goal1 hence "{a..b} = {x}" using as(1) apply-apply(rule set_eqI)
-        unfolding atLeastAtMost_iff by(auto simp only:field_simps not_less)
-      thus ?case using `e>0` by auto
-    qed } assume "a<b"
-  have "(x=a \<or> x=b) \<or> (a<x \<and> x<b)" using as(1) by (auto simp add:)
-  thus ?thesis apply-apply(erule disjE)+
-  proof- assume "x=a" have "a \<le> a" by auto
+  {
+    presume *: "a < b \<Longrightarrow> ?thesis"
+    show ?thesis
+      apply cases
+      apply (rule *)
+      apply assumption
+    proof -
+      case goal1
+      then have "{a..b} = {x}"
+        using as(1)
+        apply -
+        apply (rule set_eqI)
+        unfolding atLeastAtMost_iff
+        apply (auto simp only: field_simps not_less)
+        done
+      then show ?case using `e > 0` by auto
+    qed
+  }
+  assume "a < b"
+  have "(x = a \<or> x = b) \<or> (a < x \<and> x < b)"
+    using as(1) by auto
+  then show ?thesis
+    apply (elim disjE)
+  proof -
+    assume "x = a"
+    have "a \<le> a" ..
     from indefinite_integral_continuous_right[OF assms(1) this `a<b` `e>0`] guess d . note d=this
-    show ?thesis apply(rule,rule,rule d,safe) apply(subst dist_commute)
-      unfolding `x=a` dist_norm apply(rule d(2)[rule_format]) by auto
-  next   assume "x=b" have "b \<le> b" by auto
+    show ?thesis
+      apply rule
+      apply rule
+      apply (rule d)
+      apply safe
+      apply (subst dist_commute)
+      unfolding `x = a` dist_norm
+      apply (rule d(2)[rule_format])
+      apply auto
+      done
+  next
+    assume "x = b"
+    have "b \<le> b" ..
     from indefinite_integral_continuous_left[OF assms(1) `a<b` this `e>0`] guess d . note d=this
-    show ?thesis apply(rule,rule,rule d,safe) apply(subst dist_commute)
-      unfolding `x=b` dist_norm apply(rule d(2)[rule_format])  by auto
-  next assume "a<x \<and> x<b" hence xl:"a<x" "x\<le>b" and xr:"a\<le>x" "x<b" by(auto simp add: )
+    show ?thesis
+      apply rule
+      apply rule
+      apply (rule d)
+      apply safe
+      apply (subst dist_commute)
+      unfolding `x = b` dist_norm
+      apply (rule d(2)[rule_format])
+      apply auto
+      done
+  next
+    assume "a < x \<and> x < b"
+    then have xl: "a < x" "x \<le> b" and xr: "a \<le> x" "x < b"
+      by auto
     from indefinite_integral_continuous_left [OF assms(1) xl `e>0`] guess d1 . note d1=this
     from indefinite_integral_continuous_right[OF assms(1) xr `e>0`] guess d2 . note d2=this
-    show ?thesis apply(rule_tac x="min d1 d2" in exI)
-    proof safe show "0 < min d1 d2" using d1 d2 by auto
-      fix y assume "y\<in>{a..b}" "dist y x < min d1 d2"
-      thus "dist (integral {a..y} f) (integral {a..x} f) < e" apply-apply(subst dist_commute)
-        apply(cases "y < x") unfolding dist_norm apply(rule d1(2)[rule_format]) defer
-        apply(rule d2(2)[rule_format]) unfolding not_less by(auto simp add:field_simps)
-    qed qed qed
+    show ?thesis
+      apply (rule_tac x="min d1 d2" in exI)
+    proof safe
+      show "0 < min d1 d2"
+        using d1 d2 by auto
+      fix y
+      assume "y \<in> {a..b}" and "dist y x < min d1 d2"
+      then show "dist (integral {a..y} f) (integral {a..x} f) < e"
+        apply (subst dist_commute)
+        apply (cases "y < x")
+        unfolding dist_norm
+        apply (rule d1(2)[rule_format])
+        defer
+        apply (rule d2(2)[rule_format])
+        unfolding not_less
+        apply (auto simp add: field_simps)
+        done
+    qed
+  qed
+qed
+
 
 subsection {* This doesn't directly involve integration, but that gives an easy proof. *}
 
-lemma has_derivative_zero_unique_strong_interval: fixes f::"real \<Rightarrow> 'a::banach"
-  assumes "finite k" "continuous_on {a..b} f" "f a = y"
-  "\<forall>x\<in>({a..b} - k). (f has_derivative (\<lambda>h. 0)) (at x within {a..b})" "x \<in> {a..b}"
+lemma has_derivative_zero_unique_strong_interval:
+  fixes f :: "real \<Rightarrow> 'a::banach"
+  assumes "finite k"
+    and "continuous_on {a..b} f"
+    and "f a = y"
+    and "\<forall>x\<in>({a..b} - k). (f has_derivative (\<lambda>h. 0)) (at x within {a..b})" "x \<in> {a..b}"
   shows "f x = y"
-proof- have ab:"a\<le>b" using assms by auto
-  have *:"a\<le>x" using assms(5) by auto
+proof -
+  have ab: "a \<le> b"
+    using assms by auto
+  have *: "a \<le> x"
+    using assms(5) by auto
   have "((\<lambda>x. 0\<Colon>'a) has_integral f x - f a) {a..x}"
-    apply(rule fundamental_theorem_of_calculus_interior_strong[OF assms(1) *])
-    apply(rule continuous_on_subset[OF assms(2)]) defer
-    apply safe unfolding has_vector_derivative_def apply(subst has_derivative_within_open[symmetric])
-    apply assumption apply(rule open_interval) apply(rule has_derivative_within_subset[where s="{a..b}"])
-    using assms(4) assms(5) by auto note this[unfolded *]
+    apply (rule fundamental_theorem_of_calculus_interior_strong[OF assms(1) *])
+    apply (rule continuous_on_subset[OF assms(2)])
+    defer
+    apply safe
+    unfolding has_vector_derivative_def
+    apply (subst has_derivative_within_open[symmetric])
+    apply assumption
+    apply (rule open_interval)
+    apply (rule has_derivative_within_subset[where s="{a..b}"])
+    using assms(4) assms(5)
+    apply auto
+    done
+  note this[unfolded *]
   note has_integral_unique[OF has_integral_0 this]
-  thus ?thesis unfolding assms by auto qed
+  then show ?thesis
+    unfolding assms by auto
+qed
+
 
 subsection {* Generalize a bit to any convex set. *}
 
-lemma has_derivative_zero_unique_strong_convex: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::banach"
-  assumes "convex s" "finite k" "continuous_on s f" "c \<in> s" "f c = y"
-  "\<forall>x\<in>(s - k). (f has_derivative (\<lambda>h. 0)) (at x within s)" "x \<in> s"
+lemma has_derivative_zero_unique_strong_convex:
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::banach"
+  assumes "convex s"
+    and "finite k"
+    and "continuous_on s f"
+    and "c \<in> s"
+    and "f c = y"
+    and "\<forall>x\<in>(s - k). (f has_derivative (\<lambda>h. 0)) (at x within s)"
+    and "x \<in> s"
   shows "f x = y"
-proof- { presume *:"x \<noteq> c \<Longrightarrow> ?thesis" show ?thesis apply(cases,rule *,assumption)
-      unfolding assms(5)[symmetric] by auto } assume "x\<noteq>c"
+proof -
+  {
+    presume *: "x \<noteq> c \<Longrightarrow> ?thesis"
+    show ?thesis
+      apply cases
+      apply (rule *)
+      apply assumption
+      unfolding assms(5)[symmetric]
+      apply auto
+      done
+  }
+  assume "x \<noteq> c"
   note conv = assms(1)[unfolded convex_alt,rule_format]
-  have as1:"continuous_on {0..1} (f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x))"
-    apply(rule continuous_on_intros)+ apply(rule continuous_on_subset[OF assms(3)])
-    apply safe apply(rule conv) using assms(4,7) by auto
-  have *:"\<And>t xa. (1 - t) *\<^sub>R c + t *\<^sub>R x = (1 - xa) *\<^sub>R c + xa *\<^sub>R x \<Longrightarrow> t = xa"
-  proof- case goal1 hence "(t - xa) *\<^sub>R x = (t - xa) *\<^sub>R c"
-      unfolding scaleR_simps by(auto simp add:algebra_simps)
-    thus ?case using `x\<noteq>c` by auto qed
-  have as2:"finite {t. ((1 - t) *\<^sub>R c + t *\<^sub>R x) \<in> k}" using assms(2)
-    apply(rule finite_surj[where f="\<lambda>z. SOME t. (1-t) *\<^sub>R c + t *\<^sub>R x = z"])
-    apply safe unfolding image_iff apply rule defer apply assumption
-    apply(rule sym) apply(rule some_equality) defer apply(drule *) by auto
+  have as1: "continuous_on {0..1} (f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x))"
+    apply (rule continuous_on_intros)+
+    apply (rule continuous_on_subset[OF assms(3)])
+    apply safe
+    apply (rule conv)
+    using assms(4,7)
+    apply auto
+    done
+  have *: "\<And>t xa. (1 - t) *\<^sub>R c + t *\<^sub>R x = (1 - xa) *\<^sub>R c + xa *\<^sub>R x \<Longrightarrow> t = xa"
+  proof -
+    case goal1
+    then have "(t - xa) *\<^sub>R x = (t - xa) *\<^sub>R c"
+      unfolding scaleR_simps by (auto simp add: algebra_simps)
+    then show ?case
+      using `x \<noteq> c` by auto
+  qed
+  have as2: "finite {t. ((1 - t) *\<^sub>R c + t *\<^sub>R x) \<in> k}"
+    using assms(2)
+    apply (rule finite_surj[where f="\<lambda>z. SOME t. (1-t) *\<^sub>R c + t *\<^sub>R x = z"])
+    apply safe
+    unfolding image_iff
+    apply rule
+    defer
+    apply assumption
+    apply (rule sym)
+    apply (rule some_equality)
+    defer
+    apply (drule *)
+    apply auto
+    done
   have "(f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x)) 1 = y"
-    apply(rule has_derivative_zero_unique_strong_interval[OF as2 as1, of ])
-    unfolding o_def using assms(5) defer apply-apply(rule)
-  proof- fix t assume as:"t\<in>{0..1} - {t. (1 - t) *\<^sub>R c + t *\<^sub>R x \<in> k}"
-    have *:"c - t *\<^sub>R c + t *\<^sub>R x \<in> s - k" apply safe apply(rule conv[unfolded scaleR_simps])
-      using `x\<in>s` `c\<in>s` as by(auto simp add: algebra_simps)
-    have "(f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x) has_derivative (\<lambda>x. 0) \<circ> (\<lambda>z. (0 - z *\<^sub>R c) + z *\<^sub>R x)) (at t within {0..1})"
-      apply(rule diff_chain_within) apply(rule has_derivative_add)
+    apply (rule has_derivative_zero_unique_strong_interval[OF as2 as1, of ])
+    unfolding o_def
+    using assms(5)
+    defer
+    apply -
+    apply rule
+  proof -
+    fix t
+    assume as: "t \<in> {0..1} - {t. (1 - t) *\<^sub>R c + t *\<^sub>R x \<in> k}"
+    have *: "c - t *\<^sub>R c + t *\<^sub>R x \<in> s - k"
+      apply safe
+      apply (rule conv[unfolded scaleR_simps])
+      using `x \<in> s` `c \<in> s` as
+      by (auto simp add: algebra_simps)
+    have "(f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x) has_derivative (\<lambda>x. 0) \<circ> (\<lambda>z. (0 - z *\<^sub>R c) + z *\<^sub>R x))
+      (at t within {0..1})"
+      apply (rule diff_chain_within)
+      apply (rule has_derivative_add)
       unfolding scaleR_simps
-      apply(intro FDERIV_intros)
-      apply(intro FDERIV_intros)
-      apply(rule has_derivative_within_subset,rule assms(6)[rule_format])
-      apply(rule *) apply safe apply(rule conv[unfolded scaleR_simps]) using `x\<in>s` `c\<in>s` by auto
-    thus "((\<lambda>xa. f ((1 - xa) *\<^sub>R c + xa *\<^sub>R x)) has_derivative (\<lambda>h. 0)) (at t within {0..1})" unfolding o_def .
-  qed auto thus ?thesis by auto qed
-
-subsection {* Also to any open connected set with finite set of exceptions. Could
+      apply (intro FDERIV_intros)
+      apply (intro FDERIV_intros)
+      apply (rule has_derivative_within_subset,rule assms(6)[rule_format])
+      apply (rule *)
+      apply safe
+      apply (rule conv[unfolded scaleR_simps])
+      using `x \<in> s` `c \<in> s`
+      apply auto
+      done
+    then show "((\<lambda>xa. f ((1 - xa) *\<^sub>R c + xa *\<^sub>R x)) has_derivative (\<lambda>h. 0)) (at t within {0..1})"
+      unfolding o_def .
+  qed auto
+  then show ?thesis
+    by auto
+qed
+
+
+text {* Also to any open connected set with finite set of exceptions. Could
  generalize to locally convex set with limpt-free set of exceptions. *}
 
-lemma has_derivative_zero_unique_strong_connected: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::banach"
-  assumes "connected s" "open s" "finite k" "continuous_on s f" "c \<in> s" "f c = y"
-  "\<forall>x\<in>(s - k). (f has_derivative (\<lambda>h. 0)) (at x within s)" "x\<in>s"
+lemma has_derivative_zero_unique_strong_connected:
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::banach"
+  assumes "connected s"
+    and "open s"
+    and "finite k"
+    and "continuous_on s f"
+    and "c \<in> s"
+    and "f c = y"
+    and "\<forall>x\<in>(s - k). (f has_derivative (\<lambda>h. 0)) (at x within s)"
+    and "x\<in>s"
   shows "f x = y"
-proof- have "{x \<in> s. f x \<in> {y}} = {} \<or> {x \<in> s. f x \<in> {y}} = s"
-    apply(rule assms(1)[unfolded connected_clopen,rule_format]) apply rule defer
-    apply(rule continuous_closed_in_preimage[OF assms(4) closed_singleton])
-    apply(rule open_openin_trans[OF assms(2)]) unfolding open_contains_ball
-  proof safe fix x assume "x\<in>s"
+proof -
+  have "{x \<in> s. f x \<in> {y}} = {} \<or> {x \<in> s. f x \<in> {y}} = s"
+    apply (rule assms(1)[unfolded connected_clopen,rule_format])
+    apply rule
+    defer
+    apply (rule continuous_closed_in_preimage[OF assms(4) closed_singleton])
+    apply (rule open_openin_trans[OF assms(2)])
+    unfolding open_contains_ball
+  proof safe
+    fix x
+    assume "x \<in> s"
     from assms(2)[unfolded open_contains_ball,rule_format,OF this] guess e .. note e=conjunctD2[OF this]
-    show "\<exists>e>0. ball x e \<subseteq> {xa \<in> s. f xa \<in> {f x}}" apply(rule,rule,rule e)
-    proof safe fix y assume y:"y \<in> ball x e" thus "y\<in>s" using e by auto
-      show "f y = f x" apply(rule has_derivative_zero_unique_strong_convex[OF convex_ball])
-        apply(rule assms) apply(rule continuous_on_subset,rule assms) apply(rule e)+
-        apply(subst centre_in_ball,rule e,rule) apply safe
-        apply(rule has_derivative_within_subset) apply(rule assms(7)[rule_format])
-        using y e by auto qed qed
-  thus ?thesis using `x\<in>s` `f c = y` `c\<in>s` by auto qed
-
-subsection {* Integrating characteristic function of an interval. *}
-
-lemma has_integral_restrict_open_subinterval: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::banach"
-  assumes "(f has_integral i) {c..d}" "{c..d} \<subseteq> {a..b}"
+    show "\<exists>e>0. ball x e \<subseteq> {xa \<in> s. f xa \<in> {f x}}"
+      apply rule
+      apply rule
+      apply (rule e)
+    proof safe
+      fix y
+      assume y: "y \<in> ball x e"
+      then show "y \<in> s"
+        using e by auto
+      show "f y = f x"
+        apply (rule has_derivative_zero_unique_strong_convex[OF convex_ball])
+        apply (rule assms)
+        apply (rule continuous_on_subset)
+        apply (rule assms)
+        apply (rule e)+
+        apply (subst centre_in_ball)
+        apply (rule e)
+        apply rule
+        apply safe
+        apply (rule has_derivative_within_subset)
+        apply (rule assms(7)[rule_format])
+        using y e
+        apply auto
+        done
+    qed
+  qed
+  then show ?thesis
+    using `x \<in> s` `f c = y` `c \<in> s` by auto
+qed
+
+
+subsection {* Integrating characteristic function of an interval *}
+
+lemma has_integral_restrict_open_subinterval:
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::banach"
+  assumes "(f has_integral i) {c..d}"
+    and "{c..d} \<subseteq> {a..b}"
   shows "((\<lambda>x. if x \<in> {c<..<d} then f x else 0) has_integral i) {a..b}"
-proof- def g \<equiv> "\<lambda>x. if x \<in>{c<..<d} then f x else 0"
-  { presume *:"{c..d}\<noteq>{} \<Longrightarrow> ?thesis"
-    show ?thesis apply(cases,rule *,assumption)
-    proof- case goal1 hence *:"{c<..<d} = {}" using interval_open_subset_closed by auto
-      show ?thesis using assms(1) unfolding * using goal1 by auto
-    qed } assume "{c..d}\<noteq>{}"
+proof -
+  def g \<equiv> "\<lambda>x. if x \<in>{c<..<d} then f x else 0"
+  {
+    presume *: "{c..d} \<noteq> {} \<Longrightarrow> ?thesis"
+    show ?thesis
+      apply cases
+      apply (rule *)
+      apply assumption
+    proof -
+      case goal1
+      then have *: "{c<..<d} = {}"
+        using interval_open_subset_closed
+        by auto
+      show ?thesis
+        using assms(1)
+        unfolding *
+        using goal1
+        by auto
+    qed
+  }
+  assume "{c..d} \<noteq> {}"
   from partial_division_extend_1[OF assms(2) this] guess p . note p=this
   note mon = monoidal_lifted[OF monoidal_monoid]
   note operat = operative_division[OF this operative_integral p(1), symmetric]
   let ?P = "(if g integrable_on {a..b} then Some (integral {a..b} g) else None) = Some i"
-  { presume "?P" hence "g integrable_on {a..b} \<and> integral {a..b} g = i"
-      apply- apply(cases,subst(asm) if_P,assumption) by auto
-    thus ?thesis using integrable_integral unfolding g_def by auto }
+  {
+    presume "?P"
+    then have "g integrable_on {a..b} \<and> integral {a..b} g = i"
+      apply -
+      apply cases
+      apply (subst(asm) if_P)
+      apply assumption
+      apply auto
+      done
+    then show ?thesis
+      using integrable_integral
+      unfolding g_def
+      by auto
+  }
 
   note iterate_eq_neutral[OF mon,unfolded neutral_lifted[OF monoidal_monoid]]
   note * = this[unfolded neutral_add]
   have iterate:"iterate (lifted op +) (p - {{c..d}})
-      (\<lambda>i. if g integrable_on i then Some (integral i g) else None) = Some 0"
-  proof(rule *,rule) case goal1 hence "x\<in>p" by auto note div = division_ofD(2-5)[OF p(1) this]
-    from div(3) guess u v apply-by(erule exE)+ note uv=this
-    have "interior x \<inter> interior {c..d} = {}" using div(4)[OF p(2)] goal1 by auto
-    hence "(g has_integral 0) x" unfolding uv apply-apply(rule has_integral_spike_interior[where f="\<lambda>x. 0"])
-      unfolding g_def interior_closed_interval by auto thus ?case by auto
+    (\<lambda>i. if g integrable_on i then Some (integral i g) else None) = Some 0"
+  proof (rule *, rule)
+    case goal1
+    then have "x \<in> p"
+      by auto
+    note div = division_ofD(2-5)[OF p(1) this]
+    from div(3) guess u v by (elim exE) note uv=this
+    have "interior x \<inter> interior {c..d} = {}"
+      using div(4)[OF p(2)] goal1 by auto
+    then have "(g has_integral 0) x"
+      unfolding uv
+      apply -
+      apply (rule has_integral_spike_interior[where f="\<lambda>x. 0"])
+      unfolding g_def interior_closed_interval
+      apply auto
+      done
+    then show ?case
+      by auto
   qed
 
-  have *:"p = insert {c..d} (p - {{c..d}})" using p by auto
-  have **:"g integrable_on {c..d}" apply(rule integrable_spike_interior[where f=f])
-    unfolding g_def defer apply(rule has_integral_integrable) using assms(1) by auto
-  moreover have "integral {c..d} g = i" apply(rule has_integral_unique[OF _ assms(1)])
-    apply(rule has_integral_spike_interior[where f=g]) defer
-    apply(rule integrable_integral[OF **]) unfolding g_def by auto
-  ultimately show ?P unfolding operat apply- apply(subst *) apply(subst iterate_insert) apply rule+
-    unfolding iterate defer apply(subst if_not_P) defer using p by auto qed
-
-lemma has_integral_restrict_closed_subinterval: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::banach"
-  assumes "(f has_integral i) ({c..d})" "{c..d} \<subseteq> {a..b}"
+  have *: "p = insert {c..d} (p - {{c..d}})"
+    using p by auto
+  have **: "g integrable_on {c..d}"
+    apply (rule integrable_spike_interior[where f=f])
+    unfolding g_def
+    defer
+    apply (rule has_integral_integrable)
+    using assms(1)
+    apply auto
+    done
+  moreover
+  have "integral {c..d} g = i"
+    apply (rule has_integral_unique[OF _ assms(1)])
+    apply (rule has_integral_spike_interior[where f=g])
+    defer
+    apply (rule integrable_integral[OF **])
+    unfolding g_def
+    apply auto
+    done
+  ultimately show ?P
+    unfolding operat
+    apply (subst *)
+    apply (subst iterate_insert)
+    apply rule+
+    unfolding iterate
+    defer
+    apply (subst if_not_P)
+    defer
+    using p
+    apply auto
+    done
+qed
+
+lemma has_integral_restrict_closed_subinterval:
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::banach"
+  assumes "(f has_integral i) {c..d}"
+    and "{c..d} \<subseteq> {a..b}"
   shows "((\<lambda>x. if x \<in> {c..d} then f x else 0) has_integral i) {a..b}"
-proof- note has_integral_restrict_open_subinterval[OF assms]
+proof -
+  note has_integral_restrict_open_subinterval[OF assms]
   note * = has_integral_spike[OF negligible_frontier_interval _ this]
-  show ?thesis apply(rule *[of c d]) using interval_open_subset_closed[of c d] by auto qed
-
-lemma has_integral_restrict_closed_subintervals_eq: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::banach" assumes "{c..d} \<subseteq> {a..b}"
-  shows "((\<lambda>x. if x \<in> {c..d} then f x else 0) has_integral i) {a..b} \<longleftrightarrow> (f has_integral i) {c..d}" (is "?l = ?r")
-proof(cases "{c..d} = {}") case False let ?g = "\<lambda>x. if x \<in> {c..d} then f x else 0"
-  show ?thesis apply rule defer apply(rule has_integral_restrict_closed_subinterval[OF _ assms])
-  proof assumption assume ?l hence "?g integrable_on {c..d}"
-      apply-apply(rule integrable_subinterval[OF _ assms]) by auto
-    hence *:"f integrable_on {c..d}"apply-apply(rule integrable_eq) by auto
-    hence "i = integral {c..d} f" apply-apply(rule has_integral_unique)
-      apply(rule `?l`) apply(rule has_integral_restrict_closed_subinterval[OF _ assms]) by auto
-    thus ?r using * by auto qed qed auto
-
-subsection {* Hence we can apply the limit process uniformly to all integrals. *}
-
-lemma has_integral': fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::banach" shows
- "(f has_integral i) s \<longleftrightarrow> (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b}
-  \<longrightarrow> (\<exists>z. ((\<lambda>x. if x \<in> s then f(x) else 0) has_integral z) {a..b} \<and> norm(z - i) < e))" (is "?l \<longleftrightarrow> (\<forall>e>0. ?r e)")
-proof- { presume *:"\<exists>a b. s = {a..b} \<Longrightarrow> ?thesis"
-    show ?thesis apply(cases,rule *,assumption)
-      apply(subst has_integral_alt) by auto }
-  assume "\<exists>a b. s = {a..b}" then guess a b apply-by(erule exE)+ note s=this
+  show ?thesis
+    apply (rule *[of c d])
+    using interval_open_subset_closed[of c d]
+    apply auto
+    done
+qed
+
+lemma has_integral_restrict_closed_subintervals_eq:
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::banach"
+  assumes "{c..d} \<subseteq> {a..b}"
+  shows "((\<lambda>x. if x \<in> {c..d} then f x else 0) has_integral i) {a..b} \<longleftrightarrow> (f has_integral i) {c..d}"
+  (is "?l = ?r")
+proof (cases "{c..d} = {}")
+  case False
+  let ?g = "\<lambda>x. if x \<in> {c..d} then f x else 0"
+  show ?thesis
+    apply rule
+    defer
+    apply (rule has_integral_restrict_closed_subinterval[OF _ assms])
+    apply assumption
+  proof -
+    assume ?l
+    then have "?g integrable_on {c..d}"
+      apply -
+      apply (rule integrable_subinterval[OF _ assms])
+      apply auto
+      done
+    then have *: "f integrable_on {c..d}"
+      apply -
+      apply (rule integrable_eq)
+      apply auto
+      done
+    then have "i = integral {c..d} f"
+      apply -
+      apply (rule has_integral_unique)
+      apply (rule `?l`)
+      apply (rule has_integral_restrict_closed_subinterval[OF _ assms])
+      apply auto
+      done
+    then show ?r
+      using * by auto
+  qed
+qed auto
+
+
+text {* Hence we can apply the limit process uniformly to all integrals. *}
+
+lemma has_integral':
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
+  shows "(f has_integral i) s \<longleftrightarrow>
+    (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b} \<longrightarrow>
+      (\<exists>z. ((\<lambda>x. if x \<in> s then f(x) else 0) has_integral z) {a..b} \<and> norm(z - i) < e))"
+  (is "?l \<longleftrightarrow> (\<forall>e>0. ?r e)")
+proof -
+  {
+    presume *: "\<exists>a b. s = {a..b} \<Longrightarrow> ?thesis"
+    show ?thesis
+      apply cases
+      apply (rule *)
+      apply assumption
+      apply (subst has_integral_alt)
+      apply auto
+      done
+  }
+  assume "\<exists>a b. s = {a..b}"
+  then guess a b by (elim exE) note s=this
   from bounded_interval[of a b, THEN conjunct1, unfolded bounded_pos] guess B ..
-  note B = conjunctD2[OF this,rule_format] show ?thesis apply safe
-  proof- fix e assume ?l "e>(0::real)"
-    show "?r e" apply(rule_tac x="B+1" in exI) apply safe defer apply(rule_tac x=i in exI)
-    proof fix c d assume as:"ball 0 (B+1) \<subseteq> {c..d::'n::ordered_euclidean_space}"
-      thus "((\<lambda>x. if x \<in> s then f x else 0) has_integral i) {c..d}" unfolding s
-        apply-apply(rule has_integral_restrict_closed_subinterval) apply(rule `?l`[unfolded s])
-        apply safe apply(drule B(2)[rule_format]) unfolding subset_eq apply(erule_tac x=x in ballE)
-        by(auto simp add:dist_norm)
-    qed(insert B `e>0`, auto)
-  next assume as:"\<forall>e>0. ?r e"
+  note B = conjunctD2[OF this,rule_format] show ?thesis
+    apply safe
+  proof -
+    fix e :: real
+    assume ?l and "e > 0"
+    show "?r e"
+      apply (rule_tac x="B+1" in exI)
+      apply safe
+      defer
+      apply (rule_tac x=i in exI)
+    proof
+      fix c d :: 'n
+      assume as: "ball 0 (B+1) \<subseteq> {c..d}"
+      then show "((\<lambda>x. if x \<in> s then f x else 0) has_integral i) {c..d}"
+        unfolding s
+        apply -
+        apply (rule has_integral_restrict_closed_subinterval)
+        apply (rule `?l`[unfolded s])
+        apply safe
+        apply (drule B(2)[rule_format])
+        unfolding subset_eq
+        apply (erule_tac x=x in ballE)
+        apply (auto simp add: dist_norm)
+        done
+    qed (insert B `e>0`, auto)
+  next
+    assume as: "\<forall>e>0. ?r e"
     from this[rule_format,OF zero_less_one] guess C .. note C=conjunctD2[OF this,rule_format]
-    def c \<equiv> "(\<Sum>i\<in>Basis. (- max B C) *\<^sub>R i)::'n::ordered_euclidean_space"
-    def d \<equiv> "(\<Sum>i\<in>Basis. max B C *\<^sub>R i)::'n::ordered_euclidean_space"
-    have c_d:"{a..b} \<subseteq> {c..d}" apply safe apply(drule B(2)) unfolding mem_interval
+    def c \<equiv> "(\<Sum>i\<in>Basis. (- max B C) *\<^sub>R i)::'n"
+    def d \<equiv> "(\<Sum>i\<in>Basis. max B C *\<^sub>R i)::'n"
+    have c_d: "{a..b} \<subseteq> {c..d}"
+      apply safe
+      apply (drule B(2))
+      unfolding mem_interval
     proof
-      case goal1 thus ?case using Basis_le_norm[OF `i\<in>Basis`, of x] unfolding c_def d_def
-        by(auto simp add:field_simps setsum_negf)
+      case goal1
+      then show ?case
+        using Basis_le_norm[OF `i\<in>Basis`, of x]
+        unfolding c_def d_def
+        by (auto simp add: field_simps setsum_negf)
     qed
-    have "ball 0 C \<subseteq> {c..d}" apply safe unfolding mem_interval mem_ball dist_norm
+    have "ball 0 C \<subseteq> {c..d}"
+      apply safe
+      unfolding mem_interval mem_ball dist_norm
     proof
-      case goal1 thus ?case
-        using Basis_le_norm[OF `i\<in>Basis`, of x] unfolding c_def d_def by (auto simp: setsum_negf)
+      case goal1
+      then show ?case
+        using Basis_le_norm[OF `i\<in>Basis`, of x]
+        unfolding c_def d_def
+        by (auto simp: setsum_negf)
     qed
     from C(2)[OF this] have "\<exists>y. (f has_integral y) {a..b}"
-      unfolding has_integral_restrict_closed_subintervals_eq[OF c_d,symmetric] unfolding s by auto
+      unfolding has_integral_restrict_closed_subintervals_eq[OF c_d,symmetric]
+      unfolding s
+      by auto
     then guess y .. note y=this
 
-    have "y = i" proof(rule ccontr) assume "y\<noteq>i" hence "0 < norm (y - i)" by auto
+    have "y = i"
+    proof (rule ccontr)
+      assume "\<not> ?thesis"
+      then have "0 < norm (y - i)"
+        by auto
       from as[rule_format,OF this] guess C ..  note C=conjunctD2[OF this,rule_format]
-      def c \<equiv> "(\<Sum>i\<in>Basis. (- max B C) *\<^sub>R i)::'n::ordered_euclidean_space"
-      def d \<equiv> "(\<Sum>i\<in>Basis. max B C *\<^sub>R i)::'n::ordered_euclidean_space"
-      have c_d:"{a..b} \<subseteq> {c..d}" apply safe apply(drule B(2)) unfolding mem_interval
-      proof case goal1 thus ?case using Basis_le_norm[of i x] unfolding c_def d_def
-          by(auto simp add:field_simps setsum_negf) qed
-      have "ball 0 C \<subseteq> {c..d}" apply safe unfolding mem_interval mem_ball dist_norm
-      proof case goal1 thus ?case using Basis_le_norm[of i x] unfolding c_def d_def by (auto simp: setsum_negf) qed
+      def c \<equiv> "(\<Sum>i\<in>Basis. (- max B C) *\<^sub>R i)::'n"
+      def d \<equiv> "(\<Sum>i\<in>Basis. max B C *\<^sub>R i)::'n"
+      have c_d: "{a..b} \<subseteq> {c..d}"
+        apply safe
+        apply (drule B(2))
+        unfolding mem_interval
+      proof
+        case goal1
+        then show ?case
+          using Basis_le_norm[of i x]
+          unfolding c_def d_def
+          by (auto simp add: field_simps setsum_negf)
+      qed
+      have "ball 0 C \<subseteq> {c..d}"
+        apply safe
+        unfolding mem_interval mem_ball dist_norm
+      proof
+        case goal1
+        then show ?case
+          using Basis_le_norm[of i x]
+          unfolding c_def d_def
+          by (auto simp: setsum_negf)
+      qed
       note C(2)[OF this] then guess z .. note z = conjunctD2[OF this, unfolded s]
       note this[unfolded has_integral_restrict_closed_subintervals_eq[OF c_d]]
-      hence "z = y" "norm (z - i) < norm (y - i)" apply- apply(rule has_integral_unique[OF _ y(1)]) .
-      thus False by auto qed
-    thus ?l using y unfolding s by auto qed qed
-
-lemma has_integral_le: fixes f::"'n::ordered_euclidean_space \<Rightarrow> real"
-  assumes "(f has_integral i) s" "(g has_integral j) s"  "\<forall>x\<in>s. (f x) \<le> (g x)"
+      then have "z = y" and "norm (z - i) < norm (y - i)"
+        apply -
+        apply (rule has_integral_unique[OF _ y(1)])
+        apply assumption
+        apply assumption
+        done
+      then show False
+        by auto
+    qed
+    then show ?l
+      using y
+      unfolding s
+      by auto
+  qed
+qed
+
+lemma has_integral_le:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> real"
+  assumes "(f has_integral i) s"
+    and "(g has_integral j) s"
+    and "\<forall>x\<in>s. f x \<le> g x"
   shows "i \<le> j"
-  using has_integral_component_le[OF _ assms(1-2), of 1] using assms(3) by auto
-
-lemma integral_le: fixes f::"'n::ordered_euclidean_space \<Rightarrow> real"
-  assumes "f integrable_on s" "g integrable_on s" "\<forall>x\<in>s. f x \<le> g x"
+  using has_integral_component_le[OF _ assms(1-2), of 1]
+  using assms(3)
+  by auto
+
+lemma integral_le:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> real"
+  assumes "f integrable_on s"
+    and "g integrable_on s"
+    and "\<forall>x\<in>s. f x \<le> g x"
   shows "integral s f \<le> integral s g"
-  using has_integral_le[OF assms(1,2)[unfolded has_integral_integral] assms(3)] .
-
-lemma has_integral_nonneg: fixes f::"'n::ordered_euclidean_space \<Rightarrow> real"
-  assumes "(f has_integral i) s" "\<forall>x\<in>s. 0 \<le> f x" shows "0 \<le> i"
+  by (rule has_integral_le[OF assms(1,2)[unfolded has_integral_integral] assms(3)])
+
+lemma has_integral_nonneg:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> real"
+  assumes "(f has_integral i) s"
+    and "\<forall>x\<in>s. 0 \<le> f x"
+  shows "0 \<le> i"
   using has_integral_component_nonneg[of 1 f i s]
-  unfolding o_def using assms by auto
-
-lemma integral_nonneg: fixes f::"'n::ordered_euclidean_space \<Rightarrow> real"
-  assumes "f integrable_on s" "\<forall>x\<in>s. 0 \<le> f x" shows "0 \<le> integral s f"
-  using has_integral_nonneg[OF assms(1)[unfolded has_integral_integral] assms(2)] .
-
-subsection {* Hence a general restriction property. *}
-
-lemma has_integral_restrict[simp]: assumes "s \<subseteq> t" shows
-  "((\<lambda>x. if x \<in> s then f x else (0::'a::banach)) has_integral i) t \<longleftrightarrow> (f has_integral i) s"
-proof- have *:"\<And>x. (if x \<in> t then if x \<in> s then f x else 0 else 0) =  (if x\<in>s then f x else 0)" using assms by auto
-  show ?thesis apply(subst(2) has_integral') apply(subst has_integral') unfolding * by rule qed
-
-lemma has_integral_restrict_univ: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::banach" shows
-  "((\<lambda>x. if x \<in> s then f x else 0) has_integral i) UNIV \<longleftrightarrow> (f has_integral i) s" by auto
-
-lemma has_integral_on_superset: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
-  assumes "\<forall>x. ~(x \<in> s) \<longrightarrow> f x = 0" "s \<subseteq> t" "(f has_integral i) s"
+  unfolding o_def
+  using assms
+  by auto
+
+lemma integral_nonneg:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> real"
+  assumes "f integrable_on s"
+    and "\<forall>x\<in>s. 0 \<le> f x"
+  shows "0 \<le> integral s f"
+  by (rule has_integral_nonneg[OF assms(1)[unfolded has_integral_integral] assms(2)])
+
+
+text {* Hence a general restriction property. *}
+
+lemma has_integral_restrict[simp]:
+  assumes "s \<subseteq> t"
+  shows "((\<lambda>x. if x \<in> s then f x else (0::'a::banach)) has_integral i) t \<longleftrightarrow> (f has_integral i) s"
+proof -
+  have *: "\<And>x. (if x \<in> t then if x \<in> s then f x else 0 else 0) =  (if x\<in>s then f x else 0)"
+    using assms by auto
+  show ?thesis
+    apply (subst(2) has_integral')
+    apply (subst has_integral')
+    unfolding *
+    apply rule
+    done
+qed
+
+lemma has_integral_restrict_univ:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
+  shows "((\<lambda>x. if x \<in> s then f x else 0) has_integral i) UNIV \<longleftrightarrow> (f has_integral i) s"
+  by auto
+
+lemma has_integral_on_superset:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
+  assumes "\<forall>x. x \<notin> s \<longrightarrow> f x = 0"
+    and "s \<subseteq> t"
+    and "(f has_integral i) s"
   shows "(f has_integral i) t"
-proof- have "(\<lambda>x. if x \<in> s then f x else 0) = (\<lambda>x. if x \<in> t then f x else 0)"
-    apply(rule) using assms(1-2) by auto
-  thus ?thesis apply- using assms(3) apply(subst has_integral_restrict_univ[symmetric])
-  apply- apply(subst(asm) has_integral_restrict_univ[symmetric]) by auto qed
-
-lemma integrable_on_superset: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
-  assumes "\<forall>x. ~(x \<in> s) \<longrightarrow> f x = 0" "s \<subseteq> t" "f integrable_on s"
+proof -
+  have "(\<lambda>x. if x \<in> s then f x else 0) = (\<lambda>x. if x \<in> t then f x else 0)"
+    apply rule
+    using assms(1-2)
+    apply auto
+    done
+  then show ?thesis
+    using assms(3)
+    apply (subst has_integral_restrict_univ[symmetric])
+    apply (subst(asm) has_integral_restrict_univ[symmetric])
+    apply auto
+    done
+qed
+
+lemma integrable_on_superset:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
+  assumes "\<forall>x. x \<notin> s \<longrightarrow> f x = 0"
+    and "s \<subseteq> t"
+    and "f integrable_on s"
   shows "f integrable_on t"
-  using assms unfolding integrable_on_def by(auto intro:has_integral_on_superset)
-
-lemma integral_restrict_univ[intro]: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
+  using assms
+  unfolding integrable_on_def
+  by (auto intro:has_integral_on_superset)
+
+lemma integral_restrict_univ[intro]:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
   shows "f integrable_on s \<Longrightarrow> integral UNIV (\<lambda>x. if x \<in> s then f x else 0) = integral s f"
-  apply(rule integral_unique) unfolding has_integral_restrict_univ by auto
-
-lemma integrable_restrict_univ: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::banach" shows
- "(\<lambda>x. if x \<in> s then f x else 0) integrable_on UNIV \<longleftrightarrow> f integrable_on s"
-  unfolding integrable_on_def by auto
-
-lemma negligible_on_intervals: "negligible s \<longleftrightarrow> (\<forall>a b. negligible(s \<inter> {a..b}))" (is "?l = ?r")
-proof assume ?r show ?l unfolding negligible_def
-  proof safe case goal1 show ?case apply(rule has_integral_negligible[OF `?r`[rule_format,of a b]])
-      unfolding indicator_def by auto qed qed auto
-
-lemma has_integral_spike_set_eq: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
-  assumes "negligible((s - t) \<union> (t - s))" shows "((f has_integral y) s \<longleftrightarrow> (f has_integral y) t)"
-  unfolding has_integral_restrict_univ[symmetric,of f] apply(rule has_integral_spike_eq[OF assms]) by (auto split: split_if_asm)
-
-lemma has_integral_spike_set[dest]: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
-  assumes "negligible((s - t) \<union> (t - s))" "(f has_integral y) s"
+  apply (rule integral_unique)
+  unfolding has_integral_restrict_univ
+  apply auto
+  done
+
+lemma integrable_restrict_univ:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
+  shows "(\<lambda>x. if x \<in> s then f x else 0) integrable_on UNIV \<longleftrightarrow> f integrable_on s"
+  unfolding integrable_on_def
+  by auto
+
+lemma negligible_on_intervals: "negligible s \<longleftrightarrow> (\<forall>a b. negligible(s \<inter> {a..b}))" (is "?l \<longleftrightarrow> ?r")
+proof
+  assume ?r
+  show ?l
+    unfolding negligible_def
+  proof safe
+    case goal1
+    show ?case
+      apply (rule has_integral_negligible[OF `?r`[rule_format,of a b]])
+      unfolding indicator_def
+      apply auto
+      done
+  qed
+qed auto
+
+lemma has_integral_spike_set_eq:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
+  assumes "negligible ((s - t) \<union> (t - s))"
+  shows "(f has_integral y) s \<longleftrightarrow> (f has_integral y) t"
+  unfolding has_integral_restrict_univ[symmetric,of f]
+  apply (rule has_integral_spike_eq[OF assms])
+  by (auto split: split_if_asm)
+
+lemma has_integral_spike_set[dest]:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
+  assumes "negligible ((s - t) \<union> (t - s))"
+    and "(f has_integral y) s"
   shows "(f has_integral y) t"
-  using assms has_integral_spike_set_eq by auto
-
-lemma integrable_spike_set[dest]: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
-  assumes "negligible((s - t) \<union> (t - s))" "f integrable_on s"
-  shows "f integrable_on t" using assms(2) unfolding integrable_on_def
+  using assms has_integral_spike_set_eq
+  by auto
+
+lemma integrable_spike_set[dest]:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
+  assumes "negligible ((s - t) \<union> (t - s))"
+    and "f integrable_on s"
+  shows "f integrable_on t"
+  using assms(2)
+  unfolding integrable_on_def
   unfolding has_integral_spike_set_eq[OF assms(1)] .
 
-lemma integrable_spike_set_eq: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
-  assumes "negligible((s - t) \<union> (t - s))"
-  shows "(f integrable_on s \<longleftrightarrow> f integrable_on t)"
-  apply(rule,rule_tac[!] integrable_spike_set) using assms by auto
+lemma integrable_spike_set_eq:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
+  assumes "negligible ((s - t) \<union> (t - s))"
+  shows "f integrable_on s \<longleftrightarrow> f integrable_on t"
+  apply rule
+  apply (rule_tac[!] integrable_spike_set)
+  using assms
+  apply auto
+  done
 
 (*lemma integral_spike_set:
  "\<forall>f:real^M->real^N g s t.
@@ -8700,156 +9267,354 @@
   MP_TAC(ISPEC `s:real^M->bool` CLOSURE_SUBSET) THEN
   SET_TAC[]);;*)
 
-subsection {* More lemmas that are useful later. *}
-
-lemma has_integral_subset_component_le: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'm::ordered_euclidean_space"
-  assumes k: "k\<in>Basis" and as: "s \<subseteq> t" "(f has_integral i) s" "(f has_integral j) t" "\<forall>x\<in>t. 0 \<le> f(x)\<bullet>k"
+
+subsection {* More lemmas that are useful later *}
+
+lemma has_integral_subset_component_le:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'm::ordered_euclidean_space"
+  assumes k: "k \<in> Basis"
+    and as: "s \<subseteq> t" "(f has_integral i) s" "(f has_integral j) t" "\<forall>x\<in>t. 0 \<le> f(x)\<bullet>k"
   shows "i\<bullet>k \<le> j\<bullet>k"
-proof- note has_integral_restrict_univ[symmetric, of f]
+proof -
+  note has_integral_restrict_univ[symmetric, of f]
   note as(2-3)[unfolded this] note * = has_integral_component_le[OF k this]
-  show ?thesis apply(rule *) using as(1,4) by auto qed
-
-lemma has_integral_subset_le: fixes f::"'n::ordered_euclidean_space \<Rightarrow> real"
-  assumes as: "s \<subseteq> t" "(f has_integral i) s" "(f has_integral j) t" "\<forall>x\<in>t. 0 \<le> f(x)"
+  show ?thesis
+    apply (rule *)
+    using as(1,4)
+    apply auto
+    done
+qed
+
+lemma has_integral_subset_le:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> real"
+  assumes "s \<subseteq> t"
+    and "(f has_integral i) s"
+    and "(f has_integral j) t"
+    and "\<forall>x\<in>t. 0 \<le> f x"
   shows "i \<le> j"
-  using has_integral_subset_component_le[OF _ assms(1), of 1 f i j] using assms by auto
-
-lemma integral_subset_component_le: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'm::ordered_euclidean_space"
-  assumes "k\<in>Basis" "s \<subseteq> t" "f integrable_on s" "f integrable_on t" "\<forall>x \<in> t. 0 \<le> f(x)\<bullet>k"
+  using has_integral_subset_component_le[OF _ assms(1), of 1 f i j]
+  using assms
+  by auto
+
+lemma integral_subset_component_le:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'm::ordered_euclidean_space"
+  assumes "k \<in> Basis"
+    and "s \<subseteq> t"
+    and "f integrable_on s"
+    and "f integrable_on t"
+    and "\<forall>x \<in> t. 0 \<le> f x \<bullet> k"
   shows "(integral s f)\<bullet>k \<le> (integral t f)\<bullet>k"
-  apply(rule has_integral_subset_component_le) using assms by auto
-
-lemma integral_subset_le: fixes f::"'n::ordered_euclidean_space \<Rightarrow> real"
-  assumes "s \<subseteq> t" "f integrable_on s" "f integrable_on t" "\<forall>x \<in> t. 0 \<le> f(x)"
-  shows "(integral s f) \<le> (integral t f)"
-  apply(rule has_integral_subset_le) using assms by auto
-
-lemma has_integral_alt': fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
+  apply (rule has_integral_subset_component_le)
+  using assms
+  apply auto
+  done
+
+lemma integral_subset_le:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> real"
+  assumes "s \<subseteq> t"
+    and "f integrable_on s"
+    and "f integrable_on t"
+    and "\<forall>x \<in> t. 0 \<le> f x"
+  shows "integral s f \<le> integral t f"
+  apply (rule has_integral_subset_le)
+  using assms
+  apply auto
+  done
+
+lemma has_integral_alt':
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
   shows "(f has_integral i) s \<longleftrightarrow> (\<forall>a b. (\<lambda>x. if x \<in> s then f x else 0) integrable_on {a..b}) \<and>
-  (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b} \<longrightarrow> norm(integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - i) < e)" (is "?l = ?r")
-proof assume ?r
-  show ?l apply- apply(subst has_integral')
-  proof safe case goal1 from `?r`[THEN conjunct2,rule_format,OF this] guess B .. note B=conjunctD2[OF this]
-    show ?case apply(rule,rule,rule B,safe)
-      apply(rule_tac x="integral {a..b} (\<lambda>x. if x \<in> s then f x else 0)" in exI)
-      apply(drule B(2)[rule_format]) using integrable_integral[OF `?r`[THEN conjunct1,rule_format]] by auto
-  qed next
+    (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b} \<longrightarrow>
+      norm (integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - i) < e)"
+  (is "?l = ?r")
+proof
+  assume ?r
+  show ?l
+    apply (subst has_integral')
+    apply safe
+  proof -
+    case goal1
+    from `?r`[THEN conjunct2,rule_format,OF this] guess B .. note B=conjunctD2[OF this]
+    show ?case
+      apply rule
+      apply rule
+      apply (rule B)
+      apply safe
+      apply (rule_tac x="integral {a..b} (\<lambda>x. if x \<in> s then f x else 0)" in exI)
+      apply (drule B(2)[rule_format])
+      using integrable_integral[OF `?r`[THEN conjunct1,rule_format]]
+      apply auto
+      done
+  qed
+next
   assume ?l note as = this[unfolded has_integral'[of f],rule_format]
   let ?f = "\<lambda>x. if x \<in> s then f x else 0"
-  show ?r proof safe fix a b::"'n::ordered_euclidean_space"
+  show ?r
+  proof safe
+    fix a b :: 'n
     from as[OF zero_less_one] guess B .. note B=conjunctD2[OF this,rule_format]
-    let ?a = "\<Sum>i\<in>Basis. min (a\<bullet>i) (-B) *\<^sub>R i::'n" and ?b = "\<Sum>i\<in>Basis. max (b\<bullet>i) B *\<^sub>R i::'n"
-    show "?f integrable_on {a..b}" apply(rule integrable_subinterval[of _ ?a ?b])
-    proof- have "ball 0 B \<subseteq> {?a..?b}" apply safe unfolding mem_ball mem_interval dist_norm
-      proof case goal1 thus ?case using Basis_le_norm[of i x] by(auto simp add:field_simps) qed
+    let ?a = "\<Sum>i\<in>Basis. min (a\<bullet>i) (-B) *\<^sub>R i::'n"
+    let ?b = "\<Sum>i\<in>Basis. max (b\<bullet>i) B *\<^sub>R i::'n"
+    show "?f integrable_on {a..b}"
+    proof (rule integrable_subinterval[of _ ?a ?b])
+      have "ball 0 B \<subseteq> {?a..?b}"
+        apply safe
+        unfolding mem_ball mem_interval dist_norm
+      proof
+        case goal1
+        then show ?case using Basis_le_norm[of i x]
+          by (auto simp add:field_simps)
+      qed
       from B(2)[OF this] guess z .. note conjunct1[OF this]
-      thus "?f integrable_on {?a..?b}" unfolding integrable_on_def by auto
-      show "{a..b} \<subseteq> {?a..?b}" apply safe unfolding mem_interval apply(rule,erule_tac x=i in ballE) by auto qed
-
-    fix e::real assume "e>0" from as[OF this] guess B .. note B=conjunctD2[OF this,rule_format]
+      then show "?f integrable_on {?a..?b}"
+        unfolding integrable_on_def by auto
+      show "{a..b} \<subseteq> {?a..?b}"
+        apply safe
+        unfolding mem_interval
+        apply rule
+        apply (erule_tac x=i in ballE)
+        apply auto
+        done
+    qed
+
+    fix e :: real
+    assume "e > 0"
+    from as[OF this] guess B .. note B=conjunctD2[OF this,rule_format]
     show "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b} \<longrightarrow>
-                    norm (integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - i) < e"
-    proof(rule,rule,rule B,safe) case goal1 from B(2)[OF this] guess z .. note z=conjunctD2[OF this]
-      from integral_unique[OF this(1)] show ?case using z(2) by auto qed qed qed
+      norm (integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - i) < e"
+      apply rule
+      apply rule
+      apply (rule B)
+      apply safe
+    proof -
+      case goal1
+      from B(2)[OF this] guess z .. note z=conjunctD2[OF this]
+      from integral_unique[OF this(1)] show ?case
+        using z(2) by auto
+    qed
+  qed
+qed
 
 
 subsection {* Continuity of the integral (for a 1-dimensional interval). *}
 
-lemma integrable_alt: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::banach" shows
-  "f integrable_on s \<longleftrightarrow>
-          (\<forall>a b. (\<lambda>x. if x \<in> s then f x else 0) integrable_on {a..b}) \<and>
-          (\<forall>e>0. \<exists>B>0. \<forall>a b c d. ball 0 B \<subseteq> {a..b} \<and> ball 0 B \<subseteq> {c..d}
-  \<longrightarrow> norm(integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) -
-          integral {c..d}  (\<lambda>x. if x \<in> s then f x else 0)) < e)" (is "?l = ?r")
-proof assume ?l then guess y unfolding integrable_on_def .. note this[unfolded has_integral_alt'[of f]]
-  note y=conjunctD2[OF this,rule_format] show ?r apply safe apply(rule y)
-  proof- case goal1 hence "e/2 > 0" by auto from y(2)[OF this] guess B .. note B=conjunctD2[OF this,rule_format]
-    show ?case apply(rule,rule,rule B)
-    proof safe case goal1 show ?case apply(rule norm_triangle_half_l)
-        using B(2)[OF goal1(1)] B(2)[OF goal1(2)] by auto qed qed
-
-next assume ?r note as = conjunctD2[OF this,rule_format]
+lemma integrable_alt:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
+  shows "f integrable_on s \<longleftrightarrow>
+    (\<forall>a b. (\<lambda>x. if x \<in> s then f x else 0) integrable_on {a..b}) \<and>
+    (\<forall>e>0. \<exists>B>0. \<forall>a b c d. ball 0 B \<subseteq> {a..b} \<and> ball 0 B \<subseteq> {c..d} \<longrightarrow>
+    norm (integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) -
+      integral {c..d}  (\<lambda>x. if x \<in> s then f x else 0)) < e)"
+  (is "?l = ?r")
+proof
+  assume ?l
+  then guess y unfolding integrable_on_def .. note this[unfolded has_integral_alt'[of f]]
+  note y=conjunctD2[OF this,rule_format]
+  show ?r
+    apply safe
+    apply (rule y)
+  proof -
+    case goal1
+    then have "e/2 > 0"
+      by auto
+    from y(2)[OF this] guess B .. note B=conjunctD2[OF this,rule_format]
+    show ?case
+      apply rule
+      apply rule
+      apply (rule B)
+      apply safe
+    proof -
+      case goal1
+      show ?case
+        apply (rule norm_triangle_half_l)
+        using B(2)[OF goal1(1)] B(2)[OF goal1(2)]
+        apply auto
+        done
+    qed
+  qed
+next
+  assume ?r
+  note as = conjunctD2[OF this,rule_format]
   let ?cube = "\<lambda>n. {(\<Sum>i\<in>Basis. - real n *\<^sub>R i)::'n .. (\<Sum>i\<in>Basis. real n *\<^sub>R i)} :: 'n set"
   have "Cauchy (\<lambda>n. integral (?cube n) (\<lambda>x. if x \<in> s then f x else 0))"
-  proof(unfold Cauchy_def,safe) case goal1
+  proof (unfold Cauchy_def, safe)
+    case goal1
     from as(2)[OF this] guess B .. note B = conjunctD2[OF this,rule_format]
     from real_arch_simple[of B] guess N .. note N = this
-    { fix n assume n:"n \<ge> N" have "ball 0 B \<subseteq> ?cube n" apply safe
+    {
+      fix n
+      assume n: "n \<ge> N"
+      have "ball 0 B \<subseteq> ?cube n"
+        apply safe
         unfolding mem_ball mem_interval dist_norm
-      proof case goal1 thus ?case using Basis_le_norm[of i x] `i\<in>Basis`
-          using n N by(auto simp add:field_simps setsum_negf) qed }
-    thus ?case apply-apply(rule_tac x=N in exI) apply safe unfolding dist_norm apply(rule B(2)) by auto
-  qed from this[unfolded convergent_eq_cauchy[symmetric]] guess i ..
+      proof
+        case goal1
+        then show ?case
+          using Basis_le_norm[of i x] `i\<in>Basis`
+          using n N
+          by (auto simp add: field_simps setsum_negf)
+      qed
+    }
+    then show ?case
+      apply -
+      apply (rule_tac x=N in exI)
+      apply safe
+      unfolding dist_norm
+      apply (rule B(2))
+      apply auto
+      done
+  qed
+  from this[unfolded convergent_eq_cauchy[symmetric]] guess i ..
   note i = this[THEN LIMSEQ_D]
 
-  show ?l unfolding integrable_on_def has_integral_alt'[of f] apply(rule_tac x=i in exI)
-    apply safe apply(rule as(1)[unfolded integrable_on_def])
-  proof- case goal1 hence *:"e/2 > 0" by auto
+  show ?l unfolding integrable_on_def has_integral_alt'[of f]
+    apply (rule_tac x=i in exI)
+    apply safe
+    apply (rule as(1)[unfolded integrable_on_def])
+  proof -
+    case goal1
+    then have *: "e/2 > 0" by auto
     from i[OF this] guess N .. note N =this[rule_format]
-    from as(2)[OF *] guess B .. note B=conjunctD2[OF this,rule_format] let ?B = "max (real N) B"
-    show ?case apply(rule_tac x="?B" in exI)
-    proof safe show "0 < ?B" using B(1) by auto
-      fix a b assume ab:"ball 0 ?B \<subseteq> {a..b::'n::ordered_euclidean_space}"
+    from as(2)[OF *] guess B .. note B=conjunctD2[OF this,rule_format]
+    let ?B = "max (real N) B"
+    show ?case
+      apply (rule_tac x="?B" in exI)
+    proof safe
+      show "0 < ?B"
+        using B(1) by auto
+      fix a b :: 'n
+      assume ab: "ball 0 ?B \<subseteq> {a..b}"
       from real_arch_simple[of ?B] guess n .. note n=this
       show "norm (integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - i) < e"
-        apply(rule norm_triangle_half_l) apply(rule B(2)) defer apply(subst norm_minus_commute)
-        apply(rule N[of n])
-      proof safe show "N \<le> n" using n by auto
-        fix x::"'n::ordered_euclidean_space" assume x:"x \<in> ball 0 B" hence "x\<in> ball 0 ?B" by auto
-        thus "x\<in>{a..b}" using ab by blast
-        show "x\<in>?cube n" using x unfolding mem_interval mem_ball dist_norm apply-
-        proof case goal1 thus ?case using Basis_le_norm[of i x] `i\<in>Basis`
-            using n by(auto simp add:field_simps setsum_negf) qed qed qed qed qed
-
-lemma integrable_altD: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
+        apply (rule norm_triangle_half_l)
+        apply (rule B(2))
+        defer
+        apply (subst norm_minus_commute)
+        apply (rule N[of n])
+      proof safe
+        show "N \<le> n"
+          using n by auto
+        fix x :: 'n
+        assume x: "x \<in> ball 0 B"
+        then have "x \<in> ball 0 ?B"
+          by auto
+        then show "x \<in> {a..b}"
+          using ab by blast
+        show "x \<in> ?cube n"
+          using x
+          unfolding mem_interval mem_ball dist_norm
+          apply -
+        proof
+          case goal1
+          then show ?case
+            using Basis_le_norm[of i x] `i \<in> Basis`
+            using n
+            by (auto simp add: field_simps setsum_negf)
+        qed
+      qed
+    qed
+  qed
+qed
+
+lemma integrable_altD:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
   assumes "f integrable_on s"
   shows "\<And>a b. (\<lambda>x. if x \<in> s then f x else 0) integrable_on {a..b}"
-  "\<And>e. e>0 \<Longrightarrow> \<exists>B>0. \<forall>a b c d. ball 0 B \<subseteq> {a..b} \<and> ball 0 B \<subseteq> {c..d}
-  \<longrightarrow> norm(integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - integral {c..d}  (\<lambda>x. if x \<in> s then f x else 0)) < e"
+    and "\<And>e. e > 0 \<Longrightarrow> \<exists>B>0. \<forall>a b c d. ball 0 B \<subseteq> {a..b} \<and> ball 0 B \<subseteq> {c..d} \<longrightarrow>
+      norm (integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - integral {c..d}  (\<lambda>x. if x \<in> s then f x else 0)) < e"
   using assms[unfolded integrable_alt[of f]] by auto
 
-lemma integrable_on_subinterval: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
-  assumes "f integrable_on s" "{a..b} \<subseteq> s" shows "f integrable_on {a..b}"
-  apply(rule integrable_eq) defer apply(rule integrable_altD(1)[OF assms(1)])
-  using assms(2) by auto
-
-subsection {* A straddling criterion for integrability. *}
-
-lemma integrable_straddle_interval: fixes f::"'n::ordered_euclidean_space \<Rightarrow> real"
-  assumes "\<forall>e>0. \<exists>g  h i j. (g has_integral i) ({a..b}) \<and> (h has_integral j) ({a..b}) \<and>
-  norm(i - j) < e \<and> (\<forall>x\<in>{a..b}. (g x) \<le> (f x) \<and> (f x) \<le>(h x))"
+lemma integrable_on_subinterval:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
+  assumes "f integrable_on s"
+    and "{a..b} \<subseteq> s"
   shows "f integrable_on {a..b}"
-proof(subst integrable_cauchy,safe)
-  case goal1 hence e:"e/3 > 0" by auto note assms[rule_format,OF this]
-  then guess g h i j apply- by(erule exE conjE)+ note obt = this
+  apply (rule integrable_eq)
+  defer
+  apply (rule integrable_altD(1)[OF assms(1)])
+  using assms(2)
+  apply auto
+  done
+
+
+subsection {* A straddling criterion for integrability *}
+
+lemma integrable_straddle_interval:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> real"
+  assumes "\<forall>e>0. \<exists>g  h i j. (g has_integral i) {a..b} \<and> (h has_integral j) {a..b} \<and>
+    norm (i - j) < e \<and> (\<forall>x\<in>{a..b}. (g x) \<le> f x \<and> f x \<le> h x)"
+  shows "f integrable_on {a..b}"
+proof (subst integrable_cauchy, safe)
+  case goal1
+  then have e: "e/3 > 0"
+    by auto
+  note assms[rule_format,OF this]
+  then guess g h i j by (elim exE conjE) note obt = this
   from obt(1)[unfolded has_integral[of g], rule_format, OF e] guess d1 .. note d1=conjunctD2[OF this,rule_format]
   from obt(2)[unfolded has_integral[of h], rule_format, OF e] guess d2 .. note d2=conjunctD2[OF this,rule_format]
-  show ?case apply(rule_tac x="\<lambda>x. d1 x \<inter> d2 x" in exI) apply(rule conjI gauge_inter d1 d2)+ unfolding fine_inter
-  proof safe have **:"\<And>i j g1 g2 h1 h2 f1 f2. g1 - h2 \<le> f1 - f2 \<Longrightarrow> f1 - f2 \<le> h1 - g2 \<Longrightarrow>
-      abs(i - j) < e / 3 \<Longrightarrow> abs(g2 - i) < e / 3 \<Longrightarrow>  abs(g1 - i) < e / 3 \<Longrightarrow>
-      abs(h2 - j) < e / 3 \<Longrightarrow> abs(h1 - j) < e / 3 \<Longrightarrow> abs(f1 - f2) < e" using `e>0` by arith
-    case goal1 note tagged_division_ofD(2-4) note * = this[OF goal1(1)] this[OF goal1(4)]
+  show ?case
+    apply (rule_tac x="\<lambda>x. d1 x \<inter> d2 x" in exI)
+    apply (rule conjI gauge_inter d1 d2)+
+    unfolding fine_inter
+  proof safe
+    have **: "\<And>i j g1 g2 h1 h2 f1 f2. g1 - h2 \<le> f1 - f2 \<Longrightarrow> f1 - f2 \<le> h1 - g2 \<Longrightarrow>
+      abs (i - j) < e / 3 \<Longrightarrow> abs (g2 - i) < e / 3 \<Longrightarrow>  abs (g1 - i) < e / 3 \<Longrightarrow>
+      abs (h2 - j) < e / 3 \<Longrightarrow> abs (h1 - j) < e / 3 \<Longrightarrow> abs (f1 - f2) < e"
+    using `e > 0` by arith
+    case goal1
+    note tagged_division_ofD(2-4) note * = this[OF goal1(1)] this[OF goal1(4)]
 
     have "(\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p1. content k *\<^sub>R g x) \<ge> 0"
-      "0 \<le> (\<Sum>(x, k)\<in>p2. content k *\<^sub>R h x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)"
-      "(\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R g x) \<ge> 0"
-      "0 \<le> (\<Sum>(x, k)\<in>p1. content k *\<^sub>R h x) - (\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x)"
-      unfolding setsum_subtractf[symmetric] apply- apply(rule_tac[!] setsum_nonneg)
-      apply safe unfolding real_scaleR_def right_diff_distrib[symmetric]
-      apply(rule_tac[!] mult_nonneg_nonneg)
-    proof- fix a b assume ab:"(a,b) \<in> p1"
-      show "0 \<le> content b" using *(3)[OF ab] apply safe using content_pos_le . thus "0 \<le> content b" .
-      show "0 \<le> f a - g a" "0 \<le> h a - f a" using *(1-2)[OF ab] using obt(4)[rule_format,of a] by auto
-    next fix a b assume ab:"(a,b) \<in> p2"
-      show "0 \<le> content b" using *(6)[OF ab] apply safe using content_pos_le . thus "0 \<le> content b" .
-      show "0 \<le> f a - g a" "0 \<le> h a - f a" using *(4-5)[OF ab] using obt(4)[rule_format,of a] by auto qed
-
-    thus ?case apply- unfolding real_norm_def apply(rule **) defer defer
-      unfolding real_norm_def[symmetric] apply(rule obt(3))
-      apply(rule d1(2)[OF conjI[OF goal1(4,5)]])
-      apply(rule d1(2)[OF conjI[OF goal1(1,2)]])
-      apply(rule d2(2)[OF conjI[OF goal1(4,6)]])
-      apply(rule d2(2)[OF conjI[OF goal1(1,3)]]) by auto qed qed
+      and "0 \<le> (\<Sum>(x, k)\<in>p2. content k *\<^sub>R h x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)"
+      and "(\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R g x) \<ge> 0"
+      and "0 \<le> (\<Sum>(x, k)\<in>p1. content k *\<^sub>R h x) - (\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x)"
+      unfolding setsum_subtractf[symmetric]
+      apply -
+      apply (rule_tac[!] setsum_nonneg)
+      apply safe
+      unfolding real_scaleR_def right_diff_distrib[symmetric]
+      apply (rule_tac[!] mult_nonneg_nonneg)
+    proof -
+      fix a b
+      assume ab: "(a, b) \<in> p1"
+      show "0 \<le> content b"
+        using *(3)[OF ab]
+        apply safe
+        apply (rule content_pos_le)
+        done
+      then show "0 \<le> content b" .
+      show "0 \<le> f a - g a" "0 \<le> h a - f a"
+        using *(1-2)[OF ab]
+        using obt(4)[rule_format,of a]
+        by auto
+    next
+      fix a b
+      assume ab: "(a, b) \<in> p2"
+      show "0 \<le> content b"
+        using *(6)[OF ab]
+        apply safe
+        apply (rule content_pos_le)
+        done
+      then show "0 \<le> content b" .
+      show "0 \<le> f a - g a" and "0 \<le> h a - f a"
+        using *(4-5)[OF ab] using obt(4)[rule_format,of a] by auto
+    qed
+    then show ?case
+      apply -
+      unfolding real_norm_def
+      apply (rule **)
+      defer
+      defer
+      unfolding real_norm_def[symmetric]
+      apply (rule obt(3))
+      apply (rule d1(2)[OF conjI[OF goal1(4,5)]])
+      apply (rule d1(2)[OF conjI[OF goal1(1,2)]])
+      apply (rule d2(2)[OF conjI[OF goal1(4,6)]])
+      apply (rule d2(2)[OF conjI[OF goal1(1,3)]])
+      apply auto
+      done
+  qed
+qed
 
 lemma integrable_straddle: fixes f::"'n::ordered_euclidean_space \<Rightarrow> real"
   assumes "\<forall>e>0. \<exists>g h i j. (g has_integral i) s \<and> (h has_integral j) s \<and>