src/HOL/Multivariate_Analysis/Derivative.thy

   show ?l unfolding deriv_def LIM_def apply safe apply(drule as,safe)
     apply(rule_tac x=d in exI,safe) apply(erule_tac x="xa + x" in allE)
     unfolding dist_norm diff_0_right norm_scaleR
     unfolding dist_norm netlimit_at[of x] by(auto simp add:algebra_simps *) qed
 
-lemma FDERIV_conv_has_derivative:"FDERIV f (x::'a::{real_normed_vector,perfect_space}) :> f' = (f has_derivative f') (at x)" (is "?l = ?r") proof 
+lemma netlimit_at_vector:
+  fixes a :: "'a::real_normed_vector"
+  shows "netlimit (at a) = a"
+proof (cases "\<exists>x. x \<noteq> a")
+  case True then obtain x where x: "x \<noteq> a" ..
+  have "\<not> trivial_limit (at a)"
+    unfolding trivial_limit_def eventually_at dist_norm
+    apply clarsimp
+    apply (rule_tac x="a + scaleR (d / 2) (sgn (x - a))" in exI)
+    apply (simp add: norm_sgn sgn_zero_iff x)
+    done
+  thus ?thesis
+    by (rule netlimit_within [of a UNIV, unfolded within_UNIV])
+qed simp
+
+lemma FDERIV_conv_has_derivative:
+  shows "FDERIV f x :> f' = (f has_derivative f') (at x)" (is "?l = ?r")
+proof
   assume ?l note as = this[unfolded fderiv_def]
   show ?r unfolding has_derivative_def Lim_at apply-apply(rule,rule as[THEN conjunct1]) proof(rule,rule)
     fix e::real assume "e>0"
     guess d using as[THEN conjunct2,unfolded LIM_def,rule_format,OF`e>0`] ..
     thus "\<exists>d>0. \<forall>xa. 0 < dist xa x \<and> dist xa x < d \<longrightarrow>
       dist ((1 / norm (xa - netlimit (at x))) *\<^sub>R (f xa - (f (netlimit (at x)) + f' (xa - netlimit (at x))))) (0) < e"
       apply(rule_tac x=d in exI) apply(erule conjE,rule,assumption) apply rule apply(erule_tac x="xa - x" in allE)
-      unfolding dist_norm netlimit_at[of x] by (auto simp add: diff_diff_eq) qed next
+      unfolding dist_norm netlimit_at_vector[of x] by (auto simp add: diff_diff_eq) qed next
   assume ?r note as = this[unfolded has_derivative_def]
   show ?l unfolding fderiv_def LIM_def apply-apply(rule,rule as[THEN conjunct1]) proof(rule,rule)
     fix e::real assume "e>0"
     guess d using as[THEN conjunct2,unfolded Lim_at,rule_format,OF`e>0`] ..
     thus "\<exists>s>0. \<forall>xa. xa \<noteq> 0 \<and> dist xa 0 < s \<longrightarrow> dist (norm (f (x + xa) - f x - f' xa) / norm xa) 0 < e" apply-
       apply(rule_tac x=d in exI) apply(erule conjE,rule,assumption) apply rule apply(erule_tac x="xa + x" in allE)
-      unfolding dist_norm netlimit_at[of x] by (auto simp add: diff_diff_eq add.commute) qed qed
+      unfolding dist_norm netlimit_at_vector[of x] by (auto simp add: diff_diff_eq add.commute) qed qed
 
 subsection {* These are the only cases we'll care about, probably. *}
 
 lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow>
          bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x within s)"

 lemma has_derivative_at_within: "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f') (at x within s)"
   unfolding has_derivative_within' has_derivative_at' by meson
 
 lemma has_derivative_within_open:
   "a \<in> s \<Longrightarrow> open s \<Longrightarrow> ((f has_derivative f') (at a within s) \<longleftrightarrow> (f has_derivative f') (at a))"
-  unfolding has_derivative_within has_derivative_at using Lim_within_open by auto
+  by (simp only: at_within_interior interior_open)
 
 lemma bounded_linear_imp_linear: "bounded_linear f \<Longrightarrow> linear f" (* TODO: move elsewhere *)
 proof -
   assume "bounded_linear f"
   then interpret f: bounded_linear f .

 lemma differentiable_at_withinI: "f differentiable (at x) \<Longrightarrow> f differentiable (at x within s)"
   unfolding differentiable_def using has_derivative_at_within by blast
 
 lemma differentiable_within_open: assumes "a \<in> s" "open s" shows 
   "f differentiable (at a within s) \<longleftrightarrow> (f differentiable (at a))"
-  unfolding differentiable_def has_derivative_within_open[OF assms] by auto
+  using assms by (simp only: at_within_interior interior_open)
 
 lemma differentiable_on_eq_differentiable_at: "open s \<Longrightarrow> (f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable at x))"
   unfolding differentiable_on_def by(auto simp add: differentiable_within_open)
 
 lemma differentiable_transform_within:

 lemma differentiable_chain_within:
   "f differentiable (at x within s) \<Longrightarrow> g differentiable (at(f x) within (f ` s))
    \<Longrightarrow> (g o f) differentiable (at x within s)"
   unfolding differentiable_def by(meson diff_chain_within)
 
-subsection {* Uniqueness of derivative.                                                 *)
-(*                                                                           *)
-(* The general result is a bit messy because we need approachability of the  *)
-(* limit point from any direction. But OK for nontrivial intervals etc. *}
+subsection {* Uniqueness of derivative *}
+
+text {*
+ The general result is a bit messy because we need approachability of the
+ limit point from any direction. But OK for nontrivial intervals etc.
+*}
     
 lemma frechet_derivative_unique_within: fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes "(f has_derivative f') (at x within s)" "(f has_derivative f'') (at x within s)"
   "(\<forall>i<DIM('a). \<forall>e>0. \<exists>d. 0 < abs(d) \<and> abs(d) < e \<and> (x + d *\<^sub>R basis i) \<in> s)" shows "f' = f''" proof-
   note as = assms(1,2)[unfolded has_derivative_def]

     also have "\<dots> = e" unfolding e_def using c[THEN conjunct1] using norm_minus_cancel[of "f' (basis i) - f'' (basis i)"] by (auto simp add: add.commute ab_diff_minus)
     finally show False using c using d[THEN conjunct2,rule_format,of "x + c *\<^sub>R basis i"] 
       unfolding dist_norm unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff
         scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib using i by auto qed qed
 
-lemma frechet_derivative_unique_at: fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
+lemma frechet_derivative_unique_at:
   shows "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f'') (at x) \<Longrightarrow> f' = f''"
-  apply(rule frechet_derivative_unique_within[of f f' x UNIV f'']) unfolding within_UNIV apply(assumption)+
-  apply(rule,rule,rule,rule) apply(rule_tac x="e/2" in exI) by auto
+  unfolding FDERIV_conv_has_derivative [symmetric]
+  by (rule FDERIV_unique)
  
 lemma "isCont f x = continuous (at x) f" unfolding isCont_def LIM_def
   unfolding continuous_at Lim_at unfolding dist_nz by auto
 
 lemma frechet_derivative_unique_within_closed_interval: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"

     by (simp add: at_within_interior interior_open open_interval)
   from assms(2,3) [unfolded *] show "f' = f''"
     by (rule frechet_derivative_unique_at)
 qed
 
-lemma frechet_derivative_at: fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
+lemma frechet_derivative_at:
   shows "(f has_derivative f') (at x) \<Longrightarrow> (f' = frechet_derivative f (at x))"
   apply(rule frechet_derivative_unique_at[of f],assumption)
   unfolding frechet_derivative_works[THEN sym] using differentiable_def by auto
 
 lemma frechet_derivative_within_closed_interval: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"

   thus ?r unfolding vector_derivative_def has_vector_derivative_def
     apply-apply(rule someI_ex,rule_tac x="f' 1" in exI)
     using f' unfolding scaleR[THEN sym] by auto
 next assume ?r thus ?l  unfolding vector_derivative_def has_vector_derivative_def differentiable_def by auto qed
 
-lemma vector_derivative_unique_at: fixes f::"real\<Rightarrow> 'n::euclidean_space"
-  assumes "(f has_vector_derivative f') (at x)" "(f has_vector_derivative f'') (at x)" shows "f' = f''" proof-
-  have *:"(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')" apply(rule frechet_derivative_unique_at)
-    using assms[unfolded has_vector_derivative_def] by auto
-  show ?thesis proof(rule ccontr) assume "f' \<noteq> f''" moreover
-    hence "(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')" using * by auto
-    ultimately show False unfolding expand_fun_eq by auto qed qed
+lemma vector_derivative_unique_at:
+  assumes "(f has_vector_derivative f') (at x)"
+  assumes "(f has_vector_derivative f'') (at x)"
+  shows "f' = f''"
+proof-
+  have "(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')"
+    using assms [unfolded has_vector_derivative_def]
+    by (rule frechet_derivative_unique_at)
+  thus ?thesis unfolding expand_fun_eq by auto
+qed
 
 lemma vector_derivative_unique_within_closed_interval: fixes f::"real \<Rightarrow> 'n::ordered_euclidean_space"
   assumes "a < b" "x \<in> {a..b}"
   "(f has_vector_derivative f') (at x within {a..b})"
   "(f has_vector_derivative f'') (at x within {a..b})" shows "f' = f''" proof-

     using assms(3-)[unfolded has_vector_derivative_def] using assms(1-2) by auto
   show ?thesis proof(rule ccontr) assume "f' \<noteq> f''" moreover
     hence "(\<lambda>x. x *\<^sub>R f') 1 = (\<lambda>x. x *\<^sub>R f'') 1" using * by (auto simp: expand_fun_eq)
     ultimately show False unfolding o_def by auto qed qed
 
-lemma vector_derivative_at: fixes f::"real \<Rightarrow> 'a::euclidean_space" shows
- "(f has_vector_derivative f') (at x) \<Longrightarrow> vector_derivative f (at x) = f'"
+lemma vector_derivative_at:
+  shows "(f has_vector_derivative f') (at x) \<Longrightarrow> vector_derivative f (at x) = f'"
   apply(rule vector_derivative_unique_at) defer apply assumption
   unfolding vector_derivative_works[THEN sym] differentiable_def
   unfolding has_vector_derivative_def by auto
 
 lemma vector_derivative_within_closed_interval: fixes f::"real \<Rightarrow> 'a::ordered_euclidean_space"