src/HOL/Analysis/Convex_Euclidean_Space.thy

     apply (rule continuous_on_compose)
     apply (simp add: split_def)
     apply (rule continuous_intros | simp add: assms)+
     done
 qed
-
-lemma dim_image_eq:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  assumes lf: "linear f"
-    and fi: "inj_on f (span S)"
-  shows "dim (f ` S) = dim (S::'n::euclidean_space set)"
-proof -
-  obtain B where B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S"
-    using basis_exists[of S] by auto
-  then have "span S = span B"
-    using span_mono[of B S] span_mono[of S "span B"] span_span[of B] by auto
-  then have "independent (f ` B)"
-    using independent_inj_on_image[of B f] B assms by auto
-  moreover have "card (f ` B) = card B"
-    using assms card_image[of f B] subset_inj_on[of f "span S" B] B span_inc by auto
-  moreover have "(f ` B) \<subseteq> (f ` S)"
-    using B by auto
-  ultimately have "dim (f ` S) \<ge> dim S"
-    using independent_card_le_dim[of "f ` B" "f ` S"] B by auto
-  then show ?thesis
-    using dim_image_le[of f S] assms by auto
-qed
-
-lemma linear_injective_on_subspace_0:
-  assumes lf: "linear f"
-    and "subspace S"
-  shows "inj_on f S \<longleftrightarrow> (\<forall>x \<in> S. f x = 0 \<longrightarrow> x = 0)"
-proof -
-  have "inj_on f S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y \<in> S. f x = f y \<longrightarrow> x = y)"
-    by (simp add: inj_on_def)
-  also have "\<dots> \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y \<in> S. f x - f y = 0 \<longrightarrow> x - y = 0)"
-    by simp
-  also have "\<dots> \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y \<in> S. f (x - y) = 0 \<longrightarrow> x - y = 0)"
-    by (simp add: linear_diff[OF lf])
-  also have "\<dots> \<longleftrightarrow> (\<forall>x \<in> S. f x = 0 \<longrightarrow> x = 0)"
-    using \<open>subspace S\<close> subspace_def[of S] subspace_diff[of S] by auto
-  finally show ?thesis .
-qed
-
-lemma subspace_Inter: "\<forall>s \<in> f. subspace s \<Longrightarrow> subspace (\<Inter>f)"
-  unfolding subspace_def by auto
-
-lemma span_eq[simp]: "span s = s \<longleftrightarrow> subspace s"
-  unfolding span_def by (rule hull_eq) (rule subspace_Inter)
 
 lemma substdbasis_expansion_unique:
   assumes d: "d \<subseteq> Basis"
   shows "(\<Sum>i\<in>d. f i *\<^sub>R i) = (x::'a::euclidean_space) \<longleftrightarrow>
     (\<forall>i\<in>Basis. (i \<in> d \<longrightarrow> f i = x \<bullet> i) \<and> (i \<notin> d \<longrightarrow> x \<bullet> i = 0))"

     moreover have *: "x = (norm x / e) *\<^sub>R y"
       using y_def assms by simp
     moreover from * have "x = (norm x/e) *\<^sub>R y"
       by auto
     ultimately have "x \<in> span (cball 0 e)"
-      using span_mul[of y "cball 0 e" "norm x/e"] span_inc[of "cball 0 e"]
-      by (simp add: span_superset)
+      using span_scale[of y "cball 0 e" "norm x/e"]
+        span_superset[of "cball 0 e"]
+      by (simp add: span_base)
   }
   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)
-qed
-
-lemma indep_card_eq_dim_span:
-  fixes B :: "'n::euclidean_space set"
-  assumes "independent B"
-  shows "finite B \<and> card B = dim (span B)"
-  using assms basis_card_eq_dim[of B "span B"] span_inc by auto
+    using dim_span[of "cball (0 :: 'n::euclidean_space) e"]
+    by auto
+qed
 
 lemma sum_not_0: "sum f A \<noteq> 0 \<Longrightarrow> \<exists>a \<in> A. f a \<noteq> 0"
   by (rule ccontr) auto
 
 lemma subset_translation_eq [simp]:

 lemma convex_linear_image_eq [simp]:
     fixes f :: "'a::real_vector \<Rightarrow> 'b::real_vector"
     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 basis_to_basis_subspace_isomorphism:
-  assumes s: "subspace (S:: ('n::euclidean_space) set)"
-    and t: "subspace (T :: ('m::euclidean_space) set)"
-    and d: "dim S = dim T"
-    and B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S"
-    and C: "C \<subseteq> T" "independent C" "T \<subseteq> span C" "card C = dim T"
-  shows "\<exists>f. linear f \<and> f ` B = C \<and> f ` S = T \<and> inj_on f S"
-proof -
-  from B independent_bound have fB: "finite B"
-    by blast
-  from C independent_bound have fC: "finite C"
-    by blast
-  from B(4) C(4) card_le_inj[of B C] d obtain f where
-    f: "f ` B \<subseteq> C" "inj_on f B" using \<open>finite B\<close> \<open>finite C\<close> by auto
-  from linear_independent_extend[OF B(2)] obtain g where
-    g: "linear g" "\<forall>x \<in> B. g x = f x" by blast
-  from inj_on_iff_eq_card[OF fB, of f] f(2)
-  have "card (f ` B) = card B" by simp
-  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)
-  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)
-  note g0 = linear_indep_image_lemma[OF g(1) fB, unfolded gBC, OF C(2) gi]
-  {
-    fix x y
-    assume x: "x \<in> S" and y: "y \<in> S" and gxy: "g x = g y"
-    from B(3) x y have x': "x \<in> span B" and y': "y \<in> span B"
-      by blast+
-    from gxy have th0: "g (x - y) = 0"
-      by (simp add: linear_diff[OF g(1)])
-    have th1: "x - y \<in> span B" using x' y'
-      by (metis span_diff)
-    have "x = y" using g0[OF th1 th0] by simp
-  }
-  then have giS: "inj_on g S" unfolding inj_on_def by blast
-  from span_subspace[OF B(1,3) s]
-  have "g ` S = span (g ` B)"
-    by (simp add: span_linear_image[OF g(1)])
-  also have "\<dots> = span C"
-    unfolding gBC ..
-  also have "\<dots> = T"
-    using span_subspace[OF C(1,3) t] .
-  finally have gS: "g ` S = T" .
-  from g(1) gS giS gBC show ?thesis
-    by blast
-qed
-
 lemma closure_bounded_linear_image_subset:
   assumes f: "bounded_linear f"
   shows "f ` closure S \<subseteq> closure (f ` S)"
   using linear_continuous_on [OF f] closed_closure closure_subset
   by (rule image_closure_subset)

 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)"
+  then show "\<exists>v. x = a + v \<and> (\<exists>S u. v = (\<Sum>v\<in>S. u v *\<^sub>R v) \<and> finite S \<and> S \<subseteq> {x - a |x. x \<in> s} )"
     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
+    by (simp_all add: as sum.reindex[unfolded inj_on_def] scaleR_right_diff_distrib
+        sum_subtractf scaleR_left.sum[symmetric] sum_diff1 scaleR_left_diff_distrib)
 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}}"

 
 lemma cone_Inter[intro]: "\<forall>s\<in>f. cone s \<Longrightarrow> cone (\<Inter>f)"
   unfolding cone_def by auto
 
 lemma subspace_imp_cone: "subspace S \<Longrightarrow> cone S"
-  by (simp add: cone_def subspace_mul)
+  by (simp add: cone_def subspace_scale)
 
 
 subsubsection \<open>Conic hull\<close>
 
 lemma cone_cone_hull: "cone (cone hull s)"

 
 lemma subspace_imp_convex: "subspace s \<Longrightarrow> convex s"
   using subspace_imp_affine affine_imp_convex by auto
 
 lemma affine_hull_subset_span: "(affine hull s) \<subseteq> (span s)"
-  by (metis hull_minimal span_inc subspace_imp_affine subspace_span)
+  by (metis hull_minimal span_superset subspace_imp_affine subspace_span)
 
 lemma convex_hull_subset_span: "(convex hull s) \<subseteq> (span s)"
-  by (metis hull_minimal span_inc subspace_imp_convex subspace_span)
+  by (metis hull_minimal span_superset subspace_imp_convex subspace_span)
 
 lemma convex_hull_subset_affine_hull: "(convex hull s) \<subseteq> (affine hull s)"
   by (metis affine_affine_hull affine_imp_convex hull_minimal hull_subset)
 
 lemma affine_dependent_imp_dependent: "affine_dependent s \<Longrightarrow> dependent s"

     done
   have "dim {x - a |x. x \<in> s - {a}} \<le> dim s"
     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 add:span_base span_diff)
     done
   also have "\<dots> < dim s + 1" by auto
   also have "\<dots> \<le> card (s - {a})"
     using assms
     using card_Diff_singleton[OF assms(1) \<open>a\<in>s\<close>]

       using aff_dim_parallel_subspace_aux assms by auto
   }
   then show ?thesis by auto
 qed
 
-lemma independent_finite:
-  fixes B :: "'n::euclidean_space set"
-  assumes "independent B"
-  shows "finite B"
-  using affine_dependent_imp_dependent[of B] aff_independent_finite[of B] assms
-  by auto
-
-lemma subspace_dim_equal:
-  assumes "subspace (S :: ('n::euclidean_space) set)"
-    and "subspace T"
-    and "S \<subseteq> T"
-    and "dim S \<ge> dim T"
-  shows "S = T"
-proof -
-  obtain B where B: "B \<le> S" "independent B \<and> S \<subseteq> span B" "card B = dim S"
-    using basis_exists[of S] by auto
-  then have "span B \<subseteq> S"
-    using span_mono[of B S] span_eq[of S] assms by metis
-  then have "span B = S"
-    using B by auto
-  have "dim S = dim T"
-    using assms dim_subset[of S T] by auto
-  then have "T \<subseteq> span B"
-    using card_eq_dim[of B T] B independent_finite assms by auto
-  then show ?thesis
-    using assms \<open>span B = S\<close> by auto
-qed
-
-corollary dim_eq_span:
-  fixes S :: "'a::euclidean_space set"
-  shows "\<lbrakk>S \<subseteq> T; dim T \<le> dim S\<rbrakk> \<Longrightarrow> span S = span T"
-by (simp add: span_mono subspace_dim_equal subspace_span)
-
-lemma dim_eq_full:
-    fixes S :: "'a :: euclidean_space set"
-    shows "dim S = DIM('a) \<longleftrightarrow> span S = UNIV"
-apply (rule iffI)
- apply (metis dim_eq_span dim_subset_UNIV span_Basis span_span subset_UNIV)
-by (metis dim_UNIV dim_span)
+lemmas independent_finite = independent_imp_finite
 
 lemma span_substd_basis:
   assumes d: "d \<subseteq> Basis"
   shows "span d = {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0}"
   (is "_ = ?B")

   have "d \<subseteq> ?B"
     using d by (auto simp: inner_Basis)
   moreover have s: "subspace ?B"
     using subspace_substandard[of "\<lambda>i. i \<notin> d"] .
   ultimately have "span d \<subseteq> ?B"
-    using span_mono[of d "?B"] span_eq[of "?B"] by blast
+    using span_mono[of d "?B"] span_eq_iff[of "?B"] by blast
   moreover have *: "card d \<le> dim (span d)"
-    using independent_card_le_dim[of d "span d"] independent_substdbasis[OF assms] span_inc[of d]
+    using independent_card_le_dim[of d "span d"] independent_substdbasis[OF assms]
+      span_superset[of d]
     by auto
   moreover from * have "dim ?B \<le> dim (span d)"
     using dim_substandard[OF assms] by auto
   ultimately show ?thesis
     using s subspace_dim_equal[of "span d" "?B"] subspace_span[of d] by auto

   assumes "independent B"
   shows "\<exists>f d::'a set. card d = card B \<and> linear f \<and> f ` B = d \<and>
     f ` span B = {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0} \<and> inj_on f (span B) \<and> d \<subseteq> Basis"
 proof -
   have B: "card B = dim B"
-    using dim_unique[of B B "card B"] assms span_inc[of B] by auto
+    using dim_unique[of B B "card B"] assms span_superset[of B] by auto
   have "dim B \<le> card (Basis :: 'a set)"
     using dim_subset_UNIV[of B] by simp
   from ex_card[OF this] obtain d :: "'a set" where d: "d \<subseteq> Basis" and t: "card d = dim B"
     by auto
   let ?t = "{x::'a::euclidean_space. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0}"
   have "\<exists>f. linear f \<and> f ` B = d \<and> f ` span B = ?t \<and> inj_on f (span B)"
     apply (rule basis_to_basis_subspace_isomorphism[of "span B" ?t B "d"])
     apply (rule subspace_span)
     apply (rule subspace_substandard)
     defer
-    apply (rule span_inc)
+    apply (rule span_superset)
     apply (rule assms)
     defer
     unfolding dim_span[of B]
     apply(rule B)
     unfolding span_substd_basis[OF d, symmetric]
-    apply (rule span_inc)
+    apply (rule span_superset)
     apply (rule independent_substdbasis[OF d])
     apply rule
     apply assumption
     unfolding t[symmetric] span_substd_basis[OF d] dim_substandard[OF d]
     apply auto

     using lowdim_subset_hyperplane by blast
   moreover
   have "a \<bullet> w = a \<bullet> c" if "span ((+) (- c) ` S) \<subseteq> {x. a \<bullet> x = 0}" "w \<in> S" for w
   proof -
     have "w-c \<in> span ((+) (- c) ` S)"
-      by (simp add: span_superset \<open>w \<in> S\<close>)
+      by (simp add: span_base \<open>w \<in> S\<close>)
     with that have "w-c \<in> {x. a \<bullet> x = 0}"
       by blast
     then show ?thesis
       by (auto simp: algebra_simps)
   qed

     shows "card S = dim {x - a|x. x \<in> S} + 1"
 proof -
   have 1: "{b - a|b. b \<in> (S - {a})} \<subseteq> {x - a|x. x \<in> S}" by auto
   have 2: "x - a \<in> span {b - a |b. b \<in> S - {a}}" if "x \<in> S" for x
   proof (cases "x = a")
-    case True then show ?thesis by simp
+    case True then show ?thesis by (simp add: span_clauses)
   next
     case False then show ?thesis
-      using assms by (blast intro: span_superset that)
+      using assms by (blast intro: span_base that)
   qed
   have "\<not> affine_dependent (insert a S)"
     by (simp add: assms insert_absorb)
   then have 3: "independent {b - a |b. b \<in> S - {a}}"
       using dependent_imp_affine_dependent by fastforce

       then have "f y \<in> f ` S"
         using y e2 h1 by auto
       then have "y \<in> S"
         using assms y hull_subset[of S] affine_hull_subset_span
           inj_on_image_mem_iff [OF \<open>inj_on f (span S)\<close>]
-        by (metis Int_iff span_inc subsetCE)
+        by (metis Int_iff span_superset subsetCE)
     }
     then have "z \<in> f ` (rel_interior S)"
       using mem_rel_interior_cball[of x S] \<open>e > 0\<close> x by auto
   }
   moreover

         using cball_def[of "f x" e] dist_norm[of "f x" y] e_def by auto
       moreover have "f x - f xy = f (x - xy)"
         using assms linear_diff[of f x xy] linear_conv_bounded_linear[of f] by auto
       moreover have *: "x - xy \<in> span S"
         using subspace_diff[of "span S" x xy] subspace_span \<open>x \<in> S\<close> xy
-          affine_hull_subset_span[of S] span_inc
+          affine_hull_subset_span[of S] span_superset
         by auto
       moreover from * have "e1 * norm (x - xy) \<le> norm (f (x - xy))"
         using e1 by auto
       ultimately have "e1 * norm (x - xy) \<le> e1 * e2"
         by auto

     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
+    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 add: inner_diff)
   then have bdd: "bdd_above (((\<bullet>) a)`s)"
     using \<open>t \<noteq> {}\<close> by (auto intro: bdd_aboveI2[OF *])
   show ?thesis

   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)"
-  using linear_scaleR by (rule convex_hull_linear_image [symmetric])
+  by (simp add: convex_hull_linear_image)
 
 lemma convex_hull_affinity:
   "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)
 

   fixes s :: "'a :: euclidean_space set"
   assumes "DIM('a) = 1"
   shows "connected s \<longleftrightarrow> convex s"
 proof -
   obtain f:: "'a \<Rightarrow> real" where linf: "linear f" and "inj f"
-    using subspace_isomorphism [where 'a = 'a and 'b = real]
-    by (metis DIM_real dim_UNIV subspace_UNIV assms)
+    using subspace_isomorphism[OF subspace_UNIV subspace_UNIV,
+        where 'a='a and 'b=real]
+    unfolding Euclidean_Space.dim_UNIV
+    by (auto simp: assms)
   then have "f -` (f ` s) = s"
     by (simp add: inj_vimage_image_eq)
   then show ?thesis
     by (metis connected_convex_1 convex_linear_vimage linf convex_connected connected_linear_image)
 qed
 
 lemma is_interval_cball_1[intro, simp]: "is_interval (cball a b)" for a b::real
-  by (auto simp: is_interval_convex_1 convex_cball)
+  by (simp add: is_interval_convex_1)
 
 
 subsection%unimportant \<open>Another intermediate value theorem formulation\<close>
 
 lemma ivt_increasing_component_on_1:

   also have "\<dots> = (\<Sum>i\<in>Basis. (\<lambda>x. x *\<^sub>R i) ` cbox 0 1)"
     by (simp only: box_eq_set_sum_Basis)
   also have "\<dots> = (\<Sum>i\<in>Basis. (\<lambda>x. x *\<^sub>R i) ` (convex hull {0, 1}))"
     by (simp only: convex_hull_eq_real_cbox zero_le_one)
   also have "\<dots> = (\<Sum>i\<in>Basis. convex hull ((\<lambda>x. x *\<^sub>R i) ` {0, 1}))"
-    by (simp only: convex_hull_linear_image linear_scaleR_left)
+    by (simp add: convex_hull_linear_image)
   also have "\<dots> = convex hull (\<Sum>i\<in>Basis. (\<lambda>x. x *\<^sub>R i) ` {0, 1})"
     by (simp only: convex_hull_set_sum)
   also have "\<dots> = convex hull {x. \<forall>i\<in>Basis. x\<bullet>i \<in> {0, 1}}"
     by (simp only: box_eq_set_sum_Basis)
   also have "convex hull {x. \<forall>i\<in>Basis. x\<bullet>i \<in> {0, 1}} = convex hull ?points"