summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Probability/ex/Dining_Cryptographers.thy

author | hoelzl |

Thu, 02 Sep 2010 20:29:12 +0200 | |

changeset 39099 | 5c714fd55b1e |

parent 38656 | d5d342611edb |

child 40859 | de0b30e6c2d2 |

permissions | -rw-r--r-- |

Updated proofs in Dining Cryptographers theory

theory Dining_Cryptographers imports Information begin lemma finite_information_spaceI: "\<lbrakk> finite_measure_space M \<mu> ; \<mu> (space M) = 1 ; 1 < b \<rbrakk> \<Longrightarrow> finite_information_space M \<mu> b" unfolding finite_information_space_def finite_measure_space_def finite_measure_space_axioms_def finite_prob_space_def prob_space_def prob_space_axioms_def finite_information_space_axioms_def by auto locale finite_space = fixes S :: "'a set" assumes finite[simp]: "finite S" and not_empty[simp]: "S \<noteq> {}" definition (in finite_space) "M = \<lparr> space = S, sets = Pow S \<rparr>" definition (in finite_space) \<mu>_def[simp]: "\<mu> A = (of_nat (card A) / of_nat (card S) :: pinfreal)" lemma (in finite_space) shows space_M[simp]: "space M = S" and sets_M[simp]: "sets M = Pow S" by (simp_all add: M_def) sublocale finite_space \<subseteq> finite_information_space M \<mu> 2 proof (rule finite_information_spaceI) let ?measure = "\<lambda>s::'a set. real (card s) / real (card S)" show "finite_measure_space M \<mu>" proof (rule finite_measure_spaceI) fix A B :: "'a set" assume "A \<inter> B = {}" "A \<subseteq> space M" "B \<subseteq> space M" then show "\<mu> (A \<union> B) = \<mu> A + \<mu> B" by (simp add: inverse_eq_divide field_simps Real_real divide_le_0_iff zero_le_divide_iff card_Un_disjoint finite_subset[OF _ finite]) qed auto qed simp_all lemma set_of_list_extend: "{xs. length xs = Suc n \<and> (\<forall>x\<in>set xs. x \<in> A)} = (\<lambda>(xs, n). n#xs) ` ({xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)} \<times> A)" (is "?lists (Suc n) = _") proof show "(\<lambda>(xs, n). n#xs) ` (?lists n \<times> A) \<subseteq> ?lists (Suc n)" by auto show "?lists (Suc n) \<subseteq> (\<lambda>(xs, n). n#xs) ` (?lists n \<times> A)" proof fix x assume "x \<in> ?lists (Suc n)" moreover hence "x \<noteq> []" by auto then obtain t h where "x = h # t" by (cases x) auto ultimately show "x \<in> (\<lambda>(xs, n). n#xs) ` (?lists n \<times> A)" by (auto intro!: image_eqI[where x="(t, h)"]) qed qed lemma card_finite_list_length: assumes "finite A" shows "(card {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)} = (card A)^n) \<and> finite {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)}" (is "card (?lists n) = _ \<and> _") proof (induct n) case 0 have "{xs. length xs = 0 \<and> (\<forall>x\<in>set xs. x \<in> A)} = {[]}" by auto thus ?case by simp next case (Suc n) moreover note set_of_list_extend[of n A] moreover have "inj_on (\<lambda>(xs, n). n#xs) (?lists n \<times> A)" by (auto intro!: inj_onI) ultimately show ?case using assms by (auto simp: card_image) qed lemma assumes "finite A" shows finite_lists: "finite {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)}" and card_list_length: "card {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)} = (card A)^n" using card_finite_list_length[OF assms, of n] by auto section "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 \<ge> 3" begin definition "dining_cryptographers = ({None} \<union> Some ` {0..<n}) \<times> {xs :: bool list. length xs = n}" definition "payer dc = fst dc" definition coin :: "(nat option \<times> bool list) => nat \<Rightarrow> bool" where "coin dc c = snd dc ! (c mod n)" definition "inversion dc = map (\<lambda>c. (payer dc = Some c) \<noteq> (coin dc c \<noteq> coin dc (c + 1))) [0..<n]" definition "result dc = foldl (\<lambda> a b. a \<noteq> b) False (inversion dc)" lemma coin_n[simp]: "coin dc n = coin dc 0" unfolding coin_def by simp theorem correctness: assumes "dc \<in> dining_cryptographers" shows "result dc \<longleftrightarrow> (payer dc \<noteq> None)" proof - let "?XOR f l" = "foldl (op \<noteq>) False (map f [0..<l])" have foldl_coin: "\<not> ?XOR (\<lambda>c. coin dc c \<noteq> coin dc (c + 1)) n" proof - def n' \<equiv> n -- "Need to hide n, as it is hidden in coin" have "?XOR (\<lambda>c. coin dc c \<noteq> coin dc (c + 1)) n' = (coin dc 0 \<noteq> coin dc n')" by (induct n') auto thus ?thesis using `n' \<equiv> n` by simp qed from assms have "payer dc = None \<or> (\<exists>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 "\<exists>k<n. payer dc = Some k" then obtain k where "k < n" and "payer dc = Some k" by auto def l \<equiv> n -- "Need to hide n, as it is hidden in coin, payer etc." have "?XOR (\<lambda>c. (payer dc = Some c) \<noteq> (coin dc c \<noteq> coin dc (c + 1))) l = ((k < l) \<noteq> ?XOR (\<lambda>c. (coin dc c \<noteq> 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}\<times>UNIV" lemma dc_crypto: "dc_crypto = Some ` {0..<n} \<times> {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} \<noteq> {}" by (auto intro!: exI[of _ "replicate n undefined"]) show ?thesis unfolding payer_def_raw dc_crypto fst_image_times if_not_P[OF *] .. qed lemma image_ex1_eq: "inj_on f A \<Longrightarrow> (b \<in> f ` A) \<longleftrightarrow> (\<exists>!x \<in> A. b = f x)" by (unfold inj_on_def) blast lemma Ex1_eq: "\<exists>! x. P x \<Longrightarrow> P x \<Longrightarrow> P y \<Longrightarrow> x = y" by auto lemma card_payer_and_inversion: assumes "xs \<in> inversion ` dc_crypto" and "i < n" shows "card {dc \<in> dc_crypto. payer dc = Some i \<and> 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) \<in> 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 (\<lambda>x. inversion (Some i, x)) {ys. ys ! 0 = b \<and> length ys = length xs}" proof (rule inj_onI) fix x y assume "x \<in> {ys. ys ! 0 = b \<and> length ys = length xs}" and "y \<in> {ys. ys ! 0 = b \<and> 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 *: "\<And>j. j < n \<Longrightarrow> (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 fastsimp 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) moreover hence "j < n" by simp ultimately 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}. *} def zs \<equiv> "map (\<lambda>p. if p \<in> {min i j<..max i j} then \<not> 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 "\<And>l. l < max i j \<Longrightarrow> Suc l mod n = Suc l" using `i < n` `j < n` by auto { fix l assume "l < n" 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 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 \<noteq> i" and "l \<noteq> 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 \<noteq> j" and "Suc l \<le> max i j" using `l = min i j` using `j < n` by auto hence "zs ! l = ys ! l" and "zs ! (Suc l mod n) = (\<not> ys ! (Suc l mod n))" using `l = min i j`[symmetric] by (simp_all add: zs_def) thus ?thesis using `l = i` `i \<noteq> j` by simp next assume "j < i" hence "l = j" and "Suc l < n" and "i \<noteq> j" and "Suc l \<le> max i j" using `l = min i j` using `i < n` by auto hence "zs ! l = ys ! l" and "zs ! (Suc l mod n) = (\<not> ys ! (Suc l mod n))" using `l = min i j`[symmetric] by (simp_all add: zs_def) thus ?thesis using `l = j` `i \<noteq> 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 \<and> l < max i j" hence "i \<noteq> l" and "j \<noteq> l" and "zs ! l = (\<not> ys ! l)" "zs ! (Suc l mod n) = (\<not> 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 \<noteq> 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 = (\<not> ys ! l)" using `j < n` `i < j` by (auto simp add: `l = j` zs_def) ultimately show ?thesis using `l = j` `i \<noteq> j` by simp next assume "j < i" hence "l = i" and "i \<noteq> 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 = (\<not> ys ! l)" using `i < n` `j < i` by (auto simp add: `l = i` zs_def) ultimately show ?thesis using `l = i` `i \<noteq> 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 \<noteq> l" and "i \<noteq> 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 \<noteq> l` `i \<noteq> l` by auto qed } hence zs: "inversion (Some i, zs) = xs" by (simp add: xs_inv[symmetric] inversion_def coin_def payer_def) moreover hence Not_zs: "inversion (Some i, (map Not zs)) = xs" by (simp add: xs_inv[symmetric] inversion_def coin_def payer_def) ultimately have "{dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs} = {(Some i, zs), (Some i, map Not zs)}" using `i < n` proof (safe, simp_all add:dc_crypto payer_def) fix b assume [simp]: "length b = n" and *: "inversion (Some i, b) = xs" and "b \<noteq> zs" show "b = map Not zs" proof (cases "b ! 0 = zs ! 0") case True hence zs: "zs \<in> {ys. ys ! 0 = b ! 0 \<and> length ys = length xs} \<and> xs = inversion (Some i, zs)" using zs by simp have b: "b \<in> {ys. ys ! 0 = b ! 0 \<and> length ys = length xs} \<and> xs = inversion (Some i, b)" using * by simp hence "b \<in> {ys. ys ! 0 = b ! 0 \<and> length ys = length xs}" .. with *[symmetric] have "xs \<in> (\<lambda>x. inversion (Some i, x)) ` {ys. ys ! 0 = b ! 0 \<and> 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 \<noteq> zs` by simp next case False hence zs: "map Not zs \<in> {ys. ys ! 0 = b ! 0 \<and> length ys = length xs} \<and> xs = inversion (Some i, map Not zs)" using Not_zs by (simp add: nth_map[OF `0 < length zs`]) have b: "b \<in> {ys. ys ! 0 = b ! 0 \<and> length ys = length xs} \<and> xs = inversion (Some i, b)" using * by simp hence "b \<in> {ys. ys ! 0 = b ! 0 \<and> length ys = length xs}" .. with *[symmetric] have "xs \<in> (\<lambda>x. inversion (Some i, x)) ` {ys. ys ! 0 = b ! 0 \<and> 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 \<noteq> 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[where A="UNIV :: bool set"] unfolding dc_crypto by simp lemma card_inversion: assumes "xs \<in> inversion ` dc_crypto" shows "card {dc \<in> dc_crypto. inversion dc = xs} = 2 * n" proof - let "?set i" = "{dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs}" let "?sets" = "{?set i | i. i < n}" have [simp]: "length xs = n" using assms by (auto simp: dc_crypto inversion_def_raw) have "{dc \<in> dc_crypto. inversion dc = xs} = (\<Union> i < n. ?set i)" unfolding dc_crypto payer_def by auto also have "\<dots> = (\<Union> ?sets)" by auto finally have eq_Union: "{dc \<in> dc_crypto. inversion dc = xs} = (\<Union> ?sets)" by simp have card_double: "2 * card ?sets = card (\<Union> ?sets)" proof (rule card_partition) show "finite ?sets" by simp { fix i assume "i < n" have "?set i \<subseteq> dc_crypto" by auto have "finite (?set i)" using finite_dc_crypto by auto } thus "finite (\<Union>?sets)" by auto next fix c assume "c \<in> ?sets" thus "card c = 2" using card_payer_and_inversion[OF assms] by auto next fix x y assume "x \<in> ?sets" and "y \<in> ?sets" "x \<noteq> y" then obtain i j where xy: "x = ?set i" "y = ?set j" by auto hence "i \<noteq> j" using `x \<noteq> y` by auto thus "x \<inter> y = {}" using xy by auto qed have sets: "?sets = ?set ` {..< n}" unfolding image_def by auto { fix i j :: nat assume asm: "i \<noteq> 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 \<in> ?set i" by blast hence cj: "c \<notin> ?set j" using asm by auto { assume "?set i = ?set j" hence "False" using ci cj by auto } hence "?set i \<noteq> ?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_list_length[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} \<inter> dc_crypto |x. x \<in> inversion ` dc_crypto}" have "\<Union>?P = dc_crypto" by auto { fix a b assume *: "(a, b) \<in> dc_crypto" have inv_SOME: "inversion (SOME x. inversion x = inversion (a, b) \<and> x \<in> dc_crypto) = inversion (a, b)" apply (rule someI2) by (auto simp: *) } note inv_SOME = this { fix a b assume *: "(a, b) \<in> dc_crypto" have "(SOME x. inversion x = inversion (a, b) \<and> x \<in> dc_crypto) \<in> dc_crypto" by (rule someI2) (auto simp: *) } note SOME_inv_dc = this have "bij_betw (\<lambda>s. inversion (SOME x. x \<in> s \<and> x \<in> dc_crypto)) {inversion -` {x} \<inter> dc_crypto |x. x \<in> 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} \<inter> dc_crypto |x. x \<in> inversion ` dc_crypto} = card (inversion ` dc_crypto)" by (rule bij_betw_same_card) have "(2*n) * card (inversion ` dc_crypto) = card (\<Union>?P)" unfolding card_eq[symmetric] proof (rule card_partition) have "\<Union>?P \<subseteq> dc_crypto" by auto thus "finite (\<Union>?P)" using finite_dc_crypto by (auto intro: finite_subset) have "?P = (\<lambda>x. inversion -` {x} \<inter> dc_crypto) ` (inversion ` dc_crypto)" by auto thus "finite ?P" using finite_dc_crypto by auto next fix c assume "c \<in> {inversion -` {x} \<inter> dc_crypto |x. x \<in> inversion ` dc_crypto}" then obtain x where "c = inversion -` {x} \<inter> dc_crypto" and x: "x \<in> inversion ` dc_crypto" by auto hence "c = {dc \<in> 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 \<in> ?P" "y \<in> ?P" and "x \<noteq> y" then obtain i j where x: "x = inversion -` {i} \<inter> dc_crypto" and i: "i \<in> inversion ` dc_crypto" and y: "y = inversion -` {j} \<inter> dc_crypto" and j: "j \<in> inversion ` dc_crypto" by auto show "x \<inter> y = {}" using x y `x \<noteq> y` by auto qed hence "2 * card (inversion ` dc_crypto) = 2 ^ n" unfolding `\<Union>?P = dc_crypto` card_dc_crypto using n_gt_3 by auto thus ?thesis by (cases n) auto qed end sublocale dining_cryptographers_space \<subseteq> finite_space "dc_crypto" proof show "finite dc_crypto" using finite_dc_crypto . show "dc_crypto \<noteq> {}" unfolding dc_crypto using n_gt_3 by (auto intro: exI[of _ "replicate n True"]) qed notation (in dining_cryptographers_space) finite_mutual_information ("\<I>'( _ ; _ ')") notation (in dining_cryptographers_space) finite_entropy ("\<H>'( _ ')") notation (in dining_cryptographers_space) finite_conditional_entropy ("\<H>'( _ | _ ')") theorem (in dining_cryptographers_space) "\<I>( inversion ; payer ) = 0" proof - have n: "0 < n" using n_gt_3 by auto have lists: "{xs. length xs = n} \<noteq> {}" using Ex_list_of_length 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 let ?dIP = "distribution (\<lambda>x. (inversion x, payer x))" let ?dP = "distribution payer" let ?dI = "distribution inversion" { have "\<H>(inversion|payer) = - (\<Sum>x\<in>inversion`dc_crypto. (\<Sum>z\<in>Some ` {0..<n}. real (?dIP {(x, z)}) * log 2 (real (?dIP {(x, z)}) / real (?dP {z}))))" unfolding conditional_entropy_eq by (simp add: image_payer_dc_crypto setsum_Sigma) also have "... = - (\<Sum>x\<in>inversion`dc_crypto. (\<Sum>z\<in>Some ` {0..<n}. 2 / (real n * 2^n) * (1 - real n)))" unfolding neg_equal_iff_equal proof (rule setsum_cong[OF refl], rule setsum_cong[OF refl]) fix x z assume x: "x \<in> inversion`dc_crypto" and z: "z \<in> Some ` {0..<n}" hence "(\<lambda>x. (inversion x, payer x)) -` {(x, z)} \<inter> dc_crypto = {dc \<in> dc_crypto. payer dc = Some (the z) \<and> inversion dc = x}" by (auto simp add: payer_def) moreover from x z obtain i where "z = Some i" and "i < n" by auto moreover from x have "length x = n" by (auto simp: inversion_def_raw dc_crypto) ultimately have "real (?dIP {(x, z)}) = 2 / (real n * 2^n)" using x by (simp add: distribution_def card_dc_crypto card_payer_and_inversion inverse_eq_divide mult_le_0_iff zero_le_mult_iff power_le_zero_eq) moreover from z have "payer -` {z} \<inter> dc_crypto = {z} \<times> {xs. length xs = n}" by (auto simp: dc_crypto payer_def) hence "card (payer -` {z} \<inter> dc_crypto) = 2^n" using card_list_length[where A="UNIV::bool set"] by (simp add: card_cartesian_product_singleton) hence "real (?dP {z}) = 1 / real n" by (simp add: distribution_def card_dc_crypto field_simps inverse_eq_divide mult_le_0_iff zero_le_mult_iff power_le_zero_eq) ultimately show "real (?dIP {(x,z)}) * log 2 (real (?dIP {(x,z)}) / real (?dP {z})) = 2 / (real n * 2^n) * (1 - real n)" by (simp add: field_simps log_divide log_nat_power[of 2]) qed also have "... = real n - 1" using n finite_space by (simp add: card_image_inversion card_image[OF inj_Some] field_simps real_eq_of_nat[symmetric]) finally have "\<H>(inversion|payer) = real n - 1" . } moreover { have "\<H>(inversion) = - (\<Sum>x \<in> inversion`dc_crypto. real (?dI {x}) * log 2 (real (?dI {x})))" unfolding entropy_eq by simp also have "... = - (\<Sum>x \<in> inversion`dc_crypto. 2 * (1 - real n) / 2^n)" unfolding neg_equal_iff_equal proof (rule setsum_cong[OF refl]) fix x assume x_inv: "x \<in> inversion ` dc_crypto" hence "length x = n" by (auto simp: inversion_def_raw dc_crypto) moreover have "inversion -` {x} \<inter> dc_crypto = {dc \<in> dc_crypto. inversion dc = x}" by auto ultimately have "?dI {x} = 2 / 2^n" using `0 < n` by (simp add: distribution_def card_inversion[OF x_inv] card_dc_crypto mult_le_0_iff zero_le_mult_iff power_le_zero_eq) thus "real (?dI {x}) * log 2 (real (?dI {x})) = 2 * (1 - real n) / 2^n" by (simp add: log_divide log_nat_power power_le_zero_eq inverse_eq_divide) qed also have "... = real n - 1" by (simp add: card_image_inversion real_of_nat_def[symmetric] field_simps) finally have "\<H>(inversion) = real n - 1" . } ultimately show ?thesis unfolding mutual_information_eq_entropy_conditional_entropy by simp qed end