# HG changeset patch # User wenzelm # Date 1379369600 -7200 # Node ID 7ac7b2eaa5e6f4d4b7277178cce99a96d907d1d9 # Parent bcfd16f65014fb15dfa537e4dd0a8e5fd784311b tuned proofs; diff -r bcfd16f65014 -r 7ac7b2eaa5e6 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Sep 16 23:08:02 2013 +0200 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Sep 17 00:13:20 2013 +0200 @@ -1,3 +1,6 @@ +(* Author: John Harrison + Author: Robert Himmelmann, TU Muenchen (Translation from HOL light) +*) (* ========================================================================= *) (* Results connected with topological dimension. *) @@ -13,41 +16,51 @@ (* (c) Copyright, John Harrison 1998-2008 *) (* ========================================================================= *) -(* Author: John Harrison - Translation from HOL light: Robert Himmelmann, TU Muenchen *) - header {* Results connected with topological dimension. *} theory Brouwer_Fixpoint - imports Convex_Euclidean_Space +imports Convex_Euclidean_Space begin (** move this **) lemma divide_nonneg_nonneg: - assumes "a \ 0" "b \ 0" + assumes "a \ 0" + and "b \ 0" shows "0 \ a / (b::real)" - apply (cases "b=0") - defer - apply (rule divide_nonneg_pos) - using assms - apply auto - done +proof (cases "b = 0") + case True + then show ?thesis by auto +next + case False + show ?thesis + apply (rule divide_nonneg_pos) + using assms False + apply auto + done +qed lemma brouwer_compactness_lemma: fixes f :: "'a::metric_space \ 'b::euclidean_space" - assumes "compact s" "continuous_on s f" "\ (\x\s. (f x = 0))" - obtains d where "0 < d" "\x\s. d \ norm(f x)" + assumes "compact s" + and "continuous_on s f" + and "\ (\x\s. (f x = 0))" + obtains d where "0 < d" and "\x\s. d \ norm (f x)" proof (cases "s = {}") + case True + show thesis by (rule that [of 1]) (auto simp: True) +next case False have "continuous_on s (norm \ f)" by (rule continuous_on_intros continuous_on_norm assms(2))+ - with False obtain x where x: "x\s" "\y\s. (norm \ f) x \ (norm \ f) y" - using continuous_attains_inf[OF assms(1), of "norm \ f"] unfolding o_def by auto - have "(norm \ f) x > 0" using assms(3) and x(1) by auto - then show ?thesis by (rule that) (insert x(2), auto simp: o_def) -next - case True - show thesis by (rule that [of 1]) (auto simp: True) + with False obtain x where x: "x \ s" "\y\s. (norm \ f) x \ (norm \ f) y" + using continuous_attains_inf[OF assms(1), of "norm \ f"] + unfolding o_def + by auto + have "(norm \ f) x > 0" + using assms(3) and x(1) + by auto + then show ?thesis + by (rule that) (insert x(2), auto simp: o_def) qed lemma kuhn_labelling_lemma: @@ -112,7 +125,7 @@ {f\faces. compo' f \ face f x}" "\x. {f \ faces. compo' f \ bnd f \ face f x} \ {f \ faces. compo' f \ \ bnd f \ face f x} = {}" by auto - hence lem1:"setsum (\s. (card {f \ faces. face f s \ compo' f})) simplices = + then have lem1:"setsum (\s. (card {f \ faces. face f s \ compo' f})) simplices = setsum (\s. card {f \ {f \ faces. compo' f \ bnd f}. face f s}) simplices + setsum (\s. card {f \ {f \ faces. compo' f \ \ (bnd f)}. face f s}) simplices" unfolding setsum_addf[symmetric] @@ -557,13 +570,13 @@ apply - proof (erule disjE) assume "kle n a x" - hence "x = a" + then have "x = a" apply - unfolding pointwise_antisym[symmetric] apply (drule kle_imp_pointwise) using a(2)[rule_format,OF `x\s`] apply auto done - thus ?thesis using kle_refl by auto + then show ?thesis using kle_refl by auto qed qed (insert a, auto) qed @@ -573,12 +586,12 @@ shows "1 \ card {k\{1..n}. x k < y k}" proof - guess i using kle_strict(2)[OF assms] .. - hence "card {i} \ card {k\{1..n}. x k < y k}" + then have "card {i} \ card {k\{1..n}. x k < y k}" apply - apply (rule card_mono) apply auto done - thus ?thesis by auto + then show ?thesis by auto qed lemma kle_range_combine: @@ -611,22 +624,22 @@ assume as: "i \ {1..n}" "x i < y i" "j \ {1..n}" "y j < z j" "\ i \ j" guess kx using assms(1)[unfolded kle_def] .. note kx = this have "x i < y i" using as by auto - hence "i \ kx" using as(1) kx + then have "i \ kx" using as(1) kx apply (rule_tac ccontr) apply auto done - hence "x i + 1 = y i" using kx by auto + then have "x i + 1 = y i" using kx by auto moreover guess ky using assms(2)[unfolded kle_def] .. note ky = this have "y i < z i" using as by auto - hence "i \ ky" using as(1) ky + then have "i \ ky" using as(1) ky apply (rule_tac ccontr) apply auto done - hence "y i + 1 = z i" using ky by auto + then have "y i + 1 = z i" using ky by auto ultimately have "z i = x i + 2" by auto - thus False using assms(3) unfolding kle_def + then show False using assms(3) unfolding kle_def by (auto simp add: split_if_eq1) qed have fin: "\P. finite {x\{1..n::nat}. P x}" by auto @@ -659,10 +672,10 @@ proof - have "finite s" "s\{}" using assms(1) by (auto intro: card_ge_0_finite) - thus ?thesis using assms + then show ?thesis using assms proof (induct m arbitrary: s) case 0 - thus ?case using kle_refl by auto + then show ?case using kle_refl by auto next case (Suc m) then obtain a where a: "a \ s" "\x\s. kle n a x" @@ -670,7 +683,7 @@ show ?case proof (cases "s \ {a}") case False - hence "card (s - {a}) = Suc m" "s - {a} \ {}" + then have "card (s - {a}) = Suc m" "s - {a} \ {}" using card_Diff_singleton[OF _ a(1)] Suc(4) `finite s` by auto then obtain x b where xb:"x\s - {a}" "b\s - {a}" "kle n x b" "m \ card {k \ {1..n}. x k < b k}" @@ -681,7 +694,7 @@ using a and xb apply auto done - thus ?thesis + then show ?thesis apply (rule_tac x=a in bexI, rule_tac x=b in bexI) using kle_range_combine[OF a(2)[rule_format] xb(3) Suc(5)[rule_format], of 1 "m"] using a(1) xb(1-2) @@ -689,10 +702,10 @@ done next case True - hence "s = {a}" using Suc(3) by auto - hence "card s = 1" by auto - hence False using Suc(4) `finite s` by auto - thus ?thesis by auto + then have "s = {a}" using Suc(3) by auto + then have "card s = 1" by auto + then have False using Suc(4) `finite s` by auto + then show ?thesis by auto qed qed qed @@ -725,7 +738,7 @@ show "c i = a i + (if i \ kk1 \ kk2 then 1 else 0)" proof (cases "i \ kk1 \ kk2") case True - hence "c i \ a i + (if i \ kk1 \ kk2 then 1 else 0)" + then have "c i \ a i + (if i \ kk1 \ kk2 then 1 else 0)" unfolding kk1[THEN conjunct2,rule_format,of i] kk2[THEN conjunct2,rule_format,of i] by auto moreover @@ -734,7 +747,7 @@ ultimately show ?thesis by auto next case False - thus ?thesis using kk1 kk2 by auto + then show ?thesis using kk1 kk2 by auto qed qed (insert kk1 kk2, auto) qed @@ -809,10 +822,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 \ @@ -858,7 +871,7 @@ using c_d a b apply auto done - hence "kle n a b \ n \ card {k\{1..n}. a(k) < b(k)}" + then have "kle n a b \ n \ card {k\{1..n}. a(k) < b(k)}" apply - apply (rule kle_range_combine_l[where y=c]) using a `c \ s` `b \ s` @@ -883,7 +896,7 @@ show "b i = (if i \ {1..n} \ a i < b i then a i + 1 else a i)" proof (cases "i \ {1..n}") case True - thus ?thesis unfolding k[THEN conjunct2,rule_format] by auto + then show ?thesis unfolding k[THEN conjunct2,rule_format] by auto next case False have "a i = p" using assm and False `a\s` by auto @@ -908,7 +921,7 @@ apply (drule cong[of _ _ 1 1]) using ab(4) assms(2) apply auto done - thus ?thesis + then show ?thesis apply (rule_tac that[of a b]) using ab apply auto done @@ -926,7 +939,7 @@ shows "(\x\s. kle n x a) \ (\y\s. \k\{1..n}. \j. y(j) = (if j = k then a(j) + 1 else a(j)))" proof (cases "\x\s. kle n x a") case True - thus ?thesis by auto + then show ?thesis by auto next note assm = ksimplexD[OF assms(1)] case False @@ -945,7 +958,7 @@ using assm(2) and False apply auto done - hence sizekle1: "card ?kle1 = Suc (card ?kle1 - 1)" + then have sizekle1: "card ?kle1 = Suc (card ?kle1 - 1)" using assm(2) by auto obtain c d where c_d: "c \ s" "\ kle n c a" "d \ s" "\ kle n d a" "kle n c d" "card ?kle1 - 1 \ card {k \ {1..n}. c k < d k}" @@ -957,7 +970,7 @@ using assm(6)[rule_format,of a a] and `a\s` and assm(2) apply auto done - hence sizekle2: "card ?kle2 = Suc (card ?kle2 - 1)" + then have sizekle2: "card ?kle2 = Suc (card ?kle2 - 1)" using assm(2) by auto obtain e f where e_f: "e \ s" "kle n e a" "f \ s" "kle n f a" "kle n e f" "card ?kle2 - 1 \ card {k \ {1..n}. e k < f k}" @@ -966,7 +979,7 @@ have "card {k\{1..n}. a k < b k} = 1" proof (rule ccontr) case goal1 - hence as: "card {k\{1..n}. a k < b k} \ 2" + then have as: "card {k\{1..n}. a k < b k} \ 2" using ** by auto have *: "finite ?kle2" "finite ?kle1" "?kle2 \ ?kle1 = s" "?kle2 \ ?kle1 = {}" using assm(2) by auto @@ -986,7 +999,7 @@ using c_d using assm(6) and b apply auto done - hence "kle n a d \ 2 + (card {x \ s. \ kle n x a} - 1) \ card {k \ {1..n}. a k < d k}" + then have "kle n a d \ 2 + (card {x \ s. \ kle n x a} - 1) \ card {k \ {1..n}. a k < d k}" apply - apply (rule kle_range_combine[where y=b]) using as and b assm(6) `a\s` `d\s` apply blast+ @@ -1043,13 +1056,13 @@ shows "(\x\s. kle n a x) \ (\y\s. \k\{1..n}. \j. a(j) = (if j = k then y(j) + 1 else y(j)))" proof (cases "\x\s. kle n a x") case True - thus ?thesis by auto + then show ?thesis by auto next note assm = ksimplexD[OF assms(1)] case False then obtain b where b:"b\s" "\ kle n a b" "\x\{x \ s. \ kle n a x}. kle n x b" using kle_maximal[of "{x\s. \ kle n a x}" n] and assm by auto - hence **: "1 \ card {k\{1..n}. a k > b k}" + then have **: "1 \ card {k\{1..n}. a k > b k}" apply - apply (rule kle_strict_set) using assm(6) and `a\s` @@ -1062,7 +1075,7 @@ using assm(2) and False apply auto done - hence sizekle1: "card ?kle1 = Suc (card ?kle1 - 1)" + then have sizekle1: "card ?kle1 = Suc (card ?kle1 - 1)" using assm(2) by auto obtain c d where c_d: "c \ s" "\ kle n a c" "d \ s" "\ kle n a d" "kle n d c" "card ?kle1 - 1 \ card {k \ {1..n}. c k > d k}" @@ -1074,7 +1087,7 @@ using assm(6)[rule_format,of a a] and `a\s` and assm(2) apply auto done - hence sizekle2:"card ?kle2 = Suc (card ?kle2 - 1)" + then have sizekle2:"card ?kle2 = Suc (card ?kle2 - 1)" using assm(2) by auto obtain e f where e_f: "e \ s" "kle n a e" "f \ s" "kle n a f" "kle n f e" "card ?kle2 - 1 \ card {k \ {1..n}. e k > f k}" @@ -1083,7 +1096,7 @@ have "card {k\{1..n}. a k > b k} = 1" proof (rule ccontr) case goal1 - hence as: "card {k\{1..n}. a k > b k} \ 2" + then have as: "card {k\{1..n}. a k > b k} \ 2" using ** by auto have *: "finite ?kle2" "finite ?kle1" "?kle2 \ ?kle1 = s" "?kle2 \ ?kle1 = {}" using assm(2) by auto @@ -1103,7 +1116,7 @@ using c_d and assm(6) and b apply auto done - hence "kle n d a \ (card {x \ s. \ kle n a x} - 1) + 2 \ card {k \ {1..n}. a k > d k}" + then have "kle n d a \ (card {x \ s. \ kle n a x} - 1) + 2 \ card {k \ {1..n}. a k > d k}" apply - apply (rule kle_range_combine[where y=b]) using as and b assm(6) `a\s` `d\s` apply blast+ @@ -1138,18 +1151,18 @@ show "a j = (if j = k then b j + 1 else b j)" proof (cases "j \ kk") case True - hence "j = k" + then have "j = k" apply - apply (rule k(2)[rule_format]) using kk_raw kkk apply auto done - thus ?thesis unfolding kk using kkk by auto + then show ?thesis unfolding kk using kkk by auto next case False - hence "j \ k" using k(2)[rule_format, of j k] + then have "j \ k" using k(2)[rule_format, of j k] using kk_raw kkk by auto - thus ?thesis unfolding kk + then show ?thesis unfolding kk using kkk and False by auto qed qed (insert k(1) `b\s`, auto) @@ -1198,7 +1211,7 @@ assume as: "x = (\(b, g) x. if x = a then b else g x) xa" "xb \ UNIV - insert a s0" "xa = (xc, y)" "xc \ t" "\x\s0. y x \ t" "\x\UNIV - s0. y x = d" - thus "x xb = d" unfolding as by auto + then show "x xb = d" unfolding as by auto qed auto have inj: "inj_on ?l {(b,g). b\t \ g\?M s0}" unfolding inj_on_def @@ -1214,10 +1227,10 @@ show "ya x = yb x" proof (cases "x = a") case False - thus ?thesis using as(1)[THEN cong[of _ _ x x]] by auto + then show ?thesis using as(1)[THEN cong[of _ _ x x]] by auto next case True - thus ?thesis using as(5,7) using as0(2) by auto + then show ?thesis using as(5,7) using as0(2) by auto qed qed ultimately show ?case unfolding goal1 by auto @@ -1244,17 +1257,17 @@ case True have "card ?S = (card t) ^ (card s)" using assms by (auto intro!: card_funspace) - thus ?thesis using True by (rule_tac card_ge_0_finite) simp + then show ?thesis using True by (rule_tac card_ge_0_finite) simp next - case False hence "t = {}" using `finite t` by auto + case False then have "t = {}" using `finite t` by auto show ?thesis proof (cases "s = {}") have *: "{f. \x. f x = d} = {\x. d}" by auto case True - thus ?thesis using `t = {}` by (auto simp: *) + then show ?thesis using `t = {}` by (auto simp: *) next case False - thus ?thesis using `t = {}` by simp + then show ?thesis using `t = {}` by simp qed qed @@ -1294,7 +1307,7 @@ proof (cases "kle (n + 1) x y") case True then guess k unfolding kle_def .. note k = this - hence *: "n + 1 \ k" using xyp by auto + then have *: "n + 1 \ k" using xyp by auto have "\ (\x\k. x\{1..n})" apply (rule notI) apply (erule bexE) @@ -1302,9 +1315,9 @@ fix x assume as: "x \ k" "x \ {1..n}" have "x \ n + 1" using as and * by auto - thus False using as and k[THEN conjunct1,unfolded subset_eq] by auto + then show False using as and k[THEN conjunct1,unfolded subset_eq] by auto qed - thus ?thesis + then show ?thesis apply - apply (rule disjI1) unfolding kle_def @@ -1314,7 +1327,7 @@ done next case False - hence "kle (n + 1) y x" + then have "kle (n + 1) y x" using ksimplexD(6)[OF sa(1),rule_format, of x y] and as by auto then guess k unfolding kle_def .. note k = this then have *: "n + 1 \ k" using xyp by auto @@ -1340,7 +1353,7 @@ next fix x j assume as: "x \ s - {a}" "j\{1..n}" - thus "x j = p" + then show "x j = p" using as(1)[unfolded sa(3)[symmetric], THEN assms(2)[rule_format]] apply (cases "j = n+1") using sa(1)[unfolded ksimplex_def] @@ -1358,7 +1371,7 @@ using assms(1) apply auto done - thus ?ls + then show ?ls apply (rule_tac x = "insert c f" in exI, rule_tac x = c in exI) unfolding ksimplex_def conj_assoc apply (rule conjI) @@ -1372,7 +1385,7 @@ proof (rule_tac[3-5] ballI allI)+ fix x j assume x: "x \ insert c f" - thus "x j \ p" + then show "x j \ p" proof (cases "x=c") case True show ?thesis @@ -1391,17 +1404,17 @@ { fix z assume z: "z \ insert c f" - hence "kle (n + 1) c z" + then have "kle (n + 1) c z" apply (cases "z = c") (*defer apply(rule kle_Suc)*) proof - case False - hence "z \ f" using z by auto + then have "z \ f" using z by auto then guess k apply (drule_tac ab(3)[THEN bspec[where x=z], THEN conjunct1]) unfolding kle_def apply (erule exE) done - thus "kle (n + 1) c z" + then show "kle (n + 1) c z" unfolding kle_def apply (rule_tac x="insert (n + 1) k" in exI) unfolding c_def @@ -1415,7 +1428,7 @@ assume y: "y \ insert c f" show "kle (n + 1) x y \ kle (n + 1) y x" proof (cases "x = c \ y = c") - case False hence **: "x \ f" "y \ f" using x y by auto + case False then have **: "x \ f" "y \ f" using x y by auto show ?thesis using rs(6)[rule_format,OF **] by (auto dest: kle_Suc) qed (insert * x y, auto) @@ -1497,7 +1510,7 @@ unfolding kle_antisym[symmetric, of b0 a0 n] using exta extb and goal1(3) unfolding a a' by blast - hence "b1 = a1" + then have "b1 = a1" apply - apply (rule ext) unfolding exta(5) extb(5) @@ -1602,9 +1615,9 @@ 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 + then have "a \ insert b (s - {a})" by auto + then have "a \ s - {a}" unfolding insert_iff using goal1 by auto + then show False by auto qed guess a0 a1 by (rule ksimplex_extrema_strong[OF assms(1,3)]) note a0a1 = this { @@ -1619,7 +1632,7 @@ 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)" + then have "\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`]]) apply auto done @@ -1629,20 +1642,20 @@ have "a3 \ s" proof assume "a3\s" - hence "kle n a3 a1" + then have "kle n a3 a1" using a0a1(4) by auto - thus False + then show 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 + then have "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 + then have 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 @@ -1653,8 +1666,8 @@ using goal1(2) apply auto done - hence "x = a2" using as by auto - thus False using goal1(2) using kle_refl by auto + then have "x = a2" using as by auto + then show False using goal1(2) using kle_refl by auto qed let ?s = "insert a3 (s - {a0})" have "ksimplex p n ?s" @@ -1670,14 +1683,14 @@ proof (rule, cases "x = a3") fix j case False - thus "x j\p" using x ksimplexD(4)[OF assms(1)] by auto + then show "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 + then show "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)] .. @@ -1689,7 +1702,7 @@ 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] + then show "a3 j \p" unfolding a3_def unfolding a0a1(5)[rule_format] using k(1) k(2)assms(5) using * by simp qed qed @@ -1699,7 +1712,7 @@ assume j: "j \ {1..n}" { case False - thus "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto + then show "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto } case True show "x j = p" @@ -1718,14 +1731,14 @@ 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 + then have "a1 k = x k + 1" using kk by auto + then have "a0 k = x k" unfolding a0a1(5)[rule_format] using k(1) by auto + then have "a2 k = x k + 1" unfolding k(2)[rule_format] by auto moreover have "a2 k \ x k" using lem3[of x,THEN kle_imp_pointwise] goal1 by auto ultimately show False by auto qed - thus ?case + then show ?case unfolding kle_def apply (rule_tac x="insert k kk" in exI) using kk(1) @@ -1758,7 +1771,7 @@ done next case False - thus ?thesis + then show ?thesis apply (rule_tac ksimplexD(6)[OF assms(1),rule_format]) using x y `y \ a3` apply auto @@ -1766,7 +1779,7 @@ qed qed qed - hence "insert a3 (s - {a0}) \ ?A" + then have "insert a3 (s - {a0}) \ ?A" unfolding mem_Collect_eq apply - apply (rule, assumption) @@ -1792,13 +1805,13 @@ proof fix x assume x: "x \ s - {a}" - hence "kle n a2 x" + then have "kle n a2 x" apply - apply (rule lem3) using `a = a0` apply auto done - hence "a2 k \ x k" + then have "a2 k \ x k" apply (drule_tac kle_imp_pointwise) apply auto done @@ -1827,30 +1840,30 @@ 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 + then have "a_max = a'" using a' min_max by auto + then show 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` + then have "\i. a_max i = a1 i" by auto + then have "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 + then show ?case by (cases "x\{1..n}") auto qed - hence "s' = s" + then have "s' = s" apply - apply (rule lem1[OF a'(2)]) using `a\s` `a'\s'` apply auto done - thus ?thesis by auto + then show ?thesis by auto next case False - hence as:"a' = a_max" using ** by auto + then have as:"a' = a_max" using ** by auto have "a_min = a2" unfolding kle_antisym[symmetric, of _ _ n] apply rule apply (rule min_max(4)[rule_format,THEN conjunct1]) @@ -1861,12 +1874,12 @@ 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}" + then have "a2 \ s - {a}" using a2 by auto - thus "a2 \ s'" unfolding a'(2)[symmetric] by auto + then show "a2 \ s'" unfolding a'(2)[symmetric] by auto qed - hence "\i. a_min i = a2 i" by auto - hence "a' = a3" + then have "\i. a_min i = a2 i" by auto + then have "a' = a3" unfolding as `a = a0` apply - apply (subst fun_eq_iff, rule) @@ -1885,7 +1898,7 @@ apply auto done qed - hence "s' = insert a3 (s - {a0})" + then have "s' = insert a3 (s - {a0})" apply - apply (rule lem1) defer @@ -1895,12 +1908,12 @@ using `a3 \ s` apply auto done - thus ?thesis by auto + then show ?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 + then have ?thesis unfolding * by auto } moreover { @@ -1916,7 +1929,7 @@ 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)" + then have "\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`]]) apply auto done @@ -1926,7 +1939,7 @@ have lem3: "\x. x\(s - {a1}) \ kle n x a2" proof (rule ccontr) case goal1 - hence as: "x\s" "x\a1" by auto + then have 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 @@ -1937,8 +1950,8 @@ using goal1(2) apply auto done - hence "x = a2" using as by auto - thus False using goal1(2) using kle_refl by auto + then have "x = a2" using as by auto + then show False using goal1(2) using kle_refl by auto qed have "a0 k \ 0" proof - @@ -1948,10 +1961,10 @@ 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 + then have "a1 k > 1" unfolding k(2)[rule_format] by simp + then show ?thesis unfolding a0a1(5)[rule_format] using k(1) by simp qed - hence lem4: "\j. a0 j = (if j=k then a3 j + 1 else a3 j)" + then have 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) @@ -1961,8 +1974,8 @@ 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 + then have "a3 \ s" using a0a1(4) by auto + then have "a3 \ a1" "a3 \ a0" using a0a1 by auto let ?s = "insert a3 (s - {a1})" have "ksimplex p n ?s" apply (rule ksimplexI) @@ -1976,14 +1989,14 @@ 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 + then show "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" + then show "a3 j \p" unfolding True a3_def using `a0\s` ksimplexD(4)[OF assms(1)] by auto @@ -2004,7 +2017,7 @@ assume j: "j \ {1..n}" { case False - thus "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto + then show "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) @@ -2016,12 +2029,12 @@ have lem4: "\x. x\s \ x \ a1 \ kle n a3 x" proof - case goal1 - hence *: "x\s - {a1}" by auto + then have *: "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 + then show ?thesis unfolding kle_def apply (rule_tac x=kk in exI) unfolding lem4[rule_format] k(2)[rule_format] @@ -2029,7 +2042,7 @@ defer proof rule case goal1 - thus ?case + then show ?case apply - apply (erule conjE) apply (erule_tac[!] x=j in allE) @@ -2079,7 +2092,7 @@ done next case False - thus ?thesis + then show ?thesis apply (rule_tac ksimplexD(6)[OF assms(1),rule_format]) using x y `y\