author haftmann Sat, 06 Mar 2021 18:42:10 +0000 changeset 73392 24f0df084aad parent 73391 f16f209f996c child 73393 716d256259d5
reduced dependencies on theory List_Permutation
```--- 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"```