# HG changeset patch
# User hoelzl
# Date 1362494598 -3600
# Node ID f8a00792fbc1c874e81a7266ef07b6214f0c04ab
# Parent  d33de22432e2c76b8470b676b242c962d993f786
tuned proof of Edelstein fixed point theorem (use continuity of dist and attains_sup)

diff -r d33de22432e2 -r f8a00792fbc1 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 05 15:43:17 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 05 15:43:18 2013 +0100
@@ -6569,129 +6569,37 @@
   fixes s :: "'a::metric_space 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\<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
-  { fix y assume "y\<in>s"
-    hence "x = y" using `x\<in>s` and dist[THEN bspec[where x=x], THEN bspec[where x=y]]
-      unfolding g[THEN bspec[where x=x], OF `x\<in>s`]
-      unfolding g[THEN bspec[where x=y], OF `y\<in>s`] by auto  }
-  thus ?thesis using `x\<in>s` and g by blast+
-next
-  case True
-  then obtain x where [simp]:"x\<in>s" and "g x \<noteq> x" by auto
-  { fix x y assume "x \<in> s" "y \<in> s"
-    hence "dist (g x) (g y) \<le> dist x y"
-      using dist[THEN bspec[where x=x], THEN bspec[where x=y]] by auto } note dist' = this
-  def y \<equiv> "g x"
-  have [simp]:"y\<in>s" unfolding y_def using gs[unfolded image_subset_iff] and `x\<in>s` by blast
-  def f \<equiv> "\<lambda>n. g ^^ n"
-  have [simp]:"\<And>n z. g (f n z) = f (Suc n) z" unfolding f_def by auto
-  have [simp]:"\<And>z. f 0 z = z" unfolding f_def by auto
-  { fix n::nat and z assume "z\<in>s"
-    have "f n z \<in> s" unfolding f_def
-    proof(induct n)
-      case 0 thus ?case using `z\<in>s` by simp
-    next
-      case (Suc n) thus ?case using gs[unfolded image_subset_iff] by auto
-    qed } note fs = this
-  { fix m n ::nat assume "m\<le>n"
-    fix w z assume "w\<in>s" "z\<in>s"
-    have "dist (f n w) (f n z) \<le> dist (f m w) (f m z)" using `m\<le>n`
-    proof(induct n)
-      case 0 thus ?case by auto
-    next
-      case (Suc n)
-      thus ?case proof(cases "m\<le>n")
-        case True thus ?thesis using Suc(1)
-          using dist'[OF fs fs, OF `w\<in>s` `z\<in>s`, of n n] by auto
-      next
-        case False hence mn:"m = Suc n" using Suc(2) by simp
-        show ?thesis unfolding mn  by auto
-      qed
-    qed } note distf = this
-
-  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_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> "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 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 (rule tendsto_intros)+
-
-  { fix n::nat
-    have *:"\<And>fx fy (x::'a) y. dist fx fy \<le> dist x y \<Longrightarrow> \<not> (\<bar>dist fx fy - dist a b\<bar> < dist a b - dist x y)" by auto
-
-    { assume as:"dist a b > dist (f n x) (f n y)"
-      then obtain Na Nb where "\<forall>m\<ge>Na. dist (f (r m) x) a < (dist a b - dist (f n x) (f n y)) / 2"
-        and "\<forall>m\<ge>Nb. dist (f (r m) y) b < (dist a b - dist (f n x) (f n y)) / 2"
-        using lima limb unfolding h_def LIMSEQ_def by (fastforce simp del: less_divide_eq_numeral1)
-      hence "\<bar>dist (f (r (Na + Nb + n)) x) (f (r (Na + Nb + n)) y) - dist a b\<bar> < dist a b - dist (f n x) (f n y)"
-        apply -
-        apply (drule_tac x="Na+Nb+n" in spec, drule mp, simp)
-        apply (drule_tac x="Na+Nb+n" in spec, drule mp, simp)
-        apply (drule (1) add_strict_mono, simp only: real_sum_of_halves)
-        apply (erule le_less_trans [rotated])
-        apply (erule thin_rl)
-        apply (rule abs_leI)
-        apply (simp add: diff_le_iff add_assoc)
-        apply (rule order_trans [OF dist_triangle add_left_mono])
-        apply (subst add_commute, rule dist_triangle2)
-        apply (simp add: diff_le_iff add_assoc)
-        apply (rule order_trans [OF dist_triangle3 add_left_mono])
-        apply (subst add_commute, rule dist_triangle)
-        done
-      moreover
-      have "\<bar>dist (f (r (Na + Nb + n)) x) (f (r (Na + Nb + n)) y) - dist a b\<bar> \<ge> dist a b - dist (f n x) (f n y)"
-        using distf[of n "r (Na+Nb+n)", OF _ `x\<in>s` `y\<in>s`]
-        using seq_suble[OF r, of "Na+Nb+n"]
-        using *[of "f (r (Na + Nb + n)) x" "f (r (Na + Nb + n)) y" "f n x" "f n y"] by auto
-      ultimately have False by simp
-    }
-    hence "dist a b \<le> dist (f n x) (f n y)" by(rule ccontr)auto }
-  note ab_fn = this
-
-  have [simp]:"a = b" proof(rule ccontr)
-    def e \<equiv> "dist a b - dist (g a) (g b)"
-    assume "a\<noteq>b" hence "e > 0" unfolding e_def using dist by fastforce
-    hence "\<exists>n. dist (f n x) a < e/2 \<and> dist (f n y) b < e/2"
-      using lima limb unfolding LIMSEQ_def
-      apply (auto elim!: allE[where x="e/2"]) apply(rename_tac N N', rule_tac x="r (max N N')" in exI) unfolding h_def by fastforce
-    then obtain n where n:"dist (f n x) a < e/2 \<and> dist (f n y) b < e/2" by auto
-    have "dist (f (Suc n) x) (g a) \<le> dist (f n x) a"
-      using dist[THEN bspec[where x="f n x"], THEN bspec[where x="a"]] and fs by auto
-    moreover have "dist (f (Suc n) y) (g b) \<le> dist (f n y) b"
-      using dist[THEN bspec[where x="f n y"], THEN bspec[where x="b"]] and fs by auto
-    ultimately have "dist (f (Suc n) x) (g a) + dist (f (Suc n) y) (g b) < e" using n by auto
-    thus False unfolding e_def using ab_fn[of "Suc n"]
-      using dist_triangle2 [of "f (Suc n) y" "g a" "g b"]
-      using dist_triangle2 [of "f (Suc n) x" "f (Suc n) y" "g a"]
-      by auto
+  shows "\<exists>!x\<in>s. g x = x"
+proof -
+  let ?D = "(\<lambda>x. (x, x)) ` s"
+  have D: "compact ?D" "?D \<noteq> {}"
+    by (rule compact_continuous_image)
+       (auto intro!: s continuous_Pair continuous_within_id simp: continuous_on_eq_continuous_within)
+
+  have "\<And>x y e. x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> 0 < e \<Longrightarrow> dist y x < e \<Longrightarrow> dist (g y) (g x) < e"
+    using dist by fastforce
+  then have "continuous_on s g"
+    unfolding continuous_on_iff by auto
+  then have cont: "continuous_on ?D (\<lambda>x. dist ((g \<circ> fst) x) (snd x))"
+    unfolding continuous_on_eq_continuous_within
+    by (intro continuous_dist ballI continuous_within_compose)
+       (auto intro!:  continuous_fst continuous_snd continuous_within_id simp: image_image)
+
+  obtain a where "a \<in> s" and le: "\<And>x. x \<in> s \<Longrightarrow> dist (g a) a \<le> dist (g x) x"
+    using continuous_attains_inf[OF D cont] by auto
+
+  have "g a = a"
+  proof (rule ccontr)
+    assume "g a \<noteq> a"
+    with `a \<in> s` gs have "dist (g (g a)) (g a) < dist (g a) a"
+      by (intro dist[rule_format]) auto
+    moreover have "dist (g a) a \<le> dist (g (g a)) (g a)"
+      using `a \<in> s` gs by (intro le) auto
+    ultimately show False by auto
   qed
-
-  have [simp]:"\<And>n. f (Suc n) x = f n y" unfolding f_def y_def by(induct_tac n)auto
-  { fix x y assume "x\<in>s" "y\<in>s" moreover
-    fix e::real assume "e>0" ultimately
-    have "dist y x < e \<longrightarrow> dist (g y) (g x) < e" using dist by fastforce }
-  hence "continuous_on s g" unfolding continuous_on_iff by auto
-
-  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 tendsto_unique[OF trivial_limit_sequentially limb, of "g a"]
-    unfolding `a=b` and o_assoc by auto
-  moreover
-  { fix x assume "x\<in>s" "g x = x" "x\<noteq>a"
-    hence "False" using dist[THEN bspec[where x=a], THEN bspec[where x=x]]
-      using `g a = a` and `a\<in>s` by auto  }
-  ultimately show "\<exists>!x\<in>s. g x = x" using `a\<in>s` by blast
+  moreover have "\<And>x. x \<in> s \<Longrightarrow> g x = x \<Longrightarrow> x = a"
+    using dist[THEN bspec[where x=a]] `g a = a` and `a\<in>s` by auto
+  ultimately show "\<exists>!x\<in>s. g x = x" using `a \<in> s` by blast
 qed
 
 declare tendsto_const [intro] (* FIXME: move *)