1.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Fri Sep 14 21:23:06 2012 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Fri Sep 14 21:26:01 2012 +0200
1.3 @@ -24,12 +24,16 @@
1.4
1.5 lemma brouwer_compactness_lemma:
1.6 assumes "compact s" "continuous_on s f" "\<not> (\<exists>x\<in>s. (f x = (0::_::euclidean_space)))"
1.7 - obtains d where "0 < d" "\<forall>x\<in>s. d \<le> norm(f x)" proof(cases "s={}") case False
1.8 - have "continuous_on s (norm \<circ> f)" by(rule continuous_on_intros continuous_on_norm assms(2))+
1.9 - then obtain x where x:"x\<in>s" "\<forall>y\<in>s. (norm \<circ> f) x \<le> (norm \<circ> f) y"
1.10 - using continuous_attains_inf[OF assms(1), of "norm \<circ> f"] and False unfolding o_def by auto
1.11 + obtains d where "0 < d" "\<forall>x\<in>s. d \<le> norm(f x)"
1.12 +proof (cases "s={}")
1.13 + case False
1.14 + have "continuous_on s (norm \<circ> f)"
1.15 + by(rule continuous_on_intros continuous_on_norm assms(2))+
1.16 + with False obtain x where x: "x\<in>s" "\<forall>y\<in>s. (norm \<circ> f) x \<le> (norm \<circ> f) y"
1.17 + using continuous_attains_inf[OF assms(1), of "norm \<circ> f"] unfolding o_def by auto
1.18 have "(norm \<circ> f) x > 0" using assms(3) and x(1) by auto
1.19 - thus ?thesis apply(rule that) using x(2) unfolding o_def by auto qed(rule that[of 1], auto)
1.20 + then show ?thesis by (rule that) (insert x(2), auto simp: o_def)
1.21 +qed (rule that [of 1], auto)
1.22
1.23 lemma kuhn_labelling_lemma: fixes type::"'a::euclidean_space"
1.24 assumes "(\<forall>x::'a. P x \<longrightarrow> P (f x))" "\<forall>x. P x \<longrightarrow> (\<forall>i<DIM('a). Q i \<longrightarrow> 0 \<le> x$$i \<and> x$$i \<le> 1)"
1.25 @@ -37,19 +41,41 @@
1.26 (\<forall>x.\<forall> i<DIM('a). P x \<and> Q i \<and> (x$$i = 0) \<longrightarrow> (l x i = 0)) \<and>
1.27 (\<forall>x.\<forall> i<DIM('a). P x \<and> Q i \<and> (x$$i = 1) \<longrightarrow> (l x i = 1)) \<and>
1.28 (\<forall>x.\<forall> i<DIM('a). P x \<and> Q i \<and> (l x i = 0) \<longrightarrow> x$$i \<le> f(x)$$i) \<and>
1.29 - (\<forall>x.\<forall> i<DIM('a). P x \<and> Q i \<and> (l x i = 1) \<longrightarrow> f(x)$$i \<le> x$$i)" proof-
1.30 - 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
1.31 - 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
1.32 - show ?thesis unfolding and_forall_thm apply(subst choice_iff[THEN sym])+ proof(rule,rule) case goal1
1.33 + (\<forall>x.\<forall> i<DIM('a). P x \<and> Q i \<and> (l x i = 1) \<longrightarrow> f(x)$$i \<le> x$$i)"
1.34 +proof -
1.35 + have and_forall_thm:"\<And>P Q. (\<forall>x. P x) \<and> (\<forall>x. Q x) \<longleftrightarrow> (\<forall>x. P x \<and> Q x)"
1.36 + by auto
1.37 + 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)"
1.38 + by auto
1.39 + show ?thesis
1.40 + unfolding and_forall_thm
1.41 + apply(subst choice_iff[THEN sym])+
1.42 + apply rule
1.43 + apply rule
1.44 + proof -
1.45 + case goal1
1.46 let ?R = "\<lambda>y. (P x \<and> Q xa \<and> x $$ xa = 0 \<longrightarrow> y = (0::nat)) \<and>
1.47 - (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)"
1.48 - { assume "P x" "Q xa" "xa<DIM('a)" hence "0 \<le> f x $$ xa \<and> f x $$ xa \<le> 1" using assms(2)[rule_format,of "f x" xa]
1.49 - apply(drule_tac assms(1)[rule_format]) by auto }
1.50 - hence "xa<DIM('a) \<Longrightarrow> ?R 0 \<or> ?R 1" by auto thus ?case by auto qed qed
1.51 + (P x \<and> Q xa \<and> x $$ xa = 1 \<longrightarrow> y = 1) \<and>
1.52 + (P x \<and> Q xa \<and> y = 0 \<longrightarrow> x $$ xa \<le> f x $$ xa) \<and>
1.53 + (P x \<and> Q xa \<and> y = 1 \<longrightarrow> f x $$ xa \<le> x $$ xa)"
1.54 + {
1.55 + assume "P x" "Q xa" "xa<DIM('a)"
1.56 + then have "0 \<le> f x $$ xa \<and> f x $$ xa \<le> 1"
1.57 + using assms(2)[rule_format,of "f x" xa]
1.58 + apply (drule_tac assms(1)[rule_format])
1.59 + apply auto
1.60 + done
1.61 + }
1.62 + then have "xa<DIM('a) \<Longrightarrow> ?R 0 \<or> ?R 1" by auto
1.63 + then show ?case by auto
1.64 + qed
1.65 +qed
1.66 +
1.67
1.68 subsection {* The key "counting" observation, somewhat abstracted. *}
1.69
1.70 -lemma setsum_Un_disjoint':assumes "finite A" "finite B" "A \<inter> B = {}" "A \<union> B = C"
1.71 +lemma setsum_Un_disjoint':
1.72 + assumes "finite A" "finite B" "A \<inter> B = {}" "A \<union> B = C"
1.73 shows "setsum g C = setsum g A + setsum g B"
1.74 using setsum_Un_disjoint[OF assms(1-3)] and assms(4) by auto
1.75
1.76 @@ -60,19 +86,29 @@
1.77 "\<forall>s\<in>simplices. \<not> compo s \<longrightarrow> (card {f \<in> faces. face f s \<and> compo' f} = 0) \<or>
1.78 (card {f \<in> faces. face f s \<and> compo' f} = 2)"
1.79 "odd(card {f \<in> faces. compo' f \<and> bnd f})"
1.80 - shows "odd(card {s \<in> simplices. compo s})" proof-
1.81 - 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}"
1.82 - "\<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
1.83 + shows "odd(card {s \<in> simplices. compo s})"
1.84 +proof -
1.85 + 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} =
1.86 + {f\<in>faces. compo' f \<and> face f x}"
1.87 + "\<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} = {}"
1.88 + by auto
1.89 hence lem1:"setsum (\<lambda>s. (card {f \<in> faces. face f s \<and> compo' f})) simplices =
1.90 - setsum (\<lambda>s. card {f \<in> {f \<in> faces. compo' f \<and> bnd f}. face f s}) simplices +
1.91 - setsum (\<lambda>s. card {f \<in> {f \<in> faces. compo' f \<and> \<not> (bnd f)}. face f s}) simplices"
1.92 - unfolding setsum_addf[THEN sym] apply- apply(rule setsum_cong2)
1.93 - using assms(1) by(auto simp add: card_Un_Int, auto simp add:conj_commute)
1.94 + setsum (\<lambda>s. card {f \<in> {f \<in> faces. compo' f \<and> bnd f}. face f s}) simplices +
1.95 + setsum (\<lambda>s. card {f \<in> {f \<in> faces. compo' f \<and> \<not> (bnd f)}. face f s}) simplices"
1.96 + unfolding setsum_addf[THEN sym]
1.97 + apply -
1.98 + apply(rule setsum_cong2)
1.99 + using assms(1)
1.100 + apply (auto simp add: card_Un_Int, auto simp add:conj_commute)
1.101 + done
1.102 have lem2:"setsum (\<lambda>j. card {f \<in> {f \<in> faces. compo' f \<and> bnd f}. face f j}) simplices =
1.103 1 * card {f \<in> faces. compo' f \<and> bnd f}"
1.104 "setsum (\<lambda>j. card {f \<in> {f \<in> faces. compo' f \<and> \<not> bnd f}. face f j}) simplices =
1.105 2 * card {f \<in> faces. compo' f \<and> \<not> bnd f}"
1.106 - apply(rule_tac[!] setsum_multicount) using assms by auto
1.107 + apply(rule_tac[!] setsum_multicount)
1.108 + using assms
1.109 + apply auto
1.110 + done
1.111 have lem3:"setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) simplices =
1.112 setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices. compo s}+
1.113 setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices. \<not> compo s}"
1.114 @@ -90,27 +126,54 @@
1.115 int (card {f \<in> faces. compo' f \<and> bnd f} + 2 * card {f \<in> faces. compo' f \<and> \<not> bnd f}) -
1.116 int (card {s \<in> simplices. \<not> compo s \<and> card {f \<in> faces. face f s \<and> compo' f} = 2} * 2)"
1.117 using lem1[unfolded lem3 lem2 lem5] by auto
1.118 - have even_minus_odd:"\<And>x y. even x \<Longrightarrow> odd (y::int) \<Longrightarrow> odd (x - y)" using assms by auto
1.119 - have odd_minus_even:"\<And>x y. odd x \<Longrightarrow> even (y::int) \<Longrightarrow> odd (x - y)" using assms by auto
1.120 - show ?thesis unfolding even_nat_def unfolding card_eq_setsum and lem4[THEN sym] and *[unfolded card_eq_setsum]
1.121 - unfolding card_eq_setsum[THEN sym] apply (rule odd_minus_even) unfolding of_nat_add apply(rule odd_plus_even)
1.122 - apply(rule assms(7)[unfolded even_nat_def]) unfolding int_mult by auto qed
1.123 + have even_minus_odd:"\<And>x y. even x \<Longrightarrow> odd (y::int) \<Longrightarrow> odd (x - y)"
1.124 + using assms by auto
1.125 + have odd_minus_even:"\<And>x y. odd x \<Longrightarrow> even (y::int) \<Longrightarrow> odd (x - y)"
1.126 + using assms by auto
1.127 + show ?thesis
1.128 + unfolding even_nat_def card_eq_setsum and lem4[THEN sym] and *[unfolded card_eq_setsum]
1.129 + unfolding card_eq_setsum[THEN sym]
1.130 + apply (rule odd_minus_even)
1.131 + unfolding of_nat_add
1.132 + apply(rule odd_plus_even)
1.133 + apply(rule assms(7)[unfolded even_nat_def])
1.134 + unfolding int_mult
1.135 + apply auto
1.136 + done
1.137 +qed
1.138 +
1.139
1.140 subsection {* The odd/even result for faces of complete vertices, generalized. *}
1.141
1.142 -lemma card_1_exists: "card s = 1 \<longleftrightarrow> (\<exists>!x. x \<in> s)" unfolding One_nat_def
1.143 - apply rule apply(drule card_eq_SucD) defer apply(erule ex1E) proof-
1.144 +lemma card_1_exists: "card s = 1 \<longleftrightarrow> (\<exists>!x. x \<in> s)"
1.145 + unfolding One_nat_def
1.146 + apply rule
1.147 + apply (drule card_eq_SucD)
1.148 + defer
1.149 + apply(erule ex1E)
1.150 +proof -
1.151 fix x assume as:"x \<in> s" "\<forall>y. y \<in> s \<longrightarrow> y = x"
1.152 - have *:"s = insert x {}" apply- apply(rule set_eqI,rule) unfolding singleton_iff
1.153 - apply(rule as(2)[rule_format]) using as(1) by auto
1.154 - show "card s = Suc 0" unfolding * using card_insert by auto qed auto
1.155 + have *: "s = insert x {}"
1.156 + apply -
1.157 + apply (rule set_eqI,rule) unfolding singleton_iff
1.158 + apply (rule as(2)[rule_format]) using as(1)
1.159 + apply auto
1.160 + done
1.161 + show "card s = Suc 0" unfolding * using card_insert by auto
1.162 +qed auto
1.163
1.164 -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
1.165 - assume "card s = 2" then obtain x y where obt:"s = {x, y}" "x\<noteq>y" unfolding numeral_2_eq_2 apply - apply(erule exE conjE|drule card_eq_SucD)+ by auto
1.166 +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)))"
1.167 +proof
1.168 + assume "card s = 2"
1.169 + then obtain x y where obt:"s = {x, y}" "x\<noteq>y" unfolding numeral_2_eq_2
1.170 + apply - apply(erule exE conjE|drule card_eq_SucD)+ apply auto done
1.171 show "\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y)" using obt by auto next
1.172 - assume "\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y)" then guess x .. from this(2) guess y ..
1.173 - with `x\<in>s` have *:"s = {x, y}" "x\<noteq>y" by auto
1.174 - from this(2) show "card s = 2" unfolding * by auto qed
1.175 + assume "\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y)"
1.176 + then guess x ..
1.177 + from this(2) guess y ..
1.178 + with `x\<in>s` have *: "s = {x, y}" "x\<noteq>y" by auto
1.179 + from this(2) show "card s = 2" unfolding * by auto
1.180 +qed
1.181
1.182 lemma image_lemma_0: assumes "card {a\<in>s. f ` (s - {a}) = t - {b}} = n"
1.183 shows "card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> (f ` s' = t - {b})} = n" proof-