1.1 --- a/src/HOL/Multivariate_Analysis/Fashoda.thy Wed Aug 10 10:13:16 2011 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Wed Aug 10 13:13:37 2011 -0700
1.3 @@ -46,7 +46,7 @@
1.4 apply(rule assms)+ apply(rule continuous_on_compose,subst sqprojection_def)
1.5 apply(rule continuous_on_mul ) apply(rule continuous_at_imp_continuous_on,rule) apply(rule continuous_at_inv[unfolded o_def])
1.6 apply(rule continuous_at_infnorm) unfolding infnorm_eq_0 defer apply(rule continuous_on_id) apply(rule linear_continuous_on) proof-
1.7 - show "bounded_linear negatex" apply(rule bounded_linearI') unfolding Cart_eq proof(rule_tac[!] allI) fix i::2 and x y::"real^2" and c::real
1.8 + show "bounded_linear negatex" apply(rule bounded_linearI') unfolding vec_eq_iff proof(rule_tac[!] allI) fix i::2 and x y::"real^2" and c::real
1.9 show "negatex (x + y) $ i = (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i"
1.10 apply-apply(case_tac[!] "i\<noteq>1") prefer 3 apply(drule_tac[1-2] 21)
1.11 unfolding negatex_def by(auto simp add:vector_2 ) qed qed(insert x0, auto)
1.12 @@ -66,7 +66,7 @@
1.13 apply- apply(rule_tac[!] allI impI)+ proof- fix x::"real^2" and i::2 assume x:"x\<noteq>0"
1.14 have "inverse (infnorm x) > 0" using x[unfolded infnorm_pos_lt[THEN sym]] by auto
1.15 thus "(0 < sqprojection x $ i) = (0 < x $ i)" "(sqprojection x $ i < 0) = (x $ i < 0)"
1.16 - unfolding sqprojection_def vector_component_simps Cart_nth.scaleR real_scaleR_def
1.17 + unfolding sqprojection_def vector_component_simps vec_nth.scaleR real_scaleR_def
1.18 unfolding zero_less_mult_iff mult_less_0_iff by(auto simp add:field_simps) qed
1.19 note lem3 = this[rule_format]
1.20 have x1:"x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}" using x(1) unfolding mem_interval_cart by auto
1.21 @@ -77,7 +77,7 @@
1.22 next assume as:"x$1 = 1"
1.23 hence *:"f (x $ 1) $ 1 = 1" using assms(6) by auto
1.24 have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0"
1.25 - using x(2)[unfolded o_def Cart_eq,THEN spec[where x=1]]
1.26 + using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]]
1.27 unfolding as negatex_def vector_2 by auto moreover
1.28 from x1 have "g (x $ 2) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto
1.29 ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
1.30 @@ -85,7 +85,7 @@
1.31 next assume as:"x$1 = -1"
1.32 hence *:"f (x $ 1) $ 1 = - 1" using assms(5) by auto
1.33 have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0"
1.34 - using x(2)[unfolded o_def Cart_eq,THEN spec[where x=1]]
1.35 + using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]]
1.36 unfolding as negatex_def vector_2 by auto moreover
1.37 from x1 have "g (x $ 2) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto
1.38 ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
1.39 @@ -93,7 +93,7 @@
1.40 next assume as:"x$2 = 1"
1.41 hence *:"g (x $ 2) $ 2 = 1" using assms(8) by auto
1.42 have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0"
1.43 - using x(2)[unfolded o_def Cart_eq,THEN spec[where x=2]]
1.44 + using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]]
1.45 unfolding as negatex_def vector_2 by auto moreover
1.46 from x1 have "f (x $ 1) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto
1.47 ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
1.48 @@ -101,7 +101,7 @@
1.49 next assume as:"x$2 = -1"
1.50 hence *:"g (x $ 2) $ 2 = - 1" using assms(7) by auto
1.51 have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0"
1.52 - using x(2)[unfolded o_def Cart_eq,THEN spec[where x=2]]
1.53 + using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]]
1.54 unfolding as negatex_def vector_2 by auto moreover
1.55 from x1 have "f (x $ 1) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto
1.56 ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
1.57 @@ -120,7 +120,7 @@
1.58 have *:"continuous_on {- 1..1} iscale" unfolding iscale_def by(rule continuous_on_intros)+
1.59 show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)"
1.60 apply-apply(rule_tac[!] continuous_on_compose[OF *]) apply(rule_tac[!] continuous_on_subset[OF _ isc])
1.61 - by(rule assms)+ have *:"(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1" unfolding Cart_eq by auto
1.62 + by(rule assms)+ have *:"(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1" unfolding vec_eq_iff by auto
1.63 show "(f \<circ> iscale) (- 1) $ 1 = - 1" "(f \<circ> iscale) 1 $ 1 = 1" "(g \<circ> iscale) (- 1) $ 2 = -1" "(g \<circ> iscale) 1 $ 2 = 1"
1.64 unfolding o_def iscale_def using assms by(auto simp add:*) qed
1.65 then guess s .. from this(2) guess t .. note st=this
1.66 @@ -132,7 +132,7 @@
1.67 (* move *)
1.68 lemma interval_bij_bij_cart: fixes x::"real^'n" assumes "\<forall>i. a$i < b$i \<and> u$i < v$i"
1.69 shows "interval_bij (a,b) (u,v) (interval_bij (u,v) (a,b) x) = x"
1.70 - unfolding interval_bij_cart split_conv Cart_eq Cart_lambda_beta
1.71 + unfolding interval_bij_cart split_conv vec_eq_iff vec_lambda_beta
1.72 apply(rule,insert assms,erule_tac x=i in allE) by auto
1.73
1.74 lemma fashoda: fixes b::"real^2"
1.75 @@ -142,23 +142,23 @@
1.76 obtains z where "z \<in> path_image f" "z \<in> path_image g" proof-
1.77 fix P Q S presume "P \<or> Q \<or> S" "P \<Longrightarrow> thesis" "Q \<Longrightarrow> thesis" "S \<Longrightarrow> thesis" thus thesis by auto
1.78 next have "{a..b} \<noteq> {}" using assms(3) using path_image_nonempty by auto
1.79 - hence "a \<le> b" unfolding interval_eq_empty_cart vector_le_def by(auto simp add: not_less)
1.80 - thus "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)" unfolding vector_le_def forall_2 by auto
1.81 + hence "a \<le> b" unfolding interval_eq_empty_cart less_eq_vec_def by(auto simp add: not_less)
1.82 + 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
1.83 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)
1.84 apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image)
1.85 unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"]
1.86 - unfolding pathstart_def by(auto simp add: vector_le_def) then guess z .. note z=this
1.87 + unfolding pathstart_def by(auto simp add: less_eq_vec_def) then guess z .. note z=this
1.88 have "z \<in> {a..b}" using z(1) assms(4) unfolding path_image_def by blast
1.89 - hence "z = f 0" unfolding Cart_eq forall_2 unfolding z(2) pathstart_def
1.90 + hence "z = f 0" unfolding vec_eq_iff forall_2 unfolding z(2) pathstart_def
1.91 using assms(3)[unfolded path_image_def subset_eq mem_interval_cart,rule_format,of "f 0" 1]
1.92 unfolding mem_interval_cart apply(erule_tac x=1 in allE) using as by auto
1.93 thus thesis apply-apply(rule that[OF _ z(1)]) unfolding path_image_def by auto
1.94 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)
1.95 apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image)
1.96 unfolding assms using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"]
1.97 - unfolding pathstart_def by(auto simp add: vector_le_def) then guess z .. note z=this
1.98 + unfolding pathstart_def by(auto simp add: less_eq_vec_def) then guess z .. note z=this
1.99 have "z \<in> {a..b}" using z(1) assms(3) unfolding path_image_def by blast
1.100 - hence "z = g 0" unfolding Cart_eq forall_2 unfolding z(2) pathstart_def
1.101 + hence "z = g 0" unfolding vec_eq_iff forall_2 unfolding z(2) pathstart_def
1.102 using assms(4)[unfolded path_image_def subset_eq mem_interval_cart,rule_format,of "g 0" 2]
1.103 unfolding mem_interval_cart apply(erule_tac x=2 in allE) using as by auto
1.104 thus thesis apply-apply(rule that[OF z(1)]) unfolding path_image_def by auto
1.105 @@ -180,7 +180,7 @@
1.106 "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1"
1.107 "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1"
1.108 "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1"
1.109 - unfolding interval_bij_cart Cart_lambda_beta vector_component_simps o_def split_conv
1.110 + unfolding interval_bij_cart vec_lambda_beta vector_component_simps o_def split_conv
1.111 unfolding assms[unfolded pathstart_def pathfinish_def] using as by auto qed note z=this
1.112 from z(1) guess zf unfolding image_iff .. note zf=this
1.113 from z(2) guess zg unfolding image_iff .. note zg=this
1.114 @@ -197,7 +197,7 @@
1.115 proof-
1.116 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"
1.117 { presume "?L \<Longrightarrow> ?R" "?R \<Longrightarrow> ?L" thus ?thesis unfolding closed_segment_def mem_Collect_eq
1.118 - unfolding Cart_eq forall_2 smult_conv_scaleR[THEN sym] vector_component_simps by blast }
1.119 + unfolding vec_eq_iff forall_2 smult_conv_scaleR[THEN sym] vector_component_simps by blast }
1.120 { assume ?L then guess u apply-apply(erule exE)apply(erule conjE)+ . note u=this
1.121 { fix b a assume "b + u * a > a + u * b"
1.122 hence "(1 - u) * b > (1 - u) * a" by(auto simp add:field_simps)
1.123 @@ -221,7 +221,7 @@
1.124 proof-
1.125 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"
1.126 { presume "?L \<Longrightarrow> ?R" "?R \<Longrightarrow> ?L" thus ?thesis unfolding closed_segment_def mem_Collect_eq
1.127 - unfolding Cart_eq forall_2 smult_conv_scaleR[THEN sym] vector_component_simps by blast }
1.128 + unfolding vec_eq_iff forall_2 smult_conv_scaleR[THEN sym] vector_component_simps by blast }
1.129 { assume ?L then guess u apply-apply(erule exE)apply(erule conjE)+ . note u=this
1.130 { fix b a assume "b + u * a > a + u * b"
1.131 hence "(1 - u) * b > (1 - u) * a" by(auto simp add:field_simps)
1.132 @@ -274,7 +274,7 @@
1.133 path_image(linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1])) \<union>
1.134 path_image(linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3]))" using assms(1-2)
1.135 by(auto simp add: path_image_join path_linepath)
1.136 - have abab: "{a..b} \<subseteq> {?a..?b}" by(auto simp add:vector_le_def forall_2 vector_2)
1.137 + have abab: "{a..b} \<subseteq> {?a..?b}" by(auto simp add:less_eq_vec_def forall_2 vector_2)
1.138 guess z apply(rule fashoda[of ?P1 ?P2 ?a ?b])
1.139 unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2 proof-
1.140 show "path ?P1" "path ?P2" using assms by auto
1.141 @@ -318,11 +318,11 @@
1.142 qed hence "z \<in> path_image f \<or> z \<in> path_image g" using z unfolding Un_iff by blast
1.143 hence z':"z\<in>{a..b}" using assms(3-4) by auto
1.144 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)"
1.145 - unfolding Cart_eq forall_2 assms by auto
1.146 + unfolding vec_eq_iff forall_2 assms by auto
1.147 with z' show "z\<in>path_image f" using z(1) unfolding Un_iff mem_interval_cart forall_2 apply-
1.148 apply(simp only: segment_vertical segment_horizontal vector_2) unfolding assms by auto
1.149 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)"
1.150 - unfolding Cart_eq forall_2 assms by auto
1.151 + unfolding vec_eq_iff forall_2 assms by auto
1.152 with z' show "z\<in>path_image g" using z(2) unfolding Un_iff mem_interval_cart forall_2 apply-
1.153 apply(simp only: segment_vertical segment_horizontal vector_2) unfolding assms by auto
1.154 qed qed