src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy

 
 definition msgs :: "('key \<times> 'message list) set" where
   "msgs = keys \<times> {ms. set ms \<subseteq> messages \<and> length ms = n}"
 
 definition P :: "('key \<times> 'message list) \<Rightarrow> real" where
-  "P = (\<lambda>(k, ms). K k * (\<Prod>i<length ms. M (ms ! i)))"
+  "P = (\<lambda>(k, ms). K k * (\<Prod>i<n. M (ms ! i)))"
 
 end
 
 sublocale koepf_duermuth \<subseteq> finite_information msgs P b
 proof default

 
 definition OB :: "'key \<times> 'message list \<Rightarrow> 'observation list" where
   "OB = (\<lambda>(k, ms). map (observe k) ms)"
 
 definition t :: "'observation list \<Rightarrow> 'observation \<Rightarrow> nat" where
-  "t seq obs = length (filter (op = obs) seq)"
+  t_def2: "t seq obs = card { i. i < length seq \<and> seq ! i = obs}"
+
+lemma t_def: "t seq obs = length (filter (op = obs) seq)"
+  unfolding t_def2 length_filter_conv_card by (subst eq_commute) simp
 
 lemma card_T_bound: "card ((t\<circ>OB)`msgs) \<le> (n+1)^card observations"
 proof -
   have "(t\<circ>OB)`msgs \<subseteq> extensionalD 0 observations \<inter> (observations \<rightarrow> {.. n})"
     unfolding observations_def extensionalD_def OB_def msgs_def

     by (auto simp add: setsum_right_distrib vimage_def intro!: setsum_cong prob_conj_imp1)
   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}))) =
     -(\<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}))))" .
 qed
 
-lemma ce_OB_eq_ce_t: "\<H>(fst | OB) = \<H>(fst | t\<circ>OB)"
+lemma ce_OB_eq_ce_t: "\<I>(fst ; OB) = \<I>(fst ; t\<circ>OB)"
 proof -
   txt {* Lemma 2 *}
 
   { fix k obs obs'
     assume "k \<in> keys" "K k \<noteq> 0" and obs': "obs' \<in> OB ` msgs" and obs: "obs \<in> OB ` msgs"

       using finite_measure_finite_Union[OF _ df]
       by (force simp add: * intro!: setsum_nonneg) }
   note P_t_sum_P_O = this
 
   txt {* Lemma 3 *}
-  txt {* Lemma 3 *}
   have "\<H>(fst | OB) = -(\<Sum>obs\<in>OB`msgs. \<P>(OB) {obs} * ?Ht (t obs))"
     unfolding conditional_entropy_eq_ce_with_hypothesis using * by simp
   also have "\<dots> = -(\<Sum>obs\<in>t`OB`msgs. \<P>(t\<circ>OB) {obs} * ?Ht obs)"
     apply (subst SIGMA_image_vimage[symmetric, of "OB`msgs" t])
     apply (subst setsum_reindex)

     by (simp add: setsum_divide_distrib[symmetric] field_simps **
                   setsum_right_distrib[symmetric] setsum_left_distrib[symmetric])
   also have "\<dots> = \<H>(fst | t\<circ>OB)"
     unfolding conditional_entropy_eq_ce_with_hypothesis
     by (simp add: comp_def image_image[symmetric])
-  finally show ?thesis .
+  finally show ?thesis
+    by (subst (1 2) mutual_information_eq_entropy_conditional_entropy) simp_all
 qed
 
 theorem "\<I>(fst ; OB) \<le> real (card observations) * log b (real n + 1)"
 proof -
-  from simple_function_finite simple_function_finite
-  have "\<I>(fst ; OB) = \<H>(fst) - \<H>(fst | OB)"
-    by (rule mutual_information_eq_entropy_conditional_entropy)
-  also have "\<dots> = \<H>(fst) - \<H>(fst | t\<circ>OB)"
-    unfolding ce_OB_eq_ce_t ..
+  have "\<I>(fst ; OB) = \<H>(fst) - \<H>(fst | t\<circ>OB)"
+    unfolding ce_OB_eq_ce_t
+    by (rule mutual_information_eq_entropy_conditional_entropy simple_function_finite)+
   also have "\<dots> = \<H>(t\<circ>OB) - \<H>(t\<circ>OB | fst)"
     unfolding entropy_chain_rule[symmetric, OF simple_function_finite simple_function_finite] sign_simps
     by (subst entropy_commute) simp
   also have "\<dots> \<le> \<H>(t\<circ>OB)"
     using conditional_entropy_nonneg[of "t\<circ>OB" fst] by simp