generalize tendsto to class topological_space
authorhuffman
Sat Jun 06 09:11:12 2009 -0700 (2009-06-06)
changeset 314885691ccb8d6b5
parent 31487 93938cafc0e6
child 31489 10080e31b294
generalize tendsto to class topological_space
src/HOL/Library/Topology_Euclidean_Space.thy
src/HOL/Lim.thy
src/HOL/Limits.thy
src/HOL/SEQ.thy
     1.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Jun 05 15:59:20 2009 -0700
     1.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Sat Jun 06 09:11:12 2009 -0700
     1.3 @@ -1171,46 +1171,50 @@
     1.4  subsection{* Limits, defined as vacuously true when the limit is trivial. *}
     1.5  
     1.6    text{* Notation Lim to avoid collition with lim defined in analysis *}
     1.7 -definition "Lim net f = (THE l. (f ---> l) net)"
     1.8 +definition
     1.9 +  Lim :: "'a net \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b" where
    1.10 +  "Lim net f = (THE l. (f ---> l) net)"
    1.11  
    1.12  lemma Lim:
    1.13   "(f ---> l) net \<longleftrightarrow>
    1.14          trivial_limit net \<or>
    1.15          (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
    1.16 -  unfolding tendsto_def trivial_limit_eq by auto
    1.17 +  unfolding tendsto_iff trivial_limit_eq by auto
    1.18  
    1.19  
    1.20  text{* Show that they yield usual definitions in the various cases. *}
    1.21  
    1.22  lemma Lim_within_le: "(f ---> l)(at a within S) \<longleftrightarrow>
    1.23             (\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. 0 < dist x a  \<and> dist x a  <= d \<longrightarrow> dist (f x) l < e)"
    1.24 -  by (auto simp add: tendsto_def eventually_within_le)
    1.25 +  by (auto simp add: tendsto_iff eventually_within_le)
    1.26  
    1.27  lemma Lim_within: "(f ---> l) (at a within S) \<longleftrightarrow>
    1.28          (\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a  \<and> dist x a  < d  \<longrightarrow> dist (f x) l < e)"
    1.29 -  by (auto simp add: tendsto_def eventually_within)
    1.30 +  by (auto simp add: tendsto_iff eventually_within)
    1.31  
    1.32  lemma Lim_at: "(f ---> l) (at a) \<longleftrightarrow>
    1.33          (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a  \<and> dist x a  < d  \<longrightarrow> dist (f x) l < e)"
    1.34 -  by (auto simp add: tendsto_def eventually_at)
    1.35 +  by (auto simp add: tendsto_iff eventually_at)
    1.36  
    1.37  lemma Lim_at_iff_LIM: "(f ---> l) (at a) \<longleftrightarrow> f -- a --> l"
    1.38    unfolding Lim_at LIM_def by (simp only: zero_less_dist_iff)
    1.39  
    1.40  lemma Lim_at_infinity:
    1.41    "(f ---> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x::real^'n::finite. norm x >= b \<longrightarrow> dist (f x) l < e)"
    1.42 -  by (auto simp add: tendsto_def eventually_at_infinity)
    1.43 +  by (auto simp add: tendsto_iff eventually_at_infinity)
    1.44  
    1.45  lemma Lim_sequentially:
    1.46   "(S ---> l) sequentially \<longleftrightarrow>
    1.47            (\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (S n) l < e)"
    1.48 -  by (auto simp add: tendsto_def eventually_sequentially)
    1.49 +  by (auto simp add: tendsto_iff eventually_sequentially)
    1.50  
    1.51  lemma Lim_sequentially_iff_LIMSEQ: "(S ---> l) sequentially \<longleftrightarrow> S ----> l"
    1.52    unfolding Lim_sequentially LIMSEQ_def ..
    1.53  
    1.54 -lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
    1.55 -  unfolding tendsto_def by (auto elim: eventually_rev_mono)
    1.56 +lemma Lim_eventually:
    1.57 +  fixes l :: "'a::metric_space" (* FIXME: generalize to t2_space *)
    1.58 +  shows "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
    1.59 +  unfolding tendsto_iff by (auto elim: eventually_rev_mono)
    1.60  
    1.61  text{* The expected monotonicity property. *}
    1.62  
    1.63 @@ -1225,7 +1229,7 @@
    1.64    shows "(f ---> l) (net within (S \<union> T))"
    1.65    using assms unfolding tendsto_def Limits.eventually_within
    1.66    apply clarify
    1.67 -  apply (drule spec, drule (1) mp)+
    1.68 +  apply (drule (1) bspec)+
    1.69    apply (auto elim: eventually_elim2)
    1.70    done
    1.71  
    1.72 @@ -1238,9 +1242,11 @@
    1.73  
    1.74  lemma Lim_at_within: "(f ---> l) net ==> (f ---> l)(net within S)"
    1.75    unfolding tendsto_def Limits.eventually_within
    1.76 +  apply (clarify, drule (1) bspec)
    1.77    by (auto elim!: eventually_elim1)
    1.78  
    1.79  lemma Lim_within_open:
    1.80 +  fixes l :: "'a::metric_space" (* FIXME: generalize to topological_space *)
    1.81    assumes"a \<in> S" "open S"
    1.82    shows "(f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)" (is "?lhs \<longleftrightarrow> ?rhs")
    1.83  proof
    1.84 @@ -1268,7 +1274,9 @@
    1.85  text{* Another limit point characterization. *}
    1.86  
    1.87  lemma islimpt_sequential:
    1.88 - "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S -{x}) \<and> (f ---> x) sequentially)" (is "?lhs = ?rhs")
    1.89 +  fixes x :: "'a::metric_space" (* FIXME: generalize to topological_space *)
    1.90 +  shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S -{x}) \<and> (f ---> x) sequentially)"
    1.91 +    (is "?lhs = ?rhs")
    1.92  proof
    1.93    assume ?lhs
    1.94    then obtain f where f:"\<forall>y. y>0 \<longrightarrow> f y \<in> S \<and> f y \<noteq> x \<and> dist (f y) x < y"
    1.95 @@ -1317,11 +1325,11 @@
    1.96        apply (simp add: pos_less_divide_eq `0 < b` mult_commute)
    1.97        done
    1.98    }
    1.99 -  thus ?thesis unfolding tendsto_def by simp
   1.100 +  thus ?thesis unfolding tendsto_iff by simp
   1.101  qed
   1.102  
   1.103  lemma Lim_const: "((\<lambda>x. a) ---> a) net"
   1.104 -  by (auto simp add: Lim trivial_limit_def)
   1.105 +  unfolding tendsto_def by simp
   1.106  
   1.107  lemma Lim_cmul:
   1.108    fixes f :: "'a \<Rightarrow> real ^ 'n::finite"
   1.109 @@ -1355,7 +1363,7 @@
   1.110        apply simp
   1.111        done
   1.112    }
   1.113 -  thus ?thesis unfolding tendsto_def by simp
   1.114 +  thus ?thesis unfolding tendsto_iff by simp
   1.115  qed
   1.116  
   1.117  lemma Lim_sub:
   1.118 @@ -1377,7 +1385,7 @@
   1.119    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   1.120    assumes "eventually (\<lambda>x. norm(f x) <= g x) net" "((\<lambda>x. vec1(g x)) ---> 0) net"
   1.121    shows "(f ---> 0) net"
   1.122 -proof(simp add: tendsto_def, rule+)
   1.123 +proof(simp add: tendsto_iff, rule+)
   1.124    fix e::real assume "0<e"
   1.125    { fix x
   1.126      assume "norm (f x) \<le> g x" "dist (vec1 (g x)) 0 < e"
   1.127 @@ -1387,12 +1395,12 @@
   1.128    thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
   1.129      using eventually_and[of "\<lambda>x. norm(f x) <= g x" "\<lambda>x. dist (vec1 (g x)) 0 < e" net]
   1.130      using eventually_mono[of "(\<lambda>x. norm (f x) \<le> g x \<and> dist (vec1 (g x)) 0 < e)" "(\<lambda>x. dist (f x) 0 < e)" net]
   1.131 -    using assms `e>0` unfolding tendsto_def by auto
   1.132 +    using assms `e>0` unfolding tendsto_iff by auto
   1.133  qed
   1.134  
   1.135  lemma Lim_component: "(f ---> l) net
   1.136                        ==> ((\<lambda>a. vec1((f a :: real ^'n::finite)$i)) ---> vec1(l$i)) net"
   1.137 -  unfolding tendsto_def
   1.138 +  unfolding tendsto_iff
   1.139    apply (simp add: dist_norm vec1_sub[symmetric] norm_vec1  vector_minus_component[symmetric] del: vector_minus_component)
   1.140    apply (auto simp del: vector_minus_component)
   1.141    apply (erule_tac x=e in allE)
   1.142 @@ -1408,7 +1416,7 @@
   1.143    fixes g :: "'a \<Rightarrow> 'c::real_normed_vector"
   1.144    assumes "eventually (\<lambda>n. norm(f n) <= norm(g n)) net"  "(g ---> 0) net"
   1.145    shows "(f ---> 0) net"
   1.146 -proof(simp add: tendsto_def, rule+)
   1.147 +proof(simp add: tendsto_iff, rule+)
   1.148    fix e::real assume "e>0"
   1.149    { fix x
   1.150      assume "norm (f x) \<le> norm (g x)" "dist (g x) 0 < e"
   1.151 @@ -1416,12 +1424,13 @@
   1.152    thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
   1.153      using eventually_and[of "\<lambda>x. norm (f x) \<le> norm (g x)" "\<lambda>x. dist (g x) 0 < e" net]
   1.154      using eventually_mono[of "\<lambda>x. norm (f x) \<le> norm (g x) \<and> dist (g x) 0 < e" "\<lambda>x. dist (f x) 0 < e" net]
   1.155 -    using assms `e>0` unfolding tendsto_def by blast
   1.156 +    using assms `e>0` unfolding tendsto_iff by blast
   1.157  qed
   1.158  
   1.159  text{* Deducing things about the limit from the elements. *}
   1.160  
   1.161  lemma Lim_in_closed_set:
   1.162 +  fixes l :: "'a::metric_space" (* FIXME: generalize to topological_space *)
   1.163    assumes "closed S" "eventually (\<lambda>x. f(x) \<in> S) net"  "\<not>(trivial_limit net)" "(f ---> l) net"
   1.164    shows "l \<in> S"
   1.165  proof (rule ccontr)
   1.166 @@ -1581,17 +1590,21 @@
   1.167        by (auto elim: eventually_rev_mono)
   1.168    }
   1.169    thus "((\<lambda>x. h (f x) (g x)) ---> h l m) net"
   1.170 -    unfolding tendsto_def by simp
   1.171 +    unfolding tendsto_iff by simp
   1.172  qed
   1.173  
   1.174  text{* These are special for limits out of the same vector space. *}
   1.175  
   1.176 -lemma Lim_within_id: "(id ---> a) (at a within s)" by (auto simp add: Lim_within id_def)
   1.177 +lemma Lim_within_id: "(id ---> a) (at a within s)"
   1.178 +  unfolding tendsto_def Limits.eventually_within eventually_at_topological
   1.179 +  by auto
   1.180 +
   1.181  lemma Lim_at_id: "(id ---> a) (at a)"
   1.182  apply (subst within_UNIV[symmetric]) by (simp add: Lim_within_id)
   1.183  
   1.184  lemma Lim_at_zero:
   1.185    fixes a :: "'a::real_normed_vector"
   1.186 +  fixes l :: "'b::metric_space" (* FIXME: generalize to topological_space *)
   1.187    shows "(f ---> l) (at a) \<longleftrightarrow> ((\<lambda>x. f(a + x)) ---> l) (at 0)" (is "?lhs = ?rhs")
   1.188  proof
   1.189    assume "?lhs"
   1.190 @@ -1671,13 +1684,15 @@
   1.191  qed
   1.192  
   1.193  lemma Lim_transform_eventually:
   1.194 +  fixes l :: "'a::metric_space" (* FIXME: generalize to t2_space *)
   1.195    shows "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net ==> (g ---> l) net"
   1.196 -  unfolding tendsto_def
   1.197 +  unfolding tendsto_iff
   1.198    apply (clarify, drule spec, drule (1) mp)
   1.199    apply (erule (1) eventually_elim2, simp)
   1.200    done
   1.201  
   1.202  lemma Lim_transform_within:
   1.203 +  fixes l :: "'b::metric_space" (* TODO: generalize *)
   1.204    assumes "0 < d" "(\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x')"
   1.205            "(f ---> l) (at x within S)"
   1.206    shows   "(g ---> l) (at x within S)"
   1.207 @@ -1691,6 +1706,7 @@
   1.208    done
   1.209  
   1.210  lemma Lim_transform_at:
   1.211 +  fixes l :: "'b::metric_space" (* TODO: generalize *)
   1.212    shows "0 < d \<Longrightarrow> (\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x') \<Longrightarrow>
   1.213    (f ---> l) (at x) ==> (g ---> l) (at x)"
   1.214    apply (subst within_UNIV[symmetric])
   1.215 @@ -1701,6 +1717,7 @@
   1.216  
   1.217  lemma Lim_transform_away_within:
   1.218    fixes a b :: "'a::metric_space"
   1.219 +  fixes l :: "'b::metric_space" (* TODO: generalize *)
   1.220    assumes "a\<noteq>b" "\<forall>x\<in> S. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
   1.221    and "(f ---> l) (at a within S)"
   1.222    shows "(g ---> l) (at a within S)"
   1.223 @@ -1712,6 +1729,7 @@
   1.224  
   1.225  lemma Lim_transform_away_at:
   1.226    fixes a b :: "'a::metric_space"
   1.227 +  fixes l :: "'b::metric_space" (* TODO: generalize *)
   1.228    assumes ab: "a\<noteq>b" and fg: "\<forall>x. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
   1.229    and fl: "(f ---> l) (at a)"
   1.230    shows "(g ---> l) (at a)"
   1.231 @@ -1722,6 +1740,7 @@
   1.232  
   1.233  lemma Lim_transform_within_open:
   1.234    fixes a :: "'a::metric_space"
   1.235 +  fixes l :: "'b::metric_space" (* TODO: generalize *)
   1.236    assumes "open S"  "a \<in> S"  "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x"  "(f ---> l) (at a)"
   1.237    shows "(g ---> l) (at a)"
   1.238  proof-
   1.239 @@ -1736,19 +1755,22 @@
   1.240  (* FIXME: Only one congruence rule for tendsto can be used at a time! *)
   1.241  
   1.242  lemma Lim_cong_within[cong add]:
   1.243 -  fixes a :: "'a::metric_space" shows
   1.244 - "(\<And>x. x \<noteq> a \<Longrightarrow> f x = g x) ==> ((\<lambda>x. f x) ---> l) (at a within S) \<longleftrightarrow> ((g ---> l) (at a within S))"
   1.245 +  fixes a :: "'a::metric_space"
   1.246 +  fixes l :: "'b::metric_space" (* TODO: generalize *)
   1.247 +  shows "(\<And>x. x \<noteq> a \<Longrightarrow> f x = g x) ==> ((\<lambda>x. f x) ---> l) (at a within S) \<longleftrightarrow> ((g ---> l) (at a within S))"
   1.248    by (simp add: Lim_within dist_nz[symmetric])
   1.249  
   1.250  lemma Lim_cong_at[cong add]:
   1.251 -  fixes a :: "'a::metric_space" shows
   1.252 - "(\<And>x. x \<noteq> a ==> f x = g x) ==> (((\<lambda>x. f x) ---> l) (at a) \<longleftrightarrow> ((g ---> l) (at a)))"
   1.253 +  fixes a :: "'a::metric_space"
   1.254 +  fixes l :: "'b::metric_space" (* TODO: generalize *)
   1.255 +  shows "(\<And>x. x \<noteq> a ==> f x = g x) ==> (((\<lambda>x. f x) ---> l) (at a) \<longleftrightarrow> ((g ---> l) (at a)))"
   1.256    by (simp add: Lim_at dist_nz[symmetric])
   1.257  
   1.258  text{* Useful lemmas on closure and set of possible sequential limits.*}
   1.259  
   1.260  lemma closure_sequential:
   1.261 - "l \<in> closure S \<longleftrightarrow> (\<exists>x. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially)" (is "?lhs = ?rhs")
   1.262 +  fixes l :: "'a::metric_space" (* TODO: generalize *)
   1.263 +  shows "l \<in> closure S \<longleftrightarrow> (\<exists>x. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially)" (is "?lhs = ?rhs")
   1.264  proof
   1.265    assume "?lhs" moreover
   1.266    { assume "l \<in> S"
   1.267 @@ -1783,17 +1805,23 @@
   1.268  
   1.269  text{* Some other lemmas about sequences. *}
   1.270  
   1.271 -lemma seq_offset: "(f ---> l) sequentially ==> ((\<lambda>i. f( i + k)) ---> l) sequentially"
   1.272 +lemma seq_offset:
   1.273 +  fixes l :: "'a::metric_space" (* TODO: generalize *)
   1.274 +  shows "(f ---> l) sequentially ==> ((\<lambda>i. f( i + k)) ---> l) sequentially"
   1.275    apply (auto simp add: Lim_sequentially)
   1.276    by (metis trans_le_add1 )
   1.277  
   1.278 -lemma seq_offset_neg: "(f ---> l) sequentially ==> ((\<lambda>i. f(i - k)) ---> l) sequentially"
   1.279 +lemma seq_offset_neg:
   1.280 +  fixes l :: "'a::metric_space" (* TODO: generalize *)
   1.281 +  shows "(f ---> l) sequentially ==> ((\<lambda>i. f(i - k)) ---> l) sequentially"
   1.282    apply (simp add: Lim_sequentially)
   1.283    apply (subgoal_tac "\<And>N k (n::nat). N + k <= n ==> N <= n - k")
   1.284    apply metis
   1.285    by arith
   1.286  
   1.287 -lemma seq_offset_rev: "((\<lambda>i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially"
   1.288 +lemma seq_offset_rev:
   1.289 +  fixes l :: "'a::metric_space" (* TODO: generalize *)
   1.290 +  shows "((\<lambda>i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially"
   1.291    apply (simp add: Lim_sequentially)
   1.292    apply (subgoal_tac "\<And>N k (n::nat). N + k <= n ==> N <= n - k \<and> (n - k) + k = n")
   1.293    by metis arith
   1.294 @@ -2017,8 +2045,9 @@
   1.295  
   1.296  lemma lim_within_interior:
   1.297    fixes x :: "'a::metric_space"
   1.298 +  fixes l :: "'b::metric_space" (* TODO: generalize *)
   1.299    shows "x \<in> interior S  ==> ((f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x))"
   1.300 -  by (simp add: tendsto_def eventually_within_interior)
   1.301 +  by (simp add: tendsto_iff eventually_within_interior)
   1.302  
   1.303  lemma netlimit_within_interior:
   1.304    fixes x :: "'a::{perfect_space, real_normed_vector}"
   1.305 @@ -2241,7 +2270,9 @@
   1.306  
   1.307  subsection{* Compactness (the definition is the one based on convegent subsequences). *}
   1.308  
   1.309 -definition "compact S \<longleftrightarrow>
   1.310 +definition
   1.311 +  compact :: "'a::metric_space set \<Rightarrow> bool" where (* TODO: generalize *)
   1.312 +  "compact S \<longleftrightarrow>
   1.313     (\<forall>f. (\<forall>n::nat. f n \<in> S) \<longrightarrow>
   1.314         (\<exists>l\<in>S. \<exists>r. (\<forall>m n. m < n \<longrightarrow> r m < r n) \<and> ((f o r) ---> l) sequentially))"
   1.315  
   1.316 @@ -2256,7 +2287,9 @@
   1.317    ultimately show "Suc n \<le> r (Suc n)" by auto
   1.318  qed
   1.319  
   1.320 -lemma lim_subsequence: "\<forall>m n. m < n \<longrightarrow> r m < r n \<Longrightarrow> (s ---> l) sequentially \<Longrightarrow> ((s o r) ---> l) sequentially"
   1.321 +lemma lim_subsequence:
   1.322 +  fixes l :: "'a::metric_space" (* TODO: generalize *)
   1.323 +  shows "\<forall>m n. m < n \<longrightarrow> r m < r n \<Longrightarrow> (s ---> l) sequentially \<Longrightarrow> ((s o r) ---> l) sequentially"
   1.324  unfolding Lim_sequentially by (simp, metis  monotone_bigger le_trans)
   1.325  
   1.326  lemma num_Axiom: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
   1.327 @@ -2700,6 +2733,7 @@
   1.328  qed
   1.329  
   1.330  lemma sequence_infinite_lemma:
   1.331 +  fixes l :: "'a::metric_space" (* TODO: generalize *)
   1.332    assumes "\<forall>n::nat. (f n  \<noteq> l)"  "(f ---> l) sequentially"
   1.333    shows "infinite {y. (\<exists> n. y = f n)}"
   1.334  proof(rule ccontr)
   1.335 @@ -2714,6 +2748,7 @@
   1.336  qed
   1.337  
   1.338  lemma sequence_unique_limpt:
   1.339 +  fixes l :: "'a::metric_space" (* TODO: generalize *)
   1.340    assumes "\<forall>n::nat. (f n \<noteq> l)"  "(f ---> l) sequentially"  "l' islimpt {y.  (\<exists>n. y = f n)}"
   1.341    shows "l' = l"
   1.342  proof(rule ccontr)
   1.343 @@ -3049,15 +3084,18 @@
   1.344  
   1.345  subsection{* Define continuity over a net to take in restrictions of the set. *}
   1.346  
   1.347 -definition "continuous net f \<longleftrightarrow> (f ---> f(netlimit net)) net"
   1.348 +definition
   1.349 +  continuous :: "'a::metric_space net \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> bool" where
   1.350 +  "continuous net f \<longleftrightarrow> (f ---> f(netlimit net)) net"
   1.351 +  (* FIXME: generalize 'b to topological_space *)
   1.352  
   1.353  lemma continuous_trivial_limit:
   1.354   "trivial_limit net ==> continuous net f"
   1.355 -  unfolding continuous_def tendsto_def trivial_limit_eq by auto
   1.356 +  unfolding continuous_def tendsto_iff trivial_limit_eq by auto
   1.357  
   1.358  lemma continuous_within: "continuous (at x within s) f \<longleftrightarrow> (f ---> f(x)) (at x within s)"
   1.359    unfolding continuous_def
   1.360 -  unfolding tendsto_def
   1.361 +  unfolding tendsto_iff
   1.362    using netlimit_within[of x s]
   1.363    by (cases "trivial_limit (at x within s)") (auto simp add: trivial_limit_eventually)
   1.364  
   1.365 @@ -3149,7 +3187,7 @@
   1.366    shows "continuous_on s f"
   1.367  proof(simp add: continuous_at continuous_on_def, rule, rule, rule)
   1.368    fix x and e::real assume "x\<in>s" "e>0"
   1.369 -  hence "eventually (\<lambda>xa. dist (f xa) (f x) < e) (at x)" using assms unfolding continuous_at tendsto_def by auto
   1.370 +  hence "eventually (\<lambda>xa. dist (f xa) (f x) < e) (at x)" using assms unfolding continuous_at tendsto_iff by auto
   1.371    then obtain d where d:"d>0" "\<forall>xa. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" unfolding eventually_at by auto
   1.372    { fix x' assume "\<not> 0 < dist x' x"
   1.373      hence "x=x'"
   1.374 @@ -4025,7 +4063,7 @@
   1.375  proof-
   1.376    { fix e::real and x assume "0 < dist x a" "dist x a < e" "e>0"
   1.377      hence "\<bar>x $ i - a $ i\<bar> < e" using component_le_norm[of "x - a" i] unfolding dist_norm by auto  }
   1.378 -  thus ?thesis unfolding continuous_at tendsto_def eventually_at dist_vec1 by auto
   1.379 +  thus ?thesis unfolding continuous_at tendsto_iff eventually_at dist_vec1 by auto
   1.380  qed
   1.381  
   1.382  lemma continuous_on_vec1_component:
   1.383 @@ -4207,7 +4245,7 @@
   1.384      have "eventually (\<lambda>x. dist ((vec1 o inverse o f) x) (vec1(inverse l)) < e) net"
   1.385        by (auto elim: eventually_rev_mono)
   1.386    }
   1.387 -  thus ?thesis unfolding tendsto_def by auto
   1.388 +  thus ?thesis unfolding tendsto_iff by auto
   1.389  qed
   1.390  
   1.391  lemma continuous_inv:
   1.392 @@ -5058,7 +5096,7 @@
   1.393      ultimately have "eventually (\<lambda>x. \<bar>a \<bullet> f x - a \<bullet> l\<bar> < e) net"
   1.394        by (auto elim: eventually_rev_mono)
   1.395    }
   1.396 -  thus ?thesis unfolding tendsto_def
   1.397 +  thus ?thesis unfolding tendsto_iff
   1.398      by (auto simp add: dist_vec1)
   1.399  qed
   1.400  
   1.401 @@ -5166,11 +5204,17 @@
   1.402  
   1.403  text{* Limits relative to a union.                                               *}
   1.404  
   1.405 +lemma eventually_within_Un:
   1.406 +  "eventually P (net within (s \<union> t)) \<longleftrightarrow>
   1.407 +    eventually P (net within s) \<and> eventually P (net within t)"
   1.408 +  unfolding Limits.eventually_within
   1.409 +  by (auto elim!: eventually_rev_mp)
   1.410 +
   1.411  lemma Lim_within_union:
   1.412   "(f ---> l) (net within (s \<union> t)) \<longleftrightarrow>
   1.413    (f ---> l) (net within s) \<and> (f ---> l) (net within t)"
   1.414 -  unfolding tendsto_def Limits.eventually_within
   1.415 -  by (auto elim!: eventually_elim1 intro: eventually_conjI)
   1.416 +  unfolding tendsto_def
   1.417 +  by (auto simp add: eventually_within_Un)
   1.418  
   1.419  lemma continuous_on_union:
   1.420    assumes "closed s" "closed t" "continuous_on s f" "continuous_on t f"
     2.1 --- a/src/HOL/Lim.thy	Fri Jun 05 15:59:20 2009 -0700
     2.2 +++ b/src/HOL/Lim.thy	Sat Jun 06 09:11:12 2009 -0700
     2.3 @@ -30,7 +30,7 @@
     2.4  subsection {* Limits of Functions *}
     2.5  
     2.6  lemma LIM_conv_tendsto: "(f -- a --> L) \<longleftrightarrow> (f ---> L) (at a)"
     2.7 -unfolding LIM_def tendsto_def eventually_at ..
     2.8 +unfolding LIM_def tendsto_iff eventually_at ..
     2.9  
    2.10  lemma metric_LIM_I:
    2.11    "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)
     3.1 --- a/src/HOL/Limits.thy	Fri Jun 05 15:59:20 2009 -0700
     3.2 +++ b/src/HOL/Limits.thy	Sat Jun 06 09:11:12 2009 -0700
     3.3 @@ -353,21 +353,47 @@
     3.4  subsection{* Limits *}
     3.5  
     3.6  definition
     3.7 -  tendsto :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
     3.8 -    (infixr "--->" 55) where
     3.9 -  [code del]: "(f ---> l) net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
    3.10 +  tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
    3.11 +    (infixr "--->" 55)
    3.12 +where [code del]:
    3.13 +  "(f ---> l) net \<longleftrightarrow> (\<forall>S\<in>topo. l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
    3.14  
    3.15 -lemma tendstoI:
    3.16 -  "(\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net)
    3.17 +lemma topological_tendstoI:
    3.18 +  "(\<And>S. S \<in> topo \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net)
    3.19      \<Longrightarrow> (f ---> l) net"
    3.20    unfolding tendsto_def by auto
    3.21  
    3.22 +lemma topological_tendstoD:
    3.23 +  "(f ---> l) net \<Longrightarrow> S \<in> topo \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net"
    3.24 +  unfolding tendsto_def by auto
    3.25 +
    3.26 +lemma tendstoI:
    3.27 +  assumes "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
    3.28 +  shows "(f ---> l) net"
    3.29 +apply (rule topological_tendstoI)
    3.30 +apply (simp add: topo_dist)
    3.31 +apply (drule (1) bspec, clarify)
    3.32 +apply (drule assms)
    3.33 +apply (erule eventually_elim1, simp)
    3.34 +done
    3.35 +
    3.36  lemma tendstoD:
    3.37    "(f ---> l) net \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
    3.38 -  unfolding tendsto_def by auto
    3.39 +apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD)
    3.40 +apply (clarsimp simp add: topo_dist)
    3.41 +apply (rule_tac x="e - dist x l" in exI, clarsimp)
    3.42 +apply (simp only: less_diff_eq)
    3.43 +apply (erule le_less_trans [OF dist_triangle])
    3.44 +apply simp
    3.45 +apply simp
    3.46 +done
    3.47 +
    3.48 +lemma tendsto_iff:
    3.49 +  "(f ---> l) net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
    3.50 +using tendstoI tendstoD by fast
    3.51  
    3.52  lemma tendsto_Zfun_iff: "(f ---> a) net = Zfun (\<lambda>x. f x - a) net"
    3.53 -by (simp only: tendsto_def Zfun_def dist_norm)
    3.54 +by (simp only: tendsto_iff Zfun_def dist_norm)
    3.55  
    3.56  lemma tendsto_const: "((\<lambda>x. k) ---> k) net"
    3.57  by (simp add: tendsto_def)
    3.58 @@ -375,7 +401,7 @@
    3.59  lemma tendsto_norm:
    3.60    fixes a :: "'a::real_normed_vector"
    3.61    shows "(f ---> a) net \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> norm a) net"
    3.62 -apply (simp add: tendsto_def dist_norm, safe)
    3.63 +apply (simp add: tendsto_iff dist_norm, safe)
    3.64  apply (drule_tac x="e" in spec, safe)
    3.65  apply (erule eventually_elim1)
    3.66  apply (erule order_le_less_trans [OF norm_triangle_ineq3])
     4.1 --- a/src/HOL/SEQ.thy	Fri Jun 05 15:59:20 2009 -0700
     4.2 +++ b/src/HOL/SEQ.thy	Sat Jun 06 09:11:12 2009 -0700
     4.3 @@ -194,7 +194,7 @@
     4.4  subsection {* Limits of Sequences *}
     4.5  
     4.6  lemma LIMSEQ_conv_tendsto: "(X ----> L) \<longleftrightarrow> (X ---> L) sequentially"
     4.7 -unfolding LIMSEQ_def tendsto_def eventually_sequentially ..
     4.8 +unfolding LIMSEQ_def tendsto_iff eventually_sequentially ..
     4.9  
    4.10  lemma LIMSEQ_iff:
    4.11    fixes L :: "'a::real_normed_vector"