# HG changeset patch
# User haftmann
# Date 1615056130 0
# Node ID 24f0df084aad5fd6e07c16a1ca28a007f658f5c6
# Parent  f16f209f996c9d49fb719430503ec56bff716f19
reduced dependencies on theory List_Permutation

diff -r f16f209f996c -r 24f0df084aad src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Fri Mar 05 22:23:57 2021 +0100
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Sat Mar 06 18:42:10 2021 +0000
@@ -3,7 +3,7 @@
 section \<open>Formalization of a Countermeasure by Koepf \& Duermuth 2009\<close>
 
 theory Koepf_Duermuth_Countermeasure
-  imports "HOL-Probability.Information" "HOL-Library.List_Permutation"
+  imports "HOL-Probability.Information"
 begin
 
 lemma SIGMA_image_vimage:
@@ -237,10 +237,14 @@
   assumes "t xs = t ys"
   shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))"
 proof -
-  have "count (mset xs) = count (mset ys)"
-    using assms by (simp add: fun_eq_iff count_mset t_def)
-  then have "xs <~~> ys" unfolding mset_eq_perm count_inject .
-  then show ?thesis by (rule permutation_Ex_bij)
+  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)
+  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>
+    by (auto dest: permutes_imp_bij simp add: permute_list_nth)
+  then show ?thesis
+    by blast
 qed
 
 lemma \<P>_k: assumes "k \<in> keys" shows "\<P>(fst) {k} = K k"