src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
author huffman
Wed Sep 07 09:02:58 2011 -0700 (2011-09-07)
changeset 44821 a92f65e174cf
parent 44457 d366fa5551ef
child 44890 22f665a2e91c
permissions -rw-r--r--
avoid using legacy theorem names
     1 
     2 (* ========================================================================= *)
     3 (* Results connected with topological dimension.                             *)
     4 (*                                                                           *)
     5 (* At the moment this is just Brouwer's fixpoint theorem. The proof is from  *)
     6 (* Kuhn: "some combinatorial lemmas in topology", IBM J. v4. (1960) p. 518   *)
     7 (* See "http://www.research.ibm.com/journal/rd/045/ibmrd0405K.pdf".          *)
     8 (*                                                                           *)
     9 (* The script below is quite messy, but at least we avoid formalizing any    *)
    10 (* topological machinery; we don't even use barycentric subdivision; this is *)
    11 (* the big advantage of Kuhn's proof over the usual Sperner's lemma one.     *)
    12 (*                                                                           *)
    13 (*              (c) Copyright, John Harrison 1998-2008                       *)
    14 (* ========================================================================= *)
    15 
    16 (* Author:                     John Harrison
    17    Translation from HOL light: Robert Himmelmann, TU Muenchen *)
    18 
    19 header {* Results connected with topological dimension. *}
    20 
    21 theory Brouwer_Fixpoint
    22   imports Convex_Euclidean_Space
    23 begin
    24 
    25 lemma brouwer_compactness_lemma:
    26   assumes "compact s" "continuous_on s f" "\<not> (\<exists>x\<in>s. (f x = (0::_::euclidean_space)))"
    27   obtains d where "0 < d" "\<forall>x\<in>s. d \<le> norm(f x)" proof(cases "s={}") case False
    28   have "continuous_on s (norm \<circ> f)" by(rule continuous_on_intros continuous_on_norm assms(2))+
    29   then obtain x where x:"x\<in>s" "\<forall>y\<in>s. (norm \<circ> f) x \<le> (norm \<circ> f) y"
    30     using continuous_attains_inf[OF assms(1), of "norm \<circ> f"] and False unfolding o_def by auto
    31   have "(norm \<circ> f) x > 0" using assms(3) and x(1) by auto
    32   thus ?thesis apply(rule that) using x(2) unfolding o_def by auto qed(rule that[of 1], auto)
    33 
    34 lemma kuhn_labelling_lemma: fixes type::"'a::euclidean_space"
    35   assumes "(\<forall>x::'a. P x \<longrightarrow> P (f x))"  "\<forall>x. P x \<longrightarrow> (\<forall>i<DIM('a). Q i \<longrightarrow> 0 \<le> x$$i \<and> x$$i \<le> 1)"
    36   shows "\<exists>l. (\<forall>x.\<forall> i<DIM('a). l x i \<le> (1::nat)) \<and>
    37              (\<forall>x.\<forall> i<DIM('a). P x \<and> Q i \<and> (x$$i = 0) \<longrightarrow> (l x i = 0)) \<and>
    38              (\<forall>x.\<forall> i<DIM('a). P x \<and> Q i \<and> (x$$i = 1) \<longrightarrow> (l x i = 1)) \<and>
    39              (\<forall>x.\<forall> i<DIM('a). P x \<and> Q i \<and> (l x i = 0) \<longrightarrow> x$$i \<le> f(x)$$i) \<and>
    40              (\<forall>x.\<forall> i<DIM('a). P x \<and> Q i \<and> (l x i = 1) \<longrightarrow> f(x)$$i \<le> x$$i)" proof-
    41   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
    42   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
    43   show ?thesis unfolding and_forall_thm apply(subst choice_iff[THEN sym])+ proof(rule,rule) case goal1
    44     let ?R = "\<lambda>y. (P x \<and> Q xa \<and> x $$ xa = 0 \<longrightarrow> y = (0::nat)) \<and>
    45         (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)"
    46     { assume "P x" "Q xa" "xa<DIM('a)" hence "0 \<le> f x $$ xa \<and> f x $$ xa \<le> 1" using assms(2)[rule_format,of "f x" xa]
    47         apply(drule_tac assms(1)[rule_format]) by auto }
    48     hence "xa<DIM('a) \<Longrightarrow> ?R 0 \<or> ?R 1" by auto thus ?case by auto qed qed 
    49  
    50 subsection {* The key "counting" observation, somewhat abstracted. *}
    51 
    52 lemma setsum_Un_disjoint':assumes "finite A" "finite B" "A \<inter> B = {}" "A \<union> B = C"
    53   shows "setsum g C = setsum g A + setsum g B"
    54   using setsum_Un_disjoint[OF assms(1-3)] and assms(4) by auto
    55 
    56 lemma kuhn_counting_lemma: assumes "finite faces" "finite simplices"
    57   "\<forall>f\<in>faces. bnd f  \<longrightarrow> (card {s \<in> simplices. face f s} = 1)"
    58   "\<forall>f\<in>faces. \<not> bnd f \<longrightarrow> (card {s \<in> simplices. face f s} = 2)"
    59   "\<forall>s\<in>simplices. compo s  \<longrightarrow> (card {f \<in> faces. face f s \<and> compo' f} = 1)"
    60   "\<forall>s\<in>simplices. \<not> compo s \<longrightarrow> (card {f \<in> faces. face f s \<and> compo' f} = 0) \<or>
    61                              (card {f \<in> faces. face f s \<and> compo' f} = 2)"
    62     "odd(card {f \<in> faces. compo' f \<and> bnd f})"
    63   shows "odd(card {s \<in> simplices. compo s})" proof-
    64   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}"
    65     "\<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
    66   hence lem1:"setsum (\<lambda>s. (card {f \<in> faces. face f s \<and> compo' f})) simplices =
    67     setsum (\<lambda>s. card {f \<in> {f \<in> faces. compo' f \<and> bnd f}. face f s}) simplices +
    68     setsum (\<lambda>s. card {f \<in> {f \<in> faces. compo' f \<and> \<not> (bnd f)}. face f s}) simplices"
    69     unfolding setsum_addf[THEN sym] apply- apply(rule setsum_cong2)
    70     using assms(1) by(auto simp add: card_Un_Int, auto simp add:conj_commute)
    71   have lem2:"setsum (\<lambda>j. card {f \<in> {f \<in> faces. compo' f \<and> bnd f}. face f j}) simplices = 
    72               1 * card {f \<in> faces. compo' f \<and> bnd f}"
    73        "setsum (\<lambda>j. card {f \<in> {f \<in> faces. compo' f \<and> \<not> bnd f}. face f j}) simplices = 
    74               2 * card {f \<in> faces. compo' f \<and> \<not> bnd f}"
    75     apply(rule_tac[!] setsum_multicount) using assms by auto
    76   have lem3:"setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) simplices =
    77     setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices.   compo s}+
    78     setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices. \<not> compo s}"
    79     apply(rule setsum_Un_disjoint') using assms(2) by auto
    80   have lem4:"setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices. compo s}
    81     = setsum (\<lambda>s. 1) {s \<in> simplices. compo s}"
    82     apply(rule setsum_cong2) using assms(5) by auto
    83   have lem5: "setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices. \<not> compo s} =
    84     setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f})
    85            {s \<in> simplices. (\<not> compo s) \<and> (card {f \<in> faces. face f s \<and> compo' f} = 0)} +
    86     setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f})
    87            {s \<in> simplices. (\<not> compo s) \<and> (card {f \<in> faces. face f s \<and> compo' f} = 2)}"
    88     apply(rule setsum_Un_disjoint') using assms(2,6) by auto
    89   have *:"int (\<Sum>s\<in>{s \<in> simplices. compo s}. card {f \<in> faces. face f s \<and> compo' f}) =
    90     int (card {f \<in> faces. compo' f \<and> bnd f} + 2 * card {f \<in> faces. compo' f \<and> \<not> bnd f}) - 
    91     int (card {s \<in> simplices. \<not> compo s \<and> card {f \<in> faces. face f s \<and> compo' f} = 2} * 2)"
    92     using lem1[unfolded lem3 lem2 lem5] by auto
    93   have even_minus_odd:"\<And>x y. even x \<Longrightarrow> odd (y::int) \<Longrightarrow> odd (x - y)" using assms by auto
    94   have odd_minus_even:"\<And>x y. odd x \<Longrightarrow> even (y::int) \<Longrightarrow> odd (x - y)" using assms by auto
    95   show ?thesis unfolding even_nat_def unfolding card_eq_setsum and lem4[THEN sym] and *[unfolded card_eq_setsum]
    96     unfolding card_eq_setsum[THEN sym] apply (rule odd_minus_even) unfolding of_nat_add apply(rule odd_plus_even)
    97     apply(rule assms(7)[unfolded even_nat_def]) unfolding int_mult by auto qed
    98 
    99 subsection {* The odd/even result for faces of complete vertices, generalized. *}
   100 
   101 lemma card_1_exists: "card s = 1 \<longleftrightarrow> (\<exists>!x. x \<in> s)" unfolding One_nat_def
   102   apply rule apply(drule card_eq_SucD) defer apply(erule ex1E) proof-
   103   fix x assume as:"x \<in> s" "\<forall>y. y \<in> s \<longrightarrow> y = x"
   104   have *:"s = insert x {}" apply- apply(rule set_eqI,rule) unfolding singleton_iff
   105     apply(rule as(2)[rule_format]) using as(1) by auto
   106   show "card s = Suc 0" unfolding * using card_insert by auto qed auto
   107 
   108 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
   109   assume "card s = 2" then obtain x y where obt:"s = {x, y}" "x\<noteq>y" unfolding numeral_2_eq_2 apply - apply(erule exE conjE|drule card_eq_SucD)+ by auto
   110   show "\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y)" using obt by auto next
   111   assume "\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y)" then guess x .. from this(2) guess y  ..
   112   with `x\<in>s` have *:"s = {x, y}" "x\<noteq>y" by auto
   113   from this(2) show "card s = 2" unfolding * by auto qed
   114 
   115 lemma image_lemma_0: assumes "card {a\<in>s. f ` (s - {a}) = t - {b}} = n"
   116   shows "card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> (f ` s' = t - {b})} = n" proof-
   117   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
   118   show ?thesis unfolding * unfolding assms[THEN sym] apply(rule card_image) unfolding inj_on_def 
   119     apply(rule,rule,rule) unfolding mem_Collect_eq by auto qed
   120 
   121 lemma image_lemma_1: assumes "finite s" "finite t" "card s = card t" "f ` s = t" "b \<in> t"
   122   shows "card {s'. \<exists>a\<in>s. s' = s - {a} \<and>  f ` s' = t - {b}} = 1" proof-
   123   obtain a where a:"b = f a" "a\<in>s" using assms(4-5) by auto
   124   have inj:"inj_on f s" apply(rule eq_card_imp_inj_on) using assms(1-4) by auto
   125   have *:"{a \<in> s. f ` (s - {a}) = t - {b}} = {a}" apply(rule set_eqI) unfolding singleton_iff
   126     apply(rule,rule inj[unfolded inj_on_def,rule_format]) unfolding a using a(2) and assms and inj[unfolded inj_on_def] by auto
   127   show ?thesis apply(rule image_lemma_0) unfolding *  by auto qed
   128 
   129 lemma image_lemma_2: assumes "finite s" "finite t" "card s = card t" "f ` s \<subseteq> t" "f ` s \<noteq> t" "b \<in> t"
   130   shows "(card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> f ` s' = t - {b}} = 0) \<or>
   131          (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}} = {}")
   132   case True thus ?thesis apply-apply(rule disjI1, rule image_lemma_0) using assms(1) by auto
   133 next let ?M = "{a\<in>s. f ` (s - {a}) = t - {b}}"
   134   case False then obtain a where "a\<in>?M" by auto hence a:"a\<in>s" "f ` (s - {a}) = t - {b}" by auto
   135   have "f a \<in> t - {b}" using a and assms by auto
   136   hence "\<exists>c \<in> s - {a}. f a = f c" unfolding image_iff[symmetric] and a by auto
   137   then obtain c where c:"c \<in> s" "a \<noteq> c" "f a = f c" by auto
   138   hence *:"f ` (s - {c}) = f ` (s - {a})" apply-apply(rule set_eqI,rule) proof-
   139     fix x assume "x \<in> f ` (s - {a})" then obtain y where y:"f y = x" "y\<in>s- {a}" by auto
   140     thus "x \<in> f ` (s - {c})" unfolding image_iff apply(rule_tac x="if y = c then a else y" in bexI) using c a by auto qed auto
   141   have "c\<in>?M" unfolding mem_Collect_eq and * using a and c(1) by auto
   142   show ?thesis apply(rule disjI2, rule image_lemma_0) unfolding card_2_exists
   143     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)
   144     fix z assume as:"z \<in> s" "f ` (s - {z}) = t - {b}"
   145     have inj:"inj_on f (s - {z})" apply(rule eq_card_imp_inj_on) unfolding as using as(1) and assms by auto
   146     show "z = a \<or> z = c" proof(rule ccontr)
   147       assume "\<not> (z = a \<or> z = c)" thus False using inj[unfolded inj_on_def,THEN bspec[where x=a],THEN bspec[where x=c]]
   148         using `a\<in>s` `c\<in>s` `f a = f c` `a\<noteq>c` by auto qed qed qed
   149 
   150 subsection {* Combine this with the basic counting lemma. *}
   151 
   152 lemma kuhn_complete_lemma:
   153   assumes "finite simplices"
   154   "\<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}"
   155   "\<forall>f\<in> {f. \<exists>s\<in>simplices. face f s}. bnd f  \<longrightarrow> (card {s\<in>simplices. face f s} = 1)"
   156   "\<forall>f\<in> {f. \<exists>s\<in>simplices. face f s}. \<not>bnd f \<longrightarrow> (card {s\<in>simplices. face f s} = 2)"
   157   "odd(card {f\<in>{f. \<exists>s\<in>simplices. face f s}. rl ` f = {0..n} \<and> bnd f})"
   158   shows "odd (card {s\<in>simplices. (rl ` s = {0..n+1})})" 
   159   apply(rule kuhn_counting_lemma) defer apply(rule assms)+ prefer 3 apply(rule assms) proof(rule_tac[1-2] ballI impI)+ 
   160   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
   161   have **: "\<forall>s\<in>simplices. card s = n + 2 \<and> finite s" using assms(3) by (auto intro: card_ge_0_finite)
   162   show "finite {f. \<exists>s\<in>simplices. face f s}" unfolding assms(2)[rule_format] and *
   163     apply(rule finite_UN_I[OF assms(1)]) using ** by auto
   164   have *:"\<And> P f s. s\<in>simplices \<Longrightarrow> (f \<in> {f. \<exists>s\<in>simplices. \<exists>a\<in>s. f = s - {a}}) \<and>
   165     (\<exists>a\<in>s. (f = s - {a})) \<and> P f \<longleftrightarrow> (\<exists>a\<in>s. (f = s - {a}) \<and> P f)" by auto
   166   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}}"
   167     have "{0..n + 1} - {n + 1} = {0..n}" by auto
   168     hence S:"?S = {s'. \<exists>a\<in>s. s' = s - {a} \<and> rl ` s' = {0..n + 1} - {n + 1}}" apply- apply(rule set_eqI)
   169       unfolding assms(2)[rule_format] mem_Collect_eq and *[OF s, unfolded mem_Collect_eq, where P="\<lambda>x. rl ` x = {0..n}"] by auto
   170     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
   171       apply(rule_tac[!] image_lemma_1 image_lemma_2) using ** assms(4) and s by auto qed
   172 
   173 subsection {*We use the following notion of ordering rather than pointwise indexing. *}
   174 
   175 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)))"
   176 
   177 lemma kle_refl[intro]: "kle n x x" unfolding kle_def by auto
   178 
   179 lemma kle_antisym: "kle n x y \<and> kle n y x \<longleftrightarrow> (x = y)"
   180   unfolding kle_def apply rule apply(rule ext) by auto
   181 
   182 lemma pointwise_minimal_pointwise_maximal: fixes s::"(nat\<Rightarrow>nat) set"
   183   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)"
   184   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"
   185   using assms unfolding atomize_conj apply- proof(induct s rule:finite_induct)
   186   fix x and F::"(nat\<Rightarrow>nat) set" assume as:"finite F" "x \<notin> F" 
   187     "\<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>
   188         \<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> {}"
   189     "\<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)"
   190   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={}")
   191     case True thus ?thesis apply-apply(rule,rule_tac[!] x=x in bexI) by auto next
   192     case False obtain a b where a:"a\<in>insert x F" "\<forall>x\<in>F. \<forall>j. a j \<le> x j" and
   193       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
   194     have "\<exists>a\<in>insert x F. \<forall>x\<in>insert x F. \<forall>j. a j \<le> x j"
   195       using as(5)[rule_format,OF a(1) insertI1] apply- proof(erule disjE)
   196       assume "\<forall>j. a j \<le> x j" thus ?thesis apply(rule_tac x=a in bexI) using a by auto next
   197       assume "\<forall>j. x j \<le> a j" thus ?thesis apply(rule_tac x=x in bexI) apply(rule,rule) using a apply -
   198         apply(erule_tac x=xa in ballE) apply(erule_tac x=j in allE)+ by auto qed moreover
   199     have "\<exists>b\<in>insert x F. \<forall>x\<in>insert x F. \<forall>j. x j \<le> b j"
   200       using as(5)[rule_format,OF b(1) insertI1] apply- proof(erule disjE)
   201       assume "\<forall>j. x j \<le> b j" thus ?thesis apply(rule_tac x=b in bexI) using b by auto next
   202       assume "\<forall>j. b j \<le> x j" thus ?thesis apply(rule_tac x=x in bexI) apply(rule,rule) using b apply -
   203         apply(erule_tac x=xa in ballE) apply(erule_tac x=j in allE)+ by auto qed
   204     ultimately show  ?thesis by auto qed qed(auto)
   205 
   206 lemma kle_imp_pointwise: "kle n x y \<Longrightarrow> (\<forall>j. x j \<le> y j)" unfolding kle_def by auto
   207 
   208 lemma pointwise_antisym: fixes x::"nat \<Rightarrow> nat"
   209   shows "(\<forall>j. x j \<le> y j) \<and> (\<forall>j. y j \<le> x j) \<longleftrightarrow> (x = y)"
   210   apply(rule, rule ext,erule conjE) apply(erule_tac x=xa in allE)+ by auto
   211 
   212 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"
   213   using assms apply- apply(erule disjE) apply assumption proof- case goal1
   214   hence "x=z" apply- apply(rule ext) apply(drule kle_imp_pointwise)+ 
   215     apply(erule_tac x=xa in allE)+ by auto thus ?case by auto qed
   216 
   217 lemma kle_strict: assumes "kle n x y" "x \<noteq> y"
   218   shows "\<forall>j. x j \<le> y j"  "\<exists>k. 1 \<le> k \<and> k \<le> n \<and> x(k) < y(k)"
   219   apply(rule kle_imp_pointwise[OF assms(1)]) proof-
   220   guess k using assms(1)[unfolded kle_def] .. note k = this
   221   show "\<exists>k. 1 \<le> k \<and> k \<le> n \<and> x(k) < y(k)" proof(cases "k={}")
   222     case True hence "x=y" apply-apply(rule ext) using k by auto
   223     thus ?thesis using assms(2) by auto next
   224     case False hence "(SOME k'. k' \<in> k) \<in> k" apply-apply(rule someI_ex) by auto
   225     thus ?thesis apply(rule_tac x="SOME k'. k' \<in> k" in exI) using k by auto qed qed
   226 
   227 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"
   228   shows "\<exists>a\<in>s. \<forall>x\<in>s. kle n a x" proof-
   229   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)])
   230     apply(rule,rule) apply(drule_tac assms(3)[rule_format],assumption) using kle_imp_pointwise by auto
   231   then guess a .. note a=this show ?thesis apply(rule_tac x=a in bexI) proof fix x assume "x\<in>s"
   232     show "kle n a x" using assms(3)[rule_format,OF a(1) `x\<in>s`] apply- proof(erule disjE)
   233       assume "kle n x a" hence "x = a" apply- unfolding pointwise_antisym[THEN sym]
   234         apply(drule kle_imp_pointwise) using a(2)[rule_format,OF `x\<in>s`] by auto
   235       thus ?thesis using kle_refl by auto  qed qed(insert a, auto) qed
   236 
   237 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"
   238   shows "\<exists>a\<in>s. \<forall>x\<in>s. kle n x a" proof-
   239   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)])
   240     apply(rule,rule) apply(drule_tac assms(3)[rule_format],assumption) using kle_imp_pointwise by auto
   241   then guess a .. note a=this show ?thesis apply(rule_tac x=a in bexI) proof fix x assume "x\<in>s"
   242     show "kle n x a" using assms(3)[rule_format,OF a(1) `x\<in>s`] apply- proof(erule disjE)
   243       assume "kle n a x" hence "x = a" apply- unfolding pointwise_antisym[THEN sym]
   244         apply(drule kle_imp_pointwise) using a(2)[rule_format,OF `x\<in>s`] by auto
   245       thus ?thesis using kle_refl by auto  qed qed(insert a, auto) qed
   246 
   247 lemma kle_strict_set: assumes "kle n x y" "x \<noteq> y"
   248   shows "1 \<le> card {k\<in>{1..n}. x k < y k}" proof-
   249   guess i using kle_strict(2)[OF assms] ..
   250   hence "card {i} \<le> card {k\<in>{1..n}. x k < y k}" apply- apply(rule card_mono) by auto
   251   thus ?thesis by auto qed
   252 
   253 lemma kle_range_combine:
   254   assumes "kle n x y" "kle n y z" "kle n x z \<or> kle n z x"
   255   "m1 \<le> card {k\<in>{1..n}. x k < y k}"
   256   "m2 \<le> card {k\<in>{1..n}. y k < z k}"
   257   shows "kle n x z \<and> m1 + m2 \<le> card {k\<in>{1..n}. x k < z k}"
   258   apply(rule,rule kle_trans[OF assms(1-3)]) proof-
   259   have "\<And>j. x j < y j \<Longrightarrow> x j < z j" apply(rule less_le_trans) using kle_imp_pointwise[OF assms(2)] by auto moreover
   260   have "\<And>j. y j < z j \<Longrightarrow> x j < z j" apply(rule le_less_trans) using kle_imp_pointwise[OF assms(1)] by auto ultimately
   261   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
   262   have **:"{k \<in> {1..n}. x k < y k} \<inter> {k \<in> {1..n}. y k < z k} = {}" unfolding disjoint_iff_not_equal
   263     apply(rule,rule,unfold mem_Collect_eq,rule ccontr) apply(erule conjE)+ proof-
   264     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"
   265     guess kx using assms(1)[unfolded kle_def] .. note kx=this
   266     have "x i < y i" using as by auto hence "i \<in> kx" using as(1) kx apply(rule_tac ccontr) by auto 
   267     hence "x i + 1 = y i" using kx by auto moreover
   268     guess ky using assms(2)[unfolded kle_def] .. note ky=this
   269     have "y i < z i" using as by auto hence "i \<in> ky" using as(1) ky apply(rule_tac ccontr) by auto 
   270     hence "y i + 1 = z i" using ky by auto ultimately
   271     have "z i = x i + 2" by auto
   272     thus False using assms(3) unfolding kle_def by(auto simp add: split_if_eq1) qed
   273   have fin:"\<And>P. finite {x\<in>{1..n::nat}. P x}" by auto
   274   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
   275   also have "\<dots> \<le>  card {k\<in>{1..n}. x k < z k}" unfolding card_Un_Int[OF fin fin] unfolding * ** by auto
   276   finally show " m1 + m2 \<le> card {k \<in> {1..n}. x k < z k}" by auto qed
   277 
   278 lemma kle_range_combine_l:
   279   assumes "kle n x y" "kle n y z" "kle n x z \<or> kle n z x" "m \<le> card {k\<in>{1..n}. y(k) < z(k)}"
   280   shows "kle n x z \<and> m \<le> card {k\<in>{1..n}. x(k) < z(k)}"
   281   using kle_range_combine[OF assms(1-3) _ assms(4), of 0] by auto
   282 
   283 lemma kle_range_combine_r:
   284   assumes "kle n x y" "kle n y z" "kle n x z \<or> kle n z x" "m \<le> card {k\<in>{1..n}. x k < y k}"
   285   shows "kle n x z \<and> m \<le> card {k\<in>{1..n}. x(k) < z(k)}"
   286   using kle_range_combine[OF assms(1-3) assms(4), of 0] by auto
   287 
   288 lemma kle_range_induct:
   289   assumes "card s = Suc m" "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"
   290   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-
   291 have "finite s" "s\<noteq>{}" using assms(1) by (auto intro: card_ge_0_finite)
   292 thus ?thesis using assms apply- proof(induct m arbitrary: s)
   293   case 0 thus ?case using kle_refl by auto next
   294   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
   295   show ?case proof(cases "s \<subseteq> {a}") case False
   296     hence "card (s - {a}) = Suc m" "s - {a} \<noteq> {}" using card_Diff_singleton[OF _ a(1)] Suc(4) `finite s` by auto
   297     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}" 
   298       using Suc(1)[of "s - {a}"] using Suc(5) `finite s` by auto
   299     have "1 \<le> card {k \<in> {1..n}. a k < x k}" "m \<le> card {k \<in> {1..n}. x k < b k}"
   300       apply(rule kle_strict_set) apply(rule a(2)[rule_format]) using a and xb by auto
   301     thus ?thesis apply(rule_tac x=a in bexI, rule_tac x=b in bexI) 
   302       using kle_range_combine[OF a(2)[rule_format] xb(3) Suc(5)[rule_format], of 1 "m"] using a(1) xb(1-2) by auto next
   303     case True hence "s = {a}" using Suc(3) by auto hence "card s = 1" by auto
   304     hence False using Suc(4) `finite s` by auto thus ?thesis by auto qed qed qed
   305 
   306 lemma kle_Suc: "kle n x y \<Longrightarrow> kle (n + 1) x y"
   307   unfolding kle_def apply(erule exE) apply(rule_tac x=k in exI) by auto
   308 
   309 lemma kle_trans_1: assumes "kle n x y" shows "x j \<le> y j" "y j \<le> x j + 1"
   310   using assms[unfolded kle_def] by auto 
   311 
   312 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-
   313   guess kk1 using assms(1)[unfolded kle_def] .. note kk1=this
   314   guess kk2 using assms(2)[unfolded kle_def] .. note kk2=this
   315   show ?thesis unfolding kle_def apply(rule_tac x="kk1 \<union> kk2" in exI) apply(rule) defer proof
   316     fix i show "c i = a i + (if i \<in> kk1 \<union> kk2 then 1 else 0)" proof(cases "i\<in>kk1 \<union> kk2")
   317       case True hence "c i \<ge> a i + (if i \<in> kk1 \<union> kk2 then 1 else 0)"
   318         unfolding kk1[THEN conjunct2,rule_format,of i] kk2[THEN conjunct2,rule_format,of i] by auto
   319       moreover have "c i \<le> a i + (if i \<in> kk1 \<union> kk2 then 1 else 0)" using True assms(3) by auto  
   320       ultimately show ?thesis by auto next
   321       case False thus ?thesis using kk1 kk2 by auto qed qed(insert kk1 kk2, auto) qed
   322 
   323 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"
   324   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
   325   fix j show "x j \<le> b j + 1" apply(rule *)using kle_trans_1[OF assms(1),of j] kle_trans_1[OF assms(3), of j] by auto qed
   326 
   327 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"
   328   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
   329   fix j show "b j \<le> x j + 1" apply(rule *) using kle_trans_1[OF assms(2),of j] kle_trans_1[OF assms(4), of j] by auto qed
   330 
   331 lemma kle_adjacent:
   332   assumes "\<forall>j. b j = (if j = k then a(j) + 1 else a j)" "kle n a x" "kle n x b"
   333   shows "(x = a) \<or> (x = b)" proof(cases "x k = a k")
   334   case True show ?thesis apply(rule disjI1,rule ext) proof- fix j
   335     have "x j \<le> a j" using kle_imp_pointwise[OF assms(3),THEN spec[where x=j]] 
   336       unfolding assms(1)[rule_format] apply-apply(cases "j=k") using True by auto
   337     thus "x j = a j" using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]] by auto qed next
   338   case False show ?thesis apply(rule disjI2,rule ext) proof- fix j
   339     have "x j \<ge> b j" using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]]
   340       unfolding assms(1)[rule_format] apply-apply(cases "j=k") using False by auto
   341     thus "x j = b j" using kle_imp_pointwise[OF assms(3),THEN spec[where x=j]] by auto qed qed
   342 
   343 subsection {* kuhn's notion of a simplex (a reformulation to avoid so much indexing). *}
   344 
   345 definition "ksimplex p n (s::(nat \<Rightarrow> nat) set) \<longleftrightarrow>
   346         (card s = n + 1 \<and>
   347         (\<forall>x\<in>s. \<forall>j. x(j) \<le> p) \<and>
   348         (\<forall>x\<in>s. \<forall>j. j\<notin>{1..n} \<longrightarrow> (x j = p)) \<and>
   349         (\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x))"
   350 
   351 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"
   352   unfolding ksimplex_def by auto
   353 
   354 lemma ksimplex_eq: "ksimplex p n (s::(nat \<Rightarrow> nat) set) \<longleftrightarrow>
   355         (card s = n + 1 \<and> finite s \<and>
   356         (\<forall>x\<in>s. \<forall>j. x(j) \<le> p) \<and>
   357         (\<forall>x\<in>s. \<forall>j. j\<notin>{1..n} \<longrightarrow> (x j = p)) \<and>
   358         (\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x))"
   359   unfolding ksimplex_def by (auto intro: card_ge_0_finite)
   360 
   361 lemma ksimplex_extrema: assumes "ksimplex p n s" obtains a b where "a \<in> s" "b \<in> s"
   362   "\<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")
   363   case True obtain x where *:"s = {x}" using assms[unfolded ksimplex_eq True,THEN conjunct1]
   364     unfolding add_0_left card_1_exists by auto
   365   show ?thesis apply(rule that[of x x]) unfolding * True by auto next
   366   note assm = assms[unfolded ksimplex_eq]
   367   case False have "s\<noteq>{}" using assm by auto
   368   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
   369   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
   370   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}"
   371     using kle_range_induct[of s n n] using assm by auto
   372   have "kle n c b \<and> n \<le> card {k \<in> {1..n}. c k < b k}" apply(rule kle_range_combine_r[where y=d]) using c_d a b by auto
   373   hence "kle n a b \<and> n \<le> card {k\<in>{1..n}. a(k) < b(k)}" apply-apply(rule kle_range_combine_l[where y=c]) using a `c\<in>s` `b\<in>s` by auto
   374   moreover have "card {1..n} \<ge> card {k\<in>{1..n}. a(k) < b(k)}" apply(rule card_mono) by auto
   375   ultimately have *:"{k\<in>{1 .. n}. a k < b k} = {1..n}" apply- apply(rule card_subset_eq) by auto
   376   show ?thesis apply(rule that[OF a(1) b(1)]) defer apply(subst *[THEN sym]) unfolding mem_Collect_eq proof
   377     guess k using a(2)[rule_format,OF b(1),unfolded kle_def] .. note k=this
   378     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}")
   379       case True thus ?thesis unfolding k[THEN conjunct2,rule_format] by auto next
   380       case False have "a i = p" using assm and False `a\<in>s` by auto
   381       moreover   have "b i = p" using assm and False `b\<in>s` by auto
   382       ultimately show ?thesis by auto qed qed(insert a(2) b(2) assm,auto) qed
   383 
   384 lemma ksimplex_extrema_strong:
   385   assumes "ksimplex p n s" "n \<noteq> 0" obtains a b where "a \<in> s" "b \<in> s" "a \<noteq> b"
   386   "\<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-
   387   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))" 
   388     apply(rule ksimplex_extrema[OF assms(1)]) by auto 
   389   have "a \<noteq> b" apply(rule ccontr) unfolding not_not apply(drule cong[of _ _ 1 1]) using ab(4) assms(2) by auto
   390   thus ?thesis apply(rule_tac that[of a b]) using ab by auto qed
   391 
   392 lemma ksimplexD:
   393   assumes "ksimplex p n s"
   394   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"
   395   "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x" using assms unfolding ksimplex_eq by auto
   396 
   397 lemma ksimplex_successor:
   398   assumes "ksimplex p n s" "a \<in> s"
   399   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)))"
   400 proof(cases "\<forall>x\<in>s. kle n x a") case True thus ?thesis by auto next note assm = ksimplexD[OF assms(1)]
   401   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"
   402     using kle_minimal[of "{x\<in>s. \<not> kle n x a}" n] and assm by auto
   403   hence  **:"1 \<le> card {k\<in>{1..n}. a k < b k}" apply- apply(rule kle_strict_set) using assm(6) and `a\<in>s` by(auto simp add:kle_refl)
   404 
   405   let ?kle1 = "{x \<in> s. \<not> kle n x a}" have "card ?kle1 > 0" apply(rule ccontr) using assm(2) and False by auto
   406   hence sizekle1: "card ?kle1 = Suc (card ?kle1 - 1)" using assm(2) by auto
   407   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}"
   408     using kle_range_induct[OF sizekle1, of n] using assm by auto
   409 
   410   let ?kle2 = "{x \<in> s. kle n x a}"
   411   have "card ?kle2 > 0" apply(rule ccontr) using assm(6)[rule_format,of a a] and `a\<in>s` and assm(2) by auto
   412   hence sizekle2:"card ?kle2 = Suc (card ?kle2 - 1)" using assm(2) by auto
   413   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}"
   414     using kle_range_induct[OF sizekle2, of n] using assm by auto
   415 
   416   have "card {k\<in>{1..n}. a k < b k} = 1" proof(rule ccontr) case goal1
   417     hence as:"card {k\<in>{1..n}. a k < b k} \<ge> 2" using ** by auto
   418     have *:"finite ?kle2" "finite ?kle1" "?kle2 \<union> ?kle1 = s" "?kle2 \<inter> ?kle1 = {}" using assm(2) by auto
   419     have "(card ?kle2 - 1) + 2 + (card ?kle1 - 1) = card ?kle2 + card ?kle1" using sizekle1 sizekle2 by auto
   420     also have "\<dots> = n + 1" unfolding card_Un_Int[OF *(1-2)] *(3-) using assm(3) by auto
   421     finally have n:"(card ?kle2 - 1) + (2 + (card ?kle1 - 1)) = n + 1" by auto
   422     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}"
   423       apply(rule kle_range_combine_r[where y=f]) using e_f using `a\<in>s` assm(6) by auto
   424     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}"
   425       apply(rule kle_range_combine_l[where y=c]) using c_d using assm(6) and b by auto
   426     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-
   427       apply(rule kle_range_combine[where y=b]) using as and b assm(6) `a\<in>s` `d\<in>s` apply- by blast+
   428     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-
   429       apply(rule kle_range_combine[where y=a]) using assm(6)[rule_format,OF `e\<in>s` `d\<in>s`] apply - by blast+ 
   430     moreover have "card {k \<in> {1..n}. e k < d k} \<le> card {1..n}" apply(rule card_mono) by auto
   431     ultimately show False unfolding n by auto qed
   432   then guess k unfolding card_1_exists .. note k=this[unfolded mem_Collect_eq]
   433 
   434   show ?thesis apply(rule disjI2) apply(rule_tac x=b in bexI,rule_tac x=k in bexI) proof
   435     fix j::nat have "kle n a b" using b and assm(6)[rule_format, OF `a\<in>s` `b\<in>s`] by auto
   436     then guess kk unfolding kle_def .. note kk_raw=this note kk=this[THEN conjunct2,rule_format]
   437     have kkk:"k\<in>kk" apply(rule ccontr) using k(1) unfolding kk by auto 
   438     show "b j = (if j = k then a j + 1 else a j)" proof(cases "j\<in>kk")
   439       case True hence "j=k" apply-apply(rule k(2)[rule_format]) using kk_raw kkk by auto
   440       thus ?thesis unfolding kk using kkk by auto next
   441       case False hence "j\<noteq>k" using k(2)[rule_format, of j k] using kk_raw kkk by auto
   442       thus ?thesis unfolding kk using kkk using False by auto qed qed(insert k(1) `b\<in>s`, auto) qed
   443 
   444 lemma ksimplex_predecessor:
   445   assumes "ksimplex p n s" "a \<in> s"
   446   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)))"
   447 proof(cases "\<forall>x\<in>s. kle n a x") case True thus ?thesis by auto next note assm = ksimplexD[OF assms(1)]
   448   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" 
   449     using kle_maximal[of "{x\<in>s. \<not> kle n a x}" n] and assm by auto
   450   hence  **:"1 \<le> card {k\<in>{1..n}. a k > b k}" apply- apply(rule kle_strict_set) using assm(6) and `a\<in>s` by(auto simp add:kle_refl)
   451 
   452   let ?kle1 = "{x \<in> s. \<not> kle n a x}" have "card ?kle1 > 0" apply(rule ccontr) using assm(2) and False by auto
   453   hence sizekle1:"card ?kle1 = Suc (card ?kle1 - 1)" using assm(2) by auto
   454   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}"
   455     using kle_range_induct[OF sizekle1, of n] using assm by auto
   456 
   457   let ?kle2 = "{x \<in> s. kle n a x}"
   458   have "card ?kle2 > 0" apply(rule ccontr) using assm(6)[rule_format,of a a] and `a\<in>s` and assm(2) by auto
   459   hence sizekle2:"card ?kle2 = Suc (card ?kle2 - 1)" using assm(2) by auto
   460   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}"
   461     using kle_range_induct[OF sizekle2, of n] using assm by auto
   462 
   463   have "card {k\<in>{1..n}. a k > b k} = 1" proof(rule ccontr) case goal1
   464     hence as:"card {k\<in>{1..n}. a k > b k} \<ge> 2" using ** by auto
   465     have *:"finite ?kle2" "finite ?kle1" "?kle2 \<union> ?kle1 = s" "?kle2 \<inter> ?kle1 = {}" using assm(2) by auto
   466     have "(card ?kle2 - 1) + 2 + (card ?kle1 - 1) = card ?kle2 + card ?kle1" using sizekle1 sizekle2 by auto
   467     also have "\<dots> = n + 1" unfolding card_Un_Int[OF *(1-2)] *(3-) using assm(3) by auto
   468     finally have n:"(card ?kle1 - 1) + 2 + (card ?kle2 - 1) = n + 1" by auto
   469     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}"
   470       apply(rule kle_range_combine_l[where y=f]) using e_f using `a\<in>s` assm(6) by auto
   471     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}"
   472       apply(rule kle_range_combine_r[where y=c]) using c_d using assm(6) and b by auto
   473     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-
   474       apply(rule kle_range_combine[where y=b]) using as and b assm(6) `a\<in>s` `d\<in>s` by blast+
   475     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-
   476       apply(rule kle_range_combine[where y=a]) using assm(6)[rule_format,OF `e\<in>s` `d\<in>s`] apply - by blast+
   477     moreover have "card {k \<in> {1..n}. e k > d k} \<le> card {1..n}" apply(rule card_mono) by auto
   478     ultimately show False unfolding n by auto qed
   479   then guess k unfolding card_1_exists .. note k=this[unfolded mem_Collect_eq]
   480 
   481   show ?thesis apply(rule disjI2) apply(rule_tac x=b in bexI,rule_tac x=k in bexI) proof
   482     fix j::nat have "kle n b a" using b and assm(6)[rule_format, OF `a\<in>s` `b\<in>s`] by auto
   483     then guess kk unfolding kle_def .. note kk_raw=this note kk=this[THEN conjunct2,rule_format]
   484     have kkk:"k\<in>kk" apply(rule ccontr) using k(1) unfolding kk by auto 
   485     show "a j = (if j = k then b j + 1 else b j)" proof(cases "j\<in>kk")
   486       case True hence "j=k" apply-apply(rule k(2)[rule_format]) using kk_raw kkk by auto
   487       thus ?thesis unfolding kk using kkk by auto next
   488       case False hence "j\<noteq>k" using k(2)[rule_format, of j k] using kk_raw kkk by auto
   489       thus ?thesis unfolding kk using kkk using False by auto qed qed(insert k(1) `b\<in>s`, auto) qed
   490 
   491 subsection {* The lemmas about simplices that we need. *}
   492 
   493 lemma card_funspace': assumes "finite s" "finite t" "card s = m" "card t = n"
   494   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) = _")
   495   using assms apply - proof(induct m arbitrary: s)
   496   have *:"{f. \<forall>x. f x = d} = {\<lambda>x. d}" apply(rule set_eqI,rule)unfolding mem_Collect_eq apply(rule,rule ext) by auto
   497   case 0 thus ?case by(auto simp add: *) next
   498   case (Suc m) guess a using card_eq_SucD[OF Suc(4)] .. then guess s0
   499     apply(erule_tac exE) apply(erule conjE)+ . note as0 = this
   500   have **:"card s0 = m" using as0 using Suc(2) Suc(4) by auto
   501   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}"
   502     apply(rule set_eqI,rule) unfolding mem_Collect_eq image_iff apply(erule conjE)
   503     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
   504     apply(erule bexE,rule) unfolding mem_Collect_eq apply(erule splitE)+ apply(erule conjE)+ proof-
   505     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"
   506       "\<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
   507   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-
   508     case goal1 note as = this(1,4-)[unfolded goal1 split_conv]
   509     have "xa = xb" using as(1)[THEN cong[of _ _ a]] by auto
   510     moreover have "ya = yb" proof(rule ext) fix x show "ya x = yb x" proof(cases "x = a") 
   511         case False thus ?thesis using as(1)[THEN cong[of _ _ x x]] by auto next
   512         case True thus ?thesis using as(5,7) using as0(2) by auto qed qed 
   513     ultimately show ?case unfolding goal1 by auto qed
   514   have "finite s0" using `finite s` unfolding as0 by simp
   515   show ?case unfolding as0 * card_image[OF inj] using assms
   516     unfolding SetCompr_Sigma_eq apply-
   517     unfolding card_cartesian_product
   518     using Suc(1)[OF `finite s0` `finite t` ** `card t = n`] by auto
   519 qed
   520 
   521 lemma card_funspace: assumes  "finite s" "finite t"
   522   shows "card {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)} = (card t) ^ (card s)"
   523   using assms by (auto intro: card_funspace')
   524 
   525 lemma finite_funspace: assumes "finite s" "finite t"
   526   shows "finite {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)}" (is "finite ?S")
   527 proof (cases "card t > 0")
   528   case True
   529   have "card ?S = (card t) ^ (card s)"
   530     using assms by (auto intro!: card_funspace)
   531   thus ?thesis using True by (auto intro: card_ge_0_finite)
   532 next
   533   case False hence "t = {}" using `finite t` by auto
   534   show ?thesis
   535   proof (cases "s = {}")
   536     have *:"{f. \<forall>x. f x = d} = {\<lambda>x. d}" by auto
   537     case True thus ?thesis using `t = {}` by (auto simp: *)
   538   next
   539     case False thus ?thesis using `t = {}` by simp
   540   qed
   541 qed
   542 
   543 lemma finite_simplices: "finite {s. ksimplex p n s}"
   544   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)}}"])
   545   unfolding ksimplex_def defer apply(rule finite_Collect_subsets) apply(rule finite_funspace) by auto
   546 
   547 lemma simplex_top_face: assumes "0<p" "\<forall>x\<in>f. x (n + 1) = p"
   548   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
   549   assume ?ls then guess s .. then guess a apply-apply(erule exE,(erule conjE)+) . note sa=this
   550   show ?rs unfolding ksimplex_def sa(3) apply(rule) defer apply rule defer apply(rule,rule,rule,rule) defer apply(rule,rule) proof-
   551     fix x y assume as:"x \<in>s - {a}" "y \<in>s - {a}" have xyp:"x (n + 1) = y (n + 1)"
   552         using as(1)[unfolded sa(3)[THEN sym], THEN assms(2)[rule_format]]
   553         using as(2)[unfolded sa(3)[THEN sym], THEN assms(2)[rule_format]] by auto
   554     show "kle n x y \<or> kle n y x" proof(cases "kle (n + 1) x y")
   555       case True then guess k unfolding kle_def .. note k=this hence *:"n+1 \<notin> k" using xyp by auto
   556       have "\<not> (\<exists>x\<in>k. x\<notin>{1..n})" apply(rule ccontr) unfolding not_not apply(erule bexE) proof-
   557         fix x assume as:"x \<in> k" "x \<notin> {1..n}" have "x \<noteq> n+1" using as and * by auto
   558         thus False using as and k[THEN conjunct1,unfolded subset_eq] by auto qed
   559       thus ?thesis apply-apply(rule disjI1) unfolding kle_def using k apply(rule_tac x=k in exI) by auto next
   560       case False hence "kle (n + 1) y x" using ksimplexD(6)[OF sa(1),rule_format, of x y] using as by auto
   561       then guess k unfolding kle_def .. note k=this hence *:"n+1 \<notin> k" using xyp by auto
   562       hence "\<not> (\<exists>x\<in>k. x\<notin>{1..n})" apply-apply(rule ccontr) unfolding not_not apply(erule bexE) proof-
   563         fix x assume as:"x \<in> k" "x \<notin> {1..n}" have "x \<noteq> n+1" using as and * by auto
   564         thus False using as and k[THEN conjunct1,unfolded subset_eq] by auto qed
   565       thus ?thesis apply-apply(rule disjI2) unfolding kle_def using k apply(rule_tac x=k in exI) by auto qed next
   566     fix x j assume as:"x\<in>s - {a}" "j\<notin>{1..n}"
   567     thus "x j = p" using as(1)[unfolded sa(3)[THEN sym], THEN assms(2)[rule_format]]
   568       apply(cases "j = n+1") using sa(1)[unfolded ksimplex_def] by auto qed(insert sa ksimplexD[OF sa(1)], auto) next
   569   assume ?rs note rs=ksimplexD[OF this] guess a b apply(rule ksimplex_extrema[OF `?rs`]) . note ab = this
   570   def c \<equiv> "\<lambda>i. if i = (n + 1) then p - 1 else a i"
   571   have "c\<notin>f" apply(rule ccontr) unfolding not_not apply(drule assms(2)[rule_format]) unfolding c_def using assms(1) by auto
   572   thus ?ls apply(rule_tac x="insert c f" in exI,rule_tac x=c in exI) unfolding ksimplex_def conj_assoc
   573     apply(rule conjI) defer apply(rule conjI) defer apply(rule conjI) defer apply(rule conjI) defer  
   574   proof(rule_tac[3-5] ballI allI)+
   575     fix x j assume x:"x \<in> insert c f" thus "x j \<le> p" proof (cases "x=c")
   576       case True show ?thesis unfolding True c_def apply(cases "j=n+1") using ab(1) and rs(4) by auto 
   577     qed(insert x rs(4), auto simp add:c_def)
   578     show "j \<notin> {1..n + 1} \<longrightarrow> x j = p" apply(cases "x=c") using x ab(1) rs(5) unfolding c_def by auto
   579     { 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-
   580         case False hence "z\<in>f" using z by auto
   581         then guess k apply(drule_tac ab(3)[THEN bspec[where x=z], THEN conjunct1]) unfolding kle_def apply(erule exE) .
   582         thus "kle (n + 1) c z" unfolding kle_def apply(rule_tac x="insert (n + 1) k" in exI) unfolding c_def
   583           using ab using rs(5)[rule_format,OF ab(1),of "n + 1"] assms(1) by auto qed auto } note * = this
   584     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")
   585       case False hence **:"x\<in>f" "y\<in>f" using x y by auto
   586       show ?thesis using rs(6)[rule_format,OF **] by(auto dest: kle_Suc) qed(insert * x y, auto)
   587   qed(insert rs, auto) qed
   588 
   589 lemma ksimplex_fix_plane:
   590   assumes "a \<in> s" "j\<in>{1..n::nat}" "\<forall>x\<in>s - {a}. x j = q" "a0 \<in> s" "a1 \<in> s"
   591   "\<forall>i. a1 i = ((if i\<in>{1..n} then a0 i + 1 else a0 i)::nat)"
   592   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
   593   show ?thesis apply(rule ccontr) using *[OF assms(3), of a0 a1] unfolding assms(6)[THEN spec[where x=j]]
   594     using assms(1-2,4-5) by auto qed
   595 
   596 lemma ksimplex_fix_plane_0:
   597   assumes "a \<in> s" "j\<in>{1..n::nat}" "\<forall>x\<in>s - {a}. x j = 0" "a0 \<in> s" "a1 \<in> s"
   598   "\<forall>i. a1 i = ((if i\<in>{1..n} then a0 i + 1 else a0 i)::nat)"
   599   shows "a = a1" apply(rule ccontr) using ksimplex_fix_plane[OF assms]
   600   using assms(3)[THEN bspec[where x=a1]] using assms(2,5)  
   601   unfolding assms(6)[THEN spec[where x=j]] by simp
   602 
   603 lemma ksimplex_fix_plane_p:
   604   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"
   605   "\<forall>i. a1 i = (if i\<in>{1..n} then a0 i + 1 else a0 i)"
   606   shows "a = a0" proof(rule ccontr) note s = ksimplexD[OF assms(1),rule_format]
   607   assume as:"a \<noteq> a0" hence *:"a0 \<in> s - {a}" using assms(5) by auto
   608   hence "a1 = a" using ksimplex_fix_plane[OF assms(2-)] by auto
   609   thus False using as using assms(3,5) and assms(7)[rule_format,of j]
   610     unfolding assms(4)[rule_format,OF *] using s(4)[OF assms(6), of j] by auto qed
   611 
   612 lemma ksimplex_replace_0:
   613   assumes "ksimplex p n s" "a \<in> s" "n \<noteq> 0" "j\<in>{1..n}" "\<forall>x\<in>s - {a}. x j = 0"
   614   shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 1" proof-
   615   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
   616   have **:"\<And>s' a'. ksimplex p n s' \<Longrightarrow> a' \<in> s' \<Longrightarrow> s' - {a'} = s - {a} \<Longrightarrow> s' = s" proof- case goal1
   617     guess a0 a1 apply(rule ksimplex_extrema_strong[OF assms(1,3)]) . note exta = this[rule_format]
   618     have a:"a = a1" apply(rule ksimplex_fix_plane_0[OF assms(2,4-5)]) using exta(1-2,5) by auto moreover
   619     guess b0 b1 apply(rule ksimplex_extrema_strong[OF goal1(1) assms(3)]) . note extb = this[rule_format]
   620     have a':"a' = b1" apply(rule ksimplex_fix_plane_0[OF goal1(2) assms(4), of b0]) unfolding goal1(3) using assms extb goal1 by auto moreover
   621     have "b0 = a0" unfolding kle_antisym[THEN sym, of b0 a0 n] using exta extb using goal1(3) unfolding a a' by blast
   622     hence "b1 = a1" apply-apply(rule ext) unfolding exta(5) extb(5) by auto ultimately
   623     show "s' = s" apply-apply(rule *[of _ a1 b1]) using exta(1-2) extb(1-2) goal1 by auto qed
   624   show ?thesis unfolding card_1_exists apply-apply(rule ex1I[of _ s])
   625     unfolding mem_Collect_eq defer apply(erule conjE bexE)+ apply(rule_tac a'=b in **) using assms(1,2) by auto qed
   626 
   627 lemma ksimplex_replace_1:
   628   assumes "ksimplex p n s" "a \<in> s" "n \<noteq> 0" "j\<in>{1..n}" "\<forall>x\<in>s - {a}. x j = p"
   629   shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 1" proof-
   630   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
   631   have lem:"\<And>s' a'. ksimplex p n s' \<Longrightarrow> a'\<in>s' \<Longrightarrow> s' - {a'} = s - {a} \<Longrightarrow> s' = s" proof- case goal1
   632     guess a0 a1 apply(rule ksimplex_extrema_strong[OF assms(1,3)]) . note exta = this[rule_format]
   633     have a:"a = a0" apply(rule ksimplex_fix_plane_p[OF assms(1-2,4-5) exta(1,2)]) unfolding exta by auto moreover
   634     guess b0 b1 apply(rule ksimplex_extrema_strong[OF goal1(1) assms(3)]) . note extb = this[rule_format]
   635     have a':"a' = b0" apply(rule ksimplex_fix_plane_p[OF goal1(1-2) assms(4), of _ b1]) unfolding goal1 extb using extb(1,2) assms(5) by auto
   636     moreover have *:"b1 = a1" unfolding kle_antisym[THEN sym, of b1 a1 n] using exta extb using goal1(3) unfolding a a' by blast moreover
   637     have "a0 = b0" apply(rule ext) proof- case goal1 show "a0 x = b0 x"
   638         using *[THEN cong, of x x] unfolding exta extb apply-apply(cases "x\<in>{1..n}") by auto qed
   639     ultimately show "s' = s" apply-apply(rule lem[OF goal1(3) _ goal1(2) assms(2)]) by auto qed 
   640   show ?thesis unfolding card_1_exists apply(rule ex1I[of _ s]) unfolding mem_Collect_eq apply(rule,rule assms(1))
   641     apply(rule_tac x=a in bexI) prefer 3 apply(erule conjE bexE)+ apply(rule_tac a'=b in lem) using assms(1-2) by auto qed
   642 
   643 lemma ksimplex_replace_2:
   644   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)"
   645   shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 2" (is "card ?A = 2")  proof-
   646   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
   647   have lem2:"\<And>a b. a\<in>s \<Longrightarrow> b\<noteq>a \<Longrightarrow> s \<noteq> insert b (s - {a})" proof case goal1
   648     hence "a\<in>insert b (s - {a})" by auto hence "a\<in> s - {a}" unfolding insert_iff using goal1 by auto
   649     thus False by auto qed
   650   guess a0 a1 apply(rule ksimplex_extrema_strong[OF assms(1,3)]) . note a0a1=this
   651   { assume "a=a0"
   652     have *:"\<And>P Q. (P \<or> Q) \<Longrightarrow> \<not> P \<Longrightarrow> Q" by auto
   653     have "\<exists>x\<in>s. \<not> kle n x a0" apply(rule_tac x=a1 in bexI) proof assume as:"kle n a1 a0"
   654       show False using kle_imp_pointwise[OF as,THEN spec[where x=1]] unfolding a0a1(5)[THEN spec[where x=1]]
   655         using assms(3) by auto qed(insert a0a1,auto)
   656     hence "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then a0 j + 1 else a0 j)"
   657       apply(rule_tac *[OF ksimplex_successor[OF assms(1-2),unfolded `a=a0`]]) by auto
   658     then guess a2 .. from this(2) guess k .. note k=this note a2=`a2\<in>s`
   659     def a3 \<equiv> "\<lambda>j. if j = k then a1 j + 1 else a1 j"
   660     have "a3 \<notin> s" proof assume "a3\<in>s" hence "kle n a3 a1" using a0a1(4) by auto
   661       thus False apply(drule_tac kle_imp_pointwise) unfolding a3_def
   662         apply(erule_tac x=k in allE) by auto qed
   663     hence "a3 \<noteq> a0" "a3 \<noteq> a1" using a0a1 by auto
   664     have "a2 \<noteq> a0" using k(2)[THEN spec[where x=k]] by auto
   665     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
   666       have "kle n a2 x \<or> kle n x a2" using ksimplexD(6)[OF assms(1)] and as `a2\<in>s` by auto moreover
   667       have "kle n a0 x" using a0a1(4) as by auto
   668       ultimately have "x = a0 \<or> x = a2" apply-apply(rule kle_adjacent[OF k(2)]) using goal1(2) by auto
   669       hence "x = a2" using as by auto thus False using goal1(2) using kle_refl by auto qed
   670     let ?s = "insert a3 (s - {a0})" have "ksimplex p n ?s" apply(rule ksimplexI) proof(rule_tac[2-] ballI,rule_tac[4] ballI)
   671       show "card ?s = n + 1" using ksimplexD(2-3)[OF assms(1)]
   672         using `a3\<noteq>a0` `a3\<notin>s` `a0\<in>s` by(auto simp add:card_insert_if)
   673       fix x assume x:"x \<in> insert a3 (s - {a0})"
   674       show "\<forall>j. x j \<le> p" proof(rule,cases "x = a3")
   675         fix j case False thus "x j\<le>p" using x ksimplexD(4)[OF assms(1)] by auto next
   676         fix j case True show "x j\<le>p" unfolding True proof(cases "j=k") 
   677           case False thus "a3 j \<le>p" unfolding True a3_def using `a1\<in>s` ksimplexD(4)[OF assms(1)] by auto next
   678           guess a4 using assms(5)[unfolded bex_simps ball_simps,rule_format,OF k(1)] .. note a4=this
   679           have "a2 k \<le> a4 k" using lem3[OF a4(1)[unfolded `a=a0`],THEN kle_imp_pointwise] by auto
   680           also have "\<dots> < p" using ksimplexD(4)[OF assms(1),rule_format,of a4 k] using a4 by auto
   681           finally have *:"a0 k + 1 < p" unfolding k(2)[rule_format] by auto
   682           case True thus "a3 j \<le>p" unfolding a3_def unfolding a0a1(5)[rule_format]
   683             using k(1) k(2)assms(5) using * by simp qed qed
   684       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}"
   685         { case False thus "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto }
   686         case True show "x j = p" unfolding True a3_def using j k(1) 
   687           using ksimplexD(5)[OF assms(1),rule_format,OF `a1\<in>s` j] by auto qed
   688       fix y assume y:"y\<in>insert a3 (s - {a0})"
   689       have lem4:"\<And>x. x\<in>s \<Longrightarrow> x\<noteq>a0 \<Longrightarrow> kle n x a3" proof- case goal1
   690         guess kk using a0a1(4)[rule_format,OF `x\<in>s`,THEN conjunct2,unfolded kle_def] 
   691           apply-apply(erule exE,erule conjE) . note kk=this
   692         have "k\<notin>kk" proof assume "k\<in>kk"
   693           hence "a1 k = x k + 1" using kk by auto
   694           hence "a0 k = x k" unfolding a0a1(5)[rule_format] using k(1) by auto
   695           hence "a2 k = x k + 1" unfolding k(2)[rule_format] by auto moreover
   696           have "a2 k \<le> x k" using lem3[of x,THEN kle_imp_pointwise] goal1 by auto 
   697           ultimately show False by auto qed
   698         thus ?case unfolding kle_def apply(rule_tac x="insert k kk" in exI) using kk(1)
   699           unfolding a3_def kle_def kk(2)[rule_format] using k(1) by auto qed
   700       show "kle n x y \<or> kle n y x" proof(cases "y=a3")
   701         case True show ?thesis unfolding True apply(cases "x=a3") defer apply(rule disjI1,rule lem4)
   702           using x by auto next
   703         case False show ?thesis proof(cases "x=a3") case True show ?thesis unfolding True
   704             apply(rule disjI2,rule lem4) using y False by auto next
   705           case False thus ?thesis apply(rule_tac ksimplexD(6)[OF assms(1),rule_format]) 
   706             using x y `y\<noteq>a3` by auto qed qed qed
   707     hence "insert a3 (s - {a0}) \<in> ?A" unfolding mem_Collect_eq apply-apply(rule,assumption)
   708       apply(rule_tac x="a3" in bexI) unfolding `a=a0` using `a3\<notin>s` by auto moreover
   709     have "s \<in> ?A" using assms(1,2) by auto ultimately have  "?A \<supseteq> {s, insert a3 (s - {a0})}" by auto
   710     moreover have "?A \<subseteq> {s, insert a3 (s - {a0})}" apply(rule) unfolding mem_Collect_eq proof(erule conjE)
   711       fix s' assume as:"ksimplex p n s'" and "\<exists>b\<in>s'. s' - {b} = s - {a}"
   712       from this(2) guess a' .. note a'=this
   713       guess a_min a_max apply(rule ksimplex_extrema_strong[OF as assms(3)]) . note min_max=this
   714       have *:"\<forall>x\<in>s' - {a'}. x k = a2 k" unfolding a' proof fix x assume x:"x\<in>s-{a}"
   715         hence "kle n a2 x" apply-apply(rule lem3) using `a=a0` by auto
   716         hence "a2 k \<le> x k" apply(drule_tac kle_imp_pointwise) by auto moreover
   717         have "x k \<le> a2 k" unfolding k(2)[rule_format] using a0a1(4)[rule_format,of x,THEN conjunct1] 
   718           unfolding kle_def using x by auto ultimately show "x k = a2 k" by auto qed
   719       have **:"a'=a_min \<or> a'=a_max" apply(rule ksimplex_fix_plane[OF a'(1) k(1) *]) using min_max by auto
   720       show "s' \<in> {s, insert a3 (s - {a0})}" proof(cases "a'=a_min")
   721         case True have "a_max = a1" unfolding kle_antisym[THEN sym,of a_max a1 n] apply(rule)
   722           apply(rule a0a1(4)[rule_format,THEN conjunct2]) defer  proof(rule min_max(4)[rule_format,THEN conjunct2])
   723           show "a1\<in>s'" using a' unfolding `a=a0` using a0a1 by auto
   724           show "a_max \<in> s" proof(rule ccontr) assume "a_max\<notin>s"
   725             hence "a_max = a'" using a' min_max by auto
   726             thus False unfolding True using min_max by auto qed qed
   727         hence "\<forall>i. a_max i = a1 i" by auto
   728         hence "a' = a" unfolding True `a=a0` apply-apply(subst fun_eq_iff,rule)
   729           apply(erule_tac x=x in allE) unfolding a0a1(5)[rule_format] min_max(5)[rule_format]
   730         proof- case goal1 thus ?case apply(cases "x\<in>{1..n}") by auto qed
   731         hence "s' = s" apply-apply(rule lem1[OF a'(2)]) using `a\<in>s` `a'\<in>s'` by auto
   732         thus ?thesis by auto next
   733         case False hence as:"a' = a_max" using ** by auto
   734         have "a_min = a2" unfolding kle_antisym[THEN sym, of _ _ n] apply rule
   735           apply(rule min_max(4)[rule_format,THEN conjunct1]) defer proof(rule lem3)
   736           show "a_min \<in> s - {a0}" unfolding a'(2)[THEN sym,unfolded `a=a0`] 
   737             unfolding as using min_max(1-3) by auto
   738           have "a2 \<noteq> a" unfolding `a=a0` using k(2)[rule_format,of k] by auto
   739           hence "a2 \<in> s - {a}" using a2 by auto thus "a2 \<in> s'" unfolding a'(2)[THEN sym] by auto qed
   740         hence "\<forall>i. a_min i = a2 i" by auto
   741         hence "a' = a3" unfolding as `a=a0` apply-apply(subst fun_eq_iff,rule)
   742           apply(erule_tac x=x in allE) unfolding a0a1(5)[rule_format] min_max(5)[rule_format]
   743           unfolding a3_def k(2)[rule_format] unfolding a0a1(5)[rule_format] proof- case goal1
   744           show ?case unfolding goal1 apply(cases "x\<in>{1..n}") defer apply(cases "x=k")
   745             using `k\<in>{1..n}` by auto qed
   746         hence "s' = insert a3 (s - {a0})" apply-apply(rule lem1) defer apply assumption
   747           apply(rule a'(1)) unfolding a' `a=a0` using `a3\<notin>s` by auto
   748         thus ?thesis by auto qed qed
   749     ultimately have *:"?A = {s, insert a3 (s - {a0})}" by blast
   750     have "s \<noteq> insert a3 (s - {a0})" using `a3\<notin>s` by auto
   751     hence ?thesis unfolding * by auto } moreover
   752   { assume "a=a1"
   753     have *:"\<And>P Q. (P \<or> Q) \<Longrightarrow> \<not> P \<Longrightarrow> Q" by auto
   754     have "\<exists>x\<in>s. \<not> kle n a1 x" apply(rule_tac x=a0 in bexI) proof assume as:"kle n a1 a0"
   755       show False using kle_imp_pointwise[OF as,THEN spec[where x=1]] unfolding a0a1(5)[THEN spec[where x=1]]
   756         using assms(3) by auto qed(insert a0a1,auto)
   757     hence "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. a1 j = (if j = k then y j + 1 else y j)"
   758       apply(rule_tac *[OF ksimplex_predecessor[OF assms(1-2),unfolded `a=a1`]]) by auto
   759     then guess a2 .. from this(2) guess k .. note k=this note a2=`a2\<in>s`
   760     def a3 \<equiv> "\<lambda>j. if j = k then a0 j - 1 else a0 j"
   761     have "a2 \<noteq> a1" using k(2)[THEN spec[where x=k]] by auto
   762     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
   763       have "kle n a2 x \<or> kle n x a2" using ksimplexD(6)[OF assms(1)] and as `a2\<in>s` by auto moreover
   764       have "kle n x a1" using a0a1(4) as by auto
   765       ultimately have "x = a2 \<or> x = a1" apply-apply(rule kle_adjacent[OF k(2)]) using goal1(2) by auto
   766       hence "x = a2" using as by auto thus False using goal1(2) using kle_refl by auto qed
   767     have "a0 k \<noteq> 0" proof-
   768       guess a4 using assms(4)[unfolded bex_simps ball_simps,rule_format,OF `k\<in>{1..n}`] .. note a4=this
   769       have "a4 k \<le> a2 k" using lem3[OF a4(1)[unfolded `a=a1`],THEN kle_imp_pointwise] by auto
   770       moreover have "a4 k > 0" using a4 by auto ultimately have "a2 k > 0" by auto
   771       hence "a1 k > 1" unfolding k(2)[rule_format] by simp
   772       thus ?thesis unfolding a0a1(5)[rule_format] using k(1) by simp qed
   773     hence lem4:"\<forall>j. a0 j = (if j=k then a3 j + 1 else a3 j)" unfolding a3_def by simp
   774     have "\<not> kle n a0 a3" apply(rule ccontr) unfolding not_not apply(drule kle_imp_pointwise)
   775       unfolding lem4[rule_format] apply(erule_tac x=k in allE) by auto
   776     hence "a3 \<notin> s" using a0a1(4) by auto
   777     hence "a3 \<noteq> a1" "a3 \<noteq> a0" using a0a1 by auto
   778     let ?s = "insert a3 (s - {a1})" have "ksimplex p n ?s" apply(rule ksimplexI) proof(rule_tac[2-] ballI,rule_tac[4] ballI)
   779       show "card ?s = n+1" using ksimplexD(2-3)[OF assms(1)]
   780         using `a3\<noteq>a0` `a3\<notin>s` `a1\<in>s` by(auto simp add:card_insert_if)
   781       fix x assume x:"x \<in> insert a3 (s - {a1})"
   782       show "\<forall>j. x j \<le> p" proof(rule,cases "x = a3")
   783         fix j case False thus "x j\<le>p" using x ksimplexD(4)[OF assms(1)] by auto next
   784         fix j case True show "x j\<le>p" unfolding True proof(cases "j=k") 
   785           case False thus "a3 j \<le>p" unfolding True a3_def using `a0\<in>s` ksimplexD(4)[OF assms(1)] by auto next
   786           guess a4 using assms(5)[unfolded bex_simps ball_simps,rule_format,OF k(1)] .. note a4=this
   787           case True have "a3 k \<le> a0 k" unfolding lem4[rule_format] by auto
   788           also have "\<dots> \<le> p" using ksimplexD(4)[OF assms(1),rule_format,of a0 k] a0a1 by auto
   789           finally show "a3 j \<le> p" unfolding True by auto qed qed
   790       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}"
   791         { case False thus "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto }
   792         case True show "x j = p" unfolding True a3_def using j k(1) 
   793           using ksimplexD(5)[OF assms(1),rule_format,OF `a0\<in>s` j] by auto qed
   794       fix y assume y:"y\<in>insert a3 (s - {a1})"
   795       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
   796         have "kle n a3 a2" proof- have "kle n a0 a1" using a0a1 by auto then guess kk unfolding kle_def ..
   797           thus ?thesis unfolding kle_def apply(rule_tac x=kk in exI) unfolding lem4[rule_format] k(2)[rule_format]
   798             apply(rule)defer proof(rule) case goal1 thus ?case apply-apply(erule conjE)
   799               apply(erule_tac[!] x=j in allE) apply(cases "j\<in>kk") apply(case_tac[!] "j=k") by auto qed auto qed moreover
   800         have "kle n a3 a0" unfolding kle_def lem4[rule_format] apply(rule_tac x="{k}" in exI) using k(1) by auto
   801         ultimately show ?case apply-apply(rule kle_between_l[of _ a0 _ a2]) using lem3[OF *]
   802           using a0a1(4)[rule_format,OF goal1(1)] by auto qed
   803       show "kle n x y \<or> kle n y x" proof(cases "y=a3")
   804         case True show ?thesis unfolding True apply(cases "x=a3") defer apply(rule disjI2,rule lem4)
   805           using x by auto next
   806         case False show ?thesis proof(cases "x=a3") case True show ?thesis unfolding True
   807             apply(rule disjI1,rule lem4) using y False by auto next
   808           case False thus ?thesis apply(rule_tac ksimplexD(6)[OF assms(1),rule_format]) 
   809             using x y `y\<noteq>a3` by auto qed qed qed
   810     hence "insert a3 (s - {a1}) \<in> ?A" unfolding mem_Collect_eq apply-apply(rule,assumption)
   811       apply(rule_tac x="a3" in bexI) unfolding `a=a1` using `a3\<notin>s` by auto moreover
   812     have "s \<in> ?A" using assms(1,2) by auto ultimately have  "?A \<supseteq> {s, insert a3 (s - {a1})}" by auto
   813     moreover have "?A \<subseteq> {s, insert a3 (s - {a1})}" apply(rule) unfolding mem_Collect_eq proof(erule conjE)
   814       fix s' assume as:"ksimplex p n s'" and "\<exists>b\<in>s'. s' - {b} = s - {a}"
   815       from this(2) guess a' .. note a'=this
   816       guess a_min a_max apply(rule ksimplex_extrema_strong[OF as assms(3)]) . note min_max=this
   817       have *:"\<forall>x\<in>s' - {a'}. x k = a2 k" unfolding a' proof fix x assume x:"x\<in>s-{a}"
   818         hence "kle n x a2" apply-apply(rule lem3) using `a=a1` by auto
   819         hence "x k \<le> a2 k" apply(drule_tac kle_imp_pointwise) by auto moreover
   820         { have "a2 k \<le> a0 k" using k(2)[rule_format,of k] unfolding a0a1(5)[rule_format] using k(1) by simp
   821           also have "\<dots> \<le> x k" using a0a1(4)[rule_format,of x,THEN conjunct1,THEN kle_imp_pointwise] x by auto
   822           finally have "a2 k \<le> x k" . } ultimately show "x k = a2 k" by auto qed
   823       have **:"a'=a_min \<or> a'=a_max" apply(rule ksimplex_fix_plane[OF a'(1) k(1) *]) using min_max by auto
   824       have "a2 \<noteq> a1" proof assume as:"a2 = a1"
   825         show False using k(2) unfolding as apply(erule_tac x=k in allE) by auto qed
   826       hence a2':"a2 \<in> s' - {a'}" unfolding a' using a2 unfolding `a=a1` by auto
   827       show "s' \<in> {s, insert a3 (s - {a1})}" proof(cases "a'=a_min")
   828         case True have "a_max \<in> s - {a1}" using min_max unfolding a'(2)[unfolded `a=a1`,THEN sym] True by auto
   829         hence "a_max = a2" unfolding kle_antisym[THEN sym,of a_max a2 n] apply-apply(rule)
   830           apply(rule lem3,assumption) apply(rule min_max(4)[rule_format,THEN conjunct2]) using a2' by auto
   831         hence a_max:"\<forall>i. a_max i = a2 i" by auto
   832         have *:"\<forall>j. a2 j = (if j\<in>{1..n} then a3 j + 1 else a3 j)" 
   833           using k(2) unfolding lem4[rule_format] a0a1(5)[rule_format] apply-apply(rule,erule_tac x=j in allE)
   834         proof- case goal1 thus ?case apply(cases "j\<in>{1..n}",case_tac[!] "j=k") by auto qed
   835         have "\<forall>i. a_min i = a3 i" using a_max apply-apply(rule,erule_tac x=i in allE)
   836           unfolding min_max(5)[rule_format] *[rule_format] proof- case goal1
   837           thus ?case apply(cases "i\<in>{1..n}") by auto qed hence "a_min = a3" unfolding fun_eq_iff .
   838         hence "s' = insert a3 (s - {a1})" using a' unfolding `a=a1` True by auto thus ?thesis by auto next
   839         case False hence as:"a'=a_max" using ** by auto
   840         have "a_min = a0" unfolding kle_antisym[THEN sym,of _ _ n] apply(rule)
   841           apply(rule min_max(4)[rule_format,THEN conjunct1]) defer apply(rule a0a1(4)[rule_format,THEN conjunct1]) proof-
   842           have "a_min \<in> s - {a1}" using min_max(1,3) unfolding a'(2)[THEN sym,unfolded `a=a1`] as by auto
   843           thus "a_min \<in> s" by auto have "a0 \<in> s - {a1}" using a0a1(1-3) by auto thus "a0 \<in> s'"
   844             unfolding a'(2)[THEN sym,unfolded `a=a1`] by auto qed
   845         hence "\<forall>i. a_max i = a1 i" unfolding a0a1(5)[rule_format] min_max(5)[rule_format] by auto
   846         hence "s' = s" apply-apply(rule lem1[OF a'(2)]) using `a\<in>s` `a'\<in>s'` unfolding as `a=a1` unfolding fun_eq_iff by auto
   847         thus ?thesis by auto qed qed 
   848     ultimately have *:"?A = {s, insert a3 (s - {a1})}" by blast
   849     have "s \<noteq> insert a3 (s - {a1})" using `a3\<notin>s` by auto
   850     hence ?thesis unfolding * by auto } moreover
   851   { assume as:"a\<noteq>a0" "a\<noteq>a1" have "\<not> (\<forall>x\<in>s. kle n a x)" proof case goal1
   852       have "a=a0" unfolding kle_antisym[THEN sym,of _ _ n] apply(rule)
   853         using goal1 a0a1 assms(2) by auto thus False using as by auto qed
   854     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
   855     then guess u .. from this(2) guess k .. note k = this[rule_format] note u = `u\<in>s`
   856     have "\<not> (\<forall>x\<in>s. kle n x a)" proof case goal1
   857       have "a=a1" unfolding kle_antisym[THEN sym,of _ _ n] apply(rule)
   858         using goal1 a0a1 assms(2) by auto thus False using as by auto qed
   859     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
   860     then guess v .. from this(2) guess l .. note l = this[rule_format] note v = `v\<in>s`
   861     def a' \<equiv> "\<lambda>j. if j = l then u j + 1 else u j"
   862     have kl:"k \<noteq> l" proof assume "k=l" have *:"\<And>P. (if P then (1::nat) else 0) \<noteq> 2" by auto
   863       thus False using ksimplexD(6)[OF assms(1),rule_format,OF u v] unfolding kle_def
   864         unfolding l(2) k(2) `k=l` apply-apply(erule disjE)apply(erule_tac[!] exE conjE)+
   865         apply(erule_tac[!] x=l in allE)+ by(auto simp add: *) qed
   866     hence aa':"a'\<noteq>a" apply-apply rule unfolding fun_eq_iff unfolding a'_def k(2)
   867       apply(erule_tac x=l in allE) by auto
   868     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'")
   869       case goal2 hence "kle n a' a" by auto thus False apply(drule_tac kle_imp_pointwise)
   870         apply(erule_tac x=l in allE) unfolding a'_def k(2) using kl by auto next
   871       case True thus False apply(drule_tac kle_imp_pointwise)
   872         apply(erule_tac x=k in allE) unfolding a'_def k(2) using kl by auto qed
   873     have kle_uv:"kle n u a" "kle n u a'" "kle n a v" "kle n a' v" unfolding kle_def apply-
   874       apply(rule_tac[1] x="{k}" in exI,rule_tac[2] x="{l}" in exI)
   875       apply(rule_tac[3] x="{l}" in exI,rule_tac[4] x="{k}" in exI)
   876       unfolding l(2) k(2) a'_def using l(1) k(1) by auto
   877     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)"
   878     proof- case goal1 thus ?case proof(cases "x k = u k", case_tac[!] "x l = u l")
   879       assume as:"x l = u l" "x k = u k"
   880       have "x = u" unfolding fun_eq_iff
   881         using goal1(2)[THEN kle_imp_pointwise,unfolded l(2)] unfolding k(2) apply-
   882         using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1
   883         thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next
   884       assume as:"x l \<noteq> u l" "x k = u k"
   885       have "x = a'" unfolding fun_eq_iff unfolding a'_def
   886         using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply-
   887         using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1
   888         thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next
   889       assume as:"x l = u l" "x k \<noteq> u k"
   890       have "x = a" unfolding fun_eq_iff
   891         using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply-
   892         using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1
   893         thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next
   894       assume as:"x l \<noteq> u l" "x k \<noteq> u k"
   895       have "x = v" unfolding fun_eq_iff
   896         using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply-
   897         using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1
   898         thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as `k\<noteq>l` by auto qed thus ?case by auto qed qed
   899     have uv:"kle n u v" apply(rule kle_trans[OF kle_uv(1,3)]) using ksimplexD(6)[OF assms(1)] using u v by auto
   900     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])
   901       prefer 3 apply(rule kle_trans[OF uv]) defer apply(rule ksimplexD(6)[OF assms(1),rule_format])
   902       using kle_uv `u\<in>s` by auto
   903     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])
   904       prefer 4 apply(rule kle_trans[OF _ uv]) defer apply(rule ksimplexD(6)[OF assms(1),rule_format])
   905       using kle_uv `v\<in>s` by auto
   906     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
   907       proof(cases "kle n v x \<or> kle n x u") case True thus ?thesis using goal1 by(auto intro:lem3 lem4) next
   908         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
   909         show ?thesis using uxv[OF *] using kle_uv using goal1 by auto qed qed
   910     have "ksimplex p n (insert a' (s - {a}))" apply(rule ksimplexI) proof(rule_tac[2-] ballI,rule_tac[4] ballI)
   911       show "card (insert a' (s - {a})) = n + 1" using ksimplexD(2-3)[OF assms(1)]
   912         using `a'\<noteq>a` `a'\<notin>s` `a\<in>s` by(auto simp add:card_insert_if)
   913       fix x assume x:"x \<in> insert a' (s - {a})"
   914       show "\<forall>j. x j \<le> p" proof(rule,cases "x = a'")
   915         fix j case False thus "x j\<le>p" using x ksimplexD(4)[OF assms(1)] by auto next
   916         fix j case True show "x j\<le>p" unfolding True proof(cases "j=l") 
   917           case False thus "a' j \<le>p" unfolding True a'_def using `u\<in>s` ksimplexD(4)[OF assms(1)] by auto next
   918           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
   919           have "u l + 1 \<le> p" unfolding *[THEN sym] using ksimplexD(4)[OF assms(1)] using `v\<in>s` by auto
   920           thus "a' j \<le>p" unfolding a'_def True by auto qed qed
   921       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}"
   922         { case False thus "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto }
   923         case True show "x j = p" unfolding True a'_def using j l(1) 
   924           using ksimplexD(5)[OF assms(1),rule_format,OF `u\<in>s` j] by auto qed
   925       fix y assume y:"y\<in>insert a' (s - {a})"
   926       show "kle n x y \<or> kle n y x" proof(cases "y=a'")
   927         case True show ?thesis unfolding True apply(cases "x=a'") defer apply(rule lem5) using x by auto next
   928         case False show ?thesis proof(cases "x=a'") case True show ?thesis unfolding True
   929             using lem5[of y] using y by auto next
   930           case False thus ?thesis apply(rule_tac ksimplexD(6)[OF assms(1),rule_format]) 
   931             using x y `y\<noteq>a'` by auto qed qed qed
   932     hence "insert a' (s - {a}) \<in> ?A" unfolding mem_Collect_eq apply-apply(rule,assumption)
   933       apply(rule_tac x="a'" in bexI) using aa' `a'\<notin>s` by auto moreover
   934     have "s \<in> ?A" using assms(1,2) by auto ultimately have  "?A \<supseteq> {s, insert a' (s - {a})}" by auto
   935     moreover have "?A \<subseteq> {s, insert a' (s - {a})}" apply(rule) unfolding mem_Collect_eq proof(erule conjE)
   936       fix s' assume as:"ksimplex p n s'" and "\<exists>b\<in>s'. s' - {b} = s - {a}"
   937       from this(2) guess a'' .. note a''=this
   938       have "u\<noteq>v" unfolding fun_eq_iff unfolding l(2) k(2) by auto
   939       hence uv':"\<not> kle n v u" using uv using kle_antisym by auto
   940       have "u\<noteq>a" "v\<noteq>a" unfolding fun_eq_iff k(2) l(2) by auto 
   941       hence uvs':"u\<in>s'" "v\<in>s'" using `u\<in>s` `v\<in>s` using a'' by auto
   942       have lem6:"a \<in> s' \<or> a' \<in> s'" proof(cases "\<forall>x\<in>s'. kle n x u \<or> kle n v x")
   943         case False then guess w unfolding ball_simps .. note w=this
   944         hence "kle n u w" "kle n w v" using ksimplexD(6)[OF as] uvs' by auto
   945         hence "w = a' \<or> w = a" using uxv[of w] uvs' w by auto thus ?thesis using w by auto next
   946         case True have "\<not> (\<forall>x\<in>s'. kle n x u)" unfolding ball_simps apply(rule_tac x=v in bexI)
   947           using uv `u\<noteq>v` unfolding kle_antisym[of n u v,THEN sym] using `v\<in>s'` by auto
   948         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
   949         then guess w .. note w=this from this(2) guess kk .. note kk=this[rule_format]
   950         have "\<not> kle n w u" apply-apply(rule,drule kle_imp_pointwise) 
   951           apply(erule_tac x=kk in allE) unfolding kk by auto 
   952         hence *:"kle n v w" using True[rule_format,OF w(1)] by auto
   953         hence False proof(cases "kk\<noteq>l") case True thus False using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)]
   954             apply(erule_tac x=l in allE) using `k\<noteq>l` by auto  next
   955           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)]
   956             apply(erule_tac x=k in allE) using `k\<noteq>l` by auto qed
   957         thus ?thesis by auto qed
   958       thus "s' \<in> {s, insert a' (s - {a})}" proof(cases "a\<in>s'")
   959         case True hence "s' = s" apply-apply(rule lem1[OF a''(2)]) using a'' `a\<in>s` by auto
   960         thus ?thesis by auto next case False hence "a'\<in>s'" using lem6 by auto
   961         hence "s' = insert a' (s - {a})" apply-apply(rule lem1[of _ a'' _ a'])
   962           unfolding a''(2)[THEN sym] using a'' using `a'\<notin>s` by auto
   963         thus ?thesis by auto qed qed 
   964     ultimately have *:"?A = {s, insert a' (s - {a})}" by blast
   965     have "s \<noteq> insert a' (s - {a})" using `a'\<notin>s` by auto
   966     hence ?thesis unfolding * by auto } 
   967   ultimately show ?thesis by auto qed
   968 
   969 subsection {* Hence another step towards concreteness. *}
   970 
   971 lemma kuhn_simplex_lemma:
   972   assumes "\<forall>s. ksimplex p (n + 1) s \<longrightarrow> (rl ` s \<subseteq>{0..n+1})"
   973   "odd (card{f. \<exists>s a. ksimplex p (n + 1) s \<and> a \<in> s \<and> (f = s - {a}) \<and>
   974   (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))})"
   975   shows "odd(card {s\<in>{s. ksimplex p (n + 1) s}. rl ` s = {0..n+1} })" proof-
   976   have *:"\<And>x y. x = y \<Longrightarrow> odd (card x) \<Longrightarrow> odd (card y)" by auto
   977   have *:"odd(card {f\<in>{f. \<exists>s\<in>{s. ksimplex p (n + 1) s}. (\<exists>a\<in>s. f = s - {a})}. 
   978                 (rl ` f = {0..n}) \<and>
   979                ((\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = 0) \<or>
   980                 (\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = p))})" apply(rule *[OF _ assms(2)]) by auto
   981   show ?thesis apply(rule kuhn_complete_lemma[OF finite_simplices]) prefer 6 apply(rule *) apply(rule,rule,rule)
   982     apply(subst ksimplex_def) defer apply(rule,rule assms(1)[rule_format]) unfolding mem_Collect_eq apply assumption
   983     apply default+ unfolding mem_Collect_eq apply(erule disjE bexE)+ defer apply(erule disjE bexE)+ defer 
   984     apply default+ unfolding mem_Collect_eq apply(erule disjE bexE)+ unfolding mem_Collect_eq proof-
   985     fix f s a assume as:"ksimplex p (n + 1) s" "a\<in>s" "f = s - {a}"
   986     let ?S = "{s. ksimplex p (n + 1) s \<and> (\<exists>a\<in>s. f = s - {a})}"
   987     have S:"?S = {s'. ksimplex p (n + 1) s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})}" unfolding as by blast
   988     { 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
   989         apply-apply(rule ksimplex_replace_0) apply(rule as)+ unfolding as by auto }
   990     { 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
   991         apply-apply(rule ksimplex_replace_1) apply(rule as)+ unfolding as by auto }
   992     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"
   993       unfolding S apply(rule ksimplex_replace_2) apply(rule as)+ unfolding as by auto qed auto qed
   994 
   995 subsection {* Reduced labelling. *}
   996 
   997 definition "reduced label (n::nat) (x::nat\<Rightarrow>nat) =
   998   (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)))"
   999 
  1000 lemma reduced_labelling: shows "reduced label n x \<le> n" (is ?t1) and
  1001   "\<forall>i. 1\<le>i \<and> i < reduced label n x + 1 \<longrightarrow> (label x i = 0)" (is ?t2)
  1002   "(reduced label n x = n) \<or> (label x (reduced label n x + 1) \<noteq> 0)"  (is ?t3) proof-
  1003   have num_WOP:"\<And>P k. P (k::nat) \<Longrightarrow> \<exists>n. P n \<and> (\<forall>m<n. \<not> P m)"
  1004     apply(drule ex_has_least_nat[where m="\<lambda>x. x"]) apply(erule exE,rule_tac x=x in exI) by auto
  1005   have *:"n \<le> n \<and> (label x (n + 1) \<noteq> 0 \<or> n = n)" by auto
  1006   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) . note N=this
  1007   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)
  1008     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)
  1009   show ?t1 ?t2 ?t3 unfolding reduced_def apply(rule_tac[!] someI2_ex) using N' by(auto intro!: exI[where x=N]) qed
  1010 
  1011 lemma reduced_labelling_unique: fixes x::"nat \<Rightarrow> nat"
  1012   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)"
  1013   shows "reduced label n x = r" apply(rule le_antisym) apply(rule_tac[!] ccontr) unfolding not_le
  1014   using reduced_labelling[of label n x] using assms by auto
  1015 
  1016 lemma reduced_labelling_0: assumes "j\<in>{1..n}" "label x j = 0" shows "reduced label n x \<noteq> j - 1"
  1017   using reduced_labelling[of label n x] using assms by fastsimp 
  1018 
  1019 lemma reduced_labelling_1: assumes "j\<in>{1..n}" "label x j \<noteq> 0" shows "reduced label n x < j"
  1020   using assms and reduced_labelling[of label n x] apply(erule_tac x=j in allE) by auto
  1021 
  1022 lemma reduced_labelling_Suc:
  1023   assumes "reduced lab (n + 1) x \<noteq> n + 1" shows "reduced lab (n + 1) x = reduced lab n x"
  1024   apply(subst eq_commute) apply(rule reduced_labelling_unique)
  1025   using reduced_labelling[of lab "n+1" x] and assms by auto 
  1026 
  1027 lemma complete_face_top:
  1028   assumes "\<forall>x\<in>f. \<forall>j\<in>{1..n+1}. x j = 0 \<longrightarrow> lab x j = 0"
  1029           "\<forall>x\<in>f. \<forall>j\<in>{1..n+1}. x j = p \<longrightarrow> lab x j = 1"
  1030   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>
  1031   ((reduced lab (n + 1)) ` f = {0..n}) \<and> (\<forall>x\<in>f. x (n + 1) = p)" (is "?l = ?r") proof
  1032   assume ?l (is "?as \<and> (?a \<or> ?b)") thus ?r apply-apply(rule,erule conjE,assumption) proof(cases ?a)
  1033     case True then guess j .. note j=this {fix x assume x:"x\<in>f"
  1034       have "reduced lab (n+1) x \<noteq> j - 1" using j apply-apply(rule reduced_labelling_0) defer apply(rule assms(1)[rule_format]) using x by auto }
  1035     moreover have "j - 1 \<in> {0..n}" using j by auto
  1036     then guess y unfolding `?l`[THEN conjunct1,THEN sym] and image_iff .. note y = this
  1037     ultimately have False by auto thus "\<forall>x\<in>f. x (n + 1) = p" by auto next
  1038 
  1039     case False hence ?b using `?l` by blast then guess j .. note j=this {fix x assume x:"x\<in>f"
  1040       have "reduced lab (n+1) x < j" using j apply-apply(rule reduced_labelling_1) using assms(2)[rule_format,of x j] and x by auto } note * = this
  1041     have "j = n + 1" proof(rule ccontr) case goal1 hence "j < n + 1" using j by auto moreover
  1042       have "n \<in> {0..n}" by auto then guess y unfolding `?l`[THEN conjunct1,THEN sym] image_iff ..
  1043       ultimately show False using *[of y] by auto qed
  1044     thus "\<forall>x\<in>f. x (n + 1) = p" using j by auto qed qed(auto)
  1045 
  1046 subsection {* Hence we get just about the nice induction. *}
  1047 
  1048 lemma kuhn_induction:
  1049   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)"
  1050                   "\<forall>x. \<forall>j\<in>{1..n+1}. (\<forall>j. x j \<le> p) \<and> (x j = p) \<longrightarrow> (lab x j = 1)"
  1051         "odd (card {f. ksimplex p n f \<and> ((reduced lab n) ` f = {0..n})})"
  1052   shows "odd (card {s. ksimplex p (n+1) s \<and>((reduced lab (n+1)) `  s = {0..n+1})})" proof-
  1053   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
  1054   show ?thesis apply(rule kuhn_simplex_lemma[unfolded mem_Collect_eq]) apply(rule,rule,rule *,rule reduced_labelling)
  1055     apply(rule *(1)[OF assms(4)]) apply(rule set_eqI) unfolding mem_Collect_eq apply(rule,erule conjE) defer apply(rule) proof-(*(rule,rule)*)
  1056     fix f assume as:"ksimplex p n f" "reduced lab n ` f = {0..n}"
  1057     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"
  1058       using assms(2-3) using as(1)[unfolded ksimplex_def] by auto
  1059     have allp:"\<forall>x\<in>f. x (n + 1) = p" using assms(2) using as(1)[unfolded ksimplex_def] by auto
  1060     { fix x assume "x\<in>f" hence "reduced lab (n + 1) x < n + 1" apply-apply(rule reduced_labelling_1)
  1061         defer using assms(3) using as(1)[unfolded ksimplex_def] by auto
  1062       hence "reduced lab (n + 1) x = reduced lab n x" apply-apply(rule reduced_labelling_Suc) using reduced_labelling(1) by auto }
  1063     hence "reduced lab (n + 1) ` f = {0..n}" unfolding as(2)[THEN sym] apply- apply(rule set_eqI) unfolding image_iff by auto
  1064     moreover guess s using as(1)[unfolded simplex_top_face[OF assms(1) allp,THEN sym]] .. then guess a ..
  1065     ultimately show "\<exists>s a. ksimplex p (n + 1) s \<and>
  1066       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)
  1067       apply(rule_tac x=s in exI,rule_tac x=a in exI) unfolding complete_face_top[OF *] using allp as(1) by auto
  1068   next fix f assume as:"\<exists>s a. ksimplex p (n + 1) s \<and>
  1069       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)
  1070     then guess s .. then guess a apply-apply(erule exE,(erule conjE)+) . note sa=this
  1071     { fix x assume "x\<in>f" hence "reduced lab (n + 1) x \<in> reduced lab (n + 1) ` f" by auto
  1072       hence "reduced lab (n + 1) x < n + 1" using sa(4) by auto 
  1073       hence "reduced lab (n + 1) x = reduced lab n x" apply-apply(rule reduced_labelling_Suc)
  1074         using reduced_labelling(1) by auto }
  1075     thus part1:"reduced lab n ` f = {0..n}" unfolding sa(4)[THEN sym] apply-apply(rule set_eqI) unfolding image_iff by auto
  1076     have *:"\<forall>x\<in>f. x (n + 1) = p" proof(cases "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0")
  1077       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_0) apply assumption
  1078         apply(rule assms(2)[rule_format]) using sa(1)[unfolded ksimplex_def] unfolding sa by auto moreover
  1079       have "j - 1 \<in> {0..n}" using `j\<in>{1..n+1}` by auto
  1080       ultimately have False unfolding sa(4)[THEN sym] unfolding image_iff by fastsimp thus ?thesis by auto next
  1081       case False hence "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p" using sa(5) by fastsimp then guess j .. note j=this
  1082       thus ?thesis proof(cases "j = n+1")
  1083         case False hence *:"j\<in>{1..n}" using j by auto
  1084         hence "\<And>x. x\<in>f \<Longrightarrow> reduced lab n x < j" apply(rule reduced_labelling_1) proof- fix x assume "x\<in>f"
  1085           hence "lab x j = 1" apply-apply(rule assms(3)[rule_format,OF j(1)]) 
  1086             using sa(1)[unfolded ksimplex_def] using j unfolding sa by auto thus "lab x j \<noteq> 0" by auto qed
  1087         moreover have "j\<in>{0..n}" using * by auto
  1088         ultimately have False unfolding part1[THEN sym] using * unfolding image_iff by auto thus ?thesis by auto qed auto qed 
  1089     thus "ksimplex p n f" using as unfolding simplex_top_face[OF assms(1) *,THEN sym] by auto qed qed
  1090 
  1091 lemma kuhn_induction_Suc:
  1092   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)"
  1093                   "\<forall>x. \<forall>j\<in>{1..Suc n}. (\<forall>j. x j \<le> p) \<and> (x j = p) \<longrightarrow> (lab x j = 1)"
  1094         "odd (card {f. ksimplex p n f \<and> ((reduced lab n) ` f = {0..n})})"
  1095   shows "odd (card {s. ksimplex p (Suc n) s \<and>((reduced lab (Suc n)) `  s = {0..Suc n})})"
  1096   using assms unfolding Suc_eq_plus1 by(rule kuhn_induction)
  1097 
  1098 subsection {* And so we get the final combinatorial result. *}
  1099 
  1100 lemma ksimplex_0: "ksimplex p 0 s \<longleftrightarrow> s = {(\<lambda>x. p)}" (is "?l = ?r") proof
  1101   assume l:?l guess a using ksimplexD(3)[OF l, unfolded add_0] unfolding card_1_exists .. note a=this
  1102   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
  1103   assume r:?r show ?l unfolding r ksimplex_eq by auto qed
  1104 
  1105 lemma reduce_labelling_0[simp]: "reduced lab 0 x = 0" apply(rule reduced_labelling_unique) by auto
  1106 
  1107 lemma kuhn_combinatorial:
  1108   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)"
  1109   "\<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)"
  1110   shows " odd (card {s. ksimplex p n s \<and> ((reduced lab n) ` s = {0..n})})" using assms proof(induct n)
  1111   let ?M = "\<lambda>n. {s. ksimplex p n s \<and> ((reduced lab n) ` s = {0..n})}"
  1112   { case 0 have *:"?M 0 = {{(\<lambda>x. p)}}" unfolding ksimplex_0 by auto show ?case unfolding * by auto }
  1113   case (Suc n) have "odd (card (?M n))" apply(rule Suc(1)[OF Suc(2)]) using Suc(3-) by auto
  1114   thus ?case apply-apply(rule kuhn_induction_Suc) using Suc(2-) by auto qed
  1115 
  1116 lemma kuhn_lemma: assumes "0 < (p::nat)" "0 < (n::nat)"
  1117   "\<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))"
  1118   "\<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))"
  1119   "\<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))"
  1120   obtains q where "\<forall>i\<in>{1..n}. q i < p"
  1121   "\<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>
  1122                                (\<forall>j\<in>{1..n}. q(j) \<le> s(j) \<and> s(j) \<le> q(j) + 1) \<and>
  1123                                ~(label r i = label s i)" proof-
  1124   let ?A = "{s. ksimplex p n s \<and> reduced label n ` s = {0..n}}" have "n\<noteq>0" using assms by auto
  1125   have conjD:"\<And>P Q. P \<and> Q \<Longrightarrow> P" "\<And>P Q. P \<and> Q \<Longrightarrow> Q" by auto
  1126   have "odd (card ?A)" apply(rule kuhn_combinatorial[of p n label]) using assms by auto
  1127   hence "card ?A \<noteq> 0" apply-apply(rule ccontr) by auto hence "?A \<noteq> {}" unfolding card_eq_0_iff by auto
  1128   then obtain s where "s\<in>?A" by auto note s=conjD[OF this[unfolded mem_Collect_eq]]
  1129   guess a b apply(rule ksimplex_extrema_strong[OF s(1) `n\<noteq>0`]) . note ab=this
  1130   show ?thesis apply(rule that[of a]) proof(rule_tac[!] ballI) fix i assume "i\<in>{1..n}"
  1131     hence "a i + 1 \<le> p" apply-apply(rule order_trans[of _ "b i"]) apply(subst ab(5)[THEN spec[where x=i]])
  1132       using s(1)[unfolded ksimplex_def] defer apply- apply(erule conjE)+ apply(drule_tac bspec[OF _ ab(2)])+ by auto
  1133     thus "a i < p" by auto
  1134     case goal2 hence "i \<in> reduced label n ` s" using s by auto then guess u unfolding image_iff .. note u=this
  1135     from goal2 have "i - 1 \<in> reduced label n ` s" using s by auto then guess v unfolding image_iff .. note v=this
  1136     show ?case apply(rule_tac x=u in exI, rule_tac x=v in exI) apply(rule conjI) defer apply(rule conjI) defer 2 proof(rule_tac[1-2] ballI)
  1137       show "label u i \<noteq> label v i" using reduced_labelling[of label n u] reduced_labelling[of label n v]
  1138         unfolding u(2)[THEN sym] v(2)[THEN sym] using goal2 by auto
  1139       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"
  1140         using conjD[OF ab(4)[rule_format, OF u(1)]] and conjD[OF ab(4)[rule_format, OF v(1)]] apply- 
  1141         apply(drule_tac[!] kle_imp_pointwise)+ apply(erule_tac[!] x=j in allE)+ unfolding ab(5)[rule_format] using j
  1142         by auto qed qed qed
  1143 
  1144 subsection {* The main result for the unit cube. *}
  1145 
  1146 lemma kuhn_labelling_lemma':
  1147   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)"
  1148   shows "\<exists>l. (\<forall>x i. l x i \<le> (1::nat)) \<and>
  1149              (\<forall>x i. P x \<and> Q i \<and> (x i = 0) \<longrightarrow> (l x i = 0)) \<and>
  1150              (\<forall>x i. P x \<and> Q i \<and> (x i = 1) \<longrightarrow> (l x i = 1)) \<and>
  1151              (\<forall>x i. P x \<and> Q i \<and> (l x i = 0) \<longrightarrow> x i \<le> f(x) i) \<and>
  1152              (\<forall>x i. P x \<and> Q i \<and> (l x i = 1) \<longrightarrow> f(x) i \<le> x i)" proof-
  1153   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
  1154   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
  1155   show ?thesis unfolding and_forall_thm apply(subst choice_iff[THEN sym])+ proof(rule,rule) case goal1
  1156     let ?R = "\<lambda>y. (P x \<and> Q xa \<and> x xa = 0 \<longrightarrow> y = (0::nat)) \<and>
  1157         (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)"
  1158     { 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]
  1159         apply(drule_tac assms(1)[rule_format]) by auto }
  1160     hence "?R 0 \<or> ?R 1" by auto thus ?case by auto qed qed 
  1161 
  1162 lemma brouwer_cube: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'a::ordered_euclidean_space"
  1163   assumes "continuous_on {0..\<chi>\<chi> i. 1} f" "f ` {0..\<chi>\<chi> i. 1} \<subseteq> {0..\<chi>\<chi> i. 1}"
  1164   shows "\<exists>x\<in>{0..\<chi>\<chi> i. 1}. f x = x" apply(rule ccontr) proof-
  1165   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)
  1166   assume "\<not> (\<exists>x\<in>{0..\<chi>\<chi> i. 1}. f x = x)" hence *:"\<not> (\<exists>x\<in>{0..\<chi>\<chi> i. 1}. f x - x = 0)" by auto
  1167   guess d apply(rule brouwer_compactness_lemma[OF compact_interval _ *]) 
  1168     apply(rule continuous_on_intros assms)+ . note d=this[rule_format]
  1169   have *:"\<forall>x. x \<in> {0..\<chi>\<chi> i. 1} \<longrightarrow> f x \<in> {0..\<chi>\<chi> i. 1}"  "\<forall>x. x \<in> {0..(\<chi>\<chi> i. 1)::'a} \<longrightarrow>
  1170     (\<forall>i<DIM('a). True \<longrightarrow> 0 \<le> x $$ i \<and> x $$ i \<le> 1)"
  1171     using assms(2)[unfolded image_subset_iff Ball_def] unfolding mem_interval by auto
  1172   guess label using kuhn_labelling_lemma[OF *] apply-apply(erule exE,(erule conjE)+) . note label = this[rule_format]
  1173   have lem1:"\<forall>x\<in>{0..\<chi>\<chi> i. 1}.\<forall>y\<in>{0..\<chi>\<chi> i. 1}.\<forall>i<DIM('a). label x i \<noteq> label y i
  1174             \<longrightarrow> abs(f x $$ i - x $$ i) \<le> norm(f y - f x) + norm(y - x)" proof safe
  1175     fix x y::'a assume xy:"x\<in>{0..\<chi>\<chi> i. 1}" "y\<in>{0..\<chi>\<chi> i. 1}" fix i assume i:"label x i \<noteq> label y i" "i<DIM('a)"
  1176     have *:"\<And>x y fx fy::real. (x \<le> fx \<and> fy \<le> y \<or> fx \<le> x \<and> y \<le> fy)
  1177              \<Longrightarrow> abs(fx - x) \<le> abs(fy - fx) + abs(y - x)" by auto
  1178     have "\<bar>(f x - x) $$ i\<bar> \<le> abs((f y - f x)$$i) + abs((y - x)$$i)" unfolding euclidean_simps
  1179       apply(rule *) apply(cases "label x i = 0") apply(rule disjI1,rule) prefer 3 proof(rule disjI2,rule)
  1180       assume lx:"label x i = 0" hence ly:"label y i = 1" using i label(1)[of i y] by auto
  1181       show "x $$ i \<le> f x $$ i" apply(rule label(4)[rule_format]) using xy lx i(2) by auto
  1182       show "f y $$ i \<le> y $$ i" apply(rule label(5)[rule_format]) using xy ly i(2) by auto next
  1183       assume "label x i \<noteq> 0" hence l:"label x i = 1" "label y i = 0"
  1184         using i label(1)[of i x] label(1)[of i y] by auto
  1185       show "f x $$ i \<le> x $$ i" apply(rule label(5)[rule_format]) using xy l i(2) by auto
  1186       show "y $$ i \<le> f y $$ i" apply(rule label(4)[rule_format]) using xy l i(2) by auto qed 
  1187     also have "\<dots> \<le> norm (f y - f x) + norm (y - x)" apply(rule add_mono) by(rule component_le_norm)+
  1188     finally show "\<bar>f x $$ i - x $$ i\<bar> \<le> norm (f y - f x) + norm (y - x)" unfolding euclidean_simps . qed
  1189   have "\<exists>e>0. \<forall>x\<in>{0..\<chi>\<chi> i. 1}. \<forall>y\<in>{0..\<chi>\<chi> i. 1}. \<forall>z\<in>{0..\<chi>\<chi> i. 1}. \<forall>i<DIM('a).
  1190     norm(x - z) < e \<and> norm(y - z) < e \<and> label x i \<noteq> label y i \<longrightarrow> abs((f(z) - z)$$i) < d / (real n)" proof-
  1191     have d':"d / real n / 8 > 0" apply(rule divide_pos_pos)+ using d(1) unfolding n_def by auto
  1192     have *:"uniformly_continuous_on {0..\<chi>\<chi> i. 1} f" by(rule compact_uniformly_continuous[OF assms(1) compact_interval])
  1193     guess e using *[unfolded uniformly_continuous_on_def,rule_format,OF d'] apply-apply(erule exE,(erule conjE)+) .
  1194     note e=this[rule_format,unfolded dist_norm]
  1195     show ?thesis apply(rule_tac x="min (e/2) (d/real n/8)" in exI)
  1196     proof safe show "0 < min (e / 2) (d / real n / 8)" using d' e by auto
  1197       fix x y z i assume as:"x \<in> {0..\<chi>\<chi> i. 1}" "y \<in> {0..\<chi>\<chi> i. 1}" "z \<in> {0..\<chi>\<chi> i. 1}"
  1198         "norm (x - z) < min (e / 2) (d / real n / 8)"
  1199         "norm (y - z) < min (e / 2) (d / real n / 8)" "label x i \<noteq> label y i" and i:"i<DIM('a)"
  1200       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>
  1201         n1 < d4 \<Longrightarrow> n2 < 2 * d4 \<Longrightarrow> n3 < d4 \<Longrightarrow> n4 < d4 \<Longrightarrow> (8 * d4 = d) \<Longrightarrow> abs(fz - z) < d" by auto
  1202       show "\<bar>(f z - z) $$ i\<bar> < d / real n" unfolding euclidean_simps proof(rule *)
  1203         show "\<bar>f x $$ i - x $$ i\<bar> \<le> norm (f y -f x) + norm (y - x)" apply(rule lem1[rule_format]) using as i  by auto
  1204         show "\<bar>f x $$ i - f z $$ i\<bar> \<le> norm (f x - f z)" "\<bar>x $$ i - z $$ i\<bar> \<le> norm (x - z)"
  1205           unfolding euclidean_component_diff[THEN sym] by(rule component_le_norm)+
  1206         have tria:"norm (y - x) \<le> norm (y - z) + norm (x - z)" using dist_triangle[of y x z,unfolded dist_norm]
  1207           unfolding norm_minus_commute by auto
  1208         also have "\<dots> < e / 2 + e / 2" apply(rule add_strict_mono) using as(4,5) by auto
  1209         finally show "norm (f y - f x) < d / real n / 8" apply- apply(rule e(2)) using as by auto
  1210         have "norm (y - z) + norm (x - z) < d / real n / 8 + d / real n / 8" apply(rule add_strict_mono) using as by auto
  1211         thus "norm (y - x) < 2 * (d / real n / 8)" using tria by auto
  1212         show "norm (f x - f z) < d / real n / 8" apply(rule e(2)) using as e(1) by auto qed(insert as, auto) qed qed
  1213   then guess e apply-apply(erule exE,(erule conjE)+) . note e=this[rule_format] 
  1214   guess p using real_arch_simple[of "1 + real n / e"] .. note p=this
  1215   have "1 + real n / e > 0" apply(rule add_pos_pos) defer apply(rule divide_pos_pos) using e(1) n by auto
  1216   hence "p > 0" using p by auto
  1217   def b \<equiv> "\<lambda>i. i - 1::nat" have b:"bij_betw b {1..n} {..<DIM('a)}"
  1218     unfolding bij_betw_def inj_on_def b_def n_def apply rule defer
  1219     apply safe defer unfolding image_iff apply(rule_tac x="Suc x" in bexI) by auto
  1220   def b' \<equiv> "inv_into {1..n} b"
  1221   have b':"bij_betw b' {..<DIM('a)} {1..n}" using bij_betw_inv_into[OF b] unfolding b'_def n_def by auto
  1222   have bb'[simp]:"\<And>i. i<DIM('a) \<Longrightarrow> b (b' i) = i" unfolding b'_def apply(rule f_inv_into_f) using b  
  1223     unfolding bij_betw_def by auto
  1224   have b'b[simp]:"\<And>i. i\<in>{1..n} \<Longrightarrow> b' (b i) = i" unfolding b'_def apply(rule inv_into_f_eq)
  1225     using b unfolding n_def bij_betw_def by auto
  1226   have *:"\<And>x::nat. x=0 \<or> x=1 \<longleftrightarrow> x\<le>1" by auto
  1227   have b'':"\<And>j. j\<in>{1..n} \<Longrightarrow> b j <DIM('a)" using b unfolding bij_betw_def by auto
  1228   have q1:"0 < p" "0 < n"  "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow>
  1229     (\<forall>i\<in>{1..n}. (label (\<chi>\<chi> i. real (x (b' i)) / real p) \<circ> b) i = 0 \<or> (label (\<chi>\<chi> i. real (x (b' i)) / real p) \<circ> b) i = 1)"
  1230     unfolding * using `p>0` `n>0` using label(1)[OF b'']  by auto
  1231   have q2:"\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. x i = 0 \<longrightarrow> (label (\<chi>\<chi> i. real (x (b' i)) / real p) \<circ> b) i = 0)"
  1232     "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. x i = p \<longrightarrow> (label (\<chi>\<chi> i. real (x (b' i)) / real p) \<circ> b) i = 1)"
  1233     apply(rule,rule,rule,rule) defer proof(rule,rule,rule,rule) fix x i 
  1234     assume as:"\<forall>i\<in>{1..n}. x i \<le> p" "i \<in> {1..n}"
  1235     { assume "x i = p \<or> x i = 0" 
  1236       have "(\<chi>\<chi> i. real (x (b' i)) / real p) \<in> {0::'a..\<chi>\<chi> i. 1}" unfolding mem_interval 
  1237         apply safe unfolding euclidean_lambda_beta euclidean_component_zero
  1238       proof (simp_all only: if_P) fix j assume j':"j<DIM('a)"
  1239         hence j:"b' j \<in> {1..n}" using b' unfolding n_def bij_betw_def by auto
  1240         show "0 \<le> real (x (b' j)) / real p"
  1241           apply(rule divide_nonneg_pos) using `p>0` using as(1)[rule_format,OF j] by auto
  1242         show "real (x (b' j)) / real p \<le> 1" unfolding divide_le_eq_1
  1243           using as(1)[rule_format,OF j] by auto qed } note cube=this
  1244     { assume "x i = p" thus "(label (\<chi>\<chi> i. real (x (b' i)) / real p) \<circ> b) i = 1" unfolding o_def
  1245         apply- apply(rule label(3)) apply(rule b'') using cube using as `p>0`
  1246       proof safe assume i:"i\<in>{1..n}"
  1247         show "((\<chi>\<chi> ia. real (x (b' ia)) / real (x i))::'a) $$ b i = 1"
  1248           unfolding euclidean_lambda_beta apply(subst if_P) apply(rule b''[OF i]) unfolding b'b[OF i] 
  1249           unfolding  `x i = p` using q1(1) by auto
  1250       qed auto }
  1251     { assume "x i = 0" thus "(label (\<chi>\<chi> i. real (x (b' i)) / real p) \<circ> b) i = 0" unfolding o_def
  1252         apply-apply(rule label(2)[OF b'']) using cube using as `p>0`
  1253       proof safe assume i:"i\<in>{1..n}"
  1254         show "((\<chi>\<chi> ia. real (x (b' ia)) / real p)::'a) $$ b i = 0"
  1255           unfolding euclidean_lambda_beta apply (subst if_P) apply(rule b''[OF i]) unfolding b'b[OF i] 
  1256           unfolding `x i = 0` using q1(1) by auto 
  1257       qed auto }
  1258   qed
  1259   guess q apply(rule kuhn_lemma[OF q1 q2]) . note q=this
  1260   def z \<equiv> "(\<chi>\<chi> i. real (q (b' i)) / real p)::'a"
  1261   have "\<exists>i<DIM('a). d / real n \<le> abs((f z - z)$$i)" proof(rule ccontr)
  1262     have "\<forall>i<DIM('a). q (b' i) \<in> {0..<p}" using q(1) b'[unfolded bij_betw_def] by auto 
  1263     hence "\<forall>i<DIM('a). q (b' i) \<in> {0..p}" apply-apply(rule,erule_tac x=i in allE) by auto
  1264     hence "z\<in>{0..\<chi>\<chi> i.1}" unfolding z_def mem_interval apply safe unfolding euclidean_lambda_beta
  1265       unfolding euclidean_component_zero apply (simp_all only: if_P)
  1266       apply(rule divide_nonneg_pos) using `p>0` unfolding divide_le_eq_1 by auto
  1267     hence d_fz_z:"d \<le> norm (f z - z)" apply(drule_tac d) .
  1268     case goal1 hence as:"\<forall>i<DIM('a). \<bar>f z $$ i - z $$ i\<bar> < d / real n" using `n>0` by(auto simp add:not_le)
  1269     have "norm (f z - z) \<le> (\<Sum>i<DIM('a). \<bar>f z $$ i - z $$ i\<bar>)" unfolding euclidean_component_diff[THEN sym] by(rule norm_le_l1)
  1270     also have "\<dots> < (\<Sum>i<DIM('a). d / real n)" apply(rule setsum_strict_mono) using as by auto
  1271     also have "\<dots> = d" unfolding real_eq_of_nat n_def using n using DIM_positive[where 'a='a] by auto
  1272     finally show False using d_fz_z by auto qed then guess i .. note i=this
  1273   have *:"b' i \<in> {1..n}" using i using b'[unfolded bij_betw_def] by auto
  1274   guess r using q(2)[rule_format,OF *] .. then guess s apply-apply(erule exE,(erule conjE)+) . note rs=this[rule_format]
  1275   have b'_im:"\<And>i. i<DIM('a) \<Longrightarrow>  b' i \<in> {1..n}" using b' unfolding bij_betw_def by auto
  1276   def r' \<equiv> "(\<chi>\<chi> i. real (r (b' i)) / real p)::'a"
  1277   have "\<And>i. i<DIM('a) \<Longrightarrow> r (b' i) \<le> p" apply(rule order_trans) apply(rule rs(1)[OF b'_im,THEN conjunct2])
  1278     using q(1)[rule_format,OF b'_im] by(auto simp add: Suc_le_eq)
  1279   hence "r' \<in> {0..\<chi>\<chi> i. 1}"  unfolding r'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component_zero
  1280     apply (simp only: if_P)
  1281     apply(rule divide_nonneg_pos) using rs(1)[OF b'_im] q(1)[rule_format,OF b'_im] `p>0` by auto
  1282   def s' \<equiv> "(\<chi>\<chi> i. real (s (b' i)) / real p)::'a"
  1283   have "\<And>i. i<DIM('a) \<Longrightarrow> s (b' i) \<le> p" apply(rule order_trans) apply(rule rs(2)[OF b'_im,THEN conjunct2])
  1284     using q(1)[rule_format,OF b'_im] by(auto simp add: Suc_le_eq)
  1285   hence "s' \<in> {0..\<chi>\<chi> i.1}" unfolding s'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component_zero
  1286     apply (simp_all only: if_P) apply(rule divide_nonneg_pos) using rs(1)[OF b'_im] q(1)[rule_format,OF b'_im] `p>0` by auto
  1287   have "z\<in>{0..\<chi>\<chi> i.1}" unfolding z_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component_zero
  1288     apply (simp_all only: if_P) apply(rule divide_nonneg_pos) using q(1)[rule_format,OF b'_im] `p>0` by(auto intro:less_imp_le)
  1289   have *:"\<And>x. 1 + real x = real (Suc x)" by auto
  1290   { have "(\<Sum>i<DIM('a). \<bar>real (r (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>i<DIM('a). 1)" 
  1291       apply(rule setsum_mono) using rs(1)[OF b'_im] by(auto simp add:* field_simps)
  1292     also have "\<dots> < e * real p" using p `e>0` `p>0` unfolding n_def real_of_nat_def
  1293       by(auto simp add:field_simps)
  1294     finally have "(\<Sum>i<DIM('a). \<bar>real (r (b' i)) - real (q (b' i))\<bar>) < e * real p" . } moreover
  1295   { have "(\<Sum>i<DIM('a). \<bar>real (s (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>i<DIM('a). 1)" 
  1296       apply(rule setsum_mono) using rs(2)[OF b'_im] by(auto simp add:* field_simps)
  1297     also have "\<dots> < e * real p" using p `e>0` `p>0` unfolding n_def real_of_nat_def
  1298       by(auto simp add:field_simps)
  1299     finally have "(\<Sum>i<DIM('a). \<bar>real (s (b' i)) - real (q (b' i))\<bar>) < e * real p" . } ultimately
  1300   have "norm (r' - z) < e" "norm (s' - z) < e" unfolding r'_def s'_def z_def apply-
  1301     apply(rule_tac[!] le_less_trans[OF norm_le_l1]) using `p>0`
  1302     by(auto simp add:field_simps setsum_divide_distrib[THEN sym])
  1303   hence "\<bar>(f z - z) $$ i\<bar> < d / real n" apply-apply(rule e(2)[OF `r'\<in>{0..\<chi>\<chi> i.1}` `s'\<in>{0..\<chi>\<chi> i.1}` `z\<in>{0..\<chi>\<chi> i.1}`])
  1304     using rs(3) unfolding r'_def[symmetric] s'_def[symmetric] o_def bb' using i by auto
  1305   thus False using i by auto qed
  1306 
  1307 subsection {* Retractions. *}
  1308 
  1309 definition "retraction s t r \<longleftrightarrow>
  1310   t \<subseteq> s \<and> continuous_on s r \<and> (r ` s \<subseteq> t) \<and> (\<forall>x\<in>t. r x = x)"
  1311 
  1312 definition retract_of (infixl "retract'_of" 12) where
  1313   "(t retract_of s) \<longleftrightarrow> (\<exists>r. retraction s t r)"
  1314 
  1315 lemma retraction_idempotent: "retraction s t r \<Longrightarrow> x \<in> s \<Longrightarrow>  r(r x) = r x"
  1316   unfolding retraction_def by auto
  1317 
  1318 subsection {*preservation of fixpoints under (more general notion of) retraction. *}
  1319 
  1320 lemma invertible_fixpoint_property: fixes s::"('a::euclidean_space) set" and t::"('b::euclidean_space) set" 
  1321   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"
  1322   "\<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"
  1323   obtains y where "y\<in>t" "g y = y" proof-
  1324   have "\<exists>x\<in>s. (i \<circ> g \<circ> r) x = x" apply(rule assms(6)[rule_format],rule)
  1325     apply(rule continuous_on_compose assms)+ apply((rule continuous_on_subset)?,rule assms)+
  1326     using assms(2,4,8) unfolding image_compose by(auto,blast)
  1327     then guess x .. note x = this hence *:"g (r x) \<in> t" using assms(4,8) by auto
  1328     have "r ((i \<circ> g \<circ> r) x) = r x" using x by auto
  1329     thus ?thesis apply(rule_tac that[of "r x"]) using x unfolding o_def
  1330       unfolding assms(5)[rule_format,OF *] using assms(4) by auto qed
  1331 
  1332 lemma homeomorphic_fixpoint_property:
  1333   fixes s::"('a::euclidean_space) set" and t::"('b::euclidean_space) set" assumes "s homeomorphic t"
  1334   shows "(\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)) \<longleftrightarrow>
  1335          (\<forall>g. continuous_on t g \<and> g ` t \<subseteq> t \<longrightarrow> (\<exists>y\<in>t. g y = y))" proof-
  1336   guess r using assms[unfolded homeomorphic_def homeomorphism_def] .. then guess i ..
  1337   thus ?thesis apply- apply rule apply(rule_tac[!] allI impI)+ 
  1338     apply(rule_tac g=g in invertible_fixpoint_property[of t i s r]) prefer 10
  1339     apply(rule_tac g=f in invertible_fixpoint_property[of s r t i]) by auto qed
  1340 
  1341 lemma retract_fixpoint_property: fixes f::"'a::euclidean_space => 'b::euclidean_space" and s::"'a set"
  1342   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"
  1343   obtains y where "y \<in> t" "g y = y" proof- guess h using assms(1) unfolding retract_of_def .. 
  1344   thus ?thesis unfolding retraction_def apply-
  1345     apply(rule invertible_fixpoint_property[OF continuous_on_id _ _ _ _ assms(2), of t h g]) prefer 7
  1346     apply(rule_tac y=y in that) using assms by auto qed
  1347 
  1348 subsection {*So the Brouwer theorem for any set with nonempty interior. *}
  1349 
  1350 lemma brouwer_weak: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'a::ordered_euclidean_space"
  1351   assumes "compact s" "convex s" "interior s \<noteq> {}" "continuous_on s f" "f ` s \<subseteq> s"
  1352   obtains x where "x \<in> s" "f x = x" proof-
  1353   have *:"interior {0::'a..\<chi>\<chi> i.1} \<noteq> {}" unfolding interior_closed_interval interval_eq_empty by auto
  1354   have *:"{0::'a..\<chi>\<chi> i.1} homeomorphic s" using homeomorphic_convex_compact[OF convex_interval(1) compact_interval * assms(2,1,3)] .
  1355   have "\<forall>f. continuous_on {0::'a..\<chi>\<chi> i.1} f \<and> f ` {0::'a..\<chi>\<chi> i.1} \<subseteq> {0::'a..\<chi>\<chi> i.1} \<longrightarrow> (\<exists>x\<in>{0::'a..\<chi>\<chi> i.1}. f x = x)"
  1356     using brouwer_cube by auto
  1357   thus ?thesis unfolding homeomorphic_fixpoint_property[OF *] apply(erule_tac x=f in allE)
  1358     apply(erule impE) defer apply(erule bexE) apply(rule_tac x=y in that) using assms by auto qed
  1359 
  1360 subsection {* And in particular for a closed ball. *}
  1361 
  1362 lemma brouwer_ball: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'a"
  1363   assumes "0 < e" "continuous_on (cball a e) f" "f ` (cball a e) \<subseteq> (cball a e)"
  1364   obtains x where "x \<in> cball a e" "f x = x"
  1365   using brouwer_weak[OF compact_cball convex_cball,of a e f] unfolding interior_cball ball_eq_empty
  1366   using assms by auto
  1367 
  1368 text {*Still more general form; could derive this directly without using the 
  1369   rather involved @{text "HOMEOMORPHIC_CONVEX_COMPACT"} theorem, just using
  1370   a scaling and translation to put the set inside the unit cube. *}
  1371 
  1372 lemma brouwer: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'a"
  1373   assumes "compact s" "convex s" "s \<noteq> {}" "continuous_on s f" "f ` s \<subseteq> s"
  1374   obtains x where "x \<in> s" "f x = x" proof-
  1375   have "\<exists>e>0. s \<subseteq> cball 0 e" using compact_imp_bounded[OF assms(1)] unfolding bounded_pos
  1376     apply(erule_tac exE,rule_tac x=b in exI) by(auto simp add: dist_norm) 
  1377   then guess e apply-apply(erule exE,(erule conjE)+) . note e=this
  1378   have "\<exists>x\<in> cball 0 e. (f \<circ> closest_point s) x = x"
  1379     apply(rule_tac brouwer_ball[OF e(1), of 0 "f \<circ> closest_point s"]) apply(rule continuous_on_compose )
  1380     apply(rule continuous_on_closest_point[OF assms(2) compact_imp_closed[OF assms(1)] assms(3)])
  1381     apply(rule continuous_on_subset[OF assms(4)])
  1382     using closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3)] apply - defer
  1383     using assms(5)[unfolded subset_eq] using e(2)[unfolded subset_eq mem_cball] by(auto simp add: dist_norm)
  1384   then guess x .. note x=this
  1385   have *:"closest_point s x = x" apply(rule closest_point_self) 
  1386     apply(rule assms(5)[unfolded subset_eq,THEN bspec[where x="x"],unfolded image_iff])
  1387     apply(rule_tac x="closest_point s x" in bexI) using x unfolding o_def
  1388     using closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3), of x] by auto
  1389   show thesis apply(rule_tac x="closest_point s x" in that) unfolding x(2)[unfolded o_def]
  1390     apply(rule closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3)]) using * by auto qed
  1391 
  1392 text {*So we get the no-retraction theorem. *}
  1393 
  1394 lemma no_retraction_cball: assumes "0 < e" fixes type::"'a::ordered_euclidean_space"
  1395   shows "\<not> (frontier(cball a e) retract_of (cball (a::'a) e))" proof case goal1
  1396   have *:"\<And>xa. a - (2 *\<^sub>R a - xa) = -(a - xa)" using scaleR_left_distrib[of 1 1 a] by auto
  1397   guess x apply(rule retract_fixpoint_property[OF goal1, of "\<lambda>x. scaleR 2 a - x"])
  1398     apply(rule,rule,erule conjE) apply(rule brouwer_ball[OF assms]) apply assumption+
  1399     apply(rule_tac x=x in bexI) apply assumption+ apply(rule continuous_on_intros)+
  1400     unfolding frontier_cball subset_eq Ball_def image_iff apply(rule,rule,erule bexE)
  1401     unfolding dist_norm apply(simp add: * norm_minus_commute) . note x = this
  1402   hence "scaleR 2 a = scaleR 1 x + scaleR 1 x" by(auto simp add:algebra_simps)
  1403   hence "a = x" unfolding scaleR_left_distrib[THEN sym] by auto 
  1404   thus False using x using assms by auto qed
  1405 
  1406 subsection {*Bijections between intervals. *}
  1407 
  1408 definition "interval_bij = (\<lambda> (a::'a,b::'a) (u::'a,v::'a) (x::'a::ordered_euclidean_space).
  1409     (\<chi>\<chi> i. u$$i + (x$$i - a$$i) / (b$$i - a$$i) * (v$$i - u$$i))::'a)"
  1410 
  1411 lemma interval_bij_affine:
  1412  "interval_bij (a,b) (u,v) = (\<lambda>x. (\<chi>\<chi> i. (v$$i - u$$i) / (b$$i - a$$i) * x$$i) +
  1413             (\<chi>\<chi> i. u$$i - (v$$i - u$$i) / (b$$i - a$$i) * a$$i))"
  1414   apply rule apply(subst euclidean_eq,safe) unfolding euclidean_simps interval_bij_def euclidean_lambda_beta
  1415   by(auto simp add: field_simps add_divide_distrib[THEN sym])
  1416 
  1417 lemma continuous_interval_bij:
  1418   "continuous (at x) (interval_bij (a,b::'a::ordered_euclidean_space) (u,v::'a))" 
  1419   unfolding interval_bij_affine apply(rule continuous_intros)
  1420     apply(rule linear_continuous_at) unfolding linear_conv_bounded_linear[THEN sym]
  1421     unfolding linear_def euclidean_eq[where 'a='a] apply safe unfolding euclidean_lambda_beta prefer 3
  1422     apply(rule continuous_intros) by(auto simp add:field_simps add_divide_distrib[THEN sym])
  1423 
  1424 lemma continuous_on_interval_bij: "continuous_on s (interval_bij (a,b) (u,v))"
  1425   apply(rule continuous_at_imp_continuous_on) by(rule, rule continuous_interval_bij)
  1426 
  1427 (** move this **)
  1428 lemma divide_nonneg_nonneg:assumes "a \<ge> 0" "b \<ge> 0" shows "0 \<le> a / (b::real)"
  1429   apply(cases "b=0") defer apply(rule divide_nonneg_pos) using assms by auto
  1430 
  1431 lemma in_interval_interval_bij: assumes "x \<in> {a..b}" "{u..v} \<noteq> {}"
  1432   shows "interval_bij (a,b) (u,v) x \<in> {u..v::'a::ordered_euclidean_space}" 
  1433   unfolding interval_bij_def split_conv mem_interval apply safe unfolding euclidean_lambda_beta
  1434 proof (simp_all only: if_P)
  1435   fix i assume i:"i<DIM('a)" have "{a..b} \<noteq> {}" using assms by auto
  1436   hence *:"a$$i \<le> b$$i" "u$$i \<le> v$$i" using assms(2) unfolding interval_eq_empty not_ex apply-
  1437     apply(erule_tac[!] x=i in allE)+ by auto
  1438   have x:"a$$i\<le>x$$i" "x$$i\<le>b$$i" using assms(1)[unfolded mem_interval] using i by auto
  1439   have "0 \<le> (x $$ i - a $$ i) / (b $$ i - a $$ i) * (v $$ i - u $$ i)"
  1440     apply(rule mult_nonneg_nonneg) apply(rule divide_nonneg_nonneg)
  1441     using * x by(auto simp add:field_simps)
  1442   thus "u $$ i \<le> u $$ i + (x $$ i - a $$ i) / (b $$ i - a $$ i) * (v $$ i - u $$ i)" using * by auto
  1443   have "((x $$ i - a $$ i) / (b $$ i - a $$ i)) * (v $$ i - u $$ i) \<le> 1 * (v $$ i - u $$ i)"
  1444     apply(rule mult_right_mono) unfolding divide_le_eq_1 using * x by auto
  1445   thus "u $$ i + (x $$ i - a $$ i) / (b $$ i - a $$ i) * (v $$ i - u $$ i) \<le> v $$ i" using * by auto
  1446 qed
  1447 
  1448 lemma interval_bij_bij: fixes x::"'a::ordered_euclidean_space" assumes "\<forall>i. a$$i < b$$i \<and> u$$i < v$$i" 
  1449   shows "interval_bij (a,b) (u,v) (interval_bij (u,v) (a,b) x) = x"
  1450   unfolding interval_bij_def split_conv euclidean_eq[where 'a='a]
  1451   apply(rule,insert assms,erule_tac x=i in allE) by auto
  1452 
  1453 end