# HG changeset patch # User huffman # Date 1273003736 25200 # Node ID 621122eeb138acb92d16761d4df33e8d1af050cf # Parent 0a5b7b818d65c375d25cc29cd0187fa67d41330d generalize types of LIMSEQ and LIM; generalize many lemmas diff -r 0a5b7b818d65 -r 621122eeb138 src/HOL/Lim.thy --- a/src/HOL/Lim.thy Tue May 04 10:42:47 2010 -0700 +++ b/src/HOL/Lim.thy Tue May 04 13:08:56 2010 -0700 @@ -13,12 +13,12 @@ text{*Standard Definitions*} abbreviation - LIM :: "['a::metric_space \ 'b::metric_space, 'a, 'b] \ bool" + LIM :: "['a::topological_space \ 'b::topological_space, 'a, 'b] \ bool" ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where "f -- a --> L \ (f ---> L) (at a)" definition - isCont :: "['a::metric_space \ 'b::metric_space, 'a] \ bool" where + isCont :: "['a::topological_space \ 'b::topological_space, 'a] \ bool" where "isCont f a = (f -- a --> (f a))" definition @@ -61,23 +61,23 @@ by (simp add: LIM_eq) lemma LIM_offset: - fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space" + fixes a :: "'a::real_normed_vector" 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 (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 lemma LIM_offset_zero: - fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space" + fixes a :: "'a::real_normed_vector" 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: - fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space" + fixes a :: "'a::real_normed_vector" shows "(\h. f (a + h)) -- 0 --> L \ f -- a --> L" by (drule_tac k="- a" in LIM_offset, simp) @@ -87,60 +87,61 @@ lemma LIM_cong_limit: "\ f -- x --> L ; K = L \ \ f -- x --> K" by simp lemma LIM_add: - fixes f g :: "'a::metric_space \ 'b::real_normed_vector" + fixes f g :: "'a::topological_space \ 'b::real_normed_vector" assumes f: "f -- a --> L" and g: "g -- a --> M" shows "(\x. f x + g x) -- a --> (L + M)" using assms by (rule tendsto_add) lemma LIM_add_zero: - fixes f g :: "'a::metric_space \ 'b::real_normed_vector" + fixes f g :: "'a::topological_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 LIM_minus: - fixes f :: "'a::metric_space \ 'b::real_normed_vector" + fixes f :: "'a::topological_space \ 'b::real_normed_vector" shows "f -- a --> L \ (\x. - f x) -- a --> - L" by (rule tendsto_minus) (* TODO: delete *) lemma LIM_add_minus: - fixes f g :: "'a::metric_space \ 'b::real_normed_vector" + fixes f g :: "'a::topological_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: - fixes f g :: "'a::metric_space \ 'b::real_normed_vector" + fixes f g :: "'a::topological_space \ 'b::real_normed_vector" shows "\f -- x --> l; g -- x --> m\ \ (\x. f x - g x) -- x --> l - m" by (rule tendsto_diff) lemma LIM_zero: - fixes f :: "'a::metric_space \ 'b::real_normed_vector" + fixes f :: "'a::topological_space \ 'b::real_normed_vector" shows "f -- a --> l \ (\x. f x - l) -- a --> 0" -by (simp add: LIM_def dist_norm) +unfolding tendsto_iff dist_norm by simp lemma LIM_zero_cancel: - fixes f :: "'a::metric_space \ 'b::real_normed_vector" + fixes f :: "'a::topological_space \ 'b::real_normed_vector" shows "(\x. f x - l) -- a --> 0 \ f -- a --> l" -by (simp add: LIM_def dist_norm) +unfolding tendsto_iff dist_norm by simp 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) +unfolding tendsto_iff dist_norm by simp lemma metric_LIM_imp_LIM: assumes f: "f -- a --> l" assumes le: "\x. x \ a \ dist (g x) m \ dist (f x) l" shows "g -- a --> m" -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 (rule tendstoI, drule tendstoD [OF f]) +apply (simp add: eventually_at_topological, safe) +apply (rule_tac x="S" in exI, safe) +apply (drule_tac x="x" in bspec, safe) apply (erule (1) order_le_less_trans [OF le]) done lemma LIM_imp_LIM: - fixes f :: "'a::metric_space \ 'b::real_normed_vector" - fixes g :: "'a::metric_space \ 'c::real_normed_vector" + fixes f :: "'a::topological_space \ 'b::real_normed_vector" + fixes g :: "'a::topological_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" @@ -149,24 +150,24 @@ done lemma LIM_norm: - fixes f :: "'a::metric_space \ 'b::real_normed_vector" + fixes f :: "'a::topological_space \ 'b::real_normed_vector" shows "f -- a --> l \ (\x. norm (f x)) -- a --> norm l" by (rule tendsto_norm) lemma LIM_norm_zero: - fixes f :: "'a::metric_space \ 'b::real_normed_vector" + fixes f :: "'a::topological_space \ 'b::real_normed_vector" shows "f -- a --> 0 \ (\x. norm (f x)) -- a --> 0" -by (drule LIM_norm, simp) +by (rule tendsto_norm_zero) lemma LIM_norm_zero_cancel: - fixes f :: "'a::metric_space \ 'b::real_normed_vector" + fixes f :: "'a::topological_space \ 'b::real_normed_vector" shows "(\x. norm (f x)) -- a --> 0 \ f -- a --> 0" -by (erule LIM_imp_LIM, simp) +by (rule tendsto_norm_zero_cancel) lemma LIM_norm_zero_iff: - fixes f :: "'a::metric_space \ 'b::real_normed_vector" + fixes f :: "'a::topological_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]) +by (rule tendsto_norm_zero_iff) lemma LIM_rabs: "f -- a --> (l::real) \ (\x. \f x\) -- a --> \l\" by (fold real_norm_def, rule LIM_norm) @@ -180,40 +181,32 @@ lemma LIM_rabs_zero_iff: "(\x. \f x\) -- a --> (0::real) = f -- a --> 0" by (fold real_norm_def, rule LIM_norm_zero_iff) +lemma at_neq_bot: + fixes a :: "'a::real_normed_algebra_1" + shows "at a \ bot" -- {* TODO: find a more appropriate class *} +unfolding eventually_False [symmetric] +unfolding eventually_at dist_norm +by (clarsimp, rule_tac x="a + of_real (d/2)" in exI, simp) + lemma LIM_const_not_eq: fixes a :: "'a::real_normed_algebra_1" + fixes k L :: "'b::metric_space" shows "k \ L \ \ (\x. k) -- a --> L" -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 +by (simp add: tendsto_const_iff at_neq_bot) lemmas LIM_not_zero = LIM_const_not_eq [where L = 0] lemma LIM_const_eq: fixes a :: "'a::real_normed_algebra_1" + fixes k L :: "'b::metric_space" shows "(\x. k) -- a --> L \ k = L" -apply (rule ccontr) -apply (blast dest: LIM_const_not_eq) -done +by (simp add: tendsto_const_iff at_neq_bot) lemma LIM_unique: fixes a :: "'a::real_normed_algebra_1" -- {* TODO: find a more appropriate class *} + fixes L M :: "'b::metric_space" shows "\f -- a --> L; f -- a --> M\ \ L = M" -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 +by (drule (1) tendsto_dist, simp add: tendsto_const_iff at_neq_bot) lemma LIM_ident [simp]: "(\x. x) -- a --> a" by (rule tendsto_ident_at) @@ -221,37 +214,33 @@ text{*Limits are equal for functions equal except at limit point*} lemma LIM_equal: "[| \x. x \ a --> (f x = g x) |] ==> (f -- a --> l) = (g -- a --> l)" -by (simp add: LIM_def) +unfolding tendsto_def eventually_at_topological by simp lemma LIM_cong: "\a = b; \x. x \ b \ f x = g x; l = m\ \ ((\x. f x) -- a --> l) = ((\x. g x) -- b --> m)" -by (simp add: LIM_def) +by (simp add: LIM_equal) lemma metric_LIM_equal2: assumes 1: "0 < R" 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) -apply (rule_tac x="min s R" in exI, safe) +apply (rule topological_tendstoI) +apply (drule (2) topological_tendstoD) +apply (simp add: eventually_at, safe) +apply (rule_tac x="min d R" in exI, safe) apply (simp add: 1) apply (simp add: 2) done lemma LIM_equal2: - fixes f g :: "'a::real_normed_vector \ 'b::metric_space" + fixes f g :: "'a::real_normed_vector \ 'b::topological_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 +by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm) -text{*Two uses in Transcendental.ML*} +text{*Two uses in Transcendental.ML*} (* BH: no longer true; delete? *) lemma LIM_trans: fixes f g :: "'a::metric_space \ 'b::real_normed_vector" shows "[| (%x. f(x) + -g(x)) -- a --> 0; g -- a --> l |] ==> f -- a --> l" @@ -263,24 +252,52 @@ assumes g: "g -- l --> g l" assumes f: "f -- a --> l" shows "(\x. g (f x)) -- a --> g l" -proof (rule metric_LIM_I) - fix r::real assume r: "0 < r" - obtain s where s: "0 < s" - 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; dist x a < t\ \ dist (f x) l < s" - using metric_LIM_D [OF f s] by fast +proof (rule topological_tendstoI) + fix C assume C: "open C" "g l \ C" + obtain B where B: "open B" "l \ B" + and gC: "\y. y \ B \ y \ l \ g y \ C" + using topological_tendstoD [OF g C] + unfolding eventually_at_topological by fast + obtain A where A: "open A" "a \ A" + and fB: "\x. x \ A \ x \ a \ f x \ B" + using topological_tendstoD [OF f B] + unfolding eventually_at_topological by fast + show "eventually (\x. g (f x) \ C) (at a)" + unfolding eventually_at_topological + proof (intro exI conjI ballI impI) + show "open A" and "a \ A" using A . + next + fix x assume "x \ A" and "x \ a" + then show "g (f x) \ C" + by (cases "f x = l", simp add: C, simp add: gC fB) + qed +qed - 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 . +lemma LIM_compose_eventually: + assumes f: "f -- a --> b" + assumes g: "g -- b --> c" + assumes inj: "eventually (\x. f x \ b) (at a)" + shows "(\x. g (f x)) -- a --> c" +proof (rule topological_tendstoI) + fix C assume C: "open C" "c \ C" + obtain B where B: "open B" "b \ B" + and gC: "\y. y \ B \ y \ b \ g y \ C" + using topological_tendstoD [OF g C] + unfolding eventually_at_topological by fast + obtain A where A: "open A" "a \ A" + and fB: "\x. x \ A \ x \ a \ f x \ B" + using topological_tendstoD [OF f B] + unfolding eventually_at_topological by fast + have "eventually (\x. f x \ b \ g (f x) \ C) (at a)" + unfolding eventually_at_topological + proof (intro exI conjI ballI impI) + show "open A" and "a \ A" using A . next - 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) + fix x assume "x \ A" and "x \ a" and "f x \ b" + then show "g (f x) \ C" by (simp add: gC fB) qed + with inj show "eventually (\x. g (f x) \ C) (at a)" + by (rule eventually_rev_mp) qed lemma metric_LIM_compose2: @@ -288,31 +305,8 @@ 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 +using f g inj [folded eventually_at] +by (rule LIM_compose_eventually) lemma LIM_compose2: fixes a :: "'a::real_normed_vector" @@ -326,7 +320,7 @@ unfolding o_def by (rule LIM_compose) lemma real_LIM_sandwich_zero: - fixes f g :: "'a::metric_space \ real" + fixes f g :: "'a::topological_space \ real" assumes f: "f -- a --> 0" assumes 1: "\x. x \ a \ 0 \ g x" assumes 2: "\x. x \ a \ g x \ f x" @@ -593,7 +587,7 @@ subsection {* Relation of LIM and LIMSEQ *} lemma LIMSEQ_SEQ_conv1: - fixes a :: "'a::metric_space" + fixes a :: "'a::metric_space" and L :: "'b::metric_space" assumes X: "X -- a --> L" shows "\S. (\n. S n \ a) \ S ----> a \ (\n. X (S n)) ----> L" proof (safe intro!: metric_LIMSEQ_I) @@ -614,7 +608,7 @@ lemma LIMSEQ_SEQ_conv2: - fixes a :: real + fixes a :: real and L :: "'a::metric_space" assumes "\S. (\n. S n \ a) \ S ----> a \ (\n. X (S n)) ----> L" shows "X -- a --> L" proof (rule ccontr) @@ -682,7 +676,7 @@ lemma LIMSEQ_SEQ_conv: "(\S. (\n. S n \ a) \ S ----> (a::real) \ (\n. X (S n)) ----> L) = - (X -- a --> L)" + (X -- a --> (L::'a::metric_space))" proof assume "\S. (\n. S n \ a) \ S ----> a \ (\n. X (S n)) ----> L" thus "X -- a --> L" by (rule LIMSEQ_SEQ_conv2) diff -r 0a5b7b818d65 -r 621122eeb138 src/HOL/Limits.thy --- a/src/HOL/Limits.thy Tue May 04 10:42:47 2010 -0700 +++ b/src/HOL/Limits.thy Tue May 04 13:08:56 2010 -0700 @@ -269,13 +269,39 @@ by (simp add: expand_net_eq eventually_netmap) -subsection {* Standard Nets *} +subsection {* Sequentially *} definition sequentially :: "nat net" where [code del]: "sequentially = Abs_net (\P. \k. \n\k. P n)" +lemma eventually_sequentially: + "eventually P sequentially \ (\N. \n\N. P n)" +unfolding sequentially_def +proof (rule eventually_Abs_net, rule is_filter.intro) + fix P Q :: "nat \ bool" + assume "\i. \n\i. P n" and "\j. \n\j. Q n" + then obtain i j where "\n\i. P n" and "\n\j. Q n" by auto + then have "\n\max i j. P n \ Q n" by simp + then show "\k. \n\k. P n \ Q n" .. +qed auto + +lemma sequentially_bot [simp]: "sequentially \ bot" +unfolding expand_net_eq eventually_sequentially by auto + +lemma eventually_False_sequentially [simp]: + "\ eventually (\n. False) sequentially" +by (simp add: eventually_False) + +lemma le_sequentially: + "net \ sequentially \ (\N. eventually (\n. N \ n) net)" +unfolding le_net_def eventually_sequentially +by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp) + + +subsection {* Standard Nets *} + definition within :: "'a net \ 'a set \ 'a net" (infixr "within" 70) where [code del]: @@ -291,17 +317,6 @@ where [code del]: "at a = nhds a within - {a}" -lemma eventually_sequentially: - "eventually P sequentially \ (\N. \n\N. P n)" -unfolding sequentially_def -proof (rule eventually_Abs_net, rule is_filter.intro) - fix P Q :: "nat \ bool" - assume "\i. \n\i. P n" and "\j. \n\j. Q n" - then obtain i j where "\n\i. P n" and "\n\j. Q n" by auto - then have "\n\max i j. P n \ Q n" by simp - then show "\k. \n\k. P n \ Q n" .. -qed auto - lemma eventually_within: "eventually P (net within S) = eventually (\x. x \ S \ P x) net" unfolding within_def @@ -598,6 +613,16 @@ lemma tendsto_const [tendsto_intros]: "((\x. k) ---> k) net" by (simp add: tendsto_def) +lemma tendsto_const_iff: + fixes k l :: "'a::metric_space" + assumes "net \ bot" shows "((\n. k) ---> l) net \ k = l" +apply (safe intro!: tendsto_const) +apply (rule ccontr) +apply (drule_tac e="dist k l" in tendstoD) +apply (simp add: zero_less_dist_iff) +apply (simp add: eventually_False assms) +done + lemma tendsto_dist [tendsto_intros]: assumes f: "(f ---> l) net" and g: "(g ---> m) net" shows "((\x. dist (f x) (g x)) ---> dist l m) net" @@ -618,13 +643,24 @@ qed qed +lemma norm_conv_dist: "norm x = dist x 0" +unfolding dist_norm by simp + lemma tendsto_norm [tendsto_intros]: "(f ---> a) net \ ((\x. norm (f x)) ---> norm a) net" -apply (simp add: tendsto_iff dist_norm, safe) -apply (drule_tac x="e" in spec, safe) -apply (erule eventually_elim1) -apply (erule order_le_less_trans [OF norm_triangle_ineq3]) -done +unfolding norm_conv_dist by (intro tendsto_intros) + +lemma tendsto_norm_zero: + "(f ---> 0) net \ ((\x. norm (f x)) ---> 0) net" +by (drule tendsto_norm, simp) + +lemma tendsto_norm_zero_cancel: + "((\x. norm (f x)) ---> 0) net \ (f ---> 0) net" +unfolding tendsto_iff dist_norm by simp + +lemma tendsto_norm_zero_iff: + "((\x. norm (f x)) ---> 0) net \ (f ---> 0) net" +unfolding tendsto_iff dist_norm by simp lemma add_diff_add: fixes a b c d :: "'a::ab_group_add" diff -r 0a5b7b818d65 -r 621122eeb138 src/HOL/SEQ.thy --- a/src/HOL/SEQ.thy Tue May 04 10:42:47 2010 -0700 +++ b/src/HOL/SEQ.thy Tue May 04 13:08:56 2010 -0700 @@ -14,7 +14,7 @@ begin abbreviation - LIMSEQ :: "[nat \ 'a::metric_space, 'a] \ bool" + LIMSEQ :: "[nat \ 'a::topological_space, 'a] \ bool" ("((_)/ ----> (_))" [60, 60] 60) where "X ----> L \ (X ---> L) sequentially" @@ -153,13 +153,10 @@ lemma LIMSEQ_const: "(\n. k) ----> k" by (rule tendsto_const) -lemma LIMSEQ_const_iff: "(\n. k) ----> l \ k = l" -apply (safe intro!: LIMSEQ_const) -apply (rule ccontr) -apply (drule_tac r="dist k l" in metric_LIMSEQ_D) -apply (simp add: zero_less_dist_iff) -apply auto -done +lemma LIMSEQ_const_iff: + fixes k l :: "'a::metric_space" + shows "(\n. k) ----> l \ k = l" +by (rule tendsto_const_iff, rule sequentially_bot) lemma LIMSEQ_norm: fixes a :: "'a::real_normed_vector" @@ -168,8 +165,9 @@ lemma LIMSEQ_ignore_initial_segment: "f ----> a \ (\n. f (n + k)) ----> a" -apply (rule metric_LIMSEQ_I) -apply (drule (1) metric_LIMSEQ_D) +apply (rule topological_tendstoI) +apply (drule (2) topological_tendstoD) +apply (simp only: eventually_sequentially) apply (erule exE, rename_tac N) apply (rule_tac x=N in exI) apply simp @@ -177,8 +175,9 @@ lemma LIMSEQ_offset: "(\n. f (n + k)) ----> a \ f ----> a" -apply (rule metric_LIMSEQ_I) -apply (drule (1) metric_LIMSEQ_D) +apply (rule topological_tendstoI) +apply (drule (2) topological_tendstoD) +apply (simp only: eventually_sequentially) apply (erule exE, rename_tac N) apply (rule_tac x="N + k" in exI) apply clarify @@ -196,7 +195,7 @@ by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc) lemma LIMSEQ_linear: "\ X ----> x ; l > 0 \ \ (\ n. X (n * l)) ----> x" - unfolding LIMSEQ_def + unfolding tendsto_def eventually_sequentially by (metis div_le_dividend div_mult_self1_is_m le_trans nat_mult_commute) lemma LIMSEQ_add: @@ -219,7 +218,9 @@ shows "\X ----> a; Y ----> b\ \ (\n. X n - Y n) ----> a - b" by (rule tendsto_diff) -lemma LIMSEQ_unique: "\X ----> a; X ----> b\ \ a = b" +lemma LIMSEQ_unique: + fixes a b :: "'a::metric_space" + shows "\X ----> a; X ----> b\ \ a = b" apply (rule ccontr) apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff) apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff) @@ -750,9 +751,10 @@ lemma LIMSEQ_subseq_LIMSEQ: "\ X ----> L; subseq f \ \ (X o f) ----> L" -apply (auto simp add: LIMSEQ_def) -apply (drule_tac x=r in spec, clarify) -apply (rule_tac x=no in exI, clarify) +apply (rule topological_tendstoI) +apply (drule (2) topological_tendstoD) +apply (simp only: eventually_sequentially) +apply (clarify, rule_tac x=N in exI, clarsimp) apply (blast intro: seq_suble le_trans dest!: spec) done @@ -836,12 +838,8 @@ apply (blast dest: order_antisym)+ done -text{* The best of both worlds: Easier to prove this result as a standard - theorem and then use equivalence to "transfer" it into the - equivalent nonstandard form if needed!*} - lemma Bmonoseq_LIMSEQ: "\n. m \ n --> X n = X m ==> \L. (X ----> L)" -apply (simp add: LIMSEQ_def) +unfolding tendsto_def eventually_sequentially apply (rule_tac x = "X m" in exI, safe) apply (rule_tac x = m in exI, safe) apply (drule spec, erule impE, auto)