merged DERIV_intros, has_derivative_intros into derivative_intros
authorhoelzl
Thu Apr 03 17:56:08 2014 +0200 (2014-04-03)
changeset 563810556204bc230
parent 56380 9bb2856cc845
child 56382 5a50109d51ab
child 56383 8e7052e9fda4
merged DERIV_intros, has_derivative_intros into derivative_intros
NEWS
src/HOL/Complex.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Deriv.thy
src/HOL/Library/Inner_Product.thy
src/HOL/Library/Poly_Deriv.thy
src/HOL/Library/Product_Vector.thy
src/HOL/MacLaurin.thy
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/NSA/HDeriv.thy
src/HOL/NthRoot.thy
src/HOL/Probability/Distributions.thy
src/HOL/Transcendental.thy
     1.1 --- a/NEWS	Thu Apr 03 17:16:02 2014 +0200
     1.2 +++ b/NEWS	Thu Apr 03 17:56:08 2014 +0200
     1.3 @@ -534,6 +534,13 @@
     1.4  
     1.5    - Renamed FDERIV_... lemmas to has_derivative_...
     1.6  
     1.7 +  - renamed deriv (the syntax constant used for "DERIV _ _ :> _") to DERIV
     1.8 +
     1.9 +  - removed DERIV_intros, has_derivative_eq_intros
    1.10 +
    1.11 +  - introduced derivative_intros and deriative_eq_intros which includes now rules for
    1.12 +    DERIV, has_derivative and has_vector_derivative.
    1.13 +
    1.14    - Other renamings:
    1.15      differentiable_def        ~>  real_differentiable_def
    1.16      differentiableE           ~>  real_differentiableE
    1.17 @@ -541,6 +548,7 @@
    1.18      field_fderiv_def          ~>  field_has_derivative_at
    1.19      isDiff_der                ~>  differentiable_def
    1.20      deriv_fderiv              ~>  has_field_derivative_def
    1.21 +    deriv_def                 ~>  DERIV_def
    1.22  INCOMPATIBILITY.
    1.23  
    1.24  * Include more theorems in continuous_intros. Remove the continuous_on_intros,
     2.1 --- a/src/HOL/Complex.thy	Thu Apr 03 17:16:02 2014 +0200
     2.2 +++ b/src/HOL/Complex.thy	Thu Apr 03 17:56:08 2014 +0200
     2.3 @@ -374,30 +374,20 @@
     2.4  lemma bounded_linear_Im: "bounded_linear Im"
     2.5    by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def)
     2.6  
     2.7 -lemmas tendsto_Re [tendsto_intros] =
     2.8 -  bounded_linear.tendsto [OF bounded_linear_Re]
     2.9 -
    2.10 -lemmas tendsto_Im [tendsto_intros] =
    2.11 -  bounded_linear.tendsto [OF bounded_linear_Im]
    2.12 -
    2.13 -lemmas isCont_Re [simp] = bounded_linear.isCont [OF bounded_linear_Re]
    2.14 -lemmas isCont_Im [simp] = bounded_linear.isCont [OF bounded_linear_Im]
    2.15  lemmas Cauchy_Re = bounded_linear.Cauchy [OF bounded_linear_Re]
    2.16  lemmas Cauchy_Im = bounded_linear.Cauchy [OF bounded_linear_Im]
    2.17 -
    2.18 -lemma continuous_Re: "continuous_on X Re"
    2.19 -  by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Re 
    2.20 -            continuous_on_cong continuous_on_id)
    2.21 -
    2.22 -lemma continuous_Im: "continuous_on X Im"
    2.23 -  by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Im 
    2.24 -            continuous_on_cong continuous_on_id)
    2.25 -
    2.26 -lemma has_derivative_Re [has_derivative_intros] : "(Re has_derivative Re) F"
    2.27 -  by (auto simp add: has_derivative_def bounded_linear_Re tendsto_const)
    2.28 -
    2.29 -lemma has_derivative_Im [has_derivative_intros] : "(Im has_derivative Im) F"
    2.30 -  by (auto simp add: has_derivative_def bounded_linear_Im tendsto_const)
    2.31 +lemmas tendsto_Re [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Re]
    2.32 +lemmas tendsto_Im [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Im]
    2.33 +lemmas isCont_Re [simp] = bounded_linear.isCont [OF bounded_linear_Re]
    2.34 +lemmas isCont_Im [simp] = bounded_linear.isCont [OF bounded_linear_Im]
    2.35 +lemmas continuous_Re [simp] = bounded_linear.continuous [OF bounded_linear_Re]
    2.36 +lemmas continuous_Im [simp] = bounded_linear.continuous [OF bounded_linear_Im]
    2.37 +lemmas continuous_on_Re [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Re]
    2.38 +lemmas continuous_on_Im [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Im]
    2.39 +lemmas has_derivative_Re [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Re]
    2.40 +lemmas has_derivative_Im [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Im]
    2.41 +lemmas sums_Re = bounded_linear.sums [OF bounded_linear_Re]
    2.42 +lemmas sums_Im = bounded_linear.sums [OF bounded_linear_Im]
    2.43  
    2.44  lemma tendsto_Complex [tendsto_intros]:
    2.45    assumes "(f ---> a) F" and "(g ---> b) F"
    2.46 @@ -445,8 +435,7 @@
    2.47  qed
    2.48  
    2.49  declare
    2.50 -  DERIV_power[where 'a=complex, THEN DERIV_cong,
    2.51 -              unfolded of_nat_def[symmetric], DERIV_intros]
    2.52 +  DERIV_power[where 'a=complex, unfolded of_nat_def[symmetric], derivative_intros]
    2.53  
    2.54  
    2.55  subsection {* The Complex Number $i$ *}
    2.56 @@ -605,11 +594,11 @@
    2.57    using complex_cnj_add complex_cnj_scaleR
    2.58    by (rule bounded_linear_intro [where K=1], simp)
    2.59  
    2.60 -lemmas tendsto_cnj [tendsto_intros] =
    2.61 -  bounded_linear.tendsto [OF bounded_linear_cnj]
    2.62 -
    2.63 -lemmas isCont_cnj [simp] =
    2.64 -  bounded_linear.isCont [OF bounded_linear_cnj]
    2.65 +lemmas tendsto_cnj [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_cnj]
    2.66 +lemmas isCont_cnj [simp] = bounded_linear.isCont [OF bounded_linear_cnj]
    2.67 +lemmas continuous_cnj [simp, continuous_intros] = bounded_linear.continuous [OF bounded_linear_cnj]
    2.68 +lemmas continuous_on_cnj [simp, continuous_intros] = bounded_linear.continuous_on [OF bounded_linear_cnj]
    2.69 +lemmas has_derivative_cnj [simp, derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_cnj]
    2.70  
    2.71  lemma lim_cnj: "((\<lambda>x. cnj(f x)) ---> cnj l) F \<longleftrightarrow> (f ---> l) F"
    2.72    by (simp add: tendsto_iff dist_complex_def Complex.complex_cnj_diff [symmetric])
    2.73 @@ -704,12 +693,6 @@
    2.74  lemma sums_complex_iff: "f sums x \<longleftrightarrow> ((\<lambda>x. Re (f x)) sums Re x) \<and> ((\<lambda>x. Im (f x)) sums Im x)"
    2.75    unfolding sums_def tendsto_complex_iff Im_setsum Re_setsum ..
    2.76    
    2.77 -lemma sums_Re: "f sums a \<Longrightarrow> (\<lambda>x. Re (f x)) sums Re a"
    2.78 -  unfolding sums_complex_iff by blast
    2.79 -
    2.80 -lemma sums_Im: "f sums a \<Longrightarrow> (\<lambda>x. Im (f x)) sums Im a"
    2.81 -  unfolding sums_complex_iff by blast
    2.82 -
    2.83  lemma summable_complex_iff: "summable f \<longleftrightarrow> summable (\<lambda>x. Re (f x)) \<and>  summable (\<lambda>x. Im (f x))"
    2.84    unfolding summable_def sums_complex_iff[abs_def] by (metis Im.simps Re.simps)
    2.85  
    2.86 @@ -976,5 +959,4 @@
    2.87  lemmas complex_Re_Im_cancel_iff = complex_eq_iff
    2.88  lemmas complex_equality = complex_eqI
    2.89  
    2.90 -
    2.91  end
     3.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Thu Apr 03 17:16:02 2014 +0200
     3.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Apr 03 17:56:08 2014 +0200
     3.3 @@ -2674,24 +2674,24 @@
     3.4  proof (induct f arbitrary: x)
     3.5    case (Inverse a)
     3.6    thus ?case
     3.7 -    by (auto intro!: DERIV_intros simp add: algebra_simps power2_eq_square)
     3.8 +    by (auto intro!: derivative_eq_intros simp add: algebra_simps power2_eq_square)
     3.9  next
    3.10    case (Cos a)
    3.11    thus ?case
    3.12 -    by (auto intro!: DERIV_intros
    3.13 +    by (auto intro!: derivative_intros
    3.14             simp del: interpret_floatarith.simps(5)
    3.15             simp add: interpret_floatarith_sin interpret_floatarith.simps(5)[of a])
    3.16  next
    3.17    case (Power a n)
    3.18    thus ?case
    3.19 -    by (cases n) (auto intro!: DERIV_intros simp del: power_Suc)
    3.20 +    by (cases n) (auto intro!: derivative_intros simp del: power_Suc)
    3.21  next
    3.22    case (Ln a)
    3.23 -  thus ?case by (auto intro!: DERIV_intros simp add: divide_inverse)
    3.24 +  thus ?case by (auto intro!: derivative_intros simp add: divide_inverse)
    3.25  next
    3.26    case (Var i)
    3.27    thus ?case using `n < length vs` by auto
    3.28 -qed (auto intro!: DERIV_intros)
    3.29 +qed (auto intro!: derivative_eq_intros)
    3.30  
    3.31  declare approx.simps[simp del]
    3.32  
     4.1 --- a/src/HOL/Deriv.thy	Thu Apr 03 17:16:02 2014 +0200
     4.2 +++ b/src/HOL/Deriv.thy	Thu Apr 03 17:56:08 2014 +0200
     4.3 @@ -29,6 +29,48 @@
     4.4    most cases @{term s} is either a variable or @{term UNIV}.
     4.5  *}
     4.6  
     4.7 +lemma has_derivative_eq_rhs: "(f has_derivative f') F \<Longrightarrow> f' = g' \<Longrightarrow> (f has_derivative g') F"
     4.8 +  by simp
     4.9 +
    4.10 +definition 
    4.11 +  has_field_derivative :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a filter \<Rightarrow> bool"
    4.12 +  (infix "(has'_field'_derivative)" 50)
    4.13 +where
    4.14 +  "(f has_field_derivative D) F \<longleftrightarrow> (f has_derivative op * D) F"
    4.15 +
    4.16 +lemma DERIV_cong: "(f has_field_derivative X) F \<Longrightarrow> X = Y \<Longrightarrow> (f has_field_derivative Y) F"
    4.17 +  by simp
    4.18 +
    4.19 +definition
    4.20 +  has_vector_derivative :: "(real \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'b \<Rightarrow> real filter \<Rightarrow> bool"
    4.21 +  (infix "has'_vector'_derivative" 50)
    4.22 +where
    4.23 +  "(f has_vector_derivative f') net \<longleftrightarrow> (f has_derivative (\<lambda>x. x *\<^sub>R f')) net"
    4.24 +
    4.25 +lemma has_vector_derivative_eq_rhs: "(f has_vector_derivative X) F \<Longrightarrow> X = Y \<Longrightarrow> (f has_vector_derivative Y) F"
    4.26 +  by simp
    4.27 +
    4.28 +ML {*
    4.29 +
    4.30 +structure Derivative_Intros = Named_Thms
    4.31 +(
    4.32 +  val name = @{binding derivative_intros}
    4.33 +  val description = "structural introduction rules for derivatives"
    4.34 +)
    4.35 +
    4.36 +*}
    4.37 +
    4.38 +setup {*
    4.39 +  let
    4.40 +    val eq_thms = [@{thm has_derivative_eq_rhs}, @{thm DERIV_cong}, @{thm has_vector_derivative_eq_rhs}]
    4.41 +    fun eq_rule thm = get_first (try (fn eq_thm => eq_thm OF [thm])) eq_thms
    4.42 +  in
    4.43 +    Derivative_Intros.setup #>
    4.44 +    Global_Theory.add_thms_dynamic
    4.45 +      (@{binding derivative_eq_intros}, map_filter eq_rule o Derivative_Intros.get o Context.proof_of)
    4.46 +  end;
    4.47 +*}
    4.48 +
    4.49  text {*
    4.50    The following syntax is only used as a legacy syntax.
    4.51  *}
    4.52 @@ -38,36 +80,16 @@
    4.53  where
    4.54    "FDERIV f x :> f' \<equiv> (f has_derivative f') (at x)"
    4.55  
    4.56 -
    4.57 -lemma has_derivative_eq_rhs: "(f has_derivative f') F \<Longrightarrow> f' = g' \<Longrightarrow> (f has_derivative g') F"
    4.58 -  by simp
    4.59 -
    4.60 -ML {*
    4.61 -
    4.62 -structure has_derivative_Intros = Named_Thms
    4.63 -(
    4.64 -  val name = @{binding has_derivative_intros}
    4.65 -  val description = "introduction rules for FDERIV"
    4.66 -)
    4.67 -
    4.68 -*}
    4.69 -
    4.70 -setup {*
    4.71 -  has_derivative_Intros.setup #>
    4.72 -  Global_Theory.add_thms_dynamic (@{binding has_derivative_eq_intros},
    4.73 -    map_filter (try (fn thm => @{thm has_derivative_eq_rhs} OF [thm])) o has_derivative_Intros.get o Context.proof_of);
    4.74 -*}
    4.75 -
    4.76  lemma has_derivative_bounded_linear: "(f has_derivative f') F \<Longrightarrow> bounded_linear f'"
    4.77    by (simp add: has_derivative_def)
    4.78  
    4.79  lemma has_derivative_linear: "(f has_derivative f') F \<Longrightarrow> linear f'"
    4.80    using bounded_linear.linear[OF has_derivative_bounded_linear] .
    4.81  
    4.82 -lemma has_derivative_ident[has_derivative_intros, simp]: "((\<lambda>x. x) has_derivative (\<lambda>x. x)) F"
    4.83 +lemma has_derivative_ident[derivative_intros, simp]: "((\<lambda>x. x) has_derivative (\<lambda>x. x)) F"
    4.84    by (simp add: has_derivative_def tendsto_const)
    4.85  
    4.86 -lemma has_derivative_const[has_derivative_intros, simp]: "((\<lambda>x. c) has_derivative (\<lambda>x. 0)) F"
    4.87 +lemma has_derivative_const[derivative_intros, simp]: "((\<lambda>x. c) has_derivative (\<lambda>x. 0)) F"
    4.88    by (simp add: has_derivative_def tendsto_const)
    4.89  
    4.90  lemma (in bounded_linear) bounded_linear: "bounded_linear f" ..
    4.91 @@ -81,19 +103,19 @@
    4.92    apply (simp add: scaleR diff add zero)
    4.93    done
    4.94  
    4.95 -lemmas has_derivative_scaleR_right [has_derivative_intros] =
    4.96 +lemmas has_derivative_scaleR_right [derivative_intros] =
    4.97    bounded_linear.has_derivative [OF bounded_linear_scaleR_right]
    4.98  
    4.99 -lemmas has_derivative_scaleR_left [has_derivative_intros] =
   4.100 +lemmas has_derivative_scaleR_left [derivative_intros] =
   4.101    bounded_linear.has_derivative [OF bounded_linear_scaleR_left]
   4.102  
   4.103 -lemmas has_derivative_mult_right [has_derivative_intros] =
   4.104 +lemmas has_derivative_mult_right [derivative_intros] =
   4.105    bounded_linear.has_derivative [OF bounded_linear_mult_right]
   4.106  
   4.107 -lemmas has_derivative_mult_left [has_derivative_intros] =
   4.108 +lemmas has_derivative_mult_left [derivative_intros] =
   4.109    bounded_linear.has_derivative [OF bounded_linear_mult_left]
   4.110  
   4.111 -lemma has_derivative_add[simp, has_derivative_intros]:
   4.112 +lemma has_derivative_add[simp, derivative_intros]:
   4.113    assumes f: "(f has_derivative f') F" and g: "(g has_derivative g') F"
   4.114    shows "((\<lambda>x. f x + g x) has_derivative (\<lambda>x. f' x + g' x)) F"
   4.115    unfolding has_derivative_def
   4.116 @@ -106,7 +128,7 @@
   4.117      by (simp add: field_simps scaleR_add_right scaleR_diff_right)
   4.118  qed (blast intro: bounded_linear_add f g has_derivative_bounded_linear)
   4.119  
   4.120 -lemma has_derivative_setsum[simp, has_derivative_intros]:
   4.121 +lemma has_derivative_setsum[simp, derivative_intros]:
   4.122    assumes f: "\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) F"
   4.123    shows "((\<lambda>x. \<Sum>i\<in>I. f i x) has_derivative (\<lambda>x. \<Sum>i\<in>I. f' i x)) F"
   4.124  proof cases
   4.125 @@ -114,10 +136,10 @@
   4.126      by induct (simp_all add: f)
   4.127  qed simp
   4.128  
   4.129 -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"
   4.130 +lemma has_derivative_minus[simp, derivative_intros]: "(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. - f x) has_derivative (\<lambda>x. - f' x)) F"
   4.131    using has_derivative_scaleR_right[of f f' F "-1"] by simp
   4.132  
   4.133 -lemma has_derivative_diff[simp, has_derivative_intros]:
   4.134 +lemma has_derivative_diff[simp, derivative_intros]:
   4.135    "(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"
   4.136    by (simp only: diff_conv_add_uminus has_derivative_add has_derivative_minus)
   4.137  
   4.138 @@ -320,10 +342,10 @@
   4.139    qed simp
   4.140  qed
   4.141  
   4.142 -lemmas has_derivative_mult[simp, has_derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_mult]
   4.143 -lemmas has_derivative_scaleR[simp, has_derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_scaleR]
   4.144 +lemmas has_derivative_mult[simp, derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_mult]
   4.145 +lemmas has_derivative_scaleR[simp, derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_scaleR]
   4.146  
   4.147 -lemma has_derivative_setprod[simp, has_derivative_intros]:
   4.148 +lemma has_derivative_setprod[simp, derivative_intros]:
   4.149    fixes f :: "'i \<Rightarrow> 'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
   4.150    assumes f: "\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) (at x within s)"
   4.151    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)"
   4.152 @@ -341,7 +363,7 @@
   4.153    qed simp  
   4.154  qed simp
   4.155  
   4.156 -lemma has_derivative_power[simp, has_derivative_intros]:
   4.157 +lemma has_derivative_power[simp, derivative_intros]:
   4.158    fixes f :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
   4.159    assumes f: "(f has_derivative f') (at x within s)"
   4.160    shows "((\<lambda>x. f x^n) has_derivative (\<lambda>y. of_nat n * f' y * f x^(n - 1))) (at x within s)"
   4.161 @@ -392,13 +414,13 @@
   4.162        norm (?inv y - ?inv x) * norm (?inv x)" .
   4.163  qed
   4.164  
   4.165 -lemma has_derivative_inverse[simp, has_derivative_intros]:
   4.166 +lemma has_derivative_inverse[simp, derivative_intros]:
   4.167    fixes f :: "_ \<Rightarrow> 'a::real_normed_div_algebra"
   4.168    assumes x:  "f x \<noteq> 0" and f: "(f has_derivative f') (at x within s)"
   4.169    shows "((\<lambda>x. inverse (f x)) has_derivative (\<lambda>h. - (inverse (f x) * f' h * inverse (f x)))) (at x within s)"
   4.170    using has_derivative_compose[OF f has_derivative_inverse', OF x] .
   4.171  
   4.172 -lemma has_derivative_divide[simp, has_derivative_intros]:
   4.173 +lemma has_derivative_divide[simp, derivative_intros]:
   4.174    fixes f :: "_ \<Rightarrow> 'a::real_normed_div_algebra"
   4.175    assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)" 
   4.176    assumes x: "g x \<noteq> 0"
   4.177 @@ -409,7 +431,7 @@
   4.178  
   4.179  text{*Conventional form requires mult-AC laws. Types real and complex only.*}
   4.180  
   4.181 -lemma has_derivative_divide'[has_derivative_intros]: 
   4.182 +lemma has_derivative_divide'[derivative_intros]: 
   4.183    fixes f :: "_ \<Rightarrow> 'a::real_normed_field"
   4.184    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"
   4.185    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)"
   4.186 @@ -485,10 +507,10 @@
   4.187  
   4.188  lemmas differentiable_within_subset = differentiable_subset
   4.189  
   4.190 -lemma differentiable_ident [simp]: "(\<lambda>x. x) differentiable F"
   4.191 +lemma differentiable_ident [simp, derivative_intros]: "(\<lambda>x. x) differentiable F"
   4.192    unfolding differentiable_def by (blast intro: has_derivative_ident)
   4.193  
   4.194 -lemma differentiable_const [simp]: "(\<lambda>z. a) differentiable F"
   4.195 +lemma differentiable_const [simp, derivative_intros]: "(\<lambda>z. a) differentiable F"
   4.196    unfolding differentiable_def by (blast intro: has_derivative_const)
   4.197  
   4.198  lemma differentiable_in_compose:
   4.199 @@ -499,48 +521,42 @@
   4.200    "f differentiable (at (g x)) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> (\<lambda>x. f (g x)) differentiable (at x within s)"
   4.201    by (blast intro: differentiable_in_compose differentiable_subset)
   4.202  
   4.203 -lemma differentiable_sum [simp]:
   4.204 +lemma differentiable_sum [simp, derivative_intros]:
   4.205    "f differentiable F \<Longrightarrow> g differentiable F \<Longrightarrow> (\<lambda>x. f x + g x) differentiable F"
   4.206    unfolding differentiable_def by (blast intro: has_derivative_add)
   4.207  
   4.208 -lemma differentiable_minus [simp]:
   4.209 +lemma differentiable_minus [simp, derivative_intros]:
   4.210    "f differentiable F \<Longrightarrow> (\<lambda>x. - f x) differentiable F"
   4.211    unfolding differentiable_def by (blast intro: has_derivative_minus)
   4.212  
   4.213 -lemma differentiable_diff [simp]:
   4.214 +lemma differentiable_diff [simp, derivative_intros]:
   4.215    "f differentiable F \<Longrightarrow> g differentiable F \<Longrightarrow> (\<lambda>x. f x - g x) differentiable F"
   4.216    unfolding differentiable_def by (blast intro: has_derivative_diff)
   4.217  
   4.218 -lemma differentiable_mult [simp]:
   4.219 +lemma differentiable_mult [simp, derivative_intros]:
   4.220    fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_algebra"
   4.221    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)"
   4.222    unfolding differentiable_def by (blast intro: has_derivative_mult)
   4.223  
   4.224 -lemma differentiable_inverse [simp]:
   4.225 +lemma differentiable_inverse [simp, derivative_intros]:
   4.226    fixes f :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
   4.227    shows "f differentiable (at x within s) \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> (\<lambda>x. inverse (f x)) differentiable (at x within s)"
   4.228    unfolding differentiable_def by (blast intro: has_derivative_inverse)
   4.229  
   4.230 -lemma differentiable_divide [simp]:
   4.231 +lemma differentiable_divide [simp, derivative_intros]:
   4.232    fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
   4.233    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)"
   4.234    unfolding divide_inverse using assms by simp
   4.235  
   4.236 -lemma differentiable_power [simp]:
   4.237 +lemma differentiable_power [simp, derivative_intros]:
   4.238    fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
   4.239    shows "f differentiable (at x within s) \<Longrightarrow> (\<lambda>x. f x ^ n) differentiable (at x within s)"
   4.240    unfolding differentiable_def by (blast intro: has_derivative_power)
   4.241  
   4.242 -lemma differentiable_scaleR [simp]:
   4.243 +lemma differentiable_scaleR [simp, derivative_intros]:
   4.244    "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)"
   4.245    unfolding differentiable_def by (blast intro: has_derivative_scaleR)
   4.246  
   4.247 -definition 
   4.248 -  has_field_derivative :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a filter \<Rightarrow> bool"
   4.249 -  (infix "(has'_field'_derivative)" 50)
   4.250 -where
   4.251 -  "(f has_field_derivative D) F \<longleftrightarrow> (f has_derivative op * D) F"
   4.252 -
   4.253  lemma has_derivative_imp_has_field_derivative:
   4.254    "(f has_derivative D) F \<Longrightarrow> (\<And>x. x * D' = D x) \<Longrightarrow> (f has_field_derivative D') F"
   4.255    unfolding has_field_derivative_def 
   4.256 @@ -555,7 +571,7 @@
   4.257    by (simp add: has_field_derivative_def has_derivative_within_subset)
   4.258  
   4.259  abbreviation (input)
   4.260 -  deriv :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
   4.261 +  DERIV :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
   4.262    ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
   4.263  where
   4.264    "DERIV f x :> D \<equiv> (f has_field_derivative D) (at x)"
   4.265 @@ -588,8 +604,7 @@
   4.266  lemma differentiableI: "(f has_real_derivative D) (at x within s) \<Longrightarrow> f differentiable (at x within s)"
   4.267    by (force simp add: real_differentiable_def)
   4.268  
   4.269 -lemma deriv_def:
   4.270 -  "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
   4.271 +lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
   4.272    apply (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right LIM_zero_iff[symmetric, of _ D])
   4.273    apply (subst (2) tendsto_norm_zero_iff[symmetric])
   4.274    apply (rule filterlim_cong)
   4.275 @@ -602,40 +617,36 @@
   4.276  subsection {* Derivatives *}
   4.277  
   4.278  lemma DERIV_D: "DERIV f x :> D \<Longrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
   4.279 -  by (simp add: deriv_def)
   4.280 +  by (simp add: DERIV_def)
   4.281  
   4.282 -lemma DERIV_const [simp]: "((\<lambda>x. k) has_field_derivative 0) (at x within s)"
   4.283 +lemma DERIV_const [simp, derivative_intros]: "((\<lambda>x. k) has_field_derivative 0) F"
   4.284    by (rule has_derivative_imp_has_field_derivative[OF has_derivative_const]) auto
   4.285  
   4.286 -lemma DERIV_ident [simp]: "((\<lambda>x. x) has_field_derivative 1) (at x within s)"
   4.287 +lemma DERIV_ident [simp, derivative_intros]: "((\<lambda>x. x) has_field_derivative 1) F"
   4.288    by (rule has_derivative_imp_has_field_derivative[OF has_derivative_ident]) auto
   4.289  
   4.290 -lemma field_differentiable_add:
   4.291 -  assumes "(f has_field_derivative f') F" "(g has_field_derivative g') F"
   4.292 -    shows "((\<lambda>z. f z + g z) has_field_derivative f' + g') F"
   4.293 -  apply (rule has_derivative_imp_has_field_derivative[OF has_derivative_add])
   4.294 -  using assms 
   4.295 -  by (auto simp: has_field_derivative_def field_simps mult_commute_abs)
   4.296 +lemma field_differentiable_add[derivative_intros]:
   4.297 +  "(f has_field_derivative f') F \<Longrightarrow> (g has_field_derivative g') F \<Longrightarrow> 
   4.298 +    ((\<lambda>z. f z + g z) has_field_derivative f' + g') F"
   4.299 +  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_add])
   4.300 +     (auto simp: has_field_derivative_def field_simps mult_commute_abs)
   4.301  
   4.302  corollary DERIV_add:
   4.303    "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
   4.304    ((\<lambda>x. f x + g x) has_field_derivative D + E) (at x within s)"
   4.305    by (rule field_differentiable_add)
   4.306  
   4.307 -lemma field_differentiable_minus:
   4.308 -  assumes "(f has_field_derivative f') F" 
   4.309 -    shows "((\<lambda>z. - (f z)) has_field_derivative -f') F"
   4.310 -  apply (rule has_derivative_imp_has_field_derivative[OF has_derivative_minus])
   4.311 -  using assms 
   4.312 -  by (auto simp: has_field_derivative_def field_simps mult_commute_abs)
   4.313 +lemma field_differentiable_minus[derivative_intros]:
   4.314 +  "(f has_field_derivative f') F \<Longrightarrow> ((\<lambda>z. - (f z)) has_field_derivative -f') F"
   4.315 +  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_minus])
   4.316 +     (auto simp: has_field_derivative_def field_simps mult_commute_abs)
   4.317  
   4.318  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)"
   4.319    by (rule field_differentiable_minus)
   4.320  
   4.321 -lemma field_differentiable_diff:
   4.322 -  assumes "(f has_field_derivative f') F" "(g has_field_derivative g') F"
   4.323 -    shows "((\<lambda>z. f z - g z) has_field_derivative f' - g') F"
   4.324 -by (simp only: assms diff_conv_add_uminus field_differentiable_add field_differentiable_minus)
   4.325 +lemma field_differentiable_diff[derivative_intros]:
   4.326 +  "(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"
   4.327 +  by (simp only: assms diff_conv_add_uminus field_differentiable_add field_differentiable_minus)
   4.328  
   4.329  corollary DERIV_diff:
   4.330    "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
   4.331 @@ -658,7 +669,7 @@
   4.332    by (rule has_derivative_imp_has_field_derivative[OF has_derivative_mult])
   4.333       (auto simp: field_simps mult_commute_abs dest: has_field_derivative_imp_has_derivative)
   4.334  
   4.335 -lemma DERIV_mult:
   4.336 +lemma DERIV_mult[derivative_intros]:
   4.337    "(f has_field_derivative Da) (at x within s) \<Longrightarrow> (g has_field_derivative Db) (at x within s) \<Longrightarrow>
   4.338    ((\<lambda>x. f x * g x) has_field_derivative Da * g x + Db * f x) (at x within s)"
   4.339    by (rule has_derivative_imp_has_field_derivative[OF has_derivative_mult])
   4.340 @@ -672,7 +683,7 @@
   4.341  
   4.342  lemma DERIV_cmult_right:
   4.343    "(f has_field_derivative D) (at x within s) ==> ((\<lambda>x. f x * c) has_field_derivative D * c) (at x within s)"
   4.344 -  using DERIV_cmult   by (force simp add: mult_ac)
   4.345 +  using DERIV_cmult by (force simp add: mult_ac)
   4.346  
   4.347  lemma DERIV_cmult_Id [simp]: "(op * c has_field_derivative c) (at x within s)"
   4.348    by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp)
   4.349 @@ -683,15 +694,15 @@
   4.350  
   4.351  lemma DERIV_unique:
   4.352    "DERIV f x :> D \<Longrightarrow> DERIV f x :> E \<Longrightarrow> D = E"
   4.353 -  unfolding deriv_def by (rule LIM_unique) 
   4.354 +  unfolding DERIV_def by (rule LIM_unique) 
   4.355  
   4.356 -lemma DERIV_setsum:
   4.357 +lemma DERIV_setsum[derivative_intros]:
   4.358    "(\<And> n. n \<in> S \<Longrightarrow> ((\<lambda>x. f x n) has_field_derivative (f' x n)) F) \<Longrightarrow> 
   4.359      ((\<lambda>x. setsum (f x) S) has_field_derivative setsum (f' x) S) F"
   4.360    by (rule has_derivative_imp_has_field_derivative[OF has_derivative_setsum])
   4.361       (auto simp: setsum_right_distrib mult_commute_abs dest: has_field_derivative_imp_has_derivative)
   4.362  
   4.363 -lemma DERIV_inverse':
   4.364 +lemma DERIV_inverse'[derivative_intros]:
   4.365    "(f has_field_derivative D) (at x within s) \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow>
   4.366    ((\<lambda>x. inverse (f x)) has_field_derivative - (inverse (f x) * D * inverse (f x))) (at x within s)"
   4.367    by (rule has_derivative_imp_has_field_derivative[OF has_derivative_inverse])
   4.368 @@ -712,7 +723,7 @@
   4.369  
   4.370  text {* Derivative of quotient *}
   4.371  
   4.372 -lemma DERIV_divide:
   4.373 +lemma DERIV_divide[derivative_intros]:
   4.374    "(f has_field_derivative D) (at x within s) \<Longrightarrow>
   4.375    (g has_field_derivative E) (at x within s) \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow>
   4.376    ((\<lambda>x. f x / g x) has_field_derivative (D * g x - f x * E) / (g x * g x)) (at x within s)"
   4.377 @@ -731,7 +742,7 @@
   4.378    by (rule has_derivative_imp_has_field_derivative[OF has_derivative_power])
   4.379       (auto simp: has_field_derivative_def)
   4.380  
   4.381 -lemma DERIV_power:
   4.382 +lemma DERIV_power[derivative_intros]:
   4.383    "(f has_field_derivative D) (at x within s) \<Longrightarrow>
   4.384    ((\<lambda>x. f x ^ n) has_field_derivative of_nat n * (D * f x ^ (n - Suc 0))) (at x within s)"
   4.385    by (rule has_derivative_imp_has_field_derivative[OF has_derivative_power])
   4.386 @@ -778,34 +789,8 @@
   4.387      shows "DERIV (\<lambda>x. g(f x)) x :> f' * g'(f x)"
   4.388    by (metis UNIV_I DERIV_chain_s [of UNIV] assms)
   4.389  
   4.390 -
   4.391 -subsubsection {* @{text "DERIV_intros"} *}
   4.392 -
   4.393 -ML {*
   4.394 -structure Deriv_Intros = Named_Thms
   4.395 -(
   4.396 -  val name = @{binding DERIV_intros}
   4.397 -  val description = "DERIV introduction rules"
   4.398 -)
   4.399 -*}
   4.400 -
   4.401 -setup Deriv_Intros.setup
   4.402 -
   4.403 -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)"
   4.404 -  by simp
   4.405 -
   4.406  declare
   4.407 -  DERIV_const[THEN DERIV_cong, DERIV_intros]
   4.408 -  DERIV_ident[THEN DERIV_cong, DERIV_intros]
   4.409 -  DERIV_add[THEN DERIV_cong, DERIV_intros]
   4.410 -  DERIV_minus[THEN DERIV_cong, DERIV_intros]
   4.411 -  DERIV_mult[THEN DERIV_cong, DERIV_intros]
   4.412 -  DERIV_diff[THEN DERIV_cong, DERIV_intros]
   4.413 -  DERIV_inverse'[THEN DERIV_cong, DERIV_intros]
   4.414 -  DERIV_divide[THEN DERIV_cong, DERIV_intros]
   4.415 -  DERIV_power[where 'a=real, THEN DERIV_cong,
   4.416 -              unfolded real_of_nat_def[symmetric], DERIV_intros]
   4.417 -  DERIV_setsum[THEN DERIV_cong, DERIV_intros]
   4.418 +  DERIV_power[where 'a=real, unfolded real_of_nat_def[symmetric], derivative_intros]
   4.419  
   4.420  text{*Alternative definition for differentiability*}
   4.421  
   4.422 @@ -821,7 +806,7 @@
   4.423  done
   4.424  
   4.425  lemma DERIV_iff2: "(DERIV f x :> D) \<longleftrightarrow> (\<lambda>z. (f z - f x) / (z - x)) --x --> D"
   4.426 -  by (simp add: deriv_def DERIV_LIM_iff)
   4.427 +  by (simp add: DERIV_def DERIV_LIM_iff)
   4.428  
   4.429  lemma DERIV_cong_ev: "x = y \<Longrightarrow> eventually (\<lambda>x. f x = g x) (nhds x) \<Longrightarrow> u = v \<Longrightarrow>
   4.430      DERIV f x :> u \<longleftrightarrow> DERIV g y :> v"
   4.431 @@ -836,11 +821,11 @@
   4.432  
   4.433  lemma DERIV_shift:
   4.434    "(DERIV f (x + z) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (x + z)) x :> y)"
   4.435 -  by (simp add: deriv_def field_simps)
   4.436 +  by (simp add: DERIV_def field_simps)
   4.437  
   4.438  lemma DERIV_mirror:
   4.439    "(DERIV f (- x) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (- x::real) :: real) x :> - y)"
   4.440 -  by (simp add: deriv_def filterlim_at_split filterlim_at_left_to_right
   4.441 +  by (simp add: DERIV_def filterlim_at_split filterlim_at_left_to_right
   4.442                  tendsto_minus_cancel_left field_simps conj_commute)
   4.443  
   4.444  text {* Caratheodory formulation of derivative at a point *}
   4.445 @@ -855,7 +840,7 @@
   4.446      let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
   4.447      show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
   4.448      show "isCont ?g x" using der
   4.449 -      by (simp add: isCont_iff deriv_def cong: LIM_equal [rule_format])
   4.450 +      by (simp add: isCont_iff DERIV_def cong: LIM_equal [rule_format])
   4.451      show "?g x = l" by simp
   4.452    qed
   4.453  next
   4.454 @@ -863,7 +848,7 @@
   4.455    then obtain g where
   4.456      "(\<forall>z. f z - f x = g z * (z-x))" and "isCont g x" and "g x = l" by blast
   4.457    thus "(DERIV f x :> l)"
   4.458 -     by (auto simp add: isCont_iff deriv_def cong: LIM_cong)
   4.459 +     by (auto simp add: isCont_iff DERIV_def cong: LIM_cong)
   4.460  qed
   4.461  
   4.462  text {*
   4.463 @@ -1477,7 +1462,7 @@
   4.464  
   4.465    from cdef have "DERIV ?h c :> l" by auto
   4.466    moreover have "DERIV ?h c :>  g'c * (f b - f a) - f'c * (g b - g a)"
   4.467 -    using g'cdef f'cdef by (auto intro!: DERIV_intros)
   4.468 +    using g'cdef f'cdef by (auto intro!: derivative_eq_intros)
   4.469    ultimately have leq: "l =  g'c * (f b - f a) - f'c * (g b - g a)" by (rule DERIV_unique)
   4.470  
   4.471    {
     5.1 --- a/src/HOL/Library/Inner_Product.thy	Thu Apr 03 17:16:02 2014 +0200
     5.2 +++ b/src/HOL/Library/Inner_Product.thy	Thu Apr 03 17:56:08 2014 +0200
     5.3 @@ -180,7 +180,7 @@
     5.4  lemmas isCont_inner [simp] =
     5.5    bounded_bilinear.isCont [OF bounded_bilinear_inner]
     5.6  
     5.7 -lemmas has_derivative_inner [has_derivative_intros] =
     5.8 +lemmas has_derivative_inner [derivative_intros] =
     5.9    bounded_bilinear.FDERIV [OF bounded_bilinear_inner]
    5.10  
    5.11  lemmas bounded_linear_inner_left =
    5.12 @@ -189,10 +189,10 @@
    5.13  lemmas bounded_linear_inner_right =
    5.14    bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]
    5.15  
    5.16 -lemmas has_derivative_inner_right [has_derivative_intros] =
    5.17 +lemmas has_derivative_inner_right [derivative_intros] =
    5.18    bounded_linear.has_derivative [OF bounded_linear_inner_right]
    5.19  
    5.20 -lemmas has_derivative_inner_left [has_derivative_intros] =
    5.21 +lemmas has_derivative_inner_left [derivative_intros] =
    5.22    bounded_linear.has_derivative [OF bounded_linear_inner_left]
    5.23  
    5.24  lemma differentiable_inner [simp]:
     6.1 --- a/src/HOL/Library/Poly_Deriv.thy	Thu Apr 03 17:16:02 2014 +0200
     6.2 +++ b/src/HOL/Library/Poly_Deriv.thy	Thu Apr 03 17:56:08 2014 +0200
     6.3 @@ -102,7 +102,7 @@
     6.4  by (rule DERIV_cong, rule DERIV_add, auto)
     6.5  
     6.6  lemma poly_DERIV[simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
     6.7 -  by (induct p, auto intro!: DERIV_intros simp add: pderiv_pCons)
     6.8 +  by (induct p, auto intro!: derivative_eq_intros simp add: pderiv_pCons)
     6.9  
    6.10  text{* Consequences of the derivative theorem above*}
    6.11  
     7.1 --- a/src/HOL/Library/Product_Vector.thy	Thu Apr 03 17:16:02 2014 +0200
     7.2 +++ b/src/HOL/Library/Product_Vector.thy	Thu Apr 03 17:56:08 2014 +0200
     7.3 @@ -478,7 +478,7 @@
     7.4  
     7.5  subsubsection {* Frechet derivatives involving pairs *}
     7.6  
     7.7 -lemma has_derivative_Pair [has_derivative_intros]:
     7.8 +lemma has_derivative_Pair [derivative_intros]:
     7.9    assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
    7.10    shows "((\<lambda>x. (f x, g x)) has_derivative (\<lambda>h. (f' h, g' h))) (at x within s)"
    7.11  proof (rule has_derivativeI_sandwich[of 1])
    7.12 @@ -497,10 +497,10 @@
    7.13      by (simp add: norm_Pair divide_right_mono order_trans [OF sqrt_add_le_add_sqrt])
    7.14  qed simp
    7.15  
    7.16 -lemmas has_derivative_fst [has_derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_fst]
    7.17 -lemmas has_derivative_snd [has_derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_snd]
    7.18 +lemmas has_derivative_fst [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_fst]
    7.19 +lemmas has_derivative_snd [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_snd]
    7.20  
    7.21 -lemma has_derivative_split [has_derivative_intros]:
    7.22 +lemma has_derivative_split [derivative_intros]:
    7.23    "((\<lambda>p. f (fst p) (snd p)) has_derivative f') F \<Longrightarrow> ((\<lambda>(a, b). f a b) has_derivative f') F"
    7.24    unfolding split_beta' .
    7.25  
     8.1 --- a/src/HOL/MacLaurin.thy	Thu Apr 03 17:16:02 2014 +0200
     8.2 +++ b/src/HOL/MacLaurin.thy	Thu Apr 03 17:56:08 2014 +0200
     8.3 @@ -40,7 +40,8 @@
     8.4    have "DERIV (difg m) t :> diff (Suc m) t -
     8.5      ((\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / real (fact x)) +
     8.6       real (n - m) * t ^ (n - Suc m) * B / real (fact (n - m)))" unfolding difg_def
     8.7 -    by (auto intro!: DERIV_intros DERIV[rule_format, OF INIT2])
     8.8 +    by (auto intro!: derivative_eq_intros DERIV[rule_format, OF INIT2]
     8.9 +             simp: real_of_nat_def[symmetric])
    8.10    moreover
    8.11    from INIT2 have intvl: "{..<n - m} = insert 0 (Suc ` {..<n - Suc m})" and "0 < n - m"
    8.12      unfolding atLeast0LessThan[symmetric] by auto
    8.13 @@ -209,7 +210,7 @@
    8.14           f h = (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
    8.15           diff n t / real (fact n) * h ^ n"
    8.16  proof -
    8.17 -  txt "Transform @{text ABL'} into @{text DERIV_intros} format."
    8.18 +  txt "Transform @{text ABL'} into @{text derivative_intros} format."
    8.19    note DERIV' = DERIV_chain'[OF _ DERIV[rule_format], THEN DERIV_cong]
    8.20    from assms
    8.21    have "\<exists>t>0. t < - h \<and>
    8.22 @@ -217,7 +218,7 @@
    8.23      (\<Sum>m<n.
    8.24      (- 1) ^ m * diff m (- 0) / real (fact m) * (- h) ^ m) +
    8.25      (- 1) ^ n * diff n (- t) / real (fact n) * (- h) ^ n"
    8.26 -    by (intro Maclaurin) (auto intro!: DERIV_intros DERIV')
    8.27 +    by (intro Maclaurin) (auto intro!: derivative_eq_intros DERIV')
    8.28    then guess t ..
    8.29    moreover
    8.30    have "-1 ^ n * diff n (- t) * (- h) ^ n / real (fact n) = diff n (- t) * h ^ n / real (fact n)"
    8.31 @@ -417,7 +418,7 @@
    8.32  apply safe
    8.33  apply (simp (no_asm))
    8.34  apply (simp (no_asm) add: sin_expansion_lemma)
    8.35 -apply (force intro!: DERIV_intros)
    8.36 +apply (force intro!: derivative_eq_intros)
    8.37  apply (subst (asm) setsum_0', clarify, case_tac "x", simp, simp)
    8.38  apply (cases n, simp, simp)
    8.39  apply (rule ccontr, simp)
    8.40 @@ -446,7 +447,7 @@
    8.41  apply safe
    8.42  apply simp
    8.43  apply (simp (no_asm) add: sin_expansion_lemma)
    8.44 -apply (force intro!: DERIV_intros)
    8.45 +apply (force intro!: derivative_eq_intros)
    8.46  apply (erule ssubst)
    8.47  apply (rule_tac x = t in exI, simp)
    8.48  apply (rule setsum_cong[OF refl])
    8.49 @@ -463,7 +464,7 @@
    8.50  apply safe
    8.51  apply simp
    8.52  apply (simp (no_asm) add: sin_expansion_lemma)
    8.53 -apply (force intro!: DERIV_intros)
    8.54 +apply (force intro!: derivative_eq_intros)
    8.55  apply (erule ssubst)
    8.56  apply (rule_tac x = t in exI, simp)
    8.57  apply (rule setsum_cong[OF refl])
    8.58 @@ -553,7 +554,7 @@
    8.59      apply (clarify)
    8.60      apply (subst (1 2 3) mod_Suc_eq_Suc_mod)
    8.61      apply (cut_tac m=m in mod_exhaust_less_4)
    8.62 -    apply (safe, auto intro!: DERIV_intros)
    8.63 +    apply (safe, auto intro!: derivative_eq_intros)
    8.64      done
    8.65    from Maclaurin_all_le [OF diff_0 DERIV_diff]
    8.66    obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" and
     9.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Thu Apr 03 17:16:02 2014 +0200
     9.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Thu Apr 03 17:56:08 2014 +0200
     9.3 @@ -15,7 +15,7 @@
     9.4    shows "((op * c) has_derivative (op * c)) F"
     9.5  by (rule has_derivative_mult_right [OF has_derivative_id])
     9.6  
     9.7 -lemma has_derivative_of_real[has_derivative_intros, simp]: 
     9.8 +lemma has_derivative_of_real[derivative_intros, simp]: 
     9.9    "(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. of_real (f x)) has_derivative (\<lambda>x. of_real (f' x))) F"
    9.10    using bounded_linear.has_derivative[OF bounded_linear_of_real] .
    9.11  
    9.12 @@ -200,14 +200,6 @@
    9.13      shows "DERIV g a :> f'"
    9.14    by (blast intro: assms DERIV_transform_within)
    9.15  
    9.16 -subsection{*Further useful properties of complex conjugation*}
    9.17 -
    9.18 -lemma continuous_within_cnj: "continuous (at z within s) cnj"
    9.19 -by (metis bounded_linear_cnj linear_continuous_within)
    9.20 -
    9.21 -lemma continuous_on_cnj: "continuous_on s cnj"
    9.22 -by (metis bounded_linear_cnj linear_continuous_on)
    9.23 -
    9.24  subsection {*Some limit theorems about real part of real series etc.*}
    9.25  
    9.26  (*MOVE? But not to Finite_Cartesian_Product*)
    9.27 @@ -521,29 +513,29 @@
    9.28    "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>  
    9.29     \<Longrightarrow> deriv (\<lambda>w. f w + g w) z = deriv f z + deriv g z"
    9.30    unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
    9.31 -  by (auto intro!: DERIV_imp_deriv DERIV_intros)
    9.32 +  by (auto intro!: DERIV_imp_deriv derivative_intros)
    9.33  
    9.34  lemma complex_derivative_diff:
    9.35    "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>  
    9.36     \<Longrightarrow> deriv (\<lambda>w. f w - g w) z = deriv f z - deriv g z"
    9.37    unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
    9.38 -  by (auto intro!: DERIV_imp_deriv DERIV_intros)
    9.39 +  by (auto intro!: DERIV_imp_deriv derivative_intros)
    9.40  
    9.41  lemma complex_derivative_mult:
    9.42    "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>  
    9.43     \<Longrightarrow> deriv (\<lambda>w. f w * g w) z = f z * deriv g z + deriv f z * g z"
    9.44    unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
    9.45 -  by (auto intro!: DERIV_imp_deriv DERIV_intros)
    9.46 +  by (auto intro!: DERIV_imp_deriv derivative_eq_intros)
    9.47  
    9.48  lemma complex_derivative_cmult:
    9.49    "f complex_differentiable at z \<Longrightarrow> deriv (\<lambda>w. c * f w) z = c * deriv f z"
    9.50    unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
    9.51 -  by (auto intro!: DERIV_imp_deriv DERIV_intros)
    9.52 +  by (auto intro!: DERIV_imp_deriv derivative_eq_intros)
    9.53  
    9.54  lemma complex_derivative_cmult_right:
    9.55    "f complex_differentiable at z \<Longrightarrow> deriv (\<lambda>w. f w * c) z = deriv f z * c"
    9.56    unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
    9.57 -  by (auto intro!: DERIV_imp_deriv DERIV_intros)
    9.58 +  by (auto intro!: DERIV_imp_deriv derivative_eq_intros)
    9.59  
    9.60  lemma complex_derivative_transform_within_open:
    9.61    "\<lbrakk>f holomorphic_on s; g holomorphic_on s; open s; z \<in> s; \<And>w. w \<in> s \<Longrightarrow> f w = g w\<rbrakk> 
    9.62 @@ -1037,7 +1029,7 @@
    9.63      then have "((\<lambda>v. (\<Sum>i\<le>n. f i v * (z - v)^i / of_nat (fact i))) 
    9.64                  has_field_derivative f (Suc n) u * (z-u) ^ n / of_nat (fact n))
    9.65                 (at u within s)"
    9.66 -      apply (intro DERIV_intros DERIV_power[THEN DERIV_cong])
    9.67 +      apply (intro derivative_eq_intros)
    9.68        apply (blast intro: assms `u \<in> s`)
    9.69        apply (rule refl)+
    9.70        apply (auto simp: field_simps)
    9.71 @@ -1083,7 +1075,7 @@
    9.72  proof -
    9.73    have twz: "\<And>t. (1 - t) *\<^sub>R w + t *\<^sub>R z = w + t *\<^sub>R (z - w)"
    9.74      by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib)
    9.75 -  note assms[unfolded has_field_derivative_def, has_derivative_intros]
    9.76 +  note assms[unfolded has_field_derivative_def, derivative_intros]
    9.77    show ?thesis
    9.78      apply (cut_tac mvt_simple
    9.79                       [of 0 1 "Re o f o (\<lambda>t. (1 - t) *\<^sub>R w +  t *\<^sub>R z)"
    9.80 @@ -1091,7 +1083,7 @@
    9.81      apply auto
    9.82      apply (rule_tac x="(1 - x) *\<^sub>R w + x *\<^sub>R z" in exI)
    9.83      apply (auto simp add: open_segment_def twz) []
    9.84 -    apply (intro has_derivative_eq_intros has_derivative_at_within)
    9.85 +    apply (intro derivative_eq_intros has_derivative_at_within)
    9.86      apply simp_all
    9.87      apply (simp add: fun_eq_iff real_vector.scale_right_diff_distrib)
    9.88      apply (force simp add: twz closed_segment_def)
    9.89 @@ -1136,7 +1128,7 @@
    9.90                    f (Suc n) u * (z - u) ^ n / of_nat (fact n)" .
    9.91      then have "((\<lambda>u. \<Sum>i = 0..n. f i u * (z - u) ^ i / of_nat (fact i)) has_field_derivative
    9.92                  f (Suc n) u * (z - u) ^ n / of_nat (fact n))  (at u)"
    9.93 -      apply (intro DERIV_intros)+
    9.94 +      apply (intro derivative_eq_intros)+
    9.95        apply (force intro: u assms)
    9.96        apply (rule refl)+
    9.97        apply (auto simp: mult_ac)
    10.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Apr 03 17:16:02 2014 +0200
    10.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Apr 03 17:56:08 2014 +0200
    10.3 @@ -45,7 +45,7 @@
    10.4  
    10.5  lemma has_derivative_add_const:
    10.6    "(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net"
    10.7 -  by (intro has_derivative_eq_intros) auto
    10.8 +  by (intro derivative_eq_intros) auto
    10.9  
   10.10  
   10.11  subsection {* Derivative with composed bilinear function. *}
   10.12 @@ -319,14 +319,14 @@
   10.13  
   10.14  subsection {* The chain rule *}
   10.15  
   10.16 -lemma diff_chain_within[has_derivative_intros]:
   10.17 +lemma diff_chain_within[derivative_intros]:
   10.18    assumes "(f has_derivative f') (at x within s)"
   10.19      and "(g has_derivative g') (at (f x) within (f ` s))"
   10.20    shows "((g \<circ> f) has_derivative (g' \<circ> f'))(at x within s)"
   10.21    using has_derivative_in_compose[OF assms]
   10.22    by (simp add: comp_def)
   10.23  
   10.24 -lemma diff_chain_at[has_derivative_intros]:
   10.25 +lemma diff_chain_at[derivative_intros]:
   10.26    "(f has_derivative f') (at x) \<Longrightarrow>
   10.27      (g has_derivative g') (at (f x)) \<Longrightarrow> ((g \<circ> f) has_derivative (g' \<circ> f')) (at x)"
   10.28    using has_derivative_compose[of f f' x UNIV g g']
   10.29 @@ -544,7 +544,7 @@
   10.30      from min obtain d where d1: "0 < d" and d2: "\<forall>y\<in>ball x d. f x \<le> f y"
   10.31        unfolding eventually_at by (force simp: dist_commute)
   10.32      have "FDERIV (\<lambda>r. x + r *\<^sub>R h) 0 :> (\<lambda>r. r *\<^sub>R h)"
   10.33 -      by (intro has_derivative_eq_intros, auto)
   10.34 +      by (intro derivative_eq_intros) auto
   10.35      then have "FDERIV (\<lambda>r. f (x + r *\<^sub>R h)) 0 :> (\<lambda>k. f' (k *\<^sub>R h))"
   10.36        by (rule has_derivative_compose, simp add: deriv)
   10.37      then have "DERIV (\<lambda>r. f (x + r *\<^sub>R h)) 0 :> f' h"
   10.38 @@ -677,7 +677,7 @@
   10.39      assume x: "x \<in> {a <..< b}"
   10.40      show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative
   10.41          (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
   10.42 -      by (intro has_derivative_intros assms(3)[rule_format,OF x] mult_right_has_derivative)
   10.43 +      by (intro derivative_intros assms(3)[rule_format,OF x])
   10.44    qed (insert assms(1,2), auto intro!: continuous_intros simp: field_simps)
   10.45    then obtain x where
   10.46      "x \<in> {a <..< b}"
   10.47 @@ -815,7 +815,7 @@
   10.48      let ?u = "x + u *\<^sub>R (y - x)"
   10.49      have "(f \<circ> ?p has_derivative (f' ?u) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u within box 0 1)"
   10.50        apply (rule diff_chain_within)
   10.51 -      apply (rule has_derivative_intros)+
   10.52 +      apply (rule derivative_intros)+
   10.53        apply (rule has_derivative_within_subset)
   10.54        apply (rule assms(2)[rule_format])
   10.55        using goal1 *
   10.56 @@ -1538,12 +1538,12 @@
   10.57            unfolding ph' *
   10.58            apply (simp add: comp_def)
   10.59            apply (rule bounded_linear.has_derivative[OF assms(3)])
   10.60 -          apply (rule has_derivative_intros)
   10.61 +          apply (rule derivative_intros)
   10.62            defer
   10.63            apply (rule has_derivative_sub[where g'="\<lambda>x.0",unfolded diff_0_right])
   10.64            apply (rule has_derivative_at_within)
   10.65            using assms(5) and `u \<in> s` `a \<in> s`
   10.66 -          apply (auto intro!: has_derivative_intros bounded_linear.has_derivative[of _ "\<lambda>x. x"] has_derivative_bounded_linear)
   10.67 +          apply (auto intro!: derivative_intros bounded_linear.has_derivative[of _ "\<lambda>x. x"] has_derivative_bounded_linear)
   10.68            done
   10.69          have **: "bounded_linear (\<lambda>x. f' u x - f' a x)" "bounded_linear (\<lambda>x. f' a x - f' u x)"
   10.70            apply (rule_tac[!] bounded_linear_sub)
   10.71 @@ -1600,7 +1600,7 @@
   10.72      fix x
   10.73      assume "x \<in> s"
   10.74      show "((\<lambda>a. f m a - f n a) has_derivative (\<lambda>h. f' m x h - f' n x h)) (at x within s)"
   10.75 -      by (rule has_derivative_intros assms(2)[rule_format] `x\<in>s`)+
   10.76 +      by (rule derivative_intros assms(2)[rule_format] `x\<in>s`)+
   10.77      show "onorm (\<lambda>h. f' m x h - f' n x h) \<le> 2 * e"
   10.78      proof (rule onorm_bound)
   10.79        fix h
   10.80 @@ -1933,44 +1933,58 @@
   10.81    apply auto
   10.82    done
   10.83  
   10.84 -
   10.85  text {* Considering derivative @{typ "real \<Rightarrow> 'b\<Colon>real_normed_vector"} as a vector. *}
   10.86  
   10.87 -definition has_vector_derivative :: "(real \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'b \<Rightarrow> real filter \<Rightarrow> bool"
   10.88 -    (infix "has'_vector'_derivative" 50)
   10.89 -  where "(f has_vector_derivative f') net \<longleftrightarrow> (f has_derivative (\<lambda>x. x *\<^sub>R f')) net"
   10.90 -
   10.91 -definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)"
   10.92 -
   10.93 -lemma vector_derivative_works:
   10.94 -  fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
   10.95 -  shows "f differentiable net \<longleftrightarrow> (f has_vector_derivative (vector_derivative f net)) net"
   10.96 -    (is "?l = ?r")
   10.97 -proof
   10.98 -  assume ?l
   10.99 -  obtain f' where f': "(f has_derivative f') net"
  10.100 -    using `?l` unfolding differentiable_def ..
  10.101 -  then interpret bounded_linear f'
  10.102 -    by auto
  10.103 -  show ?r
  10.104 -    unfolding vector_derivative_def has_vector_derivative_def
  10.105 -    apply -
  10.106 -    apply (rule someI_ex,rule_tac x="f' 1" in exI)
  10.107 -    using f'
  10.108 -    unfolding scaleR[symmetric]
  10.109 -    apply auto
  10.110 -    done
  10.111 -next
  10.112 -  assume ?r
  10.113 -  then show ?l
  10.114 -    unfolding vector_derivative_def has_vector_derivative_def differentiable_def
  10.115 -    by auto
  10.116 -qed
  10.117 -
  10.118  lemma has_field_derivative_iff_has_vector_derivative:
  10.119    "(f has_field_derivative y) F \<longleftrightarrow> (f has_vector_derivative y) F"
  10.120    unfolding has_vector_derivative_def has_field_derivative_def real_scaleR_def mult_commute_abs ..
  10.121  
  10.122 +lemma has_vector_derivative_const[simp, derivative_intros]: "((\<lambda>x. c) has_vector_derivative 0) net"
  10.123 +  by (auto simp: has_vector_derivative_def)
  10.124 +
  10.125 +lemma has_vector_derivative_id[simp, derivative_intros]: "((\<lambda>x. x) has_vector_derivative 1) net"
  10.126 +  by (auto simp: has_vector_derivative_def)
  10.127 +
  10.128 +lemma has_vector_derivative_neg[derivative_intros]:
  10.129 +  "(f has_vector_derivative f') net \<Longrightarrow> ((\<lambda>x. - f x) has_vector_derivative (- f')) net"
  10.130 +  by (auto simp: has_vector_derivative_def)
  10.131 +
  10.132 +lemma has_vector_derivative_add[derivative_intros]:
  10.133 +  "(f has_vector_derivative f') net \<Longrightarrow> (g has_vector_derivative g') net \<Longrightarrow>
  10.134 +    ((\<lambda>x. f x + g x) has_vector_derivative (f' + g')) net"
  10.135 +  by (auto simp: has_vector_derivative_def scaleR_right_distrib)
  10.136 +
  10.137 +lemma has_vector_derivative_sub[derivative_intros]:
  10.138 +  "(f has_vector_derivative f') net \<Longrightarrow> (g has_vector_derivative g') net \<Longrightarrow>
  10.139 +    ((\<lambda>x. f x - g x) has_vector_derivative (f' - g')) net"
  10.140 +  by (auto simp: has_vector_derivative_def scaleR_diff_right)
  10.141 +
  10.142 +lemma (in bounded_linear) has_vector_derivative:
  10.143 +  assumes "(g has_vector_derivative g') (at x within s)"
  10.144 +  shows "((\<lambda>x. f (g x)) has_vector_derivative f g') (at x within s)"
  10.145 +  using has_derivative[OF assms[unfolded has_vector_derivative_def]]
  10.146 +  by (simp add: has_vector_derivative_def scaleR)
  10.147 +
  10.148 +lemma (in bounded_bilinear) has_vector_derivative:
  10.149 +  assumes "(f has_vector_derivative f') (at x within s)"
  10.150 +    and "(g has_vector_derivative g') (at x within s)"
  10.151 +  shows "((\<lambda>x. f x ** g x) has_vector_derivative (f x ** g' + f' ** g x)) (at x within s)"
  10.152 +  using FDERIV[OF assms(1-2)[unfolded has_vector_derivative_def]]
  10.153 +  by (simp add: has_vector_derivative_def scaleR_right scaleR_left scaleR_right_distrib)
  10.154 +
  10.155 +lemma has_vector_derivative_scaleR[derivative_intros]:
  10.156 +  "(f has_field_derivative f') (at x within s) \<Longrightarrow> (g has_vector_derivative g') (at x within s) \<Longrightarrow>
  10.157 +    ((\<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)"
  10.158 +  unfolding has_field_derivative_iff_has_vector_derivative
  10.159 +  by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_scaleR])
  10.160 +
  10.161 +lemma has_vector_derivative_mult[derivative_intros]:
  10.162 +  "(f has_vector_derivative f') (at x within s) \<Longrightarrow> (g has_vector_derivative g') (at x within s) \<Longrightarrow>
  10.163 +    ((\<lambda>x. f x * g x) has_vector_derivative (f x * g' + f' * g x :: 'a :: real_normed_algebra)) (at x within s)"
  10.164 +  by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_mult])
  10.165 +
  10.166 +definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)"
  10.167 +
  10.168  lemma vector_derivative_unique_at:
  10.169    assumes "(f has_vector_derivative f') (at x)"
  10.170      and "(f has_vector_derivative f'') (at x)"
  10.171 @@ -1983,6 +1997,20 @@
  10.172      unfolding fun_eq_iff by auto
  10.173  qed
  10.174  
  10.175 +lemma vector_derivative_works:
  10.176 +  "f differentiable net \<longleftrightarrow> (f has_vector_derivative (vector_derivative f net)) net"
  10.177 +    (is "?l = ?r")
  10.178 +proof
  10.179 +  assume ?l
  10.180 +  obtain f' where f': "(f has_derivative f') net"
  10.181 +    using `?l` unfolding differentiable_def ..
  10.182 +  then interpret bounded_linear f'
  10.183 +    by auto
  10.184 +  show ?r
  10.185 +    unfolding vector_derivative_def has_vector_derivative_def
  10.186 +    by (rule someI[of _ "f' 1"]) (simp add: scaleR[symmetric] f')
  10.187 +qed (auto simp: vector_derivative_def has_vector_derivative_def differentiable_def)
  10.188 +
  10.189  lemma vector_derivative_unique_within_closed_interval:
  10.190    assumes "a < b"
  10.191      and "x \<in> cbox a b"
  10.192 @@ -2028,87 +2056,8 @@
  10.193    done
  10.194  
  10.195  lemma has_vector_derivative_within_subset:
  10.196 -  "(f has_vector_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow>
  10.197 -    (f has_vector_derivative f') (at x within t)"
  10.198 -  unfolding has_vector_derivative_def
  10.199 -  apply (rule has_derivative_within_subset)
  10.200 -  apply auto
  10.201 -  done
  10.202 -
  10.203 -lemma has_vector_derivative_const: "((\<lambda>x. c) has_vector_derivative 0) net"
  10.204 -  unfolding has_vector_derivative_def
  10.205 -  using has_derivative_const
  10.206 -  by auto
  10.207 -
  10.208 -lemma has_vector_derivative_id: "((\<lambda>x::real. x) has_vector_derivative 1) net"
  10.209 -  unfolding has_vector_derivative_def
  10.210 -  using has_derivative_id
  10.211 -  by auto
  10.212 -
  10.213 -lemma has_vector_derivative_cmul:
  10.214 -  "(f has_vector_derivative f') net \<Longrightarrow>
  10.215 -    ((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net"
  10.216 -  unfolding has_vector_derivative_def
  10.217 -  apply (drule scaleR_right_has_derivative)
  10.218 -  apply (auto simp add: algebra_simps)
  10.219 -  done
  10.220 -
  10.221 -lemma has_vector_derivative_cmul_eq:
  10.222 -  assumes "c \<noteq> 0"
  10.223 -  shows "(((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net \<longleftrightarrow> (f has_vector_derivative f') net)"
  10.224 -  apply (rule iffI)
  10.225 -  apply (drule has_vector_derivative_cmul[where c="1/c"])
  10.226 -  apply (rule_tac [2] has_vector_derivative_cmul)
  10.227 -  using assms
  10.228 -  apply auto
  10.229 -  done
  10.230 -
  10.231 -lemma has_vector_derivative_neg:
  10.232 -  "(f has_vector_derivative f') net \<Longrightarrow> ((\<lambda>x. - f x) has_vector_derivative (- f')) net"
  10.233 -  unfolding has_vector_derivative_def
  10.234 -  apply (drule has_derivative_neg)
  10.235 -  apply auto
  10.236 -  done
  10.237 -
  10.238 -lemma has_vector_derivative_add:
  10.239 -  assumes "(f has_vector_derivative f') net"
  10.240 -    and "(g has_vector_derivative g') net"
  10.241 -  shows "((\<lambda>x. f x + g x) has_vector_derivative (f' + g')) net"
  10.242 -  using has_derivative_add[OF assms[unfolded has_vector_derivative_def]]
  10.243 -  unfolding has_vector_derivative_def
  10.244 -  unfolding scaleR_right_distrib
  10.245 -  by auto
  10.246 -
  10.247 -lemma has_vector_derivative_sub:
  10.248 -  assumes "(f has_vector_derivative f') net"
  10.249 -    and "(g has_vector_derivative g') net"
  10.250 -  shows "((\<lambda>x. f x - g x) has_vector_derivative (f' - g')) net"
  10.251 -  using has_derivative_sub[OF assms[unfolded has_vector_derivative_def]]
  10.252 -  unfolding has_vector_derivative_def scaleR_right_diff_distrib
  10.253 -  by auto
  10.254 -
  10.255 -lemma has_vector_derivative_bilinear_within:
  10.256 -  assumes "(f has_vector_derivative f') (at x within s)"
  10.257 -    and "(g has_vector_derivative g') (at x within s)"
  10.258 -  assumes "bounded_bilinear h"
  10.259 -  shows "((\<lambda>x. h (f x) (g x)) has_vector_derivative (h (f x) g' + h f' (g x))) (at x within s)"
  10.260 -proof -
  10.261 -  interpret bounded_bilinear h
  10.262 -    using assms by auto
  10.263 -  show ?thesis
  10.264 -    using has_derivative_bilinear_within[OF assms(1-2)[unfolded has_vector_derivative_def], of h]
  10.265 -    unfolding o_def has_vector_derivative_def
  10.266 -    using assms(3)
  10.267 -    unfolding scaleR_right scaleR_left scaleR_right_distrib
  10.268 -    by auto
  10.269 -qed
  10.270 -
  10.271 -lemma has_vector_derivative_bilinear_at:
  10.272 -  assumes "(f has_vector_derivative f') (at x)"
  10.273 -    and "(g has_vector_derivative g') (at x)"
  10.274 -  assumes "bounded_bilinear h"
  10.275 -  shows "((\<lambda>x. h (f x) (g x)) has_vector_derivative (h (f x) g' + h f' (g x))) (at x)"
  10.276 -  using has_vector_derivative_bilinear_within[OF assms] .
  10.277 +  "(f has_vector_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_vector_derivative f') (at x within t)"
  10.278 +  by (auto simp: has_vector_derivative_def intro: has_derivative_within_subset)
  10.279  
  10.280  lemma has_vector_derivative_at_within:
  10.281    "(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f') (at x within s)"
    11.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Thu Apr 03 17:16:02 2014 +0200
    11.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Apr 03 17:56:08 2014 +0200
    11.3 @@ -8793,11 +8793,10 @@
    11.4        by (auto simp add: algebra_simps)
    11.5      have "(f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x) has_derivative (\<lambda>x. 0) \<circ> (\<lambda>z. (0 - z *\<^sub>R c) + z *\<^sub>R x))
    11.6        (at t within {0 .. 1})"
    11.7 -      apply (rule diff_chain_within)
    11.8 -      apply (rule has_derivative_add)
    11.9 +      apply (intro derivative_eq_intros)
   11.10 +      apply simp_all
   11.11 +      apply (simp add: field_simps)
   11.12        unfolding scaleR_simps
   11.13 -      apply (intro has_derivative_intros)
   11.14 -      apply (intro has_derivative_intros)
   11.15        apply (rule has_derivative_within_subset,rule assms(6)[rule_format])
   11.16        apply (rule *)
   11.17        apply safe
    12.1 --- a/src/HOL/NSA/HDeriv.thy	Thu Apr 03 17:16:02 2014 +0200
    12.2 +++ b/src/HOL/NSA/HDeriv.thy	Thu Apr 03 17:56:08 2014 +0200
    12.3 @@ -34,10 +34,10 @@
    12.4  
    12.5  lemma DERIV_NS_iff:
    12.6        "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NS> D)"
    12.7 -by (simp add: deriv_def LIM_NSLIM_iff)
    12.8 +by (simp add: DERIV_def LIM_NSLIM_iff)
    12.9  
   12.10  lemma NS_DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --NS> D"
   12.11 -by (simp add: deriv_def LIM_NSLIM_iff)
   12.12 +by (simp add: DERIV_def LIM_NSLIM_iff)
   12.13  
   12.14  lemma hnorm_of_hypreal:
   12.15    "\<And>r. hnorm (( *f* of_real) r::'a::real_normed_div_algebra star) = \<bar>r\<bar>"
   12.16 @@ -377,7 +377,7 @@
   12.17  
   12.18  text{*Now equivalence between NSDERIV and DERIV*}
   12.19  lemma NSDERIV_DERIV_iff: "(NSDERIV f x :> D) = (DERIV f x :> D)"
   12.20 -by (simp add: deriv_def NSDERIV_NSLIM_iff LIM_NSLIM_iff)
   12.21 +by (simp add: DERIV_def NSDERIV_NSLIM_iff LIM_NSLIM_iff)
   12.22  
   12.23  (* NS version *)
   12.24  lemma NSDERIV_pow: "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"
    13.1 --- a/src/HOL/NthRoot.thy	Thu Apr 03 17:16:02 2014 +0200
    13.2 +++ b/src/HOL/NthRoot.thy	Thu Apr 03 17:56:08 2014 +0200
    13.3 @@ -326,7 +326,7 @@
    13.4    qed
    13.5  next
    13.6    show "DERIV (\<lambda>x. - (x ^ n)) (root n x) :> - real n * root n x ^ (n - Suc 0)"
    13.7 -    by  (auto intro!: DERIV_intros)
    13.8 +    by  (auto intro!: derivative_eq_intros simp: real_of_nat_def)
    13.9    show "- real n * root n x ^ (n - Suc 0) \<noteq> 0"
   13.10      using n x by simp
   13.11  qed (rule isCont_real_root)
   13.12 @@ -471,8 +471,8 @@
   13.13    using DERIV_real_sqrt_generic by simp
   13.14  
   13.15  declare
   13.16 -  DERIV_real_sqrt_generic[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
   13.17 -  DERIV_real_root_generic[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
   13.18 +  DERIV_real_sqrt_generic[THEN DERIV_chain2, derivative_intros]
   13.19 +  DERIV_real_root_generic[THEN DERIV_chain2, derivative_intros]
   13.20  
   13.21  lemma not_real_square_gt_zero [simp]: "(~ (0::real) < x*x) = (x = 0)"
   13.22  apply auto
    14.1 --- a/src/HOL/Probability/Distributions.thy	Thu Apr 03 17:16:02 2014 +0200
    14.2 +++ b/src/HOL/Probability/Distributions.thy	Thu Apr 03 17:56:08 2014 +0200
    14.3 @@ -52,7 +52,7 @@
    14.4    let ?F = "\<lambda>x. - exp (- x * l)"
    14.5  
    14.6    have deriv: "\<And>x. DERIV ?F x :> ?f x" "\<And>x. 0 \<le> l * exp (- x * l)"
    14.7 -    by (auto intro!: DERIV_intros simp: zero_le_mult_iff)
    14.8 +    by (auto intro!: derivative_eq_intros simp: zero_le_mult_iff)
    14.9  
   14.10    have "emeasure ?D (space ?D) = (\<integral>\<^sup>+ x. ereal (?f x) * indicator {0..} x \<partial>lborel)"
   14.11      by (auto simp: emeasure_density exponential_density_def
   14.12 @@ -178,12 +178,12 @@
   14.13      proof (rule integral_FTC_atLeastAtMost)
   14.14        fix x assume "0 \<le> x" "x \<le> b"
   14.15        show "DERIV (\<lambda>x. x * exp (-x)) x :> exp (-x) - x * exp (-x)"
   14.16 -        by (auto intro!: DERIV_intros)
   14.17 +        by (auto intro!: derivative_eq_intros)
   14.18        show "isCont (\<lambda>x. exp (- x) - x * exp (- x)) x "
   14.19          by (intro continuous_intros)
   14.20      qed fact
   14.21      also have "(\<integral>x. (exp (-x)) * indicator {0 .. b} x \<partial>lborel) = - exp (- b) - - exp (- 0)"
   14.22 -      by (rule integral_FTC_atLeastAtMost) (auto intro!: DERIV_intros)
   14.23 +      by (rule integral_FTC_atLeastAtMost) (auto intro!: derivative_eq_intros)
   14.24      finally show "1 - (inverse (exp b) + b / exp b) = integral\<^sup>L lborel (?f b)"
   14.25        by (auto simp: field_simps exp_minus inverse_eq_divide)
   14.26    qed
   14.27 @@ -374,7 +374,7 @@
   14.28      fix x
   14.29      show "DERIV (\<lambda>x. x\<^sup>2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}"
   14.30        using uniform_distributed_params[OF D]
   14.31 -      by (auto intro!: DERIV_intros)
   14.32 +      by (auto intro!: derivative_eq_intros)
   14.33      show "isCont (\<lambda>x. x / Sigma_Algebra.measure lborel {a..b}) x"
   14.34        using uniform_distributed_params[OF D]
   14.35        by (auto intro!: isCont_divide)
    15.1 --- a/src/HOL/Transcendental.thy	Thu Apr 03 17:16:02 2014 +0200
    15.2 +++ b/src/HOL/Transcendental.thy	Thu Apr 03 17:56:08 2014 +0200
    15.3 @@ -630,7 +630,7 @@
    15.4        and 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
    15.5        and 4: "norm x < norm K"
    15.6    shows "DERIV (\<lambda>x. \<Sum>n. c n * x ^ n) x :> (\<Sum>n. (diffs c) n * x ^ n)"
    15.7 -  unfolding deriv_def
    15.8 +  unfolding DERIV_def
    15.9  proof (rule LIM_zero_cancel)
   15.10    show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x ^ n)) / h
   15.11              - suminf (\<lambda>n. diffs c n * x ^ n)) -- 0 --> 0"
   15.12 @@ -669,7 +669,7 @@
   15.13      and "summable L"
   15.14      and L_def: "\<And>n x y. \<lbrakk> x \<in> { a <..< b} ; y \<in> { a <..< b} \<rbrakk> \<Longrightarrow> \<bar>f x n - f y n\<bar> \<le> L n * \<bar>x - y\<bar>"
   15.15    shows "DERIV (\<lambda> x. suminf (f x)) x0 :> (suminf (f' x0))"
   15.16 -  unfolding deriv_def
   15.17 +  unfolding DERIV_def
   15.18  proof (rule LIM_I)
   15.19    fix r :: real
   15.20    assume "0 < r" hence "0 < r/3" by auto
   15.21 @@ -863,7 +863,7 @@
   15.22        {
   15.23          fix n
   15.24          show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)"
   15.25 -          by (auto intro!: DERIV_intros simp del: power_Suc)
   15.26 +          by (auto intro!: derivative_eq_intros simp del: power_Suc simp: real_of_nat_def)
   15.27        }
   15.28        {
   15.29          fix x
   15.30 @@ -978,7 +978,7 @@
   15.31    apply (simp del: of_real_add)
   15.32    done
   15.33  
   15.34 -declare DERIV_exp[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
   15.35 +declare DERIV_exp[THEN DERIV_chain2, derivative_intros]
   15.36  
   15.37  lemma isCont_exp: "isCont exp x"
   15.38    by (rule DERIV_exp [THEN DERIV_isCont])
   15.39 @@ -1315,7 +1315,7 @@
   15.40  lemma DERIV_ln_divide: "0 < x \<Longrightarrow> DERIV ln x :> 1 / x"
   15.41    by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
   15.42  
   15.43 -declare DERIV_ln_divide[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
   15.44 +declare DERIV_ln_divide[THEN DERIV_chain2, derivative_intros]
   15.45  
   15.46  lemma ln_series:
   15.47    assumes "0 < x" and "x < 2"
   15.48 @@ -1356,7 +1356,7 @@
   15.49      hence "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)"
   15.50        unfolding One_nat_def by auto
   15.51      hence "DERIV (\<lambda>x. suminf (?f (x - 1))) x :> suminf (?f' x)"
   15.52 -      unfolding deriv_def repos .
   15.53 +      unfolding DERIV_def repos .
   15.54      ultimately have "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> (suminf (?f' x) - suminf (?f' x))"
   15.55        by (rule DERIV_diff)
   15.56      thus "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> 0" by auto
   15.57 @@ -1621,7 +1621,7 @@
   15.58  proof -
   15.59    let ?l = "\<lambda>y. ln y - y + 1"
   15.60    have D: "\<And>x. 0 < x \<Longrightarrow> DERIV ?l x :> (1 / x - 1)"
   15.61 -    by (auto intro!: DERIV_intros)
   15.62 +    by (auto intro!: derivative_eq_intros)
   15.63  
   15.64    show ?thesis
   15.65    proof (cases rule: linorder_cases)
   15.66 @@ -1699,9 +1699,9 @@
   15.67    show ?case
   15.68    proof (rule lhospital_at_top_at_top)
   15.69      show "eventually (\<lambda>x. DERIV (\<lambda>x. x ^ Suc k) x :> (real (Suc k) * x^k)) at_top"
   15.70 -      by eventually_elim (intro DERIV_intros, simp, simp)
   15.71 +      by eventually_elim (intro derivative_eq_intros, auto)
   15.72      show "eventually (\<lambda>x. DERIV exp x :> exp x) at_top"
   15.73 -      by eventually_elim (auto intro!: DERIV_intros)
   15.74 +      by eventually_elim auto
   15.75      show "eventually (\<lambda>x. exp x \<noteq> 0) at_top"
   15.76        by auto
   15.77      from tendsto_mult[OF tendsto_const Suc, of "real (Suc k)"]
   15.78 @@ -1825,12 +1825,12 @@
   15.79  proof -
   15.80    def lb \<equiv> "1 / ln b"
   15.81    moreover have "DERIV (\<lambda>y. lb * ln y) x :> lb / x"
   15.82 -    using `x > 0` by (auto intro!: DERIV_intros)
   15.83 +    using `x > 0` by (auto intro!: derivative_eq_intros)
   15.84    ultimately show ?thesis
   15.85      by (simp add: log_def)
   15.86  qed
   15.87  
   15.88 -lemmas DERIV_log[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
   15.89 +lemmas DERIV_log[THEN DERIV_chain2, derivative_intros]
   15.90  
   15.91  lemma powr_log_cancel [simp]: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> a powr (log a x) = x"
   15.92    by (simp add: powr_def log_def)
   15.93 @@ -2180,7 +2180,7 @@
   15.94      summable_minus summable_sin summable_cos)
   15.95    done
   15.96  
   15.97 -declare DERIV_sin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
   15.98 +declare DERIV_sin[THEN DERIV_chain2, derivative_intros]
   15.99  
  15.100  lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
  15.101    unfolding cos_def sin_def
  15.102 @@ -2189,7 +2189,7 @@
  15.103      summable_minus summable_sin summable_cos suminf_minus)
  15.104    done
  15.105  
  15.106 -declare DERIV_cos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
  15.107 +declare DERIV_cos[THEN DERIV_chain2, derivative_intros]
  15.108  
  15.109  lemma isCont_sin: "isCont sin x"
  15.110    by (rule DERIV_sin [THEN DERIV_isCont])
  15.111 @@ -2238,7 +2238,7 @@
  15.112  lemma sin_cos_squared_add [simp]: "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
  15.113  proof -
  15.114    have "\<forall>x. DERIV (\<lambda>x. (sin x)\<^sup>2 + (cos x)\<^sup>2) x :> 0"
  15.115 -    by (auto intro!: DERIV_intros)
  15.116 +    by (auto intro!: derivative_eq_intros)
  15.117    hence "(sin x)\<^sup>2 + (cos x)\<^sup>2 = (sin 0)\<^sup>2 + (cos 0)\<^sup>2"
  15.118      by (rule DERIV_isconst_all)
  15.119    thus "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1" by simp
  15.120 @@ -2276,19 +2276,19 @@
  15.121  
  15.122  lemma DERIV_fun_pow: "DERIV g x :> m ==>
  15.123        DERIV (\<lambda>x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
  15.124 -  by (auto intro!: DERIV_intros)
  15.125 +  by (auto intro!: derivative_eq_intros simp: real_of_nat_def)
  15.126  
  15.127  lemma DERIV_fun_exp:
  15.128       "DERIV g x :> m ==> DERIV (\<lambda>x. exp(g x)) x :> exp(g x) * m"
  15.129 -  by (auto intro!: DERIV_intros)
  15.130 +  by (auto intro!: derivative_intros)
  15.131  
  15.132  lemma DERIV_fun_sin:
  15.133       "DERIV g x :> m ==> DERIV (\<lambda>x. sin(g x)) x :> cos(g x) * m"
  15.134 -  by (auto intro!: DERIV_intros)
  15.135 +  by (auto intro!: derivative_intros)
  15.136  
  15.137  lemma DERIV_fun_cos:
  15.138       "DERIV g x :> m ==> DERIV (\<lambda>x. cos(g x)) x :> -sin(g x) * m"
  15.139 -  by (auto intro!: DERIV_intros)
  15.140 +  by (auto intro!: derivative_eq_intros simp: real_of_nat_def)
  15.141  
  15.142  lemma sin_cos_add_lemma:
  15.143    "(sin (x + y) - (sin x * cos y + cos x * sin y))\<^sup>2 +
  15.144 @@ -2296,7 +2296,7 @@
  15.145    (is "?f x = 0")
  15.146  proof -
  15.147    have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
  15.148 -    by (auto intro!: DERIV_intros simp add: algebra_simps)
  15.149 +    by (auto intro!: derivative_eq_intros simp add: algebra_simps)
  15.150    hence "?f x = ?f 0"
  15.151      by (rule DERIV_isconst_all)
  15.152    thus ?thesis by simp
  15.153 @@ -2312,7 +2312,7 @@
  15.154    "(sin(-x) + sin(x))\<^sup>2 + (cos(-x) - cos(x))\<^sup>2 = 0" (is "?f x = 0")
  15.155  proof -
  15.156    have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
  15.157 -    by (auto intro!: DERIV_intros simp add: algebra_simps)
  15.158 +    by (auto intro!: derivative_eq_intros simp add: algebra_simps)
  15.159    hence "?f x = ?f 0"
  15.160      by (rule DERIV_isconst_all)
  15.161    thus ?thesis by simp
  15.162 @@ -2859,7 +2859,7 @@
  15.163  
  15.164  lemma DERIV_tan [simp]: "cos x \<noteq> 0 \<Longrightarrow> DERIV tan x :> inverse ((cos x)\<^sup>2)"
  15.165    unfolding tan_def
  15.166 -  by (auto intro!: DERIV_intros, simp add: divide_inverse power2_eq_square)
  15.167 +  by (auto intro!: derivative_eq_intros, simp add: divide_inverse power2_eq_square)
  15.168  
  15.169  lemma isCont_tan: "cos x \<noteq> 0 \<Longrightarrow> isCont tan x"
  15.170    by (rule DERIV_tan [THEN DERIV_isCont])
  15.171 @@ -3332,9 +3332,9 @@
  15.172    done
  15.173  
  15.174  declare
  15.175 -  DERIV_arcsin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
  15.176 -  DERIV_arccos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
  15.177 -  DERIV_arctan[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
  15.178 +  DERIV_arcsin[THEN DERIV_chain2, derivative_intros]
  15.179 +  DERIV_arccos[THEN DERIV_chain2, derivative_intros]
  15.180 +  DERIV_arctan[THEN DERIV_chain2, derivative_intros]
  15.181  
  15.182  lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))"
  15.183    by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
  15.184 @@ -3465,7 +3465,7 @@
  15.185    done
  15.186  
  15.187  lemma DERIV_cos_add [simp]: "DERIV (\<lambda>x. cos (x + k)) xa :> - sin (xa + k)"
  15.188 -  by (auto intro!: DERIV_intros)
  15.189 +  by (auto intro!: derivative_eq_intros)
  15.190  
  15.191  lemma sin_zero_abs_cos_one: "sin x = 0 ==> \<bar>cos x\<bar> = 1"
  15.192    by (auto simp add: sin_zero_iff even_mult_two_ex)