theory Dining_Cryptographers imports "HOL-Probability.Information" begin lemma image_ex1_eq: "inj_on f A ⟹ (b ∈ f ` A) ⟷ (∃!x ∈ A. b = f x)" by (unfold inj_on_def) blast lemma Ex1_eq: "∃!x. P x ⟹ P x ⟹ P y ⟹ x = y" by auto subsection ‹Define the state space› text ‹ We introduce the state space on which the algorithm operates. This contains: \begin{description} \item[n] The number of cryptographers on the table. \item[payer] Either one of the cryptographers or the NSA. \item[coin] The result of the coin flipping for each cryptographer. \item[inversion] The public result for each cryptographer, e.g. the sum of the coin flipping for the cryptographer, its right neighbour and the information if he paid or not. \end{description} The observables are the \emph{inversions} › locale dining_cryptographers_space = fixes n :: nat assumes n_gt_3: "n ≥ 3" begin definition "dining_cryptographers = ({None} ∪ Some ` {0..<n}) × {xs :: bool list. length xs = n}" definition "payer dc = fst dc" definition coin :: "(nat option × bool list) ⇒ nat ⇒ bool" where "coin dc c = snd dc ! (c mod n)" definition "inversion dc = map (λc. (payer dc = Some c) ≠ (coin dc c ≠ coin dc (c + 1))) [0..<n]" definition "result dc = foldl (λ a b. a ≠ b) False (inversion dc)" lemma coin_n[simp]: "coin dc n = coin dc 0" unfolding coin_def by simp theorem correctness: assumes "dc ∈ dining_cryptographers" shows "result dc ⟷ (payer dc ≠ None)" proof - let ?XOR = "λf l. foldl (≠) False (map f [0..<l])" have foldl_coin: "¬ ?XOR (λc. coin dc c ≠ coin dc (c + 1)) n" proof - define n' where "n' = n" ― ‹Need to hide n, as it is hidden in coin› have "?XOR (λc. coin dc c ≠ coin dc (c + 1)) n' = (coin dc 0 ≠ coin dc n')" by (induct n') auto thus ?thesis using ‹n' ≡ n› by simp qed from assms have "payer dc = None ∨ (∃k<n. payer dc = Some k)" unfolding dining_cryptographers_def payer_def by auto thus ?thesis proof (rule disjE) assume "payer dc = None" thus ?thesis unfolding result_def inversion_def using foldl_coin by simp next assume "∃k<n. payer dc = Some k" then obtain k where "k < n" and "payer dc = Some k" by auto define l where "l = n" ― ‹Need to hide n, as it is hidden in coin, payer etc.› have "?XOR (λc. (payer dc = Some c) ≠ (coin dc c ≠ coin dc (c + 1))) l = ((k < l) ≠ ?XOR (λc. (coin dc c ≠ coin dc (c + 1))) l)" using ‹payer dc = Some k› by (induct l) auto thus ?thesis unfolding result_def inversion_def l_def using ‹payer dc = Some k› foldl_coin ‹k < n› by simp qed qed text ‹ We now restrict the state space for the dining cryptographers to the cases when one of the cryptographer pays. › definition "dc_crypto = dining_cryptographers - {None}×UNIV" lemma dc_crypto: "dc_crypto = Some ` {0..<n} × {xs :: bool list. length xs = n}" unfolding dc_crypto_def dining_cryptographers_def by auto lemma image_payer_dc_crypto: "payer ` dc_crypto = Some ` {0..<n}" proof - have *: "{xs. length xs = n} ≠ {}" by (auto intro!: exI[of _ "replicate n undefined"]) show ?thesis unfolding payer_def [abs_def] dc_crypto fst_image_times if_not_P[OF *] .. qed lemma card_payer_and_inversion: assumes "xs ∈ inversion ` dc_crypto" and "i < n" shows "card {dc ∈ dc_crypto. payer dc = Some i ∧ inversion dc = xs} = 2" (is "card ?S = 2") proof - obtain ys j where xs_inv: "inversion (Some j, ys) = xs" and "j < n" and "(Some j, ys) ∈ dc_crypto" using assms(1) by (auto simp: dc_crypto) hence "length ys = n" by (simp add: dc_crypto) have [simp]: "length xs = n" using xs_inv[symmetric] by (simp add: inversion_def) { fix b have "inj_on (λx. inversion (Some i, x)) {ys. ys ! 0 = b ∧ length ys = length xs}" proof (rule inj_onI) fix x y assume "x ∈ {ys. ys ! 0 = b ∧ length ys = length xs}" and "y ∈ {ys. ys ! 0 = b ∧ length ys = length xs}" and inv: "inversion (Some i, x) = inversion (Some i, y)" hence [simp]: "x ! 0 = y ! 0" "length y = n" "length x = n" using ‹length xs = n› by simp_all have *: "⋀j. j < n ⟹ (x ! j = x ! (Suc j mod n)) = (y ! j = y ! (Suc j mod n))" using inv unfolding inversion_def map_eq_conv payer_def coin_def by fastforce show "x = y" proof (rule nth_equalityI, simp, rule allI, rule impI) fix j assume "j < length x" hence "j < n" using ‹length xs = n› by simp thus "x ! j = y ! j" proof (induct j) case (Suc j) hence "j < n" by simp with Suc show ?case using *[OF ‹j < n›] by (cases "y ! j") simp_all qed simp qed qed } note inj_inv = this txt ‹ We now construct the possible inversions for @{term xs} when the payer is @{term i}. › define zs where "zs = map (λp. if p ∈ {min i j<..max i j} then ¬ ys ! p else ys ! p) [0..<n]" hence [simp]: "length zs = n" by simp hence [simp]: "0 < length zs" using n_gt_3 by simp have "⋀l. l < max i j ⟹ Suc l mod n = Suc l" using ‹i < n› ‹j < n› by auto { fix l assume "l < n" hence "(((l < min i j ∨ l = min i j) ∨ (min i j < l ∧ l < max i j)) ∨ l = max i j) ∨ max i j < l" by auto hence "((i = l) = (zs ! l = zs ! (Suc l mod n))) = ((j = l) = (ys ! l = ys ! (Suc l mod n)))" apply - proof ((erule disjE)+) assume "l < min i j" hence "l ≠ i" and "l ≠ j" and "zs ! l = ys ! l" and "zs ! (Suc l mod n) = ys ! (Suc l mod n)" using ‹i < n› ‹j < n› unfolding zs_def by auto thus ?thesis by simp next assume "l = min i j" show ?thesis proof (cases rule: linorder_cases) assume "i < j" hence "l = i" and "Suc l < n" and "i ≠ j" and "Suc l ≤ max i j" using ‹l = min i j› using ‹j < n› by auto hence "zs ! l = ys ! l" and "zs ! (Suc l mod n) = (¬ ys ! (Suc l mod n))" using ‹l = min i j›[symmetric] by (simp_all add: zs_def) thus ?thesis using ‹l = i› ‹i ≠ j› by simp next assume "j < i" hence "l = j" and "Suc l < n" and "i ≠ j" and "Suc l ≤ max i j" using ‹l = min i j› using ‹i < n› by auto hence "zs ! l = ys ! l" and "zs ! (Suc l mod n) = (¬ ys ! (Suc l mod n))" using ‹l = min i j›[symmetric] by (simp_all add: zs_def) thus ?thesis using ‹l = j› ‹i ≠ j› by simp next assume "i = j" hence "i = j" and "max i j = l" and "min i j = l" and "zs = ys" using ‹l = min i j› by (simp_all add: zs_def ‹length ys = n›[symmetric] map_nth) thus ?thesis by simp qed next assume "min i j < l ∧ l < max i j" hence "i ≠ l" and "j ≠ l" and "zs ! l = (¬ ys ! l)" "zs ! (Suc l mod n) = (¬ ys ! (Suc l mod n))" using ‹i < n› ‹j < n› by (auto simp: zs_def) thus ?thesis by simp next assume "l = max i j" show ?thesis proof (cases rule: linorder_cases) assume "i < j" hence "l = j" and "i ≠ j" using ‹l = max i j› using ‹j < n› by auto have "zs ! (Suc l mod n) = ys ! (Suc l mod n)" using ‹j < n› ‹i < j› ‹l = j› by (cases "Suc l = n") (auto simp add: zs_def) moreover have "zs ! l = (¬ ys ! l)" using ‹j < n› ‹i < j› by (auto simp add: ‹l = j› zs_def) ultimately show ?thesis using ‹l = j› ‹i ≠ j› by simp next assume "j < i" hence "l = i" and "i ≠ j" using ‹l = max i j› by auto have "zs ! (Suc l mod n) = ys ! (Suc l mod n)" using ‹i < n› ‹j < i› ‹l = i› by (cases "Suc l = n") (auto simp add: zs_def) moreover have "zs ! l = (¬ ys ! l)" using ‹i < n› ‹j < i› by (auto simp add: ‹l = i› zs_def) ultimately show ?thesis using ‹l = i› ‹i ≠ j› by auto next assume "i = j" hence "i = j" and "max i j = l" and "min i j = l" and "zs = ys" using ‹l = max i j› by (simp_all add: zs_def ‹length ys = n›[symmetric] map_nth) thus ?thesis by simp qed next assume "max i j < l" hence "j ≠ l" and "i ≠ l" by simp_all have "zs ! (Suc l mod n) = ys ! (Suc l mod n)" using ‹l < n› ‹max i j < l› by (cases "Suc l = n") (auto simp add: zs_def) moreover have "zs ! l = ys ! l" using ‹l < n› ‹max i j < l› by (auto simp add: zs_def) ultimately show ?thesis using ‹j ≠ l› ‹i ≠ l› by auto qed } hence zs: "inversion (Some i, zs) = xs" by (simp add: xs_inv[symmetric] inversion_def coin_def payer_def) moreover from zs have Not_zs: "inversion (Some i, (map Not zs)) = xs" by (simp add: xs_inv[symmetric] inversion_def coin_def payer_def) ultimately have "{dc ∈ dc_crypto. payer dc = Some i ∧ inversion dc = xs} = {(Some i, zs), (Some i, map Not zs)}" using ‹i < n› [[ hypsubst_thin = true ]] proof (safe, simp_all add:dc_crypto payer_def) fix b assume [simp]: "length b = n" and *: "inversion (Some i, b) = xs" and "b ≠ zs" show "b = map Not zs" proof (cases "b ! 0 = zs ! 0") case True hence zs: "zs ∈ {ys. ys ! 0 = b ! 0 ∧ length ys = length xs} ∧ xs = inversion (Some i, zs)" using zs by simp have b: "b ∈ {ys. ys ! 0 = b ! 0 ∧ length ys = length xs} ∧ xs = inversion (Some i, b)" using * by simp hence "b ∈ {ys. ys ! 0 = b ! 0 ∧ length ys = length xs}" .. with *[symmetric] have "xs ∈ (λx. inversion (Some i, x)) ` {ys. ys ! 0 = b ! 0 ∧ length ys = length xs}" by (rule image_eqI) from this[unfolded image_ex1_eq[OF inj_inv]] b zs have "b = zs" by (rule Ex1_eq) thus ?thesis using ‹b ≠ zs› by simp next case False hence zs: "map Not zs ∈ {ys. ys ! 0 = b ! 0 ∧ length ys = length xs} ∧ xs = inversion (Some i, map Not zs)" using Not_zs by (simp add: nth_map[OF ‹0 < length zs›]) have b: "b ∈ {ys. ys ! 0 = b ! 0 ∧ length ys = length xs} ∧ xs = inversion (Some i, b)" using * by simp hence "b ∈ {ys. ys ! 0 = b ! 0 ∧ length ys = length xs}" .. with *[symmetric] have "xs ∈ (λx. inversion (Some i, x)) ` {ys. ys ! 0 = b ! 0 ∧ length ys = length xs}" by (rule image_eqI) from this[unfolded image_ex1_eq[OF inj_inv]] b zs show "b = map Not zs" by (rule Ex1_eq) qed qed moreover have "zs ≠ map Not zs" using ‹0 < length zs› by (cases zs) simp_all ultimately show ?thesis by simp qed lemma finite_dc_crypto: "finite dc_crypto" using finite_lists_length_eq[where A="UNIV :: bool set"] unfolding dc_crypto by simp lemma card_inversion: assumes "xs ∈ inversion ` dc_crypto" shows "card {dc ∈ dc_crypto. inversion dc = xs} = 2 * n" proof - let ?set = "λi. {dc ∈ dc_crypto. payer dc = Some i ∧ inversion dc = xs}" let ?sets = "{?set i | i. i < n}" have [simp]: "length xs = n" using assms by (auto simp: dc_crypto inversion_def [abs_def]) have "{dc ∈ dc_crypto. inversion dc = xs} = (⋃i < n. ?set i)" unfolding dc_crypto payer_def by auto also have "… = (⋃?sets)" by auto finally have eq_Union: "{dc ∈ dc_crypto. inversion dc = xs} = (⋃?sets)" by simp have card_double: "2 * card ?sets = card (⋃?sets)" proof (rule card_partition) show "finite ?sets" by simp { fix i assume "i < n" have "?set i ⊆ dc_crypto" by auto have "finite (?set i)" using finite_dc_crypto by auto } thus "finite (⋃?sets)" by auto next fix c assume "c ∈ ?sets" thus "card c = 2" using card_payer_and_inversion[OF assms] by auto next fix x y assume "x ∈ ?sets" and "y ∈ ?sets" "x ≠ y" then obtain i j where xy: "x = ?set i" "y = ?set j" by auto hence "i ≠ j" using ‹x ≠ y› by auto thus "x ∩ y = {}" using xy by auto qed have sets: "?sets = ?set ` {..< n}" unfolding image_def by auto { fix i j :: nat assume asm: "i ≠ j" "i < n" "j < n" { assume iasm: "?set i = {}" have "card (?set i) = 2" using card_payer_and_inversion[OF assms ‹i < n›] by auto hence "False" using iasm by auto } then obtain c where ci: "c ∈ ?set i" by blast hence cj: "c ∉ ?set j" using asm by auto { assume "?set i = ?set j" hence "False" using ci cj by auto } hence "?set i ≠ ?set j" by auto } hence "inj_on ?set {..< n}" unfolding inj_on_def by auto from card_image[OF this] have "card (?set ` {..< n}) = n" by auto hence "card ?sets = n" using sets by auto thus ?thesis using eq_Union card_double by auto qed lemma card_dc_crypto: "card dc_crypto = n * 2^n" unfolding dc_crypto using card_lists_length_eq[of "UNIV :: bool set"] by (simp add: card_cartesian_product card_image) lemma card_image_inversion: "card (inversion ` dc_crypto) = 2^(n - 1)" proof - let ?P = "{inversion -` {x} ∩ dc_crypto |x. x ∈ inversion ` dc_crypto}" have "⋃?P = dc_crypto" by auto { fix a b assume *: "(a, b) ∈ dc_crypto" have inv_SOME: "inversion (SOME x. inversion x = inversion (a, b) ∧ x ∈ dc_crypto) = inversion (a, b)" apply (rule someI2) by (auto simp: *) } note inv_SOME = this { fix a b assume *: "(a, b) ∈ dc_crypto" have "(SOME x. inversion x = inversion (a, b) ∧ x ∈ dc_crypto) ∈ dc_crypto" by (rule someI2) (auto simp: *) } note SOME_inv_dc = this have "bij_betw (λs. inversion (SOME x. x ∈ s ∧ x ∈ dc_crypto)) {inversion -` {x} ∩ dc_crypto |x. x ∈ inversion ` dc_crypto} (inversion ` dc_crypto)" unfolding bij_betw_def by (auto intro!: inj_onI image_eqI simp: inv_SOME SOME_inv_dc) hence card_eq: "card {inversion -` {x} ∩ dc_crypto |x. x ∈ inversion ` dc_crypto} = card (inversion ` dc_crypto)" by (rule bij_betw_same_card) have "(2*n) * card (inversion ` dc_crypto) = card (⋃?P)" unfolding card_eq[symmetric] proof (rule card_partition) have "⋃?P ⊆ dc_crypto" by auto thus "finite (⋃?P)" using finite_dc_crypto by (auto intro: finite_subset) have "?P = (λx. inversion -` {x} ∩ dc_crypto) ` (inversion ` dc_crypto)" by auto thus "finite ?P" using finite_dc_crypto by auto next fix c assume "c ∈ {inversion -` {x} ∩ dc_crypto |x. x ∈ inversion ` dc_crypto}" then obtain x where "c = inversion -` {x} ∩ dc_crypto" and x: "x ∈ inversion ` dc_crypto" by auto hence "c = {dc ∈ dc_crypto. inversion dc = x}" by auto thus "card c = 2 * n" using card_inversion[OF x] by simp next fix x y assume "x ∈ ?P" "y ∈ ?P" and "x ≠ y" then obtain i j where x: "x = inversion -` {i} ∩ dc_crypto" and i: "i ∈ inversion ` dc_crypto" and y: "y = inversion -` {j} ∩ dc_crypto" and j: "j ∈ inversion ` dc_crypto" by auto show "x ∩ y = {}" using x y ‹x ≠ y› by auto qed hence "2 * card (inversion ` dc_crypto) = 2 ^ n" unfolding ‹⋃?P = dc_crypto› card_dc_crypto using n_gt_3 by auto thus ?thesis by (cases n) auto qed end sublocale dining_cryptographers_space ⊆ prob_space "uniform_count_measure dc_crypto" by (rule prob_space_uniform_count_measure[OF finite_dc_crypto]) (insert n_gt_3, auto simp: dc_crypto intro: exI[of _ "replicate n True"]) sublocale dining_cryptographers_space ⊆ information_space "uniform_count_measure dc_crypto" 2 by standard auto notation (in dining_cryptographers_space) mutual_information_Pow ("ℐ'( _ ; _ ')") notation (in dining_cryptographers_space) entropy_Pow ("ℋ'( _ ')") notation (in dining_cryptographers_space) conditional_entropy_Pow ("ℋ'( _ | _ ')") theorem (in dining_cryptographers_space) "ℐ( inversion ; payer ) = 0" proof (rule mutual_information_eq_0_simple) have n: "0 < n" using n_gt_3 by auto have card_image_inversion: "real (card (inversion ` dc_crypto)) = 2^n / 2" unfolding card_image_inversion using ‹0 < n› by (cases n) auto show inversion: "simple_distributed (uniform_count_measure dc_crypto) inversion (λx. 2 / 2^n)" proof (rule simple_distributedI) show "simple_function (uniform_count_measure dc_crypto) inversion" using finite_dc_crypto by (auto simp: simple_function_def space_uniform_count_measure sets_uniform_count_measure) fix x assume "x ∈ inversion ` space (uniform_count_measure dc_crypto)" moreover have "inversion -` {x} ∩ dc_crypto = {dc ∈ dc_crypto. inversion dc = x}" by auto ultimately show "2 / 2^n = prob (inversion -` {x} ∩ space (uniform_count_measure dc_crypto))" using ‹0 < n› by (simp add: card_inversion card_dc_crypto finite_dc_crypto subset_eq space_uniform_count_measure measure_uniform_count_measure) qed simp show "simple_distributed (uniform_count_measure dc_crypto) payer (λx. 1 / real n)" proof (rule simple_distributedI) show "simple_function (uniform_count_measure dc_crypto) payer" using finite_dc_crypto by (auto simp: simple_function_def space_uniform_count_measure sets_uniform_count_measure) fix z assume "z ∈ payer ` space (uniform_count_measure dc_crypto)" then have "payer -` {z} ∩ dc_crypto = {z} × {xs. length xs = n}" by (auto simp: dc_crypto payer_def space_uniform_count_measure) hence "card (payer -` {z} ∩ dc_crypto) = 2^n" using card_lists_length_eq[where A="UNIV::bool set"] by (simp add: card_cartesian_product_singleton) then show "1 / real n = prob (payer -` {z} ∩ space (uniform_count_measure dc_crypto))" using finite_dc_crypto by (subst measure_uniform_count_measure) (auto simp add: card_dc_crypto space_uniform_count_measure) qed simp show "simple_distributed (uniform_count_measure dc_crypto) (λx. (inversion x, payer x)) (λx. 2 / (real n *2^n))" proof (rule simple_distributedI) show "simple_function (uniform_count_measure dc_crypto) (λx. (inversion x, payer x))" using finite_dc_crypto by (auto simp: simple_function_def space_uniform_count_measure sets_uniform_count_measure) fix x assume "x ∈ (λx. (inversion x, payer x)) ` space (uniform_count_measure dc_crypto)" then obtain i xs where x: "x = (inversion (Some i, xs), payer (Some i, xs))" and "i < n" "length xs = n" by (simp add: image_iff space_uniform_count_measure dc_crypto Bex_def) blast then have xs: "inversion (Some i, xs) ∈ inversion`dc_crypto" and i: "Some i ∈ Some ` {0..<n}" and x: "x = (inversion (Some i, xs), Some i)" by (simp_all add: payer_def dc_crypto) moreover define ys where "ys = inversion (Some i, xs)" ultimately have ys: "ys ∈ inversion`dc_crypto" and "Some i ∈ Some ` {0..<n}" "x = (ys, Some i)" by simp_all then have "(λx. (inversion x, payer x)) -` {x} ∩ space (uniform_count_measure dc_crypto) = {dc ∈ dc_crypto. payer dc = Some (the (Some i)) ∧ inversion dc = ys}" by (auto simp add: payer_def space_uniform_count_measure) then show "2 / (real n * 2 ^ n) = prob ((λx. (inversion x, payer x)) -` {x} ∩ space (uniform_count_measure dc_crypto))" using ‹i < n› ys by (simp add: measure_uniform_count_measure card_payer_and_inversion finite_dc_crypto subset_eq card_dc_crypto) qed simp show "∀x∈space (uniform_count_measure dc_crypto). 2 / (real n * 2 ^ n) = 2 / 2 ^ n * (1 / real n) " by simp qed end