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