
diff -r 8d7cec9b861d -r 7dc8ac6f0895 src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Mon Nov 24 12:20:35 2014 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Mon Nov 24 12:20:14 2014 +0100
@@ -98,6 +98,9 @@
 interpretation measure_pmf!: subprob_space "measure_pmf M" for M
   by (rule prob_space_imp_subprob_space) unfold_locales
 
+lemma subprob_space_measure_pmf: "subprob_space (measure_pmf x)"
+  by unfold_locales
+
 locale pmf_as_measure
 begin
 
@@ -141,12 +144,16 @@
 lemma sets_measure_pmf[simp]: "sets (measure_pmf p) = UNIV"
   by transfer metis
 
-lemma sets_measure_pmf_count_space: "sets (measure_pmf M) = sets (count_space UNIV)"
+lemma sets_measure_pmf_count_space[measurable_cong]:
+  "sets (measure_pmf M) = sets (count_space UNIV)"
   by simp
 
 lemma space_measure_pmf[simp]: "space (measure_pmf p) = UNIV"
   using sets_eq_imp_space_eq[of "measure_pmf p" "count_space UNIV"] by simp
 
+lemma measure_pmf_in_subprob_algebra[measurable (raw)]: "measure_pmf x \<in> space (subprob_algebra (count_space UNIV))"
+  by (simp add: space_subprob_algebra subprob_space_measure_pmf)
+
 lemma measurable_pmf_measure1[simp]: "measurable (M :: 'a pmf) N = UNIV \<rightarrow> space N"
   by (auto simp: measurable_def)
 
@@ -555,11 +562,11 @@
   shows "bind (measure_pmf x) A = bind (measure_pmf x) B"
 proof (rule measure_eqI)
   show "sets (measure_pmf x \<guillemotright>= A) = sets (measure_pmf x \<guillemotright>= B)"
-    using assms by (subst (1 2) sets_bind) auto
+    using assms by (subst (1 2) sets_bind) (auto simp: space_subprob_algebra)
 next
   fix X assume "X \<in> sets (measure_pmf x \<guillemotright>= A)"
   then have X: "X \<in> sets N"
-    using assms by (subst (asm) sets_bind) auto
+    using assms by (subst (asm) sets_bind) (auto simp: space_subprob_algebra)
   show "emeasure (measure_pmf x \<guillemotright>= A) X = emeasure (measure_pmf x \<guillemotright>= B) X"
     using assms
     by (subst (1 2) emeasure_bind[where N=N, OF _ _ X])
@@ -575,21 +582,19 @@
 proof (intro conjI)
   fix M :: "'a pmf pmf"
 
-  have *: "measure_pmf \<in> measurable (measure_pmf M) (subprob_algebra (count_space UNIV))"
-    using measurable_measure_pmf[of "\<lambda>x. x"] by simp
-  
   interpret bind: prob_space "measure_pmf M \<guillemotright>= measure_pmf"
-    apply (rule measure_pmf.prob_space_bind[OF _ *])
-    apply (auto intro!: AE_I2)
+    apply (intro measure_pmf.prob_space_bind[where S="count_space UNIV"] AE_I2)
+    apply (auto intro!: subprob_space_measure_pmf simp: space_subprob_algebra)
     apply unfold_locales
     done
   show "prob_space (measure_pmf M \<guillemotright>= measure_pmf)"
     by intro_locales
   show "sets (measure_pmf M \<guillemotright>= measure_pmf) = UNIV"
-    by (subst sets_bind[OF *]) auto
+    by (subst sets_bind) auto
   have "AE x in measure_pmf M \<guillemotright>= measure_pmf. emeasure (measure_pmf M \<guillemotright>= measure_pmf) {x} \<noteq> 0"
-    by (auto simp add: AE_bind[OF _ *] AE_measure_pmf_iff emeasure_bind[OF _ *]
-        nn_integral_0_iff_AE measure_pmf.emeasure_eq_measure measure_le_0_iff set_pmf_iff pmf.rep_eq)
+    by (auto simp: AE_bind[where B="count_space UNIV"] measure_pmf_in_subprob_algebra
+                   emeasure_bind[where N="count_space UNIV"] AE_measure_pmf_iff nn_integral_0_iff_AE
+                   measure_pmf.emeasure_eq_measure measure_le_0_iff set_pmf_iff pmf.rep_eq)
   then show "AE x in measure_pmf M \<guillemotright>= measure_pmf. measure (measure_pmf M \<guillemotright>= measure_pmf) {x} \<noteq> 0"
     unfolding bind.emeasure_eq_measure by simp
 qed
@@ -772,6 +777,10 @@
 lemma set_pair_pmf: "set_pmf (pair_pmf A B) = set_pmf A \<times> set_pmf B"
   unfolding pair_pmf_def set_bind_pmf set_return_pmf by auto
 
+lemma measure_pmf_in_subprob_space[measurable (raw)]:
+  "measure_pmf M \<in> space (subprob_algebra (count_space UNIV))"
+  by (simp add: space_subprob_algebra) intro_locales
+
 lemma bind_pair_pmf:
   assumes M[measurable]: "M \<in> measurable (count_space UNIV \<Otimes>\<^sub>M count_space UNIV) (subprob_algebra N)"
   shows "measure_pmf (pair_pmf A B) \<guillemotright>= M = (measure_pmf A \<guillemotright>= (\<lambda>x. measure_pmf B \<guillemotright>= (\<lambda>y. M (x, y))))"
@@ -780,46 +789,25 @@
   have M'[measurable]: "M \<in> measurable (pair_pmf A B) (subprob_algebra N)"
     using M[THEN measurable_space] by (simp_all add: space_pair_measure)
 
+  note measurable_bind[where N="count_space UNIV", measurable]
+  note measure_pmf_in_subprob_space[simp]
+
   have sets_eq_N: "sets ?L = N"
-    by (simp add: sets_bind[OF M'])
+    by (subst sets_bind[OF sets_kernel[OF M']]) auto
   show "sets ?L = sets ?R"
-    unfolding sets_eq_N
-    apply (subst sets_bind[where N=N])
-    apply (rule measurable_bind)
-    apply (rule measurable_compose[OF _ measurable_measure_pmf])
-    apply measurable
-    apply (auto intro!: sets_pair_measure_cong sets_measure_pmf_count_space)
-    done
+    using measurable_space[OF M]
+    by (simp add: sets_eq_N space_pair_measure space_subprob_algebra)
   fix X assume "X \<in> sets ?L"
   then have X[measurable]: "X \<in> sets N"
     unfolding sets_eq_N .
   then show "emeasure ?L X = emeasure ?R X"
     apply (simp add: emeasure_bind[OF _ M' X])
-    unfolding pair_pmf_def measure_pmf_bind[of A]
-    apply (subst nn_integral_bind)
-    apply (rule measurable_compose[OF M' measurable_emeasure_subprob_algebra, OF X])
-    apply (subst measurable_cong_sets[OF sets_measure_pmf_count_space refl])
-    apply (subst subprob_algebra_cong[OF sets_measure_pmf_count_space])
-    apply measurable
-    unfolding measure_pmf_bind
-    apply (subst nn_integral_bind)
-    apply (rule measurable_compose[OF M' measurable_emeasure_subprob_algebra, OF X])
-    apply (subst measurable_cong_sets[OF sets_measure_pmf_count_space refl])
-    apply (subst subprob_algebra_cong[OF sets_measure_pmf_count_space])
+    apply (simp add: nn_integral_bind[where B="count_space UNIV"] pair_pmf_def measure_pmf_bind[of A]
+      nn_integral_measure_pmf_finite set_return_pmf emeasure_nonneg pmf_return one_ereal_def[symmetric])
+    apply (subst emeasure_bind[OF _ _ X])
     apply measurable
-    apply (simp add: nn_integral_measure_pmf_finite set_return_pmf emeasure_nonneg pmf_return one_ereal_def[symmetric])
     apply (subst emeasure_bind[OF _ _ X])
-    apply simp
-    apply (rule measurable_bind[where N="count_space UNIV"])
-    apply (rule measurable_compose[OF _ measurable_measure_pmf])
     apply measurable
-    apply (rule sets_pair_measure_cong sets_measure_pmf_count_space refl)+
-    apply (subst measurable_cong_sets[OF sets_pair_measure_cong[OF sets_measure_pmf_count_space refl] refl])
-    apply simp
-    apply (subst emeasure_bind[OF _ _ X])
-    apply simp
-    apply (rule measurable_compose[OF _ M])
-    apply (auto simp: space_pair_measure)
     done
 qed
 




