# Theory Brouwer_Fixpoint

theory Brouwer_Fixpoint
imports Convex_Euclidean_Space
`(*  Author:     John Harrison    Author:     Robert Himmelmann, TU Muenchen (Translation from HOL light)*)(* ========================================================================= *)(* Results connected with topological dimension.                             *)(*                                                                           *)(* 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                       *)(* ========================================================================= *)header {* Results connected with topological dimension. *}theory Brouwer_Fixpointimports Convex_Euclidean_Spacebegin(** move this **)lemma divide_nonneg_nonneg:  fixes a b :: real  assumes "a ≥ 0"    and "b ≥ 0"  shows "0 ≤ a / b"proof (cases "b = 0")  case True  then show ?thesis by autonext  case False  show ?thesis    apply (rule divide_nonneg_pos)    using assms False    apply auto    doneqedlemma brouwer_compactness_lemma:  fixes f :: "'a::metric_space => 'b::euclidean_space"  assumes "compact s"    and "continuous_on s f"    and "¬ (∃x∈s. f x = 0)"  obtains d where "0 < d" and "∀x∈s. d ≤ norm (f x)"proof (cases "s = {}")  case True  show thesis    by (rule that [of 1]) (auto simp: True)next  case False  have "continuous_on s (norm o f)"    by (rule continuous_on_intros continuous_on_norm assms(2))+  with False obtain x where x: "x ∈ s" "∀y∈s. (norm o f) x ≤ (norm o f) y"    using continuous_attains_inf[OF assms(1), of "norm o f"]    unfolding o_def    by auto  have "(norm o f) x > 0"    using assms(3) and x(1)    by auto  then show ?thesis    by (rule that) (insert x(2), auto simp: o_def)qedlemma 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 -  have and_forall_thm:"!!P Q. (∀x. P x) ∧ (∀x. Q x) <-> (∀x. P x ∧ Q x)"    by auto  have *: "∀x y::real. 0 ≤ x ∧ x ≤ 1 ∧ 0 ≤ y ∧ y ≤ 1 --> (x ≠ 1 ∧ x ≤ y ∨ x ≠ 0 ∧ y ≤ x)"    by auto  show ?thesis    unfolding and_forall_thm Ball_def    apply (subst choice_iff[symmetric])+    apply rule    apply rule  proof -    case (goal1 x)    let ?R = "λy. (P x ∧ Q xa ∧ x • xa = 0 --> y = (0::nat)) ∧        (P x ∧ Q xa ∧ x • xa = 1 --> y = 1) ∧        (P x ∧ Q xa ∧ y = 0 --> x • xa ≤ f x • xa) ∧        (P x ∧ Q xa ∧ y = 1 --> f x • xa ≤ x • xa)"    {      assume "P x" "Q xa" "xa ∈ Basis"      then have "0 ≤ f x • xa ∧ f x • xa ≤ 1"        using assms(2)[rule_format,of "f x" xa]        apply (drule_tac assms(1)[rule_format])        apply auto        done    }    then have "xa ∈ Basis ==> ?R 0 ∨ ?R 1" by auto    then show ?case by auto  qedqedsubsection {* The key "counting" observation, somewhat abstracted. *}lemma setsum_Un_disjoint':  assumes "finite A"    and "finite B"    and "A ∩ B = {}"    and "A ∪ B = C"  shows "setsum g C = setsum g A + setsum g B"  using setsum_Un_disjoint[OF assms(1-3)] and assms(4) by autolemma kuhn_counting_lemma:  assumes "finite faces"    and "finite simplices"    and "∀f∈faces. bnd f --> (card {s ∈ simplices. face f s} = 1)"    and "∀f∈faces. ¬ bnd f --> (card {s ∈ simplices. face f s} = 2)"    and "∀s∈simplices. compo s --> (card {f ∈ faces. face f s ∧ compo' f} = 1)"    and "∀s∈simplices. ¬ compo s -->      (card {f ∈ faces. face f s ∧ compo' f} = 0) ∨ (card {f ∈ faces. face f s ∧ compo' f} = 2)"    and "odd(card {f ∈ faces. compo' f ∧ bnd f})"  shows "odd(card {s ∈ simplices. compo s})"proof -  have "!!x. {f∈faces. compo' f ∧ bnd f ∧ face f x} ∪ {f∈faces. compo' f ∧ ¬bnd f ∧ face f x} =      {f∈faces. compo' f ∧ face f x}"    "!!x. {f ∈ faces. compo' f ∧ bnd f ∧ face f x} ∩ {f ∈ faces. compo' f ∧ ¬ bnd f ∧ face f x} = {}"    by auto  then have lem1: "setsum (λs. (card {f ∈ faces. face f s ∧ compo' f})) simplices =      setsum (λs. card {f ∈ {f ∈ faces. compo' f ∧ bnd f}. face f s}) simplices +      setsum (λs. card {f ∈ {f ∈ faces. compo' f ∧ ¬ (bnd f)}. face f s}) simplices"    unfolding setsum_addf[symmetric]    apply -    apply (rule setsum_cong2)    using assms(1)    apply (auto simp add: card_Un_Int, auto simp add:conj_commute)    done  have lem2:    "setsum (λj. card {f ∈ {f ∈ faces. compo' f ∧ bnd f}. face f j}) simplices =      1 * card {f ∈ faces. compo' f ∧ bnd f}"    "setsum (λj. card {f ∈ {f ∈ faces. compo' f ∧ ¬ bnd f}. face f j}) simplices =      2 * card {f ∈ faces. compo' f ∧ ¬ bnd f}"    apply (rule_tac[!] setsum_multicount)    using assms    apply auto    done  have lem3:    "setsum (λs. card {f ∈ faces. face f s ∧ compo' f}) simplices =      setsum (λs. card {f ∈ faces. face f s ∧ compo' f}) {s ∈ simplices.   compo s}+      setsum (λs. card {f ∈ faces. face f s ∧ compo' f}) {s ∈ simplices. ¬ compo s}"    apply (rule setsum_Un_disjoint')    using assms(2)    apply auto    done  have lem4: "setsum (λs. card {f ∈ faces. face f s ∧ compo' f}) {s ∈ simplices. compo s} =    setsum (λs. 1) {s ∈ simplices. compo s}"    apply (rule setsum_cong2)    using assms(5)    apply auto    done  have lem5: "setsum (λs. card {f ∈ faces. face f s ∧ compo' f}) {s ∈ simplices. ¬ compo s} =    setsum (λs. card {f ∈ faces. face f s ∧ compo' f})           {s ∈ simplices. (¬ compo s) ∧ (card {f ∈ faces. face f s ∧ compo' f} = 0)} +    setsum (λs. card {f ∈ faces. face f s ∧ compo' f})           {s ∈ simplices. (¬ compo s) ∧ (card {f ∈ faces. face f s ∧ compo' f} = 2)}"    apply (rule setsum_Un_disjoint')    using assms(2,6)    apply auto    done  have *: "int (∑s∈{s ∈ simplices. compo s}. card {f ∈ faces. face f s ∧ compo' f}) =    int (card {f ∈ faces. compo' f ∧ bnd f} + 2 * card {f ∈ faces. compo' f ∧ ¬ bnd f}) -    int (card {s ∈ simplices. ¬ compo s ∧ card {f ∈ faces. face f s ∧ compo' f} = 2} * 2)"    using lem1[unfolded lem3 lem2 lem5] by auto  have even_minus_odd:"!!x y. even x ==> odd (y::int) ==> odd (x - y)"    using assms by auto  have odd_minus_even:"!!x y. odd x ==> even (y::int) ==> odd (x - y)"    using assms by auto  show ?thesis    unfolding even_nat_def card_eq_setsum and lem4[symmetric] and *[unfolded card_eq_setsum]    unfolding card_eq_setsum[symmetric]    apply (rule odd_minus_even)    unfolding of_nat_add    apply(rule odd_plus_even)    apply(rule assms(7)[unfolded even_nat_def])    unfolding int_mult    apply auto    doneqedsubsection {* The odd/even result for faces of complete vertices, generalized. *}lemma card_1_exists: "card s = 1 <-> (∃!x. x ∈ s)"  unfolding One_nat_def  apply rule  apply (drule card_eq_SucD)  defer  apply (erule ex1E)proof -  fix x  assume as: "x ∈ s" "∀y. y ∈ s --> y = x"  have *: "s = insert x {}"    apply (rule set_eqI, rule) unfolding singleton_iff    apply (rule as(2)[rule_format]) using as(1)    apply auto    done  show "card s = Suc 0"    unfolding * using card_insert by autoqed autolemma card_2_exists: "card s = 2 <-> (∃x∈s. ∃y∈s. x ≠ y ∧ (∀z∈s. z = x ∨ z = y))"proof  assume "card s = 2"  then obtain x y where s: "s = {x, y}" "x ≠ y"    unfolding numeral_2_eq_2    apply -    apply (erule exE conjE | drule card_eq_SucD)+    apply auto    done  show "∃x∈s. ∃y∈s. x ≠ y ∧ (∀z∈s. z = x ∨ z = y)"    using s by autonext  assume "∃x∈s. ∃y∈s. x ≠ y ∧ (∀z∈s. z = x ∨ z = y)"  then obtain x y where "x ∈ s" "y ∈ s" "x ≠ y" "∀z∈s. z = x ∨ z = y"    by auto  then have "s = {x, y}"    by auto  with `x ≠ y` show "card s = 2"    by autoqedlemma image_lemma_0:  assumes "card {a∈s. f ` (s - {a}) = t - {b}} = n"  shows "card {s'. ∃a∈s. (s' = s - {a}) ∧ (f ` s' = t - {b})} = n"proof -  have *: "{s'. ∃a∈s. (s' = s - {a}) ∧ (f ` s' = t - {b})} =    (λa. s - {a}) ` {a∈s. f ` (s - {a}) = t - {b}}"    by auto  show ?thesis    unfolding *    unfolding assms[symmetric]    apply (rule card_image)    unfolding inj_on_def    apply (rule, rule, rule)    unfolding mem_Collect_eq    apply auto    doneqedlemma image_lemma_1:  assumes "finite s"    and "finite t"    and "card s = card t"    and "f ` s = t"    and "b ∈ t"  shows "card {s'. ∃a∈s. s' = s - {a} ∧  f ` s' = t - {b}} = 1"proof -  obtain a where a: "b = f a" "a ∈ s"    using assms(4-5) by auto  have inj: "inj_on f s"    apply (rule eq_card_imp_inj_on)    using assms(1-4)    apply auto    done  have *: "{a ∈ s. f ` (s - {a}) = t - {b}} = {a}"    apply (rule set_eqI)    unfolding singleton_iff    apply (rule, rule inj[unfolded inj_on_def, rule_format])    unfolding a    using a(2) and assms and inj[unfolded inj_on_def]    apply auto    done  show ?thesis    apply (rule image_lemma_0)    unfolding *    apply auto    doneqedlemma image_lemma_2:  assumes "finite s" "finite t" "card s = card t" "f ` s ⊆ t" "f ` s ≠ t" "b ∈ t"  shows "card {s'. ∃a∈s. (s' = s - {a}) ∧ f ` s' = t - {b}} = 0 ∨         card {s'. ∃a∈s. (s' = s - {a}) ∧ f ` s' = t - {b}} = 2"proof (cases "{a∈s. f ` (s - {a}) = t - {b}} = {}")  case True  then show ?thesis    apply -    apply (rule disjI1, rule image_lemma_0)    using assms(1)    apply auto    donenext  let ?M = "{a∈s. f ` (s - {a}) = t - {b}}"  case False  then obtain a where "a ∈ ?M"    by auto  then have a: "a ∈ s" "f ` (s - {a}) = t - {b}"    by auto  have "f a ∈ t - {b}"    using a and assms by auto  then have "∃c ∈ s - {a}. f a = f c"    unfolding image_iff[symmetric] and a    by auto  then obtain c where c: "c ∈ s" "a ≠ c" "f a = f c"    by auto  then have *: "f ` (s - {c}) = f ` (s - {a})"    apply -    apply (rule set_eqI)    apply rule  proof -    fix x    assume "x ∈ f ` (s - {a})"    then obtain y where y: "f y = x" "y ∈ s - {a}"      by auto    then show "x ∈ f ` (s - {c})"      unfolding image_iff      apply (rule_tac x = "if y = c then a else y" in bexI)      using c a      apply auto      done  qed auto  have "c ∈ ?M"    unfolding mem_Collect_eq and *    using a and c(1)    by auto  show ?thesis    apply (rule disjI2)    apply (rule image_lemma_0)    unfolding card_2_exists    apply (rule bexI[OF _ `a∈?M`])    apply (rule bexI[OF _ `c∈?M`])    apply rule    apply (rule `a ≠ c`)    apply rule    apply (unfold mem_Collect_eq)    apply (erule conjE)  proof -    fix z    assume as: "z ∈ s" "f ` (s - {z}) = t - {b}"    have inj: "inj_on f (s - {z})"      apply (rule eq_card_imp_inj_on)      unfolding as      using as(1) and assms      apply auto      done    show "z = a ∨ z = c"    proof (rule ccontr)      assume "¬ ?thesis"      then show False        using inj[unfolded inj_on_def, THEN bspec[where x=a], THEN bspec[where x=c]]        using `a ∈ s` `c ∈ s` `f a = f c` `a ≠ c`        apply auto        done    qed  qedqedsubsection {* Combine this with the basic counting lemma. *}lemma kuhn_complete_lemma:  assumes "finite simplices"    and "∀f s. face f s <-> (∃a∈s. f = s - {a})"    and "∀s∈simplices. card s = n + 2"    and "∀s∈simplices. (rl ` s) ⊆ {0..n+1}"    and "∀f∈{f. ∃s∈simplices. face f s}. bnd f  --> card {s∈simplices. face f s} = 1"    and "∀f∈{f. ∃s∈simplices. face f s}. ¬ bnd f --> card {s∈simplices. face f s} = 2"    and "odd (card {f∈{f. ∃s∈simplices. face f s}. rl ` f = {0..n} ∧ bnd f})"  shows "odd (card {s∈simplices. (rl ` s = {0..n+1})})"  apply (rule kuhn_counting_lemma)  defer  apply (rule assms)+  prefer 3  apply (rule assms)  apply (rule_tac[1-2] ballI impI)+proof -  have *: "{f. ∃s∈simplices. ∃a∈s. f = s - {a}} = (\<Union>s∈simplices. {f. ∃a∈s. (f = s - {a})})"    by auto  have **: "∀s∈simplices. card s = n + 2 ∧ finite s"    using assms(3) by (auto intro: card_ge_0_finite)  show "finite {f. ∃s∈simplices. face f s}"    unfolding assms(2)[rule_format] and *    apply (rule finite_UN_I[OF assms(1)])    using **    apply auto    done  have *: "!!P f s. s∈simplices ==> (f ∈ {f. ∃s∈simplices. ∃a∈s. f = s - {a}}) ∧    (∃a∈s. (f = s - {a})) ∧ P f <-> (∃a∈s. (f = s - {a}) ∧ P f)"    by auto  fix s  assume s: "s ∈ simplices"  let ?S = "{f ∈ {f. ∃s∈simplices. face f s}. face f s ∧ rl ` f = {0..n}}"  have "{0..n + 1} - {n + 1} = {0..n}"    by auto  then have S: "?S = {s'. ∃a∈s. s' = s - {a} ∧ rl ` s' = {0..n + 1} - {n + 1}}"    apply -    apply (rule set_eqI)    unfolding assms(2)[rule_format] mem_Collect_eq    unfolding *[OF s, unfolded mem_Collect_eq, where P="λx. rl ` x = {0..n}"]    apply auto    done  show "rl ` s = {0..n+1} ==> card ?S = 1" and "rl ` s ≠ {0..n+1} ==> card ?S = 0 ∨ card ?S = 2"    unfolding S    apply (rule_tac[!] image_lemma_1 image_lemma_2)    using ** assms(4) and s    apply auto    doneqedsubsection {*We use the following notion of ordering rather than pointwise indexing. *}definition "kle n x y <-> (∃k⊆{1..n::nat}. ∀j. y j = x j + (if j ∈ k then (1::nat) else 0))"lemma kle_refl [intro]: "kle n x x"  unfolding kle_def by autolemma kle_antisym: "kle n x y ∧ kle n y x <-> x = y"  unfolding kle_def  apply rule  apply auto  donelemma pointwise_minimal_pointwise_maximal:  fixes s :: "(nat => nat) set"  assumes "finite s"    and "s ≠ {}"    and "∀x∈s. ∀y∈s. (∀j. x j ≤ y j) ∨ (∀j. y j ≤ x j)"  shows "∃a∈s. ∀x∈s. ∀j. a j ≤ x j"    and "∃a∈s. ∀x∈s. ∀j. x j ≤ a j"  using assms  unfolding atomize_conjproof (induct s rule: finite_induct)  fix x  fix F :: "(nat => nat) set"  assume as: "finite F" "x ∉ F"    "[|F ≠ {}; ∀x∈F. ∀y∈F. (∀j. x j ≤ y j) ∨ (∀j. y j ≤ x j)|]        ==> (∃a∈F. ∀x∈F. ∀j. a j ≤ x j) ∧ (∃a∈F. ∀x∈F. ∀j. x j ≤ a j)" "insert x F ≠ {}"    "∀xa∈insert x F. ∀y∈insert x F. (∀j. xa j ≤ y j) ∨ (∀j. y j ≤ xa j)"  show "(∃a∈insert x F. ∀x∈insert x F. ∀j. a j ≤ x j) ∧ (∃a∈insert x F. ∀x∈insert x F. ∀j. x j ≤ a j)"  proof (cases "F = {}")    case True    then show ?thesis      apply -      apply (rule, rule_tac[!] x=x in bexI)      apply auto      done  next    case False    obtain a b where a: "a∈insert x F" "∀x∈F. ∀j. a j ≤ x j"      and b: "b ∈ insert x F" "∀x∈F. ∀j. x j ≤ b j"      using as(3)[OF False] using as(5) by auto    have "∃a ∈ insert x F. ∀x ∈ insert x F. ∀j. a j ≤ x j"      using as(5)[rule_format,OF a(1) insertI1]      apply -    proof (erule disjE)      assume "∀j. a j ≤ x j"      then show ?thesis        apply (rule_tac x=a in bexI)        using a        apply auto        done    next      assume "∀j. x j ≤ a j"      then show ?thesis        apply (rule_tac x=x in bexI)        apply (rule, rule)        apply (insert a)        apply (erule_tac x=xa in ballE)        apply (erule_tac x=j in allE)+        apply auto        done    qed    moreover    have "∃b∈insert x F. ∀x∈insert x F. ∀j. x j ≤ b j"      using as(5)[rule_format,OF b(1) insertI1]      apply -    proof (erule disjE)      assume "∀j. x j ≤ b j"      then show ?thesis        apply(rule_tac x=b in bexI) using b        apply auto        done    next      assume "∀j. b j ≤ x j"      then show ?thesis        apply (rule_tac x=x in bexI)        apply (rule, rule)        apply (insert b)        apply (erule_tac x=xa in ballE)        apply (erule_tac x=j in allE)+        apply auto        done    qed    ultimately show ?thesis by auto  qedqed autolemma kle_imp_pointwise: "kle n x y ==> ∀j. x j ≤ y j"  unfolding kle_def by autolemma pointwise_antisym:  fixes x :: "nat => nat"  shows "(∀j. x j ≤ y j) ∧ (∀j. y j ≤ x j) <-> x = y"  apply rule  apply (rule ext)  apply (erule conjE)  apply (erule_tac x = xa in allE)+  apply auto  donelemma kle_trans:  assumes "kle n x y"    and "kle n y z"    and "kle n x z ∨ kle n z x"  shows "kle n x z"  using assms  apply -  apply (erule disjE)  apply assumptionproof -  case goal1  then have "x = z"    apply -    apply (rule ext)    apply (drule kle_imp_pointwise)+    apply (erule_tac x=xa in allE)+    apply auto    done  then show ?case by autoqedlemma kle_strict:  assumes "kle n x y"    and "x ≠ y"  shows "∀j. x j ≤ y j"    and "∃k. 1 ≤ k ∧ k ≤ n ∧ x k < y k"  apply (rule kle_imp_pointwise[OF assms(1)])proof -  guess k using assms(1)[unfolded kle_def] .. note k = this  show "∃k. 1 ≤ k ∧ k ≤ n ∧ x k < y k"proof (cases "k = {}")  case True  then have "x = y"    apply -    apply (rule ext)    using k    apply auto    done  then show ?thesis    using assms(2) by autonext  case False  then have "(SOME k'. k' ∈ k) ∈ k"    apply -    apply (rule someI_ex)    apply auto    done  then show ?thesis    apply (rule_tac x = "SOME k'. k' ∈ k" in exI)    using k    apply auto    done  qedqedlemma kle_minimal:  assumes "finite s"    and "s ≠ {}"    and "∀x∈s. ∀y∈s. kle n x y ∨ kle n y x"  shows "∃a∈s. ∀x∈s. kle n a x"proof -  have "∃a∈s. ∀x∈s. ∀j. a j ≤ x j"    apply (rule pointwise_minimal_pointwise_maximal(1)[OF assms(1-2)])    apply rule    apply rule    apply (drule_tac assms(3)[rule_format])    apply assumption    using kle_imp_pointwise    apply auto    done  then guess a .. note a = this  show ?thesis    apply (rule_tac x = a in bexI)  proof    fix x    assume "x ∈ s"    show "kle n a x"      using assms(3)[rule_format,OF a(1) `x∈s`]      apply -    proof (erule disjE)      assume "kle n x a"      then have "x = a"        apply -        unfolding pointwise_antisym[symmetric]        apply (drule kle_imp_pointwise)        using a(2)[rule_format,OF `x∈s`]        apply auto        done      then show ?thesis using kle_refl by auto    qed  qed (insert a, auto)qedlemma kle_maximal:  assumes "finite s"    and "s ≠ {}"    and "∀x∈s. ∀y∈s. kle n x y ∨ kle n y x"  shows "∃a∈s. ∀x∈s. kle n x a"proof -  have "∃a∈s. ∀x∈s. ∀j. a j ≥ x j"    apply (rule pointwise_minimal_pointwise_maximal(2)[OF assms(1-2)])    apply rule    apply rule    apply (drule_tac assms(3)[rule_format],assumption)    using kle_imp_pointwise    apply auto    done  then guess a .. note a = this  show ?thesis     apply (rule_tac x = a in bexI)  proof    fix x    assume "x ∈ s"    show "kle n x a"      using assms(3)[rule_format,OF a(1) `x∈s`]      apply -    proof (erule disjE)      assume "kle n a x"      then have "x = a"        apply -        unfolding pointwise_antisym[symmetric]        apply (drule kle_imp_pointwise)        using a(2)[rule_format,OF `x∈s`]        apply auto        done      then show ?thesis        using kle_refl by auto    qed  qed (insert a, auto)qedlemma kle_strict_set:  assumes "kle n x y"    and "x ≠ y"  shows "1 ≤ card {k∈{1..n}. x k < y k}"proof -  guess i using kle_strict(2)[OF assms] ..  then have "card {i} ≤ card {k∈{1..n}. x k < y k}"    apply -    apply (rule card_mono)    apply auto    done  then show ?thesis    by autoqedlemma kle_range_combine:  assumes "kle n x y"    and "kle n y z"    and "kle n x z ∨ kle n z x"    and "m1 ≤ card {k∈{1..n}. x k < y k}"    and "m2 ≤ card {k∈{1..n}. y k < z k}"  shows "kle n x z ∧ m1 + m2 ≤ card {k∈{1..n}. x k < z k}"  apply rule  apply (rule kle_trans[OF assms(1-3)])proof -  have "!!j. x j < y j ==> x j < z j"    apply (rule less_le_trans)    using kle_imp_pointwise[OF assms(2)]    apply auto    done  moreover  have "!!j. y j < z j ==> x j < z j"    apply (rule le_less_trans)    using kle_imp_pointwise[OF assms(1)]    apply auto    done  ultimately  have *: "{k∈{1..n}. x k < y k} ∪ {k∈{1..n}. y k < z k} = {k∈{1..n}. x k < z k}"    by auto  have **: "{k ∈ {1..n}. x k < y k} ∩ {k ∈ {1..n}. y k < z k} = {}"    unfolding disjoint_iff_not_equal    apply rule    apply rule    apply (unfold mem_Collect_eq)    apply (rule notI)    apply (erule conjE)+  proof -    fix i j    assume as: "i ∈ {1..n}" "x i < y i" "j ∈ {1..n}" "y j < z j" "i = j"    guess kx using assms(1)[unfolded kle_def] .. note kx = this    have "x i < y i"      using as by auto    then have "i ∈ kx"      using as(1) kx      apply -      apply (rule ccontr)      apply auto      done    then have "x i + 1 = y i"      using kx by auto    moreover    guess ky using assms(2)[unfolded kle_def] .. note ky = this    have "y i < z i"      using as by auto    then have "i ∈ ky"      using as(1) ky      apply -      apply (rule ccontr)      apply auto      done    then have "y i + 1 = z i"      using ky by auto    ultimately    have "z i = x i + 2"      by auto    then show False      using assms(3)      unfolding kle_def      by (auto simp add: split_if_eq1)  qed  have fin: "!!P. finite {x∈{1..n::nat}. P x}"    by auto  have "m1 + m2 ≤ card {k∈{1..n}. x k < y k} + card {k∈{1..n}. y k < z k}"    using assms(4-5) by auto  also have "… ≤ card {k∈{1..n}. x k < z k}"    unfolding card_Un_Int[OF fin fin]    unfolding * **    by auto  finally show "m1 + m2 ≤ card {k ∈ {1..n}. x k < z k}"    by autoqedlemma kle_range_combine_l:  assumes "kle n x y"    and "kle n y z"    and "kle n x z ∨ kle n z x"    and "m ≤ card {k∈{1..n}. y(k) < z(k)}"  shows "kle n x z ∧ m ≤ card {k∈{1..n}. x(k) < z(k)}"  using kle_range_combine[OF assms(1-3) _ assms(4), of 0] by autolemma kle_range_combine_r:  assumes "kle n x y"    and "kle n y z"    and "kle n x z ∨ kle n z x" "m ≤ card {k∈{1..n}. x k < y k}"  shows "kle n x z ∧ m ≤ card {k∈{1..n}. x(k) < z(k)}"  using kle_range_combine[OF assms(1-3) assms(4), of 0] by autolemma kle_range_induct:  assumes "card s = Suc m"    and "∀x∈s. ∀y∈s. kle n x y ∨ kle n y x"  shows "∃x∈s. ∃y∈s. kle n x y ∧ m ≤ card {k∈{1..n}. x k < y k}"proof -  have "finite s" and "s ≠ {}"    using assms(1)    by (auto intro: card_ge_0_finite)  then show ?thesis    using assms  proof (induct m arbitrary: s)    case 0    then show ?case      using kle_refl by auto  next    case (Suc m)    then obtain a where a: "a ∈ s" "∀x∈s. kle n a x"      using kle_minimal[of s n] by auto    show ?case    proof (cases "s ⊆ {a}")      case False      then have "card (s - {a}) = Suc m" and "s - {a} ≠ {}"        using card_Diff_singleton[OF _ a(1)] Suc(4) `finite s`        by auto      then obtain x b where xb:        "x ∈ s - {a}"        "b ∈ s - {a}"        "kle n x b"        "m ≤ card {k ∈ {1..n}. x k < b k}"        using Suc(1)[of "s - {a}"]        using Suc(5) `finite s`        by auto      have "1 ≤ card {k ∈ {1..n}. a k < x k}" and "m ≤ card {k ∈ {1..n}. x k < b k}"        apply (rule kle_strict_set)        apply (rule a(2)[rule_format])        using a and xb        apply auto        done      then show ?thesis        apply (rule_tac x=a in bexI)        apply (rule_tac x=b in bexI)        using kle_range_combine[OF a(2)[rule_format] xb(3) Suc(5)[rule_format], of 1 "m"]        using a(1) xb(1-2)        apply auto        done    next      case True      then have "s = {a}"        using Suc(3) by auto      then have "card s = 1"        by auto      then have False        using Suc(4) `finite s` by auto      then show ?thesis        by auto    qed  qedqedlemma kle_Suc: "kle n x y ==> kle (n + 1) x y"  unfolding kle_def  apply (erule exE)  apply (rule_tac x=k in exI)  apply auto  donelemma kle_trans_1:  assumes "kle n x y"  shows "x j ≤ y j"    and "y j ≤ x j + 1"  using assms[unfolded kle_def] by autolemma kle_trans_2:  assumes "kle n a b"    and "kle n b c"    and "∀j. c j ≤ a j + 1"  shows "kle n a c"proof -  guess kk1 using assms(1)[unfolded kle_def] .. note kk1 = this  guess kk2 using assms(2)[unfolded kle_def] .. note kk2 = this  show ?thesis    unfolding kle_def    apply (rule_tac x="kk1 ∪ kk2" in exI)    apply rule    defer  proof    fix i    show "c i = a i + (if i ∈ kk1 ∪ kk2 then 1 else 0)"    proof (cases "i ∈ kk1 ∪ kk2")      case True      then have "c i ≥ a i + (if i ∈ kk1 ∪ kk2 then 1 else 0)"        unfolding kk1[THEN conjunct2,rule_format,of i] kk2[THEN conjunct2,rule_format,of i]        by auto      moreover      have "c i ≤ a i + (if i ∈ kk1 ∪ kk2 then 1 else 0)"        using True assms(3) by auto      ultimately show ?thesis by auto    next      case False      then show ?thesis        using kk1 kk2 by auto    qed  qed (insert kk1 kk2, auto)qedlemma kle_between_r:  assumes "kle n a b"    and "kle n b c"    and "kle n a x"    and "kle n c x"  shows "kle n b x"  apply (rule kle_trans_2[OF assms(2,4)])proof  have *: "!!c b x::nat. x ≤ c + 1 ==> c ≤ b ==> x ≤ b + 1"    by auto  fix j  show "x j ≤ b j + 1"    apply (rule *)    using kle_trans_1[OF assms(1),of j] kle_trans_1[OF assms(3), of j]    apply auto    doneqedlemma kle_between_l:  assumes "kle n a b"    and "kle n b c"    and "kle n x a"    and "kle n x c"  shows "kle n x b"  apply (rule kle_trans_2[OF assms(3,1)])proof  have *: "!!c b x::nat. c ≤ x + 1 ==> b ≤ c ==> b ≤ x + 1"    by auto  fix j  show "b j ≤ x j + 1"    apply (rule *)    using kle_trans_1[OF assms(2),of j] kle_trans_1[OF assms(4), of j]    apply auto    doneqedlemma kle_adjacent:  assumes "∀j. b j = (if j = k then a(j) + 1 else a j)"    and "kle n a x"    and "kle n x b"  shows "x = a ∨ x = b"proof (cases "x k = a k")  case True  show ?thesis    apply (rule disjI1)    apply (rule ext)  proof -    fix j    have "x j ≤ a j"      using kle_imp_pointwise[OF assms(3),THEN spec[where x=j]]      unfolding assms(1)[rule_format]      apply -      apply(cases "j = k")      using True      apply auto      done    then show "x j = a j"      using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]]      by auto  qednext  case False  show ?thesis    apply (rule disjI2)    apply (rule ext)  proof -    fix j    have "x j ≥ b j"      using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]]      unfolding assms(1)[rule_format]      apply -      apply (cases "j = k")      using False      apply auto      done    then show "x j = b j"      using kle_imp_pointwise[OF assms(3),THEN spec[where x=j]]    by auto  qedqedsubsection {* Kuhn's notion of a simplex (a reformulation to avoid so much indexing) *}definition "ksimplex p n (s::(nat => nat) set) <->  card s = n + 1 ∧  (∀x∈s. ∀j. x j ≤ p) ∧  (∀x∈s. ∀j. j ∉ {1..n} --> x j = p) ∧  (∀x∈s. ∀y∈s. kle n x y ∨ kle n y x)"lemma ksimplexI:  "card s = n + 1 ==>  ∀x∈s. ∀j. x j ≤ p ==>  ∀x∈s. ∀j. j ∉ {1..n} --> x j = p ==>  ∀x∈s. ∀y∈s. kle n x y ∨ kle n y x ==>  ksimplex p n s"  unfolding ksimplex_def by autolemma ksimplex_eq:  "ksimplex p n (s::(nat => nat) set) <->    card s = n + 1 ∧    finite s ∧    (∀x∈s. ∀j. x(j) ≤ p) ∧    (∀x∈s. ∀j. j∉{1..n} --> x j = p) ∧    (∀x∈s. ∀y∈s. kle n x y ∨ kle n y x)"  unfolding ksimplex_def by (auto intro: card_ge_0_finite)lemma ksimplex_extrema:  assumes "ksimplex p n s"  obtains a b where "a ∈ s"    and "b ∈ s"    and "∀x∈s. kle n a x ∧ kle n x b"    and "∀i. b i = (if i ∈ {1..n} then a i + 1 else a i)"proof (cases "n = 0")  case True  obtain x where *: "s = {x}"    using assms[unfolded ksimplex_eq True,THEN conjunct1]    unfolding add_0_left card_1_exists    by auto  show ?thesis    apply (rule that[of x x])    unfolding * True    apply auto    donenext  note assm = assms[unfolded ksimplex_eq]  case False  have "s ≠ {}"    using assm by auto  obtain a where a: "a ∈ s" "∀x∈s. kle n a x"    using `s ≠ {}` assm    using kle_minimal[of s n]    by auto  obtain b where b: "b ∈ s" "∀x∈s. kle n x b"    using `s ≠ {}` assm    using kle_maximal[of s n]    by auto  obtain c d where c_d: "c ∈ s" "d ∈ s" "kle n c d" "n ≤ card {k ∈ {1..n}. c k < d k}"    using kle_range_induct[of s n n]    using assm    by auto  have "kle n c b ∧ n ≤ card {k ∈ {1..n}. c k < b k}"    apply (rule kle_range_combine_r[where y=d])    using c_d a b    apply auto    done  then have "kle n a b ∧ n ≤ card {k∈{1..n}. a(k) < b(k)}"    apply -    apply (rule kle_range_combine_l[where y=c])    using a `c ∈ s` `b ∈ s`    apply auto    done  moreover  have "card {1..n} ≥ card {k∈{1..n}. a(k) < b(k)}"    by (rule card_mono) auto  ultimately  have *: "{k∈{1 .. n}. a k < b k} = {1..n}"    apply -    apply (rule card_subset_eq)    apply auto    done  show ?thesis    apply (rule that[OF a(1) b(1)])    defer    apply (subst *[symmetric])    unfolding mem_Collect_eq  proof    guess k using a(2)[rule_format,OF b(1),unfolded kle_def] .. note k = this    fix i    show "b i = (if i ∈ {1..n} ∧ a i < b i then a i + 1 else a i)"    proof (cases "i ∈ {1..n}")      case True      then show ?thesis        unfolding k[THEN conjunct2,rule_format] by auto    next      case False      have "a i = p"        using assm and False `a∈s` by auto      moreover have "b i = p"        using assm and False `b∈s` by auto      ultimately show ?thesis        by auto    qed  qed (insert a(2) b(2) assm, auto)qedlemma ksimplex_extrema_strong:  assumes "ksimplex p n s"    and "n ≠ 0"  obtains a b where "a ∈ s"    and "b ∈ s"    and "a ≠ b"    and "∀x∈s. kle n a x ∧ kle n x b"    and "∀i. b i = (if i ∈ {1..n} then a(i) + 1 else a i)"proof -  obtain a b where ab: "a ∈ s" "b ∈ s"    "∀x∈s. kle n a x ∧ kle n x b" "∀i. b(i) = (if i ∈ {1..n} then a(i) + 1 else a(i))"    apply (rule ksimplex_extrema[OF assms(1)])    apply auto    done  have "a ≠ b"    apply (rule notI)    apply (drule cong[of _ _ 1 1])    using ab(4) assms(2)    apply auto    done  then show ?thesis    apply (rule_tac that[of a b])    using ab    apply auto    doneqedlemma ksimplexD:  assumes "ksimplex p n s"  shows "card s = n + 1"    and "finite s"    and "card s = n + 1"    and "∀x∈s. ∀j. x j ≤ p"    and "∀x∈s. ∀j. j ∉ {1..n} --> x j = p"    and "∀x∈s. ∀y∈s. kle n x y ∨ kle n y x"  using assms unfolding ksimplex_eq by autolemma ksimplex_successor:  assumes "ksimplex p n s"    and "a ∈ s"  shows "(∀x∈s. kle n x a) ∨ (∃y∈s. ∃k∈{1..n}. ∀j. y j = (if j = k then a j + 1 else a j))"proof (cases "∀x∈s. kle n x a")  case True  then show ?thesis by autonext  note assm = ksimplexD[OF assms(1)]  case False  then obtain b where b: "b ∈ s" "¬ kle n b a" "∀x∈{x ∈ s. ¬ kle n x a}. kle n b x"    using kle_minimal[of "{x∈s. ¬ kle n x a}" n] and assm    by auto  then have **: "1 ≤ card {k∈{1..n}. a k < b k}"    apply -    apply (rule kle_strict_set)    using assm(6) and `a∈s`    apply (auto simp add: kle_refl)    done  let ?kle1 = "{x ∈ s. ¬ kle n x a}"  have "card ?kle1 > 0"    apply (rule ccontr)    using assm(2) and False    apply auto    done  then have sizekle1: "card ?kle1 = Suc (card ?kle1 - 1)"    using assm(2) by auto  obtain c d where c_d: "c ∈ s" "¬ kle n c a" "d ∈ s" "¬ kle n d a"    "kle n c d" "card ?kle1 - 1 ≤ card {k ∈ {1..n}. c k < d k}"    using kle_range_induct[OF sizekle1, of n] using assm by auto  let ?kle2 = "{x ∈ s. kle n x a}"  have "card ?kle2 > 0"    apply (rule ccontr)    using assm(6)[rule_format,of a a] and `a∈s` and assm(2)    apply auto    done  then have sizekle2: "card ?kle2 = Suc (card ?kle2 - 1)"    using assm(2) by auto  obtain e f where e_f: "e ∈ s" "kle n e a" "f ∈ s" "kle n f a"    "kle n e f" "card ?kle2 - 1 ≤ card {k ∈ {1..n}. e k < f k}"    using kle_range_induct[OF sizekle2, of n]    using assm    by auto  have "card {k∈{1..n}. a k < b k} = 1"  proof (rule ccontr)    assume "¬ ?thesis"    then have as: "card {k∈{1..n}. a k < b k} ≥ 2"      using ** by auto    have *: "finite ?kle2" "finite ?kle1" "?kle2 ∪ ?kle1 = s" "?kle2 ∩ ?kle1 = {}"      using assm(2) by auto    have "(card ?kle2 - 1) + 2 + (card ?kle1 - 1) = card ?kle2 + card ?kle1"      using sizekle1 sizekle2 by auto    also have "… = n + 1"      unfolding card_Un_Int[OF *(1-2)] *(3-)      using assm(3)      by auto    finally have n: "(card ?kle2 - 1) + (2 + (card ?kle1 - 1)) = n + 1"      by auto    have "kle n e a ∧ card {x ∈ s. kle n x a} - 1 ≤ card {k ∈ {1..n}. e k < a k}"      apply (rule kle_range_combine_r[where y=f])      using e_f using `a ∈ s` assm(6)      apply auto      done    moreover have "kle n b d ∧ card {x ∈ s. ¬ kle n x a} - 1 ≤ card {k ∈ {1..n}. b k < d k}"      apply (rule kle_range_combine_l[where y=c])      using c_d using assm(6) and b      apply auto      done    then have "kle n a d ∧ 2 + (card {x ∈ s. ¬ kle n x a} - 1) ≤ card {k ∈ {1..n}. a k < d k}"      apply -      apply (rule kle_range_combine[where y=b]) using as and b assm(6) `a ∈ s` `d ∈ s`      apply blast+      done    ultimately    have "kle n e d ∧ (card ?kle2 - 1) + (2 + (card ?kle1 - 1)) ≤ card {k∈{1..n}. e k < d k}"      apply -      apply (rule kle_range_combine[where y=a]) using assm(6)[rule_format, OF `e ∈ s` `d ∈ s`]      apply blast+      done    moreover have "card {k ∈ {1..n}. e k < d k} ≤ card {1..n}"      by (rule card_mono) auto    ultimately show False      unfolding n by auto  qed  then guess k unfolding card_1_exists .. note k = this[unfolded mem_Collect_eq]  show ?thesis    apply (rule disjI2)    apply (rule_tac x=b in bexI)    apply (rule_tac x=k in bexI)  proof    fix j :: nat    have "kle n a b"      using b and assm(6)[rule_format, OF `a∈s` `b∈s`]      by auto    then guess kk unfolding kle_def .. note kk_raw = this    note kk = this[THEN conjunct2, rule_format]    have kkk: "k ∈ kk"      apply (rule ccontr)      using k(1)      unfolding kk      apply auto      done    show "b j = (if j = k then a j + 1 else a j)"    proof (cases "j ∈ kk")      case True      then have "j = k"        apply -        apply (rule k(2)[rule_format])        using kk_raw kkk        apply auto        done      then show ?thesis        unfolding kk using kkk by auto    next      case False      then have "j ≠ k"        using k(2)[rule_format, of j k] and kk_raw kkk        by auto      then show ?thesis        unfolding kk        using kkk and False        by auto    qed  qed (insert k(1) `b ∈ s`, auto)qedlemma ksimplex_predecessor:  assumes "ksimplex p n s"    and "a ∈ s"  shows "(∀x∈s. kle n a x) ∨ (∃y∈s. ∃k∈{1..n}. ∀j. a j = (if j = k then y j + 1 else y j))"proof (cases "∀x∈s. kle n a x")  case True  then show ?thesis by autonext  note assm = ksimplexD[OF assms(1)]  case False  then obtain b where b: "b ∈ s" "¬ kle n a b" "∀x∈{x ∈ s. ¬ kle n a x}. kle n x b"    using kle_maximal[of "{x∈s. ¬ kle n a x}" n] and assm    by auto  then have **: "1 ≤ card {k∈{1..n}. a k > b k}"    apply -    apply (rule kle_strict_set)    using assm(6) and `a ∈ s`    apply (auto simp add: kle_refl)    done  let ?kle1 = "{x ∈ s. ¬ kle n a x}"  have "card ?kle1 > 0"    apply (rule ccontr)    using assm(2) and False    apply auto    done  then have sizekle1: "card ?kle1 = Suc (card ?kle1 - 1)"    using assm(2) by auto  obtain c d where c_d: "c ∈ s" "¬ kle n a c" "d ∈ s" "¬ kle n a d"    "kle n d c" "card ?kle1 - 1 ≤ card {k ∈ {1..n}. c k > d k}"    using kle_range_induct[OF sizekle1, of n]    using assm    by auto  let ?kle2 = "{x ∈ s. kle n a x}"  have "card ?kle2 > 0"    apply (rule ccontr)    using assm(6)[rule_format,of a a] and `a ∈ s` and assm(2)    apply auto    done  then have sizekle2: "card ?kle2 = Suc (card ?kle2 - 1)"    using assm(2)    by auto  obtain e f where e_f: "e ∈ s" "kle n a e" "f ∈ s" "kle n a f"    "kle n f e" "card ?kle2 - 1 ≤ card {k ∈ {1..n}. e k > f k}"    using kle_range_induct[OF sizekle2, of n]    using assm    by auto  have "card {k∈{1..n}. a k > b k} = 1"  proof (rule ccontr)    assume "¬ ?thesis"    then have as: "card {k∈{1..n}. a k > b k} ≥ 2"      using ** by auto    have *: "finite ?kle2" "finite ?kle1" "?kle2 ∪ ?kle1 = s" "?kle2 ∩ ?kle1 = {}"      using assm(2) by auto    have "(card ?kle2 - 1) + 2 + (card ?kle1 - 1) = card ?kle2 + card ?kle1"      using sizekle1 sizekle2 by auto    also have "… = n + 1"      unfolding card_Un_Int[OF *(1-2)] *(3-)      using assm(3) by auto    finally have n: "(card ?kle1 - 1) + 2 + (card ?kle2 - 1) = n + 1"      by auto    have "kle n a e ∧ card {x ∈ s. kle n a x} - 1 ≤ card {k ∈ {1..n}. e k > a k}"      apply (rule kle_range_combine_l[where y=f])      using e_f and `a∈s` assm(6)      apply auto      done    moreover have "kle n d b ∧ card {x ∈ s. ¬ kle n a x} - 1 ≤ card {k ∈ {1..n}. b k > d k}"      apply (rule kle_range_combine_r[where y=c])      using c_d and assm(6) and b      apply auto      done    then have "kle n d a ∧ (card {x ∈ s. ¬ kle n a x} - 1) + 2 ≤ card {k ∈ {1..n}. a k > d k}"      apply -      apply (rule kle_range_combine[where y=b]) using as and b assm(6) `a ∈ s` `d ∈ s`      apply blast+      done    ultimately have "kle n d e ∧ (card ?kle1 - 1 + 2) + (card ?kle2 - 1) ≤ card {k∈{1..n}. e k > d k}"      apply -      apply (rule kle_range_combine[where y=a])      using assm(6)[rule_format,OF `e∈s` `d∈s`]      apply blast+      done    moreover have "card {k ∈ {1..n}. e k > d k} ≤ card {1..n}"      by (rule card_mono) auto    ultimately show False      unfolding n by auto  qed  then guess k unfolding card_1_exists .. note k = this[unfolded mem_Collect_eq]  show ?thesis    apply (rule disjI2)    apply (rule_tac x=b in bexI)    apply (rule_tac x=k in bexI)  proof    fix j :: nat    have "kle n b a"      using b and assm(6)[rule_format, OF `a∈s` `b∈s`] by auto    then guess kk unfolding kle_def .. note kk_raw = this    note kk = this[THEN conjunct2,rule_format]    have kkk: "k ∈ kk"      apply (rule ccontr)      using k(1)      unfolding kk      apply auto      done    show "a j = (if j = k then b j + 1 else b j)"    proof (cases "j ∈ kk")      case True      then have "j = k"        apply -        apply (rule k(2)[rule_format])        using kk_raw kkk        apply auto        done      then show ?thesis        unfolding kk using kkk by auto    next      case False      then have "j ≠ k"        using k(2)[rule_format, of j k]        using kk_raw kkk        by auto      then show ?thesis        unfolding kk        using kkk and False        by auto    qed  qed (insert k(1) `b∈s`, auto)qedsubsection {* The lemmas about simplices that we need. *}(* FIXME: These are clones of lemmas in Library/FuncSet *)lemma card_funspace':  assumes "finite s"    and "finite t"    and "card s = m"    and "card t = n"  shows "card {f. (∀x∈s. f x ∈ t) ∧ (∀x∈UNIV - s. f x = d)} = n ^ m"    (is "card (?M s) = _")  using assmsproof (induct m arbitrary: s)  case 0  have [simp]: "{f. ∀x. f x = d} = {λx. d}"    apply (rule set_eqI)    apply rule    unfolding mem_Collect_eq    apply rule    apply (rule ext)    apply auto    done  from 0 show ?case    by autonext  case (Suc m)  guess a using card_eq_SucD[OF Suc(4)] ..  then guess s0 by (elim exE conjE) note as0 = this  have **: "card s0 = m"    using as0 using Suc(2) Suc(4)    by auto  let ?l = "(λ(b, g) x. if x = a then b else g x)"  have *: "?M (insert a s0) = ?l ` {(b,g). b∈t ∧ g∈?M s0}"    apply (rule set_eqI, rule)    unfolding mem_Collect_eq image_iff    apply (erule conjE)    apply (rule_tac x="(x a, λy. if y∈s0 then x y else d)" in bexI)    apply (rule ext)    prefer 3    apply rule    defer    apply (erule bexE)    apply rule    unfolding mem_Collect_eq    apply (erule splitE)+    apply (erule conjE)+  proof -    fix x xa xb xc y    assume as:      "x = (λ(b, g) x. if x = a then b else g x) xa"      "xb ∈ UNIV - insert a s0"      "xa = (xc, y)"      "xc ∈ t"      "∀x∈s0. y x ∈ t"      "∀x∈UNIV - s0. y x = d"    then show "x xb = d"      unfolding as by auto  qed auto  have inj: "inj_on ?l {(b,g). b∈t ∧ g∈?M s0}"    unfolding inj_on_def    apply rule    apply rule    apply rule    unfolding mem_Collect_eq    apply (erule splitE conjE)+  proof -    case goal1 note as = this(1,4-)[unfolded goal1 split_conv]    have "xa = xb"      using as(1)[THEN cong[of _ _ a]] by auto    moreover have "ya = yb"    proof (rule ext)      fix x      show "ya x = yb x"      proof (cases "x = a")        case False        then show ?thesis          using as(1)[THEN cong[of _ _ x x]] by auto      next        case True        then show ?thesis          using as(5,7) using as0(2) by auto      qed    qed    ultimately show ?case      unfolding goal1 by auto  qed  have "finite s0"    using `finite s` unfolding as0 by simp  show ?case    unfolding as0 * card_image[OF inj]    using assms    unfolding SetCompr_Sigma_eq    unfolding card_cartesian_product    using Suc(1)[OF `finite s0` `finite t` ** `card t = n`]    by autoqedlemma card_funspace:  assumes "finite s"    and "finite t"  shows "card {f. (∀x∈s. f x ∈ t) ∧ (∀x∈UNIV - s. f x = d)} = card t ^ card s"  using assms by (auto intro: card_funspace')lemma finite_funspace:  assumes "finite s"    and "finite t"  shows "finite {f. (∀x∈s. f x ∈ t) ∧ (∀x∈UNIV - s. f x = d)}"    (is "finite ?S")proof (cases "card t > 0")  case True  have "card ?S = card t ^ card s"    using assms by (auto intro!: card_funspace)  then show ?thesis    using True by (rule_tac card_ge_0_finite) simpnext  case False  then have "t = {}"    using `finite t` by auto  show ?thesis  proof (cases "s = {}")    case True    have *: "{f. ∀x. f x = d} = {λx. d}"      by auto    from True show ?thesis      using `t = {}` by (auto simp: *)  next    case False    then show ?thesis      using `t = {}` by simp  qedqedlemma finite_simplices: "finite {s. ksimplex p n s}"  apply (rule finite_subset[of _ "{s. s⊆{f. (∀i∈{1..n}. f i ∈ {0..p}) ∧ (∀i∈UNIV-{1..n}. f i = p)}}"])  unfolding ksimplex_def  defer  apply (rule finite_Collect_subsets)  apply (rule finite_funspace)  apply auto  donelemma simplex_top_face:  assumes "0 < p"    and "∀x∈f. x (n + 1) = p"  shows "(∃s a. ksimplex p (n + 1) s ∧ a ∈ s ∧ (f = s - {a})) <-> ksimplex p n f"    (is "?ls = ?rs")proof  assume ?ls  then guess s ..  then guess a by (elim exE conjE) note sa = this  show ?rs    unfolding ksimplex_def sa(3)    apply rule    defer    apply rule    defer    apply (rule, rule, rule, rule)    defer    apply (rule, rule)  proof -    fix x y    assume as: "x ∈s - {a}" "y ∈s - {a}"    have xyp: "x (n + 1) = y (n + 1)"      using as(1)[unfolded sa(3)[symmetric], THEN assms(2)[rule_format]]      using as(2)[unfolded sa(3)[symmetric], THEN assms(2)[rule_format]]      by auto    show "kle n x y ∨ kle n y x"    proof (cases "kle (n + 1) x y")      case True      then guess k unfolding kle_def .. note k = this      then have *: "n + 1 ∉ k" using xyp by auto      have "¬ (∃x∈k. x ∉ {1..n})"        apply (rule notI)        apply (erule bexE)      proof -        fix x        assume as: "x ∈ k" "x ∉ {1..n}"        have "x ≠ n + 1"          using as and * by auto        then show False          using as and k[THEN conjunct1,unfolded subset_eq] by auto      qed      then show ?thesis        apply -        apply (rule disjI1)        unfolding kle_def        using k        apply (rule_tac x=k in exI)        apply auto        done    next      case False      then have "kle (n + 1) y x"        using ksimplexD(6)[OF sa(1),rule_format, of x y] and as        by auto      then guess k unfolding kle_def .. note k = this      then have *: "n + 1 ∉ k"        using xyp by auto      then have "¬ (∃x∈k. x ∉ {1..n})"        apply -        apply (rule notI)        apply (erule bexE)      proof -        fix x        assume as: "x ∈ k" "x ∉ {1..n}"        have "x ≠ n + 1"          using as and * by auto        then show False          using as and k[THEN conjunct1,unfolded subset_eq]          by auto      qed      then show ?thesis        apply -        apply (rule disjI2)        unfolding kle_def        using k        apply (rule_tac x = k in exI)        apply auto        done    qed  next    fix x j    assume as: "x ∈ s - {a}" "j ∉ {1..n}"    then show "x j = p"      using as(1)[unfolded sa(3)[symmetric], THEN assms(2)[rule_format]]      apply (cases "j = n + 1")      using sa(1)[unfolded ksimplex_def]      apply auto      done  qed (insert sa ksimplexD[OF sa(1)], auto)next  assume ?rs note rs=ksimplexD[OF this]  guess a b by (rule ksimplex_extrema[OF `?rs`]) note ab = this  def c ≡ "λi. if i = (n + 1) then p - 1 else a i"  have "c ∉ f"    apply (rule notI)    apply (drule assms(2)[rule_format])    unfolding c_def    using assms(1)    apply auto    done  then show ?ls    apply (rule_tac x = "insert c f" in exI)    apply (rule_tac x = c in exI)    unfolding ksimplex_def conj_assoc    apply (rule conjI)    defer    apply (rule conjI)    defer    apply (rule conjI)    defer    apply (rule conjI)    defer  proof (rule_tac[3-5] ballI allI)+    fix x j    assume x: "x ∈ insert c f"    then show "x j ≤ p"    proof (cases "x = c")      case True      show ?thesis        unfolding True c_def        apply (cases "j = n + 1")        using ab(1) and rs(4)        apply auto        done    next      case False      with insert x rs(4) show ?thesis        by (auto simp add: c_def)    qed    show "j ∉ {1..n + 1} --> x j = p"      apply (cases "x = c")      using x ab(1) rs(5)      unfolding c_def      apply auto      done    {      fix z      assume z: "z ∈ insert c f"      then have "kle (n + 1) c z"      proof (cases "z = c")        case False        then have "z ∈ f"          using z by auto        then guess k          apply (drule_tac ab(3)[THEN bspec[where x=z], THEN conjunct1])          unfolding kle_def          apply (erule exE)          done        then show "kle (n + 1) c z"          unfolding kle_def          apply (rule_tac x="insert (n + 1) k" in exI)          unfolding c_def          using ab          using rs(5)[rule_format,OF ab(1),of "n + 1"] assms(1)          apply auto          done      next        case True        then show ?thesis by auto      qed    } note * = this    fix y    assume y: "y ∈ insert c f"    show "kle (n + 1) x y ∨ kle (n + 1) y x"    proof (cases "x = c ∨ y = c")      case False      then have **: "x ∈ f" "y ∈ f"        using x y by auto      show ?thesis        using rs(6)[rule_format,OF **]        by (auto dest: kle_Suc)    qed (insert * x y, auto)  qed (insert rs, auto)qedlemma ksimplex_fix_plane:  fixes a a0 a1 :: "nat => nat"  assumes "a ∈ s"    and "j ∈ {1..n}"    and "∀x∈s - {a}. x j = q"    and "a0 ∈ s"    and "a1 ∈ s"    and "∀i. a1 i = (if i ∈ {1..n} then a0 i + 1 else a0 i)"  shows "a = a0 ∨ a = a1"proof -  have *: "!!P A x y. ∀x∈A. P x ==> x∈A ==> y∈A ==> P x ∧ P y"    by auto  show ?thesis    apply (rule ccontr)    using *[OF assms(3), of a0 a1]    unfolding assms(6)[THEN spec[where x=j]]    using assms(1-2,4-5)    apply auto    doneqedlemma ksimplex_fix_plane_0:  fixes a a0 a1 :: "nat => nat"  assumes "a ∈ s"    and "j ∈ {1..n}"    and "∀x∈s - {a}. x j = 0"    and "a0 ∈ s"    and "a1 ∈ s"    and "∀i. a1 i = (if i∈{1..n} then a0 i + 1 else a0 i)"  shows "a = a1"    apply (rule ccontr)    using ksimplex_fix_plane[OF assms]    using assms(3)[THEN bspec[where x=a1]]    using assms(2,5)    unfolding assms(6)[THEN spec[where x=j]]    apply simp    donelemma ksimplex_fix_plane_p:  assumes "ksimplex p n s"    and "a ∈ s"    and "j ∈ {1..n}"    and "∀x∈s - {a}. x j = p"    and "a0 ∈ s"    and "a1 ∈ s"    and "∀i. a1 i = (if i∈{1..n} then a0 i + 1 else a0 i)"  shows "a = a0"proof (rule ccontr)  note s = ksimplexD[OF assms(1),rule_format]  assume as: "¬ ?thesis"  then have *: "a0 ∈ s - {a}"    using assms(5) by auto  then have "a1 = a"    using ksimplex_fix_plane[OF assms(2-)] by auto  then show False    using as and assms(3,5) and assms(7)[rule_format,of j]    unfolding assms(4)[rule_format,OF *]    using s(4)[OF assms(6), of j]    by autoqedlemma ksimplex_replace_0:  assumes "ksimplex p n s" "a ∈ s"    and "n ≠ 0"    and "j ∈ {1..n}"    and "∀x∈s - {a}. x j = 0"  shows "card {s'. ksimplex p n s' ∧ (∃b∈s'. s' - {b} = s - {a})} = 1"proof -  have *: "!!s' a a'. s' - {a'} = s - {a} ==> a' = a ==> a' ∈ s' ==> a ∈ s ==> s' = s"    by auto  have **: "!!s' a'. ksimplex p n s' ==> a' ∈ s' ==> s' - {a'} = s - {a} ==> s' = s"  proof -    case goal1    guess a0 a1 by (rule ksimplex_extrema_strong[OF assms(1,3)]) note exta = this[rule_format]    have a: "a = a1"      apply (rule ksimplex_fix_plane_0[OF assms(2,4-5)])      using exta(1-2,5)      apply auto      done    moreover    guess b0 b1 by (rule ksimplex_extrema_strong[OF goal1(1) assms(3)])    note extb = this[rule_format]    have a': "a' = b1"      apply (rule ksimplex_fix_plane_0[OF goal1(2) assms(4), of b0])      unfolding goal1(3)      using assms extb goal1      apply auto      done    moreover    have "b0 = a0"      unfolding kle_antisym[symmetric, of b0 a0 n]      using exta extb and goal1(3)      unfolding a a' by blast    then have "b1 = a1"      apply -      apply (rule ext)      unfolding exta(5) extb(5)      apply auto      done    ultimately    show "s' = s"      apply -      apply (rule *[of _ a1 b1])      using exta(1-2) extb(1-2) goal1      apply auto      done  qed  show ?thesis    unfolding card_1_exists    apply -    apply(rule ex1I[of _ s])    unfolding mem_Collect_eq    defer    apply (erule conjE bexE)+    apply (rule_tac a'=b in **)    using assms(1,2)    apply auto    doneqedlemma ksimplex_replace_1:  assumes "ksimplex p n s"    and "a ∈ s"    and "n ≠ 0"    and "j ∈ {1..n}"    and "∀x∈s - {a}. x j = p"  shows "card {s'. ksimplex p n s' ∧ (∃b∈s'. s' - {b} = s - {a})} = 1"proof -  have lem: "!!a a' s'. s' - {a'} = s - {a} ==> a' = a ==> a' ∈ s' ==> a ∈ s ==> s' = s"    by auto  have lem: "!!s' a'. ksimplex p n s' ==> a'∈s' ==> s' - {a'} = s - {a} ==> s' = s"  proof -    case goal1    guess a0 a1 by (rule ksimplex_extrema_strong[OF assms(1,3)]) note exta = this [rule_format]    have a: "a = a0"      apply (rule ksimplex_fix_plane_p[OF assms(1-2,4-5) exta(1,2)])      unfolding exta      apply auto      done    moreover    guess b0 b1 by (rule ksimplex_extrema_strong[OF goal1(1) assms(3)])    note extb = this [rule_format]    have a': "a' = b0"      apply (rule ksimplex_fix_plane_p[OF goal1(1-2) assms(4), of _ b1])      unfolding goal1 extb      using extb(1,2) assms(5)      apply auto      done    moreover    have *: "b1 = a1"      unfolding kle_antisym[symmetric, of b1 a1 n]      using exta extb      using goal1(3)      unfolding a a'      by blast    moreover    have "a0 = b0"    proof (rule ext)      fix x      show "a0 x = b0 x"        using *[THEN cong, of x x]        unfolding exta extb        by (cases "x ∈ {1..n}") auto    qed    ultimately    show "s' = s"      apply -      apply (rule lem[OF goal1(3) _ goal1(2) assms(2)])      apply auto      done  qed  show ?thesis    unfolding card_1_exists    apply (rule ex1I[of _ s])    unfolding mem_Collect_eq    apply rule    apply (rule assms(1))    apply (rule_tac x = a in bexI)    prefer 3    apply (erule conjE bexE)+    apply (rule_tac a'=b in lem)    using assms(1-2)    apply auto    doneqedlemma ksimplex_replace_2:  assumes "ksimplex p n s"    and "a ∈ s"    and "n ≠ 0"    and "¬ (∃j∈{1..n}. ∀x∈s - {a}. x j = 0)"    and "¬ (∃j∈{1..n}. ∀x∈s - {a}. x j = p)"  shows "card {s'. ksimplex p n s' ∧ (∃b∈s'. s' - {b} = s - {a})} = 2"    (is "card ?A = 2")proof -  have lem1: "!!a a' s s'. s' - {a'} = s - {a} ==> a' = a ==> a' ∈ s' ==> a ∈ s ==> s' = s"    by auto  have lem2: "!!a b. a ∈ s ==> b ≠ a ==> s ≠ insert b (s - {a})"  proof    case goal1    then have "a ∈ insert b (s - {a})"      by auto    then have "a ∈ s - {a}"      unfolding insert_iff      using goal1      by auto    then show False      by auto  qed  guess a0 a1 by (rule ksimplex_extrema_strong[OF assms(1,3)]) note a0a1 = this  {    assume "a = a0"    have *: "!!P Q. P ∨ Q ==> ¬ P ==> Q"      by auto    have "∃x∈s. ¬ kle n x a0"      apply (rule_tac x=a1 in bexI)    proof      assume as: "kle n a1 a0"      show False        using kle_imp_pointwise[OF as,THEN spec[where x=1]]        unfolding a0a1(5)[THEN spec[where x=1]]        using assms(3)        by auto    qed (insert a0a1, auto)    then have "∃y∈s. ∃k∈{1..n}. ∀j. y j = (if j = k then a0 j + 1 else a0 j)"      apply (rule_tac *[OF ksimplex_successor[OF assms(1-2),unfolded `a=a0`]])      apply auto      done    then guess a2 ..    from this(2) guess k .. note k = this note a2 =`a2 ∈ s`    def a3 ≡ "λj. if j = k then a1 j + 1 else a1 j"    have "a3 ∉ s"    proof      assume "a3∈s"      then have "kle n a3 a1"        using a0a1(4) by auto      then show False        apply (drule_tac kle_imp_pointwise)        unfolding a3_def        apply (erule_tac x = k in allE)        apply auto        done    qed    then have "a3 ≠ a0" and "a3 ≠ a1"      using a0a1 by auto    have "a2 ≠ a0"      using k(2)[THEN spec[where x=k]] by auto    have lem3: "!!x. x ∈ (s - {a0}) ==> kle n a2 x"    proof (rule ccontr)      case goal1      then have as: "x ∈ s" "x ≠ a0"        by auto      have "kle n a2 x ∨ kle n x a2"        using ksimplexD(6)[OF assms(1)] and as `a2 ∈ s`        by auto      moreover      have "kle n a0 x"        using a0a1(4) as by auto      ultimately have "x = a0 ∨ x = a2"        apply -        apply (rule kle_adjacent[OF k(2)])        using goal1(2)        apply auto        done      then have "x = a2"        using as by auto      then show False        using goal1(2)        using kle_refl        by auto    qed    let ?s = "insert a3 (s - {a0})"    have "ksimplex p n ?s"      apply (rule ksimplexI)      apply (rule_tac[2-] ballI)      apply (rule_tac[4] ballI)    proof -      show "card ?s = n + 1"        using ksimplexD(2-3)[OF assms(1)]        using `a3 ≠ a0` `a3 ∉ s` `a0 ∈ s`        by (auto simp add: card_insert_if)      fix x      assume x: "x ∈ insert a3 (s - {a0})"      show "∀j. x j ≤ p"      proof        fix j        show "x j ≤ p"        proof (cases "x = a3")          case False          then show ?thesis            using x ksimplexD(4)[OF assms(1)] by auto        next          case True          show ?thesis unfolding True          proof (cases "j = k")            case False            then show "a3 j ≤ p"              unfolding True a3_def              using `a1 ∈ s` ksimplexD(4)[OF assms(1)]              by auto          next            guess a4 using assms(5)[unfolded bex_simps ball_simps,rule_format,OF k(1)] ..            note a4 = this            have "a2 k ≤ a4 k"              using lem3[OF a4(1)[unfolded `a = a0`],THEN kle_imp_pointwise]              by auto            also have "… < p"              using ksimplexD(4)[OF assms(1),rule_format,of a4 k]              using a4 by auto            finally have *: "a0 k + 1 < p"              unfolding k(2)[rule_format]              by auto            case True            then show "a3 j ≤p"              unfolding a3_def              unfolding a0a1(5)[rule_format]              using k(1) k(2)assms(5)              using *              by simp          qed        qed      qed      show "∀j. j ∉ {1..n} --> x j = p"      proof (rule, rule)        fix j :: nat        assume j: "j ∉ {1..n}"        show "x j = p"        proof (cases "x = a3")          case False          then show ?thesis            using j x ksimplexD(5)[OF assms(1)]            by auto        next          case True          show ?thesis            unfolding True a3_def            using j k(1)            using ksimplexD(5)[OF assms(1),rule_format,OF `a1∈s` j]            by auto        qed      qed      fix y      assume y: "y ∈ insert a3 (s - {a0})"      have lem4: "!!x. x∈s ==> x ≠ a0 ==> kle n x a3"      proof -        case goal1        guess kk using a0a1(4)[rule_format, OF `x∈s`,THEN conjunct2,unfolded kle_def]          by (elim exE conjE)        note kk = this        have "k ∉ kk"        proof          assume "k ∈ kk"          then have "a1 k = x k + 1"            using kk by auto          then have "a0 k = x k"            unfolding a0a1(5)[rule_format] using k(1) by auto          then have "a2 k = x k + 1"            unfolding k(2)[rule_format] by auto          moreover          have "a2 k ≤ x k"            using lem3[of x,THEN kle_imp_pointwise] goal1 by auto          ultimately show False            by auto        qed        then show ?case          unfolding kle_def          apply (rule_tac x="insert k kk" in exI)          using kk(1)          unfolding a3_def kle_def kk(2)[rule_format]          using k(1)          apply auto          done      qed      show "kle n x y ∨ kle n y x"      proof (cases "y = a3")        case True        show ?thesis          unfolding True          apply (cases "x = a3")          defer          apply (rule disjI1, rule lem4)          using x          apply auto          done      next        case False        show ?thesis        proof (cases "x = a3")          case True          show ?thesis            unfolding True            apply (rule disjI2)            apply (rule lem4)            using y False            apply auto            done        next          case False          then show ?thesis            apply (rule_tac ksimplexD(6)[OF assms(1),rule_format])            using x y `y ≠ a3`            apply auto            done        qed      qed    qed    then have "insert a3 (s - {a0}) ∈ ?A"      unfolding mem_Collect_eq      apply -      apply rule      apply assumption      apply (rule_tac x = "a3" in bexI)      unfolding `a = a0`      using `a3 ∉ s`      apply auto      done    moreover    have "s ∈ ?A"      using assms(1,2) by auto    ultimately have "?A ⊇ {s, insert a3 (s - {a0})}"      by auto    moreover    have "?A ⊆ {s, insert a3 (s - {a0})}"      apply rule      unfolding mem_Collect_eq    proof (erule conjE)      fix s'      assume as: "ksimplex p n s'" and "∃b∈s'. s' - {b} = s - {a}"      from this(2) guess a' .. note a' = this      guess a_min a_max by (rule ksimplex_extrema_strong[OF as assms(3)]) note min_max = this      have *: "∀x∈s' - {a'}. x k = a2 k"        unfolding a'      proof        fix x        assume x: "x ∈ s - {a}"        then have "kle n a2 x"          apply -          apply (rule lem3)          using `a = a0`          apply auto          done        then have "a2 k ≤ x k"          apply (drule_tac kle_imp_pointwise)          apply auto          done        moreover        have "x k ≤ a2 k"          unfolding k(2)[rule_format]          using a0a1(4)[rule_format,of x, THEN conjunct1]          unfolding kle_def using x          by auto        ultimately show "x k = a2 k"        by auto      qed      have **: "a' = a_min ∨ a' = a_max"        apply (rule ksimplex_fix_plane[OF a'(1) k(1) *])        using min_max        apply auto        done      show "s' ∈ {s, insert a3 (s - {a0})}"      proof (cases "a' = a_min")        case True        have "a_max = a1"          unfolding kle_antisym[symmetric,of a_max a1 n]          apply rule          apply (rule a0a1(4)[rule_format,THEN conjunct2])          defer        proof (rule min_max(4)[rule_format,THEN conjunct2])          show "a1 ∈ s'"            using a'            unfolding `a = a0`            using a0a1            by auto          show "a_max ∈ s"          proof (rule ccontr)            assume "¬ ?thesis"            then have "a_max = a'"              using a' min_max by auto            then show False              unfolding True using min_max by auto          qed        qed        then have "∀i. a_max i = a1 i"          by auto        then have "a' = a"          unfolding True `a = a0`          apply -          apply (subst fun_eq_iff)          apply rule          apply (erule_tac x=x in allE)          unfolding a0a1(5)[rule_format] min_max(5)[rule_format]        proof -          case goal1          then show ?case            by (cases "x ∈ {1..n}") auto        qed        then have "s' = s"          apply -          apply (rule lem1[OF a'(2)])          using `a ∈ s` `a' ∈ s'`          apply auto          done        then show ?thesis          by auto      next        case False        then have as: "a' = a_max"          using ** by auto        have "a_min = a2"          unfolding kle_antisym[symmetric, of _ _ n]          apply rule          apply (rule min_max(4)[rule_format,THEN conjunct1])          defer        proof (rule lem3)          show "a_min ∈ s - {a0}"            unfolding a'(2)[symmetric,unfolded `a = a0`]            unfolding as            using min_max(1-3)            by auto          have "a2 ≠ a"            unfolding `a = a0`            using k(2)[rule_format,of k]            by auto          then have "a2 ∈ s - {a}"            using a2 by auto          then show "a2 ∈ s'"            unfolding a'(2)[symmetric] by auto        qed        then have "∀i. a_min i = a2 i"          by auto        then have "a' = a3"          unfolding as `a = a0`          apply (subst fun_eq_iff)          apply rule          apply (erule_tac x=x in allE)          unfolding a0a1(5)[rule_format] min_max(5)[rule_format]          unfolding a3_def k(2)[rule_format]          unfolding a0a1(5)[rule_format]        proof -          case goal1          show ?case            unfolding goal1            apply (cases "x ∈ {1..n}")            defer            apply (cases "x = k")            using `k ∈ {1..n}`            apply auto            done        qed        then have "s' = insert a3 (s - {a0})"          apply -          apply (rule lem1)          defer          apply assumption          apply (rule a'(1))          unfolding a' `a = a0`          using `a3 ∉ s`          apply auto          done        then show ?thesis by auto      qed    qed    ultimately have *: "?A = {s, insert a3 (s - {a0})}"      by blast    have "s ≠ insert a3 (s - {a0})"      using `a3 ∉ s` by auto    then have ?thesis      unfolding * by auto  }  moreover  {    assume "a = a1"    have *: "!!P Q. P ∨ Q ==> ¬ P ==> Q"      by auto    have "∃x∈s. ¬ kle n a1 x"      apply (rule_tac x=a0 in bexI)    proof      assume as: "kle n a1 a0"      show False        using kle_imp_pointwise[OF as,THEN spec[where x=1]]        unfolding a0a1(5)[THEN spec[where x=1]]        using assms(3)        by auto    qed (insert a0a1, auto)    then have "∃y∈s. ∃k∈{1..n}. ∀j. a1 j = (if j = k then y j + 1 else y j)"      apply (rule_tac *[OF ksimplex_predecessor[OF assms(1-2),unfolded `a=a1`]])      apply auto      done    then guess a2 .. from this(2) guess k .. note k=this note a2 = `a2 ∈ s`    def a3 ≡ "λj. if j = k then a0 j - 1 else a0 j"    have "a2 ≠ a1"      using k(2)[THEN spec[where x=k]] by auto    have lem3: "!!x. x ∈ s - {a1} ==> kle n x a2"    proof (rule ccontr)      case goal1      then have as: "x ∈ s" "x ≠ a1" by auto      have "kle n a2 x ∨ kle n x a2"        using ksimplexD(6)[OF assms(1)] and as `a2∈s`        by auto      moreover      have "kle n x a1"        using a0a1(4) as by auto      ultimately have "x = a2 ∨ x = a1"        apply -        apply (rule kle_adjacent[OF k(2)])        using goal1(2)        apply auto        done      then have "x = a2"        using as by auto      then show False        using goal1(2) using kle_refl by auto    qed    have "a0 k ≠ 0"    proof -      guess a4 using assms(4)[unfolded bex_simps ball_simps,rule_format,OF `k∈{1..n}`] ..      note a4 = this      have "a4 k ≤ a2 k"        using lem3[OF a4(1)[unfolded `a=a1`],THEN kle_imp_pointwise]        by auto      moreover have "a4 k > 0"        using a4 by auto      ultimately have "a2 k > 0"        by auto      then have "a1 k > 1"        unfolding k(2)[rule_format] by simp      then show ?thesis        unfolding a0a1(5)[rule_format] using k(1) by simp    qed    then have lem4: "∀j. a0 j = (if j = k then a3 j + 1 else a3 j)"      unfolding a3_def by simp    have "¬ kle n a0 a3"      apply (rule notI)      apply (drule kle_imp_pointwise)      unfolding lem4[rule_format]      apply (erule_tac x=k in allE)      apply auto      done    then have "a3 ∉ s"      using a0a1(4) by auto    then have "a3 ≠ a1" "a3 ≠ a0"      using a0a1 by auto    let ?s = "insert a3 (s - {a1})"    have "ksimplex p n ?s"      apply (rule ksimplexI)    proof (rule_tac[2-] ballI,rule_tac[4] ballI)      show "card ?s = n+1"        using ksimplexD(2-3)[OF assms(1)]        using `a3 ≠ a0` `a3 ∉ s` `a1 ∈ s`        by (auto simp add:card_insert_if)      fix x      assume x: "x ∈ insert a3 (s - {a1})"      show "∀j. x j ≤ p"      proof        fix j        show "x j ≤ p"        proof (cases "x = a3")          case False          then show ?thesis            using x ksimplexD(4)[OF assms(1)] by auto        next          case True          show ?thesis            unfolding True          proof (cases "j = k")            case False            then show "a3 j ≤ p"              unfolding True a3_def              using `a0 ∈ s` ksimplexD(4)[OF assms(1)]              by auto          next            guess a4 using assms(5)[unfolded bex_simps ball_simps,rule_format,OF k(1)] ..            note a4 = this            case True have "a3 k ≤ a0 k"              unfolding lem4[rule_format] by auto            also have "… ≤ p"              using ksimplexD(4)[OF assms(1),rule_format, of a0 k] a0a1              by auto            finally show "a3 j ≤ p"              unfolding True by auto          qed        qed      qed      show "∀j. j ∉ {1..n} --> x j = p"      proof (rule, rule)        fix j :: nat        assume j: "j ∉ {1..n}"        show "x j = p"        proof (cases "x = a3")          case False          then show ?thesis            using j x ksimplexD(5)[OF assms(1)] by auto        next          case True          show ?thesis            unfolding True a3_def            using j k(1)            using ksimplexD(5)[OF assms(1),rule_format,OF `a0∈s` j]            by auto        qed      qed      fix y      assume y: "y ∈ insert a3 (s - {a1})"      have lem4: "!!x. x ∈ s ==> x ≠ a1 ==> kle n a3 x"      proof -        case goal1        then have *: "x∈s - {a1}"          by auto        have "kle n a3 a2"        proof -          have "kle n a0 a1"            using a0a1 by auto then guess kk unfolding kle_def ..          then show ?thesis            unfolding kle_def            apply (rule_tac x=kk in exI)            unfolding lem4[rule_format] k(2)[rule_format]            apply rule            defer          proof rule            case goal1            then show ?case              apply -              apply (erule conjE)              apply (erule_tac[!] x=j in allE)              apply (cases "j ∈ kk")              apply (case_tac[!] "j=k")              apply auto              done          qed auto        qed        moreover        have "kle n a3 a0"          unfolding kle_def lem4[rule_format]          apply (rule_tac x="{k}" in exI)          using k(1)          apply auto          done        ultimately        show ?case          apply -          apply (rule kle_between_l[of _ a0 _ a2])          using lem3[OF *]          using a0a1(4)[rule_format,OF goal1(1)]          apply auto          done      qed      show "kle n x y ∨ kle n y x"      proof (cases "y = a3")        case True        show ?thesis          unfolding True          apply (cases "x = a3")          defer          apply (rule disjI2)          apply (rule lem4)          using x          apply auto          done      next        case False        show ?thesis        proof (cases "x = a3")          case True          show ?thesis            unfolding True            apply (rule disjI1)            apply (rule lem4)            using y False            apply auto            done        next          case False          then show ?thesis            apply (rule_tac ksimplexD(6)[OF assms(1),rule_format])            using x y `y ≠ a3`            apply auto            done        qed      qed    qed    then have "insert a3 (s - {a1}) ∈ ?A"      unfolding mem_Collect_eq        apply -        apply (rule, assumption)        apply (rule_tac x = "a3" in bexI)        unfolding `a = a1`        using `a3 ∉ s`        apply auto        done    moreover    have "s ∈ ?A"      using assms(1,2) by auto    ultimately have "?A ⊇ {s, insert a3 (s - {a1})}"      by auto    moreover have "?A ⊆ {s, insert a3 (s - {a1})}"      apply rule      unfolding mem_Collect_eq    proof (erule conjE)      fix s'      assume as: "ksimplex p n s'" and "∃b∈s'. s' - {b} = s - {a}"      from this(2) guess a' .. note a' = this      guess a_min a_max by (rule ksimplex_extrema_strong[OF as assms(3)]) note min_max = this      have *: "∀x∈s' - {a'}. x k = a2 k" unfolding a'      proof        fix x        assume x: "x ∈ s - {a}"        then have "kle n x a2"          apply -          apply (rule lem3)          using `a = a1`          apply auto          done        then have "x k ≤ a2 k"          apply (drule_tac kle_imp_pointwise)          apply auto          done        moreover        {          have "a2 k ≤ a0 k"            using k(2)[rule_format,of k]            unfolding a0a1(5)[rule_format]            using k(1)            by simp          also have "… ≤ x k"            using a0a1(4)[rule_format,of x,THEN conjunct1,THEN kle_imp_pointwise] x            by auto          finally have "a2 k ≤ x k" .        }        ultimately show "x k = a2 k"          by auto      qed      have **: "a' = a_min ∨ a' = a_max"        apply (rule ksimplex_fix_plane[OF a'(1) k(1) *])        using min_max        apply auto        done      have "a2 ≠ a1"      proof        assume as: "a2 = a1"        show False          using k(2)          unfolding as          apply (erule_tac x = k in allE)          apply auto          done      qed      then have a2': "a2 ∈ s' - {a'}"        unfolding a'        using a2        unfolding `a = a1`        by auto      show "s' ∈ {s, insert a3 (s - {a1})}"      proof (cases "a' = a_min")        case True        have "a_max ∈ s - {a1}"          using min_max          unfolding a'(2)[unfolded `a=a1`,symmetric] True          by auto        then have "a_max = a2"          unfolding kle_antisym[symmetric,of a_max a2 n]          apply -          apply rule          apply (rule lem3)          apply assumption          apply (rule min_max(4)[rule_format,THEN conjunct2])          using a2'          apply auto          done        then have a_max: "∀i. a_max i = a2 i"          by auto        have *: "∀j. a2 j = (if j ∈ {1..n} then a3 j + 1 else a3 j)"          using k(2)          unfolding lem4[rule_format] a0a1(5)[rule_format]          apply -          apply rule          apply (erule_tac x=j in allE)        proof -          case goal1          then show ?case by (cases "j ∈ {1..n}", case_tac[!] "j = k") auto        qed        have "∀i. a_min i = a3 i"          using a_max            apply -            apply rule            apply (erule_tac x=i in allE)            unfolding min_max(5)[rule_format] *[rule_format]        proof -          case goal1          then show ?case            by (cases "i ∈ {1..n}") auto        qed        then have "a_min = a3"          unfolding fun_eq_iff .        then have "s' = insert a3 (s - {a1})"          using a'          unfolding `a = a1` True          by auto        then show ?thesis          by auto      next        case False        then have as: "a' = a_max"          using ** by auto        have "a_min = a0"          unfolding kle_antisym[symmetric,of _ _ n]          apply rule          apply (rule min_max(4)[rule_format,THEN conjunct1])          defer          apply (rule a0a1(4)[rule_format,THEN conjunct1])        proof -          have "a_min ∈ s - {a1}"            using min_max(1,3)            unfolding a'(2)[symmetric,unfolded `a=a1`] as            by auto          then show "a_min ∈ s"            by auto          have "a0 ∈ s - {a1}"            using a0a1(1-3) by auto          then show "a0 ∈ s'"            unfolding a'(2)[symmetric,unfolded `a=a1`]            by auto        qed        then have "∀i. a_max i = a1 i"          unfolding a0a1(5)[rule_format] min_max(5)[rule_format]          by auto        then have "s' = s"          apply -          apply (rule lem1[OF a'(2)])          using `a ∈ s` `a' ∈ s'`          unfolding as `a = a1`          unfolding fun_eq_iff          apply auto          done        then show ?thesis          by auto      qed    qed    ultimately have *: "?A = {s, insert a3 (s - {a1})}"      by blast    have "s ≠ insert a3 (s - {a1})"      using `a3∉s` by auto    then have ?thesis      unfolding * by auto  }  moreover  {    assume as: "a ≠ a0" "a ≠ a1"    have "¬ (∀x∈s. kle n a x)"    proof      case goal1      have "a = a0"        unfolding kle_antisym[symmetric,of _ _ n]        apply rule        using goal1 a0a1 assms(2)        apply auto        done      then show False        using as by auto    qed    then have "∃y∈s. ∃k∈{1..n}. ∀j. a j = (if j = k then y j + 1 else y j)"      using ksimplex_predecessor[OF assms(1-2)]      by blast    then guess u .. from this(2) guess k .. note k = this[rule_format]    note u = `u ∈ s`    have "¬ (∀x∈s. kle n x a)"    proof      case goal1      have "a = a1"        unfolding kle_antisym[symmetric,of _ _ n]        apply rule        using goal1 a0a1 assms(2)        apply auto        done      then show False        using as by auto    qed    then have "∃y∈s. ∃k∈{1..n}. ∀j. y j = (if j = k then a j + 1 else a j)"      using ksimplex_successor[OF assms(1-2)] by blast    then guess v .. from this(2) guess l ..    note l = this[rule_format]    note v = `v ∈ s`    def a' ≡ "λj. if j = l then u j + 1 else u j"    have kl: "k ≠ l"    proof      assume "k = l"      have *: "!!P. (if P then (1::nat) else 0) ≠ 2"        by auto      then show False        using ksimplexD(6)[OF assms(1),rule_format,OF u v]        unfolding kle_def        unfolding l(2) k(2) `k = l`        apply -        apply (erule disjE)        apply (erule_tac[!] exE conjE)+        apply (erule_tac[!] x = l in allE)+        apply (auto simp add: *)        done    qed    then have aa': "a' ≠ a"      apply -      apply rule      unfolding fun_eq_iff      unfolding a'_def k(2)      apply (erule_tac x=l in allE)      apply auto      done    have "a' ∉ s"      apply rule      apply (drule ksimplexD(6)[OF assms(1),rule_format,OF `a∈s`])    proof (cases "kle n a a'")      case goal2      then have "kle n a' a"        by auto      then show False        apply (drule_tac kle_imp_pointwise)        apply (erule_tac x=l in allE)        unfolding a'_def k(2)        using kl        apply auto        done    next      case True      then show False        apply (drule_tac kle_imp_pointwise)        apply (erule_tac x=k in allE)        unfolding a'_def k(2)        using kl        apply auto        done    qed    have kle_uv: "kle n u a" "kle n u a'" "kle n a v" "kle n a' v"      unfolding kle_def      apply -      apply (rule_tac[1] x="{k}" in exI,rule_tac[2] x="{l}" in exI)      apply (rule_tac[3] x="{l}" in exI,rule_tac[4] x="{k}" in exI)      unfolding l(2) k(2) a'_def      using l(1) k(1)      apply auto      done    have uxv: "!!x. kle n u x ==> kle n x v ==> x = u ∨ x = a ∨ x = a' ∨ x = v"    proof -      case goal1      then show ?case      proof (cases "x k = u k", case_tac[!] "x l = u l")        assume as: "x l = u l" "x k = u k"        have "x = u"          unfolding fun_eq_iff          using goal1(2)[THEN kle_imp_pointwise,unfolded l(2)]          unfolding k(2)          apply -          using goal1(1)[THEN kle_imp_pointwise]          apply -          apply rule          apply (erule_tac x=xa in allE)+        proof -          case goal1          then show ?case            apply (cases "x = l")            apply (case_tac[!] "x = k")            using as            by auto        qed        then show ?case          by auto      next        assume as: "x l ≠ u l" "x k = u k"        have "x = a'"          unfolding fun_eq_iff          unfolding a'_def          using goal1(2)[THEN kle_imp_pointwise]          unfolding l(2) k(2)          using goal1(1)[THEN kle_imp_pointwise]          apply -          apply rule          apply (erule_tac x = xa in allE)+        proof -          case goal1          then show ?case            apply (cases "x = l")            apply (case_tac[!] "x = k")            using as            apply auto            done        qed        then show ?case by auto      next        assume as: "x l = u l" "x k ≠ u k"        have "x = a"          unfolding fun_eq_iff          using goal1(2)[THEN kle_imp_pointwise]          unfolding l(2) k(2)          using goal1(1)[THEN kle_imp_pointwise]          apply -          apply rule          apply (erule_tac x=xa in allE)+        proof -          case goal1          then show ?case            apply (cases "x = l")            apply (case_tac[!] "x = k")            using as            apply auto            done        qed        then show ?case          by auto      next        assume as: "x l ≠ u l" "x k ≠ u k"        have "x = v"          unfolding fun_eq_iff          using goal1(2)[THEN kle_imp_pointwise]          unfolding l(2) k(2)          using goal1(1)[THEN kle_imp_pointwise]          apply -          apply rule          apply (erule_tac x=xa in allE)+        proof -          case goal1          then show ?case            apply (cases "x = l")            apply (case_tac[!] "x = k")            using as `k ≠ l`            apply auto            done        qed        then show ?case by auto      qed    qed    have uv: "kle n u v"      apply (rule kle_trans[OF kle_uv(1,3)])      using ksimplexD(6)[OF assms(1)]      using u v      apply auto      done    have lem3: "!!x. x ∈ s ==> kle n v x ==> kle n a' x"      apply (rule kle_between_r[of _ u _ v])      prefer 3      apply (rule kle_trans[OF uv])      defer      apply (rule ksimplexD(6)[OF assms(1), rule_format])      using kle_uv `u ∈ s`      apply auto      done    have lem4: "!!x. x ∈ s ==> kle n x u ==> kle n x a'"      apply (rule kle_between_l[of _ u _ v])      prefer 4      apply (rule kle_trans[OF _ uv])      defer      apply (rule ksimplexD(6)[OF assms(1), rule_format])      using kle_uv `v ∈ s`      apply auto      done    have lem5: "!!x. x ∈ s ==> x ≠ a ==> kle n x a' ∨ kle n a' x"    proof -      case goal1      then show ?case      proof (cases "kle n v x ∨ kle n x u")        case True        then show ?thesis          using goal1 by (auto intro: lem3 lem4)      next        case False        then have *: "kle n u x" "kle n x v"          using ksimplexD(6)[OF assms(1)]          using goal1 `u ∈ s` `v ∈ s`          by auto        show ?thesis          using uxv[OF *]          using kle_uv          using goal1          by auto      qed    qed    have "ksimplex p n (insert a' (s - {a}))"      apply (rule ksimplexI)      apply (rule_tac[2-] ballI)      apply (rule_tac[4] ballI)    proof -      show "card (insert a' (s - {a})) = n + 1"        using ksimplexD(2-3)[OF assms(1)]        using `a' ≠ a` `a' ∉ s` `a ∈ s`        by (auto simp add:card_insert_if)      fix x      assume x: "x ∈ insert a' (s - {a})"      show "∀j. x j ≤ p"      proof        fix j        show "x j ≤ p"        proof (cases "x = a'")          case False          then show ?thesis            using x ksimplexD(4)[OF assms(1)] by auto        next          case True          show ?thesis            unfolding True          proof (cases "j = l")            case False            then show "a' j ≤p"              unfolding True a'_def              using `u∈s` ksimplexD(4)[OF assms(1)]              by auto          next            case True            have *: "a l = u l" "v l = a l + 1"              using k(2)[of l] l(2)[of l] `k ≠ l`              by auto            have "u l + 1 ≤ p"              unfolding *[symmetric]              using ksimplexD(4)[OF assms(1)]              using `v ∈ s`              by auto            then show "a' j ≤p"              unfolding a'_def True              by auto          qed        qed      qed      show "∀j. j ∉ {1..n} --> x j = p"      proof (rule, rule)        fix j :: nat        assume j: "j ∉ {1..n}"        show "x j = p"        proof (cases "x = a'")          case False          then show ?thesis            using j x ksimplexD(5)[OF assms(1)] by auto        next          case True          show ?thesis            unfolding True a'_def            using j l(1)            using ksimplexD(5)[OF assms(1),rule_format,OF `u∈s` j]            by auto        qed      qed      fix y      assume y: "y ∈ insert a' (s - {a})"      show "kle n x y ∨ kle n y x"      proof (cases "y = a'")        case True        show ?thesis          unfolding True          apply (cases "x = a'")          defer          apply (rule lem5)          using x          apply auto          done      next        case False        show ?thesis        proof (cases "x = a'")          case True          show ?thesis            unfolding True            using lem5[of y] using y by auto        next          case False          then show ?thesis            apply (rule_tac ksimplexD(6)[OF assms(1),rule_format])            using x y `y ≠ a'`            apply auto            done        qed      qed    qed    then have "insert a' (s - {a}) ∈ ?A"      unfolding mem_Collect_eq      apply -      apply rule      apply assumption      apply (rule_tac x = "a'" in bexI)      using aa' `a' ∉ s`      apply auto      done    moreover    have "s ∈ ?A"      using assms(1,2) by auto    ultimately have  "?A ⊇ {s, insert a' (s - {a})}"      by auto    moreover    have "?A ⊆ {s, insert a' (s - {a})}"      apply rule      unfolding mem_Collect_eq    proof (erule conjE)      fix s'      assume as: "ksimplex p n s'" and "∃b∈s'. s' - {b} = s - {a}"      from this(2) guess a'' .. note a'' = this      have "u ≠ v"        unfolding fun_eq_iff unfolding l(2) k(2) by auto      then have uv': "¬ kle n v u"        using uv using kle_antisym by auto      have "u ≠ a" "v ≠ a"        unfolding fun_eq_iff k(2) l(2) by auto      then have uvs': "u ∈ s'" "v ∈ s'"        using `u ∈ s` `v ∈ s` using a'' by auto      have lem6: "a ∈ s' ∨ a' ∈ s'"      proof (cases "∀x∈s'. kle n x u ∨ kle n v x")        case False        then guess w unfolding ball_simps .. note w = this        then have "kle n u w" "kle n w v"          using ksimplexD(6)[OF as] uvs' by auto        then have "w = a' ∨ w = a"          using uxv[of w] uvs' w by auto        then show ?thesis          using w by auto      next        case True        have "¬ (∀x∈s'. kle n x u)"          unfolding ball_simps          apply (rule_tac x=v in bexI)          using uv `u ≠ v`          unfolding kle_antisym [of n u v,symmetric]          using `v ∈ s'`          apply auto          done        then have "∃y∈s'. ∃k∈{1..n}. ∀j. y j = (if j = k then u j + 1 else u j)"          using ksimplex_successor[OF as `u∈s'`]          by blast        then guess w .. note w = this        from this(2) guess kk .. note kk = this[rule_format]        have "¬ kle n w u"          apply -          apply rule          apply (drule kle_imp_pointwise)          apply (erule_tac x = kk in allE)          unfolding kk          apply auto          done        then have *: "kle n v w"          using True[rule_format,OF w(1)]          by auto        then have False        proof (cases "kk = l")          case False          then show False using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)]            apply (erule_tac x=l in allE)            using `k ≠ l`            apply auto              done        next          case True          then have "kk ≠ k" using `k ≠ l` by auto          then show False            using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)]            apply (erule_tac x=k in allE)            using `k ≠ l`            apply auto            done        qed        then show ?thesis          by auto      qed      then show "s' ∈ {s, insert a' (s - {a})}"      proof (cases "a ∈ s'")        case True        then have "s' = s"          apply -          apply (rule lem1[OF a''(2)])          using a'' `a ∈ s`          apply auto          done        then show ?thesis          by auto      next        case False        then have "a' ∈ s'"          using lem6 by auto        then have "s' = insert a' (s - {a})"          apply -          apply (rule lem1[of _ a'' _ a'])          unfolding a''(2)[symmetric]          using a'' and `a' ∉ s`          by auto        then show ?thesis          by auto      qed    qed    ultimately have *: "?A = {s, insert a' (s - {a})}"      by blast    have "s ≠ insert a' (s - {a})"      using `a'∉s` by auto    then have ?thesis      unfolding * by auto  }  ultimately show ?thesis    by autoqedtext {* Hence another step towards concreteness. *}lemma kuhn_simplex_lemma:  assumes "∀s. ksimplex p (n + 1) s --> rl ` s ⊆ {0..n+1}"    and "odd (card {f. ∃s a. ksimplex p (n + 1) s ∧ a ∈ s ∧ (f = s - {a}) ∧      rl ` f = {0 .. n} ∧ ((∃j∈{1..n+1}. ∀x∈f. x j = 0) ∨ (∃j∈{1..n+1}. ∀x∈f. x j = p))})"  shows "odd (card {s ∈ {s. ksimplex p (n + 1) s}. rl ` s = {0..n+1}})"proof -  have *: "!!x y. x = y ==> odd (card x) ==> odd (card y)"    by auto  have *: "odd (card {f ∈ {f. ∃s∈{s. ksimplex p (n + 1) s}. (∃a∈s. f = s - {a})}.    rl ` f = {0..n} ∧ ((∃j∈{1..n+1}. ∀x∈f. x j = 0) ∨ (∃j∈{1..n+1}. ∀x∈f. x j = p))})"    apply (rule *[OF _ assms(2)])    apply auto    done  show ?thesis    apply (rule kuhn_complete_lemma[OF finite_simplices])    prefer 6    apply (rule *)    apply rule    apply rule    apply rule    apply (subst ksimplex_def)    defer    apply rule    apply (rule assms(1)[rule_format])    unfolding mem_Collect_eq    apply assumption    apply default+    unfolding mem_Collect_eq    apply (erule disjE bexE)+    defer    apply (erule disjE bexE)+    defer    apply default+    unfolding mem_Collect_eq    apply (erule disjE bexE)+    unfolding mem_Collect_eq  proof -    fix f s a    assume as: "ksimplex p (n + 1) s" "a ∈ s" "f = s - {a}"    let ?S = "{s. ksimplex p (n + 1) s ∧ (∃a∈s. f = s - {a})}"    have S: "?S = {s'. ksimplex p (n + 1) s' ∧ (∃b∈s'. s' - {b} = s - {a})}"      unfolding as by blast    {      fix j      assume j: "j ∈ {1..n + 1}" "∀x∈f. x j = 0"      then show "card {s. ksimplex p (n + 1) s ∧ (∃a∈s. f = s - {a})} = 1"        unfolding S        apply -        apply (rule ksimplex_replace_0)        apply (rule as)+        unfolding as        apply auto        done    }    {      fix j      assume j: "j ∈ {1..n + 1}" "∀x∈f. x j = p"      then show "card {s. ksimplex p (n + 1) s ∧ (∃a∈s. f = s - {a})} = 1"        unfolding S        apply -        apply (rule ksimplex_replace_1)        apply (rule as)+        unfolding as        apply auto        done    }    show "¬ ((∃j∈{1..n+1}. ∀x∈f. x j = 0) ∨ (∃j∈{1..n+1}. ∀x∈f. x j = p)) ==> card ?S = 2"      unfolding S      apply (rule ksimplex_replace_2)      apply (rule as)+      unfolding as      apply auto      done  qed autoqedsubsection {* Reduced labelling *}definition "reduced label (n::nat) (x::nat => nat) =  (SOME k. k ≤ n ∧ (∀i. 1 ≤ i ∧ i < k + 1 --> label x i = 0) ∧    (k = n ∨ label x (k + 1) ≠ (0::nat)))"lemma reduced_labelling:  shows "reduced label n x ≤ n" (is ?t1)    and "∀i. 1 ≤ i ∧ i < reduced label n x + 1 --> label x i = 0" (is ?t2)    and "reduced label n x = n ∨ label x (reduced label n x + 1) ≠ 0"  (is ?t3)proof -  have num_WOP: "!!P k. P (k::nat) ==> ∃n. P n ∧ (∀m<n. ¬ P m)"    apply (drule ex_has_least_nat[where m="λx. x"])    apply (erule exE)    apply (rule_tac x=x in exI)    apply auto    done  have *: "n ≤ n ∧ (label x (n + 1) ≠ 0 ∨ n = n)"    by auto  then guess N    apply (drule_tac num_WOP[of "λj. j≤n ∧ (label x (j+1) ≠ 0 ∨ n = j)"])    apply (erule exE)    done  note N = this  have N': "N ≤ n"    "∀i. 1 ≤ i ∧ i < N + 1 --> label x i = 0" "N = n ∨ label x (N + 1) ≠ 0"    defer  proof (rule, rule)    fix i    assume i: "1 ≤ i ∧ i < N + 1"    then show "label x i = 0"      using N[THEN conjunct2,THEN spec[where x="i - 1"]]      using N      by auto  qed (insert N, auto)  show ?t1 ?t2 ?t3    unfolding reduced_def    apply (rule_tac[!] someI2_ex)    using N'    apply (auto intro!: exI[where x=N])    doneqedlemma reduced_labelling_unique:  fixes x :: "nat => nat"  assumes "r ≤ n"    and "∀i. 1 ≤ i ∧ i < r + 1 --> label x i = 0"    and "r = n ∨ label x (r + 1) ≠ 0"  shows "reduced label n x = r"  apply (rule le_antisym)  apply (rule_tac[!] ccontr)  unfolding not_le  using reduced_labelling[of label n x]  using assms  apply auto  donelemma reduced_labelling_zero:  assumes "j ∈ {1..n}"    and "label x j = 0"  shows "reduced label n x ≠ j - 1"  using reduced_labelling[of label n x]  using assms  by fastforcelemma reduced_labelling_nonzero:  assumes "j∈{1..n}"    and "label x j ≠ 0"  shows "reduced label n x < j"  using assms and reduced_labelling[of label n x]  apply (erule_tac x=j in allE)  apply auto  donelemma reduced_labelling_Suc:  assumes "reduced lab (n + 1) x ≠ n + 1"  shows "reduced lab (n + 1) x = reduced lab n x"  apply (subst eq_commute)  apply (rule reduced_labelling_unique)  using reduced_labelling[of lab "n+1" x] and assms  apply auto  donelemma complete_face_top:  assumes "∀x∈f. ∀j∈{1..n+1}. x j = 0 --> lab x j = 0"    and "∀x∈f. ∀j∈{1..n+1}. x j = p --> lab x j = 1"  shows "reduced lab (n + 1) ` f = {0..n} ∧      ((∃j∈{1..n+1}. ∀x∈f. x j = 0) ∨ (∃j∈{1..n+1}. ∀x∈f. x j = p)) <->    reduced lab (n + 1) ` f = {0..n} ∧ (∀x∈f. x (n + 1) = p)"    (is "?l = ?r")proof  assume ?l (is "?as ∧ (?a ∨ ?b)")  then show ?r    apply -    apply rule    apply (erule conjE)    apply assumption  proof (cases ?a)    case True    then guess j .. note j = this    {      fix x      assume x: "x ∈ f"      have "reduced lab (n + 1) x ≠ j - 1"        using j        apply -        apply (rule reduced_labelling_zero)        defer        apply (rule assms(1)[rule_format])        using x        apply auto        done    }    moreover have "j - 1 ∈ {0..n}"      using j by auto    then guess y unfolding `?l`[THEN conjunct1,symmetric] and image_iff .. note y = this    ultimately have False      by auto    then show "∀x∈f. x (n + 1) = p"      by auto  next    case False    then have ?b using `?l`      by blast    then guess j .. note j = this    {      fix x      assume x: "x ∈ f"      have "reduced lab (n + 1) x < j"        using j        apply -        apply (rule reduced_labelling_nonzero)        using assms(2)[rule_format,of x j] and x        apply auto        done    } note * = this    have "j = n + 1"    proof (rule ccontr)      assume "¬ ?thesis"      then have "j < n + 1"        using j by auto      moreover      have "n ∈ {0..n}"        by auto      then guess y unfolding `?l`[THEN conjunct1,symmetric] image_iff ..      ultimately show False        using *[of y] by auto    qed    then show "∀x∈f. x (n + 1) = p"      using j by auto  qedqed autotext {* Hence we get just about the nice induction. *}lemma kuhn_induction:  assumes "0 < p"    and "∀x. ∀j∈{1..n+1}. (∀j. x j ≤ p) ∧ x j = 0 --> lab x j = 0"    and "∀x. ∀j∈{1..n+1}. (∀j. x j ≤ p) ∧ x j = p --> lab x j = 1"    and "odd (card {f. ksimplex p n f ∧ reduced lab n ` f = {0..n}})"  shows "odd (card {s. ksimplex p (n + 1) s ∧ reduced lab (n + 1) `  s = {0..n+1}})"proof -  have *: "!!s t. odd (card s) ==> s = t ==> odd (card t)"    "!!s f. (!!x. f x ≤ n + 1) ==> f ` s ⊆ {0..n+1}"    by auto  show ?thesis    apply (rule kuhn_simplex_lemma[unfolded mem_Collect_eq])    apply rule    apply rule    apply (rule *)    apply (rule reduced_labelling)    apply (rule *(1)[OF assms(4)])    apply (rule set_eqI)    unfolding mem_Collect_eq    apply rule    apply (erule conjE)    defer    apply rule  proof -    fix f    assume as: "ksimplex p n f" "reduced lab n ` f = {0..n}"    have *: "∀x∈f. ∀j∈{1..n + 1}. x j = 0 --> lab x j = 0"      "∀x∈f. ∀j∈{1..n + 1}. x j = p --> lab x j = 1"      using assms(2-3)      using as(1)[unfolded ksimplex_def]      by auto    have allp: "∀x∈f. x (n + 1) = p"      using assms(2)      using as(1)[unfolded ksimplex_def]      by auto    {      fix x      assume "x ∈ f"      then have "reduced lab (n + 1) x < n + 1"        apply -        apply (rule reduced_labelling_nonzero)        defer        using assms(3)        using as(1)[unfolded ksimplex_def]        apply auto        done      then have "reduced lab (n + 1) x = reduced lab n x"        apply -        apply (rule reduced_labelling_Suc)        using reduced_labelling(1)        apply auto        done    }    then have "reduced lab (n + 1) ` f = {0..n}"      unfolding as(2)[symmetric]      apply -      apply (rule set_eqI)      unfolding image_iff      apply auto      done    moreover guess s using as(1)[unfolded simplex_top_face[OF assms(1) allp,symmetric]] ..    then guess a ..    ultimately show "∃s a. ksimplex p (n + 1) s ∧        a ∈ s ∧ f = s - {a} ∧        reduced lab (n + 1) ` f = {0..n} ∧        ((∃j∈{1..n + 1}. ∀x∈f. x j = 0) ∨ (∃j∈{1..n + 1}. ∀x∈f. x j = p))"      apply (rule_tac x = s in exI)      apply (rule_tac x = a in exI)      unfolding complete_face_top[OF *]      using allp as(1)      apply auto      done  next    fix f    assume as: "∃s a. ksimplex p (n + 1) s ∧      a ∈ s ∧ f = s - {a} ∧ reduced lab (n + 1) ` f = {0..n} ∧      ((∃j∈{1..n + 1}. ∀x∈f. x j = 0) ∨ (∃j∈{1..n + 1}. ∀x∈f. x j = p))"    then guess s ..    then guess a by (elim exE conjE) note sa = this    {      fix x      assume "x ∈ f"      then have "reduced lab (n + 1) x ∈ reduced lab (n + 1) ` f"        by auto      then have "reduced lab (n + 1) x < n + 1"        using sa(4) by auto      then have "reduced lab (n + 1) x = reduced lab n x"        apply -        apply (rule reduced_labelling_Suc)        using reduced_labelling(1)        apply auto        done    }    then show part1: "reduced lab n ` f = {0..n}"      unfolding sa(4)[symmetric]      apply -      apply (rule set_eqI)      unfolding image_iff      apply auto      done    have *: "∀x∈f. x (n + 1) = p"    proof (cases "∃j∈{1..n + 1}. ∀x∈f. x j = 0")      case True      then guess j ..      then have "!!x. x ∈ f ==> reduced lab (n + 1) x ≠ j - 1"        apply -        apply (rule reduced_labelling_zero)        apply assumption        apply (rule assms(2)[rule_format])        using sa(1)[unfolded ksimplex_def]        unfolding sa        apply auto        done      moreover      have "j - 1 ∈ {0..n}"        using `j∈{1..n+1}` by auto      ultimately have False        unfolding sa(4)[symmetric]        unfolding image_iff        by fastforce      then show ?thesis        by auto    next      case False      then have "∃j∈{1..n + 1}. ∀x∈f. x j = p"        using sa(5) by fastforce then guess j .. note j=this      then show ?thesis      proof (cases "j = n + 1")        case False        then have *: "j ∈ {1..n}"          using j by auto        then have "!!x. x ∈ f ==> reduced lab n x < j"          apply (rule reduced_labelling_nonzero)        proof -          fix x          assume "x ∈ f"          then have "lab x j = 1"            apply -            apply (rule assms(3)[rule_format,OF j(1)])            using sa(1)[unfolded ksimplex_def]            using j            unfolding sa            apply auto            done          then show "lab x j ≠ 0"            by auto        qed        moreover have "j ∈ {0..n}"          using * by auto        ultimately have False          unfolding part1[symmetric]          using * unfolding image_iff          by auto        then show ?thesis          by auto      qed auto    qed    then show "ksimplex p n f"      using as      unfolding simplex_top_face[OF assms(1) *,symmetric]      by auto  qedqedlemma kuhn_induction_Suc:  assumes "0 < p"    and "∀x. ∀j∈{1..Suc n}. (∀j. x j ≤ p) ∧ x j = 0 --> lab x j = 0"    and "∀x. ∀j∈{1..Suc n}. (∀j. x j ≤ p) ∧ x j = p --> lab x j = 1"    and "odd (card {f. ksimplex p n f ∧ reduced lab n ` f = {0..n}})"  shows "odd (card {s. ksimplex p (Suc n) s ∧ reduced lab (Suc n) ` s = {0..Suc n}})"  using assms  unfolding Suc_eq_plus1  by (rule kuhn_induction)text {* And so we get the final combinatorial result. *}lemma ksimplex_0: "ksimplex p 0 s <-> s = {(λx. p)}"  (is "?l = ?r")proof  assume l: ?l  guess a using ksimplexD(3)[OF l, unfolded add_0] unfolding card_1_exists .. note a = this  have "a = (λx. p)"    using ksimplexD(5)[OF l, rule_format, OF a(1)]    by rule auto  then show ?r    using a by autonext  assume r: ?r  show ?l    unfolding r ksimplex_eq by autoqedlemma reduce_labelling_zero[simp]: "reduced lab 0 x = 0"  by (rule reduced_labelling_unique) autolemma kuhn_combinatorial:  assumes "0 < p"    and "∀x j. (∀j. x j ≤ p) ∧ 1 ≤ j ∧ j ≤ n ∧ x j = 0 --> lab x j = 0"    and "∀x j. (∀j. x j ≤ p) ∧ 1 ≤ j ∧ j ≤ n  ∧ x j = p --> lab x j = 1"  shows "odd (card {s. ksimplex p n s ∧ reduced lab n ` s = {0..n}})"  using assmsproof (induct n)  let ?M = "λn. {s. ksimplex p n s ∧ reduced lab n ` s = {0..n}}"  {    case 0    have *: "?M 0 = {{λx. p}}"      unfolding ksimplex_0 by auto    show ?case      unfolding * by auto  next    case (Suc n)    have "odd (card (?M n))"      apply (rule Suc(1)[OF Suc(2)])      using Suc(3-)      apply auto      done    then show ?case      apply -      apply (rule kuhn_induction_Suc)      using Suc(2-)      apply auto      done  }qedlemma kuhn_lemma:  fixes n p :: nat  assumes "0 < p"    and "0 < n"    and "∀x. (∀i∈{1..n}. x i ≤ p) --> (∀i∈{1..n}. label x i = (0::nat) ∨ label x i = 1)"    and "∀x. (∀i∈{1..n}. x i ≤ p) --> (∀i∈{1..n}. x i = 0 --> label x i = 0)"    and "∀x. (∀i∈{1..n}. x i ≤ p) --> (∀i∈{1..n}. x i = p --> label x i = 1)"  obtains q where "∀i∈{1..n}. q i < p"    and "∀i∈{1..n}. ∃r s.      (∀j∈{1..n}. q j ≤ r j ∧ r j ≤ q j + 1) ∧      (∀j∈{1..n}. q j ≤ s j ∧ s j ≤ q j + 1) ∧      label r i ≠ label s i"proof -  let ?A = "{s. ksimplex p n s ∧ reduced label n ` s = {0..n}}"  have "n ≠ 0"    using assms by auto  have conjD: "!!P Q. P ∧ Q ==> P" "!!P Q. P ∧ Q ==> Q"    by auto  have "odd (card ?A)"    apply (rule kuhn_combinatorial[of p n label])    using assms    apply auto    done  then have "card ?A ≠ 0"    apply -    apply (rule ccontr)    apply auto    done  then have "?A ≠ {}"    unfolding card_eq_0_iff by auto  then obtain s where "s ∈ ?A"    by auto note s=conjD[OF this[unfolded mem_Collect_eq]]  guess a b by (rule ksimplex_extrema_strong[OF s(1) `n ≠ 0`]) note ab = this  show ?thesis    apply (rule that[of a])    apply (rule_tac[!] ballI)  proof -    fix i    assume "i ∈ {1..n}"    then have "a i + 1 ≤ p"      apply -      apply (rule order_trans[of _ "b i"])      apply (subst ab(5)[THEN spec[where x=i]])      using s(1)[unfolded ksimplex_def]      defer      apply -      apply (erule conjE)+      apply (drule_tac bspec[OF _ ab(2)])+      apply auto      done    then show "a i < p"      by auto  next    case goal2    then have "i ∈ reduced label n ` s"      using s by auto    then guess u unfolding image_iff .. note u = this    from goal2 have "i - 1 ∈ reduced label n ` s"      using s by auto    then guess v unfolding image_iff .. note v = this    show ?case      apply (rule_tac x = u in exI)      apply (rule_tac x = v in exI)      apply (rule conjI)      defer      apply (rule conjI)      defer 2      apply (rule_tac[1-2] ballI)    proof -      show "label u i ≠ label v i"        using reduced_labelling [of label n u] reduced_labelling [of label n v]        unfolding u(2)[symmetric] v(2)[symmetric]        using goal2        apply auto        done      fix j      assume j: "j ∈ {1..n}"      show "a j ≤ u j ∧ u j ≤ a j + 1" and "a j ≤ v j ∧ v j ≤ a j + 1"        using conjD[OF ab(4)[rule_format, OF u(1)]]          and conjD[OF ab(4)[rule_format, OF v(1)]]        apply -        apply (drule_tac[!] kle_imp_pointwise)+        apply (erule_tac[!] x=j in allE)+        unfolding ab(5)[rule_format]        using j        apply auto        done    qed  qedqedsubsection {* The main result for the unit cube *}lemma kuhn_labelling_lemma':  assumes "(∀x::nat=>real. P x --> P (f x))"    and "∀x. P x --> (∀i::nat. Q i --> 0 ≤ x i ∧ x i ≤ 1)"  shows "∃l. (∀x i. l x i ≤ (1::nat)) ∧             (∀x i. P x ∧ Q i ∧ x i = 0 --> l x i = 0) ∧             (∀x i. P x ∧ Q i ∧ x i = 1 --> l x i = 1) ∧             (∀x i. P x ∧ Q i ∧ l x i = 0 --> x i ≤ f x i) ∧             (∀x i. P x ∧ Q i ∧ l x i = 1 --> f x i ≤ x i)"proof -  have and_forall_thm: "!!P Q. (∀x. P x) ∧ (∀x. Q x) <-> (∀x. P x ∧ Q x)"    by auto  have *: "∀x y::real. 0 ≤ x ∧ x ≤ 1 ∧ 0 ≤ y ∧ y ≤ 1 --> x ≠ 1 ∧ x ≤ y ∨ x ≠ 0 ∧ y ≤ x"    by auto  show ?thesis    unfolding and_forall_thm    apply (subst choice_iff[symmetric])+    apply rule    apply rule  proof -    case goal1    let ?R = "λy::nat.      (P x ∧ Q xa ∧ x xa = 0 --> y = 0) ∧      (P x ∧ Q xa ∧ x xa = 1 --> y = 1) ∧      (P x ∧ Q xa ∧ y = 0 --> x xa ≤ (f x) xa) ∧      (P x ∧ Q xa ∧ y = 1 --> (f x) xa ≤ x xa)"    {      assume "P x" and "Q xa"      then have "0 ≤ f x xa ∧ f x xa ≤ 1"        using assms(2)[rule_format,of "f x" xa]        apply (drule_tac assms(1)[rule_format])        apply auto        done    }    then have "?R 0 ∨ ?R 1"      by auto    then show ?case      by auto  qedqedlemma brouwer_cube:  fixes f :: "'a::ordered_euclidean_space => 'a::ordered_euclidean_space"  assumes "continuous_on {0..(∑Basis)} f"    and "f ` {0..(∑Basis)} ⊆ {0..(∑Basis)}"  shows "∃x∈{0..(∑Basis)}. f x = x"proof (rule ccontr)  def n ≡ "DIM('a)"  have n: "1 ≤ n" "0 < n" "n ≠ 0"    unfolding n_def by (auto simp add: Suc_le_eq DIM_positive)  assume "¬ ?thesis"  then have *: "¬ (∃x∈{0..∑Basis}. f x - x = 0)"    by auto  guess d    apply (rule brouwer_compactness_lemma[OF compact_interval _ *])    apply (rule continuous_on_intros assms)+    done  note d = this [rule_format]  have *: "∀x. x ∈ {0..∑Basis} --> f x ∈ {0..∑Basis}"  "∀x. x ∈ {0..(∑Basis)::'a} -->    (∀i∈Basis. True --> 0 ≤ x • i ∧ x • i ≤ 1)"    using assms(2)[unfolded image_subset_iff Ball_def]    unfolding mem_interval by auto  guess label using kuhn_labelling_lemma[OF *] by (elim exE conjE)  note label = this [rule_format]  have lem1: "∀x∈{0..∑Basis}.∀y∈{0..∑Basis}.∀i∈Basis. label x i ≠ label y i -->    abs (f x • i - x • i) ≤ norm (f y - f x) + norm (y - x)"  proof safe    fix x y :: 'a    assume x: "x ∈ {0..∑Basis}"    assume y: "y ∈ {0..∑Basis}"    fix i    assume i: "label x i ≠ label y i" "i ∈ Basis"    have *: "!!x y fx fy :: real. x ≤ fx ∧ fy ≤ y ∨ fx ≤ x ∧ y ≤ fy ==>      abs (fx - x) ≤ abs (fy - fx) + abs (y - x)" by auto    have "¦(f x - x) • i¦ ≤ abs ((f y - f x)•i) + abs ((y - x)•i)"      unfolding inner_simps      apply (rule *)      apply (cases "label x i = 0")      apply (rule disjI1)      apply rule      prefer 3      apply (rule disjI2)      apply rule    proof -      assume lx: "label x i = 0"      then have ly: "label y i = 1"        using i label(1)[of i y]        by auto      show "x • i ≤ f x • i"        apply (rule label(4)[rule_format])        using x y lx i(2)        apply auto        done      show "f y • i ≤ y • i"        apply (rule label(5)[rule_format])        using x y ly i(2)        apply auto        done    next      assume "label x i ≠ 0"      then have l: "label x i = 1" "label y i = 0"        using i label(1)[of i x] label(1)[of i y]        by auto      show "f x • i ≤ x • i"        apply (rule label(5)[rule_format])        using x y l i(2)        apply auto        done      show "y • i ≤ f y • i"        apply (rule label(4)[rule_format])        using x y l i(2)        apply auto        done    qed    also have "… ≤ norm (f y - f x) + norm (y - x)"      apply (rule add_mono)      apply (rule Basis_le_norm[OF i(2)])+      done    finally show "¦f x • i - x • i¦ ≤ norm (f y - f x) + norm (y - x)"      unfolding inner_simps .  qed  have "∃e>0. ∀x∈{0..∑Basis}. ∀y∈{0..∑Basis}. ∀z∈{0..∑Basis}. ∀i∈Basis.    norm (x - z) < e ∧ norm (y - z) < e ∧ label x i ≠ label y i -->      abs ((f(z) - z)•i) < d / (real n)"  proof -    have d': "d / real n / 8 > 0"      apply (rule divide_pos_pos)+      using d(1)      unfolding n_def      apply (auto simp:  DIM_positive)      done    have *: "uniformly_continuous_on {0..∑Basis} f"      by (rule compact_uniformly_continuous[OF assms(1) compact_interval])    guess e using *[unfolded uniformly_continuous_on_def,rule_format,OF d'] by (elim exE conjE)    note e=this[rule_format,unfolded dist_norm]    show ?thesis      apply (rule_tac x="min (e/2) (d/real n/8)" in exI)      apply safe    proof -      show "0 < min (e / 2) (d / real n / 8)"        using d' e by auto      fix x y z i      assume as:        "x ∈ {0..∑Basis}" "y ∈ {0..∑Basis}" "z ∈ {0..∑Basis}"        "norm (x - z) < min (e / 2) (d / real n / 8)"        "norm (y - z) < min (e / 2) (d / real n / 8)"        "label x i ≠ label y i"      assume i: "i ∈ Basis"      have *: "!!z fz x fx n1 n2 n3 n4 d4 d :: real. abs(fx - x) ≤ n1 + n2 ==>        abs (fx - fz) ≤ n3 ==> abs (x - z) ≤ n4 ==>        n1 < d4 ==> n2 < 2 * d4 ==> n3 < d4 ==> n4 < d4 ==>        (8 * d4 = d) ==> abs(fz - z) < d"        by auto      show "¦(f z - z) • i¦ < d / real n"        unfolding inner_simps      proof (rule *)        show "¦f x • i - x • i¦ ≤ norm (f y -f x) + norm (y - x)"          apply (rule lem1[rule_format])          using as i          apply auto          done        show "¦f x • i - f z • i¦ ≤ norm (f x - f z)" "¦x • i - z • i¦ ≤ norm (x - z)"          unfolding inner_diff_left[symmetric]            by (rule Basis_le_norm[OF i])+        have tria: "norm (y - x) ≤ norm (y - z) + norm (x - z)"          using dist_triangle[of y x z, unfolded dist_norm]          unfolding norm_minus_commute          by auto        also have "… < e / 2 + e / 2"          apply (rule add_strict_mono)          using as(4,5)          apply auto          done        finally show "norm (f y - f x) < d / real n / 8"          apply -          apply (rule e(2))          using as          apply auto          done        have "norm (y - z) + norm (x - z) < d / real n / 8 + d / real n / 8"          apply (rule add_strict_mono)          using as          apply auto          done        then show "norm (y - x) < 2 * (d / real n / 8)"          using tria          by auto        show "norm (f x - f z) < d / real n / 8"          apply (rule e(2))          using as e(1)          apply auto          done      qed (insert as, auto)    qed  qed  then guess e by (elim exE conjE) note e=this[rule_format]  guess p using real_arch_simple[of "1 + real n / e"] .. note p=this  have "1 + real n / e > 0"    apply (rule add_pos_pos)    defer    apply (rule divide_pos_pos)    using e(1) n    apply auto    done  then have "p > 0"    using p by auto  obtain b :: "nat => 'a" where b: "bij_betw b {1..n} Basis"    by atomize_elim (auto simp: n_def intro!: finite_same_card_bij)  def b' ≡ "inv_into {1..n} b"  then have b': "bij_betw b' Basis {1..n}"    using bij_betw_inv_into[OF b] by auto  then have b'_Basis: "!!i. i ∈ Basis ==> b' i ∈ {Suc 0 .. n}"    unfolding bij_betw_def by (auto simp: set_eq_iff)  have bb'[simp]:"!!i. i ∈ Basis ==> b (b' i) = i"    unfolding b'_def    using b    by (auto simp: f_inv_into_f bij_betw_def)  have b'b[simp]:"!!i. i ∈ {1..n} ==> b' (b i) = i"    unfolding b'_def    using b    by (auto simp: inv_into_f_eq bij_betw_def)  have *: "!!x :: nat. x = 0 ∨ x = 1 <-> x ≤ 1"    by auto  have b'': "!!j. j ∈ {Suc 0..n} ==> b j ∈ Basis"    using b unfolding bij_betw_def by auto  have q1: "0 < p" "0 < n"  "∀x. (∀i∈{1..n}. x i ≤ p) -->    (∀i∈{1..n}. (label (∑i∈Basis. (real (x (b' i)) / real p) *⇩R i) o b) i = 0 ∨                (label (∑i∈Basis. (real (x (b' i)) / real p) *⇩R i) o b) i = 1)"    unfolding *    using `p > 0` `n > 0`    using label(1)[OF b'']    by auto  have q2: "∀x. (∀i∈{1..n}. x i ≤ p) --> (∀i∈{1..n}. x i = 0 -->      (label (∑i∈Basis. (real (x (b' i)) / real p) *⇩R i) o b) i = 0)"    "∀x. (∀i∈{1..n}. x i ≤ p) --> (∀i∈{1..n}. x i = p -->      (label (∑i∈Basis. (real (x (b' i)) / real p) *⇩R i) o b) i = 1)"    apply rule    apply rule    apply rule    apply rule    defer    apply rule    apply rule    apply rule    apply rule  proof -    fix x i    assume as: "∀i∈{1..n}. x i ≤ p" "i ∈ {1..n}"    {      assume "x i = p ∨ x i = 0"      have "(∑i∈Basis. (real (x (b' i)) / real p) *⇩R i) ∈ {0::'a..∑Basis}"        unfolding mem_interval        using as b'_Basis        by (auto simp add: inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1)    }    note cube = this    {      assume "x i = p"      then show "(label (∑i∈Basis. (real (x (b' i)) / real p) *⇩R i) o b) i = 1"        unfolding o_def        using cube as `p > 0`        by (intro label(3)) (auto simp add: b'')    }    {      assume "x i = 0"      then show "(label (∑i∈Basis. (real (x (b' i)) / real p) *⇩R i) o b) i = 0"        unfolding o_def using cube as `p > 0`        by (intro label(2)) (auto simp add: b'')    }  qed  guess q by (rule kuhn_lemma[OF q1 q2]) note q = this  def z ≡ "(∑i∈Basis. (real (q (b' i)) / real p) *⇩R i)::'a"  have "∃i∈Basis. d / real n ≤ abs ((f z - z)•i)"  proof (rule ccontr)    have "∀i∈Basis. q (b' i) ∈ {0..p}"      using q(1) b'      by (auto intro: less_imp_le simp: bij_betw_def)    then have "z ∈ {0..∑Basis}"      unfolding z_def mem_interval      using b'_Basis      by (auto simp add: inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1)    then have d_fz_z: "d ≤ norm (f z - z)"      by (rule d)    assume "¬ ?thesis"    then have as: "∀i∈Basis. ¦f z • i - z • i¦ < d / real n"      using `n > 0`      by (auto simp add: not_le inner_simps)    have "norm (f z - z) ≤ (∑i∈Basis. ¦f z • i - z • i¦)"      unfolding inner_diff_left[symmetric]      by (rule norm_le_l1)    also have "… < (∑(i::'a) ∈ Basis. d / real n)"      apply (rule setsum_strict_mono)      using as      apply auto      done    also have "… = d"      using DIM_positive[where 'a='a]      by (auto simp: real_eq_of_nat n_def)    finally show False      using d_fz_z by auto  qed  then guess i .. note i = this  have *: "b' i ∈ {1..n}"    using i    using b'[unfolded bij_betw_def]    by auto  guess r using q(2)[rule_format,OF *] ..  then guess s by (elim exE conjE) note rs = this[rule_format]  have b'_im: "!!i. i ∈ Basis ==>  b' i ∈ {1..n}"    using b' unfolding bij_betw_def by auto  def r' ≡ "(∑i∈Basis. (real (r (b' i)) / real p) *⇩R i)::'a"  have "!!i. i ∈ Basis ==> r (b' i) ≤ p"    apply (rule order_trans)    apply (rule rs(1)[OF b'_im,THEN conjunct2])    using q(1)[rule_format,OF b'_im]    apply (auto simp add: Suc_le_eq)    done  then have "r' ∈ {0..∑Basis}"    unfolding r'_def mem_interval    using b'_Basis    by (auto simp add: inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1)  def s' ≡ "(∑i∈Basis. (real (s (b' i)) / real p) *⇩R i)::'a"  have "!!i. i ∈ Basis ==> s (b' i) ≤ p"    apply (rule order_trans)    apply (rule rs(2)[OF b'_im, THEN conjunct2])    using q(1)[rule_format,OF b'_im]    apply (auto simp add: Suc_le_eq)    done  then have "s' ∈ {0..∑Basis}"    unfolding s'_def mem_interval    using b'_Basis    by (auto simp add: inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1)  have "z ∈ {0..∑Basis}"    unfolding z_def mem_interval    using b'_Basis q(1)[rule_format,OF b'_im] `p > 0`    by (auto simp add: inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1 less_imp_le)  have *: "!!x. 1 + real x = real (Suc x)"    by auto  {    have "(∑i∈Basis. ¦real (r (b' i)) - real (q (b' i))¦) ≤ (∑(i::'a)∈Basis. 1)"      apply (rule setsum_mono)      using rs(1)[OF b'_im]      apply (auto simp add:* field_simps)      done    also have "… < e * real p"      using p `e > 0` `p > 0`      by (auto simp add: field_simps n_def real_of_nat_def)    finally have "(∑i∈Basis. ¦real (r (b' i)) - real (q (b' i))¦) < e * real p" .  }  moreover  {    have "(∑i∈Basis. ¦real (s (b' i)) - real (q (b' i))¦) ≤ (∑(i::'a)∈Basis. 1)"      apply (rule setsum_mono)      using rs(2)[OF b'_im]      apply (auto simp add:* field_simps)      done    also have "… < e * real p"      using p `e > 0` `p > 0`      by (auto simp add: field_simps n_def real_of_nat_def)    finally have "(∑i∈Basis. ¦real (s (b' i)) - real (q (b' i))¦) < e * real p" .  }  ultimately  have "norm (r' - z) < e" and "norm (s' - z) < e"    unfolding r'_def s'_def z_def    using `p > 0`    apply (rule_tac[!] le_less_trans[OF norm_le_l1])    apply (auto simp add: field_simps setsum_divide_distrib[symmetric] inner_diff_left)    done  then have "¦(f z - z) • i¦ < d / real n"    using rs(3) i    unfolding r'_def[symmetric] s'_def[symmetric] o_def bb'    by (intro e(2)[OF `r'∈{0..∑Basis}` `s'∈{0..∑Basis}` `z∈{0..∑Basis}`]) auto  then show False    using i by autoqedsubsection {* Retractions *}definition "retraction s t r <-> t ⊆ s ∧ continuous_on s r ∧ r ` s ⊆ t ∧ (∀x∈t. r x = x)"definition retract_of (infixl "retract'_of" 12)  where "(t retract_of s) <-> (∃r. retraction s t r)"lemma retraction_idempotent: "retraction s t r ==> x ∈ s ==>  r (r x) = r x"  unfolding retraction_def by autosubsection {* Preservation of fixpoints under (more general notion of) retraction *}lemma invertible_fixpoint_property:  fixes s :: "'a::euclidean_space set"    and t :: "'b::euclidean_space set"  assumes "continuous_on t i"    and "i ` t ⊆ s"    and "continuous_on s r"    and "r ` s ⊆ t"    and "∀y∈t. r (i y) = y"    and "∀f. continuous_on s f ∧ f ` s ⊆ s --> (∃x∈s. f x = x)"    and "continuous_on t g"    and "g ` t ⊆ t"  obtains y where "y ∈ t" and "g y = y"proof -  have "∃x∈s. (i o g o r) x = x"    apply (rule assms(6)[rule_format])    apply rule    apply (rule continuous_on_compose assms)+    apply ((rule continuous_on_subset)?, rule assms)+    using assms(2,4,8)    unfolding image_compose    apply auto    apply blast    done  then guess x .. note x = this  then have *: "g (r x) ∈ t"    using assms(4,8) by auto  have "r ((i o g o r) x) = r x"    using x by auto  then show ?thesis    apply (rule_tac that[of "r x"])    using x    unfolding o_def    unfolding assms(5)[rule_format,OF *]    using assms(4)    apply auto    doneqedlemma homeomorphic_fixpoint_property:  fixes s :: "'a::euclidean_space set"    and t :: "'b::euclidean_space set"  assumes "s homeomorphic t"  shows "(∀f. continuous_on s f ∧ f ` s ⊆ s --> (∃x∈s. f x = x)) <->    (∀g. continuous_on t g ∧ g ` t ⊆ t --> (∃y∈t. g y = y))"proof -  guess r using assms[unfolded homeomorphic_def homeomorphism_def] ..  then guess i ..  then show ?thesis    apply -    apply rule    apply (rule_tac[!] allI impI)+    apply (rule_tac g=g in invertible_fixpoint_property[of t i s r])    prefer 10    apply (rule_tac g=f in invertible_fixpoint_property[of s r t i])    apply auto    doneqedlemma retract_fixpoint_property:  fixes f :: "'a::euclidean_space => 'b::euclidean_space"    and s :: "'a set"  assumes "t retract_of s"    and "∀f. continuous_on s f ∧ f ` s ⊆ s --> (∃x∈s. f x = x)"    and "continuous_on t g"    and "g ` t ⊆ t"  obtains y where "y ∈ t" and "g y = y"proof -  guess h using assms(1) unfolding retract_of_def ..  then show ?thesis    unfolding retraction_def    apply -    apply (rule invertible_fixpoint_property[OF continuous_on_id _ _ _ _ assms(2), of t h g])    prefer 7    apply (rule_tac y = y in that)    using assms    apply auto    doneqedsubsection {* The Brouwer theorem for any set with nonempty interior *}lemma brouwer_weak:  fixes f :: "'a::ordered_euclidean_space => 'a::ordered_euclidean_space"  assumes "compact s"    and "convex s"    and "interior s ≠ {}"    and "continuous_on s f"    and "f ` s ⊆ s"  obtains x where "x ∈ s" and "f x = x"proof -  have *: "interior {0::'a..∑Basis} ≠ {}"    unfolding interior_closed_interval interval_eq_empty    by auto  have *: "{0::'a..∑Basis} homeomorphic s"    using homeomorphic_convex_compact[OF convex_interval(1) compact_interval * assms(2,1,3)] .  have "∀f. continuous_on {0::'a..∑Basis} f ∧ f ` {0::'a..∑Basis} ⊆ {0::'a..∑Basis} -->    (∃x∈{0::'a..∑Basis}. f x = x)"    using brouwer_cube by auto  then show ?thesis    unfolding homeomorphic_fixpoint_property[OF *]    apply (erule_tac x=f in allE)    apply (erule impE)    defer    apply (erule bexE)    apply (rule_tac x=y in that)    using assms    apply auto    doneqedtext {* And in particular for a closed ball. *}lemma brouwer_ball:  fixes f :: "'a::ordered_euclidean_space => 'a"  assumes "e > 0"    and "continuous_on (cball a e) f"    and "f ` cball a e ⊆ cball a e"  obtains x where "x ∈ 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 autotext {*Still more general form; could derive this directly without using the  rather involved @{text "HOMEOMORPHIC_CONVEX_COMPACT"} theorem, just using  a scaling and translation to put the set inside the unit cube. *}lemma brouwer:  fixes f :: "'a::ordered_euclidean_space => 'a"  assumes "compact s"    and "convex s"    and "s ≠ {}"    and "continuous_on s f"    and "f ` s ⊆ s"  obtains x where "x ∈ s" and "f x = x"proof -  have "∃e>0. s ⊆ cball 0 e"    using compact_imp_bounded[OF assms(1)]    unfolding bounded_pos    apply (erule_tac exE)    apply (rule_tac x=b in exI)    apply (auto simp add: dist_norm)    done  then guess e by (elim exE conjE)  note e = this  have "∃x∈ cball 0 e. (f o closest_point s) x = x"    apply (rule_tac brouwer_ball[OF e(1), of 0 "f o closest_point s"])    apply (rule continuous_on_compose )    apply (rule continuous_on_closest_point[OF assms(2) compact_imp_closed[OF assms(1)] assms(3)])    apply (rule continuous_on_subset[OF assms(4)])    apply (insert closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3)])    defer    using assms(5)[unfolded subset_eq]    using e(2)[unfolded subset_eq mem_cball]    apply (auto simp add: dist_norm)    done  then guess x .. note x=this  have *: "closest_point s x = x"    apply (rule closest_point_self)    apply (rule assms(5)[unfolded subset_eq,THEN bspec[where x="x"], unfolded image_iff])    apply (rule_tac x="closest_point s x" in bexI)    using x    unfolding o_def    using closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3), of x]    apply auto    done  show thesis    apply (rule_tac x="closest_point s x" in that)    unfolding x(2)[unfolded o_def]    apply (rule closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3)])    using *    apply auto    doneqedtext {*So we get the no-retraction theorem. *}lemma no_retraction_cball:  fixes a :: "'a::ordered_euclidean_space"  assumes "e > 0"  shows "¬ (frontier (cball a e) retract_of (cball a e))"proof  case goal1  have *: "!!xa. a - (2 *⇩R a - xa) = - (a - xa)"    using scaleR_left_distrib[of 1 1 a] by auto  guess x    apply (rule retract_fixpoint_property[OF goal1, of "λx. scaleR 2 a - x"])    apply rule    apply rule    apply (erule conjE)    apply (rule brouwer_ball[OF assms])    apply assumption+    apply (rule_tac x=x in bexI)    apply assumption+    apply (rule continuous_on_intros)+    unfolding frontier_cball subset_eq Ball_def image_iff    apply rule    apply rule    apply (erule bexE)    unfolding dist_norm    apply (simp add: * norm_minus_commute)    done  note x = this  then have "scaleR 2 a = scaleR 1 x + scaleR 1 x"    by (auto simp add: algebra_simps)  then have "a = x"    unfolding scaleR_left_distrib[symmetric]    by auto  then show False    using x assms by autoqedsubsection {*Bijections between intervals. *}definition interval_bij :: "'a × 'a => 'a × 'a => 'a => 'a::ordered_euclidean_space"  where "interval_bij =    (λ(a, b) (u, v) x. (∑i∈Basis. (u•i + (x•i - a•i) / (b•i - a•i) * (v•i - u•i)) *⇩R i))"lemma interval_bij_affine:  "interval_bij (a,b) (u,v) = (λx. (∑i∈Basis. ((v•i - u•i) / (b•i - a•i) * (x•i)) *⇩R i) +    (∑i∈Basis. (u•i - (v•i - u•i) / (b•i - a•i) * (a•i)) *⇩R i))"  by (auto simp: setsum_addf[symmetric] scaleR_add_left[symmetric] interval_bij_def fun_eq_iff    field_simps inner_simps add_divide_distrib[symmetric] intro!: setsum_cong)lemma continuous_interval_bij:  fixes a b :: "'a::ordered_euclidean_space"  shows "continuous (at x) (interval_bij (a, b) (u, v))"  by (auto simp add: divide_inverse interval_bij_def intro!: continuous_setsum continuous_intros)lemma continuous_on_interval_bij: "continuous_on s (interval_bij (a, b) (u, v))"  apply(rule continuous_at_imp_continuous_on)  apply (rule, rule continuous_interval_bij)  donelemma in_interval_interval_bij:  fixes a b u v x :: "'a::ordered_euclidean_space"  assumes "x ∈ {a..b}"    and "{u..v} ≠ {}"  shows "interval_bij (a, b) (u, v) x ∈ {u..v}"  apply (simp only: interval_bij_def split_conv mem_interval inner_setsum_left_Basis cong: ball_cong)  apply safeproof -  fix i :: 'a  assume i: "i ∈ Basis"  have "{a..b} ≠ {}"    using assms by auto  with i have *: "a•i ≤ b•i" "u•i ≤ v•i"    using assms(2) by (auto simp add: interval_eq_empty not_less)  have x: "a•i≤x•i" "x•i≤b•i"    using assms(1)[unfolded mem_interval] using i by auto  have "0 ≤ (x • i - a • i) / (b • i - a • i) * (v • i - u • i)"    using * x by (auto intro!: mult_nonneg_nonneg divide_nonneg_nonneg)  then show "u • i ≤ u • i + (x • i - a • i) / (b • i - a • i) * (v • i - u • i)"    using * by auto  have "((x • i - a • i) / (b • i - a • i)) * (v • i - u • i) ≤ 1 * (v • i - u • i)"    apply (rule mult_right_mono)    unfolding divide_le_eq_1    using * x    apply auto    done  then show "u • i + (x • i - a • i) / (b • i - a • i) * (v • i - u • i) ≤ v • i"    using * by autoqedlemma interval_bij_bij:  "∀(i::'a::ordered_euclidean_space)∈Basis. a•i < b•i ∧ u•i < v•i ==>    interval_bij (a, b) (u, v) (interval_bij (u, v) (a, b) x) = x"  by (auto simp: interval_bij_def euclidean_eq_iff[where 'a='a])end`