# HG changeset patch # User paulson # Date 1525033617 -3600 # Node ID 9e077a90520957bfeeacdedbff1bed13b6ba8c7d # Parent 2cab37094fc451cb49076c0950e10749f57f454b cleaned up more messy proofs diff -r 2cab37094fc4 -r 9e077a905209 src/HOL/Analysis/Starlike.thy --- a/src/HOL/Analysis/Starlike.thy Sun Apr 29 14:46:11 2018 +0100 +++ b/src/HOL/Analysis/Starlike.thy Sun Apr 29 21:26:57 2018 +0100 @@ -19,10 +19,7 @@ where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)" lemma midpoint_idem [simp]: "midpoint x x = x" - unfolding midpoint_def - unfolding scaleR_right_distrib - unfolding scaleR_left_distrib[symmetric] - by auto + unfolding midpoint_def by simp lemma midpoint_sym: "midpoint a b = midpoint b a" unfolding midpoint_def by (auto simp add: scaleR_right_distrib) @@ -924,61 +921,49 @@ proof (cases "a = b") case True then show ?thesis - unfolding between_def split_conv - by (auto simp add: dist_commute) + by (auto simp add: between_def dist_commute) next case False then have Fal: "norm (a - b) \ 0" and Fal2: "norm (a - b) > 0" by auto have *: "\u. a - ((1 - u) *\<^sub>R a + u *\<^sub>R b) = u *\<^sub>R (a - b)" by (auto simp add: algebra_simps) - show ?thesis - unfolding between_def split_conv closed_segment_def mem_Collect_eq - apply rule - apply (elim exE conjE) - apply (subst dist_triangle_eq) + have "norm (a - x) *\<^sub>R (x - b) = norm (x - b) *\<^sub>R (a - x)" if "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \ u" "u \ 1" for u proof - - fix u - assume as: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \ u" "u \ 1" - then have *: "a - x = u *\<^sub>R (a - b)" "x - b = (1 - u) *\<^sub>R (a - b)" - unfolding as(1) by (auto simp add:algebra_simps) + have *: "a - x = u *\<^sub>R (a - b)" "x - b = (1 - u) *\<^sub>R (a - b)" + unfolding that(1) by (auto simp add:algebra_simps) show "norm (a - x) *\<^sub>R (x - b) = norm (x - b) *\<^sub>R (a - x)" - unfolding norm_minus_commute[of x a] * using as(2,3) + unfolding norm_minus_commute[of x a] * using \0 \ u\ \u \ 1\ by (auto simp add: field_simps) - next - assume as: "dist a b = dist a x + dist x b" - have "norm (a - x) / norm (a - b) \ 1" - using Fal2 unfolding as[unfolded dist_norm] norm_ge_zero by auto - then show "\u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \ 0 \ u \ u \ 1" - apply (rule_tac x="dist a x / dist a b" in exI) - unfolding dist_norm - apply (subst euclidean_eq_iff) - apply rule - defer - apply rule - prefer 3 - apply rule - proof - - fix i :: 'a - assume i: "i \ Basis" - have "((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) \ i = - ((norm (a - b) - norm (a - x)) * (a \ i) + norm (a - x) * (b \ i)) / norm (a - b)" - using Fal by (auto simp add: field_simps inner_simps) - also have "\ = x\i" - apply (rule divide_eq_imp[OF Fal]) - unfolding as[unfolded dist_norm] - using as[unfolded dist_triangle_eq] - apply - - apply (subst (asm) euclidean_eq_iff) - using i - apply (erule_tac x=i in ballE) - apply (auto simp add: field_simps inner_simps) - done - finally show "x \ i = - ((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) \ i" - by auto - qed (insert Fal2, auto) qed + moreover have "\u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \ 0 \ u \ u \ 1" if "dist a b = dist a x + dist x b" + proof - + let ?\ = "norm (a - x) / norm (a - b)" + show "\u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \ 0 \ u \ u \ 1" + proof (intro exI conjI) + show "?\ \ 1" + using Fal2 unfolding that[unfolded dist_norm] norm_ge_zero by auto + show "x = (1 - ?\) *\<^sub>R a + (?\) *\<^sub>R b" + proof (subst euclidean_eq_iff; intro ballI) + fix i :: 'a + assume i: "i \ Basis" + have "((1 - ?\) *\<^sub>R a + (?\) *\<^sub>R b) \ i + = ((norm (a - b) - norm (a - x)) * (a \ i) + norm (a - x) * (b \ i)) / norm (a - b)" + using Fal by (auto simp add: field_simps inner_simps) + also have "\ = x\i" + apply (rule divide_eq_imp[OF Fal]) + unfolding that[unfolded dist_norm] + using that[unfolded dist_triangle_eq] i + apply (subst (asm) euclidean_eq_iff) + apply (auto simp add: field_simps inner_simps) + done + finally show "x \ i = ((1 - ?\) *\<^sub>R a + (?\) *\<^sub>R b) \ i" + by auto + qed + qed (use Fal2 in auto) + qed + ultimately show ?thesis + by (force simp add: between_def closed_segment_def dist_triangle_eq) qed lemma between_midpoint: @@ -990,10 +975,7 @@ by auto show ?t1 ?t2 unfolding between midpoint_def dist_norm - apply(rule_tac[!] *) - unfolding euclidean_eq_iff[where 'a='a] - apply (auto simp add: field_simps inner_simps) - done + by (auto simp add: field_simps inner_simps euclidean_eq_iff[where 'a='a] intro!: *) qed lemma between_mem_convex_hull: @@ -1058,25 +1040,23 @@ subsection%unimportant \Shrinking towards the interior of a convex set\ lemma mem_interior_convex_shrink: - fixes s :: "'a::euclidean_space set" - assumes "convex s" - and "c \ interior s" - and "x \ s" + fixes S :: "'a::euclidean_space set" + assumes "convex S" + and "c \ interior S" + and "x \ S" and "0 < e" and "e \ 1" - shows "x - e *\<^sub>R (x - c) \ interior s" -proof - - obtain d where "d > 0" and d: "ball c d \ s" + shows "x - e *\<^sub>R (x - c) \ interior S" +proof - + obtain d where "d > 0" and d: "ball c d \ S" using assms(2) unfolding mem_interior by auto show ?thesis unfolding mem_interior - apply (rule_tac x="e*d" in exI) - apply rule - defer - unfolding subset_eq Ball_def mem_ball - proof (rule, rule) + proof (intro exI subsetI conjI) fix y - assume as: "dist (x - e *\<^sub>R (x - c)) y < e * d" + assume "y \ ball (x - e *\<^sub>R (x - c)) (e*d)" + then have as: "dist (x - e *\<^sub>R (x - c)) y < e * d" + by simp have *: "y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x" using \e > 0\ by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib) have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = \1/e\ * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)" @@ -1090,7 +1070,7 @@ also have "\ < d" using as[unfolded dist_norm] and \e > 0\ by (auto simp add:pos_divide_less_eq[OF \e > 0\] mult.commute) - finally show "y \ s" + finally show "y \ S" apply (subst *) apply (rule assms(1)[unfolded convex_alt,rule_format]) apply (rule d[unfolded subset_eq,rule_format]) @@ -1102,18 +1082,18 @@ qed lemma mem_interior_closure_convex_shrink: - fixes s :: "'a::euclidean_space set" - assumes "convex s" - and "c \ interior s" - and "x \ closure s" + fixes S :: "'a::euclidean_space set" + assumes "convex S" + and "c \ interior S" + and "x \ closure S" and "0 < e" and "e \ 1" - shows "x - e *\<^sub>R (x - c) \ interior s" -proof - - obtain d where "d > 0" and d: "ball c d \ s" + shows "x - e *\<^sub>R (x - c) \ interior S" +proof - + obtain d where "d > 0" and d: "ball c d \ S" using assms(2) unfolding mem_interior by auto - have "\y\s. norm (y - x) * (1 - e) < e * d" - proof (cases "x \ s") + have "\y\S. norm (y - x) * (1 - e) < e * d" + proof (cases "x \ S") case True then show ?thesis using \e > 0\ \d > 0\ @@ -1122,12 +1102,12 @@ done next case False - then have x: "x islimpt s" + then have x: "x islimpt S" using assms(3)[unfolded closure_def] by auto show ?thesis proof (cases "e = 1") case True - obtain y where "y \ s" "y \ x" "dist y x < 1" + obtain y where "y \ S" "y \ x" "dist y x < 1" using x[unfolded islimpt_approachable,THEN spec[where x=1]] by auto then show ?thesis apply (rule_tac x=y in bexI) @@ -1139,7 +1119,7 @@ case False then have "0 < e * d / (1 - e)" and *: "1 - e > 0" using \e \ 1\ \e > 0\ \d > 0\ by auto - then obtain y where "y \ s" "y \ x" "dist y x < e * d / (1 - e)" + then obtain y where "y \ S" "y \ x" "dist y x < e * d / (1 - e)" using x[unfolded islimpt_approachable,THEN spec[where x="e*d / (1 - e)"]] by auto then show ?thesis apply (rule_tac x=y in bexI) @@ -1149,24 +1129,20 @@ done qed qed - then obtain y where "y \ s" and y: "norm (y - x) * (1 - e) < e * d" + then obtain y where "y \ S" and y: "norm (y - x) * (1 - e) < e * d" by auto define z where "z = c + ((1 - e) / e) *\<^sub>R (x - y)" have *: "x - e *\<^sub>R (x - c) = y - e *\<^sub>R (y - z)" unfolding z_def using \e > 0\ by (auto simp add: scaleR_right_diff_distrib scaleR_right_distrib scaleR_left_diff_distrib) - have "z \ interior s" + have "z \ interior S" apply (rule interior_mono[OF d,unfolded subset_eq,rule_format]) unfolding interior_open[OF open_ball] mem_ball z_def dist_norm using y and assms(4,5) apply (auto simp add:field_simps norm_minus_commute) done then show ?thesis unfolding * - apply - - apply (rule mem_interior_convex_shrink) - using assms(1,4-5) \y\s\ - apply auto - done + using mem_interior_convex_shrink \y \ S\ assms by blast qed lemma in_interior_closure_convex_segment: @@ -1252,23 +1228,20 @@ subsection%unimportant \Some obvious but surprisingly hard simplex lemmas\ lemma simplex: - assumes "finite s" - and "0 \ s" - shows "convex hull (insert 0 s) = - {y. (\u. (\x\s. 0 \ u x) \ sum u s \ 1 \ sum (\x. u x *\<^sub>R x) s = y)}" - unfolding convex_hull_finite[OF finite.insertI[OF assms(1)]] - apply (rule set_eqI, rule) - unfolding mem_Collect_eq - apply (erule_tac[!] exE) - apply (erule_tac[!] conjE)+ - unfolding sum_clauses(2)[OF \finite s\] - apply (rule_tac x=u in exI) - defer - apply (rule_tac x="\x. if x = 0 then 1 - sum u s else u x" in exI) - using assms(2) - unfolding if_smult and sum_delta_notmem[OF assms(2)] - apply auto - done + assumes "finite S" + and "0 \ S" + shows "convex hull (insert 0 S) = {y. \u. (\x\S. 0 \ u x) \ sum u S \ 1 \ sum (\x. u x *\<^sub>R x) S = y}" +proof (simp add: convex_hull_finite set_eq_iff assms, safe) + fix x and u :: "'a \ real" + assume "0 \ u 0" "\x\S. 0 \ u x" "u 0 + sum u S = 1" + then show "\v. (\x\S. 0 \ v x) \ sum v S \ 1 \ (\x\S. v x *\<^sub>R x) = (\x\S. u x *\<^sub>R x)" + by force +next + fix x and u :: "'a \ real" + assume "\x\S. 0 \ u x" "sum u S \ 1" + then show "\v. 0 \ v 0 \ (\x\S. 0 \ v x) \ v 0 + sum v S = 1 \ (\x\S. v x *\<^sub>R x) = (\x\S. u x *\<^sub>R x)" + by (rule_tac x="\x. if x = 0 then 1 - sum u S else u x" in exI) (auto simp: sum_delta_notmem assms if_smult) +qed lemma substd_simplex: assumes d: "d \ Basis" @@ -1283,50 +1256,27 @@ by (blast intro: finite_subset finite_Basis) show ?thesis unfolding simplex[OF \finite d\ \0 \ ?p\] - apply (rule set_eqI) - unfolding mem_Collect_eq - apply rule - apply (elim exE conjE) - apply (erule_tac[2] conjE)+ - proof - - fix x :: "'a::euclidean_space" - fix u - assume as: "\x\?D. 0 \ u x" "sum u ?D \ 1" "(\x\?D. u x *\<^sub>R x) = x" - have *: "\i\Basis. i \ d \ u i = x\i" - and "(\i\Basis. i \ d \ x \ i = 0)" - using as(3) - unfolding substdbasis_expansion_unique[OF assms] - by auto - then have **: "sum u ?D = sum ((\) x) ?D" - apply - - apply (rule sum.cong) - using assms - apply auto - done - have "(\i\Basis. 0 \ x\i) \ sum ((\) x) ?D \ 1" - proof (rule,rule) - fix i :: 'a - assume i: "i \ Basis" - have "i \ d \ 0 \ x\i" - unfolding *[rule_format,OF i,symmetric] - apply (rule_tac as(1)[rule_format]) - apply auto - done - moreover have "i \ d \ 0 \ x\i" - using \(\i\Basis. i \ d \ x \ i = 0)\[rule_format, OF i] by auto - ultimately show "0 \ x\i" by auto - qed (insert as(2)[unfolded **], auto) - then show "(\i\Basis. 0 \ x\i) \ sum ((\) x) ?D \ 1 \ (\i\Basis. i \ d \ x \ i = 0)" - using \(\i\Basis. i \ d \ x \ i = 0)\ by auto + proof (intro set_eqI; safe) + fix u :: "'a \ real" + assume as: "\x\?D. 0 \ u x" "sum u ?D \ 1" + let ?x = "(\x\?D. u x *\<^sub>R x)" + have ind: "\i\Basis. i \ d \ u i = ?x \ i" + and notind: "(\i\Basis. i \ d \ ?x \ i = 0)" + using substdbasis_expansion_unique[OF assms] by blast+ + then have **: "sum u ?D = sum ((\) ?x) ?D" + using assms by (auto intro!: sum.cong) + show "0 \ ?x \ i" if "i \ Basis" for i + using as(1) ind notind that by fastforce + show "sum ((\) ?x) ?D \ 1" + using "**" as(2) by linarith + show "?x \ i = 0" if "i \ Basis" "i \ d" for i + using notind that by blast next - fix x :: "'a::euclidean_space" - assume as: "\i\Basis. 0 \ x \ i" "sum ((\) x) ?D \ 1" "(\i\Basis. i \ d \ x \ i = 0)" - show "\u. (\x\?D. 0 \ u x) \ sum u ?D \ 1 \ (\x\?D. u x *\<^sub>R x) = x" - using as d - unfolding substdbasis_expansion_unique[OF assms] - apply (rule_tac x="inner x" in exI) - apply auto - done + fix x + assume "\i\Basis. 0 \ x \ i" "sum ((\) x) ?D \ 1" "(\i\Basis. i \ d \ x \ i = 0)" + with d show "\u. (\x\?D. 0 \ u x) \ sum u ?D \ 1 \ (\x\?D. u x *\<^sub>R x) = x" + unfolding substdbasis_expansion_unique[OF assms] + by (rule_tac x="inner x" in exI) auto qed qed @@ -1338,27 +1288,18 @@ lemma interior_std_simplex: "interior (convex hull (insert 0 Basis)) = {x::'a::euclidean_space. (\i\Basis. 0 < x\i) \ sum (\i. x\i) Basis < 1}" - apply (rule set_eqI) - unfolding mem_interior std_simplex - unfolding subset_eq mem_Collect_eq Ball_def mem_ball - unfolding Ball_def[symmetric] - apply rule - apply (elim exE conjE) - defer - apply (erule conjE) -proof - + unfolding set_eq_iff mem_interior std_simplex +proof (intro allI iffI CollectI; clarify) fix x :: 'a fix e - assume "e > 0" and as: "\xa. dist x xa < e \ (\x\Basis. 0 \ xa \ x) \ sum ((\) xa) Basis \ 1" - show "(\xa\Basis. 0 < x \ xa) \ sum ((\) x) Basis < 1" - apply safe - proof - + assume "e > 0" and as: "ball x e \ {x. (\i\Basis. 0 \ x \ i) \ sum ((\) x) Basis \ 1}" + show "(\i\Basis. 0 < x \ i) \ sum ((\) x) Basis < 1" + proof safe fix i :: 'a assume i: "i \ Basis" then show "0 < x \ i" - using as[THEN spec[where x="x - (e / 2) *\<^sub>R i"]] and \e > 0\ - unfolding dist_norm - by (auto elim!: ballE[where x=i] simp: inner_simps) + using as[THEN subsetD[where c="x - (e / 2) *\<^sub>R i"]] and \e > 0\ + by (force simp add: inner_simps) next have **: "dist x (x + (e / 2) *\<^sub>R (SOME i. i\Basis)) < e" using \e > 0\ unfolding dist_norm @@ -1368,42 +1309,31 @@ by (auto simp: SOME_Basis inner_Basis inner_simps) then have *: "sum ((\) (x + (e / 2) *\<^sub>R (SOME i. i\Basis))) Basis = sum (\i. x\i + (if (SOME i. i\Basis) = i then e/2 else 0)) Basis" - apply (rule_tac sum.cong) - apply auto - done + by (auto simp: intro!: sum.cong) have "sum ((\) x) Basis < sum ((\) (x + (e / 2) *\<^sub>R (SOME i. i\Basis))) Basis" - unfolding * sum.distrib - using \e > 0\ DIM_positive[where 'a='a] - apply (subst sum.delta') - apply (auto simp: SOME_Basis) - done + using \e > 0\ DIM_positive by (auto simp: SOME_Basis sum.distrib *) also have "\ \ 1" - using ** - apply (drule_tac as[rule_format]) - apply auto - done + using ** as by force finally show "sum ((\) x) Basis < 1" by auto - qed + qed next fix x :: 'a assume as: "\i\Basis. 0 < x \ i" "sum ((\) x) Basis < 1" obtain a :: 'b where "a \ UNIV" using UNIV_witness .. let ?d = "(1 - sum ((\) x) Basis) / real (DIM('a))" - show "\e>0. \y. dist x y < e \ (\i\Basis. 0 \ y \ i) \ sum ((\) y) Basis \ 1" - proof (rule_tac x="min (Min (((\) x) ` Basis)) D" for D in exI, intro conjI impI allI) + show "\e>0. ball x e \ {x. (\i\Basis. 0 \ x \ i) \ sum ((\) x) Basis \ 1}" + proof (rule_tac x="min (Min (((\) x) ` Basis)) D" for D in exI, intro conjI subsetI CollectI) fix y - assume y: "dist x y < min (Min ((\) x ` Basis)) ?d" + assume y: "y \ ball x (min (Min ((\) x ` Basis)) ?d)" have "sum ((\) y) Basis \ sum (\i. x\i + ?d) Basis" proof (rule sum_mono) fix i :: 'a assume i: "i \ Basis" - then have "\y\i - x\i\ < ?d" - apply - - apply (rule le_less_trans) - using Basis_le_norm[OF i, of "y - x"] - using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2] - apply (auto simp add: norm_minus_commute inner_diff_left) - done + have "\y\i - x\i\ \ norm (y - x)" + by (metis Basis_le_norm i inner_commute inner_diff_right) + also have "... < ?d" + using y by (simp add: dist_norm norm_minus_commute) + finally have "\y\i - x\i\ < ?d" . then show "y \ i \ x \ i + ?d" by auto qed also have "\ \ 1" @@ -1414,12 +1344,11 @@ proof safe fix i :: 'a assume i: "i \ Basis" - have "norm (x - y) < x\i" - apply (rule less_le_trans) - apply (rule y[unfolded min_less_iff_conj dist_norm, THEN conjunct1]) - using i - apply auto - done + have "norm (x - y) < MINIMUM Basis ((\) x)" + using y by (auto simp: dist_norm less_eq_real_def) + also have "... \ x\i" + using i by auto + finally have "norm (x - y) < x\i" . then show "0 \ y\i" using Basis_le_norm[OF i, of "x - y"] and as(1)[rule_format, OF i] by (auto simp: inner_simps) @@ -1469,82 +1398,70 @@ qed lemma rel_interior_substd_simplex: - assumes d: "d \ Basis" - shows "rel_interior (convex hull (insert 0 d)) = - {x::'a::euclidean_space. (\i\d. 0 < x\i) \ (\i\d. x\i) < 1 \ (\i\Basis. i \ d \ x\i = 0)}" + assumes D: "D \ Basis" + shows "rel_interior (convex hull (insert 0 D)) = + {x::'a::euclidean_space. (\i\D. 0 < x\i) \ (\i\D. x\i) < 1 \ (\i\Basis. i \ D \ x\i = 0)}" (is "rel_interior (convex hull (insert 0 ?p)) = ?s") proof - - have "finite d" - apply (rule finite_subset) - using assms - apply auto - done + have "finite D" + using D finite_Basis finite_subset by blast show ?thesis - proof (cases "d = {}") + proof (cases "D = {}") case True then show ?thesis using rel_interior_sing using euclidean_eq_iff[of _ 0] by auto next case False have h0: "affine hull (convex hull (insert 0 ?p)) = - {x::'a::euclidean_space. (\i\Basis. i \ d \ x\i = 0)}" + {x::'a::euclidean_space. (\i\Basis. i \ D \ x\i = 0)}" using affine_hull_convex_hull affine_hull_substd_basis assms by auto - have aux: "\x::'a. \i\Basis. (\i\d. 0 \ x\i) \ (\i\Basis. i \ d \ x\i = 0) \ 0 \ x\i" + have aux: "\x::'a. \i\Basis. (\i\D. 0 \ x\i) \ (\i\Basis. i \ D \ x\i = 0) \ 0 \ x\i" by auto { fix x :: "'a::euclidean_space" assume x: "x \ rel_interior (convex hull (insert 0 ?p))" - then obtain e where e0: "e > 0" and - "ball x e \ {xa. (\i\Basis. i \ d \ xa\i = 0)} \ convex hull (insert 0 ?p)" + then obtain e where "e > 0" and + "ball x e \ {xa. (\i\Basis. i \ D \ xa\i = 0)} \ convex hull (insert 0 ?p)" using mem_rel_interior_ball[of x "convex hull (insert 0 ?p)"] h0 by auto - then have as: "\xa. dist x xa < e \ (\i\Basis. i \ d \ xa\i = 0) \ - (\i\d. 0 \ xa \ i) \ sum ((\) xa) d \ 1" + then have as [rule_format]: "\y. dist x y < e \ (\i\Basis. i \ D \ y\i = 0) \ + (\i\D. 0 \ y \ i) \ sum ((\) y) D \ 1" unfolding ball_def unfolding substd_simplex[OF assms] using assms by auto - have x0: "(\i\Basis. i \ d \ x\i = 0)" + have x0: "(\i\Basis. i \ D \ x\i = 0)" using x rel_interior_subset substd_simplex[OF assms] by auto - have "(\i\d. 0 < x \ i) \ sum ((\) x) d < 1 \ (\i\Basis. i \ d \ x\i = 0)" - apply rule - apply rule - proof - + have "(\i\D. 0 < x \ i) \ sum ((\) x) D < 1 \ (\i\Basis. i \ D \ x\i = 0)" + proof (intro conjI ballI) fix i :: 'a - assume "i \ d" - then have "\ia\d. 0 \ (x - (e / 2) *\<^sub>R i) \ ia" + assume "i \ D" + then have "\j\D. 0 \ (x - (e / 2) *\<^sub>R i) \ j" apply - - apply (rule as[rule_format,THEN conjunct1]) - unfolding dist_norm - using d \e > 0\ x0 - apply (auto simp: inner_simps inner_Basis) + apply (rule as[THEN conjunct1]) + using D \e > 0\ x0 + apply (auto simp: dist_norm inner_simps inner_Basis) done then show "0 < x \ i" - apply (erule_tac x=i in ballE) - using \e > 0\ \i \ d\ d - apply (auto simp: inner_simps inner_Basis) - done + using \e > 0\ \i \ D\ D by (force simp: inner_simps inner_Basis) next - obtain a where a: "a \ d" - using \d \ {}\ by auto + obtain a where a: "a \ D" + using \D \ {}\ by auto then have **: "dist x (x + (e / 2) *\<^sub>R a) < e" - using \e > 0\ norm_Basis[of a] d + using \e > 0\ norm_Basis[of a] D unfolding dist_norm by auto have "\i. i \ Basis \ (x + (e / 2) *\<^sub>R a) \ i = x\i + (if i = a then e/2 else 0)" - using a d by (auto simp: inner_simps inner_Basis) - then have *: "sum ((\) (x + (e / 2) *\<^sub>R a)) d = - sum (\i. x\i + (if a = i then e/2 else 0)) d" - using d by (intro sum.cong) auto + using a D by (auto simp: inner_simps inner_Basis) + then have *: "sum ((\) (x + (e / 2) *\<^sub>R a)) D = + sum (\i. x\i + (if a = i then e/2 else 0)) D" + using D by (intro sum.cong) auto have "a \ Basis" - using \a \ d\ d by auto - then have h1: "(\i\Basis. i \ d \ (x + (e / 2) *\<^sub>R a) \ i = 0)" - using x0 d \a\d\ by (auto simp add: inner_add_left inner_Basis) - have "sum ((\) x) d < sum ((\) (x + (e / 2) *\<^sub>R a)) d" - unfolding * sum.distrib - using \e > 0\ \a \ d\ - using \finite d\ - by (auto simp add: sum.delta') + using \a \ D\ D by auto + then have h1: "(\i\Basis. i \ D \ (x + (e / 2) *\<^sub>R a) \ i = 0)" + using x0 D \a\D\ by (auto simp add: inner_add_left inner_Basis) + have "sum ((\) x) D < sum ((\) (x + (e / 2) *\<^sub>R a)) D" + using \e > 0\ \a \ D\ \finite D\ by (auto simp add: * sum.distrib) also have "\ \ 1" using ** h1 as[rule_format, of "x + (e / 2) *\<^sub>R a"] by auto - finally show "sum ((\) x) d < 1 \ (\i\Basis. i \ d \ x\i = 0)" + finally show "sum ((\) x) D < 1" "\i. i\Basis \ i \ D \ x\i = 0" using x0 by auto qed } @@ -1554,63 +1471,62 @@ assume as: "x \ ?s" have "\i. 0 < x\i \ 0 = x\i \ 0 \ x\i" by auto - moreover have "\i. i \ d \ i \ d" by auto + moreover have "\i. i \ D \ i \ D" by auto ultimately - have "\i. (\i\d. 0 < x\i) \ (\i. i \ d \ x\i = 0) \ 0 \ x\i" + have "\i. (\i\D. 0 < x\i) \ (\i. i \ D \ x\i = 0) \ 0 \ x\i" by metis then have h2: "x \ convex hull (insert 0 ?p)" using as assms unfolding substd_simplex[OF assms] by fastforce - obtain a where a: "a \ d" - using \d \ {}\ by auto - let ?d = "(1 - sum ((\) x) d) / real (card d)" - have "0 < card d" using \d \ {}\ \finite d\ + obtain a where a: "a \ D" + using \D \ {}\ by auto + let ?d = "(1 - sum ((\) x) D) / real (card D)" + have "0 < card D" using \D \ {}\ \finite D\ by (simp add: card_gt_0_iff) - have "Min (((\) x) ` d) > 0" - using as \d \ {}\ \finite d\ by (simp add: Min_gr_iff) - moreover have "?d > 0" using as using \0 < card d\ by auto - ultimately have h3: "min (Min (((\) x) ` d)) ?d > 0" + have "Min (((\) x) ` D) > 0" + using as \D \ {}\ \finite D\ by (simp add: Min_gr_iff) + moreover have "?d > 0" using as using \0 < card D\ by auto + ultimately have h3: "min (Min (((\) x) ` D)) ?d > 0" by auto have "x \ rel_interior (convex hull (insert 0 ?p))" unfolding rel_interior_ball mem_Collect_eq h0 apply (rule,rule h2) unfolding substd_simplex[OF assms] - apply (rule_tac x="min (Min (((\) x) ` d)) ?d" in exI) + apply (rule_tac x="min (Min (((\) x) ` D)) ?d" in exI) apply (rule, rule h3) apply safe unfolding mem_ball proof - fix y :: 'a - assume y: "dist x y < min (Min ((\) x ` d)) ?d" - assume y2: "\i\Basis. i \ d \ y\i = 0" - have "sum ((\) y) d \ sum (\i. x\i + ?d) d" + assume y: "dist x y < min (Min ((\) x ` D)) ?d" + assume y2: "\i\Basis. i \ D \ y\i = 0" + have "sum ((\) y) D \ sum (\i. x\i + ?d) D" proof (rule sum_mono) fix i - assume "i \ d" - with d have i: "i \ Basis" + assume "i \ D" + with D have i: "i \ Basis" by auto - have "\y\i - x\i\ < ?d" - apply (rule le_less_trans) - using Basis_le_norm[OF i, of "y - x"] - using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2] - apply (auto simp add: norm_minus_commute inner_simps) - done + have "\y\i - x\i\ \ norm (y - x)" + by (metis i inner_commute inner_diff_right norm_bound_Basis_le order_refl) + also have "... < ?d" + by (metis dist_norm min_less_iff_conj norm_minus_commute y) + finally have "\y\i - x\i\ < ?d" . then show "y \ i \ x \ i + ?d" by auto qed also have "\ \ 1" - unfolding sum.distrib sum_constant using \0 < card d\ + unfolding sum.distrib sum_constant using \0 < card D\ by auto - finally show "sum ((\) y) d \ 1" . + finally show "sum ((\) y) D \ 1" . fix i :: 'a assume i: "i \ Basis" then show "0 \ y\i" - proof (cases "i\d") + proof (cases "i\D") case True have "norm (x - y) < x\i" using y[unfolded min_less_iff_conj dist_norm, THEN conjunct1] - using Min_gr_iff[of "(\) x ` d" "norm (x - y)"] \0 < card d\ \i \ d\ + using Min_gr_iff[of "(\) x ` D" "norm (x - y)"] \0 < card D\ \i \ D\ by (simp add: card_gt_0_iff) then show "0 \ y\i" using Basis_le_norm[OF i, of "x - y"] and as(1)[rule_format] @@ -1619,36 +1535,36 @@ qed } ultimately have - "\x. x \ rel_interior (convex hull insert 0 d) \ - x \ {x. (\i\d. 0 < x \ i) \ sum ((\) x) d < 1 \ (\i\Basis. i \ d \ x \ i = 0)}" + "\x. x \ rel_interior (convex hull insert 0 D) \ + x \ {x. (\i\D. 0 < x \ i) \ sum ((\) x) D < 1 \ (\i\Basis. i \ D \ x \ i = 0)}" by blast then show ?thesis by (rule set_eqI) qed qed lemma rel_interior_substd_simplex_nonempty: - assumes "d \ {}" - and "d \ Basis" + assumes "D \ {}" + and "D \ Basis" obtains a :: "'a::euclidean_space" - where "a \ rel_interior (convex hull (insert 0 d))" -proof - - let ?D = d - let ?a = "sum (\b::'a::euclidean_space. inverse (2 * real (card d)) *\<^sub>R b) ?D" - have "finite d" + where "a \ rel_interior (convex hull (insert 0 D))" +proof - + let ?D = D + let ?a = "sum (\b::'a::euclidean_space. inverse (2 * real (card D)) *\<^sub>R b) ?D" + have "finite D" apply (rule finite_subset) using assms(2) apply auto done - then have d1: "0 < real (card d)" - using \d \ {}\ by auto + then have d1: "0 < real (card D)" + using \D \ {}\ by auto { fix i - assume "i \ d" - have "?a \ i = inverse (2 * real (card d))" - apply (rule trans[of _ "sum (\j. if i = j then inverse (2 * real (card d)) else 0) ?D"]) + assume "i \ D" + have "?a \ i = inverse (2 * real (card D))" + apply (rule trans[of _ "sum (\j. if i = j then inverse (2 * real (card D)) else 0) ?D"]) unfolding inner_sum_left apply (rule sum.cong) - using \i \ d\ \finite d\ sum.delta'[of d i "(\k. inverse (2 * real (card d)))"] + using \i \ D\ \finite D\ sum.delta'[of D i "(\k. inverse (2 * real (card D)))"] d1 assms(2) by (auto simp: inner_Basis set_rev_mp[OF _ assms(2)]) } @@ -1658,14 +1574,14 @@ unfolding rel_interior_substd_simplex[OF assms(2)] mem_Collect_eq proof safe fix i - assume "i \ d" - have "0 < inverse (2 * real (card d))" + assume "i \ D" + have "0 < inverse (2 * real (card D))" using d1 by auto - also have "\ = ?a \ i" using **[of i] \i \ d\ + also have "\ = ?a \ i" using **[of i] \i \ D\ by auto finally show "0 < ?a \ i" by auto next - have "sum ((\) ?a) ?D = sum (\i. inverse (2 * real (card d))) ?D" + have "sum ((\) ?a) ?D = sum (\i. inverse (2 * real (card D))) ?D" by (rule sum.cong) (rule refl, rule **) also have "\ < 1" unfolding sum_constant divide_real_def[symmetric] @@ -1673,22 +1589,22 @@ finally show "sum ((\) ?a) ?D < 1" by auto next fix i - assume "i \ Basis" and "i \ d" - have "?a \ span d" - proof (rule span_sum[of d "(\b. b /\<^sub>R (2 * real (card d)))" d]) + assume "i \ Basis" and "i \ D" + have "?a \ span D" + proof (rule span_sum[of D "(\b. b /\<^sub>R (2 * real (card D)))" D]) { fix x :: "'a::euclidean_space" - assume "x \ d" - then have "x \ span d" - using span_superset[of _ "d"] by auto - then have "x /\<^sub>R (2 * real (card d)) \ span d" - using span_mul[of x "d" "(inverse (real (card d)) / 2)"] by auto + assume "x \ D" + then have "x \ span D" + using span_superset[of _ "D"] by auto + then have "x /\<^sub>R (2 * real (card D)) \ span D" + using span_mul[of x "D" "(inverse (real (card D)) / 2)"] by auto } - then show "\x. x\d \ x /\<^sub>R (2 * real (card d)) \ span d" + then show "\x. x\D \ x /\<^sub>R (2 * real (card D)) \ span D" by auto qed then show "?a \ i = 0 " - using \i \ d\ unfolding span_substd_basis[OF assms(2)] using \i \ Basis\ by auto + using \i \ D\ unfolding span_substd_basis[OF assms(2)] using \i \ Basis\ by auto qed qed @@ -1916,10 +1832,7 @@ proof - define e where "e = a / (a + b)" have "z = (1 / (a + b)) *\<^sub>R ((a + b) *\<^sub>R z)" - apply auto - using assms - apply simp - done + using assms by (simp add: eq_vector_fraction_iff) also have "\ = (1 / (a + b)) *\<^sub>R (a *\<^sub>R x + b *\<^sub>R y)" using assms scaleR_cancel_left[of "1/(a+b)" "(a + b) *\<^sub>R z" "a *\<^sub>R x + b *\<^sub>R y"] by auto @@ -2089,9 +2002,8 @@ lemma rel_frontier_eq_empty: fixes S :: "'n::euclidean_space set" shows "rel_frontier S = {} \ affine S" - apply (simp add: rel_frontier_def) - apply (simp add: rel_interior_eq_closure [symmetric]) - using rel_interior_subset_closure by blast + unfolding rel_frontier_def + using rel_interior_subset_closure by (auto simp add: rel_interior_eq_closure [symmetric]) lemma rel_frontier_sing [simp]: fixes a :: "'n::euclidean_space" @@ -2365,16 +2277,12 @@ shows "z \ interior S \ (\x. \e. e > 0 \ z + e *\<^sub>R x \ S)" proof (cases "aff_dim S = int DIM('n)") case False - { - assume "z \ interior S" + { assume "z \ interior S" then have False - using False interior_rel_interior_gen[of S] by auto - } + using False interior_rel_interior_gen[of S] by auto } moreover - { - assume r: "\x. \e. e > 0 \ z + e *\<^sub>R x \ S" - { - fix x + { assume r: "\x. \e. e > 0 \ z + e *\<^sub>R x \ S" + { fix x obtain e1 where e1: "e1 > 0 \ z + e1 *\<^sub>R (x - z) \ S" using r by auto obtain e2 where e2: "e2 > 0 \ z + e2 *\<^sub>R (z - x) \ S" @@ -3679,13 +3587,7 @@ then have "x = (\i\I. c i *\<^sub>R s i) \ sum c I = 1" using k by (simp add: sum_prod) then have "x \ ?rhs" - using k - apply auto - apply (rule_tac x = c in exI) - apply (rule_tac x = s in exI) - using cs - apply auto - done + using k cs by auto } moreover { @@ -3709,7 +3611,7 @@ done then have "x \ ?lhs" using K0_def C0_def rel_interior_convex_cone_aux[of C0 1 x] - by (auto simp add: convex_convex_hull) + by auto } ultimately show ?thesis by blast qed @@ -5105,10 +5007,7 @@ "S \ S'" "T \ T'" "S' \ T' = {}" proof (cases "S = {} \ T = {}") case True with that show ?thesis - apply safe - using UT closedin_subset apply blast - using US closedin_subset apply blast - done + using UT US by (blast dest: closedin_subset) next case False define f where "f \ \x. setdist {x} T - setdist {x} S"