# HG changeset patch
# User nipkow
# Date 1575648238 -3600
# Node ID 38457af660bc89eee6ff1585de640db7f86ac1d5
# Parent  5b7c85586eb1c38abe9c12d9d08b045e762e036f
cleaning

diff -r 5b7c85586eb1 -r 38457af660bc src/HOL/Analysis/Convex.thy
--- 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"
diff -r 5b7c85586eb1 -r 38457af660bc src/HOL/Analysis/Convex_Euclidean_Space.thy
--- 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
 
diff -r 5b7c85586eb1 -r 38457af660bc src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- 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)))"
diff -r 5b7c85586eb1 -r 38457af660bc src/HOL/Analysis/Path_Connected.thy
--- 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"
diff -r 5b7c85586eb1 -r 38457af660bc src/HOL/Analysis/Polytope.thy
--- 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)
diff -r 5b7c85586eb1 -r 38457af660bc src/HOL/Analysis/Starlike.thy
--- 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