# HG changeset patch
# User huffman
# Date 1244161449 25200
# Node ID 97bab1ac463efb6e31ee252a5486676c46eb265f
# Parent  2d91b2416de842a462fa356ca090209d01a852a8
generalize type of 'at' to topological_space; generalize some lemmas

diff -r 2d91b2416de8 -r 97bab1ac463e src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Thu Jun 04 16:11:36 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Thu Jun 04 17:24:09 2009 -0700
@@ -1058,26 +1058,25 @@
   "trivial_limit net \<longleftrightarrow> {} \<in> Rep_net net"
 
 lemma trivial_limit_within:
-  fixes a :: "'a::metric_space"
   shows "trivial_limit (at a within S) \<longleftrightarrow> \<not> a islimpt S"
 proof
   assume "trivial_limit (at a within S)"
   thus "\<not> a islimpt S"
     unfolding trivial_limit_def
     unfolding Rep_net_within Rep_net_at
-    unfolding islimpt_approachable_le dist_nz
-    apply (clarsimp simp add: not_le expand_set_eq)
-    apply (rule_tac x="r/2" in exI, clarsimp)
-    apply (drule_tac x=x' in spec, simp)
+    unfolding islimpt_def open_def [symmetric]
+    apply (clarsimp simp add: expand_set_eq)
+    apply (rename_tac T, rule_tac x=T in exI)
+    apply (clarsimp, drule_tac x=y in spec, simp)
     done
 next
   assume "\<not> a islimpt S"
   thus "trivial_limit (at a within S)"
     unfolding trivial_limit_def
     unfolding Rep_net_within Rep_net_at
-    unfolding islimpt_approachable_le dist_nz
-    apply (clarsimp simp add: image_image not_le)
-    apply (rule_tac x=e in image_eqI)
+    unfolding islimpt_def open_def [symmetric]
+    apply (clarsimp simp add: image_image)
+    apply (rule_tac x=T in image_eqI)
     apply (auto simp add: expand_set_eq)
     done
 qed
@@ -1105,9 +1104,9 @@
 
 subsection{* Some property holds "sufficiently close" to the limit point. *}
 
-lemma eventually_at:
+lemma eventually_at: (* FIXME: this replaces Limits.eventually_at *)
   "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
-unfolding eventually_def Rep_net_at dist_nz by auto
+unfolding eventually_at dist_nz by auto
 
 lemma eventually_at_infinity:
   "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. norm x >= b \<longrightarrow> P x)"
@@ -1212,35 +1211,31 @@
 
 text{* The expected monotonicity property. *}
 
-lemma Lim_within_empty: "(f ---> l) (at x within {})"
-  by (simp add: Lim_within_le)
-
-lemma Lim_within_subset: "(f ---> l) (at a within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (at a within T)"
-  apply (auto simp add: Lim_within_le)
-  by (metis subset_eq)
-
-lemma Lim_Un: assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)"
-  shows "(f ---> l) (at x within (S \<union> T))"
-proof-
-  { fix e::real assume "e>0"
-    obtain d1 where d1:"d1>0" "\<forall>xa\<in>T. 0 < dist xa x \<and> dist xa x < d1 \<longrightarrow> dist (f xa) l < e" using assms unfolding Lim_within using `e>0` by auto
-    obtain d2 where d2:"d2>0" "\<forall>xa\<in>S. 0 < dist xa x \<and> dist xa x < d2 \<longrightarrow> dist (f xa) l < e" using assms unfolding Lim_within using `e>0` by auto
-    have "\<exists>d>0. \<forall>xa\<in>S \<union> T. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) l < e" using d1 d2
-      by (rule_tac x="min d1 d2" in exI)auto
-  }
-  thus ?thesis unfolding Lim_within by auto
-qed
+lemma Lim_within_empty: "(f ---> l) (net within {})"
+  unfolding tendsto_def Limits.eventually_within by simp
+
+lemma Lim_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
+  unfolding tendsto_def Limits.eventually_within
+  by (auto elim!: eventually_elim1)
+
+lemma Lim_Un: assumes "(f ---> l) (net within S)" "(f ---> l) (net within T)"
+  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 (auto elim: eventually_elim2)
+  done
 
 lemma Lim_Un_univ:
- "(f ---> l) (at x within S) \<Longrightarrow> (f ---> l) (at x within T) \<Longrightarrow>  S \<union> T = UNIV
-        ==> (f ---> l) (at x)"
+ "(f ---> l) (net within S) \<Longrightarrow> (f ---> l) (net within T) \<Longrightarrow>  S \<union> T = UNIV
+        ==> (f ---> l) net"
   by (metis Lim_Un within_UNIV)
 
 text{* Interrelations between restricted and unrestricted limits. *}
 
-lemma Lim_at_within: "(f ---> l)(at a) ==> (f ---> l)(at a within S)"
-  apply (simp add: Lim_at Lim_within)
-  by metis
+lemma Lim_at_within: "(f ---> l) net ==> (f ---> l)(net within S)"
+  unfolding tendsto_def Limits.eventually_within
+  by (auto elim!: eventually_elim1)
 
 lemma Lim_within_open:
   assumes"a \<in> S" "open S"
@@ -1248,18 +1243,23 @@
 proof
   assume ?lhs
   { fix e::real assume "e>0"
-    obtain d  where d:  "d >0" "\<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" using `?lhs` `e>0` unfolding Lim_within by auto
-    obtain d' where d': "d'>0" "\<forall>x. dist x a < d' \<longrightarrow> x \<in> S" using assms  unfolding open_dist by auto
-    from d d' have "\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" by (rule_tac x= "min d d'" in exI)auto
+    have "eventually (\<lambda>x. dist (f x) l < e) (at a within S)"
+      using `?lhs` `e>0` by (rule tendstoD)
+    hence "eventually (\<lambda>x. x \<in> S \<longrightarrow> dist (f x) l < e) (at a)"
+      unfolding Limits.eventually_within .
+    then obtain T where "open T" "a \<in> T" "\<forall>x\<in>T. x \<noteq> a \<longrightarrow> x \<in> S \<longrightarrow> dist (f x) l < e"
+      unfolding eventually_at_topological open_def by fast
+    hence "open (T \<inter> S)" "a \<in> T \<inter> S" "\<forall>x\<in>(T \<inter> S). x \<noteq> a \<longrightarrow> dist (f x) l < e"
+      using assms by auto
+    hence "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<noteq> a \<longrightarrow> dist (f x) l < e)"
+      by fast
+    hence "eventually (\<lambda>x. dist (f x) l < e) (at a)"
+      unfolding eventually_at_topological open_def Bex_def .
   }
-  thus ?rhs unfolding Lim_at by auto
+  thus ?rhs by (rule tendstoI)
 next
   assume ?rhs
-  { fix e::real assume "e>0"
-    then obtain d where "d>0" and d:"\<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" using `?rhs` unfolding Lim_at by auto
-    hence "\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" using `d>0` by auto
-  }
-  thus ?lhs using Lim_at_within[of f l a S] by (auto simp add: Lim_at)
+  thus ?lhs by (rule Lim_at_within)
 qed
 
 text{* Another limit point characterization. *}
@@ -1632,7 +1632,8 @@
   shows "netlimit (at a within S) = a"
 using assms
 apply (simp add: trivial_limit_within)
-apply (simp add: netlimit_def Rep_net_within Rep_net_at)
+apply (simp add: netlimit_def eventually_def [symmetric])
+apply (simp add: eventually_within zero_less_dist_iff)
 apply (rule some_equality, fast)
 apply (rename_tac b)
 apply (rule ccontr)
@@ -1641,7 +1642,8 @@
 apply (simp only: islimpt_approachable)
 apply (drule_tac x="min r (dist b a / 2)" in spec, drule mp, simp add: dist_nz)
 apply (clarify)
-apply (drule_tac x=x' in bspec, simp add: dist_nz)
+apply (drule_tac x=x' in bspec, simp)
+apply (drule mp, simp)
 apply (subgoal_tac "dist b a < dist b a / 2 + dist b a / 2", simp)
 apply (rule le_less_trans [OF dist_triangle3])
 apply (erule add_strict_mono)
@@ -1696,6 +1698,7 @@
 text{* Common case assuming being away from some crucial point like 0. *}
 
 lemma Lim_transform_away_within:
+  fixes a b :: "'a::metric_space"
   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)"
@@ -1706,6 +1709,7 @@
 qed
 
 lemma Lim_transform_away_at:
+  fixes a b :: "'a::metric_space"
   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)"
@@ -1715,6 +1719,7 @@
 text{* Alternatively, within an open set. *}
 
 lemma Lim_transform_within_open:
+  fixes a :: "'a::metric_space"
   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-
@@ -1729,10 +1734,12 @@
 (* 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))"
   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)))"
   by (simp add: Lim_at dist_nz[symmetric])
 
@@ -1992,7 +1999,9 @@
 
 text{* For points in the interior, localization of limits makes no difference.   *}
 
-lemma eventually_within_interior: assumes "x \<in> interior S"
+lemma eventually_within_interior:
+  fixes x :: "'a::metric_space"
+  assumes "x \<in> interior S"
   shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" (is "?lhs = ?rhs")
 proof-
   from assms obtain e where e:"e>0" "\<forall>y. dist x y < e \<longrightarrow> y \<in> S" unfolding mem_interior ball_def subset_eq by auto
@@ -2004,7 +2013,9 @@
   show "?thesis" by auto
 qed
 
-lemma lim_within_interior: "x \<in> interior S  ==> ((f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x))"
+lemma lim_within_interior:
+  fixes x :: "'a::metric_space"
+  shows "x \<in> interior S  ==> ((f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x))"
   by (simp add: tendsto_def eventually_within_interior)
 
 lemma netlimit_within_interior:
@@ -3057,7 +3068,7 @@
   (* FIXME: generalize *)
 proof(cases "x islimpt s")
   case True show ?thesis using assms unfolding continuous_def and netlimit_at
-    using Lim_at_within[of f "f x" x s]
+    using Lim_at_within[of f "f x" "at x" s]
     unfolding netlimit_within[unfolded trivial_limit_within not_not, OF True] by blast
 next
   case False thus ?thesis unfolding continuous_def and netlimit_at
@@ -5154,11 +5165,10 @@
 text{* Limits relative to a union.                                               *}
 
 lemma Lim_within_union:
- "(f ---> l) (at x within (s \<union> t)) \<longleftrightarrow>
-  (f ---> l) (at x within s) \<and> (f ---> l) (at x within t)"
-  unfolding Lim_within apply auto apply blast apply blast
-    apply(erule_tac x=e in allE)+ apply auto
-    apply(rule_tac x="min d da" in exI) by auto
+ "(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)
 
 lemma continuous_on_union:
   assumes "closed s" "closed t" "continuous_on s f" "continuous_on t f"
diff -r 2d91b2416de8 -r 97bab1ac463e src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Thu Jun 04 16:11:36 2009 -0700
+++ b/src/HOL/Limits.thy	Thu Jun 04 17:24:09 2009 -0700
@@ -109,12 +109,12 @@
   [code del]: "sequentially = Abs_net (range (\<lambda>n. {n..}))"
 
 definition
-  at :: "'a::metric_space \<Rightarrow> 'a net" where
-  [code del]: "at a = Abs_net ((\<lambda>r. {x. x \<noteq> a \<and> dist x a < r}) ` {r. 0 < r})"
+  within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70) where
+  [code del]: "net within S = Abs_net ((\<lambda>A. A \<inter> S) ` Rep_net net)"
 
 definition
-  within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70) where
-  [code del]: "net within S = Abs_net ((\<lambda>A. A \<inter> S) ` Rep_net net)"
+  at :: "'a::topological_space \<Rightarrow> 'a net" where
+  [code del]: "at a = Abs_net ((\<lambda>S. S - {a}) ` {S\<in>topo. a \<in> S})"
 
 lemma Rep_net_sequentially:
   "Rep_net sequentially = range (\<lambda>n. {n..})"
@@ -125,15 +125,6 @@
 apply (rule_tac x="max m n" in exI, auto)
 done
 
-lemma Rep_net_at:
-  "Rep_net (at a) = ((\<lambda>r. {x. x \<noteq> a \<and> 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) = (\<lambda>A. A \<inter> S) ` Rep_net net"
 unfolding within_def
@@ -144,18 +135,41 @@
 apply (clarify, rule_tac x=C in bexI, auto)
 done
 
+lemma Rep_net_at:
+  "Rep_net (at a) = ((\<lambda>S. S - {a}) ` {S\<in>topo. a \<in> S})"
+unfolding at_def
+apply (rule Abs_net_inverse')
+apply (rule image_nonempty)
+apply (rule_tac x="UNIV" in exI, simp add: topo_UNIV)
+apply (clarsimp, rename_tac S T)
+apply (rule_tac x="S \<inter> T" in exI, auto simp add: topo_Int)
+done
+
 lemma eventually_sequentially:
   "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
 unfolding eventually_def Rep_net_sequentially by auto
 
-lemma eventually_at:
-  "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
-unfolding eventually_def Rep_net_at by auto
-
 lemma eventually_within:
   "eventually P (net within S) = eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) net"
 unfolding eventually_def Rep_net_within by auto
 
+lemma eventually_at_topological:
+  "eventually P (at a) \<longleftrightarrow> (\<exists>S\<in>topo. a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
+unfolding eventually_def Rep_net_at by auto
+
+lemma eventually_at:
+  fixes a :: "'a::metric_space"
+  shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
+unfolding eventually_at_topological topo_dist
+apply safe
+apply fast
+apply (rule_tac x="{x. dist x a < d}" in bexI, simp)
+apply clarsimp
+apply (rule_tac x="d - dist x a" in exI, clarsimp)
+apply (simp only: less_diff_eq)
+apply (erule le_less_trans [OF dist_triangle])
+done
+
 
 subsection {* Boundedness *}