# HG changeset patch # User huffman # Date 1243987402 25200 # Node ID 69570155ddf8aa541bd4fbc7b7ef8d38af6ea04f # Parent 97a2a3d4088ebab4ff4b566967d0def9a0b25c99 replace filters with filter bases diff -r 97a2a3d4088e -r 69570155ddf8 src/HOL/Lim.thy --- a/src/HOL/Lim.thy Tue Jun 02 15:37:59 2009 -0700 +++ b/src/HOL/Lim.thy Tue Jun 02 17:03:22 2009 -0700 @@ -13,10 +13,6 @@ text{*Standard Definitions*} definition - at :: "'a::metric_space \ 'a filter" where - [code del]: "at a = Abs_filter (\P. \r>0. \x. x \ a \ dist x a < r \ P x)" - -definition LIM :: "['a::metric_space \ 'b::metric_space, 'a, 'b] \ bool" ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where [code del]: "f -- a --> L = @@ -31,23 +27,11 @@ 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 {* Neighborhood Filter *} - -lemma eventually_at: - "eventually P (at a) \ (\d>0. \x. x \ a \ dist x a < d \ P x)" -unfolding at_def -apply (rule eventually_Abs_filter) -apply (rule_tac x=1 in exI, simp) -apply (clarify, rule_tac x=r in exI, simp) -apply (clarify, rename_tac r s) -apply (rule_tac x="min r s" in exI, simp) -done +subsection {* Limits of Functions *} lemma LIM_conv_tendsto: "(f -- a --> L) \ tendsto f L (at a)" unfolding LIM_def tendsto_def eventually_at .. -subsection {* Limits of Functions *} - lemma metric_LIM_I: "(\r. 0 < r \ \s>0. \x. x \ a \ dist x a < s \ dist (f x) L < r) \ f -- a --> L" diff -r 97a2a3d4088e -r 69570155ddf8 src/HOL/Limits.thy --- a/src/HOL/Limits.thy Tue Jun 02 15:37:59 2009 -0700 +++ b/src/HOL/Limits.thy Tue Jun 02 17:03:22 2009 -0700 @@ -8,128 +8,204 @@ imports RealVector RComplete begin -subsection {* Filters *} +subsection {* Nets *} + +text {* + A net is now defined as a filter base. + The definition also allows non-proper filter bases. +*} + +typedef (open) 'a net = + "{net :: 'a set set. (\A. A \ net) + \ (\A\net. \B\net. \C\net. C \ A \ C \ B)}" +proof + show "UNIV \ ?net" by auto +qed -typedef (open) 'a filter = - "{f :: ('a \ bool) \ bool. f (\x. True) - \ (\P Q. (\x. P x \ Q x) \ f P \ f Q) - \ (\P Q. f P \ f Q \ f (\x. P x \ Q x))}" -proof - show "(\P. True) \ ?filter" by simp -qed +lemma Rep_net_nonempty: "\A. A \ Rep_net net" +using Rep_net [of net] by simp + +lemma Rep_net_directed: + "A \ Rep_net net \ B \ Rep_net net \ \C\Rep_net net. C \ A \ C \ B" +using Rep_net [of net] by simp + +lemma Abs_net_inverse': + assumes "\A. A \ net" + assumes "\A B. A \ net \ B \ net \ \C\net. C \ A \ C \ B" + shows "Rep_net (Abs_net net) = net" +using assms by (simp add: Abs_net_inverse) + +lemma image_nonempty: "\x. x \ A \ \x. x \ f ` A" +by auto + + +subsection {* Eventually *} definition - eventually :: "('a \ bool) \ 'a filter \ bool" where - [code del]: "eventually P F \ Rep_filter F P" + eventually :: "('a \ bool) \ 'a net \ bool" where + [code del]: "eventually P net \ (\A\Rep_net net. \x\A. P x)" -lemma eventually_True [simp]: "eventually (\x. True) F" -unfolding eventually_def using Rep_filter [of F] by blast +lemma eventually_True [simp]: "eventually (\x. True) net" +unfolding eventually_def using Rep_net_nonempty [of net] by fast lemma eventually_mono: - "(\x. P x \ Q x) \ eventually P F \ eventually Q F" -unfolding eventually_def using Rep_filter [of F] by blast + "(\x. P x \ Q x) \ eventually P net \ eventually Q net" +unfolding eventually_def by blast lemma eventually_conj: - "\eventually (\x. P x) F; eventually (\x. Q x) F\ - \ eventually (\x. P x \ Q x) F" -unfolding eventually_def using Rep_filter [of F] by blast + assumes P: "eventually (\x. P x) net" + assumes Q: "eventually (\x. Q x) net" + shows "eventually (\x. P x \ Q x) net" +proof - + obtain A where A: "A \ Rep_net net" "\x\A. P x" + using P unfolding eventually_def by fast + obtain B where B: "B \ Rep_net net" "\x\B. Q x" + using Q unfolding eventually_def by fast + obtain C where C: "C \ Rep_net net" "C \ A" "C \ B" + using Rep_net_directed [OF A(1) B(1)] by fast + then have "\x\C. P x \ Q x" "C \ Rep_net net" + using A(2) B(2) by auto + then show ?thesis unfolding eventually_def .. +qed lemma eventually_mp: - assumes "eventually (\x. P x \ Q x) F" - assumes "eventually (\x. P x) F" - shows "eventually (\x. Q x) F" + assumes "eventually (\x. P x \ Q x) net" + assumes "eventually (\x. P x) net" + shows "eventually (\x. Q x) net" proof (rule eventually_mono) show "\x. (P x \ Q x) \ P x \ Q x" by simp - show "eventually (\x. (P x \ Q x) \ P x) F" + show "eventually (\x. (P x \ Q x) \ P x) net" using assms by (rule eventually_conj) qed lemma eventually_rev_mp: - assumes "eventually (\x. P x) F" - assumes "eventually (\x. P x \ Q x) F" - shows "eventually (\x. Q x) F" + assumes "eventually (\x. P x) net" + assumes "eventually (\x. P x \ Q x) net" + shows "eventually (\x. Q x) net" using assms(2) assms(1) by (rule eventually_mp) lemma eventually_conj_iff: "eventually (\x. P x \ Q x) net \ eventually P net \ eventually Q net" by (auto intro: eventually_conj elim: eventually_rev_mp) -lemma eventually_Abs_filter: - assumes "f (\x. True)" - assumes "\P Q. (\x. P x \ Q x) \ f P \ f Q" - assumes "\P Q. f P \ f Q \ f (\x. P x \ Q x)" - shows "eventually P (Abs_filter f) \ f P" -unfolding eventually_def using assms -by (subst Abs_filter_inverse, auto) - -lemma filter_ext: - "(\P. eventually P F \ eventually P F') \ F = F'" -unfolding eventually_def -by (simp add: Rep_filter_inject [THEN iffD1] ext) - lemma eventually_elim1: - assumes "eventually (\i. P i) F" + assumes "eventually (\i. P i) net" assumes "\i. P i \ Q i" - shows "eventually (\i. Q i) F" + shows "eventually (\i. Q i) net" using assms by (auto elim!: eventually_rev_mp) lemma eventually_elim2: - assumes "eventually (\i. P i) F" - assumes "eventually (\i. Q i) F" + assumes "eventually (\i. P i) net" + assumes "eventually (\i. Q i) net" assumes "\i. P i \ Q i \ R i" - shows "eventually (\i. R i) F" + shows "eventually (\i. R i) net" using assms by (auto elim!: eventually_rev_mp) +subsection {* Standard Nets *} + +definition + sequentially :: "nat net" where + [code del]: "sequentially = Abs_net (range (\n. {n..}))" + +definition + at :: "'a::metric_space \ 'a net" where + [code del]: "at a = Abs_net ((\r. {x. x \ a \ dist x a < r}) ` {r. 0 < r})" + +definition + within :: "'a net \ 'a set \ 'a net" (infixr "within" 70) where + [code del]: "net within S = Abs_net ((\A. A \ S) ` Rep_net net)" + +lemma Rep_net_sequentially: + "Rep_net sequentially = range (\n. {n..})" +unfolding sequentially_def +apply (rule Abs_net_inverse') +apply (rule image_nonempty, simp) +apply (clarsimp, rename_tac m n) +apply (rule_tac x="max m n" in exI, auto) +done + +lemma Rep_net_at: + "Rep_net (at a) = ((\r. {x. x \ a \ dist x a < r}) ` {r. 0 < r})" +unfolding at_def +apply (rule Abs_net_inverse') +apply (rule image_nonempty, rule_tac x=1 in exI, simp) +apply (clarsimp, rename_tac r s) +apply (rule_tac x="min r s" in exI, auto) +done + +lemma Rep_net_within: + "Rep_net (net within S) = (\A. A \ S) ` Rep_net net" +unfolding within_def +apply (rule Abs_net_inverse') +apply (rule image_nonempty, rule Rep_net_nonempty) +apply (clarsimp, rename_tac A B) +apply (drule (1) Rep_net_directed) +apply (clarify, rule_tac x=C in bexI, auto) +done + +lemma eventually_sequentially: + "eventually P sequentially \ (\N. \n\N. P n)" +unfolding eventually_def Rep_net_sequentially by auto + +lemma eventually_at: + "eventually P (at a) \ (\d>0. \x. x \ a \ dist x a < d \ P x)" +unfolding eventually_def Rep_net_at by auto + +lemma eventually_within: + "eventually P (net within S) = eventually (\x. x \ S \ P x) net" +unfolding eventually_def Rep_net_within by auto + + subsection {* Boundedness *} definition - Bfun :: "('a \ 'b::real_normed_vector) \ 'a filter \ bool" where - [code del]: "Bfun S F = (\K>0. eventually (\i. norm (S i) \ K) F)" + Bfun :: "('a \ 'b::real_normed_vector) \ 'a net \ bool" where + [code del]: "Bfun S net = (\K>0. eventually (\i. norm (S i) \ K) net)" -lemma BfunI: assumes K: "eventually (\i. norm (X i) \ K) F" shows "Bfun X F" +lemma BfunI: assumes K: "eventually (\i. norm (X i) \ K) net" shows "Bfun X net" unfolding Bfun_def proof (intro exI conjI allI) show "0 < max K 1" by simp next - show "eventually (\i. norm (X i) \ max K 1) F" + show "eventually (\i. norm (X i) \ max K 1) net" using K by (rule eventually_elim1, simp) qed lemma BfunE: - assumes "Bfun S F" - obtains B where "0 < B" and "eventually (\i. norm (S i) \ B) F" + assumes "Bfun S net" + obtains B where "0 < B" and "eventually (\i. norm (S i) \ B) net" using assms unfolding Bfun_def by fast subsection {* Convergence to Zero *} definition - Zfun :: "('a \ 'b::real_normed_vector) \ 'a filter \ bool" where - [code del]: "Zfun S F = (\r>0. eventually (\i. norm (S i) < r) F)" + Zfun :: "('a \ 'b::real_normed_vector) \ 'a net \ bool" where + [code del]: "Zfun S net = (\r>0. eventually (\i. norm (S i) < r) net)" lemma ZfunI: - "(\r. 0 < r \ eventually (\i. norm (S i) < r) F) \ Zfun S F" + "(\r. 0 < r \ eventually (\i. norm (S i) < r) net) \ Zfun S net" unfolding Zfun_def by simp lemma ZfunD: - "\Zfun S F; 0 < r\ \ eventually (\i. norm (S i) < r) F" + "\Zfun S net; 0 < r\ \ eventually (\i. norm (S i) < r) net" unfolding Zfun_def by simp lemma Zfun_ssubst: - "eventually (\i. X i = Y i) F \ Zfun Y F \ Zfun X F" + "eventually (\i. X i = Y i) net \ Zfun Y net \ Zfun X net" unfolding Zfun_def by (auto elim!: eventually_rev_mp) -lemma Zfun_zero: "Zfun (\i. 0) F" +lemma Zfun_zero: "Zfun (\i. 0) net" unfolding Zfun_def by simp -lemma Zfun_norm_iff: "Zfun (\i. norm (S i)) F = Zfun (\i. S i) F" +lemma Zfun_norm_iff: "Zfun (\i. norm (S i)) net = Zfun (\i. S i) net" unfolding Zfun_def by simp lemma Zfun_imp_Zfun: - assumes X: "Zfun X F" - assumes Y: "eventually (\i. norm (Y i) \ norm (X i) * K) F" - shows "Zfun (\n. Y n) F" + assumes X: "Zfun X net" + assumes Y: "eventually (\i. norm (Y i) \ norm (X i) * K) net" + shows "Zfun (\n. Y n) net" proof (cases) assume K: "0 < K" show ?thesis @@ -137,9 +213,9 @@ fix r::real assume "0 < r" hence "0 < r / K" using K by (rule divide_pos_pos) - then have "eventually (\i. norm (X i) < r / K) F" + then have "eventually (\i. norm (X i) < r / K) net" using ZfunD [OF X] by fast - with Y show "eventually (\i. norm (Y i) < r) F" + with Y show "eventually (\i. norm (Y i) < r) net" proof (rule eventually_elim2) fix i assume *: "norm (Y i) \ norm (X i) * K" @@ -157,7 +233,7 @@ proof (rule ZfunI) fix r :: real assume "0 < r" - from Y show "eventually (\i. norm (Y i) < r) F" + from Y show "eventually (\i. norm (Y i) < r) net" proof (rule eventually_elim1) fix i assume "norm (Y i) \ norm (X i) * K" @@ -169,22 +245,22 @@ qed qed -lemma Zfun_le: "\Zfun Y F; \n. norm (X n) \ norm (Y n)\ \ Zfun X F" +lemma Zfun_le: "\Zfun Y net; \n. norm (X n) \ norm (Y n)\ \ Zfun X net" by (erule_tac K="1" in Zfun_imp_Zfun, simp) lemma Zfun_add: - assumes X: "Zfun X F" and Y: "Zfun Y F" - shows "Zfun (\n. X n + Y n) F" + assumes X: "Zfun X net" and Y: "Zfun Y net" + shows "Zfun (\n. X n + Y n) net" proof (rule ZfunI) fix r::real assume "0 < r" hence r: "0 < r / 2" by simp - have "eventually (\i. norm (X i) < r/2) F" + have "eventually (\i. norm (X i) < r/2) net" using X r by (rule ZfunD) moreover - have "eventually (\i. norm (Y i) < r/2) F" + have "eventually (\i. norm (Y i) < r/2) net" using Y r by (rule ZfunD) ultimately - show "eventually (\i. norm (X i + Y i) < r) F" + show "eventually (\i. norm (X i + Y i) < r) net" proof (rule eventually_elim2) fix i assume *: "norm (X i) < r/2" "norm (Y i) < r/2" @@ -197,28 +273,28 @@ qed qed -lemma Zfun_minus: "Zfun X F \ Zfun (\i. - X i) F" +lemma Zfun_minus: "Zfun X net \ Zfun (\i. - X i) net" unfolding Zfun_def by simp -lemma Zfun_diff: "\Zfun X F; Zfun Y F\ \ Zfun (\i. X i - Y i) F" +lemma Zfun_diff: "\Zfun X net; Zfun Y net\ \ Zfun (\i. X i - Y i) net" by (simp only: diff_minus Zfun_add Zfun_minus) lemma (in bounded_linear) Zfun: - assumes X: "Zfun X F" - shows "Zfun (\n. f (X n)) F" + assumes X: "Zfun X net" + shows "Zfun (\n. f (X n)) net" proof - obtain K where "\x. norm (f x) \ norm x * K" using bounded by fast - then have "eventually (\i. norm (f (X i)) \ norm (X i) * K) F" + then have "eventually (\i. norm (f (X i)) \ norm (X i) * K) net" by simp with X show ?thesis by (rule Zfun_imp_Zfun) qed lemma (in bounded_bilinear) Zfun: - assumes X: "Zfun X F" - assumes Y: "Zfun Y F" - shows "Zfun (\n. X n ** Y n) F" + assumes X: "Zfun X net" + assumes Y: "Zfun Y net" + shows "Zfun (\n. X n ** Y n) net" proof (rule ZfunI) fix r::real assume r: "0 < r" obtain K where K: "0 < K" @@ -226,13 +302,13 @@ using pos_bounded by fast from K have K': "0 < inverse K" by (rule positive_imp_inverse_positive) - have "eventually (\i. norm (X i) < r) F" + have "eventually (\i. norm (X i) < r) net" using X r by (rule ZfunD) moreover - have "eventually (\i. norm (Y i) < inverse K) F" + have "eventually (\i. norm (Y i) < inverse K) net" using Y K' by (rule ZfunD) ultimately - show "eventually (\i. norm (X i ** Y i) < r) F" + show "eventually (\i. norm (X i ** Y i) < r) net" proof (rule eventually_elim2) fix i assume *: "norm (X i) < r" "norm (Y i) < inverse K" @@ -247,11 +323,11 @@ qed lemma (in bounded_bilinear) Zfun_left: - "Zfun X F \ Zfun (\n. X n ** a) F" + "Zfun X net \ Zfun (\n. X n ** a) net" by (rule bounded_linear_left [THEN bounded_linear.Zfun]) lemma (in bounded_bilinear) Zfun_right: - "Zfun X F \ Zfun (\n. a ** X n) F" + "Zfun X net \ Zfun (\n. a ** X n) net" by (rule bounded_linear_right [THEN bounded_linear.Zfun]) lemmas Zfun_mult = mult.Zfun @@ -262,7 +338,7 @@ subsection{* Limits *} definition - tendsto :: "('a \ 'b::metric_space) \ 'b \ 'a filter \ bool" where + tendsto :: "('a \ 'b::metric_space) \ 'b \ 'a net \ bool" where [code del]: "tendsto f l net \ (\e>0. eventually (\x. dist (f x) l < e) net)" lemma tendstoI: @@ -274,15 +350,15 @@ "tendsto f l net \ 0 < e \ eventually (\x. dist (f x) l < e) net" unfolding tendsto_def by auto -lemma tendsto_Zfun_iff: "tendsto (\n. X n) L F = Zfun (\n. X n - L) F" +lemma tendsto_Zfun_iff: "tendsto (\n. X n) L net = Zfun (\n. X n - L) net" by (simp only: tendsto_def Zfun_def dist_norm) -lemma tendsto_const: "tendsto (\n. k) k F" +lemma tendsto_const: "tendsto (\n. k) k net" by (simp add: tendsto_def) lemma tendsto_norm: fixes a :: "'a::real_normed_vector" - shows "tendsto X a F \ tendsto (\n. norm (X n)) (norm a) F" + shows "tendsto X a net \ tendsto (\n. norm (X n)) (norm a) net" apply (simp add: tendsto_def dist_norm, safe) apply (drule_tac x="e" in spec, safe) apply (erule eventually_elim1) @@ -301,30 +377,30 @@ lemma tendsto_add: fixes a b :: "'a::real_normed_vector" - shows "\tendsto X a F; tendsto Y b F\ \ tendsto (\n. X n + Y n) (a + b) F" + shows "\tendsto X a net; tendsto Y b net\ \ tendsto (\n. X n + Y n) (a + b) net" by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add) lemma tendsto_minus: fixes a :: "'a::real_normed_vector" - shows "tendsto X a F \ tendsto (\n. - X n) (- a) F" + shows "tendsto X a net \ tendsto (\n. - X n) (- a) net" by (simp only: tendsto_Zfun_iff minus_diff_minus Zfun_minus) lemma tendsto_minus_cancel: fixes a :: "'a::real_normed_vector" - shows "tendsto (\n. - X n) (- a) F \ tendsto X a F" + shows "tendsto (\n. - X n) (- a) net \ tendsto X a net" by (drule tendsto_minus, simp) lemma tendsto_diff: fixes a b :: "'a::real_normed_vector" - shows "\tendsto X a F; tendsto Y b F\ \ tendsto (\n. X n - Y n) (a - b) F" + shows "\tendsto X a net; tendsto Y b net\ \ tendsto (\n. X n - Y n) (a - b) net" by (simp add: diff_minus tendsto_add tendsto_minus) lemma (in bounded_linear) tendsto: - "tendsto X a F \ tendsto (\n. f (X n)) (f a) F" + "tendsto X a net \ tendsto (\n. f (X n)) (f a) net" by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun) lemma (in bounded_bilinear) tendsto: - "\tendsto X a F; tendsto Y b F\ \ tendsto (\n. X n ** Y n) (a ** b) F" + "\tendsto X a net; tendsto Y b net\ \ tendsto (\n. X n ** Y n) (a ** b) net" by (simp only: tendsto_Zfun_iff prod_diff_prod Zfun_add Zfun Zfun_left Zfun_right) @@ -332,17 +408,17 @@ subsection {* Continuity of Inverse *} lemma (in bounded_bilinear) Zfun_prod_Bfun: - assumes X: "Zfun X F" - assumes Y: "Bfun Y F" - shows "Zfun (\n. X n ** Y n) F" + assumes X: "Zfun X net" + assumes Y: "Bfun Y net" + shows "Zfun (\n. X n ** Y n) net" proof - obtain K where K: "0 \ K" and norm_le: "\x y. norm (x ** y) \ norm x * norm y * K" using nonneg_bounded by fast obtain B where B: "0 < B" - and norm_Y: "eventually (\i. norm (Y i) \ B) F" + and norm_Y: "eventually (\i. norm (Y i) \ B) net" using Y by (rule BfunE) - have "eventually (\i. norm (X i ** Y i) \ norm (X i) * (B * K)) F" + have "eventually (\i. norm (X i ** Y i) \ norm (X i) * (B * K)) net" using norm_Y proof (rule eventually_elim1) fix i assume *: "norm (Y i) \ B" @@ -370,9 +446,9 @@ using bounded by fast lemma (in bounded_bilinear) Bfun_prod_Zfun: - assumes X: "Bfun X F" - assumes Y: "Zfun Y F" - shows "Zfun (\n. X n ** Y n) F" + assumes X: "Bfun X net" + assumes Y: "Zfun Y net" + shows "Zfun (\n. X n ** Y n) net" using flip Y X by (rule bounded_bilinear.Zfun_prod_Bfun) lemma inverse_diff_inverse: @@ -389,16 +465,16 @@ lemma Bfun_inverse: fixes a :: "'a::real_normed_div_algebra" - assumes X: "tendsto X a F" + assumes X: "tendsto X a net" assumes a: "a \ 0" - shows "Bfun (\n. inverse (X n)) F" + shows "Bfun (\n. inverse (X n)) net" proof - from a have "0 < norm a" by simp hence "\r>0. r < norm a" by (rule dense) then obtain r where r1: "0 < r" and r2: "r < norm a" by fast - have "eventually (\i. dist (X i) a < r) F" + have "eventually (\i. dist (X i) a < r) net" using tendstoD [OF X r1] by fast - hence "eventually (\i. norm (inverse (X i)) \ inverse (norm a - r)) F" + hence "eventually (\i. norm (inverse (X i)) \ inverse (norm a - r)) net" proof (rule eventually_elim1) fix i assume "dist (X i) a < r" @@ -425,8 +501,8 @@ lemma tendsto_inverse_lemma: fixes a :: "'a::real_normed_div_algebra" - shows "\tendsto X a F; a \ 0; eventually (\i. X i \ 0) F\ - \ tendsto (\i. inverse (X i)) (inverse a) F" + shows "\tendsto X a net; a \ 0; eventually (\i. X i \ 0) net\ + \ tendsto (\i. inverse (X i)) (inverse a) net" apply (subst tendsto_Zfun_iff) apply (rule Zfun_ssubst) apply (erule eventually_elim1) @@ -440,14 +516,14 @@ lemma tendsto_inverse: fixes a :: "'a::real_normed_div_algebra" - assumes X: "tendsto X a F" + assumes X: "tendsto X a net" assumes a: "a \ 0" - shows "tendsto (\i. inverse (X i)) (inverse a) F" + shows "tendsto (\i. inverse (X i)) (inverse a) net" proof - from a have "0 < norm a" by simp - with X have "eventually (\i. dist (X i) a < norm a) F" + with X have "eventually (\i. dist (X i) a < norm a) net" by (rule tendstoD) - then have "eventually (\i. X i \ 0) F" + then have "eventually (\i. X i \ 0) net" unfolding dist_norm by (auto elim!: eventually_elim1) with X a show ?thesis by (rule tendsto_inverse_lemma) @@ -455,8 +531,8 @@ lemma tendsto_divide: fixes a b :: "'a::real_normed_field" - shows "\tendsto X a F; tendsto Y b F; b \ 0\ - \ tendsto (\n. X n / Y n) (a / b) F" + shows "\tendsto X a net; tendsto Y b net; b \ 0\ + \ tendsto (\n. X n / Y n) (a / b) net" by (simp add: mult.tendsto tendsto_inverse divide_inverse) end diff -r 97a2a3d4088e -r 69570155ddf8 src/HOL/SEQ.thy --- a/src/HOL/SEQ.thy Tue Jun 02 15:37:59 2009 -0700 +++ b/src/HOL/SEQ.thy Tue Jun 02 17:03:22 2009 -0700 @@ -13,10 +13,6 @@ begin definition - sequentially :: "nat filter" where - [code del]: "sequentially = Abs_filter (\P. \N. \n\N. P n)" - -definition Zseq :: "[nat \ 'a::real_normed_vector] \ bool" where --{*Standard definition of sequence converging to zero*} [code del]: "Zseq X = (\r>0. \no. \n\no. norm (X n) < r)" @@ -71,24 +67,6 @@ [code del]: "Cauchy X = (\e>0. \M. \m \ M. \n \ M. dist (X m) (X n) < e)" -subsection {* Sequentially *} - -lemma eventually_sequentially: - "eventually P sequentially \ (\N. \n\N. P n)" -unfolding sequentially_def -apply (rule eventually_Abs_filter) -apply simp -apply (clarify, rule_tac x=N in exI, simp) -apply (clarify, rename_tac M N) -apply (rule_tac x="max M N" in exI, simp) -done - -lemma Zseq_conv_Zfun: "Zseq X \ Zfun X sequentially" -unfolding Zseq_def Zfun_def eventually_sequentially .. - -lemma LIMSEQ_conv_tendsto: "(X ----> L) \ tendsto X L sequentially" -unfolding LIMSEQ_def tendsto_def eventually_sequentially .. - subsection {* Bounded Sequences *} lemma BseqI': assumes K: "\n. norm (X n) \ K" shows "Bseq X" @@ -150,6 +128,9 @@ "\Zseq X; 0 < r\ \ \no. \n\no. norm (X n) < r" unfolding Zseq_def by simp +lemma Zseq_conv_Zfun: "Zseq X \ Zfun X sequentially" +unfolding Zseq_def Zfun_def eventually_sequentially .. + lemma Zseq_zero: "Zseq (\n. 0)" unfolding Zseq_def by simp @@ -212,6 +193,9 @@ subsection {* Limits of Sequences *} +lemma LIMSEQ_conv_tendsto: "(X ----> L) \ tendsto X L sequentially" +unfolding LIMSEQ_def tendsto_def eventually_sequentially .. + lemma LIMSEQ_iff: fixes L :: "'a::real_normed_vector" shows "(X ----> L) = (\r>0. \no. \n \ no. norm (X n - L) < r)"