author hoelzl Wed, 10 Oct 2012 12:12:29 +0200 changeset 49793 dd719cdeca8f parent 49792 43f49922811d child 49794 3c7b5988e094
simplified definitions
```--- 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
-  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```