src/HOL/Deriv.thy

 text {*
   Usually the filter @{term F} is @{term "at x within s"}.  @{term "(f has_derivative D)
   (at x within s)"} means: @{term D} is the derivative of function @{term f} at point @{term x}
   within the set @{term s}. Where @{term s} is used to express left or right sided derivatives. In
   most cases @{term s} is either a variable or @{term UNIV}.
+*}
+
+lemma has_derivative_eq_rhs: "(f has_derivative f') F \<Longrightarrow> f' = g' \<Longrightarrow> (f has_derivative g') F"
+  by simp
+
+definition 
+  has_field_derivative :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a filter \<Rightarrow> bool"
+  (infix "(has'_field'_derivative)" 50)
+where
+  "(f has_field_derivative D) F \<longleftrightarrow> (f has_derivative op * D) F"
+
+lemma DERIV_cong: "(f has_field_derivative X) F \<Longrightarrow> X = Y \<Longrightarrow> (f has_field_derivative Y) F"
+  by simp
+
+definition
+  has_vector_derivative :: "(real \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'b \<Rightarrow> real filter \<Rightarrow> bool"
+  (infix "has'_vector'_derivative" 50)
+where
+  "(f has_vector_derivative f') net \<longleftrightarrow> (f has_derivative (\<lambda>x. x *\<^sub>R f')) net"
+
+lemma has_vector_derivative_eq_rhs: "(f has_vector_derivative X) F \<Longrightarrow> X = Y \<Longrightarrow> (f has_vector_derivative Y) F"
+  by simp
+
+ML {*
+
+structure Derivative_Intros = Named_Thms
+(
+  val name = @{binding derivative_intros}
+  val description = "structural introduction rules for derivatives"
+)
+
+*}
+
+setup {*
+  let
+    val eq_thms = [@{thm has_derivative_eq_rhs}, @{thm DERIV_cong}, @{thm has_vector_derivative_eq_rhs}]
+    fun eq_rule thm = get_first (try (fn eq_thm => eq_thm OF [thm])) eq_thms
+  in
+    Derivative_Intros.setup #>
+    Global_Theory.add_thms_dynamic
+      (@{binding derivative_eq_intros}, map_filter eq_rule o Derivative_Intros.get o Context.proof_of)
+  end;
 *}
 
 text {*
   The following syntax is only used as a legacy syntax.
 *}

   FDERIV :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow>  ('a \<Rightarrow> 'b) \<Rightarrow> bool"
   ("(FDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
 where
   "FDERIV f x :> f' \<equiv> (f has_derivative f') (at x)"
 
-
-lemma has_derivative_eq_rhs: "(f has_derivative f') F \<Longrightarrow> f' = g' \<Longrightarrow> (f has_derivative g') F"
-  by simp
-
-ML {*
-
-structure has_derivative_Intros = Named_Thms
-(
-  val name = @{binding has_derivative_intros}
-  val description = "introduction rules for FDERIV"
-)
-
-*}
-
-setup {*
-  has_derivative_Intros.setup #>
-  Global_Theory.add_thms_dynamic (@{binding has_derivative_eq_intros},
-    map_filter (try (fn thm => @{thm has_derivative_eq_rhs} OF [thm])) o has_derivative_Intros.get o Context.proof_of);
-*}
-
 lemma has_derivative_bounded_linear: "(f has_derivative f') F \<Longrightarrow> bounded_linear f'"
   by (simp add: has_derivative_def)
 
 lemma has_derivative_linear: "(f has_derivative f') F \<Longrightarrow> linear f'"
   using bounded_linear.linear[OF has_derivative_bounded_linear] .
 
-lemma has_derivative_ident[has_derivative_intros, simp]: "((\<lambda>x. x) has_derivative (\<lambda>x. x)) F"
+lemma has_derivative_ident[derivative_intros, simp]: "((\<lambda>x. x) has_derivative (\<lambda>x. x)) F"
   by (simp add: has_derivative_def tendsto_const)
 
-lemma has_derivative_const[has_derivative_intros, simp]: "((\<lambda>x. c) has_derivative (\<lambda>x. 0)) F"
+lemma has_derivative_const[derivative_intros, simp]: "((\<lambda>x. c) has_derivative (\<lambda>x. 0)) F"
   by (simp add: has_derivative_def tendsto_const)
 
 lemma (in bounded_linear) bounded_linear: "bounded_linear f" ..
 
 lemma (in bounded_linear) has_derivative:

   apply (erule bounded_linear_compose [OF bounded_linear])
   apply (drule tendsto)
   apply (simp add: scaleR diff add zero)
   done
 
-lemmas has_derivative_scaleR_right [has_derivative_intros] =
+lemmas has_derivative_scaleR_right [derivative_intros] =
   bounded_linear.has_derivative [OF bounded_linear_scaleR_right]
 
-lemmas has_derivative_scaleR_left [has_derivative_intros] =
+lemmas has_derivative_scaleR_left [derivative_intros] =
   bounded_linear.has_derivative [OF bounded_linear_scaleR_left]
 
-lemmas has_derivative_mult_right [has_derivative_intros] =
+lemmas has_derivative_mult_right [derivative_intros] =
   bounded_linear.has_derivative [OF bounded_linear_mult_right]
 
-lemmas has_derivative_mult_left [has_derivative_intros] =
+lemmas has_derivative_mult_left [derivative_intros] =
   bounded_linear.has_derivative [OF bounded_linear_mult_left]
 
-lemma has_derivative_add[simp, has_derivative_intros]:
+lemma has_derivative_add[simp, derivative_intros]:
   assumes f: "(f has_derivative f') F" and g: "(g has_derivative g') F"
   shows "((\<lambda>x. f x + g x) has_derivative (\<lambda>x. f' x + g' x)) F"
   unfolding has_derivative_def
 proof safe
   let ?x = "Lim F (\<lambda>x. x)"

     using f g by (intro tendsto_add) (auto simp: has_derivative_def)
   then show "(?D (\<lambda>x. f x + g x) (\<lambda>x. f' x + g' x) ---> 0) F"
     by (simp add: field_simps scaleR_add_right scaleR_diff_right)
 qed (blast intro: bounded_linear_add f g has_derivative_bounded_linear)
 
-lemma has_derivative_setsum[simp, has_derivative_intros]:
+lemma has_derivative_setsum[simp, derivative_intros]:
   assumes f: "\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) F"
   shows "((\<lambda>x. \<Sum>i\<in>I. f i x) has_derivative (\<lambda>x. \<Sum>i\<in>I. f' i x)) F"
 proof cases
   assume "finite I" from this f show ?thesis
     by induct (simp_all add: f)
 qed simp
 
-lemma has_derivative_minus[simp, has_derivative_intros]: "(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. - f x) has_derivative (\<lambda>x. - f' x)) F"
+lemma has_derivative_minus[simp, derivative_intros]: "(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. - f x) has_derivative (\<lambda>x. - f' x)) F"
   using has_derivative_scaleR_right[of f f' F "-1"] by simp
 
-lemma has_derivative_diff[simp, has_derivative_intros]:
+lemma has_derivative_diff[simp, derivative_intros]:
   "(f has_derivative f') F \<Longrightarrow> (g has_derivative g') F \<Longrightarrow> ((\<lambda>x. f x - g x) has_derivative (\<lambda>x. f' x - g' x)) F"
   by (simp only: diff_conv_add_uminus has_derivative_add has_derivative_minus)
 
 lemma has_derivative_at_within:
   "(f has_derivative f') (at x within s) \<longleftrightarrow>

       by (simp add: add_divide_distrib Ng_def Nf_def)
     finally show "?fun1 y \<le> ?fun2 y" .
   qed simp
 qed
 
-lemmas has_derivative_mult[simp, has_derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_mult]
-lemmas has_derivative_scaleR[simp, has_derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_scaleR]
-
-lemma has_derivative_setprod[simp, has_derivative_intros]:
+lemmas has_derivative_mult[simp, derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_mult]
+lemmas has_derivative_scaleR[simp, derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_scaleR]
+
+lemma has_derivative_setprod[simp, derivative_intros]:
   fixes f :: "'i \<Rightarrow> 'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
   assumes f: "\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) (at x within s)"
   shows "((\<lambda>x. \<Prod>i\<in>I. f i x) has_derivative (\<lambda>y. \<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {i}. f j x))) (at x within s)"
 proof cases
   assume "finite I" from this f show ?thesis

     finally show ?case
       using insert by simp
   qed simp  
 qed simp
 
-lemma has_derivative_power[simp, has_derivative_intros]:
+lemma has_derivative_power[simp, derivative_intros]:
   fixes f :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
   assumes f: "(f has_derivative f') (at x within s)"
   shows "((\<lambda>x. f x^n) has_derivative (\<lambda>y. of_nat n * f' y * f x^(n - 1))) (at x within s)"
   using has_derivative_setprod[OF f, of "{..< n}"] by (simp add: setprod_constant ac_simps)
 

     by simp
   finally show "norm (?inv y - ?inv x - ?f (y -x)) / norm (y - x) \<le>
       norm (?inv y - ?inv x) * norm (?inv x)" .
 qed
 
-lemma has_derivative_inverse[simp, has_derivative_intros]:
+lemma has_derivative_inverse[simp, derivative_intros]:
   fixes f :: "_ \<Rightarrow> 'a::real_normed_div_algebra"
   assumes x:  "f x \<noteq> 0" and f: "(f has_derivative f') (at x within s)"
   shows "((\<lambda>x. inverse (f x)) has_derivative (\<lambda>h. - (inverse (f x) * f' h * inverse (f x)))) (at x within s)"
   using has_derivative_compose[OF f has_derivative_inverse', OF x] .
 
-lemma has_derivative_divide[simp, has_derivative_intros]:
+lemma has_derivative_divide[simp, derivative_intros]:
   fixes f :: "_ \<Rightarrow> 'a::real_normed_div_algebra"
   assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)" 
   assumes x: "g x \<noteq> 0"
   shows "((\<lambda>x. f x / g x) has_derivative
                 (\<lambda>h. - f x * (inverse (g x) * g' h * inverse (g x)) + f' h / g x)) (at x within s)"
   using has_derivative_mult[OF f has_derivative_inverse[OF x g]]
   by (simp add: divide_inverse field_simps)
 
 text{*Conventional form requires mult-AC laws. Types real and complex only.*}
 
-lemma has_derivative_divide'[has_derivative_intros]: 
+lemma has_derivative_divide'[derivative_intros]: 
   fixes f :: "_ \<Rightarrow> 'a::real_normed_field"
   assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)" and x: "g x \<noteq> 0"
   shows "((\<lambda>x. f x / g x) has_derivative (\<lambda>h. (f' h * g x - f x * g' h) / (g x * g x))) (at x within s)"
 proof -
   { fix h

 lemma differentiable_subset: "f differentiable (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f differentiable (at x within t)"
   unfolding differentiable_def by (blast intro: has_derivative_subset)
 
 lemmas differentiable_within_subset = differentiable_subset
 
-lemma differentiable_ident [simp]: "(\<lambda>x. x) differentiable F"
+lemma differentiable_ident [simp, derivative_intros]: "(\<lambda>x. x) differentiable F"
   unfolding differentiable_def by (blast intro: has_derivative_ident)
 
-lemma differentiable_const [simp]: "(\<lambda>z. a) differentiable F"
+lemma differentiable_const [simp, derivative_intros]: "(\<lambda>z. a) differentiable F"
   unfolding differentiable_def by (blast intro: has_derivative_const)
 
 lemma differentiable_in_compose:
   "f differentiable (at (g x) within (g`s)) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> (\<lambda>x. f (g x)) differentiable (at x within s)"
   unfolding differentiable_def by (blast intro: has_derivative_in_compose)
 
 lemma differentiable_compose:
   "f differentiable (at (g x)) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> (\<lambda>x. f (g x)) differentiable (at x within s)"
   by (blast intro: differentiable_in_compose differentiable_subset)
 
-lemma differentiable_sum [simp]:
+lemma differentiable_sum [simp, derivative_intros]:
   "f differentiable F \<Longrightarrow> g differentiable F \<Longrightarrow> (\<lambda>x. f x + g x) differentiable F"
   unfolding differentiable_def by (blast intro: has_derivative_add)
 
-lemma differentiable_minus [simp]:
+lemma differentiable_minus [simp, derivative_intros]:
   "f differentiable F \<Longrightarrow> (\<lambda>x. - f x) differentiable F"
   unfolding differentiable_def by (blast intro: has_derivative_minus)
 
-lemma differentiable_diff [simp]:
+lemma differentiable_diff [simp, derivative_intros]:
   "f differentiable F \<Longrightarrow> g differentiable F \<Longrightarrow> (\<lambda>x. f x - g x) differentiable F"
   unfolding differentiable_def by (blast intro: has_derivative_diff)
 
-lemma differentiable_mult [simp]:
+lemma differentiable_mult [simp, derivative_intros]:
   fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_algebra"
   shows "f differentiable (at x within s) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> (\<lambda>x. f x * g x) differentiable (at x within s)"
   unfolding differentiable_def by (blast intro: has_derivative_mult)
 
-lemma differentiable_inverse [simp]:
+lemma differentiable_inverse [simp, derivative_intros]:
   fixes f :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
   shows "f differentiable (at x within s) \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> (\<lambda>x. inverse (f x)) differentiable (at x within s)"
   unfolding differentiable_def by (blast intro: has_derivative_inverse)
 
-lemma differentiable_divide [simp]:
+lemma differentiable_divide [simp, derivative_intros]:
   fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
   shows "f differentiable (at x within s) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x / g x) differentiable (at x within s)"
   unfolding divide_inverse using assms by simp
 
-lemma differentiable_power [simp]:
+lemma differentiable_power [simp, derivative_intros]:
   fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
   shows "f differentiable (at x within s) \<Longrightarrow> (\<lambda>x. f x ^ n) differentiable (at x within s)"
   unfolding differentiable_def by (blast intro: has_derivative_power)
 
-lemma differentiable_scaleR [simp]:
+lemma differentiable_scaleR [simp, derivative_intros]:
   "f differentiable (at x within s) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> (\<lambda>x. f x *\<^sub>R g x) differentiable (at x within s)"
   unfolding differentiable_def by (blast intro: has_derivative_scaleR)
-
-definition 
-  has_field_derivative :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a filter \<Rightarrow> bool"
-  (infix "(has'_field'_derivative)" 50)
-where
-  "(f has_field_derivative D) F \<longleftrightarrow> (f has_derivative op * D) F"
 
 lemma has_derivative_imp_has_field_derivative:
   "(f has_derivative D) F \<Longrightarrow> (\<And>x. x * D' = D x) \<Longrightarrow> (f has_field_derivative D') F"
   unfolding has_field_derivative_def 
   by (rule has_derivative_eq_rhs[of f D]) (simp_all add: fun_eq_iff mult_commute)

   "(f has_field_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s 
    \<Longrightarrow> (f has_field_derivative f') (at x within t)"
   by (simp add: has_field_derivative_def has_derivative_within_subset)
 
 abbreviation (input)
-  deriv :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+  DERIV :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
   ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
 where
   "DERIV f x :> D \<equiv> (f has_field_derivative D) (at x)"
 
 abbreviation 

   by (auto elim: real_differentiableE)
 
 lemma differentiableI: "(f has_real_derivative D) (at x within s) \<Longrightarrow> f differentiable (at x within s)"
   by (force simp add: real_differentiable_def)
 
-lemma deriv_def:
-  "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
+lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
   apply (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right LIM_zero_iff[symmetric, of _ D])
   apply (subst (2) tendsto_norm_zero_iff[symmetric])
   apply (rule filterlim_cong)
   apply (simp_all add: eventually_at_filter field_simps nonzero_norm_divide)
   done

   by (simp add: fun_eq_iff mult_commute)
 
 subsection {* Derivatives *}
 
 lemma DERIV_D: "DERIV f x :> D \<Longrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
-  by (simp add: deriv_def)
-
-lemma DERIV_const [simp]: "((\<lambda>x. k) has_field_derivative 0) (at x within s)"
+  by (simp add: DERIV_def)
+
+lemma DERIV_const [simp, derivative_intros]: "((\<lambda>x. k) has_field_derivative 0) F"
   by (rule has_derivative_imp_has_field_derivative[OF has_derivative_const]) auto
 
-lemma DERIV_ident [simp]: "((\<lambda>x. x) has_field_derivative 1) (at x within s)"
+lemma DERIV_ident [simp, derivative_intros]: "((\<lambda>x. x) has_field_derivative 1) F"
   by (rule has_derivative_imp_has_field_derivative[OF has_derivative_ident]) auto
 
-lemma field_differentiable_add:
-  assumes "(f has_field_derivative f') F" "(g has_field_derivative g') F"
-    shows "((\<lambda>z. f z + g z) has_field_derivative f' + g') F"
-  apply (rule has_derivative_imp_has_field_derivative[OF has_derivative_add])
-  using assms 
-  by (auto simp: has_field_derivative_def field_simps mult_commute_abs)
+lemma field_differentiable_add[derivative_intros]:
+  "(f has_field_derivative f') F \<Longrightarrow> (g has_field_derivative g') F \<Longrightarrow> 
+    ((\<lambda>z. f z + g z) has_field_derivative f' + g') F"
+  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_add])
+     (auto simp: has_field_derivative_def field_simps mult_commute_abs)
 
 corollary DERIV_add:
   "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
   ((\<lambda>x. f x + g x) has_field_derivative D + E) (at x within s)"
   by (rule field_differentiable_add)
 
-lemma field_differentiable_minus:
-  assumes "(f has_field_derivative f') F" 
-    shows "((\<lambda>z. - (f z)) has_field_derivative -f') F"
-  apply (rule has_derivative_imp_has_field_derivative[OF has_derivative_minus])
-  using assms 
-  by (auto simp: has_field_derivative_def field_simps mult_commute_abs)
+lemma field_differentiable_minus[derivative_intros]:
+  "(f has_field_derivative f') F \<Longrightarrow> ((\<lambda>z. - (f z)) has_field_derivative -f') F"
+  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_minus])
+     (auto simp: has_field_derivative_def field_simps mult_commute_abs)
 
 corollary DERIV_minus: "(f has_field_derivative D) (at x within s) \<Longrightarrow> ((\<lambda>x. - f x) has_field_derivative -D) (at x within s)"
   by (rule field_differentiable_minus)
 
-lemma field_differentiable_diff:
-  assumes "(f has_field_derivative f') F" "(g has_field_derivative g') F"
-    shows "((\<lambda>z. f z - g z) has_field_derivative f' - g') F"
-by (simp only: assms diff_conv_add_uminus field_differentiable_add field_differentiable_minus)
+lemma field_differentiable_diff[derivative_intros]:
+  "(f has_field_derivative f') F \<Longrightarrow> (g has_field_derivative g') F \<Longrightarrow> ((\<lambda>z. f z - g z) has_field_derivative f' - g') F"
+  by (simp only: assms diff_conv_add_uminus field_differentiable_add field_differentiable_minus)
 
 corollary DERIV_diff:
   "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
   ((\<lambda>x. f x - g x) has_field_derivative D - E) (at x within s)"
   by (rule field_differentiable_diff)

   "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
   ((\<lambda>x. f x * g x) has_field_derivative f x * E + D * g x) (at x within s)"
   by (rule has_derivative_imp_has_field_derivative[OF has_derivative_mult])
      (auto simp: field_simps mult_commute_abs dest: has_field_derivative_imp_has_derivative)
 
-lemma DERIV_mult:
+lemma DERIV_mult[derivative_intros]:
   "(f has_field_derivative Da) (at x within s) \<Longrightarrow> (g has_field_derivative Db) (at x within s) \<Longrightarrow>
   ((\<lambda>x. f x * g x) has_field_derivative Da * g x + Db * f x) (at x within s)"
   by (rule has_derivative_imp_has_field_derivative[OF has_derivative_mult])
      (auto simp: field_simps dest: has_field_derivative_imp_has_derivative)
 

   "(f has_field_derivative D) (at x within s) ==> ((\<lambda>x. c * f x) has_field_derivative c * D) (at x within s)"
   by (drule DERIV_mult' [OF DERIV_const], simp)
 
 lemma DERIV_cmult_right:
   "(f has_field_derivative D) (at x within s) ==> ((\<lambda>x. f x * c) has_field_derivative D * c) (at x within s)"
-  using DERIV_cmult   by (force simp add: mult_ac)
+  using DERIV_cmult by (force simp add: mult_ac)
 
 lemma DERIV_cmult_Id [simp]: "(op * c has_field_derivative c) (at x within s)"
   by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp)
 
 lemma DERIV_cdivide:
   "(f has_field_derivative D) (at x within s) \<Longrightarrow> ((\<lambda>x. f x / c) has_field_derivative D / c) (at x within s)"
   using DERIV_cmult_right[of f D x s "1 / c"] by simp
 
 lemma DERIV_unique:
   "DERIV f x :> D \<Longrightarrow> DERIV f x :> E \<Longrightarrow> D = E"
-  unfolding deriv_def by (rule LIM_unique) 
-
-lemma DERIV_setsum:
+  unfolding DERIV_def by (rule LIM_unique) 
+
+lemma DERIV_setsum[derivative_intros]:
   "(\<And> n. n \<in> S \<Longrightarrow> ((\<lambda>x. f x n) has_field_derivative (f' x n)) F) \<Longrightarrow> 
     ((\<lambda>x. setsum (f x) S) has_field_derivative setsum (f' x) S) F"
   by (rule has_derivative_imp_has_field_derivative[OF has_derivative_setsum])
      (auto simp: setsum_right_distrib mult_commute_abs dest: has_field_derivative_imp_has_derivative)
 
-lemma DERIV_inverse':
+lemma DERIV_inverse'[derivative_intros]:
   "(f has_field_derivative D) (at x within s) \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow>
   ((\<lambda>x. inverse (f x)) has_field_derivative - (inverse (f x) * D * inverse (f x))) (at x within s)"
   by (rule has_derivative_imp_has_field_derivative[OF has_derivative_inverse])
      (auto dest: has_field_derivative_imp_has_derivative)
 

   ((\<lambda>x. inverse (f x)) has_field_derivative (- (d * inverse(f x ^ Suc (Suc 0))))) (at x within s)"
   by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib)
 
 text {* Derivative of quotient *}
 
-lemma DERIV_divide:
+lemma DERIV_divide[derivative_intros]:
   "(f has_field_derivative D) (at x within s) \<Longrightarrow>
   (g has_field_derivative E) (at x within s) \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow>
   ((\<lambda>x. f x / g x) has_field_derivative (D * g x - f x * E) / (g x * g x)) (at x within s)"
   by (rule has_derivative_imp_has_field_derivative[OF has_derivative_divide])
      (auto dest: has_field_derivative_imp_has_derivative simp: field_simps nonzero_inverse_mult_distrib divide_inverse)

   "(f has_field_derivative D) (at x within s) \<Longrightarrow>
   ((\<lambda>x. f x ^ Suc n) has_field_derivative (1 + of_nat n) * (D * f x ^ n)) (at x within s)"
   by (rule has_derivative_imp_has_field_derivative[OF has_derivative_power])
      (auto simp: has_field_derivative_def)
 
-lemma DERIV_power:
+lemma DERIV_power[derivative_intros]:
   "(f has_field_derivative D) (at x within s) \<Longrightarrow>
   ((\<lambda>x. f x ^ n) has_field_derivative of_nat n * (D * f x ^ (n - Suc 0))) (at x within s)"
   by (rule has_derivative_imp_has_field_derivative[OF has_derivative_power])
      (auto simp: has_field_derivative_def)
 

   assumes "(\<And>x. DERIV g x :> g'(x))"
       and "DERIV f x :> f'" 
     shows "DERIV (\<lambda>x. g(f x)) x :> f' * g'(f x)"
   by (metis UNIV_I DERIV_chain_s [of UNIV] assms)
 
-
-subsubsection {* @{text "DERIV_intros"} *}
-
-ML {*
-structure Deriv_Intros = Named_Thms
-(
-  val name = @{binding DERIV_intros}
-  val description = "DERIV introduction rules"
-)
-*}
-
-setup Deriv_Intros.setup
-
-lemma DERIV_cong: "(f has_field_derivative X) (at x within s) \<Longrightarrow> X = Y \<Longrightarrow> (f has_field_derivative Y) (at x within s)"
-  by simp
-
 declare
-  DERIV_const[THEN DERIV_cong, DERIV_intros]
-  DERIV_ident[THEN DERIV_cong, DERIV_intros]
-  DERIV_add[THEN DERIV_cong, DERIV_intros]
-  DERIV_minus[THEN DERIV_cong, DERIV_intros]
-  DERIV_mult[THEN DERIV_cong, DERIV_intros]
-  DERIV_diff[THEN DERIV_cong, DERIV_intros]
-  DERIV_inverse'[THEN DERIV_cong, DERIV_intros]
-  DERIV_divide[THEN DERIV_cong, DERIV_intros]
-  DERIV_power[where 'a=real, THEN DERIV_cong,
-              unfolded real_of_nat_def[symmetric], DERIV_intros]
-  DERIV_setsum[THEN DERIV_cong, DERIV_intros]
+  DERIV_power[where 'a=real, unfolded real_of_nat_def[symmetric], derivative_intros]
 
 text{*Alternative definition for differentiability*}
 
 lemma DERIV_LIM_iff:
   fixes f :: "'a::{real_normed_vector,inverse} \<Rightarrow> 'a" shows

 apply (drule_tac k="a" in LIM_offset)
 apply (simp add: add_commute)
 done
 
 lemma DERIV_iff2: "(DERIV f x :> D) \<longleftrightarrow> (\<lambda>z. (f z - f x) / (z - x)) --x --> D"
-  by (simp add: deriv_def DERIV_LIM_iff)
+  by (simp add: DERIV_def DERIV_LIM_iff)
 
 lemma DERIV_cong_ev: "x = y \<Longrightarrow> eventually (\<lambda>x. f x = g x) (nhds x) \<Longrightarrow> u = v \<Longrightarrow>
     DERIV f x :> u \<longleftrightarrow> DERIV g y :> v"
   unfolding DERIV_iff2
 proof (rule filterlim_cong)

     by (auto simp: eventually_at_filter elim: eventually_elim1)
 qed simp_all
 
 lemma DERIV_shift:
   "(DERIV f (x + z) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (x + z)) x :> y)"
-  by (simp add: deriv_def field_simps)
+  by (simp add: DERIV_def field_simps)
 
 lemma DERIV_mirror:
   "(DERIV f (- x) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (- x::real) :: real) x :> - y)"
-  by (simp add: deriv_def filterlim_at_split filterlim_at_left_to_right
+  by (simp add: DERIV_def filterlim_at_split filterlim_at_left_to_right
                 tendsto_minus_cancel_left field_simps conj_commute)
 
 text {* Caratheodory formulation of derivative at a point *}
 
 lemma CARAT_DERIV: (*FIXME: SUPERSEDED BY THE ONE IN Deriv.thy. But still used by NSA/HDeriv.thy*)

   show "\<exists>g. (\<forall>z. f z - f x = g z * (z-x)) \<and> isCont g x \<and> g x = l"
   proof (intro exI conjI)
     let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
     show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
     show "isCont ?g x" using der
-      by (simp add: isCont_iff deriv_def cong: LIM_equal [rule_format])
+      by (simp add: isCont_iff DERIV_def cong: LIM_equal [rule_format])
     show "?g x = l" by simp
   qed
 next
   assume "?rhs"
   then obtain g where
     "(\<forall>z. f z - f x = g z * (z-x))" and "isCont g x" and "g x = l" by blast
   thus "(DERIV f x :> l)"
-     by (auto simp add: isCont_iff deriv_def cong: LIM_cong)
+     by (auto simp add: isCont_iff DERIV_def cong: LIM_cong)
 qed
 
 text {*
  Let's do the standard proof, though theorem
  @{text "LIM_mult2"} follows from a NS proof

   hence "\<exists>D. DERIV f c :> D" by (rule differentiableD)
   then obtain f'c where f'cdef: "DERIV f c :> f'c" ..
 
   from cdef have "DERIV ?h c :> l" by auto
   moreover have "DERIV ?h c :>  g'c * (f b - f a) - f'c * (g b - g a)"
-    using g'cdef f'cdef by (auto intro!: DERIV_intros)
+    using g'cdef f'cdef by (auto intro!: derivative_eq_intros)
   ultimately have leq: "l =  g'c * (f b - f a) - f'c * (g b - g a)" by (rule DERIV_unique)
 
   {
     from cdef have "?h b - ?h a = (b - a) * l" by auto
     also from leq have "\<dots> = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp