diff -r fc252acb7100 -r 880ab0f27ddf src/HOL/Analysis/Convex.thy
--- a/src/HOL/Analysis/Convex.thy	Wed Jan 16 16:50:35 2019 -0500
+++ b/src/HOL/Analysis/Convex.thy	Wed Jan 16 18:14:02 2019 -0500
@@ -14,79 +14,6 @@
   "HOL-Library.Set_Algebras"
 begin
 
-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))"
-proof -
-  have *: "\<And>x a b P. x * (if P then a else b) = (if P then x * a else x * b)"
-    by auto
-  have **: "finite d"
-    by (auto intro: finite_subset[OF assms])
-  have ***: "\<And>i. i \<in> Basis \<Longrightarrow> (\<Sum>i\<in>d. f i *\<^sub>R i) \<bullet> i = (\<Sum>x\<in>d. if x = i then f x else 0)"
-    using d
-    by (auto intro!: sum.cong simp: inner_Basis inner_sum_left)
-  show ?thesis
-    unfolding euclidean_eq_iff[where 'a='a] by (auto simp: sum.delta[OF **] ***)
-qed
-
-lemma independent_substdbasis: "d \<subseteq> Basis \<Longrightarrow> independent d"
-  by (rule independent_mono[OF independent_Basis])
-
-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]:
-    fixes a :: "'a::real_vector" shows "(+) a ` s \<subseteq> (+) a ` t \<longleftrightarrow> s \<subseteq> t"
-  by auto
-
-lemma translate_inj_on:
-  fixes A :: "'a::ab_group_add set"
-  shows "inj_on (\<lambda>x. a + x) A"
-  unfolding inj_on_def by auto
-
-lemma translation_assoc:
-  fixes a b :: "'a::ab_group_add"
-  shows "(\<lambda>x. b + x) ` ((\<lambda>x. a + x) ` S) = (\<lambda>x. (a + b) + x) ` S"
-  by auto
-
-lemma translation_invert:
-  fixes a :: "'a::ab_group_add"
-  assumes "(\<lambda>x. a + x) ` A = (\<lambda>x. a + x) ` B"
-  shows "A = B"
-proof -
-  have "(\<lambda>x. -a + x) ` ((\<lambda>x. a + x) ` A) = (\<lambda>x. - a + x) ` ((\<lambda>x. a + x) ` B)"
-    using assms by auto
-  then show ?thesis
-    using translation_assoc[of "-a" a A] translation_assoc[of "-a" a B] by auto
-qed
-
-lemma translation_galois:
-  fixes a :: "'a::ab_group_add"
-  shows "T = ((\<lambda>x. a + x) ` S) \<longleftrightarrow> S = ((\<lambda>x. (- a) + x) ` T)"
-  using translation_assoc[of "-a" a S]
-  apply auto
-  using translation_assoc[of a "-a" T]
-  apply auto
-  done
-
-lemma translation_inverse_subset:
-  assumes "((\<lambda>x. - a + x) ` V) \<le> (S :: 'n::ab_group_add set)"
-  shows "V \<le> ((\<lambda>x. a + x) ` S)"
-proof -
-  {
-    fix x
-    assume "x \<in> V"
-    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"], simp)
-      done
-    then have "x \<in> ((\<lambda>x. a+x) ` S)" by auto
-  }
-  then show ?thesis by auto
-qed
-
 subsection \<open>Convexity\<close>
 
 definition%important convex :: "'a::real_vector set \<Rightarrow> bool"