generalize types of LIMSEQ and LIM; generalize many lemmas
authorhuffman
Tue May 04 13:08:56 2010 -0700 (2010-05-04)
changeset 36662621122eeb138
parent 36661 0a5b7b818d65
child 36663 f75b13ed4898
generalize types of LIMSEQ and LIM; generalize many lemmas
src/HOL/Lim.thy
src/HOL/Limits.thy
src/HOL/SEQ.thy
     1.1 --- a/src/HOL/Lim.thy	Tue May 04 10:42:47 2010 -0700
     1.2 +++ b/src/HOL/Lim.thy	Tue May 04 13:08:56 2010 -0700
     1.3 @@ -13,12 +13,12 @@
     1.4  text{*Standard Definitions*}
     1.5  
     1.6  abbreviation
     1.7 -  LIM :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a, 'b] \<Rightarrow> bool"
     1.8 +  LIM :: "['a::topological_space \<Rightarrow> 'b::topological_space, 'a, 'b] \<Rightarrow> bool"
     1.9          ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
    1.10    "f -- a --> L \<equiv> (f ---> L) (at a)"
    1.11  
    1.12  definition
    1.13 -  isCont :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a] \<Rightarrow> bool" where
    1.14 +  isCont :: "['a::topological_space \<Rightarrow> 'b::topological_space, 'a] \<Rightarrow> bool" where
    1.15    "isCont f a = (f -- a --> (f a))"
    1.16  
    1.17  definition
    1.18 @@ -61,23 +61,23 @@
    1.19  by (simp add: LIM_eq)
    1.20  
    1.21  lemma LIM_offset:
    1.22 -  fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space"
    1.23 +  fixes a :: "'a::real_normed_vector"
    1.24    shows "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
    1.25 -unfolding LIM_def dist_norm
    1.26 -apply clarify
    1.27 -apply (drule_tac x="r" in spec, safe)
    1.28 -apply (rule_tac x="s" in exI, safe)
    1.29 +apply (rule topological_tendstoI)
    1.30 +apply (drule (2) topological_tendstoD)
    1.31 +apply (simp only: eventually_at dist_norm)
    1.32 +apply (clarify, rule_tac x=d in exI, safe)
    1.33  apply (drule_tac x="x + k" in spec)
    1.34  apply (simp add: algebra_simps)
    1.35  done
    1.36  
    1.37  lemma LIM_offset_zero:
    1.38 -  fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space"
    1.39 +  fixes a :: "'a::real_normed_vector"
    1.40    shows "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
    1.41  by (drule_tac k="a" in LIM_offset, simp add: add_commute)
    1.42  
    1.43  lemma LIM_offset_zero_cancel:
    1.44 -  fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space"
    1.45 +  fixes a :: "'a::real_normed_vector"
    1.46    shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
    1.47  by (drule_tac k="- a" in LIM_offset, simp)
    1.48  
    1.49 @@ -87,60 +87,61 @@
    1.50  lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp
    1.51  
    1.52  lemma LIM_add:
    1.53 -  fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    1.54 +  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.55    assumes f: "f -- a --> L" and g: "g -- a --> M"
    1.56    shows "(\<lambda>x. f x + g x) -- a --> (L + M)"
    1.57  using assms by (rule tendsto_add)
    1.58  
    1.59  lemma LIM_add_zero:
    1.60 -  fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    1.61 +  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.62    shows "\<lbrakk>f -- a --> 0; g -- a --> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. f x + g x) -- a --> 0"
    1.63  by (drule (1) LIM_add, simp)
    1.64  
    1.65  lemma LIM_minus:
    1.66 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    1.67 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.68    shows "f -- a --> L \<Longrightarrow> (\<lambda>x. - f x) -- a --> - L"
    1.69  by (rule tendsto_minus)
    1.70  
    1.71  (* TODO: delete *)
    1.72  lemma LIM_add_minus:
    1.73 -  fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    1.74 +  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.75    shows "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"
    1.76  by (intro LIM_add LIM_minus)
    1.77  
    1.78  lemma LIM_diff:
    1.79 -  fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    1.80 +  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.81    shows "\<lbrakk>f -- x --> l; g -- x --> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --> l - m"
    1.82  by (rule tendsto_diff)
    1.83  
    1.84  lemma LIM_zero:
    1.85 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    1.86 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.87    shows "f -- a --> l \<Longrightarrow> (\<lambda>x. f x - l) -- a --> 0"
    1.88 -by (simp add: LIM_def dist_norm)
    1.89 +unfolding tendsto_iff dist_norm by simp
    1.90  
    1.91  lemma LIM_zero_cancel:
    1.92 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    1.93 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.94    shows "(\<lambda>x. f x - l) -- a --> 0 \<Longrightarrow> f -- a --> l"
    1.95 -by (simp add: LIM_def dist_norm)
    1.96 +unfolding tendsto_iff dist_norm by simp
    1.97  
    1.98  lemma LIM_zero_iff:
    1.99    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   1.100    shows "(\<lambda>x. f x - l) -- a --> 0 = f -- a --> l"
   1.101 -by (simp add: LIM_def dist_norm)
   1.102 +unfolding tendsto_iff dist_norm by simp
   1.103  
   1.104  lemma metric_LIM_imp_LIM:
   1.105    assumes f: "f -- a --> l"
   1.106    assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l"
   1.107    shows "g -- a --> m"
   1.108 -apply (rule metric_LIM_I, drule metric_LIM_D [OF f], safe)
   1.109 -apply (rule_tac x="s" in exI, safe)
   1.110 -apply (drule_tac x="x" in spec, safe)
   1.111 +apply (rule tendstoI, drule tendstoD [OF f])
   1.112 +apply (simp add: eventually_at_topological, safe)
   1.113 +apply (rule_tac x="S" in exI, safe)
   1.114 +apply (drule_tac x="x" in bspec, safe)
   1.115  apply (erule (1) order_le_less_trans [OF le])
   1.116  done
   1.117  
   1.118  lemma LIM_imp_LIM:
   1.119 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   1.120 -  fixes g :: "'a::metric_space \<Rightarrow> 'c::real_normed_vector"
   1.121 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   1.122 +  fixes g :: "'a::topological_space \<Rightarrow> 'c::real_normed_vector"
   1.123    assumes f: "f -- a --> l"
   1.124    assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
   1.125    shows "g -- a --> m"
   1.126 @@ -149,24 +150,24 @@
   1.127  done
   1.128  
   1.129  lemma LIM_norm:
   1.130 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   1.131 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   1.132    shows "f -- a --> l \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> norm l"
   1.133  by (rule tendsto_norm)
   1.134  
   1.135  lemma LIM_norm_zero:
   1.136 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   1.137 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   1.138    shows "f -- a --> 0 \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> 0"
   1.139 -by (drule LIM_norm, simp)
   1.140 +by (rule tendsto_norm_zero)
   1.141  
   1.142  lemma LIM_norm_zero_cancel:
   1.143 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   1.144 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   1.145    shows "(\<lambda>x. norm (f x)) -- a --> 0 \<Longrightarrow> f -- a --> 0"
   1.146 -by (erule LIM_imp_LIM, simp)
   1.147 +by (rule tendsto_norm_zero_cancel)
   1.148  
   1.149  lemma LIM_norm_zero_iff:
   1.150 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   1.151 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   1.152    shows "(\<lambda>x. norm (f x)) -- a --> 0 = f -- a --> 0"
   1.153 -by (rule iffI [OF LIM_norm_zero_cancel LIM_norm_zero])
   1.154 +by (rule tendsto_norm_zero_iff)
   1.155  
   1.156  lemma LIM_rabs: "f -- a --> (l::real) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) -- a --> \<bar>l\<bar>"
   1.157  by (fold real_norm_def, rule LIM_norm)
   1.158 @@ -180,40 +181,32 @@
   1.159  lemma LIM_rabs_zero_iff: "(\<lambda>x. \<bar>f x\<bar>) -- a --> (0::real) = f -- a --> 0"
   1.160  by (fold real_norm_def, rule LIM_norm_zero_iff)
   1.161  
   1.162 +lemma at_neq_bot:
   1.163 +  fixes a :: "'a::real_normed_algebra_1"
   1.164 +  shows "at a \<noteq> bot"  -- {* TODO: find a more appropriate class *}
   1.165 +unfolding eventually_False [symmetric]
   1.166 +unfolding eventually_at dist_norm
   1.167 +by (clarsimp, rule_tac x="a + of_real (d/2)" in exI, simp)
   1.168 +
   1.169  lemma LIM_const_not_eq:
   1.170    fixes a :: "'a::real_normed_algebra_1"
   1.171 +  fixes k L :: "'b::metric_space"
   1.172    shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"
   1.173 -apply (simp add: LIM_def)
   1.174 -apply (rule_tac x="dist k L" in exI, simp add: zero_less_dist_iff, safe)
   1.175 -apply (rule_tac x="a + of_real (s/2)" in exI, simp add: dist_norm)
   1.176 -done
   1.177 +by (simp add: tendsto_const_iff at_neq_bot)
   1.178  
   1.179  lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]
   1.180  
   1.181  lemma LIM_const_eq:
   1.182    fixes a :: "'a::real_normed_algebra_1"
   1.183 +  fixes k L :: "'b::metric_space"
   1.184    shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"
   1.185 -apply (rule ccontr)
   1.186 -apply (blast dest: LIM_const_not_eq)
   1.187 -done
   1.188 +by (simp add: tendsto_const_iff at_neq_bot)
   1.189  
   1.190  lemma LIM_unique:
   1.191    fixes a :: "'a::real_normed_algebra_1" -- {* TODO: find a more appropriate class *}
   1.192 +  fixes L M :: "'b::metric_space"
   1.193    shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M"
   1.194 -apply (rule ccontr)
   1.195 -apply (drule_tac r="dist L M / 2" in metric_LIM_D, simp add: zero_less_dist_iff)
   1.196 -apply (drule_tac r="dist L M / 2" in metric_LIM_D, simp add: zero_less_dist_iff)
   1.197 -apply (clarify, rename_tac r s)
   1.198 -apply (subgoal_tac "min r s \<noteq> 0")
   1.199 -apply (subgoal_tac "dist L M < dist L M / 2 + dist L M / 2", simp)
   1.200 -apply (subgoal_tac "dist L M \<le> dist (f (a + of_real (min r s / 2))) L +
   1.201 -                               dist (f (a + of_real (min r s / 2))) M")
   1.202 -apply (erule le_less_trans, rule add_strict_mono)
   1.203 -apply (drule spec, erule mp, simp add: dist_norm)
   1.204 -apply (drule spec, erule mp, simp add: dist_norm)
   1.205 -apply (subst dist_commute, rule dist_triangle)
   1.206 -apply simp
   1.207 -done
   1.208 +by (drule (1) tendsto_dist, simp add: tendsto_const_iff at_neq_bot)
   1.209  
   1.210  lemma LIM_ident [simp]: "(\<lambda>x. x) -- a --> a"
   1.211  by (rule tendsto_ident_at)
   1.212 @@ -221,37 +214,33 @@
   1.213  text{*Limits are equal for functions equal except at limit point*}
   1.214  lemma LIM_equal:
   1.215       "[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --> l) = (g -- a --> l)"
   1.216 -by (simp add: LIM_def)
   1.217 +unfolding tendsto_def eventually_at_topological by simp
   1.218  
   1.219  lemma LIM_cong:
   1.220    "\<lbrakk>a = b; \<And>x. x \<noteq> b \<Longrightarrow> f x = g x; l = m\<rbrakk>
   1.221     \<Longrightarrow> ((\<lambda>x. f x) -- a --> l) = ((\<lambda>x. g x) -- b --> m)"
   1.222 -by (simp add: LIM_def)
   1.223 +by (simp add: LIM_equal)
   1.224  
   1.225  lemma metric_LIM_equal2:
   1.226    assumes 1: "0 < R"
   1.227    assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < R\<rbrakk> \<Longrightarrow> f x = g x"
   1.228    shows "g -- a --> l \<Longrightarrow> f -- a --> l"
   1.229 -apply (unfold LIM_def, safe)
   1.230 -apply (drule_tac x="r" in spec, safe)
   1.231 -apply (rule_tac x="min s R" in exI, safe)
   1.232 +apply (rule topological_tendstoI)
   1.233 +apply (drule (2) topological_tendstoD)
   1.234 +apply (simp add: eventually_at, safe)
   1.235 +apply (rule_tac x="min d R" in exI, safe)
   1.236  apply (simp add: 1)
   1.237  apply (simp add: 2)
   1.238  done
   1.239  
   1.240  lemma LIM_equal2:
   1.241 -  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::metric_space"
   1.242 +  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
   1.243    assumes 1: "0 < R"
   1.244    assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x"
   1.245    shows "g -- a --> l \<Longrightarrow> f -- a --> l"
   1.246 -apply (unfold LIM_def dist_norm, safe)
   1.247 -apply (drule_tac x="r" in spec, safe)
   1.248 -apply (rule_tac x="min s R" in exI, safe)
   1.249 -apply (simp add: 1)
   1.250 -apply (simp add: 2)
   1.251 -done
   1.252 +by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm)
   1.253  
   1.254 -text{*Two uses in Transcendental.ML*}
   1.255 +text{*Two uses in Transcendental.ML*} (* BH: no longer true; delete? *)
   1.256  lemma LIM_trans:
   1.257    fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   1.258    shows "[| (%x. f(x) + -g(x)) -- a --> 0;  g -- a --> l |] ==> f -- a --> l"
   1.259 @@ -263,24 +252,52 @@
   1.260    assumes g: "g -- l --> g l"
   1.261    assumes f: "f -- a --> l"
   1.262    shows "(\<lambda>x. g (f x)) -- a --> g l"
   1.263 -proof (rule metric_LIM_I)
   1.264 -  fix r::real assume r: "0 < r"
   1.265 -  obtain s where s: "0 < s"
   1.266 -    and less_r: "\<And>y. \<lbrakk>y \<noteq> l; dist y l < s\<rbrakk> \<Longrightarrow> dist (g y) (g l) < r"
   1.267 -    using metric_LIM_D [OF g r] by fast
   1.268 -  obtain t where t: "0 < t"
   1.269 -    and less_s: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < t\<rbrakk> \<Longrightarrow> dist (f x) l < s"
   1.270 -    using metric_LIM_D [OF f s] by fast
   1.271 +proof (rule topological_tendstoI)
   1.272 +  fix C assume C: "open C" "g l \<in> C"
   1.273 +  obtain B where B: "open B" "l \<in> B"
   1.274 +    and gC: "\<And>y. y \<in> B \<Longrightarrow> y \<noteq> l \<Longrightarrow> g y \<in> C"
   1.275 +    using topological_tendstoD [OF g C]
   1.276 +    unfolding eventually_at_topological by fast
   1.277 +  obtain A where A: "open A" "a \<in> A"
   1.278 +    and fB: "\<And>x. x \<in> A \<Longrightarrow> x \<noteq> a \<Longrightarrow> f x \<in> B"
   1.279 +    using topological_tendstoD [OF f B]
   1.280 +    unfolding eventually_at_topological by fast
   1.281 +  show "eventually (\<lambda>x. g (f x) \<in> C) (at a)"
   1.282 +  unfolding eventually_at_topological
   1.283 +  proof (intro exI conjI ballI impI)
   1.284 +    show "open A" and "a \<in> A" using A .
   1.285 +  next
   1.286 +    fix x assume "x \<in> A" and "x \<noteq> a"
   1.287 +    then show "g (f x) \<in> C"
   1.288 +      by (cases "f x = l", simp add: C, simp add: gC fB)
   1.289 +  qed
   1.290 +qed
   1.291  
   1.292 -  show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> dist x a < t \<longrightarrow> dist (g (f x)) (g l) < r"
   1.293 -  proof (rule exI, safe)
   1.294 -    show "0 < t" using t .
   1.295 +lemma LIM_compose_eventually:
   1.296 +  assumes f: "f -- a --> b"
   1.297 +  assumes g: "g -- b --> c"
   1.298 +  assumes inj: "eventually (\<lambda>x. f x \<noteq> b) (at a)"
   1.299 +  shows "(\<lambda>x. g (f x)) -- a --> c"
   1.300 +proof (rule topological_tendstoI)
   1.301 +  fix C assume C: "open C" "c \<in> C"
   1.302 +  obtain B where B: "open B" "b \<in> B"
   1.303 +    and gC: "\<And>y. y \<in> B \<Longrightarrow> y \<noteq> b \<Longrightarrow> g y \<in> C"
   1.304 +    using topological_tendstoD [OF g C]
   1.305 +    unfolding eventually_at_topological by fast
   1.306 +  obtain A where A: "open A" "a \<in> A"
   1.307 +    and fB: "\<And>x. x \<in> A \<Longrightarrow> x \<noteq> a \<Longrightarrow> f x \<in> B"
   1.308 +    using topological_tendstoD [OF f B]
   1.309 +    unfolding eventually_at_topological by fast
   1.310 +  have "eventually (\<lambda>x. f x \<noteq> b \<longrightarrow> g (f x) \<in> C) (at a)"
   1.311 +  unfolding eventually_at_topological
   1.312 +  proof (intro exI conjI ballI impI)
   1.313 +    show "open A" and "a \<in> A" using A .
   1.314    next
   1.315 -    fix x assume "x \<noteq> a" and "dist x a < t"
   1.316 -    hence "dist (f x) l < s" by (rule less_s)
   1.317 -    thus "dist (g (f x)) (g l) < r"
   1.318 -      using r less_r by (case_tac "f x = l", simp_all)
   1.319 +    fix x assume "x \<in> A" and "x \<noteq> a" and "f x \<noteq> b"
   1.320 +    then show "g (f x) \<in> C" by (simp add: gC fB)
   1.321    qed
   1.322 +  with inj show "eventually (\<lambda>x. g (f x) \<in> C) (at a)"
   1.323 +    by (rule eventually_rev_mp)
   1.324  qed
   1.325  
   1.326  lemma metric_LIM_compose2:
   1.327 @@ -288,31 +305,8 @@
   1.328    assumes g: "g -- b --> c"
   1.329    assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b"
   1.330    shows "(\<lambda>x. g (f x)) -- a --> c"
   1.331 -proof (rule metric_LIM_I)
   1.332 -  fix r :: real
   1.333 -  assume r: "0 < r"
   1.334 -  obtain s where s: "0 < s"
   1.335 -    and less_r: "\<And>y. \<lbrakk>y \<noteq> b; dist y b < s\<rbrakk> \<Longrightarrow> dist (g y) c < r"
   1.336 -    using metric_LIM_D [OF g r] by fast
   1.337 -  obtain t where t: "0 < t"
   1.338 -    and less_s: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < t\<rbrakk> \<Longrightarrow> dist (f x) b < s"
   1.339 -    using metric_LIM_D [OF f s] by fast
   1.340 -  obtain d where d: "0 < d"
   1.341 -    and neq_b: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < d\<rbrakk> \<Longrightarrow> f x \<noteq> b"
   1.342 -    using inj by fast
   1.343 -
   1.344 -  show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> dist x a < t \<longrightarrow> dist (g (f x)) c < r"
   1.345 -  proof (safe intro!: exI)
   1.346 -    show "0 < min d t" using d t by simp
   1.347 -  next
   1.348 -    fix x
   1.349 -    assume "x \<noteq> a" and "dist x a < min d t"
   1.350 -    hence "f x \<noteq> b" and "dist (f x) b < s"
   1.351 -      using neq_b less_s by simp_all
   1.352 -    thus "dist (g (f x)) c < r"
   1.353 -      by (rule less_r)
   1.354 -  qed
   1.355 -qed
   1.356 +using f g inj [folded eventually_at]
   1.357 +by (rule LIM_compose_eventually)
   1.358  
   1.359  lemma LIM_compose2:
   1.360    fixes a :: "'a::real_normed_vector"
   1.361 @@ -326,7 +320,7 @@
   1.362  unfolding o_def by (rule LIM_compose)
   1.363  
   1.364  lemma real_LIM_sandwich_zero:
   1.365 -  fixes f g :: "'a::metric_space \<Rightarrow> real"
   1.366 +  fixes f g :: "'a::topological_space \<Rightarrow> real"
   1.367    assumes f: "f -- a --> 0"
   1.368    assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x"
   1.369    assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x"
   1.370 @@ -593,7 +587,7 @@
   1.371  subsection {* Relation of LIM and LIMSEQ *}
   1.372  
   1.373  lemma LIMSEQ_SEQ_conv1:
   1.374 -  fixes a :: "'a::metric_space"
   1.375 +  fixes a :: "'a::metric_space" and L :: "'b::metric_space"
   1.376    assumes X: "X -- a --> L"
   1.377    shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
   1.378  proof (safe intro!: metric_LIMSEQ_I)
   1.379 @@ -614,7 +608,7 @@
   1.380  
   1.381  
   1.382  lemma LIMSEQ_SEQ_conv2:
   1.383 -  fixes a :: real
   1.384 +  fixes a :: real and L :: "'a::metric_space"
   1.385    assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
   1.386    shows "X -- a --> L"
   1.387  proof (rule ccontr)
   1.388 @@ -682,7 +676,7 @@
   1.389  
   1.390  lemma LIMSEQ_SEQ_conv:
   1.391    "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::real) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
   1.392 -   (X -- a --> L)"
   1.393 +   (X -- a --> (L::'a::metric_space))"
   1.394  proof
   1.395    assume "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
   1.396    thus "X -- a --> L" by (rule LIMSEQ_SEQ_conv2)
     2.1 --- a/src/HOL/Limits.thy	Tue May 04 10:42:47 2010 -0700
     2.2 +++ b/src/HOL/Limits.thy	Tue May 04 13:08:56 2010 -0700
     2.3 @@ -269,13 +269,39 @@
     2.4  by (simp add: expand_net_eq eventually_netmap)
     2.5  
     2.6  
     2.7 -subsection {* Standard Nets *}
     2.8 +subsection {* Sequentially *}
     2.9  
    2.10  definition
    2.11    sequentially :: "nat net"
    2.12  where [code del]:
    2.13    "sequentially = Abs_net (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
    2.14  
    2.15 +lemma eventually_sequentially:
    2.16 +  "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
    2.17 +unfolding sequentially_def
    2.18 +proof (rule eventually_Abs_net, rule is_filter.intro)
    2.19 +  fix P Q :: "nat \<Rightarrow> bool"
    2.20 +  assume "\<exists>i. \<forall>n\<ge>i. P n" and "\<exists>j. \<forall>n\<ge>j. Q n"
    2.21 +  then obtain i j where "\<forall>n\<ge>i. P n" and "\<forall>n\<ge>j. Q n" by auto
    2.22 +  then have "\<forall>n\<ge>max i j. P n \<and> Q n" by simp
    2.23 +  then show "\<exists>k. \<forall>n\<ge>k. P n \<and> Q n" ..
    2.24 +qed auto
    2.25 +
    2.26 +lemma sequentially_bot [simp]: "sequentially \<noteq> bot"
    2.27 +unfolding expand_net_eq eventually_sequentially by auto
    2.28 +
    2.29 +lemma eventually_False_sequentially [simp]:
    2.30 +  "\<not> eventually (\<lambda>n. False) sequentially"
    2.31 +by (simp add: eventually_False)
    2.32 +
    2.33 +lemma le_sequentially:
    2.34 +  "net \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) net)"
    2.35 +unfolding le_net_def eventually_sequentially
    2.36 +by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp)
    2.37 +
    2.38 +
    2.39 +subsection {* Standard Nets *}
    2.40 +
    2.41  definition
    2.42    within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70)
    2.43  where [code del]:
    2.44 @@ -291,17 +317,6 @@
    2.45  where [code del]:
    2.46    "at a = nhds a within - {a}"
    2.47  
    2.48 -lemma eventually_sequentially:
    2.49 -  "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
    2.50 -unfolding sequentially_def
    2.51 -proof (rule eventually_Abs_net, rule is_filter.intro)
    2.52 -  fix P Q :: "nat \<Rightarrow> bool"
    2.53 -  assume "\<exists>i. \<forall>n\<ge>i. P n" and "\<exists>j. \<forall>n\<ge>j. Q n"
    2.54 -  then obtain i j where "\<forall>n\<ge>i. P n" and "\<forall>n\<ge>j. Q n" by auto
    2.55 -  then have "\<forall>n\<ge>max i j. P n \<and> Q n" by simp
    2.56 -  then show "\<exists>k. \<forall>n\<ge>k. P n \<and> Q n" ..
    2.57 -qed auto
    2.58 -
    2.59  lemma eventually_within:
    2.60    "eventually P (net within S) = eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) net"
    2.61  unfolding within_def
    2.62 @@ -598,6 +613,16 @@
    2.63  lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) net"
    2.64  by (simp add: tendsto_def)
    2.65  
    2.66 +lemma tendsto_const_iff:
    2.67 +  fixes k l :: "'a::metric_space"
    2.68 +  assumes "net \<noteq> bot" shows "((\<lambda>n. k) ---> l) net \<longleftrightarrow> k = l"
    2.69 +apply (safe intro!: tendsto_const)
    2.70 +apply (rule ccontr)
    2.71 +apply (drule_tac e="dist k l" in tendstoD)
    2.72 +apply (simp add: zero_less_dist_iff)
    2.73 +apply (simp add: eventually_False assms)
    2.74 +done
    2.75 +
    2.76  lemma tendsto_dist [tendsto_intros]:
    2.77    assumes f: "(f ---> l) net" and g: "(g ---> m) net"
    2.78    shows "((\<lambda>x. dist (f x) (g x)) ---> dist l m) net"
    2.79 @@ -618,13 +643,24 @@
    2.80    qed
    2.81  qed
    2.82  
    2.83 +lemma norm_conv_dist: "norm x = dist x 0"
    2.84 +unfolding dist_norm by simp
    2.85 +
    2.86  lemma tendsto_norm [tendsto_intros]:
    2.87    "(f ---> a) net \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> norm a) net"
    2.88 -apply (simp add: tendsto_iff dist_norm, safe)
    2.89 -apply (drule_tac x="e" in spec, safe)
    2.90 -apply (erule eventually_elim1)
    2.91 -apply (erule order_le_less_trans [OF norm_triangle_ineq3])
    2.92 -done
    2.93 +unfolding norm_conv_dist by (intro tendsto_intros)
    2.94 +
    2.95 +lemma tendsto_norm_zero:
    2.96 +  "(f ---> 0) net \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> 0) net"
    2.97 +by (drule tendsto_norm, simp)
    2.98 +
    2.99 +lemma tendsto_norm_zero_cancel:
   2.100 +  "((\<lambda>x. norm (f x)) ---> 0) net \<Longrightarrow> (f ---> 0) net"
   2.101 +unfolding tendsto_iff dist_norm by simp
   2.102 +
   2.103 +lemma tendsto_norm_zero_iff:
   2.104 +  "((\<lambda>x. norm (f x)) ---> 0) net \<longleftrightarrow> (f ---> 0) net"
   2.105 +unfolding tendsto_iff dist_norm by simp
   2.106  
   2.107  lemma add_diff_add:
   2.108    fixes a b c d :: "'a::ab_group_add"
     3.1 --- a/src/HOL/SEQ.thy	Tue May 04 10:42:47 2010 -0700
     3.2 +++ b/src/HOL/SEQ.thy	Tue May 04 13:08:56 2010 -0700
     3.3 @@ -14,7 +14,7 @@
     3.4  begin
     3.5  
     3.6  abbreviation
     3.7 -  LIMSEQ :: "[nat \<Rightarrow> 'a::metric_space, 'a] \<Rightarrow> bool"
     3.8 +  LIMSEQ :: "[nat \<Rightarrow> 'a::topological_space, 'a] \<Rightarrow> bool"
     3.9      ("((_)/ ----> (_))" [60, 60] 60) where
    3.10    "X ----> L \<equiv> (X ---> L) sequentially"
    3.11  
    3.12 @@ -153,13 +153,10 @@
    3.13  lemma LIMSEQ_const: "(\<lambda>n. k) ----> k"
    3.14  by (rule tendsto_const)
    3.15  
    3.16 -lemma LIMSEQ_const_iff: "(\<lambda>n. k) ----> l \<longleftrightarrow> k = l"
    3.17 -apply (safe intro!: LIMSEQ_const)
    3.18 -apply (rule ccontr)
    3.19 -apply (drule_tac r="dist k l" in metric_LIMSEQ_D)
    3.20 -apply (simp add: zero_less_dist_iff)
    3.21 -apply auto
    3.22 -done
    3.23 +lemma LIMSEQ_const_iff:
    3.24 +  fixes k l :: "'a::metric_space"
    3.25 +  shows "(\<lambda>n. k) ----> l \<longleftrightarrow> k = l"
    3.26 +by (rule tendsto_const_iff, rule sequentially_bot)
    3.27  
    3.28  lemma LIMSEQ_norm:
    3.29    fixes a :: "'a::real_normed_vector"
    3.30 @@ -168,8 +165,9 @@
    3.31  
    3.32  lemma LIMSEQ_ignore_initial_segment:
    3.33    "f ----> a \<Longrightarrow> (\<lambda>n. f (n + k)) ----> a"
    3.34 -apply (rule metric_LIMSEQ_I)
    3.35 -apply (drule (1) metric_LIMSEQ_D)
    3.36 +apply (rule topological_tendstoI)
    3.37 +apply (drule (2) topological_tendstoD)
    3.38 +apply (simp only: eventually_sequentially)
    3.39  apply (erule exE, rename_tac N)
    3.40  apply (rule_tac x=N in exI)
    3.41  apply simp
    3.42 @@ -177,8 +175,9 @@
    3.43  
    3.44  lemma LIMSEQ_offset:
    3.45    "(\<lambda>n. f (n + k)) ----> a \<Longrightarrow> f ----> a"
    3.46 -apply (rule metric_LIMSEQ_I)
    3.47 -apply (drule (1) metric_LIMSEQ_D)
    3.48 +apply (rule topological_tendstoI)
    3.49 +apply (drule (2) topological_tendstoD)
    3.50 +apply (simp only: eventually_sequentially)
    3.51  apply (erule exE, rename_tac N)
    3.52  apply (rule_tac x="N + k" in exI)
    3.53  apply clarify
    3.54 @@ -196,7 +195,7 @@
    3.55  by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
    3.56  
    3.57  lemma LIMSEQ_linear: "\<lbrakk> X ----> x ; l > 0 \<rbrakk> \<Longrightarrow> (\<lambda> n. X (n * l)) ----> x"
    3.58 -  unfolding LIMSEQ_def
    3.59 +  unfolding tendsto_def eventually_sequentially
    3.60    by (metis div_le_dividend div_mult_self1_is_m le_trans nat_mult_commute)
    3.61  
    3.62  lemma LIMSEQ_add:
    3.63 @@ -219,7 +218,9 @@
    3.64    shows "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n - Y n) ----> a - b"
    3.65  by (rule tendsto_diff)
    3.66  
    3.67 -lemma LIMSEQ_unique: "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b"
    3.68 +lemma LIMSEQ_unique:
    3.69 +  fixes a b :: "'a::metric_space"
    3.70 +  shows "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b"
    3.71  apply (rule ccontr)
    3.72  apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff)
    3.73  apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff)
    3.74 @@ -750,9 +751,10 @@
    3.75  
    3.76  lemma LIMSEQ_subseq_LIMSEQ:
    3.77    "\<lbrakk> X ----> L; subseq f \<rbrakk> \<Longrightarrow> (X o f) ----> L"
    3.78 -apply (auto simp add: LIMSEQ_def) 
    3.79 -apply (drule_tac x=r in spec, clarify)  
    3.80 -apply (rule_tac x=no in exI, clarify) 
    3.81 +apply (rule topological_tendstoI)
    3.82 +apply (drule (2) topological_tendstoD)
    3.83 +apply (simp only: eventually_sequentially)
    3.84 +apply (clarify, rule_tac x=N in exI, clarsimp)
    3.85  apply (blast intro: seq_suble le_trans dest!: spec) 
    3.86  done
    3.87  
    3.88 @@ -836,12 +838,8 @@
    3.89  apply (blast dest: order_antisym)+
    3.90  done
    3.91  
    3.92 -text{* The best of both worlds: Easier to prove this result as a standard
    3.93 -   theorem and then use equivalence to "transfer" it into the
    3.94 -   equivalent nonstandard form if needed!*}
    3.95 -
    3.96  lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
    3.97 -apply (simp add: LIMSEQ_def)
    3.98 +unfolding tendsto_def eventually_sequentially
    3.99  apply (rule_tac x = "X m" in exI, safe)
   3.100  apply (rule_tac x = m in exI, safe)
   3.101  apply (drule spec, erule impE, auto)