# HG changeset patch
# User wenzelm
# Date 1395089792 -3600
# Node ID 2666cd7d380cb872c2381650f622db574339f51f
# Parent  f998bdd4076382cd76c318d5d71dc58742f046b7# Parent  01fb1b35433b4f74f8da68c5d6cb33a4532c473a
merged

diff -r 01fb1b35433b -r 2666cd7d380c src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Mon Mar 17 20:54:41 2014 +0100
+++ b/src/HOL/Deriv.thy	Mon Mar 17 21:56:32 2014 +0100
@@ -12,46 +12,64 @@
 imports Limits
 begin
 
+subsection {* Frechet derivative *}
+
 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)
+  (infix "(has'_derivative)" 50)
 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"
+text {*
+  Usually the filter @{term F} is @{term "at x within s"}.  @{term "(f has_derivative D)
+  (at x within s)"} means: @{term D} is the derivative of function @{term f} at point @{term x}
+  within the set @{term s}. Where @{term s} is used to express left or right sided derivatives. In
+  most cases @{term s} is either a variable or @{term UNIV}.
+*}
+
+text {*
+  The following syntax is only used as a legacy syntax.
+*}
+abbreviation (input)
+  FDERIV :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow>  ('a \<Rightarrow> 'b) \<Rightarrow> bool"
+  ("(FDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
+where
+  "FDERIV f x :> f' \<equiv> (f has_derivative f') (at x)"
+
+
+lemma has_derivative_eq_rhs: "(f has_derivative f') F \<Longrightarrow> f' = g' \<Longrightarrow> (f has_derivative g') F"
   by simp
 
 ML {*
 
-structure FDERIV_Intros = Named_Thms
+structure has_derivative_Intros = Named_Thms
 (
-  val name = @{binding FDERIV_intros}
+  val name = @{binding has_derivative_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);
+  has_derivative_Intros.setup #>
+  Global_Theory.add_thms_dynamic (@{binding has_derivative_eq_intros},
+    map_filter (try (fn thm => @{thm has_derivative_eq_rhs} OF [thm])) o has_derivative_Intros.get o Context.proof_of);
 *}
 
-lemma FDERIV_bounded_linear: "(f has_derivative f') F \<Longrightarrow> bounded_linear f'"
+lemma has_derivative_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"
+lemma has_derivative_ident[has_derivative_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"
+lemma has_derivative_const[has_derivative_intros, simp]: "((\<lambda>x. c) has_derivative (\<lambda>x. 0)) F"
   by (simp add: has_derivative_def tendsto_const)
 
 lemma (in bounded_linear) bounded_linear: "bounded_linear f" ..
 
-lemma (in bounded_linear) FDERIV:
+lemma (in bounded_linear) has_derivative:
   "(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
@@ -60,19 +78,19 @@
   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 has_derivative_scaleR_right [has_derivative_intros] =
+  bounded_linear.has_derivative [OF bounded_linear_scaleR_right]
 
-lemmas FDERIV_scaleR_left [FDERIV_intros] =
-  bounded_linear.FDERIV [OF bounded_linear_scaleR_left]
+lemmas has_derivative_scaleR_left [has_derivative_intros] =
+  bounded_linear.has_derivative [OF bounded_linear_scaleR_left]
 
-lemmas FDERIV_mult_right [FDERIV_intros] =
-  bounded_linear.FDERIV [OF bounded_linear_mult_right]
+lemmas has_derivative_mult_right [has_derivative_intros] =
+  bounded_linear.has_derivative [OF bounded_linear_mult_right]
 
-lemmas FDERIV_mult_left [FDERIV_intros] =
-  bounded_linear.FDERIV [OF bounded_linear_mult_left]
+lemmas has_derivative_mult_left [has_derivative_intros] =
+  bounded_linear.has_derivative [OF bounded_linear_mult_left]
 
-lemma FDERIV_add[simp, FDERIV_intros]:
+lemma has_derivative_add[simp, has_derivative_intros]:
   assumes f: "(f has_derivative f') F" and g: "(g has_derivative g') F"
   shows "((\<lambda>x. f x + g x) has_derivative (\<lambda>x. f' x + g' x)) F"
   unfolding has_derivative_def
@@ -83,9 +101,9 @@
     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)
+qed (blast intro: bounded_linear_add f g has_derivative_bounded_linear)
 
-lemma FDERIV_setsum[simp, FDERIV_intros]:
+lemma has_derivative_setsum[simp, has_derivative_intros]:
   assumes f: "\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) F"
   shows "((\<lambda>x. \<Sum>i\<in>I. f i x) has_derivative (\<lambda>x. \<Sum>i\<in>I. f' i x)) F"
 proof cases
@@ -93,47 +111,33 @@
     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_conv_add_uminus FDERIV_add FDERIV_minus)
+lemma has_derivative_minus[simp, has_derivative_intros]: "(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. - f x) has_derivative (\<lambda>x. - f' x)) F"
+  using has_derivative_scaleR_right[of f f' F "-1"] by simp
 
-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)"
+lemma has_derivative_diff[simp, has_derivative_intros]:
+  "(f has_derivative f') F \<Longrightarrow> (g has_derivative g') F \<Longrightarrow> ((\<lambda>x. f x - g x) has_derivative (\<lambda>x. f' x - g' x)) F"
+  by (simp only: diff_conv_add_uminus has_derivative_add has_derivative_minus)
 
-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>
+lemma has_derivative_at_within:
+  "(f has_derivative f') (at x within s) \<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>
+lemma has_derivative_iff_norm:
+  "(f has_derivative f') (at x within s) \<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)
+  by (simp add: has_derivative_at_within 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 has_derivative_at:
+  "(f has_derivative D) (at x) \<longleftrightarrow> (bounded_linear D \<and> (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0)"
+  unfolding has_derivative_iff_norm LIM_offset_zero_iff[of _ _ x] by simp
 
-lemma field_fderiv_def:
+lemma field_has_derivative_at:
   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)
+  shows "(f has_derivative op * D) (at x) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
+  apply (unfold has_derivative_at)
+  apply (simp add: bounded_linear_mult_right)
   apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
   apply (subst diff_divide_distrib)
   apply (subst times_divide_eq_left [symmetric])
@@ -141,17 +145,17 @@
   apply (simp add: tendsto_norm_zero_iff LIM_zero_iff)
   done
 
-lemma FDERIV_I:
+lemma has_derivativeI:
   "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)
+  (f has_derivative f') (at x within s)"
+  by (simp add: has_derivative_at_within)
 
-lemma FDERIV_I_sandwich:
+lemma has_derivativeI_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
+  shows "(f has_derivative f') (at x within s)"
+  unfolding has_derivative_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"])
@@ -161,20 +165,20 @@
   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)
+lemma has_derivative_subset: "(f has_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_derivative f') (at x within t)"
+  by (auto simp add: has_derivative_iff_norm intro: tendsto_within_subset)
 
 subsection {* Continuity *}
 
-lemma FDERIV_continuous:
-  assumes f: "FDERIV f x : s :> f'"
+lemma has_derivative_continuous:
+  assumes f: "(f has_derivative f') (at x within s)"
   shows "continuous (at x within s) f"
 proof -
-  from f interpret F: bounded_linear f' by (rule FDERIV_bounded_linear)
+  from f interpret F: bounded_linear f' by (rule has_derivative_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
+    using f unfolding has_derivative_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)))"
@@ -195,13 +199,13 @@
   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))"
+lemma has_derivative_in_compose:
+  assumes f: "(f has_derivative f') (at x within s)"
+  assumes g: "(g has_derivative g') (at (f x) within (f`s))"
+  shows "((\<lambda>x. g (f x)) has_derivative (\<lambda>x. g' (f' x))) (at x within s)"
 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 interpret F: bounded_linear f' by (rule has_derivative_bounded_linear)
+  from g interpret G: bounded_linear g' by (rule has_derivative_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]
@@ -214,9 +218,9 @@
   def Ng \<equiv> "\<lambda>y. ?N g g' (f x) (f y)"
 
   show ?thesis
-  proof (rule FDERIV_I_sandwich[of 1])
+  proof (rule has_derivativeI_sandwich[of 1])
     show "bounded_linear (\<lambda>x. g' (f' x))"
-      using f g by (blast intro: bounded_linear_compose FDERIV_bounded_linear)
+      using f g by (blast intro: bounded_linear_compose has_derivative_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)"
@@ -237,15 +241,15 @@
     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 ..
+      using f unfolding has_derivative_iff_norm Nf_def ..
     from f have "(f ---> f x) (at x within s)"
-      by (blast intro: FDERIV_continuous continuous_within[THEN iffD1])
+      by (blast intro: has_derivative_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 ..
+      using g unfolding has_derivative_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
 
@@ -256,15 +260,16 @@
   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 has_derivative_compose:
+  "(f has_derivative f') (at x within s) \<Longrightarrow> (g has_derivative g') (at (f x)) \<Longrightarrow>
+  ((\<lambda>x. g (f x)) has_derivative (\<lambda>x. g' (f' x))) (at x within s)"
+  by (blast intro: has_derivative_in_compose has_derivative_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)"
+  assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
+  shows "((\<lambda>x. f x ** g x) has_derivative (\<lambda>h. f x ** g' h + f' h ** g x)) (at x within s)"
 proof -
-  from bounded_linear.bounded [OF FDERIV_bounded_linear [OF f]]
+  from bounded_linear.bounded [OF has_derivative_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:
@@ -278,16 +283,16 @@
   let ?F = "at x within s"
 
   show ?thesis
-  proof (rule FDERIV_I_sandwich[of 1])
+  proof (rule has_derivativeI_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])
+        has_derivative_bounded_linear [OF g] has_derivative_bounded_linear [OF f])
   next
     from g have "(g ---> g x) ?F"
-      by (intro continuous_within[THEN iffD1] FDERIV_continuous)
+      by (intro continuous_within[THEN iffD1] has_derivative_continuous)
     moreover from f g have "(Nf ---> 0) ?F" "(Ng ---> 0) ?F"
-      by (simp_all add: FDERIV_iff_norm Ng_def Nf_def)
+      by (simp_all add: has_derivative_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"
@@ -309,20 +314,20 @@
   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]
+lemmas has_derivative_mult[simp, has_derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_mult]
+lemmas has_derivative_scaleR[simp, has_derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_scaleR]
 
-lemma FDERIV_setprod[simp, FDERIV_intros]:
+lemma has_derivative_setprod[simp, has_derivative_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))"
+  assumes f: "\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) (at x within s)"
+  shows "((\<lambda>x. \<Prod>i\<in>I. f i x) has_derivative (\<lambda>y. \<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {i}. f j x))) (at x within s)"
 proof cases
   assume "finite I" from this f show ?thesis
   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
+    have "((\<lambda>x. f i x * (\<Prod>i\<in>I. f i x)) has_derivative ?P) (at x within s)"
+      using insert by (intro has_derivative_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
@@ -330,18 +335,18 @@
   qed simp  
 qed simp
 
-lemma FDERIV_power[simp, FDERIV_intros]:
+lemma has_derivative_power[simp, has_derivative_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)
+  assumes f: "(f has_derivative f') (at x within s)"
+  shows "((\<lambda>x. f x^n) has_derivative (\<lambda>y. of_nat n * f' y * f x^(n - 1))) (at x within s)"
+  using has_derivative_setprod[OF f, of "{..< n}"] by (simp add: setprod_constant ac_simps)
 
-lemma FDERIV_inverse':
+lemma has_derivative_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)
+  shows "(inverse has_derivative (\<lambda>h. - (inverse x * h * inverse x))) (at x within s)"
+        (is "(?inv has_derivative ?f) _")
+proof (rule has_derivativeI_sandwich)
   show "bounded_linear (\<lambda>h. - (?inv x * h * ?inv x))"
     apply (rule bounded_linear_minus)
     apply (rule bounded_linear_mult_const)
@@ -381,27 +386,27 @@
       norm (?inv y - ?inv x) * norm (?inv x)" .
 qed
 
-lemma FDERIV_inverse[simp, FDERIV_intros]:
+lemma has_derivative_inverse[simp, has_derivative_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] .
+  assumes x:  "f x \<noteq> 0" and f: "(f has_derivative f') (at x within s)"
+  shows "((\<lambda>x. inverse (f x)) has_derivative (\<lambda>h. - (inverse (f x) * f' h * inverse (f x)))) (at x within s)"
+  using has_derivative_compose[OF f has_derivative_inverse', OF x] .
 
-lemma FDERIV_divide[simp, FDERIV_intros]:
+lemma has_derivative_divide[simp, has_derivative_intros]:
   fixes f :: "_ \<Rightarrow> 'a::real_normed_div_algebra"
-  assumes f: "FDERIV f x : s :> f'" and g: "FDERIV g x : s :> g'" 
+  assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)" 
   assumes x: "g x \<noteq> 0"
-  shows "FDERIV (\<lambda>x. f x / g x) x : s :>
-                (\<lambda>h. - f x * (inverse (g x) * g' h * inverse (g x)) + f' h / g x)"
-  using FDERIV_mult[OF f FDERIV_inverse[OF x g]]
+  shows "((\<lambda>x. f x / g x) has_derivative
+                (\<lambda>h. - f x * (inverse (g x) * g' h * inverse (g x)) + f' h / g x)) (at x within s)"
+  using has_derivative_mult[OF f has_derivative_inverse[OF x g]]
   by (simp add: divide_inverse field_simps)
 
 text{*Conventional form requires mult-AC laws. Types real and complex only.*}
-lemma FDERIV_divide'[FDERIV_intros]: 
+
+lemma has_derivative_divide'[has_derivative_intros]: 
   fixes f :: "_ \<Rightarrow> 'a::real_normed_field"
-  assumes f: "FDERIV f x : s :> f'" and g: "FDERIV g x : s :> g'" and x: "g x \<noteq> 0"
-  shows "FDERIV (\<lambda>x. f x / g x) x : s :>
-                (\<lambda>h. (f' h * g x - f x * g' h) / (g x * g x))"
+  assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)" and x: "g x \<noteq> 0"
+  shows "((\<lambda>x. f x / g x) has_derivative (\<lambda>h. (f' h * g x - f x * g' h) / (g x * g x))) (at x within s)"
 proof -
   { fix h
     have "f' h / g x - f x * (inverse (g x) * g' h * inverse (g x)) =
@@ -409,7 +414,7 @@
       by (simp add: divide_inverse field_simps nonzero_inverse_mult_distrib x)
    }
   then show ?thesis
-    using FDERIV_divide [OF f g] x
+    using has_derivative_divide [OF f g] x
     by simp
 qed
 
@@ -417,19 +422,19 @@
 
 text {*
 
-This can not generally shown for @{const FDERIV}, as we need to approach the point from
+This can not generally shown for @{const has_derivative}, 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)"
+lemma has_derivative_zero_unique:
+  assumes "((\<lambda>x. 0) has_derivative F) (at x)" shows "F = (\<lambda>h. 0)"
 proof -
   interpret F: bounded_linear F
-    using assms by (rule FDERIV_bounded_linear)
+    using assms by (rule has_derivative_bounded_linear)
   let ?r = "\<lambda>h. norm (F h) / norm h"
   have *: "?r -- 0 --> 0"
-    using assms unfolding fderiv_def by simp
+    using assms unfolding has_derivative_at by simp
   show "F = (\<lambda>h. 0)"
   proof
     fix h show "F h = 0"
@@ -450,264 +455,286 @@
   qed
 qed
 
-lemma FDERIV_unique:
-  assumes "FDERIV f x :> F" and "FDERIV f x :> F'" shows "F = F'"
+lemma has_derivative_unique:
+  assumes "(f has_derivative F) (at x)" and "(f has_derivative F') (at x)" shows "F = F'"
 proof -
-  have "FDERIV (\<lambda>x. 0) x :> (\<lambda>h. F h - F' h)"
-    using FDERIV_diff [OF assms] by simp
+  have "((\<lambda>x. 0) has_derivative (\<lambda>h. F h - F' h)) (at x)"
+    using has_derivative_diff [OF assms] by simp
   hence "(\<lambda>h. F h - F' h) = (\<lambda>h. 0)"
-    by (rule FDERIV_zero_unique)
+    by (rule has_derivative_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"
+definition
+  differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool"
+  (infix "differentiable" 50)
+where
+  "f differentiable F \<longleftrightarrow> (\<exists>D. (f has_derivative D) 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 (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f differentiable (at x within t)"
+  unfolding differentiable_def by (blast intro: has_derivative_subset)
 
-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]: "(\<lambda>x. x) differentiable F"
+  unfolding differentiable_def by (blast intro: has_derivative_ident)
 
-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_const [simp]: "(\<lambda>z. a) differentiable F"
+  unfolding differentiable_def by (blast intro: has_derivative_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)
+  "f differentiable (at (g x) within (g`s)) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> (\<lambda>x. f (g x)) differentiable (at x within s)"
+  unfolding differentiable_def by (blast intro: has_derivative_in_compose)
 
 lemma differentiable_compose:
-  "f differentiable (g x) \<Longrightarrow> g differentiable x in s \<Longrightarrow> (\<lambda>x. f (g x)) differentiable x in s"
+  "f differentiable (at (g x)) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> (\<lambda>x. f (g x)) differentiable (at x within s)"
   by (blast intro: differentiable_in_compose differentiable_subset)
 
 lemma differentiable_sum [simp]:
-  "isDiff F f \<Longrightarrow> isDiff F g \<Longrightarrow> isDiff F (\<lambda>x. f x + g x)"
-  unfolding isDiff_def by (blast intro: FDERIV_add)
+  "f differentiable F \<Longrightarrow> g differentiable F \<Longrightarrow> (\<lambda>x. f x + g x) differentiable F"
+  unfolding differentiable_def by (blast intro: has_derivative_add)
 
 lemma differentiable_minus [simp]:
-  "isDiff F f \<Longrightarrow> isDiff F (\<lambda>x. - f x)"
-  unfolding isDiff_def by (blast intro: FDERIV_minus)
+  "f differentiable F \<Longrightarrow> (\<lambda>x. - f x) differentiable F"
+  unfolding differentiable_def by (blast intro: has_derivative_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)
+  "f differentiable F \<Longrightarrow> g differentiable F \<Longrightarrow> (\<lambda>x. f x - g x) differentiable F"
+  unfolding differentiable_def by (blast intro: has_derivative_diff)
 
 lemma differentiable_mult [simp]:
   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)
+  shows "f differentiable (at x within s) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> (\<lambda>x. f x * g x) differentiable (at x within s)"
+  unfolding differentiable_def by (blast intro: has_derivative_mult)
 
 lemma differentiable_inverse [simp]:
   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)
+  shows "f differentiable (at x within s) \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> (\<lambda>x. inverse (f x)) differentiable (at x within s)"
+  unfolding differentiable_def by (blast intro: has_derivative_inverse)
 
 lemma differentiable_divide [simp]:
   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"
+  shows "f differentiable (at x within s) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x / g x) differentiable (at x within s)"
   unfolding divide_inverse using assms by simp
 
 lemma differentiable_power [simp]:
   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)
+  shows "f differentiable (at x within s) \<Longrightarrow> (\<lambda>x. f x ^ n) differentiable (at x within s)"
+  unfolding differentiable_def by (blast intro: has_derivative_power)
 
 lemma differentiable_scaleR [simp]:
-  "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)
+  "f differentiable (at x within s) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> (\<lambda>x. f x *\<^sub>R g x) differentiable (at x within s)"
+  unfolding differentiable_def by (blast intro: has_derivative_scaleR)
 
 definition 
-  -- {*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)
+  has_field_derivative :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a filter \<Rightarrow> bool"
+  (infix "(has'_field'_derivative)" 50)
 where
-  deriv_fderiv: "DERIV f x : s :> D = FDERIV f x : s :> (\<lambda>x. x * D)"
+  "(f has_field_derivative D) F \<longleftrightarrow> (f has_derivative op * D) F"
+
+lemma has_derivative_imp_has_field_derivative:
+  "(f has_derivative D) F \<Longrightarrow> (\<And>x. x * D' = D x) \<Longrightarrow> (f has_field_derivative D') F"
+  unfolding has_field_derivative_def 
+  by (rule has_derivative_eq_rhs[of f D]) (simp_all add: fun_eq_iff mult_commute)
+
+lemma has_field_derivative_imp_has_derivative: "(f has_field_derivative D) F \<Longrightarrow> (f has_derivative op * D) F"
+  by (simp add: has_field_derivative_def)
 
-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)
+abbreviation (input)
+  deriv :: "('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"
+  "DERIV f x :> D \<equiv> (f has_field_derivative D) (at x)"
 
-lemma differentiable_def: "(f::real \<Rightarrow> real) differentiable x in s \<longleftrightarrow> (\<exists>D. DERIV f x : s :> D)"
+abbreviation 
+  has_real_derivative :: "(real \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> real filter \<Rightarrow> bool"
+  (infix "(has'_real'_derivative)" 50)
+where
+  "(f has_real_derivative D) F \<equiv> (f has_field_derivative D) F"
+
+lemma real_differentiable_def:
+  "f differentiable at x within s \<longleftrightarrow> (\<exists>D. (f has_real_derivative D) (at x within s))"
 proof safe
-  assume "f differentiable x in s"
-  then obtain f' where *: "FDERIV f x : s :> f'"
-    unfolding isDiff_def by auto
-  then obtain c where "f' = (\<lambda>x. x * c)"
-    by (metis real_bounded_linear FDERIV_bounded_linear)
-  with * show "\<exists>D. DERIV f x : s :> D"
-    unfolding deriv_fderiv by auto
-qed (auto simp: isDiff_def deriv_fderiv)
+  assume "f differentiable at x within s"
+  then obtain f' where *: "(f has_derivative f') (at x within s)"
+    unfolding differentiable_def by auto
+  then obtain c where "f' = (op * c)"
+    by (metis real_bounded_linear has_derivative_bounded_linear mult_commute fun_eq_iff)
+  with * show "\<exists>D. (f has_real_derivative D) (at x within s)"
+    unfolding has_field_derivative_def by auto
+qed (auto simp: differentiable_def has_field_derivative_def)
 
-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 real_differentiableE [elim?]:
+  assumes f: "f differentiable (at x within s)" obtains df where "(f has_real_derivative df) (at x within s)"
+  using assms by (auto simp: real_differentiable_def)
 
-lemma differentiableI: "DERIV f x : s :> D \<Longrightarrow> (f::real \<Rightarrow> real) differentiable x in s"
-  by (force simp add: differentiable_def)
+lemma differentiableD: "f differentiable (at x within s) \<Longrightarrow> \<exists>D. (f has_real_derivative D) (at x within s)"
+  by (auto elim: real_differentiableE)
 
-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 differentiableI: "(f has_real_derivative D) (at x within s) \<Longrightarrow> f differentiable (at x within s)"
+  by (force simp add: real_differentiable_def)
 
 lemma deriv_def:
   "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
-  apply (simp add: deriv_fderiv fderiv_def bounded_linear_mult_left LIM_zero_iff[symmetric, of _ D])
+  apply (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right LIM_zero_iff[symmetric, of _ D])
   apply (subst (2) tendsto_norm_zero_iff[symmetric])
   apply (rule filterlim_cong)
   apply (simp_all add: eventually_at_filter field_simps nonzero_norm_divide)
   done
 
-subsection {* Derivatives *}
+lemma mult_commute_abs: "(\<lambda>x. x * c) = op * (c::'a::ab_semigroup_mult)"
+  by (simp add: fun_eq_iff mult_commute)
 
-lemma DERIV_iff: "(DERIV f x :> D) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
-  by (simp add: deriv_def)
+subsection {* Derivatives *}
 
 lemma DERIV_D: "DERIV f x :> D \<Longrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
   by (simp add: deriv_def)
 
-lemma DERIV_const [simp]: "DERIV (\<lambda>x. k) x : s :> 0"
-  by (rule DERIV_I_FDERIV[OF FDERIV_const]) auto
+lemma DERIV_const [simp]: "((\<lambda>x. k) has_field_derivative 0) (at x within s)"
+  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_const]) auto
+
+lemma DERIV_ident [simp]: "((\<lambda>x. x) has_field_derivative 1) (at x within s)"
+  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_ident]) auto
 
-lemma DERIV_ident [simp]: "DERIV (\<lambda>x. x) x : s :> 1"
-  by (rule DERIV_I_FDERIV[OF FDERIV_ident]) auto
+lemma DERIV_add:
+  "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
+  ((\<lambda>x. f x + g x) has_field_derivative D + E) (at x within s)"
+  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_add])
+     (auto simp: field_simps mult_commute_abs dest: has_field_derivative_imp_has_derivative)
 
-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: "(f has_field_derivative D) (at x within s) \<Longrightarrow> ((\<lambda>x. - f x) has_field_derivative -D) (at x within s)"
+  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_minus]) 
+     (auto simp: field_simps mult_commute_abs dest: has_field_derivative_imp_has_derivative)
 
-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:
+  "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
+  ((\<lambda>x. f x - g x) has_field_derivative D - E) (at x within s)"
+  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_diff])
+     (auto simp: field_simps dest: has_field_derivative_imp_has_derivative)
 
-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: "DERIV f x : s :> D \<Longrightarrow> DERIV g x : s :> E \<Longrightarrow> DERIV (\<lambda>x. f x + - g x) x : s :> D + - E"
+lemma DERIV_add_minus:
+  "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
+  ((\<lambda>x. f x + - g x) has_field_derivative D + - E) (at x within s)"
   by (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_continuous: "(f has_field_derivative D) (at x within s) \<Longrightarrow> continuous (at x within s) f"
+  by (drule has_derivative_continuous[OF has_field_derivative_imp_has_derivative]) simp
 
 lemma DERIV_isCont: "DERIV f x :> D \<Longrightarrow> isCont f x"
   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':
+  "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
+  ((\<lambda>x. f x * g x) has_field_derivative f x * E + D * g x) (at x within s)"
+  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_mult])
+     (auto simp: field_simps mult_commute_abs dest: has_field_derivative_imp_has_derivative)
 
-lemma DERIV_mult: "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)
+lemma DERIV_mult:
+  "(f has_field_derivative Da) (at x within s) \<Longrightarrow> (g has_field_derivative Db) (at x within s) \<Longrightarrow>
+  ((\<lambda>x. f x * g x) has_field_derivative Da * g x + Db * f x) (at x within s)"
+  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_mult])
+     (auto simp: field_simps dest: has_field_derivative_imp_has_derivative)
 
 text {* Derivative of linear multiplication *}
 
 lemma DERIV_cmult:
-  "DERIV f x : s :> D ==> DERIV (%x. c * f x) x : s :> c*D"
+  "(f has_field_derivative D) (at x within s) ==> ((\<lambda>x. c * f x) has_field_derivative c * D) (at x within s)"
   by (drule DERIV_mult' [OF DERIV_const], simp)
 
 lemma DERIV_cmult_right:
-  "DERIV f x : s :> D ==> DERIV (%x. f x * c) x : s :> D * c"
+  "(f has_field_derivative D) (at x within s) ==> ((\<lambda>x. f x * c) has_field_derivative D * c) (at x within s)"
   using DERIV_cmult   by (force simp add: mult_ac)
 
-lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x : s :> c"
+lemma DERIV_cmult_Id [simp]: "(op * c has_field_derivative c) (at x within s)"
   by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp)
 
-lemma DERIV_cdivide: "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_cdivide:
+  "(f has_field_derivative D) (at x within s) \<Longrightarrow> ((\<lambda>x. f x / c) has_field_derivative D / c) (at x within s)"
+  using DERIV_cmult_right[of f D x s "1 / c"] by simp
 
 lemma DERIV_unique:
   "DERIV f x :> D \<Longrightarrow> DERIV f x :> E \<Longrightarrow> D = E"
   unfolding deriv_def by (rule LIM_unique) 
 
-lemma DERIV_setsum':
-  "(\<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:
-  "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)
+  "(\<And> n. n \<in> S \<Longrightarrow> ((\<lambda>x. f x n) has_field_derivative (f' x n)) F) \<Longrightarrow> 
+    ((\<lambda>x. setsum (f x) S) has_field_derivative setsum (f' x) S) F"
+  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_setsum])
+     (auto simp: setsum_right_distrib mult_commute_abs dest: has_field_derivative_imp_has_derivative)
 
 lemma DERIV_inverse':
-  "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)
+  "(f has_field_derivative D) (at x within s) \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow>
+  ((\<lambda>x. inverse (f x)) has_field_derivative - (inverse (f x) * D * inverse (f x))) (at x within s)"
+  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_inverse])
+     (auto dest: has_field_derivative_imp_has_derivative)
 
 text {* Power of @{text "-1"} *}
 
 lemma DERIV_inverse:
-  "x \<noteq> 0 \<Longrightarrow> DERIV (\<lambda>x. inverse(x)) x : s :> - (inverse x ^ Suc (Suc 0))"
+  "x \<noteq> 0 \<Longrightarrow> ((\<lambda>x. inverse(x)) has_field_derivative - (inverse x ^ Suc (Suc 0))) (at x within s)"
   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))))"
+  "(f has_field_derivative d) (at x within s) \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow>
+  ((\<lambda>x. inverse (f x)) has_field_derivative (- (d * inverse(f x ^ Suc (Suc 0))))) (at x within s)"
   by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib)
 
 text {* Derivative of quotient *}
 
 lemma DERIV_divide:
-  "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)
+  "(f has_field_derivative D) (at x within s) \<Longrightarrow>
+  (g has_field_derivative E) (at x within s) \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow>
+  ((\<lambda>x. f x / g x) has_field_derivative (D * g x - f x * E) / (g x * g x)) (at x within s)"
+  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_divide])
+     (auto dest: has_field_derivative_imp_has_derivative simp: field_simps nonzero_inverse_mult_distrib divide_inverse)
 
 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))"
+  "(f has_field_derivative d) (at x within s) \<Longrightarrow>
+  (g has_field_derivative e) (at x within s)\<Longrightarrow> g x \<noteq> 0 \<Longrightarrow> 
+  ((\<lambda>y. f y / g y) has_field_derivative (d * g x - (e * f x)) / (g x ^ Suc (Suc 0))) (at x within s)"
   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)
+  "(f has_field_derivative D) (at x within s) \<Longrightarrow>
+  ((\<lambda>x. f x ^ Suc n) has_field_derivative (1 + of_nat n) * (D * f x ^ n)) (at x within s)"
+  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_power])
+     (auto simp: has_field_derivative_def)
 
 lemma DERIV_power:
-  "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)
+  "(f has_field_derivative D) (at x within s) \<Longrightarrow>
+  ((\<lambda>x. f x ^ n) has_field_derivative of_nat n * (D * f x ^ (n - Suc 0))) (at x within s)"
+  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_power])
+     (auto simp: has_field_derivative_def)
 
-lemma DERIV_pow: "DERIV (%x. x ^ n) x : s :> real n * (x ^ (n - Suc 0))"
+lemma DERIV_pow: "((\<lambda>x. x ^ n) has_field_derivative real n * (x ^ (n - Suc 0))) (at x within s)"
   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)
+lemma DERIV_chain': "(f has_field_derivative D) (at x within s) \<Longrightarrow> DERIV g (f x) :> E \<Longrightarrow> 
+  ((\<lambda>x. g (f x)) has_field_derivative E * D) (at x within s)"
+  using has_derivative_compose[of f "op * D" x s g "op * E"]
+  unfolding has_field_derivative_def mult_commute_abs ac_simps .
 
-corollary DERIV_chain2: "DERIV f (g x) :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (%x. f (g x)) x : s :> Da * Db"
+corollary DERIV_chain2: "DERIV f (g x) :> Da \<Longrightarrow> (g has_field_derivative Db) (at x within s) \<Longrightarrow>
+  ((\<lambda>x. f (g x)) has_field_derivative Da * Db) (at x within s)"
   by (rule DERIV_chain')
 
 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"
+lemma DERIV_chain:
+  "DERIV f (g x) :> Da \<Longrightarrow> (g has_field_derivative Db) (at x within s) \<Longrightarrow> 
+  (f o g has_field_derivative Da * Db) (at x within s)"
   by (drule (1) DERIV_chain', simp add: o_def mult_commute)
 
 lemma DERIV_image_chain: 
-  "DERIV f (g x) : (g ` s) :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (f o g) x : s :> Da * Db"
-  using FDERIV_in_compose [of g "\<lambda>x. x * Db" x s f "\<lambda>x. x * Da "]
-  by (simp add: deriv_fderiv o_def  mult_ac)
+  "(f has_field_derivative Da) (at (g x) within (g ` s)) \<Longrightarrow> (g has_field_derivative Db) (at x within s) \<Longrightarrow>
+  (f o g has_field_derivative Da * Db) (at x within s)"
+  using has_derivative_in_compose [of g "op * Db" x s f "op * Da "]
+  by (simp add: has_field_derivative_def o_def mult_commute_abs ac_simps)
 
 (*These two are from HOL Light: HAS_COMPLEX_DERIVATIVE_CHAIN*)
 lemma DERIV_chain_s:
@@ -736,7 +763,7 @@
 
 setup Deriv_Intros.setup
 
-lemma DERIV_cong: "DERIV f x : s :> X \<Longrightarrow> X = Y \<Longrightarrow> DERIV f x : s :> Y"
+lemma DERIV_cong: "(f has_field_derivative X) (at x within s) \<Longrightarrow> X = Y \<Longrightarrow> (f has_field_derivative Y) (at x within s)"
   by simp
 
 declare
@@ -781,7 +808,7 @@
 
 lemma DERIV_shift:
   "(DERIV f (x + z) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (x + z)) x :> y)"
-  by (simp add: DERIV_iff field_simps)
+  by (simp add: deriv_def field_simps)
 
 lemma DERIV_mirror:
   "(DERIV f (- x) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (- x::real) :: real) x :> - y)"
@@ -800,7 +827,7 @@
     let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
     show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
     show "isCont ?g x" using der
-      by (simp add: isCont_iff DERIV_iff cong: LIM_equal [rule_format])
+      by (simp add: isCont_iff deriv_def cong: LIM_equal [rule_format])
     show "?g x = l" by simp
   qed
 next
@@ -808,7 +835,7 @@
   then obtain g where
     "(\<forall>z. f z - f x = g z * (z-x))" and "isCont g x" and "g x = l" by blast
   thus "(DERIV f x :> l)"
-     by (auto simp add: isCont_iff DERIV_iff cong: LIM_cong)
+     by (auto simp add: isCont_iff deriv_def cong: LIM_cong)
 qed
 
 text {*
@@ -881,14 +908,14 @@
 lemma DERIV_pos_inc_left:
   fixes f :: "real => real"
   shows "DERIV f x :> l \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d --> f(x - h) < f(x)"
-  apply (rule DERIV_neg_dec_left [of "%x. - f x" x "-l", simplified])
+  apply (rule DERIV_neg_dec_left [of "%x. - f x" "-l" x, simplified])
   apply (auto simp add: DERIV_minus)
   done
 
 lemma DERIV_neg_dec_right:
   fixes f :: "real => real"
   shows "DERIV f x :> l \<Longrightarrow> l < 0 \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d --> f(x) > f(x + h)"
-  apply (rule DERIV_pos_inc_right [of "%x. - f x" x "-l", simplified])
+  apply (rule DERIV_pos_inc_right [of "%x. - f x" "-l" x, simplified])
   apply (auto simp add: DERIV_minus)
   done
 
@@ -963,7 +990,7 @@
   assumes lt: "a < b"
       and eq: "f(a) = f(b)"
       and con: "\<forall>x. a \<le> x & x \<le> b --> isCont f x"
-      and dif [rule_format]: "\<forall>x. a < x & x < b --> f differentiable x"
+      and dif [rule_format]: "\<forall>x. a < x & x < b --> f differentiable (at x)"
   shows "\<exists>z::real. a < z & z < b & DERIV f z :> 0"
 proof -
   have le: "a \<le> b" using lt by simp
@@ -1055,20 +1082,20 @@
 theorem MVT:
   assumes lt:  "a < b"
       and con: "\<forall>x. a \<le> x & x \<le> b --> isCont f x"
-      and dif [rule_format]: "\<forall>x. a < x & x < b --> f differentiable x"
+      and dif [rule_format]: "\<forall>x. a < x & x < b --> f differentiable (at x)"
   shows "\<exists>l z::real. a < z & z < b & DERIV f z :> l &
                    (f(b) - f(a) = (b-a) * l)"
 proof -
   let ?F = "%x. f x - ((f b - f a) / (b-a)) * x"
   have contF: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?F x"
     using con by (fast intro: isCont_intros)
-  have difF: "\<forall>x. a < x \<and> x < b \<longrightarrow> ?F differentiable x"
+  have difF: "\<forall>x. a < x \<and> x < b \<longrightarrow> ?F differentiable (at x)"
   proof (clarify)
     fix x::real
     assume ax: "a < x" and xb: "x < b"
     from differentiableD [OF dif [OF conjI [OF ax xb]]]
     obtain l where der: "DERIV f x :> l" ..
-    show "?F differentiable x"
+    show "?F differentiable (at x)"
       by (rule differentiableI [where D = "l - (f b - f a)/(b-a)"],
           blast intro: DERIV_diff DERIV_cmult_Id der)
   qed
@@ -1094,7 +1121,7 @@
       ==> \<exists>z::real. a < z & z < b & (f b - f a = (b - a) * f'(z))"
 apply (drule MVT)
 apply (blast intro: DERIV_isCont)
-apply (force dest: order_less_imp_le simp add: differentiable_def)
+apply (force dest: order_less_imp_le simp add: real_differentiable_def)
 apply (blast dest: DERIV_unique order_less_imp_le)
 done
 
@@ -1169,7 +1196,7 @@
   shows "[|a \<noteq> b; \<forall>x. DERIV f x :> k |] ==> (f(b) - f(a)) = (b-a) * k"
 apply (rule linorder_cases [of a b], auto)
 apply (drule_tac [!] f = f in MVT)
-apply (auto dest: DERIV_isCont DERIV_unique simp add: differentiable_def)
+apply (auto dest: DERIV_isCont DERIV_unique simp add: real_differentiable_def)
 apply (auto dest: DERIV_unique simp add: ring_distribs)
 done
 
@@ -1355,9 +1382,9 @@
   fixes a b :: real
   assumes alb: "a < b"
     and fc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"
-    and fd: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable x"
+    and fd: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable (at x)"
     and gc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont g x"
-    and gd: "\<forall>x. a < x \<and> x < b \<longrightarrow> g differentiable x"
+    and gd: "\<forall>x. a < x \<and> x < b \<longrightarrow> g differentiable (at x)"
   shows "\<exists>g'c f'c c.
     DERIV g c :> g'c \<and> DERIV f c :> f'c \<and> a < c \<and> c < b \<and> ((f b - f a) * g'c) = ((g b - g a) * f'c)"
 proof -
@@ -1365,19 +1392,19 @@
   from assms have "a < b" by simp
   moreover have "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?h x"
     using fc gc by simp
-  moreover have "\<forall>x. a < x \<and> x < b \<longrightarrow> ?h differentiable x"
+  moreover have "\<forall>x. a < x \<and> x < b \<longrightarrow> ?h differentiable (at x)"
     using fd gd by simp
   ultimately have "\<exists>l z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" by (rule MVT)
   then obtain l where ldef: "\<exists>z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" ..
   then obtain c where cdef: "a < c \<and> c < b \<and> DERIV ?h c :> l \<and> ?h b - ?h a = (b - a) * l" ..
 
   from cdef have cint: "a < c \<and> c < b" by auto
-  with gd have "g differentiable c" by simp
+  with gd have "g differentiable (at c)" by simp
   hence "\<exists>D. DERIV g c :> D" by (rule differentiableD)
   then obtain g'c where g'cdef: "DERIV g c :> g'c" ..
 
   from cdef have "a < c \<and> c < b" by auto
-  with fd have "f differentiable c" by simp
+  with fd have "f differentiable (at c)" by simp
   hence "\<exists>D. DERIV f c :> D" by (rule differentiableD)
   then obtain f'c where f'cdef: "DERIV f c :> f'c" ..
 
@@ -1418,7 +1445,7 @@
 proof -
   have "\<exists>g'c f'c c. DERIV g c :> g'c \<and> DERIV f c :> f'c \<and>
     a < c \<and> c < b \<and> (f b - f a) * g'c = (g b - g a) * f'c"
-    using assms by (intro GMVT) (force simp: differentiable_def)+
+    using assms by (intro GMVT) (force simp: real_differentiable_def)+
   then obtain c where "a < c" "c < b" "(f b - f a) * g' c = (g b - g a) * f' c"
     using DERIV_f DERIV_g by (force dest: DERIV_unique)
   then show ?thesis
diff -r 01fb1b35433b -r 2666cd7d380c src/HOL/Library/Inner_Product.thy
--- a/src/HOL/Library/Inner_Product.thy	Mon Mar 17 20:54:41 2014 +0100
+++ b/src/HOL/Library/Inner_Product.thy	Mon Mar 17 21:56:32 2014 +0100
@@ -180,7 +180,7 @@
 lemmas isCont_inner [simp] =
   bounded_bilinear.isCont [OF bounded_bilinear_inner]
 
-lemmas FDERIV_inner [FDERIV_intros] =
+lemmas has_derivative_inner [has_derivative_intros] =
   bounded_bilinear.FDERIV [OF bounded_bilinear_inner]
 
 lemmas bounded_linear_inner_left =
@@ -189,15 +189,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 has_derivative_inner_right [has_derivative_intros] =
+  bounded_linear.has_derivative [OF bounded_linear_inner_right]
 
-lemmas FDERIV_inner_left [FDERIV_intros] =
-  bounded_linear.FDERIV [OF bounded_linear_inner_left]
+lemmas has_derivative_inner_left [has_derivative_intros] =
+  bounded_linear.has_derivative [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)
+  "f differentiable (at x within s) \<Longrightarrow> g differentiable at x within s \<Longrightarrow> (\<lambda>x. inner (f x) (g x)) differentiable at x within s"
+  unfolding differentiable_def by (blast intro: has_derivative_inner)
 
 subsection {* Class instances *}
 
@@ -273,46 +273,46 @@
   "GDERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. inner h D)"
 
 lemma gderiv_deriv [simp]: "GDERIV f x :> D \<longleftrightarrow> DERIV f x :> D"
-  by (simp only: gderiv_def deriv_fderiv inner_real_def)
+  by (simp only: gderiv_def has_field_derivative_def inner_real_def mult_commute_abs)
 
 lemma GDERIV_DERIV_compose:
     "\<lbrakk>GDERIV f x :> df; DERIV g (f x) :> dg\<rbrakk>
      \<Longrightarrow> GDERIV (\<lambda>x. g (f x)) x :> scaleR dg df"
-  unfolding gderiv_def deriv_fderiv
-  apply (drule (1) FDERIV_compose)
+  unfolding gderiv_def has_field_derivative_def
+  apply (drule (1) has_derivative_compose)
   apply (simp add: mult_ac)
   done
 
-lemma FDERIV_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d"
+lemma has_derivative_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d"
   by simp
 
 lemma GDERIV_subst: "\<lbrakk>GDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> GDERIV f x :> d"
   by simp
 
 lemma GDERIV_const: "GDERIV (\<lambda>x. k) x :> 0"
-  unfolding gderiv_def inner_zero_right by (rule FDERIV_const)
+  unfolding gderiv_def inner_zero_right by (rule has_derivative_const)
 
 lemma GDERIV_add:
     "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
      \<Longrightarrow> GDERIV (\<lambda>x. f x + g x) x :> df + dg"
-  unfolding gderiv_def inner_add_right by (rule FDERIV_add)
+  unfolding gderiv_def inner_add_right by (rule has_derivative_add)
 
 lemma GDERIV_minus:
     "GDERIV f x :> df \<Longrightarrow> GDERIV (\<lambda>x. - f x) x :> - df"
-  unfolding gderiv_def inner_minus_right by (rule FDERIV_minus)
+  unfolding gderiv_def inner_minus_right by (rule has_derivative_minus)
 
 lemma GDERIV_diff:
     "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
      \<Longrightarrow> GDERIV (\<lambda>x. f x - g x) x :> df - dg"
-  unfolding gderiv_def inner_diff_right by (rule FDERIV_diff)
+  unfolding gderiv_def inner_diff_right by (rule has_derivative_diff)
 
 lemma GDERIV_scaleR:
     "\<lbrakk>DERIV f x :> df; GDERIV g x :> dg\<rbrakk>
      \<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x
       :> (scaleR (f x) dg + scaleR df (g x))"
-  unfolding gderiv_def deriv_fderiv inner_add_right inner_scaleR_right
-  apply (rule FDERIV_subst)
-  apply (erule (1) FDERIV_scaleR)
+  unfolding gderiv_def has_field_derivative_def inner_add_right inner_scaleR_right
+  apply (rule has_derivative_subst)
+  apply (erule (1) has_derivative_scaleR)
   apply (simp add: mult_ac)
   done
 
@@ -320,8 +320,8 @@
     "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
      \<Longrightarrow> GDERIV (\<lambda>x. f x * g x) x :> scaleR (f x) dg + scaleR (g x) df"
   unfolding gderiv_def
-  apply (rule FDERIV_subst)
-  apply (erule (1) FDERIV_mult)
+  apply (rule has_derivative_subst)
+  apply (erule (1) has_derivative_mult)
   apply (simp add: inner_add mult_ac)
   done
 
@@ -336,7 +336,7 @@
   assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x"
 proof -
   have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
-    by (intro FDERIV_inner FDERIV_ident)
+    by (intro has_derivative_inner has_derivative_ident)
   have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
     by (simp add: fun_eq_iff inner_commute)
   have "0 < inner x x" using `x \<noteq> 0` by simp
@@ -349,12 +349,12 @@
     apply (rule GDERIV_subst [OF _ 4])
     apply (rule GDERIV_DERIV_compose [where g=sqrt and df="scaleR 2 x"])
     apply (subst gderiv_def)
-    apply (rule FDERIV_subst [OF _ 2])
+    apply (rule has_derivative_subst [OF _ 2])
     apply (rule 1)
     apply (rule 3)
     done
 qed
 
-lemmas FDERIV_norm = GDERIV_norm [unfolded gderiv_def]
+lemmas has_derivative_norm = GDERIV_norm [unfolded gderiv_def]
 
 end
diff -r 01fb1b35433b -r 2666cd7d380c src/HOL/Library/Poly_Deriv.thy
--- a/src/HOL/Library/Poly_Deriv.thy	Mon Mar 17 20:54:41 2014 +0100
+++ b/src/HOL/Library/Poly_Deriv.thy	Mon Mar 17 21:56:32 2014 +0100
@@ -106,8 +106,8 @@
 
 text{* Consequences of the derivative theorem above*}
 
-lemma poly_differentiable[simp]: "(%x. poly p x) differentiable (x::real)"
-apply (simp add: differentiable_def)
+lemma poly_differentiable[simp]: "(%x. poly p x) differentiable (at x::real filter)"
+apply (simp add: real_differentiable_def)
 apply (blast intro: poly_DERIV)
 done
 
diff -r 01fb1b35433b -r 2666cd7d380c src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Mon Mar 17 20:54:41 2014 +0100
+++ b/src/HOL/Library/Product_Vector.thy	Mon Mar 17 21:56:32 2014 +0100
@@ -478,18 +478,18 @@
 
 subsubsection {* Frechet derivatives involving pairs *}
 
-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])
+lemma has_derivative_Pair [has_derivative_intros]:
+  assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
+  shows "((\<lambda>x. (f x, g x)) has_derivative (\<lambda>h. (f' h, g' h))) (at x within s)"
+proof (rule has_derivativeI_sandwich[of 1])
   show "bounded_linear (\<lambda>h. (f' h, g' h))"
-    using f g by (intro bounded_linear_Pair FDERIV_bounded_linear)
+    using f g by (intro bounded_linear_Pair has_derivative_bounded_linear)
   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)
+    using f g by (intro tendsto_add_zero) (auto simp: has_derivative_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)"
@@ -497,10 +497,10 @@
     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]
+lemmas has_derivative_fst [has_derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_fst]
+lemmas has_derivative_snd [has_derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_snd]
 
-lemma FDERIV_split [FDERIV_intros]:
+lemma has_derivative_split [has_derivative_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' .
 
diff -r 01fb1b35433b -r 2666cd7d380c src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Mon Mar 17 20:54:41 2014 +0100
+++ b/src/HOL/MacLaurin.thy	Mon Mar 17 21:56:32 2014 +0100
@@ -116,7 +116,7 @@
     by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp
 
   have differentiable_difg:
-    "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> difg m differentiable x"
+    "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> difg m differentiable (at x)"
     by (rule differentiableI [OF difg_Suc [rule_format]]) simp
 
   have difg_Suc_eq_0: "\<And>m t. \<lbrakk>m < n; 0 \<le> t; t \<le> h; DERIV (difg m) t :> 0\<rbrakk>
@@ -135,7 +135,7 @@
       show "difg 0 0 = difg 0 h" by (simp add: difg_0 g2)
       show "\<forall>x. 0 \<le> x \<and> x \<le> h \<longrightarrow> isCont (difg (0\<Colon>nat)) x"
         by (simp add: isCont_difg n)
-      show "\<forall>x. 0 < x \<and> x < h \<longrightarrow> difg (0\<Colon>nat) differentiable x"
+      show "\<forall>x. 0 < x \<and> x < h \<longrightarrow> difg (0\<Colon>nat) differentiable (at x)"
         by (simp add: differentiable_difg n)
     qed
   next
@@ -149,7 +149,7 @@
         using t `Suc m' < n` by (simp add: difg_Suc_eq_0 difg_eq_0)
       show "\<forall>x. 0 \<le> x \<and> x \<le> t \<longrightarrow> isCont (difg (Suc m')) x"
         using `t < h` `Suc m' < n` by (simp add: isCont_difg)
-      show "\<forall>x. 0 < x \<and> x < t \<longrightarrow> difg (Suc m') differentiable x"
+      show "\<forall>x. 0 < x \<and> x < t \<longrightarrow> difg (Suc m') differentiable (at x)"
         using `t < h` `Suc m' < n` by (simp add: differentiable_difg)
     qed
     thus ?case
diff -r 01fb1b35433b -r 2666cd7d380c src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Mar 17 20:54:41 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Mar 17 21:56:32 2014 +0100
@@ -43,30 +43,26 @@
 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') \<longleftrightarrow> (f has_derivative op * f') (at x)"
-  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
+lemmas has_derivative_id = has_derivative_ident
+lemmas has_derivative_const = has_derivative_const
+lemmas has_derivative_neg = has_derivative_minus
+lemmas has_derivative_add = has_derivative_add
+lemmas has_derivative_sub = has_derivative_diff
+lemmas has_derivative_setsum = has_derivative_setsum
+lemmas scaleR_right_has_derivative = has_derivative_scaleR_right
+lemmas scaleR_left_has_derivative = has_derivative_scaleR_left
+lemmas inner_right_has_derivative = has_derivative_inner_right
+lemmas inner_left_has_derivative = has_derivative_inner_left
+lemmas mult_right_has_derivative = has_derivative_mult_right
+lemmas mult_left_has_derivative = has_derivative_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
+  by (intro has_derivative_eq_intros) auto
 
 
 subsection {* Derivative with composed bilinear function. *}
@@ -145,30 +141,30 @@
 subsubsection {*Caratheodory characterization*}
 
 lemma DERIV_within_iff:
-  "(DERIV f a : s :> D) \<longleftrightarrow> ((\<lambda>z. (f z - f a) / (z - a)) ---> D) (at a within s)"
+  "(f has_field_derivative D) (at a within s) \<longleftrightarrow> ((\<lambda>z. (f z - f a) / (z - a)) ---> D) (at a within s)"
 proof -
   have 1: "\<And>w y. ~(w = a) ==> y / (w - a) - D = (y - (w - a)*D)/(w - a)"
     by (metis divide_diff_eq_iff eq_iff_diff_eq_0)
   show ?thesis
-    apply (simp add: deriv_fderiv has_derivative_within bounded_linear_mult_left)
+    apply (simp add: has_field_derivative_def has_derivative_within bounded_linear_mult_right)
     apply (simp add: LIM_zero_iff [where l = D, symmetric])
     apply (simp add: Lim_within dist_norm)
     apply (simp add: nonzero_norm_divide [symmetric])
-    apply (simp add: 1 diff_add_eq_diff_diff)
+    apply (simp add: 1 diff_add_eq_diff_diff ac_simps)
     done
 qed
 
 lemma DERIV_caratheodory_within:
-  "(DERIV f x : s :> l) \<longleftrightarrow> 
+  "(f has_field_derivative l) (at x within s) \<longleftrightarrow> 
    (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> continuous (at x within s) g \<and> g x = l)"
       (is "?lhs = ?rhs")
 proof
-  assume der: "DERIV f x : s :> l"
+  assume ?lhs
   show ?rhs
   proof (intro exI conjI)
     let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
     show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
-    show "continuous (at x within s) ?g" using der
+    show "continuous (at x within s) ?g" using `?lhs`
       by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
     show "?g x = l" by simp
   qed
@@ -176,7 +172,7 @@
   assume ?rhs
   then obtain g where
     "(\<forall>z. f z - f x = g z * (z-x))" and "continuous (at x within s) g" and "g x = l" by blast
-  thus "(DERIV f x : s :> l)"
+  thus ?lhs
     by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
 qed
 
@@ -221,20 +217,11 @@
 
 subsection {* Differentiability *}
 
-no_notation Deriv.differentiable (infixl "differentiable" 60)
-
-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)
+    (infix "differentiable'_on" 50)
   where "f differentiable_on s \<longleftrightarrow> (\<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
@@ -286,7 +273,7 @@
   unfolding frechet_derivative_def differentiable_def
   unfolding some_eq_ex[of "\<lambda> f' . (f has_derivative f') net"] ..
 
-lemma linear_frechet_derivative: "f differentiable net \<Longrightarrow> linear(frechet_derivative f net)"
+lemma linear_frechet_derivative: "f differentiable net \<Longrightarrow> linear (frechet_derivative f net)"
   unfolding frechet_derivative_works has_derivative_def
   by (auto intro: bounded_linear_imp_linear)
 
@@ -295,7 +282,7 @@
 
 lemma differentiable_imp_continuous_within:
   "f differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
-  by (auto simp: differentiable_def intro: FDERIV_continuous)
+  by (auto simp: differentiable_def intro: has_derivative_continuous)
 
 lemma differentiable_imp_continuous_on:
   "f differentiable_on s \<Longrightarrow> continuous_on s f"
@@ -361,17 +348,17 @@
 
 subsection {* The chain rule *}
 
-lemma diff_chain_within[FDERIV_intros]:
+lemma diff_chain_within[has_derivative_intros]:
   assumes "(f has_derivative f') (at x within s)"
     and "(g has_derivative g') (at (f x) within (f ` s))"
   shows "((g \<circ> f) has_derivative (g' \<circ> f'))(at x within s)"
-  using FDERIV_in_compose[OF assms]
+  using has_derivative_in_compose[OF assms]
   by (simp add: comp_def)
 
-lemma diff_chain_at[FDERIV_intros]:
+lemma diff_chain_at[has_derivative_intros]:
   "(f has_derivative f') (at x) \<Longrightarrow>
     (g has_derivative g') (at (f x)) \<Longrightarrow> ((g \<circ> f) has_derivative (g' \<circ> f')) (at x)"
-  using FDERIV_compose[of f f' x UNIV g g']
+  using has_derivative_compose[of f f' x UNIV g g']
   by (simp add: comp_def)
 
 
@@ -468,7 +455,7 @@
 
 lemma frechet_derivative_unique_at:
   "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f'') (at x) \<Longrightarrow> f' = f''"
-  by (rule FDERIV_unique)
+  by (rule has_derivative_unique)
 
 lemma frechet_derivative_unique_within_closed_interval:
   fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
@@ -580,18 +567,18 @@
 proof
   fix h :: 'a
   interpret f': bounded_linear f'
-    using deriv by (rule FDERIV_bounded_linear)
+    using deriv by (rule has_derivative_bounded_linear)
   show "f' h = 0"
   proof (cases "h = 0")
     assume "h \<noteq> 0"
     from min obtain d where d1: "0 < d" and d2: "\<forall>y\<in>ball x d. f x \<le> f y"
       unfolding eventually_at by (force simp: dist_commute)
     have "FDERIV (\<lambda>r. x + r *\<^sub>R h) 0 :> (\<lambda>r. r *\<^sub>R h)"
-      by (intro FDERIV_eq_intros, auto)
+      by (intro has_derivative_eq_intros, auto)
     then have "FDERIV (\<lambda>r. f (x + r *\<^sub>R h)) 0 :> (\<lambda>k. f' (k *\<^sub>R h))"
-      by (rule FDERIV_compose, simp add: deriv)
+      by (rule has_derivative_compose, simp add: deriv)
     then have "DERIV (\<lambda>r. f (x + r *\<^sub>R h)) 0 :> f' h"
-      unfolding deriv_fderiv by (simp add: f'.scaleR)
+      unfolding has_field_derivative_def by (simp add: f'.scaleR mult_commute_abs)
     moreover have "0 < d / norm h"
       using d1 and `h \<noteq> 0` by (simp add: divide_pos_pos)
     moreover have "\<forall>y. \<bar>0 - y\<bar> < d / norm h \<longrightarrow> f (x + 0 *\<^sub>R h) \<le> f (x + y *\<^sub>R h)"
@@ -643,7 +630,7 @@
   moreover have "open (ball x e)" by simp
   moreover have "((\<lambda>x. f x \<bullet> k) has_derivative (\<lambda>h. ?f' h \<bullet> k)) (at x)"
     using bounded_linear_inner_left diff[unfolded frechet_derivative_works]
-    by (rule bounded_linear.FDERIV)
+    by (rule bounded_linear.has_derivative)
   ultimately have "(\<lambda>h. frechet_derivative f (at x) h \<bullet> k) = (\<lambda>v. 0)"
     using ball(2) by (rule differential_zero_maxmin)
   then show ?thesis
@@ -719,7 +706,7 @@
     assume "x \<in> box a b" hence x: "x \<in> {a<..<b}" by (simp add: box_real)
     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 FDERIV_intros assms(3)[rule_format,OF x] mult_right_has_derivative)
+      by (intro has_derivative_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 obtain x where
     "x \<in> box a b"
@@ -789,7 +776,7 @@
     apply (rule assms(1))
     apply (rule continuous_on_inner continuous_on_intros assms(2) ballI)+
     unfolding o_def
-    apply (rule FDERIV_inner_right)
+    apply (rule has_derivative_inner_right)
     using assms(3)
     apply auto
     done
@@ -857,7 +844,7 @@
     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 FDERIV_intros)+
+      apply (rule has_derivative_intros)+
       apply (rule has_derivative_within_subset)
       apply (rule assms(2)[rule_format])
       using goal1 *
@@ -1585,13 +1572,13 @@
         show "(ph has_derivative (\<lambda>v. v - g' (f' u v))) (at u within ball a d)"
           unfolding ph' *
           apply (simp add: comp_def)
-          apply (rule bounded_linear.FDERIV[OF assms(3)])
-          apply (rule FDERIV_intros)
+          apply (rule bounded_linear.has_derivative[OF assms(3)])
+          apply (rule has_derivative_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`
-          apply (auto intro!: FDERIV_intros bounded_linear.FDERIV[of _ "\<lambda>x. x"] derivative_linear)
+          apply (auto intro!: has_derivative_intros bounded_linear.has_derivative[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)
@@ -1648,7 +1635,7 @@
     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 FDERIV_intros assms(2)[rule_format] `x\<in>s`)+
+      by (rule has_derivative_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)"
@@ -1956,11 +1943,11 @@
     (\<forall>h. norm(f' x h - g' x h) \<le> inverse (real (Suc n)) * norm h)"
     by (metis assms(2) inverse_positive_iff_positive real_of_nat_Suc_gt_zero)
   obtain f where
-    *: "\<forall>x. \<exists>f'. \<forall>xa\<in>s. FDERIV (f x) xa : s :> f' xa \<and>
+    *: "\<forall>x. \<exists>f'. \<forall>xa\<in>s. (f x has_derivative f' xa) (at xa within s) \<and>
       (\<forall>h. norm (f' xa h - g' xa h) \<le> inverse (real (Suc x)) * norm h)"
     using *[THEN choice] ..
   obtain f' where
-    f: "\<forall>x. \<forall>xa\<in>s. FDERIV (f x) xa : s :> f' x xa \<and>
+    f: "\<forall>x. \<forall>xa\<in>s. (f x has_derivative f' x xa) (at xa within s) \<and>
       (\<forall>h. norm (f' x xa h - g' xa h) \<le> inverse (real (Suc x)) * norm h)"
     using *[THEN choice] ..
   show ?thesis
@@ -1996,23 +1983,19 @@
 
 subsection {* Differentiation of a series *}
 
-definition sums_seq :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> nat set \<Rightarrow> bool"
-    (infixl "sums'_seq" 12)
-  where "(f sums_seq l) s \<longleftrightarrow> ((\<lambda>n. setsum f (s \<inter> {0..n})) ---> l) sequentially"
-
 lemma has_derivative_series:
   fixes f :: "nat \<Rightarrow> 'm::euclidean_space \<Rightarrow> 'n::euclidean_space"
   assumes "convex s"
-    and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)"
-    and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (setsum (\<lambda>i. f' i x h) (k \<inter> {0..n}) - g' x h) \<le> e * norm h"
+    and "\<And>n x. x \<in> s \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within s)"
+    and "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (setsum (\<lambda>i. f' i x h) {0..<n} - g' x h) \<le> e * norm h"
     and "x \<in> s"
-    and "((\<lambda>n. f n x) sums_seq l) k"
-  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
+    and "(\<lambda>n. f n x) sums l"
+  shows "\<exists>g. \<forall>x\<in>s. (\<lambda>n. f n x) sums (g x) \<and> (g has_derivative g' x) (at x within s)"
+  unfolding sums_def
   apply (rule has_derivative_sequence[OF assms(1) _ assms(3)])
   apply (metis assms(2) has_derivative_setsum)
   using assms(4-5)
-  unfolding sums_seq_def
+  unfolding sums_def
   apply auto
   done
 
@@ -2020,7 +2003,7 @@
 text {* 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"
-    (infixl "has'_vector'_derivative" 12)
+    (infix "has'_vector'_derivative" 50)
   where "(f has_vector_derivative f') net \<longleftrightarrow> (f has_derivative (\<lambda>x. x *\<^sub>R f')) net"
 
 definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)"
@@ -2050,15 +2033,9 @@
     by auto
 qed
 
-lemma has_vector_derivative_withinI_DERIV:
-  assumes f: "DERIV f x :> y"
-  shows "(f has_vector_derivative y) (at x within s)"
-  unfolding has_vector_derivative_def real_scaleR_def
-  apply (rule has_derivative_at_within)
-  using DERIV_conv_has_derivative[THEN iffD1, OF f]
-  apply (subst mult_commute)
-  apply assumption
-  done
+lemma has_field_derivative_iff_has_vector_derivative:
+  "(f has_field_derivative y) F \<longleftrightarrow> (f has_vector_derivative y) F"
+  unfolding has_vector_derivative_def has_field_derivative_def real_scaleR_def mult_commute_abs ..
 
 lemma vector_derivative_unique_at:
   assumes "(f has_vector_derivative f') (at x)"
diff -r 01fb1b35433b -r 2666cd7d380c src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Mar 17 20:54:41 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Mar 17 21:56:32 2014 +0100
@@ -8634,8 +8634,8 @@
       apply (rule diff_chain_within)
       apply (rule has_derivative_add)
       unfolding scaleR_simps
-      apply (intro FDERIV_intros)
-      apply (intro FDERIV_intros)
+      apply (intro has_derivative_intros)
+      apply (intro has_derivative_intros)
       apply (rule has_derivative_within_subset,rule assms(6)[rule_format])
       apply (rule *)
       apply safe
@@ -11679,13 +11679,18 @@
       then show False
         using goal2 by auto
     qed
-    then guess K .. note * = this[unfolded image_iff not_le]
-    from this(1) guess d .. note this[unfolded mem_Collect_eq]
+    then obtain K where *: "\<exists>x\<in>{d. d division_of \<Union>d}. K = (\<Sum>k\<in>x. norm (integral k f))"
+      "SUPR {d. d division_of \<Union>d} (setsum (\<lambda>k. norm (integral k f))) - e < K"
+      by (auto simp add: image_iff not_le)
+    from this(1) obtain d where "d division_of \<Union>d"
+      and "K = (\<Sum>k\<in>d. norm (integral k f))"
+      by auto
     note d = this(1) *(2)[unfolded this(2)]
     note d'=division_ofD[OF this(1)]
     have "bounded (\<Union>d)"
       by (rule elementary_bounded,fact)
-    from this[unfolded bounded_pos] guess K .. note K=conjunctD2[OF this]
+    from this[unfolded bounded_pos] obtain K where
+       K: "0 < K" "\<forall>x\<in>\<Union>d. norm x \<le> K" by auto
     show ?case
       apply (rule_tac x="K + 1" in exI)
       apply safe
@@ -11742,10 +11747,18 @@
         note * = this(2)[unfolded has_integral_integral has_integral[of "\<lambda>x. norm (f x)"],rule_format]
         have "e/2>0"
           using `e > 0` by auto
-        from *[OF this] guess d1 .. note d1=conjunctD2[OF this]
-        from henstock_lemma[OF f(1) `e/2>0`] guess d2 . note d2=this
-        from fine_division_exists[OF gauge_inter[OF d1(1) d2(1)], of a b] guess p .
-        note p=this(1) conjunctD2[OF this(2)[unfolded fine_inter]]
+        from * [OF this] obtain d1 where
+          d1: "gauge d1" "\<forall>p. p tagged_division_of {a..b} \<and> d1 fine p \<longrightarrow>
+            norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - integral {a..b} (\<lambda>x. norm (f x))) < e / 2"
+          by auto
+        from henstock_lemma [OF f(1) `e/2>0`] obtain d2 where
+          d2: "gauge d2" "\<forall>p. p tagged_partial_division_of {a..b} \<and> d2 fine p \<longrightarrow>
+            (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x - integral k f)) < e / 2"
+          by blast
+        obtain p where
+          p: "p tagged_division_of {a..b}" "d1 fine p" "d2 fine p"
+          by (rule fine_division_exists [OF gauge_inter [OF d1(1) d2(1)], of a b])
+            (auto simp add: fine_inter)
         have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> ?S \<longrightarrow> abs (sf - si) < e / 2 \<longrightarrow>
           abs (sf' - di) < e / 2 \<longrightarrow> di < ?S + e"
           by arith
diff -r 01fb1b35433b -r 2666cd7d380c src/HOL/Number_Theory/Binomial.thy
--- a/src/HOL/Number_Theory/Binomial.thy	Mon Mar 17 20:54:41 2014 +0100
+++ b/src/HOL/Number_Theory/Binomial.thy	Mon Mar 17 21:56:32 2014 +0100
@@ -186,6 +186,37 @@
            of_nat_setsum [symmetric]
            of_nat_eq_iff of_nat_id)
 
+lemma choose_row_sum: "(\<Sum>k=0..n. n choose k) = 2^n"
+  using binomial [of 1 "1" n]
+  by (simp add: numeral_2_eq_2)
+
+lemma sum_choose_lower: "(\<Sum>k=0..n. (r+k) choose k) = Suc (r+n) choose n"
+  by (induct n) auto
+
+lemma sum_choose_upper: "(\<Sum>k=0..n. k choose m) = Suc n choose Suc m"
+  by (induct n) auto
+
+lemma natsum_reverse_index:
+  fixes m::nat
+  assumes "\<And>k. m \<le> k \<Longrightarrow> k \<le> n \<Longrightarrow> g k = f (m + n - k)"
+  shows "(\<Sum>k=m..n. f k) = (\<Sum>k=m..n. g k)"
+apply (rule setsum_reindex_cong [where f = "\<lambda>k. m+n-k"])
+apply (auto simp add: inj_on_def image_def)
+apply (rule_tac x="m+n-x" in bexI, auto simp: assms)
+done
+
+lemma sum_choose_diagonal:
+  assumes "m\<le>n" shows "(\<Sum>k=0..m. (n-k) choose (m-k)) = Suc n choose m"
+proof -
+  have "(\<Sum>k=0..m. (n-k) choose (m-k)) = (\<Sum>k=0..m. (n-m+k) choose k)"
+    by (rule natsum_reverse_index) (simp add: assms)
+  also have "... = Suc (n-m+m) choose m"
+    by (rule sum_choose_lower)
+  also have "... = Suc n choose m" using assms
+    by simp
+  finally show ?thesis .
+qed
+
 subsection{* Pochhammer's symbol : generalized rising factorial *}
 
 text {* See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"} *}
@@ -605,6 +636,42 @@
     n choose k = fact n div (fact k * fact (n - k))"
  by (subst binomial_fact_lemma [symmetric]) auto
 
+lemma fact_fact_dvd_fact_m: fixes k::nat shows "k \<le> n \<Longrightarrow> fact k * fact (n - k) dvd fact n"
+  by (metis binomial_fact_lemma dvd_def)
+
+lemma fact_fact_dvd_fact: fixes k::nat shows "fact k * fact n dvd fact (n + k)"
+  by (metis fact_fact_dvd_fact_m diff_add_inverse2 le_add2)
+
+lemma choose_mult_lemma:
+     "((m+r+k) choose (m+k)) * ((m+k) choose k) = ((m+r+k) choose k) * ((m+r) choose m)"
+proof -
+  have "((m+r+k) choose (m+k)) * ((m+k) choose k) =
+        fact (m+r + k) div (fact (m + k) * fact (m+r - m)) * (fact (m + k) div (fact k * fact m))"
+    by (simp add: assms binomial_altdef_nat)
+  also have "... = fact (m+r+k) div (fact r * (fact k * fact m))"
+    apply (subst div_mult_div_if_dvd)
+    apply (auto simp: fact_fact_dvd_fact)
+    apply (metis ab_semigroup_add_class.add_ac(1) add_commute fact_fact_dvd_fact)
+    done
+  also have "... = (fact (m+r+k) * fact (m+r)) div (fact r * (fact k * fact m) * fact (m+r))"
+    apply (subst div_mult_div_if_dvd [symmetric])
+    apply (auto simp: fact_fact_dvd_fact)
+    apply (metis dvd_trans dvd.dual_order.refl fact_fact_dvd_fact mult_dvd_mono mult_left_commute)
+    done
+  also have "... = (fact (m+r+k) div (fact k * fact (m+r)) * (fact (m+r) div (fact r * fact m)))"
+    apply (subst div_mult_div_if_dvd)
+    apply (auto simp: fact_fact_dvd_fact)
+    apply(metis mult_left_commute)
+    done
+  finally show ?thesis
+    by (simp add: binomial_altdef_nat mult_commute)
+qed
+
+lemma choose_mult:
+  assumes "k\<le>m" "m\<le>n"
+    shows "(n choose m) * (m choose k) = (n choose k) * ((n-k) choose (m-k))"
+using assms choose_mult_lemma [of "m-k" "n-m" k]
+by simp
 
 
 subsection {* Binomial coefficients *}
diff -r 01fb1b35433b -r 2666cd7d380c src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Mon Mar 17 20:54:41 2014 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Mon Mar 17 21:56:32 2014 +0100
@@ -1057,6 +1057,10 @@
   qed
 qed simp
 
+lemma has_field_derivative_subset:
+  "(f has_field_derivative y) (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_field_derivative y) (at x within t)"
+  unfolding has_field_derivative_def by (rule has_derivative_subset)
+
 lemma integral_FTC_atLeastAtMost:
   fixes a b :: real
   assumes "a \<le> b"
@@ -1070,7 +1074,9 @@
     by (rule borel_integral_has_integral)
   moreover
   have "(f has_integral F b - F a) {a .. b}"
-    by (intro fundamental_theorem_of_calculus has_vector_derivative_withinI_DERIV ballI assms) auto
+    by (intro fundamental_theorem_of_calculus)
+       (auto simp: has_field_derivative_iff_has_vector_derivative[symmetric]
+             intro: has_field_derivative_subset[OF F] assms(1))
   then have "(?f has_integral F b - F a) {a .. b}"
     by (subst has_integral_eq_eq[where g=f]) auto
   then have "(?f has_integral F b - F a) UNIV"
@@ -1091,7 +1097,9 @@
   shows "(\<integral>\<^sup>+x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a"
 proof -
   have i: "(f has_integral F b - F a) {a..b}"
-    by (intro fundamental_theorem_of_calculus ballI has_vector_derivative_withinI_DERIV assms)
+    by (intro fundamental_theorem_of_calculus)
+       (auto simp: has_field_derivative_iff_has_vector_derivative[symmetric]
+             intro: has_field_derivative_subset[OF f(1)] `a \<le> b`)
   have i: "((\<lambda>x. f x * indicator {a..b} x) has_integral F b - F a) {a..b}"
     by (rule has_integral_eq[OF _ i]) auto
   have i: "((\<lambda>x. f x * indicator {a..b} x) has_integral F b - F a) UNIV"
diff -r 01fb1b35433b -r 2666cd7d380c src/HOL/Series.thy
--- a/src/HOL/Series.thy	Mon Mar 17 20:54:41 2014 +0100
+++ b/src/HOL/Series.thy	Mon Mar 17 21:56:32 2014 +0100
@@ -562,6 +562,22 @@
 apply simp
 done
 
+lemma norm_bound_subset:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+  assumes "finite s" "t \<subseteq> s"
+  assumes le: "(\<And>x. x \<in> s \<Longrightarrow> norm(f x) \<le> g x)"
+  shows "norm (setsum f t) \<le> setsum g s"
+proof -
+  have "norm (setsum f t) \<le> (\<Sum>i\<in>t. norm (f i))"
+    by (rule norm_setsum)
+  also have "\<dots> \<le> (\<Sum>i\<in>t. g i)"
+    using assms by (auto intro!: setsum_mono)
+  also have "\<dots> \<le> setsum g s"
+    using assms order.trans[OF norm_ge_zero le]
+    by (auto intro!: setsum_mono3)
+  finally show ?thesis .
+qed
+
 lemma summable_comparison_test:
   fixes f :: "nat \<Rightarrow> 'a::banach"
   shows "\<lbrakk>\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n; summable g\<rbrakk> \<Longrightarrow> summable f"
diff -r 01fb1b35433b -r 2666cd7d380c src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Mar 17 20:54:41 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Mar 17 21:56:32 2014 +0100
@@ -1707,9 +1707,9 @@
     
         fun col_spec j Zero hrec hrec' =
           let
-            fun mk_Suc dtor setss z z' =
+            fun mk_Suc dtor sets z z' =
               let
-                val (set, sets) = apfst (fn xs => nth xs (j - 1)) (chop m setss);
+                val (set, sets) = apfst (fn xs => nth xs (j - 1)) (chop m sets);
                 fun mk_UN set k = mk_UNION (set $ (dtor $ z)) (mk_nthN n hrec k);
               in
                 Term.absfree z'
@@ -1748,295 +1748,32 @@
         val col_0ss' = transpose col_0ss;
         val col_Sucss' = transpose col_Sucss;
     
-        fun mk_hset Ts i j T =
+        fun mk_set Ts i j T =
           Abs (Name.uu, nth Ts (i - 1), mk_UNION (HOLogic.mk_UNIV HOLogic.natT)
             (Term.absfree nat' (mk_col Ts nat i j T $ Bound 1)));
 
-        val setss_by_bnf = map (fn i => map2 (mk_hset Ts i) ls passiveAs) ks;
-        val setss_by_range = transpose setss_by_bnf;
-
-        val hset_minimal_thms =
-          let
-            fun mk_passive_prem set dtor x K =
-              Logic.all x (HOLogic.mk_Trueprop (mk_leq (set $ (dtor $ x)) (K $ x)));
-    
-            fun mk_active_prem dtor x1 K1 set x2 K2 =
-              fold_rev Logic.all [x1, x2]
-                (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x2, set $ (dtor $ x1))),
-                  HOLogic.mk_Trueprop (mk_leq (K2 $ x2) (K1 $ x1))));
-    
-            val premss = map2 (fn j => fn Ks =>
-              map4 mk_passive_prem (map (fn xs => nth xs (j - 1)) FTs_setss) dtors Jzs Ks @
-                flat (map4 (fn sets => fn s => fn x1 => fn K1 =>
-                  map3 (mk_active_prem s x1 K1) (drop m sets) Jzs_copy Ks) FTs_setss dtors Jzs Ks))
-              ls Kss;
-    
-            val col_minimal_thms =
-              let
-                fun mk_conjunct j T i K x = mk_leq (mk_col Ts nat i j T $ x) (K $ x);
-                fun mk_concl j T Ks = list_all_free Jzs
-                  (Library.foldr1 HOLogic.mk_conj (map3 (mk_conjunct j T) ks Ks Jzs));
-                val concls = map3 mk_concl ls passiveAs Kss;
-    
-                val goals = map2 (fn prems => fn concl =>
-                  Logic.list_implies (prems, HOLogic.mk_Trueprop concl)) premss concls
-    
-                val ctss =
-                  map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) concls;
-              in
-                map4 (fn goal => fn cts => fn col_0s => fn col_Sucs =>
-                  singleton (Proof_Context.export names_lthy lthy)
-                    (Goal.prove_sorry lthy [] [] goal
-                      (fn {context = ctxt, prems = _} => mk_col_minimal_tac ctxt m cts col_0s
-                        col_Sucs))
-                  |> Thm.close_derivation)
-                goals ctss col_0ss' col_Sucss'
-              end;
-    
-            fun mk_conjunct j T i K x = mk_leq (mk_hset Ts i j T $ x) (K $ x);
-            fun mk_concl j T Ks = Library.foldr1 HOLogic.mk_conj (map3 (mk_conjunct j T) ks Ks Jzs);
-            val concls = map3 mk_concl ls passiveAs Kss;
-    
-            val goals = map3 (fn Ks => fn prems => fn concl =>
-              fold_rev Logic.all (Ks @ Jzs)
-                (Logic.list_implies (prems, HOLogic.mk_Trueprop concl))) Kss premss concls;
-          in
-            map2 (fn goal => fn col_minimal =>
-              Goal.prove_sorry lthy [] [] goal
-                (fn {context = ctxt, prems = _} => mk_hset_minimal_tac ctxt n col_minimal)
-              |> Thm.close_derivation)
-            goals col_minimal_thms
-          end;
-
-        val (set_incl_hset_thmss, set_hset_incl_hset_thmsss) =
-          let
-            fun mk_set_incl_hset dtor x set hset = fold_rev Logic.all (x :: ss)
-              (HOLogic.mk_Trueprop (mk_leq (set $ (dtor $ x)) (hset $ x)));
-    
-            fun mk_set_hset_incl_hset dtor x y set hset1 hset2 =
-              fold_rev Logic.all [x, y]
-                (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x, set $ (dtor $ y))),
-                HOLogic.mk_Trueprop (mk_leq (hset1 $ x) (hset2 $ y))));
-    
-            val set_incl_hset_goalss =
-              map4 (fn dtor => fn x => fn sets => fn hsets =>
-                map2 (mk_set_incl_hset dtor x) (take m sets) hsets)
-              dtors Jzs FTs_setss setss_by_bnf;
-    
-            (*xk : F(i)set(m+k) (si yi) ==> F(k)_hset(j) s1 ... sn xk <= F(i)_hset(j) s1 ... sn yi*)
-            val set_hset_incl_hset_goalsss =
-              map4 (fn dtori => fn yi => fn sets => fn hsetsi =>
-                map3 (fn xk => fn set => fn hsetsk =>
-                  map2 (mk_set_hset_incl_hset dtori xk yi set) hsetsk hsetsi)
-                Jzs_copy (drop m sets) setss_by_bnf)
-              dtors Jzs FTs_setss setss_by_bnf;
-          in
-            (map2 (fn goals => fn rec_Sucs =>
-              map2 (fn goal => fn rec_Suc =>
-                Goal.prove_sorry lthy [] [] goal (K (mk_set_incl_hset_tac rec_Suc))
-                |> Thm.close_derivation)
-              goals rec_Sucs)
-            set_incl_hset_goalss col_Sucss,
-            map2 (fn goalss => fn rec_Sucs =>
-              map2 (fn k => fn goals =>
-                map2 (fn goal => fn rec_Suc =>
-                  Goal.prove_sorry lthy [] [] goal
-                    (K (mk_set_hset_incl_hset_tac n rec_Suc k))
-                  |> Thm.close_derivation)
-                goals rec_Sucs)
-              ks goalss)
-            set_hset_incl_hset_goalsss col_Sucss)
-          end;
-    
-        val set_incl_hset_thmss' = transpose set_incl_hset_thmss;
-        val set_hset_incl_hset_thmsss' = transpose (map transpose set_hset_incl_hset_thmsss);
-        val set_hset_thmss = map (map (fn thm => thm RS @{thm set_mp})) set_incl_hset_thmss;
-        val set_hset_hset_thmsss = map (map (map (fn thm => thm RS @{thm set_mp})))
-          set_hset_incl_hset_thmsss;
-        val set_hset_thmss' = transpose set_hset_thmss;
-        val set_hset_hset_thmsss' = transpose (map transpose set_hset_hset_thmsss);
-
-
-        val timer = time (timer "Hereditary sets");
-    
-        val dtor_hset_induct_thms =
-          let
-            val incls =
-              maps (map (fn thm => thm RS @{thm subset_Collect_iff})) set_incl_hset_thmss @
-                @{thms subset_Collect_iff[OF subset_refl]};
-
-            val cTs = map (SOME o certifyT lthy) params';    
-            fun mk_induct_tinst phis jsets y y' =
-              map4 (fn phi => fn jset => fn Jz => fn Jz' =>
-                SOME (certify lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y',
-                  HOLogic.mk_conj (HOLogic.mk_mem (y, jset $ Jz), phi $ y $ Jz))))))
-              phis jsets Jzs Jzs';
-          in
-            map6 (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis =>
-              ((set_minimal
-                |> Drule.instantiate' cTs (mk_induct_tinst phis jsets y y')
-                |> unfold_thms lthy incls) OF
-                (replicate n ballI @
-                  maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss))
-              |> singleton (Proof_Context.export names_lthy lthy)
-              |> rule_by_tactic lthy (ALLGOALS (TRY o etac asm_rl)))
-            hset_minimal_thms set_hset_incl_hset_thmsss' setss_by_range ys ys' dtor_set_induct_phiss
-          end;
-
-        fun close_wit I wit = (I, fold_rev Term.absfree (map (nth ys') I) wit);
-
-        val all_unitTs = replicate live HOLogic.unitT;
-        val unitTs = replicate n HOLogic.unitT;
-        val unit_funs = replicate n (Term.absdummy HOLogic.unitT HOLogic.unit);
-        fun mk_map_args I =
-          map (fn i =>
-            if member (op =) I i then Term.absdummy HOLogic.unitT (nth ys i)
-            else mk_undefined (HOLogic.unitT --> nth passiveAs i))
-          (0 upto (m - 1));
-
-        fun mk_nat_wit Ds bnf (I, wit) () =
-          let
-            val passiveI = filter (fn i => i < m) I;
-            val map_args = mk_map_args passiveI;
-          in
-            Term.absdummy HOLogic.unitT (Term.list_comb
-              (mk_map_of_bnf Ds all_unitTs (passiveAs @ unitTs) bnf, map_args @ unit_funs) $ wit)
-          end;
-
-        fun mk_dummy_wit Ds bnf I =
-          let
-            val map_args = mk_map_args I;
-          in
-            Term.absdummy HOLogic.unitT (Term.list_comb
-              (mk_map_of_bnf Ds all_unitTs (passiveAs @ unitTs) bnf, map_args @ unit_funs) $
-              mk_undefined (mk_T_of_bnf Ds all_unitTs bnf))
-          end;
-
-        val nat_witss =
-          map2 (fn Ds => fn bnf => mk_wits_of_bnf (replicate (nwits_of_bnf bnf) Ds)
-            (replicate (nwits_of_bnf bnf) (replicate live HOLogic.unitT)) bnf
-            |> map (fn (I, wit) =>
-              (I, Lazy.lazy (mk_nat_wit Ds bnf (I, Term.list_comb (wit, map (K HOLogic.unit) I))))))
-          Dss bnfs;
-
-        val nat_wit_thmss = map2 (curry op ~~) nat_witss (map wit_thmss_of_bnf bnfs)
-
-        val Iss = map (map fst) nat_witss;
-
-        fun filter_wits (I, wit) =
-          let val J = filter (fn i => i < m) I;
-          in (J, (length J < length I, wit)) end;
-
-        val wit_treess = map_index (fn (i, Is) =>
-          map_index (finish Iss m [i+m] (i+m)) Is) Iss
-          |> map (minimize_wits o map filter_wits o minimize_wits o flat);
-
-        val coind_wit_argsss =
-          map (map (tree_to_coind_wits nat_wit_thmss o snd o snd) o filter (fst o snd)) wit_treess;
-
-        val nonredundant_coind_wit_argsss =
-          fold (fn i => fn argsss =>
-            nth_map (i - 1) (filter_out (fn xs =>
-              exists (fn ys =>
-                let
-                  val xs' = (map (fst o fst) xs, snd (fst (hd xs)));
-                  val ys' = (map (fst o fst) ys, snd (fst (hd ys)));
-                in
-                  eq_pair (subset (op =)) (eq_set (op =)) (xs', ys') andalso not (fst xs' = fst ys')
-                end)
-              (flat argsss)))
-            argsss)
-          ks coind_wit_argsss;
-
-        fun prepare_args args =
-          let
-            val I = snd (fst (hd args));
-            val (dummys, args') =
-              map_split (fn i =>
-                (case find_first (fn arg => fst (fst arg) = i - 1) args of
-                  SOME (_, ((_, wit), thms)) => (NONE, (Lazy.force wit, thms))
-                | NONE =>
-                  (SOME (i - 1), (mk_dummy_wit (nth Dss (i - 1)) (nth bnfs (i - 1)) I, []))))
-              ks;
-          in
-            ((I, dummys), apsnd flat (split_list args'))
-          end;
-
-        fun mk_coind_wits ((I, dummys), (args, thms)) =
-          ((I, dummys), (map (fn i => mk_unfold Ts args i $ HOLogic.unit) ks, thms));
-
-        val coind_witss =
-          maps (map (mk_coind_wits o prepare_args)) nonredundant_coind_wit_argsss;
-
-        val witss = map2 (fn Ds => fn bnf => mk_wits_of_bnf
-          (replicate (nwits_of_bnf bnf) Ds)
-          (replicate (nwits_of_bnf bnf) (passiveAs @ Ts)) bnf) Dss bnfs;
-
-        val ctor_witss =
-          map (map (uncurry close_wit o tree_to_ctor_wit ys ctors witss o snd o snd) o
-            filter_out (fst o snd)) wit_treess;
-
-        fun mk_coind_wit_thms ((I, dummys), (wits, wit_thms)) =
-          let
-            fun mk_goal sets y y_copy y'_copy j =
-              let
-                fun mk_conjunct set z dummy wit =
-                  mk_Ball (set $ z) (Term.absfree y'_copy
-                    (if dummy = NONE orelse member (op =) I (j - 1) then
-                      HOLogic.mk_imp (HOLogic.mk_eq (z, wit),
-                        if member (op =) I (j - 1) then HOLogic.mk_eq (y_copy, y)
-                        else @{term False})
-                    else @{term True}));
-              in
-                fold_rev Logic.all (map (nth ys) I @ Jzs) (HOLogic.mk_Trueprop
-                  (Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct sets Jzs dummys wits)))
-              end;
-            val goals = map5 mk_goal setss_by_range ys ys_copy ys'_copy ls;
-          in
-            map2 (fn goal => fn induct =>
-              Goal.prove_sorry lthy [] [] goal
-                (fn {context = ctxt, prems = _} => mk_coind_wit_tac ctxt induct dtor_unfold_thms
-                  (flat set_mapss) wit_thms)
-              |> Thm.close_derivation)
-            goals dtor_hset_induct_thms
-            |> map split_conj_thm
-            |> transpose
-            |> map (map_filter (try (fn thm => thm RS bspec RS mp)))
-            |> curry op ~~ (map_index Library.I (map (close_wit I) wits))
-            |> filter (fn (_, thms) => length thms = m)
-          end;
-
-        val coind_wit_thms = maps mk_coind_wit_thms coind_witss;
-
-        val (wit_thmss, all_witss) =
-          fold (fn ((i, wit), thms) => fn witss =>
-            nth_map i (fn (thms', wits) => (thms @ thms', wit :: wits)) witss)
-          coind_wit_thms (map (pair []) ctor_witss)
-          |> map (apsnd (map snd o minimize_wits))
-          |> split_list;
+        val setss = map (fn i => map2 (mk_set Ts i) ls passiveAs) ks;
 
         val (Jbnf_consts, lthy) =
-          fold_map8 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn wits =>
-              fn T => fn lthy =>
-            define_bnf_consts Dont_Inline (user_policy Note_Some lthy) false (SOME deads)
+          fold_map7 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn T =>
+              fn lthy =>
+            define_bnf_consts Hardly_Inline (user_policy Note_Some lthy) false (SOME deads)
               map_b rel_b set_bs
-              ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), wits), NONE) lthy)
-          bs map_bs rel_bs set_bss fs_maps setss_by_bnf all_witss Ts lthy;
+              ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd),
+                [Const (@{const_name undefined}, T)]), NONE) lthy)
+          bs map_bs rel_bs set_bss fs_maps setss Ts lthy;
 
         val (_, Jconsts, Jconst_defs, mk_Jconsts) = split_list4 Jbnf_consts;
-        val (_, Jsetss, Jbds_Ds, Jwitss_Ds, _) = split_list5 Jconsts;
-        val (Jmap_defs, Jset_defss, Jbd_defs, Jwit_defss, Jrel_defs) = split_list5 Jconst_defs;
+        val (_, Jsetss, Jbds_Ds, _, _) = split_list5 Jconsts;
+        val (Jmap_defs, Jset_defss, Jbd_defs, _, Jrel_defs) = split_list5 Jconst_defs;
         val (mk_Jmaps_Ds, mk_Jt_Ds, _, mk_Jrels_Ds, _) = split_list5 mk_Jconsts;
 
         val Jrel_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Jrel_defs;
         val Jset_defs = flat Jset_defss;
-        val Jset_unabs_defs = map (fn def => def RS meta_eq_to_obj_eq RS fun_cong) Jset_defs;
 
         fun mk_Jmaps As Bs = map (fn mk => mk deads As Bs) mk_Jmaps_Ds;
         fun mk_Jsetss As = map2 (fn mk => fn Jsets => map (mk deads As) Jsets) mk_Jt_Ds Jsetss;
         val Jbds = map2 (fn mk => mk deads passiveAs) mk_Jt_Ds Jbds_Ds;
-        val Jwitss =
-          map2 (fn mk => fn Jwits => map (mk deads passiveAs o snd) Jwits) mk_Jt_Ds Jwitss_Ds;
         fun mk_Jrels As Bs = map (fn mk => mk deads As Bs) mk_Jrels_Ds;
 
         val Jmaps = mk_Jmaps passiveAs passiveBs;
@@ -2098,6 +1835,135 @@
 
         val timer = time (timer "map functions for the new codatatypes");
 
+        val Jset_minimal_thms =
+          let
+            fun mk_passive_prem set dtor x K =
+              Logic.all x (HOLogic.mk_Trueprop (mk_leq (set $ (dtor $ x)) (K $ x)));
+    
+            fun mk_active_prem dtor x1 K1 set x2 K2 =
+              fold_rev Logic.all [x1, x2]
+                (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x2, set $ (dtor $ x1))),
+                  HOLogic.mk_Trueprop (mk_leq (K2 $ x2) (K1 $ x1))));
+    
+            val premss = map2 (fn j => fn Ks =>
+              map4 mk_passive_prem (map (fn xs => nth xs (j - 1)) FTs_setss) dtors Jzs Ks @
+                flat (map4 (fn sets => fn s => fn x1 => fn K1 =>
+                  map3 (mk_active_prem s x1 K1) (drop m sets) Jzs_copy Ks) FTs_setss dtors Jzs Ks))
+              ls Kss;
+    
+            val col_minimal_thms =
+              let
+                fun mk_conjunct j T i K x = mk_leq (mk_col Ts nat i j T $ x) (K $ x);
+                fun mk_concl j T Ks = list_all_free Jzs
+                  (Library.foldr1 HOLogic.mk_conj (map3 (mk_conjunct j T) ks Ks Jzs));
+                val concls = map3 mk_concl ls passiveAs Kss;
+    
+                val goals = map2 (fn prems => fn concl =>
+                  Logic.list_implies (prems, HOLogic.mk_Trueprop concl)) premss concls
+    
+                val ctss =
+                  map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) concls;
+              in
+                map4 (fn goal => fn cts => fn col_0s => fn col_Sucs =>
+                  singleton (Proof_Context.export names_lthy lthy)
+                    (Goal.prove_sorry lthy [] [] goal
+                      (fn {context = ctxt, prems = _} => mk_col_minimal_tac ctxt m cts col_0s
+                        col_Sucs))
+                  |> Thm.close_derivation)
+                goals ctss col_0ss' col_Sucss'
+              end;
+    
+            fun mk_conjunct set K x = mk_leq (set $ x) (K $ x);
+            fun mk_concl sets Ks = Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct sets Ks Jzs);
+            val concls = map2 mk_concl Jsetss_by_range Kss;
+    
+            val goals = map3 (fn Ks => fn prems => fn concl =>
+              fold_rev Logic.all (Ks @ Jzs)
+                (Logic.list_implies (prems, HOLogic.mk_Trueprop concl))) Kss premss concls;
+          in
+            map2 (fn goal => fn col_minimal =>
+              Goal.prove_sorry lthy [] [] goal
+                (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
+                  mk_Jset_minimal_tac ctxt n col_minimal)
+              |> Thm.close_derivation)
+            goals col_minimal_thms
+          end;
+
+        val (dtor_Jset_incl_thmss, dtor_set_Jset_incl_thmsss) =
+          let
+            fun mk_set_incl_Jset dtor x set Jset = fold_rev Logic.all (x :: ss)
+              (HOLogic.mk_Trueprop (mk_leq (set $ (dtor $ x)) (Jset $ x)));
+    
+            fun mk_set_Jset_incl_Jset dtor x y set Jset1 Jset2 =
+              fold_rev Logic.all [x, y]
+                (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x, set $ (dtor $ y))),
+                HOLogic.mk_Trueprop (mk_leq (Jset1 $ x) (Jset2 $ y))));
+    
+            val set_incl_Jset_goalss =
+              map4 (fn dtor => fn x => fn sets => fn Jsets =>
+                map2 (mk_set_incl_Jset dtor x) (take m sets) Jsets)
+              dtors Jzs FTs_setss Jsetss_by_bnf;
+    
+            (*x(k) : F(i)set(m+k) (dtor(i) y(i)) ==> J(k)set(j) x(k) <= J(i)set(j) y(i)*)
+            val set_Jset_incl_Jset_goalsss =
+              map4 (fn dtori => fn yi => fn sets => fn Jsetsi =>
+                map3 (fn xk => fn set => fn Jsetsk =>
+                  map2 (mk_set_Jset_incl_Jset dtori xk yi set) Jsetsk Jsetsi)
+                Jzs_copy (drop m sets) Jsetss_by_bnf)
+              dtors Jzs FTs_setss Jsetss_by_bnf;
+          in
+            (map2 (fn goals => fn rec_Sucs =>
+              map2 (fn goal => fn rec_Suc =>
+                Goal.prove_sorry lthy [] [] goal
+                  (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
+                    mk_set_incl_Jset_tac rec_Suc)
+                |> Thm.close_derivation)
+              goals rec_Sucs)
+            set_incl_Jset_goalss col_Sucss,
+            map2 (fn goalss => fn rec_Sucs =>
+              map2 (fn k => fn goals =>
+                map2 (fn goal => fn rec_Suc =>
+                  Goal.prove_sorry lthy [] [] goal
+                    (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
+                      mk_set_Jset_incl_Jset_tac n rec_Suc k)
+                  |> Thm.close_derivation)
+                goals rec_Sucs)
+              ks goalss)
+            set_Jset_incl_Jset_goalsss col_Sucss)
+          end;
+    
+        val set_incl_Jset_thmss' = transpose dtor_Jset_incl_thmss;
+        val set_Jset_incl_Jset_thmsss' = transpose (map transpose dtor_set_Jset_incl_thmsss);
+        val set_Jset_thmss = map (map (fn thm => thm RS @{thm set_mp})) dtor_Jset_incl_thmss;
+        val set_Jset_Jset_thmsss = map (map (map (fn thm => thm RS @{thm set_mp})))
+          dtor_set_Jset_incl_thmsss;
+        val set_Jset_thmss' = transpose set_Jset_thmss;
+        val set_Jset_Jset_thmsss' = transpose (map transpose set_Jset_Jset_thmsss);
+    
+        val dtor_Jset_induct_thms =
+          let
+            val incls =
+              maps (map (fn thm => thm RS @{thm subset_Collect_iff})) dtor_Jset_incl_thmss @
+                @{thms subset_Collect_iff[OF subset_refl]};
+
+            val cTs = map (SOME o certifyT lthy) params';    
+            fun mk_induct_tinst phis jsets y y' =
+              map4 (fn phi => fn jset => fn Jz => fn Jz' =>
+                SOME (certify lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y',
+                  HOLogic.mk_conj (HOLogic.mk_mem (y, jset $ Jz), phi $ y $ Jz))))))
+              phis jsets Jzs Jzs';
+          in
+            map6 (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis =>
+              ((set_minimal
+                |> Drule.instantiate' cTs (mk_induct_tinst phis jsets y y')
+                |> unfold_thms lthy incls) OF
+                (replicate n ballI @
+                  maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss))
+              |> singleton (Proof_Context.export names_lthy lthy)
+              |> rule_by_tactic lthy (ALLGOALS (TRY o etac asm_rl)))
+            Jset_minimal_thms set_Jset_incl_Jset_thmsss' Jsetss_by_range ys ys' dtor_set_induct_phiss
+          end;
+
         val (dtor_Jset_thmss', dtor_Jset_thmss) =
           let
             fun mk_simp_goal relate pas_set act_sets sets dtor z set =
@@ -2115,23 +1981,21 @@
               (fold_rev Logic.all Jzs o HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj)
               (mk_goals (uncurry mk_leq));
             val set_le_thmss = map split_conj_thm
-              (map4 (fn goal => fn hset_minimal => fn set_hsets => fn set_hset_hsetss =>
+              (map4 (fn goal => fn Jset_minimal => fn set_Jsets => fn set_Jset_Jsetss =>
                 Goal.prove_sorry lthy [] [] goal
-                  (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
-                    mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss)
+                  (K (mk_set_le_tac n Jset_minimal set_Jsets set_Jset_Jsetss))
                 |> Thm.close_derivation)
-              le_goals hset_minimal_thms set_hset_thmss' set_hset_hset_thmsss');
+              le_goals Jset_minimal_thms set_Jset_thmss' set_Jset_Jset_thmsss');
 
             val ge_goalss = map (map2 (fn z => fn goal =>
                 Logic.all z (HOLogic.mk_Trueprop goal)) Jzs)
               (mk_goals (uncurry mk_leq o swap));
             val set_ge_thmss = 
-              map3 (map3 (fn goal => fn set_incl_hset => fn set_hset_incl_hsets =>
+              map3 (map3 (fn goal => fn set_incl_Jset => fn set_Jset_incl_Jsets =>
                 Goal.prove_sorry lthy [] [] goal
-                  (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
-                    mk_set_ge_tac n set_incl_hset set_hset_incl_hsets)
+                  (K (mk_set_ge_tac n set_incl_Jset set_Jset_incl_Jsets))
                 |> Thm.close_derivation))
-              ge_goalss set_incl_hset_thmss' set_hset_incl_hset_thmsss'
+              ge_goalss set_incl_Jset_thmss' set_Jset_incl_Jset_thmsss'
           in
             map2 (map2 (fn le => fn ge => equalityI OF [le, ge])) set_le_thmss set_ge_thmss
             |> `transpose
@@ -2222,8 +2086,7 @@
             val cphis = map9 mk_cphi
               Jsetss_by_bnf Jzs' Jzs fs_Jmaps fs_copy_Jmaps Jys' Jys Jys'_copy Jys_copy;
 
-            val coinduct = unfold_thms lthy Jset_defs
-              (Drule.instantiate' cTs (map SOME cphis) dtor_coinduct_thm);
+            val coinduct = Drule.instantiate' cTs (map SOME cphis) dtor_coinduct_thm;
 
             val goal =
               HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
@@ -2231,9 +2094,8 @@
 
             val thm = singleton (Proof_Context.export names_lthy lthy)
               (Goal.prove_sorry lthy [] [] goal
-                (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
-                  mk_mcong_tac lthy m (rtac coinduct) map_comps dtor_Jmap_thms map_cong0s
-                    set_mapss set_hset_thmss set_hset_hset_thmsss in_rels))
+                (K (mk_mcong_tac lthy m (rtac coinduct) map_comps dtor_Jmap_thms map_cong0s
+                  set_mapss set_Jset_thmss set_Jset_Jset_thmsss in_rels)))
               |> Thm.close_derivation
           in
             split_conj_thm thm
@@ -2242,12 +2104,6 @@
         val in_Jrels = map (fn def => trans OF [def, @{thm OO_Grp_alt}] RS @{thm predicate2_eqD})
             Jrel_unabs_defs;
 
-        val fold_Jsets = fold_thms lthy Jset_unabs_defs;
-        val dtor_Jset_incl_thmss = map (map fold_Jsets) set_incl_hset_thmss;
-        val dtor_set_Jset_incl_thmsss = map (map (map fold_Jsets)) set_hset_incl_hset_thmsss;
-        val dtor_Jset_induct_thms = map fold_Jsets dtor_hset_induct_thms;
-        val Jwit_thmss = map (map fold_Jsets) wit_thmss;
-
         val Jrels = mk_Jrels passiveAs passiveBs;
         val Jrelphis = map (fn rel => Term.list_comb (rel, Jphis)) Jrels;
         val relphis = map (fn rel => Term.list_comb (rel, Jphis @ Jrelphis)) rels;
@@ -2413,6 +2269,140 @@
 
         val timer = time (timer "helpers for BNF properties");
 
+        fun close_wit I wit = (I, fold_rev Term.absfree (map (nth ys') I) wit);
+
+        val all_unitTs = replicate live HOLogic.unitT;
+        val unitTs = replicate n HOLogic.unitT;
+        val unit_funs = replicate n (Term.absdummy HOLogic.unitT HOLogic.unit);
+        fun mk_map_args I =
+          map (fn i =>
+            if member (op =) I i then Term.absdummy HOLogic.unitT (nth ys i)
+            else mk_undefined (HOLogic.unitT --> nth passiveAs i))
+          (0 upto (m - 1));
+
+        fun mk_nat_wit Ds bnf (I, wit) () =
+          let
+            val passiveI = filter (fn i => i < m) I;
+            val map_args = mk_map_args passiveI;
+          in
+            Term.absdummy HOLogic.unitT (Term.list_comb
+              (mk_map_of_bnf Ds all_unitTs (passiveAs @ unitTs) bnf, map_args @ unit_funs) $ wit)
+          end;
+
+        fun mk_dummy_wit Ds bnf I =
+          let
+            val map_args = mk_map_args I;
+          in
+            Term.absdummy HOLogic.unitT (Term.list_comb
+              (mk_map_of_bnf Ds all_unitTs (passiveAs @ unitTs) bnf, map_args @ unit_funs) $
+              mk_undefined (mk_T_of_bnf Ds all_unitTs bnf))
+          end;
+
+        val nat_witss =
+          map2 (fn Ds => fn bnf => mk_wits_of_bnf (replicate (nwits_of_bnf bnf) Ds)
+            (replicate (nwits_of_bnf bnf) (replicate live HOLogic.unitT)) bnf
+            |> map (fn (I, wit) =>
+              (I, Lazy.lazy (mk_nat_wit Ds bnf (I, Term.list_comb (wit, map (K HOLogic.unit) I))))))
+          Dss bnfs;
+
+        val nat_wit_thmss = map2 (curry op ~~) nat_witss (map wit_thmss_of_bnf bnfs)
+
+        val Iss = map (map fst) nat_witss;
+
+        fun filter_wits (I, wit) =
+          let val J = filter (fn i => i < m) I;
+          in (J, (length J < length I, wit)) end;
+
+        val wit_treess = map_index (fn (i, Is) =>
+          map_index (finish Iss m [i+m] (i+m)) Is) Iss
+          |> map (minimize_wits o map filter_wits o minimize_wits o flat);
+
+        val coind_wit_argsss =
+          map (map (tree_to_coind_wits nat_wit_thmss o snd o snd) o filter (fst o snd)) wit_treess;
+
+        val nonredundant_coind_wit_argsss =
+          fold (fn i => fn argsss =>
+            nth_map (i - 1) (filter_out (fn xs =>
+              exists (fn ys =>
+                let
+                  val xs' = (map (fst o fst) xs, snd (fst (hd xs)));
+                  val ys' = (map (fst o fst) ys, snd (fst (hd ys)));
+                in
+                  eq_pair (subset (op =)) (eq_set (op =)) (xs', ys') andalso not (fst xs' = fst ys')
+                end)
+              (flat argsss)))
+            argsss)
+          ks coind_wit_argsss;
+
+        fun prepare_args args =
+          let
+            val I = snd (fst (hd args));
+            val (dummys, args') =
+              map_split (fn i =>
+                (case find_first (fn arg => fst (fst arg) = i - 1) args of
+                  SOME (_, ((_, wit), thms)) => (NONE, (Lazy.force wit, thms))
+                | NONE =>
+                  (SOME (i - 1), (mk_dummy_wit (nth Dss (i - 1)) (nth bnfs (i - 1)) I, []))))
+              ks;
+          in
+            ((I, dummys), apsnd flat (split_list args'))
+          end;
+
+        fun mk_coind_wits ((I, dummys), (args, thms)) =
+          ((I, dummys), (map (fn i => mk_unfold Ts args i $ HOLogic.unit) ks, thms));
+
+        val coind_witss =
+          maps (map (mk_coind_wits o prepare_args)) nonredundant_coind_wit_argsss;
+
+        val witss = map2 (fn Ds => fn bnf => mk_wits_of_bnf
+          (replicate (nwits_of_bnf bnf) Ds)
+          (replicate (nwits_of_bnf bnf) (passiveAs @ Ts)) bnf) Dss bnfs;
+
+        val ctor_witss =
+          map (map (uncurry close_wit o tree_to_ctor_wit ys ctors witss o snd o snd) o
+            filter_out (fst o snd)) wit_treess;
+
+        fun mk_coind_wit_thms ((I, dummys), (wits, wit_thms)) =
+          let
+            fun mk_goal sets y y_copy y'_copy j =
+              let
+                fun mk_conjunct set z dummy wit =
+                  mk_Ball (set $ z) (Term.absfree y'_copy
+                    (if dummy = NONE orelse member (op =) I (j - 1) then
+                      HOLogic.mk_imp (HOLogic.mk_eq (z, wit),
+                        if member (op =) I (j - 1) then HOLogic.mk_eq (y_copy, y)
+                        else @{term False})
+                    else @{term True}));
+              in
+                fold_rev Logic.all (map (nth ys) I @ Jzs) (HOLogic.mk_Trueprop
+                  (Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct sets Jzs dummys wits)))
+              end;
+            val goals = map5 mk_goal Jsetss_by_range ys ys_copy ys'_copy ls;
+          in
+            map2 (fn goal => fn induct =>
+              Goal.prove_sorry lthy [] [] goal
+                (fn {context = ctxt, prems = _} => mk_coind_wit_tac ctxt induct dtor_unfold_thms
+                  (flat set_mapss) wit_thms)
+              |> Thm.close_derivation)
+            goals dtor_Jset_induct_thms
+            |> map split_conj_thm
+            |> transpose
+            |> map (map_filter (try (fn thm => thm RS bspec RS mp)))
+            |> curry op ~~ (map_index Library.I (map (close_wit I) wits))
+            |> filter (fn (_, thms) => length thms = m)
+          end;
+
+        val coind_wit_thms = maps mk_coind_wit_thms coind_witss;
+
+        val (wit_thmss, all_witss) =
+          fold (fn ((i, wit), thms) => fn witss =>
+            nth_map i (fn (thms', wits) => (thms @ thms', wit :: wits)) witss)
+          coind_wit_thms (map (pair []) ctor_witss)
+          |> map (apsnd (map snd o minimize_wits))
+          |> split_list;
+
+        val timer = time (timer "witnesses");
+
         val map_id0_tacs =
           map2 (K oo mk_map_id0_tac Jmap_thms) dtor_unfold_unique_thms unfold_dtor_thms;
         val map_comp0_tacs = map (fn thm => K (rtac (thm RS sym) 1)) Jmap_comp0_thms;
@@ -2439,17 +2429,17 @@
         val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss
           bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs;
 
-        fun wit_tac thms ctxt = unfold_thms_tac ctxt (flat Jwit_defss) THEN
+        fun wit_tac thms ctxt =
           mk_wit_tac ctxt n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms;
 
         val (Jbnfs, lthy) =
-          fold_map7 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn Jwit_thms =>
+          fold_map7 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn wit_thms =>
               fn consts => fn lthy =>
-            bnf_def Do_Inline (user_policy Note_Some) false I tacs (wit_tac Jwit_thms) (SOME deads)
-              map_b rel_b set_bs consts lthy
+            bnf_def Hardly_Inline (user_policy Note_Some) false I tacs (wit_tac wit_thms)
+              (SOME deads) map_b rel_b set_bs consts lthy
             |> register_bnf (Local_Theory.full_name lthy b))
-          bs tacss map_bs rel_bs set_bss Jwit_thmss
-          ((((((bs ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~ Jwitss) ~~ map SOME Jrels)
+          bs tacss map_bs rel_bs set_bss wit_thmss
+          ((((((bs ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~ all_witss) ~~ map SOME Jrels)
           lthy;
 
         val timer = time (timer "registered new codatatypes as BNFs");
diff -r 01fb1b35433b -r 2666cd7d380c src/HOL/Tools/BNF/bnf_gfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Mon Mar 17 20:54:41 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Mon Mar 17 21:56:32 2014 +0100
@@ -32,7 +32,7 @@
     thm -> thm -> thm list -> thm list -> thm list list -> tactic
   val mk_dtor_o_ctor_tac: Proof.context -> thm -> thm -> thm -> thm -> thm list -> tactic
   val mk_equiv_lsbis_tac: thm -> thm -> thm -> thm -> thm -> thm -> tactic
-  val mk_hset_minimal_tac: Proof.context -> int -> thm -> tactic
+  val mk_Jset_minimal_tac: Proof.context -> int -> thm -> tactic
   val mk_col_minimal_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
     tactic
   val mk_incl_lsbis_tac: int -> int -> thm -> tactic
@@ -75,10 +75,10 @@
   val mk_set_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
     thm list -> thm list list -> tactic
   val mk_set_bd_tac: thm -> thm -> tactic
-  val mk_set_hset_incl_hset_tac: int -> thm -> int -> tactic
+  val mk_set_Jset_incl_Jset_tac: int -> thm -> int -> tactic
   val mk_set_image_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list ->
     thm list -> thm list -> thm list list -> thm list list -> tactic
-  val mk_set_incl_hset_tac: thm -> tactic
+  val mk_set_incl_Jset_tac: thm -> tactic
   val mk_set_ge_tac: int  -> thm -> thm list -> tactic
   val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic
   val mk_set_map0_tac: thm -> tactic
@@ -162,11 +162,11 @@
 fun mk_mor_case_sum_tac ks mor_UNIV =
   (rtac (mor_UNIV RS iffD2) THEN' CONJ_WRAP' (K (rtac @{thm case_sum_o_inj(1)[symmetric]})) ks) 1;
 
-fun mk_set_incl_hset_tac rec_Suc =
+fun mk_set_incl_Jset_tac rec_Suc =
   EVERY' (map rtac [@{thm SUP_upper2}, UNIV_I, @{thm ord_le_eq_trans}, @{thm Un_upper1}, sym,
     rec_Suc]) 1;
 
-fun mk_set_hset_incl_hset_tac n rec_Suc i =
+fun mk_set_Jset_incl_Jset_tac n rec_Suc i =
   EVERY' (map rtac [@{thm UN_least}, subsetI, @{thm UN_I}, UNIV_I, set_mp, equalityD2, rec_Suc,
       UnI2, mk_UnIN n i] @ [etac @{thm UN_I}, atac]) 1;
 
@@ -185,7 +185,7 @@
             rtac subset_trans, atac, Goal.assume_rule_tac ctxt])) rec_0s])
       rec_Sucs] 1;
 
-fun mk_hset_minimal_tac ctxt n col_minimal =
+fun mk_Jset_minimal_tac ctxt n col_minimal =
   (CONJ_WRAP' (K (EVERY' [rtac @{thm UN_least}, rtac rev_mp, rtac col_minimal,
     EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac impI,
     REPEAT_DETERM o eresolve_tac [allE, conjE], atac])) (1 upto n)) 1
@@ -777,20 +777,20 @@
     REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),
     rtac map_arg_cong, rtac (o_apply RS sym)] 1;
 
-fun mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss =
-  EVERY' [rtac hset_minimal,
+fun mk_set_le_tac n Jset_minimal set_Jsets set_Jset_Jsetss =
+  EVERY' [rtac Jset_minimal,
     REPEAT_DETERM_N n o rtac @{thm Un_upper1},
     REPEAT_DETERM_N n o
-      EVERY' (map3 (fn i => fn set_hset => fn set_hset_hsets =>
+      EVERY' (map3 (fn i => fn set_Jset => fn set_Jset_Jsets =>
         EVERY' [rtac subsetI, rtac @{thm UnI2}, rtac (mk_UnIN n i), etac @{thm UN_I},
-          etac UnE, etac set_hset, REPEAT_DETERM_N (n - 1) o etac UnE,
-          EVERY' (map (fn thm => EVERY' [etac @{thm UN_E}, etac thm, atac]) set_hset_hsets)])
-      (1 upto n) set_hsets set_hset_hsetss)] 1;
+          etac UnE, etac set_Jset, REPEAT_DETERM_N (n - 1) o etac UnE,
+          EVERY' (map (fn thm => EVERY' [etac @{thm UN_E}, etac thm, atac]) set_Jset_Jsets)])
+      (1 upto n) set_Jsets set_Jset_Jsetss)] 1;
 
-fun mk_set_ge_tac n set_incl_hset set_hset_incl_hsets =
-  EVERY' [rtac @{thm Un_least}, rtac set_incl_hset,
+fun mk_set_ge_tac n set_incl_Jset set_Jset_incl_Jsets =
+  EVERY' [rtac @{thm Un_least}, rtac set_incl_Jset,
     REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least},
-    EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_hset_incl_hsets)] 1;
+    EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_Jset_incl_Jsets)] 1;
 
 fun mk_map_id0_tac maps unfold_unique unfold_dtor =
   EVERY' [rtac (unfold_unique RS trans), EVERY' (map (rtac o mk_sym) maps),
@@ -807,15 +807,15 @@
         @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl]]))
     maps map_comp0s)] 1;
 
-fun mk_mcong_tac ctxt m coinduct_tac map_comps dtor_maps map_cong0s set_map0ss set_hsetss
-  set_hset_hsetsss in_rels =
+fun mk_mcong_tac ctxt m coinduct_tac map_comps dtor_maps map_cong0s set_map0ss set_Jsetss
+  set_Jset_Jsetsss in_rels =
   let
     val n = length map_comps;
     val ks = 1 upto n;
   in
     EVERY' ([rtac rev_mp, coinduct_tac] @
-      maps (fn ((((((map_comp_trans, dtor_maps_trans), map_cong0), set_map0s), set_hsets),
-        set_hset_hsetss), in_rel) =>
+      maps (fn ((((((map_comp_trans, dtor_maps_trans), map_cong0), set_map0s), set_Jsets),
+        set_Jset_Jsetss), in_rel) =>
         [REPEAT_DETERM o resolve_tac [allI, impI, in_rel RS iffD2],
          REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt, rtac exI,
          rtac (Drule.rotate_prems 1 conjI),
@@ -823,25 +823,25 @@
          REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac @{thm fst_conv}),
          REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym,
          rtac map_comp_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
-         EVERY' (maps (fn set_hset =>
+         EVERY' (maps (fn set_Jset =>
            [rtac o_apply_trans_sym, rtac (@{thm snd_conv} RS trans), etac CollectE,
-           REPEAT_DETERM o etac conjE, etac bspec, etac set_hset]) set_hsets),
+           REPEAT_DETERM o etac conjE, etac bspec, etac set_Jset]) set_Jsets),
          REPEAT_DETERM_N n o rtac snd_convol_fun_cong_sym,
          rtac CollectI,
          EVERY' (map (fn set_map0 => EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map0,
            rtac @{thm image_subsetI}, rtac CollectI, rtac @{thm case_prodI}, rtac refl])
         (take m set_map0s)),
-         CONJ_WRAP' (fn (set_map0, set_hset_hsets) =>
+         CONJ_WRAP' (fn (set_map0, set_Jset_Jsets) =>
            EVERY' [rtac ord_eq_le_trans, rtac set_map0,
              rtac @{thm image_subsetI}, rtac CollectI, rtac @{thm case_prodI}, rtac exI, rtac conjI,
              rtac CollectI, etac CollectE,
              REPEAT_DETERM o etac conjE,
-             CONJ_WRAP' (fn set_hset_hset =>
-               EVERY' [rtac ballI, etac bspec, etac set_hset_hset, atac]) set_hset_hsets,
+             CONJ_WRAP' (fn set_Jset_Jset =>
+               EVERY' [rtac ballI, etac bspec, etac set_Jset_Jset, atac]) set_Jset_Jsets,
              rtac (conjI OF [refl, refl])])
-           (drop m set_map0s ~~ set_hset_hsetss)])
+           (drop m set_map0s ~~ set_Jset_Jsetss)])
         (map (fn th => th RS trans) map_comps ~~ map (fn th => th RS trans) dtor_maps ~~
-          map_cong0s ~~ set_map0ss ~~ set_hsetss ~~ set_hset_hsetsss ~~ in_rels) @
+          map_cong0s ~~ set_map0ss ~~ set_Jsetss ~~ set_Jset_Jsetsss ~~ in_rels) @
       [rtac impI,
        CONJ_WRAP' (fn k =>
          EVERY' [rtac impI, dtac (mk_conjunctN n k), etac mp, rtac exI, rtac conjI, etac CollectI,
diff -r 01fb1b35433b -r 2666cd7d380c src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Mon Mar 17 20:54:41 2014 +0100
+++ b/src/HOL/Transcendental.thy	Mon Mar 17 21:56:32 2014 +0100
@@ -1383,7 +1383,7 @@
     hence "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)"
       unfolding One_nat_def by auto
     hence "DERIV (\<lambda>x. suminf (?f (x - 1))) x :> suminf (?f' x)"
-      unfolding DERIV_iff repos .
+      unfolding deriv_def repos .
     ultimately have "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> (suminf (?f' x) - suminf (?f' x))"
       by (rule DERIV_diff)
     thus "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> 0" by auto
@@ -2485,8 +2485,8 @@
   fix x y
   assume x: "0 \<le> x \<and> x \<le> 2 \<and> cos x = 0"
   assume y: "0 \<le> y \<and> y \<le> 2 \<and> cos y = 0"
-  have [simp]: "\<forall>x. cos differentiable x"
-    unfolding differentiable_def by (auto intro: DERIV_cos)
+  have [simp]: "\<forall>x. cos differentiable (at x)"
+    unfolding real_differentiable_def by (auto intro: DERIV_cos)
   from x y show "x = y"
     apply (cut_tac less_linear [of x y], auto)
     apply (drule_tac f = cos in Rolle)
@@ -2661,8 +2661,8 @@
   fix a b
   assume a: "0 \<le> a \<and> a \<le> pi \<and> cos a = y"
   assume b: "0 \<le> b \<and> b \<le> pi \<and> cos b = y"
-  have [simp]: "\<forall>x. cos differentiable x"
-    unfolding differentiable_def by (auto intro: DERIV_cos)
+  have [simp]: "\<forall>x. cos differentiable (at x)"
+    unfolding real_differentiable_def by (auto intro: DERIV_cos)
   from a b show "a = b"
     apply (cut_tac less_linear [of a b], auto)
     apply (drule_tac f = cos in Rolle)
@@ -2949,7 +2949,7 @@
   apply (rule_tac [4] Rolle)
   apply (rule_tac [2] Rolle)
   apply (auto del: exI intro!: DERIV_tan DERIV_isCont exI
-              simp add: differentiable_def)
+              simp add: real_differentiable_def)
   txt{*Now, simulate TRYALL*}
   apply (rule_tac [!] DERIV_tan asm_rl)
   apply (auto dest!: DERIV_unique [OF _ DERIV_tan]