src/HOL/Analysis/Derivative.thy

   shows "vector_derivative f (at x within S) = y"
   using y
   by (intro vector_derivative_unique_within[OF not_bot vector_derivative_works[THEN iffD1] y])
      (auto simp: differentiable_def has_vector_derivative_def)
 
+lemma deriv_of_real [simp]: 
+  "at x within A \<noteq> bot \<Longrightarrow> vector_derivative of_real (at x within A) = 1"
+  by (auto intro!: vector_derivative_within derivative_eq_intros)
+
 lemma frechet_derivative_eq_vector_derivative:
   assumes "f differentiable (at x)"
     shows  "(frechet_derivative f (at x)) = (\<lambda>r. r *\<^sub>R vector_derivative f (at x))"
 using assms
 by (auto simp: differentiable_iff_scaleR vector_derivative_def has_vector_derivative_def

   apply (cases "at x within S \<noteq> bot")
   apply (intro refl conj_cong filterlim_cong)
   apply (auto simp: Lim_ident_at eventually_at_filter elim: eventually_mono)
   done
 
+lemma vector_derivative_cong_eq:
+  assumes "eventually (\<lambda>x. x \<in> A \<longrightarrow> f x = g x) (nhds x)" "x = y" "A = B" "x \<in> A"
+  shows   "vector_derivative f (at x within A) = vector_derivative g (at y within B)"
+proof -
+  have "f x = g x"
+    using assms eventually_nhds_x_imp_x by blast
+  hence "(\<lambda>D. (f has_vector_derivative D) (at x within A)) = 
+           (\<lambda>D. (g has_vector_derivative D) (at x within A))" using assms
+    by (intro ext has_vector_derivative_cong_ev refl assms) simp_all
+  thus ?thesis by (simp add: vector_derivative_def assms)
+qed
+  
 lemma islimpt_closure_open:
   fixes s :: "'a::perfect_space set"
   assumes "open s" and t: "t = closure s" "x \<in> t"
   shows "x islimpt t"
 proof cases

 lemma DERIV_deriv_iff_real_differentiable:
   fixes x :: real
   shows "DERIV f x :> deriv f x \<longleftrightarrow> f differentiable at x"
   unfolding differentiable_def by (metis DERIV_imp_deriv has_real_derivative_iff)
 
+lemma DERIV_deriv_iff_field_differentiable:
+  "DERIV f x :> deriv f x \<longleftrightarrow> f field_differentiable at x"
+  unfolding field_differentiable_def by (metis DERIV_imp_deriv)
+
+lemma vector_derivative_of_real_left:
+  assumes "f differentiable at x"
+  shows   "vector_derivative (\<lambda>x. of_real (f x)) (at x) = of_real (deriv f x)"
+  by (metis DERIV_deriv_iff_real_differentiable assms has_vector_derivative_of_real vector_derivative_at)
+  
+lemma vector_derivative_of_real_right:
+  assumes "f field_differentiable at (of_real x)"
+  shows   "vector_derivative (\<lambda>x. f (of_real x)) (at x) = deriv f (of_real x)"
+  by (metis DERIV_deriv_iff_field_differentiable assms has_vector_derivative_real_field vector_derivative_at)
+  
 lemma deriv_cong_ev:
   assumes "eventually (\<lambda>x. f x = g x) (nhds x)" "x = y"
   shows   "deriv f x = deriv g y"
 proof -
   have "(\<lambda>D. (f has_field_derivative D) (at x)) = (\<lambda>D. (g has_field_derivative D) (at y))"

       by (simp add: eventually_eventually)
     hence "eventually (\<lambda>x. deriv f x = deriv g x) (nhds x)"
       by eventually_elim (rule deriv_cong_ev, simp_all)
     thus ?case by (auto intro!: deriv_cong_ev Suc simp: funpow_Suc_right simp del: funpow.simps)
   qed auto
-  from eventually_nhds_x_imp_x[OF this] assms(2) show ?thesis by simp
+  with \<open>x = y\<close> eventually_nhds_x_imp_x show ?thesis by blast 
 qed
 
 lemma real_derivative_chain:
   fixes x :: real
   shows "f differentiable at x \<Longrightarrow> g differentiable at (f x)

 lemma vector_derivative_chain_at_general:
   assumes "f differentiable at x" "g field_differentiable at (f x)"
   shows "vector_derivative (g \<circ> f) (at x) = vector_derivative f (at x) * deriv g (f x)"
   apply (rule vector_derivative_at [OF field_vector_diff_chain_at])
   using assms vector_derivative_works by (auto simp: field_differentiable_derivI)
-
-lemma DERIV_deriv_iff_field_differentiable:
-  "DERIV f x :> deriv f x \<longleftrightarrow> f field_differentiable at x"
-  unfolding field_differentiable_def by (metis DERIV_imp_deriv)
 
 lemma deriv_chain:
   "f field_differentiable at x \<Longrightarrow> g field_differentiable at (f x)
     \<Longrightarrow> deriv (g o f) x = deriv g (f x) * deriv f x"
   by (metis DERIV_deriv_iff_field_differentiable DERIV_chain DERIV_imp_deriv)