summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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

src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy | file | annotate | diff | comparison | revisions |

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