# HG changeset patch
# User hoelzl
# Date 1295455493 -3600
# Node ID a5d1b2df5e9760bee5e0975f0f3b8b70f302154c
# Parent  32fe42892983ade191dc8d1b95bca12bf6243811
tuned proof

diff -r 32fe42892983 -r a5d1b2df5e97 src/HOL/Probability/Product_Measure.thy
--- a/src/HOL/Probability/Product_Measure.thy	Tue Jan 18 21:37:23 2011 +0100
+++ b/src/HOL/Probability/Product_Measure.thy	Wed Jan 19 17:44:53 2011 +0100
@@ -656,29 +656,14 @@
     show "range F \<subseteq> sets E" "F \<up> space E" "\<And>i. pair_measure (F i) \<noteq> \<omega>"
       using F by auto
     show "measure_space P pair_measure" by default
-  next
-    show "measure_space P ?\<nu>"
-    proof
-      show "?\<nu> {} = 0" by auto
-      show "countably_additive P ?\<nu>"
-        unfolding countably_additive_def
-      proof (intro allI impI)
-        fix F :: "nat \<Rightarrow> ('a \<times> 'b) set"
-        assume F: "range F \<subseteq> sets P" "disjoint_family F"
-        from F have *: "\<And>i. F i \<in> sets P" "(\<Union>i. F i) \<in> sets P" by auto
-        moreover from F have "\<And>i. (\<lambda>y. \<mu>1 ((\<lambda>x. (x, y)) -` F i)) \<in> borel_measurable M2"
-          by (intro measure_cut_measurable_snd) auto
-        moreover have "\<And>y. disjoint_family (\<lambda>i. (\<lambda>x. (x, y)) -` F i)"
-          by (intro disjoint_family_on_bisimulation[OF F(2)]) auto
-        moreover have "\<And>y. y \<in> space M2 \<Longrightarrow> range (\<lambda>i. (\<lambda>x. (x, y)) -` F i) \<subseteq> sets M1"
-          using F by (auto intro!: measurable_cut_snd)
-        ultimately show "(\<Sum>\<^isub>\<infinity>n. ?\<nu> (F n)) = ?\<nu> (\<Union>i. F i)"
-          by (simp add: vimage_UN M2.positive_integral_psuminf[symmetric]
-                        M1.measure_countably_additive
-                   cong: M2.positive_integral_cong)
-      qed
-    qed
-  next
+    interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
+    have space_P: "space P = space M1 \<times> space M2" unfolding pair_algebra_def by simp
+    have "measure_space (Q.vimage_algebra (space P) (\<lambda>(x,y). (y,x))) (\<lambda>A. Q.pair_measure ((\<lambda>(x,y). (y,x)) ` A))"
+      by (rule Q.measure_space_isomorphic) (auto simp add: pair_algebra_def bij_betw_def intro!: inj_onI)
+    then show "measure_space P ?\<nu>" unfolding space_P Q.pair_sigma_algebra_swap[symmetric]
+      by (rule measure_space.measure_space_cong)
+         (auto intro!: M2.positive_integral_cong arg_cong[where f=\<mu>1]
+               simp: Q.pair_measure_alt inj_vimage_image_eq sets_pair_sigma_algebra_swap)
     fix X assume "X \<in> sets E"
     then obtain A B where X: "X = A \<times> B" and AB: "A \<in> sets M1" "B \<in> sets M2"
       unfolding pair_algebra_def by auto