author paulson Sun Apr 22 21:05:14 2018 +0100 (16 months ago) changeset 68022 c8a506be83bd parent 68021 b91a043c0dcb child 68023 75130777ece4
Tidied a lot of messy proofs
```     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.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.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.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.274 -      apply (rule Basis_le_norm[OF i(2)])+
1.275 -      done
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.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.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.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.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.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.1179 -          done
1.1180 +        have "a + dd (x - a) *\<^sub>R (x - a) \<in> T"
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.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"
```