src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy

       proof (rule liseq'_expand)
         fix "is"
         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
           with \<open>is \<in> iseq xs (Suc j)\<close> have "is \<in> iseq xs i"
             by (rule iseq_mono)

   apply (rule_tac xs=xs and i=j in liseq_expand)
   apply simp
   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)
   apply simp
   apply (case_tac "j = Max js'")

   apply (simp add: less_eq_Suc_le [symmetric])
   apply (rule Max_diff)
   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)
   apply (drule_tac js=js' in iseq_butlast)
   apply assumption

   apply (rule_tac xs=xs and i=j in liseq_expand)
   apply simp
   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)
   apply simp
   apply simp

   apply (simp add: less_eq_Suc_le [symmetric])
   apply (rule Max_diff)
   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)
   done