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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
     1
theory Dining_Cryptographers
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
     2
imports Information
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
     3
begin
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
     4
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36080
diff changeset
     5
lemma finite_information_spaceI:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
     6
  "\<lbrakk> finite_measure_space M \<mu> ; \<mu> (space M) = 1 ; 1 < b \<rbrakk> \<Longrightarrow> finite_information_space M \<mu> b"
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36080
diff changeset
     7
  unfolding finite_information_space_def finite_measure_space_def finite_measure_space_axioms_def
25153c08655e Cleanup information theory
hoelzl
parents: 36080
diff changeset
     8
    finite_prob_space_def prob_space_def prob_space_axioms_def finite_information_space_axioms_def
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
     9
  by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    10
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    11
locale finite_space =
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    12
  fixes S :: "'a set"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    13
  assumes finite[simp]: "finite S"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    14
  and not_empty[simp]: "S \<noteq> {}"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    15
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    16
definition (in finite_space) "M = \<lparr> space = S, sets = Pow S \<rparr>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    17
definition (in finite_space) \<mu>_def[simp]: "\<mu> A = (of_nat (card A) / of_nat (card S) :: pinfreal)"
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    18
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    19
lemma (in finite_space)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    20
  shows space_M[simp]: "space M = S"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    21
  and sets_M[simp]: "sets M = Pow S"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    22
  by (simp_all add: M_def)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    23
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    24
sublocale finite_space \<subseteq> finite_information_space M \<mu> 2
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36080
diff changeset
    25
proof (rule finite_information_spaceI)
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    26
  let ?measure = "\<lambda>s::'a set. real (card s) / real (card S)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    27
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    28
  show "finite_measure_space M \<mu>"
39099
5c714fd55b1e Updated proofs in Dining Cryptographers theory
hoelzl
parents: 38656
diff changeset
    29
  proof (rule finite_measure_spaceI)
5c714fd55b1e Updated proofs in Dining Cryptographers theory
hoelzl
parents: 38656
diff changeset
    30
    fix A B :: "'a set" assume "A \<inter> B = {}" "A \<subseteq> space M" "B \<subseteq> space M"
5c714fd55b1e Updated proofs in Dining Cryptographers theory
hoelzl
parents: 38656
diff changeset
    31
    then show "\<mu> (A \<union> B) = \<mu> A + \<mu> B"
5c714fd55b1e Updated proofs in Dining Cryptographers theory
hoelzl
parents: 38656
diff changeset
    32
      by (simp add: inverse_eq_divide field_simps Real_real
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    33
                    divide_le_0_iff zero_le_divide_iff
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
    34
                    card_Un_disjoint finite_subset[OF _ finite])
39099
5c714fd55b1e Updated proofs in Dining Cryptographers theory
hoelzl
parents: 38656
diff changeset
    35
  qed auto
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36080
diff changeset
    36
qed simp_all
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    37
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    38
lemma set_of_list_extend:
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    39
  "{xs. length xs = Suc n \<and> (\<forall>x\<in>set xs. x \<in> A)} =
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    40
  (\<lambda>(xs, n). n#xs) ` ({xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)} \<times> A)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    41
  (is "?lists (Suc n) = _")
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    42
proof
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    43
  show "(\<lambda>(xs, n). n#xs) ` (?lists n \<times> A) \<subseteq> ?lists (Suc n)" by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    44
  show "?lists (Suc n) \<subseteq> (\<lambda>(xs, n). n#xs) ` (?lists n \<times> A)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    45
  proof
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    46
    fix x assume "x \<in> ?lists (Suc n)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    47
    moreover
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    48
    hence "x \<noteq> []" by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    49
    then obtain t h where "x = h # t" by (cases x) auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    50
    ultimately show "x \<in> (\<lambda>(xs, n). n#xs) ` (?lists n \<times> A)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    51
      by (auto intro!: image_eqI[where x="(t, h)"])
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    52
  qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    53
qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    54
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    55
lemma card_finite_list_length:
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    56
  assumes "finite A"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    57
  shows "(card {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)} = (card A)^n) \<and>
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    58
         finite {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)}"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    59
    (is "card (?lists n) = _ \<and> _")
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    60
proof (induct n)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    61
  case 0 have "{xs. length xs = 0 \<and> (\<forall>x\<in>set xs. x \<in> A)} = {[]}" by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    62
  thus ?case by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    63
next
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    64
  case (Suc n)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    65
  moreover note set_of_list_extend[of n A]
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    66
  moreover have "inj_on (\<lambda>(xs, n). n#xs) (?lists n \<times> A)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    67
    by (auto intro!: inj_onI)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    68
  ultimately show ?case using assms by (auto simp: card_image)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    69
qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    70
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    71
lemma
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    72
  assumes "finite A"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    73
  shows finite_lists: "finite {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)}"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    74
  and card_list_length: "card {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)} = (card A)^n"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    75
  using card_finite_list_length[OF assms, of n] by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    76
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    77
section "Define the state space"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    78
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    79
text {*
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    80
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    81
We introduce the state space on which the algorithm operates.
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    82
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    83
This contains:
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    84
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    85
\begin{description}
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    86
\item[n]
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    87
  The number of cryptographers on the table.
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    88
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    89
\item[payer]
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    90
  Either one of the cryptographers or the NSA.
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    91
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    92
\item[coin]
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    93
  The result of the coin flipping for each cryptographer.
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    94
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    95
\item[inversion]
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    96
  The public result for each cryptographer, e.g. the sum of the coin flipping
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    97
  for the cryptographer, its right neighbour and the information if he paid or
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    98
  not.
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    99
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   100
\end{description}
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   101
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   102
The observables are the \emph{inversions}
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   103
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   104
*}
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   105
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   106
locale dining_cryptographers_space =
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   107
  fixes n :: nat
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   108
  assumes n_gt_3: "n \<ge> 3"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   109
begin
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   110
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   111
definition "dining_cryptographers =
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   112
  ({None} \<union> Some ` {0..<n}) \<times> {xs :: bool list. length xs = n}"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   113
definition "payer dc = fst dc"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   114
definition coin :: "(nat option \<times> bool list) => nat \<Rightarrow> bool" where
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   115
  "coin dc c = snd dc ! (c mod n)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   116
definition "inversion dc =
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   117
  map (\<lambda>c. (payer dc = Some c) \<noteq> (coin dc c \<noteq> coin dc (c + 1))) [0..<n]"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   118
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   119
definition "result dc = foldl (\<lambda> a b. a \<noteq> b) False (inversion dc)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   120
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   121
lemma coin_n[simp]: "coin dc n = coin dc 0"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   122
  unfolding coin_def by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   123
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   124
theorem correctness:
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   125
  assumes "dc \<in> dining_cryptographers"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   126
  shows "result dc \<longleftrightarrow> (payer dc \<noteq> None)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   127
proof -
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   128
  let "?XOR f l" = "foldl (op \<noteq>) False (map f [0..<l])"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   129
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   130
  have foldl_coin:
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   131
    "\<not> ?XOR (\<lambda>c. coin dc c \<noteq> coin dc (c + 1)) n"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   132
  proof -
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   133
    def n' \<equiv> n -- "Need to hide n, as it is hidden in coin"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   134
    have "?XOR (\<lambda>c. coin dc c \<noteq> coin dc (c + 1)) n'
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   135
        = (coin dc 0 \<noteq> coin dc n')"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   136
      by (induct n') auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   137
    thus ?thesis using `n' \<equiv> n` by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   138
  qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   139
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   140
  from assms have "payer dc = None \<or> (\<exists>k<n. payer dc = Some k)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   141
    unfolding dining_cryptographers_def payer_def by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   142
  thus ?thesis
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   143
  proof (rule disjE)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   144
    assume "payer dc = None"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   145
    thus ?thesis unfolding result_def inversion_def
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   146
      using foldl_coin by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   147
  next
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   148
    assume "\<exists>k<n. payer dc = Some k"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   149
    then obtain k where "k < n" and "payer dc = Some k" by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   150
    def l \<equiv> n -- "Need to hide n, as it is hidden in coin, payer etc."
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   151
    have "?XOR (\<lambda>c. (payer dc = Some c) \<noteq> (coin dc c \<noteq> coin dc (c + 1))) l =
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   152
        ((k < l) \<noteq> ?XOR (\<lambda>c. (coin dc c \<noteq> coin dc (c + 1))) l)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   153
      using `payer dc = Some k` by (induct l) auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   154
    thus ?thesis
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   155
      unfolding result_def inversion_def l_def
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   156
      using `payer dc = Some k` foldl_coin `k < n` by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   157
  qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   158
qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   159
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   160
text {*
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   161
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   162
We now restrict the state space for the dining cryptographers to the cases when
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   163
one of the cryptographer pays.
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   164
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   165
*}
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   166
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   167
definition
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   168
  "dc_crypto = dining_cryptographers - {None}\<times>UNIV"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   169
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   170
lemma dc_crypto: "dc_crypto = Some ` {0..<n} \<times> {xs :: bool list. length xs = n}"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   171
  unfolding dc_crypto_def dining_cryptographers_def by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   172
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   173
lemma image_payer_dc_crypto: "payer ` dc_crypto = Some ` {0..<n}"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   174
proof -
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   175
  have *: "{xs. length xs = n} \<noteq> {}"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   176
    by (auto intro!: exI[of _ "replicate n undefined"])
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   177
  show ?thesis
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36080
diff changeset
   178
    unfolding payer_def_raw dc_crypto fst_image_times if_not_P[OF *] ..
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   179
qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   180
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36080
diff changeset
   181
lemma image_ex1_eq: "inj_on f A \<Longrightarrow> (b \<in> f ` A) \<longleftrightarrow> (\<exists>!x \<in> A. b = f x)"
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   182
  by (unfold inj_on_def) blast
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   183
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   184
lemma Ex1_eq: "\<exists>! x. P x \<Longrightarrow> P x \<Longrightarrow> P y \<Longrightarrow> x = y"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   185
  by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   186
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   187
lemma card_payer_and_inversion:
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   188
  assumes "xs \<in> inversion ` dc_crypto" and "i < n"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   189
  shows "card {dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs} = 2"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   190
    (is "card ?S = 2")
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   191
proof -
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   192
  obtain ys j where xs_inv: "inversion (Some j, ys) = xs" and
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   193
    "j < n" and "(Some j, ys) \<in> dc_crypto"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   194
    using assms(1) by (auto simp: dc_crypto)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   195
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   196
  hence "length ys = n" by (simp add: dc_crypto)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   197
  have [simp]: "length xs = n" using xs_inv[symmetric] by (simp add: inversion_def)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   198
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   199
  { fix b
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   200
    have "inj_on (\<lambda>x. inversion (Some i, x)) {ys. ys ! 0 = b \<and> length ys = length xs}"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   201
    proof (rule inj_onI)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   202
      fix x y
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   203
      assume "x \<in> {ys. ys ! 0 = b \<and> length ys = length xs}"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   204
        and "y \<in> {ys. ys ! 0 = b \<and> length ys = length xs}"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   205
        and inv: "inversion (Some i, x) = inversion (Some i, y)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   206
      hence [simp]: "x ! 0 = y ! 0" "length y = n" "length x = n"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   207
        using `length xs = n` by simp_all
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   208
      have *: "\<And>j. j < n \<Longrightarrow>
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   209
        (x ! j = x ! (Suc j mod n)) = (y ! j = y ! (Suc j mod n))"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   210
        using inv unfolding inversion_def map_eq_conv payer_def coin_def
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   211
        by fastsimp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   212
      show "x = y"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   213
      proof (rule nth_equalityI, simp, rule allI, rule impI)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   214
        fix j assume "j < length x" hence "j < n" using `length xs = n` by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   215
        thus "x ! j = y ! j"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   216
        proof (induct j)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   217
          case (Suc j)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   218
          moreover hence "j < n" by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   219
          ultimately show ?case using *[OF `j < n`]
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   220
            by (cases "y ! j") simp_all
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   221
        qed simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   222
      qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   223
    qed }
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   224
  note inj_inv = this
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   225
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   226
  txt {*
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   227
    We now construct the possible inversions for @{term xs} when the payer is
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   228
    @{term i}.
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   229
  *}
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   230
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   231
  def zs \<equiv> "map (\<lambda>p. if p \<in> {min i j<..max i j} then \<not> ys ! p else ys ! p) [0..<n]"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   232
  hence [simp]: "length zs = n" by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   233
  hence [simp]: "0 < length zs" using n_gt_3 by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   234
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   235
  have "\<And>l. l < max i j \<Longrightarrow> Suc l mod n = Suc l"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   236
    using `i < n` `j < n` by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   237
  { fix l assume "l < n"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   238
    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
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   239
    hence "((i = l) = (zs ! l = zs ! (Suc l mod n))) = ((j = l) = (ys ! l = ys ! (Suc l mod n)))"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   240
    apply - proof ((erule disjE)+)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   241
      assume "l < min i j"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   242
      hence "l \<noteq> i" and "l \<noteq> j" and "zs ! l = ys ! l" and
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   243
        "zs ! (Suc l mod n) = ys ! (Suc l mod n)" using `i < n` `j < n` unfolding zs_def by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   244
      thus ?thesis by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   245
    next
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   246
      assume "l = min i j"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   247
      show ?thesis
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   248
      proof (cases rule: linorder_cases)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   249
        assume "i < j"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   250
        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
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   251
        hence "zs ! l = ys ! l" and "zs ! (Suc l mod n) = (\<not> ys ! (Suc l mod n))"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   252
          using `l = min i j`[symmetric] by (simp_all add: zs_def)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   253
        thus ?thesis using `l = i` `i \<noteq> j` by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   254
      next
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   255
        assume "j < i"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   256
        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
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   257
        hence "zs ! l = ys ! l" and "zs ! (Suc l mod n) = (\<not> ys ! (Suc l mod n))"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   258
          using `l = min i j`[symmetric] by (simp_all add: zs_def)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   259
        thus ?thesis using `l = j` `i \<noteq> j` by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   260
      next
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   261
        assume "i = j"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   262
        hence "i = j" and "max i j = l" and "min i j = l" and "zs = ys"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   263
          using `l = min i j` by (simp_all add: zs_def `length ys = n`[symmetric] map_nth)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   264
        thus ?thesis by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   265
      qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   266
    next
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   267
      assume "min i j < l \<and> l < max i j"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   268
      hence "i \<noteq> l" and "j \<noteq> l" and "zs ! l = (\<not> ys ! l)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   269
        "zs ! (Suc l mod n) = (\<not> ys ! (Suc l mod n))"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   270
        using `i < n` `j < n` by (auto simp: zs_def)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   271
      thus ?thesis by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   272
    next
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   273
      assume "l = max i j"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   274
      show ?thesis
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   275
      proof (cases rule: linorder_cases)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   276
        assume "i < j"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   277
        hence "l = j" and "i \<noteq> j" using `l = max i j` using `j < n` by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   278
        have "zs ! (Suc l mod n) = ys ! (Suc l mod n)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   279
          using `j < n` `i < j` `l = j` by (cases "Suc l = n") (auto simp add: zs_def)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   280
        moreover have "zs ! l = (\<not> ys ! l)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   281
          using `j < n` `i < j` by (auto simp add: `l = j` zs_def)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   282
        ultimately show ?thesis using `l = j` `i \<noteq> j` by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   283
      next
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   284
        assume "j < i"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   285
        hence "l = i" and "i \<noteq> j" using `l = max i j` by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   286
        have "zs ! (Suc l mod n) = ys ! (Suc l mod n)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   287
          using `i < n` `j < i` `l = i` by (cases "Suc l = n") (auto simp add: zs_def)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   288
        moreover have "zs ! l = (\<not> ys ! l)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   289
          using `i < n` `j < i` by (auto simp add: `l = i` zs_def)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   290
        ultimately show ?thesis using `l = i` `i \<noteq> j` by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   291
      next
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   292
        assume "i = j"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   293
        hence "i = j" and "max i j = l" and "min i j = l" and "zs = ys"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   294
          using `l = max i j` by (simp_all add: zs_def `length ys = n`[symmetric] map_nth)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   295
        thus ?thesis by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   296
      qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   297
    next
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   298
      assume "max i j < l"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   299
      hence "j \<noteq> l" and "i \<noteq> l" by simp_all
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   300
      have "zs ! (Suc l mod n) = ys ! (Suc l mod n)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   301
        using `l < n` `max i j < l` by (cases "Suc l = n") (auto simp add: zs_def)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   302
      moreover have "zs ! l = ys ! l"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   303
        using `l < n` `max i j < l` by (auto simp add: zs_def)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   304
      ultimately show ?thesis using `j \<noteq> l` `i \<noteq> l` by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   305
    qed }
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   306
  hence zs: "inversion (Some i, zs) = xs"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   307
    by (simp add: xs_inv[symmetric] inversion_def coin_def payer_def)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   308
  moreover
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   309
  hence Not_zs: "inversion (Some i, (map Not zs)) = xs"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   310
    by (simp add: xs_inv[symmetric] inversion_def coin_def payer_def)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   311
  ultimately
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   312
  have "{dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs} =
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   313
    {(Some i, zs), (Some i, map Not zs)}"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   314
    using `i < n`
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   315
  proof (safe, simp_all add:dc_crypto payer_def)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   316
    fix b assume [simp]: "length b = n"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   317
      and *: "inversion (Some i, b) = xs" and "b \<noteq> zs"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   318
    show "b = map Not zs"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   319
    proof (cases "b ! 0 = zs ! 0")
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   320
      case True
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   321
      hence zs: "zs \<in> {ys. ys ! 0 = b ! 0 \<and> length ys = length xs} \<and> xs = inversion (Some i, zs)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   322
        using zs by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   323
      have b: "b \<in> {ys. ys ! 0 = b ! 0 \<and> length ys = length xs} \<and> xs = inversion (Some i, b)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   324
        using * by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   325
      hence "b \<in> {ys. ys ! 0 = b ! 0 \<and> length ys = length xs}" ..
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   326
      with *[symmetric] have "xs \<in> (\<lambda>x. inversion (Some i, x)) ` {ys. ys ! 0 = b ! 0 \<and> length ys = length xs}"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   327
         by (rule image_eqI)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   328
      from this[unfolded image_ex1_eq[OF inj_inv]] b zs
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   329
      have "b = zs" by (rule Ex1_eq)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   330
      thus ?thesis using `b \<noteq> zs` by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   331
    next
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   332
      case False
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   333
      hence zs: "map Not zs \<in> {ys. ys ! 0 = b ! 0 \<and> length ys = length xs} \<and> xs = inversion (Some i, map Not zs)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   334
        using Not_zs by (simp add: nth_map[OF `0 < length zs`])
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   335
      have b: "b \<in> {ys. ys ! 0 = b ! 0 \<and> length ys = length xs} \<and> xs = inversion (Some i, b)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   336
        using * by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   337
      hence "b \<in> {ys. ys ! 0 = b ! 0 \<and> length ys = length xs}" ..
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   338
      with *[symmetric] have "xs \<in> (\<lambda>x. inversion (Some i, x)) ` {ys. ys ! 0 = b ! 0 \<and> length ys = length xs}"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   339
         by (rule image_eqI)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   340
      from this[unfolded image_ex1_eq[OF inj_inv]] b zs
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   341
      show "b = map Not zs" by (rule Ex1_eq)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   342
    qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   343
  qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   344
  moreover
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   345
  have "zs \<noteq> map Not zs"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   346
    using `0 < length zs` by (cases zs) simp_all
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   347
  ultimately show ?thesis by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   348
qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   349
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   350
lemma finite_dc_crypto: "finite dc_crypto"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   351
  using finite_lists[where A="UNIV :: bool set"]
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   352
  unfolding dc_crypto by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   353
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   354
lemma card_inversion:
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   355
  assumes "xs \<in> inversion ` dc_crypto"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   356
  shows "card {dc \<in> dc_crypto. inversion dc = xs} = 2 * n"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   357
proof -
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   358
  let "?set i" = "{dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs}"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   359
  let "?sets" = "{?set i | i. i < n}"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   360
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   361
  have [simp]: "length xs = n" using assms
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   362
    by (auto simp: dc_crypto inversion_def_raw)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   363
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   364
  have "{dc \<in> dc_crypto. inversion dc = xs} = (\<Union> i < n. ?set i)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   365
    unfolding dc_crypto payer_def by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   366
  also have "\<dots> = (\<Union> ?sets)" by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   367
  finally have eq_Union: "{dc \<in> dc_crypto. inversion dc = xs} = (\<Union> ?sets)" by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   368
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   369
  have card_double: "2 * card ?sets = card (\<Union> ?sets)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   370
  proof (rule card_partition)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   371
    show "finite ?sets" by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   372
    { fix i assume "i < n"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   373
      have "?set i \<subseteq> dc_crypto" by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   374
      have "finite (?set i)" using finite_dc_crypto by auto }
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   375
    thus "finite (\<Union>?sets)" by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   376
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   377
  next
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   378
    fix c assume "c \<in> ?sets"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   379
    thus "card c = 2" using card_payer_and_inversion[OF assms] by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   380
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   381
  next
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   382
    fix x y assume "x \<in> ?sets" and "y \<in> ?sets" "x \<noteq> y"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   383
    then obtain i j where xy: "x = ?set i" "y = ?set j" by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   384
    hence "i \<noteq> j" using `x \<noteq> y` by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   385
    thus "x \<inter> y = {}" using xy by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   386
  qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   387
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   388
  have sets: "?sets = ?set ` {..< n}"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   389
    unfolding image_def by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   390
  { fix i j :: nat assume asm: "i \<noteq> j" "i < n" "j < n"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   391
    { assume iasm: "?set i = {}"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   392
      have "card (?set i) = 2"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   393
        using card_payer_and_inversion[OF assms `i < n`] by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   394
      hence "False"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   395
        using iasm by auto }
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   396
    then obtain c where ci: "c \<in> ?set i" by blast
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   397
    hence cj: "c \<notin> ?set j" using asm by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   398
    { assume "?set i = ?set j"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   399
      hence "False" using ci cj by auto }
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   400
    hence "?set i \<noteq> ?set j" by auto }
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   401
  hence "inj_on ?set {..< n}" unfolding inj_on_def by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   402
  from card_image[OF this]
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   403
  have "card (?set ` {..< n}) = n" by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   404
  hence "card ?sets = n" using sets by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   405
  thus ?thesis using eq_Union card_double by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   406
qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   407
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   408
lemma card_dc_crypto:
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   409
  "card dc_crypto = n * 2^n"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   410
  unfolding dc_crypto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   411
  using card_list_length[of "UNIV :: bool set"]
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   412
  by (simp add: card_cartesian_product card_image)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   413
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   414
lemma card_image_inversion:
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   415
  "card (inversion ` dc_crypto) = 2^(n - 1)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   416
proof -
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   417
  let ?P = "{inversion -` {x} \<inter> dc_crypto |x. x \<in> inversion ` dc_crypto}"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   418
  have "\<Union>?P = dc_crypto" by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   419
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   420
  { fix a b assume *: "(a, b) \<in> dc_crypto"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   421
    have inv_SOME: "inversion (SOME x. inversion x = inversion (a, b) \<and> x \<in> dc_crypto) = inversion (a, b)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   422
      apply (rule someI2)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   423
      by (auto simp: *) }
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   424
  note inv_SOME = this
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   425
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   426
  { fix a b assume *: "(a, b) \<in> dc_crypto"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   427
    have "(SOME x. inversion x = inversion (a, b) \<and> x \<in> dc_crypto) \<in> dc_crypto"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   428
      by (rule someI2) (auto simp: *) }
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   429
  note SOME_inv_dc = this
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   430
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   431
  have "bij_betw (\<lambda>s. inversion (SOME x. x \<in> s \<and> x \<in> dc_crypto))
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   432
    {inversion -` {x} \<inter> dc_crypto |x. x \<in> inversion ` dc_crypto}
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   433
    (inversion ` dc_crypto)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   434
    unfolding bij_betw_def
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   435
    by (auto intro!: inj_onI image_eqI simp: inv_SOME SOME_inv_dc)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   436
  hence card_eq: "card {inversion -` {x} \<inter> dc_crypto |x. x \<in> inversion ` dc_crypto} = card (inversion ` dc_crypto)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   437
    by (rule bij_betw_same_card)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   438
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   439
  have "(2*n) * card (inversion ` dc_crypto) = card (\<Union>?P)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   440
    unfolding card_eq[symmetric]
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   441
  proof (rule card_partition)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   442
    have "\<Union>?P \<subseteq> dc_crypto" by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   443
    thus "finite (\<Union>?P)" using finite_dc_crypto by (auto intro: finite_subset)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   444
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   445
    have "?P = (\<lambda>x. inversion -` {x} \<inter> dc_crypto) ` (inversion ` dc_crypto)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   446
      by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   447
    thus "finite ?P" using finite_dc_crypto by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   448
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   449
  next
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   450
    fix c assume "c \<in> {inversion -` {x} \<inter> dc_crypto |x. x \<in> inversion ` dc_crypto}"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   451
    then obtain x where "c = inversion -` {x} \<inter> dc_crypto" and x: "x \<in> inversion ` dc_crypto" by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   452
    hence "c = {dc \<in> dc_crypto. inversion dc = x}" by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   453
    thus "card c = 2 * n" using card_inversion[OF x] by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   454
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   455
  next
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   456
    fix x y assume "x \<in> ?P" "y \<in> ?P" and "x \<noteq> y"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   457
    then obtain i j where
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   458
      x: "x = inversion -` {i} \<inter> dc_crypto" and i: "i \<in> inversion ` dc_crypto" and
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   459
      y: "y = inversion -` {j} \<inter> dc_crypto" and j: "j \<in> inversion ` dc_crypto" by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   460
    show "x \<inter> y = {}" using x y `x \<noteq> y` by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   461
  qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   462
  hence "2 * card (inversion ` dc_crypto) = 2 ^ n" unfolding `\<Union>?P = dc_crypto` card_dc_crypto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   463
    using n_gt_3 by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   464
  thus ?thesis by (cases n) auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   465
qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   466
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   467
end
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   468
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   469
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   470
sublocale
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   471
  dining_cryptographers_space \<subseteq> finite_space "dc_crypto"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   472
proof
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   473
  show "finite dc_crypto" using finite_dc_crypto .
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   474
  show "dc_crypto \<noteq> {}"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   475
    unfolding dc_crypto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   476
    using n_gt_3 by (auto intro: exI[of _ "replicate n True"])
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   477
qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   478
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   479
notation (in dining_cryptographers_space)
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36080
diff changeset
   480
  finite_mutual_information ("\<I>'( _ ; _ ')")
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   481
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   482
notation (in dining_cryptographers_space)
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36080
diff changeset
   483
  finite_entropy ("\<H>'( _ ')")
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   484
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   485
notation (in dining_cryptographers_space)
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36080
diff changeset
   486
  finite_conditional_entropy ("\<H>'( _ | _ ')")
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   487
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   488
theorem (in dining_cryptographers_space)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   489
  "\<I>( inversion ; payer ) = 0"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   490
proof -
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   491
  have n: "0 < n" using n_gt_3 by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   492
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36080
diff changeset
   493
  have lists: "{xs. length xs = n} \<noteq> {}" using Ex_list_of_length by auto
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   494
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   495
  have card_image_inversion:
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   496
    "real (card (inversion ` dc_crypto)) = 2^n / 2"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   497
    unfolding card_image_inversion using `0 < n` by (cases n) auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   498
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   499
  let ?dIP = "distribution (\<lambda>x. (inversion x, payer x))"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   500
  let ?dP = "distribution payer"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   501
  let ?dI = "distribution inversion"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   502
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   503
  { have "\<H>(inversion|payer) =
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   504
        - (\<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}))))"
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36080
diff changeset
   505
      unfolding conditional_entropy_eq
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   506
      by (simp add: image_payer_dc_crypto setsum_Sigma)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   507
    also have "... =
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   508
        - (\<Sum>x\<in>inversion`dc_crypto. (\<Sum>z\<in>Some ` {0..<n}. 2 / (real n * 2^n) * (1 - real n)))"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   509
      unfolding neg_equal_iff_equal
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   510
    proof (rule setsum_cong[OF refl], rule setsum_cong[OF refl])
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   511
      fix x z assume x: "x \<in> inversion`dc_crypto" and z: "z \<in> Some ` {0..<n}"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   512
      hence "(\<lambda>x. (inversion x, payer x)) -` {(x, z)} \<inter> dc_crypto =
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   513
          {dc \<in> dc_crypto. payer dc = Some (the z) \<and> inversion dc = x}"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   514
        by (auto simp add: payer_def)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   515
      moreover from x z obtain i where "z = Some i" and "i < n" by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   516
      moreover from x have "length x = n" by (auto simp: inversion_def_raw dc_crypto)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   517
      ultimately
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   518
      have "real (?dIP {(x, z)}) = 2 / (real n * 2^n)" using x
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   519
        by (simp add: distribution_def card_dc_crypto card_payer_and_inversion
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   520
                      inverse_eq_divide mult_le_0_iff zero_le_mult_iff power_le_zero_eq)
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   521
      moreover
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   522
      from z have "payer -` {z} \<inter> dc_crypto = {z} \<times> {xs. length xs = n}"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   523
        by (auto simp: dc_crypto payer_def)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   524
      hence "card (payer -` {z} \<inter> dc_crypto) = 2^n"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   525
        using card_list_length[where A="UNIV::bool set"]
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   526
        by (simp add: card_cartesian_product_singleton)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   527
      hence "real (?dP {z}) = 1 / real n"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   528
        by (simp add: distribution_def card_dc_crypto field_simps inverse_eq_divide
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   529
                      mult_le_0_iff zero_le_mult_iff power_le_zero_eq)
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   530
      ultimately
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   531
      show "real (?dIP {(x,z)}) * log 2 (real (?dIP {(x,z)}) / real (?dP {z})) =
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   532
       2 / (real n * 2^n) * (1 - real n)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   533
        by (simp add: field_simps log_divide log_nat_power[of 2])
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   534
    qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   535
    also have "... = real n - 1"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   536
      using n finite_space
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   537
      by (simp add: card_image_inversion card_image[OF inj_Some] field_simps real_eq_of_nat[symmetric])
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   538
    finally have "\<H>(inversion|payer) = real n - 1" . }
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   539
  moreover
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   540
  { have "\<H>(inversion) = - (\<Sum>x \<in> inversion`dc_crypto. real (?dI {x}) * log 2 (real (?dI {x})))"
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36080
diff changeset
   541
      unfolding entropy_eq by simp
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   542
    also have "... = - (\<Sum>x \<in> inversion`dc_crypto. 2 * (1 - real n) / 2^n)"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   543
      unfolding neg_equal_iff_equal
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   544
    proof (rule setsum_cong[OF refl])
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   545
      fix x assume x_inv: "x \<in> inversion ` dc_crypto"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   546
      hence "length x = n" by (auto simp: inversion_def_raw dc_crypto)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   547
      moreover have "inversion -` {x} \<inter> dc_crypto = {dc \<in> dc_crypto. inversion dc = x}" by auto
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   548
      ultimately have "?dI {x} = 2 / 2^n" using `0 < n`
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   549
        by (simp add: distribution_def card_inversion[OF x_inv] card_dc_crypto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   550
                      mult_le_0_iff zero_le_mult_iff power_le_zero_eq)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   551
      thus "real (?dI {x}) * log 2 (real (?dI {x})) = 2 * (1 - real n) / 2^n"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36624
diff changeset
   552
        by (simp add: log_divide log_nat_power power_le_zero_eq inverse_eq_divide)
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   553
    qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   554
    also have "... = real n - 1"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   555
      by (simp add: card_image_inversion real_of_nat_def[symmetric] field_simps)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   556
    finally have "\<H>(inversion) = real n - 1" .
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   557
  }
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   558
  ultimately show ?thesis
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36080
diff changeset
   559
    unfolding mutual_information_eq_entropy_conditional_entropy
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   560
    by simp
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   561
qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   562
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   563
end