Tidied a lot of messy proofs
authorpaulson <lp15@cam.ac.uk>
Sun Apr 22 21:05:14 2018 +0100 (16 months ago)
changeset 68022c8a506be83bd
parent 68021 b91a043c0dcb
child 68023 75130777ece4
Tidied a lot of messy proofs
src/HOL/Analysis/Brouwer_Fixpoint.thy
     1.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sat Apr 21 11:13:35 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Apr 22 21:05:14 2018 +0100
     1.3 @@ -2,9 +2,6 @@
     1.4      Author:     Robert Himmelmann, TU Muenchen (Translation from HOL light) and LCP
     1.5  *)
     1.6  
     1.7 -(* ========================================================================= *)
     1.8 -(* Results connected with topological dimension.                             *)
     1.9 -(*                                                                           *)
    1.10  (* At the moment this is just Brouwer's fixpoint theorem. The proof is from  *)
    1.11  (* Kuhn: "some combinatorial lemmas in topology", IBM J. v4. (1960) p. 518   *)
    1.12  (* See "http://www.research.ibm.com/journal/rd/045/ibmrd0405K.pdf".          *)
    1.13 @@ -14,7 +11,6 @@
    1.14  (* the big advantage of Kuhn's proof over the usual Sperner's lemma one.     *)
    1.15  (*                                                                           *)
    1.16  (*              (c) Copyright, John Harrison 1998-2008                       *)
    1.17 -(* ========================================================================= *)
    1.18  
    1.19  section \<open>Results connected with topological dimension\<close>
    1.20  
    1.21 @@ -40,11 +36,7 @@
    1.22  lemma swap_image:
    1.23    "Fun.swap i j f ` A = (if i \<in> A then (if j \<in> A then f ` A else f ` ((A - {i}) \<union> {j}))
    1.24                                    else (if j \<in> A then f ` ((A - {j}) \<union> {i}) else f ` A))"
    1.25 -  apply (auto simp: Fun.swap_def image_iff)
    1.26 -  apply metis
    1.27 -  apply (metis member_remove remove_def)
    1.28 -  apply (metis member_remove remove_def)
    1.29 -  done
    1.30 +  by (auto simp: swap_def image_def) metis
    1.31  
    1.32  lemmas swap_apply1 = swap_apply(1)
    1.33  lemmas swap_apply2 = swap_apply(2)
    1.34 @@ -191,9 +183,9 @@
    1.35      moreover obtain a where "rl a = Suc n" "a \<in> s"
    1.36        by (metis atMost_iff image_iff le_Suc_eq rl)
    1.37      ultimately have n: "{..n} = rl ` (s - {a})"
    1.38 -      by (auto simp add: inj_on_image_set_diff Diff_subset rl)
    1.39 +      by (auto simp: inj_on_image_set_diff Diff_subset rl)
    1.40      have "{a\<in>s. rl ` (s - {a}) = {..n}} = {a}"
    1.41 -      using inj_rl \<open>a \<in> s\<close> by (auto simp add: n inj_on_image_eq_iff[OF inj_rl] Diff_subset)
    1.42 +      using inj_rl \<open>a \<in> s\<close> by (auto simp: n inj_on_image_eq_iff[OF inj_rl] Diff_subset)
    1.43      then show "card ?S = 1"
    1.44        unfolding card_S by simp }
    1.45  
    1.46 @@ -202,7 +194,7 @@
    1.47      proof cases
    1.48        assume *: "{..n} \<subseteq> rl ` s"
    1.49        with rl rl_bd[OF s] have rl_s: "rl ` s = {..n}"
    1.50 -        by (auto simp add: atMost_Suc subset_insert_iff split: if_split_asm)
    1.51 +        by (auto simp: atMost_Suc subset_insert_iff split: if_split_asm)
    1.52        then have "\<not> inj_on rl s"
    1.53          by (intro pigeonhole) simp
    1.54        then obtain a b where ab: "a \<in> s" "b \<in> s" "rl a = rl b" "a \<noteq> b"
    1.55 @@ -210,7 +202,7 @@
    1.56        then have eq: "rl ` (s - {a}) = rl ` s"
    1.57          by auto
    1.58        with ab have inj: "inj_on rl (s - {a})"
    1.59 -        by (intro eq_card_imp_inj_on) (auto simp add: rl_s card_Diff_singleton_if)
    1.60 +        by (intro eq_card_imp_inj_on) (auto simp: rl_s card_Diff_singleton_if)
    1.61  
    1.62        { fix x assume "x \<in> s" "x \<notin> {a, b}"
    1.63          then have "rl ` s - {rl x} = rl ` ((s - {a}) - {x})"
    1.64 @@ -275,7 +267,7 @@
    1.65      with upd have "upd ` {..< x} \<noteq> upd ` {..< y}"
    1.66        by (subst inj_on_image_eq_iff[where C="{..< n}"]) (auto simp: bij_betw_def)
    1.67      then have "enum x \<noteq> enum y"
    1.68 -      by (auto simp add: enum_def fun_eq_iff) }
    1.69 +      by (auto simp: enum_def fun_eq_iff) }
    1.70    then show ?thesis
    1.71      by (auto simp: inj_on_def)
    1.72  qed
    1.73 @@ -325,7 +317,7 @@
    1.74    by (auto simp: enum_def le_fun_def in_upd_image Ball_def[symmetric])
    1.75  
    1.76  lemma enum_strict_mono: "i \<le> n \<Longrightarrow> j \<le> n \<Longrightarrow> enum i < enum j \<longleftrightarrow> i < j"
    1.77 -  using enum_mono[of i j] enum_inj[of i j] by (auto simp add: le_less)
    1.78 +  using enum_mono[of i j] enum_inj[of i j] by (auto simp: le_less)
    1.79  
    1.80  lemma chain: "a \<in> s \<Longrightarrow> b \<in> s \<Longrightarrow> a \<le> b \<or> b \<le> a"
    1.81    by (auto simp: s_eq enum_mono)
    1.82 @@ -346,7 +338,7 @@
    1.83    by (induct i) (auto simp: enum_Suc enum_0 base_out upd_space not_less[symmetric])
    1.84  
    1.85  lemma out_eq_p: "a \<in> s \<Longrightarrow> n \<le> j \<Longrightarrow> a j = p"
    1.86 -  unfolding s_eq by (auto simp add: enum_eq_p)
    1.87 +  unfolding s_eq by (auto simp: enum_eq_p)
    1.88  
    1.89  lemma s_le_p: "a \<in> s \<Longrightarrow> a j \<le> p"
    1.90    using out_eq_p[of a j] s_space by (cases "j < n") auto
    1.91 @@ -578,7 +570,7 @@
    1.92          by (auto simp: image_iff Ball_def) arith
    1.93        then have upd_Suc: "\<And>i. i \<le> n \<Longrightarrow> (upd\<circ>Suc) ` {..< i} = upd ` {..< Suc i} - {n}"
    1.94          using \<open>upd 0 = n\<close> upd_inj
    1.95 -        by (auto simp add: image_comp[symmetric] inj_on_image_set_diff[OF inj_upd])
    1.96 +        by (auto simp: image_comp[symmetric] inj_on_image_set_diff[OF inj_upd])
    1.97        have n_in_upd: "\<And>i. n \<in> upd ` {..< Suc i}"
    1.98          using \<open>upd 0 = n\<close> by auto
    1.99  
   1.100 @@ -685,7 +677,7 @@
   1.101  qed
   1.102  
   1.103  lemma card_2_exists: "card s = 2 \<longleftrightarrow> (\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y))"
   1.104 -  by (auto simp add: card_Suc_eq eval_nat_numeral)
   1.105 +  by (auto simp: card_Suc_eq eval_nat_numeral)
   1.106  
   1.107  lemma ksimplex_replace_2:
   1.108    assumes s: "ksimplex p n s" and "a \<in> s" and "n \<noteq> 0"
   1.109 @@ -723,11 +715,11 @@
   1.110        obtain i' where "i' \<le> n" "enum i' \<noteq> enum 0" "enum i' (upd 0) \<noteq> p"
   1.111          unfolding s_eq by (auto intro: upd_space simp: enum_inj)
   1.112        then have "enum 1 \<le> enum i'" "enum i' (upd 0) < p"
   1.113 -        using enum_le_p[of i' "upd 0"] by (auto simp add: enum_inj enum_mono upd_space)
   1.114 +        using enum_le_p[of i' "upd 0"] by (auto simp: enum_inj enum_mono upd_space)
   1.115        then have "enum 1 (upd 0) < p"
   1.116 -        by (auto simp add: le_fun_def intro: le_less_trans)
   1.117 +        by (auto simp: le_fun_def intro: le_less_trans)
   1.118        then show "enum (Suc 0) \<in> {..<n} \<rightarrow> {..<p}"
   1.119 -        using base \<open>n \<noteq> 0\<close> by (auto simp add: enum_0 enum_Suc PiE_iff extensional_def upd_space)
   1.120 +        using base \<open>n \<noteq> 0\<close> by (auto simp: enum_0 enum_Suc PiE_iff extensional_def upd_space)
   1.121  
   1.122        { fix i assume "n \<le> i" then show "enum (Suc 0) i = p"
   1.123          using \<open>n \<noteq> 0\<close> by (auto simp: enum_eq_p) }
   1.124 @@ -745,7 +737,7 @@
   1.125  
   1.126      { fix j assume j: "j < n"
   1.127        from j \<open>n \<noteq> 0\<close> have "f' j = enum (Suc j)"
   1.128 -        by (auto simp add: f'_def enum_def upd_inj in_upd_image image_comp[symmetric] fun_eq_iff) }
   1.129 +        by (auto simp: f'_def enum_def upd_inj in_upd_image image_comp[symmetric] fun_eq_iff) }
   1.130      note f'_eq_enum = this
   1.131      then have "enum ` Suc ` {..< n} = f' ` {..< n}"
   1.132        by (force simp: enum_inj)
   1.133 @@ -859,10 +851,10 @@
   1.134        by (simp_all add: rot_def)
   1.135  
   1.136      { fix j assume j: "Suc j \<le> n" then have "b.enum (Suc j) = enum j"
   1.137 -        by (induct j) (auto simp add: benum1 enum_0 b.enum_Suc enum_Suc rot_simps) }
   1.138 +        by (induct j) (auto simp: benum1 enum_0 b.enum_Suc enum_Suc rot_simps) }
   1.139      note b_enum_eq_enum = this
   1.140      then have "enum ` {..< n} = b.enum ` Suc ` {..< n}"
   1.141 -      by (auto simp add: image_comp intro!: image_cong)
   1.142 +      by (auto simp: image_comp intro!: image_cong)
   1.143      also have "Suc ` {..< n} = {.. n} - {0}"
   1.144        by (auto simp: image_iff Ball_def) arith
   1.145      also have "{..< n} = {.. n} - {n}"
   1.146 @@ -871,7 +863,7 @@
   1.147        unfolding s_eq \<open>a = enum i\<close> \<open>i = n\<close>
   1.148        using inj_on_image_set_diff[OF inj_enum Diff_subset, of "{n}"]
   1.149              inj_on_image_set_diff[OF b.inj_enum Diff_subset, of "{0}"]
   1.150 -      by (simp add: comp_def )
   1.151 +      by (simp add: comp_def)
   1.152  
   1.153      have "b.enum 0 \<le> b.enum n"
   1.154        by (simp add: b.enum_mono)
   1.155 @@ -956,7 +948,7 @@
   1.156        moreover note i
   1.157        ultimately have "enum j = b.enum j \<longleftrightarrow> j \<noteq> i"
   1.158          unfolding enum_def[abs_def] b.enum_def[abs_def]
   1.159 -        by (auto simp add: fun_eq_iff swap_image i'_def
   1.160 +        by (auto simp: fun_eq_iff swap_image i'_def
   1.161                             in_upd_image inj_on_image_set_diff[OF inj_upd]) }
   1.162      note enum_eq_benum = this
   1.163      then have "enum ` ({.. n} - {i}) = b.enum ` ({.. n} - {i})"
   1.164 @@ -1001,7 +993,7 @@
   1.165          then obtain j where "t.enum (Suc l) = enum j" "j \<le> n" "enum j \<noteq> enum i"
   1.166            unfolding s_eq \<open>a = enum i\<close> by auto
   1.167          with i have "t.enum (Suc l) \<le> t.enum l \<or> t.enum k \<le> t.enum (Suc l)"
   1.168 -          by (auto simp add: i'_def enum_mono enum_inj l k)
   1.169 +          by (auto simp: i'_def enum_mono enum_inj l k)
   1.170          with \<open>Suc l < k\<close> \<open>k \<le> n\<close> show False
   1.171            by (simp add: t.enum_mono)
   1.172        qed
   1.173 @@ -1041,7 +1033,7 @@
   1.174          assume u: "u l = upd (Suc i')"
   1.175          define B where "B = b.enum ` {..n}"
   1.176          have "b.enum i' = enum i'"
   1.177 -          using enum_eq_benum[of i'] i by (auto simp add: i'_def gr0_conv_Suc)
   1.178 +          using enum_eq_benum[of i'] i by (auto simp: i'_def gr0_conv_Suc)
   1.179          have "c = t.enum (Suc l)" unfolding c_eq ..
   1.180          also have "t.enum (Suc l) = b.enum (Suc i')"
   1.181            using u \<open>l < k\<close> \<open>k \<le> n\<close> \<open>Suc i' < n\<close>
   1.182 @@ -1432,7 +1424,7 @@
   1.183  proof (rule ccontr)
   1.184    define n where "n = DIM('a)"
   1.185    have n: "1 \<le> n" "0 < n" "n \<noteq> 0"
   1.186 -    unfolding n_def by (auto simp add: Suc_le_eq DIM_positive)
   1.187 +    unfolding n_def by (auto simp: Suc_le_eq DIM_positive)
   1.188    assume "\<not> ?thesis"
   1.189    then have *: "\<not> (\<exists>x\<in>unit_cube. f x - x = 0)"
   1.190      by auto
   1.191 @@ -1447,73 +1439,45 @@
   1.192      using assms(2)[unfolded image_subset_iff Ball_def]
   1.193      unfolding mem_unit_cube
   1.194      by auto
   1.195 -  obtain label :: "'a \<Rightarrow> 'a \<Rightarrow> nat" where
   1.196 +  obtain label :: "'a \<Rightarrow> 'a \<Rightarrow> nat" where label [rule_format]:
   1.197      "\<forall>x. \<forall>i\<in>Basis. label x i \<le> 1"
   1.198 -    "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> True \<and> x \<bullet> i = 0 \<longrightarrow> label x i = 0"
   1.199 -    "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> True \<and> x \<bullet> i = 1 \<longrightarrow> label x i = 1"
   1.200 -    "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> True \<and> label x i = 0 \<longrightarrow> x \<bullet> i \<le> f x \<bullet> i"
   1.201 -    "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> True \<and> label x i = 1 \<longrightarrow> f x \<bullet> i \<le> x \<bullet> i"
   1.202 -    using kuhn_labelling_lemma[OF *] by blast
   1.203 +    "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> x \<bullet> i = 0 \<longrightarrow> label x i = 0"
   1.204 +    "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> x \<bullet> i = 1 \<longrightarrow> label x i = 1"
   1.205 +    "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> label x i = 0 \<longrightarrow> x \<bullet> i \<le> f x \<bullet> i"
   1.206 +    "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> label x i = 1 \<longrightarrow> f x \<bullet> i \<le> x \<bullet> i"
   1.207 +    using kuhn_labelling_lemma[OF *] by auto
   1.208    note label = this [rule_format]
   1.209    have lem1: "\<forall>x\<in>unit_cube. \<forall>y\<in>unit_cube. \<forall>i\<in>Basis. label x i \<noteq> label y i \<longrightarrow>
   1.210      \<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y - f x) + norm (y - x)"
   1.211    proof safe
   1.212      fix x y :: 'a
   1.213 -    assume x: "x \<in> unit_cube"
   1.214 -    assume y: "y \<in> unit_cube"
   1.215 +    assume x: "x \<in> unit_cube" and y: "y \<in> unit_cube"
   1.216      fix i
   1.217      assume i: "label x i \<noteq> label y i" "i \<in> Basis"
   1.218      have *: "\<And>x y fx fy :: real. x \<le> fx \<and> fy \<le> y \<or> fx \<le> x \<and> y \<le> fy \<Longrightarrow>
   1.219        \<bar>fx - x\<bar> \<le> \<bar>fy - fx\<bar> + \<bar>y - x\<bar>" by auto
   1.220      have "\<bar>(f x - x) \<bullet> i\<bar> \<le> \<bar>(f y - f x)\<bullet>i\<bar> + \<bar>(y - x)\<bullet>i\<bar>"
   1.221 -      unfolding inner_simps
   1.222 -      apply (rule *)
   1.223 -      apply (cases "label x i = 0")
   1.224 -      apply (rule disjI1)
   1.225 -      apply rule
   1.226 -      prefer 3
   1.227 -      apply (rule disjI2)
   1.228 -      apply rule
   1.229 -    proof -
   1.230 -      assume lx: "label x i = 0"
   1.231 -      then have ly: "label y i = 1"
   1.232 -        using i label(1)[of i y]
   1.233 -        by auto
   1.234 -      show "x \<bullet> i \<le> f x \<bullet> i"
   1.235 -        apply (rule label(4)[rule_format])
   1.236 -        using x y lx i(2)
   1.237 -        apply auto
   1.238 -        done
   1.239 -      show "f y \<bullet> i \<le> y \<bullet> i"
   1.240 -        apply (rule label(5)[rule_format])
   1.241 -        using x y ly i(2)
   1.242 -        apply auto
   1.243 -        done
   1.244 +    proof (cases "label x i = 0")
   1.245 +      case True
   1.246 +      then have fxy: "\<not> f y \<bullet> i \<le> y \<bullet> i \<Longrightarrow> f x \<bullet> i \<le> x \<bullet> i"
   1.247 +        by (metis True i label(1) label(5) le_antisym less_one not_le_imp_less y)
   1.248 +      show ?thesis
   1.249 +      unfolding inner_simps         
   1.250 +      by (rule *) (auto simp: True i label x y fxy)
   1.251      next
   1.252 -      assume "label x i \<noteq> 0"
   1.253 -      then have l: "label x i = 1" "label y i = 0"
   1.254 -        using i label(1)[of i x] label(1)[of i y]
   1.255 -        by auto
   1.256 -      show "f x \<bullet> i \<le> x \<bullet> i"
   1.257 -        apply (rule label(5)[rule_format])
   1.258 -        using x y l i(2)
   1.259 -        apply auto
   1.260 -        done
   1.261 -      show "y \<bullet> i \<le> f y \<bullet> i"
   1.262 -        apply (rule label(4)[rule_format])
   1.263 -        using x y l i(2)
   1.264 -        apply auto
   1.265 -        done
   1.266 +      case False
   1.267 +      then show ?thesis
   1.268 +        using label [OF \<open>i \<in> Basis\<close>] i(1) x y
   1.269 +        apply (auto simp: inner_diff_left le_Suc_eq)
   1.270 +        by (metis "*")
   1.271      qed
   1.272      also have "\<dots> \<le> norm (f y - f x) + norm (y - x)"
   1.273 -      apply (rule add_mono)
   1.274 -      apply (rule Basis_le_norm[OF i(2)])+
   1.275 -      done
   1.276 +      by (simp add: add_mono i(2) norm_bound_Basis_le)
   1.277      finally show "\<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y - f x) + norm (y - x)"
   1.278        unfolding inner_simps .
   1.279    qed
   1.280    have "\<exists>e>0. \<forall>x\<in>unit_cube. \<forall>y\<in>unit_cube. \<forall>z\<in>unit_cube. \<forall>i\<in>Basis.
   1.281 -    norm (x - z) < e \<and> norm (y - z) < e \<and> label x i \<noteq> label y i \<longrightarrow>
   1.282 +    norm (x - z) < e \<longrightarrow> norm (y - z) < e \<longrightarrow> label x i \<noteq> label y i \<longrightarrow>
   1.283        \<bar>(f(z) - z)\<bullet>i\<bar> < d / (real n)"
   1.284    proof -
   1.285      have d': "d / real n / 8 > 0"
   1.286 @@ -1530,9 +1494,7 @@
   1.287        unfolding dist_norm
   1.288        by blast
   1.289      show ?thesis
   1.290 -      apply (rule_tac x="min (e/2) (d/real n/8)" in exI)
   1.291 -      apply safe
   1.292 -    proof -
   1.293 +    proof (intro exI conjI ballI impI)
   1.294        show "0 < min (e / 2) (d / real n / 8)"
   1.295          using d' e by auto
   1.296        fix x y z i
   1.297 @@ -1551,10 +1513,9 @@
   1.298          unfolding inner_simps
   1.299        proof (rule *)
   1.300          show "\<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y -f x) + norm (y - x)"
   1.301 -          apply (rule lem1[rule_format])
   1.302 -          using as i
   1.303 -          apply auto
   1.304 -          done
   1.305 +          using as(1) as(2) as(6) i lem1 by blast
   1.306 +        show "norm (f x - f z) < d / real n / 8"
   1.307 +          using d' e as by auto
   1.308          show "\<bar>f x \<bullet> i - f z \<bullet> i\<bar> \<le> norm (f x - f z)" "\<bar>x \<bullet> i - z \<bullet> i\<bar> \<le> norm (x - z)"
   1.309            unfolding inner_diff_left[symmetric]
   1.310            by (rule Basis_le_norm[OF i])+
   1.311 @@ -1563,30 +1524,14 @@
   1.312            unfolding norm_minus_commute
   1.313            by auto
   1.314          also have "\<dots> < e / 2 + e / 2"
   1.315 -          apply (rule add_strict_mono)
   1.316 -          using as(4,5)
   1.317 -          apply auto
   1.318 -          done
   1.319 +          using as(4) as(5) by auto
   1.320          finally show "norm (f y - f x) < d / real n / 8"
   1.321 -          apply -
   1.322 -          apply (rule e(2))
   1.323 -          using as
   1.324 -          apply auto
   1.325 -          done
   1.326 +          using as(1) as(2) e(2) by auto
   1.327          have "norm (y - z) + norm (x - z) < d / real n / 8 + d / real n / 8"
   1.328 -          apply (rule add_strict_mono)
   1.329 -          using as
   1.330 -          apply auto
   1.331 -          done
   1.332 -        then show "norm (y - x) < 2 * (d / real n / 8)"
   1.333 -          using tria
   1.334 +          using as(4) as(5) by auto
   1.335 +        with tria show "norm (y - x) < 2 * (d / real n / 8)"
   1.336            by auto
   1.337 -        show "norm (f x - f z) < d / real n / 8"
   1.338 -          apply (rule e(2))
   1.339 -          using as e(1)
   1.340 -          apply auto
   1.341 -          done
   1.342 -      qed (insert as, auto)
   1.343 +      qed (use as in auto)
   1.344      qed
   1.345    qed
   1.346    then
   1.347 @@ -1635,14 +1580,14 @@
   1.348    { fix x :: "nat \<Rightarrow> nat" and i assume "\<forall>i<n. x i \<le> p" "i < n" "x i = p \<or> x i = 0"
   1.349      then have "(\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<in> (unit_cube::'a set)"
   1.350        using b'_Basis
   1.351 -      by (auto simp add: mem_unit_cube inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1) }
   1.352 +      by (auto simp: mem_unit_cube inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1) }
   1.353    note cube = this
   1.354    have q2: "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = 0 \<longrightarrow>
   1.355        (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0)"
   1.356 -    unfolding o_def using cube \<open>p > 0\<close> by (intro allI impI label(2)) (auto simp add: b'')
   1.357 +    unfolding o_def using cube \<open>p > 0\<close> by (intro allI impI label(2)) (auto simp: b'')
   1.358    have q3: "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = p \<longrightarrow>
   1.359        (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 1)"
   1.360 -    using cube \<open>p > 0\<close> unfolding o_def by (intro allI impI label(3)) (auto simp add: b'')
   1.361 +    using cube \<open>p > 0\<close> unfolding o_def by (intro allI impI label(3)) (auto simp: b'')
   1.362    obtain q where q:
   1.363        "\<forall>i<n. q i < p"
   1.364        "\<forall>i<n.
   1.365 @@ -1660,24 +1605,20 @@
   1.366      then have "z \<in> unit_cube"
   1.367        unfolding z_def mem_unit_cube
   1.368        using b'_Basis
   1.369 -      by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1)
   1.370 +      by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1)
   1.371      then have d_fz_z: "d \<le> norm (f z - z)"
   1.372        by (rule d)
   1.373      assume "\<not> ?thesis"
   1.374      then have as: "\<forall>i\<in>Basis. \<bar>f z \<bullet> i - z \<bullet> i\<bar> < d / real n"
   1.375        using \<open>n > 0\<close>
   1.376 -      by (auto simp add: not_le inner_diff)
   1.377 +      by (auto simp: not_le inner_diff)
   1.378      have "norm (f z - z) \<le> (\<Sum>i\<in>Basis. \<bar>f z \<bullet> i - z \<bullet> i\<bar>)"
   1.379        unfolding inner_diff_left[symmetric]
   1.380        by (rule norm_le_l1)
   1.381      also have "\<dots> < (\<Sum>(i::'a) \<in> Basis. d / real n)"
   1.382 -      apply (rule sum_strict_mono)
   1.383 -      using as
   1.384 -      apply auto
   1.385 -      done
   1.386 +      by (meson as finite_Basis nonempty_Basis sum_strict_mono)
   1.387      also have "\<dots> = d"
   1.388 -      using DIM_positive[where 'a='a]
   1.389 -      by (auto simp: n_def)
   1.390 +      using DIM_positive[where 'a='a] by (auto simp: n_def)
   1.391      finally show False
   1.392        using d_fz_z by auto
   1.393    qed
   1.394 @@ -1698,50 +1639,37 @@
   1.395      apply (rule order_trans)
   1.396      apply (rule rs(1)[OF b'_im,THEN conjunct2])
   1.397      using q(1)[rule_format,OF b'_im]
   1.398 -    apply (auto simp add: Suc_le_eq)
   1.399 +    apply (auto simp: Suc_le_eq)
   1.400      done
   1.401    then have "r' \<in> unit_cube"
   1.402      unfolding r'_def mem_unit_cube
   1.403      using b'_Basis
   1.404 -    by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1)
   1.405 +    by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1)
   1.406    define s' :: 'a where "s' = (\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i)"
   1.407    have "\<And>i. i \<in> Basis \<Longrightarrow> s (b' i) \<le> p"
   1.408 -    apply (rule order_trans)
   1.409 -    apply (rule rs(2)[OF b'_im, THEN conjunct2])
   1.410 -    using q(1)[rule_format,OF b'_im]
   1.411 -    apply (auto simp add: Suc_le_eq)
   1.412 -    done
   1.413 +    using b'_im q(1) rs(2) by fastforce
   1.414    then have "s' \<in> unit_cube"
   1.415      unfolding s'_def mem_unit_cube
   1.416 -    using b'_Basis
   1.417 -    by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1)
   1.418 +    using b'_Basis by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1)
   1.419    have "z \<in> unit_cube"
   1.420      unfolding z_def mem_unit_cube
   1.421      using b'_Basis q(1)[rule_format,OF b'_im] \<open>p > 0\<close>
   1.422 -    by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1 less_imp_le)
   1.423 -  have *: "\<And>x. 1 + real x = real (Suc x)"
   1.424 -    by auto
   1.425 +    by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1 less_imp_le)
   1.426    {
   1.427      have "(\<Sum>i\<in>Basis. \<bar>real (r (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
   1.428 -      apply (rule sum_mono)
   1.429 -      using rs(1)[OF b'_im]
   1.430 -      apply (auto simp add:* field_simps simp del: of_nat_Suc)
   1.431 -      done
   1.432 +      by (rule sum_mono) (use rs(1)[OF b'_im] in force)
   1.433      also have "\<dots> < e * real p"
   1.434        using p \<open>e > 0\<close> \<open>p > 0\<close>
   1.435 -      by (auto simp add: field_simps n_def)
   1.436 +      by (auto simp: field_simps n_def)
   1.437      finally have "(\<Sum>i\<in>Basis. \<bar>real (r (b' i)) - real (q (b' i))\<bar>) < e * real p" .
   1.438    }
   1.439    moreover
   1.440    {
   1.441      have "(\<Sum>i\<in>Basis. \<bar>real (s (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
   1.442 -      apply (rule sum_mono)
   1.443 -      using rs(2)[OF b'_im]
   1.444 -      apply (auto simp add:* field_simps simp del: of_nat_Suc)
   1.445 -      done
   1.446 +      by (rule sum_mono) (use rs(2)[OF b'_im] in force)
   1.447      also have "\<dots> < e * real p"
   1.448        using p \<open>e > 0\<close> \<open>p > 0\<close>
   1.449 -      by (auto simp add: field_simps n_def)
   1.450 +      by (auto simp: field_simps n_def)
   1.451      finally have "(\<Sum>i\<in>Basis. \<bar>real (s (b' i)) - real (q (b' i))\<bar>) < e * real p" .
   1.452    }
   1.453    ultimately
   1.454 @@ -1749,7 +1677,7 @@
   1.455      unfolding r'_def s'_def z_def
   1.456      using \<open>p > 0\<close>
   1.457      apply (rule_tac[!] le_less_trans[OF norm_le_l1])
   1.458 -    apply (auto simp add: field_simps sum_divide_distrib[symmetric] inner_diff_left)
   1.459 +    apply (auto simp: field_simps sum_divide_distrib[symmetric] inner_diff_left)
   1.460      done
   1.461    then have "\<bar>(f z - z) \<bullet> i\<bar> < d / real n"
   1.462      using rs(3) i
   1.463 @@ -1762,121 +1690,100 @@
   1.464  
   1.465  subsection \<open>Retractions\<close>
   1.466  
   1.467 -definition "retraction s t r \<longleftrightarrow> t \<subseteq> s \<and> continuous_on s r \<and> r ` s \<subseteq> t \<and> (\<forall>x\<in>t. r x = x)"
   1.468 +definition "retraction S T r \<longleftrightarrow> T \<subseteq> S \<and> continuous_on S r \<and> r ` S \<subseteq> T \<and> (\<forall>x\<in>T. r x = x)"
   1.469  
   1.470  definition retract_of (infixl "retract'_of" 50)
   1.471 -  where "(t retract_of s) \<longleftrightarrow> (\<exists>r. retraction s t r)"
   1.472 -
   1.473 -lemma retraction_idempotent: "retraction s t r \<Longrightarrow> x \<in> s \<Longrightarrow>  r (r x) = r x"
   1.474 +  where "(T retract_of S) \<longleftrightarrow> (\<exists>r. retraction S T r)"
   1.475 +
   1.476 +lemma retraction_idempotent: "retraction S T r \<Longrightarrow> x \<in> S \<Longrightarrow>  r (r x) = r x"
   1.477    unfolding retraction_def by auto
   1.478  
   1.479  subsection \<open>Preservation of fixpoints under (more general notion of) retraction\<close>
   1.480  
   1.481  lemma invertible_fixpoint_property:
   1.482 -  fixes s :: "'a::euclidean_space set"
   1.483 -    and t :: "'b::euclidean_space set"
   1.484 -  assumes "continuous_on t i"
   1.485 -    and "i ` t \<subseteq> s"
   1.486 -    and "continuous_on s r"
   1.487 -    and "r ` s \<subseteq> t"
   1.488 -    and "\<forall>y\<in>t. r (i y) = y"
   1.489 -    and "\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)"
   1.490 -    and "continuous_on t g"
   1.491 -    and "g ` t \<subseteq> t"
   1.492 -  obtains y where "y \<in> t" and "g y = y"
   1.493 +  fixes S :: "'a::euclidean_space set"
   1.494 +    and T :: "'b::euclidean_space set"
   1.495 +  assumes contt: "continuous_on T i"
   1.496 +    and "i ` T \<subseteq> S"
   1.497 +    and contr: "continuous_on S r"
   1.498 +    and "r ` S \<subseteq> T"
   1.499 +    and ri: "\<And>y. y \<in> T \<Longrightarrow> r (i y) = y"
   1.500 +    and FP: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. f x = x"
   1.501 +    and contg: "continuous_on T g"
   1.502 +    and "g ` T \<subseteq> T"
   1.503 +  obtains y where "y \<in> T" and "g y = y"
   1.504  proof -
   1.505 -  have "\<exists>x\<in>s. (i \<circ> g \<circ> r) x = x"
   1.506 -    apply (rule assms(6)[rule_format])
   1.507 -    apply rule
   1.508 -    apply (rule continuous_on_compose assms)+
   1.509 -    apply ((rule continuous_on_subset)?, rule assms)+
   1.510 -    using assms(2,4,8)
   1.511 -    apply auto
   1.512 -    apply blast
   1.513 -    done
   1.514 -  then obtain x where x: "x \<in> s" "(i \<circ> g \<circ> r) x = x" ..
   1.515 -  then have *: "g (r x) \<in> t"
   1.516 +  have "\<exists>x\<in>S. (i \<circ> g \<circ> r) x = x"
   1.517 +  proof (rule FP)
   1.518 +    show "continuous_on S (i \<circ> g \<circ> r)"
   1.519 +      by (meson contt contr assms(4) contg assms(8) continuous_on_compose continuous_on_subset)
   1.520 +    show "(i \<circ> g \<circ> r) ` S \<subseteq> S"
   1.521 +      using assms(2,4,8) by force
   1.522 +  qed
   1.523 +  then obtain x where x: "x \<in> S" "(i \<circ> g \<circ> r) x = x" ..
   1.524 +  then have *: "g (r x) \<in> T"
   1.525      using assms(4,8) by auto
   1.526    have "r ((i \<circ> g \<circ> r) x) = r x"
   1.527      using x by auto
   1.528    then show ?thesis
   1.529 -    apply (rule_tac that[of "r x"])
   1.530 -    using x
   1.531 -    unfolding o_def
   1.532 -    unfolding assms(5)[rule_format,OF *]
   1.533 -    using assms(4)
   1.534 -    apply auto
   1.535 -    done
   1.536 +    using "*" ri that by auto
   1.537  qed
   1.538  
   1.539  lemma homeomorphic_fixpoint_property:
   1.540 -  fixes s :: "'a::euclidean_space set"
   1.541 -    and t :: "'b::euclidean_space set"
   1.542 -  assumes "s homeomorphic t"
   1.543 -  shows "(\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)) \<longleftrightarrow>
   1.544 -    (\<forall>g. continuous_on t g \<and> g ` t \<subseteq> t \<longrightarrow> (\<exists>y\<in>t. g y = y))"
   1.545 +  fixes S :: "'a::euclidean_space set"
   1.546 +    and T :: "'b::euclidean_space set"
   1.547 +  assumes "S homeomorphic T"
   1.548 +  shows "(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> S \<longrightarrow> (\<exists>x\<in>S. f x = x)) \<longleftrightarrow>
   1.549 +         (\<forall>g. continuous_on T g \<and> g ` T \<subseteq> T \<longrightarrow> (\<exists>y\<in>T. g y = y))"
   1.550 +         (is "?lhs = ?rhs")
   1.551  proof -
   1.552 -  obtain r i where
   1.553 -      "\<forall>x\<in>s. i (r x) = x"
   1.554 -      "r ` s = t"
   1.555 -      "continuous_on s r"
   1.556 -      "\<forall>y\<in>t. r (i y) = y"
   1.557 -      "i ` t = s"
   1.558 -      "continuous_on t i"
   1.559 -    using assms
   1.560 -    unfolding homeomorphic_def homeomorphism_def
   1.561 -    by blast
   1.562 -  then show ?thesis
   1.563 -    apply -
   1.564 -    apply rule
   1.565 -    apply (rule_tac[!] allI impI)+
   1.566 -    apply (rule_tac g=g in invertible_fixpoint_property[of t i s r])
   1.567 -    prefer 10
   1.568 -    apply (rule_tac g=f in invertible_fixpoint_property[of s r t i])
   1.569 -    apply auto
   1.570 -    done
   1.571 +  obtain r i where r:
   1.572 +      "\<forall>x\<in>S. i (r x) = x" "r ` S = T" "continuous_on S r"
   1.573 +      "\<forall>y\<in>T. r (i y) = y" "i ` T = S" "continuous_on T i"
   1.574 +    using assms unfolding homeomorphic_def homeomorphism_def  by blast
   1.575 +  show ?thesis
   1.576 +  proof
   1.577 +    assume ?lhs
   1.578 +    with r show ?rhs
   1.579 +      by (metis invertible_fixpoint_property[of T i S r] order_refl)
   1.580 +  next
   1.581 +    assume ?rhs
   1.582 +    with r show ?lhs
   1.583 +      by (metis invertible_fixpoint_property[of S r T i] order_refl)
   1.584 +  qed
   1.585  qed
   1.586  
   1.587  lemma retract_fixpoint_property:
   1.588    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   1.589 -    and s :: "'a set"
   1.590 -  assumes "t retract_of s"
   1.591 -    and "\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)"
   1.592 -    and "continuous_on t g"
   1.593 -    and "g ` t \<subseteq> t"
   1.594 -  obtains y where "y \<in> t" and "g y = y"
   1.595 +    and S :: "'a set"
   1.596 +  assumes "T retract_of S"
   1.597 +    and FP: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. f x = x"
   1.598 +    and contg: "continuous_on T g"
   1.599 +    and "g ` T \<subseteq> T"
   1.600 +  obtains y where "y \<in> T" and "g y = y"
   1.601  proof -
   1.602 -  obtain h where "retraction s t h"
   1.603 +  obtain h where "retraction S T h"
   1.604      using assms(1) unfolding retract_of_def ..
   1.605    then show ?thesis
   1.606      unfolding retraction_def
   1.607 -    apply -
   1.608 -    apply (rule invertible_fixpoint_property[OF continuous_on_id _ _ _ _ assms(2), of t h g])
   1.609 -    prefer 7
   1.610 -    apply (rule_tac y = y in that)
   1.611 -    using assms
   1.612 -    apply auto
   1.613 -    done
   1.614 +    using invertible_fixpoint_property[OF continuous_on_id _ _ _ _ FP]
   1.615 +    by (metis assms(4) contg image_ident that)
   1.616  qed
   1.617  
   1.618  
   1.619  subsection \<open>The Brouwer theorem for any set with nonempty interior\<close>
   1.620  
   1.621  lemma convex_unit_cube: "convex unit_cube"
   1.622 -  apply (rule is_interval_convex)
   1.623 -  apply (clarsimp simp add: is_interval_def mem_unit_cube)
   1.624 -  apply (drule (1) bspec)+
   1.625 -  apply auto
   1.626 -  done
   1.627 +  by (rule is_interval_convex) (fastforce simp add: is_interval_def mem_unit_cube)
   1.628  
   1.629  lemma brouwer_weak:
   1.630    fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
   1.631 -  assumes "compact s"
   1.632 -    and "convex s"
   1.633 -    and "interior s \<noteq> {}"
   1.634 -    and "continuous_on s f"
   1.635 -    and "f ` s \<subseteq> s"
   1.636 -  obtains x where "x \<in> s" and "f x = x"
   1.637 +  assumes "compact S"
   1.638 +    and "convex S"
   1.639 +    and "interior S \<noteq> {}"
   1.640 +    and "continuous_on S f"
   1.641 +    and "f ` S \<subseteq> S"
   1.642 +  obtains x where "x \<in> S" and "f x = x"
   1.643  proof -
   1.644    let ?U = "unit_cube :: 'a set"
   1.645    have "\<Sum>Basis /\<^sub>R 2 \<in> interior ?U"
   1.646 @@ -1890,7 +1797,7 @@
   1.647        unfolding unit_cube_def by force
   1.648    qed
   1.649    then have *: "interior ?U \<noteq> {}" by fast
   1.650 -  have *: "?U homeomorphic s"
   1.651 +  have *: "?U homeomorphic S"
   1.652      using homeomorphic_convex_compact[OF convex_unit_cube compact_unit_cube * assms(2,1,3)] .
   1.653    have "\<forall>f. continuous_on ?U f \<and> f ` ?U \<subseteq> ?U \<longrightarrow>
   1.654      (\<exists>x\<in>?U. f x = x)"
   1.655 @@ -1898,7 +1805,7 @@
   1.656    then show ?thesis
   1.657      unfolding homeomorphic_fixpoint_property[OF *]
   1.658      using assms
   1.659 -    by (auto simp: intro: that)
   1.660 +    by (auto intro: that)
   1.661  qed
   1.662  
   1.663  
   1.664 @@ -1920,49 +1827,37 @@
   1.665  
   1.666  lemma brouwer:
   1.667    fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
   1.668 -  assumes "compact s"
   1.669 -    and "convex s"
   1.670 -    and "s \<noteq> {}"
   1.671 -    and "continuous_on s f"
   1.672 -    and "f ` s \<subseteq> s"
   1.673 -  obtains x where "x \<in> s" and "f x = x"
   1.674 +  assumes S: "compact S" "convex S" "S \<noteq> {}"
   1.675 +    and contf: "continuous_on S f"
   1.676 +    and fim: "f ` S \<subseteq> S"
   1.677 +  obtains x where "x \<in> S" and "f x = x"
   1.678  proof -
   1.679 -  have "\<exists>e>0. s \<subseteq> cball 0 e"
   1.680 -    using compact_imp_bounded[OF assms(1)]
   1.681 -    unfolding bounded_pos
   1.682 -    apply (erule_tac exE)
   1.683 -    apply (rule_tac x=b in exI)
   1.684 -    apply (auto simp add: dist_norm)
   1.685 -    done
   1.686 -  then obtain e where e: "e > 0" "s \<subseteq> cball 0 e"
   1.687 +  have "\<exists>e>0. S \<subseteq> cball 0 e"
   1.688 +    using compact_imp_bounded[OF \<open>compact S\<close>]  unfolding bounded_pos
   1.689 +    by auto
   1.690 +  then obtain e where e: "e > 0" "S \<subseteq> cball 0 e"
   1.691      by blast
   1.692 -  have "\<exists>x\<in> cball 0 e. (f \<circ> closest_point s) x = x"
   1.693 -    apply (rule_tac brouwer_ball[OF e(1), of 0 "f \<circ> closest_point s"])
   1.694 -    apply (rule continuous_on_compose )
   1.695 -    apply (rule continuous_on_closest_point[OF assms(2) compact_imp_closed[OF assms(1)] assms(3)])
   1.696 -    apply (rule continuous_on_subset[OF assms(4)])
   1.697 -    apply (insert closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3)])
   1.698 -    using assms(5)[unfolded subset_eq]
   1.699 -    using e(2)[unfolded subset_eq mem_cball]
   1.700 -    apply (auto simp add: dist_norm)
   1.701 -    done
   1.702 -  then obtain x where x: "x \<in> cball 0 e" "(f \<circ> closest_point s) x = x" ..
   1.703 -  have *: "closest_point s x = x"
   1.704 -    apply (rule closest_point_self)
   1.705 -    apply (rule assms(5)[unfolded subset_eq,THEN bspec[where x="x"], unfolded image_iff])
   1.706 -    apply (rule_tac x="closest_point s x" in bexI)
   1.707 -    using x
   1.708 -    unfolding o_def
   1.709 -    using closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3), of x]
   1.710 -    apply auto
   1.711 -    done
   1.712 +  have "\<exists>x\<in> cball 0 e. (f \<circ> closest_point S) x = x"
   1.713 +  proof (rule_tac brouwer_ball[OF e(1)])
   1.714 +    show "continuous_on (cball 0 e) (f \<circ> closest_point S)"
   1.715 +      apply (rule continuous_on_compose)
   1.716 +      using S compact_eq_bounded_closed continuous_on_closest_point apply blast
   1.717 +      by (meson S contf closest_point_in_set compact_imp_closed continuous_on_subset image_subsetI)
   1.718 +    show "(f \<circ> closest_point S) ` cball 0 e \<subseteq> cball 0 e"
   1.719 +      by clarsimp (metis S fim closest_point_exists(1) compact_eq_bounded_closed e(2) image_subset_iff mem_cball_0 subsetCE)
   1.720 +  qed (use assms in auto)
   1.721 +  then obtain x where x: "x \<in> cball 0 e" "(f \<circ> closest_point S) x = x" ..
   1.722 +  have "x \<in> S"
   1.723 +    by (metis closest_point_in_set comp_apply compact_imp_closed fim image_eqI S(1) S(3) subset_iff x(2))
   1.724 +  then have *: "closest_point S x = x"
   1.725 +    by (rule closest_point_self)
   1.726    show thesis
   1.727 -    apply (rule_tac x="closest_point s x" in that)
   1.728 -    unfolding x(2)[unfolded o_def]
   1.729 -    apply (rule closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3)])
   1.730 -    using *
   1.731 -    apply auto
   1.732 -    done
   1.733 +  proof
   1.734 +    show "closest_point S x \<in> S"
   1.735 +      by (simp add: "*" \<open>x \<in> S\<close>)
   1.736 +    show "f (closest_point S x) = closest_point S x"
   1.737 +      using "*" x(2) by auto
   1.738 +  qed
   1.739  qed
   1.740  
   1.741  text \<open>So we get the no-retraction theorem.\<close>
   1.742 @@ -1975,17 +1870,15 @@
   1.743    assume *: "frontier (cball a e) retract_of (cball a e)"
   1.744    have **: "\<And>xa. a - (2 *\<^sub>R a - xa) = - (a - xa)"
   1.745      using scaleR_left_distrib[of 1 1 a] by auto
   1.746 -  obtain x where x:
   1.747 -      "x \<in> {x. norm (a - x) = e}"
   1.748 -      "2 *\<^sub>R a - x = x"
   1.749 -    apply (rule retract_fixpoint_property[OF *, of "\<lambda>x. scaleR 2 a - x"])
   1.750 -    apply (blast intro: brouwer_ball[OF assms])
   1.751 -    apply (intro continuous_intros)
   1.752 -    unfolding frontier_cball subset_eq Ball_def image_iff dist_norm sphere_def
   1.753 -    apply (auto simp add: ** norm_minus_commute)
   1.754 -    done
   1.755 +  obtain x where x: "x \<in> {x. norm (a - x) = e}" "2 *\<^sub>R a - x = x"
   1.756 +  proof (rule retract_fixpoint_property[OF *, of "\<lambda>x. scaleR 2 a - x"])
   1.757 +    show "continuous_on (frontier (cball a e)) ((-) (2 *\<^sub>R a))"
   1.758 +      by (intro continuous_intros)
   1.759 +    show "(-) (2 *\<^sub>R a) ` frontier (cball a e) \<subseteq> frontier (cball a e)"
   1.760 +      by clarsimp (metis "**" dist_norm norm_minus_cancel)
   1.761 +  qed (auto simp: dist_norm intro: brouwer_ball[OF assms])
   1.762    then have "scaleR 2 a = scaleR 1 x + scaleR 1 x"
   1.763 -    by (auto simp add: algebra_simps)
   1.764 +    by (auto simp: algebra_simps)
   1.765    then have "a = x"
   1.766      unfolding scaleR_left_distrib[symmetric]
   1.767      by auto
   1.768 @@ -2006,11 +1899,7 @@
   1.769    case False
   1.770    then show ?thesis
   1.771      unfolding contractible_def nullhomotopic_from_sphere_extension
   1.772 -    apply (simp add: not_less)
   1.773 -    apply (rule_tac x=id in exI)
   1.774 -    apply (auto simp: continuous_on_def)
   1.775 -    apply (meson dist_not_less_zero le_less less_le_trans)
   1.776 -    done
   1.777 +    using continuous_on_const less_eq_real_def by auto
   1.778  qed
   1.779  
   1.780  lemma connected_sphere_eq:
   1.781 @@ -2035,9 +1924,8 @@
   1.782          by (metis dist_self greater insertI1 less_add_same_cancel1 mem_sphere mult_2 not_le zero_le_dist)
   1.783        then have "finite (sphere a r)"
   1.784          by auto
   1.785 -      with L \<open>r > 0\<close> show "False"
   1.786 -        apply (auto simp: connected_finite_iff_sing)
   1.787 -        using xy by auto
   1.788 +      with L \<open>r > 0\<close> xy show "False"
   1.789 +        using connected_finite_iff_sing by auto
   1.790      qed
   1.791      with greater show ?rhs
   1.792        by (metis DIM_ge_Suc0 One_nat_def Suc_1 le_antisym not_less_eq_eq)
   1.793 @@ -2098,12 +1986,10 @@
   1.794      unfolding retraction_def
   1.795    proof (intro conjI ballI)
   1.796      show "frontier (cball a B) \<subseteq> cball a B"
   1.797 -      by (force simp:)
   1.798 +      by force
   1.799      show "continuous_on (cball a B) h"
   1.800        unfolding h_def
   1.801 -      apply (intro continuous_intros)
   1.802 -      using contg continuous_on_subset notga apply auto
   1.803 -      done
   1.804 +      by (intro continuous_intros) (use contg continuous_on_subset notga in auto)
   1.805      show "h ` cball a B \<subseteq> frontier (cball a B)"
   1.806        using \<open>0 < B\<close> by (auto simp: h_def notga dist_norm)
   1.807      show "\<And>x. x \<in> frontier (cball a B) \<Longrightarrow> h x = x"
   1.808 @@ -2117,76 +2003,76 @@
   1.809  subsection\<open>More Properties of Retractions\<close>
   1.810  
   1.811  lemma retraction:
   1.812 -   "retraction s t r \<longleftrightarrow>
   1.813 -    t \<subseteq> s \<and> continuous_on s r \<and> r ` s = t \<and> (\<forall>x \<in> t. r x = x)"
   1.814 +   "retraction S T r \<longleftrightarrow>
   1.815 +    T \<subseteq> S \<and> continuous_on S r \<and> r ` S = T \<and> (\<forall>x \<in> T. r x = x)"
   1.816  by (force simp: retraction_def)
   1.817  
   1.818  lemma retract_of_imp_extensible:
   1.819 -  assumes "s retract_of t" and "continuous_on s f" and "f ` s \<subseteq> u"
   1.820 -  obtains g where "continuous_on t g" "g ` t \<subseteq> u" "\<And>x. x \<in> s \<Longrightarrow> g x = f x"
   1.821 +  assumes "S retract_of T" and "continuous_on S f" and "f ` S \<subseteq> U"
   1.822 +  obtains g where "continuous_on T g" "g ` T \<subseteq> U" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
   1.823  using assms
   1.824  apply (clarsimp simp add: retract_of_def retraction)
   1.825 -apply (rule_tac g = "f o r" in that)
   1.826 +apply (rule_tac g = "f \<circ> r" in that)
   1.827  apply (auto simp: continuous_on_compose2)
   1.828  done
   1.829  
   1.830  lemma idempotent_imp_retraction:
   1.831 -  assumes "continuous_on s f" and "f ` s \<subseteq> s" and "\<And>x. x \<in> s \<Longrightarrow> f(f x) = f x"
   1.832 -    shows "retraction s (f ` s) f"
   1.833 +  assumes "continuous_on S f" and "f ` S \<subseteq> S" and "\<And>x. x \<in> S \<Longrightarrow> f(f x) = f x"
   1.834 +    shows "retraction S (f ` S) f"
   1.835  by (simp add: assms retraction)
   1.836  
   1.837  lemma retraction_subset:
   1.838 -  assumes "retraction s t r" and "t \<subseteq> s'" and "s' \<subseteq> s"
   1.839 -    shows "retraction s' t r"
   1.840 -apply (simp add: retraction_def)
   1.841 -by (metis assms continuous_on_subset image_mono retraction)
   1.842 +  assumes "retraction S T r" and "T \<subseteq> s'" and "s' \<subseteq> S"
   1.843 +  shows "retraction s' T r"
   1.844 +  unfolding retraction_def
   1.845 +  by (metis assms continuous_on_subset image_mono retraction)
   1.846  
   1.847  lemma retract_of_subset:
   1.848 -  assumes "t retract_of s" and "t \<subseteq> s'" and "s' \<subseteq> s"
   1.849 -    shows "t retract_of s'"
   1.850 +  assumes "T retract_of S" and "T \<subseteq> s'" and "s' \<subseteq> S"
   1.851 +    shows "T retract_of s'"
   1.852  by (meson assms retract_of_def retraction_subset)
   1.853  
   1.854 -lemma retraction_refl [simp]: "retraction s s (\<lambda>x. x)"
   1.855 +lemma retraction_refl [simp]: "retraction S S (\<lambda>x. x)"
   1.856  by (simp add: continuous_on_id retraction)
   1.857  
   1.858 -lemma retract_of_refl [iff]: "s retract_of s"
   1.859 +lemma retract_of_refl [iff]: "S retract_of S"
   1.860    using continuous_on_id retract_of_def retraction_def by fastforce
   1.861  
   1.862  lemma retract_of_imp_subset:
   1.863 -   "s retract_of t \<Longrightarrow> s \<subseteq> t"
   1.864 +   "S retract_of T \<Longrightarrow> S \<subseteq> T"
   1.865  by (simp add: retract_of_def retraction_def)
   1.866  
   1.867  lemma retract_of_empty [simp]:
   1.868 -     "({} retract_of s) \<longleftrightarrow> s = {}"  "(s retract_of {}) \<longleftrightarrow> s = {}"
   1.869 +     "({} retract_of S) \<longleftrightarrow> S = {}"  "(S retract_of {}) \<longleftrightarrow> S = {}"
   1.870  by (auto simp: retract_of_def retraction_def)
   1.871  
   1.872 -lemma retract_of_singleton [iff]: "({x} retract_of s) \<longleftrightarrow> x \<in> s"
   1.873 +lemma retract_of_singleton [iff]: "({x} retract_of S) \<longleftrightarrow> x \<in> S"
   1.874    using continuous_on_const
   1.875    by (auto simp: retract_of_def retraction_def)
   1.876  
   1.877  lemma retraction_comp:
   1.878 -   "\<lbrakk>retraction s t f; retraction t u g\<rbrakk>
   1.879 -        \<Longrightarrow> retraction s u (g o f)"
   1.880 +   "\<lbrakk>retraction S T f; retraction T U g\<rbrakk>
   1.881 +        \<Longrightarrow> retraction S U (g \<circ> f)"
   1.882  apply (auto simp: retraction_def intro: continuous_on_compose2)
   1.883  by blast
   1.884  
   1.885  lemma retract_of_trans [trans]:
   1.886 -  assumes "s retract_of t" and "t retract_of u"
   1.887 -    shows "s retract_of u"
   1.888 +  assumes "S retract_of T" and "T retract_of U"
   1.889 +    shows "S retract_of U"
   1.890  using assms by (auto simp: retract_of_def intro: retraction_comp)
   1.891  
   1.892  lemma closedin_retract:
   1.893 -  fixes s :: "'a :: real_normed_vector set"
   1.894 -  assumes "s retract_of t"
   1.895 -    shows "closedin (subtopology euclidean t) s"
   1.896 +  fixes S :: "'a :: real_normed_vector set"
   1.897 +  assumes "S retract_of T"
   1.898 +    shows "closedin (subtopology euclidean T) S"
   1.899  proof -
   1.900 -  obtain r where "s \<subseteq> t" "continuous_on t r" "r ` t \<subseteq> s" "\<And>x. x \<in> s \<Longrightarrow> r x = x"
   1.901 +  obtain r where "S \<subseteq> T" "continuous_on T r" "r ` T \<subseteq> S" "\<And>x. x \<in> S \<Longrightarrow> r x = x"
   1.902      using assms by (auto simp: retract_of_def retraction_def)
   1.903 -  then have s: "s = {x \<in> t. (norm(r x - x)) = 0}" by auto
   1.904 +  then have S: "S = {x \<in> T. (norm(r x - x)) = 0}" by auto
   1.905    show ?thesis
   1.906 -    apply (subst s)
   1.907 +    apply (subst S)
   1.908      apply (rule continuous_closedin_preimage_constant)
   1.909 -    by (simp add: \<open>continuous_on t r\<close> continuous_on_diff continuous_on_id continuous_on_norm)
   1.910 +    by (simp add: \<open>continuous_on T r\<close> continuous_on_diff continuous_on_id continuous_on_norm)
   1.911  qed
   1.912  
   1.913  lemma closedin_self [simp]:
   1.914 @@ -2195,52 +2081,52 @@
   1.915    by (simp add: closedin_retract)
   1.916  
   1.917  lemma retract_of_contractible:
   1.918 -  assumes "contractible t" "s retract_of t"
   1.919 -    shows "contractible s"
   1.920 +  assumes "contractible T" "S retract_of T"
   1.921 +    shows "contractible S"
   1.922  using assms
   1.923  apply (clarsimp simp add: retract_of_def contractible_def retraction_def homotopic_with)
   1.924  apply (rule_tac x="r a" in exI)
   1.925 -apply (rule_tac x="r o h" in exI)
   1.926 +apply (rule_tac x="r \<circ> h" in exI)
   1.927  apply (intro conjI continuous_intros continuous_on_compose)
   1.928  apply (erule continuous_on_subset | force)+
   1.929  done
   1.930  
   1.931  lemma retract_of_compact:
   1.932 -     "\<lbrakk>compact t; s retract_of t\<rbrakk> \<Longrightarrow> compact s"
   1.933 +     "\<lbrakk>compact T; S retract_of T\<rbrakk> \<Longrightarrow> compact S"
   1.934    by (metis compact_continuous_image retract_of_def retraction)
   1.935  
   1.936  lemma retract_of_closed:
   1.937 -    fixes s :: "'a :: real_normed_vector set"
   1.938 -    shows "\<lbrakk>closed t; s retract_of t\<rbrakk> \<Longrightarrow> closed s"
   1.939 +    fixes S :: "'a :: real_normed_vector set"
   1.940 +    shows "\<lbrakk>closed T; S retract_of T\<rbrakk> \<Longrightarrow> closed S"
   1.941    by (metis closedin_retract closedin_closed_eq)
   1.942  
   1.943  lemma retract_of_connected:
   1.944 -    "\<lbrakk>connected t; s retract_of t\<rbrakk> \<Longrightarrow> connected s"
   1.945 +    "\<lbrakk>connected T; S retract_of T\<rbrakk> \<Longrightarrow> connected S"
   1.946    by (metis Topological_Spaces.connected_continuous_image retract_of_def retraction)
   1.947  
   1.948  lemma retract_of_path_connected:
   1.949 -    "\<lbrakk>path_connected t; s retract_of t\<rbrakk> \<Longrightarrow> path_connected s"
   1.950 +    "\<lbrakk>path_connected T; S retract_of T\<rbrakk> \<Longrightarrow> path_connected S"
   1.951    by (metis path_connected_continuous_image retract_of_def retraction)
   1.952  
   1.953  lemma retract_of_simply_connected:
   1.954 -    "\<lbrakk>simply_connected t; s retract_of t\<rbrakk> \<Longrightarrow> simply_connected s"
   1.955 +    "\<lbrakk>simply_connected T; S retract_of T\<rbrakk> \<Longrightarrow> simply_connected S"
   1.956  apply (simp add: retract_of_def retraction_def, clarify)
   1.957  apply (rule simply_connected_retraction_gen)
   1.958  apply (force simp: continuous_on_id elim!: continuous_on_subset)+
   1.959  done
   1.960  
   1.961  lemma retract_of_homotopically_trivial:
   1.962 -  assumes ts: "t retract_of s"
   1.963 -      and hom: "\<And>f g. \<lbrakk>continuous_on u f; f ` u \<subseteq> s;
   1.964 -                       continuous_on u g; g ` u \<subseteq> s\<rbrakk>
   1.965 -                       \<Longrightarrow> homotopic_with (\<lambda>x. True) u s f g"
   1.966 -      and "continuous_on u f" "f ` u \<subseteq> t"
   1.967 -      and "continuous_on u g" "g ` u \<subseteq> t"
   1.968 -    shows "homotopic_with (\<lambda>x. True) u t f g"
   1.969 +  assumes ts: "T retract_of S"
   1.970 +      and hom: "\<And>f g. \<lbrakk>continuous_on U f; f ` U \<subseteq> S;
   1.971 +                       continuous_on U g; g ` U \<subseteq> S\<rbrakk>
   1.972 +                       \<Longrightarrow> homotopic_with (\<lambda>x. True) U S f g"
   1.973 +      and "continuous_on U f" "f ` U \<subseteq> T"
   1.974 +      and "continuous_on U g" "g ` U \<subseteq> T"
   1.975 +    shows "homotopic_with (\<lambda>x. True) U T f g"
   1.976  proof -
   1.977 -  obtain r where "r ` s \<subseteq> s" "continuous_on s r" "\<forall>x\<in>s. r (r x) = r x" "t = r ` s"
   1.978 +  obtain r where "r ` S \<subseteq> S" "continuous_on S r" "\<forall>x\<in>S. r (r x) = r x" "T = r ` S"
   1.979      using ts by (auto simp: retract_of_def retraction)
   1.980 -  then obtain k where "Retracts s r t k"
   1.981 +  then obtain k where "Retracts S r T k"
   1.982      unfolding Retracts_def
   1.983      by (metis continuous_on_subset dual_order.trans image_iff image_mono)
   1.984    then show ?thesis
   1.985 @@ -2251,15 +2137,15 @@
   1.986  qed
   1.987  
   1.988  lemma retract_of_homotopically_trivial_null:
   1.989 -  assumes ts: "t retract_of s"
   1.990 -      and hom: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s\<rbrakk>
   1.991 -                     \<Longrightarrow> \<exists>c. homotopic_with (\<lambda>x. True) u s f (\<lambda>x. c)"
   1.992 -      and "continuous_on u f" "f ` u \<subseteq> t"
   1.993 -  obtains c where "homotopic_with (\<lambda>x. True) u t f (\<lambda>x. c)"
   1.994 +  assumes ts: "T retract_of S"
   1.995 +      and hom: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> S\<rbrakk>
   1.996 +                     \<Longrightarrow> \<exists>c. homotopic_with (\<lambda>x. True) U S f (\<lambda>x. c)"
   1.997 +      and "continuous_on U f" "f ` U \<subseteq> T"
   1.998 +  obtains c where "homotopic_with (\<lambda>x. True) U T f (\<lambda>x. c)"
   1.999  proof -
  1.1000 -  obtain r where "r ` s \<subseteq> s" "continuous_on s r" "\<forall>x\<in>s. r (r x) = r x" "t = r ` s"
  1.1001 +  obtain r where "r ` S \<subseteq> S" "continuous_on S r" "\<forall>x\<in>S. r (r x) = r x" "T = r ` S"
  1.1002      using ts by (auto simp: retract_of_def retraction)
  1.1003 -  then obtain k where "Retracts s r t k"
  1.1004 +  then obtain k where "Retracts S r T k"
  1.1005      unfolding Retracts_def
  1.1006      by (metis continuous_on_subset dual_order.trans image_iff image_mono)
  1.1007    then show ?thesis
  1.1008 @@ -2269,35 +2155,34 @@
  1.1009  qed
  1.1010  
  1.1011  lemma retraction_imp_quotient_map:
  1.1012 -   "retraction s t r
  1.1013 -    \<Longrightarrow> u \<subseteq> t
  1.1014 -            \<Longrightarrow> (openin (subtopology euclidean s) (s \<inter> r -` u) \<longleftrightarrow>
  1.1015 -                 openin (subtopology euclidean t) u)"
  1.1016 +   "retraction S T r
  1.1017 +    \<Longrightarrow> U \<subseteq> T
  1.1018 +            \<Longrightarrow> (openin (subtopology euclidean S) (S \<inter> r -` U) \<longleftrightarrow>
  1.1019 +                 openin (subtopology euclidean T) U)"
  1.1020  apply (clarsimp simp add: retraction)
  1.1021  apply (rule continuous_right_inverse_imp_quotient_map [where g=r])
  1.1022  apply (auto simp: elim: continuous_on_subset)
  1.1023  done
  1.1024  
  1.1025  lemma retract_of_locally_compact:
  1.1026 -    fixes s :: "'a :: {heine_borel,real_normed_vector} set"
  1.1027 -    shows  "\<lbrakk> locally compact s; t retract_of s\<rbrakk> \<Longrightarrow> locally compact t"
  1.1028 +    fixes S :: "'a :: {heine_borel,real_normed_vector} set"
  1.1029 +    shows  "\<lbrakk> locally compact S; T retract_of S\<rbrakk> \<Longrightarrow> locally compact T"
  1.1030    by (metis locally_compact_closedin closedin_retract)
  1.1031  
  1.1032  lemma retract_of_Times:
  1.1033 -   "\<lbrakk>s retract_of s'; t retract_of t'\<rbrakk> \<Longrightarrow> (s \<times> t) retract_of (s' \<times> t')"
  1.1034 +   "\<lbrakk>S retract_of s'; T retract_of t'\<rbrakk> \<Longrightarrow> (S \<times> T) retract_of (s' \<times> t')"
  1.1035  apply (simp add: retract_of_def retraction_def Sigma_mono, clarify)
  1.1036  apply (rename_tac f g)
  1.1037 -apply (rule_tac x="\<lambda>z. ((f o fst) z, (g o snd) z)" in exI)
  1.1038 +apply (rule_tac x="\<lambda>z. ((f \<circ> fst) z, (g \<circ> snd) z)" in exI)
  1.1039  apply (rule conjI continuous_intros | erule continuous_on_subset | force)+
  1.1040  done
  1.1041  
  1.1042  lemma homotopic_into_retract:
  1.1043 -   "\<lbrakk>f ` s \<subseteq> t; g ` s \<subseteq> t; t retract_of u;
  1.1044 -        homotopic_with (\<lambda>x. True) s u f g\<rbrakk>
  1.1045 -        \<Longrightarrow> homotopic_with (\<lambda>x. True) s t f g"
  1.1046 +   "\<lbrakk>f ` S \<subseteq> T; g ` S \<subseteq> T; T retract_of U; homotopic_with (\<lambda>x. True) S U f g\<rbrakk>
  1.1047 +        \<Longrightarrow> homotopic_with (\<lambda>x. True) S T f g"
  1.1048  apply (subst (asm) homotopic_with_def)
  1.1049  apply (simp add: homotopic_with retract_of_def retraction_def, clarify)
  1.1050 -apply (rule_tac x="r o h" in exI)
  1.1051 +apply (rule_tac x="r \<circ> h" in exI)
  1.1052  apply (rule conjI continuous_intros | erule continuous_on_subset | force simp: image_subset_iff)+
  1.1053  done
  1.1054  
  1.1055 @@ -2317,15 +2202,19 @@
  1.1056  
  1.1057  lemma deformation_retract_imp_homotopy_eqv:
  1.1058    fixes S :: "'a::euclidean_space set"
  1.1059 -  assumes "homotopic_with (\<lambda>x. True) S S id r" "retraction S T r"
  1.1060 -    shows "S homotopy_eqv T"
  1.1061 -  apply (simp add: homotopy_eqv_def)
  1.1062 -  apply (rule_tac x=r in exI)
  1.1063 -  using assms apply (simp add: retraction_def)
  1.1064 -  apply (rule_tac x=id in exI)
  1.1065 -  apply (auto simp: continuous_on_id)
  1.1066 -   apply (metis homotopic_with_symD)
  1.1067 -  by (metis continuous_on_id' homotopic_with_equal homotopic_with_symD id_apply image_id subset_refl)
  1.1068 +  assumes "homotopic_with (\<lambda>x. True) S S id r" and r: "retraction S T r"
  1.1069 +  shows "S homotopy_eqv T"
  1.1070 +proof -
  1.1071 +  have "homotopic_with (\<lambda>x. True) S S (id \<circ> r) id"
  1.1072 +    by (simp add: assms(1) homotopic_with_symD)
  1.1073 +  moreover have "homotopic_with (\<lambda>x. True) T T (r \<circ> id) id"
  1.1074 +    using r unfolding retraction_def
  1.1075 +    by (metis (no_types, lifting) comp_id continuous_on_id' homotopic_with_equal homotopic_with_symD id_def image_id order_refl)
  1.1076 +  ultimately
  1.1077 +  show ?thesis
  1.1078 +    unfolding homotopy_eqv_def
  1.1079 +    by (metis continuous_on_id' id_def image_id r retraction_def)
  1.1080 +qed
  1.1081  
  1.1082  lemma deformation_retract:
  1.1083    fixes S :: "'a::euclidean_space set"
  1.1084 @@ -2356,10 +2245,8 @@
  1.1085    have "{a} retract_of S"
  1.1086      by (simp add: \<open>a \<in> S\<close>)
  1.1087    moreover have "homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
  1.1088 -    using assms
  1.1089 -    apply (clarsimp simp add: contractible_def)
  1.1090 -    apply (rule homotopic_with_trans, assumption)
  1.1091 -    by (metis assms(1) contractible_imp_path_connected homotopic_constant_maps homotopic_with_sym homotopic_with_trans insert_absorb insert_not_empty path_component_mem(1) path_connected_component)
  1.1092 +      using assms
  1.1093 +      by (auto simp: contractible_def continuous_on_const continuous_on_id homotopic_into_contractible image_subset_iff)
  1.1094    moreover have "(\<lambda>x. a) ` S \<subseteq> {a}"
  1.1095      by (simp add: image_subsetI)
  1.1096    ultimately show ?thesis
  1.1097 @@ -2382,15 +2269,12 @@
  1.1098      using assms by auto (metis imageI subset_iff)
  1.1099    have contp': "continuous_on S p"
  1.1100      by (rule continuous_on_subset [OF contp \<open>S \<subseteq> T\<close>])
  1.1101 -  have "continuous_on T (q \<circ> p)"
  1.1102 -    apply (rule continuous_on_compose [OF contp])
  1.1103 -    apply (simp add: *)
  1.1104 -    apply (rule continuous_on_inv [OF contp' \<open>compact S\<close>])
  1.1105 -    using assms by auto
  1.1106 +  have "continuous_on (p ` T) q"
  1.1107 +    by (simp add: "*" assms(1) assms(2) assms(5) continuous_on_inv contp' rev_subsetD)
  1.1108 +  then have "continuous_on T (q \<circ> p)"
  1.1109 +    by (rule continuous_on_compose [OF contp])
  1.1110    then show ?thesis
  1.1111 -    apply (rule continuous_on_eq [of _ "q o p"])
  1.1112 -    apply (simp add: o_def)
  1.1113 -    done
  1.1114 +    by (rule continuous_on_eq [of _ "q \<circ> p"]) (simp add: o_def)
  1.1115  qed
  1.1116  
  1.1117  lemma continuous_on_compact_surface_projection:
  1.1118 @@ -2441,21 +2325,19 @@
  1.1119    have aaffS: "a \<in> affine hull S"
  1.1120      by (meson arelS subsetD hull_inc rel_interior_subset)
  1.1121    have "((\<lambda>z. z - a) ` (affine hull S - {a})) = ((\<lambda>z. z - a) ` (affine hull S)) - {0}"
  1.1122 -    by (auto simp: )
  1.1123 +    by auto
  1.1124    moreover have "continuous_on (((\<lambda>z. z - a) ` (affine hull S)) - {0}) (\<lambda>x. dd x *\<^sub>R x)"
  1.1125    proof (rule continuous_on_compact_surface_projection)
  1.1126      show "compact (rel_frontier ((\<lambda>z. z - a) ` S))"
  1.1127        by (simp add: \<open>bounded S\<close> bounded_translation_minus compact_rel_frontier_bounded)
  1.1128      have releq: "rel_frontier ((\<lambda>z. z - a) ` S) = (\<lambda>z. z - a) ` rel_frontier S"
  1.1129        using rel_frontier_translation [of "-a"] add.commute by simp
  1.1130 -    also have "... \<subseteq> (\<lambda>z. z - a) ` (affine hull S) - {0}"
  1.1131 +    also have "\<dots> \<subseteq> (\<lambda>z. z - a) ` (affine hull S) - {0}"
  1.1132        using rel_frontier_affine_hull arelS rel_frontier_def by fastforce
  1.1133      finally show "rel_frontier ((\<lambda>z. z - a) ` S) \<subseteq> (\<lambda>z. z - a) ` (affine hull S) - {0}" .
  1.1134      show "cone ((\<lambda>z. z - a) ` (affine hull S))"
  1.1135 -      apply (rule subspace_imp_cone)
  1.1136 -      using aaffS
  1.1137 -      apply (simp add: subspace_affine image_comp o_def affine_translation_aux [of a])
  1.1138 -      done
  1.1139 +      by (rule subspace_imp_cone)
  1.1140 +         (use aaffS in \<open>simp add: subspace_affine image_comp o_def affine_translation_aux [of a]\<close>)
  1.1141      show "(0 < k \<and> k *\<^sub>R x \<in> rel_frontier ((\<lambda>z. z - a) ` S)) \<longleftrightarrow> (dd x = k)"
  1.1142           if x: "x \<in> (\<lambda>z. z - a) ` (affine hull S) - {0}" for k x
  1.1143      proof
  1.1144 @@ -2471,7 +2353,7 @@
  1.1145          then have segsub: "open_segment a (a + k *\<^sub>R x) \<subseteq> rel_interior S"
  1.1146            by (metis rel_interior_closure_convex_segment [OF \<open>convex S\<close> arelS])
  1.1147          have "x \<noteq> 0" and xaffS: "a + x \<in> affine hull S"
  1.1148 -          using x by (auto simp: )
  1.1149 +          using x by auto
  1.1150          then have "0 < dd x" and inS: "a + dd x *\<^sub>R x \<in> rel_frontier S"
  1.1151            using dd1 by auto
  1.1152          moreover have "a + dd x *\<^sub>R x \<in> open_segment a (a + k *\<^sub>R x)"
  1.1153 @@ -2483,7 +2365,7 @@
  1.1154            apply (metis (no_types) \<open>k \<noteq> 0\<close> divide_inverse_commute inverse_eq_divide mult.left_commute right_inverse)
  1.1155            done
  1.1156          ultimately show ?thesis
  1.1157 -          using segsub by (auto simp add: rel_frontier_def)
  1.1158 +          using segsub by (auto simp: rel_frontier_def)
  1.1159        qed
  1.1160        moreover have False if "k < dd x"
  1.1161          using x k that rel_frontier_def
  1.1162 @@ -2497,7 +2379,7 @@
  1.1163    have "continuous_on (affine hull S - {a}) ((\<lambda>x. a + dd x *\<^sub>R x) \<circ> (\<lambda>z. z - a))"
  1.1164      by (intro * continuous_intros continuous_on_compose)
  1.1165    with affS have contdd: "continuous_on (T - {a}) ((\<lambda>x. a + dd x *\<^sub>R x) \<circ> (\<lambda>z. z - a))"
  1.1166 -    by (blast intro: continuous_on_subset elim: )
  1.1167 +    by (blast intro: continuous_on_subset)
  1.1168    show ?thesis
  1.1169    proof
  1.1170      show "homotopic_with (\<lambda>x. True) (T - {a}) (T - {a}) id (\<lambda>x. a + dd (x - a) *\<^sub>R (x - a))"
  1.1171 @@ -2510,11 +2392,10 @@
  1.1172             if "x \<in> T - {a}" for x
  1.1173        proof (clarsimp simp: in_segment, intro conjI)
  1.1174          fix u::real assume u: "0 \<le> u" "u \<le> 1"
  1.1175 -        show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x - a) *\<^sub>R (x - a)) \<in> T"
  1.1176 -          apply (rule convexD [OF \<open>convex T\<close>])
  1.1177 -          using that u apply (auto simp add: )
  1.1178 -          apply (metis add.commute affS dd1 diff_add_cancel eq_iff_diff_eq_0 relS subsetD)
  1.1179 -          done
  1.1180 +        have "a + dd (x - a) *\<^sub>R (x - a) \<in> T"
  1.1181 +          by (metis DiffD1 DiffD2 add.commute add.right_neutral affS dd1 diff_add_cancel relS singletonI subsetCE that)
  1.1182 +        then show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x - a) *\<^sub>R (x - a)) \<in> T"
  1.1183 +          using convexD [OF \<open>convex T\<close>] that u by simp
  1.1184          have iff: "(1 - u) *\<^sub>R x + u *\<^sub>R (a + d *\<^sub>R (x - a)) = a \<longleftrightarrow>
  1.1185                    (1 - u + u * d) *\<^sub>R (x - a) = 0" for d
  1.1186            by (auto simp: algebra_simps)
  1.1187 @@ -2541,7 +2422,7 @@
  1.1188        show "a + dd (x - a) *\<^sub>R (x - a) = x" if x: "x \<in> rel_frontier S" for x
  1.1189        proof -
  1.1190          have "x \<noteq> a"
  1.1191 -          using that arelS by (auto simp add: rel_frontier_def)
  1.1192 +          using that arelS by (auto simp: rel_frontier_def)
  1.1193          have False if "dd (x - a) < 1"
  1.1194          proof -
  1.1195            have "x \<in> closure S"
  1.1196 @@ -2551,7 +2432,7 @@
  1.1197            have  xaffS: "x \<in> affine hull S"
  1.1198              using affS relS x by auto
  1.1199            then have "0 < dd (x - a)" and inS: "a + dd (x - a) *\<^sub>R (x - a) \<in> rel_frontier S"
  1.1200 -            using dd1 by (auto simp add: \<open>x \<noteq> a\<close>)
  1.1201 +            using dd1 by (auto simp: \<open>x \<noteq> a\<close>)
  1.1202            moreover have "a + dd (x - a) *\<^sub>R (x - a) \<in> open_segment a x"
  1.1203              using  \<open>x \<noteq> a\<close> \<open>0 < dd (x - a)\<close>
  1.1204              apply (simp add: in_segment)
  1.1205 @@ -2559,7 +2440,7 @@
  1.1206              apply (simp add: algebra_simps that)
  1.1207              done
  1.1208            ultimately show ?thesis
  1.1209 -            using segsub by (auto simp add: rel_frontier_def)
  1.1210 +            using segsub by (auto simp: rel_frontier_def)
  1.1211          qed
  1.1212          moreover have False if "1 < dd (x - a)"
  1.1213            using x that dd2 [of "x - a" 1] \<open>x \<noteq> a\<close> closure_affine_hull
  1.1214 @@ -2578,7 +2459,7 @@
  1.1215    assumes "bounded S" "convex S" "a \<in> rel_interior S"
  1.1216      shows "rel_frontier S retract_of (affine hull S - {a})"
  1.1217  apply (rule rel_frontier_deformation_retract_of_punctured_convex [of S "affine hull S" a])
  1.1218 -apply (auto simp add: affine_imp_convex rel_frontier_affine_hull retract_of_def assms)
  1.1219 +apply (auto simp: affine_imp_convex rel_frontier_affine_hull retract_of_def assms)
  1.1220  done
  1.1221  
  1.1222  corollary rel_boundary_retract_of_punctured_affine_hull:
  1.1223 @@ -2643,7 +2524,7 @@
  1.1224      using assms by (auto simp: path_component_def)
  1.1225    then show ?thesis
  1.1226      apply (simp add: path_def path_image_def pathstart_def pathfinish_def homotopic_with_def)
  1.1227 -    apply (rule_tac x = "\<lambda>z. inverse(norm(snd z - (g o fst)z)) *\<^sub>R (snd z - (g o fst)z)" in exI)
  1.1228 +    apply (rule_tac x = "\<lambda>z. inverse(norm(snd z - (g \<circ> fst)z)) *\<^sub>R (snd z - (g \<circ> fst)z)" in exI)
  1.1229      apply (intro conjI continuous_intros)
  1.1230      apply (rule continuous_intros | erule continuous_on_subset | fastforce simp: divide_simps sphere_def)+
  1.1231      done
  1.1232 @@ -2767,7 +2648,7 @@
  1.1233      using hom by (force simp: homeomorphic_def)
  1.1234    then have "continuous_on (f ` T) g"
  1.1235      by (meson \<open>f ` T \<subseteq> S\<close> continuous_on_subset homeomorphism_def)
  1.1236 -  then have contgf: "continuous_on T (g o f)"
  1.1237 +  then have contgf: "continuous_on T (g \<circ> f)"
  1.1238      by (metis continuous_on_compose contf)
  1.1239    have gfTC: "(g \<circ> f) ` T \<subseteq> C"
  1.1240    proof -
  1.1241 @@ -2779,7 +2660,7 @@
  1.1242                        "\<And>x. x \<in> T \<Longrightarrow> f' x = (g \<circ> f) x"
  1.1243      by (metis Dugundji [OF C cloUT contgf gfTC])
  1.1244    show ?thesis
  1.1245 -  proof (rule_tac g = "h o r o f'" in that)
  1.1246 +  proof (rule_tac g = "h \<circ> r \<circ> f'" in that)
  1.1247      show "continuous_on U (h \<circ> r \<circ> f')"
  1.1248        apply (intro continuous_on_compose f')
  1.1249         using continuous_on_subset contr f' apply blast
  1.1250 @@ -2811,7 +2692,7 @@
  1.1251    have [simp]: "S' \<subseteq> U" using clo closedin_limpt by blast
  1.1252    show ?thesis
  1.1253    proof (simp add: retraction_def retract_of_def, intro exI conjI)
  1.1254 -    show "continuous_on U (g o h')"
  1.1255 +    show "continuous_on U (g \<circ> h')"
  1.1256        apply (intro continuous_on_compose h')
  1.1257        apply (meson hom continuous_on_subset h' homeomorphism_cont1)
  1.1258        done
  1.1259 @@ -2853,7 +2734,7 @@
  1.1260      using clo closedin_imp_subset by auto
  1.1261    show "T retract_of U"
  1.1262    proof (simp add: retraction_def retract_of_def, intro exI conjI)
  1.1263 -    show "continuous_on U (g o h')"
  1.1264 +    show "continuous_on U (g \<circ> h')"
  1.1265        apply (intro continuous_on_compose h')
  1.1266        apply (meson hom continuous_on_subset h' homeomorphism_cont1)
  1.1267        done
  1.1268 @@ -2919,7 +2800,7 @@
  1.1269      using hom by (force simp: homeomorphic_def)
  1.1270    have "continuous_on (f ` T) g"
  1.1271      by (meson \<open>f ` T \<subseteq> S\<close> continuous_on_subset homeomorphism_def homgh)
  1.1272 -  then have contgf: "continuous_on T (g o f)"
  1.1273 +  then have contgf: "continuous_on T (g \<circ> f)"
  1.1274      by (intro continuous_on_compose contf)
  1.1275    have gfTC: "(g \<circ> f) ` T \<subseteq> C"
  1.1276    proof -
  1.1277 @@ -2933,7 +2814,7 @@
  1.1278                and eq: "\<And>x. x \<in> T \<Longrightarrow> f' x = (g \<circ> f) x"
  1.1279      by (metis Dugundji [OF C cloUT contgf gfTC])
  1.1280    show ?thesis
  1.1281 -  proof (rule_tac V = "U \<inter> f' -` D" and g = "h o r o f'" in that)
  1.1282 +  proof (rule_tac V = "U \<inter> f' -` D" and g = "h \<circ> r \<circ> f'" in that)
  1.1283      show "T \<subseteq> U \<inter> f' -` D"
  1.1284        using cloUT closedin_imp_subset \<open>S' \<subseteq> D\<close> \<open>f ` T \<subseteq> S\<close> eq homeomorphism_image1 homgh
  1.1285        by fastforce
  1.1286 @@ -2976,7 +2857,7 @@
  1.1287      by (blast intro: ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> h clo])
  1.1288    have "S' retract_of V"
  1.1289    proof (simp add: retraction_def retract_of_def, intro exI conjI \<open>S' \<subseteq> V\<close>)
  1.1290 -    show "continuous_on V (g o h')"
  1.1291 +    show "continuous_on V (g \<circ> h')"
  1.1292        apply (intro continuous_on_compose h')
  1.1293        apply (meson hom continuous_on_subset h' homeomorphism_cont1)
  1.1294        done
  1.1295 @@ -3029,7 +2910,7 @@
  1.1296      using clo closedin_imp_subset by auto
  1.1297    have "T retract_of V"
  1.1298    proof (simp add: retraction_def retract_of_def, intro exI conjI \<open>T \<subseteq> V\<close>)
  1.1299 -    show "continuous_on V (g o h')"
  1.1300 +    show "continuous_on V (g \<circ> h')"
  1.1301        apply (intro continuous_on_compose h')
  1.1302        apply (meson hom continuous_on_subset h' homeomorphism_cont1)
  1.1303        done
  1.1304 @@ -3086,7 +2967,7 @@
  1.1305      using Diff_subset_conv \<open>U - Z \<subseteq> W\<close> by blast
  1.1306    ultimately show ?thesis
  1.1307      apply (rule_tac V=V and W = "U-W" in that)
  1.1308 -    using openin_imp_subset apply (force simp:)+
  1.1309 +    using openin_imp_subset apply force+
  1.1310      done
  1.1311  qed
  1.1312  
  1.1313 @@ -3146,7 +3027,7 @@
  1.1314    proof (simp add: retraction_def retract_of_def, intro exI conjI)
  1.1315      show "S' \<subseteq> W" "S' \<subseteq> h -` X"
  1.1316        using him WS' closedin_imp_subset by blast+
  1.1317 -    show "continuous_on (W \<inter> h -` X) (f o r o h)"
  1.1318 +    show "continuous_on (W \<inter> h -` X) (f \<circ> r \<circ> h)"
  1.1319      proof (intro continuous_on_compose)
  1.1320        show "continuous_on (W \<inter> h -` X) h"
  1.1321          by (meson conth continuous_on_subset inf_le1)
  1.1322 @@ -3356,7 +3237,7 @@
  1.1323  apply (clarsimp elim!: all_forward)
  1.1324  apply (erule impCE, metis subset_trans)
  1.1325  apply (clarsimp elim!: ex_forward)
  1.1326 -apply (rule_tac x="r o g" in exI)
  1.1327 +apply (rule_tac x="r \<circ> g" in exI)
  1.1328  by (metis comp_apply continuous_on_compose continuous_on_subset subsetD imageI image_comp image_mono subset_trans)
  1.1329  
  1.1330  lemma AR_retract_of_AR:
  1.1331 @@ -3642,7 +3523,7 @@
  1.1332    obtain r0
  1.1333      where "S \<inter> T \<subseteq> W0" and contr0: "continuous_on W0 r0" and "r0 ` W0 \<subseteq> S \<inter> T"
  1.1334        and r0 [simp]: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> r0 x = x"
  1.1335 -    using ret  by (force simp add: retract_of_def retraction_def)
  1.1336 +    using ret  by (force simp: retract_of_def retraction_def)
  1.1337    have ST: "x \<in> W \<Longrightarrow> x \<in> S \<longleftrightarrow> x \<in> T" for x
  1.1338      using assms by (auto simp: W_def setdist_sing_in_set dest!: setdist_eq_0_closedin)
  1.1339    define r where "r \<equiv> \<lambda>x. if x \<in> W0 then r0 x else x"
  1.1340 @@ -3667,8 +3548,7 @@
  1.1341                  and opeSW1: "openin (subtopology euclidean S') W1"
  1.1342                  and "g ` W1 \<subseteq> S" and geqr: "\<And>x. x \<in> W0 \<union> S \<Longrightarrow> g x = r x"
  1.1343      apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> _ \<open>r ` (W0 \<union> S) \<subseteq> S\<close> cloS'WS])
  1.1344 -     apply (rule continuous_on_subset [OF contr])
  1.1345 -    apply (blast intro:  elim: )+
  1.1346 +     apply (rule continuous_on_subset [OF contr], blast+)
  1.1347      done
  1.1348    have cloT'WT: "closedin (subtopology euclidean T') (W0 \<union> T)"
  1.1349      by (meson closedin_subset_trans UT cloUT' \<open>T \<subseteq> T'\<close> \<open>W \<subseteq> T'\<close> cloUW cloWW0 
  1.1350 @@ -3677,13 +3557,12 @@
  1.1351                  and opeSW2: "openin (subtopology euclidean T') W2"
  1.1352                  and "h ` W2 \<subseteq> T" and heqr: "\<And>x. x \<in> W0 \<union> T \<Longrightarrow> h x = r x"
  1.1353      apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> _ \<open>r ` (W0 \<union> T) \<subseteq> T\<close> cloT'WT])
  1.1354 -     apply (rule continuous_on_subset [OF contr])
  1.1355 -    apply (blast intro:  elim: )+
  1.1356 +     apply (rule continuous_on_subset [OF contr], blast+)
  1.1357      done
  1.1358    have "S' \<inter> T' = W"
  1.1359      by (force simp: S'_def T'_def W_def)
  1.1360    obtain O1 O2 where "open O1" "W1 = S' \<inter> O1" "open O2" "W2 = T' \<inter> O2"
  1.1361 -    using opeSW1 opeSW2 by (force simp add: openin_open)
  1.1362 +    using opeSW1 opeSW2 by (force simp: openin_open)
  1.1363    show ?thesis
  1.1364    proof
  1.1365      have eq: "W1 - (W - U0) \<union> (W2 - (W - U0)) =
  1.1366 @@ -3692,25 +3571,23 @@
  1.1367        by (auto simp: \<open>S' \<union> T' = U\<close> [symmetric] \<open>S' \<inter> T' = W\<close> [symmetric] \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close>)
  1.1368      show "openin (subtopology euclidean U) (W1 - (W - U0) \<union> (W2 - (W - U0)))"
  1.1369        apply (subst eq)
  1.1370 -      apply (intro openin_Un openin_Int_open openin_diff closedin_diff cloUW opeUU0 cloUS' cloUT' \<open>open O1\<close> \<open>open O2\<close>)
  1.1371 -      apply simp_all
  1.1372 +      apply (intro openin_Un openin_Int_open openin_diff closedin_diff cloUW opeUU0 cloUS' cloUT' \<open>open O1\<close> \<open>open O2\<close>, simp_all)
  1.1373        done
  1.1374      have cloW1: "closedin (subtopology euclidean (W1 - (W - U0) \<union> (W2 - (W - U0)))) (W1 - (W - U0))"
  1.1375        using cloUS' apply (simp add: closedin_closed)
  1.1376        apply (erule ex_forward)
  1.1377        using U0 \<open>W0 \<union> S \<subseteq> W1\<close>
  1.1378 -      apply (auto simp add: \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<union> T' = U\<close> [symmetric]\<open>S' \<inter> T' = W\<close> [symmetric])
  1.1379 +      apply (auto simp: \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<union> T' = U\<close> [symmetric]\<open>S' \<inter> T' = W\<close> [symmetric])
  1.1380        done
  1.1381      have cloW2: "closedin (subtopology euclidean (W1 - (W - U0) \<union> (W2 - (W - U0)))) (W2 - (W - U0))"
  1.1382        using cloUT' apply (simp add: closedin_closed)
  1.1383        apply (erule ex_forward)
  1.1384        using U0 \<open>W0 \<union> T \<subseteq> W2\<close>
  1.1385 -      apply (auto simp add: \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<union> T' = U\<close> [symmetric]\<open>S' \<inter> T' = W\<close> [symmetric])
  1.1386 +      apply (auto simp: \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<union> T' = U\<close> [symmetric]\<open>S' \<inter> T' = W\<close> [symmetric])
  1.1387        done
  1.1388      have *: "\<forall>x\<in>S \<union> T. (if x \<in> S' then g x else h x) = x"
  1.1389        using ST \<open>S' \<inter> T' = W\<close> cloT'WT closedin_subset geqr heqr 
  1.1390 -      apply (auto simp: r_def)
  1.1391 -       apply fastforce
  1.1392 +      apply (auto simp: r_def, fastforce)
  1.1393        using \<open>S \<subseteq> S'\<close> \<open>T \<subseteq> T'\<close> \<open>W0 \<union> S \<subseteq> W1\<close> \<open>W1 = S' \<inter> O1\<close>  by auto
  1.1394      have "\<exists>r. continuous_on (W1 - (W - U0) \<union> (W2 - (W - U0))) r \<and>
  1.1395                r ` (W1 - (W - U0) \<union> (W2 - (W - U0))) \<subseteq> S \<union> T \<and> 
  1.1396 @@ -3725,7 +3602,7 @@
  1.1397        done
  1.1398      then show "S \<union> T retract_of W1 - (W - U0) \<union> (W2 - (W - U0))"
  1.1399        using  \<open>W0 \<union> S \<subseteq> W1\<close> \<open>W0 \<union> T \<subseteq> W2\<close> ST opeUU0 U0
  1.1400 -      by (auto simp add: retract_of_def retraction_def)
  1.1401 +      by (auto simp: retract_of_def retraction_def)
  1.1402    qed
  1.1403  qed
  1.1404  
  1.1405 @@ -4059,15 +3936,15 @@
  1.1406      by (auto simp: closest_point_self)
  1.1407    have "rel_frontier S retract_of affine hull S - {a}"
  1.1408      by (simp add: assms a rel_frontier_retract_of_punctured_affine_hull)
  1.1409 -  also have "... retract_of {x. closest_point (affine hull S) x \<noteq> a}"
  1.1410 +  also have "\<dots> retract_of {x. closest_point (affine hull S) x \<noteq> a}"
  1.1411      apply (simp add: retract_of_def retraction_def ahS)
  1.1412      apply (rule_tac x="closest_point (affine hull S)" in exI)
  1.1413 -    apply (auto simp add: False closest_point_self affine_imp_convex closest_point_in_set continuous_on_closest_point)
  1.1414 +    apply (auto simp: False closest_point_self affine_imp_convex closest_point_in_set continuous_on_closest_point)
  1.1415      done
  1.1416    finally have "rel_frontier S retract_of {x. closest_point (affine hull S) x \<noteq> a}" .
  1.1417    moreover have "openin (subtopology euclidean UNIV) (UNIV \<inter> closest_point (affine hull S) -` (- {a}))"
  1.1418      apply (rule continuous_openin_preimage_gen)
  1.1419 -    apply (auto simp add: False affine_imp_convex continuous_on_closest_point)
  1.1420 +    apply (auto simp: False affine_imp_convex continuous_on_closest_point)
  1.1421      done
  1.1422    ultimately show ?thesis
  1.1423      unfolding ENR_def
  1.1424 @@ -4116,7 +3993,7 @@
  1.1425        apply (rule continuous_on_cases_local [OF clS clT])
  1.1426        using r by (auto simp: continuous_on_id)
  1.1427    qed (use r in auto)
  1.1428 -  also have "... retract_of U"
  1.1429 +  also have "\<dots> retract_of U"
  1.1430      by (rule Un)
  1.1431    finally show ?thesis .
  1.1432  qed
  1.1433 @@ -4499,7 +4376,7 @@
  1.1434               and him: "h ` ({0..1} \<times> S) \<subseteq> U"
  1.1435               and [simp]: "\<And>x. h(0, x) = f x" "\<And>x. h(1::real, x) = g x"
  1.1436         using assms by (auto simp: homotopic_with_def)
  1.1437 -  define h' where "h' \<equiv>  \<lambda>z. if snd z \<in> S then h z else (f o snd) z"
  1.1438 +  define h' where "h' \<equiv>  \<lambda>z. if snd z \<in> S then h z else (f \<circ> snd) z"
  1.1439    define B where "B \<equiv> {0::real} \<times> T \<union> {0..1} \<times> S"
  1.1440    have clo0T: "closedin (subtopology euclidean ({0..1} \<times> T)) ({0::real} \<times> T)"
  1.1441      by (simp add: closedin_subtopology_refl closedin_Times)
  1.1442 @@ -4542,7 +4419,7 @@
  1.1443                        "retraction V B r" for V r
  1.1444        using that
  1.1445        apply (clarsimp simp add: retraction_def)
  1.1446 -      apply (rule Vk [of V "h' o r"], assumption+)
  1.1447 +      apply (rule Vk [of V "h' \<circ> r"], assumption+)
  1.1448          apply (metis continuous_on_compose conth' continuous_on_subset) 
  1.1449        using \<open>h' ` B \<subseteq> U\<close> apply force+
  1.1450        done
  1.1451 @@ -4629,7 +4506,7 @@
  1.1452  proof
  1.1453    assume ?lhs
  1.1454    then obtain c where c: "homotopic_with (\<lambda>x. True) S T (\<lambda>x. c) f"
  1.1455 -    by (blast intro: homotopic_with_symD elim: )
  1.1456 +    by (blast intro: homotopic_with_symD)
  1.1457    have "closedin (subtopology euclidean UNIV) S"
  1.1458      using \<open>closed S\<close> closed_closedin by fastforce
  1.1459    then obtain g where "continuous_on UNIV g" "range g \<subseteq> T"
  1.1460 @@ -4645,10 +4522,10 @@
  1.1461    then obtain c where "homotopic_with (\<lambda>h. True) UNIV T g (\<lambda>x. c)"
  1.1462      using nullhomotopic_from_contractible [of UNIV g T] contractible_UNIV by blast
  1.1463    then show ?lhs
  1.1464 -    apply (rule_tac x="c" in exI)
  1.1465 +    apply (rule_tac x=c in exI)
  1.1466      apply (rule homotopic_with_eq [of _ _ _ g "\<lambda>x. c"])
  1.1467      apply (rule homotopic_with_subset_left)
  1.1468 -    apply (auto simp add: \<open>\<And>x. x \<in> S \<Longrightarrow> g x = f x\<close>)
  1.1469 +    apply (auto simp: \<open>\<And>x. x \<in> S \<Longrightarrow> g x = f x\<close>)
  1.1470      done
  1.1471  qed
  1.1472  
  1.1473 @@ -4672,7 +4549,7 @@
  1.1474             (is "?lhs = ?rhs")
  1.1475  proof (cases "r = 0")
  1.1476    case True with fim show ?thesis
  1.1477 -    apply (auto simp: )
  1.1478 +    apply auto
  1.1479      using fim continuous_on_const apply fastforce
  1.1480      by (metis contf contractible_sing nullhomotopic_into_contractible)
  1.1481  next
  1.1482 @@ -4717,11 +4594,11 @@
  1.1483      obtain g where "range g \<subseteq> sphere 0 1" "continuous_on UNIV g"
  1.1484                          "\<And>x. x \<in> S \<Longrightarrow> g x = (x - a) /\<^sub>R norm (x - a)"
  1.1485        using notr
  1.1486 -      by (auto simp add: nullhomotopic_into_sphere_extension
  1.1487 +      by (auto simp: nullhomotopic_into_sphere_extension
  1.1488                   [OF \<open>closed S\<close> continuous_on_Borsuk_map [OF \<open>a \<notin> S\<close>] False s01])
  1.1489      with \<open>a \<notin> S\<close> show  "~ ?lhs"
  1.1490        apply (clarsimp simp: Borsuk_map_into_sphere [of a S, symmetric] dest!: nog)
  1.1491 -      apply (drule_tac x="g" in spec)
  1.1492 +      apply (drule_tac x=g in spec)
  1.1493        using continuous_on_subset by fastforce 
  1.1494    next
  1.1495      assume "~ ?lhs"
  1.1496 @@ -5070,7 +4947,7 @@
  1.1497          then obtain k where "y \<in> V k" and j: "\<forall>j<k. y \<notin> V j"
  1.1498            by (metis image_iff V wop)
  1.1499          with him t show "\<zeta>(t, y) \<in> T"
  1.1500 -          by (subst eq) (force simp:)+
  1.1501 +          by (subst eq) force+
  1.1502        qed
  1.1503        fix X y
  1.1504        assume "X \<in> \<V>" "y \<in> X"