merged
authorwenzelm
Tue, 10 Feb 2015 17:13:23 +0100
changeset 59500 59817f489ce3
parent 59496 6faf024a1893 (diff)
parent 59499 14095f771781 (current diff)
child 59501 38c6cba073f4
merged
--- a/src/HOL/Library/Infinite_Set.thy	Tue Feb 10 16:46:21 2015 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Tue Feb 10 17:13:23 2015 +0100
@@ -143,23 +143,33 @@
   contains some element that occurs infinitely often.
 *}
 
+lemma inf_img_fin_dom':
+  assumes img: "finite (f ` A)" and dom: "infinite A"
+  shows "\<exists>y \<in> f ` A. infinite (f -` {y} \<inter> A)"
+proof (rule ccontr)
+  have "A \<subseteq> (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by auto
+  moreover
+  assume "\<not> ?thesis"
+  with img have "finite (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by blast
+  ultimately have "finite A" by(rule finite_subset)
+  with dom show False by contradiction
+qed
+
+lemma inf_img_fin_domE':
+  assumes "finite (f ` A)" and "infinite A"
+  obtains y where "y \<in> f`A" and "infinite (f -` {y} \<inter> A)"
+  using assms by (blast dest: inf_img_fin_dom')
+
 lemma inf_img_fin_dom:
   assumes img: "finite (f`A)" and dom: "infinite A"
   shows "\<exists>y \<in> f`A. infinite (f -` {y})"
-proof (rule ccontr)
-  assume "\<not> ?thesis"
-  with img have "finite (UN y:f`A. f -` {y})" by blast
-  moreover have "A \<subseteq> (UN y:f`A. f -` {y})" by auto
-  moreover note dom
-  ultimately show False by (simp add: infinite_super)
-qed
+using inf_img_fin_dom'[OF assms] by auto
 
 lemma inf_img_fin_domE:
   assumes "finite (f`A)" and "infinite A"
   obtains y where "y \<in> f`A" and "infinite (f -` {y})"
   using assms by (blast dest: inf_img_fin_dom)
 
-
 subsection "Infinitely Many and Almost All"
 
 text {*
--- a/src/HOL/Probability/Binary_Product_Measure.thy	Tue Feb 10 16:46:21 2015 +0100
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Tue Feb 10 17:13:23 2015 +0100
@@ -835,7 +835,6 @@
   "nn_integral (count_space UNIV \<Otimes>\<^sub>M count_space UNIV) f = nn_integral (count_space UNIV) f"
   by (subst (1 2) nn_integral_max_0[symmetric]) (auto intro!: nn_intergal_count_space_prod_eq')
 
-
 lemma pair_measure_density:
   assumes f: "f \<in> borel_measurable M1" "AE x in M1. 0 \<le> f x"
   assumes g: "g \<in> borel_measurable M2" "AE x in M2. 0 \<le> g x"
@@ -957,6 +956,106 @@
     by (subst (1 2 3) emeasure_count_space) (auto simp: finite_cartesian_product_iff)
 qed
 
+lemma nn_integral_fst_count_space':
+  assumes nonneg: "\<And>xy. 0 \<le> f xy"
+  shows "(\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f (x, y) \<partial>count_space UNIV \<partial>count_space UNIV) = integral\<^sup>N (count_space UNIV) f"
+  (is "?lhs = ?rhs")
+proof(cases)
+  assume *: "countable {xy. f xy \<noteq> 0}"
+  let ?A = "fst ` {xy. f xy \<noteq> 0}"
+  let ?B = "snd ` {xy. f xy \<noteq> 0}"
+  from * have [simp]: "countable ?A" "countable ?B" by(rule countable_image)+
+  from nonneg have f_neq_0: "\<And>xy. f xy \<noteq> 0 \<longleftrightarrow> f xy > 0"
+    by(auto simp add: order.order_iff_strict)
+  have "?lhs = (\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f (x, y) \<partial>count_space UNIV \<partial>count_space ?A)"
+    by(rule nn_integral_count_space_eq)
+      (auto simp add: f_neq_0 nn_integral_0_iff_AE AE_count_space not_le intro: rev_image_eqI)
+  also have "\<dots> = (\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f (x, y) \<partial>count_space ?B \<partial>count_space ?A)"
+    by(intro nn_integral_count_space_eq nn_integral_cong)(auto intro: rev_image_eqI)
+  also have "\<dots> = (\<integral>\<^sup>+ xy. f xy \<partial>count_space (?A \<times> ?B))"
+    by(subst sigma_finite_measure.nn_integral_fst)
+      (simp_all add: sigma_finite_measure_count_space_countable pair_measure_countable)
+  also have "\<dots> = ?rhs"
+    by(rule nn_integral_count_space_eq)(auto intro: rev_image_eqI)
+  finally show ?thesis .
+next
+  { fix xy assume "f xy \<noteq> 0"
+    with `0 \<le> f xy` have "(\<exists>r. 0 < r \<and> f xy = ereal r) \<or> f xy = \<infinity>"
+      by (cases "f xy") (auto simp: less_le)
+    then have "\<exists>n. ereal (1 / real (Suc n)) \<le> f xy"
+      by (auto elim!: nat_approx_posE intro!: less_imp_le) }
+  note * = this
+
+  assume cntbl: "uncountable {xy. f xy \<noteq> 0}"
+  also have "{xy. f xy \<noteq> 0} = (\<Union>n. {xy. 1/Suc n \<le> f xy})"
+    using * by auto
+  finally obtain n where "infinite {xy. 1/Suc n \<le> f xy}"
+    by (meson countableI_type countable_UN uncountable_infinite)
+  then obtain C where C: "C \<subseteq> {xy. 1/Suc n \<le> f xy}" and "countable C" "infinite C"
+    by (metis infinite_countable_subset')
+
+  have "\<infinity> = (\<integral>\<^sup>+ xy. ereal (1 / Suc n) * indicator C xy \<partial>count_space UNIV)"
+    using \<open>infinite C\<close> by(simp add: nn_integral_cmult)
+  also have "\<dots> \<le> ?rhs" using C
+    by(intro nn_integral_mono)(auto split: split_indicator simp add: nonneg)
+  finally have "?rhs = \<infinity>" by simp
+  moreover have "?lhs = \<infinity>"
+  proof(cases "finite (fst ` C)")
+    case True
+    then obtain x C' where x: "x \<in> fst ` C" 
+      and C': "C' = fst -` {x} \<inter> C"
+      and "infinite C'"
+      using \<open>infinite C\<close> by(auto elim!: inf_img_fin_domE')
+    from x C C' have **: "C' \<subseteq> {xy. 1 / Suc n \<le> f xy}" by auto
+
+    from C' \<open>infinite C'\<close> have "infinite (snd ` C')"
+      by(auto dest!: finite_imageD simp add: inj_on_def)
+    then have "\<infinity> = (\<integral>\<^sup>+ y. ereal (1 / Suc n) * indicator (snd ` C') y \<partial>count_space UNIV)"
+      by(simp add: nn_integral_cmult)
+    also have "\<dots> = (\<integral>\<^sup>+ y. ereal (1 / Suc n) * indicator C' (x, y) \<partial>count_space UNIV)"
+      by(rule nn_integral_cong)(force split: split_indicator intro: rev_image_eqI simp add: C')
+    also have "\<dots> = (\<integral>\<^sup>+ x'. (\<integral>\<^sup>+ y. ereal (1 / Suc n) * indicator C' (x, y) \<partial>count_space UNIV) * indicator {x} x' \<partial>count_space UNIV)"
+      by(simp add: one_ereal_def[symmetric] nn_integral_nonneg nn_integral_cmult_indicator)
+    also have "\<dots> \<le> (\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. ereal (1 / Suc n) * indicator C' (x, y) \<partial>count_space UNIV \<partial>count_space UNIV)"
+      by(rule nn_integral_mono)(simp split: split_indicator add: nn_integral_nonneg)
+    also have "\<dots> \<le> ?lhs" using **
+      by(intro nn_integral_mono)(auto split: split_indicator simp add: nonneg)
+    finally show ?thesis by simp
+  next
+    case False
+    def C' \<equiv> "fst ` C"
+    have "\<infinity> = \<integral>\<^sup>+ x. ereal (1 / Suc n) * indicator C' x \<partial>count_space UNIV"
+      using C'_def False by(simp add: nn_integral_cmult)
+    also have "\<dots> = \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. ereal (1 / Suc n) * indicator C' x * indicator {SOME y. (x, y) \<in> C} y \<partial>count_space UNIV \<partial>count_space UNIV"
+      by(auto simp add: one_ereal_def[symmetric] nn_integral_cmult_indicator intro: nn_integral_cong)
+    also have "\<dots> \<le> \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. ereal (1 / Suc n) * indicator C (x, y) \<partial>count_space UNIV \<partial>count_space UNIV"
+      by(intro nn_integral_mono)(auto simp add: C'_def split: split_indicator intro: someI)
+    also have "\<dots> \<le> ?lhs" using C
+      by(intro nn_integral_mono)(auto split: split_indicator simp add: nonneg)
+    finally show ?thesis by simp
+  qed
+  ultimately show ?thesis by simp
+qed
+
+lemma nn_integral_fst_count_space:
+  "(\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f (x, y) \<partial>count_space UNIV \<partial>count_space UNIV) = integral\<^sup>N (count_space UNIV) f"
+by(subst (2 3) nn_integral_max_0[symmetric])(rule nn_integral_fst_count_space', simp)
+
+lemma nn_integral_snd_count_space:
+  "(\<integral>\<^sup>+ y. \<integral>\<^sup>+ x. f (x, y) \<partial>count_space UNIV \<partial>count_space UNIV) = integral\<^sup>N (count_space UNIV) f"
+  (is "?lhs = ?rhs")
+proof -
+  have "?lhs = (\<integral>\<^sup>+ y. \<integral>\<^sup>+ x. (\<lambda>(y, x). f (x, y)) (y, x) \<partial>count_space UNIV \<partial>count_space UNIV)"
+    by(simp)
+  also have "\<dots> = \<integral>\<^sup>+ yx. (\<lambda>(y, x). f (x, y)) yx \<partial>count_space UNIV"
+    by(rule nn_integral_fst_count_space)
+  also have "\<dots> = \<integral>\<^sup>+ xy. f xy \<partial>count_space ((\<lambda>(x, y). (y, x)) ` UNIV)"
+    by(subst nn_integral_bij_count_space[OF inj_on_imp_bij_betw, symmetric])
+      (simp_all add: inj_on_def split_def)
+  also have "\<dots> = ?rhs" by(rule nn_integral_count_space_eq) auto
+  finally show ?thesis .
+qed
+
 subsection {* Product of Borel spaces *}
 
 lemma borel_Times:
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Feb 10 16:46:21 2015 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Feb 10 17:13:23 2015 +0100
@@ -12,6 +12,9 @@
   "~~/src/HOL/Library/Multiset"
 begin
 
+lemma ereal_divide': "b \<noteq> 0 \<Longrightarrow> ereal (a / b) = ereal a / ereal b"
+  using ereal_divide[of a b] by simp
+
 lemma (in finite_measure) countable_support:
   "countable {x. measure M {x} \<noteq> 0}"
 proof cases
@@ -279,6 +282,9 @@
     using measure_pmf.emeasure_space_1 by simp
 qed
 
+lemma emeasure_pmf_UNIV [simp]: "emeasure (measure_pmf M) UNIV = 1"
+using measure_pmf.emeasure_space_1[of M] by simp
+
 lemma in_null_sets_measure_pmfI:
   "A \<inter> set_pmf p = {} \<Longrightarrow> A \<in> null_sets (measure_pmf p)"
 using emeasure_eq_0_AE[where ?P="\<lambda>x. x \<in> A" and M="measure_pmf p"]
@@ -685,6 +691,11 @@
     by (intro subprob_space.measure_bind[where N="count_space UNIV", OF N]) auto
 qed (auto simp: Transfer.Rel_def rel_fun_def cr_pmf_def)
 
+lemma ereal_pmf_join: "ereal (pmf (join_pmf N) i) = (\<integral>\<^sup>+M. pmf M i \<partial>measure_pmf N)"
+  unfolding pmf_join
+  by (intro nn_integral_eq_integral[symmetric] measure_pmf.integrable_const_bound[where B=1])
+     (auto simp: pmf_le_1 pmf_nonneg)
+
 lemma set_pmf_join_pmf: "set_pmf (join_pmf f) = (\<Union>p\<in>set_pmf f. set_pmf p)"
 apply(simp add: set_eq_iff set_pmf_iff pmf_join)
 apply(subst integral_nonneg_eq_0_iff_AE)
@@ -732,6 +743,9 @@
     unfolding f by (subst bind_distr[OF _ measurable_measure_pmf]) auto
 qed
 
+lemma ereal_pmf_bind: "pmf (bind_pmf N f) i = (\<integral>\<^sup>+x. pmf (f x) i \<partial>measure_pmf N)"
+  by (auto intro!: nn_integral_distr simp: bind_pmf_def ereal_pmf_join map_pmf.rep_eq)
+
 lemma pmf_bind: "pmf (bind_pmf N f) i = (\<integral>x. pmf (f x) i \<partial>measure_pmf N)"
   by (auto intro!: integral_distr simp: bind_pmf_def pmf_join map_pmf.rep_eq)
 
@@ -854,6 +868,12 @@
 
 end
 
+lemma map_bind_pmf: "map_pmf f (bind_pmf M g) = bind_pmf M (\<lambda>x. map_pmf f (g x))"
+  unfolding bind_return_pmf''[symmetric] bind_assoc_pmf[of M] ..
+
+lemma bind_map_pmf: "bind_pmf (map_pmf f M) g = bind_pmf M (\<lambda>x. g (f x))"
+  unfolding bind_return_pmf''[symmetric] bind_assoc_pmf bind_return_pmf ..
+
 lemma map_join_pmf: "map_pmf f (join_pmf AA) = join_pmf (map_pmf (map_pmf f) AA)"
   unfolding bind_pmf_def[symmetric]
   unfolding bind_return_pmf''[symmetric] join_eq_bind_pmf bind_assoc_pmf
@@ -979,6 +999,94 @@
   by (auto simp: pmf.rep_eq map_pmf.rep_eq measure_distr AE_measure_pmf_iff inj_onD
            intro!: measure_pmf.finite_measure_eq_AE)
 
+subsection \<open> Conditional Probabilities \<close>
+
+context
+  fixes p :: "'a pmf" and s :: "'a set"
+  assumes not_empty: "set_pmf p \<inter> s \<noteq> {}"
+begin
+
+interpretation pmf_as_measure .
+
+lemma emeasure_measure_pmf_not_zero: "emeasure (measure_pmf p) s \<noteq> 0"
+proof
+  assume "emeasure (measure_pmf p) s = 0"
+  then have "AE x in measure_pmf p. x \<notin> s"
+    by (rule AE_I[rotated]) auto
+  with not_empty show False
+    by (auto simp: AE_measure_pmf_iff)
+qed
+
+lemma measure_measure_pmf_not_zero: "measure (measure_pmf p) s \<noteq> 0"
+  using emeasure_measure_pmf_not_zero unfolding measure_pmf.emeasure_eq_measure by simp
+
+lift_definition cond_pmf :: "'a pmf" is
+  "uniform_measure (measure_pmf p) s"
+proof (intro conjI)
+  show "prob_space (uniform_measure (measure_pmf p) s)"
+    by (intro prob_space_uniform_measure) (auto simp: emeasure_measure_pmf_not_zero)
+  show "AE x in uniform_measure (measure_pmf p) s. measure (uniform_measure (measure_pmf p) s) {x} \<noteq> 0"
+    by (simp add: emeasure_measure_pmf_not_zero measure_measure_pmf_not_zero AE_uniform_measure
+                  AE_measure_pmf_iff set_pmf.rep_eq)
+qed simp
+
+lemma pmf_cond: "pmf cond_pmf x = (if x \<in> s then pmf p x / measure p s else 0)"
+  by transfer (simp add: emeasure_measure_pmf_not_zero pmf.rep_eq)
+
+lemma set_cond_pmf: "set_pmf cond_pmf = set_pmf p \<inter> s"
+  by (auto simp add: set_pmf_iff pmf_cond measure_measure_pmf_not_zero split: split_if_asm)
+
+end
+
+lemma cond_map_pmf:
+  assumes "set_pmf p \<inter> f -` s \<noteq> {}"
+  shows "cond_pmf (map_pmf f p) s = map_pmf f (cond_pmf p (f -` s))"
+proof -
+  have *: "set_pmf (map_pmf f p) \<inter> s \<noteq> {}"
+    using assms by (simp add: set_map_pmf) auto
+  { fix x
+    have "ereal (pmf (map_pmf f (cond_pmf p (f -` s))) x) =
+      emeasure p (f -` s \<inter> f -` {x}) / emeasure p (f -` s)"
+      unfolding ereal_pmf_map cond_pmf.rep_eq[OF assms] by (simp add: nn_integral_uniform_measure)
+    also have "f -` s \<inter> f -` {x} = (if x \<in> s then f -` {x} else {})"
+      by auto
+    also have "emeasure p (if x \<in> s then f -` {x} else {}) / emeasure p (f -` s) =
+      ereal (pmf (cond_pmf (map_pmf f p) s) x)"
+      using measure_measure_pmf_not_zero[OF *]
+      by (simp add: pmf_cond[OF *] ereal_divide' ereal_pmf_map measure_pmf.emeasure_eq_measure[symmetric]
+               del: ereal_divide)
+    finally have "ereal (pmf (cond_pmf (map_pmf f p) s) x) = ereal (pmf (map_pmf f (cond_pmf p (f -` s))) x)"
+      by simp }
+  then show ?thesis
+    by (intro pmf_eqI) simp
+qed
+
+lemma bind_cond_pmf_cancel:
+  assumes in_S: "\<And>x. x \<in> set_pmf p \<Longrightarrow> x \<in> S x"
+  assumes S_eq: "\<And>x y. x \<in> S y \<Longrightarrow> S x = S y"
+  shows "bind_pmf p (\<lambda>x. cond_pmf p (S x)) = p"
+proof (rule pmf_eqI)
+  have [simp]: "\<And>x. x \<in> p \<Longrightarrow> p \<inter> (S x) \<noteq> {}"
+    using in_S by auto
+  fix z
+  have pmf_le: "pmf p z \<le> measure p (S z)"
+  proof cases
+    assume "z \<in> p" from in_S[OF this] show ?thesis
+      by (auto intro!: measure_pmf.finite_measure_mono simp: pmf.rep_eq)
+  qed (simp add: set_pmf_iff measure_nonneg)
+
+  have "ereal (pmf (bind_pmf p (\<lambda>x. cond_pmf p (S x))) z) =
+    (\<integral>\<^sup>+ x. ereal (pmf p z / measure p (S z)) * indicator (S z) x \<partial>p)"
+    by (subst ereal_pmf_bind)
+       (auto intro!: nn_integral_cong_AE dest!: S_eq split: split_indicator
+             simp: AE_measure_pmf_iff pmf_cond pmf_eq_0_set_pmf in_S)
+  also have "\<dots> = pmf p z"
+    using pmf_le pmf_nonneg[of p z]
+    by (subst nn_integral_cmult) (simp_all add: measure_nonneg measure_pmf.emeasure_eq_measure)
+  finally show "pmf (bind_pmf p (\<lambda>x. cond_pmf p (S x))) z = pmf p z"
+    by simp
+qed
+
 inductive rel_pmf :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a pmf \<Rightarrow> 'b pmf \<Rightarrow> bool"
 for R p q
 where
@@ -1023,97 +1131,23 @@
     from qr obtain qr where qr: "\<And>y z. (y, z) \<in> set_pmf qr \<Longrightarrow> S y z"
       and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto
 
-    note pmf_nonneg[intro, simp]
-    let ?pq = "\<lambda>y x. pmf pq (x, y)"
-    let ?qr = "\<lambda>y z. pmf qr (y, z)"
-
-    have nn_integral_pp2: "\<And>y. (\<integral>\<^sup>+ x. ?pq y x \<partial>count_space UNIV) = pmf q y"
-      by (simp add: nn_integral_pmf' inj_on_def q)
-         (auto simp add: ereal_pmf_map intro!: arg_cong2[where f=emeasure])
-    have nn_integral_rr1: "\<And>y. (\<integral>\<^sup>+ x. ?qr y x \<partial>count_space UNIV) = pmf q y"
-      by (simp add: nn_integral_pmf' inj_on_def q')
-         (auto simp add: ereal_pmf_map intro!: arg_cong2[where f=emeasure])
-    have eq: "\<And>y. (\<integral>\<^sup>+ x. ?pq y x \<partial>count_space UNIV) = (\<integral>\<^sup>+ z. ?qr y z \<partial>count_space UNIV)"
-      by(simp add: nn_integral_pp2 nn_integral_rr1)
-
-    def assign \<equiv> "\<lambda>y x z. ?pq y x * ?qr y z / pmf q y"
-    have assign_nonneg [simp]: "\<And>y x z. 0 \<le> assign y x z" by(simp add: assign_def)
-    have assign_eq_0_outside: "\<And>y x z. \<lbrakk> ?pq y x = 0 \<or> ?qr y z = 0 \<rbrakk> \<Longrightarrow> assign y x z = 0"
-      by(auto simp add: assign_def)
-    have nn_integral_assign1: "\<And>y z. (\<integral>\<^sup>+ x. assign y x z \<partial>count_space UNIV) = ?qr y z"
-    proof -
-      fix y z
-      have "(\<integral>\<^sup>+ x. assign y x z \<partial>count_space UNIV) = 
-            (\<integral>\<^sup>+ x. ?pq y x \<partial>count_space UNIV) * (?qr y z / pmf q y)"
-        by(simp add: assign_def nn_integral_multc times_ereal.simps(1)[symmetric] divide_real_def mult.assoc del: times_ereal.simps(1))
-      also have "\<dots> = ?qr y z" by(auto simp add: image_iff q' pmf_eq_0_set_pmf set_map_pmf nn_integral_pp2)
-      finally show "?thesis y z" .
-    qed
-    have nn_integral_assign2: "\<And>y x. (\<integral>\<^sup>+ z. assign y x z \<partial>count_space UNIV) = ?pq y x"
-    proof -
-      fix x y
-      have "(\<integral>\<^sup>+ z. assign y x z \<partial>count_space UNIV) = (\<integral>\<^sup>+ z. ?qr y z \<partial>count_space UNIV) * (?pq y x / pmf q y)"
-        by(simp add: assign_def divide_real_def mult.commute[where a="?pq y x"] mult.assoc nn_integral_multc times_ereal.simps(1)[symmetric] del: times_ereal.simps(1))
-      also have "\<dots> = ?pq y x" by(auto simp add: image_iff pmf_eq_0_set_pmf set_map_pmf q nn_integral_rr1)
-      finally show "?thesis y x" .
-    qed
-
-    def pqr \<equiv> "embed_pmf (\<lambda>(y, x, z). assign y x z)"
-    { fix y x z
-      have "assign y x z = pmf pqr (y, x, z)"
-        unfolding pqr_def
-      proof (subst pmf_embed_pmf)
-        have "(\<integral>\<^sup>+ x. ereal ((\<lambda>(y, x, z). assign y x z) x) \<partial>count_space UNIV) =
-          (\<integral>\<^sup>+ x. ereal ((\<lambda>(y, x, z). assign y x z) x) \<partial>(count_space ((\<lambda>((x, y), z). (y, x, z)) ` (pq \<times> r))))"
-          by (force simp add: pmf_eq_0_set_pmf r set_map_pmf split: split_indicator
-                    intro!: nn_integral_count_space_eq assign_eq_0_outside)
-        also have "\<dots> = (\<integral>\<^sup>+ x. ereal ((\<lambda>((x, y), z). assign y x z) x) \<partial>(count_space (pq \<times> r)))"
-          by (subst nn_integral_bij_count_space[OF inj_on_imp_bij_betw, symmetric])
-             (auto simp: inj_on_def intro!: nn_integral_cong)
-        also have "\<dots> = (\<integral>\<^sup>+ xy. \<integral>\<^sup>+z. ereal ((\<lambda>((x, y), z). assign y x z) (xy, z)) \<partial>count_space r \<partial>count_space pq)"
-          by (subst sigma_finite_measure.nn_integral_fst)
-             (auto simp: pair_measure_countable sigma_finite_measure_count_space_countable)
-        also have "\<dots> = (\<integral>\<^sup>+ xy. \<integral>\<^sup>+z. ereal ((\<lambda>((x, y), z). assign y x z) (xy, z)) \<partial>count_space UNIV \<partial>count_space pq)"
-          by (intro nn_integral_cong nn_integral_count_space_eq)
-             (force simp: r set_map_pmf pmf_eq_0_set_pmf intro!: assign_eq_0_outside)+
-        also have "\<dots> = (\<integral>\<^sup>+ z. ?pq (snd z) (fst z) \<partial>count_space pq)"
-          by (subst nn_integral_assign2[symmetric]) (auto intro!: nn_integral_cong)
-        finally show "(\<integral>\<^sup>+ x. ereal ((\<lambda>(y, x, z). assign y x z) x) \<partial>count_space UNIV) = 1"
-          by (simp add: nn_integral_pmf emeasure_pmf)
-      qed auto }
-    note a = this
-
-    def pr \<equiv> "map_pmf (\<lambda>(y, x, z). (x, z)) pqr"
+    def pr \<equiv> "bind_pmf pq (\<lambda>(x, y). bind_pmf (cond_pmf qr {(y', z). y' = y}) (\<lambda>(y', z). return_pmf (x, z)))"
+    have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {(y', z). y' = y} \<noteq> {}"
+      by (force simp: q' set_map_pmf)
 
     have "rel_pmf (R OO S) p r"
-    proof
-      have pq_eq: "pq = map_pmf (\<lambda>(y, x, z). (x, y)) pqr"
-      proof (rule pmf_eqI)
-        fix i
-        show "pmf pq i = pmf (map_pmf (\<lambda>(y, x, z). (x, y)) pqr) i"
-          using nn_integral_assign2[of "snd i" "fst i", symmetric]
-          by (auto simp add: a nn_integral_pmf' inj_on_def ereal.inject[symmetric] ereal_pmf_map 
-                   simp del: ereal.inject intro!: arg_cong2[where f=emeasure])
-      qed
-      then show "map_pmf fst pr = p"
-        unfolding p pr_def by (simp add: map_pmf_comp split_beta)
-
-      have qr_eq: "qr = map_pmf (\<lambda>(y, x, z). (y, z)) pqr"
-      proof (rule pmf_eqI)
-        fix i show "pmf qr i = pmf (map_pmf (\<lambda>(y, x, z). (y, z)) pqr) i"
-          using nn_integral_assign1[of "fst i" "snd i", symmetric]
-          by (auto simp add: a nn_integral_pmf' inj_on_def ereal.inject[symmetric] ereal_pmf_map 
-                   simp del: ereal.inject intro!: arg_cong2[where f=emeasure])
-      qed
-      then show "map_pmf snd pr = r"
-        unfolding r pr_def by (simp add: map_pmf_comp split_beta)
-
-      fix x z assume "(x, z) \<in> set_pmf pr"
-      then have "\<exists>y. (x, y) \<in> set_pmf pq \<and> (y, z) \<in> set_pmf qr"
-        unfolding pr_def pq_eq qr_eq by (force simp: set_map_pmf)
+    proof (rule rel_pmf.intros)
+      fix x z assume "(x, z) \<in> pr"
+      then have "\<exists>y. (x, y) \<in> pq \<and> (y, z) \<in> qr"
+        by (auto simp: q pr_welldefined pr_def set_bind_pmf split_beta set_return_pmf set_cond_pmf set_map_pmf)
       with pq qr show "(R OO S) x z"
         by blast
-    qed }
+    next
+      have "map_pmf snd pr = map_pmf snd (bind_pmf q (\<lambda>y. cond_pmf qr {(y', z). y' = y}))"
+        by (simp add: pr_def q split_beta bind_map_pmf bind_return_pmf'' map_bind_pmf map_return_pmf)
+      then show "map_pmf snd pr = r"
+        unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) auto
+    qed (simp add: pr_def map_bind_pmf split_beta map_return_pmf bind_return_pmf'' p) }
   then show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)"
     by(auto simp add: le_fun_def)
 qed (fact natLeq_card_order natLeq_cinfinite)+