(*  Author:     John Harrison
    Author:     Robert Himmelmann, TU Muenchen (Translation from HOL light) and LCP
*)

(* At the moment this is just Brouwer's fixpoint theorem. The proof is from  *)
(* Kuhn: "some combinatorial lemmas in topology", IBM J. v4. (1960) p. 518   *)
(* See "http://www.research.ibm.com/journal/rd/045/ibmrd0405K.pdf".          *)
(*                                                                           *)
(* The script below is quite messy, but at least we avoid formalizing any    *)
(* topological machinery; we don't even use barycentric subdivision; this is *)
(* the big advantage of Kuhn's proof over the usual Sperner's lemma one.     *)
(*                                                                           *)
(*              (c) Copyright, John Harrison 1998-2008                       *)

section ‹Brouwer's Fixed Point Theorem›

theory Brouwer_Fixpoint
  imports Homeomorphism Derivative
begin

subsection ‹Retractions›

lemma retract_of_contractible:
  assumes "contractible T" "S retract_of T"
  shows "contractible S"
  using assms
  apply (clarsimp simp add: retract_of_def contractible_def retraction_def homotopic_with image_subset_iff_funcset)
  apply (rule_tac x="r a" in exI)
  apply (rule_tac x="r ∘ h" in exI)
  apply (intro conjI continuous_intros continuous_on_compose)
      apply (erule continuous_on_subset | force)+
  done

lemma retract_of_path_connected:
    "[path_connected T; S retract_of T] ==> path_connected S"
  by (metis path_connected_continuous_image retract_of_def retraction)

lemma retract_of_simply_connected:
  assumes T: "simply_connected T" and "S retract_of T"
  shows "simply_connected S"
proof -
  obtain r where r: "retraction T S r"
    using assms by (metis retract_of_def) 
  have "S ⊆ T"
    by (meson ‹retraction T S r› retraction)
  then have "(λa. a) ∈ S → T"
    by blast
  then show ?thesis
    using simply_connected_retraction_gen [OF T]
    by (metis (no_types) r retraction retraction_refl)
qed

lemma retract_of_homotopically_trivial:
  assumes ts: "T retract_of S"
      and hom: "∧f g. [continuous_on U f; f ∈ U → S;
                       continuous_on U g; g ∈ U → S]
                       ==> homotopic_with_canon (λx. True) U S f g"
      and "continuous_on U f" "f ∈ U → T"
      and "continuous_on U g" "g ∈ U → T"
    shows "homotopic_with_canon (λx. True) U T f g"
proof -
  obtain r where "r ∈ S → S" "continuous_on S r" "∀x∈S. r (r x) = r x" "T = r ` S"
    using ts by (auto simp: retract_of_def retraction)
  then obtain k where "Retracts S r T k"
    unfolding Retracts_def using continuous_on_id by blast
  then show ?thesis
    by (rule Retracts.homotopically_trivial_retraction_gen) (use assms hom in force)+
qed

lemma retract_of_homotopically_trivial_null:
  assumes ts: "T retract_of S"
      and hom: "∧f. [continuous_on U f; f ∈ U → S]
                     ==> ∃c. homotopic_with_canon (λx. True) U S f (λx. c)"
      and "continuous_on U f" "f ∈ U → T"
  obtains c where "homotopic_with_canon (λx. True) U T f (λx. c)"
proof -
  obtain r where "r ∈ S → S" "continuous_on S r" "∀x∈S. r (r x) = r x" "T = r ` S"
    using ts by (auto simp: retract_of_def retraction)
  then obtain k where "Retracts S r T k"
    unfolding Retracts_def by fastforce
  then show ?thesis
  proof (rule Retracts.homotopically_trivial_retraction_null_gen)
    show "∧f. [continuous_on U f; f ∈ U → S]
         ==> ∃c. homotopic_with_canon (λa. True) U S f (λx. c)"
      using hom by blast
  qed (use assms that in auto)
qed

lemma retraction_openin_vimage_iff:
  "openin (top_of_set S) (S ∩ r -` U) ⟷ openin (top_of_set T) U"
  if "retraction S T r" and "U ⊆ T"
  by (simp add: retraction_openin_vimage_iff that)

lemma retract_of_locally_compact:
    fixes S :: "'a :: {heine_borel,real_normed_vector} set"
    shows  "[ locally compact S; T retract_of S] ==> locally compact T"
  by (metis locally_compact_closedin closedin_retract)

lemma homotopic_into_retract:
  assumes fg: "f ∈ S → T" "g ∈ S → T"
  assumes "T retract_of U"
  assumes "homotopic_with_canon (λx. True) S U f g"
  shows "homotopic_with_canon (λx. True) S T f g"
proof -
  obtain h r where r: "retraction U T r"
     "continuous_on ({0..1::real} × S) h"
      and h: "h ∈ {0..1} × S → U ∧ (∀x. h (0, x) = f x) ∧ (∀x. h (1, x) = g x)"
    using assms by (auto simp: homotopic_with_def retract_of_def)
  then have "continuous_on ({0..1} × S) (r ∘ h)"
    by (metis continuous_on_compose continuous_on_subset funcset_image
        retraction_def)
  then show ?thesis
    using r fg h
    apply (simp add: retraction homotopic_with Pi_iff)
    by (smt (verit, best) imageI)
qed

lemma retract_of_locally_connected:
  assumes "locally connected T" "S retract_of T"
  shows "locally connected S"
  using assms
  by (metis retraction_openin_vimage_iff idempotent_imp_retraction locally_connected_quotient_image retract_ofE)

lemma retract_of_locally_path_connected:
  assumes "locally path_connected T" "S retract_of T"
  shows "locally path_connected S"
  using assms
  by (metis retraction_openin_vimage_iff idempotent_imp_retraction locally_path_connected_quotient_image retract_ofE)

text ‹A few simple lemmas about deformation retracts›

lemma deformation_retract_imp_homotopy_eqv:
  fixes S :: "'a::euclidean_space set"
  assumes "homotopic_with_canon (λx. True) S S id r" and r: "retraction S T r"
  shows "S homotopy_eqv T"
proof -
  have "homotopic_with_canon (λx. True) S S (id ∘ r) id"
    by (simp add: assms(1) homotopic_with_symD)
  moreover have "homotopic_with_canon (λx. True) T T (r ∘ id) id"
    using r unfolding retraction_def
    by (metis eq_id_iff homotopic_with_id2 topspace_euclidean_subtopology)
  ultimately
  show ?thesis
    unfolding homotopy_equivalent_space_def
    by (meson continuous_map_from_subtopology_mono continuous_map_id
        continuous_map_subtopology_eu r retraction_def)
qed

lemma deformation_retract:
  fixes S :: "'a::euclidean_space set"
    shows "(∃r. homotopic_with_canon (λx. True) S S id r ∧ retraction S T r) ⟷
           T retract_of S ∧ (∃f. homotopic_with_canon (λx. True) S S id f ∧ f ∈ S → T)"
    (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (auto simp: retract_of_def retraction_def)
next
  assume R: ?rhs
  have "∧r f. [T ⊆ S; continuous_on S r; homotopic_with_canon (λx. True) S S id f;
            f ∈ S → T; r ∈ S → T; ∀x∈T. r x = x]
           ==> homotopic_with_canon (λx. True) S S f r"
    apply (rule_tac f = "r ∘ f" and g="r ∘ id" in homotopic_with_eq)
       apply (rule_tac Y=S in homotopic_with_compose_continuous_left)
         apply (auto simp: homotopic_with_sym Pi_iff)
    done
  with R homotopic_with_trans show ?lhs
    unfolding retract_of_def retraction_def by blast
qed

lemma deformation_retract_of_contractible_sing:
  fixes S :: "'a::euclidean_space set"
  assumes "contractible S" "a ∈ S"
  obtains r where "homotopic_with_canon (λx. True) S S id r" "retraction S {a} r"
proof -
  have "{a} retract_of S"
    by (simp add: ‹a ∈ S›)
  moreover have "homotopic_with_canon (λx. True) S S id (λx. a)"
      using assms
      by (auto simp: contractible_def homotopic_into_contractible image_subset_iff)
  moreover have "(λx. a) ∈ S → {a}"
    by (simp add: image_subsetI)
  ultimately show ?thesis
    by (metis that deformation_retract)
qed


lemma continuous_on_compact_surface_projection_aux:
  fixes S :: "'a::t2_space set"
  assumes "compact S" "S ⊆ T" "image q T ⊆ S"
      and contp: "continuous_on T p"
      and "∧x. x ∈ S ==> q x = x"
      and [simp]: "∧x. x ∈ T ==> q(p x) = q x"
      and "∧x. x ∈ T ==> p(q x) = p x"
    shows "continuous_on T q"
proof -
  have *: "image p T = image p S"
    using assms by auto (metis imageI subset_iff)
  have contp': "continuous_on S p"
    by (rule continuous_on_subset [OF contp ‹S ⊆ T›])
  have "continuous_on (p ` T) q"
    by (simp add: "*" assms(1) assms(2) assms(5) continuous_on_inv contp' rev_subsetD)
  then have "continuous_on T (q ∘ p)"
    by (rule continuous_on_compose [OF contp])
  then show ?thesis
    by (rule continuous_on_eq [of _ "q ∘ p"]) (simp add: o_def)
qed

lemma continuous_on_compact_surface_projection:
  fixes S :: "'a::real_normed_vector set"
  assumes "compact S"
      and S: "S ⊆ V - {0}" and "cone V"
      and iff: "∧x k. x ∈ V - {0} ==> 0 < k ∧ (k *_R x) ∈ S ⟷ d x = k"
  shows "continuous_on (V - {0}) (λx. d x *_R x)"
proof (rule continuous_on_compact_surface_projection_aux [OF ‹compact S› S])
  show "(λx. d x *_R x) ` (V - {0}) ⊆ S"
    using iff by auto
  show "continuous_on (V - {0}) (λx. inverse(norm x) *_R x)"
    by (intro continuous_intros) force
  show "∧x. x ∈ S ==> d x *_R x = x"
    by (metis S zero_less_one local.iff scaleR_one subset_eq)
  show "d (x /_R norm x) *_R (x /_R norm x) = d x *_R x" if "x ∈ V - {0}" for x
    using iff [of "inverse(norm x) *_R x" "norm x * d x", symmetric] iff that ‹cone V›
    by (simp add: field_simps cone_def zero_less_mult_iff)
  show "d x *_R x /_R norm (d x *_R x) = x /_R norm x" if "x ∈ V - {0}" for x
  proof -
    have "0 < d x"
      using local.iff that by blast
    then show ?thesis
      by simp
  qed
qed

subsection ‹Kuhn Simplices›

lemma bij_betw_singleton_eq:
  assumes f: "bij_betw f A B" and g: "bij_betw g A B" and a: "a ∈ A"
  assumes eq: "(∧x. x ∈ A ==> x ≠ a ==> f x = g x)"
  shows "f a = g a"
proof -
  have "f ` (A - {a}) = g ` (A - {a})"
    by (intro image_cong) (simp_all add: eq)
  then have "B - {f a} = B - {g a}"
    using f g a  by (auto simp: bij_betw_def inj_on_image_set_diff set_eq_iff)
  moreover have "f a ∈ B" "g a ∈ B"
    using f g a by (auto simp: bij_betw_def)
  ultimately show ?thesis
    by auto
qed

lemmas swap_apply1 = swap_apply(1)
lemmas swap_apply2 = swap_apply(2)

lemma pointwise_minimal_pointwise_maximal:
  fixes s :: "(nat → nat) set"
  assumes "finite s"
    and "s ≠ {}"
    and "∀x∈s. ∀y∈s. x ≤ y ∨ y ≤ x"
  shows "∃a∈s. ∀x∈s. a ≤ x"
    and "∃a∈s. ∀x∈s. x ≤ a"
  using assms
proof (induct s rule: finite_ne_induct)
  case (insert b s)
  assume *: "∀x∈insert b s. ∀y∈insert b s. x ≤ y ∨ y ≤ x"
  then obtain u l where "l ∈ s" "∀b∈s. l ≤ b" "u ∈ s" "∀b∈s. b ≤ u"
    using insert by auto
  with * show "∃a∈insert b s. ∀x∈insert b s. a ≤ x" "∃a∈insert b s. ∀x∈insert b s. x ≤ a"
    by (metis insert_iff order.trans)+
qed auto

lemma kuhn_labelling_lemma:
  fixes P Q :: "'a::euclidean_space → bool"
  assumes "∀x. P x ⟶ P (f x)"
    and "∀x. P x ⟶ (∀i∈Basis. Q i ⟶ 0 ≤ x∙i ∧ x∙i ≤ 1)"
  shows "∃l. (∀x.∀i∈Basis. l x i ≤ (1::nat)) ∧
             (∀x.∀i∈Basis. P x ∧ Q i ∧ (x∙i = 0) ⟶ (l x i = 0)) ∧
             (∀x.∀i∈Basis. P x ∧ Q i ∧ (x∙i = 1) ⟶ (l x i = 1)) ∧
             (∀x.∀i∈Basis. P x ∧ Q i ∧ (l x i = 0) ⟶ x∙i ≤ f x∙i) ∧
             (∀x.∀i∈Basis. P x ∧ Q i ∧ (l x i = 1) ⟶ f x∙i ≤ x∙i)"
proof -
  { fix x i
    let ?R = "λy. (P x ∧ Q i ∧ x ∙ i = 0 ⟶ y = (0::nat)) ∧
        (P x ∧ Q i ∧ x ∙ i = 1 ⟶ y = 1) ∧
        (P x ∧ Q i ∧ y = 0 ⟶ x ∙ i ≤ f x ∙ i) ∧
        (P x ∧ Q i ∧ y = 1 ⟶ f x ∙ i ≤ x ∙ i)"
    { assume "P x" "Q i" "i ∈ Basis" with assms have "0 ≤ f x ∙ i ∧ f x ∙ i ≤ 1" by auto }
    then have "i ∈ Basis ==> ?R 0 ∨ ?R 1" by auto }
  then show ?thesis
    unfolding all_conj_distrib[symmetric] Ball_def (* FIXME: shouldn't this work by metis? *)
    by (subst choice_iff[symmetric])+ blast
qed


subsubsection ‹The key "counting" observation, somewhat abstracted›

lemma kuhn_counting_lemma:
  fixes bnd compo compo' face S F
  defines "nF s == card {f∈F. face f s ∧ compo' f}"
  assumes [simp, intro]: "finite F" ― ‹faces› and [simp, intro]: "finite S" ― ‹simplices›
    and "∧f. f ∈ F ==> bnd f ==> card {s∈S. face f s} = 1"
    and "∧f. f ∈ F ==> ¬ bnd f ==> card {s∈S. face f s} = 2"
    and "∧s. s ∈ S ==> compo s ==> nF s = 1"
    and "∧s. s ∈ S ==> ¬ compo s ==> nF s = 0 ∨ nF s = 2"
    and "odd (card {f∈F. compo' f ∧ bnd f})"
  shows "odd (card {s∈S. compo s})"
proof -
  have "(∑s | s ∈ S ∧ ¬ compo s. nF s) + (∑s | s ∈ S ∧ compo s. nF s) = (∑s∈S. nF s)"
    by (subst sum.union_disjoint[symmetric]) (auto intro!: sum.cong)
  also have "… = (∑s∈S. card {f ∈ {f∈F. compo' f ∧ bnd f}. face f s}) +
                  (∑s∈S. card {f ∈ {f∈F. compo' f ∧ ¬ bnd f}. face f s})"
    unfolding sum.distrib[symmetric]
    by (subst card_Un_disjoint[symmetric])
       (auto simp: nF_def intro!: sum.cong arg_cong[where f=card])
  also have "… = 1 * card {f∈F. compo' f ∧ bnd f} + 2 * card {f∈F. compo' f ∧ ¬ bnd f}"
    using assms(4,5) by (fastforce intro!: arg_cong2[where f="(+)"] sum_multicount)
  finally have "odd ((∑s | s ∈ S ∧ ¬ compo s. nF s) + card {s∈S. compo s})"
    using assms(6,8) by simp
  moreover have "(∑s | s ∈ S ∧ ¬ compo s. nF s) =
    (∑s | s ∈ S ∧ ¬ compo s ∧ nF s = 0. nF s) + (∑s | s ∈ S ∧ ¬ compo s ∧ nF s = 2. nF s)"
    using assms(7) by (subst sum.union_disjoint[symmetric]) (fastforce intro!: sum.cong)+
  ultimately show ?thesis
    by auto
qed

subsubsection ‹The odd/even result for faces of complete vertices, generalized›

lemma kuhn_complete_lemma:
  assumes [simp]: "finite simplices"
    and face: "∧f s. face f s ⟷ (∃a∈s. f = s - {a})"
    and card_s[simp]:  "∧s. s ∈ simplices ==> card s = n + 2"
    and rl_bd: "∧s. s ∈ simplices ==> rl ` s ⊆ {..Suc n}"
    and bnd: "∧f s. s ∈ simplices ==> face f s ==> bnd f ==> card {s∈simplices. face f s} = 1"
    and nbnd: "∧f s. s ∈ simplices ==> face f s ==> ¬ bnd f ==> card {s∈simplices. face f s} = 2"
    and odd_card: "odd (card {f. (∃s∈simplices. face f s) ∧ rl ` f = {..n} ∧ bnd f})"
  shows "odd (card {s∈simplices. (rl ` s = {..Suc n})})"
proof (rule kuhn_counting_lemma)
  have finite_s[simp]: "∧s. s ∈ simplices ==> finite s"
    by (metis add_is_0 zero_neq_numeral card.infinite assms(3))

  let ?F = "{f. ∃s∈simplices. face f s}"
  have F_eq: "?F = (∪s∈simplices. ∪a∈s. {s - {a}})"
    by (auto simp: face)
  show "finite ?F"
    using ‹finite simplices› unfolding F_eq by auto

  show "card {s ∈ simplices. face f s} = 1" if "f ∈ ?F" "bnd f" for f
    using bnd that by auto

  show "card {s ∈ simplices. face f s} = 2" if "f ∈ ?F" "¬ bnd f" for f
    using nbnd that by auto

  show "odd (card {f ∈ {f. ∃s∈simplices. face f s}. rl ` f = {..n} ∧ bnd f})"
    using odd_card by simp

  fix s assume s[simp]: "s ∈ simplices"
  let ?S = "{f ∈ {f. ∃s∈simplices. face f s}. face f s ∧ rl ` f = {..n}}"
  have "?S = (λa. s - {a}) ` {a∈s. rl ` (s - {a}) = {..n}}"
    using s by (fastforce simp: face)
  then have card_S: "card ?S = card {a∈s. rl ` (s - {a}) = {..n}}"
    by (auto intro!: card_image inj_onI)

  { assume rl: "rl ` s = {..Suc n}"
    then have inj_rl: "inj_on rl s"
      by (intro eq_card_imp_inj_on) auto
    moreover obtain a where "rl a = Suc n" "a ∈ s"
      by (metis atMost_iff image_iff le_Suc_eq rl)
    ultimately have n: "{..n} = rl ` (s - {a})"
      by (auto simp: inj_on_image_set_diff rl)
    have "{a∈s. rl ` (s - {a}) = {..n}} = {a}"
      using inj_rl ‹a ∈ s› by (auto simp: n inj_on_image_eq_iff[OF inj_rl])
    then show "card ?S = 1"
      unfolding card_S by simp }

  { assume rl: "rl ` s ≠ {..Suc n}"
    show "card ?S = 0 ∨ card ?S = 2"
    proof cases
      assume *: "{..n} ⊆ rl ` s"
      with rl rl_bd[OF s] have rl_s: "rl ` s = {..n}"
        by (auto simp: atMost_Suc subset_insert_iff split: if_split_asm)
      then have "¬ inj_on rl s"
        by (intro pigeonhole) simp
      then obtain a b where ab: "a ∈ s" "b ∈ s" "rl a = rl b" "a ≠ b"
        by (auto simp: inj_on_def)
      then have eq: "rl ` (s - {a}) = rl ` s"
        by auto
      with ab have inj: "inj_on rl (s - {a})"
        by (intro eq_card_imp_inj_on) (auto simp: rl_s card_Diff_singleton_if)

      { fix x assume "x ∈ s" "x ∉ {a, b}"
        then have "rl ` s - {rl x} = rl ` ((s - {a}) - {x})"
          by (auto simp: eq inj_on_image_set_diff[OF inj])
        also have "… = rl ` (s - {x})"
          using ab ‹x ∉ {a, b}› by auto
        also assume "… = rl ` s"
        finally have False
          using ‹x∈s› by auto }
      moreover
      { fix x assume "x ∈ {a, b}" with ab have "x ∈ s ∧ rl ` (s - {x}) = rl ` s"
          by (simp add: set_eq_iff image_iff Bex_def) metis }
      ultimately have "{a∈s. rl ` (s - {a}) = {..n}} = {a, b}"
        unfolding rl_s[symmetric] by fastforce
      with ‹a ≠ b› show "card ?S = 0 ∨ card ?S = 2"
        unfolding card_S by simp
    next
      assume "¬ {..n} ⊆ rl ` s"
      then have "∧x. rl ` (s - {x}) ≠ {..n}"
        by auto
      then show "card ?S = 0 ∨ card ?S = 2"
        unfolding card_S by simp
    qed }
qed fact

locale kuhn_simplex =
  fixes p n and base upd and S :: "(nat → nat) set"
  assumes base: "base ∈ {..< n} → {..< p}"
  assumes base_out: "∧i. n ≤ i ==> base i = p"
  assumes upd: "bij_betw upd {..< n} {..< n}"
  assumes s_pre: "S = (λi j. if j ∈ upd`{..< i} then Suc (base j) else base j) ` {.. n}"
begin

definition "enum i j = (if j ∈ upd`{..< i} then Suc (base j) else base j)"

lemma s_eq: "S = enum ` {.. n}"
  unfolding s_pre enum_def[abs_def] ..

lemma upd_space: "i < n ==> upd i < n"
  using upd by (auto dest!: bij_betwE)

lemma s_space: "S ⊆ {..< n} → {.. p}"
proof -
  { fix i assume "i ≤ n" then have "enum i ∈ {..< n} → {.. p}"
    proof (induct i)
      case 0 then show ?case
        using base by (auto simp: Pi_iff less_imp_le enum_def)
    next
      case (Suc i) with base show ?case
        by (auto simp: Pi_iff Suc_le_eq less_imp_le enum_def intro: upd_space)
    qed }
  then show ?thesis
    by (auto simp: s_eq)
qed

lemma inj_upd: "inj_on upd {..< n}"
  using upd by (simp add: bij_betw_def)

lemma inj_enum: "inj_on enum {.. n}"
proof -
  { fix x y :: nat assume "x ≠ y" "x ≤ n" "y ≤ n"
    with upd have "upd ` {..< x} ≠ upd ` {..< y}"
      by (subst inj_on_image_eq_iff[where C="{..< n}"]) (auto simp: bij_betw_def)
    then have "enum x ≠ enum y"
      by (auto simp: enum_def fun_eq_iff) }
  then show ?thesis
    by (auto simp: inj_on_def)
qed

lemma enum_0: "enum 0 = base"
  by (simp add: enum_def[abs_def])

lemma base_in_s: "base ∈ S"
  unfolding s_eq by (subst enum_0[symmetric]) auto

lemma enum_in: "i ≤ n ==> enum i ∈ S"
  unfolding s_eq by auto

lemma one_step:
  assumes a: "a ∈ S" "j < n"
  assumes *: "∧a'. a' ∈ S ==> a' ≠ a ==> a' j = p'"
  shows "a j ≠ p'"
proof
  assume "a j = p'"
  with * a have "∧a'. a' ∈ S ==> a' j = p'"
    by auto
  then have "∧i. i ≤ n ==> enum i j = p'"
    unfolding s_eq by auto
  from this[of 0] this[of n] have "j ∉ upd ` {..< n}"
    by (auto simp: enum_def fun_eq_iff split: if_split_asm)
  with upd ‹j < n› show False
    by (auto simp: bij_betw_def)
qed

lemma upd_inj: "i < n ==> j < n ==> upd i = upd j ⟷ i = j"
  using upd by (auto simp: bij_betw_def inj_on_eq_iff)

lemma upd_surj: "upd ` {..< n} = {..< n}"
  using upd by (auto simp: bij_betw_def)

lemma in_upd_image: "A ⊆ {..< n} ==> i < n ==> upd i ∈ upd ` A ⟷ i ∈ A"
  using inj_on_image_mem_iff[of upd "{..< n}"] upd
  by (auto simp: bij_betw_def)

lemma enum_inj: "i ≤ n ==> j ≤ n ==> enum i = enum j ⟷ i = j"
  using inj_enum by (auto simp: inj_on_eq_iff)

lemma in_enum_image: "A ⊆ {.. n} ==> i ≤ n ==> enum i ∈ enum ` A ⟷ i ∈ A"
  using inj_on_image_mem_iff[OF inj_enum] by auto

lemma enum_mono: "i ≤ n ==> j ≤ n ==> enum i ≤ enum j ⟷ i ≤ j"
  by (auto simp: enum_def le_fun_def in_upd_image Ball_def[symmetric])

lemma enum_strict_mono: "i ≤ n ==> j ≤ n ==> enum i < enum j ⟷ i < j"
  using enum_mono[of i j] enum_inj[of i j] by (auto simp: le_less)

lemma chain: "a ∈ S ==> b ∈ S ==> a ≤ b ∨ b ≤ a"
  by (auto simp: s_eq enum_mono)

lemma less: "a ∈ S ==> b ∈ S ==> a i < b i ==> a < b"
  using chain[of a b] by (auto simp: less_fun_def le_fun_def not_le[symmetric])

lemma enum_0_bot: "a ∈ S ==> a = enum 0 ⟷ (∀a'∈S. a ≤ a')"
  unfolding s_eq by (auto simp: enum_mono Ball_def)

lemma enum_n_top: "a ∈ S ==> a = enum n ⟷ (∀a'∈S. a' ≤ a)"
  unfolding s_eq by (auto simp: enum_mono Ball_def)

lemma enum_Suc: "i < n ==> enum (Suc i) = (enum i)(upd i := Suc (enum i (upd i)))"
  by (auto simp: fun_eq_iff enum_def upd_inj)

lemma enum_eq_p: "i ≤ n ==> n ≤ j ==> enum i j = p"
  by (induct i) (auto simp: enum_Suc enum_0 base_out upd_space not_less[symmetric])

lemma out_eq_p: "a ∈ S ==> n ≤ j ==> a j = p"
  unfolding s_eq by (auto simp: enum_eq_p)

lemma s_le_p: "a ∈ S ==> a j ≤ p"
  using out_eq_p[of a j] s_space by (cases "j < n") auto

lemma le_Suc_base: "a ∈ S ==> a j ≤ Suc (base j)"
  unfolding s_eq by (auto simp: enum_def)

lemma base_le: "a ∈ S ==> base j ≤ a j"
  unfolding s_eq by (auto simp: enum_def)

lemma enum_le_p: "i ≤ n ==> j < n ==> enum i j ≤ p"
  using enum_in[of i] s_space by auto

lemma enum_less: "a ∈ S ==> i < n ==> enum i < a ⟷ enum (Suc i) ≤ a"
  unfolding s_eq by (auto simp: enum_strict_mono enum_mono)

lemma ksimplex_0:
  "n = 0 ==> S = {(λx. p)}"
  using s_eq enum_def base_out by auto

lemma replace_0:
  assumes "j < n" "a ∈ S" and p: "∀x∈S - {a}. x j = 0" and "x ∈ S"
  shows "x ≤ a"
proof cases
  assume "x ≠ a"
  have "a j ≠ 0"
    using assms by (intro one_step[where a=a]) auto
  with less[OF ‹x∈S› ‹a∈S›, of j] p[rule_format, of x] ‹x ∈ S› ‹x ≠ a›
  show ?thesis
    by auto
qed simp

lemma replace_1:
  assumes "j < n" "a ∈ S" and p: "∀x∈S - {a}. x j = p" and "x ∈ S"
  shows "a ≤ x"
proof cases
  assume "x ≠ a"
  have "a j ≠ p"
    using assms by (intro one_step[where a=a]) auto
  with enum_le_p[of _ j] ‹j < n› ‹a∈S›
  have "a j < p"
    by (auto simp: less_le s_eq)
  with less[OF ‹a∈S› ‹x∈S›, of j] p[rule_format, of x] ‹x ∈ S› ‹x ≠ a›
  show ?thesis
    by auto
qed simp

end

locale kuhn_simplex_pair = s: kuhn_simplex p n b_s u_s s + t: kuhn_simplex p n b_t u_t t
  for p n b_s u_s s b_t u_t t
begin

lemma enum_eq:
  assumes l: "i ≤ l" "l ≤ j" and "j + d ≤ n"
  assumes eq: "s.enum ` {i .. j} = t.enum ` {i + d .. j + d}"
  shows "s.enum l = t.enum (l + d)"
using l proof (induct l rule: dec_induct)
  case base
  then have s: "s.enum i ∈ t.enum ` {i + d .. j + d}" and t: "t.enum (i + d) ∈ s.enum ` {i .. j}"
    using eq by auto
  from t ‹i ≤ j› ‹j + d ≤ n› have "s.enum i ≤ t.enum (i + d)"
    by (auto simp: s.enum_mono)
  moreover from s ‹i ≤ j› ‹j + d ≤ n› have "t.enum (i + d) ≤ s.enum i"
    by (auto simp: t.enum_mono)
  ultimately show ?case
    by auto
next
  case (step l)
  moreover from step.prems ‹j + d ≤ n› have
      "s.enum l < s.enum (Suc l)"
      "t.enum (l + d) < t.enum (Suc l + d)"
    by (simp_all add: s.enum_strict_mono t.enum_strict_mono)
  moreover have
      "s.enum (Suc l) ∈ t.enum ` {i + d .. j + d}"
      "t.enum (Suc l + d) ∈ s.enum ` {i .. j}"
    using step ‹j + d ≤ n› eq by (auto simp: s.enum_inj t.enum_inj)
  ultimately have "s.enum (Suc l) = t.enum (Suc (l + d))"
    using ‹j + d ≤ n›
    by (intro antisym s.enum_less[THEN iffD1] t.enum_less[THEN iffD1])
       (auto intro!: s.enum_in t.enum_in)
  then show ?case by simp
qed

lemma ksimplex_eq_bot:
  assumes a: "a ∈ s" "∧a'. a' ∈ s ==> a ≤ a'"
  assumes b: "b ∈ t" "∧b'. b' ∈ t ==> b ≤ b'"
  assumes eq: "s - {a} = t - {b}"
  shows "s = t"
proof cases
  assume "n = 0" with s.ksimplex_0 t.ksimplex_0 show ?thesis by simp
next
  assume "n ≠ 0"
  have "s.enum 0 = (s.enum (Suc 0)) (u_s 0 := s.enum (Suc 0) (u_s 0) - 1)"
       "t.enum 0 = (t.enum (Suc 0)) (u_t 0 := t.enum (Suc 0) (u_t 0) - 1)"
    using ‹n ≠ 0› by (simp_all add: s.enum_Suc t.enum_Suc)
  moreover have e0: "a = s.enum 0" "b = t.enum 0"
    using a b by (simp_all add: s.enum_0_bot t.enum_0_bot)
  moreover
  { fix j assume "0 < j" "j ≤ n"
    moreover have "s - {a} = s.enum ` {Suc 0 .. n}" "t - {b} = t.enum ` {Suc 0 .. n}"
      unfolding s.s_eq t.s_eq e0 by (auto simp: s.enum_inj t.enum_inj)
    ultimately have "s.enum j = t.enum j"
      using enum_eq[of "1" j n 0] eq by auto }
  note enum_eq = this
  then have "s.enum (Suc 0) = t.enum (Suc 0)"
    using ‹n ≠ 0› by auto
  moreover
  { fix j assume "Suc j < n"
    with enum_eq[of "Suc j"] enum_eq[of "Suc (Suc j)"]
    have "u_s (Suc j) = u_t (Suc j)"
      using s.enum_Suc[of "Suc j"] t.enum_Suc[of "Suc j"]
      by (auto simp: fun_eq_iff split: if_split_asm) }
  then have "∧j. 0 < j ==> j < n ==> u_s j = u_t j"
    by (auto simp: gr0_conv_Suc)
  with ‹n ≠ 0› have "u_t 0 = u_s 0"
    by (intro bij_betw_singleton_eq[OF t.upd s.upd, of 0]) auto
  ultimately have "a = b"
    by simp
  with assms show "s = t"
    by auto
qed

lemma ksimplex_eq_top:
  assumes a: "a ∈ s" "∧a'. a' ∈ s ==> a' ≤ a"
  assumes b: "b ∈ t" "∧b'. b' ∈ t ==> b' ≤ b"
  assumes eq: "s - {a} = t - {b}"
  shows "s = t"
proof (cases n)
  assume "n = 0" with s.ksimplex_0 t.ksimplex_0 show ?thesis by simp
next
  case (Suc n')
  have "s.enum n = (s.enum n') (u_s n' := Suc (s.enum n' (u_s n')))"
       "t.enum n = (t.enum n') (u_t n' := Suc (t.enum n' (u_t n')))"
    using Suc by (simp_all add: s.enum_Suc t.enum_Suc)
  moreover have en: "a = s.enum n" "b = t.enum n"
    using a b by (simp_all add: s.enum_n_top t.enum_n_top)
  moreover
  { fix j assume "j < n"
    moreover have "s - {a} = s.enum ` {0 .. n'}" "t - {b} = t.enum ` {0 .. n'}"
      unfolding s.s_eq t.s_eq en by (auto simp: s.enum_inj t.enum_inj Suc)
    ultimately have "s.enum j = t.enum j"
      using enum_eq[of "0" j n' 0] eq Suc by auto }
  note enum_eq = this
  then have "s.enum n' = t.enum n'"
    using Suc by auto
  moreover
  { fix j assume "j < n'"
    with enum_eq[of j] enum_eq[of "Suc j"]
    have "u_s j = u_t j"
      using s.enum_Suc[of j] t.enum_Suc[of j]
      by (auto simp: Suc fun_eq_iff split: if_split_asm) }
  then have "∧j. j < n' ==> u_s j = u_t j"
    by (auto simp: gr0_conv_Suc)
  then have "u_t n' = u_s n'"
    by (intro bij_betw_singleton_eq[OF t.upd s.upd, of n']) (auto simp: Suc)
  ultimately have "a = b"
    by simp
  with assms show "s = t"
    by auto
qed

end

inductive ksimplex for p n :: nat where
  ksimplex: "kuhn_simplex p n base upd s ==> ksimplex p n s"

lemma finite_ksimplexes: "finite {s. ksimplex p n s}"
proof (rule finite_subset)
  { fix a s assume "ksimplex p n s" "a ∈ s"
    then obtain b u where "kuhn_simplex p n b u s" by (auto elim: ksimplex.cases)
    then interpret kuhn_simplex p n b u s .
    from s_space ‹a ∈ s› out_eq_p[OF ‹a ∈ s›]
    have "a ∈ (λf x. if n ≤ x then p else f x) ` ({..< n} →<sub>E</sub> {.. p})"
      by (auto simp: image_iff subset_eq Pi_iff split: if_split_asm
               intro!: bexI[of _ "restrict a {..< n}"]) }
  then show "{s. ksimplex p n s} ⊆ Pow ((λf x. if n ≤ x then p else f x) ` ({..< n} →_E {.. p}))"
    by auto
qed (simp add: finite_PiE)

lemma ksimplex_card:
  assumes "ksimplex p n s" shows "card s = Suc n"
using assms proof cases
  case (ksimplex u b)
  then interpret kuhn_simplex p n u b s .
  show ?thesis
    by (simp add: card_image s_eq inj_enum)
qed

lemma simplex_top_face:
  assumes "0 < p" "∀x∈s'. x n = p"
  shows "ksimplex p n s' ⟷ (∃s a. ksimplex p (Suc n) s ∧ a ∈ s ∧ s' = s - {a})"
  using assms
proof safe
  fix s a assume "ksimplex p (Suc n) s" and a: "a ∈ s" and na: "∀x∈s - {a}. x n = p"
  then show "ksimplex p n (s - {a})"
  proof cases
    case (ksimplex base upd)
    then interpret kuhn_simplex p "Suc n" base upd "s" .

    have "a n < p"
      using one_step[of a n p] na ‹a∈s› s_space by (auto simp: less_le)
    then have "a = enum 0"
      using ‹a ∈ s› na by (subst enum_0_bot) (auto simp: le_less intro!: less[of a _ n])
    then have s_eq: "s - {a} = enum ` Suc ` {.. n}"
      using s_eq by (simp add: atMost_Suc_eq_insert_0 insert_ident in_enum_image subset_eq)
    then have "enum 1 ∈ s - {a}"
      by auto
    then have "upd 0 = n"
      using ‹a n < p› ‹a = enum 0› na[rule_format, of "enum 1"]
      by (auto simp: fun_eq_iff enum_Suc split: if_split_asm)
    then have "bij_betw upd (Suc ` {..< n}) {..< n}"
      using upd
      by (subst notIn_Un_bij_betw3[where b=0])
         (auto simp: lessThan_Suc[symmetric] lessThan_Suc_eq_insert_0)
    then have "bij_betw (upd∘Suc) {..<n} {..<n}"
      by (rule bij_betw_trans[rotated]) (auto simp: bij_betw_def)

    have "a n = p - 1"
      using enum_Suc[of 0] na[rule_format, OF ‹enum 1 ∈ s - {a}›] ‹a = enum 0› by (auto simp: ‹upd 0 = n›)

    show ?thesis
    proof (rule ksimplex.intros, standard)
      show "bij_betw (upd∘Suc) {..< n} {..< n}" by fact
      show "base(n := p) ∈ {..<n} → {..<p}" "∧i. n≤i ==> (base(n := p)) i = p"
        using base base_out by (auto simp: Pi_iff)

      have "∧i. Suc ` {..< i} = {..< Suc i} - {0}"
        by (auto simp: image_iff Ball_def) arith
      then have upd_Suc: "∧i. i ≤ n ==> (upd∘Suc) ` {..< i} = upd ` {..< Suc i} - {n}"
        using ‹upd 0 = n› upd_inj by (auto simp add: image_iff less_Suc_eq_0_disj)
      have n_in_upd: "∧i. n ∈ upd ` {..< Suc i}"
        using ‹upd 0 = n› by auto

      define f' where "f' i j =
        (if j ∈ (upd∘Suc)`{..< i} then Suc ((base(n := p)) j) else (base(n := p)) j)" for i j
      { fix x i
        assume i [arith]: "i ≤ n"
        with upd_Suc have "(upd ∘ Suc) ` {..<i} = upd ` {..<Suc i} - {n}" .
        with ‹a n < p› ‹a = enum 0› ‹upd 0 = n› ‹a n = p - 1›
        have "enum (Suc i) x = f' i x"
          by (auto simp add: f'_def enum_def)  }
      then show "s - {a} = f' ` {.. n}"
        unfolding s_eq image_comp by (intro image_cong) auto
    qed
  qed
next
  assume "ksimplex p n s'" and *: "∀x∈s'. x n = p"
  then show "∃s a. ksimplex p (Suc n) s ∧ a ∈ s ∧ s' = s - {a}"
  proof cases
    case (ksimplex base upd)
    then interpret kuhn_simplex p n base upd s' .
    define b where "b = base (n := p - 1)"
    define u where "u i = (case i of 0 → n | Suc i → upd i)" for i

    have "ksimplex p (Suc n) (s' ∪ {b})"
    proof (rule ksimplex.intros, standard)
      show "b ∈ {..<Suc n} → {..<p}"
        using base ‹0 < p› unfolding lessThan_Suc b_def by (auto simp: PiE_iff)
      show "∧i. Suc n ≤ i ==> b i = p"
        using base_out by (auto simp: b_def)

      have "bij_betw u (Suc ` {..< n} ∪ {0}) ({..<n} ∪ {u 0})"
        using upd
        by (intro notIn_Un_bij_betw) (auto simp: u_def bij_betw_def image_comp comp_def inj_on_def)
      then show "bij_betw u {..<Suc n} {..<Suc n}"
        by (simp add: u_def lessThan_Suc[symmetric] lessThan_Suc_eq_insert_0)

      define f' where "f' i j = (if j ∈ u`{..< i} then Suc (b j) else b j)" for i j

      have u_eq: "∧i. i ≤ n ==> u ` {..< Suc i} = upd ` {..< i} ∪ { n }"
        by (auto simp: u_def image_iff upd_inj Ball_def split: nat.split) arith

      { fix x have "x ≤ n ==> n ∉ upd ` {..<x}"
          using upd_space by (simp add: image_iff neq_iff) }
      note n_not_upd = this

      have *: "f' ` {.. Suc n} = f' ` (Suc ` {.. n} ∪ {0})"
        unfolding atMost_Suc_eq_insert_0 by simp
      also have "… = (f' ∘ Suc) ` {.. n} ∪ {b}"
        by (auto simp: f'_def)
      also have "(f' ∘ Suc) ` {.. n} = s'"
        using ‹0 < p› base_out[of n]
        unfolding s_eq enum_def[abs_def] f'_def[abs_def] upd_space
        by (intro image_cong) (simp_all add: u_eq b_def fun_eq_iff n_not_upd)
      finally show "s' ∪ {b} = f' ` {.. Suc n}" ..
    qed
    moreover have "b ∉ s'"
      using * ‹0 < p› by (auto simp: b_def)
    ultimately show ?thesis by auto
  qed
qed

lemma ksimplex_replace_0:
  assumes s: "ksimplex p n s" and a: "a ∈ s"
  assumes j: "j < n" and p: "∀x∈s - {a}. x j = 0"
  shows "card {s'. ksimplex p n s' ∧ (∃b∈s'. s' - {b} = s - {a})} = 1"
  using s
proof cases
  case (ksimplex b_s u_s)

  { fix t b assume "ksimplex p n t"
    then obtain b_t u_t where "kuhn_simplex p n b_t u_t t"
      by (auto elim: ksimplex.cases)
    interpret kuhn_simplex_pair p n b_s u_s s b_t u_t t
      by intro_locales fact+

    assume b: "b ∈ t" "t - {b} = s - {a}"
    with a j p s.replace_0[of _ a] t.replace_0[of _ b] have "s = t"
      by (intro ksimplex_eq_top[of a b]) auto }
  then have "{s'. ksimplex p n s' ∧ (∃b∈s'. s' - {b} = s - {a})} = {s}"
    using s ‹a ∈ s› by auto
  then show ?thesis
    by simp
qed

lemma ksimplex_replace_1:
  assumes s: "ksimplex p n s" and a: "a ∈ s"
  assumes j: "j < n" and p: "∀x∈s - {a}. x j = p"
  shows "card {s'. ksimplex p n s' ∧ (∃b∈s'. s' - {b} = s - {a})} = 1"
  using s
proof cases
  case (ksimplex b_s u_s)

  { fix t b assume "ksimplex p n t"
    then obtain b_t u_t where "kuhn_simplex p n b_t u_t t"
      by (auto elim: ksimplex.cases)
    interpret kuhn_simplex_pair p n b_s u_s s b_t u_t t
      by intro_locales fact+

    assume b: "b ∈ t" "t - {b} = s - {a}"
    with a j p s.replace_1[of _ a] t.replace_1[of _ b] have "s = t"
      by (intro ksimplex_eq_bot[of a b]) auto }
  then have "{s'. ksimplex p n s' ∧ (∃b∈s'. s' - {b} = s - {a})} = {s}"
    using s ‹a ∈ s› by auto
  then show ?thesis
    by simp
qed

lemma ksimplex_replace_2:
  assumes s: "ksimplex p n s" and "a ∈ s" and "n ≠ 0"
    and lb: "∀j<n. ∃x∈s - {a}. x j ≠ 0"
    and ub: "∀j<n. ∃x∈s - {a}. x j ≠ p"
  shows "card {s'. ksimplex p n s' ∧ (∃b∈s'. s' - {b} = s - {a})} = 2"
  using s
proof cases
  case (ksimplex base upd)
  then interpret kuhn_simplex p n base upd s .

  from ‹a ∈ s› obtain i where "i ≤ n" "a = enum i"
    unfolding s_eq by auto

  from ‹i ≤ n› have "i = 0 ∨ i = n ∨ (0 < i ∧ i < n)"
    by linarith
  then have "∃!s'. s' ≠ s ∧ ksimplex p n s' ∧ (∃b∈s'. s - {a} = s'- {b})"
  proof (elim disjE conjE)
    assume "i = 0"
    define rot where [abs_def]: "rot i = (if i + 1 = n then 0 else i + 1)" for i
    let ?upd = "upd ∘ rot"

    have rot: "bij_betw rot {..< n} {..< n}"
      by (auto simp: bij_betw_def inj_on_def image_iff Ball_def rot_def)
         arith+
    from rot upd have "bij_betw ?upd {..<n} {..<n}"
      by (rule bij_betw_trans)

    define f' where [abs_def]: "f' i j =
      (if j ∈ ?upd`{..< i} then Suc (enum (Suc 0) j) else enum (Suc 0) j)" for i j

    interpret b: kuhn_simplex p n "enum (Suc 0)" "upd ∘ rot" "f' ` {.. n}"
    proof
      from ‹a = enum i› ub ‹n ≠ 0› ‹i = 0›
      obtain i' where "i' ≤ n" "enum i' ≠ enum 0" "enum i' (upd 0) ≠ p"
        unfolding s_eq by (auto intro: upd_space simp: enum_inj)
      then have "enum 1 ≤ enum i'" "enum i' (upd 0) < p"
        using enum_le_p[of i' "upd 0"] by (auto simp: enum_inj enum_mono upd_space)
      then have "enum 1 (upd 0) < p"
        by (auto simp: le_fun_def intro: le_less_trans)
      then show "enum (Suc 0) ∈ {..<n} → {..<p}"
        using base ‹n ≠ 0› by (auto simp: enum_0 enum_Suc PiE_iff extensional_def upd_space)

      { fix i assume "n ≤ i" then show "enum (Suc 0) i = p"
        using ‹n ≠ 0› by (auto simp: enum_eq_p) }
      show "bij_betw ?upd {..<n} {..<n}" by fact
    qed (simp add: f'_def)
    have ks_f': "ksimplex p n (f' ` {.. n})"
      by rule unfold_locales

    have b_enum: "b.enum = f'" unfolding f'_def b.enum_def[abs_def] ..
    with b.inj_enum have inj_f': "inj_on f' {.. n}" by simp

    have f'_eq_enum: "f' j = enum (Suc j)" if "j < n" for j
    proof -
      from that have "rot ` {..< j} = {0 <..< Suc j}"
        by (auto simp: rot_def image_Suc_lessThan cong: image_cong_simp)
      with that ‹n ≠ 0› show ?thesis
        by (simp only: f'_def enum_def fun_eq_iff image_comp [symmetric])
          (auto simp add: upd_inj)
    qed
    then have "enum ` Suc ` {..< n} = f' ` {..< n}"
      by (force simp: enum_inj)
    also have "Suc ` {..< n} = {.. n} - {0}"
      by (auto simp: image_iff Ball_def) arith
    also have "{..< n} = {.. n} - {n}"
      by auto
    finally have eq: "s - {a} = f' ` {.. n} - {f' n}"
      unfolding s_eq ‹a = enum i› ‹i = 0›
      by (simp add: inj_on_image_set_diff[OF inj_enum] inj_on_image_set_diff[OF inj_f'])

    have "enum 0 < f' 0"
      using ‹n ≠ 0› by (simp add: enum_strict_mono f'_eq_enum)
    also have "… < f' n"
      using ‹n ≠ 0› b.enum_strict_mono[of 0 n] unfolding b_enum by simp
    finally have "a ≠ f' n"
      using ‹a = enum i› ‹i = 0› by auto

    { fix t c assume "ksimplex p n t" "c ∈ t" and eq_sma: "s - {a} = t - {c}"
      obtain b u where "kuhn_simplex p n b u t"
        using ‹ksimplex p n t› by (auto elim: ksimplex.cases)
      then interpret t: kuhn_simplex p n b u t .

      { fix x assume "x ∈ s" "x ≠ a"
         then have "x (upd 0) = enum (Suc 0) (upd 0)"
           by (auto simp: ‹a = enum i› ‹i = 0› s_eq enum_def enum_inj) }
      then have eq_upd0: "∀x∈t-{c}. x (upd 0) = enum (Suc 0) (upd 0)"
        unfolding eq_sma[symmetric] by auto
      then have "c (upd 0) ≠ enum (Suc 0) (upd 0)"
        using ‹n ≠ 0› by (intro t.one_step[OF ‹c∈t› ]) (auto simp: upd_space)
      then have "c (upd 0) < enum (Suc 0) (upd 0) ∨ c (upd 0) > enum (Suc 0) (upd 0)"
        by auto
      then have "t = s ∨ t = f' ` {..n}"
      proof (elim disjE conjE)
        assume *: "c (upd 0) < enum (Suc 0) (upd 0)"
        interpret st: kuhn_simplex_pair p n base upd s b u t ..
        { fix x assume "x ∈ t" with * ‹c∈t› eq_upd0[rule_format, of x] have "c ≤ x"
            by (auto simp: le_less intro!: t.less[of _ _ "upd 0"]) }
        note top = this
        have "s = t"
          using ‹a = enum i› ‹i = 0› ‹c ∈ t›
          by (intro st.ksimplex_eq_bot[OF _ _ _ _ eq_sma])
             (auto simp: s_eq enum_mono t.s_eq t.enum_mono top)
        then show ?thesis by simp
      next
        assume *: "c (upd 0) > enum (Suc 0) (upd 0)"
        interpret st: kuhn_simplex_pair p n "enum (Suc 0)" "upd ∘ rot" "f' ` {.. n}" b u t ..
        have eq: "f' ` {..n} - {f' n} = t - {c}"
          using eq_sma eq by simp
        { fix x assume "x ∈ t" with * ‹c∈t› eq_upd0[rule_format, of x] have "x ≤ c"
            by (auto simp: le_less intro!: t.less[of _ _ "upd 0"]) }
        note top = this
        have "f' ` {..n} = t"
          using ‹a = enum i› ‹i = 0› ‹c ∈ t›
          by (intro st.ksimplex_eq_top[OF _ _ _ _ eq])
             (auto simp: b.s_eq b.enum_mono t.s_eq t.enum_mono b_enum[symmetric] top)
        then show ?thesis by simp
      qed }
    with ks_f' eq ‹a ≠ f' n› ‹n ≠ 0› show ?thesis
      apply (intro ex1I[of _ "f' ` {.. n}"])
       apply auto []
      apply metis
      done
  next
    assume "i = n"
    from ‹n ≠ 0› obtain n' where n': "n = Suc n'"
      by (cases n) auto

    define rot where "rot i = (case i of 0 → n' | Suc i → i)" for i
    let ?upd = "upd ∘ rot"

    have rot: "bij_betw rot {..< n} {..< n}"
      by (auto simp: bij_betw_def inj_on_def image_iff Bex_def rot_def n' split: nat.splits)
         arith
    from rot upd have "bij_betw ?upd {..<n} {..<n}"
      by (rule bij_betw_trans)

    define b where "b = base (upd n' := base (upd n') - 1)"
    define f' where [abs_def]: "f' i j = (if j ∈ ?upd`{..< i} then Suc (b j) else b j)" for i j

    interpret b: kuhn_simplex p n b "upd ∘ rot" "f' ` {.. n}"
    proof
      { fix i assume "n ≤ i" then show "b i = p"
          using base_out[of i] upd_space[of n'] by (auto simp: b_def n') }
      show "b ∈ {..<n} → {..<p}"
        using base ‹n ≠ 0› upd_space[of n']
        by (auto simp: b_def PiE_def Pi_iff Ball_def upd_space extensional_def n')

      show "bij_betw ?upd {..<n} {..<n}" by fact
    qed (simp add: f'_def)
    have f': "b.enum = f'" unfolding f'_def b.enum_def[abs_def] ..
    have ks_f': "ksimplex p n (b.enum ` {.. n})"
      unfolding f' by rule unfold_locales

    have "0 < n"
      using ‹n ≠ 0› by auto

    { from ‹a = enum i› ‹n ≠ 0› ‹i = n› lb upd_space[of n']
      obtain i' where "i' ≤ n" "enum i' ≠ enum n" "0 < enum i' (upd n')"
        unfolding s_eq by (auto simp: enum_inj n')
      moreover have "enum i' (upd n') = base (upd n')"
        unfolding enum_def using ‹i' ≤ n› ‹enum i' ≠ enum n› by (auto simp: n' upd_inj enum_inj)
      ultimately have "0 < base (upd n')"
        by auto }
    then have benum1: "b.enum (Suc 0) = base"
      unfolding b.enum_Suc[OF ‹0<n\›] b.enum_0 by (auto simp: b_def rot_def)

    have [simp]: "∧j. Suc j < n ==> rot ` {..< Suc j} = {n'} ∪ {..< j}"
      by (auto simp: rot_def image_iff Ball_def split: nat.splits)
    have rot_simps: "∧j. rot (Suc j) = j" "rot 0 = n'"
      by (simp_all add: rot_def)

    { fix j assume j: "Suc j ≤ n" then have "b.enum (Suc j) = enum j"
        by (induct j) (auto simp: benum1 enum_0 b.enum_Suc enum_Suc rot_simps) }
    note b_enum_eq_enum = this
    then have "enum ` {..< n} = b.enum ` Suc ` {..< n}"
      by (auto simp: image_comp intro!: image_cong)
    also have "Suc ` {..< n} = {.. n} - {0}"
      by (auto simp: image_iff Ball_def) arith
    also have "{..< n} = {.. n} - {n}"
      by auto
    finally have eq: "s - {a} = b.enum ` {.. n} - {b.enum 0}"
      unfolding s_eq ‹a = enum i› ‹i = n›
      using inj_on_image_set_diff[OF inj_enum Diff_subset, of "{n}"]
            inj_on_image_set_diff[OF b.inj_enum Diff_subset, of "{0}"]
      by (simp add: comp_def)

    have "b.enum 0 ≤ b.enum n"
      by (simp add: b.enum_mono)
    also have "b.enum n < enum n"
      using ‹n ≠ 0› by (simp add: enum_strict_mono b_enum_eq_enum n')
    finally have "a ≠ b.enum 0"
      using ‹a = enum i› ‹i = n› by auto

    { fix t c assume "ksimplex p n t" "c ∈ t" and eq_sma: "s - {a} = t - {c}"
      obtain b' u where "kuhn_simplex p n b' u t"
        using ‹ksimplex p n t› by (auto elim: ksimplex.cases)
      then interpret t: kuhn_simplex p n b' u t .

      { fix x assume "x ∈ s" "x ≠ a"
         then have "x (upd n') = enum n' (upd n')"
           by (auto simp: ‹a = enum i› n' ‹i = n› s_eq enum_def enum_inj in_upd_image) }
      then have eq_upd0: "∀x∈t-{c}. x (upd n') = enum n' (upd n')"
        unfolding eq_sma[symmetric] by auto
      then have "c (upd n') ≠ enum n' (upd n')"
        using ‹n ≠ 0› by (intro t.one_step[OF ‹c∈t› ]) (auto simp: n' upd_space[unfolded n'])
      then have "c (upd n') < enum n' (upd n') ∨ c (upd n') > enum n' (upd n')"
        by auto
      then have "t = s ∨ t = b.enum ` {..n}"
      proof (elim disjE conjE)
        assume *: "c (upd n') > enum n' (upd n')"
        interpret st: kuhn_simplex_pair p n base upd s b' u t ..
        { fix x assume "x ∈ t" with * ‹c∈t› eq_upd0[rule_format, of x] have "x ≤ c"
            by (auto simp: le_less intro!: t.less[of _ _ "upd n'"]) }
        note top = this
        have "s = t"
          using ‹a = enum i› ‹i = n› ‹c ∈ t›
          by (intro st.ksimplex_eq_top[OF _ _ _ _ eq_sma])
             (auto simp: s_eq enum_mono t.s_eq t.enum_mono top)
        then show ?thesis by simp
      next
        assume *: "c (upd n') < enum n' (upd n')"
        interpret st: kuhn_simplex_pair p n b "upd ∘ rot" "f' ` {.. n}" b' u t ..
        have eq: "f' ` {..n} - {b.enum 0} = t - {c}"
          using eq_sma eq f' by simp
        { fix x assume "x ∈ t" with * ‹c∈t› eq_upd0[rule_format, of x] have "c ≤ x"
            by (auto simp: le_less intro!: t.less[of _ _ "upd n'"]) }
        note bot = this
        have "f' ` {..n} = t"
          using ‹a = enum i› ‹i = n› ‹c ∈ t›
          by (intro st.ksimplex_eq_bot[OF _ _ _ _ eq])
             (auto simp: b.s_eq b.enum_mono t.s_eq t.enum_mono bot)
        with f' show ?thesis by simp
      qed }
    with ks_f' eq ‹a ≠ b.enum 0› ‹n ≠ 0› show ?thesis
      apply (intro ex1I[of _ "b.enum ` {.. n}"])
      apply fastforce
      apply metis
      done
  next
    assume i: "0 < i" "i < n"
    define i' where "i' = i - 1"
    with i have "Suc i' < n"
      by simp
    with i have Suc_i': "Suc i' = i"
      by (simp add: i'_def)

    let ?upd = "Fun.swap i' i upd"
    from i upd have "bij_betw ?upd {..< n} {..< n}"
      by (subst bij_betw_swap_iff) (auto simp: i'_def)

    define f' where [abs_def]: "f' i j = (if j ∈ ?upd`{..< i} then Suc (base j) else base j)"
      for i j
    interpret b: kuhn_simplex p n base ?upd "f' ` {.. n}"
    proof
      show "base ∈ {..<n} → {..<p}" by (rule base)
      { fix i assume "n ≤ i" then show "base i = p" by (rule base_out) }
      show "bij_betw ?upd {..<n} {..<n}" by fact
    qed (simp add: f'_def)
    have f': "b.enum = f'" unfolding f'_def b.enum_def[abs_def] ..
    have ks_f': "ksimplex p n (b.enum ` {.. n})"
      unfolding f' by rule unfold_locales

    have "{i} ⊆ {..n}"
      using i by auto
    { fix j assume "j ≤ n"
      with i Suc_i' have "enum j = b.enum j ⟷ j ≠ i"
        unfolding fun_eq_iff enum_def b.enum_def image_comp [symmetric]
        apply (cases ‹i = j›)
         apply (metis imageI in_upd_image lessI lessThan_iff lessThan_subset_iff order_less_le transpose_apply_first)
        by (metis lessThan_iff linorder_not_less not_less_eq_eq order_less_le transpose_image_eq)
      }
    note enum_eq_benum = this
    then have "enum ` ({.. n} - {i}) = b.enum ` ({.. n} - {i})"
      by (intro image_cong) auto
    then have eq: "s - {a} = b.enum ` {.. n} - {b.enum i}"
      unfolding s_eq ‹a = enum i›
      using inj_on_image_set_diff[OF inj_enum Diff_subset ‹{i} ⊆ {..n}›]
            inj_on_image_set_diff[OF b.inj_enum Diff_subset ‹{i} ⊆ {..n}›]
      by (simp add: comp_def)

    have "a ≠ b.enum i"
      using ‹a = enum i› enum_eq_benum i by auto

    { fix t c assume "ksimplex p n t" "c ∈ t" and eq_sma: "s - {a} = t - {c}"
      obtain b' u where "kuhn_simplex p n b' u t"
        using ‹ksimplex p n t› by (auto elim: ksimplex.cases)
      then interpret t: kuhn_simplex p n b' u t .
      have "enum i' ∈ s - {a}" "enum (i + 1) ∈ s - {a}"
        using ‹a = enum i› i enum_in by (auto simp: enum_inj i'_def)
      then obtain l k where
        l: "t.enum l = enum i'" "l ≤ n" "t.enum l ≠ c" and
        k: "t.enum k = enum (i + 1)" "k ≤ n" "t.enum k ≠ c"
        unfolding eq_sma by (auto simp: t.s_eq)
      with i have "t.enum l < t.enum k"
        by (simp add: enum_strict_mono i'_def)
      with ‹l ≤ n› ‹k ≤ n› have "l < k"
        by (simp add: t.enum_strict_mono)
      { assume "Suc l = k"
        have "enum (Suc (Suc i')) = t.enum (Suc l)"
          using i by (simp add: k ‹Suc l = k› i'_def)
        then have False
          using ‹l < k› ‹k ≤ n› ‹Suc i' < n›
          by (auto simp: t.enum_Suc enum_Suc l upd_inj fun_eq_iff split: if_split_asm)
             (metis Suc_lessD n_not_Suc_n upd_inj) }
      with ‹l < k› have "Suc l < k"
        by arith
      have c_eq: "c = t.enum (Suc l)"
      proof (rule ccontr)
        assume "c ≠ t.enum (Suc l)"
        then have "t.enum (Suc l) ∈ s - {a}"
          using ‹l < k› ‹k ≤ n› by (simp add: t.s_eq eq_sma)
        then obtain j where "t.enum (Suc l) = enum j" "j ≤ n" "enum j ≠ enum i"
          unfolding s_eq ‹a = enum i› by auto
        with i have "t.enum (Suc l) ≤ t.enum l ∨ t.enum k ≤ t.enum (Suc l)"
          by (auto simp: i'_def enum_mono enum_inj l k)
        with ‹Suc l < k› ‹k ≤ n› show False
          by (simp add: t.enum_mono)
      qed

      { have "t.enum (Suc (Suc l)) ∈ s - {a}"
          unfolding eq_sma c_eq t.s_eq using ‹Suc l < k› ‹k ≤ n› by (auto simp: t.enum_inj)
        then obtain j where eq: "t.enum (Suc (Suc l)) = enum j" and "j ≤ n" "j ≠ i"
          by (auto simp: s_eq ‹a = enum i›)
        moreover have "enum i' < t.enum (Suc (Suc l))"
          unfolding l(1)[symmetric] using ‹Suc l < k› ‹k ≤ n› by (auto simp: t.enum_strict_mono)
        ultimately have "i' < j"
          using i by (simp add: enum_strict_mono i'_def)
        with ‹j ≠ i› ‹j ≤ n› have "t.enum k ≤ t.enum (Suc (Suc l))"
          unfolding i'_def by (simp add: enum_mono k eq)
        then have "k ≤ Suc (Suc l)"
          using ‹k ≤ n› ‹Suc l < k› by (simp add: t.enum_mono) }
      with ‹Suc l < k› have "Suc (Suc l) = k" by simp
      then have "enum (Suc (Suc i')) = t.enum (Suc (Suc l))"
        using i by (simp add: k i'_def)
      also have "… = (enum i') (u l := Suc (enum i' (u l)), u (Suc l) := Suc (enum i' (u (Suc l))))"
        using ‹Suc l < k› ‹k ≤ n› by (simp add: t.enum_Suc l t.upd_inj)
      finally have "(u l = upd i' ∧ u (Suc l) = upd (Suc i')) ∨
        (u l = upd (Suc i') ∧ u (Suc l) = upd i')"
        using ‹Suc i' < n› by (auto simp: enum_Suc fun_eq_iff split: if_split_asm)

      then have "t = s ∨ t = b.enum ` {..n}"
      proof (elim disjE conjE)
        assume u: "u l = upd i'"
        have "c = t.enum (Suc l)" unfolding c_eq ..
        also have "t.enum (Suc l) = enum (Suc i')"
          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)
        also have "\<dots> = a"
          using \<open>a = enum i\<close> i by (simp add: i'_def)
        finally show ?thesis
          using eq_sma \<open>a \<in> s\<close> \<open>c \<in> t\<close> by auto
      next
        assume u: "u l = upd (Suc i')"
        define B where "B = b.enum ` {..n}"
        have "b.enum i' = enum i'"
          using enum_eq_benum[of i'] i by (auto simp: i'_def gr0_conv_Suc)
        have "c = t.enum (Suc l)" unfolding c_eq ..
        also have "t.enum (Suc l) = b.enum (Suc i')"
          using u \<open>l < k\<close> \<open>k \<le> n\<close> \<open>Suc i' < n\<close>
          by (simp_all add: enum_Suc t.enum_Suc l b.enum_Suc \<open>b.enum i' = enum i'\<close>)
             (simp add: Suc_i')
        also have "\<dots> = b.enum i"
          using i by (simp add: i'_def)
        finally have "c = b.enum i" .
        then have "t - {c} = B - {c}" "c \<in> B"
          unfolding eq_sma[symmetric] eq B_def using i by auto
        with \<open>c \<in> t\<close> have "t = B"
          by auto
        then show ?thesis
          by (simp add: B_def)
      qed }
    with ks_f' eq \<open>a \<noteq> b.enum i\<close> \<open>n \<noteq> 0\<close> \<open>i \<le> n\<close> show ?thesis
      apply (intro ex1I[of _ "b.enum ` {.. n}"])
      apply auto []
      apply metis
      done
  qed
  then show ?thesis
    using s \<open>a \<in> s\<close> by (simp add: card_2_iff' Ex1_def) metis
qed

text \<open>Hence another step towards concreteness.\<close>

lemma kuhn_simplex_lemma:
  assumes "\<forall>s. ksimplex p (Suc n) s \<longrightarrow> rl ` s \<subseteq> {.. Suc n}"
    and "odd (card {f. \<exists>s a. ksimplex p (Suc n) s \<and> a \<in> s \<and> (f = s - {a}) \<and>
      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))})"
  shows "odd (card {s. ksimplex p (Suc n) s \<and> rl ` s = {..Suc n}})"
proof (rule kuhn_complete_lemma[OF finite_ksimplexes refl, unfolded mem_Collect_eq,
    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)"],
    safe del: notI)

  have *: "\<And>x y. x = y \<Longrightarrow> odd (card x) \<Longrightarrow> odd (card y)"
    by auto
  show "odd (card {f. (\<exists>s\<in>{s. ksimplex p (Suc n) s}. \<exists>a\<in>s. f = s - {a}) \<and>
    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))})"
    apply (rule *[OF _ assms(2)])
    apply (auto simp: atLeast0AtMost)
    done

next

  fix s assume s: "ksimplex p (Suc n) s"
  then show "card s = n + 2"
    by (simp add: ksimplex_card)

  fix a assume a: "a \<in> s" then show "rl a \<le> Suc n"
    using assms(1) s by (auto simp: subset_eq)

  let ?S = "{t. ksimplex p (Suc n) t \<and> (\<exists>b\<in>t. s - {a} = t - {b})}"
  { fix j assume j: "j \<le> n" "\<forall>x\<in>s - {a}. x j = 0"
    with s a show "card ?S = 1"
      using ksimplex_replace_0[of p "n + 1" s a j]
      by (subst eq_commute) simp }

  { fix j assume j: "j \<le> n" "\<forall>x\<in>s - {a}. x j = p"
    with s a show "card ?S = 1"
      using ksimplex_replace_1[of p "n + 1" s a j]
      by (subst eq_commute) simp }

  { assume "card ?S \<noteq> 2" "\<not> (\<exists>j\<in>{..n}. \<forall>x\<in>s - {a}. x j = p)"
    with s a show "\<exists>j\<in>{..n}. \<forall>x\<in>s - {a}. x j = 0"
      using ksimplex_replace_2[of p "n + 1" s a]
      by (subst (asm) eq_commute) auto }
qed

subsubsection \<open>Reduced labelling\<close>

definition reduced :: "nat \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> nat" where "reduced n x = (LEAST k. k = n \<or> x k \<noteq> 0)"

lemma reduced_labelling:
  shows "reduced n x \<le> n"
    and "\<forall>i<reduced n x. x i = 0"
    and "reduced n x = n \<or> x (reduced n x) \<noteq> 0"
proof -
  show "reduced n x \<le> n"
    unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) auto
  show "\<forall>i<reduced n x. x i = 0"
    unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) fastforce+
  show "reduced n x = n \<or> x (reduced n x) \<noteq> 0"
    unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) fastforce+
qed

lemma reduced_labelling_unique:
  "r \<le> n \<Longrightarrow> \<forall>i<r. x i = 0 \<Longrightarrow> r = n \<or> x r \<noteq> 0 \<Longrightarrow> reduced n x = r"
  by (metis linorder_less_linear linorder_not_le reduced_labelling)

lemma reduced_labelling_zero: "j < n \<Longrightarrow> x j = 0 \<Longrightarrow> reduced n x \<noteq> j"
  using reduced_labelling[of n x] by auto

lemma reduce_labelling_zero[simp]: "reduced 0 x = 0"
  by (rule reduced_labelling_unique) auto

lemma reduced_labelling_nonzero: "j < n \<Longrightarrow> x j \<noteq> 0 \<Longrightarrow> reduced n x \<le> j"
  using reduced_labelling[of n x] by (elim allE[where x=j]) auto

lemma reduced_labelling_Suc: "reduced (Suc n) x \<noteq> Suc n \<Longrightarrow> reduced (Suc n) x = reduced n x"
  using reduced_labelling[of "Suc n" x]
  by (intro reduced_labelling_unique[symmetric]) auto

lemma complete_face_top:
  assumes "\<forall>x\<in>f. \<forall>j\<le>n. x j = 0 \<longrightarrow> lab x j = 0"
    and "\<forall>x\<in>f. \<forall>j\<le>n. x j = p \<longrightarrow> lab x j = 1"
    and eq: "(reduced (Suc n) \<circ> lab) ` f = {..n}"
  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)"
proof (safe del: disjCI)
  fix x j assume j: "j \<le> n" "\<forall>x\<in>f. x j = 0"
  { fix x assume "x \<in> f" with assms j have "reduced (Suc n) (lab x) \<noteq> j"
      by (intro reduced_labelling_zero) auto }
  moreover have "j \<in> (reduced (Suc n) \<circ> lab) ` f"
    using j eq by auto
  ultimately show "x n = p"
    by force
next
  fix x j assume j: "j \<le> n" "\<forall>x\<in>f. x j = p" and x: "x \<in> f"
  have "j = n"
  proof (rule ccontr)
    assume "\<not> ?thesis"
    { fix x assume "x \<in> f"
      with assms j have "reduced (Suc n) (lab x) \<le> j"
        by (intro reduced_labelling_nonzero) auto
      then have "reduced (Suc n) (lab x) \<noteq> n"
        using \<open>j \<noteq> n\<close> \<open>j \<le> n\<close> by simp }
    moreover
    have "n \<in> (reduced (Suc n) \<circ> lab) ` f"
      using eq by auto
    ultimately show False
      by force
  qed
  moreover have "j \<in> (reduced (Suc n) \<circ> lab) ` f"
    using j eq by auto
  ultimately show "x n = p"
    using j x by auto
qed auto

text \<open>Hence we get just about the nice induction.\<close>

lemma kuhn_induction:
  assumes "0 < p"
    and lab_0: "\<forall>x. \<forall>j\<le>n. (\<forall>j. x j \<le> p) \<and> x j = 0 \<longrightarrow> lab x j = 0"
    and lab_1: "\<forall>x. \<forall>j\<le>n. (\<forall>j. x j \<le> p) \<and> x j = p \<longrightarrow> lab x j = 1"
    and odd: "odd (card {s. ksimplex p n s \<and> (reduced n\<circ>lab) ` s = {..n}})"
  shows "odd (card {s. ksimplex p (Suc n) s \<and> (reduced (Suc n)\<circ>lab) ` s = {..Suc n}})"
proof -
  let ?rl = "reduced (Suc n) \<circ> lab" and ?ext = "\<lambda>f v. \<exists>j\<le>n. \<forall>x\<in>f. x j = v"
  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)"
  have "\<forall>s. ksimplex p (Suc n) s \<longrightarrow> ?rl ` s \<subseteq> {..Suc n}"
    by (simp add: reduced_labelling subset_eq)
  moreover
  have "{s. ksimplex p n s \<and> (reduced n \<circ> lab) ` s = {..n}} =
        {f. \<exists>s a. ksimplex p (Suc n) s \<and> a \<in> s \<and> f = s - {a} \<and> ?rl ` f = {..n} \<and> ?ext f}"
  proof (intro set_eqI, safe del: disjCI equalityI disjE)
    fix s assume s: "ksimplex p n s" and rl: "(reduced n \<circ> lab) ` s = {..n}"
    from s obtain u b where "kuhn_simplex p n u b s" by (auto elim: ksimplex.cases)
    then interpret kuhn_simplex p n u b s .
    have all_eq_p: "\<forall>x\<in>s. x n = p"
      by (auto simp: out_eq_p)
    moreover
    { fix x assume "x \<in> s"
      with lab_1[rule_format, of n x] all_eq_p s_le_p[of x] 
      have "?rl x \<le> n"
        by (auto intro!: reduced_labelling_nonzero)
      then have "?rl x = reduced n (lab x)"
        by (auto intro!: reduced_labelling_Suc) }
    then have "?rl ` s = {..n}"
      using rl by (simp cong: image_cong)
    moreover
    obtain t a where "ksimplex p (Suc n) t" "a \<in> t" "s = t - {a}"
      using s unfolding simplex_top_face[OF \<open>0 < p\<close> all_eq_p] by auto
    ultimately
    show "\<exists>t a. ksimplex p (Suc n) t \<and> a \<in> t \<and> s = t - {a} \<and> ?rl ` s = {..n} \<and> ?ext s"
      by auto
  next
    fix x s a assume s: "ksimplex p (Suc n) s" and rl: "?rl ` (s - {a}) = {.. n}"
      and a: "a \<in> s" and "?ext (s - {a})"
    from s obtain u b where "kuhn_simplex p (Suc n) u b s" by (auto elim: ksimplex.cases)
    then interpret kuhn_simplex p "Suc n" u b s .
    have all_eq_p: "\<forall>x\<in>s. x (Suc n) = p"
      by (auto simp: out_eq_p)

    { fix x assume "x \<in> s - {a}"
      then have "?rl x \<in> ?rl ` (s - {a})"
        by auto
      then have "?rl x \<le> n"
        unfolding rl by auto
      then have "?rl x = reduced n (lab x)"
        by (auto intro!: reduced_labelling_Suc) }
    then show rl': "(reduced n\<circ>lab) ` (s - {a}) = {..n}"
      unfolding rl[symmetric] by (intro image_cong) auto

    from \<open>?ext (s - {a})\<close>
    have all_eq_p: "\<forall>x\<in>s - {a}. x n = p"
    proof (elim disjE exE conjE)
      fix j assume "j \<le> n" "\<forall>x\<in>s - {a}. x j = 0"
      with lab_0[rule_format, of j] all_eq_p s_le_p
      have "\<And>x. x \<in> s - {a} \<Longrightarrow> reduced (Suc n) (lab x) \<noteq> j"
        by (intro reduced_labelling_zero) auto
      moreover have "j \<in> ?rl ` (s - {a})"
        using \<open>j \<le> n\<close> unfolding rl by auto
      ultimately show ?thesis
        by force
    next
      fix j assume "j \<le> n" and eq_p: "\<forall>x\<in>s - {a}. x j = p"
      show ?thesis
      proof cases
        assume "j = n" with eq_p show ?thesis by simp
      next
        assume "j \<noteq> n"
        { fix x assume x: "x \<in> s - {a}"
          have "reduced n (lab x) \<le> j"
          proof (rule reduced_labelling_nonzero)
            show "lab x j \<noteq> 0"
              using lab_1[rule_format, of j x] x s_le_p[of x] eq_p \<open>j \<le> n\<close> by auto
            show "j < n"
              using \<open>j \<le> n\<close> \<open>j \<noteq> n\<close> by simp
          qed
          then have "reduced n (lab x) \<noteq> n"
            using \<open>j \<le> n\<close> \<open>j \<noteq> n\<close> by simp }
        moreover have "n \<in> (reduced n\<circ>lab) ` (s - {a})"
          unfolding rl' by auto
        ultimately show ?thesis
          by force
      qed
    qed
    show "ksimplex p n (s - {a})"
      unfolding simplex_top_face[OF \<open>0 < p\<close> all_eq_p] using s a by auto
  qed
  ultimately show ?thesis
    using assms by (intro kuhn_simplex_lemma) auto
qed

text \<open>And so we get the final combinatorial result.\<close>

lemma ksimplex_0: "ksimplex p 0 s \<longleftrightarrow> s = {(\<lambda>x. p)}"
proof
  assume "ksimplex p 0 s" then show "s = {(\<lambda>x. p)}"
    by (blast dest: kuhn_simplex.ksimplex_0 elim: ksimplex.cases)
next
  assume s: "s = {(\<lambda>x. p)}"
  show "ksimplex p 0 s"
  proof (intro ksimplex, unfold_locales)
    show "(\<lambda>_. p) \<in> {..<0::nat} \<rightarrow> {..<p}" by auto
    show "bij_betw id {..<0} {..<0}"
      by simp
  qed (auto simp: s)
qed

lemma kuhn_combinatorial:
  assumes "0 < p"
    and "\<forall>x j. (\<forall>j. x j \<le> p) \<and> j < n \<and> x j = 0 \<longrightarrow> lab x j = 0"
    and "\<forall>x j. (\<forall>j. x j \<le> p) \<and> j < n  \<and> x j = p \<longrightarrow> lab x j = 1"
  shows "odd (card {s. ksimplex p n s \<and> (reduced n\<circ>lab) ` s = {..n}})"
    (is "odd (card (?M n))")
  using assms
proof (induct n)
  case 0 then show ?case
    by (simp add: ksimplex_0 cong: conj_cong)
next
  case (Suc n)
  then have "odd (card (?M n))"
    by force
  with Suc show ?case
    using kuhn_induction[of p n] by (auto simp: comp_def)
qed

lemma kuhn_lemma:
  fixes n p :: nat
  assumes "0 < p"
    and "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. label x i = (0::nat) \<or> label x i = 1)"
    and "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = 0 \<longrightarrow> label x i = 0)"
    and "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = p \<longrightarrow> label x i = 1)"
  obtains q where "\<forall>i<n. q i < p"
    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"
proof -
  let ?rl = "reduced n \<circ> label"
  let ?A = "{s. ksimplex p n s \<and> ?rl ` s = {..n}}"
  have "odd (card ?A)"
    using assms by (intro kuhn_combinatorial[of p n label]) auto
  then have "?A \<noteq> {}"
    by (rule odd_card_imp_not_empty)
  then obtain s b u where "kuhn_simplex p n b u s" and rl: "?rl ` s = {..n}"
    by (auto elim: ksimplex.cases)
  interpret kuhn_simplex p n b u s by fact

  show ?thesis
  proof (intro that[of b] allI impI)
    fix i
    assume "i < n"
    then show "b i < p"
      using base by auto
  next
    fix i
    assume "i < n"
    then have "i \<in> {.. n}" "Suc i \<in> {.. n}"
      by auto
    then obtain u v where u: "u \<in> s" "Suc i = ?rl u" and v: "v \<in> s" "i = ?rl v"
      unfolding rl[symmetric] by blast

    have "label u i \<noteq> label v i"
      using reduced_labelling [of n "label u"] reduced_labelling [of n "label v"]
        u(2)[symmetric] v(2)[symmetric] \<open>i < n\<close>
      by auto
    moreover
    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
      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>]
      by auto
    ultimately show "\<exists>r s. (\<forall>j<n. b j \<le> r j \<and> r j \<le> b j + 1) \<and>
        (\<forall>j<n. b j \<le> s j \<and> s j \<le> b j + 1) \<and> label r i \<noteq> label s i"
      by blast
  qed
qed

subsubsection \<open>Main result for the unit cube\<close>

lemma kuhn_labelling_lemma':
  assumes "(\<forall>x::nat\<Rightarrow>real. P x \<longrightarrow> P (f x))"
    and "\<forall>x. P x \<longrightarrow> (\<forall>i::nat. Q i \<longrightarrow> 0 \<le> x i \<and> x i \<le> 1)"
  shows "\<exists>l. (\<forall>x i. l x i \<le> (1::nat)) \<and>
             (\<forall>x i. P x \<and> Q i \<and> x i = 0 \<longrightarrow> l x i = 0) \<and>
             (\<forall>x i. P x \<and> Q i \<and> x i = 1 \<longrightarrow> l x i = 1) \<and>
             (\<forall>x i. P x \<and> Q i \<and> l x i = 0 \<longrightarrow> x i \<le> f x i) \<and>
             (\<forall>x i. P x \<and> Q i \<and> l x i = 1 \<longrightarrow> f x i \<le> x i)"
  unfolding all_conj_distrib [symmetric] 
  apply (subst choice_iff[symmetric])+
  by (metis assms choice_iff bot_nat_0.extremum nle_le zero_neq_one)

subsection \<open>Brouwer's fixed point theorem\<close>

text \<open>We start proving Brouwer's fixed point theorem for the unit cube = \<open>cbox 0 One\<close>.\<close>

lemma brouwer_cube:
  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
  assumes "continuous_on (cbox 0 One) f"
    and "f ` cbox 0 One \<subseteq> cbox 0 One"
  shows "\<exists>x\<in>cbox 0 One. f x = x"
proof (rule ccontr)
  define n where "n = DIM('a)"
  have n: "1 \<le> n" "0 < n" "n \<noteq> 0"
    unfolding n_def by (auto simp: Suc_le_eq)
  assume "\<not> ?thesis"
  then have *: "\<not> (\<exists>x\<in>cbox 0 One. f x - x = 0)"
    by auto
  obtain d where
      d: "d > 0" "\<And>x. x \<in> cbox 0 One \<Longrightarrow> d \<le> norm (f x - x)"
    using brouwer_compactness_lemma[OF compact_cbox _ *] assms
    by (metis (no_types, lifting) continuous_on_cong continuous_on_diff continuous_on_id)
  have *: "\<forall>x. x \<in> cbox 0 One \<longrightarrow> f x \<in> cbox 0 One"
    "\<forall>x. x \<in> (cbox 0 One::'a set) \<longrightarrow> (\<forall>i\<in>Basis. True \<longrightarrow> 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1)"
    using assms(2)[unfolded image_subset_iff Ball_def]
    unfolding cbox_def
    by auto
  obtain label :: "'a \<Rightarrow> 'a \<Rightarrow> nat" where label [rule_format]:
    "\<forall>x. \<forall>i\<in>Basis. label x i \<le> 1"
    "\<forall>x. \<forall>i\<in>Basis. x \<in> cbox 0 One \<and> x \<bullet> i = 0 \<longrightarrow> label x i = 0"
    "\<forall>x. \<forall>i\<in>Basis. x \<in> cbox 0 One \<and> x \<bullet> i = 1 \<longrightarrow> label x i = 1"
    "\<forall>x. \<forall>i\<in>Basis. x \<in> cbox 0 One \<and> label x i = 0 \<longrightarrow> x \<bullet> i \<le> f x \<bullet> i"
    "\<forall>x. \<forall>i\<in>Basis. x \<in> cbox 0 One \<and> label x i = 1 \<longrightarrow> f x \<bullet> i \<le> x \<bullet> i"
    using kuhn_labelling_lemma[OF *] by auto
  note label = this [rule_format]
  have lem1: "\<forall>x\<in>cbox 0 One. \<forall>y\<in>cbox 0 One. \<forall>i\<in>Basis. label x i \<noteq> label y i \<longrightarrow>
    \<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y - f x) + norm (y - x)"
  proof safe
    fix x y :: 'a
    assume x: "x \<in> cbox 0 One" and y: "y \<in> cbox 0 One"
    fix i
    assume i: "label x i \<noteq> label y i" "i \<in> Basis"
    have *: "\<And>x y fx fy :: real. x \<le> fx \<and> fy \<le> y \<or> fx \<le> x \<and> y \<le> fy \<Longrightarrow>
      \<bar>fx - x\<bar> \<le> \<bar>fy - fx\<bar> + \<bar>y - x\<bar>" by auto
    have "\<bar>(f x - x) \<bullet> i\<bar> \<le> \<bar>(f y - f x)\<bullet>i\<bar> + \<bar>(y - x)\<bullet>i\<bar>"
    proof (cases "label x i = 0")
      case True
      then have fxy: "\<not> f y \<bullet> i \<le> y \<bullet> i \<Longrightarrow> f x \<bullet> i \<le> x \<bullet> i"
        by (metis True i label(1) label(5) le_antisym less_one not_le_imp_less y)
      show ?thesis
      unfolding inner_simps         
      by (rule *) (auto simp: True i label x y fxy)
    next
      case False
      then show ?thesis
        using label [OF \<open>i \<in> Basis\<close>] i(1) x y
        by (smt (verit, ccfv_threshold) inner_diff_left less_one order_le_less)
    qed
    also have "\<dots> \<le> norm (f y - f x) + norm (y - x)"
      by (simp add: add_mono i(2) norm_bound_Basis_le)
    finally show "\<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y - f x) + norm (y - x)"
      unfolding inner_simps .
  qed
  have "\<exists>e>0. \<forall>x\<in>cbox 0 One. \<forall>y\<in>cbox 0 One. \<forall>z\<in>cbox 0 One. \<forall>i\<in>Basis.
    norm (x - z) < e \<longrightarrow> norm (y - z) < e \<longrightarrow> label x i \<noteq> label y i \<longrightarrow>
      \<bar>(f(z) - z)\<bullet>i\<bar> < d / (real n)"
  proof -
    have d': "d / real n / 8 > 0"
      using d(1) by (simp add: n_def)
    have *: "uniformly_continuous_on (cbox 0 One) f"
      by (rule compact_uniformly_continuous[OF assms(1) compact_cbox])
    obtain e where e:
        "e > 0"
        "\<And>x x'. x \<in> cbox 0 One \<Longrightarrow>
          x' \<in> cbox 0 One \<Longrightarrow>
          norm (x' - x) < e \<Longrightarrow>
          norm (f x' - f x) < d / real n / 8"
      using *[unfolded uniformly_continuous_on_def,rule_format,OF d']
      unfolding dist_norm
      by blast
    show ?thesis
    proof (intro exI conjI ballI impI)
      show "0 < min (e / 2) (d / real n / 8)"
        using d' e by auto
      fix x y z i
      assume as:
        "x \<in> cbox 0 One" "y \<in> cbox 0 One" "z \<in> cbox 0 One"
        "norm (x - z) < min (e / 2) (d / real n / 8)"
        "norm (y - z) < min (e / 2) (d / real n / 8)"
        "label x i \<noteq> label y i"
      assume i: "i \<in> Basis"
      have *: "\<And>z fz x fx n1 n2 n3 n4 d4 d :: real. \<bar>fx - x\<bar> \<le> n1 + n2 \<Longrightarrow>
        \<bar>fx - fz\<bar> \<le> n3 \<Longrightarrow> \<bar>x - z\<bar> \<le> n4 \<Longrightarrow>
        n1 < d4 \<Longrightarrow> n2 < 2 * d4 \<Longrightarrow> n3 < d4 \<Longrightarrow> n4 < d4 \<Longrightarrow>
        (8 * d4 = d) \<Longrightarrow> \<bar>fz - z\<bar> < d"
        by auto
      show "\<bar>(f z - z) \<bullet> i\<bar> < d / real n"
        unfolding inner_simps
      proof (rule *)
        show "\<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y -f x) + norm (y - x)"
          using as(1) as(2) as(6) i lem1 by blast
        show "norm (f x - f z) < d / real n / 8"
          using d' e as by auto
        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)"
          unfolding inner_diff_left[symmetric]
          by (rule Basis_le_norm[OF i])+
        have tria: "norm (y - x) \<le> norm (y - z) + norm (x - z)"
          using dist_triangle[of y x z, unfolded dist_norm]
          unfolding norm_minus_commute
          by auto
        also have "\<dots> < e / 2 + e / 2"
          using as(4) as(5) by auto
        finally show "norm (f y - f x) < d / real n / 8"
          using as(1) as(2) e(2) by auto
        have "norm (y - z) + norm (x - z) < d / real n / 8 + d / real n / 8"
          using as(4) as(5) by auto
        with tria show "norm (y - x) < 2 * (d / real n / 8)"
          by auto
      qed (use as in auto)
    qed
  qed
  then
  obtain e where e:
    "e > 0"
    "\<And>x y z i. x \<in> cbox 0 One \<Longrightarrow>
      y \<in> cbox 0 One \<Longrightarrow>
      z \<in> cbox 0 One \<Longrightarrow>
      i \<in> Basis \<Longrightarrow>
      norm (x - z) < e \<and> norm (y - z) < e \<and> label x i \<noteq> label y i \<Longrightarrow>
      \<bar>(f z - z) \<bullet> i\<bar> < d / real n"
    by blast
  obtain p :: nat where p: "1 + real n / e \<le> real p"
    using real_arch_simple ..
  have "1 + real n / e > 0"
    using e(1) n by (simp add: add_pos_pos)
  then have "p > 0"
    using p by auto

  obtain b :: "nat \<Rightarrow> 'a" where b: "bij_betw b {..< n} Basis"
    by atomize_elim (auto simp: n_def intro!: finite_same_card_bij)
  define b' where "b' = inv_into {..< n} b"
  then have b': "bij_betw b' Basis {..< n}"
    using bij_betw_inv_into[OF b] by auto
  then have b'_Basis: "\<And>i. i \<in> Basis \<Longrightarrow> b' i \<in> {..< n}"
    unfolding bij_betw_def by (auto simp: set_eq_iff)
  have bb'[simp]:"\<And>i. i \<in> Basis \<Longrightarrow> b (b' i) = i"
    unfolding b'_def
    using b
    by (auto simp: f_inv_into_f bij_betw_def)
  have b'b[simp]:"\<And>i. i < n \<Longrightarrow> b' (b i) = i"
    unfolding b'_def
    using b
    by (auto simp: inv_into_f_eq bij_betw_def)
  have *: "\<And>x :: nat. x = 0 \<or> x = 1 \<longleftrightarrow> x \<le> 1"
    by auto
  have b'': "\<And>j. j < n \<Longrightarrow> b j \<in> Basis"
    using b unfolding bij_betw_def by auto
  have q1: "0 < p" "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow>
    (\<forall>i<n. (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0 \<or>
           (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 1)"
    unfolding *
    using \<open>p > 0\<close> \<open>n > 0\<close>
    using label(1)[OF b'']
    by auto
  { fix x :: "nat \<Rightarrow> nat" and i assume "\<forall>i<n. x i \<le> p" "i < n" "x i = p \<or> x i = 0"
    then have "(\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<in> (cbox 0 One::'a set)"
      using b'_Basis
      by (auto simp: cbox_def bij_betw_def zero_le_divide_iff divide_le_eq_1) }
  note cube = this
  have q2: "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = 0 \<longrightarrow>
      (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0)"
    unfolding o_def using cube \<open>p > 0\<close> by (intro allI impI label(2)) (auto simp: b'')
  have q3: "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = p \<longrightarrow>
      (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 1)"
    using cube \<open>p > 0\<close> unfolding o_def by (intro allI impI label(3)) (auto simp: b'')
  obtain q where q:
      "\<forall>i<n. q i < p"
      "\<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 (\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i) \<circ> b) i \<noteq>
               (label (\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i) \<circ> b) i"
    by (rule kuhn_lemma[OF q1 q2 q3])
  define z :: 'a where "z = (\<Sum>i\<in>Basis. (real (q (b' i)) / real p) *\<^sub>R i)"
  have "\<exists>i\<in>Basis. d / real n \<le> \<bar>(f z - z)\<bullet>i\<bar>"
  proof (rule ccontr)
    have "\<forall>i\<in>Basis. q (b' i) \<in> {0..p}"
      using q(1) b'
      by (auto intro: less_imp_le simp: bij_betw_def)
    then have "z \<in> cbox 0 One"
      unfolding z_def cbox_def
      using b'_Basis
      by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1)
    then have d_fz_z: "d \<le> norm (f z - z)"
      by (rule d)
    assume "\<not> ?thesis"
    then have as: "\<forall>i\<in>Basis. \<bar>f z \<bullet> i - z \<bullet> i\<bar> < d / real n"
      using \<open>n > 0\<close>
      by (auto simp: not_le inner_diff)
    have "norm (f z - z) \<le> (\<Sum>i\<in>Basis. \<bar>f z \<bullet> i - z \<bullet> i\<bar>)"
      unfolding inner_diff_left[symmetric]
      by (rule norm_le_l1)
    also have "\<dots> < (\<Sum>(i::'a) \<in> Basis. d / real n)"
      by (meson as finite_Basis nonempty_Basis sum_strict_mono)
    also have "\<dots> = d"
      using DIM_positive[where 'a='a] by (auto simp: n_def)
    finally show False
      using d_fz_z by auto
  qed
  then obtain i where i: "i \<in> Basis" "d / real n \<le> \<bar>(f z - z) \<bullet> i\<bar>" ..
  have *: "b' i < n"
    using i and b'[unfolded bij_betw_def]
    by auto
  obtain r s where rs:
    "\<And>j. j < n \<Longrightarrow> q j \<le> r j \<and> r j \<le> q j + 1"
    "\<And>j. j < n \<Longrightarrow> q j \<le> s j \<and> s j \<le> q j + 1"
    "(label (\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i) \<circ> b) (b' i) \<noteq>
      (label (\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i) \<circ> b) (b' i)"
    using q(2)[rule_format,OF *] by blast
  have b'_im: "\<And>i. i \<in> Basis \<Longrightarrow>  b' i < n"
    using b' unfolding bij_betw_def by auto
  define r' ::'a where "r' = (\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i)"
  have "\<And>i. i \<in> Basis \<Longrightarrow> r (b' i) \<le> p"
    using b'_im q(1) rs(1) by fastforce
  then have "r' \<in> cbox 0 One"
    unfolding r'_def cbox_def
    using b'_Basis
    by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1)
  define s' :: 'a where "s' = (\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i)"
  have "\<And>i. i \<in> Basis \<Longrightarrow> s (b' i) \<le> p"
    using b'_im q(1) rs(2) by fastforce
  then have "s' \<in> cbox 0 One"
    unfolding s'_def cbox_def
    using b'_Basis by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1)
  have "z \<in> cbox 0 One"
    unfolding z_def cbox_def
    using b'_Basis q(1)[rule_format,OF b'_im] \<open>p > 0\<close>
    by (auto simp: bij_betw_def zero_le_divide_iff divide_le_eq_1 less_imp_le)
  {
    have "(\<Sum>i\<in>Basis. \<bar>real (r (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
      by (rule sum_mono) (use rs(1)[OF b'_im] in force)
    also have "\<dots> < e * real p"
      using p \<open>e > 0\<close> \<open>p > 0\<close>
      by (auto simp: field_simps n_def)
    finally have "(\<Sum>i\<in>Basis. \<bar>real (r (b' i)) - real (q (b' i))\<bar>) < e * real p" .
  }
  moreover
  {
    have "(\<Sum>i\<in>Basis. \<bar>real (s (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
      by (rule sum_mono) (use rs(2)[OF b'_im] in force)
    also have "\<dots> < e * real p"
      using p \<open>e > 0\<close> \<open>p > 0\<close>
      by (auto simp: field_simps n_def)
    finally have "(\<Sum>i\<in>Basis. \<bar>real (s (b' i)) - real (q (b' i))\<bar>) < e * real p" .
  }
  ultimately
  have "norm (r' - z) < e" and "norm (s' - z) < e"
    unfolding r'_def s'_def z_def
    using \<open>p > 0\<close>
    apply (rule_tac[!] le_less_trans[OF norm_le_l1])
    apply (auto simp: field_simps sum_divide_distrib[symmetric] inner_diff_left)
    done
  then have "\<bar>(f z - z) \<bullet> i\<bar> < d / real n"
    using rs(3) i
    unfolding r'_def[symmetric] s'_def[symmetric] o_def bb'
    by (intro e(2)[OF \<open>r'\<in>cbox 0 One\<close> \<open>s'\<in>cbox 0 One\<close> \<open>z\<in>cbox 0 One\<close>]) auto
  then show False
    using i by auto
qed

text \<open>Next step is to prove it for nonempty interiors.\<close>

lemma brouwer_weak:
  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
  assumes "compact S"
    and "convex S"
    and "interior S \<noteq> {}"
    and "continuous_on S f"
    and "f \<in> S \<rightarrow> S"
  obtains x where "x \<in> S" and "f x = x"
proof -
  let ?U = "cbox 0 One :: 'a set"
  have "\<Sum>Basis /\<^sub>R 2 \<in> interior ?U"
  proof (rule interiorI)
    let ?I = "(\<Inter>i\<in>Basis. {x::'a. 0 < x \<bullet> i} \<inter> {x. x \<bullet> i < 1})"
    show "open ?I"
      by (intro open_INT finite_Basis ballI open_Int, auto intro: open_Collect_less simp: continuous_on_inner)
    show "\<Sum>Basis /\<^sub>R 2 \<in> ?I"
      by simp
    show "?I \<subseteq> cbox 0 One"
      unfolding cbox_def by force
  qed
  then have *: "interior ?U \<noteq> {}" by fast
  have *: "?U homeomorphic S"
    using homeomorphic_convex_compact[OF convex_box(1) compact_cbox * assms(2,1,3)] .
  have "\<forall>f. continuous_on ?U f \<and> f \<in> ?U \<rightarrow> ?U \<longrightarrow> (\<exists>x\<in>?U. f x = x)"
    using brouwer_cube by auto
  then show ?thesis
    unfolding homeomorphic_fixpoint_property[OF *]
    using assms
    by (auto intro: that)
qed

text \<open>Then the particular case for closed balls.\<close>

lemma brouwer_ball:
  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
  assumes "e > 0"
    and "continuous_on (cball a e) f"
    and "f \<in> cball a e \<rightarrow> cball a e"
  obtains x where "x \<in> cball a e" and "f x = x"
  using brouwer_weak[OF compact_cball convex_cball, of a e f]
  unfolding interior_cball ball_eq_empty
  using assms by auto

text \<open>And finally we prove Brouwer's fixed point theorem in its general version.\<close>

theorem brouwer:
  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
  assumes S: "compact S" "convex S" "S \<noteq> {}"
    and contf: "continuous_on S f"
    and fim: "f \<in> S \<rightarrow> S"
  obtains x where "x \<in> S" and "f x = x"
proof -
  have "\<exists>e>0. S \<subseteq> cball 0 e"
    using compact_imp_bounded[OF \<open>compact S\<close>]  unfolding bounded_pos
    by auto
  then obtain e where e: "e > 0" "S \<subseteq> cball 0 e"
    by blast
  have "\<exists>x\<in> cball 0 e. (f \<circ> closest_point S) x = x"
  proof (rule_tac brouwer_ball[OF e(1)])
    show "continuous_on (cball 0 e) (f \<circ> closest_point S)"
      by (meson assms closest_point_in_set compact_eq_bounded_closed contf continuous_on_closest_point
          continuous_on_compose continuous_on_subset image_subsetI)
    show "f \<circ> closest_point S \<in> cball 0 e \<rightarrow> cball 0 e"
      by (smt (verit) Pi_iff assms(1) assms(3) closest_point_in_set comp_apply compact_eq_bounded_closed e(2) fim subset_eq)
  qed (use assms in auto)
  then obtain x where x: "x \<in> cball 0 e" "(f \<circ> closest_point S) x = x" ..
  with S have "x \<in> S"
    by (metis PiE closest_point_in_set comp_apply compact_imp_closed fim)
  then have *: "closest_point S x = x"
    by (rule closest_point_self)
  show thesis
  proof
    show "closest_point S x \<in> S"
      by (simp add: "*" \<open>x \<in> S\<close>)
    show "f (closest_point S x) = closest_point S x"
      using "*" x by auto
  qed
qed

subsection \<open>Applications\<close>

text \<open>So we get the no-retraction theorem.\<close>

corollary no_retraction_cball:
  fixes a :: "'a::euclidean_space"
  assumes "e > 0"
  shows "\<not> (frontier (cball a e) retract_of (cball a e))"
proof
  assume *: "frontier (cball a e) retract_of (cball a e)"
  have **: "\<And>xa. a - (2 *\<^sub>R a - xa) = - (a - xa)"
    using scaleR_left_distrib[of 1 1 a] by auto
  obtain x where x: "x \<in> {x. norm (a - x) = e}" "2 *\<^sub>R a - x = x"
  proof (rule retract_fixpoint_property[OF *, of "\<lambda>x. scaleR 2 a - x"])
    show "continuous_on (frontier (cball a e)) ((-) (2 *\<^sub>R a))"
      by (intro continuous_intros)
    show "(-) (2 *\<^sub>R a) \<in> frontier (cball a e) \<rightarrow> frontier (cball a e)"
      by clarsimp (metis "**" dist_norm norm_minus_cancel)
  qed (auto simp: dist_norm intro: brouwer_ball[OF assms])
  then have "scaleR 2 a = scaleR 1 x + scaleR 1 x"
    by (auto simp: algebra_simps)
  then have "a = x"
    unfolding scaleR_left_distrib[symmetric] by auto
  then show False
    using x assms by auto
qed

corollary contractible_sphere:
  fixes a :: "'a::euclidean_space"
  shows "contractible(sphere a r) \<longleftrightarrow> r \<le> 0"
proof (cases "0 < r")
  case True
  then show ?thesis
    unfolding contractible_def nullhomotopic_from_sphere_extension
    using no_retraction_cball [OF True, of a]
    by (auto simp: retract_of_def retraction_def)
next
  case False
  then show ?thesis
    unfolding contractible_def nullhomotopic_from_sphere_extension
    using less_eq_real_def by auto
qed

corollary connected_sphere_eq:
  fixes a :: "'a :: euclidean_space"
  shows "connected(sphere a r) \<longleftrightarrow> 2 \<le> DIM('a) \<or> r \<le> 0"
    (is "?lhs = ?rhs")
proof (cases r "0::real" rule: linorder_cases)
  case less
  then show ?thesis by auto
next
  case equal
  then show ?thesis by auto
next
  case greater
  show ?thesis
  proof
    assume L: ?lhs
    have "False" if 1: "DIM('a) = 1"
    proof -
      obtain x y where xy: "sphere a r = {x,y}" "x \<noteq> y"
        using sphere_1D_doubleton [OF 1 greater]
        by (metis dist_self greater insertI1 less_add_same_cancel1 mem_sphere mult_2 not_le zero_le_dist)
      then have "finite (sphere a r)"
        by auto
      with L \<open>r > 0\<close> xy show "False"
        using connected_finite_iff_sing by auto
    qed
    with greater show ?rhs
      by (metis DIM_ge_Suc0 One_nat_def Suc_1 le_antisym not_less_eq_eq)
  next
    assume ?rhs
    then show ?lhs
      using connected_sphere greater by auto
  qed
qed

corollary path_connected_sphere_eq:
  fixes a :: "'a :: euclidean_space"
  shows "path_connected(sphere a r) \<longleftrightarrow> 2 \<le> DIM('a) \<or> r \<le> 0"
         (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    using connected_sphere_eq path_connected_imp_connected by blast
next
  assume R: ?rhs
  then show ?lhs
    by (auto simp: contractible_imp_path_connected contractible_sphere path_connected_sphere)
qed

proposition frontier_subset_retraction:
  fixes S :: "'a::euclidean_space set"
  assumes "bounded S" and fros: "frontier S \<subseteq> T"
      and contf: "continuous_on (closure S) f"
      and fim: "f \<in> S \<rightarrow> T"
      and fid: "\<And>x. x \<in> T \<Longrightarrow> f x = x"
    shows "S \<subseteq> T"
proof (rule ccontr)
  assume "\<not> S \<subseteq> T"
  then obtain a where "a \<in> S" "a \<notin> T" by blast
  define g where "g \<equiv> \<lambda>z. if z \<in> closure S then f z else z"
  have "continuous_on (closure S \<union> closure(-S)) g"
    unfolding g_def using fros fid frontier_closures
    by (intro continuous_on_cases) (auto simp: contf)
  moreover have "closure S \<union> closure(- S) = UNIV"
    using closure_Un by fastforce
  ultimately have contg: "continuous_on UNIV g" by metis
  obtain B where "0 < B" and B: "closure S \<subseteq> ball a B"
    using \<open>bounded S\<close> bounded_subset_ballD by blast
  have notga: "g x \<noteq> a" for x
    unfolding g_def using fros fim \<open>a \<notin> T\<close>
    by (metis PiE Un_iff \<open>a \<in> S\<close> closure_Un_frontier fid subsetD)
  define h where "h \<equiv> (\<lambda>y. a + (B / norm(y - a)) *\<^sub>R (y - a)) \<circ> g"
  have "\<not> (frontier (cball a B) retract_of (cball a B))"
    by (metis no_retraction_cball \<open>0 < B\<close>)
  then have "\<And>k. \<not> retraction (cball a B) (frontier (cball a B)) k"
    by (simp add: retract_of_def)
  moreover have "retraction (cball a B) (frontier (cball a B)) h"
    unfolding retraction_def
  proof (intro conjI ballI)
    show "frontier (cball a B) \<subseteq> cball a B"
      by force
    show "continuous_on (cball a B) h"
      unfolding h_def
      by (intro continuous_intros) (use contg continuous_on_subset notga in auto)
    show "h \<in> cball a B \<rightarrow> frontier (cball a B)"
      using \<open>0 < B\<close> by (auto simp: h_def notga dist_norm)
    show "\<And>x. x \<in> frontier (cball a B) \<Longrightarrow> h x = x"
      using notga \<open>0 < B\<close>
      apply (simp add: g_def h_def field_simps)
      by (metis B dist_commute dist_norm mem_ball order_less_irrefl subset_eq)
  qed
  ultimately show False by simp
qed

subsubsection \<open>Punctured affine hulls, etc\<close>

lemma rel_frontier_deformation_retract_of_punctured_convex:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" "convex T" "bounded S"
      and arelS: "a \<in> rel_interior S"
      and relS: "rel_frontier S \<subseteq> T"
      and affS: "T \<subseteq> affine hull S"
  obtains r where "homotopic_with_canon (\<lambda>x. True) (T - {a}) (T - {a}) id r"
                  "retraction (T - {a}) (rel_frontier S) r"
proof -
  have "\<exists>d. 0 < d \<and> (a + d *\<^sub>R l) \<in> rel_frontier S \<and>
            (\<forall>e. 0 \<le> e \<and> e < d \<longrightarrow> (a + e *\<^sub>R l) \<in> rel_interior S)"
    if "(a + l) \<in> affine hull S" "l \<noteq> 0" for l
    using ray_to_rel_frontier [OF \<open>bounded S\<close> arelS] that by metis
  then obtain dd
    where dd1: "\<And>l. \<lbrakk>(a + l) \<in> affine hull S; l \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < dd l \<and> (a + dd l *\<^sub>R l) \<in> rel_frontier S"
      and dd2: "\<And>l e. \<lbrakk>(a + l) \<in> affine hull S; e < dd l; 0 \<le> e; l \<noteq> 0\<rbrakk>
                      \<Longrightarrow> (a + e *\<^sub>R l) \<in> rel_interior S"
    by metis+
  have aaffS: "a \<in> affine hull S"
    by (meson arelS subsetD hull_inc rel_interior_subset)
  have "((\<lambda>z. z - a) ` (affine hull S - {a})) = ((\<lambda>z. z - a) ` (affine hull S)) - {0}"
    by auto
  moreover have "continuous_on (((\<lambda>z. z - a) ` (affine hull S)) - {0}) (\<lambda>x. dd x *\<^sub>R x)"
  proof (rule continuous_on_compact_surface_projection)
    show "compact (rel_frontier ((\<lambda>z. z - a) ` S))"
      by (simp add: \<open>bounded S\<close> bounded_translation_minus compact_rel_frontier_bounded)
    have releq: "rel_frontier ((\<lambda>z. z - a) ` S) = (\<lambda>z. z - a) ` rel_frontier S"
      using rel_frontier_translation [of "-a"] add.commute by simp
    also have "\<dots> \<subseteq> (\<lambda>z. z - a) ` (affine hull S) - {0}"
      using rel_frontier_affine_hull arelS rel_frontier_def by fastforce
    finally show "rel_frontier ((\<lambda>z. z - a) ` S) \<subseteq> (\<lambda>z. z - a) ` (affine hull S) - {0}" .
    show "cone ((\<lambda>z. z - a) ` (affine hull S))"
      by (rule subspace_imp_cone)
         (use aaffS in \<open>simp add: subspace_affine image_comp o_def affine_translation_aux [of a]\<close>)
    show "(0 < k \<and> k *\<^sub>R x \<in> rel_frontier ((\<lambda>z. z - a) ` S)) \<longleftrightarrow> (dd x = k)"
         if x: "x \<in> (\<lambda>z. z - a) ` (affine hull S) - {0}" for k x
    proof
      show "dd x = k \<Longrightarrow> 0 < k \<and> k *\<^sub>R x \<in> rel_frontier ((\<lambda>z. z - a) ` S)"
      using dd1 [of x] that image_iff by (fastforce simp add: releq)
    next
      assume k: "0 < k \<and> k *\<^sub>R x \<in> rel_frontier ((\<lambda>z. z - a) ` S)"
      have False if "dd x < k"
      proof -
        have "k \<noteq> 0" "a + k *\<^sub>R x \<in> closure S"
          using k closure_translation [of "-a"]
          by (auto simp: rel_frontier_def cong: image_cong_simp)
        then have segsub: "open_segment a (a + k *\<^sub>R x) \<subseteq> rel_interior S"
          by (metis rel_interior_closure_convex_segment [OF \<open>convex S\<close> arelS])
        have "x \<noteq> 0" and xaffS: "a + x \<in> affine hull S"
          using x by auto
        then have "0 < dd x" and inS: "a + dd x *\<^sub>R x \<in> rel_frontier S"
          using dd1 by auto
        moreover have "a + dd x *\<^sub>R x \<in> open_segment a (a + k *\<^sub>R x)"
          unfolding in_segment
        proof (intro conjI exI)
          show "a + dd x *\<^sub>R x = (1 - dd x / k) *\<^sub>R a + (dd x / k) *\<^sub>R (a + k *\<^sub>R x)"
            using k by (simp add: that algebra_simps)
        qed (use \<open>x \<noteq> 0\<close> \<open>0 < dd x\<close> that in auto)
        ultimately show ?thesis
          using segsub by (auto simp: rel_frontier_def)
      qed
      moreover have False if "k < dd x"
        using x k that rel_frontier_def
        by (fastforce simp: algebra_simps releq dest!: dd2)
      ultimately show "dd x = k"
        by fastforce
    qed
  qed
  ultimately have *: "continuous_on ((\<lambda>z. z - a) ` (affine hull S - {a})) (\<lambda>x. dd x *\<^sub>R x)"
    by auto
  have "continuous_on (affine hull S - {a}) ((\<lambda>x. a + dd x *\<^sub>R x) \<circ> (\<lambda>z. z - a))"
    by (intro * continuous_intros continuous_on_compose)
  with affS have contdd: "continuous_on (T - {a}) ((\<lambda>x. a + dd x *\<^sub>R x) \<circ> (\<lambda>z. z - a))"
    by (blast intro: continuous_on_subset)
  show ?thesis
  proof
    show "homotopic_with_canon (\<lambda>x. True) (T - {a}) (T - {a}) id (\<lambda>x. a + dd (x-a) *\<^sub>R (x-a))"
    proof (rule homotopic_with_linear)
      show "continuous_on (T - {a}) id"
        by (intro continuous_intros continuous_on_compose)
      show "continuous_on (T - {a}) (\<lambda>x. a + dd (x-a) *\<^sub>R (x-a))"
        using contdd by (simp add: o_def)
      show "closed_segment (id x) (a + dd (x-a) *\<^sub>R (x-a)) \<subseteq> T - {a}"
           if "x \<in> T - {a}" for x
      proof (clarsimp simp: in_segment, intro conjI)
        fix u::real assume u: "0 \<le> u" "u \<le> 1"
        have "a + dd (x-a) *\<^sub>R (x-a) \<in> T"
          by (metis DiffD1 DiffD2 add.commute add.right_neutral affS dd1 diff_add_cancel relS singletonI subsetCE that)
        then show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x-a) *\<^sub>R (x-a)) \<in> T"
          using convexD [OF \<open>convex T\<close>] that u by simp
        have iff: "(1 - u) *\<^sub>R x + u *\<^sub>R (a + d *\<^sub>R (x-a)) = a \<longleftrightarrow>
                  (1 - u + u * d) *\<^sub>R (x-a) = 0" for d
          by (auto simp: algebra_simps)
        have "x \<in> T" "x \<noteq> a" using that by auto
        then have axa: "a + (x-a) \<in> affine hull S"
           by (metis (no_types) add.commute affS diff_add_cancel rev_subsetD)
        then have "\<not> dd (x-a) \<le> 0 \<and> a + dd (x-a) *\<^sub>R (x-a) \<in> rel_frontier S"
          using \<open>x \<noteq> a\<close> dd1 by fastforce
        with \<open>x \<noteq> a\<close> show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x-a) *\<^sub>R (x-a)) \<noteq> a"
          using less_eq_real_def mult_le_0_iff not_less u by (fastforce simp: iff)
      qed
    qed
    show "retraction (T - {a}) (rel_frontier S) (\<lambda>x. a + dd (x-a) *\<^sub>R (x-a))"
    proof (simp add: retraction_def, intro conjI ballI)
      show "rel_frontier S \<subseteq> T - {a}"
        using arelS relS rel_frontier_def by fastforce
      show "continuous_on (T - {a}) (\<lambda>x. a + dd (x-a) *\<^sub>R (x-a))"
        using contdd by (simp add: o_def)
      show "(\<lambda>x. a + dd (x-a) *\<^sub>R (x-a)) \<in> (T - {a}) \<rightarrow> rel_frontier S"
        unfolding Pi_iff using affS dd1 subset_eq by force
      show "a + dd (x-a) *\<^sub>R (x-a) = x" if x: "x \<in> rel_frontier S" for x
      proof -
        have "x \<noteq> a"
          using that arelS by (auto simp: rel_frontier_def)
        have False if "dd (x-a) < 1"
        proof -
          have "x \<in> closure S"
            using x by (auto simp: rel_frontier_def)
          then have segsub: "open_segment a x \<subseteq> rel_interior S"
            by (metis rel_interior_closure_convex_segment [OF \<open>convex S\<close> arelS])
          have  xaffS: "x \<in> affine hull S"
            using affS relS x by auto
          then have "0 < dd (x-a)" and inS: "a + dd (x-a) *\<^sub>R (x-a) \<in> rel_frontier S"
            using dd1 by (auto simp: \<open>x \<noteq> a\<close>)
          moreover have "a + dd (x-a) *\<^sub>R (x-a) \<in> open_segment a x"
            unfolding in_segment
          proof (intro exI conjI)
            show "a + dd (x-a) *\<^sub>R (x-a) = (1 - dd (x-a)) *\<^sub>R a + (dd (x-a)) *\<^sub>R x"
              by (simp add: algebra_simps)
          qed (use  \<open>x \<noteq> a\<close> \<open>0 < dd (x-a)\<close> that in auto)
          ultimately show ?thesis
            using segsub by (auto simp: rel_frontier_def)
        qed
        moreover have False if "1 < dd (x-a)"
          using x that dd2 [of "x - a" 1] \<open>x \<noteq> a\<close> closure_affine_hull
          by (auto simp: rel_frontier_def)
        ultimately have "dd (x-a) = 1" \<comment> \<open>similar to another proof above\<close>
          by fastforce
        with that show ?thesis
          by (simp add: rel_frontier_def)
      qed
    qed
  qed
qed

corollary rel_frontier_retract_of_punctured_affine_hull:
  fixes S :: "'a::euclidean_space set"
  assumes "bounded S" "convex S" "a \<in> rel_interior S"
    shows "rel_frontier S retract_of (affine hull S - {a})"
  by (meson assms convex_affine_hull dual_order.refl rel_frontier_affine_hull 
      rel_frontier_deformation_retract_of_punctured_convex retract_of_def)

corollary rel_boundary_retract_of_punctured_affine_hull:
  fixes S :: "'a::euclidean_space set"
  assumes "compact S" "convex S" "a \<in> rel_interior S"
    shows "(S - rel_interior S) retract_of (affine hull S - {a})"
by (metis assms closure_closed compact_eq_bounded_closed rel_frontier_def
          rel_frontier_retract_of_punctured_affine_hull)

lemma homotopy_eqv_rel_frontier_punctured_convex:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" "bounded S" "a \<in> rel_interior S" "convex T" "rel_frontier S \<subseteq> T" "T \<subseteq> affine hull S"
  shows "(rel_frontier S) homotopy_eqv (T - {a})"
  by (meson assms deformation_retract_imp_homotopy_eqv homotopy_equivalent_space_sym 
      rel_frontier_deformation_retract_of_punctured_convex[of S T])

lemma homotopy_eqv_rel_frontier_punctured_affine_hull:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S" "bounded S" "a \<in> rel_interior S"
    shows "(rel_frontier S) homotopy_eqv (affine hull S - {a})"
  by (simp add: assms homotopy_eqv_rel_frontier_punctured_convex rel_frontier_affine_hull)

lemma path_connected_sphere_gen:
  assumes "convex S" "bounded S" "aff_dim S \<noteq> 1"
  shows "path_connected(rel_frontier S)"
proof -
  have "convex (closure S)" 
    using assms by auto
  then show ?thesis
    by (metis Diff_empty aff_dim_affine_hull assms convex_affine_hull convex_imp_path_connected equals0I 
       path_connected_punctured_convex rel_frontier_def rel_frontier_retract_of_punctured_affine_hull retract_of_path_connected)
qed

lemma connected_sphere_gen:
  assumes "convex S" "bounded S" "aff_dim S \<noteq> 1"
  shows "connected(rel_frontier S)"
  by (simp add: assms path_connected_imp_connected path_connected_sphere_gen)

subsubsection\<open>Borsuk-style characterization of separation\<close>

lemma continuous_on_Borsuk_map:
   "a \<notin> S \<Longrightarrow>  continuous_on S (\<lambda>x. inverse(norm (x-a)) *\<^sub>R (x-a))"
by (rule continuous_intros | force)+

lemma Borsuk_map_into_sphere:
   "(\<lambda>x. inverse(norm (x-a)) *\<^sub>R (x-a)) \<in> S \<rightarrow> sphere 0 1 \<longleftrightarrow> (a \<notin> S)"
proof -
  have "\<And>x. \<lbrakk>a \<notin> S; x \<in> S\<rbrakk> \<Longrightarrow> inverse (norm (x-a)) * norm (x-a) = 1"
    by (metis left_inverse norm_eq_zero right_minus_eq)
  then show ?thesis
    by force
qed

lemma Borsuk_maps_homotopic_in_path_component:
  assumes "path_component (- S) a b"
    shows "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1)
                   (\<lambda>x. inverse(norm(x-a)) *\<^sub>R (x-a))
                   (\<lambda>x. inverse(norm(x - b)) *\<^sub>R (x - b))"
proof -
  obtain g where g: "path g" "path_image g \<subseteq> -S" "pathstart g = a" "pathfinish g = b"
    using assms by (auto simp: path_component_def)
  define h where "h \<equiv> \<lambda>z. (snd z - (g \<circ> fst) z) /\<^sub>R norm (snd z - (g \<circ> fst) z)"
  have "continuous_on ({0..1} \<times> S) h"
    unfolding h_def using g by (intro continuous_intros) (auto simp: path_defs)
  moreover
  have "h \<in> ({0..1} \<times> S) \<rightarrow> sphere 0 1"
    unfolding h_def using g  by (auto simp: divide_simps path_defs)
  ultimately show ?thesis
    using g by (auto simp: h_def path_defs homotopic_with_def)
qed

lemma non_extensible_Borsuk_map:
  fixes a :: "'a :: euclidean_space"
  assumes "compact S" and cin: "C \<in> components(- S)" and boc: "bounded C" and "a \<in> C"
    shows "\<not> (\<exists>g. continuous_on (S \<union> C) g \<and>
                  g \<in> (S \<union> C) \<rightarrow> sphere 0 1 \<and>
                  (\<forall>x \<in> S. g x = inverse(norm(x-a)) *\<^sub>R (x-a)))"
proof -
  have "closed S" using assms by (simp add: compact_imp_closed)
  have "C \<subseteq> -S"
    using assms by (simp add: in_components_subset)
  with \<open>a \<in> C\<close> have "a \<notin> S" by blast
  then have ceq: "C = connected_component_set (- S) a"
    by (metis \<open>a \<in> C\<close> cin components_iff connected_component_eq)
  then have "bounded (S \<union> connected_component_set (- S) a)"
    using \<open>compact S\<close> boc compact_imp_bounded by auto
  with bounded_subset_ballD obtain r where "0 < r" and r: "(S \<union> connected_component_set (- S) a) \<subseteq> ball a r"
    by blast
  { fix g
    assume "continuous_on (S \<union> C) g"
            "g \<in> (S \<union> C) \<rightarrow> sphere 0 1"
       and [simp]: "\<And>x. x \<in> S \<Longrightarrow> g x = (x-a) /\<^sub>R norm (x-a)"
    then have norm_g1[simp]: "\<And>x. x \<in> S \<union> C \<Longrightarrow> norm (g x) = 1"
      by force
    have cb_eq: "cball a r = (S \<union> connected_component_set (- S) a) \<union>
                      (cball a r - connected_component_set (- S) a)"
      using ball_subset_cball [of a r] r by auto
    have cont1: "continuous_on (S \<union> connected_component_set (- S) a)
                     (\<lambda>x. a + r *\<^sub>R g x)"
      using \<open>continuous_on (S \<union> C) g\<close> ceq
      by (intro continuous_intros) blast
    have cont2: "continuous_on (cball a r - connected_component_set (- S) a)
            (\<lambda>x. a + r *\<^sub>R ((x-a) /\<^sub>R norm (x-a)))"
      by (rule continuous_intros | force simp: \<open>a \<notin> S\<close>)+
    have 1: "continuous_on (cball a r)
             (\<lambda>x. if connected_component (- S) a x
                  then a + r *\<^sub>R g x
                  else a + r *\<^sub>R ((x-a) /\<^sub>R norm (x-a)))"
      apply (subst cb_eq)
      apply (rule continuous_on_cases [OF _ _ cont1 cont2])
      using \<open>closed S\<close> ceq cin 
      by (force simp: closed_Diff open_Compl closed_Un_complement_component open_connected_component)+
    have 2: "(\<lambda>x. a + r *\<^sub>R g x) ` (cball a r \<inter> connected_component_set (- S) a)
             \<subseteq> sphere a r "
      using \<open>0 < r\<close> by (force simp: dist_norm ceq)
    have "retraction (cball a r) (sphere a r)
            (\<lambda>x. if x \<in> connected_component_set (- S) a
                 then a + r *\<^sub>R g x
                 else a + r *\<^sub>R ((x-a) /\<^sub>R norm (x-a)))"
      using  \<open>0 < r\<close> \<open>a \<notin> S\<close> \<open>a \<in> C\<close> r
      by (auto simp: norm_minus_commute retraction_def Pi_iff ceq dist_norm abs_if 
          mult_less_0_iff divide_simps 1 2)
    then have False
      using no_retraction_cball
             [OF \<open>0 < r\<close>, of a, unfolded retract_of_def, simplified, rule_format,
              of "\<lambda>x. if x \<in> connected_component_set (- S) a
                      then a + r *\<^sub>R g x
                      else a + r *\<^sub>R inverse(norm(x-a)) *\<^sub>R (x-a)"]
      by blast
  }
  then show ?thesis
    by blast
qed

subsubsection \<open>Proving surjectivity via Brouwer fixpoint theorem\<close>

lemma brouwer_surjective:
  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
  assumes T: "compact T" "convex T" "T \<noteq> {}"
    and f: "continuous_on T f"
    and "\<And>x y. \<lbrakk>x\<in>S; y\<in>T\<rbrakk> \<Longrightarrow> x + (y - f y) \<in> T"
    and "x \<in> S"
  shows "\<exists>y\<in>T. f y = x"
proof -
  have *: "\<And>x y. f y = x \<longleftrightarrow> x + (y - f y) = y"
    by (auto simp add: algebra_simps)
  show ?thesis
    unfolding *
  proof (rule brouwer[OF T])
    show "continuous_on T (\<lambda>y. x + (y - f y))"
      by (intro continuous_intros f)
  qed (use assms in auto)
qed

lemma brouwer_surjective_cball:
  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
  assumes "continuous_on (cball a e) f"
    and "e > 0"
    and "x \<in> S"
    and "\<And>x y. \<lbrakk>x\<in>S; y\<in>cball a e\<rbrakk> \<Longrightarrow> x + (y - f y) \<in> cball a e"
  shows "\<exists>y\<in>cball a e. f y = x"
  by (smt (verit, best) assms brouwer_surjective cball_eq_empty compact_cball convex_cball)

subsubsection \<open>Inverse function theorem\<close>

text \<open>See Sussmann: "Multidifferential calculus", Theorem 2.1.1\<close>

lemma sussmann_open_mapping:
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
  assumes "open S"
    and contf: "continuous_on S f"
    and "x \<in> S"
    and derf: "(f has_derivative f') (at x)"
    and "bounded_linear g'" "f' \<circ> g' = id"
    and "T \<subseteq> S"
    and x: "x \<in> interior T"
  shows "f x \<in> interior (f ` T)"
proof -
  interpret f': bounded_linear f'
    using assms unfolding has_derivative_def by auto
  interpret g': bounded_linear g'
    using assms by auto
  obtain B where B: "0 < B" "\<forall>x. norm (g' x) \<le> norm x * B"
    using bounded_linear.pos_bounded[OF assms(5)] by blast
  hence *: "1 / (2 * B) > 0" by auto
  obtain e0 where e0:
      "0 < e0"
      "\<forall>y. norm (y - x) < e0 \<longrightarrow> norm (f y - f x - f' (y - x)) \<le> 1 / (2 * B) * norm (y - x)"
    using derf unfolding has_derivative_at_alt
    using * by blast
  obtain e1 where e1: "0 < e1" "cball x e1 \<subseteq> T"
    using mem_interior_cball x by blast
  have *: "0 < e0 / B" "0 < e1 / B" using e0 e1 B by auto
  obtain e where e: "0 < e" "e < e0 / B" "e < e1 / B"
    using field_lbound_gt_zero[OF *] by blast
  have lem: "\<exists>y\<in>cball (f x) e. f (x + g' (y - f x)) = z" if "z\<in>cball (f x) (e / 2)" for z
  proof (rule brouwer_surjective_cball)
    have z: "z \<in> S" if as: "y \<in>cball (f x) e" "z = x + (g' y - g' (f x))" for y z
    proof-
      have "dist x z = norm (g' (f x) - g' y)"
        unfolding as(2) and dist_norm by auto
      also have "\<dots> \<le> norm (f x - y) * B"
        by (metis B(2) g'.diff)
      also have "\<dots> \<le> e * B"
        by (metis B(1) dist_norm mem_cball mult_le_cancel_right_pos that(1))
      also have "\<dots> \<le> e1"
        using B(1) e(3) pos_less_divide_eq by fastforce
      finally have "z \<in> cball x e1"
        by force
      then show "z \<in> S"
        using e1 assms(7) by auto
    qed
    show "continuous_on (cball (f x) e) (\<lambda>y. f (x + g' (y - f x)))"
      unfolding g'.diff
    proof (rule continuous_on_compose2 [OF _ _ order_refl, of _ _ f])
      show "continuous_on ((\<lambda>y. x + (g' y - g' (f x))) ` cball (f x) e) f"
        by (rule continuous_on_subset[OF contf]) (use z in blast)
      show "continuous_on (cball (f x) e) (\<lambda>y. x + (g' y - g' (f x)))"
        by (intro continuous_intros linear_continuous_on[OF \<open>bounded_linear g'\<close>])
    qed
  next
    fix y z
    assume y: "y \<in> cball (f x) (e / 2)" and z: "z \<in> cball (f x) e"
    have "norm (g' (z - f x)) \<le> norm (z - f x) * B"
      using B by auto
    also have "\<dots> \<le> e * B"
      by (metis B(1) z dist_norm mem_cball norm_minus_commute mult_le_cancel_right_pos)
    also have "\<dots> < e0"
      using B(1) e(2) pos_less_divide_eq by blast
    finally have *: "norm (x + g' (z - f x) - x) < e0"
      by auto
    have **: "f x + f' (x + g' (z - f x) - x) = z"
      using assms(6)[unfolded o_def id_def,THEN cong]
      by auto
    have "norm (f x - (y + (z - f (x + g' (z - f x))))) \<le>
          norm (f (x + g' (z - f x)) - z) + norm (f x - y)"
      using norm_triangle_ineq[of "f (x + g'(z - f x)) - z" "f x - y"]
      by (auto simp add: algebra_simps)
    also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)"
      using e0(2)[rule_format, OF *]
      by (simp only: algebra_simps **) auto
    also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + e/2"
      using y by (auto simp: dist_norm)
    also have "\<dots> \<le> 1 / (B * 2) * B * norm (z - f x) + e/2"
      using * B by (auto simp add: field_simps)
    also have "\<dots> \<le> 1 / 2 * norm (z - f x) + e/2"
      by auto
    also have "\<dots> \<le> e/2 + e/2"
      using B(1) \<open>norm (z - f x) * B \<le> e * B\<close> by auto
    finally show "y + (z - f (x + g' (z - f x))) \<in> cball (f x) e"
      by (auto simp: dist_norm)
  qed (use e that in auto) 
  show ?thesis
    unfolding mem_interior
  proof (intro exI conjI subsetI)
    fix y
    assume "y \<in> ball (f x) (e / 2)"
    then have *: "y \<in> cball (f x) (e / 2)"
      by auto
    obtain z where z: "z \<in> cball (f x) e" "f (x + g' (z - f x)) = y"
      using lem * by blast
    then have "norm (g' (z - f x)) \<le> norm (z - f x) * B"
      using B
      by (auto simp add: field_simps)
    also have "\<dots> \<le> e * B"
      by (metis B(1) dist_norm mem_cball norm_minus_commute mult_le_cancel_right_pos z(1))
    also have "\<dots> \<le> e1"
      using e B unfolding less_divide_eq by auto
    finally have "x + g'(z - f x) \<in> T"
      by (metis add_diff_cancel diff_diff_add dist_norm e1(2) mem_cball norm_minus_commute subset_eq)
    then show "y \<in> f ` T"
      using z by auto
  qed (use e in auto)
qed

text \<open>Hence the following eccentric variant of the inverse function theorem.
  This has no continuity assumptions, but we do need the inverse function.
  We could put \<open>f' \<circ> g = I\<close> but this happens to fit with the minimal linear
  algebra theory I've set up so far.\<close>

lemma has_derivative_inverse_strong:
  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
  assumes S: "open S" "x \<in> S"
    and contf: "continuous_on S f"
    and gf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
    and derf: "(f has_derivative f') (at x)"
    and id: "f' \<circ> g' = id"
  shows "(g has_derivative g') (at (f x))"
proof -
  have linf: "bounded_linear f'"
    using derf unfolding has_derivative_def by auto
  then have ling: "bounded_linear g'"
    unfolding linear_conv_bounded_linear[symmetric]
    using id right_inverse_linear by blast
  moreover have "g' \<circ> f' = id"
    using id linear_inverse_left linear_linear linf ling by blast
  moreover have *: "\<And>T. \<lbrakk>T \<subseteq> S; x \<in> interior T\<rbrakk> \<Longrightarrow> f x \<in> interior (f ` T)"
    using S derf contf id ling sussmann_open_mapping by blast
  have "continuous (at (f x)) g"
    unfolding continuous_at Lim_at
  proof (intro strip)
    fix e :: real
    assume "e > 0"
    then have "f x \<in> interior (f ` (ball x e \<inter> S))"
      by (simp add: "*" S interior_open)
    then obtain d where d: "0 < d" "ball (f x) d \<subseteq> f ` (ball x e \<inter> S)"
      unfolding mem_interior by blast
    show "\<exists>d>0. \<forall>y. 0 < dist y (f x) \<and> dist y (f x) < d \<longrightarrow> dist (g y) (g (f x)) < e"
    proof (intro exI allI impI conjI)
      fix y
      assume "0 < dist y (f x) \<and> dist y (f x) < d"
      then have "g y \<in> g ` f ` (ball x e \<inter> S)"
        by (metis d(2) dist_commute mem_ball rev_image_eqI subset_iff)
      then show "dist (g y) (g (f x)) < e"
        using \<open>x \<in> S\<close> by (simp add: gf dist_commute image_iff)
    qed (use d in auto)
  qed
  moreover have "f x \<in> interior (f ` S)"
    using "*" S interior_eq by blast
  moreover have "f (g y) = y" if "y \<in> interior (f ` S)" for y
    by (metis gf imageE interiorE subsetD that)
  ultimately show ?thesis using assms
    by (metis has_derivative_inverse_basic_x open_interior)
qed

text \<open>A rewrite based on the other domain.\<close>

lemma has_derivative_inverse_strong_x:
  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
  assumes "open S"
    and "g y \<in> S"
    and "continuous_on S f"
    and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
    and "(f has_derivative f') (at (g y))"
    and "f' \<circ> g' = id"
    and f: "f (g y) = y"
  shows "(g has_derivative g') (at y)"
  using has_derivative_inverse_strong[OF assms(1-6)] by (simp add: f)

text \<open>On a region.\<close>

theorem has_derivative_inverse_on:
  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
  assumes "open S"
    and "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f'(x)) (at x)"
    and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
    and "f' x \<circ> g' x = id"
    and "x \<in> S"
  shows "(g has_derivative g'(x)) (at (f x))"
  by (meson assms continuous_on_eq_continuous_at has_derivative_continuous has_derivative_inverse_strong)

end