# HG changeset patch
# User wenzelm
# Date 1378331858 -7200
# Node ID 0d45f21e372d1afad629e58db483284e2d74a75e
# Parent  e114f515527c4350bb1c49eb835d15531bf4b0b3
tuned proofs;

diff -r e114f515527c -r 0d45f21e372d src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Sep 04 22:37:19 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Sep 04 23:57:38 2013 +0200
@@ -2427,16 +2427,22 @@
   obtains p where "p tagged_division_of {a..b}" "g fine p"
 proof -
   presume "\<not> (\<exists>p. p tagged_division_of {a..b} \<and> g fine p) \<Longrightarrow> False"
-  then obtain p where "p tagged_division_of {a..b}" "g fine p" by blast
+  then obtain p where "p tagged_division_of {a..b}" "g fine p"
+    by blast
   then show thesis ..
 next
   assume as: "\<not> (\<exists>p. p tagged_division_of {a..b} \<and> g fine p)"
-  guess x apply(rule interval_bisection[of "\<lambda>s. \<exists>p. p tagged_division_of s \<and> g fine p",rule_format,OF _ _ as])
-    apply(rule_tac x="{}" in exI)
-    defer apply(erule conjE exE)+
+  guess x
+    apply (rule interval_bisection[of "\<lambda>s. \<exists>p. p tagged_division_of s \<and> g fine p",rule_format,OF _ _ as])
+    apply (rule_tac x="{}" in exI)
+    defer
+    apply (erule conjE exE)+
   proof -
-    show "{} tagged_division_of {} \<and> g fine {}" unfolding fine_def by auto
-    fix s t p p' assume "p tagged_division_of s" "g fine p" "p' tagged_division_of t" "g fine p'" "interior s \<inter> interior t = {}"
+    show "{} tagged_division_of {} \<and> g fine {}"
+      unfolding fine_def by auto
+    fix s t p p'
+    assume "p tagged_division_of s" "g fine p" "p' tagged_division_of t" "g fine p'"
+      "interior s \<inter> interior t = {}"
     then show "\<exists>p. p tagged_division_of s \<union> t \<and> g fine p"
       apply -
       apply (rule_tac x="p \<union> p'" in exI)
@@ -2446,13 +2452,19 @@
       apply (rule fine_union)
       apply auto
       done
-  qed note x=this
-  obtain e where e:"e > 0" "ball x e \<subseteq> g x"
+  qed note x = this
+  obtain e where e: "e > 0" "ball x e \<subseteq> g x"
     using gaugeD[OF assms, of x] unfolding open_contains_ball by auto
-  from x(2)[OF e(1)] guess c d apply-apply(erule exE conjE)+ . note c_d = this
+  from x(2)[OF e(1)] obtain c d where c_d:
+    "x \<in> {c..d}"
+    "{c..d} \<subseteq> ball x e"
+    "{c..d} \<subseteq> {a..b}"
+    "\<not> (\<exists>p. p tagged_division_of {c..d} \<and> g fine p)"
+    by blast
   have "g fine {(x, {c..d})}"
     unfolding fine_def using e using c_d(2) by auto
-  then show False using tagged_division_of_self[OF c_d(1)] using c_d by auto
+  then show False
+    using tagged_division_of_self[OF c_d(1)] using c_d by auto
 qed
 
 
@@ -2460,303 +2472,656 @@
 
 lemma has_integral_unique:
   fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::real_normed_vector"
-  assumes "(f has_integral k1) i" and "(f has_integral k2) i"
+  assumes "(f has_integral k1) i"
+    and "(f has_integral k2) i"
   shows "k1 = k2"
-proof (rule ccontr) let ?e = "norm(k1 - k2) / 2" assume as:"k1 \<noteq> k2" hence e:"?e > 0" by auto
-  have lem:"\<And>f::'n \<Rightarrow> 'a.  \<And> a b k1 k2.
+proof (rule ccontr)
+  let ?e = "norm(k1 - k2) / 2"
+  assume as:"k1 \<noteq> k2"
+  then have e: "?e > 0"
+    by auto
+  have lem: "\<And>f::'n \<Rightarrow> 'a.  \<And>a b k1 k2.
     (f has_integral k1) ({a..b}) \<Longrightarrow> (f has_integral k2) ({a..b}) \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> False"
-  proof- case goal1 let ?e = "norm(k1 - k2) / 2" from goal1(3) have e:"?e > 0" by auto
-    guess d1 by(rule has_integralD[OF goal1(1) e]) note d1=this
-    guess d2 by(rule has_integralD[OF goal1(2) e]) note d2=this
-    guess p by(rule fine_division_exists[OF gauge_inter[OF d1(1) d2(1)],of a b]) note p=this
-    let ?c = "(\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)" have "norm (k1 - k2) \<le> norm (?c - k2) + norm (?c - k1)"
-      using norm_triangle_ineq4[of "k1 - ?c" "k2 - ?c"] by(auto simp add:algebra_simps norm_minus_commute)
+  proof -
+    case goal1
+    let ?e = "norm (k1 - k2) / 2"
+    from goal1(3) have e: "?e > 0" by auto
+    guess d1 by (rule has_integralD[OF goal1(1) e]) note d1=this
+    guess d2 by (rule has_integralD[OF goal1(2) e]) note d2=this
+    guess p by (rule fine_division_exists[OF gauge_inter[OF d1(1) d2(1)],of a b]) note p=this
+    let ?c = "(\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)"
+    have "norm (k1 - k2) \<le> norm (?c - k2) + norm (?c - k1)"
+      using norm_triangle_ineq4[of "k1 - ?c" "k2 - ?c"]
+      by (auto simp add:algebra_simps norm_minus_commute)
     also have "\<dots> < norm (k1 - k2) / 2 + norm (k1 - k2) / 2"
-      apply(rule add_strict_mono) apply(rule_tac[!] d2(2) d1(2)) using p unfolding fine_def by auto
+      apply (rule add_strict_mono)
+      apply (rule_tac[!] d2(2) d1(2))
+      using p unfolding fine_def
+      apply auto
+      done
     finally show False by auto
-  qed { presume "\<not> (\<exists>a b. i = {a..b}) \<Longrightarrow> False"
-    thus False apply-apply(cases "\<exists>a b. i = {a..b}")
-      using assms by(auto simp add:has_integral intro:lem[OF _ _ as]) }
-  assume as:"\<not> (\<exists>a b. i = {a..b})"
-  guess B1 by(rule has_integral_altD[OF assms(1) as,OF e]) note B1=this[rule_format]
-  guess B2 by(rule has_integral_altD[OF assms(2) as,OF e]) note B2=this[rule_format]
-  have "\<exists>a b::'n. ball 0 B1 \<union> ball 0 B2 \<subseteq> {a..b}" apply(rule bounded_subset_closed_interval)
-    using bounded_Un bounded_ball by auto then guess a b apply-by(erule exE)+
-  note ab=conjunctD2[OF this[unfolded Un_subset_iff]]
-  guess w using B1(2)[OF ab(1)] .. note w=conjunctD2[OF this]
-  guess z using B2(2)[OF ab(2)] .. note z=conjunctD2[OF this]
-  have "z = w" using lem[OF w(1) z(1)] by auto
-  hence "norm (k1 - k2) \<le> norm (z - k2) + norm (w - k1)"
-    using norm_triangle_ineq4[of "k1 - w" "k2 - z"] by(auto simp add: norm_minus_commute)
-  also have "\<dots> < norm (k1 - k2) / 2 + norm (k1 - k2) / 2" apply(rule add_strict_mono) by(rule_tac[!] z(2) w(2))
-  finally show False by auto qed
-
-lemma integral_unique[intro]:
-  "(f has_integral y) k \<Longrightarrow> integral k f = y"
-  unfolding integral_def apply(rule some_equality) by(auto intro: has_integral_unique)
-
-lemma has_integral_is_0: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::real_normed_vector"
-  assumes "\<forall>x\<in>s. f x = 0" shows "(f has_integral 0) s"
-proof- have lem:"\<And>a b. \<And>f::'n \<Rightarrow> 'a.
-    (\<forall>x\<in>{a..b}. f(x) = 0) \<Longrightarrow> (f has_integral 0) ({a..b})" unfolding has_integral
-  proof(rule,rule) fix a b e and f::"'n \<Rightarrow> 'a"
-    assume as:"\<forall>x\<in>{a..b}. f x = 0" "0 < (e::real)"
-    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) - 0) < e)"
-      apply(rule_tac x="\<lambda>x. ball x 1" in exI)  apply(rule,rule gaugeI) unfolding centre_in_ball defer apply(rule open_ball)
-    proof(rule,rule,erule conjE) case goal1
-      have "(\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) = 0" proof(rule setsum_0',rule)
-        fix x assume x:"x\<in>p" have "f (fst x) = 0" using tagged_division_ofD(2-3)[OF goal1(1), of "fst x" "snd x"] using as x by auto
-        thus "(\<lambda>(x, k). content k *\<^sub>R f x) x = 0" apply(subst surjective_pairing[of x]) unfolding split_conv by auto
-      qed thus ?case using as by auto
-    qed auto qed  { presume "\<not> (\<exists>a b. s = {a..b}) \<Longrightarrow> ?thesis"
-    thus ?thesis apply-apply(cases "\<exists>a b. s = {a..b}")
-      using assms by(auto simp add:has_integral intro:lem) }
-  have *:"(\<lambda>x. if x \<in> s then f x else 0) = (\<lambda>x. 0)" apply(rule ext) using assms by auto
-  assume "\<not> (\<exists>a b. s = {a..b})" thus ?thesis apply(subst has_integral_alt) unfolding if_not_P *
-  apply(rule,rule,rule_tac x=1 in exI,rule) defer apply(rule,rule,rule)
-  proof- fix e::real and a b assume "e>0"
-    thus "\<exists>z. ((\<lambda>x::'n. 0::'a) has_integral z) {a..b} \<and> norm (z - 0) < e"
-      apply(rule_tac x=0 in exI) apply(rule,rule lem) by auto
-  qed auto qed
+  qed
+  {
+    presume "\<not> (\<exists>a b. i = {a..b}) \<Longrightarrow> False"
+    then show False
+      apply -
+      apply (cases "\<exists>a b. i = {a..b}")
+      using assms
+      apply (auto simp add:has_integral intro:lem[OF _ _ as])
+      done
+  }
+  assume as: "\<not> (\<exists>a b. i = {a..b})"
+  guess B1 by (rule has_integral_altD[OF assms(1) as,OF e]) note B1=this[rule_format]
+  guess B2 by (rule has_integral_altD[OF assms(2) as,OF e]) note B2=this[rule_format]
+  have "\<exists>a b::'n. ball 0 B1 \<union> ball 0 B2 \<subseteq> {a..b}"
+    apply (rule bounded_subset_closed_interval)
+    using bounded_Un bounded_ball
+    apply auto
+    done
+  then obtain a b :: 'n where ab: "ball 0 B1 \<subseteq> {a..b}" "ball 0 B2 \<subseteq> {a..b}"
+    by blast
+  obtain w where w:
+    "((\<lambda>x. if x \<in> i then f x else 0) has_integral w) {a..b}"
+    "norm (w - k1) < norm (k1 - k2) / 2"
+    using B1(2)[OF ab(1)] by blast
+  obtain z where z:
+    "((\<lambda>x. if x \<in> i then f x else 0) has_integral z) {a..b}"
+    "norm (z - k2) < norm (k1 - k2) / 2"
+    using B2(2)[OF ab(2)] by blast
+  have "z = w"
+    using lem[OF w(1) z(1)] by auto
+  then have "norm (k1 - k2) \<le> norm (z - k2) + norm (w - k1)"
+    using norm_triangle_ineq4 [of "k1 - w" "k2 - z"]
+    by (auto simp add: norm_minus_commute)
+  also have "\<dots> < norm (k1 - k2) / 2 + norm (k1 - k2) / 2"
+    apply (rule add_strict_mono)
+    apply (rule_tac[!] z(2) w(2))
+    done
+  finally show False by auto
+qed
+
+lemma integral_unique [intro]: "(f has_integral y) k \<Longrightarrow> integral k f = y"
+  unfolding integral_def
+  by (rule some_equality) (auto intro: has_integral_unique)
+
+lemma has_integral_is_0:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::real_normed_vector"
+  assumes "\<forall>x\<in>s. f x = 0"
+  shows "(f has_integral 0) s"
+proof -
+  have lem: "\<And>a b. \<And>f::'n \<Rightarrow> 'a.
+    (\<forall>x\<in>{a..b}. f(x) = 0) \<Longrightarrow> (f has_integral 0) ({a..b})"
+    unfolding has_integral
+    apply rule
+    apply rule
+  proof -
+    fix a b e
+    fix f :: "'n \<Rightarrow> 'a"
+    assume as: "\<forall>x\<in>{a..b}. f x = 0" "0 < (e::real)"
+    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) - 0) < e)"
+      apply (rule_tac x="\<lambda>x. ball x 1" in exI)
+      apply rule
+      apply (rule gaugeI)
+      unfolding centre_in_ball
+      defer
+      apply (rule open_ball)
+      apply rule
+      apply rule
+      apply (erule conjE)
+    proof -
+      case goal1
+      have "(\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) = 0"
+      proof (rule setsum_0', rule)
+        fix x
+        assume x: "x \<in> p"
+        have "f (fst x) = 0"
+          using tagged_division_ofD(2-3)[OF goal1(1), of "fst x" "snd x"] using as x by auto
+        then show "(\<lambda>(x, k). content k *\<^sub>R f x) x = 0"
+          apply (subst surjective_pairing[of x])
+          unfolding split_conv
+          apply auto
+          done
+      qed
+      then show ?case
+        using as by auto
+    qed auto
+  qed
+  {
+    presume "\<not> (\<exists>a b. s = {a..b}) \<Longrightarrow> ?thesis"
+    then show ?thesis
+      apply -
+      apply (cases "\<exists>a b. s = {a..b}")
+      using assms
+      apply (auto simp add:has_integral intro: lem)
+      done
+  }
+  have *: "(\<lambda>x. if x \<in> s then f x else 0) = (\<lambda>x. 0)"
+    apply (rule ext)
+    using assms
+    apply auto
+    done
+  assume "\<not> (\<exists>a b. s = {a..b})"
+  then show ?thesis
+    apply (subst has_integral_alt)
+    unfolding if_not_P *
+    apply rule
+    apply rule
+    apply (rule_tac x=1 in exI)
+    apply rule
+    defer
+    apply rule
+    apply rule
+    apply rule
+  proof -
+    fix e :: real
+    fix a b
+    assume "e > 0"
+    then show "\<exists>z. ((\<lambda>x::'n. 0::'a) has_integral z) {a..b} \<and> norm (z - 0) < e"
+      apply (rule_tac x=0 in exI)
+      apply(rule,rule lem)
+      apply auto
+      done
+  qed auto
+qed
 
 lemma has_integral_0[simp]: "((\<lambda>x::'n::ordered_euclidean_space. 0) has_integral 0) s"
-  apply(rule has_integral_is_0) by auto
+  by (rule has_integral_is_0) auto
 
 lemma has_integral_0_eq[simp]: "((\<lambda>x. 0) has_integral i) s \<longleftrightarrow> i = 0"
   using has_integral_unique[OF has_integral_0] by auto
 
-lemma has_integral_linear: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::real_normed_vector"
-  assumes "(f has_integral y) s" "bounded_linear h" shows "((h o f) has_integral ((h y))) s"
-proof- interpret bounded_linear h using assms(2) . from pos_bounded guess B .. note B=conjunctD2[OF this,rule_format]
-  have lem:"\<And>f::'n \<Rightarrow> 'a. \<And> y a b.
-    (f has_integral y) ({a..b}) \<Longrightarrow> ((h o f) has_integral h(y)) ({a..b})"
-  proof(subst has_integral,rule,rule) case goal1
-    from pos_bounded guess B .. note B=conjunctD2[OF this,rule_format]
-    have *:"e / B > 0" apply(rule divide_pos_pos) using goal1(2) B by auto
-    guess g using has_integralD[OF goal1(1) *] . note g=this
-    show ?case apply(rule_tac x=g in exI) apply(rule,rule g(1))
-    proof(rule,rule,erule conjE) fix p assume as:"p tagged_division_of {a..b}" "g fine p"
-      have *:"\<And>x k. h ((\<lambda>(x, k). content k *\<^sub>R f x) x) = (\<lambda>(x, k). h (content k *\<^sub>R f x)) x" by auto
+lemma has_integral_linear:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::real_normed_vector"
+  assumes "(f has_integral y) s"
+    and "bounded_linear h"
+  shows "((h o f) has_integral ((h y))) s"
+proof -
+  interpret bounded_linear h
+    using assms(2) .
+  from pos_bounded obtain B where B: "0 < B" "\<And>x. norm (h x) \<le> norm x * B"
+    by blast
+  have lem: "\<And>(f :: 'n \<Rightarrow> 'a) y a b.
+    (f has_integral y) {a..b} \<Longrightarrow> ((h o f) has_integral h y) {a..b}"
+    apply (subst has_integral)
+    apply rule
+    apply rule
+  proof -
+    case goal1
+    from pos_bounded
+    obtain B where B: "0 < B" "\<And>x. norm (h x) \<le> norm x * B"
+      by blast
+    have *: "e / B > 0"
+      apply (rule divide_pos_pos)
+      using goal1(2) B
+      apply auto
+      done
+      thm has_integralD[OF goal1(1) *]
+    obtain g where g:
+      "gauge g"
+      "\<And>p. p tagged_division_of {a..b} \<Longrightarrow> g fine p \<Longrightarrow>
+        norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - y) < e / B"
+      by (rule has_integralD[OF goal1(1) *]) blast
+    show ?case
+      apply (rule_tac x=g in exI)
+      apply rule
+      apply (rule g(1))
+      apply rule
+      apply rule
+      apply (erule conjE)
+    proof -
+      fix p
+      assume as: "p tagged_division_of {a..b}" "g fine p"
+      have *: "\<And>x k. h ((\<lambda>(x, k). content k *\<^sub>R f x) x) = (\<lambda>(x, k). h (content k *\<^sub>R f x)) x"
+        by auto
       have "(\<Sum>(x, k)\<in>p. content k *\<^sub>R (h \<circ> f) x) = setsum (h \<circ> (\<lambda>(x, k). content k *\<^sub>R f x)) p"
         unfolding o_def unfolding scaleR[symmetric] * by simp
-      also have "\<dots> = h (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)" using setsum[of "\<lambda>(x,k). content k *\<^sub>R f x" p] using as by auto
-      finally have *:"(\<Sum>(x, k)\<in>p. content k *\<^sub>R (h \<circ> f) x) = h (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)" .
-      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (h \<circ> f) x) - h y) < e" unfolding * diff[symmetric]
-        apply(rule le_less_trans[OF B(2)]) using g(2)[OF as] B(1) by(auto simp add:field_simps)
-    qed qed { presume "\<not> (\<exists>a b. s = {a..b}) \<Longrightarrow> ?thesis"
-    thus ?thesis apply-apply(cases "\<exists>a b. s = {a..b}") using assms by(auto simp add:has_integral intro!:lem) }
-  assume as:"\<not> (\<exists>a b. s = {a..b})" thus ?thesis apply(subst has_integral_alt) unfolding if_not_P
-  proof(rule,rule) fix e::real  assume e:"0<e"
-    have *:"0 < e/B" by(rule divide_pos_pos,rule e,rule B(1))
-    guess M using has_integral_altD[OF assms(1) as *,rule_format] . note M=this
-    show "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b} \<longrightarrow> (\<exists>z. ((\<lambda>x. if x \<in> s then (h \<circ> f) x else 0) has_integral z) {a..b} \<and> norm (z - h y) < e)"
-      apply(rule_tac x=M in exI) apply(rule,rule M(1))
-    proof(rule,rule,rule) case goal1 guess z using M(2)[OF goal1(1)] .. note z=conjunctD2[OF this]
-      have *:"(\<lambda>x. if x \<in> s then (h \<circ> f) x else 0) = h \<circ> (\<lambda>x. if x \<in> s then f x else 0)"
-        unfolding o_def apply(rule ext) using zero by auto
-      show ?case apply(rule_tac x="h z" in exI,rule) unfolding * apply(rule lem[OF z(1)]) unfolding diff[symmetric]
-        apply(rule le_less_trans[OF B(2)]) using B(1) z(2) by(auto simp add:field_simps)
-    qed qed qed
-
-lemma has_integral_cmul:
-  shows "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) s"
-  unfolding o_def[symmetric] apply(rule has_integral_linear,assumption)
-  by(rule bounded_linear_scaleR_right)
+      also have "\<dots> = h (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)"
+        using setsum[of "\<lambda>(x,k). content k *\<^sub>R f x" p] using as by auto
+      finally have *: "(\<Sum>(x, k)\<in>p. content k *\<^sub>R (h \<circ> f) x) = h (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)" .
+      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (h \<circ> f) x) - h y) < e"
+        unfolding * diff[symmetric]
+        apply (rule le_less_trans[OF B(2)])
+        using g(2)[OF as] B(1)
+        apply (auto simp add: field_simps)
+        done
+    qed
+  qed
+  {
+    presume "\<not> (\<exists>a b. s = {a..b}) \<Longrightarrow> ?thesis"
+    then show ?thesis
+      apply -
+      apply (cases "\<exists>a b. s = {a..b}")
+      using assms
+      apply (auto simp add:has_integral intro!:lem)
+      done
+  }
+  assume as: "\<not> (\<exists>a b. s = {a..b})"
+  then show ?thesis
+    apply (subst has_integral_alt)
+    unfolding if_not_P
+    apply rule
+    apply rule
+  proof -
+    fix e :: real
+    assume e: "e > 0"
+    have *: "0 < e/B"
+      by (rule divide_pos_pos,rule e,rule B(1))
+    obtain M where M:
+      "M > 0"
+      "\<And>a b. ball 0 M \<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 - y) < e / B"
+      using has_integral_altD[OF assms(1) as *] by blast
+    show "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b} \<longrightarrow>
+      (\<exists>z. ((\<lambda>x. if x \<in> s then (h \<circ> f) x else 0) has_integral z) {a..b} \<and> norm (z - h y) < e)"
+      apply (rule_tac x=M in exI)
+      apply rule
+      apply (rule M(1))
+      apply rule
+      apply rule
+      apply rule
+    proof -
+      case goal1
+      obtain z where z:
+        "((\<lambda>x. if x \<in> s then f x else 0) has_integral z) {a..b}"
+        "norm (z - y) < e / B"
+        using M(2)[OF goal1(1)] by blast
+      have *: "(\<lambda>x. if x \<in> s then (h \<circ> f) x else 0) = h \<circ> (\<lambda>x. if x \<in> s then f x else 0)"
+        unfolding o_def
+        apply (rule ext)
+        using zero
+        apply auto
+        done
+      show ?case
+        apply (rule_tac x="h z" in exI)
+        apply rule
+        unfolding *
+        apply (rule lem[OF z(1)])
+        unfolding diff[symmetric]
+        apply (rule le_less_trans[OF B(2)])
+        using B(1) z(2)
+        apply (auto simp add: field_simps)
+        done
+    qed
+  qed
+qed
+
+lemma has_integral_cmul: "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) s"
+  unfolding o_def[symmetric]
+  apply (rule has_integral_linear,assumption)
+  apply (rule bounded_linear_scaleR_right)
+  done
 
 lemma has_integral_cmult_real:
   fixes c :: real
   assumes "c \<noteq> 0 \<Longrightarrow> (f has_integral x) A"
   shows "((\<lambda>x. c * f x) has_integral c * x) A"
-proof cases
-  assume "c \<noteq> 0"
+proof (cases "c = 0")
+  case True
+  then show ?thesis by simp
+next
+  case False
   from has_integral_cmul[OF assms[OF this], of c] show ?thesis
     unfolding real_scaleR_def .
-qed simp
-
-lemma has_integral_neg:
-  shows "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. -(f x)) has_integral (-k)) s"
-  apply(drule_tac c="-1" in has_integral_cmul) by auto
-
-lemma has_integral_add: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::real_normed_vector"
-  assumes "(f has_integral k) s" "(g has_integral l) s"
+qed
+
+lemma has_integral_neg: "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. -(f x)) has_integral (-k)) s"
+  apply (drule_tac c="-1" in has_integral_cmul)
+  apply auto
+  done
+
+lemma has_integral_add:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::real_normed_vector"
+  assumes "(f has_integral k) s"
+    and "(g has_integral l) s"
   shows "((\<lambda>x. f x + g x) has_integral (k + l)) s"
-proof- have lem:"\<And>f g::'n \<Rightarrow> 'a. \<And>a b k l.
-    (f has_integral k) ({a..b}) \<Longrightarrow> (g has_integral l) ({a..b}) \<Longrightarrow>
-     ((\<lambda>x. f(x) + g(x)) has_integral (k + l)) ({a..b})" proof- case goal1
-    show ?case unfolding has_integral proof(rule,rule) fix e::real assume e:"e>0" hence *:"e/2>0" by auto
-      guess d1 using has_integralD[OF goal1(1) *] . note d1=this
-      guess d2 using has_integralD[OF goal1(2) *] . note d2=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 + g x)) - (k + l)) < e)"
-        apply(rule_tac x="\<lambda>x. (d1 x) \<inter> (d2 x)" in exI) apply(rule,rule gauge_inter[OF d1(1) d2(1)])
-      proof(rule,rule,erule conjE) fix p assume as:"p tagged_division_of {a..b}" "(\<lambda>x. d1 x \<inter> d2 x) fine p"
-        have *:"(\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) = (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p. content k *\<^sub>R g x)"
+proof -
+  have lem:"\<And>(f:: 'n \<Rightarrow> 'a) g a b k l.
+    (f has_integral k) {a..b} \<Longrightarrow>
+    (g has_integral l) {a..b} \<Longrightarrow>
+    ((\<lambda>x. f x + g x) has_integral (k + l)) {a..b}"
+  proof -
+    case goal1
+    show ?case
+      unfolding has_integral
+      apply rule
+      apply rule
+    proof -
+      fix e :: real
+      assume e: "e > 0"
+      then have *: "e/2 > 0"
+        by auto
+      obtain d1 where d1:
+        "gauge d1"
+        "\<And>p. p tagged_division_of {a..b} \<Longrightarrow> d1 fine p \<Longrightarrow>
+          norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k) < e / 2"
+        using has_integralD[OF goal1(1) *] by blast
+      obtain d2 where d2:
+        "gauge d2"
+        "\<And>p. p tagged_division_of {a..b} \<Longrightarrow> d2 fine p \<Longrightarrow>
+          norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - l) < e / 2"
+        using has_integralD[OF goal1(2) *] by blast
+      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 + g x)) - (k + l)) < e)"
+        apply (rule_tac x="\<lambda>x. (d1 x) \<inter> (d2 x)" in exI)
+        apply rule
+        apply (rule gauge_inter[OF d1(1) d2(1)])
+        apply (rule,rule,erule conjE)
+      proof -
+        fix p
+        assume as: "p tagged_division_of {a..b}" "(\<lambda>x. d1 x \<inter> d2 x) fine p"
+        have *: "(\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) =
+          (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p. content k *\<^sub>R g x)"
           unfolding scaleR_right_distrib setsum_addf[of "\<lambda>(x,k). content k *\<^sub>R f x" "\<lambda>(x,k). content k *\<^sub>R g x" p,symmetric]
-          by(rule setsum_cong2,auto)
-        have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) = norm (((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k) + ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - l))"
-          unfolding * by(auto simp add:algebra_simps) also let ?res = "\<dots>"
-        from as have *:"d1 fine p" "d2 fine p" unfolding fine_inter by auto
-        have "?res < e/2 + e/2" apply(rule le_less_trans[OF norm_triangle_ineq])
-          apply(rule add_strict_mono) using d1(2)[OF as(1) *(1)] and d2(2)[OF as(1) *(2)] by auto
-        finally show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) < e" by auto
-      qed qed qed { presume "\<not> (\<exists>a b. s = {a..b}) \<Longrightarrow> ?thesis"
-    thus ?thesis apply-apply(cases "\<exists>a b. s = {a..b}") using assms by(auto simp add:has_integral intro!:lem) }
-  assume as:"\<not> (\<exists>a b. s = {a..b})" thus ?thesis apply(subst has_integral_alt) unfolding if_not_P
-  proof(rule,rule) case goal1 hence *:"e/2 > 0" by auto
+          by (rule setsum_cong2) auto
+        have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) =
+          norm (((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k) + ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - l))"
+          unfolding * by (auto simp add: algebra_simps)
+        also
+        let ?res = "\<dots>"
+        from as have *: "d1 fine p" "d2 fine p"
+          unfolding fine_inter by auto
+        have "?res < e/2 + e/2"
+          apply (rule le_less_trans[OF norm_triangle_ineq])
+          apply (rule add_strict_mono)
+          using d1(2)[OF as(1) *(1)] and d2(2)[OF as(1) *(2)]
+          apply auto
+          done
+        finally show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) < e"
+          by auto
+      qed
+    qed
+  qed
+  {
+    presume "\<not> (\<exists>a b. s = {a..b}) \<Longrightarrow> ?thesis"
+    then show ?thesis
+      apply -
+      apply (cases "\<exists>a b. s = {a..b}")
+      using assms
+      apply (auto simp add:has_integral intro!:lem)
+      done
+  }
+  assume as: "\<not> (\<exists>a b. s = {a..b})"
+  then show ?thesis
+    apply (subst has_integral_alt)
+    unfolding if_not_P
+    apply rule
+    apply rule
+  proof -
+    case goal1
+    then have *: "e/2 > 0"
+      by auto
     from has_integral_altD[OF assms(1) as *] guess B1 . note B1=this[rule_format]
     from has_integral_altD[OF assms(2) as *] guess B2 . note B2=this[rule_format]
-    show ?case apply(rule_tac x="max B1 B2" in exI) apply(rule,rule min_max.less_supI1,rule B1)
-    proof(rule,rule,rule) fix a b assume "ball 0 (max B1 B2) \<subseteq> {a..b::'n}"
-      hence *:"ball 0 B1 \<subseteq> {a..b::'n}" "ball 0 B2 \<subseteq> {a..b::'n}" by auto
-      guess w using B1(2)[OF *(1)] .. note w=conjunctD2[OF this]
-      guess z using B2(2)[OF *(2)] .. note z=conjunctD2[OF this]
-      have *:"\<And>x. (if x \<in> s then f x + g x else 0) = (if x \<in> s then f x else 0) + (if x \<in> s then g x else 0)" by auto
+    show ?case
+      apply (rule_tac x="max B1 B2" in exI)
+      apply rule
+      apply (rule min_max.less_supI1)
+      apply (rule B1)
+      apply rule
+      apply rule
+      apply rule
+    proof -
+      fix a b
+      assume "ball 0 (max B1 B2) \<subseteq> {a..b::'n}"
+      then have *: "ball 0 B1 \<subseteq> {a..b::'n}" "ball 0 B2 \<subseteq> {a..b::'n}"
+        by auto
+      obtain w where w:
+        "((\<lambda>x. if x \<in> s then f x else 0) has_integral w) {a..b}"
+        "norm (w - k) < e / 2"
+        using B1(2)[OF *(1)] by blast
+      obtain z where z:
+        "((\<lambda>x. if x \<in> s then g x else 0) has_integral z) {a..b}"
+        "norm (z - l) < e / 2"
+        using B2(2)[OF *(2)] by blast
+      have *: "\<And>x. (if x \<in> s then f x + g x else 0) =
+        (if x \<in> s then f x else 0) + (if x \<in> s then g x else 0)"
+        by auto
       show "\<exists>z. ((\<lambda>x. if x \<in> s then f x + g x else 0) has_integral z) {a..b} \<and> norm (z - (k + l)) < e"
-        apply(rule_tac x="w + z" in exI) apply(rule,rule lem[OF w(1) z(1), unfolded *[symmetric]])
-        using norm_triangle_ineq[of "w - k" "z - l"] w(2) z(2) by(auto simp add:field_simps)
-    qed qed qed
+        apply (rule_tac x="w + z" in exI)
+        apply rule
+        apply (rule lem[OF w(1) z(1), unfolded *[symmetric]])
+        using norm_triangle_ineq[of "w - k" "z - l"] w(2) z(2)
+        apply (auto simp add: field_simps)
+        done
+    qed
+  qed
+qed
 
 lemma has_integral_sub:
-  shows "(f has_integral k) s \<Longrightarrow> (g has_integral l) s \<Longrightarrow> ((\<lambda>x. f(x) - g(x)) has_integral (k - l)) s"
-  using has_integral_add[OF _ has_integral_neg,of f k s g l] unfolding algebra_simps by auto
-
-lemma integral_0: "integral s (\<lambda>x::'n::ordered_euclidean_space. 0::'m::real_normed_vector) = 0"
-  by(rule integral_unique has_integral_0)+
-
-lemma integral_add:
-  shows "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow>
-   integral s (\<lambda>x. f x + g x) = integral s f + integral s g"
-  apply(rule integral_unique) apply(drule integrable_integral)+
-  apply(rule has_integral_add) by assumption+
-
-lemma integral_cmul:
-  shows "f integrable_on s \<Longrightarrow> integral s (\<lambda>x. c *\<^sub>R f x) = c *\<^sub>R integral s f"
-  apply(rule integral_unique) apply(drule integrable_integral)+
-  apply(rule has_integral_cmul) by assumption+
-
-lemma integral_neg:
-  shows "f integrable_on s \<Longrightarrow> integral s (\<lambda>x. - f x) = - integral s f"
-  apply(rule integral_unique) apply(drule integrable_integral)+
-  apply(rule has_integral_neg) by assumption+
-
-lemma integral_sub:
-  shows "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow> integral s (\<lambda>x. f x - g x) = integral s f - integral s g"
-  apply(rule integral_unique) apply(drule integrable_integral)+
-  apply(rule has_integral_sub) by assumption+
+  "(f has_integral k) s \<Longrightarrow> (g has_integral l) s \<Longrightarrow>
+    ((\<lambda>x. f x - g x) has_integral (k - l)) s"
+  using has_integral_add[OF _ has_integral_neg, of f k s g l]
+  unfolding algebra_simps
+  by auto
+
+lemma integral_0:
+  "integral s (\<lambda>x::'n::ordered_euclidean_space. 0::'m::real_normed_vector) = 0"
+  by (rule integral_unique has_integral_0)+
+
+lemma integral_add: "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow>
+    integral s (\<lambda>x. f x + g x) = integral s f + integral s g"
+  apply (rule integral_unique)
+  apply (drule integrable_integral)+
+  apply (rule has_integral_add)
+  apply assumption+
+  done
+
+lemma integral_cmul: "f integrable_on s \<Longrightarrow> integral s (\<lambda>x. c *\<^sub>R f x) = c *\<^sub>R integral s f"
+  apply (rule integral_unique)
+  apply (drule integrable_integral)+
+  apply (rule has_integral_cmul)
+  apply assumption+
+  done
+
+lemma integral_neg: "f integrable_on s \<Longrightarrow> integral s (\<lambda>x. - f x) = - integral s f"
+  apply (rule integral_unique)
+  apply (drule integrable_integral)+
+  apply (rule has_integral_neg)
+  apply assumption+
+  done
+
+lemma integral_sub: "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow>
+    integral s (\<lambda>x. f x - g x) = integral s f - integral s g"
+  apply (rule integral_unique)
+  apply (drule integrable_integral)+
+  apply (rule has_integral_sub)
+  apply assumption+
+  done
 
 lemma integrable_0: "(\<lambda>x. 0) integrable_on s"
   unfolding integrable_on_def using has_integral_0 by auto
 
-lemma integrable_add:
-  shows "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow> (\<lambda>x. f x + g x) integrable_on s"
+lemma integrable_add: "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow> (\<lambda>x. f x + g x) integrable_on s"
   unfolding integrable_on_def by(auto intro: has_integral_add)
 
-lemma integrable_cmul:
-  shows "f integrable_on s \<Longrightarrow> (\<lambda>x. c *\<^sub>R f(x)) integrable_on s"
+lemma integrable_cmul: "f integrable_on s \<Longrightarrow> (\<lambda>x. c *\<^sub>R f(x)) integrable_on s"
   unfolding integrable_on_def by(auto intro: has_integral_cmul)
 
 lemma integrable_on_cmult_iff:
-  fixes c :: real assumes "c \<noteq> 0"
+  fixes c :: real
+  assumes "c \<noteq> 0"
   shows "(\<lambda>x. c * f x) integrable_on s \<longleftrightarrow> f integrable_on s"
   using integrable_cmul[of "\<lambda>x. c * f x" s "1 / c"] integrable_cmul[of f s c] `c \<noteq> 0`
   by auto
 
-lemma integrable_neg:
-  shows "f integrable_on s \<Longrightarrow> (\<lambda>x. -f(x)) integrable_on s"
+lemma integrable_neg: "f integrable_on s \<Longrightarrow> (\<lambda>x. -f(x)) integrable_on s"
   unfolding integrable_on_def by(auto intro: has_integral_neg)
 
 lemma integrable_sub:
-  shows "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow> (\<lambda>x. f x - g x) integrable_on s"
+  "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow> (\<lambda>x. f x - g x) integrable_on s"
   unfolding integrable_on_def by(auto intro: has_integral_sub)
 
 lemma integrable_linear:
-  shows "f integrable_on s \<Longrightarrow> bounded_linear h \<Longrightarrow> (h o f) integrable_on s"
+  "f integrable_on s \<Longrightarrow> bounded_linear h \<Longrightarrow> (h \<circ> f) integrable_on s"
   unfolding integrable_on_def by(auto intro: has_integral_linear)
 
 lemma integral_linear:
-  shows "f integrable_on s \<Longrightarrow> bounded_linear h \<Longrightarrow> integral s (h o f) = h(integral s f)"
-  apply(rule has_integral_unique) defer unfolding has_integral_integral
-  apply(drule has_integral_linear,assumption,assumption) unfolding has_integral_integral[symmetric]
-  apply(rule integrable_linear) by assumption+
-
-lemma integral_component_eq[simp]: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'm::ordered_euclidean_space"
-  assumes "f integrable_on s" shows "integral s (\<lambda>x. f x \<bullet> k) = integral s f \<bullet> k"
+  "f integrable_on s \<Longrightarrow> bounded_linear h \<Longrightarrow> integral s (h \<circ> f) = h (integral s f)"
+  apply (rule has_integral_unique)
+  defer
+  unfolding has_integral_integral
+  apply (drule (2) has_integral_linear)
+  unfolding has_integral_integral[symmetric]
+  apply (rule integrable_linear)
+  apply assumption+
+  done
+
+lemma integral_component_eq[simp]:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'm::ordered_euclidean_space"
+  assumes "f integrable_on s"
+  shows "integral s (\<lambda>x. f x \<bullet> k) = integral s f \<bullet> k"
   unfolding integral_linear[OF assms(1) bounded_linear_component,unfolded o_def] ..
 
 lemma has_integral_setsum:
-  assumes "finite t" "\<forall>a\<in>t. ((f a) has_integral (i a)) s"
+  assumes "finite t"
+    and "\<forall>a\<in>t. ((f a) has_integral (i a)) s"
   shows "((\<lambda>x. setsum (\<lambda>a. f a x) t) has_integral (setsum i t)) s"
-proof(insert assms(1) subset_refl[of t],induct rule:finite_subset_induct)
-  case (insert x F) show ?case unfolding setsum_insert[OF insert(1,3)]
-    apply(rule has_integral_add) using insert assms by auto
-qed auto
-
-lemma integral_setsum:
-  shows "finite t \<Longrightarrow> \<forall>a\<in>t. (f a) integrable_on s \<Longrightarrow>
+  using assms(1) subset_refl[of t]
+proof (induct rule: finite_subset_induct)
+  case empty
+  then show ?case by auto
+next
+  case (insert x F)
+  show ?case
+    unfolding setsum_insert[OF insert(1,3)]
+    apply (rule has_integral_add)
+    using insert assms
+    apply auto
+    done
+qed
+
+lemma integral_setsum: "finite t \<Longrightarrow> \<forall>a\<in>t. (f a) integrable_on s \<Longrightarrow>
   integral s (\<lambda>x. setsum (\<lambda>a. f a x) t) = setsum (\<lambda>a. integral s (f a)) t"
-  apply(rule integral_unique) apply(rule has_integral_setsum)
-  using integrable_integral by auto
+  apply (rule integral_unique)
+  apply (rule has_integral_setsum)
+  using integrable_integral
+  apply auto
+  done
 
 lemma integrable_setsum:
-  shows "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] by auto
+  "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]
+  apply auto
+  done
 
 lemma has_integral_eq:
-  assumes "\<forall>x\<in>s. f x = g x" "(f has_integral k) s" shows "(g has_integral k) s"
+  assumes "\<forall>x\<in>s. f x = g x"
+    and "(f has_integral k) s"
+  shows "(g has_integral k) s"
   using has_integral_sub[OF assms(2), of "\<lambda>x. f x - g x" 0]
-  using has_integral_is_0[of s "\<lambda>x. f x - g x"] using assms(1) by auto
-
-lemma integrable_eq:
-  shows "\<forall>x\<in>s. f x = g x \<Longrightarrow> f integrable_on s \<Longrightarrow> g integrable_on s"
-  unfolding integrable_on_def using has_integral_eq[of s f g] by auto
-
-lemma has_integral_eq_eq:
-  shows "\<forall>x\<in>s. f x = g x \<Longrightarrow> ((f has_integral k) s \<longleftrightarrow> (g has_integral k) s)"
-  using has_integral_eq[of s f g] has_integral_eq[of s g f] by rule auto
+  using has_integral_is_0[of s "\<lambda>x. f x - g x"]
+  using assms(1)
+  by auto
+
+lemma integrable_eq: "\<forall>x\<in>s. f x = g x \<Longrightarrow> f integrable_on s \<Longrightarrow> g integrable_on s"
+  unfolding integrable_on_def
+  using has_integral_eq[of s f g]
+  by auto
+
+lemma has_integral_eq_eq: "\<forall>x\<in>s. f x = g x \<Longrightarrow> (f has_integral k) s \<longleftrightarrow> (g has_integral k) s"
+  using has_integral_eq[of s f g] has_integral_eq[of s g f]
+  by auto
 
 lemma has_integral_null[dest]:
-  assumes "content({a..b}) = 0" shows  "(f has_integral 0) ({a..b})"
-  unfolding has_integral apply(rule,rule,rule_tac x="\<lambda>x. ball x 1" in exI,rule) defer
-proof(rule,rule,erule conjE) fix e::real assume e:"e>0" thus "gauge (\<lambda>x. ball x 1)" by auto
-  fix p assume p:"p tagged_division_of {a..b}" (*"(\<lambda>x. ball x 1) fine p"*)
-  have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) = 0" unfolding norm_eq_zero diff_0_right
+  assumes "content({a..b}) = 0"
+  shows "(f has_integral 0) ({a..b})"
+  unfolding has_integral
+  apply rule
+  apply rule
+  apply (rule_tac x="\<lambda>x. ball x 1" in exI)
+  apply rule
+  defer
+  apply rule
+  apply rule
+  apply (erule conjE)
+proof -
+  fix e :: real
+  assume e: "e > 0"
+  then show "gauge (\<lambda>x. ball x 1)"
+    by auto
+  fix p
+  assume p: "p tagged_division_of {a..b}"
+  have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) = 0"
+    unfolding norm_eq_zero diff_0_right
     using setsum_content_null[OF assms(1) p, of f] .
-  thus "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) < e" using e by auto qed
-
-lemma has_integral_null_eq[simp]:
-  shows "content({a..b}) = 0 \<Longrightarrow> ((f has_integral i) ({a..b}) \<longleftrightarrow> i = 0)"
-  apply rule apply(rule has_integral_unique,assumption)
-  apply(drule has_integral_null,assumption)
-  apply(drule has_integral_null) by auto
-
-lemma integral_null[dest]: shows "content({a..b}) = 0 \<Longrightarrow> integral({a..b}) f = 0"
-  by(rule integral_unique,drule has_integral_null)
-
-lemma integrable_on_null[dest]: shows "content({a..b}) = 0 \<Longrightarrow> f integrable_on {a..b}"
-  unfolding integrable_on_def apply(drule has_integral_null) by auto
-
-lemma has_integral_empty[intro]: shows "(f has_integral 0) {}"
-  unfolding empty_as_interval apply(rule has_integral_null)
-  using content_empty unfolding empty_as_interval .
-
-lemma has_integral_empty_eq[simp]: shows "(f has_integral i) {} \<longleftrightarrow> i = 0"
-  apply(rule,rule has_integral_unique,assumption) by auto
-
-lemma integrable_on_empty[intro]: shows "f integrable_on {}" unfolding integrable_on_def by auto
-
-lemma integral_empty[simp]: shows "integral {} f = 0"
-  apply(rule integral_unique) using has_integral_empty .
-
-lemma has_integral_refl[intro]: shows "(f has_integral 0) {a..a}" "(f has_integral 0) {a::'a::ordered_euclidean_space}"
-proof-
-  have *:"{a} = {a..a}" apply(rule set_eqI) unfolding mem_interval singleton_iff euclidean_eq_iff[where 'a='a]
-    apply safe prefer 3 apply(erule_tac x=b in ballE) by(auto simp add: field_simps)
-  show "(f has_integral 0) {a..a}" "(f has_integral 0) {a}" unfolding *
-    apply(rule_tac[!] has_integral_null) unfolding content_eq_0_interior
-    unfolding interior_closed_interval using interval_sing by auto qed
-
-lemma integrable_on_refl[intro]: shows "f integrable_on {a..a}" unfolding integrable_on_def by auto
-
-lemma integral_refl: shows "integral {a..a} f = 0" apply(rule integral_unique) by auto
+  then show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) < e"
+    using e by auto
+qed
+
+lemma has_integral_null_eq[simp]: "content {a..b} = 0 \<Longrightarrow> (f has_integral i) {a..b} \<longleftrightarrow> i = 0"
+  apply rule
+  apply (rule has_integral_unique)
+  apply assumption
+  apply (drule (1) has_integral_null)
+  apply (drule has_integral_null)
+  apply auto
+  done
+
+lemma integral_null[dest]: "content {a..b} = 0 \<Longrightarrow> integral {a..b} f = 0"
+  apply (rule integral_unique)
+  apply (drule has_integral_null)
+  apply assumption
+  done
+
+lemma integrable_on_null[dest]: "content {a..b} = 0 \<Longrightarrow> f integrable_on {a..b}"
+  unfolding integrable_on_def
+  apply (drule has_integral_null)
+  apply auto
+  done
+
+lemma has_integral_empty[intro]: "(f has_integral 0) {}"
+  unfolding empty_as_interval
+  apply (rule has_integral_null)
+  using content_empty
+  unfolding empty_as_interval
+  apply assumption
+  done
+
+lemma has_integral_empty_eq[simp]: "(f has_integral i) {} \<longleftrightarrow> i = 0"
+  apply rule
+  apply (rule has_integral_unique)
+  apply assumption
+  apply auto
+  done
+
+lemma integrable_on_empty[intro]: "f integrable_on {}"
+  unfolding integrable_on_def by auto
+
+lemma integral_empty[simp]: "integral {} f = 0"
+  by (rule integral_unique) (rule has_integral_empty)
+
+lemma has_integral_refl[intro]:
+  fixes a :: "'a::ordered_euclidean_space"
+  shows "(f has_integral 0) {a..a}"
+    and "(f has_integral 0) {a}"
+proof -
+  have *: "{a} = {a..a}"
+    apply (rule set_eqI)
+    unfolding mem_interval singleton_iff euclidean_eq_iff[where 'a='a]
+    apply safe
+    prefer 3
+    apply (erule_tac x=b in ballE)
+    apply (auto simp add: field_simps)
+    done
+  show "(f has_integral 0) {a..a}" "(f has_integral 0) {a}"
+    unfolding *
+    apply (rule_tac[!] has_integral_null)
+    unfolding content_eq_0_interior
+    unfolding interior_closed_interval
+    using interval_sing
+    apply auto
+    done
+qed
+
+lemma integrable_on_refl[intro]: "f integrable_on {a..a}"
+  unfolding integrable_on_def by auto
+
+lemma integral_refl: "integral {a..a} f = 0"
+  by (rule integral_unique) auto
+
 
 subsection {* Cauchy-type criterion for integrability. *}