(* ========================================================================= *)

(* 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                       *)

(* ========================================================================= *)

(* Author:                     John Harrison

   Translation from HOL light: Robert Himmelmann, TU Muenchen *)

header {* Results connected with topological dimension. *}

theory Brouwer_Fixpoint

  imports Convex_Euclidean_Space

begin

lemma brouwer_compactness_lemma:

  assumes "compact s" "continuous_on s f" "\<not> (\<exists>x\<in>s. (f x = (0::_::euclidean_space)))"

  obtains d where "0 < d" "\<forall>x\<in>s. d \<le> norm(f x)" proof(cases "s={}") case False

  have "continuous_on s (norm \<circ> f)" by(rule continuous_on_intros continuous_on_norm assms(2))+

  then obtain x where x:"x\<in>s" "\<forall>y\<in>s. (norm \<circ> f) x \<le> (norm \<circ> f) y"

    using continuous_attains_inf[OF assms(1), of "norm \<circ> f"] and False unfolding o_def by auto

  have "(norm \<circ> f) x > 0" using assms(3) and x(1) by auto

  thus ?thesis apply(rule that) using x(2) unfolding o_def by auto qed(rule that[of 1], auto)

lemma kuhn_labelling_lemma: fixes type::"'a::euclidean_space"

  assumes "(\<forall>x::'a. P x \<longrightarrow> P (f x))"  "\<forall>x. P x \<longrightarrow> (\<forall>i<DIM('a). Q i \<longrightarrow> 0 \<le> x$$i \<and> x$$i \<le> 1)"

  shows "\<exists>l. (\<forall>x.\<forall> i<DIM('a). l x i \<le> (1::nat)) \<and>

             (\<forall>x.\<forall> i<DIM('a). P x \<and> Q i \<and> (x$$i = 0) \<longrightarrow> (l x i = 0)) \<and>

             (\<forall>x.\<forall> i<DIM('a). P x \<and> Q i \<and> (x$$i = 1) \<longrightarrow> (l x i = 1)) \<and>

             (\<forall>x.\<forall> i<DIM('a). P x \<and> Q i \<and> (l x i = 0) \<longrightarrow> x$$i \<le> f(x)$$i) \<and>

             (\<forall>x.\<forall> i<DIM('a). P x \<and> Q i \<and> (l x i = 1) \<longrightarrow> f(x)$$i \<le> x$$i)" proof-

  have and_forall_thm:"\<And>P Q. (\<forall>x. P x) \<and> (\<forall>x. Q x) \<longleftrightarrow> (\<forall>x. P x \<and> Q x)" by auto

  have *:"\<forall>x y::real. 0 \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1 \<longrightarrow> (x \<noteq> 1 \<and> x \<le> y \<or> x \<noteq> 0 \<and> y \<le> x)" by auto

  show ?thesis unfolding and_forall_thm apply(subst choice_iff[THEN sym])+ proof(rule,rule) case goal1

    let ?R = "\<lambda>y. (P x \<and> Q xa \<and> x $$ xa = 0 \<longrightarrow> y = (0::nat)) \<and>

        (P x \<and> Q xa \<and> x $$ xa = 1 \<longrightarrow> y = 1) \<and> (P x \<and> Q xa \<and> y = 0 \<longrightarrow> x $$ xa \<le> f x $$ xa) \<and> (P x \<and> Q xa \<and> y = 1 \<longrightarrow> f x $$ xa \<le> x $$ xa)"

    { assume "P x" "Q xa" "xa<DIM('a)" hence "0 \<le> f x $$ xa \<and> f x $$ xa \<le> 1" using assms(2)[rule_format,of "f x" xa]

        apply(drule_tac assms(1)[rule_format]) by auto }

    hence "xa<DIM('a) \<Longrightarrow> ?R 0 \<or> ?R 1" by auto thus ?case by auto qed qed 

subsection {* The key "counting" observation, somewhat abstracted. *}

lemma setsum_Un_disjoint':assumes "finite A" "finite B" "A \<inter> B = {}" "A \<union> B = C"

  shows "setsum g C = setsum g A + setsum g B"

  using setsum_Un_disjoint[OF assms(1-3)] and assms(4) by auto

lemma kuhn_counting_lemma: assumes "finite faces" "finite simplices"

  "\<forall>f\<in>faces. bnd f  \<longrightarrow> (card {s \<in> simplices. face f s} = 1)"

  "\<forall>f\<in>faces. \<not> bnd f \<longrightarrow> (card {s \<in> simplices. face f s} = 2)"

  "\<forall>s\<in>simplices. compo s  \<longrightarrow> (card {f \<in> faces. face f s \<and> compo' f} = 1)"

  "\<forall>s\<in>simplices. \<not> compo s \<longrightarrow> (card {f \<in> faces. face f s \<and> compo' f} = 0) \<or>

                             (card {f \<in> faces. face f s \<and> compo' f} = 2)"

    "odd(card {f \<in> faces. compo' f \<and> bnd f})"

  shows "odd(card {s \<in> simplices. compo s})" proof-

  have "\<And>x. {f\<in>faces. compo' f \<and> bnd f \<and> face f x} \<union> {f\<in>faces. compo' f \<and> \<not>bnd f \<and> face f x} = {f\<in>faces. compo' f \<and> face f x}"

    "\<And>x. {f \<in> faces. compo' f \<and> bnd f \<and> face f x} \<inter> {f \<in> faces. compo' f \<and> \<not> bnd f \<and> face f x} = {}" by auto

  hence lem1:"setsum (\<lambda>s. (card {f \<in> faces. face f s \<and> compo' f})) simplices =

    setsum (\<lambda>s. card {f \<in> {f \<in> faces. compo' f \<and> bnd f}. face f s}) simplices +

    setsum (\<lambda>s. card {f \<in> {f \<in> faces. compo' f \<and> \<not> (bnd f)}. face f s}) simplices"

    unfolding setsum_addf[THEN sym] apply- apply(rule setsum_cong2)

    using assms(1) by(auto simp add: card_Un_Int, auto simp add:conj_commute)

  have lem2:"setsum (\<lambda>j. card {f \<in> {f \<in> faces. compo' f \<and> bnd f}. face f j}) simplices = 

              1 * card {f \<in> faces. compo' f \<and> bnd f}"

       "setsum (\<lambda>j. card {f \<in> {f \<in> faces. compo' f \<and> \<not> bnd f}. face f j}) simplices = 

              2 * card {f \<in> faces. compo' f \<and> \<not> bnd f}"

    apply(rule_tac[!] setsum_multicount) using assms by auto

  have lem3:"setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) simplices =

    setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices.   compo s}+

    setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices. \<not> compo s}"

    apply(rule setsum_Un_disjoint') using assms(2) by auto

  have lem4:"setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices. compo s}

    = setsum (\<lambda>s. 1) {s \<in> simplices. compo s}"

    apply(rule setsum_cong2) using assms(5) by auto

  have lem5: "setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices. \<not> compo s} =

    setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f})

           {s \<in> simplices. (\<not> compo s) \<and> (card {f \<in> faces. face f s \<and> compo' f} = 0)} +

    setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f})

           {s \<in> simplices. (\<not> compo s) \<and> (card {f \<in> faces. face f s \<and> compo' f} = 2)}"

    apply(rule setsum_Un_disjoint') using assms(2,6) by auto

  have *:"int (\<Sum>s\<in>{s \<in> simplices. compo s}. card {f \<in> faces. face f s \<and> compo' f}) =

    int (card {f \<in> faces. compo' f \<and> bnd f} + 2 * card {f \<in> faces. compo' f \<and> \<not> bnd f}) - 

    int (card {s \<in> simplices. \<not> compo s \<and> card {f \<in> faces. face f s \<and> compo' f} = 2} * 2)"

    using lem1[unfolded lem3 lem2 lem5] by auto

  have even_minus_odd:"\<And>x y. even x \<Longrightarrow> odd (y::int) \<Longrightarrow> odd (x - y)" using assms by auto

  have odd_minus_even:"\<And>x y. odd x \<Longrightarrow> even (y::int) \<Longrightarrow> odd (x - y)" using assms by auto

  show ?thesis unfolding even_nat_def unfolding card_eq_setsum and lem4[THEN sym] and *[unfolded card_eq_setsum]

    unfolding card_eq_setsum[THEN sym] apply (rule odd_minus_even) unfolding zadd_int[THEN sym] apply(rule odd_plus_even)

    apply(rule assms(7)[unfolded even_nat_def]) unfolding int_mult by auto qed

subsection {* The odd/even result for faces of complete vertices, generalized. *}

lemma card_1_exists: "card s = 1 \<longleftrightarrow> (\<exists>!x. x \<in> s)" unfolding One_nat_def

  apply rule apply(drule card_eq_SucD) defer apply(erule ex1E) proof-

  fix x assume as:"x \<in> s" "\<forall>y. y \<in> s \<longrightarrow> y = x"

  have *:"s = insert x {}" apply- apply(rule set_eqI,rule) unfolding singleton_iff

    apply(rule as(2)[rule_format]) using as(1) by auto

  show "card s = Suc 0" unfolding * using card_insert by auto qed auto

lemma card_2_exists: "card s = 2 \<longleftrightarrow> (\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. (z = x) \<or> (z = y)))" proof

  assume "card s = 2" then obtain x y where obt:"s = {x, y}" "x\<noteq>y" unfolding numeral_2_eq_2 apply - apply(erule exE conjE|drule card_eq_SucD)+ by auto

  show "\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y)" using obt by auto next

  assume "\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y)" then guess x .. from this(2) guess y  ..

  with `x\<in>s` have *:"s = {x, y}" "x\<noteq>y" by auto

  from this(2) show "card s = 2" unfolding * by auto qed

lemma image_lemma_0: assumes "card {a\<in>s. f ` (s - {a}) = t - {b}} = n"

  shows "card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> (f ` s' = t - {b})} = n" proof-

  have *:"{s'. \<exists>a\<in>s. (s' = s - {a}) \<and> (f ` s' = t - {b})} = (\<lambda>a. s - {a}) ` {a\<in>s. f ` (s - {a}) = t - {b}}" by auto

  show ?thesis unfolding * unfolding assms[THEN sym] apply(rule card_image) unfolding inj_on_def 

    apply(rule,rule,rule) unfolding mem_Collect_eq by auto qed

lemma image_lemma_1: assumes "finite s" "finite t" "card s = card t" "f ` s = t" "b \<in> t"

  shows "card {s'. \<exists>a\<in>s. s' = s - {a} \<and>  f ` s' = t - {b}} = 1" proof-

  obtain a where a:"b = f a" "a\<in>s" using assms(4-5) by auto

  have inj:"inj_on f s" apply(rule eq_card_imp_inj_on) using assms(1-4) by auto

  have *:"{a \<in> 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] by auto

  show ?thesis apply(rule image_lemma_0) unfolding *  by auto qed

lemma image_lemma_2: assumes "finite s" "finite t" "card s = card t" "f ` s \<subseteq> t" "f ` s \<noteq> t" "b \<in> t"

  shows "(card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> f ` s' = t - {b}} = 0) \<or>

         (card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> f ` s' = t - {b}} = 2)" proof(cases "{a\<in>s. f ` (s - {a}) = t - {b}} = {}")

  case True thus ?thesis apply-apply(rule disjI1, rule image_lemma_0) using assms(1) by auto

next let ?M = "{a\<in>s. f ` (s - {a}) = t - {b}}"

  case False then obtain a where "a\<in>?M" by auto hence a:"a\<in>s" "f ` (s - {a}) = t - {b}" by auto

  have "f a \<in> t - {b}" using a and assms by auto

  hence "\<exists>c \<in> s - {a}. f a = f c" unfolding image_iff[symmetric] and a by auto

  then obtain c where c:"c \<in> s" "a \<noteq> c" "f a = f c" by auto

  hence *:"f ` (s - {c}) = f ` (s - {a})" apply-apply(rule set_eqI,rule) proof-

    fix x assume "x \<in> f ` (s - {a})" then obtain y where y:"f y = x" "y\<in>s- {a}" by auto

    thus "x \<in> f ` (s - {c})" unfolding image_iff apply(rule_tac x="if y = c then a else y" in bexI) using c a by auto qed auto

  have "c\<in>?M" unfolding mem_Collect_eq and * using a and c(1) by auto

  show ?thesis apply(rule disjI2, rule image_lemma_0) unfolding card_2_exists

    apply(rule bexI[OF _ `a\<in>?M`], rule bexI[OF _ `c\<in>?M`],rule,rule `a\<noteq>c`) proof(rule,unfold mem_Collect_eq,erule conjE)

    fix z assume as:"z \<in> 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 by auto

    show "z = a \<or> z = c" proof(rule ccontr)

      assume "\<not> (z = a \<or> z = c)" thus False using inj[unfolded inj_on_def,THEN bspec[where x=a],THEN bspec[where x=c]]

        using `a\<in>s` `c\<in>s` `f a = f c` `a\<noteq>c` by auto qed qed qed

subsection {* Combine this with the basic counting lemma. *}

lemma kuhn_complete_lemma:

  assumes "finite simplices"

  "\<forall>f s. face f s \<longleftrightarrow> (\<exists>a\<in>s. f = s - {a})" "\<forall>s\<in>simplices. card s = n + 2" "\<forall>s\<in>simplices. (rl ` s) \<subseteq> {0..n+1}"

  "\<forall>f\<in> {f. \<exists>s\<in>simplices. face f s}. bnd f  \<longrightarrow> (card {s\<in>simplices. face f s} = 1)"

  "\<forall>f\<in> {f. \<exists>s\<in>simplices. face f s}. \<not>bnd f \<longrightarrow> (card {s\<in>simplices. face f s} = 2)"

  "odd(card {f\<in>{f. \<exists>s\<in>simplices. face f s}. rl ` f = {0..n} \<and> bnd f})"

  shows "odd (card {s\<in>simplices. (rl ` s = {0..n+1})})" 

  apply(rule kuhn_counting_lemma) defer apply(rule assms)+ prefer 3 apply(rule assms) proof(rule_tac[1-2] ballI impI)+ 

  have *:"{f. \<exists>s\<in>simplices. \<exists>a\<in>s. f = s - {a}} = (\<Union>s\<in>simplices. {f. \<exists>a\<in>s. (f = s - {a})})" by auto

  have **: "\<forall>s\<in>simplices. card s = n + 2 \<and> finite s" using assms(3) by (auto intro: card_ge_0_finite)

  show "finite {f. \<exists>s\<in>simplices. face f s}" unfolding assms(2)[rule_format] and *

    apply(rule finite_UN_I[OF assms(1)]) using ** by auto

  have *:"\<And> P f s. s\<in>simplices \<Longrightarrow> (f \<in> {f. \<exists>s\<in>simplices. \<exists>a\<in>s. f = s - {a}}) \<and>

    (\<exists>a\<in>s. (f = s - {a})) \<and> P f \<longleftrightarrow> (\<exists>a\<in>s. (f = s - {a}) \<and> P f)" by auto

  fix s assume s:"s\<in>simplices" let ?S = "{f \<in> {f. \<exists>s\<in>simplices. face f s}. face f s \<and> rl ` f = {0..n}}"

    have "{0..n + 1} - {n + 1} = {0..n}" by auto

    hence S:"?S = {s'. \<exists>a\<in>s. s' = s - {a} \<and> rl ` s' = {0..n + 1} - {n + 1}}" apply- apply(rule set_eqI)

      unfolding assms(2)[rule_format] mem_Collect_eq and *[OF s, unfolded mem_Collect_eq, where P="\<lambda>x. rl ` x = {0..n}"] by auto

    show "rl ` s = {0..n+1} \<Longrightarrow> card ?S = 1" "rl ` s \<noteq> {0..n+1} \<Longrightarrow> card ?S = 0 \<or> card ?S = 2" unfolding S

      apply(rule_tac[!] image_lemma_1 image_lemma_2) using ** assms(4) and s by auto qed

subsection {*We use the following notion of ordering rather than pointwise indexing. *}

definition "kle n x y \<longleftrightarrow> (\<exists>k\<subseteq>{1..n::nat}. (\<forall>j. y(j) = x(j) + (if j \<in> k then (1::nat) else 0)))"

lemma kle_refl[intro]: "kle n x x" unfolding kle_def by auto

lemma kle_antisym: "kle n x y \<and> kle n y x \<longleftrightarrow> (x = y)"

  unfolding kle_def apply rule apply(rule ext) by auto

lemma pointwise_minimal_pointwise_maximal: fixes s::"(nat\<Rightarrow>nat) set"

  assumes  "finite s" "s \<noteq> {}" "\<forall>x\<in>s. \<forall>y\<in>s. (\<forall>j. x j \<le> y j) \<or> (\<forall>j. y j \<le> x j)"

  shows "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. a j \<le> x j" "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. x j \<le> a j"

  using assms unfolding atomize_conj apply- proof(induct s rule:finite_induct)

  fix x and F::"(nat\<Rightarrow>nat) set" assume as:"finite F" "x \<notin> F" 

    "\<lbrakk>F \<noteq> {}; \<forall>x\<in>F. \<forall>y\<in>F. (\<forall>j. x j \<le> y j) \<or> (\<forall>j. y j \<le> x j)\<rbrakk>

        \<Longrightarrow> (\<exists>a\<in>F. \<forall>x\<in>F. \<forall>j. a j \<le> x j) \<and> (\<exists>a\<in>F. \<forall>x\<in>F. \<forall>j. x j \<le> a j)" "insert x F \<noteq> {}"

    "\<forall>xa\<in>insert x F. \<forall>y\<in>insert x F. (\<forall>j. xa j \<le> y j) \<or> (\<forall>j. y j \<le> xa j)"

  show "(\<exists>a\<in>insert x F. \<forall>x\<in>insert x F. \<forall>j. a j \<le> x j) \<and> (\<exists>a\<in>insert x F. \<forall>x\<in>insert x F. \<forall>j. x j \<le> a j)" proof(cases "F={}")

    case True thus ?thesis apply-apply(rule,rule_tac[!] x=x in bexI) by auto next

    case False obtain a b where a:"a\<in>insert x F" "\<forall>x\<in>F. \<forall>j. a j \<le> x j" and

      b:"b\<in>insert x F" "\<forall>x\<in>F. \<forall>j. x j \<le> b j" using as(3)[OF False] using as(5) by auto

    have "\<exists>a\<in>insert x F. \<forall>x\<in>insert x F. \<forall>j. a j \<le> x j"

      using as(5)[rule_format,OF a(1) insertI1] apply- proof(erule disjE)

      assume "\<forall>j. a j \<le> x j" thus ?thesis apply(rule_tac x=a in bexI) using a by auto next

      assume "\<forall>j. x j \<le> a j" thus ?thesis apply(rule_tac x=x in bexI) apply(rule,rule) using a apply -

        apply(erule_tac x=xa in ballE) apply(erule_tac x=j in allE)+ by auto qed moreover

    have "\<exists>b\<in>insert x F. \<forall>x\<in>insert x F. \<forall>j. x j \<le> b j"

      using as(5)[rule_format,OF b(1) insertI1] apply- proof(erule disjE)

      assume "\<forall>j. x j \<le> b j" thus ?thesis apply(rule_tac x=b in bexI) using b by auto next

      assume "\<forall>j. b j \<le> x j" thus ?thesis apply(rule_tac x=x in bexI) apply(rule,rule) using b apply -

        apply(erule_tac x=xa in ballE) apply(erule_tac x=j in allE)+ by auto qed

    ultimately show  ?thesis by auto qed qed(auto)

lemma kle_imp_pointwise: "kle n x y \<Longrightarrow> (\<forall>j. x j \<le> y j)" unfolding kle_def by auto

lemma pointwise_antisym: fixes x::"nat \<Rightarrow> nat"

  shows "(\<forall>j. x j \<le> y j) \<and> (\<forall>j. y j \<le> x j) \<longleftrightarrow> (x = y)"

  apply(rule, rule ext,erule conjE) apply(erule_tac x=xa in allE)+ by auto

lemma kle_trans: assumes "kle n x y" "kle n y z" "kle n x z \<or> kle n z x" shows "kle n x z"

  using assms apply- apply(erule disjE) apply assumption proof- case goal1

  hence "x=z" apply- apply(rule ext) apply(drule kle_imp_pointwise)+ 

    apply(erule_tac x=xa in allE)+ by auto thus ?case by auto qed

lemma kle_strict: assumes "kle n x y" "x \<noteq> y"

  shows "\<forall>j. x j \<le> y j"  "\<exists>k. 1 \<le> k \<and> k \<le> n \<and> 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 "\<exists>k. 1 \<le> k \<and> k \<le> n \<and> x(k) < y(k)" proof(cases "k={}")

    case True hence "x=y" apply-apply(rule ext) using k by auto

    thus ?thesis using assms(2) by auto next

    case False hence "(SOME k'. k' \<in> k) \<in> k" apply-apply(rule someI_ex) by auto

    thus ?thesis apply(rule_tac x="SOME k'. k' \<in> k" in exI) using k by auto qed qed

lemma kle_minimal: assumes "finite s" "s \<noteq> {}" "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"

  shows "\<exists>a\<in>s. \<forall>x\<in>s. kle n a x" proof-

  have "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. a j \<le> x j" apply(rule pointwise_minimal_pointwise_maximal(1)[OF assms(1-2)])

    apply(rule,rule) apply(drule_tac assms(3)[rule_format],assumption) using kle_imp_pointwise by auto

  then guess a .. note a=this show ?thesis apply(rule_tac x=a in bexI) proof fix x assume "x\<in>s"

    show "kle n a x" using assms(3)[rule_format,OF a(1) `x\<in>s`] apply- proof(erule disjE)

      assume "kle n x a" hence "x = a" apply- unfolding pointwise_antisym[THEN sym]

        apply(drule kle_imp_pointwise) using a(2)[rule_format,OF `x\<in>s`] by auto

      thus ?thesis using kle_refl by auto  qed qed(insert a, auto) qed

lemma kle_maximal: assumes "finite s" "s \<noteq> {}" "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"

  shows "\<exists>a\<in>s. \<forall>x\<in>s. kle n x a" proof-

  have "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. a j \<ge> x j" apply(rule pointwise_minimal_pointwise_maximal(2)[OF assms(1-2)])

    apply(rule,rule) apply(drule_tac assms(3)[rule_format],assumption) using kle_imp_pointwise by auto

  then guess a .. note a=this show ?thesis apply(rule_tac x=a in bexI) proof fix x assume "x\<in>s"

    show "kle n x a" using assms(3)[rule_format,OF a(1) `x\<in>s`] apply- proof(erule disjE)

      assume "kle n a x" hence "x = a" apply- unfolding pointwise_antisym[THEN sym]

        apply(drule kle_imp_pointwise) using a(2)[rule_format,OF `x\<in>s`] by auto

      thus ?thesis using kle_refl by auto  qed qed(insert a, auto) qed

lemma kle_strict_set: assumes "kle n x y" "x \<noteq> y"

  shows "1 \<le> card {k\<in>{1..n}. x k < y k}" proof-

  guess i using kle_strict(2)[OF assms] ..

  hence "card {i} \<le> card {k\<in>{1..n}. x k < y k}" apply- apply(rule card_mono) by auto

  thus ?thesis by auto qed

lemma kle_range_combine:

  assumes "kle n x y" "kle n y z" "kle n x z \<or> kle n z x"

  "m1 \<le> card {k\<in>{1..n}. x k < y k}"

  "m2 \<le> card {k\<in>{1..n}. y k < z k}"

  shows "kle n x z \<and> m1 + m2 \<le> card {k\<in>{1..n}. x k < z k}"

  apply(rule,rule kle_trans[OF assms(1-3)]) proof-

  have "\<And>j. x j < y j \<Longrightarrow> x j < z j" apply(rule less_le_trans) using kle_imp_pointwise[OF assms(2)] by auto moreover

  have "\<And>j. y j < z j \<Longrightarrow> x j < z j" apply(rule le_less_trans) using kle_imp_pointwise[OF assms(1)] by auto ultimately

  have *:"{k\<in>{1..n}. x k < y k} \<union> {k\<in>{1..n}. y k < z k} = {k\<in>{1..n}. x k < z k}" by auto

  have **:"{k \<in> {1..n}. x k < y k} \<inter> {k \<in> {1..n}. y k < z k} = {}" unfolding disjoint_iff_not_equal

    apply(rule,rule,unfold mem_Collect_eq,rule ccontr) apply(erule conjE)+ proof-

    fix i j assume as:"i \<in> {1..n}" "x i < y i" "j \<in> {1..n}" "y j < z j" "\<not> i \<noteq> j"

    guess kx using assms(1)[unfolded kle_def] .. note kx=this

    have "x i < y i" using as by auto hence "i \<in> kx" using as(1) kx apply(rule_tac ccontr) by auto 

    hence "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 hence "i \<in> ky" using as(1) ky apply(rule_tac ccontr) by auto 

    hence "y i + 1 = z i" using ky by auto ultimately

    have "z i = x i + 2" by auto

    thus False using assms(3) unfolding kle_def by(auto simp add: split_if_eq1) qed

  have fin:"\<And>P. finite {x\<in>{1..n::nat}. P x}" by auto

  have "m1 + m2 \<le> card {k\<in>{1..n}. x k < y k} + card {k\<in>{1..n}. y k < z k}" using assms(4-5) by auto

  also have "\<dots> \<le>  card {k\<in>{1..n}. x k < z k}" unfolding card_Un_Int[OF fin fin] unfolding * ** by auto

  finally show " m1 + m2 \<le> card {k \<in> {1..n}. x k < z k}" by auto qed

lemma kle_range_combine_l:

  assumes "kle n x y" "kle n y z" "kle n x z \<or> kle n z x" "m \<le> card {k\<in>{1..n}. y(k) < z(k)}"

  shows "kle n x z \<and> m \<le> card {k\<in>{1..n}. x(k) < z(k)}"

  using kle_range_combine[OF assms(1-3) _ assms(4), of 0] by auto

lemma kle_range_combine_r:

  assumes "kle n x y" "kle n y z" "kle n x z \<or> kle n z x" "m \<le> card {k\<in>{1..n}. x k < y k}"

  shows "kle n x z \<and> m \<le> card {k\<in>{1..n}. x(k) < z(k)}"

  using kle_range_combine[OF assms(1-3) assms(4), of 0] by auto

lemma kle_range_induct:

  assumes "card s = Suc m" "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"

  shows "\<exists>x\<in>s. \<exists>y\<in>s. kle n x y \<and> m \<le> card {k\<in>{1..n}. x k < y k}" proof-

have "finite s" "s\<noteq>{}" using assms(1) by (auto intro: card_ge_0_finite)

thus ?thesis using assms apply- proof(induct m arbitrary: s)

  case 0 thus ?case using kle_refl by auto next

  case (Suc m) then obtain a where a:"a\<in>s" "\<forall>x\<in>s. kle n a x" using kle_minimal[of s n] by auto

  show ?case proof(cases "s \<subseteq> {a}") case False

    hence "card (s - {a}) = Suc m" "s - {a} \<noteq> {}" using card_Diff_singleton[OF _ a(1)] Suc(4) `finite s` by auto

    then obtain x b where xb:"x\<in>s - {a}" "b\<in>s - {a}" "kle n x b" "m \<le> card {k \<in> {1..n}. x k < b k}" 

      using Suc(1)[of "s - {a}"] using Suc(5) `finite s` by auto

    have "1 \<le> card {k \<in> {1..n}. a k < x k}" "m \<le> card {k \<in> {1..n}. x k < b k}"

      apply(rule kle_strict_set) apply(rule a(2)[rule_format]) using a and xb by auto

    thus ?thesis apply(rule_tac x=a in bexI, 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) by auto next

    case True hence "s = {a}" using Suc(3) by auto hence "card s = 1" by auto

    hence False using Suc(4) `finite s` by auto thus ?thesis by auto qed qed qed

lemma kle_Suc: "kle n x y \<Longrightarrow> kle (n + 1) x y"

  unfolding kle_def apply(erule exE) apply(rule_tac x=k in exI) by auto

lemma kle_trans_1: assumes "kle n x y" shows "x j \<le> y j" "y j \<le> x j + 1"

  using assms[unfolded kle_def] by auto 

lemma kle_trans_2: assumes "kle n a b" "kle n b c" "\<forall>j. c j \<le> 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 \<union> kk2" in exI) apply(rule) defer proof

    fix i show "c i = a i + (if i \<in> kk1 \<union> kk2 then 1 else 0)" proof(cases "i\<in>kk1 \<union> kk2")

      case True hence "c i \<ge> a i + (if i \<in> kk1 \<union> 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 \<le> a i + (if i \<in> kk1 \<union> kk2 then 1 else 0)" using True assms(3) by auto  

      ultimately show ?thesis by auto next

      case False thus ?thesis using kk1 kk2 by auto qed qed(insert kk1 kk2, auto) qed

lemma kle_between_r: assumes "kle n a b" "kle n b c" "kle n a x" "kle n c x" shows "kle n b x"

  apply(rule kle_trans_2[OF assms(2,4)]) proof have *:"\<And>c b x::nat. x \<le> c + 1 \<Longrightarrow> c \<le> b \<Longrightarrow> x \<le> b + 1" by auto

  fix j show "x j \<le> b j + 1" apply(rule *)using kle_trans_1[OF assms(1),of j] kle_trans_1[OF assms(3), of j] by auto qed

lemma kle_between_l: assumes "kle n a b" "kle n b c" "kle n x a" "kle n x c" shows "kle n x b"

  apply(rule kle_trans_2[OF assms(3,1)]) proof have *:"\<And>c b x::nat. c \<le> x + 1 \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> x + 1" by auto

  fix j show "b j \<le> x j + 1" apply(rule *) using kle_trans_1[OF assms(2),of j] kle_trans_1[OF assms(4), of j] by auto qed

lemma kle_adjacent:

  assumes "\<forall>j. b j = (if j = k then a(j) + 1 else a j)" "kle n a x" "kle n x b"

  shows "(x = a) \<or> (x = b)" proof(cases "x k = a k")

  case True show ?thesis apply(rule disjI1,rule ext) proof- fix j

    have "x j \<le> 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 by auto

    thus "x j = a j" using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]] by auto qed next

  case False show ?thesis apply(rule disjI2,rule ext) proof- fix j

    have "x j \<ge> 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 by auto

    thus "x j = b j" using kle_imp_pointwise[OF assms(3),THEN spec[where x=j]] by auto qed qed

subsection {* kuhn's notion of a simplex (a reformulation to avoid so much indexing). *}

definition "ksimplex p n (s::(nat \<Rightarrow> nat) set) \<longleftrightarrow>

        (card s = n + 1 \<and>

        (\<forall>x\<in>s. \<forall>j. x(j) \<le> p) \<and>

        (\<forall>x\<in>s. \<forall>j. j\<notin>{1..n} \<longrightarrow> (x j = p)) \<and>

        (\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x))"

lemma ksimplexI:"card s = n + 1 \<Longrightarrow>  \<forall>x\<in>s. \<forall>j. x j \<le> p \<Longrightarrow> \<forall>x\<in>s. \<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p \<Longrightarrow> \<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x \<Longrightarrow> ksimplex p n s"

  unfolding ksimplex_def by auto

lemma ksimplex_eq: "ksimplex p n (s::(nat \<Rightarrow> nat) set) \<longleftrightarrow>

        (card s = n + 1 \<and> finite s \<and>

        (\<forall>x\<in>s. \<forall>j. x(j) \<le> p) \<and>

        (\<forall>x\<in>s. \<forall>j. j\<notin>{1..n} \<longrightarrow> (x j = p)) \<and>

        (\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> 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 \<in> s" "b \<in> s"

  "\<forall>x\<in>s. kle n a x \<and> kle n x b" "\<forall>i. b(i) = (if i \<in> {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 by auto next

  note assm = assms[unfolded ksimplex_eq]

  case False have "s\<noteq>{}" using assm by auto

  obtain a where a:"a\<in>s" "\<forall>x\<in>s. kle n a x" using `s\<noteq>{}` assm using kle_minimal[of s n] by auto

  obtain b where b:"b\<in>s" "\<forall>x\<in>s. kle n x b" using `s\<noteq>{}` assm using kle_maximal[of s n] by auto

  obtain c d where c_d:"c\<in>s" "d\<in>s" "kle n c d" "n \<le> card {k \<in> {1..n}. c k < d k}"

    using kle_range_induct[of s n n] using assm by auto

  have "kle n c b \<and> n \<le> card {k \<in> {1..n}. c k < b k}" apply(rule kle_range_combine_r[where y=d]) using c_d a b by auto

  hence "kle n a b \<and> n \<le> card {k\<in>{1..n}. a(k) < b(k)}" apply-apply(rule kle_range_combine_l[where y=c]) using a `c\<in>s` `b\<in>s` by auto

  moreover have "card {1..n} \<ge> card {k\<in>{1..n}. a(k) < b(k)}" apply(rule card_mono) by auto

  ultimately have *:"{k\<in>{1 .. n}. a k < b k} = {1..n}" apply- apply(rule card_subset_eq) by auto

  show ?thesis apply(rule that[OF a(1) b(1)]) defer apply(subst *[THEN sym]) 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 \<in> {1..n} \<and> a i < b i then a i + 1 else a i)" proof(cases "i \<in> {1..n}")

      case True thus ?thesis unfolding k[THEN conjunct2,rule_format] by auto next

      case False have "a i = p" using assm and False `a\<in>s` by auto

      moreover   have "b i = p" using assm and False `b\<in>s` by auto

      ultimately show ?thesis by auto qed qed(insert a(2) b(2) assm,auto) qed

lemma ksimplex_extrema_strong:

  assumes "ksimplex p n s" "n \<noteq> 0" obtains a b where "a \<in> s" "b \<in> s" "a \<noteq> b"

  "\<forall>x\<in>s. kle n a x \<and> kle n x b" "\<forall>i. b(i) = (if i \<in> {1..n} then a(i) + 1 else a(i))" proof-

  obtain a b where ab:"a \<in> s" "b \<in> s" "\<forall>x\<in>s. kle n a x \<and> kle n x b" "\<forall>i. b(i) = (if i \<in> {1..n} then a(i) + 1 else a(i))" 

    apply(rule ksimplex_extrema[OF assms(1)]) by auto 

  have "a \<noteq> b" apply(rule ccontr) unfolding not_not apply(drule cong[of _ _ 1 1]) using ab(4) assms(2) by auto

  thus ?thesis apply(rule_tac that[of a b]) using ab by auto qed

lemma ksimplexD:

  assumes "ksimplex p n s"

  shows "card s = n + 1" "finite s" "card s = n + 1" "\<forall>x\<in>s. \<forall>j. x j \<le> p" "\<forall>x\<in>s. \<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p"

  "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x" using assms unfolding ksimplex_eq by auto

lemma ksimplex_successor:

  assumes "ksimplex p n s" "a \<in> s"

  shows "(\<forall>x\<in>s. kle n x a) \<or> (\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. y(j) = (if j = k then a(j) + 1 else a(j)))"

proof(cases "\<forall>x\<in>s. kle n x a") case True thus ?thesis by auto next note assm = ksimplexD[OF assms(1)]

  case False then obtain b where b:"b\<in>s" "\<not> kle n b a" "\<forall>x\<in>{x \<in> s. \<not> kle n x a}. kle n b x"

    using kle_minimal[of "{x\<in>s. \<not> kle n x a}" n] and assm by auto

  hence  **:"1 \<le> card {k\<in>{1..n}. a k < b k}" apply- apply(rule kle_strict_set) using assm(6) and `a\<in>s` by(auto simp add:kle_refl)

  let ?kle1 = "{x \<in> s. \<not> kle n x a}" have "card ?kle1 > 0" apply(rule ccontr) using assm(2) and False by auto

  hence sizekle1: "card ?kle1 = Suc (card ?kle1 - 1)" using assm(2) by auto

  obtain c d where c_d: "c \<in> s" "\<not> kle n c a" "d \<in> s" "\<not> kle n d a" "kle n c d" "card ?kle1 - 1 \<le> card {k \<in> {1..n}. c k < d k}"

    using kle_range_induct[OF sizekle1, of n] using assm by auto

  let ?kle2 = "{x \<in> s. kle n x a}"

  have "card ?kle2 > 0" apply(rule ccontr) using assm(6)[rule_format,of a a] and `a\<in>s` and assm(2) by auto

  hence sizekle2:"card ?kle2 = Suc (card ?kle2 - 1)" using assm(2) by auto

  obtain e f where e_f: "e \<in> s" "kle n e a" "f \<in> s" "kle n f a" "kle n e f" "card ?kle2 - 1 \<le> card {k \<in> {1..n}. e k < f k}"

    using kle_range_induct[OF sizekle2, of n] using assm by auto

  have "card {k\<in>{1..n}. a k < b k} = 1" proof(rule ccontr) case goal1

    hence as:"card {k\<in>{1..n}. a k < b k} \<ge> 2" using ** by auto

    have *:"finite ?kle2" "finite ?kle1" "?kle2 \<union> ?kle1 = s" "?kle2 \<inter> ?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 "\<dots> = 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 \<and> card {x \<in> s. kle n x a} - 1 \<le> card {k \<in> {1..n}. e k < a k}"

      apply(rule kle_range_combine_r[where y=f]) using e_f using `a\<in>s` assm(6) by auto

    moreover have "kle n b d \<and> card {x \<in> s. \<not> kle n x a} - 1 \<le> card {k \<in> {1..n}. b k < d k}"

      apply(rule kle_range_combine_l[where y=c]) using c_d using assm(6) and b by auto

    hence "kle n a d \<and> 2 + (card {x \<in> s. \<not> kle n x a} - 1) \<le> card {k \<in> {1..n}. a k < d k}" apply-

      apply(rule kle_range_combine[where y=b]) using as and b assm(6) `a\<in>s` `d\<in>s` apply- by blast+

    ultimately have "kle n e d \<and> (card ?kle2 - 1) + (2 + (card ?kle1 - 1)) \<le> card {k\<in>{1..n}. e k < d k}" apply-

      apply(rule kle_range_combine[where y=a]) using assm(6)[rule_format,OF `e\<in>s` `d\<in>s`] apply - by blast+ 

    moreover have "card {k \<in> {1..n}. e k < d k} \<le> card {1..n}" apply(rule card_mono) by 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,rule_tac x=k in bexI) proof

    fix j::nat have "kle n a b" using b and assm(6)[rule_format, OF `a\<in>s` `b\<in>s`] by auto

    then guess kk unfolding kle_def .. note kk_raw=this note kk=this[THEN conjunct2,rule_format]

    have kkk:"k\<in>kk" apply(rule ccontr) using k(1) unfolding kk by auto 

    show "b j = (if j = k then a j + 1 else a j)" proof(cases "j\<in>kk")

      case True hence "j=k" apply-apply(rule k(2)[rule_format]) using kk_raw kkk by auto

      thus ?thesis unfolding kk using kkk by auto next

      case False hence "j\<noteq>k" using k(2)[rule_format, of j k] using kk_raw kkk by auto

      thus ?thesis unfolding kk using kkk using False by auto qed qed(insert k(1) `b\<in>s`, auto) qed

lemma ksimplex_predecessor:

  assumes "ksimplex p n s" "a \<in> s"

  shows "(\<forall>x\<in>s. kle n a x) \<or> (\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. a(j) = (if j = k then y(j) + 1 else y(j)))"

proof(cases "\<forall>x\<in>s. kle n a x") case True thus ?thesis by auto next note assm = ksimplexD[OF assms(1)]

  case False then obtain b where b:"b\<in>s" "\<not> kle n a b" "\<forall>x\<in>{x \<in> s. \<not> kle n a x}. kle n x b" 

    using kle_maximal[of "{x\<in>s. \<not> kle n a x}" n] and assm by auto

  hence  **:"1 \<le> card {k\<in>{1..n}. a k > b k}" apply- apply(rule kle_strict_set) using assm(6) and `a\<in>s` by(auto simp add:kle_refl)

  let ?kle1 = "{x \<in> s. \<not> kle n a x}" have "card ?kle1 > 0" apply(rule ccontr) using assm(2) and False by auto

  hence sizekle1:"card ?kle1 = Suc (card ?kle1 - 1)" using assm(2) by auto

  obtain c d where c_d: "c \<in> s" "\<not> kle n a c" "d \<in> s" "\<not> kle n a d" "kle n d c" "card ?kle1 - 1 \<le> card {k \<in> {1..n}. c k > d k}"

    using kle_range_induct[OF sizekle1, of n] using assm by auto

  let ?kle2 = "{x \<in> s. kle n a x}"

  have "card ?kle2 > 0" apply(rule ccontr) using assm(6)[rule_format,of a a] and `a\<in>s` and assm(2) by auto

  hence sizekle2:"card ?kle2 = Suc (card ?kle2 - 1)" using assm(2) by auto

  obtain e f where e_f: "e \<in> s" "kle n a e" "f \<in> s" "kle n a f" "kle n f e" "card ?kle2 - 1 \<le> card {k \<in> {1..n}. e k > f k}"

    using kle_range_induct[OF sizekle2, of n] using assm by auto

  have "card {k\<in>{1..n}. a k > b k} = 1" proof(rule ccontr) case goal1

    hence as:"card {k\<in>{1..n}. a k > b k} \<ge> 2" using ** by auto

    have *:"finite ?kle2" "finite ?kle1" "?kle2 \<union> ?kle1 = s" "?kle2 \<inter> ?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 "\<dots> = 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 \<and> card {x \<in> s. kle n a x} - 1 \<le> card {k \<in> {1..n}. e k > a k}"

      apply(rule kle_range_combine_l[where y=f]) using e_f using `a\<in>s` assm(6) by auto

    moreover have "kle n d b \<and> card {x \<in> s. \<not> kle n a x} - 1 \<le> card {k \<in> {1..n}. b k > d k}"

      apply(rule kle_range_combine_r[where y=c]) using c_d using assm(6) and b by auto

    hence "kle n d a \<and> (card {x \<in> s. \<not> kle n a x} - 1) + 2 \<le> card {k \<in> {1..n}. a k > d k}" apply-

      apply(rule kle_range_combine[where y=b]) using as and b assm(6) `a\<in>s` `d\<in>s` by blast+

    ultimately have "kle n d e \<and> (card ?kle1 - 1 + 2) + (card ?kle2 - 1) \<le> card {k\<in>{1..n}. e k > d k}" apply-

      apply(rule kle_range_combine[where y=a]) using assm(6)[rule_format,OF `e\<in>s` `d\<in>s`] apply - by blast+

    moreover have "card {k \<in> {1..n}. e k > d k} \<le> card {1..n}" apply(rule card_mono) by 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,rule_tac x=k in bexI) proof

    fix j::nat have "kle n b a" using b and assm(6)[rule_format, OF `a\<in>s` `b\<in>s`] by auto

    then guess kk unfolding kle_def .. note kk_raw=this note kk=this[THEN conjunct2,rule_format]

    have kkk:"k\<in>kk" apply(rule ccontr) using k(1) unfolding kk by auto 

    show "a j = (if j = k then b j + 1 else b j)" proof(cases "j\<in>kk")

      case True hence "j=k" apply-apply(rule k(2)[rule_format]) using kk_raw kkk by auto

      thus ?thesis unfolding kk using kkk by auto next

      case False hence "j\<noteq>k" using k(2)[rule_format, of j k] using kk_raw kkk by auto

      thus ?thesis unfolding kk using kkk using False by auto qed qed(insert k(1) `b\<in>s`, auto) qed

subsection {* The lemmas about simplices that we need. *}

lemma card_funspace': assumes "finite s" "finite t" "card s = m" "card t = n"

  shows "card {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)} = n ^ m" (is "card (?M s) = _")

  using assms apply - proof(induct m arbitrary: s)

  have *:"{f. \<forall>x. f x = d} = {\<lambda>x. d}" apply(rule set_eqI,rule)unfolding mem_Collect_eq apply(rule,rule ext) by auto

  case 0 thus ?case by(auto simp add: *) next

  case (Suc m) guess a using card_eq_SucD[OF Suc(4)] .. then guess s0

    apply(erule_tac exE) apply(erule conjE)+ . note as0 = this

  have **:"card s0 = m" using as0 using Suc(2) Suc(4) by auto

  let ?l = "(\<lambda>(b,g) x. if x = a then b else g x)" have *:"?M (insert a s0) = ?l ` {(b,g). b\<in>t \<and> g\<in>?M s0}"

    apply(rule set_eqI,rule) unfolding mem_Collect_eq image_iff apply(erule conjE)

    apply(rule_tac x="(x a, \<lambda>y. if y\<in>s0 then x y else d)" in bexI) apply(rule ext) prefer 3 apply rule defer

    apply(erule bexE,rule) unfolding mem_Collect_eq apply(erule splitE)+ apply(erule conjE)+ proof-

    fix x xa xb xc y assume as:"x = (\<lambda>(b, g) x. if x = a then b else g x) xa" "xb \<in> UNIV - insert a s0" "xa = (xc, y)" "xc \<in> t"

      "\<forall>x\<in>s0. y x \<in> t" "\<forall>x\<in>UNIV - s0. y x = d" thus "x xb = d" unfolding as by auto qed auto

  have inj:"inj_on ?l {(b,g). b\<in>t \<and> g\<in>?M s0}" unfolding inj_on_def apply(rule,rule,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 thus ?thesis using as(1)[THEN cong[of _ _ x x]] by auto next

        case True thus ?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 apply-

    unfolding card_cartesian_product

    using Suc(1)[OF `finite s0` `finite t` ** `card t = n`] by auto

qed

lemma card_funspace: assumes  "finite s" "finite t"

  shows "card {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)} = (card t) ^ (card s)"

  using assms by (auto intro: card_funspace')

lemma finite_funspace: assumes "finite s" "finite t"

  shows "finite {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>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)

  thus ?thesis using True by (auto intro: card_ge_0_finite)

next

  case False hence "t = {}" using `finite t` by auto

  show ?thesis

  proof (cases "s = {}")

    have *:"{f. \<forall>x. f x = d} = {\<lambda>x. d}" by (auto intro: ext)

    case True thus ?thesis using `t = {}` by (auto simp: *)

  next

    case False thus ?thesis using `t = {}` by simp

  qed

qed

lemma finite_simplices: "finite {s. ksimplex p n s}"

  apply(rule finite_subset[of _ "{s. s\<subseteq>{f. (\<forall>i\<in>{1..n}. f i \<in> {0..p}) \<and> (\<forall>i\<in>UNIV-{1..n}. f i = p)}}"])

  unfolding ksimplex_def defer apply(rule finite_Collect_subsets) apply(rule finite_funspace) by auto

lemma simplex_top_face: assumes "0<p" "\<forall>x\<in>f. x (n + 1) = p"

  shows "(\<exists>s a. ksimplex p (n + 1) s \<and> a \<in> s \<and> (f = s - {a})) \<longleftrightarrow> ksimplex p n f" (is "?ls = ?rs") proof

  assume ?ls then guess s .. then guess a apply-apply(erule exE,(erule 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 \<in>s - {a}" "y \<in>s - {a}" have xyp:"x (n + 1) = y (n + 1)"

        using as(1)[unfolded sa(3)[THEN sym], THEN assms(2)[rule_format]]

        using as(2)[unfolded sa(3)[THEN sym], THEN assms(2)[rule_format]] by auto

    show "kle n x y \<or> kle n y x" proof(cases "kle (n + 1) x y")

      case True then guess k unfolding kle_def .. note k=this hence *:"n+1 \<notin> k" using xyp by auto

      have "\<not> (\<exists>x\<in>k. x\<notin>{1..n})" apply(rule ccontr) unfolding not_not apply(erule bexE) proof-

        fix x assume as:"x \<in> k" "x \<notin> {1..n}" have "x \<noteq> n+1" using as and * by auto

        thus False using as and k[THEN conjunct1,unfolded subset_eq] by auto qed

      thus ?thesis apply-apply(rule disjI1) unfolding kle_def using k apply(rule_tac x=k in exI) by auto next

      case False hence "kle (n + 1) y x" using ksimplexD(6)[OF sa(1),rule_format, of x y] using as by auto

      then guess k unfolding kle_def .. note k=this hence *:"n+1 \<notin> k" using xyp by auto

      hence "\<not> (\<exists>x\<in>k. x\<notin>{1..n})" apply-apply(rule ccontr) unfolding not_not apply(erule bexE) proof-

        fix x assume as:"x \<in> k" "x \<notin> {1..n}" have "x \<noteq> n+1" using as and * by auto

        thus False using as and k[THEN conjunct1,unfolded subset_eq] by auto qed

      thus ?thesis apply-apply(rule disjI2) unfolding kle_def using k apply(rule_tac x=k in exI) by auto qed next

    fix x j assume as:"x\<in>s - {a}" "j\<notin>{1..n}"

    thus "x j = p" using as(1)[unfolded sa(3)[THEN sym], THEN assms(2)[rule_format]]

      apply(cases "j = n+1") using sa(1)[unfolded ksimplex_def] by auto qed(insert sa ksimplexD[OF sa(1)], auto) next

  assume ?rs note rs=ksimplexD[OF this] guess a b apply(rule ksimplex_extrema[OF `?rs`]) . note ab = this

  def c \<equiv> "\<lambda>i. if i = (n + 1) then p - 1 else a i"

  have "c\<notin>f" apply(rule ccontr) unfolding not_not apply(drule assms(2)[rule_format]) unfolding c_def using assms(1) by auto

  thus ?ls apply(rule_tac x="insert c f" in exI,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 \<in> insert c f" thus "x j \<le> p" proof (cases "x=c")

      case True show ?thesis unfolding True c_def apply(cases "j=n+1") using ab(1) and rs(4) by auto 

    qed(insert x rs(4), auto simp add:c_def)

    show "j \<notin> {1..n + 1} \<longrightarrow> x j = p" apply(cases "x=c") using x ab(1) rs(5) unfolding c_def by auto

    { fix z assume z:"z \<in> insert c f" hence "kle (n + 1) c z" apply(cases "z = c") (*defer apply(rule kle_Suc)*) proof-

        case False hence "z\<in>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) .

        thus "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) by auto qed auto } note * = this

    fix y assume y:"y \<in> insert c f" show "kle (n + 1) x y \<or> kle (n + 1) y x" proof(cases "x = c \<or> y = c")

      case False hence **:"x\<in>f" "y\<in>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) qed

lemma ksimplex_fix_plane:

  assumes "a \<in> s" "j\<in>{1..n::nat}" "\<forall>x\<in>s - {a}. x j = q" "a0 \<in> s" "a1 \<in> s"

  "\<forall>i. a1 i = ((if i\<in>{1..n} then a0 i + 1 else a0 i)::nat)"

  shows "(a = a0) \<or> (a = a1)" proof- have *:"\<And>P A x y. \<forall>x\<in>A. P x \<Longrightarrow> x\<in>A \<Longrightarrow> y\<in>A \<Longrightarrow> P x \<and> 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) by auto qed

lemma ksimplex_fix_plane_0:

  assumes "a \<in> s" "j\<in>{1..n::nat}" "\<forall>x\<in>s - {a}. x j = 0" "a0 \<in> s" "a1 \<in> s"

  "\<forall>i. a1 i = ((if i\<in>{1..n} then a0 i + 1 else a0 i)::nat)"

  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]] by simp

lemma ksimplex_fix_plane_p:

  assumes "ksimplex p n s" "a \<in> s" "j\<in>{1..n}" "\<forall>x\<in>s - {a}. x j = p" "a0 \<in> s" "a1 \<in> s"

  "\<forall>i. a1 i = (if i\<in>{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:"a \<noteq> a0" hence *:"a0 \<in> s - {a}" using assms(5) by auto

  hence "a1 = a" using ksimplex_fix_plane[OF assms(2-)] by auto

  thus False using as using 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 auto qed

lemma ksimplex_replace_0:

  assumes "ksimplex p n s" "a \<in> s" "n \<noteq> 0" "j\<in>{1..n}" "\<forall>x\<in>s - {a}. x j = 0"

  shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 1" proof-

  have *:"\<And>s' a a'. s' - {a'} = s - {a} \<Longrightarrow> a' = a \<Longrightarrow> a' \<in> s' \<Longrightarrow> a \<in> s \<Longrightarrow> (s' = s)" by auto

  have **:"\<And>s' a'. ksimplex p n s' \<Longrightarrow> a' \<in> s' \<Longrightarrow> s' - {a'} = s - {a} \<Longrightarrow> s' = s" proof- case goal1

    guess a0 a1 apply(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) by auto moreover

    guess b0 b1 apply(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 by auto moreover

    have "b0 = a0" unfolding kle_antisym[THEN sym, of b0 a0 n] using exta extb using goal1(3) unfolding a a' by blast

    hence "b1 = a1" apply-apply(rule ext) unfolding exta(5) extb(5) by auto ultimately

    show "s' = s" apply-apply(rule *[of _ a1 b1]) using exta(1-2) extb(1-2) goal1 by auto 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) by auto qed

lemma ksimplex_replace_1:

  assumes "ksimplex p n s" "a \<in> s" "n \<noteq> 0" "j\<in>{1..n}" "\<forall>x\<in>s - {a}. x j = p"

  shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 1" proof-

  have lem:"\<And>a a' s'. s' - {a'} = s - {a} \<Longrightarrow> a' = a \<Longrightarrow> a' \<in> s' \<Longrightarrow> a \<in> s \<Longrightarrow> s' = s" by auto

  have lem:"\<And>s' a'. ksimplex p n s' \<Longrightarrow> a'\<in>s' \<Longrightarrow> s' - {a'} = s - {a} \<Longrightarrow> s' = s" proof- case goal1

    guess a0 a1 apply(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 by auto moreover

    guess b0 b1 apply(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) by auto

    moreover have *:"b1 = a1" unfolding kle_antisym[THEN sym, of b1 a1 n] using exta extb using goal1(3) unfolding a a' by blast moreover

    have "a0 = b0" apply(rule ext) proof- case goal1 show "a0 x = b0 x"

        using *[THEN cong, of x x] unfolding exta extb apply-apply(cases "x\<in>{1..n}") by auto qed

    ultimately show "s' = s" apply-apply(rule lem[OF goal1(3) _ goal1(2) assms(2)]) by auto qed 

  show ?thesis unfolding card_1_exists apply(rule ex1I[of _ s]) unfolding mem_Collect_eq apply(rule,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) by auto qed

lemma ksimplex_replace_2:

  assumes "ksimplex p n s" "a \<in> s" "n \<noteq> 0" "~(\<exists>j\<in>{1..n}. \<forall>x\<in>s - {a}. x j = 0)" "~(\<exists>j\<in>{1..n}. \<forall>x\<in>s - {a}. x j = p)"

  shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 2" (is "card ?A = 2")  proof-

  have lem1:"\<And>a a' s s'. s' - {a'} = s - {a} \<Longrightarrow> a' = a \<Longrightarrow> a' \<in> s' \<Longrightarrow> a \<in> s \<Longrightarrow> s' = s" by auto

  have lem2:"\<And>a b. a\<in>s \<Longrightarrow> b\<noteq>a \<Longrightarrow> s \<noteq> insert b (s - {a})" proof case goal1

    hence "a\<in>insert b (s - {a})" by auto hence "a\<in> s - {a}" unfolding insert_iff using goal1 by auto

    thus False by auto qed

  guess a0 a1 apply(rule ksimplex_extrema_strong[OF assms(1,3)]) . note a0a1=this

  { assume "a=a0"

    have *:"\<And>P Q. (P \<or> Q) \<Longrightarrow> \<not> P \<Longrightarrow> Q" by auto

    have "\<exists>x\<in>s. \<not> 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)

    hence "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>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`]]) by auto

    then guess a2 .. from this(2) guess k .. note k=this note a2=`a2\<in>s`

    def a3 \<equiv> "\<lambda>j. if j = k then a1 j + 1 else a1 j"

    have "a3 \<notin> s" proof assume "a3\<in>s" hence "kle n a3 a1" using a0a1(4) by auto

      thus False apply(drule_tac kle_imp_pointwise) unfolding a3_def

        apply(erule_tac x=k in allE) by auto qed

    hence "a3 \<noteq> a0" "a3 \<noteq> a1" using a0a1 by auto

    have "a2 \<noteq> a0" using k(2)[THEN spec[where x=k]] by auto

    have lem3:"\<And>x. x\<in>(s - {a0}) \<Longrightarrow> kle n a2 x" proof(rule ccontr) case goal1 hence as:"x\<in>s" "x\<noteq>a0" by auto

      have "kle n a2 x \<or> kle n x a2" using ksimplexD(6)[OF assms(1)] and as `a2\<in>s` by auto moreover

      have "kle n a0 x" using a0a1(4) as by auto

      ultimately have "x = a0 \<or> x = a2" apply-apply(rule kle_adjacent[OF k(2)]) using goal1(2) by auto

      hence "x = a2" using as by auto thus False using goal1(2) using kle_refl by auto qed

    let ?s = "insert a3 (s - {a0})" 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\<noteq>a0` `a3\<notin>s` `a0\<in>s` by(auto simp add:card_insert_if)

      fix x assume x:"x \<in> insert a3 (s - {a0})"

      show "\<forall>j. x j \<le> p" proof(rule,cases "x = a3")

        fix j case False thus "x j\<le>p" using x ksimplexD(4)[OF assms(1)] by auto next

        fix j case True show "x j\<le>p" unfolding True proof(cases "j=k") 

          case False thus "a3 j \<le>p" unfolding True a3_def using `a1\<in>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 \<le> a4 k" using lem3[OF a4(1)[unfolded `a=a0`],THEN kle_imp_pointwise] by auto

          also have "\<dots> < 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 thus "a3 j \<le>p" unfolding a3_def unfolding a0a1(5)[rule_format]

            using k(1) k(2)assms(5) using * by simp qed qed

      show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p" proof(rule,rule,cases "x=a3") fix j::nat assume j:"j\<notin>{1..n}"

        { case False thus "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto }

        case True show "x j = p" unfolding True a3_def using j k(1) 

          using ksimplexD(5)[OF assms(1),rule_format,OF `a1\<in>s` j] by auto qed

      fix y assume y:"y\<in>insert a3 (s - {a0})"

      have lem4:"\<And>x. x\<in>s \<Longrightarrow> x\<noteq>a0 \<Longrightarrow> kle n x a3" proof- case goal1

        guess kk using a0a1(4)[rule_format,OF `x\<in>s`,THEN conjunct2,unfolded kle_def] 

          apply-apply(erule exE,erule conjE) . note kk=this

        have "k\<notin>kk" proof assume "k\<in>kk"

          hence "a1 k = x k + 1" using kk by auto

          hence "a0 k = x k" unfolding a0a1(5)[rule_format] using k(1) by auto

          hence "a2 k = x k + 1" unfolding k(2)[rule_format] by auto moreover

          have "a2 k \<le> x k" using lem3[of x,THEN kle_imp_pointwise] goal1 by auto 

          ultimately show False by auto qed

        thus ?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) by auto qed

      show "kle n x y \<or> 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 by auto next

        case False show ?thesis proof(cases "x=a3") case True show ?thesis unfolding True

            apply(rule disjI2,rule lem4) using y False by auto next

          case False thus ?thesis apply(rule_tac ksimplexD(6)[OF assms(1),rule_format]) 

            using x y `y\<noteq>a3` by auto qed qed qed

    hence "insert a3 (s - {a0}) \<in> ?A" unfolding mem_Collect_eq apply-apply(rule,assumption)

      apply(rule_tac x="a3" in bexI) unfolding `a=a0` using `a3\<notin>s` by auto moreover

    have "s \<in> ?A" using assms(1,2) by auto ultimately have  "?A \<supseteq> {s, insert a3 (s - {a0})}" by auto

    moreover have "?A \<subseteq> {s, insert a3 (s - {a0})}" apply(rule) unfolding mem_Collect_eq proof(erule conjE)

      fix s' assume as:"ksimplex p n s'" and "\<exists>b\<in>s'. s' - {b} = s - {a}"

      from this(2) guess a' .. note a'=this

      guess a_min a_max apply(rule ksimplex_extrema_strong[OF as assms(3)]) . note min_max=this

      have *:"\<forall>x\<in>s' - {a'}. x k = a2 k" unfolding a' proof fix x assume x:"x\<in>s-{a}"

        hence "kle n a2 x" apply-apply(rule lem3) using `a=a0` by auto

        hence "a2 k \<le> x k" apply(drule_tac kle_imp_pointwise) by auto moreover

        have "x k \<le> 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 \<or> a'=a_max" apply(rule ksimplex_fix_plane[OF a'(1) k(1) *]) using min_max by auto

      show "s' \<in> {s, insert a3 (s - {a0})}" proof(cases "a'=a_min")

        case True have "a_max = a1" unfolding kle_antisym[THEN sym,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\<in>s'" using a' unfolding `a=a0` using a0a1 by auto

          show "a_max \<in> s" proof(rule ccontr) assume "a_max\<notin>s"

            hence "a_max = a'" using a' min_max by auto

            thus False unfolding True using min_max by auto qed qed

        hence "\<forall>i. a_max i = a1 i" by auto

        hence "a' = a" unfolding True `a=a0` apply-apply(subst fun_eq_iff,rule)

          apply(erule_tac x=x in allE) unfolding a0a1(5)[rule_format] min_max(5)[rule_format]

        proof- case goal1 thus ?case apply(cases "x\<in>{1..n}") by auto qed

        hence "s' = s" apply-apply(rule lem1[OF a'(2)]) using `a\<in>s` `a'\<in>s'` by auto

        thus ?thesis by auto next

        case False hence as:"a' = a_max" using ** by auto

        have "a_min = a2" unfolding kle_antisym[THEN sym, of _ _ n] apply rule

          apply(rule min_max(4)[rule_format,THEN conjunct1]) defer proof(rule lem3)

          show "a_min \<in> s - {a0}" unfolding a'(2)[THEN sym,unfolded `a=a0`] 

            unfolding as using min_max(1-3) by auto

          have "a2 \<noteq> a" unfolding `a=a0` using k(2)[rule_format,of k] by auto

          hence "a2 \<in> s - {a}" using a2 by auto thus "a2 \<in> s'" unfolding a'(2)[THEN sym] by auto qed

        hence "\<forall>i. a_min i = a2 i" by auto

        hence "a' = a3" unfolding as `a=a0` apply-apply(subst fun_eq_iff,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\<in>{1..n}") defer apply(cases "x=k")

            using `k\<in>{1..n}` by auto qed

        hence "s' = insert a3 (s - {a0})" apply-apply(rule lem1) defer apply assumption

          apply(rule a'(1)) unfolding a' `a=a0` using `a3\<notin>s` by auto

        thus ?thesis by auto qed qed

    ultimately have *:"?A = {s, insert a3 (s - {a0})}" by blast

    have "s \<noteq> insert a3 (s - {a0})" using `a3\<notin>s` by auto

    hence ?thesis unfolding * by auto } moreover

  { assume "a=a1"

    have *:"\<And>P Q. (P \<or> Q) \<Longrightarrow> \<not> P \<Longrightarrow> Q" by auto

    have "\<exists>x\<in>s. \<not> 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)

    hence "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>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`]]) by auto

    then guess a2 .. from this(2) guess k .. note k=this note a2=`a2\<in>s`

    def a3 \<equiv> "\<lambda>j. if j = k then a0 j - 1 else a0 j"

    have "a2 \<noteq> a1" using k(2)[THEN spec[where x=k]] by auto

    have lem3:"\<And>x. x\<in>(s - {a1}) \<Longrightarrow> kle n x a2" proof(rule ccontr) case goal1 hence as:"x\<in>s" "x\<noteq>a1" by auto

      have "kle n a2 x \<or> kle n x a2" using ksimplexD(6)[OF assms(1)] and as `a2\<in>s` by auto moreover

      have "kle n x a1" using a0a1(4) as by auto

      ultimately have "x = a2 \<or> x = a1" apply-apply(rule kle_adjacent[OF k(2)]) using goal1(2) by auto

      hence "x = a2" using as by auto thus False using goal1(2) using kle_refl by auto qed

    have "a0 k \<noteq> 0" proof-

      guess a4 using assms(4)[unfolded bex_simps ball_simps,rule_format,OF `k\<in>{1..n}`] .. note a4=this

      have "a4 k \<le> 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

      hence "a1 k > 1" unfolding k(2)[rule_format] by simp

      thus ?thesis unfolding a0a1(5)[rule_format] using k(1) by simp qed

    hence lem4:"\<forall>j. a0 j = (if j=k then a3 j + 1 else a3 j)" unfolding a3_def by simp

    have "\<not> kle n a0 a3" apply(rule ccontr) unfolding not_not apply(drule kle_imp_pointwise)

      unfolding lem4[rule_format] apply(erule_tac x=k in allE) by auto

    hence "a3 \<notin> s" using a0a1(4) by auto

    hence "a3 \<noteq> a1" "a3 \<noteq> 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\<noteq>a0` `a3\<notin>s` `a1\<in>s` by(auto simp add:card_insert_if)

      fix x assume x:"x \<in> insert a3 (s - {a1})"

      show "\<forall>j. x j \<le> p" proof(rule,cases "x = a3")

        fix j case False thus "x j\<le>p" using x ksimplexD(4)[OF assms(1)] by auto next

        fix j case True show "x j\<le>p" unfolding True proof(cases "j=k") 

          case False thus "a3 j \<le>p" unfolding True a3_def using `a0\<in>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 \<le> a0 k" unfolding lem4[rule_format] by auto

          also have "\<dots> \<le> p" using ksimplexD(4)[OF assms(1),rule_format,of a0 k] a0a1 by auto

          finally show "a3 j \<le> p" unfolding True by auto qed qed

      show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p" proof(rule,rule,cases "x=a3") fix j::nat assume j:"j\<notin>{1..n}"

        { case False thus "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto }

        case True show "x j = p" unfolding True a3_def using j k(1) 

          using ksimplexD(5)[OF assms(1),rule_format,OF `a0\<in>s` j] by auto qed

      fix y assume y:"y\<in>insert a3 (s - {a1})"

      have lem4:"\<And>x. x\<in>s \<Longrightarrow> x\<noteq>a1 \<Longrightarrow> kle n a3 x" proof- case goal1 hence *:"x\<in>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 ..

          thus ?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 thus ?case apply-apply(erule conjE)

              apply(erule_tac[!] x=j in allE) apply(cases "j\<in>kk") apply(case_tac[!] "j=k") by auto 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) by auto

        ultimately show ?case apply-apply(rule kle_between_l[of _ a0 _ a2]) using lem3[OF *]

          using a0a1(4)[rule_format,OF goal1(1)] by auto qed

      show "kle n x y \<or> kle n y x" proof(cases "y=a3")

        case True show ?thesis unfolding True apply(cases "x=a3") defer apply(rule disjI2,rule lem4)

          using x by auto next

        case False show ?thesis proof(cases "x=a3") case True show ?thesis unfolding True

            apply(rule disjI1,rule lem4) using y False by auto next

          case False thus ?thesis apply(rule_tac ksimplexD(6)[OF assms(1),rule_format]) 

            using x y `y\<noteq>a3` by auto qed qed qed

    hence "insert a3 (s - {a1}) \<in> ?A" unfolding mem_Collect_eq apply-apply(rule,assumption)

      apply(rule_tac x="a3" in bexI) unfolding `a=a1` using `a3\<notin>s` by auto moreover

    have "s \<in> ?A" using assms(1,2) by auto ultimately have  "?A \<supseteq> {s, insert a3 (s - {a1})}" by auto

    moreover have "?A \<subseteq> {s, insert a3 (s - {a1})}" apply(rule) unfolding mem_Collect_eq proof(erule conjE)

      fix s' assume as:"ksimplex p n s'" and "\<exists>b\<in>s'. s' - {b} = s - {a}"

      from this(2) guess a' .. note a'=this

      guess a_min a_max apply(rule ksimplex_extrema_strong[OF as assms(3)]) . note min_max=this

      have *:"\<forall>x\<in>s' - {a'}. x k = a2 k" unfolding a' proof fix x assume x:"x\<in>s-{a}"

        hence "kle n x a2" apply-apply(rule lem3) using `a=a1` by auto

        hence "x k \<le> a2 k" apply(drule_tac kle_imp_pointwise) by auto moreover

        { have "a2 k \<le> a0 k" using k(2)[rule_format,of k] unfolding a0a1(5)[rule_format] using k(1) by simp

          also have "\<dots> \<le> x k" using a0a1(4)[rule_format,of x,THEN conjunct1,THEN kle_imp_pointwise] x by auto

          finally have "a2 k \<le> x k" . } ultimately show "x k = a2 k" by auto qed

      have **:"a'=a_min \<or> a'=a_max" apply(rule ksimplex_fix_plane[OF a'(1) k(1) *]) using min_max by auto

      have "a2 \<noteq> a1" proof assume as:"a2 = a1"

        show False using k(2) unfolding as apply(erule_tac x=k in allE) by auto qed

      hence a2':"a2 \<in> s' - {a'}" unfolding a' using a2 unfolding `a=a1` by auto

      show "s' \<in> {s, insert a3 (s - {a1})}" proof(cases "a'=a_min")

        case True have "a_max \<in> s - {a1}" using min_max unfolding a'(2)[unfolded `a=a1`,THEN sym] True by auto

        hence "a_max = a2" unfolding kle_antisym[THEN sym,of a_max a2 n] apply-apply(rule)

          apply(rule lem3,assumption) apply(rule min_max(4)[rule_format,THEN conjunct2]) using a2' by auto

        hence a_max:"\<forall>i. a_max i = a2 i" by auto

        have *:"\<forall>j. a2 j = (if j\<in>{1..n} then a3 j + 1 else a3 j)" 

          using k(2) unfolding lem4[rule_format] a0a1(5)[rule_format] apply-apply(rule,erule_tac x=j in allE)

        proof- case goal1 thus ?case apply(cases "j\<in>{1..n}",case_tac[!] "j=k") by auto qed

        have "\<forall>i. a_min i = a3 i" using a_max apply-apply(rule,erule_tac x=i in allE)

          unfolding min_max(5)[rule_format] *[rule_format] proof- case goal1

          thus ?case apply(cases "i\<in>{1..n}") by auto qed hence "a_min = a3" unfolding fun_eq_iff .

        hence "s' = insert a3 (s - {a1})" using a' unfolding `a=a1` True by auto thus ?thesis by auto next

        case False hence as:"a'=a_max" using ** by auto

        have "a_min = a0" unfolding kle_antisym[THEN sym,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 \<in> s - {a1}" using min_max(1,3) unfolding a'(2)[THEN sym,unfolded `a=a1`] as by auto

          thus "a_min \<in> s" by auto have "a0 \<in> s - {a1}" using a0a1(1-3) by auto thus "a0 \<in> s'"

            unfolding a'(2)[THEN sym,unfolded `a=a1`] by auto qed

        hence "\<forall>i. a_max i = a1 i" unfolding a0a1(5)[rule_format] min_max(5)[rule_format] by auto

        hence "s' = s" apply-apply(rule lem1[OF a'(2)]) using `a\<in>s` `a'\<in>s'` unfolding as `a=a1` unfolding fun_eq_iff by auto

        thus ?thesis by auto qed qed 

    ultimately have *:"?A = {s, insert a3 (s - {a1})}" by blast

    have "s \<noteq> insert a3 (s - {a1})" using `a3\<notin>s` by auto

    hence ?thesis unfolding * by auto } moreover

  { assume as:"a\<noteq>a0" "a\<noteq>a1" have "\<not> (\<forall>x\<in>s. kle n a x)" proof case goal1

      have "a=a0" unfolding kle_antisym[THEN sym,of _ _ n] apply(rule)

        using goal1 a0a1 assms(2) by auto thus False using as by auto qed

    hence "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>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\<in>s`

    have "\<not> (\<forall>x\<in>s. kle n x a)" proof case goal1

      have "a=a1" unfolding kle_antisym[THEN sym,of _ _ n] apply(rule)

        using goal1 a0a1 assms(2) by auto thus False using as by auto qed

    hence "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>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\<in>s`

    def a' \<equiv> "\<lambda>j. if j = l then u j + 1 else u j"

    have kl:"k \<noteq> l" proof assume "k=l" have *:"\<And>P. (if P then (1::nat) else 0) \<noteq> 2" by auto

      thus 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)+ by(auto simp add: *) qed

    hence aa':"a'\<noteq>a" apply-apply rule unfolding fun_eq_iff unfolding a'_def k(2)

      apply(erule_tac x=l in allE) by auto

    have "a' \<notin> s" apply(rule) apply(drule ksimplexD(6)[OF assms(1),rule_format,OF `a\<in>s`]) proof(cases "kle n a a'")

      case goal2 hence "kle n a' a" by auto thus False apply(drule_tac kle_imp_pointwise)

        apply(erule_tac x=l in allE) unfolding a'_def k(2) using kl by auto next

      case True thus False apply(drule_tac kle_imp_pointwise)

        apply(erule_tac x=k in allE) unfolding a'_def k(2) using kl by auto 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) by auto

    have uxv:"\<And>x. kle n u x \<Longrightarrow> kle n x v \<Longrightarrow> (x = u) \<or> (x = a) \<or> (x = a') \<or> (x = v)"

    proof- case goal1 thus ?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

        thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next

      assume as:"x l \<noteq> 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) apply-

        using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1

        thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next

      assume as:"x l = u l" "x k \<noteq> u k"

      have "x = a" unfolding fun_eq_iff

        using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply-

        using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1

        thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next

      assume as:"x l \<noteq> u l" "x k \<noteq> u k"

      have "x = v" unfolding fun_eq_iff

        using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply-

        using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1

        thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as `k\<noteq>l` by auto qed thus ?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 by auto

    have lem3:"\<And>x. x\<in>s \<Longrightarrow> kle n v x \<Longrightarrow> 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\<in>s` by auto

    have lem4:"\<And>x. x\<in>s \<Longrightarrow> kle n x u \<Longrightarrow> 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\<in>s` by auto

    have lem5:"\<And>x. x\<in>s \<Longrightarrow> x\<noteq>a \<Longrightarrow> kle n x a' \<or> kle n a' x" proof- case goal1 thus ?case

      proof(cases "kle n v x \<or> kle n x u") case True thus ?thesis using goal1 by(auto intro:lem3 lem4) next

        case False hence *:"kle n u x" "kle n x v" using ksimplexD(6)[OF assms(1)] using goal1 `u\<in>s` `v\<in>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) proof(rule_tac[2-] ballI,rule_tac[4] ballI)

      show "card (insert a' (s - {a})) = n + 1" using ksimplexD(2-3)[OF assms(1)]

        using `a'\<noteq>a` `a'\<notin>s` `a\<in>s` by(auto simp add:card_insert_if)

      fix x assume x:"x \<in> insert a' (s - {a})"

      show "\<forall>j. x j \<le> p" proof(rule,cases "x = a'")

        fix j case False thus "x j\<le>p" using x ksimplexD(4)[OF assms(1)] by auto next

        fix j case True show "x j\<le>p" unfolding True proof(cases "j=l") 

          case False thus "a' j \<le>p" unfolding True a'_def using `u\<in>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\<noteq>l` by auto

          have "u l + 1 \<le> p" unfolding *[THEN sym] using ksimplexD(4)[OF assms(1)] using `v\<in>s` by auto

          thus "a' j \<le>p" unfolding a'_def True by auto qed qed

      show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p" proof(rule,rule,cases "x=a'") fix j::nat assume j:"j\<notin>{1..n}"

        { case False thus "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto }

        case True show "x j = p" unfolding True a'_def using j l(1) 

          using ksimplexD(5)[OF assms(1),rule_format,OF `u\<in>s` j] by auto qed

      fix y assume y:"y\<in>insert a' (s - {a})"

      show "kle n x y \<or> kle n y x" proof(cases "y=a'")

        case True show ?thesis unfolding True apply(cases "x=a'") defer apply(rule lem5) using x by auto 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 thus ?thesis apply(rule_tac ksimplexD(6)[OF assms(1),rule_format]) 

            using x y `y\<noteq>a'` by auto qed qed qed

    hence "insert a' (s - {a}) \<in> ?A" unfolding mem_Collect_eq apply-apply(rule,assumption)

      apply(rule_tac x="a'" in bexI) using aa' `a'\<notin>s` by auto moreover

    have "s \<in> ?A" using assms(1,2) by auto ultimately have  "?A \<supseteq> {s, insert a' (s - {a})}" by auto

    moreover have "?A \<subseteq> {s, insert a' (s - {a})}" apply(rule) unfolding mem_Collect_eq proof(erule conjE)

      fix s' assume as:"ksimplex p n s'" and "\<exists>b\<in>s'. s' - {b} = s - {a}"

      from this(2) guess a'' .. note a''=this

      have "u\<noteq>v" unfolding fun_eq_iff unfolding l(2) k(2) by auto

      hence uv':"\<not> kle n v u" using uv using kle_antisym by auto

      have "u\<noteq>a" "v\<noteq>a" unfolding fun_eq_iff k(2) l(2) by auto 

      hence uvs':"u\<in>s'" "v\<in>s'" using `u\<in>s` `v\<in>s` using a'' by auto

      have lem6:"a \<in> s' \<or> a' \<in> s'" proof(cases "\<forall>x\<in>s'. kle n x u \<or> kle n v x")

        case False then guess w unfolding ball_simps .. note w=this

        hence "kle n u w" "kle n w v" using ksimplexD(6)[OF as] uvs' by auto

        hence "w = a' \<or> w = a" using uxv[of w] uvs' w by auto thus ?thesis using w by auto next

        case True have "\<not> (\<forall>x\<in>s'. kle n x u)" unfolding ball_simps apply(rule_tac x=v in bexI)

          using uv `u\<noteq>v` unfolding kle_antisym[of n u v,THEN sym] using `v\<in>s'` by auto

        hence "\<exists>y\<in>s'. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then u j + 1 else u j)" using ksimplex_successor[OF as `u\<in>s'`] by blast

        then guess w .. note w=this from this(2) guess kk .. note kk=this[rule_format]

        have "\<not> kle n w u" apply-apply(rule,drule kle_imp_pointwise) 

          apply(erule_tac x=kk in allE) unfolding kk by auto 

        hence *:"kle n v w" using True[rule_format,OF w(1)] by auto

        hence False proof(cases "kk\<noteq>l") case True thus False using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)]

            apply(erule_tac x=l in allE) using `k\<noteq>l` by auto  next

          case False hence "kk\<noteq>k" using `k\<noteq>l` by auto thus False using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)]

            apply(erule_tac x=k in allE) using `k\<noteq>l` by auto qed

        thus ?thesis by auto qed

      thus "s' \<in> {s, insert a' (s - {a})}" proof(cases "a\<in>s'")

        case True hence "s' = s" apply-apply(rule lem1[OF a''(2)]) using a'' `a\<in>s` by auto

        thus ?thesis by auto next case False hence "a'\<in>s'" using lem6 by auto

        hence "s' = insert a' (s - {a})" apply-apply(rule lem1[of _ a'' _ a'])

          unfolding a''(2)[THEN sym] using a'' using `a'\<notin>s` by auto

        thus ?thesis by auto qed qed 

    ultimately have *:"?A = {s, insert a' (s - {a})}" by blast

    have "s \<noteq> insert a' (s - {a})" using `a'\<notin>s` by auto

    hence ?thesis unfolding * by auto } 

  ultimately show ?thesis by auto qed

subsection {* Hence another step towards concreteness. *}

lemma kuhn_simplex_lemma:

  assumes "\<forall>s. ksimplex p (n + 1) s \<longrightarrow> (rl ` s \<subseteq>{0..n+1})"

  "odd (card{f. \<exists>s a. ksimplex p (n + 1) s \<and> a \<in> s \<and> (f = s - {a}) \<and>

  (rl ` f = {0 .. n}) \<and> ((\<exists>j\<in>{1..n+1}.\<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n+1}.\<forall>x\<in>f. x j = p))})"

  shows "odd(card {s\<in>{s. ksimplex p (n + 1) s}. rl ` s = {0..n+1} })" proof-

  have *:"\<And>x y. x = y \<Longrightarrow> odd (card x) \<Longrightarrow> odd (card y)" by auto

  have *:"odd(card {f\<in>{f. \<exists>s\<in>{s. ksimplex p (n + 1) s}. (\<exists>a\<in>s. f = s - {a})}. 

                (rl ` f = {0..n}) \<and>

               ((\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = 0) \<or>

                (\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = p))})" apply(rule *[OF _ assms(2)]) by auto

  show ?thesis apply(rule kuhn_complete_lemma[OF finite_simplices]) prefer 6 apply(rule *) apply(rule,rule,rule)

    apply(subst ksimplex_def) defer apply(rule,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\<in>s" "f = s - {a}"

    let ?S = "{s. ksimplex p (n + 1) s \<and> (\<exists>a\<in>s. f = s - {a})}"

    have S:"?S = {s'. ksimplex p (n + 1) s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})}" unfolding as by blast

    { fix j assume j:"j \<in> {1..n + 1}" "\<forall>x\<in>f. x j = 0" thus "card {s. ksimplex p (n + 1) s \<and> (\<exists>a\<in>s. f = s - {a})} = 1" unfolding S

        apply-apply(rule ksimplex_replace_0) apply(rule as)+ unfolding as by auto }

    { fix j assume j:"j \<in> {1..n + 1}" "\<forall>x\<in>f. x j = p" thus "card {s. ksimplex p (n + 1) s \<and> (\<exists>a\<in>s. f = s - {a})} = 1" unfolding S

        apply-apply(rule ksimplex_replace_1) apply(rule as)+ unfolding as by auto }

    show "\<not> ((\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = p)) \<Longrightarrow> card ?S = 2"

      unfolding S apply(rule ksimplex_replace_2) apply(rule as)+ unfolding as by auto qed auto qed