1.1 --- a/Admin/components/components.sha1 Fri Sep 13 21:55:33 2013 +0200
1.2 +++ b/Admin/components/components.sha1 Fri Sep 13 22:33:16 2013 +0200
1.3 @@ -19,6 +19,7 @@
1.4 d765bc4ad2f34d494429b2a8c1563c49db224944 jdk-7u13.tar.gz
1.5 13a265e4b706ece26fdfa6fc9f4a3dd1366016d2 jdk-7u21.tar.gz
1.6 5080274f8721a18111a7f614793afe6c88726739 jdk-7u25.tar.gz
1.7 +9e4a76578287849591188e928f46789cbbdfe9cb jdk-7u40.tar.gz
1.8 ec740ee9ffd43551ddf1e5b91641405116af6291 jdk-7u6.tar.gz
1.9 7d5b152ac70f720bb9e783fa45ecadcf95069584 jdk-7u9.tar.gz
1.10 44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
2.1 --- a/Admin/components/main Fri Sep 13 21:55:33 2013 +0200
2.2 +++ b/Admin/components/main Fri Sep 13 22:33:16 2013 +0200
2.3 @@ -3,7 +3,7 @@
2.4 e-1.8
2.5 exec_process-1.0.3
2.6 Haskabelle-2013
2.7 -jdk-7u25
2.8 +jdk-7u40
2.9 jedit_build-20130910
2.10 jfreechart-1.0.14-1
2.11 kodkodi-1.5.2
3.1 --- a/Admin/java/build Fri Sep 13 21:55:33 2013 +0200
3.2 +++ b/Admin/java/build Fri Sep 13 22:33:16 2013 +0200
3.3 @@ -11,8 +11,8 @@
3.4
3.5 ## parameters
3.6
3.7 -VERSION="7u25"
3.8 -FULL_VERSION="1.7.0_25"
3.9 +VERSION="7u40"
3.10 +FULL_VERSION="1.7.0_40"
3.11
3.12 ARCHIVE_LINUX32="jdk-${VERSION}-linux-i586.tar.gz"
3.13 ARCHIVE_LINUX64="jdk-${VERSION}-linux-x64.tar.gz"
4.1 --- a/src/HOL/Multivariate_Analysis/Fashoda.thy Fri Sep 13 21:55:33 2013 +0200
4.2 +++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Fri Sep 13 22:33:16 2013 +0200
4.3 @@ -57,7 +57,7 @@
4.4 unfolding sqprojection_def
4.5 unfolding infnorm_mul[unfolded scalar_mult_eq_scaleR]
4.6 unfolding abs_inverse real_abs_infnorm
4.7 - apply (subst infnorm_eq_0[THEN sym])
4.8 + apply (subst infnorm_eq_0[symmetric])
4.9 apply auto
4.10 done
4.11 let ?F = "\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w"
4.12 @@ -121,9 +121,11 @@
4.13 apply auto
4.14 done
4.15 then have *: "infnorm (sqprojection (?F y)) = 1"
4.16 - unfolding y o_def by - (rule lem2[rule_format])
4.17 + unfolding y o_def
4.18 + by - (rule lem2[rule_format])
4.19 have "infnorm x = 1"
4.20 - unfolding *[THEN sym] y o_def by (rule lem1[rule_format])
4.21 + unfolding *[symmetric] y o_def
4.22 + by (rule lem1[rule_format])
4.23 then show "x \<in> {- 1..1}"
4.24 unfolding mem_interval_cart infnorm_2
4.25 apply -
4.26 @@ -150,10 +152,11 @@
4.27 apply auto
4.28 done
4.29 then have *: "infnorm (sqprojection (?F x)) = 1"
4.30 - unfolding o_def by (rule lem2[rule_format])
4.31 + unfolding o_def
4.32 + by (rule lem2[rule_format])
4.33 have nx: "infnorm x = 1"
4.34 - apply (subst x(2)[THEN sym])
4.35 - unfolding *[THEN sym] o_def
4.36 + apply (subst x(2)[symmetric])
4.37 + unfolding *[symmetric] o_def
4.38 apply (rule lem1[rule_format])
4.39 done
4.40 have "\<forall>x i. x \<noteq> 0 \<longrightarrow> (0 < (sqprojection x)$i \<longleftrightarrow> 0 < x$i)"
4.41 @@ -165,7 +168,7 @@
4.42 fix i :: 2
4.43 assume x: "x \<noteq> 0"
4.44 have "inverse (infnorm x) > 0"
4.45 - using x[unfolded infnorm_pos_lt[THEN sym]] by auto
4.46 + using x[unfolded infnorm_pos_lt[symmetric]] by auto
4.47 then show "(0 < sqprojection x $ i) = (0 < x $ i)"
4.48 and "(sqprojection x $ i < 0) = (x $ i < 0)"
4.49 unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def
4.50 @@ -311,8 +314,8 @@
4.51 qed
4.52 then guess s .. from this(2) guess t .. note st=this
4.53 show thesis
4.54 - apply (rule_tac z="f (iscale s)" in that)
4.55 - using st `s\<in>{- 1..1}`
4.56 + apply (rule_tac z = "f (iscale s)" in that)
4.57 + using st `s \<in> {- 1..1}`
4.58 unfolding o_def path_image_def image_iff
4.59 apply -
4.60 apply (rule_tac x="iscale s" in bexI)
4.61 @@ -323,127 +326,335 @@
4.62 done
4.63 qed
4.64
4.65 -lemma fashoda: fixes b::"real^2"
4.66 - assumes "path f" "path g" "path_image f \<subseteq> {a..b}" "path_image g \<subseteq> {a..b}"
4.67 - "(pathstart f)$1 = a$1" "(pathfinish f)$1 = b$1"
4.68 - "(pathstart g)$2 = a$2" "(pathfinish g)$2 = b$2"
4.69 - obtains z where "z \<in> path_image f" "z \<in> path_image g" proof-
4.70 - fix P Q S presume "P \<or> Q \<or> S" "P \<Longrightarrow> thesis" "Q \<Longrightarrow> thesis" "S \<Longrightarrow> thesis" thus thesis by auto
4.71 -next have "{a..b} \<noteq> {}" using assms(3) using path_image_nonempty by auto
4.72 - hence "a \<le> b" unfolding interval_eq_empty_cart less_eq_vec_def by(auto simp add: not_less)
4.73 - thus "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)" unfolding less_eq_vec_def forall_2 by auto
4.74 -next assume as:"a$1 = b$1" have "\<exists>z\<in>path_image g. z$2 = (pathstart f)$2" apply(rule connected_ivt_component_cart)
4.75 - apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image)
4.76 +lemma fashoda:
4.77 + fixes b :: "real^2"
4.78 + assumes "path f"
4.79 + and "path g"
4.80 + and "path_image f \<subseteq> {a..b}"
4.81 + and "path_image g \<subseteq> {a..b}"
4.82 + and "(pathstart f)$1 = a$1"
4.83 + and "(pathfinish f)$1 = b$1"
4.84 + and "(pathstart g)$2 = a$2"
4.85 + and "(pathfinish g)$2 = b$2"
4.86 + obtains z where "z \<in> path_image f" and "z \<in> path_image g"
4.87 +proof -
4.88 + fix P Q S
4.89 + presume "P \<or> Q \<or> S" "P \<Longrightarrow> thesis" and "Q \<Longrightarrow> thesis" and "S \<Longrightarrow> thesis"
4.90 + then show thesis
4.91 + by auto
4.92 +next
4.93 + have "{a..b} \<noteq> {}"
4.94 + using assms(3) using path_image_nonempty by auto
4.95 + then have "a \<le> b"
4.96 + unfolding interval_eq_empty_cart less_eq_vec_def by (auto simp add: not_less)
4.97 + then show "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)"
4.98 + unfolding less_eq_vec_def forall_2 by auto
4.99 +next
4.100 + assume as: "a$1 = b$1"
4.101 + have "\<exists>z\<in>path_image g. z$2 = (pathstart f)$2"
4.102 + apply (rule connected_ivt_component_cart)
4.103 + apply (rule connected_path_image assms)+
4.104 + apply (rule pathstart_in_path_image)
4.105 + apply (rule pathfinish_in_path_image)
4.106 unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"]
4.107 - unfolding pathstart_def by(auto simp add: less_eq_vec_def) then guess z .. note z=this
4.108 - have "z \<in> {a..b}" using z(1) assms(4) unfolding path_image_def by blast
4.109 - hence "z = f 0" unfolding vec_eq_iff forall_2 unfolding z(2) pathstart_def
4.110 + unfolding pathstart_def
4.111 + apply (auto simp add: less_eq_vec_def)
4.112 + done
4.113 + then guess z .. note z=this
4.114 + have "z \<in> {a..b}"
4.115 + using z(1) assms(4)
4.116 + unfolding path_image_def
4.117 + by blast
4.118 + then have "z = f 0"
4.119 + unfolding vec_eq_iff forall_2
4.120 + unfolding z(2) pathstart_def
4.121 using assms(3)[unfolded path_image_def subset_eq mem_interval_cart,rule_format,of "f 0" 1]
4.122 - unfolding mem_interval_cart apply(erule_tac x=1 in allE) using as by auto
4.123 - thus thesis apply-apply(rule that[OF _ z(1)]) unfolding path_image_def by auto
4.124 -next assume as:"a$2 = b$2" have "\<exists>z\<in>path_image f. z$1 = (pathstart g)$1" apply(rule connected_ivt_component_cart)
4.125 - apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image)
4.126 - unfolding assms using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"]
4.127 - unfolding pathstart_def by(auto simp add: less_eq_vec_def) then guess z .. note z=this
4.128 - have "z \<in> {a..b}" using z(1) assms(3) unfolding path_image_def by blast
4.129 - hence "z = g 0" unfolding vec_eq_iff forall_2 unfolding z(2) pathstart_def
4.130 + unfolding mem_interval_cart
4.131 + apply (erule_tac x=1 in allE)
4.132 + using as
4.133 + apply auto
4.134 + done
4.135 + then show thesis
4.136 + apply -
4.137 + apply (rule that[OF _ z(1)])
4.138 + unfolding path_image_def
4.139 + apply auto
4.140 + done
4.141 +next
4.142 + assume as: "a$2 = b$2"
4.143 + have "\<exists>z\<in>path_image f. z$1 = (pathstart g)$1"
4.144 + apply (rule connected_ivt_component_cart)
4.145 + apply (rule connected_path_image assms)+
4.146 + apply (rule pathstart_in_path_image)
4.147 + apply (rule pathfinish_in_path_image)
4.148 + unfolding assms
4.149 + using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"]
4.150 + unfolding pathstart_def
4.151 + apply (auto simp add: less_eq_vec_def)
4.152 + done
4.153 + then guess z .. note z=this
4.154 + have "z \<in> {a..b}"
4.155 + using z(1) assms(3)
4.156 + unfolding path_image_def
4.157 + by blast
4.158 + then have "z = g 0"
4.159 + unfolding vec_eq_iff forall_2
4.160 + unfolding z(2) pathstart_def
4.161 using assms(4)[unfolded path_image_def subset_eq mem_interval_cart,rule_format,of "g 0" 2]
4.162 - unfolding mem_interval_cart apply(erule_tac x=2 in allE) using as by auto
4.163 - thus thesis apply-apply(rule that[OF z(1)]) unfolding path_image_def by auto
4.164 -next assume as:"a $ 1 < b $ 1 \<and> a $ 2 < b $ 2"
4.165 - have int_nem:"{- 1..1::real^2} \<noteq> {}" unfolding interval_eq_empty_cart by auto
4.166 - guess z apply(rule fashoda_unit_path[of "interval_bij (a,b) (- 1,1) \<circ> f" "interval_bij (a,b) (- 1,1) \<circ> g"])
4.167 + unfolding mem_interval_cart
4.168 + apply (erule_tac x=2 in allE)
4.169 + using as
4.170 + apply auto
4.171 + done
4.172 + then show thesis
4.173 + apply -
4.174 + apply (rule that[OF z(1)])
4.175 + unfolding path_image_def
4.176 + apply auto
4.177 + done
4.178 +next
4.179 + assume as: "a $ 1 < b $ 1 \<and> a $ 2 < b $ 2"
4.180 + have int_nem: "{- 1..1::real^2} \<noteq> {}"
4.181 + unfolding interval_eq_empty_cart by auto
4.182 + guess z
4.183 + apply (rule fashoda_unit_path[of "interval_bij (a,b) (- 1,1) \<circ> f" "interval_bij (a,b) (- 1,1) \<circ> g"])
4.184 unfolding path_def path_image_def pathstart_def pathfinish_def
4.185 - apply(rule_tac[1-2] continuous_on_compose) apply(rule assms[unfolded path_def] continuous_on_interval_bij)+
4.186 - unfolding subset_eq apply(rule_tac[1-2] ballI)
4.187 - proof- fix x assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
4.188 + apply (rule_tac[1-2] continuous_on_compose)
4.189 + apply (rule assms[unfolded path_def] continuous_on_interval_bij)+
4.190 + unfolding subset_eq
4.191 + apply(rule_tac[1-2] ballI)
4.192 + proof -
4.193 + fix x
4.194 + assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
4.195 + then guess y
4.196 + unfolding image_iff .. note y=this
4.197 + show "x \<in> {- 1..1}"
4.198 + unfolding y o_def
4.199 + apply (rule in_interval_interval_bij)
4.200 + using y(1)
4.201 + using assms(3)[unfolded path_image_def subset_eq] int_nem
4.202 + apply auto
4.203 + done
4.204 + next
4.205 + fix x
4.206 + assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
4.207 then guess y unfolding image_iff .. note y=this
4.208 - show "x \<in> {- 1..1}" unfolding y o_def apply(rule in_interval_interval_bij)
4.209 - using y(1) using assms(3)[unfolded path_image_def subset_eq] int_nem by auto
4.210 - next fix x assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
4.211 - then guess y unfolding image_iff .. note y=this
4.212 - show "x \<in> {- 1..1}" unfolding y o_def apply(rule in_interval_interval_bij)
4.213 - using y(1) using assms(4)[unfolded path_image_def subset_eq] int_nem by auto
4.214 - next show "(interval_bij (a, b) (- 1, 1) \<circ> f) 0 $ 1 = -1"
4.215 - "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1"
4.216 - "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1"
4.217 - "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1"
4.218 + show "x \<in> {- 1..1}"
4.219 + unfolding y o_def
4.220 + apply (rule in_interval_interval_bij)
4.221 + using y(1)
4.222 + using assms(4)[unfolded path_image_def subset_eq] int_nem
4.223 + apply auto
4.224 + done
4.225 + next
4.226 + show "(interval_bij (a, b) (- 1, 1) \<circ> f) 0 $ 1 = -1"
4.227 + and "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1"
4.228 + and "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1"
4.229 + and "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1"
4.230 using assms as
4.231 by (simp_all add: axis_in_Basis cart_eq_inner_axis pathstart_def pathfinish_def interval_bij_def)
4.232 (simp_all add: inner_axis)
4.233 - qed note z=this
4.234 + qed
4.235 + note z=this
4.236 from z(1) guess zf unfolding image_iff .. note zf=this
4.237 from z(2) guess zg unfolding image_iff .. note zg=this
4.238 - have *:"\<forall>i. (- 1) $ i < (1::real^2) $ i \<and> a $ i < b $ i" unfolding forall_2 using as by auto
4.239 - show thesis apply(rule_tac z="interval_bij (- 1,1) (a,b) z" in that)
4.240 - apply(subst zf) defer apply(subst zg) unfolding o_def interval_bij_bij_cart[OF *] path_image_def
4.241 - using zf(1) zg(1) by auto qed
4.242 + have *: "\<forall>i. (- 1) $ i < (1::real^2) $ i \<and> a $ i < b $ i"
4.243 + unfolding forall_2
4.244 + using as
4.245 + by auto
4.246 + show thesis
4.247 + apply (rule_tac z="interval_bij (- 1,1) (a,b) z" in that)
4.248 + apply (subst zf)
4.249 + defer
4.250 + apply (subst zg)
4.251 + unfolding o_def interval_bij_bij_cart[OF *] path_image_def
4.252 + using zf(1) zg(1)
4.253 + apply auto
4.254 + done
4.255 +qed
4.256
4.257 -subsection {*Some slightly ad hoc lemmas I use below*}
4.258
4.259 -lemma segment_vertical: fixes a::"real^2" assumes "a$1 = b$1"
4.260 - shows "x \<in> closed_segment a b \<longleftrightarrow> (x$1 = a$1 \<and> x$1 = b$1 \<and>
4.261 - (a$2 \<le> x$2 \<and> x$2 \<le> b$2 \<or> b$2 \<le> x$2 \<and> x$2 \<le> a$2))" (is "_ = ?R")
4.262 -proof-
4.263 +subsection {* Some slightly ad hoc lemmas I use below *}
4.264 +
4.265 +lemma segment_vertical:
4.266 + fixes a :: "real^2"
4.267 + assumes "a$1 = b$1"
4.268 + shows "x \<in> closed_segment a b \<longleftrightarrow>
4.269 + x$1 = a$1 \<and> x$1 = b$1 \<and> (a$2 \<le> x$2 \<and> x$2 \<le> b$2 \<or> b$2 \<le> x$2 \<and> x$2 \<le> a$2)"
4.270 + (is "_ = ?R")
4.271 +proof -
4.272 let ?L = "\<exists>u. (x $ 1 = (1 - u) * a $ 1 + u * b $ 1 \<and> x $ 2 = (1 - u) * a $ 2 + u * b $ 2) \<and> 0 \<le> u \<and> u \<le> 1"
4.273 - { presume "?L \<Longrightarrow> ?R" "?R \<Longrightarrow> ?L" thus ?thesis unfolding closed_segment_def mem_Collect_eq
4.274 - unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[THEN sym] vector_component_simps by blast }
4.275 - { assume ?L then guess u apply-apply(erule exE)apply(erule conjE)+ . note u=this
4.276 - { fix b a assume "b + u * a > a + u * b"
4.277 - hence "(1 - u) * b > (1 - u) * a" by(auto simp add:field_simps)
4.278 - hence "b \<ge> a" apply(drule_tac mult_less_imp_less_left) using u by auto
4.279 - hence "u * a \<le> u * b" apply-apply(rule mult_left_mono[OF _ u(3)])
4.280 - using u(3-4) by(auto simp add:field_simps) } note * = this
4.281 - { fix a b assume "u * b > u * a" hence "(1 - u) * a \<le> (1 - u) * b" apply-apply(rule mult_left_mono)
4.282 - apply(drule mult_less_imp_less_left) using u by auto
4.283 - hence "a + u * b \<le> b + u * a" by(auto simp add:field_simps) } note ** = this
4.284 - thus ?R unfolding u assms using u by(auto simp add:field_simps not_le intro:* **) }
4.285 - { assume ?R thus ?L proof(cases "x$2 = b$2")
4.286 - case True thus ?L apply(rule_tac x="(x$2 - a$2) / (b$2 - a$2)" in exI) unfolding assms True
4.287 - using `?R` by(auto simp add:field_simps)
4.288 - next case False thus ?L apply(rule_tac x="1 - (x$2 - b$2) / (a$2 - b$2)" in exI) unfolding assms using `?R`
4.289 - by(auto simp add:field_simps)
4.290 - qed } qed
4.291 + {
4.292 + presume "?L \<Longrightarrow> ?R" and "?R \<Longrightarrow> ?L"
4.293 + then show ?thesis
4.294 + unfolding closed_segment_def mem_Collect_eq
4.295 + unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[symmetric] vector_component_simps
4.296 + by blast
4.297 + }
4.298 + {
4.299 + assume ?L
4.300 + then guess u by (elim exE conjE) note u=this
4.301 + { fix b a
4.302 + assume "b + u * a > a + u * b"
4.303 + then have "(1 - u) * b > (1 - u) * a"
4.304 + by (auto simp add:field_simps)
4.305 + then have "b \<ge> a"
4.306 + apply (drule_tac mult_less_imp_less_left)
4.307 + using u
4.308 + apply auto
4.309 + done
4.310 + then have "u * a \<le> u * b"
4.311 + apply -
4.312 + apply (rule mult_left_mono[OF _ u(3)])
4.313 + using u(3-4)
4.314 + apply (auto simp add: field_simps)
4.315 + done
4.316 + } note * = this
4.317 + {
4.318 + fix a b
4.319 + assume "u * b > u * a"
4.320 + then have "(1 - u) * a \<le> (1 - u) * b"
4.321 + apply -
4.322 + apply (rule mult_left_mono)
4.323 + apply (drule mult_less_imp_less_left)
4.324 + using u
4.325 + apply auto
4.326 + done
4.327 + then have "a + u * b \<le> b + u * a"
4.328 + by (auto simp add: field_simps)
4.329 + } note ** = this
4.330 + then show ?R
4.331 + unfolding u assms
4.332 + using u
4.333 + by (auto simp add:field_simps not_le intro: * **)
4.334 + }
4.335 + {
4.336 + assume ?R
4.337 + then show ?L
4.338 + proof (cases "x$2 = b$2")
4.339 + case True
4.340 + then show ?L
4.341 + apply (rule_tac x="(x$2 - a$2) / (b$2 - a$2)" in exI)
4.342 + unfolding assms True
4.343 + using `?R`
4.344 + apply (auto simp add: field_simps)
4.345 + done
4.346 + next
4.347 + case False
4.348 + then show ?L
4.349 + apply (rule_tac x="1 - (x$2 - b$2) / (a$2 - b$2)" in exI)
4.350 + unfolding assms
4.351 + using `?R`
4.352 + apply (auto simp add: field_simps)
4.353 + done
4.354 + qed
4.355 + }
4.356 +qed
4.357
4.358 -lemma segment_horizontal: fixes a::"real^2" assumes "a$2 = b$2"
4.359 - shows "x \<in> closed_segment a b \<longleftrightarrow> (x$2 = a$2 \<and> x$2 = b$2 \<and>
4.360 - (a$1 \<le> x$1 \<and> x$1 \<le> b$1 \<or> b$1 \<le> x$1 \<and> x$1 \<le> a$1))" (is "_ = ?R")
4.361 -proof-
4.362 +lemma segment_horizontal:
4.363 + fixes a :: "real^2"
4.364 + assumes "a$2 = b$2"
4.365 + shows "x \<in> closed_segment a b \<longleftrightarrow>
4.366 + x$2 = a$2 \<and> x$2 = b$2 \<and> (a$1 \<le> x$1 \<and> x$1 \<le> b$1 \<or> b$1 \<le> x$1 \<and> x$1 \<le> a$1)"
4.367 + (is "_ = ?R")
4.368 +proof -
4.369 let ?L = "\<exists>u. (x $ 1 = (1 - u) * a $ 1 + u * b $ 1 \<and> x $ 2 = (1 - u) * a $ 2 + u * b $ 2) \<and> 0 \<le> u \<and> u \<le> 1"
4.370 - { presume "?L \<Longrightarrow> ?R" "?R \<Longrightarrow> ?L" thus ?thesis unfolding closed_segment_def mem_Collect_eq
4.371 - unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[THEN sym] vector_component_simps by blast }
4.372 - { assume ?L then guess u apply-apply(erule exE)apply(erule conjE)+ . note u=this
4.373 - { fix b a assume "b + u * a > a + u * b"
4.374 - hence "(1 - u) * b > (1 - u) * a" by(auto simp add:field_simps)
4.375 - hence "b \<ge> a" apply(drule_tac mult_less_imp_less_left) using u by auto
4.376 - hence "u * a \<le> u * b" apply-apply(rule mult_left_mono[OF _ u(3)])
4.377 - using u(3-4) by(auto simp add:field_simps) } note * = this
4.378 - { fix a b assume "u * b > u * a" hence "(1 - u) * a \<le> (1 - u) * b" apply-apply(rule mult_left_mono)
4.379 - apply(drule mult_less_imp_less_left) using u by auto
4.380 - hence "a + u * b \<le> b + u * a" by(auto simp add:field_simps) } note ** = this
4.381 - thus ?R unfolding u assms using u by(auto simp add:field_simps not_le intro:* **) }
4.382 - { assume ?R thus ?L proof(cases "x$1 = b$1")
4.383 - case True thus ?L apply(rule_tac x="(x$1 - a$1) / (b$1 - a$1)" in exI) unfolding assms True
4.384 - using `?R` by(auto simp add:field_simps)
4.385 - next case False thus ?L apply(rule_tac x="1 - (x$1 - b$1) / (a$1 - b$1)" in exI) unfolding assms using `?R`
4.386 - by(auto simp add:field_simps)
4.387 - qed } qed
4.388 + {
4.389 + presume "?L \<Longrightarrow> ?R" and "?R \<Longrightarrow> ?L"
4.390 + then show ?thesis
4.391 + unfolding closed_segment_def mem_Collect_eq
4.392 + unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[symmetric] vector_component_simps
4.393 + by blast
4.394 + }
4.395 + {
4.396 + assume ?L
4.397 + then guess u by (elim exE conjE) note u=this
4.398 + {
4.399 + fix b a
4.400 + assume "b + u * a > a + u * b"
4.401 + then have "(1 - u) * b > (1 - u) * a"
4.402 + by (auto simp add: field_simps)
4.403 + then have "b \<ge> a"
4.404 + apply (drule_tac mult_less_imp_less_left)
4.405 + using u
4.406 + apply auto
4.407 + done
4.408 + then have "u * a \<le> u * b"
4.409 + apply -
4.410 + apply (rule mult_left_mono[OF _ u(3)])
4.411 + using u(3-4)
4.412 + apply (auto simp add: field_simps)
4.413 + done
4.414 + } note * = this
4.415 + {
4.416 + fix a b
4.417 + assume "u * b > u * a"
4.418 + then have "(1 - u) * a \<le> (1 - u) * b"
4.419 + apply -
4.420 + apply (rule mult_left_mono)
4.421 + apply (drule mult_less_imp_less_left)
4.422 + using u
4.423 + apply auto
4.424 + done
4.425 + then have "a + u * b \<le> b + u * a"
4.426 + by (auto simp add: field_simps)
4.427 + } note ** = this
4.428 + then show ?R
4.429 + unfolding u assms
4.430 + using u
4.431 + by (auto simp add: field_simps not_le intro: * **)
4.432 + }
4.433 + {
4.434 + assume ?R
4.435 + then show ?L
4.436 + proof (cases "x$1 = b$1")
4.437 + case True
4.438 + then show ?L
4.439 + apply (rule_tac x="(x$1 - a$1) / (b$1 - a$1)" in exI)
4.440 + unfolding assms True
4.441 + using `?R`
4.442 + apply (auto simp add: field_simps)
4.443 + done
4.444 + next
4.445 + case False
4.446 + then show ?L
4.447 + apply (rule_tac x="1 - (x$1 - b$1) / (a$1 - b$1)" in exI)
4.448 + unfolding assms
4.449 + using `?R`
4.450 + apply (auto simp add: field_simps)
4.451 + done
4.452 + qed
4.453 + }
4.454 +qed
4.455
4.456 -subsection {*useful Fashoda corollary pointed out to me by Tom Hales. *}
4.457
4.458 -lemma fashoda_interlace: fixes a::"real^2"
4.459 - assumes "path f" "path g"
4.460 - "path_image f \<subseteq> {a..b}" "path_image g \<subseteq> {a..b}"
4.461 - "(pathstart f)$2 = a$2" "(pathfinish f)$2 = a$2"
4.462 - "(pathstart g)$2 = a$2" "(pathfinish g)$2 = a$2"
4.463 - "(pathstart f)$1 < (pathstart g)$1" "(pathstart g)$1 < (pathfinish f)$1"
4.464 - "(pathfinish f)$1 < (pathfinish g)$1"
4.465 - obtains z where "z \<in> path_image f" "z \<in> path_image g"
4.466 -proof-
4.467 - have "{a..b} \<noteq> {}" using path_image_nonempty using assms(3) by auto
4.468 +subsection {* Useful Fashoda corollary pointed out to me by Tom Hales *}
4.469 +
4.470 +lemma fashoda_interlace:
4.471 + fixes a :: "real^2"
4.472 + assumes "path f"
4.473 + and "path g"
4.474 + and "path_image f \<subseteq> {a..b}"
4.475 + and "path_image g \<subseteq> {a..b}"
4.476 + and "(pathstart f)$2 = a$2"
4.477 + and "(pathfinish f)$2 = a$2"
4.478 + and "(pathstart g)$2 = a$2"
4.479 + and "(pathfinish g)$2 = a$2"
4.480 + and "(pathstart f)$1 < (pathstart g)$1"
4.481 + and "(pathstart g)$1 < (pathfinish f)$1"
4.482 + and "(pathfinish f)$1 < (pathfinish g)$1"
4.483 + obtains z where "z \<in> path_image f" and "z \<in> path_image g"
4.484 +proof -
4.485 + have "{a..b} \<noteq> {}"
4.486 + using path_image_nonempty using assms(3) by auto
4.487 note ab=this[unfolded interval_eq_empty_cart not_ex forall_2 not_less]
4.488 - have "pathstart f \<in> {a..b}" "pathfinish f \<in> {a..b}" "pathstart g \<in> {a..b}" "pathfinish g \<in> {a..b}"
4.489 - using pathstart_in_path_image pathfinish_in_path_image using assms(3-4) by auto
4.490 + have "pathstart f \<in> {a..b}"
4.491 + and "pathfinish f \<in> {a..b}"
4.492 + and "pathstart g \<in> {a..b}"
4.493 + and "pathfinish g \<in> {a..b}"
4.494 + using pathstart_in_path_image pathfinish_in_path_image
4.495 + using assms(3-4)
4.496 + by auto
4.497 note startfin = this[unfolded mem_interval_cart forall_2]
4.498 let ?P1 = "linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2]) +++
4.499 linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f) +++ f +++
4.500 @@ -455,7 +666,7 @@
4.501 linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3])"
4.502 let ?a = "vector[a$1 - 2, a$2 - 3]"
4.503 let ?b = "vector[b$1 + 2, b$2 + 3]"
4.504 - have P1P2:"path_image ?P1 = path_image (linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2])) \<union>
4.505 + have P1P2: "path_image ?P1 = path_image (linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2])) \<union>
4.506 path_image (linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f)) \<union> path_image f \<union>
4.507 path_image (linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2])) \<union>
4.508 path_image (linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2]))"
4.509 @@ -464,58 +675,128 @@
4.510 path_image(linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1])) \<union>
4.511 path_image(linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3]))" using assms(1-2)
4.512 by(auto simp add: path_image_join path_linepath)
4.513 - have abab: "{a..b} \<subseteq> {?a..?b}" by(auto simp add:less_eq_vec_def forall_2 vector_2)
4.514 - guess z apply(rule fashoda[of ?P1 ?P2 ?a ?b])
4.515 - unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2 proof-
4.516 - show "path ?P1" "path ?P2" using assms by auto
4.517 - have "path_image ?P1 \<subseteq> {?a .. ?b}" unfolding P1P2 path_image_linepath apply(rule Un_least)+ defer 3
4.518 - apply(rule_tac[1-4] convex_interval(1)[unfolded convex_contains_segment,rule_format])
4.519 - unfolding mem_interval_cart forall_2 vector_2 using ab startfin abab assms(3)
4.520 - using assms(9-) unfolding assms by(auto simp add:field_simps)
4.521 - thus "path_image ?P1 \<subseteq> {?a .. ?b}" .
4.522 - have "path_image ?P2 \<subseteq> {?a .. ?b}" unfolding P1P2 path_image_linepath apply(rule Un_least)+ defer 2
4.523 - apply(rule_tac[1-4] convex_interval(1)[unfolded convex_contains_segment,rule_format])
4.524 - unfolding mem_interval_cart forall_2 vector_2 using ab startfin abab assms(4)
4.525 - using assms(9-) unfolding assms by(auto simp add:field_simps)
4.526 - thus "path_image ?P2 \<subseteq> {?a .. ?b}" .
4.527 - show "a $ 1 - 2 = a $ 1 - 2" "b $ 1 + 2 = b $ 1 + 2" "pathstart g $ 2 - 3 = a $ 2 - 3" "b $ 2 + 3 = b $ 2 + 3"
4.528 - by(auto simp add: assms)
4.529 - qed note z=this[unfolded P1P2 path_image_linepath]
4.530 - show thesis apply(rule that[of z]) proof-
4.531 + have abab: "{a..b} \<subseteq> {?a..?b}"
4.532 + by (auto simp add:less_eq_vec_def forall_2 vector_2)
4.533 + guess z
4.534 + apply (rule fashoda[of ?P1 ?P2 ?a ?b])
4.535 + unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2
4.536 + proof -
4.537 + show "path ?P1" and "path ?P2"
4.538 + using assms by auto
4.539 + have "path_image ?P1 \<subseteq> {?a .. ?b}"
4.540 + unfolding P1P2 path_image_linepath
4.541 + apply (rule Un_least)+
4.542 + defer 3
4.543 + apply (rule_tac[1-4] convex_interval(1)[unfolded convex_contains_segment,rule_format])
4.544 + unfolding mem_interval_cart forall_2 vector_2
4.545 + using ab startfin abab assms(3)
4.546 + using assms(9-)
4.547 + unfolding assms
4.548 + apply (auto simp add: field_simps)
4.549 + done
4.550 + then show "path_image ?P1 \<subseteq> {?a .. ?b}" .
4.551 + have "path_image ?P2 \<subseteq> {?a .. ?b}"
4.552 + unfolding P1P2 path_image_linepath
4.553 + apply (rule Un_least)+
4.554 + defer 2
4.555 + apply (rule_tac[1-4] convex_interval(1)[unfolded convex_contains_segment,rule_format])
4.556 + unfolding mem_interval_cart forall_2 vector_2
4.557 + using ab startfin abab assms(4)
4.558 + using assms(9-)
4.559 + unfolding assms
4.560 + apply (auto simp add: field_simps)
4.561 + done
4.562 + then show "path_image ?P2 \<subseteq> {?a .. ?b}" .
4.563 + show "a $ 1 - 2 = a $ 1 - 2"
4.564 + and "b $ 1 + 2 = b $ 1 + 2"
4.565 + and "pathstart g $ 2 - 3 = a $ 2 - 3"
4.566 + and "b $ 2 + 3 = b $ 2 + 3"
4.567 + by (auto simp add: assms)
4.568 + qed
4.569 + note z=this[unfolded P1P2 path_image_linepath]
4.570 + show thesis
4.571 + apply (rule that[of z])
4.572 + proof -
4.573 have "(z \<in> closed_segment (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) \<or>
4.574 - z \<in> closed_segment (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f)) \<or>
4.575 - z \<in> closed_segment (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) \<or>
4.576 - z \<in> closed_segment (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]) \<Longrightarrow>
4.577 - (((z \<in> closed_segment (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g)) \<or>
4.578 - z \<in> closed_segment (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1])) \<or>
4.579 - z \<in> closed_segment (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1])) \<or>
4.580 - z \<in> closed_segment (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]) \<Longrightarrow> False"
4.581 - apply(simp only: segment_vertical segment_horizontal vector_2) proof- case goal1 note as=this
4.582 - have "pathfinish f \<in> {a..b}" using assms(3) pathfinish_in_path_image[of f] by auto
4.583 - hence "1 + b $ 1 \<le> pathfinish f $ 1 \<Longrightarrow> False" unfolding mem_interval_cart forall_2 by auto
4.584 - hence "z$1 \<noteq> pathfinish f$1" using as(2) using assms ab by(auto simp add:field_simps)
4.585 - moreover have "pathstart f \<in> {a..b}" using assms(3) pathstart_in_path_image[of f] by auto
4.586 - hence "1 + b $ 1 \<le> pathstart f $ 1 \<Longrightarrow> False" unfolding mem_interval_cart forall_2 by auto
4.587 - hence "z$1 \<noteq> pathstart f$1" using as(2) using assms ab by(auto simp add:field_simps)
4.588 - ultimately have *:"z$2 = a$2 - 2" using goal1(1) by auto
4.589 - have "z$1 \<noteq> pathfinish g$1" using as(2) using assms ab by(auto simp add:field_simps *)
4.590 - moreover have "pathstart g \<in> {a..b}" using assms(4) pathstart_in_path_image[of g] by auto
4.591 + z \<in> closed_segment (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f)) \<or>
4.592 + z \<in> closed_segment (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) \<or>
4.593 + z \<in> closed_segment (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]) \<Longrightarrow>
4.594 + (((z \<in> closed_segment (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g)) \<or>
4.595 + z \<in> closed_segment (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1])) \<or>
4.596 + z \<in> closed_segment (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1])) \<or>
4.597 + z \<in> closed_segment (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]) \<Longrightarrow> False"
4.598 + apply (simp only: segment_vertical segment_horizontal vector_2)
4.599 + proof -
4.600 + case goal1 note as=this
4.601 + have "pathfinish f \<in> {a..b}"
4.602 + using assms(3) pathfinish_in_path_image[of f] by auto
4.603 + then have "1 + b $ 1 \<le> pathfinish f $ 1 \<Longrightarrow> False"
4.604 + unfolding mem_interval_cart forall_2 by auto
4.605 + then have "z$1 \<noteq> pathfinish f$1"
4.606 + using as(2)
4.607 + using assms ab
4.608 + by (auto simp add: field_simps)
4.609 + moreover have "pathstart f \<in> {a..b}"
4.610 + using assms(3) pathstart_in_path_image[of f]
4.611 + by auto
4.612 + then have "1 + b $ 1 \<le> pathstart f $ 1 \<Longrightarrow> False"
4.613 + unfolding mem_interval_cart forall_2
4.614 + by auto
4.615 + then have "z$1 \<noteq> pathstart f$1"
4.616 + using as(2) using assms ab
4.617 + by (auto simp add: field_simps)
4.618 + ultimately have *: "z$2 = a$2 - 2"
4.619 + using goal1(1)
4.620 + by auto
4.621 + have "z$1 \<noteq> pathfinish g$1"
4.622 + using as(2)
4.623 + using assms ab
4.624 + by (auto simp add: field_simps *)
4.625 + moreover have "pathstart g \<in> {a..b}"
4.626 + using assms(4) pathstart_in_path_image[of g]
4.627 + by auto
4.628 note this[unfolded mem_interval_cart forall_2]
4.629 - hence "z$1 \<noteq> pathstart g$1" using as(1) using assms ab by(auto simp add:field_simps *)
4.630 + then have "z$1 \<noteq> pathstart g$1"
4.631 + using as(1)
4.632 + using assms ab
4.633 + by (auto simp add: field_simps *)
4.634 ultimately have "a $ 2 - 1 \<le> z $ 2 \<and> z $ 2 \<le> b $ 2 + 3 \<or> b $ 2 + 3 \<le> z $ 2 \<and> z $ 2 \<le> a $ 2 - 1"
4.635 - using as(2) unfolding * assms by(auto simp add:field_simps)
4.636 - thus False unfolding * using ab by auto
4.637 - qed hence "z \<in> path_image f \<or> z \<in> path_image g" using z unfolding Un_iff by blast
4.638 - hence z':"z\<in>{a..b}" using assms(3-4) by auto
4.639 - have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart f $ 1 \<or> z $ 1 = pathfinish f $ 1) \<Longrightarrow> (z = pathstart f \<or> z = pathfinish f)"
4.640 - unfolding vec_eq_iff forall_2 assms by auto
4.641 - with z' show "z\<in>path_image f" using z(1) unfolding Un_iff mem_interval_cart forall_2 apply-
4.642 - apply(simp only: segment_vertical segment_horizontal vector_2) unfolding assms by auto
4.643 - have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart g $ 1 \<or> z $ 1 = pathfinish g $ 1) \<Longrightarrow> (z = pathstart g \<or> z = pathfinish g)"
4.644 - unfolding vec_eq_iff forall_2 assms by auto
4.645 - with z' show "z\<in>path_image g" using z(2) unfolding Un_iff mem_interval_cart forall_2 apply-
4.646 - apply(simp only: segment_vertical segment_horizontal vector_2) unfolding assms by auto
4.647 - qed qed
4.648 + using as(2)
4.649 + unfolding * assms
4.650 + by (auto simp add: field_simps)
4.651 + then show False
4.652 + unfolding * using ab by auto
4.653 + qed
4.654 + then have "z \<in> path_image f \<or> z \<in> path_image g"
4.655 + using z unfolding Un_iff by blast
4.656 + then have z': "z \<in> {a..b}"
4.657 + using assms(3-4)
4.658 + by auto
4.659 + have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart f $ 1 \<or> z $ 1 = pathfinish f $ 1) \<Longrightarrow>
4.660 + z = pathstart f \<or> z = pathfinish f"
4.661 + unfolding vec_eq_iff forall_2 assms
4.662 + by auto
4.663 + with z' show "z \<in> path_image f"
4.664 + using z(1)
4.665 + unfolding Un_iff mem_interval_cart forall_2
4.666 + apply -
4.667 + apply (simp only: segment_vertical segment_horizontal vector_2)
4.668 + unfolding assms
4.669 + apply auto
4.670 + done
4.671 + have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart g $ 1 \<or> z $ 1 = pathfinish g $ 1) \<Longrightarrow>
4.672 + z = pathstart g \<or> z = pathfinish g"
4.673 + unfolding vec_eq_iff forall_2 assms
4.674 + by auto
4.675 + with z' show "z \<in> path_image g"
4.676 + using z(2)
4.677 + unfolding Un_iff mem_interval_cart forall_2
4.678 + apply (simp only: segment_vertical segment_horizontal vector_2)
4.679 + unfolding assms
4.680 + apply auto
4.681 + done
4.682 + qed
4.683 +qed
4.684
4.685 (** The Following still needs to be translated. Maybe I will do that later.
4.686