src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 41023 9118eb4eb8dc
child 41689 3e39b0e730d6
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
hoelzl@40859
     1
(* Author: Johannes Hoelzl, TU Muenchen *)
hoelzl@40859
     2
hoelzl@40859
     3
header {* Formalization of a Countermeasure by Koepf & Duermuth 2009 *}
hoelzl@40859
     4
hoelzl@40859
     5
theory Koepf_Duermuth_Countermeasure
wenzelm@41413
     6
  imports Information "~~/src/HOL/Library/Permutation"
hoelzl@40859
     7
begin
hoelzl@40859
     8
hoelzl@40859
     9
lemma
hoelzl@40859
    10
  fixes p u :: "'a \<Rightarrow> real"
hoelzl@40859
    11
  assumes "1 < b"
hoelzl@40859
    12
  assumes sum: "(\<Sum>i\<in>S. p i) = (\<Sum>i\<in>S. u i)"
hoelzl@40859
    13
  and pos: "\<And>i. i \<in> S \<Longrightarrow> 0 \<le> p i" "\<And>i. i \<in> S \<Longrightarrow> 0 \<le> u i"
hoelzl@40859
    14
  and cont: "\<And>i. i \<in> S \<Longrightarrow> 0 < p i \<Longrightarrow> 0 < u i"
hoelzl@40859
    15
  shows "(\<Sum>i\<in>S. p i * log b (u i)) \<le> (\<Sum>i\<in>S. p i * log b (p i))"
hoelzl@40859
    16
proof -
hoelzl@40859
    17
  have "(\<Sum>i\<in>S. p i * ln (u i) - p i * ln (p i)) \<le> (\<Sum>i\<in>S. u i - p i)"
hoelzl@40859
    18
  proof (intro setsum_mono)
hoelzl@40859
    19
    fix i assume [intro, simp]: "i \<in> S"
hoelzl@40859
    20
    show "p i * ln (u i) - p i * ln (p i) \<le> u i - p i"
hoelzl@40859
    21
    proof cases
hoelzl@40859
    22
      assume "p i = 0" with pos[of i] show ?thesis by simp
hoelzl@40859
    23
    next
hoelzl@40859
    24
      assume "p i \<noteq> 0"
hoelzl@40859
    25
      then have "0 < p i" "0 < u i" using pos[of i] cont[of i] by auto
hoelzl@40859
    26
      then have *: "0 < u i / p i" by (blast intro: divide_pos_pos cont)
hoelzl@40859
    27
      from `0 < p i` `0 < u i`
hoelzl@40859
    28
      have "p i * ln (u i) - p i * ln (p i) = p i * ln (u i / p i)"
hoelzl@40859
    29
        by (simp add: ln_div field_simps)
hoelzl@40859
    30
      also have "\<dots> \<le> p i * (u i / p i - 1)"
hoelzl@40859
    31
        using exp_ge_add_one_self[of "ln (u i / p i)"] pos[of i] exp_ln[OF *]
hoelzl@40859
    32
        by (auto intro!: mult_left_mono)
hoelzl@40859
    33
      also have "\<dots> = u i - p i"
hoelzl@40859
    34
        using `p i \<noteq> 0` by (simp add: field_simps)
hoelzl@40859
    35
      finally show ?thesis by simp
hoelzl@40859
    36
    qed
hoelzl@40859
    37
  qed
hoelzl@40859
    38
  also have "\<dots> = 0" using sum by (simp add: setsum_subtractf)
hoelzl@40859
    39
  finally show ?thesis using `1 < b` unfolding log_def setsum_subtractf
hoelzl@40859
    40
    by (auto intro!: divide_right_mono
hoelzl@40859
    41
             simp: times_divide_eq_right setsum_divide_distrib[symmetric])
hoelzl@40859
    42
qed
hoelzl@40859
    43
hoelzl@40859
    44
definition (in prob_space)
hoelzl@40859
    45
  "ordered_variable_partition X = (SOME f. bij_betw f {0..<card (X`space M)} (X`space M) \<and>
hoelzl@40859
    46
    (\<forall>i<card (X`space M). \<forall>j<card (X`space M). i \<le> j \<longrightarrow> distribution X {f i} \<le> distribution X {f j}))"
hoelzl@40859
    47
hoelzl@40859
    48
lemma ex_ordered_bij_betw_nat_finite:
hoelzl@40859
    49
  fixes order :: "nat \<Rightarrow> 'a\<Colon>linorder"
hoelzl@40859
    50
  assumes "finite S"
hoelzl@40859
    51
  shows "\<exists>f. bij_betw f {0..<card S} S \<and> (\<forall>i<card S. \<forall>j<card S. i \<le> j \<longrightarrow> order (f i) \<le> order (f j))"
hoelzl@40859
    52
proof -
hoelzl@40859
    53
  from ex_bij_betw_nat_finite [OF `finite S`] guess f .. note f = this
hoelzl@40859
    54
  let ?xs = "sort_key order (map f [0 ..< card S])"
hoelzl@40859
    55
hoelzl@40859
    56
  have "?xs <~~> map f [0 ..< card S]"
hoelzl@40859
    57
    unfolding multiset_of_eq_perm[symmetric] by (rule multiset_of_sort)
hoelzl@40859
    58
  from permutation_Ex_bij [OF this]
hoelzl@40859
    59
  obtain g where g: "bij_betw g {0..<card S} {0..<card S}" and
hoelzl@40859
    60
    map: "\<And>i. i<card S \<Longrightarrow> ?xs ! i = map f [0 ..< card S] ! g i"
hoelzl@40859
    61
    by (auto simp: atLeast0LessThan)
hoelzl@40859
    62
hoelzl@40859
    63
  { fix i assume "i < card S"
hoelzl@40859
    64
    then have "g i < card S" using g by (auto simp: bij_betw_def)
hoelzl@40859
    65
    with map [OF `i < card S`] have "f (g i) = ?xs ! i" by simp }
hoelzl@40859
    66
  note this[simp]
hoelzl@40859
    67
hoelzl@40859
    68
  show ?thesis
hoelzl@40859
    69
  proof (intro exI allI conjI impI)
hoelzl@40859
    70
    show "bij_betw (f\<circ>g) {0..<card S} S"
hoelzl@40859
    71
      using g f by (rule bij_betw_trans)
hoelzl@40859
    72
    fix i j assume [simp]: "i < card S" "j < card S" "i \<le> j"
hoelzl@40859
    73
    from sorted_nth_mono[of "map order ?xs" i j]
hoelzl@40859
    74
    show "order ((f\<circ>g) i) \<le> order ((f\<circ>g) j)" by simp
hoelzl@40859
    75
  qed
hoelzl@40859
    76
qed
hoelzl@40859
    77
hoelzl@40859
    78
lemma (in prob_space)
hoelzl@40859
    79
  assumes "finite (X`space M)"
hoelzl@40859
    80
  shows "bij_betw (ordered_variable_partition X) {0..<card (X`space M)} (X`space M)"
hoelzl@40859
    81
  and "\<And>i j. \<lbrakk> i < card (X`space M) ; j < card (X`space M) ; i \<le> j \<rbrakk> \<Longrightarrow>
hoelzl@40859
    82
    distribution X {ordered_variable_partition X i} \<le> distribution X {ordered_variable_partition X j}"
hoelzl@40859
    83
proof -
hoelzl@40859
    84
  
hoelzl@40859
    85
qed
hoelzl@40859
    86
hoelzl@40859
    87
definition (in prob_space)
hoelzl@40859
    88
  "order_distribution X i = real (distribution X {ordered_variable_partition X i})"
hoelzl@40859
    89
hoelzl@40859
    90
definition (in prob_space)
hoelzl@40859
    91
  "guessing_entropy b X = (\<Sum>i<card(X`space M). real i * log b (order_distribution X i))"
hoelzl@40859
    92
hoelzl@40859
    93
abbreviation (in finite_information_space)
hoelzl@40859
    94
  finite_guessing_entropy ("\<G>'(_')") where
hoelzl@40859
    95
  "\<G>(X) \<equiv> guessing_entropy b X"
hoelzl@40859
    96
hoelzl@40859
    97
hoelzl@40859
    98
hoelzl@40859
    99
lemma zero_notin_Suc_image[simp]: "0 \<notin> Suc ` A"
hoelzl@40859
   100
  by auto
hoelzl@40859
   101
hoelzl@40859
   102
definition extensional :: "'b \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) set" where
hoelzl@40859
   103
  "extensional d A = {f. \<forall>x. x \<notin> A \<longrightarrow> f x = d}"
hoelzl@40859
   104
hoelzl@40859
   105
lemma extensional_empty[simp]: "extensional d {} = {\<lambda>x. d}"
hoelzl@40859
   106
  unfolding extensional_def by (simp add: expand_set_eq expand_fun_eq)
hoelzl@40859
   107
hoelzl@40859
   108
lemma funset_eq_UN_fun_upd_I:
hoelzl@40859
   109
  assumes *: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f(a := d) \<in> F A"
hoelzl@40859
   110
  and **: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f a \<in> G (f(a:=d))"
hoelzl@40859
   111
  and ***: "\<And>f x. \<lbrakk> f \<in> F A ; x \<in> G f \<rbrakk> \<Longrightarrow> f(a:=x) \<in> F (insert a A)"
hoelzl@40859
   112
  shows "F (insert a A) = (\<Union>f\<in>F A. fun_upd f a ` (G f))"
hoelzl@40859
   113
proof safe
hoelzl@40859
   114
  fix f assume f: "f \<in> F (insert a A)"
hoelzl@40859
   115
  show "f \<in> (\<Union>f\<in>F A. fun_upd f a ` G f)"
hoelzl@40859
   116
  proof (rule UN_I[of "f(a := d)"])
hoelzl@40859
   117
    show "f(a := d) \<in> F A" using *[OF f] .
hoelzl@40859
   118
    show "f \<in> fun_upd (f(a:=d)) a ` G (f(a:=d))"
hoelzl@40859
   119
    proof (rule image_eqI[of _ _ "f a"])
hoelzl@40859
   120
      show "f a \<in> G (f(a := d))" using **[OF f] .
hoelzl@40859
   121
    qed simp
hoelzl@40859
   122
  qed
hoelzl@40859
   123
next
hoelzl@40859
   124
  fix f x assume "f \<in> F A" "x \<in> G f"
hoelzl@40859
   125
  from ***[OF this] show "f(a := x) \<in> F (insert a A)" .
hoelzl@40859
   126
qed
hoelzl@40859
   127
hoelzl@40859
   128
lemma extensional_insert[simp]:
hoelzl@40859
   129
  assumes "a \<notin> A"
hoelzl@40859
   130
  shows "extensional d (insert a A) \<inter> (insert a A \<rightarrow> B) = (\<Union>f \<in> extensional d A \<inter> (A \<rightarrow> B). (\<lambda>b. f(a := b)) ` B)"
hoelzl@40859
   131
  apply (rule funset_eq_UN_fun_upd_I)
hoelzl@40859
   132
  using assms
hoelzl@40859
   133
  by (auto intro!: inj_onI dest: inj_onD split: split_if_asm simp: extensional_def)
hoelzl@40859
   134
hoelzl@40859
   135
lemma finite_extensional_funcset[simp, intro]:
hoelzl@40859
   136
  assumes "finite A" "finite B"
hoelzl@40859
   137
  shows "finite (extensional d A \<inter> (A \<rightarrow> B))"
hoelzl@40859
   138
  using assms by induct auto
hoelzl@40859
   139
hoelzl@40859
   140
lemma fun_upd_eq_iff: "f(a := b) = g(a := b') \<longleftrightarrow> b = b' \<and> f(a := d) = g(a := d)"
hoelzl@40859
   141
  by (auto simp: expand_fun_eq)
hoelzl@40859
   142
hoelzl@40859
   143
lemma card_funcset:
hoelzl@40859
   144
  assumes "finite A" "finite B"
hoelzl@40859
   145
  shows "card (extensional d A \<inter> (A \<rightarrow> B)) = card B ^ card A"
hoelzl@40859
   146
using `finite A` proof induct
hoelzl@40859
   147
  case (insert a A) thus ?case unfolding extensional_insert[OF `a \<notin> A`]
hoelzl@40859
   148
  proof (subst card_UN_disjoint, safe, simp_all)
hoelzl@40859
   149
    show "finite (extensional d A \<inter> (A \<rightarrow> B))" "\<And>f. finite (fun_upd f a ` B)"
hoelzl@40859
   150
      using `finite B` `finite A` by simp_all
hoelzl@40859
   151
  next
hoelzl@40859
   152
    fix f g b b' assume "f \<noteq> g" and eq: "f(a := b) = g(a := b')" and
hoelzl@40859
   153
      ext: "f \<in> extensional d A" "g \<in> extensional d A"
hoelzl@40859
   154
    have "f a = d" "g a = d"
hoelzl@40859
   155
      using ext `a \<notin> A` by (auto simp add: extensional_def)
hoelzl@40859
   156
    with `f \<noteq> g` eq show False unfolding fun_upd_eq_iff[of _ _ b _ _ d]
hoelzl@40859
   157
      by (auto simp: fun_upd_idem fun_upd_eq_iff)
hoelzl@40859
   158
  next
hoelzl@40859
   159
    { fix f assume "f \<in> extensional d A \<inter> (A \<rightarrow> B)"
hoelzl@40859
   160
      have "card (fun_upd f a ` B) = card B"
hoelzl@40859
   161
      proof (auto intro!: card_image inj_onI)
hoelzl@40859
   162
        fix b b' assume "f(a := b) = f(a := b')"
hoelzl@40859
   163
        from fun_upd_eq_iff[THEN iffD1, OF this] show "b = b'" by simp
hoelzl@40859
   164
      qed }
hoelzl@40859
   165
    then show "(\<Sum>i\<in>extensional d A \<inter> (A \<rightarrow> B). card (fun_upd i a ` B)) = card B * card B ^ card A"
hoelzl@40859
   166
      using insert by simp
hoelzl@40859
   167
  qed
hoelzl@40859
   168
qed simp
hoelzl@40859
   169
hoelzl@40859
   170
lemma set_of_list_extend:
hoelzl@40859
   171
  "{xs. length xs = Suc n \<and> (\<forall>x\<in>set xs. x \<in> A)} =
hoelzl@40859
   172
    (\<lambda>(xs, n). n#xs) ` ({xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)} \<times> A)"
hoelzl@40859
   173
  by (auto simp: length_Suc_conv)
hoelzl@40859
   174
hoelzl@40859
   175
lemma
hoelzl@40859
   176
  assumes "finite A"
hoelzl@40859
   177
  shows finite_lists:
hoelzl@40859
   178
    "finite {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)}" (is "finite (?lists n)")
hoelzl@40859
   179
  and card_list_length:
hoelzl@40859
   180
    "card {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)} = (card A)^n"
hoelzl@40859
   181
proof -
hoelzl@40859
   182
  from `finite A`
hoelzl@40859
   183
  have "(card {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)} = (card A)^n) \<and>
hoelzl@40859
   184
         finite {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)}"
hoelzl@40859
   185
  proof (induct n)
hoelzl@40859
   186
    case (Suc n)
hoelzl@40859
   187
    moreover note set_of_list_extend[of n A]
hoelzl@40859
   188
    moreover have "inj_on (\<lambda>(xs, n). n#xs) (?lists n \<times> A)"
hoelzl@40859
   189
      by (auto intro!: inj_onI)
hoelzl@40859
   190
    ultimately show ?case using assms by (auto simp: card_image)
hoelzl@40859
   191
  qed (simp cong: conj_cong)
hoelzl@40859
   192
  then show "finite (?lists n)" "card (?lists n) = card A ^ n"
hoelzl@40859
   193
    by auto
hoelzl@40859
   194
qed
hoelzl@40859
   195
hoelzl@40859
   196
locale finite_information =
hoelzl@40859
   197
  fixes \<Omega> :: "'a set"
hoelzl@40859
   198
    and p :: "'a \<Rightarrow> real"
hoelzl@40859
   199
    and b :: real
hoelzl@40859
   200
  assumes finite_space[simp, intro]: "finite \<Omega>"
hoelzl@40859
   201
  and p_sums_1[simp]: "(\<Sum>\<omega>\<in>\<Omega>. p \<omega>) = 1"
hoelzl@40859
   202
  and positive_p[simp, intro]: "\<And>x. 0 \<le> p x"
hoelzl@40859
   203
  and b_gt_1[simp, intro]: "1 < b"
hoelzl@40859
   204
hoelzl@40859
   205
lemma (in finite_information) positive_p_sum[simp]: "0 \<le> setsum p X"
hoelzl@40859
   206
   by (auto intro!: setsum_nonneg)
hoelzl@40859
   207
hoelzl@40859
   208
sublocale finite_information \<subseteq> finite_information_space "\<lparr> space = \<Omega>, sets = Pow \<Omega> \<rparr>" "\<lambda>S. Real (setsum p S)" b
hoelzl@40859
   209
proof -
hoelzl@40859
   210
  show "finite_information_space \<lparr> space = \<Omega>, sets = Pow \<Omega> \<rparr> (\<lambda>S. Real (setsum p S)) b"
hoelzl@40859
   211
    unfolding finite_information_space_def finite_information_space_axioms_def
hoelzl@40859
   212
    unfolding finite_prob_space_def prob_space_def prob_space_axioms_def
hoelzl@40859
   213
    unfolding finite_measure_space_def finite_measure_space_axioms_def
hoelzl@40859
   214
    by (force intro!: sigma_algebra.finite_additivity_sufficient
hoelzl@40859
   215
              simp: additive_def sigma_algebra_Pow positive_def Real_eq_Real
hoelzl@40859
   216
                    setsum.union_disjoint finite_subset)
hoelzl@40859
   217
qed
hoelzl@40859
   218
hoelzl@40859
   219
lemma (in prob_space) prob_space_subalgebra:
hoelzl@40859
   220
  assumes "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
hoelzl@40859
   221
  shows "prob_space (M\<lparr> sets := N \<rparr>) \<mu>" sorry
hoelzl@40859
   222
hoelzl@40859
   223
lemma (in measure_space) measure_space_subalgebra:
hoelzl@40859
   224
  assumes "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
hoelzl@40859
   225
  shows "measure_space (M\<lparr> sets := N \<rparr>) \<mu>" sorry
hoelzl@40859
   226
hoelzl@40859
   227
locale koepf_duermuth = K: finite_information keys K b + M: finite_information messages M b
hoelzl@40859
   228
    for b :: real
hoelzl@40859
   229
    and keys :: "'key set" and K :: "'key \<Rightarrow> real"
hoelzl@40859
   230
    and messages :: "'message set" and M :: "'message \<Rightarrow> real" +
hoelzl@40859
   231
  fixes observe :: "'key \<Rightarrow> 'message \<Rightarrow> 'observation"
hoelzl@40859
   232
    and n :: nat
hoelzl@40859
   233
begin
hoelzl@40859
   234
hoelzl@40859
   235
definition msgs :: "('key \<times> 'message list) set" where
hoelzl@40859
   236
  "msgs = keys \<times> {ms. length ms = n \<and> (\<forall>M\<in>set ms. M \<in> messages)}"
hoelzl@40859
   237
hoelzl@40859
   238
definition P :: "('key \<times> 'message list) \<Rightarrow> real" where
hoelzl@40859
   239
  "P = (\<lambda>(k, ms). K k * (\<Prod>i<length ms. M (ms ! i)))"
hoelzl@40859
   240
hoelzl@40859
   241
end
hoelzl@40859
   242
hoelzl@40859
   243
sublocale koepf_duermuth \<subseteq> finite_information msgs P b
hoelzl@40859
   244
proof default
hoelzl@40859
   245
  show "finite msgs" unfolding msgs_def
hoelzl@40859
   246
    using finite_lists[OF M.finite_space, of n]
hoelzl@40859
   247
    by auto
hoelzl@40859
   248
hoelzl@40859
   249
  have [simp]: "\<And>A. inj_on (\<lambda>(xs, n). n # xs) A" by (force intro!: inj_onI)
hoelzl@40859
   250
hoelzl@40859
   251
  note setsum_right_distrib[symmetric, simp]
hoelzl@40859
   252
  note setsum_left_distrib[symmetric, simp]
hoelzl@40859
   253
  note setsum_cartesian_product'[simp]
hoelzl@40859
   254
hoelzl@40859
   255
  have "(\<Sum>ms | length ms = n \<and> (\<forall>M\<in>set ms. M \<in> messages). \<Prod>x<length ms. M (ms ! x)) = 1"
hoelzl@40859
   256
  proof (induct n)
hoelzl@40859
   257
    case 0 then show ?case by (simp cong: conj_cong)
hoelzl@40859
   258
  next
hoelzl@40859
   259
    case (Suc n)
hoelzl@40859
   260
    then show ?case
hoelzl@40859
   261
      by (simp add: comp_def set_of_list_extend
hoelzl@40859
   262
                    lessThan_eq_Suc_image setsum_reindex setprod_reindex)
hoelzl@40859
   263
  qed
hoelzl@40859
   264
  then show "setsum P msgs = 1"
hoelzl@40859
   265
    unfolding msgs_def P_def by simp
hoelzl@40859
   266
hoelzl@40859
   267
  fix x
hoelzl@40859
   268
  have "\<And> A f. 0 \<le> (\<Prod>x\<in>A. M (f x))" by (auto simp: setprod_nonneg)
hoelzl@40859
   269
  then show "0 \<le> P x"
hoelzl@40859
   270
    unfolding P_def by (auto split: prod.split simp: zero_le_mult_iff)
hoelzl@40859
   271
qed auto
hoelzl@40859
   272
hoelzl@40859
   273
lemma SIGMA_image_vimage:
hoelzl@40859
   274
  "snd ` (SIGMA x:f`X. f -` {x} \<inter> X) = X"
hoelzl@40859
   275
  by (auto simp: image_iff)
hoelzl@40859
   276
hoelzl@41023
   277
lemma zero_le_eq_True: "0 \<le> (x::pextreal) \<longleftrightarrow> True" by simp
hoelzl@40859
   278
hoelzl@40859
   279
lemma Real_setprod:
hoelzl@40859
   280
  assumes"\<And>i. i\<in>X \<Longrightarrow> 0 \<le> f i"
hoelzl@40859
   281
  shows "(\<Prod>i\<in>X. Real (f i)) = Real (\<Prod>i\<in>X. f i)"
hoelzl@40859
   282
proof cases
hoelzl@40859
   283
  assume "finite X"
hoelzl@40859
   284
  from this assms show ?thesis by induct (auto simp: mult_le_0_iff)
hoelzl@40859
   285
qed simp
hoelzl@40859
   286
hoelzl@40859
   287
lemma inj_Cons[simp]: "\<And>X. inj_on (\<lambda>(xs, x). x#xs) X" by (auto intro!: inj_onI)
hoelzl@40859
   288
hoelzl@40859
   289
lemma setprod_setsum_distrib_lists:
hoelzl@40859
   290
  fixes P and S :: "'a set" and f :: "'a \<Rightarrow> _::semiring_0" assumes "finite S"
hoelzl@40859
   291
  shows "(\<Sum>ms\<in>{ms. length ms = n \<and> set ms \<subseteq> S \<and> (\<forall>i<n. P i (ms!i))}. \<Prod>x<n. f (ms ! x)) =
hoelzl@40859
   292
         (\<Prod>i<n. \<Sum>m\<in>{m\<in>S. P i m}. f m)"
hoelzl@40859
   293
proof (induct n arbitrary: P)
hoelzl@40859
   294
  case 0 then show ?case by (simp cong: conj_cong)
hoelzl@40859
   295
next
hoelzl@40859
   296
  case (Suc n)
hoelzl@40859
   297
  have *: "{ms. length ms = Suc n \<and> set ms \<subseteq> S \<and> (\<forall>i<Suc n. P i (ms ! i))} =
hoelzl@40859
   298
    (\<lambda>(xs, x). x#xs) ` ({ms. length ms = n \<and> set ms \<subseteq> S \<and> (\<forall>i<n. P (Suc i) (ms ! i))} \<times> {m\<in>S. P 0 m})"
hoelzl@40859
   299
    apply (auto simp: image_iff length_Suc_conv)
hoelzl@40859
   300
    apply force+
hoelzl@40859
   301
    apply (case_tac i)
hoelzl@40859
   302
    by force+
hoelzl@40859
   303
  show ?case unfolding *
hoelzl@40859
   304
    using Suc[of "\<lambda>i. P (Suc i)"]
hoelzl@40859
   305
    by (simp add: setsum_reindex split_conv setsum_cartesian_product'
hoelzl@40859
   306
      lessThan_eq_Suc_image setprod_reindex setsum_left_distrib[symmetric] setsum_right_distrib[symmetric])
hoelzl@40859
   307
qed
hoelzl@40859
   308
hoelzl@40859
   309
context koepf_duermuth
hoelzl@40859
   310
begin
hoelzl@40859
   311
hoelzl@40859
   312
definition observations :: "'observation set" where
hoelzl@40859
   313
  "observations = (\<Union>f\<in>observe ` keys. f ` messages)"
hoelzl@40859
   314
hoelzl@40859
   315
lemma finite_observations[simp, intro]: "finite observations"
hoelzl@40859
   316
  unfolding observations_def by auto
hoelzl@40859
   317
hoelzl@40859
   318
definition OB :: "'key \<times> 'message list \<Rightarrow> 'observation list" where
hoelzl@40859
   319
  "OB = (\<lambda>(k, ms). map (observe k) ms)"
hoelzl@40859
   320
hoelzl@40859
   321
definition t :: "'observation list \<Rightarrow> 'observation \<Rightarrow> nat" where
hoelzl@40859
   322
  "t seq obs = length (filter (op = obs) seq)"
hoelzl@40859
   323
hoelzl@40859
   324
lemma card_T_bound: "card ((t\<circ>OB)`msgs) \<le> (n+1)^card observations"
hoelzl@40859
   325
proof -
hoelzl@40859
   326
  have "(t\<circ>OB)`msgs \<subseteq> extensional 0 observations \<inter> (observations \<rightarrow> {.. n})"
hoelzl@40859
   327
    unfolding observations_def extensional_def OB_def msgs_def
hoelzl@40859
   328
    by (auto simp add: t_def comp_def image_iff)
hoelzl@40859
   329
  with finite_extensional_funcset
hoelzl@40859
   330
  have "card ((t\<circ>OB)`msgs) \<le> card (extensional 0 observations \<inter> (observations \<rightarrow> {.. n}))"
hoelzl@40859
   331
    by (rule card_mono) auto
hoelzl@40859
   332
  also have "\<dots> = (n + 1) ^ card observations"
hoelzl@40859
   333
    by (subst card_funcset) auto
hoelzl@40859
   334
  finally show ?thesis .
hoelzl@40859
   335
qed
hoelzl@40859
   336
hoelzl@40859
   337
abbreviation
hoelzl@40859
   338
 "p A \<equiv> setsum P A"
hoelzl@40859
   339
hoelzl@40859
   340
abbreviation probability ("\<P>'(_') _") where
hoelzl@40859
   341
 "\<P>(X) x \<equiv> real (distribution X x)"
hoelzl@40859
   342
hoelzl@40859
   343
abbreviation joint_probability ("\<P>'(_, _') _") where
hoelzl@40859
   344
 "\<P>(X, Y) x \<equiv> real (joint_distribution X Y x)"
hoelzl@40859
   345
hoelzl@40859
   346
abbreviation conditional_probability ("\<P>'(_|_') _") where
hoelzl@40859
   347
 "\<P>(X|Y) x \<equiv> \<P>(X, Y) x / \<P>(Y) (snd`x)"
hoelzl@40859
   348
hoelzl@40859
   349
notation
hoelzl@40859
   350
  finite_entropy ("\<H>'( _ ')")
hoelzl@40859
   351
hoelzl@40859
   352
notation
hoelzl@40859
   353
  finite_conditional_entropy ("\<H>'( _ | _ ')")
hoelzl@40859
   354
hoelzl@40859
   355
notation
hoelzl@40859
   356
  finite_mutual_information ("\<I>'( _ ; _ ')")
hoelzl@40859
   357
hoelzl@40859
   358
lemma t_eq_imp_bij_func:
hoelzl@40859
   359
  assumes "t xs = t ys"
hoelzl@40859
   360
  shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))"
hoelzl@40859
   361
proof -
hoelzl@40859
   362
  have "count (multiset_of xs) = count (multiset_of ys)"
hoelzl@40859
   363
    using assms by (simp add: expand_fun_eq count_multiset_of t_def)
hoelzl@40859
   364
  then have "xs <~~> ys" unfolding multiset_of_eq_perm count_inject .
hoelzl@40859
   365
  then show ?thesis by (rule permutation_Ex_func)
hoelzl@40859
   366
qed
hoelzl@40859
   367
hoelzl@40859
   368
lemma \<P>_k: assumes "k \<in> keys" shows "\<P>(fst) {k} = K k"
hoelzl@40859
   369
proof -
hoelzl@40859
   370
  from assms have *:
hoelzl@40859
   371
      "fst -` {k} \<inter> msgs = {k}\<times>{ms. length ms = n \<and> (\<forall>M\<in>set ms. M \<in> messages)}"
hoelzl@40859
   372
    unfolding msgs_def by auto
hoelzl@40859
   373
  show "\<P>(fst) {k} = K k" unfolding distribution_def
hoelzl@40859
   374
    apply (simp add: *) unfolding P_def
hoelzl@40859
   375
    apply (simp add: setsum_cartesian_product')
hoelzl@40859
   376
    using setprod_setsum_distrib_lists[OF M.finite_space, of M n "\<lambda>x x. True"]
hoelzl@40859
   377
    by (simp add: setsum_right_distrib[symmetric] subset_eq setprod_1)
hoelzl@40859
   378
qed
hoelzl@40859
   379
hoelzl@40859
   380
lemma fst_image_msgs[simp]: "fst`msgs = keys"
hoelzl@40859
   381
proof -
hoelzl@40859
   382
  from M.not_empty obtain m where "m \<in> messages" by auto
hoelzl@40859
   383
  then have *: "{m. length m = n \<and> (\<forall>x\<in>set m. x\<in>messages)} \<noteq> {}"
hoelzl@40859
   384
    by (auto intro!: exI[of _ "replicate n m"])
hoelzl@40859
   385
  then show ?thesis
hoelzl@40859
   386
    unfolding msgs_def fst_image_times if_not_P[OF *] by simp
hoelzl@40859
   387
qed
hoelzl@40859
   388
hoelzl@40859
   389
lemma ce_OB_eq_ce_t: "\<H>(fst | OB) = \<H>(fst | t\<circ>OB)"
hoelzl@40859
   390
proof -
hoelzl@40859
   391
  txt {* Lemma 2 *}
hoelzl@40859
   392
hoelzl@40859
   393
  { fix k obs obs'
hoelzl@40859
   394
    assume "k \<in> keys" "K k \<noteq> 0" and obs': "obs' \<in> OB ` msgs" and obs: "obs \<in> OB ` msgs"
hoelzl@40859
   395
    assume "t obs = t obs'"
hoelzl@40859
   396
    from t_eq_imp_bij_func[OF this]
hoelzl@40859
   397
    obtain t_f where "bij_betw t_f {..<n} {..<n}" and
hoelzl@40859
   398
      obs_t_f: "\<And>i. i<n \<Longrightarrow> obs!i = obs' ! t_f i"
hoelzl@40859
   399
      using obs obs' unfolding OB_def msgs_def by auto
hoelzl@40859
   400
    then have t_f: "inj_on t_f {..<n}" "{..<n} = t_f`{..<n}" unfolding bij_betw_def by auto
hoelzl@40859
   401
hoelzl@40859
   402
    { fix obs assume "obs \<in> OB`msgs"
hoelzl@40859
   403
      then have **: "\<And>ms. length ms = n \<Longrightarrow> OB (k, ms) = obs \<longleftrightarrow> (\<forall>i<n. observe k (ms!i) = obs ! i)"
hoelzl@40859
   404
        unfolding OB_def msgs_def by (simp add: image_iff list_eq_iff_nth_eq)
hoelzl@40859
   405
hoelzl@40859
   406
      have "\<P>(OB, fst) {(obs, k)} / K k =
hoelzl@40859
   407
          p ({k}\<times>{ms. (k,ms) \<in> msgs \<and> OB (k,ms) = obs}) / K k"
hoelzl@40859
   408
        unfolding distribution_def by (auto intro!: arg_cong[where f=p])
hoelzl@40859
   409
      also have "\<dots> =
hoelzl@40859
   410
          (\<Prod>i<n. \<Sum>m\<in>{m\<in>messages. observe k m = obs ! i}. M m)"
hoelzl@40859
   411
        unfolding P_def using `K k \<noteq> 0` `k \<in> keys`
hoelzl@40859
   412
        apply (simp add: setsum_cartesian_product' setsum_divide_distrib msgs_def ** cong: conj_cong)
hoelzl@40859
   413
        apply (subst setprod_setsum_distrib_lists[OF M.finite_space, unfolded subset_eq]) ..
hoelzl@40859
   414
      finally have "\<P>(OB, fst) {(obs, k)} / K k =
hoelzl@40859
   415
            (\<Prod>i<n. \<Sum>m\<in>{m\<in>messages. observe k m = obs ! i}. M m)" . }
hoelzl@40859
   416
    note * = this
hoelzl@40859
   417
hoelzl@40859
   418
    have "\<P>(OB, fst) {(obs, k)} / K k = \<P>(OB, fst) {(obs', k)} / K k"
hoelzl@40859
   419
      unfolding *[OF obs] *[OF obs']
hoelzl@40859
   420
      using t_f(1) obs_t_f by (subst (2) t_f(2)) (simp add: setprod_reindex)
hoelzl@40859
   421
    then have "\<P>(OB, fst) {(obs, k)} = \<P>(OB, fst) {(obs', k)}"
hoelzl@40859
   422
      using `K k \<noteq> 0` by auto }
hoelzl@40859
   423
  note t_eq_imp = this
hoelzl@40859
   424
hoelzl@40859
   425
  let "?S obs" = "t -`{t obs} \<inter> OB`msgs"
hoelzl@40859
   426
  { fix k obs assume "k \<in> keys" "K k \<noteq> 0" and obs: "obs \<in> OB`msgs"
hoelzl@40859
   427
    have *: "((\<lambda>x. (t (OB x), fst x)) -` {(t obs, k)} \<inter> msgs) =
hoelzl@40859
   428
      (\<Union>obs'\<in>?S obs. ((\<lambda>x. (OB x, fst x)) -` {(obs', k)} \<inter> msgs))" by auto
hoelzl@40859
   429
    have df: "disjoint_family_on (\<lambda>obs'. (\<lambda>x. (OB x, fst x)) -` {(obs', k)} \<inter> msgs) (?S obs)"
hoelzl@40859
   430
      unfolding disjoint_family_on_def by auto
hoelzl@40859
   431
    have "\<P>(t\<circ>OB, fst) {(t obs, k)} = (\<Sum>obs'\<in>?S obs. \<P>(OB, fst) {(obs', k)})"
hoelzl@40859
   432
      unfolding distribution_def comp_def
hoelzl@40859
   433
      using real_finite_measure_finite_Union[OF _ df]
hoelzl@40859
   434
      by (force simp add: * intro!: setsum_nonneg)
hoelzl@40859
   435
    also have "(\<Sum>obs'\<in>?S obs. \<P>(OB, fst) {(obs', k)}) = real (card (?S obs)) * \<P>(OB, fst) {(obs, k)}"
hoelzl@40859
   436
      by (simp add: t_eq_imp[OF `k \<in> keys` `K k \<noteq> 0` obs] real_eq_of_nat)
hoelzl@40859
   437
    finally have "\<P>(t\<circ>OB, fst) {(t obs, k)} = real (card (?S obs)) * \<P>(OB, fst) {(obs, k)}" .}
hoelzl@40859
   438
  note P_t_eq_P_OB = this
hoelzl@40859
   439
hoelzl@40859
   440
  { fix k obs assume "k \<in> keys" and obs: "obs \<in> OB`msgs"
hoelzl@40859
   441
    have "\<P>(t\<circ>OB | fst) {(t obs, k)} =
hoelzl@40859
   442
      real (card (t -` {t obs} \<inter> OB ` msgs)) * \<P>(OB | fst) {(obs, k)}"
hoelzl@40859
   443
      using \<P>_k[OF `k \<in> keys`] P_t_eq_P_OB[OF `k \<in> keys` _ obs] by auto }
hoelzl@40859
   444
  note CP_t_K = this
hoelzl@40859
   445
hoelzl@40859
   446
  { fix k obs assume "k \<in> keys" and obs: "obs \<in> OB`msgs"
hoelzl@40859
   447
    then have "t -`{t obs} \<inter> OB`msgs \<noteq> {}" (is "?S \<noteq> {}") by auto
hoelzl@40859
   448
    then have "real (card ?S) \<noteq> 0" by auto
hoelzl@40859
   449
hoelzl@40859
   450
    have "\<P>(fst | t\<circ>OB) {(k, t obs)} = \<P>(t\<circ>OB | fst) {(t obs, k)} * \<P>(fst) {k} / \<P>(t\<circ>OB) {t obs}"
hoelzl@40859
   451
      using real_distribution_order'[of fst k "t\<circ>OB" "t obs"]
hoelzl@40859
   452
      by (subst joint_distribution_commute) auto
hoelzl@40859
   453
    also have "\<P>(t\<circ>OB) {t obs} = (\<Sum>k'\<in>keys. \<P>(t\<circ>OB|fst) {(t obs, k')} * \<P>(fst) {k'})"
hoelzl@40859
   454
      using setsum_real_distribution(2)[of "t\<circ>OB" fst "t obs", symmetric]
hoelzl@40859
   455
      using real_distribution_order'[of fst _ "t\<circ>OB" "t obs"] by (auto intro!: setsum_cong)
hoelzl@40859
   456
    also have "\<P>(t\<circ>OB | fst) {(t obs, k)} * \<P>(fst) {k} / (\<Sum>k'\<in>keys. \<P>(t\<circ>OB|fst) {(t obs, k')} * \<P>(fst) {k'}) =
hoelzl@40859
   457
      \<P>(OB | fst) {(obs, k)} * \<P>(fst) {k} / (\<Sum>k'\<in>keys. \<P>(OB|fst) {(obs, k')} * \<P>(fst) {k'})"
hoelzl@40859
   458
      using CP_t_K[OF `k\<in>keys` obs] CP_t_K[OF _ obs] `real (card ?S) \<noteq> 0`
hoelzl@40859
   459
      by (simp only: setsum_right_distrib[symmetric] ac_simps
hoelzl@40859
   460
          mult_divide_mult_cancel_left[OF `real (card ?S) \<noteq> 0`]
hoelzl@40859
   461
        cong: setsum_cong)
hoelzl@40859
   462
    also have "(\<Sum>k'\<in>keys. \<P>(OB|fst) {(obs, k')} * \<P>(fst) {k'}) = \<P>(OB) {obs}"
hoelzl@40859
   463
      using setsum_real_distribution(2)[of OB fst obs, symmetric]
hoelzl@40859
   464
      using real_distribution_order'[of fst _ OB obs] by (auto intro!: setsum_cong)
hoelzl@40859
   465
    also have "\<P>(OB | fst) {(obs, k)} * \<P>(fst) {k} / \<P>(OB) {obs} = \<P>(fst | OB) {(k, obs)}"
hoelzl@40859
   466
      using real_distribution_order'[of fst k OB obs]
hoelzl@40859
   467
      by (subst joint_distribution_commute) auto
hoelzl@40859
   468
    finally have "\<P>(fst | t\<circ>OB) {(k, t obs)} = \<P>(fst | OB) {(k, obs)}" . }
hoelzl@40859
   469
  note CP_T_eq_CP_O = this
hoelzl@40859
   470
hoelzl@40859
   471
  let "?H obs" = "(\<Sum>k\<in>keys. \<P>(fst|OB) {(k, obs)} * log b (\<P>(fst|OB) {(k, obs)})) :: real"
hoelzl@40859
   472
  let "?Ht obs" = "(\<Sum>k\<in>keys. \<P>(fst|t\<circ>OB) {(k, obs)} * log b (\<P>(fst|t\<circ>OB) {(k, obs)})) :: real"
hoelzl@40859
   473
hoelzl@40859
   474
  note [[simproc del: finite_information_space.mult_log]]
hoelzl@40859
   475
hoelzl@40859
   476
  { fix obs assume obs: "obs \<in> OB`msgs"
hoelzl@40859
   477
    have "?H obs = (\<Sum>k\<in>keys. \<P>(fst|t\<circ>OB) {(k, t obs)} * log b (\<P>(fst|t\<circ>OB) {(k, t obs)}))"
hoelzl@40859
   478
      using CP_T_eq_CP_O[OF _ obs]
hoelzl@40859
   479
      by simp
hoelzl@40859
   480
    then have "?H obs = ?Ht (t obs)" . }
hoelzl@40859
   481
  note * = this
hoelzl@40859
   482
hoelzl@40859
   483
  have **: "\<And>x f A. (\<Sum>y\<in>t-`{x}\<inter>A. f y (t y)) = (\<Sum>y\<in>t-`{x}\<inter>A. f y x)" by auto
hoelzl@40859
   484
hoelzl@40859
   485
  { fix x
hoelzl@40859
   486
    have *: "(\<lambda>x. t (OB x)) -` {t (OB x)} \<inter> msgs =
hoelzl@40859
   487
      (\<Union>obs\<in>?S (OB x). OB -` {obs} \<inter> msgs)" by auto
hoelzl@40859
   488
    have df: "disjoint_family_on (\<lambda>obs. OB -` {obs} \<inter> msgs) (?S (OB x))"
hoelzl@40859
   489
      unfolding disjoint_family_on_def by auto
hoelzl@40859
   490
    have "\<P>(t\<circ>OB) {t (OB x)} = (\<Sum>obs\<in>?S (OB x). \<P>(OB) {obs})"
hoelzl@40859
   491
      unfolding distribution_def comp_def
hoelzl@40859
   492
      using real_finite_measure_finite_Union[OF _ df]
hoelzl@40859
   493
      by (force simp add: * intro!: setsum_nonneg) }
hoelzl@40859
   494
  note P_t_sum_P_O = this
hoelzl@40859
   495
hoelzl@40859
   496
  txt {* Lemma 3 *}
hoelzl@40859
   497
  have "\<H>(fst | OB) = -(\<Sum>obs\<in>OB`msgs. \<P>(OB) {obs} * ?Ht (t obs))"
hoelzl@40859
   498
    unfolding conditional_entropy_eq_ce_with_hypothesis using * by simp
hoelzl@40859
   499
  also have "\<dots> = -(\<Sum>obs\<in>t`OB`msgs. \<P>(t\<circ>OB) {obs} * ?Ht obs)"
hoelzl@40859
   500
    apply (subst SIGMA_image_vimage[symmetric, of "OB`msgs" t])
hoelzl@40859
   501
    apply (subst setsum_reindex)
hoelzl@40859
   502
    apply (fastsimp intro!: inj_onI)
hoelzl@40859
   503
    apply simp
hoelzl@40859
   504
    apply (subst setsum_Sigma[symmetric, unfolded split_def])
hoelzl@40859
   505
    using finite_space apply fastsimp
hoelzl@40859
   506
    using finite_space apply fastsimp
hoelzl@40859
   507
    apply (safe intro!: setsum_cong)
hoelzl@40859
   508
    using P_t_sum_P_O
hoelzl@40859
   509
    by (simp add: setsum_divide_distrib[symmetric] field_simps **
hoelzl@40859
   510
                  setsum_right_distrib[symmetric] setsum_left_distrib[symmetric])
hoelzl@40859
   511
  also have "\<dots> = \<H>(fst | t\<circ>OB)"
hoelzl@40859
   512
    unfolding conditional_entropy_eq_ce_with_hypothesis
hoelzl@40859
   513
    by (simp add: comp_def image_image[symmetric])
hoelzl@40859
   514
  finally show ?thesis .
hoelzl@40859
   515
qed
hoelzl@40859
   516
hoelzl@40859
   517
theorem "\<I>(fst ; OB) \<le> real (card observations) * log b (real n + 1)"
hoelzl@40859
   518
proof -
hoelzl@40859
   519
  have "\<I>(fst ; OB) = \<H>(fst) - \<H>(fst | OB)"
hoelzl@40859
   520
    using mutual_information_eq_entropy_conditional_entropy .
hoelzl@40859
   521
  also have "\<dots> = \<H>(fst) - \<H>(fst | t\<circ>OB)"
hoelzl@40859
   522
    unfolding ce_OB_eq_ce_t ..
hoelzl@40859
   523
  also have "\<dots> = \<H>(t\<circ>OB) - \<H>(t\<circ>OB | fst)"
hoelzl@40859
   524
    unfolding entropy_chain_rule[symmetric] sign_simps
hoelzl@40859
   525
    by (subst entropy_commute) simp
hoelzl@40859
   526
  also have "\<dots> \<le> \<H>(t\<circ>OB)"
hoelzl@40859
   527
    using conditional_entropy_positive[of "t\<circ>OB" fst] by simp
hoelzl@40859
   528
  also have "\<dots> \<le> log b (real (card ((t\<circ>OB)`msgs)))"
hoelzl@40859
   529
    using entropy_le_card[of "t\<circ>OB"] by simp
hoelzl@40859
   530
  also have "\<dots> \<le> log b (real (n + 1)^card observations)"
hoelzl@40859
   531
    using card_T_bound not_empty
hoelzl@40859
   532
    by (auto intro!: log_le simp: card_gt_0_iff power_real_of_nat simp del: real_of_nat_power)
hoelzl@40859
   533
  also have "\<dots> = real (card observations) * log b (real n + 1)"
hoelzl@40859
   534
    by (simp add: log_nat_power real_of_nat_Suc)
hoelzl@40859
   535
  finally show ?thesis  .
hoelzl@40859
   536
qed
hoelzl@40859
   537
hoelzl@40859
   538
end
hoelzl@40859
   539
hoelzl@40859
   540
end