Quelle  Dining_Cryptographers.thy   Sprache: Isabelle

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..

  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
    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
    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.. {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..
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)

  have inj_inv: "inj_on (\x. inversion (Some i, x)) {ys. ys ! 0 = b \ length ys = length xs}"
    for b
  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)
      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

  txt ‹
    We now construct the possible inversions for 🍋‹xs› when the payer is
    🍋‹i›.
›

  define zs where "zs = map (\p. if p \ {min i j<..max i j} then \ ys ! p else ys ! p) [0..
  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
  have "((i = l) = (zs ! l = zs ! (Suc l mod n))) = ((j = l) = (ys ! l = ys ! (Suc l mod n)))"
    if "l < n" for l
  proof -
    from that consider "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 linarith
    thus ?thesis
    proof cases
      case 1
      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
      case 2
      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
      case 3
      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
      case 4
      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
      case 5
      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
  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
    have "finite (?set i)" for 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
  have "?set i \ ?set j" if asm: "i \ j" "i < n" "j < n" for i j
  proof -
    have False if iasm: "?set i = {}"
    proof -
      have "card (?set i) = 2"
        using card_payer_and_inversion[OF assms ‹i < n›] by auto
      thus ?thesis using iasm by auto
    qed
    then obtain c where ci: "c \ ?set i" by blast
    hence cj: "c \ ?set j" using asm by auto
    have False if "?set i = ?set j"
      using that ci cj by auto
    thus ?thesis by auto
  qed
  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

  have inv_SOME: "inversion (SOME x. inversion x = inversion (a, b) \ x \ dc_crypto) = inversion (a, b)"
    if "(a, b) \ dc_crypto" for a b
    by (rule someI2) (auto simp: that)

  have SOME_inv_dc: "(SOME x. inversion x = inversion (a, b) \ x \ dc_crypto) \ dc_crypto"
    if "(a, b) \ dc_crypto" for a b
    by (rule someI2) (auto simp: that)

  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 (‹I'( _ ; _ ')›)

notation (in dining_cryptographers_space)
  entropy_Pow (‹H'( _ ')›)

notation (in dining_cryptographers_space)
  conditional_entropy_Pow (‹H'( _ | _ ')›)

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 cong del: image_cong_simp)
    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..
      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.. "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