# HG changeset patch
# User hoelzl
# Date 1365509087 -7200
# Node ID 400ec5ae7f8f15012d5f7822a57d9684077d83b1
# Parent  cd05e9fcc63dbb7dd33198752178013791d3e3cf
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative

diff -r cd05e9fcc63d -r 400ec5ae7f8f src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Tue Apr 09 14:04:41 2013 +0200
+++ b/src/HOL/Deriv.thy	Tue Apr 09 14:04:47 2013 +0200
@@ -1,6 +1,7 @@
 (*  Title       : Deriv.thy
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
+    Author      : Brian Huffman
     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     GMVT by Benjamin Porter, 2005
 *)
@@ -11,102 +12,703 @@
 imports Limits
 begin
 
-text{*Standard Definitions*}
+definition
+  -- {* Frechet derivative: D is derivative of function f at x within s *}
+  has_derivative :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow>  bool"
+  (infixl "(has'_derivative)" 12)
+where
+  "(f has_derivative f') F \<longleftrightarrow>
+    (bounded_linear f' \<and>
+     ((\<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)"
+
+lemma FDERIV_eq_rhs: "(f has_derivative f') F \<Longrightarrow> f' = g' \<Longrightarrow> (f has_derivative g') F"
+  by simp
+
+ML {*
+
+structure FDERIV_Intros = Named_Thms
+(
+  val name = @{binding FDERIV_intros}
+  val description = "introduction rules for FDERIV"
+)
+
+*}
+
+setup {*
+  FDERIV_Intros.setup #>
+  Global_Theory.add_thms_dynamic (@{binding FDERIV_eq_intros},
+    map_filter (try (fn thm => @{thm FDERIV_eq_rhs} OF [thm])) o FDERIV_Intros.get o Context.proof_of);
+*}
+
+lemma FDERIV_bounded_linear: "(f has_derivative f') F \<Longrightarrow> bounded_linear f'"
+  by (simp add: has_derivative_def)
+
+lemma FDERIV_ident[FDERIV_intros, simp]: "((\<lambda>x. x) has_derivative (\<lambda>x. x)) F"
+  by (simp add: has_derivative_def tendsto_const)
+
+lemma FDERIV_const[FDERIV_intros, simp]: "((\<lambda>x. c) has_derivative (\<lambda>x. 0)) F"
+  by (simp add: has_derivative_def tendsto_const)
+
+lemma (in bounded_linear) bounded_linear: "bounded_linear f" ..
+
+lemma (in bounded_linear) FDERIV:
+  "(g has_derivative g') F \<Longrightarrow> ((\<lambda>x. f (g x)) has_derivative (\<lambda>x. f (g' x))) F"
+  using assms unfolding has_derivative_def
+  apply safe
+  apply (erule bounded_linear_compose [OF local.bounded_linear])
+  apply (drule local.tendsto)
+  apply (simp add: local.scaleR local.diff local.add local.zero)
+  done
+
+lemmas FDERIV_scaleR_right [FDERIV_intros] =
+  bounded_linear.FDERIV [OF bounded_linear_scaleR_right]
+
+lemmas FDERIV_scaleR_left [FDERIV_intros] =
+  bounded_linear.FDERIV [OF bounded_linear_scaleR_left]
+
+lemmas FDERIV_mult_right [FDERIV_intros] =
+  bounded_linear.FDERIV [OF bounded_linear_mult_right]
+
+lemmas FDERIV_mult_left [FDERIV_intros] =
+  bounded_linear.FDERIV [OF bounded_linear_mult_left]
+
+lemma FDERIV_add[simp, FDERIV_intros]:
+  assumes f: "(f has_derivative f') F" and g: "(g has_derivative g') F"
+  shows "((\<lambda>x. f x + g x) has_derivative (\<lambda>x. f' x + g' x)) F"
+  unfolding has_derivative_def
+proof safe
+  let ?x = "Lim F (\<lambda>x. x)"
+  let ?D = "\<lambda>f f' y. ((f y - f ?x) - f' (y - ?x)) /\<^sub>R norm (y - ?x)"
+  have "((\<lambda>x. ?D f f' x + ?D g g' x) ---> (0 + 0)) F"
+    using f g by (intro tendsto_add) (auto simp: has_derivative_def)
+  then show "(?D (\<lambda>x. f x + g x) (\<lambda>x. f' x + g' x) ---> 0) F"
+    by (simp add: field_simps scaleR_add_right scaleR_diff_right)
+qed (blast intro: bounded_linear_add f g FDERIV_bounded_linear)
+
+lemma FDERIV_setsum[simp, FDERIV_intros]:
+  assumes f: "\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) F"
+  shows "((\<lambda>x. \<Sum>i\<in>I. f i x) has_derivative (\<lambda>x. \<Sum>i\<in>I. f' i x)) F"
+proof cases
+  assume "finite I" from this f show ?thesis
+    by induct (simp_all add: f)
+qed simp
+
+lemma FDERIV_minus[simp, FDERIV_intros]: "(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. - f x) has_derivative (\<lambda>x. - f' x)) F"
+  using FDERIV_scaleR_right[of f f' F "-1"] by simp
+
+lemma FDERIV_diff[simp, FDERIV_intros]:
+  "(f has_derivative f') F \<Longrightarrow> (g has_derivative g') F \<Longrightarrow> ((\<lambda>x. f x - g x) has_derivative (\<lambda>x. f' x - g' x)) F"
+  by (simp only: diff_minus FDERIV_add FDERIV_minus)
+
+abbreviation
+  -- {* Frechet derivative: D is derivative of function f at x within s *}
+  FDERIV :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow>  ('a \<Rightarrow> 'b) \<Rightarrow> bool"
+  ("(FDERIV (_)/ (_)/ : (_)/ :> (_))" [1000, 1000, 1000, 60] 60)
+where
+  "FDERIV f x : s :> f' \<equiv> (f has_derivative f') (at x within s)"
+
+abbreviation
+  fderiv_at ::
+    "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
+    ("(FDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
+where
+  "FDERIV f x :> D \<equiv> FDERIV f x : UNIV :> D"
+
+lemma FDERIV_def:
+  "FDERIV f x : s :> f' \<longleftrightarrow>
+    (bounded_linear f' \<and> ((\<lambda>y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) ---> 0) (at x within s))"
+  by (cases "at x within s = bot") (simp_all add: has_derivative_def Lim_ident_at)
+
+lemma FDERIV_iff_norm:
+  "FDERIV f x : s :> f' \<longleftrightarrow>
+    (bounded_linear f' \<and> ((\<lambda>y. norm ((f y - f x) - f' (y - x)) / norm (y - x)) ---> 0) (at x within s))"
+  using tendsto_norm_zero_iff[of _ "at x within s", where 'b="'b", symmetric]
+  by (simp add: FDERIV_def divide_inverse ac_simps)
+
+lemma fderiv_def:
+  "FDERIV f x :> D = (bounded_linear D \<and> (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0)"
+  unfolding FDERIV_iff_norm LIM_offset_zero_iff[of _ _ x] by simp
+
+lemma field_fderiv_def:
+  fixes x :: "'a::real_normed_field"
+  shows "FDERIV f x :> (\<lambda>h. h * D) = (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
+  apply (unfold fderiv_def)
+  apply (simp add: bounded_linear_mult_left)
+  apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
+  apply (subst diff_divide_distrib)
+  apply (subst times_divide_eq_left [symmetric])
+  apply (simp cong: LIM_cong)
+  apply (simp add: tendsto_norm_zero_iff LIM_zero_iff)
+  done
+
+lemma FDERIV_I:
+  "bounded_linear f' \<Longrightarrow> ((\<lambda>y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) ---> 0) (at x within s) \<Longrightarrow>
+  FDERIV f x : s :> f'"
+  by (simp add: FDERIV_def)
+
+lemma FDERIV_I_sandwich:
+  assumes e: "0 < e" and bounded: "bounded_linear f'"
+    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)"
+    and "(H ---> 0) (at x within s)"
+  shows "FDERIV f x : s :> f'"
+  unfolding FDERIV_iff_norm
+proof safe
+  show "((\<lambda>y. norm (f y - f x - f' (y - x)) / norm (y - x)) ---> 0) (at x within s)"
+  proof (rule tendsto_sandwich[where f="\<lambda>x. 0"])
+    show "(H ---> 0) (at x within s)" by fact
+    show "eventually (\<lambda>n. norm (f n - f x - f' (n - x)) / norm (n - x) \<le> H n) (at x within s)"
+      unfolding eventually_at using e sandwich by auto
+  qed (auto simp: le_divide_eq tendsto_const)
+qed fact
+
+lemma FDERIV_subset: "FDERIV f x : s :> f' \<Longrightarrow> t \<subseteq> s \<Longrightarrow> FDERIV f x : t :> f'"
+  by (auto simp add: FDERIV_iff_norm intro: tendsto_within_subset)
+
+subsection {* Continuity *}
+
+lemma FDERIV_continuous:
+  assumes f: "FDERIV f x : s :> f'"
+  shows "continuous (at x within s) f"
+proof -
+  from f interpret F: bounded_linear f' by (rule FDERIV_bounded_linear)
+  note F.tendsto[tendsto_intros]
+  let ?L = "\<lambda>f. (f ---> 0) (at x within s)"
+  have "?L (\<lambda>y. norm ((f y - f x) - f' (y - x)) / norm (y - x))"
+    using f unfolding FDERIV_iff_norm by blast
+  then have "?L (\<lambda>y. norm ((f y - f x) - f' (y - x)) / norm (y - x) * norm (y - x))" (is ?m)
+    by (rule tendsto_mult_zero) (auto intro!: tendsto_eq_intros)
+  also have "?m \<longleftrightarrow> ?L (\<lambda>y. norm ((f y - f x) - f' (y - x)))"
+    by (intro filterlim_cong) (simp_all add: eventually_at_filter)
+  finally have "?L (\<lambda>y. (f y - f x) - f' (y - x))"
+    by (rule tendsto_norm_zero_cancel)
+  then have "?L (\<lambda>y. ((f y - f x) - f' (y - x)) + f' (y - x))"
+    by (rule tendsto_eq_intros) (auto intro!: tendsto_eq_intros simp: F.zero)
+  then have "?L (\<lambda>y. f y - f x)"
+    by simp
+  from tendsto_add[OF this tendsto_const, of "f x"] show ?thesis
+    by (simp add: continuous_within)
+qed
+
+subsection {* Composition *}
+
+lemma tendsto_at_iff_tendsto_nhds_within: "f x = y \<Longrightarrow> (f ---> y) (at x within s) \<longleftrightarrow> (f ---> y) (inf (nhds x) (principal s))"
+  unfolding tendsto_def eventually_inf_principal eventually_at_filter
+  by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1)
+
+lemma FDERIV_in_compose:
+  assumes f: "FDERIV f x : s :> f'"
+  assumes g: "FDERIV g (f x) : (f`s) :> g'"
+  shows "FDERIV (\<lambda>x. g (f x)) x : s :> (\<lambda>x. g' (f' x))"
+proof -
+  from f interpret F: bounded_linear f' by (rule FDERIV_bounded_linear)
+  from g interpret G: bounded_linear g' by (rule FDERIV_bounded_linear)
+  from F.bounded obtain kF where kF: "\<And>x. norm (f' x) \<le> norm x * kF" by fast
+  from G.bounded obtain kG where kG: "\<And>x. norm (g' x) \<le> norm x * kG" by fast
+  note G.tendsto[tendsto_intros]
+
+  let ?L = "\<lambda>f. (f ---> 0) (at x within s)"
+  let ?D = "\<lambda>f f' x y. (f y - f x) - f' (y - x)"
+  let ?N = "\<lambda>f f' x y. norm (?D f f' x y) / norm (y - x)"
+  let ?gf = "\<lambda>x. g (f x)" and ?gf' = "\<lambda>x. g' (f' x)"
+  def Nf \<equiv> "?N f f' x"
+  def Ng \<equiv> "\<lambda>y. ?N g g' (f x) (f y)"
+
+  show ?thesis
+  proof (rule FDERIV_I_sandwich[of 1])
+    show "bounded_linear (\<lambda>x. g' (f' x))"
+      using f g by (blast intro: bounded_linear_compose FDERIV_bounded_linear)
+  next
+    fix y::'a assume neq: "y \<noteq> x"
+    have "?N ?gf ?gf' x y = norm (g' (?D f f' x y) + ?D g g' (f x) (f y)) / norm (y - x)"
+      by (simp add: G.diff G.add field_simps)
+    also have "\<dots> \<le> norm (g' (?D f f' x y)) / norm (y - x) + Ng y * (norm (f y - f x) / norm (y - x))"
+      by (simp add: add_divide_distrib[symmetric] divide_right_mono norm_triangle_ineq G.zero Ng_def)
+    also have "\<dots> \<le> Nf y * kG + Ng y * (Nf y + kF)"
+    proof (intro add_mono mult_left_mono)
+      have "norm (f y - f x) = norm (?D f f' x y + f' (y - x))"
+        by simp
+      also have "\<dots> \<le> norm (?D f f' x y) + norm (f' (y - x))"
+        by (rule norm_triangle_ineq)
+      also have "\<dots> \<le> norm (?D f f' x y) + norm (y - x) * kF"
+        using kF by (intro add_mono) simp
+      finally show "norm (f y - f x) / norm (y - x) \<le> Nf y + kF"
+        by (simp add: neq Nf_def field_simps)
+    qed (insert kG, simp_all add: Ng_def Nf_def neq zero_le_divide_iff field_simps)
+    finally show "?N ?gf ?gf' x y \<le> Nf y * kG + Ng y * (Nf y + kF)" .
+  next
+    have [tendsto_intros]: "?L Nf"
+      using f unfolding FDERIV_iff_norm Nf_def ..
+    from f have "(f ---> f x) (at x within s)"
+      by (blast intro: FDERIV_continuous continuous_within[THEN iffD1])
+    then have f': "LIM x at x within s. f x :> inf (nhds (f x)) (principal (f`s))"
+      unfolding filterlim_def
+      by (simp add: eventually_filtermap eventually_at_filter le_principal)
+
+    have "((?N g  g' (f x)) ---> 0) (at (f x) within f`s)"
+      using g unfolding FDERIV_iff_norm ..
+    then have g': "((?N g  g' (f x)) ---> 0) (inf (nhds (f x)) (principal (f`s)))"
+      by (rule tendsto_at_iff_tendsto_nhds_within[THEN iffD1, rotated]) simp
+
+    have [tendsto_intros]: "?L Ng"
+      unfolding Ng_def by (rule filterlim_compose[OF g' f'])
+    show "((\<lambda>y. Nf y * kG + Ng y * (Nf y + kF)) ---> 0) (at x within s)"
+      by (intro tendsto_eq_intros) auto
+  qed simp
+qed
+
+lemma FDERIV_compose:
+  "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))"
+  by (blast intro: FDERIV_in_compose FDERIV_subset)
+
+lemma (in bounded_bilinear) FDERIV:
+  assumes f: "FDERIV f x : s :> f'" and g: "FDERIV g x : s :> g'"
+  shows "FDERIV (\<lambda>x. f x ** g x) x : s :> (\<lambda>h. f x ** g' h + f' h ** g x)"
+proof -
+  from bounded_linear.bounded [OF FDERIV_bounded_linear [OF f]]
+  obtain KF where norm_F: "\<And>x. norm (f' x) \<le> norm x * KF" by fast
+
+  from pos_bounded obtain K where K: "0 < K" and norm_prod:
+    "\<And>a b. norm (a ** b) \<le> norm a * norm b * K" by fast
+  let ?D = "\<lambda>f f' y. f y - f x - f' (y - x)"
+  let ?N = "\<lambda>f f' y. norm (?D f f' y) / norm (y - x)"
+  def Ng =="?N g g'" and Nf =="?N f f'"
+
+  let ?fun1 = "\<lambda>y. norm (f y ** g y - f x ** g x - (f x ** g' (y - x) + f' (y - x) ** g x)) / norm (y - x)"
+  let ?fun2 = "\<lambda>y. norm (f x) * Ng y * K + Nf y * norm (g y) * K + KF * norm (g y - g x) * K"
+  let ?F = "at x within s"
 
-definition
-  deriv :: "['a::real_normed_field \<Rightarrow> 'a, 'a, 'a] \<Rightarrow> bool"
-    --{*Differentiation: D is derivative of function f at x*}
-          ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where
-  "DERIV f x :> D = ((%h. (f(x + h) - f x) / h) -- 0 --> D)"
+  show ?thesis
+  proof (rule FDERIV_I_sandwich[of 1])
+    show "bounded_linear (\<lambda>h. f x ** g' h + f' h ** g x)"
+      by (intro bounded_linear_add
+        bounded_linear_compose [OF bounded_linear_right] bounded_linear_compose [OF bounded_linear_left]
+        FDERIV_bounded_linear [OF g] FDERIV_bounded_linear [OF f])
+  next
+    from g have "(g ---> g x) ?F"
+      by (intro continuous_within[THEN iffD1] FDERIV_continuous)
+    moreover from f g have "(Nf ---> 0) ?F" "(Ng ---> 0) ?F"
+      by (simp_all add: FDERIV_iff_norm Ng_def Nf_def)
+    ultimately have "(?fun2 ---> norm (f x) * 0 * K + 0 * norm (g x) * K + KF * norm (0::'b) * K) ?F"
+      by (intro tendsto_intros) (simp_all add: LIM_zero_iff)
+    then show "(?fun2 ---> 0) ?F"
+      by simp
+  next
+    fix y::'d assume "y \<noteq> x"
+    have "?fun1 y = norm (f x ** ?D g g' y + ?D f f' y ** g y + f' (y - x) ** (g y - g x)) / norm (y - x)"
+      by (simp add: diff_left diff_right add_left add_right field_simps)
+    also have "\<dots> \<le> (norm (f x) * norm (?D g g' y) * K + norm (?D f f' y) * norm (g y) * K +
+        norm (y - x) * KF * norm (g y - g x) * K) / norm (y - x)"
+      by (intro divide_right_mono mult_mono'
+                order_trans [OF norm_triangle_ineq add_mono]
+                order_trans [OF norm_prod mult_right_mono]
+                mult_nonneg_nonneg order_refl norm_ge_zero norm_F
+                K [THEN order_less_imp_le])
+    also have "\<dots> = ?fun2 y"
+      by (simp add: add_divide_distrib Ng_def Nf_def)
+    finally show "?fun1 y \<le> ?fun2 y" .
+  qed simp
+qed
+
+lemmas FDERIV_mult[simp, FDERIV_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_mult]
+lemmas FDERIV_scaleR[simp, FDERIV_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_scaleR]
+
+lemma FDERIV_setprod[simp, FDERIV_intros]:
+  fixes f :: "'i \<Rightarrow> 'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
+  assumes f: "\<And>i. i \<in> I \<Longrightarrow> FDERIV (f i) x : s :> f' i"
+  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))"
+proof cases
+  assume "finite I" from this f show ?thesis
+  proof induct
+    case (insert i I)
+    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)"
+    have "FDERIV (\<lambda>x. f i x * (\<Prod>i\<in>I. f i x)) x : s :> ?P"
+      using insert by (intro FDERIV_mult) auto
+    also have "?P = (\<lambda>y. \<Sum>i'\<in>insert i I. f' i' y * (\<Prod>j\<in>insert i I - {i'}. f j x))"
+      using insert(1,2) by (auto simp add: setsum_right_distrib insert_Diff_if intro!: ext setsum_cong)
+    finally show ?case
+      using insert by simp
+  qed simp  
+qed simp
+
+lemma FDERIV_power[simp, FDERIV_intros]:
+  fixes f :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
+  assumes f: "FDERIV f x : s :> f'"
+  shows "FDERIV  (\<lambda>x. f x^n) x : s :> (\<lambda>y. of_nat n * f' y * f x^(n - 1))"
+  using FDERIV_setprod[OF f, of "{..< n}"] by (simp add: setprod_constant ac_simps)
+
+lemma FDERIV_inverse':
+  fixes x :: "'a::real_normed_div_algebra"
+  assumes x: "x \<noteq> 0"
+  shows "FDERIV inverse x : s :> (\<lambda>h. - (inverse x * h * inverse x))"
+        (is "FDERIV ?inv x : s :> ?f")
+proof (rule FDERIV_I_sandwich)
+  show "bounded_linear (\<lambda>h. - (?inv x * h * ?inv x))"
+    apply (rule bounded_linear_minus)
+    apply (rule bounded_linear_mult_const)
+    apply (rule bounded_linear_const_mult)
+    apply (rule bounded_linear_ident)
+    done
+next
+  show "0 < norm x" using x by simp
+next
+  show "((\<lambda>y. norm (?inv y - ?inv x) * norm (?inv x)) ---> 0) (at x within s)"
+    apply (rule tendsto_mult_left_zero)
+    apply (rule tendsto_norm_zero)
+    apply (rule LIM_zero)
+    apply (rule tendsto_inverse)
+    apply (rule tendsto_ident_at)
+    apply (rule x)
+    done
+next
+  fix y::'a assume h: "y \<noteq> x" "dist y x < norm x"
+  then have "y \<noteq> 0"
+    by (auto simp: norm_conv_dist dist_commute)
+  have "norm (?inv y - ?inv x - ?f (y -x)) / norm (y - x) = norm ((?inv y - ?inv x) * (y - x) * ?inv x) / norm (y - x)"
+    apply (subst inverse_diff_inverse [OF `y \<noteq> 0` x])
+    apply (subst minus_diff_minus)
+    apply (subst norm_minus_cancel)
+    apply (simp add: left_diff_distrib)
+    done
+  also have "\<dots> \<le> norm (?inv y - ?inv x) * norm (y - x) * norm (?inv x) / norm (y - x)"
+    apply (rule divide_right_mono [OF _ norm_ge_zero])
+    apply (rule order_trans [OF norm_mult_ineq])
+    apply (rule mult_right_mono [OF _ norm_ge_zero])
+    apply (rule norm_mult_ineq)
+    done
+  also have "\<dots> = norm (?inv y - ?inv x) * norm (?inv x)"
+    by simp
+  finally show "norm (?inv y - ?inv x - ?f (y -x)) / norm (y - x) \<le>
+      norm (?inv y - ?inv x) * norm (?inv x)" .
+qed
+
+lemma FDERIV_inverse[simp, FDERIV_intros]:
+  fixes f :: "_ \<Rightarrow> 'a::real_normed_div_algebra"
+  assumes x:  "f x \<noteq> 0" and f: "FDERIV f x : s :> f'"
+  shows "FDERIV (\<lambda>x. inverse (f x)) x : s :> (\<lambda>h. - (inverse (f x) * f' h * inverse (f x)))"
+  using FDERIV_compose[OF f FDERIV_inverse', OF x] .
+
+lemma FDERIV_divide[simp, FDERIV_intros]:
+  fixes f :: "_ \<Rightarrow> 'a::real_normed_div_algebra"
+  assumes g: "FDERIV g x : s :> g'"
+  assumes x:  "f x \<noteq> 0" and f: "FDERIV f x : s :> f'"
+  shows "FDERIV (\<lambda>x. g x / f x) x : s :> (\<lambda>h. - g x * (inverse (f x) * f' h * inverse (f x)) + g' h / f x)"
+  using FDERIV_mult[OF g FDERIV_inverse[OF x f]]
+  by (simp add: divide_inverse)
+
+subsection {* Uniqueness *}
+
+text {*
+
+This can not generally shown for @{const FDERIV}, as we need to approach the point from
+all directions. There is a proof in @{text Multivariate_Analysis} for @{text euclidean_space}.
+
+*}
+
+lemma FDERIV_zero_unique:
+  assumes "FDERIV (\<lambda>x. 0) x :> F" shows "F = (\<lambda>h. 0)"
+proof -
+  interpret F: bounded_linear F
+    using assms by (rule FDERIV_bounded_linear)
+  let ?r = "\<lambda>h. norm (F h) / norm h"
+  have *: "?r -- 0 --> 0"
+    using assms unfolding fderiv_def by simp
+  show "F = (\<lambda>h. 0)"
+  proof
+    fix h show "F h = 0"
+    proof (rule ccontr)
+      assume "F h \<noteq> 0"
+      moreover from this have h: "h \<noteq> 0"
+        by (clarsimp simp add: F.zero)
+      ultimately have "0 < ?r h"
+        by (simp add: divide_pos_pos)
+      from LIM_D [OF * this] obtain s where s: "0 < s"
+        and r: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> ?r x < ?r h" by auto
+      from dense [OF s] obtain t where t: "0 < t \<and> t < s" ..
+      let ?x = "scaleR (t / norm h) h"
+      have "?x \<noteq> 0" and "norm ?x < s" using t h by simp_all
+      hence "?r ?x < ?r h" by (rule r)
+      thus "False" using t h by (simp add: F.scaleR)
+    qed
+  qed
+qed
+
+lemma FDERIV_unique:
+  assumes "FDERIV f x :> F" and "FDERIV f x :> F'" shows "F = F'"
+proof -
+  have "FDERIV (\<lambda>x. 0) x :> (\<lambda>h. F h - F' h)"
+    using FDERIV_diff [OF assms] by simp
+  hence "(\<lambda>h. F h - F' h) = (\<lambda>h. 0)"
+    by (rule FDERIV_zero_unique)
+  thus "F = F'"
+    unfolding fun_eq_iff right_minus_eq .
+qed
+
+subsection {* Differentiability predicate *}
+
+definition isDiff :: "'a filter \<Rightarrow> ('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> bool" where
+  isDiff_def: "isDiff F f \<longleftrightarrow> (\<exists>D. (f has_derivative D) F)"
+
+abbreviation differentiable_in :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool"
+    ("(_) differentiable (_) in (_)"  [1000, 1000, 60] 60) where
+  "f differentiable x in s \<equiv> isDiff (at x within s) f"
+
+abbreviation differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool"
+    (infixl "differentiable" 60) where
+  "f differentiable x \<equiv> f differentiable x in UNIV"
+
+lemma differentiable_subset: "f differentiable x in s \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f differentiable x in t"
+  unfolding isDiff_def by (blast intro: FDERIV_subset)
+
+lemma differentiable_ident [simp]: "isDiff F (\<lambda>x. x)"
+  unfolding isDiff_def by (blast intro: FDERIV_ident)
+
+lemma differentiable_const [simp]: "isDiff F (\<lambda>z. a)"
+  unfolding isDiff_def by (blast intro: FDERIV_const)
+
+lemma differentiable_in_compose:
+  "f differentiable (g x) in (g`s) \<Longrightarrow> g differentiable x in s \<Longrightarrow> (\<lambda>x. f (g x)) differentiable x in s"
+  unfolding isDiff_def by (blast intro: FDERIV_in_compose)
+
+lemma differentiable_compose:
+  "f differentiable (g x) \<Longrightarrow> g differentiable x in s \<Longrightarrow> (\<lambda>x. f (g x)) differentiable x in s"
+  by (blast intro: differentiable_in_compose differentiable_subset)
+
+lemma differentiable_sum [simp]:
+  "isDiff F f \<Longrightarrow> isDiff F g \<Longrightarrow> isDiff F (\<lambda>x. f x + g x)"
+  unfolding isDiff_def by (blast intro: FDERIV_add)
+
+lemma differentiable_minus [simp]:
+  "isDiff F f \<Longrightarrow> isDiff F (\<lambda>x. - f x)"
+  unfolding isDiff_def by (blast intro: FDERIV_minus)
+
+lemma differentiable_diff [simp]:
+  "isDiff F f \<Longrightarrow> isDiff F g \<Longrightarrow> isDiff F (\<lambda>x. f x - g x)"
+  unfolding isDiff_def by (blast intro: FDERIV_diff)
+
+lemma differentiable_mult [simp]:
+  fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_algebra"
+  shows "f differentiable x in s \<Longrightarrow> g differentiable x in s \<Longrightarrow> (\<lambda>x. f x * g x) differentiable x in s"
+  unfolding isDiff_def by (blast intro: FDERIV_mult)
+
+lemma differentiable_inverse [simp]:
+  fixes f :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
+  shows "f differentiable x in s \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> (\<lambda>x. inverse (f x)) differentiable x in s"
+  unfolding isDiff_def by (blast intro: FDERIV_inverse)
+
+lemma differentiable_divide [simp]:
+  fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
+  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"
+  unfolding divide_inverse using assms by simp
+
+lemma differentiable_power [simp]:
+  fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
+  shows "f differentiable x in s \<Longrightarrow> (\<lambda>x. f x ^ n) differentiable x in s"
+  unfolding isDiff_def by (blast intro: FDERIV_power)
+
+lemma differentiable_scaleR [simp]:
+  "f differentiable x in s \<Longrightarrow> g differentiable x in s \<Longrightarrow> (\<lambda>x. f x *\<^sub>R g x) differentiable x in s"
+  unfolding isDiff_def by (blast intro: FDERIV_scaleR)
+
+definition 
+  -- {*Differentiation: D is derivative of function f at x*}
+  deriv ::
+    "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool"
+    ("(DERIV (_)/ (_)/ : (_)/ :> (_))" [1000, 1000, 1000, 60] 60)
+where
+  deriv_fderiv: "DERIV f x : s :> D = FDERIV f x : s :> (\<lambda>x. x * D)"
+
+abbreviation
+  -- {*Differentiation: D is derivative of function f at x*}
+  deriv_at ::
+    "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+    ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
+where
+  "DERIV f x :> D \<equiv> DERIV f x : UNIV :> D"
+
+lemma differentiable_def: "(f::real \<Rightarrow> real) differentiable x in s \<longleftrightarrow> (\<exists>D. DERIV f x : s :> D)"
+proof safe
+  assume "f differentiable x in s"
+  then obtain f' where "FDERIV f x : s :> f'"
+    unfolding isDiff_def by auto
+  moreover then obtain c where "f' = (\<lambda>x. x * c)"
+    by (metis real_bounded_linear FDERIV_bounded_linear)
+  ultimately show "\<exists>D. DERIV f x : s :> D"
+    unfolding deriv_fderiv by auto
+qed (auto simp: isDiff_def deriv_fderiv)
+
+lemma differentiableE [elim?]:
+  fixes f :: "real \<Rightarrow> real"
+  assumes f: "f differentiable x in s" obtains df where "DERIV f x : s :> df"
+  using assms by (auto simp: differentiable_def)
+
+lemma differentiableD: "(f::real \<Rightarrow> real) differentiable x in s \<Longrightarrow> \<exists>D. DERIV f x : s :> D"
+  by (auto elim: differentiableE)
+
+lemma differentiableI: "DERIV f x : s :> D \<Longrightarrow> (f::real \<Rightarrow> real) differentiable x in s"
+  by (force simp add: differentiable_def)
+
+lemma DERIV_I_FDERIV: "FDERIV f x : s :> F \<Longrightarrow> (\<And>x. x * F' = F x) \<Longrightarrow> DERIV f x : s :> F'"
+  by (simp add: deriv_fderiv)
+
+lemma DERIV_D_FDERIV: "DERIV f x : s :> F \<Longrightarrow> FDERIV f x : s :> (\<lambda>x. x * F)"
+  by (simp add: deriv_fderiv)
+
+lemma deriv_def:
+  "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
+  apply (simp add: deriv_fderiv fderiv_def bounded_linear_mult_left LIM_zero_iff[symmetric, of _ D])
+  apply (subst (2) tendsto_norm_zero_iff[symmetric])
+  apply (rule filterlim_cong)
+  apply (simp_all add: eventually_at_filter field_simps nonzero_norm_divide)
+  done
 
 subsection {* Derivatives *}
 
-lemma DERIV_iff: "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --> D)"
-by (simp add: deriv_def)
+lemma DERIV_iff: "(DERIV f x :> D) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
+  by (simp add: deriv_def)
 
-lemma DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --> D"
-by (simp add: deriv_def)
+lemma DERIV_D: "DERIV f x :> D \<Longrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
+  by (simp add: deriv_def)
 
-lemma DERIV_const [simp]: "DERIV (\<lambda>x. k) x :> 0"
-  by (simp add: deriv_def tendsto_const)
+lemma DERIV_const [simp]: "DERIV (\<lambda>x. k) x : s :> 0"
+  by (rule DERIV_I_FDERIV[OF FDERIV_const]) auto
 
-lemma DERIV_ident [simp]: "DERIV (\<lambda>x. x) x :> 1"
-  by (simp add: deriv_def tendsto_const cong: LIM_cong)
+lemma DERIV_ident [simp]: "DERIV (\<lambda>x. x) x : s :> 1"
+  by (rule DERIV_I_FDERIV[OF FDERIV_ident]) auto
 
-lemma DERIV_add:
-  "\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x + g x) x :> D + E"
-  by (simp only: deriv_def add_diff_add add_divide_distrib tendsto_add)
+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"
+  by (rule DERIV_I_FDERIV[OF FDERIV_add]) (auto simp: field_simps dest: DERIV_D_FDERIV)
 
-lemma DERIV_minus:
-  "DERIV f x :> D \<Longrightarrow> DERIV (\<lambda>x. - f x) x :> - D"
-  by (simp only: deriv_def minus_diff_minus divide_minus_left tendsto_minus)
+lemma DERIV_minus: "DERIV f x : s :> D \<Longrightarrow> DERIV (\<lambda>x. - f x) x : s :> - D"
+  by (rule DERIV_I_FDERIV[OF FDERIV_minus]) (auto simp: field_simps dest: DERIV_D_FDERIV)
 
-lemma DERIV_diff:
-  "\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x - g x) x :> D - E"
-by (simp only: diff_minus DERIV_add DERIV_minus)
+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"
+  by (rule DERIV_I_FDERIV[OF FDERIV_diff]) (auto simp: field_simps dest: DERIV_D_FDERIV)
 
-lemma DERIV_add_minus:
-  "\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x + - g x) x :> D + - E"
-by (simp only: DERIV_add DERIV_minus)
+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"
+  by (simp only: DERIV_add DERIV_minus)
+
+lemma DERIV_continuous: "DERIV f x : s :> D \<Longrightarrow> continuous (at x within s) f"
+  by (drule FDERIV_continuous[OF DERIV_D_FDERIV]) simp
 
 lemma DERIV_isCont: "DERIV f x :> D \<Longrightarrow> isCont f x"
-proof (unfold isCont_iff)
-  assume "DERIV f x :> D"
-  hence "(\<lambda>h. (f(x+h) - f(x)) / h) -- 0 --> D"
-    by (rule DERIV_D)
-  hence "(\<lambda>h. (f(x+h) - f(x)) / h * h) -- 0 --> D * 0"
-    by (intro tendsto_mult tendsto_ident_at)
-  hence "(\<lambda>h. (f(x+h) - f(x)) * (h / h)) -- 0 --> 0"
-    by simp
-  hence "(\<lambda>h. f(x+h) - f(x)) -- 0 --> 0"
-    by (simp cong: LIM_cong)
-  thus "(\<lambda>h. f(x+h)) -- 0 --> f(x)"
-    by (simp add: LIM_def dist_norm)
-qed
+  by (auto dest!: DERIV_continuous)
+
+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"
+  by (rule DERIV_I_FDERIV[OF FDERIV_mult]) (auto simp: field_simps dest: DERIV_D_FDERIV)
 
-lemma DERIV_mult_lemma:
-  fixes a b c d :: "'a::real_field"
-  shows "(a * b - c * d) / h = a * ((b - d) / h) + ((a - c) / h) * d"
-  by (simp add: field_simps diff_divide_distrib)
+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"
+  by (rule DERIV_I_FDERIV[OF FDERIV_mult]) (auto simp: field_simps dest: DERIV_D_FDERIV)
+
+text {* Derivative of linear multiplication *}
 
-lemma DERIV_mult':
-  assumes f: "DERIV f x :> D"
-  assumes g: "DERIV g x :> E"
-  shows "DERIV (\<lambda>x. f x * g x) x :> f x * E + D * g x"
-proof (unfold deriv_def)
-  from f have "isCont f x"
-    by (rule DERIV_isCont)
-  hence "(\<lambda>h. f(x+h)) -- 0 --> f x"
-    by (simp only: isCont_iff)
-  hence "(\<lambda>h. f(x+h) * ((g(x+h) - g x) / h) +
-              ((f(x+h) - f x) / h) * g x)
-          -- 0 --> f x * E + D * g x"
-    by (intro tendsto_intros DERIV_D f g)
-  thus "(\<lambda>h. (f(x+h) * g(x+h) - f x * g x) / h)
-         -- 0 --> f x * E + D * g x"
-    by (simp only: DERIV_mult_lemma)
-qed
+lemma DERIV_cmult:
+  "DERIV f x : s :> D ==> DERIV (%x. c * f x) x : s :> c*D"
+  by (drule DERIV_mult' [OF DERIV_const], simp)
 
-lemma DERIV_mult:
-    "DERIV f x :> Da \<Longrightarrow> DERIV g x :> Db \<Longrightarrow> DERIV (\<lambda>x. f x * g x) x :> Da * g x + Db * f x"
-  by (drule (1) DERIV_mult', simp only: mult_commute add_commute)
+lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x : s :> c"
+  by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp)
+
+lemma DERIV_cdivide: "DERIV f x : s :> D ==> DERIV (%x. f x / c) x : s :> D / c"
+  apply (subgoal_tac "DERIV (%x. (1 / c) * f x) x : s :> (1 / c) * D", force)
+  apply (erule DERIV_cmult)
+  done
 
 lemma DERIV_unique:
-    "DERIV f x :> D \<Longrightarrow> DERIV f x :> E \<Longrightarrow> D = E"
+  "DERIV f x :> D \<Longrightarrow> DERIV f x :> E \<Longrightarrow> D = E"
   unfolding deriv_def by (rule LIM_unique) 
 
-text{*Differentiation of finite sum*}
+lemma DERIV_setsum':
+  "(\<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"
+  by (rule DERIV_I_FDERIV[OF FDERIV_setsum]) (auto simp: setsum_right_distrib dest: DERIV_D_FDERIV)
 
 lemma DERIV_setsum:
-  assumes "finite S"
-  and "\<And> n. n \<in> S \<Longrightarrow> DERIV (%x. f x n) x :> (f' x n)"
-  shows "DERIV (%x. setsum (f x) S) x :> setsum (f' x) S"
-  using assms by induct (auto intro!: DERIV_add)
+  "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"
+  by (rule DERIV_setsum')
+
+lemma DERIV_sumr [rule_format (no_asm)]: (* REMOVE *)
+     "(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x : s :> (f' r x))
+      --> DERIV (%x. \<Sum>n=m..<n::nat. f n x :: real) x : s :> (\<Sum>r=m..<n. f' r x)"
+  by (auto intro: DERIV_setsum)
+
+lemma DERIV_inverse':
+  "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))"
+  by (rule DERIV_I_FDERIV[OF FDERIV_inverse]) (auto dest: DERIV_D_FDERIV)
+
+text {* Power of @{text "-1"} *}
+
+lemma DERIV_inverse:
+  "x \<noteq> 0 \<Longrightarrow> DERIV (\<lambda>x. inverse(x)) x : s :> - (inverse x ^ Suc (Suc 0))"
+  by (drule DERIV_inverse' [OF DERIV_ident]) simp
+
+text {* Derivative of inverse *}
+
+lemma DERIV_inverse_fun:
+  "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))))"
+  by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib)
+
+text {* Derivative of quotient *}
+
+lemma DERIV_divide:
+  "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)"
+  by (rule DERIV_I_FDERIV[OF FDERIV_divide])
+     (auto dest: DERIV_D_FDERIV simp: field_simps nonzero_inverse_mult_distrib divide_inverse)
+
+lemma DERIV_quotient:
+  "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))"
+  by (drule (2) DERIV_divide) (simp add: mult_commute)
+
+lemma DERIV_power_Suc:
+  "DERIV f x : s :> D \<Longrightarrow> DERIV (\<lambda>x. f x ^ Suc n) x : s :> (1 + of_nat n) * (D * f x ^ n)"
+  by (rule DERIV_I_FDERIV[OF FDERIV_power]) (auto simp: deriv_fderiv)
+
+lemma DERIV_power:
+  "DERIV f x : s :> D \<Longrightarrow> DERIV (\<lambda>x. f x ^ n) x : s :> of_nat n * (D * f x ^ (n - Suc 0))"
+  by (rule DERIV_I_FDERIV[OF FDERIV_power]) (auto simp: deriv_fderiv)
 
-lemma DERIV_sumr [rule_format (no_asm)]:
-     "(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))
-      --> DERIV (%x. \<Sum>n=m..<n::nat. f n x :: real) x :> (\<Sum>r=m..<n. f' r x)"
-  by (auto intro: DERIV_setsum)
+lemma DERIV_pow: "DERIV (%x. x ^ n) x : s :> real n * (x ^ (n - Suc 0))"
+  apply (cut_tac DERIV_power [OF DERIV_ident])
+  apply (simp add: real_of_nat_def)
+  done
+
+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"
+  using FDERIV_compose[of f "\<lambda>x. x * D" x s g "\<lambda>x. x * E"]
+  by (auto simp: deriv_fderiv ac_simps dest: FDERIV_subset)
+
+text {* Standard version *}
+
+lemma DERIV_chain: "DERIV f (g x) :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (f o g) x : s :> Da * Db"
+  by (drule (1) DERIV_chain', simp add: o_def mult_commute)
+
+lemma DERIV_chain2: "DERIV f (g x) :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (%x. f (g x)) x : s :> Da * Db"
+  by (auto dest: DERIV_chain simp add: o_def)
+
+subsubsection {* @{text "DERIV_intros"} *}
+
+ML {*
+structure Deriv_Intros = Named_Thms
+(
+  val name = @{binding DERIV_intros}
+  val description = "DERIV introduction rules"
+)
+*}
+
+setup Deriv_Intros.setup
+
+lemma DERIV_cong: "DERIV f x : s :> X \<Longrightarrow> X = Y \<Longrightarrow> DERIV f x : s :> Y"
+  by simp
+
+declare
+  DERIV_const[THEN DERIV_cong, DERIV_intros]
+  DERIV_ident[THEN DERIV_cong, DERIV_intros]
+  DERIV_add[THEN DERIV_cong, DERIV_intros]
+  DERIV_minus[THEN DERIV_cong, DERIV_intros]
+  DERIV_mult[THEN DERIV_cong, DERIV_intros]
+  DERIV_diff[THEN DERIV_cong, DERIV_intros]
+  DERIV_inverse'[THEN DERIV_cong, DERIV_intros]
+  DERIV_divide[THEN DERIV_cong, DERIV_intros]
+  DERIV_power[where 'a=real, THEN DERIV_cong,
+              unfolded real_of_nat_def[symmetric], DERIV_intros]
+  DERIV_setsum[THEN DERIV_cong, DERIV_intros]
 
 text{*Alternative definition for differentiability*}
 
@@ -121,86 +723,33 @@
 apply (simp add: add_commute)
 done
 
-lemma DERIV_iff2: "(DERIV f x :> D) = ((%z. (f(z) - f(x)) / (z-x)) -- x --> D)"
-by (simp add: deriv_def diff_minus [symmetric] DERIV_LIM_iff)
-
-lemma DERIV_inverse_lemma:
-  "\<lbrakk>a \<noteq> 0; b \<noteq> (0::'a::real_normed_field)\<rbrakk>
-   \<Longrightarrow> (inverse a - inverse b) / h
-     = - (inverse a * ((a - b) / h) * inverse b)"
-by (simp add: inverse_diff_inverse)
-
-lemma DERIV_inverse':
-  assumes der: "DERIV f x :> D"
-  assumes neq: "f x \<noteq> 0"
-  shows "DERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x) * D * inverse (f x))"
-    (is "DERIV _ _ :> ?E")
-proof (unfold DERIV_iff2)
-  from der have lim_f: "f -- x --> f x"
-    by (rule DERIV_isCont [unfolded isCont_def])
-
-  from neq have "0 < norm (f x)" by simp
-  with LIM_D [OF lim_f] obtain s
-    where s: "0 < s"
-    and less_fx: "\<And>z. \<lbrakk>z \<noteq> x; norm (z - x) < s\<rbrakk>
-                  \<Longrightarrow> norm (f z - f x) < norm (f x)"
-    by fast
+lemma DERIV_iff2: "(DERIV f x :> D) \<longleftrightarrow> (\<lambda>z. (f z - f x) / (z - x)) --x --> D"
+  by (simp add: deriv_def diff_minus [symmetric] DERIV_LIM_iff)
 
-  show "(\<lambda>z. (inverse (f z) - inverse (f x)) / (z - x)) -- x --> ?E"
-  proof (rule LIM_equal2 [OF s])
-    fix z
-    assume "z \<noteq> x" "norm (z - x) < s"
-    hence "norm (f z - f x) < norm (f x)" by (rule less_fx)
-    hence "f z \<noteq> 0" by auto
-    thus "(inverse (f z) - inverse (f x)) / (z - x) =
-          - (inverse (f z) * ((f z - f x) / (z - x)) * inverse (f x))"
-      using neq by (rule DERIV_inverse_lemma)
-  next
-    from der have "(\<lambda>z. (f z - f x) / (z - x)) -- x --> D"
-      by (unfold DERIV_iff2)
-    thus "(\<lambda>z. - (inverse (f z) * ((f z - f x) / (z - x)) * inverse (f x)))
-          -- x --> ?E"
-      by (intro tendsto_intros lim_f neq)
-  qed
-qed
+lemma DERIV_cong_ev: "x = y \<Longrightarrow> eventually (\<lambda>x. f x = g x) (nhds x) \<Longrightarrow> u = v \<Longrightarrow>
+    DERIV f x :> u \<longleftrightarrow> DERIV g y :> v"
+  unfolding DERIV_iff2
+proof (rule filterlim_cong)
+  assume "eventually (\<lambda>x. f x = g x) (nhds x)"
+  moreover then have "f x = g x" by (auto simp: eventually_nhds)
+  moreover assume "x = y" "u = v"
+  ultimately show "eventually (\<lambda>xa. (f xa - f x) / (xa - x) = (g xa - g y) / (xa - y)) (at x)"
+    by (auto simp: eventually_at_filter elim: eventually_elim1)
+qed simp_all
 
-lemma DERIV_divide:
-  "\<lbrakk>DERIV f x :> D; DERIV g x :> E; g x \<noteq> 0\<rbrakk>
-   \<Longrightarrow> DERIV (\<lambda>x. f x / g x) x :> (D * g x - f x * E) / (g x * g x)"
-apply (subgoal_tac "f x * - (inverse (g x) * E * inverse (g x)) +
-          D * inverse (g x) = (D * g x - f x * E) / (g x * g x)")
-apply (erule subst)
-apply (unfold divide_inverse)
-apply (erule DERIV_mult')
-apply (erule (1) DERIV_inverse')
-apply (simp add: ring_distribs nonzero_inverse_mult_distrib)
-done
+lemma DERIV_shift:
+  "(DERIV f (x + z) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (x + z)) x :> y)"
+  by (simp add: DERIV_iff field_simps)
 
-lemma DERIV_power_Suc:
-  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field}"
-  assumes f: "DERIV f x :> D"
-  shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (1 + of_nat n) * (D * f x ^ n)"
-proof (induct n)
-case 0
-  show ?case by (simp add: f)
-case (Suc k)
-  from DERIV_mult' [OF f Suc] show ?case
-    apply (simp only: of_nat_Suc ring_distribs mult_1_left)
-    apply (simp only: power_Suc algebra_simps)
-    done
-qed
-
-lemma DERIV_power:
-  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field}"
-  assumes f: "DERIV f x :> D"
-  shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n * (D * f x ^ (n - Suc 0))"
-by (cases "n", simp, simp add: DERIV_power_Suc f del: power_Suc)
+lemma DERIV_mirror:
+  "(DERIV f (- x) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (- x::real) :: real) x :> - y)"
+  by (simp add: deriv_def filterlim_at_split filterlim_at_left_to_right
+                tendsto_minus_cancel_left field_simps conj_commute)
 
 text {* Caratheodory formulation of derivative at a point *}
 
 lemma CARAT_DERIV:
-     "(DERIV f x :> l) =
-      (\<exists>g. (\<forall>z. f z - f x = g z * (z-x)) & isCont g x & g x = l)"
+  "(DERIV f x :> l) \<longleftrightarrow> (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> isCont g x \<and> g x = l)"
       (is "?lhs = ?rhs")
 proof
   assume der: "DERIV f x :> l"
@@ -221,207 +770,11 @@
      by (auto simp add: isCont_iff DERIV_iff cong: LIM_cong)
 qed
 
-lemma DERIV_chain':
-  assumes f: "DERIV f x :> D"
-  assumes g: "DERIV g (f x) :> E"
-  shows "DERIV (\<lambda>x. g (f x)) x :> E * D"
-proof (unfold DERIV_iff2)
-  obtain d where d: "\<forall>y. g y - g (f x) = d y * (y - f x)"
-    and cont_d: "isCont d (f x)" and dfx: "d (f x) = E"
-    using CARAT_DERIV [THEN iffD1, OF g] by fast
-  from f have "f -- x --> f x"
-    by (rule DERIV_isCont [unfolded isCont_def])
-  with cont_d have "(\<lambda>z. d (f z)) -- x --> d (f x)"
-    by (rule isCont_tendsto_compose)
-  hence "(\<lambda>z. d (f z) * ((f z - f x) / (z - x)))
-          -- x --> d (f x) * D"
-    by (rule tendsto_mult [OF _ f [unfolded DERIV_iff2]])
-  thus "(\<lambda>z. (g (f z) - g (f x)) / (z - x)) -- x --> E * D"
-    by (simp add: d dfx)
-qed
-
 text {*
  Let's do the standard proof, though theorem
  @{text "LIM_mult2"} follows from a NS proof
 *}
 
-lemma DERIV_cmult:
-      "DERIV f x :> D ==> DERIV (%x. c * f x) x :> c*D"
-by (drule DERIV_mult' [OF DERIV_const], simp)
-
-lemma DERIV_cdivide: "DERIV f x :> D ==> DERIV (%x. f x / c) x :> D / c"
-  apply (subgoal_tac "DERIV (%x. (1 / c) * f x) x :> (1 / c) * D", force)
-  apply (erule DERIV_cmult)
-  done
-
-text {* Standard version *}
-lemma DERIV_chain: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (f o g) x :> Da * Db"
-by (drule (1) DERIV_chain', simp add: o_def mult_commute)
-
-lemma DERIV_chain2: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (%x. f (g x)) x :> Da * Db"
-by (auto dest: DERIV_chain simp add: o_def)
-
-text {* Derivative of linear multiplication *}
-lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x :> c"
-by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp)
-
-lemma DERIV_pow: "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"
-apply (cut_tac DERIV_power [OF DERIV_ident])
-apply (simp add: real_of_nat_def)
-done
-
-text {* Power of @{text "-1"} *}
-
-lemma DERIV_inverse:
-  fixes x :: "'a::{real_normed_field}"
-  shows "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"
-by (drule DERIV_inverse' [OF DERIV_ident]) simp
-
-text {* Derivative of inverse *}
-lemma DERIV_inverse_fun:
-  fixes x :: "'a::{real_normed_field}"
-  shows "[| DERIV f x :> d; f(x) \<noteq> 0 |]
-      ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
-by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib)
-
-text {* Derivative of quotient *}
-lemma DERIV_quotient:
-  fixes x :: "'a::{real_normed_field}"
-  shows "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]
-       ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
-by (drule (2) DERIV_divide) (simp add: mult_commute)
-
-text {* @{text "DERIV_intros"} *}
-ML {*
-structure Deriv_Intros = Named_Thms
-(
-  val name = @{binding DERIV_intros}
-  val description = "DERIV introduction rules"
-)
-*}
-
-setup Deriv_Intros.setup
-
-lemma DERIV_cong: "\<lbrakk> DERIV f x :> X ; X = Y \<rbrakk> \<Longrightarrow> DERIV f x :> Y"
-  by simp
-
-declare
-  DERIV_const[THEN DERIV_cong, DERIV_intros]
-  DERIV_ident[THEN DERIV_cong, DERIV_intros]
-  DERIV_add[THEN DERIV_cong, DERIV_intros]
-  DERIV_minus[THEN DERIV_cong, DERIV_intros]
-  DERIV_mult[THEN DERIV_cong, DERIV_intros]
-  DERIV_diff[THEN DERIV_cong, DERIV_intros]
-  DERIV_inverse'[THEN DERIV_cong, DERIV_intros]
-  DERIV_divide[THEN DERIV_cong, DERIV_intros]
-  DERIV_power[where 'a=real, THEN DERIV_cong,
-              unfolded real_of_nat_def[symmetric], DERIV_intros]
-  DERIV_setsum[THEN DERIV_cong, DERIV_intros]
-
-
-subsection {* Differentiability predicate *}
-
-definition
-  differentiable :: "['a::real_normed_field \<Rightarrow> 'a, 'a] \<Rightarrow> bool"
-    (infixl "differentiable" 60) where
-  "f differentiable x = (\<exists>D. DERIV f x :> D)"
-
-lemma differentiableE [elim?]:
-  assumes "f differentiable x"
-  obtains df where "DERIV f x :> df"
-  using assms unfolding differentiable_def ..
-
-lemma differentiableD: "f differentiable x ==> \<exists>D. DERIV f x :> D"
-by (simp add: differentiable_def)
-
-lemma differentiableI: "DERIV f x :> D ==> f differentiable x"
-by (force simp add: differentiable_def)
-
-lemma differentiable_ident [simp]: "(\<lambda>x. x) differentiable x"
-  by (rule DERIV_ident [THEN differentiableI])
-
-lemma differentiable_const [simp]: "(\<lambda>z. a) differentiable x"
-  by (rule DERIV_const [THEN differentiableI])
-
-lemma differentiable_compose:
-  assumes f: "f differentiable (g x)"
-  assumes g: "g differentiable x"
-  shows "(\<lambda>x. f (g x)) differentiable x"
-proof -
-  from `f differentiable (g x)` obtain df where "DERIV f (g x) :> df" ..
-  moreover
-  from `g differentiable x` obtain dg where "DERIV g x :> dg" ..
-  ultimately
-  have "DERIV (\<lambda>x. f (g x)) x :> df * dg" by (rule DERIV_chain2)
-  thus ?thesis by (rule differentiableI)
-qed
-
-lemma differentiable_sum [simp]:
-  assumes "f differentiable x"
-  and "g differentiable x"
-  shows "(\<lambda>x. f x + g x) differentiable x"
-proof -
-  from `f differentiable x` obtain df where "DERIV f x :> df" ..
-  moreover
-  from `g differentiable x` obtain dg where "DERIV g x :> dg" ..
-  ultimately
-  have "DERIV (\<lambda>x. f x + g x) x :> df + dg" by (rule DERIV_add)
-  thus ?thesis by (rule differentiableI)
-qed
-
-lemma differentiable_minus [simp]:
-  assumes "f differentiable x"
-  shows "(\<lambda>x. - f x) differentiable x"
-proof -
-  from `f differentiable x` obtain df where "DERIV f x :> df" ..
-  hence "DERIV (\<lambda>x. - f x) x :> - df" by (rule DERIV_minus)
-  thus ?thesis by (rule differentiableI)
-qed
-
-lemma differentiable_diff [simp]:
-  assumes "f differentiable x"
-  assumes "g differentiable x"
-  shows "(\<lambda>x. f x - g x) differentiable x"
-  unfolding diff_minus using assms by simp
-
-lemma differentiable_mult [simp]:
-  assumes "f differentiable x"
-  assumes "g differentiable x"
-  shows "(\<lambda>x. f x * g x) differentiable x"
-proof -
-  from `f differentiable x` obtain df where "DERIV f x :> df" ..
-  moreover
-  from `g differentiable x` obtain dg where "DERIV g x :> dg" ..
-  ultimately
-  have "DERIV (\<lambda>x. f x * g x) x :> df * g x + dg * f x" by (rule DERIV_mult)
-  thus ?thesis by (rule differentiableI)
-qed
-
-lemma differentiable_inverse [simp]:
-  assumes "f differentiable x" and "f x \<noteq> 0"
-  shows "(\<lambda>x. inverse (f x)) differentiable x"
-proof -
-  from `f differentiable x` obtain df where "DERIV f x :> df" ..
-  hence "DERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x) * df * inverse (f x))"
-    using `f x \<noteq> 0` by (rule DERIV_inverse')
-  thus ?thesis by (rule differentiableI)
-qed
-
-lemma differentiable_divide [simp]:
-  assumes "f differentiable x"
-  assumes "g differentiable x" and "g x \<noteq> 0"
-  shows "(\<lambda>x. f x / g x) differentiable x"
-  unfolding divide_inverse using assms by simp
-
-lemma differentiable_power [simp]:
-  fixes f :: "'a::{real_normed_field} \<Rightarrow> 'a"
-  assumes "f differentiable x"
-  shows "(\<lambda>x. f x ^ n) differentiable x"
-  apply (induct n)
-  apply simp
-  apply (simp add: assms)
-  done
-
 subsection {* Local extrema *}
 
 text{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*}
@@ -1035,26 +1388,6 @@
 
 subsection {* L'Hopitals rule *}
 
-lemma DERIV_cong_ev: "x = y \<Longrightarrow> eventually (\<lambda>x. f x = g x) (nhds x) \<Longrightarrow> u = v \<Longrightarrow>
-    DERIV f x :> u \<longleftrightarrow> DERIV g y :> v"
-  unfolding DERIV_iff2
-proof (rule filterlim_cong)
-  assume "eventually (\<lambda>x. f x = g x) (nhds x)"
-  moreover then have "f x = g x" by (auto simp: eventually_nhds)
-  moreover assume "x = y" "u = v"
-  ultimately show "eventually (\<lambda>xa. (f xa - f x) / (xa - x) = (g xa - g y) / (xa - y)) (at x)"
-    by (auto simp: eventually_at_filter elim: eventually_elim1)
-qed simp_all
-
-lemma DERIV_shift:
-  "(DERIV f (x + z) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (x + z)) x :> y)"
-  by (simp add: DERIV_iff field_simps)
-
-lemma DERIV_mirror:
-  "(DERIV f (- x) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (- x::real) :: real) x :> - y)"
-  by (simp add: deriv_def filterlim_at_split filterlim_at_left_to_right
-                tendsto_minus_cancel_left field_simps conj_commute)
-
 lemma isCont_If_ge:
   fixes a :: "'a :: linorder_topology"
   shows "continuous (at_left a) g \<Longrightarrow> (f ---> g a) (at_right a) \<Longrightarrow> isCont (\<lambda>x. if x \<le> a then g x else f x) a"
diff -r cd05e9fcc63d -r 400ec5ae7f8f src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Tue Apr 09 14:04:41 2013 +0200
+++ b/src/HOL/Library/Convex.thy	Tue Apr 09 14:04:47 2013 +0200
@@ -669,7 +669,7 @@
 proof -
   have "\<And>z. z > 0 \<Longrightarrow> DERIV (log b) z :> 1 / (ln b * z)" using DERIV_log by auto
   then have f': "\<And>z. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - log b z) z :> - 1 / (ln b * z)"
-    using DERIV_minus by auto
+    by (auto simp: DERIV_minus)
   have "\<And>z :: real. z > 0 \<Longrightarrow> DERIV inverse z :> - (inverse z ^ Suc (Suc 0))"
     using less_imp_neq[THEN not_sym, THEN DERIV_inverse] by auto
   from this[THEN DERIV_cmult, of _ "- 1 / ln b"]
diff -r cd05e9fcc63d -r 400ec5ae7f8f src/HOL/Library/FrechetDeriv.thy
--- a/src/HOL/Library/FrechetDeriv.thy	Tue Apr 09 14:04:41 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,523 +0,0 @@
-(*  Title       : FrechetDeriv.thy
-    Author      : Brian Huffman
-*)
-
-header {* Frechet Derivative *}
-
-theory FrechetDeriv
-imports Complex_Main
-begin
-
-definition
-  fderiv ::
-  "['a::real_normed_vector \<Rightarrow> 'b::real_normed_vector, 'a, 'a \<Rightarrow> 'b] \<Rightarrow> bool"
-    -- {* Frechet derivative: D is derivative of function f at x *}
-          ("(FDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where
-  "FDERIV f x :> D = (bounded_linear D \<and>
-    (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0)"
-
-lemma FDERIV_I:
-  "\<lbrakk>bounded_linear D; (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0\<rbrakk>
-   \<Longrightarrow> FDERIV f x :> D"
-by (simp add: fderiv_def)
-
-lemma FDERIV_D:
-  "FDERIV f x :> D \<Longrightarrow> (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0"
-by (simp add: fderiv_def)
-
-lemma FDERIV_bounded_linear: "FDERIV f x :> D \<Longrightarrow> bounded_linear D"
-by (simp add: fderiv_def)
-
-lemma bounded_linear_zero: "bounded_linear (\<lambda>x. 0)"
-  by (rule bounded_linear_intro [where K=0], simp_all)
-
-lemma FDERIV_const: "FDERIV (\<lambda>x. k) x :> (\<lambda>h. 0)"
-  by (simp add: fderiv_def bounded_linear_zero tendsto_const)
-
-lemma bounded_linear_ident: "bounded_linear (\<lambda>x. x)"
-  by (rule bounded_linear_intro [where K=1], simp_all)
-
-lemma FDERIV_ident: "FDERIV (\<lambda>x. x) x :> (\<lambda>h. h)"
-  by (simp add: fderiv_def bounded_linear_ident tendsto_const)
-
-subsection {* Addition *}
-
-lemma bounded_linear_add:
-  assumes "bounded_linear f"
-  assumes "bounded_linear g"
-  shows "bounded_linear (\<lambda>x. f x + g x)"
-proof -
-  interpret f: bounded_linear f by fact
-  interpret g: bounded_linear g by fact
-  show ?thesis apply (unfold_locales)
-    apply (simp only: f.add g.add add_ac)
-    apply (simp only: f.scaleR g.scaleR scaleR_right_distrib)
-    apply (rule f.pos_bounded [THEN exE], rename_tac Kf)
-    apply (rule g.pos_bounded [THEN exE], rename_tac Kg)
-    apply (rule_tac x="Kf + Kg" in exI, safe)
-    apply (subst distrib_left)
-    apply (rule order_trans [OF norm_triangle_ineq])
-    apply (rule add_mono, erule spec, erule spec)
-    done
-qed
-
-lemma norm_ratio_ineq:
-  fixes x y :: "'a::real_normed_vector"
-  fixes h :: "'b::real_normed_vector"
-  shows "norm (x + y) / norm h \<le> norm x / norm h + norm y / norm h"
-apply (rule ord_le_eq_trans)
-apply (rule divide_right_mono)
-apply (rule norm_triangle_ineq)
-apply (rule norm_ge_zero)
-apply (rule add_divide_distrib)
-done
-
-lemma FDERIV_add:
-  assumes f: "FDERIV f x :> F"
-  assumes g: "FDERIV g x :> G"
-  shows "FDERIV (\<lambda>x. f x + g x) x :> (\<lambda>h. F h + G h)"
-proof (rule FDERIV_I)
-  show "bounded_linear (\<lambda>h. F h + G h)"
-    apply (rule bounded_linear_add)
-    apply (rule FDERIV_bounded_linear [OF f])
-    apply (rule FDERIV_bounded_linear [OF g])
-    done
-next
-  have f': "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0"
-    using f by (rule FDERIV_D)
-  have g': "(\<lambda>h. norm (g (x + h) - g x - G h) / norm h) -- 0 --> 0"
-    using g by (rule FDERIV_D)
-  from f' g'
-  have "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h
-           + norm (g (x + h) - g x - G h) / norm h) -- 0 --> 0"
-    by (rule tendsto_add_zero)
-  thus "(\<lambda>h. norm (f (x + h) + g (x + h) - (f x + g x) - (F h + G h))
-           / norm h) -- 0 --> 0"
-    apply (rule real_LIM_sandwich_zero)
-     apply (simp add: divide_nonneg_pos)
-    apply (simp only: add_diff_add)
-    apply (rule norm_ratio_ineq)
-    done
-qed
-
-subsection {* Subtraction *}
-
-lemma bounded_linear_minus:
-  assumes "bounded_linear f"
-  shows "bounded_linear (\<lambda>x. - f x)"
-proof -
-  interpret f: bounded_linear f by fact
-  show ?thesis apply (unfold_locales)
-    apply (simp add: f.add)
-    apply (simp add: f.scaleR)
-    apply (simp add: f.bounded)
-    done
-qed
-
-lemma FDERIV_minus:
-  "FDERIV f x :> F \<Longrightarrow> FDERIV (\<lambda>x. - f x) x :> (\<lambda>h. - F h)"
-apply (rule FDERIV_I)
-apply (rule bounded_linear_minus)
-apply (erule FDERIV_bounded_linear)
-apply (simp only: fderiv_def minus_diff_minus norm_minus_cancel)
-done
-
-lemma FDERIV_diff:
-  "\<lbrakk>FDERIV f x :> F; FDERIV g x :> G\<rbrakk>
-   \<Longrightarrow> FDERIV (\<lambda>x. f x - g x) x :> (\<lambda>h. F h - G h)"
-by (simp only: diff_minus FDERIV_add FDERIV_minus)
-
-subsection {* Uniqueness *}
-
-lemma FDERIV_zero_unique:
-  assumes "FDERIV (\<lambda>x. 0) x :> F" shows "F = (\<lambda>h. 0)"
-proof -
-  interpret F: bounded_linear F
-    using assms by (rule FDERIV_bounded_linear)
-  let ?r = "\<lambda>h. norm (F h) / norm h"
-  have *: "?r -- 0 --> 0"
-    using assms unfolding fderiv_def by simp
-  show "F = (\<lambda>h. 0)"
-  proof
-    fix h show "F h = 0"
-    proof (rule ccontr)
-      assume "F h \<noteq> 0"
-      moreover from this have h: "h \<noteq> 0"
-        by (clarsimp simp add: F.zero)
-      ultimately have "0 < ?r h"
-        by (simp add: divide_pos_pos)
-      from LIM_D [OF * this] obtain s where s: "0 < s"
-        and r: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> ?r x < ?r h" by auto
-      from dense [OF s] obtain t where t: "0 < t \<and> t < s" ..
-      let ?x = "scaleR (t / norm h) h"
-      have "?x \<noteq> 0" and "norm ?x < s" using t h by simp_all
-      hence "?r ?x < ?r h" by (rule r)
-      thus "False" using t h by (simp add: F.scaleR)
-    qed
-  qed
-qed
-
-lemma FDERIV_unique:
-  assumes "FDERIV f x :> F" and "FDERIV f x :> F'" shows "F = F'"
-proof -
-  have "FDERIV (\<lambda>x. 0) x :> (\<lambda>h. F h - F' h)"
-    using FDERIV_diff [OF assms] by simp
-  hence "(\<lambda>h. F h - F' h) = (\<lambda>h. 0)"
-    by (rule FDERIV_zero_unique)
-  thus "F = F'"
-    unfolding fun_eq_iff right_minus_eq .
-qed
-
-subsection {* Continuity *}
-
-lemma FDERIV_isCont:
-  assumes f: "FDERIV f x :> F"
-  shows "isCont f x"
-proof -
-  from f interpret F: bounded_linear "F" by (rule FDERIV_bounded_linear)
-  have "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0"
-    by (rule FDERIV_D [OF f])
-  hence "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h * norm h) -- 0 --> 0"
-    by (intro tendsto_mult_zero tendsto_norm_zero tendsto_ident_at)
-  hence "(\<lambda>h. norm (f (x + h) - f x - F h)) -- 0 --> 0"
-    by (simp cong: LIM_cong)
-  hence "(\<lambda>h. f (x + h) - f x - F h) -- 0 --> 0"
-    by (rule tendsto_norm_zero_cancel)
-  hence "(\<lambda>h. f (x + h) - f x - F h + F h) -- 0 --> 0"
-    by (intro tendsto_add_zero F.tendsto_zero tendsto_ident_at)
-  hence "(\<lambda>h. f (x + h) - f x) -- 0 --> 0"
-    by simp
-  thus "isCont f x"
-    unfolding isCont_iff by (rule LIM_zero_cancel)
-qed
-
-subsection {* Composition *}
-
-lemma real_divide_cancel_lemma:
-  fixes a b c :: real
-  shows "(b = 0 \<Longrightarrow> a = 0) \<Longrightarrow> (a / b) * (b / c) = a / c"
-by simp
-
-lemma bounded_linear_compose:
-  assumes "bounded_linear f"
-  assumes "bounded_linear g"
-  shows "bounded_linear (\<lambda>x. f (g x))"
-proof -
-  interpret f: bounded_linear f by fact
-  interpret g: bounded_linear g by fact
-  show ?thesis proof (unfold_locales)
-    fix x y show "f (g (x + y)) = f (g x) + f (g y)"
-      by (simp only: f.add g.add)
-  next
-    fix r x show "f (g (scaleR r x)) = scaleR r (f (g x))"
-      by (simp only: f.scaleR g.scaleR)
-  next
-    from f.pos_bounded
-    obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by fast
-    from g.pos_bounded
-    obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by fast
-    show "\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K"
-    proof (intro exI allI)
-      fix x
-      have "norm (f (g x)) \<le> norm (g x) * Kf"
-        using f .
-      also have "\<dots> \<le> (norm x * Kg) * Kf"
-        using g Kf [THEN order_less_imp_le] by (rule mult_right_mono)
-      also have "(norm x * Kg) * Kf = norm x * (Kg * Kf)"
-        by (rule mult_assoc)
-      finally show "norm (f (g x)) \<le> norm x * (Kg * Kf)" .
-    qed
-  qed
-qed
-
-lemma FDERIV_compose:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
-  fixes g :: "'b::real_normed_vector \<Rightarrow> 'c::real_normed_vector"
-  assumes f: "FDERIV f x :> F"
-  assumes g: "FDERIV g (f x) :> G"
-  shows "FDERIV (\<lambda>x. g (f x)) x :> (\<lambda>h. G (F h))"
-proof (rule FDERIV_I)
-  from FDERIV_bounded_linear [OF g] FDERIV_bounded_linear [OF f]
-  show "bounded_linear (\<lambda>h. G (F h))"
-    by (rule bounded_linear_compose)
-next
-  let ?Rf = "\<lambda>h. f (x + h) - f x - F h"
-  let ?Rg = "\<lambda>k. g (f x + k) - g (f x) - G k"
-  let ?k = "\<lambda>h. f (x + h) - f x"
-  let ?Nf = "\<lambda>h. norm (?Rf h) / norm h"
-  let ?Ng = "\<lambda>h. norm (?Rg (?k h)) / norm (?k h)"
-  from f interpret F: bounded_linear "F" by (rule FDERIV_bounded_linear)
-  from g interpret G: bounded_linear "G" by (rule FDERIV_bounded_linear)
-  from F.bounded obtain kF where kF: "\<And>x. norm (F x) \<le> norm x * kF" by fast
-  from G.bounded obtain kG where kG: "\<And>x. norm (G x) \<le> norm x * kG" by fast
-
-  let ?fun2 = "\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF)"
-
-  show "(\<lambda>h. norm (g (f (x + h)) - g (f x) - G (F h)) / norm h) -- 0 --> 0"
-  proof (rule real_LIM_sandwich_zero)
-    have Nf: "?Nf -- 0 --> 0"
-      using FDERIV_D [OF f] .
-
-    have Ng1: "isCont (\<lambda>k. norm (?Rg k) / norm k) 0"
-      by (simp add: isCont_def FDERIV_D [OF g])
-    have Ng2: "?k -- 0 --> 0"
-      apply (rule LIM_zero)
-      apply (fold isCont_iff)
-      apply (rule FDERIV_isCont [OF f])
-      done
-    have Ng: "?Ng -- 0 --> 0"
-      using isCont_tendsto_compose [OF Ng1 Ng2] by simp
-
-    have "(\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF))
-           -- 0 --> 0 * kG + 0 * (0 + kF)"
-      by (intro tendsto_intros Nf Ng)
-    thus "(\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF)) -- 0 --> 0"
-      by simp
-  next
-    fix h::'a assume h: "h \<noteq> 0"
-    thus "0 \<le> norm (g (f (x + h)) - g (f x) - G (F h)) / norm h"
-      by (simp add: divide_nonneg_pos)
-  next
-    fix h::'a assume h: "h \<noteq> 0"
-    have "g (f (x + h)) - g (f x) - G (F h) = G (?Rf h) + ?Rg (?k h)"
-      by (simp add: G.diff)
-    hence "norm (g (f (x + h)) - g (f x) - G (F h)) / norm h
-           = norm (G (?Rf h) + ?Rg (?k h)) / norm h"
-      by (rule arg_cong)
-    also have "\<dots> \<le> norm (G (?Rf h)) / norm h + norm (?Rg (?k h)) / norm h"
-      by (rule norm_ratio_ineq)
-    also have "\<dots> \<le> ?Nf h * kG + ?Ng h * (?Nf h + kF)"
-    proof (rule add_mono)
-      show "norm (G (?Rf h)) / norm h \<le> ?Nf h * kG"
-        apply (rule ord_le_eq_trans)
-        apply (rule divide_right_mono [OF kG norm_ge_zero])
-        apply simp
-        done
-    next
-      have "norm (?Rg (?k h)) / norm h = ?Ng h * (norm (?k h) / norm h)"
-        apply (rule real_divide_cancel_lemma [symmetric])
-        apply (simp add: G.zero)
-        done
-      also have "\<dots> \<le> ?Ng h * (?Nf h + kF)"
-      proof (rule mult_left_mono)
-        have "norm (?k h) / norm h = norm (?Rf h + F h) / norm h"
-          by simp
-        also have "\<dots> \<le> ?Nf h + norm (F h) / norm h"
-          by (rule norm_ratio_ineq)
-        also have "\<dots> \<le> ?Nf h + kF"
-          apply (rule add_left_mono)
-          apply (subst pos_divide_le_eq, simp add: h)
-          apply (subst mult_commute)
-          apply (rule kF)
-          done
-        finally show "norm (?k h) / norm h \<le> ?Nf h + kF" .
-      next
-        show "0 \<le> ?Ng h"
-        apply (case_tac "f (x + h) - f x = 0", simp)
-        apply (rule divide_nonneg_pos [OF norm_ge_zero])
-        apply simp
-        done
-      qed
-      finally show "norm (?Rg (?k h)) / norm h \<le> ?Ng h * (?Nf h + kF)" .
-    qed
-    finally show "norm (g (f (x + h)) - g (f x) - G (F h)) / norm h
-        \<le> ?Nf h * kG + ?Ng h * (?Nf h + kF)" .
-  qed
-qed
-
-subsection {* Product Rule *}
-
-lemma (in bounded_bilinear) FDERIV_lemma:
-  "a' ** b' - a ** b - (a ** B + A ** b)
-   = a ** (b' - b - B) + (a' - a - A) ** b' + A ** (b' - b)"
-by (simp add: diff_left diff_right)
-
-lemma (in bounded_bilinear) FDERIV:
-  fixes x :: "'d::real_normed_vector"
-  assumes f: "FDERIV f x :> F"
-  assumes g: "FDERIV g x :> G"
-  shows "FDERIV (\<lambda>x. f x ** g x) x :> (\<lambda>h. f x ** G h + F h ** g x)"
-proof (rule FDERIV_I)
-  show "bounded_linear (\<lambda>h. f x ** G h + F h ** g x)"
-    apply (rule bounded_linear_add)
-    apply (rule bounded_linear_compose [OF bounded_linear_right])
-    apply (rule FDERIV_bounded_linear [OF g])
-    apply (rule bounded_linear_compose [OF bounded_linear_left])
-    apply (rule FDERIV_bounded_linear [OF f])
-    done
-next
-  from bounded_linear.bounded [OF FDERIV_bounded_linear [OF f]]
-  obtain KF where norm_F: "\<And>x. norm (F x) \<le> norm x * KF" by fast
-
-  from pos_bounded obtain K where K: "0 < K" and norm_prod:
-    "\<And>a b. norm (a ** b) \<le> norm a * norm b * K" by fast
-
-  let ?Rf = "\<lambda>h. f (x + h) - f x - F h"
-  let ?Rg = "\<lambda>h. g (x + h) - g x - G h"
-
-  let ?fun1 = "\<lambda>h.
-        norm (f x ** ?Rg h + ?Rf h ** g (x + h) + F h ** (g (x + h) - g x)) /
-        norm h"
-
-  let ?fun2 = "\<lambda>h.
-        norm (f x) * (norm (?Rg h) / norm h) * K +
-        norm (?Rf h) / norm h * norm (g (x + h)) * K +
-        KF * norm (g (x + h) - g x) * K"
-
-  have "?fun1 -- 0 --> 0"
-  proof (rule real_LIM_sandwich_zero)
-    from f g isCont_iff [THEN iffD1, OF FDERIV_isCont [OF g]]
-    have "?fun2 -- 0 -->
-          norm (f x) * 0 * K + 0 * norm (g x) * K + KF * norm (0::'b) * K"
-      by (intro tendsto_intros LIM_zero FDERIV_D)
-    thus "?fun2 -- 0 --> 0"
-      by simp
-  next
-    fix h::'d assume "h \<noteq> 0"
-    thus "0 \<le> ?fun1 h"
-      by (simp add: divide_nonneg_pos)
-  next
-    fix h::'d assume "h \<noteq> 0"
-    have "?fun1 h \<le> (norm (f x) * norm (?Rg h) * K +
-         norm (?Rf h) * norm (g (x + h)) * K +
-         norm h * KF * norm (g (x + h) - g x) * K) / norm h"
-      by (intro
-        divide_right_mono mult_mono'
-        order_trans [OF norm_triangle_ineq add_mono]
-        order_trans [OF norm_prod mult_right_mono]
-        mult_nonneg_nonneg order_refl norm_ge_zero norm_F
-        K [THEN order_less_imp_le]
-      )
-    also have "\<dots> = ?fun2 h"
-      by (simp add: add_divide_distrib)
-    finally show "?fun1 h \<le> ?fun2 h" .
-  qed
-  thus "(\<lambda>h.
-    norm (f (x + h) ** g (x + h) - f x ** g x - (f x ** G h + F h ** g x))
-    / norm h) -- 0 --> 0"
-    by (simp only: FDERIV_lemma)
-qed
-
-lemmas FDERIV_mult =
-  bounded_bilinear.FDERIV [OF bounded_bilinear_mult]
-
-lemmas FDERIV_scaleR =
-  bounded_bilinear.FDERIV [OF bounded_bilinear_scaleR]
-
-
-subsection {* Powers *}
-
-lemma FDERIV_power_Suc:
-  fixes x :: "'a::{real_normed_algebra,comm_ring_1}"
-  shows "FDERIV (\<lambda>x. x ^ Suc n) x :> (\<lambda>h. (1 + of_nat n) * x ^ n * h)"
- apply (induct n)
-  apply (simp add: FDERIV_ident)
- apply (drule FDERIV_mult [OF FDERIV_ident])
- apply (simp only: of_nat_Suc distrib_right mult_1_left)
- apply (simp only: power_Suc distrib_left add_ac mult_ac)
-done
-
-lemma FDERIV_power:
-  fixes x :: "'a::{real_normed_algebra,comm_ring_1}"
-  shows "FDERIV (\<lambda>x. x ^ n) x :> (\<lambda>h. of_nat n * x ^ (n - 1) * h)"
-  apply (cases n)
-   apply (simp add: FDERIV_const)
-  apply (simp add: FDERIV_power_Suc del: power_Suc)
-  done
-
-
-subsection {* Inverse *}
-
-lemmas bounded_linear_mult_const =
-  bounded_linear_mult_left [THEN bounded_linear_compose]
-
-lemmas bounded_linear_const_mult =
-  bounded_linear_mult_right [THEN bounded_linear_compose]
-
-lemma FDERIV_inverse:
-  fixes x :: "'a::real_normed_div_algebra"
-  assumes x: "x \<noteq> 0"
-  shows "FDERIV inverse x :> (\<lambda>h. - (inverse x * h * inverse x))"
-        (is "FDERIV ?inv _ :> _")
-proof (rule FDERIV_I)
-  show "bounded_linear (\<lambda>h. - (?inv x * h * ?inv x))"
-    apply (rule bounded_linear_minus)
-    apply (rule bounded_linear_mult_const)
-    apply (rule bounded_linear_const_mult)
-    apply (rule bounded_linear_ident)
-    done
-next
-  show "(\<lambda>h. norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h)
-        -- 0 --> 0"
-  proof (rule LIM_equal2)
-    show "0 < norm x" using x by simp
-  next
-    fix h::'a
-    assume 1: "h \<noteq> 0"
-    assume "norm (h - 0) < norm x"
-    hence "h \<noteq> -x" by clarsimp
-    hence 2: "x + h \<noteq> 0"
-      apply (rule contrapos_nn)
-      apply (rule sym)
-      apply (erule minus_unique)
-      done
-    show "norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h
-          = norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h"
-      apply (subst inverse_diff_inverse [OF 2 x])
-      apply (subst minus_diff_minus)
-      apply (subst norm_minus_cancel)
-      apply (simp add: left_diff_distrib)
-      done
-  next
-    show "(\<lambda>h. norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h)
-          -- 0 --> 0"
-    proof (rule real_LIM_sandwich_zero)
-      show "(\<lambda>h. norm (?inv (x + h) - ?inv x) * norm (?inv x))
-            -- 0 --> 0"
-        apply (rule tendsto_mult_left_zero)
-        apply (rule tendsto_norm_zero)
-        apply (rule LIM_zero)
-        apply (rule LIM_offset_zero)
-        apply (rule tendsto_inverse)
-        apply (rule tendsto_ident_at)
-        apply (rule x)
-        done
-    next
-      fix h::'a assume h: "h \<noteq> 0"
-      show "0 \<le> norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h"
-        apply (rule divide_nonneg_pos)
-        apply (rule norm_ge_zero)
-        apply (simp add: h)
-        done
-    next
-      fix h::'a assume h: "h \<noteq> 0"
-      have "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h
-            \<le> norm (?inv (x + h) - ?inv x) * norm h * norm (?inv x) / norm h"
-        apply (rule divide_right_mono [OF _ norm_ge_zero])
-        apply (rule order_trans [OF norm_mult_ineq])
-        apply (rule mult_right_mono [OF _ norm_ge_zero])
-        apply (rule norm_mult_ineq)
-        done
-      also have "\<dots> = norm (?inv (x + h) - ?inv x) * norm (?inv x)"
-        by simp
-      finally show "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h
-            \<le> norm (?inv (x + h) - ?inv x) * norm (?inv x)" .
-    qed
-  qed
-qed
-
-subsection {* Alternate definition *}
-
-lemma field_fderiv_def:
-  fixes x :: "'a::real_normed_field" shows
-  "FDERIV f x :> (\<lambda>h. h * D) = (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
- apply (unfold fderiv_def)
- apply (simp add: bounded_linear_mult_left)
- apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
- apply (subst diff_divide_distrib)
- apply (subst times_divide_eq_left [symmetric])
- apply (simp cong: LIM_cong)
- apply (simp add: tendsto_norm_zero_iff LIM_zero_iff)
-done
-
-end
diff -r cd05e9fcc63d -r 400ec5ae7f8f src/HOL/Library/Inner_Product.thy
--- a/src/HOL/Library/Inner_Product.thy	Tue Apr 09 14:04:41 2013 +0200
+++ b/src/HOL/Library/Inner_Product.thy	Tue Apr 09 14:04:47 2013 +0200
@@ -5,7 +5,7 @@
 header {* Inner Product Spaces and the Gradient Derivative *}
 
 theory Inner_Product
-imports FrechetDeriv
+imports "~~/src/HOL/Complex_Main"
 begin
 
 subsection {* Real inner product spaces *}
@@ -177,7 +177,7 @@
 lemmas isCont_inner [simp] =
   bounded_bilinear.isCont [OF bounded_bilinear_inner]
 
-lemmas FDERIV_inner =
+lemmas FDERIV_inner [FDERIV_intros] =
   bounded_bilinear.FDERIV [OF bounded_bilinear_inner]
 
 lemmas bounded_linear_inner_left =
@@ -186,6 +186,15 @@
 lemmas bounded_linear_inner_right =
   bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]
 
+lemmas FDERIV_inner_right [FDERIV_intros] =
+  bounded_linear.FDERIV [OF bounded_linear_inner_right]
+
+lemmas FDERIV_inner_left [FDERIV_intros] =
+  bounded_linear.FDERIV [OF bounded_linear_inner_left]
+
+lemma differentiable_inner [simp]:
+  "f differentiable x in s \<Longrightarrow> g differentiable x in s \<Longrightarrow> (\<lambda>x. inner (f x) (g x)) differentiable x in s"
+  unfolding isDiff_def by (blast intro: FDERIV_inner)
 
 subsection {* Class instances *}
 
@@ -260,9 +269,6 @@
 where
   "GDERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. inner h D)"
 
-lemma deriv_fderiv: "DERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. h * D)"
-  by (simp only: deriv_def field_fderiv_def)
-
 lemma gderiv_deriv [simp]: "GDERIV f x :> D \<longleftrightarrow> DERIV f x :> D"
   by (simp only: gderiv_def deriv_fderiv inner_real_def)
 
diff -r cd05e9fcc63d -r 400ec5ae7f8f src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Tue Apr 09 14:04:41 2013 +0200
+++ b/src/HOL/Library/Library.thy	Tue Apr 09 14:04:47 2013 +0200
@@ -23,7 +23,6 @@
   Float
   Formal_Power_Series
   Fraction_Field
-  FrechetDeriv
   FuncSet
   Function_Division
   Function_Growth
diff -r cd05e9fcc63d -r 400ec5ae7f8f src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Tue Apr 09 14:04:41 2013 +0200
+++ b/src/HOL/Library/Product_Vector.thy	Tue Apr 09 14:04:47 2013 +0200
@@ -480,28 +480,31 @@
 
 subsubsection {* Frechet derivatives involving pairs *}
 
-lemma FDERIV_Pair:
-  assumes f: "FDERIV f x :> f'" and g: "FDERIV g x :> g'"
-  shows "FDERIV (\<lambda>x. (f x, g x)) x :> (\<lambda>h. (f' h, g' h))"
-proof (rule FDERIV_I)
+lemma FDERIV_Pair [FDERIV_intros]:
+  assumes f: "FDERIV f x : s :> f'" and g: "FDERIV g x : s :> g'"
+  shows "FDERIV (\<lambda>x. (f x, g x)) x : s :> (\<lambda>h. (f' h, g' h))"
+proof (rule FDERIV_I_sandwich[of 1])
   show "bounded_linear (\<lambda>h. (f' h, g' h))"
     using f g by (intro bounded_linear_Pair FDERIV_bounded_linear)
-  let ?Rf = "\<lambda>h. f (x + h) - f x - f' h"
-  let ?Rg = "\<lambda>h. g (x + h) - g x - g' h"
-  let ?R = "\<lambda>h. ((f (x + h), g (x + h)) - (f x, g x) - (f' h, g' h))"
-  show "(\<lambda>h. norm (?R h) / norm h) -- 0 --> 0"
-  proof (rule real_LIM_sandwich_zero)
-    show "(\<lambda>h. norm (?Rf h) / norm h + norm (?Rg h) / norm h) -- 0 --> 0"
-      using f g by (intro tendsto_add_zero FDERIV_D)
-    fix h :: 'a assume "h \<noteq> 0"
-    thus "0 \<le> norm (?R h) / norm h"
-      by (simp add: divide_nonneg_pos)
-    show "norm (?R h) / norm h \<le> norm (?Rf h) / norm h + norm (?Rg h) / norm h"
-      unfolding add_divide_distrib [symmetric]
-      by (simp add: norm_Pair divide_right_mono
-        order_trans [OF sqrt_add_le_add_sqrt])
-  qed
-qed
+  let ?Rf = "\<lambda>y. f y - f x - f' (y - x)"
+  let ?Rg = "\<lambda>y. g y - g x - g' (y - x)"
+  let ?R = "\<lambda>y. ((f y, g y) - (f x, g x) - (f' (y - x), g' (y - x)))"
+
+  show "((\<lambda>y. norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)) ---> 0) (at x within s)"
+    using f g by (intro tendsto_add_zero) (auto simp: FDERIV_iff_norm)
+
+  fix y :: 'a assume "y \<noteq> x"
+  show "norm (?R y) / norm (y - x) \<le> norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)"
+    unfolding add_divide_distrib [symmetric]
+    by (simp add: norm_Pair divide_right_mono order_trans [OF sqrt_add_le_add_sqrt])
+qed simp
+
+lemmas FDERIV_fst [FDERIV_intros] = bounded_linear.FDERIV [OF bounded_linear_fst]
+lemmas FDERIV_snd [FDERIV_intros] = bounded_linear.FDERIV [OF bounded_linear_snd]
+
+lemma FDERIV_split [FDERIV_intros]:
+  "((\<lambda>p. f (fst p) (snd p)) has_derivative f') F \<Longrightarrow> ((\<lambda>(a, b). f a b) has_derivative f') F"
+  unfolding split_beta' .
 
 subsection {* Product is an inner product space *}
 
diff -r cd05e9fcc63d -r 400ec5ae7f8f src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Tue Apr 09 14:04:41 2013 +0200
+++ b/src/HOL/Limits.thy	Tue Apr 09 14:04:47 2013 +0200
@@ -1532,6 +1532,11 @@
   shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
 by (drule_tac k="- a" in LIM_offset, simp)
 
+lemma LIM_offset_zero_iff:
+  fixes f :: "'a :: real_normed_vector \<Rightarrow> _"
+  shows  "f -- a --> L \<longleftrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
+  using LIM_offset_zero_cancel[of f a L] LIM_offset_zero[of f L a] by auto
+
 lemma LIM_zero:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. f x - l) ---> 0) F"
diff -r cd05e9fcc63d -r 400ec5ae7f8f src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Apr 09 14:04:41 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Apr 09 14:04:47 2013 +0200
@@ -9,26 +9,15 @@
 imports Brouwer_Fixpoint Operator_Norm
 begin
 
-(* Because I do not want to type this all the time *)
-lemmas linear_linear = linear_conv_bounded_linear[THEN sym]
-
-subsection {* Derivatives *}
-
-text {* The definition is slightly tricky since we make it work over
-  nets of a particular form. This lets us prove theorems generally and use 
-  "at a" or "at a within s" for restriction to a set (1-sided on R etc.) *}
+lemma bounded_linear_imp_linear: "bounded_linear f \<Longrightarrow> linear f" (* TODO: move elsewhere *)
+proof -
+  assume "bounded_linear f"
+  then interpret f: bounded_linear f .
+  show "linear f"
+    by (simp add: f.add f.scaleR linear_def)
+qed
 
-definition has_derivative :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a filter \<Rightarrow> bool)"
-(infixl "(has'_derivative)" 12) where
- "(f has_derivative f') net \<equiv> bounded_linear f' \<and> ((\<lambda>y. (1 / (norm (y - netlimit net))) *\<^sub>R
-   (f y - (f (netlimit net) + f'(y - netlimit net)))) ---> 0) net"
-
-lemma derivative_linear[dest]:
-  "(f has_derivative f') net \<Longrightarrow> bounded_linear f'"
-  unfolding has_derivative_def by auto
-
-lemma netlimit_at_vector:
-  (* TODO: move *)
+lemma netlimit_at_vector: (* TODO: move *)
   fixes a :: "'a::real_normed_vector"
   shows "netlimit (at a) = a"
 proof (cases "\<exists>x. x \<noteq> a")
@@ -43,22 +32,63 @@
     by (rule netlimit_within [of a UNIV])
 qed simp
 
-lemma FDERIV_conv_has_derivative:
-  shows "FDERIV f x :> f' = (f has_derivative f') (at x)"
-  unfolding fderiv_def has_derivative_def netlimit_at_vector
-  by (simp add: diff_diff_eq Lim_at_zero [where a=x]
-    tendsto_norm_zero_iff [where 'b='b, symmetric])
+(* Because I do not want to type this all the time *)
+lemmas linear_linear = linear_conv_bounded_linear[THEN sym]
+
+lemma derivative_linear[dest]:
+  "(f has_derivative f') net \<Longrightarrow> bounded_linear f'"
+  unfolding has_derivative_def by auto
+
+lemma derivative_is_linear:
+  "(f has_derivative f') net \<Longrightarrow> linear f'"
+  by (rule derivative_linear [THEN bounded_linear_imp_linear])
 
 lemma DERIV_conv_has_derivative:
   "(DERIV f x :> f') = (f has_derivative op * f') (at x)"
-  unfolding deriv_fderiv FDERIV_conv_has_derivative
-  by (subst mult_commute, rule refl)
+  using deriv_fderiv[of f x UNIV f'] by (subst (asm) mult_commute)
+
+subsection {* Derivatives *}
+
+subsubsection {* Combining theorems. *}
+
+lemmas has_derivative_id = FDERIV_ident
+lemmas has_derivative_const = FDERIV_const
+lemmas has_derivative_neg = FDERIV_minus
+lemmas has_derivative_add = FDERIV_add
+lemmas has_derivative_sub = FDERIV_diff
+lemmas has_derivative_setsum = FDERIV_setsum
+lemmas scaleR_right_has_derivative = FDERIV_scaleR_right
+lemmas scaleR_left_has_derivative = FDERIV_scaleR_left
+lemmas inner_right_has_derivative = FDERIV_inner_right
+lemmas inner_left_has_derivative = FDERIV_inner_left
+lemmas mult_right_has_derivative = FDERIV_mult_right
+lemmas mult_left_has_derivative = FDERIV_mult_left
+
+lemma has_derivative_add_const:
+  "(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net"
+  by (intro FDERIV_eq_intros) auto
+
+subsection {* Derivative with composed bilinear function. *}
+
+lemma has_derivative_bilinear_within:
+  assumes "(f has_derivative f') (at x within s)"
+  assumes "(g has_derivative g') (at x within s)"
+  assumes "bounded_bilinear h"
+  shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x within s)"
+  using bounded_bilinear.FDERIV[OF assms(3,1,2)] .
+
+lemma has_derivative_bilinear_at:
+  assumes "(f has_derivative f') (at x)"
+  assumes "(g has_derivative g') (at x)"
+  assumes "bounded_bilinear h"
+  shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x)"
+  using has_derivative_bilinear_within[of f f' x UNIV g g' h] assms by simp
 
 text {* These are the only cases we'll care about, probably. *}
 
 lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow>
          bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x within s)"
-  unfolding has_derivative_def and Lim by(auto simp add:netlimit_within)
+  unfolding has_derivative_def Lim by (auto simp add: netlimit_within inverse_eq_divide field_simps)
 
 lemma has_derivative_at: "(f has_derivative f') (at x) \<longleftrightarrow>
          bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x)"
@@ -102,111 +132,6 @@
     by (simp add: bounded_linear_mult_right has_derivative_within)
 qed
 
-lemma bounded_linear_imp_linear: "bounded_linear f \<Longrightarrow> linear f" (* TODO: move elsewhere *)
-proof -
-  assume "bounded_linear f"
-  then interpret f: bounded_linear f .
-  show "linear f"
-    by (simp add: f.add f.scaleR linear_def)
-qed
-
-lemma derivative_is_linear:
-  "(f has_derivative f') net \<Longrightarrow> linear f'"
-  by (rule derivative_linear [THEN bounded_linear_imp_linear])
-
-subsubsection {* Combining theorems. *}
-
-lemma has_derivative_eq_rhs: "(f has_derivative x) F \<Longrightarrow> x = y \<Longrightarrow> (f has_derivative y) F"
-  by simp
-
-ML {*
-
-structure Has_Derivative_Intros = Named_Thms
-(
-  val name = @{binding has_derivative_intros}
-  val description = "introduction rules for has_derivative"
-)
-
-*}
-
-setup {*
-  Has_Derivative_Intros.setup #>
-  Global_Theory.add_thms_dynamic (@{binding has_derivative_eq_intros},
-    map (fn thm => @{thm has_derivative_eq_rhs} OF [thm]) o Has_Derivative_Intros.get o Context.proof_of);
-*}
-
-lemma has_derivative_id[has_derivative_intros]: "((\<lambda>x. x) has_derivative (\<lambda>h. h)) net"
-  unfolding has_derivative_def
-  by (simp add: bounded_linear_ident tendsto_const)
-
-lemma has_derivative_const[has_derivative_intros]: "((\<lambda>x. c) has_derivative (\<lambda>h. 0)) net"
-  unfolding has_derivative_def
-  by (simp add: bounded_linear_zero tendsto_const)
-
-lemma (in bounded_linear) has_derivative'[has_derivative_intros]: "(f has_derivative f) net"
-  unfolding has_derivative_def apply(rule,rule bounded_linear_axioms)
-  unfolding diff by (simp add: tendsto_const)
-
-lemma (in bounded_linear) bounded_linear: "bounded_linear f" ..
-
-lemma (in bounded_linear) has_derivative[has_derivative_intros]:
-  assumes "((\<lambda>x. g x) has_derivative (\<lambda>h. g' h)) net"
-  shows "((\<lambda>x. f (g x)) has_derivative (\<lambda>h. f (g' h))) net"
-  using assms unfolding has_derivative_def
-  apply safe
-  apply (erule bounded_linear_compose [OF local.bounded_linear])
-  apply (drule local.tendsto)
-  apply (simp add: local.scaleR local.diff local.add local.zero)
-  done
-
-lemmas scaleR_right_has_derivative[has_derivative_intros] =
-  bounded_linear.has_derivative [OF bounded_linear_scaleR_right]
-
-lemmas scaleR_left_has_derivative[has_derivative_intros] =
-  bounded_linear.has_derivative [OF bounded_linear_scaleR_left]
-
-lemmas inner_right_has_derivative[has_derivative_intros] =
-  bounded_linear.has_derivative [OF bounded_linear_inner_right]
-
-lemmas inner_left_has_derivative[has_derivative_intros] =
-  bounded_linear.has_derivative [OF bounded_linear_inner_left]
-
-lemmas mult_right_has_derivative[has_derivative_intros] =
-  bounded_linear.has_derivative [OF bounded_linear_mult_right]
-
-lemmas mult_left_has_derivative[has_derivative_intros] =
-  bounded_linear.has_derivative [OF bounded_linear_mult_left]
-
-lemma has_derivative_neg[has_derivative_intros]:
-  assumes "(f has_derivative f') net"
-  shows "((\<lambda>x. -(f x)) has_derivative (\<lambda>h. -(f' h))) net"
-  using scaleR_right_has_derivative [where r="-1", OF assms] by auto
-
-lemma has_derivative_add[has_derivative_intros]:
-  assumes "(f has_derivative f') net" and "(g has_derivative g') net"
-  shows "((\<lambda>x. f(x) + g(x)) has_derivative (\<lambda>h. f'(h) + g'(h))) net"
-proof-
-  note as = assms[unfolded has_derivative_def]
-  show ?thesis unfolding has_derivative_def apply(rule,rule bounded_linear_add)
-    using tendsto_add[OF as(1)[THEN conjunct2] as(2)[THEN conjunct2]] and as
-    by (auto simp add: algebra_simps)
-qed
-
-lemma has_derivative_add_const:
-  "(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net"
-  by (intro has_derivative_eq_intros) auto
-
-lemma has_derivative_sub[has_derivative_intros]:
-  assumes "(f has_derivative f') net" and "(g has_derivative g') net"
-  shows "((\<lambda>x. f(x) - g(x)) has_derivative (\<lambda>h. f'(h) - g'(h))) net"
-  unfolding diff_minus by (intro has_derivative_intros assms)
-
-lemma has_derivative_setsum[has_derivative_intros]:
-  assumes "finite s" and "\<forall>a\<in>s. ((f a) has_derivative (f' a)) net"
-  shows "((\<lambda>x. setsum (\<lambda>a. f a x) s) has_derivative (\<lambda>h. setsum (\<lambda>a. f' a h) s)) net"
-  using assms by (induct, simp_all add: has_derivative_const has_derivative_add)
-text {* Somewhat different results for derivative of scalar multiplier. *}
-
 subsubsection {* Limit transformation for derivatives *}
 
 lemma has_derivative_transform_within:
@@ -232,12 +157,14 @@
 
 no_notation Deriv.differentiable (infixl "differentiable" 60)
 
-definition differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" (infixr "differentiable" 30) where
-  "f differentiable net \<equiv> (\<exists>f'. (f has_derivative f') net)"
+abbreviation differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" (infixr "differentiable" 30) where
+  "f differentiable net \<equiv> isDiff net f"
 
 definition differentiable_on :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "differentiable'_on" 30) where
   "f differentiable_on s \<equiv> (\<forall>x\<in>s. f differentiable (at x within s))"
 
+lemmas differentiable_def = isDiff_def
+
 lemma differentiableI: "(f has_derivative f') net \<Longrightarrow> f differentiable net"
   unfolding differentiable_def by auto
 
@@ -292,32 +219,8 @@
   by(auto intro!: mult_strict_mono[of _ "1::real", unfolded mult_1_left])
 
 lemma differentiable_imp_continuous_within:
-  assumes "f differentiable (at x within s)" 
-  shows "continuous (at x within s) f"
-proof-
-  from assms guess f' unfolding differentiable_def has_derivative_within ..
-  note f'=this
-  then interpret bounded_linear f' by auto
-  have *:"\<And>xa. x\<noteq>xa \<Longrightarrow> (f' \<circ> (\<lambda>y. y - x)) xa + norm (xa - x) *\<^sub>R ((1 / norm (xa - x)) *\<^sub>R (f xa - (f x + f' (xa - x)))) - ((f' \<circ> (\<lambda>y. y - x)) x + 0) = f xa - f x"
-    using zero by auto
-  have **:"continuous (at x within s) (f' \<circ> (\<lambda>y. y - x))"
-    apply(rule continuous_within_compose) apply(rule continuous_intros)+
-    by(rule linear_continuous_within[OF f'[THEN conjunct1]])
-  show ?thesis unfolding continuous_within
-    using f'[THEN conjunct2, THEN Lim_mul_norm_within]
-    apply- apply(drule tendsto_add)
-    apply(rule **[unfolded continuous_within])
-    unfolding Lim_within and dist_norm
-    apply (rule, rule)
-    apply (erule_tac x=e in allE)
-    apply (erule impE | assumption)+
-    apply (erule exE, rule_tac x=d in exI)
-    by (auto simp add: zero *)
-qed
-
-lemma differentiable_imp_continuous_at:
-  "f differentiable at x \<Longrightarrow> continuous (at x) f"
- by(rule differentiable_imp_continuous_within[of _ x UNIV])
+  "f differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
+  by (auto simp: differentiable_def intro: FDERIV_continuous)
 
 lemma differentiable_imp_continuous_on:
   "f differentiable_on s \<Longrightarrow> continuous_on s f"
@@ -390,132 +293,25 @@
 
 subsection {* The chain rule. *}
 
-lemma diff_chain_within[has_derivative_intros]:
+lemma diff_chain_within[FDERIV_intros]:
   assumes "(f has_derivative f') (at x within s)"
   assumes "(g has_derivative g') (at (f x) within (f ` s))"
   shows "((g o f) has_derivative (g' o f'))(at x within s)"
-  unfolding has_derivative_within_alt
-  apply(rule,rule bounded_linear_compose[unfolded o_def[THEN sym]])
-  apply(rule assms(2)[unfolded has_derivative_def,THEN conjE],assumption)
-  apply(rule assms(1)[unfolded has_derivative_def,THEN conjE],assumption)
-proof(rule,rule)
-  note assms = assms[unfolded has_derivative_within_alt]
-  fix e::real assume "0<e"
-  guess B1 using bounded_linear.pos_bounded[OF assms(1)[THEN conjunct1, rule_format]] .. note B1 = this
-  guess B2 using bounded_linear.pos_bounded[OF assms(2)[THEN conjunct1, rule_format]] .. note B2 = this
-  have *:"e / 2 / B2 > 0" using `e>0` B2 apply-apply(rule divide_pos_pos) by auto
-  guess d1 using assms(1)[THEN conjunct2, rule_format, OF *] .. note d1 = this
-  have *:"e / 2 / (1 + B1) > 0" using `e>0` B1 apply-apply(rule divide_pos_pos) by auto
-  guess de using assms(2)[THEN conjunct2, rule_format, OF *] .. note de = this
-  guess d2 using assms(1)[THEN conjunct2, rule_format, OF zero_less_one] .. note d2 = this
-
-  def d0 \<equiv> "(min d1 d2)/2" have d0:"d0>0" "d0 < d1" "d0 < d2" unfolding d0_def using d1 d2 by auto
-  def d \<equiv> "(min d0 (de / (B1 + 1))) / 2" have "de * 2 / (B1 + 1) > de / (B1 + 1)" apply(rule divide_strict_right_mono) using B1 de by auto
-  hence d:"d>0" "d < d1" "d < d2" "d < (de / (B1 + 1))" unfolding d_def using d0 d1 d2 de B1 by(auto intro!: divide_pos_pos simp add:min_less_iff_disj not_less)
-
-  show "\<exists>d>0. \<forall>y\<in>s. norm (y - x) < d \<longrightarrow> norm ((g \<circ> f) y - (g \<circ> f) x - (g' \<circ> f') (y - x)) \<le> e * norm (y - x)" apply(rule_tac x=d in exI)
-    proof(rule,rule `d>0`,rule,rule) 
-    fix y assume as:"y \<in> s" "norm (y - x) < d"
-    hence 1:"norm (f y - f x - f' (y - x)) \<le> min (norm (y - x)) (e / 2 / B2 * norm (y - x))" using d1 d2 d by auto
-
-    have "norm (f y - f x) \<le> norm (f y - f x - f' (y - x)) + norm (f' (y - x))"
-      using norm_triangle_sub[of "f y - f x" "f' (y - x)"]
-      by(auto simp add:algebra_simps)
-    also have "\<dots> \<le> norm (f y - f x - f' (y - x)) + B1 * norm (y - x)"
-      apply(rule add_left_mono) using B1 by(auto simp add:algebra_simps)
-    also have "\<dots> \<le> min (norm (y - x)) (e / 2 / B2 * norm (y - x)) + B1 * norm (y - x)"
-      apply(rule add_right_mono) using d1 d2 d as by auto
-    also have "\<dots> \<le> norm (y - x) + B1 * norm (y - x)" by auto
-    also have "\<dots> = norm (y - x) * (1 + B1)" by(auto simp add:field_simps)
-    finally have 3:"norm (f y - f x) \<le> norm (y - x) * (1 + B1)" by auto 
+  using FDERIV_in_compose[OF assms] by (simp add: comp_def)
 
-    hence "norm (f y - f x) \<le> d * (1 + B1)" apply-
-      apply(rule order_trans,assumption,rule mult_right_mono)
-      using as B1 by auto 
-    also have "\<dots> < de" using d B1 by(auto simp add:field_simps) 
-    finally have "norm (g (f y) - g (f x) - g' (f y - f x)) \<le> e / 2 / (1 + B1) * norm (f y - f x)"
-      apply-apply(rule de[THEN conjunct2,rule_format])
-      using `y\<in>s` using d as by auto 
-    also have "\<dots> = (e / 2) * (1 / (1 + B1) * norm (f y - f x))" by auto 
-    also have "\<dots> \<le> e / 2 * norm (y - x)" apply(rule mult_left_mono)
-      using `e>0` and 3 using B1 and `e>0` by(auto simp add:divide_le_eq)
-    finally have 4:"norm (g (f y) - g (f x) - g' (f y - f x)) \<le> e / 2 * norm (y - x)" by auto
-    
-    interpret g': bounded_linear g' using assms(2) by auto
-    interpret f': bounded_linear f' using assms(1) by auto
-    have "norm (- g' (f' (y - x)) + g' (f y - f x)) = norm (g' (f y - f x - f' (y - x)))"
-      by(auto simp add:algebra_simps f'.diff g'.diff g'.add)
-    also have "\<dots> \<le> B2 * norm (f y - f x - f' (y - x))" using B2
-      by (auto simp add: algebra_simps)
-    also have "\<dots> \<le> B2 * (e / 2 / B2 * norm (y - x))"
-      apply (rule mult_left_mono) using as d1 d2 d B2 by auto 
-    also have "\<dots> \<le> e / 2 * norm (y - x)" using B2 by auto
-    finally have 5:"norm (- g' (f' (y - x)) + g' (f y - f x)) \<le> e / 2 * norm (y - x)" by auto
-    
-    have "norm (g (f y) - g (f x) - g' (f y - f x)) + norm (g (f y) - g (f x) - g' (f' (y - x)) - (g (f y) - g (f x) - g' (f y - f x))) \<le> e * norm (y - x)"
-      using 5 4 by auto
-    thus "norm ((g \<circ> f) y - (g \<circ> f) x - (g' \<circ> f') (y - x)) \<le> e * norm (y - x)"
-      unfolding o_def apply- apply(rule order_trans, rule norm_triangle_sub)
-      by assumption
-  qed
-qed
+lemma diff_chain_at[FDERIV_intros]:
+  "(f has_derivative f') (at x) \<Longrightarrow> (g has_derivative g') (at (f x)) \<Longrightarrow> ((g o f) has_derivative (g' o f')) (at x)"
+  using FDERIV_compose[of f f' x UNIV g g'] by (simp add: comp_def)
 
-lemma diff_chain_at[has_derivative_intros]:
-  "(f has_derivative f') (at x) \<Longrightarrow> (g has_derivative g') (at (f x)) \<Longrightarrow> ((g o f) has_derivative (g' o f')) (at x)"
-  using diff_chain_within[of f f' x UNIV g g']
-  using has_derivative_within_subset[of g g' "f x" UNIV "range f"]
-  by simp
 
 subsection {* Composition rules stated just for differentiability. *}
 
-lemma differentiable_const [intro]:
-  "(\<lambda>z. c) differentiable (net::'a::real_normed_vector filter)"
-  unfolding differentiable_def using has_derivative_const by auto
-
-lemma differentiable_id [intro]:
-  "(\<lambda>z. z) differentiable (net::'a::real_normed_vector filter)"
-    unfolding differentiable_def using has_derivative_id by auto
-
-lemma differentiable_cmul [intro]:
-  "f differentiable net \<Longrightarrow>
-  (\<lambda>x. c *\<^sub>R f(x)) differentiable (net::'a::real_normed_vector filter)"
-  unfolding differentiable_def
-  apply(erule exE, drule scaleR_right_has_derivative) by auto
-
-lemma differentiable_neg [intro]:
-  "f differentiable net \<Longrightarrow>
-  (\<lambda>z. -(f z)) differentiable (net::'a::real_normed_vector filter)"
-  unfolding differentiable_def
-  apply(erule exE, drule has_derivative_neg) by auto
-
-lemma differentiable_add [intro]: "f differentiable net \<Longrightarrow> g differentiable net
-   \<Longrightarrow> (\<lambda>z. f z + g z) differentiable net"
-  by (auto intro: has_derivative_eq_intros simp: differentiable_def)
-
-lemma differentiable_sub [intro]: "f differentiable net \<Longrightarrow> g differentiable net
-  \<Longrightarrow> (\<lambda>z. f z - g z) differentiable net"
-  by (auto intro: has_derivative_eq_intros simp: differentiable_def)
-
-lemma differentiable_setsum [intro]:
-  assumes "finite s" "\<forall>a\<in>s. (f a) differentiable net"
-  shows "(\<lambda>x. setsum (\<lambda>a. f a x) s) differentiable net"
-proof-
-  guess f' using bchoice[OF assms(2)[unfolded differentiable_def]] ..
-  thus ?thesis unfolding differentiable_def apply-
-    apply(rule,rule has_derivative_setsum[where f'=f'],rule assms(1)) by auto
-qed
-
-lemma differentiable_setsum_numseg:
-  shows "\<forall>i. m \<le> i \<and> i \<le> n \<longrightarrow> (f i) differentiable net \<Longrightarrow> (\<lambda>x. setsum (\<lambda>a. f a x) {m::nat..n}) differentiable net"
-  apply(rule differentiable_setsum) using finite_atLeastAtMost[of n m] by auto
-
 lemma differentiable_chain_at:
-  "f differentiable (at x) \<Longrightarrow> g differentiable (at(f x)) \<Longrightarrow> (g o f) differentiable (at x)"
+  "f differentiable (at x) \<Longrightarrow> g differentiable (at (f x)) \<Longrightarrow> (g o f) differentiable (at x)"
   unfolding differentiable_def by(meson diff_chain_at)
 
 lemma differentiable_chain_within:
-  "f differentiable (at x within s) \<Longrightarrow> g differentiable (at(f x) within (f ` s))
-   \<Longrightarrow> (g o f) differentiable (at x within s)"
+  "f differentiable (at x within s) \<Longrightarrow> g differentiable (at(f x) within (f ` s)) \<Longrightarrow> (g o f) differentiable (at x within s)"
   unfolding differentiable_def by(meson diff_chain_within)
 
 subsection {* Uniqueness of derivative *}
@@ -567,13 +363,12 @@
       unfolding dist_norm
       unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff
         scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib
-      using i by auto
+      using i by (auto simp: inverse_eq_divide)
   qed
 qed
 
 lemma frechet_derivative_unique_at:
   shows "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f'') (at x) \<Longrightarrow> f' = f''"
-  unfolding FDERIV_conv_has_derivative [symmetric]
   by (rule FDERIV_unique)
 
 lemma frechet_derivative_unique_within_closed_interval:
@@ -735,7 +530,8 @@
   show ?thesis by (simp add: fun_eq_iff)
 qed
 
-lemma rolle: fixes f::"real\<Rightarrow>real"
+lemma rolle:
+  fixes f::"real\<Rightarrow>real"
   assumes "a < b" and "f a = f b" and "continuous_on {a..b} f"
   assumes "\<forall>x\<in>{a<..<b}. (f has_derivative f'(x)) (at x)"
   shows "\<exists>x\<in>{a<..<b}. f' x = (\<lambda>v. 0)"
@@ -782,8 +578,7 @@
   proof (intro rolle[OF assms(1), of "\<lambda>x. f x - (f b - f a) / (b - a) * x"] ballI)
     fix x assume x:"x \<in> {a<..<b}"
     show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
-      by (intro has_derivative_intros assms(3)[rule_format,OF x]
-        mult_right_has_derivative)
+      by (intro FDERIV_intros assms(3)[rule_format,OF x] mult_right_has_derivative)
   qed (insert assms(1,2), auto intro!: continuous_on_intros simp: field_simps)
   then guess x ..
   thus ?thesis apply(rule_tac x=x in bexI)
@@ -827,8 +622,9 @@
 proof-
   have "\<exists>x\<in>{a<..<b}. (op \<bullet> (f b - f a) \<circ> f) b - (op \<bullet> (f b - f a) \<circ> f) a = (f b - f a) \<bullet> f' x (b - a)"
     apply(rule mvt) apply(rule assms(1))
-    apply(rule continuous_on_inner continuous_on_intros assms(2))+
-    unfolding o_def apply(rule,rule has_derivative_intros)
+    apply(rule continuous_on_inner continuous_on_intros assms(2) ballI)+
+    unfolding o_def
+    apply(rule FDERIV_inner_right)
     using assms(3) by auto
   then guess x .. note x=this
   show ?thesis proof(cases "f a = f b")
@@ -873,7 +669,7 @@
     case goal1
     let ?u = "x + u *\<^sub>R (y - x)"
     have "(f \<circ> ?p has_derivative (f' ?u) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u within {0<..<1})" 
-      apply(rule diff_chain_within) apply(rule has_derivative_intros)+ 
+      apply(rule diff_chain_within) apply(rule FDERIV_intros)+ 
       apply(rule has_derivative_within_subset)
       apply(rule assms(2)[rule_format]) using goal1 * by auto
     thus ?case
@@ -1252,7 +1048,7 @@
   apply(rule has_derivative_inverse_strong[where g'="g' x" and f=f])
   apply(rule assms)+
   unfolding continuous_on_eq_continuous_at[OF assms(1)]
-  apply(rule,rule differentiable_imp_continuous_at)
+  apply(rule,rule differentiable_imp_continuous_within)
   unfolding differentiable_def using assms by auto
 
 text {* Invertible derivative continous at a point implies local
@@ -1306,13 +1102,15 @@
         have *:"(\<lambda>v. v - g' (f' u v)) = g' \<circ> (\<lambda>w. f' a w - f' u w)"
           unfolding o_def and diff using f'g' by auto
         show "(ph has_derivative (\<lambda>v. v - g' (f' u v))) (at u within ball a d)"
-          unfolding ph' * apply(rule diff_chain_within) defer
-          apply(rule bounded_linear.has_derivative'[OF assms(3)])
-          apply(rule has_derivative_intros) defer
+          unfolding ph' *
+          apply(simp add: comp_def)
+          apply(rule bounded_linear.FDERIV[OF assms(3)])
+          apply(rule FDERIV_intros) defer
           apply(rule has_derivative_sub[where g'="\<lambda>x.0",unfolded diff_0_right])
           apply(rule has_derivative_at_within)
           using assms(5) and `u\<in>s` `a\<in>s`
-          by(auto intro!: has_derivative_intros bounded_linear.has_derivative' derivative_linear)
+          apply (auto intro!: FDERIV_intros bounded_linear.FDERIV[of _ "\<lambda>x. x"] derivative_linear)
+          done
         have **:"bounded_linear (\<lambda>x. f' u x - f' a x)"
           "bounded_linear (\<lambda>x. f' a x - f' u x)"
           apply(rule_tac[!] bounded_linear_sub)
@@ -1354,7 +1152,7 @@
   proof-
     fix x assume "x\<in>s"
     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)"
-      by(rule has_derivative_intros assms(2)[rule_format] `x\<in>s`)+
+      by(rule FDERIV_intros assms(2)[rule_format] `x\<in>s`)+
     { fix h
       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)"
         using norm_triangle_ineq[of "f' m x h - g' x h" "- f' n x h + g' x h"]
@@ -1587,88 +1385,12 @@
   shows "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) sums_seq (g x)) k \<and> (g has_derivative g'(x)) (at x within s)"
   unfolding sums_seq_def
   apply(rule has_derivative_sequence[OF assms(1) _ assms(3)])
-  apply(rule,rule)
-  apply(rule has_derivative_setsum) defer
-  apply(rule,rule assms(2)[rule_format],assumption)
+  apply(rule, rule)
+  apply(rule has_derivative_setsum)
+  apply(rule assms(2)[rule_format])
+  apply assumption
   using assms(4-5) unfolding sums_seq_def by auto
 
-subsection {* Derivative with composed bilinear function. *}
-
-lemma has_derivative_bilinear_within:
-  assumes "(f has_derivative f') (at x within s)"
-  assumes "(g has_derivative g') (at x within s)"
-  assumes "bounded_bilinear h"
-  shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x within s)"
-proof-
-  have "(g ---> g x) (at x within s)"
-    apply(rule differentiable_imp_continuous_within[unfolded continuous_within])
-    using assms(2) unfolding differentiable_def by auto
-  moreover
-  interpret f':bounded_linear f'
-    using assms unfolding has_derivative_def by auto
-  interpret g':bounded_linear g'
-    using assms unfolding has_derivative_def by auto
-  interpret h:bounded_bilinear h
-    using assms by auto
-  have "((\<lambda>y. f' (y - x)) ---> 0) (at x within s)"
-    unfolding f'.zero[THEN sym]
-    using bounded_linear.tendsto [of f' "\<lambda>y. y - x" 0 "at x within s"]
-    using tendsto_diff [OF Lim_within_id tendsto_const, of x x s]
-    unfolding id_def using assms(1) unfolding has_derivative_def by auto
-  hence "((\<lambda>y. f x + f' (y - x)) ---> f x) (at x within s)"
-    using tendsto_add[OF tendsto_const, of "\<lambda>y. f' (y - x)" 0 "at x within s" "f x"]
-    by auto
-  ultimately
-  have *:"((\<lambda>x'. h (f x + f' (x' - x)) ((1/(norm (x' - x))) *\<^sub>R (g x' - (g x + g' (x' - x))))
-             + h ((1/ (norm (x' - x))) *\<^sub>R (f x' - (f x + f' (x' - x)))) (g x')) ---> h (f x) 0 + h 0 (g x)) (at x within s)"
-    apply-apply(rule tendsto_add) apply(rule_tac[!] Lim_bilinear[OF _ _ assms(3)])
-    using assms(1-2)  unfolding has_derivative_within by auto
-  guess B using bounded_bilinear.pos_bounded[OF assms(3)] .. note B=this
-  guess C using f'.pos_bounded .. note C=this
-  guess D using g'.pos_bounded .. note D=this
-  have bcd:"B * C * D > 0" using B C D by (auto intro!: mult_pos_pos)
-  have **:"((\<lambda>y. (1/(norm(y - x))) *\<^sub>R (h (f'(y - x)) (g'(y - x)))) ---> 0) (at x within s)"
-    unfolding Lim_within
-  proof(rule,rule) case goal1
-    hence "e/(B*C*D)>0" using B C D by(auto intro!:divide_pos_pos mult_pos_pos)
-    thus ?case apply(rule_tac x="e/(B*C*D)" in exI,rule)
-    proof(rule,rule,erule conjE)
-      fix y assume as:"y \<in> s" "0 < dist y x" "dist y x < e / (B * C * D)"
-      have "norm (h (f' (y - x)) (g' (y - x))) \<le> norm (f' (y - x)) * norm (g' (y - x)) * B" using B by auto
-      also have "\<dots> \<le> (norm (y - x) * C) * (D * norm (y - x)) * B"
-        apply(rule mult_right_mono)
-        apply(rule mult_mono) using B C D
-        by (auto simp add: field_simps intro!:mult_nonneg_nonneg)
-      also have "\<dots> = (B * C * D * norm (y - x)) * norm (y - x)"
-        by (auto simp add: field_simps)
-      also have "\<dots> < e * norm (y - x)"
-        apply(rule mult_strict_right_mono)
-        using as(3)[unfolded dist_norm] and as(2)
-        unfolding pos_less_divide_eq[OF bcd] by (auto simp add: field_simps)
-      finally show "dist ((1 / norm (y - x)) *\<^sub>R h (f' (y - x)) (g' (y - x))) 0 < e"
-        unfolding dist_norm apply-apply(cases "y = x")
-        by(auto simp add: field_simps)
-    qed
-  qed
-  have "bounded_linear (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))"
-    apply (rule bounded_linear_add)
-    apply (rule bounded_linear_compose [OF h.bounded_linear_right `bounded_linear g'`])
-    apply (rule bounded_linear_compose [OF h.bounded_linear_left `bounded_linear f'`])
-    done
-  thus ?thesis using tendsto_add[OF * **] unfolding has_derivative_within 
-    unfolding g'.add f'.scaleR f'.add g'.scaleR f'.diff g'.diff
-     h.add_right h.add_left scaleR_right_distrib h.scaleR_left h.scaleR_right h.diff_right h.diff_left
-    scaleR_right_diff_distrib h.zero_right h.zero_left
-    by(auto simp add:field_simps)
-qed
-
-lemma has_derivative_bilinear_at:
-  assumes "(f has_derivative f') (at x)"
-  assumes "(g has_derivative g') (at x)"
-  assumes "bounded_bilinear h"
-  shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x)"
-  using has_derivative_bilinear_within[of f f' x UNIV g g' h] assms by simp
-
 subsection {* Considering derivative @{typ "real \<Rightarrow> 'b\<Colon>real_normed_vector"} as a vector. *}
 
 definition has_vector_derivative :: "(real \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'b \<Rightarrow> (real filter \<Rightarrow> bool)"
diff -r cd05e9fcc63d -r 400ec5ae7f8f src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Apr 09 14:04:41 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Apr 09 14:04:47 2013 +0200
@@ -4405,8 +4405,8 @@
     have "(f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x) has_derivative (\<lambda>x. 0) \<circ> (\<lambda>z. (0 - z *\<^sub>R c) + z *\<^sub>R x)) (at t within {0..1})"
       apply(rule diff_chain_within) apply(rule has_derivative_add)
       unfolding scaleR_simps
-      apply(intro has_derivative_intros)
-      apply(intro has_derivative_intros)
+      apply(intro FDERIV_intros)
+      apply(intro FDERIV_intros)
       apply(rule has_derivative_within_subset,rule assms(6)[rule_format])
       apply(rule *) apply safe apply(rule conv[unfolded scaleR_simps]) using `x\<in>s` `c\<in>s` by auto
     thus "((\<lambda>xa. f ((1 - xa) *\<^sub>R c + xa *\<^sub>R x)) has_derivative (\<lambda>h. 0)) (at t within {0..1})" unfolding o_def .
diff -r cd05e9fcc63d -r 400ec5ae7f8f src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Tue Apr 09 14:04:41 2013 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Tue Apr 09 14:04:47 2013 +0200
@@ -1048,6 +1048,73 @@
 
 end
 
+lemma bounded_linear_ident[simp]: "bounded_linear (\<lambda>x. x)"
+  by default (auto intro!: exI[of _ 1])
+
+lemma bounded_linear_zero[simp]: "bounded_linear (\<lambda>x. 0)"
+  by default (auto intro!: exI[of _ 1])
+
+lemma bounded_linear_add:
+  assumes "bounded_linear f"
+  assumes "bounded_linear g"
+  shows "bounded_linear (\<lambda>x. f x + g x)"
+proof -
+  interpret f: bounded_linear f by fact
+  interpret g: bounded_linear g by fact
+  show ?thesis
+  proof
+    from f.bounded obtain Kf where Kf: "\<And>x. norm (f x) \<le> norm x * Kf" by blast
+    from g.bounded obtain Kg where Kg: "\<And>x. norm (g x) \<le> norm x * Kg" by blast
+    show "\<exists>K. \<forall>x. norm (f x + g x) \<le> norm x * K"
+      using add_mono[OF Kf Kg]
+      by (intro exI[of _ "Kf + Kg"]) (auto simp: field_simps intro: norm_triangle_ineq order_trans)
+  qed (simp_all add: f.add g.add f.scaleR g.scaleR scaleR_right_distrib)
+qed
+
+lemma bounded_linear_minus:
+  assumes "bounded_linear f"
+  shows "bounded_linear (\<lambda>x. - f x)"
+proof -
+  interpret f: bounded_linear f by fact
+  show ?thesis apply (unfold_locales)
+    apply (simp add: f.add)
+    apply (simp add: f.scaleR)
+    apply (simp add: f.bounded)
+    done
+qed
+
+lemma bounded_linear_compose:
+  assumes "bounded_linear f"
+  assumes "bounded_linear g"
+  shows "bounded_linear (\<lambda>x. f (g x))"
+proof -
+  interpret f: bounded_linear f by fact
+  interpret g: bounded_linear g by fact
+  show ?thesis proof (unfold_locales)
+    fix x y show "f (g (x + y)) = f (g x) + f (g y)"
+      by (simp only: f.add g.add)
+  next
+    fix r x show "f (g (scaleR r x)) = scaleR r (f (g x))"
+      by (simp only: f.scaleR g.scaleR)
+  next
+    from f.pos_bounded
+    obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by fast
+    from g.pos_bounded
+    obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by fast
+    show "\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K"
+    proof (intro exI allI)
+      fix x
+      have "norm (f (g x)) \<le> norm (g x) * Kf"
+        using f .
+      also have "\<dots> \<le> (norm x * Kg) * Kf"
+        using g Kf [THEN order_less_imp_le] by (rule mult_right_mono)
+      also have "(norm x * Kg) * Kf = norm x * (Kg * Kf)"
+        by (rule mult_assoc)
+      finally show "norm (f (g x)) \<le> norm x * (Kg * Kf)" .
+    qed
+  qed
+qed
+
 lemma bounded_bilinear_mult:
   "bounded_bilinear (op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)"
 apply (rule bounded_bilinear.intro)
@@ -1069,6 +1136,12 @@
   using bounded_bilinear_mult
   by (rule bounded_bilinear.bounded_linear_right)
 
+lemmas bounded_linear_mult_const =
+  bounded_linear_mult_left [THEN bounded_linear_compose]
+
+lemmas bounded_linear_const_mult =
+  bounded_linear_mult_right [THEN bounded_linear_compose]
+
 lemma bounded_linear_divide:
   "bounded_linear (\<lambda>x::'a::real_normed_field. x / y)"
   unfolding divide_inverse by (rule bounded_linear_mult_left)
@@ -1093,6 +1166,18 @@
 lemma bounded_linear_of_real: "bounded_linear (\<lambda>r. of_real r)"
   unfolding of_real_def by (rule bounded_linear_scaleR_left)
 
+lemma real_bounded_linear:
+  fixes f :: "real \<Rightarrow> real"
+  shows "bounded_linear f \<longleftrightarrow> (\<exists>c::real. f = (\<lambda>x. x * c))"
+proof -
+  { fix x assume "bounded_linear f"
+    then interpret bounded_linear f .
+    from scaleR[of x 1] have "f x = x * f 1"
+      by simp }
+  then show ?thesis
+    by (auto intro: exI[of _ "f 1"] bounded_linear_mult_left)
+qed
+
 instance real_normed_algebra_1 \<subseteq> perfect_space
 proof
   fix x::'a