1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Jan 18 16:06:45 2013 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Jan 17 15:28:53 2013 -0800
1.3 @@ -6699,7 +6699,7 @@
1.4 subsection {* Edelstein fixed point theorem *}
1.5
1.6 lemma edelstein_fix:
1.7 - fixes s :: "'a::real_normed_vector set"
1.8 + fixes s :: "'a::metric_space set"
1.9 assumes s:"compact s" "s \<noteq> {}" and gs:"(g ` s) \<subseteq> s"
1.10 and dist:"\<forall>x\<in>s. \<forall>y\<in>s. x \<noteq> y \<longrightarrow> dist (g x) (g y) < dist x y"
1.11 shows "\<exists>! x\<in>s. g x = x"
1.12 @@ -6760,23 +6760,29 @@
1.13 unfolding o_def a_def b_def by (rule tendsto_intros)+
1.14
1.15 { fix n::nat
1.16 - 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
1.17 - { fix x y :: 'a
1.18 - have "dist (-x) (-y) = dist x y" unfolding dist_norm
1.19 - using norm_minus_cancel[of "x - y"] by (auto simp add: uminus_add_conv_diff) } note ** = this
1.20 + 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
1.21
1.22 { assume as:"dist a b > dist (f n x) (f n y)"
1.23 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"
1.24 and "\<forall>m\<ge>Nb. dist (f (r m) y) b < (dist a b - dist (f n x) (f n y)) / 2"
1.25 using lima limb unfolding h_def LIMSEQ_def by (fastforce simp del: less_divide_eq_numeral1)
1.26 - hence "dist (f (r (Na + Nb + n)) x - f (r (Na + Nb + n)) y) (a - b) < dist a b - dist (f n x) (f n y)"
1.27 - apply(erule_tac x="Na+Nb+n" in allE)
1.28 - apply(erule_tac x="Na+Nb+n" in allE) apply simp
1.29 - using dist_triangle_add_half[of a "f (r (Na + Nb + n)) x" "dist a b - dist (f n x) (f n y)"
1.30 - "-b" "- f (r (Na + Nb + n)) y"]
1.31 - unfolding ** by (auto simp add: algebra_simps dist_commute)
1.32 + 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)"
1.33 + apply -
1.34 + apply (drule_tac x="Na+Nb+n" in spec, drule mp, simp)
1.35 + apply (drule_tac x="Na+Nb+n" in spec, drule mp, simp)
1.36 + apply (drule (1) add_strict_mono, simp only: real_sum_of_halves)
1.37 + apply (erule le_less_trans [rotated])
1.38 + apply (erule thin_rl)
1.39 + apply (rule abs_leI)
1.40 + apply (simp add: diff_le_iff add_assoc)
1.41 + apply (rule order_trans [OF dist_triangle add_left_mono])
1.42 + apply (subst add_commute, rule dist_triangle2)
1.43 + apply (simp add: diff_le_iff add_assoc)
1.44 + apply (rule order_trans [OF dist_triangle3 add_left_mono])
1.45 + apply (subst add_commute, rule dist_triangle)
1.46 + done
1.47 moreover
1.48 - have "dist (f (r (Na + Nb + n)) x - f (r (Na + Nb + n)) y) (a - b) \<ge> dist a b - dist (f n x) (f n y)"
1.49 + 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)"
1.50 using distf[of n "r (Na+Nb+n)", OF _ `x\<in>s` `y\<in>s`]
1.51 using seq_suble[OF r, of "Na+Nb+n"]
1.52 using *[of "f (r (Na + Nb + n)) x" "f (r (Na + Nb + n)) y" "f n x" "f n y"] by auto
1.53 @@ -6797,7 +6803,10 @@
1.54 moreover have "dist (f (Suc n) y) (g b) \<le> dist (f n y) b"
1.55 using dist[THEN bspec[where x="f n y"], THEN bspec[where x="b"]] and fs by auto
1.56 ultimately have "dist (f (Suc n) x) (g a) + dist (f (Suc n) y) (g b) < e" using n by auto
1.57 - thus False unfolding e_def using ab_fn[of "Suc n"] by norm
1.58 + thus False unfolding e_def using ab_fn[of "Suc n"]
1.59 + using dist_triangle2 [of "f (Suc n) y" "g a" "g b"]
1.60 + using dist_triangle2 [of "f (Suc n) x" "f (Suc n) y" "g a"]
1.61 + by auto
1.62 qed
1.63
1.64 have [simp]:"\<And>n. f (Suc n) x = f n y" unfolding f_def y_def by(induct_tac n)auto