equal
deleted
inserted
replaced
1 (* Author: Johannes Hölzl, TU München *) |
1 (* Author: Johannes Hölzl, TU München *) |
2 |
2 |
3 section \<open>Formalization of a Countermeasure by Koepf \& Duermuth 2009\<close> |
3 section \<open>Formalization of a Countermeasure by Koepf \& Duermuth 2009\<close> |
4 |
4 |
5 theory Koepf_Duermuth_Countermeasure |
5 theory Koepf_Duermuth_Countermeasure |
6 imports "~~/src/HOL/Probability/Information" "~~/src/HOL/Library/Permutation" |
6 imports "HOL-Probability.Information" "HOL-Library.Permutation" |
7 begin |
7 begin |
8 |
8 |
9 lemma SIGMA_image_vimage: |
9 lemma SIGMA_image_vimage: |
10 "snd ` (SIGMA x:f`X. f -` {x} \<inter> X) = X" |
10 "snd ` (SIGMA x:f`X. f -` {x} \<inter> X) = X" |
11 by (auto simp: image_iff) |
11 by (auto simp: image_iff) |