--- a/src/HOL/Analysis/Convex.thy Fri Dec 06 14:36:11 2019 +0100
+++ b/src/HOL/Analysis/Convex.thy Fri Dec 06 17:03:58 2019 +0100
@@ -562,36 +562,6 @@
using convex_translation[OF convex_scaling[OF assms], of a c] by auto
qed
-lemma pos_is_convex: "convex {0 :: real <..}"
- unfolding convex_alt
-proof safe
- fix y x \<mu> :: real
- assume *: "y > 0" "x > 0" "\<mu> \<ge> 0" "\<mu> \<le> 1"
- {
- assume "\<mu> = 0"
- then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y = y"
- by simp
- then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0"
- using * by simp
- }
- moreover
- {
- assume "\<mu> = 1"
- then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0"
- using * by simp
- }
- moreover
- {
- assume "\<mu> \<noteq> 1" "\<mu> \<noteq> 0"
- then have "\<mu> > 0" "(1 - \<mu>) > 0"
- using * by auto
- then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0"
- using * by (auto simp: add_pos_pos)
- }
- ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0"
- by fastforce
-qed
-
lemma convex_on_sum:
fixes a :: "'a \<Rightarrow> real"
and y :: "'a \<Rightarrow> 'b::real_vector"
@@ -923,7 +893,7 @@
unfolding inverse_eq_divide by (auto simp: mult.assoc)
have f''_ge0: "\<And>z::real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
using \<open>b > 1\<close> by (auto intro!: less_imp_le)
- from f''_ge0_imp_convex[OF pos_is_convex, unfolded greaterThan_iff, OF f' f''0 f''_ge0]
+ from f''_ge0_imp_convex[OF convex_real_interval(3), unfolded greaterThan_iff, OF f' f''0 f''_ge0]
show ?thesis
by auto
qed
@@ -1049,12 +1019,6 @@
shows "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> convex (f ` s) \<longleftrightarrow> convex s"
by (metis (no_types) convex_linear_image convex_linear_vimage inj_vimage_image_eq)
-lemma fst_linear: "linear fst"
- unfolding linear_iff by (simp add: algebra_simps)
-
-lemma snd_linear: "linear snd"
- unfolding linear_iff by (simp add: algebra_simps)
-
lemma fst_snd_linear: "linear (\<lambda>(x,y). x + y)"
unfolding linear_iff by (simp add: algebra_simps)
@@ -1284,10 +1248,6 @@
subsection\<^marker>\<open>tag unimportant\<close> \<open>Connectedness of convex sets\<close>
-lemma connectedD:
- "connected S \<Longrightarrow> open A \<Longrightarrow> open B \<Longrightarrow> S \<subseteq> A \<union> B \<Longrightarrow> A \<inter> B \<inter> S = {} \<Longrightarrow> A \<inter> S = {} \<or> B \<inter> S = {}"
- by (rule Topological_Spaces.topological_space_class.connectedD)
-
lemma convex_connected:
fixes S :: "'a::real_normed_vector set"
assumes "convex S"
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Fri Dec 06 14:36:11 2019 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Fri Dec 06 17:03:58 2019 +0100
@@ -180,9 +180,6 @@
shows "rel_interior S = S"
by (metis assms interior_eq interior_subset_rel_interior rel_interior_subset set_eq_subset)
-lemma interior_ball [simp]: "interior (ball x e) = ball x e"
- by (simp add: interior_open)
-
lemma interior_rel_interior_gen:
fixes S :: "'n::euclidean_space set"
shows "interior S = (if aff_dim S = int(DIM('n)) then rel_interior S else {})"
@@ -1200,16 +1197,13 @@
lemma closest_point_exists:
assumes "closed S"
and "S \<noteq> {}"
- shows "closest_point S a \<in> S"
+ shows closest_point_in_set: "closest_point S a \<in> S"
and "\<forall>y\<in>S. dist a (closest_point S a) \<le> dist a y"
unfolding closest_point_def
apply(rule_tac[!] someI2_ex)
apply (auto intro: distance_attains_inf[OF assms(1,2), of a])
done
-lemma closest_point_in_set: "closed S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> closest_point S a \<in> S"
- by (meson closest_point_exists)
-
lemma closest_point_le: "closed S \<Longrightarrow> x \<in> S \<Longrightarrow> dist a (closest_point S a) \<le> dist a x"
using closest_point_exists[of S] by auto
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Dec 06 14:36:11 2019 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Dec 06 17:03:58 2019 +0100
@@ -1999,7 +1999,7 @@
using diff_f
apply (clarsimp simp add: differentiable_on_def)
apply (intro differentiable_chain_within linear_imp_differentiable [OF \<open>linear drop\<close>]
- linear_imp_differentiable [OF fst_linear])
+ linear_imp_differentiable [OF linear_fst])
apply (force simp: image_comp o_def)
done
have "f = (f o fst o drop o (\<lambda>x. lift (x, 0)))"
--- a/src/HOL/Analysis/Path_Connected.thy Fri Dec 06 14:36:11 2019 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy Fri Dec 06 17:03:58 2019 +0100
@@ -2910,7 +2910,7 @@
have "T \<inter> \<Union>(B - {T}) = {}" using \<open>T \<in> B\<close> \<open>pairwise disjnt B\<close>
by (auto simp: pairwise_def disjnt_def)
then have 4: "T \<inter> \<Union>(B - {T}) \<inter> S = {}" by auto
- from connectedD [OF \<open>connected S\<close> 1 2 3 4]
+ from connectedD [OF \<open>connected S\<close> 1 2 4 3]
have "S \<inter> \<Union>(B-{T}) = {}"
by (auto simp: Int_commute \<open>S \<inter> T \<noteq> {}\<close>)
with \<open>T \<in> B\<close> have "S \<subseteq> T"
--- a/src/HOL/Analysis/Polytope.thy Fri Dec 06 14:36:11 2019 +0100
+++ b/src/HOL/Analysis/Polytope.thy Fri Dec 06 17:03:58 2019 +0100
@@ -545,7 +545,7 @@
have "convex c"
using c by (metis face_of_imp_convex)
have conv: "convex (fst ` c)" "convex (snd ` c)"
- by (simp_all add: \<open>convex c\<close> convex_linear_image fst_linear snd_linear)
+ by (simp_all add: \<open>convex c\<close> convex_linear_image linear_fst linear_snd)
have fstab: "a \<in> fst ` c \<and> b \<in> fst ` c"
if "a \<in> S" "b \<in> S" "x \<in> open_segment a b" "(x,x') \<in> c" for a b x x'
proof -
@@ -567,7 +567,7 @@
have snd: "snd ` c face_of S'"
by (force simp: face_of_def 1 conv sndab)
have cc: "rel_interior c \<subseteq> rel_interior (fst ` c) \<times> rel_interior (snd ` c)"
- by (force simp: face_of_Times rel_interior_Times conv fst snd \<open>convex c\<close> fst_linear snd_linear rel_interior_convex_linear_image [symmetric])
+ by (force simp: face_of_Times rel_interior_Times conv fst snd \<open>convex c\<close> linear_fst linear_snd rel_interior_convex_linear_image [symmetric])
have "c = fst ` c \<times> snd ` c"
apply (rule face_of_eq [OF c])
apply (simp_all add: face_of_Times rel_interior_Times conv fst snd)
--- a/src/HOL/Analysis/Starlike.thy Fri Dec 06 14:36:11 2019 +0100
+++ b/src/HOL/Analysis/Starlike.thy Fri Dec 06 17:03:58 2019 +0100
@@ -1830,13 +1830,13 @@
then have "fst -` rel_interior S \<noteq> {}"
using fst_vimage_eq_Times[of "rel_interior S"] by auto
then have "rel_interior ((fst :: 'n * 'm \<Rightarrow> 'n) -` S) = fst -` rel_interior S"
- using fst_linear \<open>convex S\<close> rel_interior_convex_linear_preimage[of fst S] by auto
+ using linear_fst \<open>convex S\<close> rel_interior_convex_linear_preimage[of fst S] by auto
then have s: "rel_interior (S \<times> (UNIV :: 'm set)) = rel_interior S \<times> UNIV"
by (simp add: fst_vimage_eq_Times)
from ri have "snd -` rel_interior T \<noteq> {}"
using snd_vimage_eq_Times[of "rel_interior T"] by auto
then have "rel_interior ((snd :: 'n * 'm \<Rightarrow> 'm) -` T) = snd -` rel_interior T"
- using snd_linear \<open>convex T\<close> rel_interior_convex_linear_preimage[of snd T] by auto
+ using linear_snd \<open>convex T\<close> rel_interior_convex_linear_preimage[of snd T] by auto
then have t: "rel_interior ((UNIV :: 'n set) \<times> T) = UNIV \<times> rel_interior T"
by (simp add: snd_vimage_eq_Times)
from s t have *: "rel_interior (S \<times> (UNIV :: 'm set)) \<inter> rel_interior ((UNIV :: 'n set) \<times> T) =
@@ -1951,7 +1951,7 @@
then have "fst ` S = {y. f y \<noteq> {}}"
unfolding fst_def using assms by auto
then have h1: "fst ` rel_interior S = rel_interior {y. f y \<noteq> {}}"
- using rel_interior_convex_linear_image[of fst S] assms fst_linear by auto
+ using rel_interior_convex_linear_image[of fst S] assms linear_fst by auto
{
fix y
assume "y \<in> rel_interior {y. f y \<noteq> {}}"
@@ -1977,7 +1977,7 @@
then have "snd ` (S \<inter> fst -` {y}) = f y"
using assms by auto
then have ***: "rel_interior (f y) = snd ` rel_interior (S \<inter> fst -` {y})"
- using rel_interior_convex_linear_image[of snd "S \<inter> fst -` {y}"] snd_linear conv
+ using rel_interior_convex_linear_image[of snd "S \<inter> fst -` {y}"] linear_snd conv
by auto
{
fix z