
diff -r e0a4cb91a8a9 -r 6b9b9ebba47d src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Wed Oct 10 12:12:27 2012 +0200
+++ b/src/HOL/Probability/Information.thy	Wed Oct 10 12:12:27 2012 +0200
@@ -1121,7 +1121,6 @@
 lemma (in information_space)
   fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
   assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
-  assumes Px: "distributed M S X Px"
   assumes Py: "distributed M T Y Py"
   assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
   assumes I1: "integrable (S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Pxy x))"
@@ -1149,17 +1148,13 @@
     by (subst distributed_transform_integral[OF Pxy Py, where T=snd]) (auto intro!: integral_cong)
   finally have e_eq: "entropy b T Y = - (\<integral>(x,y). Pxy (x,y) * log b (Py y) \<partial>(S \<Otimes>\<^isub>M T))" .
   
-  have ae1: "AE x in S \<Otimes>\<^isub>M T. Px (fst x) = 0 \<longrightarrow> Pxy x = 0"
-    by (intro subdensity_real[of fst, OF _ Pxy Px]) (auto intro: measurable_Pair)
-  moreover have ae2: "AE x in S \<Otimes>\<^isub>M T. Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
+  have ae2: "AE x in S \<Otimes>\<^isub>M T. Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
     by (intro subdensity_real[of snd, OF _ Pxy Py]) (auto intro: measurable_Pair)
-  moreover have ae3: "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Px (fst x)"
-    using Px by (intro ST.AE_pair_measure) (auto simp: comp_def intro!: measurable_fst'' dest: distributed_real_AE distributed_real_measurable)
   moreover have ae4: "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Py (snd x)"
     using Py by (intro ST.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
   moreover note ae5 = Pxy[THEN distributed_real_AE]
-  ultimately have pos: "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Pxy x \<and> 0 \<le> Px (fst x) \<and> 0 \<le> Py (snd x) \<and>
-    (Pxy x = 0 \<or> (Pxy x \<noteq> 0 \<longrightarrow> 0 < Pxy x \<and> 0 < Px (fst x) \<and> 0 < Py (snd x)))"
+  ultimately have pos: "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Pxy x \<and> 0 \<le> Py (snd x) \<and>
+    (Pxy x = 0 \<or> (Pxy x \<noteq> 0 \<longrightarrow> 0 < Pxy x \<and> 0 < Py (snd x)))"
     by eventually_elim auto
 
   from pos have ae: "AE x in S \<Otimes>\<^isub>M T.
@@ -1180,7 +1175,7 @@
   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 simple_distributedI[OF X refl]] simple_distributed[OF Y] simple_distributed_joint[OF XY]])
+  simple_distributed[OF Y] simple_distributed_joint[OF XY]])
   have [simp]: "finite (X`space M)" using X by (simp add: simple_function_def)
   note Y[THEN simple_distributed_finite, simp]
   show "sigma_finite_measure (count_space (X ` space M))"
@@ -1234,7 +1229,7 @@
     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]
-    apply (auto simp add: not_le[symmetric] AE_count_space)
+  apply (auto simp add: not_le[symmetric] AE_count_space)
     done
 qed
 




