--- a/src/HOL/Conditional_Complete_Lattices.thy Tue Apr 09 21:22:15 2013 +0200
+++ b/src/HOL/Conditional_Complete_Lattices.thy Tue Apr 09 21:39:55 2013 +0200
@@ -1,6 +1,6 @@
(* Title: HOL/Conditional_Complete_Lattices.thy
Author: Amine Chaieb and L C Paulson, University of Cambridge
- Author: Johanens Hölzl, TU München
+ Author: Johannes Hölzl, TU München
*)
header {* Conditional Complete Lattices *}
--- a/src/HOL/Deriv.thy Tue Apr 09 21:22:15 2013 +0200
+++ b/src/HOL/Deriv.thy Tue Apr 09 21:39:55 2013 +0200
@@ -1,6 +1,7 @@
(* Title : Deriv.thy
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
+ Author : Brian Huffman
Conversion to Isar and new proofs by Lawrence C Paulson, 2004
GMVT by Benjamin Porter, 2005
*)
@@ -11,102 +12,703 @@
imports Limits
begin
-text{*Standard Definitions*}
+definition
+ -- {* Frechet derivative: D is derivative of function f at x within s *}
+ has_derivative :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> bool"
+ (infixl "(has'_derivative)" 12)
+where
+ "(f has_derivative f') F \<longleftrightarrow>
+ (bounded_linear f' \<and>
+ ((\<lambda>y. ((f y - f (Lim F (\<lambda>x. x))) - f' (y - Lim F (\<lambda>x. x))) /\<^sub>R norm (y - Lim F (\<lambda>x. x))) ---> 0) F)"
+
+lemma FDERIV_eq_rhs: "(f has_derivative f') F \<Longrightarrow> f' = g' \<Longrightarrow> (f has_derivative g') F"
+ by simp
+
+ML {*
+
+structure FDERIV_Intros = Named_Thms
+(
+ val name = @{binding FDERIV_intros}
+ val description = "introduction rules for FDERIV"
+)
+
+*}
+
+setup {*
+ FDERIV_Intros.setup #>
+ Global_Theory.add_thms_dynamic (@{binding FDERIV_eq_intros},
+ map_filter (try (fn thm => @{thm FDERIV_eq_rhs} OF [thm])) o FDERIV_Intros.get o Context.proof_of);
+*}
+
+lemma FDERIV_bounded_linear: "(f has_derivative f') F \<Longrightarrow> bounded_linear f'"
+ by (simp add: has_derivative_def)
+
+lemma FDERIV_ident[FDERIV_intros, simp]: "((\<lambda>x. x) has_derivative (\<lambda>x. x)) F"
+ by (simp add: has_derivative_def tendsto_const)
+
+lemma FDERIV_const[FDERIV_intros, simp]: "((\<lambda>x. c) has_derivative (\<lambda>x. 0)) F"
+ by (simp add: has_derivative_def tendsto_const)
+
+lemma (in bounded_linear) bounded_linear: "bounded_linear f" ..
+
+lemma (in bounded_linear) FDERIV:
+ "(g has_derivative g') F \<Longrightarrow> ((\<lambda>x. f (g x)) has_derivative (\<lambda>x. f (g' x))) F"
+ using assms unfolding has_derivative_def
+ apply safe
+ apply (erule bounded_linear_compose [OF local.bounded_linear])
+ apply (drule local.tendsto)
+ apply (simp add: local.scaleR local.diff local.add local.zero)
+ done
+
+lemmas FDERIV_scaleR_right [FDERIV_intros] =
+ bounded_linear.FDERIV [OF bounded_linear_scaleR_right]
+
+lemmas FDERIV_scaleR_left [FDERIV_intros] =
+ bounded_linear.FDERIV [OF bounded_linear_scaleR_left]
+
+lemmas FDERIV_mult_right [FDERIV_intros] =
+ bounded_linear.FDERIV [OF bounded_linear_mult_right]
+
+lemmas FDERIV_mult_left [FDERIV_intros] =
+ bounded_linear.FDERIV [OF bounded_linear_mult_left]
+
+lemma FDERIV_add[simp, FDERIV_intros]:
+ assumes f: "(f has_derivative f') F" and g: "(g has_derivative g') F"
+ shows "((\<lambda>x. f x + g x) has_derivative (\<lambda>x. f' x + g' x)) F"
+ unfolding has_derivative_def
+proof safe
+ let ?x = "Lim F (\<lambda>x. x)"
+ let ?D = "\<lambda>f f' y. ((f y - f ?x) - f' (y - ?x)) /\<^sub>R norm (y - ?x)"
+ have "((\<lambda>x. ?D f f' x + ?D g g' x) ---> (0 + 0)) F"
+ using f g by (intro tendsto_add) (auto simp: has_derivative_def)
+ then show "(?D (\<lambda>x. f x + g x) (\<lambda>x. f' x + g' x) ---> 0) F"
+ by (simp add: field_simps scaleR_add_right scaleR_diff_right)
+qed (blast intro: bounded_linear_add f g FDERIV_bounded_linear)
+
+lemma FDERIV_setsum[simp, FDERIV_intros]:
+ assumes f: "\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) F"
+ shows "((\<lambda>x. \<Sum>i\<in>I. f i x) has_derivative (\<lambda>x. \<Sum>i\<in>I. f' i x)) F"
+proof cases
+ assume "finite I" from this f show ?thesis
+ by induct (simp_all add: f)
+qed simp
+
+lemma FDERIV_minus[simp, FDERIV_intros]: "(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. - f x) has_derivative (\<lambda>x. - f' x)) F"
+ using FDERIV_scaleR_right[of f f' F "-1"] by simp
+
+lemma FDERIV_diff[simp, FDERIV_intros]:
+ "(f has_derivative f') F \<Longrightarrow> (g has_derivative g') F \<Longrightarrow> ((\<lambda>x. f x - g x) has_derivative (\<lambda>x. f' x - g' x)) F"
+ by (simp only: diff_minus FDERIV_add FDERIV_minus)
+
+abbreviation
+ -- {* Frechet derivative: D is derivative of function f at x within s *}
+ FDERIV :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
+ ("(FDERIV (_)/ (_)/ : (_)/ :> (_))" [1000, 1000, 1000, 60] 60)
+where
+ "FDERIV f x : s :> f' \<equiv> (f has_derivative f') (at x within s)"
+
+abbreviation
+ fderiv_at ::
+ "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
+ ("(FDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
+where
+ "FDERIV f x :> D \<equiv> FDERIV f x : UNIV :> D"
+
+lemma FDERIV_def:
+ "FDERIV f x : s :> f' \<longleftrightarrow>
+ (bounded_linear f' \<and> ((\<lambda>y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) ---> 0) (at x within s))"
+ by (cases "at x within s = bot") (simp_all add: has_derivative_def Lim_ident_at)
+
+lemma FDERIV_iff_norm:
+ "FDERIV f x : s :> f' \<longleftrightarrow>
+ (bounded_linear f' \<and> ((\<lambda>y. norm ((f y - f x) - f' (y - x)) / norm (y - x)) ---> 0) (at x within s))"
+ using tendsto_norm_zero_iff[of _ "at x within s", where 'b="'b", symmetric]
+ by (simp add: FDERIV_def divide_inverse ac_simps)
+
+lemma fderiv_def:
+ "FDERIV f x :> D = (bounded_linear D \<and> (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0)"
+ unfolding FDERIV_iff_norm LIM_offset_zero_iff[of _ _ x] by simp
+
+lemma field_fderiv_def:
+ fixes x :: "'a::real_normed_field"
+ shows "FDERIV f x :> (\<lambda>h. h * D) = (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
+ apply (unfold fderiv_def)
+ apply (simp add: bounded_linear_mult_left)
+ apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
+ apply (subst diff_divide_distrib)
+ apply (subst times_divide_eq_left [symmetric])
+ apply (simp cong: LIM_cong)
+ apply (simp add: tendsto_norm_zero_iff LIM_zero_iff)
+ done
+
+lemma FDERIV_I:
+ "bounded_linear f' \<Longrightarrow> ((\<lambda>y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) ---> 0) (at x within s) \<Longrightarrow>
+ FDERIV f x : s :> f'"
+ by (simp add: FDERIV_def)
+
+lemma FDERIV_I_sandwich:
+ assumes e: "0 < e" and bounded: "bounded_linear f'"
+ and sandwich: "(\<And>y. y \<in> s \<Longrightarrow> y \<noteq> x \<Longrightarrow> dist y x < e \<Longrightarrow> norm ((f y - f x) - f' (y - x)) / norm (y - x) \<le> H y)"
+ and "(H ---> 0) (at x within s)"
+ shows "FDERIV f x : s :> f'"
+ unfolding FDERIV_iff_norm
+proof safe
+ show "((\<lambda>y. norm (f y - f x - f' (y - x)) / norm (y - x)) ---> 0) (at x within s)"
+ proof (rule tendsto_sandwich[where f="\<lambda>x. 0"])
+ show "(H ---> 0) (at x within s)" by fact
+ show "eventually (\<lambda>n. norm (f n - f x - f' (n - x)) / norm (n - x) \<le> H n) (at x within s)"
+ unfolding eventually_at using e sandwich by auto
+ qed (auto simp: le_divide_eq tendsto_const)
+qed fact
+
+lemma FDERIV_subset: "FDERIV f x : s :> f' \<Longrightarrow> t \<subseteq> s \<Longrightarrow> FDERIV f x : t :> f'"
+ by (auto simp add: FDERIV_iff_norm intro: tendsto_within_subset)
+
+subsection {* Continuity *}
+
+lemma FDERIV_continuous:
+ assumes f: "FDERIV f x : s :> f'"
+ shows "continuous (at x within s) f"
+proof -
+ from f interpret F: bounded_linear f' by (rule FDERIV_bounded_linear)
+ note F.tendsto[tendsto_intros]
+ let ?L = "\<lambda>f. (f ---> 0) (at x within s)"
+ have "?L (\<lambda>y. norm ((f y - f x) - f' (y - x)) / norm (y - x))"
+ using f unfolding FDERIV_iff_norm by blast
+ then have "?L (\<lambda>y. norm ((f y - f x) - f' (y - x)) / norm (y - x) * norm (y - x))" (is ?m)
+ by (rule tendsto_mult_zero) (auto intro!: tendsto_eq_intros)
+ also have "?m \<longleftrightarrow> ?L (\<lambda>y. norm ((f y - f x) - f' (y - x)))"
+ by (intro filterlim_cong) (simp_all add: eventually_at_filter)
+ finally have "?L (\<lambda>y. (f y - f x) - f' (y - x))"
+ by (rule tendsto_norm_zero_cancel)
+ then have "?L (\<lambda>y. ((f y - f x) - f' (y - x)) + f' (y - x))"
+ by (rule tendsto_eq_intros) (auto intro!: tendsto_eq_intros simp: F.zero)
+ then have "?L (\<lambda>y. f y - f x)"
+ by simp
+ from tendsto_add[OF this tendsto_const, of "f x"] show ?thesis
+ by (simp add: continuous_within)
+qed
+
+subsection {* Composition *}
+
+lemma tendsto_at_iff_tendsto_nhds_within: "f x = y \<Longrightarrow> (f ---> y) (at x within s) \<longleftrightarrow> (f ---> y) (inf (nhds x) (principal s))"
+ unfolding tendsto_def eventually_inf_principal eventually_at_filter
+ by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1)
+
+lemma FDERIV_in_compose:
+ assumes f: "FDERIV f x : s :> f'"
+ assumes g: "FDERIV g (f x) : (f`s) :> g'"
+ shows "FDERIV (\<lambda>x. g (f x)) x : s :> (\<lambda>x. g' (f' x))"
+proof -
+ from f interpret F: bounded_linear f' by (rule FDERIV_bounded_linear)
+ from g interpret G: bounded_linear g' by (rule FDERIV_bounded_linear)
+ from F.bounded obtain kF where kF: "\<And>x. norm (f' x) \<le> norm x * kF" by fast
+ from G.bounded obtain kG where kG: "\<And>x. norm (g' x) \<le> norm x * kG" by fast
+ note G.tendsto[tendsto_intros]
+
+ let ?L = "\<lambda>f. (f ---> 0) (at x within s)"
+ let ?D = "\<lambda>f f' x y. (f y - f x) - f' (y - x)"
+ let ?N = "\<lambda>f f' x y. norm (?D f f' x y) / norm (y - x)"
+ let ?gf = "\<lambda>x. g (f x)" and ?gf' = "\<lambda>x. g' (f' x)"
+ def Nf \<equiv> "?N f f' x"
+ def Ng \<equiv> "\<lambda>y. ?N g g' (f x) (f y)"
+
+ show ?thesis
+ proof (rule FDERIV_I_sandwich[of 1])
+ show "bounded_linear (\<lambda>x. g' (f' x))"
+ using f g by (blast intro: bounded_linear_compose FDERIV_bounded_linear)
+ next
+ fix y::'a assume neq: "y \<noteq> x"
+ have "?N ?gf ?gf' x y = norm (g' (?D f f' x y) + ?D g g' (f x) (f y)) / norm (y - x)"
+ by (simp add: G.diff G.add field_simps)
+ also have "\<dots> \<le> norm (g' (?D f f' x y)) / norm (y - x) + Ng y * (norm (f y - f x) / norm (y - x))"
+ by (simp add: add_divide_distrib[symmetric] divide_right_mono norm_triangle_ineq G.zero Ng_def)
+ also have "\<dots> \<le> Nf y * kG + Ng y * (Nf y + kF)"
+ proof (intro add_mono mult_left_mono)
+ have "norm (f y - f x) = norm (?D f f' x y + f' (y - x))"
+ by simp
+ also have "\<dots> \<le> norm (?D f f' x y) + norm (f' (y - x))"
+ by (rule norm_triangle_ineq)
+ also have "\<dots> \<le> norm (?D f f' x y) + norm (y - x) * kF"
+ using kF by (intro add_mono) simp
+ finally show "norm (f y - f x) / norm (y - x) \<le> Nf y + kF"
+ by (simp add: neq Nf_def field_simps)
+ qed (insert kG, simp_all add: Ng_def Nf_def neq zero_le_divide_iff field_simps)
+ finally show "?N ?gf ?gf' x y \<le> Nf y * kG + Ng y * (Nf y + kF)" .
+ next
+ have [tendsto_intros]: "?L Nf"
+ using f unfolding FDERIV_iff_norm Nf_def ..
+ from f have "(f ---> f x) (at x within s)"
+ by (blast intro: FDERIV_continuous continuous_within[THEN iffD1])
+ then have f': "LIM x at x within s. f x :> inf (nhds (f x)) (principal (f`s))"
+ unfolding filterlim_def
+ by (simp add: eventually_filtermap eventually_at_filter le_principal)
+
+ have "((?N g g' (f x)) ---> 0) (at (f x) within f`s)"
+ using g unfolding FDERIV_iff_norm ..
+ then have g': "((?N g g' (f x)) ---> 0) (inf (nhds (f x)) (principal (f`s)))"
+ by (rule tendsto_at_iff_tendsto_nhds_within[THEN iffD1, rotated]) simp
+
+ have [tendsto_intros]: "?L Ng"
+ unfolding Ng_def by (rule filterlim_compose[OF g' f'])
+ show "((\<lambda>y. Nf y * kG + Ng y * (Nf y + kF)) ---> 0) (at x within s)"
+ by (intro tendsto_eq_intros) auto
+ qed simp
+qed
+
+lemma FDERIV_compose:
+ "FDERIV f x : s :> f' \<Longrightarrow> FDERIV g (f x) :> g' \<Longrightarrow> FDERIV (\<lambda>x. g (f x)) x : s :> (\<lambda>x. g' (f' x))"
+ by (blast intro: FDERIV_in_compose FDERIV_subset)
+
+lemma (in bounded_bilinear) FDERIV:
+ assumes f: "FDERIV f x : s :> f'" and g: "FDERIV g x : s :> g'"
+ shows "FDERIV (\<lambda>x. f x ** g x) x : s :> (\<lambda>h. f x ** g' h + f' h ** g x)"
+proof -
+ from bounded_linear.bounded [OF FDERIV_bounded_linear [OF f]]
+ obtain KF where norm_F: "\<And>x. norm (f' x) \<le> norm x * KF" by fast
+
+ from pos_bounded obtain K where K: "0 < K" and norm_prod:
+ "\<And>a b. norm (a ** b) \<le> norm a * norm b * K" by fast
+ let ?D = "\<lambda>f f' y. f y - f x - f' (y - x)"
+ let ?N = "\<lambda>f f' y. norm (?D f f' y) / norm (y - x)"
+ def Ng =="?N g g'" and Nf =="?N f f'"
+
+ let ?fun1 = "\<lambda>y. norm (f y ** g y - f x ** g x - (f x ** g' (y - x) + f' (y - x) ** g x)) / norm (y - x)"
+ let ?fun2 = "\<lambda>y. norm (f x) * Ng y * K + Nf y * norm (g y) * K + KF * norm (g y - g x) * K"
+ let ?F = "at x within s"
-definition
- deriv :: "['a::real_normed_field \<Rightarrow> 'a, 'a, 'a] \<Rightarrow> bool"
- --{*Differentiation: D is derivative of function f at x*}
- ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where
- "DERIV f x :> D = ((%h. (f(x + h) - f x) / h) -- 0 --> D)"
+ show ?thesis
+ proof (rule FDERIV_I_sandwich[of 1])
+ show "bounded_linear (\<lambda>h. f x ** g' h + f' h ** g x)"
+ by (intro bounded_linear_add
+ bounded_linear_compose [OF bounded_linear_right] bounded_linear_compose [OF bounded_linear_left]
+ FDERIV_bounded_linear [OF g] FDERIV_bounded_linear [OF f])
+ next
+ from g have "(g ---> g x) ?F"
+ by (intro continuous_within[THEN iffD1] FDERIV_continuous)
+ moreover from f g have "(Nf ---> 0) ?F" "(Ng ---> 0) ?F"
+ by (simp_all add: FDERIV_iff_norm Ng_def Nf_def)
+ ultimately have "(?fun2 ---> norm (f x) * 0 * K + 0 * norm (g x) * K + KF * norm (0::'b) * K) ?F"
+ by (intro tendsto_intros) (simp_all add: LIM_zero_iff)
+ then show "(?fun2 ---> 0) ?F"
+ by simp
+ next
+ fix y::'d assume "y \<noteq> x"
+ have "?fun1 y = norm (f x ** ?D g g' y + ?D f f' y ** g y + f' (y - x) ** (g y - g x)) / norm (y - x)"
+ by (simp add: diff_left diff_right add_left add_right field_simps)
+ also have "\<dots> \<le> (norm (f x) * norm (?D g g' y) * K + norm (?D f f' y) * norm (g y) * K +
+ norm (y - x) * KF * norm (g y - g x) * K) / norm (y - x)"
+ by (intro divide_right_mono mult_mono'
+ order_trans [OF norm_triangle_ineq add_mono]
+ order_trans [OF norm_prod mult_right_mono]
+ mult_nonneg_nonneg order_refl norm_ge_zero norm_F
+ K [THEN order_less_imp_le])
+ also have "\<dots> = ?fun2 y"
+ by (simp add: add_divide_distrib Ng_def Nf_def)
+ finally show "?fun1 y \<le> ?fun2 y" .
+ qed simp
+qed
+
+lemmas FDERIV_mult[simp, FDERIV_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_mult]
+lemmas FDERIV_scaleR[simp, FDERIV_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_scaleR]
+
+lemma FDERIV_setprod[simp, FDERIV_intros]:
+ fixes f :: "'i \<Rightarrow> 'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
+ assumes f: "\<And>i. i \<in> I \<Longrightarrow> FDERIV (f i) x : s :> f' i"
+ shows "FDERIV (\<lambda>x. \<Prod>i\<in>I. f i x) x : s :> (\<lambda>y. \<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {i}. f j x))"
+proof cases
+ assume "finite I" from this f show ?thesis
+ proof induct
+ case (insert i I)
+ let ?P = "\<lambda>y. f i x * (\<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {i}. f j x)) + (f' i y) * (\<Prod>i\<in>I. f i x)"
+ have "FDERIV (\<lambda>x. f i x * (\<Prod>i\<in>I. f i x)) x : s :> ?P"
+ using insert by (intro FDERIV_mult) auto
+ also have "?P = (\<lambda>y. \<Sum>i'\<in>insert i I. f' i' y * (\<Prod>j\<in>insert i I - {i'}. f j x))"
+ using insert(1,2) by (auto simp add: setsum_right_distrib insert_Diff_if intro!: ext setsum_cong)
+ finally show ?case
+ using insert by simp
+ qed simp
+qed simp
+
+lemma FDERIV_power[simp, FDERIV_intros]:
+ fixes f :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
+ assumes f: "FDERIV f x : s :> f'"
+ shows "FDERIV (\<lambda>x. f x^n) x : s :> (\<lambda>y. of_nat n * f' y * f x^(n - 1))"
+ using FDERIV_setprod[OF f, of "{..< n}"] by (simp add: setprod_constant ac_simps)
+
+lemma FDERIV_inverse':
+ fixes x :: "'a::real_normed_div_algebra"
+ assumes x: "x \<noteq> 0"
+ shows "FDERIV inverse x : s :> (\<lambda>h. - (inverse x * h * inverse x))"
+ (is "FDERIV ?inv x : s :> ?f")
+proof (rule FDERIV_I_sandwich)
+ show "bounded_linear (\<lambda>h. - (?inv x * h * ?inv x))"
+ apply (rule bounded_linear_minus)
+ apply (rule bounded_linear_mult_const)
+ apply (rule bounded_linear_const_mult)
+ apply (rule bounded_linear_ident)
+ done
+next
+ show "0 < norm x" using x by simp
+next
+ show "((\<lambda>y. norm (?inv y - ?inv x) * norm (?inv x)) ---> 0) (at x within s)"
+ apply (rule tendsto_mult_left_zero)
+ apply (rule tendsto_norm_zero)
+ apply (rule LIM_zero)
+ apply (rule tendsto_inverse)
+ apply (rule tendsto_ident_at)
+ apply (rule x)
+ done
+next
+ fix y::'a assume h: "y \<noteq> x" "dist y x < norm x"
+ then have "y \<noteq> 0"
+ by (auto simp: norm_conv_dist dist_commute)
+ have "norm (?inv y - ?inv x - ?f (y -x)) / norm (y - x) = norm ((?inv y - ?inv x) * (y - x) * ?inv x) / norm (y - x)"
+ apply (subst inverse_diff_inverse [OF `y \<noteq> 0` x])
+ apply (subst minus_diff_minus)
+ apply (subst norm_minus_cancel)
+ apply (simp add: left_diff_distrib)
+ done
+ also have "\<dots> \<le> norm (?inv y - ?inv x) * norm (y - x) * norm (?inv x) / norm (y - x)"
+ apply (rule divide_right_mono [OF _ norm_ge_zero])
+ apply (rule order_trans [OF norm_mult_ineq])
+ apply (rule mult_right_mono [OF _ norm_ge_zero])
+ apply (rule norm_mult_ineq)
+ done
+ also have "\<dots> = norm (?inv y - ?inv x) * norm (?inv x)"
+ by simp
+ finally show "norm (?inv y - ?inv x - ?f (y -x)) / norm (y - x) \<le>
+ norm (?inv y - ?inv x) * norm (?inv x)" .
+qed
+
+lemma FDERIV_inverse[simp, FDERIV_intros]:
+ fixes f :: "_ \<Rightarrow> 'a::real_normed_div_algebra"
+ assumes x: "f x \<noteq> 0" and f: "FDERIV f x : s :> f'"
+ shows "FDERIV (\<lambda>x. inverse (f x)) x : s :> (\<lambda>h. - (inverse (f x) * f' h * inverse (f x)))"
+ using FDERIV_compose[OF f FDERIV_inverse', OF x] .
+
+lemma FDERIV_divide[simp, FDERIV_intros]:
+ fixes f :: "_ \<Rightarrow> 'a::real_normed_div_algebra"
+ assumes g: "FDERIV g x : s :> g'"
+ assumes x: "f x \<noteq> 0" and f: "FDERIV f x : s :> f'"
+ shows "FDERIV (\<lambda>x. g x / f x) x : s :> (\<lambda>h. - g x * (inverse (f x) * f' h * inverse (f x)) + g' h / f x)"
+ using FDERIV_mult[OF g FDERIV_inverse[OF x f]]
+ by (simp add: divide_inverse)
+
+subsection {* Uniqueness *}
+
+text {*
+
+This can not generally shown for @{const FDERIV}, as we need to approach the point from
+all directions. There is a proof in @{text Multivariate_Analysis} for @{text euclidean_space}.
+
+*}
+
+lemma FDERIV_zero_unique:
+ assumes "FDERIV (\<lambda>x. 0) x :> F" shows "F = (\<lambda>h. 0)"
+proof -
+ interpret F: bounded_linear F
+ using assms by (rule FDERIV_bounded_linear)
+ let ?r = "\<lambda>h. norm (F h) / norm h"
+ have *: "?r -- 0 --> 0"
+ using assms unfolding fderiv_def by simp
+ show "F = (\<lambda>h. 0)"
+ proof
+ fix h show "F h = 0"
+ proof (rule ccontr)
+ assume "F h \<noteq> 0"
+ moreover from this have h: "h \<noteq> 0"
+ by (clarsimp simp add: F.zero)
+ ultimately have "0 < ?r h"
+ by (simp add: divide_pos_pos)
+ from LIM_D [OF * this] obtain s where s: "0 < s"
+ and r: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> ?r x < ?r h" by auto
+ from dense [OF s] obtain t where t: "0 < t \<and> t < s" ..
+ let ?x = "scaleR (t / norm h) h"
+ have "?x \<noteq> 0" and "norm ?x < s" using t h by simp_all
+ hence "?r ?x < ?r h" by (rule r)
+ thus "False" using t h by (simp add: F.scaleR)
+ qed
+ qed
+qed
+
+lemma FDERIV_unique:
+ assumes "FDERIV f x :> F" and "FDERIV f x :> F'" shows "F = F'"
+proof -
+ have "FDERIV (\<lambda>x. 0) x :> (\<lambda>h. F h - F' h)"
+ using FDERIV_diff [OF assms] by simp
+ hence "(\<lambda>h. F h - F' h) = (\<lambda>h. 0)"
+ by (rule FDERIV_zero_unique)
+ thus "F = F'"
+ unfolding fun_eq_iff right_minus_eq .
+qed
+
+subsection {* Differentiability predicate *}
+
+definition isDiff :: "'a filter \<Rightarrow> ('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> bool" where
+ isDiff_def: "isDiff F f \<longleftrightarrow> (\<exists>D. (f has_derivative D) F)"
+
+abbreviation differentiable_in :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool"
+ ("(_) differentiable (_) in (_)" [1000, 1000, 60] 60) where
+ "f differentiable x in s \<equiv> isDiff (at x within s) f"
+
+abbreviation differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool"
+ (infixl "differentiable" 60) where
+ "f differentiable x \<equiv> f differentiable x in UNIV"
+
+lemma differentiable_subset: "f differentiable x in s \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f differentiable x in t"
+ unfolding isDiff_def by (blast intro: FDERIV_subset)
+
+lemma differentiable_ident [simp]: "isDiff F (\<lambda>x. x)"
+ unfolding isDiff_def by (blast intro: FDERIV_ident)
+
+lemma differentiable_const [simp]: "isDiff F (\<lambda>z. a)"
+ unfolding isDiff_def by (blast intro: FDERIV_const)
+
+lemma differentiable_in_compose:
+ "f differentiable (g x) in (g`s) \<Longrightarrow> g differentiable x in s \<Longrightarrow> (\<lambda>x. f (g x)) differentiable x in s"
+ unfolding isDiff_def by (blast intro: FDERIV_in_compose)
+
+lemma differentiable_compose:
+ "f differentiable (g x) \<Longrightarrow> g differentiable x in s \<Longrightarrow> (\<lambda>x. f (g x)) differentiable x in s"
+ by (blast intro: differentiable_in_compose differentiable_subset)
+
+lemma differentiable_sum [simp]:
+ "isDiff F f \<Longrightarrow> isDiff F g \<Longrightarrow> isDiff F (\<lambda>x. f x + g x)"
+ unfolding isDiff_def by (blast intro: FDERIV_add)
+
+lemma differentiable_minus [simp]:
+ "isDiff F f \<Longrightarrow> isDiff F (\<lambda>x. - f x)"
+ unfolding isDiff_def by (blast intro: FDERIV_minus)
+
+lemma differentiable_diff [simp]:
+ "isDiff F f \<Longrightarrow> isDiff F g \<Longrightarrow> isDiff F (\<lambda>x. f x - g x)"
+ unfolding isDiff_def by (blast intro: FDERIV_diff)
+
+lemma differentiable_mult [simp]:
+ fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_algebra"
+ shows "f differentiable x in s \<Longrightarrow> g differentiable x in s \<Longrightarrow> (\<lambda>x. f x * g x) differentiable x in s"
+ unfolding isDiff_def by (blast intro: FDERIV_mult)
+
+lemma differentiable_inverse [simp]:
+ fixes f :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
+ shows "f differentiable x in s \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> (\<lambda>x. inverse (f x)) differentiable x in s"
+ unfolding isDiff_def by (blast intro: FDERIV_inverse)
+
+lemma differentiable_divide [simp]:
+ fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
+ shows "f differentiable x in s \<Longrightarrow> g differentiable x in s \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x / g x) differentiable x in s"
+ unfolding divide_inverse using assms by simp
+
+lemma differentiable_power [simp]:
+ fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
+ shows "f differentiable x in s \<Longrightarrow> (\<lambda>x. f x ^ n) differentiable x in s"
+ unfolding isDiff_def by (blast intro: FDERIV_power)
+
+lemma differentiable_scaleR [simp]:
+ "f differentiable x in s \<Longrightarrow> g differentiable x in s \<Longrightarrow> (\<lambda>x. f x *\<^sub>R g x) differentiable x in s"
+ unfolding isDiff_def by (blast intro: FDERIV_scaleR)
+
+definition
+ -- {*Differentiation: D is derivative of function f at x*}
+ deriv ::
+ "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool"
+ ("(DERIV (_)/ (_)/ : (_)/ :> (_))" [1000, 1000, 1000, 60] 60)
+where
+ deriv_fderiv: "DERIV f x : s :> D = FDERIV f x : s :> (\<lambda>x. x * D)"
+
+abbreviation
+ -- {*Differentiation: D is derivative of function f at x*}
+ deriv_at ::
+ "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+ ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
+where
+ "DERIV f x :> D \<equiv> DERIV f x : UNIV :> D"
+
+lemma differentiable_def: "(f::real \<Rightarrow> real) differentiable x in s \<longleftrightarrow> (\<exists>D. DERIV f x : s :> D)"
+proof safe
+ assume "f differentiable x in s"
+ then obtain f' where "FDERIV f x : s :> f'"
+ unfolding isDiff_def by auto
+ moreover then obtain c where "f' = (\<lambda>x. x * c)"
+ by (metis real_bounded_linear FDERIV_bounded_linear)
+ ultimately show "\<exists>D. DERIV f x : s :> D"
+ unfolding deriv_fderiv by auto
+qed (auto simp: isDiff_def deriv_fderiv)
+
+lemma differentiableE [elim?]:
+ fixes f :: "real \<Rightarrow> real"
+ assumes f: "f differentiable x in s" obtains df where "DERIV f x : s :> df"
+ using assms by (auto simp: differentiable_def)
+
+lemma differentiableD: "(f::real \<Rightarrow> real) differentiable x in s \<Longrightarrow> \<exists>D. DERIV f x : s :> D"
+ by (auto elim: differentiableE)
+
+lemma differentiableI: "DERIV f x : s :> D \<Longrightarrow> (f::real \<Rightarrow> real) differentiable x in s"
+ by (force simp add: differentiable_def)
+
+lemma DERIV_I_FDERIV: "FDERIV f x : s :> F \<Longrightarrow> (\<And>x. x * F' = F x) \<Longrightarrow> DERIV f x : s :> F'"
+ by (simp add: deriv_fderiv)
+
+lemma DERIV_D_FDERIV: "DERIV f x : s :> F \<Longrightarrow> FDERIV f x : s :> (\<lambda>x. x * F)"
+ by (simp add: deriv_fderiv)
+
+lemma deriv_def:
+ "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
+ apply (simp add: deriv_fderiv fderiv_def bounded_linear_mult_left LIM_zero_iff[symmetric, of _ D])
+ apply (subst (2) tendsto_norm_zero_iff[symmetric])
+ apply (rule filterlim_cong)
+ apply (simp_all add: eventually_at_filter field_simps nonzero_norm_divide)
+ done
subsection {* Derivatives *}
-lemma DERIV_iff: "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --> D)"
-by (simp add: deriv_def)
+lemma DERIV_iff: "(DERIV f x :> D) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
+ by (simp add: deriv_def)
-lemma DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --> D"
-by (simp add: deriv_def)
+lemma DERIV_D: "DERIV f x :> D \<Longrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
+ by (simp add: deriv_def)
-lemma DERIV_const [simp]: "DERIV (\<lambda>x. k) x :> 0"
- by (simp add: deriv_def tendsto_const)
+lemma DERIV_const [simp]: "DERIV (\<lambda>x. k) x : s :> 0"
+ by (rule DERIV_I_FDERIV[OF FDERIV_const]) auto
-lemma DERIV_ident [simp]: "DERIV (\<lambda>x. x) x :> 1"
- by (simp add: deriv_def tendsto_const cong: LIM_cong)
+lemma DERIV_ident [simp]: "DERIV (\<lambda>x. x) x : s :> 1"
+ by (rule DERIV_I_FDERIV[OF FDERIV_ident]) auto
-lemma DERIV_add:
- "\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x + g x) x :> D + E"
- by (simp only: deriv_def add_diff_add add_divide_distrib tendsto_add)
+lemma DERIV_add: "DERIV f x : s :> D \<Longrightarrow> DERIV g x : s :> E \<Longrightarrow> DERIV (\<lambda>x. f x + g x) x : s :> D + E"
+ by (rule DERIV_I_FDERIV[OF FDERIV_add]) (auto simp: field_simps dest: DERIV_D_FDERIV)
-lemma DERIV_minus:
- "DERIV f x :> D \<Longrightarrow> DERIV (\<lambda>x. - f x) x :> - D"
- by (simp only: deriv_def minus_diff_minus divide_minus_left tendsto_minus)
+lemma DERIV_minus: "DERIV f x : s :> D \<Longrightarrow> DERIV (\<lambda>x. - f x) x : s :> - D"
+ by (rule DERIV_I_FDERIV[OF FDERIV_minus]) (auto simp: field_simps dest: DERIV_D_FDERIV)
-lemma DERIV_diff:
- "\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x - g x) x :> D - E"
-by (simp only: diff_minus DERIV_add DERIV_minus)
+lemma DERIV_diff: "DERIV f x : s :> D \<Longrightarrow> DERIV g x : s :> E \<Longrightarrow> DERIV (\<lambda>x. f x - g x) x : s :> D - E"
+ by (rule DERIV_I_FDERIV[OF FDERIV_diff]) (auto simp: field_simps dest: DERIV_D_FDERIV)
-lemma DERIV_add_minus:
- "\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x + - g x) x :> D + - E"
-by (simp only: DERIV_add DERIV_minus)
+lemma DERIV_add_minus: "DERIV f x : s :> D \<Longrightarrow> DERIV g x : s :> E \<Longrightarrow> DERIV (\<lambda>x. f x + - g x) x : s :> D + - E"
+ by (simp only: DERIV_add DERIV_minus)
+
+lemma DERIV_continuous: "DERIV f x : s :> D \<Longrightarrow> continuous (at x within s) f"
+ by (drule FDERIV_continuous[OF DERIV_D_FDERIV]) simp
lemma DERIV_isCont: "DERIV f x :> D \<Longrightarrow> isCont f x"
-proof (unfold isCont_iff)
- assume "DERIV f x :> D"
- hence "(\<lambda>h. (f(x+h) - f(x)) / h) -- 0 --> D"
- by (rule DERIV_D)
- hence "(\<lambda>h. (f(x+h) - f(x)) / h * h) -- 0 --> D * 0"
- by (intro tendsto_mult tendsto_ident_at)
- hence "(\<lambda>h. (f(x+h) - f(x)) * (h / h)) -- 0 --> 0"
- by simp
- hence "(\<lambda>h. f(x+h) - f(x)) -- 0 --> 0"
- by (simp cong: LIM_cong)
- thus "(\<lambda>h. f(x+h)) -- 0 --> f(x)"
- by (simp add: LIM_def dist_norm)
-qed
+ by (auto dest!: DERIV_continuous)
+
+lemma DERIV_mult': "DERIV f x : s :> D \<Longrightarrow> DERIV g x : s :> E \<Longrightarrow> DERIV (\<lambda>x. f x * g x) x : s :> f x * E + D * g x"
+ by (rule DERIV_I_FDERIV[OF FDERIV_mult]) (auto simp: field_simps dest: DERIV_D_FDERIV)
-lemma DERIV_mult_lemma:
- fixes a b c d :: "'a::real_field"
- shows "(a * b - c * d) / h = a * ((b - d) / h) + ((a - c) / h) * d"
- by (simp add: field_simps diff_divide_distrib)
+lemma DERIV_mult: "DERIV f x : s :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (\<lambda>x. f x * g x) x : s :> Da * g x + Db * f x"
+ by (rule DERIV_I_FDERIV[OF FDERIV_mult]) (auto simp: field_simps dest: DERIV_D_FDERIV)
+
+text {* Derivative of linear multiplication *}
-lemma DERIV_mult':
- assumes f: "DERIV f x :> D"
- assumes g: "DERIV g x :> E"
- shows "DERIV (\<lambda>x. f x * g x) x :> f x * E + D * g x"
-proof (unfold deriv_def)
- from f have "isCont f x"
- by (rule DERIV_isCont)
- hence "(\<lambda>h. f(x+h)) -- 0 --> f x"
- by (simp only: isCont_iff)
- hence "(\<lambda>h. f(x+h) * ((g(x+h) - g x) / h) +
- ((f(x+h) - f x) / h) * g x)
- -- 0 --> f x * E + D * g x"
- by (intro tendsto_intros DERIV_D f g)
- thus "(\<lambda>h. (f(x+h) * g(x+h) - f x * g x) / h)
- -- 0 --> f x * E + D * g x"
- by (simp only: DERIV_mult_lemma)
-qed
+lemma DERIV_cmult:
+ "DERIV f x : s :> D ==> DERIV (%x. c * f x) x : s :> c*D"
+ by (drule DERIV_mult' [OF DERIV_const], simp)
-lemma DERIV_mult:
- "DERIV f x :> Da \<Longrightarrow> DERIV g x :> Db \<Longrightarrow> DERIV (\<lambda>x. f x * g x) x :> Da * g x + Db * f x"
- by (drule (1) DERIV_mult', simp only: mult_commute add_commute)
+lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x : s :> c"
+ by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp)
+
+lemma DERIV_cdivide: "DERIV f x : s :> D ==> DERIV (%x. f x / c) x : s :> D / c"
+ apply (subgoal_tac "DERIV (%x. (1 / c) * f x) x : s :> (1 / c) * D", force)
+ apply (erule DERIV_cmult)
+ done
lemma DERIV_unique:
- "DERIV f x :> D \<Longrightarrow> DERIV f x :> E \<Longrightarrow> D = E"
+ "DERIV f x :> D \<Longrightarrow> DERIV f x :> E \<Longrightarrow> D = E"
unfolding deriv_def by (rule LIM_unique)
-text{*Differentiation of finite sum*}
+lemma DERIV_setsum':
+ "(\<And> n. n \<in> S \<Longrightarrow> DERIV (%x. f x n) x : s :> (f' x n)) \<Longrightarrow> DERIV (\<lambda>x. setsum (f x) S) x : s :> setsum (f' x) S"
+ by (rule DERIV_I_FDERIV[OF FDERIV_setsum]) (auto simp: setsum_right_distrib dest: DERIV_D_FDERIV)
lemma DERIV_setsum:
- assumes "finite S"
- and "\<And> n. n \<in> S \<Longrightarrow> DERIV (%x. f x n) x :> (f' x n)"
- shows "DERIV (%x. setsum (f x) S) x :> setsum (f' x) S"
- using assms by induct (auto intro!: DERIV_add)
+ "finite S \<Longrightarrow> (\<And> n. n \<in> S \<Longrightarrow> DERIV (%x. f x n) x : s :> (f' x n)) \<Longrightarrow> DERIV (\<lambda>x. setsum (f x) S) x : s :> setsum (f' x) S"
+ by (rule DERIV_setsum')
+
+lemma DERIV_sumr [rule_format (no_asm)]: (* REMOVE *)
+ "(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x : s :> (f' r x))
+ --> DERIV (%x. \<Sum>n=m..<n::nat. f n x :: real) x : s :> (\<Sum>r=m..<n. f' r x)"
+ by (auto intro: DERIV_setsum)
+
+lemma DERIV_inverse':
+ "DERIV f x : s :> D \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> DERIV (\<lambda>x. inverse (f x)) x : s :> - (inverse (f x) * D * inverse (f x))"
+ by (rule DERIV_I_FDERIV[OF FDERIV_inverse]) (auto dest: DERIV_D_FDERIV)
+
+text {* Power of @{text "-1"} *}
+
+lemma DERIV_inverse:
+ "x \<noteq> 0 \<Longrightarrow> DERIV (\<lambda>x. inverse(x)) x : s :> - (inverse x ^ Suc (Suc 0))"
+ by (drule DERIV_inverse' [OF DERIV_ident]) simp
+
+text {* Derivative of inverse *}
+
+lemma DERIV_inverse_fun:
+ "DERIV f x : s :> d \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> DERIV (\<lambda>x. inverse (f x)) x : s :> (- (d * inverse(f x ^ Suc (Suc 0))))"
+ by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib)
+
+text {* Derivative of quotient *}
+
+lemma DERIV_divide:
+ "DERIV f x : s :> D \<Longrightarrow> DERIV g x : s :> E \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow> DERIV (\<lambda>x. f x / g x) x : s :> (D * g x - f x * E) / (g x * g x)"
+ by (rule DERIV_I_FDERIV[OF FDERIV_divide])
+ (auto dest: DERIV_D_FDERIV simp: field_simps nonzero_inverse_mult_distrib divide_inverse)
+
+lemma DERIV_quotient:
+ "DERIV f x : s :> d \<Longrightarrow> DERIV g x : s :> e \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow> DERIV (\<lambda>y. f y / g y) x : s :> (d * g x - (e * f x)) / (g x ^ Suc (Suc 0))"
+ by (drule (2) DERIV_divide) (simp add: mult_commute)
+
+lemma DERIV_power_Suc:
+ "DERIV f x : s :> D \<Longrightarrow> DERIV (\<lambda>x. f x ^ Suc n) x : s :> (1 + of_nat n) * (D * f x ^ n)"
+ by (rule DERIV_I_FDERIV[OF FDERIV_power]) (auto simp: deriv_fderiv)
+
+lemma DERIV_power:
+ "DERIV f x : s :> D \<Longrightarrow> DERIV (\<lambda>x. f x ^ n) x : s :> of_nat n * (D * f x ^ (n - Suc 0))"
+ by (rule DERIV_I_FDERIV[OF FDERIV_power]) (auto simp: deriv_fderiv)
-lemma DERIV_sumr [rule_format (no_asm)]:
- "(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))
- --> DERIV (%x. \<Sum>n=m..<n::nat. f n x :: real) x :> (\<Sum>r=m..<n. f' r x)"
- by (auto intro: DERIV_setsum)
+lemma DERIV_pow: "DERIV (%x. x ^ n) x : s :> real n * (x ^ (n - Suc 0))"
+ apply (cut_tac DERIV_power [OF DERIV_ident])
+ apply (simp add: real_of_nat_def)
+ done
+
+lemma DERIV_chain': "DERIV f x : s :> D \<Longrightarrow> DERIV g (f x) :> E \<Longrightarrow> DERIV (\<lambda>x. g (f x)) x : s :> E * D"
+ using FDERIV_compose[of f "\<lambda>x. x * D" x s g "\<lambda>x. x * E"]
+ by (auto simp: deriv_fderiv ac_simps dest: FDERIV_subset)
+
+text {* Standard version *}
+
+lemma DERIV_chain: "DERIV f (g x) :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (f o g) x : s :> Da * Db"
+ by (drule (1) DERIV_chain', simp add: o_def mult_commute)
+
+lemma DERIV_chain2: "DERIV f (g x) :> Da \<Longrightarrow> DERIV g x : s :> Db \<Longrightarrow> DERIV (%x. f (g x)) x : s :> Da * Db"
+ by (auto dest: DERIV_chain simp add: o_def)
+
+subsubsection {* @{text "DERIV_intros"} *}
+
+ML {*
+structure Deriv_Intros = Named_Thms
+(
+ val name = @{binding DERIV_intros}
+ val description = "DERIV introduction rules"
+)
+*}
+
+setup Deriv_Intros.setup
+
+lemma DERIV_cong: "DERIV f x : s :> X \<Longrightarrow> X = Y \<Longrightarrow> DERIV f x : s :> Y"
+ by simp
+
+declare
+ DERIV_const[THEN DERIV_cong, DERIV_intros]
+ DERIV_ident[THEN DERIV_cong, DERIV_intros]
+ DERIV_add[THEN DERIV_cong, DERIV_intros]
+ DERIV_minus[THEN DERIV_cong, DERIV_intros]
+ DERIV_mult[THEN DERIV_cong, DERIV_intros]
+ DERIV_diff[THEN DERIV_cong, DERIV_intros]
+ DERIV_inverse'[THEN DERIV_cong, DERIV_intros]
+ DERIV_divide[THEN DERIV_cong, DERIV_intros]
+ DERIV_power[where 'a=real, THEN DERIV_cong,
+ unfolded real_of_nat_def[symmetric], DERIV_intros]
+ DERIV_setsum[THEN DERIV_cong, DERIV_intros]
text{*Alternative definition for differentiability*}
@@ -121,86 +723,33 @@
apply (simp add: add_commute)
done
-lemma DERIV_iff2: "(DERIV f x :> D) = ((%z. (f(z) - f(x)) / (z-x)) -- x --> D)"
-by (simp add: deriv_def diff_minus [symmetric] DERIV_LIM_iff)
-
-lemma DERIV_inverse_lemma:
- "\<lbrakk>a \<noteq> 0; b \<noteq> (0::'a::real_normed_field)\<rbrakk>
- \<Longrightarrow> (inverse a - inverse b) / h
- = - (inverse a * ((a - b) / h) * inverse b)"
-by (simp add: inverse_diff_inverse)
-
-lemma DERIV_inverse':
- assumes der: "DERIV f x :> D"
- assumes neq: "f x \<noteq> 0"
- shows "DERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x) * D * inverse (f x))"
- (is "DERIV _ _ :> ?E")
-proof (unfold DERIV_iff2)
- from der have lim_f: "f -- x --> f x"
- by (rule DERIV_isCont [unfolded isCont_def])
-
- from neq have "0 < norm (f x)" by simp
- with LIM_D [OF lim_f] obtain s
- where s: "0 < s"
- and less_fx: "\<And>z. \<lbrakk>z \<noteq> x; norm (z - x) < s\<rbrakk>
- \<Longrightarrow> norm (f z - f x) < norm (f x)"
- by fast
+lemma DERIV_iff2: "(DERIV f x :> D) \<longleftrightarrow> (\<lambda>z. (f z - f x) / (z - x)) --x --> D"
+ by (simp add: deriv_def diff_minus [symmetric] DERIV_LIM_iff)
- show "(\<lambda>z. (inverse (f z) - inverse (f x)) / (z - x)) -- x --> ?E"
- proof (rule LIM_equal2 [OF s])
- fix z
- assume "z \<noteq> x" "norm (z - x) < s"
- hence "norm (f z - f x) < norm (f x)" by (rule less_fx)
- hence "f z \<noteq> 0" by auto
- thus "(inverse (f z) - inverse (f x)) / (z - x) =
- - (inverse (f z) * ((f z - f x) / (z - x)) * inverse (f x))"
- using neq by (rule DERIV_inverse_lemma)
- next
- from der have "(\<lambda>z. (f z - f x) / (z - x)) -- x --> D"
- by (unfold DERIV_iff2)
- thus "(\<lambda>z. - (inverse (f z) * ((f z - f x) / (z - x)) * inverse (f x)))
- -- x --> ?E"
- by (intro tendsto_intros lim_f neq)
- qed
-qed
+lemma DERIV_cong_ev: "x = y \<Longrightarrow> eventually (\<lambda>x. f x = g x) (nhds x) \<Longrightarrow> u = v \<Longrightarrow>
+ DERIV f x :> u \<longleftrightarrow> DERIV g y :> v"
+ unfolding DERIV_iff2
+proof (rule filterlim_cong)
+ assume "eventually (\<lambda>x. f x = g x) (nhds x)"
+ moreover then have "f x = g x" by (auto simp: eventually_nhds)
+ moreover assume "x = y" "u = v"
+ ultimately show "eventually (\<lambda>xa. (f xa - f x) / (xa - x) = (g xa - g y) / (xa - y)) (at x)"
+ by (auto simp: eventually_at_filter elim: eventually_elim1)
+qed simp_all
-lemma DERIV_divide:
- "\<lbrakk>DERIV f x :> D; DERIV g x :> E; g x \<noteq> 0\<rbrakk>
- \<Longrightarrow> DERIV (\<lambda>x. f x / g x) x :> (D * g x - f x * E) / (g x * g x)"
-apply (subgoal_tac "f x * - (inverse (g x) * E * inverse (g x)) +
- D * inverse (g x) = (D * g x - f x * E) / (g x * g x)")
-apply (erule subst)
-apply (unfold divide_inverse)
-apply (erule DERIV_mult')
-apply (erule (1) DERIV_inverse')
-apply (simp add: ring_distribs nonzero_inverse_mult_distrib)
-done
+lemma DERIV_shift:
+ "(DERIV f (x + z) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (x + z)) x :> y)"
+ by (simp add: DERIV_iff field_simps)
-lemma DERIV_power_Suc:
- fixes f :: "'a \<Rightarrow> 'a::{real_normed_field}"
- assumes f: "DERIV f x :> D"
- shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (1 + of_nat n) * (D * f x ^ n)"
-proof (induct n)
-case 0
- show ?case by (simp add: f)
-case (Suc k)
- from DERIV_mult' [OF f Suc] show ?case
- apply (simp only: of_nat_Suc ring_distribs mult_1_left)
- apply (simp only: power_Suc algebra_simps)
- done
-qed
-
-lemma DERIV_power:
- fixes f :: "'a \<Rightarrow> 'a::{real_normed_field}"
- assumes f: "DERIV f x :> D"
- shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n * (D * f x ^ (n - Suc 0))"
-by (cases "n", simp, simp add: DERIV_power_Suc f del: power_Suc)
+lemma DERIV_mirror:
+ "(DERIV f (- x) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (- x::real) :: real) x :> - y)"
+ by (simp add: deriv_def filterlim_at_split filterlim_at_left_to_right
+ tendsto_minus_cancel_left field_simps conj_commute)
text {* Caratheodory formulation of derivative at a point *}
lemma CARAT_DERIV:
- "(DERIV f x :> l) =
- (\<exists>g. (\<forall>z. f z - f x = g z * (z-x)) & isCont g x & g x = l)"
+ "(DERIV f x :> l) \<longleftrightarrow> (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> isCont g x \<and> g x = l)"
(is "?lhs = ?rhs")
proof
assume der: "DERIV f x :> l"
@@ -221,207 +770,11 @@
by (auto simp add: isCont_iff DERIV_iff cong: LIM_cong)
qed
-lemma DERIV_chain':
- assumes f: "DERIV f x :> D"
- assumes g: "DERIV g (f x) :> E"
- shows "DERIV (\<lambda>x. g (f x)) x :> E * D"
-proof (unfold DERIV_iff2)
- obtain d where d: "\<forall>y. g y - g (f x) = d y * (y - f x)"
- and cont_d: "isCont d (f x)" and dfx: "d (f x) = E"
- using CARAT_DERIV [THEN iffD1, OF g] by fast
- from f have "f -- x --> f x"
- by (rule DERIV_isCont [unfolded isCont_def])
- with cont_d have "(\<lambda>z. d (f z)) -- x --> d (f x)"
- by (rule isCont_tendsto_compose)
- hence "(\<lambda>z. d (f z) * ((f z - f x) / (z - x)))
- -- x --> d (f x) * D"
- by (rule tendsto_mult [OF _ f [unfolded DERIV_iff2]])
- thus "(\<lambda>z. (g (f z) - g (f x)) / (z - x)) -- x --> E * D"
- by (simp add: d dfx)
-qed
-
text {*
Let's do the standard proof, though theorem
@{text "LIM_mult2"} follows from a NS proof
*}
-lemma DERIV_cmult:
- "DERIV f x :> D ==> DERIV (%x. c * f x) x :> c*D"
-by (drule DERIV_mult' [OF DERIV_const], simp)
-
-lemma DERIV_cdivide: "DERIV f x :> D ==> DERIV (%x. f x / c) x :> D / c"
- apply (subgoal_tac "DERIV (%x. (1 / c) * f x) x :> (1 / c) * D", force)
- apply (erule DERIV_cmult)
- done
-
-text {* Standard version *}
-lemma DERIV_chain: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (f o g) x :> Da * Db"
-by (drule (1) DERIV_chain', simp add: o_def mult_commute)
-
-lemma DERIV_chain2: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (%x. f (g x)) x :> Da * Db"
-by (auto dest: DERIV_chain simp add: o_def)
-
-text {* Derivative of linear multiplication *}
-lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x :> c"
-by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp)
-
-lemma DERIV_pow: "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"
-apply (cut_tac DERIV_power [OF DERIV_ident])
-apply (simp add: real_of_nat_def)
-done
-
-text {* Power of @{text "-1"} *}
-
-lemma DERIV_inverse:
- fixes x :: "'a::{real_normed_field}"
- shows "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"
-by (drule DERIV_inverse' [OF DERIV_ident]) simp
-
-text {* Derivative of inverse *}
-lemma DERIV_inverse_fun:
- fixes x :: "'a::{real_normed_field}"
- shows "[| DERIV f x :> d; f(x) \<noteq> 0 |]
- ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
-by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib)
-
-text {* Derivative of quotient *}
-lemma DERIV_quotient:
- fixes x :: "'a::{real_normed_field}"
- shows "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]
- ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
-by (drule (2) DERIV_divide) (simp add: mult_commute)
-
-text {* @{text "DERIV_intros"} *}
-ML {*
-structure Deriv_Intros = Named_Thms
-(
- val name = @{binding DERIV_intros}
- val description = "DERIV introduction rules"
-)
-*}
-
-setup Deriv_Intros.setup
-
-lemma DERIV_cong: "\<lbrakk> DERIV f x :> X ; X = Y \<rbrakk> \<Longrightarrow> DERIV f x :> Y"
- by simp
-
-declare
- DERIV_const[THEN DERIV_cong, DERIV_intros]
- DERIV_ident[THEN DERIV_cong, DERIV_intros]
- DERIV_add[THEN DERIV_cong, DERIV_intros]
- DERIV_minus[THEN DERIV_cong, DERIV_intros]
- DERIV_mult[THEN DERIV_cong, DERIV_intros]
- DERIV_diff[THEN DERIV_cong, DERIV_intros]
- DERIV_inverse'[THEN DERIV_cong, DERIV_intros]
- DERIV_divide[THEN DERIV_cong, DERIV_intros]
- DERIV_power[where 'a=real, THEN DERIV_cong,
- unfolded real_of_nat_def[symmetric], DERIV_intros]
- DERIV_setsum[THEN DERIV_cong, DERIV_intros]
-
-
-subsection {* Differentiability predicate *}
-
-definition
- differentiable :: "['a::real_normed_field \<Rightarrow> 'a, 'a] \<Rightarrow> bool"
- (infixl "differentiable" 60) where
- "f differentiable x = (\<exists>D. DERIV f x :> D)"
-
-lemma differentiableE [elim?]:
- assumes "f differentiable x"
- obtains df where "DERIV f x :> df"
- using assms unfolding differentiable_def ..
-
-lemma differentiableD: "f differentiable x ==> \<exists>D. DERIV f x :> D"
-by (simp add: differentiable_def)
-
-lemma differentiableI: "DERIV f x :> D ==> f differentiable x"
-by (force simp add: differentiable_def)
-
-lemma differentiable_ident [simp]: "(\<lambda>x. x) differentiable x"
- by (rule DERIV_ident [THEN differentiableI])
-
-lemma differentiable_const [simp]: "(\<lambda>z. a) differentiable x"
- by (rule DERIV_const [THEN differentiableI])
-
-lemma differentiable_compose:
- assumes f: "f differentiable (g x)"
- assumes g: "g differentiable x"
- shows "(\<lambda>x. f (g x)) differentiable x"
-proof -
- from `f differentiable (g x)` obtain df where "DERIV f (g x) :> df" ..
- moreover
- from `g differentiable x` obtain dg where "DERIV g x :> dg" ..
- ultimately
- have "DERIV (\<lambda>x. f (g x)) x :> df * dg" by (rule DERIV_chain2)
- thus ?thesis by (rule differentiableI)
-qed
-
-lemma differentiable_sum [simp]:
- assumes "f differentiable x"
- and "g differentiable x"
- shows "(\<lambda>x. f x + g x) differentiable x"
-proof -
- from `f differentiable x` obtain df where "DERIV f x :> df" ..
- moreover
- from `g differentiable x` obtain dg where "DERIV g x :> dg" ..
- ultimately
- have "DERIV (\<lambda>x. f x + g x) x :> df + dg" by (rule DERIV_add)
- thus ?thesis by (rule differentiableI)
-qed
-
-lemma differentiable_minus [simp]:
- assumes "f differentiable x"
- shows "(\<lambda>x. - f x) differentiable x"
-proof -
- from `f differentiable x` obtain df where "DERIV f x :> df" ..
- hence "DERIV (\<lambda>x. - f x) x :> - df" by (rule DERIV_minus)
- thus ?thesis by (rule differentiableI)
-qed
-
-lemma differentiable_diff [simp]:
- assumes "f differentiable x"
- assumes "g differentiable x"
- shows "(\<lambda>x. f x - g x) differentiable x"
- unfolding diff_minus using assms by simp
-
-lemma differentiable_mult [simp]:
- assumes "f differentiable x"
- assumes "g differentiable x"
- shows "(\<lambda>x. f x * g x) differentiable x"
-proof -
- from `f differentiable x` obtain df where "DERIV f x :> df" ..
- moreover
- from `g differentiable x` obtain dg where "DERIV g x :> dg" ..
- ultimately
- have "DERIV (\<lambda>x. f x * g x) x :> df * g x + dg * f x" by (rule DERIV_mult)
- thus ?thesis by (rule differentiableI)
-qed
-
-lemma differentiable_inverse [simp]:
- assumes "f differentiable x" and "f x \<noteq> 0"
- shows "(\<lambda>x. inverse (f x)) differentiable x"
-proof -
- from `f differentiable x` obtain df where "DERIV f x :> df" ..
- hence "DERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x) * df * inverse (f x))"
- using `f x \<noteq> 0` by (rule DERIV_inverse')
- thus ?thesis by (rule differentiableI)
-qed
-
-lemma differentiable_divide [simp]:
- assumes "f differentiable x"
- assumes "g differentiable x" and "g x \<noteq> 0"
- shows "(\<lambda>x. f x / g x) differentiable x"
- unfolding divide_inverse using assms by simp
-
-lemma differentiable_power [simp]:
- fixes f :: "'a::{real_normed_field} \<Rightarrow> 'a"
- assumes "f differentiable x"
- shows "(\<lambda>x. f x ^ n) differentiable x"
- apply (induct n)
- apply simp
- apply (simp add: assms)
- done
-
subsection {* Local extrema *}
text{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*}
@@ -1035,25 +1388,16 @@
subsection {* L'Hopitals rule *}
-lemma DERIV_cong_ev: "x = y \<Longrightarrow> eventually (\<lambda>x. f x = g x) (nhds x) \<Longrightarrow> u = v \<Longrightarrow>
- DERIV f x :> u \<longleftrightarrow> DERIV g y :> v"
- unfolding DERIV_iff2
-proof (rule filterlim_cong)
- assume "eventually (\<lambda>x. f x = g x) (nhds x)"
- moreover then have "f x = g x" by (auto simp: eventually_nhds)
- moreover assume "x = y" "u = v"
- ultimately show "eventually (\<lambda>xa. (f xa - f x) / (xa - x) = (g xa - g y) / (xa - y)) (at x)"
- by (auto simp: eventually_within at_def elim: eventually_elim1)
-qed simp_all
-
-lemma DERIV_shift:
- "(DERIV f (x + z) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (x + z)) x :> y)"
- by (simp add: DERIV_iff field_simps)
-
-lemma DERIV_mirror:
- "(DERIV f (- x) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (- x::real) :: real) x :> - y)"
- by (simp add: deriv_def filterlim_at_split filterlim_at_left_to_right
- tendsto_minus_cancel_left field_simps conj_commute)
+lemma isCont_If_ge:
+ fixes a :: "'a :: linorder_topology"
+ shows "continuous (at_left a) g \<Longrightarrow> (f ---> g a) (at_right a) \<Longrightarrow> isCont (\<lambda>x. if x \<le> a then g x else f x) a"
+ unfolding isCont_def continuous_within
+ apply (intro filterlim_split_at)
+ apply (subst filterlim_cong[OF refl refl, where g=g])
+ apply (simp_all add: eventually_at_filter less_le)
+ apply (subst filterlim_cong[OF refl refl, where g=f])
+ apply (simp_all add: eventually_at_filter less_le)
+ done
lemma lhopital_right_0:
fixes f0 g0 :: "real \<Rightarrow> real"
@@ -1081,7 +1425,7 @@
and g'_neq_0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> g' x \<noteq> 0"
and f0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> DERIV f0 x :> (f' x)"
and g0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> DERIV g0 x :> (g' x)"
- unfolding eventually_within eventually_at by (auto simp: dist_real_def)
+ unfolding eventually_at eventually_at by (auto simp: dist_real_def)
have g_neq_0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> g x \<noteq> 0"
using g0_neq_0 by (simp add: g_def)
@@ -1097,18 +1441,10 @@
note g = this
have "isCont f 0"
- using tendsto_const[of "0::real" "at 0"] f_0
- unfolding isCont_def f_def
- by (intro filterlim_split_at_real)
- (auto elim: eventually_elim1
- simp add: filterlim_def le_filter_def eventually_within eventually_filtermap)
-
+ unfolding f_def by (intro isCont_If_ge f_0 continuous_const)
+
have "isCont g 0"
- using tendsto_const[of "0::real" "at 0"] g_0
- unfolding isCont_def g_def
- by (intro filterlim_split_at_real)
- (auto elim: eventually_elim1
- simp add: filterlim_def le_filter_def eventually_within eventually_filtermap)
+ unfolding g_def by (intro isCont_If_ge g_0 continuous_const)
have "\<exists>\<zeta>. \<forall>x\<in>{0 <..< a}. 0 < \<zeta> x \<and> \<zeta> x < x \<and> f x / g x = f' (\<zeta> x) / g' (\<zeta> x)"
proof (rule bchoice, rule)
@@ -1131,24 +1467,24 @@
qed
then guess \<zeta> ..
then have \<zeta>: "eventually (\<lambda>x. 0 < \<zeta> x \<and> \<zeta> x < x \<and> f x / g x = f' (\<zeta> x) / g' (\<zeta> x)) (at_right 0)"
- unfolding eventually_within eventually_at by (intro exI[of _ a]) (auto simp: dist_real_def)
+ unfolding eventually_at by (intro exI[of _ a]) (auto simp: dist_real_def)
moreover
from \<zeta> have "eventually (\<lambda>x. norm (\<zeta> x) \<le> x) (at_right 0)"
by eventually_elim auto
then have "((\<lambda>x. norm (\<zeta> x)) ---> 0) (at_right 0)"
by (rule_tac real_tendsto_sandwich[where f="\<lambda>x. 0" and h="\<lambda>x. x"])
- (auto intro: tendsto_const tendsto_ident_at_within)
+ (auto intro: tendsto_const tendsto_ident_at)
then have "(\<zeta> ---> 0) (at_right 0)"
by (rule tendsto_norm_zero_cancel)
with \<zeta> have "filterlim \<zeta> (at_right 0) (at_right 0)"
- by (auto elim!: eventually_elim1 simp: filterlim_within filterlim_at)
+ by (auto elim!: eventually_elim1 simp: filterlim_at)
from this lim have "((\<lambda>t. f' (\<zeta> t) / g' (\<zeta> t)) ---> x) (at_right 0)"
by (rule_tac filterlim_compose[of _ _ _ \<zeta>])
ultimately have "((\<lambda>t. f t / g t) ---> x) (at_right 0)" (is ?P)
by (rule_tac filterlim_cong[THEN iffD1, OF refl refl])
(auto elim: eventually_elim1)
also have "?P \<longleftrightarrow> ?thesis"
- by (rule filterlim_cong) (auto simp: f_def g_def eventually_within)
+ by (rule filterlim_cong) (auto simp: f_def g_def eventually_at_filter)
finally show ?thesis .
qed
@@ -1206,11 +1542,12 @@
and f0: "\<And>x. 0 < x \<Longrightarrow> x \<le> a \<Longrightarrow> DERIV f x :> (f' x)"
and g0: "\<And>x. 0 < x \<Longrightarrow> x \<le> a \<Longrightarrow> DERIV g x :> (g' x)"
and Df: "\<And>t. 0 < t \<Longrightarrow> t < a \<Longrightarrow> dist (f' t / g' t) x < e / 4"
- unfolding eventually_within_le by (auto simp: dist_real_def)
+ unfolding eventually_at_le by (auto simp: dist_real_def)
+
from Df have
"eventually (\<lambda>t. t < a) (at_right 0)" "eventually (\<lambda>t::real. 0 < t) (at_right 0)"
- unfolding eventually_within eventually_at by (auto intro!: exI[of _ a] simp: dist_real_def)
+ unfolding eventually_at by (auto intro!: exI[of _ a] simp: dist_real_def)
moreover
have "eventually (\<lambda>t. 0 < g t) (at_right 0)" "eventually (\<lambda>t. g a < g t) (at_right 0)"
--- a/src/HOL/Library/Convex.thy Tue Apr 09 21:22:15 2013 +0200
+++ b/src/HOL/Library/Convex.thy Tue Apr 09 21:39:55 2013 +0200
@@ -669,7 +669,7 @@
proof -
have "\<And>z. z > 0 \<Longrightarrow> DERIV (log b) z :> 1 / (ln b * z)" using DERIV_log by auto
then have f': "\<And>z. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - log b z) z :> - 1 / (ln b * z)"
- using DERIV_minus by auto
+ by (auto simp: DERIV_minus)
have "\<And>z :: real. z > 0 \<Longrightarrow> DERIV inverse z :> - (inverse z ^ Suc (Suc 0))"
using less_imp_neq[THEN not_sym, THEN DERIV_inverse] by auto
from this[THEN DERIV_cmult, of _ "- 1 / ln b"]
--- a/src/HOL/Library/FrechetDeriv.thy Tue Apr 09 21:22:15 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,523 +0,0 @@
-(* Title : FrechetDeriv.thy
- Author : Brian Huffman
-*)
-
-header {* Frechet Derivative *}
-
-theory FrechetDeriv
-imports Complex_Main
-begin
-
-definition
- fderiv ::
- "['a::real_normed_vector \<Rightarrow> 'b::real_normed_vector, 'a, 'a \<Rightarrow> 'b] \<Rightarrow> bool"
- -- {* Frechet derivative: D is derivative of function f at x *}
- ("(FDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where
- "FDERIV f x :> D = (bounded_linear D \<and>
- (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0)"
-
-lemma FDERIV_I:
- "\<lbrakk>bounded_linear D; (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0\<rbrakk>
- \<Longrightarrow> FDERIV f x :> D"
-by (simp add: fderiv_def)
-
-lemma FDERIV_D:
- "FDERIV f x :> D \<Longrightarrow> (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0"
-by (simp add: fderiv_def)
-
-lemma FDERIV_bounded_linear: "FDERIV f x :> D \<Longrightarrow> bounded_linear D"
-by (simp add: fderiv_def)
-
-lemma bounded_linear_zero: "bounded_linear (\<lambda>x. 0)"
- by (rule bounded_linear_intro [where K=0], simp_all)
-
-lemma FDERIV_const: "FDERIV (\<lambda>x. k) x :> (\<lambda>h. 0)"
- by (simp add: fderiv_def bounded_linear_zero tendsto_const)
-
-lemma bounded_linear_ident: "bounded_linear (\<lambda>x. x)"
- by (rule bounded_linear_intro [where K=1], simp_all)
-
-lemma FDERIV_ident: "FDERIV (\<lambda>x. x) x :> (\<lambda>h. h)"
- by (simp add: fderiv_def bounded_linear_ident tendsto_const)
-
-subsection {* Addition *}
-
-lemma bounded_linear_add:
- assumes "bounded_linear f"
- assumes "bounded_linear g"
- shows "bounded_linear (\<lambda>x. f x + g x)"
-proof -
- interpret f: bounded_linear f by fact
- interpret g: bounded_linear g by fact
- show ?thesis apply (unfold_locales)
- apply (simp only: f.add g.add add_ac)
- apply (simp only: f.scaleR g.scaleR scaleR_right_distrib)
- apply (rule f.pos_bounded [THEN exE], rename_tac Kf)
- apply (rule g.pos_bounded [THEN exE], rename_tac Kg)
- apply (rule_tac x="Kf + Kg" in exI, safe)
- apply (subst distrib_left)
- apply (rule order_trans [OF norm_triangle_ineq])
- apply (rule add_mono, erule spec, erule spec)
- done
-qed
-
-lemma norm_ratio_ineq:
- fixes x y :: "'a::real_normed_vector"
- fixes h :: "'b::real_normed_vector"
- shows "norm (x + y) / norm h \<le> norm x / norm h + norm y / norm h"
-apply (rule ord_le_eq_trans)
-apply (rule divide_right_mono)
-apply (rule norm_triangle_ineq)
-apply (rule norm_ge_zero)
-apply (rule add_divide_distrib)
-done
-
-lemma FDERIV_add:
- assumes f: "FDERIV f x :> F"
- assumes g: "FDERIV g x :> G"
- shows "FDERIV (\<lambda>x. f x + g x) x :> (\<lambda>h. F h + G h)"
-proof (rule FDERIV_I)
- show "bounded_linear (\<lambda>h. F h + G h)"
- apply (rule bounded_linear_add)
- apply (rule FDERIV_bounded_linear [OF f])
- apply (rule FDERIV_bounded_linear [OF g])
- done
-next
- have f': "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0"
- using f by (rule FDERIV_D)
- have g': "(\<lambda>h. norm (g (x + h) - g x - G h) / norm h) -- 0 --> 0"
- using g by (rule FDERIV_D)
- from f' g'
- have "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h
- + norm (g (x + h) - g x - G h) / norm h) -- 0 --> 0"
- by (rule tendsto_add_zero)
- thus "(\<lambda>h. norm (f (x + h) + g (x + h) - (f x + g x) - (F h + G h))
- / norm h) -- 0 --> 0"
- apply (rule real_LIM_sandwich_zero)
- apply (simp add: divide_nonneg_pos)
- apply (simp only: add_diff_add)
- apply (rule norm_ratio_ineq)
- done
-qed
-
-subsection {* Subtraction *}
-
-lemma bounded_linear_minus:
- assumes "bounded_linear f"
- shows "bounded_linear (\<lambda>x. - f x)"
-proof -
- interpret f: bounded_linear f by fact
- show ?thesis apply (unfold_locales)
- apply (simp add: f.add)
- apply (simp add: f.scaleR)
- apply (simp add: f.bounded)
- done
-qed
-
-lemma FDERIV_minus:
- "FDERIV f x :> F \<Longrightarrow> FDERIV (\<lambda>x. - f x) x :> (\<lambda>h. - F h)"
-apply (rule FDERIV_I)
-apply (rule bounded_linear_minus)
-apply (erule FDERIV_bounded_linear)
-apply (simp only: fderiv_def minus_diff_minus norm_minus_cancel)
-done
-
-lemma FDERIV_diff:
- "\<lbrakk>FDERIV f x :> F; FDERIV g x :> G\<rbrakk>
- \<Longrightarrow> FDERIV (\<lambda>x. f x - g x) x :> (\<lambda>h. F h - G h)"
-by (simp only: diff_minus FDERIV_add FDERIV_minus)
-
-subsection {* Uniqueness *}
-
-lemma FDERIV_zero_unique:
- assumes "FDERIV (\<lambda>x. 0) x :> F" shows "F = (\<lambda>h. 0)"
-proof -
- interpret F: bounded_linear F
- using assms by (rule FDERIV_bounded_linear)
- let ?r = "\<lambda>h. norm (F h) / norm h"
- have *: "?r -- 0 --> 0"
- using assms unfolding fderiv_def by simp
- show "F = (\<lambda>h. 0)"
- proof
- fix h show "F h = 0"
- proof (rule ccontr)
- assume "F h \<noteq> 0"
- moreover from this have h: "h \<noteq> 0"
- by (clarsimp simp add: F.zero)
- ultimately have "0 < ?r h"
- by (simp add: divide_pos_pos)
- from LIM_D [OF * this] obtain s where s: "0 < s"
- and r: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> ?r x < ?r h" by auto
- from dense [OF s] obtain t where t: "0 < t \<and> t < s" ..
- let ?x = "scaleR (t / norm h) h"
- have "?x \<noteq> 0" and "norm ?x < s" using t h by simp_all
- hence "?r ?x < ?r h" by (rule r)
- thus "False" using t h by (simp add: F.scaleR)
- qed
- qed
-qed
-
-lemma FDERIV_unique:
- assumes "FDERIV f x :> F" and "FDERIV f x :> F'" shows "F = F'"
-proof -
- have "FDERIV (\<lambda>x. 0) x :> (\<lambda>h. F h - F' h)"
- using FDERIV_diff [OF assms] by simp
- hence "(\<lambda>h. F h - F' h) = (\<lambda>h. 0)"
- by (rule FDERIV_zero_unique)
- thus "F = F'"
- unfolding fun_eq_iff right_minus_eq .
-qed
-
-subsection {* Continuity *}
-
-lemma FDERIV_isCont:
- assumes f: "FDERIV f x :> F"
- shows "isCont f x"
-proof -
- from f interpret F: bounded_linear "F" by (rule FDERIV_bounded_linear)
- have "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0"
- by (rule FDERIV_D [OF f])
- hence "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h * norm h) -- 0 --> 0"
- by (intro tendsto_mult_zero tendsto_norm_zero tendsto_ident_at)
- hence "(\<lambda>h. norm (f (x + h) - f x - F h)) -- 0 --> 0"
- by (simp cong: LIM_cong)
- hence "(\<lambda>h. f (x + h) - f x - F h) -- 0 --> 0"
- by (rule tendsto_norm_zero_cancel)
- hence "(\<lambda>h. f (x + h) - f x - F h + F h) -- 0 --> 0"
- by (intro tendsto_add_zero F.tendsto_zero tendsto_ident_at)
- hence "(\<lambda>h. f (x + h) - f x) -- 0 --> 0"
- by simp
- thus "isCont f x"
- unfolding isCont_iff by (rule LIM_zero_cancel)
-qed
-
-subsection {* Composition *}
-
-lemma real_divide_cancel_lemma:
- fixes a b c :: real
- shows "(b = 0 \<Longrightarrow> a = 0) \<Longrightarrow> (a / b) * (b / c) = a / c"
-by simp
-
-lemma bounded_linear_compose:
- assumes "bounded_linear f"
- assumes "bounded_linear g"
- shows "bounded_linear (\<lambda>x. f (g x))"
-proof -
- interpret f: bounded_linear f by fact
- interpret g: bounded_linear g by fact
- show ?thesis proof (unfold_locales)
- fix x y show "f (g (x + y)) = f (g x) + f (g y)"
- by (simp only: f.add g.add)
- next
- fix r x show "f (g (scaleR r x)) = scaleR r (f (g x))"
- by (simp only: f.scaleR g.scaleR)
- next
- from f.pos_bounded
- obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by fast
- from g.pos_bounded
- obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by fast
- show "\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K"
- proof (intro exI allI)
- fix x
- have "norm (f (g x)) \<le> norm (g x) * Kf"
- using f .
- also have "\<dots> \<le> (norm x * Kg) * Kf"
- using g Kf [THEN order_less_imp_le] by (rule mult_right_mono)
- also have "(norm x * Kg) * Kf = norm x * (Kg * Kf)"
- by (rule mult_assoc)
- finally show "norm (f (g x)) \<le> norm x * (Kg * Kf)" .
- qed
- qed
-qed
-
-lemma FDERIV_compose:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
- fixes g :: "'b::real_normed_vector \<Rightarrow> 'c::real_normed_vector"
- assumes f: "FDERIV f x :> F"
- assumes g: "FDERIV g (f x) :> G"
- shows "FDERIV (\<lambda>x. g (f x)) x :> (\<lambda>h. G (F h))"
-proof (rule FDERIV_I)
- from FDERIV_bounded_linear [OF g] FDERIV_bounded_linear [OF f]
- show "bounded_linear (\<lambda>h. G (F h))"
- by (rule bounded_linear_compose)
-next
- let ?Rf = "\<lambda>h. f (x + h) - f x - F h"
- let ?Rg = "\<lambda>k. g (f x + k) - g (f x) - G k"
- let ?k = "\<lambda>h. f (x + h) - f x"
- let ?Nf = "\<lambda>h. norm (?Rf h) / norm h"
- let ?Ng = "\<lambda>h. norm (?Rg (?k h)) / norm (?k h)"
- from f interpret F: bounded_linear "F" by (rule FDERIV_bounded_linear)
- from g interpret G: bounded_linear "G" by (rule FDERIV_bounded_linear)
- from F.bounded obtain kF where kF: "\<And>x. norm (F x) \<le> norm x * kF" by fast
- from G.bounded obtain kG where kG: "\<And>x. norm (G x) \<le> norm x * kG" by fast
-
- let ?fun2 = "\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF)"
-
- show "(\<lambda>h. norm (g (f (x + h)) - g (f x) - G (F h)) / norm h) -- 0 --> 0"
- proof (rule real_LIM_sandwich_zero)
- have Nf: "?Nf -- 0 --> 0"
- using FDERIV_D [OF f] .
-
- have Ng1: "isCont (\<lambda>k. norm (?Rg k) / norm k) 0"
- by (simp add: isCont_def FDERIV_D [OF g])
- have Ng2: "?k -- 0 --> 0"
- apply (rule LIM_zero)
- apply (fold isCont_iff)
- apply (rule FDERIV_isCont [OF f])
- done
- have Ng: "?Ng -- 0 --> 0"
- using isCont_tendsto_compose [OF Ng1 Ng2] by simp
-
- have "(\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF))
- -- 0 --> 0 * kG + 0 * (0 + kF)"
- by (intro tendsto_intros Nf Ng)
- thus "(\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF)) -- 0 --> 0"
- by simp
- next
- fix h::'a assume h: "h \<noteq> 0"
- thus "0 \<le> norm (g (f (x + h)) - g (f x) - G (F h)) / norm h"
- by (simp add: divide_nonneg_pos)
- next
- fix h::'a assume h: "h \<noteq> 0"
- have "g (f (x + h)) - g (f x) - G (F h) = G (?Rf h) + ?Rg (?k h)"
- by (simp add: G.diff)
- hence "norm (g (f (x + h)) - g (f x) - G (F h)) / norm h
- = norm (G (?Rf h) + ?Rg (?k h)) / norm h"
- by (rule arg_cong)
- also have "\<dots> \<le> norm (G (?Rf h)) / norm h + norm (?Rg (?k h)) / norm h"
- by (rule norm_ratio_ineq)
- also have "\<dots> \<le> ?Nf h * kG + ?Ng h * (?Nf h + kF)"
- proof (rule add_mono)
- show "norm (G (?Rf h)) / norm h \<le> ?Nf h * kG"
- apply (rule ord_le_eq_trans)
- apply (rule divide_right_mono [OF kG norm_ge_zero])
- apply simp
- done
- next
- have "norm (?Rg (?k h)) / norm h = ?Ng h * (norm (?k h) / norm h)"
- apply (rule real_divide_cancel_lemma [symmetric])
- apply (simp add: G.zero)
- done
- also have "\<dots> \<le> ?Ng h * (?Nf h + kF)"
- proof (rule mult_left_mono)
- have "norm (?k h) / norm h = norm (?Rf h + F h) / norm h"
- by simp
- also have "\<dots> \<le> ?Nf h + norm (F h) / norm h"
- by (rule norm_ratio_ineq)
- also have "\<dots> \<le> ?Nf h + kF"
- apply (rule add_left_mono)
- apply (subst pos_divide_le_eq, simp add: h)
- apply (subst mult_commute)
- apply (rule kF)
- done
- finally show "norm (?k h) / norm h \<le> ?Nf h + kF" .
- next
- show "0 \<le> ?Ng h"
- apply (case_tac "f (x + h) - f x = 0", simp)
- apply (rule divide_nonneg_pos [OF norm_ge_zero])
- apply simp
- done
- qed
- finally show "norm (?Rg (?k h)) / norm h \<le> ?Ng h * (?Nf h + kF)" .
- qed
- finally show "norm (g (f (x + h)) - g (f x) - G (F h)) / norm h
- \<le> ?Nf h * kG + ?Ng h * (?Nf h + kF)" .
- qed
-qed
-
-subsection {* Product Rule *}
-
-lemma (in bounded_bilinear) FDERIV_lemma:
- "a' ** b' - a ** b - (a ** B + A ** b)
- = a ** (b' - b - B) + (a' - a - A) ** b' + A ** (b' - b)"
-by (simp add: diff_left diff_right)
-
-lemma (in bounded_bilinear) FDERIV:
- fixes x :: "'d::real_normed_vector"
- assumes f: "FDERIV f x :> F"
- assumes g: "FDERIV g x :> G"
- shows "FDERIV (\<lambda>x. f x ** g x) x :> (\<lambda>h. f x ** G h + F h ** g x)"
-proof (rule FDERIV_I)
- show "bounded_linear (\<lambda>h. f x ** G h + F h ** g x)"
- apply (rule bounded_linear_add)
- apply (rule bounded_linear_compose [OF bounded_linear_right])
- apply (rule FDERIV_bounded_linear [OF g])
- apply (rule bounded_linear_compose [OF bounded_linear_left])
- apply (rule FDERIV_bounded_linear [OF f])
- done
-next
- from bounded_linear.bounded [OF FDERIV_bounded_linear [OF f]]
- obtain KF where norm_F: "\<And>x. norm (F x) \<le> norm x * KF" by fast
-
- from pos_bounded obtain K where K: "0 < K" and norm_prod:
- "\<And>a b. norm (a ** b) \<le> norm a * norm b * K" by fast
-
- let ?Rf = "\<lambda>h. f (x + h) - f x - F h"
- let ?Rg = "\<lambda>h. g (x + h) - g x - G h"
-
- let ?fun1 = "\<lambda>h.
- norm (f x ** ?Rg h + ?Rf h ** g (x + h) + F h ** (g (x + h) - g x)) /
- norm h"
-
- let ?fun2 = "\<lambda>h.
- norm (f x) * (norm (?Rg h) / norm h) * K +
- norm (?Rf h) / norm h * norm (g (x + h)) * K +
- KF * norm (g (x + h) - g x) * K"
-
- have "?fun1 -- 0 --> 0"
- proof (rule real_LIM_sandwich_zero)
- from f g isCont_iff [THEN iffD1, OF FDERIV_isCont [OF g]]
- have "?fun2 -- 0 -->
- norm (f x) * 0 * K + 0 * norm (g x) * K + KF * norm (0::'b) * K"
- by (intro tendsto_intros LIM_zero FDERIV_D)
- thus "?fun2 -- 0 --> 0"
- by simp
- next
- fix h::'d assume "h \<noteq> 0"
- thus "0 \<le> ?fun1 h"
- by (simp add: divide_nonneg_pos)
- next
- fix h::'d assume "h \<noteq> 0"
- have "?fun1 h \<le> (norm (f x) * norm (?Rg h) * K +
- norm (?Rf h) * norm (g (x + h)) * K +
- norm h * KF * norm (g (x + h) - g x) * K) / norm h"
- by (intro
- divide_right_mono mult_mono'
- order_trans [OF norm_triangle_ineq add_mono]
- order_trans [OF norm_prod mult_right_mono]
- mult_nonneg_nonneg order_refl norm_ge_zero norm_F
- K [THEN order_less_imp_le]
- )
- also have "\<dots> = ?fun2 h"
- by (simp add: add_divide_distrib)
- finally show "?fun1 h \<le> ?fun2 h" .
- qed
- thus "(\<lambda>h.
- norm (f (x + h) ** g (x + h) - f x ** g x - (f x ** G h + F h ** g x))
- / norm h) -- 0 --> 0"
- by (simp only: FDERIV_lemma)
-qed
-
-lemmas FDERIV_mult =
- bounded_bilinear.FDERIV [OF bounded_bilinear_mult]
-
-lemmas FDERIV_scaleR =
- bounded_bilinear.FDERIV [OF bounded_bilinear_scaleR]
-
-
-subsection {* Powers *}
-
-lemma FDERIV_power_Suc:
- fixes x :: "'a::{real_normed_algebra,comm_ring_1}"
- shows "FDERIV (\<lambda>x. x ^ Suc n) x :> (\<lambda>h. (1 + of_nat n) * x ^ n * h)"
- apply (induct n)
- apply (simp add: FDERIV_ident)
- apply (drule FDERIV_mult [OF FDERIV_ident])
- apply (simp only: of_nat_Suc distrib_right mult_1_left)
- apply (simp only: power_Suc distrib_left add_ac mult_ac)
-done
-
-lemma FDERIV_power:
- fixes x :: "'a::{real_normed_algebra,comm_ring_1}"
- shows "FDERIV (\<lambda>x. x ^ n) x :> (\<lambda>h. of_nat n * x ^ (n - 1) * h)"
- apply (cases n)
- apply (simp add: FDERIV_const)
- apply (simp add: FDERIV_power_Suc del: power_Suc)
- done
-
-
-subsection {* Inverse *}
-
-lemmas bounded_linear_mult_const =
- bounded_linear_mult_left [THEN bounded_linear_compose]
-
-lemmas bounded_linear_const_mult =
- bounded_linear_mult_right [THEN bounded_linear_compose]
-
-lemma FDERIV_inverse:
- fixes x :: "'a::real_normed_div_algebra"
- assumes x: "x \<noteq> 0"
- shows "FDERIV inverse x :> (\<lambda>h. - (inverse x * h * inverse x))"
- (is "FDERIV ?inv _ :> _")
-proof (rule FDERIV_I)
- show "bounded_linear (\<lambda>h. - (?inv x * h * ?inv x))"
- apply (rule bounded_linear_minus)
- apply (rule bounded_linear_mult_const)
- apply (rule bounded_linear_const_mult)
- apply (rule bounded_linear_ident)
- done
-next
- show "(\<lambda>h. norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h)
- -- 0 --> 0"
- proof (rule LIM_equal2)
- show "0 < norm x" using x by simp
- next
- fix h::'a
- assume 1: "h \<noteq> 0"
- assume "norm (h - 0) < norm x"
- hence "h \<noteq> -x" by clarsimp
- hence 2: "x + h \<noteq> 0"
- apply (rule contrapos_nn)
- apply (rule sym)
- apply (erule minus_unique)
- done
- show "norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h
- = norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h"
- apply (subst inverse_diff_inverse [OF 2 x])
- apply (subst minus_diff_minus)
- apply (subst norm_minus_cancel)
- apply (simp add: left_diff_distrib)
- done
- next
- show "(\<lambda>h. norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h)
- -- 0 --> 0"
- proof (rule real_LIM_sandwich_zero)
- show "(\<lambda>h. norm (?inv (x + h) - ?inv x) * norm (?inv x))
- -- 0 --> 0"
- apply (rule tendsto_mult_left_zero)
- apply (rule tendsto_norm_zero)
- apply (rule LIM_zero)
- apply (rule LIM_offset_zero)
- apply (rule tendsto_inverse)
- apply (rule tendsto_ident_at)
- apply (rule x)
- done
- next
- fix h::'a assume h: "h \<noteq> 0"
- show "0 \<le> norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h"
- apply (rule divide_nonneg_pos)
- apply (rule norm_ge_zero)
- apply (simp add: h)
- done
- next
- fix h::'a assume h: "h \<noteq> 0"
- have "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h
- \<le> norm (?inv (x + h) - ?inv x) * norm h * norm (?inv x) / norm h"
- apply (rule divide_right_mono [OF _ norm_ge_zero])
- apply (rule order_trans [OF norm_mult_ineq])
- apply (rule mult_right_mono [OF _ norm_ge_zero])
- apply (rule norm_mult_ineq)
- done
- also have "\<dots> = norm (?inv (x + h) - ?inv x) * norm (?inv x)"
- by simp
- finally show "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h
- \<le> norm (?inv (x + h) - ?inv x) * norm (?inv x)" .
- qed
- qed
-qed
-
-subsection {* Alternate definition *}
-
-lemma field_fderiv_def:
- fixes x :: "'a::real_normed_field" shows
- "FDERIV f x :> (\<lambda>h. h * D) = (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
- apply (unfold fderiv_def)
- apply (simp add: bounded_linear_mult_left)
- apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
- apply (subst diff_divide_distrib)
- apply (subst times_divide_eq_left [symmetric])
- apply (simp cong: LIM_cong)
- apply (simp add: tendsto_norm_zero_iff LIM_zero_iff)
-done
-
-end
--- a/src/HOL/Library/Inner_Product.thy Tue Apr 09 21:22:15 2013 +0200
+++ b/src/HOL/Library/Inner_Product.thy Tue Apr 09 21:39:55 2013 +0200
@@ -5,7 +5,7 @@
header {* Inner Product Spaces and the Gradient Derivative *}
theory Inner_Product
-imports FrechetDeriv
+imports "~~/src/HOL/Complex_Main"
begin
subsection {* Real inner product spaces *}
@@ -177,7 +177,7 @@
lemmas isCont_inner [simp] =
bounded_bilinear.isCont [OF bounded_bilinear_inner]
-lemmas FDERIV_inner =
+lemmas FDERIV_inner [FDERIV_intros] =
bounded_bilinear.FDERIV [OF bounded_bilinear_inner]
lemmas bounded_linear_inner_left =
@@ -186,6 +186,15 @@
lemmas bounded_linear_inner_right =
bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]
+lemmas FDERIV_inner_right [FDERIV_intros] =
+ bounded_linear.FDERIV [OF bounded_linear_inner_right]
+
+lemmas FDERIV_inner_left [FDERIV_intros] =
+ bounded_linear.FDERIV [OF bounded_linear_inner_left]
+
+lemma differentiable_inner [simp]:
+ "f differentiable x in s \<Longrightarrow> g differentiable x in s \<Longrightarrow> (\<lambda>x. inner (f x) (g x)) differentiable x in s"
+ unfolding isDiff_def by (blast intro: FDERIV_inner)
subsection {* Class instances *}
@@ -260,9 +269,6 @@
where
"GDERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. inner h D)"
-lemma deriv_fderiv: "DERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. h * D)"
- by (simp only: deriv_def field_fderiv_def)
-
lemma gderiv_deriv [simp]: "GDERIV f x :> D \<longleftrightarrow> DERIV f x :> D"
by (simp only: gderiv_def deriv_fderiv inner_real_def)
--- a/src/HOL/Library/Library.thy Tue Apr 09 21:22:15 2013 +0200
+++ b/src/HOL/Library/Library.thy Tue Apr 09 21:39:55 2013 +0200
@@ -23,7 +23,6 @@
Float
Formal_Power_Series
Fraction_Field
- FrechetDeriv
FuncSet
Function_Division
Function_Growth
--- a/src/HOL/Library/Product_Vector.thy Tue Apr 09 21:22:15 2013 +0200
+++ b/src/HOL/Library/Product_Vector.thy Tue Apr 09 21:39:55 2013 +0200
@@ -202,6 +202,15 @@
lemma continuous_Pair[continuous_intros]: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))"
unfolding continuous_def by (rule tendsto_Pair)
+lemma continuous_on_fst[continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. fst (f x))"
+ unfolding continuous_on_def by (auto intro: tendsto_fst)
+
+lemma continuous_on_snd[continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. snd (f x))"
+ unfolding continuous_on_def by (auto intro: tendsto_snd)
+
+lemma continuous_on_Pair[continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. (f x, g x))"
+ unfolding continuous_on_def by (auto intro: tendsto_Pair)
+
lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
by (fact continuous_fst)
@@ -480,28 +489,31 @@
subsubsection {* Frechet derivatives involving pairs *}
-lemma FDERIV_Pair:
- assumes f: "FDERIV f x :> f'" and g: "FDERIV g x :> g'"
- shows "FDERIV (\<lambda>x. (f x, g x)) x :> (\<lambda>h. (f' h, g' h))"
-proof (rule FDERIV_I)
+lemma FDERIV_Pair [FDERIV_intros]:
+ assumes f: "FDERIV f x : s :> f'" and g: "FDERIV g x : s :> g'"
+ shows "FDERIV (\<lambda>x. (f x, g x)) x : s :> (\<lambda>h. (f' h, g' h))"
+proof (rule FDERIV_I_sandwich[of 1])
show "bounded_linear (\<lambda>h. (f' h, g' h))"
using f g by (intro bounded_linear_Pair FDERIV_bounded_linear)
- let ?Rf = "\<lambda>h. f (x + h) - f x - f' h"
- let ?Rg = "\<lambda>h. g (x + h) - g x - g' h"
- let ?R = "\<lambda>h. ((f (x + h), g (x + h)) - (f x, g x) - (f' h, g' h))"
- show "(\<lambda>h. norm (?R h) / norm h) -- 0 --> 0"
- proof (rule real_LIM_sandwich_zero)
- show "(\<lambda>h. norm (?Rf h) / norm h + norm (?Rg h) / norm h) -- 0 --> 0"
- using f g by (intro tendsto_add_zero FDERIV_D)
- fix h :: 'a assume "h \<noteq> 0"
- thus "0 \<le> norm (?R h) / norm h"
- by (simp add: divide_nonneg_pos)
- show "norm (?R h) / norm h \<le> norm (?Rf h) / norm h + norm (?Rg h) / norm h"
- unfolding add_divide_distrib [symmetric]
- by (simp add: norm_Pair divide_right_mono
- order_trans [OF sqrt_add_le_add_sqrt])
- qed
-qed
+ let ?Rf = "\<lambda>y. f y - f x - f' (y - x)"
+ let ?Rg = "\<lambda>y. g y - g x - g' (y - x)"
+ let ?R = "\<lambda>y. ((f y, g y) - (f x, g x) - (f' (y - x), g' (y - x)))"
+
+ show "((\<lambda>y. norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)) ---> 0) (at x within s)"
+ using f g by (intro tendsto_add_zero) (auto simp: FDERIV_iff_norm)
+
+ fix y :: 'a assume "y \<noteq> x"
+ show "norm (?R y) / norm (y - x) \<le> norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)"
+ unfolding add_divide_distrib [symmetric]
+ by (simp add: norm_Pair divide_right_mono order_trans [OF sqrt_add_le_add_sqrt])
+qed simp
+
+lemmas FDERIV_fst [FDERIV_intros] = bounded_linear.FDERIV [OF bounded_linear_fst]
+lemmas FDERIV_snd [FDERIV_intros] = bounded_linear.FDERIV [OF bounded_linear_snd]
+
+lemma FDERIV_split [FDERIV_intros]:
+ "((\<lambda>p. f (fst p) (snd p)) has_derivative f') F \<Longrightarrow> ((\<lambda>(a, b). f a b) has_derivative f') F"
+ unfolding split_beta' .
subsection {* Product is an inner product space *}
--- a/src/HOL/Limits.thy Tue Apr 09 21:22:15 2013 +0200
+++ b/src/HOL/Limits.thy Tue Apr 09 21:39:55 2013 +0200
@@ -12,10 +12,6 @@
imports Real_Vector_Spaces
begin
-(* Unfortunately eventually_within was overwritten by Multivariate_Analysis.
- Hence it was references as Limits.eventually_within, but now it is Basic_Topology.eventually_within *)
-lemmas eventually_within = eventually_within
-
subsection {* Filter going to infinity norm *}
definition at_infinity :: "'a::real_normed_vector filter" where
@@ -910,25 +906,36 @@
lemmas filterlim_split_at_real = filterlim_split_at[where 'a=real]
-lemma filtermap_nhds_shift: "filtermap (\<lambda>x. x - d) (nhds a) = nhds (a - d::real)"
- unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
- by (intro allI ex_cong) (auto simp: dist_real_def field_simps)
+lemma filtermap_homeomorph:
+ assumes f: "continuous (at a) f"
+ assumes g: "continuous (at (f a)) g"
+ assumes bij1: "\<forall>x. f (g x) = x" and bij2: "\<forall>x. g (f x) = x"
+ shows "filtermap f (nhds a) = nhds (f a)"
+ unfolding filter_eq_iff eventually_filtermap eventually_nhds
+proof safe
+ fix P S assume S: "open S" "f a \<in> S" and P: "\<forall>x\<in>S. P x"
+ from continuous_within_topological[THEN iffD1, rule_format, OF f S] P
+ show "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P (f x))" by auto
+next
+ fix P S assume S: "open S" "a \<in> S" and P: "\<forall>x\<in>S. P (f x)"
+ with continuous_within_topological[THEN iffD1, rule_format, OF g, of S] bij2
+ obtain A where "open A" "f a \<in> A" "(\<forall>y\<in>A. g y \<in> S)"
+ by (metis UNIV_I)
+ with P bij1 show "\<exists>S. open S \<and> f a \<in> S \<and> (\<forall>x\<in>S. P x)"
+ by (force intro!: exI[of _ A])
+qed
-lemma filtermap_nhds_minus: "filtermap (\<lambda>x. - x) (nhds a) = nhds (- a::real)"
- unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
- apply (intro allI ex_cong)
- apply (auto simp: dist_real_def field_simps)
- apply (erule_tac x="-x" in allE)
- apply simp
- done
+lemma filtermap_nhds_shift: "filtermap (\<lambda>x. x - d) (nhds a) = nhds (a - d::'a::real_normed_vector)"
+ by (rule filtermap_homeomorph[where g="\<lambda>x. x + d"]) (auto intro: continuous_intros)
-lemma filtermap_at_shift: "filtermap (\<lambda>x. x - d) (at a) = at (a - d::real)"
- unfolding at_def filtermap_nhds_shift[symmetric]
- by (simp add: filter_eq_iff eventually_filtermap eventually_within)
+lemma filtermap_nhds_minus: "filtermap (\<lambda>x. - x) (nhds a) = nhds (- a::'a::real_normed_vector)"
+ by (rule filtermap_homeomorph[where g=uminus]) (auto intro: continuous_minus)
+
+lemma filtermap_at_shift: "filtermap (\<lambda>x. x - d) (at a) = at (a - d::'a::real_normed_vector)"
+ by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric])
lemma filtermap_at_right_shift: "filtermap (\<lambda>x. x - d) (at_right a) = at_right (a - d::real)"
- unfolding filtermap_at_shift[symmetric]
- by (simp add: filter_eq_iff eventually_filtermap eventually_within)
+ by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric])
lemma at_right_to_0: "at_right (a::real) = filtermap (\<lambda>x. x + a) (at_right 0)"
using filtermap_at_right_shift[of "-a" 0] by simp
@@ -941,15 +948,14 @@
"eventually P (at_right (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (x + a)) (at_right 0)"
unfolding at_right_to_0[of a] by (simp add: eventually_filtermap)
-lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a::real)"
- unfolding at_def filtermap_nhds_minus[symmetric]
- by (simp add: filter_eq_iff eventually_filtermap eventually_within)
+lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a::'a::real_normed_vector)"
+ by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
lemma at_left_minus: "at_left (a::real) = filtermap (\<lambda>x. - x) (at_right (- a))"
- by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
+ by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
lemma at_right_minus: "at_right (a::real) = filtermap (\<lambda>x. - x) (at_left (- a))"
- by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
+ by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
lemma filterlim_at_left_to_right:
"filterlim f F (at_left (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (- x)) F (at_right (-a))"
@@ -989,19 +995,19 @@
unfolding filterlim_uminus_at_top by simp
lemma filterlim_inverse_at_top_right: "LIM x at_right (0::real). inverse x :> at_top"
- unfolding filterlim_at_top_gt[where c=0] eventually_within at_def
+ unfolding filterlim_at_top_gt[where c=0] eventually_at_filter
proof safe
fix Z :: real assume [arith]: "0 < Z"
then have "eventually (\<lambda>x. x < inverse Z) (nhds 0)"
by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"])
- then show "eventually (\<lambda>x. x \<in> - {0} \<longrightarrow> x \<in> {0<..} \<longrightarrow> Z \<le> inverse x) (nhds 0)"
+ then show "eventually (\<lambda>x. x \<noteq> 0 \<longrightarrow> x \<in> {0<..} \<longrightarrow> Z \<le> inverse x) (nhds 0)"
by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps)
qed
lemma filterlim_inverse_at_top:
"(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> LIM x F. inverse (f x) :> at_top"
by (intro filterlim_compose[OF filterlim_inverse_at_top_right])
- (simp add: filterlim_def eventually_filtermap le_within_iff at_def eventually_elim1)
+ (simp add: filterlim_def eventually_filtermap eventually_elim1 at_within_def le_principal)
lemma filterlim_inverse_at_bot_neg:
"LIM x (at_left (0::real)). inverse x :> at_bot"
@@ -1033,8 +1039,7 @@
have "(inverse ---> (0::real)) at_top"
by (metis tendsto_inverse_0 filterlim_mono at_top_le_at_infinity order_refl)
then show "filtermap inverse at_top \<le> at_right (0::real)"
- unfolding at_within_eq
- by (intro le_withinI) (simp_all add: eventually_filtermap eventually_gt_at_top filterlim_def)
+ by (simp add: le_principal eventually_filtermap eventually_gt_at_top filterlim_def at_within_def)
next
have "filtermap inverse (filtermap inverse (at_right (0::real))) \<le> filtermap inverse at_top"
using filterlim_inverse_at_top_right unfolding filterlim_def by (rule filtermap_mono)
@@ -1082,9 +1087,9 @@
then have "filtermap inverse (filtermap g F) \<le> filtermap inverse at_infinity"
by (rule filtermap_mono)
also have "\<dots> \<le> at 0"
- using tendsto_inverse_0
- by (auto intro!: le_withinI exI[of _ 1]
- simp: eventually_filtermap eventually_at_infinity filterlim_def at_def)
+ using tendsto_inverse_0[where 'a='b]
+ by (auto intro!: exI[of _ 1]
+ simp: le_principal eventually_filtermap filterlim_def at_within_def eventually_at_infinity)
finally show "filtermap inverse (filtermap g F) \<le> at 0" .
next
assume "filtermap inverse (filtermap g F) \<le> at 0"
@@ -1094,9 +1099,8 @@
by (auto intro: order_trans simp: filterlim_def filtermap_filtermap)
qed
-lemma tendsto_inverse_0_at_top:
- "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) ---> 0) F"
- by (metis at_top_le_at_infinity filterlim_at filterlim_inverse_at_iff filterlim_mono order_refl)
+lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) ---> 0) F"
+ by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
text {*
@@ -1516,13 +1520,7 @@
lemma LIM_offset:
fixes a :: "'a::real_normed_vector"
shows "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
-apply (rule topological_tendstoI)
-apply (drule (2) topological_tendstoD)
-apply (simp only: eventually_at dist_norm)
-apply (clarify, rule_tac x=d in exI, safe)
-apply (drule_tac x="x + k" in spec)
-apply (simp add: algebra_simps)
-done
+ unfolding filtermap_at_shift[symmetric, of a k] filterlim_def filtermap_filtermap by simp
lemma LIM_offset_zero:
fixes a :: "'a::real_normed_vector"
@@ -1534,6 +1532,11 @@
shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
by (drule_tac k="- a" in LIM_offset, simp)
+lemma LIM_offset_zero_iff:
+ fixes f :: "'a :: real_normed_vector \<Rightarrow> _"
+ shows "f -- a --> L \<longleftrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
+ using LIM_offset_zero_cancel[of f a L] LIM_offset_zero[of f L a] by auto
+
lemma LIM_zero:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. f x - l) ---> 0) F"
@@ -1717,7 +1720,7 @@
show "(f ---> f x) (at_left x)"
using `isCont f x` by (simp add: filterlim_at_split isCont_def)
show "eventually (\<lambda>x. 0 \<le> f x) (at_left x)"
- using ev by (auto simp: eventually_within_less dist_real_def intro!: exI[of _ "x - b"])
+ using ev by (auto simp: eventually_at dist_real_def intro!: exI[of _ "x - b"])
qed simp
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Apr 09 21:22:15 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Apr 09 21:39:55 2013 +0200
@@ -1167,7 +1167,7 @@
lemma differentiable_at_imp_differentiable_on:
"(\<forall>x\<in>(s::(real^'n) set). f differentiable at x) \<Longrightarrow> f differentiable_on s"
- unfolding differentiable_on_def by(auto intro!: differentiable_at_withinI)
+ by (metis differentiable_at_withinI differentiable_on_def)
definition "jacobian f net = matrix(frechet_derivative f net)"
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Apr 09 21:22:15 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Apr 09 21:39:55 2013 +0200
@@ -9,26 +9,15 @@
imports Brouwer_Fixpoint Operator_Norm
begin
-(* Because I do not want to type this all the time *)
-lemmas linear_linear = linear_conv_bounded_linear[THEN sym]
-
-subsection {* Derivatives *}
-
-text {* The definition is slightly tricky since we make it work over
- nets of a particular form. This lets us prove theorems generally and use
- "at a" or "at a within s" for restriction to a set (1-sided on R etc.) *}
+lemma bounded_linear_imp_linear: "bounded_linear f \<Longrightarrow> linear f" (* TODO: move elsewhere *)
+proof -
+ assume "bounded_linear f"
+ then interpret f: bounded_linear f .
+ show "linear f"
+ by (simp add: f.add f.scaleR linear_def)
+qed
-definition has_derivative :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a filter \<Rightarrow> bool)"
-(infixl "(has'_derivative)" 12) where
- "(f has_derivative f') net \<equiv> bounded_linear f' \<and> ((\<lambda>y. (1 / (norm (y - netlimit net))) *\<^sub>R
- (f y - (f (netlimit net) + f'(y - netlimit net)))) ---> 0) net"
-
-lemma derivative_linear[dest]:
- "(f has_derivative f') net \<Longrightarrow> bounded_linear f'"
- unfolding has_derivative_def by auto
-
-lemma netlimit_at_vector:
- (* TODO: move *)
+lemma netlimit_at_vector: (* TODO: move *)
fixes a :: "'a::real_normed_vector"
shows "netlimit (at a) = a"
proof (cases "\<exists>x. x \<noteq> a")
@@ -40,25 +29,66 @@
apply (simp add: norm_sgn sgn_zero_iff x)
done
thus ?thesis
- by (rule netlimit_within [of a UNIV, unfolded within_UNIV])
+ by (rule netlimit_within [of a UNIV])
qed simp
-lemma FDERIV_conv_has_derivative:
- shows "FDERIV f x :> f' = (f has_derivative f') (at x)"
- unfolding fderiv_def has_derivative_def netlimit_at_vector
- by (simp add: diff_diff_eq Lim_at_zero [where a=x]
- tendsto_norm_zero_iff [where 'b='b, symmetric])
+(* Because I do not want to type this all the time *)
+lemmas linear_linear = linear_conv_bounded_linear[THEN sym]
+
+lemma derivative_linear[dest]:
+ "(f has_derivative f') net \<Longrightarrow> bounded_linear f'"
+ unfolding has_derivative_def by auto
+
+lemma derivative_is_linear:
+ "(f has_derivative f') net \<Longrightarrow> linear f'"
+ by (rule derivative_linear [THEN bounded_linear_imp_linear])
lemma DERIV_conv_has_derivative:
"(DERIV f x :> f') = (f has_derivative op * f') (at x)"
- unfolding deriv_fderiv FDERIV_conv_has_derivative
- by (subst mult_commute, rule refl)
+ using deriv_fderiv[of f x UNIV f'] by (subst (asm) mult_commute)
+
+subsection {* Derivatives *}
+
+subsubsection {* Combining theorems. *}
+
+lemmas has_derivative_id = FDERIV_ident
+lemmas has_derivative_const = FDERIV_const
+lemmas has_derivative_neg = FDERIV_minus
+lemmas has_derivative_add = FDERIV_add
+lemmas has_derivative_sub = FDERIV_diff
+lemmas has_derivative_setsum = FDERIV_setsum
+lemmas scaleR_right_has_derivative = FDERIV_scaleR_right
+lemmas scaleR_left_has_derivative = FDERIV_scaleR_left
+lemmas inner_right_has_derivative = FDERIV_inner_right
+lemmas inner_left_has_derivative = FDERIV_inner_left
+lemmas mult_right_has_derivative = FDERIV_mult_right
+lemmas mult_left_has_derivative = FDERIV_mult_left
+
+lemma has_derivative_add_const:
+ "(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net"
+ by (intro FDERIV_eq_intros) auto
+
+subsection {* Derivative with composed bilinear function. *}
+
+lemma has_derivative_bilinear_within:
+ assumes "(f has_derivative f') (at x within s)"
+ assumes "(g has_derivative g') (at x within s)"
+ assumes "bounded_bilinear h"
+ shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x within s)"
+ using bounded_bilinear.FDERIV[OF assms(3,1,2)] .
+
+lemma has_derivative_bilinear_at:
+ assumes "(f has_derivative f') (at x)"
+ assumes "(g has_derivative g') (at x)"
+ assumes "bounded_bilinear h"
+ shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x)"
+ using has_derivative_bilinear_within[of f f' x UNIV g g' h] assms by simp
text {* These are the only cases we'll care about, probably. *}
lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow>
bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x within s)"
- unfolding has_derivative_def and Lim by(auto simp add:netlimit_within)
+ unfolding has_derivative_def Lim by (auto simp add: netlimit_within inverse_eq_divide field_simps)
lemma has_derivative_at: "(f has_derivative f') (at x) \<longleftrightarrow>
bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x)"
@@ -80,7 +110,7 @@
using has_derivative_within' [of f f' x UNIV] by simp
lemma has_derivative_at_within: "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f') (at x within s)"
- unfolding has_derivative_within' has_derivative_at' by meson
+ unfolding has_derivative_within' has_derivative_at' by blast
lemma has_derivative_within_open:
"a \<in> s \<Longrightarrow> open s \<Longrightarrow> ((f has_derivative f') (at a within s) \<longleftrightarrow> (f has_derivative f') (at a))"
@@ -102,111 +132,6 @@
by (simp add: bounded_linear_mult_right has_derivative_within)
qed
-lemma bounded_linear_imp_linear: "bounded_linear f \<Longrightarrow> linear f" (* TODO: move elsewhere *)
-proof -
- assume "bounded_linear f"
- then interpret f: bounded_linear f .
- show "linear f"
- by (simp add: f.add f.scaleR linear_def)
-qed
-
-lemma derivative_is_linear:
- "(f has_derivative f') net \<Longrightarrow> linear f'"
- by (rule derivative_linear [THEN bounded_linear_imp_linear])
-
-subsubsection {* Combining theorems. *}
-
-lemma has_derivative_eq_rhs: "(f has_derivative x) F \<Longrightarrow> x = y \<Longrightarrow> (f has_derivative y) F"
- by simp
-
-ML {*
-
-structure Has_Derivative_Intros = Named_Thms
-(
- val name = @{binding has_derivative_intros}
- val description = "introduction rules for has_derivative"
-)
-
-*}
-
-setup {*
- Has_Derivative_Intros.setup #>
- Global_Theory.add_thms_dynamic (@{binding has_derivative_eq_intros},
- map (fn thm => @{thm has_derivative_eq_rhs} OF [thm]) o Has_Derivative_Intros.get o Context.proof_of);
-*}
-
-lemma has_derivative_id[has_derivative_intros]: "((\<lambda>x. x) has_derivative (\<lambda>h. h)) net"
- unfolding has_derivative_def
- by (simp add: bounded_linear_ident tendsto_const)
-
-lemma has_derivative_const[has_derivative_intros]: "((\<lambda>x. c) has_derivative (\<lambda>h. 0)) net"
- unfolding has_derivative_def
- by (simp add: bounded_linear_zero tendsto_const)
-
-lemma (in bounded_linear) has_derivative'[has_derivative_intros]: "(f has_derivative f) net"
- unfolding has_derivative_def apply(rule,rule bounded_linear_axioms)
- unfolding diff by (simp add: tendsto_const)
-
-lemma (in bounded_linear) bounded_linear: "bounded_linear f" ..
-
-lemma (in bounded_linear) has_derivative[has_derivative_intros]:
- assumes "((\<lambda>x. g x) has_derivative (\<lambda>h. g' h)) net"
- shows "((\<lambda>x. f (g x)) has_derivative (\<lambda>h. f (g' h))) net"
- using assms unfolding has_derivative_def
- apply safe
- apply (erule bounded_linear_compose [OF local.bounded_linear])
- apply (drule local.tendsto)
- apply (simp add: local.scaleR local.diff local.add local.zero)
- done
-
-lemmas scaleR_right_has_derivative[has_derivative_intros] =
- bounded_linear.has_derivative [OF bounded_linear_scaleR_right]
-
-lemmas scaleR_left_has_derivative[has_derivative_intros] =
- bounded_linear.has_derivative [OF bounded_linear_scaleR_left]
-
-lemmas inner_right_has_derivative[has_derivative_intros] =
- bounded_linear.has_derivative [OF bounded_linear_inner_right]
-
-lemmas inner_left_has_derivative[has_derivative_intros] =
- bounded_linear.has_derivative [OF bounded_linear_inner_left]
-
-lemmas mult_right_has_derivative[has_derivative_intros] =
- bounded_linear.has_derivative [OF bounded_linear_mult_right]
-
-lemmas mult_left_has_derivative[has_derivative_intros] =
- bounded_linear.has_derivative [OF bounded_linear_mult_left]
-
-lemma has_derivative_neg[has_derivative_intros]:
- assumes "(f has_derivative f') net"
- shows "((\<lambda>x. -(f x)) has_derivative (\<lambda>h. -(f' h))) net"
- using scaleR_right_has_derivative [where r="-1", OF assms] by auto
-
-lemma has_derivative_add[has_derivative_intros]:
- assumes "(f has_derivative f') net" and "(g has_derivative g') net"
- shows "((\<lambda>x. f(x) + g(x)) has_derivative (\<lambda>h. f'(h) + g'(h))) net"
-proof-
- note as = assms[unfolded has_derivative_def]
- show ?thesis unfolding has_derivative_def apply(rule,rule bounded_linear_add)
- using tendsto_add[OF as(1)[THEN conjunct2] as(2)[THEN conjunct2]] and as
- by (auto simp add: algebra_simps)
-qed
-
-lemma has_derivative_add_const:
- "(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net"
- by (intro has_derivative_eq_intros) auto
-
-lemma has_derivative_sub[has_derivative_intros]:
- assumes "(f has_derivative f') net" and "(g has_derivative g') net"
- shows "((\<lambda>x. f(x) - g(x)) has_derivative (\<lambda>h. f'(h) - g'(h))) net"
- unfolding diff_minus by (intro has_derivative_intros assms)
-
-lemma has_derivative_setsum[has_derivative_intros]:
- assumes "finite s" and "\<forall>a\<in>s. ((f a) has_derivative (f' a)) net"
- shows "((\<lambda>x. setsum (\<lambda>a. f a x) s) has_derivative (\<lambda>h. setsum (\<lambda>a. f' a h) s)) net"
- using assms by (induct, simp_all add: has_derivative_const has_derivative_add)
-text {* Somewhat different results for derivative of scalar multiplier. *}
-
subsubsection {* Limit transformation for derivatives *}
lemma has_derivative_transform_within:
@@ -232,12 +157,14 @@
no_notation Deriv.differentiable (infixl "differentiable" 60)
-definition differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" (infixr "differentiable" 30) where
- "f differentiable net \<equiv> (\<exists>f'. (f has_derivative f') net)"
+abbreviation differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" (infixr "differentiable" 30) where
+ "f differentiable net \<equiv> isDiff net f"
definition differentiable_on :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "differentiable'_on" 30) where
"f differentiable_on s \<equiv> (\<forall>x\<in>s. f differentiable (at x within s))"
+lemmas differentiable_def = isDiff_def
+
lemma differentiableI: "(f has_derivative f') net \<Longrightarrow> f differentiable net"
unfolding differentiable_def by auto
@@ -252,7 +179,7 @@
lemma differentiable_on_eq_differentiable_at:
"open s \<Longrightarrow> (f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable at x))"
unfolding differentiable_on_def
- by (auto simp add: at_within_interior interior_open)
+ by (metis at_within_interior interior_open)
lemma differentiable_transform_within:
assumes "0 < d" and "x \<in> s" and "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'"
@@ -292,32 +219,8 @@
by(auto intro!: mult_strict_mono[of _ "1::real", unfolded mult_1_left])
lemma differentiable_imp_continuous_within:
- assumes "f differentiable (at x within s)"
- shows "continuous (at x within s) f"
-proof-
- from assms guess f' unfolding differentiable_def has_derivative_within ..
- note f'=this
- then interpret bounded_linear f' by auto
- have *:"\<And>xa. x\<noteq>xa \<Longrightarrow> (f' \<circ> (\<lambda>y. y - x)) xa + norm (xa - x) *\<^sub>R ((1 / norm (xa - x)) *\<^sub>R (f xa - (f x + f' (xa - x)))) - ((f' \<circ> (\<lambda>y. y - x)) x + 0) = f xa - f x"
- using zero by auto
- have **:"continuous (at x within s) (f' \<circ> (\<lambda>y. y - x))"
- apply(rule continuous_within_compose) apply(rule continuous_intros)+
- by(rule linear_continuous_within[OF f'[THEN conjunct1]])
- show ?thesis unfolding continuous_within
- using f'[THEN conjunct2, THEN Lim_mul_norm_within]
- apply- apply(drule tendsto_add)
- apply(rule **[unfolded continuous_within])
- unfolding Lim_within and dist_norm
- apply (rule, rule)
- apply (erule_tac x=e in allE)
- apply (erule impE | assumption)+
- apply (erule exE, rule_tac x=d in exI)
- by (auto simp add: zero *)
-qed
-
-lemma differentiable_imp_continuous_at:
- "f differentiable at x \<Longrightarrow> continuous (at x) f"
- by(rule differentiable_imp_continuous_within[of _ x UNIV, unfolded within_UNIV])
+ "f differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
+ by (auto simp: differentiable_def intro: FDERIV_continuous)
lemma differentiable_imp_continuous_on:
"f differentiable_on s \<Longrightarrow> continuous_on s f"
@@ -326,7 +229,7 @@
lemma has_derivative_within_subset:
"(f has_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_derivative f') (at x within t)"
- unfolding has_derivative_within using Lim_within_subset by blast
+ unfolding has_derivative_within using tendsto_within_subset by blast
lemma differentiable_within_subset:
"f differentiable (at x within t) \<Longrightarrow> s \<subseteq> t \<Longrightarrow> f differentiable (at x within s)"
@@ -390,132 +293,25 @@
subsection {* The chain rule. *}
-lemma diff_chain_within[has_derivative_intros]:
+lemma diff_chain_within[FDERIV_intros]:
assumes "(f has_derivative f') (at x within s)"
assumes "(g has_derivative g') (at (f x) within (f ` s))"
shows "((g o f) has_derivative (g' o f'))(at x within s)"
- unfolding has_derivative_within_alt
- apply(rule,rule bounded_linear_compose[unfolded o_def[THEN sym]])
- apply(rule assms(2)[unfolded has_derivative_def,THEN conjE],assumption)
- apply(rule assms(1)[unfolded has_derivative_def,THEN conjE],assumption)
-proof(rule,rule)
- note assms = assms[unfolded has_derivative_within_alt]
- fix e::real assume "0<e"
- guess B1 using bounded_linear.pos_bounded[OF assms(1)[THEN conjunct1, rule_format]] .. note B1 = this
- guess B2 using bounded_linear.pos_bounded[OF assms(2)[THEN conjunct1, rule_format]] .. note B2 = this
- have *:"e / 2 / B2 > 0" using `e>0` B2 apply-apply(rule divide_pos_pos) by auto
- guess d1 using assms(1)[THEN conjunct2, rule_format, OF *] .. note d1 = this
- have *:"e / 2 / (1 + B1) > 0" using `e>0` B1 apply-apply(rule divide_pos_pos) by auto
- guess de using assms(2)[THEN conjunct2, rule_format, OF *] .. note de = this
- guess d2 using assms(1)[THEN conjunct2, rule_format, OF zero_less_one] .. note d2 = this
-
- def d0 \<equiv> "(min d1 d2)/2" have d0:"d0>0" "d0 < d1" "d0 < d2" unfolding d0_def using d1 d2 by auto
- def d \<equiv> "(min d0 (de / (B1 + 1))) / 2" have "de * 2 / (B1 + 1) > de / (B1 + 1)" apply(rule divide_strict_right_mono) using B1 de by auto
- hence d:"d>0" "d < d1" "d < d2" "d < (de / (B1 + 1))" unfolding d_def using d0 d1 d2 de B1 by(auto intro!: divide_pos_pos simp add:min_less_iff_disj not_less)
-
- show "\<exists>d>0. \<forall>y\<in>s. norm (y - x) < d \<longrightarrow> norm ((g \<circ> f) y - (g \<circ> f) x - (g' \<circ> f') (y - x)) \<le> e * norm (y - x)" apply(rule_tac x=d in exI)
- proof(rule,rule `d>0`,rule,rule)
- fix y assume as:"y \<in> s" "norm (y - x) < d"
- hence 1:"norm (f y - f x - f' (y - x)) \<le> min (norm (y - x)) (e / 2 / B2 * norm (y - x))" using d1 d2 d by auto
-
- have "norm (f y - f x) \<le> norm (f y - f x - f' (y - x)) + norm (f' (y - x))"
- using norm_triangle_sub[of "f y - f x" "f' (y - x)"]
- by(auto simp add:algebra_simps)
- also have "\<dots> \<le> norm (f y - f x - f' (y - x)) + B1 * norm (y - x)"
- apply(rule add_left_mono) using B1 by(auto simp add:algebra_simps)
- also have "\<dots> \<le> min (norm (y - x)) (e / 2 / B2 * norm (y - x)) + B1 * norm (y - x)"
- apply(rule add_right_mono) using d1 d2 d as by auto
- also have "\<dots> \<le> norm (y - x) + B1 * norm (y - x)" by auto
- also have "\<dots> = norm (y - x) * (1 + B1)" by(auto simp add:field_simps)
- finally have 3:"norm (f y - f x) \<le> norm (y - x) * (1 + B1)" by auto
+ using FDERIV_in_compose[OF assms] by (simp add: comp_def)
- hence "norm (f y - f x) \<le> d * (1 + B1)" apply-
- apply(rule order_trans,assumption,rule mult_right_mono)
- using as B1 by auto
- also have "\<dots> < de" using d B1 by(auto simp add:field_simps)
- finally have "norm (g (f y) - g (f x) - g' (f y - f x)) \<le> e / 2 / (1 + B1) * norm (f y - f x)"
- apply-apply(rule de[THEN conjunct2,rule_format])
- using `y\<in>s` using d as by auto
- also have "\<dots> = (e / 2) * (1 / (1 + B1) * norm (f y - f x))" by auto
- also have "\<dots> \<le> e / 2 * norm (y - x)" apply(rule mult_left_mono)
- using `e>0` and 3 using B1 and `e>0` by(auto simp add:divide_le_eq)
- finally have 4:"norm (g (f y) - g (f x) - g' (f y - f x)) \<le> e / 2 * norm (y - x)" by auto
-
- interpret g': bounded_linear g' using assms(2) by auto
- interpret f': bounded_linear f' using assms(1) by auto
- have "norm (- g' (f' (y - x)) + g' (f y - f x)) = norm (g' (f y - f x - f' (y - x)))"
- by(auto simp add:algebra_simps f'.diff g'.diff g'.add)
- also have "\<dots> \<le> B2 * norm (f y - f x - f' (y - x))" using B2
- by (auto simp add: algebra_simps)
- also have "\<dots> \<le> B2 * (e / 2 / B2 * norm (y - x))"
- apply (rule mult_left_mono) using as d1 d2 d B2 by auto
- also have "\<dots> \<le> e / 2 * norm (y - x)" using B2 by auto
- finally have 5:"norm (- g' (f' (y - x)) + g' (f y - f x)) \<le> e / 2 * norm (y - x)" by auto
-
- have "norm (g (f y) - g (f x) - g' (f y - f x)) + norm (g (f y) - g (f x) - g' (f' (y - x)) - (g (f y) - g (f x) - g' (f y - f x))) \<le> e * norm (y - x)"
- using 5 4 by auto
- thus "norm ((g \<circ> f) y - (g \<circ> f) x - (g' \<circ> f') (y - x)) \<le> e * norm (y - x)"
- unfolding o_def apply- apply(rule order_trans, rule norm_triangle_sub)
- by assumption
- qed
-qed
+lemma diff_chain_at[FDERIV_intros]:
+ "(f has_derivative f') (at x) \<Longrightarrow> (g has_derivative g') (at (f x)) \<Longrightarrow> ((g o f) has_derivative (g' o f')) (at x)"
+ using FDERIV_compose[of f f' x UNIV g g'] by (simp add: comp_def)
-lemma diff_chain_at[has_derivative_intros]:
- "(f has_derivative f') (at x) \<Longrightarrow> (g has_derivative g') (at (f x)) \<Longrightarrow> ((g o f) has_derivative (g' o f')) (at x)"
- using diff_chain_within[of f f' x UNIV g g']
- using has_derivative_within_subset[of g g' "f x" UNIV "range f"]
- by simp
subsection {* Composition rules stated just for differentiability. *}
-lemma differentiable_const [intro]:
- "(\<lambda>z. c) differentiable (net::'a::real_normed_vector filter)"
- unfolding differentiable_def using has_derivative_const by auto
-
-lemma differentiable_id [intro]:
- "(\<lambda>z. z) differentiable (net::'a::real_normed_vector filter)"
- unfolding differentiable_def using has_derivative_id by auto
-
-lemma differentiable_cmul [intro]:
- "f differentiable net \<Longrightarrow>
- (\<lambda>x. c *\<^sub>R f(x)) differentiable (net::'a::real_normed_vector filter)"
- unfolding differentiable_def
- apply(erule exE, drule scaleR_right_has_derivative) by auto
-
-lemma differentiable_neg [intro]:
- "f differentiable net \<Longrightarrow>
- (\<lambda>z. -(f z)) differentiable (net::'a::real_normed_vector filter)"
- unfolding differentiable_def
- apply(erule exE, drule has_derivative_neg) by auto
-
-lemma differentiable_add [intro]: "f differentiable net \<Longrightarrow> g differentiable net
- \<Longrightarrow> (\<lambda>z. f z + g z) differentiable net"
- by (auto intro: has_derivative_eq_intros simp: differentiable_def)
-
-lemma differentiable_sub [intro]: "f differentiable net \<Longrightarrow> g differentiable net
- \<Longrightarrow> (\<lambda>z. f z - g z) differentiable net"
- by (auto intro: has_derivative_eq_intros simp: differentiable_def)
-
-lemma differentiable_setsum [intro]:
- assumes "finite s" "\<forall>a\<in>s. (f a) differentiable net"
- shows "(\<lambda>x. setsum (\<lambda>a. f a x) s) differentiable net"
-proof-
- guess f' using bchoice[OF assms(2)[unfolded differentiable_def]] ..
- thus ?thesis unfolding differentiable_def apply-
- apply(rule,rule has_derivative_setsum[where f'=f'],rule assms(1)) by auto
-qed
-
-lemma differentiable_setsum_numseg:
- shows "\<forall>i. m \<le> i \<and> i \<le> n \<longrightarrow> (f i) differentiable net \<Longrightarrow> (\<lambda>x. setsum (\<lambda>a. f a x) {m::nat..n}) differentiable net"
- apply(rule differentiable_setsum) using finite_atLeastAtMost[of n m] by auto
-
lemma differentiable_chain_at:
- "f differentiable (at x) \<Longrightarrow> g differentiable (at(f x)) \<Longrightarrow> (g o f) differentiable (at x)"
+ "f differentiable (at x) \<Longrightarrow> g differentiable (at (f x)) \<Longrightarrow> (g o f) differentiable (at x)"
unfolding differentiable_def by(meson diff_chain_at)
lemma differentiable_chain_within:
- "f differentiable (at x within s) \<Longrightarrow> g differentiable (at(f x) within (f ` s))
- \<Longrightarrow> (g o f) differentiable (at x within s)"
+ "f differentiable (at x within s) \<Longrightarrow> g differentiable (at(f x) within (f ` s)) \<Longrightarrow> (g o f) differentiable (at x within s)"
unfolding differentiable_def by(meson diff_chain_within)
subsection {* Uniqueness of derivative *}
@@ -567,13 +363,12 @@
unfolding dist_norm
unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff
scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib
- using i by auto
+ using i by (auto simp: inverse_eq_divide)
qed
qed
lemma frechet_derivative_unique_at:
shows "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f'') (at x) \<Longrightarrow> f' = f''"
- unfolding FDERIV_conv_has_derivative [symmetric]
by (rule FDERIV_unique)
lemma frechet_derivative_unique_within_closed_interval:
@@ -621,7 +416,7 @@
shows "f' = f''"
proof -
from assms(1) have *: "at x within {a<..<b} = at x"
- by (simp add: at_within_interior interior_open open_interval)
+ by (metis at_within_interior interior_open open_interval)
from assms(2,3) [unfolded *] show "f' = f''"
by (rule frechet_derivative_unique_at)
qed
@@ -735,7 +530,8 @@
show ?thesis by (simp add: fun_eq_iff)
qed
-lemma rolle: fixes f::"real\<Rightarrow>real"
+lemma rolle:
+ fixes f::"real\<Rightarrow>real"
assumes "a < b" and "f a = f b" and "continuous_on {a..b} f"
assumes "\<forall>x\<in>{a<..<b}. (f has_derivative f'(x)) (at x)"
shows "\<exists>x\<in>{a<..<b}. f' x = (\<lambda>v. 0)"
@@ -782,8 +578,7 @@
proof (intro rolle[OF assms(1), of "\<lambda>x. f x - (f b - f a) / (b - a) * x"] ballI)
fix x assume x:"x \<in> {a<..<b}"
show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
- by (intro has_derivative_intros assms(3)[rule_format,OF x]
- mult_right_has_derivative)
+ by (intro FDERIV_intros assms(3)[rule_format,OF x] mult_right_has_derivative)
qed (insert assms(1,2), auto intro!: continuous_on_intros simp: field_simps)
then guess x ..
thus ?thesis apply(rule_tac x=x in bexI)
@@ -827,8 +622,9 @@
proof-
have "\<exists>x\<in>{a<..<b}. (op \<bullet> (f b - f a) \<circ> f) b - (op \<bullet> (f b - f a) \<circ> f) a = (f b - f a) \<bullet> f' x (b - a)"
apply(rule mvt) apply(rule assms(1))
- apply(rule continuous_on_inner continuous_on_intros assms(2))+
- unfolding o_def apply(rule,rule has_derivative_intros)
+ apply(rule continuous_on_inner continuous_on_intros assms(2) ballI)+
+ unfolding o_def
+ apply(rule FDERIV_inner_right)
using assms(3) by auto
then guess x .. note x=this
show ?thesis proof(cases "f a = f b")
@@ -873,7 +669,7 @@
case goal1
let ?u = "x + u *\<^sub>R (y - x)"
have "(f \<circ> ?p has_derivative (f' ?u) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u within {0<..<1})"
- apply(rule diff_chain_within) apply(rule has_derivative_intros)+
+ apply(rule diff_chain_within) apply(rule FDERIV_intros)+
apply(rule has_derivative_within_subset)
apply(rule assms(2)[rule_format]) using goal1 * by auto
thus ?case
@@ -1252,7 +1048,7 @@
apply(rule has_derivative_inverse_strong[where g'="g' x" and f=f])
apply(rule assms)+
unfolding continuous_on_eq_continuous_at[OF assms(1)]
- apply(rule,rule differentiable_imp_continuous_at)
+ apply(rule,rule differentiable_imp_continuous_within)
unfolding differentiable_def using assms by auto
text {* Invertible derivative continous at a point implies local
@@ -1306,13 +1102,15 @@
have *:"(\<lambda>v. v - g' (f' u v)) = g' \<circ> (\<lambda>w. f' a w - f' u w)"
unfolding o_def and diff using f'g' by auto
show "(ph has_derivative (\<lambda>v. v - g' (f' u v))) (at u within ball a d)"
- unfolding ph' * apply(rule diff_chain_within) defer
- apply(rule bounded_linear.has_derivative'[OF assms(3)])
- apply(rule has_derivative_intros) defer
+ unfolding ph' *
+ apply(simp add: comp_def)
+ apply(rule bounded_linear.FDERIV[OF assms(3)])
+ apply(rule FDERIV_intros) defer
apply(rule has_derivative_sub[where g'="\<lambda>x.0",unfolded diff_0_right])
apply(rule has_derivative_at_within)
using assms(5) and `u\<in>s` `a\<in>s`
- by(auto intro!: has_derivative_intros bounded_linear.has_derivative' derivative_linear)
+ apply (auto intro!: FDERIV_intros bounded_linear.FDERIV[of _ "\<lambda>x. x"] derivative_linear)
+ done
have **:"bounded_linear (\<lambda>x. f' u x - f' a x)"
"bounded_linear (\<lambda>x. f' a x - f' u x)"
apply(rule_tac[!] bounded_linear_sub)
@@ -1354,7 +1152,7 @@
proof-
fix x assume "x\<in>s"
show "((\<lambda>a. f m a - f n a) has_derivative (\<lambda>h. f' m x h - f' n x h)) (at x within s)"
- by(rule has_derivative_intros assms(2)[rule_format] `x\<in>s`)+
+ by(rule FDERIV_intros assms(2)[rule_format] `x\<in>s`)+
{ fix h
have "norm (f' m x h - f' n x h) \<le> norm (f' m x h - g' x h) + norm (f' n x h - g' x h)"
using norm_triangle_ineq[of "f' m x h - g' x h" "- f' n x h + g' x h"]
@@ -1587,88 +1385,12 @@
shows "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) sums_seq (g x)) k \<and> (g has_derivative g'(x)) (at x within s)"
unfolding sums_seq_def
apply(rule has_derivative_sequence[OF assms(1) _ assms(3)])
- apply(rule,rule)
- apply(rule has_derivative_setsum) defer
- apply(rule,rule assms(2)[rule_format],assumption)
+ apply(rule, rule)
+ apply(rule has_derivative_setsum)
+ apply(rule assms(2)[rule_format])
+ apply assumption
using assms(4-5) unfolding sums_seq_def by auto
-subsection {* Derivative with composed bilinear function. *}
-
-lemma has_derivative_bilinear_within:
- assumes "(f has_derivative f') (at x within s)"
- assumes "(g has_derivative g') (at x within s)"
- assumes "bounded_bilinear h"
- shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x within s)"
-proof-
- have "(g ---> g x) (at x within s)"
- apply(rule differentiable_imp_continuous_within[unfolded continuous_within])
- using assms(2) unfolding differentiable_def by auto
- moreover
- interpret f':bounded_linear f'
- using assms unfolding has_derivative_def by auto
- interpret g':bounded_linear g'
- using assms unfolding has_derivative_def by auto
- interpret h:bounded_bilinear h
- using assms by auto
- have "((\<lambda>y. f' (y - x)) ---> 0) (at x within s)"
- unfolding f'.zero[THEN sym]
- using bounded_linear.tendsto [of f' "\<lambda>y. y - x" 0 "at x within s"]
- using tendsto_diff [OF Lim_within_id tendsto_const, of x x s]
- unfolding id_def using assms(1) unfolding has_derivative_def by auto
- hence "((\<lambda>y. f x + f' (y - x)) ---> f x) (at x within s)"
- using tendsto_add[OF tendsto_const, of "\<lambda>y. f' (y - x)" 0 "at x within s" "f x"]
- by auto
- ultimately
- have *:"((\<lambda>x'. h (f x + f' (x' - x)) ((1/(norm (x' - x))) *\<^sub>R (g x' - (g x + g' (x' - x))))
- + h ((1/ (norm (x' - x))) *\<^sub>R (f x' - (f x + f' (x' - x)))) (g x')) ---> h (f x) 0 + h 0 (g x)) (at x within s)"
- apply-apply(rule tendsto_add) apply(rule_tac[!] Lim_bilinear[OF _ _ assms(3)])
- using assms(1-2) unfolding has_derivative_within by auto
- guess B using bounded_bilinear.pos_bounded[OF assms(3)] .. note B=this
- guess C using f'.pos_bounded .. note C=this
- guess D using g'.pos_bounded .. note D=this
- have bcd:"B * C * D > 0" using B C D by (auto intro!: mult_pos_pos)
- have **:"((\<lambda>y. (1/(norm(y - x))) *\<^sub>R (h (f'(y - x)) (g'(y - x)))) ---> 0) (at x within s)"
- unfolding Lim_within
- proof(rule,rule) case goal1
- hence "e/(B*C*D)>0" using B C D by(auto intro!:divide_pos_pos mult_pos_pos)
- thus ?case apply(rule_tac x="e/(B*C*D)" in exI,rule)
- proof(rule,rule,erule conjE)
- fix y assume as:"y \<in> s" "0 < dist y x" "dist y x < e / (B * C * D)"
- have "norm (h (f' (y - x)) (g' (y - x))) \<le> norm (f' (y - x)) * norm (g' (y - x)) * B" using B by auto
- also have "\<dots> \<le> (norm (y - x) * C) * (D * norm (y - x)) * B"
- apply(rule mult_right_mono)
- apply(rule mult_mono) using B C D
- by (auto simp add: field_simps intro!:mult_nonneg_nonneg)
- also have "\<dots> = (B * C * D * norm (y - x)) * norm (y - x)"
- by (auto simp add: field_simps)
- also have "\<dots> < e * norm (y - x)"
- apply(rule mult_strict_right_mono)
- using as(3)[unfolded dist_norm] and as(2)
- unfolding pos_less_divide_eq[OF bcd] by (auto simp add: field_simps)
- finally show "dist ((1 / norm (y - x)) *\<^sub>R h (f' (y - x)) (g' (y - x))) 0 < e"
- unfolding dist_norm apply-apply(cases "y = x")
- by(auto simp add: field_simps)
- qed
- qed
- have "bounded_linear (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))"
- apply (rule bounded_linear_add)
- apply (rule bounded_linear_compose [OF h.bounded_linear_right `bounded_linear g'`])
- apply (rule bounded_linear_compose [OF h.bounded_linear_left `bounded_linear f'`])
- done
- thus ?thesis using tendsto_add[OF * **] unfolding has_derivative_within
- unfolding g'.add f'.scaleR f'.add g'.scaleR f'.diff g'.diff
- h.add_right h.add_left scaleR_right_distrib h.scaleR_left h.scaleR_right h.diff_right h.diff_left
- scaleR_right_diff_distrib h.zero_right h.zero_left
- by(auto simp add:field_simps)
-qed
-
-lemma has_derivative_bilinear_at:
- assumes "(f has_derivative f') (at x)"
- assumes "(g has_derivative g') (at x)"
- assumes "bounded_bilinear h"
- shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x)"
- using has_derivative_bilinear_within[of f f' x UNIV g g' h] assms by simp
-
subsection {* Considering derivative @{typ "real \<Rightarrow> 'b\<Colon>real_normed_vector"} as a vector. *}
definition has_vector_derivative :: "(real \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'b \<Rightarrow> (real filter \<Rightarrow> bool)"
@@ -1805,7 +1527,7 @@
assumes "(g has_vector_derivative g') (at x)"
assumes "bounded_bilinear h"
shows "((\<lambda>x. h (f x) (g x)) has_vector_derivative (h (f x) g' + h f' (g x))) (at x)"
- using has_vector_derivative_bilinear_within[where s=UNIV] assms by simp
+ using has_vector_derivative_bilinear_within[OF assms] .
lemma has_vector_derivative_at_within:
"(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f') (at x within s)"
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Apr 09 21:22:15 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Apr 09 21:39:55 2013 +0200
@@ -890,16 +890,16 @@
lemma Liminf_within:
fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
- unfolding Liminf_def eventually_within_less
+ unfolding Liminf_def eventually_at
proof (rule SUPR_eq, simp_all add: Ball_def Bex_def, safe)
- fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
+ fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
by (auto simp: zero_less_dist_iff dist_commute)
then show "\<exists>r>0. INFI (Collect P) f \<le> INFI (S \<inter> ball x r - {x}) f"
by (intro exI[of _ d] INF_mono conjI `0 < d`) auto
next
fix d :: real assume "0 < d"
- then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
+ then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> xa \<noteq> x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
INFI (S \<inter> ball x d - {x}) f \<le> INFI (Collect P) f"
by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
(auto intro!: INF_mono exI[of _ d] simp: dist_commute)
@@ -908,16 +908,16 @@
lemma Limsup_within:
fixes f :: "'a::metric_space => 'b::complete_lattice"
shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
- unfolding Limsup_def eventually_within_less
+ unfolding Limsup_def eventually_at
proof (rule INFI_eq, simp_all add: Ball_def Bex_def, safe)
- fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
+ fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
by (auto simp: zero_less_dist_iff dist_commute)
then show "\<exists>r>0. SUPR (S \<inter> ball x r - {x}) f \<le> SUPR (Collect P) f"
by (intro exI[of _ d] SUP_mono conjI `0 < d`) auto
next
fix d :: real assume "0 < d"
- then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
+ then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> xa \<noteq> x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
SUPR (Collect P) f \<le> SUPR (S \<inter> ball x d - {x}) f"
by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
(auto intro!: SUP_mono exI[of _ d] simp: dist_commute)
--- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Apr 09 21:22:15 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Apr 09 21:39:55 2013 +0200
@@ -4405,8 +4405,8 @@
have "(f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x) has_derivative (\<lambda>x. 0) \<circ> (\<lambda>z. (0 - z *\<^sub>R c) + z *\<^sub>R x)) (at t within {0..1})"
apply(rule diff_chain_within) apply(rule has_derivative_add)
unfolding scaleR_simps
- apply(intro has_derivative_intros)
- apply(intro has_derivative_intros)
+ apply(intro FDERIV_intros)
+ apply(intro FDERIV_intros)
apply(rule has_derivative_within_subset,rule assms(6)[rule_format])
apply(rule *) apply safe apply(rule conv[unfolded scaleR_simps]) using `x\<in>s` `c\<in>s` by auto
thus "((\<lambda>xa. f ((1 - xa) *\<^sub>R c + xa *\<^sub>R x)) has_derivative (\<lambda>h. 0)) (at t within {0..1})" unfolding o_def .
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Apr 09 21:22:15 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Apr 09 21:39:55 2013 +0200
@@ -39,9 +39,6 @@
shows "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)"
by (fact tendsto_within_open)
-lemma Lim_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
- by (fact tendsto_within_subset)
-
lemma continuous_on_union:
"closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
by (fact continuous_on_closed_Un)
@@ -1205,7 +1202,7 @@
definition
indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a filter"
(infixr "indirection" 70) where
- "a indirection v = (at a) within {b. \<exists>c\<ge>0. b - a = scaleR c v}"
+ "a indirection v = at a within {b. \<exists>c\<ge>0. b - a = scaleR c v}"
text {* Identify Trivial limits, where we can't approach arbitrarily closely. *}
@@ -1215,7 +1212,7 @@
assume "trivial_limit (at a within S)"
thus "\<not> a islimpt S"
unfolding trivial_limit_def
- unfolding eventually_within eventually_at_topological
+ unfolding eventually_at_topological
unfolding islimpt_def
apply (clarsimp simp add: set_eq_iff)
apply (rename_tac T, rule_tac x=T in exI)
@@ -1225,7 +1222,7 @@
assume "\<not> a islimpt S"
thus "trivial_limit (at a within S)"
unfolding trivial_limit_def
- unfolding eventually_within eventually_at_topological
+ unfolding eventually_at_topological
unfolding islimpt_def
apply clarsimp
apply (rule_tac x=T in exI)
@@ -1292,11 +1289,11 @@
lemma Lim_within_le: "(f ---> l)(at a within S) \<longleftrightarrow>
(\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a <= d \<longrightarrow> dist (f x) l < e)"
- by (auto simp add: tendsto_iff eventually_within_le)
+ by (auto simp add: tendsto_iff eventually_at_le dist_nz)
lemma Lim_within: "(f ---> l) (at a within S) \<longleftrightarrow>
(\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)"
- by (auto simp add: tendsto_iff eventually_within_less)
+ by (auto simp add: tendsto_iff eventually_at dist_nz)
lemma Lim_at: "(f ---> l) (at a) \<longleftrightarrow>
(\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)"
@@ -1311,12 +1308,12 @@
text{* The expected monotonicity property. *}
-lemma Lim_within_empty: "(f ---> l) (net within {})"
- unfolding tendsto_def Limits.eventually_within by simp
-
-lemma Lim_Un: assumes "(f ---> l) (net within S)" "(f ---> l) (net within T)"
- shows "(f ---> l) (net within (S \<union> T))"
- using assms unfolding tendsto_def Limits.eventually_within
+lemma Lim_within_empty: "(f ---> l) (at x within {})"
+ unfolding tendsto_def eventually_at_filter by simp
+
+lemma Lim_Un: assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)"
+ shows "(f ---> l) (at x within (S \<union> T))"
+ using assms unfolding tendsto_def eventually_at_filter
apply clarify
apply (drule spec, drule (1) mp, drule (1) mp)
apply (drule spec, drule (1) mp, drule (1) mp)
@@ -1324,17 +1321,16 @@
done
lemma Lim_Un_univ:
- "(f ---> l) (net within S) \<Longrightarrow> (f ---> l) (net within T) \<Longrightarrow> S \<union> T = UNIV
- ==> (f ---> l) net"
- by (metis Lim_Un within_UNIV)
+ "(f ---> l) (at x within S) \<Longrightarrow> (f ---> l) (at x within T) \<Longrightarrow> S \<union> T = UNIV
+ ==> (f ---> l) (at x)"
+ by (metis Lim_Un)
text{* Interrelations between restricted and unrestricted limits. *}
-lemma Lim_at_within: "(f ---> l) net ==> (f ---> l)(net within S)"
- (* FIXME: rename *)
- unfolding tendsto_def Limits.eventually_within
- apply (clarify, drule spec, drule (1) mp, drule (1) mp)
- by (auto elim!: eventually_elim1)
+
+lemma Lim_at_within: (* FIXME: rename *)
+ "(f ---> l) (at x) \<Longrightarrow> (f ---> l) (at x within S)"
+ by (metis order_refl filterlim_mono subset_UNIV at_le)
lemma eventually_within_interior:
assumes "x \<in> interior S"
@@ -1343,7 +1339,7 @@
from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" ..
{ assume "?lhs"
then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
- unfolding Limits.eventually_within eventually_at_topological
+ unfolding eventually_at_topological
by auto
with T have "open (A \<inter> T)" "x \<in> A \<inter> T" "\<forall>y\<in>(A \<inter> T). y \<noteq> x \<longrightarrow> P y"
by auto
@@ -1351,15 +1347,14 @@
unfolding eventually_at_topological by auto
} moreover
{ assume "?rhs" hence "?lhs"
- unfolding Limits.eventually_within
- by (auto elim: eventually_elim1)
+ by (auto elim: eventually_elim1 simp: eventually_at_filter)
} ultimately
show "?thesis" ..
qed
lemma at_within_interior:
"x \<in> interior S \<Longrightarrow> at x within S = at x"
- by (simp add: filter_eq_iff eventually_within_interior)
+ unfolding filter_eq_iff by (intro allI eventually_within_interior)
lemma Lim_within_LIMSEQ:
fixes a :: "'a::metric_space"
@@ -1386,17 +1381,14 @@
by (auto intro: cInf_lower)
with a have "a < f y" by (blast intro: less_le_trans) }
then show "eventually (\<lambda>x. a < f x) (at x within ({x<..} \<inter> I))"
- by (auto simp: Topological_Spaces.eventually_within intro: exI[of _ 1] zero_less_one)
+ by (auto simp: eventually_at_filter intro: exI[of _ 1] zero_less_one)
next
fix a assume "Inf (f ` ({x<..} \<inter> I)) < a"
from cInf_lessD[OF _ this] e obtain y where y: "x < y" "y \<in> I" "f y < a" by auto
- show "eventually (\<lambda>x. f x < a) (at x within ({x<..} \<inter> I))"
- unfolding within_within_eq[symmetric]
- Topological_Spaces.eventually_within[of _ _ I] eventually_at_right
- proof (safe intro!: exI[of _ y] y)
- fix z assume "x < z" "z \<in> I" "z < y"
- with mono[OF `z\<in>I` `y\<in>I`] `f y < a` show "f z < a" by (auto simp: less_imp_le)
- qed
+ then have "eventually (\<lambda>x. x \<in> I \<longrightarrow> f x < a) (at_right x)"
+ unfolding eventually_at_right by (metis less_imp_le le_less_trans mono)
+ then show "eventually (\<lambda>x. f x < a) (at x within ({x<..} \<inter> I))"
+ unfolding eventually_at_filter by eventually_elim simp
qed
qed
@@ -1540,7 +1532,7 @@
text{* These are special for limits out of the same vector space. *}
lemma Lim_within_id: "(id ---> a) (at a within s)"
- unfolding id_def by (rule tendsto_ident_at_within)
+ unfolding id_def by (rule tendsto_ident_at)
lemma Lim_at_id: "(id ---> a) (at a)"
unfolding id_def by (rule tendsto_ident_at)
@@ -1567,13 +1559,13 @@
lemma lim_within_interior:
"x \<in> interior S \<Longrightarrow> (f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x)"
- by (simp add: at_within_interior)
+ by (metis at_within_interior)
lemma netlimit_within_interior:
fixes x :: "'a::{t2_space,perfect_space}"
assumes "x \<in> interior S"
shows "netlimit (at x within S) = x"
-using assms by (simp add: at_within_interior netlimit_at)
+using assms by (metis at_within_interior netlimit_at)
text{* Transformation of limit. *}
@@ -1596,8 +1588,7 @@
shows "(g ---> l) (at x within S)"
proof (rule Lim_transform_eventually)
show "eventually (\<lambda>x. f x = g x) (at x within S)"
- unfolding eventually_within_less
- using assms(1,2) by auto
+ using assms(1,2) by (auto simp: dist_nz eventually_at)
show "(f ---> l) (at x within S)" by fact
qed
@@ -1622,7 +1613,7 @@
proof (rule Lim_transform_eventually)
show "(f ---> l) (at a within S)" by fact
show "eventually (\<lambda>x. f x = g x) (at a within S)"
- unfolding Limits.eventually_within eventually_at_topological
+ unfolding eventually_at_topological
by (rule exI [where x="- {b}"], simp add: open_Compl assms)
qed
@@ -1655,7 +1646,7 @@
assumes "a = b" "x = y" "S = T"
assumes "\<And>x. x \<noteq> b \<Longrightarrow> x \<in> T \<Longrightarrow> f x = g x"
shows "(f ---> x) (at a within S) \<longleftrightarrow> (g ---> y) (at b within T)"
- unfolding tendsto_def Limits.eventually_within eventually_at_topological
+ unfolding tendsto_def eventually_at_topological
using assms by simp
lemma Lim_cong_at(*[cong add]*):
@@ -3759,7 +3750,7 @@
lemma continuous_within_subset:
"continuous (at x within s) f \<Longrightarrow> t \<subseteq> s
==> continuous (at x within t) f"
- unfolding continuous_within by(metis Lim_within_subset)
+ unfolding continuous_within by(metis tendsto_within_subset)
lemma continuous_on_interior:
shows "continuous_on s f \<Longrightarrow> x \<in> interior s \<Longrightarrow> continuous (at x) f"
@@ -3768,7 +3759,7 @@
lemma continuous_on_eq:
"(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on s g"
- unfolding continuous_on_def tendsto_def Limits.eventually_within
+ unfolding continuous_on_def tendsto_def eventually_at_topological
by simp
text {* Characterization of various kinds of continuity in terms of sequences. *}
@@ -3783,7 +3774,7 @@
{ fix x::"nat \<Rightarrow> 'a" assume x:"\<forall>n. x n \<in> s" "\<forall>e>0. eventually (\<lambda>n. dist (x n) a < e) sequentially"
fix T::"'b set" assume "open T" and "f a \<in> T"
with `?lhs` obtain d where "d>0" and d:"\<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> f x \<in> T"
- unfolding continuous_within tendsto_def eventually_within_less by auto
+ unfolding continuous_within tendsto_def eventually_at by (auto simp: dist_nz)
have "eventually (\<lambda>n. dist (x n) a < d) sequentially"
using x(2) `d>0` by simp
hence "eventually (\<lambda>n. (f \<circ> x) n \<in> T) sequentially"
@@ -4015,7 +4006,7 @@
lemma continuous_at_open:
shows "continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t --> (\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x' \<in> s. (f x') \<in> t)))"
-unfolding continuous_within_topological [of x UNIV f, unfolded within_UNIV]
+unfolding continuous_within_topological [of x UNIV f]
unfolding imp_conjL by (intro all_cong imp_cong ex_cong conj_cong refl) auto
lemma continuous_imp_tendsto:
@@ -4181,7 +4172,7 @@
hence "eventually (\<lambda>y. f y \<noteq> a) (at x within s)"
using `a \<notin> U` by (fast elim: eventually_mono [rotated])
thus ?thesis
- using `f x \<noteq> a` by (auto simp: dist_commute zero_less_dist_iff eventually_within_less)
+ using `f x \<noteq> a` by (auto simp: dist_commute zero_less_dist_iff eventually_at)
qed
lemma continuous_at_avoid:
@@ -4514,7 +4505,7 @@
proof (rule continuous_attains_sup [OF assms])
{ fix x assume "x\<in>s"
have "(dist a ---> dist a x) (at x within s)"
- by (intro tendsto_dist tendsto_const Lim_at_within tendsto_ident_at)
+ by (intro tendsto_dist tendsto_const tendsto_ident_at)
}
thus "continuous_on s (dist a)"
unfolding continuous_on ..
@@ -5350,7 +5341,7 @@
assumes "\<And>x. isCont f x" and "open s" shows "open (f -` s)"
proof -
from assms(1) have "continuous_on UNIV f"
- unfolding isCont_def continuous_on_def within_UNIV by simp
+ unfolding isCont_def continuous_on_def by simp
hence "open {x \<in> UNIV. f x \<in> s}"
using open_UNIV `open s` by (rule continuous_open_preimage)
thus "open (f -` s)"
@@ -5508,14 +5499,13 @@
text{* Limits relative to a union. *}
lemma eventually_within_Un:
- "eventually P (net within (s \<union> t)) \<longleftrightarrow>
- eventually P (net within s) \<and> eventually P (net within t)"
- unfolding Limits.eventually_within
+ "eventually P (at x within (s \<union> t)) \<longleftrightarrow> eventually P (at x within s) \<and> eventually P (at x within t)"
+ unfolding eventually_at_filter
by (auto elim!: eventually_rev_mp)
lemma Lim_within_union:
- "(f ---> l) (net within (s \<union> t)) \<longleftrightarrow>
- (f ---> l) (net within s) \<and> (f ---> l) (net within t)"
+ "(f ---> l) (at x within (s \<union> t)) \<longleftrightarrow>
+ (f ---> l) (at x within s) \<and> (f ---> l) (at x within t)"
unfolding tendsto_def
by (auto simp add: eventually_within_Un)
--- a/src/HOL/Probability/Fin_Map.thy Tue Apr 09 21:22:15 2013 +0200
+++ b/src/HOL/Probability/Fin_Map.thy Tue Apr 09 21:39:55 2013 +0200
@@ -206,8 +206,7 @@
lemma continuous_proj:
shows "continuous_on s (\<lambda>x. (x)\<^isub>F i)"
- unfolding continuous_on_def
- by (safe intro!: tendsto_proj tendsto_ident_at_within)
+ unfolding continuous_on_def by (safe intro!: tendsto_proj tendsto_ident_at)
instance finmap :: (type, first_countable_topology) first_countable_topology
proof
--- a/src/HOL/Real_Vector_Spaces.thy Tue Apr 09 21:22:15 2013 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Tue Apr 09 21:39:55 2013 +0200
@@ -1048,6 +1048,73 @@
end
+lemma bounded_linear_ident[simp]: "bounded_linear (\<lambda>x. x)"
+ by default (auto intro!: exI[of _ 1])
+
+lemma bounded_linear_zero[simp]: "bounded_linear (\<lambda>x. 0)"
+ by default (auto intro!: exI[of _ 1])
+
+lemma bounded_linear_add:
+ assumes "bounded_linear f"
+ assumes "bounded_linear g"
+ shows "bounded_linear (\<lambda>x. f x + g x)"
+proof -
+ interpret f: bounded_linear f by fact
+ interpret g: bounded_linear g by fact
+ show ?thesis
+ proof
+ from f.bounded obtain Kf where Kf: "\<And>x. norm (f x) \<le> norm x * Kf" by blast
+ from g.bounded obtain Kg where Kg: "\<And>x. norm (g x) \<le> norm x * Kg" by blast
+ show "\<exists>K. \<forall>x. norm (f x + g x) \<le> norm x * K"
+ using add_mono[OF Kf Kg]
+ by (intro exI[of _ "Kf + Kg"]) (auto simp: field_simps intro: norm_triangle_ineq order_trans)
+ qed (simp_all add: f.add g.add f.scaleR g.scaleR scaleR_right_distrib)
+qed
+
+lemma bounded_linear_minus:
+ assumes "bounded_linear f"
+ shows "bounded_linear (\<lambda>x. - f x)"
+proof -
+ interpret f: bounded_linear f by fact
+ show ?thesis apply (unfold_locales)
+ apply (simp add: f.add)
+ apply (simp add: f.scaleR)
+ apply (simp add: f.bounded)
+ done
+qed
+
+lemma bounded_linear_compose:
+ assumes "bounded_linear f"
+ assumes "bounded_linear g"
+ shows "bounded_linear (\<lambda>x. f (g x))"
+proof -
+ interpret f: bounded_linear f by fact
+ interpret g: bounded_linear g by fact
+ show ?thesis proof (unfold_locales)
+ fix x y show "f (g (x + y)) = f (g x) + f (g y)"
+ by (simp only: f.add g.add)
+ next
+ fix r x show "f (g (scaleR r x)) = scaleR r (f (g x))"
+ by (simp only: f.scaleR g.scaleR)
+ next
+ from f.pos_bounded
+ obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by fast
+ from g.pos_bounded
+ obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by fast
+ show "\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K"
+ proof (intro exI allI)
+ fix x
+ have "norm (f (g x)) \<le> norm (g x) * Kf"
+ using f .
+ also have "\<dots> \<le> (norm x * Kg) * Kf"
+ using g Kf [THEN order_less_imp_le] by (rule mult_right_mono)
+ also have "(norm x * Kg) * Kf = norm x * (Kg * Kf)"
+ by (rule mult_assoc)
+ finally show "norm (f (g x)) \<le> norm x * (Kg * Kf)" .
+ qed
+ qed
+qed
+
lemma bounded_bilinear_mult:
"bounded_bilinear (op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)"
apply (rule bounded_bilinear.intro)
@@ -1069,6 +1136,12 @@
using bounded_bilinear_mult
by (rule bounded_bilinear.bounded_linear_right)
+lemmas bounded_linear_mult_const =
+ bounded_linear_mult_left [THEN bounded_linear_compose]
+
+lemmas bounded_linear_const_mult =
+ bounded_linear_mult_right [THEN bounded_linear_compose]
+
lemma bounded_linear_divide:
"bounded_linear (\<lambda>x::'a::real_normed_field. x / y)"
unfolding divide_inverse by (rule bounded_linear_mult_left)
@@ -1093,6 +1166,18 @@
lemma bounded_linear_of_real: "bounded_linear (\<lambda>r. of_real r)"
unfolding of_real_def by (rule bounded_linear_scaleR_left)
+lemma real_bounded_linear:
+ fixes f :: "real \<Rightarrow> real"
+ shows "bounded_linear f \<longleftrightarrow> (\<exists>c::real. f = (\<lambda>x. x * c))"
+proof -
+ { fix x assume "bounded_linear f"
+ then interpret bounded_linear f .
+ from scaleR[of x 1] have "f x = x * f 1"
+ by simp }
+ then show ?thesis
+ by (auto intro: exI[of _ "f 1"] bounded_linear_mult_left)
+qed
+
instance real_normed_algebra_1 \<subseteq> perfect_space
proof
fix x::'a
@@ -1117,19 +1202,18 @@
done
lemma eventually_at:
- fixes a :: "'a::metric_space"
- shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
-unfolding at_def eventually_within eventually_nhds_metric by auto
+ fixes a :: "'a :: metric_space"
+ shows "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
+ unfolding eventually_at_filter eventually_nhds_metric by (auto simp: dist_nz)
-lemma eventually_within_less:
- fixes a :: "'a :: metric_space"
- shows "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
- unfolding eventually_within eventually_at dist_nz by auto
-
-lemma eventually_within_le:
- fixes a :: "'a :: metric_space"
- shows "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a \<le> d \<longrightarrow> P x)"
- unfolding eventually_within_less by auto (metis dense order_le_less_trans)
+lemma eventually_at_le:
+ fixes a :: "'a::metric_space"
+ shows "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<and> dist x a \<le> d \<longrightarrow> P x)"
+ unfolding eventually_at_filter eventually_nhds_metric
+ apply auto
+ apply (rule_tac x="d / 2" in exI)
+ apply auto
+ done
lemma tendstoI:
fixes l :: "'a :: metric_space"
@@ -1200,7 +1284,7 @@
lemma LIM_def: "f -- (a::'a::metric_space) --> (L::'b::metric_space) =
(\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s
--> dist (f x) L < r)"
-unfolding tendsto_iff eventually_at ..
+ unfolding tendsto_iff eventually_at by simp
lemma metric_LIM_I:
"(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)
@@ -1235,8 +1319,8 @@
assumes g: "g -- b --> c"
assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b"
shows "(\<lambda>x. g (f x)) -- a --> c"
- using g f inj [folded eventually_at]
- by (rule tendsto_compose_eventually)
+ using inj
+ by (intro tendsto_compose_eventually[OF g f]) (auto simp: eventually_at)
lemma metric_isCont_LIM_compose2:
fixes f :: "'a :: metric_space \<Rightarrow> _"
--- a/src/HOL/TPTP/ATP_Theory_Export.thy Tue Apr 09 21:22:15 2013 +0200
+++ b/src/HOL/TPTP/ATP_Theory_Export.thy Tue Apr 09 21:39:55 2013 +0200
@@ -17,15 +17,16 @@
ML {*
val do_it = false (* switch to "true" to generate the files *)
+val ctxt = @{context}
val thy = @{theory List}
-val ctxt = @{context}
+val infer_policy = Unchecked_Inferences
*}
ML {*
if do_it then
"/tmp/axs_tc_native.dfg"
|> generate_atp_inference_file_for_theory ctxt thy (DFG Polymorphic)
- "tc_native"
+ infer_policy "tc_native"
else
()
*}
@@ -33,8 +34,8 @@
ML {*
if do_it then
"/tmp/infs_poly_guards_query_query.tptp"
- |> generate_atp_inference_file_for_theory ctxt thy FOF
- "poly_guards_query_query"
+ |> generate_atp_inference_file_for_theory ctxt thy FOF infer_policy
+ "poly_guards??"
else
()
*}
@@ -42,8 +43,17 @@
ML {*
if do_it then
"/tmp/infs_poly_tags_query_query.tptp"
- |> generate_atp_inference_file_for_theory ctxt thy FOF
- "poly_tags_query_query"
+ |> generate_atp_inference_file_for_theory ctxt thy FOF infer_policy
+ "poly_tags??"
+else
+ ()
+*}
+
+ML {*
+if do_it then
+ "/tmp/casc_ltb_isa"
+ |> generate_casc_lbt_isa_files_for_theory ctxt thy FOF infer_policy
+ "poly_tags??"
else
()
*}
--- a/src/HOL/TPTP/atp_theory_export.ML Tue Apr 09 21:22:15 2013 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Tue Apr 09 21:39:55 2013 +0200
@@ -9,8 +9,15 @@
sig
type atp_format = ATP_Problem.atp_format
+ datatype inference_policy =
+ No_Inferences | Unchecked_Inferences | Checked_Inferences
+
val generate_atp_inference_file_for_theory :
- Proof.context -> theory -> atp_format -> string -> string -> unit
+ Proof.context -> theory -> atp_format -> inference_policy -> string
+ -> string -> unit
+ val generate_casc_lbt_isa_files_for_theory :
+ Proof.context -> theory -> atp_format -> inference_policy -> string
+ -> string -> unit
end;
structure ATP_Theory_Export : ATP_THEORY_EXPORT =
@@ -21,30 +28,10 @@
open ATP_Problem_Generate
open ATP_Systems
-val fact_name_of = prefix fact_prefix o ascii_of
+datatype inference_policy =
+ No_Inferences | Unchecked_Inferences | Checked_Inferences
-fun inference_term [] = NONE
- | inference_term ss =
- ATerm (("inference", []),
- [ATerm (("isabelle", []), []),
- ATerm ((tptp_empty_list, []), []),
- ATerm ((tptp_empty_list, []),
- map (fn s => ATerm ((s, []), [])) ss)])
- |> SOME
-fun inference infers ident =
- these (AList.lookup (op =) infers ident) |> inference_term
-fun add_inferences_to_problem_line infers
- (Formula ((ident, alt), Axiom, phi, NONE, tms)) =
- Formula ((ident, alt), Lemma, phi, inference infers ident, tms)
- | add_inferences_to_problem_line _ line = line
-fun add_inferences_to_problem infers =
- map (apsnd (map (add_inferences_to_problem_line infers)))
-
-fun ident_of_problem_line (Class_Decl (ident, _, _)) = ident
- | ident_of_problem_line (Type_Decl (ident, _, _)) = ident
- | ident_of_problem_line (Sym_Decl (ident, _, _)) = ident
- | ident_of_problem_line (Class_Memb (ident, _, _, _)) = ident
- | ident_of_problem_line (Formula ((ident, _), _, _, _, _)) = ident
+val fact_name_of = prefix fact_prefix o ascii_of
fun atp_for_format (THF (Polymorphic, _, _, _)) = dummy_thfN
| atp_for_format (THF (Monomorphic, _, _, _)) = satallaxN
@@ -56,7 +43,9 @@
| atp_for_format CNF_UEQ = waldmeisterN
| atp_for_format CNF = eN
-fun run_some_atp ctxt format problem =
+val atp_timeout = seconds 0.5
+
+fun run_atp ctxt format problem =
let
val thy = Proof_Context.theory_of ctxt
val prob_file = File.tmp_path (Path.explode "prob")
@@ -69,29 +58,76 @@
val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec)
val command =
File.shell_path (Path.explode path) ^ " " ^
- arguments ctxt false "" (seconds 1.0) (File.shell_path prob_file)
+ arguments ctxt false "" atp_timeout (File.shell_path prob_file)
(ord, K [], K [])
- in
- TimeLimit.timeLimit (seconds 0.3) Isabelle_System.bash_output command
- |> fst
- |> extract_tstplike_proof_and_outcome false proof_delims known_failures
- |> snd
- end
- handle TimeLimit.TimeOut => SOME TimedOut
+ val outcome =
+ TimeLimit.timeLimit atp_timeout Isabelle_System.bash_output command
+ |> fst
+ |> extract_tstplike_proof_and_outcome false proof_delims known_failures
+ |> snd
+ handle TimeLimit.TimeOut => SOME TimedOut
+ val _ =
+ tracing ("Ran ATP: " ^
+ (case outcome of
+ NONE => "Success"
+ | SOME failure => string_for_failure failure))
+ in outcome end
+
+fun is_problem_line_reprovable ctxt format prelude axioms deps
+ (Formula (ident', _, phi, _, _)) =
+ is_none (run_atp ctxt format
+ ((factsN, Formula (ident', Conjecture, phi, NONE, []) ::
+ map_filter (Symtab.lookup axioms) deps) ::
+ prelude))
+ | is_problem_line_reprovable _ _ _ _ _ _ = false
+
+fun inference_term _ [] = NONE
+ | inference_term check_infs ss =
+ ATerm (("inference", []),
+ [ATerm (("checked_isabelle" |> not check_infs ? prefix "un", []), []),
+ ATerm ((tptp_empty_list, []), []),
+ ATerm ((tptp_empty_list, []),
+ map (fn s => ATerm ((s, []), [])) ss)])
+ |> SOME
-val tautology_prefixes =
- [@{theory HOL}, @{theory Meson}, @{theory ATP}, @{theory Metis}]
- |> map (fact_name_of o Context.theory_name)
+fun add_inferences_to_problem_line ctxt format check_infs prelude axioms infers
+ (line as Formula ((ident, alt), Axiom, phi, NONE, tms)) =
+ let
+ val deps =
+ case these (AList.lookup (op =) infers ident) of
+ [] => []
+ | deps =>
+ if check_infs andalso
+ not (is_problem_line_reprovable ctxt format prelude axioms deps
+ line) then
+ []
+ else
+ deps
+ in
+ Formula ((ident, alt), Lemma, phi, inference_term check_infs deps, tms)
+ end
+ | add_inferences_to_problem_line _ _ _ _ _ _ line = line
-fun is_problem_line_tautology ctxt format
- (Formula ((ident, alt), _, phi, _, _)) =
- exists (fn prefix => String.isPrefix prefix ident)
- tautology_prefixes andalso
- is_none (run_some_atp ctxt format
- [(factsN, [Formula ((ident, alt), Conjecture, phi, NONE, [])])])
- | is_problem_line_tautology _ _ _ = false
+fun add_inferences_to_problem ctxt format check_infs prelude infers problem =
+ let
+ fun add_if_axiom (axiom as Formula ((ident, _), Axiom, _, _, _)) =
+ Symtab.default (ident, axiom)
+ | add_if_axiom _ = I
+ val add_axioms_of_problem = fold (fold add_if_axiom o snd)
+ val axioms = Symtab.empty |> check_infs ? add_axioms_of_problem problem
+ in
+ map (apsnd (map (add_inferences_to_problem_line ctxt format check_infs
+ prelude axioms infers))) problem
+ end
+
+fun ident_of_problem_line (Class_Decl (ident, _, _)) = ident
+ | ident_of_problem_line (Type_Decl (ident, _, _)) = ident
+ | ident_of_problem_line (Sym_Decl (ident, _, _)) = ident
+ | ident_of_problem_line (Class_Memb (ident, _, _, _)) = ident
+ | ident_of_problem_line (Formula ((ident, _), _, _, _, _)) = ident
fun order_facts ord = sort (ord o pairself ident_of_problem_line)
+
fun order_problem_facts _ [] = []
| order_problem_facts ord ((heading, lines) :: problem) =
if heading = factsN then (heading, order_facts ord lines) :: problem
@@ -117,65 +153,195 @@
fun heading_sort_key heading =
if String.isPrefix "Relevant fact" heading then "_" ^ heading else heading
-fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name =
+fun problem_for_theory ctxt thy format infer_policy type_enc =
let
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
val type_enc =
type_enc |> type_enc_from_string Non_Strict
|> adjust_type_enc format
val mono = not (is_type_enc_polymorphic type_enc)
- val path = file_name |> Path.explode
- val _ = File.write path ""
val facts =
Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true false
Symtab.empty [] [] css_table
|> sort (Sledgehammer_MaSh.crude_thm_ord o pairself snd)
- val atp_problem =
+ val problem =
facts
|> map (fn ((_, loc), th) =>
((Thm.get_name_hint th, loc),
th |> prop_of |> mono ? monomorphize_term ctxt))
|> prepare_atp_problem ctxt format Axiom type_enc Exporter combsN false
false true [] @{prop False}
- |> #1
- val atp_problem =
- atp_problem
- |> map (apsnd (filter_out (is_problem_line_tautology ctxt format)))
- |> sort_wrt (heading_sort_key o fst)
+ |> #1 |> sort_wrt (heading_sort_key o fst)
+ val prelude = fst (split_last problem)
val name_tabs = Sledgehammer_Fact.build_name_tables Thm.get_name_hint facts
val infers =
- facts
- |> map (fn (_, th) =>
- (fact_name_of (Thm.get_name_hint th),
- th |> Sledgehammer_Util.thms_in_proof (SOME name_tabs)
- |> map fact_name_of))
- val all_atp_problem_names =
- atp_problem |> maps (map ident_of_problem_line o snd)
+ if infer_policy = No_Inferences then
+ []
+ else
+ facts
+ |> map (fn (_, th) =>
+ (fact_name_of (Thm.get_name_hint th),
+ th |> Sledgehammer_Util.thms_in_proof (SOME name_tabs)
+ |> map fact_name_of))
+ val all_problem_names =
+ problem |> maps (map ident_of_problem_line o snd)
+ |> distinct (op =)
+ val all_problem_name_set = Symtab.make (map (rpair ()) all_problem_names)
val infers =
- infers |> filter (member (op =) all_atp_problem_names o fst)
- |> map (apsnd (filter (member (op =) all_atp_problem_names)))
+ infers |> filter (Symtab.defined all_problem_name_set o fst)
+ |> map (apsnd (filter (Symtab.defined all_problem_name_set)))
+ val maybe_add_edge = perhaps o try o String_Graph.add_edge_acyclic
val ordered_names =
String_Graph.empty
- |> fold (String_Graph.new_node o rpair ()) all_atp_problem_names
+ |> fold (String_Graph.new_node o rpair ()) all_problem_names
|> fold (fn (to, froms) =>
- fold (fn from => String_Graph.add_edge (from, to)) froms)
+ fold (fn from => maybe_add_edge (from, to)) froms)
infers
- |> fold (fn (to, from) => String_Graph.add_edge_acyclic (from, to))
- (tl all_atp_problem_names
- ~~ fst (split_last all_atp_problem_names))
+ |> fold (fn (to, from) => maybe_add_edge (from, to))
+ (tl all_problem_names ~~ fst (split_last all_problem_names))
|> String_Graph.topological_order
val order_tab =
Symtab.empty
|> fold (Symtab.insert (op =))
(ordered_names ~~ (1 upto length ordered_names))
val name_ord = int_ord o pairself (the o Symtab.lookup order_tab)
- val atp_problem =
- atp_problem
- |> (case format of DFG _ => I | _ => add_inferences_to_problem infers)
- |> order_problem_facts name_ord
- val ord = effective_term_order ctxt eN (* dummy *)
- val ss = lines_for_atp_problem format ord (K []) atp_problem
+ in
+ problem
+ |> (case format of
+ DFG _ => I
+ | _ => add_inferences_to_problem ctxt format
+ (infer_policy = Checked_Inferences) prelude infers)
+ |> order_problem_facts name_ord
+ end
+
+fun lines_for_problem ctxt format =
+ lines_for_atp_problem format (effective_term_order ctxt eN (* dummy *)) (K [])
+
+fun write_lines path ss =
+ let
+ val _ = File.write path ""
val _ = app (File.append path) ss
in () end
+fun generate_atp_inference_file_for_theory ctxt thy format infer_policy type_enc
+ file_name =
+ let
+ val problem = problem_for_theory ctxt thy format infer_policy type_enc
+ val ss = lines_for_problem ctxt format problem
+ in write_lines (Path.explode file_name) ss end
+
+fun ap dir = Path.append dir o Path.explode
+
+fun chop_maximal_groups eq xs =
+ let
+ val rev_xs = rev xs
+ fun chop_group _ [] = []
+ | chop_group n (xs as x :: _) =
+ let
+ val n' = find_index (curry eq x) rev_xs
+ val (ws', xs') = chop (n - n') xs
+ in ws' :: chop_group n' xs' end
+ in chop_group (length xs) xs end
+
+fun theory_name_of_fact (Formula ((_, alt), _, _, _, _)) =
+ (case first_field Long_Name.separator alt of
+ NONE => alt
+ | SOME (thy, _) => thy)
+ | theory_name_of_fact _ = ""
+
+val problem_suffix = ".p"
+val include_suffix = ".ax"
+
+val file_order_name = "FilesInProcessingOrder"
+val problem_order_name = "ProblemsInProcessingOrder"
+val problem_name = "problems"
+val include_name = "incl"
+val prelude_base_name = "prelude"
+val prelude_name = prelude_base_name ^ include_suffix
+
+val encode_meta = Sledgehammer_MaSh.encode_str
+
+val include_base_name_of_fact = encode_meta o theory_name_of_fact
+
+fun include_line base_name =
+ "include('" ^ include_name ^ "/" ^ base_name ^ include_suffix ^ "').\n"
+
+val hol_base_name = encode_meta "HOL"
+
+fun should_generate_problem thy base_name (Formula ((_, alt), _, _, _, _)) =
+ case try (Global_Theory.get_thm thy) alt of
+ SOME th =>
+ (* This is a crude hack to detect theorems stated and proved by the user (as
+ opposed to those derived by various packages). In addition, we leave out
+ everything in "HOL" as too basic to be interesting. *)
+ Thm.legacy_get_kind th <> "" andalso base_name <> hol_base_name
+ | NONE => false
+
+(* Convention: theoryname__goalname *)
+fun problem_name_of base_name n alt =
+ base_name ^ "__" ^ string_of_int n ^ "_" ^
+ perhaps (try (unprefix (base_name ^ "_"))) alt ^ problem_suffix
+
+fun generate_casc_lbt_isa_files_for_theory ctxt thy format infer_policy type_enc
+ dir_name =
+ let
+ val dir = Path.explode dir_name
+ val _ = Isabelle_System.mkdir dir
+ val file_order_path = ap dir file_order_name
+ val _ = File.write file_order_path ""
+ val problem_order_path = ap dir problem_order_name
+ val _ = File.write problem_order_path ""
+ val problem_dir = ap dir problem_name
+ val _ = Isabelle_System.mkdir problem_dir
+ val include_dir = ap problem_dir include_name
+ val _ = Isabelle_System.mkdir include_dir
+ val (prelude, groups) =
+ problem_for_theory ctxt thy format infer_policy type_enc
+ |> split_last
+ ||> (snd
+ #> chop_maximal_groups (op = o pairself theory_name_of_fact)
+ #> map (`(include_base_name_of_fact o hd)))
+ fun write_prelude () =
+ let val ss = lines_for_problem ctxt format prelude in
+ File.append file_order_path (prelude_base_name ^ "\n");
+ write_lines (ap include_dir prelude_name) ss
+ end
+ fun write_include_file (base_name, facts) =
+ let
+ val name = base_name ^ include_suffix
+ val ss = lines_for_problem ctxt format [(factsN, facts)]
+ in
+ File.append file_order_path (base_name ^ "\n");
+ write_lines (ap include_dir name) ss
+ end
+ fun write_problem_files _ _ _ [] = ()
+ | write_problem_files _ includes [] groups =
+ write_problem_files 1 includes includes groups
+ | write_problem_files n includes _ ((base_name, []) :: groups) =
+ write_problem_files n (includes @ [include_line base_name]) [] groups
+ | write_problem_files n includes seen
+ ((base_name, fact :: facts) :: groups) =
+ let val fact_s = tptp_string_for_line format fact in
+ (if should_generate_problem thy base_name fact then
+ let
+ val (name, conj) =
+ (case fact of
+ Formula ((ident, alt), _, phi, _, _) =>
+ (problem_name_of base_name n (encode_meta alt),
+ Formula ((ident, alt), Conjecture, phi, NONE, [])))
+ val conj_s = tptp_string_for_line format conj
+ in
+ File.append problem_order_path (name ^ "\n");
+ write_lines (ap problem_dir name) (seen @ [conj_s])
+ end
+ else
+ ();
+ write_problem_files (n + 1) includes (seen @ [fact_s])
+ ((base_name, facts) :: groups))
+ end
+ val _ = write_prelude ()
+ val _ = app write_include_file groups
+ val _ = write_problem_files 1 [include_line prelude_base_name] [] groups
+ in () end
+
end;
--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Apr 09 21:22:15 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Apr 09 21:39:55 2013 +0200
@@ -124,6 +124,7 @@
val formula_map :
('c -> 'e) -> ('a, 'b, 'c, 'd) formula -> ('a, 'b, 'e, 'd) formula
val is_format_higher_order : atp_format -> bool
+ val tptp_string_for_line : atp_format -> string problem_line -> string
val lines_for_atp_problem :
atp_format -> term_order -> (unit -> (string * int) list) -> string problem
-> string list
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Apr 09 21:22:15 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Apr 09 21:39:55 2013 +0200
@@ -477,23 +477,24 @@
val (cls', pairs') = all_class_pairs thy tycons new_cls
in (cls' @ cls, union (op =) pairs' pairs) end
-fun tcon_clause _ _ (_, []) = []
- | tcon_clause seen n (tcons, (ar as (cl, _)) :: ars) =
+fun tcon_clause _ _ [] = []
+ | tcon_clause seen n ((_, []) :: rest) = tcon_clause seen n rest
+ | tcon_clause seen n ((tcons, (ar as (cl, _)) :: ars) :: rest) =
if cl = class_of_types then
- tcon_clause seen n (tcons, ars)
+ tcon_clause seen n ((tcons, ars) :: rest)
else if member (op =) seen cl then
(* multiple clauses for the same (tycon, cl) pair *)
make_axiom_tcon_clause (tcons,
lookup_const tcons ^ "___" ^ ascii_of cl ^ "_" ^ string_of_int n,
ar) ::
- tcon_clause seen (n + 1) (tcons, ars)
+ tcon_clause seen (n + 1) ((tcons, ars) :: rest)
else
make_axiom_tcon_clause (tcons, lookup_const tcons ^ "___" ^ ascii_of cl,
ar) ::
- tcon_clause (cl :: seen) n (tcons, ars)
+ tcon_clause (cl :: seen) n ((tcons, ars) :: rest)
fun make_tcon_clauses thy tycons =
- all_class_pairs thy tycons ##> maps (tcon_clause [] 1)
+ all_class_pairs thy tycons ##> tcon_clause [] 1
(** Isabelle class relations **)
--- a/src/HOL/Topological_Spaces.thy Tue Apr 09 21:22:15 2013 +0200
+++ b/src/HOL/Topological_Spaces.thy Tue Apr 09 21:39:55 2013 +0200
@@ -658,40 +658,58 @@
subsubsection {* Standard filters *}
-definition within :: "'a filter \<Rightarrow> 'a set \<Rightarrow> 'a filter" (infixr "within" 70)
- where "F within S = Abs_filter (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) F)"
+definition principal :: "'a set \<Rightarrow> 'a filter" where
+ "principal S = Abs_filter (\<lambda>P. \<forall>x\<in>S. P x)"
+
+lemma eventually_principal: "eventually P (principal S) \<longleftrightarrow> (\<forall>x\<in>S. P x)"
+ unfolding principal_def
+ by (rule eventually_Abs_filter, rule is_filter.intro) auto
-lemma eventually_within:
- "eventually P (F within S) = eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) F"
- unfolding within_def
- by (rule eventually_Abs_filter, rule is_filter.intro)
- (auto elim!: eventually_rev_mp)
+lemma eventually_inf_principal: "eventually P (inf F (principal s)) \<longleftrightarrow> eventually (\<lambda>x. x \<in> s \<longrightarrow> P x) F"
+ unfolding eventually_inf eventually_principal by (auto elim: eventually_elim1)
+
+lemma principal_UNIV[simp]: "principal UNIV = top"
+ by (auto simp: filter_eq_iff eventually_principal)
-lemma within_UNIV [simp]: "F within UNIV = F"
- unfolding filter_eq_iff eventually_within by simp
+lemma principal_empty[simp]: "principal {} = bot"
+ by (auto simp: filter_eq_iff eventually_principal)
+
+lemma principal_le_iff[iff]: "principal A \<le> principal B \<longleftrightarrow> A \<subseteq> B"
+ by (auto simp: le_filter_def eventually_principal)
-lemma within_empty [simp]: "F within {} = bot"
- unfolding filter_eq_iff eventually_within by simp
+lemma le_principal: "F \<le> principal A \<longleftrightarrow> eventually (\<lambda>x. x \<in> A) F"
+ unfolding le_filter_def eventually_principal
+ apply safe
+ apply (erule_tac x="\<lambda>x. x \<in> A" in allE)
+ apply (auto elim: eventually_elim1)
+ done
-lemma within_within_eq: "(F within S) within T = F within (S \<inter> T)"
- by (auto simp: filter_eq_iff eventually_within elim: eventually_elim1)
+lemma principal_inject[iff]: "principal A = principal B \<longleftrightarrow> A = B"
+ unfolding eq_iff by simp
-lemma within_le: "F within S \<le> F"
- unfolding le_filter_def eventually_within by (auto elim: eventually_elim1)
+lemma sup_principal[simp]: "sup (principal A) (principal B) = principal (A \<union> B)"
+ unfolding filter_eq_iff eventually_sup eventually_principal by auto
-lemma le_withinI: "F \<le> F' \<Longrightarrow> eventually (\<lambda>x. x \<in> S) F \<Longrightarrow> F \<le> F' within S"
- unfolding le_filter_def eventually_within by (auto elim: eventually_elim2)
+lemma inf_principal[simp]: "inf (principal A) (principal B) = principal (A \<inter> B)"
+ unfolding filter_eq_iff eventually_inf eventually_principal
+ by (auto intro: exI[of _ "\<lambda>x. x \<in> A"] exI[of _ "\<lambda>x. x \<in> B"])
-lemma le_within_iff: "eventually (\<lambda>x. x \<in> S) F \<Longrightarrow> F \<le> F' within S \<longleftrightarrow> F \<le> F'"
- by (blast intro: within_le le_withinI order_trans)
+lemma SUP_principal[simp]: "(SUP i : I. principal (A i)) = principal (\<Union>i\<in>I. A i)"
+ unfolding filter_eq_iff eventually_Sup SUP_def by (auto simp: eventually_principal)
+
+lemma filtermap_principal[simp]: "filtermap f (principal A) = principal (f ` A)"
+ unfolding filter_eq_iff eventually_filtermap eventually_principal by simp
subsubsection {* Topological filters *}
definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter"
where "nhds a = Abs_filter (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
-definition (in topological_space) at :: "'a \<Rightarrow> 'a filter"
- where "at a = nhds a within - {a}"
+definition (in topological_space) at_within :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a filter" ("at (_) within (_)" [1000, 60] 60)
+ where "at a within s = inf (nhds a) (principal (s - {a}))"
+
+abbreviation (in topological_space) at :: "'a \<Rightarrow> 'a filter" ("at") where
+ "at x \<equiv> at x within (CONST UNIV)"
abbreviation (in order_topology) at_right :: "'a \<Rightarrow> 'a filter" where
"at_right x \<equiv> at x within {x <..}"
@@ -720,12 +738,19 @@
lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
unfolding trivial_limit_def eventually_nhds by simp
+lemma eventually_at_filter:
+ "eventually P (at a within s) \<longleftrightarrow> eventually (\<lambda>x. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x) (nhds a)"
+ unfolding at_within_def eventually_inf_principal by (simp add: imp_conjL[symmetric] conj_commute)
+
+lemma at_le: "s \<subseteq> t \<Longrightarrow> at x within s \<le> at x within t"
+ unfolding at_within_def by (intro inf_mono) auto
+
lemma eventually_at_topological:
- "eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
-unfolding at_def eventually_within eventually_nhds by simp
+ "eventually P (at a within s) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x))"
+ unfolding eventually_nhds eventually_at_filter by simp
lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
- unfolding filter_eq_iff eventually_within eventually_at_topological by (metis open_Int Int_iff)
+ unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I)
lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
unfolding trivial_limit_def eventually_at_topological
@@ -737,33 +762,33 @@
lemma eventually_at_right:
fixes x :: "'a :: {no_top, linorder_topology}"
shows "eventually P (at_right x) \<longleftrightarrow> (\<exists>b. x < b \<and> (\<forall>z. x < z \<and> z < b \<longrightarrow> P z))"
- unfolding eventually_nhds eventually_within at_def
+ unfolding eventually_at_topological
proof safe
from gt_ex[of x] guess y ..
moreover fix S assume "open S" "x \<in> S" note open_right[OF this, of y]
moreover note gt_ex[of x]
- moreover assume "\<forall>s\<in>S. s \<in> - {x} \<longrightarrow> s \<in> {x<..} \<longrightarrow> P s"
+ moreover assume "\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {x<..} \<longrightarrow> P s"
ultimately show "\<exists>b>x. \<forall>z. x < z \<and> z < b \<longrightarrow> P z"
by (auto simp: subset_eq Ball_def)
next
fix b assume "x < b" "\<forall>z. x < z \<and> z < b \<longrightarrow> P z"
- then show "\<exists>S. open S \<and> x \<in> S \<and> (\<forall>xa\<in>S. xa \<in> - {x} \<longrightarrow> xa \<in> {x<..} \<longrightarrow> P xa)"
+ then show "\<exists>S. open S \<and> x \<in> S \<and> (\<forall>xa\<in>S. xa \<noteq> x \<longrightarrow> xa \<in> {x<..} \<longrightarrow> P xa)"
by (intro exI[of _ "{..< b}"]) auto
qed
lemma eventually_at_left:
fixes x :: "'a :: {no_bot, linorder_topology}"
shows "eventually P (at_left x) \<longleftrightarrow> (\<exists>b. x > b \<and> (\<forall>z. b < z \<and> z < x \<longrightarrow> P z))"
- unfolding eventually_nhds eventually_within at_def
+ unfolding eventually_at_topological
proof safe
from lt_ex[of x] guess y ..
moreover fix S assume "open S" "x \<in> S" note open_left[OF this, of y]
- moreover assume "\<forall>s\<in>S. s \<in> - {x} \<longrightarrow> s \<in> {..<x} \<longrightarrow> P s"
+ moreover assume "\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {..<x} \<longrightarrow> P s"
ultimately show "\<exists>b<x. \<forall>z. b < z \<and> z < x \<longrightarrow> P z"
by (auto simp: subset_eq Ball_def)
next
fix b assume "b < x" "\<forall>z. b < z \<and> z < x \<longrightarrow> P z"
- then show "\<exists>S. open S \<and> x \<in> S \<and> (\<forall>xa\<in>S. xa \<in> - {x} \<longrightarrow> xa \<in> {..<x} \<longrightarrow> P xa)"
+ then show "\<exists>S. open S \<and> x \<in> S \<and> (\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {..<x} \<longrightarrow> P s)"
by (intro exI[of _ "{b <..}"]) auto
qed
@@ -775,11 +800,8 @@
"\<not> trivial_limit (at_right (x::'a::{no_top, dense_linorder, linorder_topology}))"
unfolding trivial_limit_def eventually_at_right by (auto dest: dense)
-lemma at_within_eq: "at x within T = nhds x within (T - {x})"
- unfolding at_def within_within_eq by (simp add: ac_simps Diff_eq)
-
lemma at_eq_sup_left_right: "at (x::'a::linorder_topology) = sup (at_left x) (at_right x)"
- by (auto simp: eventually_within at_def filter_eq_iff eventually_sup
+ by (auto simp: eventually_at_filter filter_eq_iff eventually_sup
elim: eventually_elim2 eventually_elim1)
lemma eventually_at_split:
@@ -816,13 +838,13 @@
"F1 = F1' \<Longrightarrow> F2 = F2' \<Longrightarrow> eventually (\<lambda>x. f x = g x) F2 \<Longrightarrow> filterlim f F1 F2 = filterlim g F1' F2'"
by (auto simp: filterlim_def le_filter_def eventually_filtermap elim: eventually_elim2)
-lemma filterlim_within:
- "(LIM x F1. f x :> F2 within S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F1 \<and> (LIM x F1. f x :> F2))"
- unfolding filterlim_def
-proof safe
- assume "filtermap f F1 \<le> F2 within S" then show "eventually (\<lambda>x. f x \<in> S) F1"
- by (auto simp: le_filter_def eventually_filtermap eventually_within elim!: allE[of _ "\<lambda>x. x \<in> S"])
-qed (auto intro: within_le order_trans simp: le_within_iff eventually_filtermap)
+lemma filterlim_principal:
+ "(LIM x F. f x :> principal S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F)"
+ unfolding filterlim_def eventually_filtermap le_principal ..
+
+lemma filterlim_inf:
+ "(LIM x F1. f x :> inf F2 F3) \<longleftrightarrow> ((LIM x F1. f x :> F2) \<and> (LIM x F1. f x :> F3))"
+ unfolding filterlim_def by simp
lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2"
unfolding filterlim_def filtermap_filtermap ..
@@ -859,7 +881,7 @@
setup {*
Tendsto_Intros.setup #>
Global_Theory.add_thms_dynamic (@{binding tendsto_eq_intros},
- map (fn thm => @{thm tendsto_eq_rhs} OF [thm]) o Tendsto_Intros.get o Context.proof_of);
+ map_filter (try (fn thm => @{thm tendsto_eq_rhs} OF [thm])) o Tendsto_Intros.get o Context.proof_of);
*}
lemma (in topological_space) tendsto_def:
@@ -872,19 +894,18 @@
by (auto elim!: allE[of _ "\<lambda>x. x \<in> S"] eventually_rev_mp)
qed (auto elim!: eventually_rev_mp simp: eventually_nhds eventually_filtermap le_filter_def)
-lemma tendsto_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
- by (auto simp: tendsto_def eventually_within elim!: eventually_elim1)
-
-lemma filterlim_at:
- "(LIM x F. f x :> at b) \<longleftrightarrow> (eventually (\<lambda>x. f x \<noteq> b) F \<and> (f ---> b) F)"
- by (simp add: at_def filterlim_within)
-
lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f ---> l) F' \<Longrightarrow> (f ---> l) F"
unfolding tendsto_def le_filter_def by fast
+lemma tendsto_within_subset: "(f ---> l) (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (at x within T)"
+ by (blast intro: tendsto_mono at_le)
+
+lemma filterlim_at:
+ "(LIM x F. f x :> at b within s) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> s \<and> f x \<noteq> b) F \<and> (f ---> b) F)"
+ by (simp add: at_within_def filterlim_inf filterlim_principal conj_commute)
+
lemma (in topological_space) topological_tendstoI:
- "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F)
- \<Longrightarrow> (f ---> l) F"
+ "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F) \<Longrightarrow> (f ---> l) F"
unfolding tendsto_def by auto
lemma (in topological_space) topological_tendstoD:
@@ -923,13 +944,9 @@
lemma tendsto_bot [simp]: "(f ---> a) bot"
unfolding tendsto_def by simp
-lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a)"
+lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a within s)"
unfolding tendsto_def eventually_at_topological by auto
-lemma tendsto_ident_at_within [tendsto_intros]:
- "((\<lambda>x. x) ---> a) (at a within S)"
- unfolding tendsto_def eventually_within eventually_at_topological by auto
-
lemma (in topological_space) tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) F"
by (simp add: tendsto_def)
@@ -1018,12 +1035,9 @@
"\<not>(trivial_limit net) \<Longrightarrow> (f ---> l) net \<Longrightarrow> Lim net f = l"
unfolding Lim_def using tendsto_unique[of net f] by auto
-lemma Lim_ident_at: "\<not> trivial_limit (at x) \<Longrightarrow> Lim (at x) (\<lambda>x. x) = x"
+lemma Lim_ident_at: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto
-lemma Lim_ident_at_within: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
- by (rule tendsto_Lim[OF _ tendsto_ident_at_within]) auto
-
subsection {* Limits to @{const at_top} and @{const at_bot} *}
lemma filterlim_at_top:
@@ -1508,12 +1522,12 @@
lemma (in first_countable_topology) sequentially_imp_eventually_nhds_within:
assumes "\<forall>f. (\<forall>n. f n \<in> s) \<and> f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially"
- shows "eventually P (nhds a within s)"
+ shows "eventually P (inf (nhds a) (principal s))"
proof (rule ccontr)
from countable_basis[of a] guess A . note A = this
- assume "\<not> eventually P (nhds a within s)"
+ assume "\<not> eventually P (inf (nhds a) (principal s))"
with A have P: "\<exists>F. \<forall>n. F n \<in> s \<and> F n \<in> A n \<and> \<not> P (F n)"
- unfolding eventually_within eventually_nhds by (intro choice) fastforce
+ unfolding eventually_inf_principal eventually_nhds by (intro choice) fastforce
then guess F ..
hence F0: "\<forall>n. F n \<in> s" and F2: "\<forall>n. F n \<in> A n" and F3: "\<forall>n. \<not> P (F n)"
by fast+
@@ -1524,12 +1538,12 @@
qed
lemma (in first_countable_topology) eventually_nhds_within_iff_sequentially:
- "eventually P (nhds a within s) \<longleftrightarrow>
+ "eventually P (inf (nhds a) (principal s)) \<longleftrightarrow>
(\<forall>f. (\<forall>n. f n \<in> s) \<and> f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially)"
proof (safe intro!: sequentially_imp_eventually_nhds_within)
- assume "eventually P (nhds a within s)"
+ assume "eventually P (inf (nhds a) (principal s))"
then obtain S where "open S" "a \<in> S" "\<forall>x\<in>S. x \<in> s \<longrightarrow> P x"
- by (auto simp: eventually_within eventually_nhds)
+ by (auto simp: eventually_inf_principal eventually_nhds)
moreover fix f assume "\<forall>n. f n \<in> s" "f ----> a"
ultimately show "eventually (\<lambda>n. P (f n)) sequentially"
by (auto dest!: topological_tendstoD elim: eventually_elim1)
@@ -1547,7 +1561,7 @@
"f -- a --> L \<equiv> (f ---> L) (at a)"
lemma tendsto_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f ---> l) (at a within S) \<longleftrightarrow> (f -- a --> l)"
- unfolding tendsto_def by (simp add: at_within_open)
+ unfolding tendsto_def by (simp add: at_within_open[where S=S])
lemma LIM_const_not_eq[tendsto_intros]:
fixes a :: "'a::perfect_space"
@@ -1581,7 +1595,7 @@
lemma tendsto_at_iff_tendsto_nhds:
"g -- l --> g l \<longleftrightarrow> (g ---> g l) (nhds l)"
- unfolding tendsto_def at_def eventually_within
+ unfolding tendsto_def eventually_at_filter
by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1)
lemma tendsto_compose:
@@ -1607,7 +1621,7 @@
lemma (in first_countable_topology) sequentially_imp_eventually_within:
"(\<forall>f. (\<forall>n. f n \<in> s \<and> f n \<noteq> a) \<and> f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially) \<Longrightarrow>
eventually P (at a within s)"
- unfolding at_def within_within_eq
+ unfolding at_within_def
by (intro sequentially_imp_eventually_nhds_within) auto
lemma (in first_countable_topology) sequentially_imp_eventually_at:
@@ -1640,12 +1654,12 @@
lemma continuous_on_cong [cong]:
"s = t \<Longrightarrow> (\<And>x. x \<in> t \<Longrightarrow> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g"
- unfolding continuous_on_def by (intro ball_cong filterlim_cong) (auto simp: eventually_within)
+ unfolding continuous_on_def by (intro ball_cong filterlim_cong) (auto simp: eventually_at_filter)
lemma continuous_on_topological:
"continuous_on s f \<longleftrightarrow>
(\<forall>x\<in>s. \<forall>B. open B \<longrightarrow> f x \<in> B \<longrightarrow> (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)))"
- unfolding continuous_on_def tendsto_def eventually_within eventually_at_topological by metis
+ unfolding continuous_on_def tendsto_def eventually_at_topological by metis
lemma continuous_on_open_invariant:
"continuous_on s f \<longleftrightarrow> (\<forall>B. open B \<longrightarrow> (\<exists>A. open A \<and> A \<inter> s = f -` B \<inter> s))"
@@ -1689,7 +1703,7 @@
lemma continuous_on_open_Union:
"(\<And>s. s \<in> S \<Longrightarrow> open s) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on s f) \<Longrightarrow> continuous_on (\<Union>S) f"
- unfolding continuous_on_def by (simp add: tendsto_within_open open_Union)
+ unfolding continuous_on_def by safe (metis open_Union at_within_open UnionI)
lemma continuous_on_open_UN:
"(\<And>s. s \<in> S \<Longrightarrow> open (A s)) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on (A s) f) \<Longrightarrow> continuous_on (\<Union>s\<in>S. A s) f"
@@ -1725,7 +1739,7 @@
setup Continuous_On_Intros.setup
lemma continuous_on_id[continuous_on_intros]: "continuous_on s (\<lambda>x. x)"
- unfolding continuous_on_def by (fast intro: tendsto_ident_at_within)
+ unfolding continuous_on_def by (fast intro: tendsto_ident_at)
lemma continuous_on_const[continuous_on_intros]: "continuous_on s (\<lambda>x. c)"
unfolding continuous_on_def by (auto intro: tendsto_const)
@@ -1762,12 +1776,12 @@
by simp
lemma continuous_within: "continuous (at x within s) f \<longleftrightarrow> (f ---> f x) (at x within s)"
- by (cases "trivial_limit (at x within s)") (auto simp add: Lim_ident_at_within continuous_def)
+ by (cases "trivial_limit (at x within s)") (auto simp add: Lim_ident_at continuous_def)
lemma continuous_within_topological:
"continuous (at x within s) f \<longleftrightarrow>
(\<forall>B. open B \<longrightarrow> f x \<in> B \<longrightarrow> (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)))"
- unfolding continuous_within tendsto_def eventually_within eventually_at_topological by metis
+ unfolding continuous_within tendsto_def eventually_at_topological by metis
lemma continuous_within_compose[continuous_intros]:
"continuous (at x within s) f \<Longrightarrow> continuous (at (f x) within f ` s) g \<Longrightarrow>
@@ -1783,7 +1797,7 @@
using continuous_within[of x UNIV f] by simp
lemma continuous_ident[continuous_intros, simp]: "continuous (at x within S) (\<lambda>x. x)"
- unfolding continuous_within by (rule tendsto_ident_at_within)
+ unfolding continuous_within by (rule tendsto_ident_at)
lemma continuous_const[continuous_intros, simp]: "continuous F (\<lambda>x. c)"
unfolding continuous_def by (rule tendsto_const)
@@ -1799,10 +1813,10 @@
by (rule continuous_at)
lemma continuous_at_within: "isCont f x \<Longrightarrow> continuous (at x within s) f"
- by (auto intro: within_le filterlim_mono simp: continuous_at continuous_within)
+ by (auto intro: tendsto_mono at_le simp: continuous_at continuous_within)
lemma continuous_on_eq_continuous_at: "open s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. isCont f x)"
- by (simp add: continuous_on_def continuous_at tendsto_within_open)
+ by (simp add: continuous_on_def continuous_at at_within_open[of _ s])
lemma continuous_on_subset: "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> continuous_on t f"
unfolding continuous_on_def by (metis subset_eq tendsto_within_subset)
--- a/src/HOL/Transcendental.thy Tue Apr 09 21:22:15 2013 +0200
+++ b/src/HOL/Transcendental.thy Tue Apr 09 21:39:55 2013 +0200
@@ -1578,7 +1578,7 @@
lemma ln_at_0: "LIM x at_right 0. ln x :> at_bot"
by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
- (auto simp: eventually_within)
+ (auto simp: eventually_at_filter)
lemma ln_at_top: "LIM x at_top. ln x :> at_top"
by (rule filterlim_at_top_at_top[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
@@ -3190,12 +3190,12 @@
lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))"
by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
- (auto simp: le_less eventually_within_less dist_real_def simp del: less_divide_eq_numeral1
+ (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
intro!: tan_monotone exI[of _ "pi/2"])
lemma filterlim_tan_at_left: "filterlim tan at_top (at_left (pi/2))"
by (rule filterlim_at_top_at_left[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
- (auto simp: le_less eventually_within_less dist_real_def simp del: less_divide_eq_numeral1
+ (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
intro!: tan_monotone exI[of _ "pi/2"])
lemma tendsto_arctan_at_top: "(arctan ---> (pi/2)) at_top"