1 theory Dining_Cryptographers |
1 theory Dining_Cryptographers |
2 imports "~~/src/HOL/Probability/Information" |
2 imports "~~/src/HOL/Probability/Information" |
3 begin |
3 begin |
|
4 |
|
5 lemma 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 |
|
8 lemma Ex1_eq: "\<exists>! x. P x \<Longrightarrow> P x \<Longrightarrow> P y \<Longrightarrow> x = y" |
|
9 by auto |
4 |
10 |
5 locale finite_space = |
11 locale finite_space = |
6 fixes S :: "'a set" |
12 fixes S :: "'a set" |
7 assumes finite[simp]: "finite S" |
13 assumes finite[simp]: "finite S" |
8 and not_empty[simp]: "S \<noteq> {}" |
14 and not_empty[simp]: "S \<noteq> {}" |
25 sublocale finite_space \<subseteq> information_space M 2 |
31 sublocale finite_space \<subseteq> information_space M 2 |
26 by default (simp_all add: M_def one_ereal_def) |
32 by default (simp_all add: M_def one_ereal_def) |
27 |
33 |
28 lemma (in finite_space) \<mu>'_eq[simp]: "\<mu>' A = (if A \<subseteq> S then card A / card S else 0)" |
34 lemma (in finite_space) \<mu>'_eq[simp]: "\<mu>' A = (if A \<subseteq> S then card A / card S else 0)" |
29 unfolding \<mu>'_def by (auto simp: M_def) |
35 unfolding \<mu>'_def by (auto simp: M_def) |
30 |
|
31 lemma set_of_list_extend: |
|
32 "{xs. length xs = Suc n \<and> (\<forall>x\<in>set xs. x \<in> A)} = |
|
33 (\<lambda>(xs, n). n#xs) ` ({xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)} \<times> A)" |
|
34 (is "?lists (Suc n) = _") |
|
35 proof |
|
36 show "(\<lambda>(xs, n). n#xs) ` (?lists n \<times> A) \<subseteq> ?lists (Suc n)" by auto |
|
37 show "?lists (Suc n) \<subseteq> (\<lambda>(xs, n). n#xs) ` (?lists n \<times> A)" |
|
38 proof |
|
39 fix x assume "x \<in> ?lists (Suc n)" |
|
40 moreover |
|
41 hence "x \<noteq> []" by auto |
|
42 then obtain t h where "x = h # t" by (cases x) auto |
|
43 ultimately show "x \<in> (\<lambda>(xs, n). n#xs) ` (?lists n \<times> A)" |
|
44 by (auto intro!: image_eqI[where x="(t, h)"]) |
|
45 qed |
|
46 qed |
|
47 |
|
48 lemma card_finite_list_length: |
|
49 assumes "finite A" |
|
50 shows "(card {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)} = (card A)^n) \<and> |
|
51 finite {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)}" |
|
52 (is "card (?lists n) = _ \<and> _") |
|
53 proof (induct n) |
|
54 case 0 have "{xs. length xs = 0 \<and> (\<forall>x\<in>set xs. x \<in> A)} = {[]}" by auto |
|
55 thus ?case by simp |
|
56 next |
|
57 case (Suc n) |
|
58 moreover note set_of_list_extend[of n A] |
|
59 moreover have "inj_on (\<lambda>(xs, n). n#xs) (?lists n \<times> A)" |
|
60 by (auto intro!: inj_onI) |
|
61 ultimately show ?case using assms by (auto simp: card_image) |
|
62 qed |
|
63 |
|
64 lemma |
|
65 assumes "finite A" |
|
66 shows finite_lists: "finite {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)}" |
|
67 and card_list_length: "card {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)} = (card A)^n" |
|
68 using card_finite_list_length[OF assms, of n] by auto |
|
69 |
36 |
70 section "Define the state space" |
37 section "Define the state space" |
71 |
38 |
72 text {* |
39 text {* |
73 |
40 |
168 have *: "{xs. length xs = n} \<noteq> {}" |
135 have *: "{xs. length xs = n} \<noteq> {}" |
169 by (auto intro!: exI[of _ "replicate n undefined"]) |
136 by (auto intro!: exI[of _ "replicate n undefined"]) |
170 show ?thesis |
137 show ?thesis |
171 unfolding payer_def_raw dc_crypto fst_image_times if_not_P[OF *] .. |
138 unfolding payer_def_raw dc_crypto fst_image_times if_not_P[OF *] .. |
172 qed |
139 qed |
173 |
|
174 lemma image_ex1_eq: "inj_on f A \<Longrightarrow> (b \<in> f ` A) \<longleftrightarrow> (\<exists>!x \<in> A. b = f x)" |
|
175 by (unfold inj_on_def) blast |
|
176 |
|
177 lemma Ex1_eq: "\<exists>! x. P x \<Longrightarrow> P x \<Longrightarrow> P y \<Longrightarrow> x = y" |
|
178 by auto |
|
179 |
140 |
180 lemma card_payer_and_inversion: |
141 lemma card_payer_and_inversion: |
181 assumes "xs \<in> inversion ` dc_crypto" and "i < n" |
142 assumes "xs \<in> inversion ` dc_crypto" and "i < n" |
182 shows "card {dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs} = 2" |
143 shows "card {dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs} = 2" |
183 (is "card ?S = 2") |
144 (is "card ?S = 2") |
339 using `0 < length zs` by (cases zs) simp_all |
300 using `0 < length zs` by (cases zs) simp_all |
340 ultimately show ?thesis by simp |
301 ultimately show ?thesis by simp |
341 qed |
302 qed |
342 |
303 |
343 lemma finite_dc_crypto: "finite dc_crypto" |
304 lemma finite_dc_crypto: "finite dc_crypto" |
344 using finite_lists[where A="UNIV :: bool set"] |
305 using finite_lists_length_eq[where A="UNIV :: bool set"] |
345 unfolding dc_crypto by simp |
306 unfolding dc_crypto by simp |
346 |
307 |
347 lemma card_inversion: |
308 lemma card_inversion: |
348 assumes "xs \<in> inversion ` dc_crypto" |
309 assumes "xs \<in> inversion ` dc_crypto" |
349 shows "card {dc \<in> dc_crypto. inversion dc = xs} = 2 * n" |
310 shows "card {dc \<in> dc_crypto. inversion dc = xs} = 2 * n" |
399 qed |
360 qed |
400 |
361 |
401 lemma card_dc_crypto: |
362 lemma card_dc_crypto: |
402 "card dc_crypto = n * 2^n" |
363 "card dc_crypto = n * 2^n" |
403 unfolding dc_crypto |
364 unfolding dc_crypto |
404 using card_list_length[of "UNIV :: bool set"] |
365 using card_lists_length_eq[of "UNIV :: bool set"] |
405 by (simp add: card_cartesian_product card_image) |
366 by (simp add: card_cartesian_product card_image) |
406 |
367 |
407 lemma card_image_inversion: |
368 lemma card_image_inversion: |
408 "card (inversion ` dc_crypto) = 2^(n - 1)" |
369 "card (inversion ` dc_crypto) = 2^(n - 1)" |
409 proof - |
370 proof - |
510 by (auto simp add: card_dc_crypto card_payer_and_inversion distribution_def) |
471 by (auto simp add: card_dc_crypto card_payer_and_inversion distribution_def) |
511 moreover |
472 moreover |
512 from z have "payer -` {z} \<inter> dc_crypto = {z} \<times> {xs. length xs = n}" |
473 from z have "payer -` {z} \<inter> dc_crypto = {z} \<times> {xs. length xs = n}" |
513 by (auto simp: dc_crypto payer_def) |
474 by (auto simp: dc_crypto payer_def) |
514 hence "card (payer -` {z} \<inter> dc_crypto) = 2^n" |
475 hence "card (payer -` {z} \<inter> dc_crypto) = 2^n" |
515 using card_list_length[where A="UNIV::bool set"] |
476 using card_lists_length_eq[where A="UNIV::bool set"] |
516 by (simp add: card_cartesian_product_singleton) |
477 by (simp add: card_cartesian_product_singleton) |
517 hence "?dP {z} = 1 / real n" |
478 hence "?dP {z} = 1 / real n" |
518 by (simp add: distribution_def card_dc_crypto) |
479 by (simp add: distribution_def card_dc_crypto) |
519 ultimately |
480 ultimately |
520 show "?dIP {(x,z)} * log 2 (?dIP {(x,z)} / ?dP {z}) = |
481 show "?dIP {(x,z)} * log 2 (?dIP {(x,z)} / ?dP {z}) = |