# HG changeset patch
# User nipkow
# Date 1750134595 -7200
# Node ID 71574900b6ba3e30597f2e8e70b672cdc5d17d3e
# Parent  3b98b1b57435f3ffc7fe3cfc86cc7677129825cf# Parent  acd065f001943f7890810a652ea84d2bb3f1f8c4
merged

diff -r 3b98b1b57435 -r 71574900b6ba src/HOL/Combinatorics/Permutations.thy
--- a/src/HOL/Combinatorics/Permutations.thy	Mon Jun 16 15:25:38 2025 +0200
+++ b/src/HOL/Combinatorics/Permutations.thy	Tue Jun 17 06:29:55 2025 +0200
@@ -1688,7 +1688,7 @@
   also from assms have "card \<dots> = card {i. i < length xs \<and> y = xs ! i}"
     by (intro card_vimage_inj) (auto simp: permutes_inj permutes_surj)
   also have "\<dots> = count (mset xs) y"
-    by (simp add: count_mset length_filter_conv_card)
+    by (simp add: count_mset count_list_eq_length_filter length_filter_conv_card)
   finally show "count (mset (permute_list f xs)) y = count (mset xs) y"
     by simp
 qed
diff -r 3b98b1b57435 -r 71574900b6ba src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Jun 16 15:25:38 2025 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue Jun 17 06:29:55 2025 +0200
@@ -1998,7 +1998,7 @@
   by (induct xs) simp_all
 
 lemma count_mset:
-  "count (mset xs) x = length (filter (\<lambda>y. x = y) xs)"
+  "count (mset xs) x = count_list xs x"
   by (induct xs) simp_all
 
 lemma mset_zero_iff[simp]: "(mset x = {#}) = (x = [])"
@@ -2107,7 +2107,7 @@
 
 lemma mset_eq_length_filter:
   assumes "mset xs = mset ys"
-  shows "length (filter (\<lambda>x. z = x) xs) = length (filter (\<lambda>y. z = y) ys)"
+  shows "count_list xs z = count_list ys z"
   using assms by (metis count_mset)
 
 lemma fold_multiset_equiv:
@@ -2232,7 +2232,7 @@
 qed
 
 lemma mset_minus_list_mset[simp]: "mset(minus_list_mset xs ys) = mset xs - mset ys"
-by(induction ys) (auto)
+by (simp add: count_mset multiset_eq_iff)
 
 lemma mset_set_set: "distinct xs \<Longrightarrow> mset_set (set xs) = mset xs"
   by (induction xs) simp_all
@@ -3075,7 +3075,7 @@
   from multiset show "mset ys = mset xs" .
   from \<open>sorted ys\<close> show "sorted (map (\<lambda>x. x) ys)" by simp
   from multiset have "length (filter (\<lambda>y. k = y) ys) = length (filter (\<lambda>x. k = x) xs)" for k
-    by (rule mset_eq_length_filter)
+    by (metis mset_filter size_mset)
   then have "replicate (length (filter (\<lambda>y. k = y) ys)) k =
     replicate (length (filter (\<lambda>x. k = x) xs)) k" for k
     by simp
diff -r 3b98b1b57435 -r 71574900b6ba src/HOL/List.thy
--- 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)"
diff -r 3b98b1b57435 -r 71574900b6ba src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Mon Jun 16 15:25:38 2025 +0200
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Tue Jun 17 06:29:55 2025 +0200
@@ -238,7 +238,7 @@
   shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))"
 proof -
   from assms have \<open>mset xs = mset ys\<close>
-    using assms by (simp add: fun_eq_iff t_def multiset_eq_iff flip: count_mset)
+    using assms by (simp add: fun_eq_iff t_def multiset_eq_iff count_mset count_list_eq_length_filter)
   then obtain p where \<open>p permutes {..<length ys}\<close> \<open>permute_list p ys = xs\<close>
     by (rule mset_eq_permutation)
   then have \<open>bij_betw p {..<length xs} {..<length ys}\<close> \<open>\<forall>i<length xs. xs ! i = ys ! p i\<close>