# HG changeset patch
# User hoelzl
# Date 1349863949 -7200
# Node ID 43f49922811d3068403af7cc8c8212a23a50966b
# Parent  e0854abfb3fc401a8fe39daf8d4be2870043d8b7
remove unnecessary assumption from conditional_entropy_eq

diff -r e0854abfb3fc -r 43f49922811d src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Wed Oct 10 12:12:28 2012 +0200
+++ b/src/HOL/Probability/Information.thy	Wed Oct 10 12:12:29 2012 +0200
@@ -1227,12 +1227,16 @@
 qed
 
 lemma (in information_space) conditional_entropy_eq:
-  assumes Y: "simple_distributed M Y Py" and X: "simple_function M X"
+  assumes Y: "simple_distributed M Y Py"
   assumes XY: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
     shows "\<H>(X | Y) = - (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / Py y))"
 proof (subst conditional_entropy_generic_eq[OF _ _
   simple_distributed[OF Y] simple_distributed_joint[OF XY]])
-  have [simp]: "finite (X`space M)" using X by (simp add: simple_function_def)
+  have "finite ((\<lambda>x. (X x, Y x))`space M)"
+    using XY unfolding simple_distributed_def by auto
+  from finite_imageI[OF this, of fst]
+  have [simp]: "finite (X`space M)"
+    by (simp add: image_compose[symmetric] comp_def)
   note Y[THEN simple_distributed_finite, simp]
   show "sigma_finite_measure (count_space (X ` space M))"
     by (simp add: sigma_finite_measure_count_space_finite)
@@ -1241,11 +1245,11 @@
   let ?f = "(\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy x else 0)"
   have "count_space (X ` space M) \<Otimes>\<^isub>M count_space (Y ` space M) = count_space (X`space M \<times> Y`space M)"
     (is "?P = ?C")
-    using X Y by (simp add: simple_distributed_finite pair_measure_count_space)
+    using Y by (simp add: simple_distributed_finite pair_measure_count_space)
   have eq: "(\<lambda>(x, y). ?f (x, y) * log b (?f (x, y) / Py y)) =
     (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy x * log b (Pxy x / Py (snd x)) else 0)"
     by auto
-  from X Y show "- (\<integral> (x, y). ?f (x, y) * log b (?f (x, y) / Py y) \<partial>?P) =
+  from Y show "- (\<integral> (x, y). ?f (x, y) * log b (?f (x, y) / Py y) \<partial>?P) =
     - (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / Py y))"
     by (auto intro!: setsum_cong simp add: `?P = ?C` lebesgue_integral_count_space_finite simple_distributed_finite eq setsum_cases split_beta')
 qed
@@ -1277,7 +1281,7 @@
     by (intro subdensity_real[of snd, OF _ Pxy[THEN simple_distributed] Py[THEN simple_distributed]]) (auto intro: measurable_Pair)
   then show ?thesis
     apply (subst conditional_mutual_information_eq[OF Py Pxy Pxy Pxxy])
-    apply (subst conditional_entropy_eq[OF Py X Pxy])
+    apply (subst conditional_entropy_eq[OF Py Pxy])
     apply (auto intro!: setsum_cong simp: Pxxy_eq setsum_negf[symmetric] eq setsum_reindex[OF inj]
                 log_simps zero_less_mult_iff zero_le_mult_iff field_simps mult_less_0_iff AE_count_space)
     using Py[THEN simple_distributed, THEN distributed_real_AE] Pxy[THEN simple_distributed, THEN distributed_real_AE]
diff -r e0854abfb3fc -r 43f49922811d src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Wed Oct 10 12:12:28 2012 +0200
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Wed Oct 10 12:12:29 2012 +0200
@@ -306,7 +306,6 @@
      log b ((\<P>(X ; Y) {(x,y)}) / (\<P>(Y) {y}))))"
   apply (subst conditional_entropy_eq[OF
     simple_distributedI[OF simple_function_finite refl]
-    simple_function_finite
     simple_distributedI[OF simple_function_finite refl]])
   unfolding space_point_measure
 proof -