# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1460986232 -3600
# Node ID aa894a49f77d978651b00369fb2c81dbe2fb0755
# Parent  89d19aa73081a487d42f8d96dbb592aa95e550d9
new theorems about convex hulls, etc.; also, renamed some theorems

diff -r 89d19aa73081 -r aa894a49f77d src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Sun Apr 17 22:38:50 2016 +0200
+++ b/src/HOL/Library/Convex.thy	Mon Apr 18 14:30:32 2016 +0100
@@ -65,13 +65,13 @@
 lemma convex_UNIV[intro,simp]: "convex UNIV"
   unfolding convex_def by auto
 
-lemma convex_Inter: "(\<forall>s\<in>f. convex s) \<Longrightarrow> convex(\<Inter>f)"
+lemma convex_Inter: "(\<And>s. s\<in>f \<Longrightarrow> convex s) \<Longrightarrow> convex(\<Inter>f)"
   unfolding convex_def by auto
 
 lemma convex_Int: "convex s \<Longrightarrow> convex t \<Longrightarrow> convex (s \<inter> t)"
   unfolding convex_def by auto
 
-lemma convex_INT: "\<forall>i\<in>A. convex (B i) \<Longrightarrow> convex (\<Inter>i\<in>A. B i)"
+lemma convex_INT: "(\<And>i. i \<in> A \<Longrightarrow> convex (B i)) \<Longrightarrow> convex (\<Inter>i\<in>A. B i)"
   unfolding convex_def by auto
 
 lemma convex_Times: "convex s \<Longrightarrow> convex t \<Longrightarrow> convex (s \<times> t)"
diff -r 89d19aa73081 -r aa894a49f77d src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Apr 17 22:38:50 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Apr 18 14:30:32 2016 +0100
@@ -420,7 +420,7 @@
 lemma affine_UNIV [iff]: "affine UNIV"
   unfolding affine_def by auto
 
-lemma affine_Inter[intro]: "(\<forall>s\<in>f. affine s) \<Longrightarrow> affine (\<Inter>f)"
+lemma affine_Inter [intro]: "(\<And>s. s\<in>f \<Longrightarrow> affine s) \<Longrightarrow> affine (\<Inter>f)"
   unfolding affine_def by auto
 
 lemma affine_Int[intro]: "affine s \<Longrightarrow> affine t \<Longrightarrow> affine (s \<inter> t)"
@@ -1274,6 +1274,20 @@
 definition affine_dependent :: "'a::real_vector set \<Rightarrow> bool"
   where "affine_dependent s \<longleftrightarrow> (\<exists>x\<in>s. x \<in> affine hull (s - {x}))"
 
+lemma affine_dependent_subset:
+   "\<lbrakk>affine_dependent s; s \<subseteq> t\<rbrakk> \<Longrightarrow> affine_dependent t"
+apply (simp add: affine_dependent_def Bex_def)
+apply (blast dest: hull_mono [OF Diff_mono [OF _ subset_refl]])
+done
+
+lemma affine_independent_subset:
+  shows "\<lbrakk>~ affine_dependent t; s \<subseteq> t\<rbrakk> \<Longrightarrow> ~ affine_dependent s"
+by (metis affine_dependent_subset)
+
+lemma affine_independent_Diff:
+   "~ affine_dependent s \<Longrightarrow> ~ affine_dependent(s - t)"
+by (meson Diff_subset affine_dependent_subset)
+
 lemma affine_dependent_explicit:
   "affine_dependent p \<longleftrightarrow>
     (\<exists>s u. finite s \<and> s \<subseteq> p \<and> setsum u s = 0 \<and>
@@ -1392,6 +1406,11 @@
     shows "\<lbrakk>finite S; open S\<rbrakk> \<Longrightarrow> S={}"
   using clopen [of S] finite_imp_closed not_bounded_UNIV by blast
 
+corollary empty_interior_finite:
+    fixes S :: "'a::{real_normed_vector, perfect_space} set"
+    shows "finite S \<Longrightarrow> interior S = {}"
+  by (metis interior_subset finite_subset open_interior [of S] finite_imp_not_open)
+
 text \<open>Balls, being convex, are connected.\<close>
 
 lemma convex_prod:
@@ -2261,12 +2280,15 @@
 
 subsection \<open>Some Properties of Affine Dependent Sets\<close>
 
-lemma affine_independent_empty: "\<not> affine_dependent {}"
+lemma affine_independent_0: "\<not> affine_dependent {}"
   by (simp add: affine_dependent_def)
 
-lemma affine_independent_sing: "\<not> affine_dependent {a}"
+lemma affine_independent_1: "\<not> affine_dependent {a}"
   by (simp add: affine_dependent_def)
 
+lemma affine_independent_2: "\<not> affine_dependent {a,b}"
+  by (simp add: affine_dependent_def insert_Diff_if hull_same)
+
 lemma affine_hull_translation: "affine hull ((\<lambda>x. a + x) `  S) = (\<lambda>x. a + x) ` (affine hull S)"
 proof -
   have "affine ((\<lambda>x. a + x) ` (affine hull S))"
@@ -2473,7 +2495,7 @@
 proof (cases "V = {}")
   case True
   then show ?thesis
-    using affine_independent_empty by auto
+    using affine_independent_0 by auto
 next
   case False
   then obtain x where "x \<in> V" by auto
@@ -2756,7 +2778,7 @@
 lemma aff_dim_sing [simp]:
   fixes a :: "'n::euclidean_space"
   shows "aff_dim {a} = 0"
-  using aff_dim_affine_independent[of "{a}"] affine_independent_sing by auto
+  using aff_dim_affine_independent[of "{a}"] affine_independent_1 by auto
 
 lemma aff_dim_inner_basis_exists:
   fixes V :: "('n::euclidean_space) set"
@@ -2937,7 +2959,7 @@
   with B show ?thesis by auto
 qed
 
-lemma aff_dim_subset_univ:
+lemma aff_dim_le_DIM:
   fixes S :: "'n::euclidean_space set"
   shows "aff_dim S \<le> int (DIM('n))"
 proof -
@@ -2978,7 +3000,7 @@
   ultimately show ?thesis by auto
 qed
 
-lemma affine_hull_univ:
+lemma affine_hull_UNIV:
   fixes S :: "'n::euclidean_space set"
   assumes "aff_dim S = int(DIM('n))"
   shows "affine hull S = (UNIV :: ('n::euclidean_space) set)"
@@ -2990,7 +3012,7 @@
   have h1: "aff_dim (UNIV :: ('n::euclidean_space) set) = aff_dim S"
     using aff_dim_univ assms by auto
   then have h2: "aff_dim (affine hull S) \<le> aff_dim (UNIV :: ('n::euclidean_space) set)"
-    using aff_dim_subset_univ[of "affine hull S"] assms h0 by auto
+    using aff_dim_le_DIM[of "affine hull S"] assms h0 by auto
   have h3: "aff_dim S \<le> aff_dim (affine hull S)"
     using h0 aff_dim_subset[of S "affine hull S"] assms by auto
   then have h4: "aff_dim (affine hull S) = aff_dim (UNIV :: ('n::euclidean_space) set)"
@@ -3001,6 +3023,34 @@
     by auto
 qed
 
+lemma disjoint_affine_hull:
+  fixes s :: "'n::euclidean_space set"
+  assumes "~ affine_dependent s" "t \<subseteq> s" "u \<subseteq> s" "t \<inter> u = {}"
+    shows "(affine hull t) \<inter> (affine hull u) = {}"
+proof -
+  have "finite s" using assms by (simp add: aff_independent_finite)
+  then have "finite t" "finite u" using assms finite_subset by blast+
+  { fix y
+    assume yt: "y \<in> affine hull t" and yu: "y \<in> affine hull u"
+    then obtain a b
+           where a1 [simp]: "setsum a t = 1" and [simp]: "setsum (\<lambda>v. a v *\<^sub>R v) t = y"
+             and [simp]: "setsum b u = 1" "setsum (\<lambda>v. b v *\<^sub>R v) u = y"
+      by (auto simp: affine_hull_finite \<open>finite t\<close> \<open>finite u\<close>)
+    def c \<equiv> "\<lambda>x. if x \<in> t then a x else if x \<in> u then -(b x) else 0"
+    have [simp]: "s \<inter> t = t" "s \<inter> - t \<inter> u = u" using assms by auto
+    have "setsum c s = 0"
+      by (simp add: c_def comm_monoid_add_class.setsum.If_cases \<open>finite s\<close> setsum_negf)
+    moreover have "~ (\<forall>v\<in>s. c v = 0)"
+      by (metis (no_types) IntD1 \<open>s \<inter> t = t\<close> a1 c_def setsum_not_0 zero_neq_one)
+    moreover have "(\<Sum>v\<in>s. c v *\<^sub>R v) = 0"
+      by (simp add: c_def if_smult setsum_negf
+             comm_monoid_add_class.setsum.If_cases \<open>finite s\<close>)
+    ultimately have False
+      using assms \<open>finite s\<close> by (auto simp: affine_dependent_explicit)
+  }
+  then show ?thesis by blast
+qed
+
 lemma aff_dim_convex_hull:
   fixes S :: "'n::euclidean_space set"
   shows "aff_dim (convex hull S) = aff_dim S"
@@ -3025,7 +3075,7 @@
       centre_in_cball[of "(0 :: 'n::euclidean_space)"] assms
     by (simp add: dim_cball[of e] aff_dim_zero[of "cball 0 e"])
   ultimately show ?thesis
-    using aff_dim_subset_univ[of "cball a e"] by auto
+    using aff_dim_le_DIM[of "cball a e"] by auto
 qed
 
 lemma aff_dim_open:
@@ -3041,7 +3091,7 @@
   then have "aff_dim (cball x e) \<le> aff_dim S"
     using aff_dim_subset by auto
   with e show ?thesis
-    using aff_dim_cball[of e x] aff_dim_subset_univ[of S] by auto
+    using aff_dim_cball[of e x] aff_dim_le_DIM[of S] by auto
 qed
 
 lemma low_dim_interior:
@@ -3052,13 +3102,13 @@
   have "aff_dim(interior S) \<le> aff_dim S"
     using interior_subset aff_dim_subset[of "interior S" S] by auto
   then show ?thesis
-    using aff_dim_open[of "interior S"] aff_dim_subset_univ[of S] assms by auto
+    using aff_dim_open[of "interior S"] aff_dim_le_DIM[of S] assms by auto
 qed
 
 corollary empty_interior_lowdim:
   fixes S :: "'n::euclidean_space set"
   shows "dim S < DIM ('n) \<Longrightarrow> interior S = {}"
-by (metis low_dim_interior affine_hull_univ dim_affine_hull less_not_refl dim_UNIV)
+by (metis low_dim_interior affine_hull_UNIV dim_affine_hull less_not_refl dim_UNIV)
 
 subsection \<open>Caratheodory's theorem.\<close>
 
@@ -3185,7 +3235,7 @@
   assume "x \<in> ?lhs" then show "x \<in> ?rhs"
     apply (simp only: convex_hull_caratheodory_aff_dim Set.mem_Collect_eq)
     apply (erule ex_forward)+
-    using aff_dim_subset_univ [of p]
+    using aff_dim_le_DIM [of p]
     apply simp
     done
 next
@@ -3303,7 +3353,7 @@
   shows "rel_interior S = interior S"
 proof -
   have "affine hull S = UNIV"
-    using assms affine_hull_univ[of S] by auto
+    using assms affine_hull_UNIV[of S] by auto
   then show ?thesis
     unfolding rel_interior interior_def by auto
 qed
@@ -3328,7 +3378,17 @@
   shows "interior S = (if aff_dim S = int(DIM('n)) then rel_interior S else {})"
   by (metis interior_rel_interior low_dim_interior)
 
-lemma rel_interior_univ:
+lemma rel_interior_nonempty_interior:
+  fixes S :: "'n::euclidean_space set"
+  shows "interior S \<noteq> {} \<Longrightarrow> rel_interior S = interior S"
+by (metis interior_rel_interior_gen)
+
+lemma affine_hull_nonempty_interior:
+  fixes S :: "'n::euclidean_space set"
+  shows "interior S \<noteq> {} \<Longrightarrow> affine hull S = UNIV"
+by (metis affine_hull_UNIV interior_rel_interior_gen)
+
+lemma rel_interior_affine_hull [simp]:
   fixes S :: "'n::euclidean_space set"
   shows "rel_interior (affine hull S) = affine hull S"
 proof -
@@ -3346,7 +3406,7 @@
   then show ?thesis using * by auto
 qed
 
-lemma rel_interior_univ2: "rel_interior (UNIV :: ('n::euclidean_space) set) = UNIV"
+lemma rel_interior_UNIV [simp]: "rel_interior (UNIV :: ('n::euclidean_space) set) = UNIV"
   by (metis open_UNIV rel_interior_open)
 
 lemma rel_interior_convex_shrink:
@@ -3535,7 +3595,7 @@
   assumes "affine S"
   shows "rel_open S"
   unfolding rel_open_def
-  using assms rel_interior_univ[of S] affine_hull_eq[of S]
+  using assms rel_interior_affine_hull[of S] affine_hull_eq[of S]
   by metis
 
 lemma affine_closed:
@@ -6111,6 +6171,82 @@
     done
 qed
 
+subsubsection\<open>Representation of any interval as a finite convex hull\<close>
+
+lemma image_stretch_interval:
+  "(\<lambda>x. \<Sum>k\<in>Basis. (m k * (x\<bullet>k)) *\<^sub>R k) ` cbox a (b::'a::euclidean_space) =
+  (if (cbox a b) = {} then {} else
+    cbox (\<Sum>k\<in>Basis. (min (m k * (a\<bullet>k)) (m k * (b\<bullet>k))) *\<^sub>R k::'a)
+     (\<Sum>k\<in>Basis. (max (m k * (a\<bullet>k)) (m k * (b\<bullet>k))) *\<^sub>R k))"
+proof cases
+  assume *: "cbox a b \<noteq> {}"
+  show ?thesis
+    unfolding box_ne_empty if_not_P[OF *]
+    apply (simp add: cbox_def image_Collect set_eq_iff euclidean_eq_iff[where 'a='a] ball_conj_distrib[symmetric])
+    apply (subst choice_Basis_iff[symmetric])
+  proof (intro allI ball_cong refl)
+    fix x i :: 'a assume "i \<in> Basis"
+    with * have a_le_b: "a \<bullet> i \<le> b \<bullet> i"
+      unfolding box_ne_empty by auto
+    show "(\<exists>xa. x \<bullet> i = m i * xa \<and> a \<bullet> i \<le> xa \<and> xa \<le> b \<bullet> i) \<longleftrightarrow>
+        min (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) \<le> x \<bullet> i \<and> x \<bullet> i \<le> max (m i * (a \<bullet> i)) (m i * (b \<bullet> i))"
+    proof (cases "m i = 0")
+      case True
+      with a_le_b show ?thesis by auto
+    next
+      case False
+      then have *: "\<And>a b. a = m i * b \<longleftrightarrow> b = a / m i"
+        by (auto simp add: 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)
+    qed
+  qed
+qed simp
+
+lemma interval_image_stretch_interval:
+  "\<exists>u v. (\<lambda>x. \<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k) ` cbox a (b::'a::euclidean_space) = cbox u (v::'a::euclidean_space)"
+  unfolding image_stretch_interval by auto
+
+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)
+
+lemma cbox_image_unit_interval:
+  fixes a :: "'a::euclidean_space"
+  assumes "cbox a b \<noteq> {}"
+    shows "cbox a b =
+           op + a ` (\<lambda>x. \<Sum>k\<in>Basis. ((b \<bullet> k - a \<bullet> k) * (x \<bullet> k)) *\<^sub>R k) ` cbox 0 One"
+using assms
+apply (simp add: box_ne_empty image_stretch_interval cbox_translation [symmetric])
+apply (simp add: min_def max_def algebra_simps setsum_subtractf euclidean_representation)
+done
+
+lemma closed_interval_as_convex_hull:
+  fixes a :: "'a::euclidean_space"
+  obtains s where "finite s" "cbox a b = convex hull s"
+proof (cases "cbox a b = {}")
+  case True with convex_hull_empty that show ?thesis
+    by blast
+next
+  case False
+  obtain s::"'a set" where "finite s" and eq: "cbox 0 One = convex hull s"
+    by (blast intro: unit_cube_convex_hull)
+  have lin: "linear (\<lambda>x. \<Sum>k\<in>Basis. ((b \<bullet> k - a \<bullet> k) * (x \<bullet> k)) *\<^sub>R k)"
+    by (rule linear_compose_setsum) (auto simp: algebra_simps linearI)
+  have "finite (op + a ` (\<lambda>x. \<Sum>k\<in>Basis. ((b \<bullet> k - a \<bullet> k) * (x \<bullet> k)) *\<^sub>R k) ` s)"
+    by (rule finite_imageI \<open>finite s\<close>)+
+  then show ?thesis
+    apply (rule that)
+    apply (simp add: convex_hull_translation convex_hull_linear_image [OF lin, symmetric])
+    apply (simp add: eq [symmetric] cbox_image_unit_interval [OF False])
+    done
+qed
+
 
 subsection \<open>Bounded convex function on open set is continuous\<close>
 
@@ -6392,6 +6528,32 @@
     "x \<in> open_segment a b \<longleftrightarrow> a \<noteq> b \<and> (\<exists>u. 0 < u \<and> u < 1 \<and> x = (1 - u) *\<^sub>R a + u *\<^sub>R b)"
   using less_eq_real_def by (auto simp: segment algebra_simps)
 
+lemma open_segment_PairD:
+  "(x, x') \<in> open_segment (a, a') (b, b')
+  \<Longrightarrow> (x \<in> open_segment a b \<or> a = b) \<and> (x' \<in> open_segment a' b' \<or> a' = b')"
+  by (auto simp: in_segment)
+
+lemma closed_segment_PairD:
+  "(x, x') \<in> closed_segment (a, a') (b, b') \<Longrightarrow> x \<in> closed_segment a b \<and> x' \<in> closed_segment a' b'"
+  by (auto simp: closed_segment_def)
+
+lemma closed_segment_translation_eq [simp]:
+    "d + x \<in> closed_segment (d + a) (d + b) \<longleftrightarrow> x \<in> closed_segment a b"
+proof -
+  have *: "\<And>d x a b. x \<in> closed_segment a b \<Longrightarrow> d + x \<in> closed_segment (d + a) (d + b)"
+    apply (simp add: closed_segment_def)
+    apply (erule ex_forward)
+    apply (simp add: algebra_simps)
+    done
+  show ?thesis
+  using * [where d = "-d"] *
+  by (fastforce simp add:)
+qed
+
+lemma open_segment_translation_eq [simp]:
+    "d + x \<in> open_segment (d + a) (d + b) \<longleftrightarrow> x \<in> open_segment a b"
+  by (simp add: open_segment_def)
+
 definition "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
 
 definition "starlike s \<longleftrightarrow> (\<exists>a\<in>s. \<forall>x\<in>s. closed_segment a x \<subseteq> s)"
@@ -7954,6 +8116,16 @@
   shows "closed (affine hull S)"
   by (metis affine_affine_hull affine_closed)
 
+lemma rel_frontier_nonempty_interior:
+  fixes S :: "'n::euclidean_space set"
+  shows "interior S \<noteq> {} \<Longrightarrow> rel_frontier S = frontier S"
+by (metis frontier_def interior_rel_interior_gen rel_frontier_def)
+
+lemma rel_frontier_frontier:
+  fixes S :: "'n::euclidean_space set"
+  shows "affine hull S = UNIV \<Longrightarrow> rel_frontier S = frontier S"
+by (simp add: frontier_def rel_frontier_def rel_interior_interior)
+
 lemma closed_rel_frontier:
   fixes S :: "'n::euclidean_space set"
   shows "closed (rel_frontier S)"
@@ -8199,7 +8371,7 @@
   then have "S \<noteq> {}"
     using aff_dim_empty[of S] by auto
   have *: "affine hull S = UNIV"
-    using True affine_hull_univ by auto
+    using True affine_hull_UNIV by auto
   {
     assume "z \<in> interior S"
     then have "z \<in> rel_interior S"
@@ -8402,7 +8574,7 @@
   proof (cases "I = {}")
     case True
     then show ?thesis
-      using Inter_empty rel_interior_univ2 by auto
+      using Inter_empty rel_interior_UNIV by auto
   next
     case False
     {
@@ -8463,7 +8635,7 @@
   have "affine hull T = T"
     using assms by auto
   then have "rel_interior T = T"
-    using rel_interior_univ[of T] by metis
+    using rel_interior_affine_hull[of T] by metis
   moreover have "closure T = T"
     using assms affine_closed[of T] by auto
   ultimately show ?thesis
@@ -8493,7 +8665,7 @@
   have "affine hull T = T"
     using assms by auto
   then have "rel_interior T = T"
-    using rel_interior_univ[of T] by metis
+    using rel_interior_affine_hull[of T] by metis
   moreover have "closure T = T"
     using assms affine_closed[of T] by auto
   ultimately show ?thesis
@@ -8649,7 +8821,7 @@
   ultimately show ?thesis by auto
 qed
 
-lemma rel_interior_direct_sum:
+lemma rel_interior_Times:
   fixes S :: "'n::euclidean_space set"
     and T :: "'m::euclidean_space set"
   assumes "convex S"
@@ -8864,6 +9036,14 @@
   then show ?thesis using h2 by blast
 qed
 
+lemma rel_frontier_Times:
+  fixes S :: "'n::euclidean_space set"
+    and T :: "'m::euclidean_space set"
+  assumes "convex S"
+    and "convex T"
+  shows "rel_frontier S \<times> rel_frontier T \<subseteq> rel_frontier (S \<times> T)"
+    by (force simp: rel_frontier_def rel_interior_Times assms closure_Times)
+
 
 subsubsection \<open>Relative interior of convex cone\<close>
 
@@ -9155,7 +9335,7 @@
   have "rel_interior S + rel_interior T = (\<lambda>(x,y). x + y) ` (rel_interior S \<times> rel_interior T)"
     by (simp add: set_plus_image)
   also have "\<dots> = (\<lambda>(x,y). x + y) ` rel_interior (S \<times> T)"
-    using rel_interior_direct_sum assms by auto
+    using rel_interior_Times assms by auto
   also have "\<dots> = rel_interior (S + T)"
     using fst_snd_linear convex_Times assms
       rel_interior_convex_linear_image[of "(\<lambda>(x,y). x + y)" "S \<times> T"]
@@ -9179,7 +9359,7 @@
     and "convex T"
     and "rel_open T"
   shows "convex (S \<times> T) \<and> rel_open (S \<times> T)"
-  by (metis assms convex_Times rel_interior_direct_sum rel_open_def)
+  by (metis assms convex_Times rel_interior_Times rel_open_def)
 
 lemma convex_rel_open_sum:
   fixes S T :: "'n::euclidean_space set"
diff -r 89d19aa73081 -r aa894a49f77d src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Apr 17 22:38:50 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Apr 18 14:30:32 2016 +0100
@@ -107,6 +107,9 @@
 lemma DIM_positive: "0 < DIM('a::euclidean_space)"
   by (simp add: card_gt_0_iff)
 
+lemma DIM_ge_Suc0 [iff]: "Suc 0 \<le> card Basis"
+  by (meson DIM_positive Suc_leI)
+
 subsection \<open>Subclass relationships\<close>
 
 instance euclidean_space \<subseteq> perfect_space
diff -r 89d19aa73081 -r aa894a49f77d src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Sun Apr 17 22:38:50 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Apr 18 14:30:32 2016 +0100
@@ -6805,44 +6805,6 @@
 
 subsection \<open>Special case of stretching coordinate axes separately.\<close>
 
-lemma image_stretch_interval:
-  "(\<lambda>x. \<Sum>k\<in>Basis. (m k * (x\<bullet>k)) *\<^sub>R k) ` cbox a (b::'a::euclidean_space) =
-  (if (cbox a b) = {} then {} else
-    cbox (\<Sum>k\<in>Basis. (min (m k * (a\<bullet>k)) (m k * (b\<bullet>k))) *\<^sub>R k::'a)
-     (\<Sum>k\<in>Basis. (max (m k * (a\<bullet>k)) (m k * (b\<bullet>k))) *\<^sub>R k))"
-proof cases
-  assume *: "cbox a b \<noteq> {}"
-  show ?thesis
-    unfolding box_ne_empty if_not_P[OF *]
-    apply (simp add: cbox_def image_Collect set_eq_iff euclidean_eq_iff[where 'a='a] ball_conj_distrib[symmetric])
-    apply (subst choice_Basis_iff[symmetric])
-  proof (intro allI ball_cong refl)
-    fix x i :: 'a assume "i \<in> Basis"
-    with * have a_le_b: "a \<bullet> i \<le> b \<bullet> i"
-      unfolding box_ne_empty by auto
-    show "(\<exists>xa. x \<bullet> i = m i * xa \<and> a \<bullet> i \<le> xa \<and> xa \<le> b \<bullet> i) \<longleftrightarrow>
-        min (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) \<le> x \<bullet> i \<and> x \<bullet> i \<le> max (m i * (a \<bullet> i)) (m i * (b \<bullet> i))"
-    proof (cases "m i = 0")
-      case True
-      with a_le_b show ?thesis by auto
-    next
-      case False
-      then have *: "\<And>a b. a = m i * b \<longleftrightarrow> b = a / m i"
-        by (auto simp add: 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)
-    qed
-  qed
-qed simp
-
-lemma interval_image_stretch_interval:
-  "\<exists>u v. (\<lambda>x. \<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k) ` cbox a (b::'a::euclidean_space) = cbox u (v::'a::euclidean_space)"
-  unfolding image_stretch_interval by auto
-
 lemma content_image_stretch_interval:
   "content ((\<lambda>x::'a::euclidean_space. (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)::'a) ` cbox a b) =
     \<bar>setprod m Basis\<bar> * content (cbox a b)"
diff -r 89d19aa73081 -r aa894a49f77d src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sun Apr 17 22:38:50 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon Apr 18 14:30:32 2016 +0100
@@ -216,6 +216,9 @@
 lemma linear_compose_cmul: "linear f \<Longrightarrow> linear (\<lambda>x. c *\<^sub>R f x)"
   by (simp add: linear_iff algebra_simps)
 
+lemma linear_compose_scaleR: "linear f \<Longrightarrow> linear (\<lambda>x. f x *\<^sub>R c)"
+  by (simp add: linear_iff scaleR_add_left)
+
 lemma linear_compose_neg: "linear f \<Longrightarrow> linear (\<lambda>x. - f x)"
   by (simp add: linear_iff)
 
@@ -526,7 +529,7 @@
 lemma hull_eq: "(\<And>T. Ball T S \<Longrightarrow> S (\<Inter>T)) \<Longrightarrow> (S hull s) = s \<longleftrightarrow> S s"
   using hull_same[of S s] hull_in[of S s] by metis
 
-lemma hull_hull: "S hull (S hull s) = S hull s"
+lemma hull_hull [simp]: "S hull (S hull s) = S hull s"
   unfolding hull_def by blast
 
 lemma hull_subset[intro]: "s \<subseteq> (S hull s)"
@@ -544,7 +547,7 @@
 lemma subset_hull: "S t \<Longrightarrow> S hull s \<subseteq> t \<longleftrightarrow> s \<subseteq> t"
   unfolding hull_def by blast
 
-lemma hull_UNIV: "S hull UNIV = UNIV"
+lemma hull_UNIV [simp]: "S hull UNIV = UNIV"
   unfolding hull_def by auto
 
 lemma hull_unique: "s \<subseteq> t \<Longrightarrow> S t \<Longrightarrow> (\<And>t'. s \<subseteq> t' \<Longrightarrow> S t' \<Longrightarrow> t \<subseteq> t') \<Longrightarrow> (S hull s = t)"
diff -r 89d19aa73081 -r aa894a49f77d src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Apr 17 22:38:50 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 18 14:30:32 2016 +0100
@@ -1403,6 +1403,12 @@
   finally show ?thesis .
 qed
 
+lemma cbox01_nonempty [simp]: "cbox 0 One \<noteq> {}"
+  by (simp add: box_ne_empty inner_Basis inner_setsum_left setsum_nonneg)
+
+lemma box01_nonempty [simp]: "box 0 One \<noteq> {}"
+  by (simp add: box_ne_empty inner_Basis inner_setsum_left) (simp add: setsum.remove)
+  
 
 subsection\<open>Connectedness\<close>
 
@@ -8422,6 +8428,11 @@
   shows "subspace s \<Longrightarrow> complete s"
   using complete_eq_closed closed_subspace by auto
 
+lemma closed_span [iff]:
+  fixes s :: "'a::euclidean_space set"
+  shows "closed (span s)"
+by (simp add: closed_subspace subspace_span)
+
 lemma dim_closure:
   fixes s :: "('a::euclidean_space) set"
   shows "dim(closure s) = dim s" (is "?dc = ?d")
diff -r 89d19aa73081 -r aa894a49f77d src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Sun Apr 17 22:38:50 2016 +0200
+++ b/src/HOL/Product_Type.thy	Mon Apr 18 14:30:32 2016 +0100
@@ -1233,6 +1233,9 @@
     using * eq[symmetric] by auto
 qed simp_all
 
+lemma subset_fst_snd: "A \<subseteq> (fst ` A \<times> snd ` A)"
+  by force
+
 lemma inj_on_apfst [simp]: "inj_on (apfst f) (A \<times> UNIV) \<longleftrightarrow> inj_on f A"
 by(auto simp add: inj_on_def)
 
diff -r 89d19aa73081 -r aa894a49f77d src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sun Apr 17 22:38:50 2016 +0200
+++ b/src/HOL/Set.thy	Mon Apr 18 14:30:32 2016 +0100
@@ -1001,6 +1001,9 @@
   shows "\<exists>x\<in>A. P (f x)"
   using assms by auto
 
+lemma image_add_0 [simp]: "op+ (0::'a::comm_monoid_add) ` S = S"
+  by auto
+
 
 text \<open>
   \medskip Range of a function -- just a translation for image!
diff -r 89d19aa73081 -r aa894a49f77d src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Sun Apr 17 22:38:50 2016 +0200
+++ b/src/HOL/Topological_Spaces.thy	Mon Apr 18 14:30:32 2016 +0100
@@ -1825,8 +1825,10 @@
 qed
 
 lemma compact_imp_fip:
-  "compact s \<Longrightarrow> \<forall>t \<in> f. closed t \<Longrightarrow> \<forall>f'. finite f' \<and> f' \<subseteq> f \<longrightarrow> (s \<inter> (\<Inter>f') \<noteq> {}) \<Longrightarrow>
-    s \<inter> (\<Inter>f) \<noteq> {}"
+    "\<lbrakk>compact S;
+      \<And>T. T \<in> F \<Longrightarrow> closed T;
+      \<And>F'. \<lbrakk>finite F'; F' \<subseteq> F\<rbrakk> \<Longrightarrow> S \<inter> (\<Inter>F') \<noteq> {}\<rbrakk>
+     \<Longrightarrow> S \<inter> (\<Inter>F) \<noteq> {}"
   unfolding compact_fip by auto
 
 lemma compact_imp_fip_image:
@@ -1846,7 +1848,7 @@
       using finite_subset_image [of A f I] by blast
     with Q [of B] show "s \<inter> \<Inter>A \<noteq> {}" by simp
   qed
-  ultimately have "s \<inter> (\<Inter>(f ` I)) \<noteq> {}" by (rule compact_imp_fip)
+  ultimately have "s \<inter> (\<Inter>(f ` I)) \<noteq> {}" by (metis compact_imp_fip)
   then show ?thesis by simp
 qed