# HG changeset patch
# User huffman
# Date 1244486195 25200
# Node ID 2ce3583b9261420b15f2e96942319e7be5d8a6f5
# Parent  472b844f860732fe57fbfe50ce2f9704939ba8ab
generalize more lemmas

diff -r 472b844f8607 -r 2ce3583b9261 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Jun 08 08:42:33 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Jun 08 11:36:35 2009 -0700
@@ -1514,31 +1514,41 @@
 
 lemma Lim_at_zero:
   fixes a :: "'a::real_normed_vector"
-  fixes l :: "'b::metric_space" (* FIXME: generalize to topological_space *)
+  fixes l :: "'b::topological_space"
   shows "(f ---> l) (at a) \<longleftrightarrow> ((\<lambda>x. f(a + x)) ---> l) (at 0)" (is "?lhs = ?rhs")
 proof
   assume "?lhs"
-  { fix e::real assume "e>0"
-    with `?lhs` obtain d where d:"d>0" "\<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" unfolding Lim_at by auto
-    { fix x::"'a" assume "0 < dist x 0 \<and> dist x 0 < d"
-      hence "dist (f (a + x)) l < e" using d
-      apply(erule_tac x="x+a" in allE) by(auto simp add: comm_monoid_add.mult_commute dist_norm dist_commute)
+  { fix S assume "open S" "l \<in> S"
+    with `?lhs` have "eventually (\<lambda>x. f x \<in> S) (at a)"
+      by (rule topological_tendstoD)
+    then obtain d where d: "d>0" "\<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<in> S"
+      unfolding Limits.eventually_at by fast
+    { fix x::"'a" assume "x \<noteq> 0 \<and> dist x 0 < d"
+      hence "f (a + x) \<in> S" using d
+      apply(erule_tac x="x+a" in allE)
+      by(auto simp add: comm_monoid_add.mult_commute dist_norm dist_commute)
     }
-    hence "\<exists>d>0. \<forall>x. 0 < dist x 0 \<and> dist x 0 < d \<longrightarrow> dist (f (a + x)) l < e" using d(1) by auto
+    hence "\<exists>d>0. \<forall>x. x \<noteq> 0 \<and> dist x 0 < d \<longrightarrow> f (a + x) \<in> S"
+      using d(1) by auto
+    hence "eventually (\<lambda>x. f (a + x) \<in> S) (at 0)"
+      unfolding Limits.eventually_at .
   }
-  thus "?rhs" unfolding Lim_at by auto
+  thus "?rhs" by (rule topological_tendstoI)
 next
   assume "?rhs"
-  { fix e::real assume "e>0"
-    with `?rhs` obtain d where d:"d>0" "\<forall>x. 0 < dist x 0 \<and> dist x 0 < d \<longrightarrow> dist (f (a + x)) l < e"
-      unfolding Lim_at by auto
-    { fix x::"'a" assume "0 < dist x a \<and> dist x a < d"
-      hence "dist (f x) l < e" using d apply(erule_tac x="x-a" in allE)
+  { fix S assume "open S" "l \<in> S"
+    with `?rhs` have "eventually (\<lambda>x. f (a + x) \<in> S) (at 0)"
+      by (rule topological_tendstoD)
+    then obtain d where d: "d>0" "\<forall>x. x \<noteq> 0 \<and> dist x 0 < d \<longrightarrow> f (a + x) \<in> S"
+      unfolding Limits.eventually_at by fast
+    { fix x::"'a" assume "x \<noteq> a \<and> dist x a < d"
+      hence "f x \<in> S" using d apply(erule_tac x="x-a" in allE)
 	by(auto simp add: comm_monoid_add.mult_commute dist_norm dist_commute)
     }
-    hence "\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" using d(1) by auto
+    hence "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<in> S" using d(1) by auto
+    hence "eventually (\<lambda>x. f x \<in> S) (at a)" unfolding Limits.eventually_at .
   }
-  thus "?lhs" unfolding Lim_at by auto
+  thus "?lhs" by (rule topological_tendstoI)
 qed
 
 text{* It's also sometimes useful to extract the limit point from the net.  *}
@@ -1594,10 +1604,9 @@
 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_iff
-  apply (clarify, drule spec, drule (1) mp)
+  "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net ==> (g ---> l) net"
+  apply (rule topological_tendstoI)
+  apply (drule (2) topological_tendstoD)
   apply (erule (1) eventually_elim2, simp)
   done
 
@@ -1722,17 +1731,19 @@
   by (metis trans_le_add1 )
 
 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)
+  "(f ---> l) sequentially ==> ((\<lambda>i. f(i - k)) ---> l) sequentially"
+  apply (rule topological_tendstoI)
+  apply (drule (2) topological_tendstoD)
+  apply (simp only: eventually_sequentially)
   apply (subgoal_tac "\<And>N k (n::nat). N + k <= n ==> N <= n - k")
   apply metis
   by arith
 
 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)
+  "((\<lambda>i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially"
+  apply (rule topological_tendstoI)
+  apply (drule (2) topological_tendstoD)
+  apply (simp only: eventually_sequentially)
   apply (subgoal_tac "\<And>N k (n::nat). N + k <= n ==> N <= n - k \<and> (n - k) + k = n")
   by metis arith
 
@@ -1749,7 +1760,7 @@
 text{* More properties of closed balls. *}
 
 lemma closed_cball: "closed (cball x e)"
-unfolding cball_def closed_def Compl_eq_Diff_UNIV [symmetric]
+unfolding cball_def closed_def
 unfolding Collect_neg_eq [symmetric] not_le
 apply (clarsimp simp add: open_dist, rename_tac y)
 apply (rule_tac x="dist x y - e" in exI, clarsimp)
@@ -1781,7 +1792,6 @@
 
 lemma islimpt_ball:
   fixes x y :: "'a::{real_normed_vector,perfect_space}"
-    (* FIXME: generalize to metric_space *)
   shows "y islimpt ball x e \<longleftrightarrow> 0 < e \<and> y \<in> cball x e" (is "?lhs = ?rhs")
 proof
   assume "?lhs"
@@ -1789,7 +1799,7 @@
     hence *:"ball x e = {}" using ball_eq_empty[of x e] by auto
     have False using `?lhs` unfolding * using islimpt_EMPTY[of y] by auto
   }
-  hence "e > 0" by (metis dlo_simps(3))
+  hence "e > 0" by (metis not_less)
   moreover
   have "y \<in> cball x e" using closed_cball[of x e] islimpt_subset[of y "ball x e" "cball x e"] ball_subset_cball[of x e] `?lhs` unfolding closed_limpt by auto
   ultimately show "?rhs" by auto
@@ -1848,12 +1858,56 @@
   thus "?lhs" unfolding mem_cball islimpt_approachable mem_ball by auto
 qed
 
+lemma closure_ball_lemma:
+  fixes x y :: "'a::real_normed_vector"
+  assumes "x \<noteq> y" shows "y islimpt ball x (dist x y)"
+proof (rule islimptI)
+  fix T assume "y \<in> T" "open T"
+  then obtain r where "0 < r" "\<forall>z. dist z y < r \<longrightarrow> z \<in> T"
+    unfolding open_dist by fast
+  (* choose point between x and y, within distance r of y. *)
+  def k \<equiv> "min 1 (r / (2 * dist x y))"
+  def z \<equiv> "y + scaleR k (x - y)"
+  have z_def2: "z = x + scaleR (1 - k) (y - x)"
+    unfolding z_def by (simp add: algebra_simps)
+  have "dist z y < r"
+    unfolding z_def k_def using `0 < r`
+    by (simp add: dist_norm norm_scaleR min_def)
+  hence "z \<in> T" using `\<forall>z. dist z y < r \<longrightarrow> z \<in> T` by simp
+  have "dist x z < dist x y"
+    unfolding z_def2 dist_norm
+    apply (simp add: norm_scaleR norm_minus_commute)
+    apply (simp only: dist_norm [symmetric])
+    apply (subgoal_tac "\<bar>1 - k\<bar> * dist x y < 1 * dist x y", simp)
+    apply (rule mult_strict_right_mono)
+    apply (simp add: k_def divide_pos_pos zero_less_dist_iff `0 < r` `x \<noteq> y`)
+    apply (simp add: zero_less_dist_iff `x \<noteq> y`)
+    done
+  hence "z \<in> ball x (dist x y)" by simp
+  have "z \<noteq> y"
+    unfolding z_def k_def using `x \<noteq> y` `0 < r`
+    by (simp add: min_def)
+  show "\<exists>z\<in>ball x (dist x y). z \<in> T \<and> z \<noteq> y"
+    using `z \<in> ball x (dist x y)` `z \<in> T` `z \<noteq> y`
+    by fast
+qed
+
 lemma closure_ball:
-  fixes x y :: "'a::{real_normed_vector,perfect_space}"
-    (* FIXME: generalize to metric_space *)
-  shows "0 < e ==> (closure(ball x e) = cball x e)"
-  apply (simp add: closure_def islimpt_ball expand_set_eq)
-  by arith
+  fixes x :: "'a::real_normed_vector"
+  shows "0 < e \<Longrightarrow> closure (ball x e) = cball x e"
+apply (rule equalityI)
+apply (rule closure_minimal)
+apply (rule ball_subset_cball)
+apply (rule closed_cball)
+apply (rule subsetI, rename_tac y)
+apply (simp add: le_less [where 'a=real])
+apply (erule disjE)
+apply (rule subsetD [OF closure_subset], simp)
+apply (simp add: closure_def)
+apply clarify
+apply (rule closure_ball_lemma)
+apply (simp add: zero_less_dist_iff)
+done
 
 lemma interior_cball:
   fixes x :: "real ^ _" (* FIXME: generalize *)