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