# HG changeset patch # User huffman # Date 1272216183 25200 # Node ID 2623a1987e1d92deafeb5c3c11f60696a03d6734 # Parent 46328f9ddf3aea9c8bdd182408c834a0b435f55a generalize more constants and lemmas diff -r 46328f9ddf3a -r 2623a1987e1d src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sun Apr 25 09:01:03 2010 -0700 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sun Apr 25 10:23:03 2010 -0700 @@ -2609,11 +2609,11 @@ "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)" definition - open_segment :: "real ^ 'n \ real ^ 'n \ (real ^ 'n) set" where + open_segment :: "'a::real_vector \ 'a \ 'a set" where "open_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 < u \ u < 1}" definition - closed_segment :: "real ^ 'n \ real ^ 'n \ (real ^ 'n) set" where + closed_segment :: "'a::real_vector \ 'a \ 'a set" where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \ u \ u \ 1}" definition "between = (\ (a,b). closed_segment a b)" @@ -2684,12 +2684,14 @@ unfolding segment_convex_hull apply(rule_tac[!] hull_subset[unfolded subset_eq, rule_format]) by auto lemma segment_furthest_le: + fixes a b x y :: "real ^ 'n" assumes "x \ closed_segment a b" shows "norm(y - x) \ norm(y - a) \ norm(y - x) \ norm(y - b)" proof- obtain z where "z\{a, b}" "norm (x - y) \ norm (z - y)" using simplex_furthest_le[of "{a, b}" y] using assms[unfolded segment_convex_hull] by auto thus ?thesis by(auto simp add:norm_minus_commute) qed lemma segment_bound: + fixes x a b :: "real ^ 'n" assumes "x \ closed_segment a b" shows "norm(x - a) \ norm(b - a)" "norm(x - b) \ norm(b - a)" using segment_furthest_le[OF assms, of a] @@ -2871,24 +2873,42 @@ subsection {* Paths. *} -definition "path (g::real \ real^'n) \ continuous_on {0 .. 1} g" - -definition "pathstart (g::real \ real^'n) = g 0" - -definition "pathfinish (g::real \ real^'n) = g 1" - -definition "path_image (g::real \ real^'n) = g ` {0 .. 1}" - -definition "reversepath (g::real \ real^'n) = (\x. g(1 - x))" - -definition joinpaths:: "(real \ real^'n) \ (real \ real^'n) \ (real \ real^'n)" (infixr "+++" 75) - where "joinpaths g1 g2 = (\x. if x \ ((1 / 2)::real) then g1 (2 * x) else g2(2 * x - 1))" - -definition "simple_path (g::real \ real^'n) \ +text {* TODO: Once @{const continuous_on} is generalized to arbitrary +topological spaces, all of these concepts should be similarly generalized. *} + +definition + path :: "(real \ 'a::metric_space) \ bool" + where "path g \ continuous_on {0 .. 1} g" + +definition + pathstart :: "(real \ 'a::metric_space) \ 'a" + where "pathstart g = g 0" + +definition + pathfinish :: "(real \ 'a::metric_space) \ 'a" + where "pathfinish g = g 1" + +definition + path_image :: "(real \ 'a::metric_space) \ 'a set" + where "path_image g = g ` {0 .. 1}" + +definition + reversepath :: "(real \ 'a::metric_space) \ (real \ 'a)" + where "reversepath g = (\x. g(1 - x))" + +definition + joinpaths :: "(real \ 'a::metric_space) \ (real \ 'a) \ (real \ 'a)" + (infixr "+++" 75) + where "g1 +++ g2 = (\x. if x \ 1/2 then g1 (2 * x) else g2 (2 * x - 1))" + +definition + simple_path :: "(real \ 'a::metric_space) \ bool" + where "simple_path g \ (\x\{0..1}. \y\{0..1}. g x = g y \ x = y \ x = 0 \ y = 1 \ x = 1 \ y = 0)" -definition "injective_path (g::real \ real^'n) \ - (\x\{0..1}. \y\{0..1}. g x = g y \ x = y)" +definition + injective_path :: "(real \ 'a::metric_space) \ bool" + where "injective_path g \ (\x\{0..1}. \y\{0..1}. g x = g y \ x = y)" subsection {* Some lemmas about these concepts. *} @@ -2900,20 +2920,19 @@ unfolding path_image_def image_is_empty interval_eq_empty by auto lemma pathstart_in_path_image[intro]: "(pathstart g) \ path_image g" - unfolding pathstart_def path_image_def apply(rule imageI) - unfolding mem_interval_1 vec_1[THEN sym] dest_vec1_vec by auto + unfolding pathstart_def path_image_def by auto lemma pathfinish_in_path_image[intro]: "(pathfinish g) \ path_image g" - unfolding pathfinish_def path_image_def apply(rule imageI) - unfolding mem_interval_1 vec_1[THEN sym] dest_vec1_vec by auto + unfolding pathfinish_def path_image_def by auto lemma connected_path_image[intro]: "path g \ connected(path_image g)" - unfolding path_def path_image_def apply(rule connected_continuous_image, assumption) + unfolding path_def path_image_def + apply (erule connected_continuous_image) by(rule convex_connected, rule convex_real_interval) lemma compact_path_image[intro]: "path g \ compact(path_image g)" - unfolding path_def path_image_def apply(rule compact_continuous_image, assumption) - by(rule compact_real_interval) + unfolding path_def path_image_def + by (erule compact_continuous_image, rule compact_real_interval) lemma reversepath_reversepath[simp]: "reversepath(reversepath g) = g" unfolding reversepath_def by auto @@ -2941,7 +2960,7 @@ apply(rule continuous_on_compose[unfolded o_def, of _ "\x. 1 - x"]) apply(rule continuous_on_sub, rule continuous_on_const, rule continuous_on_id) apply(rule continuous_on_subset[of "{0..1}"], assumption) by auto - show ?thesis using *[of g] *[of "reversepath g"] unfolding reversepath_reversepath by auto qed + show ?thesis using *[of "reversepath g"] *[of g] unfolding reversepath_reversepath by (rule iffI) qed lemmas reversepath_simps = path_reversepath path_image_reversepath pathstart_reversepath pathfinish_reversepath @@ -3005,7 +3024,7 @@ fix x assume "x \ path_image g1" then obtain y where y:"y\{0..1}" "x = g1 y" unfolding path_image_def image_iff by auto thus "x \ path_image (g1 +++ g2)" unfolding joinpaths_def path_image_def image_iff - apply(rule_tac x="(1/2) *\<^sub>R y" in bexI) by(auto simp add: vector_component_simps) next + apply(rule_tac x="(1/2) *\<^sub>R y" in bexI) by auto next fix x assume "x \ path_image g2" then obtain y where y:"y\{0..1}" "x = g2 y" unfolding path_image_def image_iff by auto then show "x \ path_image (g1 +++ g2)" unfolding joinpaths_def path_image_def image_iff @@ -3019,7 +3038,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 simp add:vector_component_simps) + unfolding mem_interval_1 by auto (** move this **) declare vector_scaleR_component[simp] @@ -3035,37 +3054,37 @@ assume as:"x \ 1 / 2" "y \ 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 \ {0..1}" "2 *\<^sub>R y \ {0..1}" using xy(1,2) as - unfolding mem_interval_1 by(auto simp add:vector_component_simps) + unfolding mem_interval_1 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 \ {0..1}" "2 *\<^sub>R y - 1 \ {0..1}" using xy(1,2) as unfolding mem_interval_1 by(auto simp add:vector_component_simps) + moreover have "2 *\<^sub>R x - 1 \ {0..1}" "2 *\<^sub>R y - 1 \ {0..1}" using xy(1,2) as unfolding mem_interval_1 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 \ 1 / 2" "y > 1 / 2" hence "?g x \ path_image g1" "?g y \ path_image g2" unfolding path_image_def joinpaths_def - using xy(1,2)[unfolded mem_interval_1] by(auto simp add:vector_component_simps intro!: imageI) + using xy(1,2)[unfolded mem_interval_1] by auto moreover have "?g y \ 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] - by(auto simp add:vector_component_simps field_simps Cart_eq) + 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] - using inj(1)[of "2 *\<^sub>R x" 0] by(auto simp add:vector_component_simps) + 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] - using inj(2)[of "2 *\<^sub>R y - 1" 1] by (auto simp add:vector_component_simps Cart_eq) - ultimately show ?thesis by auto + using inj(2)[of "2 *\<^sub>R y - 1" 1] by auto + ultimately show ?thesis by auto next assume as:"x > 1 / 2" "y \ 1 / 2" hence "?g x \ path_image g2" "?g y \ path_image g1" unfolding path_image_def joinpaths_def - using xy(1,2)[unfolded mem_interval_1] by(auto simp add:vector_component_simps intro!: imageI) + using xy(1,2)[unfolded mem_interval_1] by auto moreover have "?g x \ 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] - by(auto simp add:vector_component_simps field_simps Cart_eq) + 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] - using inj(1)[of "2 *\<^sub>R y" 0] by(auto simp add:vector_component_simps) + 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] - using inj(2)[of "2 *\<^sub>R x - 1" 1] by(auto simp add:vector_component_simps Cart_eq) + using inj(2)[of "2 *\<^sub>R x - 1" 1] by auto ultimately show ?thesis by auto qed qed lemma injective_path_join: @@ -3074,45 +3093,41 @@ shows "injective_path(g1 +++ g2)" unfolding injective_path_def proof(rule,rule,rule) let ?g = "g1 +++ g2" note inj = assms(1,2)[unfolded injective_path_def, rule_format] - have *:"\x y::real. 2 *\<^sub>R x = 1 \ 2 *\<^sub>R y = 1 \ x = y" by auto fix x y assume xy:"x \ {0..1}" "y \ {0..1}" "(g1 +++ g2) x = (g1 +++ g2) y" show "x = y" proof(cases "x \ 1/2", case_tac[!] "y \ 1/2", unfold not_le) assume "x \ 1 / 2" "y \ 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 simp add:vector_component_simps) + unfolding mem_interval_1 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 simp add:vector_component_simps) + unfolding mem_interval_1 joinpaths_def by auto next assume as:"x \ 1 / 2" "y > 1 / 2" hence "?g x \ path_image g1" "?g y \ path_image g2" unfolding path_image_def joinpaths_def - using xy(1,2)[unfolded mem_interval_1] by(auto simp add:vector_component_simps intro!: imageI) + using xy(1,2)[unfolded mem_interval_1] 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 - by(auto simp add:vector_component_simps intro:*) + by auto next assume as:"x > 1 / 2" "y \ 1 / 2" hence "?g x \ path_image g2" "?g y \ path_image g1" unfolding path_image_def joinpaths_def - using xy(1,2)[unfolded mem_interval_1] by(auto simp add:vector_component_simps intro!: imageI) + using xy(1,2)[unfolded mem_interval_1] 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 - by(auto simp add:vector_component_simps intro:*) qed qed + 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 \ real^'n) = +definition "shiftpath a (f::real \ 'a::metric_space) = (\x. if (a + x) \ 1 then f(a + x) else f(a + x - 1))" lemma pathstart_shiftpath: "a \ 1 \ pathstart(shiftpath a g) = g a" unfolding pathstart_def shiftpath_def by auto -(** move this **) -declare forall_1[simp] ex_1[simp] - lemma pathfinish_shiftpath: assumes "0 \ a" "pathfinish g = pathstart g" shows "pathfinish(shiftpath a g) = g a" using assms unfolding pathstart_def pathfinish_def shiftpath_def - by(auto simp add: vector_component_simps) + by auto lemma endpoints_shiftpath: assumes "pathfinish g = pathstart g" "a \ {0 .. 1}" @@ -3127,7 +3142,7 @@ lemma path_shiftpath: assumes "path g" "pathfinish g = pathstart g" "a \ {0..1}" shows "path(shiftpath a g)" proof- - have *:"{0 .. 1} = {0 .. 1-a} \ {1-a .. 1}" using assms(3) by(auto simp add: vector_component_simps) + have *:"{0 .. 1} = {0 .. 1-a} \ {1-a .. 1}" using assms(3) by auto have **:"\x. x + a = 1 \ g (x + a - 1) = g (x + a)" using assms(2)[unfolded pathfinish_def pathstart_def] by auto show ?thesis unfolding path_def shiftpath_def * apply(rule continuous_on_union) @@ -3157,7 +3172,7 @@ subsection {* Special case of straight-line paths. *} definition - linepath :: "real ^ 'n \ real ^ 'n \ real \ real ^ 'n" where + linepath :: "'a::real_normed_vector \ 'a \ real \ 'a" where "linepath a b = (\x. (1 - x) *\<^sub>R a + x *\<^sub>R b)" lemma pathstart_linepath[simp]: "pathstart(linepath a b) = a" @@ -3184,25 +3199,31 @@ lemma reversepath_linepath[simp]: "reversepath(linepath a b) = linepath b a" unfolding reversepath_def linepath_def by(rule ext, auto) -lemma injective_path_linepath: assumes "a \ b" shows "injective_path(linepath a b)" proof- - { obtain i where i:"a$i \ b$i" using assms[unfolded Cart_eq] by auto - fix x y::"real" assume "x *\<^sub>R b + y *\<^sub>R a = x *\<^sub>R a + y *\<^sub>R b" - hence "x * (b$i - a$i) = y * (b$i - a$i)" unfolding Cart_eq by(auto simp add:field_simps) - hence "x = y" unfolding mult_cancel_right Cart_eq using i(1) by(auto simp add:field_simps) } +lemma injective_path_linepath: + assumes "a \ b" shows "injective_path(linepath a b)" +proof - + { fix x y :: "real" + assume "x *\<^sub>R b + y *\<^sub>R a = x *\<^sub>R a + y *\<^sub>R b" + hence "(x - y) *\<^sub>R a = (x - y) *\<^sub>R b" by (simp add: algebra_simps) + with assms have "x = y" by simp } thus ?thesis unfolding injective_path_def linepath_def by(auto simp add: algebra_simps) qed lemma simple_path_linepath[intro]: "a \ b \ simple_path(linepath a b)" by(auto intro!: injective_imp_simple_path injective_path_linepath) subsection {* Bounding a point away from a path. *} -lemma not_on_path_ball: assumes "path g" "z \ path_image g" +lemma not_on_path_ball: + fixes g :: "real \ 'a::heine_borel" + assumes "path g" "z \ path_image g" shows "\e>0. ball z e \ (path_image g) = {}" proof- obtain a where "a\path_image g" "\y\path_image g. dist z a \ dist z y" using distance_attains_inf[OF _ path_image_nonempty, of g z] using compact_path_image[THEN compact_imp_closed, OF assms(1)] by auto thus ?thesis apply(rule_tac x="dist z a" in exI) using assms(2) by(auto intro!: dist_pos_lt) qed -lemma not_on_path_cball: assumes "path g" "z \ path_image g" +lemma not_on_path_cball: + fixes g :: "real \ 'a::heine_borel" + assumes "path g" "z \ path_image g" shows "\e>0. cball z e \ (path_image g) = {}" proof- obtain e where "ball z e \ path_image g = {}" "e>0" using not_on_path_ball[OF assms] by auto moreover have "cball z (e/2) \ ball z e" using `e>0` by auto @@ -3219,14 +3240,14 @@ lemma path_component_refl: assumes "x \ s" shows "path_component s x x" unfolding path_defs apply(rule_tac x="\u. x" in exI) using assms - by(auto intro!:continuous_on_intros) + by(auto intro!:continuous_on_intros) lemma path_component_refl_eq: "path_component s x x \ x \ s" - by(auto intro!: path_component_mem path_component_refl) + by(auto intro!: path_component_mem path_component_refl) lemma path_component_sym: "path_component s x y \ path_component s y x" - using assms unfolding path_component_def apply(erule exE) apply(rule_tac x="reversepath g" in exI) - by(auto simp add: reversepath_simps) + using assms unfolding path_component_def apply(erule exE) apply(rule_tac x="reversepath g" in exI) + by auto lemma path_component_trans: assumes "path_component s x y" "path_component s y z" shows "path_component s x z" using assms unfolding path_component_def apply- apply(erule exE)+ apply(rule_tac x="g +++ ga" in exI) by(auto simp add: path_image_join) @@ -3261,7 +3282,9 @@ subsection {* Some useful lemmas about path-connectedness. *} -lemma convex_imp_path_connected: assumes "convex s" shows "path_connected s" +lemma convex_imp_path_connected: + fixes s :: "'a::real_normed_vector set" + assumes "convex s" shows "path_connected s" unfolding path_connected_def apply(rule,rule,rule_tac x="linepath x y" in exI) unfolding path_image_linepath using assms[unfolded convex_contains_segment] by auto @@ -3280,7 +3303,9 @@ using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(1)] using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(2)] by auto qed -lemma open_path_component: assumes "open s" shows "open(path_component s x)" +lemma open_path_component: + fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*) + assumes "open s" shows "open(path_component s x)" unfolding open_contains_ball proof fix y assume as:"y \ path_component s x" hence "y\s" apply- apply(rule path_component_mem(2)) unfolding mem_def by auto @@ -3290,7 +3315,10 @@ apply(rule path_component_of_subset[OF e(2)]) apply(rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format]) using `e>0` using as[unfolded mem_def] by auto qed qed -lemma open_non_path_component: assumes "open s" shows "open(s - path_component s x)" unfolding open_contains_ball proof +lemma open_non_path_component: + fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*) + assumes "open s" shows "open(s - path_component s x)" + unfolding open_contains_ball proof fix y assume as:"y\s - path_component s x" then obtain e where e:"e>0" "ball y e \ s" using assms[unfolded open_contains_ball] by auto show "\e>0. ball y e \ s - path_component s x" apply(rule_tac x=e in exI) apply(rule,rule `e>0`,rule,rule) defer proof(rule ccontr) @@ -3300,7 +3328,9 @@ apply(rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format]) by auto thus False using as by auto qed(insert e(2), auto) qed -lemma connected_open_path_connected: assumes "open s" "connected s" shows "path_connected s" +lemma connected_open_path_connected: + fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*) + assumes "open s" "connected s" shows "path_connected s" unfolding path_connected_component_set proof(rule,rule,rule path_component_subset, rule) fix x y assume "x \ s" "y \ s" show "y \ path_component s x" proof(rule ccontr) assume "y \ path_component s x" moreover @@ -3329,8 +3359,10 @@ unfolding path_connected_def by auto lemma path_connected_singleton: "path_connected {a}" - unfolding path_connected_def apply(rule,rule) - apply(rule_tac x="linepath a a" in exI) by(auto simp add:segment scaleR_left_diff_distrib) + unfolding path_connected_def pathstart_def pathfinish_def path_image_def + apply (clarify, rule_tac x="\x. a" in exI, simp add: image_constant_conv) + apply (simp add: path_def continuous_on_const) + done lemma path_connected_Un: assumes "path_connected s" "path_connected t" "s \ t \ {}" shows "path_connected (s \ t)" unfolding path_connected_component proof(rule,rule)