# HG changeset patch
# User hoelzl
# Date 1301671233 -7200
# Node ID aded341192137a6c7cf1936d9191b9a0bb1fe9d6
# Parent  5f311600ba2674ddd0ba08f957071317dd4ac9df
add prob_space_vimage

diff -r 5f311600ba26 -r aded34119213 src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Fri Apr 01 16:29:58 2011 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy	Fri Apr 01 17:20:33 2011 +0200
@@ -201,24 +201,35 @@
   finally show ?thesis .
 qed
 
-lemma (in prob_space) distribution_prob_space:
-  assumes "random_variable S X"
-  shows "prob_space (S\<lparr>measure := extreal \<circ> distribution X\<rparr>)"
+lemma (in prob_space) prob_space_vimage:
+  assumes S: "sigma_algebra S"
+  assumes T: "T \<in> measure_preserving M S"
+  shows "prob_space S"
 proof -
-  interpret S: measure_space "S\<lparr>measure := extreal \<circ> distribution X\<rparr>"
-  proof (rule measure_space.measure_space_cong)
-    show "measure_space (S\<lparr> measure := \<lambda>A. \<mu> (X -` A \<inter> space M) \<rparr>)"
-      using assms by (auto intro!: measure_space_vimage simp: measure_preserving_def)
-  qed (insert assms, auto simp add: finite_measure_eq distribution_def measurable_sets)
+  interpret S: measure_space S
+    using S and T by (rule measure_space_vimage)
   show ?thesis
-  proof (default, simp)
-    have "X -` space S \<inter> space M = space M"
-      using `random_variable S X` by (auto simp: measurable_def)
-    then show "extreal (distribution X (space S)) = 1"
-      by (simp add: distribution_def one_extreal_def prob_space)
+  proof
+    from T[THEN measure_preservingD2]
+    have "T -` space S \<inter> space M = space M"
+      by (auto simp: measurable_def)
+    with T[THEN measure_preservingD, of "space S", symmetric]
+    show  "measure S (space S) = 1"
+      using measure_space_1 by simp
   qed
 qed
 
+lemma (in prob_space) distribution_prob_space:
+  assumes X: "random_variable S X"
+  shows "prob_space (S\<lparr>measure := extreal \<circ> distribution X\<rparr>)" (is "prob_space ?S")
+proof (rule prob_space_vimage)
+  show "X \<in> measure_preserving M ?S"
+    using X
+    unfolding measure_preserving_def distribution_def_raw
+    by (auto simp: finite_measure_eq measurable_sets)
+  show "sigma_algebra ?S" using X by simp
+qed
+
 lemma (in prob_space) AE_distribution:
   assumes X: "random_variable MX X" and "AE x in MX\<lparr>measure := extreal \<circ> distribution X\<rparr>. Q x"
   shows "AE x. Q (X x)"