--- 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
--- 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
--- 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
--- 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' .
--- 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
--- 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)"
--- 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
--- 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 *}
--- 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"
--- 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"
--- 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");
--- 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,
--- 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]