src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 62061 bd2ccef8209b
child 62381 a6479cb85944
child 62390 842917225d56
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
     1 (*  Author:     John Harrison
     2     Author:     Robert Himmelmann, TU Muenchen (Translation from HOL light)
     3 *)
     4 
     5 (* ========================================================================= *)
     6 (* Results connected with topological dimension.                             *)
     7 (*                                                                           *)
     8 (* At the moment this is just Brouwer's fixpoint theorem. The proof is from  *)
     9 (* Kuhn: "some combinatorial lemmas in topology", IBM J. v4. (1960) p. 518   *)
    10 (* See "http://www.research.ibm.com/journal/rd/045/ibmrd0405K.pdf".          *)
    11 (*                                                                           *)
    12 (* The script below is quite messy, but at least we avoid formalizing any    *)
    13 (* topological machinery; we don't even use barycentric subdivision; this is *)
    14 (* the big advantage of Kuhn's proof over the usual Sperner's lemma one.     *)
    15 (*                                                                           *)
    16 (*              (c) Copyright, John Harrison 1998-2008                       *)
    17 (* ========================================================================= *)
    18 
    19 section \<open>Results connected with topological dimension.\<close>
    20 
    21 theory Brouwer_Fixpoint
    22 imports Convex_Euclidean_Space
    23 begin
    24 
    25 lemma bij_betw_singleton_eq:
    26   assumes f: "bij_betw f A B" and g: "bij_betw g A B" and a: "a \<in> A"
    27   assumes eq: "(\<And>x. x \<in> A \<Longrightarrow> x \<noteq> a \<Longrightarrow> f x = g x)"
    28   shows "f a = g a"
    29 proof -
    30   have "f ` (A - {a}) = g ` (A - {a})"
    31     by (intro image_cong) (simp_all add: eq)
    32   then have "B - {f a} = B - {g a}"
    33     using f g a  by (auto simp: bij_betw_def inj_on_image_set_diff set_eq_iff Diff_subset)
    34   moreover have "f a \<in> B" "g a \<in> B"
    35     using f g a by (auto simp: bij_betw_def)
    36   ultimately show ?thesis
    37     by auto
    38 qed
    39 
    40 lemma swap_image:
    41   "Fun.swap i j f ` A = (if i \<in> A then (if j \<in> A then f ` A else f ` ((A - {i}) \<union> {j}))
    42                                   else (if j \<in> A then f ` ((A - {j}) \<union> {i}) else f ` A))"
    43   apply (auto simp: Fun.swap_def image_iff)
    44   apply metis
    45   apply (metis member_remove remove_def)
    46   apply (metis member_remove remove_def)
    47   done
    48 
    49 lemma swap_apply1: "Fun.swap x y f x = f y"
    50   by (simp add: Fun.swap_def)
    51 
    52 lemma swap_apply2: "Fun.swap x y f y = f x"
    53   by (simp add: Fun.swap_def)
    54 
    55 lemma lessThan_empty_iff: "{..< n::nat} = {} \<longleftrightarrow> n = 0"
    56   by auto
    57 
    58 lemma Zero_notin_Suc: "0 \<notin> Suc ` A"
    59   by auto
    60 
    61 lemma atMost_Suc_eq_insert_0: "{.. Suc n} = insert 0 (Suc ` {.. n})"
    62   apply auto
    63   apply (case_tac x)
    64   apply auto
    65   done
    66 
    67 lemma setsum_union_disjoint':
    68   assumes "finite A"
    69     and "finite B"
    70     and "A \<inter> B = {}"
    71     and "A \<union> B = C"
    72   shows "setsum g C = setsum g A + setsum g B"
    73   using setsum.union_disjoint[OF assms(1-3)] and assms(4) by auto
    74 
    75 lemma pointwise_minimal_pointwise_maximal:
    76   fixes s :: "(nat \<Rightarrow> nat) set"
    77   assumes "finite s"
    78     and "s \<noteq> {}"
    79     and "\<forall>x\<in>s. \<forall>y\<in>s. x \<le> y \<or> y \<le> x"
    80   shows "\<exists>a\<in>s. \<forall>x\<in>s. a \<le> x"
    81     and "\<exists>a\<in>s. \<forall>x\<in>s. x \<le> a"
    82   using assms
    83 proof (induct s rule: finite_ne_induct)
    84   case (insert b s)
    85   assume *: "\<forall>x\<in>insert b s. \<forall>y\<in>insert b s. x \<le> y \<or> y \<le> x"
    86   moreover then obtain u l where "l \<in> s" "\<forall>b\<in>s. l \<le> b" "u \<in> s" "\<forall>b\<in>s. b \<le> u"
    87     using insert by auto
    88   ultimately show "\<exists>a\<in>insert b s. \<forall>x\<in>insert b s. a \<le> x" "\<exists>a\<in>insert b s. \<forall>x\<in>insert b s. x \<le> a"
    89     using *[rule_format, of b u] *[rule_format, of b l] by (metis insert_iff order.trans)+
    90 qed auto
    91 
    92 lemma brouwer_compactness_lemma:
    93   fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    94   assumes "compact s"
    95     and "continuous_on s f"
    96     and "\<not> (\<exists>x\<in>s. f x = 0)"
    97   obtains d where "0 < d" and "\<forall>x\<in>s. d \<le> norm (f x)"
    98 proof (cases "s = {}")
    99   case True
   100   show thesis
   101     by (rule that [of 1]) (auto simp: True)
   102 next
   103   case False
   104   have "continuous_on s (norm \<circ> f)"
   105     by (rule continuous_intros continuous_on_norm assms(2))+
   106   with False obtain x where x: "x \<in> s" "\<forall>y\<in>s. (norm \<circ> f) x \<le> (norm \<circ> f) y"
   107     using continuous_attains_inf[OF assms(1), of "norm \<circ> f"]
   108     unfolding o_def
   109     by auto
   110   have "(norm \<circ> f) x > 0"
   111     using assms(3) and x(1)
   112     by auto
   113   then show ?thesis
   114     by (rule that) (insert x(2), auto simp: o_def)
   115 qed
   116 
   117 lemma kuhn_labelling_lemma:
   118   fixes P Q :: "'a::euclidean_space \<Rightarrow> bool"
   119   assumes "\<forall>x. P x \<longrightarrow> P (f x)"
   120     and "\<forall>x. P x \<longrightarrow> (\<forall>i\<in>Basis. Q i \<longrightarrow> 0 \<le> x\<bullet>i \<and> x\<bullet>i \<le> 1)"
   121   shows "\<exists>l. (\<forall>x.\<forall>i\<in>Basis. l x i \<le> (1::nat)) \<and>
   122              (\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (x\<bullet>i = 0) \<longrightarrow> (l x i = 0)) \<and>
   123              (\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (x\<bullet>i = 1) \<longrightarrow> (l x i = 1)) \<and>
   124              (\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (l x i = 0) \<longrightarrow> x\<bullet>i \<le> f x\<bullet>i) \<and>
   125              (\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (l x i = 1) \<longrightarrow> f x\<bullet>i \<le> x\<bullet>i)"
   126 proof -
   127   { fix x i
   128     let ?R = "\<lambda>y. (P x \<and> Q i \<and> x \<bullet> i = 0 \<longrightarrow> y = (0::nat)) \<and>
   129         (P x \<and> Q i \<and> x \<bullet> i = 1 \<longrightarrow> y = 1) \<and>
   130         (P x \<and> Q i \<and> y = 0 \<longrightarrow> x \<bullet> i \<le> f x \<bullet> i) \<and>
   131         (P x \<and> Q i \<and> y = 1 \<longrightarrow> f x \<bullet> i \<le> x \<bullet> i)"
   132     { assume "P x" "Q i" "i \<in> Basis" with assms have "0 \<le> f x \<bullet> i \<and> f x \<bullet> i \<le> 1" by auto }
   133     then have "i \<in> Basis \<Longrightarrow> ?R 0 \<or> ?R 1" by auto }
   134   then show ?thesis
   135     unfolding all_conj_distrib[symmetric] Ball_def (* FIXME: shouldn't this work by metis? *)
   136     by (subst choice_iff[symmetric])+ blast
   137 qed
   138 
   139 
   140 subsection \<open>The key "counting" observation, somewhat abstracted.\<close>
   141 
   142 lemma kuhn_counting_lemma:
   143   fixes bnd compo compo' face S F
   144   defines "nF s == card {f\<in>F. face f s \<and> compo' f}"
   145   assumes [simp, intro]: "finite F" \<comment> "faces" and [simp, intro]: "finite S" \<comment> "simplices"
   146     and "\<And>f. f \<in> F \<Longrightarrow> bnd f \<Longrightarrow> card {s\<in>S. face f s} = 1"
   147     and "\<And>f. f \<in> F \<Longrightarrow> \<not> bnd f \<Longrightarrow> card {s\<in>S. face f s} = 2"
   148     and "\<And>s. s \<in> S \<Longrightarrow> compo s \<Longrightarrow> nF s = 1"
   149     and "\<And>s. s \<in> S \<Longrightarrow> \<not> compo s \<Longrightarrow> nF s = 0 \<or> nF s = 2"
   150     and "odd (card {f\<in>F. compo' f \<and> bnd f})"
   151   shows "odd (card {s\<in>S. compo s})"
   152 proof -
   153   have "(\<Sum>s | s \<in> S \<and> \<not> compo s. nF s) + (\<Sum>s | s \<in> S \<and> compo s. nF s) = (\<Sum>s\<in>S. nF s)"
   154     by (subst setsum.union_disjoint[symmetric]) (auto intro!: setsum.cong)
   155   also have "\<dots> = (\<Sum>s\<in>S. card {f \<in> {f\<in>F. compo' f \<and> bnd f}. face f s}) +
   156                   (\<Sum>s\<in>S. card {f \<in> {f\<in>F. compo' f \<and> \<not> bnd f}. face f s})"
   157     unfolding setsum.distrib[symmetric]
   158     by (subst card_Un_disjoint[symmetric])
   159        (auto simp: nF_def intro!: setsum.cong arg_cong[where f=card])
   160   also have "\<dots> = 1 * card {f\<in>F. compo' f \<and> bnd f} + 2 * card {f\<in>F. compo' f \<and> \<not> bnd f}"
   161     using assms(4,5) by (fastforce intro!: arg_cong2[where f="op +"] setsum_multicount)
   162   finally have "odd ((\<Sum>s | s \<in> S \<and> \<not> compo s. nF s) + card {s\<in>S. compo s})"
   163     using assms(6,8) by simp
   164   moreover have "(\<Sum>s | s \<in> S \<and> \<not> compo s. nF s) =
   165     (\<Sum>s | s \<in> S \<and> \<not> compo s \<and> nF s = 0. nF s) + (\<Sum>s | s \<in> S \<and> \<not> compo s \<and> nF s = 2. nF s)"
   166     using assms(7) by (subst setsum.union_disjoint[symmetric]) (fastforce intro!: setsum.cong)+
   167   ultimately show ?thesis
   168     by auto
   169 qed
   170 
   171 subsection \<open>The odd/even result for faces of complete vertices, generalized.\<close>
   172 
   173 lemma kuhn_complete_lemma:
   174   assumes [simp]: "finite simplices"
   175     and face: "\<And>f s. face f s \<longleftrightarrow> (\<exists>a\<in>s. f = s - {a})"
   176     and card_s[simp]:  "\<And>s. s \<in> simplices \<Longrightarrow> card s = n + 2"
   177     and rl_bd: "\<And>s. s \<in> simplices \<Longrightarrow> rl ` s \<subseteq> {..Suc n}"
   178     and bnd: "\<And>f s. s \<in> simplices \<Longrightarrow> face f s \<Longrightarrow> bnd f \<Longrightarrow> card {s\<in>simplices. face f s} = 1"
   179     and nbnd: "\<And>f s. s \<in> simplices \<Longrightarrow> face f s \<Longrightarrow> \<not> bnd f \<Longrightarrow> card {s\<in>simplices. face f s} = 2"
   180     and odd_card: "odd (card {f. (\<exists>s\<in>simplices. face f s) \<and> rl ` f = {..n} \<and> bnd f})"
   181   shows "odd (card {s\<in>simplices. (rl ` s = {..Suc n})})"
   182 proof (rule kuhn_counting_lemma)
   183   have finite_s[simp]: "\<And>s. s \<in> simplices \<Longrightarrow> finite s"
   184     by (metis add_is_0 zero_neq_numeral card_infinite assms(3))
   185 
   186   let ?F = "{f. \<exists>s\<in>simplices. face f s}"
   187   have F_eq: "?F = (\<Union>s\<in>simplices. \<Union>a\<in>s. {s - {a}})"
   188     by (auto simp: face)
   189   show "finite ?F"
   190     using \<open>finite simplices\<close> unfolding F_eq by auto
   191 
   192   show "card {s \<in> simplices. face f s} = 1" if "f \<in> ?F" "bnd f" for f
   193     using bnd that by auto
   194 
   195   show "card {s \<in> simplices. face f s} = 2" if "f \<in> ?F" "\<not> bnd f" for f
   196     using nbnd that by auto
   197 
   198   show "odd (card {f \<in> {f. \<exists>s\<in>simplices. face f s}. rl ` f = {..n} \<and> bnd f})"
   199     using odd_card by simp
   200 
   201   fix s assume s[simp]: "s \<in> simplices"
   202   let ?S = "{f \<in> {f. \<exists>s\<in>simplices. face f s}. face f s \<and> rl ` f = {..n}}"
   203   have "?S = (\<lambda>a. s - {a}) ` {a\<in>s. rl ` (s - {a}) = {..n}}"
   204     using s by (fastforce simp: face)
   205   then have card_S: "card ?S = card {a\<in>s. rl ` (s - {a}) = {..n}}"
   206     by (auto intro!: card_image inj_onI)
   207 
   208   { assume rl: "rl ` s = {..Suc n}"
   209     then have inj_rl: "inj_on rl s"
   210       by (intro eq_card_imp_inj_on) auto
   211     moreover obtain a where "rl a = Suc n" "a \<in> s"
   212       by (metis atMost_iff image_iff le_Suc_eq rl)
   213     ultimately have n: "{..n} = rl ` (s - {a})"
   214       by (auto simp add: inj_on_image_set_diff Diff_subset rl)
   215     have "{a\<in>s. rl ` (s - {a}) = {..n}} = {a}"
   216       using inj_rl \<open>a \<in> s\<close> by (auto simp add: n inj_on_image_eq_iff[OF inj_rl] Diff_subset)
   217     then show "card ?S = 1"
   218       unfolding card_S by simp }
   219 
   220   { assume rl: "rl ` s \<noteq> {..Suc n}"
   221     show "card ?S = 0 \<or> card ?S = 2"
   222     proof cases
   223       assume *: "{..n} \<subseteq> rl ` s"
   224       with rl rl_bd[OF s] have rl_s: "rl ` s = {..n}"
   225         by (auto simp add: atMost_Suc subset_insert_iff split: split_if_asm)
   226       then have "\<not> inj_on rl s"
   227         by (intro pigeonhole) simp
   228       then obtain a b where ab: "a \<in> s" "b \<in> s" "rl a = rl b" "a \<noteq> b"
   229         by (auto simp: inj_on_def)
   230       then have eq: "rl ` (s - {a}) = rl ` s"
   231         by auto
   232       with ab have inj: "inj_on rl (s - {a})"
   233         by (intro eq_card_imp_inj_on) (auto simp add: rl_s card_Diff_singleton_if)
   234 
   235       { fix x assume "x \<in> s" "x \<notin> {a, b}"
   236         then have "rl ` s - {rl x} = rl ` ((s - {a}) - {x})"
   237           by (auto simp: eq Diff_subset inj_on_image_set_diff[OF inj])
   238         also have "\<dots> = rl ` (s - {x})"
   239           using ab \<open>x \<notin> {a, b}\<close> by auto
   240         also assume "\<dots> = rl ` s"
   241         finally have False
   242           using \<open>x\<in>s\<close> by auto }
   243       moreover
   244       { fix x assume "x \<in> {a, b}" with ab have "x \<in> s \<and> rl ` (s - {x}) = rl ` s"
   245           by (simp add: set_eq_iff image_iff Bex_def) metis }
   246       ultimately have "{a\<in>s. rl ` (s - {a}) = {..n}} = {a, b}"
   247         unfolding rl_s[symmetric] by fastforce
   248       with \<open>a \<noteq> b\<close> show "card ?S = 0 \<or> card ?S = 2"
   249         unfolding card_S by simp
   250     next
   251       assume "\<not> {..n} \<subseteq> rl ` s"
   252       then have "\<And>x. rl ` (s - {x}) \<noteq> {..n}"
   253         by auto
   254       then show "card ?S = 0 \<or> card ?S = 2"
   255         unfolding card_S by simp
   256     qed }
   257 qed fact
   258 
   259 locale kuhn_simplex =
   260   fixes p n and base upd and s :: "(nat \<Rightarrow> nat) set"
   261   assumes base: "base \<in> {..< n} \<rightarrow> {..< p}"
   262   assumes base_out: "\<And>i. n \<le> i \<Longrightarrow> base i = p"
   263   assumes upd: "bij_betw upd {..< n} {..< n}"
   264   assumes s_pre: "s = (\<lambda>i j. if j \<in> upd`{..< i} then Suc (base j) else base j) ` {.. n}"
   265 begin
   266 
   267 definition "enum i j = (if j \<in> upd`{..< i} then Suc (base j) else base j)"
   268 
   269 lemma s_eq: "s = enum ` {.. n}"
   270   unfolding s_pre enum_def[abs_def] ..
   271 
   272 lemma upd_space: "i < n \<Longrightarrow> upd i < n"
   273   using upd by (auto dest!: bij_betwE)
   274 
   275 lemma s_space: "s \<subseteq> {..< n} \<rightarrow> {.. p}"
   276 proof -
   277   { fix i assume "i \<le> n" then have "enum i \<in> {..< n} \<rightarrow> {.. p}"
   278     proof (induct i)
   279       case 0 then show ?case
   280         using base by (auto simp: Pi_iff less_imp_le enum_def)
   281     next
   282       case (Suc i) with base show ?case
   283         by (auto simp: Pi_iff Suc_le_eq less_imp_le enum_def intro: upd_space)
   284     qed }
   285   then show ?thesis
   286     by (auto simp: s_eq)
   287 qed
   288 
   289 lemma inj_upd: "inj_on upd {..< n}"
   290   using upd by (simp add: bij_betw_def)
   291 
   292 lemma inj_enum: "inj_on enum {.. n}"
   293 proof -
   294   { fix x y :: nat assume "x \<noteq> y" "x \<le> n" "y \<le> n"
   295     with upd have "upd ` {..< x} \<noteq> upd ` {..< y}"
   296       by (subst inj_on_image_eq_iff[where C="{..< n}"]) (auto simp: bij_betw_def)
   297     then have "enum x \<noteq> enum y"
   298       by (auto simp add: enum_def fun_eq_iff) }
   299   then show ?thesis
   300     by (auto simp: inj_on_def)
   301 qed
   302 
   303 lemma enum_0: "enum 0 = base"
   304   by (simp add: enum_def[abs_def])
   305 
   306 lemma base_in_s: "base \<in> s"
   307   unfolding s_eq by (subst enum_0[symmetric]) auto
   308 
   309 lemma enum_in: "i \<le> n \<Longrightarrow> enum i \<in> s"
   310   unfolding s_eq by auto
   311 
   312 lemma one_step:
   313   assumes a: "a \<in> s" "j < n"
   314   assumes *: "\<And>a'. a' \<in> s \<Longrightarrow> a' \<noteq> a \<Longrightarrow> a' j = p'"
   315   shows "a j \<noteq> p'"
   316 proof
   317   assume "a j = p'"
   318   with * a have "\<And>a'. a' \<in> s \<Longrightarrow> a' j = p'"
   319     by auto
   320   then have "\<And>i. i \<le> n \<Longrightarrow> enum i j = p'"
   321     unfolding s_eq by auto
   322   from this[of 0] this[of n] have "j \<notin> upd ` {..< n}"
   323     by (auto simp: enum_def fun_eq_iff split: split_if_asm)
   324   with upd \<open>j < n\<close> show False
   325     by (auto simp: bij_betw_def)
   326 qed
   327 
   328 lemma upd_inj: "i < n \<Longrightarrow> j < n \<Longrightarrow> upd i = upd j \<longleftrightarrow> i = j"
   329   using upd by (auto simp: bij_betw_def inj_on_eq_iff)
   330 
   331 lemma upd_surj: "upd ` {..< n} = {..< n}"
   332   using upd by (auto simp: bij_betw_def)
   333 
   334 lemma in_upd_image: "A \<subseteq> {..< n} \<Longrightarrow> i < n \<Longrightarrow> upd i \<in> upd ` A \<longleftrightarrow> i \<in> A"
   335   using inj_on_image_mem_iff[of upd "{..< n}"] upd
   336   by (auto simp: bij_betw_def)
   337 
   338 lemma enum_inj: "i \<le> n \<Longrightarrow> j \<le> n \<Longrightarrow> enum i = enum j \<longleftrightarrow> i = j"
   339   using inj_enum by (auto simp: inj_on_eq_iff)
   340 
   341 lemma in_enum_image: "A \<subseteq> {.. n} \<Longrightarrow> i \<le> n \<Longrightarrow> enum i \<in> enum ` A \<longleftrightarrow> i \<in> A"
   342   using inj_on_image_mem_iff[OF inj_enum] by auto
   343 
   344 lemma enum_mono: "i \<le> n \<Longrightarrow> j \<le> n \<Longrightarrow> enum i \<le> enum j \<longleftrightarrow> i \<le> j"
   345   by (auto simp: enum_def le_fun_def in_upd_image Ball_def[symmetric])
   346 
   347 lemma enum_strict_mono: "i \<le> n \<Longrightarrow> j \<le> n \<Longrightarrow> enum i < enum j \<longleftrightarrow> i < j"
   348   using enum_mono[of i j] enum_inj[of i j] by (auto simp add: le_less)
   349 
   350 lemma chain: "a \<in> s \<Longrightarrow> b \<in> s \<Longrightarrow> a \<le> b \<or> b \<le> a"
   351   by (auto simp: s_eq enum_mono)
   352 
   353 lemma less: "a \<in> s \<Longrightarrow> b \<in> s \<Longrightarrow> a i < b i \<Longrightarrow> a < b"
   354   using chain[of a b] by (auto simp: less_fun_def le_fun_def not_le[symmetric])
   355 
   356 lemma enum_0_bot: "a \<in> s \<Longrightarrow> a = enum 0 \<longleftrightarrow> (\<forall>a'\<in>s. a \<le> a')"
   357   unfolding s_eq by (auto simp: enum_mono Ball_def)
   358 
   359 lemma enum_n_top: "a \<in> s \<Longrightarrow> a = enum n \<longleftrightarrow> (\<forall>a'\<in>s. a' \<le> a)"
   360   unfolding s_eq by (auto simp: enum_mono Ball_def)
   361 
   362 lemma enum_Suc: "i < n \<Longrightarrow> enum (Suc i) = (enum i)(upd i := Suc (enum i (upd i)))"
   363   by (auto simp: fun_eq_iff enum_def upd_inj)
   364 
   365 lemma enum_eq_p: "i \<le> n \<Longrightarrow> n \<le> j \<Longrightarrow> enum i j = p"
   366   by (induct i) (auto simp: enum_Suc enum_0 base_out upd_space not_less[symmetric])
   367 
   368 lemma out_eq_p: "a \<in> s \<Longrightarrow> n \<le> j \<Longrightarrow> a j = p"
   369   unfolding s_eq by (auto simp add: enum_eq_p)
   370 
   371 lemma s_le_p: "a \<in> s \<Longrightarrow> a j \<le> p"
   372   using out_eq_p[of a j] s_space by (cases "j < n") auto
   373 
   374 lemma le_Suc_base: "a \<in> s \<Longrightarrow> a j \<le> Suc (base j)"
   375   unfolding s_eq by (auto simp: enum_def)
   376 
   377 lemma base_le: "a \<in> s \<Longrightarrow> base j \<le> a j"
   378   unfolding s_eq by (auto simp: enum_def)
   379 
   380 lemma enum_le_p: "i \<le> n \<Longrightarrow> j < n \<Longrightarrow> enum i j \<le> p"
   381   using enum_in[of i] s_space by auto
   382 
   383 lemma enum_less: "a \<in> s \<Longrightarrow> i < n \<Longrightarrow> enum i < a \<longleftrightarrow> enum (Suc i) \<le> a"
   384   unfolding s_eq by (auto simp: enum_strict_mono enum_mono)
   385 
   386 lemma ksimplex_0:
   387   "n = 0 \<Longrightarrow> s = {(\<lambda>x. p)}"
   388   using s_eq enum_def base_out by auto
   389 
   390 lemma replace_0:
   391   assumes "j < n" "a \<in> s" and p: "\<forall>x\<in>s - {a}. x j = 0" and "x \<in> s"
   392   shows "x \<le> a"
   393 proof cases
   394   assume "x \<noteq> a"
   395   have "a j \<noteq> 0"
   396     using assms by (intro one_step[where a=a]) auto
   397   with less[OF \<open>x\<in>s\<close> \<open>a\<in>s\<close>, of j] p[rule_format, of x] \<open>x \<in> s\<close> \<open>x \<noteq> a\<close>
   398   show ?thesis
   399     by auto
   400 qed simp
   401 
   402 lemma replace_1:
   403   assumes "j < n" "a \<in> s" and p: "\<forall>x\<in>s - {a}. x j = p" and "x \<in> s"
   404   shows "a \<le> x"
   405 proof cases
   406   assume "x \<noteq> a"
   407   have "a j \<noteq> p"
   408     using assms by (intro one_step[where a=a]) auto
   409   with enum_le_p[of _ j] \<open>j < n\<close> \<open>a\<in>s\<close>
   410   have "a j < p"
   411     by (auto simp: less_le s_eq)
   412   with less[OF \<open>a\<in>s\<close> \<open>x\<in>s\<close>, of j] p[rule_format, of x] \<open>x \<in> s\<close> \<open>x \<noteq> a\<close>
   413   show ?thesis
   414     by auto
   415 qed simp
   416 
   417 end
   418 
   419 locale kuhn_simplex_pair = s: kuhn_simplex p n b_s u_s s + t: kuhn_simplex p n b_t u_t t
   420   for p n b_s u_s s b_t u_t t
   421 begin
   422 
   423 lemma enum_eq:
   424   assumes l: "i \<le> l" "l \<le> j" and "j + d \<le> n"
   425   assumes eq: "s.enum ` {i .. j} = t.enum ` {i + d .. j + d}"
   426   shows "s.enum l = t.enum (l + d)"
   427 using l proof (induct l rule: dec_induct)
   428   case base
   429   then have s: "s.enum i \<in> t.enum ` {i + d .. j + d}" and t: "t.enum (i + d) \<in> s.enum ` {i .. j}"
   430     using eq by auto
   431   from t \<open>i \<le> j\<close> \<open>j + d \<le> n\<close> have "s.enum i \<le> t.enum (i + d)"
   432     by (auto simp: s.enum_mono)
   433   moreover from s \<open>i \<le> j\<close> \<open>j + d \<le> n\<close> have "t.enum (i + d) \<le> s.enum i"
   434     by (auto simp: t.enum_mono)
   435   ultimately show ?case
   436     by auto
   437 next
   438   case (step l)
   439   moreover from step.prems \<open>j + d \<le> n\<close> have
   440       "s.enum l < s.enum (Suc l)"
   441       "t.enum (l + d) < t.enum (Suc l + d)"
   442     by (simp_all add: s.enum_strict_mono t.enum_strict_mono)
   443   moreover have
   444       "s.enum (Suc l) \<in> t.enum ` {i + d .. j + d}"
   445       "t.enum (Suc l + d) \<in> s.enum ` {i .. j}"
   446     using step \<open>j + d \<le> n\<close> eq by (auto simp: s.enum_inj t.enum_inj)
   447   ultimately have "s.enum (Suc l) = t.enum (Suc (l + d))"
   448     using \<open>j + d \<le> n\<close>
   449     by (intro antisym s.enum_less[THEN iffD1] t.enum_less[THEN iffD1])
   450        (auto intro!: s.enum_in t.enum_in)
   451   then show ?case by simp
   452 qed
   453 
   454 lemma ksimplex_eq_bot:
   455   assumes a: "a \<in> s" "\<And>a'. a' \<in> s \<Longrightarrow> a \<le> a'"
   456   assumes b: "b \<in> t" "\<And>b'. b' \<in> t \<Longrightarrow> b \<le> b'"
   457   assumes eq: "s - {a} = t - {b}"
   458   shows "s = t"
   459 proof cases
   460   assume "n = 0" with s.ksimplex_0 t.ksimplex_0 show ?thesis by simp
   461 next
   462   assume "n \<noteq> 0"
   463   have "s.enum 0 = (s.enum (Suc 0)) (u_s 0 := s.enum (Suc 0) (u_s 0) - 1)"
   464        "t.enum 0 = (t.enum (Suc 0)) (u_t 0 := t.enum (Suc 0) (u_t 0) - 1)"
   465     using \<open>n \<noteq> 0\<close> by (simp_all add: s.enum_Suc t.enum_Suc)
   466   moreover have e0: "a = s.enum 0" "b = t.enum 0"
   467     using a b by (simp_all add: s.enum_0_bot t.enum_0_bot)
   468   moreover
   469   { fix j assume "0 < j" "j \<le> n"
   470     moreover have "s - {a} = s.enum ` {Suc 0 .. n}" "t - {b} = t.enum ` {Suc 0 .. n}"
   471       unfolding s.s_eq t.s_eq e0 by (auto simp: s.enum_inj t.enum_inj)
   472     ultimately have "s.enum j = t.enum j"
   473       using enum_eq[of "1" j n 0] eq by auto }
   474   note enum_eq = this
   475   then have "s.enum (Suc 0) = t.enum (Suc 0)"
   476     using \<open>n \<noteq> 0\<close> by auto
   477   moreover
   478   { fix j assume "Suc j < n"
   479     with enum_eq[of "Suc j"] enum_eq[of "Suc (Suc j)"]
   480     have "u_s (Suc j) = u_t (Suc j)"
   481       using s.enum_Suc[of "Suc j"] t.enum_Suc[of "Suc j"]
   482       by (auto simp: fun_eq_iff split: split_if_asm) }
   483   then have "\<And>j. 0 < j \<Longrightarrow> j < n \<Longrightarrow> u_s j = u_t j"
   484     by (auto simp: gr0_conv_Suc)
   485   with \<open>n \<noteq> 0\<close> have "u_t 0 = u_s 0"
   486     by (intro bij_betw_singleton_eq[OF t.upd s.upd, of 0]) auto
   487   ultimately have "a = b"
   488     by simp
   489   with assms show "s = t"
   490     by auto
   491 qed
   492 
   493 lemma ksimplex_eq_top:
   494   assumes a: "a \<in> s" "\<And>a'. a' \<in> s \<Longrightarrow> a' \<le> a"
   495   assumes b: "b \<in> t" "\<And>b'. b' \<in> t \<Longrightarrow> b' \<le> b"
   496   assumes eq: "s - {a} = t - {b}"
   497   shows "s = t"
   498 proof (cases n)
   499   assume "n = 0" with s.ksimplex_0 t.ksimplex_0 show ?thesis by simp
   500 next
   501   case (Suc n')
   502   have "s.enum n = (s.enum n') (u_s n' := Suc (s.enum n' (u_s n')))"
   503        "t.enum n = (t.enum n') (u_t n' := Suc (t.enum n' (u_t n')))"
   504     using Suc by (simp_all add: s.enum_Suc t.enum_Suc)
   505   moreover have en: "a = s.enum n" "b = t.enum n"
   506     using a b by (simp_all add: s.enum_n_top t.enum_n_top)
   507   moreover
   508   { fix j assume "j < n"
   509     moreover have "s - {a} = s.enum ` {0 .. n'}" "t - {b} = t.enum ` {0 .. n'}"
   510       unfolding s.s_eq t.s_eq en by (auto simp: s.enum_inj t.enum_inj Suc)
   511     ultimately have "s.enum j = t.enum j"
   512       using enum_eq[of "0" j n' 0] eq Suc by auto }
   513   note enum_eq = this
   514   then have "s.enum n' = t.enum n'"
   515     using Suc by auto
   516   moreover
   517   { fix j assume "j < n'"
   518     with enum_eq[of j] enum_eq[of "Suc j"]
   519     have "u_s j = u_t j"
   520       using s.enum_Suc[of j] t.enum_Suc[of j]
   521       by (auto simp: Suc fun_eq_iff split: split_if_asm) }
   522   then have "\<And>j. j < n' \<Longrightarrow> u_s j = u_t j"
   523     by (auto simp: gr0_conv_Suc)
   524   then have "u_t n' = u_s n'"
   525     by (intro bij_betw_singleton_eq[OF t.upd s.upd, of n']) (auto simp: Suc)
   526   ultimately have "a = b"
   527     by simp
   528   with assms show "s = t"
   529     by auto
   530 qed
   531 
   532 end
   533 
   534 inductive ksimplex for p n :: nat where
   535   ksimplex: "kuhn_simplex p n base upd s \<Longrightarrow> ksimplex p n s"
   536 
   537 lemma finite_ksimplexes: "finite {s. ksimplex p n s}"
   538 proof (rule finite_subset)
   539   { fix a s assume "ksimplex p n s" "a \<in> s"
   540     then obtain b u where "kuhn_simplex p n b u s" by (auto elim: ksimplex.cases)
   541     then interpret kuhn_simplex p n b u s .
   542     from s_space \<open>a \<in> s\<close> out_eq_p[OF \<open>a \<in> s\<close>]
   543     have "a \<in> (\<lambda>f x. if n \<le> x then p else f x) ` ({..< n} \<rightarrow>\<^sub>E {.. p})"
   544       by (auto simp: image_iff subset_eq Pi_iff split: split_if_asm
   545                intro!: bexI[of _ "restrict a {..< n}"]) }
   546   then show "{s. ksimplex p n s} \<subseteq> Pow ((\<lambda>f x. if n \<le> x then p else f x) ` ({..< n} \<rightarrow>\<^sub>E {.. p}))"
   547     by auto
   548 qed (simp add: finite_PiE)
   549 
   550 lemma ksimplex_card:
   551   assumes "ksimplex p n s" shows "card s = Suc n"
   552 using assms proof cases
   553   case (ksimplex u b)
   554   then interpret kuhn_simplex p n u b s .
   555   show ?thesis
   556     by (simp add: card_image s_eq inj_enum)
   557 qed
   558 
   559 lemma simplex_top_face:
   560   assumes "0 < p" "\<forall>x\<in>s'. x n = p"
   561   shows "ksimplex p n s' \<longleftrightarrow> (\<exists>s a. ksimplex p (Suc n) s \<and> a \<in> s \<and> s' = s - {a})"
   562   using assms
   563 proof safe
   564   fix s a assume "ksimplex p (Suc n) s" and a: "a \<in> s" and na: "\<forall>x\<in>s - {a}. x n = p"
   565   then show "ksimplex p n (s - {a})"
   566   proof cases
   567     case (ksimplex base upd)
   568     then interpret kuhn_simplex p "Suc n" base upd "s" .
   569 
   570     have "a n < p"
   571       using one_step[of a n p] na \<open>a\<in>s\<close> s_space by (auto simp: less_le)
   572     then have "a = enum 0"
   573       using \<open>a \<in> s\<close> na by (subst enum_0_bot) (auto simp: le_less intro!: less[of a _ n])
   574     then have s_eq: "s - {a} = enum ` Suc ` {.. n}"
   575       using s_eq by (simp add: atMost_Suc_eq_insert_0 insert_ident Zero_notin_Suc in_enum_image subset_eq)
   576     then have "enum 1 \<in> s - {a}"
   577       by auto
   578     then have "upd 0 = n"
   579       using \<open>a n < p\<close> \<open>a = enum 0\<close> na[rule_format, of "enum 1"]
   580       by (auto simp: fun_eq_iff enum_Suc split: split_if_asm)
   581     then have "bij_betw upd (Suc ` {..< n}) {..< n}"
   582       using upd
   583       by (subst notIn_Un_bij_betw3[where b=0])
   584          (auto simp: lessThan_Suc[symmetric] lessThan_Suc_eq_insert_0)
   585     then have "bij_betw (upd\<circ>Suc) {..<n} {..<n}"
   586       by (rule bij_betw_trans[rotated]) (auto simp: bij_betw_def)
   587 
   588     have "a n = p - 1"
   589       using enum_Suc[of 0] na[rule_format, OF \<open>enum 1 \<in> s - {a}\<close>] \<open>a = enum 0\<close> by (auto simp: \<open>upd 0 = n\<close>)
   590 
   591     show ?thesis
   592     proof (rule ksimplex.intros, standard)
   593       show "bij_betw (upd\<circ>Suc) {..< n} {..< n}" by fact
   594       show "base(n := p) \<in> {..<n} \<rightarrow> {..<p}" "\<And>i. n\<le>i \<Longrightarrow> (base(n := p)) i = p"
   595         using base base_out by (auto simp: Pi_iff)
   596 
   597       have "\<And>i. Suc ` {..< i} = {..< Suc i} - {0}"
   598         by (auto simp: image_iff Ball_def) arith
   599       then have upd_Suc: "\<And>i. i \<le> n \<Longrightarrow> (upd\<circ>Suc) ` {..< i} = upd ` {..< Suc i} - {n}"
   600         using \<open>upd 0 = n\<close> upd_inj
   601         by (auto simp add: image_comp[symmetric] inj_on_image_set_diff[OF inj_upd])
   602       have n_in_upd: "\<And>i. n \<in> upd ` {..< Suc i}"
   603         using \<open>upd 0 = n\<close> by auto
   604 
   605       def f' \<equiv> "\<lambda>i j. if j \<in> (upd\<circ>Suc)`{..< i} then Suc ((base(n := p)) j) else (base(n := p)) j"
   606       { fix x i assume i[arith]: "i \<le> n" then have "enum (Suc i) x = f' i x"
   607           unfolding f'_def enum_def using \<open>a n < p\<close> \<open>a = enum 0\<close> \<open>upd 0 = n\<close> \<open>a n = p - 1\<close>
   608           by (simp add: upd_Suc enum_0 n_in_upd) }
   609       then show "s - {a} = f' ` {.. n}"
   610         unfolding s_eq image_comp by (intro image_cong) auto
   611     qed
   612   qed
   613 next
   614   assume "ksimplex p n s'" and *: "\<forall>x\<in>s'. x n = p"
   615   then show "\<exists>s a. ksimplex p (Suc n) s \<and> a \<in> s \<and> s' = s - {a}"
   616   proof cases
   617     case (ksimplex base upd)
   618     then interpret kuhn_simplex p n base upd s' .
   619     def b \<equiv> "base (n := p - 1)"
   620     def u \<equiv> "\<lambda>i. case i of 0 \<Rightarrow> n | Suc i \<Rightarrow> upd i"
   621 
   622     have "ksimplex p (Suc n) (s' \<union> {b})"
   623     proof (rule ksimplex.intros, standard)
   624       show "b \<in> {..<Suc n} \<rightarrow> {..<p}"
   625         using base \<open>0 < p\<close> unfolding lessThan_Suc b_def by (auto simp: PiE_iff)
   626       show "\<And>i. Suc n \<le> i \<Longrightarrow> b i = p"
   627         using base_out by (auto simp: b_def)
   628 
   629       have "bij_betw u (Suc ` {..< n} \<union> {0}) ({..<n} \<union> {u 0})"
   630         using upd
   631         by (intro notIn_Un_bij_betw) (auto simp: u_def bij_betw_def image_comp comp_def inj_on_def)
   632       then show "bij_betw u {..<Suc n} {..<Suc n}"
   633         by (simp add: u_def lessThan_Suc[symmetric] lessThan_Suc_eq_insert_0)
   634 
   635       def f' \<equiv> "\<lambda>i j. if j \<in> u`{..< i} then Suc (b j) else b j"
   636 
   637       have u_eq: "\<And>i. i \<le> n \<Longrightarrow> u ` {..< Suc i} = upd ` {..< i} \<union> { n }"
   638         by (auto simp: u_def image_iff upd_inj Ball_def split: nat.split) arith
   639 
   640       { fix x have "x \<le> n \<Longrightarrow> n \<notin> upd ` {..<x}"
   641           using upd_space by (simp add: image_iff neq_iff) }
   642       note n_not_upd = this
   643 
   644       have *: "f' ` {.. Suc n} = f' ` (Suc ` {.. n} \<union> {0})"
   645         unfolding atMost_Suc_eq_insert_0 by simp
   646       also have "\<dots> = (f' \<circ> Suc) ` {.. n} \<union> {b}"
   647         by (auto simp: f'_def)
   648       also have "(f' \<circ> Suc) ` {.. n} = s'"
   649         using \<open>0 < p\<close> base_out[of n]
   650         unfolding s_eq enum_def[abs_def] f'_def[abs_def] upd_space
   651         by (intro image_cong) (simp_all add: u_eq b_def fun_eq_iff n_not_upd)
   652       finally show "s' \<union> {b} = f' ` {.. Suc n}" ..
   653     qed
   654     moreover have "b \<notin> s'"
   655       using * \<open>0 < p\<close> by (auto simp: b_def)
   656     ultimately show ?thesis by auto
   657   qed
   658 qed
   659 
   660 lemma ksimplex_replace_0:
   661   assumes s: "ksimplex p n s" and a: "a \<in> s"
   662   assumes j: "j < n" and p: "\<forall>x\<in>s - {a}. x j = 0"
   663   shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 1"
   664   using s
   665 proof cases
   666   case (ksimplex b_s u_s)
   667 
   668   { fix t b assume "ksimplex p n t"
   669     then obtain b_t u_t where "kuhn_simplex p n b_t u_t t"
   670       by (auto elim: ksimplex.cases)
   671     interpret kuhn_simplex_pair p n b_s u_s s b_t u_t t
   672       by intro_locales fact+
   673 
   674     assume b: "b \<in> t" "t - {b} = s - {a}"
   675     with a j p s.replace_0[of _ a] t.replace_0[of _ b] have "s = t"
   676       by (intro ksimplex_eq_top[of a b]) auto }
   677   then have "{s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = {s}"
   678     using s \<open>a \<in> s\<close> by auto
   679   then show ?thesis
   680     by simp
   681 qed
   682 
   683 lemma ksimplex_replace_1:
   684   assumes s: "ksimplex p n s" and a: "a \<in> s"
   685   assumes j: "j < n" and p: "\<forall>x\<in>s - {a}. x j = p"
   686   shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 1"
   687   using s
   688 proof cases
   689   case (ksimplex b_s u_s)
   690 
   691   { fix t b assume "ksimplex p n t"
   692     then obtain b_t u_t where "kuhn_simplex p n b_t u_t t"
   693       by (auto elim: ksimplex.cases)
   694     interpret kuhn_simplex_pair p n b_s u_s s b_t u_t t
   695       by intro_locales fact+
   696 
   697     assume b: "b \<in> t" "t - {b} = s - {a}"
   698     with a j p s.replace_1[of _ a] t.replace_1[of _ b] have "s = t"
   699       by (intro ksimplex_eq_bot[of a b]) auto }
   700   then have "{s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = {s}"
   701     using s \<open>a \<in> s\<close> by auto
   702   then show ?thesis
   703     by simp
   704 qed
   705 
   706 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))"
   707   by (auto simp add: card_Suc_eq eval_nat_numeral)
   708 
   709 lemma ksimplex_replace_2:
   710   assumes s: "ksimplex p n s" and "a \<in> s" and "n \<noteq> 0"
   711     and lb: "\<forall>j<n. \<exists>x\<in>s - {a}. x j \<noteq> 0"
   712     and ub: "\<forall>j<n. \<exists>x\<in>s - {a}. x j \<noteq> p"
   713   shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 2"
   714   using s
   715 proof cases
   716   case (ksimplex base upd)
   717   then interpret kuhn_simplex p n base upd s .
   718 
   719   from \<open>a \<in> s\<close> obtain i where "i \<le> n" "a = enum i"
   720     unfolding s_eq by auto
   721 
   722   from \<open>i \<le> n\<close> have "i = 0 \<or> i = n \<or> (0 < i \<and> i < n)"
   723     by linarith
   724   then have "\<exists>!s'. s' \<noteq> s \<and> ksimplex p n s' \<and> (\<exists>b\<in>s'. s - {a} = s'- {b})"
   725   proof (elim disjE conjE)
   726     assume "i = 0"
   727     def rot \<equiv> "\<lambda>i. if i + 1 = n then 0 else i + 1"
   728     let ?upd = "upd \<circ> rot"
   729 
   730     have rot: "bij_betw rot {..< n} {..< n}"
   731       by (auto simp: bij_betw_def inj_on_def image_iff Ball_def rot_def)
   732          arith+
   733     from rot upd have "bij_betw ?upd {..<n} {..<n}"
   734       by (rule bij_betw_trans)
   735 
   736     def f' \<equiv> "\<lambda>i j. if j \<in> ?upd`{..< i} then Suc (enum (Suc 0) j) else enum (Suc 0) j"
   737 
   738     interpret b: kuhn_simplex p n "enum (Suc 0)" "upd \<circ> rot" "f' ` {.. n}"
   739     proof
   740       from \<open>a = enum i\<close> ub \<open>n \<noteq> 0\<close> \<open>i = 0\<close>
   741       obtain i' where "i' \<le> n" "enum i' \<noteq> enum 0" "enum i' (upd 0) \<noteq> p"
   742         unfolding s_eq by (auto intro: upd_space simp: enum_inj)
   743       then have "enum 1 \<le> enum i'" "enum i' (upd 0) < p"
   744         using enum_le_p[of i' "upd 0"] by (auto simp add: enum_inj enum_mono upd_space)
   745       then have "enum 1 (upd 0) < p"
   746         by (auto simp add: le_fun_def intro: le_less_trans)
   747       then show "enum (Suc 0) \<in> {..<n} \<rightarrow> {..<p}"
   748         using base \<open>n \<noteq> 0\<close> by (auto simp add: enum_0 enum_Suc PiE_iff extensional_def upd_space)
   749 
   750       { fix i assume "n \<le> i" then show "enum (Suc 0) i = p"
   751         using \<open>n \<noteq> 0\<close> by (auto simp: enum_eq_p) }
   752       show "bij_betw ?upd {..<n} {..<n}" by fact
   753     qed (simp add: f'_def)
   754     have ks_f': "ksimplex p n (f' ` {.. n})"
   755       by rule unfold_locales
   756 
   757     have b_enum: "b.enum = f'" unfolding f'_def b.enum_def[abs_def] ..
   758     with b.inj_enum have inj_f': "inj_on f' {.. n}" by simp
   759 
   760     have [simp]: "\<And>j. j < n \<Longrightarrow> rot ` {..< j} = {0 <..< Suc j}"
   761       by (auto simp: rot_def image_iff Ball_def)
   762          arith
   763 
   764     { fix j assume j: "j < n"
   765       from j \<open>n \<noteq> 0\<close> have "f' j = enum (Suc j)"
   766         by (auto simp add: f'_def enum_def upd_inj in_upd_image image_comp[symmetric] fun_eq_iff) }
   767     note f'_eq_enum = this
   768     then have "enum ` Suc ` {..< n} = f' ` {..< n}"
   769       by (force simp: enum_inj)
   770     also have "Suc ` {..< n} = {.. n} - {0}"
   771       by (auto simp: image_iff Ball_def) arith
   772     also have "{..< n} = {.. n} - {n}"
   773       by auto
   774     finally have eq: "s - {a} = f' ` {.. n} - {f' n}"
   775       unfolding s_eq \<open>a = enum i\<close> \<open>i = 0\<close>
   776       by (simp add: Diff_subset inj_on_image_set_diff[OF inj_enum] inj_on_image_set_diff[OF inj_f'])
   777 
   778     have "enum 0 < f' 0"
   779       using \<open>n \<noteq> 0\<close> by (simp add: enum_strict_mono f'_eq_enum)
   780     also have "\<dots> < f' n"
   781       using \<open>n \<noteq> 0\<close> b.enum_strict_mono[of 0 n] unfolding b_enum by simp
   782     finally have "a \<noteq> f' n"
   783       using \<open>a = enum i\<close> \<open>i = 0\<close> by auto
   784 
   785     { fix t c assume "ksimplex p n t" "c \<in> t" and eq_sma: "s - {a} = t - {c}"
   786       obtain b u where "kuhn_simplex p n b u t"
   787         using \<open>ksimplex p n t\<close> by (auto elim: ksimplex.cases)
   788       then interpret t: kuhn_simplex p n b u t .
   789 
   790       { fix x assume "x \<in> s" "x \<noteq> a"
   791          then have "x (upd 0) = enum (Suc 0) (upd 0)"
   792            by (auto simp: \<open>a = enum i\<close> \<open>i = 0\<close> s_eq enum_def enum_inj) }
   793       then have eq_upd0: "\<forall>x\<in>t-{c}. x (upd 0) = enum (Suc 0) (upd 0)"
   794         unfolding eq_sma[symmetric] by auto
   795       then have "c (upd 0) \<noteq> enum (Suc 0) (upd 0)"
   796         using \<open>n \<noteq> 0\<close> by (intro t.one_step[OF \<open>c\<in>t\<close> ]) (auto simp: upd_space)
   797       then have "c (upd 0) < enum (Suc 0) (upd 0) \<or> c (upd 0) > enum (Suc 0) (upd 0)"
   798         by auto
   799       then have "t = s \<or> t = f' ` {..n}"
   800       proof (elim disjE conjE)
   801         assume *: "c (upd 0) < enum (Suc 0) (upd 0)"
   802         interpret st: kuhn_simplex_pair p n base upd s b u t ..
   803         { fix x assume "x \<in> t" with * \<open>c\<in>t\<close> eq_upd0[rule_format, of x] have "c \<le> x"
   804             by (auto simp: le_less intro!: t.less[of _ _ "upd 0"]) }
   805         note top = this
   806         have "s = t"
   807           using \<open>a = enum i\<close> \<open>i = 0\<close> \<open>c \<in> t\<close>
   808           by (intro st.ksimplex_eq_bot[OF _ _ _ _ eq_sma])
   809              (auto simp: s_eq enum_mono t.s_eq t.enum_mono top)
   810         then show ?thesis by simp
   811       next
   812         assume *: "c (upd 0) > enum (Suc 0) (upd 0)"
   813         interpret st: kuhn_simplex_pair p n "enum (Suc 0)" "upd \<circ> rot" "f' ` {.. n}" b u t ..
   814         have eq: "f' ` {..n} - {f' n} = t - {c}"
   815           using eq_sma eq by simp
   816         { fix x assume "x \<in> t" with * \<open>c\<in>t\<close> eq_upd0[rule_format, of x] have "x \<le> c"
   817             by (auto simp: le_less intro!: t.less[of _ _ "upd 0"]) }
   818         note top = this
   819         have "f' ` {..n} = t"
   820           using \<open>a = enum i\<close> \<open>i = 0\<close> \<open>c \<in> t\<close>
   821           by (intro st.ksimplex_eq_top[OF _ _ _ _ eq])
   822              (auto simp: b.s_eq b.enum_mono t.s_eq t.enum_mono b_enum[symmetric] top)
   823         then show ?thesis by simp
   824       qed }
   825     with ks_f' eq \<open>a \<noteq> f' n\<close> \<open>n \<noteq> 0\<close> show ?thesis
   826       apply (intro ex1I[of _ "f' ` {.. n}"])
   827       apply auto []
   828       apply metis
   829       done
   830   next
   831     assume "i = n"
   832     from \<open>n \<noteq> 0\<close> obtain n' where n': "n = Suc n'"
   833       by (cases n) auto
   834 
   835     def rot \<equiv> "\<lambda>i. case i of 0 \<Rightarrow> n' | Suc i \<Rightarrow> i"
   836     let ?upd = "upd \<circ> rot"
   837 
   838     have rot: "bij_betw rot {..< n} {..< n}"
   839       by (auto simp: bij_betw_def inj_on_def image_iff Bex_def rot_def n' split: nat.splits)
   840          arith
   841     from rot upd have "bij_betw ?upd {..<n} {..<n}"
   842       by (rule bij_betw_trans)
   843 
   844     def b \<equiv> "base (upd n' := base (upd n') - 1)"
   845     def f' \<equiv> "\<lambda>i j. if j \<in> ?upd`{..< i} then Suc (b j) else b j"
   846 
   847     interpret b: kuhn_simplex p n b "upd \<circ> rot" "f' ` {.. n}"
   848     proof
   849       { fix i assume "n \<le> i" then show "b i = p"
   850           using base_out[of i] upd_space[of n'] by (auto simp: b_def n') }
   851       show "b \<in> {..<n} \<rightarrow> {..<p}"
   852         using base \<open>n \<noteq> 0\<close> upd_space[of n']
   853         by (auto simp: b_def PiE_def Pi_iff Ball_def upd_space extensional_def n')
   854 
   855       show "bij_betw ?upd {..<n} {..<n}" by fact
   856     qed (simp add: f'_def)
   857     have f': "b.enum = f'" unfolding f'_def b.enum_def[abs_def] ..
   858     have ks_f': "ksimplex p n (b.enum ` {.. n})"
   859       unfolding f' by rule unfold_locales
   860 
   861     have "0 < n"
   862       using \<open>n \<noteq> 0\<close> by auto
   863 
   864     { from \<open>a = enum i\<close> \<open>n \<noteq> 0\<close> \<open>i = n\<close> lb upd_space[of n']
   865       obtain i' where "i' \<le> n" "enum i' \<noteq> enum n" "0 < enum i' (upd n')"
   866         unfolding s_eq by (auto simp: enum_inj n')
   867       moreover have "enum i' (upd n') = base (upd n')"
   868         unfolding enum_def using \<open>i' \<le> n\<close> \<open>enum i' \<noteq> enum n\<close> by (auto simp: n' upd_inj enum_inj)
   869       ultimately have "0 < base (upd n')"
   870         by auto }
   871     then have benum1: "b.enum (Suc 0) = base"
   872       unfolding b.enum_Suc[OF \<open>0<n\<close>] b.enum_0 by (auto simp: b_def rot_def)
   873 
   874     have [simp]: "\<And>j. Suc j < n \<Longrightarrow> rot ` {..< Suc j} = {n'} \<union> {..< j}"
   875       by (auto simp: rot_def image_iff Ball_def split: nat.splits)
   876     have rot_simps: "\<And>j. rot (Suc j) = j" "rot 0 = n'"
   877       by (simp_all add: rot_def)
   878 
   879     { fix j assume j: "Suc j \<le> n" then have "b.enum (Suc j) = enum j"
   880         by (induct j) (auto simp add: benum1 enum_0 b.enum_Suc enum_Suc rot_simps) }
   881     note b_enum_eq_enum = this
   882     then have "enum ` {..< n} = b.enum ` Suc ` {..< n}"
   883       by (auto simp add: image_comp intro!: image_cong)
   884     also have "Suc ` {..< n} = {.. n} - {0}"
   885       by (auto simp: image_iff Ball_def) arith
   886     also have "{..< n} = {.. n} - {n}"
   887       by auto
   888     finally have eq: "s - {a} = b.enum ` {.. n} - {b.enum 0}"
   889       unfolding s_eq \<open>a = enum i\<close> \<open>i = n\<close>
   890       using inj_on_image_set_diff[OF inj_enum Diff_subset, of "{n}"]
   891             inj_on_image_set_diff[OF b.inj_enum Diff_subset, of "{0}"]
   892       by (simp add: comp_def )
   893 
   894     have "b.enum 0 \<le> b.enum n"
   895       by (simp add: b.enum_mono)
   896     also have "b.enum n < enum n"
   897       using \<open>n \<noteq> 0\<close> by (simp add: enum_strict_mono b_enum_eq_enum n')
   898     finally have "a \<noteq> b.enum 0"
   899       using \<open>a = enum i\<close> \<open>i = n\<close> by auto
   900 
   901     { fix t c assume "ksimplex p n t" "c \<in> t" and eq_sma: "s - {a} = t - {c}"
   902       obtain b' u where "kuhn_simplex p n b' u t"
   903         using \<open>ksimplex p n t\<close> by (auto elim: ksimplex.cases)
   904       then interpret t: kuhn_simplex p n b' u t .
   905 
   906       { fix x assume "x \<in> s" "x \<noteq> a"
   907          then have "x (upd n') = enum n' (upd n')"
   908            by (auto simp: \<open>a = enum i\<close> n' \<open>i = n\<close> s_eq enum_def enum_inj in_upd_image) }
   909       then have eq_upd0: "\<forall>x\<in>t-{c}. x (upd n') = enum n' (upd n')"
   910         unfolding eq_sma[symmetric] by auto
   911       then have "c (upd n') \<noteq> enum n' (upd n')"
   912         using \<open>n \<noteq> 0\<close> by (intro t.one_step[OF \<open>c\<in>t\<close> ]) (auto simp: n' upd_space[unfolded n'])
   913       then have "c (upd n') < enum n' (upd n') \<or> c (upd n') > enum n' (upd n')"
   914         by auto
   915       then have "t = s \<or> t = b.enum ` {..n}"
   916       proof (elim disjE conjE)
   917         assume *: "c (upd n') > enum n' (upd n')"
   918         interpret st: kuhn_simplex_pair p n base upd s b' u t ..
   919         { fix x assume "x \<in> t" with * \<open>c\<in>t\<close> eq_upd0[rule_format, of x] have "x \<le> c"
   920             by (auto simp: le_less intro!: t.less[of _ _ "upd n'"]) }
   921         note top = this
   922         have "s = t"
   923           using \<open>a = enum i\<close> \<open>i = n\<close> \<open>c \<in> t\<close>
   924           by (intro st.ksimplex_eq_top[OF _ _ _ _ eq_sma])
   925              (auto simp: s_eq enum_mono t.s_eq t.enum_mono top)
   926         then show ?thesis by simp
   927       next
   928         assume *: "c (upd n') < enum n' (upd n')"
   929         interpret st: kuhn_simplex_pair p n b "upd \<circ> rot" "f' ` {.. n}" b' u t ..
   930         have eq: "f' ` {..n} - {b.enum 0} = t - {c}"
   931           using eq_sma eq f' by simp
   932         { fix x assume "x \<in> t" with * \<open>c\<in>t\<close> eq_upd0[rule_format, of x] have "c \<le> x"
   933             by (auto simp: le_less intro!: t.less[of _ _ "upd n'"]) }
   934         note bot = this
   935         have "f' ` {..n} = t"
   936           using \<open>a = enum i\<close> \<open>i = n\<close> \<open>c \<in> t\<close>
   937           by (intro st.ksimplex_eq_bot[OF _ _ _ _ eq])
   938              (auto simp: b.s_eq b.enum_mono t.s_eq t.enum_mono bot)
   939         with f' show ?thesis by simp
   940       qed }
   941     with ks_f' eq \<open>a \<noteq> b.enum 0\<close> \<open>n \<noteq> 0\<close> show ?thesis
   942       apply (intro ex1I[of _ "b.enum ` {.. n}"])
   943       apply auto []
   944       apply metis
   945       done
   946   next
   947     assume i: "0 < i" "i < n"
   948     def i' \<equiv> "i - 1"
   949     with i have "Suc i' < n"
   950       by simp
   951     with i have Suc_i': "Suc i' = i"
   952       by (simp add: i'_def)
   953 
   954     let ?upd = "Fun.swap i' i upd"
   955     from i upd have "bij_betw ?upd {..< n} {..< n}"
   956       by (subst bij_betw_swap_iff) (auto simp: i'_def)
   957 
   958     def f' \<equiv> "\<lambda>i j. if j \<in> ?upd`{..< i} then Suc (base j) else base j"
   959     interpret b: kuhn_simplex p n base ?upd "f' ` {.. n}"
   960     proof
   961       show "base \<in> {..<n} \<rightarrow> {..<p}" by fact
   962       { fix i assume "n \<le> i" then show "base i = p" by fact }
   963       show "bij_betw ?upd {..<n} {..<n}" by fact
   964     qed (simp add: f'_def)
   965     have f': "b.enum = f'" unfolding f'_def b.enum_def[abs_def] ..
   966     have ks_f': "ksimplex p n (b.enum ` {.. n})"
   967       unfolding f' by rule unfold_locales
   968 
   969     have "{i} \<subseteq> {..n}"
   970       using i by auto
   971     { fix j assume "j \<le> n"
   972       moreover have "j < i \<or> i = j \<or> i < j" by arith
   973       moreover note i
   974       ultimately have "enum j = b.enum j \<longleftrightarrow> j \<noteq> i"
   975         unfolding enum_def[abs_def] b.enum_def[abs_def]
   976         by (auto simp add: fun_eq_iff swap_image i'_def
   977                            in_upd_image inj_on_image_set_diff[OF inj_upd]) }
   978     note enum_eq_benum = this
   979     then have "enum ` ({.. n} - {i}) = b.enum ` ({.. n} - {i})"
   980       by (intro image_cong) auto
   981     then have eq: "s - {a} = b.enum ` {.. n} - {b.enum i}"
   982       unfolding s_eq \<open>a = enum i\<close>
   983       using inj_on_image_set_diff[OF inj_enum Diff_subset \<open>{i} \<subseteq> {..n}\<close>]
   984             inj_on_image_set_diff[OF b.inj_enum Diff_subset \<open>{i} \<subseteq> {..n}\<close>]
   985       by (simp add: comp_def)
   986 
   987     have "a \<noteq> b.enum i"
   988       using \<open>a = enum i\<close> enum_eq_benum i by auto
   989 
   990     { fix t c assume "ksimplex p n t" "c \<in> t" and eq_sma: "s - {a} = t - {c}"
   991       obtain b' u where "kuhn_simplex p n b' u t"
   992         using \<open>ksimplex p n t\<close> by (auto elim: ksimplex.cases)
   993       then interpret t: kuhn_simplex p n b' u t .
   994       have "enum i' \<in> s - {a}" "enum (i + 1) \<in> s - {a}"
   995         using \<open>a = enum i\<close> i enum_in by (auto simp: enum_inj i'_def)
   996       then obtain l k where
   997         l: "t.enum l = enum i'" "l \<le> n" "t.enum l \<noteq> c" and
   998         k: "t.enum k = enum (i + 1)" "k \<le> n" "t.enum k \<noteq> c"
   999         unfolding eq_sma by (auto simp: t.s_eq)
  1000       with i have "t.enum l < t.enum k"
  1001         by (simp add: enum_strict_mono i'_def)
  1002       with \<open>l \<le> n\<close> \<open>k \<le> n\<close> have "l < k"
  1003         by (simp add: t.enum_strict_mono)
  1004       { assume "Suc l = k"
  1005         have "enum (Suc (Suc i')) = t.enum (Suc l)"
  1006           using i by (simp add: k \<open>Suc l = k\<close> i'_def)
  1007         then have False
  1008           using \<open>l < k\<close> \<open>k \<le> n\<close> \<open>Suc i' < n\<close>
  1009           by (auto simp: t.enum_Suc enum_Suc l upd_inj fun_eq_iff split: split_if_asm)
  1010              (metis Suc_lessD n_not_Suc_n upd_inj) }
  1011       with \<open>l < k\<close> have "Suc l < k"
  1012         by arith
  1013       have c_eq: "c = t.enum (Suc l)"
  1014       proof (rule ccontr)
  1015         assume "c \<noteq> t.enum (Suc l)"
  1016         then have "t.enum (Suc l) \<in> s - {a}"
  1017           using \<open>l < k\<close> \<open>k \<le> n\<close> by (simp add: t.s_eq eq_sma)
  1018         then obtain j where "t.enum (Suc l) = enum j" "j \<le> n" "enum j \<noteq> enum i"
  1019           unfolding s_eq \<open>a = enum i\<close> by auto
  1020         with i have "t.enum (Suc l) \<le> t.enum l \<or> t.enum k \<le> t.enum (Suc l)"
  1021           by (auto simp add: i'_def enum_mono enum_inj l k)
  1022         with \<open>Suc l < k\<close> \<open>k \<le> n\<close> show False
  1023           by (simp add: t.enum_mono)
  1024       qed
  1025 
  1026       { have "t.enum (Suc (Suc l)) \<in> s - {a}"
  1027           unfolding eq_sma c_eq t.s_eq using \<open>Suc l < k\<close> \<open>k \<le> n\<close> by (auto simp: t.enum_inj)
  1028         then obtain j where eq: "t.enum (Suc (Suc l)) = enum j" and "j \<le> n" "j \<noteq> i"
  1029           by (auto simp: s_eq \<open>a = enum i\<close>)
  1030         moreover have "enum i' < t.enum (Suc (Suc l))"
  1031           unfolding l(1)[symmetric] using \<open>Suc l < k\<close> \<open>k \<le> n\<close> by (auto simp: t.enum_strict_mono)
  1032         ultimately have "i' < j"
  1033           using i by (simp add: enum_strict_mono i'_def)
  1034         with \<open>j \<noteq> i\<close> \<open>j \<le> n\<close> have "t.enum k \<le> t.enum (Suc (Suc l))"
  1035           unfolding i'_def by (simp add: enum_mono k eq)
  1036         then have "k \<le> Suc (Suc l)"
  1037           using \<open>k \<le> n\<close> \<open>Suc l < k\<close> by (simp add: t.enum_mono) }
  1038       with \<open>Suc l < k\<close> have "Suc (Suc l) = k" by simp
  1039       then have "enum (Suc (Suc i')) = t.enum (Suc (Suc l))"
  1040         using i by (simp add: k i'_def)
  1041       also have "\<dots> = (enum i') (u l := Suc (enum i' (u l)), u (Suc l) := Suc (enum i' (u (Suc l))))"
  1042         using \<open>Suc l < k\<close> \<open>k \<le> n\<close> by (simp add: t.enum_Suc l t.upd_inj)
  1043       finally have "(u l = upd i' \<and> u (Suc l) = upd (Suc i')) \<or>
  1044         (u l = upd (Suc i') \<and> u (Suc l) = upd i')"
  1045         using \<open>Suc i' < n\<close> by (auto simp: enum_Suc fun_eq_iff split: split_if_asm)
  1046 
  1047       then have "t = s \<or> t = b.enum ` {..n}"
  1048       proof (elim disjE conjE)
  1049         assume u: "u l = upd i'"
  1050         have "c = t.enum (Suc l)" unfolding c_eq ..
  1051         also have "t.enum (Suc l) = enum (Suc i')"
  1052           using u \<open>l < k\<close> \<open>k \<le> n\<close> \<open>Suc i' < n\<close> by (simp add: enum_Suc t.enum_Suc l)
  1053         also have "\<dots> = a"
  1054           using \<open>a = enum i\<close> i by (simp add: i'_def)
  1055         finally show ?thesis
  1056           using eq_sma \<open>a \<in> s\<close> \<open>c \<in> t\<close> by auto
  1057       next
  1058         assume u: "u l = upd (Suc i')"
  1059         def B \<equiv> "b.enum ` {..n}"
  1060         have "b.enum i' = enum i'"
  1061           using enum_eq_benum[of i'] i by (auto simp add: i'_def gr0_conv_Suc)
  1062         have "c = t.enum (Suc l)" unfolding c_eq ..
  1063         also have "t.enum (Suc l) = b.enum (Suc i')"
  1064           using u \<open>l < k\<close> \<open>k \<le> n\<close> \<open>Suc i' < n\<close>
  1065           by (simp_all add: enum_Suc t.enum_Suc l b.enum_Suc \<open>b.enum i' = enum i'\<close> swap_apply1)
  1066              (simp add: Suc_i')
  1067         also have "\<dots> = b.enum i"
  1068           using i by (simp add: i'_def)
  1069         finally have "c = b.enum i" .
  1070         then have "t - {c} = B - {c}" "c \<in> B"
  1071           unfolding eq_sma[symmetric] eq B_def using i by auto
  1072         with \<open>c \<in> t\<close> have "t = B"
  1073           by auto
  1074         then show ?thesis
  1075           by (simp add: B_def)
  1076       qed }
  1077     with ks_f' eq \<open>a \<noteq> b.enum i\<close> \<open>n \<noteq> 0\<close> \<open>i \<le> n\<close> show ?thesis
  1078       apply (intro ex1I[of _ "b.enum ` {.. n}"])
  1079       apply auto []
  1080       apply metis
  1081       done
  1082   qed
  1083   then show ?thesis
  1084     using s \<open>a \<in> s\<close> by (simp add: card_2_exists Ex1_def) metis
  1085 qed
  1086 
  1087 text \<open>Hence another step towards concreteness.\<close>
  1088 
  1089 lemma kuhn_simplex_lemma:
  1090   assumes "\<forall>s. ksimplex p (Suc n) s \<longrightarrow> rl ` s \<subseteq> {.. Suc n}"
  1091     and "odd (card {f. \<exists>s a. ksimplex p (Suc n) s \<and> a \<in> s \<and> (f = s - {a}) \<and>
  1092       rl ` f = {..n} \<and> ((\<exists>j\<le>n. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<le>n. \<forall>x\<in>f. x j = p))})"
  1093   shows "odd (card {s. ksimplex p (Suc n) s \<and> rl ` s = {..Suc n}})"
  1094 proof (rule kuhn_complete_lemma[OF finite_ksimplexes refl, unfolded mem_Collect_eq,
  1095     where bnd="\<lambda>f. (\<exists>j\<in>{..n}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{..n}. \<forall>x\<in>f. x j = p)"],
  1096     safe del: notI)
  1097 
  1098   have *: "\<And>x y. x = y \<Longrightarrow> odd (card x) \<Longrightarrow> odd (card y)"
  1099     by auto
  1100   show "odd (card {f. (\<exists>s\<in>{s. ksimplex p (Suc n) s}. \<exists>a\<in>s. f = s - {a}) \<and>
  1101     rl ` f = {..n} \<and> ((\<exists>j\<in>{..n}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{..n}. \<forall>x\<in>f. x j = p))})"
  1102     apply (rule *[OF _ assms(2)])
  1103     apply (auto simp: atLeast0AtMost)
  1104     done
  1105 
  1106 next
  1107 
  1108   fix s assume s: "ksimplex p (Suc n) s"
  1109   then show "card s = n + 2"
  1110     by (simp add: ksimplex_card)
  1111 
  1112   fix a assume a: "a \<in> s" then show "rl a \<le> Suc n"
  1113     using assms(1) s by (auto simp: subset_eq)
  1114 
  1115   let ?S = "{t. ksimplex p (Suc n) t \<and> (\<exists>b\<in>t. s - {a} = t - {b})}"
  1116   { fix j assume j: "j \<le> n" "\<forall>x\<in>s - {a}. x j = 0"
  1117     with s a show "card ?S = 1"
  1118       using ksimplex_replace_0[of p "n + 1" s a j]
  1119       by (subst eq_commute) simp }
  1120 
  1121   { fix j assume j: "j \<le> n" "\<forall>x\<in>s - {a}. x j = p"
  1122     with s a show "card ?S = 1"
  1123       using ksimplex_replace_1[of p "n + 1" s a j]
  1124       by (subst eq_commute) simp }
  1125 
  1126   { assume "card ?S \<noteq> 2" "\<not> (\<exists>j\<in>{..n}. \<forall>x\<in>s - {a}. x j = p)"
  1127     with s a show "\<exists>j\<in>{..n}. \<forall>x\<in>s - {a}. x j = 0"
  1128       using ksimplex_replace_2[of p "n + 1" s a]
  1129       by (subst (asm) eq_commute) auto }
  1130 qed
  1131 
  1132 subsection \<open>Reduced labelling\<close>
  1133 
  1134 definition reduced :: "nat \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> nat" where "reduced n x = (LEAST k. k = n \<or> x k \<noteq> 0)"
  1135 
  1136 lemma reduced_labelling:
  1137   shows "reduced n x \<le> n"
  1138     and "\<forall>i<reduced n x. x i = 0"
  1139     and "reduced n x = n \<or> x (reduced n x) \<noteq> 0"
  1140 proof -
  1141   show "reduced n x \<le> n"
  1142     unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) auto
  1143   show "\<forall>i<reduced n x. x i = 0"
  1144     unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) fastforce+
  1145   show "reduced n x = n \<or> x (reduced n x) \<noteq> 0"
  1146     unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) fastforce+
  1147 qed
  1148 
  1149 lemma reduced_labelling_unique:
  1150   "r \<le> n \<Longrightarrow> \<forall>i<r. x i = 0 \<Longrightarrow> r = n \<or> x r \<noteq> 0 \<Longrightarrow> reduced n x = r"
  1151  unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) (metis le_less not_le)+
  1152 
  1153 lemma reduced_labelling_zero: "j < n \<Longrightarrow> x j = 0 \<Longrightarrow> reduced n x \<noteq> j"
  1154   using reduced_labelling[of n x] by auto
  1155 
  1156 lemma reduce_labelling_zero[simp]: "reduced 0 x = 0"
  1157   by (rule reduced_labelling_unique) auto
  1158 
  1159 lemma reduced_labelling_nonzero: "j < n \<Longrightarrow> x j \<noteq> 0 \<Longrightarrow> reduced n x \<le> j"
  1160   using reduced_labelling[of n x] by (elim allE[where x=j]) auto
  1161 
  1162 lemma reduced_labelling_Suc: "reduced (Suc n) x \<noteq> Suc n \<Longrightarrow> reduced (Suc n) x = reduced n x"
  1163   using reduced_labelling[of "Suc n" x]
  1164   by (intro reduced_labelling_unique[symmetric]) auto
  1165 
  1166 lemma complete_face_top:
  1167   assumes "\<forall>x\<in>f. \<forall>j\<le>n. x j = 0 \<longrightarrow> lab x j = 0"
  1168     and "\<forall>x\<in>f. \<forall>j\<le>n. x j = p \<longrightarrow> lab x j = 1"
  1169     and eq: "(reduced (Suc n) \<circ> lab) ` f = {..n}"
  1170   shows "((\<exists>j\<le>n. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<le>n. \<forall>x\<in>f. x j = p)) \<longleftrightarrow> (\<forall>x\<in>f. x n = p)"
  1171 proof (safe del: disjCI)
  1172   fix x j assume j: "j \<le> n" "\<forall>x\<in>f. x j = 0"
  1173   { fix x assume "x \<in> f" with assms j have "reduced (Suc n) (lab x) \<noteq> j"
  1174       by (intro reduced_labelling_zero) auto }
  1175   moreover have "j \<in> (reduced (Suc n) \<circ> lab) ` f"
  1176     using j eq by auto
  1177   ultimately show "x n = p"
  1178     by force
  1179 next
  1180   fix x j assume j: "j \<le> n" "\<forall>x\<in>f. x j = p" and x: "x \<in> f"
  1181   have "j = n"
  1182   proof (rule ccontr)
  1183     assume "\<not> ?thesis"
  1184     { fix x assume "x \<in> f"
  1185       with assms j have "reduced (Suc n) (lab x) \<le> j"
  1186         by (intro reduced_labelling_nonzero) auto
  1187       then have "reduced (Suc n) (lab x) \<noteq> n"
  1188         using \<open>j \<noteq> n\<close> \<open>j \<le> n\<close> by simp }
  1189     moreover
  1190     have "n \<in> (reduced (Suc n) \<circ> lab) ` f"
  1191       using eq by auto
  1192     ultimately show False
  1193       by force
  1194   qed
  1195   moreover have "j \<in> (reduced (Suc n) \<circ> lab) ` f"
  1196     using j eq by auto
  1197   ultimately show "x n = p"
  1198     using j x by auto
  1199 qed auto
  1200 
  1201 text \<open>Hence we get just about the nice induction.\<close>
  1202 
  1203 lemma kuhn_induction:
  1204   assumes "0 < p"
  1205     and lab_0: "\<forall>x. \<forall>j\<le>n. (\<forall>j. x j \<le> p) \<and> x j = 0 \<longrightarrow> lab x j = 0"
  1206     and lab_1: "\<forall>x. \<forall>j\<le>n. (\<forall>j. x j \<le> p) \<and> x j = p \<longrightarrow> lab x j = 1"
  1207     and odd: "odd (card {s. ksimplex p n s \<and> (reduced n\<circ>lab) ` s = {..n}})"
  1208   shows "odd (card {s. ksimplex p (Suc n) s \<and> (reduced (Suc n)\<circ>lab) ` s = {..Suc n}})"
  1209 proof -
  1210   let ?rl = "reduced (Suc n) \<circ> lab" and ?ext = "\<lambda>f v. \<exists>j\<le>n. \<forall>x\<in>f. x j = v"
  1211   let ?ext = "\<lambda>s. (\<exists>j\<le>n. \<forall>x\<in>s. x j = 0) \<or> (\<exists>j\<le>n. \<forall>x\<in>s. x j = p)"
  1212   have "\<forall>s. ksimplex p (Suc n) s \<longrightarrow> ?rl ` s \<subseteq> {..Suc n}"
  1213     by (simp add: reduced_labelling subset_eq)
  1214   moreover
  1215   have "{s. ksimplex p n s \<and> (reduced n \<circ> lab) ` s = {..n}} =
  1216         {f. \<exists>s a. ksimplex p (Suc n) s \<and> a \<in> s \<and> f = s - {a} \<and> ?rl ` f = {..n} \<and> ?ext f}"
  1217   proof (intro set_eqI, safe del: disjCI equalityI disjE)
  1218     fix s assume s: "ksimplex p n s" and rl: "(reduced n \<circ> lab) ` s = {..n}"
  1219     from s obtain u b where "kuhn_simplex p n u b s" by (auto elim: ksimplex.cases)
  1220     then interpret kuhn_simplex p n u b s .
  1221     have all_eq_p: "\<forall>x\<in>s. x n = p"
  1222       by (auto simp: out_eq_p)
  1223     moreover
  1224     { fix x assume "x \<in> s"
  1225       with lab_1[rule_format, of n x] all_eq_p s_le_p[of x]
  1226       have "?rl x \<le> n"
  1227         by (auto intro!: reduced_labelling_nonzero)
  1228       then have "?rl x = reduced n (lab x)"
  1229         by (auto intro!: reduced_labelling_Suc) }
  1230     then have "?rl ` s = {..n}"
  1231       using rl by (simp cong: image_cong)
  1232     moreover
  1233     obtain t a where "ksimplex p (Suc n) t" "a \<in> t" "s = t - {a}"
  1234       using s unfolding simplex_top_face[OF \<open>0 < p\<close> all_eq_p] by auto
  1235     ultimately
  1236     show "\<exists>t a. ksimplex p (Suc n) t \<and> a \<in> t \<and> s = t - {a} \<and> ?rl ` s = {..n} \<and> ?ext s"
  1237       by auto
  1238   next
  1239     fix x s a assume s: "ksimplex p (Suc n) s" and rl: "?rl ` (s - {a}) = {.. n}"
  1240       and a: "a \<in> s" and "?ext (s - {a})"
  1241     from s obtain u b where "kuhn_simplex p (Suc n) u b s" by (auto elim: ksimplex.cases)
  1242     then interpret kuhn_simplex p "Suc n" u b s .
  1243     have all_eq_p: "\<forall>x\<in>s. x (Suc n) = p"
  1244       by (auto simp: out_eq_p)
  1245 
  1246     { fix x assume "x \<in> s - {a}"
  1247       then have "?rl x \<in> ?rl ` (s - {a})"
  1248         by auto
  1249       then have "?rl x \<le> n"
  1250         unfolding rl by auto
  1251       then have "?rl x = reduced n (lab x)"
  1252         by (auto intro!: reduced_labelling_Suc) }
  1253     then show rl': "(reduced n\<circ>lab) ` (s - {a}) = {..n}"
  1254       unfolding rl[symmetric] by (intro image_cong) auto
  1255 
  1256     from \<open>?ext (s - {a})\<close>
  1257     have all_eq_p: "\<forall>x\<in>s - {a}. x n = p"
  1258     proof (elim disjE exE conjE)
  1259       fix j assume "j \<le> n" "\<forall>x\<in>s - {a}. x j = 0"
  1260       with lab_0[rule_format, of j] all_eq_p s_le_p
  1261       have "\<And>x. x \<in> s - {a} \<Longrightarrow> reduced (Suc n) (lab x) \<noteq> j"
  1262         by (intro reduced_labelling_zero) auto
  1263       moreover have "j \<in> ?rl ` (s - {a})"
  1264         using \<open>j \<le> n\<close> unfolding rl by auto
  1265       ultimately show ?thesis
  1266         by force
  1267     next
  1268       fix j assume "j \<le> n" and eq_p: "\<forall>x\<in>s - {a}. x j = p"
  1269       show ?thesis
  1270       proof cases
  1271         assume "j = n" with eq_p show ?thesis by simp
  1272       next
  1273         assume "j \<noteq> n"
  1274         { fix x assume x: "x \<in> s - {a}"
  1275           have "reduced n (lab x) \<le> j"
  1276           proof (rule reduced_labelling_nonzero)
  1277             show "lab x j \<noteq> 0"
  1278               using lab_1[rule_format, of j x] x s_le_p[of x] eq_p \<open>j \<le> n\<close> by auto
  1279             show "j < n"
  1280               using \<open>j \<le> n\<close> \<open>j \<noteq> n\<close> by simp
  1281           qed
  1282           then have "reduced n (lab x) \<noteq> n"
  1283             using \<open>j \<le> n\<close> \<open>j \<noteq> n\<close> by simp }
  1284         moreover have "n \<in> (reduced n\<circ>lab) ` (s - {a})"
  1285           unfolding rl' by auto
  1286         ultimately show ?thesis
  1287           by force
  1288       qed
  1289     qed
  1290     show "ksimplex p n (s - {a})"
  1291       unfolding simplex_top_face[OF \<open>0 < p\<close> all_eq_p] using s a by auto
  1292   qed
  1293   ultimately show ?thesis
  1294     using assms by (intro kuhn_simplex_lemma) auto
  1295 qed
  1296 
  1297 text \<open>And so we get the final combinatorial result.\<close>
  1298 
  1299 lemma ksimplex_0: "ksimplex p 0 s \<longleftrightarrow> s = {(\<lambda>x. p)}"
  1300 proof
  1301   assume "ksimplex p 0 s" then show "s = {(\<lambda>x. p)}"
  1302     by (blast dest: kuhn_simplex.ksimplex_0 elim: ksimplex.cases)
  1303 next
  1304   assume s: "s = {(\<lambda>x. p)}"
  1305   show "ksimplex p 0 s"
  1306   proof (intro ksimplex, unfold_locales)
  1307     show "(\<lambda>_. p) \<in> {..<0::nat} \<rightarrow> {..<p}" by auto
  1308     show "bij_betw id {..<0} {..<0}"
  1309       by simp
  1310   qed (auto simp: s)
  1311 qed
  1312 
  1313 lemma kuhn_combinatorial:
  1314   assumes "0 < p"
  1315     and "\<forall>x j. (\<forall>j. x j \<le> p) \<and> j < n \<and> x j = 0 \<longrightarrow> lab x j = 0"
  1316     and "\<forall>x j. (\<forall>j. x j \<le> p) \<and> j < n  \<and> x j = p \<longrightarrow> lab x j = 1"
  1317   shows "odd (card {s. ksimplex p n s \<and> (reduced n\<circ>lab) ` s = {..n}})"
  1318     (is "odd (card (?M n))")
  1319   using assms
  1320 proof (induct n)
  1321   case 0 then show ?case
  1322     by (simp add: ksimplex_0 cong: conj_cong)
  1323 next
  1324   case (Suc n)
  1325   then have "odd (card (?M n))"
  1326     by force
  1327   with Suc show ?case
  1328     using kuhn_induction[of p n] by (auto simp: comp_def)
  1329 qed
  1330 
  1331 lemma kuhn_lemma:
  1332   fixes n p :: nat
  1333   assumes "0 < p"
  1334     and "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. label x i = (0::nat) \<or> label x i = 1)"
  1335     and "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = 0 \<longrightarrow> label x i = 0)"
  1336     and "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = p \<longrightarrow> label x i = 1)"
  1337   obtains q where "\<forall>i<n. q i < p"
  1338     and "\<forall>i<n. \<exists>r s. (\<forall>j<n. q j \<le> r j \<and> r j \<le> q j + 1) \<and> (\<forall>j<n. q j \<le> s j \<and> s j \<le> q j + 1) \<and> label r i \<noteq> label s i"
  1339 proof -
  1340   let ?rl = "reduced n \<circ> label"
  1341   let ?A = "{s. ksimplex p n s \<and> ?rl ` s = {..n}}"
  1342   have "odd (card ?A)"
  1343     using assms by (intro kuhn_combinatorial[of p n label]) auto
  1344   then have "?A \<noteq> {}"
  1345     by fastforce
  1346   then obtain s b u where "kuhn_simplex p n b u s" and rl: "?rl ` s = {..n}"
  1347     by (auto elim: ksimplex.cases)
  1348   interpret kuhn_simplex p n b u s by fact
  1349 
  1350   show ?thesis
  1351   proof (intro that[of b] allI impI)
  1352     fix i
  1353     assume "i < n"
  1354     then show "b i < p"
  1355       using base by auto
  1356   next
  1357     fix i
  1358     assume "i < n"
  1359     then have "i \<in> {.. n}" "Suc i \<in> {.. n}"
  1360       by auto
  1361     then obtain u v where u: "u \<in> s" "Suc i = ?rl u" and v: "v \<in> s" "i = ?rl v"
  1362       unfolding rl[symmetric] by blast
  1363 
  1364     have "label u i \<noteq> label v i"
  1365       using reduced_labelling [of n "label u"] reduced_labelling [of n "label v"]
  1366         u(2)[symmetric] v(2)[symmetric] \<open>i < n\<close>
  1367       by auto
  1368     moreover
  1369     have "b j \<le> u j" "u j \<le> b j + 1" "b j \<le> v j" "v j \<le> b j + 1" if "j < n" for j
  1370       using that base_le[OF \<open>u\<in>s\<close>] le_Suc_base[OF \<open>u\<in>s\<close>] base_le[OF \<open>v\<in>s\<close>] le_Suc_base[OF \<open>v\<in>s\<close>]
  1371       by auto
  1372     ultimately show "\<exists>r s. (\<forall>j<n. b j \<le> r j \<and> r j \<le> b j + 1) \<and>
  1373         (\<forall>j<n. b j \<le> s j \<and> s j \<le> b j + 1) \<and> label r i \<noteq> label s i"
  1374       by blast
  1375   qed
  1376 qed
  1377 
  1378 subsection \<open>The main result for the unit cube\<close>
  1379 
  1380 lemma kuhn_labelling_lemma':
  1381   assumes "(\<forall>x::nat\<Rightarrow>real. P x \<longrightarrow> P (f x))"
  1382     and "\<forall>x. P x \<longrightarrow> (\<forall>i::nat. Q i \<longrightarrow> 0 \<le> x i \<and> x i \<le> 1)"
  1383   shows "\<exists>l. (\<forall>x i. l x i \<le> (1::nat)) \<and>
  1384              (\<forall>x i. P x \<and> Q i \<and> x i = 0 \<longrightarrow> l x i = 0) \<and>
  1385              (\<forall>x i. P x \<and> Q i \<and> x i = 1 \<longrightarrow> l x i = 1) \<and>
  1386              (\<forall>x i. P x \<and> Q i \<and> l x i = 0 \<longrightarrow> x i \<le> f x i) \<and>
  1387              (\<forall>x i. P x \<and> Q i \<and> l x i = 1 \<longrightarrow> f x i \<le> x i)"
  1388 proof -
  1389   have and_forall_thm: "\<And>P Q. (\<forall>x. P x) \<and> (\<forall>x. Q x) \<longleftrightarrow> (\<forall>x. P x \<and> Q x)"
  1390     by auto
  1391   have *: "\<forall>x y::real. 0 \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1 \<longrightarrow> x \<noteq> 1 \<and> x \<le> y \<or> x \<noteq> 0 \<and> y \<le> x"
  1392     by auto
  1393   show ?thesis
  1394     unfolding and_forall_thm
  1395     apply (subst choice_iff[symmetric])+
  1396     apply rule
  1397     apply rule
  1398   proof -
  1399     fix x x'
  1400     let ?R = "\<lambda>y::nat.
  1401       (P x \<and> Q x' \<and> x x' = 0 \<longrightarrow> y = 0) \<and>
  1402       (P x \<and> Q x' \<and> x x' = 1 \<longrightarrow> y = 1) \<and>
  1403       (P x \<and> Q x' \<and> y = 0 \<longrightarrow> x x' \<le> (f x) x') \<and>
  1404       (P x \<and> Q x' \<and> y = 1 \<longrightarrow> (f x) x' \<le> x x')"
  1405     have "0 \<le> f x x' \<and> f x x' \<le> 1" if "P x" "Q x'"
  1406       using assms(2)[rule_format,of "f x" x'] that
  1407       apply (drule_tac assms(1)[rule_format])
  1408       apply auto
  1409       done
  1410     then have "?R 0 \<or> ?R 1"
  1411       by auto
  1412     then show "\<exists>y\<le>1. ?R y"
  1413       by auto
  1414   qed
  1415 qed
  1416 
  1417 definition unit_cube :: "'a::euclidean_space set"
  1418   where "unit_cube = {x. \<forall>i\<in>Basis. 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1}"
  1419 
  1420 lemma mem_unit_cube: "x \<in> unit_cube \<longleftrightarrow> (\<forall>i\<in>Basis. 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1)"
  1421   unfolding unit_cube_def by simp
  1422 
  1423 lemma bounded_unit_cube: "bounded unit_cube"
  1424   unfolding bounded_def
  1425 proof (intro exI ballI)
  1426   fix y :: 'a assume y: "y \<in> unit_cube"
  1427   have "dist 0 y = norm y" by (rule dist_0_norm)
  1428   also have "\<dots> = norm (\<Sum>i\<in>Basis. (y \<bullet> i) *\<^sub>R i)" unfolding euclidean_representation ..
  1429   also have "\<dots> \<le> (\<Sum>i\<in>Basis. norm ((y \<bullet> i) *\<^sub>R i))" by (rule norm_setsum)
  1430   also have "\<dots> \<le> (\<Sum>i::'a\<in>Basis. 1)"
  1431     by (rule setsum_mono, simp add: y [unfolded mem_unit_cube])
  1432   finally show "dist 0 y \<le> (\<Sum>i::'a\<in>Basis. 1)" .
  1433 qed
  1434 
  1435 lemma closed_unit_cube: "closed unit_cube"
  1436   unfolding unit_cube_def Collect_ball_eq Collect_conj_eq
  1437   by (rule closed_INT, auto intro!: closed_Collect_le)
  1438 
  1439 lemma compact_unit_cube: "compact unit_cube" (is "compact ?C")
  1440   unfolding compact_eq_seq_compact_metric
  1441   using bounded_unit_cube closed_unit_cube
  1442   by (rule bounded_closed_imp_seq_compact)
  1443 
  1444 lemma brouwer_cube:
  1445   fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
  1446   assumes "continuous_on unit_cube f"
  1447     and "f ` unit_cube \<subseteq> unit_cube"
  1448   shows "\<exists>x\<in>unit_cube. f x = x"
  1449 proof (rule ccontr)
  1450   def n \<equiv> "DIM('a)"
  1451   have n: "1 \<le> n" "0 < n" "n \<noteq> 0"
  1452     unfolding n_def by (auto simp add: Suc_le_eq DIM_positive)
  1453   assume "\<not> ?thesis"
  1454   then have *: "\<not> (\<exists>x\<in>unit_cube. f x - x = 0)"
  1455     by auto
  1456   obtain d where
  1457       d: "d > 0" "\<And>x. x \<in> unit_cube \<Longrightarrow> d \<le> norm (f x - x)"
  1458     apply (rule brouwer_compactness_lemma[OF compact_unit_cube _ *])
  1459     apply (rule continuous_intros assms)+
  1460     apply blast
  1461     done
  1462   have *: "\<forall>x. x \<in> unit_cube \<longrightarrow> f x \<in> unit_cube"
  1463     "\<forall>x. x \<in> (unit_cube::'a set) \<longrightarrow> (\<forall>i\<in>Basis. True \<longrightarrow> 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1)"
  1464     using assms(2)[unfolded image_subset_iff Ball_def]
  1465     unfolding mem_unit_cube
  1466     by auto
  1467   obtain label :: "'a \<Rightarrow> 'a \<Rightarrow> nat" where
  1468     "\<forall>x. \<forall>i\<in>Basis. label x i \<le> 1"
  1469     "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> True \<and> x \<bullet> i = 0 \<longrightarrow> label x i = 0"
  1470     "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> True \<and> x \<bullet> i = 1 \<longrightarrow> label x i = 1"
  1471     "\<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"
  1472     "\<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"
  1473     using kuhn_labelling_lemma[OF *] by blast
  1474   note label = this [rule_format]
  1475   have lem1: "\<forall>x\<in>unit_cube. \<forall>y\<in>unit_cube. \<forall>i\<in>Basis. label x i \<noteq> label y i \<longrightarrow>
  1476     \<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y - f x) + norm (y - x)"
  1477   proof safe
  1478     fix x y :: 'a
  1479     assume x: "x \<in> unit_cube"
  1480     assume y: "y \<in> unit_cube"
  1481     fix i
  1482     assume i: "label x i \<noteq> label y i" "i \<in> Basis"
  1483     have *: "\<And>x y fx fy :: real. x \<le> fx \<and> fy \<le> y \<or> fx \<le> x \<and> y \<le> fy \<Longrightarrow>
  1484       \<bar>fx - x\<bar> \<le> \<bar>fy - fx\<bar> + \<bar>y - x\<bar>" by auto
  1485     have "\<bar>(f x - x) \<bullet> i\<bar> \<le> \<bar>(f y - f x)\<bullet>i\<bar> + \<bar>(y - x)\<bullet>i\<bar>"
  1486       unfolding inner_simps
  1487       apply (rule *)
  1488       apply (cases "label x i = 0")
  1489       apply (rule disjI1)
  1490       apply rule
  1491       prefer 3
  1492       apply (rule disjI2)
  1493       apply rule
  1494     proof -
  1495       assume lx: "label x i = 0"
  1496       then have ly: "label y i = 1"
  1497         using i label(1)[of i y]
  1498         by auto
  1499       show "x \<bullet> i \<le> f x \<bullet> i"
  1500         apply (rule label(4)[rule_format])
  1501         using x y lx i(2)
  1502         apply auto
  1503         done
  1504       show "f y \<bullet> i \<le> y \<bullet> i"
  1505         apply (rule label(5)[rule_format])
  1506         using x y ly i(2)
  1507         apply auto
  1508         done
  1509     next
  1510       assume "label x i \<noteq> 0"
  1511       then have l: "label x i = 1" "label y i = 0"
  1512         using i label(1)[of i x] label(1)[of i y]
  1513         by auto
  1514       show "f x \<bullet> i \<le> x \<bullet> i"
  1515         apply (rule label(5)[rule_format])
  1516         using x y l i(2)
  1517         apply auto
  1518         done
  1519       show "y \<bullet> i \<le> f y \<bullet> i"
  1520         apply (rule label(4)[rule_format])
  1521         using x y l i(2)
  1522         apply auto
  1523         done
  1524     qed
  1525     also have "\<dots> \<le> norm (f y - f x) + norm (y - x)"
  1526       apply (rule add_mono)
  1527       apply (rule Basis_le_norm[OF i(2)])+
  1528       done
  1529     finally show "\<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y - f x) + norm (y - x)"
  1530       unfolding inner_simps .
  1531   qed
  1532   have "\<exists>e>0. \<forall>x\<in>unit_cube. \<forall>y\<in>unit_cube. \<forall>z\<in>unit_cube. \<forall>i\<in>Basis.
  1533     norm (x - z) < e \<and> norm (y - z) < e \<and> label x i \<noteq> label y i \<longrightarrow>
  1534       \<bar>(f(z) - z)\<bullet>i\<bar> < d / (real n)"
  1535   proof -
  1536     have d': "d / real n / 8 > 0"
  1537       using d(1) by (simp add: n_def DIM_positive)
  1538     have *: "uniformly_continuous_on unit_cube f"
  1539       by (rule compact_uniformly_continuous[OF assms(1) compact_unit_cube])
  1540     obtain e where e:
  1541         "e > 0"
  1542         "\<And>x x'. x \<in> unit_cube \<Longrightarrow>
  1543           x' \<in> unit_cube \<Longrightarrow>
  1544           norm (x' - x) < e \<Longrightarrow>
  1545           norm (f x' - f x) < d / real n / 8"
  1546       using *[unfolded uniformly_continuous_on_def,rule_format,OF d']
  1547       unfolding dist_norm
  1548       by blast
  1549     show ?thesis
  1550       apply (rule_tac x="min (e/2) (d/real n/8)" in exI)
  1551       apply safe
  1552     proof -
  1553       show "0 < min (e / 2) (d / real n / 8)"
  1554         using d' e by auto
  1555       fix x y z i
  1556       assume as:
  1557         "x \<in> unit_cube" "y \<in> unit_cube" "z \<in> unit_cube"
  1558         "norm (x - z) < min (e / 2) (d / real n / 8)"
  1559         "norm (y - z) < min (e / 2) (d / real n / 8)"
  1560         "label x i \<noteq> label y i"
  1561       assume i: "i \<in> Basis"
  1562       have *: "\<And>z fz x fx n1 n2 n3 n4 d4 d :: real. \<bar>fx - x\<bar> \<le> n1 + n2 \<Longrightarrow>
  1563         \<bar>fx - fz\<bar> \<le> n3 \<Longrightarrow> \<bar>x - z\<bar> \<le> n4 \<Longrightarrow>
  1564         n1 < d4 \<Longrightarrow> n2 < 2 * d4 \<Longrightarrow> n3 < d4 \<Longrightarrow> n4 < d4 \<Longrightarrow>
  1565         (8 * d4 = d) \<Longrightarrow> \<bar>fz - z\<bar> < d"
  1566         by auto
  1567       show "\<bar>(f z - z) \<bullet> i\<bar> < d / real n"
  1568         unfolding inner_simps
  1569       proof (rule *)
  1570         show "\<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y -f x) + norm (y - x)"
  1571           apply (rule lem1[rule_format])
  1572           using as i
  1573           apply auto
  1574           done
  1575         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)"
  1576           unfolding inner_diff_left[symmetric]
  1577           by (rule Basis_le_norm[OF i])+
  1578         have tria: "norm (y - x) \<le> norm (y - z) + norm (x - z)"
  1579           using dist_triangle[of y x z, unfolded dist_norm]
  1580           unfolding norm_minus_commute
  1581           by auto
  1582         also have "\<dots> < e / 2 + e / 2"
  1583           apply (rule add_strict_mono)
  1584           using as(4,5)
  1585           apply auto
  1586           done
  1587         finally show "norm (f y - f x) < d / real n / 8"
  1588           apply -
  1589           apply (rule e(2))
  1590           using as
  1591           apply auto
  1592           done
  1593         have "norm (y - z) + norm (x - z) < d / real n / 8 + d / real n / 8"
  1594           apply (rule add_strict_mono)
  1595           using as
  1596           apply auto
  1597           done
  1598         then show "norm (y - x) < 2 * (d / real n / 8)"
  1599           using tria
  1600           by auto
  1601         show "norm (f x - f z) < d / real n / 8"
  1602           apply (rule e(2))
  1603           using as e(1)
  1604           apply auto
  1605           done
  1606       qed (insert as, auto)
  1607     qed
  1608   qed
  1609   then
  1610   obtain e where e:
  1611     "e > 0"
  1612     "\<And>x y z i. x \<in> unit_cube \<Longrightarrow>
  1613       y \<in> unit_cube \<Longrightarrow>
  1614       z \<in> unit_cube \<Longrightarrow>
  1615       i \<in> Basis \<Longrightarrow>
  1616       norm (x - z) < e \<and> norm (y - z) < e \<and> label x i \<noteq> label y i \<Longrightarrow>
  1617       \<bar>(f z - z) \<bullet> i\<bar> < d / real n"
  1618     by blast
  1619   obtain p :: nat where p: "1 + real n / e \<le> real p"
  1620     using real_arch_simple ..
  1621   have "1 + real n / e > 0"
  1622     using e(1) n by (simp add: add_pos_pos)
  1623   then have "p > 0"
  1624     using p by auto
  1625 
  1626   obtain b :: "nat \<Rightarrow> 'a" where b: "bij_betw b {..< n} Basis"
  1627     by atomize_elim (auto simp: n_def intro!: finite_same_card_bij)
  1628   def b' \<equiv> "inv_into {..< n} b"
  1629   then have b': "bij_betw b' Basis {..< n}"
  1630     using bij_betw_inv_into[OF b] by auto
  1631   then have b'_Basis: "\<And>i. i \<in> Basis \<Longrightarrow> b' i \<in> {..< n}"
  1632     unfolding bij_betw_def by (auto simp: set_eq_iff)
  1633   have bb'[simp]:"\<And>i. i \<in> Basis \<Longrightarrow> b (b' i) = i"
  1634     unfolding b'_def
  1635     using b
  1636     by (auto simp: f_inv_into_f bij_betw_def)
  1637   have b'b[simp]:"\<And>i. i < n \<Longrightarrow> b' (b i) = i"
  1638     unfolding b'_def
  1639     using b
  1640     by (auto simp: inv_into_f_eq bij_betw_def)
  1641   have *: "\<And>x :: nat. x = 0 \<or> x = 1 \<longleftrightarrow> x \<le> 1"
  1642     by auto
  1643   have b'': "\<And>j. j < n \<Longrightarrow> b j \<in> Basis"
  1644     using b unfolding bij_betw_def by auto
  1645   have q1: "0 < p" "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow>
  1646     (\<forall>i<n. (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0 \<or>
  1647            (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 1)"
  1648     unfolding *
  1649     using \<open>p > 0\<close> \<open>n > 0\<close>
  1650     using label(1)[OF b'']
  1651     by auto
  1652   { fix x :: "nat \<Rightarrow> nat" and i assume "\<forall>i<n. x i \<le> p" "i < n" "x i = p \<or> x i = 0"
  1653     then have "(\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<in> (unit_cube::'a set)"
  1654       using b'_Basis
  1655       by (auto simp add: mem_unit_cube inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1) }
  1656   note cube = this
  1657   have q2: "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = 0 \<longrightarrow>
  1658       (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0)"
  1659     unfolding o_def using cube \<open>p > 0\<close> by (intro allI impI label(2)) (auto simp add: b'')
  1660   have q3: "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = p \<longrightarrow>
  1661       (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 1)"
  1662     using cube \<open>p > 0\<close> unfolding o_def by (intro allI impI label(3)) (auto simp add: b'')
  1663   obtain q where q:
  1664       "\<forall>i<n. q i < p"
  1665       "\<forall>i<n.
  1666          \<exists>r s. (\<forall>j<n. q j \<le> r j \<and> r j \<le> q j + 1) \<and>
  1667                (\<forall>j<n. q j \<le> s j \<and> s j \<le> q j + 1) \<and>
  1668                (label (\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i) \<circ> b) i \<noteq>
  1669                (label (\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i) \<circ> b) i"
  1670     by (rule kuhn_lemma[OF q1 q2 q3])
  1671   def z \<equiv> "(\<Sum>i\<in>Basis. (real (q (b' i)) / real p) *\<^sub>R i)::'a"
  1672   have "\<exists>i\<in>Basis. d / real n \<le> \<bar>(f z - z)\<bullet>i\<bar>"
  1673   proof (rule ccontr)
  1674     have "\<forall>i\<in>Basis. q (b' i) \<in> {0..p}"
  1675       using q(1) b'
  1676       by (auto intro: less_imp_le simp: bij_betw_def)
  1677     then have "z \<in> unit_cube"
  1678       unfolding z_def mem_unit_cube
  1679       using b'_Basis
  1680       by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1)
  1681     then have d_fz_z: "d \<le> norm (f z - z)"
  1682       by (rule d)
  1683     assume "\<not> ?thesis"
  1684     then have as: "\<forall>i\<in>Basis. \<bar>f z \<bullet> i - z \<bullet> i\<bar> < d / real n"
  1685       using \<open>n > 0\<close>
  1686       by (auto simp add: not_le inner_diff)
  1687     have "norm (f z - z) \<le> (\<Sum>i\<in>Basis. \<bar>f z \<bullet> i - z \<bullet> i\<bar>)"
  1688       unfolding inner_diff_left[symmetric]
  1689       by (rule norm_le_l1)
  1690     also have "\<dots> < (\<Sum>(i::'a) \<in> Basis. d / real n)"
  1691       apply (rule setsum_strict_mono)
  1692       using as
  1693       apply auto
  1694       done
  1695     also have "\<dots> = d"
  1696       using DIM_positive[where 'a='a]
  1697       by (auto simp: n_def)
  1698     finally show False
  1699       using d_fz_z by auto
  1700   qed
  1701   then obtain i where i: "i \<in> Basis" "d / real n \<le> \<bar>(f z - z) \<bullet> i\<bar>" ..
  1702   have *: "b' i < n"
  1703     using i and b'[unfolded bij_betw_def]
  1704     by auto
  1705   obtain r s where rs:
  1706     "\<And>j. j < n \<Longrightarrow> q j \<le> r j \<and> r j \<le> q j + 1"
  1707     "\<And>j. j < n \<Longrightarrow> q j \<le> s j \<and> s j \<le> q j + 1"
  1708     "(label (\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i) \<circ> b) (b' i) \<noteq>
  1709       (label (\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i) \<circ> b) (b' i)"
  1710     using q(2)[rule_format,OF *] by blast
  1711   have b'_im: "\<And>i. i \<in> Basis \<Longrightarrow>  b' i < n"
  1712     using b' unfolding bij_betw_def by auto
  1713   def r' \<equiv> "(\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i)::'a"
  1714   have "\<And>i. i \<in> Basis \<Longrightarrow> r (b' i) \<le> p"
  1715     apply (rule order_trans)
  1716     apply (rule rs(1)[OF b'_im,THEN conjunct2])
  1717     using q(1)[rule_format,OF b'_im]
  1718     apply (auto simp add: Suc_le_eq)
  1719     done
  1720   then have "r' \<in> unit_cube"
  1721     unfolding r'_def mem_unit_cube
  1722     using b'_Basis
  1723     by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1)
  1724   def s' \<equiv> "(\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i)::'a"
  1725   have "\<And>i. i \<in> Basis \<Longrightarrow> s (b' i) \<le> p"
  1726     apply (rule order_trans)
  1727     apply (rule rs(2)[OF b'_im, THEN conjunct2])
  1728     using q(1)[rule_format,OF b'_im]
  1729     apply (auto simp add: Suc_le_eq)
  1730     done
  1731   then have "s' \<in> unit_cube"
  1732     unfolding s'_def mem_unit_cube
  1733     using b'_Basis
  1734     by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1)
  1735   have "z \<in> unit_cube"
  1736     unfolding z_def mem_unit_cube
  1737     using b'_Basis q(1)[rule_format,OF b'_im] \<open>p > 0\<close>
  1738     by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1 less_imp_le)
  1739   have *: "\<And>x. 1 + real x = real (Suc x)"
  1740     by auto
  1741   {
  1742     have "(\<Sum>i\<in>Basis. \<bar>real (r (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
  1743       apply (rule setsum_mono)
  1744       using rs(1)[OF b'_im]
  1745       apply (auto simp add:* field_simps simp del: of_nat_Suc)
  1746       done
  1747     also have "\<dots> < e * real p"
  1748       using p \<open>e > 0\<close> \<open>p > 0\<close>
  1749       by (auto simp add: field_simps n_def)
  1750     finally have "(\<Sum>i\<in>Basis. \<bar>real (r (b' i)) - real (q (b' i))\<bar>) < e * real p" .
  1751   }
  1752   moreover
  1753   {
  1754     have "(\<Sum>i\<in>Basis. \<bar>real (s (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
  1755       apply (rule setsum_mono)
  1756       using rs(2)[OF b'_im]
  1757       apply (auto simp add:* field_simps simp del: of_nat_Suc)
  1758       done
  1759     also have "\<dots> < e * real p"
  1760       using p \<open>e > 0\<close> \<open>p > 0\<close>
  1761       by (auto simp add: field_simps n_def)
  1762     finally have "(\<Sum>i\<in>Basis. \<bar>real (s (b' i)) - real (q (b' i))\<bar>) < e * real p" .
  1763   }
  1764   ultimately
  1765   have "norm (r' - z) < e" and "norm (s' - z) < e"
  1766     unfolding r'_def s'_def z_def
  1767     using \<open>p > 0\<close>
  1768     apply (rule_tac[!] le_less_trans[OF norm_le_l1])
  1769     apply (auto simp add: field_simps setsum_divide_distrib[symmetric] inner_diff_left)
  1770     done
  1771   then have "\<bar>(f z - z) \<bullet> i\<bar> < d / real n"
  1772     using rs(3) i
  1773     unfolding r'_def[symmetric] s'_def[symmetric] o_def bb'
  1774     by (intro e(2)[OF \<open>r'\<in>unit_cube\<close> \<open>s'\<in>unit_cube\<close> \<open>z\<in>unit_cube\<close>]) auto
  1775   then show False
  1776     using i by auto
  1777 qed
  1778 
  1779 
  1780 subsection \<open>Retractions\<close>
  1781 
  1782 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)"
  1783 
  1784 definition retract_of (infixl "retract'_of" 12)
  1785   where "(t retract_of s) \<longleftrightarrow> (\<exists>r. retraction s t r)"
  1786 
  1787 lemma retraction_idempotent: "retraction s t r \<Longrightarrow> x \<in> s \<Longrightarrow>  r (r x) = r x"
  1788   unfolding retraction_def by auto
  1789 
  1790 subsection \<open>Preservation of fixpoints under (more general notion of) retraction\<close>
  1791 
  1792 lemma invertible_fixpoint_property:
  1793   fixes s :: "'a::euclidean_space set"
  1794     and t :: "'b::euclidean_space set"
  1795   assumes "continuous_on t i"
  1796     and "i ` t \<subseteq> s"
  1797     and "continuous_on s r"
  1798     and "r ` s \<subseteq> t"
  1799     and "\<forall>y\<in>t. r (i y) = y"
  1800     and "\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)"
  1801     and "continuous_on t g"
  1802     and "g ` t \<subseteq> t"
  1803   obtains y where "y \<in> t" and "g y = y"
  1804 proof -
  1805   have "\<exists>x\<in>s. (i \<circ> g \<circ> r) x = x"
  1806     apply (rule assms(6)[rule_format])
  1807     apply rule
  1808     apply (rule continuous_on_compose assms)+
  1809     apply ((rule continuous_on_subset)?, rule assms)+
  1810     using assms(2,4,8)
  1811     apply auto
  1812     apply blast
  1813     done
  1814   then obtain x where x: "x \<in> s" "(i \<circ> g \<circ> r) x = x" ..
  1815   then have *: "g (r x) \<in> t"
  1816     using assms(4,8) by auto
  1817   have "r ((i \<circ> g \<circ> r) x) = r x"
  1818     using x by auto
  1819   then show ?thesis
  1820     apply (rule_tac that[of "r x"])
  1821     using x
  1822     unfolding o_def
  1823     unfolding assms(5)[rule_format,OF *]
  1824     using assms(4)
  1825     apply auto
  1826     done
  1827 qed
  1828 
  1829 lemma homeomorphic_fixpoint_property:
  1830   fixes s :: "'a::euclidean_space set"
  1831     and t :: "'b::euclidean_space set"
  1832   assumes "s homeomorphic t"
  1833   shows "(\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)) \<longleftrightarrow>
  1834     (\<forall>g. continuous_on t g \<and> g ` t \<subseteq> t \<longrightarrow> (\<exists>y\<in>t. g y = y))"
  1835 proof -
  1836   obtain r i where
  1837       "\<forall>x\<in>s. i (r x) = x"
  1838       "r ` s = t"
  1839       "continuous_on s r"
  1840       "\<forall>y\<in>t. r (i y) = y"
  1841       "i ` t = s"
  1842       "continuous_on t i"
  1843     using assms
  1844     unfolding homeomorphic_def homeomorphism_def
  1845     by blast
  1846   then show ?thesis
  1847     apply -
  1848     apply rule
  1849     apply (rule_tac[!] allI impI)+
  1850     apply (rule_tac g=g in invertible_fixpoint_property[of t i s r])
  1851     prefer 10
  1852     apply (rule_tac g=f in invertible_fixpoint_property[of s r t i])
  1853     apply auto
  1854     done
  1855 qed
  1856 
  1857 lemma retract_fixpoint_property:
  1858   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  1859     and s :: "'a set"
  1860   assumes "t retract_of s"
  1861     and "\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)"
  1862     and "continuous_on t g"
  1863     and "g ` t \<subseteq> t"
  1864   obtains y where "y \<in> t" and "g y = y"
  1865 proof -
  1866   obtain h where "retraction s t h"
  1867     using assms(1) unfolding retract_of_def ..
  1868   then show ?thesis
  1869     unfolding retraction_def
  1870     apply -
  1871     apply (rule invertible_fixpoint_property[OF continuous_on_id _ _ _ _ assms(2), of t h g])
  1872     prefer 7
  1873     apply (rule_tac y = y in that)
  1874     using assms
  1875     apply auto
  1876     done
  1877 qed
  1878 
  1879 
  1880 subsection \<open>The Brouwer theorem for any set with nonempty interior\<close>
  1881 
  1882 lemma convex_unit_cube: "convex unit_cube"
  1883   apply (rule is_interval_convex)
  1884   apply (clarsimp simp add: is_interval_def mem_unit_cube)
  1885   apply (drule (1) bspec)+
  1886   apply auto
  1887   done
  1888 
  1889 lemma brouwer_weak:
  1890   fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
  1891   assumes "compact s"
  1892     and "convex s"
  1893     and "interior s \<noteq> {}"
  1894     and "continuous_on s f"
  1895     and "f ` s \<subseteq> s"
  1896   obtains x where "x \<in> s" and "f x = x"
  1897 proof -
  1898   let ?U = "unit_cube :: 'a set"
  1899   have "\<Sum>Basis /\<^sub>R 2 \<in> interior ?U"
  1900   proof (rule interiorI)
  1901     let ?I = "(\<Inter>i\<in>Basis. {x::'a. 0 < x \<bullet> i} \<inter> {x. x \<bullet> i < 1})"
  1902     show "open ?I"
  1903       by (intro open_INT finite_Basis ballI open_Int, auto intro: open_Collect_less)
  1904     show "\<Sum>Basis /\<^sub>R 2 \<in> ?I"
  1905       by simp
  1906     show "?I \<subseteq> unit_cube"
  1907       unfolding unit_cube_def by force
  1908   qed
  1909   then have *: "interior ?U \<noteq> {}" by fast
  1910   have *: "?U homeomorphic s"
  1911     using homeomorphic_convex_compact[OF convex_unit_cube compact_unit_cube * assms(2,1,3)] .
  1912   have "\<forall>f. continuous_on ?U f \<and> f ` ?U \<subseteq> ?U \<longrightarrow>
  1913     (\<exists>x\<in>?U. f x = x)"
  1914     using brouwer_cube by auto
  1915   then show ?thesis
  1916     unfolding homeomorphic_fixpoint_property[OF *]
  1917     using assms
  1918     by (auto simp: intro: that)
  1919 qed
  1920 
  1921 
  1922 text \<open>And in particular for a closed ball.\<close>
  1923 
  1924 lemma brouwer_ball:
  1925   fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
  1926   assumes "e > 0"
  1927     and "continuous_on (cball a e) f"
  1928     and "f ` cball a e \<subseteq> cball a e"
  1929   obtains x where "x \<in> cball a e" and "f x = x"
  1930   using brouwer_weak[OF compact_cball convex_cball, of a e f]
  1931   unfolding interior_cball ball_eq_empty
  1932   using assms by auto
  1933 
  1934 text \<open>Still more general form; could derive this directly without using the
  1935   rather involved \<open>HOMEOMORPHIC_CONVEX_COMPACT\<close> theorem, just using
  1936   a scaling and translation to put the set inside the unit cube.\<close>
  1937 
  1938 lemma brouwer:
  1939   fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
  1940   assumes "compact s"
  1941     and "convex s"
  1942     and "s \<noteq> {}"
  1943     and "continuous_on s f"
  1944     and "f ` s \<subseteq> s"
  1945   obtains x where "x \<in> s" and "f x = x"
  1946 proof -
  1947   have "\<exists>e>0. s \<subseteq> cball 0 e"
  1948     using compact_imp_bounded[OF assms(1)]
  1949     unfolding bounded_pos
  1950     apply (erule_tac exE)
  1951     apply (rule_tac x=b in exI)
  1952     apply (auto simp add: dist_norm)
  1953     done
  1954   then obtain e where e: "e > 0" "s \<subseteq> cball 0 e"
  1955     by blast
  1956   have "\<exists>x\<in> cball 0 e. (f \<circ> closest_point s) x = x"
  1957     apply (rule_tac brouwer_ball[OF e(1), of 0 "f \<circ> closest_point s"])
  1958     apply (rule continuous_on_compose )
  1959     apply (rule continuous_on_closest_point[OF assms(2) compact_imp_closed[OF assms(1)] assms(3)])
  1960     apply (rule continuous_on_subset[OF assms(4)])
  1961     apply (insert closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3)])
  1962     using assms(5)[unfolded subset_eq]
  1963     using e(2)[unfolded subset_eq mem_cball]
  1964     apply (auto simp add: dist_norm)
  1965     done
  1966   then obtain x where x: "x \<in> cball 0 e" "(f \<circ> closest_point s) x = x" ..
  1967   have *: "closest_point s x = x"
  1968     apply (rule closest_point_self)
  1969     apply (rule assms(5)[unfolded subset_eq,THEN bspec[where x="x"], unfolded image_iff])
  1970     apply (rule_tac x="closest_point s x" in bexI)
  1971     using x
  1972     unfolding o_def
  1973     using closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3), of x]
  1974     apply auto
  1975     done
  1976   show thesis
  1977     apply (rule_tac x="closest_point s x" in that)
  1978     unfolding x(2)[unfolded o_def]
  1979     apply (rule closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3)])
  1980     using *
  1981     apply auto
  1982     done
  1983 qed
  1984 
  1985 text \<open>So we get the no-retraction theorem.\<close>
  1986 
  1987 lemma no_retraction_cball:
  1988   fixes a :: "'a::euclidean_space"
  1989   assumes "e > 0"
  1990   shows "\<not> (frontier (cball a e) retract_of (cball a e))"
  1991 proof
  1992   assume *: "frontier (cball a e) retract_of (cball a e)"
  1993   have **: "\<And>xa. a - (2 *\<^sub>R a - xa) = - (a - xa)"
  1994     using scaleR_left_distrib[of 1 1 a] by auto
  1995   obtain x where x:
  1996       "x \<in> {x. norm (a - x) = e}"
  1997       "2 *\<^sub>R a - x = x"
  1998     apply (rule retract_fixpoint_property[OF *, of "\<lambda>x. scaleR 2 a - x"])
  1999     apply (blast intro: brouwer_ball[OF assms])
  2000     apply (intro continuous_intros)
  2001     unfolding frontier_cball subset_eq Ball_def image_iff dist_norm
  2002     apply (auto simp add: ** norm_minus_commute)
  2003     done
  2004   then have "scaleR 2 a = scaleR 1 x + scaleR 1 x"
  2005     by (auto simp add: algebra_simps)
  2006   then have "a = x"
  2007     unfolding scaleR_left_distrib[symmetric]
  2008     by auto
  2009   then show False
  2010     using x assms by auto
  2011 qed
  2012 
  2013 end