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