99 subsection {* The odd/even result for faces of complete vertices, generalized. *} |
99 subsection {* The odd/even result for faces of complete vertices, generalized. *} |
100 |
100 |
101 lemma card_1_exists: "card s = 1 \<longleftrightarrow> (\<exists>!x. x \<in> s)" unfolding One_nat_def |
101 lemma card_1_exists: "card s = 1 \<longleftrightarrow> (\<exists>!x. x \<in> s)" unfolding One_nat_def |
102 apply rule apply(drule card_eq_SucD) defer apply(erule ex1E) proof- |
102 apply rule apply(drule card_eq_SucD) defer apply(erule ex1E) proof- |
103 fix x assume as:"x \<in> s" "\<forall>y. y \<in> s \<longrightarrow> y = x" |
103 fix x assume as:"x \<in> s" "\<forall>y. y \<in> s \<longrightarrow> y = x" |
104 have *:"s = insert x {}" apply- apply(rule set_ext,rule) unfolding singleton_iff |
104 have *:"s = insert x {}" apply- apply(rule set_eqI,rule) unfolding singleton_iff |
105 apply(rule as(2)[rule_format]) using as(1) by auto |
105 apply(rule as(2)[rule_format]) using as(1) by auto |
106 show "card s = Suc 0" unfolding * using card_insert by auto qed auto |
106 show "card s = Suc 0" unfolding * using card_insert by auto qed auto |
107 |
107 |
108 lemma card_2_exists: "card s = 2 \<longleftrightarrow> (\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. (z = x) \<or> (z = y)))" proof |
108 lemma card_2_exists: "card s = 2 \<longleftrightarrow> (\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. (z = x) \<or> (z = y)))" proof |
109 assume "card s = 2" then obtain x y where obt:"s = {x, y}" "x\<noteq>y" unfolding numeral_2_eq_2 apply - apply(erule exE conjE|drule card_eq_SucD)+ by auto |
109 assume "card s = 2" then obtain x y where obt:"s = {x, y}" "x\<noteq>y" unfolding numeral_2_eq_2 apply - apply(erule exE conjE|drule card_eq_SucD)+ by auto |
120 |
120 |
121 lemma image_lemma_1: assumes "finite s" "finite t" "card s = card t" "f ` s = t" "b \<in> t" |
121 lemma image_lemma_1: assumes "finite s" "finite t" "card s = card t" "f ` s = t" "b \<in> t" |
122 shows "card {s'. \<exists>a\<in>s. s' = s - {a} \<and> f ` s' = t - {b}} = 1" proof- |
122 shows "card {s'. \<exists>a\<in>s. s' = s - {a} \<and> f ` s' = t - {b}} = 1" proof- |
123 obtain a where a:"b = f a" "a\<in>s" using assms(4-5) by auto |
123 obtain a where a:"b = f a" "a\<in>s" using assms(4-5) by auto |
124 have inj:"inj_on f s" apply(rule eq_card_imp_inj_on) using assms(1-4) by auto |
124 have inj:"inj_on f s" apply(rule eq_card_imp_inj_on) using assms(1-4) by auto |
125 have *:"{a \<in> s. f ` (s - {a}) = t - {b}} = {a}" apply(rule set_ext) unfolding singleton_iff |
125 have *:"{a \<in> s. f ` (s - {a}) = t - {b}} = {a}" apply(rule set_eqI) unfolding singleton_iff |
126 apply(rule,rule inj[unfolded inj_on_def,rule_format]) unfolding a using a(2) and assms and inj[unfolded inj_on_def] by auto |
126 apply(rule,rule inj[unfolded inj_on_def,rule_format]) unfolding a using a(2) and assms and inj[unfolded inj_on_def] by auto |
127 show ?thesis apply(rule image_lemma_0) unfolding * by auto qed |
127 show ?thesis apply(rule image_lemma_0) unfolding * by auto qed |
128 |
128 |
129 lemma image_lemma_2: assumes "finite s" "finite t" "card s = card t" "f ` s \<subseteq> t" "f ` s \<noteq> t" "b \<in> t" |
129 lemma image_lemma_2: assumes "finite s" "finite t" "card s = card t" "f ` s \<subseteq> t" "f ` s \<noteq> t" "b \<in> t" |
130 shows "(card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> f ` s' = t - {b}} = 0) \<or> |
130 shows "(card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> f ` s' = t - {b}} = 0) \<or> |
133 next let ?M = "{a\<in>s. f ` (s - {a}) = t - {b}}" |
133 next let ?M = "{a\<in>s. f ` (s - {a}) = t - {b}}" |
134 case False then obtain a where "a\<in>?M" by auto hence a:"a\<in>s" "f ` (s - {a}) = t - {b}" by auto |
134 case False then obtain a where "a\<in>?M" by auto hence a:"a\<in>s" "f ` (s - {a}) = t - {b}" by auto |
135 have "f a \<in> t - {b}" using a and assms by auto |
135 have "f a \<in> t - {b}" using a and assms by auto |
136 hence "\<exists>c \<in> s - {a}. f a = f c" unfolding image_iff[symmetric] and a by auto |
136 hence "\<exists>c \<in> s - {a}. f a = f c" unfolding image_iff[symmetric] and a by auto |
137 then obtain c where c:"c \<in> s" "a \<noteq> c" "f a = f c" by auto |
137 then obtain c where c:"c \<in> s" "a \<noteq> c" "f a = f c" by auto |
138 hence *:"f ` (s - {c}) = f ` (s - {a})" apply-apply(rule set_ext,rule) proof- |
138 hence *:"f ` (s - {c}) = f ` (s - {a})" apply-apply(rule set_eqI,rule) proof- |
139 fix x assume "x \<in> f ` (s - {a})" then obtain y where y:"f y = x" "y\<in>s- {a}" by auto |
139 fix x assume "x \<in> f ` (s - {a})" then obtain y where y:"f y = x" "y\<in>s- {a}" by auto |
140 thus "x \<in> f ` (s - {c})" unfolding image_iff apply(rule_tac x="if y = c then a else y" in bexI) using c a by auto qed auto |
140 thus "x \<in> f ` (s - {c})" unfolding image_iff apply(rule_tac x="if y = c then a else y" in bexI) using c a by auto qed auto |
141 have "c\<in>?M" unfolding mem_Collect_eq and * using a and c(1) by auto |
141 have "c\<in>?M" unfolding mem_Collect_eq and * using a and c(1) by auto |
142 show ?thesis apply(rule disjI2, rule image_lemma_0) unfolding card_2_exists |
142 show ?thesis apply(rule disjI2, rule image_lemma_0) unfolding card_2_exists |
143 apply(rule bexI[OF _ `a\<in>?M`], rule bexI[OF _ `c\<in>?M`],rule,rule `a\<noteq>c`) proof(rule,unfold mem_Collect_eq,erule conjE) |
143 apply(rule bexI[OF _ `a\<in>?M`], rule bexI[OF _ `c\<in>?M`],rule,rule `a\<noteq>c`) proof(rule,unfold mem_Collect_eq,erule conjE) |
163 apply(rule finite_UN_I[OF assms(1)]) using ** by auto |
163 apply(rule finite_UN_I[OF assms(1)]) using ** by auto |
164 have *:"\<And> P f s. s\<in>simplices \<Longrightarrow> (f \<in> {f. \<exists>s\<in>simplices. \<exists>a\<in>s. f = s - {a}}) \<and> |
164 have *:"\<And> P f s. s\<in>simplices \<Longrightarrow> (f \<in> {f. \<exists>s\<in>simplices. \<exists>a\<in>s. f = s - {a}}) \<and> |
165 (\<exists>a\<in>s. (f = s - {a})) \<and> P f \<longleftrightarrow> (\<exists>a\<in>s. (f = s - {a}) \<and> P f)" by auto |
165 (\<exists>a\<in>s. (f = s - {a})) \<and> P f \<longleftrightarrow> (\<exists>a\<in>s. (f = s - {a}) \<and> P f)" by auto |
166 fix s assume s:"s\<in>simplices" let ?S = "{f \<in> {f. \<exists>s\<in>simplices. face f s}. face f s \<and> rl ` f = {0..n}}" |
166 fix s assume s:"s\<in>simplices" let ?S = "{f \<in> {f. \<exists>s\<in>simplices. face f s}. face f s \<and> rl ` f = {0..n}}" |
167 have "{0..n + 1} - {n + 1} = {0..n}" by auto |
167 have "{0..n + 1} - {n + 1} = {0..n}" by auto |
168 hence S:"?S = {s'. \<exists>a\<in>s. s' = s - {a} \<and> rl ` s' = {0..n + 1} - {n + 1}}" apply- apply(rule set_ext) |
168 hence S:"?S = {s'. \<exists>a\<in>s. s' = s - {a} \<and> rl ` s' = {0..n + 1} - {n + 1}}" apply- apply(rule set_eqI) |
169 unfolding assms(2)[rule_format] mem_Collect_eq and *[OF s, unfolded mem_Collect_eq, where P="\<lambda>x. rl ` x = {0..n}"] by auto |
169 unfolding assms(2)[rule_format] mem_Collect_eq and *[OF s, unfolded mem_Collect_eq, where P="\<lambda>x. rl ` x = {0..n}"] by auto |
170 show "rl ` s = {0..n+1} \<Longrightarrow> card ?S = 1" "rl ` s \<noteq> {0..n+1} \<Longrightarrow> card ?S = 0 \<or> card ?S = 2" unfolding S |
170 show "rl ` s = {0..n+1} \<Longrightarrow> card ?S = 1" "rl ` s \<noteq> {0..n+1} \<Longrightarrow> card ?S = 0 \<or> card ?S = 2" unfolding S |
171 apply(rule_tac[!] image_lemma_1 image_lemma_2) using ** assms(4) and s by auto qed |
171 apply(rule_tac[!] image_lemma_1 image_lemma_2) using ** assms(4) and s by auto qed |
172 |
172 |
173 subsection {*We use the following notion of ordering rather than pointwise indexing. *} |
173 subsection {*We use the following notion of ordering rather than pointwise indexing. *} |
491 subsection {* The lemmas about simplices that we need. *} |
491 subsection {* The lemmas about simplices that we need. *} |
492 |
492 |
493 lemma card_funspace': assumes "finite s" "finite t" "card s = m" "card t = n" |
493 lemma card_funspace': assumes "finite s" "finite t" "card s = m" "card t = n" |
494 shows "card {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)} = n ^ m" (is "card (?M s) = _") |
494 shows "card {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)} = n ^ m" (is "card (?M s) = _") |
495 using assms apply - proof(induct m arbitrary: s) |
495 using assms apply - proof(induct m arbitrary: s) |
496 have *:"{f. \<forall>x. f x = d} = {\<lambda>x. d}" apply(rule set_ext,rule)unfolding mem_Collect_eq apply(rule,rule ext) by auto |
496 have *:"{f. \<forall>x. f x = d} = {\<lambda>x. d}" apply(rule set_eqI,rule)unfolding mem_Collect_eq apply(rule,rule ext) by auto |
497 case 0 thus ?case by(auto simp add: *) next |
497 case 0 thus ?case by(auto simp add: *) next |
498 case (Suc m) guess a using card_eq_SucD[OF Suc(4)] .. then guess s0 |
498 case (Suc m) guess a using card_eq_SucD[OF Suc(4)] .. then guess s0 |
499 apply(erule_tac exE) apply(erule conjE)+ . note as0 = this |
499 apply(erule_tac exE) apply(erule conjE)+ . note as0 = this |
500 have **:"card s0 = m" using as0 using Suc(2) Suc(4) by auto |
500 have **:"card s0 = m" using as0 using Suc(2) Suc(4) by auto |
501 let ?l = "(\<lambda>(b,g) x. if x = a then b else g x)" have *:"?M (insert a s0) = ?l ` {(b,g). b\<in>t \<and> g\<in>?M s0}" |
501 let ?l = "(\<lambda>(b,g) x. if x = a then b else g x)" have *:"?M (insert a s0) = ?l ` {(b,g). b\<in>t \<and> g\<in>?M s0}" |
502 apply(rule set_ext,rule) unfolding mem_Collect_eq image_iff apply(erule conjE) |
502 apply(rule set_eqI,rule) unfolding mem_Collect_eq image_iff apply(erule conjE) |
503 apply(rule_tac x="(x a, \<lambda>y. if y\<in>s0 then x y else d)" in bexI) apply(rule ext) prefer 3 apply rule defer |
503 apply(rule_tac x="(x a, \<lambda>y. if y\<in>s0 then x y else d)" in bexI) apply(rule ext) prefer 3 apply rule defer |
504 apply(erule bexE,rule) unfolding mem_Collect_eq apply(erule splitE)+ apply(erule conjE)+ proof- |
504 apply(erule bexE,rule) unfolding mem_Collect_eq apply(erule splitE)+ apply(erule conjE)+ proof- |
505 fix x xa xb xc y assume as:"x = (\<lambda>(b, g) x. if x = a then b else g x) xa" "xb \<in> UNIV - insert a s0" "xa = (xc, y)" "xc \<in> t" |
505 fix x xa xb xc y assume as:"x = (\<lambda>(b, g) x. if x = a then b else g x) xa" "xb \<in> UNIV - insert a s0" "xa = (xc, y)" "xc \<in> t" |
506 "\<forall>x\<in>s0. y x \<in> t" "\<forall>x\<in>UNIV - s0. y x = d" thus "x xb = d" unfolding as by auto qed auto |
506 "\<forall>x\<in>s0. y x \<in> t" "\<forall>x\<in>UNIV - s0. y x = d" thus "x xb = d" unfolding as by auto qed auto |
507 have inj:"inj_on ?l {(b,g). b\<in>t \<and> g\<in>?M s0}" unfolding inj_on_def apply(rule,rule,rule) unfolding mem_Collect_eq apply(erule splitE conjE)+ proof- |
507 have inj:"inj_on ?l {(b,g). b\<in>t \<and> g\<in>?M s0}" unfolding inj_on_def apply(rule,rule,rule) unfolding mem_Collect_eq apply(erule splitE conjE)+ proof- |
723 show "a1\<in>s'" using a' unfolding `a=a0` using a0a1 by auto |
723 show "a1\<in>s'" using a' unfolding `a=a0` using a0a1 by auto |
724 show "a_max \<in> s" proof(rule ccontr) assume "a_max\<notin>s" |
724 show "a_max \<in> s" proof(rule ccontr) assume "a_max\<notin>s" |
725 hence "a_max = a'" using a' min_max by auto |
725 hence "a_max = a'" using a' min_max by auto |
726 thus False unfolding True using min_max by auto qed qed |
726 thus False unfolding True using min_max by auto qed qed |
727 hence "\<forall>i. a_max i = a1 i" by auto |
727 hence "\<forall>i. a_max i = a1 i" by auto |
728 hence "a' = a" unfolding True `a=a0` apply-apply(subst ext_iff,rule) |
728 hence "a' = a" unfolding True `a=a0` apply-apply(subst fun_eq_iff,rule) |
729 apply(erule_tac x=x in allE) unfolding a0a1(5)[rule_format] min_max(5)[rule_format] |
729 apply(erule_tac x=x in allE) unfolding a0a1(5)[rule_format] min_max(5)[rule_format] |
730 proof- case goal1 thus ?case apply(cases "x\<in>{1..n}") by auto qed |
730 proof- case goal1 thus ?case apply(cases "x\<in>{1..n}") by auto qed |
731 hence "s' = s" apply-apply(rule lem1[OF a'(2)]) using `a\<in>s` `a'\<in>s'` by auto |
731 hence "s' = s" apply-apply(rule lem1[OF a'(2)]) using `a\<in>s` `a'\<in>s'` by auto |
732 thus ?thesis by auto next |
732 thus ?thesis by auto next |
733 case False hence as:"a' = a_max" using ** by auto |
733 case False hence as:"a' = a_max" using ** by auto |
736 show "a_min \<in> s - {a0}" unfolding a'(2)[THEN sym,unfolded `a=a0`] |
736 show "a_min \<in> s - {a0}" unfolding a'(2)[THEN sym,unfolded `a=a0`] |
737 unfolding as using min_max(1-3) by auto |
737 unfolding as using min_max(1-3) by auto |
738 have "a2 \<noteq> a" unfolding `a=a0` using k(2)[rule_format,of k] by auto |
738 have "a2 \<noteq> a" unfolding `a=a0` using k(2)[rule_format,of k] by auto |
739 hence "a2 \<in> s - {a}" using a2 by auto thus "a2 \<in> s'" unfolding a'(2)[THEN sym] by auto qed |
739 hence "a2 \<in> s - {a}" using a2 by auto thus "a2 \<in> s'" unfolding a'(2)[THEN sym] by auto qed |
740 hence "\<forall>i. a_min i = a2 i" by auto |
740 hence "\<forall>i. a_min i = a2 i" by auto |
741 hence "a' = a3" unfolding as `a=a0` apply-apply(subst ext_iff,rule) |
741 hence "a' = a3" unfolding as `a=a0` apply-apply(subst fun_eq_iff,rule) |
742 apply(erule_tac x=x in allE) unfolding a0a1(5)[rule_format] min_max(5)[rule_format] |
742 apply(erule_tac x=x in allE) unfolding a0a1(5)[rule_format] min_max(5)[rule_format] |
743 unfolding a3_def k(2)[rule_format] unfolding a0a1(5)[rule_format] proof- case goal1 |
743 unfolding a3_def k(2)[rule_format] unfolding a0a1(5)[rule_format] proof- case goal1 |
744 show ?case unfolding goal1 apply(cases "x\<in>{1..n}") defer apply(cases "x=k") |
744 show ?case unfolding goal1 apply(cases "x\<in>{1..n}") defer apply(cases "x=k") |
745 using `k\<in>{1..n}` by auto qed |
745 using `k\<in>{1..n}` by auto qed |
746 hence "s' = insert a3 (s - {a0})" apply-apply(rule lem1) defer apply assumption |
746 hence "s' = insert a3 (s - {a0})" apply-apply(rule lem1) defer apply assumption |
832 have *:"\<forall>j. a2 j = (if j\<in>{1..n} then a3 j + 1 else a3 j)" |
832 have *:"\<forall>j. a2 j = (if j\<in>{1..n} then a3 j + 1 else a3 j)" |
833 using k(2) unfolding lem4[rule_format] a0a1(5)[rule_format] apply-apply(rule,erule_tac x=j in allE) |
833 using k(2) unfolding lem4[rule_format] a0a1(5)[rule_format] apply-apply(rule,erule_tac x=j in allE) |
834 proof- case goal1 thus ?case apply(cases "j\<in>{1..n}",case_tac[!] "j=k") by auto qed |
834 proof- case goal1 thus ?case apply(cases "j\<in>{1..n}",case_tac[!] "j=k") by auto qed |
835 have "\<forall>i. a_min i = a3 i" using a_max apply-apply(rule,erule_tac x=i in allE) |
835 have "\<forall>i. a_min i = a3 i" using a_max apply-apply(rule,erule_tac x=i in allE) |
836 unfolding min_max(5)[rule_format] *[rule_format] proof- case goal1 |
836 unfolding min_max(5)[rule_format] *[rule_format] proof- case goal1 |
837 thus ?case apply(cases "i\<in>{1..n}") by auto qed hence "a_min = a3" unfolding ext_iff . |
837 thus ?case apply(cases "i\<in>{1..n}") by auto qed hence "a_min = a3" unfolding fun_eq_iff . |
838 hence "s' = insert a3 (s - {a1})" using a' unfolding `a=a1` True by auto thus ?thesis by auto next |
838 hence "s' = insert a3 (s - {a1})" using a' unfolding `a=a1` True by auto thus ?thesis by auto next |
839 case False hence as:"a'=a_max" using ** by auto |
839 case False hence as:"a'=a_max" using ** by auto |
840 have "a_min = a0" unfolding kle_antisym[THEN sym,of _ _ n] apply(rule) |
840 have "a_min = a0" unfolding kle_antisym[THEN sym,of _ _ n] apply(rule) |
841 apply(rule min_max(4)[rule_format,THEN conjunct1]) defer apply(rule a0a1(4)[rule_format,THEN conjunct1]) proof- |
841 apply(rule min_max(4)[rule_format,THEN conjunct1]) defer apply(rule a0a1(4)[rule_format,THEN conjunct1]) proof- |
842 have "a_min \<in> s - {a1}" using min_max(1,3) unfolding a'(2)[THEN sym,unfolded `a=a1`] as by auto |
842 have "a_min \<in> s - {a1}" using min_max(1,3) unfolding a'(2)[THEN sym,unfolded `a=a1`] as by auto |
843 thus "a_min \<in> s" by auto have "a0 \<in> s - {a1}" using a0a1(1-3) by auto thus "a0 \<in> s'" |
843 thus "a_min \<in> s" by auto have "a0 \<in> s - {a1}" using a0a1(1-3) by auto thus "a0 \<in> s'" |
844 unfolding a'(2)[THEN sym,unfolded `a=a1`] by auto qed |
844 unfolding a'(2)[THEN sym,unfolded `a=a1`] by auto qed |
845 hence "\<forall>i. a_max i = a1 i" unfolding a0a1(5)[rule_format] min_max(5)[rule_format] by auto |
845 hence "\<forall>i. a_max i = a1 i" unfolding a0a1(5)[rule_format] min_max(5)[rule_format] by auto |
846 hence "s' = s" apply-apply(rule lem1[OF a'(2)]) using `a\<in>s` `a'\<in>s'` unfolding as `a=a1` unfolding ext_iff by auto |
846 hence "s' = s" apply-apply(rule lem1[OF a'(2)]) using `a\<in>s` `a'\<in>s'` unfolding as `a=a1` unfolding fun_eq_iff by auto |
847 thus ?thesis by auto qed qed |
847 thus ?thesis by auto qed qed |
848 ultimately have *:"?A = {s, insert a3 (s - {a1})}" by blast |
848 ultimately have *:"?A = {s, insert a3 (s - {a1})}" by blast |
849 have "s \<noteq> insert a3 (s - {a1})" using `a3\<notin>s` by auto |
849 have "s \<noteq> insert a3 (s - {a1})" using `a3\<notin>s` by auto |
850 hence ?thesis unfolding * by auto } moreover |
850 hence ?thesis unfolding * by auto } moreover |
851 { assume as:"a\<noteq>a0" "a\<noteq>a1" have "\<not> (\<forall>x\<in>s. kle n a x)" proof case goal1 |
851 { assume as:"a\<noteq>a0" "a\<noteq>a1" have "\<not> (\<forall>x\<in>s. kle n a x)" proof case goal1 |
861 def a' \<equiv> "\<lambda>j. if j = l then u j + 1 else u j" |
861 def a' \<equiv> "\<lambda>j. if j = l then u j + 1 else u j" |
862 have kl:"k \<noteq> l" proof assume "k=l" have *:"\<And>P. (if P then (1::nat) else 0) \<noteq> 2" by auto |
862 have kl:"k \<noteq> l" proof assume "k=l" have *:"\<And>P. (if P then (1::nat) else 0) \<noteq> 2" by auto |
863 thus False using ksimplexD(6)[OF assms(1),rule_format,OF u v] unfolding kle_def |
863 thus False using ksimplexD(6)[OF assms(1),rule_format,OF u v] unfolding kle_def |
864 unfolding l(2) k(2) `k=l` apply-apply(erule disjE)apply(erule_tac[!] exE conjE)+ |
864 unfolding l(2) k(2) `k=l` apply-apply(erule disjE)apply(erule_tac[!] exE conjE)+ |
865 apply(erule_tac[!] x=l in allE)+ by(auto simp add: *) qed |
865 apply(erule_tac[!] x=l in allE)+ by(auto simp add: *) qed |
866 hence aa':"a'\<noteq>a" apply-apply rule unfolding ext_iff unfolding a'_def k(2) |
866 hence aa':"a'\<noteq>a" apply-apply rule unfolding fun_eq_iff unfolding a'_def k(2) |
867 apply(erule_tac x=l in allE) by auto |
867 apply(erule_tac x=l in allE) by auto |
868 have "a' \<notin> s" apply(rule) apply(drule ksimplexD(6)[OF assms(1),rule_format,OF `a\<in>s`]) proof(cases "kle n a a'") |
868 have "a' \<notin> s" apply(rule) apply(drule ksimplexD(6)[OF assms(1),rule_format,OF `a\<in>s`]) proof(cases "kle n a a'") |
869 case goal2 hence "kle n a' a" by auto thus False apply(drule_tac kle_imp_pointwise) |
869 case goal2 hence "kle n a' a" by auto thus False apply(drule_tac kle_imp_pointwise) |
870 apply(erule_tac x=l in allE) unfolding a'_def k(2) using kl by auto next |
870 apply(erule_tac x=l in allE) unfolding a'_def k(2) using kl by auto next |
871 case True thus False apply(drule_tac kle_imp_pointwise) |
871 case True thus False apply(drule_tac kle_imp_pointwise) |
875 apply(rule_tac[3] x="{l}" in exI,rule_tac[4] x="{k}" in exI) |
875 apply(rule_tac[3] x="{l}" in exI,rule_tac[4] x="{k}" in exI) |
876 unfolding l(2) k(2) a'_def using l(1) k(1) by auto |
876 unfolding l(2) k(2) a'_def using l(1) k(1) by auto |
877 have uxv:"\<And>x. kle n u x \<Longrightarrow> kle n x v \<Longrightarrow> (x = u) \<or> (x = a) \<or> (x = a') \<or> (x = v)" |
877 have uxv:"\<And>x. kle n u x \<Longrightarrow> kle n x v \<Longrightarrow> (x = u) \<or> (x = a) \<or> (x = a') \<or> (x = v)" |
878 proof- case goal1 thus ?case proof(cases "x k = u k", case_tac[!] "x l = u l") |
878 proof- case goal1 thus ?case proof(cases "x k = u k", case_tac[!] "x l = u l") |
879 assume as:"x l = u l" "x k = u k" |
879 assume as:"x l = u l" "x k = u k" |
880 have "x = u" unfolding ext_iff |
880 have "x = u" unfolding fun_eq_iff |
881 using goal1(2)[THEN kle_imp_pointwise,unfolded l(2)] unfolding k(2) apply- |
881 using goal1(2)[THEN kle_imp_pointwise,unfolded l(2)] unfolding k(2) apply- |
882 using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1 |
882 using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1 |
883 thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next |
883 thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next |
884 assume as:"x l \<noteq> u l" "x k = u k" |
884 assume as:"x l \<noteq> u l" "x k = u k" |
885 have "x = a'" unfolding ext_iff unfolding a'_def |
885 have "x = a'" unfolding fun_eq_iff unfolding a'_def |
886 using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply- |
886 using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply- |
887 using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1 |
887 using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1 |
888 thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next |
888 thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next |
889 assume as:"x l = u l" "x k \<noteq> u k" |
889 assume as:"x l = u l" "x k \<noteq> u k" |
890 have "x = a" unfolding ext_iff |
890 have "x = a" unfolding fun_eq_iff |
891 using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply- |
891 using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply- |
892 using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1 |
892 using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1 |
893 thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next |
893 thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next |
894 assume as:"x l \<noteq> u l" "x k \<noteq> u k" |
894 assume as:"x l \<noteq> u l" "x k \<noteq> u k" |
895 have "x = v" unfolding ext_iff |
895 have "x = v" unfolding fun_eq_iff |
896 using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply- |
896 using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply- |
897 using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1 |
897 using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1 |
898 thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as `k\<noteq>l` by auto qed thus ?case by auto qed qed |
898 thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as `k\<noteq>l` by auto qed thus ?case by auto qed qed |
899 have uv:"kle n u v" apply(rule kle_trans[OF kle_uv(1,3)]) using ksimplexD(6)[OF assms(1)] using u v by auto |
899 have uv:"kle n u v" apply(rule kle_trans[OF kle_uv(1,3)]) using ksimplexD(6)[OF assms(1)] using u v by auto |
900 have lem3:"\<And>x. x\<in>s \<Longrightarrow> kle n v x \<Longrightarrow> kle n a' x" apply(rule kle_between_r[of _ u _ v]) |
900 have lem3:"\<And>x. x\<in>s \<Longrightarrow> kle n v x \<Longrightarrow> kle n a' x" apply(rule kle_between_r[of _ u _ v]) |
933 apply(rule_tac x="a'" in bexI) using aa' `a'\<notin>s` by auto moreover |
933 apply(rule_tac x="a'" in bexI) using aa' `a'\<notin>s` by auto moreover |
934 have "s \<in> ?A" using assms(1,2) by auto ultimately have "?A \<supseteq> {s, insert a' (s - {a})}" by auto |
934 have "s \<in> ?A" using assms(1,2) by auto ultimately have "?A \<supseteq> {s, insert a' (s - {a})}" by auto |
935 moreover have "?A \<subseteq> {s, insert a' (s - {a})}" apply(rule) unfolding mem_Collect_eq proof(erule conjE) |
935 moreover have "?A \<subseteq> {s, insert a' (s - {a})}" apply(rule) unfolding mem_Collect_eq proof(erule conjE) |
936 fix s' assume as:"ksimplex p n s'" and "\<exists>b\<in>s'. s' - {b} = s - {a}" |
936 fix s' assume as:"ksimplex p n s'" and "\<exists>b\<in>s'. s' - {b} = s - {a}" |
937 from this(2) guess a'' .. note a''=this |
937 from this(2) guess a'' .. note a''=this |
938 have "u\<noteq>v" unfolding ext_iff unfolding l(2) k(2) by auto |
938 have "u\<noteq>v" unfolding fun_eq_iff unfolding l(2) k(2) by auto |
939 hence uv':"\<not> kle n v u" using uv using kle_antisym by auto |
939 hence uv':"\<not> kle n v u" using uv using kle_antisym by auto |
940 have "u\<noteq>a" "v\<noteq>a" unfolding ext_iff k(2) l(2) by auto |
940 have "u\<noteq>a" "v\<noteq>a" unfolding fun_eq_iff k(2) l(2) by auto |
941 hence uvs':"u\<in>s'" "v\<in>s'" using `u\<in>s` `v\<in>s` using a'' by auto |
941 hence uvs':"u\<in>s'" "v\<in>s'" using `u\<in>s` `v\<in>s` using a'' by auto |
942 have lem6:"a \<in> s' \<or> a' \<in> s'" proof(cases "\<forall>x\<in>s'. kle n x u \<or> kle n v x") |
942 have lem6:"a \<in> s' \<or> a' \<in> s'" proof(cases "\<forall>x\<in>s'. kle n x u \<or> kle n v x") |
943 case False then guess w unfolding ball_simps .. note w=this |
943 case False then guess w unfolding ball_simps .. note w=this |
944 hence "kle n u w" "kle n w v" using ksimplexD(6)[OF as] uvs' by auto |
944 hence "kle n u w" "kle n w v" using ksimplexD(6)[OF as] uvs' by auto |
945 hence "w = a' \<or> w = a" using uxv[of w] uvs' w by auto thus ?thesis using w by auto next |
945 hence "w = a' \<or> w = a" using uxv[of w] uvs' w by auto thus ?thesis using w by auto next |
1050 "\<forall>x. \<forall>j\<in>{1..n+1}. (\<forall>j. x j \<le> p) \<and> (x j = p) \<longrightarrow> (lab x j = 1)" |
1050 "\<forall>x. \<forall>j\<in>{1..n+1}. (\<forall>j. x j \<le> p) \<and> (x j = p) \<longrightarrow> (lab x j = 1)" |
1051 "odd (card {f. ksimplex p n f \<and> ((reduced lab n) ` f = {0..n})})" |
1051 "odd (card {f. ksimplex p n f \<and> ((reduced lab n) ` f = {0..n})})" |
1052 shows "odd (card {s. ksimplex p (n+1) s \<and>((reduced lab (n+1)) ` s = {0..n+1})})" proof- |
1052 shows "odd (card {s. ksimplex p (n+1) s \<and>((reduced lab (n+1)) ` s = {0..n+1})})" proof- |
1053 have *:"\<And>s t. odd (card s) \<Longrightarrow> s = t \<Longrightarrow> odd (card t)" "\<And>s f. (\<And>x. f x \<le> n +1 ) \<Longrightarrow> f ` s \<subseteq> {0..n+1}" by auto |
1053 have *:"\<And>s t. odd (card s) \<Longrightarrow> s = t \<Longrightarrow> odd (card t)" "\<And>s f. (\<And>x. f x \<le> n +1 ) \<Longrightarrow> f ` s \<subseteq> {0..n+1}" by auto |
1054 show ?thesis apply(rule kuhn_simplex_lemma[unfolded mem_Collect_eq]) apply(rule,rule,rule *,rule reduced_labelling) |
1054 show ?thesis apply(rule kuhn_simplex_lemma[unfolded mem_Collect_eq]) apply(rule,rule,rule *,rule reduced_labelling) |
1055 apply(rule *(1)[OF assms(4)]) apply(rule set_ext) unfolding mem_Collect_eq apply(rule,erule conjE) defer apply(rule) proof-(*(rule,rule)*) |
1055 apply(rule *(1)[OF assms(4)]) apply(rule set_eqI) unfolding mem_Collect_eq apply(rule,erule conjE) defer apply(rule) proof-(*(rule,rule)*) |
1056 fix f assume as:"ksimplex p n f" "reduced lab n ` f = {0..n}" |
1056 fix f assume as:"ksimplex p n f" "reduced lab n ` f = {0..n}" |
1057 have *:"\<forall>x\<in>f. \<forall>j\<in>{1..n + 1}. x j = 0 \<longrightarrow> lab x j = 0" "\<forall>x\<in>f. \<forall>j\<in>{1..n + 1}. x j = p \<longrightarrow> lab x j = 1" |
1057 have *:"\<forall>x\<in>f. \<forall>j\<in>{1..n + 1}. x j = 0 \<longrightarrow> lab x j = 0" "\<forall>x\<in>f. \<forall>j\<in>{1..n + 1}. x j = p \<longrightarrow> lab x j = 1" |
1058 using assms(2-3) using as(1)[unfolded ksimplex_def] by auto |
1058 using assms(2-3) using as(1)[unfolded ksimplex_def] by auto |
1059 have allp:"\<forall>x\<in>f. x (n + 1) = p" using assms(2) using as(1)[unfolded ksimplex_def] by auto |
1059 have allp:"\<forall>x\<in>f. x (n + 1) = p" using assms(2) using as(1)[unfolded ksimplex_def] by auto |
1060 { fix x assume "x\<in>f" hence "reduced lab (n + 1) x < n + 1" apply-apply(rule reduced_labelling_1) |
1060 { fix x assume "x\<in>f" hence "reduced lab (n + 1) x < n + 1" apply-apply(rule reduced_labelling_1) |
1061 defer using assms(3) using as(1)[unfolded ksimplex_def] by auto |
1061 defer using assms(3) using as(1)[unfolded ksimplex_def] by auto |
1062 hence "reduced lab (n + 1) x = reduced lab n x" apply-apply(rule reduced_labelling_Suc) using reduced_labelling(1) by auto } |
1062 hence "reduced lab (n + 1) x = reduced lab n x" apply-apply(rule reduced_labelling_Suc) using reduced_labelling(1) by auto } |
1063 hence "reduced lab (n + 1) ` f = {0..n}" unfolding as(2)[THEN sym] apply- apply(rule set_ext) unfolding image_iff by auto |
1063 hence "reduced lab (n + 1) ` f = {0..n}" unfolding as(2)[THEN sym] apply- apply(rule set_eqI) unfolding image_iff by auto |
1064 moreover guess s using as(1)[unfolded simplex_top_face[OF assms(1) allp,THEN sym]] .. then guess a .. |
1064 moreover guess s using as(1)[unfolded simplex_top_face[OF assms(1) allp,THEN sym]] .. then guess a .. |
1065 ultimately show "\<exists>s a. ksimplex p (n + 1) s \<and> |
1065 ultimately show "\<exists>s a. ksimplex p (n + 1) s \<and> |
1066 a \<in> s \<and> f = s - {a} \<and> reduced lab (n + 1) ` f = {0..n} \<and> ((\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p))" (is ?ex) |
1066 a \<in> s \<and> f = s - {a} \<and> reduced lab (n + 1) ` f = {0..n} \<and> ((\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p))" (is ?ex) |
1067 apply(rule_tac x=s in exI,rule_tac x=a in exI) unfolding complete_face_top[OF *] using allp as(1) by auto |
1067 apply(rule_tac x=s in exI,rule_tac x=a in exI) unfolding complete_face_top[OF *] using allp as(1) by auto |
1068 next fix f assume as:"\<exists>s a. ksimplex p (n + 1) s \<and> |
1068 next fix f assume as:"\<exists>s a. ksimplex p (n + 1) s \<and> |
1070 then guess s .. then guess a apply-apply(erule exE,(erule conjE)+) . note sa=this |
1070 then guess s .. then guess a apply-apply(erule exE,(erule conjE)+) . note sa=this |
1071 { fix x assume "x\<in>f" hence "reduced lab (n + 1) x \<in> reduced lab (n + 1) ` f" by auto |
1071 { fix x assume "x\<in>f" hence "reduced lab (n + 1) x \<in> reduced lab (n + 1) ` f" by auto |
1072 hence "reduced lab (n + 1) x < n + 1" using sa(4) by auto |
1072 hence "reduced lab (n + 1) x < n + 1" using sa(4) by auto |
1073 hence "reduced lab (n + 1) x = reduced lab n x" apply-apply(rule reduced_labelling_Suc) |
1073 hence "reduced lab (n + 1) x = reduced lab n x" apply-apply(rule reduced_labelling_Suc) |
1074 using reduced_labelling(1) by auto } |
1074 using reduced_labelling(1) by auto } |
1075 thus part1:"reduced lab n ` f = {0..n}" unfolding sa(4)[THEN sym] apply-apply(rule set_ext) unfolding image_iff by auto |
1075 thus part1:"reduced lab n ` f = {0..n}" unfolding sa(4)[THEN sym] apply-apply(rule set_eqI) unfolding image_iff by auto |
1076 have *:"\<forall>x\<in>f. x (n + 1) = p" proof(cases "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0") |
1076 have *:"\<forall>x\<in>f. x (n + 1) = p" proof(cases "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0") |
1077 case True then guess j .. hence "\<And>x. x\<in>f \<Longrightarrow> reduced lab (n + 1) x \<noteq> j - 1" apply-apply(rule reduced_labelling_0) apply assumption |
1077 case True then guess j .. hence "\<And>x. x\<in>f \<Longrightarrow> reduced lab (n + 1) x \<noteq> j - 1" apply-apply(rule reduced_labelling_0) apply assumption |
1078 apply(rule assms(2)[rule_format]) using sa(1)[unfolded ksimplex_def] unfolding sa by auto moreover |
1078 apply(rule assms(2)[rule_format]) using sa(1)[unfolded ksimplex_def] unfolding sa by auto moreover |
1079 have "j - 1 \<in> {0..n}" using `j\<in>{1..n+1}` by auto |
1079 have "j - 1 \<in> {0..n}" using `j\<in>{1..n+1}` by auto |
1080 ultimately have False unfolding sa(4)[THEN sym] unfolding image_iff by fastsimp thus ?thesis by auto next |
1080 ultimately have False unfolding sa(4)[THEN sym] unfolding image_iff by fastsimp thus ?thesis by auto next |