author hoelzl Mon Mar 17 19:12:52 2014 +0100 (2014-03-17) changeset 56181 2aa0b19e74f3 parent 56180 fae7a45d0fef child 56182 528fae0816ea
unify syntax for has_derivative and differentiable
 src/HOL/Deriv.thy file | annotate | diff | revisions src/HOL/Library/Inner_Product.thy file | annotate | diff | revisions src/HOL/Library/Poly_Deriv.thy file | annotate | diff | revisions src/HOL/Library/Product_Vector.thy file | annotate | diff | revisions src/HOL/MacLaurin.thy file | annotate | diff | revisions src/HOL/Multivariate_Analysis/Derivative.thy file | annotate | diff | revisions src/HOL/Multivariate_Analysis/Integration.thy file | annotate | diff | revisions src/HOL/Probability/Lebesgue_Measure.thy file | annotate | diff | revisions src/HOL/Transcendental.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Deriv.thy	Mon Mar 17 18:06:59 2014 +0100
1.2 +++ b/src/HOL/Deriv.thy	Mon Mar 17 19:12:52 2014 +0100
1.3 @@ -12,8 +12,9 @@
1.4  imports Limits
1.5  begin
1.6
1.7 +subsection {* Frechet derivative *}
1.8 +
1.9  definition
1.10 -  -- {* Frechet derivative: D is derivative of function f at x within s *}
1.11    has_derivative :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow>  bool"
1.12    (infixl "(has'_derivative)" 12)
1.13  where
1.14 @@ -21,37 +22,54 @@
1.15      (bounded_linear f' \<and>
1.16       ((\<lambda>y. ((f y - f (Lim F (\<lambda>x. x))) - f' (y - Lim F (\<lambda>x. x))) /\<^sub>R norm (y - Lim F (\<lambda>x. x))) ---> 0) F)"
1.17
1.18 -lemma FDERIV_eq_rhs: "(f has_derivative f') F \<Longrightarrow> f' = g' \<Longrightarrow> (f has_derivative g') F"
1.19 +text {*
1.20 +  Usually the filter @{term F} is @{term "at x within s"}.  @{term "(f has_derivative D)
1.21 +  (at x within s)"} means: @{term D} is the derivative of function @{term f} at point @{term x}
1.22 +  within the set @{term s}. Where @{term s} is used to express left or right sided derivatives. In
1.23 +  most cases @{term s} is either a variable or @{term UNIV}.
1.24 +*}
1.25 +
1.26 +text {*
1.27 +  The following syntax is only used as a legacy syntax.
1.28 +*}
1.29 +abbreviation (input)
1.30 +  FDERIV :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow>  ('a \<Rightarrow> 'b) \<Rightarrow> bool"
1.31 +  ("(FDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
1.32 +where
1.33 +  "FDERIV f x :> f' \<equiv> (f has_derivative f') (at x)"
1.34 +
1.35 +
1.36 +lemma has_derivative_eq_rhs: "(f has_derivative f') F \<Longrightarrow> f' = g' \<Longrightarrow> (f has_derivative g') F"
1.37    by simp
1.38
1.39  ML {*
1.40
1.41 -structure FDERIV_Intros = Named_Thms
1.42 +structure has_derivative_Intros = Named_Thms
1.43  (
1.44 -  val name = @{binding FDERIV_intros}
1.45 +  val name = @{binding has_derivative_intros}
1.46    val description = "introduction rules for FDERIV"
1.47  )
1.48
1.49  *}
1.50
1.51  setup {*
1.52 -  FDERIV_Intros.setup #>
1.54 -    map_filter (try (fn thm => @{thm FDERIV_eq_rhs} OF [thm])) o FDERIV_Intros.get o Context.proof_of);
1.55 +  has_derivative_Intros.setup #>
1.57 +    map_filter (try (fn thm => @{thm has_derivative_eq_rhs} OF [thm])) o has_derivative_Intros.get o Context.proof_of);
1.58  *}
1.59
1.60 -lemma FDERIV_bounded_linear: "(f has_derivative f') F \<Longrightarrow> bounded_linear f'"
1.61 +lemma has_derivative_bounded_linear: "(f has_derivative f') F \<Longrightarrow> bounded_linear f'"
1.63
1.64 -lemma FDERIV_ident[FDERIV_intros, simp]: "((\<lambda>x. x) has_derivative (\<lambda>x. x)) F"
1.65 +lemma has_derivative_ident[has_derivative_intros, simp]: "((\<lambda>x. x) has_derivative (\<lambda>x. x)) F"
1.66    by (simp add: has_derivative_def tendsto_const)
1.67
1.68 -lemma FDERIV_const[FDERIV_intros, simp]: "((\<lambda>x. c) has_derivative (\<lambda>x. 0)) F"
1.69 +lemma has_derivative_const[has_derivative_intros, simp]: "((\<lambda>x. c) has_derivative (\<lambda>x. 0)) F"
1.70    by (simp add: has_derivative_def tendsto_const)
1.71
1.72  lemma (in bounded_linear) bounded_linear: "bounded_linear f" ..
1.73
1.74 -lemma (in bounded_linear) FDERIV:
1.75 +lemma (in bounded_linear) has_derivative:
1.76    "(g has_derivative g') F \<Longrightarrow> ((\<lambda>x. f (g x)) has_derivative (\<lambda>x. f (g' x))) F"
1.77    using assms unfolding has_derivative_def
1.78    apply safe
1.79 @@ -60,19 +78,19 @@
1.81    done
1.82
1.83 -lemmas FDERIV_scaleR_right [FDERIV_intros] =
1.84 -  bounded_linear.FDERIV [OF bounded_linear_scaleR_right]
1.85 +lemmas has_derivative_scaleR_right [has_derivative_intros] =
1.86 +  bounded_linear.has_derivative [OF bounded_linear_scaleR_right]
1.87
1.88 -lemmas FDERIV_scaleR_left [FDERIV_intros] =
1.89 -  bounded_linear.FDERIV [OF bounded_linear_scaleR_left]
1.90 +lemmas has_derivative_scaleR_left [has_derivative_intros] =
1.91 +  bounded_linear.has_derivative [OF bounded_linear_scaleR_left]
1.92
1.93 -lemmas FDERIV_mult_right [FDERIV_intros] =
1.94 -  bounded_linear.FDERIV [OF bounded_linear_mult_right]
1.95 +lemmas has_derivative_mult_right [has_derivative_intros] =
1.96 +  bounded_linear.has_derivative [OF bounded_linear_mult_right]
1.97
1.98 -lemmas FDERIV_mult_left [FDERIV_intros] =
1.99 -  bounded_linear.FDERIV [OF bounded_linear_mult_left]
1.100 +lemmas has_derivative_mult_left [has_derivative_intros] =
1.101 +  bounded_linear.has_derivative [OF bounded_linear_mult_left]
1.102
1.105    assumes f: "(f has_derivative f') F" and g: "(g has_derivative g') F"
1.106    shows "((\<lambda>x. f x + g x) has_derivative (\<lambda>x. f' x + g' x)) F"
1.107    unfolding has_derivative_def
1.108 @@ -83,9 +101,9 @@
1.109      using f g by (intro tendsto_add) (auto simp: has_derivative_def)
1.110    then show "(?D (\<lambda>x. f x + g x) (\<lambda>x. f' x + g' x) ---> 0) F"
1.112 -qed (blast intro: bounded_linear_add f g FDERIV_bounded_linear)
1.113 +qed (blast intro: bounded_linear_add f g has_derivative_bounded_linear)
1.114
1.115 -lemma FDERIV_setsum[simp, FDERIV_intros]:
1.116 +lemma has_derivative_setsum[simp, has_derivative_intros]:
1.117    assumes f: "\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) F"
1.118    shows "((\<lambda>x. \<Sum>i\<in>I. f i x) has_derivative (\<lambda>x. \<Sum>i\<in>I. f' i x)) F"
1.119  proof cases
1.120 @@ -93,47 +111,33 @@
1.121      by induct (simp_all add: f)
1.122  qed simp
1.123
1.124 -lemma FDERIV_minus[simp, FDERIV_intros]: "(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. - f x) has_derivative (\<lambda>x. - f' x)) F"
1.125 -  using FDERIV_scaleR_right[of f f' F "-1"] by simp
1.126 -
1.127 -lemma FDERIV_diff[simp, FDERIV_intros]:
1.128 -  "(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"
1.130 +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"
1.131 +  using has_derivative_scaleR_right[of f f' F "-1"] by simp
1.132
1.133 -abbreviation
1.134 -  -- {* Frechet derivative: D is derivative of function f at x within s *}
1.135 -  FDERIV :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow>  ('a \<Rightarrow> 'b) \<Rightarrow> bool"
1.136 -  ("(FDERIV (_)/ (_)/ : (_)/ :> (_))" [1000, 1000, 1000, 60] 60)
1.137 -where
1.138 -  "FDERIV f x : s :> f' \<equiv> (f has_derivative f') (at x within s)"
1.139 +lemma has_derivative_diff[simp, has_derivative_intros]:
1.140 +  "(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"
1.142
1.143 -abbreviation
1.144 -  fderiv_at ::
1.145 -    "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
1.146 -    ("(FDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
1.147 -where
1.148 -  "FDERIV f x :> D \<equiv> FDERIV f x : UNIV :> D"
1.149 -
1.150 -lemma FDERIV_def:
1.151 -  "FDERIV f x : s :> f' \<longleftrightarrow>
1.152 +lemma has_derivative_at_within:
1.153 +  "(f has_derivative f') (at x within s) \<longleftrightarrow>
1.154      (bounded_linear f' \<and> ((\<lambda>y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) ---> 0) (at x within s))"
1.155    by (cases "at x within s = bot") (simp_all add: has_derivative_def Lim_ident_at)
1.156
1.157 -lemma FDERIV_iff_norm:
1.158 -  "FDERIV f x : s :> f' \<longleftrightarrow>
1.159 +lemma has_derivative_iff_norm:
1.160 +  "(f has_derivative f') (at x within s) \<longleftrightarrow>
1.161      (bounded_linear f' \<and> ((\<lambda>y. norm ((f y - f x) - f' (y - x)) / norm (y - x)) ---> 0) (at x within s))"
1.162    using tendsto_norm_zero_iff[of _ "at x within s", where 'b="'b", symmetric]
1.163 -  by (simp add: FDERIV_def divide_inverse ac_simps)
1.164 +  by (simp add: has_derivative_at_within divide_inverse ac_simps)
1.165
1.166 -lemma fderiv_def:
1.167 -  "FDERIV f x :> D = (bounded_linear D \<and> (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0)"
1.168 -  unfolding FDERIV_iff_norm LIM_offset_zero_iff[of _ _ x] by simp
1.169 +lemma has_derivative_at:
1.170 +  "(f has_derivative D) (at x) \<longleftrightarrow> (bounded_linear D \<and> (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0)"
1.171 +  unfolding has_derivative_iff_norm LIM_offset_zero_iff[of _ _ x] by simp
1.172
1.173 -lemma field_fderiv_def:
1.174 +lemma field_has_derivative_at:
1.175    fixes x :: "'a::real_normed_field"
1.176 -  shows "FDERIV f x :> (\<lambda>h. h * D) = (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
1.177 -  apply (unfold fderiv_def)
1.178 -  apply (simp add: bounded_linear_mult_left)
1.179 +  shows "(f has_derivative op * D) (at x) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
1.180 +  apply (unfold has_derivative_at)
1.181 +  apply (simp add: bounded_linear_mult_right)
1.182    apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
1.183    apply (subst diff_divide_distrib)
1.184    apply (subst times_divide_eq_left [symmetric])
1.185 @@ -141,17 +145,17 @@
1.186    apply (simp add: tendsto_norm_zero_iff LIM_zero_iff)
1.187    done
1.188
1.189 -lemma FDERIV_I:
1.190 +lemma has_derivativeI:
1.191    "bounded_linear f' \<Longrightarrow> ((\<lambda>y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) ---> 0) (at x within s) \<Longrightarrow>
1.192 -  FDERIV f x : s :> f'"
1.193 -  by (simp add: FDERIV_def)
1.194 +  (f has_derivative f') (at x within s)"
1.195 +  by (simp add: has_derivative_at_within)
1.196
1.197 -lemma FDERIV_I_sandwich:
1.198 +lemma has_derivativeI_sandwich:
1.199    assumes e: "0 < e" and bounded: "bounded_linear f'"
1.200      and sandwich: "(\<And>y. y \<in> s \<Longrightarrow> y \<noteq> x \<Longrightarrow> dist y x < e \<Longrightarrow> norm ((f y - f x) - f' (y - x)) / norm (y - x) \<le> H y)"
1.201      and "(H ---> 0) (at x within s)"
1.202 -  shows "FDERIV f x : s :> f'"
1.203 -  unfolding FDERIV_iff_norm
1.204 +  shows "(f has_derivative f') (at x within s)"
1.205 +  unfolding has_derivative_iff_norm
1.206  proof safe
1.207    show "((\<lambda>y. norm (f y - f x - f' (y - x)) / norm (y - x)) ---> 0) (at x within s)"
1.208    proof (rule tendsto_sandwich[where f="\<lambda>x. 0"])
1.209 @@ -161,20 +165,20 @@
1.210    qed (auto simp: le_divide_eq tendsto_const)
1.211  qed fact
1.212
1.213 -lemma FDERIV_subset: "FDERIV f x : s :> f' \<Longrightarrow> t \<subseteq> s \<Longrightarrow> FDERIV f x : t :> f'"
1.214 -  by (auto simp add: FDERIV_iff_norm intro: tendsto_within_subset)
1.215 +lemma has_derivative_subset: "(f has_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_derivative f') (at x within t)"
1.216 +  by (auto simp add: has_derivative_iff_norm intro: tendsto_within_subset)
1.217
1.218  subsection {* Continuity *}
1.219
1.220 -lemma FDERIV_continuous:
1.221 -  assumes f: "FDERIV f x : s :> f'"
1.222 +lemma has_derivative_continuous:
1.223 +  assumes f: "(f has_derivative f') (at x within s)"
1.224    shows "continuous (at x within s) f"
1.225  proof -
1.226 -  from f interpret F: bounded_linear f' by (rule FDERIV_bounded_linear)
1.227 +  from f interpret F: bounded_linear f' by (rule has_derivative_bounded_linear)
1.228    note F.tendsto[tendsto_intros]
1.229    let ?L = "\<lambda>f. (f ---> 0) (at x within s)"
1.230    have "?L (\<lambda>y. norm ((f y - f x) - f' (y - x)) / norm (y - x))"
1.231 -    using f unfolding FDERIV_iff_norm by blast
1.232 +    using f unfolding has_derivative_iff_norm by blast
1.233    then have "?L (\<lambda>y. norm ((f y - f x) - f' (y - x)) / norm (y - x) * norm (y - x))" (is ?m)
1.234      by (rule tendsto_mult_zero) (auto intro!: tendsto_eq_intros)
1.235    also have "?m \<longleftrightarrow> ?L (\<lambda>y. norm ((f y - f x) - f' (y - x)))"
1.236 @@ -195,13 +199,13 @@
1.237    unfolding tendsto_def eventually_inf_principal eventually_at_filter
1.238    by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1)
1.239
1.240 -lemma FDERIV_in_compose:
1.241 -  assumes f: "FDERIV f x : s :> f'"
1.242 -  assumes g: "FDERIV g (f x) : (f`s) :> g'"
1.243 -  shows "FDERIV (\<lambda>x. g (f x)) x : s :> (\<lambda>x. g' (f' x))"
1.244 +lemma has_derivative_in_compose:
1.245 +  assumes f: "(f has_derivative f') (at x within s)"
1.246 +  assumes g: "(g has_derivative g') (at (f x) within (f`s))"
1.247 +  shows "((\<lambda>x. g (f x)) has_derivative (\<lambda>x. g' (f' x))) (at x within s)"
1.248  proof -
1.249 -  from f interpret F: bounded_linear f' by (rule FDERIV_bounded_linear)
1.250 -  from g interpret G: bounded_linear g' by (rule FDERIV_bounded_linear)
1.251 +  from f interpret F: bounded_linear f' by (rule has_derivative_bounded_linear)
1.252 +  from g interpret G: bounded_linear g' by (rule has_derivative_bounded_linear)
1.253    from F.bounded obtain kF where kF: "\<And>x. norm (f' x) \<le> norm x * kF" by fast
1.254    from G.bounded obtain kG where kG: "\<And>x. norm (g' x) \<le> norm x * kG" by fast
1.255    note G.tendsto[tendsto_intros]
1.256 @@ -214,9 +218,9 @@
1.257    def Ng \<equiv> "\<lambda>y. ?N g g' (f x) (f y)"
1.258
1.259    show ?thesis
1.260 -  proof (rule FDERIV_I_sandwich[of 1])
1.261 +  proof (rule has_derivativeI_sandwich[of 1])
1.262      show "bounded_linear (\<lambda>x. g' (f' x))"
1.263 -      using f g by (blast intro: bounded_linear_compose FDERIV_bounded_linear)
1.264 +      using f g by (blast intro: bounded_linear_compose has_derivative_bounded_linear)
1.265    next
1.266      fix y::'a assume neq: "y \<noteq> x"
1.267      have "?N ?gf ?gf' x y = norm (g' (?D f f' x y) + ?D g g' (f x) (f y)) / norm (y - x)"
1.268 @@ -237,15 +241,15 @@
1.269      finally show "?N ?gf ?gf' x y \<le> Nf y * kG + Ng y * (Nf y + kF)" .
1.270    next
1.271      have [tendsto_intros]: "?L Nf"
1.272 -      using f unfolding FDERIV_iff_norm Nf_def ..
1.273 +      using f unfolding has_derivative_iff_norm Nf_def ..
1.274      from f have "(f ---> f x) (at x within s)"
1.275 -      by (blast intro: FDERIV_continuous continuous_within[THEN iffD1])
1.276 +      by (blast intro: has_derivative_continuous continuous_within[THEN iffD1])
1.277      then have f': "LIM x at x within s. f x :> inf (nhds (f x)) (principal (f`s))"
1.278        unfolding filterlim_def
1.279        by (simp add: eventually_filtermap eventually_at_filter le_principal)
1.280
1.281      have "((?N g  g' (f x)) ---> 0) (at (f x) within f`s)"
1.282 -      using g unfolding FDERIV_iff_norm ..
1.283 +      using g unfolding has_derivative_iff_norm ..
1.284      then have g': "((?N g  g' (f x)) ---> 0) (inf (nhds (f x)) (principal (f`s)))"
1.285        by (rule tendsto_at_iff_tendsto_nhds_within[THEN iffD1, rotated]) simp
1.286
1.287 @@ -256,15 +260,16 @@
1.288    qed simp
1.289  qed
1.290
1.291 -lemma FDERIV_compose:
1.292 -  "FDERIV f x : s :> f' \<Longrightarrow> FDERIV g (f x) :> g' \<Longrightarrow> FDERIV (\<lambda>x. g (f x)) x : s :> (\<lambda>x. g' (f' x))"
1.293 -  by (blast intro: FDERIV_in_compose FDERIV_subset)
1.294 +lemma has_derivative_compose:
1.295 +  "(f has_derivative f') (at x within s) \<Longrightarrow> (g has_derivative g') (at (f x)) \<Longrightarrow>
1.296 +  ((\<lambda>x. g (f x)) has_derivative (\<lambda>x. g' (f' x))) (at x within s)"
1.297 +  by (blast intro: has_derivative_in_compose has_derivative_subset)
1.298
1.299  lemma (in bounded_bilinear) FDERIV:
1.300 -  assumes f: "FDERIV f x : s :> f'" and g: "FDERIV g x : s :> g'"
1.301 -  shows "FDERIV (\<lambda>x. f x ** g x) x : s :> (\<lambda>h. f x ** g' h + f' h ** g x)"
1.302 +  assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
1.303 +  shows "((\<lambda>x. f x ** g x) has_derivative (\<lambda>h. f x ** g' h + f' h ** g x)) (at x within s)"
1.304  proof -
1.305 -  from bounded_linear.bounded [OF FDERIV_bounded_linear [OF f]]
1.306 +  from bounded_linear.bounded [OF has_derivative_bounded_linear [OF f]]
1.307    obtain KF where norm_F: "\<And>x. norm (f' x) \<le> norm x * KF" by fast
1.308
1.309    from pos_bounded obtain K where K: "0 < K" and norm_prod:
1.310 @@ -278,16 +283,16 @@
1.311    let ?F = "at x within s"
1.312
1.313    show ?thesis
1.314 -  proof (rule FDERIV_I_sandwich[of 1])
1.315 +  proof (rule has_derivativeI_sandwich[of 1])
1.316      show "bounded_linear (\<lambda>h. f x ** g' h + f' h ** g x)"
1.318          bounded_linear_compose [OF bounded_linear_right] bounded_linear_compose [OF bounded_linear_left]
1.319 -        FDERIV_bounded_linear [OF g] FDERIV_bounded_linear [OF f])
1.320 +        has_derivative_bounded_linear [OF g] has_derivative_bounded_linear [OF f])
1.321    next
1.322      from g have "(g ---> g x) ?F"
1.323 -      by (intro continuous_within[THEN iffD1] FDERIV_continuous)
1.324 +      by (intro continuous_within[THEN iffD1] has_derivative_continuous)
1.325      moreover from f g have "(Nf ---> 0) ?F" "(Ng ---> 0) ?F"
1.326 -      by (simp_all add: FDERIV_iff_norm Ng_def Nf_def)
1.327 +      by (simp_all add: has_derivative_iff_norm Ng_def Nf_def)
1.328      ultimately have "(?fun2 ---> norm (f x) * 0 * K + 0 * norm (g x) * K + KF * norm (0::'b) * K) ?F"
1.329        by (intro tendsto_intros) (simp_all add: LIM_zero_iff)
1.330      then show "(?fun2 ---> 0) ?F"
1.331 @@ -309,20 +314,20 @@
1.332    qed simp
1.333  qed
1.334
1.335 -lemmas FDERIV_mult[simp, FDERIV_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_mult]
1.336 -lemmas FDERIV_scaleR[simp, FDERIV_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_scaleR]
1.337 +lemmas has_derivative_mult[simp, has_derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_mult]
1.338 +lemmas has_derivative_scaleR[simp, has_derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_scaleR]
1.339
1.340 -lemma FDERIV_setprod[simp, FDERIV_intros]:
1.341 +lemma has_derivative_setprod[simp, has_derivative_intros]:
1.342    fixes f :: "'i \<Rightarrow> 'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
1.343 -  assumes f: "\<And>i. i \<in> I \<Longrightarrow> FDERIV (f i) x : s :> f' i"
1.344 -  shows "FDERIV (\<lambda>x. \<Prod>i\<in>I. f i x) x : s :> (\<lambda>y. \<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {i}. f j x))"
1.345 +  assumes f: "\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) (at x within s)"
1.346 +  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)"
1.347  proof cases
1.348    assume "finite I" from this f show ?thesis
1.349    proof induct
1.350      case (insert i I)
1.351      let ?P = "\<lambda>y. f i x * (\<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {i}. f j x)) + (f' i y) * (\<Prod>i\<in>I. f i x)"
1.352 -    have "FDERIV (\<lambda>x. f i x * (\<Prod>i\<in>I. f i x)) x : s :> ?P"
1.353 -      using insert by (intro FDERIV_mult) auto
1.354 +    have "((\<lambda>x. f i x * (\<Prod>i\<in>I. f i x)) has_derivative ?P) (at x within s)"
1.355 +      using insert by (intro has_derivative_mult) auto
1.356      also have "?P = (\<lambda>y. \<Sum>i'\<in>insert i I. f' i' y * (\<Prod>j\<in>insert i I - {i'}. f j x))"
1.357        using insert(1,2) by (auto simp add: setsum_right_distrib insert_Diff_if intro!: ext setsum_cong)
1.358      finally show ?case
1.359 @@ -330,18 +335,18 @@
1.360    qed simp
1.361  qed simp
1.362
1.363 -lemma FDERIV_power[simp, FDERIV_intros]:
1.364 +lemma has_derivative_power[simp, has_derivative_intros]:
1.365    fixes f :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
1.366 -  assumes f: "FDERIV f x : s :> f'"
1.367 -  shows "FDERIV  (\<lambda>x. f x^n) x : s :> (\<lambda>y. of_nat n * f' y * f x^(n - 1))"
1.368 -  using FDERIV_setprod[OF f, of "{..< n}"] by (simp add: setprod_constant ac_simps)
1.369 +  assumes f: "(f has_derivative f') (at x within s)"
1.370 +  shows "((\<lambda>x. f x^n) has_derivative (\<lambda>y. of_nat n * f' y * f x^(n - 1))) (at x within s)"
1.371 +  using has_derivative_setprod[OF f, of "{..< n}"] by (simp add: setprod_constant ac_simps)
1.372
1.373 -lemma FDERIV_inverse':
1.374 +lemma has_derivative_inverse':
1.375    fixes x :: "'a::real_normed_div_algebra"
1.376    assumes x: "x \<noteq> 0"
1.377 -  shows "FDERIV inverse x : s :> (\<lambda>h. - (inverse x * h * inverse x))"
1.378 -        (is "FDERIV ?inv x : s :> ?f")
1.379 -proof (rule FDERIV_I_sandwich)
1.380 +  shows "(inverse has_derivative (\<lambda>h. - (inverse x * h * inverse x))) (at x within s)"
1.381 +        (is "(?inv has_derivative ?f) _")
1.382 +proof (rule has_derivativeI_sandwich)
1.383    show "bounded_linear (\<lambda>h. - (?inv x * h * ?inv x))"
1.384      apply (rule bounded_linear_minus)
1.385      apply (rule bounded_linear_mult_const)
1.386 @@ -381,27 +386,27 @@
1.387        norm (?inv y - ?inv x) * norm (?inv x)" .
1.388  qed
1.389
1.390 -lemma FDERIV_inverse[simp, FDERIV_intros]:
1.391 +lemma has_derivative_inverse[simp, has_derivative_intros]:
1.392    fixes f :: "_ \<Rightarrow> 'a::real_normed_div_algebra"
1.393 -  assumes x:  "f x \<noteq> 0" and f: "FDERIV f x : s :> f'"
1.394 -  shows "FDERIV (\<lambda>x. inverse (f x)) x : s :> (\<lambda>h. - (inverse (f x) * f' h * inverse (f x)))"
1.395 -  using FDERIV_compose[OF f FDERIV_inverse', OF x] .
1.396 +  assumes x:  "f x \<noteq> 0" and f: "(f has_derivative f') (at x within s)"
1.397 +  shows "((\<lambda>x. inverse (f x)) has_derivative (\<lambda>h. - (inverse (f x) * f' h * inverse (f x)))) (at x within s)"
1.398 +  using has_derivative_compose[OF f has_derivative_inverse', OF x] .
1.399
1.400 -lemma FDERIV_divide[simp, FDERIV_intros]:
1.401 +lemma has_derivative_divide[simp, has_derivative_intros]:
1.402    fixes f :: "_ \<Rightarrow> 'a::real_normed_div_algebra"
1.403 -  assumes f: "FDERIV f x : s :> f'" and g: "FDERIV g x : s :> g'"
1.404 +  assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
1.405    assumes x: "g x \<noteq> 0"
1.406 -  shows "FDERIV (\<lambda>x. f x / g x) x : s :>
1.407 -                (\<lambda>h. - f x * (inverse (g x) * g' h * inverse (g x)) + f' h / g x)"
1.408 -  using FDERIV_mult[OF f FDERIV_inverse[OF x g]]
1.409 +  shows "((\<lambda>x. f x / g x) has_derivative
1.410 +                (\<lambda>h. - f x * (inverse (g x) * g' h * inverse (g x)) + f' h / g x)) (at x within s)"
1.411 +  using has_derivative_mult[OF f has_derivative_inverse[OF x g]]
1.412    by (simp add: divide_inverse field_simps)
1.413
1.414  text{*Conventional form requires mult-AC laws. Types real and complex only.*}
1.415 -lemma FDERIV_divide'[FDERIV_intros]:
1.416 +
1.417 +lemma has_derivative_divide'[has_derivative_intros]:
1.418    fixes f :: "_ \<Rightarrow> 'a::real_normed_field"
1.419 -  assumes f: "FDERIV f x : s :> f'" and g: "FDERIV g x : s :> g'" and x: "g x \<noteq> 0"
1.420 -  shows "FDERIV (\<lambda>x. f x / g x) x : s :>
1.421 -                (\<lambda>h. (f' h * g x - f x * g' h) / (g x * g x))"
1.422 +  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"
1.423 +  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)"
1.424  proof -
1.425    { fix h
1.426      have "f' h / g x - f x * (inverse (g x) * g' h * inverse (g x)) =
1.427 @@ -409,7 +414,7 @@
1.428        by (simp add: divide_inverse field_simps nonzero_inverse_mult_distrib x)
1.429     }
1.430    then show ?thesis
1.431 -    using FDERIV_divide [OF f g] x
1.432 +    using has_derivative_divide [OF f g] x
1.433      by simp
1.434  qed
1.435
1.436 @@ -417,19 +422,19 @@
1.437
1.438  text {*
1.439
1.440 -This can not generally shown for @{const FDERIV}, as we need to approach the point from
1.441 +This can not generally shown for @{const has_derivative}, as we need to approach the point from
1.442  all directions. There is a proof in @{text Multivariate_Analysis} for @{text euclidean_space}.
1.443
1.444  *}
1.445
1.446 -lemma FDERIV_zero_unique:
1.447 -  assumes "FDERIV (\<lambda>x. 0) x :> F" shows "F = (\<lambda>h. 0)"
1.448 +lemma has_derivative_zero_unique:
1.449 +  assumes "((\<lambda>x. 0) has_derivative F) (at x)" shows "F = (\<lambda>h. 0)"
1.450  proof -
1.451    interpret F: bounded_linear F
1.452 -    using assms by (rule FDERIV_bounded_linear)
1.453 +    using assms by (rule has_derivative_bounded_linear)
1.454    let ?r = "\<lambda>h. norm (F h) / norm h"
1.455    have *: "?r -- 0 --> 0"
1.456 -    using assms unfolding fderiv_def by simp
1.457 +    using assms unfolding has_derivative_at by simp
1.458    show "F = (\<lambda>h. 0)"
1.459    proof
1.460      fix h show "F h = 0"
1.461 @@ -450,264 +455,286 @@
1.462    qed
1.463  qed
1.464
1.465 -lemma FDERIV_unique:
1.466 -  assumes "FDERIV f x :> F" and "FDERIV f x :> F'" shows "F = F'"
1.467 +lemma has_derivative_unique:
1.468 +  assumes "(f has_derivative F) (at x)" and "(f has_derivative F') (at x)" shows "F = F'"
1.469  proof -
1.470 -  have "FDERIV (\<lambda>x. 0) x :> (\<lambda>h. F h - F' h)"
1.471 -    using FDERIV_diff [OF assms] by simp
1.472 +  have "((\<lambda>x. 0) has_derivative (\<lambda>h. F h - F' h)) (at x)"
1.473 +    using has_derivative_diff [OF assms] by simp
1.474    hence "(\<lambda>h. F h - F' h) = (\<lambda>h. 0)"
1.475 -    by (rule FDERIV_zero_unique)
1.476 +    by (rule has_derivative_zero_unique)
1.477    thus "F = F'"
1.478      unfolding fun_eq_iff right_minus_eq .
1.479  qed
1.480
1.481  subsection {* Differentiability predicate *}
1.482
1.483 -definition isDiff :: "'a filter \<Rightarrow> ('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> bool" where
1.484 -  isDiff_def: "isDiff F f \<longleftrightarrow> (\<exists>D. (f has_derivative D) F)"
1.485 -
1.486 -abbreviation differentiable_in :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool"
1.487 -    ("(_) differentiable (_) in (_)"  [1000, 1000, 60] 60) where
1.488 -  "f differentiable x in s \<equiv> isDiff (at x within s) f"
1.489 +definition
1.490 +  differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool"
1.491 +  (infixr "differentiable" 30)
1.492 +where
1.493 +  "f differentiable F \<longleftrightarrow> (\<exists>D. (f has_derivative D) F)"
1.494
1.495 -abbreviation differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool"
1.496 -    (infixl "differentiable" 60) where
1.497 -  "f differentiable x \<equiv> f differentiable x in UNIV"
1.498 +lemma differentiable_subset: "f differentiable (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f differentiable (at x within t)"
1.499 +  unfolding differentiable_def by (blast intro: has_derivative_subset)
1.500
1.501 -lemma differentiable_subset: "f differentiable x in s \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f differentiable x in t"
1.502 -  unfolding isDiff_def by (blast intro: FDERIV_subset)
1.503 +lemma differentiable_ident [simp]: "(\<lambda>x. x) differentiable F"
1.504 +  unfolding differentiable_def by (blast intro: has_derivative_ident)
1.505
1.506 -lemma differentiable_ident [simp]: "isDiff F (\<lambda>x. x)"
1.507 -  unfolding isDiff_def by (blast intro: FDERIV_ident)
1.508 -
1.509 -lemma differentiable_const [simp]: "isDiff F (\<lambda>z. a)"
1.510 -  unfolding isDiff_def by (blast intro: FDERIV_const)
1.511 +lemma differentiable_const [simp]: "(\<lambda>z. a) differentiable F"
1.512 +  unfolding differentiable_def by (blast intro: has_derivative_const)
1.513
1.514  lemma differentiable_in_compose:
1.515 -  "f differentiable (g x) in (g`s) \<Longrightarrow> g differentiable x in s \<Longrightarrow> (\<lambda>x. f (g x)) differentiable x in s"
1.516 -  unfolding isDiff_def by (blast intro: FDERIV_in_compose)
1.517 +  "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)"
1.518 +  unfolding differentiable_def by (blast intro: has_derivative_in_compose)
1.519
1.520  lemma differentiable_compose:
1.521 -  "f differentiable (g x) \<Longrightarrow> g differentiable x in s \<Longrightarrow> (\<lambda>x. f (g x)) differentiable x in s"
1.522 +  "f differentiable (at (g x)) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> (\<lambda>x. f (g x)) differentiable (at x within s)"
1.523    by (blast intro: differentiable_in_compose differentiable_subset)
1.524
1.525  lemma differentiable_sum [simp]:
1.526 -  "isDiff F f \<Longrightarrow> isDiff F g \<Longrightarrow> isDiff F (\<lambda>x. f x + g x)"
1.527 -  unfolding isDiff_def by (blast intro: FDERIV_add)
1.528 +  "f differentiable F \<Longrightarrow> g differentiable F \<Longrightarrow> (\<lambda>x. f x + g x) differentiable F"
1.529 +  unfolding differentiable_def by (blast intro: has_derivative_add)
1.530
1.531  lemma differentiable_minus [simp]:
1.532 -  "isDiff F f \<Longrightarrow> isDiff F (\<lambda>x. - f x)"
1.533 -  unfolding isDiff_def by (blast intro: FDERIV_minus)
1.534 +  "f differentiable F \<Longrightarrow> (\<lambda>x. - f x) differentiable F"
1.535 +  unfolding differentiable_def by (blast intro: has_derivative_minus)
1.536
1.537  lemma differentiable_diff [simp]:
1.538 -  "isDiff F f \<Longrightarrow> isDiff F g \<Longrightarrow> isDiff F (\<lambda>x. f x - g x)"
1.539 -  unfolding isDiff_def by (blast intro: FDERIV_diff)
1.540 +  "f differentiable F \<Longrightarrow> g differentiable F \<Longrightarrow> (\<lambda>x. f x - g x) differentiable F"
1.541 +  unfolding differentiable_def by (blast intro: has_derivative_diff)
1.542
1.543  lemma differentiable_mult [simp]:
1.544    fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_algebra"
1.545 -  shows "f differentiable x in s \<Longrightarrow> g differentiable x in s \<Longrightarrow> (\<lambda>x. f x * g x) differentiable x in s"
1.546 -  unfolding isDiff_def by (blast intro: FDERIV_mult)
1.547 +  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)"
1.548 +  unfolding differentiable_def by (blast intro: has_derivative_mult)
1.549
1.550  lemma differentiable_inverse [simp]:
1.551    fixes f :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
1.552 -  shows "f differentiable x in s \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> (\<lambda>x. inverse (f x)) differentiable x in s"
1.553 -  unfolding isDiff_def by (blast intro: FDERIV_inverse)
1.554 +  shows "f differentiable (at x within s) \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> (\<lambda>x. inverse (f x)) differentiable (at x within s)"
1.555 +  unfolding differentiable_def by (blast intro: has_derivative_inverse)
1.556
1.557  lemma differentiable_divide [simp]:
1.558    fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
1.559 -  shows "f differentiable x in s \<Longrightarrow> g differentiable x in s \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x / g x) differentiable x in s"
1.560 +  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)"
1.561    unfolding divide_inverse using assms by simp
1.562
1.563  lemma differentiable_power [simp]:
1.564    fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
1.565 -  shows "f differentiable x in s \<Longrightarrow> (\<lambda>x. f x ^ n) differentiable x in s"
1.566 -  unfolding isDiff_def by (blast intro: FDERIV_power)
1.567 +  shows "f differentiable (at x within s) \<Longrightarrow> (\<lambda>x. f x ^ n) differentiable (at x within s)"
1.568 +  unfolding differentiable_def by (blast intro: has_derivative_power)
1.569
1.570  lemma differentiable_scaleR [simp]:
1.571 -  "f differentiable x in s \<Longrightarrow> g differentiable x in s \<Longrightarrow> (\<lambda>x. f x *\<^sub>R g x) differentiable x in s"
1.572 -  unfolding isDiff_def by (blast intro: FDERIV_scaleR)
1.573 +  "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)"
1.574 +  unfolding differentiable_def by (blast intro: has_derivative_scaleR)
1.575
1.576  definition
1.577 -  -- {*Differentiation: D is derivative of function f at x*}
1.578 -  deriv ::
1.579 -    "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool"
1.580 -    ("(DERIV (_)/ (_)/ : (_)/ :> (_))" [1000, 1000, 1000, 60] 60)
1.581 +  has_field_derivative :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a filter \<Rightarrow> bool"
1.582 +  (infixl "(has'_field'_derivative)" 12)
1.583  where
1.584 -  deriv_fderiv: "DERIV f x : s :> D = FDERIV f x : s :> (\<lambda>x. x * D)"
1.585 +  "(f has_field_derivative D) F \<longleftrightarrow> (f has_derivative op * D) F"
1.586 +
1.587 +lemma has_derivative_imp_has_field_derivative:
1.588 +  "(f has_derivative D) F \<Longrightarrow> (\<And>x. x * D' = D x) \<Longrightarrow> (f has_field_derivative D') F"
1.589 +  unfolding has_field_derivative_def
1.590 +  by (rule has_derivative_eq_rhs[of f D]) (simp_all add: fun_eq_iff mult_commute)
1.591 +
1.592 +lemma has_field_derivative_imp_has_derivative: "(f has_field_derivative D) F \<Longrightarrow> (f has_derivative op * D) F"
1.593 +  by (simp add: has_field_derivative_def)
1.594
1.595 -abbreviation
1.596 -  -- {*Differentiation: D is derivative of function f at x*}
1.597 -  deriv_at ::
1.598 -    "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
1.599 -    ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
1.600 +abbreviation (input)
1.601 +  deriv :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
1.602 +  ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
1.603  where
1.604 -  "DERIV f x :> D \<equiv> DERIV f x : UNIV :> D"
1.605 +  "DERIV f x :> D \<equiv> (f has_field_derivative D) (at x)"
1.606
1.607 -lemma differentiable_def: "(f::real \<Rightarrow> real) differentiable x in s \<longleftrightarrow> (\<exists>D. DERIV f x : s :> D)"
1.608 +abbreviation
1.609 +  has_real_derivative :: "(real \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> real filter \<Rightarrow> bool"
1.610 +  (infixl "(has'_real'_derivative)" 12)
1.611 +where
1.612 +  "(f has_real_derivative D) F \<equiv> (f has_field_derivative D) F"
1.613 +
1.614 +lemma real_differentiable_def:
1.615 +  "f differentiable at x within s \<longleftrightarrow> (\<exists>D. (f has_real_derivative D) (at x within s))"
1.616  proof safe
1.617 -  assume "f differentiable x in s"
1.618 -  then obtain f' where *: "FDERIV f x : s :> f'"
1.619 -    unfolding isDiff_def by auto
1.620 -  then obtain c where "f' = (\<lambda>x. x * c)"
1.621 -    by (metis real_bounded_linear FDERIV_bounded_linear)
1.622 -  with * show "\<exists>D. DERIV f x : s :> D"
1.623 -    unfolding deriv_fderiv by auto
1.624 -qed (auto simp: isDiff_def deriv_fderiv)
1.625 +  assume "f differentiable at x within s"
1.626 +  then obtain f' where *: "(f has_derivative f') (at x within s)"
1.627 +    unfolding differentiable_def by auto
1.628 +  then obtain c where "f' = (op * c)"
1.629 +    by (metis real_bounded_linear has_derivative_bounded_linear mult_commute fun_eq_iff)
1.630 +  with * show "\<exists>D. (f has_real_derivative D) (at x within s)"
1.631 +    unfolding has_field_derivative_def by auto
1.632 +qed (auto simp: differentiable_def has_field_derivative_def)
1.633
1.634 -lemma differentiableE [elim?]:
1.635 -  fixes f :: "real \<Rightarrow> real"
1.636 -  assumes f: "f differentiable x in s" obtains df where "DERIV f x : s :> df"
1.637 -  using assms by (auto simp: differentiable_def)
1.638 -
1.639 -lemma differentiableD: "(f::real \<Rightarrow> real) differentiable x in s \<Longrightarrow> \<exists>D. DERIV f x : s :> D"
1.640 -  by (auto elim: differentiableE)
1.641 +lemma real_differentiableE [elim?]:
1.642 +  assumes f: "f differentiable (at x within s)" obtains df where "(f has_real_derivative df) (at x within s)"
1.643 +  using assms by (auto simp: real_differentiable_def)
1.644
1.645 -lemma differentiableI: "DERIV f x : s :> D \<Longrightarrow> (f::real \<Rightarrow> real) differentiable x in s"
1.646 -  by (force simp add: differentiable_def)
1.647 +lemma differentiableD: "f differentiable (at x within s) \<Longrightarrow> \<exists>D. (f has_real_derivative D) (at x within s)"
1.648 +  by (auto elim: real_differentiableE)
1.649
1.650 -lemma DERIV_I_FDERIV: "FDERIV f x : s :> F \<Longrightarrow> (\<And>x. x * F' = F x) \<Longrightarrow> DERIV f x : s :> F'"
1.651 -  by (simp add: deriv_fderiv)
1.652 -
1.653 -lemma DERIV_D_FDERIV: "DERIV f x : s :> F \<Longrightarrow> FDERIV f x : s :> (\<lambda>x. x * F)"
1.654 -  by (simp add: deriv_fderiv)
1.655 +lemma differentiableI: "(f has_real_derivative D) (at x within s) \<Longrightarrow> f differentiable (at x within s)"
1.656 +  by (force simp add: real_differentiable_def)
1.657
1.658  lemma deriv_def:
1.659    "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
1.660 -  apply (simp add: deriv_fderiv fderiv_def bounded_linear_mult_left LIM_zero_iff[symmetric, of _ D])
1.661 +  apply (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right LIM_zero_iff[symmetric, of _ D])
1.662    apply (subst (2) tendsto_norm_zero_iff[symmetric])
1.663    apply (rule filterlim_cong)
1.664    apply (simp_all add: eventually_at_filter field_simps nonzero_norm_divide)
1.665    done
1.666
1.667 -subsection {* Derivatives *}
1.668 +lemma mult_commute_abs: "(\<lambda>x. x * c) = op * (c::'a::ab_semigroup_mult)"
1.669 +  by (simp add: fun_eq_iff mult_commute)
1.670
1.671 -lemma DERIV_iff: "(DERIV f x :> D) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
1.672 -  by (simp add: deriv_def)
1.673 +subsection {* Derivatives *}
1.674
1.675  lemma DERIV_D: "DERIV f x :> D \<Longrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
1.677
1.678 -lemma DERIV_const [simp]: "DERIV (\<lambda>x. k) x : s :> 0"
1.679 -  by (rule DERIV_I_FDERIV[OF FDERIV_const]) auto
1.680 +lemma DERIV_const [simp]: "((\<lambda>x. k) has_field_derivative 0) (at x within s)"
1.681 +  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_const]) auto
1.682 +
1.683 +lemma DERIV_ident [simp]: "((\<lambda>x. x) has_field_derivative 1) (at x within s)"
1.684 +  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_ident]) auto
1.685
1.686 -lemma DERIV_ident [simp]: "DERIV (\<lambda>x. x) x : s :> 1"
1.687 -  by (rule DERIV_I_FDERIV[OF FDERIV_ident]) auto
1.689 +  "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
1.690 +  ((\<lambda>x. f x + g x) has_field_derivative D + E) (at x within s)"
1.691 +  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_add])
1.692 +     (auto simp: field_simps mult_commute_abs dest: has_field_derivative_imp_has_derivative)
1.693
1.694 -lemma DERIV_add: "DERIV f x : s :> D \<Longrightarrow> DERIV g x : s :> E \<Longrightarrow> DERIV (\<lambda>x. f x + g x) x : s :> D + E"
1.695 -  by (rule DERIV_I_FDERIV[OF FDERIV_add]) (auto simp: field_simps dest: DERIV_D_FDERIV)
1.696 +lemma DERIV_minus: "(f has_field_derivative D) (at x within s) \<Longrightarrow> ((\<lambda>x. - f x) has_field_derivative -D) (at x within s)"
1.697 +  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_minus])
1.698 +     (auto simp: field_simps mult_commute_abs dest: has_field_derivative_imp_has_derivative)
1.699
1.700 -lemma DERIV_minus: "DERIV f x : s :> D \<Longrightarrow> DERIV (\<lambda>x. - f x) x : s :> - D"
1.701 -  by (rule DERIV_I_FDERIV[OF FDERIV_minus]) (auto simp: field_simps dest: DERIV_D_FDERIV)
1.702 +lemma DERIV_diff:
1.703 +  "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
1.704 +  ((\<lambda>x. f x - g x) has_field_derivative D - E) (at x within s)"
1.705 +  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_diff])
1.706 +     (auto simp: field_simps dest: has_field_derivative_imp_has_derivative)
1.707
1.708 -lemma DERIV_diff: "DERIV f x : s :> D \<Longrightarrow> DERIV g x : s :> E \<Longrightarrow> DERIV (\<lambda>x. f x - g x) x : s :> D - E"
1.709 -  by (rule DERIV_I_FDERIV[OF FDERIV_diff]) (auto simp: field_simps dest: DERIV_D_FDERIV)
1.710 -
1.711 -lemma DERIV_add_minus: "DERIV f x : s :> D \<Longrightarrow> DERIV g x : s :> E \<Longrightarrow> DERIV (\<lambda>x. f x + - g x) x : s :> D + - E"
1.713 +  "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
1.714 +  ((\<lambda>x. f x + - g x) has_field_derivative D + - E) (at x within s)"
1.715    by (simp only: DERIV_add DERIV_minus)
1.716
1.717 -lemma DERIV_continuous: "DERIV f x : s :> D \<Longrightarrow> continuous (at x within s) f"
1.718 -  by (drule FDERIV_continuous[OF DERIV_D_FDERIV]) simp
1.719 +lemma DERIV_continuous: "(f has_field_derivative D) (at x within s) \<Longrightarrow> continuous (at x within s) f"
1.720 +  by (drule has_derivative_continuous[OF has_field_derivative_imp_has_derivative]) simp
1.721
1.722  lemma DERIV_isCont: "DERIV f x :> D \<Longrightarrow> isCont f x"
1.723    by (auto dest!: DERIV_continuous)
1.724
1.725 -lemma DERIV_mult': "DERIV f x : s :> D \<Longrightarrow> DERIV g x : s :> E \<Longrightarrow> DERIV (\<lambda>x. f x * g x) x : s :> f x * E + D * g x"
1.726 -  by (rule DERIV_I_FDERIV[OF FDERIV_mult]) (auto simp: field_simps dest: DERIV_D_FDERIV)
1.727 +lemma DERIV_mult':
1.728 +  "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
1.729 +  ((\<lambda>x. f x * g x) has_field_derivative f x * E + D * g x) (at x within s)"
1.730 +  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_mult])
1.731 +     (auto simp: field_simps mult_commute_abs dest: has_field_derivative_imp_has_derivative)
1.732
1.733 -lemma DERIV_mult: "DERIV f x : s :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (\<lambda>x. f x * g x) x : s :> Da * g x + Db * f x"
1.734 -  by (rule DERIV_I_FDERIV[OF FDERIV_mult]) (auto simp: field_simps dest: DERIV_D_FDERIV)
1.735 +lemma DERIV_mult:
1.736 +  "(f has_field_derivative Da) (at x within s) \<Longrightarrow> (g has_field_derivative Db) (at x within s) \<Longrightarrow>
1.737 +  ((\<lambda>x. f x * g x) has_field_derivative Da * g x + Db * f x) (at x within s)"
1.738 +  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_mult])
1.739 +     (auto simp: field_simps dest: has_field_derivative_imp_has_derivative)
1.740
1.741  text {* Derivative of linear multiplication *}
1.742
1.743  lemma DERIV_cmult:
1.744 -  "DERIV f x : s :> D ==> DERIV (%x. c * f x) x : s :> c*D"
1.745 +  "(f has_field_derivative D) (at x within s) ==> ((\<lambda>x. c * f x) has_field_derivative c * D) (at x within s)"
1.746    by (drule DERIV_mult' [OF DERIV_const], simp)
1.747
1.748  lemma DERIV_cmult_right:
1.749 -  "DERIV f x : s :> D ==> DERIV (%x. f x * c) x : s :> D * c"
1.750 +  "(f has_field_derivative D) (at x within s) ==> ((\<lambda>x. f x * c) has_field_derivative D * c) (at x within s)"
1.751    using DERIV_cmult   by (force simp add: mult_ac)
1.752
1.753 -lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x : s :> c"
1.754 +lemma DERIV_cmult_Id [simp]: "(op * c has_field_derivative c) (at x within s)"
1.755    by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp)
1.756
1.757 -lemma DERIV_cdivide: "DERIV f x : s :> D ==> DERIV (%x. f x / c) x : s :> D / c"
1.758 -  apply (subgoal_tac "DERIV (%x. (1 / c) * f x) x : s :> (1 / c) * D", force)
1.759 -  apply (erule DERIV_cmult)
1.760 -  done
1.761 +lemma DERIV_cdivide:
1.762 +  "(f has_field_derivative D) (at x within s) \<Longrightarrow> ((\<lambda>x. f x / c) has_field_derivative D / c) (at x within s)"
1.763 +  using DERIV_cmult_right[of f D x s "1 / c"] by simp
1.764
1.765  lemma DERIV_unique:
1.766    "DERIV f x :> D \<Longrightarrow> DERIV f x :> E \<Longrightarrow> D = E"
1.767    unfolding deriv_def by (rule LIM_unique)
1.768
1.769 -lemma DERIV_setsum':
1.770 -  "(\<And> n. n \<in> S \<Longrightarrow> DERIV (%x. f x n) x : s :> (f' x n)) \<Longrightarrow> DERIV (\<lambda>x. setsum (f x) S) x : s :> setsum (f' x) S"
1.771 -  by (rule DERIV_I_FDERIV[OF FDERIV_setsum]) (auto simp: setsum_right_distrib dest: DERIV_D_FDERIV)
1.772 -
1.773  lemma DERIV_setsum:
1.774 -  "finite S \<Longrightarrow> (\<And> n. n \<in> S \<Longrightarrow> DERIV (%x. f x n) x : s :> (f' x n)) \<Longrightarrow> DERIV (\<lambda>x. setsum (f x) S) x : s :> setsum (f' x) S"
1.775 -  by (rule DERIV_setsum')
1.776 -
1.777 -lemma DERIV_sumr [rule_format (no_asm)]: (* REMOVE *)
1.778 -     "(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x : s :> (f' r x))
1.779 -      --> DERIV (%x. \<Sum>n=m..<n::nat. f n x :: real) x : s :> (\<Sum>r=m..<n. f' r x)"
1.780 -  by (auto intro: DERIV_setsum)
1.781 +  "(\<And> n. n \<in> S \<Longrightarrow> ((\<lambda>x. f x n) has_field_derivative (f' x n)) F) \<Longrightarrow>
1.782 +    ((\<lambda>x. setsum (f x) S) has_field_derivative setsum (f' x) S) F"
1.783 +  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_setsum])
1.784 +     (auto simp: setsum_right_distrib mult_commute_abs dest: has_field_derivative_imp_has_derivative)
1.785
1.786  lemma DERIV_inverse':
1.787 -  "DERIV f x : s :> D \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> DERIV (\<lambda>x. inverse (f x)) x : s :> - (inverse (f x) * D * inverse (f x))"
1.788 -  by (rule DERIV_I_FDERIV[OF FDERIV_inverse]) (auto dest: DERIV_D_FDERIV)
1.789 +  "(f has_field_derivative D) (at x within s) \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow>
1.790 +  ((\<lambda>x. inverse (f x)) has_field_derivative - (inverse (f x) * D * inverse (f x))) (at x within s)"
1.791 +  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_inverse])
1.792 +     (auto dest: has_field_derivative_imp_has_derivative)
1.793
1.794  text {* Power of @{text "-1"} *}
1.795
1.796  lemma DERIV_inverse:
1.797 -  "x \<noteq> 0 \<Longrightarrow> DERIV (\<lambda>x. inverse(x)) x : s :> - (inverse x ^ Suc (Suc 0))"
1.798 +  "x \<noteq> 0 \<Longrightarrow> ((\<lambda>x. inverse(x)) has_field_derivative - (inverse x ^ Suc (Suc 0))) (at x within s)"
1.799    by (drule DERIV_inverse' [OF DERIV_ident]) simp
1.800
1.801  text {* Derivative of inverse *}
1.802
1.803  lemma DERIV_inverse_fun:
1.804 -  "DERIV f x : s :> d \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> DERIV (\<lambda>x. inverse (f x)) x : s :> (- (d * inverse(f x ^ Suc (Suc 0))))"
1.805 +  "(f has_field_derivative d) (at x within s) \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow>
1.806 +  ((\<lambda>x. inverse (f x)) has_field_derivative (- (d * inverse(f x ^ Suc (Suc 0))))) (at x within s)"
1.807    by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib)
1.808
1.809  text {* Derivative of quotient *}
1.810
1.811  lemma DERIV_divide:
1.812 -  "DERIV f x : s :> D \<Longrightarrow> DERIV g x : s :> E \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow> DERIV (\<lambda>x. f x / g x) x : s :> (D * g x - f x * E) / (g x * g x)"
1.813 -  by (rule DERIV_I_FDERIV[OF FDERIV_divide])
1.814 -     (auto dest: DERIV_D_FDERIV simp: field_simps nonzero_inverse_mult_distrib divide_inverse)
1.815 +  "(f has_field_derivative D) (at x within s) \<Longrightarrow>
1.816 +  (g has_field_derivative E) (at x within s) \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow>
1.817 +  ((\<lambda>x. f x / g x) has_field_derivative (D * g x - f x * E) / (g x * g x)) (at x within s)"
1.818 +  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_divide])
1.819 +     (auto dest: has_field_derivative_imp_has_derivative simp: field_simps nonzero_inverse_mult_distrib divide_inverse)
1.820
1.821  lemma DERIV_quotient:
1.822 -  "DERIV f x : s :> d \<Longrightarrow> DERIV g x : s :> e \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow> DERIV (\<lambda>y. f y / g y) x : s :> (d * g x - (e * f x)) / (g x ^ Suc (Suc 0))"
1.823 +  "(f has_field_derivative d) (at x within s) \<Longrightarrow>
1.824 +  (g has_field_derivative e) (at x within s)\<Longrightarrow> g x \<noteq> 0 \<Longrightarrow>
1.825 +  ((\<lambda>y. f y / g y) has_field_derivative (d * g x - (e * f x)) / (g x ^ Suc (Suc 0))) (at x within s)"
1.826    by (drule (2) DERIV_divide) (simp add: mult_commute)
1.827
1.828  lemma DERIV_power_Suc:
1.829 -  "DERIV f x : s :> D \<Longrightarrow> DERIV (\<lambda>x. f x ^ Suc n) x : s :> (1 + of_nat n) * (D * f x ^ n)"
1.830 -  by (rule DERIV_I_FDERIV[OF FDERIV_power]) (auto simp: deriv_fderiv)
1.831 +  "(f has_field_derivative D) (at x within s) \<Longrightarrow>
1.832 +  ((\<lambda>x. f x ^ Suc n) has_field_derivative (1 + of_nat n) * (D * f x ^ n)) (at x within s)"
1.833 +  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_power])
1.834 +     (auto simp: has_field_derivative_def)
1.835
1.836  lemma DERIV_power:
1.837 -  "DERIV f x : s :> D \<Longrightarrow> DERIV (\<lambda>x. f x ^ n) x : s :> of_nat n * (D * f x ^ (n - Suc 0))"
1.838 -  by (rule DERIV_I_FDERIV[OF FDERIV_power]) (auto simp: deriv_fderiv)
1.839 +  "(f has_field_derivative D) (at x within s) \<Longrightarrow>
1.840 +  ((\<lambda>x. f x ^ n) has_field_derivative of_nat n * (D * f x ^ (n - Suc 0))) (at x within s)"
1.841 +  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_power])
1.842 +     (auto simp: has_field_derivative_def)
1.843
1.844 -lemma DERIV_pow: "DERIV (%x. x ^ n) x : s :> real n * (x ^ (n - Suc 0))"
1.845 +lemma DERIV_pow: "((\<lambda>x. x ^ n) has_field_derivative real n * (x ^ (n - Suc 0))) (at x within s)"
1.846    apply (cut_tac DERIV_power [OF DERIV_ident])
1.848    done
1.849
1.850 -lemma DERIV_chain': "DERIV f x : s :> D \<Longrightarrow> DERIV g (f x) :> E \<Longrightarrow> DERIV (\<lambda>x. g (f x)) x : s :> E * D"
1.851 -  using FDERIV_compose[of f "\<lambda>x. x * D" x s g "\<lambda>x. x * E"]
1.852 -  by (auto simp: deriv_fderiv ac_simps dest: FDERIV_subset)
1.853 +lemma DERIV_chain': "(f has_field_derivative D) (at x within s) \<Longrightarrow> DERIV g (f x) :> E \<Longrightarrow>
1.854 +  ((\<lambda>x. g (f x)) has_field_derivative E * D) (at x within s)"
1.855 +  using has_derivative_compose[of f "op * D" x s g "op * E"]
1.856 +  unfolding has_field_derivative_def mult_commute_abs ac_simps .
1.857
1.858 -corollary DERIV_chain2: "DERIV f (g x) :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (%x. f (g x)) x : s :> Da * Db"
1.859 +corollary DERIV_chain2: "DERIV f (g x) :> Da \<Longrightarrow> (g has_field_derivative Db) (at x within s) \<Longrightarrow>
1.860 +  ((\<lambda>x. f (g x)) has_field_derivative Da * Db) (at x within s)"
1.861    by (rule DERIV_chain')
1.862
1.863  text {* Standard version *}
1.864
1.865 -lemma DERIV_chain: "DERIV f (g x) :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (f o g) x : s :> Da * Db"
1.866 +lemma DERIV_chain:
1.867 +  "DERIV f (g x) :> Da \<Longrightarrow> (g has_field_derivative Db) (at x within s) \<Longrightarrow>
1.868 +  (f o g has_field_derivative Da * Db) (at x within s)"
1.869    by (drule (1) DERIV_chain', simp add: o_def mult_commute)
1.870
1.871  lemma DERIV_image_chain:
1.872 -  "DERIV f (g x) : (g ` s) :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (f o g) x : s :> Da * Db"
1.873 -  using FDERIV_in_compose [of g "\<lambda>x. x * Db" x s f "\<lambda>x. x * Da "]
1.874 -  by (simp add: deriv_fderiv o_def  mult_ac)
1.875 +  "(f has_field_derivative Da) (at (g x) within (g ` s)) \<Longrightarrow> (g has_field_derivative Db) (at x within s) \<Longrightarrow>
1.876 +  (f o g has_field_derivative Da * Db) (at x within s)"
1.877 +  using has_derivative_in_compose [of g "op * Db" x s f "op * Da "]
1.878 +  by (simp add: has_field_derivative_def o_def mult_commute_abs ac_simps)
1.879
1.880  (*These two are from HOL Light: HAS_COMPLEX_DERIVATIVE_CHAIN*)
1.881  lemma DERIV_chain_s:
1.882 @@ -736,7 +763,7 @@
1.883
1.884  setup Deriv_Intros.setup
1.885
1.886 -lemma DERIV_cong: "DERIV f x : s :> X \<Longrightarrow> X = Y \<Longrightarrow> DERIV f x : s :> Y"
1.887 +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)"
1.888    by simp
1.889
1.890  declare
1.891 @@ -781,7 +808,7 @@
1.892
1.893  lemma DERIV_shift:
1.894    "(DERIV f (x + z) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (x + z)) x :> y)"
1.895 -  by (simp add: DERIV_iff field_simps)
1.896 +  by (simp add: deriv_def field_simps)
1.897
1.898  lemma DERIV_mirror:
1.899    "(DERIV f (- x) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (- x::real) :: real) x :> - y)"
1.900 @@ -800,7 +827,7 @@
1.901      let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
1.902      show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
1.903      show "isCont ?g x" using der
1.904 -      by (simp add: isCont_iff DERIV_iff cong: LIM_equal [rule_format])
1.905 +      by (simp add: isCont_iff deriv_def cong: LIM_equal [rule_format])
1.906      show "?g x = l" by simp
1.907    qed
1.908  next
1.909 @@ -808,7 +835,7 @@
1.910    then obtain g where
1.911      "(\<forall>z. f z - f x = g z * (z-x))" and "isCont g x" and "g x = l" by blast
1.912    thus "(DERIV f x :> l)"
1.913 -     by (auto simp add: isCont_iff DERIV_iff cong: LIM_cong)
1.914 +     by (auto simp add: isCont_iff deriv_def cong: LIM_cong)
1.915  qed
1.916
1.917  text {*
1.918 @@ -881,14 +908,14 @@
1.919  lemma DERIV_pos_inc_left:
1.920    fixes f :: "real => real"
1.921    shows "DERIV f x :> l \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d --> f(x - h) < f(x)"
1.922 -  apply (rule DERIV_neg_dec_left [of "%x. - f x" x "-l", simplified])
1.923 +  apply (rule DERIV_neg_dec_left [of "%x. - f x" "-l" x, simplified])
1.924    apply (auto simp add: DERIV_minus)
1.925    done
1.926
1.927  lemma DERIV_neg_dec_right:
1.928    fixes f :: "real => real"
1.929    shows "DERIV f x :> l \<Longrightarrow> l < 0 \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d --> f(x) > f(x + h)"
1.930 -  apply (rule DERIV_pos_inc_right [of "%x. - f x" x "-l", simplified])
1.931 +  apply (rule DERIV_pos_inc_right [of "%x. - f x" "-l" x, simplified])
1.932    apply (auto simp add: DERIV_minus)
1.933    done
1.934
1.935 @@ -963,7 +990,7 @@
1.936    assumes lt: "a < b"
1.937        and eq: "f(a) = f(b)"
1.938        and con: "\<forall>x. a \<le> x & x \<le> b --> isCont f x"
1.939 -      and dif [rule_format]: "\<forall>x. a < x & x < b --> f differentiable x"
1.940 +      and dif [rule_format]: "\<forall>x. a < x & x < b --> f differentiable (at x)"
1.941    shows "\<exists>z::real. a < z & z < b & DERIV f z :> 0"
1.942  proof -
1.943    have le: "a \<le> b" using lt by simp
1.944 @@ -1055,20 +1082,20 @@
1.945  theorem MVT:
1.946    assumes lt:  "a < b"
1.947        and con: "\<forall>x. a \<le> x & x \<le> b --> isCont f x"
1.948 -      and dif [rule_format]: "\<forall>x. a < x & x < b --> f differentiable x"
1.949 +      and dif [rule_format]: "\<forall>x. a < x & x < b --> f differentiable (at x)"
1.950    shows "\<exists>l z::real. a < z & z < b & DERIV f z :> l &
1.951                     (f(b) - f(a) = (b-a) * l)"
1.952  proof -
1.953    let ?F = "%x. f x - ((f b - f a) / (b-a)) * x"
1.954    have contF: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?F x"
1.955      using con by (fast intro: isCont_intros)
1.956 -  have difF: "\<forall>x. a < x \<and> x < b \<longrightarrow> ?F differentiable x"
1.957 +  have difF: "\<forall>x. a < x \<and> x < b \<longrightarrow> ?F differentiable (at x)"
1.958    proof (clarify)
1.959      fix x::real
1.960      assume ax: "a < x" and xb: "x < b"
1.961      from differentiableD [OF dif [OF conjI [OF ax xb]]]
1.962      obtain l where der: "DERIV f x :> l" ..
1.963 -    show "?F differentiable x"
1.964 +    show "?F differentiable (at x)"
1.965        by (rule differentiableI [where D = "l - (f b - f a)/(b-a)"],
1.966            blast intro: DERIV_diff DERIV_cmult_Id der)
1.967    qed
1.968 @@ -1094,7 +1121,7 @@
1.969        ==> \<exists>z::real. a < z & z < b & (f b - f a = (b - a) * f'(z))"
1.970  apply (drule MVT)
1.971  apply (blast intro: DERIV_isCont)
1.972 -apply (force dest: order_less_imp_le simp add: differentiable_def)
1.973 +apply (force dest: order_less_imp_le simp add: real_differentiable_def)
1.974  apply (blast dest: DERIV_unique order_less_imp_le)
1.975  done
1.976
1.977 @@ -1169,7 +1196,7 @@
1.978    shows "[|a \<noteq> b; \<forall>x. DERIV f x :> k |] ==> (f(b) - f(a)) = (b-a) * k"
1.979  apply (rule linorder_cases [of a b], auto)
1.980  apply (drule_tac [!] f = f in MVT)
1.981 -apply (auto dest: DERIV_isCont DERIV_unique simp add: differentiable_def)
1.982 +apply (auto dest: DERIV_isCont DERIV_unique simp add: real_differentiable_def)
1.983  apply (auto dest: DERIV_unique simp add: ring_distribs)
1.984  done
1.985
1.986 @@ -1355,9 +1382,9 @@
1.987    fixes a b :: real
1.988    assumes alb: "a < b"
1.989      and fc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"
1.990 -    and fd: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable x"
1.991 +    and fd: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable (at x)"
1.992      and gc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont g x"
1.993 -    and gd: "\<forall>x. a < x \<and> x < b \<longrightarrow> g differentiable x"
1.994 +    and gd: "\<forall>x. a < x \<and> x < b \<longrightarrow> g differentiable (at x)"
1.995    shows "\<exists>g'c f'c c.
1.996      DERIV g c :> g'c \<and> DERIV f c :> f'c \<and> a < c \<and> c < b \<and> ((f b - f a) * g'c) = ((g b - g a) * f'c)"
1.997  proof -
1.998 @@ -1365,19 +1392,19 @@
1.999    from assms have "a < b" by simp
1.1000    moreover have "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?h x"
1.1001      using fc gc by simp
1.1002 -  moreover have "\<forall>x. a < x \<and> x < b \<longrightarrow> ?h differentiable x"
1.1003 +  moreover have "\<forall>x. a < x \<and> x < b \<longrightarrow> ?h differentiable (at x)"
1.1004      using fd gd by simp
1.1005    ultimately have "\<exists>l z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" by (rule MVT)
1.1006    then obtain l where ldef: "\<exists>z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" ..
1.1007    then obtain c where cdef: "a < c \<and> c < b \<and> DERIV ?h c :> l \<and> ?h b - ?h a = (b - a) * l" ..
1.1008
1.1009    from cdef have cint: "a < c \<and> c < b" by auto
1.1010 -  with gd have "g differentiable c" by simp
1.1011 +  with gd have "g differentiable (at c)" by simp
1.1012    hence "\<exists>D. DERIV g c :> D" by (rule differentiableD)
1.1013    then obtain g'c where g'cdef: "DERIV g c :> g'c" ..
1.1014
1.1015    from cdef have "a < c \<and> c < b" by auto
1.1016 -  with fd have "f differentiable c" by simp
1.1017 +  with fd have "f differentiable (at c)" by simp
1.1018    hence "\<exists>D. DERIV f c :> D" by (rule differentiableD)
1.1019    then obtain f'c where f'cdef: "DERIV f c :> f'c" ..
1.1020
1.1021 @@ -1418,7 +1445,7 @@
1.1022  proof -
1.1023    have "\<exists>g'c f'c c. DERIV g c :> g'c \<and> DERIV f c :> f'c \<and>
1.1024      a < c \<and> c < b \<and> (f b - f a) * g'c = (g b - g a) * f'c"
1.1025 -    using assms by (intro GMVT) (force simp: differentiable_def)+
1.1026 +    using assms by (intro GMVT) (force simp: real_differentiable_def)+
1.1027    then obtain c where "a < c" "c < b" "(f b - f a) * g' c = (g b - g a) * f' c"
1.1028      using DERIV_f DERIV_g by (force dest: DERIV_unique)
1.1029    then show ?thesis
```
```     2.1 --- a/src/HOL/Library/Inner_Product.thy	Mon Mar 17 18:06:59 2014 +0100
2.2 +++ b/src/HOL/Library/Inner_Product.thy	Mon Mar 17 19:12:52 2014 +0100
2.3 @@ -180,7 +180,7 @@
2.4  lemmas isCont_inner [simp] =
2.5    bounded_bilinear.isCont [OF bounded_bilinear_inner]
2.6
2.7 -lemmas FDERIV_inner [FDERIV_intros] =
2.8 +lemmas has_derivative_inner [has_derivative_intros] =
2.9    bounded_bilinear.FDERIV [OF bounded_bilinear_inner]
2.10
2.11  lemmas bounded_linear_inner_left =
2.12 @@ -189,15 +189,15 @@
2.13  lemmas bounded_linear_inner_right =
2.14    bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]
2.15
2.16 -lemmas FDERIV_inner_right [FDERIV_intros] =
2.17 -  bounded_linear.FDERIV [OF bounded_linear_inner_right]
2.18 +lemmas has_derivative_inner_right [has_derivative_intros] =
2.19 +  bounded_linear.has_derivative [OF bounded_linear_inner_right]
2.20
2.21 -lemmas FDERIV_inner_left [FDERIV_intros] =
2.22 -  bounded_linear.FDERIV [OF bounded_linear_inner_left]
2.23 +lemmas has_derivative_inner_left [has_derivative_intros] =
2.24 +  bounded_linear.has_derivative [OF bounded_linear_inner_left]
2.25
2.26  lemma differentiable_inner [simp]:
2.27 -  "f differentiable x in s \<Longrightarrow> g differentiable x in s \<Longrightarrow> (\<lambda>x. inner (f x) (g x)) differentiable x in s"
2.28 -  unfolding isDiff_def by (blast intro: FDERIV_inner)
2.29 +  "f differentiable (at x within s) \<Longrightarrow> g differentiable at x within s \<Longrightarrow> (\<lambda>x. inner (f x) (g x)) differentiable at x within s"
2.30 +  unfolding differentiable_def by (blast intro: has_derivative_inner)
2.31
2.32  subsection {* Class instances *}
2.33
2.34 @@ -273,46 +273,46 @@
2.35    "GDERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. inner h D)"
2.36
2.37  lemma gderiv_deriv [simp]: "GDERIV f x :> D \<longleftrightarrow> DERIV f x :> D"
2.38 -  by (simp only: gderiv_def deriv_fderiv inner_real_def)
2.39 +  by (simp only: gderiv_def has_field_derivative_def inner_real_def mult_commute_abs)
2.40
2.41  lemma GDERIV_DERIV_compose:
2.42      "\<lbrakk>GDERIV f x :> df; DERIV g (f x) :> dg\<rbrakk>
2.43       \<Longrightarrow> GDERIV (\<lambda>x. g (f x)) x :> scaleR dg df"
2.44 -  unfolding gderiv_def deriv_fderiv
2.45 -  apply (drule (1) FDERIV_compose)
2.46 +  unfolding gderiv_def has_field_derivative_def
2.47 +  apply (drule (1) has_derivative_compose)
2.49    done
2.50
2.51 -lemma FDERIV_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d"
2.52 +lemma has_derivative_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d"
2.53    by simp
2.54
2.55  lemma GDERIV_subst: "\<lbrakk>GDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> GDERIV f x :> d"
2.56    by simp
2.57
2.58  lemma GDERIV_const: "GDERIV (\<lambda>x. k) x :> 0"
2.59 -  unfolding gderiv_def inner_zero_right by (rule FDERIV_const)
2.60 +  unfolding gderiv_def inner_zero_right by (rule has_derivative_const)
2.61
2.63      "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
2.64       \<Longrightarrow> GDERIV (\<lambda>x. f x + g x) x :> df + dg"
2.67
2.68  lemma GDERIV_minus:
2.69      "GDERIV f x :> df \<Longrightarrow> GDERIV (\<lambda>x. - f x) x :> - df"
2.70 -  unfolding gderiv_def inner_minus_right by (rule FDERIV_minus)
2.71 +  unfolding gderiv_def inner_minus_right by (rule has_derivative_minus)
2.72
2.73  lemma GDERIV_diff:
2.74      "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
2.75       \<Longrightarrow> GDERIV (\<lambda>x. f x - g x) x :> df - dg"
2.76 -  unfolding gderiv_def inner_diff_right by (rule FDERIV_diff)
2.77 +  unfolding gderiv_def inner_diff_right by (rule has_derivative_diff)
2.78
2.79  lemma GDERIV_scaleR:
2.80      "\<lbrakk>DERIV f x :> df; GDERIV g x :> dg\<rbrakk>
2.81       \<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x
2.82        :> (scaleR (f x) dg + scaleR df (g x))"
2.83 -  unfolding gderiv_def deriv_fderiv inner_add_right inner_scaleR_right
2.84 -  apply (rule FDERIV_subst)
2.85 -  apply (erule (1) FDERIV_scaleR)
2.86 +  unfolding gderiv_def has_field_derivative_def inner_add_right inner_scaleR_right
2.87 +  apply (rule has_derivative_subst)
2.88 +  apply (erule (1) has_derivative_scaleR)
2.90    done
2.91
2.92 @@ -320,8 +320,8 @@
2.93      "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
2.94       \<Longrightarrow> GDERIV (\<lambda>x. f x * g x) x :> scaleR (f x) dg + scaleR (g x) df"
2.95    unfolding gderiv_def
2.96 -  apply (rule FDERIV_subst)
2.97 -  apply (erule (1) FDERIV_mult)
2.98 +  apply (rule has_derivative_subst)
2.99 +  apply (erule (1) has_derivative_mult)
2.101    done
2.102
2.103 @@ -336,7 +336,7 @@
2.104    assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x"
2.105  proof -
2.106    have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
2.107 -    by (intro FDERIV_inner FDERIV_ident)
2.108 +    by (intro has_derivative_inner has_derivative_ident)
2.109    have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
2.110      by (simp add: fun_eq_iff inner_commute)
2.111    have "0 < inner x x" using `x \<noteq> 0` by simp
2.112 @@ -349,12 +349,12 @@
2.113      apply (rule GDERIV_subst [OF _ 4])
2.114      apply (rule GDERIV_DERIV_compose [where g=sqrt and df="scaleR 2 x"])
2.115      apply (subst gderiv_def)
2.116 -    apply (rule FDERIV_subst [OF _ 2])
2.117 +    apply (rule has_derivative_subst [OF _ 2])
2.118      apply (rule 1)
2.119      apply (rule 3)
2.120      done
2.121  qed
2.122
2.123 -lemmas FDERIV_norm = GDERIV_norm [unfolded gderiv_def]
2.124 +lemmas has_derivative_norm = GDERIV_norm [unfolded gderiv_def]
2.125
2.126  end
```
```     3.1 --- a/src/HOL/Library/Poly_Deriv.thy	Mon Mar 17 18:06:59 2014 +0100
3.2 +++ b/src/HOL/Library/Poly_Deriv.thy	Mon Mar 17 19:12:52 2014 +0100
3.3 @@ -106,8 +106,8 @@
3.4
3.5  text{* Consequences of the derivative theorem above*}
3.6
3.7 -lemma poly_differentiable[simp]: "(%x. poly p x) differentiable (x::real)"
3.9 +lemma poly_differentiable[simp]: "(%x. poly p x) differentiable (at x::real filter)"
3.11  apply (blast intro: poly_DERIV)
3.12  done
3.13
```
```     4.1 --- a/src/HOL/Library/Product_Vector.thy	Mon Mar 17 18:06:59 2014 +0100
4.2 +++ b/src/HOL/Library/Product_Vector.thy	Mon Mar 17 19:12:52 2014 +0100
4.3 @@ -478,18 +478,18 @@
4.4
4.5  subsubsection {* Frechet derivatives involving pairs *}
4.6
4.7 -lemma FDERIV_Pair [FDERIV_intros]:
4.8 -  assumes f: "FDERIV f x : s :> f'" and g: "FDERIV g x : s :> g'"
4.9 -  shows "FDERIV (\<lambda>x. (f x, g x)) x : s :> (\<lambda>h. (f' h, g' h))"
4.10 -proof (rule FDERIV_I_sandwich[of 1])
4.11 +lemma has_derivative_Pair [has_derivative_intros]:
4.12 +  assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
4.13 +  shows "((\<lambda>x. (f x, g x)) has_derivative (\<lambda>h. (f' h, g' h))) (at x within s)"
4.14 +proof (rule has_derivativeI_sandwich[of 1])
4.15    show "bounded_linear (\<lambda>h. (f' h, g' h))"
4.16 -    using f g by (intro bounded_linear_Pair FDERIV_bounded_linear)
4.17 +    using f g by (intro bounded_linear_Pair has_derivative_bounded_linear)
4.18    let ?Rf = "\<lambda>y. f y - f x - f' (y - x)"
4.19    let ?Rg = "\<lambda>y. g y - g x - g' (y - x)"
4.20    let ?R = "\<lambda>y. ((f y, g y) - (f x, g x) - (f' (y - x), g' (y - x)))"
4.21
4.22    show "((\<lambda>y. norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)) ---> 0) (at x within s)"
4.23 -    using f g by (intro tendsto_add_zero) (auto simp: FDERIV_iff_norm)
4.24 +    using f g by (intro tendsto_add_zero) (auto simp: has_derivative_iff_norm)
4.25
4.26    fix y :: 'a assume "y \<noteq> x"
4.27    show "norm (?R y) / norm (y - x) \<le> norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)"
4.28 @@ -497,10 +497,10 @@
4.30  qed simp
4.31
4.32 -lemmas FDERIV_fst [FDERIV_intros] = bounded_linear.FDERIV [OF bounded_linear_fst]
4.33 -lemmas FDERIV_snd [FDERIV_intros] = bounded_linear.FDERIV [OF bounded_linear_snd]
4.34 +lemmas has_derivative_fst [has_derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_fst]
4.35 +lemmas has_derivative_snd [has_derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_snd]
4.36
4.37 -lemma FDERIV_split [FDERIV_intros]:
4.38 +lemma has_derivative_split [has_derivative_intros]:
4.39    "((\<lambda>p. f (fst p) (snd p)) has_derivative f') F \<Longrightarrow> ((\<lambda>(a, b). f a b) has_derivative f') F"
4.40    unfolding split_beta' .
4.41
```
```     5.1 --- a/src/HOL/MacLaurin.thy	Mon Mar 17 18:06:59 2014 +0100
5.2 +++ b/src/HOL/MacLaurin.thy	Mon Mar 17 19:12:52 2014 +0100
5.3 @@ -116,7 +116,7 @@
5.4      by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp
5.5
5.6    have differentiable_difg:
5.7 -    "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> difg m differentiable x"
5.8 +    "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> difg m differentiable (at x)"
5.9      by (rule differentiableI [OF difg_Suc [rule_format]]) simp
5.10
5.11    have difg_Suc_eq_0: "\<And>m t. \<lbrakk>m < n; 0 \<le> t; t \<le> h; DERIV (difg m) t :> 0\<rbrakk>
5.12 @@ -135,7 +135,7 @@
5.13        show "difg 0 0 = difg 0 h" by (simp add: difg_0 g2)
5.14        show "\<forall>x. 0 \<le> x \<and> x \<le> h \<longrightarrow> isCont (difg (0\<Colon>nat)) x"
5.15          by (simp add: isCont_difg n)
5.16 -      show "\<forall>x. 0 < x \<and> x < h \<longrightarrow> difg (0\<Colon>nat) differentiable x"
5.17 +      show "\<forall>x. 0 < x \<and> x < h \<longrightarrow> difg (0\<Colon>nat) differentiable (at x)"
5.18          by (simp add: differentiable_difg n)
5.19      qed
5.20    next
5.21 @@ -149,7 +149,7 @@
5.22          using t `Suc m' < n` by (simp add: difg_Suc_eq_0 difg_eq_0)
5.23        show "\<forall>x. 0 \<le> x \<and> x \<le> t \<longrightarrow> isCont (difg (Suc m')) x"
5.24          using `t < h` `Suc m' < n` by (simp add: isCont_difg)
5.25 -      show "\<forall>x. 0 < x \<and> x < t \<longrightarrow> difg (Suc m') differentiable x"
5.26 +      show "\<forall>x. 0 < x \<and> x < t \<longrightarrow> difg (Suc m') differentiable (at x)"
5.27          using `t < h` `Suc m' < n` by (simp add: differentiable_difg)
5.28      qed
5.29      thus ?case
```
```     6.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Mar 17 18:06:59 2014 +0100
6.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Mar 17 19:12:52 2014 +0100
6.3 @@ -43,30 +43,26 @@
6.4  lemma derivative_is_linear: "(f has_derivative f') net \<Longrightarrow> linear f'"
6.5    by (rule derivative_linear [THEN bounded_linear_imp_linear])
6.6
6.7 -lemma DERIV_conv_has_derivative: "(DERIV f x :> f') \<longleftrightarrow> (f has_derivative op * f') (at x)"
6.8 -  using deriv_fderiv[of f x UNIV f'] by (subst (asm) mult_commute)
6.9 -
6.10 -
6.11  subsection {* Derivatives *}
6.12
6.13  subsubsection {* Combining theorems. *}
6.14
6.15 -lemmas has_derivative_id = FDERIV_ident
6.16 -lemmas has_derivative_const = FDERIV_const
6.17 -lemmas has_derivative_neg = FDERIV_minus
6.19 -lemmas has_derivative_sub = FDERIV_diff
6.20 -lemmas has_derivative_setsum = FDERIV_setsum
6.21 -lemmas scaleR_right_has_derivative = FDERIV_scaleR_right
6.22 -lemmas scaleR_left_has_derivative = FDERIV_scaleR_left
6.23 -lemmas inner_right_has_derivative = FDERIV_inner_right
6.24 -lemmas inner_left_has_derivative = FDERIV_inner_left
6.25 -lemmas mult_right_has_derivative = FDERIV_mult_right
6.26 -lemmas mult_left_has_derivative = FDERIV_mult_left
6.27 +lemmas has_derivative_id = has_derivative_ident
6.28 +lemmas has_derivative_const = has_derivative_const
6.29 +lemmas has_derivative_neg = has_derivative_minus
6.31 +lemmas has_derivative_sub = has_derivative_diff
6.32 +lemmas has_derivative_setsum = has_derivative_setsum
6.33 +lemmas scaleR_right_has_derivative = has_derivative_scaleR_right
6.34 +lemmas scaleR_left_has_derivative = has_derivative_scaleR_left
6.35 +lemmas inner_right_has_derivative = has_derivative_inner_right
6.36 +lemmas inner_left_has_derivative = has_derivative_inner_left
6.37 +lemmas mult_right_has_derivative = has_derivative_mult_right
6.38 +lemmas mult_left_has_derivative = has_derivative_mult_left
6.39
6.41    "(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net"
6.42 -  by (intro FDERIV_eq_intros) auto
6.43 +  by (intro has_derivative_eq_intros) auto
6.44
6.45
6.46  subsection {* Derivative with composed bilinear function. *}
6.47 @@ -145,30 +141,30 @@
6.48  subsubsection {*Caratheodory characterization*}
6.49
6.50  lemma DERIV_within_iff:
6.51 -  "(DERIV f a : s :> D) \<longleftrightarrow> ((\<lambda>z. (f z - f a) / (z - a)) ---> D) (at a within s)"
6.52 +  "(f has_field_derivative D) (at a within s) \<longleftrightarrow> ((\<lambda>z. (f z - f a) / (z - a)) ---> D) (at a within s)"
6.53  proof -
6.54    have 1: "\<And>w y. ~(w = a) ==> y / (w - a) - D = (y - (w - a)*D)/(w - a)"
6.55      by (metis divide_diff_eq_iff eq_iff_diff_eq_0)
6.56    show ?thesis
6.57 -    apply (simp add: deriv_fderiv has_derivative_within bounded_linear_mult_left)
6.58 +    apply (simp add: has_field_derivative_def has_derivative_within bounded_linear_mult_right)
6.59      apply (simp add: LIM_zero_iff [where l = D, symmetric])
6.60      apply (simp add: Lim_within dist_norm)
6.61      apply (simp add: nonzero_norm_divide [symmetric])
6.64      done
6.65  qed
6.66
6.67  lemma DERIV_caratheodory_within:
6.68 -  "(DERIV f x : s :> l) \<longleftrightarrow>
6.69 +  "(f has_field_derivative l) (at x within s) \<longleftrightarrow>
6.70     (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> continuous (at x within s) g \<and> g x = l)"
6.71        (is "?lhs = ?rhs")
6.72  proof
6.73 -  assume der: "DERIV f x : s :> l"
6.74 +  assume ?lhs
6.75    show ?rhs
6.76    proof (intro exI conjI)
6.77      let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
6.78      show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
6.79 -    show "continuous (at x within s) ?g" using der
6.80 +    show "continuous (at x within s) ?g" using `?lhs`
6.81        by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
6.82      show "?g x = l" by simp
6.83    qed
6.84 @@ -176,7 +172,7 @@
6.85    assume ?rhs
6.86    then obtain g where
6.87      "(\<forall>z. f z - f x = g z * (z-x))" and "continuous (at x within s) g" and "g x = l" by blast
6.88 -  thus "(DERIV f x : s :> l)"
6.89 +  thus ?lhs
6.90      by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
6.91  qed
6.92
6.93 @@ -221,20 +217,11 @@
6.94
6.95  subsection {* Differentiability *}
6.96
6.97 -no_notation Deriv.differentiable (infixl "differentiable" 60)
6.98 -
6.99 -abbreviation
6.100 -  differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool"
6.101 -    (infixr "differentiable" 30)
6.102 -  where "f differentiable net \<equiv> isDiff net f"
6.103 -
6.104  definition
6.105    differentiable_on :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a set \<Rightarrow> bool"
6.106      (infixr "differentiable'_on" 30)
6.107    where "f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable (at x within s))"
6.108
6.109 -lemmas differentiable_def = isDiff_def
6.110 -
6.111  lemma differentiableI: "(f has_derivative f') net \<Longrightarrow> f differentiable net"
6.112    unfolding differentiable_def
6.113    by auto
6.114 @@ -286,7 +273,7 @@
6.115    unfolding frechet_derivative_def differentiable_def
6.116    unfolding some_eq_ex[of "\<lambda> f' . (f has_derivative f') net"] ..
6.117
6.118 -lemma linear_frechet_derivative: "f differentiable net \<Longrightarrow> linear(frechet_derivative f net)"
6.119 +lemma linear_frechet_derivative: "f differentiable net \<Longrightarrow> linear (frechet_derivative f net)"
6.120    unfolding frechet_derivative_works has_derivative_def
6.121    by (auto intro: bounded_linear_imp_linear)
6.122
6.123 @@ -295,7 +282,7 @@
6.124
6.125  lemma differentiable_imp_continuous_within:
6.126    "f differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
6.127 -  by (auto simp: differentiable_def intro: FDERIV_continuous)
6.128 +  by (auto simp: differentiable_def intro: has_derivative_continuous)
6.129
6.130  lemma differentiable_imp_continuous_on:
6.131    "f differentiable_on s \<Longrightarrow> continuous_on s f"
6.132 @@ -361,17 +348,17 @@
6.133
6.134  subsection {* The chain rule *}
6.135
6.136 -lemma diff_chain_within[FDERIV_intros]:
6.137 +lemma diff_chain_within[has_derivative_intros]:
6.138    assumes "(f has_derivative f') (at x within s)"
6.139      and "(g has_derivative g') (at (f x) within (f ` s))"
6.140    shows "((g \<circ> f) has_derivative (g' \<circ> f'))(at x within s)"
6.141 -  using FDERIV_in_compose[OF assms]
6.142 +  using has_derivative_in_compose[OF assms]
6.144
6.145 -lemma diff_chain_at[FDERIV_intros]:
6.146 +lemma diff_chain_at[has_derivative_intros]:
6.147    "(f has_derivative f') (at x) \<Longrightarrow>
6.148      (g has_derivative g') (at (f x)) \<Longrightarrow> ((g \<circ> f) has_derivative (g' \<circ> f')) (at x)"
6.149 -  using FDERIV_compose[of f f' x UNIV g g']
6.150 +  using has_derivative_compose[of f f' x UNIV g g']
6.152
6.153
6.154 @@ -468,7 +455,7 @@
6.155
6.156  lemma frechet_derivative_unique_at:
6.157    "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f'') (at x) \<Longrightarrow> f' = f''"
6.158 -  by (rule FDERIV_unique)
6.159 +  by (rule has_derivative_unique)
6.160
6.161  lemma frechet_derivative_unique_within_closed_interval:
6.162    fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
6.163 @@ -719,7 +706,7 @@
6.164      assume "x \<in> box a b" hence x: "x \<in> {a<..<b}" by (simp add: box_real)
6.165      show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative
6.166          (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
6.167 -      by (intro FDERIV_intros assms(3)[rule_format,OF x] mult_right_has_derivative)
6.168 +      by (intro has_derivative_intros assms(3)[rule_format,OF x] mult_right_has_derivative)
6.169    qed (insert assms(1,2), auto intro!: continuous_on_intros simp: field_simps)
6.170    then obtain x where
6.171      "x \<in> box a b"
6.172 @@ -789,7 +776,7 @@
6.173      apply (rule assms(1))
6.174      apply (rule continuous_on_inner continuous_on_intros assms(2) ballI)+
6.175      unfolding o_def
6.176 -    apply (rule FDERIV_inner_right)
6.177 +    apply (rule has_derivative_inner_right)
6.178      using assms(3)
6.179      apply auto
6.180      done
6.181 @@ -857,7 +844,7 @@
6.182      let ?u = "x + u *\<^sub>R (y - x)"
6.183      have "(f \<circ> ?p has_derivative (f' ?u) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u within {0<..<1})"
6.184        apply (rule diff_chain_within)
6.185 -      apply (rule FDERIV_intros)+
6.186 +      apply (rule has_derivative_intros)+
6.187        apply (rule has_derivative_within_subset)
6.188        apply (rule assms(2)[rule_format])
6.189        using goal1 *
6.190 @@ -1585,13 +1572,13 @@
6.191          show "(ph has_derivative (\<lambda>v. v - g' (f' u v))) (at u within ball a d)"
6.192            unfolding ph' *
6.194 -          apply (rule bounded_linear.FDERIV[OF assms(3)])
6.195 -          apply (rule FDERIV_intros)
6.196 +          apply (rule bounded_linear.has_derivative[OF assms(3)])
6.197 +          apply (rule has_derivative_intros)
6.198            defer
6.199            apply (rule has_derivative_sub[where g'="\<lambda>x.0",unfolded diff_0_right])
6.200            apply (rule has_derivative_at_within)
6.201            using assms(5) and `u \<in> s` `a \<in> s`
6.202 -          apply (auto intro!: FDERIV_intros bounded_linear.FDERIV[of _ "\<lambda>x. x"] derivative_linear)
6.203 +          apply (auto intro!: has_derivative_intros bounded_linear.has_derivative[of _ "\<lambda>x. x"] derivative_linear)
6.204            done
6.205          have **: "bounded_linear (\<lambda>x. f' u x - f' a x)" "bounded_linear (\<lambda>x. f' a x - f' u x)"
6.206            apply (rule_tac[!] bounded_linear_sub)
6.207 @@ -1648,7 +1635,7 @@
6.208      fix x
6.209      assume "x \<in> s"
6.210      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)"
6.211 -      by (rule FDERIV_intros assms(2)[rule_format] `x\<in>s`)+
6.212 +      by (rule has_derivative_intros assms(2)[rule_format] `x\<in>s`)+
6.213      {
6.214        fix h
6.215        have "norm (f' m x h - f' n x h) \<le> norm (f' m x h - g' x h) + norm (f' n x h - g' x h)"
6.216 @@ -1956,11 +1943,11 @@
6.217      (\<forall>h. norm(f' x h - g' x h) \<le> inverse (real (Suc n)) * norm h)"
6.218      by (metis assms(2) inverse_positive_iff_positive real_of_nat_Suc_gt_zero)
6.219    obtain f where
6.220 -    *: "\<forall>x. \<exists>f'. \<forall>xa\<in>s. FDERIV (f x) xa : s :> f' xa \<and>
6.221 +    *: "\<forall>x. \<exists>f'. \<forall>xa\<in>s. (f x has_derivative f' xa) (at xa within s) \<and>
6.222        (\<forall>h. norm (f' xa h - g' xa h) \<le> inverse (real (Suc x)) * norm h)"
6.223      using *[THEN choice] ..
6.224    obtain f' where
6.225 -    f: "\<forall>x. \<forall>xa\<in>s. FDERIV (f x) xa : s :> f' x xa \<and>
6.226 +    f: "\<forall>x. \<forall>xa\<in>s. (f x has_derivative f' x xa) (at xa within s) \<and>
6.227        (\<forall>h. norm (f' x xa h - g' xa h) \<le> inverse (real (Suc x)) * norm h)"
6.228      using *[THEN choice] ..
6.229    show ?thesis
6.230 @@ -2050,15 +2037,9 @@
6.231      by auto
6.232  qed
6.233
6.234 -lemma has_vector_derivative_withinI_DERIV:
6.235 -  assumes f: "DERIV f x :> y"
6.236 -  shows "(f has_vector_derivative y) (at x within s)"
6.237 -  unfolding has_vector_derivative_def real_scaleR_def
6.238 -  apply (rule has_derivative_at_within)
6.239 -  using DERIV_conv_has_derivative[THEN iffD1, OF f]
6.240 -  apply (subst mult_commute)
6.241 -  apply assumption
6.242 -  done
6.243 +lemma has_field_derivative_iff_has_vector_derivative:
6.244 +  "(f has_field_derivative y) F \<longleftrightarrow> (f has_vector_derivative y) F"
6.245 +  unfolding has_vector_derivative_def has_field_derivative_def real_scaleR_def mult_commute_abs ..
6.246
6.247  lemma vector_derivative_unique_at:
6.248    assumes "(f has_vector_derivative f') (at x)"
```
```     7.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Mar 17 18:06:59 2014 +0100
7.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Mar 17 19:12:52 2014 +0100
7.3 @@ -8634,8 +8634,8 @@
7.4        apply (rule diff_chain_within)
7.6        unfolding scaleR_simps
7.7 -      apply (intro FDERIV_intros)
7.8 -      apply (intro FDERIV_intros)
7.9 +      apply (intro has_derivative_intros)
7.10 +      apply (intro has_derivative_intros)
7.11        apply (rule has_derivative_within_subset,rule assms(6)[rule_format])
7.12        apply (rule *)
7.13        apply safe
```
```     8.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Mon Mar 17 18:06:59 2014 +0100
8.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Mon Mar 17 19:12:52 2014 +0100
8.3 @@ -1057,6 +1057,10 @@
8.4    qed
8.5  qed simp
8.6
8.7 +lemma has_field_derivative_subset:
8.8 +  "(f has_field_derivative y) (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_field_derivative y) (at x within t)"
8.9 +  unfolding has_field_derivative_def by (rule has_derivative_subset)
8.10 +
8.11  lemma integral_FTC_atLeastAtMost:
8.12    fixes a b :: real
8.13    assumes "a \<le> b"
8.14 @@ -1070,7 +1074,9 @@
8.15      by (rule borel_integral_has_integral)
8.16    moreover
8.17    have "(f has_integral F b - F a) {a .. b}"
8.18 -    by (intro fundamental_theorem_of_calculus has_vector_derivative_withinI_DERIV ballI assms) auto
8.19 +    by (intro fundamental_theorem_of_calculus)
8.20 +       (auto simp: has_field_derivative_iff_has_vector_derivative[symmetric]
8.21 +             intro: has_field_derivative_subset[OF F] assms(1))
8.22    then have "(?f has_integral F b - F a) {a .. b}"
8.23      by (subst has_integral_eq_eq[where g=f]) auto
8.24    then have "(?f has_integral F b - F a) UNIV"
8.25 @@ -1091,7 +1097,9 @@
8.26    shows "(\<integral>\<^sup>+x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a"
8.27  proof -
8.28    have i: "(f has_integral F b - F a) {a..b}"
8.29 -    by (intro fundamental_theorem_of_calculus ballI has_vector_derivative_withinI_DERIV assms)
8.30 +    by (intro fundamental_theorem_of_calculus)
8.31 +       (auto simp: has_field_derivative_iff_has_vector_derivative[symmetric]
8.32 +             intro: has_field_derivative_subset[OF f(1)] `a \<le> b`)
8.33    have i: "((\<lambda>x. f x * indicator {a..b} x) has_integral F b - F a) {a..b}"
8.34      by (rule has_integral_eq[OF _ i]) auto
8.35    have i: "((\<lambda>x. f x * indicator {a..b} x) has_integral F b - F a) UNIV"
```
```     9.1 --- a/src/HOL/Transcendental.thy	Mon Mar 17 18:06:59 2014 +0100
9.2 +++ b/src/HOL/Transcendental.thy	Mon Mar 17 19:12:52 2014 +0100
9.3 @@ -1383,7 +1383,7 @@
9.4      hence "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)"
9.5        unfolding One_nat_def by auto
9.6      hence "DERIV (\<lambda>x. suminf (?f (x - 1))) x :> suminf (?f' x)"
9.7 -      unfolding DERIV_iff repos .
9.8 +      unfolding deriv_def repos .
9.9      ultimately have "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> (suminf (?f' x) - suminf (?f' x))"
9.10        by (rule DERIV_diff)
9.11      thus "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> 0" by auto
9.12 @@ -2485,8 +2485,8 @@
9.13    fix x y
9.14    assume x: "0 \<le> x \<and> x \<le> 2 \<and> cos x = 0"
9.15    assume y: "0 \<le> y \<and> y \<le> 2 \<and> cos y = 0"
9.16 -  have [simp]: "\<forall>x. cos differentiable x"
9.17 -    unfolding differentiable_def by (auto intro: DERIV_cos)
9.18 +  have [simp]: "\<forall>x. cos differentiable (at x)"
9.19 +    unfolding real_differentiable_def by (auto intro: DERIV_cos)
9.20    from x y show "x = y"
9.21      apply (cut_tac less_linear [of x y], auto)
9.22      apply (drule_tac f = cos in Rolle)
9.23 @@ -2661,8 +2661,8 @@
9.24    fix a b
9.25    assume a: "0 \<le> a \<and> a \<le> pi \<and> cos a = y"
9.26    assume b: "0 \<le> b \<and> b \<le> pi \<and> cos b = y"
9.27 -  have [simp]: "\<forall>x. cos differentiable x"
9.28 -    unfolding differentiable_def by (auto intro: DERIV_cos)
9.29 +  have [simp]: "\<forall>x. cos differentiable (at x)"
9.30 +    unfolding real_differentiable_def by (auto intro: DERIV_cos)
9.31    from a b show "a = b"
9.32      apply (cut_tac less_linear [of a b], auto)
9.33      apply (drule_tac f = cos in Rolle)
9.34 @@ -2949,7 +2949,7 @@
9.35    apply (rule_tac [4] Rolle)
9.36    apply (rule_tac [2] Rolle)
9.37    apply (auto del: exI intro!: DERIV_tan DERIV_isCont exI