--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Wed Aug 28 16:36:46 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Wed Aug 28 17:20:16 2013 +0200
@@ -29,7 +29,8 @@
apply (cases "b=0")
defer
apply (rule divide_nonneg_pos)
- using assms apply auto
+ using assms
+ apply auto
done
lemma brouwer_compactness_lemma:
@@ -175,7 +176,8 @@
apply (rule as(2)[rule_format]) using as(1)
apply auto
done
- show "card s = Suc 0" unfolding * using card_insert by auto
+ show "card s = Suc 0"
+ 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)))"
@@ -653,12 +655,14 @@
have "1 \<le> card {k \<in> {1..n}. a k < x k}" "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
+ using a and xb
+ apply auto
done
thus ?thesis
apply (rule_tac x=a in bexI, rule_tac x=b in bexI)
using kle_range_combine[OF a(2)[rule_format] xb(3) Suc(5)[rule_format], of 1 "m"]
- using a(1) xb(1-2) apply auto
+ using a(1) xb(1-2)
+ apply auto
done
next
case True
@@ -764,10 +768,14 @@
show ?thesis apply(rule disjI2,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")
+ 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
- thus "x j = b j" using kle_imp_pointwise[OF assms(3),THEN spec[where x=j]]
+ thus "x j = b j"
+ using kle_imp_pointwise[OF assms(3),THEN spec[where x=j]]
by auto
qed
qed
@@ -818,7 +826,7 @@
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
- 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}"
+ 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
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])
@@ -827,7 +835,7 @@
hence "kle n a b \<and> n \<le> card {k\<in>{1..n}. a(k) < b(k)}"
apply -
apply (rule kle_range_combine_l[where y=c])
- using a `c\<in>s` `b\<in>s` apply auto
+ using a `c \<in> s` `b \<in> s` apply auto
done
moreover
have "card {1..n} \<ge> card {k\<in>{1..n}. a(k) < b(k)}"
@@ -2774,46 +2782,148 @@
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})})" 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
- show ?thesis apply(rule kuhn_simplex_lemma[unfolded mem_Collect_eq]) apply(rule,rule,rule *,rule reduced_labelling)
- apply(rule *(1)[OF assms(4)]) apply(rule set_eqI) unfolding mem_Collect_eq apply(rule,erule conjE) defer apply(rule) proof-(*(rule,rule)*)
- fix f 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"
+ "\<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})})"
+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
+ show ?thesis
+ apply (rule kuhn_simplex_lemma[unfolded mem_Collect_eq])
+ apply (rule, rule, rule *, rule reduced_labelling)
+ apply (rule *(1)[OF assms(4)])
+ apply (rule set_eqI)
+ unfolding mem_Collect_eq
+ apply (rule, erule conjE)
+ defer
+ apply rule
+ proof -
+ fix f
+ 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
- have allp:"\<forall>x\<in>f. x (n + 1) = p" using assms(2) using as(1)[unfolded ksimplex_def] by auto
- { fix x assume "x\<in>f" hence "reduced lab (n + 1) x < n + 1" apply-apply(rule reduced_labelling_nonzero)
- defer using assms(3) using as(1)[unfolded ksimplex_def] by auto
- hence "reduced lab (n + 1) x = reduced lab n x" apply-apply(rule reduced_labelling_Suc) using reduced_labelling(1) by auto }
- hence "reduced lab (n + 1) ` f = {0..n}" unfolding as(2)[symmetric] apply- apply(rule set_eqI) unfolding image_iff by auto
- moreover guess s using as(1)[unfolded simplex_top_face[OF assms(1) allp,symmetric]] .. then guess a ..
+ have allp: "\<forall>x\<in>f. x (n + 1) = p"
+ using assms(2) using as(1)[unfolded ksimplex_def] by auto
+ {
+ fix x
+ assume "x \<in> f"
+ hence "reduced lab (n + 1) x < n + 1"
+ apply -
+ apply (rule reduced_labelling_nonzero)
+ defer using assms(3) using as(1)[unfolded ksimplex_def]
+ apply auto
+ done
+ hence "reduced lab (n + 1) x = reduced lab n x"
+ apply -
+ apply (rule reduced_labelling_Suc)
+ using reduced_labelling(1)
+ apply auto
+ done
+ }
+ hence "reduced lab (n + 1) ` f = {0..n}"
+ unfolding as(2)[symmetric]
+ apply -
+ apply (rule set_eqI)
+ unfolding image_iff
+ apply auto
+ done
+ moreover guess s using as(1)[unfolded simplex_top_face[OF assms(1) allp,symmetric]] ..
+ then guess a ..
ultimately show "\<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)
- apply(rule_tac x=s in exI,rule_tac x=a in exI) unfolding complete_face_top[OF *] using allp as(1) by auto
- next fix f assume as:"\<exists>s a. ksimplex p (n + 1) s \<and>
+ apply (rule_tac x = s in exI)
+ apply (rule_tac x = a in exI)
+ unfolding complete_face_top[OF *]
+ using allp as(1)
+ apply auto
+ done
+ next
+ fix f
+ 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)+) . note sa=this
- { fix x assume "x\<in>f" hence "reduced lab (n + 1) x \<in> reduced lab (n + 1) ` f" by auto
- hence "reduced lab (n + 1) x < n + 1" using sa(4) by auto
- hence "reduced lab (n + 1) x = reduced lab n x" apply-apply(rule reduced_labelling_Suc)
- using reduced_labelling(1) by auto }
- thus part1:"reduced lab n ` f = {0..n}" unfolding sa(4)[symmetric] apply-apply(rule set_eqI) unfolding image_iff by auto
- have *:"\<forall>x\<in>f. x (n + 1) = p" proof(cases "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0")
- case True then guess j .. hence "\<And>x. x\<in>f \<Longrightarrow> reduced lab (n + 1) x \<noteq> j - 1" apply-apply(rule reduced_labelling_zero) apply assumption
- apply(rule assms(2)[rule_format]) using sa(1)[unfolded ksimplex_def] unfolding sa by auto moreover
+ then guess s ..
+ then guess a
+ apply -
+ apply (erule exE,(erule conjE)+)
+ done
+ note sa = this
+ {
+ fix x
+ assume "x \<in> f"
+ hence "reduced lab (n + 1) x \<in> reduced lab (n + 1) ` f"
+ by auto
+ hence "reduced lab (n + 1) x < n + 1"
+ using sa(4) by auto
+ hence "reduced lab (n + 1) x = reduced lab n x"
+ apply -
+ apply (rule reduced_labelling_Suc)
+ using reduced_labelling(1)
+ apply auto
+ done
+ }
+ thus part1: "reduced lab n ` f = {0..n}"
+ unfolding sa(4)[symmetric]
+ apply -
+ apply (rule set_eqI)
+ unfolding image_iff
+ apply auto
+ done
+ have *: "\<forall>x\<in>f. x (n + 1) = p"
+ proof (cases "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0")
+ case True
+ then guess j ..
+ hence "\<And>x. x \<in> f \<Longrightarrow> reduced lab (n + 1) x \<noteq> j - 1"
+ apply -
+ apply (rule reduced_labelling_zero)
+ apply assumption
+ apply (rule assms(2)[rule_format])
+ using sa(1)[unfolded ksimplex_def]
+ unfolding sa
+ apply auto
+ done
+ moreover
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 thus ?thesis by auto next
- case False hence "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p" using sa(5) by fastforce then guess j .. note j=this
- thus ?thesis proof(cases "j = n+1")
- case False hence *:"j\<in>{1..n}" using j by auto
- hence "\<And>x. x\<in>f \<Longrightarrow> reduced lab n x < j" apply(rule reduced_labelling_nonzero) proof- fix x assume "x\<in>f"
- hence "lab x j = 1" apply-apply(rule assms(3)[rule_format,OF j(1)])
- using sa(1)[unfolded ksimplex_def] using j unfolding sa by auto thus "lab x j \<noteq> 0" by auto qed
- moreover have "j\<in>{0..n}" using * by auto
- ultimately have False unfolding part1[symmetric] using * unfolding image_iff by auto thus ?thesis by auto qed auto qed
- thus "ksimplex p n f" using as unfolding simplex_top_face[OF assms(1) *,symmetric] by auto qed qed
+ ultimately have False
+ unfolding sa(4)[symmetric]
+ unfolding image_iff
+ by fastforce
+ thus ?thesis by auto
+ next
+ case False
+ hence "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p"
+ using sa(5) by fastforce then guess j .. note j=this
+ thus ?thesis
+ proof (cases "j = n + 1")
+ case False hence *: "j \<in> {1..n}"
+ using j by auto
+ hence "\<And>x. x \<in> f \<Longrightarrow> reduced lab n x < j"
+ apply (rule reduced_labelling_nonzero)
+ proof -
+ fix x
+ assume "x \<in> f"
+ hence "lab x j = 1"
+ apply -
+ apply (rule assms(3)[rule_format,OF j(1)])
+ using sa(1)[unfolded ksimplex_def]
+ using j
+ unfolding sa
+ apply auto
+ done
+ thus "lab x j \<noteq> 0" by auto
+ qed
+ moreover have "j \<in> {0..n}" using * by auto
+ ultimately have False
+ unfolding part1[symmetric]
+ using * unfolding image_iff
+ by auto
+ thus ?thesis by auto
+ qed auto
+ qed
+ thus "ksimplex p n f"
+ 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)"
@@ -2822,51 +2932,135 @@
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. *}
-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) thus ?r using a by auto next
- assume r:?r show ?l unfolding r ksimplex_eq by auto qed
+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
+ thus ?r using a by auto
+next
+ assume r: ?r
+ show ?l unfolding r ksimplex_eq by auto
+qed
-lemma reduce_labelling_zero[simp]: "reduced lab 0 x = 0" apply(rule reduced_labelling_unique) by auto
+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})})" using assms proof(induct n)
+ "\<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})}"
- { case 0 have *:"?M 0 = {{(\<lambda>x. p)}}" unfolding ksimplex_0 by auto show ?case unfolding * by auto }
- case (Suc n) have "odd (card (?M n))" apply(rule Suc(1)[OF Suc(2)]) using Suc(3-) by auto
- thus ?case apply-apply(rule kuhn_induction_Suc) using Suc(2-) by auto qed
+ {
+ case 0
+ have *: "?M 0 = {{(\<lambda>x. p)}}"
+ unfolding ksimplex_0 by auto
+ show ?case unfolding * by auto
+ next
+ case (Suc n)
+ have "odd (card (?M n))"
+ apply (rule Suc(1)[OF Suc(2)])
+ using Suc(3-)
+ apply auto
+ done
+ thus ?case
+ apply -
+ apply (rule kuhn_induction_Suc)
+ using Suc(2-)
+ apply auto
+ done
+ }
+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))"
+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))"
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)" 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" by auto
- have "odd (card ?A)" apply(rule kuhn_combinatorial[of p n label]) using assms by auto
- hence "card ?A \<noteq> 0" apply-apply(rule ccontr) by auto hence "?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 apply(rule ksimplex_extrema_strong[OF s(1) `n\<noteq>0`]) . note ab=this
- show ?thesis apply(rule that[of a]) proof(rule_tac[!] ballI) fix i assume "i\<in>{1..n}"
- hence "a i + 1 \<le> p" apply-apply(rule order_trans[of _ "b i"]) apply(subst ab(5)[THEN spec[where x=i]])
- using s(1)[unfolded ksimplex_def] defer apply- apply(erule conjE)+ apply(drule_tac bspec[OF _ ab(2)])+ by auto
+ "\<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)"
+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"
+ by auto
+ have "odd (card ?A)"
+ apply (rule kuhn_combinatorial[of p n label])
+ using assms
+ apply auto
+ done
+ hence "card ?A \<noteq> 0"
+ apply -
+ apply (rule ccontr)
+ apply auto
+ done
+ hence "?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
+ show ?thesis
+ apply (rule that[of a])
+ apply (rule_tac[!] ballI)
+ proof -
+ fix i
+ assume "i\<in>{1..n}"
+ hence "a i + 1 \<le> p"
+ apply -
+ apply (rule order_trans[of _ "b i"])
+ apply (subst ab(5)[THEN spec[where x=i]])
+ using s(1)[unfolded ksimplex_def]
+ defer
+ apply -
+ apply (erule conjE)+
+ apply (drule_tac bspec[OF _ ab(2)])+
+ apply auto
+ done
thus "a i < p" by auto
- case goal2 hence "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 then guess v unfolding image_iff .. note v=this
- show ?case apply(rule_tac x=u in exI, rule_tac x=v in exI) apply(rule conjI) defer apply(rule conjI) defer 2 proof(rule_tac[1-2] ballI)
- show "label u i \<noteq> label v i" using reduced_labelling[of label n u] reduced_labelling[of label n v]
- unfolding u(2)[symmetric] v(2)[symmetric] using goal2 by auto
- 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"
- using conjD[OF ab(4)[rule_format, OF u(1)]] and conjD[OF ab(4)[rule_format, OF v(1)]] apply-
- apply(drule_tac[!] kle_imp_pointwise)+ apply(erule_tac[!] x=j in allE)+ unfolding ab(5)[rule_format] using j
- by auto qed qed qed
+ next
+ case goal2
+ hence "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
+ then guess v unfolding image_iff .. note v = this
+ show ?case
+ apply (rule_tac x = u in exI)
+ apply (rule_tac x = v in exI)
+ apply (rule conjI)
+ defer
+ apply (rule conjI)
+ defer 2
+ apply (rule_tac[1-2] ballI)
+ proof -
+ show "label u i \<noteq> label v i"
+ using reduced_labelling [of label n u] reduced_labelling [of label n v]
+ unfolding u(2)[symmetric] v(2)[symmetric]
+ using goal2
+ apply auto
+ 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"
+ using conjD[OF ab(4)[rule_format, OF u(1)]]
+ and conjD[OF ab(4)[rule_format, OF v(1)]]
+ apply -
+ apply (drule_tac[!] kle_imp_pointwise)+
+ apply (erule_tac[!] x=j in allE)+
+ unfolding ab(5)[rule_format]
+ using j
+ apply auto
+ done
+ qed
+ qed
+qed
subsection {* The main result for the unit cube. *}
@@ -2986,7 +3180,8 @@
note e=this[rule_format,unfolded dist_norm]
show ?thesis
apply (rule_tac x="min (e/2) (d/real n/8)" in exI)
- proof safe
+ apply safe
+ proof -
show "0 < min (e / 2) (d / real n / 8)"
using d' e by auto
fix x y z i
@@ -3216,7 +3411,7 @@
and t :: "('b::euclidean_space) set"
assumes "s homeomorphic t"
shows "(\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)) \<longleftrightarrow>
- (\<forall>g. continuous_on t g \<and> g ` t \<subseteq> t \<longrightarrow> (\<exists>y\<in>t. g y = y))"
+ (\<forall>g. continuous_on t g \<and> g ` t \<subseteq> t \<longrightarrow> (\<exists>y\<in>t. g y = y))"
proof -
guess r using assms[unfolded homeomorphic_def homeomorphism_def] ..
then guess i ..
@@ -3244,8 +3439,9 @@
apply -
apply (rule invertible_fixpoint_property[OF continuous_on_id _ _ _ _ assms(2), of t h g])
prefer 7
- apply (rule_tac y=y in that)
- using assms apply auto
+ apply (rule_tac y = y in that)
+ using assms
+ apply auto
done
qed
@@ -3253,7 +3449,7 @@
subsection {*So the Brouwer theorem for any set with nonempty interior. *}
lemma brouwer_weak:
- fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'a::ordered_euclidean_space"
+ fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'a::ordered_euclidean_space"
assumes "compact s" "convex s" "interior s \<noteq> {}" "continuous_on s f" "f ` s \<subseteq> s"
obtains x where "x \<in> s" "f x = x"
proof -
@@ -3290,7 +3486,8 @@
rather involved @{text "HOMEOMORPHIC_CONVEX_COMPACT"} theorem, just using
a scaling and translation to put the set inside the unit cube. *}
-lemma brouwer: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'a"
+lemma brouwer:
+ fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'a"
assumes "compact s" "convex s" "s \<noteq> {}" "continuous_on s f" "f ` s \<subseteq> s"
obtains x where "x \<in> s" "f x = x"
proof -
@@ -3353,7 +3550,8 @@
apply (simp add: * norm_minus_commute)
done
note x = this
- hence "scaleR 2 a = scaleR 1 x + scaleR 1 x" by (auto simp add:algebra_simps)
+ hence "scaleR 2 a = scaleR 1 x + scaleR 1 x"
+ by (auto simp add: algebra_simps)
hence "a = x" unfolding scaleR_left_distrib[symmetric] by auto
thus False using x assms by auto
qed
@@ -3361,14 +3559,15 @@
subsection {*Bijections between intervals. *}
-definition interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::ordered_euclidean_space" where
- "interval_bij \<equiv> \<lambda>(a, b) (u, v) x. (\<Sum>i\<in>Basis. (u\<bullet>i + (x\<bullet>i - a\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (v\<bullet>i - u\<bullet>i)) *\<^sub>R i)"
+definition interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::ordered_euclidean_space"
+ where "interval_bij =
+ (\<lambda>(a, b) (u, v) x. (\<Sum>i\<in>Basis. (u\<bullet>i + (x\<bullet>i - a\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (v\<bullet>i - u\<bullet>i)) *\<^sub>R i))"
lemma interval_bij_affine:
"interval_bij (a,b) (u,v) = (\<lambda>x. (\<Sum>i\<in>Basis. ((v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (x\<bullet>i)) *\<^sub>R i) +
(\<Sum>i\<in>Basis. (u\<bullet>i - (v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (a\<bullet>i)) *\<^sub>R i))"
by (auto simp: setsum_addf[symmetric] scaleR_add_left[symmetric] interval_bij_def fun_eq_iff
- field_simps inner_simps add_divide_distrib[symmetric] intro!: setsum_cong)
+ field_simps inner_simps add_divide_distrib[symmetric] intro!: setsum_cong)
lemma continuous_interval_bij:
"continuous (at x) (interval_bij (a,b::'a::ordered_euclidean_space) (u,v::'a))"
@@ -3384,7 +3583,8 @@
assumes "x \<in> {a..b}" "{u..v} \<noteq> {}"
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)
-proof safe
+ apply safe
+proof -
fix i :: 'a
assume i: "i \<in> Basis"
have "{a..b} \<noteq> {}" using assms by auto