# HG changeset patch
# User huffman
# Date 1244774679 25200
# Node ID 784decc70e07679eb90082dec396b8ebe91bf77d
# Parent  f11a849bab610d0b562d085602c97b090c5b2912
generalize lemma edelstein_fix

diff -r f11a849bab61 -r 784decc70e07 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Thu Jun 11 19:23:56 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Thu Jun 11 19:44:39 2009 -0700
@@ -5945,9 +5945,10 @@
 subsection{* Edelstein fixed point theorem.                                            *}
 
 lemma edelstein_fix:
+  fixes s :: "'a::{heine_borel, real_normed_vector} set"
   assumes s:"compact s" "s \<noteq> {}" and gs:"(g ` s) \<subseteq> s"
       and dist:"\<forall>x\<in>s. \<forall>y\<in>s. x \<noteq> y \<longrightarrow> dist (g x) (g y) < dist x y"
-  shows "\<exists>! x::real^'a::finite\<in>s. g x = x"
+  shows "\<exists>! x\<in>s. g x = x"
 proof(cases "\<exists>x\<in>s. g x \<noteq> x")
   obtain x where "x\<in>s" using s(2) by auto
   case False hence g:"\<forall>x\<in>s. g x = x" by auto
@@ -5990,26 +5991,23 @@
       qed
     qed } note distf = this
 
-  def h \<equiv> "\<lambda>n. pastecart (f n x) (f n y)"
-  let ?s2 = "{pastecart x y |x y. x \<in> s \<and> y \<in> s}"
+  def h \<equiv> "\<lambda>n. (f n x, f n y)"
+  let ?s2 = "s \<times> s"
   obtain l r where "l\<in>?s2" and r:"subseq r" and lr:"((h \<circ> r) ---> l) sequentially"
-    using compact_pastecart[OF s(1) s(1), unfolded compact_def, THEN spec[where x=h]] unfolding  h_def
+    using compact_Times [OF s(1) s(1), unfolded compact_def, THEN spec[where x=h]] unfolding  h_def
     using fs[OF `x\<in>s`] and fs[OF `y\<in>s`] by blast
-  def a \<equiv> "fstcart l" def b \<equiv> "sndcart l"
-  have lab:"l = pastecart a b" unfolding a_def b_def and pastecart_fst_snd by simp
+  def a \<equiv> "fst l" def b \<equiv> "snd l"
+  have lab:"l = (a, b)" unfolding a_def b_def by simp
   have [simp]:"a\<in>s" "b\<in>s" unfolding a_def b_def using `l\<in>?s2` by auto
 
-  have "continuous_on (UNIV :: (real ^ _) set) fstcart"
-   and "continuous_on (UNIV :: (real ^ _) set) sndcart"
-    using linear_continuous_on using linear_fstcart and linear_sndcart by auto
-  hence lima:"((fstcart \<circ> (h \<circ> r)) ---> a) sequentially" and limb:"((sndcart \<circ> (h \<circ> r)) ---> b) sequentially"
-    unfolding atomize_conj unfolding continuous_on_sequentially
-    apply(erule_tac x="h \<circ> r" in allE) apply(erule_tac x="h \<circ> r" in allE) using lr
-    unfolding o_def and h_def a_def b_def  by auto
+  have lima:"((fst \<circ> (h \<circ> r)) ---> a) sequentially"
+   and limb:"((snd \<circ> (h \<circ> r)) ---> b) sequentially"
+    using lr
+    unfolding o_def a_def b_def by (simp_all add: tendsto_intros)
 
   { fix n::nat
-    have *:"\<And>fx fy (x::real^_) y. dist fx fy \<le> dist x y \<Longrightarrow> \<not> (dist (fx - fy) (a - b) < dist a b - dist x y)" unfolding dist_norm by norm
-    { fix x y ::"real^'a"
+    have *:"\<And>fx fy (x::'a) y. dist fx fy \<le> dist x y \<Longrightarrow> \<not> (dist (fx - fy) (a - b) < dist a b - dist x y)" unfolding dist_norm by norm
+    { fix x y :: 'a
       have "dist (-x) (-y) = dist x y" unfolding dist_norm
 	using norm_minus_cancel[of "x - y"] by (auto simp add: uminus_add_conv_diff) } note ** = this
 
@@ -6054,8 +6052,8 @@
     have "dist y x < e \<longrightarrow> dist (g y) (g x) < e" using dist by fastsimp }
   hence "continuous_on s g" unfolding continuous_on_def by auto
 
-  hence "((sndcart \<circ> h \<circ> r) ---> g a) sequentially" unfolding continuous_on_sequentially
-    apply (rule allE[where x="\<lambda>n. (fstcart \<circ> h \<circ> r) n"]) apply (erule ballE[where x=a])
+  hence "((snd \<circ> h \<circ> r) ---> g a) sequentially" unfolding continuous_on_sequentially
+    apply (rule allE[where x="\<lambda>n. (fst \<circ> h \<circ> r) n"]) apply (erule ballE[where x=a])
     using lima unfolding h_def o_def using fs[OF `x\<in>s`] by (auto simp add: y_def)
   hence "g a = a" using Lim_unique[OF trivial_limit_sequentially limb, of "g a"]
     unfolding `a=b` and o_assoc by auto