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