src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy

tuned proofs -- clarified flow of facts wrt. calculation;

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

(** move this **)
lemma divide_nonneg_nonneg:
  assumes "a \<ge> 0" "b \<ge> 0"
  shows "0 \<le> a / (b::real)"
  apply (cases "b=0")
  defer
  apply (rule divide_nonneg_pos)
  using assms
  apply auto
  done

lemma brouwer_compactness_lemma:
  fixes f :: "'a::metric_space \<Rightarrow> 'b::euclidean_space"
  assumes "compact s" "continuous_on s f" "\<not> (\<exists>x\<in>s. (f x = 0))"
  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))+
  with False 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"] unfolding o_def by auto
  have "(norm \<circ> f) x > 0" using assms(3) and x(1) by auto
  then show ?thesis by (rule that) (insert x(2), auto simp: o_def)
next
  case True
  show thesis by (rule that [of 1]) (auto simp: True)
qed

lemma kuhn_labelling_lemma:
  fixes P Q :: "'a::euclidean_space \<Rightarrow> bool"
  assumes "(\<forall>x. P x \<longrightarrow> P (f x))"
    and "\<forall>x. P x \<longrightarrow> (\<forall>i\<in>Basis. Q i \<longrightarrow> 0 \<le> x\<bullet>i \<and> x\<bullet>i \<le> 1)"
  shows "\<exists>l. (\<forall>x.\<forall>i\<in>Basis. l x i \<le> (1::nat)) \<and>
             (\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (x\<bullet>i = 0) \<longrightarrow> (l x i = 0)) \<and>
             (\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (x\<bullet>i = 1) \<longrightarrow> (l x i = 1)) \<and>
             (\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (l x i = 0) \<longrightarrow> x\<bullet>i \<le> f(x)\<bullet>i) \<and>
             (\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (l x i = 1) \<longrightarrow> f(x)\<bullet>i \<le> x\<bullet>i)"
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 Ball_def
    apply (subst choice_iff[symmetric])+
    apply rule
    apply rule
  proof -
    case (goal1 x)
    let ?R = "\<lambda>y. (P x \<and> Q xa \<and> x \<bullet> xa = 0 \<longrightarrow> y = (0::nat)) \<and>
        (P x \<and> Q xa \<and> x \<bullet> xa = 1 \<longrightarrow> y = 1) \<and>
        (P x \<and> Q xa \<and> y = 0 \<longrightarrow> x \<bullet> xa \<le> f x \<bullet> xa) \<and>
        (P x \<and> Q xa \<and> y = 1 \<longrightarrow> f x \<bullet> xa \<le> x \<bullet> xa)"
    {
      assume "P x" "Q xa" "xa\<in>Basis"
      then have "0 \<le> f x \<bullet> xa \<and> f x \<bullet> xa \<le> 1"
        using assms(2)[rule_format,of "f x" xa]
        apply (drule_tac assms(1)[rule_format])
        apply auto
        done
    }
    then have "xa\<in>Basis \<Longrightarrow> ?R 0 \<or> ?R 1" by auto
    then show ?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[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 (\<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
    apply auto
    done
  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)
    apply auto
    done
  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)
    apply auto
    done
  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)
    apply auto
    done
  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 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
    done
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 (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 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 s: "s = {x, y}" "x\<noteq>y" unfolding numeral_2_eq_2
    apply -
    apply (erule exE conjE | drule card_eq_SucD)+
    apply auto
    done
  show "\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y)"
    using s 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 obtain x y where "x\<in>s" "y\<in>s" "x \<noteq> y" "\<forall>z\<in>s. z = x \<or> z = y"
    by auto
  then have "s = {x, y}" by auto
  with `x \<noteq> y` show "card s = 2" 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[symmetric]
    apply (rule card_image)
    unfolding inj_on_def
    apply (rule, rule, rule)
    unfolding mem_Collect_eq
    apply auto
    done
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) apply auto
    done
  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]
    apply auto
    done
  show ?thesis
    apply (rule image_lemma_0)
    unfolding *
    apply auto
    done
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
  then show ?thesis
    apply -
    apply (rule disjI1, rule image_lemma_0)
    using assms(1)
    apply auto
    done
next
  let ?M = "{a\<in>s. f ` (s - {a}) = t - {b}}"
  case False
  then obtain a where "a\<in>?M" by auto
  then have a: "a\<in>s" "f ` (s - {a}) = t - {b}" by auto
  have "f a \<in> t - {b}" using a and assms by auto
  then have "\<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
  then have *: "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
    then show "x \<in> 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\<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
      apply auto
      done
    show "z = a \<or> z = c"
    proof (rule ccontr)
      assume "\<not> ?thesis"
      then show 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`
        apply auto
        done
    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 **
    apply auto
    done
  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
  then have 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
    unfolding *[OF s, unfolded mem_Collect_eq, where P="\<lambda>x. rl ` x = {0..n}"]
    apply auto
    done
  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
    apply auto
    done
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 auto
  done

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
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
    then show ?thesis
      apply -
      apply (rule, rule_tac[!] x=x in bexI)
      apply auto
      done
  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"
      then show ?thesis
        apply (rule_tac x=a in bexI)
        using a apply auto
        done
    next
      assume "\<forall>j. x j \<le> 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 "\<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"
      then show ?thesis
        apply(rule_tac x=b in bexI) using b
        apply auto
        done
    next
      assume "\<forall>j. b j \<le> 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
  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)+
  apply auto
  done

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
  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 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
  then have "x = y"
    apply -
    apply (rule ext)
    using k apply auto
    done
  then show ?thesis using assms(2) by auto
next
  case False
  then have "(SOME k'. k' \<in> k) \<in> k"
    apply -
    apply (rule someI_ex)
    apply auto
    done
  then show ?thesis
    apply (rule_tac x = "SOME k'. k' \<in> k" in exI)
    using k apply auto
    done
  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
    apply auto
    done
  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"
      then have "x = a"
        apply -
        unfolding pointwise_antisym[symmetric]
        apply (drule kle_imp_pointwise)
        using a(2)[rule_format,OF `x\<in>s`]
        apply auto
        done
      then show ?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 apply auto
    done
  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[symmetric]
        apply (drule kle_imp_pointwise)
        using a(2)[rule_format,OF `x\<in>s`] apply auto
        done
      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)
    apply auto
    done
  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)]
    apply auto
    done
  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)]
    apply auto
    done
  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)
      apply auto
      done
    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)
      apply auto
      done
    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"
    and "kle n y z"
    and "kle n x z \<or> kle n z x"
    and "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"
    and "kle n y z"
    and "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"
    and "\<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
  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
        apply auto
        done
      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)
        apply auto
        done
    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)
  apply auto
  done

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]
    apply auto
    done
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]
    apply auto
    done
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)
    apply (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
      apply auto
      done
    then show "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
    then show "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
    apply auto
    done
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
    apply auto
    done
  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`
    apply auto
    done
  moreover
  have "card {1..n} \<ge> card {k\<in>{1..n}. a(k) < b(k)}"
    by (rule card_mono) auto
  ultimately
  have *: "{k\<in>{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 \<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)])
    apply auto
    done
  have "a \<noteq> b"
    apply (rule notI)
    apply (drule cong[of _ _ 1 1])
    using ab(4) assms(2) apply auto
    done
  thus ?thesis
    apply (rule_tac that[of a b])
    using ab apply auto
    done
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
  then have **: "1 \<le> card {k\<in>{1..n}. a k < b k}"
    apply -
    apply (rule kle_strict_set)
    using assm(6) and `a\<in>s`
    apply (auto simp add:kle_refl)
    done

  let ?kle1 = "{x \<in> s. \<not> kle n x a}"
  have "card ?kle1 > 0"
    apply (rule ccontr)
    using assm(2) and False
    apply auto
    done
  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)
    apply auto
    done
  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)
      apply auto
      done
    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
      apply auto
      done
    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 blast+
      done
    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 blast+
      done
    moreover have "card {k \<in> {1..n}. e k < d k} \<le> 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, 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
      apply auto
      done
    show "b j = (if j = k then a j + 1 else a j)"
    proof (cases "j \<in> 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 \<noteq> 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\<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`
    apply (auto simp add: kle_refl)
    done

  let ?kle1 = "{x \<in> s. \<not> kle n a x}"
  have "card ?kle1 > 0"
    apply (rule ccontr)
    using assm(2) and False
    apply auto
    done
  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)
    apply auto
    done
  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 and `a\<in>s` assm(6)
      apply auto
      done
    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 and assm(6) and b
      apply auto
      done
    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`
      apply blast+
      done
    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 blast+
      done
    moreover have "card {k \<in> {1..n}. e k > d k} \<le> 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,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
      apply auto
      done
    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
        apply auto
        done
      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 and False by auto
    qed
  qed (insert k(1) `b\<in>s`, auto)
qed


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

(* FIXME: These are clones of lemmas in Library/FuncSet *)
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)
  case 0
  have [simp]: "{f. \<forall>x. f x = d} = {\<lambda>x. d}"
    apply (rule set_eqI,rule)
    unfolding mem_Collect_eq
    apply (rule, rule ext)
    apply auto
    done
  from 0 show ?case by auto
next
  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 = "(\<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
    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 (rule_tac card_ge_0_finite) simp
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
    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)
  apply auto
  done

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 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 \<in>s - {a}" "y \<in>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 \<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 notI)
        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)
        apply auto
        done
    next
      case False
      hence "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 \<notin> k" using xyp by auto
      then have "\<not> (\<exists>x\<in>k. x\<notin>{1..n})"
        apply -
        apply (rule notI)
        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
        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 \<in> s - {a}" "j\<notin>{1..n}"
    thus "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 \<equiv> "\<lambda>i. if i = (n + 1) then p - 1 else a i"
  have "c \<notin> f"
    apply (rule notI)
    apply (drule assms(2)[rule_format])
    unfolding c_def
    using assms(1)
    apply auto
    done
  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)
        apply auto
        done
    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
      apply auto
      done
    {
      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)
          done
        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)
          apply auto
          done
        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)
    apply auto
    done
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]]
    apply simp
    done

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"
  then have *: "a0 \<in> 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 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 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
    hence "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
    done
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 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"
      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}")
        apply auto
        done
    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, 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
    done
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 by (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`]])
      apply auto
      done
    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)
        apply auto
        done
    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)
        apply auto
        done
      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]
          by (elim exE 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)
          apply auto
          done
      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
          apply auto
          done
      next
        case False
        show ?thesis
        proof (cases "x = a3")
          case True
          show ?thesis
            unfolding True
            apply (rule disjI2, rule lem4)
            using y False
            apply auto
            done
        next
          case False
          thus ?thesis
            apply (rule_tac ksimplexD(6)[OF assms(1),rule_format])
            using x y `y \<noteq> a3`
            apply auto
            done
        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`
      apply auto
      done
    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 by (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`
          apply auto
          done
        hence "a2 k \<le> x k"
          apply (drule_tac kle_imp_pointwise)
          apply auto
          done
        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
        apply auto
        done
      show "s' \<in> {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\<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 by (cases "x\<in>{1..n}") auto
        qed
        hence "s' = s"
          apply -
          apply (rule lem1[OF a'(2)])
          using `a\<in>s` `a'\<in>s'`
          apply auto
          done
        thus ?thesis by auto
      next
        case False
        hence 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 \<in> s - {a0}"
            unfolding a'(2)[symmetric,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)[symmetric] 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}`
            apply auto
            done
        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`
          apply auto
          done
        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`]])
      apply auto
      done
    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)
        apply auto
        done
      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)
      apply auto
      done
    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
        next
          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")
              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 \<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
          apply auto
          done
      next
        case False
        show ?thesis
        proof (cases "x = a3")
          case True
          show ?thesis
            unfolding True
            apply (rule disjI1, rule lem4)
            using y False
            apply auto
            done
        next
          case False
          thus ?thesis
            apply (rule_tac ksimplexD(6)[OF assms(1),rule_format])
            using x y `y\<noteq>a3`
            apply auto
            done
        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`
        apply auto
        done
    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 by (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`
          apply auto
          done
        hence "x k \<le> a2 k"
          apply (drule_tac kle_imp_pointwise)
          apply auto
          done
        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
        apply auto
        done
      have "a2 \<noteq> a1"
      proof
        assume as: "a2 = a1"
        show False
          using k(2)
          unfolding as
          apply (erule_tac x = k in allE)
          apply auto
          done
      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`,symmetric] True
          by auto
        hence "a_max = a2"
          unfolding kle_antisym[symmetric,of a_max a2 n]
          apply -
          apply rule
          apply (rule lem3,assumption)
          apply (rule min_max(4)[rule_format,THEN conjunct2])
          using a2'
          apply auto
          done
        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 by (cases "j\<in>{1..n}",case_tac[!] "j=k") 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 by (cases "i\<in>{1..n}") 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[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 \<in> s - {a1}"
            using min_max(1,3)
            unfolding a'(2)[symmetric,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)[symmetric,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
          apply auto
          done
        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[symmetric,of _ _ n]
        apply rule
        using goal1 a0a1 assms(2)
        apply auto
        done
      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[symmetric,of _ _ n]
        apply rule
        using goal1 a0a1 assms(2)
        apply auto
        done
      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)+
        apply (auto simp add: *)
        done
    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)
      apply auto
      done
    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
        apply auto
        done
    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
        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: "\<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)
          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
            apply auto
            done
        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)
          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
            apply auto
            done
        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)
          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`
            apply auto
            done
        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
      apply auto
      done
    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`
      apply auto
      done
    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`
      apply auto
      done
    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 *[symmetric] 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
        next
          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
          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
          thus ?thesis
            apply (rule_tac ksimplexD(6)[OF assms(1),rule_format])
            using x y `y\<noteq>a'`
            apply auto
            done
        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`
      apply auto
      done
    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,symmetric]
          using `v\<in>s'`
          apply auto
          done
        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
          apply auto
          done
        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`
            apply auto  
            done
        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`
            apply auto
            done
        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`
          apply auto
          done
        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)[symmetric] using a'' and `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)])
    apply auto
    done
  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
        apply auto
        done
    }
    {
      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
        apply auto
        done
    }
    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
      apply auto
      done
  qed auto
qed


subsection {* Reduced labelling. *}

definition "reduced label (n::nat) (x::nat\<Rightarrow>nat) =
  (SOME k. k \<le> n \<and> (\<forall>i. 1\<le>i \<and> i<k+1 \<longrightarrow> label x i = 0) \<and>
    (k = n \<or> label x (k + 1) \<noteq> (0::nat)))"

lemma reduced_labelling:
  shows "reduced label n x \<le> n" (is ?t1)
    and "\<forall>i. 1\<le>i \<and> i < reduced label n x + 1 \<longrightarrow> (label x i = 0)" (is ?t2)
    and "(reduced label n x = n) \<or> (label x (reduced label n x + 1) \<noteq> 0)"  (is ?t3)
proof -
  have num_WOP: "\<And>P k. P (k::nat) \<Longrightarrow> \<exists>n. P n \<and> (\<forall>m<n. \<not> P m)"
    apply (drule ex_has_least_nat[where m="\<lambda>x. x"])
    apply (erule exE,rule_tac x=x in exI)
    apply auto
    done
  have *: "n \<le> n \<and> (label x (n + 1) \<noteq> 0 \<or> n = n)" by auto
  then guess N
    apply (drule_tac num_WOP[of "\<lambda>j. j\<le>n \<and> (label x (j+1) \<noteq> 0 \<or> n = j)"])
    apply (erule exE)
    done
  note N = this
  have N': "N \<le> n"
    "\<forall>i. 1 \<le> i \<and> i < N + 1 \<longrightarrow> label x i = 0" "N = n \<or> label x (N + 1) \<noteq> 0"
    defer
  proof (rule, rule)
    fix i
    assume i: "1\<le>i \<and> i<N+1"
    thus "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])
    done
qed

lemma reduced_labelling_unique:
  fixes x :: "nat \<Rightarrow> nat"
  assumes "r \<le> n"
    "\<forall>i. 1 \<le> i \<and> i < r + 1 \<longrightarrow> (label x i = 0)" "(r = n) \<or> (label x (r + 1) \<noteq> 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
  done

lemma reduced_labelling_zero:
  assumes "j\<in>{1..n}" "label x j = 0"
  shows "reduced label n x \<noteq> j - 1"
  using reduced_labelling[of label n x]
  using assms by fastforce

lemma reduced_labelling_nonzero:
  assumes "j\<in>{1..n}" "label x j \<noteq> 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
  done

lemma reduced_labelling_Suc:
  assumes "reduced lab (n + 1) x \<noteq> 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
  done

lemma complete_face_top:
  assumes "\<forall>x\<in>f. \<forall>j\<in>{1..n+1}. x j = 0 \<longrightarrow> lab x j = 0"
          "\<forall>x\<in>f. \<forall>j\<in>{1..n+1}. x j = p \<longrightarrow> lab x j = 1"
  shows "((reduced lab (n + 1)) ` 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)) \<longleftrightarrow>
  ((reduced lab (n + 1)) ` f = {0..n}) \<and> (\<forall>x\<in>f. x (n + 1) = p)" (is "?l = ?r")
proof
  assume ?l (is "?as \<and> (?a \<or> ?b)")
  thus ?r
    apply -
    apply (rule, erule conjE, assumption)
  proof (cases ?a)
    case True
    then guess j .. note j = this
    {
      fix x
      assume x: "x \<in> f"
      have "reduced lab (n + 1) x \<noteq> 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 \<in> {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
    thus "\<forall>x\<in>f. x (n + 1) = p" by auto
  next
    case False
    hence ?b using `?l` by blast
    then guess j .. note j = this
    {
      fix x
      assume x: "x \<in> 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)
      case goal1
      hence "j < n + 1" using j by auto
      moreover
      have "n \<in> {0..n}" by auto
      then guess y unfolding `?l`[THEN conjunct1,symmetric] image_iff ..
      ultimately show False using *[of y] by auto
    qed
    thus "\<forall>x\<in>f. x (n + 1) = p" using j by auto
  qed
qed(auto)


subsection {* Hence we get just about the nice induction. *}

lemma kuhn_induction:
  assumes "0 < p" "\<forall>x. \<forall>j\<in>{1..n+1}. (\<forall>j. x j \<le> p) \<and> (x j = 0) \<longrightarrow> (lab x j = 0)"
    "\<forall>x. \<forall>j\<in>{1..n+1}. (\<forall>j. x j \<le> p) \<and> (x j = p) \<longrightarrow> (lab x j = 1)"
    "odd (card {f. ksimplex p n f \<and> ((reduced lab n) ` f = {0..n})})"
  shows "odd (card {s. ksimplex p (n+1) s \<and>((reduced lab (n+1)) `  s = {0..n+1})})"
proof -
  have *: "\<And>s t. odd (card s) \<Longrightarrow> s = t \<Longrightarrow> odd (card t)"
    "\<And>s f. (\<And>x. f x \<le> n +1 ) \<Longrightarrow> f ` s \<subseteq> {0..n+1}" by auto
  show ?thesis
    apply (rule kuhn_simplex_lemma[unfolded mem_Collect_eq])
    apply (rule, rule, rule *, rule reduced_labelling)
    apply (rule *(1)[OF assms(4)])
    apply (rule set_eqI)
    unfolding mem_Collect_eq
    apply (rule, erule conjE)
    defer
    apply rule
  proof -
    fix f
    assume as: "ksimplex p n f" "reduced lab n ` f = {0..n}"
    have *: "\<forall>x\<in>f. \<forall>j\<in>{1..n + 1}. x j = 0 \<longrightarrow> lab x j = 0"
      "\<forall>x\<in>f. \<forall>j\<in>{1..n + 1}. x j = p \<longrightarrow> lab x j = 1"
      using assms(2-3) using as(1)[unfolded ksimplex_def] by auto
    have allp: "\<forall>x\<in>f. x (n + 1) = p"
      using assms(2) using as(1)[unfolded ksimplex_def] by auto
    {
      fix x
      assume "x \<in> f"
      hence "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
      hence "reduced lab (n + 1) x = reduced lab n x"
        apply -
        apply (rule reduced_labelling_Suc)
        using reduced_labelling(1)
        apply auto
        done
    }
    hence "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 "\<exists>s a. ksimplex p (n + 1) s \<and>
      a \<in> s \<and> f = s - {a} \<and> reduced lab (n + 1) ` 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))" (is ?ex)
      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: "\<exists>s a. ksimplex p (n + 1) s \<and>
      a \<in> s \<and> f = s - {a} \<and> reduced lab (n + 1) ` 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))" (is ?ex)
    then guess s ..
    then guess a
      apply -
      apply (erule exE,(erule conjE)+)
      done
    note sa = this
    {
      fix x
      assume "x \<in> f"
      hence "reduced lab (n + 1) x \<in> reduced lab (n + 1) ` f"
        by auto
      hence "reduced lab (n + 1) x < n + 1"
        using sa(4) by auto
      hence "reduced lab (n + 1) x = reduced lab n x"
        apply -
        apply (rule reduced_labelling_Suc)
        using reduced_labelling(1)
        apply auto
        done
    }
    thus part1: "reduced lab n ` f = {0..n}"
      unfolding sa(4)[symmetric]
      apply -
      apply (rule set_eqI)
      unfolding image_iff
      apply auto
      done
    have *: "\<forall>x\<in>f. x (n + 1) = p"
    proof (cases "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0")
      case True
      then guess j ..
      hence "\<And>x. x \<in> f \<Longrightarrow> reduced lab (n + 1) x \<noteq> 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 \<in> {0..n}" using `j\<in>{1..n+1}` by auto
      ultimately have False
        unfolding sa(4)[symmetric]
        unfolding image_iff
        by fastforce
      thus ?thesis by auto
    next
      case False
      hence "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p"
        using sa(5) by fastforce then guess j .. note j=this
      thus ?thesis
      proof (cases "j = n + 1")
        case False hence *: "j \<in> {1..n}"
          using j by auto
        hence "\<And>x. x \<in> f \<Longrightarrow> reduced lab n x < j"
          apply (rule reduced_labelling_nonzero)
        proof -
          fix x
          assume "x \<in> f"
          hence "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
          thus "lab x j \<noteq> 0" by auto
        qed
        moreover have "j \<in> {0..n}" using * by auto
        ultimately have False
          unfolding part1[symmetric]
          using * unfolding image_iff
          by auto
        thus ?thesis by auto
      qed auto
    qed
    thus "ksimplex p n f"
      using as unfolding simplex_top_face[OF assms(1) *,symmetric] by auto
  qed
qed

lemma kuhn_induction_Suc:
  assumes "0 < p" "\<forall>x. \<forall>j\<in>{1..Suc n}. (\<forall>j. x j \<le> p) \<and> (x j = 0) \<longrightarrow> (lab x j = 0)"
                  "\<forall>x. \<forall>j\<in>{1..Suc n}. (\<forall>j. x j \<le> p) \<and> (x j = p) \<longrightarrow> (lab x j = 1)"
        "odd (card {f. ksimplex p n f \<and> ((reduced lab n) ` f = {0..n})})"
  shows "odd (card {s. ksimplex p (Suc n) s \<and>((reduced lab (Suc n)) `  s = {0..Suc n})})"
  using assms unfolding Suc_eq_plus1 by(rule kuhn_induction)


subsection {* And so we get the final combinatorial result. *}

lemma ksimplex_0: "ksimplex p 0 s \<longleftrightarrow> s = {(\<lambda>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 = (\<lambda>x. p)"
    using ksimplexD(5)[OF l, rule_format, OF a(1)] by rule auto
  thus ?r using a by auto
next
  assume r: ?r
  show ?l unfolding r ksimplex_eq by auto
qed

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

lemma kuhn_combinatorial:
  assumes "0 < p" "\<forall>x j. (\<forall>j. x(j) \<le> p) \<and> 1 \<le> j \<and> j \<le> n \<and> (x j = 0) \<longrightarrow> (lab x j = 0)"
    "\<forall>x j. (\<forall>j. x(j) \<le> p) \<and> 1 \<le> j \<and> j \<le> n  \<and> (x j = p) \<longrightarrow> (lab x j = 1)"
  shows " odd (card {s. ksimplex p n s \<and> ((reduced lab n) ` s = {0..n})})"
  using assms
proof (induct n)
  let ?M = "\<lambda>n. {s. ksimplex p n s \<and> ((reduced lab n) ` s = {0..n})}"
  {
    case 0
    have *: "?M 0 = {{(\<lambda>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
    thus ?case
      apply -
      apply (rule kuhn_induction_Suc)
      using Suc(2-)
      apply auto
      done
  }
qed

lemma kuhn_lemma:
  assumes "0 < (p::nat)" "0 < (n::nat)"
    "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. (label x i = (0::nat)) \<or> (label x i = 1))"
    "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. (x i = 0) \<longrightarrow> (label x i = 0))"
    "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. (x i = p) \<longrightarrow> (label x i = 1))"
  obtains q where "\<forall>i\<in>{1..n}. q i < p"
    "\<forall>i\<in>{1..n}. \<exists>r s. (\<forall>j\<in>{1..n}. q(j) \<le> r(j) \<and> r(j) \<le> q(j) + 1) \<and>
                                 (\<forall>j\<in>{1..n}. q(j) \<le> s(j) \<and> s(j) \<le> q(j) + 1) \<and>
                                 ~(label r i = label s i)"
proof -
  let ?A = "{s. ksimplex p n s \<and> reduced label n ` s = {0..n}}"
  have "n \<noteq> 0" using assms by auto
  have conjD:"\<And>P Q. P \<and> Q \<Longrightarrow> P" "\<And>P Q. P \<and> Q \<Longrightarrow> Q"
    by auto
  have "odd (card ?A)"
    apply (rule kuhn_combinatorial[of p n label])
    using assms
    apply auto
    done
  hence "card ?A \<noteq> 0"
    apply -
    apply (rule ccontr)
    apply auto
    done
  hence "?A \<noteq> {}" unfolding card_eq_0_iff by auto
  then obtain s where "s \<in> ?A"
    by auto note s=conjD[OF this[unfolded mem_Collect_eq]]
  guess a b by (rule ksimplex_extrema_strong[OF s(1) `n\<noteq>0`]) note ab = this
  show ?thesis
    apply (rule that[of a])
    apply (rule_tac[!] ballI)
  proof -
    fix i
    assume "i\<in>{1..n}"
    hence "a i + 1 \<le> 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
    thus "a i < p" by auto
  next
    case goal2
    hence "i \<in> reduced label n ` s" using s by auto
    then guess u unfolding image_iff .. note u = this
    from goal2 have "i - 1 \<in> 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 \<noteq> 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 \<in> {1..n}"
      show "a j \<le> u j \<and> u j \<le> a j + 1" "a j \<le> v j \<and> v j \<le> 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
  qed
qed


subsection {* The main result for the unit cube. *}

lemma kuhn_labelling_lemma':
  assumes "(\<forall>x::nat\<Rightarrow>real. P x \<longrightarrow> P (f x))"  "\<forall>x. P x \<longrightarrow> (\<forall>i::nat. Q i \<longrightarrow> 0 \<le> x i \<and> x i \<le> 1)"
  shows "\<exists>l. (\<forall>x i. l x i \<le> (1::nat)) \<and>
             (\<forall>x i. P x \<and> Q i \<and> (x i = 0) \<longrightarrow> (l x i = 0)) \<and>
             (\<forall>x i. P x \<and> Q i \<and> (x i = 1) \<longrightarrow> (l x i = 1)) \<and>
             (\<forall>x i. P x \<and> Q i \<and> (l x i = 0) \<longrightarrow> x i \<le> f(x) i) \<and>
             (\<forall>x i. P x \<and> Q i \<and> (l x i = 1) \<longrightarrow> f(x) i \<le> x i)"
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[symmetric])+
  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"
      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])
        apply auto
        done
    }
    hence "?R 0 \<or> ?R 1" by auto
    thus ?case by auto
  qed
qed

lemma brouwer_cube:
  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'a::ordered_euclidean_space"
  assumes "continuous_on {0..(\<Sum>Basis)} f" "f ` {0..(\<Sum>Basis)} \<subseteq> {0..(\<Sum>Basis)}"
  shows "\<exists>x\<in>{0..(\<Sum>Basis)}. f x = x"
proof (rule ccontr)
  def n \<equiv> "DIM('a)"
  have n: "1 \<le> n" "0 < n" "n \<noteq> 0"
    unfolding n_def by (auto simp add: Suc_le_eq DIM_positive)
  assume "\<not> (\<exists>x\<in>{0..\<Sum>Basis}. f x = x)"
  hence *: "\<not> (\<exists>x\<in>{0..\<Sum>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 *: "\<forall>x. x \<in> {0..\<Sum>Basis} \<longrightarrow> f x \<in> {0..\<Sum>Basis}"  "\<forall>x. x \<in> {0..(\<Sum>Basis)::'a} \<longrightarrow>
    (\<forall>i\<in>Basis. True \<longrightarrow> 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1)"
    using assms(2)[unfolded image_subset_iff Ball_def]
    unfolding mem_interval by auto
  guess label using kuhn_labelling_lemma[OF *] by (elim exE conjE)
  note label = this [rule_format]
  have lem1: "\<forall>x\<in>{0..\<Sum>Basis}.\<forall>y\<in>{0..\<Sum>Basis}.\<forall>i\<in>Basis. label x i \<noteq> label y i
    \<longrightarrow> abs(f x \<bullet> i - x \<bullet> i) \<le> norm(f y - f x) + norm(y - x)"
  proof safe
    fix x y :: 'a
    assume xy: "x\<in>{0..\<Sum>Basis}" "y\<in>{0..\<Sum>Basis}"
    fix i
    assume i: "label x i \<noteq> label y i" "i \<in> Basis"
    have *: "\<And>x y fx fy :: real. x \<le> fx \<and> fy \<le> y \<or> fx \<le> x \<and> y \<le> fy \<Longrightarrow>
      abs (fx - x) \<le> abs (fy - fx) + abs (y - x)" by auto
    have "\<bar>(f x - x) \<bullet> i\<bar> \<le> abs((f y - f x)\<bullet>i) + abs((y - x)\<bullet>i)"
      unfolding inner_simps
      apply (rule *)
      apply (cases "label x i = 0")
      apply (rule disjI1, rule)
      prefer 3
    proof (rule disjI2, rule)
      assume lx: "label x i = 0"
      hence ly: "label y i = 1"
        using i label(1)[of i y] by auto
      show "x \<bullet> i \<le> f x \<bullet> i"
        apply (rule label(4)[rule_format])
        using xy lx i(2)
        apply auto
        done
      show "f y \<bullet> i \<le> y \<bullet> i"
        apply (rule label(5)[rule_format])
        using xy ly i(2)
        apply auto
        done
    next
      assume "label x i \<noteq> 0"
      hence 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 \<bullet> i \<le> x \<bullet> i"
        apply (rule label(5)[rule_format])
        using xy l i(2)
        apply auto
        done
      show "y \<bullet> i \<le> f y \<bullet> i"
        apply (rule label(4)[rule_format])
        using xy l i(2)
        apply auto
        done
    qed
    also have "\<dots> \<le> norm (f y - f x) + norm (y - x)"
      apply (rule add_mono)
      apply (rule Basis_le_norm[OF i(2)])+
      done
    finally show "\<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y - f x) + norm (y - x)"
      unfolding inner_simps .
  qed
  have "\<exists>e>0. \<forall>x\<in>{0..\<Sum>Basis}. \<forall>y\<in>{0..\<Sum>Basis}. \<forall>z\<in>{0..\<Sum>Basis}. \<forall>i\<in>Basis.
    norm(x - z) < e \<and> norm(y - z) < e \<and> label x i \<noteq> label y i \<longrightarrow> abs((f(z) - z)\<bullet>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..\<Sum>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 \<in> {0..\<Sum>Basis}" "y \<in> {0..\<Sum>Basis}" "z \<in> {0..\<Sum>Basis}"
        "norm (x - z) < min (e / 2) (d / real n / 8)"
        "norm (y - z) < min (e / 2) (d / real n / 8)" "label x i \<noteq> label y i"
        and i: "i \<in> Basis"
      have *: "\<And>z fz x fx n1 n2 n3 n4 d4 d :: real. abs(fx - x) \<le> n1 + n2 \<Longrightarrow>
        abs(fx - fz) \<le> n3 \<Longrightarrow> abs(x - z) \<le> n4 \<Longrightarrow>
        n1 < d4 \<Longrightarrow> n2 < 2 * d4 \<Longrightarrow> n3 < d4 \<Longrightarrow> n4 < d4 \<Longrightarrow>
        (8 * d4 = d) \<Longrightarrow> abs(fz - z) < d" by auto
      show "\<bar>(f z - z) \<bullet> i\<bar> < d / real n" unfolding inner_simps
      proof (rule *)
        show "\<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y -f x) + norm (y - x)"
          apply (rule lem1[rule_format])
          using as i apply auto
          done
        show "\<bar>f x \<bullet> i - f z \<bullet> i\<bar> \<le> norm (f x - f z)" "\<bar>x \<bullet> i - z \<bullet> i\<bar> \<le> norm (x - z)"
          unfolding inner_diff_left[symmetric] by(rule Basis_le_norm[OF i])+
        have tria:"norm (y - x) \<le> norm (y - z) + norm (x - z)"
          using dist_triangle[of y x z, unfolded dist_norm]
          unfolding norm_minus_commute by auto
        also have "\<dots> < e / 2 + e / 2"
          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
        thus "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 \<Rightarrow> 'a" where b: "bij_betw b {1..n} Basis"
    by atomize_elim (auto simp: n_def intro!: finite_same_card_bij)
  def b' \<equiv> "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: "\<And>i. i \<in> Basis \<Longrightarrow> b' i \<in> {Suc 0 .. n}"
    unfolding bij_betw_def by (auto simp: set_eq_iff)
  have bb'[simp]:"\<And>i. i \<in> Basis \<Longrightarrow> b (b' i) = i"
    unfolding b'_def using b by (auto simp: f_inv_into_f bij_betw_def)
  have b'b[simp]:"\<And>i. i \<in> {1..n} \<Longrightarrow> b' (b i) = i"
    unfolding b'_def using b by (auto simp: inv_into_f_eq bij_betw_def)
  have *: "\<And>x :: nat. x=0 \<or> x=1 \<longleftrightarrow> x\<le>1" by auto
  have b'': "\<And>j. j \<in> {Suc 0..n} \<Longrightarrow> b j \<in> Basis"
    using b unfolding bij_betw_def by auto
  have q1: "0 < p" "0 < n"  "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow>
    (\<forall>i\<in>{1..n}. (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0 \<or>
                (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 1)"
    unfolding * using `p>0` `n>0` using label(1)[OF b''] by auto
  have q2: "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. x i = 0 \<longrightarrow>
      (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0)"
    "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. x i = p \<longrightarrow>
      (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 1)"
    apply (rule, rule, rule, rule)
    defer
  proof (rule, rule, rule, rule)
    fix x i
    assume as: "\<forall>i\<in>{1..n}. x i \<le> p" "i \<in> {1..n}"
    {
      assume "x i = p \<or> x i = 0"
      have "(\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<in> {0::'a..\<Sum>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"
      thus "(label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 1"
        unfolding o_def using cube as `p>0`
        by (intro label(3)) (auto simp add: b'')
    }
    {
      assume "x i = 0"
      thus "(label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> 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 \<equiv> "(\<Sum>i\<in>Basis. (real (q (b' i)) / real p) *\<^sub>R i)::'a"
  have "\<exists>i\<in>Basis. d / real n \<le> abs((f z - z)\<bullet>i)"
  proof (rule ccontr)
    have "\<forall>i\<in>Basis. q (b' i) \<in> {0..p}"
      using q(1) b' by (auto intro: less_imp_le simp: bij_betw_def)
    hence "z\<in>{0..\<Sum>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)
    hence d_fz_z:"d \<le> norm (f z - z)" by (rule d)
    case goal1
    hence as: "\<forall>i\<in>Basis. \<bar>f z \<bullet> i - z \<bullet> i\<bar> < d / real n"
      using `n > 0` by (auto simp add: not_le inner_simps)
    have "norm (f z - z) \<le> (\<Sum>i\<in>Basis. \<bar>f z \<bullet> i - z \<bullet> i\<bar>)"
      unfolding inner_diff_left[symmetric] by(rule norm_le_l1)
    also have "\<dots> < (\<Sum>(i::'a) \<in> Basis. d / real n)"
      apply (rule setsum_strict_mono)
      using as apply auto
      done
    also have "\<dots> = 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 \<in> {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: "\<And>i. i \<in> Basis \<Longrightarrow>  b' i \<in> {1..n}"
    using b' unfolding bij_betw_def by auto
  def r' \<equiv> "(\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i)::'a"
  have "\<And>i. i \<in> Basis \<Longrightarrow> r (b' i) \<le> 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
  hence "r' \<in> {0..\<Sum>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' \<equiv> "(\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i)::'a"
  have "\<And>i. i\<in>Basis \<Longrightarrow> s (b' i) \<le> 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
  hence "s' \<in> {0..\<Sum>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 \<in> {0..\<Sum>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 *: "\<And>x. 1 + real x = real (Suc x)" by auto
  { have "(\<Sum>i\<in>Basis. \<bar>real (r (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
      apply (rule setsum_mono)
      using rs(1)[OF b'_im]
      apply (auto simp add:* field_simps)
      done
    also have "\<dots> < e * real p" using p `e>0` `p>0`
      by (auto simp add: field_simps n_def real_of_nat_def)
    finally have "(\<Sum>i\<in>Basis. \<bar>real (r (b' i)) - real (q (b' i))\<bar>) < e * real p" .
  }
  moreover
  { have "(\<Sum>i\<in>Basis. \<bar>real (s (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
      apply (rule setsum_mono)
      using rs(2)[OF b'_im]
      apply (auto simp add:* field_simps)
      done
    also have "\<dots> < e * real p" using p `e > 0` `p > 0`
      by (auto simp add: field_simps n_def real_of_nat_def)
    finally have "(\<Sum>i\<in>Basis. \<bar>real (s (b' i)) - real (q (b' i))\<bar>) < e * real p" .
  }
  ultimately
  have "norm (r' - z) < e" "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
  hence "\<bar>(f z - z) \<bullet> i\<bar> < d / real n"
    using rs(3) i unfolding r'_def[symmetric] s'_def[symmetric] o_def bb'
    by (intro e(2)[OF `r'\<in>{0..\<Sum>Basis}` `s'\<in>{0..\<Sum>Basis}` `z\<in>{0..\<Sum>Basis}`]) auto
  thus False using i by auto
qed


subsection {* Retractions. *}

definition "retraction s t r \<longleftrightarrow>
  t \<subseteq> s \<and> continuous_on s r \<and> (r ` s \<subseteq> t) \<and> (\<forall>x\<in>t. r x = x)"

definition retract_of (infixl "retract'_of" 12)
  where "(t retract_of s) \<longleftrightarrow> (\<exists>r. retraction s t r)"

lemma retraction_idempotent: "retraction s t r \<Longrightarrow> x \<in> s \<Longrightarrow>  r(r x) = r x"
  unfolding retraction_def by auto

subsection {*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" "i ` t \<subseteq> s"
    "continuous_on s r" "r ` s \<subseteq> t"
    "\<forall>y\<in>t. r (i y) = y"
    "\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)" "continuous_on t g" "g ` t \<subseteq> t"
  obtains y where "y\<in>t" "g y = y"
proof -
  have "\<exists>x\<in>s. (i \<circ> g \<circ> r) x = x"
    apply (rule assms(6)[rule_format], 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
  hence *: "g (r x) \<in> t" using assms(4,8) by auto
  have "r ((i \<circ> g \<circ> r) x) = r x" using x by auto
  thus ?thesis
    apply (rule_tac that[of "r x"])
    using x unfolding o_def
    unfolding assms(5)[rule_format,OF *] using assms(4)
    apply auto
    done
qed

lemma homeomorphic_fixpoint_property:
  fixes s :: "('a::euclidean_space) set"
    and t :: "('b::euclidean_space) set"
  assumes "s homeomorphic t"
  shows "(\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)) \<longleftrightarrow>
    (\<forall>g. continuous_on t g \<and> g ` t \<subseteq> t \<longrightarrow> (\<exists>y\<in>t. g y = y))"
proof -
  guess r using assms[unfolded homeomorphic_def homeomorphism_def] ..
  then guess i ..
  thus ?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
    done
qed

lemma retract_fixpoint_property:
  fixes f :: "'a::euclidean_space => 'b::euclidean_space" and s::"'a set"
  assumes "t retract_of s"
    "\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)"
    "continuous_on t g" "g ` t \<subseteq> t"
  obtains y where "y \<in> t" "g y = y"
proof -
  guess h using assms(1) unfolding retract_of_def ..
  thus ?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
    done
qed


subsection {*So the Brouwer theorem for any set with nonempty interior. *}

lemma brouwer_weak:
  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'a::ordered_euclidean_space"
  assumes "compact s" "convex s" "interior s \<noteq> {}" "continuous_on s f" "f ` s \<subseteq> s"
  obtains x where "x \<in> s" "f x = x"
proof -
  have *: "interior {0::'a..\<Sum>Basis} \<noteq> {}"
    unfolding interior_closed_interval interval_eq_empty by auto
  have *: "{0::'a..\<Sum>Basis} homeomorphic s"
    using homeomorphic_convex_compact[OF convex_interval(1) compact_interval * assms(2,1,3)] .
  have "\<forall>f. continuous_on {0::'a..\<Sum>Basis} f \<and> f ` {0::'a..\<Sum>Basis} \<subseteq> {0::'a..\<Sum>Basis} \<longrightarrow>
    (\<exists>x\<in>{0::'a..\<Sum>Basis}. f x = x)"
    using brouwer_cube by auto
  thus ?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
    done
qed


subsection {* And in particular for a closed ball. *}

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

text {*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 \<Rightarrow> 'a"
  assumes "compact s" "convex s" "s \<noteq> {}" "continuous_on s f" "f ` s \<subseteq> s"
  obtains x where "x \<in> s" "f x = x"
proof -
  have "\<exists>e>0. s \<subseteq> cball 0 e"
    using compact_imp_bounded[OF assms(1)] unfolding bounded_pos
    apply (erule_tac exE, rule_tac x=b in exI)
    apply (auto simp add: dist_norm)
    done
  then guess e by (elim exE conjE)
  note e = this
  have "\<exists>x\<in> cball 0 e. (f \<circ> closest_point s) x = x"
    apply (rule_tac brouwer_ball[OF e(1), of 0 "f \<circ> 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 * by auto
qed

text {*So we get the no-retraction theorem. *}

lemma no_retraction_cball:
  assumes "0 < e"
  fixes type :: "'a::ordered_euclidean_space"
  shows "\<not> (frontier(cball a e) retract_of (cball (a::'a) e))"
proof
  case goal1
  have *:"\<And>xa. a - (2 *\<^sub>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 "\<lambda>x. scaleR 2 a - x"])
    apply (rule,rule,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,rule,erule bexE)
    unfolding dist_norm
    apply (simp add: * norm_minus_commute)
    done
  note x = this
  hence "scaleR 2 a = scaleR 1 x + scaleR 1 x"
    by (auto simp add: algebra_simps)
  hence "a = x" unfolding scaleR_left_distrib[symmetric] by auto
  thus False using x assms by auto
qed


subsection {*Bijections between intervals. *}

definition interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::ordered_euclidean_space"
  where "interval_bij =
    (\<lambda>(a, b) (u, v) x. (\<Sum>i\<in>Basis. (u\<bullet>i + (x\<bullet>i - a\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (v\<bullet>i - u\<bullet>i)) *\<^sub>R i))"

lemma interval_bij_affine:
  "interval_bij (a,b) (u,v) = (\<lambda>x. (\<Sum>i\<in>Basis. ((v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (x\<bullet>i)) *\<^sub>R i) +
    (\<Sum>i\<in>Basis. (u\<bullet>i - (v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (a\<bullet>i)) *\<^sub>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:
  "continuous (at x) (interval_bij (a,b::'a::ordered_euclidean_space) (u,v::'a))"
  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)
  done

lemma in_interval_interval_bij:
  fixes a b u v x :: "'a::ordered_euclidean_space"
  assumes "x \<in> {a..b}" "{u..v} \<noteq> {}"
  shows "interval_bij (a,b) (u,v) x \<in> {u..v}"
  apply (simp only: interval_bij_def split_conv mem_interval inner_setsum_left_Basis cong: ball_cong)
  apply safe
proof -
  fix i :: 'a
  assume i: "i \<in> Basis"
  have "{a..b} \<noteq> {}" using assms by auto
  with i have *: "a\<bullet>i \<le> b\<bullet>i" "u\<bullet>i \<le> v\<bullet>i"
    using assms(2) by (auto simp add: interval_eq_empty not_less)
  have x: "a\<bullet>i\<le>x\<bullet>i" "x\<bullet>i\<le>b\<bullet>i"
    using assms(1)[unfolded mem_interval] using i by auto
  have "0 \<le> (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
    using * x by (auto intro!: mult_nonneg_nonneg divide_nonneg_nonneg)
  thus "u \<bullet> i \<le> u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
    using * by auto
  have "((x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (v \<bullet> i - u \<bullet> i) \<le> 1 * (v \<bullet> i - u \<bullet> i)"
    apply (rule mult_right_mono)
    unfolding divide_le_eq_1
    using * x
    apply auto
    done
  thus "u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i) \<le> v \<bullet> i"
    using * by auto
qed

lemma interval_bij_bij:
  "\<forall>(i::'a::ordered_euclidean_space)\<in>Basis. a\<bullet>i < b\<bullet>i \<and> u\<bullet>i < v\<bullet>i \<Longrightarrow>
    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