src/HOL/Analysis/Polytope.thy

     assumes "card S = Suc (DIM('a))"
       shows "frontier(convex hull S) = \<Union> {convex hull (S - {a}) | a. a \<in> S}"
 proof (cases "affine_dependent S")
   case True
     have [iff]: "finite S"
-      using assms using card_infinite by force
+      using assms using card.infinite by force
     then have ccs: "closed (convex hull S)"
       by (simp add: compact_imp_closed finite_imp_compact_convex_hull)
     { fix x T
       assume "finite T" "T \<subseteq> S" "int (card T) \<le> aff_dim S + 1" "x \<in> convex hull T"
       then have "S \<noteq> T"

 proof (cases "b = a \<or> c = a \<or> c = b")
   case True then show ?thesis
     by (auto simp: assms segment_convex_hull frontier_def empty_interior_convex_hull insert_commute card_insert_le_m1 hull_inc insert_absorb)
 next
   case False then have [simp]: "card {a, b, c} = Suc (DIM('a))"
-    by (simp add: card_insert Set.insert_Diff_if assms)
+    by (simp add: card.insert_remove Set.insert_Diff_if assms)
   show ?thesis
   proof
     show "?lhs \<subseteq> ?rhs"
       using False
       by (force simp: segment_convex_hull frontier_of_convex_hull insert_Diff_if insert_commute split: if_split_asm)

 
 lemma simplex_empty [simp]: "n simplex {} \<longleftrightarrow> n = -1"
 proof
   assume "n simplex {}"
   then show "n = -1"
-    unfolding simplex by (metis card_empty convex_hull_eq_empty diff_0 diff_eq_eq of_nat_0)
+    unfolding simplex by (metis card.empty convex_hull_eq_empty diff_0 diff_eq_eq of_nat_0)
 next
   assume "n = -1" then show "n simplex {}"
     by (fastforce simp: simplex)
 qed
 

    "n simplex S \<Longrightarrow> aff_dim S = n"
   by (metis simplex add.commute add_diff_cancel_left' aff_dim_convex_hull affine_independent_iff_card)
 
 lemma zero_simplex_sing: "0 simplex {a}"
   apply (simp add: simplex_def)
-  by (metis affine_independent_1 card_empty card_insert_disjoint convex_hull_singleton empty_iff finite.emptyI)
+  by (metis affine_independent_1 card.empty card_insert_disjoint convex_hull_singleton empty_iff finite.emptyI)
 
 lemma simplex_sing [simp]: "n simplex {a} \<longleftrightarrow> n = 0"
   using aff_dim_simplex aff_dim_sing zero_simplex_sing by blast
 
 lemma simplex_zero: "0 simplex S \<longleftrightarrow> (\<exists>a. S = {a})"