--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Tue Apr 24 14:17:58 2018 +0000
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Tue Apr 24 22:22:08 2018 +0100
@@ -111,7 +111,7 @@
then have "span (cball 0 e) = (UNIV :: 'n::euclidean_space set)"
by auto
then show ?thesis
- using dim_span[of "cball (0 :: 'n::euclidean_space) e"] by (auto simp add: dim_UNIV)
+ using dim_span[of "cball (0 :: 'n::euclidean_space) e"] by (auto simp: dim_UNIV)
qed
lemma indep_card_eq_dim_span:
@@ -167,8 +167,7 @@
then have "x-a \<in> S" using assms by auto
then have "x \<in> {a + v |v. v \<in> S}"
apply auto
- apply (rule exI[of _ "x-a"])
- apply simp
+ apply (rule exI[of _ "x-a"], simp)
done
then have "x \<in> ((\<lambda>x. a+x) ` S)" by auto
}
@@ -1239,11 +1238,11 @@
with B(4) C(4) have ceq: "card (f ` B) = card C" using d
by simp
have "g ` B = f ` B" using g(2)
- by (auto simp add: image_iff)
+ by (auto simp: image_iff)
also have "\<dots> = C" using card_subset_eq[OF fC f(1) ceq] .
finally have gBC: "g ` B = C" .
have gi: "inj_on g B" using f(2) g(2)
- by (auto simp add: inj_on_def)
+ by (auto simp: inj_on_def)
note g0 = linear_indep_image_lemma[OF g(1) fB, unfolded gBC, OF C(2) gi]
{
fix x y
@@ -1400,7 +1399,7 @@
proof -
have *: "x - y + (y - z) = x - z" by auto
show ?thesis unfolding dist_norm norm_triangle_eq[of "x - y" "y - z", unfolded *]
- by (auto simp add:norm_minus_commute)
+ by (auto simp:norm_minus_commute)
qed
@@ -1416,7 +1415,7 @@
unfolding affine_def by auto
lemma affine_sing [iff]: "affine {x}"
- unfolding affine_alt by (auto simp add: scaleR_left_distrib [symmetric])
+ unfolding affine_alt by (auto simp: scaleR_left_distrib [symmetric])
lemma affine_UNIV [iff]: "affine UNIV"
unfolding affine_def by auto
@@ -1472,7 +1471,7 @@
proof cases
assume "card S = 1"
then obtain a where "S={a}"
- by (auto simp add: card_Suc_eq)
+ by (auto simp: card_Suc_eq)
then show ?thesis
using that by simp
next
@@ -1481,7 +1480,7 @@
by (metis Suc_1 card_1_singletonE card_Suc_eq)
then show ?thesis
using *[of a b] that
- by (auto simp add: sum_clauses(2))
+ by (auto simp: sum_clauses(2))
next
assume "card S > 2"
then show ?thesis using that n_def
@@ -1517,7 +1516,7 @@
unfolding card_Suc_eq by auto
then show ?thesis
using eq1 \<open>S \<subseteq> V\<close>
- by (auto simp add: sum_distrib_left distrib_left intro!: Suc.prems(2)[of a b])
+ by (auto simp: sum_distrib_left distrib_left intro!: Suc.prems(2)[of a b])
qed
have "u x + (1 - u x) = 1 \<Longrightarrow>
u x *\<^sub>R x + (1 - u x) *\<^sub>R ((\<Sum>y\<in>S - {x}. u y *\<^sub>R y) /\<^sub>R (1 - u x)) \<in> V"
@@ -1567,7 +1566,7 @@
using x y
unfolding scaleR_left_distrib scaleR_zero_left if_smult
by (simp add: sum_Un sum.distrib sum.inter_restrict[symmetric] **)
- also have "... = u *\<^sub>R (\<Sum>v\<in>sx. ux v *\<^sub>R v) + v *\<^sub>R (\<Sum>v\<in>sy. uy v *\<^sub>R v)"
+ also have "\<dots> = u *\<^sub>R (\<Sum>v\<in>sx. ux v *\<^sub>R v) + v *\<^sub>R (\<Sum>v\<in>sy. uy v *\<^sub>R v)"
unfolding scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] by blast
finally show "(\<Sum>i\<in>sx \<union> sy. ((if i \<in> sx then u * ux i else 0) + (if i \<in> sy then v * uy i else 0)) *\<^sub>R i)
= u *\<^sub>R (\<Sum>v\<in>sx. ux v *\<^sub>R v) + v *\<^sub>R (\<Sum>v\<in>sy. uy v *\<^sub>R v)" .
@@ -1578,52 +1577,37 @@
lemma affine_hull_finite:
assumes "finite S"
shows "affine hull S = {y. \<exists>u. sum u S = 1 \<and> sum (\<lambda>v. u v *\<^sub>R v) S = y}"
- unfolding affine_hull_explicit and set_eq_iff and mem_Collect_eq
- apply (rule, rule)
- apply (erule exE)+
- apply (erule conjE)+
- defer
- apply (erule exE)
- apply (erule conjE)
-proof -
- fix x u
- assume "sum u S = 1" "(\<Sum>v\<in>S. u v *\<^sub>R v) = x"
- then show "\<exists>sa u. finite sa \<and>
- \<not> (\<forall>x. (x \<in> sa) = (x \<in> {})) \<and> sa \<subseteq> S \<and> sum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = x"
- apply (rule_tac x=S in exI, rule_tac x=u in exI)
- using assms
- apply auto
- done
-next
- fix x t u
- assume "t \<subseteq> S"
- then have *: "S \<inter> t = t"
- by auto
- assume "finite t" "\<not> (\<forall>x. (x \<in> t) = (x \<in> {}))" "sum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = x"
- then show "\<exists>u. sum u S = 1 \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = x"
- apply (rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI)
- unfolding if_smult scaleR_zero_left and sum.inter_restrict[OF assms, symmetric] and *
- apply auto
- done
+proof -
+ have *: "\<exists>h. sum h S = 1 \<and> (\<Sum>v\<in>S. h v *\<^sub>R v) = x"
+ if "F \<subseteq> S" "finite F" "F \<noteq> {}" and sum: "sum u F = 1" and x: "(\<Sum>v\<in>F. u v *\<^sub>R v) = x" for x F u
+ proof -
+ have "S \<inter> F = F"
+ using that by auto
+ show ?thesis
+ proof (intro exI conjI)
+ show "(\<Sum>x\<in>S. if x \<in> F then u x else 0) = 1"
+ by (metis (mono_tags, lifting) \<open>S \<inter> F = F\<close> assms sum.inter_restrict sum)
+ show "(\<Sum>v\<in>S. (if v \<in> F then u v else 0) *\<^sub>R v) = x"
+ by (simp add: if_smult cong: if_cong) (metis (no_types) \<open>S \<inter> F = F\<close> assms sum.inter_restrict x)
+ qed
+ qed
+ show ?thesis
+ unfolding affine_hull_explicit using assms
+ by (fastforce dest: *)
qed
subsubsection%unimportant \<open>Stepping theorems and hence small special cases\<close>
lemma affine_hull_empty[simp]: "affine hull {} = {}"
- by (rule hull_unique) auto
-
-(*could delete: it simply rewrites sum expressions, but it's used twice*)
+ by simp
+
lemma affine_hull_finite_step:
fixes y :: "'a::real_vector"
- shows
- "(\<exists>u. sum u {} = w \<and> sum (\<lambda>x. u x *\<^sub>R x) {} = y) \<longleftrightarrow> w = 0 \<and> y = 0" (is ?th1)
- and
- "finite S \<Longrightarrow>
+ shows "finite S \<Longrightarrow>
(\<exists>u. sum u (insert a S) = w \<and> sum (\<lambda>x. u x *\<^sub>R x) (insert a S) = y) \<longleftrightarrow>
(\<exists>v u. sum u S = w - v \<and> sum (\<lambda>x. u x *\<^sub>R x) S = y - v *\<^sub>R a)" (is "_ \<Longrightarrow> ?lhs = ?rhs")
proof -
- show ?th1 by simp
assume fin: "finite S"
show "?lhs = ?rhs"
proof
@@ -1633,19 +1617,12 @@
show ?rhs
proof (cases "a \<in> S")
case True
- then have *: "insert a S = S" by auto
- show ?thesis
- using u[unfolded *]
- apply(rule_tac x=0 in exI)
- apply auto
- done
+ then show ?thesis
+ using u by (simp add: insert_absorb) (metis diff_zero real_vector.scale_zero_left)
next
case False
- then show ?thesis
- apply (rule_tac x="u a" in exI)
- using u and fin
- apply auto
- done
+ show ?thesis
+ by (rule exI [where x="u a"]) (use u fin False in auto)
qed
next
assume ?rhs
@@ -1656,26 +1633,15 @@
show ?lhs
proof (cases "a \<in> S")
case True
- then show ?thesis
- apply (rule_tac x="\<lambda>x. (if x=a then v else 0) + u x" in exI)
- unfolding sum_clauses(2)[OF fin]
- apply simp
- unfolding scaleR_left_distrib and sum.distrib
- unfolding vu and * and scaleR_zero_left
- apply (auto simp add: sum.delta[OF fin])
- done
+ show ?thesis
+ by (rule exI [where x="\<lambda>x. (if x=a then v else 0) + u x"])
+ (simp add: True scaleR_left_distrib sum.distrib sum_clauses fin vu * cong: if_cong)
next
case False
- then have **:
- "\<And>x. x \<in> S \<Longrightarrow> u x = (if x = a then v else u x)"
- "\<And>x. x \<in> S \<Longrightarrow> u x *\<^sub>R x = (if x = a then v *\<^sub>R x else u x *\<^sub>R x)" by auto
- from False show ?thesis
- apply (rule_tac x="\<lambda>x. if x=a then v else u x" in exI)
- unfolding sum_clauses(2)[OF fin] and * using vu
- using sum.cong [of S _ "\<lambda>x. u x *\<^sub>R x" "\<lambda>x. if x = a then v *\<^sub>R x else u x *\<^sub>R x", OF _ **(2)]
- using sum.cong [of S _ u "\<lambda>x. if x = a then v else u x", OF _ **(1)]
- apply auto
- done
+ then show ?thesis
+ apply (rule_tac x="\<lambda>x. if x=a then v else u x" in exI)
+ apply (simp add: vu sum_clauses(2)[OF fin] *)
+ by (simp add: sum_delta_notmem(3) vu)
qed
qed
qed
@@ -1691,7 +1657,7 @@
have "?lhs = {y. \<exists>u. sum u {a, b} = 1 \<and> (\<Sum>v\<in>{a, b}. u v *\<^sub>R v) = y}"
using affine_hull_finite[of "{a,b}"] by auto
also have "\<dots> = {y. \<exists>v u. u b = 1 - v \<and> u b *\<^sub>R b = y - v *\<^sub>R a}"
- by (simp add: affine_hull_finite_step(2)[of "{b}" a])
+ by (simp add: affine_hull_finite_step[of "{b}" a])
also have "\<dots> = ?rhs" unfolding * by auto
finally show ?thesis by auto
qed
@@ -1706,12 +1672,9 @@
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
- apply (rule_tac x=u in exI)
- apply force
+ apply safe
+ apply (metis add.assoc)
+ apply (rule_tac x=u in exI, force)
done
qed
@@ -1749,62 +1712,57 @@
subsubsection%unimportant \<open>Some relations between affine hull and subspaces\<close>
lemma affine_hull_insert_subset_span:
- "affine hull (insert a s) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> s}}"
- unfolding subset_eq Ball_def
- unfolding affine_hull_explicit span_explicit mem_Collect_eq
- apply (rule, rule)
- apply (erule exE)+
- apply (erule conjE)+
-proof -
- fix x t u
- assume as: "finite t" "t \<noteq> {}" "t \<subseteq> insert a s" "sum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = x"
- have "(\<lambda>x. x - a) ` (t - {a}) \<subseteq> {x - a |x. x \<in> s}"
- using as(3) by auto
- then show "\<exists>v. x = a + v \<and> (\<exists>S u. finite S \<and> S \<subseteq> {x - a |x. x \<in> s} \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = v)"
- apply (rule_tac x="x - a" in exI)
- apply (rule conjI, simp)
- apply (rule_tac x="(\<lambda>x. x - a) ` (t - {a})" in exI)
- apply (rule_tac x="\<lambda>x. u (x + a)" in exI)
- apply (rule conjI) using as(1) apply simp
- apply (erule conjI)
- using as(1)
- apply (simp add: sum.reindex[unfolded inj_on_def] scaleR_right_diff_distrib
- sum_subtractf scaleR_left.sum[symmetric] sum_diff1 scaleR_left_diff_distrib)
- unfolding as
- apply simp
- done
+ "affine hull (insert a S) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> S}}"
+proof -
+ have "\<exists>v T u. x = a + v \<and> (finite T \<and> T \<subseteq> {x - a |x. x \<in> S} \<and> (\<Sum>v\<in>T. u v *\<^sub>R v) = v)"
+ if "finite F" "F \<noteq> {}" "F \<subseteq> insert a S" "sum u F = 1" "(\<Sum>v\<in>F. u v *\<^sub>R v) = x"
+ for x F u
+ proof -
+ have *: "(\<lambda>x. x - a) ` (F - {a}) \<subseteq> {x - a |x. x \<in> S}"
+ using that by auto
+ show ?thesis
+ proof (intro exI conjI)
+ show "finite ((\<lambda>x. x - a) ` (F - {a}))"
+ by (simp add: that(1))
+ show "(\<Sum>v\<in>(\<lambda>x. x - a) ` (F - {a}). u(v+a) *\<^sub>R v) = x-a"
+ by (simp add: sum.reindex[unfolded inj_on_def] algebra_simps
+ sum_subtractf scaleR_left.sum[symmetric] sum_diff1 that)
+ qed (use \<open>F \<subseteq> insert a S\<close> in auto)
+ qed
+ then show ?thesis
+ unfolding affine_hull_explicit span_explicit by auto
qed
lemma affine_hull_insert_span:
- assumes "a \<notin> s"
- shows "affine hull (insert a s) = {a + v | v . v \<in> span {x - a | x. x \<in> s}}"
- apply (rule, rule affine_hull_insert_subset_span)
- unfolding subset_eq Ball_def
- unfolding affine_hull_explicit and mem_Collect_eq
-proof (rule, rule, erule exE, erule conjE)
- fix y v
- assume "y = a + v" "v \<in> span {x - a |x. x \<in> s}"
- then obtain t u where obt: "finite t" "t \<subseteq> {x - a |x. x \<in> s}" "a + (\<Sum>v\<in>t. u v *\<^sub>R v) = y"
- unfolding span_explicit by auto
- define f where "f = (\<lambda>x. x + a) ` t"
- have f: "finite f" "f \<subseteq> s" "(\<Sum>v\<in>f. u (v - a) *\<^sub>R (v - a)) = y - a"
- unfolding f_def using obt by (auto simp add: sum.reindex[unfolded inj_on_def])
- have *: "f \<inter> {a} = {}" "f \<inter> - {a} = f"
- using f(2) assms by auto
- show "\<exists>sa u. finite sa \<and> sa \<noteq> {} \<and> sa \<subseteq> insert a s \<and> sum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = y"
- apply (rule_tac x = "insert a f" in exI)
- apply (rule_tac x = "\<lambda>x. if x=a then 1 - sum (\<lambda>x. u (x - a)) f else u (x - a)" in exI)
- using assms and f
- unfolding sum_clauses(2)[OF f(1)] and if_smult
- unfolding sum.If_cases[OF f(1), of "\<lambda>x. x = a"]
- apply (auto simp add: sum_subtractf scaleR_left.sum algebra_simps *)
- done
+ assumes "a \<notin> S"
+ shows "affine hull (insert a S) = {a + v | v . v \<in> span {x - a | x. x \<in> S}}"
+proof -
+ have *: "\<exists>G u. finite G \<and> G \<noteq> {} \<and> G \<subseteq> insert a S \<and> sum u G = 1 \<and> (\<Sum>v\<in>G. u v *\<^sub>R v) = y"
+ if "v \<in> span {x - a |x. x \<in> S}" "y = a + v" for y v
+ proof -
+ from that
+ obtain T u where u: "finite T" "T \<subseteq> {x - a |x. x \<in> S}" "a + (\<Sum>v\<in>T. u v *\<^sub>R v) = y"
+ unfolding span_explicit by auto
+ define F where "F = (\<lambda>x. x + a) ` T"
+ have F: "finite F" "F \<subseteq> S" "(\<Sum>v\<in>F. u (v - a) *\<^sub>R (v - a)) = y - a"
+ unfolding F_def using u by (auto simp: sum.reindex[unfolded inj_on_def])
+ have *: "F \<inter> {a} = {}" "F \<inter> - {a} = F"
+ using F assms by auto
+ show "\<exists>G u. finite G \<and> G \<noteq> {} \<and> G \<subseteq> insert a S \<and> sum u G = 1 \<and> (\<Sum>v\<in>G. u v *\<^sub>R v) = y"
+ apply (rule_tac x = "insert a F" in exI)
+ apply (rule_tac x = "\<lambda>x. if x=a then 1 - sum (\<lambda>x. u (x - a)) F else u (x - a)" in exI)
+ using assms F
+ apply (auto simp: sum_clauses sum.If_cases if_smult sum_subtractf scaleR_left.sum algebra_simps *)
+ done
+ qed
+ show ?thesis
+ by (intro subset_antisym affine_hull_insert_subset_span) (auto simp: affine_hull_explicit dest!: *)
qed
lemma affine_hull_span:
- assumes "a \<in> s"
- shows "affine hull s = {a + v | v. v \<in> span {x - a | x. x \<in> s - {a}}}"
- using affine_hull_insert_span[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto
+ assumes "a \<in> S"
+ shows "affine hull S = {a + v | v. v \<in> span {x - a | x. x \<in> S - {a}}}"
+ using affine_hull_insert_span[of a "S - {a}", unfolded insert_Diff[OF assms]] by auto
subsubsection%unimportant \<open>Parallel affine sets\<close>
@@ -1814,17 +1772,12 @@
lemma affine_parallel_expl_aux:
fixes S T :: "'a::real_vector set"
- assumes "\<forall>x. x \<in> S \<longleftrightarrow> a + x \<in> T"
+ assumes "\<And>x. x \<in> S \<longleftrightarrow> a + x \<in> T"
shows "T = (\<lambda>x. a + x) ` S"
proof -
- {
- fix x
- assume "x \<in> T"
- then have "( - a) + x \<in> S"
- using assms by auto
- then have "x \<in> ((\<lambda>x. a + x) ` S)"
- using imageI[of "-a+x" S "(\<lambda>x. a+x)"] by auto
- }
+ have "x \<in> ((\<lambda>x. a + x) ` S)" if "x \<in> T" for x
+ using that
+ by (simp add: image_iff) (metis add.commute diff_add_cancel assms)
moreover have "T \<ge> (\<lambda>x. a + x) ` S"
using assms by auto
ultimately show ?thesis by auto
@@ -1836,9 +1789,7 @@
lemma affine_parallel_reflex: "affine_parallel S S"
unfolding affine_parallel_def
- apply (rule exI[of _ "0"])
- apply auto
- done
+ using image_add_0 by blast
lemma affine_parallel_commut:
assumes "affine_parallel A B"
@@ -2154,7 +2105,7 @@
shows "c *\<^sub>R x \<in> cone hull S"
by (metis assms cone_cone_hull hull_inc mem_cone)
-lemma%important cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \<ge> 0 \<and> x \<in> S}"
+proposition%important cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \<ge> 0 \<and> x \<in> S}"
(is "?lhs = ?rhs")
proof%unimportant -
{
@@ -2180,8 +2131,7 @@
assume "x \<in> S"
then have "1 *\<^sub>R x \<in> ?rhs"
apply auto
- apply (rule_tac x = 1 in exI)
- apply auto
+ apply (rule_tac x = 1 in exI, auto)
done
then have "x \<in> ?rhs" by auto
}
@@ -2214,7 +2164,7 @@
then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` S = S)"
using cone_iff[of S] assms by auto
then have "0 \<in> closure S \<and> (\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` closure S = closure S)"
- using closure_subset by (auto simp add: closure_scaleR)
+ using closure_subset by (auto simp: closure_scaleR)
then show ?thesis
using False cone_iff[of "closure S"] by auto
qed
@@ -2239,7 +2189,7 @@
"~ affine_dependent s \<Longrightarrow> ~ affine_dependent(s - t)"
by (meson Diff_subset affine_dependent_subset)
-lemma%important affine_dependent_explicit:
+proposition%important affine_dependent_explicit:
"affine_dependent p \<longleftrightarrow>
(\<exists>s u. finite s \<and> s \<subseteq> p \<and> sum u s = 0 \<and>
(\<exists>v\<in>s. u v \<noteq> 0) \<and> sum (\<lambda>v. u v *\<^sub>R v) s = 0)"
@@ -2417,7 +2367,7 @@
lemma convex_ball [iff]:
fixes x :: "'a::real_normed_vector"
shows "convex (ball x e)"
-proof (auto simp add: convex_def)
+proof (auto simp: convex_def)
fix y z
assume yz: "dist x y < e" "dist x z < e"
fix u v :: real
@@ -2448,7 +2398,7 @@
then have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e"
using convex_bound_le[OF yz uv] by auto
}
- then show ?thesis by (auto simp add: convex_def Ball_def)
+ then show ?thesis by (auto simp: convex_def Ball_def)
qed
lemma connected_ball [iff]:
@@ -2537,7 +2487,7 @@
by (intro convex_linear_vimage convex_translation convex_convex_hull,
simp add: linear_iff)
also have "?S = {y. (x, y) \<in> convex hull (s \<times> t)}"
- by (auto simp add: image_def Bex_def)
+ by (auto simp: image_def Bex_def)
finally show "convex {y. (x, y) \<in> convex hull (s \<times> t)}" .
next
show "convex {x. \<forall>y\<in>convex hull t. (x, y) \<in> convex hull (s \<times> t)}"
@@ -2547,7 +2497,7 @@
by (intro convex_linear_vimage convex_translation convex_convex_hull,
simp add: linear_iff)
also have "?S = {x. (x, y) \<in> convex hull (s \<times> t)}"
- by (auto simp add: image_def Bex_def)
+ by (auto simp: image_def Bex_def)
finally show "convex {x. (x, y) \<in> convex hull (s \<times> t)}" .
qed
qed
@@ -2609,13 +2559,13 @@
obt2: "u2\<ge>0" "v2\<ge>0" "u2 + v2 = 1" "b2 \<in> convex hull s" "y = u2 *\<^sub>R a + v2 *\<^sub>R b2"
by auto
have *: "\<And>(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)
+ by (auto simp: algebra_simps)
have **: "\<exists>b \<in> 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")
case True
have *: "\<And>(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)
+ by (auto simp: algebra_simps)
from True have ***: "u * v1 = 0" "v * v2 = 0"
using mult_nonneg_nonneg[OF \<open>u\<ge>0\<close> \<open>v1\<ge>0\<close>] mult_nonneg_nonneg[OF \<open>v\<ge>0\<close> \<open>v2\<ge>0\<close>]
by arith+
@@ -2624,13 +2574,13 @@
then show ?thesis
unfolding obt1(5) obt2(5) *
using assms hull_subset[of s convex]
- by (auto simp add: *** scaleR_right_distrib)
+ by (auto simp: *** scaleR_right_distrib)
next
case False
have "1 - (u * u1 + v * u2) = (u + v) - (u * u1 + v * u2)"
- using as(3) obt1(3) obt2(3) by (auto simp add: field_simps)
+ using as(3) obt1(3) obt2(3) by (auto simp: field_simps)
also have "\<dots> = u * (v1 + u1 - u1) + v * (v2 + u2 - u2)"
- using as(3) obt1(3) obt2(3) by (auto simp add: field_simps)
+ using as(3) obt1(3) obt2(3) by (auto simp: field_simps)
also have "\<dots> = u * v1 + v * v2"
by simp
finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto
@@ -2646,7 +2596,7 @@
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)
+ apply (auto simp: scaleR_left_distrib scaleR_right_distrib)
done
qed
have u1: "u1 \<le> 1"
@@ -2669,7 +2619,7 @@
apply (rule_tac x="1 - u * u1 - v * u2" in exI)
unfolding Bex_def
using as(1,2) obt1(1,2) obt2(1,2) **
- apply (auto simp add: algebra_simps)
+ apply (auto simp: algebra_simps)
done
qed
qed
@@ -2684,7 +2634,7 @@
subsubsection%unimportant \<open>Explicit expression for convex hull\<close>
-lemma%important convex_hull_indexed:
+proposition%important convex_hull_indexed:
fixes s :: "'a::real_vector set"
shows "convex hull s =
{y. \<exists>k u x.
@@ -2700,8 +2650,7 @@
assume "x\<in>s"
then show "x \<in> ?hull"
unfolding mem_Collect_eq
- apply (rule_tac x=1 in exI, rule_tac x="\<lambda>x. 1" in exI)
- apply auto
+ apply (rule_tac x=1 in exI, rule_tac x="\<lambda>x. 1" in exI, auto)
done
next
fix t
@@ -2738,7 +2687,7 @@
apply (rule, rule)
unfolding image_iff
apply (rule_tac x = "x - k1" in bexI)
- apply (auto simp add: not_le)
+ apply (auto simp: not_le)
done
have inj: "inj_on (\<lambda>i. i + k1) {1..k2}"
unfolding inj_on_def by auto
@@ -2771,7 +2720,7 @@
using False uv(2) y(1)[THEN bspec[where x=j]]
by (auto simp: j_def[symmetric])
qed
- qed (auto simp add: not_le x(2,3) y(2,3) uv(3))
+ qed (auto simp: not_le x(2,3) y(2,3) uv(3))
qed
lemma convex_hull_finite:
@@ -2780,12 +2729,11 @@
shows "convex hull s = {y. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and>
sum u s = 1 \<and> sum (\<lambda>x. u x *\<^sub>R x) s = y}"
(is "?HULL = ?set")
-proof (rule hull_unique, auto simp add: convex_def[of ?set])
+proof (rule hull_unique, auto simp: convex_def[of ?set])
fix x
assume "x \<in> s"
then show "\<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> sum u s = 1 \<and> (\<Sum>x\<in>s. u x *\<^sub>R x) = x"
- apply (rule_tac x="\<lambda>y. if x=y then 1 else 0" in exI)
- apply auto
+ apply (rule_tac x="\<lambda>y. if x=y then 1 else 0" in exI, auto)
unfolding sum.delta'[OF assms] and sum_delta''[OF assms]
apply auto
done
@@ -2813,8 +2761,7 @@
ultimately
show "\<exists>uc. (\<forall>x\<in>s. 0 \<le> uc x) \<and> sum uc s = 1 \<and>
(\<Sum>x\<in>s. uc x *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>s. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>s. uy x *\<^sub>R x)"
- apply (rule_tac x="\<lambda>x. u * ux x + v * uy x" in exI)
- apply auto
+ apply (rule_tac x="\<lambda>x. u * ux x + v * uy x" in exI, auto)
done
next
fix t
@@ -2864,8 +2811,7 @@
ultimately
have "\<exists>s u. finite s \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> sum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x"
apply (rule_tac x="y ` {1..k}" in exI)
- apply (rule_tac x="\<lambda>v. sum u {i\<in>{1..k}. y i = v}" in exI)
- apply auto
+ apply (rule_tac x="\<lambda>v. sum u {i\<in>{1..k}. y i = v}" in exI, auto)
done
then have "x\<in>?rhs" by auto
}
@@ -2899,13 +2845,11 @@
then have "{x. Suc 0 \<le> x \<and> x \<le> card s \<and> f x = y} = {i}"
apply auto
using f(1)[unfolded inj_on_def]
- apply(erule_tac x=x in ballE)
- apply auto
- done
+ by (metis One_nat_def atLeastAtMost_iff)
then have "card {x. Suc 0 \<le> x \<and> x \<le> card s \<and> f x = y} = 1" by auto
then have "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x)) = u y"
"(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x) = u y *\<^sub>R y"
- by (auto simp add: sum_constant_scaleR)
+ by (auto simp: sum_constant_scaleR)
}
then have "(\<Sum>x = 1..card s. u (f x)) = 1" "(\<Sum>i = 1..card s. u (f i) *\<^sub>R f i) = y"
unfolding sum_image_gen[OF *(1), of "\<lambda>x. u (f x) *\<^sub>R f x" f]
@@ -2920,8 +2864,7 @@
(\<Sum>i::nat = 1..k. u i *\<^sub>R x i) = y"
apply (rule_tac x="card s" in exI)
apply (rule_tac x="u \<circ> f" in exI)
- apply (rule_tac x=f in exI)
- apply fastforce
+ apply (rule_tac x=f in exI, fastforce)
done
then have "y \<in> ?lhs"
unfolding convex_hull_indexed by auto
@@ -2946,8 +2889,7 @@
assume ?lhs
then show ?rhs
unfolding *
- apply (rule_tac x=0 in exI)
- apply auto
+ apply (rule_tac x=0 in exI, auto)
done
next
assume ?lhs
@@ -3014,12 +2956,9 @@
unfolding convex_hull_finite_step[OF **, of a 1, unfolded * conj_assoc]
apply auto
apply (rule_tac x=v in exI)
- apply (rule_tac x="1 - v" in exI)
- apply simp
- apply (rule_tac x=u in exI)
- apply simp
- apply (rule_tac x="\<lambda>x. v" in exI)
- apply simp
+ apply (rule_tac x="1 - v" in exI, simp)
+ apply (rule_tac x=u in exI, simp)
+ apply (rule_tac x="\<lambda>x. v" in exI, simp)
done
qed
@@ -3034,7 +2973,7 @@
unfolding *
apply auto
apply (rule_tac[!] x=u in exI)
- apply (auto simp add: algebra_simps)
+ apply (auto simp: algebra_simps)
done
qed
@@ -3044,22 +2983,17 @@
have fin: "finite {a,b,c}" "finite {b,c}" "finite {c}"
by auto
have *: "\<And>x y z ::real. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z"
- by (auto simp add: field_simps)
+ by (auto simp: field_simps)
show ?thesis
unfolding convex_hull_finite[OF fin(1)] and convex_hull_finite_step[OF fin(2)] and *
unfolding convex_hull_finite_step[OF fin(3)]
- apply (rule Collect_cong)
- apply simp
+ apply (rule Collect_cong, simp)
apply auto
apply (rule_tac x=va in exI)
- apply (rule_tac x="u c" in exI)
- apply simp
- apply (rule_tac x="1 - v - w" in exI)
- apply simp
- apply (rule_tac x=v in exI)
- apply simp
- apply (rule_tac x="\<lambda>x. w" in exI)
- apply simp
+ apply (rule_tac x="u c" in exI, simp)
+ apply (rule_tac x="1 - v - w" in exI, simp)
+ apply (rule_tac x=v in exI, simp)
+ apply (rule_tac x="\<lambda>x. w" in exI, simp)
done
qed
@@ -3070,7 +3004,7 @@
by auto
show ?thesis
unfolding convex_hull_3
- apply (auto simp add: *)
+ apply (auto simp: *)
apply (rule_tac x=v in exI)
apply (rule_tac x=w in exI)
apply (simp add: algebra_simps)
@@ -3150,15 +3084,14 @@
unfolding scaleR_left.sum
unfolding t_def and sum.reindex[OF inj] and o_def
using obt(5)
- by (auto simp add: sum.distrib scaleR_right_distrib)
+ by (auto simp: sum.distrib scaleR_right_distrib)
then have "(\<Sum>v\<in>insert a t. (if v = a then - (\<Sum>x\<in>t. u (x - a)) else u (v - a)) *\<^sub>R v) = 0"
unfolding sum_clauses(2)[OF fin]
using \<open>a\<notin>s\<close> \<open>t\<subseteq>s\<close>
- by (auto simp add: *)
+ by (auto simp: *)
ultimately show ?thesis
unfolding affine_dependent_explicit
- apply (rule_tac x="insert a t" in exI)
- apply auto
+ apply (rule_tac x="insert a t" in exI, auto)
done
qed
@@ -3175,10 +3108,8 @@
using \<open>?lhs\<close>[unfolded convex_def, THEN conjunct1]
apply (erule_tac x="2*\<^sub>R x" in ballE)
apply (erule_tac x="2*\<^sub>R y" in ballE)
- apply (erule_tac x="1/2" in allE)
- apply simp
- apply (erule_tac x="1/2" in allE)
- apply auto
+ apply (erule_tac x="1/2" in allE, simp)
+ apply (erule_tac x="1/2" in allE, auto)
done
}
then show ?thesis
@@ -3205,8 +3136,7 @@
finally show ?thesis
apply (subst insert_Diff[OF \<open>a\<in>s\<close>, symmetric])
apply (rule dependent_imp_affine_dependent)
- apply (rule dependent_biggerset)
- apply auto
+ apply (rule dependent_biggerset, auto)
done
qed
@@ -3229,7 +3159,7 @@
apply (rule subset_le_dim)
unfolding subset_eq
using \<open>a\<in>s\<close>
- apply (auto simp add:span_superset span_diff)
+ apply (auto simp:span_superset span_diff)
done
also have "\<dots> < dim s + 1" by auto
also have "\<dots> \<le> card (s - {a})"
@@ -3502,8 +3432,7 @@
some_eq_ex[of "\<lambda>d. \<exists>B. affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> of_nat (card B) = d + 1"]
apply auto
apply (rule exI[of _ "int (card B) - (1 :: int)"])
- apply (rule exI[of _ "B"])
- apply auto
+ apply (rule exI[of _ "B"], auto)
done
qed
@@ -3685,8 +3614,7 @@
apply(rule B)
unfolding span_substd_basis[OF d, symmetric]
apply (rule span_inc)
- apply (rule independent_substdbasis[OF d])
- apply rule
+ apply (rule independent_substdbasis[OF d], rule)
apply assumption
unfolding t[symmetric] span_substd_basis[OF d] dim_substandard[OF d]
apply auto
@@ -3776,7 +3704,7 @@
assume "a \<noteq> b"
then have "aff_dim{a,b} = card{a,b} - 1"
using affine_independent_2 [of a b] aff_dim_affine_independent by fastforce
- also have "... = 1"
+ also have "\<dots> = 1"
using \<open>a \<noteq> b\<close> by simp
finally show "aff_dim {a, b} = 1" .
qed
@@ -4005,9 +3933,9 @@
by blast
then have "card {b - a |b. b \<in> S - {a}} = card ((\<lambda>b. b-a) ` (S - {a}))"
by simp
- also have "... = card (S - {a})"
+ also have "\<dots> = card (S - {a})"
by (metis (no_types, lifting) card_image diff_add_cancel inj_onI)
- also have "... = card S - 1"
+ also have "\<dots> = card S - 1"
by (simp add: aff_independent_finite assms)
finally have 4: "card {b - a |b. b \<in> S - {a}} = card S - 1" .
have "finite S"
@@ -4238,8 +4166,7 @@
assume "\<exists>s u. finite s \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> sum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
then obtain N where "?P N" by auto
then have "\<exists>n\<le>N. (\<forall>k<n. \<not> ?P k) \<and> ?P n"
- apply (rule_tac ex_least_nat_le)
- apply auto
+ apply (rule_tac ex_least_nat_le, auto)
done
then obtain n where "?P n" and smallest: "\<forall>k<n. \<not> ?P k"
by blast
@@ -4260,8 +4187,7 @@
proof (rule ccontr, simp add: not_less)
assume as:"\<forall>x\<in>s. 0 \<le> w x"
then have "sum w (s - {v}) \<ge> 0"
- apply (rule_tac sum_nonneg)
- apply auto
+ apply (rule_tac sum_nonneg, auto)
done
then have "sum w s > 0"
unfolding sum.remove[OF obt(1) \<open>v\<in>s\<close>]
@@ -4311,7 +4237,7 @@
apply (rule_tac x="(s - {a})" in exI)
apply (rule_tac x="\<lambda>v. u v + t * w v" in exI)
using obt(1-3) and t and a
- apply (auto simp add: * scaleR_left_distrib)
+ apply (auto simp: * scaleR_left_distrib)
done
then show False
using smallest[THEN spec[where x="n - 1"]] by auto
@@ -4327,9 +4253,8 @@
(is "?lhs = ?rhs")
proof
show "?lhs \<subseteq> ?rhs"
- apply (subst convex_hull_caratheodory_aff_dim)
- apply clarify
- apply (rule_tac x="s" in exI)
+ apply (subst convex_hull_caratheodory_aff_dim, clarify)
+ apply (rule_tac x=s in exI)
apply (simp add: hull_subset convex_explicit [THEN iffD1, OF convex_convex_hull])
done
next
@@ -4354,7 +4279,7 @@
next
fix x
assume "x \<in> ?rhs" then show "x \<in> ?lhs"
- by (auto simp add: convex_hull_explicit)
+ by (auto simp: convex_hull_explicit)
qed
theorem%important caratheodory:
@@ -4413,14 +4338,13 @@
qed
lemma mem_rel_interior: "x \<in> rel_interior S \<longleftrightarrow> (\<exists>T. open T \<and> x \<in> T \<inter> S \<and> T \<inter> affine hull S \<subseteq> S)"
- by (auto simp add: rel_interior)
+ by (auto simp: rel_interior)
lemma mem_rel_interior_ball:
"x \<in> rel_interior S \<longleftrightarrow> x \<in> S \<and> (\<exists>e. e > 0 \<and> ball x e \<inter> affine hull S \<subseteq> S)"
apply (simp add: rel_interior, safe)
- apply (force simp add: open_contains_ball)
- apply (rule_tac x = "ball x e" in exI)
- apply simp
+ apply (force simp: open_contains_ball)
+ apply (rule_tac x = "ball x e" in exI, simp)
done
lemma rel_interior_ball:
@@ -4430,10 +4354,9 @@
lemma mem_rel_interior_cball:
"x \<in> rel_interior S \<longleftrightarrow> x \<in> S \<and> (\<exists>e. e > 0 \<and> cball x e \<inter> affine hull S \<subseteq> S)"
apply (simp add: rel_interior, safe)
- apply (force simp add: open_contains_cball)
+ apply (force simp: open_contains_cball)
apply (rule_tac x = "ball x e" in exI)
- apply (simp add: subset_trans [OF ball_subset_cball])
- apply auto
+ apply (simp add: subset_trans [OF ball_subset_cball], auto)
done
lemma rel_interior_cball:
@@ -4441,7 +4364,7 @@
using mem_rel_interior_cball [of _ S] by auto
lemma rel_interior_empty [simp]: "rel_interior {} = {}"
- by (auto simp add: rel_interior_def)
+ by (auto simp: rel_interior_def)
lemma affine_hull_sing [simp]: "affine hull {a :: 'n::euclidean_space} = {a}"
by (metis affine_hull_eq affine_sing)
@@ -4449,8 +4372,7 @@
lemma rel_interior_sing [simp]:
fixes a :: "'n::euclidean_space" shows "rel_interior {a} = {a}"
apply (auto simp: rel_interior_ball)
- apply (rule_tac x=1 in exI)
- apply force
+ apply (rule_tac x=1 in exI, force)
done
lemma subset_rel_interior:
@@ -4458,16 +4380,16 @@
assumes "S \<subseteq> T"
and "affine hull S = affine hull T"
shows "rel_interior S \<subseteq> rel_interior T"
- using assms by (auto simp add: rel_interior_def)
+ using assms by (auto simp: rel_interior_def)
lemma rel_interior_subset: "rel_interior S \<subseteq> S"
- by (auto simp add: rel_interior_def)
+ by (auto simp: rel_interior_def)
lemma rel_interior_subset_closure: "rel_interior S \<subseteq> closure S"
- using rel_interior_subset by (auto simp add: closure_def)
+ using rel_interior_subset by (auto simp: closure_def)
lemma interior_subset_rel_interior: "interior S \<subseteq> rel_interior S"
- by (auto simp add: rel_interior interior_def)
+ by (auto simp: rel_interior interior_def)
lemma interior_rel_interior:
fixes S :: "'n::euclidean_space set"
@@ -4546,7 +4468,7 @@
fix y
assume as: "dist (x - e *\<^sub>R (x - c)) y < e * d" "y \<in> affine hull S"
have *: "y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x"
- using \<open>e > 0\<close> by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
+ using \<open>e > 0\<close> by (auto simp: scaleR_left_diff_distrib scaleR_right_diff_distrib)
have "x \<in> affine hull S"
using assms hull_subset[of S] by auto
moreover have "1 / e + - ((1 - e) / e) = 1"
@@ -4558,13 +4480,13 @@
unfolding dist_norm norm_scaleR[symmetric]
apply (rule arg_cong[where f=norm])
using \<open>e > 0\<close>
- apply (auto simp add: euclidean_eq_iff[where 'a='a] field_simps inner_simps)
+ apply (auto simp: euclidean_eq_iff[where 'a='a] field_simps inner_simps)
done
also have "\<dots> = \<bar>1/e\<bar> * norm (x - e *\<^sub>R (x - c) - y)"
by (auto intro!:arg_cong[where f=norm] simp add: algebra_simps)
also have "\<dots> < d"
using as[unfolded dist_norm] and \<open>e > 0\<close>
- by (auto simp add:pos_divide_less_eq[OF \<open>e > 0\<close>] mult.commute)
+ by (auto simp:pos_divide_less_eq[OF \<open>e > 0\<close>] mult.commute)
finally have "y \<in> S"
apply (subst *)
apply (rule assms(1)[unfolded convex_alt,rule_format])
@@ -4600,7 +4522,7 @@
then have "y \<in> interior {a..}"
apply (simp add: mem_interior)
apply (rule_tac x="(y-a)" in exI)
- apply (auto simp add: dist_norm)
+ apply (auto simp: dist_norm)
done
}
moreover
@@ -4610,7 +4532,7 @@
then obtain e where e: "e > 0" "cball y e \<subseteq> {a..}"
using mem_interior_cball[of y "{a..}"] by auto
moreover from e have "y - e \<in> cball y e"
- by (auto simp add: cball_def dist_norm)
+ by (auto simp: cball_def dist_norm)
ultimately have "a \<le> y - e" by blast
then have "a < y" using e by auto
}
@@ -4640,7 +4562,7 @@
then have "y \<in> interior {..a}"
apply (simp add: mem_interior)
apply (rule_tac x="(a-y)" in exI)
- apply (auto simp add: dist_norm)
+ apply (auto simp: dist_norm)
done
}
moreover
@@ -4650,7 +4572,7 @@
then obtain e where e: "e > 0" "cball y e \<subseteq> {..a}"
using mem_interior_cball[of y "{..a}"] by auto
moreover from e have "y + e \<in> cball y e"
- by (auto simp add: cball_def dist_norm)
+ by (auto simp: cball_def dist_norm)
ultimately have "a \<ge> y + e" by auto
then have "a > y" using e by auto
}
@@ -4660,9 +4582,9 @@
lemma interior_atLeastAtMost_real [simp]: "interior {a..b} = {a<..<b :: real}"
proof-
have "{a..b} = {a..} \<inter> {..b}" by auto
- also have "interior ... = {a<..} \<inter> {..<b}"
+ also have "interior \<dots> = {a<..} \<inter> {..<b}"
by (simp add: interior_real_semiline interior_real_semiline')
- also have "... = {a<..<b}" by auto
+ also have "\<dots> = {a<..<b}" by auto
finally show ?thesis .
qed
@@ -4681,7 +4603,7 @@
lemma frontier_real_Iic [simp]:
fixes a :: real
shows "frontier {..a} = {a}"
- unfolding frontier_def by (auto simp add: interior_real_semiline')
+ unfolding frontier_def by (auto simp: interior_real_semiline')
lemma rel_interior_real_box [simp]:
fixes a b :: real
@@ -4720,8 +4642,7 @@
lemma openin_rel_interior: "openin (subtopology euclidean (affine hull S)) (rel_interior S)"
apply (simp add: rel_interior_def)
- apply (subst openin_subopen)
- apply blast
+ apply (subst openin_subopen, blast)
done
lemma openin_set_rel_interior:
@@ -4800,8 +4721,7 @@
proof (cases "x \<in> S")
case True
then show ?thesis using \<open>e > 0\<close> \<open>d > 0\<close>
- apply (rule_tac bexI[where x=x])
- apply (auto)
+ apply (rule_tac bexI[where x=x], auto)
done
next
case False
@@ -4821,7 +4741,7 @@
next
case False
then have "0 < e * d / (1 - e)" and *: "1 - e > 0"
- using \<open>e \<le> 1\<close> \<open>e > 0\<close> \<open>d > 0\<close> by (auto)
+ using \<open>e \<le> 1\<close> \<open>e > 0\<close> \<open>d > 0\<close> by auto
then obtain y where "y \<in> S" "y \<noteq> 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
@@ -4837,11 +4757,11 @@
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 \<open>e > 0\<close>
- by (auto simp add: scaleR_right_diff_distrib scaleR_right_distrib scaleR_left_diff_distrib)
+ by (auto simp: scaleR_right_diff_distrib scaleR_right_distrib scaleR_left_diff_distrib)
have zball: "z \<in> ball c d"
using mem_ball z_def dist_norm[of c]
using y and assms(4,5)
- by (auto simp add:field_simps norm_minus_commute)
+ by (auto simp:field_simps norm_minus_commute)
have "x \<in> affine hull S"
using closure_affine_hull assms by auto
moreover have "y \<in> affine hull S"
@@ -4852,7 +4772,7 @@
using z_def affine_affine_hull[of S]
mem_affine_3_minus [of "affine hull S" c x y "(1 - e) / e"]
assms
- by (auto simp add: field_simps)
+ by (auto simp: field_simps)
then have "z \<in> S" using d zball by auto
obtain d1 where "d1 > 0" and d1: "ball z d1 \<le> ball c d"
using zball open_ball[of c d] openE[of "ball c d" z] by auto
@@ -4955,18 +4875,16 @@
apply (rule_tac[!] hull_induct, rule hull_inc)
prefer 3
apply (erule imageE)
- apply (rule_tac x=xa in image_eqI)
- apply assumption
- apply (rule hull_subset[unfolded subset_eq, rule_format])
- apply assumption
+ apply (rule_tac x=xa in image_eqI, assumption)
+ apply (rule hull_subset[unfolded subset_eq, rule_format], assumption)
proof -
interpret f: bounded_linear f by fact
show "affine {x. f x \<in> affine hull f ` s}"
unfolding affine_def
- by (auto simp add: f.scaleR f.add affine_affine_hull[unfolded affine_def, rule_format])
+ by (auto simp: f.scaleR f.add affine_affine_hull[unfolded affine_def, rule_format])
show "affine {x. x \<in> f ` (affine hull s)}"
using affine_affine_hull[unfolded affine_def, of s]
- unfolding affine_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric])
+ unfolding affine_def by (auto simp: f.scaleR [symmetric] f.add [symmetric])
qed auto
@@ -5181,11 +5099,9 @@
unfolding image_iff mem_Collect_eq
apply rule
apply auto
- apply (rule_tac x=u in rev_bexI)
- apply simp
+ apply (rule_tac x=u in rev_bexI, simp)
apply (erule rev_bexI)
- apply (erule rev_bexI)
- apply simp
+ apply (erule rev_bexI, simp)
apply auto
done
have "continuous_on ?X (\<lambda>z. (1 - fst z) *\<^sub>R fst (snd z) + fst z *\<^sub>R snd (snd z))"
@@ -5224,8 +5140,7 @@
unfolding convex_hull_insert [OF \<open>A \<noteq> {}\<close>]
apply safe
apply (rule_tac x=a in exI, simp)
- apply (rule_tac x="1 - a" in exI, simp)
- apply fast
+ apply (rule_tac x="1 - a" in exI, simp, fast)
apply (rule_tac x="(u, b)" in image_eqI, simp_all)
done
finally show "compact (convex hull (insert x A))" .
@@ -5302,7 +5217,7 @@
done
ultimately show "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t"
apply (rule_tac x="insert u t" in exI)
- apply (auto simp add: card_insert_if)
+ apply (auto simp: card_insert_if)
done
next
fix x
@@ -5322,8 +5237,7 @@
next
case True
then obtain a u where au: "t = insert a u" "a\<notin>u"
- apply (drule_tac card_eq_SucD)
- apply auto
+ apply (drule_tac card_eq_SucD, auto)
done
show ?thesis
proof (cases "u = {}")
@@ -5445,7 +5359,7 @@
proof
assume "x = b"
then have "y = b" unfolding obt(5)
- using obt(3) by (auto simp add: scaleR_left_distrib[symmetric])
+ using obt(3) by (auto simp: scaleR_left_distrib[symmetric])
then show False using obt(4) and False by simp
qed
then have *: "w *\<^sub>R (x - b) \<noteq> 0" using w(1) by auto
@@ -5459,8 +5373,7 @@
by (simp add: algebra_simps)
moreover have "(u + w) *\<^sub>R x + (v - w) *\<^sub>R b \<in> convex hull insert x s"
unfolding convex_hull_insert[OF \<open>s\<noteq>{}\<close>] and mem_Collect_eq
- apply (rule_tac x="u + w" in exI)
- apply rule
+ apply (rule_tac x="u + w" in exI, rule)
defer
apply (rule_tac x="v - w" in exI)
using \<open>u \<ge> 0\<close> and w and obt(3,4)
@@ -5475,8 +5388,7 @@
by (simp add: algebra_simps)
moreover have "(u - w) *\<^sub>R x + (v + w) *\<^sub>R b \<in> convex hull insert x s"
unfolding convex_hull_insert[OF \<open>s\<noteq>{}\<close>] and mem_Collect_eq
- apply (rule_tac x="u - w" in exI)
- apply rule
+ apply (rule_tac x="u - w" in exI, rule)
defer
apply (rule_tac x="v + w" in exI)
using \<open>u \<ge> 0\<close> and w and obt(3,4)
@@ -5487,7 +5399,7 @@
qed auto
qed
qed auto
-qed (auto simp add: assms)
+qed (auto simp: assms)
lemma simplex_furthest_le:
fixes s :: "'a::real_inner set"
@@ -5549,7 +5461,7 @@
by auto
then show ?thesis
using obt(3)[THEN bspec[where x=u], THEN bspec[where x=y]] and obt(1)
- by (auto simp add: norm_minus_commute)
+ by (auto simp: norm_minus_commute)
qed auto
qed
@@ -5601,18 +5513,13 @@
proof -
have z: "inner z z > 0"
unfolding inner_gt_zero_iff using assms by auto
+ have "norm (v *\<^sub>R z - y) < norm y"
+ if "0 < v" and "v \<le> inner y z / inner z z" for v
+ unfolding norm_lt using z assms that
+ by (simp add: field_simps inner_diff inner_commute mult_strict_left_mono[OF _ \<open>0<v\<close>])
then show ?thesis
- using assms
- apply (rule_tac x = "inner y z / inner z z" in exI)
- apply rule
- defer
- proof rule+
- fix v
- assume "0 < v" and "v \<le> inner y z / inner z z"
- then show "norm (v *\<^sub>R z - y) < norm y"
- unfolding norm_lt using z and assms
- by (simp add: field_simps inner_diff inner_commute mult_strict_left_mono[OF _ \<open>0<v\<close>])
- qed auto
+ using assms z
+ by (rule_tac x = "inner y z / inner z z" in exI) auto
qed
lemma closer_point_lemma:
@@ -5625,7 +5532,7 @@
show ?thesis
apply (rule_tac x="min u 1" in exI)
using u[THEN spec[where x="min u 1"]] and \<open>u > 0\<close>
- unfolding dist_norm by (auto simp add: norm_minus_commute field_simps)
+ unfolding dist_norm by (auto simp: norm_minus_commute field_simps)
qed
lemma any_closest_point_dot:
@@ -5640,7 +5547,7 @@
using convexD_alt[OF assms(1,3,4), of u] using u by auto
then show False
using assms(5)[THEN bspec[where x="?z"]] and u(3)
- by (auto simp add: dist_commute algebra_simps)
+ by (auto simp: dist_commute algebra_simps)
qed
lemma any_closest_point_unique:
@@ -5650,7 +5557,7 @@
shows "x = y"
using any_closest_point_dot[OF assms(1-4,5)] and any_closest_point_dot[OF assms(1-2,4,3,6)]
unfolding norm_pths(1) and norm_le_square
- by (auto simp add: algebra_simps)
+ by (auto simp: algebra_simps)
lemma closest_point_unique:
assumes "convex s" "closed s" "x \<in> s" "\<forall>z\<in>s. dist a x \<le> dist a z"
@@ -5729,7 +5636,7 @@
by (simp add: y_def algebra_simps)
then have "norm (x - y) = abs ((1 - min 1 (e / norm (closest_point S x - x)))) * norm(x - closest_point S x)"
by simp
- also have "... < norm(x - closest_point S x)"
+ also have "\<dots> < norm(x - closest_point S x)"
using clo_notx \<open>e > 0\<close>
by (auto simp: mult_less_cancel_right2 divide_simps)
finally have no_less: "norm (x - y) < norm (x - closest_point S x)" .
@@ -5766,8 +5673,7 @@
show ?thesis
apply (rule_tac x="y - z" in exI)
apply (rule_tac x="inner (y - z) y" in exI)
- apply (rule_tac x=y in bexI)
- apply rule
+ apply (rule_tac x=y in bexI, rule)
defer
apply rule
defer
@@ -5788,9 +5694,9 @@
using assms(1)[unfolded convex_alt] and y and \<open>x\<in>s\<close> and \<open>y\<in>s\<close> by auto
assume "\<not> inner (y - z) y \<le> inner (y - z) x"
then obtain v where "v > 0" "v \<le> 1" "dist (y + v *\<^sub>R (x - y)) z < dist y z"
- using closer_point_lemma[of z y x] by (auto simp add: inner_diff)
+ using closer_point_lemma[of z y x] by (auto simp: inner_diff)
then show False
- using *[THEN spec[where x=v]] by (auto simp add: dist_commute algebra_simps)
+ using *[THEN spec[where x=v]] by (auto simp: dist_commute algebra_simps)
qed auto
qed
@@ -5830,7 +5736,7 @@
by auto
then show False using y[THEN bspec[where x="y + u *\<^sub>R (x - y)"]]
using assms(1)[unfolded convex_alt, THEN bspec[where x=y]]
- using \<open>x\<in>s\<close> \<open>y\<in>s\<close> by (auto simp add: dist_commute algebra_simps)
+ using \<open>x\<in>s\<close> \<open>y\<in>s\<close> by (auto simp: dist_commute algebra_simps)
qed
moreover have "0 < (norm (y - z))\<^sup>2"
using \<open>y\<in>s\<close> \<open>z\<notin>s\<close> by auto
@@ -5838,7 +5744,7 @@
unfolding power2_norm_eq_inner by simp
ultimately show "inner (y - z) z + (norm (y - z))\<^sup>2 / 2 < inner (y - z) x"
unfolding power2_norm_eq_inner and not_less
- by (auto simp add: field_simps inner_commute inner_diff)
+ by (auto simp: field_simps inner_commute inner_diff)
qed (insert \<open>y\<in>s\<close> \<open>z\<notin>s\<close>, auto)
qed
@@ -5867,8 +5773,7 @@
apply (elim exE)
unfolding inner_zero_right
apply (rule_tac x=a in exI)
- apply (rule_tac x=b in exI)
- apply auto
+ apply (rule_tac x=b in exI, auto)
done
qed
@@ -5908,7 +5813,7 @@
apply rule
apply rule
apply (erule_tac x="x - y" in ballE)
- apply (auto simp add: inner_diff)
+ apply (auto simp: inner_diff)
done
define k where "k = (SUP x:T. a \<bullet> x)"
show ?thesis
@@ -5958,8 +5863,7 @@
by auto
then show ?thesis
apply (rule_tac x="-a" in exI)
- apply (rule_tac x="-b" in exI)
- apply auto
+ apply (rule_tac x="-b" in exI, auto)
done
qed
@@ -5967,13 +5871,13 @@
subsubsection%unimportant \<open>General case without assuming closure and getting non-strict separation\<close>
lemma separating_hyperplane_set_0:
- assumes "convex s" "(0::'a::euclidean_space) \<notin> s"
- shows "\<exists>a. a \<noteq> 0 \<and> (\<forall>x\<in>s. 0 \<le> inner a x)"
+ assumes "convex S" "(0::'a::euclidean_space) \<notin> S"
+ shows "\<exists>a. a \<noteq> 0 \<and> (\<forall>x\<in>S. 0 \<le> inner a x)"
proof -
let ?k = "\<lambda>c. {x::'a. 0 \<le> inner c x}"
- have *: "frontier (cball 0 1) \<inter> \<Inter>f \<noteq> {}" if as: "f \<subseteq> ?k ` s" "finite f" for f
+ have *: "frontier (cball 0 1) \<inter> \<Inter>f \<noteq> {}" if as: "f \<subseteq> ?k ` S" "finite f" for f
proof -
- obtain c where c: "f = ?k ` c" "c \<subseteq> s" "finite c"
+ obtain c where c: "f = ?k ` c" "c \<subseteq> S" "finite c"
using finite_subset_image[OF as(2,1)] by auto
then obtain a b where ab: "a \<noteq> 0" "0 < b" "\<forall>x\<in>convex hull c. b < inner a x"
using separating_hyperplane_closed_0[OF convex_convex_hull, of c]
@@ -5984,50 +5888,50 @@
apply (rule_tac x = "inverse(norm a) *\<^sub>R a" in exI)
using hull_subset[of c convex]
unfolding subset_eq and inner_scaleR
- by (auto simp add: inner_commute del: ballE elim!: ballE)
+ by (auto simp: inner_commute del: ballE elim!: ballE)
then show "frontier (cball 0 1) \<inter> \<Inter>f \<noteq> {}"
unfolding c(1) frontier_cball sphere_def dist_norm by auto
qed
- have "frontier (cball 0 1) \<inter> (\<Inter>(?k ` s)) \<noteq> {}"
+ have "frontier (cball 0 1) \<inter> (\<Inter>(?k ` S)) \<noteq> {}"
apply (rule compact_imp_fip)
apply (rule compact_frontier[OF compact_cball])
using * closed_halfspace_ge
by auto
- then obtain x where "norm x = 1" "\<forall>y\<in>s. x\<in>?k y"
+ then obtain x where "norm x = 1" "\<forall>y\<in>S. x\<in>?k y"
unfolding frontier_cball dist_norm sphere_def by auto
then show ?thesis
by (metis inner_commute mem_Collect_eq norm_eq_zero zero_neq_one)
qed
lemma separating_hyperplane_sets:
- fixes s t :: "'a::euclidean_space set"
- assumes "convex s"
- and "convex t"
- and "s \<noteq> {}"
- and "t \<noteq> {}"
- and "s \<inter> t = {}"
- shows "\<exists>a b. a \<noteq> 0 \<and> (\<forall>x\<in>s. inner a x \<le> b) \<and> (\<forall>x\<in>t. inner a x \<ge> b)"
+ fixes S T :: "'a::euclidean_space set"
+ assumes "convex S"
+ and "convex T"
+ and "S \<noteq> {}"
+ and "T \<noteq> {}"
+ and "S \<inter> T = {}"
+ shows "\<exists>a b. a \<noteq> 0 \<and> (\<forall>x\<in>S. inner a x \<le> b) \<and> (\<forall>x\<in>T. inner a x \<ge> b)"
proof -
from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]]
- obtain a where "a \<noteq> 0" "\<forall>x\<in>{x - y |x y. x \<in> t \<and> y \<in> s}. 0 \<le> inner a x"
- using assms(3-5) by fastforce
- then have *: "\<And>x y. x \<in> t \<Longrightarrow> y \<in> s \<Longrightarrow> inner a y \<le> inner a x"
- by (force simp add: inner_diff)
- then have bdd: "bdd_above (((\<bullet>) a)`s)"
- using \<open>t \<noteq> {}\<close> by (auto intro: bdd_aboveI2[OF *])
+ obtain a where "a \<noteq> 0" "\<forall>x\<in>{x - y |x y. x \<in> T \<and> y \<in> S}. 0 \<le> inner a x"
+ using assms(3-5) by force
+ then have *: "\<And>x y. x \<in> T \<Longrightarrow> y \<in> S \<Longrightarrow> inner a y \<le> inner a x"
+ by (force simp: inner_diff)
+ then have bdd: "bdd_above (((\<bullet>) a)`S)"
+ using \<open>T \<noteq> {}\<close> by (auto intro: bdd_aboveI2[OF *])
show ?thesis
using \<open>a\<noteq>0\<close>
- by (intro exI[of _ a] exI[of _ "SUP x:s. a \<bullet> x"])
- (auto intro!: cSUP_upper bdd cSUP_least \<open>a \<noteq> 0\<close> \<open>s \<noteq> {}\<close> *)
+ by (intro exI[of _ a] exI[of _ "SUP x:S. a \<bullet> x"])
+ (auto intro!: cSUP_upper bdd cSUP_least \<open>a \<noteq> 0\<close> \<open>S \<noteq> {}\<close> *)
qed
subsection%unimportant \<open>More convexity generalities\<close>
lemma convex_closure [intro,simp]:
- fixes s :: "'a::real_normed_vector set"
- assumes "convex s"
- shows "convex (closure s)"
+ fixes S :: "'a::real_normed_vector set"
+ assumes "convex S"
+ shows "convex (closure S)"
apply (rule convexI)
apply (unfold closure_sequential, elim exE)
apply (rule_tac x="\<lambda>n. u *\<^sub>R xa n + v *\<^sub>R xb n" in exI)
@@ -6037,9 +5941,9 @@
done
lemma convex_interior [intro,simp]:
- fixes s :: "'a::real_normed_vector set"
- assumes "convex s"
- shows "convex (interior s)"
+ fixes S :: "'a::real_normed_vector set"
+ assumes "convex S"
+ shows "convex (interior S)"
unfolding convex_alt Ball_def mem_interior
apply (rule,rule,rule,rule,rule,rule)
apply (elim exE conjE)
@@ -6047,55 +5951,54 @@
fix x y u
assume u: "0 \<le> u" "u \<le> (1::real)"
fix e d
- assume ed: "ball x e \<subseteq> s" "ball y d \<subseteq> s" "0<d" "0<e"
- show "\<exists>e>0. ball ((1 - u) *\<^sub>R x + u *\<^sub>R y) e \<subseteq> s"
- apply (rule_tac x="min d e" in exI)
- apply rule
+ assume ed: "ball x e \<subseteq> S" "ball y d \<subseteq> S" "0<d" "0<e"
+ show "\<exists>e>0. ball ((1 - u) *\<^sub>R x + u *\<^sub>R y) e \<subseteq> S"
+ apply (rule_tac x="min d e" in exI, rule)
unfolding subset_eq
defer
apply rule
proof -
fix z
assume "z \<in> ball ((1 - u) *\<^sub>R x + u *\<^sub>R y) (min d e)"
- then have "(1- u) *\<^sub>R (z - u *\<^sub>R (y - x)) + u *\<^sub>R (z + (1 - u) *\<^sub>R (y - x)) \<in> s"
+ then have "(1- u) *\<^sub>R (z - u *\<^sub>R (y - x)) + u *\<^sub>R (z + (1 - u) *\<^sub>R (y - x)) \<in> S"
apply (rule_tac assms[unfolded convex_alt, rule_format])
using ed(1,2) and u
unfolding subset_eq mem_ball Ball_def dist_norm
- apply (auto simp add: algebra_simps)
+ apply (auto simp: algebra_simps)
done
- then show "z \<in> s"
- using u by (auto simp add: algebra_simps)
+ then show "z \<in> S"
+ using u by (auto simp: algebra_simps)
qed(insert u ed(3-4), auto)
qed
-lemma convex_hull_eq_empty[simp]: "convex hull s = {} \<longleftrightarrow> s = {}"
- using hull_subset[of s convex] convex_hull_empty by auto
+lemma convex_hull_eq_empty[simp]: "convex hull S = {} \<longleftrightarrow> S = {}"
+ using hull_subset[of S convex] convex_hull_empty by auto
subsection%unimportant \<open>Moving and scaling convex hulls\<close>
lemma convex_hull_set_plus:
- "convex hull (s + t) = convex hull s + convex hull t"
+ "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: "(\<lambda>x. a + x) ` t = {a} + t"
+lemma translation_eq_singleton_plus: "(\<lambda>x. a + x) ` T = {a} + T"
unfolding set_plus_def by auto
lemma convex_hull_translation:
- "convex hull ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (convex hull s)"
+ "convex hull ((\<lambda>x. a + x) ` S) = (\<lambda>x. a + x) ` (convex hull S)"
unfolding translation_eq_singleton_plus
by (simp only: convex_hull_set_plus convex_hull_singleton)
lemma convex_hull_scaling:
- "convex hull ((\<lambda>x. c *\<^sub>R x) ` s) = (\<lambda>x. c *\<^sub>R x) ` (convex hull s)"
+ "convex hull ((\<lambda>x. c *\<^sub>R x) ` S) = (\<lambda>x. c *\<^sub>R x) ` (convex hull S)"
using linear_scaleR by (rule convex_hull_linear_image [symmetric])
lemma convex_hull_affinity:
- "convex hull ((\<lambda>x. a + c *\<^sub>R x) ` s) = (\<lambda>x. a + c *\<^sub>R x) ` (convex hull s)"
+ "convex hull ((\<lambda>x. a + c *\<^sub>R x) ` S) = (\<lambda>x. a + c *\<^sub>R x) ` (convex hull S)"
by(simp only: image_image[symmetric] convex_hull_scaling convex_hull_translation)
@@ -6133,7 +6036,7 @@
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 \<in> cone hull S"
using mem_cone_hull[of "(cx/(cx+cy)) *\<^sub>R xx + (cy/(cx+cy)) *\<^sub>R yy" S "cx+cy"] \<open>cx+cy>0\<close>
- by (auto simp add: scaleR_right_distrib)
+ by (auto simp: scaleR_right_distrib)
then have "u *\<^sub>R x + v *\<^sub>R y \<in> cone hull S"
using x y by auto
}
@@ -6173,8 +6076,7 @@
fixes s :: "('a::euclidean_space) set"
assumes "closed s" "convex s"
shows "s = \<Inter>{h. s \<subseteq> h \<and> (\<exists>a b. h = {x. inner a x \<le> b})}"
- apply (rule set_eqI)
- apply rule
+ apply (rule set_eqI, rule)
unfolding Inter_iff Ball_def mem_Collect_eq
apply (rule,rule,erule conjE)
proof -
@@ -6187,8 +6089,7 @@
apply (drule separating_hyperplane_closed_point[OF assms(2,1)])
apply (erule exE)+
apply (erule_tac x="-a" in allE)
- apply (erule_tac x="-b" in allE)
- apply auto
+ apply (erule_tac x="-b" in allE, auto)
done
qed auto
@@ -6206,7 +6107,7 @@
then show ?thesis
apply (rule_tac x="\<lambda>v. if v\<in>s then u v else 0" in exI)
unfolding if_smult scaleR_zero_left and sum.inter_restrict[OF assms(1), symmetric]
- apply (auto simp add: Int_absorb1)
+ apply (auto simp: Int_absorb1)
done
qed
@@ -6261,8 +6162,7 @@
next
case False
then have "sum u c \<le> sum (\<lambda>x. if x=v then u v else 0) c"
- apply (rule_tac sum_mono)
- apply auto
+ apply (rule_tac sum_mono, auto)
done
then show ?thesis
unfolding sum.delta[OF assms(1)] using uv(2) and \<open>u v < 0\<close> and uv(1) by auto
@@ -6272,20 +6172,18 @@
then have *: "sum u {x\<in>c. u x > 0} > 0"
unfolding less_le
apply (rule_tac conjI)
- apply (rule_tac sum_nonneg)
- apply auto
+ apply (rule_tac sum_nonneg, auto)
done
moreover have "sum u ({x \<in> c. 0 < u x} \<union> {x \<in> c. u x < 0}) = sum u c"
"(\<Sum>x\<in>{x \<in> c. 0 < u x} \<union> {x \<in> c. u x < 0}. u x *\<^sub>R x) = (\<Sum>x\<in>c. u x *\<^sub>R x)"
using assms(1)
- apply (rule_tac[!] sum.mono_neutral_left)
- apply auto
+ apply (rule_tac[!] sum.mono_neutral_left, auto)
done
then have "sum u {x \<in> c. 0 < u x} = - sum u {x \<in> c. 0 > u x}"
"(\<Sum>x\<in>{x \<in> c. 0 < u x}. u x *\<^sub>R x) = - (\<Sum>x\<in>{x \<in> c. 0 > u x}. u x *\<^sub>R x)"
unfolding eq_neg_iff_add_eq_0
using uv(1,4)
- by (auto simp add: sum.union_inter_neutral[OF fin, symmetric])
+ by (auto simp: sum.union_inter_neutral[OF fin, symmetric])
moreover have "\<forall>x\<in>{v \<in> c. u v < 0}. 0 \<le> inverse (sum u {x \<in> c. 0 < u x}) * - u x"
apply rule
apply (rule mult_nonneg_nonneg)
@@ -6297,7 +6195,7 @@
apply (rule_tac x="{v \<in> c. u v < 0}" in exI)
apply (rule_tac x="\<lambda>y. inverse (sum u {x\<in>c. u x > 0}) * - u y" in exI)
using assms(1) unfolding scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] and z_def
- apply (auto simp add: sum_negf sum_distrib_left[symmetric])
+ apply (auto simp: sum_negf sum_distrib_left[symmetric])
done
moreover have "\<forall>x\<in>{v \<in> c. 0 < u v}. 0 \<le> inverse (sum u {x \<in> c. 0 < u x}) * u x"
apply rule
@@ -6312,12 +6210,11 @@
using assms(1)
unfolding scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] and z_def
using *
- apply (auto simp add: sum_negf sum_distrib_left[symmetric])
+ apply (auto simp: sum_negf sum_distrib_left[symmetric])
done
ultimately show ?thesis
apply (rule_tac x="{v\<in>c. u v \<le> 0}" in exI)
- apply (rule_tac x="{v\<in>c. u v > 0}" in exI)
- apply auto
+ apply (rule_tac x="{v\<in>c. u v > 0}" in exI, auto)
done
qed
@@ -6387,8 +6284,7 @@
show ?thesis
unfolding *
unfolding ex_in_conv[symmetric]
- apply (rule_tac x="X s" in exI)
- apply rule
+ apply (rule_tac x="X s" in exI, rule)
apply (rule X[rule_format])
using X st
apply auto
@@ -6419,7 +6315,6 @@
using Suc gh(3-4)
unfolding subset_eq
apply (rule_tac [2] convex_Inter, rule_tac [4] convex_Inter)
- apply rule
prefer 3
apply rule
proof -
@@ -6430,12 +6325,15 @@
then show "x \<in> \<Inter>h"
using X[THEN bspec[where x=y]] using * f by auto
next
+ show "\<forall>x\<in>X ` h. x \<in> \<Inter>g"
+ proof
fix x
assume "x \<in> X ` h"
then obtain y where "y \<in> h" "x = X y"
unfolding image_iff ..
then show "x \<in> \<Inter>g"
using X[THEN bspec[where x=y]] using * f by auto
+ qed
qed auto
then show ?thesis
unfolding f using mp(3)[unfolded gh] by blast
@@ -6468,8 +6366,7 @@
apply safe
defer
apply (erule_tac x=x in allE)
- apply (erule_tac x="f x" in allE)
- apply safe
+ apply (erule_tac x="f x" in allE, safe)
apply (erule_tac x=xa in allE)
apply (erule_tac x="f xa" in allE)
prefer 3
@@ -6491,7 +6388,7 @@
assumes "convex s"
shows "convex_on s f \<longleftrightarrow>
(\<forall>k u x. (\<forall>i\<in>{1..k::nat}. 0 \<le> u i \<and> x i \<in> s) \<and> sum u {1..k} = 1 \<longrightarrow>
- f (sum (\<lambda>i. u i *\<^sub>R x i) {1..k} ) \<le> sum (\<lambda>i. u i * f(x i)) {1..k})"
+ f (sum (\<lambda>i. u i *\<^sub>R x i) {1..k}) \<le> sum (\<lambda>i. u i * f(x i)) {1..k})"
unfolding convex_epigraph_convex[OF assms] convex epigraph_def Ball_def mem_Collect_eq
unfolding fst_sum snd_sum fst_scaleR snd_scaleR
apply safe
@@ -6527,31 +6424,31 @@
fix a b
assume "\<not> b \<le> u * a + v * b"
then have "u * a < (1 - v) * b"
- unfolding not_le using as(4) by (auto simp add: field_simps)
+ unfolding not_le using as(4) by (auto simp: field_simps)
then have "a < b"
unfolding * using as(4) *(2)
apply (rule_tac mult_left_less_imp_less[of "1 - v"])
- apply (auto simp add: field_simps)
+ apply (auto simp: field_simps)
done
then have "a \<le> u * a + v * b"
unfolding * using as(4)
- by (auto simp add: field_simps intro!:mult_right_mono)
+ by (auto simp: field_simps intro!:mult_right_mono)
}
moreover
{
fix a b
assume "\<not> u * a + v * b \<le> a"
then have "v * b > (1 - u) * a"
- unfolding not_le using as(4) by (auto simp add: field_simps)
+ unfolding not_le using as(4) by (auto simp: field_simps)
then have "a < b"
unfolding * using as(4)
apply (rule_tac mult_left_less_imp_less)
- apply (auto simp add: field_simps)
+ apply (auto simp: field_simps)
done
then have "u * a + v * b \<le> b"
unfolding **
using **(2) as(3)
- by (auto simp add: field_simps intro!:mult_right_mono)
+ by (auto simp: field_simps intro!:mult_right_mono)
}
ultimately show "u *\<^sub>R x + v *\<^sub>R y \<in> s"
apply -
@@ -6638,12 +6535,9 @@
ultimately show False
apply (rule_tac notE[OF as(1)[unfolded connected_def]])
apply (rule_tac x = ?halfl in exI)
- apply (rule_tac x = ?halfr in exI)
- apply rule
- apply (rule open_lessThan)
- apply rule
- apply (rule open_greaterThan)
- apply auto
+ apply (rule_tac x = ?halfr in exI, rule)
+ apply (rule open_lessThan, rule)
+ apply (rule open_greaterThan, auto)
done
qed
@@ -6705,7 +6599,7 @@
fixes f :: "real \<Rightarrow> 'a::euclidean_space"
shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a..b}. continuous (at x) f \<Longrightarrow>
f a\<bullet>k \<le> y \<Longrightarrow> y \<le> f b\<bullet>k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)\<bullet>k = y"
- by (rule ivt_increasing_component_on_1) (auto simp add: continuous_at_imp_continuous_on)
+ by (rule ivt_increasing_component_on_1) (auto simp: continuous_at_imp_continuous_on)
lemma ivt_decreasing_component_on_1:
fixes f :: "real \<Rightarrow> 'a::euclidean_space"
@@ -6781,38 +6675,30 @@
lemma set_sum_eq:
"finite A \<Longrightarrow> (\<Sum>i\<in>A. B i) = {\<Sum>i\<in>A. f i |f. \<forall>i\<in>A. f i \<in> B i}"
- apply (induct set: finite)
- apply simp
+ apply (induct set: finite, simp)
apply simp
apply (safe elim!: set_plus_elim)
- apply (rule_tac x="fun_upd f x a" in exI)
- apply simp
+ apply (rule_tac x="fun_upd f x a" in exI, simp)
apply (rule_tac f="\<lambda>x. a + x" in arg_cong)
- apply (rule sum.cong [OF refl])
- apply clarsimp
+ apply (rule sum.cong [OF refl], clarsimp)
apply fast
done
lemma box_eq_set_sum_Basis:
shows "{x. \<forall>i\<in>Basis. x\<bullet>i \<in> B i} = (\<Sum>i\<in>Basis. image (\<lambda>x. x *\<^sub>R i) (B i))"
- apply (subst set_sum_eq [OF finite_Basis])
- apply safe
+ apply (subst set_sum_eq [OF finite_Basis], safe)
apply (fast intro: euclidean_representation [symmetric])
apply (subst inner_sum_left)
apply (subgoal_tac "(\<Sum>x\<in>Basis. f x \<bullet> i) = f i \<bullet> i")
apply (drule (1) bspec)
apply clarsimp
apply (frule sum.remove [OF finite_Basis])
- apply (erule trans)
- apply simp
- apply (rule sum.neutral)
- apply clarsimp
+ apply (erule trans, simp)
+ apply (rule sum.neutral, clarsimp)
apply (frule_tac x=i in bspec, assumption)
- apply (drule_tac x=x in bspec, assumption)
- apply clarsimp
+ apply (drule_tac x=x in bspec, assumption, clarsimp)
apply (cut_tac u=x and v=i in inner_Basis, assumption+)
- apply (rule ccontr)
- apply simp
+ apply (rule ccontr, simp)
done
lemma convex_hull_set_sum:
@@ -6867,8 +6753,7 @@
apply (rule that[of "{x::'a. \<forall>i\<in>Basis. x\<bullet>i=0 \<or> x\<bullet>i=1}"])
apply (rule finite_subset[of _ "(\<lambda>s. (\<Sum>i\<in>Basis. (if i\<in>s then 1 else 0) *\<^sub>R i)::'a) ` Pow Basis"])
prefer 3
- apply (rule unit_interval_convex_hull)
- apply rule
+ apply (rule unit_interval_convex_hull, rule)
unfolding mem_Collect_eq
proof -
fix x :: 'a
@@ -6876,8 +6761,7 @@
show "x \<in> (\<lambda>s. \<Sum>i\<in>Basis. (if i\<in>s then 1 else 0) *\<^sub>R i) ` Pow Basis"
apply (rule image_eqI[where x="{i. i\<in>Basis \<and> x\<bullet>i = 1}"])
using as
- apply (subst euclidean_eq_iff)
- apply auto
+ apply (subst euclidean_eq_iff, auto)
done
qed auto
@@ -6906,13 +6790,7 @@
assume as: "z\<in>cbox 0 (\<Sum>Basis)" "y = x - ?d + (2*d) *\<^sub>R z"
have "\<And>i. i\<in>Basis \<Longrightarrow> 0 \<le> d * (z \<bullet> i) \<and> d * (z \<bullet> i) \<le> d"
using assms as(1)[unfolded mem_box]
- apply (erule_tac x=i in ballE)
- apply rule
- prefer 2
- apply (rule mult_right_le_one_le)
- using assms
- apply auto
- done
+ by auto
then show "y \<in> cbox (x - ?d) (x + ?d)"
unfolding as(2) mem_box
apply -
@@ -6957,13 +6835,13 @@
next
case False
then have *: "\<And>a b. a = m i * b \<longleftrightarrow> b = a / m i"
- by (auto simp add: field_simps)
+ by (auto simp: field_simps)
from False have
"min (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) = (if 0 < m i then m i * (a \<bullet> i) else m i * (b \<bullet> i))"
"max (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) = (if 0 < m i then m i * (b \<bullet> i) else m i * (a \<bullet> i))"
using a_le_b by (auto simp: min_def max_def mult_le_cancel_left)
with False show ?thesis using a_le_b
- unfolding * by (auto simp add: le_divide_eq divide_le_eq ac_simps)
+ unfolding * by (auto simp: le_divide_eq divide_le_eq ac_simps)
qed
qed
qed simp
@@ -6975,7 +6853,7 @@
lemma cbox_translation: "cbox (c + a) (c + b) = image (\<lambda>x. c + x) (cbox a b)"
using image_affinity_cbox [of 1 c a b]
using box_ne_empty [of "a+c" "b+c"] box_ne_empty [of a b]
- by (auto simp add: inner_left_distrib add.commute)
+ by (auto simp: inner_left_distrib add.commute)
lemma cbox_image_unit_interval:
fixes a :: "'a::euclidean_space"
@@ -7045,13 +6923,13 @@
define t where "t = k / norm (y - x)"
have "2 < t" "0<t"
unfolding t_def using as False and \<open>k>0\<close>
- by (auto simp add:field_simps)
+ by (auto simp:field_simps)
have "y \<in> s"
apply (rule k[unfolded subset_eq,rule_format])
unfolding mem_cball dist_norm
apply (rule order_trans[of _ "2 * norm (x - y)"])
using as
- by (auto simp add: field_simps norm_minus_commute)
+ by (auto simp: field_simps norm_minus_commute)
{
define w where "w = x + t *\<^sub>R (y - x)"
have "w \<in> s"
@@ -7063,18 +6941,18 @@
apply auto
done
have "(1 / t) *\<^sub>R x + - x + ((t - 1) / t) *\<^sub>R x = (1 / t - 1 + (t - 1) / t) *\<^sub>R x"
- by (auto simp add: algebra_simps)
+ by (auto simp: algebra_simps)
also have "\<dots> = 0"
- using \<open>t > 0\<close> by (auto simp add:field_simps)
+ using \<open>t > 0\<close> by (auto simp:field_simps)
finally have w: "(1 / t) *\<^sub>R w + ((t - 1) / t) *\<^sub>R x = y"
unfolding w_def using False and \<open>t > 0\<close>
- by (auto simp add: algebra_simps)
+ by (auto simp: algebra_simps)
have "2 * B < e * t"
unfolding t_def using \<open>0 < e\<close> \<open>0 < k\<close> \<open>B > 0\<close> and as and False
- by (auto simp add:field_simps)
+ by (auto simp:field_simps)
then have "(f w - f x) / t < e"
using B(2)[OF \<open>w\<in>s\<close>] and B(2)[OF \<open>x\<in>s\<close>]
- using \<open>t > 0\<close> by (auto simp add:field_simps)
+ using \<open>t > 0\<close> by (auto simp:field_simps)
then have th1: "f y - f x < e"
apply -
apply (rule le_less_trans)
@@ -7082,7 +6960,7 @@
apply assumption
using assms(2)[unfolded convex_on_def,rule_format,of w x "1/t" "(t - 1)/t", unfolded w]
using \<open>0 < t\<close> \<open>2 < t\<close> and \<open>x \<in> s\<close> \<open>w \<in> s\<close>
- by (auto simp add:field_simps)
+ by (auto simp:field_simps)
}
moreover
{
@@ -7096,28 +6974,28 @@
apply auto
done
have "(1 / (1 + t)) *\<^sub>R x + (t / (1 + t)) *\<^sub>R x = (1 / (1 + t) + t / (1 + t)) *\<^sub>R x"
- by (auto simp add: algebra_simps)
+ by (auto simp: algebra_simps)
also have "\<dots> = x"
- using \<open>t > 0\<close> by (auto simp add:field_simps)
+ using \<open>t > 0\<close> by (auto simp:field_simps)
finally have w: "(1 / (1+t)) *\<^sub>R w + (t / (1 + t)) *\<^sub>R y = x"
unfolding w_def using False and \<open>t > 0\<close>
- by (auto simp add: algebra_simps)
+ by (auto simp: algebra_simps)
have "2 * B < e * t"
unfolding t_def
using \<open>0 < e\<close> \<open>0 < k\<close> \<open>B > 0\<close> and as and False
- by (auto simp add:field_simps)
+ by (auto simp:field_simps)
then have *: "(f w - f y) / t < e"
using B(2)[OF \<open>w\<in>s\<close>] and B(2)[OF \<open>y\<in>s\<close>]
using \<open>t > 0\<close>
- by (auto simp add:field_simps)
+ by (auto simp:field_simps)
have "f x \<le> 1 / (1 + t) * f w + (t / (1 + t)) * f y"
using assms(2)[unfolded convex_on_def,rule_format,of w y "1/(1+t)" "t / (1+t)",unfolded w]
using \<open>0 < t\<close> \<open>2 < t\<close> and \<open>y \<in> s\<close> \<open>w \<in> s\<close>
- by (auto simp add:field_simps)
+ by (auto simp:field_simps)
also have "\<dots> = (f w + t * f y) / (1 + t)"
- using \<open>t > 0\<close> by (auto simp add: divide_simps)
+ using \<open>t > 0\<close> by (auto simp: divide_simps)
also have "\<dots> < e + f y"
- using \<open>t > 0\<close> * \<open>e > 0\<close> by (auto simp add: field_simps)
+ using \<open>t > 0\<close> * \<open>e > 0\<close> by (auto simp: field_simps)
finally have "f x - f y < e" by auto
}
ultimately show ?thesis by auto
@@ -7142,13 +7020,13 @@
have *: "x - (2 *\<^sub>R x - y) = y - x"
by (simp add: scaleR_2)
have z: "z \<in> cball x e"
- using y unfolding z_def mem_cball dist_norm * by (auto simp add: norm_minus_commute)
+ using y unfolding z_def mem_cball dist_norm * by (auto simp: norm_minus_commute)
have "(1 / 2) *\<^sub>R y + (1 / 2) *\<^sub>R z = x"
- unfolding z_def by (auto simp add: algebra_simps)
+ unfolding z_def by (auto simp: algebra_simps)
then show "\<bar>f y\<bar> \<le> b + 2 * \<bar>f x\<bar>"
using assms(1)[unfolded convex_on_def,rule_format, OF y z, of "1/2" "1/2"]
using assms(2)[rule_format,OF y] assms(2)[rule_format,OF z]
- by (auto simp add:field_simps)
+ by (auto simp:field_simps)
next
case False
fix y
@@ -7203,8 +7081,7 @@
unfolding 2
apply clarsimp
apply (simp only: dist_norm)
- apply (subst inner_diff_left [symmetric])
- apply simp
+ apply (subst inner_diff_left [symmetric], simp)
apply (erule (1) order_trans [OF Basis_le_norm])
done
have e': "e = (\<Sum>(i::'a)\<in>Basis. d)"
@@ -7216,8 +7093,7 @@
apply (rule order_trans [OF L2_set_le_sum])
apply (rule zero_le_dist)
unfolding e'
- apply (rule sum_mono)
- apply simp
+ apply (rule sum_mono, simp)
done
qed
define k where "k = Max (f ` c)"
@@ -7227,8 +7103,7 @@
apply(rule c1)
done
then have k: "\<forall>y\<in>convex hull c. f y \<le> k"
- apply (rule_tac convex_on_convex_hull_bound)
- apply assumption
+ apply (rule_tac convex_on_convex_hull_bound, assumption)
unfolding k_def
apply (rule, rule Max_ge)
using c(1)
@@ -7244,11 +7119,7 @@
then have dsube: "cball x d \<subseteq> cball x e"
by (rule subset_cball)
have conv: "convex_on (cball x d) f"
- apply (rule convex_on_subset)
- apply (rule convex_on_subset[OF assms(2)])
- apply (rule e(1))
- apply (rule dsube)
- done
+ using \<open>convex_on (convex hull c) f\<close> c2 convex_on_subset by blast
then have "\<forall>y\<in>cball x d. \<bar>f y\<bar> \<le> k + 2 * \<bar>f x\<bar>"
apply (rule convex_bounds_lemma)
apply (rule ballI)
@@ -7259,8 +7130,7 @@
then have "continuous_on (ball x d) f"
apply (rule_tac convex_on_bounded_continuous)
apply (rule open_ball, rule convex_on_subset[OF conv])
- apply (rule ball_subset_cball)
- apply force
+ apply (rule ball_subset_cball, force)
done
then show "continuous (at x) f"
unfolding continuous_on_eq_continuous_at[OF open_ball]