src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
author haftmann
Sun Oct 08 22:28:20 2017 +0200 (20 months ago)
changeset 66804 3f9bb52082c4
parent 66453 cc19f7ca2ed6
child 67399 eab6ce8368fa
permissions -rw-r--r--
avoid name clashes on interpretation of abstract locales
hoelzl@41689
     1
(* Author: Johannes Hölzl, TU München *)
hoelzl@40859
     2
wenzelm@61808
     3
section \<open>Formalization of a Countermeasure by Koepf \& Duermuth 2009\<close>
hoelzl@40859
     4
hoelzl@40859
     5
theory Koepf_Duermuth_Countermeasure
wenzelm@66453
     6
  imports "HOL-Probability.Information" "HOL-Library.Permutation"
hoelzl@40859
     7
begin
hoelzl@40859
     8
hoelzl@45715
     9
lemma SIGMA_image_vimage:
hoelzl@45715
    10
  "snd ` (SIGMA x:f`X. f -` {x} \<inter> X) = X"
hoelzl@45715
    11
  by (auto simp: image_iff)
hoelzl@40859
    12
hoelzl@45715
    13
declare inj_split_Cons[simp]
hoelzl@40859
    14
hoelzl@42256
    15
definition extensionalD :: "'b \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) set" where
hoelzl@42256
    16
  "extensionalD d A = {f. \<forall>x. x \<notin> A \<longrightarrow> f x = d}"
hoelzl@40859
    17
hoelzl@42256
    18
lemma extensionalD_empty[simp]: "extensionalD d {} = {\<lambda>x. d}"
hoelzl@42256
    19
  unfolding extensionalD_def by (simp add: set_eq_iff fun_eq_iff)
hoelzl@40859
    20
hoelzl@40859
    21
lemma funset_eq_UN_fun_upd_I:
hoelzl@40859
    22
  assumes *: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f(a := d) \<in> F A"
hoelzl@40859
    23
  and **: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f a \<in> G (f(a:=d))"
hoelzl@40859
    24
  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
    25
  shows "F (insert a A) = (\<Union>f\<in>F A. fun_upd f a ` (G f))"
hoelzl@40859
    26
proof safe
hoelzl@40859
    27
  fix f assume f: "f \<in> F (insert a A)"
hoelzl@40859
    28
  show "f \<in> (\<Union>f\<in>F A. fun_upd f a ` G f)"
hoelzl@40859
    29
  proof (rule UN_I[of "f(a := d)"])
hoelzl@40859
    30
    show "f(a := d) \<in> F A" using *[OF f] .
hoelzl@40859
    31
    show "f \<in> fun_upd (f(a:=d)) a ` G (f(a:=d))"
hoelzl@40859
    32
    proof (rule image_eqI[of _ _ "f a"])
hoelzl@40859
    33
      show "f a \<in> G (f(a := d))" using **[OF f] .
hoelzl@40859
    34
    qed simp
hoelzl@40859
    35
  qed
hoelzl@40859
    36
next
hoelzl@40859
    37
  fix f x assume "f \<in> F A" "x \<in> G f"
hoelzl@40859
    38
  from ***[OF this] show "f(a := x) \<in> F (insert a A)" .
hoelzl@40859
    39
qed
hoelzl@40859
    40
hoelzl@42256
    41
lemma extensionalD_insert[simp]:
hoelzl@40859
    42
  assumes "a \<notin> A"
hoelzl@42256
    43
  shows "extensionalD d (insert a A) \<inter> (insert a A \<rightarrow> B) = (\<Union>f \<in> extensionalD d A \<inter> (A \<rightarrow> B). (\<lambda>b. f(a := b)) ` B)"
hoelzl@40859
    44
  apply (rule funset_eq_UN_fun_upd_I)
hoelzl@40859
    45
  using assms
nipkow@62390
    46
  by (auto intro!: inj_onI dest: inj_onD split: if_split_asm simp: extensionalD_def)
hoelzl@40859
    47
hoelzl@42256
    48
lemma finite_extensionalD_funcset[simp, intro]:
hoelzl@40859
    49
  assumes "finite A" "finite B"
hoelzl@42256
    50
  shows "finite (extensionalD d A \<inter> (A \<rightarrow> B))"
hoelzl@40859
    51
  using assms by induct auto
hoelzl@40859
    52
hoelzl@40859
    53
lemma fun_upd_eq_iff: "f(a := b) = g(a := b') \<longleftrightarrow> b = b' \<and> f(a := d) = g(a := d)"
hoelzl@41689
    54
  by (auto simp: fun_eq_iff)
hoelzl@40859
    55
hoelzl@40859
    56
lemma card_funcset:
hoelzl@40859
    57
  assumes "finite A" "finite B"
hoelzl@42256
    58
  shows "card (extensionalD d A \<inter> (A \<rightarrow> B)) = card B ^ card A"
wenzelm@61808
    59
using \<open>finite A\<close> proof induct
wenzelm@61808
    60
  case (insert a A) thus ?case unfolding extensionalD_insert[OF \<open>a \<notin> A\<close>]
hoelzl@40859
    61
  proof (subst card_UN_disjoint, safe, simp_all)
hoelzl@42256
    62
    show "finite (extensionalD d A \<inter> (A \<rightarrow> B))" "\<And>f. finite (fun_upd f a ` B)"
wenzelm@61808
    63
      using \<open>finite B\<close> \<open>finite A\<close> by simp_all
hoelzl@40859
    64
  next
hoelzl@40859
    65
    fix f g b b' assume "f \<noteq> g" and eq: "f(a := b) = g(a := b')" and
hoelzl@42256
    66
      ext: "f \<in> extensionalD d A" "g \<in> extensionalD d A"
hoelzl@40859
    67
    have "f a = d" "g a = d"
wenzelm@61808
    68
      using ext \<open>a \<notin> A\<close> by (auto simp add: extensionalD_def)
wenzelm@61808
    69
    with \<open>f \<noteq> g\<close> eq show False unfolding fun_upd_eq_iff[of _ _ b _ _ d]
hoelzl@40859
    70
      by (auto simp: fun_upd_idem fun_upd_eq_iff)
hoelzl@40859
    71
  next
hoelzl@42256
    72
    { fix f assume "f \<in> extensionalD d A \<inter> (A \<rightarrow> B)"
hoelzl@40859
    73
      have "card (fun_upd f a ` B) = card B"
hoelzl@40859
    74
      proof (auto intro!: card_image inj_onI)
hoelzl@40859
    75
        fix b b' assume "f(a := b) = f(a := b')"
hoelzl@40859
    76
        from fun_upd_eq_iff[THEN iffD1, OF this] show "b = b'" by simp
hoelzl@40859
    77
      qed }
hoelzl@42256
    78
    then show "(\<Sum>i\<in>extensionalD d A \<inter> (A \<rightarrow> B). card (fun_upd i a ` B)) = card B * card B ^ card A"
hoelzl@40859
    79
      using insert by simp
hoelzl@40859
    80
  qed
hoelzl@40859
    81
qed simp
hoelzl@40859
    82
hoelzl@45715
    83
lemma zero_notin_Suc_image[simp]: "0 \<notin> Suc ` A"
hoelzl@45715
    84
  by auto
hoelzl@40859
    85
nipkow@64272
    86
lemma prod_sum_distrib_lists:
hoelzl@45715
    87
  fixes P and S :: "'a set" and f :: "'a \<Rightarrow> _::semiring_0" assumes "finite S"
hoelzl@45715
    88
  shows "(\<Sum>ms\<in>{ms. set ms \<subseteq> S \<and> length ms = n \<and> (\<forall>i<n. P i (ms!i))}. \<Prod>x<n. f (ms ! x)) =
hoelzl@45715
    89
         (\<Prod>i<n. \<Sum>m\<in>{m\<in>S. P i m}. f m)"
hoelzl@45715
    90
proof (induct n arbitrary: P)
hoelzl@45715
    91
  case 0 then show ?case by (simp cong: conj_cong)
hoelzl@45715
    92
next
hoelzl@45715
    93
  case (Suc n)
hoelzl@45715
    94
  have *: "{ms. set ms \<subseteq> S \<and> length ms = Suc n \<and> (\<forall>i<Suc n. P i (ms ! i))} =
hoelzl@45715
    95
    (\<lambda>(xs, x). x#xs) ` ({ms. set ms \<subseteq> S \<and> length ms = n \<and> (\<forall>i<n. P (Suc i) (ms ! i))} \<times> {m\<in>S. P 0 m})"
hoelzl@45715
    96
    apply (auto simp: image_iff length_Suc_conv)
hoelzl@45715
    97
    apply force+
hoelzl@45715
    98
    apply (case_tac i)
hoelzl@45715
    99
    by force+
hoelzl@45715
   100
  show ?case unfolding *
hoelzl@45715
   101
    using Suc[of "\<lambda>i. P (Suc i)"]
nipkow@64267
   102
    by (simp add: sum.reindex split_conv sum_cartesian_product'
nipkow@64272
   103
      lessThan_Suc_eq_insert_0 prod.reindex sum_distrib_right[symmetric] sum_distrib_left[symmetric])
hoelzl@45715
   104
qed
hoelzl@45715
   105
hoelzl@47694
   106
declare space_point_measure[simp]
hoelzl@45715
   107
hoelzl@47694
   108
declare sets_point_measure[simp]
hoelzl@45715
   109
hoelzl@47694
   110
lemma measure_point_measure:
hoelzl@47694
   111
  "finite \<Omega> \<Longrightarrow> A \<subseteq> \<Omega> \<Longrightarrow> (\<And>x. x \<in> \<Omega> \<Longrightarrow> 0 \<le> p x) \<Longrightarrow>
hoelzl@62977
   112
    measure (point_measure \<Omega> (\<lambda>x. ennreal (p x))) A = (\<Sum>i\<in>A. p i)"
hoelzl@62977
   113
  unfolding measure_def
nipkow@64267
   114
  by (subst emeasure_point_measure_finite) (auto simp: subset_eq sum_nonneg)
hoelzl@45715
   115
hoelzl@40859
   116
locale finite_information =
hoelzl@40859
   117
  fixes \<Omega> :: "'a set"
hoelzl@40859
   118
    and p :: "'a \<Rightarrow> real"
hoelzl@40859
   119
    and b :: real
hoelzl@40859
   120
  assumes finite_space[simp, intro]: "finite \<Omega>"
hoelzl@40859
   121
  and p_sums_1[simp]: "(\<Sum>\<omega>\<in>\<Omega>. p \<omega>) = 1"
hoelzl@40859
   122
  and positive_p[simp, intro]: "\<And>x. 0 \<le> p x"
hoelzl@40859
   123
  and b_gt_1[simp, intro]: "1 < b"
hoelzl@40859
   124
nipkow@64267
   125
lemma (in finite_information) positive_p_sum[simp]: "0 \<le> sum p X"
nipkow@64267
   126
   by (auto intro!: sum_nonneg)
hoelzl@40859
   127
hoelzl@47694
   128
sublocale finite_information \<subseteq> prob_space "point_measure \<Omega> p"
wenzelm@61169
   129
  by standard (simp add: one_ereal_def emeasure_point_measure_finite)
hoelzl@40859
   130
hoelzl@47694
   131
sublocale finite_information \<subseteq> information_space "point_measure \<Omega> p" b
wenzelm@61169
   132
  by standard simp
hoelzl@40859
   133
nipkow@64267
   134
lemma (in finite_information) \<mu>'_eq: "A \<subseteq> \<Omega> \<Longrightarrow> prob A = sum p A"
hoelzl@47694
   135
  by (auto simp: measure_point_measure)
hoelzl@40859
   136
hoelzl@40859
   137
locale koepf_duermuth = K: finite_information keys K b + M: finite_information messages M b
hoelzl@40859
   138
    for b :: real
hoelzl@40859
   139
    and keys :: "'key set" and K :: "'key \<Rightarrow> real"
hoelzl@40859
   140
    and messages :: "'message set" and M :: "'message \<Rightarrow> real" +
hoelzl@40859
   141
  fixes observe :: "'key \<Rightarrow> 'message \<Rightarrow> 'observation"
hoelzl@40859
   142
    and n :: nat
hoelzl@40859
   143
begin
hoelzl@40859
   144
hoelzl@40859
   145
definition msgs :: "('key \<times> 'message list) set" where
hoelzl@45715
   146
  "msgs = keys \<times> {ms. set ms \<subseteq> messages \<and> length ms = n}"
hoelzl@40859
   147
hoelzl@40859
   148
definition P :: "('key \<times> 'message list) \<Rightarrow> real" where
hoelzl@49793
   149
  "P = (\<lambda>(k, ms). K k * (\<Prod>i<n. M (ms ! i)))"
hoelzl@40859
   150
hoelzl@40859
   151
end
hoelzl@40859
   152
hoelzl@40859
   153
sublocale koepf_duermuth \<subseteq> finite_information msgs P b
wenzelm@61169
   154
proof
hoelzl@40859
   155
  show "finite msgs" unfolding msgs_def
hoelzl@45715
   156
    using finite_lists_length_eq[OF M.finite_space, of n]
hoelzl@40859
   157
    by auto
hoelzl@40859
   158
hoelzl@40859
   159
  have [simp]: "\<And>A. inj_on (\<lambda>(xs, n). n # xs) A" by (force intro!: inj_onI)
hoelzl@40859
   160
nipkow@64267
   161
  note sum_distrib_left[symmetric, simp]
nipkow@64267
   162
  note sum_distrib_right[symmetric, simp]
nipkow@64267
   163
  note sum_cartesian_product'[simp]
hoelzl@40859
   164
hoelzl@45715
   165
  have "(\<Sum>ms | set ms \<subseteq> messages \<and> length ms = n. \<Prod>x<length ms. M (ms ! x)) = 1"
hoelzl@40859
   166
  proof (induct n)
hoelzl@40859
   167
    case 0 then show ?case by (simp cong: conj_cong)
hoelzl@40859
   168
  next
hoelzl@40859
   169
    case (Suc n)
hoelzl@40859
   170
    then show ?case
hoelzl@45715
   171
      by (simp add: lists_length_Suc_eq lessThan_Suc_eq_insert_0
nipkow@64272
   172
                    sum.reindex prod.reindex)
hoelzl@40859
   173
  qed
nipkow@64267
   174
  then show "sum P msgs = 1"
hoelzl@40859
   175
    unfolding msgs_def P_def by simp
hoelzl@40859
   176
  fix x
nipkow@64272
   177
  have "\<And> A f. 0 \<le> (\<Prod>x\<in>A. M (f x))" by (auto simp: prod_nonneg)
hoelzl@40859
   178
  then show "0 \<le> P x"
hoelzl@40859
   179
    unfolding P_def by (auto split: prod.split simp: zero_le_mult_iff)
hoelzl@40859
   180
qed auto
hoelzl@40859
   181
hoelzl@40859
   182
context koepf_duermuth
hoelzl@40859
   183
begin
hoelzl@40859
   184
hoelzl@40859
   185
definition observations :: "'observation set" where
hoelzl@40859
   186
  "observations = (\<Union>f\<in>observe ` keys. f ` messages)"
hoelzl@40859
   187
hoelzl@40859
   188
lemma finite_observations[simp, intro]: "finite observations"
hoelzl@40859
   189
  unfolding observations_def by auto
hoelzl@40859
   190
hoelzl@40859
   191
definition OB :: "'key \<times> 'message list \<Rightarrow> 'observation list" where
hoelzl@40859
   192
  "OB = (\<lambda>(k, ms). map (observe k) ms)"
hoelzl@40859
   193
hoelzl@40859
   194
definition t :: "'observation list \<Rightarrow> 'observation \<Rightarrow> nat" where
hoelzl@49793
   195
  t_def2: "t seq obs = card { i. i < length seq \<and> seq ! i = obs}"
hoelzl@49793
   196
hoelzl@49793
   197
lemma t_def: "t seq obs = length (filter (op = obs) seq)"
hoelzl@49793
   198
  unfolding t_def2 length_filter_conv_card by (subst eq_commute) simp
hoelzl@40859
   199
hoelzl@40859
   200
lemma card_T_bound: "card ((t\<circ>OB)`msgs) \<le> (n+1)^card observations"
hoelzl@40859
   201
proof -
hoelzl@42256
   202
  have "(t\<circ>OB)`msgs \<subseteq> extensionalD 0 observations \<inter> (observations \<rightarrow> {.. n})"
hoelzl@42256
   203
    unfolding observations_def extensionalD_def OB_def msgs_def
hoelzl@45715
   204
    by (auto simp add: t_def comp_def image_iff subset_eq)
hoelzl@42256
   205
  with finite_extensionalD_funcset
hoelzl@42256
   206
  have "card ((t\<circ>OB)`msgs) \<le> card (extensionalD 0 observations \<inter> (observations \<rightarrow> {.. n}))"
hoelzl@40859
   207
    by (rule card_mono) auto
hoelzl@40859
   208
  also have "\<dots> = (n + 1) ^ card observations"
hoelzl@40859
   209
    by (subst card_funcset) auto
hoelzl@40859
   210
  finally show ?thesis .
hoelzl@40859
   211
qed
hoelzl@40859
   212
hoelzl@40859
   213
abbreviation
nipkow@64267
   214
 "p A \<equiv> sum P A"
hoelzl@40859
   215
hoelzl@47694
   216
abbreviation
hoelzl@47694
   217
  "\<mu> \<equiv> point_measure msgs P"
hoelzl@47694
   218
hoelzl@40859
   219
abbreviation probability ("\<P>'(_') _") where
hoelzl@47694
   220
  "\<P>(X) x \<equiv> measure \<mu> (X -` x \<inter> msgs)"
hoelzl@40859
   221
hoelzl@47694
   222
abbreviation joint_probability ("\<P>'(_ ; _') _") where
hoelzl@47694
   223
  "\<P>(X ; Y) x \<equiv> \<P>(\<lambda>x. (X x, Y x)) x"
hoelzl@40859
   224
hoelzl@47694
   225
no_notation disj (infixr "|" 30)
hoelzl@47694
   226
hoelzl@47694
   227
abbreviation conditional_probability ("\<P>'(_ | _') _") where
hoelzl@47694
   228
  "\<P>(X | Y) x \<equiv> (\<P>(X ; Y) x) / \<P>(Y) (snd`x)"
hoelzl@40859
   229
hoelzl@40859
   230
notation
hoelzl@41689
   231
  entropy_Pow ("\<H>'( _ ')")
hoelzl@40859
   232
hoelzl@40859
   233
notation
hoelzl@41689
   234
  conditional_entropy_Pow ("\<H>'( _ | _ ')")
hoelzl@40859
   235
hoelzl@40859
   236
notation
hoelzl@41689
   237
  mutual_information_Pow ("\<I>'( _ ; _ ')")
hoelzl@40859
   238
hoelzl@40859
   239
lemma t_eq_imp_bij_func:
hoelzl@40859
   240
  assumes "t xs = t ys"
hoelzl@40859
   241
  shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))"
hoelzl@40859
   242
proof -
nipkow@60515
   243
  have "count (mset xs) = count (mset ys)"
nipkow@60515
   244
    using assms by (simp add: fun_eq_iff count_mset t_def)
nipkow@60515
   245
  then have "xs <~~> ys" unfolding mset_eq_perm count_inject .
hoelzl@41689
   246
  then show ?thesis by (rule permutation_Ex_bij)
hoelzl@40859
   247
qed
hoelzl@40859
   248
hoelzl@40859
   249
lemma \<P>_k: assumes "k \<in> keys" shows "\<P>(fst) {k} = K k"
hoelzl@40859
   250
proof -
hoelzl@40859
   251
  from assms have *:
hoelzl@45715
   252
      "fst -` {k} \<inter> msgs = {k}\<times>{ms. set ms \<subseteq> messages \<and> length ms = n}"
hoelzl@40859
   253
    unfolding msgs_def by auto
hoelzl@47694
   254
  show "(\<P>(fst) {k}) = K k"
hoelzl@47694
   255
    apply (simp add: \<mu>'_eq)
hoelzl@41981
   256
    apply (simp add: * P_def)
nipkow@64267
   257
    apply (simp add: sum_cartesian_product')
nipkow@64272
   258
    using prod_sum_distrib_lists[OF M.finite_space, of M n "\<lambda>x x. True"] \<open>k \<in> keys\<close>
nipkow@64272
   259
    by (auto simp add: sum_distrib_left[symmetric] subset_eq prod.neutral_const)
hoelzl@40859
   260
qed
hoelzl@40859
   261
hoelzl@40859
   262
lemma fst_image_msgs[simp]: "fst`msgs = keys"
hoelzl@40859
   263
proof -
hoelzl@40859
   264
  from M.not_empty obtain m where "m \<in> messages" by auto
hoelzl@45715
   265
  then have *: "{m. set m \<subseteq> messages \<and> length m = n} \<noteq> {}"
hoelzl@40859
   266
    by (auto intro!: exI[of _ "replicate n m"])
hoelzl@40859
   267
  then show ?thesis
hoelzl@40859
   268
    unfolding msgs_def fst_image_times if_not_P[OF *] by simp
hoelzl@40859
   269
qed
hoelzl@40859
   270
nipkow@64267
   271
lemma sum_distribution_cut:
hoelzl@47694
   272
  "\<P>(X) {x} = (\<Sum>y \<in> Y`space \<mu>. \<P>(X ; Y) {(x, y)})"
hoelzl@47694
   273
  by (subst finite_measure_finite_Union[symmetric])
hoelzl@47694
   274
     (auto simp add: disjoint_family_on_def inj_on_def
hoelzl@47694
   275
           intro!: arg_cong[where f=prob])
hoelzl@47694
   276
hoelzl@47694
   277
lemma prob_conj_imp1:
hoelzl@47694
   278
  "prob ({x. Q x} \<inter> msgs) = 0 \<Longrightarrow> prob ({x. Pr x \<and> Q x} \<inter> msgs) = 0"
hoelzl@47694
   279
  using finite_measure_mono[of "{x. Pr x \<and> Q x} \<inter> msgs" "{x. Q x} \<inter> msgs"]
hoelzl@47694
   280
  using measure_nonneg[of \<mu> "{x. Pr x \<and> Q x} \<inter> msgs"]
hoelzl@47694
   281
  by (simp add: subset_eq)
hoelzl@47694
   282
hoelzl@47694
   283
lemma prob_conj_imp2:
hoelzl@47694
   284
  "prob ({x. Pr x} \<inter> msgs) = 0 \<Longrightarrow> prob ({x. Pr x \<and> Q x} \<inter> msgs) = 0"
hoelzl@47694
   285
  using finite_measure_mono[of "{x. Pr x \<and> Q x} \<inter> msgs" "{x. Pr x} \<inter> msgs"]
hoelzl@47694
   286
  using measure_nonneg[of \<mu> "{x. Pr x \<and> Q x} \<inter> msgs"]
hoelzl@47694
   287
  by (simp add: subset_eq)
hoelzl@47694
   288
hoelzl@47694
   289
lemma simple_function_finite: "simple_function \<mu> f"
hoelzl@47694
   290
  by (simp add: simple_function_def)
hoelzl@47694
   291
hoelzl@47694
   292
lemma entropy_commute: "\<H>(\<lambda>x. (X x, Y x)) = \<H>(\<lambda>x. (Y x, X x))"
hoelzl@62977
   293
  apply (subst (1 2) entropy_simple_distributed[OF simple_distributedI[OF simple_function_finite _ refl]])
hoelzl@47694
   294
  unfolding space_point_measure
hoelzl@47694
   295
proof -
hoelzl@47694
   296
  have eq: "(\<lambda>x. (X x, Y x)) ` msgs = (\<lambda>(x, y). (y, x)) ` (\<lambda>x. (Y x, X x)) ` msgs"
hoelzl@47694
   297
    by auto
hoelzl@47694
   298
  show "- (\<Sum>x\<in>(\<lambda>x. (X x, Y x)) ` msgs. (\<P>(X ; Y) {x}) * log b (\<P>(X ; Y) {x})) =
hoelzl@47694
   299
    - (\<Sum>x\<in>(\<lambda>x. (Y x, X x)) ` msgs. (\<P>(Y ; X) {x}) * log b (\<P>(Y ; X) {x}))"
hoelzl@47694
   300
    unfolding eq
nipkow@64267
   301
    apply (subst sum.reindex)
nipkow@64267
   302
    apply (auto simp: vimage_def inj_on_def intro!: sum.cong arg_cong[where f="\<lambda>x. prob x * log b (prob x)"])
hoelzl@47694
   303
    done
hoelzl@62977
   304
qed simp_all
hoelzl@47694
   305
hoelzl@47694
   306
lemma (in -) measure_eq_0I: "A = {} \<Longrightarrow> measure M A = 0" by simp
hoelzl@47694
   307
hoelzl@47694
   308
lemma conditional_entropy_eq_ce_with_hypothesis:
hoelzl@47694
   309
  "\<H>(X | Y) = -(\<Sum>y\<in>Y`msgs. (\<P>(Y) {y}) * (\<Sum>x\<in>X`msgs. (\<P>(X ; Y) {(x,y)}) / (\<P>(Y) {y}) *
hoelzl@47694
   310
     log b ((\<P>(X ; Y) {(x,y)}) / (\<P>(Y) {y}))))"
hoelzl@47694
   311
  apply (subst conditional_entropy_eq[OF
hoelzl@62977
   312
    simple_distributedI[OF simple_function_finite _ refl]
hoelzl@62977
   313
    simple_distributedI[OF simple_function_finite _ refl]])
hoelzl@47694
   314
  unfolding space_point_measure
hoelzl@47694
   315
proof -
hoelzl@47694
   316
  have "- (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` msgs. (\<P>(X ; Y) {(x, y)}) * log b ((\<P>(X ; Y) {(x, y)}) / (\<P>(Y) {y}))) =
hoelzl@47694
   317
    - (\<Sum>x\<in>X`msgs. (\<Sum>y\<in>Y`msgs. (\<P>(X ; Y) {(x, y)}) * log b ((\<P>(X ; Y) {(x, y)}) / (\<P>(Y) {y}))))"
nipkow@64267
   318
    unfolding sum.cartesian_product
nipkow@64267
   319
    apply (intro arg_cong[where f=uminus] sum.mono_neutral_left)
hoelzl@47694
   320
    apply (auto simp: vimage_def image_iff intro!: measure_eq_0I)
hoelzl@47694
   321
    apply metis
hoelzl@47694
   322
    done
hoelzl@47694
   323
  also have "\<dots> = - (\<Sum>y\<in>Y`msgs. (\<Sum>x\<in>X`msgs. (\<P>(X ; Y) {(x, y)}) * log b ((\<P>(X ; Y) {(x, y)}) / (\<P>(Y) {y}))))"
haftmann@66804
   324
    by (subst sum.swap) rule
hoelzl@47694
   325
  also have "\<dots> = -(\<Sum>y\<in>Y`msgs. (\<P>(Y) {y}) * (\<Sum>x\<in>X`msgs. (\<P>(X ; Y) {(x,y)}) / (\<P>(Y) {y}) * log b ((\<P>(X ; Y) {(x,y)}) / (\<P>(Y) {y}))))"
nipkow@64267
   326
    by (auto simp add: sum_distrib_left vimage_def intro!: sum.cong prob_conj_imp1)
hoelzl@47694
   327
  finally show "- (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` msgs. (\<P>(X ; Y) {(x, y)}) * log b ((\<P>(X ; Y) {(x, y)}) / (\<P>(Y) {y}))) =
hoelzl@47694
   328
    -(\<Sum>y\<in>Y`msgs. (\<P>(Y) {y}) * (\<Sum>x\<in>X`msgs. (\<P>(X ; Y) {(x,y)}) / (\<P>(Y) {y}) * log b ((\<P>(X ; Y) {(x,y)}) / (\<P>(Y) {y}))))" .
hoelzl@62977
   329
qed simp_all
hoelzl@47694
   330
hoelzl@49793
   331
lemma ce_OB_eq_ce_t: "\<I>(fst ; OB) = \<I>(fst ; t\<circ>OB)"
hoelzl@40859
   332
proof -
wenzelm@61808
   333
  txt \<open>Lemma 2\<close>
hoelzl@40859
   334
hoelzl@40859
   335
  { fix k obs obs'
hoelzl@40859
   336
    assume "k \<in> keys" "K k \<noteq> 0" and obs': "obs' \<in> OB ` msgs" and obs: "obs \<in> OB ` msgs"
hoelzl@40859
   337
    assume "t obs = t obs'"
hoelzl@40859
   338
    from t_eq_imp_bij_func[OF this]
hoelzl@40859
   339
    obtain t_f where "bij_betw t_f {..<n} {..<n}" and
hoelzl@40859
   340
      obs_t_f: "\<And>i. i<n \<Longrightarrow> obs!i = obs' ! t_f i"
hoelzl@40859
   341
      using obs obs' unfolding OB_def msgs_def by auto
hoelzl@40859
   342
    then have t_f: "inj_on t_f {..<n}" "{..<n} = t_f`{..<n}" unfolding bij_betw_def by auto
hoelzl@40859
   343
hoelzl@40859
   344
    { fix obs assume "obs \<in> OB`msgs"
hoelzl@40859
   345
      then have **: "\<And>ms. length ms = n \<Longrightarrow> OB (k, ms) = obs \<longleftrightarrow> (\<forall>i<n. observe k (ms!i) = obs ! i)"
hoelzl@40859
   346
        unfolding OB_def msgs_def by (simp add: image_iff list_eq_iff_nth_eq)
hoelzl@40859
   347
hoelzl@47694
   348
      have "(\<P>(OB ; fst) {(obs, k)}) / K k =
hoelzl@40859
   349
          p ({k}\<times>{ms. (k,ms) \<in> msgs \<and> OB (k,ms) = obs}) / K k"
hoelzl@47694
   350
        apply (simp add: \<mu>'_eq) by (auto intro!: arg_cong[where f=p])
hoelzl@40859
   351
      also have "\<dots> =
hoelzl@40859
   352
          (\<Prod>i<n. \<Sum>m\<in>{m\<in>messages. observe k m = obs ! i}. M m)"
wenzelm@61808
   353
        unfolding P_def using \<open>K k \<noteq> 0\<close> \<open>k \<in> keys\<close>
nipkow@64267
   354
        apply (simp add: sum_cartesian_product' sum_divide_distrib msgs_def ** cong: conj_cong)
nipkow@64272
   355
        apply (subst prod_sum_distrib_lists[OF M.finite_space]) ..
hoelzl@47694
   356
      finally have "(\<P>(OB ; fst) {(obs, k)}) / K k =
hoelzl@40859
   357
            (\<Prod>i<n. \<Sum>m\<in>{m\<in>messages. observe k m = obs ! i}. M m)" . }
hoelzl@40859
   358
    note * = this
hoelzl@40859
   359
hoelzl@47694
   360
    have "(\<P>(OB ; fst) {(obs, k)}) / K k = (\<P>(OB ; fst) {(obs', k)}) / K k"
hoelzl@40859
   361
      unfolding *[OF obs] *[OF obs']
nipkow@64272
   362
      using t_f(1) obs_t_f by (subst (2) t_f(2)) (simp add: prod.reindex)
hoelzl@47694
   363
    then have "(\<P>(OB ; fst) {(obs, k)}) = (\<P>(OB ; fst) {(obs', k)})"
wenzelm@61808
   364
      using \<open>K k \<noteq> 0\<close> by auto }
hoelzl@40859
   365
  note t_eq_imp = this
hoelzl@40859
   366
wenzelm@46731
   367
  let ?S = "\<lambda>obs. t -`{t obs} \<inter> OB`msgs"
hoelzl@40859
   368
  { fix k obs assume "k \<in> keys" "K k \<noteq> 0" and obs: "obs \<in> OB`msgs"
hoelzl@40859
   369
    have *: "((\<lambda>x. (t (OB x), fst x)) -` {(t obs, k)} \<inter> msgs) =
hoelzl@40859
   370
      (\<Union>obs'\<in>?S obs. ((\<lambda>x. (OB x, fst x)) -` {(obs', k)} \<inter> msgs))" by auto
hoelzl@40859
   371
    have df: "disjoint_family_on (\<lambda>obs'. (\<lambda>x. (OB x, fst x)) -` {(obs', k)} \<inter> msgs) (?S obs)"
hoelzl@40859
   372
      unfolding disjoint_family_on_def by auto
hoelzl@47694
   373
    have "\<P>(t\<circ>OB ; fst) {(t obs, k)} = (\<Sum>obs'\<in>?S obs. \<P>(OB ; fst) {(obs', k)})"
hoelzl@47694
   374
      unfolding comp_def
hoelzl@62977
   375
      using finite_measure_finite_Union[OF _ _ df]
nipkow@64267
   376
      by (auto simp add: * intro!: sum_nonneg)
hoelzl@47694
   377
    also have "(\<Sum>obs'\<in>?S obs. \<P>(OB ; fst) {(obs', k)}) = real (card (?S obs)) * \<P>(OB ; fst) {(obs, k)}"
wenzelm@61808
   378
      by (simp add: t_eq_imp[OF \<open>k \<in> keys\<close> \<open>K k \<noteq> 0\<close> obs])
hoelzl@47694
   379
    finally have "\<P>(t\<circ>OB ; fst) {(t obs, k)} = real (card (?S obs)) * \<P>(OB ; fst) {(obs, k)}" .}
hoelzl@40859
   380
  note P_t_eq_P_OB = this
hoelzl@40859
   381
hoelzl@40859
   382
  { fix k obs assume "k \<in> keys" and obs: "obs \<in> OB`msgs"
hoelzl@40859
   383
    have "\<P>(t\<circ>OB | fst) {(t obs, k)} =
hoelzl@40859
   384
      real (card (t -` {t obs} \<inter> OB ` msgs)) * \<P>(OB | fst) {(obs, k)}"
wenzelm@61808
   385
      using \<P>_k[OF \<open>k \<in> keys\<close>] P_t_eq_P_OB[OF \<open>k \<in> keys\<close> _ obs] by auto }
hoelzl@40859
   386
  note CP_t_K = this
hoelzl@40859
   387
hoelzl@40859
   388
  { fix k obs assume "k \<in> keys" and obs: "obs \<in> OB`msgs"
hoelzl@40859
   389
    then have "t -`{t obs} \<inter> OB`msgs \<noteq> {}" (is "?S \<noteq> {}") by auto
hoelzl@40859
   390
    then have "real (card ?S) \<noteq> 0" by auto
hoelzl@40859
   391
hoelzl@40859
   392
    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@47694
   393
      using finite_measure_mono[of "{x. fst x = k \<and> t (OB x) = t obs} \<inter> msgs" "{x. fst x = k} \<inter> msgs"]
hoelzl@47694
   394
      using measure_nonneg[of \<mu> "{x. fst x = k \<and> t (OB x) = t obs} \<inter> msgs"]
hoelzl@62977
   395
      by (auto simp add: vimage_def conj_commute subset_eq simp del: measure_nonneg)
hoelzl@47694
   396
    also have "(\<P>(t\<circ>OB) {t obs}) = (\<Sum>k'\<in>keys. (\<P>(t\<circ>OB|fst) {(t obs, k')}) * (\<P>(fst) {k'}))"
hoelzl@47694
   397
      using finite_measure_mono[of "{x. t (OB x) = t obs \<and> fst x = k} \<inter> msgs" "{x. fst x = k} \<inter> msgs"]
hoelzl@47694
   398
      using measure_nonneg[of \<mu> "{x. fst x = k \<and> t (OB x) = t obs} \<inter> msgs"]
nipkow@64267
   399
      apply (simp add: sum_distribution_cut[of "t\<circ>OB" "t obs" fst])
nipkow@64267
   400
      apply (auto intro!: sum.cong simp: subset_eq vimage_def prob_conj_imp1)
hoelzl@47694
   401
      done
hoelzl@40859
   402
    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
   403
      \<P>(OB | fst) {(obs, k)} * \<P>(fst) {k} / (\<Sum>k'\<in>keys. \<P>(OB|fst) {(obs, k')} * \<P>(fst) {k'})"
wenzelm@61808
   404
      using CP_t_K[OF \<open>k\<in>keys\<close> obs] CP_t_K[OF _ obs] \<open>real (card ?S) \<noteq> 0\<close>
nipkow@64267
   405
      by (simp only: sum_distrib_left[symmetric] ac_simps
wenzelm@61808
   406
          mult_divide_mult_cancel_left[OF \<open>real (card ?S) \<noteq> 0\<close>]
nipkow@64267
   407
        cong: sum.cong)
hoelzl@40859
   408
    also have "(\<Sum>k'\<in>keys. \<P>(OB|fst) {(obs, k')} * \<P>(fst) {k'}) = \<P>(OB) {obs}"
nipkow@64267
   409
      using sum_distribution_cut[of OB obs fst]
nipkow@64267
   410
      by (auto intro!: sum.cong simp: prob_conj_imp1 vimage_def)
hoelzl@40859
   411
    also have "\<P>(OB | fst) {(obs, k)} * \<P>(fst) {k} / \<P>(OB) {obs} = \<P>(fst | OB) {(k, obs)}"
hoelzl@47694
   412
      by (auto simp: vimage_def conj_commute prob_conj_imp2)
hoelzl@40859
   413
    finally have "\<P>(fst | t\<circ>OB) {(k, t obs)} = \<P>(fst | OB) {(k, obs)}" . }
hoelzl@40859
   414
  note CP_T_eq_CP_O = this
hoelzl@40859
   415
wenzelm@46731
   416
  let ?H = "\<lambda>obs. (\<Sum>k\<in>keys. \<P>(fst|OB) {(k, obs)} * log b (\<P>(fst|OB) {(k, obs)})) :: real"
wenzelm@46731
   417
  let ?Ht = "\<lambda>obs. (\<Sum>k\<in>keys. \<P>(fst|t\<circ>OB) {(k, obs)} * log b (\<P>(fst|t\<circ>OB) {(k, obs)})) :: real"
hoelzl@40859
   418
hoelzl@40859
   419
  { fix obs assume obs: "obs \<in> OB`msgs"
hoelzl@40859
   420
    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
   421
      using CP_T_eq_CP_O[OF _ obs]
hoelzl@40859
   422
      by simp
hoelzl@40859
   423
    then have "?H obs = ?Ht (t obs)" . }
hoelzl@40859
   424
  note * = this
hoelzl@40859
   425
hoelzl@40859
   426
  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
   427
hoelzl@40859
   428
  { fix x
hoelzl@40859
   429
    have *: "(\<lambda>x. t (OB x)) -` {t (OB x)} \<inter> msgs =
hoelzl@40859
   430
      (\<Union>obs\<in>?S (OB x). OB -` {obs} \<inter> msgs)" by auto
hoelzl@40859
   431
    have df: "disjoint_family_on (\<lambda>obs. OB -` {obs} \<inter> msgs) (?S (OB x))"
hoelzl@40859
   432
      unfolding disjoint_family_on_def by auto
hoelzl@40859
   433
    have "\<P>(t\<circ>OB) {t (OB x)} = (\<Sum>obs\<in>?S (OB x). \<P>(OB) {obs})"
hoelzl@47694
   434
      unfolding comp_def
hoelzl@62977
   435
      using finite_measure_finite_Union[OF _ _ df]
nipkow@64267
   436
      by (force simp add: * intro!: sum_nonneg) }
hoelzl@40859
   437
  note P_t_sum_P_O = this
hoelzl@40859
   438
wenzelm@61808
   439
  txt \<open>Lemma 3\<close>
hoelzl@40859
   440
  have "\<H>(fst | OB) = -(\<Sum>obs\<in>OB`msgs. \<P>(OB) {obs} * ?Ht (t obs))"
hoelzl@47694
   441
    unfolding conditional_entropy_eq_ce_with_hypothesis using * by simp
hoelzl@40859
   442
  also have "\<dots> = -(\<Sum>obs\<in>t`OB`msgs. \<P>(t\<circ>OB) {obs} * ?Ht obs)"
hoelzl@40859
   443
    apply (subst SIGMA_image_vimage[symmetric, of "OB`msgs" t])
nipkow@64267
   444
    apply (subst sum.reindex)
nipkow@44890
   445
    apply (fastforce intro!: inj_onI)
hoelzl@40859
   446
    apply simp
nipkow@64267
   447
    apply (subst sum.Sigma[symmetric, unfolded split_def])
nipkow@44890
   448
    using finite_space apply fastforce
nipkow@44890
   449
    using finite_space apply fastforce
nipkow@64267
   450
    apply (safe intro!: sum.cong)
hoelzl@40859
   451
    using P_t_sum_P_O
nipkow@64267
   452
    by (simp add: sum_divide_distrib[symmetric] field_simps **
nipkow@64267
   453
                  sum_distrib_left[symmetric] sum_distrib_right[symmetric])
hoelzl@40859
   454
  also have "\<dots> = \<H>(fst | t\<circ>OB)"
hoelzl@47694
   455
    unfolding conditional_entropy_eq_ce_with_hypothesis
hoelzl@40859
   456
    by (simp add: comp_def image_image[symmetric])
hoelzl@49793
   457
  finally show ?thesis
hoelzl@49793
   458
    by (subst (1 2) mutual_information_eq_entropy_conditional_entropy) simp_all
hoelzl@40859
   459
qed
hoelzl@40859
   460
hoelzl@40859
   461
theorem "\<I>(fst ; OB) \<le> real (card observations) * log b (real n + 1)"
hoelzl@40859
   462
proof -
hoelzl@49793
   463
  have "\<I>(fst ; OB) = \<H>(fst) - \<H>(fst | t\<circ>OB)"
hoelzl@49793
   464
    unfolding ce_OB_eq_ce_t
hoelzl@49793
   465
    by (rule mutual_information_eq_entropy_conditional_entropy simple_function_finite)+
hoelzl@40859
   466
  also have "\<dots> = \<H>(t\<circ>OB) - \<H>(t\<circ>OB | fst)"
hoelzl@41689
   467
    unfolding entropy_chain_rule[symmetric, OF simple_function_finite simple_function_finite] sign_simps
hoelzl@47694
   468
    by (subst entropy_commute) simp
hoelzl@40859
   469
  also have "\<dots> \<le> \<H>(t\<circ>OB)"
hoelzl@47694
   470
    using conditional_entropy_nonneg[of "t\<circ>OB" fst] by simp
hoelzl@40859
   471
  also have "\<dots> \<le> log b (real (card ((t\<circ>OB)`msgs)))"
hoelzl@62977
   472
    using entropy_le_card[of "t\<circ>OB", OF simple_distributedI[OF simple_function_finite _ refl]] by simp
hoelzl@40859
   473
  also have "\<dots> \<le> log b (real (n + 1)^card observations)"
hoelzl@40859
   474
    using card_T_bound not_empty
lp15@61649
   475
    by (auto intro!: log_le simp: card_gt_0_iff of_nat_power [symmetric] simp del: of_nat_power of_nat_Suc)
hoelzl@40859
   476
  also have "\<dots> = real (card observations) * log b (real n + 1)"
lp15@61609
   477
    by (simp add: log_nat_power add.commute)
hoelzl@40859
   478
  finally show ?thesis  .
hoelzl@40859
   479
qed
hoelzl@40859
   480
hoelzl@40859
   481
end
hoelzl@40859
   482
hoelzl@41689
   483
end