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