# HG changeset patch
# User huffman
# Date 1395363333 25200
# Node ID 2a091015a89651715e10bb4b2c94e2dfe481f34e
# Parent  9b32aafecec172f0eb6a662de6d396a3380b6c50
tuned proofs

diff -r 9b32aafecec1 -r 2a091015a896 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Mar 24 16:33:36 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Mar 20 17:55:33 2014 -0700
@@ -707,22 +707,24 @@
   assumes "a < b"
     and "\<forall>x\<in>{a..b}. (f has_derivative f' x) (at x within {a..b})"
   shows "\<exists>x\<in>{a<..<b}. f b - f a = f' x (b - a)"
-  apply (rule mvt)
-  apply (rule assms(1))
-  apply (rule differentiable_imp_continuous_on)
-  unfolding differentiable_on_def differentiable_def
-  defer
-proof
-  fix x
-  assume x: "x \<in> {a <..< b}"
-  show "(f has_derivative f' x) (at x)"
-    unfolding has_derivative_within_open[OF x open_greaterThanLessThan,symmetric]
-    apply (rule has_derivative_within_subset)
-    apply (rule assms(2)[rule_format])
-    using x
-    apply auto
-    done
-qed (insert assms(2), auto)
+proof (rule mvt)
+  have "f differentiable_on {a..b}"
+    using assms(2) unfolding differentiable_on_def differentiable_def by fast
+  then show "continuous_on {a..b} f"
+    by (rule differentiable_imp_continuous_on)
+  show "\<forall>x\<in>{a<..<b}. (f has_derivative f' x) (at x)"
+  proof
+    fix x
+    assume x: "x \<in> {a <..< b}"
+    show "(f has_derivative f' x) (at x)"
+      unfolding at_within_open[OF x open_greaterThanLessThan,symmetric]
+      apply (rule has_derivative_within_subset)
+      apply (rule assms(2)[rule_format])
+      using x
+      apply auto
+      done
+  qed
+qed (rule assms(1))
 
 lemma mvt_very_simple:
   fixes f :: "real \<Rightarrow> real"
@@ -758,18 +760,16 @@
     and "\<forall>x\<in>{a<..<b}. (f has_derivative f'(x)) (at x)"
   shows "\<exists>x\<in>{a<..<b}. norm (f b - f a) \<le> norm (f' x (b - a))"
 proof -
-  have "\<exists>x\<in>{a<..<b}. (op \<bullet> (f b - f a) \<circ> f) b - (op \<bullet> (f b - f a) \<circ> f) a = (f b - f a) \<bullet> f' x (b - a)"
+  have "\<exists>x\<in>{a<..<b}. (f b - f a) \<bullet> f b - (f b - f a) \<bullet> f a = (f b - f a) \<bullet> f' x (b - a)"
     apply (rule mvt)
     apply (rule assms(1))
-    apply (rule continuous_on_inner continuous_on_intros assms(2) ballI)+
-    unfolding o_def
-    apply (rule has_derivative_inner_right)
+    apply (intro continuous_on_intros assms(2))
     using assms(3)
-    apply auto
+    apply (fast intro: has_derivative_inner_right)
     done
   then obtain x where x:
     "x \<in> {a<..<b}"
-    "(op \<bullet> (f b - f a) \<circ> f) b - (op \<bullet> (f b - f a) \<circ> f) a = (f b - f a) \<bullet> f' x (b - a)" ..
+    "(f b - f a) \<bullet> f b - (f b - f a) \<bullet> f a = (f b - f a) \<bullet> f' x (b - a)" ..
   show ?thesis
   proof (cases "f a = f b")
     case False
@@ -778,9 +778,7 @@
     also have "\<dots> = (f b - f a) \<bullet> (f b - f a)"
       unfolding power2_norm_eq_inner ..
     also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)"
-      using x
-      unfolding inner_simps
-      by (auto simp add: inner_diff_left)
+      using x(2) by (simp only: inner_diff_right)
     also have "\<dots> \<le> norm (f b - f a) * norm (f' x (b - a))"
       by (rule norm_cauchy_schwarz)
     finally show ?thesis