# HG changeset patch
# User huffman
# Date 1244906294 25200
# Node ID bcb1eb2197f8bf7570d0212f1fed3958de051577
# Parent  83662a8604c274aecfdf025cc13de2e0c43de4e3
generalize constants netlimit and continuous

diff -r 83662a8604c2 -r bcb1eb2197f8 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Sat Jun 13 07:33:50 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Sat Jun 13 08:18:14 2009 -0700
@@ -1492,29 +1492,19 @@
 text{* It's also sometimes useful to extract the limit point from the net.  *}
 
 definition
-  netlimit :: "'a::metric_space net \<Rightarrow> 'a" where
-  "netlimit net = (SOME a. \<forall>r>0. eventually (\<lambda>x. dist x a < r) net)"
+  netlimit :: "'a::t2_space net \<Rightarrow> 'a" where
+  "netlimit net = (SOME a. ((\<lambda>x. x) ---> a) net)"
 
 lemma netlimit_within:
   assumes "\<not> trivial_limit (at a within S)"
   shows "netlimit (at a within S) = a"
-using assms
-apply (simp add: trivial_limit_within)
-apply (simp add: netlimit_def eventually_within zero_less_dist_iff)
-apply (rule some_equality, fast)
-apply (rename_tac b)
-apply (rule ccontr)
-apply (drule_tac x="dist b a / 2" in spec, drule mp, simp add: dist_nz)
-apply (clarify, rename_tac r)
-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)
-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)
-apply simp
+unfolding netlimit_def
+apply (rule some_equality)
+apply (rule Lim_at_within)
+apply (rule Lim_ident_at)
+apply (erule Lim_unique [OF assms])
+apply (rule Lim_at_within)
+apply (rule Lim_ident_at)
 done
 
 lemma netlimit_at:
@@ -3144,17 +3134,16 @@
 subsection{* Define continuity over a net to take in restrictions of the set. *}
 
 definition
-  continuous :: "'a::metric_space net \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> bool" where
+  continuous :: "'a::t2_space net \<Rightarrow> ('a \<Rightarrow> 'b::topological_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_iff trivial_limit_eq by auto
+  unfolding continuous_def tendsto_def 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_iff
+  unfolding tendsto_def
   using netlimit_within[of x s]
   by (cases "trivial_limit (at x within s)") (auto simp add: trivial_limit_eventually)
 
@@ -3162,17 +3151,9 @@
   using continuous_within [of x UNIV f] by (simp add: within_UNIV)
 
 lemma continuous_at_within:
-  fixes x :: "'a::perfect_space"
   assumes "continuous (at x) f"  shows "continuous (at x within s) f"
-  (* 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" "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
-    unfolding Lim and trivial_limit_within by auto
-qed
+  using assms unfolding continuous_at continuous_within
+  by (rule Lim_at_within)
 
 text{* Derive the epsilon-delta forms, which we often use as "definitions" *}
 
@@ -3304,8 +3285,10 @@
 
 text{* Characterization of various kinds of continuity in terms of sequences.  *}
 
+(* \<longrightarrow> could be generalized, but \<longleftarrow> requires metric space *)
 lemma continuous_within_sequentially:
- "continuous (at a within s) f \<longleftrightarrow>
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  shows "continuous (at a within s) f \<longleftrightarrow>
                 (\<forall>x. (\<forall>n::nat. x n \<in> s) \<and> (x ---> a) sequentially
                      --> ((f o x) ---> f a) sequentially)" (is "?lhs = ?rhs")
 proof
@@ -3345,7 +3328,8 @@
 qed
 
 lemma continuous_at_sequentially:
- "continuous (at a) f \<longleftrightarrow> (\<forall>x. (x ---> a) sequentially
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  shows "continuous (at a) f \<longleftrightarrow> (\<forall>x. (x ---> a) sequentially
                   --> ((f o x) ---> f a) sequentially)"
   using continuous_within_sequentially[of a UNIV f] unfolding within_UNIV by auto
 
@@ -3445,22 +3429,22 @@
   by (auto simp add: continuous_def Lim_const)
 
 lemma continuous_cmul:
-  fixes f :: "'a::metric_space \<Rightarrow> real ^ 'n::finite"
+  fixes f :: "'a::t2_space \<Rightarrow> real ^ 'n::finite"
   shows "continuous net f ==> continuous net (\<lambda>x. c *\<^sub>R f x)"
   by (auto simp add: continuous_def Lim_cmul)
 
 lemma continuous_neg:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   shows "continuous net f ==> continuous net (\<lambda>x. -(f x))"
   by (auto simp add: continuous_def Lim_neg)
 
 lemma continuous_add:
-  fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   shows "continuous net f \<Longrightarrow> continuous net g \<Longrightarrow> continuous net (\<lambda>x. f x + g x)"
   by (auto simp add: continuous_def Lim_add)
 
 lemma continuous_sub:
-  fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   shows "continuous net f \<Longrightarrow> continuous net g \<Longrightarrow> continuous net (\<lambda>x. f x - g x)"
   by (auto simp add: continuous_def Lim_sub)
 
@@ -3547,11 +3531,11 @@
 
 lemma continuous_within_id:
  "continuous (at a within s) (\<lambda>x. x)"
-  unfolding continuous_within Lim_within by auto
+  unfolding continuous_within by (rule Lim_at_within [OF Lim_ident_at])
 
 lemma continuous_at_id:
  "continuous (at a) (\<lambda>x. x)"
-  unfolding continuous_at Lim_at by auto
+  unfolding continuous_at by (rule Lim_ident_at)
 
 lemma continuous_on_id:
  "continuous_on s (\<lambda>x. x)"
@@ -3564,6 +3548,8 @@
 text{* Continuity of all kinds is preserved under composition. *}
 
 lemma continuous_within_compose:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
+  fixes g :: "'b::metric_space \<Rightarrow> 'c::metric_space"
   assumes "continuous (at x within s) f"   "continuous (at (f x) within f ` s) g"
   shows "continuous (at x within s) (g o f)"
 proof-
@@ -3578,6 +3564,8 @@
 qed
 
 lemma continuous_at_compose:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
+  fixes g :: "'b::metric_space \<Rightarrow> 'c::metric_space"
   assumes "continuous (at x) f"  "continuous (at (f x)) g"
   shows "continuous (at x) (g o f)"
 proof-
@@ -3603,7 +3591,8 @@
 text{* Continuity in terms of open preimages. *}
 
 lemma continuous_at_open:
- "continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t --> (\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x' \<in> s. (f x') \<in> t)))" (is "?lhs = ?rhs")
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
+  shows "continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t --> (\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x' \<in> s. (f x') \<in> t)))" (is "?lhs = ?rhs")
 proof
   assume ?lhs
   { fix t assume as: "open t" "f x \<in> t"
@@ -3732,11 +3721,13 @@
 qed
 
 lemma continuous_open_preimage_univ:
-  "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open {x. f x \<in> s}"
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
+  shows "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open {x. f x \<in> s}"
   using continuous_open_preimage[of UNIV f s] open_UNIV continuous_at_imp_continuous_on by auto
 
 lemma continuous_closed_preimage_univ:
-  "(\<forall>x. continuous (at x) f) \<Longrightarrow> closed s ==> closed {x. f x \<in> s}"
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
+  shows "(\<forall>x. continuous (at x) f) \<Longrightarrow> closed s ==> closed {x. f x \<in> s}"
   using continuous_closed_preimage[of UNIV f s] closed_UNIV continuous_at_imp_continuous_on by auto
 
 text{* Equality of continuous functions on closure and related results.          *}
@@ -3782,6 +3773,7 @@
 text{* Making a continuous function avoid some value in a neighbourhood.         *}
 
 lemma continuous_within_avoid:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
   assumes "continuous (at x within s) f"  "x \<in> s"  "f x \<noteq> a"
   shows "\<exists>e>0. \<forall>y \<in> s. dist x y < e --> f y \<noteq> a"
 proof-
@@ -3794,6 +3786,7 @@
 qed
 
 lemma continuous_at_avoid:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
   assumes "continuous (at x) f"  "f x \<noteq> a"
   shows "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> f y \<noteq> a"
 using assms using continuous_within_avoid[of x UNIV f a, unfolded within_UNIV] by auto