# HG changeset patch # User nipkow # Date 1270117160 -7200 # Node ID c8ae8e56d42ed1704eda02251f27fe6ee587c8e5 # Parent d80e5d3c8fe1ea4140794b93365d19377690e674 tuned many proofs a bit diff -r d80e5d3c8fe1 -r c8ae8e56d42e src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Apr 01 09:31:58 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Apr 01 12:19:20 2010 +0200 @@ -101,11 +101,7 @@ "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 - { fix x y assume "x\s" "y\s" - hence "(\u v::real. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ s) \ (\u::real. (1 - u) *\<^sub>R x + u *\<^sub>R y \ s)" apply auto - apply(erule_tac[!] x="1 - u" in allE) unfolding * by auto } - thus ?thesis unfolding affine_def by auto qed +unfolding affine_def by(metis eq_diff_eq') lemma affine_empty[intro]: "affine {}" unfolding affine_def by auto @@ -127,11 +123,7 @@ unfolding mem_def by auto lemma affine_hull_eq[simp]: "(affine hull s = s) \ affine s" -proof- - { fix f assume "f \ affine" - hence "affine (\f)" using affine_Inter[of f] unfolding subset_eq mem_def by auto } - thus ?thesis using hull_eq[unfolded mem_def, of affine s] by auto -qed +by (metis affine_affine_hull hull_same mem_def) lemma setsum_restrict_set'': assumes "finite A" shows "setsum f {x \ A. P x} = (\x\A. if P x then f x else 0)" @@ -437,7 +429,7 @@ thus ?thesis unfolding setsum_cl_ivl_Suc using True and Suc(2) by auto next have *:"setsum u {1..k} = 1 - u (Suc k)" using Suc(3)[unfolded setsum_cl_ivl_Suc] by auto - have **:"u (Suc k) \ 1" apply(rule ccontr) unfolding not_le using Suc(3) using setsum_nonneg[of "{1..k}" u] using Suc(2) by auto + have **:"u (Suc k) \ 1" unfolding not_le using Suc(3) using setsum_nonneg[of "{1..k}" u] using Suc(2) by auto have ***:"\i k. (u i / (1 - u (Suc k))) *\<^sub>R x i = (inverse (1 - u (Suc k))) *\<^sub>R (u i *\<^sub>R x i)" unfolding real_divide_def by (auto simp add: algebra_simps) case False hence nn:"1 - u (Suc k) \ 0" by auto have "(\i = 1..k. (u i / (1 - u (Suc k))) *\<^sub>R x i) \ s" apply(rule Suc(1)) unfolding setsum_divide_distrib[THEN sym] and * @@ -474,7 +466,7 @@ thus ?thesis unfolding setsum_clauses(2)[OF as(1)] using as(2,3) unfolding True by auto next have *:"setsum u f = setsum u (insert x f) - u x" using as(2) unfolding setsum_clauses(2)[OF as(1)] by auto - have **:"u x \ 1" apply(rule ccontr) unfolding not_le using as(5)[unfolded setsum_clauses(2)[OF as(1)]] and as(2) + have **:"u x \ 1" unfolding not_le using as(5)[unfolded setsum_clauses(2)[OF as(1)]] and as(2) using setsum_nonneg[of f u] and as(4) by auto case False hence "inverse (1 - u x) *\<^sub>R (\x\f. u x *\<^sub>R x) \ s" unfolding scaleR_right.setsum and scaleR_scaleR apply(rule_tac ind[THEN spec, THEN mp]) apply rule defer apply rule apply rule apply(rule mult_nonneg_nonneg) @@ -780,10 +772,7 @@ unfolding mem_def by auto lemma convex_hull_eq: "convex hull s = s \ convex s" - apply (rule hull_eq [unfolded mem_def]) - apply (rule convex_Inter [unfolded Ball_def mem_def]) - apply (simp add: le_fun_def le_bool_def) - done +by (metis convex_convex_hull hull_same mem_def) lemma bounded_convex_hull: fixes s :: "'a::real_normed_vector set" @@ -831,8 +820,8 @@ 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::'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 + case True hence **:"u * v1 = 0" "v * v2 = 0" + using mult_nonneg_nonneg[OF `u\0` `v1\0`] mult_nonneg_nonneg[OF `v\0` `v2\0`] by arith+ hence "u * u1 + v * u2 = 1" using as(3) obt1(3) obt2(3) by auto thus ?thesis unfolding obt1(5) obt2(5) * using assms hull_subset[of s convex] by(auto simp add: ** scaleR_right_distrib) next @@ -848,8 +837,8 @@ unfolding add_divide_distrib[THEN sym] and real_0_le_divide_iff by (auto simp add: scaleR_left_distrib scaleR_right_distrib) qed note * = this - have u1:"u1 \ 1" apply(rule ccontr) unfolding obt1(3)[THEN sym] and not_le using obt1(2) by auto - have u2:"u2 \ 1" apply(rule ccontr) unfolding obt2(3)[THEN sym] and not_le using obt2(2) by auto + have u1:"u1 \ 1" unfolding obt1(3)[THEN sym] and not_le using obt1(2) by auto + have u2:"u2 \ 1" unfolding obt2(3)[THEN sym] and not_le using obt2(2) by auto have "u1 * u + u2 * v \ (max u1 u2) * u + (max u1 u2) * v" apply(rule add_mono) apply(rule_tac [!] mult_right_mono) using as(1,2) obt1(1,2) obt2(1,2) by auto also have "\ \ 1" unfolding mult.add_right[THEN sym] and as(3) using u1 u2 by auto @@ -1072,17 +1061,15 @@ lemma affine_hull_subset_span: fixes s :: "(real ^ _) set" shows "(affine hull s) \ (span s)" - unfolding span_def apply(rule hull_antimono) unfolding subset_eq Ball_def mem_def - using subspace_imp_affine by auto +by (metis hull_minimal mem_def span_inc subspace_imp_affine subspace_span) lemma convex_hull_subset_span: fixes s :: "(real ^ _) set" shows "(convex hull s) \ (span s)" - unfolding span_def apply(rule hull_antimono) unfolding subset_eq Ball_def mem_def - using subspace_imp_convex by auto +by (metis hull_minimal mem_def span_inc subspace_imp_convex subspace_span) lemma convex_hull_subset_affine_hull: "(convex hull s) \ (affine hull s)" - unfolding span_def apply(rule hull_antimono) unfolding subset_eq Ball_def mem_def - using affine_imp_convex by auto +by (metis affine_affine_hull affine_imp_convex hull_minimal hull_subset mem_def) + lemma affine_dependent_imp_dependent: fixes s :: "(real ^ _) set" shows "affine_dependent s \ dependent s" @@ -1282,11 +1269,7 @@ lemma tendsto_dest_vec1 [tendsto_intros]: "(f ---> l) net \ ((\x. dest_vec1 (f x)) ---> dest_vec1 l) net" - unfolding tendsto_def - apply clarify - apply (drule_tac x="dest_vec1 -` S" in spec) - apply (simp add: open_dest_vec1_vimage) - done +by(rule tendsto_Cart_nth) lemma continuous_dest_vec1: "continuous net f \ continuous net (\x. dest_vec1 (f x))" unfolding continuous_def by (rule tendsto_dest_vec1) @@ -1405,7 +1388,7 @@ lemma finite_imp_compact_convex_hull: fixes s :: "(real ^ _) set" shows "finite s \ compact(convex hull s)" - apply(drule finite_imp_compact, drule compact_convex_hull) by assumption +by (metis compact_convex_hull finite_imp_compact) subsection {* Extremal points of a simplex are some vertices. *} @@ -1598,18 +1581,6 @@ let ?z = "(1 - u) *\<^sub>R x + u *\<^sub>R y" have "?z \ s" using mem_convex[OF assms(1,3,4), of u] using u by auto thus False using assms(5)[THEN bspec[where x="?z"]] and u(3) by (auto simp add: dist_commute algebra_simps) qed -(* TODO: move *) -lemma norm_le_square: "norm x \ a \ 0 \ a \ inner x x \ a\" -proof - - have "norm x \ a \ 0 \ a \ norm x \ a" - using norm_ge_zero [of x] by arith - also have "\ \ 0 \ a \ (norm x)\ \ a\" - by (auto intro: power_mono dest: power2_le_imp_le) - also have "\ \ 0 \ a \ inner x x \ a\" - unfolding power2_norm_eq_inner .. - finally show ?thesis . -qed - lemma any_closest_point_unique: fixes s :: "(real ^ _) set" assumes "convex s" "closed s" "x \ s" "y \ s" @@ -1658,7 +1629,7 @@ lemma continuous_on_closest_point: assumes "convex s" "closed s" "s \ {}" shows "continuous_on t (closest_point s)" - apply(rule continuous_at_imp_continuous_on) using continuous_at_closest_point[OF assms] by auto +by(metis continuous_at_imp_continuous_on continuous_at_closest_point[OF assms]) subsection {* Various point-to-set separating/supporting hyperplane theorems. *} @@ -1798,7 +1769,7 @@ prefer 4 apply (rule Sup_least) using assms(3-5) apply (auto simp add: setle_def) - apply (metis COMBC_def Collect_def Collect_mem_eq) + apply metis done qed @@ -1834,8 +1805,7 @@ lemma convex_hull_translation_lemma: "convex hull ((\x. a + x) ` s) \ (\x. a + x) ` (convex hull s)" - apply(rule hull_minimal, rule image_mono, rule hull_subset) unfolding mem_def - using convex_translation[OF convex_convex_hull, of a s] by assumption +by (metis convex_convex_hull convex_translation hull_minimal hull_subset image_mono mem_def) lemma convex_hull_bilemma: fixes neg assumes "(\s a. (convex hull (up a s)) \ up a (convex hull s))" @@ -1849,8 +1819,7 @@ lemma convex_hull_scaling_lemma: "(convex hull ((\x. c *\<^sub>R x) ` s)) \ (\x. c *\<^sub>R x) ` (convex hull s)" - apply(rule hull_minimal, rule image_mono, rule hull_subset) - unfolding mem_def by(rule convex_scaling, rule convex_convex_hull) +by (metis convex_convex_hull convex_scaling hull_subset mem_def subset_hull subset_image_iff) lemma convex_hull_scaling: "convex hull ((\x. c *\<^sub>R x) ` s) = (\x. c *\<^sub>R x) ` (convex hull s)" @@ -1859,7 +1828,7 @@ lemma convex_hull_affinity: "convex hull ((\x. a + c *\<^sub>R x) ` s) = (\x. a + c *\<^sub>R x) ` (convex hull s)" - unfolding image_image[THEN sym] convex_hull_scaling convex_hull_translation .. +by(simp only: image_image[THEN sym] convex_hull_scaling convex_hull_translation) subsection {* Convex set as intersection of halfspaces. *} @@ -2048,8 +2017,8 @@ hence "u + e / 2 / norm x > u" using`norm x > 0` by(auto simp del:zero_less_norm_iff intro!: divide_pos_pos) thus False using u_max[OF _ as] by auto qed(insert `y\s`, auto simp add: dist_norm scaleR_left_distrib obt(3)) - thus ?thesis apply(rule_tac that[of u]) apply(rule obt(1), assumption) - apply(rule,rule,rule ccontr) apply(rule u_max) by auto qed + thus ?thesis by(metis that[of u] u_max obt(1)) +qed lemma starlike_compact_projective: assumes "compact s" "cball (0::real^'n) 1 \ s " @@ -2251,11 +2220,13 @@ apply(erule_tac x=xa in allE,erule_tac x="f xa" in allE) prefer 3 apply(rule_tac y="u * f x + v * f xb" in order_trans) defer by(auto intro!:mult_left_mono add_mono) -lemma convex_epigraphI: assumes "convex_on s f" "convex s" - shows "convex(epigraph s f)" using assms unfolding convex_epigraph by auto - -lemma convex_epigraph_convex: "convex s \ (convex_on s f \ convex(epigraph s f))" - using convex_epigraph by auto +lemma convex_epigraphI: + "convex_on s f \ convex s \ convex(epigraph s f)" +unfolding convex_epigraph by auto + +lemma convex_epigraph_convex: + "convex s \ convex_on s f \ convex(epigraph s f)" +by(simp add: convex_epigraph) subsection {* Use this to derive general bound property of convex function. *} @@ -2335,16 +2306,16 @@ hence "?halfl \ s \ {}" "?halfr \ s \ {}" using as(2-3) by auto ultimately show False apply(rule_tac notE[OF as(1)[unfolded connected_def]]) apply(rule_tac x="?halfl" in exI, rule_tac x="?halfr" in exI) - apply(rule, rule open_halfspace_lt, rule, rule open_halfspace_gt) apply(rule, rule, rule ccontr) - by(auto simp add: basis_component field_simps) qed + apply(rule, rule open_halfspace_lt, rule, rule open_halfspace_gt) + by(auto simp add: field_simps) qed lemma is_interval_convex_1: "is_interval s \ convex (s::(real^1) set)" - using is_interval_convex convex_connected is_interval_connected_1 by auto +by(metis is_interval_convex convex_connected is_interval_connected_1) lemma convex_connected_1: "connected s \ convex (s::(real^1) set)" - using is_interval_convex convex_connected is_interval_connected_1 by auto +by(metis is_interval_convex convex_connected is_interval_connected_1) subsection {* Another intermediate value theorem formulation. *} @@ -2358,10 +2329,10 @@ using assms by(auto intro!: imageI) qed lemma ivt_increasing_component_1: fixes f::"real^1 \ real^'n" - assumes "dest_vec1 a \ dest_vec1 b" - "\x\{a .. b}. continuous (at x) f" "f a$k \ y" "y \ f b$k" - shows "\x\{a..b}. (f x)$k = y" - apply(rule ivt_increasing_component_on_1) using assms using continuous_at_imp_continuous_on by auto + shows "dest_vec1 a \ dest_vec1 b \ \x\{a .. b}. continuous (at x) f + \ f a$k \ y \ y \ f b$k \ \x\{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 \ real^'n" assumes "dest_vec1 a \ dest_vec1 b" "continuous_on {a .. b} f" "(f b)$k \ y" "y \ (f a)$k" @@ -2371,9 +2342,10 @@ by(auto simp add:vector_uminus_component) lemma ivt_decreasing_component_1: fixes f::"real^1 \ real^'n" - assumes "dest_vec1 a \ dest_vec1 b" "\x\{a .. b}. continuous (at x) f" "f b$k \ y" "y \ f a$k" - shows "\x\{a..b}. (f x)$k = y" - apply(rule ivt_decreasing_component_on_1) using assms using continuous_at_imp_continuous_on by auto + shows "dest_vec1 a \ dest_vec1 b \ \x\{a .. b}. continuous (at x) f + \ f b$k \ y \ y \ f a$k \ \x\{a..b}. (f x)$k = y" +by(rule ivt_decreasing_component_on_1) + (auto simp: continuous_at_imp_continuous_on) subsection {* A bound within a convex hull, and so an interval. *} @@ -2560,13 +2532,13 @@ let ?d = "(\ i. d)::real^'n" obtain c where c:"finite c" "{x - ?d..x + ?d} = convex hull c" using cube_convex_hull[OF `d>0`, of x] by auto have "x\{x - ?d..x + ?d}" using `d>0` unfolding mem_interval by(auto simp add:vector_component_simps) - hence "c\{}" apply(rule_tac ccontr) using c by(auto simp add:convex_hull_empty) + hence "c\{}" using c by(auto simp add:convex_hull_empty) def k \ "Max (f ` c)" have "convex_on {x - ?d..x + ?d} f" apply(rule convex_on_subset[OF assms(2)]) apply(rule subset_trans[OF _ e(1)]) unfolding subset_eq mem_cball proof fix z assume z:"z\{x - ?d..x + ?d}" have e:"e = setsum (\i. d) (UNIV::'n set)" unfolding setsum_constant d_def using dimge1 - by (metis card_enum field_simps d_def not_one_le_zero of_nat_le_iff real_eq_of_nat real_of_nat_1) + by (metis eq_divide_imp mult_frac_num real_dimindex_gt_0 real_eq_of_nat real_less_def real_mult_commute) show "dist x z \ e" unfolding dist_norm e apply(rule_tac order_trans[OF norm_le_l1], rule setsum_mono) using z[unfolded mem_interval] apply(erule_tac x=i in allE) by(auto simp add:field_simps vector_component_simps) qed hence k:"\y\{x - ?d..x + ?d}. f y \ k" unfolding c(2) apply(rule_tac convex_on_convex_hull_bound) apply assumption @@ -3021,7 +2993,7 @@ using xy(1,2)[unfolded mem_interval_1] by(auto simp add:vector_component_simps intro!: imageI) 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] - apply(rule_tac ccontr) by(auto simp add:vector_component_simps field_simps Cart_eq) + by(auto simp add:vector_component_simps field_simps Cart_eq) 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) @@ -3034,7 +3006,7 @@ using xy(1,2)[unfolded mem_interval_1] by(auto simp add:vector_component_simps intro!: imageI) 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] - apply(rule_tac ccontr) by(auto simp add:vector_component_simps field_simps Cart_eq) + by(auto simp add:vector_component_simps field_simps Cart_eq) 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) @@ -3336,12 +3308,12 @@ by(auto simp add: inner_basis vector_component_simps intro!:bexI[where x=k]) show ?thesis unfolding * Un_assoc apply(rule path_connected_Un) defer apply(rule path_connected_Un) prefer 5 apply(rule_tac[1-2] convex_imp_path_connected, rule convex_halfspace_lt, rule convex_halfspace_gt) - apply(rule Suc(1)) apply(rule_tac[2-3] ccontr) using d ** False by auto + apply(rule Suc(1)) using d ** False by auto next case True hence d:"1\{1..CARD('n)}" "2\{1..CARD('n)}" using Suc(2) by auto have ***:"Suc 1 = 2" by auto have **:"\s t P Q. s \ t \ {x. P x \ Q x} = (s \ {x. P x}) \ (t \ {x. Q x})" by auto have nequals0I:"\x A. x\A \ A \ {}" by auto - have "\ 2 \ \ (Suc 0)" apply(rule ccontr) using \[unfolded bij_betw_def inj_on_def, THEN conjunct1, THEN bspec[where x=2]] using assms by auto + have "\ 2 \ \ (Suc 0)" using \[unfolded bij_betw_def inj_on_def, THEN conjunct1, THEN bspec[where x=2]] using assms by auto thus ?thesis unfolding * True unfolding ** neq_iff bex_disj_distrib apply - apply(rule path_connected_Un, rule_tac[1-2] path_connected_Un) defer 3 apply(rule_tac[1-4] convex_imp_path_connected) apply(rule_tac[5] x=" ?basis 1 + ?basis 2" in nequals0I)