# HG changeset patch # User huffman # Date 1244939516 25200 # Node ID 84912dff2d746d64a57c15e0bde315cefc30927a # Parent 937dea81dde0d3e70cbe26f43f2e7b328a101d36 generalize many constants and lemmas from Convex_Euclidean_Space diff -r 937dea81dde0 -r 84912dff2d74 src/HOL/Library/Convex_Euclidean_Space.thy --- a/src/HOL/Library/Convex_Euclidean_Space.thy Sat Jun 13 17:31:24 2009 -0700 +++ b/src/HOL/Library/Convex_Euclidean_Space.thy Sat Jun 13 17:31:56 2009 -0700 @@ -46,7 +46,8 @@ "setsum (\y. if (x = y) then P y else Q y) s = setsum Q s" apply(rule_tac [!] setsum_cong2) using assms by auto -lemma setsum_delta'': fixes s::"(real^'n) set" assumes "finite s" +lemma setsum_delta'': + fixes s::"'a::real_vector set" assumes "finite s" shows "(\x\s. (if y = x then f x else 0) *\<^sub>R x) = (if y\s then (f y) *\<^sub>R y else 0)" proof- have *:"\x y. (if y = x then f x else (0::real)) *\<^sub>R x = (if x=y then (f x) *\<^sub>R x else 0)" by auto @@ -107,8 +108,8 @@ subsection {* Affine set and affine hull.*} definition - affine :: "(real ^ 'n::finite) set \ bool" where - "affine s \ (\x\s. \y\s. \u v::real. u + v = 1 \ (u *\<^sub>R x + v *\<^sub>R y) \ s)" + affine :: "'a::real_vector set \ bool" where + "affine s \ (\x\s. \y\s. \u v. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ s)" lemma affine_alt: "affine s \ (\x\s. \y\s. \u::real. (1 - u) *\<^sub>R x + u *\<^sub>R y \ s)" proof- have *:"\u v ::real. u + v = 1 \ v = 1 - u" by auto @@ -149,7 +150,7 @@ subsection {* Some explicit formulations (from Lars Schewe). *} -lemma affine: fixes V::"(real^'n::finite) set" +lemma affine: fixes V::"'a::real_vector set" shows "affine V \ (\s u. finite s \ s \ {} \ s \ V \ setsum u s = 1 \ (setsum (\x. (u x) *\<^sub>R x)) s \ V)" unfolding affine_def apply rule apply(rule, rule, rule) apply(erule conjE)+ defer apply(rule, rule, rule, rule, rule) proof- @@ -169,7 +170,7 @@ thus ?thesis using as(1)[THEN bspec[where x=a], THEN bspec[where x=b]] using as(4,5) by(auto simp add: setsum_clauses(2)) next assume "card s > 2" thus ?thesis using as and n_def proof(induct n arbitrary: u s) - case (Suc n) fix s::"(real^'n) set" and u::"real^'n\ real" + case (Suc n) fix s::"'a set" and u::"'a \ real" assume IA:"\u s. \2 < card s; \x\V. \y\V. \u v. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ V; finite s; s \ {}; s \ V; setsum u s = 1; n \ card s \ \ (\x\s. u x *\<^sub>R x) \ V" and as:"Suc n \ card s" "2 < card s" "\x\V. \y\V. \u v. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ V" @@ -251,7 +252,8 @@ apply(rule hull_unique) unfolding mem_def by auto lemma affine_hull_finite_step: - shows "(\u::real^'n=>real. setsum u {} = w \ setsum (\x. u x *\<^sub>R x) {} = y) \ w = 0 \ y = 0" (is ?th1) + fixes y :: "'a::real_vector" + shows "(\u. setsum u {} = w \ setsum (\x. u x *\<^sub>R x) {} = y) \ w = 0 \ y = 0" (is ?th1) "finite s \ (\u. setsum u (insert a s) = w \ setsum (\x. u x *\<^sub>R x) (insert a s) = y) \ (\v u. setsum u s = w - v \ setsum (\x. u x *\<^sub>R x) s = y - v *\<^sub>R a)" (is "?as \ (?lhs = ?rhs)") proof- @@ -288,10 +290,12 @@ ultimately show "?lhs = ?rhs" by blast qed -lemma affine_hull_2:"affine hull {a,b::real^'n::finite} = {u *\<^sub>R a + v *\<^sub>R b| u v. (u + v = 1)}" (is "?lhs = ?rhs") +lemma affine_hull_2: + fixes a b :: "'a::real_vector" + shows "affine hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b| u v. (u + v = 1)}" (is "?lhs = ?rhs") proof- have *:"\x y z. z = x - y \ y + z = (x::real)" - "\x y z. z = x - y \ y + z = (x::real^'n)" by auto + "\x y z. z = x - y \ y + z = (x::'a)" by auto have "?lhs = {y. \u. setsum u {a, b} = 1 \ (\v\{a, b}. u v *\<^sub>R v) = y}" using affine_hull_finite[of "{a,b}"] by auto also have "\ = {y. \v u. u b = 1 - v \ u b *\<^sub>R b = y - v *\<^sub>R a}" @@ -300,10 +304,12 @@ finally show ?thesis by auto qed -lemma affine_hull_3: "affine hull {a,b,c::real^'n::finite} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c| u v w. u + v + w = 1}" (is "?lhs = ?rhs") +lemma affine_hull_3: + fixes a b c :: "'a::real_vector" + shows "affine hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c| u v w. u + v + w = 1}" (is "?lhs = ?rhs") proof- have *:"\x y z. z = x - y \ y + z = (x::real)" - "\x y z. z = x - y \ y + z = (x::real^'n)" by auto + "\x y z. z = x - y \ y + z = (x::'a)" by auto show ?thesis apply(simp add: affine_hull_finite affine_hull_finite_step) unfolding * apply auto apply(rule_tac x=v in exI) apply(rule_tac x=va in exI) apply auto @@ -313,7 +319,8 @@ subsection {* Some relations between affine hull and subspaces. *} lemma affine_hull_insert_subset_span: - "affine hull (insert a s) \ {a + v| v . v \ span {x - a | x . x \ s}}" + fixes a :: "real ^ _" + shows "affine hull (insert a s) \ {a + v| v . v \ span {x - a | x . x \ s}}" unfolding subset_eq Ball_def unfolding affine_hull_explicit span_explicit mem_Collect_eq smult_conv_scaleR apply(rule,rule) apply(erule exE)+ apply(erule conjE)+ proof- fix x t u assume as:"finite t" "t \ {}" "t \ insert a s" "setsum u t = 1" "(\v\t. u v *\<^sub>R v) = x" @@ -330,6 +337,7 @@ unfolding as by simp qed lemma affine_hull_insert_span: + fixes a :: "real ^ _" assumes "a \ s" shows "affine hull (insert a s) = {a + v | v . v \ span {x - a | x. x \ s}}" @@ -349,14 +357,16 @@ by (auto simp add: setsum_subtractf scaleR_left.setsum algebra_simps) qed lemma affine_hull_span: + fixes a :: "real ^ _" assumes "a \ s" shows "affine hull s = {a + v | v. v \ span {x - a | x. x \ s - {a}}}" using affine_hull_insert_span[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto subsection {* Convexity. *} -definition "convex (s::(real^'n::finite) set) \ - (\x\s. \y\s. \u\0. \v\0. (u + v = 1) \ (u *\<^sub>R x + v *\<^sub>R y) \ s)" +definition + convex :: "'a::real_vector set \ bool" where + "convex s \ (\x\s. \y\s. \u\0. \v\0. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ s)" lemma convex_alt: "convex s \ (\x\s. \y\s. \u. 0 \ u \ u \ 1 \ ((1 - u) *\<^sub>R x + u *\<^sub>R y) \ s)" proof- have *:"\u v::real. u + v = 1 \ u = 1 - v" by auto @@ -445,7 +455,9 @@ thus ?thesis unfolding setsum_cl_ivl_Suc and *** and scaleR_right.setsum [symmetric] using nn by auto qed qed auto qed -lemma convex_explicit: "convex (s::(real^'n::finite) set) \ +lemma convex_explicit: + fixes s :: "'a::real_vector set" + shows "convex s \ (\t u. finite t \ t \ s \ (\x\t. 0 \ u x) \ setsum u t = 1 \ setsum (\x. u x *\<^sub>R x) t \ s)" unfolding convex_def apply(rule,rule,rule) apply(subst imp_conjL,rule) defer apply(rule,rule,rule,rule,rule,rule,rule) proof- fix x y u v assume as:"\t u. finite t \ t \ s \ (\x\t. 0 \ u x) \ setsum u t = 1 \ (\x\t. u x *\<^sub>R x) \ s" "x \ s" "y \ s" "0 \ u" "0 \ v" "u + v = (1::real)" @@ -453,7 +465,7 @@ case True show ?thesis unfolding True and scaleR_left_distrib[THEN sym] using as(3,6) by auto next case False thus ?thesis using as(1)[THEN spec[where x="{x,y}"], THEN spec[where x="\z. if z=x then u else v"]] and as(2-) by auto qed next - fix t u assume asm:"\x\s. \y\s. \u\0. \v\0. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ s" "finite (t::(real^'n) set)" + fix t u assume asm:"\x\s. \y\s. \u\0. \v\0. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ s" "finite (t::'a set)" (*"finite t" "t \ s" "\x\t. (0::real) \ u x" "setsum u t = 1"*) from this(2) have "\u. t \ s \ (\x\t. 0 \ u x) \ setsum u t = 1 \ (\x\t. u x *\<^sub>R x) \ s" apply(induct_tac t rule:finite_induct) prefer 3 apply (rule,rule) apply(erule conjE)+ proof- @@ -493,7 +505,9 @@ subsection {* Cones. *} -definition "cone (s::(real^'n) set) \ (\x\s. \c\0. (c *\<^sub>R x) \ s)" +definition + cone :: "'a::real_vector set \ bool" where + "cone s \ (\x\s. \c\0. (c *\<^sub>R x) \ s)" lemma cone_empty[intro, simp]: "cone {}" unfolding cone_def by auto @@ -517,7 +531,7 @@ subsection {* Affine dependence and consequential theorems (from Lars Schewe). *} definition - affine_dependent :: "(real ^ 'n::finite) set \ bool" where + affine_dependent :: "'a::real_vector set \ bool" where "affine_dependent s \ (\x\s. x \ (affine hull (s - {x})))" lemma affine_dependent_explicit: @@ -537,21 +551,21 @@ have "s \ {v}" using as(3,6) by auto thus "\x\p. \s u. finite s \ s \ {} \ s \ p - {x} \ setsum u s = 1 \ (\v\s. u v *\<^sub>R v) = x" apply(rule_tac x=v in bexI, rule_tac x="s - {v}" in exI, rule_tac x="\x. - (1 / u v) * u x" in exI) - unfolding scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric] unfolding setsum_right_distrib[THEN sym] and setsum_diff1_ring[OF as(1,5)] using as by auto + unfolding scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric] unfolding setsum_right_distrib[THEN sym] and setsum_diff1[OF as(1)] using as by auto qed lemma affine_dependent_explicit_finite: - assumes "finite (s::(real^'n::finite) set)" + fixes s :: "'a::real_vector set" assumes "finite s" shows "affine_dependent s \ (\u. setsum u s = 0 \ (\v\s. u v \ 0) \ setsum (\v. u v *\<^sub>R v) s = 0)" (is "?lhs = ?rhs") proof - have *:"\vt u v. (if vt then u v else 0) *\<^sub>R v = (if vt then (u v) *\<^sub>R v else (0::real^'n))" by auto + have *:"\vt u v. (if vt then u v else 0) *\<^sub>R v = (if vt then (u v) *\<^sub>R v else (0::'a))" by auto assume ?lhs then obtain t u v where "finite t" "t \ s" "setsum u t = 0" "v\t" "u v \ 0" "(\v\t. u v *\<^sub>R v) = 0" unfolding affine_dependent_explicit by auto thus ?rhs apply(rule_tac x="\x. if x\t then u x else 0" in exI) apply auto unfolding * and setsum_restrict_set[OF assms, THEN sym] - unfolding Int_absorb2[OF `t\s`, unfolded Int_commute] by auto + unfolding Int_absorb1[OF `t\s`] by auto next assume ?rhs then obtain u v where "setsum u s = 0" "v\s" "u v \ 0" "(\v\s. u v *\<^sub>R v) = 0" by auto @@ -561,6 +575,7 @@ subsection {* A general lemma. *} lemma convex_connected: + fixes s :: "'a::real_normed_vector set" assumes "convex s" shows "connected s" proof- { fix e1 e2 assume as:"open e1" "open e2" "e1 \ e2 \ s = {}" "s \ e1 \ e2" @@ -595,12 +610,14 @@ subsection {* One rather trivial consequence. *} -lemma connected_UNIV: "connected (UNIV :: (real ^ _) set)" +lemma connected_UNIV: "connected (UNIV :: 'a::real_normed_vector set)" by(simp add: convex_connected convex_UNIV) subsection {* Convex functions into the reals. *} -definition "convex_on s (f::real^'n \ real) = +definition + convex_on :: "'a::real_vector set \ ('a \ real) \ bool" where + "convex_on s f \ (\x\s. \y\s. \u\0. \v\0. u + v = 1 \ f (u *\<^sub>R x + v *\<^sub>R y) \ u * f x + v * f y)" lemma convex_on_subset: "convex_on t f \ s \ t \ convex_on s f" @@ -641,6 +658,7 @@ qed lemma convex_local_global_minimum: + fixes s :: "'a::real_normed_vector set" assumes "0 s" "\y\ball x e. f x \ f y" shows "\y\s. f x \ f y" proof(rule ccontr) @@ -661,7 +679,9 @@ ultimately show False using mult_strict_left_mono[OF y `u>0`] unfolding left_diff_distrib by auto qed -lemma convex_distance: "convex_on s (\x. dist a x)" +lemma convex_distance: + fixes s :: "'a::real_normed_vector set" + shows "convex_on s (\x. dist a x)" proof(auto simp add: convex_on_def dist_norm) fix x y assume "x\s" "y\s" fix u v ::real assume "0 \ u" "0 \ v" "u + v = 1" @@ -710,7 +730,7 @@ proof- have "{a + y |y. y \ s} = (\x. a + x) ` s" by auto thus ?thesis using convex_sums[OF convex_singleton[of a] assms] by auto qed -lemma convex_affinity: assumes "convex (s::(real^'n::finite) set)" shows "convex ((\x. a + c *\<^sub>R x) ` s)" +lemma convex_affinity: assumes "convex s" shows "convex ((\x. a + c *\<^sub>R x) ` s)" proof- have "(\x. a + c *\<^sub>R x) ` s = op + a ` op *\<^sub>R c ` s" by auto thus ?thesis using convex_translation[OF convex_scaling[OF assms], of a c] by auto qed @@ -729,7 +749,9 @@ subsection {* Balls, being convex, are connected. *} -lemma convex_ball: "convex (ball x e)" +lemma convex_ball: + fixes x :: "'a::real_normed_vector" + shows "convex (ball x e)" proof(auto simp add: convex_def) fix y z assume yz:"dist x y < e" "dist x z < e" fix u v ::real assume uv:"0 \ u" "0 \ v" "u + v = 1" @@ -738,7 +760,9 @@ thus "dist x (u *\<^sub>R y + v *\<^sub>R z) < e" using real_convex_bound_lt[OF yz uv] by auto qed -lemma convex_cball: "convex(cball x e)" +lemma convex_cball: + fixes x :: "'a::real_normed_vector" + shows "convex(cball x e)" proof(auto simp add: convex_def Ball_def mem_cball) fix y z assume yz:"dist x y \ e" "dist x z \ e" fix u v ::real assume uv:" 0 \ u" "0 \ v" "u + v = 1" @@ -747,10 +771,14 @@ thus "dist x (u *\<^sub>R y + v *\<^sub>R z) \ e" using real_convex_bound_le[OF yz uv] by auto qed -lemma connected_ball: "connected(ball (x::real^_) e)" (* FIXME: generalize *) +lemma connected_ball: + fixes x :: "'a::real_normed_vector" + shows "connected (ball x e)" using convex_connected convex_ball by auto -lemma connected_cball: "connected(cball (x::real^_) e)" (* FIXME: generalize *) +lemma connected_cball: + fixes x :: "'a::real_normed_vector" + shows "connected(cball x e)" using convex_connected convex_cball by auto subsection {* Convex hull. *} @@ -762,14 +790,17 @@ lemma convex_hull_eq: "(convex hull s = s) \ convex s" apply(rule hull_eq[unfolded mem_def]) using convex_Inter[unfolded Ball_def mem_def] by auto -lemma bounded_convex_hull: assumes "bounded s" shows "bounded(convex hull s)" +lemma bounded_convex_hull: + fixes s :: "'a::real_normed_vector set" + assumes "bounded s" shows "bounded(convex hull s)" proof- from assms obtain B where B:"\x\s. norm x \ B" unfolding bounded_iff by auto show ?thesis apply(rule bounded_subset[OF bounded_cball, of _ 0 B]) unfolding subset_hull[unfolded mem_def, of convex, OF convex_cball] unfolding subset_eq mem_cball dist_norm using B by auto qed lemma finite_imp_bounded_convex_hull: - "finite s \ bounded(convex hull s)" + fixes s :: "'a::real_normed_vector set" + shows "finite s \ bounded(convex hull s)" using bounded_convex_hull finite_imp_bounded by auto subsection {* Stepping theorems for convex hulls of finite sets. *} @@ -781,6 +812,7 @@ apply(rule hull_unique) unfolding mem_def by auto lemma convex_hull_insert: + fixes s :: "'a::real_vector set" assumes "s \ {}" shows "convex hull (insert a s) = {x. \u\0. \v\0. \b. (u + v = 1) \ b \ (convex hull s) \ (x = u *\<^sub>R a + v *\<^sub>R b)}" (is "?xyz = ?hull") @@ -800,10 +832,10 @@ fix x y u v assume as:"(0::real) \ u" "0 \ v" "u + v = 1" "x\?hull" "y\?hull" from as(4) obtain u1 v1 b1 where obt1:"u1\0" "v1\0" "u1 + v1 = 1" "b1 \ convex hull s" "x = u1 *\<^sub>R a + v1 *\<^sub>R b1" by auto from as(5) obtain u2 v2 b2 where obt2:"u2\0" "v2\0" "u2 + v2 = 1" "b2 \ convex hull s" "y = u2 *\<^sub>R a + v2 *\<^sub>R b2" by auto - have *:"\(x::real^_) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps) + have *:"\(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps) have "\b \ convex hull s. u *\<^sub>R x + v *\<^sub>R y = (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (b - (u * u1) *\<^sub>R b - (v * u2) *\<^sub>R b)" proof(cases "u * v1 + v * v2 = 0") - have *:"\(x::real^_) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps) + have *:"\(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps) case True hence **:"u * v1 = 0" "v * v2 = 0" apply- apply(rule_tac [!] ccontr) using mult_nonneg_nonneg[OF `u\0` `v1\0`] mult_nonneg_nonneg[OF `v\0` `v2\0`] by auto hence "u * u1 + v * u2 = 1" using as(3) obt1(3) obt2(3) by auto @@ -837,7 +869,8 @@ subsection {* Explicit expression for convex hull. *} lemma convex_hull_indexed: - "convex hull s = {y. \k u x. (\i\{1::nat .. k}. 0 \ u i \ x i \ s) \ + fixes s :: "'a::real_vector set" + shows "convex hull s = {y. \k u x. (\i\{1::nat .. k}. 0 \ u i \ x i \ s) \ (setsum u {1..k} = 1) \ (setsum (\i. u i *\<^sub>R x i) {1..k} = y)}" (is "?xyz = ?hull") apply(rule hull_unique) unfolding mem_def[of _ convex] apply(rule) defer @@ -855,7 +888,7 @@ fix x y u v assume uv:"0\u" "0\v" "u+v=(1::real)" and xy:"x\?hull" "y\?hull" from xy obtain k1 u1 x1 where x:"\i\{1::nat..k1}. 0\u1 i \ x1 i \ s" "setsum u1 {Suc 0..k1} = 1" "(\i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x" by auto from xy obtain k2 u2 x2 where y:"\i\{1::nat..k2}. 0\u2 i \ x2 i \ s" "setsum u2 {Suc 0..k2} = 1" "(\i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y" by auto - have *:"\P x1 x2 s1 s2 i.(if P i then s1 else s2) *\<^sub>R (if P i then x1 else x2) = (if P i then s1 *\<^sub>R x1 else s2 *\<^sub>R x2)" + have *:"\P (x1::'a) x2 s1 s2 i.(if P i then s1 else s2) *\<^sub>R (if P i then x1 else x2) = (if P i then s1 *\<^sub>R x1 else s2 *\<^sub>R x2)" "{1..k1 + k2} \ {1..k1} = {1..k1}" "{1..k1 + k2} \ - {1..k1} = (\i. i + k1) ` {1..k2}" prefer 3 apply(rule,rule) unfolding image_iff apply(rule_tac x="x - k1" in bexI) by(auto simp add: not_le) have inj:"inj_on (\i. i + k1) {1..k2}" unfolding inj_on_def by auto @@ -876,7 +909,8 @@ qed lemma convex_hull_finite: - assumes "finite (s::(real^'n::finite)set)" + fixes s :: "'a::real_vector set" + assumes "finite s" shows "convex hull s = {y. \u. (\