# HG changeset patch # User huffman # Date 1313342743 25200 # Node ID 18da2a87421cc52189eb8ec4d61f6a349cc6d767 # Parent f5363511b2129fd40b1a4e21f59f2b82c267e752 generalize constant 'lim' and limit uniqueness theorems to class t2_space diff -r f5363511b212 -r 18da2a87421c src/HOL/Lim.thy --- a/src/HOL/Lim.thy Sun Aug 14 08:45:38 2011 -0700 +++ b/src/HOL/Lim.thy Sun Aug 14 10:25:43 2011 -0700 @@ -181,32 +181,32 @@ lemma LIM_rabs_zero_iff: "(\x. \f x\) -- a --> (0::real) = f -- a --> 0" by (rule tendsto_rabs_zero_iff) -lemma at_neq_bot: +lemma trivial_limit_at: fixes a :: "'a::real_normed_algebra_1" - shows "at a \ bot" -- {* TODO: find a more appropriate class *} -unfolding eventually_False [symmetric] + shows "\ trivial_limit (at a)" -- {* TODO: find a more appropriate class *} +unfolding trivial_limit_def 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" + fixes k L :: "'b::t2_space" shows "k \ L \ \ (\x. k) -- a --> L" -by (simp add: tendsto_const_iff at_neq_bot) +by (simp add: tendsto_const_iff trivial_limit_at) 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" + fixes k L :: "'b::t2_space" shows "(\x. k) -- a --> L \ k = L" -by (simp add: tendsto_const_iff at_neq_bot) + by (simp add: tendsto_const_iff trivial_limit_at) lemma LIM_unique: fixes a :: "'a::real_normed_algebra_1" -- {* TODO: find a more appropriate class *} - fixes L M :: "'b::metric_space" + fixes L M :: "'b::t2_space" shows "\f -- a --> L; f -- a --> M\ \ L = M" -by (drule (1) tendsto_dist, simp add: tendsto_const_iff at_neq_bot) + using trivial_limit_at by (rule tendsto_unique) lemma LIM_ident [simp]: "(\x. x) -- a --> a" by (rule tendsto_ident_at) diff -r f5363511b212 -r 18da2a87421c src/HOL/Limits.thy --- a/src/HOL/Limits.thy Sun Aug 14 08:45:38 2011 -0700 +++ b/src/HOL/Limits.thy Sun Aug 14 10:25:43 2011 -0700 @@ -581,15 +581,37 @@ lemma tendsto_const [tendsto_intros]: "((\x. k) ---> k) F" by (simp add: tendsto_def) +lemma tendsto_unique: + fixes f :: "'a \ 'b::t2_space" + assumes "\ trivial_limit F" and "(f ---> a) F" and "(f ---> b) F" + shows "a = b" +proof (rule ccontr) + assume "a \ b" + obtain U V where "open U" "open V" "a \ U" "b \ V" "U \ V = {}" + using hausdorff [OF `a \ b`] by fast + have "eventually (\x. f x \ U) F" + using `(f ---> a) F` `open U` `a \ U` by (rule topological_tendstoD) + moreover + have "eventually (\x. f x \ V) F" + using `(f ---> b) F` `open V` `b \ V` by (rule topological_tendstoD) + ultimately + have "eventually (\x. False) F" + proof (rule eventually_elim2) + fix x + assume "f x \ U" "f x \ V" + hence "f x \ U \ V" by simp + with `U \ V = {}` show "False" by simp + qed + with `\ trivial_limit F` show "False" + by (simp add: trivial_limit_def) +qed + lemma tendsto_const_iff: - fixes k l :: "'a::metric_space" - assumes "F \ bot" shows "((\n. k) ---> l) F \ 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 + fixes a b :: "'a::t2_space" + assumes "\ trivial_limit F" shows "((\x. a) ---> b) F \ a = b" + by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const]) + +subsubsection {* Distance and norms *} lemma tendsto_dist [tendsto_intros]: assumes f: "(f ---> l) F" and g: "(g ---> m) F" @@ -611,8 +633,6 @@ qed qed -subsubsection {* Norms *} - lemma norm_conv_dist: "norm x = dist x 0" unfolding dist_norm by simp @@ -865,31 +885,4 @@ shows "\(f ---> l) F; l \ 0\ \ ((\x. sgn (f x)) ---> sgn l) F" unfolding sgn_div_norm by (simp add: tendsto_intros) -subsubsection {* Uniqueness *} - -lemma tendsto_unique: - fixes f :: "'a \ 'b::t2_space" - assumes "\ trivial_limit F" "(f ---> l) F" "(f ---> l') F" - shows "l = l'" -proof (rule ccontr) - assume "l \ l'" - obtain U V where "open U" "open V" "l \ U" "l' \ V" "U \ V = {}" - using hausdorff [OF `l \ l'`] by fast - have "eventually (\x. f x \ U) F" - using `(f ---> l) F` `open U` `l \ U` by (rule topological_tendstoD) - moreover - have "eventually (\x. f x \ V) F" - using `(f ---> l') F` `open V` `l' \ V` by (rule topological_tendstoD) - ultimately - have "eventually (\x. False) F" - proof (rule eventually_elim2) - fix x - assume "f x \ U" "f x \ V" - hence "f x \ U \ V" by simp - with `U \ V = {}` show "False" by simp - qed - with `\ trivial_limit F` show "False" - by (simp add: trivial_limit_def) -qed - end diff -r f5363511b212 -r 18da2a87421c src/HOL/SEQ.thy --- a/src/HOL/SEQ.thy Sun Aug 14 08:45:38 2011 -0700 +++ b/src/HOL/SEQ.thy Sun Aug 14 10:25:43 2011 -0700 @@ -189,7 +189,7 @@ "X ----> L \ (X ---> L) sequentially" definition - lim :: "(nat \ 'a::metric_space) \ 'a" where + lim :: "(nat \ 'a::t2_space) \ 'a" where --{*Standard definition of limit using choice operator*} "lim X = (THE L. X ----> L)" @@ -301,9 +301,9 @@ by (rule tendsto_const) lemma LIMSEQ_const_iff: - fixes k l :: "'a::metric_space" + fixes k l :: "'a::t2_space" shows "(\n. k) ----> l \ k = l" -by (rule tendsto_const_iff, rule sequentially_bot) + using trivial_limit_sequentially by (rule tendsto_const_iff) lemma LIMSEQ_norm: fixes a :: "'a::real_normed_vector" @@ -366,9 +366,9 @@ by (rule tendsto_diff) lemma LIMSEQ_unique: - fixes a b :: "'a::metric_space" + fixes a b :: "'a::t2_space" shows "\X ----> a; X ----> b\ \ a = b" -by (drule (1) tendsto_dist, simp add: LIMSEQ_const_iff) + using trivial_limit_sequentially by (rule tendsto_unique) lemma (in bounded_linear) LIMSEQ: "X ----> a \ (\n. f (X n)) ----> f a"