--- a/src/HOL/List.thy Mon Jun 16 15:25:38 2025 +0200
+++ b/src/HOL/List.thy Tue Jun 17 06:29:55 2025 +0200
@@ -4521,6 +4521,9 @@
with 1 2 show ?thesis by blast
qed
+lemma count_list_eq_length_filter: "count_list xs y = length(filter ((=) y) xs)"
+by (induction xs) auto
+
lemma split_list_cycles:
"\<exists>pref xss. xs = pref @ concat xss \<and> x \<notin> set pref \<and> (\<forall>ys \<in> set xss. \<exists>zs. ys = x # zs)"
proof (induction "count_list xs x" arbitrary: xs)
@@ -4571,6 +4574,10 @@
subsubsection \<open>\<^const>\<open>remove1\<close>\<close>
+lemma count_list_remove1[simp]:
+ "count_list (remove1 a xs) b = count_list xs b - (if a=b then 1 else 0)"
+by(induction xs) auto
+
lemma remove1_append:
"remove1 x (xs @ ys) =
(if x \<in> set xs then remove1 x xs @ ys else xs @ remove1 x ys)"
@@ -4700,7 +4707,8 @@
text \<open>Conceptually, the result of \<^const>\<open>minus_list_mset\<close> is only determined up to permutation,
i.e. up to the multiset of elements. Thus this function comes into its own in connection
-with multisets where \<open>mset(minus_list_mset xs ys) = mset xs - mset ys\<close> is proved.\<close>
+with multisets where \<open>mset(minus_list_mset xs ys) = mset xs - mset ys\<close> is proved. Lemma
+\<open>count_list_minus_list_mset\<close> is the equivalent on the list level.\<close>
lemma minus_list_mset_Nil2 [simp]: "minus_list_mset xs [] = xs"
by (simp add: minus_list_mset_def)
@@ -4708,8 +4716,12 @@
lemma minus_list_mset_Cons2 [simp]: "minus_list_mset xs (y#ys) = remove1 y (minus_list_mset xs ys)"
by (simp add: minus_list_mset_def)
+lemma count_list_minus_list_mset[simp]:
+ "count_list (minus_list_mset xs ys) a = count_list xs a - count_list ys a"
+by(induction ys arbitrary: xs) auto
+
lemma minus_list_set_subset_minus_list_mset: "set xs - set ys \<subseteq> set(minus_list_mset xs ys)"
-by(induction ys arbitrary: xs)(simp, fastforce)
+by(induction ys)(simp, fastforce)
lemma minus_list_mset_remove1_commute:
"minus_list_mset (remove1 x xs) ys = remove1 x (minus_list_mset xs ys)"