1theory Dining_Cryptographers
2imports "HOL-Probability.Information"
3begin
4
5lemma image_ex1_eq: "inj_on f A \<Longrightarrow> (b \<in> f ` A) \<longleftrightarrow> (\<exists>!x \<in> A. b = f x)"
6  by (unfold inj_on_def) blast
7
8lemma Ex1_eq: "\<exists>!x. P x \<Longrightarrow> P x \<Longrightarrow> P y \<Longrightarrow> x = y"
9  by auto
10
11subsection \<open>Define the state space\<close>
12
13text \<open>
14
15We introduce the state space on which the algorithm operates.
16
17This contains:
18
19\begin{description}
20\item[n]
21  The number of cryptographers on the table.
22
23\item[payer]
24  Either one of the cryptographers or the NSA.
25
26\item[coin]
27  The result of the coin flipping for each cryptographer.
28
29\item[inversion]
30  The public result for each cryptographer, e.g. the sum of the coin flipping
31  for the cryptographer, its right neighbour and the information if he paid or
32  not.
33
34\end{description}
35
36The observables are the \emph{inversions}
37
38\<close>
39
40locale dining_cryptographers_space =
41  fixes n :: nat
42  assumes n_gt_3: "n \<ge> 3"
43begin
44
45definition "dining_cryptographers =
46  ({None} \<union> Some ` {0..<n}) \<times> {xs :: bool list. length xs = n}"
47definition "payer dc = fst dc"
48definition coin :: "(nat option \<times> bool list) \<Rightarrow> nat \<Rightarrow> bool" where
49  "coin dc c = snd dc ! (c mod n)"
50definition "inversion dc =
51  map (\<lambda>c. (payer dc = Some c) \<noteq> (coin dc c \<noteq> coin dc (c + 1))) [0..<n]"
52
53definition "result dc = foldl (\<lambda> a b. a \<noteq> b) False (inversion dc)"
54
55lemma coin_n[simp]: "coin dc n = coin dc 0"
56  unfolding coin_def by simp
57
58theorem correctness:
59  assumes "dc \<in> dining_cryptographers"
60  shows "result dc \<longleftrightarrow> (payer dc \<noteq> None)"
61proof -
62  let ?XOR = "\<lambda>f l. foldl (\<noteq>) False (map f [0..<l])"
63
64  have foldl_coin:
65    "\<not> ?XOR (\<lambda>c. coin dc c \<noteq> coin dc (c + 1)) n"
66  proof -
67    define n' where "n' = n" \<comment> \<open>Need to hide n, as it is hidden in coin\<close>
68    have "?XOR (\<lambda>c. coin dc c \<noteq> coin dc (c + 1)) n'
69        = (coin dc 0 \<noteq> coin dc n')"
70      by (induct n') auto
71    thus ?thesis using \<open>n' \<equiv> n\<close> by simp
72  qed
73
74  from assms have "payer dc = None \<or> (\<exists>k<n. payer dc = Some k)"
75    unfolding dining_cryptographers_def payer_def by auto
76  thus ?thesis
77  proof (rule disjE)
78    assume "payer dc = None"
79    thus ?thesis unfolding result_def inversion_def
80      using foldl_coin by simp
81  next
82    assume "\<exists>k<n. payer dc = Some k"
83    then obtain k where "k < n" and "payer dc = Some k" by auto
84    define l where "l = n" \<comment> \<open>Need to hide n, as it is hidden in coin, payer etc.\<close>
85    have "?XOR (\<lambda>c. (payer dc = Some c) \<noteq> (coin dc c \<noteq> coin dc (c + 1))) l =
86        ((k < l) \<noteq> ?XOR (\<lambda>c. (coin dc c \<noteq> coin dc (c + 1))) l)"
87      using \<open>payer dc = Some k\<close> by (induct l) auto
88    thus ?thesis
89      unfolding result_def inversion_def l_def
90      using \<open>payer dc = Some k\<close> foldl_coin \<open>k < n\<close> by simp
91  qed
92qed
93
94text \<open>
95
96We now restrict the state space for the dining cryptographers to the cases when
97one of the cryptographer pays.
98
99\<close>
100
101definition
102  "dc_crypto = dining_cryptographers - {None}\<times>UNIV"
103
104lemma dc_crypto: "dc_crypto = Some ` {0..<n} \<times> {xs :: bool list. length xs = n}"
105  unfolding dc_crypto_def dining_cryptographers_def by auto
106
107lemma image_payer_dc_crypto: "payer ` dc_crypto = Some ` {0..<n}"
108proof -
109  have *: "{xs. length xs = n} \<noteq> {}"
110    by (auto intro!: exI[of _ "replicate n undefined"])
111  show ?thesis
112    unfolding payer_def [abs_def] dc_crypto fst_image_times if_not_P[OF *] ..
113qed
114
115lemma card_payer_and_inversion:
116  assumes "xs \<in> inversion ` dc_crypto" and "i < n"
117  shows "card {dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs} = 2"
118    (is "card ?S = 2")
119proof -
120  obtain ys j where xs_inv: "inversion (Some j, ys) = xs" and
121    "j < n" and "(Some j, ys) \<in> dc_crypto"
122    using assms(1) by (auto simp: dc_crypto)
123
124  hence "length ys = n" by (simp add: dc_crypto)
125  have [simp]: "length xs = n" using xs_inv[symmetric] by (simp add: inversion_def)
126
127  { fix b
128    have "inj_on (\<lambda>x. inversion (Some i, x)) {ys. ys ! 0 = b \<and> length ys = length xs}"
129    proof (rule inj_onI)
130      fix x y
131      assume "x \<in> {ys. ys ! 0 = b \<and> length ys = length xs}"
132        and "y \<in> {ys. ys ! 0 = b \<and> length ys = length xs}"
133        and inv: "inversion (Some i, x) = inversion (Some i, y)"
134      hence [simp]: "x ! 0 = y ! 0" "length y = n" "length x = n"
135        using \<open>length xs = n\<close> by simp_all
136      have *: "\<And>j. j < n \<Longrightarrow>
137        (x ! j = x ! (Suc j mod n)) = (y ! j = y ! (Suc j mod n))"
138        using inv unfolding inversion_def map_eq_conv payer_def coin_def
139        by fastforce
140      show "x = y"
141      proof (rule nth_equalityI, simp)
142        fix j assume "j < length x" hence "j < n" using \<open>length xs = n\<close> by simp
143        thus "x ! j = y ! j"
144        proof (induct j)
145          case (Suc j)
146          hence "j < n" by simp
147          with Suc show ?case using *[OF \<open>j < n\<close>]
148            by (cases "y ! j") simp_all
149        qed simp
150      qed
151    qed }
152  note inj_inv = this
153
154  txt \<open>
155    We now construct the possible inversions for \<^term>\<open>xs\<close> when the payer is
156    \<^term>\<open>i\<close>.
157\<close>
158
159  define zs where "zs = map (\<lambda>p. if p \<in> {min i j<..max i j} then \<not> ys ! p else ys ! p) [0..<n]"
160  hence [simp]: "length zs = n" by simp
161  hence [simp]: "0 < length zs" using n_gt_3 by simp
162
163  have "\<And>l. l < max i j \<Longrightarrow> Suc l mod n = Suc l"
164    using \<open>i < n\<close> \<open>j < n\<close> by auto
165  { fix l assume "l < n"
166    hence "(((l < min i j \<or> l = min i j) \<or> (min i j < l \<and> l < max i j)) \<or> l = max i j) \<or> max i j < l" by auto
167    hence "((i = l) = (zs ! l = zs ! (Suc l mod n))) = ((j = l) = (ys ! l = ys ! (Suc l mod n)))"
168    apply - proof ((erule disjE)+)
169      assume "l < min i j"
170      hence "l \<noteq> i" and "l \<noteq> j" and "zs ! l = ys ! l" and
171        "zs ! (Suc l mod n) = ys ! (Suc l mod n)" using \<open>i < n\<close> \<open>j < n\<close> unfolding zs_def by auto
172      thus ?thesis by simp
173    next
174      assume "l = min i j"
175      show ?thesis
176      proof (cases rule: linorder_cases)
177        assume "i < j"
178        hence "l = i" and "Suc l < n" and "i \<noteq> j" and "Suc l \<le> max i j" using \<open>l = min i j\<close> using \<open>j < n\<close> by auto
179        hence "zs ! l = ys ! l" and "zs ! (Suc l mod n) = (\<not> ys ! (Suc l mod n))"
180          using \<open>l = min i j\<close>[symmetric] by (simp_all add: zs_def)
181        thus ?thesis using \<open>l = i\<close> \<open>i \<noteq> j\<close> by simp
182      next
183        assume "j < i"
184        hence "l = j" and "Suc l < n" and "i \<noteq> j" and "Suc l \<le> max i j" using \<open>l = min i j\<close> using \<open>i < n\<close> by auto
185        hence "zs ! l = ys ! l" and "zs ! (Suc l mod n) = (\<not> ys ! (Suc l mod n))"
186          using \<open>l = min i j\<close>[symmetric] by (simp_all add: zs_def)
187        thus ?thesis using \<open>l = j\<close> \<open>i \<noteq> j\<close> by simp
188      next
189        assume "i = j"
190        hence "i = j" and "max i j = l" and "min i j = l" and "zs = ys"
191          using \<open>l = min i j\<close> by (simp_all add: zs_def \<open>length ys = n\<close>[symmetric] map_nth)
192        thus ?thesis by simp
193      qed
194    next
195      assume "min i j < l \<and> l < max i j"
196      hence "i \<noteq> l" and "j \<noteq> l" and "zs ! l = (\<not> ys ! l)"
197        "zs ! (Suc l mod n) = (\<not> ys ! (Suc l mod n))"
198        using \<open>i < n\<close> \<open>j < n\<close> by (auto simp: zs_def)
199      thus ?thesis by simp
200    next
201      assume "l = max i j"
202      show ?thesis
203      proof (cases rule: linorder_cases)
204        assume "i < j"
205        hence "l = j" and "i \<noteq> j" using \<open>l = max i j\<close> using \<open>j < n\<close> by auto
206        have "zs ! (Suc l mod n) = ys ! (Suc l mod n)"
207          using \<open>j < n\<close> \<open>i < j\<close> \<open>l = j\<close> by (cases "Suc l = n") (auto simp add: zs_def)
208        moreover have "zs ! l = (\<not> ys ! l)"
209          using \<open>j < n\<close> \<open>i < j\<close> by (auto simp add: \<open>l = j\<close> zs_def)
210        ultimately show ?thesis using \<open>l = j\<close> \<open>i \<noteq> j\<close> by simp
211      next
212        assume "j < i"
213        hence "l = i" and "i \<noteq> j" using \<open>l = max i j\<close> by auto
214        have "zs ! (Suc l mod n) = ys ! (Suc l mod n)"
215          using \<open>i < n\<close> \<open>j < i\<close> \<open>l = i\<close> by (cases "Suc l = n") (auto simp add: zs_def)
216        moreover have "zs ! l = (\<not> ys ! l)"
217          using \<open>i < n\<close> \<open>j < i\<close> by (auto simp add: \<open>l = i\<close> zs_def)
218        ultimately show ?thesis using \<open>l = i\<close> \<open>i \<noteq> j\<close> by auto
219      next
220        assume "i = j"
221        hence "i = j" and "max i j = l" and "min i j = l" and "zs = ys"
222          using \<open>l = max i j\<close> by (simp_all add: zs_def \<open>length ys = n\<close>[symmetric] map_nth)
223        thus ?thesis by simp
224      qed
225    next
226      assume "max i j < l"
227      hence "j \<noteq> l" and "i \<noteq> l" by simp_all
228      have "zs ! (Suc l mod n) = ys ! (Suc l mod n)"
229        using \<open>l < n\<close> \<open>max i j < l\<close> by (cases "Suc l = n") (auto simp add: zs_def)
230      moreover have "zs ! l = ys ! l"
231        using \<open>l < n\<close> \<open>max i j < l\<close> by (auto simp add: zs_def)
232      ultimately show ?thesis using \<open>j \<noteq> l\<close> \<open>i \<noteq> l\<close> by auto
233    qed }
234  hence zs: "inversion (Some i, zs) = xs"
235    by (simp add: xs_inv[symmetric] inversion_def coin_def payer_def)
236  moreover
237  from zs have Not_zs: "inversion (Some i, (map Not zs)) = xs"
238    by (simp add: xs_inv[symmetric] inversion_def coin_def payer_def)
239  ultimately
240  have "{dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs} =
241    {(Some i, zs), (Some i, map Not zs)}"
242    using \<open>i < n\<close> [[ hypsubst_thin = true ]]
243  proof (safe, simp_all add:dc_crypto payer_def)
244    fix b assume [simp]: "length b = n"
245      and *: "inversion (Some i, b) = xs" and "b \<noteq> zs"
246    show "b = map Not zs"
247    proof (cases "b ! 0 = zs ! 0")
248      case True
249      hence zs: "zs \<in> {ys. ys ! 0 = b ! 0 \<and> length ys = length xs} \<and> xs = inversion (Some i, zs)"
250        using zs by simp
251      have b: "b \<in> {ys. ys ! 0 = b ! 0 \<and> length ys = length xs} \<and> xs = inversion (Some i, b)"
252        using * by simp
253      hence "b \<in> {ys. ys ! 0 = b ! 0 \<and> length ys = length xs}" ..
254      with *[symmetric] have "xs \<in> (\<lambda>x. inversion (Some i, x)) ` {ys. ys ! 0 = b ! 0 \<and> length ys = length xs}"
255         by (rule image_eqI)
256      from this[unfolded image_ex1_eq[OF inj_inv]] b zs
257      have "b = zs" by (rule Ex1_eq)
258      thus ?thesis using \<open>b \<noteq> zs\<close> by simp
259    next
260      case False
261      hence zs: "map Not zs \<in> {ys. ys ! 0 = b ! 0 \<and> length ys = length xs} \<and> xs = inversion (Some i, map Not zs)"
262        using Not_zs by (simp add: nth_map[OF \<open>0 < length zs\<close>])
263      have b: "b \<in> {ys. ys ! 0 = b ! 0 \<and> length ys = length xs} \<and> xs = inversion (Some i, b)"
264        using * by simp
265      hence "b \<in> {ys. ys ! 0 = b ! 0 \<and> length ys = length xs}" ..
266      with *[symmetric] have "xs \<in> (\<lambda>x. inversion (Some i, x)) ` {ys. ys ! 0 = b ! 0 \<and> length ys = length xs}"
267         by (rule image_eqI)
268      from this[unfolded image_ex1_eq[OF inj_inv]] b zs
269      show "b = map Not zs" by (rule Ex1_eq)
270    qed
271  qed
272  moreover
273  have "zs \<noteq> map Not zs"
274    using \<open>0 < length zs\<close> by (cases zs) simp_all
275  ultimately show ?thesis by simp
276qed
277
278lemma finite_dc_crypto: "finite dc_crypto"
279  using finite_lists_length_eq[where A="UNIV :: bool set"]
280  unfolding dc_crypto by simp
281
282lemma card_inversion:
283  assumes "xs \<in> inversion ` dc_crypto"
284  shows "card {dc \<in> dc_crypto. inversion dc = xs} = 2 * n"
285proof -
286  let ?set = "\<lambda>i. {dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs}"
287  let ?sets = "{?set i | i. i < n}"
288
289  have [simp]: "length xs = n" using assms
290    by (auto simp: dc_crypto inversion_def [abs_def])
291
292  have "{dc \<in> dc_crypto. inversion dc = xs} = (\<Union>i < n. ?set i)"
293    unfolding dc_crypto payer_def by auto
294  also have "\<dots> = (\<Union>?sets)" by auto
295  finally have eq_Union: "{dc \<in> dc_crypto. inversion dc = xs} = (\<Union>?sets)" by simp
296
297  have card_double: "2 * card ?sets = card (\<Union>?sets)"
298  proof (rule card_partition)
299    show "finite ?sets" by simp
300    { fix i assume "i < n"
301      have "?set i \<subseteq> dc_crypto" by auto
302      have "finite (?set i)" using finite_dc_crypto by auto }
303    thus "finite (\<Union>?sets)" by auto
304
305  next
306    fix c assume "c \<in> ?sets"
307    thus "card c = 2" using card_payer_and_inversion[OF assms] by auto
308
309  next
310    fix x y assume "x \<in> ?sets" and "y \<in> ?sets" "x \<noteq> y"
311    then obtain i j where xy: "x = ?set i" "y = ?set j" by auto
312    hence "i \<noteq> j" using \<open>x \<noteq> y\<close> by auto
313    thus "x \<inter> y = {}" using xy by auto
314  qed
315
316  have sets: "?sets = ?set ` {..< n}"
317    unfolding image_def by auto
318  { fix i j :: nat assume asm: "i \<noteq> j" "i < n" "j < n"
319    { assume iasm: "?set i = {}"
320      have "card (?set i) = 2"
321        using card_payer_and_inversion[OF assms \<open>i < n\<close>] by auto
322      hence "False"
323        using iasm by auto }
324    then obtain c where ci: "c \<in> ?set i" by blast
325    hence cj: "c \<notin> ?set j" using asm by auto
326    { assume "?set i = ?set j"
327      hence "False" using ci cj by auto }
328    hence "?set i \<noteq> ?set j" by auto }
329  hence "inj_on ?set {..< n}" unfolding inj_on_def by auto
330  from card_image[OF this]
331  have "card (?set ` {..< n}) = n" by auto
332  hence "card ?sets = n" using sets by auto
333  thus ?thesis using eq_Union card_double by auto
334qed
335
336lemma card_dc_crypto:
337  "card dc_crypto = n * 2^n"
338  unfolding dc_crypto
339  using card_lists_length_eq[of "UNIV :: bool set"]
340  by (simp add: card_cartesian_product card_image)
341
342lemma card_image_inversion:
343  "card (inversion ` dc_crypto) = 2^(n - 1)"
344proof -
345  let ?P = "{inversion -` {x} \<inter> dc_crypto |x. x \<in> inversion ` dc_crypto}"
346  have "\<Union>?P = dc_crypto" by auto
347
348  { fix a b assume *: "(a, b) \<in> dc_crypto"
349    have inv_SOME: "inversion (SOME x. inversion x = inversion (a, b) \<and> x \<in> dc_crypto) = inversion (a, b)"
350      apply (rule someI2)
351      by (auto simp: *) }
352  note inv_SOME = this
353
354  { fix a b assume *: "(a, b) \<in> dc_crypto"
355    have "(SOME x. inversion x = inversion (a, b) \<and> x \<in> dc_crypto) \<in> dc_crypto"
356      by (rule someI2) (auto simp: *) }
357  note SOME_inv_dc = this
358
359  have "bij_betw (\<lambda>s. inversion (SOME x. x \<in> s \<and> x \<in> dc_crypto))
360    {inversion -` {x} \<inter> dc_crypto |x. x \<in> inversion ` dc_crypto}
361    (inversion ` dc_crypto)"
362    unfolding bij_betw_def
363    by (auto intro!: inj_onI image_eqI simp: inv_SOME SOME_inv_dc)
364  hence card_eq: "card {inversion -` {x} \<inter> dc_crypto |x. x \<in> inversion ` dc_crypto} = card (inversion ` dc_crypto)"
365    by (rule bij_betw_same_card)
366
367  have "(2*n) * card (inversion ` dc_crypto) = card (\<Union>?P)"
368    unfolding card_eq[symmetric]
369  proof (rule card_partition)
370    have "\<Union>?P \<subseteq> dc_crypto" by auto
371    thus "finite (\<Union>?P)" using finite_dc_crypto by (auto intro: finite_subset)
372
373    have "?P = (\<lambda>x. inversion -` {x} \<inter> dc_crypto) ` (inversion ` dc_crypto)"
374      by auto
375    thus "finite ?P" using finite_dc_crypto by auto
376
377  next
378    fix c assume "c \<in> {inversion -` {x} \<inter> dc_crypto |x. x \<in> inversion ` dc_crypto}"
379    then obtain x where "c = inversion -` {x} \<inter> dc_crypto" and x: "x \<in> inversion ` dc_crypto" by auto
380    hence "c = {dc \<in> dc_crypto. inversion dc = x}" by auto
381    thus "card c = 2 * n" using card_inversion[OF x] by simp
382
383  next
384    fix x y assume "x \<in> ?P" "y \<in> ?P" and "x \<noteq> y"
385    then obtain i j where
386      x: "x = inversion -` {i} \<inter> dc_crypto" and i: "i \<in> inversion ` dc_crypto" and
387      y: "y = inversion -` {j} \<inter> dc_crypto" and j: "j \<in> inversion ` dc_crypto" by auto
388    show "x \<inter> y = {}" using x y \<open>x \<noteq> y\<close> by auto
389  qed
390  hence "2 * card (inversion ` dc_crypto) = 2 ^ n" unfolding \<open>\<Union>?P = dc_crypto\<close> card_dc_crypto
391    using n_gt_3 by auto
392  thus ?thesis by (cases n) auto
393qed
394
395end
396
397sublocale dining_cryptographers_space \<subseteq> prob_space "uniform_count_measure dc_crypto"
398  by (rule prob_space_uniform_count_measure[OF finite_dc_crypto])
399     (insert n_gt_3, auto simp: dc_crypto intro: exI[of _ "replicate n True"])
400
401sublocale dining_cryptographers_space \<subseteq> information_space "uniform_count_measure dc_crypto" 2
402  by standard auto
403
404notation (in dining_cryptographers_space)
405  mutual_information_Pow ("\<I>'( _ ; _ ')")
406
407notation (in dining_cryptographers_space)
408  entropy_Pow ("\<H>'( _ ')")
409
410notation (in dining_cryptographers_space)
411  conditional_entropy_Pow ("\<H>'( _ | _ ')")
412
413theorem (in dining_cryptographers_space)
414  "\<I>( inversion ; payer ) = 0"
415proof (rule mutual_information_eq_0_simple)
416  have n: "0 < n" using n_gt_3 by auto
417  have card_image_inversion:
418    "real (card (inversion ` dc_crypto)) = 2^n / 2"
419    unfolding card_image_inversion using \<open>0 < n\<close> by (cases n) auto
420
421  show inversion: "simple_distributed (uniform_count_measure dc_crypto) inversion (\<lambda>x. 2 / 2^n)"
422  proof (rule simple_distributedI)
423    show "simple_function (uniform_count_measure dc_crypto) inversion"
424      using finite_dc_crypto
425      by (auto simp: simple_function_def space_uniform_count_measure sets_uniform_count_measure)
426    fix x assume "x \<in> inversion ` space (uniform_count_measure dc_crypto)"
427    moreover have "inversion -` {x} \<inter> dc_crypto = {dc \<in> dc_crypto. inversion dc = x}" by auto
428    ultimately show "2 / 2^n = prob (inversion -` {x} \<inter> space (uniform_count_measure dc_crypto))"
429      using \<open>0 < n\<close>
430      by (simp add: card_inversion card_dc_crypto finite_dc_crypto
431                    subset_eq space_uniform_count_measure measure_uniform_count_measure)
432  qed simp
433
434  show "simple_distributed (uniform_count_measure dc_crypto) payer (\<lambda>x. 1 / real n)"
435  proof (rule simple_distributedI)
436    show "simple_function (uniform_count_measure dc_crypto) payer"
437      using finite_dc_crypto
438      by (auto simp: simple_function_def space_uniform_count_measure sets_uniform_count_measure)
439    fix z assume "z \<in> payer ` space (uniform_count_measure dc_crypto)"
440    then have "payer -` {z} \<inter> dc_crypto = {z} \<times> {xs. length xs = n}"
441      by (auto simp: dc_crypto payer_def space_uniform_count_measure cong del: image_cong_simp)
442    hence "card (payer -` {z} \<inter> dc_crypto) = 2^n"
443      using card_lists_length_eq[where A="UNIV::bool set"]
444      by (simp add: card_cartesian_product_singleton)
445    then show "1 / real n = prob (payer -` {z} \<inter> space (uniform_count_measure dc_crypto))"
446      using finite_dc_crypto
447      by (subst measure_uniform_count_measure) (auto simp add: card_dc_crypto space_uniform_count_measure)
448  qed simp
449
450  show "simple_distributed (uniform_count_measure dc_crypto) (\<lambda>x. (inversion x, payer x)) (\<lambda>x. 2 / (real n *2^n))"
451  proof (rule simple_distributedI)
452    show "simple_function (uniform_count_measure dc_crypto) (\<lambda>x. (inversion x, payer x))"
453      using finite_dc_crypto
454      by (auto simp: simple_function_def space_uniform_count_measure sets_uniform_count_measure)
455    fix x assume "x \<in> (\<lambda>x. (inversion x, payer x)) ` space (uniform_count_measure dc_crypto)"
456    then obtain i xs where x: "x = (inversion (Some i, xs), payer (Some i, xs))"
457      and "i < n" "length xs = n"
458      by (simp add: image_iff space_uniform_count_measure dc_crypto Bex_def) blast
459    then have xs: "inversion (Some i, xs) \<in> inversion`dc_crypto" and i: "Some i \<in> Some ` {0..<n}"
460      and x: "x = (inversion (Some i, xs), Some i)" by (simp_all add: payer_def dc_crypto)
461    moreover define ys where "ys = inversion (Some i, xs)"
462    ultimately have ys: "ys \<in> inversion`dc_crypto"
463      and "Some i \<in> Some ` {0..<n}" "x = (ys, Some i)" by simp_all
464    then have "(\<lambda>x. (inversion x, payer x)) -` {x} \<inter> space (uniform_count_measure dc_crypto) =
465      {dc \<in> dc_crypto. payer dc = Some (the (Some i)) \<and> inversion dc = ys}"
466      by (auto simp add: payer_def space_uniform_count_measure)
467    then show "2 / (real n * 2 ^ n) = prob ((\<lambda>x. (inversion x, payer x)) -` {x} \<inter> space (uniform_count_measure dc_crypto))"
468      using \<open>i < n\<close> ys
469      by (simp add: measure_uniform_count_measure card_payer_and_inversion finite_dc_crypto subset_eq card_dc_crypto)
470  qed simp
471
472  show "\<forall>x\<in>space (uniform_count_measure dc_crypto). 2 / (real n * 2 ^ n) = 2 / 2 ^ n * (1 / real n) "
473    by simp
474qed
475
476end
477