--- 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 \<in> s" "\<forall>y. y \<in> s \<longrightarrow> y = x"
+ fix x
+ assume as: "x \<in> s" "\<forall>y. y \<in> s \<longrightarrow> y = x"
have *: "s = insert x {}"
apply (rule set_eqI, rule) unfolding singleton_iff
apply (rule as(2)[rule_format]) using as(1)
@@ -180,12 +181,17 @@
lemma card_2_exists: "card s = 2 \<longleftrightarrow> (\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. (z = x) \<or> (z = y)))"
proof
assume "card s = 2"
- then obtain x y where obt:"s = {x, y}" "x\<noteq>y" unfolding numeral_2_eq_2
- apply - apply (erule exE conjE | drule card_eq_SucD)+ apply auto done
- show "\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y)" using obt by auto
+ then obtain x y where s: "s = {x, y}" "x\<noteq>y" unfolding numeral_2_eq_2
+ apply -
+ apply (erule exE conjE | drule card_eq_SucD)+
+ apply auto
+ done
+ show "\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y)"
+ using s by auto
next
assume "\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y)"
- then obtain x y where "x\<in>s" "y\<in>s" "x \<noteq> y" "\<forall>z\<in>s. z = x \<or> z = y" by auto
+ then obtain x y where "x\<in>s" "y\<in>s" "x \<noteq> y" "\<forall>z\<in>s. z = x \<or> z = y"
+ by auto
then have "s = {x, y}" by auto
with `x \<noteq> y` show "card s = 2" by auto
qed
@@ -247,8 +253,9 @@
then obtain a where "a\<in>?M" by auto
then have a: "a\<in>s" "f ` (s - {a}) = t - {b}" by auto
have "f a \<in> t - {b}" using a and assms by auto
- then have "\<exists>c \<in> s - {a}. f a = f c" unfolding image_iff[symmetric] and a by auto
- then obtain c where c:"c \<in> s" "a \<noteq> c" "f a = f c" by auto
+ then have "\<exists>c \<in> s - {a}. f a = f c"
+ unfolding image_iff[symmetric] and a by auto
+ then obtain c where c: "c \<in> s" "a \<noteq> c" "f a = f c" by auto
then have *: "f ` (s - {c}) = f ` (s - {a})"
apply -
apply (rule set_eqI, 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\<in>?M" unfolding mem_Collect_eq and * using a and c(1) by auto
+ have "c\<in>?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\<in>?M`], rule bexI[OF _ `c\<in>?M`],rule,rule `a\<noteq>c`)
+ 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)
fix z
assume as: "z \<in> s" "f ` (s - {z}) = t - {b}"
have inj: "inj_on f (s - {z})"
apply (rule eq_card_imp_inj_on)
- unfolding as using as(1) and assms apply auto
+ unfolding as using as(1) and assms
+ apply auto
done
show "z = a \<or> z = c"
proof (rule ccontr)
assume "\<not> ?thesis"
then show False
using inj[unfolded inj_on_def, THEN bspec[where x=a], THEN bspec[where x=c]]
- using `a\<in>s` `c\<in>s` `f a = f c` `a\<noteq>c` apply auto
+ using `a\<in>s` `c\<in>s` `f a = f c` `a\<noteq>c`
+ apply auto
done
qed
qed
@@ -362,9 +373,10 @@
done
next
case False
- obtain a b where a: "a\<in>insert x F" "\<forall>x\<in>F. \<forall>j. a j \<le> x j" and
- b: "b\<in>insert x F" "\<forall>x\<in>F. \<forall>j. x j \<le> b j" using as(3)[OF False] using as(5) by auto
- have "\<exists>a\<in>insert x F. \<forall>x\<in>insert x F. \<forall>j. a j \<le> x j"
+ obtain a b where a: "a\<in>insert x F" "\<forall>x\<in>F. \<forall>j. a j \<le> x j"
+ and b: "b \<in> insert x F" "\<forall>x\<in>F. \<forall>j. x j \<le> b j"
+ using as(3)[OF False] using as(5) by auto
+ have "\<exists>a \<in> insert x F. \<forall>x \<in> insert x F. \<forall>j. a j \<le> x j"
using as(5)[rule_format,OF a(1) insertI1]
apply -
proof (erule disjE)
@@ -386,7 +398,8 @@
qed
moreover
have "\<exists>b\<in>insert x F. \<forall>x\<in>insert x F. \<forall>j. x j \<le> b j"
- using as(5)[rule_format,OF b(1) insertI1] apply-
+ using as(5)[rule_format,OF b(1) insertI1]
+ apply -
proof (erule disjE)
assume "\<forall>j. x j \<le> b j"
then show ?thesis
@@ -409,7 +422,8 @@
qed auto
-lemma kle_imp_pointwise: "kle n x y \<Longrightarrow> (\<forall>j. x j \<le> y j)" unfolding kle_def by auto
+lemma kle_imp_pointwise: "kle n x y \<Longrightarrow> (\<forall>j. x j \<le> y j)"
+ unfolding kle_def by auto
lemma pointwise_antisym:
fixes x :: "nat \<Rightarrow> nat"
@@ -445,7 +459,7 @@
proof -
guess k using assms(1)[unfolded kle_def] .. note k = this
show "\<exists>k. 1 \<le> k \<and> k \<le> n \<and> 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 \<in> s"
@@ -706,7 +720,8 @@
fix j
show "x j \<le> b j + 1"
apply (rule *)
- using kle_trans_1[OF assms(1),of j] kle_trans_1[OF assms(3), of j] apply auto
+ 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 \<le> x j + 1"
apply (rule *)
- using kle_trans_1[OF assms(2),of j] kle_trans_1[OF assms(4), of j] apply auto
+ 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 \<le> a j" using kle_imp_pointwise[OF assms(3),THEN spec[where x=j]]
- unfolding assms(1)[rule_format] apply-apply(cases "j=k")
- using True 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 \<Rightarrow> nat) set) \<longleftrightarrow>
- (card s = n + 1 \<and>
- (\<forall>x\<in>s. \<forall>j. x(j) \<le> p) \<and>
- (\<forall>x\<in>s. \<forall>j. j\<notin>{1..n} \<longrightarrow> (x j = p)) \<and>
- (\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x))"
+ (card s = n + 1 \<and>
+ (\<forall>x\<in>s. \<forall>j. x(j) \<le> p) \<and>
+ (\<forall>x\<in>s. \<forall>j. j\<notin>{1..n} \<longrightarrow> (x j = p)) \<and>
+ (\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x))"
lemma ksimplexI:
"card s = n + 1 \<Longrightarrow>
@@ -1081,7 +1102,7 @@
thus ?thesis unfolding kk
using kkk and False by auto
qed
- qed(insert k(1) `b\<in>s`, auto)
+ qed (insert k(1) `b\<in>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. \<forall>x. f x = d} = {\<lambda>x. d}" by auto
+ have *: "{f. \<forall>x. f x = d} = {\<lambda>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 \<in> s" "n \<noteq> 0" "j\<in>{1..n}" "\<forall>x\<in>s - {a}. x j = p"
- shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 1" proof-
- have lem:"\<And>a a' s'. s' - {a'} = s - {a} \<Longrightarrow> a' = a \<Longrightarrow> a' \<in> s' \<Longrightarrow> a \<in> s \<Longrightarrow> s' = s" by auto
- have lem:"\<And>s' a'. ksimplex p n s' \<Longrightarrow> a'\<in>s' \<Longrightarrow> s' - {a'} = s - {a} \<Longrightarrow> s' = s" proof- case goal1
- 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\<in>{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' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 1"
+proof -
+ have lem: "\<And>a a' s'. s' - {a'} = s - {a} \<Longrightarrow> a' = a \<Longrightarrow> a' \<in> s' \<Longrightarrow> a \<in> s \<Longrightarrow> s' = s"
+ by auto
+ have lem: "\<And>s' a'. ksimplex p n s' \<Longrightarrow> a'\<in>s' \<Longrightarrow> s' - {a'} = s - {a} \<Longrightarrow> s' = s"
+ proof -
+ case goal1
+ 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 \<in> {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 \<in> s" "n \<noteq> 0" "~(\<exists>j\<in>{1..n}. \<forall>x\<in>s - {a}. x j = 0)" "~(\<exists>j\<in>{1..n}. \<forall>x\<in>s - {a}. x j = p)"
- shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 2" (is "card ?A = 2") proof-
- have lem1:"\<And>a a' s s'. s' - {a'} = s - {a} \<Longrightarrow> a' = a \<Longrightarrow> a' \<in> s' \<Longrightarrow> a \<in> s \<Longrightarrow> s' = s" by auto
- have lem2:"\<And>a b. a\<in>s \<Longrightarrow> b\<noteq>a \<Longrightarrow> s \<noteq> insert b (s - {a})" proof case goal1
- hence "a\<in>insert b (s - {a})" by auto hence "a\<in> 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 *:"\<And>P Q. (P \<or> Q) \<Longrightarrow> \<not> P \<Longrightarrow> Q" by auto
- have "\<exists>x\<in>s. \<not> kle n x a0" apply(rule_tac x=a1 in bexI) proof assume as:"kle n a1 a0"
- show False using kle_imp_pointwise[OF as,THEN spec[where x=1]] unfolding a0a1(5)[THEN spec[where x=1]]
- using assms(3) by auto qed(insert a0a1,auto)
+ assumes "ksimplex p n s" "a \<in> s"
+ "n \<noteq> 0"
+ "~(\<exists>j\<in>{1..n}. \<forall>x\<in>s - {a}. x j = 0)"
+ "~(\<exists>j\<in>{1..n}. \<forall>x\<in>s - {a}. x j = p)"
+ shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 2"
+ (is "card ?A = 2")
+proof -
+ have lem1: "\<And>a a' s s'. s' - {a'} = s - {a} \<Longrightarrow> a' = a \<Longrightarrow> a' \<in> s' \<Longrightarrow> a \<in> s \<Longrightarrow> s' = s"
+ by auto
+ have lem2: "\<And>a b. a\<in>s \<Longrightarrow> b\<noteq>a \<Longrightarrow> s \<noteq> insert b (s - {a})"
+ proof
+ case goal1
+ hence "a \<in> insert b (s - {a})" by auto
+ hence "a \<in> 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 *: "\<And>P Q. (P \<or> Q) \<Longrightarrow> \<not> P \<Longrightarrow> Q" by auto
+ have "\<exists>x\<in>s. \<not> kle n x a0"
+ apply (rule_tac x=a1 in bexI)
+ proof
+ assume as: "kle n a1 a0"
+ show False
+ using kle_imp_pointwise[OF as,THEN spec[where x=1]]
+ unfolding a0a1(5)[THEN spec[where x=1]]
+ using assms(3) by auto
+ qed (insert a0a1, auto)
hence "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then a0 j + 1 else a0 j)"
- apply(rule_tac *[OF ksimplex_successor[OF assms(1-2),unfolded `a=a0`]]) by auto
- then guess a2 .. from this(2) guess k .. note k=this note a2=`a2\<in>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 \<in> s`
def a3 \<equiv> "\<lambda>j. if j = k then a1 j + 1 else a1 j"
- have "a3 \<notin> s" proof assume "a3\<in>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 \<notin> s"
+ proof
+ assume "a3\<in>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 \<noteq> a0" "a3 \<noteq> a1" using a0a1 by auto
have "a2 \<noteq> a0" using k(2)[THEN spec[where x=k]] by auto
- have lem3:"\<And>x. x\<in>(s - {a0}) \<Longrightarrow> kle n a2 x" proof(rule ccontr) case goal1 hence as:"x\<in>s" "x\<noteq>a0" by auto
- have "kle n a2 x \<or> kle n x a2" using ksimplexD(6)[OF assms(1)] and as `a2\<in>s` by auto moreover
+ have lem3: "\<And>x. x\<in>(s - {a0}) \<Longrightarrow> kle n a2 x"
+ proof (rule ccontr)
+ case goal1
+ hence as: "x\<in>s" "x\<noteq>a0" by auto
+ have "kle n a2 x \<or> kle n x a2"
+ using ksimplexD(6)[OF assms(1)] and as `a2\<in>s` by auto
+ moreover
have "kle n a0 x" using a0a1(4) as by auto
- ultimately have "x = a0 \<or> x = a2" apply-apply(rule kle_adjacent[OF k(2)]) using goal1(2) 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\<noteq>a0` `a3\<notin>s` `a0\<in>s` by(auto simp add:card_insert_if)
- fix x assume x:"x \<in> insert a3 (s - {a0})"
- show "\<forall>j. x j \<le> p" proof(rule,cases "x = a3")
- fix j case False thus "x j\<le>p" using x ksimplexD(4)[OF assms(1)] by auto next
- fix j case True show "x j\<le>p" unfolding True proof(cases "j=k")
- case False thus "a3 j \<le>p" unfolding True a3_def using `a1\<in>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 \<le> a4 k" using lem3[OF a4(1)[unfolded `a=a0`],THEN kle_imp_pointwise] by auto
- also have "\<dots> < p" using ksimplexD(4)[OF assms(1),rule_format,of a4 k] using a4 by auto
- finally have *:"a0 k + 1 < p" unfolding k(2)[rule_format] by auto
- case True thus "a3 j \<le>p" unfolding a3_def unfolding a0a1(5)[rule_format]
- using k(1) k(2)assms(5) using * by simp qed qed
- show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p" proof(rule,rule,cases "x=a3") fix j::nat assume j:"j\<notin>{1..n}"
- { 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\<in>s` j] by auto qed
- fix y assume y:"y\<in>insert a3 (s - {a0})"
- have lem4:"\<And>x. x\<in>s \<Longrightarrow> x\<noteq>a0 \<Longrightarrow> kle n x a3" proof- case goal1
- guess kk using a0a1(4)[rule_format,OF `x\<in>s`,THEN conjunct2,unfolded kle_def]
- apply-apply(erule exE,erule conjE) . note kk=this
- have "k\<notin>kk" proof assume "k\<in>kk"
+ ultimately have "x = a0 \<or> 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\<noteq>a0` `a3\<notin>s` `a0\<in>s`
+ by (auto simp add:card_insert_if)
+ fix x
+ assume x: "x \<in> insert a3 (s - {a0})"
+ show "\<forall>j. x j \<le> p"
+ proof (rule, cases "x = a3")
+ fix j
+ case False
+ thus "x j\<le>p" using x ksimplexD(4)[OF assms(1)] by auto
+ next
+ fix j
+ case True
+ show "x j\<le>p" unfolding True
+ proof (cases "j = k")
+ case False
+ thus "a3 j \<le>p" unfolding True a3_def
+ using `a1\<in>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 \<le> a4 k"
+ using lem3[OF a4(1)[unfolded `a=a0`],THEN kle_imp_pointwise] by auto
+ also have "\<dots> < p"
+ using ksimplexD(4)[OF assms(1),rule_format,of a4 k] using a4 by auto
+ finally have *:"a0 k + 1 < p"
+ unfolding k(2)[rule_format] by auto
+ case True
+ thus "a3 j \<le>p" unfolding a3_def unfolding a0a1(5)[rule_format]
+ using k(1) k(2)assms(5) using * by simp
+ qed
+ qed
+ show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p"
+ proof (rule, rule, cases "x=a3")
+ fix j :: nat
+ assume j: "j \<notin> {1..n}"
+ {
+ 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\<in>s` j] by auto
+ qed
+ fix y
+ assume y: "y \<in> insert a3 (s - {a0})"
+ have lem4: "\<And>x. x\<in>s \<Longrightarrow> x\<noteq>a0 \<Longrightarrow> kle n x a3"
+ proof -
+ case goal1
+ guess kk using a0a1(4)[rule_format, OF `x\<in>s`,THEN conjunct2,unfolded kle_def]
+ by (elim exE conjE)
+ note kk = this
+ have "k \<notin> kk"
+ proof
+ assume "k \<in> 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 \<le> 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 \<or> kle n y x" proof(cases "y=a3")
- case True show ?thesis unfolding True apply(cases "x=a3") defer apply(rule disjI1,rule lem4)
- using x 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\<noteq>a3` by auto qed qed qed
- hence "insert a3 (s - {a0}) \<in> ?A" unfolding mem_Collect_eq apply-apply(rule,assumption)
- apply(rule_tac x="a3" in bexI) unfolding `a=a0` using `a3\<notin>s` by auto moreover
- have "s \<in> ?A" using assms(1,2) by auto ultimately have "?A \<supseteq> {s, insert a3 (s - {a0})}" by auto
- moreover have "?A \<subseteq> {s, insert a3 (s - {a0})}" apply(rule) unfolding mem_Collect_eq proof(erule conjE)
- fix s' assume as:"ksimplex p n s'" and "\<exists>b\<in>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 *:"\<forall>x\<in>s' - {a'}. x k = a2 k" unfolding a' proof fix x assume x:"x\<in>s-{a}"
- hence "kle n a2 x" apply-apply(rule lem3) using `a=a0` by auto
- hence "a2 k \<le> x k" apply(drule_tac kle_imp_pointwise) by auto moreover
- have "x k \<le> a2 k" unfolding k(2)[rule_format] using a0a1(4)[rule_format,of x,THEN conjunct1]
- unfolding kle_def using x by auto ultimately show "x k = a2 k" by auto qed
- have **:"a'=a_min \<or> a'=a_max" apply(rule ksimplex_fix_plane[OF a'(1) k(1) *]) using min_max by auto
- show "s' \<in> {s, insert a3 (s - {a0})}" proof(cases "a'=a_min")
- case True have "a_max = a1" unfolding kle_antisym[symmetric,of a_max a1 n] apply(rule)
- apply(rule a0a1(4)[rule_format,THEN conjunct2]) defer proof(rule min_max(4)[rule_format,THEN conjunct2])
+ 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 \<or> kle n y x"
+ proof (cases "y = a3")
+ case True
+ show ?thesis
+ unfolding True
+ apply (cases "x = a3")
+ defer
+ apply (rule disjI1, rule lem4)
+ using x
+ apply auto
+ done
+ next
+ case False
+ show ?thesis
+ proof (cases "x = a3")
+ case True
+ show ?thesis
+ unfolding True
+ apply (rule disjI2, 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 \<noteq> a3`
+ apply auto
+ done
+ qed
+ qed
+ qed
+ hence "insert a3 (s - {a0}) \<in> ?A"
+ unfolding mem_Collect_eq
+ apply -
+ apply (rule, assumption)
+ apply (rule_tac x = "a3" in bexI)
+ unfolding `a = a0`
+ using `a3 \<notin> s`
+ apply auto
+ done
+ moreover
+ have "s \<in> ?A" using assms(1,2) by auto
+ ultimately have "?A \<supseteq> {s, insert a3 (s - {a0})}" by auto
+ moreover
+ have "?A \<subseteq> {s, insert a3 (s - {a0})}"
+ apply rule
+ unfolding mem_Collect_eq
+ proof (erule conjE)
+ fix s'
+ assume as: "ksimplex p n s'" and "\<exists>b\<in>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 *: "\<forall>x\<in>s' - {a'}. x k = a2 k"
+ unfolding a'
+ proof
+ fix x
+ assume x: "x \<in> s - {a}"
+ hence "kle n a2 x"
+ apply -
+ apply (rule lem3)
+ using `a = a0`
+ apply auto
+ done
+ hence "a2 k \<le> x k"
+ apply (drule_tac kle_imp_pointwise)
+ apply auto
+ done
+ moreover
+ have "x k \<le> a2 k"
+ unfolding k(2)[rule_format]
+ using a0a1(4)[rule_format,of x, THEN conjunct1]
+ unfolding kle_def using x by auto
+ ultimately show "x k = a2 k" by auto
+ qed
+ have **: "a' = a_min \<or> a' = a_max"
+ apply (rule ksimplex_fix_plane[OF a'(1) k(1) *])
+ using min_max
+ apply auto
+ done
+ show "s' \<in> {s, insert a3 (s - {a0})}"
+ proof (cases "a' = a_min")
+ case True
+ have "a_max = a1"
+ unfolding kle_antisym[symmetric,of a_max a1 n]
+ apply rule
+ apply (rule a0a1(4)[rule_format,THEN conjunct2])
+ defer
+ proof (rule min_max(4)[rule_format,THEN conjunct2])
show "a1\<in>s'" using a' unfolding `a=a0` using a0a1 by auto
- show "a_max \<in> s" proof(rule ccontr) assume "a_max\<notin>s"
+ show "a_max \<in> s"
+ proof (rule ccontr)
+ assume "a_max \<notin> 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 "\<forall>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\<in>{1..n}") by auto qed
- hence "s' = s" apply-apply(rule lem1[OF a'(2)]) using `a\<in>s` `a'\<in>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 \<in> 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\<in>{1..n}") auto
+ qed
+ hence "s' = s"
+ apply -
+ apply (rule lem1[OF a'(2)])
+ using `a\<in>s` `a'\<in>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 \<in> s - {a0}"
+ unfolding a'(2)[symmetric,unfolded `a = a0`]
unfolding as using min_max(1-3) by auto
- have "a2 \<noteq> a" unfolding `a=a0` using k(2)[rule_format,of k] by auto
- hence "a2 \<in> s - {a}" using a2 by auto thus "a2 \<in> s'" unfolding a'(2)[symmetric] by auto qed
+ have "a2 \<noteq> a"
+ unfolding `a = a0` using k(2)[rule_format,of k] by auto
+ hence "a2 \<in> s - {a}"
+ using a2 by auto
+ thus "a2 \<in> s'" unfolding a'(2)[symmetric] by auto
+ qed
hence "\<forall>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\<in>{1..n}") defer apply(cases "x=k")
- using `k\<in>{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\<notin>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\<in>{1..n}")
+ defer
+ apply (cases "x = k")
+ using `k\<in>{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 \<notin> s`
+ apply auto
+ done
+ thus ?thesis by auto
+ qed
+ qed
+ ultimately have *: "?A = {s, insert a3 (s - {a0})}" by blast
have "s \<noteq> insert a3 (s - {a0})" using `a3\<notin>s` by auto
- hence ?thesis unfolding * by auto } moreover
- { assume "a=a1"
- have *:"\<And>P Q. (P \<or> Q) \<Longrightarrow> \<not> P \<Longrightarrow> Q" by auto
- have "\<exists>x\<in>s. \<not> kle n a1 x" apply(rule_tac x=a0 in bexI) proof assume as:"kle n a1 a0"
- show False using kle_imp_pointwise[OF as,THEN spec[where x=1]] unfolding a0a1(5)[THEN spec[where x=1]]
- using assms(3) by auto qed(insert a0a1,auto)
+ hence ?thesis unfolding * by auto
+ }
+ moreover
+ {
+ assume "a = a1"
+ have *: "\<And>P Q. (P \<or> Q) \<Longrightarrow> \<not> P \<Longrightarrow> Q" by auto
+ have "\<exists>x\<in>s. \<not> kle n a1 x"
+ apply (rule_tac x=a0 in bexI)
+ proof
+ assume as: "kle n a1 a0"
+ show False
+ using kle_imp_pointwise[OF as,THEN spec[where x=1]]
+ unfolding a0a1(5)[THEN spec[where x=1]]
+ using assms(3)
+ by auto
+ qed (insert a0a1, auto)
hence "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. a1 j = (if j = k then y j + 1 else y j)"
- apply(rule_tac *[OF ksimplex_predecessor[OF assms(1-2),unfolded `a=a1`]]) by auto
- then guess a2 .. from this(2) guess k .. note k=this note a2=`a2\<in>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 \<in> s`
def a3 \<equiv> "\<lambda>j. if j = k then a0 j - 1 else a0 j"
have "a2 \<noteq> a1" using k(2)[THEN spec[where x=k]] by auto
- have lem3:"\<And>x. x\<in>(s - {a1}) \<Longrightarrow> kle n x a2" proof(rule ccontr) case goal1 hence as:"x\<in>s" "x\<noteq>a1" by auto
- have "kle n a2 x \<or> kle n x a2" using ksimplexD(6)[OF assms(1)] and as `a2\<in>s` by auto moreover
+ have lem3: "\<And>x. x\<in>(s - {a1}) \<Longrightarrow> kle n x a2"
+ proof (rule ccontr)
+ case goal1
+ hence as: "x\<in>s" "x\<noteq>a1" by auto
+ have "kle n a2 x \<or> kle n x a2"
+ using ksimplexD(6)[OF assms(1)] and as `a2\<in>s` by auto
+ moreover
have "kle n x a1" using a0a1(4) as by auto
- ultimately have "x = a2 \<or> x = a1" apply-apply(rule kle_adjacent[OF k(2)]) using goal1(2) by auto
- hence "x = a2" using as by auto thus False using goal1(2) using kle_refl by auto qed
- have "a0 k \<noteq> 0" proof-
- guess a4 using assms(4)[unfolded bex_simps ball_simps,rule_format,OF `k\<in>{1..n}`] .. note a4=this
- have "a4 k \<le> a2 k" using lem3[OF a4(1)[unfolded `a=a1`],THEN kle_imp_pointwise] by auto
- moreover have "a4 k > 0" using a4 by auto ultimately have "a2 k > 0" by auto
+ ultimately have "x = a2 \<or> 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 \<noteq> 0"
+ proof -
+ guess a4 using assms(4)[unfolded bex_simps ball_simps,rule_format,OF `k\<in>{1..n}`] ..
+ note a4 = this
+ have "a4 k \<le> a2 k" using lem3[OF a4(1)[unfolded `a=a1`],THEN kle_imp_pointwise]
+ by auto
+ moreover have "a4 k > 0" using a4 by auto
+ ultimately have "a2 k > 0" by auto
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:"\<forall>j. a0 j = (if j=k then a3 j + 1 else a3 j)" unfolding a3_def by simp
- have "\<not> kle n a0 a3" apply(rule 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: "\<forall>j. a0 j = (if j=k then a3 j + 1 else a3 j)"
+ unfolding a3_def by simp
+ have "\<not> kle n a0 a3"
+ apply (rule 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 \<notin> s" using a0a1(4) by auto
hence "a3 \<noteq> a1" "a3 \<noteq> a0" using a0a1 by auto
- let ?s = "insert a3 (s - {a1})" have "ksimplex p n ?s" apply(rule ksimplexI) proof(rule_tac[2-] ballI,rule_tac[4] ballI)
- show "card ?s = n+1" using ksimplexD(2-3)[OF assms(1)]
- using `a3\<noteq>a0` `a3\<notin>s` `a1\<in>s` by(auto simp add:card_insert_if)
- fix x assume x:"x \<in> insert a3 (s - {a1})"
+ let ?s = "insert a3 (s - {a1})"
+ have "ksimplex p n ?s"
+ apply (rule ksimplexI)
+ proof (rule_tac[2-] ballI,rule_tac[4] ballI)
+ show "card ?s = n+1"
+ using ksimplexD(2-3)[OF assms(1)]
+ using `a3\<noteq>a0` `a3\<notin>s` `a1\<in>s`
+ by(auto simp add:card_insert_if)
+ fix x
+ assume x: "x \<in> insert a3 (s - {a1})"
show "\<forall>j. x j \<le> p" proof(rule,cases "x = a3")
- fix j case False thus "x j\<le>p" using x ksimplexD(4)[OF assms(1)] by auto next
- fix j case True show "x j\<le>p" unfolding True proof(cases "j=k")
- case False thus "a3 j \<le>p" unfolding True a3_def using `a0\<in>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 \<le> a0 k" unfolding lem4[rule_format] by auto
- also have "\<dots> \<le> p" using ksimplexD(4)[OF assms(1),rule_format,of a0 k] a0a1 by auto
- finally show "a3 j \<le> p" unfolding True by auto qed qed
- show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p" proof(rule,rule,cases "x=a3") fix j::nat assume j:"j\<notin>{1..n}"
- { 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\<in>s` j] by auto qed
- fix y assume y:"y\<in>insert a3 (s - {a1})"
- have lem4:"\<And>x. x\<in>s \<Longrightarrow> x\<noteq>a1 \<Longrightarrow> kle n a3 x" proof- case goal1 hence *:"x\<in>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\<in>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 \<or> 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\<noteq>a3` by auto qed qed qed
- hence "insert a3 (s - {a1}) \<in> ?A" unfolding mem_Collect_eq apply-apply(rule,assumption)
- apply(rule_tac x="a3" in bexI) unfolding `a=a1` using `a3\<notin>s` by auto moreover
- have "s \<in> ?A" using assms(1,2) by auto ultimately have "?A \<supseteq> {s, insert a3 (s - {a1})}" by auto
- moreover have "?A \<subseteq> {s, insert a3 (s - {a1})}" apply(rule) unfolding mem_Collect_eq proof(erule conjE)
- fix s' assume as:"ksimplex p n s'" and "\<exists>b\<in>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 *:"\<forall>x\<in>s' - {a'}. x k = a2 k" unfolding a' proof fix x assume x:"x\<in>s-{a}"
- hence "kle n x a2" apply-apply(rule lem3) using `a=a1` by auto
- hence "x k \<le> a2 k" apply(drule_tac kle_imp_pointwise) by auto moreover
- { have "a2 k \<le> a0 k" using k(2)[rule_format,of k] unfolding a0a1(5)[rule_format] using k(1) by simp
- also have "\<dots> \<le> x k" using a0a1(4)[rule_format,of x,THEN conjunct1,THEN kle_imp_pointwise] x by auto
- finally have "a2 k \<le> x k" . } ultimately show "x k = a2 k" by auto qed
- have **:"a'=a_min \<or> a'=a_max" apply(rule ksimplex_fix_plane[OF a'(1) k(1) *]) using min_max by auto
- have "a2 \<noteq> 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 \<in> s' - {a'}" unfolding a' using a2 unfolding `a=a1` by auto
- show "s' \<in> {s, insert a3 (s - {a1})}" proof(cases "a'=a_min")
- case True have "a_max \<in> s - {a1}" using min_max unfolding a'(2)[unfolded `a=a1`,symmetric] True by auto
- 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\<le>p" using x ksimplexD(4)[OF assms(1)] by auto
+ next
+ fix j
+ case True
+ show "x j\<le>p" unfolding True
+ proof (cases "j = k")
+ case False
+ thus "a3 j \<le>p"
+ unfolding True a3_def
+ using `a0\<in>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 \<le> a0 k"
+ unfolding lem4[rule_format] by auto
+ also have "\<dots> \<le> p"
+ using ksimplexD(4)[OF assms(1),rule_format,of a0 k] a0a1 by auto
+ finally show "a3 j \<le> p"
+ unfolding True by auto
+ qed
+ qed
+ show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p"
+ proof (rule, rule, cases "x = a3")
+ fix j :: nat
+ assume j: "j \<notin> {1..n}"
+ {
+ 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\<in>s` j] by auto
+ }
+ qed
+ fix y
+ assume y: "y\<in>insert a3 (s - {a1})"
+ have lem4: "\<And>x. x\<in>s \<Longrightarrow> x \<noteq> a1 \<Longrightarrow> kle n a3 x"
+ proof -
+ case goal1
+ hence *: "x\<in>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 \<in> kk")
+ apply (case_tac[!] "j=k")
+ apply auto
+ done
+ qed auto
+ qed
+ moreover
+ have "kle n a3 a0"
+ unfolding kle_def lem4[rule_format]
+ apply (rule_tac x="{k}" in exI)
+ using k(1)
+ apply auto
+ done
+ ultimately
+ show ?case
+ apply -
+ apply (rule kle_between_l[of _ a0 _ a2])
+ using lem3[OF *]
+ using a0a1(4)[rule_format,OF goal1(1)]
+ apply auto
+ done
+ qed
+ show "kle n x y \<or> kle n y x"
+ proof (cases "y = a3")
+ case True
+ show ?thesis
+ unfolding True
+ apply (cases "x = a3")
+ defer
+ apply (rule disjI2, 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\<noteq>a3`
+ apply auto
+ done
+ qed
+ qed
+ qed
+ hence "insert a3 (s - {a1}) \<in> ?A"
+ unfolding mem_Collect_eq
+ apply -
+ apply (rule, assumption)
+ apply (rule_tac x = "a3" in bexI)
+ unfolding `a = a1`
+ using `a3 \<notin> s`
+ apply auto
+ done
+ moreover
+ have "s \<in> ?A" using assms(1,2) by auto
+ ultimately have "?A \<supseteq> {s, insert a3 (s - {a1})}" by auto
+ moreover have "?A \<subseteq> {s, insert a3 (s - {a1})}"
+ apply rule
+ unfolding mem_Collect_eq
+ proof (erule conjE)
+ fix s'
+ assume as: "ksimplex p n s'" and "\<exists>b\<in>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 *: "\<forall>x\<in>s' - {a'}. x k = a2 k" unfolding a'
+ proof
+ fix x
+ assume x: "x \<in> s - {a}"
+ hence "kle n x a2"
+ apply -
+ apply (rule lem3)
+ using `a = a1`
+ apply auto
+ done
+ hence "x k \<le> a2 k"
+ apply (drule_tac kle_imp_pointwise)
+ apply auto
+ done
+ moreover
+ {
+ have "a2 k \<le> a0 k"
+ using k(2)[rule_format,of k]
+ unfolding a0a1(5)[rule_format]
+ using k(1)
+ by simp
+ also have "\<dots> \<le> x k"
+ using a0a1(4)[rule_format,of x,THEN conjunct1,THEN kle_imp_pointwise] x
+ by auto
+ finally have "a2 k \<le> x k" .
+ }
+ ultimately show "x k = a2 k" by auto
+ qed
+ have **: "a' = a_min \<or> a' = a_max"
+ apply (rule ksimplex_fix_plane[OF a'(1) k(1) *])
+ using min_max
+ apply auto
+ done
+ have "a2 \<noteq> a1"
+ proof
+ assume as: "a2 = a1"
+ show False
+ using k(2)
+ unfolding as
+ apply (erule_tac x = k in allE)
+ apply auto
+ done
+ qed
+ hence a2': "a2 \<in> s' - {a'}"
+ unfolding a'
+ using a2
+ unfolding `a = a1`
+ by auto
+ show "s' \<in> {s, insert a3 (s - {a1})}"
+ proof (cases "a' = a_min")
+ case True
+ have "a_max \<in> s - {a1}"
+ using min_max
+ unfolding a'(2)[unfolded `a=a1`,symmetric] True
+ by auto
+ 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:"\<forall>i. a_max i = a2 i" by auto
- have *:"\<forall>j. a2 j = (if j\<in>{1..n} then a3 j + 1 else a3 j)"
- using k(2) unfolding lem4[rule_format] a0a1(5)[rule_format] apply-apply(rule,erule_tac x=j in allE)
- proof- case goal1 thus ?case apply(cases "j\<in>{1..n}",case_tac[!] "j=k") by auto qed
- have "\<forall>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\<in>{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 *: "\<forall>j. a2 j = (if j\<in>{1..n} then a3 j + 1 else a3 j)"
+ using k(2)
+ unfolding lem4[rule_format] a0a1(5)[rule_format]
+ apply -
+ apply (rule,erule_tac x=j in allE)
+ proof -
+ case goal1
+ thus ?case by (cases "j\<in>{1..n}",case_tac[!] "j=k") auto
+ qed
+ have "\<forall>i. a_min i = a3 i"
+ using a_max
+ apply -
+ apply (rule,erule_tac x=i in allE)
+ unfolding min_max(5)[rule_format] *[rule_format]
+ proof -
+ case goal1
+ thus ?case by (cases "i\<in>{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 \<in> s - {a1}" using min_max(1,3) unfolding a'(2)[symmetric,unfolded `a=a1`] as by auto
- thus "a_min \<in> s" by auto have "a0 \<in> s - {a1}" using a0a1(1-3) by auto thus "a0 \<in> s'"
- unfolding a'(2)[symmetric,unfolded `a=a1`] by auto qed
- hence "\<forall>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\<in>s` `a'\<in>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 \<in> s - {a1}"
+ using min_max(1,3)
+ unfolding a'(2)[symmetric,unfolded `a=a1`] as
+ by auto
+ thus "a_min \<in> s" by auto
+ have "a0 \<in> s - {a1}" using a0a1(1-3) by auto
+ thus "a0 \<in> s'" unfolding a'(2)[symmetric,unfolded `a=a1`] by auto
+ qed
+ hence "\<forall>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 \<in> s` `a' \<in> 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 \<noteq> insert a3 (s - {a1})" using `a3\<notin>s` by auto
- hence ?thesis unfolding * by auto } moreover
- { assume as:"a\<noteq>a0" "a\<noteq>a1" have "\<not> (\<forall>x\<in>s. kle n a x)" proof case goal1
- have "a=a0" unfolding kle_antisym[symmetric,of _ _ n] apply(rule)
- using goal1 a0a1 assms(2) by auto thus False using as by auto qed
- hence "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. a j = (if j = k then y j + 1 else y j)" using ksimplex_predecessor[OF assms(1-2)] by blast
- then guess u .. from this(2) guess k .. note k = this[rule_format] note u = `u\<in>s`
- have "\<not> (\<forall>x\<in>s. kle n x a)" proof case goal1
- have "a=a1" unfolding kle_antisym[symmetric,of _ _ n] apply(rule)
- using goal1 a0a1 assms(2) by auto thus False using as by auto qed
- hence "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then a j + 1 else a j)" using ksimplex_successor[OF assms(1-2)] by blast
- then guess v .. from this(2) guess l .. note l = this[rule_format] note v = `v\<in>s`
+ hence ?thesis unfolding * by auto
+ }
+ moreover
+ {
+ assume as: "a \<noteq> a0" "a \<noteq> a1" have "\<not> (\<forall>x\<in>s. kle n a x)"
+ proof
+ case goal1
+ have "a = a0"
+ unfolding kle_antisym[symmetric,of _ _ n]
+ apply rule
+ using goal1 a0a1 assms(2)
+ apply auto
+ done
+ thus False using as by auto
+ qed
+ hence "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. a j = (if j = k then y j + 1 else y j)"
+ using ksimplex_predecessor[OF assms(1-2)] by blast
+ then guess u .. from this(2) guess k .. note k = this[rule_format]
+ note u = `u \<in> s`
+ have "\<not> (\<forall>x\<in>s. kle n x a)"
+ proof
+ case goal1
+ have "a = a1"
+ unfolding kle_antisym[symmetric,of _ _ n]
+ apply rule
+ using goal1 a0a1 assms(2)
+ apply auto
+ done
+ thus False using as by auto
+ qed
+ hence "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then a j + 1 else a j)"
+ using ksimplex_successor[OF assms(1-2)] by blast
+ then guess v .. from this(2) guess l ..
+ note l = this[rule_format]
+ note v = `v\<in>s`
def a' \<equiv> "\<lambda>j. if j = l then u j + 1 else u j"
- have kl:"k \<noteq> l" proof assume "k=l" have *:"\<And>P. (if P then (1::nat) else 0) \<noteq> 2" by auto
+ have kl: "k \<noteq> l"
+ proof
+ assume "k = l"
+ have *: "\<And>P. (if P then (1::nat) else 0) \<noteq> 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'\<noteq>a" apply-apply rule unfolding fun_eq_iff unfolding a'_def k(2)
- apply(erule_tac x=l in allE) by auto
- have "a' \<notin> s" apply(rule) apply(drule ksimplexD(6)[OF assms(1),rule_format,OF `a\<in>s`]) proof(cases "kle n a a'")
- case goal2 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:"\<And>x. kle n u x \<Longrightarrow> kle n x v \<Longrightarrow> (x = u) \<or> (x = a) \<or> (x = a') \<or> (x = v)"
- proof- case goal1 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 \<noteq> u l" "x k = u k"
- have "x = a'" unfolding fun_eq_iff unfolding a'_def
- using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) 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 \<noteq> 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 \<noteq> u l" "x k \<noteq> u k"
- have "x = v" unfolding fun_eq_iff
- using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) 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\<noteq>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:"\<And>x. x\<in>s \<Longrightarrow> kle n v x \<Longrightarrow> kle n a' x" apply(rule kle_between_r[of _ u _ v])
- prefer 3 apply(rule kle_trans[OF uv]) defer apply(rule ksimplexD(6)[OF assms(1),rule_format])
- using kle_uv `u\<in>s` by auto
- have lem4:"\<And>x. x\<in>s \<Longrightarrow> kle n x u \<Longrightarrow> kle n x a'" apply(rule kle_between_l[of _ u _ v])
- prefer 4 apply(rule kle_trans[OF _ uv]) defer apply(rule ksimplexD(6)[OF assms(1),rule_format])
- using kle_uv `v\<in>s` by auto
- have lem5:"\<And>x. x\<in>s \<Longrightarrow> x\<noteq>a \<Longrightarrow> kle n x a' \<or> kle n a' x" proof- case goal1 thus ?case
- proof(cases "kle n v x \<or> 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\<in>s` `v\<in>s` by auto
- show ?thesis using uxv[OF *] using kle_uv using goal1 by auto qed qed
- have "ksimplex p n (insert a' (s - {a}))" apply(rule ksimplexI) 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'\<noteq>a` `a'\<notin>s` `a\<in>s` by(auto simp add:card_insert_if)
- fix x assume x:"x \<in> insert a' (s - {a})"
- show "\<forall>j. x j \<le> p" proof(rule,cases "x = a'")
- fix j case False thus "x j\<le>p" using x ksimplexD(4)[OF assms(1)] by auto next
- fix j case True show "x j\<le>p" unfolding True proof(cases "j=l")
- case False thus "a' j \<le>p" unfolding True a'_def using `u\<in>s` ksimplexD(4)[OF assms(1)] by auto next
- case True have *:"a l = u l" "v l = a l + 1" using k(2)[of l] l(2)[of l] `k\<noteq>l` by auto
- have "u l + 1 \<le> p" unfolding *[symmetric] using ksimplexD(4)[OF assms(1)] using `v\<in>s` by auto
- thus "a' j \<le>p" unfolding a'_def True by auto qed qed
- show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p" proof(rule,rule,cases "x=a'") fix j::nat assume j:"j\<notin>{1..n}"
- { 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\<in>s` j] by auto qed
- fix y assume y:"y\<in>insert a' (s - {a})"
- show "kle n x y \<or> kle n y x" proof(cases "y=a'")
- case True show ?thesis unfolding True apply(cases "x=a'") defer apply(rule lem5) using x 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\<noteq>a'` by auto qed qed qed
- hence "insert a' (s - {a}) \<in> ?A" unfolding mem_Collect_eq apply-apply(rule,assumption)
- apply(rule_tac x="a'" in bexI) using aa' `a'\<notin>s` by auto moreover
- have "s \<in> ?A" using assms(1,2) by auto ultimately have "?A \<supseteq> {s, insert a' (s - {a})}" by auto
- moreover have "?A \<subseteq> {s, insert a' (s - {a})}" apply(rule) unfolding mem_Collect_eq proof(erule conjE)
- fix s' assume as:"ksimplex p n s'" and "\<exists>b\<in>s'. s' - {b} = s - {a}"
- from this(2) guess a'' .. note a''=this
- have "u\<noteq>v" unfolding fun_eq_iff unfolding l(2) k(2) by auto
- hence uv':"\<not> kle n v u" using uv using kle_antisym by auto
- have "u\<noteq>a" "v\<noteq>a" unfolding fun_eq_iff k(2) l(2) by auto
- hence uvs':"u\<in>s'" "v\<in>s'" using `u\<in>s` `v\<in>s` using a'' by auto
- have lem6:"a \<in> s' \<or> a' \<in> s'" proof(cases "\<forall>x\<in>s'. kle n x u \<or> kle n v x")
- case False then 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' \<or> w = a" using uxv[of w] uvs' w by auto thus ?thesis using w by auto next
- case True have "\<not> (\<forall>x\<in>s'. kle n x u)" unfolding ball_simps apply(rule_tac x=v in bexI)
- using uv `u\<noteq>v` unfolding kle_antisym[of n u v,symmetric] using `v\<in>s'` by auto
- hence "\<exists>y\<in>s'. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then u j + 1 else u j)" using ksimplex_successor[OF as `u\<in>s'`] by blast
- then guess w .. note w=this from this(2) guess kk .. note kk=this[rule_format]
- have "\<not> 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\<noteq>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\<noteq>l` by auto next
- case False hence "kk\<noteq>k" using `k\<noteq>l` by auto thus False using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)]
- apply(erule_tac x=k in allE) using `k\<noteq>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' \<noteq> a"
+ apply -
+ apply rule
+ unfolding fun_eq_iff
+ unfolding a'_def k(2)
+ apply (erule_tac x=l in allE)
+ apply auto
+ done
+ have "a' \<notin> s"
+ apply rule
+ apply (drule ksimplexD(6)[OF assms(1),rule_format,OF `a\<in>s`])
+ proof (cases "kle n a a'")
+ case goal2
+ 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: "\<And>x. kle n u x \<Longrightarrow> kle n x v \<Longrightarrow> x = u \<or> x = a \<or> x = a' \<or> x = v"
+ proof -
+ case goal1
+ 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 \<noteq> u l" "x k = u k"
+ have "x = a'"
+ unfolding fun_eq_iff
+ unfolding a'_def
+ using goal1(2)[THEN kle_imp_pointwise]
+ unfolding l(2) k(2)
+ using goal1(1)[THEN kle_imp_pointwise]
+ apply -
+ apply rule
+ apply (erule_tac x = xa in allE)+
+ proof -
+ case goal1
+ 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 \<noteq> u k"
+ have "x = a"
+ unfolding fun_eq_iff
+ using goal1(2)[THEN kle_imp_pointwise]
+ unfolding l(2) k(2)
+ using goal1(1)[THEN kle_imp_pointwise]
+ apply -
+ apply rule
+ apply (erule_tac x=xa in allE)+
+ proof -
+ case goal1
+ 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 \<noteq> u l" "x k \<noteq> u k"
+ have "x = v"
+ unfolding fun_eq_iff
+ using goal1(2)[THEN kle_imp_pointwise]
+ unfolding l(2) k(2)
+ using goal1(1)[THEN kle_imp_pointwise]
+ apply -
+ apply rule
+ apply (erule_tac x=xa in allE)+
+ proof -
+ case goal1
+ thus ?case
+ apply (cases "x = l")
+ apply (case_tac[!] "x = k")
+ using as `k \<noteq> 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: "\<And>x. x \<in> s \<Longrightarrow> kle n v x \<Longrightarrow> kle n a' x"
+ apply (rule kle_between_r[of _ u _ v])
+ prefer 3
+ apply (rule kle_trans[OF uv])
+ defer
+ apply (rule ksimplexD(6)[OF assms(1), rule_format])
+ using kle_uv `u\<in>s`
+ apply auto
+ done
+ have lem4: "\<And>x. x\<in>s \<Longrightarrow> kle n x u \<Longrightarrow> kle n x a'"
+ apply (rule kle_between_l[of _ u _ v])
+ prefer 4
+ apply (rule kle_trans[OF _ uv])
+ defer
+ apply (rule ksimplexD(6)[OF assms(1), rule_format])
+ using kle_uv `v\<in>s`
+ apply auto
+ done
+ have lem5: "\<And>x. x \<in> s \<Longrightarrow> x \<noteq> a \<Longrightarrow> kle n x a' \<or> kle n a' x"
+ proof -
+ case goal1
+ thus ?case
+ proof (cases "kle n v x \<or> 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\<in>s` `v\<in>s`
+ by auto
+ show ?thesis
+ using uxv[OF *]
+ using kle_uv
+ using goal1
+ by auto
+ qed
+ qed
+ have "ksimplex p n (insert a' (s - {a}))"
+ apply (rule ksimplexI)
+ 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' \<noteq> a` `a' \<notin> s` `a \<in> s`
+ by (auto simp add:card_insert_if)
+ fix x
+ assume x: "x \<in> insert a' (s - {a})"
+ show "\<forall>j. x j \<le> p"
+ proof (rule, cases "x = a'")
+ fix j
+ case False
+ thus "x j\<le>p" using x ksimplexD(4)[OF assms(1)] by auto
+ next
+ fix j
+ case True
+ show "x j\<le>p" unfolding True
+ proof (cases "j = l")
+ case False
+ thus "a' j \<le>p"
+ unfolding True a'_def using `u\<in>s` ksimplexD(4)[OF assms(1)] by auto
+ next
+ case True
+ have *: "a l = u l" "v l = a l + 1"
+ using k(2)[of l] l(2)[of l] `k\<noteq>l` by auto
+ have "u l + 1 \<le> p"
+ unfolding *[symmetric] using ksimplexD(4)[OF assms(1)] using `v\<in>s` by auto
+ thus "a' j \<le>p" unfolding a'_def True by auto
+ qed
+ qed
+ show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p"
+ proof (rule, rule,cases "x = a'")
+ fix j :: nat
+ assume j: "j \<notin> {1..n}"
+ {
+ 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\<in>s` j]
+ by auto
+ }
+ qed
+ fix y
+ assume y: "y\<in>insert a' (s - {a})"
+ show "kle n x y \<or> kle n y x"
+ proof (cases "y = a'")
+ case True
+ show ?thesis
+ unfolding True
+ apply (cases "x = a'")
+ defer
+ apply (rule lem5)
+ using x
+ apply auto
+ done
+ next
+ case False
+ show ?thesis
+ proof (cases "x = a'")
+ case True
+ show ?thesis
+ unfolding True
+ using lem5[of y] using y by auto
+ next
+ case False
+ thus ?thesis
+ apply (rule_tac ksimplexD(6)[OF assms(1),rule_format])
+ using x y `y\<noteq>a'`
+ apply auto
+ done
+ qed
+ qed
+ qed
+ hence "insert a' (s - {a}) \<in> ?A"
+ unfolding mem_Collect_eq
+ apply -
+ apply (rule, assumption)
+ apply (rule_tac x = "a'" in bexI)
+ using aa' `a' \<notin> s`
+ apply auto
+ done
+ moreover
+ have "s \<in> ?A" using assms(1,2) by auto
+ ultimately have "?A \<supseteq> {s, insert a' (s - {a})}" by auto
+ moreover
+ have "?A \<subseteq> {s, insert a' (s - {a})}"
+ apply rule unfolding mem_Collect_eq
+ proof (erule conjE)
+ fix s'
+ assume as: "ksimplex p n s'" and "\<exists>b\<in>s'. s' - {b} = s - {a}"
+ from this(2) guess a'' .. note a'' = this
+ have "u \<noteq> v" unfolding fun_eq_iff unfolding l(2) k(2) by auto
+ hence uv': "\<not> kle n v u" using uv using kle_antisym by auto
+ have "u \<noteq> a" "v \<noteq> a" unfolding fun_eq_iff k(2) l(2) by auto
+ hence uvs': "u \<in> s'" "v \<in> s'" using `u \<in> s` `v \<in> s` using a'' by auto
+ have lem6: "a \<in> s' \<or> a' \<in> s'"
+ proof (cases "\<forall>x\<in>s'. kle n x u \<or> kle n v x")
+ case False
+ then 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' \<or> w = a"
+ using uxv[of w] uvs' w by auto
+ thus ?thesis using w by auto
+ next
+ case True
+ have "\<not> (\<forall>x\<in>s'. kle n x u)"
+ unfolding ball_simps
+ apply (rule_tac x=v in bexI)
+ using uv `u \<noteq> v`
+ unfolding kle_antisym [of n u v,symmetric]
+ using `v\<in>s'`
+ apply auto
+ done
+ hence "\<exists>y\<in>s'. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then u j + 1 else u j)"
+ using ksimplex_successor[OF as `u\<in>s'`] by blast
+ then guess w .. note w = this
+ from this(2) guess kk .. note kk = this[rule_format]
+ have "\<not> 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 \<noteq> 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 \<noteq> l`
+ apply auto
+ done
+ next
+ case False
+ hence "kk \<noteq> k" using `k \<noteq> l` by auto
+ thus False using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)]
+ apply (erule_tac x=k in allE)
+ using `k \<noteq> l`
+ apply auto
+ done
+ qed
+ thus ?thesis by auto
+ qed
thus "s' \<in> {s, insert a' (s - {a})}" proof(cases "a\<in>s'")
- case True hence "s' = s" apply-apply(rule lem1[OF a''(2)]) using a'' `a\<in>s` by auto
- thus ?thesis by auto next case False hence "a'\<in>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'\<notin>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 \<in> s`
+ apply auto
+ done
+ thus ?thesis by auto
+ next
+ case False hence "a'\<in>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'\<notin>s` by auto
+ thus ?thesis by auto
+ qed
+ qed
+ ultimately have *: "?A = {s, insert a' (s - {a})}" by blast
have "s \<noteq> insert a' (s - {a})" using `a'\<notin>s` by auto
- 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 "\<forall>s. ksimplex p (n + 1) s \<longrightarrow> (rl ` s \<subseteq>{0..n+1})"
- "odd (card{f. \<exists>s a. ksimplex p (n + 1) s \<and> a \<in> s \<and> (f = s - {a}) \<and>
- (rl ` f = {0 .. n}) \<and> ((\<exists>j\<in>{1..n+1}.\<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n+1}.\<forall>x\<in>f. x j = p))})"
- shows "odd(card {s\<in>{s. ksimplex p (n + 1) s}. rl ` s = {0..n+1} })" proof-
- have *:"\<And>x y. x = y \<Longrightarrow> odd (card x) \<Longrightarrow> odd (card y)" by auto
- have *:"odd(card {f\<in>{f. \<exists>s\<in>{s. ksimplex p (n + 1) s}. (\<exists>a\<in>s. f = s - {a})}.
- (rl ` f = {0..n}) \<and>
- ((\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = 0) \<or>
- (\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = p))})" 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\<in>s" "f = s - {a}"
+ "odd (card{f. \<exists>s a. ksimplex p (n + 1) s \<and> a \<in> s \<and> (f = s - {a}) \<and>
+ (rl ` f = {0 .. n}) \<and> ((\<exists>j\<in>{1..n+1}.\<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n+1}.\<forall>x\<in>f. x j = p))})"
+ shows "odd(card {s\<in>{s. ksimplex p (n + 1) s}. rl ` s = {0..n+1} })"
+proof -
+ have *: "\<And>x y. x = y \<Longrightarrow> odd (card x) \<Longrightarrow> odd (card y)"
+ by auto
+ have *: "odd(card {f\<in>{f. \<exists>s\<in>{s. ksimplex p (n + 1) s}. (\<exists>a\<in>s. f = s - {a})}.
+ (rl ` f = {0..n}) \<and>
+ ((\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = 0) \<or>
+ (\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = p))})"
+ 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\<in>s" "f = s - {a}"
let ?S = "{s. ksimplex p (n + 1) s \<and> (\<exists>a\<in>s. f = s - {a})}"
- have S:"?S = {s'. ksimplex p (n + 1) s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})}" unfolding as by blast
- { fix j assume j:"j \<in> {1..n + 1}" "\<forall>x\<in>f. x j = 0" thus "card {s. ksimplex p (n + 1) s \<and> (\<exists>a\<in>s. f = s - {a})} = 1" unfolding S
- apply-apply(rule ksimplex_replace_0) apply(rule as)+ unfolding as by auto }
- { fix j assume j:"j \<in> {1..n + 1}" "\<forall>x\<in>f. x j = p" thus "card {s. ksimplex p (n + 1) s \<and> (\<exists>a\<in>s. f = s - {a})} = 1" unfolding S
- apply-apply(rule ksimplex_replace_1) apply(rule as)+ unfolding as by auto }
+ have S: "?S = {s'. ksimplex p (n + 1) s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})}"
+ unfolding as by blast
+ {
+ fix j
+ assume j: "j \<in> {1..n + 1}" "\<forall>x\<in>f. x j = 0"
+ thus "card {s. ksimplex p (n + 1) s \<and> (\<exists>a\<in>s. f = s - {a})} = 1"
+ unfolding S
+ apply -
+ apply (rule ksimplex_replace_0)
+ apply (rule as)+
+ unfolding as
+ apply auto
+ done
+ }
+ {
+ fix j
+ assume j: "j \<in> {1..n + 1}" "\<forall>x\<in>f. x j = p"
+ thus "card {s. ksimplex p (n + 1) s \<and> (\<exists>a\<in>s. f = s - {a})} = 1"
+ unfolding S
+ apply -
+ apply (rule ksimplex_replace_1)
+ apply (rule as)+
+ unfolding as
+ apply auto
+ done
+ }
show "\<not> ((\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = p)) \<Longrightarrow> card ?S = 2"
- unfolding S apply(rule ksimplex_replace_2) apply(rule as)+ unfolding as 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\<Rightarrow>nat) =
- (SOME k. k \<le> n \<and> (\<forall>i. 1\<le>i \<and> i<k+1 \<longrightarrow> label x i = 0) \<and> (k = n \<or> label x (k + 1) \<noteq> (0::nat)))"
+ (SOME k. k \<le> n \<and> (\<forall>i. 1\<le>i \<and> i<k+1 \<longrightarrow> label x i = 0) \<and>
+ (k = n \<or> label x (k + 1) \<noteq> (0::nat)))"
-lemma reduced_labelling: shows "reduced label n x \<le> n" (is ?t1) and
- "\<forall>i. 1\<le>i \<and> i < reduced label n x + 1 \<longrightarrow> (label x i = 0)" (is ?t2)
- "(reduced label n x = n) \<or> (label x (reduced label n x + 1) \<noteq> 0)" (is ?t3) proof-
- have num_WOP:"\<And>P k. P (k::nat) \<Longrightarrow> \<exists>n. P n \<and> (\<forall>m<n. \<not> P m)"
- apply(drule ex_has_least_nat[where m="\<lambda>x. x"]) apply(erule exE,rule_tac x=x in exI) by auto
- have *:"n \<le> n \<and> (label x (n + 1) \<noteq> 0 \<or> n = n)" by auto
- then guess N apply(drule_tac num_WOP[of "\<lambda>j. j\<le>n \<and> (label x (j+1) \<noteq> 0 \<or> n = j)"]) apply(erule exE) . note N=this
- have N':"N \<le> n" "\<forall>i. 1 \<le> i \<and> i < N + 1 \<longrightarrow> label x i = 0" "N = n \<or> label x (N + 1) \<noteq> 0" defer proof(rule,rule)
- fix i assume i:"1\<le>i \<and> i<N+1" thus "label x i = 0" using N[THEN conjunct2,THEN spec[where x="i - 1"]] using N by auto qed(insert N, auto)
- show ?t1 ?t2 ?t3 unfolding reduced_def apply(rule_tac[!] someI2_ex) using N' by(auto intro!: exI[where x=N]) qed
+lemma reduced_labelling:
+ shows "reduced label n x \<le> n" (is ?t1)
+ and "\<forall>i. 1\<le>i \<and> i < reduced label n x + 1 \<longrightarrow> (label x i = 0)" (is ?t2)
+ and "(reduced label n x = n) \<or> (label x (reduced label n x + 1) \<noteq> 0)" (is ?t3)
+proof -
+ have num_WOP: "\<And>P k. P (k::nat) \<Longrightarrow> \<exists>n. P n \<and> (\<forall>m<n. \<not> P m)"
+ apply (drule ex_has_least_nat[where m="\<lambda>x. x"])
+ apply (erule exE,rule_tac x=x in exI)
+ apply auto
+ done
+ have *: "n \<le> n \<and> (label x (n + 1) \<noteq> 0 \<or> n = n)" by auto
+ then guess N
+ apply (drule_tac num_WOP[of "\<lambda>j. j\<le>n \<and> (label x (j+1) \<noteq> 0 \<or> n = j)"])
+ apply (erule exE)
+ done
+ note N = this
+ have N': "N \<le> n"
+ "\<forall>i. 1 \<le> i \<and> i < N + 1 \<longrightarrow> label x i = 0" "N = n \<or> label x (N + 1) \<noteq> 0"
+ defer
+ proof (rule, rule)
+ fix i
+ assume i: "1\<le>i \<and> i<N+1"
+ thus "label x i = 0"
+ using N[THEN conjunct2,THEN spec[where x="i - 1"]]
+ using N by auto
+ qed (insert N, auto)
+ show ?t1 ?t2 ?t3
+ unfolding reduced_def
+ apply (rule_tac[!] someI2_ex)
+ using N'
+ apply (auto intro!: exI[where x=N])
+ done
+qed
-lemma reduced_labelling_unique: fixes x::"nat \<Rightarrow> nat"
- assumes "r \<le> n" "\<forall>i. 1 \<le> i \<and> i < r + 1 \<longrightarrow> (label x i = 0)" "(r = n) \<or> (label x (r + 1) \<noteq> 0)"
- 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 \<Rightarrow> nat"
+ assumes "r \<le> n"
+ "\<forall>i. 1 \<le> i \<and> i < r + 1 \<longrightarrow> (label x i = 0)" "(r = n) \<or> (label x (r + 1) \<noteq> 0)"
+ 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\<in>{1..n}" "label x j = 0" shows "reduced label n x \<noteq> j - 1"
- using reduced_labelling[of label n x] using assms by fastforce
+lemma reduced_labelling_zero:
+ assumes "j\<in>{1..n}" "label x j = 0"
+ shows "reduced label n x \<noteq> j - 1"
+ using reduced_labelling[of label n x]
+ using assms by fastforce
-lemma reduced_labelling_nonzero: assumes "j\<in>{1..n}" "label x j \<noteq> 0" shows "reduced label n x < j"
- using assms and reduced_labelling[of label n x] apply(erule_tac x=j in allE) by auto
+lemma reduced_labelling_nonzero:
+ assumes "j\<in>{1..n}" "label x j \<noteq> 0"
+ shows "reduced label n x < j"
+ using assms and reduced_labelling[of label n x]
+ apply (erule_tac x=j in allE)
+ apply auto
+ done
lemma reduced_labelling_Suc:
- assumes "reduced lab (n + 1) x \<noteq> n + 1" shows "reduced lab (n + 1) x = reduced lab n x"
- apply(subst eq_commute) apply(rule reduced_labelling_unique)
- using reduced_labelling[of lab "n+1" x] and assms by auto
+ assumes "reduced lab (n + 1) x \<noteq> n + 1"
+ shows "reduced lab (n + 1) x = reduced lab n x"
+ apply (subst eq_commute)
+ apply (rule reduced_labelling_unique)
+ using reduced_labelling[of lab "n+1" x] and assms
+ apply auto
+ done
lemma complete_face_top:
assumes "\<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"
shows "((reduced lab (n + 1)) ` f = {0..n}) \<and> ((\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = p)) \<longleftrightarrow>
- ((reduced lab (n + 1)) ` f = {0..n}) \<and> (\<forall>x\<in>f. x (n + 1) = p)" (is "?l = ?r") proof
- assume ?l (is "?as \<and> (?a \<or> ?b)") thus ?r apply-apply(rule,erule conjE,assumption) proof(cases ?a)
- case True then guess j .. note j=this {fix x assume x:"x\<in>f"
- have "reduced lab (n+1) x \<noteq> j - 1" using j apply-apply(rule reduced_labelling_zero) defer apply(rule assms(1)[rule_format]) using x by auto }
+ ((reduced lab (n + 1)) ` f = {0..n}) \<and> (\<forall>x\<in>f. x (n + 1) = p)" (is "?l = ?r")
+proof
+ assume ?l (is "?as \<and> (?a \<or> ?b)")
+ thus ?r
+ apply -
+ apply (rule, erule conjE, assumption)
+ proof (cases ?a)
+ case True
+ then guess j .. note j = this
+ {
+ fix x
+ assume x: "x \<in> f"
+ have "reduced lab (n + 1) x \<noteq> j - 1"
+ using j
+ apply -
+ apply (rule reduced_labelling_zero)
+ defer
+ apply (rule assms(1)[rule_format])
+ using x
+ apply auto
+ done
+ }
moreover have "j - 1 \<in> {0..n}" using j by auto
then guess y unfolding `?l`[THEN conjunct1,symmetric] and image_iff .. note y = this
- ultimately have False by auto thus "\<forall>x\<in>f. x (n + 1) = p" by auto next
+ ultimately have False by auto
+ thus "\<forall>x\<in>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 \<in> f"
+ have "reduced lab (n + 1) x < j"
+ using j
+ apply -
+ apply (rule reduced_labelling_nonzero)
+ using assms(2)[rule_format,of x j] and x
+ apply auto
+ done
+ } note * = this
+ have "j = n + 1"
+ proof (rule ccontr)
+ case goal1
+ hence "j < n + 1" using j by auto
+ moreover
+ have "n \<in> {0..n}" by auto
+ then guess y unfolding `?l`[THEN conjunct1,symmetric] image_iff ..
+ ultimately show False using *[of y] by auto
+ qed
+ thus "\<forall>x\<in>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\<in>f"
- have "reduced lab (n+1) x < j" using j apply-apply(rule reduced_labelling_nonzero) using assms(2)[rule_format,of x j] and x by auto } note * = this
- have "j = n + 1" proof(rule ccontr) case goal1 hence "j < n + 1" using j by auto moreover
- have "n \<in> {0..n}" by auto then guess y unfolding `?l`[THEN conjunct1,symmetric] image_iff ..
- ultimately show False using *[of y] by auto qed
- thus "\<forall>x\<in>f. x (n + 1) = p" using j by auto qed qed(auto)
subsection {* Hence we get just about the nice induction. *}