Rewrite the Probability theory.
Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.
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_Pow_additivity_sufficient, simp_all)
show "positive \<mu>" by (simp add: positive_def)
show "additive M \<mu>"
by (simp add: additive_def inverse_eq_divide field_simps Real_real
divide_le_0_iff zero_le_divide_iff
card_Un_disjoint finite_subset[OF _ finite])
qed
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