# HG changeset patch
# User huffman
# Date 1273024518 25200
# Node ID 21404f7dec597b116e360e5af3e928c0bed614bb
# Parent  1ea81fc5227a1524dd71b3fa8a5312f4e59fd290
generalize some lemmas

diff -r 1ea81fc5227a -r 21404f7dec59 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue May 04 17:37:31 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue May 04 18:55:18 2010 -0700
@@ -1200,7 +1200,7 @@
 text{* Another limit point characterization. *}
 
 lemma islimpt_sequential:
-  fixes x :: "'a::metric_space" (* FIXME: generalize to topological_space *)
+  fixes x :: "'a::metric_space"
   shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S -{x}) \<and> (f ---> x) sequentially)"
     (is "?lhs = ?rhs")
 proof
@@ -1537,40 +1537,41 @@
 qed
 
 lemma Lim_transform_eventually:
-  "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net ==> (g ---> l) net"
+  "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net \<Longrightarrow> (g ---> l) net"
   apply (rule topological_tendstoI)
   apply (drule (2) topological_tendstoD)
   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)"
-  using assms(1,3) unfolding Lim_within
-  apply -
-  apply (clarify, rename_tac e)
-  apply (drule_tac x=e in spec, clarsimp, rename_tac r)
-  apply (rule_tac x="min d r" in exI, clarsimp, rename_tac y)
-  apply (drule_tac x=y in bspec, assumption, clarsimp)
-  apply (simp add: assms(2))
-  done
+  assumes "0 < d" and "\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
+  and "(f ---> l) (at x within S)"
+  shows "(g ---> l) (at x within S)"
+proof (rule Lim_transform_eventually)
+  show "eventually (\<lambda>x. f x = g x) (at x within S)"
+    unfolding eventually_within
+    using assms(1,2) by auto
+  show "(f ---> l) (at x within S)" by fact
+qed
 
 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])
-  using Lim_transform_within[of d UNIV x f g l]
-  by (auto simp add: within_UNIV)
+  assumes "0 < d" and "\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
+  and "(f ---> l) (at x)"
+  shows "(g ---> l) (at x)"
+proof (rule Lim_transform_eventually)
+  show "eventually (\<lambda>x. f x = g x) (at x)"
+    unfolding eventually_at
+    using assms(1,2) by auto
+  show "(f ---> l) (at x)" by fact
+qed
 
 text{* Common case assuming being away from some crucial point like 0. *}
 
+text {* TODO: generalize the next few lemmas to T1 spaces. *}
+
 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"
+  assumes "a \<noteq> b" and "\<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)"
 proof-
@@ -1581,7 +1582,6 @@
 
 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)"
@@ -1591,15 +1591,14 @@
 text{* Alternatively, within an open set. *}
 
 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)"
+  assumes "open S" and "a \<in> S" and "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x"
+  and "(f ---> l) (at a)"
   shows "(g ---> l) (at a)"
-proof-
-  from assms(1,2) obtain e::real where "e>0" and e:"ball a e \<subseteq> S" unfolding open_contains_ball by auto
-  hence "\<forall>x'. 0 < dist x' a \<and> dist x' a < e \<longrightarrow> f x' = g x'" using assms(3)
-    unfolding ball_def subset_eq apply auto apply(erule_tac x=x' in allE) apply(erule_tac x=x' in ballE) by(auto simp add: dist_commute)
-  thus ?thesis using Lim_transform_at[of e a f g l] `e>0` assms(4) by auto
+proof (rule Lim_transform_eventually)
+  show "eventually (\<lambda>x. f x = g x) (at a)"
+    unfolding eventually_at_topological
+    using assms(1,2,3) by auto
+  show "(f ---> l) (at a)" by fact
 qed
 
 text{* A congruence rule allowing us to transform limits assuming not at point. *}
@@ -1607,21 +1606,21 @@
 (* FIXME: Only one congruence rule for tendsto can be used at a time! *)
 
 lemma Lim_cong_within(*[cong add]*):
-  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"
-  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])
+  assumes "\<And>x. x \<noteq> a \<Longrightarrow> f x = g x"
+  shows "((\<lambda>x. f x) ---> l) (at a within S) \<longleftrightarrow> ((g ---> l) (at a within S))"
+  unfolding tendsto_def Limits.eventually_within eventually_at_topological
+  using assms by simp
+
+lemma Lim_cong_at(*[cong add]*):
+  assumes "\<And>x. x \<noteq> a \<Longrightarrow> f x = g x"
+  shows "((\<lambda>x. f x) ---> l) (at a) \<longleftrightarrow> ((g ---> l) (at a))"
+  unfolding tendsto_def eventually_at_topological
+  using assms by simp
 
 text{* Useful lemmas on closure and set of possible sequential limits.*}
 
 lemma closure_sequential:
-  fixes l :: "'a::metric_space" (* TODO: generalize *)
+  fixes l :: "'a::metric_space"
   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
@@ -2911,7 +2910,7 @@
 qed
 
 lemma closed_sing [simp]:
-  fixes a :: "'a::metric_space"
+  fixes a :: "'a::metric_space" (* TODO: generalize to t1_space *)
   shows "closed {a}"
   apply (clarsimp simp add: closed_def open_dist)
   apply (rule ccontr)
@@ -3252,7 +3251,7 @@
       by (rule Lim_trivial_limit)
   next
     case False
-    hence "netlimit (at x) = x"
+    hence 1: "netlimit (at x) = x"
       using netlimit_within [of x UNIV]
       by (simp add: within_UNIV)
     with * show ?thesis by simp
@@ -3411,38 +3410,28 @@
 text{* The usual transformation theorems. *}
 
 lemma continuous_transform_within:
-  fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+  fixes f g :: "'a::metric_space \<Rightarrow> 'b::topological_space"
   assumes "0 < d" "x \<in> s" "\<forall>x' \<in> s. dist x' x < d --> f x' = g x'"
           "continuous (at x within s) f"
   shows "continuous (at x within s) g"
-proof-
-  { fix e::real assume "e>0"
-    then obtain d' where d':"d'>0" "\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d' \<longrightarrow> dist (f xa) (f x) < e" using assms(4) unfolding continuous_within Lim_within by auto
-    { fix x' assume "x'\<in>s" "0 < dist x' x" "dist x' x < (min d d')"
-      hence "dist (f x') (g x) < e" using assms(2,3) apply(erule_tac x=x in ballE) using d' by auto  }
-    hence "\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < (min d d') \<longrightarrow> dist (f xa) (g x) < e" by blast
-    hence "\<exists>d>0. \<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (g x) < e" using `d>0` `d'>0` by(rule_tac x="min d d'" in exI)auto  }
-  hence "(f ---> g x) (at x within s)" unfolding Lim_within using assms(1) by auto
-  thus ?thesis unfolding continuous_within using Lim_transform_within[of d s x f g "g x"] using assms by blast
+unfolding continuous_within
+proof (rule Lim_transform_within)
+  show "0 < d" by fact
+  show "\<forall>x'\<in>s. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
+    using assms(3) by auto
+  have "f x = g x"
+    using assms(1,2,3) by auto
+  thus "(f ---> g x) (at x within s)"
+    using assms(4) unfolding continuous_within by simp
 qed
 
 lemma continuous_transform_at:
-  fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+  fixes f g :: "'a::metric_space \<Rightarrow> 'b::topological_space"
   assumes "0 < d" "\<forall>x'. dist x' x < d --> f x' = g x'"
           "continuous (at x) f"
   shows "continuous (at x) g"
-proof-
-  { fix e::real assume "e>0"
-    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" using assms(3) unfolding continuous_at Lim_at by auto
-    { fix x' assume "0 < dist x' x" "dist x' x < (min d d')"
-      hence "dist (f x') (g x) < e" using assms(2) apply(erule_tac x=x in allE) using d' by auto
-    }
-    hence "\<forall>xa. 0 < dist xa x \<and> dist xa x < (min d d') \<longrightarrow> dist (f xa) (g x) < e" by blast
-    hence "\<exists>d>0. \<forall>xa. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (g x) < e" using `d>0` `d'>0` by(rule_tac x="min d d'" in exI)auto
-  }
-  hence "(f ---> g x) (at x)" unfolding Lim_at using assms(1) by auto
-  thus ?thesis unfolding continuous_at using Lim_transform_at[of d x f g "g x"] using assms by blast
-qed
+  using continuous_transform_within [of d x UNIV f g] assms
+  by (simp add: within_UNIV)
 
 text{* Combination results for pointwise continuity. *}