--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Mar 25 13:14:33 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Mar 25 14:20:58 2014 +0100
@@ -22,23 +22,77 @@
imports Convex_Euclidean_Space
begin
-(** move this **)
+lemma bij_betw_singleton_eq:
+ assumes f: "bij_betw f A B" and g: "bij_betw g A B" and a: "a \<in> A"
+ assumes eq: "(\<And>x. x \<in> A \<Longrightarrow> x \<noteq> a \<Longrightarrow> f x = g x)"
+ shows "f a = g a"
+proof -
+ have "f ` (A - {a}) = g ` (A - {a})"
+ by (intro image_cong) (simp_all add: eq)
+ then have "B - {f a} = B - {g a}"
+ using f g a by (auto simp: bij_betw_def inj_on_image_set_diff set_eq_iff)
+ moreover have "f a \<in> B" "g a \<in> B"
+ using f g a by (auto simp: bij_betw_def)
+ ultimately show ?thesis
+ by auto
+qed
+
+lemma swap_image:
+ "Fun.swap i j f ` A = (if i \<in> A then (if j \<in> A then f ` A else f ` ((A - {i}) \<union> {j}))
+ else (if j \<in> A then f ` ((A - {j}) \<union> {i}) else f ` A))"
+ apply (auto simp: Fun.swap_def image_iff)
+ apply metis
+ apply (metis member_remove remove_def)
+ apply (metis member_remove remove_def)
+ done
+
+lemma swap_apply1: "Fun.swap x y f x = f y"
+ by (simp add: swap_def)
+
+lemma swap_apply2: "Fun.swap x y f y = f x"
+ by (simp add: swap_def)
+
+lemma (in -) lessThan_empty_iff: "{..< n::nat} = {} \<longleftrightarrow> n = 0"
+ by auto
+
+lemma Zero_notin_Suc: "0 \<notin> Suc ` A"
+ by auto
+
+lemma atMost_Suc_eq_insert_0: "{.. Suc n} = insert 0 (Suc ` {.. n})"
+ apply auto
+ apply (case_tac x)
+ apply auto
+ done
+
lemma divide_nonneg_nonneg:
- fixes a b :: real
- assumes "a \<ge> 0"
- and "b \<ge> 0"
- shows "0 \<le> a / b"
-proof (cases "b = 0")
- case True
- then show ?thesis by auto
-next
- case False
- show ?thesis
- apply (rule divide_nonneg_pos)
- using assms False
- apply auto
- done
-qed
+ fixes a b :: "'a :: {linordered_field, field_inverse_zero}"
+ shows "a \<ge> 0 \<Longrightarrow> b \<ge> 0 \<Longrightarrow> 0 \<le> a / b"
+ by (cases "b = 0") (auto intro!: divide_nonneg_pos)
+
+lemma setsum_Un_disjoint':
+ assumes "finite A"
+ and "finite B"
+ and "A \<inter> B = {}"
+ and "A \<union> B = C"
+ shows "setsum g C = setsum g A + setsum g B"
+ using setsum_Un_disjoint[OF assms(1-3)] and assms(4) by auto
+
+lemma pointwise_minimal_pointwise_maximal:
+ fixes s :: "(nat \<Rightarrow> nat) set"
+ assumes "finite s"
+ and "s \<noteq> {}"
+ and "\<forall>x\<in>s. \<forall>y\<in>s. x \<le> y \<or> y \<le> x"
+ shows "\<exists>a\<in>s. \<forall>x\<in>s. a \<le> x"
+ and "\<exists>a\<in>s. \<forall>x\<in>s. x \<le> a"
+ using assms
+proof (induct s rule: finite_ne_induct)
+ case (insert b s)
+ assume *: "\<forall>x\<in>insert b s. \<forall>y\<in>insert b s. x \<le> y \<or> y \<le> x"
+ moreover then obtain u l where "l \<in> s" "\<forall>b\<in>s. l \<le> b" "u \<in> s" "\<forall>b\<in>s. b \<le> u"
+ using insert by auto
+ ultimately show "\<exists>a\<in>insert b s. \<forall>x\<in>insert b s. a \<le> x" "\<exists>a\<in>insert b s. \<forall>x\<in>insert b s. x \<le> a"
+ using *[rule_format, of b u] *[rule_format, of b l] by (metis insert_iff order.trans)+
+qed auto
lemma brouwer_compactness_lemma:
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
@@ -67,3649 +121,1261 @@
lemma kuhn_labelling_lemma:
fixes P Q :: "'a::euclidean_space \<Rightarrow> bool"
- assumes "(\<forall>x. P x \<longrightarrow> P (f x))"
+ assumes "\<forall>x. P x \<longrightarrow> P (f x)"
and "\<forall>x. P x \<longrightarrow> (\<forall>i\<in>Basis. Q i \<longrightarrow> 0 \<le> x\<bullet>i \<and> x\<bullet>i \<le> 1)"
shows "\<exists>l. (\<forall>x.\<forall>i\<in>Basis. l x i \<le> (1::nat)) \<and>
(\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (x\<bullet>i = 0) \<longrightarrow> (l x i = 0)) \<and>
(\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (x\<bullet>i = 1) \<longrightarrow> (l x i = 1)) \<and>
- (\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (l x i = 0) \<longrightarrow> x\<bullet>i \<le> f(x)\<bullet>i) \<and>
- (\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (l x i = 1) \<longrightarrow> f(x)\<bullet>i \<le> x\<bullet>i)"
+ (\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (l x i = 0) \<longrightarrow> x\<bullet>i \<le> f x\<bullet>i) \<and>
+ (\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (l x i = 1) \<longrightarrow> f x\<bullet>i \<le> x\<bullet>i)"
proof -
- have and_forall_thm:"\<And>P Q. (\<forall>x. P x) \<and> (\<forall>x. Q x) \<longleftrightarrow> (\<forall>x. P x \<and> Q x)"
- by auto
- have *: "\<forall>x y::real. 0 \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1 \<longrightarrow> (x \<noteq> 1 \<and> x \<le> y \<or> x \<noteq> 0 \<and> y \<le> x)"
- by auto
- show ?thesis
- unfolding and_forall_thm Ball_def
- apply (subst choice_iff[symmetric])+
- apply rule
- apply rule
- proof -
- case (goal1 x)
- let ?R = "\<lambda>y. (P x \<and> Q xa \<and> x \<bullet> xa = 0 \<longrightarrow> y = (0::nat)) \<and>
- (P x \<and> Q xa \<and> x \<bullet> xa = 1 \<longrightarrow> y = 1) \<and>
- (P x \<and> Q xa \<and> y = 0 \<longrightarrow> x \<bullet> xa \<le> f x \<bullet> xa) \<and>
- (P x \<and> Q xa \<and> y = 1 \<longrightarrow> f x \<bullet> xa \<le> x \<bullet> xa)"
- {
- assume "P x" "Q xa" "xa \<in> Basis"
- then have "0 \<le> f x \<bullet> xa \<and> f x \<bullet> xa \<le> 1"
- using assms(2)[rule_format,of "f x" xa]
- apply (drule_tac assms(1)[rule_format])
- apply auto
- done
- }
- then have "xa \<in> Basis \<Longrightarrow> ?R 0 \<or> ?R 1" by auto
- then show ?case by auto
- qed
+ { fix x i
+ let ?R = "\<lambda>y. (P x \<and> Q i \<and> x \<bullet> i = 0 \<longrightarrow> y = (0::nat)) \<and>
+ (P x \<and> Q i \<and> x \<bullet> i = 1 \<longrightarrow> y = 1) \<and>
+ (P x \<and> Q i \<and> y = 0 \<longrightarrow> x \<bullet> i \<le> f x \<bullet> i) \<and>
+ (P x \<and> Q i \<and> y = 1 \<longrightarrow> f x \<bullet> i \<le> x \<bullet> i)"
+ { assume "P x" "Q i" "i \<in> Basis" with assms have "0 \<le> f x \<bullet> i \<and> f x \<bullet> i \<le> 1" by auto }
+ then have "i \<in> Basis \<Longrightarrow> ?R 0 \<or> ?R 1" by auto }
+ then show ?thesis
+ unfolding all_conj_distrib[symmetric] Ball_def (* FIXME: shouldn't this work by metis? *)
+ by (subst choice_iff[symmetric])+ blast
qed
subsection {* The key "counting" observation, somewhat abstracted. *}
-lemma setsum_Un_disjoint':
- assumes "finite A"
- and "finite B"
- and "A \<inter> B = {}"
- and "A \<union> B = C"
- shows "setsum g C = setsum g A + setsum g B"
- using setsum_Un_disjoint[OF assms(1-3)] and assms(4) by auto
-
lemma kuhn_counting_lemma:
- assumes "finite faces"
- and "finite simplices"
- and "\<forall>f\<in>faces. bnd f \<longrightarrow> (card {s \<in> simplices. face f s} = 1)"
- and "\<forall>f\<in>faces. \<not> bnd f \<longrightarrow> (card {s \<in> simplices. face f s} = 2)"
- and "\<forall>s\<in>simplices. compo s \<longrightarrow> (card {f \<in> faces. face f s \<and> compo' f} = 1)"
- and "\<forall>s\<in>simplices. \<not> compo s \<longrightarrow>
- (card {f \<in> faces. face f s \<and> compo' f} = 0) \<or> (card {f \<in> faces. face f s \<and> compo' f} = 2)"
- and "odd(card {f \<in> faces. compo' f \<and> bnd f})"
- shows "odd(card {s \<in> simplices. compo s})"
-proof -
- have "\<And>x. {f\<in>faces. compo' f \<and> bnd f \<and> face f x} \<union> {f\<in>faces. compo' f \<and> \<not>bnd f \<and> face f x} =
- {f\<in>faces. compo' f \<and> face f x}"
- "\<And>x. {f \<in> faces. compo' f \<and> bnd f \<and> face f x} \<inter> {f \<in> faces. compo' f \<and> \<not> bnd f \<and> face f x} = {}"
- by auto
- then have lem1: "setsum (\<lambda>s. (card {f \<in> faces. face f s \<and> compo' f})) simplices =
- setsum (\<lambda>s. card {f \<in> {f \<in> faces. compo' f \<and> bnd f}. face f s}) simplices +
- setsum (\<lambda>s. card {f \<in> {f \<in> faces. compo' f \<and> \<not> (bnd f)}. face f s}) simplices"
- unfolding setsum_addf[symmetric]
- apply -
- apply (rule setsum_cong2)
- using assms(1)
- apply (auto simp add: card_Un_Int, auto simp add:conj_commute)
- done
- have lem2:
- "setsum (\<lambda>j. card {f \<in> {f \<in> faces. compo' f \<and> bnd f}. face f j}) simplices =
- 1 * card {f \<in> faces. compo' f \<and> bnd f}"
- "setsum (\<lambda>j. card {f \<in> {f \<in> faces. compo' f \<and> \<not> bnd f}. face f j}) simplices =
- 2 * card {f \<in> faces. compo' f \<and> \<not> bnd f}"
- apply (rule_tac[!] setsum_multicount)
- using assms
- apply auto
- done
- have lem3:
- "setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) simplices =
- setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices. compo s}+
- setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices. \<not> compo s}"
- apply (rule setsum_Un_disjoint')
- using assms(2)
- apply auto
- done
- have lem4: "setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices. compo s} =
- setsum (\<lambda>s. 1) {s \<in> simplices. compo s}"
- apply (rule setsum_cong2)
- using assms(5)
- apply auto
- done
- have lem5: "setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices. \<not> compo s} =
- setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f})
- {s \<in> simplices. (\<not> compo s) \<and> (card {f \<in> faces. face f s \<and> compo' f} = 0)} +
- setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f})
- {s \<in> simplices. (\<not> compo s) \<and> (card {f \<in> faces. face f s \<and> compo' f} = 2)}"
- apply (rule setsum_Un_disjoint')
- using assms(2,6)
- apply auto
- done
- have *: "int (\<Sum>s\<in>{s \<in> simplices. compo s}. card {f \<in> faces. face f s \<and> compo' f}) =
- int (card {f \<in> faces. compo' f \<and> bnd f} + 2 * card {f \<in> faces. compo' f \<and> \<not> bnd f}) -
- int (card {s \<in> simplices. \<not> compo s \<and> card {f \<in> faces. face f s \<and> compo' f} = 2} * 2)"
- using lem1[unfolded lem3 lem2 lem5] by auto
- have even_minus_odd:"\<And>x y. even x \<Longrightarrow> odd (y::int) \<Longrightarrow> odd (x - y)"
- using assms by auto
- have odd_minus_even:"\<And>x y. odd x \<Longrightarrow> even (y::int) \<Longrightarrow> odd (x - y)"
- using assms by auto
- show ?thesis
- unfolding even_nat_def card_eq_setsum and lem4[symmetric] and *[unfolded card_eq_setsum]
- unfolding card_eq_setsum[symmetric]
- apply (rule odd_minus_even)
- unfolding of_nat_add
- apply(rule odd_plus_even)
- apply(rule assms(7)[unfolded even_nat_def])
- unfolding int_mult
- apply auto
- done
-qed
-
-
-subsection {* The odd/even result for faces of complete vertices, generalized. *}
-
-lemma card_1_exists: "card s = 1 \<longleftrightarrow> (\<exists>!x. x \<in> s)"
- unfolding One_nat_def
- apply rule
- apply (drule card_eq_SucD)
- defer
- apply (erule ex1E)
-proof -
- fix x
- assume as: "x \<in> s" "\<forall>y. y \<in> s \<longrightarrow> y = x"
- have *: "s = insert x {}"
- apply (rule set_eqI, rule) unfolding singleton_iff
- apply (rule as(2)[rule_format]) using as(1)
- apply auto
- done
- show "card s = Suc 0"
- unfolding * using card_insert by auto
-qed auto
-
-lemma card_2_exists: "card s = 2 \<longleftrightarrow> (\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y))"
-proof
- assume "card s = 2"
- then obtain x y where s: "s = {x, y}" "x \<noteq> y"
- unfolding numeral_2_eq_2
- apply -
- apply (erule exE conjE | drule card_eq_SucD)+
- apply auto
- done
- show "\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y)"
- using s by auto
-next
- assume "\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y)"
- then obtain x y where "x \<in> s" "y \<in> s" "x \<noteq> y" "\<forall>z\<in>s. z = x \<or> z = y"
- by auto
- then have "s = {x, y}"
- by auto
- with `x \<noteq> y` show "card s = 2"
- by auto
-qed
-
-lemma image_lemma_0:
- assumes "card {a\<in>s. f ` (s - {a}) = t - {b}} = n"
- shows "card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> (f ` s' = t - {b})} = n"
-proof -
- have *: "{s'. \<exists>a\<in>s. (s' = s - {a}) \<and> (f ` s' = t - {b})} =
- (\<lambda>a. s - {a}) ` {a\<in>s. f ` (s - {a}) = t - {b}}"
- by auto
- show ?thesis
- unfolding *
- unfolding assms[symmetric]
- apply (rule card_image)
- unfolding inj_on_def
- apply (rule, rule, rule)
- unfolding mem_Collect_eq
- apply auto
- done
-qed
-
-lemma image_lemma_1:
- assumes "finite s"
- and "finite t"
- and "card s = card t"
- and "f ` s = t"
- and "b \<in> t"
- shows "card {s'. \<exists>a\<in>s. s' = s - {a} \<and> f ` s' = t - {b}} = 1"
-proof -
- obtain a where a: "b = f a" "a \<in> s"
- using assms(4-5) by auto
- have inj: "inj_on f s"
- apply (rule eq_card_imp_inj_on)
- using assms(1-4)
- apply auto
- done
- have *: "{a \<in> s. f ` (s - {a}) = t - {b}} = {a}"
- apply (rule set_eqI)
- unfolding singleton_iff
- apply (rule, rule inj[unfolded inj_on_def, rule_format])
- unfolding a
- using a(2) and assms and inj[unfolded inj_on_def]
- apply auto
- done
- show ?thesis
- apply (rule image_lemma_0)
- unfolding *
- apply auto
- done
-qed
-
-lemma image_lemma_2:
- assumes "finite s" "finite t" "card s = card t" "f ` s \<subseteq> t" "f ` s \<noteq> t" "b \<in> t"
- shows "card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> f ` s' = t - {b}} = 0 \<or>
- card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> f ` s' = t - {b}} = 2"
-proof (cases "{a\<in>s. f ` (s - {a}) = t - {b}} = {}")
- case True
- then show ?thesis
- apply -
- apply (rule disjI1, rule image_lemma_0)
- using assms(1)
- apply auto
- done
-next
- let ?M = "{a\<in>s. f ` (s - {a}) = t - {b}}"
- case False
- then obtain a where "a \<in> ?M"
- by auto
- then have a: "a \<in> s" "f ` (s - {a}) = t - {b}"
- by auto
- have "f a \<in> t - {b}"
- using a and assms by auto
- then have "\<exists>c \<in> s - {a}. f a = f c"
- unfolding image_iff[symmetric] and a
- by auto
- then obtain c where c: "c \<in> s" "a \<noteq> c" "f a = f c"
- by auto
- then have *: "f ` (s - {c}) = f ` (s - {a})"
- apply -
- apply (rule set_eqI)
- apply rule
- proof -
- fix x
- assume "x \<in> f ` (s - {a})"
- then obtain y where y: "f y = x" "y \<in> s - {a}"
- by auto
- then show "x \<in> f ` (s - {c})"
- unfolding image_iff
- apply (rule_tac x = "if y = c then a else y" in bexI)
- using c a
- apply auto
- done
- qed auto
- have "c \<in> ?M"
- unfolding mem_Collect_eq and *
- using a and c(1)
- by auto
- show ?thesis
- apply (rule disjI2)
- apply (rule image_lemma_0)
- unfolding card_2_exists
- apply (rule bexI[OF _ `a\<in>?M`])
- apply (rule bexI[OF _ `c\<in>?M`])
- apply rule
- apply (rule `a \<noteq> c`)
- apply rule
- apply (unfold mem_Collect_eq)
- apply (erule conjE)
- proof -
- fix z
- assume as: "z \<in> s" "f ` (s - {z}) = t - {b}"
- have inj: "inj_on f (s - {z})"
- apply (rule eq_card_imp_inj_on)
- unfolding as
- using as(1) and assms
- apply auto
- done
- show "z = a \<or> z = c"
- proof (rule ccontr)
- assume "\<not> ?thesis"
- then show False
- using inj[unfolded inj_on_def, THEN bspec[where x=a], THEN bspec[where x=c]]
- using `a \<in> s` `c \<in> s` `f a = f c` `a \<noteq> c`
- apply auto
- done
- qed
- qed
-qed
-
-
-subsection {* Combine this with the basic counting lemma. *}
-
-lemma kuhn_complete_lemma:
- assumes "finite simplices"
- and "\<forall>f s. face f s \<longleftrightarrow> (\<exists>a\<in>s. f = s - {a})"
- and "\<forall>s\<in>simplices. card s = n + 2"
- and "\<forall>s\<in>simplices. (rl ` s) \<subseteq> {0..n+1}"
- and "\<forall>f\<in>{f. \<exists>s\<in>simplices. face f s}. bnd f \<longrightarrow> card {s\<in>simplices. face f s} = 1"
- and "\<forall>f\<in>{f. \<exists>s\<in>simplices. face f s}. \<not> bnd f \<longrightarrow> card {s\<in>simplices. face f s} = 2"
- and "odd (card {f\<in>{f. \<exists>s\<in>simplices. face f s}. rl ` f = {0..n} \<and> bnd f})"
- shows "odd (card {s\<in>simplices. (rl ` s = {0..n+1})})"
- apply (rule kuhn_counting_lemma)
- defer
- apply (rule assms)+
- prefer 3
- apply (rule assms)
- apply (rule_tac[1-2] ballI impI)+
-proof -
- have *: "{f. \<exists>s\<in>simplices. \<exists>a\<in>s. f = s - {a}} = (\<Union>s\<in>simplices. {f. \<exists>a\<in>s. (f = s - {a})})"
- by auto
- have **: "\<forall>s\<in>simplices. card s = n + 2 \<and> finite s"
- using assms(3) by (auto intro: card_ge_0_finite)
- show "finite {f. \<exists>s\<in>simplices. face f s}"
- unfolding assms(2)[rule_format] and *
- apply (rule finite_UN_I[OF assms(1)])
- using **
- apply auto
- done
- have *: "\<And>P f s. s\<in>simplices \<Longrightarrow> (f \<in> {f. \<exists>s\<in>simplices. \<exists>a\<in>s. f = s - {a}}) \<and>
- (\<exists>a\<in>s. (f = s - {a})) \<and> P f \<longleftrightarrow> (\<exists>a\<in>s. (f = s - {a}) \<and> P f)"
- by auto
- fix s
- assume s: "s \<in> simplices"
- let ?S = "{f \<in> {f. \<exists>s\<in>simplices. face f s}. face f s \<and> rl ` f = {0..n}}"
- have "{0..n + 1} - {n + 1} = {0..n}"
- by auto
- then have S: "?S = {s'. \<exists>a\<in>s. s' = s - {a} \<and> rl ` s' = {0..n + 1} - {n + 1}}"
- apply -
- apply (rule set_eqI)
- unfolding assms(2)[rule_format] mem_Collect_eq
- unfolding *[OF s, unfolded mem_Collect_eq, where P="\<lambda>x. rl ` x = {0..n}"]
- apply auto
- done
- show "rl ` s = {0..n+1} \<Longrightarrow> card ?S = 1" and "rl ` s \<noteq> {0..n+1} \<Longrightarrow> card ?S = 0 \<or> card ?S = 2"
- unfolding S
- apply (rule_tac[!] image_lemma_1 image_lemma_2)
- using ** assms(4) and s
- apply auto
- done
-qed
-
-
-subsection {*We use the following notion of ordering rather than pointwise indexing. *}
-
-definition "kle n x y \<longleftrightarrow> (\<exists>k\<subseteq>{1..n::nat}. \<forall>j. y j = x j + (if j \<in> k then (1::nat) else 0))"
-
-lemma kle_refl [intro]: "kle n x x"
- unfolding kle_def by auto
-
-lemma kle_antisym: "kle n x y \<and> kle n y x \<longleftrightarrow> x = y"
- unfolding kle_def
- apply rule
- apply auto
- done
-
-lemma pointwise_minimal_pointwise_maximal:
- fixes s :: "(nat \<Rightarrow> nat) set"
- assumes "finite s"
- and "s \<noteq> {}"
- and "\<forall>x\<in>s. \<forall>y\<in>s. (\<forall>j. x j \<le> y j) \<or> (\<forall>j. y j \<le> x j)"
- shows "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. a j \<le> x j"
- and "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. x j \<le> a j"
- using assms
- unfolding atomize_conj
-proof (induct s rule: finite_induct)
- fix x
- fix F :: "(nat \<Rightarrow> nat) set"
- assume as: "finite F" "x \<notin> F"
- "\<lbrakk>F \<noteq> {}; \<forall>x\<in>F. \<forall>y\<in>F. (\<forall>j. x j \<le> y j) \<or> (\<forall>j. y j \<le> x j)\<rbrakk>
- \<Longrightarrow> (\<exists>a\<in>F. \<forall>x\<in>F. \<forall>j. a j \<le> x j) \<and> (\<exists>a\<in>F. \<forall>x\<in>F. \<forall>j. x j \<le> a j)" "insert x F \<noteq> {}"
- "\<forall>xa\<in>insert x F. \<forall>y\<in>insert x F. (\<forall>j. xa j \<le> y j) \<or> (\<forall>j. y j \<le> xa j)"
- show "(\<exists>a\<in>insert x F. \<forall>x\<in>insert x F. \<forall>j. a j \<le> x j) \<and> (\<exists>a\<in>insert x F. \<forall>x\<in>insert x F. \<forall>j. x j \<le> a j)"
- proof (cases "F = {}")
- case True
- then show ?thesis
- apply -
- apply (rule, rule_tac[!] x=x in bexI)
- apply auto
- done
- next
- case False
- obtain a b where a: "a\<in>insert x F" "\<forall>x\<in>F. \<forall>j. a j \<le> x j"
- and b: "b \<in> insert x F" "\<forall>x\<in>F. \<forall>j. x j \<le> b j"
- using as(3)[OF False] using as(5) by auto
- have "\<exists>a \<in> insert x F. \<forall>x \<in> insert x F. \<forall>j. a j \<le> x j"
- using as(5)[rule_format,OF a(1) insertI1]
- apply -
- proof (erule disjE)
- assume "\<forall>j. a j \<le> x j"
- then show ?thesis
- apply (rule_tac x=a in bexI)
- using a
- apply auto
- done
- next
- assume "\<forall>j. x j \<le> a j"
- then show ?thesis
- apply (rule_tac x=x in bexI)
- apply (rule, rule)
- apply (insert a)
- apply (erule_tac x=xa in ballE)
- apply (erule_tac x=j in allE)+
- apply auto
- done
- qed
- moreover
- have "\<exists>b\<in>insert x F. \<forall>x\<in>insert x F. \<forall>j. x j \<le> b j"
- using as(5)[rule_format,OF b(1) insertI1]
- apply -
- proof (erule disjE)
- assume "\<forall>j. x j \<le> b j"
- then show ?thesis
- apply(rule_tac x=b in bexI) using b
- apply auto
- done
- next
- assume "\<forall>j. b j \<le> x j"
- then show ?thesis
- apply (rule_tac x=x in bexI)
- apply (rule, rule)
- apply (insert b)
- apply (erule_tac x=xa in ballE)
- apply (erule_tac x=j in allE)+
- apply auto
- done
- qed
- ultimately show ?thesis by auto
- qed
-qed auto
-
-
-lemma kle_imp_pointwise: "kle n x y \<Longrightarrow> \<forall>j. x j \<le> y j"
- unfolding kle_def by auto
-
-lemma pointwise_antisym:
- fixes x :: "nat \<Rightarrow> nat"
- shows "(\<forall>j. x j \<le> y j) \<and> (\<forall>j. y j \<le> x j) \<longleftrightarrow> x = y"
- apply rule
- apply (rule ext)
- apply (erule conjE)
- apply (erule_tac x = xa in allE)+
- apply auto
- done
-
-lemma kle_trans:
- assumes "kle n x y"
- and "kle n y z"
- and "kle n x z \<or> kle n z x"
- shows "kle n x z"
- using assms
- apply -
- apply (erule disjE)
- apply assumption
-proof -
- case goal1
- then have "x = z"
- apply -
- apply (rule ext)
- apply (drule kle_imp_pointwise)+
- apply (erule_tac x=xa in allE)+
- apply auto
- done
- then show ?case by auto
-qed
-
-lemma kle_strict:
- assumes "kle n x y"
- and "x \<noteq> y"
- shows "\<forall>j. x j \<le> y j"
- and "\<exists>k. 1 \<le> k \<and> k \<le> n \<and> x k < y k"
- apply (rule kle_imp_pointwise[OF assms(1)])
-proof -
- obtain k where k: "k \<subseteq> {1..n} \<and> (\<forall>j. y j = x j + (if j \<in> k then 1 else 0))"
- using assms(1)[unfolded kle_def] ..
- show "\<exists>k. 1 \<le> k \<and> k \<le> n \<and> x k < y k"
- proof (cases "k = {}")
- case True
- then have "x = y"
- apply -
- apply (rule ext)
- using k
- apply auto
- done
- then show ?thesis
- using assms(2) by auto
- next
- case False
- then have "(SOME k'. k' \<in> k) \<in> k"
- apply -
- apply (rule someI_ex)
- apply auto
- done
- then show ?thesis
- apply (rule_tac x = "SOME k'. k' \<in> k" in exI)
- using k
- apply auto
- done
- qed
-qed
-
-lemma kle_minimal:
- assumes "finite s"
- and "s \<noteq> {}"
- and "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"
- shows "\<exists>a\<in>s. \<forall>x\<in>s. kle n a x"
-proof -
- have "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. a j \<le> x j"
- apply (rule pointwise_minimal_pointwise_maximal(1)[OF assms(1-2)])
- apply rule
- apply rule
- apply (drule_tac assms(3)[rule_format])
- apply assumption
- using kle_imp_pointwise
- apply auto
- done
- then obtain a where a: "a \<in> s" "\<forall>x\<in>s. \<forall>j. a j \<le> x j" ..
- show ?thesis
- apply (rule_tac x = a in bexI)
- proof
- fix x
- assume "x \<in> s"
- show "kle n a x"
- using assms(3)[rule_format,OF a(1) `x\<in>s`]
- apply -
- proof (erule disjE)
- assume "kle n x a"
- then have "x = a"
- apply -
- unfolding pointwise_antisym[symmetric]
- apply (drule kle_imp_pointwise)
- using a(2)[rule_format,OF `x\<in>s`]
- apply auto
- done
- then show ?thesis using kle_refl by auto
- qed
- qed (insert a, auto)
-qed
-
-lemma kle_maximal:
- assumes "finite s"
- and "s \<noteq> {}"
- and "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"
- shows "\<exists>a\<in>s. \<forall>x\<in>s. kle n x a"
-proof -
- have "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. a j \<ge> x j"
- apply (rule pointwise_minimal_pointwise_maximal(2)[OF assms(1-2)])
- apply rule
- apply rule
- apply (drule_tac assms(3)[rule_format],assumption)
- using kle_imp_pointwise
- apply auto
- done
- then obtain a where a: "a \<in> s" "\<forall>x\<in>s. \<forall>j. x j \<le> a j" ..
- show ?thesis
- apply (rule_tac x = a in bexI)
- proof
- fix x
- assume "x \<in> s"
- show "kle n x a"
- using assms(3)[rule_format,OF a(1) `x\<in>s`]
- apply -
- proof (erule disjE)
- assume "kle n a x"
- then have "x = a"
- apply -
- unfolding pointwise_antisym[symmetric]
- apply (drule kle_imp_pointwise)
- using a(2)[rule_format,OF `x\<in>s`]
- apply auto
- done
- then show ?thesis
- using kle_refl by auto
- qed
- qed (insert a, auto)
-qed
-
-lemma kle_strict_set:
- assumes "kle n x y"
- and "x \<noteq> y"
- shows "1 \<le> card {k\<in>{1..n}. x k < y k}"
-proof -
- obtain i where "1 \<le> i" "i \<le> n" "x i < y i"
- using kle_strict(2)[OF assms] by blast
- then have "card {i} \<le> card {k\<in>{1..n}. x k < y k}"
- apply -
- apply (rule card_mono)
- apply auto
- done
- then show ?thesis
- by auto
-qed
-
-lemma kle_range_combine:
- assumes "kle n x y"
- and "kle n y z"
- and "kle n x z \<or> kle n z x"
- and "m1 \<le> card {k\<in>{1..n}. x k < y k}"
- and "m2 \<le> card {k\<in>{1..n}. y k < z k}"
- shows "kle n x z \<and> m1 + m2 \<le> card {k\<in>{1..n}. x k < z k}"
- apply rule
- apply (rule kle_trans[OF assms(1-3)])
-proof -
- have "\<And>j. x j < y j \<Longrightarrow> x j < z j"
- apply (rule less_le_trans)
- using kle_imp_pointwise[OF assms(2)]
- apply auto
- done
- moreover
- have "\<And>j. y j < z j \<Longrightarrow> x j < z j"
- apply (rule le_less_trans)
- using kle_imp_pointwise[OF assms(1)]
- apply auto
- done
- ultimately
- have *: "{k\<in>{1..n}. x k < y k} \<union> {k\<in>{1..n}. y k < z k} = {k\<in>{1..n}. x k < z k}"
- by auto
- have **: "{k \<in> {1..n}. x k < y k} \<inter> {k \<in> {1..n}. y k < z k} = {}"
- unfolding disjoint_iff_not_equal
- apply rule
- apply rule
- apply (unfold mem_Collect_eq)
- apply (rule notI)
- apply (erule conjE)+
- proof -
- fix i j
- assume as: "i \<in> {1..n}" "x i < y i" "j \<in> {1..n}" "y j < z j" "i = j"
- obtain kx where kx: "kx \<subseteq> {1..n} \<and> (\<forall>j. y j = x j + (if j \<in> kx then 1 else 0))"
- using assms(1)[unfolded kle_def] ..
- have "x i < y i"
- using as by auto
- then have "i \<in> kx"
- using as(1) kx
- apply -
- apply (rule ccontr)
- apply auto
- done
- then have "x i + 1 = y i"
- using kx by auto
- moreover
- obtain ky where ky: "ky \<subseteq> {1..n} \<and> (\<forall>j. z j = y j + (if j \<in> ky then 1 else 0))"
- using assms(2)[unfolded kle_def] ..
- have "y i < z i"
- using as by auto
- then have "i \<in> ky"
- using as(1) ky
- apply -
- apply (rule ccontr)
- apply auto
- done
- then have "y i + 1 = z i"
- using ky by auto
- ultimately
- have "z i = x i + 2"
- by auto
- then show False
- using assms(3)
- unfolding kle_def
- by (auto simp add: split_if_eq1)
- qed
- have fin: "\<And>P. finite {x\<in>{1..n::nat}. P x}"
- by auto
- have "m1 + m2 \<le> card {k\<in>{1..n}. x k < y k} + card {k\<in>{1..n}. y k < z k}"
- using assms(4-5) by auto
- also have "\<dots> \<le> card {k\<in>{1..n}. x k < z k}"
- unfolding card_Un_Int[OF fin fin]
- unfolding * **
- by auto
- finally show "m1 + m2 \<le> card {k \<in> {1..n}. x k < z k}"
- by auto
-qed
-
-lemma kle_range_combine_l:
- assumes "kle n x y"
- and "kle n y z"
- and "kle n x z \<or> kle n z x"
- and "m \<le> card {k\<in>{1..n}. y(k) < z(k)}"
- shows "kle n x z \<and> m \<le> card {k\<in>{1..n}. x(k) < z(k)}"
- using kle_range_combine[OF assms(1-3) _ assms(4), of 0] by auto
-
-lemma kle_range_combine_r:
- assumes "kle n x y"
- and "kle n y z"
- and "kle n x z \<or> kle n z x" "m \<le> card {k\<in>{1..n}. x k < y k}"
- shows "kle n x z \<and> m \<le> card {k\<in>{1..n}. x(k) < z(k)}"
- using kle_range_combine[OF assms(1-3) assms(4), of 0] by auto
-
-lemma kle_range_induct:
- assumes "card s = Suc m"
- and "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"
- shows "\<exists>x\<in>s. \<exists>y\<in>s. kle n x y \<and> m \<le> card {k\<in>{1..n}. x k < y k}"
-proof -
- have "finite s" and "s \<noteq> {}"
- using assms(1)
- by (auto intro: card_ge_0_finite)
- then show ?thesis
- using assms
- proof (induct m arbitrary: s)
- case 0
- then show ?case
- using kle_refl by auto
- next
- case (Suc m)
- then obtain a where a: "a \<in> s" "\<forall>x\<in>s. kle n a x"
- using kle_minimal[of s n] by auto
- show ?case
- proof (cases "s \<subseteq> {a}")
- case False
- then have "card (s - {a}) = Suc m" and "s - {a} \<noteq> {}"
- using card_Diff_singleton[OF _ a(1)] Suc(4) `finite s`
- by auto
- then obtain x b where xb:
- "x \<in> s - {a}"
- "b \<in> s - {a}"
- "kle n x b"
- "m \<le> card {k \<in> {1..n}. x k < b k}"
- using Suc(1)[of "s - {a}"]
- using Suc(5) `finite s`
- by auto
- have "1 \<le> card {k \<in> {1..n}. a k < x k}" and "m \<le> card {k \<in> {1..n}. x k < b k}"
- apply (rule kle_strict_set)
- apply (rule a(2)[rule_format])
- using a and xb
- apply auto
- done
- then show ?thesis
- apply (rule_tac x=a in bexI)
- apply (rule_tac x=b in bexI)
- using kle_range_combine[OF a(2)[rule_format] xb(3) Suc(5)[rule_format], of 1 "m"]
- using a(1) xb(1-2)
- apply auto
- done
- next
- case True
- then have "s = {a}"
- using Suc(3) by auto
- then have "card s = 1"
- by auto
- then have False
- using Suc(4) `finite s` by auto
- then show ?thesis
- by auto
- qed
- qed
-qed
-
-lemma kle_Suc: "kle n x y \<Longrightarrow> kle (n + 1) x y"
- unfolding kle_def
- apply (erule exE)
- apply (rule_tac x=k in exI)
- apply auto
- done
-
-lemma kle_trans_1:
- assumes "kle n x y"
- shows "x j \<le> y j"
- and "y j \<le> x j + 1"
- using assms[unfolded kle_def] by auto
-
-lemma kle_trans_2:
- assumes "kle n a b"
- and "kle n b c"
- and "\<forall>j. c j \<le> a j + 1"
- shows "kle n a c"
-proof -
- obtain kk1 where kk1: "kk1 \<subseteq> {1..n} \<and> (\<forall>j. b j = a j + (if j \<in> kk1 then 1 else 0))"
- using assms(1)[unfolded kle_def] ..
- obtain kk2 where kk2: "kk2 \<subseteq> {1..n} \<and> (\<forall>j. c j = b j + (if j \<in> kk2 then 1 else 0))"
- using assms(2)[unfolded kle_def] ..
- show ?thesis
- unfolding kle_def
- apply (rule_tac x="kk1 \<union> kk2" in exI)
- apply rule
- defer
- proof
- fix i
- show "c i = a i + (if i \<in> kk1 \<union> kk2 then 1 else 0)"
- proof (cases "i \<in> kk1 \<union> kk2")
- case True
- then have "c i \<ge> a i + (if i \<in> kk1 \<union> kk2 then 1 else 0)"
- unfolding kk1[THEN conjunct2,rule_format,of i] kk2[THEN conjunct2,rule_format,of i]
- by auto
- moreover
- have "c i \<le> a i + (if i \<in> kk1 \<union> kk2 then 1 else 0)"
- using True assms(3) by auto
- ultimately show ?thesis by auto
- next
- case False
- then show ?thesis
- using kk1 kk2 by auto
- qed
- qed (insert kk1 kk2, auto)
-qed
-
-lemma kle_between_r:
- assumes "kle n a b"
- and "kle n b c"
- and "kle n a x"
- and "kle n c x"
- shows "kle n b x"
- apply (rule kle_trans_2[OF assms(2,4)])
-proof
- have *: "\<And>c b x::nat. x \<le> c + 1 \<Longrightarrow> c \<le> b \<Longrightarrow> x \<le> b + 1"
- by auto
- fix j
- show "x j \<le> b j + 1"
- apply (rule *)
- using kle_trans_1[OF assms(1),of j] kle_trans_1[OF assms(3), of j]
- apply auto
- done
-qed
-
-lemma kle_between_l:
- assumes "kle n a b"
- and "kle n b c"
- and "kle n x a"
- and "kle n x c"
- shows "kle n x b"
- apply (rule kle_trans_2[OF assms(3,1)])
-proof
- have *: "\<And>c b x::nat. c \<le> x + 1 \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> x + 1"
- by auto
- fix j
- show "b j \<le> x j + 1"
- apply (rule *)
- using kle_trans_1[OF assms(2),of j] kle_trans_1[OF assms(4), of j]
- apply auto
- done
-qed
-
-lemma kle_adjacent:
- assumes "\<forall>j. b j = (if j = k then a(j) + 1 else a j)"
- and "kle n a x"
- and "kle n x b"
- shows "x = a \<or> x = b"
-proof (cases "x k = a k")
- case True
- show ?thesis
- apply (rule disjI1)
- apply (rule ext)
- proof -
- fix j
- have "x j \<le> a j"
- using kle_imp_pointwise[OF assms(3),THEN spec[where x=j]]
- unfolding assms(1)[rule_format]
- apply -
- apply(cases "j = k")
- using True
- apply auto
- done
- then show "x j = a j"
- using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]]
- by auto
- qed
-next
- case False
- show ?thesis
- apply (rule disjI2)
- apply (rule ext)
- proof -
- fix j
- have "x j \<ge> b j"
- using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]]
- unfolding assms(1)[rule_format]
- apply -
- apply (cases "j = k")
- using False
- apply auto
- done
- then show "x j = b j"
- using kle_imp_pointwise[OF assms(3),THEN spec[where x=j]]
- by auto
- qed
-qed
-
-
-subsection {* Kuhn's notion of a simplex (a reformulation to avoid so much indexing) *}
-
-definition "ksimplex p n (s::(nat \<Rightarrow> nat) set) \<longleftrightarrow>
- card s = n + 1 \<and>
- (\<forall>x\<in>s. \<forall>j. x j \<le> p) \<and>
- (\<forall>x\<in>s. \<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p) \<and>
- (\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x)"
-
-lemma ksimplexI:
- "card s = n + 1 \<Longrightarrow>
- \<forall>x\<in>s. \<forall>j. x j \<le> p \<Longrightarrow>
- \<forall>x\<in>s. \<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p \<Longrightarrow>
- \<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x \<Longrightarrow>
- ksimplex p n s"
- unfolding ksimplex_def by auto
-
-lemma ksimplex_eq:
- "ksimplex p n (s::(nat \<Rightarrow> nat) set) \<longleftrightarrow>
- card s = n + 1 \<and>
- finite s \<and>
- (\<forall>x\<in>s. \<forall>j. x(j) \<le> p) \<and>
- (\<forall>x\<in>s. \<forall>j. j\<notin>{1..n} \<longrightarrow> x j = p) \<and>
- (\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x)"
- unfolding ksimplex_def by (auto intro: card_ge_0_finite)
-
-lemma ksimplex_extrema:
- assumes "ksimplex p n s"
- obtains a b where "a \<in> s"
- and "b \<in> s"
- and "\<forall>x\<in>s. kle n a x \<and> kle n x b"
- and "\<forall>i. b i = (if i \<in> {1..n} then a i + 1 else a i)"
-proof (cases "n = 0")
- case True
- obtain x where *: "s = {x}"
- using assms[unfolded ksimplex_eq True,THEN conjunct1]
- unfolding add_0_left card_1_exists
- by auto
- show ?thesis
- apply (rule that[of x x])
- unfolding * True
- apply auto
- done
-next
- note assm = assms[unfolded ksimplex_eq]
- case False
- have "s \<noteq> {}"
- using assm by auto
- obtain a where a: "a \<in> s" "\<forall>x\<in>s. kle n a x"
- using `s \<noteq> {}` assm
- using kle_minimal[of s n]
- by auto
- obtain b where b: "b \<in> s" "\<forall>x\<in>s. kle n x b"
- using `s \<noteq> {}` assm
- using kle_maximal[of s n]
- by auto
- obtain c d where c_d: "c \<in> s" "d \<in> s" "kle n c d" "n \<le> card {k \<in> {1..n}. c k < d k}"
- using kle_range_induct[of s n n]
- using assm
- by auto
- have "kle n c b \<and> n \<le> card {k \<in> {1..n}. c k < b k}"
- apply (rule kle_range_combine_r[where y=d])
- using c_d a b
- apply auto
- done
- then have "kle n a b \<and> n \<le> card {k\<in>{1..n}. a(k) < b(k)}"
- apply -
- apply (rule kle_range_combine_l[where y=c])
- using a `c \<in> s` `b \<in> s`
- apply auto
- done
- moreover
- have "card {1..n} \<ge> card {k\<in>{1..n}. a(k) < b(k)}"
- by (rule card_mono) auto
- ultimately
- have *: "{k\<in>{1 .. n}. a k < b k} = {1..n}"
- apply -
- apply (rule card_subset_eq)
- apply auto
- done
- show ?thesis
- apply (rule that[OF a(1) b(1)])
- defer
- apply (subst *[symmetric])
- unfolding mem_Collect_eq
- proof
- obtain k where k: "k \<subseteq> {1..n} \<and> (\<forall>j. b j = a j + (if j \<in> k then 1 else 0))"
- using a(2)[rule_format, OF b(1), unfolded kle_def] ..
- fix i
- show "b i = (if i \<in> {1..n} \<and> a i < b i then a i + 1 else a i)"
- proof (cases "i \<in> {1..n}")
- case True
- then show ?thesis
- unfolding k[THEN conjunct2,rule_format] by auto
- next
- case False
- have "a i = p"
- using assm and False `a\<in>s` by auto
- moreover have "b i = p"
- using assm and False `b\<in>s` by auto
- ultimately show ?thesis
- by auto
- qed
- qed (insert a(2) b(2) assm, auto)
-qed
-
-lemma ksimplex_extrema_strong:
- assumes "ksimplex p n s"
- and "n \<noteq> 0"
- obtains a b where "a \<in> s"
- and "b \<in> s"
- and "a \<noteq> b"
- and "\<forall>x\<in>s. kle n a x \<and> kle n x b"
- and "\<forall>i. b i = (if i \<in> {1..n} then a(i) + 1 else a i)"
+ fixes bnd compo compo' face S F
+ defines "nF s == card {f\<in>F. face f s \<and> compo' f}"
+ assumes [simp, intro]: "finite F" -- "faces" and [simp, intro]: "finite S" -- "simplices"
+ and "\<And>f. f \<in> F \<Longrightarrow> bnd f \<Longrightarrow> card {s\<in>S. face f s} = 1"
+ and "\<And>f. f \<in> F \<Longrightarrow> \<not> bnd f \<Longrightarrow> card {s\<in>S. face f s} = 2"
+ and "\<And>s. s \<in> S \<Longrightarrow> compo s \<Longrightarrow> nF s = 1"
+ and "\<And>s. s \<in> S \<Longrightarrow> \<not> compo s \<Longrightarrow> nF s = 0 \<or> nF s = 2"
+ and "odd (card {f\<in>F. compo' f \<and> bnd f})"
+ shows "odd (card {s\<in>S. compo s})"
proof -
- obtain a b where ab: "a \<in> s" "b \<in> s"
- "\<forall>x\<in>s. kle n a x \<and> kle n x b" "\<forall>i. b(i) = (if i \<in> {1..n} then a(i) + 1 else a(i))"
- apply (rule ksimplex_extrema[OF assms(1)])
- apply auto
- done
- have "a \<noteq> b"
- apply (rule notI)
- apply (drule cong[of _ _ 1 1])
- using ab(4) assms(2)
- apply auto
- done
- then show ?thesis
- apply (rule_tac that[of a b])
- using ab
- apply auto
- done
-qed
-
-lemma ksimplexD:
- assumes "ksimplex p n s"
- shows "card s = n + 1"
- and "finite s"
- and "card s = n + 1"
- and "\<forall>x\<in>s. \<forall>j. x j \<le> p"
- and "\<forall>x\<in>s. \<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p"
- and "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"
- using assms unfolding ksimplex_eq by auto
-
-lemma ksimplex_successor:
- assumes "ksimplex p n s"
- and "a \<in> s"
- shows "(\<forall>x\<in>s. kle n x a) \<or> (\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then a j + 1 else a j))"
-proof (cases "\<forall>x\<in>s. kle n x a")
- case True
- then show ?thesis by auto
-next
- note assm = ksimplexD[OF assms(1)]
- case False
- then obtain b where b: "b \<in> s" "\<not> kle n b a" "\<forall>x\<in>{x \<in> s. \<not> kle n x a}. kle n b x"
- using kle_minimal[of "{x\<in>s. \<not> kle n x a}" n] and assm
- by auto
- then have **: "1 \<le> card {k\<in>{1..n}. a k < b k}"
- apply -
- apply (rule kle_strict_set)
- using assm(6) and `a\<in>s`
- apply (auto simp add: kle_refl)
- done
-
- let ?kle1 = "{x \<in> s. \<not> kle n x a}"
- have "card ?kle1 > 0"
- apply (rule ccontr)
- using assm(2) and False
- apply auto
- done
- then have sizekle1: "card ?kle1 = Suc (card ?kle1 - 1)"
- using assm(2) by auto
- obtain c d where c_d: "c \<in> s" "\<not> kle n c a" "d \<in> s" "\<not> kle n d a"
- "kle n c d" "card ?kle1 - 1 \<le> card {k \<in> {1..n}. c k < d k}"
- using kle_range_induct[OF sizekle1, of n] using assm by auto
-
- let ?kle2 = "{x \<in> s. kle n x a}"
- have "card ?kle2 > 0"
- apply (rule ccontr)
- using assm(6)[rule_format,of a a] and `a\<in>s` and assm(2)
- apply auto
- done
- then have sizekle2: "card ?kle2 = Suc (card ?kle2 - 1)"
- using assm(2) by auto
- obtain e f where e_f: "e \<in> s" "kle n e a" "f \<in> s" "kle n f a"
- "kle n e f" "card ?kle2 - 1 \<le> card {k \<in> {1..n}. e k < f k}"
- using kle_range_induct[OF sizekle2, of n]
- using assm
- by auto
-
- have "card {k\<in>{1..n}. a k < b k} = 1"
- proof (rule ccontr)
- assume "\<not> ?thesis"
- then have as: "card {k\<in>{1..n}. a k < b k} \<ge> 2"
- using ** by auto
- have *: "finite ?kle2" "finite ?kle1" "?kle2 \<union> ?kle1 = s" "?kle2 \<inter> ?kle1 = {}"
- using assm(2) by auto
- have "(card ?kle2 - 1) + 2 + (card ?kle1 - 1) = card ?kle2 + card ?kle1"
- using sizekle1 sizekle2 by auto
- also have "\<dots> = n + 1"
- unfolding card_Un_Int[OF *(1-2)] *(3-)
- using assm(3)
- by auto
- finally have n: "(card ?kle2 - 1) + (2 + (card ?kle1 - 1)) = n + 1"
- by auto
- have "kle n e a \<and> card {x \<in> s. kle n x a} - 1 \<le> card {k \<in> {1..n}. e k < a k}"
- apply (rule kle_range_combine_r[where y=f])
- using e_f using `a \<in> s` assm(6)
- apply auto
- done
- moreover have "kle n b d \<and> card {x \<in> s. \<not> kle n x a} - 1 \<le> card {k \<in> {1..n}. b k < d k}"
- apply (rule kle_range_combine_l[where y=c])
- using c_d using assm(6) and b
- apply auto
- done
- then have "kle n a d \<and> 2 + (card {x \<in> s. \<not> kle n x a} - 1) \<le> card {k \<in> {1..n}. a k < d k}"
- apply -
- apply (rule kle_range_combine[where y=b]) using as and b assm(6) `a \<in> s` `d \<in> s`
- apply blast+
- done
- ultimately
- have "kle n e d \<and> (card ?kle2 - 1) + (2 + (card ?kle1 - 1)) \<le> card {k\<in>{1..n}. e k < d k}"
- apply -
- apply (rule kle_range_combine[where y=a]) using assm(6)[rule_format, OF `e \<in> s` `d \<in> s`]
- apply blast+
- done
- moreover have "card {k \<in> {1..n}. e k < d k} \<le> card {1..n}"
- by (rule card_mono) auto
- ultimately show False
- unfolding n by auto
- qed
- then obtain k where k:
- "k \<in> {1..n} \<and> a k < b k"
- "\<And>y y'. (y \<in> {1..n} \<and> a y < b y) \<and> y' \<in> {1..n} \<and> a y' < b y' \<Longrightarrow> y = y'"
- unfolding card_1_exists by blast
-
- show ?thesis
- apply (rule disjI2)
- apply (rule_tac x=b in bexI)
- apply (rule_tac x=k in bexI)
- proof
- fix j :: nat
- have "kle n a b"
- using b and assm(6)[rule_format, OF `a\<in>s` `b\<in>s`]
- by auto
- then obtain kk where kk: "kk \<subseteq> {1..n}" "\<And>j. b j = a j + (if j \<in> kk then 1 else 0)"
- unfolding kle_def by blast
- have kkk: "k \<in> kk"
- apply (rule ccontr)
- using k(1)
- unfolding kk(2)
- apply auto
- done
- show "b j = (if j = k then a j + 1 else a j)"
- proof (cases "j \<in> kk")
- case True
- then have "j = k"
- apply -
- apply (rule k(2))
- using kk kkk
- apply auto
- done
- then show ?thesis
- unfolding kk(2) using kkk by auto
- next
- case False
- then have "j \<noteq> k"
- using k(2)[of j k] and kkk
- by auto
- then show ?thesis
- unfolding kk(2)
- using kkk and False
- by auto
- qed
- qed (insert k(1) `b \<in> s`, auto)
-qed
-
-lemma ksimplex_predecessor:
- assumes "ksimplex p n s"
- and "a \<in> s"
- shows "(\<forall>x\<in>s. kle n a x) \<or> (\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. a j = (if j = k then y j + 1 else y j))"
-proof (cases "\<forall>x\<in>s. kle n a x")
- case True
- then show ?thesis by auto
-next
- note assm = ksimplexD[OF assms(1)]
- case False
- then obtain b where b: "b \<in> s" "\<not> kle n a b" "\<forall>x\<in>{x \<in> s. \<not> kle n a x}. kle n x b"
- using kle_maximal[of "{x\<in>s. \<not> kle n a x}" n] and assm
- by auto
- then have **: "1 \<le> card {k\<in>{1..n}. a k > b k}"
- apply -
- apply (rule kle_strict_set)
- using assm(6) and `a \<in> s`
- apply (auto simp add: kle_refl)
- done
-
- let ?kle1 = "{x \<in> s. \<not> kle n a x}"
- have "card ?kle1 > 0"
- apply (rule ccontr)
- using assm(2) and False
- apply auto
- done
- then have sizekle1: "card ?kle1 = Suc (card ?kle1 - 1)"
- using assm(2) by auto
- obtain c d where c_d: "c \<in> s" "\<not> kle n a c" "d \<in> s" "\<not> kle n a d"
- "kle n d c" "card ?kle1 - 1 \<le> card {k \<in> {1..n}. c k > d k}"
- using kle_range_induct[OF sizekle1, of n]
- using assm
- by auto
-
- let ?kle2 = "{x \<in> s. kle n a x}"
- have "card ?kle2 > 0"
- apply (rule ccontr)
- using assm(6)[rule_format,of a a] and `a \<in> s` and assm(2)
- apply auto
- done
- then have sizekle2: "card ?kle2 = Suc (card ?kle2 - 1)"
- using assm(2)
- by auto
- obtain e f where e_f: "e \<in> s" "kle n a e" "f \<in> s" "kle n a f"
- "kle n f e" "card ?kle2 - 1 \<le> card {k \<in> {1..n}. e k > f k}"
- using kle_range_induct[OF sizekle2, of n]
- using assm
- by auto
-
- have "card {k\<in>{1..n}. a k > b k} = 1"
- proof (rule ccontr)
- assume "\<not> ?thesis"
- then have as: "card {k\<in>{1..n}. a k > b k} \<ge> 2"
- using ** by auto
- have *: "finite ?kle2" "finite ?kle1" "?kle2 \<union> ?kle1 = s" "?kle2 \<inter> ?kle1 = {}"
- using assm(2) by auto
- have "(card ?kle2 - 1) + 2 + (card ?kle1 - 1) = card ?kle2 + card ?kle1"
- using sizekle1 sizekle2 by auto
- also have "\<dots> = n + 1"
- unfolding card_Un_Int[OF *(1-2)] *(3-)
- using assm(3) by auto
- finally have n: "(card ?kle1 - 1) + 2 + (card ?kle2 - 1) = n + 1"
- by auto
- have "kle n a e \<and> card {x \<in> s. kle n a x} - 1 \<le> card {k \<in> {1..n}. e k > a k}"
- apply (rule kle_range_combine_l[where y=f])
- using e_f and `a\<in>s` assm(6)
- apply auto
- done
- moreover have "kle n d b \<and> card {x \<in> s. \<not> kle n a x} - 1 \<le> card {k \<in> {1..n}. b k > d k}"
- apply (rule kle_range_combine_r[where y=c])
- using c_d and assm(6) and b
- apply auto
- done
- then have "kle n d a \<and> (card {x \<in> s. \<not> kle n a x} - 1) + 2 \<le> card {k \<in> {1..n}. a k > d k}"
- apply -
- apply (rule kle_range_combine[where y=b]) using as and b assm(6) `a \<in> s` `d \<in> s`
- apply blast+
- done
- ultimately have "kle n d e \<and> (card ?kle1 - 1 + 2) + (card ?kle2 - 1) \<le> card {k\<in>{1..n}. e k > d k}"
- apply -
- apply (rule kle_range_combine[where y=a])
- using assm(6)[rule_format,OF `e\<in>s` `d\<in>s`]
- apply blast+
- done
- moreover have "card {k \<in> {1..n}. e k > d k} \<le> card {1..n}"
- by (rule card_mono) auto
- ultimately show False
- unfolding n by auto
- qed
- then obtain k where k:
- "k \<in> {1..n} \<and> b k < a k"
- "\<And>y y'. (y \<in> {1..n} \<and> b y < a y) \<and> y' \<in> {1..n} \<and> b y' < a y' \<Longrightarrow> y = y'"
- unfolding card_1_exists by blast
-
- show ?thesis
- apply (rule disjI2)
- apply (rule_tac x=b in bexI)
- apply (rule_tac x=k in bexI)
- proof
- fix j :: nat
- have "kle n b a"
- using b and assm(6)[rule_format, OF `a\<in>s` `b\<in>s`] by auto
- then obtain kk where kk: "kk \<subseteq> {1..n}" "\<And>j. a j = b j + (if j \<in> kk then 1 else 0)"
- unfolding kle_def by blast
- have kkk: "k \<in> kk"
- apply (rule ccontr)
- using k(1)
- unfolding kk(2)
- apply auto
- done
- show "a j = (if j = k then b j + 1 else b j)"
- proof (cases "j \<in> kk")
- case True
- then have "j = k"
- apply -
- apply (rule k(2))
- using kk kkk
- apply auto
- done
- then show ?thesis
- unfolding kk(2) using kkk by auto
- next
- case False
- then have "j \<noteq> k"
- using k(2)[of j k]
- using kkk
- by auto
- then show ?thesis
- unfolding kk(2)
- using kkk and False
- by auto
- qed
- qed (insert k(1) `b\<in>s`, auto)
-qed
-
-
-subsection {* The lemmas about simplices that we need. *}
-
-(* FIXME: These are clones of lemmas in Library/FuncSet *)
-lemma card_funspace':
- assumes "finite s"
- and "finite t"
- and "card s = m"
- and "card t = n"
- shows "card {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)} = n ^ m"
- (is "card (?M s) = _")
- using assms
-proof (induct m arbitrary: s)
- case 0
- have [simp]: "{f. \<forall>x. f x = d} = {\<lambda>x. d}"
- apply (rule set_eqI)
- apply rule
- unfolding mem_Collect_eq
- apply rule
- apply (rule ext)
- apply auto
- done
- from 0 show ?case
- by auto
-next
- case (Suc m)
- obtain a s0 where as0:
- "s = insert a s0"
- "a \<notin> s0"
- "card s0 = m"
- "m = 0 \<longrightarrow> s0 = {}"
- using card_eq_SucD[OF Suc(4)] by auto
- have **: "card s0 = m"
- using as0 using Suc(2) Suc(4)
- by auto
- let ?l = "(\<lambda>(b, g) x. if x = a then b else g x)"
- have *: "?M (insert a s0) = ?l ` {(b,g). b\<in>t \<and> g\<in>?M s0}"
- apply (rule set_eqI, rule)
- unfolding mem_Collect_eq image_iff
- apply (erule conjE)
- apply (rule_tac x="(x a, \<lambda>y. if y\<in>s0 then x y else d)" in bexI)
- apply (rule ext)
- prefer 3
- apply rule
- defer
- apply (erule bexE)
- apply rule
- unfolding mem_Collect_eq
- apply (erule splitE)+
- apply (erule conjE)+
- proof -
- fix x xa xb xc y
- assume as:
- "x = (\<lambda>(b, g) x. if x = a then b else g x) xa"
- "xb \<in> UNIV - insert a s0"
- "xa = (xc, y)"
- "xc \<in> t"
- "\<forall>x\<in>s0. y x \<in> t"
- "\<forall>x\<in>UNIV - s0. y x = d"
- then show "x xb = d"
- unfolding as by auto
- qed auto
- have inj: "inj_on ?l {(b,g). b\<in>t \<and> g\<in>?M s0}"
- unfolding inj_on_def
- apply rule
- apply rule
- apply rule
- unfolding mem_Collect_eq
- apply (erule splitE conjE)+
- proof -
- case goal1 note as = this(1,4-)[unfolded goal1 split_conv]
- have "xa = xb"
- using as(1)[THEN cong[of _ _ a]] by auto
- moreover have "ya = yb"
- proof (rule ext)
- fix x
- show "ya x = yb x"
- proof (cases "x = a")
- case False
- then show ?thesis
- using as(1)[THEN cong[of _ _ x x]] by auto
- next
- case True
- then show ?thesis
- using as(5,7) using as0(2) by auto
- qed
- qed
- ultimately show ?case
- unfolding goal1 by auto
- qed
- have "finite s0"
- using `finite s` unfolding as0 by simp
- show ?case
- unfolding as0 * card_image[OF inj]
- using assms
- unfolding SetCompr_Sigma_eq
- unfolding card_cartesian_product
- using Suc(1)[OF `finite s0` `finite t` ** `card t = n`]
- by auto
-qed
-
-lemma card_funspace:
- assumes "finite s"
- and "finite t"
- shows "card {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)} = card t ^ card s"
- using assms by (auto intro: card_funspace')
-
-lemma finite_funspace:
- assumes "finite s"
- and "finite t"
- shows "finite {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)}"
- (is "finite ?S")
-proof (cases "card t > 0")
- case True
- have "card ?S = card t ^ card s"
- using assms by (auto intro!: card_funspace)
- then show ?thesis
- using True by (rule_tac card_ge_0_finite) simp
-next
- case False
- then have "t = {}"
- using `finite t` by auto
- show ?thesis
- proof (cases "s = {}")
- case True
- have *: "{f. \<forall>x. f x = d} = {\<lambda>x. d}"
- by auto
- from True show ?thesis
- using `t = {}` by (auto simp: *)
- next
- case False
- then show ?thesis
- using `t = {}` by simp
- qed
-qed
-
-lemma finite_simplices: "finite {s. ksimplex p n s}"
- apply (rule finite_subset[of _ "{s. s\<subseteq>{f. (\<forall>i\<in>{1..n}. f i \<in> {0..p}) \<and> (\<forall>i\<in>UNIV-{1..n}. f i = p)}}"])
- unfolding ksimplex_def
- defer
- apply (rule finite_Collect_subsets)
- apply (rule finite_funspace)
- apply auto
- done
-
-lemma simplex_top_face:
- assumes "0 < p"
- and "\<forall>x\<in>f. x (n + 1) = p"
- shows "(\<exists>s a. ksimplex p (n + 1) s \<and> a \<in> s \<and> (f = s - {a})) \<longleftrightarrow> ksimplex p n f"
- (is "?ls = ?rs")
-proof
- assume ?ls
- then obtain s a where sa:
- "ksimplex p (n + 1) s"
- "a \<in> s"
- "f = s - {a}"
- by auto
- show ?rs
- unfolding ksimplex_def sa(3)
- apply rule
- defer
- apply rule
- defer
- apply (rule, rule, rule, rule)
- defer
- apply (rule, rule)
- proof -
- fix x y
- assume as: "x \<in>s - {a}" "y \<in>s - {a}"
- have xyp: "x (n + 1) = y (n + 1)"
- using as(1)[unfolded sa(3)[symmetric], THEN assms(2)[rule_format]]
- using as(2)[unfolded sa(3)[symmetric], THEN assms(2)[rule_format]]
- by auto
- show "kle n x y \<or> kle n y x"
- proof (cases "kle (n + 1) x y")
- case True
- then obtain k where k: "k \<subseteq> {1..n + 1}" "\<And>j. y j = x j + (if j \<in> k then 1 else 0)"
- unfolding kle_def by blast
- then have *: "n + 1 \<notin> k" using xyp by auto
- have "\<not> (\<exists>x\<in>k. x \<notin> {1..n})"
- apply (rule notI)
- apply (erule bexE)
- proof -
- fix x
- assume as: "x \<in> k" "x \<notin> {1..n}"
- have "x \<noteq> n + 1"
- using as and * by auto
- then show False
- using as and k(1) by auto
- qed
- then show ?thesis
- apply -
- apply (rule disjI1)
- unfolding kle_def
- using k(2)
- apply (rule_tac x=k in exI)
- apply auto
- done
- next
- case False
- then have "kle (n + 1) y x"
- using ksimplexD(6)[OF sa(1),rule_format, of x y] and as
- by auto
- then obtain k where k: "k \<subseteq> {1..n + 1}" "\<And>j. x j = y j + (if j \<in> k then 1 else 0)"
- unfolding kle_def by auto
- then have *: "n + 1 \<notin> k"
- using xyp by auto
- then have "\<not> (\<exists>x\<in>k. x \<notin> {1..n})"
- apply -
- apply (rule notI)
- apply (erule bexE)
- proof -
- fix x
- assume as: "x \<in> k" "x \<notin> {1..n}"
- have "x \<noteq> n + 1"
- using as and * by auto
- then show False
- using as and k(1)
- by auto
- qed
- then show ?thesis
- apply -
- apply (rule disjI2)
- unfolding kle_def
- using k(2)
- apply (rule_tac x = k in exI)
- apply auto
- done
- qed
- next
- fix x j
- assume as: "x \<in> s - {a}" "j \<notin> {1..n}"
- then show "x j = p"
- using as(1)[unfolded sa(3)[symmetric], THEN assms(2)[rule_format]]
- apply (cases "j = n + 1")
- using sa(1)[unfolded ksimplex_def]
- apply auto
- done
- qed (insert sa ksimplexD[OF sa(1)], auto)
-next
- assume ?rs note rs=ksimplexD[OF this]
- obtain a b where ab:
- "a \<in> f"
- "b \<in> f"
- "\<forall>x\<in>f. 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)"
- by (rule ksimplex_extrema[OF `?rs`])
- def c \<equiv> "\<lambda>i. if i = (n + 1) then p - 1 else a i"
- have "c \<notin> f"
- apply (rule notI)
- apply (drule assms(2)[rule_format])
- unfolding c_def
- using assms(1)
- apply auto
- done
- then show ?ls
- apply (rule_tac x = "insert c f" in exI)
- apply (rule_tac x = c in exI)
- unfolding ksimplex_def conj_assoc
- apply (rule conjI)
- defer
- apply (rule conjI)
- defer
- apply (rule conjI)
- defer
- apply (rule conjI)
- defer
- proof (rule_tac[3-5] ballI allI)+
- fix x j
- assume x: "x \<in> insert c f"
- then show "x j \<le> p"
- proof (cases "x = c")
- case True
- show ?thesis
- unfolding True c_def
- apply (cases "j = n + 1")
- using ab(1) and rs(4)
- apply auto
- done
- next
- case False
- with insert x rs(4) show ?thesis
- by (auto simp add: c_def)
- qed
- show "j \<notin> {1..n + 1} \<longrightarrow> x j = p"
- apply (cases "x = c")
- using x ab(1) rs(5)
- unfolding c_def
- apply auto
- done
- {
- fix z
- assume z: "z \<in> insert c f"
- then have "kle (n + 1) c z"
- proof (cases "z = c")
- case False
- then have "z \<in> f"
- using z by auto
- with ab(3) have "kle n a z" by blast
- then obtain k where "k \<subseteq> {1..n}" "\<And>j. z j = a j + (if j \<in> k then 1 else 0)"
- unfolding kle_def by blast
- then show "kle (n + 1) c z"
- unfolding kle_def
- apply (rule_tac x="insert (n + 1) k" in exI)
- unfolding c_def
- using ab
- using rs(5)[rule_format,OF ab(1),of "n + 1"] assms(1)
- apply auto
- done
- next
- case True
- then show ?thesis by auto
- qed
- } note * = this
- fix y
- assume y: "y \<in> insert c f"
- show "kle (n + 1) x y \<or> kle (n + 1) y x"
- proof (cases "x = c \<or> y = c")
- case False
- then have **: "x \<in> f" "y \<in> f"
- using x y by auto
- show ?thesis
- using rs(6)[rule_format,OF **]
- by (auto dest: kle_Suc)
- qed (insert * x y, auto)
- qed (insert rs, auto)
-qed
-
-lemma ksimplex_fix_plane:
- fixes a a0 a1 :: "nat \<Rightarrow> nat"
- assumes "a \<in> s"
- and "j \<in> {1..n}"
- and "\<forall>x\<in>s - {a}. x j = q"
- and "a0 \<in> s"
- and "a1 \<in> s"
- and "\<forall>i. a1 i = (if i \<in> {1..n} then a0 i + 1 else a0 i)"
- shows "a = a0 \<or> a = a1"
-proof -
- have *: "\<And>P A x y. \<forall>x\<in>A. P x \<Longrightarrow> x\<in>A \<Longrightarrow> y\<in>A \<Longrightarrow> P x \<and> P y"
- by auto
- show ?thesis
- apply (rule ccontr)
- using *[OF assms(3), of a0 a1]
- unfolding assms(6)[THEN spec[where x=j]]
- using assms(1-2,4-5)
- apply auto
- done
-qed
-
-lemma ksimplex_fix_plane_0:
- fixes a a0 a1 :: "nat \<Rightarrow> nat"
- assumes "a \<in> s"
- and "j \<in> {1..n}"
- and "\<forall>x\<in>s - {a}. x j = 0"
- and "a0 \<in> s"
- and "a1 \<in> s"
- and "\<forall>i. a1 i = (if i\<in>{1..n} then a0 i + 1 else a0 i)"
- shows "a = a1"
- apply (rule ccontr)
- using ksimplex_fix_plane[OF assms]
- using assms(3)[THEN bspec[where x=a1]]
- using assms(2,5)
- unfolding assms(6)[THEN spec[where x=j]]
- apply simp
- done
-
-lemma ksimplex_fix_plane_p:
- assumes "ksimplex p n s"
- and "a \<in> s"
- and "j \<in> {1..n}"
- and "\<forall>x\<in>s - {a}. x j = p"
- and "a0 \<in> s"
- and "a1 \<in> s"
- and "\<forall>i. a1 i = (if i\<in>{1..n} then a0 i + 1 else a0 i)"
- shows "a = a0"
-proof (rule ccontr)
- note s = ksimplexD[OF assms(1),rule_format]
- assume as: "\<not> ?thesis"
- then have *: "a0 \<in> s - {a}"
- using assms(5) by auto
- then have "a1 = a"
- using ksimplex_fix_plane[OF assms(2-)] by auto
- then show False
- using as and assms(3,5) and assms(7)[rule_format,of j]
- unfolding assms(4)[rule_format,OF *]
- using s(4)[OF assms(6), of j]
- by auto
-qed
-
-lemma ksimplex_replace_0:
- assumes "ksimplex p n s" "a \<in> s"
- and "n \<noteq> 0"
- and "j \<in> {1..n}"
- and "\<forall>x\<in>s - {a}. x j = 0"
- shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 1"
-proof -
- have *: "\<And>s' a a'. s' - {a'} = s - {a} \<Longrightarrow> a' = a \<Longrightarrow> a' \<in> s' \<Longrightarrow> a \<in> s \<Longrightarrow> s' = s"
- by auto
- have **: "\<And>s' a'. ksimplex p n s' \<Longrightarrow> a' \<in> s' \<Longrightarrow> s' - {a'} = s - {a} \<Longrightarrow> s' = s"
- proof -
- case goal1
- obtain a0 a1 where exta:
- "a0 \<in> s"
- "a1 \<in> s"
- "a0 \<noteq> a1"
- "\<And>x. x \<in> s \<Longrightarrow> kle n a0 x \<and> kle n x a1"
- "\<And>i. a1 i = (if i \<in> {1..n} then a0 i + 1 else a0 i)"
- by (rule ksimplex_extrema_strong[OF assms(1,3)]) blast
- have a: "a = a1"
- apply (rule ksimplex_fix_plane_0[OF assms(2,4-5)])
- using exta(1-2,5)
- apply auto
- done
- moreover
- obtain b0 b1 where extb:
- "b0 \<in> s'"
- "b1 \<in> s'"
- "b0 \<noteq> b1"
- "\<And>x. x \<in> s' \<Longrightarrow> kle n b0 x \<and> kle n x b1"
- "\<And>i. b1 i = (if i \<in> {1..n} then b0 i + 1 else b0 i)"
- by (rule ksimplex_extrema_strong[OF goal1(1) assms(3)]) blast
- have a': "a' = b1"
- apply (rule ksimplex_fix_plane_0[OF goal1(2) assms(4), of b0])
- unfolding goal1(3)
- using assms extb goal1
- apply auto
- done
- moreover
- have "b0 = a0"
- unfolding kle_antisym[symmetric, of b0 a0 n]
- using exta extb and goal1(3)
- unfolding a a' by blast
- then have "b1 = a1"
- apply -
- apply (rule ext)
- unfolding exta(5) extb(5)
- apply auto
- done
- ultimately
- show "s' = s"
- apply -
- apply (rule *[of _ a1 b1])
- using exta(1-2) extb(1-2) goal1
- apply auto
- done
- qed
- show ?thesis
- unfolding card_1_exists
- apply -
- apply(rule ex1I[of _ s])
- unfolding mem_Collect_eq
- defer
- apply (erule conjE bexE)+
- apply (rule_tac a'=b in **)
- using assms(1,2)
- apply auto
- done
-qed
-
-lemma ksimplex_replace_1:
- assumes "ksimplex p n s"
- and "a \<in> s"
- and "n \<noteq> 0"
- and "j \<in> {1..n}"
- and "\<forall>x\<in>s - {a}. x j = p"
- shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 1"
-proof -
- have lem: "\<And>a a' s'. s' - {a'} = s - {a} \<Longrightarrow> a' = a \<Longrightarrow> a' \<in> s' \<Longrightarrow> a \<in> s \<Longrightarrow> s' = s"
- by auto
- have lem: "\<And>s' a'. ksimplex p n s' \<Longrightarrow> a'\<in>s' \<Longrightarrow> s' - {a'} = s - {a} \<Longrightarrow> s' = s"
- proof -
- case goal1
- obtain a0 a1 where exta:
- "a0 \<in> s"
- "a1 \<in> s"
- "a0 \<noteq> a1"
- "\<And>x. x \<in> s \<Longrightarrow> kle n a0 x \<and> kle n x a1"
- "\<And>i. a1 i = (if i \<in> {1..n} then a0 i + 1 else a0 i)"
- by (rule ksimplex_extrema_strong[OF assms(1,3)]) blast
- have a: "a = a0"
- apply (rule ksimplex_fix_plane_p[OF assms(1-2,4-5) exta(1,2)])
- unfolding exta
- apply auto
- done
- moreover
- obtain b0 b1 where extb:
- "b0 \<in> s'"
- "b1 \<in> s'"
- "b0 \<noteq> b1"
- "\<And>x. x \<in> s' \<Longrightarrow> kle n b0 x \<and> kle n x b1"
- "\<And>i. b1 i = (if i \<in> {1..n} then b0 i + 1 else b0 i)"
- by (rule ksimplex_extrema_strong[OF goal1(1) assms(3)]) blast
- have a': "a' = b0"
- apply (rule ksimplex_fix_plane_p[OF goal1(1-2) assms(4), of _ b1])
- unfolding goal1 extb
- using extb(1,2) assms(5)
- apply auto
- done
- moreover
- have *: "b1 = a1"
- unfolding kle_antisym[symmetric, of b1 a1 n]
- using exta extb
- using goal1(3)
- unfolding a a'
- by blast
- moreover
- have "a0 = b0"
- proof (rule ext)
- fix x
- show "a0 x = b0 x"
- using *[THEN cong, of x x]
- unfolding exta extb
- by (cases "x \<in> {1..n}") auto
- qed
- ultimately
- show "s' = s"
- apply -
- apply (rule lem[OF goal1(3) _ goal1(2) assms(2)])
- apply auto
- done
- qed
- show ?thesis
- unfolding card_1_exists
- apply (rule ex1I[of _ s])
- unfolding mem_Collect_eq
- apply rule
- apply (rule assms(1))
- apply (rule_tac x = a in bexI)
- prefer 3
- apply (erule conjE bexE)+
- apply (rule_tac a'=b in lem)
- using assms(1-2)
- apply auto
- done
-qed
-
-lemma ksimplex_replace_2:
- assumes "ksimplex p n s"
- and "a \<in> s"
- and "n \<noteq> 0"
- and "\<not> (\<exists>j\<in>{1..n}. \<forall>x\<in>s - {a}. x j = 0)"
- and "\<not> (\<exists>j\<in>{1..n}. \<forall>x\<in>s - {a}. x j = p)"
- shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 2"
- (is "card ?A = 2")
-proof -
- have lem1: "\<And>a a' s s'. s' - {a'} = s - {a} \<Longrightarrow> a' = a \<Longrightarrow> a' \<in> s' \<Longrightarrow> a \<in> s \<Longrightarrow> s' = s"
- by auto
- have lem2: "\<And>a b. a \<in> s \<Longrightarrow> b \<noteq> a \<Longrightarrow> s \<noteq> insert b (s - {a})"
- proof
- case goal1
- then have "a \<in> insert b (s - {a})"
- by auto
- then have "a \<in> s - {a}"
- unfolding insert_iff
- using goal1
- by auto
- then show False
- by auto
- qed
- obtain a0 a1 where a0a1:
- "a0 \<in> s"
- "a1 \<in> s"
- "a0 \<noteq> a1"
- "\<forall>x\<in>s. kle n a0 x \<and> kle n x a1"
- "\<forall>i. a1 i = (if i \<in> {1..n} then a0 i + 1 else a0 i)"
- by (rule ksimplex_extrema_strong[OF assms(1,3)])
- {
- assume "a = a0"
- have *: "\<And>P Q. P \<or> Q \<Longrightarrow> \<not> P \<Longrightarrow> Q"
- by auto
- have "\<exists>x\<in>s. \<not> kle n x a0"
- apply (rule_tac x=a1 in bexI)
- proof
- assume as: "kle n a1 a0"
- show False
- using kle_imp_pointwise[OF as,THEN spec[where x=1]]
- unfolding a0a1(5)[THEN spec[where x=1]]
- using assms(3)
- by auto
- qed (insert a0a1, auto)
- then have "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then a0 j + 1 else a0 j)"
- apply (rule_tac *[OF ksimplex_successor[OF assms(1-2),unfolded `a=a0`]])
- apply auto
- done
- then
- obtain a2 k where a2: "a2 \<in> s"
- and k: "k \<in> {1..n}" "\<forall>j. a2 j = (if j = k then a0 j + 1 else a0 j)"
- by blast
- def a3 \<equiv> "\<lambda>j. if j = k then a1 j + 1 else a1 j"
- have "a3 \<notin> s"
- proof
- assume "a3\<in>s"
- then have "kle n a3 a1"
- using a0a1(4) by auto
- then show False
- apply (drule_tac kle_imp_pointwise)
- unfolding a3_def
- apply (erule_tac x = k in allE)
- apply auto
- done
- qed
- then have "a3 \<noteq> a0" and "a3 \<noteq> a1"
- using a0a1 by auto
- have "a2 \<noteq> a0"
- using k(2)[THEN spec[where x=k]] by auto
- have lem3: "\<And>x. x \<in> (s - {a0}) \<Longrightarrow> kle n a2 x"
- proof (rule ccontr)
- case goal1
- then have as: "x \<in> s" "x \<noteq> a0"
- by auto
- have "kle n a2 x \<or> kle n x a2"
- using ksimplexD(6)[OF assms(1)] and as `a2 \<in> s`
- by auto
- moreover
- have "kle n a0 x"
- using a0a1(4) as by auto
- ultimately have "x = a0 \<or> x = a2"
- apply -
- apply (rule kle_adjacent[OF k(2)])
- using goal1(2)
- apply auto
- done
- then have "x = a2"
- using as by auto
- then show False
- using goal1(2)
- using kle_refl
- by auto
- qed
- let ?s = "insert a3 (s - {a0})"
- have "ksimplex p n ?s"
- apply (rule ksimplexI)
- apply (rule_tac[2-] ballI)
- apply (rule_tac[4] ballI)
- proof -
- show "card ?s = n + 1"
- using ksimplexD(2-3)[OF assms(1)]
- using `a3 \<noteq> a0` `a3 \<notin> s` `a0 \<in> s`
- by (auto simp add: card_insert_if)
- fix x
- assume x: "x \<in> insert a3 (s - {a0})"
- show "\<forall>j. x j \<le> p"
- proof
- fix j
- show "x j \<le> p"
- proof (cases "x = a3")
- case False
- then show ?thesis
- using x ksimplexD(4)[OF assms(1)] by auto
- next
- case True
- show ?thesis unfolding True
- proof (cases "j = k")
- case False
- then show "a3 j \<le> p"
- unfolding True a3_def
- using `a1 \<in> s` ksimplexD(4)[OF assms(1)]
- by auto
- next
- obtain a4 where a4: "a4 \<in> s - {a}" "a4 k \<noteq> p"
- using assms(5) k(1) by blast
- have "a2 k \<le> a4 k"
- using lem3[OF a4(1)[unfolded `a = a0`],THEN kle_imp_pointwise]
- by auto
- also have "\<dots> < p"
- using ksimplexD(4)[OF assms(1),rule_format,of a4 k]
- using a4 by auto
- finally have *: "a0 k + 1 < p"
- unfolding k(2)[rule_format]
- by auto
- case True
- then show "a3 j \<le>p"
- unfolding a3_def
- unfolding a0a1(5)[rule_format]
- using k(1) k(2)assms(5)
- using *
- by simp
- qed
- qed
- qed
- show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p"
- proof (rule, rule)
- fix j :: nat
- assume j: "j \<notin> {1..n}"
- show "x j = p"
- proof (cases "x = a3")
- case False
- then show ?thesis
- using j x ksimplexD(5)[OF assms(1)]
- by auto
- next
- case True
- show ?thesis
- unfolding True a3_def
- using j k(1)
- using ksimplexD(5)[OF assms(1),rule_format,OF `a1\<in>s` j]
- by auto
- qed
- qed
- fix y
- assume y: "y \<in> insert a3 (s - {a0})"
- have lem4: "\<And>x. x\<in>s \<Longrightarrow> x \<noteq> a0 \<Longrightarrow> kle n x a3"
- proof -
- case goal1
- obtain kk where kk:
- "kk \<subseteq> {1..n}"
- "\<forall>j. a1 j = x j + (if j \<in> kk then 1 else 0)"
- using a0a1(4)[rule_format, OF `x\<in>s`,THEN conjunct2,unfolded kle_def]
- by blast
- have "k \<notin> kk"
- proof
- assume "k \<in> kk"
- then have "a1 k = x k + 1"
- using kk by auto
- then have "a0 k = x k"
- unfolding a0a1(5)[rule_format] using k(1) by auto
- then have "a2 k = x k + 1"
- unfolding k(2)[rule_format] by auto
- moreover
- have "a2 k \<le> x k"
- using lem3[of x,THEN kle_imp_pointwise] goal1 by auto
- ultimately show False
- by auto
- qed
- then show ?case
- unfolding kle_def
- apply (rule_tac x="insert k kk" in exI)
- using kk(1)
- unfolding a3_def kle_def kk(2)[rule_format]
- using k(1)
- apply auto
- done
- qed
- show "kle n x y \<or> kle n y x"
- proof (cases "y = a3")
- case True
- show ?thesis
- unfolding True
- apply (cases "x = a3")
- defer
- apply (rule disjI1, rule lem4)
- using x
- apply auto
- done
- next
- case False
- show ?thesis
- proof (cases "x = a3")
- case True
- show ?thesis
- unfolding True
- apply (rule disjI2)
- apply (rule lem4)
- using y False
- apply auto
- done
- next
- case False
- then show ?thesis
- apply (rule_tac ksimplexD(6)[OF assms(1),rule_format])
- using x y `y \<noteq> a3`
- apply auto
- done
- qed
- qed
- qed
- then have "insert a3 (s - {a0}) \<in> ?A"
- unfolding mem_Collect_eq
- apply -
- apply rule
- apply assumption
- apply (rule_tac x = "a3" in bexI)
- unfolding `a = a0`
- using `a3 \<notin> s`
- apply auto
- done
- moreover
- have "s \<in> ?A"
- using assms(1,2) by auto
- ultimately have "?A \<supseteq> {s, insert a3 (s - {a0})}"
- by auto
- moreover
- have "?A \<subseteq> {s, insert a3 (s - {a0})}"
- apply rule
- unfolding mem_Collect_eq
- proof (erule conjE)
- fix s'
- assume as: "ksimplex p n s'"
- assume "\<exists>b\<in>s'. s' - {b} = s - {a}"
- then obtain a' where a': "a' \<in> s'" "s' - {a'} = s - {a}" ..
- obtain a_min a_max where min_max:
- "a_min \<in> s'"
- "a_max \<in> s'"
- "a_min \<noteq> a_max"
- "\<forall>x\<in>s'. kle n a_min x \<and> kle n x a_max"
- "\<forall>i. a_max i = (if i \<in> {1..n} then a_min i + 1 else a_min i)"
- by (rule ksimplex_extrema_strong[OF as assms(3)])
- have *: "\<forall>x\<in>s' - {a'}. x k = a2 k"
- unfolding a'
- proof
- fix x
- assume x: "x \<in> s - {a}"
- then have "kle n a2 x"
- apply -
- apply (rule lem3)
- using `a = a0`
- apply auto
- done
- then have "a2 k \<le> x k"
- apply (drule_tac kle_imp_pointwise)
- apply auto
- done
- moreover
- have "x k \<le> a2 k"
- unfolding k(2)[rule_format]
- using a0a1(4)[rule_format,of x, THEN conjunct1]
- unfolding kle_def using x
- by auto
- ultimately show "x k = a2 k"
- by auto
- qed
- have **: "a' = a_min \<or> a' = a_max"
- apply (rule ksimplex_fix_plane[OF a'(1) k(1) *])
- using min_max
- apply auto
- done
- show "s' \<in> {s, insert a3 (s - {a0})}"
- proof (cases "a' = a_min")
- case True
- have "a_max = a1"
- unfolding kle_antisym[symmetric,of a_max a1 n]
- apply rule
- apply (rule a0a1(4)[rule_format,THEN conjunct2])
- defer
- proof (rule min_max(4)[rule_format,THEN conjunct2])
- show "a1 \<in> s'"
- using a'
- unfolding `a = a0`
- using a0a1
- by auto
- show "a_max \<in> s"
- proof (rule ccontr)
- assume "\<not> ?thesis"
- then have "a_max = a'"
- using a' min_max by auto
- then show False
- unfolding True using min_max by auto
- qed
- qed
- then have "\<forall>i. a_max i = a1 i"
- by auto
- then have "a' = a"
- unfolding True `a = a0`
- apply -
- apply (subst fun_eq_iff)
- apply rule
- apply (erule_tac x=x in allE)
- unfolding a0a1(5)[rule_format] min_max(5)[rule_format]
- proof -
- case goal1
- then show ?case
- by (cases "x \<in> {1..n}") auto
- qed
- then have "s' = s"
- apply -
- apply (rule lem1[OF a'(2)])
- using `a \<in> s` `a' \<in> s'`
- apply auto
- done
- then show ?thesis
- by auto
- next
- case False
- then have as: "a' = a_max"
- using ** by auto
- have "a_min = a2"
- unfolding kle_antisym[symmetric, of _ _ n]
- apply rule
- apply (rule min_max(4)[rule_format,THEN conjunct1])
- defer
- proof (rule lem3)
- show "a_min \<in> s - {a0}"
- unfolding a'(2)[symmetric,unfolded `a = a0`]
- unfolding as
- using min_max(1-3)
- by auto
- have "a2 \<noteq> a"
- unfolding `a = a0`
- using k(2)[rule_format,of k]
- by auto
- then have "a2 \<in> s - {a}"
- using a2 by auto
- then show "a2 \<in> s'"
- unfolding a'(2)[symmetric] by auto
- qed
- then have "\<forall>i. a_min i = a2 i"
- by auto
- then have "a' = a3"
- unfolding as `a = a0`
- apply (subst fun_eq_iff)
- apply rule
- apply (erule_tac x=x in allE)
- unfolding a0a1(5)[rule_format] min_max(5)[rule_format]
- unfolding a3_def k(2)[rule_format]
- unfolding a0a1(5)[rule_format]
- proof -
- case goal1
- show ?case
- unfolding goal1
- apply (cases "x \<in> {1..n}")
- defer
- apply (cases "x = k")
- using `k \<in> {1..n}`
- apply auto
- done
- qed
- then have "s' = insert a3 (s - {a0})"
- apply -
- apply (rule lem1)
- defer
- apply assumption
- apply (rule a'(1))
- unfolding a' `a = a0`
- using `a3 \<notin> s`
- apply auto
- done
- then show ?thesis by auto
- qed
- qed
- ultimately have *: "?A = {s, insert a3 (s - {a0})}"
- by blast
- have "s \<noteq> insert a3 (s - {a0})"
- using `a3 \<notin> s` by auto
- then have ?thesis
- unfolding * by auto
- }
- moreover
- {
- assume "a = a1"
- have *: "\<And>P Q. P \<or> Q \<Longrightarrow> \<not> P \<Longrightarrow> Q"
- by auto
- have "\<exists>x\<in>s. \<not> kle n a1 x"
- apply (rule_tac x=a0 in bexI)
- proof
- assume as: "kle n a1 a0"
- show False
- using kle_imp_pointwise[OF as,THEN spec[where x=1]]
- unfolding a0a1(5)[THEN spec[where x=1]]
- using assms(3)
- by auto
- qed (insert a0a1, auto)
- then have "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. a1 j = (if j = k then y j + 1 else y j)"
- apply (rule_tac *[OF ksimplex_predecessor[OF assms(1-2),unfolded `a=a1`]])
- apply auto
- done
- then
- obtain a2 k where a2: "a2 \<in> s"
- and k: "k \<in> {1..n}" "\<forall>j. a1 j = (if j = k then a2 j + 1 else a2 j)"
- by blast
- def a3 \<equiv> "\<lambda>j. if j = k then a0 j - 1 else a0 j"
- have "a2 \<noteq> a1"
- using k(2)[THEN spec[where x=k]] by auto
- have lem3: "\<And>x. x \<in> s - {a1} \<Longrightarrow> kle n x a2"
- proof (rule ccontr)
- case goal1
- then have as: "x \<in> s" "x \<noteq> a1" by auto
- have "kle n a2 x \<or> kle n x a2"
- using ksimplexD(6)[OF assms(1)] and as `a2\<in>s`
- by auto
- moreover
- have "kle n x a1"
- using a0a1(4) as by auto
- ultimately have "x = a2 \<or> x = a1"
- apply -
- apply (rule kle_adjacent[OF k(2)])
- using goal1(2)
- apply auto
- done
- then have "x = a2"
- using as by auto
- then show False
- using goal1(2) using kle_refl by auto
- qed
- have "a0 k \<noteq> 0"
- proof -
- obtain a4 where a4: "a4 \<in> s - {a}" "a4 k \<noteq> 0"
- using assms(4) `k\<in>{1..n}` by blast
- have "a4 k \<le> a2 k"
- using lem3[OF a4(1)[unfolded `a=a1`],THEN kle_imp_pointwise]
- by auto
- moreover have "a4 k > 0"
- using a4 by auto
- ultimately have "a2 k > 0"
- by auto
- then have "a1 k > 1"
- unfolding k(2)[rule_format] by simp
- then show ?thesis
- unfolding a0a1(5)[rule_format] using k(1) by simp
- qed
- then have lem4: "\<forall>j. a0 j = (if j = k then a3 j + 1 else a3 j)"
- unfolding a3_def by simp
- have "\<not> kle n a0 a3"
- apply (rule notI)
- apply (drule kle_imp_pointwise)
- unfolding lem4[rule_format]
- apply (erule_tac x=k in allE)
- apply auto
- done
- then have "a3 \<notin> s"
- using a0a1(4) by auto
- then have "a3 \<noteq> a1" "a3 \<noteq> a0"
- using a0a1 by auto
- let ?s = "insert a3 (s - {a1})"
- have "ksimplex p n ?s"
- apply (rule ksimplexI)
- proof (rule_tac[2-] ballI,rule_tac[4] ballI)
- show "card ?s = n+1"
- using ksimplexD(2-3)[OF assms(1)]
- using `a3 \<noteq> a0` `a3 \<notin> s` `a1 \<in> s`
- by (auto simp add:card_insert_if)
- fix x
- assume x: "x \<in> insert a3 (s - {a1})"
- show "\<forall>j. x j \<le> p"
- proof
- fix j
- show "x j \<le> p"
- proof (cases "x = a3")
- case False
- then show ?thesis
- using x ksimplexD(4)[OF assms(1)] by auto
- next
- case True
- show ?thesis
- unfolding True
- proof (cases "j = k")
- case False
- then show "a3 j \<le> p"
- unfolding True a3_def
- using `a0 \<in> s` ksimplexD(4)[OF assms(1)]
- by auto
- next
- case True
- obtain a4 where a4: "a4 \<in> s - {a}" "a4 k \<noteq> p"
- using assms(5) k(1) by blast
- have "a3 k \<le> a0 k"
- unfolding lem4[rule_format] by auto
- also have "\<dots> \<le> p"
- using ksimplexD(4)[OF assms(1),rule_format, of a0 k] a0a1
- by auto
- finally show "a3 j \<le> p"
- unfolding True by auto
- qed
- qed
- qed
- show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p"
- proof (rule, rule)
- fix j :: nat
- assume j: "j \<notin> {1..n}"
- show "x j = p"
- proof (cases "x = a3")
- case False
- then show ?thesis
- using j x ksimplexD(5)[OF assms(1)] by auto
- next
- case True
- show ?thesis
- unfolding True a3_def
- using j k(1)
- using ksimplexD(5)[OF assms(1),rule_format,OF `a0\<in>s` j]
- by auto
- qed
- qed
- fix y
- assume y: "y \<in> insert a3 (s - {a1})"
- have lem4: "\<And>x. x \<in> s \<Longrightarrow> x \<noteq> a1 \<Longrightarrow> kle n a3 x"
- proof -
- case goal1
- then have *: "x\<in>s - {a1}"
- by auto
- have "kle n a3 a2"
- proof -
- have "kle n a0 a1"
- using a0a1 by auto
- then obtain kk where "kk \<subseteq> {1..n}" "(\<forall>j. a1 j = a0 j + (if j \<in> kk then 1 else 0))"
- unfolding kle_def by blast
- then show ?thesis
- unfolding kle_def
- apply (rule_tac x=kk in exI)
- unfolding lem4[rule_format] k(2)[rule_format]
- apply rule
- defer
- proof rule
- case goal1
- then show ?case
- apply -
- apply (erule_tac[!] x=j in allE)
- apply (cases "j \<in> kk")
- apply (case_tac[!] "j=k")
- apply auto
- done
- qed auto
- qed
- moreover
- have "kle n a3 a0"
- unfolding kle_def lem4[rule_format]
- apply (rule_tac x="{k}" in exI)
- using k(1)
- apply auto
- done
- ultimately
- show ?case
- apply -
- apply (rule kle_between_l[of _ a0 _ a2])
- using lem3[OF *]
- using a0a1(4)[rule_format,OF goal1(1)]
- apply auto
- done
- qed
- show "kle n x y \<or> kle n y x"
- proof (cases "y = a3")
- case True
- show ?thesis
- unfolding True
- apply (cases "x = a3")
- defer
- apply (rule disjI2)
- apply (rule lem4)
- using x
- apply auto
- done
- next
- case False
- show ?thesis
- proof (cases "x = a3")
- case True
- show ?thesis
- unfolding True
- apply (rule disjI1)
- apply (rule lem4)
- using y False
- apply auto
- done
- next
- case False
- then show ?thesis
- apply (rule_tac ksimplexD(6)[OF assms(1),rule_format])
- using x y `y \<noteq> a3`
- apply auto
- done
- qed
- qed
- qed
- then have "insert a3 (s - {a1}) \<in> ?A"
- unfolding mem_Collect_eq
- apply -
- apply (rule, assumption)
- apply (rule_tac x = "a3" in bexI)
- unfolding `a = a1`
- using `a3 \<notin> s`
- apply auto
- done
- moreover
- have "s \<in> ?A"
- using assms(1,2) by auto
- ultimately have "?A \<supseteq> {s, insert a3 (s - {a1})}"
- by auto
- moreover have "?A \<subseteq> {s, insert a3 (s - {a1})}"
- apply rule
- unfolding mem_Collect_eq
- proof (erule conjE)
- fix s'
- assume as: "ksimplex p n s'"
- assume "\<exists>b\<in>s'. s' - {b} = s - {a}"
- then obtain a' where a': "a' \<in> s'" "s' - {a'} = s - {a}" ..
- obtain a_min a_max where min_max:
- "a_min \<in> s'"
- "a_max \<in> s'"
- "a_min \<noteq> a_max"
- "\<forall>x\<in>s'. kle n a_min x \<and> kle n x a_max"
- "\<forall>i. a_max i = (if i \<in> {1..n} then a_min i + 1 else a_min i)"
- by (rule ksimplex_extrema_strong[OF as assms(3)])
- have *: "\<forall>x\<in>s' - {a'}. x k = a2 k" unfolding a'
- proof
- fix x
- assume x: "x \<in> s - {a}"
- then have "kle n x a2"
- apply -
- apply (rule lem3)
- using `a = a1`
- apply auto
- done
- then have "x k \<le> a2 k"
- apply (drule_tac kle_imp_pointwise)
- apply auto
- done
- moreover
- {
- have "a2 k \<le> a0 k"
- using k(2)[rule_format,of k]
- unfolding a0a1(5)[rule_format]
- using k(1)
- by simp
- also have "\<dots> \<le> x k"
- using a0a1(4)[rule_format,of x,THEN conjunct1,THEN kle_imp_pointwise] x
- by auto
- finally have "a2 k \<le> x k" .
- }
- ultimately show "x k = a2 k"
- by auto
- qed
- have **: "a' = a_min \<or> a' = a_max"
- apply (rule ksimplex_fix_plane[OF a'(1) k(1) *])
- using min_max
- apply auto
- done
- have "a2 \<noteq> a1"
- proof
- assume as: "a2 = a1"
- show False
- using k(2)
- unfolding as
- apply (erule_tac x = k in allE)
- apply auto
- done
- qed
- then have a2': "a2 \<in> s' - {a'}"
- unfolding a'
- using a2
- unfolding `a = a1`
- by auto
- show "s' \<in> {s, insert a3 (s - {a1})}"
- proof (cases "a' = a_min")
- case True
- have "a_max \<in> s - {a1}"
- using min_max
- unfolding a'(2)[unfolded `a=a1`,symmetric] True
- by auto
- then have "a_max = a2"
- unfolding kle_antisym[symmetric,of a_max a2 n]
- apply -
- apply rule
- apply (rule lem3)
- apply assumption
- apply (rule min_max(4)[rule_format,THEN conjunct2])
- using a2'
- apply auto
- done
- then have a_max: "\<forall>i. a_max i = a2 i"
- by auto
- have *: "\<forall>j. a2 j = (if j \<in> {1..n} then a3 j + 1 else a3 j)"
- using k(2)
- unfolding lem4[rule_format] a0a1(5)[rule_format]
- apply -
- apply rule
- apply (erule_tac x=j in allE)
- proof -
- case goal1
- then show ?case by (cases "j \<in> {1..n}", case_tac[!] "j = k") auto
- qed
- have "\<forall>i. a_min i = a3 i"
- using a_max
- apply -
- apply rule
- apply (erule_tac x=i in allE)
- unfolding min_max(5)[rule_format] *[rule_format]
- proof -
- case goal1
- then show ?case
- by (cases "i \<in> {1..n}") auto
- qed
- then have "a_min = a3"
- unfolding fun_eq_iff .
- then have "s' = insert a3 (s - {a1})"
- using a'
- unfolding `a = a1` True
- by auto
- then show ?thesis
- by auto
- next
- case False
- then have as: "a' = a_max"
- using ** by auto
- have "a_min = a0"
- unfolding kle_antisym[symmetric,of _ _ n]
- apply rule
- apply (rule min_max(4)[rule_format,THEN conjunct1])
- defer
- apply (rule a0a1(4)[rule_format,THEN conjunct1])
- proof -
- have "a_min \<in> s - {a1}"
- using min_max(1,3)
- unfolding a'(2)[symmetric,unfolded `a=a1`] as
- by auto
- then show "a_min \<in> s"
- by auto
- have "a0 \<in> s - {a1}"
- using a0a1(1-3) by auto
- then show "a0 \<in> s'"
- unfolding a'(2)[symmetric,unfolded `a=a1`]
- by auto
- qed
- then have "\<forall>i. a_max i = a1 i"
- unfolding a0a1(5)[rule_format] min_max(5)[rule_format]
- by auto
- then have "s' = s"
- apply -
- apply (rule lem1[OF a'(2)])
- using `a \<in> s` `a' \<in> s'`
- unfolding as `a = a1`
- unfolding fun_eq_iff
- apply auto
- done
- then show ?thesis
- by auto
- qed
- qed
- ultimately have *: "?A = {s, insert a3 (s - {a1})}"
- by blast
- have "s \<noteq> insert a3 (s - {a1})"
- using `a3\<notin>s` by auto
- then have ?thesis
- unfolding * by auto
- }
- moreover
- {
- assume as: "a \<noteq> a0" "a \<noteq> a1"
- have "\<not> (\<forall>x\<in>s. kle n a x)"
- proof
- case goal1
- have "a = a0"
- unfolding kle_antisym[symmetric,of _ _ n]
- apply rule
- using goal1 a0a1 assms(2)
- apply auto
- done
- then show False
- using as by auto
- qed
- then have "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. a j = (if j = k then y j + 1 else y j)"
- using ksimplex_predecessor[OF assms(1-2)]
- by blast
- then obtain u k where u: "u \<in> s"
- and k: "k \<in> {1..n}" "\<And>j. a j = (if j = k then u j + 1 else u j)"
- by blast
- have "\<not> (\<forall>x\<in>s. kle n x a)"
- proof
- case goal1
- have "a = a1"
- unfolding kle_antisym[symmetric,of _ _ n]
- apply rule
- using goal1 a0a1 assms(2)
- apply auto
- done
- then show False
- using as by auto
- qed
- then have "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then a j + 1 else a j)"
- using ksimplex_successor[OF assms(1-2)] by blast
- then obtain v l where v: "v \<in> s"
- and l: "l \<in> {1..n}" "\<And>j. v j = (if j = l then a j + 1 else a j)"
- by blast
- def a' \<equiv> "\<lambda>j. if j = l then u j + 1 else u j"
- have kl: "k \<noteq> l"
- proof
- assume "k = l"
- have *: "\<And>P. (if P then (1::nat) else 0) \<noteq> 2"
- by auto
- then show False
- using ksimplexD(6)[OF assms(1),rule_format,OF u v]
- unfolding kle_def
- unfolding l(2) k(2) `k = l`
- apply -
- apply (erule disjE)
- apply (erule_tac[!] exE conjE)+
- apply (erule_tac[!] x = l in allE)+
- apply (auto simp add: *)
- done
- qed
- then have aa': "a' \<noteq> a"
- apply -
- apply rule
- unfolding fun_eq_iff
- unfolding a'_def k(2)
- apply (erule_tac x=l in allE)
- apply auto
- done
- have "a' \<notin> s"
- apply rule
- apply (drule ksimplexD(6)[OF assms(1),rule_format,OF `a\<in>s`])
- proof (cases "kle n a a'")
- case goal2
- then have "kle n a' a"
- by auto
- then show False
- apply (drule_tac kle_imp_pointwise)
- apply (erule_tac x=l in allE)
- unfolding a'_def k(2)
- using kl
- apply auto
- done
- next
- case True
- then show False
- apply (drule_tac kle_imp_pointwise)
- apply (erule_tac x=k in allE)
- unfolding a'_def k(2)
- using kl
- apply auto
- done
- qed
- have kle_uv: "kle n u a" "kle n u a'" "kle n a v" "kle n a' v"
- unfolding kle_def
- apply -
- apply (rule_tac[1] x="{k}" in exI,rule_tac[2] x="{l}" in exI)
- apply (rule_tac[3] x="{l}" in exI,rule_tac[4] x="{k}" in exI)
- unfolding l(2) k(2) a'_def
- using l(1) k(1)
- apply auto
- done
- have uxv: "\<And>x. kle n u x \<Longrightarrow> kle n x v \<Longrightarrow> x = u \<or> x = a \<or> x = a' \<or> x = v"
- proof -
- case goal1
- then show ?case
- proof (cases "x k = u k", case_tac[!] "x l = u l")
- assume as: "x l = u l" "x k = u k"
- have "x = u"
- unfolding fun_eq_iff
- using goal1(2)[THEN kle_imp_pointwise,unfolded l(2)]
- unfolding k(2)
- apply -
- using goal1(1)[THEN kle_imp_pointwise]
- apply -
- apply rule
- apply (erule_tac x=xa in allE)+
- proof -
- case goal1
- then show ?case
- apply (cases "x = l")
- apply (case_tac[!] "x = k")
- using as
- by auto
- qed
- then show ?case
- by auto
- next
- assume as: "x l \<noteq> u l" "x k = u k"
- have "x = a'"
- unfolding fun_eq_iff
- unfolding a'_def
- using goal1(2)[THEN kle_imp_pointwise]
- unfolding l(2) k(2)
- using goal1(1)[THEN kle_imp_pointwise]
- apply -
- apply rule
- apply (erule_tac x = xa in allE)+
- proof -
- case goal1
- then show ?case
- apply (cases "x = l")
- apply (case_tac[!] "x = k")
- using as
- apply auto
- done
- qed
- then show ?case by auto
- next
- assume as: "x l = u l" "x k \<noteq> u k"
- have "x = a"
- unfolding fun_eq_iff
- using goal1(2)[THEN kle_imp_pointwise]
- unfolding l(2) k(2)
- using goal1(1)[THEN kle_imp_pointwise]
- apply -
- apply rule
- apply (erule_tac x=xa in allE)+
- proof -
- case goal1
- then show ?case
- apply (cases "x = l")
- apply (case_tac[!] "x = k")
- using as
- apply auto
- done
- qed
- then show ?case
- by auto
- next
- assume as: "x l \<noteq> u l" "x k \<noteq> u k"
- have "x = v"
- unfolding fun_eq_iff
- using goal1(2)[THEN kle_imp_pointwise]
- unfolding l(2) k(2)
- using goal1(1)[THEN kle_imp_pointwise]
- apply -
- apply rule
- apply (erule_tac x=xa in allE)+
- proof -
- case goal1
- then show ?case
- apply (cases "x = l")
- apply (case_tac[!] "x = k")
- using as `k \<noteq> l`
- apply auto
- done
- qed
- then show ?case by auto
- qed
- qed
- have uv: "kle n u v"
- apply (rule kle_trans[OF kle_uv(1,3)])
- using ksimplexD(6)[OF assms(1)]
- using u v
- apply auto
- done
- have lem3: "\<And>x. x \<in> s \<Longrightarrow> kle n v x \<Longrightarrow> kle n a' x"
- apply (rule kle_between_r[of _ u _ v])
- prefer 3
- apply (rule kle_trans[OF uv])
- defer
- apply (rule ksimplexD(6)[OF assms(1), rule_format])
- using kle_uv `u \<in> s`
- apply auto
- done
- have lem4: "\<And>x. x \<in> s \<Longrightarrow> kle n x u \<Longrightarrow> kle n x a'"
- apply (rule kle_between_l[of _ u _ v])
- prefer 4
- apply (rule kle_trans[OF _ uv])
- defer
- apply (rule ksimplexD(6)[OF assms(1), rule_format])
- using kle_uv `v \<in> s`
- apply auto
- done
- have lem5: "\<And>x. x \<in> s \<Longrightarrow> x \<noteq> a \<Longrightarrow> kle n x a' \<or> kle n a' x"
- proof -
- case goal1
- then show ?case
- proof (cases "kle n v x \<or> kle n x u")
- case True
- then show ?thesis
- using goal1 by (auto intro: lem3 lem4)
- next
- case False
- then have *: "kle n u x" "kle n x v"
- using ksimplexD(6)[OF assms(1)]
- using goal1 `u \<in> s` `v \<in> s`
- by auto
- show ?thesis
- using uxv[OF *]
- using kle_uv
- using goal1
- by auto
- qed
- qed
- have "ksimplex p n (insert a' (s - {a}))"
- apply (rule ksimplexI)
- apply (rule_tac[2-] ballI)
- apply (rule_tac[4] ballI)
- proof -
- show "card (insert a' (s - {a})) = n + 1"
- using ksimplexD(2-3)[OF assms(1)]
- using `a' \<noteq> a` `a' \<notin> s` `a \<in> s`
- by (auto simp add:card_insert_if)
- fix x
- assume x: "x \<in> insert a' (s - {a})"
- show "\<forall>j. x j \<le> p"
- proof
- fix j
- show "x j \<le> p"
- proof (cases "x = a'")
- case False
- then show ?thesis
- using x ksimplexD(4)[OF assms(1)] by auto
- next
- case True
- show ?thesis
- unfolding True
- proof (cases "j = l")
- case False
- then show "a' j \<le>p"
- unfolding True a'_def
- using `u\<in>s` ksimplexD(4)[OF assms(1)]
- by auto
- next
- case True
- have *: "a l = u l" "v l = a l + 1"
- using k(2)[of l] l(2)[of l] `k \<noteq> l`
- by auto
- have "u l + 1 \<le> p"
- unfolding *[symmetric]
- using ksimplexD(4)[OF assms(1)]
- using `v \<in> s`
- by auto
- then show "a' j \<le>p"
- unfolding a'_def True
- by auto
- qed
- qed
- qed
- show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p"
- proof (rule, rule)
- fix j :: nat
- assume j: "j \<notin> {1..n}"
- show "x j = p"
- proof (cases "x = a'")
- case False
- then show ?thesis
- using j x ksimplexD(5)[OF assms(1)] by auto
- next
- case True
- show ?thesis
- unfolding True a'_def
- using j l(1)
- using ksimplexD(5)[OF assms(1),rule_format,OF `u\<in>s` j]
- by auto
- qed
- qed
- fix y
- assume y: "y \<in> insert a' (s - {a})"
- show "kle n x y \<or> kle n y x"
- proof (cases "y = a'")
- case True
- show ?thesis
- unfolding True
- apply (cases "x = a'")
- defer
- apply (rule lem5)
- using x
- apply auto
- done
- next
- case False
- show ?thesis
- proof (cases "x = a'")
- case True
- show ?thesis
- unfolding True
- using lem5[of y] using y by auto
- next
- case False
- then show ?thesis
- apply (rule_tac ksimplexD(6)[OF assms(1),rule_format])
- using x y `y \<noteq> a'`
- apply auto
- done
- qed
- qed
- qed
- then have "insert a' (s - {a}) \<in> ?A"
- unfolding mem_Collect_eq
- apply -
- apply rule
- apply assumption
- apply (rule_tac x = "a'" in bexI)
- using aa' `a' \<notin> s`
- apply auto
- done
- moreover
- have "s \<in> ?A"
- using assms(1,2) by auto
- ultimately have "?A \<supseteq> {s, insert a' (s - {a})}"
- by auto
- moreover
- have "?A \<subseteq> {s, insert a' (s - {a})}"
- apply rule
- unfolding mem_Collect_eq
- proof (erule conjE)
- fix s'
- assume as: "ksimplex p n s'"
- assume "\<exists>b\<in>s'. s' - {b} = s - {a}"
- then obtain a'' where a'': "a'' \<in> s'" "s' - {a''} = s - {a}"
- by blast
- have "u \<noteq> v"
- unfolding fun_eq_iff l(2) k(2) by auto
- then have uv': "\<not> kle n v u"
- using uv using kle_antisym by auto
- have "u \<noteq> a" "v \<noteq> a"
- unfolding fun_eq_iff k(2) l(2) by auto
- then have uvs': "u \<in> s'" "v \<in> s'"
- using `u \<in> s` `v \<in> s` using a'' by auto
- have lem6: "a \<in> s' \<or> a' \<in> s'"
- proof (cases "\<forall>x\<in>s'. kle n x u \<or> kle n v x")
- case False
- then obtain w where w: "w \<in> s'" "\<not> (kle n w u \<or> kle n v w)"
- by blast
- then have "kle n u w" "kle n w v"
- using ksimplexD(6)[OF as] uvs' by auto
- then have "w = a' \<or> w = a"
- using uxv[of w] uvs' w by auto
- then show ?thesis
- using w by auto
- next
- case True
- have "\<not> (\<forall>x\<in>s'. kle n x u)"
- unfolding ball_simps
- apply (rule_tac x=v in bexI)
- using uv `u \<noteq> v`
- unfolding kle_antisym [of n u v,symmetric]
- using `v \<in> s'`
- apply auto
- done
- then have "\<exists>y\<in>s'. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then u j + 1 else u j)"
- using ksimplex_successor[OF as `u\<in>s'`]
- by blast
- then obtain w where
- w: "w \<in> s'" "\<exists>k\<in>{1..n}. \<forall>j. w j = (if j = k then u j + 1 else u j)"
- ..
- from this(2) obtain kk where kk:
- "kk \<in> {1..n}"
- "\<And>j. w j = (if j = kk then u j + 1 else u j)"
- by blast
- have "\<not> kle n w u"
- apply -
- apply rule
- apply (drule kle_imp_pointwise)
- apply (erule_tac x = kk in allE)
- unfolding kk
- apply auto
- done
- then have *: "kle n v w"
- using True[rule_format,OF w(1)]
- by auto
- then have False
- proof (cases "kk = l")
- case False
- then show False using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)]
- apply (erule_tac x=l in allE)
- using `k \<noteq> l`
- apply auto
- done
- next
- case True
- then have "kk \<noteq> k" using `k \<noteq> l` by auto
- then show False
- using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)]
- apply (erule_tac x=k in allE)
- using `k \<noteq> l`
- apply auto
- done
- qed
- then show ?thesis
- by auto
- qed
- then show "s' \<in> {s, insert a' (s - {a})}"
- proof (cases "a \<in> s'")
- case True
- then have "s' = s"
- apply -
- apply (rule lem1[OF a''(2)])
- using a'' `a \<in> s`
- apply auto
- done
- then show ?thesis
- by auto
- next
- case False
- then have "a' \<in> s'"
- using lem6 by auto
- then have "s' = insert a' (s - {a})"
- apply -
- apply (rule lem1[of _ a'' _ a'])
- unfolding a''(2)[symmetric]
- using a'' and `a' \<notin> s`
- by auto
- then show ?thesis
- by auto
- qed
- qed
- ultimately have *: "?A = {s, insert a' (s - {a})}"
- by blast
- have "s \<noteq> insert a' (s - {a})"
- using `a'\<notin>s` by auto
- then have ?thesis
- unfolding * by auto
- }
+ have "(\<Sum>s | s \<in> S \<and> \<not> compo s. nF s) + (\<Sum>s | s \<in> S \<and> compo s. nF s) = (\<Sum>s\<in>S. nF s)"
+ by (subst setsum_Un_disjoint[symmetric]) (auto intro!: setsum_cong)
+ also have "\<dots> = (\<Sum>s\<in>S. card {f \<in> {f\<in>F. compo' f \<and> bnd f}. face f s}) +
+ (\<Sum>s\<in>S. card {f \<in> {f\<in>F. compo' f \<and> \<not> bnd f}. face f s})"
+ unfolding setsum_addf[symmetric]
+ by (subst card_Un_disjoint[symmetric])
+ (auto simp: nF_def intro!: setsum_cong arg_cong[where f=card])
+ also have "\<dots> = 1 * card {f\<in>F. compo' f \<and> bnd f} + 2 * card {f\<in>F. compo' f \<and> \<not> bnd f}"
+ using assms(4,5) by (fastforce intro!: arg_cong2[where f="op +"] setsum_multicount)
+ finally have "odd ((\<Sum>s | s \<in> S \<and> \<not> compo s. nF s) + card {s\<in>S. compo s})"
+ using assms(6,8) by simp
+ moreover have "(\<Sum>s | s \<in> S \<and> \<not> compo s. nF s) =
+ (\<Sum>s | s \<in> S \<and> \<not> compo s \<and> nF s = 0. nF s) + (\<Sum>s | s \<in> S \<and> \<not> compo s \<and> nF s = 2. nF s)"
+ using assms(7) by (subst setsum_Un_disjoint[symmetric]) (fastforce intro!: setsum_cong)+
ultimately show ?thesis
by auto
qed
+subsection {* The odd/even result for faces of complete vertices, generalized. *}
+
+lemma kuhn_complete_lemma:
+ assumes [simp]: "finite simplices"
+ and face: "\<And>f s. face f s \<longleftrightarrow> (\<exists>a\<in>s. f = s - {a})"
+ and card_s[simp]: "\<And>s. s \<in> simplices \<Longrightarrow> card s = n + 2"
+ and rl_bd: "\<And>s. s \<in> simplices \<Longrightarrow> rl ` s \<subseteq> {..Suc n}"
+ and bnd: "\<And>f s. s \<in> simplices \<Longrightarrow> face f s \<Longrightarrow> bnd f \<Longrightarrow> card {s\<in>simplices. face f s} = 1"
+ and nbnd: "\<And>f s. s \<in> simplices \<Longrightarrow> face f s \<Longrightarrow> \<not> bnd f \<Longrightarrow> card {s\<in>simplices. face f s} = 2"
+ and odd_card: "odd (card {f. (\<exists>s\<in>simplices. face f s) \<and> rl ` f = {..n} \<and> bnd f})"
+ shows "odd (card {s\<in>simplices. (rl ` s = {..Suc n})})"
+proof (rule kuhn_counting_lemma)
+ have finite_s[simp]: "\<And>s. s \<in> simplices \<Longrightarrow> finite s"
+ by (metis add_is_0 zero_neq_numeral card_infinite assms(3))
+
+ let ?F = "{f. \<exists>s\<in>simplices. face f s}"
+ have F_eq: "?F = (\<Union>s\<in>simplices. \<Union>a\<in>s. {s - {a}})"
+ by (auto simp: face)
+ show "finite ?F"
+ using `finite simplices` unfolding F_eq by auto
+
+ { fix f assume "f \<in> ?F" "bnd f" then show "card {s \<in> simplices. face f s} = 1"
+ using bnd by auto }
+
+ { fix f assume "f \<in> ?F" "\<not> bnd f" then show "card {s \<in> simplices. face f s} = 2"
+ using nbnd by auto }
+
+ show "odd (card {f \<in> {f. \<exists>s\<in>simplices. face f s}. rl ` f = {..n} \<and> bnd f})"
+ using odd_card by simp
+
+ fix s assume s[simp]: "s \<in> simplices"
+ let ?S = "{f \<in> {f. \<exists>s\<in>simplices. face f s}. face f s \<and> rl ` f = {..n}}"
+ have "?S = (\<lambda>a. s - {a}) ` {a\<in>s. rl ` (s - {a}) = {..n}}"
+ using s by (fastforce simp: face)
+ then have card_S: "card ?S = card {a\<in>s. rl ` (s - {a}) = {..n}}"
+ by (auto intro!: card_image inj_onI)
+
+ { assume rl: "rl ` s = {..Suc n}"
+ then have inj_rl: "inj_on rl s"
+ by (intro eq_card_imp_inj_on) auto
+ moreover obtain a where "rl a = Suc n" "a \<in> s"
+ by (metis atMost_iff image_iff le_Suc_eq rl)
+ ultimately have n: "{..n} = rl ` (s - {a})"
+ by (auto simp add: inj_on_image_set_diff rl)
+ have "{a\<in>s. rl ` (s - {a}) = {..n}} = {a}"
+ using inj_rl `a \<in> s` by (auto simp add: n inj_on_image_eq_iff[OF inj_rl] Diff_subset)
+ then show "card ?S = 1"
+ unfolding card_S by simp }
+
+ { assume rl: "rl ` s \<noteq> {..Suc n}"
+ show "card ?S = 0 \<or> card ?S = 2"
+ proof cases
+ assume *: "{..n} \<subseteq> rl ` s"
+ with rl rl_bd[OF s] have rl_s: "rl ` s = {..n}"
+ by (auto simp add: atMost_Suc subset_insert_iff split: split_if_asm)
+ then have "\<not> inj_on rl s"
+ by (intro pigeonhole) simp
+ then obtain a b where ab: "a \<in> s" "b \<in> s" "rl a = rl b" "a \<noteq> b"
+ by (auto simp: inj_on_def)
+ then have eq: "rl ` (s - {a}) = rl ` s"
+ by auto
+ with ab have inj: "inj_on rl (s - {a})"
+ by (intro eq_card_imp_inj_on) (auto simp add: rl_s card_Diff_singleton_if)
+
+ { fix x assume "x \<in> s" "x \<notin> {a, b}"
+ then have "rl ` s - {rl x} = rl ` ((s - {a}) - {x})"
+ by (auto simp: eq inj_on_image_set_diff[OF inj])
+ also have "\<dots> = rl ` (s - {x})"
+ using ab `x \<notin> {a, b}` by auto
+ also assume "\<dots> = rl ` s"
+ finally have False
+ using `x\<in>s` by auto }
+ moreover
+ { fix x assume "x \<in> {a, b}" with ab have "x \<in> s \<and> rl ` (s - {x}) = rl ` s"
+ by (simp add: set_eq_iff image_iff Bex_def) metis }
+ ultimately have "{a\<in>s. rl ` (s - {a}) = {..n}} = {a, b}"
+ unfolding rl_s[symmetric] by fastforce
+ with `a \<noteq> b` show "card ?S = 0 \<or> card ?S = 2"
+ unfolding card_S by simp
+ next
+ assume "\<not> {..n} \<subseteq> rl ` s"
+ then have "\<And>x. rl ` (s - {x}) \<noteq> {..n}"
+ by auto
+ then show "card ?S = 0 \<or> card ?S = 2"
+ unfolding card_S by simp
+ qed }
+qed fact
+
+locale kuhn_simplex =
+ fixes p n and base upd and s :: "(nat \<Rightarrow> nat) set"
+ assumes base: "base \<in> {..< n} \<rightarrow> {..< p}"
+ assumes base_out: "\<And>i. n \<le> i \<Longrightarrow> base i = p"
+ assumes upd: "bij_betw upd {..< n} {..< n}"
+ assumes s_pre: "s = (\<lambda>i j. if j \<in> upd`{..< i} then Suc (base j) else base j) ` {.. n}"
+begin
+
+definition "enum i j = (if j \<in> upd`{..< i} then Suc (base j) else base j)"
+
+lemma s_eq: "s = enum ` {.. n}"
+ unfolding s_pre enum_def[abs_def] ..
+
+lemma upd_space: "i < n \<Longrightarrow> upd i < n"
+ using upd by (auto dest!: bij_betwE)
+
+lemma s_space: "s \<subseteq> {..< n} \<rightarrow> {.. p}"
+proof -
+ { fix i assume "i \<le> n" then have "enum i \<in> {..< n} \<rightarrow> {.. p}"
+ proof (induct i)
+ case 0 then show ?case
+ using base by (auto simp: Pi_iff less_imp_le enum_def)
+ next
+ case (Suc i) with base show ?case
+ by (auto simp: Pi_iff Suc_le_eq less_imp_le enum_def intro: upd_space)
+ qed }
+ then show ?thesis
+ by (auto simp: s_eq)
+qed
+
+lemma inj_upd: "inj_on upd {..< n}"
+ using upd by (simp add: bij_betw_def)
+
+lemma inj_enum: "inj_on enum {.. n}"
+proof -
+ { fix x y :: nat assume "x \<noteq> y" "x \<le> n" "y \<le> n"
+ with upd have "upd ` {..< x} \<noteq> upd ` {..< y}"
+ by (subst inj_on_image_eq_iff[where C="{..< n}"]) (auto simp: bij_betw_def)
+ then have "enum x \<noteq> enum y"
+ by (auto simp add: enum_def fun_eq_iff) }
+ then show ?thesis
+ by (auto simp: inj_on_def)
+qed
+
+lemma enum_0: "enum 0 = base"
+ by (simp add: enum_def[abs_def])
+
+lemma base_in_s: "base \<in> s"
+ unfolding s_eq by (subst enum_0[symmetric]) auto
+
+lemma enum_in: "i \<le> n \<Longrightarrow> enum i \<in> s"
+ unfolding s_eq by auto
+
+lemma one_step:
+ assumes a: "a \<in> s" "j < n"
+ assumes *: "\<And>a'. a' \<in> s \<Longrightarrow> a' \<noteq> a \<Longrightarrow> a' j = p'"
+ shows "a j \<noteq> p'"
+proof
+ assume "a j = p'"
+ with * a have "\<And>a'. a' \<in> s \<Longrightarrow> a' j = p'"
+ by auto
+ then have "\<And>i. i \<le> n \<Longrightarrow> enum i j = p'"
+ unfolding s_eq by auto
+ from this[of 0] this[of n] have "j \<notin> upd ` {..< n}"
+ by (auto simp: enum_def fun_eq_iff split: split_if_asm)
+ with upd `j < n` show False
+ by (auto simp: bij_betw_def)
+qed
+
+lemma upd_inj: "i < n \<Longrightarrow> j < n \<Longrightarrow> upd i = upd j \<longleftrightarrow> i = j"
+ using upd by (auto simp: bij_betw_def inj_on_iff)
+
+lemma upd_surj: "upd ` {..< n} = {..< n}"
+ using upd by (auto simp: bij_betw_def)
+
+lemma in_upd_image: "A \<subseteq> {..< n} \<Longrightarrow> i < n \<Longrightarrow> upd i \<in> upd ` A \<longleftrightarrow> i \<in> A"
+ using inj_on_image_mem_iff[of upd "{..< n}" A i ] upd
+ by (auto simp: bij_betw_def)
+
+lemma enum_inj: "i \<le> n \<Longrightarrow> j \<le> n \<Longrightarrow> enum i = enum j \<longleftrightarrow> i = j"
+ using inj_enum by (auto simp: inj_on_iff)
+
+lemma in_enum_image: "A \<subseteq> {.. n} \<Longrightarrow> i \<le> n \<Longrightarrow> enum i \<in> enum ` A \<longleftrightarrow> i \<in> A"
+ using inj_on_image_mem_iff[OF inj_enum, of A i] by auto
+
+lemma enum_mono: "i \<le> n \<Longrightarrow> j \<le> n \<Longrightarrow> enum i \<le> enum j \<longleftrightarrow> i \<le> j"
+ by (auto simp: enum_def le_fun_def in_upd_image Ball_def[symmetric])
+
+lemma enum_strict_mono: "i \<le> n \<Longrightarrow> j \<le> n \<Longrightarrow> enum i < enum j \<longleftrightarrow> i < j"
+ using enum_mono[of i j] enum_inj[of i j] by (auto simp add: le_less)
+
+lemma chain: "a \<in> s \<Longrightarrow> b \<in> s \<Longrightarrow> a \<le> b \<or> b \<le> a"
+ by (auto simp: s_eq enum_mono)
+
+lemma less: "a \<in> s \<Longrightarrow> b \<in> s \<Longrightarrow> a i < b i \<Longrightarrow> a < b"
+ using chain[of a b] by (auto simp: less_fun_def le_fun_def not_le[symmetric])
+
+lemma enum_0_bot: "a \<in> s \<Longrightarrow> a = enum 0 \<longleftrightarrow> (\<forall>a'\<in>s. a \<le> a')"
+ unfolding s_eq by (auto simp: enum_mono Ball_def)
+
+lemma enum_n_top: "a \<in> s \<Longrightarrow> a = enum n \<longleftrightarrow> (\<forall>a'\<in>s. a' \<le> a)"
+ unfolding s_eq by (auto simp: enum_mono Ball_def)
+
+lemma enum_Suc: "i < n \<Longrightarrow> enum (Suc i) = (enum i)(upd i := Suc (enum i (upd i)))"
+ by (auto simp: fun_eq_iff enum_def upd_inj)
+
+lemma enum_eq_p: "i \<le> n \<Longrightarrow> n \<le> j \<Longrightarrow> enum i j = p"
+ by (induct i) (auto simp: enum_Suc enum_0 base_out upd_space not_less[symmetric])
+
+lemma out_eq_p: "a \<in> s \<Longrightarrow> n \<le> j \<Longrightarrow> a j = p"
+ unfolding s_eq by (auto simp add: enum_eq_p)
+
+lemma s_le_p: "a \<in> s \<Longrightarrow> a j \<le> p"
+ using out_eq_p[of a j] s_space by (cases "j < n") auto
+
+lemma le_Suc_base: "a \<in> s \<Longrightarrow> a j \<le> Suc (base j)"
+ unfolding s_eq by (auto simp: enum_def)
+
+lemma base_le: "a \<in> s \<Longrightarrow> base j \<le> a j"
+ unfolding s_eq by (auto simp: enum_def)
+
+lemma enum_le_p: "i \<le> n \<Longrightarrow> j < n \<Longrightarrow> enum i j \<le> p"
+ using enum_in[of i] s_space by auto
+
+lemma enum_less: "a \<in> s \<Longrightarrow> i < n \<Longrightarrow> enum i < a \<longleftrightarrow> enum (Suc i) \<le> a"
+ unfolding s_eq by (auto simp: enum_strict_mono enum_mono)
+
+lemma ksimplex_0:
+ "n = 0 \<Longrightarrow> s = {(\<lambda>x. p)}"
+ using s_eq enum_def base_out by auto
+
+lemma replace_0:
+ assumes "j < n" "a \<in> s" and p: "\<forall>x\<in>s - {a}. x j = 0" and "x \<in> s"
+ shows "x \<le> a"
+proof cases
+ assume "x \<noteq> a"
+ have "a j \<noteq> 0"
+ using assms by (intro one_step[where a=a]) auto
+ with less[OF `x\<in>s` `a\<in>s`, of j] p[rule_format, of x] `x \<in> s` `x \<noteq> a`
+ show ?thesis
+ by auto
+qed simp
+
+lemma replace_1:
+ assumes "j < n" "a \<in> s" and p: "\<forall>x\<in>s - {a}. x j = p" and "x \<in> s"
+ shows "a \<le> x"
+proof cases
+ assume "x \<noteq> a"
+ have "a j \<noteq> p"
+ using assms by (intro one_step[where a=a]) auto
+ with enum_le_p[of _ j] `j < n` `a\<in>s`
+ have "a j < p"
+ by (auto simp: less_le s_eq)
+ with less[OF `a\<in>s` `x\<in>s`, of j] p[rule_format, of x] `x \<in> s` `x \<noteq> a`
+ show ?thesis
+ by auto
+qed simp
+
+end
+
+locale kuhn_simplex_pair = s: kuhn_simplex p n b_s u_s s + t: kuhn_simplex p n b_t u_t t
+ for p n b_s u_s s b_t u_t t
+begin
+
+lemma enum_eq:
+ assumes l: "i \<le> l" "l \<le> j" and "j + d \<le> n"
+ assumes eq: "s.enum ` {i .. j} = t.enum ` {i + d .. j + d}"
+ shows "s.enum l = t.enum (l + d)"
+using l proof (induct l rule: dec_induct)
+ case base
+ then have s: "s.enum i \<in> t.enum ` {i + d .. j + d}" and t: "t.enum (i + d) \<in> s.enum ` {i .. j}"
+ using eq by auto
+ from t `i \<le> j` `j + d \<le> n` have "s.enum i \<le> t.enum (i + d)"
+ by (auto simp: s.enum_mono)
+ moreover from s `i \<le> j` `j + d \<le> n` have "t.enum (i + d) \<le> s.enum i"
+ by (auto simp: t.enum_mono)
+ ultimately show ?case
+ by auto
+next
+ case (step l)
+ moreover from step.prems `j + d \<le> n` have
+ "s.enum l < s.enum (Suc l)"
+ "t.enum (l + d) < t.enum (Suc l + d)"
+ by (simp_all add: s.enum_strict_mono t.enum_strict_mono)
+ moreover have
+ "s.enum (Suc l) \<in> t.enum ` {i + d .. j + d}"
+ "t.enum (Suc l + d) \<in> s.enum ` {i .. j}"
+ using step `j + d \<le> n` eq by (auto simp: s.enum_inj t.enum_inj)
+ ultimately have "s.enum (Suc l) = t.enum (Suc (l + d))"
+ using `j + d \<le> n`
+ by (intro antisym s.enum_less[THEN iffD1] t.enum_less[THEN iffD1])
+ (auto intro!: s.enum_in t.enum_in)
+ then show ?case by simp
+qed
+
+lemma ksimplex_eq_bot:
+ assumes a: "a \<in> s" "\<And>a'. a' \<in> s \<Longrightarrow> a \<le> a'"
+ assumes b: "b \<in> t" "\<And>b'. b' \<in> t \<Longrightarrow> b \<le> b'"
+ assumes eq: "s - {a} = t - {b}"
+ shows "s = t"
+proof cases
+ assume "n = 0" with s.ksimplex_0 t.ksimplex_0 show ?thesis by simp
+next
+ assume "n \<noteq> 0"
+ have "s.enum 0 = (s.enum (Suc 0)) (u_s 0 := s.enum (Suc 0) (u_s 0) - 1)"
+ "t.enum 0 = (t.enum (Suc 0)) (u_t 0 := t.enum (Suc 0) (u_t 0) - 1)"
+ using `n \<noteq> 0` by (simp_all add: s.enum_Suc t.enum_Suc)
+ moreover have e0: "a = s.enum 0" "b = t.enum 0"
+ using a b by (simp_all add: s.enum_0_bot t.enum_0_bot)
+ moreover
+ { fix j assume "0 < j" "j \<le> n"
+ moreover have "s - {a} = s.enum ` {Suc 0 .. n}" "t - {b} = t.enum ` {Suc 0 .. n}"
+ unfolding s.s_eq t.s_eq e0 by (auto simp: s.enum_inj t.enum_inj)
+ ultimately have "s.enum j = t.enum j"
+ using enum_eq[of "1" j n 0] eq by auto }
+ note enum_eq = this
+ then have "s.enum (Suc 0) = t.enum (Suc 0)"
+ using `n \<noteq> 0` by auto
+ moreover
+ { fix j assume "Suc j < n"
+ with enum_eq[of "Suc j"] enum_eq[of "Suc (Suc j)"]
+ have "u_s (Suc j) = u_t (Suc j)"
+ using s.enum_Suc[of "Suc j"] t.enum_Suc[of "Suc j"]
+ by (auto simp: fun_eq_iff split: split_if_asm) }
+ then have "\<And>j. 0 < j \<Longrightarrow> j < n \<Longrightarrow> u_s j = u_t j"
+ by (auto simp: gr0_conv_Suc)
+ with `n \<noteq> 0` have "u_t 0 = u_s 0"
+ by (intro bij_betw_singleton_eq[OF t.upd s.upd, of 0]) auto
+ ultimately have "a = b"
+ by simp
+ with assms show "s = t"
+ by auto
+qed
+
+lemma ksimplex_eq_top:
+ assumes a: "a \<in> s" "\<And>a'. a' \<in> s \<Longrightarrow> a' \<le> a"
+ assumes b: "b \<in> t" "\<And>b'. b' \<in> t \<Longrightarrow> b' \<le> b"
+ assumes eq: "s - {a} = t - {b}"
+ shows "s = t"
+proof (cases n)
+ assume "n = 0" with s.ksimplex_0 t.ksimplex_0 show ?thesis by simp
+next
+ case (Suc n')
+ have "s.enum n = (s.enum n') (u_s n' := Suc (s.enum n' (u_s n')))"
+ "t.enum n = (t.enum n') (u_t n' := Suc (t.enum n' (u_t n')))"
+ using Suc by (simp_all add: s.enum_Suc t.enum_Suc)
+ moreover have en: "a = s.enum n" "b = t.enum n"
+ using a b by (simp_all add: s.enum_n_top t.enum_n_top)
+ moreover
+ { fix j assume "j < n"
+ moreover have "s - {a} = s.enum ` {0 .. n'}" "t - {b} = t.enum ` {0 .. n'}"
+ unfolding s.s_eq t.s_eq en by (auto simp: s.enum_inj t.enum_inj Suc)
+ ultimately have "s.enum j = t.enum j"
+ using enum_eq[of "0" j n' 0] eq Suc by auto }
+ note enum_eq = this
+ then have "s.enum n' = t.enum n'"
+ using Suc by auto
+ moreover
+ { fix j assume "j < n'"
+ with enum_eq[of j] enum_eq[of "Suc j"]
+ have "u_s j = u_t j"
+ using s.enum_Suc[of j] t.enum_Suc[of j]
+ by (auto simp: Suc fun_eq_iff split: split_if_asm) }
+ then have "\<And>j. j < n' \<Longrightarrow> u_s j = u_t j"
+ by (auto simp: gr0_conv_Suc)
+ then have "u_t n' = u_s n'"
+ by (intro bij_betw_singleton_eq[OF t.upd s.upd, of n']) (auto simp: Suc)
+ ultimately have "a = b"
+ by simp
+ with assms show "s = t"
+ by auto
+qed
+
+end
+
+inductive ksimplex for p n :: nat where
+ ksimplex: "kuhn_simplex p n base upd s \<Longrightarrow> ksimplex p n s"
+
+lemma finite_ksimplexes: "finite {s. ksimplex p n s}"
+proof (rule finite_subset)
+ { fix a s assume "ksimplex p n s" "a \<in> s"
+ then obtain b u where "kuhn_simplex p n b u s" by (auto elim: ksimplex.cases)
+ then interpret kuhn_simplex p n b u s .
+ from s_space `a \<in> s` out_eq_p[OF `a \<in> s`]
+ have "a \<in> (\<lambda>f x. if n \<le> x then p else f x) ` ({..< n} \<rightarrow>\<^sub>E {.. p})"
+ by (auto simp: image_iff subset_eq Pi_iff split: split_if_asm
+ intro!: bexI[of _ "restrict a {..< n}"]) }
+ then show "{s. ksimplex p n s} \<subseteq> Pow ((\<lambda>f x. if n \<le> x then p else f x) ` ({..< n} \<rightarrow>\<^sub>E {.. p}))"
+ by auto
+qed (simp add: finite_PiE)
+
+lemma ksimplex_card:
+ assumes "ksimplex p n s" shows "card s = Suc n"
+using assms proof cases
+ case (ksimplex u b)
+ then interpret kuhn_simplex p n u b s .
+ show ?thesis
+ by (simp add: card_image s_eq inj_enum)
+qed
+
+lemma simplex_top_face:
+ assumes "0 < p" "\<forall>x\<in>s'. x n = p"
+ shows "ksimplex p n s' \<longleftrightarrow> (\<exists>s a. ksimplex p (Suc n) s \<and> a \<in> s \<and> s' = s - {a})"
+ using assms
+proof safe
+ fix s a assume "ksimplex p (Suc n) s" and a: "a \<in> s" and na: "\<forall>x\<in>s - {a}. x n = p"
+ then show "ksimplex p n (s - {a})"
+ proof cases
+ case (ksimplex base upd)
+ then interpret kuhn_simplex p "Suc n" base upd "s" .
+
+ have "a n < p"
+ using one_step[of a n p] na `a\<in>s` s_space by (auto simp: less_le)
+ then have "a = enum 0"
+ using `a \<in> s` na by (subst enum_0_bot) (auto simp: le_less intro!: less[of a _ n])
+ then have s_eq: "s - {a} = enum ` Suc ` {.. n}"
+ using s_eq by (simp add: atMost_Suc_eq_insert_0 insert_ident Zero_notin_Suc in_enum_image subset_eq)
+ then have "enum 1 \<in> s - {a}"
+ by auto
+ then have "upd 0 = n"
+ using `a n < p` `a = enum 0` na[rule_format, of "enum 1"]
+ by (auto simp: fun_eq_iff enum_Suc split: split_if_asm)
+ then have "bij_betw upd (Suc ` {..< n}) {..< n}"
+ using upd
+ by (subst notIn_Un_bij_betw3[where b=0])
+ (auto simp: lessThan_Suc[symmetric] lessThan_Suc_eq_insert_0)
+ then have "bij_betw (upd\<circ>Suc) {..<n} {..<n}"
+ by (rule bij_betw_trans[rotated]) (auto simp: bij_betw_def)
+
+ have "a n = p - 1"
+ using enum_Suc[of 0] na[rule_format, OF `enum 1 \<in> s - {a}`] `a = enum 0` by (auto simp: `upd 0 = n`)
+
+ show ?thesis
+ proof (rule ksimplex.intros, default)
+ show "bij_betw (upd\<circ>Suc) {..< n} {..< n}" by fact
+ show "base(n := p) \<in> {..<n} \<rightarrow> {..<p}" "\<And>i. n\<le>i \<Longrightarrow> (base(n := p)) i = p"
+ using base base_out by (auto simp: Pi_iff)
+
+ have "\<And>i. Suc ` {..< i} = {..< Suc i} - {0}"
+ by (auto simp: image_iff Ball_def) arith
+ then have upd_Suc: "\<And>i. i \<le> n \<Longrightarrow> (upd\<circ>Suc) ` {..< i} = upd ` {..< Suc i} - {n}"
+ using `upd 0 = n`
+ by (simp add: image_comp[symmetric] inj_on_image_set_diff[OF inj_upd])
+ have n_in_upd: "\<And>i. n \<in> upd ` {..< Suc i}"
+ using `upd 0 = n` by auto
+
+ def f' \<equiv> "\<lambda>i j. if j \<in> (upd\<circ>Suc)`{..< i} then Suc ((base(n := p)) j) else (base(n := p)) j"
+ { fix x i assume i[arith]: "i \<le> n" then have "enum (Suc i) x = f' i x"
+ unfolding f'_def enum_def using `a n < p` `a = enum 0` `upd 0 = n` `a n = p - 1`
+ by (simp add: upd_Suc enum_0 n_in_upd) }
+ then show "s - {a} = f' ` {.. n}"
+ unfolding s_eq image_comp by (intro image_cong) auto
+ qed
+ qed
+next
+ assume "ksimplex p n s'" and *: "\<forall>x\<in>s'. x n = p"
+ then show "\<exists>s a. ksimplex p (Suc n) s \<and> a \<in> s \<and> s' = s - {a}"
+ proof cases
+ case (ksimplex base upd)
+ then interpret kuhn_simplex p n base upd s' .
+ def b \<equiv> "base (n := p - 1)"
+ def u \<equiv> "\<lambda>i. case i of 0 \<Rightarrow> n | Suc i \<Rightarrow> upd i"
+
+ have "ksimplex p (Suc n) (s' \<union> {b})"
+ proof (rule ksimplex.intros, default)
+ show "b \<in> {..<Suc n} \<rightarrow> {..<p}"
+ using base `0 < p` unfolding lessThan_Suc b_def by (auto simp: PiE_iff)
+ show "\<And>i. Suc n \<le> i \<Longrightarrow> b i = p"
+ using base_out by (auto simp: b_def)
+
+ have "bij_betw u (Suc ` {..< n} \<union> {0}) ({..<n} \<union> {u 0})"
+ using upd
+ by (intro notIn_Un_bij_betw) (auto simp: u_def bij_betw_def image_comp comp_def inj_on_def)
+ then show "bij_betw u {..<Suc n} {..<Suc n}"
+ by (simp add: u_def lessThan_Suc[symmetric] lessThan_Suc_eq_insert_0)
+
+ def f' \<equiv> "\<lambda>i j. if j \<in> u`{..< i} then Suc (b j) else b j"
+
+ have u_eq: "\<And>i. i \<le> n \<Longrightarrow> u ` {..< Suc i} = upd ` {..< i} \<union> { n }"
+ by (auto simp: u_def image_iff upd_inj Ball_def split: nat.split) arith
+
+ { fix x have "x \<le> n \<Longrightarrow> n \<notin> upd ` {..<x}"
+ using upd_space by (simp add: image_iff neq_iff) }
+ note n_not_upd = this
+
+ have *: "f' ` {.. Suc n} = f' ` (Suc ` {.. n} \<union> {0})"
+ unfolding atMost_Suc_eq_insert_0 by simp
+ also have "\<dots> = (f' \<circ> Suc) ` {.. n} \<union> {b}"
+ by (auto simp: f'_def)
+ also have "(f' \<circ> Suc) ` {.. n} = s'"
+ using `0 < p` base_out[of n]
+ unfolding s_eq enum_def[abs_def] f'_def[abs_def] upd_space
+ by (intro image_cong) (simp_all add: u_eq b_def fun_eq_iff n_not_upd)
+ finally show "s' \<union> {b} = f' ` {.. Suc n}" ..
+ qed
+ moreover have "b \<notin> s'"
+ using * `0 < p` by (auto simp: b_def)
+ ultimately show ?thesis by auto
+ qed
+qed
+
+lemma ksimplex_replace_0:
+ assumes s: "ksimplex p n s" and a: "a \<in> s"
+ assumes j: "j < n" and p: "\<forall>x\<in>s - {a}. x j = 0"
+ shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 1"
+ using s
+proof cases
+ case (ksimplex b_s u_s)
+
+ { fix t b assume "ksimplex p n t"
+ then obtain b_t u_t where "kuhn_simplex p n b_t u_t t"
+ by (auto elim: ksimplex.cases)
+ interpret kuhn_simplex_pair p n b_s u_s s b_t u_t t
+ by intro_locales fact+
+
+ assume b: "b \<in> t" "t - {b} = s - {a}"
+ with a j p s.replace_0[of _ a] t.replace_0[of _ b] have "s = t"
+ by (intro ksimplex_eq_top[of a b]) auto }
+ then have "{s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = {s}"
+ using s `a \<in> s` by auto
+ then show ?thesis
+ by simp
+qed
+
+lemma ksimplex_replace_1:
+ assumes s: "ksimplex p n s" and a: "a \<in> s"
+ assumes j: "j < n" and p: "\<forall>x\<in>s - {a}. x j = p"
+ shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 1"
+ using s
+proof cases
+ case (ksimplex b_s u_s)
+
+ { fix t b assume "ksimplex p n t"
+ then obtain b_t u_t where "kuhn_simplex p n b_t u_t t"
+ by (auto elim: ksimplex.cases)
+ interpret kuhn_simplex_pair p n b_s u_s s b_t u_t t
+ by intro_locales fact+
+
+ assume b: "b \<in> t" "t - {b} = s - {a}"
+ with a j p s.replace_1[of _ a] t.replace_1[of _ b] have "s = t"
+ by (intro ksimplex_eq_bot[of a b]) auto }
+ then have "{s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = {s}"
+ using s `a \<in> s` by auto
+ then show ?thesis
+ by simp
+qed
+
+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))"
+ by (auto simp add: card_Suc_eq eval_nat_numeral)
+
+lemma ksimplex_replace_2:
+ assumes s: "ksimplex p n s" and "a \<in> s" and "n \<noteq> 0"
+ and lb: "\<forall>j<n. \<exists>x\<in>s - {a}. x j \<noteq> 0"
+ and ub: "\<forall>j<n. \<exists>x\<in>s - {a}. x j \<noteq> p"
+ shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 2"
+ using s
+proof cases
+ case (ksimplex base upd)
+ then interpret kuhn_simplex p n base upd s .
+
+ from `a \<in> s` obtain i where "i \<le> n" "a = enum i"
+ unfolding s_eq by auto
+
+ from `i \<le> n` have "i = 0 \<or> i = n \<or> (0 < i \<and> i < n)"
+ by linarith
+ then have "\<exists>!s'. s' \<noteq> s \<and> ksimplex p n s' \<and> (\<exists>b\<in>s'. s - {a} = s'- {b})"
+ proof (elim disjE conjE)
+ assume "i = 0"
+ def rot \<equiv> "\<lambda>i. if i + 1 = n then 0 else i + 1"
+ let ?upd = "upd \<circ> rot"
+
+ have rot: "bij_betw rot {..< n} {..< n}"
+ by (auto simp: bij_betw_def inj_on_def image_iff Ball_def rot_def)
+ arith+
+ from rot upd have "bij_betw ?upd {..<n} {..<n}"
+ by (rule bij_betw_trans)
+
+ def f' \<equiv> "\<lambda>i j. if j \<in> ?upd`{..< i} then Suc (enum (Suc 0) j) else enum (Suc 0) j"
+
+ interpret b: kuhn_simplex p n "enum (Suc 0)" "upd \<circ> rot" "f' ` {.. n}"
+ proof
+ from `a = enum i` ub `n \<noteq> 0` `i = 0`
+ obtain i' where "i' \<le> n" "enum i' \<noteq> enum 0" "enum i' (upd 0) \<noteq> p"
+ unfolding s_eq by (auto intro: upd_space simp: enum_inj)
+ then have "enum 1 \<le> enum i'" "enum i' (upd 0) < p"
+ using enum_le_p[of i' "upd 0"] by (auto simp add: enum_inj enum_mono upd_space)
+ then have "enum 1 (upd 0) < p"
+ by (auto simp add: le_fun_def intro: le_less_trans)
+ then show "enum (Suc 0) \<in> {..<n} \<rightarrow> {..<p}"
+ using base `n \<noteq> 0` by (auto simp add: enum_0 enum_Suc PiE_iff extensional_def upd_space)
+
+ { fix i assume "n \<le> i" then show "enum (Suc 0) i = p"
+ using `n \<noteq> 0` by (auto simp: enum_eq_p) }
+ show "bij_betw ?upd {..<n} {..<n}" by fact
+ qed (simp add: f'_def)
+ have ks_f': "ksimplex p n (f' ` {.. n})"
+ by rule unfold_locales
+
+ have b_enum: "b.enum = f'" unfolding f'_def b.enum_def[abs_def] ..
+ with b.inj_enum have inj_f': "inj_on f' {.. n}" by simp
+
+ have [simp]: "\<And>j. j < n \<Longrightarrow> rot ` {..< j} = {0 <..< Suc j}"
+ by (auto simp: rot_def image_iff Ball_def)
+ arith
+
+ { fix j assume j: "j < n"
+ from j `n \<noteq> 0` have "f' j = enum (Suc j)"
+ by (auto simp add: f'_def enum_def upd_inj in_upd_image image_comp[symmetric] fun_eq_iff) }
+ note f'_eq_enum = this
+ then have "enum ` Suc ` {..< n} = f' ` {..< n}"
+ by (force simp: enum_inj)
+ also have "Suc ` {..< n} = {.. n} - {0}"
+ by (auto simp: image_iff Ball_def) arith
+ also have "{..< n} = {.. n} - {n}"
+ by auto
+ finally have eq: "s - {a} = f' ` {.. n} - {f' n}"
+ unfolding s_eq `a = enum i` `i = 0`
+ by (simp add: inj_on_image_set_diff[OF inj_enum] inj_on_image_set_diff[OF inj_f'])
+
+ have "enum 0 < f' 0"
+ using `n \<noteq> 0` by (simp add: enum_strict_mono f'_eq_enum)
+ also have "\<dots> < f' n"
+ using `n \<noteq> 0` b.enum_strict_mono[of 0 n] unfolding b_enum by simp
+ finally have "a \<noteq> f' n"
+ using `a = enum i` `i = 0` by auto
+
+ { fix t c assume "ksimplex p n t" "c \<in> t" and eq_sma: "s - {a} = t - {c}"
+ obtain b u where "kuhn_simplex p n b u t"
+ using `ksimplex p n t` by (auto elim: ksimplex.cases)
+ then interpret t: kuhn_simplex p n b u t .
+
+ { fix x assume "x \<in> s" "x \<noteq> a"
+ then have "x (upd 0) = enum (Suc 0) (upd 0)"
+ by (auto simp: `a = enum i` `i = 0` s_eq enum_def enum_inj) }
+ then have eq_upd0: "\<forall>x\<in>t-{c}. x (upd 0) = enum (Suc 0) (upd 0)"
+ unfolding eq_sma[symmetric] by auto
+ then have "c (upd 0) \<noteq> enum (Suc 0) (upd 0)"
+ using `n \<noteq> 0` by (intro t.one_step[OF `c\<in>t` ]) (auto simp: upd_space)
+ then have "c (upd 0) < enum (Suc 0) (upd 0) \<or> c (upd 0) > enum (Suc 0) (upd 0)"
+ by auto
+ then have "t = s \<or> t = f' ` {..n}"
+ proof (elim disjE conjE)
+ assume *: "c (upd 0) < enum (Suc 0) (upd 0)"
+ interpret st: kuhn_simplex_pair p n base upd s b u t ..
+ { fix x assume "x \<in> t" with * `c\<in>t` eq_upd0[rule_format, of x] have "c \<le> x"
+ by (auto simp: le_less intro!: t.less[of _ _ "upd 0"]) }
+ note top = this
+ have "s = t"
+ using `a = enum i` `i = 0` `c \<in> t`
+ by (intro st.ksimplex_eq_bot[OF _ _ _ _ eq_sma])
+ (auto simp: s_eq enum_mono t.s_eq t.enum_mono top)
+ then show ?thesis by simp
+ next
+ assume *: "c (upd 0) > enum (Suc 0) (upd 0)"
+ interpret st: kuhn_simplex_pair p n "enum (Suc 0)" "upd \<circ> rot" "f' ` {.. n}" b u t ..
+ have eq: "f' ` {..n} - {f' n} = t - {c}"
+ using eq_sma eq by simp
+ { fix x assume "x \<in> t" with * `c\<in>t` eq_upd0[rule_format, of x] have "x \<le> c"
+ by (auto simp: le_less intro!: t.less[of _ _ "upd 0"]) }
+ note top = this
+ have "f' ` {..n} = t"
+ using `a = enum i` `i = 0` `c \<in> t`
+ by (intro st.ksimplex_eq_top[OF _ _ _ _ eq])
+ (auto simp: b.s_eq b.enum_mono t.s_eq t.enum_mono b_enum[symmetric] top)
+ then show ?thesis by simp
+ qed }
+ with ks_f' eq `a \<noteq> f' n` `n \<noteq> 0` show ?thesis
+ apply (intro ex1I[of _ "f' ` {.. n}"])
+ apply auto []
+ apply metis
+ done
+ next
+ assume "i = n"
+ from `n \<noteq> 0` obtain n' where n': "n = Suc n'"
+ by (cases n) auto
+
+ def rot \<equiv> "\<lambda>i. case i of 0 \<Rightarrow> n' | Suc i \<Rightarrow> i"
+ let ?upd = "upd \<circ> rot"
+
+ have rot: "bij_betw rot {..< n} {..< n}"
+ by (auto simp: bij_betw_def inj_on_def image_iff Bex_def rot_def n' split: nat.splits)
+ arith
+ from rot upd have "bij_betw ?upd {..<n} {..<n}"
+ by (rule bij_betw_trans)
+
+ def b \<equiv> "base (upd n' := base (upd n') - 1)"
+ def f' \<equiv> "\<lambda>i j. if j \<in> ?upd`{..< i} then Suc (b j) else b j"
+
+ interpret b: kuhn_simplex p n b "upd \<circ> rot" "f' ` {.. n}"
+ proof
+ { fix i assume "n \<le> i" then show "b i = p"
+ using base_out[of i] upd_space[of n'] by (auto simp: b_def n') }
+ show "b \<in> {..<n} \<rightarrow> {..<p}"
+ using base `n \<noteq> 0` upd_space[of n']
+ by (auto simp: b_def PiE_def Pi_iff Ball_def upd_space extensional_def n')
+
+ show "bij_betw ?upd {..<n} {..<n}" by fact
+ qed (simp add: f'_def)
+ have f': "b.enum = f'" unfolding f'_def b.enum_def[abs_def] ..
+ have ks_f': "ksimplex p n (b.enum ` {.. n})"
+ unfolding f' by rule unfold_locales
+
+ have "0 < n"
+ using `n \<noteq> 0` by auto
+
+ { from `a = enum i` `n \<noteq> 0` `i = n` lb upd_space[of n']
+ obtain i' where "i' \<le> n" "enum i' \<noteq> enum n" "0 < enum i' (upd n')"
+ unfolding s_eq by (auto simp: enum_inj n')
+ moreover have "enum i' (upd n') = base (upd n')"
+ unfolding enum_def using `i' \<le> n` `enum i' \<noteq> enum n` by (auto simp: n' upd_inj enum_inj)
+ ultimately have "0 < base (upd n')"
+ by auto }
+ then have benum1: "b.enum (Suc 0) = base"
+ unfolding b.enum_Suc[OF `0<n`] b.enum_0 by (auto simp: b_def rot_def)
+
+ have [simp]: "\<And>j. Suc j < n \<Longrightarrow> rot ` {..< Suc j} = {n'} \<union> {..< j}"
+ by (auto simp: rot_def image_iff Ball_def split: nat.splits)
+ have rot_simps: "\<And>j. rot (Suc j) = j" "rot 0 = n'"
+ by (simp_all add: rot_def)
+
+ { fix j assume j: "Suc j \<le> n" then have "b.enum (Suc j) = enum j"
+ by (induct j) (auto simp add: benum1 enum_0 b.enum_Suc enum_Suc rot_simps) }
+ note b_enum_eq_enum = this
+ then have "enum ` {..< n} = b.enum ` Suc ` {..< n}"
+ by (auto simp add: image_comp intro!: image_cong)
+ also have "Suc ` {..< n} = {.. n} - {0}"
+ by (auto simp: image_iff Ball_def) arith
+ also have "{..< n} = {.. n} - {n}"
+ by auto
+ finally have eq: "s - {a} = b.enum ` {.. n} - {b.enum 0}"
+ unfolding s_eq `a = enum i` `i = n`
+ using inj_on_image_set_diff[OF inj_enum order_refl, of "{n}"]
+ inj_on_image_set_diff[OF b.inj_enum order_refl, of "{0}"]
+ by (simp add: comp_def)
+
+ have "b.enum 0 \<le> b.enum n"
+ by (simp add: b.enum_mono)
+ also have "b.enum n < enum n"
+ using `n \<noteq> 0` by (simp add: enum_strict_mono b_enum_eq_enum n')
+ finally have "a \<noteq> b.enum 0"
+ using `a = enum i` `i = n` by auto
+
+ { fix t c assume "ksimplex p n t" "c \<in> t" and eq_sma: "s - {a} = t - {c}"
+ obtain b' u where "kuhn_simplex p n b' u t"
+ using `ksimplex p n t` by (auto elim: ksimplex.cases)
+ then interpret t: kuhn_simplex p n b' u t .
+
+ { fix x assume "x \<in> s" "x \<noteq> a"
+ then have "x (upd n') = enum n' (upd n')"
+ by (auto simp: `a = enum i` n' `i = n` s_eq enum_def enum_inj in_upd_image) }
+ then have eq_upd0: "\<forall>x\<in>t-{c}. x (upd n') = enum n' (upd n')"
+ unfolding eq_sma[symmetric] by auto
+ then have "c (upd n') \<noteq> enum n' (upd n')"
+ using `n \<noteq> 0` by (intro t.one_step[OF `c\<in>t` ]) (auto simp: n' upd_space[unfolded n'])
+ then have "c (upd n') < enum n' (upd n') \<or> c (upd n') > enum n' (upd n')"
+ by auto
+ then have "t = s \<or> t = b.enum ` {..n}"
+ proof (elim disjE conjE)
+ assume *: "c (upd n') > enum n' (upd n')"
+ interpret st: kuhn_simplex_pair p n base upd s b' u t ..
+ { fix x assume "x \<in> t" with * `c\<in>t` eq_upd0[rule_format, of x] have "x \<le> c"
+ by (auto simp: le_less intro!: t.less[of _ _ "upd n'"]) }
+ note top = this
+ have "s = t"
+ using `a = enum i` `i = n` `c \<in> t`
+ by (intro st.ksimplex_eq_top[OF _ _ _ _ eq_sma])
+ (auto simp: s_eq enum_mono t.s_eq t.enum_mono top)
+ then show ?thesis by simp
+ next
+ assume *: "c (upd n') < enum n' (upd n')"
+ interpret st: kuhn_simplex_pair p n b "upd \<circ> rot" "f' ` {.. n}" b' u t ..
+ have eq: "f' ` {..n} - {b.enum 0} = t - {c}"
+ using eq_sma eq f' by simp
+ { fix x assume "x \<in> t" with * `c\<in>t` eq_upd0[rule_format, of x] have "c \<le> x"
+ by (auto simp: le_less intro!: t.less[of _ _ "upd n'"]) }
+ note bot = this
+ have "f' ` {..n} = t"
+ using `a = enum i` `i = n` `c \<in> t`
+ by (intro st.ksimplex_eq_bot[OF _ _ _ _ eq])
+ (auto simp: b.s_eq b.enum_mono t.s_eq t.enum_mono bot)
+ with f' show ?thesis by simp
+ qed }
+ with ks_f' eq `a \<noteq> b.enum 0` `n \<noteq> 0` show ?thesis
+ apply (intro ex1I[of _ "b.enum ` {.. n}"])
+ apply auto []
+ apply metis
+ done
+ next
+ assume i: "0 < i" "i < n"
+ def i' \<equiv> "i - 1"
+ with i have "Suc i' < n"
+ by simp
+ with i have Suc_i': "Suc i' = i"
+ by (simp add: i'_def)
+
+ let ?upd = "Fun.swap i' i upd"
+ from i upd have "bij_betw ?upd {..< n} {..< n}"
+ by (subst bij_betw_swap_iff) (auto simp: i'_def)
+
+ def f' \<equiv> "\<lambda>i j. if j \<in> ?upd`{..< i} then Suc (base j) else base j"
+ interpret b: kuhn_simplex p n base ?upd "f' ` {.. n}"
+ proof
+ show "base \<in> {..<n} \<rightarrow> {..<p}" by fact
+ { fix i assume "n \<le> i" then show "base i = p" by fact }
+ show "bij_betw ?upd {..<n} {..<n}" by fact
+ qed (simp add: f'_def)
+ have f': "b.enum = f'" unfolding f'_def b.enum_def[abs_def] ..
+ have ks_f': "ksimplex p n (b.enum ` {.. n})"
+ unfolding f' by rule unfold_locales
+
+ have "{i} \<subseteq> {..n}"
+ using i by auto
+ { fix j assume "j \<le> n"
+ moreover have "j < i \<or> i = j \<or> i < j" by arith
+ moreover note i
+ ultimately have "enum j = b.enum j \<longleftrightarrow> j \<noteq> i"
+ unfolding enum_def[abs_def] b.enum_def[abs_def]
+ by (auto simp add: fun_eq_iff swap_image i'_def
+ in_upd_image inj_on_image_set_diff[OF inj_upd]) }
+ note enum_eq_benum = this
+ then have "enum ` ({.. n} - {i}) = b.enum ` ({.. n} - {i})"
+ by (intro image_cong) auto
+ then have eq: "s - {a} = b.enum ` {.. n} - {b.enum i}"
+ unfolding s_eq `a = enum i`
+ using inj_on_image_set_diff[OF inj_enum order_refl `{i} \<subseteq> {..n}`]
+ inj_on_image_set_diff[OF b.inj_enum order_refl `{i} \<subseteq> {..n}`]
+ by (simp add: comp_def)
+
+ have "a \<noteq> b.enum i"
+ using `a = enum i` enum_eq_benum i by auto
+
+ { fix t c assume "ksimplex p n t" "c \<in> t" and eq_sma: "s - {a} = t - {c}"
+ obtain b' u where "kuhn_simplex p n b' u t"
+ using `ksimplex p n t` by (auto elim: ksimplex.cases)
+ then interpret t: kuhn_simplex p n b' u t .
+ have "enum i' \<in> s - {a}" "enum (i + 1) \<in> s - {a}"
+ using `a = enum i` i enum_in by (auto simp: enum_inj i'_def)
+ then obtain l k where
+ l: "t.enum l = enum i'" "l \<le> n" "t.enum l \<noteq> c" and
+ k: "t.enum k = enum (i + 1)" "k \<le> n" "t.enum k \<noteq> c"
+ unfolding eq_sma by (auto simp: t.s_eq)
+ with i have "t.enum l < t.enum k"
+ by (simp add: enum_strict_mono i'_def)
+ with `l \<le> n` `k \<le> n` have "l < k"
+ by (simp add: t.enum_strict_mono)
+ { assume "Suc l = k"
+ have "enum (Suc (Suc i')) = t.enum (Suc l)"
+ using i by (simp add: k `Suc l = k` i'_def)
+ then have False
+ using `l < k` `k \<le> n` `Suc i' < n`
+ by (auto simp: t.enum_Suc enum_Suc l upd_inj fun_eq_iff split: split_if_asm)
+ (metis Suc_lessD n_not_Suc_n upd_inj) }
+ with `l < k` have "Suc l < k"
+ by arith
+ have c_eq: "c = t.enum (Suc l)"
+ proof (rule ccontr)
+ assume "c \<noteq> t.enum (Suc l)"
+ then have "t.enum (Suc l) \<in> s - {a}"
+ using `l < k` `k \<le> n` by (simp add: t.s_eq eq_sma)
+ then obtain j where "t.enum (Suc l) = enum j" "j \<le> n" "enum j \<noteq> enum i"
+ unfolding s_eq `a = enum i` by auto
+ with i have "t.enum (Suc l) \<le> t.enum l \<or> t.enum k \<le> t.enum (Suc l)"
+ by (auto simp add: i'_def enum_mono enum_inj l k)
+ with `Suc l < k` `k \<le> n` show False
+ by (simp add: t.enum_mono)
+ qed
+
+ { have "t.enum (Suc (Suc l)) \<in> s - {a}"
+ unfolding eq_sma c_eq t.s_eq using `Suc l < k` `k \<le> n` by (auto simp: t.enum_inj)
+ then obtain j where eq: "t.enum (Suc (Suc l)) = enum j" and "j \<le> n" "j \<noteq> i"
+ by (auto simp: s_eq `a = enum i`)
+ moreover have "enum i' < t.enum (Suc (Suc l))"
+ unfolding l(1)[symmetric] using `Suc l < k` `k \<le> n` by (auto simp: t.enum_strict_mono)
+ ultimately have "i' < j"
+ using i by (simp add: enum_strict_mono i'_def)
+ with `j \<noteq> i` `j \<le> n` have "t.enum k \<le> t.enum (Suc (Suc l))"
+ unfolding i'_def by (simp add: enum_mono k eq)
+ then have "k \<le> Suc (Suc l)"
+ using `k \<le> n` `Suc l < k` by (simp add: t.enum_mono) }
+ with `Suc l < k` have "Suc (Suc l) = k" by simp
+ then have "enum (Suc (Suc i')) = t.enum (Suc (Suc l))"
+ using i by (simp add: k i'_def)
+ also have "\<dots> = (enum i') (u l := Suc (enum i' (u l)), u (Suc l) := Suc (enum i' (u (Suc l))))"
+ using `Suc l < k` `k \<le> n` by (simp add: t.enum_Suc l t.upd_inj)
+ finally have "(u l = upd i' \<and> u (Suc l) = upd (Suc i')) \<or>
+ (u l = upd (Suc i') \<and> u (Suc l) = upd i')"
+ using `Suc i' < n` by (auto simp: enum_Suc fun_eq_iff split: split_if_asm)
+
+ then have "t = s \<or> t = b.enum ` {..n}"
+ proof (elim disjE conjE)
+ assume u: "u l = upd i'"
+ have "c = t.enum (Suc l)" unfolding c_eq ..
+ also have "t.enum (Suc l) = enum (Suc i')"
+ using u `l < k` `k \<le> n` `Suc i' < n` by (simp add: enum_Suc t.enum_Suc l)
+ also have "\<dots> = a"
+ using `a = enum i` i by (simp add: i'_def)
+ finally show ?thesis
+ using eq_sma `a \<in> s` `c \<in> t` by auto
+ next
+ assume u: "u l = upd (Suc i')"
+ def B \<equiv> "b.enum ` {..n}"
+ have "b.enum i' = enum i'"
+ using enum_eq_benum[of i'] i by (auto simp add: i'_def gr0_conv_Suc)
+ have "c = t.enum (Suc l)" unfolding c_eq ..
+ also have "t.enum (Suc l) = b.enum (Suc i')"
+ using u `l < k` `k \<le> n` `Suc i' < n`
+ by (simp_all add: enum_Suc t.enum_Suc l b.enum_Suc `b.enum i' = enum i'` swap_apply1)
+ (simp add: Suc_i')
+ also have "\<dots> = b.enum i"
+ using i by (simp add: i'_def)
+ finally have "c = b.enum i" .
+ then have "t - {c} = B - {c}" "c \<in> B"
+ unfolding eq_sma[symmetric] eq B_def using i by auto
+ with `c \<in> t` have "t = B"
+ by auto
+ then show ?thesis
+ by (simp add: B_def)
+ qed }
+ with ks_f' eq `a \<noteq> b.enum i` `n \<noteq> 0` `i \<le> n` show ?thesis
+ apply (intro ex1I[of _ "b.enum ` {.. n}"])
+ apply auto []
+ apply metis
+ done
+ qed
+ then show ?thesis
+ using s `a \<in> s` by (simp add: card_2_exists Ex1_def) metis
+qed
text {* Hence another step towards concreteness. *}
lemma kuhn_simplex_lemma:
- assumes "\<forall>s. ksimplex p (n + 1) s \<longrightarrow> rl ` s \<subseteq> {0..n+1}"
- and "odd (card {f. \<exists>s a. ksimplex p (n + 1) s \<and> a \<in> s \<and> (f = s - {a}) \<and>
- rl ` f = {0 .. n} \<and> ((\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = p))})"
- shows "odd (card {s \<in> {s. ksimplex p (n + 1) s}. rl ` s = {0..n+1}})"
-proof -
+ assumes "\<forall>s. ksimplex p (Suc n) s \<longrightarrow> rl ` s \<subseteq> {.. Suc n}"
+ and "odd (card {f. \<exists>s a. ksimplex p (Suc n) s \<and> a \<in> s \<and> (f = s - {a}) \<and>
+ rl ` f = {..n} \<and> ((\<exists>j\<le>n. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<le>n. \<forall>x\<in>f. x j = p))})"
+ shows "odd (card {s. ksimplex p (Suc n) s \<and> rl ` s = {..Suc n}})"
+proof (rule kuhn_complete_lemma[OF finite_ksimplexes refl, unfolded mem_Collect_eq,
+ where bnd="\<lambda>f. (\<exists>j\<in>{..n}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{..n}. \<forall>x\<in>f. x j = p)"],
+ safe del: notI)
+
have *: "\<And>x y. x = y \<Longrightarrow> odd (card x) \<Longrightarrow> odd (card y)"
by auto
- have *: "odd (card {f \<in> {f. \<exists>s\<in>{s. ksimplex p (n + 1) s}. (\<exists>a\<in>s. f = s - {a})}.
- rl ` f = {0..n} \<and> ((\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = p))})"
+ show "odd (card {f. (\<exists>s\<in>{s. ksimplex p (Suc n) s}. \<exists>a\<in>s. f = s - {a}) \<and>
+ rl ` f = {..n} \<and> ((\<exists>j\<in>{..n}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{..n}. \<forall>x\<in>f. x j = p))})"
apply (rule *[OF _ assms(2)])
- apply auto
+ apply (auto simp: atLeast0AtMost)
done
- show ?thesis
- apply (rule kuhn_complete_lemma[OF finite_simplices])
- prefer 6
- apply (rule *)
- apply rule
- apply rule
- apply rule
- apply (subst ksimplex_def)
- defer
- apply rule
- apply (rule assms(1)[rule_format])
- unfolding mem_Collect_eq
- apply assumption
- apply default+
- unfolding mem_Collect_eq
- apply (erule disjE bexE)+
- defer
- apply (erule disjE bexE)+
- defer
- apply default+
- unfolding mem_Collect_eq
- apply (erule disjE bexE)+
- unfolding mem_Collect_eq
- proof -
- fix f s a
- assume as: "ksimplex p (n + 1) s" "a \<in> s" "f = s - {a}"
- let ?S = "{s. ksimplex p (n + 1) s \<and> (\<exists>a\<in>s. f = s - {a})}"
- have S: "?S = {s'. ksimplex p (n + 1) s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})}"
- unfolding as by blast
- {
- fix j
- assume j: "j \<in> {1..n + 1}" "\<forall>x\<in>f. x j = 0"
- then show "card {s. ksimplex p (n + 1) s \<and> (\<exists>a\<in>s. f = s - {a})} = 1"
- unfolding S
- apply -
- apply (rule ksimplex_replace_0)
- apply (rule as)+
- unfolding as
- apply auto
- done
- }
- {
- fix j
- assume j: "j \<in> {1..n + 1}" "\<forall>x\<in>f. x j = p"
- then show "card {s. ksimplex p (n + 1) s \<and> (\<exists>a\<in>s. f = s - {a})} = 1"
- unfolding S
- apply -
- apply (rule ksimplex_replace_1)
- apply (rule as)+
- unfolding as
- apply auto
- done
- }
- show "\<not> ((\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = p)) \<Longrightarrow> card ?S = 2"
- unfolding S
- apply (rule ksimplex_replace_2)
- apply (rule as)+
- unfolding as
- apply auto
- done
- qed auto
+
+next
+
+ fix s assume s: "ksimplex p (Suc n) s"
+ then show "card s = n + 2"
+ by (simp add: ksimplex_card)
+
+ fix a assume a: "a \<in> s" then show "rl a \<le> Suc n"
+ using assms(1) s by (auto simp: subset_eq)
+
+ let ?S = "{t. ksimplex p (Suc n) t \<and> (\<exists>b\<in>t. s - {a} = t - {b})}"
+ { fix j assume j: "j \<le> n" "\<forall>x\<in>s - {a}. x j = 0"
+ with s a show "card ?S = 1"
+ using ksimplex_replace_0[of p "n + 1" s a j]
+ by (subst eq_commute) simp }
+
+ { fix j assume j: "j \<le> n" "\<forall>x\<in>s - {a}. x j = p"
+ with s a show "card ?S = 1"
+ using ksimplex_replace_1[of p "n + 1" s a j]
+ by (subst eq_commute) simp }
+
+ { assume "card ?S \<noteq> 2" "\<not> (\<exists>j\<in>{..n}. \<forall>x\<in>s - {a}. x j = p)"
+ with s a show "\<exists>j\<in>{..n}. \<forall>x\<in>s - {a}. x j = 0"
+ using ksimplex_replace_2[of p "n + 1" s a]
+ by (subst (asm) eq_commute) auto }
qed
-
subsection {* Reduced labelling *}
-definition "reduced label (n::nat) (x::nat \<Rightarrow> nat) =
- (SOME k. k \<le> n \<and> (\<forall>i. 1 \<le> i \<and> i < k + 1 \<longrightarrow> label x i = 0) \<and>
- (k = n \<or> label x (k + 1) \<noteq> (0::nat)))"
+definition reduced :: "nat \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> nat" where "reduced n x = (LEAST k. k = n \<or> x k \<noteq> 0)"
lemma reduced_labelling:
- shows "reduced label n x \<le> n" (is ?t1)
- and "\<forall>i. 1 \<le> i \<and> i < reduced label n x + 1 \<longrightarrow> label x i = 0" (is ?t2)
- and "reduced label n x = n \<or> label x (reduced label n x + 1) \<noteq> 0" (is ?t3)
+ shows "reduced n x \<le> n"
+ and "\<forall>i<reduced n x. x i = 0"
+ and "reduced n x = n \<or> x (reduced n x) \<noteq> 0"
proof -
- have num_WOP: "\<And>P k. P (k::nat) \<Longrightarrow> \<exists>n. P n \<and> (\<forall>m<n. \<not> P m)"
- apply (drule ex_has_least_nat[where m="\<lambda>x. x"])
- apply (erule exE)
- apply (rule_tac x=x in exI)
- apply auto
- done
- have *: "n \<le> n \<and> (label x (n + 1) \<noteq> 0 \<or> n = n)"
- by auto
- then obtain N where N:
- "N \<le> n \<and> (label x (N + 1) \<noteq> 0 \<or> n = N)"
- "\<forall>m<N. \<not> (m \<le> n \<and> (label x (m + 1) \<noteq> 0 \<or> n = m))"
- apply (drule_tac num_WOP[of "\<lambda>j. j\<le>n \<and> (label x (j+1) \<noteq> 0 \<or> n = j)"])
- apply blast
- done
- have N': "N \<le> n"
- "\<forall>i. 1 \<le> i \<and> i < N + 1 \<longrightarrow> label x i = 0" "N = n \<or> label x (N + 1) \<noteq> 0"
- defer
- proof (rule, rule)
- fix i
- assume i: "1 \<le> i \<and> i < N + 1"
- then show "label x i = 0"
- using N(2)[THEN spec[where x="i - 1"]]
- using N
- by auto
- qed (insert N(1), auto)
- show ?t1 ?t2 ?t3
- unfolding reduced_def
- apply (rule_tac[!] someI2_ex)
- using N'
- apply (auto intro!: exI[where x=N])
- done
+ show "reduced n x \<le> n"
+ unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) auto
+ show "\<forall>i<reduced n x. x i = 0"
+ unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) fastforce+
+ show "reduced n x = n \<or> x (reduced n x) \<noteq> 0"
+ unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) fastforce+
qed
lemma reduced_labelling_unique:
- fixes x :: "nat \<Rightarrow> nat"
- assumes "r \<le> n"
- and "\<forall>i. 1 \<le> i \<and> i < r + 1 \<longrightarrow> label x i = 0"
- and "r = n \<or> label x (r + 1) \<noteq> 0"
- shows "reduced label n x = r"
- apply (rule le_antisym)
- apply (rule_tac[!] ccontr)
- unfolding not_le
- using reduced_labelling[of label n x]
- using assms
- apply auto
- done
+ "r \<le> n \<Longrightarrow> \<forall>i<r. x i = 0 \<Longrightarrow> r = n \<or> x r \<noteq> 0 \<Longrightarrow> reduced n x = r"
+ unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) (metis le_less not_le)+
+
+lemma reduced_labelling_zero: "j < n \<Longrightarrow> x j = 0 \<Longrightarrow> reduced n x \<noteq> j"
+ using reduced_labelling[of n x] by auto
-lemma reduced_labelling_zero:
- assumes "j \<in> {1..n}"
- and "label x j = 0"
- shows "reduced label n x \<noteq> j - 1"
- using reduced_labelling[of label n x]
- using assms
- by fastforce
+lemma reduce_labelling_zero[simp]: "reduced 0 x = 0"
+ by (rule reduced_labelling_unique) auto
-lemma reduced_labelling_nonzero:
- assumes "j\<in>{1..n}"
- and "label x j \<noteq> 0"
- shows "reduced label n x < j"
- using assms and reduced_labelling[of label n x]
- apply (erule_tac x=j in allE)
- apply auto
- done
+lemma reduced_labelling_nonzero: "j < n \<Longrightarrow> x j \<noteq> 0 \<Longrightarrow> reduced n x \<le> j"
+ using reduced_labelling[of n x] by (elim allE[where x=j]) auto
-lemma reduced_labelling_Suc:
- assumes "reduced lab (n + 1) x \<noteq> n + 1"
- shows "reduced lab (n + 1) x = reduced lab n x"
- apply (subst eq_commute)
- apply (rule reduced_labelling_unique)
- using reduced_labelling[of lab "n+1" x] and assms
- apply auto
- done
+lemma reduced_labelling_Suc: "reduced (Suc n) x \<noteq> Suc n \<Longrightarrow> reduced (Suc n) x = reduced n x"
+ using reduced_labelling[of "Suc n" x]
+ by (intro reduced_labelling_unique[symmetric]) auto
lemma complete_face_top:
- assumes "\<forall>x\<in>f. \<forall>j\<in>{1..n+1}. x j = 0 \<longrightarrow> lab x j = 0"
- and "\<forall>x\<in>f. \<forall>j\<in>{1..n+1}. x j = p \<longrightarrow> lab x j = 1"
- shows "reduced lab (n + 1) ` f = {0..n} \<and>
- ((\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = p)) \<longleftrightarrow>
- reduced lab (n + 1) ` f = {0..n} \<and> (\<forall>x\<in>f. x (n + 1) = p)"
- (is "?l = ?r")
-proof
- assume ?l (is "?as \<and> (?a \<or> ?b)")
- then show ?r
- apply -
- apply rule
- apply (erule conjE)
- apply assumption
- proof (cases ?a)
- case True
- then obtain j where j: "j \<in> {1..n + 1}" "\<forall>x\<in>f. x j = 0" ..
- {
- fix x
- assume x: "x \<in> f"
- have "reduced lab (n + 1) x \<noteq> j - 1"
- using j
- apply -
- apply (rule reduced_labelling_zero)
- defer
- apply (rule assms(1)[rule_format])
- using x
- apply auto
- done
- }
- moreover have "j - 1 \<in> {0..n}"
- using j by auto
- then obtain y where y:
- "y \<in> f"
- "j - 1 = reduced lab (n + 1) y"
- unfolding `?l`[THEN conjunct1,symmetric] and image_iff ..
- ultimately
- have False
- by auto
- then show "\<forall>x\<in>f. x (n + 1) = p"
- by auto
- next
- case False
- then have ?b using `?l`
- by blast
- then obtain j where j: "j \<in> {1..n + 1}" "\<forall>x\<in>f. x j = p" ..
- {
- fix x
- assume x: "x \<in> f"
- have "reduced lab (n + 1) x < j"
- using j
- apply -
- apply (rule reduced_labelling_nonzero)
- using assms(2)[rule_format,of x j] and x
- apply auto
- done
- } note * = this
- have "j = n + 1"
- proof (rule ccontr)
- assume "\<not> ?thesis"
- then have "j < n + 1"
- using j by auto
- moreover
- have "n \<in> {0..n}"
- by auto
- then obtain y where "y \<in> f" "n = reduced lab (n + 1) y"
- unfolding `?l`[THEN conjunct1,symmetric] image_iff ..
- ultimately
- show False
- using *[of y] by auto
- qed
- then show "\<forall>x\<in>f. x (n + 1) = p"
- using j by auto
+ assumes "\<forall>x\<in>f. \<forall>j\<le>n. x j = 0 \<longrightarrow> lab x j = 0"
+ and "\<forall>x\<in>f. \<forall>j\<le>n. x j = p \<longrightarrow> lab x j = 1"
+ and eq: "(reduced (Suc n) \<circ> lab) ` f = {..n}"
+ shows "((\<exists>j\<le>n. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<le>n. \<forall>x\<in>f. x j = p)) \<longleftrightarrow> (\<forall>x\<in>f. x n = p)"
+proof (safe del: disjCI)
+ fix x j assume j: "j \<le> n" "\<forall>x\<in>f. x j = 0"
+ { fix x assume "x \<in> f" with assms j have "reduced (Suc n) (lab x) \<noteq> j"
+ by (intro reduced_labelling_zero) auto }
+ moreover have "j \<in> (reduced (Suc n) \<circ> lab) ` f"
+ using j eq by auto
+ ultimately show "x n = p"
+ by force
+next
+ fix x j assume j: "j \<le> n" "\<forall>x\<in>f. x j = p" and x: "x \<in> f"
+ have "j = n"
+ proof (rule ccontr)
+ assume "\<not> ?thesis"
+ { fix x assume "x \<in> f"
+ with assms j have "reduced (Suc n) (lab x) \<le> j"
+ by (intro reduced_labelling_nonzero) auto
+ then have "reduced (Suc n) (lab x) \<noteq> n"
+ using `j \<noteq> n` `j \<le> n` by simp }
+ moreover
+ have "n \<in> (reduced (Suc n) \<circ> lab) ` f"
+ using eq by auto
+ ultimately show False
+ by force
qed
+ moreover have "j \<in> (reduced (Suc n) \<circ> lab) ` f"
+ using j eq by auto
+ ultimately show "x n = p"
+ using j x by auto
qed auto
-
text {* Hence we get just about the nice induction. *}
lemma kuhn_induction:
assumes "0 < p"
- and "\<forall>x. \<forall>j\<in>{1..n+1}. (\<forall>j. x j \<le> p) \<and> x j = 0 \<longrightarrow> lab x j = 0"
- and "\<forall>x. \<forall>j\<in>{1..n+1}. (\<forall>j. x j \<le> p) \<and> x j = p \<longrightarrow> lab x j = 1"
- and "odd (card {f. ksimplex p n f \<and> reduced lab n ` f = {0..n}})"
- shows "odd (card {s. ksimplex p (n + 1) s \<and> reduced lab (n + 1) ` s = {0..n+1}})"
+ and lab_0: "\<forall>x. \<forall>j\<le>n. (\<forall>j. x j \<le> p) \<and> x j = 0 \<longrightarrow> lab x j = 0"
+ and lab_1: "\<forall>x. \<forall>j\<le>n. (\<forall>j. x j \<le> p) \<and> x j = p \<longrightarrow> lab x j = 1"
+ and odd: "odd (card {s. ksimplex p n s \<and> (reduced n\<circ>lab) ` s = {..n}})"
+ shows "odd (card {s. ksimplex p (Suc n) s \<and> (reduced (Suc n)\<circ>lab) ` s = {..Suc n}})"
proof -
- have *: "\<And>s t. odd (card s) \<Longrightarrow> s = t \<Longrightarrow> odd (card t)"
- "\<And>s f. (\<And>x. f x \<le> n + 1) \<Longrightarrow> f ` s \<subseteq> {0..n+1}"
- by auto
- show ?thesis
- apply (rule kuhn_simplex_lemma[unfolded mem_Collect_eq])
- apply rule
- apply rule
- apply (rule *)
- apply (rule reduced_labelling)
- apply (rule *(1)[OF assms(4)])
- apply (rule set_eqI)
- unfolding mem_Collect_eq
- apply rule
- apply (erule conjE)
- defer
- apply rule
- proof -
- fix f
- assume as: "ksimplex p n f" "reduced lab n ` f = {0..n}"
- have *: "\<forall>x\<in>f. \<forall>j\<in>{1..n + 1}. x j = 0 \<longrightarrow> lab x j = 0"
- "\<forall>x\<in>f. \<forall>j\<in>{1..n + 1}. x j = p \<longrightarrow> lab x j = 1"
- using assms(2-3)
- using as(1)[unfolded ksimplex_def]
- by auto
- have allp: "\<forall>x\<in>f. x (n + 1) = p"
- using assms(2)
- using as(1)[unfolded ksimplex_def]
+ let ?rl = "reduced (Suc n) \<circ> lab" and ?ext = "\<lambda>f v. \<exists>j\<le>n. \<forall>x\<in>f. x j = v"
+ let ?ext = "\<lambda>s. (\<exists>j\<le>n. \<forall>x\<in>s. x j = 0) \<or> (\<exists>j\<le>n. \<forall>x\<in>s. x j = p)"
+ have "\<forall>s. ksimplex p (Suc n) s \<longrightarrow> ?rl ` s \<subseteq> {..Suc n}"
+ by (simp add: reduced_labelling subset_eq)
+ moreover
+ have "{s. ksimplex p n s \<and> (reduced n \<circ> lab) ` s = {..n}} =
+ {f. \<exists>s a. ksimplex p (Suc n) s \<and> a \<in> s \<and> f = s - {a} \<and> ?rl ` f = {..n} \<and> ?ext f}"
+ proof (intro set_eqI, safe del: disjCI equalityI disjE)
+ fix s assume s: "ksimplex p n s" and rl: "(reduced n \<circ> lab) ` s = {..n}"
+ from s obtain u b where "kuhn_simplex p n u b s" by (auto elim: ksimplex.cases)
+ then interpret kuhn_simplex p n u b s .
+ have all_eq_p: "\<forall>x\<in>s. x n = p"
+ by (auto simp: out_eq_p)
+ moreover
+ { fix x assume "x \<in> s"
+ with lab_1[rule_format, of n x] all_eq_p s_le_p[of x]
+ have "?rl x \<le> n"
+ by (auto intro!: reduced_labelling_nonzero)
+ then have "?rl x = reduced n (lab x)"
+ by (auto intro!: reduced_labelling_Suc) }
+ then have "?rl ` s = {..n}"
+ using rl by (simp cong: image_cong)
+ moreover
+ obtain t a where "ksimplex p (Suc n) t" "a \<in> t" "s = t - {a}"
+ using s unfolding simplex_top_face[OF `0 < p` all_eq_p] by auto
+ ultimately
+ show "\<exists>t a. ksimplex p (Suc n) t \<and> a \<in> t \<and> s = t - {a} \<and> ?rl ` s = {..n} \<and> ?ext s"
by auto
- {
- fix x
- assume "x \<in> f"
- then have "reduced lab (n + 1) x < n + 1"
- apply -
- apply (rule reduced_labelling_nonzero)
- defer
- using assms(3)
- using as(1)[unfolded ksimplex_def]
- apply auto
- done
- then have "reduced lab (n + 1) x = reduced lab n x"
- apply -
- apply (rule reduced_labelling_Suc)
- using reduced_labelling(1)
- apply auto
- done
- }
- then have "reduced lab (n + 1) ` f = {0..n}"
- unfolding as(2)[symmetric]
- apply -
- apply (rule set_eqI)
- unfolding image_iff
- apply auto
- done
- moreover
- obtain s a where "ksimplex p (n + 1) s \<and> a \<in> s \<and> f = s - {a}"
- using as(1)[unfolded simplex_top_face[OF assms(1) allp,symmetric]] by blast
- ultimately show "\<exists>s a. ksimplex p (n + 1) s \<and>
- a \<in> s \<and> f = s - {a} \<and>
- reduced lab (n + 1) ` f = {0..n} \<and>
- ((\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p))"
- apply (rule_tac x = s in exI)
- apply (rule_tac x = a in exI)
- unfolding complete_face_top[OF *]
- using allp as(1)
- apply auto
- done
next
- fix f
- assume as: "\<exists>s a. ksimplex p (n + 1) s \<and>
- a \<in> s \<and> f = s - {a} \<and> reduced lab (n + 1) ` f = {0..n} \<and>
- ((\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p))"
- then obtain s a where sa:
- "ksimplex p (n + 1) s"
- "a \<in> s"
- "f = s - {a}"
- "reduced lab (n + 1) ` f = {0..n}"
- "(\<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)"
- by auto
- {
- fix x
- assume "x \<in> f"
- then have "reduced lab (n + 1) x \<in> reduced lab (n + 1) ` f"
+ fix x s a assume s: "ksimplex p (Suc n) s" and rl: "?rl ` (s - {a}) = {.. n}"
+ and a: "a \<in> s" and "?ext (s - {a})"
+ from s obtain u b where "kuhn_simplex p (Suc n) u b s" by (auto elim: ksimplex.cases)
+ then interpret kuhn_simplex p "Suc n" u b s .
+ have all_eq_p: "\<forall>x\<in>s. x (Suc n) = p"
+ by (auto simp: out_eq_p)
+
+ { fix x assume "x \<in> s - {a}"
+ then have "?rl x \<in> ?rl ` (s - {a})"
by auto
- then have "reduced lab (n + 1) x < n + 1"
- using sa(4) by auto
- then have "reduced lab (n + 1) x = reduced lab n x"
- apply -
- apply (rule reduced_labelling_Suc)
- using reduced_labelling(1)
- apply auto
- done
- }
- then show part1: "reduced lab n ` f = {0..n}"
- unfolding sa(4)[symmetric]
- apply -
- apply (rule set_eqI)
- unfolding image_iff
- apply auto
- done
- have *: "\<forall>x\<in>f. x (n + 1) = p"
- proof (cases "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0")
- case True
- then obtain j where "j \<in> {1..n + 1}" "\<forall>x\<in>f. x j = 0" ..
- then have "\<And>x. x \<in> f \<Longrightarrow> reduced lab (n + 1) x \<noteq> j - 1"
- apply -
- apply (rule reduced_labelling_zero)
- apply assumption
- apply (rule assms(2)[rule_format])
- using sa(1)[unfolded ksimplex_def]
- unfolding sa
- apply auto
- done
- moreover
- have "j - 1 \<in> {0..n}"
- using `j\<in>{1..n+1}` by auto
- ultimately have False
- unfolding sa(4)[symmetric]
- unfolding image_iff
- by fastforce
- then show ?thesis
- by auto
+ then have "?rl x \<le> n"
+ unfolding rl by auto
+ then have "?rl x = reduced n (lab x)"
+ by (auto intro!: reduced_labelling_Suc) }
+ then show rl': "(reduced n\<circ>lab) ` (s - {a}) = {..n}"
+ unfolding rl[symmetric] by (intro image_cong) auto
+
+ from `?ext (s - {a})`
+ have all_eq_p: "\<forall>x\<in>s - {a}. x n = p"
+ proof (elim disjE exE conjE)
+ fix j assume "j \<le> n" "\<forall>x\<in>s - {a}. x j = 0"
+ with lab_0[rule_format, of j] all_eq_p s_le_p
+ have "\<And>x. x \<in> s - {a} \<Longrightarrow> reduced (Suc n) (lab x) \<noteq> j"
+ by (intro reduced_labelling_zero) auto
+ moreover have "j \<in> ?rl ` (s - {a})"
+ using `j \<le> n` unfolding rl by auto
+ ultimately show ?thesis
+ by force
next
- case False
- then have "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p"
- using sa(5) by fastforce
- then obtain j where j: "j \<in> {1..n + 1}" "\<forall>x\<in>f. x j = p" ..
- then show ?thesis
- proof (cases "j = n + 1")
- case False
- then have *: "j \<in> {1..n}"
- using j by auto
- then have "\<And>x. x \<in> f \<Longrightarrow> reduced lab n x < j"
- apply (rule reduced_labelling_nonzero)
- proof -
- fix x
- assume "x \<in> f"
- then have "lab x j = 1"
- apply -
- apply (rule assms(3)[rule_format,OF j(1)])
- using sa(1)[unfolded ksimplex_def]
- using j
- unfolding sa
- apply auto
- done
- then show "lab x j \<noteq> 0"
- by auto
- qed
- moreover have "j \<in> {0..n}"
- using * by auto
- ultimately have False
- unfolding part1[symmetric]
- using * unfolding image_iff
- by auto
- then show ?thesis
- by auto
- qed auto
+ fix j assume "j \<le> n" and eq_p: "\<forall>x\<in>s - {a}. x j = p"
+ show ?thesis
+ proof cases
+ assume "j = n" with eq_p show ?thesis by simp
+ next
+ assume "j \<noteq> n"
+ { fix x assume x: "x \<in> s - {a}"
+ have "reduced n (lab x) \<le> j"
+ proof (rule reduced_labelling_nonzero)
+ show "lab x j \<noteq> 0"
+ using lab_1[rule_format, of j x] x s_le_p[of x] eq_p `j \<le> n` by auto
+ show "j < n"
+ using `j \<le> n` `j \<noteq> n` by simp
+ qed
+ then have "reduced n (lab x) \<noteq> n"
+ using `j \<le> n` `j \<noteq> n` by simp }
+ moreover have "n \<in> (reduced n\<circ>lab) ` (s - {a})"
+ unfolding rl' by auto
+ ultimately show ?thesis
+ by force
+ qed
qed
- then show "ksimplex p n f"
- using as
- unfolding simplex_top_face[OF assms(1) *,symmetric]
- by auto
+ show "ksimplex p n (s - {a})"
+ unfolding simplex_top_face[OF `0 < p` all_eq_p] using s a by auto
qed
+ ultimately show ?thesis
+ using assms by (intro kuhn_simplex_lemma) auto
qed
-lemma kuhn_induction_Suc:
- assumes "0 < p"
- and "\<forall>x. \<forall>j\<in>{1..Suc n}. (\<forall>j. x j \<le> p) \<and> x j = 0 \<longrightarrow> lab x j = 0"
- and "\<forall>x. \<forall>j\<in>{1..Suc n}. (\<forall>j. x j \<le> p) \<and> x j = p \<longrightarrow> lab x j = 1"
- and "odd (card {f. ksimplex p n f \<and> reduced lab n ` f = {0..n}})"
- shows "odd (card {s. ksimplex p (Suc n) s \<and> reduced lab (Suc n) ` s = {0..Suc n}})"
- using assms
- unfolding Suc_eq_plus1
- by (rule kuhn_induction)
-
-
text {* And so we get the final combinatorial result. *}
lemma ksimplex_0: "ksimplex p 0 s \<longleftrightarrow> s = {(\<lambda>x. p)}"
- (is "?l = ?r")
proof
- assume l: ?l
- obtain a where a: "a \<in> s" "\<forall>y y'. y \<in> s \<and> y' \<in> s \<longrightarrow> y = y'"
- using ksimplexD(3)[OF l, unfolded add_0]
- unfolding card_1_exists ..
- have "a = (\<lambda>x. p)"
- using ksimplexD(5)[OF l, rule_format, OF a(1)]
- by rule auto
- then show ?r
- using a by auto
+ assume "ksimplex p 0 s" then show "s = {(\<lambda>x. p)}"
+ by (blast dest: kuhn_simplex.ksimplex_0 elim: ksimplex.cases)
next
- assume r: ?r
- show ?l
- unfolding r ksimplex_eq by auto
+ assume s: "s = {(\<lambda>x. p)}"
+ show "ksimplex p 0 s"
+ proof (intro ksimplex, unfold_locales)
+ show "(\<lambda>_. p) \<in> {..<0::nat} \<rightarrow> {..<p}" by auto
+ show "bij_betw id {..<0} {..<0}"
+ by simp
+ qed (auto simp: s)
qed
-lemma reduce_labelling_zero[simp]: "reduced lab 0 x = 0"
- by (rule reduced_labelling_unique) auto
-
lemma kuhn_combinatorial:
assumes "0 < p"
- and "\<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"
- and "\<forall>x j. (\<forall>j. x j \<le> p) \<and> 1 \<le> j \<and> j \<le> n \<and> x j = p \<longrightarrow> lab x j = 1"
- shows "odd (card {s. ksimplex p n s \<and> reduced lab n ` s = {0..n}})"
+ and "\<forall>x j. (\<forall>j. x j \<le> p) \<and> j < n \<and> x j = 0 \<longrightarrow> lab x j = 0"
+ and "\<forall>x j. (\<forall>j. x j \<le> p) \<and> j < n \<and> x j = p \<longrightarrow> lab x j = 1"
+ shows "odd (card {s. ksimplex p n s \<and> (reduced n\<circ>lab) ` s = {..n}})"
+ (is "odd (card (?M n))")
using assms
proof (induct n)
- let ?M = "\<lambda>n. {s. ksimplex p n s \<and> reduced lab n ` s = {0..n}}"
- {
- case 0
- have *: "?M 0 = {{\<lambda>x. p}}"
- unfolding ksimplex_0 by auto
- show ?case
- unfolding * by auto
- next
- case (Suc n)
- have "odd (card (?M n))"
- apply (rule Suc(1)[OF Suc(2)])
- using Suc(3-)
- apply auto
- done
- then show ?case
- apply -
- apply (rule kuhn_induction_Suc)
- using Suc(2-)
- apply auto
- done
- }
+ case 0 then show ?case
+ by (simp add: ksimplex_0 cong: conj_cong)
+next
+ case (Suc n)
+ then have "odd (card (?M n))"
+ by force
+ with Suc show ?case
+ using kuhn_induction[of p n] by (auto simp: comp_def)
qed
lemma kuhn_lemma:
fixes n p :: nat
assumes "0 < p"
- and "0 < n"
- and "\<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)"
- and "\<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)"
- and "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. x i = p \<longrightarrow> label x i = 1)"
- obtains q where "\<forall>i\<in>{1..n}. q i < p"
- and "\<forall>i\<in>{1..n}. \<exists>r s.
- (\<forall>j\<in>{1..n}. q j \<le> r j \<and> r j \<le> q j + 1) \<and>
- (\<forall>j\<in>{1..n}. q j \<le> s j \<and> s j \<le> q j + 1) \<and>
- label r i \<noteq> label s i"
+ and "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. label x i = (0::nat) \<or> label x i = 1)"
+ and "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = 0 \<longrightarrow> label x i = 0)"
+ and "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = p \<longrightarrow> label x i = 1)"
+ obtains q where "\<forall>i<n. q i < p"
+ and "\<forall>i<n. \<exists>r s. (\<forall>j<n. q j \<le> r j \<and> r j \<le> q j + 1) \<and> (\<forall>j<n. q j \<le> s j \<and> s j \<le> q j + 1) \<and> label r i \<noteq> label s i"
proof -
- let ?A = "{s. ksimplex p n s \<and> reduced label n ` s = {0..n}}"
- have "n \<noteq> 0"
- using assms by auto
- have conjD: "\<And>P Q. P \<and> Q \<Longrightarrow> P" "\<And>P Q. P \<and> Q \<Longrightarrow> Q"
- by auto
+ let ?rl = "reduced n\<circ>label"
+ let ?A = "{s. ksimplex p n s \<and> ?rl ` s = {..n}}"
have "odd (card ?A)"
- apply (rule kuhn_combinatorial[of p n label])
- using assms
- apply auto
- done
- then have "card ?A \<noteq> 0"
- apply -
- apply (rule ccontr)
- apply auto
- done
+ using assms by (intro kuhn_combinatorial[of p n label]) auto
then have "?A \<noteq> {}"
- unfolding card_eq_0_iff by auto
- then obtain s where "s \<in> ?A"
- by auto note s=conjD[OF this[unfolded mem_Collect_eq]]
- obtain a b where ab:
- "a \<in> s"
- "b \<in> s"
- "a \<noteq> b"
- "\<forall>x\<in>s. kle n a x \<and> kle n x b"
- "\<forall>i. b i = (if i \<in> {1..n} then a i + 1 else a i)"
- by (rule ksimplex_extrema_strong[OF s(1) `n \<noteq> 0`])
+ by (intro notI) simp
+ then obtain s b u where "kuhn_simplex p n b u s" and rl: "?rl ` s = {..n}"
+ by (auto elim: ksimplex.cases)
+ interpret kuhn_simplex p n b u s by fact
+
show ?thesis
- apply (rule that[of a])
- apply (rule_tac[!] ballI)
- proof -
- fix i
- assume "i \<in> {1..n}"
- then have "a i + 1 \<le> p"
- apply -
- apply (rule order_trans[of _ "b i"])
- apply (subst ab(5)[THEN spec[where x=i]])
- using s(1)[unfolded ksimplex_def]
- defer
- apply -
- apply (erule conjE)+
- apply (drule_tac bspec[OF _ ab(2)])+
- apply auto
- done
- then show "a i < p"
- by auto
+ proof (intro that[of b] allI impI)
+ fix i assume "i < n" then show "b i < p"
+ using base by auto
next
case goal2
- then have "i \<in> reduced label n ` s"
- using s by auto
- then obtain u where u: "u \<in> s" "i = reduced label n u"
- unfolding image_iff ..
- from goal2 have "i - 1 \<in> reduced label n ` s"
- using s by auto
- then obtain v where v: "v \<in> s" "i - 1 = reduced label n v"
- unfolding image_iff ..
- show ?case
- apply (rule_tac x = u in exI)
- apply (rule_tac x = v in exI)
- apply (rule conjI)
- defer
- apply (rule conjI)
- defer 2
- apply (rule_tac[1-2] ballI)
- proof -
- show "label u i \<noteq> label v i"
- using reduced_labelling [of label n u] reduced_labelling [of label n v]
- unfolding u(2)[symmetric] v(2)[symmetric]
- using goal2
- apply auto
- done
- fix j
- assume j: "j \<in> {1..n}"
- show "a j \<le> u j \<and> u j \<le> a j + 1" and "a j \<le> v j \<and> v j \<le> a j + 1"
- using conjD[OF ab(4)[rule_format, OF u(1)]]
- and conjD[OF ab(4)[rule_format, OF v(1)]]
- apply -
- apply (drule_tac[!] kle_imp_pointwise)+
- apply (erule_tac[!] x=j in allE)+
- unfolding ab(5)[rule_format]
- using j
- apply auto
- done
- qed
+ then have "i \<in> {.. n}" "Suc i \<in> {.. n}"
+ by auto
+ then obtain u v where u: "u \<in> s" "Suc i = ?rl u" and v: "v \<in> s" "i = ?rl v"
+ unfolding rl[symmetric] by blast
+
+ have "label u i \<noteq> label v i"
+ using reduced_labelling [of n "label u"] reduced_labelling [of n "label v"]
+ u(2)[symmetric] v(2)[symmetric] `i < n`
+ by auto
+ moreover
+ { fix j assume "j < n"
+ then have "b j \<le> u j" "u j \<le> b j + 1" "b j \<le> v j" "v j \<le> b j + 1"
+ using base_le[OF `u\<in>s`] le_Suc_base[OF `u\<in>s`] base_le[OF `v\<in>s`] le_Suc_base[OF `v\<in>s`] by auto }
+ ultimately show ?case
+ by blast
qed
qed
-
subsection {* The main result for the unit cube *}
lemma kuhn_labelling_lemma':
@@ -3970,78 +1636,51 @@
then have "p > 0"
using p by auto
- obtain b :: "nat \<Rightarrow> 'a" where b: "bij_betw b {1..n} Basis"
+ obtain b :: "nat \<Rightarrow> 'a" where b: "bij_betw b {..< n} Basis"
by atomize_elim (auto simp: n_def intro!: finite_same_card_bij)
- def b' \<equiv> "inv_into {1..n} b"
- then have b': "bij_betw b' Basis {1..n}"
+ def b' \<equiv> "inv_into {..< n} b"
+ then have b': "bij_betw b' Basis {..< n}"
using bij_betw_inv_into[OF b] by auto
- then have b'_Basis: "\<And>i. i \<in> Basis \<Longrightarrow> b' i \<in> {Suc 0 .. n}"
+ then have b'_Basis: "\<And>i. i \<in> Basis \<Longrightarrow> b' i \<in> {..< n}"
unfolding bij_betw_def by (auto simp: set_eq_iff)
have bb'[simp]:"\<And>i. i \<in> Basis \<Longrightarrow> b (b' i) = i"
unfolding b'_def
using b
by (auto simp: f_inv_into_f bij_betw_def)
- have b'b[simp]:"\<And>i. i \<in> {1..n} \<Longrightarrow> b' (b i) = i"
+ have b'b[simp]:"\<And>i. i < n \<Longrightarrow> b' (b i) = i"
unfolding b'_def
using b
by (auto simp: inv_into_f_eq bij_betw_def)
have *: "\<And>x :: nat. x = 0 \<or> x = 1 \<longleftrightarrow> x \<le> 1"
by auto
- have b'': "\<And>j. j \<in> {Suc 0..n} \<Longrightarrow> b j \<in> Basis"
+ have b'': "\<And>j. j < n \<Longrightarrow> b j \<in> Basis"
using b unfolding bij_betw_def by auto
- have q1: "0 < p" "0 < n" "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow>
- (\<forall>i\<in>{1..n}. (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0 \<or>
- (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 1)"
+ have q1: "0 < p" "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow>
+ (\<forall>i<n. (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0 \<or>
+ (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 1)"
unfolding *
using `p > 0` `n > 0`
using label(1)[OF b'']
by auto
- have q2: "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. x i = 0 \<longrightarrow>
+ { fix x :: "nat \<Rightarrow> nat" and i assume "\<forall>i<n. x i \<le> p" "i < n" "x i = p \<or> x i = 0"
+ then have "(\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<in> (unit_cube::'a set)"
+ using b'_Basis
+ by (auto simp add: mem_unit_cube inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1) }
+ note cube = this
+ have q2: "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = 0 \<longrightarrow>
(label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0)"
- "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. x i = p \<longrightarrow>
+ unfolding o_def using cube `p > 0` by (intro allI impI label(2)) (auto simp add: b'')
+ have q3: "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = p \<longrightarrow>
(label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 1)"
- apply rule
- apply rule
- apply rule
- apply rule
- defer
- apply rule
- apply rule
- apply rule
- apply rule
- proof -
- fix x i
- assume as: "\<forall>i\<in>{1..n}. x i \<le> p" "i \<in> {1..n}"
- {
- assume "x i = p \<or> x i = 0"
- have "(\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<in> (unit_cube::'a set)"
- unfolding mem_unit_cube
- using as b'_Basis
- by (auto simp add: inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1)
- }
- note cube = this
- {
- assume "x i = p"
- then show "(label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 1"
- unfolding o_def
- using cube as `p > 0`
- by (intro label(3)) (auto simp add: b'')
- }
- {
- assume "x i = 0"
- then show "(label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0"
- unfolding o_def using cube as `p > 0`
- by (intro label(2)) (auto simp add: b'')
- }
- qed
+ using cube `p > 0` unfolding o_def by (intro allI impI label(3)) (auto simp add: b'')
obtain q where q:
- "\<forall>i\<in>{1..n}. q i < p"
- "\<forall>i\<in>{1..n}.
- \<exists>r s. (\<forall>j\<in>{1..n}. q j \<le> r j \<and> r j \<le> q j + 1) \<and>
- (\<forall>j\<in>{1..n}. q j \<le> s j \<and> s j \<le> q j + 1) \<and>
+ "\<forall>i<n. q i < p"
+ "\<forall>i<n.
+ \<exists>r s. (\<forall>j<n. q j \<le> r j \<and> r j \<le> q j + 1) \<and>
+ (\<forall>j<n. q j \<le> s j \<and> s j \<le> q j + 1) \<and>
(label (\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i) \<circ> b) i \<noteq>
(label (\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i) \<circ> b) i"
- by (rule kuhn_lemma[OF q1 q2])
+ by (rule kuhn_lemma[OF q1 q2 q3])
def z \<equiv> "(\<Sum>i\<in>Basis. (real (q (b' i)) / real p) *\<^sub>R i)::'a"
have "\<exists>i\<in>Basis. d / real n \<le> abs ((f z - z)\<bullet>i)"
proof (rule ccontr)
@@ -4051,13 +1690,13 @@
then have "z \<in> unit_cube"
unfolding z_def mem_unit_cube
using b'_Basis
- by (auto simp add: inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1)
+ by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1)
then have d_fz_z: "d \<le> norm (f z - z)"
by (rule d)
assume "\<not> ?thesis"
then have as: "\<forall>i\<in>Basis. \<bar>f z \<bullet> i - z \<bullet> i\<bar> < d / real n"
using `n > 0`
- by (auto simp add: not_le inner_simps)
+ by (auto simp add: not_le inner_diff)
have "norm (f z - z) \<le> (\<Sum>i\<in>Basis. \<bar>f z \<bullet> i - z \<bullet> i\<bar>)"
unfolding inner_diff_left[symmetric]
by (rule norm_le_l1)
@@ -4073,16 +1712,16 @@
using d_fz_z by auto
qed
then obtain i where i: "i \<in> Basis" "d / real n \<le> \<bar>(f z - z) \<bullet> i\<bar>" ..
- have *: "b' i \<in> {1..n}"
+ have *: "b' i < n"
using i and b'[unfolded bij_betw_def]
by auto
obtain r s where rs:
- "\<And>j. j \<in> {1..n} \<Longrightarrow> q j \<le> r j \<and> r j \<le> q j + 1"
- "\<And>j. j \<in> {1..n} \<Longrightarrow> q j \<le> s j \<and> s j \<le> q j + 1"
+ "\<And>j. j < n \<Longrightarrow> q j \<le> r j \<and> r j \<le> q j + 1"
+ "\<And>j. j < n \<Longrightarrow> q j \<le> s j \<and> s j \<le> q j + 1"
"(label (\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i) \<circ> b) (b' i) \<noteq>
(label (\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i) \<circ> b) (b' i)"
using q(2)[rule_format,OF *] by blast
- have b'_im: "\<And>i. i \<in> Basis \<Longrightarrow> b' i \<in> {1..n}"
+ have b'_im: "\<And>i. i \<in> Basis \<Longrightarrow> b' i < n"
using b' unfolding bij_betw_def by auto
def r' \<equiv> "(\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i)::'a"
have "\<And>i. i \<in> Basis \<Longrightarrow> r (b' i) \<le> p"
@@ -4094,7 +1733,7 @@
then have "r' \<in> unit_cube"
unfolding r'_def mem_unit_cube
using b'_Basis
- by (auto simp add: inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1)
+ by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1)
def s' \<equiv> "(\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i)::'a"
have "\<And>i. i \<in> Basis \<Longrightarrow> s (b' i) \<le> p"
apply (rule order_trans)
@@ -4105,11 +1744,11 @@
then have "s' \<in> unit_cube"
unfolding s'_def mem_unit_cube
using b'_Basis
- by (auto simp add: inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1)
+ by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1)
have "z \<in> unit_cube"
unfolding z_def mem_unit_cube
using b'_Basis q(1)[rule_format,OF b'_im] `p > 0`
- by (auto simp add: inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1 less_imp_le)
+ by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1 less_imp_le)
have *: "\<And>x. 1 + real x = real (Suc x)"
by auto
{
@@ -4402,62 +2041,4 @@
using x assms by auto
qed
-
-subsection {*Bijections between intervals. *}
-
-definition interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::euclidean_space"
- where "interval_bij =
- (\<lambda>(a, b) (u, v) x. (\<Sum>i\<in>Basis. (u\<bullet>i + (x\<bullet>i - a\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (v\<bullet>i - u\<bullet>i)) *\<^sub>R i))"
-
-lemma interval_bij_affine:
- "interval_bij (a,b) (u,v) = (\<lambda>x. (\<Sum>i\<in>Basis. ((v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (x\<bullet>i)) *\<^sub>R i) +
- (\<Sum>i\<in>Basis. (u\<bullet>i - (v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (a\<bullet>i)) *\<^sub>R i))"
- by (auto simp: setsum_addf[symmetric] scaleR_add_left[symmetric] interval_bij_def fun_eq_iff
- field_simps inner_simps add_divide_distrib[symmetric] intro!: setsum_cong)
-
-lemma continuous_interval_bij:
- fixes a b :: "'a::euclidean_space"
- shows "continuous (at x) (interval_bij (a, b) (u, v))"
- by (auto simp add: divide_inverse interval_bij_def intro!: continuous_setsum continuous_intros)
-
-lemma continuous_on_interval_bij: "continuous_on s (interval_bij (a, b) (u, v))"
- apply(rule continuous_at_imp_continuous_on)
- apply (rule, rule continuous_interval_bij)
- done
-
-lemma in_interval_interval_bij:
- fixes a b u v x :: "'a::euclidean_space"
- assumes "x \<in> cbox a b"
- and "cbox u v \<noteq> {}"
- shows "interval_bij (a, b) (u, v) x \<in> cbox u v"
- apply (simp only: interval_bij_def split_conv mem_box inner_setsum_left_Basis cong: ball_cong)
- apply safe
-proof -
- fix i :: 'a
- assume i: "i \<in> Basis"
- have "cbox a b \<noteq> {}"
- using assms by auto
- with i have *: "a\<bullet>i \<le> b\<bullet>i" "u\<bullet>i \<le> v\<bullet>i"
- using assms(2) by (auto simp add: box_eq_empty)
- have x: "a\<bullet>i\<le>x\<bullet>i" "x\<bullet>i\<le>b\<bullet>i"
- using assms(1)[unfolded mem_box] using i by auto
- have "0 \<le> (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
- using * x by (auto intro!: mult_nonneg_nonneg divide_nonneg_nonneg)
- then show "u \<bullet> i \<le> u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
- using * by auto
- have "((x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (v \<bullet> i - u \<bullet> i) \<le> 1 * (v \<bullet> i - u \<bullet> i)"
- apply (rule mult_right_mono)
- unfolding divide_le_eq_1
- using * x
- apply auto
- done
- then show "u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i) \<le> v \<bullet> i"
- using * by auto
-qed
-
-lemma interval_bij_bij:
- "\<forall>(i::'a::euclidean_space)\<in>Basis. a\<bullet>i < b\<bullet>i \<and> u\<bullet>i < v\<bullet>i \<Longrightarrow>
- interval_bij (a, b) (u, v) (interval_bij (u, v) (a, b) x) = x"
- by (auto simp: interval_bij_def euclidean_eq_iff[where 'a='a])
-
end