unify syntax for has_derivative and differentiable
authorhoelzl
Mon Mar 17 19:12:52 2014 +0100 (2014-03-17)
changeset 561812aa0b19e74f3
parent 56180 fae7a45d0fef
child 56182 528fae0816ea
unify syntax for has_derivative and differentiable
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/Derivative.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Transcendental.thy
     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.53 -  Global_Theory.add_thms_dynamic (@{binding FDERIV_eq_intros},
    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.56 +  Global_Theory.add_thms_dynamic (@{binding has_derivative_eq_intros},
    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.62    by (simp add: has_derivative_def)
    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.80    apply (simp add: local.scaleR local.diff local.add local.zero)
    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.103 -lemma FDERIV_add[simp, FDERIV_intros]:
   1.104 +lemma has_derivative_add[simp, has_derivative_intros]:
   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.111      by (simp add: field_simps scaleR_add_right scaleR_diff_right)
   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.129 -  by (simp only: diff_conv_add_uminus FDERIV_add FDERIV_minus)
   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.141 +  by (simp only: diff_conv_add_uminus has_derivative_add has_derivative_minus)
   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.317        by (intro bounded_linear_add
   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.676    by (simp add: deriv_def)
   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.688 +lemma DERIV_add:
   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.712 +lemma DERIV_add_minus:
   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.847    apply (simp add: real_of_nat_def)
   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.48    apply (simp add: mult_ac)
    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.62  lemma GDERIV_add:
    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.65 -  unfolding gderiv_def inner_add_right by (rule FDERIV_add)
    2.66 +  unfolding gderiv_def inner_add_right by (rule has_derivative_add)
    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.89    apply (simp add: mult_ac)
    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.100    apply (simp add: inner_add mult_ac)
   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.8 -apply (simp add: differentiable_def)
     3.9 +lemma poly_differentiable[simp]: "(%x. poly p x) differentiable (at x::real filter)"
    3.10 +apply (simp add: real_differentiable_def)
    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.29      by (simp add: norm_Pair divide_right_mono order_trans [OF sqrt_add_le_add_sqrt])
    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.18 -lemmas has_derivative_add = FDERIV_add
    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.30 +lemmas has_derivative_add = has_derivative_add
    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.40  lemma has_derivative_add_const:
    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.62 -    apply (simp add: 1 diff_add_eq_diff_diff)
    6.63 +    apply (simp add: 1 diff_add_eq_diff_diff ac_simps)
    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.143    by (simp add: comp_def)
   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.151    by (simp add: comp_def)
   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.193            apply (simp add: comp_def)
   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.5        apply (rule has_derivative_add)
     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
    9.38 -              simp add: differentiable_def)
    9.39 +              simp add: real_differentiable_def)
    9.40    txt{*Now, simulate TRYALL*}
    9.41    apply (rule_tac [!] DERIV_tan asm_rl)
    9.42    apply (auto dest!: DERIV_unique [OF _ DERIV_tan]