# HG changeset patch
# User hoelzl
# Date 1349863949 -7200
# Node ID dd719cdeca8f03065e71806f9fbf6bcd8e848182
# Parent  43f49922811d3068403af7cc8c8212a23a50966b
simplified definitions

diff -r 43f49922811d -r dd719cdeca8f src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Wed Oct 10 12:12:29 2012 +0200
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Wed Oct 10 12:12:29 2012 +0200
@@ -145,7 +145,7 @@
   "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
 
@@ -191,7 +191,10 @@
   "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 -
@@ -324,7 +327,7 @@
     -(\<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 *}
 
@@ -433,7 +436,6 @@
   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)"
@@ -451,16 +453,15 @@
   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