# HG changeset patch # User huffman # Date 1243614176 25200 # Node ID d41a8ba25b674ece945f773a9396c76c92f9949e # Parent a9ed5fcc5e39a32514931986a1ba2e83b9901310 generalize constants from Lim.thy to class metric_space diff -r a9ed5fcc5e39 -r d41a8ba25b67 src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Thu May 28 23:03:12 2009 -0700 +++ b/src/HOL/Deriv.thy Fri May 29 09:22:56 2009 -0700 @@ -76,7 +76,7 @@ hence "(\h. f(x+h) - f(x)) -- 0 --> 0" by (simp cong: LIM_cong) thus "(\h. f(x+h)) -- 0 --> f(x)" - by (simp add: LIM_def) + by (simp add: LIM_def dist_norm) qed lemma DERIV_mult_lemma: @@ -125,6 +125,7 @@ text{*Alternative definition for differentiability*} lemma DERIV_LIM_iff: + fixes f :: "'a::{real_normed_vector,inverse} \ 'a" shows "((%h. (f(a + h) - f(a)) / h) -- 0 --> D) = ((%x. (f(x)-f(a)) / (x-a)) -- a --> D)" apply (rule iffI) @@ -614,7 +615,7 @@ apply (cut_tac P = "% (u,v) . a \ u & u \ v & v \ b --> ~ (f (u) \ y & y \ f (v))" in lemma_BOLZANO2) apply safe apply simp_all -apply (simp add: isCont_iff LIM_def) +apply (simp add: isCont_iff LIM_eq) apply (rule ccontr) apply (subgoal_tac "a \ x & x \ b") prefer 2 @@ -675,7 +676,7 @@ apply (case_tac "a \ x & x \ b") apply (rule_tac [2] x = 1 in exI) prefer 2 apply force -apply (simp add: LIM_def isCont_iff) +apply (simp add: LIM_eq isCont_iff) apply (drule_tac x = x in spec, auto) apply (erule_tac V = "\M. \x. a \ x & x \ b & ~ f x \ M" in thin_rl) apply (drule_tac x = 1 in spec, auto) @@ -1486,7 +1487,7 @@ lemma LIM_fun_gt_zero: "[| f -- c --> (l::real); 0 < l |] ==> \r. 0 < r & (\x::real. x \ c & \c - x\ < r --> 0 < f x)" -apply (auto simp add: LIM_def) +apply (auto simp add: LIM_eq) apply (drule_tac x = "l/2" in spec, safe, force) apply (rule_tac x = s in exI) apply (auto simp only: abs_less_iff) @@ -1495,7 +1496,7 @@ lemma LIM_fun_less_zero: "[| f -- c --> (l::real); l < 0 |] ==> \r. 0 < r & (\x::real. x \ c & \c - x\ < r --> f x < 0)" -apply (auto simp add: LIM_def) +apply (auto simp add: LIM_eq) apply (drule_tac x = "-l/2" in spec, safe, force) apply (rule_tac x = s in exI) apply (auto simp only: abs_less_iff) diff -r a9ed5fcc5e39 -r d41a8ba25b67 src/HOL/Integration.thy --- a/src/HOL/Integration.thy Thu May 28 23:03:12 2009 -0700 +++ b/src/HOL/Integration.thy Fri May 29 09:22:56 2009 -0700 @@ -272,7 +272,7 @@ fix x :: real assume "a \ x" and "x \ b" with f' have "DERIV f x :> f'(x)" by simp then have "\r>0. \s>0. \z. z \ x \ \z - x\ < s \ \(f z - f x) / (z - x) - f' x\ < r" - by (simp add: DERIV_iff2 LIM_def) + by (simp add: DERIV_iff2 LIM_eq) with `0 < e` obtain s where "\z. z \ x \ \z - x\ < s \ \(f z - f x) / (z - x) - f' x\ < e/2" and "0 < s" by (drule_tac x="e/2" in spec, auto) diff -r a9ed5fcc5e39 -r d41a8ba25b67 src/HOL/Lim.thy --- a/src/HOL/Lim.thy Thu May 28 23:03:12 2009 -0700 +++ b/src/HOL/Lim.thy Fri May 29 09:22:56 2009 -0700 @@ -13,90 +13,110 @@ text{*Standard Definitions*} definition - LIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool" + LIM :: "['a::metric_space \ 'b::metric_space, 'a, 'b] \ bool" ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where [code del]: "f -- a --> L = - (\r > 0. \s > 0. \x. x \ a & norm (x - a) < s - --> norm (f x - L) < r)" + (\r > 0. \s > 0. \x. x \ a & dist x a < s + --> dist (f x) L < r)" definition - isCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where + isCont :: "['a::metric_space \ 'b::metric_space, 'a] \ bool" where "isCont f a = (f -- a --> (f a))" definition - isUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where - [code del]: "isUCont f = (\r>0. \s>0. \x y. norm (x - y) < s \ norm (f x - f y) < r)" + isUCont :: "['a::metric_space \ 'b::metric_space] \ bool" where + [code del]: "isUCont f = (\r>0. \s>0. \x y. dist x y < s \ dist (f x) (f y) < r)" subsection {* Limits of Functions *} -subsubsection {* Purely standard proofs *} +lemma metric_LIM_I: + "(\r. 0 < r \ \s>0. \x. x \ a \ dist x a < s \ dist (f x) L < r) + \ f -- a --> L" +by (simp add: LIM_def) + +lemma metric_LIM_D: + "\f -- a --> L; 0 < r\ + \ \s>0. \x. x \ a \ dist x a < s \ dist (f x) L < r" +by (simp add: LIM_def) lemma LIM_eq: - "f -- a --> L = + fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector" + shows "f -- a --> L = (\r>0.\s>0.\x. x \ a & norm (x-a) < s --> norm (f x - L) < r)" -by (simp add: LIM_def diff_minus) +by (simp add: LIM_def dist_norm) lemma LIM_I: - "(!!r. 0 \s>0.\x. x \ a & norm (x-a) < s --> norm (f x - L) < r) + fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector" + shows "(!!r. 0 \s>0.\x. x \ a & norm (x-a) < s --> norm (f x - L) < r) ==> f -- a --> L" by (simp add: LIM_eq) lemma LIM_D: - "[| f -- a --> L; 0 L; 0 \s>0.\x. x \ a & norm (x-a) < s --> norm (f x - L) < r" by (simp add: LIM_eq) -lemma LIM_offset: "f -- a --> L \ (\x. f (x + k)) -- a - k --> L" -apply (rule LIM_I) -apply (drule_tac r="r" in LIM_D, safe) +lemma LIM_offset: + fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space" + shows "f -- a --> L \ (\x. f (x + k)) -- a - k --> L" +unfolding LIM_def dist_norm +apply clarify +apply (drule_tac x="r" in spec, safe) apply (rule_tac x="s" in exI, safe) apply (drule_tac x="x + k" in spec) apply (simp add: algebra_simps) done -lemma LIM_offset_zero: "f -- a --> L \ (\h. f (a + h)) -- 0 --> L" +lemma LIM_offset_zero: + fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space" + shows "f -- a --> L \ (\h. f (a + h)) -- 0 --> L" by (drule_tac k="a" in LIM_offset, simp add: add_commute) -lemma LIM_offset_zero_cancel: "(\h. f (a + h)) -- 0 --> L \ f -- a --> L" +lemma LIM_offset_zero_cancel: + fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space" + shows "(\h. f (a + h)) -- 0 --> L \ f -- a --> L" by (drule_tac k="- a" in LIM_offset, simp) lemma LIM_const [simp]: "(%x. k) -- x --> k" by (simp add: LIM_def) lemma LIM_add: - fixes f g :: "'a::real_normed_vector \ 'b::real_normed_vector" + fixes f g :: "'a::metric_space \ 'b::real_normed_vector" assumes f: "f -- a --> L" and g: "g -- a --> M" - shows "(%x. f x + g(x)) -- a --> (L + M)" -proof (rule LIM_I) + shows "(\x. f x + g x) -- a --> (L + M)" +proof (rule metric_LIM_I) fix r :: real assume r: "0 < r" - from LIM_D [OF f half_gt_zero [OF r]] + from metric_LIM_D [OF f half_gt_zero [OF r]] obtain fs where fs: "0 < fs" - and fs_lt: "\x. x \ a & norm (x-a) < fs --> norm (f x - L) < r/2" + and fs_lt: "\x. x \ a \ dist x a < fs \ dist (f x) L < r/2" by blast - from LIM_D [OF g half_gt_zero [OF r]] + from metric_LIM_D [OF g half_gt_zero [OF r]] obtain gs where gs: "0 < gs" - and gs_lt: "\x. x \ a & norm (x-a) < gs --> norm (g x - M) < r/2" + and gs_lt: "\x. x \ a \ dist x a < gs \ dist (g x) M < r/2" by blast - show "\s>0.\x. x \ a \ norm (x-a) < s \ norm (f x + g x - (L + M)) < r" + show "\s>0. \x. x \ a \ dist x a < s \ dist (f x + g x) (L + M) < r" proof (intro exI conjI strip) show "0 < min fs gs" by (simp add: fs gs) fix x :: 'a - assume "x \ a \ norm (x-a) < min fs gs" - hence "x \ a \ norm (x-a) < fs \ norm (x-a) < gs" by simp + assume "x \ a \ dist x a < min fs gs" + hence "x \ a \ dist x a < fs \ dist x a < gs" by simp with fs_lt gs_lt - have "norm (f x - L) < r/2" and "norm (g x - M) < r/2" by blast+ - hence "norm (f x - L) + norm (g x - M) < r" by arith - thus "norm (f x + g x - (L + M)) < r" + have "dist (f x) L < r/2" and "dist (g x) M < r/2" by blast+ + hence "dist (f x) L + dist (g x) M < r" by arith + thus "dist (f x + g x) (L + M) < r" + unfolding dist_norm by (blast intro: norm_diff_triangle_ineq order_le_less_trans) qed qed lemma LIM_add_zero: - "\f -- a --> 0; g -- a --> 0\ \ (\x. f x + g x) -- a --> 0" + fixes f g :: "'a::metric_space \ 'b::real_normed_vector" + shows "\f -- a --> 0; g -- a --> 0\ \ (\x. f x + g x) -- a --> 0" by (drule (1) LIM_add, simp) lemma minus_diff_minus: @@ -104,46 +124,75 @@ shows "(- a) - (- b) = - (a - b)" by simp -lemma LIM_minus: "f -- a --> L ==> (%x. -f(x)) -- a --> -L" -by (simp only: LIM_eq minus_diff_minus norm_minus_cancel) +lemma LIM_minus: + fixes f :: "'a::metric_space \ 'b::real_normed_vector" + shows "f -- a --> L \ (\x. - f x) -- a --> - L" +by (simp only: LIM_def dist_norm minus_diff_minus norm_minus_cancel) +(* TODO: delete *) lemma LIM_add_minus: - "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)" + fixes f g :: "'a::metric_space \ 'b::real_normed_vector" + shows "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)" by (intro LIM_add LIM_minus) lemma LIM_diff: - "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) - g(x)) -- x --> l-m" + fixes f g :: "'a::metric_space \ 'b::real_normed_vector" + shows "\f -- x --> l; g -- x --> m\ \ (\x. f x - g x) -- x --> l - m" by (simp only: diff_minus LIM_add LIM_minus) -lemma LIM_zero: "f -- a --> l \ (\x. f x - l) -- a --> 0" -by (simp add: LIM_def) +lemma LIM_zero: + fixes f :: "'a::metric_space \ 'b::real_normed_vector" + shows "f -- a --> l \ (\x. f x - l) -- a --> 0" +by (simp add: LIM_def dist_norm) -lemma LIM_zero_cancel: "(\x. f x - l) -- a --> 0 \ f -- a --> l" -by (simp add: LIM_def) +lemma LIM_zero_cancel: + fixes f :: "'a::metric_space \ 'b::real_normed_vector" + shows "(\x. f x - l) -- a --> 0 \ f -- a --> l" +by (simp add: LIM_def dist_norm) -lemma LIM_zero_iff: "(\x. f x - l) -- a --> 0 = f -- a --> l" -by (simp add: LIM_def) +lemma LIM_zero_iff: + fixes f :: "'a::metric_space \ 'b::real_normed_vector" + shows "(\x. f x - l) -- a --> 0 = f -- a --> l" +by (simp add: LIM_def dist_norm) -lemma LIM_imp_LIM: +lemma metric_LIM_imp_LIM: assumes f: "f -- a --> l" - assumes le: "\x. x \ a \ norm (g x - m) \ norm (f x - l)" + assumes le: "\x. x \ a \ dist (g x) m \ dist (f x) l" shows "g -- a --> m" -apply (rule LIM_I, drule LIM_D [OF f], safe) +apply (rule metric_LIM_I, drule metric_LIM_D [OF f], safe) apply (rule_tac x="s" in exI, safe) apply (drule_tac x="x" in spec, safe) apply (erule (1) order_le_less_trans [OF le]) done -lemma LIM_norm: "f -- a --> l \ (\x. norm (f x)) -- a --> norm l" +lemma LIM_imp_LIM: + fixes f :: "'a::metric_space \ 'b::real_normed_vector" + fixes g :: "'a::metric_space \ 'c::real_normed_vector" + assumes f: "f -- a --> l" + assumes le: "\x. x \ a \ norm (g x - m) \ norm (f x - l)" + shows "g -- a --> m" +apply (rule metric_LIM_imp_LIM [OF f]) +apply (simp add: dist_norm le) +done + +lemma LIM_norm: + fixes f :: "'a::metric_space \ 'b::real_normed_vector" + shows "f -- a --> l \ (\x. norm (f x)) -- a --> norm l" by (erule LIM_imp_LIM, simp add: norm_triangle_ineq3) -lemma LIM_norm_zero: "f -- a --> 0 \ (\x. norm (f x)) -- a --> 0" +lemma LIM_norm_zero: + fixes f :: "'a::metric_space \ 'b::real_normed_vector" + shows "f -- a --> 0 \ (\x. norm (f x)) -- a --> 0" by (drule LIM_norm, simp) -lemma LIM_norm_zero_cancel: "(\x. norm (f x)) -- a --> 0 \ f -- a --> 0" +lemma LIM_norm_zero_cancel: + fixes f :: "'a::metric_space \ 'b::real_normed_vector" + shows "(\x. norm (f x)) -- a --> 0 \ f -- a --> 0" by (erule LIM_imp_LIM, simp) -lemma LIM_norm_zero_iff: "(\x. norm (f x)) -- a --> 0 = f -- a --> 0" +lemma LIM_norm_zero_iff: + fixes f :: "'a::metric_space \ 'b::real_normed_vector" + shows "(\x. norm (f x)) -- a --> 0 = f -- a --> 0" by (rule iffI [OF LIM_norm_zero_cancel LIM_norm_zero]) lemma LIM_rabs: "f -- a --> (l::real) \ (\x. \f x\) -- a --> \l\" @@ -161,9 +210,9 @@ lemma LIM_const_not_eq: fixes a :: "'a::real_normed_algebra_1" shows "k \ L \ \ (\x. k) -- a --> L" -apply (simp add: LIM_eq) -apply (rule_tac x="norm (k - L)" in exI, simp, safe) -apply (rule_tac x="a + of_real (s/2)" in exI, simp add: norm_of_real) +apply (simp add: LIM_def) +apply (rule_tac x="dist k L" in exI, simp add: zero_less_dist_iff, safe) +apply (rule_tac x="a + of_real (s/2)" in exI, simp add: dist_norm) done lemmas LIM_not_zero = LIM_const_not_eq [where L = 0] @@ -176,10 +225,21 @@ done lemma LIM_unique: - fixes a :: "'a::real_normed_algebra_1" + fixes a :: "'a::real_normed_algebra_1" -- {* TODO: find a more appropriate class *} shows "\f -- a --> L; f -- a --> M\ \ L = M" -apply (drule (1) LIM_diff) -apply (auto dest!: LIM_const_eq) +apply (rule ccontr) +apply (drule_tac r="dist L M / 2" in metric_LIM_D, simp add: zero_less_dist_iff) +apply (drule_tac r="dist L M / 2" in metric_LIM_D, simp add: zero_less_dist_iff) +apply (clarify, rename_tac r s) +apply (subgoal_tac "min r s \ 0") +apply (subgoal_tac "dist L M < dist L M / 2 + dist L M / 2", simp) +apply (subgoal_tac "dist L M \ dist (f (a + of_real (min r s / 2))) L + + dist (f (a + of_real (min r s / 2))) M") +apply (erule le_less_trans, rule add_strict_mono) +apply (drule spec, erule mp, simp add: dist_norm) +apply (drule spec, erule mp, simp add: dist_norm) +apply (subst dist_commute, rule dist_triangle) +apply simp done lemma LIM_ident [simp]: "(\x. x) -- a --> a" @@ -195,9 +255,9 @@ \ ((\x. f x) -- a --> l) = ((\x. g x) -- b --> m)" by (simp add: LIM_def) -lemma LIM_equal2: +lemma metric_LIM_equal2: assumes 1: "0 < R" - assumes 2: "\x. \x \ a; norm (x - a) < R\ \ f x = g x" + assumes 2: "\x. \x \ a; dist x a < R\ \ f x = g x" shows "g -- a --> l \ f -- a --> l" apply (unfold LIM_def, safe) apply (drule_tac x="r" in spec, safe) @@ -206,9 +266,22 @@ apply (simp add: 2) done -text{*Two uses in Hyperreal/Transcendental.ML*} +lemma LIM_equal2: + fixes f g :: "'a::real_normed_vector \ 'b::metric_space" + assumes 1: "0 < R" + assumes 2: "\x. \x \ a; norm (x - a) < R\ \ f x = g x" + shows "g -- a --> l \ f -- a --> l" +apply (unfold LIM_def dist_norm, safe) +apply (drule_tac x="r" in spec, safe) +apply (rule_tac x="min s R" in exI, safe) +apply (simp add: 1) +apply (simp add: 2) +done + +text{*Two uses in Transcendental.ML*} lemma LIM_trans: - "[| (%x. f(x) + -g(x)) -- a --> 0; g -- a --> l |] ==> f -- a --> l" + fixes f g :: "'a::metric_space \ 'b::real_normed_vector" + shows "[| (%x. f(x) + -g(x)) -- a --> 0; g -- a --> l |] ==> f -- a --> l" apply (drule LIM_add, assumption) apply (auto simp add: add_assoc) done @@ -217,62 +290,70 @@ assumes g: "g -- l --> g l" assumes f: "f -- a --> l" shows "(\x. g (f x)) -- a --> g l" -proof (rule LIM_I) +proof (rule metric_LIM_I) fix r::real assume r: "0 < r" obtain s where s: "0 < s" - and less_r: "\y. \y \ l; norm (y - l) < s\ \ norm (g y - g l) < r" - using LIM_D [OF g r] by fast + and less_r: "\y. \y \ l; dist y l < s\ \ dist (g y) (g l) < r" + using metric_LIM_D [OF g r] by fast obtain t where t: "0 < t" - and less_s: "\x. \x \ a; norm (x - a) < t\ \ norm (f x - l) < s" - using LIM_D [OF f s] by fast + and less_s: "\x. \x \ a; dist x a < t\ \ dist (f x) l < s" + using metric_LIM_D [OF f s] by fast - show "\t>0. \x. x \ a \ norm (x - a) < t \ norm (g (f x) - g l) < r" + show "\t>0. \x. x \ a \ dist x a < t \ dist (g (f x)) (g l) < r" proof (rule exI, safe) show "0 < t" using t . next - fix x assume "x \ a" and "norm (x - a) < t" - hence "norm (f x - l) < s" by (rule less_s) - thus "norm (g (f x) - g l) < r" + fix x assume "x \ a" and "dist x a < t" + hence "dist (f x) l < s" by (rule less_s) + thus "dist (g (f x)) (g l) < r" using r less_r by (case_tac "f x = l", simp_all) qed qed +lemma metric_LIM_compose2: + assumes f: "f -- a --> b" + assumes g: "g -- b --> c" + assumes inj: "\d>0. \x. x \ a \ dist x a < d \ f x \ b" + shows "(\x. g (f x)) -- a --> c" +proof (rule metric_LIM_I) + fix r :: real + assume r: "0 < r" + obtain s where s: "0 < s" + and less_r: "\y. \y \ b; dist y b < s\ \ dist (g y) c < r" + using metric_LIM_D [OF g r] by fast + obtain t where t: "0 < t" + and less_s: "\x. \x \ a; dist x a < t\ \ dist (f x) b < s" + using metric_LIM_D [OF f s] by fast + obtain d where d: "0 < d" + and neq_b: "\x. \x \ a; dist x a < d\ \ f x \ b" + using inj by fast + + show "\t>0. \x. x \ a \ dist x a < t \ dist (g (f x)) c < r" + proof (safe intro!: exI) + show "0 < min d t" using d t by simp + next + fix x + assume "x \ a" and "dist x a < min d t" + hence "f x \ b" and "dist (f x) b < s" + using neq_b less_s by simp_all + thus "dist (g (f x)) c < r" + by (rule less_r) + qed +qed + lemma LIM_compose2: + fixes a :: "'a::real_normed_vector" assumes f: "f -- a --> b" assumes g: "g -- b --> c" assumes inj: "\d>0. \x. x \ a \ norm (x - a) < d \ f x \ b" shows "(\x. g (f x)) -- a --> c" -proof (rule LIM_I) - fix r :: real - assume r: "0 < r" - obtain s where s: "0 < s" - and less_r: "\y. \y \ b; norm (y - b) < s\ \ norm (g y - c) < r" - using LIM_D [OF g r] by fast - obtain t where t: "0 < t" - and less_s: "\x. \x \ a; norm (x - a) < t\ \ norm (f x - b) < s" - using LIM_D [OF f s] by fast - obtain d where d: "0 < d" - and neq_b: "\x. \x \ a; norm (x - a) < d\ \ f x \ b" - using inj by fast - - show "\t>0. \x. x \ a \ norm (x - a) < t \ norm (g (f x) - c) < r" - proof (safe intro!: exI) - show "0 < min d t" using d t by simp - next - fix x - assume "x \ a" and "norm (x - a) < min d t" - hence "f x \ b" and "norm (f x - b) < s" - using neq_b less_s by simp_all - thus "norm (g (f x) - c) < r" - by (rule less_r) - qed -qed +by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]]) lemma LIM_o: "\g -- l --> g l; f -- a --> l\ \ (g \ f) -- a --> g l" unfolding o_def by (rule LIM_compose) lemma real_LIM_sandwich_zero: - fixes f g :: "'a::real_normed_vector \ real" + fixes f g :: "'a::metric_space \ real" assumes f: "f -- a --> 0" assumes 1: "\x. x \ a \ 0 \ g x" assumes 2: "\x. x \ a \ g x \ f x" @@ -316,10 +397,11 @@ text {* Bounded Bilinear Operators *} lemma (in bounded_bilinear) LIM_prod_zero: + fixes a :: "'d::metric_space" assumes f: "f -- a --> 0" assumes g: "g -- a --> 0" shows "(\x. f x ** g x) -- a --> 0" -proof (rule LIM_I) +proof (rule metric_LIM_I, unfold dist_norm) fix r::real assume r: "0 < r" obtain K where K: "0 < K" and norm_le: "\x y. norm (x ** y) \ norm x * norm y * K" @@ -327,18 +409,18 @@ from K have K': "0 < inverse K" by (rule positive_imp_inverse_positive) obtain s where s: "0 < s" - and norm_f: "\x. \x \ a; norm (x - a) < s\ \ norm (f x) < r" - using LIM_D [OF f r] by auto + and norm_f: "\x. \x \ a; dist x a < s\ \ norm (f x) < r" + using metric_LIM_D [OF f r, unfolded dist_norm] by auto obtain t where t: "0 < t" - and norm_g: "\x. \x \ a; norm (x - a) < t\ \ norm (g x) < inverse K" - using LIM_D [OF g K'] by auto - show "\s>0. \x. x \ a \ norm (x - a) < s \ norm (f x ** g x - 0) < r" + and norm_g: "\x. \x \ a; dist x a < t\ \ norm (g x) < inverse K" + using metric_LIM_D [OF g K', unfolded dist_norm] by auto + show "\s>0. \x. x \ a \ dist x a < s \ norm (f x ** g x - 0) < r" proof (rule exI, safe) from s t show "0 < min s t" by simp next fix x assume x: "x \ a" - assume "norm (x - a) < min s t" - hence xs: "norm (x - a) < s" and xt: "norm (x - a) < t" by simp_all + assume "dist x a < min s t" + hence xs: "dist x a < s" and xt: "dist x a < t" by simp_all from x xs have 1: "norm (f x) < r" by (rule norm_f) from x xt have 2: "norm (g x) < inverse K" by (rule norm_g) have "norm (f x ** g x) \ norm (f x) * norm (g x) * K" by (rule norm_le) @@ -383,7 +465,7 @@ lemmas LIM_of_real = of_real.LIM lemma LIM_power: - fixes f :: "'a::real_normed_vector \ 'b::{power,real_normed_algebra}" + fixes f :: "'a::metric_space \ 'b::{power,real_normed_algebra}" assumes f: "f -- a --> l" shows "(\x. f x ^ n) -- a --> l ^ n" by (induct n, simp, simp add: LIM_mult f) @@ -453,19 +535,22 @@ by (rule LIM_inverse_fun [THEN LIM_compose]) lemma LIM_sgn: - "\f -- a --> l; l \ 0\ \ (\x. sgn (f x)) -- a --> sgn l" + fixes f :: "'a::metric_space \