src/HOL/Analysis/Convex.thy

     apply (rule exI[of _ "int (card B) - (1 :: int)"])
     apply (rule exI[of _ "B"], auto)
     done
 qed
 
-lemma affine_hull_nonempty: "S \<noteq> {} \<longleftrightarrow> affine hull S \<noteq> {}"
-proof -
-  have "S = {} \<Longrightarrow> affine hull S = {}"
-    using affine_hull_empty by auto
-  moreover have "affine hull S = {} \<Longrightarrow> S = {}"
-    unfolding hull_def by auto
-  ultimately show ?thesis by blast
-qed
+lemma affine_hull_eq_empty [simp]: "affine hull S = {} \<longleftrightarrow> S = {}"
+by (metis affine_empty subset_empty subset_hull)
+
+lemma empty_eq_affine_hull[simp]: "{} = affine hull S \<longleftrightarrow> S = {}"
+by (metis affine_hull_eq_empty)
 
 lemma aff_dim_parallel_subspace_aux:
   fixes B :: "'n::euclidean_space set"
   assumes "\<not> affine_dependent B" "a \<in> B"
   shows "finite B \<and> ((card B) - 1 = dim (span ((\<lambda>x. -a+x) ` (B-{a}))))"

 proof -
   obtain B where
     B: "affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> int (card B) = aff_dim V + 1"
     using aff_dim_basis_exists by auto
   then have "B \<noteq> {}"
-    using assms B affine_hull_nonempty[of V] affine_hull_nonempty[of B]
+    using assms B
     by auto
   then obtain a where a: "a \<in> B" by auto
   define Lb where "Lb = span ((\<lambda>x. -a+x) ` (B-{a}))"
   moreover have "affine_parallel (affine hull B) Lb"
     using Lb_def B assms affine_hull_span2[of a B] a

     unfolding affine_parallel_def
     by auto
   moreover have "subspace Lb"
     using Lb_def subspace_span by auto
   moreover have "affine hull B \<noteq> {}"
-    using assms B affine_hull_nonempty[of V] by auto
+    using assms B by auto
   ultimately have "L = Lb"
     using assms affine_parallel_subspace[of "affine hull B"] affine_affine_hull[of B] B
     by auto
   then have "dim L = dim Lb"
     by auto

     and "\<not> affine_dependent B"
     and "int (card B) = aff_dim S + 1"
     using aff_dim_basis_exists by auto
   moreover
   from * have "S = {} \<longleftrightarrow> B = {}"
-    using affine_hull_nonempty[of B] affine_hull_nonempty[of S] by auto
+    by auto
   ultimately show ?thesis
     using aff_independent_finite[of B] card_gt_0_iff[of B] by auto
 qed
 
 lemma aff_dim_empty_eq [simp]: "aff_dim ({}::'a::euclidean_space set) = -1"

   assumes "affine hull B = affine hull V \<and> \<not> affine_dependent B"
   shows "of_nat (card B) = aff_dim V + 1"
 proof (cases "B = {}")
   case True
   then have "V = {}"
-    using affine_hull_nonempty[of V] affine_hull_nonempty[of B] assms
+    using assms
     by auto
   then have "aff_dim V = (-1::int)"
     using aff_dim_empty by auto
   then show ?thesis
     using \<open>B = {}\<close> by auto

 proof -
   {
     assume "T \<noteq> {}" "S \<noteq> {}"
     then obtain L where L: "subspace L \<and> affine_parallel (affine hull T) L"
       using affine_parallel_subspace[of "affine hull T"]
-        affine_affine_hull[of T] affine_hull_nonempty
+        affine_affine_hull[of T]
       by auto
     then have "aff_dim T = int (dim L)"
       using aff_dim_parallel_subspace \<open>T \<noteq> {}\<close> by auto
     moreover have *: "subspace L \<and> affine_parallel (affine hull S) L"
        using L affine_parallel_assoc[of "affine hull S" "affine hull T" L] assms by auto

   }
   moreover
   {
     assume "S = {}"
     then have "S = {}" and "T = {}"
-      using assms affine_hull_nonempty
+      using assms
       unfolding affine_parallel_def
       by auto
     then have ?thesis using aff_dim_empty by auto
   }
   moreover
   {
     assume "T = {}"
     then have "S = {}" and "T = {}"
-      using assms affine_hull_nonempty
+      using assms
       unfolding affine_parallel_def
       by auto
     then have ?thesis
       using aff_dim_empty by auto
   }