vimage of measurable function is a measure space

--- a/src/HOL/Probability/Measure.thy	Fri Aug 27 14:05:16 2010 +0200
+++ b/src/HOL/Probability/Measure.thy	Fri Aug 27 14:06:12 2010 +0200
@@ -451,6 +451,32 @@
   qed
 qed
 
+lemma (in measure_space) measure_space_vimage:
+  assumes "f \<in> measurable M M'"
+  and "sigma_algebra M'"
+  shows "measure_space M' (\<lambda>A. \<mu> (f -` A \<inter> space M))" (is "measure_space M' ?T")
+proof -
+  interpret M': sigma_algebra M' by fact
+
+  show ?thesis
+  proof
+    show "?T {} = 0" by simp
+
+    show "countably_additive M' ?T"
+    proof (unfold countably_additive_def, safe)
+      fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets M'" "disjoint_family A"
+      hence *: "\<And>i. f -` (A i) \<inter> space M \<in> sets M"
+        using `f \<in> measurable M M'` by (auto simp: measurable_def)
+      moreover have "(\<Union>i. f -`  A i \<inter> space M) \<in> sets M"
+        using * by blast
+      moreover have **: "disjoint_family (\<lambda>i. f -` A i \<inter> space M)"
+        using `disjoint_family A` by (auto simp: disjoint_family_on_def)
+      ultimately show "(\<Sum>\<^isub>\<infinity> i. ?T (A i)) = ?T (\<Union>i. A i)"
+        using measure_countably_additive[OF _ **] by (auto simp: comp_def vimage_UN)
+    qed
+  qed
+qed
+
 section "@{text \<sigma>}-finite Measures"
 
 locale sigma_finite_measure = measure_space +

--- a/src/HOL/Probability/Probability_Space.thy	Fri Aug 27 14:05:16 2010 +0200
+++ b/src/HOL/Probability/Probability_Space.thy	Fri Aug 27 14:06:12 2010 +0200
@@ -197,35 +197,17 @@
 qed
 
 lemma distribution_prob_space:
-  fixes S :: "('c, 'd) algebra_scheme"
-  assumes "sigma_algebra S" "random_variable S X"
+  assumes S: "sigma_algebra S" "random_variable S X"
   shows "prob_space S (distribution X)"
 proof -
-  interpret S: sigma_algebra S by fact
+  interpret S: measure_space S "distribution X"
+    using measure_space_vimage[OF S(2,1)] unfolding distribution_def .
   show ?thesis
   proof
-    show "distribution X {} = 0" unfolding distribution_def by simp
     have "X -` space S \<inter> space M = space M"
       using `random_variable S X` by (auto simp: measurable_def)
-    then show "distribution X (space S) = 1" using measure_space_1 by (simp add: distribution_def)
-
-    show "countably_additive S (distribution X)"
-    proof (unfold countably_additive_def, safe)
-      fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets S" "disjoint_family A"
-      hence *: "\<And>i. X -` A i \<inter> space M \<in> sets M"
-        using `random_variable S X` by (auto simp: measurable_def)
-      moreover hence "\<And>i. \<mu> (X -` A i \<inter> space M) \<noteq> \<omega>"
-        using finite_measure by auto
-      moreover have "(\<Union>i. X -`  A i \<inter> space M) \<in> sets M"
-        using * by blast
-      moreover hence "\<mu> (\<Union>i. X -` A i \<inter> space M) \<noteq> \<omega>"
-        using finite_measure by auto
-      moreover have **: "disjoint_family (\<lambda>i. X -` A i \<inter> space M)"
-        using `disjoint_family A` by (auto simp: disjoint_family_on_def)
-      ultimately show "(\<Sum>\<^isub>\<infinity> i. distribution X (A i)) = distribution X (\<Union>i. A i)"
-        using measure_countably_additive[OF _ **]
-        by (auto simp: distribution_def Real_real comp_def vimage_UN)
-    qed
+    then show "distribution X (space S) = 1"
+      using measure_space_1 by (simp add: distribution_def)
   qed
 qed