# HG changeset patch # User blanchet # Date 1379373097 -7200 # Node ID 81e244e71986cf4d0f34204a984f38dd14e3cf16 # Parent e55bb583342e37f2d46f9ea8dbd81f671357d1a4# Parent 476ef9b468d218e870ddd497a5e0e74ad5024956 merge diff -r e55bb583342e -r 81e244e71986 src/HOL/Library/Convex.thy --- a/src/HOL/Library/Convex.thy Tue Sep 17 01:09:51 2013 +0200 +++ b/src/HOL/Library/Convex.thy Tue Sep 17 01:11:37 2013 +0200 @@ -14,6 +14,16 @@ 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 convexI: + assumes "\x y u v. x \ s \ y \ s \ 0 \ u \ 0 \ v \ u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ s" + shows "convex s" + using assms unfolding convex_def by fast + +lemma convexD: + assumes "convex s" and "x \ s" and "y \ s" and "0 \ u" and "0 \ v" and "u + v = 1" + shows "u *\<^sub>R x + v *\<^sub>R y \ s" + using assms unfolding convex_def by fast + lemma convex_alt: "convex s \ (\x\s. \y\s. \u. 0 \ u \ u \ 1 \ ((1 - u) *\<^sub>R x + u *\<^sub>R y) \ s)" (is "_ \ ?alt") @@ -140,7 +150,7 @@ then have a1: "(\ j \ s. ?a j) = 1" unfolding setsum_divide_distrib by simp with asms have "(\j\s. ?a j *\<^sub>R y j) \ C" using a_nonneg by fastforce then have "a i *\<^sub>R y i + (1 - a i) *\<^sub>R (\ j \ s. ?a j *\<^sub>R y j) \ C" - using asms[unfolded convex_def, rule_format] yai ai1 by auto + using asms yai ai1 by (auto intro: convexD) then have "a i *\<^sub>R y i + (\ j \ s. (1 - a i) *\<^sub>R (?a j *\<^sub>R y j)) \ C" using scaleR_right.setsum[of "(1 - a i)" "\ j. ?a j *\<^sub>R y j" s] by auto then have "a i *\<^sub>R y i + (\ j \ s. a j *\<^sub>R y j) \ C" using i0 by auto diff -r e55bb583342e -r 81e244e71986 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Sep 17 01:09:51 2013 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Sep 17 01:11:37 2013 +0200 @@ -31,19 +31,12 @@ shows "f (a *\<^sub>R x + b *\<^sub>R y) = a *\<^sub>R f x + b *\<^sub>R f y" using linear_add[of f] linear_cmul[of f] assms by simp -lemma mem_convex_2: - assumes "convex S" "x \ S" "y \ S" "u \ 0" "v \ 0" "u + v = 1" - shows "u *\<^sub>R x + v *\<^sub>R y \ S" - using assms convex_def[of S] by auto - lemma mem_convex_alt: assumes "convex S" "x \ S" "y \ S" "u \ 0" "v \ 0" "u + v > 0" shows "((u/(u+v)) *\<^sub>R x + (v/(u+v)) *\<^sub>R y) \ S" - apply (subst mem_convex_2) + apply (rule convexD) using assms - apply (auto simp add: algebra_simps zero_le_divide_iff) - using add_divide_distrib[of u v "u+v"] - apply auto + apply (simp_all add: zero_le_divide_iff add_divide_distrib [symmetric]) done lemma inj_on_image_mem_iff: "inj_on f B \ A \ B \ f a \ f`A \ a \ B \ a \ A" @@ -1348,7 +1341,6 @@ text {* Balls, being convex, are connected. *} lemma convex_box: - fixes a::"'a::euclidean_space" assumes "\i. i \ Basis \ convex {x. P i x}" shows "convex {x. \i\Basis. P i (x\i)}" using assms unfolding convex_def @@ -1575,19 +1567,11 @@ using hull_mono[of s "insert a s" convex] hull_mono[of "{a}" "insert a s" convex] and obt(4) by auto then show "x \ convex hull insert a s" - unfolding obt(5) - using convex_convex_hull[of "insert a s", unfolded convex_def] - apply (erule_tac x = a in ballE) - apply (erule_tac x = b in ballE) - apply (erule_tac x = u in allE) - using obt - apply auto - done + unfolding obt(5) using obt(1-3) + by (rule convexD [OF convex_convex_hull]) next show "convex ?hull" - unfolding convex_def - apply (rule, rule, rule, rule, rule, rule, rule) - proof - + proof (rule convexI) 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 @@ -1637,7 +1621,7 @@ apply (rule_tac x = "((u * v1) / (u * v1 + v * v2)) *\<^sub>R b1 + ((v * v2) / (u * v1 + v * v2)) *\<^sub>R b2" in bexI) defer - apply (rule convex_convex_hull[of s, unfolded convex_def, rule_format]) + apply (rule convexD [OF convex_convex_hull]) using obt1(4) obt2(4) unfolding add_divide_distrib[symmetric] and zero_le_divide_iff apply (auto simp add: scaleR_left_distrib scaleR_right_distrib) @@ -1681,8 +1665,7 @@ apply (rule hull_unique) apply rule defer - apply (subst convex_def) - apply (rule, rule, rule, rule, rule, rule, rule) + apply (rule convexI) proof - fix x assume "x\s" @@ -4667,13 +4650,11 @@ fixes s :: "'a::real_normed_vector set" assumes "convex s" shows "convex (closure s)" - unfolding convex_def Ball_def closure_sequential - apply (rule,rule,rule,rule,rule,rule,rule,rule,rule) - apply (elim exE) - apply (rule_tac x="\n. u *\<^sub>R xb n + v *\<^sub>R xc n" in exI) + apply (rule convexI) + apply (unfold closure_sequential, elim exE) + apply (rule_tac x="\n. u *\<^sub>R xa n + v *\<^sub>R xb n" in exI) apply (rule,rule) - apply (rule assms[unfolded convex_def, rule_format]) - prefer 6 + apply (rule convexD [OF assms]) apply (auto del: tendsto_const intro!: tendsto_intros) done @@ -4715,37 +4696,25 @@ subsection {* Moving and scaling convex hulls. *} -lemma convex_hull_translation_lemma: - "convex hull ((\x. a + x) ` s) \ (\x. a + x) ` (convex hull s)" - by (metis convex_convex_hull convex_translation hull_minimal hull_subset image_mono) - -lemma convex_hull_bilemma: - assumes "\s a. (convex hull (up a s)) \ up a (convex hull s)" - shows "(\s. up a (up (neg a) s) = s) \ (\s. up (neg a) (up a s) = s) \ (\s t a. s \ t \ up a s \ up a t) - \ \s. (convex hull (up a s)) = up a (convex hull s)" - using assms by (metis subset_antisym) +lemma convex_hull_set_plus: + "convex hull (s + t) = convex hull s + convex hull t" + unfolding set_plus_image + apply (subst convex_hull_linear_image [symmetric]) + apply (simp add: linear_iff scaleR_right_distrib) + apply (simp add: convex_hull_Times) + done + +lemma translation_eq_singleton_plus: "(\x. a + x) ` t = {a} + t" + unfolding set_plus_def by auto lemma convex_hull_translation: "convex hull ((\x. a + x) ` s) = (\x. a + x) ` (convex hull s)" - apply (rule convex_hull_bilemma[rule_format, of _ _ "\a. -a"]) - apply (rule convex_hull_translation_lemma) - unfolding image_image - apply auto - done - -lemma convex_hull_scaling_lemma: - "convex hull ((\x. c *\<^sub>R x) ` s) \ (\x. c *\<^sub>R x) ` (convex hull s)" - by (metis convex_convex_hull convex_scaling hull_subset subset_hull subset_image_iff) + unfolding translation_eq_singleton_plus + by (simp only: convex_hull_set_plus convex_hull_singleton) lemma convex_hull_scaling: "convex hull ((\x. c *\<^sub>R x) ` s) = (\x. c *\<^sub>R x) ` (convex hull s)" - apply (cases "c = 0") - defer - apply (rule convex_hull_bilemma[rule_format, of _ _ inverse]) - apply (rule convex_hull_scaling_lemma) - unfolding image_image scaleR_scaleR - apply (auto simp add:image_constant_conv) - done + using linear_scaleR by (rule convex_hull_linear_image [symmetric]) lemma convex_hull_affinity: "convex hull ((\x. a + c *\<^sub>R x) ` s) = (\x. a + c *\<^sub>R x) ` (convex hull s)" @@ -4757,44 +4726,41 @@ lemma convex_cone_hull: assumes "convex S" shows "convex (cone hull S)" -proof - +proof (rule convexI) + fix x y + assume xy: "x \ cone hull S" "y \ cone hull S" + then have "S \ {}" + using cone_hull_empty_iff[of S] by auto + fix u v :: real + assume uv: "u \ 0" "v \ 0" "u + v = 1" + then have *: "u *\<^sub>R x \ cone hull S" "v *\<^sub>R y \ cone hull S" + using cone_cone_hull[of S] xy cone_def[of "cone hull S"] by auto + from * obtain cx :: real and xx where x: "u *\<^sub>R x = cx *\<^sub>R xx" "cx \ 0" "xx \ S" + using cone_hull_expl[of S] by auto + from * obtain cy :: real and yy where y: "v *\<^sub>R y = cy *\<^sub>R yy" "cy \ 0" "yy \ S" + using cone_hull_expl[of S] by auto { - fix x y - assume xy: "x \ cone hull S" "y \ cone hull S" - then have "S \ {}" - using cone_hull_empty_iff[of S] by auto - fix u v :: real - assume uv: "u \ 0" "v \ 0" "u + v = 1" - then have *: "u *\<^sub>R x \ cone hull S" "v *\<^sub>R y \ cone hull S" - using cone_cone_hull[of S] xy cone_def[of "cone hull S"] by auto - from * obtain cx :: real and xx where x: "u *\<^sub>R x = cx *\<^sub>R xx" "cx \ 0" "xx \ S" - using cone_hull_expl[of S] by auto - from * obtain cy :: real and yy where y: "v *\<^sub>R y = cy *\<^sub>R yy" "cy \ 0" "yy \ S" - using cone_hull_expl[of S] by auto - { - assume "cx + cy \ 0" - then have "u *\<^sub>R x = 0" and "v *\<^sub>R y = 0" - using x y by auto - then have "u *\<^sub>R x+ v *\<^sub>R y = 0" - by auto - then have "u *\<^sub>R x+ v *\<^sub>R y \ cone hull S" - using cone_hull_contains_0[of S] `S \ {}` by auto - } - moreover - { - assume "cx + cy > 0" - then have "(cx / (cx + cy)) *\<^sub>R xx + (cy / (cx + cy)) *\<^sub>R yy \ S" - using assms mem_convex_alt[of S xx yy cx cy] x y by auto - then have "cx *\<^sub>R xx + cy *\<^sub>R yy \ cone hull S" - using mem_cone_hull[of "(cx/(cx+cy)) *\<^sub>R xx + (cy/(cx+cy)) *\<^sub>R yy" S "cx+cy"] `cx+cy>0` - by (auto simp add: scaleR_right_distrib) - then have "u *\<^sub>R x+ v *\<^sub>R y \ cone hull S" - using x y by auto - } - moreover have "cx + cy \ 0 \ cx + cy > 0" by auto - ultimately have "u *\<^sub>R x+ v *\<^sub>R y \ cone hull S" by blast + assume "cx + cy \ 0" + then have "u *\<^sub>R x = 0" and "v *\<^sub>R y = 0" + using x y by auto + then have "u *\<^sub>R x + v *\<^sub>R y = 0" + by auto + then have "u *\<^sub>R x + v *\<^sub>R y \ cone hull S" + using cone_hull_contains_0[of S] `S \ {}` by auto } - then show ?thesis unfolding convex_def by auto + moreover + { + assume "cx + cy > 0" + then have "(cx / (cx + cy)) *\<^sub>R xx + (cy / (cx + cy)) *\<^sub>R yy \ S" + using assms mem_convex_alt[of S xx yy cx cy] x y by auto + then have "cx *\<^sub>R xx + cy *\<^sub>R yy \ cone hull S" + using mem_cone_hull[of "(cx/(cx+cy)) *\<^sub>R xx + (cy/(cx+cy)) *\<^sub>R yy" S "cx+cy"] `cx+cy>0` + by (auto simp add: scaleR_right_distrib) + then have "u *\<^sub>R x + v *\<^sub>R y \ cone hull S" + using x y by auto + } + moreover have "cx + cy \ 0 \ cx + cy > 0" by auto + ultimately show "u *\<^sub>R x + v *\<^sub>R y \ cone hull S" by blast qed lemma cone_convex_hull: @@ -5660,11 +5626,6 @@ subsection {* Convexity of general and special intervals *} -lemma convexI: (* TODO: move to Library/Convex.thy *) - assumes "\x y u v. x \ s \ y \ s \ 0 \ u \ 0 \ v \ u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ s" - shows "convex s" - using assms unfolding convex_def by fast - lemma is_interval_convex: fixes s :: "'a::euclidean_space set" assumes "is_interval s" @@ -5880,14 +5841,6 @@ apply simp done -lemma convex_hull_set_plus: - "convex hull (s + t) = convex hull s + convex hull t" - unfolding set_plus_image - apply (subst convex_hull_linear_image [symmetric]) - apply (simp add: linear_iff scaleR_right_distrib) - apply (simp add: convex_hull_Times) - done - lemma convex_hull_set_setsum: "convex hull (\i\A. B i) = (\i\A. convex hull (B i))" proof (cases "finite A")