--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Sep 17 21:20:55 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Wed Sep 18 00:11:15 2013 +0200
@@ -43,11 +43,12 @@
fixes f :: "'a::metric_space \<Rightarrow> 'b::euclidean_space"
assumes "compact s"
and "continuous_on s f"
- and "\<not> (\<exists>x\<in>s. (f x = 0))"
+ and "\<not> (\<exists>x\<in>s. f x = 0)"
obtains d where "0 < d" and "\<forall>x\<in>s. d \<le> norm (f x)"
proof (cases "s = {}")
case True
- show thesis by (rule that [of 1]) (auto simp: True)
+ show thesis
+ by (rule that [of 1]) (auto simp: True)
next
case False
have "continuous_on s (norm \<circ> f)"
@@ -89,14 +90,14 @@
(P x \<and> Q xa \<and> y = 0 \<longrightarrow> x \<bullet> xa \<le> f x \<bullet> xa) \<and>
(P x \<and> Q xa \<and> y = 1 \<longrightarrow> f x \<bullet> xa \<le> x \<bullet> xa)"
{
- assume "P x" "Q xa" "xa\<in>Basis"
+ assume "P x" "Q xa" "xa \<in> Basis"
then have "0 \<le> f x \<bullet> xa \<and> f x \<bullet> xa \<le> 1"
using assms(2)[rule_format,of "f x" xa]
apply (drule_tac assms(1)[rule_format])
apply auto
done
}
- then have "xa\<in>Basis \<Longrightarrow> ?R 0 \<or> ?R 1" by auto
+ then have "xa \<in> Basis \<Longrightarrow> ?R 0 \<or> ?R 1" by auto
then show ?case by auto
qed
qed
@@ -105,32 +106,34 @@
subsection {* The key "counting" observation, somewhat abstracted. *}
lemma setsum_Un_disjoint':
- assumes "finite A" "finite B" "A \<inter> B = {}" "A \<union> B = C"
+ assumes "finite A"
+ and "finite B"
+ and "A \<inter> B = {}"
+ and "A \<union> B = C"
shows "setsum g C = setsum g A + setsum g B"
using setsum_Un_disjoint[OF assms(1-3)] and assms(4) by auto
lemma kuhn_counting_lemma:
- assumes
- "finite faces"
- "finite simplices"
- "\<forall>f\<in>faces. bnd f \<longrightarrow> (card {s \<in> simplices. face f s} = 1)"
- "\<forall>f\<in>faces. \<not> bnd f \<longrightarrow> (card {s \<in> simplices. face f s} = 2)"
- "\<forall>s\<in>simplices. compo s \<longrightarrow> (card {f \<in> faces. face f s \<and> compo' f} = 1)"
- "\<forall>s\<in>simplices. \<not> compo s \<longrightarrow>
+ assumes "finite faces"
+ and "finite simplices"
+ and "\<forall>f\<in>faces. bnd f \<longrightarrow> (card {s \<in> simplices. face f s} = 1)"
+ and "\<forall>f\<in>faces. \<not> bnd f \<longrightarrow> (card {s \<in> simplices. face f s} = 2)"
+ and "\<forall>s\<in>simplices. compo s \<longrightarrow> (card {f \<in> faces. face f s \<and> compo' f} = 1)"
+ and "\<forall>s\<in>simplices. \<not> compo s \<longrightarrow>
(card {f \<in> faces. face f s \<and> compo' f} = 0) \<or> (card {f \<in> faces. face f s \<and> compo' f} = 2)"
- "odd(card {f \<in> faces. compo' f \<and> bnd f})"
+ and "odd(card {f \<in> faces. compo' f \<and> bnd f})"
shows "odd(card {s \<in> simplices. compo s})"
proof -
have "\<And>x. {f\<in>faces. compo' f \<and> bnd f \<and> face f x} \<union> {f\<in>faces. compo' f \<and> \<not>bnd f \<and> face f x} =
{f\<in>faces. compo' f \<and> face f x}"
"\<And>x. {f \<in> faces. compo' f \<and> bnd f \<and> face f x} \<inter> {f \<in> faces. compo' f \<and> \<not> bnd f \<and> face f x} = {}"
by auto
- then have lem1:"setsum (\<lambda>s. (card {f \<in> faces. face f s \<and> compo' f})) simplices =
+ then have lem1: "setsum (\<lambda>s. (card {f \<in> faces. face f s \<and> compo' f})) simplices =
setsum (\<lambda>s. card {f \<in> {f \<in> faces. compo' f \<and> bnd f}. face f s}) simplices +
setsum (\<lambda>s. card {f \<in> {f \<in> faces. compo' f \<and> \<not> (bnd f)}. face f s}) simplices"
unfolding setsum_addf[symmetric]
apply -
- apply(rule setsum_cong2)
+ apply (rule setsum_cong2)
using assms(1)
apply (auto simp add: card_Un_Int, auto simp add:conj_commute)
done
@@ -139,7 +142,7 @@
1 * card {f \<in> faces. compo' f \<and> bnd f}"
"setsum (\<lambda>j. card {f \<in> {f \<in> faces. compo' f \<and> \<not> bnd f}. face f j}) simplices =
2 * card {f \<in> faces. compo' f \<and> \<not> bnd f}"
- apply(rule_tac[!] setsum_multicount)
+ apply (rule_tac[!] setsum_multicount)
using assms
apply auto
done
@@ -207,10 +210,11 @@
unfolding * using card_insert by auto
qed auto
-lemma card_2_exists: "card s = 2 \<longleftrightarrow> (\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. (z = x) \<or> (z = y)))"
+lemma card_2_exists: "card s = 2 \<longleftrightarrow> (\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y))"
proof
assume "card s = 2"
- then obtain x y where s: "s = {x, y}" "x\<noteq>y" unfolding numeral_2_eq_2
+ 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
@@ -219,10 +223,12 @@
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"
+ 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
+ then have "s = {x, y}"
+ by auto
+ with `x \<noteq> y` show "card s = 2"
+ by auto
qed
lemma image_lemma_0:
@@ -244,19 +250,26 @@
qed
lemma image_lemma_1:
- assumes "finite s" "finite t" "card s = card t" "f ` s = t" "b \<in> t"
+ assumes "finite s"
+ and "finite t"
+ and "card s = card t"
+ and "f ` s = t"
+ and "b \<in> t"
shows "card {s'. \<exists>a\<in>s. s' = s - {a} \<and> f ` s' = t - {b}} = 1"
proof -
- obtain a where a: "b = f a" "a\<in>s" using assms(4-5) by auto
+ obtain a where a: "b = f a" "a \<in> s"
+ using assms(4-5) by auto
have inj: "inj_on f s"
apply (rule eq_card_imp_inj_on)
- using assms(1-4) apply auto
+ using assms(1-4)
+ apply auto
done
have *: "{a \<in> s. f ` (s - {a}) = t - {b}} = {a}"
apply (rule set_eqI)
unfolding singleton_iff
apply (rule, rule inj[unfolded inj_on_def, rule_format])
- unfolding a using a(2) and assms and inj[unfolded inj_on_def]
+ unfolding a
+ using a(2) and assms and inj[unfolded inj_on_def]
apply auto
done
show ?thesis
@@ -268,8 +281,8 @@
lemma image_lemma_2:
assumes "finite s" "finite t" "card s = card t" "f ` s \<subseteq> t" "f ` s \<noteq> t" "b \<in> t"
- shows "(card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> f ` s' = t - {b}} = 0) \<or>
- (card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> f ` s' = t - {b}} = 2)"
+ shows "card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> f ` s' = t - {b}} = 0 \<or>
+ card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> f ` s' = t - {b}} = 2"
proof (cases "{a\<in>s. f ` (s - {a}) = t - {b}} = {}")
case True
then show ?thesis
@@ -281,36 +294,55 @@
next
let ?M = "{a\<in>s. f ` (s - {a}) = t - {b}}"
case False
- then obtain a where "a\<in>?M" by auto
- then have a: "a\<in>s" "f ` (s - {a}) = t - {b}" by auto
- have "f a \<in> t - {b}" using a and assms by auto
+ then 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
+ 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)
+ apply (rule set_eqI)
+ apply rule
proof -
fix x
assume "x \<in> f ` (s - {a})"
- then obtain y where y: "f y = x" "y\<in>s- {a}" by auto
+ then obtain y where y: "f y = x" "y \<in> s - {a}"
+ by auto
then show "x \<in> f ` (s - {c})"
unfolding image_iff
apply (rule_tac x = "if y = c then a else y" in bexI)
- using c a apply auto done
+ using c a
+ apply auto
+ done
qed auto
- have "c\<in>?M"
+ have "c \<in> ?M"
unfolding mem_Collect_eq and *
- using a and c(1) by auto
+ 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`)
- proof (rule, unfold mem_Collect_eq, erule conjE)
+ apply (rule disjI2)
+ apply (rule image_lemma_0)
+ unfolding card_2_exists
+ apply (rule bexI[OF _ `a\<in>?M`])
+ apply (rule bexI[OF _ `c\<in>?M`])
+ apply rule
+ apply (rule `a \<noteq> c`)
+ apply rule
+ apply (unfold mem_Collect_eq)
+ apply (erule conjE)
+ proof -
fix z
assume as: "z \<in> s" "f ` (s - {z}) = t - {b}"
have inj: "inj_on f (s - {z})"
apply (rule eq_card_imp_inj_on)
- unfolding as using as(1) and assms
+ unfolding as
+ using as(1) and assms
apply auto
done
show "z = a \<or> z = c"
@@ -318,7 +350,7 @@
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`
+ using `a \<in> s` `c \<in> s` `f a = f c` `a \<noteq> c`
apply auto
done
qed
@@ -330,18 +362,20 @@
lemma kuhn_complete_lemma:
assumes "finite simplices"
- "\<forall>f s. face f s \<longleftrightarrow> (\<exists>a\<in>s. f = s - {a})"
- "\<forall>s\<in>simplices. card s = n + 2" "\<forall>s\<in>simplices. (rl ` s) \<subseteq> {0..n+1}"
- "\<forall>f\<in> {f. \<exists>s\<in>simplices. face f s}. bnd f \<longrightarrow> (card {s\<in>simplices. face f s} = 1)"
- "\<forall>f\<in> {f. \<exists>s\<in>simplices. face f s}. \<not>bnd f \<longrightarrow> (card {s\<in>simplices. face f s} = 2)"
- "odd(card {f\<in>{f. \<exists>s\<in>simplices. face f s}. rl ` f = {0..n} \<and> bnd f})"
+ and "\<forall>f s. face f s \<longleftrightarrow> (\<exists>a\<in>s. f = s - {a})"
+ and "\<forall>s\<in>simplices. card s = n + 2"
+ and "\<forall>s\<in>simplices. (rl ` s) \<subseteq> {0..n+1}"
+ and "\<forall>f\<in>{f. \<exists>s\<in>simplices. face f s}. bnd f \<longrightarrow> card {s\<in>simplices. face f s} = 1"
+ and "\<forall>f\<in>{f. \<exists>s\<in>simplices. face f s}. \<not> bnd f \<longrightarrow> card {s\<in>simplices. face f s} = 2"
+ and "odd (card {f\<in>{f. \<exists>s\<in>simplices. face f s}. rl ` f = {0..n} \<and> bnd f})"
shows "odd (card {s\<in>simplices. (rl ` s = {0..n+1})})"
apply (rule kuhn_counting_lemma)
defer
apply (rule assms)+
prefer 3
apply (rule assms)
-proof (rule_tac[1-2] ballI impI)+
+ apply (rule_tac[1-2] ballI impI)+
+proof -
have *: "{f. \<exists>s\<in>simplices. \<exists>a\<in>s. f = s - {a}} = (\<Union>s\<in>simplices. {f. \<exists>a\<in>s. (f = s - {a})})"
by auto
have **: "\<forall>s\<in>simplices. card s = n + 2 \<and> finite s"
@@ -353,10 +387,13 @@
apply auto
done
have *: "\<And>P f s. s\<in>simplices \<Longrightarrow> (f \<in> {f. \<exists>s\<in>simplices. \<exists>a\<in>s. f = s - {a}}) \<and>
- (\<exists>a\<in>s. (f = s - {a})) \<and> P f \<longleftrightarrow> (\<exists>a\<in>s. (f = s - {a}) \<and> P f)" by auto
- fix s assume s: "s\<in>simplices"
+ (\<exists>a\<in>s. (f = s - {a})) \<and> P f \<longleftrightarrow> (\<exists>a\<in>s. (f = s - {a}) \<and> P f)"
+ by auto
+ fix s
+ assume s: "s \<in> simplices"
let ?S = "{f \<in> {f. \<exists>s\<in>simplices. face f s}. face f s \<and> rl ` f = {0..n}}"
- have "{0..n + 1} - {n + 1} = {0..n}" by auto
+ have "{0..n + 1} - {n + 1} = {0..n}"
+ by auto
then have S: "?S = {s'. \<exists>a\<in>s. s' = s - {a} \<and> rl ` s' = {0..n + 1} - {n + 1}}"
apply -
apply (rule set_eqI)
@@ -364,9 +401,9 @@
unfolding *[OF s, unfolded mem_Collect_eq, where P="\<lambda>x. rl ` x = {0..n}"]
apply auto
done
- show "rl ` s = {0..n+1} \<Longrightarrow> card ?S = 1" "rl ` s \<noteq> {0..n+1} \<Longrightarrow> card ?S = 0 \<or> card ?S = 2"
+ show "rl ` s = {0..n+1} \<Longrightarrow> card ?S = 1" and "rl ` s \<noteq> {0..n+1} \<Longrightarrow> card ?S = 0 \<or> card ?S = 2"
unfolding S
- apply(rule_tac[!] image_lemma_1 image_lemma_2)
+ apply (rule_tac[!] image_lemma_1 image_lemma_2)
using ** assms(4) and s
apply auto
done
@@ -375,12 +412,12 @@
subsection {*We use the following notion of ordering rather than pointwise indexing. *}
-definition "kle n x y \<longleftrightarrow> (\<exists>k\<subseteq>{1..n::nat}. (\<forall>j. y(j) = x(j) + (if j \<in> k then (1::nat) else 0)))"
+definition "kle n x y \<longleftrightarrow> (\<exists>k\<subseteq>{1..n::nat}. \<forall>j. y j = x j + (if j \<in> k then (1::nat) else 0))"
lemma kle_refl [intro]: "kle n x x"
unfolding kle_def by auto
-lemma kle_antisym: "kle n x y \<and> kle n y x \<longleftrightarrow> (x = y)"
+lemma kle_antisym: "kle n x y \<and> kle n y x \<longleftrightarrow> x = y"
unfolding kle_def
apply rule
apply auto
@@ -388,12 +425,17 @@
lemma pointwise_minimal_pointwise_maximal:
fixes s :: "(nat \<Rightarrow> nat) set"
- assumes "finite s" "s \<noteq> {}" "\<forall>x\<in>s. \<forall>y\<in>s. (\<forall>j. x j \<le> y j) \<or> (\<forall>j. y j \<le> x j)"
- shows "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. a j \<le> x j" "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. x j \<le> a j"
- using assms unfolding atomize_conj
+ assumes "finite s"
+ and "s \<noteq> {}"
+ and "\<forall>x\<in>s. \<forall>y\<in>s. (\<forall>j. x j \<le> y j) \<or> (\<forall>j. y j \<le> x j)"
+ shows "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. a j \<le> x j"
+ and "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. x j \<le> a j"
+ using assms
+ unfolding atomize_conj
proof (induct s rule: finite_induct)
- fix x and F::"(nat\<Rightarrow>nat) set"
- assume as:"finite F" "x \<notin> F"
+ fix x
+ fix F :: "(nat \<Rightarrow> nat) set"
+ assume as: "finite F" "x \<notin> F"
"\<lbrakk>F \<noteq> {}; \<forall>x\<in>F. \<forall>y\<in>F. (\<forall>j. x j \<le> y j) \<or> (\<forall>j. y j \<le> x j)\<rbrakk>
\<Longrightarrow> (\<exists>a\<in>F. \<forall>x\<in>F. \<forall>j. a j \<le> x j) \<and> (\<exists>a\<in>F. \<forall>x\<in>F. \<forall>j. x j \<le> a j)" "insert x F \<noteq> {}"
"\<forall>xa\<in>insert x F. \<forall>y\<in>insert x F. (\<forall>j. xa j \<le> y j) \<or> (\<forall>j. y j \<le> xa j)"
@@ -417,7 +459,8 @@
assume "\<forall>j. a j \<le> x j"
then show ?thesis
apply (rule_tac x=a in bexI)
- using a apply auto
+ using a
+ apply auto
done
next
assume "\<forall>j. x j \<le> a j"
@@ -456,24 +499,28 @@
qed auto
-lemma kle_imp_pointwise: "kle n x y \<Longrightarrow> (\<forall>j. x j \<le> y j)"
+lemma kle_imp_pointwise: "kle n x y \<Longrightarrow> \<forall>j. x j \<le> y j"
unfolding kle_def by auto
lemma pointwise_antisym:
fixes x :: "nat \<Rightarrow> nat"
shows "(\<forall>j. x j \<le> y j) \<and> (\<forall>j. y j \<le> x j) \<longleftrightarrow> x = y"
- apply (rule, rule ext, erule conjE)
+ apply rule
+ apply (rule ext)
+ apply (erule conjE)
apply (erule_tac x = xa in allE)+
apply auto
done
lemma kle_trans:
- assumes "kle n x y" "kle n y z" "kle n x z \<or> kle n z x"
+ assumes "kle n x y"
+ and "kle n y z"
+ and "kle n x z \<or> kle n z x"
shows "kle n x z"
using assms
- apply -
- apply (erule disjE)
- apply assumption
+ apply -
+ apply (erule disjE)
+ apply assumption
proof -
case goal1
then have "x = z"
@@ -487,20 +534,24 @@
qed
lemma kle_strict:
- assumes "kle n x y" "x \<noteq> y"
- shows "\<forall>j. x j \<le> y j" "\<exists>k. 1 \<le> k \<and> k \<le> n \<and> x(k) < y(k)"
+ assumes "kle n x y"
+ and "x \<noteq> y"
+ shows "\<forall>j. x j \<le> y j"
+ and "\<exists>k. 1 \<le> k \<and> k \<le> n \<and> x k < y k"
apply (rule kle_imp_pointwise[OF assms(1)])
proof -
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)"
+ show "\<exists>k. 1 \<le> k \<and> k \<le> n \<and> x k < y k"
proof (cases "k = {}")
case True
then have "x = y"
apply -
apply (rule ext)
- using k apply auto
+ using k
+ apply auto
done
- then show ?thesis using assms(2) by auto
+ then show ?thesis
+ using assms(2) by auto
next
case False
then have "(SOME k'. k' \<in> k) \<in> k"
@@ -510,19 +561,24 @@
done
then show ?thesis
apply (rule_tac x = "SOME k'. k' \<in> k" in exI)
- using k apply auto
+ using k
+ apply auto
done
qed
qed
lemma kle_minimal:
- assumes "finite s" "s \<noteq> {}" "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"
+ assumes "finite s"
+ and "s \<noteq> {}"
+ and "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"
shows "\<exists>a\<in>s. \<forall>x\<in>s. kle n a x"
proof -
have "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. a j \<le> x j"
apply (rule pointwise_minimal_pointwise_maximal(1)[OF assms(1-2)])
- apply (rule, rule)
- apply (drule_tac assms(3)[rule_format], assumption)
+ apply rule
+ apply rule
+ apply (drule_tac assms(3)[rule_format])
+ apply assumption
using kle_imp_pointwise
apply auto
done
@@ -550,14 +606,18 @@
qed
lemma kle_maximal:
- assumes "finite s" "s \<noteq> {}" "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"
+ assumes "finite s"
+ and "s \<noteq> {}"
+ and "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"
shows "\<exists>a\<in>s. \<forall>x\<in>s. kle n x a"
proof -
have "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. a j \<ge> x j"
apply (rule pointwise_minimal_pointwise_maximal(2)[OF assms(1-2)])
- apply (rule, rule)
+ apply rule
+ apply rule
apply (drule_tac assms(3)[rule_format],assumption)
- using kle_imp_pointwise apply auto
+ using kle_imp_pointwise
+ apply auto
done
then guess a .. note a = this
show ?thesis
@@ -574,15 +634,18 @@
apply -
unfolding pointwise_antisym[symmetric]
apply (drule kle_imp_pointwise)
- using a(2)[rule_format,OF `x\<in>s`] apply auto
+ using a(2)[rule_format,OF `x\<in>s`]
+ apply auto
done
- then show ?thesis using kle_refl by auto
+ then show ?thesis
+ using kle_refl by auto
qed
qed (insert a, auto)
qed
lemma kle_strict_set:
- assumes "kle n x y" "x \<noteq> y"
+ assumes "kle n x y"
+ and "x \<noteq> y"
shows "1 \<le> card {k\<in>{1..n}. x k < y k}"
proof -
guess i using kle_strict(2)[OF assms] ..
@@ -591,15 +654,19 @@
apply (rule card_mono)
apply auto
done
- then show ?thesis by auto
+ then show ?thesis
+ by auto
qed
lemma kle_range_combine:
- assumes "kle n x y" "kle n y z" "kle n x z \<or> kle n z x"
- "m1 \<le> card {k\<in>{1..n}. x k < y k}"
- "m2 \<le> card {k\<in>{1..n}. y k < z k}"
+ assumes "kle n x y"
+ and "kle n y z"
+ and "kle n x z \<or> kle n z x"
+ and "m1 \<le> card {k\<in>{1..n}. x k < y k}"
+ and "m2 \<le> card {k\<in>{1..n}. y k < z k}"
shows "kle n x z \<and> m1 + m2 \<le> card {k\<in>{1..n}. x k < z k}"
- apply (rule, rule kle_trans[OF assms(1-3)])
+ apply rule
+ apply (rule kle_trans[OF assms(1-3)])
proof -
have "\<And>j. x j < y j \<Longrightarrow> x j < z j"
apply (rule less_le_trans)
@@ -617,37 +684,55 @@
by auto
have **: "{k \<in> {1..n}. x k < y k} \<inter> {k \<in> {1..n}. y k < z k} = {}"
unfolding disjoint_iff_not_equal
- apply (rule, rule, unfold mem_Collect_eq, rule ccontr)
+ apply rule
+ apply rule
+ apply (unfold mem_Collect_eq)
+ apply (rule notI)
apply (erule conjE)+
proof -
fix i j
- assume as: "i \<in> {1..n}" "x i < y i" "j \<in> {1..n}" "y j < z j" "\<not> i \<noteq> j"
+ assume as: "i \<in> {1..n}" "x i < y i" "j \<in> {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
- then have "i \<in> kx" using as(1) kx
- apply (rule_tac ccontr)
+ have "x i < y i"
+ using as by auto
+ then have "i \<in> kx"
+ using as(1) kx
+ apply -
+ apply (rule ccontr)
apply auto
done
- then have "x i + 1 = y i" using kx by auto
+ 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
- then have "i \<in> ky" using as(1) ky
- apply (rule_tac ccontr)
+ have "y i < z i"
+ using as by auto
+ then have "i \<in> ky"
+ using as(1) ky
+ apply -
+ apply (rule ccontr)
apply auto
done
- then have "y i + 1 = z i" using ky by auto
+ then have "y i + 1 = z i"
+ using ky by auto
ultimately
- have "z i = x i + 2" by auto
- then show False using assms(3) unfolding kle_def
+ have "z i = x i + 2"
+ by auto
+ then show False
+ using assms(3)
+ unfolding kle_def
by (auto simp add: split_if_eq1)
qed
- have fin: "\<And>P. finite {x\<in>{1..n::nat}. P x}" by auto
+ have fin: "\<And>P. finite {x\<in>{1..n::nat}. P x}"
+ by auto
have "m1 + m2 \<le> card {k\<in>{1..n}. x k < y k} + card {k\<in>{1..n}. y k < z k}"
using assms(4-5) by auto
also have "\<dots> \<le> card {k\<in>{1..n}. x k < z k}"
- unfolding card_Un_Int[OF fin fin] unfolding * ** by auto
- finally show " m1 + m2 \<le> card {k \<in> {1..n}. x k < z k}" by auto
+ unfolding card_Un_Int[OF fin fin]
+ unfolding * **
+ by auto
+ finally show "m1 + m2 \<le> card {k \<in> {1..n}. x k < z k}"
+ by auto
qed
lemma kle_range_combine_l:
@@ -670,12 +755,15 @@
and "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"
shows "\<exists>x\<in>s. \<exists>y\<in>s. kle n x y \<and> m \<le> card {k\<in>{1..n}. x k < y k}"
proof -
- have "finite s" "s\<noteq>{}" using assms(1)
+ have "finite s" and "s \<noteq> {}"
+ using assms(1)
by (auto intro: card_ge_0_finite)
- then show ?thesis using assms
+ then show ?thesis
+ using assms
proof (induct m arbitrary: s)
case 0
- then show ?case using kle_refl by auto
+ then show ?case
+ using kle_refl by auto
next
case (Suc m)
then obtain a where a: "a \<in> s" "\<forall>x\<in>s. kle n a x"
@@ -683,29 +771,40 @@
show ?case
proof (cases "s \<subseteq> {a}")
case False
- then have "card (s - {a}) = Suc m" "s - {a} \<noteq> {}"
- using card_Diff_singleton[OF _ a(1)] Suc(4) `finite s` by auto
- then obtain x b where xb:"x\<in>s - {a}" "b\<in>s - {a}"
- "kle n x b" "m \<le> card {k \<in> {1..n}. x k < b k}"
- using Suc(1)[of "s - {a}"] using Suc(5) `finite s` by auto
- have "1 \<le> card {k \<in> {1..n}. a k < x k}" "m \<le> card {k \<in> {1..n}. x k < b k}"
+ then have "card (s - {a}) = Suc m" and "s - {a} \<noteq> {}"
+ using card_Diff_singleton[OF _ a(1)] Suc(4) `finite s`
+ by auto
+ then obtain x b where xb:
+ "x \<in> s - {a}"
+ "b \<in> s - {a}"
+ "kle n x b"
+ "m \<le> card {k \<in> {1..n}. x k < b k}"
+ using Suc(1)[of "s - {a}"]
+ using Suc(5) `finite s`
+ by auto
+ have "1 \<le> card {k \<in> {1..n}. a k < x k}" and "m \<le> card {k \<in> {1..n}. x k < b k}"
apply (rule kle_strict_set)
apply (rule a(2)[rule_format])
using a and xb
apply auto
done
then show ?thesis
- apply (rule_tac x=a in bexI, rule_tac x=b in bexI)
+ apply (rule_tac x=a in bexI)
+ apply (rule_tac x=b in bexI)
using kle_range_combine[OF a(2)[rule_format] xb(3) Suc(5)[rule_format], of 1 "m"]
using a(1) xb(1-2)
apply auto
done
next
case True
- then have "s = {a}" using Suc(3) by auto
- then have "card s = 1" by auto
- then have False using Suc(4) `finite s` by auto
- then show ?thesis by auto
+ 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
@@ -719,11 +818,14 @@
lemma kle_trans_1:
assumes "kle n x y"
- shows "x j \<le> y j" "y j \<le> x j + 1"
+ shows "x j \<le> y j"
+ and "y j \<le> x j + 1"
using assms[unfolded kle_def] by auto
lemma kle_trans_2:
- assumes "kle n a b" "kle n b c" "\<forall>j. c j \<le> a j + 1"
+ assumes "kle n a b"
+ and "kle n b c"
+ and "\<forall>j. c j \<le> a j + 1"
shows "kle n a c"
proof -
guess kk1 using assms(1)[unfolded kle_def] .. note kk1 = this
@@ -747,17 +849,22 @@
ultimately show ?thesis by auto
next
case False
- then show ?thesis using kk1 kk2 by auto
+ then show ?thesis
+ using kk1 kk2 by auto
qed
qed (insert kk1 kk2, auto)
qed
lemma kle_between_r:
- assumes "kle n a b" "kle n b c" "kle n a x" "kle n c x"
+ assumes "kle n a b"
+ and "kle n b c"
+ and "kle n a x"
+ and "kle n c x"
shows "kle n b x"
apply (rule kle_trans_2[OF assms(2,4)])
proof
- have *: "\<And>c b x::nat. x \<le> c + 1 \<Longrightarrow> c \<le> b \<Longrightarrow> x \<le> b + 1" by auto
+ have *: "\<And>c b x::nat. x \<le> c + 1 \<Longrightarrow> c \<le> b \<Longrightarrow> x \<le> b + 1"
+ by auto
fix j
show "x j \<le> b j + 1"
apply (rule *)
@@ -767,7 +874,10 @@
qed
lemma kle_between_l:
- assumes "kle n a b" "kle n b c" "kle n x a" "kle n x c"
+ assumes "kle n a b"
+ and "kle n b c"
+ and "kle n x a"
+ and "kle n x c"
shows "kle n x b"
apply (rule kle_trans_2[OF assms(3,1)])
proof
@@ -782,7 +892,9 @@
qed
lemma kle_adjacent:
- assumes "\<forall>j. b j = (if j = k then a(j) + 1 else a j)" "kle n a x" "kle n x b"
+ assumes "\<forall>j. b j = (if j = k then a(j) + 1 else a j)"
+ and "kle n a x"
+ and "kle n x b"
shows "x = a \<or> x = b"
proof (cases "x k = a k")
case True
@@ -791,7 +903,8 @@
apply (rule ext)
proof -
fix j
- have "x j \<le> a j" using kle_imp_pointwise[OF assms(3),THEN spec[where x=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")
@@ -799,19 +912,24 @@
apply auto
done
then show "x j = a j"
- using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]] by auto
+ using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]]
+ by auto
qed
next
case False
- show ?thesis apply(rule disjI2,rule ext)
+ show ?thesis
+ apply (rule disjI2)
+ apply (rule ext)
proof -
fix j
have "x j \<ge> b j"
using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]]
unfolding assms(1)[rule_format]
apply -
- apply(cases "j = k")
- using False by auto
+ apply (cases "j = k")
+ using False
+ apply auto
+ done
then show "x j = b j"
using kle_imp_pointwise[OF assms(3),THEN spec[where x=j]]
by auto
@@ -819,7 +937,7 @@
qed
-subsection {* kuhn's notion of a simplex (a reformulation to avoid so much indexing). *}
+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>
@@ -837,35 +955,47 @@
lemma ksimplex_eq:
"ksimplex p n (s::(nat \<Rightarrow> nat) set) \<longleftrightarrow>
- (card s = n + 1 \<and> finite s \<and>
+ card s = n + 1 \<and>
+ finite s \<and>
(\<forall>x\<in>s. \<forall>j. x(j) \<le> p) \<and>
- (\<forall>x\<in>s. \<forall>j. j\<notin>{1..n} \<longrightarrow> (x j = p)) \<and>
- (\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x))"
+ (\<forall>x\<in>s. \<forall>j. j\<notin>{1..n} \<longrightarrow> x j = p) \<and>
+ (\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x)"
unfolding ksimplex_def by (auto intro: card_ge_0_finite)
lemma ksimplex_extrema:
assumes "ksimplex p n s"
- obtains a b where "a \<in> s" "b \<in> s"
- "\<forall>x\<in>s. kle n a x \<and> kle n x b" "\<forall>i. b(i) = (if i \<in> {1..n} then a(i) + 1 else a(i))"
+ obtains a b where "a \<in> s"
+ and "b \<in> s"
+ and "\<forall>x\<in>s. kle n a x \<and> kle n x b"
+ and "\<forall>i. b i = (if i \<in> {1..n} then a i + 1 else a i)"
proof (cases "n = 0")
case True
obtain x where *: "s = {x}"
using assms[unfolded ksimplex_eq True,THEN conjunct1]
- unfolding add_0_left card_1_exists by auto
+ unfolding add_0_left card_1_exists
+ by auto
show ?thesis
- apply (rule that[of x x]) unfolding * True
+ apply (rule that[of x x])
+ unfolding * True
apply auto
done
next
note assm = assms[unfolded ksimplex_eq]
case False
- have "s\<noteq>{}" using assm by auto
+ have "s \<noteq> {}"
+ using assm by auto
obtain a where a: "a \<in> s" "\<forall>x\<in>s. kle n a x"
- using `s\<noteq>{}` assm using kle_minimal[of s n] by auto
+ using `s \<noteq> {}` assm
+ using kle_minimal[of s n]
+ by auto
obtain b where b: "b \<in> s" "\<forall>x\<in>s. kle n x b"
- using `s\<noteq>{}` assm using kle_maximal[of s n] by auto
+ using `s \<noteq> {}` assm
+ using kle_maximal[of s n]
+ by auto
obtain c d where c_d: "c \<in> s" "d \<in> s" "kle n c d" "n \<le> card {k \<in> {1..n}. c k < d k}"
- using kle_range_induct[of s n n] using assm by auto
+ using kle_range_induct[of s n n]
+ using assm
+ by auto
have "kle n c b \<and> n \<le> card {k \<in> {1..n}. c k < b k}"
apply (rule kle_range_combine_r[where y=d])
using c_d a b
@@ -889,27 +1019,36 @@
show ?thesis
apply (rule that[OF a(1) b(1)])
defer
- apply (subst *[symmetric]) unfolding mem_Collect_eq
+ apply (subst *[symmetric])
+ unfolding mem_Collect_eq
proof
guess k using a(2)[rule_format,OF b(1),unfolded kle_def] .. note k = this
fix i
show "b i = (if i \<in> {1..n} \<and> a i < b i then a i + 1 else a i)"
proof (cases "i \<in> {1..n}")
case True
- then show ?thesis unfolding k[THEN conjunct2,rule_format] by auto
+ then show ?thesis
+ unfolding k[THEN conjunct2,rule_format] by auto
next
case False
- have "a i = p" using assm and False `a\<in>s` by auto
- moreover have "b i = p" using assm and False `b\<in>s` by auto
- ultimately show ?thesis by auto
+ have "a i = p"
+ using assm and False `a\<in>s` by auto
+ moreover have "b i = p"
+ using assm and False `b\<in>s` by auto
+ ultimately show ?thesis
+ by auto
qed
- qed(insert a(2) b(2) assm, auto)
+ qed (insert a(2) b(2) assm, auto)
qed
lemma ksimplex_extrema_strong:
- assumes "ksimplex p n s" "n \<noteq> 0"
- obtains a b where "a \<in> s" "b \<in> s" "a \<noteq> b"
- "\<forall>x\<in>s. kle n a x \<and> kle n x b" "\<forall>i. b(i) = (if i \<in> {1..n} then a(i) + 1 else a(i))"
+ assumes "ksimplex p n s"
+ and "n \<noteq> 0"
+ obtains a b where "a \<in> s"
+ and "b \<in> s"
+ and "a \<noteq> b"
+ and "\<forall>x\<in>s. kle n a x \<and> kle n x b"
+ and "\<forall>i. b i = (if i \<in> {1..n} then a(i) + 1 else a i)"
proof -
obtain a b where ab: "a \<in> s" "b \<in> s"
"\<forall>x\<in>s. kle n a x \<and> kle n x b" "\<forall>i. b(i) = (if i \<in> {1..n} then a(i) + 1 else a(i))"
@@ -919,37 +1058,44 @@
have "a \<noteq> b"
apply (rule notI)
apply (drule cong[of _ _ 1 1])
- using ab(4) assms(2) apply auto
+ using ab(4) assms(2)
+ apply auto
done
then show ?thesis
apply (rule_tac that[of a b])
- using ab apply auto
+ using ab
+ apply auto
done
qed
lemma ksimplexD:
assumes "ksimplex p n s"
- shows "card s = n + 1" "finite s" "card s = n + 1"
- "\<forall>x\<in>s. \<forall>j. x j \<le> p" "\<forall>x\<in>s. \<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p"
- "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"
+ shows "card s = n + 1"
+ and "finite s"
+ and "card s = n + 1"
+ and "\<forall>x\<in>s. \<forall>j. x j \<le> p"
+ and "\<forall>x\<in>s. \<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p"
+ and "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"
using assms unfolding ksimplex_eq by auto
lemma ksimplex_successor:
- assumes "ksimplex p n s" "a \<in> s"
- shows "(\<forall>x\<in>s. kle n x a) \<or> (\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. y(j) = (if j = k then a(j) + 1 else a(j)))"
+ assumes "ksimplex p n s"
+ and "a \<in> s"
+ shows "(\<forall>x\<in>s. kle n x a) \<or> (\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then a j + 1 else a j))"
proof (cases "\<forall>x\<in>s. kle n x a")
case True
then show ?thesis by auto
next
note assm = ksimplexD[OF assms(1)]
case False
- then obtain b where b: "b\<in>s" "\<not> kle n b a" "\<forall>x\<in>{x \<in> s. \<not> kle n x a}. kle n b x"
- using kle_minimal[of "{x\<in>s. \<not> kle n x a}" n] and assm by auto
+ then obtain b where b: "b \<in> s" "\<not> kle n b a" "\<forall>x\<in>{x \<in> s. \<not> kle n x a}. kle n b x"
+ using kle_minimal[of "{x\<in>s. \<not> kle n x a}" n] and assm
+ by auto
then have **: "1 \<le> card {k\<in>{1..n}. a k < b k}"
apply -
apply (rule kle_strict_set)
using assm(6) and `a\<in>s`
- apply (auto simp add:kle_refl)
+ apply (auto simp add: kle_refl)
done
let ?kle1 = "{x \<in> s. \<not> kle n x a}"
@@ -974,11 +1120,13 @@
using assm(2) by auto
obtain e f where e_f: "e \<in> s" "kle n e a" "f \<in> s" "kle n f a"
"kle n e f" "card ?kle2 - 1 \<le> card {k \<in> {1..n}. e k < f k}"
- using kle_range_induct[OF sizekle2, of n] using assm by auto
+ using kle_range_induct[OF sizekle2, of n]
+ using assm
+ by auto
have "card {k\<in>{1..n}. a k < b k} = 1"
proof (rule ccontr)
- case goal1
+ assume "\<not> ?thesis"
then have as: "card {k\<in>{1..n}. a k < b k} \<ge> 2"
using ** by auto
have *: "finite ?kle2" "finite ?kle1" "?kle2 \<union> ?kle1 = s" "?kle2 \<inter> ?kle1 = {}"
@@ -986,12 +1134,14 @@
have "(card ?kle2 - 1) + 2 + (card ?kle1 - 1) = card ?kle2 + card ?kle1"
using sizekle1 sizekle2 by auto
also have "\<dots> = n + 1"
- unfolding card_Un_Int[OF *(1-2)] *(3-) using assm(3) by auto
+ unfolding card_Un_Int[OF *(1-2)] *(3-)
+ using assm(3)
+ by auto
finally have n: "(card ?kle2 - 1) + (2 + (card ?kle1 - 1)) = n + 1"
by auto
have "kle n e a \<and> card {x \<in> s. kle n x a} - 1 \<le> card {k \<in> {1..n}. e k < a k}"
apply (rule kle_range_combine_r[where y=f])
- using e_f using `a\<in>s` assm(6)
+ using e_f using `a \<in> s` assm(6)
apply auto
done
moreover have "kle n b d \<and> card {x \<in> s. \<not> kle n x a} - 1 \<le> card {k \<in> {1..n}. b k < d k}"
@@ -1001,28 +1151,31 @@
done
then have "kle n a d \<and> 2 + (card {x \<in> s. \<not> kle n x a} - 1) \<le> card {k \<in> {1..n}. a k < d k}"
apply -
- apply (rule kle_range_combine[where y=b]) using as and b assm(6) `a\<in>s` `d\<in>s`
+ apply (rule kle_range_combine[where y=b]) using as and b assm(6) `a \<in> s` `d \<in> s`
apply blast+
done
ultimately
have "kle n e d \<and> (card ?kle2 - 1) + (2 + (card ?kle1 - 1)) \<le> card {k\<in>{1..n}. e k < d k}"
apply -
- apply (rule kle_range_combine[where y=a]) using assm(6)[rule_format,OF `e\<in>s` `d\<in>s`]
+ apply (rule kle_range_combine[where y=a]) using assm(6)[rule_format, OF `e \<in> s` `d \<in> s`]
apply blast+
done
moreover have "card {k \<in> {1..n}. e k < d k} \<le> card {1..n}"
by (rule card_mono) auto
- ultimately show False unfolding n by auto
+ ultimately show False
+ unfolding n by auto
qed
then guess k unfolding card_1_exists .. note k = this[unfolded mem_Collect_eq]
show ?thesis
apply (rule disjI2)
- apply (rule_tac x=b in bexI, rule_tac x=k in bexI)
+ apply (rule_tac x=b in bexI)
+ apply (rule_tac x=k in bexI)
proof
fix j :: nat
have "kle n a b"
- using b and assm(6)[rule_format, OF `a\<in>s` `b\<in>s`] by auto
+ using b and assm(6)[rule_format, OF `a\<in>s` `b\<in>s`]
+ by auto
then guess kk unfolding kle_def .. note kk_raw = this
note kk = this[THEN conjunct2, rule_format]
have kkk: "k \<in> kk"
@@ -1040,32 +1193,38 @@
using kk_raw kkk
apply auto
done
- then show ?thesis unfolding kk using kkk by auto
+ then show ?thesis
+ unfolding kk using kkk by auto
next
case False
then have "j \<noteq> k"
- using k(2)[rule_format, of j k] and kk_raw kkk by auto
- then show ?thesis unfolding kk using kkk and False
+ using k(2)[rule_format, of j k] and kk_raw kkk
+ by auto
+ then show ?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
lemma ksimplex_predecessor:
- assumes "ksimplex p n s" "a \<in> s"
- shows "(\<forall>x\<in>s. kle n a x) \<or> (\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. a(j) = (if j = k then y(j) + 1 else y(j)))"
+ assumes "ksimplex p n s"
+ and "a \<in> s"
+ shows "(\<forall>x\<in>s. kle n a x) \<or> (\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. a j = (if j = k then y j + 1 else y j))"
proof (cases "\<forall>x\<in>s. kle n a x")
case True
then show ?thesis by auto
next
note assm = ksimplexD[OF assms(1)]
case False
- then obtain b where b:"b\<in>s" "\<not> kle n a b" "\<forall>x\<in>{x \<in> s. \<not> kle n a x}. kle n x b"
- using kle_maximal[of "{x\<in>s. \<not> kle n a x}" n] and assm by auto
+ then obtain b where b: "b \<in> s" "\<not> kle n a b" "\<forall>x\<in>{x \<in> s. \<not> kle n a x}. kle n x b"
+ using kle_maximal[of "{x\<in>s. \<not> kle n a x}" n] and assm
+ by auto
then have **: "1 \<le> card {k\<in>{1..n}. a k > b k}"
apply -
apply (rule kle_strict_set)
- using assm(6) and `a\<in>s`
+ using assm(6) and `a \<in> s`
apply (auto simp add: kle_refl)
done
@@ -1079,23 +1238,28 @@
using assm(2) by auto
obtain c d where c_d: "c \<in> s" "\<not> kle n a c" "d \<in> s" "\<not> kle n a d"
"kle n d c" "card ?kle1 - 1 \<le> card {k \<in> {1..n}. c k > d k}"
- using kle_range_induct[OF sizekle1, of n] using assm by auto
+ using kle_range_induct[OF sizekle1, of n]
+ using assm
+ by auto
let ?kle2 = "{x \<in> s. kle n a x}"
have "card ?kle2 > 0"
apply (rule ccontr)
- using assm(6)[rule_format,of a a] and `a\<in>s` and assm(2)
+ using assm(6)[rule_format,of a a] and `a \<in> s` and assm(2)
apply auto
done
- then have sizekle2:"card ?kle2 = Suc (card ?kle2 - 1)"
- using assm(2) by auto
+ then have sizekle2: "card ?kle2 = Suc (card ?kle2 - 1)"
+ using assm(2)
+ by auto
obtain e f where e_f: "e \<in> s" "kle n a e" "f \<in> s" "kle n a f"
"kle n f e" "card ?kle2 - 1 \<le> card {k \<in> {1..n}. e k > f k}"
- using kle_range_induct[OF sizekle2, of n] using assm by auto
+ using kle_range_induct[OF sizekle2, of n]
+ using assm
+ by auto
have "card {k\<in>{1..n}. a k > b k} = 1"
proof (rule ccontr)
- case goal1
+ assume "\<not> ?thesis"
then have as: "card {k\<in>{1..n}. a k > b k} \<ge> 2"
using ** by auto
have *: "finite ?kle2" "finite ?kle1" "?kle2 \<union> ?kle1 = s" "?kle2 \<inter> ?kle1 = {}"
@@ -1103,7 +1267,8 @@
have "(card ?kle2 - 1) + 2 + (card ?kle1 - 1) = card ?kle2 + card ?kle1"
using sizekle1 sizekle2 by auto
also have "\<dots> = n + 1"
- unfolding card_Un_Int[OF *(1-2)] *(3-) using assm(3) by auto
+ unfolding card_Un_Int[OF *(1-2)] *(3-)
+ using assm(3) by auto
finally have n: "(card ?kle1 - 1) + 2 + (card ?kle2 - 1) = n + 1"
by auto
have "kle n a e \<and> card {x \<in> s. kle n a x} - 1 \<le> card {k \<in> {1..n}. e k > a k}"
@@ -1118,7 +1283,7 @@
done
then have "kle n d a \<and> (card {x \<in> s. \<not> kle n a x} - 1) + 2 \<le> card {k \<in> {1..n}. a k > d k}"
apply -
- apply (rule kle_range_combine[where y=b]) using as and b assm(6) `a\<in>s` `d\<in>s`
+ apply (rule kle_range_combine[where y=b]) using as and b assm(6) `a \<in> s` `d \<in> s`
apply blast+
done
ultimately have "kle n d e \<and> (card ?kle1 - 1 + 2) + (card ?kle2 - 1) \<le> card {k\<in>{1..n}. e k > d k}"
@@ -1129,13 +1294,15 @@
done
moreover have "card {k \<in> {1..n}. e k > d k} \<le> card {1..n}"
by (rule card_mono) auto
- ultimately show False unfolding n by auto
+ ultimately show False
+ unfolding n by auto
qed
then guess k unfolding card_1_exists .. note k = this[unfolded mem_Collect_eq]
show ?thesis
apply (rule disjI2)
- apply (rule_tac x=b in bexI,rule_tac x=k in bexI)
+ apply (rule_tac x=b in bexI)
+ apply (rule_tac x=k in bexI)
proof
fix j :: nat
have "kle n b a"
@@ -1157,13 +1324,18 @@
using kk_raw kkk
apply auto
done
- then show ?thesis unfolding kk using kkk by auto
+ then show ?thesis
+ unfolding kk using kkk by auto
next
case False
- then have "j \<noteq> k" using k(2)[rule_format, of j k]
- using kk_raw kkk by auto
- then show ?thesis unfolding kk
- using kkk and False by auto
+ then have "j \<noteq> k"
+ using k(2)[rule_format, of j k]
+ using kk_raw kkk
+ by auto
+ then show ?thesis
+ unfolding kk
+ using kkk and False
+ by auto
qed
qed (insert k(1) `b\<in>s`, auto)
qed
@@ -1173,25 +1345,32 @@
(* FIXME: These are clones of lemmas in Library/FuncSet *)
lemma card_funspace':
- assumes "finite s" "finite t" "card s = m" "card t = n"
- shows "card {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)} = n ^ m" (is "card (?M s) = _")
+ assumes "finite s"
+ and "finite t"
+ and "card s = m"
+ and "card t = n"
+ shows "card {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)} = n ^ m"
+ (is "card (?M s) = _")
using assms
- apply -
proof (induct m arbitrary: s)
case 0
have [simp]: "{f. \<forall>x. f x = d} = {\<lambda>x. d}"
- apply (rule set_eqI,rule)
+ apply (rule set_eqI)
+ apply rule
unfolding mem_Collect_eq
- apply (rule, rule ext)
+ apply rule
+ apply (rule ext)
apply auto
done
- from 0 show ?case by auto
+ from 0 show ?case
+ by auto
next
case (Suc m)
guess a using card_eq_SucD[OF Suc(4)] ..
then guess s0 by (elim exE conjE) note as0 = this
have **: "card s0 = m"
- using as0 using Suc(2) Suc(4) by auto
+ using as0 using Suc(2) Suc(4)
+ by auto
let ?l = "(\<lambda>(b, g) x. if x = a then b else g x)"
have *: "?M (insert a s0) = ?l ` {(b,g). b\<in>t \<and> g\<in>?M s0}"
apply (rule set_eqI, rule)
@@ -1202,40 +1381,52 @@
prefer 3
apply rule
defer
- apply (erule bexE, rule)
+ apply (erule bexE)
+ apply rule
unfolding mem_Collect_eq
apply (erule splitE)+
apply (erule conjE)+
proof -
fix x xa xb xc y
- assume as: "x = (\<lambda>(b, g) x. if x = a then b else g x) xa"
- "xb \<in> UNIV - insert a s0" "xa = (xc, y)" "xc \<in> t"
- "\<forall>x\<in>s0. y x \<in> t" "\<forall>x\<in>UNIV - s0. y x = d"
- then show "x xb = d" unfolding as by auto
+ assume as:
+ "x = (\<lambda>(b, g) x. if x = a then b else g x) xa"
+ "xb \<in> UNIV - insert a s0" "xa = (xc, y)"
+ "xc \<in> t"
+ "\<forall>x\<in>s0. y x \<in> t"
+ "\<forall>x\<in>UNIV - s0. y x = d"
+ then show "x xb = d"
+ unfolding as by auto
qed auto
have inj: "inj_on ?l {(b,g). b\<in>t \<and> g\<in>?M s0}"
unfolding inj_on_def
- apply (rule, rule, rule)
- unfolding mem_Collect_eq
- apply (erule splitE conjE)+
+ apply rule
+ apply rule
+ apply rule
+ unfolding mem_Collect_eq
+ apply (erule splitE conjE)+
proof -
case goal1 note as = this(1,4-)[unfolded goal1 split_conv]
- have "xa = xb" using as(1)[THEN cong[of _ _ a]] by auto
+ have "xa = xb"
+ using as(1)[THEN cong[of _ _ a]] by auto
moreover have "ya = yb"
proof (rule ext)
fix x
show "ya x = yb x"
proof (cases "x = a")
case False
- then show ?thesis using as(1)[THEN cong[of _ _ x x]] by auto
+ then show ?thesis
+ using as(1)[THEN cong[of _ _ x x]] by auto
next
case True
- then show ?thesis using as(5,7) using as0(2) by auto
+ then show ?thesis
+ using as(5,7) using as0(2) by auto
qed
qed
- ultimately show ?case unfolding goal1 by auto
+ ultimately show ?case
+ unfolding goal1 by auto
qed
- have "finite s0" using `finite s` unfolding as0 by simp
+ have "finite s0"
+ using `finite s` unfolding as0 by simp
show ?case
unfolding as0 * card_image[OF inj]
using assms
@@ -1246,28 +1437,37 @@
qed
lemma card_funspace:
- assumes "finite s" "finite t"
- shows "card {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)} = (card t) ^ (card s)"
+ assumes "finite s"
+ and "finite t"
+ shows "card {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)} = card t ^ card s"
using assms by (auto intro: card_funspace')
lemma finite_funspace:
- assumes "finite s" "finite t"
- shows "finite {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)}" (is "finite ?S")
+ assumes "finite s"
+ and "finite t"
+ shows "finite {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)}"
+ (is "finite ?S")
proof (cases "card t > 0")
case True
- have "card ?S = (card t) ^ (card s)"
+ have "card ?S = card t ^ card s"
using assms by (auto intro!: card_funspace)
- then show ?thesis using True by (rule_tac card_ge_0_finite) simp
+ then show ?thesis
+ using True by (rule_tac card_ge_0_finite) simp
next
- case False then have "t = {}" using `finite t` by auto
+ case False
+ then have "t = {}"
+ using `finite t` by auto
show ?thesis
proof (cases "s = {}")
- have *: "{f. \<forall>x. f x = d} = {\<lambda>x. d}" by auto
case True
- then show ?thesis using `t = {}` by (auto simp: *)
+ have *: "{f. \<forall>x. f x = d} = {\<lambda>x. d}"
+ by auto
+ from True show ?thesis
+ using `t = {}` by (auto simp: *)
next
case False
- then show ?thesis using `t = {}` by simp
+ then show ?thesis
+ using `t = {}` by simp
qed
qed
@@ -1281,8 +1481,10 @@
done
lemma simplex_top_face:
- assumes "0 < p" "\<forall>x\<in>f. x (n + 1) = p"
- shows "(\<exists>s a. ksimplex p (n + 1) s \<and> a \<in> s \<and> (f = s - {a})) \<longleftrightarrow> ksimplex p n f" (is "?ls = ?rs")
+ assumes "0 < p"
+ and "\<forall>x\<in>f. x (n + 1) = p"
+ shows "(\<exists>s a. ksimplex p (n + 1) s \<and> a \<in> s \<and> (f = s - {a})) \<longleftrightarrow> ksimplex p n f"
+ (is "?ls = ?rs")
proof
assume ?ls
then guess s ..
@@ -1308,14 +1510,16 @@
case True
then guess k unfolding kle_def .. note k = this
then have *: "n + 1 \<notin> k" using xyp by auto
- have "\<not> (\<exists>x\<in>k. x\<notin>{1..n})"
+ have "\<not> (\<exists>x\<in>k. x \<notin> {1..n})"
apply (rule notI)
apply (erule bexE)
proof -
fix x
assume as: "x \<in> k" "x \<notin> {1..n}"
- have "x \<noteq> n + 1" using as and * by auto
- then show False using as and k[THEN conjunct1,unfolded subset_eq] by auto
+ have "x \<noteq> n + 1"
+ using as and * by auto
+ then show False
+ using as and k[THEN conjunct1,unfolded subset_eq] by auto
qed
then show ?thesis
apply -
@@ -1328,18 +1532,23 @@
next
case False
then have "kle (n + 1) y x"
- using ksimplexD(6)[OF sa(1),rule_format, of x y] and as by auto
+ 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 \<notin> k" using xyp by auto
- then have "\<not> (\<exists>x\<in>k. x\<notin>{1..n})"
+ then have *: "n + 1 \<notin> k"
+ using xyp by auto
+ then have "\<not> (\<exists>x\<in>k. x \<notin> {1..n})"
apply -
apply (rule notI)
apply (erule bexE)
proof -
fix x
assume as: "x \<in> k" "x \<notin> {1..n}"
- have "x \<noteq> n + 1" using as and * by auto
- then show False using as and k[THEN conjunct1,unfolded subset_eq] by auto
+ have "x \<noteq> n + 1"
+ using as and * by auto
+ then show False
+ using as and k[THEN conjunct1,unfolded subset_eq]
+ by auto
qed
then show ?thesis
apply -
@@ -1352,10 +1561,10 @@
qed
next
fix x j
- assume as: "x \<in> s - {a}" "j\<notin>{1..n}"
+ assume as: "x \<in> s - {a}" "j \<notin> {1..n}"
then show "x j = p"
using as(1)[unfolded sa(3)[symmetric], THEN assms(2)[rule_format]]
- apply (cases "j = n+1")
+ apply (cases "j = n + 1")
using sa(1)[unfolded ksimplex_def]
apply auto
done
@@ -1372,7 +1581,8 @@
apply auto
done
then show ?ls
- apply (rule_tac x = "insert c f" in exI, rule_tac x = c in exI)
+ apply (rule_tac x = "insert c f" in exI)
+ apply (rule_tac x = c in exI)
unfolding ksimplex_def conj_assoc
apply (rule conjI)
defer
@@ -1386,15 +1596,19 @@
fix x j
assume x: "x \<in> insert c f"
then show "x j \<le> p"
- proof (cases "x=c")
+ proof (cases "x = c")
case True
show ?thesis
unfolding True c_def
- apply (cases "j=n+1")
+ apply (cases "j = n + 1")
using ab(1) and rs(4)
apply auto
done
- qed (insert x rs(4), auto simp add:c_def)
+ next
+ case False
+ with insert x rs(4) show ?thesis
+ by (auto simp add: c_def)
+ qed
show "j \<notin> {1..n + 1} \<longrightarrow> x j = p"
apply (cases "x = c")
using x ab(1) rs(5)
@@ -1405,10 +1619,10 @@
fix z
assume z: "z \<in> insert c f"
then have "kle (n + 1) c z"
- apply (cases "z = c") (*defer apply(rule kle_Suc)*)
- proof -
+ proof (cases "z = c")
case False
- then have "z \<in> f" using z by auto
+ then have "z \<in> f"
+ using z by auto
then guess k
apply (drule_tac ab(3)[THEN bspec[where x=z], THEN conjunct1])
unfolding kle_def
@@ -1422,23 +1636,34 @@
using rs(5)[rule_format,OF ab(1),of "n + 1"] assms(1)
apply auto
done
- qed auto
+ next
+ case True
+ then show ?thesis by auto
+ qed
} note * = this
fix y
assume y: "y \<in> insert c f"
show "kle (n + 1) x y \<or> kle (n + 1) y x"
proof (cases "x = c \<or> y = c")
- case False then have **: "x \<in> f" "y \<in> f" using x y by auto
- show ?thesis using rs(6)[rule_format,OF **]
+ case False
+ then have **: "x \<in> f" "y \<in> f"
+ using x y by auto
+ show ?thesis
+ using rs(6)[rule_format,OF **]
by (auto dest: kle_Suc)
qed (insert * x y, auto)
qed (insert rs, auto)
qed
lemma ksimplex_fix_plane:
- assumes "a \<in> s" "j\<in>{1..n::nat}" "\<forall>x\<in>s - {a}. x j = q" "a0 \<in> s" "a1 \<in> s"
- "\<forall>i. a1 i = ((if i\<in>{1..n} then a0 i + 1 else a0 i)::nat)"
- shows "(a = a0) \<or> (a = a1)"
+ fixes a a0 a1 :: "nat \<Rightarrow> nat"
+ assumes "a \<in> s"
+ and "j \<in> {1..n}"
+ and "\<forall>x\<in>s - {a}. x j = q"
+ and "a0 \<in> s"
+ and "a1 \<in> s"
+ and "\<forall>i. a1 i = (if i \<in> {1..n} then a0 i + 1 else a0 i)"
+ shows "a = a0 \<or> a = a1"
proof -
have *: "\<And>P A x y. \<forall>x\<in>A. P x \<Longrightarrow> x\<in>A \<Longrightarrow> y\<in>A \<Longrightarrow> P x \<and> P y"
by auto
@@ -1452,8 +1677,13 @@
qed
lemma ksimplex_fix_plane_0:
- assumes "a \<in> s" "j\<in>{1..n::nat}" "\<forall>x\<in>s - {a}. x j = 0" "a0 \<in> s" "a1 \<in> s"
- "\<forall>i. a1 i = ((if i\<in>{1..n} then a0 i + 1 else a0 i)::nat)"
+ fixes a a0 a1 :: "nat \<Rightarrow> nat"
+ assumes "a \<in> s"
+ and "j \<in> {1..n}"
+ and "\<forall>x\<in>s - {a}. x j = 0"
+ and "a0 \<in> s"
+ and "a1 \<in> s"
+ and "\<forall>i. a1 i = (if i\<in>{1..n} then a0 i + 1 else a0 i)"
shows "a = a1"
apply (rule ccontr)
using ksimplex_fix_plane[OF assms]
@@ -1464,12 +1694,17 @@
done
lemma ksimplex_fix_plane_p:
- assumes "ksimplex p n s" "a \<in> s" "j\<in>{1..n}" "\<forall>x\<in>s - {a}. x j = p" "a0 \<in> s" "a1 \<in> s"
- "\<forall>i. a1 i = (if i\<in>{1..n} then a0 i + 1 else a0 i)"
+ assumes "ksimplex p n s"
+ and "a \<in> s"
+ and "j \<in> {1..n}"
+ and "\<forall>x\<in>s - {a}. x j = p"
+ and "a0 \<in> s"
+ and "a1 \<in> s"
+ and "\<forall>i. a1 i = (if i\<in>{1..n} then a0 i + 1 else a0 i)"
shows "a = a0"
proof (rule ccontr)
note s = ksimplexD[OF assms(1),rule_format]
- assume as: "a \<noteq> a0"
+ assume as: "\<not> ?thesis"
then have *: "a0 \<in> s - {a}"
using assms(5) by auto
then have "a1 = a"
@@ -1482,16 +1717,19 @@
qed
lemma ksimplex_replace_0:
- assumes "ksimplex p n s" "a \<in> s" "n \<noteq> 0" "j\<in>{1..n}" "\<forall>x\<in>s - {a}. x j = 0"
+ assumes "ksimplex p n s" "a \<in> s"
+ and "n \<noteq> 0"
+ and "j \<in> {1..n}"
+ and "\<forall>x\<in>s - {a}. x j = 0"
shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 1"
proof -
- have *: "\<And>s' a a'. s' - {a'} = s - {a} \<Longrightarrow> a' = a \<Longrightarrow> a' \<in> s' \<Longrightarrow> a \<in> s \<Longrightarrow> (s' = s)"
+ have *: "\<And>s' a a'. s' - {a'} = s - {a} \<Longrightarrow> a' = a \<Longrightarrow> a' \<in> s' \<Longrightarrow> a \<in> s \<Longrightarrow> s' = s"
by auto
have **: "\<And>s' a'. ksimplex p n s' \<Longrightarrow> a' \<in> s' \<Longrightarrow> s' - {a'} = s - {a} \<Longrightarrow> s' = s"
proof -
case goal1
guess a0 a1 by (rule ksimplex_extrema_strong[OF assms(1,3)]) note exta = this[rule_format]
- have a:"a = a1"
+ have a: "a = a1"
apply (rule ksimplex_fix_plane_0[OF assms(2,4-5)])
using exta(1-2,5)
apply auto
@@ -1538,7 +1776,11 @@
qed
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"
+ assumes "ksimplex p n s"
+ and "a \<in> s"
+ and "n \<noteq> 0"
+ and "j \<in> {1..n}"
+ and "\<forall>x\<in>s - {a}. x j = p"
shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 1"
proof -
have lem: "\<And>a a' s'. s' - {a'} = s - {a} \<Longrightarrow> a' = a \<Longrightarrow> a' \<in> s' \<Longrightarrow> a \<in> s \<Longrightarrow> s' = s"
@@ -1570,16 +1812,12 @@
by blast
moreover
have "a0 = b0"
- apply (rule ext)
- proof -
- case goal1
+ proof (rule ext)
+ fix x
show "a0 x = b0 x"
using *[THEN cong, of x x]
unfolding exta extb
- apply -
- apply (cases "x \<in> {1..n}")
- apply auto
- done
+ by (cases "x \<in> {1..n}") auto
qed
ultimately
show "s' = s"
@@ -1592,7 +1830,8 @@
unfolding card_1_exists
apply (rule ex1I[of _ s])
unfolding mem_Collect_eq
- apply (rule, rule assms(1))
+ apply rule
+ apply (rule assms(1))
apply (rule_tac x = a in bexI)
prefer 3
apply (erule conjE bexE)+
@@ -1603,26 +1842,33 @@
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)"
+ assumes "ksimplex p n s"
+ and "a \<in> s"
+ and "n \<noteq> 0"
+ and "\<not> (\<exists>j\<in>{1..n}. \<forall>x\<in>s - {a}. x j = 0)"
+ and "\<not> (\<exists>j\<in>{1..n}. \<forall>x\<in>s - {a}. x j = p)"
shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 2"
- (is "card ?A = 2")
+ (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})"
+ have lem2: "\<And>a b. a \<in> s \<Longrightarrow> b \<noteq> a \<Longrightarrow> s \<noteq> insert b (s - {a})"
proof
case goal1
- then have "a \<in> insert b (s - {a})" by auto
- then have "a \<in> s - {a}" unfolding insert_iff using goal1 by auto
- then show False by auto
+ then have "a \<in> insert b (s - {a})"
+ by auto
+ then have "a \<in> s - {a}"
+ unfolding insert_iff
+ using goal1
+ by auto
+ then show False
+ by auto
qed
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 *: "\<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
@@ -1630,7 +1876,8 @@
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
+ using assms(3)
+ by auto
qed (insert a0a1, auto)
then have "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then a0 j + 1 else a0 j)"
apply (rule_tac *[OF ksimplex_successor[OF assms(1-2),unfolded `a=a0`]])
@@ -1643,86 +1890,115 @@
proof
assume "a3\<in>s"
then have "kle n a3 a1"
- using a0a1(4) by auto
+ using a0a1(4) by auto
then show False
- apply (drule_tac kle_imp_pointwise) unfolding a3_def
+ apply (drule_tac kle_imp_pointwise)
+ unfolding a3_def
apply (erule_tac x = k in allE)
apply auto
done
qed
- then have "a3 \<noteq> a0" "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"
+ then have "a3 \<noteq> a0" and "a3 \<noteq> a1"
+ using a0a1 by auto
+ have "a2 \<noteq> a0"
+ using k(2)[THEN spec[where x=k]] by auto
+ have lem3: "\<And>x. x \<in> (s - {a0}) \<Longrightarrow> kle n a2 x"
proof (rule ccontr)
case goal1
- then have as: "x\<in>s" "x\<noteq>a0" by auto
+ then have as: "x \<in> s" "x \<noteq> a0"
+ by auto
have "kle n a2 x \<or> kle n x a2"
- using ksimplexD(6)[OF assms(1)] and as `a2\<in>s` by auto
+ 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
+ have "kle n a0 x"
+ using a0a1(4) as by auto
ultimately have "x = a0 \<or> x = a2"
apply -
apply (rule kle_adjacent[OF k(2)])
using goal1(2)
apply auto
done
- then have "x = a2" using as by auto
- then show False using goal1(2) using kle_refl by auto
+ then have "x = a2"
+ using as by auto
+ then show False
+ using goal1(2)
+ using kle_refl
+ by auto
qed
let ?s = "insert a3 (s - {a0})"
have "ksimplex p n ?s"
apply (rule ksimplexI)
- proof (rule_tac[2-] ballI,rule_tac[4] ballI)
+ apply (rule_tac[2-] ballI)
+ apply (rule_tac[4] ballI)
+ proof -
show "card ?s = n + 1"
using ksimplexD(2-3)[OF assms(1)]
- using `a3\<noteq>a0` `a3\<notin>s` `a0\<in>s`
- by (auto simp add:card_insert_if)
+ 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")
+ proof
fix j
- case False
- then show "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")
+ show "x j \<le> p"
+ proof (cases "x = a3")
case False
- then show "a3 j \<le>p" unfolding True a3_def
- using `a1\<in>s` ksimplexD(4)[OF assms(1)] by auto
+ then show ?thesis
+ using x 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
- then show "a3 j \<le>p" unfolding a3_def unfolding a0a1(5)[rule_format]
- using k(1) k(2)assms(5) using * by simp
+ show ?thesis unfolding True
+ proof (cases "j = k")
+ case False
+ then show "a3 j \<le> p"
+ unfolding True a3_def
+ using `a1 \<in> s` ksimplexD(4)[OF assms(1)]
+ by auto
+ next
+ 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
+ then show "a3 j \<le>p"
+ unfolding a3_def
+ unfolding a0a1(5)[rule_format]
+ using k(1) k(2)assms(5)
+ using *
+ by simp
+ qed
qed
qed
show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p"
- proof (rule, rule, cases "x=a3")
+ proof (rule, rule)
fix j :: nat
assume j: "j \<notin> {1..n}"
- {
+ show "x j = p"
+ proof (cases "x = a3")
case False
- then show "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
+ then show ?thesis
+ using j x ksimplexD(5)[OF assms(1)]
+ by auto
+ next
+ case True
+ show ?thesis
+ unfolding True a3_def
+ using j k(1)
+ using ksimplexD(5)[OF assms(1),rule_format,OF `a1\<in>s` j]
+ by auto
+ qed
qed
fix y
assume y: "y \<in> insert a3 (s - {a0})"
- have lem4: "\<And>x. x\<in>s \<Longrightarrow> x\<noteq>a0 \<Longrightarrow> kle n x a3"
+ 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]
@@ -1731,12 +2007,17 @@
have "k \<notin> kk"
proof
assume "k \<in> kk"
- then have "a1 k = x k + 1" using kk by auto
- then have "a0 k = x k" unfolding a0a1(5)[rule_format] using k(1) by auto
- then have "a2 k = x k + 1" unfolding k(2)[rule_format] by auto
+ then have "a1 k = x k + 1"
+ using kk by auto
+ then have "a0 k = x k"
+ unfolding a0a1(5)[rule_format] using k(1) by auto
+ then have "a2 k = x k + 1"
+ unfolding k(2)[rule_format] by auto
moreover
- have "a2 k \<le> x k" using lem3[of x,THEN kle_imp_pointwise] goal1 by auto
- ultimately show False by auto
+ have "a2 k \<le> x k"
+ using lem3[of x,THEN kle_imp_pointwise] goal1 by auto
+ ultimately show False
+ by auto
qed
then show ?case
unfolding kle_def
@@ -1765,7 +2046,8 @@
case True
show ?thesis
unfolding True
- apply (rule disjI2, rule lem4)
+ apply (rule disjI2)
+ apply (rule lem4)
using y False
apply auto
done
@@ -1782,15 +2064,18 @@
then have "insert a3 (s - {a0}) \<in> ?A"
unfolding mem_Collect_eq
apply -
- apply (rule, assumption)
+ apply rule
+ apply assumption
apply (rule_tac x = "a3" in bexI)
unfolding `a = a0`
using `a3 \<notin> s`
apply auto
done
moreover
- have "s \<in> ?A" using assms(1,2) by auto
- ultimately have "?A \<supseteq> {s, insert a3 (s - {a0})}" by auto
+ 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
@@ -1819,8 +2104,10 @@
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
+ 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) *])
@@ -1836,53 +2123,72 @@
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 "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"
- then have "a_max = a'" using a' min_max by auto
- then show False unfolding True using min_max by auto
+ assume "\<not> ?thesis"
+ then have "a_max = a'"
+ using a' min_max by auto
+ then show False
+ unfolding True using min_max by auto
qed
qed
- then have "\<forall>i. a_max i = a1 i" by auto
- then have "a' = a" unfolding True `a = a0`
+ then have "\<forall>i. a_max i = a1 i"
+ by auto
+ then have "a' = a"
+ unfolding True `a = a0`
apply -
- apply (subst fun_eq_iff, rule)
+ apply (subst fun_eq_iff)
+ apply rule
apply (erule_tac x=x in allE)
unfolding a0a1(5)[rule_format] min_max(5)[rule_format]
proof -
case goal1
- then show ?case by (cases "x\<in>{1..n}") auto
+ then show ?case
+ by (cases "x \<in> {1..n}") auto
qed
then have "s' = s"
apply -
apply (rule lem1[OF a'(2)])
- using `a\<in>s` `a'\<in>s'`
+ using `a \<in> s` `a' \<in> s'`
apply auto
done
- then show ?thesis by auto
+ then show ?thesis
+ by auto
next
case False
- then have as:"a' = a_max" using ** by auto
- have "a_min = a2" unfolding kle_antisym[symmetric, of _ _ n]
+ then have as: "a' = a_max"
+ using ** by auto
+ have "a_min = a2"
+ unfolding kle_antisym[symmetric, of _ _ n]
apply rule
apply (rule min_max(4)[rule_format,THEN conjunct1])
defer
proof (rule lem3)
show "a_min \<in> s - {a0}"
unfolding a'(2)[symmetric,unfolded `a = a0`]
- unfolding as using min_max(1-3) by auto
+ 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
+ unfolding `a = a0`
+ using k(2)[rule_format,of k]
+ by auto
then have "a2 \<in> s - {a}"
using a2 by auto
- then show "a2 \<in> s'" unfolding a'(2)[symmetric] by auto
+ then show "a2 \<in> s'"
+ unfolding a'(2)[symmetric] by auto
qed
- then have "\<forall>i. a_min i = a2 i" by auto
+ then have "\<forall>i. a_min i = a2 i"
+ by auto
then have "a' = a3"
unfolding as `a = a0`
- apply -
- apply (subst fun_eq_iff, rule)
+ apply (subst fun_eq_iff)
+ apply rule
apply (erule_tac x=x in allE)
unfolding a0a1(5)[rule_format] min_max(5)[rule_format]
unfolding a3_def k(2)[rule_format]
@@ -1891,10 +2197,10 @@
case goal1
show ?case
unfolding goal1
- apply (cases "x\<in>{1..n}")
+ apply (cases "x \<in> {1..n}")
defer
apply (cases "x = k")
- using `k\<in>{1..n}`
+ using `k \<in> {1..n}`
apply auto
done
qed
@@ -1911,14 +2217,18 @@
then show ?thesis by auto
qed
qed
- ultimately have *: "?A = {s, insert a3 (s - {a0})}" by blast
- have "s \<noteq> insert a3 (s - {a0})" using `a3\<notin>s` by auto
- then have ?thesis unfolding * by auto
+ ultimately have *: "?A = {s, insert a3 (s - {a0})}"
+ by blast
+ have "s \<noteq> insert a3 (s - {a0})"
+ using `a3\<notin>s` by auto
+ then have ?thesis
+ unfolding * by auto
}
moreover
{
assume "a = a1"
- have *: "\<And>P Q. (P \<or> Q) \<Longrightarrow> \<not> P \<Longrightarrow> Q" by auto
+ have *: "\<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
@@ -1935,101 +2245,124 @@
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"
+ have "a2 \<noteq> a1"
+ using k(2)[THEN spec[where x=k]] by auto
+ have lem3: "\<And>x. x \<in> s - {a1} \<Longrightarrow> kle n x a2"
proof (rule ccontr)
case goal1
- then have as: "x\<in>s" "x\<noteq>a1" by auto
+ then have as: "x \<in> s" "x \<noteq> a1" by auto
have "kle n a2 x \<or> kle n x a2"
- using ksimplexD(6)[OF assms(1)] and as `a2\<in>s` by auto
+ 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
+ have "kle n x a1"
+ using a0a1(4) as by auto
ultimately have "x = a2 \<or> x = a1"
apply -
apply (rule kle_adjacent[OF k(2)])
using goal1(2)
apply auto
done
- then have "x = a2" using as by auto
- then show False using goal1(2) using kle_refl by auto
+ then have "x = a2"
+ using as by auto
+ then show False
+ using goal1(2) using kle_refl by auto
qed
have "a0 k \<noteq> 0"
proof -
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]
+ 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
- moreover have "a4 k > 0" using a4 by auto
- ultimately have "a2 k > 0" by auto
- then have "a1 k > 1" unfolding k(2)[rule_format] by simp
- then show ?thesis unfolding a0a1(5)[rule_format] using k(1) by simp
+ then have "a1 k > 1"
+ unfolding k(2)[rule_format] by simp
+ then show ?thesis
+ unfolding a0a1(5)[rule_format] using k(1) by simp
qed
- then have lem4: "\<forall>j. a0 j = (if j=k then a3 j + 1 else a3 j)"
+ then have lem4: "\<forall>j. a0 j = (if j = k then a3 j + 1 else a3 j)"
unfolding a3_def by simp
have "\<not> kle n a0 a3"
- apply (rule ccontr)
- unfolding not_not
+ apply (rule notI)
apply (drule kle_imp_pointwise)
unfolding lem4[rule_format]
apply (erule_tac x=k in allE)
apply auto
done
- then have "a3 \<notin> s" using a0a1(4) by auto
- then have "a3 \<noteq> a1" "a3 \<noteq> a0" using a0a1 by auto
+ then have "a3 \<notin> s"
+ using a0a1(4) by auto
+ then have "a3 \<noteq> a1" "a3 \<noteq> a0"
+ using a0a1 by auto
let ?s = "insert a3 (s - {a1})"
have "ksimplex p n ?s"
apply (rule ksimplexI)
proof (rule_tac[2-] ballI,rule_tac[4] ballI)
show "card ?s = n+1"
using ksimplexD(2-3)[OF assms(1)]
- using `a3\<noteq>a0` `a3\<notin>s` `a1\<in>s`
- by(auto simp add:card_insert_if)
+ 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")
+ show "\<forall>j. x j \<le> p"
+ proof
fix j
- case False
- then show "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")
+ show "x j \<le> p"
+ proof (cases "x = a3")
case False
- then show "a3 j \<le>p"
- unfolding True a3_def
- using `a0\<in>s` ksimplexD(4)[OF assms(1)]
- by auto
+ then show ?thesis
+ using x 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
+ case True
+ show ?thesis
+ unfolding True
+ proof (cases "j = k")
+ case False
+ then show "a3 j \<le> p"
+ unfolding True a3_def
+ using `a0 \<in> s` ksimplexD(4)[OF assms(1)]
+ by auto
+ next
+ 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
qed
show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p"
- proof (rule, rule, cases "x = a3")
+ proof (rule, rule)
fix j :: nat
assume j: "j \<notin> {1..n}"
- {
+ show "x j = p"
+ proof (cases "x = a3")
case False
- then show "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto
+ then show ?thesis
+ 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
- }
+ show ?thesis
+ unfolding True a3_def
+ using j k(1)
+ using ksimplexD(5)[OF assms(1),rule_format,OF `a0\<in>s` j]
+ by auto
+ qed
qed
fix y
- assume y: "y\<in>insert a3 (s - {a1})"
- have lem4: "\<And>x. x\<in>s \<Longrightarrow> x \<noteq> a1 \<Longrightarrow> kle n a3 x"
+ assume y: "y \<in> insert a3 (s - {a1})"
+ have lem4: "\<And>x. x \<in> s \<Longrightarrow> x \<noteq> a1 \<Longrightarrow> kle n a3 x"
proof -
case goal1
- then have *: "x\<in>s - {a1}" by auto
+ then have *: "x\<in>s - {a1}"
+ by auto
have "kle n a3 a2"
proof -
have "kle n a0 a1"
@@ -2075,7 +2408,8 @@
unfolding True
apply (cases "x = a3")
defer
- apply (rule disjI2, rule lem4)
+ apply (rule disjI2)
+ apply (rule lem4)
using x
apply auto
done
@@ -2086,7 +2420,8 @@
case True
show ?thesis
unfolding True
- apply (rule disjI1, rule lem4)
+ apply (rule disjI1)
+ apply (rule lem4)
using y False
apply auto
done
@@ -2094,7 +2429,7 @@
case False
then show ?thesis
apply (rule_tac ksimplexD(6)[OF assms(1),rule_format])
- using x y `y\<noteq>a3`
+ using x y `y \<noteq> a3`
apply auto
done
qed
@@ -2110,8 +2445,10 @@
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
+ 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
@@ -2146,7 +2483,8 @@
by auto
finally have "a2 k \<le> x k" .
}
- ultimately show "x k = a2 k" 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) *])
@@ -2179,36 +2517,47 @@
unfolding kle_antisym[symmetric,of a_max a2 n]
apply -
apply rule
- apply (rule lem3,assumption)
+ apply (rule lem3)
+ apply assumption
apply (rule min_max(4)[rule_format,THEN conjunct2])
using a2'
apply auto
done
- then have a_max:"\<forall>i. a_max i = a2 i" by auto
- have *: "\<forall>j. a2 j = (if j\<in>{1..n} then a3 j + 1 else a3 j)"
+ then have a_max: "\<forall>i. a_max i = a2 i"
+ by auto
+ have *: "\<forall>j. a2 j = (if j \<in> {1..n} then a3 j + 1 else a3 j)"
using k(2)
unfolding lem4[rule_format] a0a1(5)[rule_format]
apply -
- apply (rule,erule_tac x=j in allE)
+ apply rule
+ apply (erule_tac x=j in allE)
proof -
case goal1
- then show ?case by (cases "j\<in>{1..n}",case_tac[!] "j=k") auto
+ then show ?case by (cases "j \<in> {1..n}", case_tac[!] "j = k") auto
qed
have "\<forall>i. a_min i = a3 i"
using a_max
apply -
- apply (rule,erule_tac x=i in allE)
+ apply rule
+ apply (erule_tac x=i in allE)
unfolding min_max(5)[rule_format] *[rule_format]
proof -
case goal1
- then show ?case by (cases "i\<in>{1..n}") auto
+ then show ?case
+ by (cases "i \<in> {1..n}") auto
qed
- then have "a_min = a3" unfolding fun_eq_iff .
+ then have "a_min = a3"
+ unfolding fun_eq_iff .
then have "s' = insert a3 (s - {a1})"
- using a' unfolding `a = a1` True by auto
- then show ?thesis by auto
+ using a'
+ unfolding `a = a1` True
+ by auto
+ then show ?thesis
+ by auto
next
- case False then have as:"a'=a_max" using ** by auto
+ case False
+ then have as: "a' = a_max"
+ using ** by auto
have "a_min = a0"
unfolding kle_antisym[symmetric,of _ _ n]
apply rule
@@ -2220,12 +2569,17 @@
using min_max(1,3)
unfolding a'(2)[symmetric,unfolded `a=a1`] as
by auto
- then show "a_min \<in> s" by auto
- have "a0 \<in> s - {a1}" using a0a1(1-3) by auto
- then show "a0 \<in> s'" unfolding a'(2)[symmetric,unfolded `a=a1`] by auto
+ then show "a_min \<in> s"
+ by auto
+ have "a0 \<in> s - {a1}"
+ using a0a1(1-3) by auto
+ then show "a0 \<in> s'"
+ unfolding a'(2)[symmetric,unfolded `a=a1`]
+ by auto
qed
then have "\<forall>i. a_max i = a1 i"
- unfolding a0a1(5)[rule_format] min_max(5)[rule_format] by auto
+ unfolding a0a1(5)[rule_format] min_max(5)[rule_format]
+ by auto
then have "s' = s"
apply -
apply (rule lem1[OF a'(2)])
@@ -2234,16 +2588,21 @@
unfolding fun_eq_iff
apply auto
done
- then show ?thesis by auto
+ then show ?thesis
+ by auto
qed
qed
- ultimately have *: "?A = {s, insert a3 (s - {a1})}" by blast
- have "s \<noteq> insert a3 (s - {a1})" using `a3\<notin>s` by auto
- then have ?thesis unfolding * by auto
+ ultimately have *: "?A = {s, insert a3 (s - {a1})}"
+ by blast
+ have "s \<noteq> insert a3 (s - {a1})"
+ using `a3\<notin>s` by auto
+ then have ?thesis
+ unfolding * by auto
}
moreover
{
- assume as: "a \<noteq> a0" "a \<noteq> a1" have "\<not> (\<forall>x\<in>s. kle n a x)"
+ assume as: "a \<noteq> a0" "a \<noteq> a1"
+ have "\<not> (\<forall>x\<in>s. kle n a x)"
proof
case goal1
have "a = a0"
@@ -2252,10 +2611,12 @@
using goal1 a0a1 assms(2)
apply auto
done
- then show False using as by auto
+ then show False
+ using as by auto
qed
then have "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. a j = (if j = k then y j + 1 else y j)"
- using ksimplex_predecessor[OF assms(1-2)] by blast
+ 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)"
@@ -2267,19 +2628,23 @@
using goal1 a0a1 assms(2)
apply auto
done
- then show False using as by auto
+ then show False
+ using as by auto
qed
then have "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then a j + 1 else a j)"
using ksimplex_successor[OF assms(1-2)] by blast
then guess v .. from this(2) guess l ..
note l = this[rule_format]
- note v = `v\<in>s`
+ 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
- then show False using ksimplexD(6)[OF assms(1),rule_format,OF u v] unfolding kle_def
+ have *: "\<And>P. (if P then (1::nat) else 0) \<noteq> 2"
+ by auto
+ then show False
+ using ksimplexD(6)[OF assms(1),rule_format,OF u v]
+ unfolding kle_def
unfolding l(2) k(2) `k = l`
apply -
apply (erule disjE)
@@ -2301,7 +2666,8 @@
apply (drule ksimplexD(6)[OF assms(1),rule_format,OF `a\<in>s`])
proof (cases "kle n a a'")
case goal2
- then have "kle n a' a" by auto
+ then have "kle n a' a"
+ by auto
then show False
apply (drule_tac kle_imp_pointwise)
apply (erule_tac x=l in allE)
@@ -2334,8 +2700,10 @@
then show ?case
proof (cases "x k = u k", case_tac[!] "x l = u l")
assume as: "x l = u l" "x k = u k"
- have "x = u" unfolding fun_eq_iff
- using goal1(2)[THEN kle_imp_pointwise,unfolded l(2)] unfolding k(2)
+ 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 -
@@ -2346,9 +2714,11 @@
then show ?case
apply (cases "x = l")
apply (case_tac[!] "x = k")
- using as by auto
+ using as
+ by auto
qed
- then show ?case by auto
+ then show ?case
+ by auto
next
assume as: "x l \<noteq> u l" "x k = u k"
have "x = a'"
@@ -2389,7 +2759,8 @@
apply auto
done
qed
- then show ?case by auto
+ then show ?case
+ by auto
next
assume as: "x l \<noteq> u l" "x k \<noteq> u k"
have "x = v"
@@ -2424,16 +2795,16 @@
apply (rule kle_trans[OF uv])
defer
apply (rule ksimplexD(6)[OF assms(1), rule_format])
- using kle_uv `u\<in>s`
+ 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'"
+ 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`
+ 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"
@@ -2442,12 +2813,13 @@
then show ?case
proof (cases "kle n v x \<or> kle n x u")
case True
- then show ?thesis using goal1 by(auto intro:lem3 lem4)
+ then show ?thesis
+ using goal1 by (auto intro: lem3 lem4)
next
case False
then have *: "kle n u x" "kle n x v"
using ksimplexD(6)[OF assms(1)]
- using goal1 `u\<in>s` `v\<in>s`
+ using goal1 `u \<in> s` `v \<in> s`
by auto
show ?thesis
using uxv[OF *]
@@ -2458,7 +2830,9 @@
qed
have "ksimplex p n (insert a' (s - {a}))"
apply (rule ksimplexI)
- proof (rule_tac[2-] ballI, rule_tac[4] ballI)
+ apply (rule_tac[2-] ballI)
+ apply (rule_tac[4] ballI)
+ proof -
show "card (insert a' (s - {a})) = n + 1"
using ksimplexD(2-3)[OF assms(1)]
using `a' \<noteq> a` `a' \<notin> s` `a \<in> s`
@@ -2466,45 +2840,59 @@
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
- then show "x j\<le>p" using x ksimplexD(4)[OF assms(1)] by auto
- next
+ proof
fix j
- case True
- show "x j\<le>p" unfolding True
- proof (cases "j = l")
+ show "x j \<le> p"
+ proof (cases "x = a'")
case False
- then show "a' j \<le>p"
- unfolding True a'_def using `u\<in>s` ksimplexD(4)[OF assms(1)] by auto
+ then show ?thesis
+ using x ksimplexD(4)[OF assms(1)] by auto
next
case True
- have *: "a l = u l" "v l = a l + 1"
- using k(2)[of l] l(2)[of l] `k\<noteq>l` by auto
- have "u l + 1 \<le> p"
- unfolding *[symmetric] using ksimplexD(4)[OF assms(1)] using `v\<in>s` by auto
- then show "a' j \<le>p" unfolding a'_def True by auto
+ show ?thesis
+ unfolding True
+ proof (cases "j = l")
+ case False
+ then show "a' j \<le>p"
+ unfolding True a'_def
+ using `u\<in>s` ksimplexD(4)[OF assms(1)]
+ by auto
+ next
+ case True
+ have *: "a l = u l" "v l = a l + 1"
+ using k(2)[of l] l(2)[of l] `k \<noteq> l`
+ by auto
+ have "u l + 1 \<le> p"
+ unfolding *[symmetric]
+ using ksimplexD(4)[OF assms(1)]
+ using `v \<in> s`
+ by auto
+ then show "a' j \<le>p"
+ unfolding a'_def True
+ by auto
+ qed
qed
qed
show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p"
- proof (rule, rule,cases "x = a'")
+ proof (rule, rule)
fix j :: nat
assume j: "j \<notin> {1..n}"
- {
+ show "x j = p"
+ proof (cases "x = a'")
case False
- then show "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto
+ then show ?thesis
+ using j x ksimplexD(5)[OF assms(1)] by auto
next
case True
- show "x j = p"
+ show ?thesis
unfolding True a'_def
using j l(1)
using ksimplexD(5)[OF assms(1),rule_format,OF `u\<in>s` j]
by auto
- }
+ qed
qed
fix y
- assume y: "y\<in>insert a' (s - {a})"
+ assume y: "y \<in> insert a' (s - {a})"
show "kle n x y \<or> kle n y x"
proof (cases "y = a'")
case True
@@ -2528,7 +2916,7 @@
case False
then show ?thesis
apply (rule_tac ksimplexD(6)[OF assms(1),rule_format])
- using x y `y\<noteq>a'`
+ using x y `y \<noteq> a'`
apply auto
done
qed
@@ -2537,25 +2925,33 @@
then have "insert a' (s - {a}) \<in> ?A"
unfolding mem_Collect_eq
apply -
- apply (rule, assumption)
+ apply rule
+ apply assumption
apply (rule_tac x = "a'" in bexI)
using aa' `a' \<notin> s`
apply auto
done
moreover
- have "s \<in> ?A" using assms(1,2) by auto
- ultimately have "?A \<supseteq> {s, insert a' (s - {a})}" by auto
+ 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
+ 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
- then have uv': "\<not> kle n v u" using uv using kle_antisym by auto
- have "u \<noteq> a" "v \<noteq> a" unfolding fun_eq_iff k(2) l(2) by auto
- then have uvs': "u \<in> s'" "v \<in> s'" using `u \<in> s` `v \<in> s` using a'' by auto
+ have "u \<noteq> v"
+ unfolding fun_eq_iff unfolding l(2) k(2) by auto
+ then have uv': "\<not> kle n v u"
+ using uv using kle_antisym by auto
+ have "u \<noteq> a" "v \<noteq> a"
+ unfolding fun_eq_iff k(2) l(2) by auto
+ then have uvs': "u \<in> s'" "v \<in> s'"
+ using `u \<in> s` `v \<in> s` using a'' by auto
have lem6: "a \<in> s' \<or> a' \<in> s'"
proof (cases "\<forall>x\<in>s'. kle n x u \<or> kle n v x")
case False
@@ -2564,7 +2960,8 @@
using ksimplexD(6)[OF as] uvs' by auto
then have "w = a' \<or> w = a"
using uxv[of w] uvs' w by auto
- then show ?thesis using w by auto
+ then show ?thesis
+ using w by auto
next
case True
have "\<not> (\<forall>x\<in>s'. kle n x u)"
@@ -2572,42 +2969,48 @@
apply (rule_tac x=v in bexI)
using uv `u \<noteq> v`
unfolding kle_antisym [of n u v,symmetric]
- using `v\<in>s'`
+ using `v \<in> s'`
apply auto
done
then have "\<exists>y\<in>s'. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then u j + 1 else u j)"
- using ksimplex_successor[OF as `u\<in>s'`] by blast
+ 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 rule
+ apply (drule kle_imp_pointwise)
apply (erule_tac x = kk in allE)
unfolding kk
apply auto
done
then have *: "kle n v w"
- using True[rule_format,OF w(1)] by auto
+ using True[rule_format,OF w(1)]
+ by auto
then have False
- proof (cases "kk \<noteq> l")
- case True
+ proof (cases "kk = l")
+ case False
then show False using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)]
apply (erule_tac x=l in allE)
using `k \<noteq> l`
apply auto
done
next
- case False
+ case True
then have "kk \<noteq> k" using `k \<noteq> l` by auto
- then show False using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)]
+ then show False
+ using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)]
apply (erule_tac x=k in allE)
using `k \<noteq> l`
apply auto
done
qed
- then show ?thesis by auto
+ then show ?thesis
+ by auto
qed
- then show "s' \<in> {s, insert a' (s - {a})}" proof(cases "a\<in>s'")
+ then show "s' \<in> {s, insert a' (s - {a})}"
+ proof (cases "a \<in> s'")
case True
then have "s' = s"
apply -
@@ -2615,38 +3018,46 @@
using a'' `a \<in> s`
apply auto
done
- then show ?thesis by auto
+ then show ?thesis
+ by auto
next
- case False then have "a'\<in>s'" using lem6 by auto
+ case False
+ then have "a' \<in> s'"
+ using lem6 by auto
then have "s' = insert a' (s - {a})"
apply -
apply (rule lem1[of _ a'' _ a'])
- unfolding a''(2)[symmetric] using a'' and `a'\<notin>s` by auto
- then show ?thesis by auto
+ unfolding a''(2)[symmetric]
+ using a'' and `a' \<notin> s`
+ by auto
+ then show ?thesis
+ by auto
qed
qed
- ultimately have *: "?A = {s, insert a' (s - {a})}" by blast
- have "s \<noteq> insert a' (s - {a})" using `a'\<notin>s` by auto
- then have ?thesis unfolding * by auto
+ ultimately have *: "?A = {s, insert a' (s - {a})}"
+ by blast
+ have "s \<noteq> insert a' (s - {a})"
+ using `a'\<notin>s` by auto
+ then have ?thesis
+ unfolding * by auto
}
- ultimately show ?thesis by auto
+ ultimately show ?thesis
+ by auto
qed
-subsection {* Hence another step towards concreteness. *}
+text {* Hence another step towards concreteness. *}
lemma kuhn_simplex_lemma:
- assumes "\<forall>s. ksimplex p (n + 1) s \<longrightarrow> (rl ` s \<subseteq>{0..n+1})"
- "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} })"
+ assumes "\<forall>s. ksimplex p (n + 1) s \<longrightarrow> rl ` s \<subseteq> {0..n+1}"
+ and "odd (card {f. \<exists>s a. ksimplex p (n + 1) s \<and> a \<in> s \<and> (f = s - {a}) \<and>
+ rl ` f = {0 .. n} \<and> ((\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = p))})"
+ shows "odd (card {s \<in> {s. ksimplex p (n + 1) s}. rl ` s = {0..n+1}})"
proof -
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))})"
+ 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
@@ -2654,10 +3065,13 @@
apply (rule kuhn_complete_lemma[OF finite_simplices])
prefer 6
apply (rule *)
- apply (rule, rule, rule)
+ apply rule
+ apply rule
+ apply rule
apply (subst ksimplex_def)
defer
- apply (rule, rule assms(1)[rule_format])
+ apply rule
+ apply (rule assms(1)[rule_format])
unfolding mem_Collect_eq
apply assumption
apply default+
@@ -2672,7 +3086,7 @@
unfolding mem_Collect_eq
proof -
fix f s a
- assume as: "ksimplex p (n + 1) s" "a\<in>s" "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
@@ -2711,23 +3125,25 @@
qed
-subsection {* Reduced labelling. *}
+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>
+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)))"
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)
+ 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 (erule exE)
+ apply (rule_tac x=x in exI)
apply auto
done
- have *: "n \<le> n \<and> (label x (n + 1) \<noteq> 0 \<or> n = n)" by auto
+ 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)
@@ -2738,10 +3154,11 @@
defer
proof (rule, rule)
fix i
- assume i: "1\<le>i \<and> i<N+1"
+ assume i: "1 \<le> i \<and> i < N + 1"
then show "label x i = 0"
using N[THEN conjunct2,THEN spec[where x="i - 1"]]
- using N by auto
+ using N
+ by auto
qed (insert N, auto)
show ?t1 ?t2 ?t3
unfolding reduced_def
@@ -2754,7 +3171,8 @@
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)"
+ and "\<forall>i. 1 \<le> i \<and> i < r + 1 \<longrightarrow> label x i = 0"
+ and "r = n \<or> label x (r + 1) \<noteq> 0"
shows "reduced label n x = r"
apply (rule le_antisym)
apply (rule_tac[!] ccontr)
@@ -2765,13 +3183,16 @@
done
lemma reduced_labelling_zero:
- assumes "j\<in>{1..n}" "label x j = 0"
+ assumes "j \<in> {1..n}"
+ and "label x j = 0"
shows "reduced label n x \<noteq> j - 1"
using reduced_labelling[of label n x]
- using assms by fastforce
+ using assms
+ by fastforce
lemma reduced_labelling_nonzero:
- assumes "j\<in>{1..n}" "label x j \<noteq> 0"
+ assumes "j\<in>{1..n}"
+ and "label x j \<noteq> 0"
shows "reduced label n x < j"
using assms and reduced_labelling[of label n x]
apply (erule_tac x=j in allE)
@@ -2789,14 +3210,18 @@
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")
+ and "\<forall>x\<in>f. \<forall>j\<in>{1..n+1}. x j = p \<longrightarrow> lab x j = 1"
+ shows "reduced lab (n + 1) ` f = {0..n} \<and>
+ ((\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = p)) \<longleftrightarrow>
+ reduced lab (n + 1) ` f = {0..n} \<and> (\<forall>x\<in>f. x (n + 1) = p)"
+ (is "?l = ?r")
proof
assume ?l (is "?as \<and> (?a \<or> ?b)")
then show ?r
apply -
- apply (rule, erule conjE, assumption)
+ apply rule
+ apply (erule conjE)
+ apply assumption
proof (cases ?a)
case True
then guess j .. note j = this
@@ -2813,13 +3238,17 @@
apply auto
done
}
- moreover have "j - 1 \<in> {0..n}" using j by auto
+ 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
- then show "\<forall>x\<in>f. x (n + 1) = p" by auto
+ ultimately have False
+ by auto
+ then show "\<forall>x\<in>f. x (n + 1) = p"
+ by auto
next
case False
- then have ?b using `?l` by blast
+ then have ?b using `?l`
+ by blast
then guess j .. note j = this
{
fix x
@@ -2834,35 +3263,45 @@
} note * = this
have "j = n + 1"
proof (rule ccontr)
- case goal1
- then have "j < n + 1" using j by auto
+ assume "\<not> ?thesis"
+ then have "j < n + 1"
+ using j by auto
moreover
- have "n \<in> {0..n}" by auto
+ 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
+ ultimately show False
+ using *[of y] by auto
qed
- then show "\<forall>x\<in>f. x (n + 1) = p" using j by auto
+ then show "\<forall>x\<in>f. x (n + 1) = p"
+ using j by auto
qed
-qed(auto)
+qed auto
-subsection {* Hence we get just about the nice induction. *}
+text {* Hence we get just about the nice induction. *}
lemma kuhn_induction:
- assumes "0 < p" "\<forall>x. \<forall>j\<in>{1..n+1}. (\<forall>j. x j \<le> p) \<and> (x j = 0) \<longrightarrow> (lab x j = 0)"
- "\<forall>x. \<forall>j\<in>{1..n+1}. (\<forall>j. x j \<le> p) \<and> (x j = p) \<longrightarrow> (lab x j = 1)"
- "odd (card {f. ksimplex p n f \<and> ((reduced lab n) ` f = {0..n})})"
- shows "odd (card {s. ksimplex p (n+1) s \<and>((reduced lab (n+1)) ` s = {0..n+1})})"
+ assumes "0 < p"
+ and "\<forall>x. \<forall>j\<in>{1..n+1}. (\<forall>j. x j \<le> p) \<and> x j = 0 \<longrightarrow> lab x j = 0"
+ and "\<forall>x. \<forall>j\<in>{1..n+1}. (\<forall>j. x j \<le> p) \<and> x j = p \<longrightarrow> lab x j = 1"
+ and "odd (card {f. ksimplex p n f \<and> reduced lab n ` f = {0..n}})"
+ shows "odd (card {s. ksimplex p (n + 1) s \<and> reduced lab (n + 1) ` s = {0..n+1}})"
proof -
have *: "\<And>s t. odd (card s) \<Longrightarrow> s = t \<Longrightarrow> odd (card t)"
- "\<And>s f. (\<And>x. f x \<le> n +1 ) \<Longrightarrow> f ` s \<subseteq> {0..n+1}" by auto
+ "\<And>s f. (\<And>x. f x \<le> n + 1) \<Longrightarrow> f ` s \<subseteq> {0..n+1}"
+ by auto
show ?thesis
apply (rule kuhn_simplex_lemma[unfolded mem_Collect_eq])
- apply (rule, rule, rule *, rule reduced_labelling)
+ apply rule
+ apply rule
+ apply (rule *)
+ apply (rule reduced_labelling)
apply (rule *(1)[OF assms(4)])
apply (rule set_eqI)
unfolding mem_Collect_eq
- apply (rule, erule conjE)
+ apply rule
+ apply (erule conjE)
defer
apply rule
proof -
@@ -2870,16 +3309,22 @@
assume as: "ksimplex p n f" "reduced lab n ` f = {0..n}"
have *: "\<forall>x\<in>f. \<forall>j\<in>{1..n + 1}. x j = 0 \<longrightarrow> lab x j = 0"
"\<forall>x\<in>f. \<forall>j\<in>{1..n + 1}. x j = p \<longrightarrow> lab x j = 1"
- using assms(2-3) using as(1)[unfolded ksimplex_def] by auto
+ using assms(2-3)
+ using as(1)[unfolded ksimplex_def]
+ by auto
have allp: "\<forall>x\<in>f. x (n + 1) = p"
- using assms(2) using as(1)[unfolded ksimplex_def] by auto
+ using assms(2)
+ using as(1)[unfolded ksimplex_def]
+ by auto
{
fix x
assume "x \<in> f"
then have "reduced lab (n + 1) x < n + 1"
apply -
apply (rule reduced_labelling_nonzero)
- defer using assms(3) using as(1)[unfolded ksimplex_def]
+ defer
+ using assms(3)
+ using as(1)[unfolded ksimplex_def]
apply auto
done
then have "reduced lab (n + 1) x = reduced lab n x"
@@ -2911,11 +3356,7 @@
assume as: "\<exists>s a. ksimplex p (n + 1) s \<and>
a \<in> s \<and> f = s - {a} \<and> reduced lab (n + 1) ` f = {0..n} \<and> ((\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p))" (is ?ex)
then guess s ..
- then guess a
- apply -
- apply (erule exE,(erule conjE)+)
- done
- note sa = this
+ then guess a by (elim exE conjE) note sa = this
{
fix x
assume "x \<in> f"
@@ -2951,19 +3392,22 @@
apply auto
done
moreover
- have "j - 1 \<in> {0..n}" using `j\<in>{1..n+1}` by auto
+ have "j - 1 \<in> {0..n}"
+ using `j\<in>{1..n+1}` by auto
ultimately have False
unfolding sa(4)[symmetric]
unfolding image_iff
by fastforce
- then show ?thesis by auto
+ then show ?thesis
+ by auto
next
case False
then have "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p"
using sa(5) by fastforce then guess j .. note j=this
then show ?thesis
proof (cases "j = n + 1")
- case False then have *: "j \<in> {1..n}"
+ case False
+ then have *: "j \<in> {1..n}"
using j by auto
then have "\<And>x. x \<in> f \<Longrightarrow> reduced lab n x < j"
apply (rule reduced_labelling_nonzero)
@@ -2978,58 +3422,72 @@
unfolding sa
apply auto
done
- then show "lab x j \<noteq> 0" by auto
+ then show "lab x j \<noteq> 0"
+ by auto
qed
- moreover have "j \<in> {0..n}" using * by auto
+ moreover have "j \<in> {0..n}"
+ using * by auto
ultimately have False
unfolding part1[symmetric]
using * unfolding image_iff
by auto
- then show ?thesis by auto
+ then show ?thesis
+ by auto
qed auto
qed
then show "ksimplex p n f"
- using as unfolding simplex_top_face[OF assms(1) *,symmetric] by auto
+ using as
+ unfolding simplex_top_face[OF assms(1) *,symmetric]
+ by auto
qed
qed
lemma kuhn_induction_Suc:
- assumes "0 < p" "\<forall>x. \<forall>j\<in>{1..Suc n}. (\<forall>j. x j \<le> p) \<and> (x j = 0) \<longrightarrow> (lab x j = 0)"
- "\<forall>x. \<forall>j\<in>{1..Suc n}. (\<forall>j. x j \<le> p) \<and> (x j = p) \<longrightarrow> (lab x j = 1)"
- "odd (card {f. ksimplex p n f \<and> ((reduced lab n) ` f = {0..n})})"
- shows "odd (card {s. ksimplex p (Suc n) s \<and>((reduced lab (Suc n)) ` s = {0..Suc n})})"
- using assms unfolding Suc_eq_plus1 by(rule kuhn_induction)
+ assumes "0 < p"
+ and "\<forall>x. \<forall>j\<in>{1..Suc n}. (\<forall>j. x j \<le> p) \<and> x j = 0 \<longrightarrow> lab x j = 0"
+ and "\<forall>x. \<forall>j\<in>{1..Suc n}. (\<forall>j. x j \<le> p) \<and> x j = p \<longrightarrow> lab x j = 1"
+ and "odd (card {f. ksimplex p n f \<and> reduced lab n ` f = {0..n}})"
+ shows "odd (card {s. ksimplex p (Suc n) s \<and> reduced lab (Suc n) ` s = {0..Suc n}})"
+ using assms
+ unfolding Suc_eq_plus1
+ by (rule kuhn_induction)
-subsection {* And so we get the final combinatorial result. *}
+text {* And so we get the final combinatorial result. *}
-lemma ksimplex_0: "ksimplex p 0 s \<longleftrightarrow> s = {(\<lambda>x. p)}" (is "?l = ?r")
+lemma ksimplex_0: "ksimplex p 0 s \<longleftrightarrow> s = {(\<lambda>x. p)}"
+ (is "?l = ?r")
proof
assume l: ?l
guess a using ksimplexD(3)[OF l, unfolded add_0] unfolding card_1_exists .. note a = this
have "a = (\<lambda>x. p)"
- using ksimplexD(5)[OF l, rule_format, OF a(1)] by rule auto
- then show ?r using a by auto
+ using ksimplexD(5)[OF l, rule_format, OF a(1)]
+ by rule auto
+ then show ?r
+ using a by auto
next
assume r: ?r
- show ?l unfolding r ksimplex_eq by auto
+ show ?l
+ unfolding r ksimplex_eq by auto
qed
lemma reduce_labelling_zero[simp]: "reduced lab 0 x = 0"
by (rule reduced_labelling_unique) auto
lemma kuhn_combinatorial:
- assumes "0 < p" "\<forall>x j. (\<forall>j. x(j) \<le> p) \<and> 1 \<le> j \<and> j \<le> n \<and> (x j = 0) \<longrightarrow> (lab x j = 0)"
- "\<forall>x j. (\<forall>j. x(j) \<le> p) \<and> 1 \<le> j \<and> j \<le> n \<and> (x j = p) \<longrightarrow> (lab x j = 1)"
- shows " odd (card {s. ksimplex p n s \<and> ((reduced lab n) ` s = {0..n})})"
+ assumes "0 < p"
+ and "\<forall>x j. (\<forall>j. x j \<le> p) \<and> 1 \<le> j \<and> j \<le> n \<and> x j = 0 \<longrightarrow> lab x j = 0"
+ and "\<forall>x j. (\<forall>j. x j \<le> p) \<and> 1 \<le> j \<and> j \<le> n \<and> x j = p \<longrightarrow> lab x j = 1"
+ shows "odd (card {s. ksimplex p n s \<and> reduced lab n ` s = {0..n}})"
using assms
proof (induct n)
- let ?M = "\<lambda>n. {s. ksimplex p n s \<and> ((reduced lab n) ` s = {0..n})}"
+ let ?M = "\<lambda>n. {s. ksimplex p n s \<and> reduced lab n ` s = {0..n}}"
{
case 0
- have *: "?M 0 = {{(\<lambda>x. p)}}"
+ have *: "?M 0 = {{\<lambda>x. p}}"
unfolding ksimplex_0 by auto
- show ?case unfolding * by auto
+ show ?case
+ unfolding * by auto
next
case (Suc n)
have "odd (card (?M n))"
@@ -3047,18 +3505,22 @@
qed
lemma kuhn_lemma:
- assumes "0 < (p::nat)" "0 < (n::nat)"
- "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. (label x i = (0::nat)) \<or> (label x i = 1))"
- "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. (x i = 0) \<longrightarrow> (label x i = 0))"
- "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. (x i = p) \<longrightarrow> (label x i = 1))"
+ fixes n p :: nat
+ assumes "0 < p"
+ and "0 < n"
+ and "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. label x i = (0::nat) \<or> label x i = 1)"
+ and "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. x i = 0 \<longrightarrow> label x i = 0)"
+ and "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. x i = p \<longrightarrow> label x i = 1)"
obtains q where "\<forall>i\<in>{1..n}. q i < p"
- "\<forall>i\<in>{1..n}. \<exists>r s. (\<forall>j\<in>{1..n}. q(j) \<le> r(j) \<and> r(j) \<le> q(j) + 1) \<and>
- (\<forall>j\<in>{1..n}. q(j) \<le> s(j) \<and> s(j) \<le> q(j) + 1) \<and>
- ~(label r i = label s i)"
+ and "\<forall>i\<in>{1..n}. \<exists>r s.
+ (\<forall>j\<in>{1..n}. q j \<le> r j \<and> r j \<le> q j + 1) \<and>
+ (\<forall>j\<in>{1..n}. q j \<le> s j \<and> s j \<le> q j + 1) \<and>
+ label r i \<noteq> label s i"
proof -
let ?A = "{s. ksimplex p n s \<and> reduced label n ` s = {0..n}}"
- have "n \<noteq> 0" using assms by auto
- have conjD:"\<And>P Q. P \<and> Q \<Longrightarrow> P" "\<And>P Q. P \<and> Q \<Longrightarrow> Q"
+ have "n \<noteq> 0"
+ using assms by auto
+ have conjD: "\<And>P Q. P \<and> Q \<Longrightarrow> P" "\<And>P Q. P \<and> Q \<Longrightarrow> Q"
by auto
have "odd (card ?A)"
apply (rule kuhn_combinatorial[of p n label])
@@ -3070,16 +3532,17 @@
apply (rule ccontr)
apply auto
done
- then have "?A \<noteq> {}" unfolding card_eq_0_iff by auto
+ then have "?A \<noteq> {}"
+ unfolding card_eq_0_iff by auto
then obtain s where "s \<in> ?A"
by auto note s=conjD[OF this[unfolded mem_Collect_eq]]
- guess a b by (rule ksimplex_extrema_strong[OF s(1) `n\<noteq>0`]) note ab = this
+ guess a b by (rule ksimplex_extrema_strong[OF s(1) `n \<noteq> 0`]) note ab = this
show ?thesis
apply (rule that[of a])
apply (rule_tac[!] ballI)
proof -
fix i
- assume "i\<in>{1..n}"
+ assume "i \<in> {1..n}"
then have "a i + 1 \<le> p"
apply -
apply (rule order_trans[of _ "b i"])
@@ -3091,10 +3554,12 @@
apply (drule_tac bspec[OF _ ab(2)])+
apply auto
done
- then show "a i < p" by auto
+ then show "a i < p"
+ by auto
next
case goal2
- then have "i \<in> reduced label n ` s" using s by auto
+ then have "i \<in> reduced label n ` s"
+ using s by auto
then guess u unfolding image_iff .. note u = this
from goal2 have "i - 1 \<in> reduced label n ` s"
using s by auto
@@ -3116,7 +3581,7 @@
done
fix j
assume j: "j \<in> {1..n}"
- show "a j \<le> u j \<and> u j \<le> a j + 1" "a j \<le> v j \<and> v j \<le> a j + 1"
+ show "a j \<le> u j \<and> u j \<le> a j + 1" and "a j \<le> v j \<and> v j \<le> a j + 1"
using conjD[OF ab(4)[rule_format, OF u(1)]]
and conjD[OF ab(4)[rule_format, OF v(1)]]
apply -
@@ -3131,38 +3596,45 @@
qed
-subsection {* The main result for the unit cube. *}
+subsection {* The main result for the unit cube *}
lemma kuhn_labelling_lemma':
- assumes "(\<forall>x::nat\<Rightarrow>real. P x \<longrightarrow> P (f x))" "\<forall>x. P x \<longrightarrow> (\<forall>i::nat. Q i \<longrightarrow> 0 \<le> x i \<and> x i \<le> 1)"
+ assumes "(\<forall>x::nat\<Rightarrow>real. P x \<longrightarrow> P (f x))"
+ and "\<forall>x. P x \<longrightarrow> (\<forall>i::nat. Q i \<longrightarrow> 0 \<le> x i \<and> x i \<le> 1)"
shows "\<exists>l. (\<forall>x i. l x i \<le> (1::nat)) \<and>
- (\<forall>x i. P x \<and> Q i \<and> (x i = 0) \<longrightarrow> (l x i = 0)) \<and>
- (\<forall>x i. P x \<and> Q i \<and> (x i = 1) \<longrightarrow> (l x i = 1)) \<and>
- (\<forall>x i. P x \<and> Q i \<and> (l x i = 0) \<longrightarrow> x i \<le> f(x) i) \<and>
- (\<forall>x i. P x \<and> Q i \<and> (l x i = 1) \<longrightarrow> f(x) i \<le> x i)"
+ (\<forall>x i. P x \<and> Q i \<and> x i = 0 \<longrightarrow> l x i = 0) \<and>
+ (\<forall>x i. P x \<and> Q i \<and> x i = 1 \<longrightarrow> l x i = 1) \<and>
+ (\<forall>x i. P x \<and> Q i \<and> l x i = 0 \<longrightarrow> x i \<le> f x i) \<and>
+ (\<forall>x i. P x \<and> Q i \<and> l x i = 1 \<longrightarrow> f x i \<le> x i)"
proof -
- have and_forall_thm: "\<And>P Q. (\<forall>x. P x) \<and> (\<forall>x. Q x) \<longleftrightarrow> (\<forall>x. P x \<and> Q x)" by auto
- have *: "\<forall>x y::real. 0 \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1 \<longrightarrow> (x \<noteq> 1 \<and> x \<le> y \<or> x \<noteq> 0 \<and> y \<le> x)"
+ have and_forall_thm: "\<And>P Q. (\<forall>x. P x) \<and> (\<forall>x. Q x) \<longleftrightarrow> (\<forall>x. P x \<and> Q x)"
+ by auto
+ have *: "\<forall>x y::real. 0 \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1 \<longrightarrow> x \<noteq> 1 \<and> x \<le> y \<or> x \<noteq> 0 \<and> y \<le> x"
by auto
show ?thesis
unfolding and_forall_thm
apply (subst choice_iff[symmetric])+
- proof (rule, rule)
+ apply rule
+ apply rule
+ proof -
case goal1
- let ?R = "\<lambda>y. (P x \<and> Q xa \<and> x xa = 0 \<longrightarrow> y = (0::nat)) \<and>
+ let ?R = "\<lambda>y::nat.
+ (P x \<and> Q xa \<and> x xa = 0 \<longrightarrow> y = 0) \<and>
(P x \<and> Q xa \<and> x xa = 1 \<longrightarrow> y = 1) \<and>
(P x \<and> Q xa \<and> y = 0 \<longrightarrow> x xa \<le> (f x) xa) \<and>
(P x \<and> Q xa \<and> y = 1 \<longrightarrow> (f x) xa \<le> x xa)"
{
- assume "P x" "Q xa"
- then have "0 \<le> (f x) xa \<and> (f x) xa \<le> 1"
+ assume "P x" and "Q xa"
+ then have "0 \<le> f x xa \<and> f x xa \<le> 1"
using assms(2)[rule_format,of "f x" xa]
apply (drule_tac assms(1)[rule_format])
apply auto
done
}
- then have "?R 0 \<or> ?R 1" by auto
- then show ?case by auto
+ then have "?R 0 \<or> ?R 1"
+ by auto
+ then show ?case
+ by auto
qed
qed
@@ -3193,22 +3665,26 @@
abs (f x \<bullet> i - x \<bullet> i) \<le> norm (f y - f x) + norm (y - x)"
proof safe
fix x y :: 'a
- assume x: "x\<in>{0..\<Sum>Basis}"
- assume y: "y\<in>{0..\<Sum>Basis}"
+ assume x: "x \<in> {0..\<Sum>Basis}"
+ assume y: "y \<in> {0..\<Sum>Basis}"
fix i
assume i: "label x i \<noteq> label y i" "i \<in> Basis"
have *: "\<And>x y fx fy :: real. x \<le> fx \<and> fy \<le> y \<or> fx \<le> x \<and> y \<le> fy \<Longrightarrow>
abs (fx - x) \<le> abs (fy - fx) + abs (y - x)" by auto
- have "\<bar>(f x - x) \<bullet> i\<bar> \<le> abs((f y - f x)\<bullet>i) + abs((y - x)\<bullet>i)"
+ have "\<bar>(f x - x) \<bullet> i\<bar> \<le> abs ((f y - f x)\<bullet>i) + abs ((y - x)\<bullet>i)"
unfolding inner_simps
apply (rule *)
apply (cases "label x i = 0")
- apply (rule disjI1, rule)
+ apply (rule disjI1)
+ apply rule
prefer 3
- proof (rule disjI2, rule)
+ apply (rule disjI2)
+ apply rule
+ proof -
assume lx: "label x i = 0"
then have ly: "label y i = 1"
- using i label(1)[of i y] by auto
+ using i label(1)[of i y]
+ by auto
show "x \<bullet> i \<le> f x \<bullet> i"
apply (rule label(4)[rule_format])
using x y lx i(2)
@@ -3221,8 +3697,9 @@
done
next
assume "label x i \<noteq> 0"
- then have l:"label x i = 1" "label y i = 0"
- using i label(1)[of i x] label(1)[of i y] by auto
+ then have l: "label x i = 1" "label y i = 0"
+ using i label(1)[of i x] label(1)[of i y]
+ by auto
show "f x \<bullet> i \<le> x \<bullet> i"
apply (rule label(5)[rule_format])
using x y l i(2)
@@ -3242,11 +3719,13 @@
unfolding inner_simps .
qed
have "\<exists>e>0. \<forall>x\<in>{0..\<Sum>Basis}. \<forall>y\<in>{0..\<Sum>Basis}. \<forall>z\<in>{0..\<Sum>Basis}. \<forall>i\<in>Basis.
- norm(x - z) < e \<and> norm(y - z) < e \<and> label x i \<noteq> label y i \<longrightarrow> abs((f(z) - z)\<bullet>i) < d / (real n)"
+ norm (x - z) < e \<and> norm (y - z) < e \<and> label x i \<noteq> label y i \<longrightarrow>
+ abs ((f(z) - z)\<bullet>i) < d / (real n)"
proof -
- have d':"d / real n / 8 > 0"
+ have d': "d / real n / 8 > 0"
apply (rule divide_pos_pos)+
- using d(1) unfolding n_def
+ using d(1)
+ unfolding n_def
apply (auto simp: DIM_positive)
done
have *: "uniformly_continuous_on {0..\<Sum>Basis} f"
@@ -3260,25 +3739,32 @@
show "0 < min (e / 2) (d / real n / 8)"
using d' e by auto
fix x y z i
- assume as: "x \<in> {0..\<Sum>Basis}" "y \<in> {0..\<Sum>Basis}" "z \<in> {0..\<Sum>Basis}"
+ assume as:
+ "x \<in> {0..\<Sum>Basis}" "y \<in> {0..\<Sum>Basis}" "z \<in> {0..\<Sum>Basis}"
"norm (x - z) < min (e / 2) (d / real n / 8)"
- "norm (y - z) < min (e / 2) (d / real n / 8)" "label x i \<noteq> label y i"
- and i: "i \<in> Basis"
+ "norm (y - z) < min (e / 2) (d / real n / 8)"
+ "label x i \<noteq> label y i"
+ assume i: "i \<in> Basis"
have *: "\<And>z fz x fx n1 n2 n3 n4 d4 d :: real. abs(fx - x) \<le> n1 + n2 \<Longrightarrow>
- abs(fx - fz) \<le> n3 \<Longrightarrow> abs(x - z) \<le> n4 \<Longrightarrow>
+ abs (fx - fz) \<le> n3 \<Longrightarrow> abs (x - z) \<le> n4 \<Longrightarrow>
n1 < d4 \<Longrightarrow> n2 < 2 * d4 \<Longrightarrow> n3 < d4 \<Longrightarrow> n4 < d4 \<Longrightarrow>
- (8 * d4 = d) \<Longrightarrow> abs(fz - z) < d" by auto
- show "\<bar>(f z - z) \<bullet> i\<bar> < d / real n" unfolding inner_simps
+ (8 * d4 = d) \<Longrightarrow> abs(fz - z) < d"
+ by auto
+ show "\<bar>(f z - z) \<bullet> i\<bar> < d / real n"
+ unfolding inner_simps
proof (rule *)
show "\<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y -f x) + norm (y - x)"
apply (rule lem1[rule_format])
- using as i apply auto
+ using as i
+ apply auto
done
show "\<bar>f x \<bullet> i - f z \<bullet> i\<bar> \<le> norm (f x - f z)" "\<bar>x \<bullet> i - z \<bullet> i\<bar> \<le> norm (x - z)"
- unfolding inner_diff_left[symmetric] by(rule Basis_le_norm[OF i])+
- have tria:"norm (y - x) \<le> norm (y - z) + norm (x - z)"
+ unfolding inner_diff_left[symmetric]
+ by (rule Basis_le_norm[OF i])+
+ have tria: "norm (y - x) \<le> norm (y - z) + norm (x - z)"
using dist_triangle[of y x z, unfolded dist_norm]
- unfolding norm_minus_commute by auto
+ unfolding norm_minus_commute
+ by auto
also have "\<dots> < e / 2 + e / 2"
apply (rule add_strict_mono)
using as(4,5)
@@ -3295,7 +3781,9 @@
using as
apply auto
done
- then show "norm (y - x) < 2 * (d / real n / 8)" using tria by auto
+ then show "norm (y - x) < 2 * (d / real n / 8)"
+ using tria
+ by auto
show "norm (f x - f z) < d / real n / 8"
apply (rule e(2))
using as e(1)
@@ -3313,7 +3801,8 @@
using e(1) n
apply auto
done
- then have "p > 0" using p by auto
+ then have "p > 0"
+ using p by auto
obtain b :: "nat \<Rightarrow> 'a" where b: "bij_betw b {1..n} Basis"
by atomize_elim (auto simp: n_def intro!: finite_same_card_bij)
@@ -3323,71 +3812,98 @@
then have b'_Basis: "\<And>i. i \<in> Basis \<Longrightarrow> b' i \<in> {Suc 0 .. n}"
unfolding bij_betw_def by (auto simp: set_eq_iff)
have bb'[simp]:"\<And>i. i \<in> Basis \<Longrightarrow> b (b' i) = i"
- unfolding b'_def using b by (auto simp: f_inv_into_f bij_betw_def)
+ unfolding b'_def
+ using b
+ by (auto simp: f_inv_into_f bij_betw_def)
have b'b[simp]:"\<And>i. i \<in> {1..n} \<Longrightarrow> b' (b i) = i"
- unfolding b'_def using b by (auto simp: inv_into_f_eq bij_betw_def)
- have *: "\<And>x :: nat. x=0 \<or> x=1 \<longleftrightarrow> x\<le>1" by auto
+ unfolding b'_def
+ using b
+ by (auto simp: inv_into_f_eq bij_betw_def)
+ have *: "\<And>x :: nat. x = 0 \<or> x = 1 \<longleftrightarrow> x \<le> 1"
+ by auto
have b'': "\<And>j. j \<in> {Suc 0..n} \<Longrightarrow> b j \<in> Basis"
using b unfolding bij_betw_def by auto
have q1: "0 < p" "0 < n" "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow>
(\<forall>i\<in>{1..n}. (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0 \<or>
(label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 1)"
- unfolding * using `p>0` `n>0` using label(1)[OF b''] by auto
+ unfolding *
+ using `p > 0` `n > 0`
+ using label(1)[OF b'']
+ by auto
have q2: "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. x i = 0 \<longrightarrow>
(label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0)"
"\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. x i = p \<longrightarrow>
(label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 1)"
- apply (rule, rule, rule, rule)
+ apply rule
+ apply rule
+ apply rule
+ apply rule
defer
- proof (rule, rule, rule, rule)
+ apply rule
+ apply rule
+ apply rule
+ apply rule
+ proof -
fix x i
assume as: "\<forall>i\<in>{1..n}. x i \<le> p" "i \<in> {1..n}"
{
assume "x i = p \<or> x i = 0"
have "(\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<in> {0::'a..\<Sum>Basis}"
- unfolding mem_interval using as b'_Basis
+ unfolding mem_interval
+ using as b'_Basis
by (auto simp add: inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1)
}
note cube = this
{
assume "x i = p"
then show "(label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 1"
- unfolding o_def using cube as `p>0`
+ unfolding o_def
+ using cube as `p > 0`
by (intro label(3)) (auto simp add: b'')
}
{
assume "x i = 0"
then show "(label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0"
- unfolding o_def using cube as `p>0`
+ unfolding o_def using cube as `p > 0`
by (intro label(2)) (auto simp add: b'')
}
qed
guess q by (rule kuhn_lemma[OF q1 q2]) note q = this
def z \<equiv> "(\<Sum>i\<in>Basis. (real (q (b' i)) / real p) *\<^sub>R i)::'a"
- have "\<exists>i\<in>Basis. d / real n \<le> abs((f z - z)\<bullet>i)"
+ have "\<exists>i\<in>Basis. d / real n \<le> abs ((f z - z)\<bullet>i)"
proof (rule ccontr)
have "\<forall>i\<in>Basis. q (b' i) \<in> {0..p}"
- using q(1) b' by (auto intro: less_imp_le simp: bij_betw_def)
- then have "z\<in>{0..\<Sum>Basis}"
- unfolding z_def mem_interval using b'_Basis
+ using q(1) b'
+ by (auto intro: less_imp_le simp: bij_betw_def)
+ then have "z \<in> {0..\<Sum>Basis}"
+ unfolding z_def mem_interval
+ using b'_Basis
by (auto simp add: inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1)
- then have d_fz_z:"d \<le> norm (f z - z)" by (rule d)
- case goal1
+ then have d_fz_z: "d \<le> norm (f z - z)"
+ by (rule d)
+ assume "\<not> ?thesis"
then have as: "\<forall>i\<in>Basis. \<bar>f z \<bullet> i - z \<bullet> i\<bar> < d / real n"
- using `n > 0` by (auto simp add: not_le inner_simps)
+ using `n > 0`
+ by (auto simp add: not_le inner_simps)
have "norm (f z - z) \<le> (\<Sum>i\<in>Basis. \<bar>f z \<bullet> i - z \<bullet> i\<bar>)"
- unfolding inner_diff_left[symmetric] by(rule norm_le_l1)
+ unfolding inner_diff_left[symmetric]
+ by (rule norm_le_l1)
also have "\<dots> < (\<Sum>(i::'a) \<in> Basis. d / real n)"
apply (rule setsum_strict_mono)
- using as apply auto
+ using as
+ apply auto
done
also have "\<dots> = d"
- using DIM_positive[where 'a='a] by (auto simp: real_eq_of_nat n_def)
- finally show False using d_fz_z by auto
+ using DIM_positive[where 'a='a]
+ by (auto simp: real_eq_of_nat n_def)
+ finally show False
+ using d_fz_z by auto
qed
then guess i .. note i = this
have *: "b' i \<in> {1..n}"
- using i using b'[unfolded bij_betw_def] by auto
+ using i
+ using b'[unfolded bij_betw_def]
+ by auto
guess r using q(2)[rule_format,OF *] ..
then guess s by (elim exE conjE) note rs = this[rule_format]
have b'_im: "\<And>i. i \<in> Basis \<Longrightarrow> b' i \<in> {1..n}"
@@ -3400,59 +3916,68 @@
apply (auto simp add: Suc_le_eq)
done
then have "r' \<in> {0..\<Sum>Basis}"
- unfolding r'_def mem_interval using b'_Basis
+ unfolding r'_def mem_interval
+ using b'_Basis
by (auto simp add: inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1)
def s' \<equiv> "(\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i)::'a"
- have "\<And>i. i\<in>Basis \<Longrightarrow> s (b' i) \<le> p"
+ have "\<And>i. i \<in> Basis \<Longrightarrow> s (b' i) \<le> p"
apply (rule order_trans)
apply (rule rs(2)[OF b'_im, THEN conjunct2])
using q(1)[rule_format,OF b'_im]
apply (auto simp add: Suc_le_eq)
done
then have "s' \<in> {0..\<Sum>Basis}"
- unfolding s'_def mem_interval using b'_Basis
+ unfolding s'_def mem_interval
+ using b'_Basis
by (auto simp add: inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1)
have "z \<in> {0..\<Sum>Basis}"
- unfolding z_def mem_interval using b'_Basis q(1)[rule_format,OF b'_im] `p>0`
+ unfolding z_def mem_interval
+ using b'_Basis q(1)[rule_format,OF b'_im] `p > 0`
by (auto simp add: inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1 less_imp_le)
- have *: "\<And>x. 1 + real x = real (Suc x)" by auto
- { have "(\<Sum>i\<in>Basis. \<bar>real (r (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
+ have *: "\<And>x. 1 + real x = real (Suc x)"
+ by auto
+ {
+ have "(\<Sum>i\<in>Basis. \<bar>real (r (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
apply (rule setsum_mono)
using rs(1)[OF b'_im]
apply (auto simp add:* field_simps)
done
- also have "\<dots> < e * real p" using p `e>0` `p>0`
+ also have "\<dots> < e * real p"
+ using p `e > 0` `p > 0`
by (auto simp add: field_simps n_def real_of_nat_def)
finally have "(\<Sum>i\<in>Basis. \<bar>real (r (b' i)) - real (q (b' i))\<bar>) < e * real p" .
}
moreover
- { have "(\<Sum>i\<in>Basis. \<bar>real (s (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
+ {
+ have "(\<Sum>i\<in>Basis. \<bar>real (s (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
apply (rule setsum_mono)
using rs(2)[OF b'_im]
apply (auto simp add:* field_simps)
done
- also have "\<dots> < e * real p" using p `e > 0` `p > 0`
+ also have "\<dots> < e * real p"
+ using p `e > 0` `p > 0`
by (auto simp add: field_simps n_def real_of_nat_def)
finally have "(\<Sum>i\<in>Basis. \<bar>real (s (b' i)) - real (q (b' i))\<bar>) < e * real p" .
}
ultimately
- have "norm (r' - z) < e" "norm (s' - z) < e"
+ have "norm (r' - z) < e" and "norm (s' - z) < e"
unfolding r'_def s'_def z_def
- using `p>0`
+ using `p > 0`
apply (rule_tac[!] le_less_trans[OF norm_le_l1])
apply (auto simp add: field_simps setsum_divide_distrib[symmetric] inner_diff_left)
done
then have "\<bar>(f z - z) \<bullet> i\<bar> < d / real n"
- using rs(3) i unfolding r'_def[symmetric] s'_def[symmetric] o_def bb'
+ using rs(3) i
+ unfolding r'_def[symmetric] s'_def[symmetric] o_def bb'
by (intro e(2)[OF `r'\<in>{0..\<Sum>Basis}` `s'\<in>{0..\<Sum>Basis}` `z\<in>{0..\<Sum>Basis}`]) auto
- then show False using i by auto
+ then show False
+ using i by auto
qed
-subsection {* Retractions. *}
+subsection {* Retractions *}
-definition "retraction s t r \<longleftrightarrow>
- t \<subseteq> s \<and> continuous_on s r \<and> (r ` s \<subseteq> t) \<and> (\<forall>x\<in>t. r x = x)"
+definition "retraction s t r \<longleftrightarrow> t \<subseteq> s \<and> continuous_on s r \<and> r ` s \<subseteq> t \<and> (\<forall>x\<in>t. r x = x)"
definition retract_of (infixl "retract'_of" 12)
where "(t retract_of s) \<longleftrightarrow> (\<exists>r. retraction s t r)"
@@ -3460,14 +3985,15 @@
lemma retraction_idempotent: "retraction s t r \<Longrightarrow> x \<in> s \<Longrightarrow> r (r x) = r x"
unfolding retraction_def by auto
-subsection {*preservation of fixpoints under (more general notion of) retraction. *}
+subsection {* Preservation of fixpoints under (more general notion of) retraction *}
lemma invertible_fixpoint_property:
fixes s :: "'a::euclidean_space set"
and t :: "'b::euclidean_space set"
assumes "continuous_on t i"
and "i ` t \<subseteq> s"
- and "continuous_on s r" "r ` s \<subseteq> t"
+ and "continuous_on s r"
+ and "r ` s \<subseteq> t"
and "\<forall>y\<in>t. r (i y) = y"
and "\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)"
and "continuous_on t g"
@@ -3475,10 +4001,12 @@
obtains y where "y \<in> t" and "g y = y"
proof -
have "\<exists>x\<in>s. (i \<circ> g \<circ> r) x = x"
- apply (rule assms(6)[rule_format], rule)
+ apply (rule assms(6)[rule_format])
+ apply rule
apply (rule continuous_on_compose assms)+
- apply ((rule continuous_on_subset)?,rule assms)+
- using assms(2,4,8) unfolding image_compose
+ apply ((rule continuous_on_subset)?, rule assms)+
+ using assms(2,4,8)
+ unfolding image_compose
apply auto
apply blast
done
@@ -3518,7 +4046,7 @@
qed
lemma retract_fixpoint_property:
- fixes f :: "'a::euclidean_space => 'b::euclidean_space"
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
and s :: "'a set"
assumes "t retract_of s"
and "\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)"
@@ -3539,7 +4067,7 @@
qed
-subsection {*So the Brouwer theorem for any set with nonempty interior. *}
+subsection {* The Brouwer theorem for any set with nonempty interior *}
lemma brouwer_weak:
fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'a::ordered_euclidean_space"
@@ -3571,13 +4099,13 @@
qed
-subsection {* And in particular for a closed ball. *}
+text {* And in particular for a closed ball. *}
lemma brouwer_ball:
fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'a"
assumes "e > 0"
and "continuous_on (cball a e) f"
- and "f ` (cball a e) \<subseteq> cball a e"
+ and "f ` cball a e \<subseteq> cball a e"
obtains x where "x \<in> cball a e" and "f x = x"
using brouwer_weak[OF compact_cball convex_cball, of a e f]
unfolding interior_cball ball_eq_empty
@@ -3597,7 +4125,8 @@
obtains x where "x \<in> s" and "f x = x"
proof -
have "\<exists>e>0. s \<subseteq> cball 0 e"
- using compact_imp_bounded[OF assms(1)] unfolding bounded_pos
+ using compact_imp_bounded[OF assms(1)]
+ unfolding bounded_pos
apply (erule_tac exE)
apply (rule_tac x=b in exI)
apply (auto simp add: dist_norm)
@@ -3665,7 +4194,8 @@
then have "scaleR 2 a = scaleR 1 x + scaleR 1 x"
by (auto simp add: algebra_simps)
then have "a = x"
- unfolding scaleR_left_distrib[symmetric] by auto
+ unfolding scaleR_left_distrib[symmetric]
+ by auto
then show False
using x assms by auto
qed
@@ -3697,7 +4227,7 @@
fixes a b u v x :: "'a::ordered_euclidean_space"
assumes "x \<in> {a..b}"
and "{u..v} \<noteq> {}"
- shows "interval_bij (a,b) (u,v) x \<in> {u..v}"
+ shows "interval_bij (a, b) (u, v) x \<in> {u..v}"
apply (simp only: interval_bij_def split_conv mem_interval inner_setsum_left_Basis cong: ball_cong)
apply safe
proof -