src/HOL/Deriv.thy

   by (auto simp: has_field_derivative_def ac_simps)
 
 
 subsection \<open>Vector derivative\<close>
 
-lemma has_field_derivative_iff_has_vector_derivative:
-  "(f has_field_derivative y) F \<longleftrightarrow> (f has_vector_derivative y) F"
+text \<open>It's for real derivatives only, and not obviously generalisable to field derivatives\<close>
+lemma has_real_derivative_iff_has_vector_derivative:
+  "(f has_real_derivative y) F \<longleftrightarrow> (f has_vector_derivative y) F"
   unfolding has_vector_derivative_def has_field_derivative_def real_scaleR_def mult_commute_abs ..
 
 lemma has_field_derivative_subset:
   "(f has_field_derivative y) (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow>
     (f has_field_derivative y) (at x within t)"
-  unfolding has_field_derivative_def by (rule has_derivative_subset)
+  by (fact DERIV_subset)
 
 lemma has_vector_derivative_const[simp, derivative_intros]: "((\<lambda>x. c) has_vector_derivative 0) net"
   by (auto simp: has_vector_derivative_def)
 
 lemma has_vector_derivative_id[simp, derivative_intros]: "((\<lambda>x. x) has_vector_derivative 1) net"

   by (simp add: has_vector_derivative_def scaleR_right scaleR_left scaleR_right_distrib)
 
 lemma has_vector_derivative_scaleR[derivative_intros]:
   "(f has_field_derivative f') (at x within s) \<Longrightarrow> (g has_vector_derivative g') (at x within s) \<Longrightarrow>
     ((\<lambda>x. f x *\<^sub>R g x) has_vector_derivative (f x *\<^sub>R g' + f' *\<^sub>R g x)) (at x within s)"
-  unfolding has_field_derivative_iff_has_vector_derivative
+  unfolding has_real_derivative_iff_has_vector_derivative
   by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_scaleR])
 
 lemma has_vector_derivative_mult[derivative_intros]:
   "(f has_vector_derivative f') (at x within s) \<Longrightarrow> (g has_vector_derivative g') (at x within s) \<Longrightarrow>
     ((\<lambda>x. f x * g x) has_vector_derivative (f x * g' + f' * g x)) (at x within s)"

   by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_mult])
 
 lemma has_vector_derivative_of_real[derivative_intros]:
   "(f has_field_derivative D) F \<Longrightarrow> ((\<lambda>x. of_real (f x)) has_vector_derivative (of_real D)) F"
   by (rule bounded_linear.has_vector_derivative[OF bounded_linear_of_real])
-    (simp add: has_field_derivative_iff_has_vector_derivative)
+    (simp add: has_real_derivative_iff_has_vector_derivative)
 
 lemma has_vector_derivative_real_field:
   "(f has_field_derivative f') (at (of_real a)) \<Longrightarrow> ((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a within s)"
   using has_derivative_compose[of of_real of_real a _ f "(*) f'"] 
   by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def)