# HG changeset patch
# User huffman
# Date 1244304672 25200
# Node ID 5691ccb8d6b52bd17bd2381a880897d60ce346ca
# Parent  93938cafc0e61548a02a44e35fad70abe689a13a
generalize tendsto to class topological_space

diff -r 93938cafc0e6 -r 5691ccb8d6b5 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Jun 05 15:59:20 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Sat Jun 06 09:11:12 2009 -0700
@@ -1171,46 +1171,50 @@
 subsection{* Limits, defined as vacuously true when the limit is trivial. *}
 
   text{* Notation Lim to avoid collition with lim defined in analysis *}
-definition "Lim net f = (THE l. (f ---> l) net)"
+definition
+  Lim :: "'a net \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b" where
+  "Lim net f = (THE l. (f ---> l) net)"
 
 lemma Lim:
  "(f ---> l) net \<longleftrightarrow>
         trivial_limit net \<or>
         (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
-  unfolding tendsto_def trivial_limit_eq by auto
+  unfolding tendsto_iff trivial_limit_eq by auto
 
 
 text{* Show that they yield usual definitions in the various cases. *}
 
 lemma Lim_within_le: "(f ---> l)(at a within S) \<longleftrightarrow>
            (\<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)"
-  by (auto simp add: tendsto_def eventually_within_le)
+  by (auto simp add: tendsto_iff eventually_within_le)
 
 lemma Lim_within: "(f ---> l) (at a within S) \<longleftrightarrow>
         (\<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)"
-  by (auto simp add: tendsto_def eventually_within)
+  by (auto simp add: tendsto_iff eventually_within)
 
 lemma Lim_at: "(f ---> l) (at a) \<longleftrightarrow>
         (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a  \<and> dist x a  < d  \<longrightarrow> dist (f x) l < e)"
-  by (auto simp add: tendsto_def eventually_at)
+  by (auto simp add: tendsto_iff eventually_at)
 
 lemma Lim_at_iff_LIM: "(f ---> l) (at a) \<longleftrightarrow> f -- a --> l"
   unfolding Lim_at LIM_def by (simp only: zero_less_dist_iff)
 
 lemma Lim_at_infinity:
   "(f ---> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x::real^'n::finite. norm x >= b \<longrightarrow> dist (f x) l < e)"
-  by (auto simp add: tendsto_def eventually_at_infinity)
+  by (auto simp add: tendsto_iff eventually_at_infinity)
 
 lemma Lim_sequentially:
  "(S ---> l) sequentially \<longleftrightarrow>
           (\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (S n) l < e)"
-  by (auto simp add: tendsto_def eventually_sequentially)
+  by (auto simp add: tendsto_iff eventually_sequentially)
 
 lemma Lim_sequentially_iff_LIMSEQ: "(S ---> l) sequentially \<longleftrightarrow> S ----> l"
   unfolding Lim_sequentially LIMSEQ_def ..
 
-lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
-  unfolding tendsto_def by (auto elim: eventually_rev_mono)
+lemma Lim_eventually:
+  fixes l :: "'a::metric_space" (* FIXME: generalize to t2_space *)
+  shows "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
+  unfolding tendsto_iff by (auto elim: eventually_rev_mono)
 
 text{* The expected monotonicity property. *}
 
@@ -1225,7 +1229,7 @@
   shows "(f ---> l) (net within (S \<union> T))"
   using assms unfolding tendsto_def Limits.eventually_within
   apply clarify
-  apply (drule spec, drule (1) mp)+
+  apply (drule (1) bspec)+
   apply (auto elim: eventually_elim2)
   done
 
@@ -1238,9 +1242,11 @@
 
 lemma Lim_at_within: "(f ---> l) net ==> (f ---> l)(net within S)"
   unfolding tendsto_def Limits.eventually_within
+  apply (clarify, drule (1) bspec)
   by (auto elim!: eventually_elim1)
 
 lemma Lim_within_open:
+  fixes l :: "'a::metric_space" (* FIXME: generalize to topological_space *)
   assumes"a \<in> S" "open S"
   shows "(f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)" (is "?lhs \<longleftrightarrow> ?rhs")
 proof
@@ -1268,7 +1274,9 @@
 text{* Another limit point characterization. *}
 
 lemma islimpt_sequential:
- "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S -{x}) \<and> (f ---> x) sequentially)" (is "?lhs = ?rhs")
+  fixes x :: "'a::metric_space" (* FIXME: generalize to topological_space *)
+  shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S -{x}) \<and> (f ---> x) sequentially)"
+    (is "?lhs = ?rhs")
 proof
   assume ?lhs
   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"
@@ -1317,11 +1325,11 @@
       apply (simp add: pos_less_divide_eq `0 < b` mult_commute)
       done
   }
-  thus ?thesis unfolding tendsto_def by simp
+  thus ?thesis unfolding tendsto_iff by simp
 qed
 
 lemma Lim_const: "((\<lambda>x. a) ---> a) net"
-  by (auto simp add: Lim trivial_limit_def)
+  unfolding tendsto_def by simp
 
 lemma Lim_cmul:
   fixes f :: "'a \<Rightarrow> real ^ 'n::finite"
@@ -1355,7 +1363,7 @@
       apply simp
       done
   }
-  thus ?thesis unfolding tendsto_def by simp
+  thus ?thesis unfolding tendsto_iff by simp
 qed
 
 lemma Lim_sub:
@@ -1377,7 +1385,7 @@
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   assumes "eventually (\<lambda>x. norm(f x) <= g x) net" "((\<lambda>x. vec1(g x)) ---> 0) net"
   shows "(f ---> 0) net"
-proof(simp add: tendsto_def, rule+)
+proof(simp add: tendsto_iff, rule+)
   fix e::real assume "0<e"
   { fix x
     assume "norm (f x) \<le> g x" "dist (vec1 (g x)) 0 < e"
@@ -1387,12 +1395,12 @@
   thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
     using eventually_and[of "\<lambda>x. norm(f x) <= g x" "\<lambda>x. dist (vec1 (g x)) 0 < e" net]
     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]
-    using assms `e>0` unfolding tendsto_def by auto
+    using assms `e>0` unfolding tendsto_iff by auto
 qed
 
 lemma Lim_component: "(f ---> l) net
                       ==> ((\<lambda>a. vec1((f a :: real ^'n::finite)$i)) ---> vec1(l$i)) net"
-  unfolding tendsto_def
+  unfolding tendsto_iff
   apply (simp add: dist_norm vec1_sub[symmetric] norm_vec1  vector_minus_component[symmetric] del: vector_minus_component)
   apply (auto simp del: vector_minus_component)
   apply (erule_tac x=e in allE)
@@ -1408,7 +1416,7 @@
   fixes g :: "'a \<Rightarrow> 'c::real_normed_vector"
   assumes "eventually (\<lambda>n. norm(f n) <= norm(g n)) net"  "(g ---> 0) net"
   shows "(f ---> 0) net"
-proof(simp add: tendsto_def, rule+)
+proof(simp add: tendsto_iff, rule+)
   fix e::real assume "e>0"
   { fix x
     assume "norm (f x) \<le> norm (g x)" "dist (g x) 0 < e"
@@ -1416,12 +1424,13 @@
   thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
     using eventually_and[of "\<lambda>x. norm (f x) \<le> norm (g x)" "\<lambda>x. dist (g x) 0 < e" net]
     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]
-    using assms `e>0` unfolding tendsto_def by blast
+    using assms `e>0` unfolding tendsto_iff by blast
 qed
 
 text{* Deducing things about the limit from the elements. *}
 
 lemma Lim_in_closed_set:
+  fixes l :: "'a::metric_space" (* FIXME: generalize to topological_space *)
   assumes "closed S" "eventually (\<lambda>x. f(x) \<in> S) net"  "\<not>(trivial_limit net)" "(f ---> l) net"
   shows "l \<in> S"
 proof (rule ccontr)
@@ -1581,17 +1590,21 @@
       by (auto elim: eventually_rev_mono)
   }
   thus "((\<lambda>x. h (f x) (g x)) ---> h l m) net"
-    unfolding tendsto_def by simp
+    unfolding tendsto_iff by simp
 qed
 
 text{* These are special for limits out of the same vector space. *}
 
-lemma Lim_within_id: "(id ---> a) (at a within s)" by (auto simp add: Lim_within id_def)
+lemma Lim_within_id: "(id ---> a) (at a within s)"
+  unfolding tendsto_def Limits.eventually_within eventually_at_topological
+  by auto
+
 lemma Lim_at_id: "(id ---> a) (at a)"
 apply (subst within_UNIV[symmetric]) by (simp add: Lim_within_id)
 
 lemma Lim_at_zero:
   fixes a :: "'a::real_normed_vector"
+  fixes l :: "'b::metric_space" (* FIXME: generalize to topological_space *)
   shows "(f ---> l) (at a) \<longleftrightarrow> ((\<lambda>x. f(a + x)) ---> l) (at 0)" (is "?lhs = ?rhs")
 proof
   assume "?lhs"
@@ -1671,13 +1684,15 @@
 qed
 
 lemma Lim_transform_eventually:
+  fixes l :: "'a::metric_space" (* FIXME: generalize to t2_space *)
   shows "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net ==> (g ---> l) net"
-  unfolding tendsto_def
+  unfolding tendsto_iff
   apply (clarify, drule spec, drule (1) mp)
   apply (erule (1) eventually_elim2, simp)
   done
 
 lemma Lim_transform_within:
+  fixes l :: "'b::metric_space" (* TODO: generalize *)
   assumes "0 < d" "(\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x')"
           "(f ---> l) (at x within S)"
   shows   "(g ---> l) (at x within S)"
@@ -1691,6 +1706,7 @@
   done
 
 lemma Lim_transform_at:
+  fixes l :: "'b::metric_space" (* TODO: generalize *)
   shows "0 < d \<Longrightarrow> (\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x') \<Longrightarrow>
   (f ---> l) (at x) ==> (g ---> l) (at x)"
   apply (subst within_UNIV[symmetric])
@@ -1701,6 +1717,7 @@
 
 lemma Lim_transform_away_within:
   fixes a b :: "'a::metric_space"
+  fixes l :: "'b::metric_space" (* TODO: generalize *)
   assumes "a\<noteq>b" "\<forall>x\<in> S. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
   and "(f ---> l) (at a within S)"
   shows "(g ---> l) (at a within S)"
@@ -1712,6 +1729,7 @@
 
 lemma Lim_transform_away_at:
   fixes a b :: "'a::metric_space"
+  fixes l :: "'b::metric_space" (* TODO: generalize *)
   assumes ab: "a\<noteq>b" and fg: "\<forall>x. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
   and fl: "(f ---> l) (at a)"
   shows "(g ---> l) (at a)"
@@ -1722,6 +1740,7 @@
 
 lemma Lim_transform_within_open:
   fixes a :: "'a::metric_space"
+  fixes l :: "'b::metric_space" (* TODO: generalize *)
   assumes "open S"  "a \<in> S"  "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x"  "(f ---> l) (at a)"
   shows "(g ---> l) (at a)"
 proof-
@@ -1736,19 +1755,22 @@
 (* FIXME: Only one congruence rule for tendsto can be used at a time! *)
 
 lemma Lim_cong_within[cong add]:
-  fixes a :: "'a::metric_space" 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))"
+  fixes a :: "'a::metric_space"
+  fixes l :: "'b::metric_space" (* TODO: generalize *)
+  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))"
   by (simp add: Lim_within dist_nz[symmetric])
 
 lemma Lim_cong_at[cong add]:
-  fixes a :: "'a::metric_space" shows
- "(\<And>x. x \<noteq> a ==> f x = g x) ==> (((\<lambda>x. f x) ---> l) (at a) \<longleftrightarrow> ((g ---> l) (at a)))"
+  fixes a :: "'a::metric_space"
+  fixes l :: "'b::metric_space" (* TODO: generalize *)
+  shows "(\<And>x. x \<noteq> a ==> f x = g x) ==> (((\<lambda>x. f x) ---> l) (at a) \<longleftrightarrow> ((g ---> l) (at a)))"
   by (simp add: Lim_at dist_nz[symmetric])
 
 text{* Useful lemmas on closure and set of possible sequential limits.*}
 
 lemma closure_sequential:
- "l \<in> closure S \<longleftrightarrow> (\<exists>x. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially)" (is "?lhs = ?rhs")
+  fixes l :: "'a::metric_space" (* TODO: generalize *)
+  shows "l \<in> closure S \<longleftrightarrow> (\<exists>x. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially)" (is "?lhs = ?rhs")
 proof
   assume "?lhs" moreover
   { assume "l \<in> S"
@@ -1783,17 +1805,23 @@
 
 text{* Some other lemmas about sequences. *}
 
-lemma seq_offset: "(f ---> l) sequentially ==> ((\<lambda>i. f( i + k)) ---> l) sequentially"
+lemma seq_offset:
+  fixes l :: "'a::metric_space" (* TODO: generalize *)
+  shows "(f ---> l) sequentially ==> ((\<lambda>i. f( i + k)) ---> l) sequentially"
   apply (auto simp add: Lim_sequentially)
   by (metis trans_le_add1 )
 
-lemma seq_offset_neg: "(f ---> l) sequentially ==> ((\<lambda>i. f(i - k)) ---> l) sequentially"
+lemma seq_offset_neg:
+  fixes l :: "'a::metric_space" (* TODO: generalize *)
+  shows "(f ---> l) sequentially ==> ((\<lambda>i. f(i - k)) ---> l) sequentially"
   apply (simp add: Lim_sequentially)
   apply (subgoal_tac "\<And>N k (n::nat). N + k <= n ==> N <= n - k")
   apply metis
   by arith
 
-lemma seq_offset_rev: "((\<lambda>i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially"
+lemma seq_offset_rev:
+  fixes l :: "'a::metric_space" (* TODO: generalize *)
+  shows "((\<lambda>i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially"
   apply (simp add: Lim_sequentially)
   apply (subgoal_tac "\<And>N k (n::nat). N + k <= n ==> N <= n - k \<and> (n - k) + k = n")
   by metis arith
@@ -2017,8 +2045,9 @@
 
 lemma lim_within_interior:
   fixes x :: "'a::metric_space"
+  fixes l :: "'b::metric_space" (* TODO: generalize *)
   shows "x \<in> interior S  ==> ((f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x))"
-  by (simp add: tendsto_def eventually_within_interior)
+  by (simp add: tendsto_iff eventually_within_interior)
 
 lemma netlimit_within_interior:
   fixes x :: "'a::{perfect_space, real_normed_vector}"
@@ -2241,7 +2270,9 @@
 
 subsection{* Compactness (the definition is the one based on convegent subsequences). *}
 
-definition "compact S \<longleftrightarrow>
+definition
+  compact :: "'a::metric_space set \<Rightarrow> bool" where (* TODO: generalize *)
+  "compact S \<longleftrightarrow>
    (\<forall>f. (\<forall>n::nat. f n \<in> S) \<longrightarrow>
        (\<exists>l\<in>S. \<exists>r. (\<forall>m n. m < n \<longrightarrow> r m < r n) \<and> ((f o r) ---> l) sequentially))"
 
@@ -2256,7 +2287,9 @@
   ultimately show "Suc n \<le> r (Suc n)" by auto
 qed
 
-lemma lim_subsequence: "\<forall>m n. m < n \<longrightarrow> r m < r n \<Longrightarrow> (s ---> l) sequentially \<Longrightarrow> ((s o r) ---> l) sequentially"
+lemma lim_subsequence:
+  fixes l :: "'a::metric_space" (* TODO: generalize *)
+  shows "\<forall>m n. m < n \<longrightarrow> r m < r n \<Longrightarrow> (s ---> l) sequentially \<Longrightarrow> ((s o r) ---> l) sequentially"
 unfolding Lim_sequentially by (simp, metis  monotone_bigger le_trans)
 
 lemma num_Axiom: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
@@ -2700,6 +2733,7 @@
 qed
 
 lemma sequence_infinite_lemma:
+  fixes l :: "'a::metric_space" (* TODO: generalize *)
   assumes "\<forall>n::nat. (f n  \<noteq> l)"  "(f ---> l) sequentially"
   shows "infinite {y. (\<exists> n. y = f n)}"
 proof(rule ccontr)
@@ -2714,6 +2748,7 @@
 qed
 
 lemma sequence_unique_limpt:
+  fixes l :: "'a::metric_space" (* TODO: generalize *)
   assumes "\<forall>n::nat. (f n \<noteq> l)"  "(f ---> l) sequentially"  "l' islimpt {y.  (\<exists>n. y = f n)}"
   shows "l' = l"
 proof(rule ccontr)
@@ -3049,15 +3084,18 @@
 
 subsection{* Define continuity over a net to take in restrictions of the set. *}
 
-definition "continuous net f \<longleftrightarrow> (f ---> f(netlimit net)) net"
+definition
+  continuous :: "'a::metric_space net \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> bool" where
+  "continuous net f \<longleftrightarrow> (f ---> f(netlimit net)) net"
+  (* FIXME: generalize 'b to topological_space *)
 
 lemma continuous_trivial_limit:
  "trivial_limit net ==> continuous net f"
-  unfolding continuous_def tendsto_def trivial_limit_eq by auto
+  unfolding continuous_def tendsto_iff trivial_limit_eq by auto
 
 lemma continuous_within: "continuous (at x within s) f \<longleftrightarrow> (f ---> f(x)) (at x within s)"
   unfolding continuous_def
-  unfolding tendsto_def
+  unfolding tendsto_iff
   using netlimit_within[of x s]
   by (cases "trivial_limit (at x within s)") (auto simp add: trivial_limit_eventually)
 
@@ -3149,7 +3187,7 @@
   shows "continuous_on s f"
 proof(simp add: continuous_at continuous_on_def, rule, rule, rule)
   fix x and e::real assume "x\<in>s" "e>0"
-  hence "eventually (\<lambda>xa. dist (f xa) (f x) < e) (at x)" using assms unfolding continuous_at tendsto_def by auto
+  hence "eventually (\<lambda>xa. dist (f xa) (f x) < e) (at x)" using assms unfolding continuous_at tendsto_iff by auto
   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
   { fix x' assume "\<not> 0 < dist x' x"
     hence "x=x'"
@@ -4025,7 +4063,7 @@
 proof-
   { fix e::real and x assume "0 < dist x a" "dist x a < e" "e>0"
     hence "\<bar>x $ i - a $ i\<bar> < e" using component_le_norm[of "x - a" i] unfolding dist_norm by auto  }
-  thus ?thesis unfolding continuous_at tendsto_def eventually_at dist_vec1 by auto
+  thus ?thesis unfolding continuous_at tendsto_iff eventually_at dist_vec1 by auto
 qed
 
 lemma continuous_on_vec1_component:
@@ -4207,7 +4245,7 @@
     have "eventually (\<lambda>x. dist ((vec1 o inverse o f) x) (vec1(inverse l)) < e) net"
       by (auto elim: eventually_rev_mono)
   }
-  thus ?thesis unfolding tendsto_def by auto
+  thus ?thesis unfolding tendsto_iff by auto
 qed
 
 lemma continuous_inv:
@@ -5058,7 +5096,7 @@
     ultimately have "eventually (\<lambda>x. \<bar>a \<bullet> f x - a \<bullet> l\<bar> < e) net"
       by (auto elim: eventually_rev_mono)
   }
-  thus ?thesis unfolding tendsto_def
+  thus ?thesis unfolding tendsto_iff
     by (auto simp add: dist_vec1)
 qed
 
@@ -5166,11 +5204,17 @@
 
 text{* Limits relative to a union.                                               *}
 
+lemma eventually_within_Un:
+  "eventually P (net within (s \<union> t)) \<longleftrightarrow>
+    eventually P (net within s) \<and> eventually P (net within t)"
+  unfolding Limits.eventually_within
+  by (auto elim!: eventually_rev_mp)
+
 lemma Lim_within_union:
  "(f ---> l) (net within (s \<union> t)) \<longleftrightarrow>
   (f ---> l) (net within s) \<and> (f ---> l) (net within t)"
-  unfolding tendsto_def Limits.eventually_within
-  by (auto elim!: eventually_elim1 intro: eventually_conjI)
+  unfolding tendsto_def
+  by (auto simp add: eventually_within_Un)
 
 lemma continuous_on_union:
   assumes "closed s" "closed t" "continuous_on s f" "continuous_on t f"
diff -r 93938cafc0e6 -r 5691ccb8d6b5 src/HOL/Lim.thy
--- a/src/HOL/Lim.thy	Fri Jun 05 15:59:20 2009 -0700
+++ b/src/HOL/Lim.thy	Sat Jun 06 09:11:12 2009 -0700
@@ -30,7 +30,7 @@
 subsection {* Limits of Functions *}
 
 lemma LIM_conv_tendsto: "(f -- a --> L) \<longleftrightarrow> (f ---> L) (at a)"
-unfolding LIM_def tendsto_def eventually_at ..
+unfolding LIM_def tendsto_iff eventually_at ..
 
 lemma metric_LIM_I:
   "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)
diff -r 93938cafc0e6 -r 5691ccb8d6b5 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Fri Jun 05 15:59:20 2009 -0700
+++ b/src/HOL/Limits.thy	Sat Jun 06 09:11:12 2009 -0700
@@ -353,21 +353,47 @@
 subsection{* Limits *}
 
 definition
-  tendsto :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
-    (infixr "--->" 55) where
-  [code del]: "(f ---> l) net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
+  tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
+    (infixr "--->" 55)
+where [code del]:
+  "(f ---> l) net \<longleftrightarrow> (\<forall>S\<in>topo. l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
 
-lemma tendstoI:
-  "(\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net)
+lemma topological_tendstoI:
+  "(\<And>S. S \<in> topo \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net)
     \<Longrightarrow> (f ---> l) net"
   unfolding tendsto_def by auto
 
+lemma topological_tendstoD:
+  "(f ---> l) net \<Longrightarrow> S \<in> topo \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net"
+  unfolding tendsto_def by auto
+
+lemma tendstoI:
+  assumes "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
+  shows "(f ---> l) net"
+apply (rule topological_tendstoI)
+apply (simp add: topo_dist)
+apply (drule (1) bspec, clarify)
+apply (drule assms)
+apply (erule eventually_elim1, simp)
+done
+
 lemma tendstoD:
   "(f ---> l) net \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
-  unfolding tendsto_def by auto
+apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD)
+apply (clarsimp simp add: topo_dist)
+apply (rule_tac x="e - dist x l" in exI, clarsimp)
+apply (simp only: less_diff_eq)
+apply (erule le_less_trans [OF dist_triangle])
+apply simp
+apply simp
+done
+
+lemma tendsto_iff:
+  "(f ---> l) net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
+using tendstoI tendstoD by fast
 
 lemma tendsto_Zfun_iff: "(f ---> a) net = Zfun (\<lambda>x. f x - a) net"
-by (simp only: tendsto_def Zfun_def dist_norm)
+by (simp only: tendsto_iff Zfun_def dist_norm)
 
 lemma tendsto_const: "((\<lambda>x. k) ---> k) net"
 by (simp add: tendsto_def)
@@ -375,7 +401,7 @@
 lemma tendsto_norm:
   fixes a :: "'a::real_normed_vector"
   shows "(f ---> a) net \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> norm a) net"
-apply (simp add: tendsto_def dist_norm, safe)
+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])
diff -r 93938cafc0e6 -r 5691ccb8d6b5 src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Fri Jun 05 15:59:20 2009 -0700
+++ b/src/HOL/SEQ.thy	Sat Jun 06 09:11:12 2009 -0700
@@ -194,7 +194,7 @@
 subsection {* Limits of Sequences *}
 
 lemma LIMSEQ_conv_tendsto: "(X ----> L) \<longleftrightarrow> (X ---> L) sequentially"
-unfolding LIMSEQ_def tendsto_def eventually_sequentially ..
+unfolding LIMSEQ_def tendsto_iff eventually_sequentially ..
 
 lemma LIMSEQ_iff:
   fixes L :: "'a::real_normed_vector"