author huffman Sat, 13 Jun 2009 08:18:14 -0700 changeset 31655 bcb1eb2197f8 parent 31654 83662a8604c2 child 31656 abadaf4922f8
generalize constants netlimit and continuous
```--- 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: 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 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)

-  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)"

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```