# HG changeset patch
# User wenzelm
# Date 1378850459 -7200
# Node ID ee1bdeb9e0ed6e1bac801b93c92c989113637dec
# Parent  706f7edea3d402abe8725535499b84898df84f1f
tuned proofs;

diff -r 706f7edea3d4 -r ee1bdeb9e0ed src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Sep 10 23:50:03 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Sep 11 00:00:59 2013 +0200
@@ -8206,35 +8206,89 @@
 
 subsection {* Stronger form with finite number of exceptional points. *}
 
-lemma fundamental_theorem_of_calculus_interior_strong: fixes f::"real \<Rightarrow> 'a::banach"
-  assumes"finite s" "a \<le> b" "continuous_on {a..b} f"
-  "\<forall>x\<in>{a<..<b} - s. (f has_vector_derivative f'(x)) (at x)"
-  shows "(f' has_integral (f b - f a)) {a..b}" using assms apply-
-proof(induct "card s" arbitrary:s a b)
-  case 0 show ?case apply(rule fundamental_theorem_of_calculus_interior) using 0 by auto
-next case (Suc n) from this(2) guess c s' apply-apply(subst(asm) eq_commute) unfolding card_Suc_eq
-    apply(subst(asm)(2) eq_commute) by(erule exE conjE)+ note cs = this[rule_format]
-  show ?case proof(cases "c\<in>{a<..<b}")
-    case False thus ?thesis apply- apply(rule Suc(1)[OF cs(3) _ Suc(4,5)]) apply safe defer
-      apply(rule Suc(6)[rule_format]) using Suc(3) unfolding cs by auto
-  next have *:"f b - f a = (f c - f a) + (f b - f c)" by auto
-    case True hence "a \<le> c" "c \<le> b" by auto
-    thus ?thesis apply(subst *) apply(rule has_integral_combine) apply assumption+
-      apply(rule_tac[!] Suc(1)[OF cs(3)]) using Suc(3) unfolding cs
-    proof- show "continuous_on {a..c} f" "continuous_on {c..b} f"
-        apply(rule_tac[!] continuous_on_subset[OF Suc(5)]) using True by auto
+lemma fundamental_theorem_of_calculus_interior_strong:
+  fixes f :: "real \<Rightarrow> 'a::banach"
+  assumes "finite s"
+    and "a \<le> b"
+    and "continuous_on {a..b} f"
+    and "\<forall>x\<in>{a<..<b} - s. (f has_vector_derivative f'(x)) (at x)"
+  shows "(f' has_integral (f b - f a)) {a..b}"
+  using assms
+proof (induct "card s" arbitrary: s a b)
+  case 0
+  show ?case
+    apply (rule fundamental_theorem_of_calculus_interior)
+    using 0
+    apply auto
+    done
+next
+  case (Suc n)
+  from this(2) guess c s'
+    apply -
+    apply (subst(asm) eq_commute)
+    unfolding card_Suc_eq
+    apply (subst(asm)(2) eq_commute)
+    apply (elim exE conjE)
+    done
+  note cs = this[rule_format]
+  show ?case
+  proof (cases "c \<in> {a<..<b}")
+    case False
+    then show ?thesis
+      apply -
+      apply (rule Suc(1)[OF cs(3) _ Suc(4,5)])
+      apply safe
+      defer
+      apply (rule Suc(6)[rule_format])
+      using Suc(3)
+      unfolding cs
+      apply auto
+      done
+  next
+    have *: "f b - f a = (f c - f a) + (f b - f c)"
+      by auto
+    case True
+    then have "a \<le> c" "c \<le> b"
+      by auto
+    then show ?thesis
+      apply (subst *)
+      apply (rule has_integral_combine)
+      apply assumption+
+      apply (rule_tac[!] Suc(1)[OF cs(3)])
+      using Suc(3)
+      unfolding cs
+    proof -
+      show "continuous_on {a..c} f" "continuous_on {c..b} f"
+        apply (rule_tac[!] continuous_on_subset[OF Suc(5)])
+        using True
+        apply auto
+        done
       let ?P = "\<lambda>i j. \<forall>x\<in>{i<..<j} - s'. (f has_vector_derivative f' x) (at x)"
-      show "?P a c" "?P c b" apply safe apply(rule_tac[!] Suc(6)[rule_format]) using True unfolding cs by auto
-    qed auto qed qed
-
-lemma fundamental_theorem_of_calculus_strong: fixes f::"real \<Rightarrow> 'a::banach"
-  assumes "finite s" "a \<le> b" "continuous_on {a..b} f"
-  "\<forall>x\<in>{a..b} - s. (f has_vector_derivative f'(x)) (at x)"
+      show "?P a c" "?P c b"
+        apply safe
+        apply (rule_tac[!] Suc(6)[rule_format])
+        using True
+        unfolding cs
+        apply auto
+        done
+    qed auto
+  qed
+qed
+
+lemma fundamental_theorem_of_calculus_strong:
+  fixes f :: "real \<Rightarrow> 'a::banach"
+  assumes "finite s"
+    and "a \<le> b"
+    and "continuous_on {a..b} f"
+    and "\<forall>x\<in>{a..b} - s. (f has_vector_derivative f'(x)) (at x)"
   shows "(f' has_integral (f(b) - f(a))) {a..b}"
-  apply(rule fundamental_theorem_of_calculus_interior_strong[OF assms(1-3), of f'])
-  using assms(4) by auto
-
-lemma indefinite_integral_continuous_left: fixes f::"real \<Rightarrow> 'a::banach"
+  apply (rule fundamental_theorem_of_calculus_interior_strong[OF assms(1-3), of f'])
+  using assms(4)
+  apply auto
+  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"
@@ -10162,7 +10216,8 @@
         apply (rule_tac x=N in exI)
       proof safe
         case goal1
-        have *:"\<And>y ix. y < i + r \<longrightarrow> i \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> abs(ix - i) < r" by arith
+        have *: "\<And>y ix. y < i + r \<longrightarrow> i \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> abs(ix - i) < r"
+          by arith
         show ?case
           unfolding real_norm_def
             apply (rule *[rule_format,OF y(2)])