--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Apr 27 16:24:57 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Apr 27 11:17:50 2010 -0700
@@ -1430,550 +1430,4 @@
unfolding interval_bij_def split_conv Cart_eq Cart_lambda_beta
apply(rule,insert assms,erule_tac x=i in allE) by auto
-subsection {*Fashoda meet theorem. *}
-
-lemma infnorm_2: "infnorm (x::real^2) = max (abs(x$1)) (abs(x$2))"
- unfolding infnorm_def UNIV_2 apply(rule Sup_eq) by auto
-
-lemma infnorm_eq_1_2: "infnorm (x::real^2) = 1 \<longleftrightarrow>
- (abs(x$1) \<le> 1 \<and> abs(x$2) \<le> 1 \<and> (x$1 = -1 \<or> x$1 = 1 \<or> x$2 = -1 \<or> x$2 = 1))"
- unfolding infnorm_2 by auto
-
-lemma infnorm_eq_1_imp: assumes "infnorm (x::real^2) = 1" shows "abs(x$1) \<le> 1" "abs(x$2) \<le> 1"
- using assms unfolding infnorm_eq_1_2 by auto
-
-lemma fashoda_unit: fixes f g::"real \<Rightarrow> real^2"
- assumes "f ` {- 1..1} \<subseteq> {- 1..1}" "g ` {- 1..1} \<subseteq> {- 1..1}"
- "continuous_on {- 1..1} f" "continuous_on {- 1..1} g"
- "f (- 1)$1 = - 1" "f 1$1 = 1" "g (- 1) $2 = -1" "g 1 $2 = 1"
- shows "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. f s = g t" proof(rule ccontr)
- case goal1 note as = this[unfolded bex_simps,rule_format]
- def sqprojection \<equiv> "\<lambda>z::real^2. (inverse (infnorm z)) *\<^sub>R z"
- def negatex \<equiv> "\<lambda>x::real^2. (vector [-(x$1), x$2])::real^2"
- have lem1:"\<forall>z::real^2. infnorm(negatex z) = infnorm z"
- unfolding negatex_def infnorm_2 vector_2 by auto
- have lem2:"\<forall>z. z\<noteq>0 \<longrightarrow> infnorm(sqprojection z) = 1" unfolding sqprojection_def
- unfolding infnorm_mul[unfolded smult_conv_scaleR] unfolding abs_inverse real_abs_infnorm
- unfolding infnorm_eq_0[THEN sym] by auto
- let ?F = "(\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w)"
- have *:"\<And>i. (\<lambda>x::real^2. x $ i) ` {- 1..1} = {- 1..1::real}"
- apply(rule set_ext) unfolding image_iff Bex_def mem_interval apply rule defer
- apply(rule_tac x="vec x" in exI) by auto
- { fix x assume "x \<in> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w) ` {- 1..1::real^2}"
- then guess w unfolding image_iff .. note w = this
- hence "x \<noteq> 0" using as[of "w$1" "w$2"] unfolding mem_interval by auto} note x0=this
- have 21:"\<And>i::2. i\<noteq>1 \<Longrightarrow> i=2" using UNIV_2 by auto
- have 1:"{- 1<..<1::real^2} \<noteq> {}" unfolding interval_eq_empty by auto
- have 2:"continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)" apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+
- prefer 2 apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+ unfolding *
- apply(rule assms)+ apply(rule continuous_on_compose,subst sqprojection_def)
- apply(rule continuous_on_mul ) apply(rule continuous_at_imp_continuous_on,rule) apply(rule continuous_at_inv[unfolded o_def])
- apply(rule continuous_at_infnorm) unfolding infnorm_eq_0 defer apply(rule continuous_on_id) apply(rule linear_continuous_on) proof-
- 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
- show "negatex (x + y) $ i = (negatex x + negatex y) $ i" "negatex (c *s x) $ i = (c *s negatex x) $ i"
- apply-apply(case_tac[!] "i\<noteq>1") prefer 3 apply(drule_tac[1-2] 21)
- unfolding negatex_def by(auto simp add:vector_2 ) qed qed(insert x0, auto)
- have 3:"(negatex \<circ> sqprojection \<circ> ?F) ` {- 1..1} \<subseteq> {- 1..1}" unfolding subset_eq apply rule proof-
- case goal1 then guess y unfolding image_iff .. note y=this have "?F y \<noteq> 0" apply(rule x0) using y(1) by auto
- hence *:"infnorm (sqprojection (?F y)) = 1" unfolding y o_def apply- by(rule lem2[rule_format])
- have "infnorm x = 1" unfolding *[THEN sym] y o_def by(rule lem1[rule_format])
- thus "x\<in>{- 1..1}" unfolding mem_interval infnorm_2 apply- apply rule
- proof-case goal1 thus ?case apply(cases "i=1") defer apply(drule 21) by auto qed qed
- guess x apply(rule brouwer_weak[of "{- 1..1::real^2}" "negatex \<circ> sqprojection \<circ> ?F"])
- apply(rule compact_interval convex_interval)+ unfolding interior_closed_interval
- apply(rule 1 2 3)+ . note x=this
- have "?F x \<noteq> 0" apply(rule x0) using x(1) by auto
- hence *:"infnorm (sqprojection (?F x)) = 1" unfolding o_def by(rule lem2[rule_format])
- have nx:"infnorm x = 1" apply(subst x(2)[THEN sym]) unfolding *[THEN sym] o_def by(rule lem1[rule_format])
- have "\<forall>x i. x \<noteq> 0 \<longrightarrow> (0 < (sqprojection x)$i \<longleftrightarrow> 0 < x$i)" "\<forall>x i. x \<noteq> 0 \<longrightarrow> ((sqprojection x)$i < 0 \<longleftrightarrow> x$i < 0)"
- apply- apply(rule_tac[!] allI impI)+ proof- fix x::"real^2" and i::2 assume x:"x\<noteq>0"
- have "inverse (infnorm x) > 0" using x[unfolded infnorm_pos_lt[THEN sym]] by auto
- thus "(0 < sqprojection x $ i) = (0 < x $ i)" "(sqprojection x $ i < 0) = (x $ i < 0)"
- unfolding sqprojection_def vector_component_simps Cart_nth.scaleR real_scaleR_def
- unfolding zero_less_mult_iff mult_less_0_iff by(auto simp add:field_simps) qed
- note lem3 = this[rule_format]
- have x1:"x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}" using x(1) unfolding mem_interval by auto
- hence nz:"f (x $ 1) - g (x $ 2) \<noteq> 0" unfolding right_minus_eq apply-apply(rule as) by auto
- have "x $ 1 = -1 \<or> x $ 1 = 1 \<or> x $ 2 = -1 \<or> x $ 2 = 1" using nx unfolding infnorm_eq_1_2 by auto
- thus False proof- fix P Q R S
- presume "P \<or> Q \<or> R \<or> S" "P\<Longrightarrow>False" "Q\<Longrightarrow>False" "R\<Longrightarrow>False" "S\<Longrightarrow>False" thus False by auto
- next assume as:"x$1 = 1"
- hence *:"f (x $ 1) $ 1 = 1" using assms(6) by auto
- have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0"
- using x(2)[unfolded o_def Cart_eq,THEN spec[where x=1]]
- unfolding as negatex_def vector_2 by auto moreover
- from x1 have "g (x $ 2) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto
- ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval
- apply(erule_tac x=1 in allE) by auto
- next assume as:"x$1 = -1"
- hence *:"f (x $ 1) $ 1 = - 1" using assms(5) by auto
- have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0"
- using x(2)[unfolded o_def Cart_eq,THEN spec[where x=1]]
- unfolding as negatex_def vector_2 by auto moreover
- from x1 have "g (x $ 2) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto
- ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval
- apply(erule_tac x=1 in allE) by auto
- next assume as:"x$2 = 1"
- hence *:"g (x $ 2) $ 2 = 1" using assms(8) by auto
- have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0"
- using x(2)[unfolded o_def Cart_eq,THEN spec[where x=2]]
- unfolding as negatex_def vector_2 by auto moreover
- from x1 have "f (x $ 1) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto
- ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval
- apply(erule_tac x=2 in allE) by auto
- next assume as:"x$2 = -1"
- hence *:"g (x $ 2) $ 2 = - 1" using assms(7) by auto
- have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0"
- using x(2)[unfolded o_def Cart_eq,THEN spec[where x=2]]
- unfolding as negatex_def vector_2 by auto moreover
- from x1 have "f (x $ 1) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto
- ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval
- apply(erule_tac x=2 in allE) by auto qed(auto) qed
-
-lemma fashoda_unit_path: fixes f ::"real \<Rightarrow> real^2" and g ::"real \<Rightarrow> real^2"
- assumes "path f" "path g" "path_image f \<subseteq> {- 1..1}" "path_image g \<subseteq> {- 1..1}"
- "(pathstart f)$1 = -1" "(pathfinish f)$1 = 1" "(pathstart g)$2 = -1" "(pathfinish g)$2 = 1"
- obtains z where "z \<in> path_image f" "z \<in> path_image g" proof-
- note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
- def iscale \<equiv> "\<lambda>z::real. inverse 2 *\<^sub>R (z + 1)"
- have isc:"iscale ` {- 1..1} \<subseteq> {0..1}" unfolding iscale_def by(auto)
- have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t" proof(rule fashoda_unit)
- show "(f \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}" "(g \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}"
- using isc and assms(3-4) unfolding image_compose by auto
- have *:"continuous_on {- 1..1} iscale" unfolding iscale_def by(rule continuous_on_intros)+
- show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)"
- apply-apply(rule_tac[!] continuous_on_compose[OF *]) apply(rule_tac[!] continuous_on_subset[OF _ isc])
- by(rule assms)+ have *:"(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1" unfolding Cart_eq by auto
- 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"
- unfolding o_def iscale_def using assms by(auto simp add:*) qed
- then guess s .. from this(2) guess t .. note st=this
- show thesis apply(rule_tac z="f (iscale s)" in that)
- using st `s\<in>{- 1..1}` unfolding o_def path_image_def image_iff apply-
- apply(rule_tac x="iscale s" in bexI) prefer 3 apply(rule_tac x="iscale t" in bexI)
- using isc[unfolded subset_eq, rule_format] by auto qed
-
-lemma fashoda: fixes b::"real^2"
- assumes "path f" "path g" "path_image f \<subseteq> {a..b}" "path_image g \<subseteq> {a..b}"
- "(pathstart f)$1 = a$1" "(pathfinish f)$1 = b$1"
- "(pathstart g)$2 = a$2" "(pathfinish g)$2 = b$2"
- obtains z where "z \<in> path_image f" "z \<in> path_image g" proof-
- fix P Q S presume "P \<or> Q \<or> S" "P \<Longrightarrow> thesis" "Q \<Longrightarrow> thesis" "S \<Longrightarrow> thesis" thus thesis by auto
-next have "{a..b} \<noteq> {}" using assms(3) using path_image_nonempty by auto
- hence "a \<le> b" unfolding interval_eq_empty vector_le_def by(auto simp add: not_less)
- 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
-next assume as:"a$1 = b$1" have "\<exists>z\<in>path_image g. z$2 = (pathstart f)$2" apply(rule connected_ivt_component)
- apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image)
- unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"]
- unfolding pathstart_def by(auto simp add: vector_le_def) then guess z .. note z=this
- have "z \<in> {a..b}" using z(1) assms(4) unfolding path_image_def by blast
- hence "z = f 0" unfolding Cart_eq forall_2 unfolding z(2) pathstart_def
- using assms(3)[unfolded path_image_def subset_eq mem_interval,rule_format,of "f 0" 1]
- unfolding mem_interval apply(erule_tac x=1 in allE) using as by auto
- thus thesis apply-apply(rule that[OF _ z(1)]) unfolding path_image_def by auto
-next assume as:"a$2 = b$2" have "\<exists>z\<in>path_image f. z$1 = (pathstart g)$1" apply(rule connected_ivt_component)
- apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image)
- unfolding assms using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"]
- unfolding pathstart_def by(auto simp add: vector_le_def) then guess z .. note z=this
- have "z \<in> {a..b}" using z(1) assms(3) unfolding path_image_def by blast
- hence "z = g 0" unfolding Cart_eq forall_2 unfolding z(2) pathstart_def
- using assms(4)[unfolded path_image_def subset_eq mem_interval,rule_format,of "g 0" 2]
- unfolding mem_interval apply(erule_tac x=2 in allE) using as by auto
- thus thesis apply-apply(rule that[OF z(1)]) unfolding path_image_def by auto
-next assume as:"a $ 1 < b $ 1 \<and> a $ 2 < b $ 2"
- have int_nem:"{- 1..1::real^2} \<noteq> {}" unfolding interval_eq_empty by auto
- guess z apply(rule fashoda_unit_path[of "interval_bij (a,b) (- 1,1) \<circ> f" "interval_bij (a,b) (- 1,1) \<circ> g"])
- unfolding path_def path_image_def pathstart_def pathfinish_def
- apply(rule_tac[1-2] continuous_on_compose) apply(rule assms[unfolded path_def] continuous_on_interval_bij)+
- unfolding subset_eq apply(rule_tac[1-2] ballI)
- proof- fix x assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
- then guess y unfolding image_iff .. note y=this
- show "x \<in> {- 1..1}" unfolding y o_def apply(rule in_interval_interval_bij)
- using y(1) using assms(3)[unfolded path_image_def subset_eq] int_nem by auto
- next fix x assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
- then guess y unfolding image_iff .. note y=this
- show "x \<in> {- 1..1}" unfolding y o_def apply(rule in_interval_interval_bij)
- using y(1) using assms(4)[unfolded path_image_def subset_eq] int_nem by auto
- next show "(interval_bij (a, b) (- 1, 1) \<circ> f) 0 $ 1 = -1"
- "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1"
- "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1"
- "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1" unfolding interval_bij_def Cart_lambda_beta vector_component_simps o_def split_conv
- unfolding assms[unfolded pathstart_def pathfinish_def] using as by auto qed note z=this
- from z(1) guess zf unfolding image_iff .. note zf=this
- from z(2) guess zg unfolding image_iff .. note zg=this
- have *:"\<forall>i. (- 1) $ i < (1::real^2) $ i \<and> a $ i < b $ i" unfolding forall_2 using as by auto
- show thesis apply(rule_tac z="interval_bij (- 1,1) (a,b) z" in that)
- apply(subst zf) defer apply(subst zg) unfolding o_def interval_bij_bij[OF *] path_image_def
- using zf(1) zg(1) by auto qed
-
-subsection {*Some slightly ad hoc lemmas I use below*}
-
-lemma segment_vertical: fixes a::"real^2" assumes "a$1 = b$1"
- shows "x \<in> closed_segment a b \<longleftrightarrow> (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))" (is "_ = ?R")
-proof-
- 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"
- { presume "?L \<Longrightarrow> ?R" "?R \<Longrightarrow> ?L" thus ?thesis unfolding closed_segment_def mem_Collect_eq
- unfolding Cart_eq forall_2 smult_conv_scaleR[THEN sym] vector_component_simps by blast }
- { assume ?L then guess u apply-apply(erule exE)apply(erule conjE)+ . note u=this
- { fix b a assume "b + u * a > a + u * b"
- hence "(1 - u) * b > (1 - u) * a" by(auto simp add:field_simps)
- hence "b \<ge> a" apply(drule_tac mult_less_imp_less_left) using u by auto
- hence "u * a \<le> u * b" apply-apply(rule mult_left_mono[OF _ u(3)])
- using u(3-4) by(auto simp add:field_simps) } note * = this
- { fix a b assume "u * b > u * a" hence "(1 - u) * a \<le> (1 - u) * b" apply-apply(rule mult_left_mono)
- apply(drule mult_less_imp_less_left) using u by auto
- hence "a + u * b \<le> b + u * a" by(auto simp add:field_simps) } note ** = this
- thus ?R unfolding u assms using u by(auto simp add:field_simps not_le intro:* **) }
- { assume ?R thus ?L proof(cases "x$2 = b$2")
- case True thus ?L apply(rule_tac x="(x$2 - a$2) / (b$2 - a$2)" in exI) unfolding assms True
- using `?R` by(auto simp add:field_simps)
- next case False thus ?L apply(rule_tac x="1 - (x$2 - b$2) / (a$2 - b$2)" in exI) unfolding assms using `?R`
- by(auto simp add:field_simps)
- qed } qed
-
-lemma segment_horizontal: fixes a::"real^2" assumes "a$2 = b$2"
- shows "x \<in> closed_segment a b \<longleftrightarrow> (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))" (is "_ = ?R")
-proof-
- 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"
- { presume "?L \<Longrightarrow> ?R" "?R \<Longrightarrow> ?L" thus ?thesis unfolding closed_segment_def mem_Collect_eq
- unfolding Cart_eq forall_2 smult_conv_scaleR[THEN sym] vector_component_simps by blast }
- { assume ?L then guess u apply-apply(erule exE)apply(erule conjE)+ . note u=this
- { fix b a assume "b + u * a > a + u * b"
- hence "(1 - u) * b > (1 - u) * a" by(auto simp add:field_simps)
- hence "b \<ge> a" apply(drule_tac mult_less_imp_less_left) using u by auto
- hence "u * a \<le> u * b" apply-apply(rule mult_left_mono[OF _ u(3)])
- using u(3-4) by(auto simp add:field_simps) } note * = this
- { fix a b assume "u * b > u * a" hence "(1 - u) * a \<le> (1 - u) * b" apply-apply(rule mult_left_mono)
- apply(drule mult_less_imp_less_left) using u by auto
- hence "a + u * b \<le> b + u * a" by(auto simp add:field_simps) } note ** = this
- thus ?R unfolding u assms using u by(auto simp add:field_simps not_le intro:* **) }
- { assume ?R thus ?L proof(cases "x$1 = b$1")
- case True thus ?L apply(rule_tac x="(x$1 - a$1) / (b$1 - a$1)" in exI) unfolding assms True
- using `?R` by(auto simp add:field_simps)
- next case False thus ?L apply(rule_tac x="1 - (x$1 - b$1) / (a$1 - b$1)" in exI) unfolding assms using `?R`
- by(auto simp add:field_simps)
- qed } qed
-
-subsection {*useful Fashoda corollary pointed out to me by Tom Hales. *}
-
-lemma fashoda_interlace: fixes a::"real^2"
- assumes "path f" "path g"
- "path_image f \<subseteq> {a..b}" "path_image g \<subseteq> {a..b}"
- "(pathstart f)$2 = a$2" "(pathfinish f)$2 = a$2"
- "(pathstart g)$2 = a$2" "(pathfinish g)$2 = a$2"
- "(pathstart f)$1 < (pathstart g)$1" "(pathstart g)$1 < (pathfinish f)$1"
- "(pathfinish f)$1 < (pathfinish g)$1"
- obtains z where "z \<in> path_image f" "z \<in> path_image g"
-proof-
- have "{a..b} \<noteq> {}" using path_image_nonempty using assms(3) by auto
- note ab=this[unfolded interval_eq_empty not_ex forall_2 not_less]
- have "pathstart f \<in> {a..b}" "pathfinish f \<in> {a..b}" "pathstart g \<in> {a..b}" "pathfinish g \<in> {a..b}"
- using pathstart_in_path_image pathfinish_in_path_image using assms(3-4) by auto
- note startfin = this[unfolded mem_interval forall_2]
- let ?P1 = "linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2]) +++
- linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f) +++ f +++
- linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2]) +++
- linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2])"
- let ?P2 = "linepath(vector[(pathstart g)$1, (pathstart g)$2 - 3])(pathstart g) +++ g +++
- linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1]) +++
- linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1]) +++
- linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3])"
- let ?a = "vector[a$1 - 2, a$2 - 3]"
- let ?b = "vector[b$1 + 2, b$2 + 3]"
- have P1P2:"path_image ?P1 = path_image (linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2])) \<union>
- path_image (linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f)) \<union> path_image f \<union>
- path_image (linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2])) \<union>
- path_image (linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2]))"
- "path_image ?P2 = path_image(linepath(vector[(pathstart g)$1, (pathstart g)$2 - 3])(pathstart g)) \<union> path_image g \<union>
- path_image(linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1])) \<union>
- path_image(linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1])) \<union>
- path_image(linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3]))" using assms(1-2)
- by(auto simp add: path_image_join path_linepath)
- have abab: "{a..b} \<subseteq> {?a..?b}" by(auto simp add:vector_le_def forall_2 vector_2)
- guess z apply(rule fashoda[of ?P1 ?P2 ?a ?b])
- unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2 proof-
- show "path ?P1" "path ?P2" using assms by auto
- have "path_image ?P1 \<subseteq> {?a .. ?b}" unfolding P1P2 path_image_linepath apply(rule Un_least)+ defer 3
- apply(rule_tac[1-4] convex_interval(1)[unfolded convex_contains_segment,rule_format])
- unfolding mem_interval forall_2 vector_2 using ab startfin abab assms(3)
- using assms(9-) unfolding assms by(auto simp add:field_simps)
- thus "path_image ?P1 \<subseteq> {?a .. ?b}" .
- have "path_image ?P2 \<subseteq> {?a .. ?b}" unfolding P1P2 path_image_linepath apply(rule Un_least)+ defer 2
- apply(rule_tac[1-4] convex_interval(1)[unfolded convex_contains_segment,rule_format])
- unfolding mem_interval forall_2 vector_2 using ab startfin abab assms(4)
- using assms(9-) unfolding assms by(auto simp add:field_simps)
- thus "path_image ?P2 \<subseteq> {?a .. ?b}" .
- 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"
- by(auto simp add: assms)
- qed note z=this[unfolded P1P2 path_image_linepath]
- show thesis apply(rule that[of z]) proof-
- have "(z \<in> closed_segment (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) \<or>
- z \<in> closed_segment (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f)) \<or>
- z \<in> closed_segment (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) \<or>
- z \<in> closed_segment (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]) \<Longrightarrow>
- (((z \<in> closed_segment (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g)) \<or>
- z \<in> closed_segment (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1])) \<or>
- z \<in> closed_segment (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1])) \<or>
- z \<in> closed_segment (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]) \<Longrightarrow> False"
- apply(simp only: segment_vertical segment_horizontal vector_2) proof- case goal1 note as=this
- have "pathfinish f \<in> {a..b}" using assms(3) pathfinish_in_path_image[of f] by auto
- hence "1 + b $ 1 \<le> pathfinish f $ 1 \<Longrightarrow> False" unfolding mem_interval forall_2 by auto
- hence "z$1 \<noteq> pathfinish f$1" using as(2) using assms ab by(auto simp add:field_simps)
- moreover have "pathstart f \<in> {a..b}" using assms(3) pathstart_in_path_image[of f] by auto
- hence "1 + b $ 1 \<le> pathstart f $ 1 \<Longrightarrow> False" unfolding mem_interval forall_2 by auto
- hence "z$1 \<noteq> pathstart f$1" using as(2) using assms ab by(auto simp add:field_simps)
- ultimately have *:"z$2 = a$2 - 2" using goal1(1) by auto
- have "z$1 \<noteq> pathfinish g$1" using as(2) using assms ab by(auto simp add:field_simps *)
- moreover have "pathstart g \<in> {a..b}" using assms(4) pathstart_in_path_image[of g] by auto
- note this[unfolded mem_interval forall_2]
- hence "z$1 \<noteq> pathstart g$1" using as(1) using assms ab by(auto simp add:field_simps *)
- 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"
- using as(2) unfolding * assms by(auto simp add:field_simps)
- thus False unfolding * using ab by auto
- qed hence "z \<in> path_image f \<or> z \<in> path_image g" using z unfolding Un_iff by blast
- hence z':"z\<in>{a..b}" using assms(3-4) by auto
- 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)"
- unfolding Cart_eq forall_2 assms by auto
- with z' show "z\<in>path_image f" using z(1) unfolding Un_iff mem_interval forall_2 apply-
- apply(simp only: segment_vertical segment_horizontal vector_2) unfolding assms by auto
- 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)"
- unfolding Cart_eq forall_2 assms by auto
- with z' show "z\<in>path_image g" using z(2) unfolding Un_iff mem_interval forall_2 apply-
- apply(simp only: segment_vertical segment_horizontal vector_2) unfolding assms by auto
- qed qed
-
-(** The Following still needs to be translated. Maybe I will do that later.
-
-(* ------------------------------------------------------------------------- *)
-(* Complement in dimension N >= 2 of set homeomorphic to any interval in *)
-(* any dimension is (path-)connected. This naively generalizes the argument *)
-(* in Ryuji Maehara's paper "The Jordan curve theorem via the Brouwer *)
-(* fixed point theorem", American Mathematical Monthly 1984. *)
-(* ------------------------------------------------------------------------- *)
-
-let RETRACTION_INJECTIVE_IMAGE_INTERVAL = prove
- (`!p:real^M->real^N a b.
- ~(interval[a,b] = {}) /\
- p continuous_on interval[a,b] /\
- (!x y. x IN interval[a,b] /\ y IN interval[a,b] /\ p x = p y ==> x = y)
- ==> ?f. f continuous_on (:real^N) /\
- IMAGE f (:real^N) SUBSET (IMAGE p (interval[a,b])) /\
- (!x. x IN (IMAGE p (interval[a,b])) ==> f x = x)`,
- REPEAT STRIP_TAC THEN
- FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INJECTIVE_ON_LEFT_INVERSE]) THEN
- DISCH_THEN(X_CHOOSE_TAC `q:real^N->real^M`) THEN
- SUBGOAL_THEN `(q:real^N->real^M) continuous_on
- (IMAGE p (interval[a:real^M,b]))`
- ASSUME_TAC THENL
- [MATCH_MP_TAC CONTINUOUS_ON_INVERSE THEN ASM_REWRITE_TAC[COMPACT_INTERVAL];
- ALL_TAC] THEN
- MP_TAC(ISPECL [`q:real^N->real^M`;
- `IMAGE (p:real^M->real^N)
- (interval[a,b])`;
- `a:real^M`; `b:real^M`]
- TIETZE_CLOSED_INTERVAL) THEN
- ASM_SIMP_TAC[COMPACT_INTERVAL; COMPACT_CONTINUOUS_IMAGE;
- COMPACT_IMP_CLOSED] THEN
- ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
- DISCH_THEN(X_CHOOSE_THEN `r:real^N->real^M` STRIP_ASSUME_TAC) THEN
- EXISTS_TAC `(p:real^M->real^N) o (r:real^N->real^M)` THEN
- REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; o_THM; IN_UNIV] THEN
- CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
- MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN ASM_REWRITE_TAC[] THEN
- FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP(REWRITE_RULE[IMP_CONJ]
- CONTINUOUS_ON_SUBSET)) THEN ASM SET_TAC[]);;
-
-let UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove
- (`!s:real^N->bool a b:real^M.
- s homeomorphic (interval[a,b])
- ==> !x. ~(x IN s) ==> ~bounded(path_component((:real^N) DIFF s) x)`,
- REPEAT GEN_TAC THEN REWRITE_TAC[homeomorphic; homeomorphism] THEN
- REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
- MAP_EVERY X_GEN_TAC [`p':real^N->real^M`; `p:real^M->real^N`] THEN
- DISCH_TAC THEN
- SUBGOAL_THEN
- `!x y. x IN interval[a,b] /\ y IN interval[a,b] /\
- (p:real^M->real^N) x = p y ==> x = y`
- ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
- FIRST_X_ASSUM(MP_TAC o funpow 4 CONJUNCT2) THEN
- DISCH_THEN(CONJUNCTS_THEN2 (SUBST1_TAC o SYM) ASSUME_TAC) THEN
- ASM_CASES_TAC `interval[a:real^M,b] = {}` THEN
- ASM_REWRITE_TAC[IMAGE_CLAUSES; DIFF_EMPTY; PATH_COMPONENT_UNIV;
- NOT_BOUNDED_UNIV] THEN
- ABBREV_TAC `s = (:real^N) DIFF (IMAGE p (interval[a:real^M,b]))` THEN
- X_GEN_TAC `c:real^N` THEN REPEAT STRIP_TAC THEN
- SUBGOAL_THEN `(c:real^N) IN s` ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
- SUBGOAL_THEN `bounded((path_component s c) UNION
- (IMAGE (p:real^M->real^N) (interval[a,b])))`
- MP_TAC THENL
- [ASM_SIMP_TAC[BOUNDED_UNION; COMPACT_IMP_BOUNDED; COMPACT_IMP_BOUNDED;
- COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
- ALL_TAC] THEN
- DISCH_THEN(MP_TAC o SPEC `c:real^N` o MATCH_MP BOUNDED_SUBSET_BALL) THEN
- REWRITE_TAC[UNION_SUBSET] THEN
- DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
- MP_TAC(ISPECL [`p:real^M->real^N`; `a:real^M`; `b:real^M`]
- RETRACTION_INJECTIVE_IMAGE_INTERVAL) THEN
- ASM_REWRITE_TAC[SUBSET; IN_UNIV] THEN
- DISCH_THEN(X_CHOOSE_THEN `r:real^N->real^N` MP_TAC) THEN
- DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
- (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
- REWRITE_TAC[FORALL_IN_IMAGE; IN_UNIV] THEN DISCH_TAC THEN
- ABBREV_TAC `q = \z:real^N. if z IN path_component s c then r(z) else z` THEN
- SUBGOAL_THEN
- `(q:real^N->real^N) continuous_on
- (closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)))`
- MP_TAC THENL
- [EXPAND_TAC "q" THEN MATCH_MP_TAC CONTINUOUS_ON_CASES THEN
- REWRITE_TAC[CLOSED_CLOSURE; CONTINUOUS_ON_ID; GSYM OPEN_CLOSED] THEN
- REPEAT CONJ_TAC THENL
- [MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN
- ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED;
- COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
- ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV];
- ALL_TAC] THEN
- X_GEN_TAC `z:real^N` THEN
- REWRITE_TAC[SET_RULE `~(z IN (s DIFF t) /\ z IN t)`] THEN
- STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
- MP_TAC(ISPECL
- [`path_component s (z:real^N)`; `path_component s (c:real^N)`]
- OPEN_INTER_CLOSURE_EQ_EMPTY) THEN
- ASM_REWRITE_TAC[GSYM DISJOINT; PATH_COMPONENT_DISJOINT] THEN ANTS_TAC THENL
- [MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN
- ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED;
- COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
- REWRITE_TAC[DISJOINT; EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
- DISCH_THEN(MP_TAC o SPEC `z:real^N`) THEN ASM_REWRITE_TAC[] THEN
- GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [IN] THEN
- REWRITE_TAC[PATH_COMPONENT_REFL_EQ] THEN ASM SET_TAC[]];
- ALL_TAC] THEN
- SUBGOAL_THEN
- `closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)) =
- (:real^N)`
- SUBST1_TAC THENL
- [MATCH_MP_TAC(SET_RULE `s SUBSET t ==> t UNION (UNIV DIFF s) = UNIV`) THEN
- REWRITE_TAC[CLOSURE_SUBSET];
- DISCH_TAC] THEN
- MP_TAC(ISPECL
- [`(\x. &2 % c - x) o
- (\x. c + B / norm(x - c) % (x - c)) o (q:real^N->real^N)`;
- `cball(c:real^N,B)`]
- BROUWER) THEN
- REWRITE_TAC[NOT_IMP; GSYM CONJ_ASSOC; COMPACT_CBALL; CONVEX_CBALL] THEN
- ASM_SIMP_TAC[CBALL_EQ_EMPTY; REAL_LT_IMP_LE; REAL_NOT_LT] THEN
- SUBGOAL_THEN `!x. ~((q:real^N->real^N) x = c)` ASSUME_TAC THENL
- [X_GEN_TAC `x:real^N` THEN EXPAND_TAC "q" THEN
- REWRITE_TAC[NORM_EQ_0; VECTOR_SUB_EQ] THEN COND_CASES_TAC THEN
- ASM SET_TAC[PATH_COMPONENT_REFL_EQ];
- ALL_TAC] THEN
- REPEAT CONJ_TAC THENL
- [MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
- SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN
- MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN CONJ_TAC THENL
- [ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV]; ALL_TAC] THEN
- MATCH_MP_TAC CONTINUOUS_ON_ADD THEN REWRITE_TAC[CONTINUOUS_ON_CONST] THEN
- MATCH_MP_TAC CONTINUOUS_ON_MUL THEN
- SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN
- REWRITE_TAC[o_DEF; real_div; LIFT_CMUL] THEN
- MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN
- MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_ON_INV) THEN
- ASM_REWRITE_TAC[FORALL_IN_IMAGE; NORM_EQ_0; VECTOR_SUB_EQ] THEN
- SUBGOAL_THEN
- `(\x:real^N. lift(norm(x - c))) = (lift o norm) o (\x. x - c)`
- SUBST1_TAC THENL [REWRITE_TAC[o_DEF]; ALL_TAC] THEN
- MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
- ASM_SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST;
- CONTINUOUS_ON_LIFT_NORM];
- REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_CBALL; o_THM; dist] THEN
- X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
- REWRITE_TAC[VECTOR_ARITH `c - (&2 % c - (c + x)) = x`] THEN
- REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN
- ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN
- ASM_REAL_ARITH_TAC;
- REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(c /\ b) <=> c ==> ~b`] THEN
- REWRITE_TAC[IN_CBALL; o_THM; dist] THEN
- X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
- REWRITE_TAC[VECTOR_ARITH `&2 % c - (c + x') = x <=> --x' = x - c`] THEN
- ASM_CASES_TAC `(x:real^N) IN path_component s c` THENL
- [MATCH_MP_TAC(NORM_ARITH `norm(y) < B /\ norm(x) = B ==> ~(--x = y)`) THEN
- REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN
- ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN
- ASM_SIMP_TAC[REAL_ARITH `&0 < B ==> abs B = B`] THEN
- UNDISCH_TAC `path_component s c SUBSET ball(c:real^N,B)` THEN
- REWRITE_TAC[SUBSET; IN_BALL] THEN ASM_MESON_TAC[dist; NORM_SUB];
- EXPAND_TAC "q" THEN REWRITE_TAC[] THEN ASM_REWRITE_TAC[] THEN
- REWRITE_TAC[VECTOR_ARITH `--(c % x) = x <=> (&1 + c) % x = vec 0`] THEN
- ASM_REWRITE_TAC[DE_MORGAN_THM; VECTOR_SUB_EQ; VECTOR_MUL_EQ_0] THEN
- SUBGOAL_THEN `~(x:real^N = c)` ASSUME_TAC THENL
- [ASM_MESON_TAC[PATH_COMPONENT_REFL; IN]; ALL_TAC] THEN
- ASM_REWRITE_TAC[] THEN
- MATCH_MP_TAC(REAL_ARITH `&0 < x ==> ~(&1 + x = &0)`) THEN
- ASM_SIMP_TAC[REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ]]]);;
-
-let PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove
- (`!s:real^N->bool a b:real^M.
- 2 <= dimindex(:N) /\ s homeomorphic interval[a,b]
- ==> path_connected((:real^N) DIFF s)`,
- REPEAT STRIP_TAC THEN REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN
- FIRST_ASSUM(MP_TAC o MATCH_MP
- UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN
- ASM_REWRITE_TAC[SET_RULE `~(x IN s) <=> x IN (UNIV DIFF s)`] THEN
- ABBREV_TAC `t = (:real^N) DIFF s` THEN
- DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN
- STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP HOMEOMORPHIC_COMPACTNESS) THEN
- REWRITE_TAC[COMPACT_INTERVAL] THEN
- DISCH_THEN(MP_TAC o MATCH_MP COMPACT_IMP_BOUNDED) THEN
- REWRITE_TAC[BOUNDED_POS; LEFT_IMP_EXISTS_THM] THEN
- X_GEN_TAC `B:real` THEN STRIP_TAC THEN
- SUBGOAL_THEN `(?u:real^N. u IN path_component t x /\ B < norm(u)) /\
- (?v:real^N. v IN path_component t y /\ B < norm(v))`
- STRIP_ASSUME_TAC THENL
- [ASM_MESON_TAC[BOUNDED_POS; REAL_NOT_LE]; ALL_TAC] THEN
- MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `u:real^N` THEN
- CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN
- MATCH_MP_TAC PATH_COMPONENT_SYM THEN
- MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `v:real^N` THEN
- CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN
- MATCH_MP_TAC PATH_COMPONENT_OF_SUBSET THEN
- EXISTS_TAC `(:real^N) DIFF cball(vec 0,B)` THEN CONJ_TAC THENL
- [EXPAND_TAC "t" THEN MATCH_MP_TAC(SET_RULE
- `s SUBSET t ==> (u DIFF t) SUBSET (u DIFF s)`) THEN
- ASM_REWRITE_TAC[SUBSET; IN_CBALL_0];
- MP_TAC(ISPEC `cball(vec 0:real^N,B)`
- PATH_CONNECTED_COMPLEMENT_BOUNDED_CONVEX) THEN
- ASM_REWRITE_TAC[BOUNDED_CBALL; CONVEX_CBALL] THEN
- REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN
- DISCH_THEN MATCH_MP_TAC THEN
- ASM_REWRITE_TAC[IN_DIFF; IN_UNIV; IN_CBALL_0; REAL_NOT_LE]]);;
-
-(* ------------------------------------------------------------------------- *)
-(* In particular, apply all these to the special case of an arc. *)
-(* ------------------------------------------------------------------------- *)
-
-let RETRACTION_ARC = prove
- (`!p. arc p
- ==> ?f. f continuous_on (:real^N) /\
- IMAGE f (:real^N) SUBSET path_image p /\
- (!x. x IN path_image p ==> f x = x)`,
- REWRITE_TAC[arc; path; path_image] THEN REPEAT STRIP_TAC THEN
- MATCH_MP_TAC RETRACTION_INJECTIVE_IMAGE_INTERVAL THEN
- ASM_REWRITE_TAC[INTERVAL_EQ_EMPTY_1; DROP_VEC; REAL_NOT_LT; REAL_POS]);;
-
-let PATH_CONNECTED_ARC_COMPLEMENT = prove
- (`!p. 2 <= dimindex(:N) /\ arc p
- ==> path_connected((:real^N) DIFF path_image p)`,
- REWRITE_TAC[arc; path] THEN REPEAT STRIP_TAC THEN SIMP_TAC[path_image] THEN
- MP_TAC(ISPECL [`path_image p:real^N->bool`; `vec 0:real^1`; `vec 1:real^1`]
- PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN
- ASM_REWRITE_TAC[path_image] THEN DISCH_THEN MATCH_MP_TAC THEN
- ONCE_REWRITE_TAC[HOMEOMORPHIC_SYM] THEN
- MATCH_MP_TAC HOMEOMORPHIC_COMPACT THEN
- EXISTS_TAC `p:real^1->real^N` THEN ASM_REWRITE_TAC[COMPACT_INTERVAL]);;
-
-let CONNECTED_ARC_COMPLEMENT = prove
- (`!p. 2 <= dimindex(:N) /\ arc p
- ==> connected((:real^N) DIFF path_image p)`,
- SIMP_TAC[PATH_CONNECTED_ARC_COMPLEMENT; PATH_CONNECTED_IMP_CONNECTED]);; *)
-
end
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Apr 27 16:24:57 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Apr 27 11:17:50 2010 -0700
@@ -15,17 +15,11 @@
declare vector_add_ldistrib[simp] vector_ssub_ldistrib[simp] vector_smult_assoc[simp] vector_smult_rneg[simp]
declare vector_sadd_rdistrib[simp] vector_sub_rdistrib[simp]
-declare UNIV_1[simp]
(*lemma dim1in[intro]:"Suc 0 \<in> {1::nat .. CARD(1)}" by auto*)
lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component vector_le_def Cart_lambda_beta basis_component vector_uminus_component
-lemma dest_vec1_simps[simp]: fixes a::"real^1"
- shows "a$1 = 0 \<longleftrightarrow> a = 0" (*"a \<le> 1 \<longleftrightarrow> dest_vec1 a \<le> 1" "0 \<le> a \<longleftrightarrow> 0 \<le> dest_vec1 a"*)
- "a \<le> b \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 b" "dest_vec1 (1::real^1) = 1"
- by(auto simp add: vector_le_def Cart_eq)
-
lemma norm_not_0:"(x::real^'n)\<noteq>0 \<Longrightarrow> norm x \<noteq> 0" by auto
lemma setsum_delta_notmem: assumes "x\<notin>s"
@@ -47,31 +41,10 @@
lemma if_smult:"(if P then x else (y::real)) *\<^sub>R v = (if P then x *\<^sub>R v else y *\<^sub>R v)" by auto
-lemma mem_interval_1: fixes x :: "real^1" shows
- "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
- "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
-by(simp_all add: Cart_eq vector_less_def vector_le_def)
-
lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::real^'n)) ` {a..b} =
(if {a..b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a..m *\<^sub>R b} else {m *\<^sub>R b..m *\<^sub>R a})"
using image_affinity_interval[of m 0 a b] by auto
-lemma dest_vec1_inverval:
- "dest_vec1 ` {a .. b} = {dest_vec1 a .. dest_vec1 b}"
- "dest_vec1 ` {a<.. b} = {dest_vec1 a<.. dest_vec1 b}"
- "dest_vec1 ` {a ..<b} = {dest_vec1 a ..<dest_vec1 b}"
- "dest_vec1 ` {a<..<b} = {dest_vec1 a<..<dest_vec1 b}"
- apply(rule_tac [!] equalityI)
- unfolding subset_eq Ball_def Bex_def mem_interval_1 image_iff
- apply(rule_tac [!] allI)apply(rule_tac [!] impI)
- apply(rule_tac[2] x="vec1 x" in exI)apply(rule_tac[4] x="vec1 x" in exI)
- apply(rule_tac[6] x="vec1 x" in exI)apply(rule_tac[8] x="vec1 x" in exI)
- by (auto simp add: vector_less_def vector_le_def)
-
-lemma dest_vec1_setsum: assumes "finite S"
- shows " dest_vec1 (setsum f S) = setsum (\<lambda>x. dest_vec1 (f x)) S"
- using dest_vec1_sum[OF assms] by auto
-
lemma dist_triangle_eq:
fixes x y z :: "real ^ _"
shows "dist x z = dist x y + dist y z \<longleftrightarrow> norm (x - y) *\<^sub>R (y - z) = norm (y - z) *\<^sub>R (x - y)"
@@ -359,9 +332,6 @@
shows "((1 - u) *\<^sub>R a + u *\<^sub>R b) \<in> s"
using assms unfolding convex_alt by auto
-lemma convex_vec1:"convex (vec1 ` s) = convex (s::real set)"
- unfolding convex_def Ball_def forall_vec1 unfolding vec1_dest_vec1_simps image_iff by auto
-
lemma convex_empty[intro]: "convex {}"
unfolding convex_def by simp
@@ -1292,29 +1262,14 @@
qed
qed
-lemma open_dest_vec1_vimage: "open S \<Longrightarrow> open (dest_vec1 -` S)"
-unfolding open_vector_def forall_1 by auto
-
-lemma tendsto_dest_vec1 [tendsto_intros]:
- "(f ---> l) net \<Longrightarrow> ((\<lambda>x. dest_vec1 (f x)) ---> dest_vec1 l) net"
-by(rule tendsto_Cart_nth)
-
-lemma continuous_dest_vec1: "continuous net f \<Longrightarrow> continuous net (\<lambda>x. dest_vec1 (f x))"
- unfolding continuous_def by (rule tendsto_dest_vec1)
-
(* TODO: move *)
lemma compact_real_interval:
fixes a b :: real shows "compact {a..b}"
-proof -
- have "continuous_on {vec1 a .. vec1 b} dest_vec1"
- unfolding continuous_on
- by (simp add: tendsto_dest_vec1 Lim_at_within Lim_ident_at)
- moreover have "compact {vec1 a .. vec1 b}" by (rule compact_interval)
- ultimately have "compact (dest_vec1 ` {vec1 a .. vec1 b})"
- by (rule compact_continuous_image)
- also have "dest_vec1 ` {vec1 a .. vec1 b} = {a..b}"
- by (auto simp add: image_def Bex_def exists_vec1)
- finally show ?thesis .
+proof (rule bounded_closed_imp_compact)
+ have "\<forall>y\<in>{a..b}. dist a y \<le> dist a b"
+ unfolding dist_real_def by auto
+ thus "bounded {a..b}" unfolding bounded_def by fast
+ show "closed {a..b}" by (rule closed_real_atLeastAtMost)
qed
lemma compact_convex_combinations:
@@ -2015,13 +1970,11 @@
proof-
obtain b where b:"b>0" "\<forall>x\<in>s. norm x \<le> b" using compact_imp_bounded[OF assms(1), unfolded bounded_pos] by auto
let ?A = "{y. \<exists>u. 0 \<le> u \<and> u \<le> b / norm(x) \<and> (y = u *\<^sub>R x)}"
- have A:"?A = (\<lambda>u. dest_vec1 u *\<^sub>R x) ` {0 .. vec1 (b / norm x)}"
- unfolding image_image[of "\<lambda>u. u *\<^sub>R x" "\<lambda>x. dest_vec1 x", THEN sym]
- unfolding dest_vec1_inverval vec1_dest_vec1 by auto
+ have A:"?A = (\<lambda>u. u *\<^sub>R x) ` {0 .. b / norm x}"
+ by auto
have "compact ?A" unfolding A apply(rule compact_continuous_image, rule continuous_at_imp_continuous_on)
apply(rule, rule continuous_vmul)
- apply (rule continuous_dest_vec1)
- apply(rule continuous_at_id) by(rule compact_interval)
+ apply(rule continuous_at_id) by(rule compact_real_interval)
moreover have "{y. \<exists>u\<ge>0. u \<le> b / norm x \<and> y = u *\<^sub>R x} \<inter> s \<noteq> {}" apply(rule not_disjointI[OF _ assms(2)])
unfolding mem_Collect_eq using `b>0` assms(3) by(auto intro!: divide_nonneg_pos)
ultimately obtain u y where obt: "u\<ge>0" "u \<le> b / norm x" "y = u *\<^sub>R x"
@@ -2232,10 +2185,6 @@
lemma mem_epigraph: "(x, y) \<in> epigraph s f \<longleftrightarrow> x \<in> s \<and> f x \<le> y" unfolding epigraph_def by auto
-(** move this**)
-lemma forall_dest_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P(dest_vec1 x))"
- apply safe defer apply(erule_tac x="vec1 x" in allE) by auto
-
(** This might break sooner or later. In fact it did already once. **)
lemma convex_epigraph:
"convex(epigraph s f) \<longleftrightarrow> convex_on s f \<and> convex s"
@@ -2264,16 +2213,11 @@
"(\<forall>p. P (fstcart p) (sndcart p)) \<longleftrightarrow> (\<forall>x y. P x y)" apply meson
apply(erule_tac x="pastecart x y" in allE) unfolding o_def by auto
-lemma forall_of_dest_vec1: "(\<forall>v. P (\<lambda>x. dest_vec1 (v x))) \<longleftrightarrow> (\<forall>x. P x)"
- apply rule apply rule apply(erule_tac x="(vec1 \<circ> x)" in allE) unfolding o_def vec1_dest_vec1 by auto
-
-lemma forall_of_dest_vec1': "(\<forall>v. P (dest_vec1 v)) \<longleftrightarrow> (\<forall>x. P x)"
- apply rule apply rule apply(erule_tac x="(vec1 x)" in allE) defer apply rule
- apply(erule_tac x="dest_vec1 v" in allE) unfolding o_def vec1_dest_vec1 by auto
-
+(* TODO: move *)
lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
by (cases "finite A", induct set: finite, simp_all)
+(* TODO: move *)
lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
by (cases "finite A", induct set: finite, simp_all)
@@ -2322,6 +2266,7 @@
lemma convex_interval: "convex {a .. b}" "convex {a<..<b::real^'n}"
apply(rule_tac[!] is_interval_convex) using is_interval_interval by auto
+(* FIXME: rewrite these lemmas without using vec1
subsection {* On @{text "real^1"}, @{text "is_interval"}, @{text "convex"} and @{text "connected"} are all equivalent. *}
lemma is_interval_1:
@@ -2350,33 +2295,33 @@
lemma convex_connected_1:
"connected s \<longleftrightarrow> convex (s::(real^1) set)"
by(metis is_interval_convex convex_connected is_interval_connected_1)
-
+*)
subsection {* Another intermediate value theorem formulation. *}
-lemma ivt_increasing_component_on_1: fixes f::"real^1 \<Rightarrow> real^'n"
- assumes "dest_vec1 a \<le> dest_vec1 b" "continuous_on {a .. b} f" "(f a)$k \<le> y" "y \<le> (f b)$k"
+lemma ivt_increasing_component_on_1: fixes f::"real \<Rightarrow> real^'n"
+ assumes "a \<le> b" "continuous_on {a .. b} f" "(f a)$k \<le> y" "y \<le> (f b)$k"
shows "\<exists>x\<in>{a..b}. (f x)$k = y"
proof- have "f a \<in> f ` {a..b}" "f b \<in> f ` {a..b}" apply(rule_tac[!] imageI)
using assms(1) by(auto simp add: vector_le_def)
thus ?thesis using connected_ivt_component[of "f ` {a..b}" "f a" "f b" k y]
- using connected_continuous_image[OF assms(2) convex_connected[OF convex_interval(1)]]
+ using connected_continuous_image[OF assms(2) convex_connected[OF convex_real_interval(5)]]
using assms by(auto intro!: imageI) qed
-lemma ivt_increasing_component_1: fixes f::"real^1 \<Rightarrow> real^'n"
- shows "dest_vec1 a \<le> dest_vec1 b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
+lemma ivt_increasing_component_1: fixes f::"real \<Rightarrow> real^'n"
+ shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
\<Longrightarrow> f a$k \<le> y \<Longrightarrow> y \<le> f b$k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)$k = y"
by(rule ivt_increasing_component_on_1)
(auto simp add: continuous_at_imp_continuous_on)
-lemma ivt_decreasing_component_on_1: fixes f::"real^1 \<Rightarrow> real^'n"
- assumes "dest_vec1 a \<le> dest_vec1 b" "continuous_on {a .. b} f" "(f b)$k \<le> y" "y \<le> (f a)$k"
+lemma ivt_decreasing_component_on_1: fixes f::"real \<Rightarrow> real^'n"
+ assumes "a \<le> b" "continuous_on {a .. b} f" "(f b)$k \<le> y" "y \<le> (f a)$k"
shows "\<exists>x\<in>{a..b}. (f x)$k = y"
apply(subst neg_equal_iff_equal[THEN sym]) unfolding vector_uminus_component[THEN sym]
apply(rule ivt_increasing_component_on_1) using assms using continuous_on_neg
by auto
-lemma ivt_decreasing_component_1: fixes f::"real^1 \<Rightarrow> real^'n"
- shows "dest_vec1 a \<le> dest_vec1 b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
+lemma ivt_decreasing_component_1: fixes f::"real \<Rightarrow> real^'n"
+ shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
\<Longrightarrow> f b$k \<le> y \<Longrightarrow> y \<le> f a$k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)$k = y"
by(rule ivt_decreasing_component_on_1)
(auto simp: continuous_at_imp_continuous_on)
@@ -2872,41 +2817,38 @@
subsection {* Paths. *}
-text {* TODO: Once @{const continuous_on} is generalized to arbitrary
-topological spaces, all of these concepts should be similarly generalized. *}
-
definition
- path :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> bool"
+ path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
where "path g \<longleftrightarrow> continuous_on {0 .. 1} g"
definition
- pathstart :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a"
+ pathstart :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a"
where "pathstart g = g 0"
definition
- pathfinish :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a"
+ pathfinish :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a"
where "pathfinish g = g 1"
definition
- path_image :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a set"
+ path_image :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a set"
where "path_image g = g ` {0 .. 1}"
definition
- reversepath :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> (real \<Rightarrow> 'a)"
+ reversepath :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> (real \<Rightarrow> 'a)"
where "reversepath g = (\<lambda>x. g(1 - x))"
definition
- joinpaths :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a)"
+ joinpaths :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a)"
(infixr "+++" 75)
where "g1 +++ g2 = (\<lambda>x. if x \<le> 1/2 then g1 (2 * x) else g2 (2 * x - 1))"
definition
- simple_path :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> bool"
+ simple_path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
where "simple_path g \<longleftrightarrow>
(\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. g x = g y \<longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0)"
definition
- injective_path :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> bool"
+ injective_path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
where "injective_path g \<longleftrightarrow> (\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. g x = g y \<longrightarrow> x = y)"
subsection {* Some lemmas about these concepts. *}
@@ -3037,7 +2979,7 @@
lemma simple_path_reversepath: assumes "simple_path g" shows "simple_path (reversepath g)"
using assms unfolding simple_path_def reversepath_def apply- apply(rule ballI)+
apply(erule_tac x="1-x" in ballE, erule_tac x="1-y" in ballE)
- unfolding mem_interval_1 by auto
+ by auto
lemma simple_path_join_loop:
assumes "injective_path g1" "injective_path g2" "pathfinish g2 = pathstart g1"
@@ -3050,36 +2992,36 @@
assume as:"x \<le> 1 / 2" "y \<le> 1 / 2"
hence "g1 (2 *\<^sub>R x) = g1 (2 *\<^sub>R y)" using xy(3) unfolding joinpaths_def by auto
moreover have "2 *\<^sub>R x \<in> {0..1}" "2 *\<^sub>R y \<in> {0..1}" using xy(1,2) as
- unfolding mem_interval_1 by auto
+ by auto
ultimately show ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] by auto
next assume as:"x > 1 / 2" "y > 1 / 2"
hence "g2 (2 *\<^sub>R x - 1) = g2 (2 *\<^sub>R y - 1)" using xy(3) unfolding joinpaths_def by auto
- moreover have "2 *\<^sub>R x - 1 \<in> {0..1}" "2 *\<^sub>R y - 1 \<in> {0..1}" using xy(1,2) as unfolding mem_interval_1 by auto
+ moreover have "2 *\<^sub>R x - 1 \<in> {0..1}" "2 *\<^sub>R y - 1 \<in> {0..1}" using xy(1,2) as by auto
ultimately show ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] by auto
next assume as:"x \<le> 1 / 2" "y > 1 / 2"
hence "?g x \<in> path_image g1" "?g y \<in> path_image g2" unfolding path_image_def joinpaths_def
- using xy(1,2)[unfolded mem_interval_1] by auto
+ using xy(1,2) by auto
moreover have "?g y \<noteq> pathstart g2" using as(2) unfolding pathstart_def joinpaths_def
- using inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(2)[unfolded mem_interval_1]
+ using inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(2)
by (auto simp add: field_simps)
ultimately have *:"?g x = pathstart g1" using assms(4) unfolding xy(3) by auto
- hence "x = 0" unfolding pathstart_def joinpaths_def using as(1) and xy(1)[unfolded mem_interval_1]
+ hence "x = 0" unfolding pathstart_def joinpaths_def using as(1) and xy(1)
using inj(1)[of "2 *\<^sub>R x" 0] by auto
moreover have "y = 1" using * unfolding xy(3) assms(3)[THEN sym]
- unfolding joinpaths_def pathfinish_def using as(2) and xy(2)[unfolded mem_interval_1]
+ unfolding joinpaths_def pathfinish_def using as(2) and xy(2)
using inj(2)[of "2 *\<^sub>R y - 1" 1] by auto
ultimately show ?thesis by auto
next assume as:"x > 1 / 2" "y \<le> 1 / 2"
hence "?g x \<in> path_image g2" "?g y \<in> path_image g1" unfolding path_image_def joinpaths_def
- using xy(1,2)[unfolded mem_interval_1] by auto
+ using xy(1,2) by auto
moreover have "?g x \<noteq> pathstart g2" using as(1) unfolding pathstart_def joinpaths_def
- using inj(2)[of "2 *\<^sub>R x - 1" 0] and xy(1)[unfolded mem_interval_1]
+ using inj(2)[of "2 *\<^sub>R x - 1" 0] and xy(1)
by (auto simp add: field_simps)
ultimately have *:"?g y = pathstart g1" using assms(4) unfolding xy(3) by auto
- hence "y = 0" unfolding pathstart_def joinpaths_def using as(2) and xy(2)[unfolded mem_interval_1]
+ hence "y = 0" unfolding pathstart_def joinpaths_def using as(2) and xy(2)
using inj(1)[of "2 *\<^sub>R y" 0] by auto
moreover have "x = 1" using * unfolding xy(3)[THEN sym] assms(3)[THEN sym]
- unfolding joinpaths_def pathfinish_def using as(1) and xy(1)[unfolded mem_interval_1]
+ unfolding joinpaths_def pathfinish_def using as(1) and xy(1)
using inj(2)[of "2 *\<^sub>R x - 1" 1] by auto
ultimately show ?thesis by auto qed qed
@@ -3092,29 +3034,29 @@
fix x y assume xy:"x \<in> {0..1}" "y \<in> {0..1}" "(g1 +++ g2) x = (g1 +++ g2) y"
show "x = y" proof(cases "x \<le> 1/2", case_tac[!] "y \<le> 1/2", unfold not_le)
assume "x \<le> 1 / 2" "y \<le> 1 / 2" thus ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] and xy
- unfolding mem_interval_1 joinpaths_def by auto
+ unfolding joinpaths_def by auto
next assume "x > 1 / 2" "y > 1 / 2" thus ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] and xy
- unfolding mem_interval_1 joinpaths_def by auto
+ unfolding joinpaths_def by auto
next assume as:"x \<le> 1 / 2" "y > 1 / 2"
hence "?g x \<in> path_image g1" "?g y \<in> path_image g2" unfolding path_image_def joinpaths_def
- using xy(1,2)[unfolded mem_interval_1] by auto
+ using xy(1,2) by auto
hence "?g x = pathfinish g1" "?g y = pathstart g2" using assms(4) unfolding assms(3) xy(3) by auto
thus ?thesis using as and inj(1)[of "2 *\<^sub>R x" 1] inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(1,2)
- unfolding pathstart_def pathfinish_def joinpaths_def mem_interval_1
+ unfolding pathstart_def pathfinish_def joinpaths_def
by auto
next assume as:"x > 1 / 2" "y \<le> 1 / 2"
hence "?g x \<in> path_image g2" "?g y \<in> path_image g1" unfolding path_image_def joinpaths_def
- using xy(1,2)[unfolded mem_interval_1] by auto
+ using xy(1,2) by auto
hence "?g x = pathstart g2" "?g y = pathfinish g1" using assms(4) unfolding assms(3) xy(3) by auto
thus ?thesis using as and inj(2)[of "2 *\<^sub>R x - 1" 0] inj(1)[of "2 *\<^sub>R y" 1] and xy(1,2)
- unfolding pathstart_def pathfinish_def joinpaths_def mem_interval_1
+ unfolding pathstart_def pathfinish_def joinpaths_def
by auto qed qed
lemmas join_paths_simps = path_join path_image_join pathstart_join pathfinish_join
subsection {* Reparametrizing a closed curve to start at some chosen point. *}
-definition "shiftpath a (f::real \<Rightarrow> 'a::metric_space) =
+definition "shiftpath a (f::real \<Rightarrow> 'a::topological_space) =
(\<lambda>x. if (a + x) \<le> 1 then f(a + x) else f(a + x - 1))"
lemma pathstart_shiftpath: "a \<le> 1 \<Longrightarrow> pathstart(shiftpath a g) = g a"
@@ -3178,8 +3120,7 @@
unfolding pathfinish_def linepath_def by auto
lemma continuous_linepath_at[intro]: "continuous (at x) (linepath a b)"
- unfolding linepath_def
- by (intro continuous_intros continuous_dest_vec1)
+ unfolding linepath_def by (intro continuous_intros)
lemma continuous_on_linepath[intro]: "continuous_on s (linepath a b)"
using continuous_linepath_at by(auto intro!: continuous_at_imp_continuous_on)
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Apr 27 16:24:57 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Apr 27 11:17:50 2010 -0700
@@ -6,16 +6,13 @@
header {* Multivariate calculus in Euclidean space. *}
theory Derivative
-imports Brouwer_Fixpoint RealVector
+imports Brouwer_Fixpoint Vec1 RealVector
begin
(* Because I do not want to type this all the time *)
lemmas linear_linear = linear_conv_bounded_linear[THEN sym]
-(** move this **)
-declare norm_vec1[simp]
-
subsection {* Derivatives *}
text {* The definition is slightly tricky since we make it work over
@@ -94,16 +91,6 @@
subsection {* Derivatives on real = Derivatives on @{typ "real^1"} *}
-lemma dist_vec1_0[simp]: "dist(vec1 (x::real)) 0 = norm x" unfolding vector_dist_norm by auto
-
-lemma bounded_linear_vec1_dest_vec1: fixes f::"real \<Rightarrow> real"
- shows "linear (vec1 \<circ> f \<circ> dest_vec1) = bounded_linear f" (is "?l = ?r") proof-
- { assume ?l guess K using linear_bounded[OF `?l`] ..
- hence "\<exists>K. \<forall>x. \<bar>f x\<bar> \<le> \<bar>x\<bar> * K" apply(rule_tac x=K in exI)
- unfolding vec1_dest_vec1_simps by (auto simp add:field_simps) }
- thus ?thesis unfolding linear_def bounded_linear_def additive_def bounded_linear_axioms_def o_def
- unfolding vec1_dest_vec1_simps by auto qed
-
lemma has_derivative_within_vec1_dest_vec1: fixes f::"real\<Rightarrow>real" shows
"((vec1 \<circ> f \<circ> dest_vec1) has_derivative (vec1 \<circ> f' \<circ> dest_vec1)) (at (vec1 x) within vec1 ` s)
= (f has_derivative f') (at x within s)"
@@ -156,14 +143,14 @@
lemma has_derivative_const: "((\<lambda>x. c) has_derivative (\<lambda>h. 0)) net"
unfolding has_derivative_def apply(rule,rule bounded_linear_zero) by(simp add: Lim_const)
-lemma (in bounded_linear) cmul: shows "bounded_linear (\<lambda>x. (c::real) *\<^sub>R f x)" proof
- guess K using pos_bounded ..
- thus "\<exists>K. \<forall>x. norm ((c::real) *\<^sub>R f x) \<le> norm x * K" apply(rule_tac x="abs c * K" in exI) proof
- fix x case goal1
- hence "abs c * norm (f x) \<le> abs c * (norm x * K)" apply-apply(erule conjE,erule_tac x=x in allE)
- apply(rule mult_left_mono) by auto
- thus ?case by(auto simp add:field_simps)
- qed qed(auto simp add: scaleR.add_right add scaleR)
+lemma (in bounded_linear) cmul: shows "bounded_linear (\<lambda>x. (c::real) *\<^sub>R f x)"
+proof -
+ have "bounded_linear (\<lambda>x. c *\<^sub>R x)"
+ by (rule scaleR.bounded_linear_right)
+ moreover have "bounded_linear f" ..
+ ultimately show ?thesis
+ by (rule bounded_linear_compose)
+qed
lemma has_derivative_cmul: assumes "(f has_derivative f') net" shows "((\<lambda>x. c *\<^sub>R f(x)) has_derivative (\<lambda>h. c *\<^sub>R f'(h))) net"
unfolding has_derivative_def apply(rule,rule bounded_linear.cmul)
@@ -647,11 +634,6 @@
subsection {* The traditional Rolle theorem in one dimension. *}
-lemma vec1_le[simp]:fixes a::real shows "vec1 a \<le> vec1 b \<longleftrightarrow> a \<le> b"
- unfolding vector_le_def by auto
-lemma vec1_less[simp]:fixes a::real shows "vec1 a < vec1 b \<longleftrightarrow> a < b"
- unfolding vector_less_def by auto
-
lemma rolle: fixes f::"real\<Rightarrow>real"
assumes "a < b" "f a = f b" "continuous_on {a..b} f"
"\<forall>x\<in>{a<..<b}. (f has_derivative f'(x)) (at x)"
@@ -763,6 +745,9 @@
have 4:"{norm (f x) |x. norm x = 1} = (\<lambda>x. norm (f x)) ` {x. norm x=1}" by auto
show ?thesis unfolding onorm_def 1 2 3 4 by(simp add:Sup_finite_Max) qed
+lemma convex_vec1:"convex (vec1 ` s) = convex (s::real set)"
+ unfolding convex_def Ball_def forall_vec1 unfolding vec1_dest_vec1_simps image_iff by auto
+
lemma differentiable_bound_real: fixes f::"real \<Rightarrow> real"
assumes "convex s" "\<forall>x\<in>s. (f has_derivative f' x) (at x within s)" "\<forall>x\<in>s. onorm(f' x) \<le> B" and x:"x\<in>s" and y:"y\<in>s"
shows "norm(f x - f y) \<le> B * norm(x - y)"
--- a/src/HOL/Multivariate_Analysis/Determinants.thy Tue Apr 27 16:24:57 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy Tue Apr 27 11:17:50 2010 -0700
@@ -5,7 +5,7 @@
header {* Traces, Determinant of square matrices and some properties *}
theory Determinants
-imports Euclidean_Space Permutations
+imports Euclidean_Space Permutations Vec1
begin
subsection{* First some facts about products*}
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Apr 27 16:24:57 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Apr 27 11:17:50 2010 -0700
@@ -12,56 +12,6 @@
uses "positivstellensatz.ML" ("normarith.ML")
begin
-text{* Some common special cases.*}
-
-lemma forall_1[simp]: "(\<forall>i::1. P i) \<longleftrightarrow> P 1"
- by (metis num1_eq_iff)
-
-lemma ex_1[simp]: "(\<exists>x::1. P x) \<longleftrightarrow> P 1"
- by auto (metis num1_eq_iff)
-
-lemma exhaust_2:
- fixes x :: 2 shows "x = 1 \<or> x = 2"
-proof (induct x)
- case (of_int z)
- then have "0 <= z" and "z < 2" by simp_all
- then have "z = 0 | z = 1" by arith
- then show ?case by auto
-qed
-
-lemma forall_2: "(\<forall>i::2. P i) \<longleftrightarrow> P 1 \<and> P 2"
- by (metis exhaust_2)
-
-lemma exhaust_3:
- fixes x :: 3 shows "x = 1 \<or> x = 2 \<or> x = 3"
-proof (induct x)
- case (of_int z)
- then have "0 <= z" and "z < 3" by simp_all
- then have "z = 0 \<or> z = 1 \<or> z = 2" by arith
- then show ?case by auto
-qed
-
-lemma forall_3: "(\<forall>i::3. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3"
- by (metis exhaust_3)
-
-lemma UNIV_1: "UNIV = {1::1}"
- by (auto simp add: num1_eq_iff)
-
-lemma UNIV_2: "UNIV = {1::2, 2::2}"
- using exhaust_2 by auto
-
-lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}"
- using exhaust_3 by auto
-
-lemma setsum_1: "setsum f (UNIV::1 set) = f 1"
- unfolding UNIV_1 by simp
-
-lemma setsum_2: "setsum f (UNIV::2 set) = f 1 + f 2"
- unfolding UNIV_2 by simp
-
-lemma setsum_3: "setsum f (UNIV::3 set) = f 1 + f 2 + f 3"
- unfolding UNIV_3 by (simp add: add_ac)
-
subsection{* Basic componentwise operations on vectors. *}
instantiation cart :: (plus,finite) plus
@@ -114,7 +64,7 @@
instance by (intro_classes)
end
-text{* The ordering on @{typ "real^1"} is linear. *}
+text{* The ordering on one-dimensional vectors is linear. *}
class cart_one = assumes UNIV_one: "card (UNIV \<Colon> 'a set) = Suc 0"
begin
@@ -123,11 +73,6 @@
by (auto intro!: card_ge_0_finite) qed
end
-instantiation num1 :: cart_one begin
-instance proof
- show "CARD(1) = Suc 0" by auto
-qed end
-
instantiation cart :: (linorder,cart_one) linorder begin
instance proof
guess a B using UNIV_one[where 'a='b] unfolding card_Suc_eq apply- by(erule exE)+
@@ -654,39 +599,6 @@
end
-lemma setsum_squares_eq_0_iff: assumes fS: "finite F" and fp: "\<forall>x \<in> F. f x \<ge> (0 ::'a::ordered_ab_group_add)" shows "setsum f F = 0 \<longleftrightarrow> (ALL x:F. f x = 0)"
-using fS fp setsum_nonneg[OF fp]
-proof (induct set: finite)
- case empty thus ?case by simp
-next
- case (insert x F)
- from insert.prems have Fx: "f x \<ge> 0" and Fp: "\<forall> a \<in> F. f a \<ge> 0" by simp_all
- from insert.hyps Fp setsum_nonneg[OF Fp]
- have h: "setsum f F = 0 \<longleftrightarrow> (\<forall>a \<in>F. f a = 0)" by metis
- from add_nonneg_eq_0_iff[OF Fx setsum_nonneg[OF Fp]] insert.hyps(1,2)
- show ?case by (simp add: h)
-qed
-
-subsection{* The collapse of the general concepts to dimension one. *}
-
-lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
- by (simp add: Cart_eq)
-
-lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))"
- apply auto
- apply (erule_tac x= "x$1" in allE)
- apply (simp only: vector_one[symmetric])
- done
-
-lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)"
- by (simp add: norm_vector_def UNIV_1)
-
-lemma norm_real: "norm(x::real ^ 1) = abs(x$1)"
- by (simp add: norm_vector_1)
-
-lemma dist_real: "dist(x::real ^ 1) y = abs((x$1) - (y$1))"
- by (auto simp add: norm_real dist_norm)
-
subsection {* A connectedness or intermediate value lemma with several applications. *}
lemma connected_real_lemma:
@@ -747,7 +659,7 @@
ultimately show ?thesis using alb by metis
qed
-text{* One immediately useful corollary is the existence of square roots! --- Should help to get rid of all the development of square-root for reals as a special case @{typ "real^1"} *}
+text{* One immediately useful corollary is the existence of square roots! --- Should help to get rid of all the development of square-root for reals as a special case *}
lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)"
proof-
@@ -1364,67 +1276,6 @@
lemma orthogonal_commute: "orthogonal (x::real ^'n)y \<longleftrightarrow> orthogonal y x"
by (simp add: orthogonal_def inner_commute)
-subsection{* Explicit vector construction from lists. *}
-
-primrec from_nat :: "nat \<Rightarrow> 'a::{monoid_add,one}"
-where "from_nat 0 = 0" | "from_nat (Suc n) = 1 + from_nat n"
-
-lemma from_nat [simp]: "from_nat = of_nat"
-by (rule ext, induct_tac x, simp_all)
-
-primrec
- list_fun :: "nat \<Rightarrow> _ list \<Rightarrow> _ \<Rightarrow> _"
-where
- "list_fun n [] = (\<lambda>x. 0)"
-| "list_fun n (x # xs) = fun_upd (list_fun (Suc n) xs) (from_nat n) x"
-
-definition "vector l = (\<chi> i. list_fun 1 l i)"
-(*definition "vector l = (\<chi> i. if i <= length l then l ! (i - 1) else 0)"*)
-
-lemma vector_1: "(vector[x]) $1 = x"
- unfolding vector_def by simp
-
-lemma vector_2:
- "(vector[x,y]) $1 = x"
- "(vector[x,y] :: 'a^2)$2 = (y::'a::zero)"
- unfolding vector_def by simp_all
-
-lemma vector_3:
- "(vector [x,y,z] ::('a::zero)^3)$1 = x"
- "(vector [x,y,z] ::('a::zero)^3)$2 = y"
- "(vector [x,y,z] ::('a::zero)^3)$3 = z"
- unfolding vector_def by simp_all
-
-lemma forall_vector_1: "(\<forall>v::'a::zero^1. P v) \<longleftrightarrow> (\<forall>x. P(vector[x]))"
- apply auto
- apply (erule_tac x="v$1" in allE)
- apply (subgoal_tac "vector [v$1] = v")
- apply simp
- apply (vector vector_def)
- apply simp
- done
-
-lemma forall_vector_2: "(\<forall>v::'a::zero^2. P v) \<longleftrightarrow> (\<forall>x y. P(vector[x, y]))"
- apply auto
- apply (erule_tac x="v$1" in allE)
- apply (erule_tac x="v$2" in allE)
- apply (subgoal_tac "vector [v$1, v$2] = v")
- apply simp
- apply (vector vector_def)
- apply (simp add: forall_2)
- done
-
-lemma forall_vector_3: "(\<forall>v::'a::zero^3. P v) \<longleftrightarrow> (\<forall>x y z. P(vector[x, y, z]))"
- apply auto
- apply (erule_tac x="v$1" in allE)
- apply (erule_tac x="v$2" in allE)
- apply (erule_tac x="v$3" in allE)
- apply (subgoal_tac "vector [v$1, v$2, v$3] = v")
- apply simp
- apply (vector vector_def)
- apply (simp add: forall_3)
- done
-
subsection{* Linear functions. *}
definition "linear f \<longleftrightarrow> (\<forall>x y. f(x + y) = f x + f y) \<and> (\<forall>c x. f(c *s x) = c *s f x)"
@@ -2216,33 +2067,6 @@
apply (rule onorm_triangle)
by assumption+
-(* "lift" from 'a to 'a^1 and "drop" from 'a^1 to 'a -- FIXME: potential use of transfer *)
-
-abbreviation vec1:: "'a \<Rightarrow> 'a ^ 1" where "vec1 x \<equiv> vec x"
-
-abbreviation dest_vec1:: "'a ^1 \<Rightarrow> 'a"
- where "dest_vec1 x \<equiv> (x$1)"
-
-lemma vec1_component[simp]: "(vec1 x)$1 = x"
- by simp
-
-lemma vec1_dest_vec1: "vec1(dest_vec1 x) = x" "dest_vec1(vec1 y) = y"
- by (simp_all add: Cart_eq)
-
-declare vec1_dest_vec1(1) [simp]
-
-lemma forall_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (vec1 x))"
- by (metis vec1_dest_vec1(1))
-
-lemma exists_vec1: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P(vec1 x))"
- by (metis vec1_dest_vec1(1))
-
-lemma vec1_eq[simp]: "vec1 x = vec1 y \<longleftrightarrow> x = y"
- by (metis vec1_dest_vec1(2))
-
-lemma dest_vec1_eq[simp]: "dest_vec1 x = dest_vec1 y \<longleftrightarrow> x = y"
- by (metis vec1_dest_vec1(1))
-
lemma vec_in_image_vec: "vec x \<in> (vec ` S) \<longleftrightarrow> x \<in> S" by auto
lemma vec_add: "vec(x + y) = vec x + vec y" by (vector vec_def)
@@ -2250,9 +2074,6 @@
lemma vec_cmul: "vec(c* x) = c *s vec x " by (vector vec_def)
lemma vec_neg: "vec(- x) = - vec x " by (vector vec_def)
-lemma range_vec1[simp]:"range vec1 = UNIV" apply(rule set_ext,rule) unfolding image_iff defer
- apply(rule_tac x="dest_vec1 x" in bexI) by auto
-
lemma vec_setsum: assumes fS: "finite S"
shows "vec(setsum f S) = setsum (vec o f) S"
apply (induct rule: finite_induct[OF fS])
@@ -2260,70 +2081,6 @@
apply (auto simp add: vec_add)
done
-lemma dest_vec1_lambda: "dest_vec1(\<chi> i. x i) = x 1"
- by (simp)
-
-lemma dest_vec1_vec: "dest_vec1(vec x) = x"
- by (simp)
-
-lemma dest_vec1_sum: assumes fS: "finite S"
- shows "dest_vec1(setsum f S) = setsum (dest_vec1 o f) S"
- apply (induct rule: finite_induct[OF fS])
- apply simp
- apply auto
- done
-
-lemma norm_vec1: "norm(vec1 x) = abs(x)"
- by (simp add: vec_def norm_real)
-
-lemma dist_vec1: "dist(vec1 x) (vec1 y) = abs(x - y)"
- by (simp only: dist_real vec1_component)
-lemma abs_dest_vec1: "norm x = \<bar>dest_vec1 x\<bar>"
- by (metis vec1_dest_vec1(1) norm_vec1)
-
-lemmas vec1_dest_vec1_simps = forall_vec1 vec_add[THEN sym] dist_vec1 vec_sub[THEN sym] vec1_dest_vec1 norm_vec1 vector_smult_component
- vec1_eq vec_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def norm_vec1 real_norm_def
-
-lemma bounded_linear_vec1:"bounded_linear (vec1::real\<Rightarrow>real^1)"
- unfolding bounded_linear_def additive_def bounded_linear_axioms_def
- unfolding smult_conv_scaleR[THEN sym] unfolding vec1_dest_vec1_simps
- apply(rule conjI) defer apply(rule conjI) defer apply(rule_tac x=1 in exI) by auto
-
-lemma linear_vmul_dest_vec1:
- fixes f:: "'a::semiring_1^_ \<Rightarrow> 'a^1"
- shows "linear f \<Longrightarrow> linear (\<lambda>x. dest_vec1(f x) *s v)"
- apply (rule linear_vmul_component)
- by auto
-
-lemma linear_from_scalars:
- assumes lf: "linear (f::'a::comm_ring_1 ^1 \<Rightarrow> 'a^_)"
- shows "f = (\<lambda>x. dest_vec1 x *s column 1 (matrix f))"
- apply (rule ext)
- apply (subst matrix_works[OF lf, symmetric])
- apply (auto simp add: Cart_eq matrix_vector_mult_def column_def mult_commute UNIV_1)
- done
-
-lemma linear_to_scalars: assumes lf: "linear (f::real ^'n \<Rightarrow> real^1)"
- shows "f = (\<lambda>x. vec1(row 1 (matrix f) \<bullet> x))"
- apply (rule ext)
- apply (subst matrix_works[OF lf, symmetric])
- apply (simp add: Cart_eq matrix_vector_mult_def row_def inner_vector_def mult_commute)
- done
-
-lemma dest_vec1_eq_0: "dest_vec1 x = 0 \<longleftrightarrow> x = 0"
- by (simp add: dest_vec1_eq[symmetric])
-
-lemma setsum_scalars: assumes fS: "finite S"
- shows "setsum f S = vec1 (setsum (dest_vec1 o f) S)"
- unfolding vec_setsum[OF fS] by simp
-
-lemma dest_vec1_wlog_le: "(\<And>(x::'a::linorder ^ 1) y. P x y \<longleftrightarrow> P y x) \<Longrightarrow> (\<And>x y. dest_vec1 x <= dest_vec1 y ==> P x y) \<Longrightarrow> P x y"
- apply (cases "dest_vec1 x \<le> dest_vec1 y")
- apply simp
- apply (subgoal_tac "dest_vec1 y \<le> dest_vec1 x")
- apply (auto)
- done
-
text{* Pasting vectors. *}
lemma linear_fstcart[intro]: "linear fstcart"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Tue Apr 27 11:17:50 2010 -0700
@@ -0,0 +1,556 @@
+(* Author: John Harrison
+ Translation from HOL light: Robert Himmelmann, TU Muenchen *)
+
+header {* Fashoda meet theorem. *}
+
+theory Fashoda
+imports Brouwer_Fixpoint Vec1
+begin
+
+subsection {*Fashoda meet theorem. *}
+
+lemma infnorm_2: "infnorm (x::real^2) = max (abs(x$1)) (abs(x$2))"
+ unfolding infnorm_def UNIV_2 apply(rule Sup_eq) by auto
+
+lemma infnorm_eq_1_2: "infnorm (x::real^2) = 1 \<longleftrightarrow>
+ (abs(x$1) \<le> 1 \<and> abs(x$2) \<le> 1 \<and> (x$1 = -1 \<or> x$1 = 1 \<or> x$2 = -1 \<or> x$2 = 1))"
+ unfolding infnorm_2 by auto
+
+lemma infnorm_eq_1_imp: assumes "infnorm (x::real^2) = 1" shows "abs(x$1) \<le> 1" "abs(x$2) \<le> 1"
+ using assms unfolding infnorm_eq_1_2 by auto
+
+lemma fashoda_unit: fixes f g::"real \<Rightarrow> real^2"
+ assumes "f ` {- 1..1} \<subseteq> {- 1..1}" "g ` {- 1..1} \<subseteq> {- 1..1}"
+ "continuous_on {- 1..1} f" "continuous_on {- 1..1} g"
+ "f (- 1)$1 = - 1" "f 1$1 = 1" "g (- 1) $2 = -1" "g 1 $2 = 1"
+ shows "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. f s = g t" proof(rule ccontr)
+ case goal1 note as = this[unfolded bex_simps,rule_format]
+ def sqprojection \<equiv> "\<lambda>z::real^2. (inverse (infnorm z)) *\<^sub>R z"
+ def negatex \<equiv> "\<lambda>x::real^2. (vector [-(x$1), x$2])::real^2"
+ have lem1:"\<forall>z::real^2. infnorm(negatex z) = infnorm z"
+ unfolding negatex_def infnorm_2 vector_2 by auto
+ have lem2:"\<forall>z. z\<noteq>0 \<longrightarrow> infnorm(sqprojection z) = 1" unfolding sqprojection_def
+ unfolding infnorm_mul[unfolded smult_conv_scaleR] unfolding abs_inverse real_abs_infnorm
+ unfolding infnorm_eq_0[THEN sym] by auto
+ let ?F = "(\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w)"
+ have *:"\<And>i. (\<lambda>x::real^2. x $ i) ` {- 1..1} = {- 1..1::real}"
+ apply(rule set_ext) unfolding image_iff Bex_def mem_interval apply rule defer
+ apply(rule_tac x="vec x" in exI) by auto
+ { fix x assume "x \<in> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w) ` {- 1..1::real^2}"
+ then guess w unfolding image_iff .. note w = this
+ hence "x \<noteq> 0" using as[of "w$1" "w$2"] unfolding mem_interval by auto} note x0=this
+ have 21:"\<And>i::2. i\<noteq>1 \<Longrightarrow> i=2" using UNIV_2 by auto
+ have 1:"{- 1<..<1::real^2} \<noteq> {}" unfolding interval_eq_empty by auto
+ have 2:"continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)" apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+
+ prefer 2 apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+ unfolding *
+ apply(rule assms)+ apply(rule continuous_on_compose,subst sqprojection_def)
+ apply(rule continuous_on_mul ) apply(rule continuous_at_imp_continuous_on,rule) apply(rule continuous_at_inv[unfolded o_def])
+ apply(rule continuous_at_infnorm) unfolding infnorm_eq_0 defer apply(rule continuous_on_id) apply(rule linear_continuous_on) proof-
+ 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
+ show "negatex (x + y) $ i = (negatex x + negatex y) $ i" "negatex (c *s x) $ i = (c *s negatex x) $ i"
+ apply-apply(case_tac[!] "i\<noteq>1") prefer 3 apply(drule_tac[1-2] 21)
+ unfolding negatex_def by(auto simp add:vector_2 ) qed qed(insert x0, auto)
+ have 3:"(negatex \<circ> sqprojection \<circ> ?F) ` {- 1..1} \<subseteq> {- 1..1}" unfolding subset_eq apply rule proof-
+ case goal1 then guess y unfolding image_iff .. note y=this have "?F y \<noteq> 0" apply(rule x0) using y(1) by auto
+ hence *:"infnorm (sqprojection (?F y)) = 1" unfolding y o_def apply- by(rule lem2[rule_format])
+ have "infnorm x = 1" unfolding *[THEN sym] y o_def by(rule lem1[rule_format])
+ thus "x\<in>{- 1..1}" unfolding mem_interval infnorm_2 apply- apply rule
+ proof-case goal1 thus ?case apply(cases "i=1") defer apply(drule 21) by auto qed qed
+ guess x apply(rule brouwer_weak[of "{- 1..1::real^2}" "negatex \<circ> sqprojection \<circ> ?F"])
+ apply(rule compact_interval convex_interval)+ unfolding interior_closed_interval
+ apply(rule 1 2 3)+ . note x=this
+ have "?F x \<noteq> 0" apply(rule x0) using x(1) by auto
+ hence *:"infnorm (sqprojection (?F x)) = 1" unfolding o_def by(rule lem2[rule_format])
+ have nx:"infnorm x = 1" apply(subst x(2)[THEN sym]) unfolding *[THEN sym] o_def by(rule lem1[rule_format])
+ have "\<forall>x i. x \<noteq> 0 \<longrightarrow> (0 < (sqprojection x)$i \<longleftrightarrow> 0 < x$i)" "\<forall>x i. x \<noteq> 0 \<longrightarrow> ((sqprojection x)$i < 0 \<longleftrightarrow> x$i < 0)"
+ apply- apply(rule_tac[!] allI impI)+ proof- fix x::"real^2" and i::2 assume x:"x\<noteq>0"
+ have "inverse (infnorm x) > 0" using x[unfolded infnorm_pos_lt[THEN sym]] by auto
+ thus "(0 < sqprojection x $ i) = (0 < x $ i)" "(sqprojection x $ i < 0) = (x $ i < 0)"
+ unfolding sqprojection_def vector_component_simps Cart_nth.scaleR real_scaleR_def
+ unfolding zero_less_mult_iff mult_less_0_iff by(auto simp add:field_simps) qed
+ note lem3 = this[rule_format]
+ have x1:"x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}" using x(1) unfolding mem_interval by auto
+ hence nz:"f (x $ 1) - g (x $ 2) \<noteq> 0" unfolding right_minus_eq apply-apply(rule as) by auto
+ have "x $ 1 = -1 \<or> x $ 1 = 1 \<or> x $ 2 = -1 \<or> x $ 2 = 1" using nx unfolding infnorm_eq_1_2 by auto
+ thus False proof- fix P Q R S
+ presume "P \<or> Q \<or> R \<or> S" "P\<Longrightarrow>False" "Q\<Longrightarrow>False" "R\<Longrightarrow>False" "S\<Longrightarrow>False" thus False by auto
+ next assume as:"x$1 = 1"
+ hence *:"f (x $ 1) $ 1 = 1" using assms(6) by auto
+ have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0"
+ using x(2)[unfolded o_def Cart_eq,THEN spec[where x=1]]
+ unfolding as negatex_def vector_2 by auto moreover
+ from x1 have "g (x $ 2) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto
+ ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval
+ apply(erule_tac x=1 in allE) by auto
+ next assume as:"x$1 = -1"
+ hence *:"f (x $ 1) $ 1 = - 1" using assms(5) by auto
+ have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0"
+ using x(2)[unfolded o_def Cart_eq,THEN spec[where x=1]]
+ unfolding as negatex_def vector_2 by auto moreover
+ from x1 have "g (x $ 2) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto
+ ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval
+ apply(erule_tac x=1 in allE) by auto
+ next assume as:"x$2 = 1"
+ hence *:"g (x $ 2) $ 2 = 1" using assms(8) by auto
+ have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0"
+ using x(2)[unfolded o_def Cart_eq,THEN spec[where x=2]]
+ unfolding as negatex_def vector_2 by auto moreover
+ from x1 have "f (x $ 1) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto
+ ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval
+ apply(erule_tac x=2 in allE) by auto
+ next assume as:"x$2 = -1"
+ hence *:"g (x $ 2) $ 2 = - 1" using assms(7) by auto
+ have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0"
+ using x(2)[unfolded o_def Cart_eq,THEN spec[where x=2]]
+ unfolding as negatex_def vector_2 by auto moreover
+ from x1 have "f (x $ 1) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto
+ ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval
+ apply(erule_tac x=2 in allE) by auto qed(auto) qed
+
+lemma fashoda_unit_path: fixes f ::"real \<Rightarrow> real^2" and g ::"real \<Rightarrow> real^2"
+ assumes "path f" "path g" "path_image f \<subseteq> {- 1..1}" "path_image g \<subseteq> {- 1..1}"
+ "(pathstart f)$1 = -1" "(pathfinish f)$1 = 1" "(pathstart g)$2 = -1" "(pathfinish g)$2 = 1"
+ obtains z where "z \<in> path_image f" "z \<in> path_image g" proof-
+ note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
+ def iscale \<equiv> "\<lambda>z::real. inverse 2 *\<^sub>R (z + 1)"
+ have isc:"iscale ` {- 1..1} \<subseteq> {0..1}" unfolding iscale_def by(auto)
+ have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t" proof(rule fashoda_unit)
+ show "(f \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}" "(g \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}"
+ using isc and assms(3-4) unfolding image_compose by auto
+ have *:"continuous_on {- 1..1} iscale" unfolding iscale_def by(rule continuous_on_intros)+
+ show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)"
+ apply-apply(rule_tac[!] continuous_on_compose[OF *]) apply(rule_tac[!] continuous_on_subset[OF _ isc])
+ by(rule assms)+ have *:"(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1" unfolding Cart_eq by auto
+ 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"
+ unfolding o_def iscale_def using assms by(auto simp add:*) qed
+ then guess s .. from this(2) guess t .. note st=this
+ show thesis apply(rule_tac z="f (iscale s)" in that)
+ using st `s\<in>{- 1..1}` unfolding o_def path_image_def image_iff apply-
+ apply(rule_tac x="iscale s" in bexI) prefer 3 apply(rule_tac x="iscale t" in bexI)
+ using isc[unfolded subset_eq, rule_format] by auto qed
+
+lemma fashoda: fixes b::"real^2"
+ assumes "path f" "path g" "path_image f \<subseteq> {a..b}" "path_image g \<subseteq> {a..b}"
+ "(pathstart f)$1 = a$1" "(pathfinish f)$1 = b$1"
+ "(pathstart g)$2 = a$2" "(pathfinish g)$2 = b$2"
+ obtains z where "z \<in> path_image f" "z \<in> path_image g" proof-
+ fix P Q S presume "P \<or> Q \<or> S" "P \<Longrightarrow> thesis" "Q \<Longrightarrow> thesis" "S \<Longrightarrow> thesis" thus thesis by auto
+next have "{a..b} \<noteq> {}" using assms(3) using path_image_nonempty by auto
+ hence "a \<le> b" unfolding interval_eq_empty vector_le_def by(auto simp add: not_less)
+ 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
+next assume as:"a$1 = b$1" have "\<exists>z\<in>path_image g. z$2 = (pathstart f)$2" apply(rule connected_ivt_component)
+ apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image)
+ unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"]
+ unfolding pathstart_def by(auto simp add: vector_le_def) then guess z .. note z=this
+ have "z \<in> {a..b}" using z(1) assms(4) unfolding path_image_def by blast
+ hence "z = f 0" unfolding Cart_eq forall_2 unfolding z(2) pathstart_def
+ using assms(3)[unfolded path_image_def subset_eq mem_interval,rule_format,of "f 0" 1]
+ unfolding mem_interval apply(erule_tac x=1 in allE) using as by auto
+ thus thesis apply-apply(rule that[OF _ z(1)]) unfolding path_image_def by auto
+next assume as:"a$2 = b$2" have "\<exists>z\<in>path_image f. z$1 = (pathstart g)$1" apply(rule connected_ivt_component)
+ apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image)
+ unfolding assms using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"]
+ unfolding pathstart_def by(auto simp add: vector_le_def) then guess z .. note z=this
+ have "z \<in> {a..b}" using z(1) assms(3) unfolding path_image_def by blast
+ hence "z = g 0" unfolding Cart_eq forall_2 unfolding z(2) pathstart_def
+ using assms(4)[unfolded path_image_def subset_eq mem_interval,rule_format,of "g 0" 2]
+ unfolding mem_interval apply(erule_tac x=2 in allE) using as by auto
+ thus thesis apply-apply(rule that[OF z(1)]) unfolding path_image_def by auto
+next assume as:"a $ 1 < b $ 1 \<and> a $ 2 < b $ 2"
+ have int_nem:"{- 1..1::real^2} \<noteq> {}" unfolding interval_eq_empty by auto
+ guess z apply(rule fashoda_unit_path[of "interval_bij (a,b) (- 1,1) \<circ> f" "interval_bij (a,b) (- 1,1) \<circ> g"])
+ unfolding path_def path_image_def pathstart_def pathfinish_def
+ apply(rule_tac[1-2] continuous_on_compose) apply(rule assms[unfolded path_def] continuous_on_interval_bij)+
+ unfolding subset_eq apply(rule_tac[1-2] ballI)
+ proof- fix x assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
+ then guess y unfolding image_iff .. note y=this
+ show "x \<in> {- 1..1}" unfolding y o_def apply(rule in_interval_interval_bij)
+ using y(1) using assms(3)[unfolded path_image_def subset_eq] int_nem by auto
+ next fix x assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
+ then guess y unfolding image_iff .. note y=this
+ show "x \<in> {- 1..1}" unfolding y o_def apply(rule in_interval_interval_bij)
+ using y(1) using assms(4)[unfolded path_image_def subset_eq] int_nem by auto
+ next show "(interval_bij (a, b) (- 1, 1) \<circ> f) 0 $ 1 = -1"
+ "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1"
+ "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1"
+ "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1" unfolding interval_bij_def Cart_lambda_beta vector_component_simps o_def split_conv
+ unfolding assms[unfolded pathstart_def pathfinish_def] using as by auto qed note z=this
+ from z(1) guess zf unfolding image_iff .. note zf=this
+ from z(2) guess zg unfolding image_iff .. note zg=this
+ have *:"\<forall>i. (- 1) $ i < (1::real^2) $ i \<and> a $ i < b $ i" unfolding forall_2 using as by auto
+ show thesis apply(rule_tac z="interval_bij (- 1,1) (a,b) z" in that)
+ apply(subst zf) defer apply(subst zg) unfolding o_def interval_bij_bij[OF *] path_image_def
+ using zf(1) zg(1) by auto qed
+
+subsection {*Some slightly ad hoc lemmas I use below*}
+
+lemma segment_vertical: fixes a::"real^2" assumes "a$1 = b$1"
+ shows "x \<in> closed_segment a b \<longleftrightarrow> (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))" (is "_ = ?R")
+proof-
+ 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"
+ { presume "?L \<Longrightarrow> ?R" "?R \<Longrightarrow> ?L" thus ?thesis unfolding closed_segment_def mem_Collect_eq
+ unfolding Cart_eq forall_2 smult_conv_scaleR[THEN sym] vector_component_simps by blast }
+ { assume ?L then guess u apply-apply(erule exE)apply(erule conjE)+ . note u=this
+ { fix b a assume "b + u * a > a + u * b"
+ hence "(1 - u) * b > (1 - u) * a" by(auto simp add:field_simps)
+ hence "b \<ge> a" apply(drule_tac mult_less_imp_less_left) using u by auto
+ hence "u * a \<le> u * b" apply-apply(rule mult_left_mono[OF _ u(3)])
+ using u(3-4) by(auto simp add:field_simps) } note * = this
+ { fix a b assume "u * b > u * a" hence "(1 - u) * a \<le> (1 - u) * b" apply-apply(rule mult_left_mono)
+ apply(drule mult_less_imp_less_left) using u by auto
+ hence "a + u * b \<le> b + u * a" by(auto simp add:field_simps) } note ** = this
+ thus ?R unfolding u assms using u by(auto simp add:field_simps not_le intro:* **) }
+ { assume ?R thus ?L proof(cases "x$2 = b$2")
+ case True thus ?L apply(rule_tac x="(x$2 - a$2) / (b$2 - a$2)" in exI) unfolding assms True
+ using `?R` by(auto simp add:field_simps)
+ next case False thus ?L apply(rule_tac x="1 - (x$2 - b$2) / (a$2 - b$2)" in exI) unfolding assms using `?R`
+ by(auto simp add:field_simps)
+ qed } qed
+
+lemma segment_horizontal: fixes a::"real^2" assumes "a$2 = b$2"
+ shows "x \<in> closed_segment a b \<longleftrightarrow> (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))" (is "_ = ?R")
+proof-
+ 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"
+ { presume "?L \<Longrightarrow> ?R" "?R \<Longrightarrow> ?L" thus ?thesis unfolding closed_segment_def mem_Collect_eq
+ unfolding Cart_eq forall_2 smult_conv_scaleR[THEN sym] vector_component_simps by blast }
+ { assume ?L then guess u apply-apply(erule exE)apply(erule conjE)+ . note u=this
+ { fix b a assume "b + u * a > a + u * b"
+ hence "(1 - u) * b > (1 - u) * a" by(auto simp add:field_simps)
+ hence "b \<ge> a" apply(drule_tac mult_less_imp_less_left) using u by auto
+ hence "u * a \<le> u * b" apply-apply(rule mult_left_mono[OF _ u(3)])
+ using u(3-4) by(auto simp add:field_simps) } note * = this
+ { fix a b assume "u * b > u * a" hence "(1 - u) * a \<le> (1 - u) * b" apply-apply(rule mult_left_mono)
+ apply(drule mult_less_imp_less_left) using u by auto
+ hence "a + u * b \<le> b + u * a" by(auto simp add:field_simps) } note ** = this
+ thus ?R unfolding u assms using u by(auto simp add:field_simps not_le intro:* **) }
+ { assume ?R thus ?L proof(cases "x$1 = b$1")
+ case True thus ?L apply(rule_tac x="(x$1 - a$1) / (b$1 - a$1)" in exI) unfolding assms True
+ using `?R` by(auto simp add:field_simps)
+ next case False thus ?L apply(rule_tac x="1 - (x$1 - b$1) / (a$1 - b$1)" in exI) unfolding assms using `?R`
+ by(auto simp add:field_simps)
+ qed } qed
+
+subsection {*useful Fashoda corollary pointed out to me by Tom Hales. *}
+
+lemma fashoda_interlace: fixes a::"real^2"
+ assumes "path f" "path g"
+ "path_image f \<subseteq> {a..b}" "path_image g \<subseteq> {a..b}"
+ "(pathstart f)$2 = a$2" "(pathfinish f)$2 = a$2"
+ "(pathstart g)$2 = a$2" "(pathfinish g)$2 = a$2"
+ "(pathstart f)$1 < (pathstart g)$1" "(pathstart g)$1 < (pathfinish f)$1"
+ "(pathfinish f)$1 < (pathfinish g)$1"
+ obtains z where "z \<in> path_image f" "z \<in> path_image g"
+proof-
+ have "{a..b} \<noteq> {}" using path_image_nonempty using assms(3) by auto
+ note ab=this[unfolded interval_eq_empty not_ex forall_2 not_less]
+ have "pathstart f \<in> {a..b}" "pathfinish f \<in> {a..b}" "pathstart g \<in> {a..b}" "pathfinish g \<in> {a..b}"
+ using pathstart_in_path_image pathfinish_in_path_image using assms(3-4) by auto
+ note startfin = this[unfolded mem_interval forall_2]
+ let ?P1 = "linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2]) +++
+ linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f) +++ f +++
+ linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2]) +++
+ linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2])"
+ let ?P2 = "linepath(vector[(pathstart g)$1, (pathstart g)$2 - 3])(pathstart g) +++ g +++
+ linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1]) +++
+ linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1]) +++
+ linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3])"
+ let ?a = "vector[a$1 - 2, a$2 - 3]"
+ let ?b = "vector[b$1 + 2, b$2 + 3]"
+ have P1P2:"path_image ?P1 = path_image (linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2])) \<union>
+ path_image (linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f)) \<union> path_image f \<union>
+ path_image (linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2])) \<union>
+ path_image (linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2]))"
+ "path_image ?P2 = path_image(linepath(vector[(pathstart g)$1, (pathstart g)$2 - 3])(pathstart g)) \<union> path_image g \<union>
+ path_image(linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1])) \<union>
+ path_image(linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1])) \<union>
+ path_image(linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3]))" using assms(1-2)
+ by(auto simp add: path_image_join path_linepath)
+ have abab: "{a..b} \<subseteq> {?a..?b}" by(auto simp add:vector_le_def forall_2 vector_2)
+ guess z apply(rule fashoda[of ?P1 ?P2 ?a ?b])
+ unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2 proof-
+ show "path ?P1" "path ?P2" using assms by auto
+ have "path_image ?P1 \<subseteq> {?a .. ?b}" unfolding P1P2 path_image_linepath apply(rule Un_least)+ defer 3
+ apply(rule_tac[1-4] convex_interval(1)[unfolded convex_contains_segment,rule_format])
+ unfolding mem_interval forall_2 vector_2 using ab startfin abab assms(3)
+ using assms(9-) unfolding assms by(auto simp add:field_simps)
+ thus "path_image ?P1 \<subseteq> {?a .. ?b}" .
+ have "path_image ?P2 \<subseteq> {?a .. ?b}" unfolding P1P2 path_image_linepath apply(rule Un_least)+ defer 2
+ apply(rule_tac[1-4] convex_interval(1)[unfolded convex_contains_segment,rule_format])
+ unfolding mem_interval forall_2 vector_2 using ab startfin abab assms(4)
+ using assms(9-) unfolding assms by(auto simp add:field_simps)
+ thus "path_image ?P2 \<subseteq> {?a .. ?b}" .
+ 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"
+ by(auto simp add: assms)
+ qed note z=this[unfolded P1P2 path_image_linepath]
+ show thesis apply(rule that[of z]) proof-
+ have "(z \<in> closed_segment (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) \<or>
+ z \<in> closed_segment (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f)) \<or>
+ z \<in> closed_segment (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) \<or>
+ z \<in> closed_segment (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]) \<Longrightarrow>
+ (((z \<in> closed_segment (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g)) \<or>
+ z \<in> closed_segment (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1])) \<or>
+ z \<in> closed_segment (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1])) \<or>
+ z \<in> closed_segment (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]) \<Longrightarrow> False"
+ apply(simp only: segment_vertical segment_horizontal vector_2) proof- case goal1 note as=this
+ have "pathfinish f \<in> {a..b}" using assms(3) pathfinish_in_path_image[of f] by auto
+ hence "1 + b $ 1 \<le> pathfinish f $ 1 \<Longrightarrow> False" unfolding mem_interval forall_2 by auto
+ hence "z$1 \<noteq> pathfinish f$1" using as(2) using assms ab by(auto simp add:field_simps)
+ moreover have "pathstart f \<in> {a..b}" using assms(3) pathstart_in_path_image[of f] by auto
+ hence "1 + b $ 1 \<le> pathstart f $ 1 \<Longrightarrow> False" unfolding mem_interval forall_2 by auto
+ hence "z$1 \<noteq> pathstart f$1" using as(2) using assms ab by(auto simp add:field_simps)
+ ultimately have *:"z$2 = a$2 - 2" using goal1(1) by auto
+ have "z$1 \<noteq> pathfinish g$1" using as(2) using assms ab by(auto simp add:field_simps *)
+ moreover have "pathstart g \<in> {a..b}" using assms(4) pathstart_in_path_image[of g] by auto
+ note this[unfolded mem_interval forall_2]
+ hence "z$1 \<noteq> pathstart g$1" using as(1) using assms ab by(auto simp add:field_simps *)
+ 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"
+ using as(2) unfolding * assms by(auto simp add:field_simps)
+ thus False unfolding * using ab by auto
+ qed hence "z \<in> path_image f \<or> z \<in> path_image g" using z unfolding Un_iff by blast
+ hence z':"z\<in>{a..b}" using assms(3-4) by auto
+ 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)"
+ unfolding Cart_eq forall_2 assms by auto
+ with z' show "z\<in>path_image f" using z(1) unfolding Un_iff mem_interval forall_2 apply-
+ apply(simp only: segment_vertical segment_horizontal vector_2) unfolding assms by auto
+ 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)"
+ unfolding Cart_eq forall_2 assms by auto
+ with z' show "z\<in>path_image g" using z(2) unfolding Un_iff mem_interval forall_2 apply-
+ apply(simp only: segment_vertical segment_horizontal vector_2) unfolding assms by auto
+ qed qed
+
+(** The Following still needs to be translated. Maybe I will do that later.
+
+(* ------------------------------------------------------------------------- *)
+(* Complement in dimension N >= 2 of set homeomorphic to any interval in *)
+(* any dimension is (path-)connected. This naively generalizes the argument *)
+(* in Ryuji Maehara's paper "The Jordan curve theorem via the Brouwer *)
+(* fixed point theorem", American Mathematical Monthly 1984. *)
+(* ------------------------------------------------------------------------- *)
+
+let RETRACTION_INJECTIVE_IMAGE_INTERVAL = prove
+ (`!p:real^M->real^N a b.
+ ~(interval[a,b] = {}) /\
+ p continuous_on interval[a,b] /\
+ (!x y. x IN interval[a,b] /\ y IN interval[a,b] /\ p x = p y ==> x = y)
+ ==> ?f. f continuous_on (:real^N) /\
+ IMAGE f (:real^N) SUBSET (IMAGE p (interval[a,b])) /\
+ (!x. x IN (IMAGE p (interval[a,b])) ==> f x = x)`,
+ REPEAT STRIP_TAC THEN
+ FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INJECTIVE_ON_LEFT_INVERSE]) THEN
+ DISCH_THEN(X_CHOOSE_TAC `q:real^N->real^M`) THEN
+ SUBGOAL_THEN `(q:real^N->real^M) continuous_on
+ (IMAGE p (interval[a:real^M,b]))`
+ ASSUME_TAC THENL
+ [MATCH_MP_TAC CONTINUOUS_ON_INVERSE THEN ASM_REWRITE_TAC[COMPACT_INTERVAL];
+ ALL_TAC] THEN
+ MP_TAC(ISPECL [`q:real^N->real^M`;
+ `IMAGE (p:real^M->real^N)
+ (interval[a,b])`;
+ `a:real^M`; `b:real^M`]
+ TIETZE_CLOSED_INTERVAL) THEN
+ ASM_SIMP_TAC[COMPACT_INTERVAL; COMPACT_CONTINUOUS_IMAGE;
+ COMPACT_IMP_CLOSED] THEN
+ ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
+ DISCH_THEN(X_CHOOSE_THEN `r:real^N->real^M` STRIP_ASSUME_TAC) THEN
+ EXISTS_TAC `(p:real^M->real^N) o (r:real^N->real^M)` THEN
+ REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; o_THM; IN_UNIV] THEN
+ CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
+ MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN ASM_REWRITE_TAC[] THEN
+ FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP(REWRITE_RULE[IMP_CONJ]
+ CONTINUOUS_ON_SUBSET)) THEN ASM SET_TAC[]);;
+
+let UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove
+ (`!s:real^N->bool a b:real^M.
+ s homeomorphic (interval[a,b])
+ ==> !x. ~(x IN s) ==> ~bounded(path_component((:real^N) DIFF s) x)`,
+ REPEAT GEN_TAC THEN REWRITE_TAC[homeomorphic; homeomorphism] THEN
+ REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
+ MAP_EVERY X_GEN_TAC [`p':real^N->real^M`; `p:real^M->real^N`] THEN
+ DISCH_TAC THEN
+ SUBGOAL_THEN
+ `!x y. x IN interval[a,b] /\ y IN interval[a,b] /\
+ (p:real^M->real^N) x = p y ==> x = y`
+ ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
+ FIRST_X_ASSUM(MP_TAC o funpow 4 CONJUNCT2) THEN
+ DISCH_THEN(CONJUNCTS_THEN2 (SUBST1_TAC o SYM) ASSUME_TAC) THEN
+ ASM_CASES_TAC `interval[a:real^M,b] = {}` THEN
+ ASM_REWRITE_TAC[IMAGE_CLAUSES; DIFF_EMPTY; PATH_COMPONENT_UNIV;
+ NOT_BOUNDED_UNIV] THEN
+ ABBREV_TAC `s = (:real^N) DIFF (IMAGE p (interval[a:real^M,b]))` THEN
+ X_GEN_TAC `c:real^N` THEN REPEAT STRIP_TAC THEN
+ SUBGOAL_THEN `(c:real^N) IN s` ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
+ SUBGOAL_THEN `bounded((path_component s c) UNION
+ (IMAGE (p:real^M->real^N) (interval[a,b])))`
+ MP_TAC THENL
+ [ASM_SIMP_TAC[BOUNDED_UNION; COMPACT_IMP_BOUNDED; COMPACT_IMP_BOUNDED;
+ COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
+ ALL_TAC] THEN
+ DISCH_THEN(MP_TAC o SPEC `c:real^N` o MATCH_MP BOUNDED_SUBSET_BALL) THEN
+ REWRITE_TAC[UNION_SUBSET] THEN
+ DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
+ MP_TAC(ISPECL [`p:real^M->real^N`; `a:real^M`; `b:real^M`]
+ RETRACTION_INJECTIVE_IMAGE_INTERVAL) THEN
+ ASM_REWRITE_TAC[SUBSET; IN_UNIV] THEN
+ DISCH_THEN(X_CHOOSE_THEN `r:real^N->real^N` MP_TAC) THEN
+ DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
+ (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
+ REWRITE_TAC[FORALL_IN_IMAGE; IN_UNIV] THEN DISCH_TAC THEN
+ ABBREV_TAC `q = \z:real^N. if z IN path_component s c then r(z) else z` THEN
+ SUBGOAL_THEN
+ `(q:real^N->real^N) continuous_on
+ (closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)))`
+ MP_TAC THENL
+ [EXPAND_TAC "q" THEN MATCH_MP_TAC CONTINUOUS_ON_CASES THEN
+ REWRITE_TAC[CLOSED_CLOSURE; CONTINUOUS_ON_ID; GSYM OPEN_CLOSED] THEN
+ REPEAT CONJ_TAC THENL
+ [MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN
+ ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED;
+ COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
+ ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV];
+ ALL_TAC] THEN
+ X_GEN_TAC `z:real^N` THEN
+ REWRITE_TAC[SET_RULE `~(z IN (s DIFF t) /\ z IN t)`] THEN
+ STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
+ MP_TAC(ISPECL
+ [`path_component s (z:real^N)`; `path_component s (c:real^N)`]
+ OPEN_INTER_CLOSURE_EQ_EMPTY) THEN
+ ASM_REWRITE_TAC[GSYM DISJOINT; PATH_COMPONENT_DISJOINT] THEN ANTS_TAC THENL
+ [MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN
+ ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED;
+ COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
+ REWRITE_TAC[DISJOINT; EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
+ DISCH_THEN(MP_TAC o SPEC `z:real^N`) THEN ASM_REWRITE_TAC[] THEN
+ GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [IN] THEN
+ REWRITE_TAC[PATH_COMPONENT_REFL_EQ] THEN ASM SET_TAC[]];
+ ALL_TAC] THEN
+ SUBGOAL_THEN
+ `closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)) =
+ (:real^N)`
+ SUBST1_TAC THENL
+ [MATCH_MP_TAC(SET_RULE `s SUBSET t ==> t UNION (UNIV DIFF s) = UNIV`) THEN
+ REWRITE_TAC[CLOSURE_SUBSET];
+ DISCH_TAC] THEN
+ MP_TAC(ISPECL
+ [`(\x. &2 % c - x) o
+ (\x. c + B / norm(x - c) % (x - c)) o (q:real^N->real^N)`;
+ `cball(c:real^N,B)`]
+ BROUWER) THEN
+ REWRITE_TAC[NOT_IMP; GSYM CONJ_ASSOC; COMPACT_CBALL; CONVEX_CBALL] THEN
+ ASM_SIMP_TAC[CBALL_EQ_EMPTY; REAL_LT_IMP_LE; REAL_NOT_LT] THEN
+ SUBGOAL_THEN `!x. ~((q:real^N->real^N) x = c)` ASSUME_TAC THENL
+ [X_GEN_TAC `x:real^N` THEN EXPAND_TAC "q" THEN
+ REWRITE_TAC[NORM_EQ_0; VECTOR_SUB_EQ] THEN COND_CASES_TAC THEN
+ ASM SET_TAC[PATH_COMPONENT_REFL_EQ];
+ ALL_TAC] THEN
+ REPEAT CONJ_TAC THENL
+ [MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
+ SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN
+ MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN CONJ_TAC THENL
+ [ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV]; ALL_TAC] THEN
+ MATCH_MP_TAC CONTINUOUS_ON_ADD THEN REWRITE_TAC[CONTINUOUS_ON_CONST] THEN
+ MATCH_MP_TAC CONTINUOUS_ON_MUL THEN
+ SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN
+ REWRITE_TAC[o_DEF; real_div; LIFT_CMUL] THEN
+ MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN
+ MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_ON_INV) THEN
+ ASM_REWRITE_TAC[FORALL_IN_IMAGE; NORM_EQ_0; VECTOR_SUB_EQ] THEN
+ SUBGOAL_THEN
+ `(\x:real^N. lift(norm(x - c))) = (lift o norm) o (\x. x - c)`
+ SUBST1_TAC THENL [REWRITE_TAC[o_DEF]; ALL_TAC] THEN
+ MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
+ ASM_SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST;
+ CONTINUOUS_ON_LIFT_NORM];
+ REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_CBALL; o_THM; dist] THEN
+ X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
+ REWRITE_TAC[VECTOR_ARITH `c - (&2 % c - (c + x)) = x`] THEN
+ REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN
+ ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN
+ ASM_REAL_ARITH_TAC;
+ REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(c /\ b) <=> c ==> ~b`] THEN
+ REWRITE_TAC[IN_CBALL; o_THM; dist] THEN
+ X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
+ REWRITE_TAC[VECTOR_ARITH `&2 % c - (c + x') = x <=> --x' = x - c`] THEN
+ ASM_CASES_TAC `(x:real^N) IN path_component s c` THENL
+ [MATCH_MP_TAC(NORM_ARITH `norm(y) < B /\ norm(x) = B ==> ~(--x = y)`) THEN
+ REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN
+ ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN
+ ASM_SIMP_TAC[REAL_ARITH `&0 < B ==> abs B = B`] THEN
+ UNDISCH_TAC `path_component s c SUBSET ball(c:real^N,B)` THEN
+ REWRITE_TAC[SUBSET; IN_BALL] THEN ASM_MESON_TAC[dist; NORM_SUB];
+ EXPAND_TAC "q" THEN REWRITE_TAC[] THEN ASM_REWRITE_TAC[] THEN
+ REWRITE_TAC[VECTOR_ARITH `--(c % x) = x <=> (&1 + c) % x = vec 0`] THEN
+ ASM_REWRITE_TAC[DE_MORGAN_THM; VECTOR_SUB_EQ; VECTOR_MUL_EQ_0] THEN
+ SUBGOAL_THEN `~(x:real^N = c)` ASSUME_TAC THENL
+ [ASM_MESON_TAC[PATH_COMPONENT_REFL; IN]; ALL_TAC] THEN
+ ASM_REWRITE_TAC[] THEN
+ MATCH_MP_TAC(REAL_ARITH `&0 < x ==> ~(&1 + x = &0)`) THEN
+ ASM_SIMP_TAC[REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ]]]);;
+
+let PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove
+ (`!s:real^N->bool a b:real^M.
+ 2 <= dimindex(:N) /\ s homeomorphic interval[a,b]
+ ==> path_connected((:real^N) DIFF s)`,
+ REPEAT STRIP_TAC THEN REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN
+ FIRST_ASSUM(MP_TAC o MATCH_MP
+ UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN
+ ASM_REWRITE_TAC[SET_RULE `~(x IN s) <=> x IN (UNIV DIFF s)`] THEN
+ ABBREV_TAC `t = (:real^N) DIFF s` THEN
+ DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN
+ STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP HOMEOMORPHIC_COMPACTNESS) THEN
+ REWRITE_TAC[COMPACT_INTERVAL] THEN
+ DISCH_THEN(MP_TAC o MATCH_MP COMPACT_IMP_BOUNDED) THEN
+ REWRITE_TAC[BOUNDED_POS; LEFT_IMP_EXISTS_THM] THEN
+ X_GEN_TAC `B:real` THEN STRIP_TAC THEN
+ SUBGOAL_THEN `(?u:real^N. u IN path_component t x /\ B < norm(u)) /\
+ (?v:real^N. v IN path_component t y /\ B < norm(v))`
+ STRIP_ASSUME_TAC THENL
+ [ASM_MESON_TAC[BOUNDED_POS; REAL_NOT_LE]; ALL_TAC] THEN
+ MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `u:real^N` THEN
+ CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN
+ MATCH_MP_TAC PATH_COMPONENT_SYM THEN
+ MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `v:real^N` THEN
+ CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN
+ MATCH_MP_TAC PATH_COMPONENT_OF_SUBSET THEN
+ EXISTS_TAC `(:real^N) DIFF cball(vec 0,B)` THEN CONJ_TAC THENL
+ [EXPAND_TAC "t" THEN MATCH_MP_TAC(SET_RULE
+ `s SUBSET t ==> (u DIFF t) SUBSET (u DIFF s)`) THEN
+ ASM_REWRITE_TAC[SUBSET; IN_CBALL_0];
+ MP_TAC(ISPEC `cball(vec 0:real^N,B)`
+ PATH_CONNECTED_COMPLEMENT_BOUNDED_CONVEX) THEN
+ ASM_REWRITE_TAC[BOUNDED_CBALL; CONVEX_CBALL] THEN
+ REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN
+ DISCH_THEN MATCH_MP_TAC THEN
+ ASM_REWRITE_TAC[IN_DIFF; IN_UNIV; IN_CBALL_0; REAL_NOT_LE]]);;
+
+(* ------------------------------------------------------------------------- *)
+(* In particular, apply all these to the special case of an arc. *)
+(* ------------------------------------------------------------------------- *)
+
+let RETRACTION_ARC = prove
+ (`!p. arc p
+ ==> ?f. f continuous_on (:real^N) /\
+ IMAGE f (:real^N) SUBSET path_image p /\
+ (!x. x IN path_image p ==> f x = x)`,
+ REWRITE_TAC[arc; path; path_image] THEN REPEAT STRIP_TAC THEN
+ MATCH_MP_TAC RETRACTION_INJECTIVE_IMAGE_INTERVAL THEN
+ ASM_REWRITE_TAC[INTERVAL_EQ_EMPTY_1; DROP_VEC; REAL_NOT_LT; REAL_POS]);;
+
+let PATH_CONNECTED_ARC_COMPLEMENT = prove
+ (`!p. 2 <= dimindex(:N) /\ arc p
+ ==> path_connected((:real^N) DIFF path_image p)`,
+ REWRITE_TAC[arc; path] THEN REPEAT STRIP_TAC THEN SIMP_TAC[path_image] THEN
+ MP_TAC(ISPECL [`path_image p:real^N->bool`; `vec 0:real^1`; `vec 1:real^1`]
+ PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN
+ ASM_REWRITE_TAC[path_image] THEN DISCH_THEN MATCH_MP_TAC THEN
+ ONCE_REWRITE_TAC[HOMEOMORPHIC_SYM] THEN
+ MATCH_MP_TAC HOMEOMORPHIC_COMPACT THEN
+ EXISTS_TAC `p:real^1->real^N` THEN ASM_REWRITE_TAC[COMPACT_INTERVAL]);;
+
+let CONNECTED_ARC_COMPLEMENT = prove
+ (`!p. 2 <= dimindex(:N) /\ arc p
+ ==> connected((:real^N) DIFF path_image p)`,
+ SIMP_TAC[PATH_CONNECTED_ARC_COMPLEMENT; PATH_CONNECTED_IMP_CONNECTED]);; *)
+
+end
--- a/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy Tue Apr 27 16:24:57 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy Tue Apr 27 11:17:50 2010 -0700
@@ -1,5 +1,5 @@
theory Multivariate_Analysis
-imports Determinants Integration Real_Integration
+imports Determinants Integration Real_Integration Fashoda
begin
end
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Apr 27 16:24:57 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Apr 27 11:17:50 2010 -0700
@@ -250,8 +250,6 @@
lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s"
by (simp add: expand_set_eq)
-subsection{* Topological properties of open balls *}
-
lemma diff_less_iff: "(a::real) - b > 0 \<longleftrightarrow> a > b"
"(a::real) - b < 0 \<longleftrightarrow> a < b"
"a - b < c \<longleftrightarrow> a < c +b" "a - b > c \<longleftrightarrow> a > c +b" by arith+
@@ -965,7 +963,9 @@
using frontier_complement frontier_subset_eq[of "- S"]
unfolding open_closed by auto
-subsection{* Common nets and The "within" modifier for nets. *}
+subsection {* Nets and the ``eventually true'' quantifier *}
+
+text {* Common nets and The "within" modifier for nets. *}
definition
at_infinity :: "'a::real_normed_vector net" where
@@ -989,7 +989,7 @@
then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x \<and> Q x" ..
qed auto
-subsection{* Identify Trivial limits, where we can't approach arbitrarily closely. *}
+text {* Identify Trivial limits, where we can't approach arbitrarily closely. *}
definition
trivial_limit :: "'a net \<Rightarrow> bool" where
@@ -1040,7 +1040,7 @@
lemma trivial_limit_sequentially[intro]: "\<not> trivial_limit sequentially"
by (auto simp add: trivial_limit_def eventually_sequentially)
-subsection{* Some property holds "sufficiently close" to the limit point. *}
+text {* Some property holds "sufficiently close" to the limit point. *}
lemma eventually_at: (* FIXME: this replaces Limits.eventually_at *)
"eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
@@ -1096,7 +1096,7 @@
lemma not_eventually: "(\<forall>x. \<not> P x ) \<Longrightarrow> ~(trivial_limit net) ==> ~(eventually (\<lambda>x. P x) net)"
by (simp add: eventually_False)
-subsection{* Limits, defined as vacuously true when the limit is trivial. *}
+subsection {* Limits *}
text{* Notation Lim to avoid collition with lim defined in analysis *}
definition
@@ -1266,6 +1266,23 @@
shows "(f ---> l) net \<Longrightarrow> (g ---> m) net \<Longrightarrow> ((\<lambda>x. f(x) - g(x)) ---> l - m) net"
by (rule tendsto_diff)
+lemma Lim_mul:
+ fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+ assumes "(c ---> d) net" "(f ---> l) net"
+ shows "((\<lambda>x. c(x) *\<^sub>R f x) ---> (d *\<^sub>R l)) net"
+ using assms by (rule scaleR.tendsto)
+
+lemma Lim_inv:
+ fixes f :: "'a \<Rightarrow> real"
+ assumes "(f ---> l) (net::'a net)" "l \<noteq> 0"
+ shows "((inverse o f) ---> inverse l) net"
+ unfolding o_def using assms by (rule tendsto_inverse)
+
+lemma Lim_vmul:
+ fixes c :: "'a \<Rightarrow> real" and v :: "'b::real_normed_vector"
+ shows "(c ---> d) net ==> ((\<lambda>x. c(x) *\<^sub>R v) ---> d *\<^sub>R v) net"
+ by (intro tendsto_intros)
+
lemma Lim_null:
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
shows "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net" by (simp add: Lim dist_norm)
@@ -1441,6 +1458,8 @@
unfolding tendsto_def Limits.eventually_within eventually_at_topological
by auto
+lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
+
lemma Lim_at_id: "(id ---> a) (at a)"
apply (subst within_UNIV[symmetric]) by (simp add: Lim_within_id)
@@ -1640,11 +1659,16 @@
text{* Some other lemmas about sequences. *}
+lemma sequentially_offset:
+ assumes "eventually (\<lambda>i. P i) sequentially"
+ shows "eventually (\<lambda>i. P (i + k)) sequentially"
+ using assms unfolding eventually_sequentially by (metis trans_le_add1)
+
lemma seq_offset:
- fixes l :: "'a::metric_space" (* TODO: generalize *)
- shows "(f ---> l) sequentially ==> ((\<lambda>i. f( i + k)) ---> l) sequentially"
- apply (auto simp add: Lim_sequentially)
- by (metis trans_le_add1 )
+ assumes "(f ---> l) sequentially"
+ shows "((\<lambda>i. f (i + k)) ---> l) sequentially"
+ using assms unfolding tendsto_def
+ by clarify (rule sequentially_offset, simp)
lemma seq_offset_neg:
"(f ---> l) sequentially ==> ((\<lambda>i. f(i - k)) ---> l) sequentially"
@@ -1673,7 +1697,7 @@
thus ?thesis unfolding Lim_sequentially dist_norm by simp
qed
-text{* More properties of closed balls. *}
+subsection {* More properties of closed balls. *}
lemma closed_cball: "closed (cball x e)"
unfolding cball_def closed_def
@@ -2156,7 +2180,9 @@
apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
done
-subsection{* Compactness (the definition is the one based on convegent subsequences). *}
+subsection {* Equivalent versions of compactness *}
+
+subsubsection{* Sequential compactness *}
definition
compact :: "'a::metric_space set \<Rightarrow> bool" where (* TODO: generalize *)
@@ -2390,7 +2416,7 @@
using l r by fast
qed
-subsection{* Completeness. *}
+subsubsection{* Completeness *}
lemma cauchy_def:
"Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N --> dist(s m)(s n) < e)"
@@ -2537,7 +2563,7 @@
unfolding image_def
by auto
-subsection{* Total boundedness. *}
+subsubsection{* Total boundedness *}
fun helper_1::"('a::metric_space set) \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> 'a" where
"helper_1 s e n = (SOME y::'a. y \<in> s \<and> (\<forall>m<n. \<not> (dist (helper_1 s e m) y < e)))"
@@ -2570,7 +2596,9 @@
using x[THEN spec[where x="r (N+1)"], THEN spec[where x="r (N)"]] by auto
qed
-subsection{* Heine-Borel theorem (following Burkill \& Burkill vol. 2) *}
+subsubsection{* Heine-Borel theorem *}
+
+text {* Following Burkill \& Burkill vol. 2. *}
lemma heine_borel_lemma: fixes s::"'a::metric_space set"
assumes "compact s" "s \<subseteq> (\<Union> t)" "\<forall>b \<in> t. open b"
@@ -2634,7 +2662,7 @@
ultimately show "\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f'" using bb k(2) by (rule_tac x="bb ` k" in exI) auto
qed
-subsection{* Bolzano-Weierstrass property. *}
+subsubsection {* Bolzano-Weierstrass property *}
lemma heine_borel_imp_bolzano_weierstrass:
assumes "\<forall>f. (\<forall>t \<in> f. open t) \<and> s \<subseteq> (\<Union> f) --> (\<exists>f'. f' \<subseteq> f \<and> finite f' \<and> s \<subseteq> (\<Union> f'))"
@@ -2662,7 +2690,7 @@
ultimately show False using g(2) using finite_subset by auto
qed
-subsection{* Complete the chain of compactness variants. *}
+subsubsection {* Complete the chain of compactness variants *}
primrec helper_2::"(real \<Rightarrow> 'a::metric_space) \<Rightarrow> nat \<Rightarrow> 'a" where
"helper_2 beyond 0 = beyond 0" |
@@ -3098,7 +3126,9 @@
ultimately show ?thesis by auto
qed
-subsection{* Define continuity over a net to take in restrictions of the set. *}
+subsection {* Continuity *}
+
+text {* Define continuity over a net to take in restrictions of the set. *}
definition
continuous :: "'a::t2_space net \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool" where
@@ -3166,59 +3196,37 @@
apply auto apply(erule_tac x=e in allE) apply auto apply(rule_tac x=d in exI) apply auto apply(erule_tac x="f xa" in allE) by (auto simp add: dist_commute dist_nz)
qed
-text{* For setwise continuity, just start from the epsilon-delta definitions. *}
+text{* Define setwise continuity in terms of limits within the set. *}
definition
continuous_on ::
"'a set \<Rightarrow> ('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> bool"
where
+ "continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. (f ---> f x) (at x within s))"
+
+lemma continuous_on_topological:
"continuous_on s f \<longleftrightarrow>
(\<forall>x\<in>s. \<forall>B. open B \<longrightarrow> f x \<in> B \<longrightarrow>
- (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>x'\<in>s. x' \<in> A \<longrightarrow> f x' \<in> B)))"
+ (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)))"
+unfolding continuous_on_def tendsto_def
+unfolding Limits.eventually_within eventually_at_topological
+by (intro ball_cong [OF refl] all_cong imp_cong ex_cong conj_cong refl) auto
lemma continuous_on_iff:
"continuous_on s f \<longleftrightarrow>
- (\<forall>x\<in>s. \<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. dist x' x < d --> dist (f x') (f x) < e)"
-unfolding continuous_on_def
-apply safe
-apply (drule (1) bspec)
-apply (drule_tac x="ball (f x) e" in spec, simp, clarify)
-apply (drule (1) open_dist [THEN iffD1, THEN bspec])
-apply (clarify, rename_tac d)
-apply (rule_tac x=d in exI, clarify)
-apply (drule_tac x=x' in bspec, assumption)
-apply (drule_tac x=x' in spec, simp add: dist_commute)
-apply (drule_tac x=x in bspec, assumption)
-apply (drule (1) open_dist [THEN iffD1, THEN bspec], clarify)
-apply (drule_tac x=e in spec, simp, clarify)
-apply (rule_tac x="ball x d" in exI, simp, clarify)
-apply (drule_tac x=x' in bspec, assumption)
-apply (simp add: dist_commute)
+ (\<forall>x\<in>s. \<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
+unfolding continuous_on_def Lim_within
+apply (intro ball_cong [OF refl] all_cong ex_cong)
+apply (rename_tac y, case_tac "y = x", simp)
+apply (simp add: dist_nz)
done
definition
uniformly_continuous_on ::
- "'a::metric_space set \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> bool" where
+ "'a set \<Rightarrow> ('a::metric_space \<Rightarrow> 'b::metric_space) \<Rightarrow> bool"
+where
"uniformly_continuous_on s f \<longleftrightarrow>
- (\<forall>e>0. \<exists>d>0. \<forall>x\<in>s. \<forall> x'\<in>s. dist x' x < d
- --> dist (f x') (f x) < e)"
-
-
-text{* Lifting and dropping *}
-
-lemma continuous_on_o_dest_vec1: fixes f::"real \<Rightarrow> 'a::real_normed_vector"
- assumes "continuous_on {a..b::real} f" shows "continuous_on {vec1 a..vec1 b} (f o dest_vec1)"
- using assms unfolding continuous_on_iff apply safe
- apply(erule_tac x="x$1" in ballE,erule_tac x=e in allE) apply safe
- apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real
- apply(erule_tac x="dest_vec1 x'" in ballE) by(auto simp add:vector_le_def)
-
-lemma continuous_on_o_vec1: fixes f::"real^1 \<Rightarrow> 'a::real_normed_vector"
- assumes "continuous_on {a..b} f" shows "continuous_on {dest_vec1 a..dest_vec1 b} (f o vec1)"
- using assms unfolding continuous_on_iff apply safe
- apply(erule_tac x="vec x" in ballE,erule_tac x=e in allE) apply safe
- apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real
- apply(erule_tac x="vec1 x'" in ballE) by(auto simp add:vector_le_def)
+ (\<forall>e>0. \<exists>d>0. \<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
text{* Some simple consequential lemmas. *}
@@ -3230,50 +3238,44 @@
"continuous (at x) f ==> continuous (at x within s) f"
unfolding continuous_within continuous_at using Lim_at_within by auto
+lemma Lim_trivial_limit: "trivial_limit net \<Longrightarrow> (f ---> l) net"
+unfolding tendsto_def by (simp add: trivial_limit_eq)
+
lemma continuous_at_imp_continuous_on:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
- assumes "(\<forall>x \<in> s. continuous (at x) f)"
+ assumes "\<forall>x\<in>s. continuous (at x) f"
shows "continuous_on s f"
-proof(simp add: continuous_at continuous_on_iff, rule, rule, rule)
- fix x and e::real assume "x\<in>s" "e>0"
- hence "eventually (\<lambda>xa. dist (f xa) (f x) < e) (at x)" using assms unfolding continuous_at tendsto_iff by auto
- then obtain d where d:"d>0" "\<forall>xa. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" unfolding eventually_at by auto
- { fix x' assume "\<not> 0 < dist x' x"
- hence "x=x'"
- using dist_nz[of x' x] by auto
- hence "dist (f x') (f x) < e" using `e>0` by auto
- }
- thus "\<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e" using d by auto
+unfolding continuous_on_def
+proof
+ fix x assume "x \<in> s"
+ with assms have *: "(f ---> f (netlimit (at x))) (at x)"
+ unfolding continuous_def by simp
+ have "(f ---> f x) (at x)"
+ proof (cases "trivial_limit (at x)")
+ case True thus ?thesis
+ by (rule Lim_trivial_limit)
+ next
+ case False
+ hence "netlimit (at x) = x"
+ using netlimit_within [of x UNIV]
+ by (simp add: within_UNIV)
+ with * show ?thesis by simp
+ qed
+ thus "(f ---> f x) (at x within s)"
+ by (rule Lim_at_within)
qed
lemma continuous_on_eq_continuous_within:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
- shows "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. continuous (at x within s) f)"
- (is "?lhs = ?rhs")
-proof
- assume ?rhs
- { fix x assume "x\<in>s"
- fix e::real assume "e>0"
- assume "\<exists>d>0. \<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e"
- then obtain d where "d>0" and d:"\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" by auto
- { fix x' assume as:"x'\<in>s" "dist x' x < d"
- hence "dist (f x') (f x) < e" using `e>0` d `x'\<in>s` dist_eq_0_iff[of x' x] zero_le_dist[of x' x] as(2) by (metis dist_eq_0_iff dist_nz) }
- hence "\<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e" using `d>0` by auto
- }
- thus ?lhs using `?rhs` unfolding continuous_on_iff continuous_within Lim_within by auto
-next
- assume ?lhs
- thus ?rhs unfolding continuous_on_iff continuous_within Lim_within by blast
-qed
-
-lemma continuous_on:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
- shows "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. (f ---> f(x)) (at x within s))"
- by (auto simp add: continuous_on_eq_continuous_within continuous_within)
- (* BH: maybe this should be the definition? *)
+ "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. continuous (at x within s) f)"
+unfolding continuous_on_def continuous_def
+apply (rule ball_cong [OF refl])
+apply (case_tac "trivial_limit (at x within s)")
+apply (simp add: Lim_trivial_limit)
+apply (simp add: netlimit_within)
+done
+
+lemmas continuous_on = continuous_on_def -- "legacy theorem name"
lemma continuous_on_eq_continuous_at:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
shows "open s ==> (continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. continuous (at x) f))"
by (auto simp add: continuous_on continuous_at Lim_within_open)
@@ -3283,22 +3285,19 @@
unfolding continuous_within by(metis Lim_within_subset)
lemma continuous_on_subset:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
shows "continuous_on s f \<Longrightarrow> t \<subseteq> s ==> continuous_on t f"
unfolding continuous_on by (metis subset_eq Lim_within_subset)
lemma continuous_on_interior:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
shows "continuous_on s f \<Longrightarrow> x \<in> interior s ==> continuous (at x) f"
unfolding interior_def
apply simp
by (meson continuous_on_eq_continuous_at continuous_on_subset)
lemma continuous_on_eq:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
- shows "(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f
- ==> continuous_on s g"
- by (simp add: continuous_on_iff)
+ "(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on s g"
+ unfolding continuous_on_def tendsto_def Limits.eventually_within
+ by simp
text{* Characterization of various kinds of continuity in terms of sequences. *}
@@ -3351,7 +3350,7 @@
using continuous_within_sequentially[of a UNIV f] unfolding within_UNIV by auto
lemma continuous_on_sequentially:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
shows "continuous_on s f \<longleftrightarrow>
(\<forall>x. \<forall>a \<in> s. (\<forall>n. x(n) \<in> s) \<and> (x ---> a) sequentially
--> ((f o x) ---> f(a)) sequentially)" (is "?lhs = ?rhs")
@@ -3361,24 +3360,23 @@
assume ?lhs thus ?rhs unfolding continuous_on_eq_continuous_within using continuous_within_sequentially[of _ s f] by auto
qed
-lemma uniformly_continuous_on_sequentially:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
- shows "uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and>
- ((\<lambda>n. x n - y n) ---> 0) sequentially
- \<longrightarrow> ((\<lambda>n. f(x n) - f(y n)) ---> 0) sequentially)" (is "?lhs = ?rhs")
+lemma uniformly_continuous_on_sequentially':
+ "uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and>
+ ((\<lambda>n. dist (x n) (y n)) ---> 0) sequentially
+ \<longrightarrow> ((\<lambda>n. dist (f(x n)) (f(y n))) ---> 0) sequentially)" (is "?lhs = ?rhs")
proof
assume ?lhs
- { fix x y assume x:"\<forall>n. x n \<in> s" and y:"\<forall>n. y n \<in> s" and xy:"((\<lambda>n. x n - y n) ---> 0) sequentially"
+ { fix x y assume x:"\<forall>n. x n \<in> s" and y:"\<forall>n. y n \<in> s" and xy:"((\<lambda>n. dist (x n) (y n)) ---> 0) sequentially"
{ fix e::real assume "e>0"
then obtain d where "d>0" and d:"\<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
using `?lhs`[unfolded uniformly_continuous_on_def, THEN spec[where x=e]] by auto
- obtain N where N:"\<forall>n\<ge>N. norm (x n - y n - 0) < d" using xy[unfolded Lim_sequentially dist_norm] and `d>0` by auto
+ obtain N where N:"\<forall>n\<ge>N. dist (x n) (y n) < d" using xy[unfolded Lim_sequentially dist_norm] and `d>0` by auto
{ fix n assume "n\<ge>N"
- hence "norm (f (x n) - f (y n) - 0) < e"
+ hence "dist (f (x n)) (f (y n)) < e"
using N[THEN spec[where x=n]] using d[THEN bspec[where x="x n"], THEN bspec[where x="y n"]] using x and y
- unfolding dist_commute and dist_norm by simp }
- hence "\<exists>N. \<forall>n\<ge>N. norm (f (x n) - f (y n) - 0) < e" by auto }
- hence "((\<lambda>n. f(x n) - f(y n)) ---> 0) sequentially" unfolding Lim_sequentially and dist_norm by auto }
+ unfolding dist_commute by simp }
+ hence "\<exists>N. \<forall>n\<ge>N. dist (f (x n)) (f (y n)) < e" by auto }
+ hence "((\<lambda>n. dist (f(x n)) (f(y n))) ---> 0) sequentially" unfolding Lim_sequentially and dist_real_def by auto }
thus ?rhs by auto
next
assume ?rhs
@@ -3391,25 +3389,32 @@
def y \<equiv> "\<lambda>n::nat. snd (fa (inverse (real n + 1)))"
have xyn:"\<forall>n. x n \<in> s \<and> y n \<in> s" and xy0:"\<forall>n. dist (x n) (y n) < inverse (real n + 1)" and fxy:"\<forall>n. \<not> dist (f (x n)) (f (y n)) < e"
unfolding x_def and y_def using fa by auto
- have 1:"\<And>(x::'a) y. dist (x - y) 0 = dist x y" unfolding dist_norm by auto
- have 2:"\<And>(x::'b) y. dist (x - y) 0 = dist x y" unfolding dist_norm by auto
{ fix e::real assume "e>0"
then obtain N::nat where "N \<noteq> 0" and N:"0 < inverse (real N) \<and> inverse (real N) < e" unfolding real_arch_inv[of e] by auto
{ fix n::nat assume "n\<ge>N"
hence "inverse (real n + 1) < inverse (real N)" using real_of_nat_ge_zero and `N\<noteq>0` by auto
also have "\<dots> < e" using N by auto
finally have "inverse (real n + 1) < e" by auto
- hence "dist (x n - y n) 0 < e" unfolding 1 using xy0[THEN spec[where x=n]] by auto }
- hence "\<exists>N. \<forall>n\<ge>N. dist (x n - y n) 0 < e" by auto }
- hence "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f (x n) - f (y n)) 0 < e" using `?rhs`[THEN spec[where x=x], THEN spec[where x=y]] and xyn unfolding Lim_sequentially by auto
- hence False unfolding 2 using fxy and `e>0` by auto }
+ hence "dist (x n) (y n) < e" using xy0[THEN spec[where x=n]] by auto }
+ hence "\<exists>N. \<forall>n\<ge>N. dist (x n) (y n) < e" by auto }
+ hence "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f (x n)) (f (y n)) < e" using `?rhs`[THEN spec[where x=x], THEN spec[where x=y]] and xyn unfolding Lim_sequentially dist_real_def by auto
+ hence False using fxy and `e>0` by auto }
thus ?lhs unfolding uniformly_continuous_on_def by blast
qed
+lemma uniformly_continuous_on_sequentially:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+ shows "uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and>
+ ((\<lambda>n. x n - y n) ---> 0) sequentially
+ \<longrightarrow> ((\<lambda>n. f(x n) - f(y n)) ---> 0) sequentially)" (is "?lhs = ?rhs")
+(* BH: maybe the previous lemma should replace this one? *)
+unfolding uniformly_continuous_on_sequentially'
+unfolding dist_norm Lim_null_norm [symmetric] ..
+
text{* The usual transformation theorems. *}
lemma continuous_transform_within:
- fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+ fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "0 < d" "x \<in> s" "\<forall>x' \<in> s. dist x' x < d --> f x' = g x'"
"continuous (at x within s) f"
shows "continuous (at x within s) g"
@@ -3425,7 +3430,7 @@
qed
lemma continuous_transform_at:
- fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+ fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "0 < d" "\<forall>x'. dist x' x < d --> f x' = g x'"
"continuous (at x) f"
shows "continuous (at x) g"
@@ -3475,26 +3480,26 @@
unfolding continuous_on_def by auto
lemma continuous_on_cmul:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
- shows "continuous_on s f ==> continuous_on s (\<lambda>x. c *\<^sub>R (f x))"
- unfolding continuous_on_eq_continuous_within using continuous_cmul by blast
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
+ shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. c *\<^sub>R (f x))"
+ unfolding continuous_on_def by (auto intro: tendsto_intros)
lemma continuous_on_neg:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. - f x)"
- unfolding continuous_on_eq_continuous_within using continuous_neg by blast
+ unfolding continuous_on_def by (auto intro: tendsto_intros)
lemma continuous_on_add:
- fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "continuous_on s f \<Longrightarrow> continuous_on s g
\<Longrightarrow> continuous_on s (\<lambda>x. f x + g x)"
- unfolding continuous_on_eq_continuous_within using continuous_add by blast
+ unfolding continuous_on_def by (auto intro: tendsto_intros)
lemma continuous_on_sub:
- fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "continuous_on s f \<Longrightarrow> continuous_on s g
\<Longrightarrow> continuous_on s (\<lambda>x. f x - g x)"
- unfolding continuous_on_eq_continuous_within using continuous_sub by blast
+ unfolding continuous_on_def by (auto intro: tendsto_intros)
text{* Same thing for uniform continuity, using sequential formulations. *}
@@ -3503,8 +3508,7 @@
unfolding uniformly_continuous_on_def by simp
lemma uniformly_continuous_on_cmul:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
- (* FIXME: generalize 'a to metric_space *)
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
assumes "uniformly_continuous_on s f"
shows "uniformly_continuous_on s (\<lambda>x. c *\<^sub>R f(x))"
proof-
@@ -3513,7 +3517,8 @@
using Lim_cmul[of "(\<lambda>n. f (x n) - f (y n))" 0 sequentially c]
unfolding scaleR_zero_right scaleR_right_diff_distrib by auto
}
- thus ?thesis using assms unfolding uniformly_continuous_on_sequentially by auto
+ thus ?thesis using assms unfolding uniformly_continuous_on_sequentially'
+ unfolding dist_norm Lim_null_norm [symmetric] by auto
qed
lemma dist_minus:
@@ -3528,7 +3533,7 @@
unfolding uniformly_continuous_on_def dist_minus .
lemma uniformly_continuous_on_add:
- fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" (* FIXME: generalize 'a *)
+ fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
assumes "uniformly_continuous_on s f" "uniformly_continuous_on s g"
shows "uniformly_continuous_on s (\<lambda>x. f x + g x)"
proof-
@@ -3537,11 +3542,12 @@
hence "((\<lambda>xa. f (x xa) - f (y xa) + (g (x xa) - g (y xa))) ---> 0 + 0) sequentially"
using Lim_add[of "\<lambda> n. f (x n) - f (y n)" 0 sequentially "\<lambda> n. g (x n) - g (y n)" 0] by auto
hence "((\<lambda>n. f (x n) + g (x n) - (f (y n) + g (y n))) ---> 0) sequentially" unfolding Lim_sequentially and add_diff_add [symmetric] by auto }
- thus ?thesis using assms unfolding uniformly_continuous_on_sequentially by auto
+ thus ?thesis using assms unfolding uniformly_continuous_on_sequentially'
+ unfolding dist_norm Lim_null_norm [symmetric] by auto
qed
lemma uniformly_continuous_on_sub:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" (* FIXME: generalize 'a *)
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s g
==> uniformly_continuous_on s (\<lambda>x. f x - g x)"
unfolding ab_diff_minus
@@ -3560,7 +3566,7 @@
lemma continuous_on_id:
"continuous_on s (\<lambda>x. x)"
- unfolding continuous_on_def by auto
+ unfolding continuous_on_def by (auto intro: tendsto_ident_at_within)
lemma uniformly_continuous_on_id:
"uniformly_continuous_on s (\<lambda>x. x)"
@@ -3568,25 +3574,21 @@
text{* Continuity of all kinds is preserved under composition. *}
+lemma continuous_within_topological:
+ "continuous (at x within s) f \<longleftrightarrow>
+ (\<forall>B. open B \<longrightarrow> f x \<in> B \<longrightarrow>
+ (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)))"
+unfolding continuous_within
+unfolding tendsto_def Limits.eventually_within eventually_at_topological
+by (intro ball_cong [OF refl] all_cong imp_cong ex_cong conj_cong refl) auto
+
lemma continuous_within_compose:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
- fixes g :: "'b::metric_space \<Rightarrow> 'c::metric_space"
- assumes "continuous (at x within s) f" "continuous (at (f x) within f ` s) g"
+ assumes "continuous (at x within s) f"
+ assumes "continuous (at (f x) within f ` s) g"
shows "continuous (at x within s) (g o f)"
-proof-
- { fix e::real assume "e>0"
- with assms(2)[unfolded continuous_within Lim_within] obtain d where "d>0" and d:"\<forall>xa\<in>f ` s. 0 < dist xa (f x) \<and> dist xa (f x) < d \<longrightarrow> dist (g xa) (g (f x)) < e" by auto
- from assms(1)[unfolded continuous_within Lim_within] obtain d' where "d'>0" and d':"\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d' \<longrightarrow> dist (f xa) (f x) < d" using `d>0` by auto
- { fix y assume as:"y\<in>s" "0 < dist y x" "dist y x < d'"
- hence "dist (f y) (f x) < d" using d'[THEN bspec[where x=y]] by (auto simp add:dist_commute)
- hence "dist (g (f y)) (g (f x)) < e" using as(1) d[THEN bspec[where x="f y"]] unfolding dist_nz[THEN sym] using `e>0` by auto }
- hence "\<exists>d>0. \<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (g (f xa)) (g (f x)) < e" using `d'>0` by auto }
- thus ?thesis unfolding continuous_within Lim_within by auto
-qed
+using assms unfolding continuous_within_topological by simp metis
lemma continuous_at_compose:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
- fixes g :: "'b::metric_space \<Rightarrow> 'c::metric_space"
assumes "continuous (at x) f" "continuous (at (f x)) g"
shows "continuous (at x) (g o f)"
proof-
@@ -3595,10 +3597,8 @@
qed
lemma continuous_on_compose:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
- fixes g :: "'b::metric_space \<Rightarrow> 'c::metric_space" (* TODO: generalize *)
- shows "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)"
- unfolding continuous_on_eq_continuous_within using continuous_within_compose[of _ s f g] by auto
+ "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)"
+ unfolding continuous_on_topological by simp metis
lemma uniformly_continuous_on_compose:
assumes "uniformly_continuous_on s f" "uniformly_continuous_on (f ` s) g"
@@ -3614,75 +3614,55 @@
text{* Continuity in terms of open preimages. *}
lemma continuous_at_open:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
- shows "continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t --> (\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x' \<in> s. (f x') \<in> t)))" (is "?lhs = ?rhs")
-proof
- assume ?lhs
- { fix t assume as: "open t" "f x \<in> t"
- then obtain e where "e>0" and e:"ball (f x) e \<subseteq> t" unfolding open_contains_ball by auto
-
- obtain d where "d>0" and d:"\<forall>y. 0 < dist y x \<and> dist y x < d \<longrightarrow> dist (f y) (f x) < e" using `e>0` using `?lhs`[unfolded continuous_at Lim_at open_dist] by auto
-
- have "open (ball x d)" using open_ball by auto
- moreover have "x \<in> ball x d" unfolding centre_in_ball using `d>0` by simp
- moreover
- { fix x' assume "x'\<in>ball x d" hence "f x' \<in> t"
- using e[unfolded subset_eq Ball_def mem_ball, THEN spec[where x="f x'"]] d[THEN spec[where x=x']]
- unfolding mem_ball apply (auto simp add: dist_commute)
- unfolding dist_nz[THEN sym] using as(2) by auto }
- hence "\<forall>x'\<in>ball x d. f x' \<in> t" by auto
- ultimately have "\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x'\<in>s. f x' \<in> t)"
- apply(rule_tac x="ball x d" in exI) by simp }
- thus ?rhs by auto
-next
- assume ?rhs
- { fix e::real assume "e>0"
- then obtain s where s: "open s" "x \<in> s" "\<forall>x'\<in>s. f x' \<in> ball (f x) e" using `?rhs`[unfolded continuous_at Lim_at, THEN spec[where x="ball (f x) e"]]
- unfolding centre_in_ball[of "f x" e, THEN sym] by auto
- then obtain d where "d>0" and d:"ball x d \<subseteq> s" unfolding open_contains_ball by auto
- { fix y assume "0 < dist y x \<and> dist y x < d"
- hence "dist (f y) (f x) < e" using d[unfolded subset_eq Ball_def mem_ball, THEN spec[where x=y]]
- using s(3)[THEN bspec[where x=y], unfolded mem_ball] by (auto simp add: dist_commute) }
- hence "\<exists>d>0. \<forall>xa. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" using `d>0` by auto }
- thus ?lhs unfolding continuous_at Lim_at by auto
-qed
+ shows "continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t --> (\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x' \<in> s. (f x') \<in> t)))"
+unfolding continuous_within_topological [of x UNIV f, unfolded within_UNIV]
+unfolding imp_conjL by (intro all_cong imp_cong ex_cong conj_cong refl) auto
lemma continuous_on_open:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
- shows "continuous_on s f \<longleftrightarrow>
+ shows "continuous_on s f \<longleftrightarrow>
(\<forall>t. openin (subtopology euclidean (f ` s)) t
--> openin (subtopology euclidean s) {x \<in> s. f x \<in> t})" (is "?lhs = ?rhs")
-proof
- assume ?lhs
- { fix t assume as:"openin (subtopology euclidean (f ` s)) t"
- have "{x \<in> s. f x \<in> t} \<subseteq> s" using as[unfolded openin_euclidean_subtopology_iff] by auto
- moreover
- { fix x assume as':"x\<in>{x \<in> s. f x \<in> t}"
- then obtain e where e: "e>0" "\<forall>x'\<in>f ` s. dist x' (f x) < e \<longrightarrow> x' \<in> t" using as[unfolded openin_euclidean_subtopology_iff, THEN conjunct2, THEN bspec[where x="f x"]] by auto
- from this(1) obtain d where d: "d>0" "\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" using `?lhs`[unfolded continuous_on Lim_within, THEN bspec[where x=x]] using as' by auto
- have "\<exists>e>0. \<forall>x'\<in>s. dist x' x < e \<longrightarrow> x' \<in> {x \<in> s. f x \<in> t}" using d e unfolding dist_nz[THEN sym] by (rule_tac x=d in exI, auto) }
- ultimately have "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}" unfolding openin_euclidean_subtopology_iff by auto }
- thus ?rhs unfolding continuous_on Lim_within using openin by auto
+proof (safe)
+ fix t :: "'b set"
+ assume 1: "continuous_on s f"
+ assume 2: "openin (subtopology euclidean (f ` s)) t"
+ from 2 obtain B where B: "open B" and t: "t = f ` s \<inter> B"
+ unfolding openin_open by auto
+ def U == "\<Union>{A. open A \<and> (\<forall>x\<in>s. x \<in> A \<longrightarrow> f x \<in> B)}"
+ have "open U" unfolding U_def by (simp add: open_Union)
+ moreover have "\<forall>x\<in>s. x \<in> U \<longleftrightarrow> f x \<in> t"
+ proof (intro ballI iffI)
+ fix x assume "x \<in> s" and "x \<in> U" thus "f x \<in> t"
+ unfolding U_def t by auto
+ next
+ fix x assume "x \<in> s" and "f x \<in> t"
+ hence "x \<in> s" and "f x \<in> B"
+ unfolding t by auto
+ with 1 B obtain A where "open A" "x \<in> A" "\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B"
+ unfolding t continuous_on_topological by metis
+ then show "x \<in> U"
+ unfolding U_def by auto
+ qed
+ ultimately have "open U \<and> {x \<in> s. f x \<in> t} = s \<inter> U" by auto
+ then show "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
+ unfolding openin_open by fast
next
- assume ?rhs
- { fix e::real and x assume "x\<in>s" "e>0"
- { fix xa x' assume "dist (f xa) (f x) < e" "xa \<in> s" "x' \<in> s" "dist (f xa) (f x') < e - dist (f xa) (f x)"
- hence "dist (f x') (f x) < e" using dist_triangle[of "f x'" "f x" "f xa"]
- by (auto simp add: dist_commute) }
- hence "ball (f x) e \<inter> f ` s \<subseteq> f ` s \<and> (\<forall>xa\<in>ball (f x) e \<inter> f ` s. \<exists>ea>0. \<forall>x'\<in>f ` s. dist x' xa < ea \<longrightarrow> x' \<in> ball (f x) e \<inter> f ` s)" apply auto
- apply(rule_tac x="e - dist (f xa) (f x)" in exI) using `e>0` by (auto simp add: dist_commute)
- hence "\<forall>xa\<in>{xa \<in> s. f xa \<in> ball (f x) e \<inter> f ` s}. \<exists>ea>0. \<forall>x'\<in>s. dist x' xa < ea \<longrightarrow> x' \<in> {xa \<in> s. f xa \<in> ball (f x) e \<inter> f ` s}"
- using `?rhs`[unfolded openin_euclidean_subtopology_iff, THEN spec[where x="ball (f x) e \<inter> f ` s"]] by auto
- hence "\<exists>d>0. \<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" apply(erule_tac x=x in ballE) apply auto using `e>0` `x\<in>s` by (auto simp add: dist_commute) }
- thus ?lhs unfolding continuous_on Lim_within by auto
-qed
-
-(* ------------------------------------------------------------------------- *)
-(* Similarly in terms of closed sets. *)
-(* ------------------------------------------------------------------------- *)
+ assume "?rhs" show "continuous_on s f"
+ unfolding continuous_on_topological
+ proof (clarify)
+ fix x and B assume "x \<in> s" and "open B" and "f x \<in> B"
+ have "openin (subtopology euclidean (f ` s)) (f ` s \<inter> B)"
+ unfolding openin_open using `open B` by auto
+ then have "openin (subtopology euclidean s) {x \<in> s. f x \<in> f ` s \<inter> B}"
+ using `?rhs` by fast
+ then show "\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)"
+ unfolding openin_open using `x \<in> s` and `f x \<in> B` by auto
+ qed
+qed
+
+text {* Similarly in terms of closed sets. *}
lemma continuous_on_closed:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
shows "continuous_on s f \<longleftrightarrow> (\<forall>t. closedin (subtopology euclidean (f ` s)) t --> closedin (subtopology euclidean s) {x \<in> s. f x \<in> t})" (is "?lhs = ?rhs")
proof
assume ?lhs
@@ -3707,7 +3687,6 @@
text{* Half-global and completely global cases. *}
lemma continuous_open_in_preimage:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "continuous_on s f" "open t"
shows "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
proof-
@@ -3718,7 +3697,6 @@
qed
lemma continuous_closed_in_preimage:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "continuous_on s f" "closed t"
shows "closedin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
proof-
@@ -3730,7 +3708,6 @@
qed
lemma continuous_open_preimage:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "continuous_on s f" "open s" "open t"
shows "open {x \<in> s. f x \<in> t}"
proof-
@@ -3740,7 +3717,6 @@
qed
lemma continuous_closed_preimage:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "continuous_on s f" "closed s" "closed t"
shows "closed {x \<in> s. f x \<in> t}"
proof-
@@ -3750,26 +3726,22 @@
qed
lemma continuous_open_preimage_univ:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
shows "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open {x. f x \<in> s}"
using continuous_open_preimage[of UNIV f s] open_UNIV continuous_at_imp_continuous_on by auto
lemma continuous_closed_preimage_univ:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
shows "(\<forall>x. continuous (at x) f) \<Longrightarrow> closed s ==> closed {x. f x \<in> s}"
using continuous_closed_preimage[of UNIV f s] closed_UNIV continuous_at_imp_continuous_on by auto
lemma continuous_open_vimage:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
shows "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open (f -` s)"
unfolding vimage_def by (rule continuous_open_preimage_univ)
lemma continuous_closed_vimage:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
shows "\<forall>x. continuous (at x) f \<Longrightarrow> closed s \<Longrightarrow> closed (f -` s)"
unfolding vimage_def by (rule continuous_closed_preimage_univ)
-lemma interior_image_subset: fixes f::"_::metric_space \<Rightarrow> _::metric_space"
+lemma interior_image_subset:
assumes "\<forall>x. continuous (at x) f" "inj f"
shows "interior (f ` s) \<subseteq> f ` (interior s)"
apply rule unfolding interior_def mem_Collect_eq image_iff apply safe
@@ -3783,17 +3755,17 @@
text{* Equality of continuous functions on closure and related results. *}
lemma continuous_closed_in_preimage_constant:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
shows "continuous_on s f ==> closedin (subtopology euclidean s) {x \<in> s. f x = a}"
using continuous_closed_in_preimage[of s f "{a}"] closed_sing by auto
lemma continuous_closed_preimage_constant:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
shows "continuous_on s f \<Longrightarrow> closed s ==> closed {x \<in> s. f x = a}"
using continuous_closed_preimage[of s f "{a}"] closed_sing by auto
lemma continuous_constant_on_closure:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
assumes "continuous_on (closure s) f"
"\<forall>x \<in> s. f x = a"
shows "\<forall>x \<in> (closure s). f x = a"
@@ -3801,7 +3773,6 @@
assms closure_minimal[of s "{x \<in> closure s. f x = a}"] closure_subset unfolding subset_eq by auto
lemma image_closure_subset:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "continuous_on (closure s) f" "closed t" "(f ` s) \<subseteq> t"
shows "f ` (closure s) \<subseteq> t"
proof-
@@ -3860,14 +3831,14 @@
text{* Proving a function is constant by proving open-ness of level set. *}
lemma continuous_levelset_open_in_cases:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
shows "connected s \<Longrightarrow> continuous_on s f \<Longrightarrow>
openin (subtopology euclidean s) {x \<in> s. f x = a}
==> (\<forall>x \<in> s. f x \<noteq> a) \<or> (\<forall>x \<in> s. f x = a)"
unfolding connected_clopen using continuous_closed_in_preimage_constant by auto
lemma continuous_levelset_open_in:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
shows "connected s \<Longrightarrow> continuous_on s f \<Longrightarrow>
openin (subtopology euclidean s) {x \<in> s. f x = a} \<Longrightarrow>
(\<exists>x \<in> s. f x = a) ==> (\<forall>x \<in> s. f x = a)"
@@ -3875,7 +3846,7 @@
by meson
lemma continuous_levelset_open:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
assumes "connected s" "continuous_on s f" "open {x \<in> s. f x = a}" "\<exists>x \<in> s. f x = a"
shows "\<forall>x \<in> s. f x = a"
using continuous_levelset_open_in[OF assms(1,2), of a, unfolded openin_open] using assms (3,4) by fast
@@ -3949,7 +3920,104 @@
thus "x \<in> interior (op + a ` s)" unfolding mem_interior using `e>0` by auto
qed
-subsection {* Preservation of compactness and connectedness under continuous function. *}
+text {* We can now extend limit compositions to consider the scalar multiplier. *}
+
+lemma continuous_vmul:
+ fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
+ shows "continuous net c ==> continuous net (\<lambda>x. c(x) *\<^sub>R v)"
+ unfolding continuous_def using Lim_vmul[of c] by auto
+
+lemma continuous_mul:
+ fixes c :: "'a::metric_space \<Rightarrow> real"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "continuous net c \<Longrightarrow> continuous net f
+ ==> continuous net (\<lambda>x. c(x) *\<^sub>R f x) "
+ unfolding continuous_def by (intro tendsto_intros)
+
+lemmas continuous_intros = continuous_add continuous_vmul continuous_cmul continuous_const continuous_sub continuous_at_id continuous_within_id continuous_mul
+
+lemma continuous_on_vmul:
+ fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
+ shows "continuous_on s c ==> continuous_on s (\<lambda>x. c(x) *\<^sub>R v)"
+ unfolding continuous_on_eq_continuous_within using continuous_vmul[of _ c] by auto
+
+lemma continuous_on_mul:
+ fixes c :: "'a::metric_space \<Rightarrow> real"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "continuous_on s c \<Longrightarrow> continuous_on s f
+ ==> continuous_on s (\<lambda>x. c(x) *\<^sub>R f x)"
+ unfolding continuous_on_eq_continuous_within using continuous_mul[of _ c] by auto
+
+lemmas continuous_on_intros = continuous_on_add continuous_on_const continuous_on_id continuous_on_compose continuous_on_cmul continuous_on_neg continuous_on_sub
+ uniformly_continuous_on_add uniformly_continuous_on_const uniformly_continuous_on_id uniformly_continuous_on_compose uniformly_continuous_on_cmul uniformly_continuous_on_neg uniformly_continuous_on_sub
+ continuous_on_mul continuous_on_vmul
+
+text{* And so we have continuity of inverse. *}
+
+lemma continuous_inv:
+ fixes f :: "'a::metric_space \<Rightarrow> real"
+ shows "continuous net f \<Longrightarrow> f(netlimit net) \<noteq> 0
+ ==> continuous net (inverse o f)"
+ unfolding continuous_def using Lim_inv by auto
+
+lemma continuous_at_within_inv:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_field"
+ assumes "continuous (at a within s) f" "f a \<noteq> 0"
+ shows "continuous (at a within s) (inverse o f)"
+ using assms unfolding continuous_within o_def
+ by (intro tendsto_intros)
+
+lemma continuous_at_inv:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_field"
+ shows "continuous (at a) f \<Longrightarrow> f a \<noteq> 0
+ ==> continuous (at a) (inverse o f) "
+ using within_UNIV[THEN sym, of "at a"] using continuous_at_within_inv[of a UNIV] by auto
+
+text {* Topological properties of linear functions. *}
+
+lemma linear_lim_0:
+ assumes "bounded_linear f" shows "(f ---> 0) (at (0))"
+proof-
+ interpret f: bounded_linear f by fact
+ have "(f ---> f 0) (at 0)"
+ using tendsto_ident_at by (rule f.tendsto)
+ thus ?thesis unfolding f.zero .
+qed
+
+lemma linear_continuous_at:
+ assumes "bounded_linear f" shows "continuous (at a) f"
+ unfolding continuous_at using assms
+ apply (rule bounded_linear.tendsto)
+ apply (rule tendsto_ident_at)
+ done
+
+lemma linear_continuous_within:
+ shows "bounded_linear f ==> continuous (at x within s) f"
+ using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto
+
+lemma linear_continuous_on:
+ shows "bounded_linear f ==> continuous_on s f"
+ using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
+
+text{* Also bilinear functions, in composition form. *}
+
+lemma bilinear_continuous_at_compose:
+ shows "continuous (at x) f \<Longrightarrow> continuous (at x) g \<Longrightarrow> bounded_bilinear h
+ ==> continuous (at x) (\<lambda>x. h (f x) (g x))"
+ unfolding continuous_at using Lim_bilinear[of f "f x" "(at x)" g "g x" h] by auto
+
+lemma bilinear_continuous_within_compose:
+ shows "continuous (at x within s) f \<Longrightarrow> continuous (at x within s) g \<Longrightarrow> bounded_bilinear h
+ ==> continuous (at x within s) (\<lambda>x. h (f x) (g x))"
+ unfolding continuous_within using Lim_bilinear[of f "f x"] by auto
+
+lemma bilinear_continuous_on_compose:
+ shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> bounded_bilinear h
+ ==> continuous_on s (\<lambda>x. h (f x) (g x))"
+ unfolding continuous_on_def
+ by (fast elim: bounded_bilinear.tendsto)
+
+text {* Preservation of compactness and connectedness under continuous function. *}
lemma compact_continuous_image:
assumes "continuous_on s f" "compact s"
@@ -3968,7 +4036,6 @@
qed
lemma connected_continuous_image:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "continuous_on s f" "connected s"
shows "connected(f ` s)"
proof-
@@ -4042,7 +4109,7 @@
thus ?thesis unfolding continuous_on_closed by auto
qed
-subsection{* A uniformly convergent limit of continuous functions is continuous. *}
+text {* A uniformly convergent limit of continuous functions is continuous. *}
lemma norm_triangle_lt:
fixes x y :: "'a::real_normed_vector"
@@ -4072,54 +4139,6 @@
thus ?thesis unfolding continuous_on_iff by auto
qed
-subsection{* Topological properties of linear functions. *}
-
-lemma linear_lim_0:
- assumes "bounded_linear f" shows "(f ---> 0) (at (0))"
-proof-
- interpret f: bounded_linear f by fact
- have "(f ---> f 0) (at 0)"
- using tendsto_ident_at by (rule f.tendsto)
- thus ?thesis unfolding f.zero .
-qed
-
-lemma linear_continuous_at:
- assumes "bounded_linear f" shows "continuous (at a) f"
- unfolding continuous_at using assms
- apply (rule bounded_linear.tendsto)
- apply (rule tendsto_ident_at)
- done
-
-lemma linear_continuous_within:
- shows "bounded_linear f ==> continuous (at x within s) f"
- using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto
-
-lemma linear_continuous_on:
- shows "bounded_linear f ==> continuous_on s f"
- using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
-
-lemma continuous_on_vec1:"continuous_on A (vec1::real\<Rightarrow>real^1)"
- by(rule linear_continuous_on[OF bounded_linear_vec1])
-
-text{* Also bilinear functions, in composition form. *}
-
-lemma bilinear_continuous_at_compose:
- shows "continuous (at x) f \<Longrightarrow> continuous (at x) g \<Longrightarrow> bounded_bilinear h
- ==> continuous (at x) (\<lambda>x. h (f x) (g x))"
- unfolding continuous_at using Lim_bilinear[of f "f x" "(at x)" g "g x" h] by auto
-
-lemma bilinear_continuous_within_compose:
- shows "continuous (at x within s) f \<Longrightarrow> continuous (at x within s) g \<Longrightarrow> bounded_bilinear h
- ==> continuous (at x within s) (\<lambda>x. h (f x) (g x))"
- unfolding continuous_within using Lim_bilinear[of f "f x"] by auto
-
-lemma bilinear_continuous_on_compose:
- fixes s :: "'a::metric_space set" (* TODO: generalize *)
- shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> bounded_bilinear h
- ==> continuous_on s (\<lambda>x. h (f x) (g x))"
- unfolding continuous_on_eq_continuous_within apply auto apply(erule_tac x=x in ballE) apply auto apply(erule_tac x=x in ballE) apply auto
- using bilinear_continuous_within_compose[of _ s f g h] by auto
-
subsection{* Topological stuff lifted from and dropped to R *}
@@ -4164,10 +4183,8 @@
lemma continuous_at_component: "continuous (at a) (\<lambda>x. x $ i)"
unfolding continuous_at by (intro tendsto_intros)
-lemma continuous_on_component:
- fixes s :: "('a::metric_space ^ 'n) set" (* TODO: generalize *)
- shows "continuous_on s (\<lambda>x. x $ i)"
-unfolding continuous_on by (intro ballI tendsto_intros)
+lemma continuous_on_component: "continuous_on s (\<lambda>x. x $ i)"
+unfolding continuous_on_def by (intro ballI tendsto_intros)
lemma continuous_at_infnorm: "continuous (at x) infnorm"
unfolding continuous_at Lim_at o_def unfolding dist_norm
@@ -4275,79 +4292,7 @@
thus ?thesis by fastsimp
qed
-subsection{* We can now extend limit compositions to consider the scalar multiplier. *}
-
-lemma Lim_mul:
- fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
- assumes "(c ---> d) net" "(f ---> l) net"
- shows "((\<lambda>x. c(x) *\<^sub>R f x) ---> (d *\<^sub>R l)) net"
- using assms by (rule scaleR.tendsto)
-
-lemma Lim_vmul:
- fixes c :: "'a \<Rightarrow> real" and v :: "'b::real_normed_vector"
- shows "(c ---> d) net ==> ((\<lambda>x. c(x) *\<^sub>R v) ---> d *\<^sub>R v) net"
- by (intro tendsto_intros)
-
-lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
-
-lemma continuous_vmul:
- fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
- shows "continuous net c ==> continuous net (\<lambda>x. c(x) *\<^sub>R v)"
- unfolding continuous_def using Lim_vmul[of c] by auto
-
-lemma continuous_mul:
- fixes c :: "'a::metric_space \<Rightarrow> real"
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
- shows "continuous net c \<Longrightarrow> continuous net f
- ==> continuous net (\<lambda>x. c(x) *\<^sub>R f x) "
- unfolding continuous_def by (intro tendsto_intros)
-
-lemmas continuous_intros = continuous_add continuous_vmul continuous_cmul continuous_const continuous_sub continuous_at_id continuous_within_id continuous_mul
-
-lemma continuous_on_vmul:
- fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
- shows "continuous_on s c ==> continuous_on s (\<lambda>x. c(x) *\<^sub>R v)"
- unfolding continuous_on_eq_continuous_within using continuous_vmul[of _ c] by auto
-
-lemma continuous_on_mul:
- fixes c :: "'a::metric_space \<Rightarrow> real"
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
- shows "continuous_on s c \<Longrightarrow> continuous_on s f
- ==> continuous_on s (\<lambda>x. c(x) *\<^sub>R f x)"
- unfolding continuous_on_eq_continuous_within using continuous_mul[of _ c] by auto
-
-lemmas continuous_on_intros = continuous_on_add continuous_on_const continuous_on_id continuous_on_compose continuous_on_cmul continuous_on_neg continuous_on_sub
- uniformly_continuous_on_add uniformly_continuous_on_const uniformly_continuous_on_id uniformly_continuous_on_compose uniformly_continuous_on_cmul uniformly_continuous_on_neg uniformly_continuous_on_sub
- continuous_on_mul continuous_on_vmul
-
-text{* And so we have continuity of inverse. *}
-
-lemma Lim_inv:
- fixes f :: "'a \<Rightarrow> real"
- assumes "(f ---> l) (net::'a net)" "l \<noteq> 0"
- shows "((inverse o f) ---> inverse l) net"
- unfolding o_def using assms by (rule tendsto_inverse)
-
-lemma continuous_inv:
- fixes f :: "'a::metric_space \<Rightarrow> real"
- shows "continuous net f \<Longrightarrow> f(netlimit net) \<noteq> 0
- ==> continuous net (inverse o f)"
- unfolding continuous_def using Lim_inv by auto
-
-lemma continuous_at_within_inv:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_field"
- assumes "continuous (at a within s) f" "f a \<noteq> 0"
- shows "continuous (at a within s) (inverse o f)"
- using assms unfolding continuous_within o_def
- by (intro tendsto_intros)
-
-lemma continuous_at_inv:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_field"
- shows "continuous (at a) f \<Longrightarrow> f a \<noteq> 0
- ==> continuous (at a) (inverse o f) "
- using within_UNIV[THEN sym, of "at a"] using continuous_at_within_inv[of a UNIV] by auto
-
-subsection{* Preservation properties for pasted sets. *}
+subsection {* Pasted sets *}
lemma bounded_pastecart:
fixes s :: "('a::real_normed_vector ^ _) set" (* FIXME: generalize to metric_space *)
@@ -4710,7 +4655,7 @@
by (auto simp add: dist_commute)
qed
-(* A cute way of denoting open and closed intervals using overloading. *)
+subsection {* Intervals *}
lemma interval: fixes a :: "'a::ord^'n" shows
"{a <..< b} = {x::'a^'n. \<forall>i. a$i < x$i \<and> x$i < b$i}" and
@@ -4722,20 +4667,6 @@
"x \<in> {a .. b} \<longleftrightarrow> (\<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i)"
using interval[of a b] by(auto simp add: expand_set_eq vector_less_def vector_le_def)
-lemma mem_interval_1: fixes x :: "real^1" shows
- "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
- "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
-by(simp_all add: Cart_eq vector_less_def vector_le_def)
-
-lemma vec1_interval:fixes a::"real" shows
- "vec1 ` {a .. b} = {vec1 a .. vec1 b}"
- "vec1 ` {a<..<b} = {vec1 a<..<vec1 b}"
- apply(rule_tac[!] set_ext) unfolding image_iff vector_less_def unfolding mem_interval
- unfolding forall_1 unfolding vec1_dest_vec1_simps
- apply rule defer apply(rule_tac x="dest_vec1 x" in bexI) prefer 3 apply rule defer
- apply(rule_tac x="dest_vec1 x" in bexI) by auto
-
-
lemma interval_eq_empty: fixes a :: "real^'n" shows
"({a <..< b} = {} \<longleftrightarrow> (\<exists>i. b$i \<le> a$i))" (is ?th1) and
"({a .. b} = {} \<longleftrightarrow> (\<exists>i. b$i < a$i))" (is ?th2)
@@ -4918,10 +4849,7 @@
qed
lemma open_interval_real[intro]: fixes a :: "real" shows "open {a<..<b}"
- using open_interval[of "vec1 a" "vec1 b"] unfolding open_contains_ball
- apply-apply(rule,erule_tac x="vec1 x" in ballE) apply(erule exE,rule_tac x=e in exI)
- unfolding subset_eq mem_ball apply(rule) defer apply(rule,erule conjE,erule_tac x="vec1 xa" in ballE)
- by(auto simp add: dist_vec1 dist_real_def vector_less_def)
+ by (rule open_real_greaterThanLessThan)
lemma closed_interval[intro]: fixes a :: "real^'n" shows "closed {a .. b}"
proof-
@@ -5112,56 +5040,6 @@
unfolding closure_open_interval[OF assms, THEN sym] unfolding open_inter_closure_eq_empty[OF open_interval] ..
-(* Some special cases for intervals in R^1. *)
-
-lemma interval_cases_1: fixes x :: "real^1" shows
- "x \<in> {a .. b} ==> x \<in> {a<..<b} \<or> (x = a) \<or> (x = b)"
- unfolding Cart_eq vector_less_def vector_le_def mem_interval by(auto simp del:dest_vec1_eq)
-
-lemma in_interval_1: fixes x :: "real^1" shows
- "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b) \<and>
- (x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
- unfolding Cart_eq vector_less_def vector_le_def mem_interval by(auto simp del:dest_vec1_eq)
-
-lemma interval_eq_empty_1: fixes a :: "real^1" shows
- "{a .. b} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a"
- "{a<..<b} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a"
- unfolding interval_eq_empty and ex_1 by auto
-
-lemma subset_interval_1: fixes a :: "real^1" shows
- "({a .. b} \<subseteq> {c .. d} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or>
- dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a \<le> dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
- "({a .. b} \<subseteq> {c<..<d} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or>
- dest_vec1 c < dest_vec1 a \<and> dest_vec1 a \<le> dest_vec1 b \<and> dest_vec1 b < dest_vec1 d)"
- "({a<..<b} \<subseteq> {c .. d} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or>
- dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a < dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
- "({a<..<b} \<subseteq> {c<..<d} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or>
- dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a < dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
- unfolding subset_interval[of a b c d] unfolding forall_1 by auto
-
-lemma eq_interval_1: fixes a :: "real^1" shows
- "{a .. b} = {c .. d} \<longleftrightarrow>
- dest_vec1 b < dest_vec1 a \<and> dest_vec1 d < dest_vec1 c \<or>
- dest_vec1 a = dest_vec1 c \<and> dest_vec1 b = dest_vec1 d"
-unfolding set_eq_subset[of "{a .. b}" "{c .. d}"]
-unfolding subset_interval_1(1)[of a b c d]
-unfolding subset_interval_1(1)[of c d a b]
-by auto
-
-lemma disjoint_interval_1: fixes a :: "real^1" shows
- "{a .. b} \<inter> {c .. d} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or> dest_vec1 d < dest_vec1 c \<or> dest_vec1 b < dest_vec1 c \<or> dest_vec1 d < dest_vec1 a"
- "{a .. b} \<inter> {c<..<d} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or> dest_vec1 d \<le> dest_vec1 c \<or> dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
- "{a<..<b} \<inter> {c .. d} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or> dest_vec1 d < dest_vec1 c \<or> dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
- "{a<..<b} \<inter> {c<..<d} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or> dest_vec1 d \<le> dest_vec1 c \<or> dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
- unfolding disjoint_interval and ex_1 by auto
-
-lemma open_closed_interval_1: fixes a :: "real^1" shows
- "{a<..<b} = {a .. b} - {a, b}"
- unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
-
-lemma closed_open_interval_1: "dest_vec1 (a::real^1) \<le> dest_vec1 b ==> {a .. b} = {a<..<b} \<union> {a,b}"
- unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
-
(* Some stuff for half-infinite intervals too; FIXME: notation? *)
lemma closed_interval_left: fixes b::"real^'n"
@@ -5188,7 +5066,7 @@
thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
qed
-subsection{* Intervals in general, including infinite and mixtures of open and closed. *}
+text {* Intervals in general, including infinite and mixtures of open and closed. *}
definition "is_interval s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i. ((a$i \<le> x$i \<and> x$i \<le> b$i) \<or> (b$i \<le> x$i \<and> x$i \<le> a$i))) \<longrightarrow> x \<in> s)"
@@ -5295,14 +5173,6 @@
shows "l$i = b"
using ev[unfolded order_eq_iff eventually_and] using Lim_component_ge[OF net, of b i] and Lim_component_le[OF net, of i b] by auto
-lemma Lim_drop_le: fixes f :: "'a \<Rightarrow> real^1" shows
- "(f ---> l) net \<Longrightarrow> ~(trivial_limit net) \<Longrightarrow> eventually (\<lambda>x. dest_vec1 (f x) \<le> b) net ==> dest_vec1 l \<le> b"
- using Lim_component_le[of f l net 1 b] by auto
-
-lemma Lim_drop_ge: fixes f :: "'a \<Rightarrow> real^1" shows
- "(f ---> l) net \<Longrightarrow> ~(trivial_limit net) \<Longrightarrow> eventually (\<lambda>x. b \<le> dest_vec1 (f x)) net ==> b \<le> dest_vec1 l"
- using Lim_component_ge[of f l net b 1] by auto
-
text{* Limits relative to a union. *}
lemma eventually_within_Un:
@@ -5317,15 +5187,19 @@
unfolding tendsto_def
by (auto simp add: eventually_within_Un)
+lemma Lim_topological:
+ "(f ---> l) net \<longleftrightarrow>
+ trivial_limit net \<or>
+ (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
+ unfolding tendsto_def trivial_limit_eq by auto
+
lemma continuous_on_union:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "closed s" "closed t" "continuous_on s f" "continuous_on t f"
shows "continuous_on (s \<union> t) f"
- using assms unfolding continuous_on unfolding Lim_within_union
- unfolding Lim unfolding trivial_limit_within unfolding closed_limpt by auto
+ using assms unfolding continuous_on Lim_within_union
+ unfolding Lim_topological trivial_limit_within closed_limpt by auto
lemma continuous_on_cases:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "closed s" "closed t" "continuous_on s f" "continuous_on t g"
"\<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x"
shows "continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
@@ -5359,23 +5233,7 @@
"connected s \<Longrightarrow> x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x$k \<le> a \<Longrightarrow> a \<le> y$k \<Longrightarrow> (\<exists>z\<in>s. z$k = a)"
using connected_ivt_hyperplane[of s x y "(basis k)::real^'n" a] by (auto simp add: inner_basis)
-text{* Also more convenient formulations of monotone convergence. *}
-
-lemma bounded_increasing_convergent: fixes s::"nat \<Rightarrow> real^1"
- assumes "bounded {s n| n::nat. True}" "\<forall>n. dest_vec1(s n) \<le> dest_vec1(s(Suc n))"
- shows "\<exists>l. (s ---> l) sequentially"
-proof-
- obtain a where a:"\<forall>n. \<bar>dest_vec1 (s n)\<bar> \<le> a" using assms(1)[unfolded bounded_iff abs_dest_vec1] by auto
- { fix m::nat
- have "\<And> n. n\<ge>m \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)"
- apply(induct_tac n) apply simp using assms(2) apply(erule_tac x="na" in allE) by(auto simp add: not_less_eq_eq) }
- hence "\<forall>m n. m \<le> n \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)" by auto
- then obtain l where "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<bar>dest_vec1 (s n) - l\<bar> < e" using convergent_bounded_monotone[OF a] unfolding monoseq_def by auto
- thus ?thesis unfolding Lim_sequentially apply(rule_tac x="vec1 l" in exI)
- unfolding dist_norm unfolding abs_dest_vec1 by auto
-qed
-
-subsection{* Basic homeomorphism definitions. *}
+subsection {* Homeomorphisms *}
definition "homeomorphism s t f g \<equiv>
(\<forall>x\<in>s. (g(f x) = x)) \<and> (f ` s = t) \<and> continuous_on s f \<and>
@@ -5431,13 +5289,7 @@
apply(erule_tac x="f x" in ballE) apply(erule_tac x="x" in ballE)
apply auto apply(rule_tac x="f x" in bexI) by auto
-subsection{* Relatively weak hypotheses if a set is compact. *}
-
-definition "inv_on f s = (\<lambda>x. SOME y. y\<in>s \<and> f y = x)"
-
-lemma assumes "inj_on f s" "x\<in>s"
- shows "inv_on f s (f x) = x"
- using assms unfolding inj_on_def inv_on_def by auto
+text {* Relatively weak hypotheses if a set is compact. *}
lemma homeomorphism_compact:
fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
@@ -5772,7 +5624,7 @@
thus ?thesis using dim_subset[OF closure_subset, of s] by auto
qed
-text{* Affine transformations of intervals. *}
+subsection {* Affine transformations of intervals *}
lemma affinity_inverses:
assumes m0: "m \<noteq> (0::'a::field)"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Multivariate_Analysis/Vec1.thy Tue Apr 27 11:17:50 2010 -0700
@@ -0,0 +1,404 @@
+(* Title: Multivariate_Analysis/Vec1.thy
+ Author: Amine Chaieb, University of Cambridge
+ Author: Robert Himmelmann, TU Muenchen
+*)
+
+header {* Vectors of size 1, 2, or 3 *}
+
+theory Vec1
+imports Topology_Euclidean_Space
+begin
+
+text{* Some common special cases.*}
+
+lemma forall_1[simp]: "(\<forall>i::1. P i) \<longleftrightarrow> P 1"
+ by (metis num1_eq_iff)
+
+lemma ex_1[simp]: "(\<exists>x::1. P x) \<longleftrightarrow> P 1"
+ by auto (metis num1_eq_iff)
+
+lemma exhaust_2:
+ fixes x :: 2 shows "x = 1 \<or> x = 2"
+proof (induct x)
+ case (of_int z)
+ then have "0 <= z" and "z < 2" by simp_all
+ then have "z = 0 | z = 1" by arith
+ then show ?case by auto
+qed
+
+lemma forall_2: "(\<forall>i::2. P i) \<longleftrightarrow> P 1 \<and> P 2"
+ by (metis exhaust_2)
+
+lemma exhaust_3:
+ fixes x :: 3 shows "x = 1 \<or> x = 2 \<or> x = 3"
+proof (induct x)
+ case (of_int z)
+ then have "0 <= z" and "z < 3" by simp_all
+ then have "z = 0 \<or> z = 1 \<or> z = 2" by arith
+ then show ?case by auto
+qed
+
+lemma forall_3: "(\<forall>i::3. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3"
+ by (metis exhaust_3)
+
+lemma UNIV_1 [simp]: "UNIV = {1::1}"
+ by (auto simp add: num1_eq_iff)
+
+lemma UNIV_2: "UNIV = {1::2, 2::2}"
+ using exhaust_2 by auto
+
+lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}"
+ using exhaust_3 by auto
+
+lemma setsum_1: "setsum f (UNIV::1 set) = f 1"
+ unfolding UNIV_1 by simp
+
+lemma setsum_2: "setsum f (UNIV::2 set) = f 1 + f 2"
+ unfolding UNIV_2 by simp
+
+lemma setsum_3: "setsum f (UNIV::3 set) = f 1 + f 2 + f 3"
+ unfolding UNIV_3 by (simp add: add_ac)
+
+instantiation num1 :: cart_one begin
+instance proof
+ show "CARD(1) = Suc 0" by auto
+qed end
+
+(* "lift" from 'a to 'a^1 and "drop" from 'a^1 to 'a -- FIXME: potential use of transfer *)
+
+abbreviation vec1:: "'a \<Rightarrow> 'a ^ 1" where "vec1 x \<equiv> vec x"
+
+abbreviation dest_vec1:: "'a ^1 \<Rightarrow> 'a"
+ where "dest_vec1 x \<equiv> (x$1)"
+
+lemma vec1_component[simp]: "(vec1 x)$1 = x"
+ by simp
+
+lemma vec1_dest_vec1: "vec1(dest_vec1 x) = x" "dest_vec1(vec1 y) = y"
+ by (simp_all add: Cart_eq)
+
+declare vec1_dest_vec1(1) [simp]
+
+lemma forall_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (vec1 x))"
+ by (metis vec1_dest_vec1(1))
+
+lemma exists_vec1: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P(vec1 x))"
+ by (metis vec1_dest_vec1(1))
+
+lemma vec1_eq[simp]: "vec1 x = vec1 y \<longleftrightarrow> x = y"
+ by (metis vec1_dest_vec1(2))
+
+lemma dest_vec1_eq[simp]: "dest_vec1 x = dest_vec1 y \<longleftrightarrow> x = y"
+ by (metis vec1_dest_vec1(1))
+
+subsection{* The collapse of the general concepts to dimension one. *}
+
+lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
+ by (simp add: Cart_eq)
+
+lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))"
+ apply auto
+ apply (erule_tac x= "x$1" in allE)
+ apply (simp only: vector_one[symmetric])
+ done
+
+lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)"
+ by (simp add: norm_vector_def)
+
+lemma norm_real: "norm(x::real ^ 1) = abs(x$1)"
+ by (simp add: norm_vector_1)
+
+lemma dist_real: "dist(x::real ^ 1) y = abs((x$1) - (y$1))"
+ by (auto simp add: norm_real dist_norm)
+
+subsection{* Explicit vector construction from lists. *}
+
+primrec from_nat :: "nat \<Rightarrow> 'a::{monoid_add,one}"
+where "from_nat 0 = 0" | "from_nat (Suc n) = 1 + from_nat n"
+
+lemma from_nat [simp]: "from_nat = of_nat"
+by (rule ext, induct_tac x, simp_all)
+
+primrec
+ list_fun :: "nat \<Rightarrow> _ list \<Rightarrow> _ \<Rightarrow> _"
+where
+ "list_fun n [] = (\<lambda>x. 0)"
+| "list_fun n (x # xs) = fun_upd (list_fun (Suc n) xs) (from_nat n) x"
+
+definition "vector l = (\<chi> i. list_fun 1 l i)"
+(*definition "vector l = (\<chi> i. if i <= length l then l ! (i - 1) else 0)"*)
+
+lemma vector_1: "(vector[x]) $1 = x"
+ unfolding vector_def by simp
+
+lemma vector_2:
+ "(vector[x,y]) $1 = x"
+ "(vector[x,y] :: 'a^2)$2 = (y::'a::zero)"
+ unfolding vector_def by simp_all
+
+lemma vector_3:
+ "(vector [x,y,z] ::('a::zero)^3)$1 = x"
+ "(vector [x,y,z] ::('a::zero)^3)$2 = y"
+ "(vector [x,y,z] ::('a::zero)^3)$3 = z"
+ unfolding vector_def by simp_all
+
+lemma forall_vector_1: "(\<forall>v::'a::zero^1. P v) \<longleftrightarrow> (\<forall>x. P(vector[x]))"
+ apply auto
+ apply (erule_tac x="v$1" in allE)
+ apply (subgoal_tac "vector [v$1] = v")
+ apply simp
+ apply (vector vector_def)
+ apply simp
+ done
+
+lemma forall_vector_2: "(\<forall>v::'a::zero^2. P v) \<longleftrightarrow> (\<forall>x y. P(vector[x, y]))"
+ apply auto
+ apply (erule_tac x="v$1" in allE)
+ apply (erule_tac x="v$2" in allE)
+ apply (subgoal_tac "vector [v$1, v$2] = v")
+ apply simp
+ apply (vector vector_def)
+ apply (simp add: forall_2)
+ done
+
+lemma forall_vector_3: "(\<forall>v::'a::zero^3. P v) \<longleftrightarrow> (\<forall>x y z. P(vector[x, y, z]))"
+ apply auto
+ apply (erule_tac x="v$1" in allE)
+ apply (erule_tac x="v$2" in allE)
+ apply (erule_tac x="v$3" in allE)
+ apply (subgoal_tac "vector [v$1, v$2, v$3] = v")
+ apply simp
+ apply (vector vector_def)
+ apply (simp add: forall_3)
+ done
+
+lemma range_vec1[simp]:"range vec1 = UNIV" apply(rule set_ext,rule) unfolding image_iff defer
+ apply(rule_tac x="dest_vec1 x" in bexI) by auto
+
+lemma dest_vec1_lambda: "dest_vec1(\<chi> i. x i) = x 1"
+ by (simp)
+
+lemma dest_vec1_vec: "dest_vec1(vec x) = x"
+ by (simp)
+
+lemma dest_vec1_sum: assumes fS: "finite S"
+ shows "dest_vec1(setsum f S) = setsum (dest_vec1 o f) S"
+ apply (induct rule: finite_induct[OF fS])
+ apply simp
+ apply auto
+ done
+
+lemma norm_vec1 [simp]: "norm(vec1 x) = abs(x)"
+ by (simp add: vec_def norm_real)
+
+lemma dist_vec1: "dist(vec1 x) (vec1 y) = abs(x - y)"
+ by (simp only: dist_real vec1_component)
+lemma abs_dest_vec1: "norm x = \<bar>dest_vec1 x\<bar>"
+ by (metis vec1_dest_vec1(1) norm_vec1)
+
+lemmas vec1_dest_vec1_simps = forall_vec1 vec_add[THEN sym] dist_vec1 vec_sub[THEN sym] vec1_dest_vec1 norm_vec1 vector_smult_component
+ vec1_eq vec_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def norm_vec1 real_norm_def
+
+lemma bounded_linear_vec1:"bounded_linear (vec1::real\<Rightarrow>real^1)"
+ unfolding bounded_linear_def additive_def bounded_linear_axioms_def
+ unfolding smult_conv_scaleR[THEN sym] unfolding vec1_dest_vec1_simps
+ apply(rule conjI) defer apply(rule conjI) defer apply(rule_tac x=1 in exI) by auto
+
+lemma linear_vmul_dest_vec1:
+ fixes f:: "'a::semiring_1^_ \<Rightarrow> 'a^1"
+ shows "linear f \<Longrightarrow> linear (\<lambda>x. dest_vec1(f x) *s v)"
+ apply (rule linear_vmul_component)
+ by auto
+
+lemma linear_from_scalars:
+ assumes lf: "linear (f::'a::comm_ring_1 ^1 \<Rightarrow> 'a^_)"
+ shows "f = (\<lambda>x. dest_vec1 x *s column 1 (matrix f))"
+ apply (rule ext)
+ apply (subst matrix_works[OF lf, symmetric])
+ apply (auto simp add: Cart_eq matrix_vector_mult_def column_def mult_commute)
+ done
+
+lemma linear_to_scalars: assumes lf: "linear (f::real ^'n \<Rightarrow> real^1)"
+ shows "f = (\<lambda>x. vec1(row 1 (matrix f) \<bullet> x))"
+ apply (rule ext)
+ apply (subst matrix_works[OF lf, symmetric])
+ apply (simp add: Cart_eq matrix_vector_mult_def row_def inner_vector_def mult_commute)
+ done
+
+lemma dest_vec1_eq_0: "dest_vec1 x = 0 \<longleftrightarrow> x = 0"
+ by (simp add: dest_vec1_eq[symmetric])
+
+lemma setsum_scalars: assumes fS: "finite S"
+ shows "setsum f S = vec1 (setsum (dest_vec1 o f) S)"
+ unfolding vec_setsum[OF fS] by simp
+
+lemma dest_vec1_wlog_le: "(\<And>(x::'a::linorder ^ 1) y. P x y \<longleftrightarrow> P y x) \<Longrightarrow> (\<And>x y. dest_vec1 x <= dest_vec1 y ==> P x y) \<Longrightarrow> P x y"
+ apply (cases "dest_vec1 x \<le> dest_vec1 y")
+ apply simp
+ apply (subgoal_tac "dest_vec1 y \<le> dest_vec1 x")
+ apply (auto)
+ done
+
+text{* Lifting and dropping *}
+
+lemma continuous_on_o_dest_vec1: fixes f::"real \<Rightarrow> 'a::real_normed_vector"
+ assumes "continuous_on {a..b::real} f" shows "continuous_on {vec1 a..vec1 b} (f o dest_vec1)"
+ using assms unfolding continuous_on_iff apply safe
+ apply(erule_tac x="x$1" in ballE,erule_tac x=e in allE) apply safe
+ apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real
+ apply(erule_tac x="dest_vec1 x'" in ballE) by(auto simp add:vector_le_def)
+
+lemma continuous_on_o_vec1: fixes f::"real^1 \<Rightarrow> 'a::real_normed_vector"
+ assumes "continuous_on {a..b} f" shows "continuous_on {dest_vec1 a..dest_vec1 b} (f o vec1)"
+ using assms unfolding continuous_on_iff apply safe
+ apply(erule_tac x="vec x" in ballE,erule_tac x=e in allE) apply safe
+ apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real
+ apply(erule_tac x="vec1 x'" in ballE) by(auto simp add:vector_le_def)
+
+lemma continuous_on_vec1:"continuous_on A (vec1::real\<Rightarrow>real^1)"
+ by(rule linear_continuous_on[OF bounded_linear_vec1])
+
+lemma mem_interval_1: fixes x :: "real^1" shows
+ "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
+ "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
+by(simp_all add: Cart_eq vector_less_def vector_le_def)
+
+lemma vec1_interval:fixes a::"real" shows
+ "vec1 ` {a .. b} = {vec1 a .. vec1 b}"
+ "vec1 ` {a<..<b} = {vec1 a<..<vec1 b}"
+ apply(rule_tac[!] set_ext) unfolding image_iff vector_less_def unfolding mem_interval
+ unfolding forall_1 unfolding vec1_dest_vec1_simps
+ apply rule defer apply(rule_tac x="dest_vec1 x" in bexI) prefer 3 apply rule defer
+ apply(rule_tac x="dest_vec1 x" in bexI) by auto
+
+(* Some special cases for intervals in R^1. *)
+
+lemma interval_cases_1: fixes x :: "real^1" shows
+ "x \<in> {a .. b} ==> x \<in> {a<..<b} \<or> (x = a) \<or> (x = b)"
+ unfolding Cart_eq vector_less_def vector_le_def mem_interval by(auto simp del:dest_vec1_eq)
+
+lemma in_interval_1: fixes x :: "real^1" shows
+ "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b) \<and>
+ (x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
+ unfolding Cart_eq vector_less_def vector_le_def mem_interval by(auto simp del:dest_vec1_eq)
+
+lemma interval_eq_empty_1: fixes a :: "real^1" shows
+ "{a .. b} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a"
+ "{a<..<b} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a"
+ unfolding interval_eq_empty and ex_1 by auto
+
+lemma subset_interval_1: fixes a :: "real^1" shows
+ "({a .. b} \<subseteq> {c .. d} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or>
+ dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a \<le> dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
+ "({a .. b} \<subseteq> {c<..<d} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or>
+ dest_vec1 c < dest_vec1 a \<and> dest_vec1 a \<le> dest_vec1 b \<and> dest_vec1 b < dest_vec1 d)"
+ "({a<..<b} \<subseteq> {c .. d} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or>
+ dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a < dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
+ "({a<..<b} \<subseteq> {c<..<d} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or>
+ dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a < dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
+ unfolding subset_interval[of a b c d] unfolding forall_1 by auto
+
+lemma eq_interval_1: fixes a :: "real^1" shows
+ "{a .. b} = {c .. d} \<longleftrightarrow>
+ dest_vec1 b < dest_vec1 a \<and> dest_vec1 d < dest_vec1 c \<or>
+ dest_vec1 a = dest_vec1 c \<and> dest_vec1 b = dest_vec1 d"
+unfolding set_eq_subset[of "{a .. b}" "{c .. d}"]
+unfolding subset_interval_1(1)[of a b c d]
+unfolding subset_interval_1(1)[of c d a b]
+by auto
+
+lemma disjoint_interval_1: fixes a :: "real^1" shows
+ "{a .. b} \<inter> {c .. d} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or> dest_vec1 d < dest_vec1 c \<or> dest_vec1 b < dest_vec1 c \<or> dest_vec1 d < dest_vec1 a"
+ "{a .. b} \<inter> {c<..<d} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or> dest_vec1 d \<le> dest_vec1 c \<or> dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
+ "{a<..<b} \<inter> {c .. d} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or> dest_vec1 d < dest_vec1 c \<or> dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
+ "{a<..<b} \<inter> {c<..<d} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or> dest_vec1 d \<le> dest_vec1 c \<or> dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
+ unfolding disjoint_interval and ex_1 by auto
+
+lemma open_closed_interval_1: fixes a :: "real^1" shows
+ "{a<..<b} = {a .. b} - {a, b}"
+ unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
+
+lemma closed_open_interval_1: "dest_vec1 (a::real^1) \<le> dest_vec1 b ==> {a .. b} = {a<..<b} \<union> {a,b}"
+ unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
+
+lemma Lim_drop_le: fixes f :: "'a \<Rightarrow> real^1" shows
+ "(f ---> l) net \<Longrightarrow> ~(trivial_limit net) \<Longrightarrow> eventually (\<lambda>x. dest_vec1 (f x) \<le> b) net ==> dest_vec1 l \<le> b"
+ using Lim_component_le[of f l net 1 b] by auto
+
+lemma Lim_drop_ge: fixes f :: "'a \<Rightarrow> real^1" shows
+ "(f ---> l) net \<Longrightarrow> ~(trivial_limit net) \<Longrightarrow> eventually (\<lambda>x. b \<le> dest_vec1 (f x)) net ==> b \<le> dest_vec1 l"
+ using Lim_component_ge[of f l net b 1] by auto
+
+text{* Also more convenient formulations of monotone convergence. *}
+
+lemma bounded_increasing_convergent: fixes s::"nat \<Rightarrow> real^1"
+ assumes "bounded {s n| n::nat. True}" "\<forall>n. dest_vec1(s n) \<le> dest_vec1(s(Suc n))"
+ shows "\<exists>l. (s ---> l) sequentially"
+proof-
+ obtain a where a:"\<forall>n. \<bar>dest_vec1 (s n)\<bar> \<le> a" using assms(1)[unfolded bounded_iff abs_dest_vec1] by auto
+ { fix m::nat
+ have "\<And> n. n\<ge>m \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)"
+ apply(induct_tac n) apply simp using assms(2) apply(erule_tac x="na" in allE) by(auto simp add: not_less_eq_eq) }
+ hence "\<forall>m n. m \<le> n \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)" by auto
+ then obtain l where "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<bar>dest_vec1 (s n) - l\<bar> < e" using convergent_bounded_monotone[OF a] unfolding monoseq_def by auto
+ thus ?thesis unfolding Lim_sequentially apply(rule_tac x="vec1 l" in exI)
+ unfolding dist_norm unfolding abs_dest_vec1 by auto
+qed
+
+lemma dest_vec1_simps[simp]: fixes a::"real^1"
+ shows "a$1 = 0 \<longleftrightarrow> a = 0" (*"a \<le> 1 \<longleftrightarrow> dest_vec1 a \<le> 1" "0 \<le> a \<longleftrightarrow> 0 \<le> dest_vec1 a"*)
+ "a \<le> b \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 b" "dest_vec1 (1::real^1) = 1"
+ by(auto simp add: vector_le_def Cart_eq)
+
+lemma dest_vec1_inverval:
+ "dest_vec1 ` {a .. b} = {dest_vec1 a .. dest_vec1 b}"
+ "dest_vec1 ` {a<.. b} = {dest_vec1 a<.. dest_vec1 b}"
+ "dest_vec1 ` {a ..<b} = {dest_vec1 a ..<dest_vec1 b}"
+ "dest_vec1 ` {a<..<b} = {dest_vec1 a<..<dest_vec1 b}"
+ apply(rule_tac [!] equalityI)
+ unfolding subset_eq Ball_def Bex_def mem_interval_1 image_iff
+ apply(rule_tac [!] allI)apply(rule_tac [!] impI)
+ apply(rule_tac[2] x="vec1 x" in exI)apply(rule_tac[4] x="vec1 x" in exI)
+ apply(rule_tac[6] x="vec1 x" in exI)apply(rule_tac[8] x="vec1 x" in exI)
+ by (auto simp add: vector_less_def vector_le_def)
+
+lemma dest_vec1_setsum: assumes "finite S"
+ shows " dest_vec1 (setsum f S) = setsum (\<lambda>x. dest_vec1 (f x)) S"
+ using dest_vec1_sum[OF assms] by auto
+
+lemma open_dest_vec1_vimage: "open S \<Longrightarrow> open (dest_vec1 -` S)"
+unfolding open_vector_def forall_1 by auto
+
+lemma tendsto_dest_vec1 [tendsto_intros]:
+ "(f ---> l) net \<Longrightarrow> ((\<lambda>x. dest_vec1 (f x)) ---> dest_vec1 l) net"
+by(rule tendsto_Cart_nth)
+
+lemma continuous_dest_vec1: "continuous net f \<Longrightarrow> continuous net (\<lambda>x. dest_vec1 (f x))"
+ unfolding continuous_def by (rule tendsto_dest_vec1)
+
+lemma forall_dest_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P(dest_vec1 x))"
+ apply safe defer apply(erule_tac x="vec1 x" in allE) by auto
+
+lemma forall_of_dest_vec1: "(\<forall>v. P (\<lambda>x. dest_vec1 (v x))) \<longleftrightarrow> (\<forall>x. P x)"
+ apply rule apply rule apply(erule_tac x="(vec1 \<circ> x)" in allE) unfolding o_def vec1_dest_vec1 by auto
+
+lemma forall_of_dest_vec1': "(\<forall>v. P (dest_vec1 v)) \<longleftrightarrow> (\<forall>x. P x)"
+ apply rule apply rule apply(erule_tac x="(vec1 x)" in allE) defer apply rule
+ apply(erule_tac x="dest_vec1 v" in allE) unfolding o_def vec1_dest_vec1 by auto
+
+lemma dist_vec1_0[simp]: "dist(vec1 (x::real)) 0 = norm x" unfolding vector_dist_norm by auto
+
+lemma bounded_linear_vec1_dest_vec1: fixes f::"real \<Rightarrow> real"
+ shows "linear (vec1 \<circ> f \<circ> dest_vec1) = bounded_linear f" (is "?l = ?r") proof-
+ { assume ?l guess K using linear_bounded[OF `?l`] ..
+ hence "\<exists>K. \<forall>x. \<bar>f x\<bar> \<le> \<bar>x\<bar> * K" apply(rule_tac x=K in exI)
+ unfolding vec1_dest_vec1_simps by (auto simp add:field_simps) }
+ thus ?thesis unfolding linear_def bounded_linear_def additive_def bounded_linear_axioms_def o_def
+ unfolding vec1_dest_vec1_simps by auto qed
+
+lemma vec1_le[simp]:fixes a::real shows "vec1 a \<le> vec1 b \<longleftrightarrow> a \<le> b"
+ unfolding vector_le_def by auto
+lemma vec1_less[simp]:fixes a::real shows "vec1 a < vec1 b \<longleftrightarrow> a < b"
+ unfolding vector_less_def by auto
+
+end