# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1601039508 -3600
# Node ID d7d90ed4c74ef4d2357d0550adf12bf7013e2381
# Parent  c5d1a01d2d6c179116a8b6b2d4ec6ec4f7b6b3a3
fixed some remarkably ugly proofs

diff -r c5d1a01d2d6c -r d7d90ed4c74e src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Fri Sep 25 14:11:48 2020 +0100
@@ -326,7 +326,7 @@
   shows "odd (card {s\<in>simplices. (rl ` s = {..Suc n})})"
 proof (rule kuhn_counting_lemma)
   have finite_s[simp]: "\<And>s. s \<in> simplices \<Longrightarrow> finite s"
-    by (metis add_is_0 zero_neq_numeral card_infinite assms(3))
+    by (metis add_is_0 zero_neq_numeral card.infinite assms(3))
 
   let ?F = "{f. \<exists>s\<in>simplices. face f s}"
   have F_eq: "?F = (\<Union>s\<in>simplices. \<Union>a\<in>s. {s - {a}})"
diff -r c5d1a01d2d6c -r d7d90ed4c74e src/HOL/Analysis/Polytope.thy
--- a/src/HOL/Analysis/Polytope.thy	Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Analysis/Polytope.thy	Fri Sep 25 14:11:48 2020 +0100
@@ -2783,7 +2783,7 @@
 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
@@ -2839,7 +2839,7 @@
     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"
@@ -3125,7 +3125,7 @@
 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)
@@ -3141,7 +3141,7 @@
 
 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
diff -r c5d1a01d2d6c -r d7d90ed4c74e src/HOL/Analysis/Simplex_Content.thy
--- a/src/HOL/Analysis/Simplex_Content.thy	Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Analysis/Simplex_Content.thy	Fri Sep 25 14:11:48 2020 +0100
@@ -89,7 +89,7 @@
   also have "t ^ n / n / fact (card A) = t ^ n / fact n"
     by (simp add: n_def)
   also have "n = card (insert b A)"
-    using insert.hyps by (subst card_insert) (auto simp: n_def)
+    using insert.hyps by (subst card.insert_remove) (auto simp: n_def)
   finally show ?case .
 qed
 
diff -r c5d1a01d2d6c -r d7d90ed4c74e src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Fri Sep 25 14:11:48 2020 +0100
@@ -3270,7 +3270,7 @@
     fix a b
     assume "b \<in> S" "b \<in> affine hull (S - {b})"
     then have "interior(affine hull S) = {}" using assms
-      by (metis DIM_positive One_nat_def Suc_mono card.remove card_infinite empty_interior_affine_hull eq_iff hull_redundant insert_Diff not_less zero_le_one)
+      by (metis DIM_positive One_nat_def Suc_mono card.remove card.infinite empty_interior_affine_hull eq_iff hull_redundant insert_Diff not_less zero_le_one)
     then show "interior (convex hull S) = {}" 
       using affine_hull_nonempty_interior by fastforce
   qed
diff -r c5d1a01d2d6c -r d7d90ed4c74e src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Binomial.thy	Fri Sep 25 14:11:48 2020 +0100
@@ -81,11 +81,11 @@
     proof -
       from \<open>n \<in> K\<close> obtain L where "K = insert n L" and "n \<notin> L"
         by (blast elim: Set.set_insert)
-      with that show ?thesis by (simp add: card_insert)
+      with that show ?thesis by (simp add: card.insert_remove)
     qed
     show "K \<in> ?A \<longleftrightarrow> K \<in> ?B"
       by (subst in_image_insert_iff)
-        (auto simp add: card_insert subset_eq_atLeast0_lessThan_finite
+        (auto simp add: card.insert_remove subset_eq_atLeast0_lessThan_finite
           Diff_subset_conv K_finite Suc_card_K)
   qed
   also have "{K\<in>?Q. n \<notin> K} = ?P n (Suc k)"
diff -r c5d1a01d2d6c -r d7d90ed4c74e src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Sep 25 14:11:48 2020 +0100
@@ -1387,12 +1387,6 @@
   defines card = "folding.F (\<lambda>_. Suc) 0"
   by standard rule
 
-lemma card_infinite: "\<not> finite A \<Longrightarrow> card A = 0"
-  by (fact card.infinite)
-
-lemma card_empty: "card {} = 0"
-  by (fact card.empty)
-
 lemma card_insert_disjoint: "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> card (insert x A) = Suc (card A)"
   by (fact card.insert)
 
@@ -1417,17 +1411,20 @@
 lemma card_gt_0_iff: "0 < card A \<longleftrightarrow> A \<noteq> {} \<and> finite A"
   by (simp add: neq0_conv [symmetric] card_eq_0_iff)
 
-lemma card_Suc_Diff1: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> Suc (card (A - {x})) = card A"
-  apply (rule insert_Diff [THEN subst, where t = A])
-   apply assumption
-  apply (simp del: insert_Diff_single)
-  done
+lemma card_Suc_Diff1:
+  assumes "finite A" "x \<in> A" shows "Suc (card (A - {x})) = card A"
+proof -
+  have "Suc (card (A - {x})) = card (insert x (A - {x}))"
+    using assms by (simp add: card.insert_remove)
+  also have "... = card A"
+    using assms by (simp add: card_insert_if)
+  finally show ?thesis .
+qed
 
-lemma card_insert_le_m1: "n > 0 \<Longrightarrow> card y \<le> n - 1 \<Longrightarrow> card (insert x y) \<le> n"
-  apply (cases "finite y")
-   apply (cases "x \<in> y")
-    apply (auto simp: insert_absorb)
-  done
+lemma card_insert_le_m1:
+  assumes "n > 0" "card y \<le> n - 1" shows  "card (insert x y) \<le> n"
+  using assms
+  by (cases "finite y") (auto simp: card_insert_if)
 
 lemma card_Diff_singleton: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> card (A - {x}) = card A - 1"
   by (simp add: card_Suc_Diff1 [symmetric])
@@ -1446,9 +1443,6 @@
     using assms by (simp add: card_Diff_singleton)
 qed
 
-lemma card_insert: "finite A \<Longrightarrow> card (insert x A) = Suc (card (A - {x}))"
-  by (fact card.insert_remove)
-
 lemma card_insert_le: "finite A \<Longrightarrow> card A \<le> card (insert x A)"
   by (simp add: card_insert_if)
 
@@ -1482,21 +1476,24 @@
   qed
 qed
 
-lemma card_seteq: "finite B \<Longrightarrow> (\<And>A. A \<subseteq> B \<Longrightarrow> card B \<le> card A \<Longrightarrow> A = B)"
-  apply (induct rule: finite_induct)
-   apply simp
-  apply clarify
-  apply (subgoal_tac "finite A \<and> A - {x} \<subseteq> F")
-   prefer 2 apply (blast intro: finite_subset, atomize)
-  apply (drule_tac x = "A - {x}" in spec)
-  apply (simp add: card_Diff_singleton_if split: if_split_asm)
-  apply (case_tac "card A", auto)
-  done
+lemma card_seteq: 
+  assumes "finite B" and A: "A \<subseteq> B" "card B \<le> card A"
+  shows "A = B"
+  using assms
+proof (induction arbitrary: A rule: finite_induct)
+  case (insert b B)
+  then have A: "finite A" "A - {b} \<subseteq> B" 
+    by force+
+  then have "card B \<le> card (A - {b})"
+    using insert by (auto simp add: card_Diff_singleton_if)
+  then have "A - {b} = B"
+    using A insert.IH by auto
+  then show ?case 
+    using insert.hyps insert.prems by auto
+qed auto
 
 lemma psubset_card_mono: "finite B \<Longrightarrow> A < B \<Longrightarrow> card A < card B"
-  apply (simp add: psubset_eq linorder_not_le [symmetric])
-  apply (blast dest: card_seteq)
-  done
+  using card_seteq [of B A] by (auto simp add: psubset_eq)
 
 lemma card_Un_Int:
   assumes "finite A" "finite B"
@@ -1579,15 +1576,29 @@
   finally show ?thesis .
 qed
 
+lemma card_Diff1_less_iff: "card (A - {x}) < card A \<longleftrightarrow> finite A \<and> x \<in> A"
+proof (cases "finite A \<and> x \<in> A")
+  case True
+  then show ?thesis
+    by (auto simp: card_gt_0_iff intro: diff_less)
+qed auto
+
 lemma card_Diff1_less: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> card (A - {x}) < card A"
-  by (rule Suc_less_SucD) (simp add: card_Suc_Diff1 del: card_Diff_insert)
+  unfolding card_Diff1_less_iff by auto
 
-lemma card_Diff2_less: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> card (A - {x} - {y}) < card A"
-  apply (cases "x = y")
-   apply (simp add: card_Diff1_less del:card_Diff_insert)
-  apply (rule less_trans)
-   prefer 2 apply (auto intro!: card_Diff1_less simp del: card_Diff_insert)
-  done
+lemma card_Diff2_less:
+  assumes "finite A" "x \<in> A" "y \<in> A" shows "card (A - {x} - {y}) < card A"
+proof (cases "x = y")
+  case True
+  with assms show ?thesis
+    by (simp add: card_Diff1_less del: card_Diff_insert)
+next
+  case False
+  then have "card (A - {x} - {y}) < card (A - {x})" "card (A - {x}) < card A"
+    using assms by (intro card_Diff1_less; simp)+
+  then show ?thesis
+    by (blast intro: less_trans)
+qed
 
 lemma card_Diff1_le: "finite A \<Longrightarrow> card (A - {x}) \<le> card A"
   by (cases "x \<in> A") (simp_all add: card_Diff1_less less_imp_le)
@@ -1618,10 +1629,8 @@
     obtain f where "f ` s \<subseteq> t" "inj_on f s"
       by blast
     with "2.prems"(2) "2.hyps"(2) show ?case
-      apply -
-      apply (rule exI[where x = "\<lambda>z. if z = x then y else f z"])
-      apply (auto simp add: inj_on_def)
-      done
+      unfolding inj_on_def
+      by (rule_tac x = "\<lambda>z. if z = x then y else f z" in exI) auto
   qed
 qed
 
@@ -1800,10 +1809,7 @@
 lemma card_Suc_eq:
   "card A = Suc k \<longleftrightarrow>
     (\<exists>b B. A = insert b B \<and> b \<notin> B \<and> card B = k \<and> (k = 0 \<longrightarrow> B = {}))"
-  apply (auto elim!: card_eq_SucD)
-  apply (subst card.insert)
-    apply (auto simp add: intro:ccontr)
-  done
+  by (auto simp: card_insert_if card_gt_0_iff elim!: card_eq_SucD)
 
 lemma card_1_singletonE:
   assumes "card A = 1"
@@ -1836,10 +1842,11 @@
 
 lemma card_le_Suc_iff:
   "Suc n \<le> card A = (\<exists>a B. A = insert a B \<and> a \<notin> B \<and> n \<le> card B \<and> finite B)"
-apply(cases "finite A")
- apply (fastforce simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff
-    dest: subset_singletonD split: nat.splits if_splits)
-by auto
+proof (cases "finite A")
+  case True
+  then show ?thesis
+    by (fastforce simp: card_Suc_eq less_eq_nat.simps split: nat.splits)
+qed auto
 
 lemma finite_fun_UNIVD2:
   assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
@@ -1886,7 +1893,7 @@
   case False
   obtain n::nat where n: "n > max C 0" by auto
   obtain G where G: "G \<subseteq> F" "card G = n" using infinite_arbitrarily_large[OF False] by auto
-  hence "finite G" using \<open>n > max C 0\<close> using card_infinite gr_implies_not0 by blast
+  hence "finite G" using \<open>n > max C 0\<close> using card.infinite gr_implies_not0 by blast
   hence False using assms G n not_less by auto
   thus ?thesis ..
 next
@@ -2042,12 +2049,11 @@
     case empty
     show ?case by simp
   next
-    case insert
-    then show ?case
-      apply simp
-      apply (subst card_Un_disjoint)
-         apply (auto simp add: disjoint_eq_subset_Compl)
-      done
+    case (insert c C)
+    then have "c \<inter> \<Union>C = {}"
+      by auto
+    with insert show ?case
+      by (simp add: card_Un_disjoint)
   qed
 qed
 
@@ -2209,10 +2215,10 @@
     then have "X (A - {x})"
       using psubset.hyps by blast
     show False
-      apply (rule psubset.IH [where B = "A - {x}"])
-       apply (use \<open>x \<in> A\<close> in blast)
-      apply (simp add: \<open>X (A - {x})\<close>)
-      done
+    proof (rule psubset.IH [where B = "A - {x}"])
+      show "A - {x} \<subset> A"
+        using \<open>x \<in> A\<close> by blast
+    qed fact
   qed
 qed
 
diff -r c5d1a01d2d6c -r d7d90ed4c74e src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Library/FSet.thy	Fri Sep 25 14:11:48 2020 +0100
@@ -600,7 +600,7 @@
 
 lemma fcard_fempty:
   "fcard {||} = 0"
-  by transfer (rule card_empty)
+  by transfer (rule card.empty)
 
 lemma fcard_finsert_disjoint:
   "x |\<notin>| A \<Longrightarrow> fcard (finsert x A) = Suc (fcard A)"
@@ -632,7 +632,7 @@
 using assms by transfer (rule card_Diff_insert)
 
 lemma fcard_finsert: "fcard (finsert x A) = Suc (fcard (A |-| {|x|}))"
-by transfer (rule card_insert)
+by transfer (rule card.insert_remove)
 
 lemma fcard_finsert_le: "fcard A \<le> fcard (finsert x A)"
 by transfer (rule card_insert_le)
diff -r c5d1a01d2d6c -r d7d90ed4c74e src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Fri Sep 25 14:11:48 2020 +0100
@@ -417,7 +417,7 @@
 proof (induction n arbitrary: S)
   case 0
   then show ?case
-    by (metis all_not_in_conv card_empty enumerate.simps(1) not_less0 wellorder_Least_lemma(1))
+    by (metis all_not_in_conv card.empty enumerate.simps(1) not_less0 wellorder_Least_lemma(1))
 next
   case (Suc n)
   show ?case
diff -r c5d1a01d2d6c -r d7d90ed4c74e src/HOL/Library/Perm.thy
--- a/src/HOL/Library/Perm.thy	Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Library/Perm.thy	Fri Sep 25 14:11:48 2020 +0100
@@ -365,7 +365,7 @@
   then obtain B b where "affected f = insert b B"
     by blast
   with finite_affected [of f] have "card (affected f) \<ge> 1"
-    by (simp add: card_insert)
+    by (simp add: card.insert_remove)
   case False then have "order f a = 1"
     by (simp add: order_eq_one_iff)
   with \<open>card (affected f) \<ge> 1\<close> show ?thesis
diff -r c5d1a01d2d6c -r d7d90ed4c74e src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Library/Permutations.thy	Fri Sep 25 14:11:48 2020 +0100
@@ -334,20 +334,20 @@
   case (insert x F)
   {
     fix n
-    assume card_insert: "card (insert x F) = n"
+    assume card.insert_remove: "card (insert x F) = n"
     let ?xF = "{p. p permutes insert x F}"
     let ?pF = "{p. p permutes F}"
     let ?pF' = "{(b, p). b \<in> insert x F \<and> p \<in> ?pF}"
     let ?g = "(\<lambda>(b, p). Fun.swap x b id \<circ> p)"
     have xfgpF': "?xF = ?g ` ?pF'"
       by (rule permutes_insert[of x F])
-    from \<open>x \<notin> F\<close> \<open>finite F\<close> card_insert have Fs: "card F = n - 1"
+    from \<open>x \<notin> F\<close> \<open>finite F\<close> card.insert_remove have Fs: "card F = n - 1"
       by auto
     from \<open>finite F\<close> insert.hyps Fs have pFs: "card ?pF = fact (n - 1)"
       by auto
     then have "finite ?pF"
       by (auto intro: card_ge_0_finite)
-    with \<open>finite F\<close> card_insert have pF'f: "finite ?pF'"
+    with \<open>finite F\<close> card.insert_remove have pF'f: "finite ?pF'"
       apply (simp only: Collect_case_prod Collect_mem_eq)
       apply (rule finite_cartesian_product)
       apply simp_all
@@ -383,13 +383,13 @@
       then show ?thesis
         unfolding inj_on_def by blast
     qed
-    from \<open>x \<notin> F\<close> \<open>finite F\<close> card_insert have "n \<noteq> 0"
+    from \<open>x \<notin> F\<close> \<open>finite F\<close> card.insert_remove have "n \<noteq> 0"
       by auto
     then have "\<exists>m. n = Suc m"
       by presburger
     then obtain m where n: "n = Suc m"
       by blast
-    from pFs card_insert have *: "card ?xF = fact n"
+    from pFs card.insert_remove have *: "card ?xF = fact n"
       unfolding xfgpF' card_image[OF ginj]
       using \<open>finite F\<close> \<open>finite ?pF\<close>
       by (simp only: Collect_case_prod Collect_mem_eq card_cartesian_product) (simp add: n)
diff -r c5d1a01d2d6c -r d7d90ed4c74e src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/List.thy	Fri Sep 25 14:11:48 2020 +0100
@@ -5326,7 +5326,7 @@
   assumes "k < card A"
   shows "card {xs. length xs = k \<and> distinct xs \<and> set xs \<subseteq> A} = \<Prod>{card A - k + 1 .. card A}"
 proof -
-  from \<open>k < card A\<close> have "finite A" and "k \<le> card A" using card_infinite by force+
+  from \<open>k < card A\<close> have "finite A" and "k \<le> card A" using card.infinite by force+
   from this show ?thesis by (rule card_lists_distinct_length_eq)
 qed
 
diff -r c5d1a01d2d6c -r d7d90ed4c74e src/HOL/Number_Theory/Quadratic_Reciprocity.thy
--- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Fri Sep 25 14:11:48 2020 +0100
@@ -294,7 +294,7 @@
   have "B \<inter> C = {}" "finite B" "finite C" "B \<union> C = BuC"
     unfolding B_def C_def BuC_def by fastforce+
   then show ?thesis
-    unfolding b_def c_def using card_empty card_Un_Int QR_lemma_04 QR_lemma_05 by fastforce
+    unfolding b_def c_def using card.empty card_Un_Int QR_lemma_04 QR_lemma_05 by fastforce
 qed
 
 definition f_2:: "int \<Rightarrow> int"
diff -r c5d1a01d2d6c -r d7d90ed4c74e src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy
--- a/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy	Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy	Fri Sep 25 14:11:48 2020 +0100
@@ -235,7 +235,7 @@
         assume H: "liseq' xs j = card is" "is \<in> iseq xs (Suc j)"
           "finite is" "Max is = j" "is \<noteq> {}"
         from H j have "card is + 1 = card (is \<union> {i})"
-          by (simp add: card_insert max_notin)
+          by (simp add: card.insert_remove max_notin)
         moreover {
           from H j have "xs (Max is) \<le> xs i" by simp
           moreover from \<open>j < i\<close> have "Suc j \<le> i" by simp
@@ -367,7 +367,7 @@
   apply (rule_tac xs=xs and i=i in liseq'_expand)
   apply simp
   apply (rule_tac js="isa \<union> {j}" in liseq_eq [symmetric])
-  apply (simp add: card_insert card_Diff_singleton_if max_notin)
+  apply (simp add: card.insert_remove card_Diff_singleton_if max_notin)
   apply (rule iseq_insert)
   apply simp
   apply (erule iseq_mono)
@@ -388,9 +388,9 @@
   apply simp
   apply (rule le_diff_iff [THEN iffD1, of 1])
   apply (simp add: card_0_eq [symmetric] del: card_0_eq)
-  apply (simp add: card_insert)
+  apply (simp add: card.insert_remove)
   apply (subgoal_tac "card (js' - {j}) = card js' - 1")
-  apply (simp add: card_insert card_Diff_singleton_if max_notin)
+  apply (simp add: card.insert_remove card_Diff_singleton_if max_notin)
   apply (frule_tac A=js' in Max_in)
   apply assumption
   apply (simp add: card_Diff_singleton_if)
@@ -411,7 +411,7 @@
   apply (rule_tac xs=xs and i=i in liseq'_expand)
   apply simp
   apply (rule_tac js="isa \<union> {j}" in liseq'_eq [symmetric])
-  apply (simp add: card_insert card_Diff_singleton_if max_notin)
+  apply (simp add: card.insert_remove card_Diff_singleton_if max_notin)
   apply (rule iseq_insert)
   apply simp
   apply (erule iseq_mono)
@@ -434,9 +434,9 @@
   apply simp
   apply (rule le_diff_iff [THEN iffD1, of 1])
   apply (simp add: card_0_eq [symmetric] del: card_0_eq)
-  apply (simp add: card_insert)
+  apply (simp add: card.insert_remove)
   apply (subgoal_tac "card (js' - {j}) = card js' - 1")
-  apply (simp add: card_insert card_Diff_singleton_if max_notin)
+  apply (simp add: card.insert_remove card_Diff_singleton_if max_notin)
   apply (frule_tac A=js' in Max_in)
   apply assumption
   apply (simp add: card_Diff_singleton_if)
diff -r c5d1a01d2d6c -r d7d90ed4c74e src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Set_Interval.thy	Fri Sep 25 14:11:48 2020 +0100
@@ -1538,7 +1538,7 @@
   also have "\<dots> = Suc (card ({k \<in> M. k < Suc i} - {0}))"
     by (force intro: arg_cong [where f=card])
   also have "\<dots> = card (insert 0 ({k \<in> M. k < Suc i} - {0}))"
-    by (simp add: card_insert)
+    by (simp add: card.insert_remove)
   also have "... = card {k \<in> M. k < Suc i}"
     using assms
     by (force simp add: intro: arg_cong [where f=card])
diff -r c5d1a01d2d6c -r d7d90ed4c74e src/HOL/Vector_Spaces.thy
--- a/src/HOL/Vector_Spaces.thy	Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Vector_Spaces.thy	Fri Sep 25 14:11:48 2020 +0100
@@ -1453,7 +1453,7 @@
 
     have "b \<notin> f ` B1" using vs2.span_base[of b "f ` B1"] b by auto
     then have "Suc (card B1) = card (insert b (f ` B1))"
-      using sf[THEN inj_on_subset, of B1] by (subst card_insert) (auto intro: vs1.finite_Basis simp: card_image)
+      using sf[THEN inj_on_subset, of B1] by (subst card.insert_remove) (auto intro: vs1.finite_Basis simp: card_image)
     also have "\<dots> = vs2.dim (insert b (f ` B1))"
       using vs2.dim_eq_card_independent[OF **] by simp
     also have "vs2.dim (insert b (f ` B1)) \<le> vs2.dim B2"