# HG changeset patch # User wenzelm # Date 1377378997 -7200 # Node ID 0f4d9df1eaec030e1cfcec676303e74d7db3abe2 # Parent 752e05d09708bf8e7a8dc86fc075861bd5088d5d tuned proofs; diff -r 752e05d09708 -r 0f4d9df1eaec src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Sat Aug 24 21:23:40 2013 +0200 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Sat Aug 24 23:16:37 2013 +0200 @@ -168,7 +168,8 @@ defer apply (erule ex1E) proof - - fix x assume as:"x \ s" "\y. y \ s \ y = x" + fix x + assume as: "x \ s" "\y. y \ s \ y = x" have *: "s = insert x {}" apply (rule set_eqI, rule) unfolding singleton_iff apply (rule as(2)[rule_format]) using as(1) @@ -180,12 +181,17 @@ lemma card_2_exists: "card s = 2 \ (\x\s. \y\s. x \ y \ (\z\s. (z = x) \ (z = y)))" proof assume "card s = 2" - then obtain x y where obt:"s = {x, y}" "x\y" unfolding numeral_2_eq_2 - apply - apply (erule exE conjE | drule card_eq_SucD)+ apply auto done - show "\x\s. \y\s. x \ y \ (\z\s. z = x \ z = y)" using obt by auto + then obtain x y where s: "s = {x, y}" "x\y" unfolding numeral_2_eq_2 + apply - + apply (erule exE conjE | drule card_eq_SucD)+ + apply auto + done + show "\x\s. \y\s. x \ y \ (\z\s. z = x \ z = y)" + using s by auto next assume "\x\s. \y\s. x \ y \ (\z\s. z = x \ z = y)" - then obtain x y where "x\s" "y\s" "x \ y" "\z\s. z = x \ z = y" by auto + then obtain x y where "x\s" "y\s" "x \ y" "\z\s. z = x \ z = y" + by auto then have "s = {x, y}" by auto with `x \ y` show "card s = 2" by auto qed @@ -247,8 +253,9 @@ then obtain a where "a\?M" by auto then have a: "a\s" "f ` (s - {a}) = t - {b}" by auto have "f a \ t - {b}" using a and assms by auto - then have "\c \ s - {a}. f a = f c" unfolding image_iff[symmetric] and a by auto - then obtain c where c:"c \ s" "a \ c" "f a = f c" by auto + then have "\c \ s - {a}. f a = f c" + unfolding image_iff[symmetric] and a by auto + then obtain c where c: "c \ s" "a \ c" "f a = f c" by auto then have *: "f ` (s - {c}) = f ` (s - {a})" apply - apply (rule set_eqI, rule) @@ -261,23 +268,27 @@ apply (rule_tac x = "if y = c then a else y" in bexI) using c a apply auto done qed auto - have "c\?M" unfolding mem_Collect_eq and * using a and c(1) by auto + have "c\?M" + unfolding mem_Collect_eq and * + using a and c(1) by auto show ?thesis apply (rule disjI2, rule image_lemma_0) unfolding card_2_exists - apply (rule bexI[OF _ `a\?M`], rule bexI[OF _ `c\?M`],rule,rule `a\c`) + apply (rule bexI[OF _ `a\?M`], rule bexI[OF _ `c\?M`], rule, rule `a\c`) proof (rule, unfold mem_Collect_eq, erule conjE) fix z assume as: "z \ 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 + unfolding as using as(1) and assms + apply auto done show "z = a \ z = c" proof (rule ccontr) assume "\ ?thesis" then show False using inj[unfolded inj_on_def, THEN bspec[where x=a], THEN bspec[where x=c]] - using `a\s` `c\s` `f a = f c` `a\c` apply auto + using `a\s` `c\s` `f a = f c` `a\c` + apply auto done qed qed @@ -362,9 +373,10 @@ done next case False - obtain a b where a: "a\insert x F" "\x\F. \j. a j \ x j" and - b: "b\insert x F" "\x\F. \j. x j \ b j" using as(3)[OF False] using as(5) by auto - have "\a\insert x F. \x\insert x F. \j. a j \ x j" + obtain a b where a: "a\insert x F" "\x\F. \j. a j \ x j" + and b: "b \ insert x F" "\x\F. \j. x j \ b j" + using as(3)[OF False] using as(5) by auto + have "\a \ insert x F. \x \ insert x F. \j. a j \ x j" using as(5)[rule_format,OF a(1) insertI1] apply - proof (erule disjE) @@ -386,7 +398,8 @@ qed moreover have "\b\insert x F. \x\insert x F. \j. x j \ b j" - using as(5)[rule_format,OF b(1) insertI1] apply- + using as(5)[rule_format,OF b(1) insertI1] + apply - proof (erule disjE) assume "\j. x j \ b j" then show ?thesis @@ -409,7 +422,8 @@ qed auto -lemma kle_imp_pointwise: "kle n x y \ (\j. x j \ y j)" unfolding kle_def by auto +lemma kle_imp_pointwise: "kle n x y \ (\j. x j \ y j)" + unfolding kle_def by auto lemma pointwise_antisym: fixes x :: "nat \ nat" @@ -445,7 +459,7 @@ proof - guess k using assms(1)[unfolded kle_def] .. note k = this show "\k. 1 \ k \ k \ n \ x(k) < y(k)" -proof (cases "k={}") +proof (cases "k = {}") case True then have "x = y" apply - @@ -511,7 +525,7 @@ done then guess a .. note a = this show ?thesis - apply (rule_tac x=a in bexI) + apply (rule_tac x = a in bexI) proof fix x assume "x \ s" @@ -706,7 +720,8 @@ fix j show "x j \ b j + 1" apply (rule *) - using kle_trans_1[OF assms(1),of j] kle_trans_1[OF assms(3), of j] apply auto + using kle_trans_1[OF assms(1),of j] kle_trans_1[OF assms(3), of j] + apply auto done qed @@ -720,7 +735,8 @@ fix j show "b j \ x j + 1" apply (rule *) - using kle_trans_1[OF assms(2),of j] kle_trans_1[OF assms(4), of j] apply auto + using kle_trans_1[OF assms(2),of j] kle_trans_1[OF assms(4), of j] + apply auto done qed @@ -730,12 +746,17 @@ proof (cases "x k = a k") case True show ?thesis - apply (rule disjI1, rule ext) + apply (rule disjI1) + apply (rule ext) proof - fix j have "x j \ 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 by auto + unfolding assms(1)[rule_format] + apply - + apply(cases "j = k") + using True + apply auto + done thus "x j = a j" using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]] by auto qed next @@ -755,10 +776,10 @@ subsection {* kuhn's notion of a simplex (a reformulation to avoid so much indexing). *} definition "ksimplex p n (s::(nat \ nat) set) \ - (card s = n + 1 \ - (\x\s. \j. x(j) \ p) \ - (\x\s. \j. j\{1..n} \ (x j = p)) \ - (\x\s. \y\s. kle n x y \ kle n y x))" + (card s = n + 1 \ + (\x\s. \j. x(j) \ p) \ + (\x\s. \j. j\{1..n} \ (x j = p)) \ + (\x\s. \y\s. kle n x y \ kle n y x))" lemma ksimplexI: "card s = n + 1 \ @@ -1081,7 +1102,7 @@ thus ?thesis unfolding kk using kkk and False by auto qed - qed(insert k(1) `b\s`, auto) + qed (insert k(1) `b\s`, auto) qed @@ -1118,7 +1139,7 @@ prefer 3 apply rule defer - apply (erule bexE,rule) + apply (erule bexE, rule) unfolding mem_Collect_eq apply (erule splitE)+ apply (erule conjE)+ @@ -1178,7 +1199,7 @@ case False hence "t = {}" using `finite t` by auto show ?thesis proof (cases "s = {}") - have *:"{f. \x. f x = d} = {\x. d}" by auto + have *: "{f. \x. f x = d} = {\x. d}" by auto case True thus ?thesis using `t = {}` by (auto simp: *) next @@ -1442,422 +1463,1312 @@ lemma ksimplex_replace_1: assumes "ksimplex p n s" "a \ s" "n \ 0" "j\{1..n}" "\x\s - {a}. x j = p" - shows "card {s'. ksimplex p n s' \ (\b\s'. s' - {b} = s - {a})} = 1" proof- - have lem:"\a a' s'. s' - {a'} = s - {a} \ a' = a \ a' \ s' \ a \ s \ s' = s" by auto - have lem:"\s' a'. ksimplex p n s' \ a'\s' \ s' - {a'} = s - {a} \ s' = s" proof- case goal1 - guess a0 a1 apply(rule ksimplex_extrema_strong[OF assms(1,3)]) . note exta = this[rule_format] - have a:"a = a0" apply(rule ksimplex_fix_plane_p[OF assms(1-2,4-5) exta(1,2)]) unfolding exta by auto moreover - guess b0 b1 apply(rule ksimplex_extrema_strong[OF goal1(1) assms(3)]) . note extb = this[rule_format] - have a':"a' = b0" apply(rule ksimplex_fix_plane_p[OF goal1(1-2) assms(4), of _ b1]) unfolding goal1 extb using extb(1,2) assms(5) by auto - 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" apply(rule ext) proof- case goal1 show "a0 x = b0 x" - using *[THEN cong, of x x] unfolding exta extb apply-apply(cases "x\{1..n}") by auto qed - ultimately show "s' = s" apply-apply(rule lem[OF goal1(3) _ goal1(2) assms(2)]) by auto qed - show ?thesis unfolding card_1_exists apply(rule ex1I[of _ s]) unfolding mem_Collect_eq apply(rule,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) by auto qed + shows "card {s'. ksimplex p n s' \ (\b\s'. s' - {b} = s - {a})} = 1" +proof - + have lem: "\a a' s'. s' - {a'} = s - {a} \ a' = a \ a' \ s' \ a \ s \ s' = s" + by auto + have lem: "\s' a'. ksimplex p n s' \ a'\s' \ s' - {a'} = s - {a} \ s' = s" + proof - + case goal1 + guess a0 a1 by (rule ksimplex_extrema_strong[OF assms(1,3)]) note exta = this [rule_format] + 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 + guess b0 b1 by (rule ksimplex_extrema_strong[OF goal1(1) assms(3)]) + note extb = this [rule_format] + 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" + apply (rule ext) + proof - + case goal1 + show "a0 x = b0 x" + using *[THEN cong, of x x] + unfolding exta extb + apply - + apply (cases "x \ {1..n}") + apply auto + done + 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, 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" "a \ s" "n \ 0" "~(\j\{1..n}. \x\s - {a}. x j = 0)" "~(\j\{1..n}. \x\s - {a}. x j = p)" - shows "card {s'. ksimplex p n s' \ (\b\s'. s' - {b} = s - {a})} = 2" (is "card ?A = 2") proof- - have lem1:"\a a' s s'. s' - {a'} = s - {a} \ a' = a \ a' \ s' \ a \ s \ s' = s" by auto - have lem2:"\a b. a\s \ b\a \ s \ insert b (s - {a})" proof case goal1 - hence "a\insert b (s - {a})" by auto hence "a\ s - {a}" unfolding insert_iff using goal1 by auto - thus False by auto qed - guess a0 a1 apply(rule ksimplex_extrema_strong[OF assms(1,3)]) . note a0a1=this - { assume "a=a0" - have *:"\P Q. (P \ Q) \ \ P \ Q" by auto - have "\x\s. \ 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) + assumes "ksimplex p n s" "a \ s" + "n \ 0" + "~(\j\{1..n}. \x\s - {a}. x j = 0)" + "~(\j\{1..n}. \x\s - {a}. x j = p)" + shows "card {s'. ksimplex p n s' \ (\b\s'. s' - {b} = s - {a})} = 2" + (is "card ?A = 2") +proof - + have lem1: "\a a' s s'. s' - {a'} = s - {a} \ a' = a \ a' \ s' \ a \ s \ s' = s" + by auto + have lem2: "\a b. a\s \ b\a \ s \ insert b (s - {a})" + proof + case goal1 + hence "a \ insert b (s - {a})" by auto + hence "a \ s - {a}" unfolding insert_iff using goal1 by auto + thus False by auto + qed + guess a0 a1 by (rule ksimplex_extrema_strong[OF assms(1,3)]) note a0a1 = this + { + assume "a = a0" + have *: "\P Q. (P \ Q) \ \ P \ Q" by auto + have "\x\s. \ 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) hence "\y\s. \k\{1..n}. \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`]]) by auto - then guess a2 .. from this(2) guess k .. note k=this note a2=`a2\s` + apply (rule_tac *[OF ksimplex_successor[OF assms(1-2),unfolded `a=a0`]]) + apply auto + done + then guess a2 .. + from this(2) guess k .. note k = this note a2 =`a2 \ s` def a3 \ "\j. if j = k then a1 j + 1 else a1 j" - have "a3 \ s" proof assume "a3\s" hence "kle n a3 a1" using a0a1(4) by auto - thus False apply(drule_tac kle_imp_pointwise) unfolding a3_def - apply(erule_tac x=k in allE) by auto qed + have "a3 \ s" + proof + assume "a3\s" + hence "kle n a3 a1" + using a0a1(4) by auto + thus False + apply (drule_tac kle_imp_pointwise) unfolding a3_def + apply (erule_tac x = k in allE) + apply auto + done + qed hence "a3 \ a0" "a3 \ a1" using a0a1 by auto have "a2 \ a0" using k(2)[THEN spec[where x=k]] by auto - have lem3:"\x. x\(s - {a0}) \ kle n a2 x" proof(rule ccontr) case goal1 hence as:"x\s" "x\a0" by auto - have "kle n a2 x \ kle n x a2" using ksimplexD(6)[OF assms(1)] and as `a2\s` by auto moreover + have lem3: "\x. x\(s - {a0}) \ kle n a2 x" + proof (rule ccontr) + case goal1 + hence as: "x\s" "x\a0" by auto + have "kle n a2 x \ kle n x a2" + using ksimplexD(6)[OF assms(1)] and as `a2\s` by auto + moreover have "kle n a0 x" using a0a1(4) as by auto - ultimately have "x = a0 \ x = a2" apply-apply(rule kle_adjacent[OF k(2)]) using goal1(2) by auto - hence "x = a2" using as by auto thus False using goal1(2) using kle_refl by auto qed - let ?s = "insert a3 (s - {a0})" 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\a0` `a3\s` `a0\s` by(auto simp add:card_insert_if) - fix x assume x:"x \ insert a3 (s - {a0})" - show "\j. x j \ p" proof(rule,cases "x = a3") - fix j case False thus "x j\p" using x ksimplexD(4)[OF assms(1)] by auto next - fix j case True show "x j\p" unfolding True proof(cases "j=k") - case False thus "a3 j \p" unfolding True a3_def using `a1\s` ksimplexD(4)[OF assms(1)] by auto next - guess a4 using assms(5)[unfolded bex_simps ball_simps,rule_format,OF k(1)] .. note a4=this - have "a2 k \ a4 k" using lem3[OF a4(1)[unfolded `a=a0`],THEN kle_imp_pointwise] by auto - also have "\ < 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 thus "a3 j \p" unfolding a3_def unfolding a0a1(5)[rule_format] - using k(1) k(2)assms(5) using * by simp qed qed - show "\j. j \ {1..n} \ x j = p" proof(rule,rule,cases "x=a3") fix j::nat assume j:"j\{1..n}" - { case False thus "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto } - case True show "x j = p" unfolding True a3_def using j k(1) - using ksimplexD(5)[OF assms(1),rule_format,OF `a1\s` j] by auto qed - fix y assume y:"y\insert a3 (s - {a0})" - have lem4:"\x. x\s \ x\a0 \ kle n x a3" proof- case goal1 - guess kk using a0a1(4)[rule_format,OF `x\s`,THEN conjunct2,unfolded kle_def] - apply-apply(erule exE,erule conjE) . note kk=this - have "k\kk" proof assume "k\kk" + ultimately have "x = a0 \ x = a2" + apply - + apply (rule kle_adjacent[OF k(2)]) + using goal1(2) + apply auto + done + hence "x = a2" using as by auto + thus False using goal1(2) using kle_refl by auto + qed + let ?s = "insert a3 (s - {a0})" + 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\a0` `a3\s` `a0\s` + by (auto simp add:card_insert_if) + fix x + assume x: "x \ insert a3 (s - {a0})" + show "\j. x j \ p" + proof (rule, cases "x = a3") + fix j + case False + thus "x j\p" using x ksimplexD(4)[OF assms(1)] by auto + next + fix j + case True + show "x j\p" unfolding True + proof (cases "j = k") + case False + thus "a3 j \p" unfolding True a3_def + using `a1\s` ksimplexD(4)[OF assms(1)] by auto + next + guess a4 using assms(5)[unfolded bex_simps ball_simps,rule_format,OF k(1)] .. + note a4 = this + have "a2 k \ a4 k" + using lem3[OF a4(1)[unfolded `a=a0`],THEN kle_imp_pointwise] by auto + also have "\ < 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 + thus "a3 j \p" unfolding a3_def unfolding a0a1(5)[rule_format] + using k(1) k(2)assms(5) using * by simp + qed + qed + show "\j. j \ {1..n} \ x j = p" + proof (rule, rule, cases "x=a3") + fix j :: nat + assume j: "j \ {1..n}" + { + case False + thus "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto + } + case True + show "x j = p" + unfolding True a3_def + using j k(1) + using ksimplexD(5)[OF assms(1),rule_format,OF `a1\s` j] by auto + qed + fix y + assume y: "y \ insert a3 (s - {a0})" + have lem4: "\x. x\s \ x\a0 \ kle n x a3" + proof - + case goal1 + guess kk using a0a1(4)[rule_format, OF `x\s`,THEN conjunct2,unfolded kle_def] + by (elim exE conjE) + note kk = this + have "k \ kk" + proof + assume "k \ kk" hence "a1 k = x k + 1" using kk by auto hence "a0 k = x k" unfolding a0a1(5)[rule_format] using k(1) by auto - hence "a2 k = x k + 1" unfolding k(2)[rule_format] by auto moreover + hence "a2 k = x k + 1" unfolding k(2)[rule_format] by auto + moreover have "a2 k \ x k" using lem3[of x,THEN kle_imp_pointwise] goal1 by auto - ultimately show False by auto qed - thus ?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) by auto qed - show "kle n x y \ 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 by auto next - case False show ?thesis proof(cases "x=a3") case True show ?thesis unfolding True - apply(rule disjI2,rule lem4) using y False by auto next - case False thus ?thesis apply(rule_tac ksimplexD(6)[OF assms(1),rule_format]) - using x y `y\a3` by auto qed qed qed - hence "insert a3 (s - {a0}) \ ?A" unfolding mem_Collect_eq apply-apply(rule,assumption) - apply(rule_tac x="a3" in bexI) unfolding `a=a0` using `a3\s` by auto moreover - have "s \ ?A" using assms(1,2) by auto ultimately have "?A \ {s, insert a3 (s - {a0})}" by auto - moreover have "?A \ {s, insert a3 (s - {a0})}" apply(rule) unfolding mem_Collect_eq proof(erule conjE) - fix s' assume as:"ksimplex p n s'" and "\b\s'. s' - {b} = s - {a}" - from this(2) guess a' .. note a'=this - guess a_min a_max apply(rule ksimplex_extrema_strong[OF as assms(3)]) . note min_max=this - have *:"\x\s' - {a'}. x k = a2 k" unfolding a' proof fix x assume x:"x\s-{a}" - hence "kle n a2 x" apply-apply(rule lem3) using `a=a0` by auto - hence "a2 k \ x k" apply(drule_tac kle_imp_pointwise) by auto moreover - have "x k \ 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 \ a'=a_max" apply(rule ksimplex_fix_plane[OF a'(1) k(1) *]) using min_max by auto - show "s' \ {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]) + ultimately show False by auto + qed + thus ?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 \ 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, rule lem4) + using y False + apply auto + done + next + case False + thus ?thesis + apply (rule_tac ksimplexD(6)[OF assms(1),rule_format]) + using x y `y \ a3` + apply auto + done + qed + qed + qed + hence "insert a3 (s - {a0}) \ ?A" + unfolding mem_Collect_eq + apply - + apply (rule, assumption) + apply (rule_tac x = "a3" in bexI) + unfolding `a = a0` + using `a3 \ s` + apply auto + done + moreover + have "s \ ?A" using assms(1,2) by auto + ultimately have "?A \ {s, insert a3 (s - {a0})}" by auto + moreover + have "?A \ {s, insert a3 (s - {a0})}" + apply rule + unfolding mem_Collect_eq + proof (erule conjE) + fix s' + assume as: "ksimplex p n s'" and "\b\s'. s' - {b} = s - {a}" + from this(2) guess a' .. note a' = this + guess a_min a_max by (rule ksimplex_extrema_strong[OF as assms(3)]) note min_max = this + have *: "\x\s' - {a'}. x k = a2 k" + unfolding a' + proof + fix x + assume x: "x \ s - {a}" + hence "kle n a2 x" + apply - + apply (rule lem3) + using `a = a0` + apply auto + done + hence "a2 k \ x k" + apply (drule_tac kle_imp_pointwise) + apply auto + done + moreover + have "x k \ 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 \ a' = a_max" + apply (rule ksimplex_fix_plane[OF a'(1) k(1) *]) + using min_max + apply auto + done + show "s' \ {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\s'" using a' unfolding `a=a0` using a0a1 by auto - show "a_max \ s" proof(rule ccontr) assume "a_max\s" + show "a_max \ s" + proof (rule ccontr) + assume "a_max \ s" hence "a_max = a'" using a' min_max by auto - thus False unfolding True using min_max by auto qed qed + thus False unfolding True using min_max by auto + qed + qed hence "\i. a_max i = a1 i" by auto - hence "a' = a" unfolding True `a=a0` apply-apply(subst fun_eq_iff,rule) - apply(erule_tac x=x in allE) unfolding a0a1(5)[rule_format] min_max(5)[rule_format] - proof- case goal1 thus ?case apply(cases "x\{1..n}") by auto qed - hence "s' = s" apply-apply(rule lem1[OF a'(2)]) using `a\s` `a'\s'` by auto - thus ?thesis by auto next - case False hence 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 \ s - {a0}" unfolding a'(2)[symmetric,unfolded `a=a0`] + hence "a' = a" unfolding True `a = a0` + apply - + apply (subst fun_eq_iff, rule) + apply (erule_tac x=x in allE) + unfolding a0a1(5)[rule_format] min_max(5)[rule_format] + proof - + case goal1 + thus ?case by (cases "x\{1..n}") auto + qed + hence "s' = s" + apply - + apply (rule lem1[OF a'(2)]) + using `a\s` `a'\s'` + apply auto + done + thus ?thesis by auto + next + case False + hence 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 \ s - {a0}" + unfolding a'(2)[symmetric,unfolded `a = a0`] unfolding as using min_max(1-3) by auto - have "a2 \ a" unfolding `a=a0` using k(2)[rule_format,of k] by auto - hence "a2 \ s - {a}" using a2 by auto thus "a2 \ s'" unfolding a'(2)[symmetric] by auto qed + have "a2 \ a" + unfolding `a = a0` using k(2)[rule_format,of k] by auto + hence "a2 \ s - {a}" + using a2 by auto + thus "a2 \ s'" unfolding a'(2)[symmetric] by auto + qed hence "\i. a_min i = a2 i" by auto - hence "a' = a3" unfolding as `a=a0` apply-apply(subst fun_eq_iff,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\{1..n}") defer apply(cases "x=k") - using `k\{1..n}` by auto qed - hence "s' = insert a3 (s - {a0})" apply-apply(rule lem1) defer apply assumption - apply(rule a'(1)) unfolding a' `a=a0` using `a3\s` by auto - thus ?thesis by auto qed qed - ultimately have *:"?A = {s, insert a3 (s - {a0})}" by blast + hence "a' = a3" + unfolding as `a = a0` + apply - + apply (subst fun_eq_iff, 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\{1..n}") + defer + apply (cases "x = k") + using `k\{1..n}` + apply auto + done + qed + hence "s' = insert a3 (s - {a0})" + apply - + apply (rule lem1) + defer + apply assumption + apply (rule a'(1)) + unfolding a' `a = a0` + using `a3 \ s` + apply auto + done + thus ?thesis by auto + qed + qed + ultimately have *: "?A = {s, insert a3 (s - {a0})}" by blast have "s \ insert a3 (s - {a0})" using `a3\s` by auto - hence ?thesis unfolding * by auto } moreover - { assume "a=a1" - have *:"\P Q. (P \ Q) \ \ P \ Q" by auto - have "\x\s. \ 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) + hence ?thesis unfolding * by auto + } + moreover + { + assume "a = a1" + have *: "\P Q. (P \ Q) \ \ P \ Q" by auto + have "\x\s. \ 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) hence "\y\s. \k\{1..n}. \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`]]) by auto - then guess a2 .. from this(2) guess k .. note k=this note a2=`a2\s` + apply (rule_tac *[OF ksimplex_predecessor[OF assms(1-2),unfolded `a=a1`]]) + apply auto + done + then guess a2 .. from this(2) guess k .. note k=this note a2 = `a2 \ s` def a3 \ "\j. if j = k then a0 j - 1 else a0 j" have "a2 \ a1" using k(2)[THEN spec[where x=k]] by auto - have lem3:"\x. x\(s - {a1}) \ kle n x a2" proof(rule ccontr) case goal1 hence as:"x\s" "x\a1" by auto - have "kle n a2 x \ kle n x a2" using ksimplexD(6)[OF assms(1)] and as `a2\s` by auto moreover + have lem3: "\x. x\(s - {a1}) \ kle n x a2" + proof (rule ccontr) + case goal1 + hence as: "x\s" "x\a1" by auto + have "kle n a2 x \ kle n x a2" + using ksimplexD(6)[OF assms(1)] and as `a2\s` by auto + moreover have "kle n x a1" using a0a1(4) as by auto - ultimately have "x = a2 \ x = a1" apply-apply(rule kle_adjacent[OF k(2)]) using goal1(2) by auto - hence "x = a2" using as by auto thus False using goal1(2) using kle_refl by auto qed - have "a0 k \ 0" proof- - guess a4 using assms(4)[unfolded bex_simps ball_simps,rule_format,OF `k\{1..n}`] .. note a4=this - have "a4 k \ 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 + ultimately have "x = a2 \ x = a1" + apply - + apply (rule kle_adjacent[OF k(2)]) + using goal1(2) + apply auto + done + hence "x = a2" using as by auto + thus False using goal1(2) using kle_refl by auto + qed + have "a0 k \ 0" + proof - + guess a4 using assms(4)[unfolded bex_simps ball_simps,rule_format,OF `k\{1..n}`] .. + note a4 = this + have "a4 k \ 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 hence "a1 k > 1" unfolding k(2)[rule_format] by simp - thus ?thesis unfolding a0a1(5)[rule_format] using k(1) by simp qed - hence lem4:"\j. a0 j = (if j=k then a3 j + 1 else a3 j)" unfolding a3_def by simp - have "\ kle n a0 a3" apply(rule ccontr) unfolding not_not apply(drule kle_imp_pointwise) - unfolding lem4[rule_format] apply(erule_tac x=k in allE) by auto + thus ?thesis unfolding a0a1(5)[rule_format] using k(1) by simp + qed + hence lem4: "\j. a0 j = (if j=k then a3 j + 1 else a3 j)" + unfolding a3_def by simp + have "\ kle n a0 a3" + apply (rule ccontr) + unfolding not_not + apply (drule kle_imp_pointwise) + unfolding lem4[rule_format] + apply (erule_tac x=k in allE) + apply auto + done hence "a3 \ s" using a0a1(4) by auto hence "a3 \ a1" "a3 \ 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\a0` `a3\s` `a1\s` by(auto simp add:card_insert_if) - fix x assume x:"x \ insert a3 (s - {a1})" + 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\a0` `a3\s` `a1\s` + by(auto simp add:card_insert_if) + fix x + assume x: "x \ insert a3 (s - {a1})" show "\j. x j \ p" proof(rule,cases "x = a3") - fix j case False thus "x j\p" using x ksimplexD(4)[OF assms(1)] by auto next - fix j case True show "x j\p" unfolding True proof(cases "j=k") - case False thus "a3 j \p" unfolding True a3_def using `a0\s` ksimplexD(4)[OF assms(1)] by auto next - guess a4 using assms(5)[unfolded bex_simps ball_simps,rule_format,OF k(1)] .. note a4=this - case True have "a3 k \ a0 k" unfolding lem4[rule_format] by auto - also have "\ \ p" using ksimplexD(4)[OF assms(1),rule_format,of a0 k] a0a1 by auto - finally show "a3 j \ p" unfolding True by auto qed qed - show "\j. j \ {1..n} \ x j = p" proof(rule,rule,cases "x=a3") fix j::nat assume j:"j\{1..n}" - { case False thus "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto } - case True show "x j = p" unfolding True a3_def using j k(1) - using ksimplexD(5)[OF assms(1),rule_format,OF `a0\s` j] by auto qed - fix y assume y:"y\insert a3 (s - {a1})" - have lem4:"\x. x\s \ x\a1 \ kle n a3 x" proof- case goal1 hence *:"x\s - {a1}" by auto - have "kle n a3 a2" proof- have "kle n a0 a1" using a0a1 by auto then guess kk unfolding kle_def .. - thus ?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 thus ?case apply-apply(erule conjE) - apply(erule_tac[!] x=j in allE) apply(cases "j\kk") apply(case_tac[!] "j=k") by auto 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) by auto - ultimately show ?case apply-apply(rule kle_between_l[of _ a0 _ a2]) using lem3[OF *] - using a0a1(4)[rule_format,OF goal1(1)] by auto qed - show "kle n x y \ kle n y x" proof(cases "y=a3") - case True show ?thesis unfolding True apply(cases "x=a3") defer apply(rule disjI2,rule lem4) - using x by auto next - case False show ?thesis proof(cases "x=a3") case True show ?thesis unfolding True - apply(rule disjI1,rule lem4) using y False by auto next - case False thus ?thesis apply(rule_tac ksimplexD(6)[OF assms(1),rule_format]) - using x y `y\a3` by auto qed qed qed - hence "insert a3 (s - {a1}) \ ?A" unfolding mem_Collect_eq apply-apply(rule,assumption) - apply(rule_tac x="a3" in bexI) unfolding `a=a1` using `a3\s` by auto moreover - have "s \ ?A" using assms(1,2) by auto ultimately have "?A \ {s, insert a3 (s - {a1})}" by auto - moreover have "?A \ {s, insert a3 (s - {a1})}" apply(rule) unfolding mem_Collect_eq proof(erule conjE) - fix s' assume as:"ksimplex p n s'" and "\b\s'. s' - {b} = s - {a}" - from this(2) guess a' .. note a'=this - guess a_min a_max apply(rule ksimplex_extrema_strong[OF as assms(3)]) . note min_max=this - have *:"\x\s' - {a'}. x k = a2 k" unfolding a' proof fix x assume x:"x\s-{a}" - hence "kle n x a2" apply-apply(rule lem3) using `a=a1` by auto - hence "x k \ a2 k" apply(drule_tac kle_imp_pointwise) by auto moreover - { have "a2 k \ a0 k" using k(2)[rule_format,of k] unfolding a0a1(5)[rule_format] using k(1) by simp - also have "\ \ x k" using a0a1(4)[rule_format,of x,THEN conjunct1,THEN kle_imp_pointwise] x by auto - finally have "a2 k \ x k" . } ultimately show "x k = a2 k" by auto qed - have **:"a'=a_min \ a'=a_max" apply(rule ksimplex_fix_plane[OF a'(1) k(1) *]) using min_max by auto - have "a2 \ a1" proof assume as:"a2 = a1" - show False using k(2) unfolding as apply(erule_tac x=k in allE) by auto qed - hence a2':"a2 \ s' - {a'}" unfolding a' using a2 unfolding `a=a1` by auto - show "s' \ {s, insert a3 (s - {a1})}" proof(cases "a'=a_min") - case True have "a_max \ s - {a1}" using min_max unfolding a'(2)[unfolded `a=a1`,symmetric] True by auto - hence "a_max = a2" unfolding kle_antisym[symmetric,of a_max a2 n] apply-apply(rule) - apply(rule lem3,assumption) apply(rule min_max(4)[rule_format,THEN conjunct2]) using a2' by auto + fix j + case False + thus "x j\p" using x ksimplexD(4)[OF assms(1)] by auto + next + fix j + case True + show "x j\p" unfolding True + proof (cases "j = k") + case False + thus "a3 j \p" + unfolding True a3_def + using `a0\s` ksimplexD(4)[OF assms(1)] + by auto + next + guess a4 using assms(5)[unfolded bex_simps ball_simps,rule_format,OF k(1)] .. + note a4 = this + case True have "a3 k \ a0 k" + unfolding lem4[rule_format] by auto + also have "\ \ p" + using ksimplexD(4)[OF assms(1),rule_format,of a0 k] a0a1 by auto + finally show "a3 j \ p" + unfolding True by auto + qed + qed + show "\j. j \ {1..n} \ x j = p" + proof (rule, rule, cases "x = a3") + fix j :: nat + assume j: "j \ {1..n}" + { + case False + thus "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto + next + case True + show "x j = p" unfolding True a3_def using j k(1) + using ksimplexD(5)[OF assms(1),rule_format,OF `a0\s` j] by auto + } + qed + fix y + assume y: "y\insert a3 (s - {a1})" + have lem4: "\x. x\s \ x \ a1 \ kle n a3 x" + proof - + case goal1 + hence *: "x\s - {a1}" by auto + have "kle n a3 a2" + proof - + have "kle n a0 a1" + using a0a1 by auto then guess kk unfolding kle_def .. + thus ?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 + thus ?case + apply - + apply (erule conjE) + apply (erule_tac[!] x=j in allE) + apply (cases "j \ 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 \ kle n y x" + proof (cases "y = a3") + case True + show ?thesis + unfolding True + apply (cases "x = a3") + defer + apply (rule disjI2, 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, rule lem4) + using y False + apply auto + done + next + case False + thus ?thesis + apply (rule_tac ksimplexD(6)[OF assms(1),rule_format]) + using x y `y\a3` + apply auto + done + qed + qed + qed + hence "insert a3 (s - {a1}) \ ?A" + unfolding mem_Collect_eq + apply - + apply (rule, assumption) + apply (rule_tac x = "a3" in bexI) + unfolding `a = a1` + using `a3 \ s` + apply auto + done + moreover + have "s \ ?A" using assms(1,2) by auto + ultimately have "?A \ {s, insert a3 (s - {a1})}" by auto + moreover have "?A \ {s, insert a3 (s - {a1})}" + apply rule + unfolding mem_Collect_eq + proof (erule conjE) + fix s' + assume as: "ksimplex p n s'" and "\b\s'. s' - {b} = s - {a}" + from this(2) guess a' .. note a' = this + guess a_min a_max by (rule ksimplex_extrema_strong[OF as assms(3)]) note min_max = this + have *: "\x\s' - {a'}. x k = a2 k" unfolding a' + proof + fix x + assume x: "x \ s - {a}" + hence "kle n x a2" + apply - + apply (rule lem3) + using `a = a1` + apply auto + done + hence "x k \ a2 k" + apply (drule_tac kle_imp_pointwise) + apply auto + done + moreover + { + have "a2 k \ a0 k" + using k(2)[rule_format,of k] + unfolding a0a1(5)[rule_format] + using k(1) + by simp + also have "\ \ x k" + using a0a1(4)[rule_format,of x,THEN conjunct1,THEN kle_imp_pointwise] x + by auto + finally have "a2 k \ x k" . + } + ultimately show "x k = a2 k" by auto + qed + have **: "a' = a_min \ a' = a_max" + apply (rule ksimplex_fix_plane[OF a'(1) k(1) *]) + using min_max + apply auto + done + have "a2 \ a1" + proof + assume as: "a2 = a1" + show False + using k(2) + unfolding as + apply (erule_tac x = k in allE) + apply auto + done + qed + hence a2': "a2 \ s' - {a'}" + unfolding a' + using a2 + unfolding `a = a1` + by auto + show "s' \ {s, insert a3 (s - {a1})}" + proof (cases "a' = a_min") + case True + have "a_max \ s - {a1}" + using min_max + unfolding a'(2)[unfolded `a=a1`,symmetric] True + by auto + hence "a_max = a2" + unfolding kle_antisym[symmetric,of a_max a2 n] + apply - + apply rule + apply (rule lem3,assumption) + apply (rule min_max(4)[rule_format,THEN conjunct2]) + using a2' + apply auto + done hence a_max:"\i. a_max i = a2 i" by auto - have *:"\j. a2 j = (if j\{1..n} then a3 j + 1 else a3 j)" - using k(2) unfolding lem4[rule_format] a0a1(5)[rule_format] apply-apply(rule,erule_tac x=j in allE) - proof- case goal1 thus ?case apply(cases "j\{1..n}",case_tac[!] "j=k") by auto qed - have "\i. a_min i = a3 i" using a_max apply-apply(rule,erule_tac x=i in allE) - unfolding min_max(5)[rule_format] *[rule_format] proof- case goal1 - thus ?case apply(cases "i\{1..n}") by auto qed hence "a_min = a3" unfolding fun_eq_iff . - hence "s' = insert a3 (s - {a1})" using a' unfolding `a=a1` True by auto thus ?thesis by auto next + have *: "\j. a2 j = (if j\{1..n} then a3 j + 1 else a3 j)" + using k(2) + unfolding lem4[rule_format] a0a1(5)[rule_format] + apply - + apply (rule,erule_tac x=j in allE) + proof - + case goal1 + thus ?case by (cases "j\{1..n}",case_tac[!] "j=k") auto + qed + have "\i. a_min i = a3 i" + using a_max + apply - + apply (rule,erule_tac x=i in allE) + unfolding min_max(5)[rule_format] *[rule_format] + proof - + case goal1 + thus ?case by (cases "i\{1..n}") auto + qed + hence "a_min = a3" unfolding fun_eq_iff . + hence "s' = insert a3 (s - {a1})" + using a' unfolding `a = a1` True by auto + thus ?thesis by auto + next case False hence 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 \ s - {a1}" using min_max(1,3) unfolding a'(2)[symmetric,unfolded `a=a1`] as by auto - thus "a_min \ s" by auto have "a0 \ s - {a1}" using a0a1(1-3) by auto thus "a0 \ s'" - unfolding a'(2)[symmetric,unfolded `a=a1`] by auto qed - hence "\i. a_max i = a1 i" unfolding a0a1(5)[rule_format] min_max(5)[rule_format] by auto - hence "s' = s" apply-apply(rule lem1[OF a'(2)]) using `a\s` `a'\s'` unfolding as `a=a1` unfolding fun_eq_iff by auto - thus ?thesis by auto qed qed - ultimately have *:"?A = {s, insert a3 (s - {a1})}" by blast + 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 \ s - {a1}" + using min_max(1,3) + unfolding a'(2)[symmetric,unfolded `a=a1`] as + by auto + thus "a_min \ s" by auto + have "a0 \ s - {a1}" using a0a1(1-3) by auto + thus "a0 \ s'" unfolding a'(2)[symmetric,unfolded `a=a1`] by auto + qed + hence "\i. a_max i = a1 i" + unfolding a0a1(5)[rule_format] min_max(5)[rule_format] by auto + hence "s' = s" + apply - + apply (rule lem1[OF a'(2)]) + using `a \ s` `a' \ s'` + unfolding as `a = a1` + unfolding fun_eq_iff + apply auto + done + thus ?thesis by auto + qed + qed + ultimately have *: "?A = {s, insert a3 (s - {a1})}" by blast have "s \ insert a3 (s - {a1})" using `a3\s` by auto - hence ?thesis unfolding * by auto } moreover - { assume as:"a\a0" "a\a1" have "\ (\x\s. kle n a x)" proof case goal1 - have "a=a0" unfolding kle_antisym[symmetric,of _ _ n] apply(rule) - using goal1 a0a1 assms(2) by auto thus False using as by auto qed - hence "\y\s. \k\{1..n}. \j. a j = (if j = k then y j + 1 else y j)" using ksimplex_predecessor[OF assms(1-2)] by blast - then guess u .. from this(2) guess k .. note k = this[rule_format] note u = `u\s` - have "\ (\x\s. kle n x a)" proof case goal1 - have "a=a1" unfolding kle_antisym[symmetric,of _ _ n] apply(rule) - using goal1 a0a1 assms(2) by auto thus False using as by auto qed - hence "\y\s. \k\{1..n}. \j. y j = (if j = k then a j + 1 else a j)" using ksimplex_successor[OF assms(1-2)] by blast - then guess v .. from this(2) guess l .. note l = this[rule_format] note v = `v\s` + hence ?thesis unfolding * by auto + } + moreover + { + assume as: "a \ a0" "a \ a1" have "\ (\x\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 + thus False using as by auto + qed + hence "\y\s. \k\{1..n}. \j. a j = (if j = k then y j + 1 else y j)" + using ksimplex_predecessor[OF assms(1-2)] by blast + then guess u .. from this(2) guess k .. note k = this[rule_format] + note u = `u \ s` + have "\ (\x\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 + thus False using as by auto + qed + hence "\y\s. \k\{1..n}. \j. y j = (if j = k then a j + 1 else a j)" + using ksimplex_successor[OF assms(1-2)] by blast + then guess v .. from this(2) guess l .. + note l = this[rule_format] + note v = `v\s` def a' \ "\j. if j = l then u j + 1 else u j" - have kl:"k \ l" proof assume "k=l" have *:"\P. (if P then (1::nat) else 0) \ 2" by auto + have kl: "k \ l" + proof + assume "k = l" + have *: "\P. (if P then (1::nat) else 0) \ 2" by auto thus 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)+ by(auto simp add: *) qed - hence aa':"a'\a" apply-apply rule unfolding fun_eq_iff unfolding a'_def k(2) - apply(erule_tac x=l in allE) by auto - have "a' \ s" apply(rule) apply(drule ksimplexD(6)[OF assms(1),rule_format,OF `a\s`]) proof(cases "kle n a a'") - case goal2 hence "kle n a' a" by auto thus False apply(drule_tac kle_imp_pointwise) - apply(erule_tac x=l in allE) unfolding a'_def k(2) using kl by auto next - case True thus False apply(drule_tac kle_imp_pointwise) - apply(erule_tac x=k in allE) unfolding a'_def k(2) using kl by auto 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) by auto - have uxv:"\x. kle n u x \ kle n x v \ (x = u) \ (x = a) \ (x = a') \ (x = v)" - proof- case goal1 thus ?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 - thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next - assume as:"x l \ 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) apply- - using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1 - thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next - assume as:"x l = u l" "x k \ u k" - have "x = a" unfolding fun_eq_iff - using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply- - using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1 - thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next - assume as:"x l \ u l" "x k \ u k" - have "x = v" unfolding fun_eq_iff - using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply- - using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1 - thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as `k\l` by auto qed thus ?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 by auto - have lem3:"\x. x\s \ kle n v x \ 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\s` by auto - have lem4:"\x. x\s \ kle n x u \ 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\s` by auto - have lem5:"\x. x\s \ x\a \ kle n x a' \ kle n a' x" proof- case goal1 thus ?case - proof(cases "kle n v x \ kle n x u") case True thus ?thesis using goal1 by(auto intro:lem3 lem4) next - case False hence *:"kle n u x" "kle n x v" using ksimplexD(6)[OF assms(1)] using goal1 `u\s` `v\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) proof(rule_tac[2-] ballI,rule_tac[4] ballI) - show "card (insert a' (s - {a})) = n + 1" using ksimplexD(2-3)[OF assms(1)] - using `a'\a` `a'\s` `a\s` by(auto simp add:card_insert_if) - fix x assume x:"x \ insert a' (s - {a})" - show "\j. x j \ p" proof(rule,cases "x = a'") - fix j case False thus "x j\p" using x ksimplexD(4)[OF assms(1)] by auto next - fix j case True show "x j\p" unfolding True proof(cases "j=l") - case False thus "a' j \p" unfolding True a'_def using `u\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\l` by auto - have "u l + 1 \ p" unfolding *[symmetric] using ksimplexD(4)[OF assms(1)] using `v\s` by auto - thus "a' j \p" unfolding a'_def True by auto qed qed - show "\j. j \ {1..n} \ x j = p" proof(rule,rule,cases "x=a'") fix j::nat assume j:"j\{1..n}" - { case False thus "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto } - case True show "x j = p" unfolding True a'_def using j l(1) - using ksimplexD(5)[OF assms(1),rule_format,OF `u\s` j] by auto qed - fix y assume y:"y\insert a' (s - {a})" - show "kle n x y \ kle n y x" proof(cases "y=a'") - case True show ?thesis unfolding True apply(cases "x=a'") defer apply(rule lem5) using x by auto 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 thus ?thesis apply(rule_tac ksimplexD(6)[OF assms(1),rule_format]) - using x y `y\a'` by auto qed qed qed - hence "insert a' (s - {a}) \ ?A" unfolding mem_Collect_eq apply-apply(rule,assumption) - apply(rule_tac x="a'" in bexI) using aa' `a'\s` by auto moreover - have "s \ ?A" using assms(1,2) by auto ultimately have "?A \ {s, insert a' (s - {a})}" by auto - moreover have "?A \ {s, insert a' (s - {a})}" apply(rule) unfolding mem_Collect_eq proof(erule conjE) - fix s' assume as:"ksimplex p n s'" and "\b\s'. s' - {b} = s - {a}" - from this(2) guess a'' .. note a''=this - have "u\v" unfolding fun_eq_iff unfolding l(2) k(2) by auto - hence uv':"\ kle n v u" using uv using kle_antisym by auto - have "u\a" "v\a" unfolding fun_eq_iff k(2) l(2) by auto - hence uvs':"u\s'" "v\s'" using `u\s` `v\s` using a'' by auto - have lem6:"a \ s' \ a' \ s'" proof(cases "\x\s'. kle n x u \ kle n v x") - case False then guess w unfolding ball_simps .. note w=this - hence "kle n u w" "kle n w v" using ksimplexD(6)[OF as] uvs' by auto - hence "w = a' \ w = a" using uxv[of w] uvs' w by auto thus ?thesis using w by auto next - case True have "\ (\x\s'. kle n x u)" unfolding ball_simps apply(rule_tac x=v in bexI) - using uv `u\v` unfolding kle_antisym[of n u v,symmetric] using `v\s'` by auto - hence "\y\s'. \k\{1..n}. \j. y j = (if j = k then u j + 1 else u j)" using ksimplex_successor[OF as `u\s'`] by blast - then guess w .. note w=this from this(2) guess kk .. note kk=this[rule_format] - have "\ kle n w u" apply-apply(rule,drule kle_imp_pointwise) - apply(erule_tac x=kk in allE) unfolding kk by auto - hence *:"kle n v w" using True[rule_format,OF w(1)] by auto - hence False proof(cases "kk\l") case True thus False using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)] - apply(erule_tac x=l in allE) using `k\l` by auto next - case False hence "kk\k" using `k\l` by auto thus False using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)] - apply(erule_tac x=k in allE) using `k\l` by auto qed - thus ?thesis by auto qed + 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 + hence aa': "a' \ 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' \ s" + apply rule + apply (drule ksimplexD(6)[OF assms(1),rule_format,OF `a\s`]) + proof (cases "kle n a a'") + case goal2 + hence "kle n a' a" by auto + thus 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 + thus 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: "\x. kle n u x \ kle n x v \ x = u \ x = a \ x = a' \ x = v" + proof - + case goal1 + thus ?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 + thus ?case + apply (cases "x = l") + apply (case_tac[!] "x = k") + using as by auto + qed + thus ?case by auto + next + assume as: "x l \ 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 + thus ?case + apply (cases "x = l") + apply (case_tac[!] "x = k") + using as + apply auto + done + qed + thus ?case by auto + next + assume as: "x l = u l" "x k \ 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 + thus ?case + apply (cases "x = l") + apply (case_tac[!] "x = k") + using as + apply auto + done + qed + thus ?case by auto + next + assume as: "x l \ u l" "x k \ 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 + thus ?case + apply (cases "x = l") + apply (case_tac[!] "x = k") + using as `k \ l` + apply auto + done + qed + thus ?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: "\x. x \ s \ kle n v x \ 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\s` + apply auto + done + have lem4: "\x. x\s \ kle n x u \ 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\s` + apply auto + done + have lem5: "\x. x \ s \ x \ a \ kle n x a' \ kle n a' x" + proof - + case goal1 + thus ?case + proof (cases "kle n v x \ kle n x u") + case True + thus ?thesis using goal1 by(auto intro:lem3 lem4) + next + case False + hence *: "kle n u x" "kle n x v" + using ksimplexD(6)[OF assms(1)] + using goal1 `u\s` `v\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) + proof (rule_tac[2-] ballI, rule_tac[4] ballI) + show "card (insert a' (s - {a})) = n + 1" + using ksimplexD(2-3)[OF assms(1)] + using `a' \ a` `a' \ s` `a \ s` + by (auto simp add:card_insert_if) + fix x + assume x: "x \ insert a' (s - {a})" + show "\j. x j \ p" + proof (rule, cases "x = a'") + fix j + case False + thus "x j\p" using x ksimplexD(4)[OF assms(1)] by auto + next + fix j + case True + show "x j\p" unfolding True + proof (cases "j = l") + case False + thus "a' j \p" + unfolding True a'_def using `u\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\l` by auto + have "u l + 1 \ p" + unfolding *[symmetric] using ksimplexD(4)[OF assms(1)] using `v\s` by auto + thus "a' j \p" unfolding a'_def True by auto + qed + qed + show "\j. j \ {1..n} \ x j = p" + proof (rule, rule,cases "x = a'") + fix j :: nat + assume j: "j \ {1..n}" + { + case False + thus "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto + next + case True + show "x j = p" + unfolding True a'_def + using j l(1) + using ksimplexD(5)[OF assms(1),rule_format,OF `u\s` j] + by auto + } + qed + fix y + assume y: "y\insert a' (s - {a})" + show "kle n x y \ 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 + thus ?thesis + apply (rule_tac ksimplexD(6)[OF assms(1),rule_format]) + using x y `y\a'` + apply auto + done + qed + qed + qed + hence "insert a' (s - {a}) \ ?A" + unfolding mem_Collect_eq + apply - + apply (rule, assumption) + apply (rule_tac x = "a'" in bexI) + using aa' `a' \ s` + apply auto + done + moreover + have "s \ ?A" using assms(1,2) by auto + ultimately have "?A \ {s, insert a' (s - {a})}" by auto + moreover + have "?A \ {s, insert a' (s - {a})}" + apply rule unfolding mem_Collect_eq + proof (erule conjE) + fix s' + assume as: "ksimplex p n s'" and "\b\s'. s' - {b} = s - {a}" + from this(2) guess a'' .. note a'' = this + have "u \ v" unfolding fun_eq_iff unfolding l(2) k(2) by auto + hence uv': "\ kle n v u" using uv using kle_antisym by auto + have "u \ a" "v \ a" unfolding fun_eq_iff k(2) l(2) by auto + hence uvs': "u \ s'" "v \ s'" using `u \ s` `v \ s` using a'' by auto + have lem6: "a \ s' \ a' \ s'" + proof (cases "\x\s'. kle n x u \ kle n v x") + case False + then guess w unfolding ball_simps .. note w = this + hence "kle n u w" "kle n w v" + using ksimplexD(6)[OF as] uvs' by auto + hence "w = a' \ w = a" + using uxv[of w] uvs' w by auto + thus ?thesis using w by auto + next + case True + have "\ (\x\s'. kle n x u)" + unfolding ball_simps + apply (rule_tac x=v in bexI) + using uv `u \ v` + unfolding kle_antisym [of n u v,symmetric] + using `v\s'` + apply auto + done + hence "\y\s'. \k\{1..n}. \j. y j = (if j = k then u j + 1 else u j)" + using ksimplex_successor[OF as `u\s'`] by blast + then guess w .. note w = this + from this(2) guess kk .. note kk = this[rule_format] + have "\ kle n w u" + apply - + apply (rule, drule kle_imp_pointwise) + apply (erule_tac x = kk in allE) + unfolding kk + apply auto + done + hence *: "kle n v w" + using True[rule_format,OF w(1)] by auto + hence False + proof (cases "kk \ l") + case True + thus False using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)] + apply (erule_tac x=l in allE) + using `k \ l` + apply auto + done + next + case False + hence "kk \ k" using `k \ l` by auto + thus False using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)] + apply (erule_tac x=k in allE) + using `k \ l` + apply auto + done + qed + thus ?thesis by auto + qed thus "s' \ {s, insert a' (s - {a})}" proof(cases "a\s'") - case True hence "s' = s" apply-apply(rule lem1[OF a''(2)]) using a'' `a\s` by auto - thus ?thesis by auto next case False hence "a'\s'" using lem6 by auto - hence "s' = insert a' (s - {a})" apply-apply(rule lem1[of _ a'' _ a']) - unfolding a''(2)[symmetric] using a'' using `a'\s` by auto - thus ?thesis by auto qed qed - ultimately have *:"?A = {s, insert a' (s - {a})}" by blast + case True + hence "s' = s" + apply - + apply (rule lem1[OF a''(2)]) + using a'' `a \ s` + apply auto + done + thus ?thesis by auto + next + case False hence "a'\s'" using lem6 by auto + hence "s' = insert a' (s - {a})" + apply - + apply (rule lem1[of _ a'' _ a']) + unfolding a''(2)[symmetric] using a'' and `a'\s` by auto + thus ?thesis by auto + qed + qed + ultimately have *: "?A = {s, insert a' (s - {a})}" by blast have "s \ insert a' (s - {a})" using `a'\s` by auto - hence ?thesis unfolding * by auto } - ultimately show ?thesis by auto qed + hence ?thesis unfolding * by auto + } + ultimately show ?thesis by auto +qed + subsection {* Hence another step towards concreteness. *} lemma kuhn_simplex_lemma: assumes "\s. ksimplex p (n + 1) s \ (rl ` s \{0..n+1})" - "odd (card{f. \s a. ksimplex p (n + 1) s \ a \ s \ (f = s - {a}) \ - (rl ` f = {0 .. n}) \ ((\j\{1..n+1}.\x\f. x j = 0) \ (\j\{1..n+1}.\x\f. x j = p))})" - shows "odd(card {s\{s. ksimplex p (n + 1) s}. rl ` s = {0..n+1} })" proof- - have *:"\x y. x = y \ odd (card x) \ odd (card y)" by auto - have *:"odd(card {f\{f. \s\{s. ksimplex p (n + 1) s}. (\a\s. f = s - {a})}. - (rl ` f = {0..n}) \ - ((\j\{1..n+1}. \x\f. x j = 0) \ - (\j\{1..n+1}. \x\f. x j = p))})" apply(rule *[OF _ assms(2)]) by auto - show ?thesis apply(rule kuhn_complete_lemma[OF finite_simplices]) prefer 6 apply(rule *) apply(rule,rule,rule) - apply(subst ksimplex_def) defer apply(rule,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\s" "f = s - {a}" + "odd (card{f. \s a. ksimplex p (n + 1) s \ a \ s \ (f = s - {a}) \ + (rl ` f = {0 .. n}) \ ((\j\{1..n+1}.\x\f. x j = 0) \ (\j\{1..n+1}.\x\f. x j = p))})" + shows "odd(card {s\{s. ksimplex p (n + 1) s}. rl ` s = {0..n+1} })" +proof - + have *: "\x y. x = y \ odd (card x) \ odd (card y)" + by auto + have *: "odd(card {f\{f. \s\{s. ksimplex p (n + 1) s}. (\a\s. f = s - {a})}. + (rl ` f = {0..n}) \ + ((\j\{1..n+1}. \x\f. x j = 0) \ + (\j\{1..n+1}. \x\f. x j = p))})" + apply (rule *[OF _ assms(2)]) + apply auto + done + show ?thesis + apply (rule kuhn_complete_lemma[OF finite_simplices]) + prefer 6 + apply (rule *) + apply (rule, rule, rule) + apply (subst ksimplex_def) + defer + apply (rule, 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\s" "f = s - {a}" let ?S = "{s. ksimplex p (n + 1) s \ (\a\s. f = s - {a})}" - have S:"?S = {s'. ksimplex p (n + 1) s' \ (\b\s'. s' - {b} = s - {a})}" unfolding as by blast - { fix j assume j:"j \ {1..n + 1}" "\x\f. x j = 0" thus "card {s. ksimplex p (n + 1) s \ (\a\s. f = s - {a})} = 1" unfolding S - apply-apply(rule ksimplex_replace_0) apply(rule as)+ unfolding as by auto } - { fix j assume j:"j \ {1..n + 1}" "\x\f. x j = p" thus "card {s. ksimplex p (n + 1) s \ (\a\s. f = s - {a})} = 1" unfolding S - apply-apply(rule ksimplex_replace_1) apply(rule as)+ unfolding as by auto } + have S: "?S = {s'. ksimplex p (n + 1) s' \ (\b\s'. s' - {b} = s - {a})}" + unfolding as by blast + { + fix j + assume j: "j \ {1..n + 1}" "\x\f. x j = 0" + thus "card {s. ksimplex p (n + 1) s \ (\a\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 \ {1..n + 1}" "\x\f. x j = p" + thus "card {s. ksimplex p (n + 1) s \ (\a\s. f = s - {a})} = 1" + unfolding S + apply - + apply (rule ksimplex_replace_1) + apply (rule as)+ + unfolding as + apply auto + done + } show "\ ((\j\{1..n+1}. \x\f. x j = 0) \ (\j\{1..n+1}. \x\f. x j = p)) \ card ?S = 2" - unfolding S apply(rule ksimplex_replace_2) apply(rule as)+ unfolding as by auto qed auto qed + unfolding S + apply (rule ksimplex_replace_2) + apply (rule as)+ + unfolding as + apply auto + done + qed auto +qed + subsection {* Reduced labelling. *} definition "reduced label (n::nat) (x::nat\nat) = - (SOME k. k \ n \ (\i. 1\i \ i label x i = 0) \ (k = n \ label x (k + 1) \ (0::nat)))" + (SOME k. k \ n \ (\i. 1\i \ i label x i = 0) \ + (k = n \ label x (k + 1) \ (0::nat)))" -lemma reduced_labelling: shows "reduced label n x \ n" (is ?t1) and - "\i. 1\i \ i < reduced label n x + 1 \ (label x i = 0)" (is ?t2) - "(reduced label n x = n) \ (label x (reduced label n x + 1) \ 0)" (is ?t3) proof- - have num_WOP:"\P k. P (k::nat) \ \n. P n \ (\m P m)" - apply(drule ex_has_least_nat[where m="\x. x"]) apply(erule exE,rule_tac x=x in exI) by auto - have *:"n \ n \ (label x (n + 1) \ 0 \ n = n)" by auto - then guess N apply(drule_tac num_WOP[of "\j. j\n \ (label x (j+1) \ 0 \ n = j)"]) apply(erule exE) . note N=this - have N':"N \ n" "\i. 1 \ i \ i < N + 1 \ label x i = 0" "N = n \ label x (N + 1) \ 0" defer proof(rule,rule) - fix i assume i:"1\i \ i n" (is ?t1) + and "\i. 1\i \ i < reduced label n x + 1 \ (label x i = 0)" (is ?t2) + and "(reduced label n x = n) \ (label x (reduced label n x + 1) \ 0)" (is ?t3) +proof - + have num_WOP: "\P k. P (k::nat) \ \n. P n \ (\m P m)" + apply (drule ex_has_least_nat[where m="\x. x"]) + apply (erule exE,rule_tac x=x in exI) + apply auto + done + have *: "n \ n \ (label x (n + 1) \ 0 \ n = n)" by auto + then guess N + apply (drule_tac num_WOP[of "\j. j\n \ (label x (j+1) \ 0 \ n = j)"]) + apply (erule exE) + done + note N = this + have N': "N \ n" + "\i. 1 \ i \ i < N + 1 \ label x i = 0" "N = n \ label x (N + 1) \ 0" + defer + proof (rule, rule) + fix i + assume i: "1\i \ i nat" - assumes "r \ n" "\i. 1 \ i \ i < r + 1 \ (label x i = 0)" "(r = n) \ (label x (r + 1) \ 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 by auto +lemma reduced_labelling_unique: + fixes x :: "nat \ nat" + assumes "r \ n" + "\i. 1 \ i \ i < r + 1 \ (label x i = 0)" "(r = n) \ (label x (r + 1) \ 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 -lemma reduced_labelling_zero: assumes "j\{1..n}" "label x j = 0" shows "reduced label n x \ j - 1" - using reduced_labelling[of label n x] using assms by fastforce +lemma reduced_labelling_zero: + assumes "j\{1..n}" "label x j = 0" + shows "reduced label n x \ j - 1" + using reduced_labelling[of label n x] + using assms by fastforce -lemma reduced_labelling_nonzero: assumes "j\{1..n}" "label x j \ 0" shows "reduced label n x < j" - using assms and reduced_labelling[of label n x] apply(erule_tac x=j in allE) by auto +lemma reduced_labelling_nonzero: + assumes "j\{1..n}" "label x j \ 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_Suc: - assumes "reduced lab (n + 1) x \ 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 by auto + assumes "reduced lab (n + 1) x \ 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 complete_face_top: assumes "\x\f. \j\{1..n+1}. x j = 0 \ lab x j = 0" "\x\f. \j\{1..n+1}. x j = p \ lab x j = 1" shows "((reduced lab (n + 1)) ` f = {0..n}) \ ((\j\{1..n+1}. \x\f. x j = 0) \ (\j\{1..n+1}. \x\f. x j = p)) \ - ((reduced lab (n + 1)) ` f = {0..n}) \ (\x\f. x (n + 1) = p)" (is "?l = ?r") proof - assume ?l (is "?as \ (?a \ ?b)") thus ?r apply-apply(rule,erule conjE,assumption) proof(cases ?a) - case True then guess j .. note j=this {fix x assume x:"x\f" - have "reduced lab (n+1) x \ j - 1" using j apply-apply(rule reduced_labelling_zero) defer apply(rule assms(1)[rule_format]) using x by auto } + ((reduced lab (n + 1)) ` f = {0..n}) \ (\x\f. x (n + 1) = p)" (is "?l = ?r") +proof + assume ?l (is "?as \ (?a \ ?b)") + thus ?r + apply - + apply (rule, erule conjE, assumption) + proof (cases ?a) + case True + then guess j .. note j = this + { + fix x + assume x: "x \ f" + have "reduced lab (n + 1) x \ 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 \ {0..n}" using j by auto then guess y unfolding `?l`[THEN conjunct1,symmetric] and image_iff .. note y = this - ultimately have False by auto thus "\x\f. x (n + 1) = p" by auto next + ultimately have False by auto + thus "\x\f. x (n + 1) = p" by auto + next + case False + hence ?b using `?l` by blast + then guess j .. note j = this + { + fix x + assume x: "x \ 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) + case goal1 + hence "j < n + 1" using j by auto + moreover + have "n \ {0..n}" by auto + then guess y unfolding `?l`[THEN conjunct1,symmetric] image_iff .. + ultimately show False using *[of y] by auto + qed + thus "\x\f. x (n + 1) = p" using j by auto + qed +qed(auto) - case False hence ?b using `?l` by blast then guess j .. note j=this {fix x assume x:"x\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 by auto } note * = this - have "j = n + 1" proof(rule ccontr) case goal1 hence "j < n + 1" using j by auto moreover - have "n \ {0..n}" by auto then guess y unfolding `?l`[THEN conjunct1,symmetric] image_iff .. - ultimately show False using *[of y] by auto qed - thus "\x\f. x (n + 1) = p" using j by auto qed qed(auto) subsection {* Hence we get just about the nice induction. *}