# HG changeset patch
# User huffman
# Date 1243662133 25200
# Node ID fa93996e95721559e316070d975e67b209535815
# Parent  80667d5bee32a39b61a360ed9b30293b7fb50d5f
generalize at function to class perfect_space

diff -r 80667d5bee32 -r fa93996e9572 src/HOL/Library/Convex_Euclidean_Space.thy
--- a/src/HOL/Library/Convex_Euclidean_Space.thy	Fri May 29 18:23:07 2009 -0700
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Fri May 29 22:42:13 2009 -0700
@@ -2990,7 +2990,9 @@
 
 subsection {* Special case of straight-line paths. *}
 
-definition "linepath a b = (\<lambda>x. (1 - dest_vec1 x) *s a + dest_vec1 x *s b)"
+definition
+  linepath :: "real ^ 'n::finite \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 1 \<Rightarrow> real ^ 'n" where
+  "linepath a b = (\<lambda>x. (1 - dest_vec1 x) *s a + dest_vec1 x *s b)"
 
 lemma pathstart_linepath[simp]: "pathstart(linepath a b) = a"
   unfolding pathstart_def linepath_def by auto
diff -r 80667d5bee32 -r fa93996e9572 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Fri May 29 18:23:07 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Fri May 29 22:42:13 2009 -0700
@@ -1012,17 +1012,24 @@
 subsection{* Common nets and The "within" modifier for nets. *}
 
 definition
-  at :: "real ^ 'n::finite \<Rightarrow> (real ^ 'n) net" where
+  at :: "'a::perfect_space \<Rightarrow> 'a net" where
   "at a = mknet(\<lambda>x y. 0 < dist x a \<and> dist x a <= dist y a)"
 
-definition "at_infinity = mknet(\<lambda>x y. norm x \<ge> norm y)"
-definition "sequentially = mknet(\<lambda>(m::nat) n. m >= n)"
-
-definition within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70) where
-  within_def: "net within S = mknet (\<lambda>x y. netord net x y \<and> x \<in> S)"
-
-definition indirection :: "real ^'n::finite \<Rightarrow> real ^'n \<Rightarrow> (real ^'n) net" (infixr "indirection" 70) where
-  indirection_def: "a indirection v = (at a) within {b. \<exists>c\<ge>0. b - a = c*s v}"
+definition
+  at_infinity :: "'a::real_normed_vector net" where
+  "at_infinity = mknet (\<lambda>x y. norm x \<ge> norm y)"
+
+definition
+  sequentially :: "nat net" where
+  "sequentially = mknet (\<lambda>m n. n \<le> m)"
+
+definition
+  within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70) where
+  "net within S = mknet (\<lambda>x y. netord net x y \<and> x \<in> S)"
+
+definition
+  indirection :: "real ^'n::finite \<Rightarrow> real ^'n \<Rightarrow> (real ^'n) net" (infixr "indirection" 70) where
+  "a indirection v = (at a) within {b. \<exists>c\<ge>0. b - a = c*s v}"
 
 text{* Prove That They are all nets. *}
 
@@ -1065,19 +1072,22 @@
 lemma in_direction: "netord (a indirection v) x y \<longleftrightarrow> 0 < dist x a \<and> dist x a \<le> dist y a \<and> (\<exists>c \<ge> 0. x - a = c *s v)"
   by (simp add: within at indirection_def)
 
-lemma within_UNIV: "at x within UNIV = at x"
-  by (simp add: within_def at_def netord_inverse)
+lemma within_UNIV: "net within UNIV = net"
+  by (simp add: within_def netord_inverse)
 
 subsection{* Identify Trivial limits, where we can't approach arbitrarily closely. *}
 
-
-definition "trivial_limit (net:: 'a net) \<longleftrightarrow>
-  (\<forall>(a::'a) b. a = b) \<or> (\<exists>(a::'a) b. a \<noteq> b \<and> (\<forall>x. ~(netord (net) x a) \<and> ~(netord(net) x b)))"
-
-
-lemma trivial_limit_within: "trivial_limit (at (a::real^'n::finite) within S) \<longleftrightarrow> ~(a islimpt S)"
+definition
+  trivial_limit :: "'a net \<Rightarrow> bool" where
+  "trivial_limit (net:: 'a net) \<longleftrightarrow>
+    (\<forall>(a::'a) b. a = b) \<or>
+    (\<exists>(a::'a) b. a \<noteq> b \<and> (\<forall>x. ~(netord (net) x a) \<and> ~(netord(net) x b)))"
+
+lemma trivial_limit_within:
+  fixes a :: "'a::perfect_space"
+  shows "trivial_limit (at a within S) \<longleftrightarrow> \<not> a islimpt S"
 proof-
-  {assume "\<forall>(a::real^'n) b. a = b" hence "\<not> a islimpt S"
+  {assume "\<forall>(a::'a) b. a = b" hence "\<not> a islimpt S"
       apply (simp add: islimpt_approachable_le)
       by (rule exI[where x=1], auto)}
   moreover
@@ -1092,30 +1102,35 @@
   {assume "\<not> a islimpt S"
     then obtain e where e: "e > 0" "\<forall>x' \<in> S. x' \<noteq> a \<longrightarrow> dist x' a > e"
       unfolding islimpt_approachable_le by (auto simp add: not_le)
-    from e vector_choose_dist[of e a] obtain b where b: "dist a b = e" by auto
-    from b e(1) have "a \<noteq> b" by (simp add: dist_nz)
+    from e perfect_choose_dist[of e a] obtain b where b: "b \<noteq> a" "dist b a < e" by auto
+    then have "a \<noteq> b" by auto
     moreover have "\<forall>x. \<not> ((0 < dist x a \<and> dist x a \<le> dist a a) \<and> x \<in> S) \<and>
                  \<not> ((0 < dist x a \<and> dist x a \<le> dist b a) \<and> x \<in> S)"
       using e(2) b by (auto simp add: dist_commute)
-    ultimately have "trivial_limit (at a within S)"  unfolding trivial_limit_def within at
+    ultimately have "trivial_limit (at a within S)"
+      unfolding trivial_limit_def within at
       by blast}
   ultimately show ?thesis unfolding trivial_limit_def by blast
 qed
 
-lemma trivial_limit_at: "~(trivial_limit (at a))"
-  apply (subst within_UNIV[symmetric])
-  by (simp add: trivial_limit_within islimpt_UNIV)
-
-lemma trivial_limit_at_infinity: "~(trivial_limit (at_infinity :: ('a::{norm,zero_neq_one}) net))"
+lemma trivial_limit_at: "\<not> trivial_limit (at a)"
+  using trivial_limit_within [of a UNIV]
+  by (simp add: within_UNIV)
+
+lemma trivial_limit_at_infinity:
+  "\<not> trivial_limit (at_infinity :: ('a::{real_normed_vector,zero_neq_one}) net)"
   apply (simp add: trivial_limit_def at_infinity)
   by (metis order_refl zero_neq_one)
 
-lemma trivial_limit_sequentially:  "~(trivial_limit sequentially)"
+lemma trivial_limit_sequentially: "\<not> trivial_limit sequentially"
   by (auto simp add: trivial_limit_def sequentially)
 
 subsection{* Some property holds "sufficiently close" to the limit point. *}
 
-definition "eventually P net \<longleftrightarrow> trivial_limit net \<or> (\<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> P x))"
+definition
+  eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a net \<Rightarrow> bool" where
+  "eventually P net \<longleftrightarrow> trivial_limit net \<or>
+    (\<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> P x))"
 
 lemma eventually_happens: "eventually P net ==> trivial_limit net \<or> (\<exists>x. P x)"
   by (metis eventually_def)
@@ -1141,7 +1156,7 @@
     unfolding eventually_def trivial_limit_within islimpt_approachable_le within at unfolding dist_nz[THEN sym] by (clarsimp, rule_tac x=d in exI, auto)
 qed
 
-lemma eventually_within:  " eventually P (at a within S) \<longleftrightarrow>
+lemma eventually_within: "eventually P (at a within S) \<longleftrightarrow>
         (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
 proof-
   { fix d
@@ -1273,7 +1288,7 @@
 qed
 
 lemma Lim_Un_univ:
- "(f ---> l) (at x within S) \<Longrightarrow> (f ---> l) (at x within T) \<Longrightarrow>  S \<union> T = (UNIV::(real^'n::finite) set)
+ "(f ---> l) (at x within S) \<Longrightarrow> (f ---> l) (at x within T) \<Longrightarrow>  S \<union> T = UNIV
         ==> (f ---> l) (at x)"
   by (metis Lim_Un within_UNIV)
 
@@ -1626,12 +1641,14 @@
 lemma Lim_at_id: "(id ---> a) (at a)"
 apply (subst within_UNIV[symmetric]) by (simp add: Lim_within_id)
 
-lemma Lim_at_zero: "(f ---> l) (at (a::real^'a::finite)) \<longleftrightarrow> ((\<lambda>x. f(a + x)) ---> l) (at 0)" (is "?lhs = ?rhs")
+lemma Lim_at_zero:
+  fixes a :: "'a::{real_normed_vector, perfect_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::"real^'a" assume "0 < dist x 0 \<and> dist x 0 < d"
+    { 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)
     }
@@ -1643,7 +1660,7 @@
   { 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::"real^'a" assume "0 < dist x a \<and> dist x a < d"
+    { 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)
 	by(auto simp add: comm_monoid_add.mult_commute dist_norm dist_commute)
     }
@@ -1669,9 +1686,7 @@
   ultimately show ?thesis unfolding netlimit_def using some_equality[of "\<lambda>x. \<forall>y. \<not> netord (at a within S) y x"] by blast
 qed
 
-lemma netlimit_at:
-  fixes a :: "real ^ 'n::finite"
-  shows "netlimit(at a) = a"
+lemma netlimit_at: "netlimit (at a) = a"
   apply (subst within_UNIV[symmetric])
   using netlimit_within[of a UNIV]
   by (simp add: trivial_limit_at within_UNIV)
@@ -1689,12 +1704,13 @@
 
 lemma Lim_transform_eventually:
   fixes f g :: "'a::type \<Rightarrow> 'b::real_normed_vector"
+    (* FIXME: generalize to metric_space *)
   shows "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net ==> (g ---> l) net"
   using Lim_eventually[of "\<lambda>x. f x - g x" 0 net] Lim_transform[of f g net l] by auto
 
 lemma Lim_transform_within:
-  fixes f g :: "real ^ 'n::finite \<Rightarrow> 'b::real_normed_vector"
-  fixes x :: "real ^ 'n::finite"
+  fixes f g :: "'a::perfect_space \<Rightarrow> 'b::real_normed_vector"
+    (* FIXME: generalize to metric_space *)
   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)"
@@ -1704,7 +1720,8 @@
 qed
 
 lemma Lim_transform_at:
-  fixes f g :: "real ^ 'n::finite \<Rightarrow> 'b::real_normed_vector"
+  fixes f g :: "'a::perfect_space \<Rightarrow> 'b::real_normed_vector"
+    (* FIXME: generalize to metric_space *)
   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])
@@ -1714,7 +1731,8 @@
 text{* Common case assuming being away from some crucial point like 0. *}
 
 lemma Lim_transform_away_within:
-  fixes f:: "real ^'m::finite \<Rightarrow> 'b::real_normed_vector"
+  fixes f:: "'a::perfect_space \<Rightarrow> 'b::real_normed_vector"
+    (* FIXME: generalize to 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)"
@@ -1725,7 +1743,8 @@
 qed
 
 lemma Lim_transform_away_at:
-  fixes f:: "real ^'m::finite \<Rightarrow> 'b::real_normed_vector"
+  fixes f:: "'a::perfect_space \<Rightarrow> 'b::real_normed_vector"
+    (* FIXME: generalize to 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)"
@@ -1735,7 +1754,8 @@
 text{* Alternatively, within an open set. *}
 
 lemma Lim_transform_within_open:
-  fixes f:: "real ^'m::finite \<Rightarrow> 'b::real_normed_vector"
+  fixes f:: "'a::perfect_space \<Rightarrow> 'b::real_normed_vector"
+    (* FIXME: generalize to 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-
@@ -2025,7 +2045,10 @@
 lemma lim_within_interior: "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: assumes "x \<in> interior S"
+lemma netlimit_within_interior:
+  fixes x :: "'a::{perfect_space, real_normed_vector}"
+    (* FIXME: generalize to perfect_space *)
+  assumes "x \<in> interior S"
   shows "netlimit(at x within S) = x" (is "?lhs = ?rhs")
 proof-
   from assms obtain e::real where e:"e>0" "ball x e \<subseteq> S" using open_interior[of S] unfolding open_contains_ball using interior_subset[of S] by auto
@@ -3027,8 +3050,8 @@
   unfolding eventually_def
   by (cases "trivial_limit (at x within s)") auto
 
-lemma continuous_at: "continuous (at x) f \<longleftrightarrow> (f ---> f(x)) (at x)" using within_UNIV[of x]
-  using continuous_within[of x UNIV f] by auto
+lemma continuous_at: "continuous (at x) f \<longleftrightarrow> (f ---> f(x)) (at x)"
+  using continuous_within [of x UNIV f] by (simp add: within_UNIV)
 
 lemma continuous_at_within:
   assumes "continuous (at x) f"  shows "continuous (at x within s) f"
@@ -3074,8 +3097,8 @@
     apply (auto simp add: dist_commute) apply(erule_tac x=e in allE) by auto
 qed
 
-lemma continuous_at_ball: fixes f::"real^'a::finite \<Rightarrow> real^'a"
-  shows "continuous (at x) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. f ` (ball x d) \<subseteq> ball (f x) e)" (is "?lhs = ?rhs")
+lemma continuous_at_ball:
+  "continuous (at x) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. f ` (ball x d) \<subseteq> ball (f x) e)" (is "?lhs = ?rhs")
 proof
   assume ?lhs thus ?rhs unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball
     apply auto apply(erule_tac x=e in allE) apply auto apply(rule_tac x=d in exI) apply auto apply(erule_tac x=xa in allE) apply (auto simp add: dist_commute dist_nz)
@@ -3177,7 +3200,7 @@
                      --> ((f o x) ---> f a) sequentially)" (is "?lhs = ?rhs")
 proof
   assume ?lhs
-  { fix x::"nat \<Rightarrow> real^'a" assume x:"\<forall>n. x n \<in> s" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (x n) a < e"
+  { fix x::"nat \<Rightarrow> 'a" assume x:"\<forall>n. x n \<in> s" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (x n) a < e"
     fix e::real assume "e>0"
     from `?lhs` obtain d where "d>0" and d:"\<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) (f a) < e" unfolding continuous_within Lim_within using `e>0` by auto
     from x(2) `d>0` obtain N where N:"\<forall>n\<ge>N. dist (x n) a < d" by auto
@@ -3874,12 +3897,14 @@
 qed
 
 lemma linear_continuous_at:
+  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
   assumes "linear f"  shows "continuous (at a) f"
   unfolding continuous_at Lim_at_zero[of f "f a" a] using linear_lim_0[OF assms]
   unfolding Lim_null[of "\<lambda>x. f (a + x)"] unfolding linear_sub[OF assms, THEN sym] by auto
 
 lemma linear_continuous_within:
- "linear f ==> continuous (at x within s) f"
+  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
+  shows "linear f ==> continuous (at x within s) f"
   using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto
 
 lemma linear_continuous_on:
@@ -3942,7 +3967,8 @@
   unfolding continuous_on_def apply (simp del: dist_commute) unfolding dist_vec1 unfolding dist_norm ..
 
 lemma continuous_at_vec1_norm:
- "continuous (at x) (vec1 o norm)"
+  fixes x :: "real ^ _"
+  shows "continuous (at x) (vec1 o norm)"
   unfolding continuous_at_vec1_range using real_abs_sub_norm order_le_less_trans by blast
 
 lemma continuous_on_vec1_norm:
@@ -4152,7 +4178,7 @@
   fixes f :: "real ^ _ \<Rightarrow> real"
   shows "continuous (at a) (vec1 o f) \<Longrightarrow> f a \<noteq> 0
          ==> continuous (at a) (vec1 o inverse o f) "
-  using within_UNIV[THEN sym, of a] using continuous_at_within_inv[of a UNIV] by auto
+  using within_UNIV[THEN sym, of "at a"] using continuous_at_within_inv[of a UNIV] by auto
 
 subsection{* Preservation properties for pasted sets.                                  *}
 
@@ -4962,7 +4988,8 @@
 qed
 
 lemma continuous_at_vec1_dot:
- "continuous (at x) (vec1 o (\<lambda>y. a \<bullet> y))"
+  fixes x :: "real ^ _"
+  shows "continuous (at x) (vec1 o (\<lambda>y. a \<bullet> y))"
 proof-
   have "((\<lambda>x. x) ---> x) (at x)" unfolding Lim_at by auto
   thus ?thesis unfolding continuous_at and o_def using Lim_vec1_dot[of "\<lambda>x. x" x "at x" a] by auto