--- 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
--- 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
--- 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)"
--- 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>