# HG changeset patch
# User hoelzl
# Date 1295945145 -3600
# Node ID 621fa31e1dbd2d5e8cd14629dca6fce0de5cc6b3
# Parent  1eef159301dfa389f04526cd8a3926a009d558c5# Parent  baf1964bc4681a1641a960aac664f3a9b3622699
merged

diff -r 1eef159301df -r 621fa31e1dbd src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Fri Jan 21 10:43:09 2011 +0100
+++ b/src/HOL/Probability/Information.thy	Tue Jan 25 09:45:45 2011 +0100
@@ -180,30 +180,6 @@
     by (simp add: cong \<nu>.integral_cong_measure[OF cong(2)])
 qed
 
-lemma (in sigma_finite_measure) KL_divergence_vimage:
-  assumes f: "bij_betw f S (space M)"
-  assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
-  shows "KL_divergence b (vimage_algebra S f) (\<lambda>A. \<nu> (f ` A)) (\<lambda>A. \<mu> (f ` A)) = KL_divergence b M \<nu> \<mu>"
-    (is "KL_divergence b ?M ?\<nu> ?\<mu> = _")
-proof -
-  interpret \<nu>: measure_space M \<nu> by fact
-  interpret v: measure_space ?M ?\<nu>
-    using f by (rule \<nu>.measure_space_isomorphic)
-
-  let ?RN = "sigma_finite_measure.RN_deriv ?M ?\<mu> ?\<nu>"
-  from RN_deriv_vimage[OF f[THEN bij_inv_the_inv_into] \<nu>]
-  have *: "\<nu>.almost_everywhere (\<lambda>x. ?RN (the_inv_into S f x) = RN_deriv \<nu> x)"
-    by (rule absolutely_continuous_AE[OF \<nu>])
-
-  show ?thesis
-    unfolding KL_divergence_def \<nu>.integral_vimage_inv[OF f]
-    apply (rule \<nu>.integral_cong_AE)
-    apply (rule \<nu>.AE_mp[OF *])
-    apply (rule \<nu>.AE_cong)
-    apply simp
-    done
-qed
-
 lemma (in finite_measure_space) KL_divergence_eq_finite:
   assumes v: "finite_measure_space M \<nu>"
   assumes ac: "absolutely_continuous \<nu>"
@@ -259,50 +235,6 @@
     \<lparr> space = X`space M, sets = Pow (X`space M) \<rparr>
     \<lparr> space = Y`space M, sets = Pow (Y`space M) \<rparr> X Y"
 
-lemma (in information_space) mutual_information_commute_generic:
-  assumes X: "random_variable S X" and Y: "random_variable T Y"
-  assumes ac: "measure_space.absolutely_continuous (sigma (pair_algebra S T))
-   (pair_sigma_finite.pair_measure S (distribution X) T (distribution Y)) (joint_distribution X Y)"
-  shows "mutual_information b S T X Y = mutual_information b T S Y X"
-proof -
-  interpret P: prob_space "sigma (pair_algebra S T)" "joint_distribution X Y"
-    using random_variable_pairI[OF X Y] by (rule distribution_prob_space)
-  interpret Q: prob_space "sigma (pair_algebra T S)" "joint_distribution Y X"
-    using random_variable_pairI[OF Y X] by (rule distribution_prob_space)
-  interpret X: prob_space S "distribution X" using X by (rule distribution_prob_space)
-  interpret Y: prob_space T "distribution Y" using Y by (rule distribution_prob_space)
-  interpret ST: pair_sigma_finite S "distribution X" T "distribution Y" by default
-  interpret TS: pair_sigma_finite T "distribution Y" S "distribution X" by default
-
-  have ST: "measure_space (sigma (pair_algebra S T)) (joint_distribution X Y)" by default
-  have TS: "measure_space (sigma (pair_algebra T S)) (joint_distribution Y X)" by default
-
-  have bij_ST: "bij_betw (\<lambda>(x, y). (y, x)) (space (sigma (pair_algebra S T))) (space (sigma (pair_algebra T S)))"
-    by (auto intro!: inj_onI simp: space_pair_algebra bij_betw_def)
-  have bij_TS: "bij_betw (\<lambda>(x, y). (y, x)) (space (sigma (pair_algebra T S))) (space (sigma (pair_algebra S T)))"
-    by (auto intro!: inj_onI simp: space_pair_algebra bij_betw_def)
-
-  { fix A
-    have "joint_distribution X Y ((\<lambda>(x, y). (y, x)) ` A) = joint_distribution Y X A"
-      unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>]) }
-  note jd_commute = this
-
-  { fix A assume A: "A \<in> sets (sigma (pair_algebra T S))"
-    have *: "\<And>x y. indicator ((\<lambda>(x, y). (y, x)) ` A) (x, y) = (indicator A (y, x) :: pextreal)"
-      unfolding indicator_def by auto
-    have "ST.pair_measure ((\<lambda>(x, y). (y, x)) ` A) = TS.pair_measure A"
-      unfolding ST.pair_measure_def TS.pair_measure_def
-      using A by (auto simp add: TS.Fubini[symmetric] *) }
-  note pair_measure_commute = this
-
-  show ?thesis
-    unfolding mutual_information_def
-    unfolding ST.KL_divergence_vimage[OF bij_TS ST ac, symmetric]
-    unfolding space_sigma space_pair_algebra jd_commute
-    unfolding ST.pair_sigma_algebra_swap[symmetric]
-    by (simp cong: TS.KL_divergence_cong[OF TS] add: pair_measure_commute)
-qed
-
 lemma (in prob_space) finite_variables_absolutely_continuous:
   assumes X: "finite_random_variable S X" and Y: "finite_random_variable T Y"
   shows "measure_space.absolutely_continuous (sigma (pair_algebra S T))
@@ -330,16 +262,6 @@
   qed
 qed
 
-lemma (in information_space) mutual_information_commute:
-  assumes X: "finite_random_variable S X" and Y: "finite_random_variable T Y"
-  shows "mutual_information b S T X Y = mutual_information b T S Y X"
-  by (intro finite_random_variableD X Y mutual_information_commute_generic finite_variables_absolutely_continuous)
-
-lemma (in information_space) mutual_information_commute_simple:
-  assumes X: "simple_function X" and Y: "simple_function Y"
-  shows "\<I>(X;Y) = \<I>(Y;X)"
-  by (intro X Y simple_function_imp_finite_random_variable mutual_information_commute)
-
 lemma (in information_space)
   assumes MX: "finite_random_variable MX X"
   assumes MY: "finite_random_variable MY Y"
@@ -371,6 +293,18 @@
     unfolding mutual_information_def .
 qed
 
+lemma (in information_space) mutual_information_commute:
+  assumes X: "finite_random_variable S X" and Y: "finite_random_variable T Y"
+  shows "mutual_information b S T X Y = mutual_information b T S Y X"
+  unfolding mutual_information_generic_eq[OF X Y] mutual_information_generic_eq[OF Y X]
+  unfolding joint_distribution_commute_singleton[of X Y]
+  by (auto simp add: ac_simps intro!: setsum_reindex_cong[OF swap_inj_on])
+
+lemma (in information_space) mutual_information_commute_simple:
+  assumes X: "simple_function X" and Y: "simple_function Y"
+  shows "\<I>(X;Y) = \<I>(Y;X)"
+  by (intro X Y simple_function_imp_finite_random_variable mutual_information_commute)
+
 lemma (in information_space) mutual_information_eq:
   assumes "simple_function X" "simple_function Y"
   shows "\<I>(X;Y) = (\<Sum> (x,y) \<in> X ` space M \<times> Y ` space M.
diff -r 1eef159301df -r 621fa31e1dbd src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Jan 21 10:43:09 2011 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue Jan 25 09:45:45 2011 +0100
@@ -471,20 +471,26 @@
   unfolding sigma_algebra.simple_function_def[OF N_subalgebra(3)]
   by auto
 
-lemma (in sigma_algebra) simple_function_vimage:
-  fixes g :: "'a \<Rightarrow> pextreal" and f :: "'d \<Rightarrow> 'a"
-  assumes g: "simple_function g" and f: "f \<in> S \<rightarrow> space M"
-  shows "sigma_algebra.simple_function (vimage_algebra S f) (\<lambda>x. g (f x))"
-proof -
-  have subset: "(\<lambda>x. g (f x)) ` S \<subseteq> g ` space M"
-    using f by auto
-  interpret V: sigma_algebra "vimage_algebra S f"
-    using f by (rule sigma_algebra_vimage)
-  show ?thesis using g
-    unfolding simple_function_eq_borel_measurable
-    unfolding V.simple_function_eq_borel_measurable
-    using measurable_vimage[OF _ f, of g borel]
-    using finite_subset[OF subset] by auto
+lemma (in measure_space) simple_function_vimage:
+  assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
+    and f: "sigma_algebra.simple_function M' f"
+  shows "simple_function (\<lambda>x. f (T x))"
+proof (intro simple_function_def[THEN iffD2] conjI ballI)
+  interpret T: sigma_algebra M' by fact
+  have "(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'"
+    using T unfolding measurable_def by auto
+  then show "finite ((\<lambda>x. f (T x)) ` space M)"
+    using f unfolding T.simple_function_def by (auto intro: finite_subset)
+  fix i assume i: "i \<in> (\<lambda>x. f (T x)) ` space M"
+  then have "i \<in> f ` space M'"
+    using T unfolding measurable_def by auto
+  then have "f -` {i} \<inter> space M' \<in> sets M'"
+    using f unfolding T.simple_function_def by auto
+  then have "T -` (f -` {i} \<inter> space M') \<inter> space M \<in> sets M"
+    using T unfolding measurable_def by auto
+  also have "T -` (f -` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) -` {i} \<inter> space M"
+    using T unfolding measurable_def by auto
+  finally show "(\<lambda>x. f (T x)) -` {i} \<inter> space M \<in> sets M" .
 qed
 
 section "Simple integral"
@@ -816,28 +822,30 @@
   unfolding measure_space.simple_integral_def_raw[OF N] by simp
 
 lemma (in measure_space) simple_integral_vimage:
-  fixes g :: "'a \<Rightarrow> pextreal" and f :: "'d \<Rightarrow> 'a"
-  assumes f: "bij_betw f S (space M)"
-  shows "simple_integral g =
-         measure_space.simple_integral (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>x. g (f x))"
-    (is "_ = measure_space.simple_integral ?T ?\<mu> _")
+  assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
+    and f: "sigma_algebra.simple_function M' f"
+  shows "measure_space.simple_integral M' (\<lambda>A. \<mu> (T -` A \<inter> space M)) f = (\<integral>\<^isup>S x. f (T x))"
+    (is "measure_space.simple_integral M' ?nu f = _")
 proof -
-  from f interpret T: measure_space ?T ?\<mu> by (rule measure_space_isomorphic)
-  have surj: "f`S = space M"
-    using f unfolding bij_betw_def by simp
-  have *: "(\<lambda>x. g (f x)) ` S = g ` f ` S" by auto
-  have **: "f`S = space M" using f unfolding bij_betw_def by auto
-  { fix x assume "x \<in> space M"
-    have "(f ` ((\<lambda>x. g (f x)) -` {g x} \<inter> S)) =
-      (f ` (f -` (g -` {g x}) \<inter> S))" by auto
-    also have "f -` (g -` {g x}) \<inter> S = f -` (g -` {g x} \<inter> space M) \<inter> S"
-      using f unfolding bij_betw_def by auto
-    also have "(f ` (f -` (g -` {g x} \<inter> space M) \<inter> S)) = g -` {g x} \<inter> space M"
-      using ** by (intro image_vimage_inter_eq) auto
-    finally have "(f ` ((\<lambda>x. g (f x)) -` {g x} \<inter> S)) = g -` {g x} \<inter> space M" by auto }
-  then show ?thesis using assms
-    unfolding simple_integral_def T.simple_integral_def bij_betw_def
-    by (auto simp add: * intro!: setsum_cong)
+  interpret T: measure_space M' ?nu using T by (rule measure_space_vimage) auto
+  show "T.simple_integral f = (\<integral>\<^isup>S x. f (T x))"
+    unfolding simple_integral_def T.simple_integral_def
+  proof (intro setsum_mono_zero_cong_right ballI)
+    show "(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'"
+      using T unfolding measurable_def by auto
+    show "finite (f ` space M')"
+      using f unfolding T.simple_function_def by auto
+  next
+    fix i assume "i \<in> f ` space M' - (\<lambda>x. f (T x)) ` space M"
+    then have "T -` (f -` {i} \<inter> space M') \<inter> space M = {}" by (auto simp: image_iff)
+    then show "i * \<mu> (T -` (f -` {i} \<inter> space M') \<inter> space M) = 0" by simp
+  next
+    fix i assume "i \<in> (\<lambda>x. f (T x)) ` space M"
+    then have "T -` (f -` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) -` {i} \<inter> space M"
+      using T unfolding measurable_def by auto
+    then show "i * \<mu> (T -` (f -` {i} \<inter> space M') \<inter> space M) = i * \<mu> ((\<lambda>x. f (T x)) -` {i} \<inter> space M)"
+      by auto
+  qed
 qed
 
 section "Continuous posititve integration"
@@ -1016,71 +1024,6 @@
   shows "f ` A = g ` B"
   using assms by blast
 
-lemma (in measure_space) positive_integral_vimage:
-  fixes g :: "'a \<Rightarrow> pextreal" and f :: "'d \<Rightarrow> 'a"
-  assumes f: "bij_betw f S (space M)"
-  shows "positive_integral g =
-         measure_space.positive_integral (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>x. g (f x))"
-    (is "_ = measure_space.positive_integral ?T ?\<mu> _")
-proof -
-  from f interpret T: measure_space ?T ?\<mu> by (rule measure_space_isomorphic)
-  have f_fun: "f \<in> S \<rightarrow> space M" using assms unfolding bij_betw_def by auto
-  from assms have inv: "bij_betw (the_inv_into S f) (space M) S"
-    by (rule bij_betw_the_inv_into)
-  then have inv_fun: "the_inv_into S f \<in> space M \<rightarrow> S" unfolding bij_betw_def by auto
-  have surj: "f`S = space M"
-    using f unfolding bij_betw_def by simp
-  have inj: "inj_on f S"
-    using f unfolding bij_betw_def by simp
-  have inv_f: "\<And>x. x \<in> space M \<Longrightarrow> f (the_inv_into S f x) = x"
-    using f_the_inv_into_f[of f S] f unfolding bij_betw_def by auto
-  from simple_integral_vimage[OF assms, symmetric]
-  have *: "simple_integral = T.simple_integral \<circ> (\<lambda>g. g \<circ> f)" by (simp add: comp_def)
-  show ?thesis
-    unfolding positive_integral_alt1 T.positive_integral_alt1 SUPR_def * image_compose
-  proof (safe intro!: arg_cong[where f=Sup] image_set_cong, simp_all add: comp_def)
-    fix g' :: "'a \<Rightarrow> pextreal" assume "simple_function g'" "\<forall>x\<in>space M. g' x \<le> g x \<and> g' x \<noteq> \<omega>"
-    then show "\<exists>h. T.simple_function h \<and> (\<forall>x\<in>S. h x \<le> g (f x) \<and> h x \<noteq> \<omega>) \<and>
-                   T.simple_integral (\<lambda>x. g' (f x)) = T.simple_integral h"
-      using f unfolding bij_betw_def
-      by (auto intro!: exI[of _ "\<lambda>x. g' (f x)"]
-               simp add: le_fun_def simple_function_vimage[OF _ f_fun])
-  next
-    fix g' :: "'d \<Rightarrow> pextreal" assume g': "T.simple_function g'" "\<forall>x\<in>S. g' x \<le> g (f x) \<and> g' x \<noteq> \<omega>"
-    let ?g = "\<lambda>x. g' (the_inv_into S f x)"
-    show "\<exists>h. simple_function h \<and> (\<forall>x\<in>space M. h x \<le> g x \<and> h x \<noteq> \<omega>) \<and>
-              T.simple_integral g' = T.simple_integral (\<lambda>x. h (f x))"
-    proof (intro exI[of _ ?g] conjI ballI)
-      { fix x assume x: "x \<in> space M"
-        then have "the_inv_into S f x \<in> S" using inv_fun by auto
-        with g' have "g' (the_inv_into S f x) \<le> g (f (the_inv_into S f x)) \<and> g' (the_inv_into S f x) \<noteq> \<omega>"
-          by auto
-        then show "g' (the_inv_into S f x) \<le> g x" "g' (the_inv_into S f x) \<noteq> \<omega>"
-          using f_the_inv_into_f[of f S x] x f unfolding bij_betw_def by auto }
-      note vimage_vimage_inv[OF f inv_f inv_fun, simp]
-      from T.simple_function_vimage[OF g'(1), unfolded space_vimage_algebra, OF inv_fun]
-      show "simple_function (\<lambda>x. g' (the_inv_into S f x))"
-        unfolding simple_function_def by (simp add: simple_function_def)
-      show "T.simple_integral g' = T.simple_integral (\<lambda>x. ?g (f x))"
-        using the_inv_into_f_f[OF inj] by (auto intro!: T.simple_integral_cong)
-    qed
-  qed
-qed
-
-lemma (in measure_space) positive_integral_vimage_inv:
-  fixes g :: "'d \<Rightarrow> pextreal" and f :: "'d \<Rightarrow> 'a"
-  assumes f: "bij_inv S (space M) f h"
-  shows "measure_space.positive_integral (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) g =
-      (\<integral>\<^isup>+x. g (h x))"
-proof -
-  interpret v: measure_space "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
-    using f by (rule measure_space_isomorphic[OF bij_inv_bij_betw(1)])
-  show ?thesis
-    unfolding positive_integral_vimage[OF f[THEN bij_inv_bij_betw(1)], of "\<lambda>x. g (h x)"]
-    using f[unfolded bij_inv_def]
-    by (auto intro!: v.positive_integral_cong)
-qed
-
 lemma (in measure_space) positive_integral_SUP_approx:
   assumes "f \<up> s"
   and f: "\<And>i. f i \<in> borel_measurable M"
@@ -1245,6 +1188,23 @@
   using positive_integral_isoton[OF `f \<up> u` e(1)[THEN borel_measurable_simple_function]]
   unfolding positive_integral_eq_simple_integral[OF e] .
 
+lemma (in measure_space) positive_integral_vimage:
+  assumes T: "sigma_algebra M'" "T \<in> measurable M M'" and f: "f \<in> borel_measurable M'"
+  shows "measure_space.positive_integral M' (\<lambda>A. \<mu> (T -` A \<inter> space M)) f = (\<integral>\<^isup>+ x. f (T x))"
+    (is "measure_space.positive_integral M' ?nu f = _")
+proof -
+  interpret T: measure_space M' ?nu using T by (rule measure_space_vimage) auto
+  obtain f' where f': "f' \<up> f" "\<And>i. T.simple_function (f' i)"
+    using T.borel_measurable_implies_simple_function_sequence[OF f] by blast
+  then have f: "(\<lambda>i x. f' i (T x)) \<up> (\<lambda>x. f (T x))" "\<And>i. simple_function (\<lambda>x. f' i (T x))"
+    using simple_function_vimage[OF T] unfolding isoton_fun_expand by auto
+  show "T.positive_integral f = (\<integral>\<^isup>+ x. f (T x))"
+    using positive_integral_isoton_simple[OF f]
+    using T.positive_integral_isoton_simple[OF f']
+    unfolding simple_integral_vimage[OF T f'(2)] isoton_def
+    by simp
+qed
+
 lemma (in measure_space) positive_integral_linear:
   assumes f: "f \<in> borel_measurable M"
   and g: "g \<in> borel_measurable M"
@@ -1614,21 +1574,21 @@
   thus ?thesis by (simp del: Real_eq_0 add: integral_def)
 qed
 
-lemma (in measure_space) integral_vimage_inv:
-  assumes f: "bij_betw f S (space M)"
-  shows "measure_space.integral (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>x. g x) = (\<integral>x. g (the_inv_into S f x))"
+lemma (in measure_space) integral_vimage:
+  assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
+  assumes f: "measure_space.integrable M' (\<lambda>A. \<mu> (T -` A \<inter> space M)) f"
+  shows "integrable (\<lambda>x. f (T x))" (is ?P)
+    and "measure_space.integral M' (\<lambda>A. \<mu> (T -` A \<inter> space M)) f = (\<integral>x. f (T x))" (is ?I)
 proof -
-  interpret v: measure_space "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
-    using f by (rule measure_space_isomorphic)
-  have "\<And>x. x \<in> space (vimage_algebra S f) \<Longrightarrow> the_inv_into S f (f x) = x"
-    using f[unfolded bij_betw_def] by (simp add: the_inv_into_f_f)
-  then have *: "v.positive_integral (\<lambda>x. Real (g (the_inv_into S f (f x)))) = v.positive_integral (\<lambda>x. Real (g x))"
-     "v.positive_integral (\<lambda>x. Real (- g (the_inv_into S f (f x)))) = v.positive_integral (\<lambda>x. Real (- g x))"
-    by (auto intro!: v.positive_integral_cong)
-  show ?thesis
-    unfolding integral_def v.integral_def
-    unfolding positive_integral_vimage[OF f]
-    by (simp add: *)
+  interpret T: measure_space M' "\<lambda>A. \<mu> (T -` A \<inter> space M)"
+    using T by (rule measure_space_vimage) auto
+  from measurable_comp[OF T(2), of f borel]
+  have borel: "(\<lambda>x. Real (f x)) \<in> borel_measurable M'" "(\<lambda>x. Real (- f x)) \<in> borel_measurable M'"
+    and "(\<lambda>x. f (T x)) \<in> borel_measurable M"
+    using f unfolding T.integrable_def by (auto simp: comp_def)
+  then show ?P ?I
+    using f unfolding T.integral_def integral_def T.integrable_def integrable_def
+    unfolding borel[THEN positive_integral_vimage[OF T]] by auto
 qed
 
 lemma (in measure_space) integral_minus[intro, simp]:
diff -r 1eef159301df -r 621fa31e1dbd src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Fri Jan 21 10:43:09 2011 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Tue Jan 25 09:45:45 2011 +0100
@@ -45,6 +45,8 @@
 definition lebesgue :: "'a::ordered_euclidean_space algebra" where
   "lebesgue = \<lparr> space = UNIV, sets = {A. \<forall>n. (indicator A :: 'a \<Rightarrow> real) integrable_on cube n} \<rparr>"
 
+definition "lmeasure A = (SUP n. Real (integral (cube n) (indicator A)))"
+
 lemma space_lebesgue[simp]: "space lebesgue = UNIV"
   unfolding lebesgue_def by simp
 
@@ -104,8 +106,6 @@
   qed (auto intro: LIMSEQ_indicator_UN simp: cube_def)
 qed simp
 
-definition "lmeasure A = (SUP n. Real (integral (cube n) (indicator A)))"
-
 interpretation lebesgue: measure_space lebesgue lmeasure
 proof
   have *: "indicator {} = (\<lambda>x. 0 :: real)" by (simp add: fun_eq_iff)
@@ -736,6 +736,21 @@
   show "p2e \<in> ?P \<rightarrow> ?U" "e2p \<in> ?U \<rightarrow> ?P" by (auto simp: e2p_def)
 qed auto
 
+declare restrict_extensional[intro]
+
+lemma e2p_extensional[intro]:"e2p (y::'a::ordered_euclidean_space) \<in> extensional {..<DIM('a)}"
+  unfolding e2p_def by auto
+
+lemma e2p_image_vimage: fixes A::"'a::ordered_euclidean_space set"
+  shows "e2p ` A = p2e -` A \<inter> extensional {..<DIM('a)}"
+proof(rule set_eqI,rule)
+  fix x assume "x \<in> e2p ` A" then guess y unfolding image_iff .. note y=this
+  show "x \<in> p2e -` A \<inter> extensional {..<DIM('a)}"
+    apply safe apply(rule vimageI[OF _ y(1)]) unfolding y p2e_e2p by auto
+next fix x assume "x \<in> p2e -` A \<inter> extensional {..<DIM('a)}"
+  thus "x \<in> e2p ` A" unfolding image_iff apply(rule_tac x="p2e x" in bexI) apply(subst e2p_p2e) by auto
+qed
+
 interpretation borel_product: product_sigma_finite "\<lambda>x. borel::real algebra" "\<lambda>x. lmeasure"
   by default
 
@@ -767,6 +782,14 @@
   then show "e2p -` A \<inter> space ?E \<in> sets ?E" by simp
 qed
 
+lemma measurable_e2p:
+  "e2p \<in> measurable (borel::'a algebra)
+                    (sigma (product_algebra (\<lambda>x. borel :: real algebra) {..<DIM('a::ordered_euclidean_space)}))"
+  using measurable_e2p_on_generator[where 'a='a] unfolding borel_eq_lessThan
+  by (subst sigma_product_algebra_sigma_eq[where S="\<lambda>_ i. {..<real i}"])
+     (auto intro!: measurable_sigma_sigma isotoneI real_arch_lt
+           simp: product_algebra_def)
+
 lemma measurable_p2e_on_generator:
   "p2e \<in> measurable
     (product_algebra
@@ -785,33 +808,13 @@
   then show "p2e -` A \<inter> space ?P \<in> sets ?P" by auto
 qed
 
-lemma borel_vimage_algebra_eq:
-  defines "F \<equiv> product_algebra (\<lambda>x. \<lparr> space = (UNIV::real set), sets = range lessThan \<rparr>) {..<DIM('a::ordered_euclidean_space)}"
-  shows "sigma_algebra.vimage_algebra (borel::'a::ordered_euclidean_space algebra) (space (sigma F)) p2e = sigma F"
-  unfolding borel_eq_lessThan
-proof (intro vimage_algebra_sigma)
-  let ?E = "\<lparr>space = (UNIV::'a set), sets = range lessThan\<rparr>"
-  show "bij_inv (space (sigma F)) (space (sigma ?E)) p2e e2p"
-    using bij_inv_p2e_e2p unfolding F_def by simp
-  show "sets F \<subseteq> Pow (space F)" "sets ?E \<subseteq> Pow (space ?E)" unfolding F_def
-    by (intro product_algebra_sets_into_space) auto
-  show "p2e \<in> measurable F ?E"
-    "e2p \<in> measurable ?E F"
-    unfolding F_def using measurable_p2e_on_generator measurable_e2p_on_generator by auto
-qed
-
-lemma product_borel_eq_vimage:
-  "sigma (product_algebra (\<lambda>x. borel) {..<DIM('a::ordered_euclidean_space)}) =
-  sigma_algebra.vimage_algebra borel (extensional {..<DIM('a)})
-  (p2e:: _ \<Rightarrow> 'a::ordered_euclidean_space)"
-  unfolding borel_vimage_algebra_eq[simplified]
-  unfolding borel_eq_lessThan
-  apply(subst sigma_product_algebra_sigma_eq[where S="\<lambda>i. \<lambda>n. lessThan (real n)"])
-  unfolding lessThan_iff
-proof- fix i assume i:"i<DIM('a)"
-  show "(\<lambda>n. {..<real n}) \<up> space \<lparr>space = UNIV, sets = range lessThan\<rparr>"
-    by(auto intro!:real_arch_lt isotoneI)
-qed auto
+lemma measurable_p2e:
+  "p2e \<in> measurable (sigma (product_algebra (\<lambda>x. borel :: real algebra) {..<DIM('a::ordered_euclidean_space)}))
+                    (borel::'a algebra)"
+  using measurable_p2e_on_generator[where 'a='a] unfolding borel_eq_lessThan
+  by (subst sigma_product_algebra_sigma_eq[where S="\<lambda>_ i. {..<real i}"])
+     (auto intro!: measurable_sigma_sigma isotoneI real_arch_lt
+           simp: product_algebra_def)
 
 lemma e2p_Int:"e2p ` A \<inter> e2p ` B = e2p ` (A \<inter> B)" (is "?L = ?R")
   apply(rule image_Int[THEN sym])
@@ -834,42 +837,12 @@
   unfolding Int_stable_def algebra.select_convs
   apply safe unfolding inter_interval by auto
 
-lemma inj_on_disjoint_family_on: assumes "disjoint_family_on A S" "inj f"
-  shows "disjoint_family_on (\<lambda>x. f ` A x) S"
-  unfolding disjoint_family_on_def
-proof(rule,rule,rule)
-  fix x1 x2 assume x:"x1 \<in> S" "x2 \<in> S" "x1 \<noteq> x2"
-  show "f ` A x1 \<inter> f ` A x2 = {}"
-  proof(rule ccontr) case goal1
-    then obtain z where z:"z \<in> f ` A x1 \<inter> f ` A x2" by auto
-    then obtain z1 z2 where z12:"z1 \<in> A x1" "z2 \<in> A x2" "f z1 = z" "f z2 = z" by auto
-    hence "z1 = z2" using assms(2) unfolding inj_on_def by blast
-    hence "x1 = x2" using z12(1-2) using assms[unfolded disjoint_family_on_def] using x by auto
-    thus False using x(3) by auto
-  qed
-qed
-
-declare restrict_extensional[intro]
-
-lemma e2p_extensional[intro]:"e2p (y::'a::ordered_euclidean_space) \<in> extensional {..<DIM('a)}"
-  unfolding e2p_def by auto
-
-lemma e2p_image_vimage: fixes A::"'a::ordered_euclidean_space set"
-  shows "e2p ` A = p2e -` A \<inter> extensional {..<DIM('a)}"
-proof(rule set_eqI,rule)
-  fix x assume "x \<in> e2p ` A" then guess y unfolding image_iff .. note y=this
-  show "x \<in> p2e -` A \<inter> extensional {..<DIM('a)}"
-    apply safe apply(rule vimageI[OF _ y(1)]) unfolding y p2e_e2p by auto
-next fix x assume "x \<in> p2e -` A \<inter> extensional {..<DIM('a)}"
-  thus "x \<in> e2p ` A" unfolding image_iff apply(rule_tac x="p2e x" in bexI) apply(subst e2p_p2e) by auto
-qed
-
 lemma lmeasure_measure_eq_borel_prod:
   fixes A :: "('a::ordered_euclidean_space) set"
   assumes "A \<in> sets borel"
   shows "lmeasure A = borel_product.product_measure {..<DIM('a)} (e2p ` A :: (nat \<Rightarrow> real) set)"
 proof (rule measure_unique_Int_stable[where X=A and A=cube])
-  interpret fprod: finite_product_sigma_finite "\<lambda>x. borel" "\<lambda>x. lmeasure" "{..<DIM('a)}" by default auto
+  interpret fprod: finite_product_sigma_finite "\<lambda>x. borel :: real algebra" "\<lambda>x. lmeasure" "{..<DIM('a)}" by default auto
   show "Int_stable \<lparr> space = UNIV :: 'a set, sets = range (\<lambda>(a,b). {a..b}) \<rparr>"
     (is "Int_stable ?E" ) using Int_stable_cuboids' .
   show "borel = sigma ?E" using borel_eq_atLeastAtMost .
@@ -906,64 +879,19 @@
   show "measure_space borel lmeasure" by default
   show "measure_space borel
      (\<lambda>a::'a set. finite_product_sigma_finite.measure (\<lambda>x. borel) (\<lambda>x. lmeasure) {..<DIM('a)} (e2p ` a))"
-    apply default unfolding countably_additive_def
-  proof safe fix A::"nat \<Rightarrow> 'a set" assume A:"range A \<subseteq> sets borel" "disjoint_family A"
-      "(\<Union>i. A i) \<in> sets borel"
-    note fprod.ca[unfolded countably_additive_def,rule_format]
-    note ca = this[of "\<lambda> n. e2p ` (A n)"]
-    show "(\<Sum>\<^isub>\<infinity>n. finite_product_sigma_finite.measure
-        (\<lambda>x. borel) (\<lambda>x. lmeasure) {..<DIM('a)} (e2p ` A n)) =
-           finite_product_sigma_finite.measure (\<lambda>x. borel)
-            (\<lambda>x. lmeasure) {..<DIM('a)} (e2p ` (\<Union>i. A i))" unfolding image_UN
-    proof(rule ca) show "range (\<lambda>n. e2p ` A n) \<subseteq> sets
-       (sigma (product_algebra (\<lambda>x. borel) {..<DIM('a)}))"
-        unfolding product_borel_eq_vimage
-      proof case goal1
-        then guess y unfolding image_iff .. note y=this(2)
-        show ?case unfolding borel.in_vimage_algebra y apply-
-          apply(rule_tac x="A y" in bexI,rule e2p_image_vimage)
-          using A(1) by auto
-      qed
-
-      show "disjoint_family (\<lambda>n. e2p ` A n)" apply(rule inj_on_disjoint_family_on)
-        using bij_inv_p2e_e2p[THEN bij_inv_bij_betw(2)] using A(2) unfolding bij_betw_def by auto
-      show "(\<Union>n. e2p ` A n) \<in> sets (sigma (product_algebra (\<lambda>x. borel) {..<DIM('a)}))"
-        unfolding product_borel_eq_vimage borel.in_vimage_algebra
-      proof(rule bexI[OF _ A(3)],rule set_eqI,rule)
-        fix x assume x:"x \<in> (\<Union>n. e2p ` A n)" hence "p2e x \<in> (\<Union>i. A i)" by auto
-        moreover have "x \<in> extensional {..<DIM('a)}"
-          using x unfolding extensional_def e2p_def_raw by auto
-        ultimately show "x \<in> p2e -` (\<Union>i. A i) \<inter> extensional {..<DIM('a)}" by auto
-      next fix x assume x:"x \<in> p2e -` (\<Union>i. A i) \<inter> extensional {..<DIM('a)}"
-        hence "p2e x \<in> (\<Union>i. A i)" by auto
-        hence "\<exists>n. x \<in> e2p ` A n" apply safe apply(rule_tac x=i in exI)
-          unfolding image_iff apply(rule_tac x="p2e x" in bexI)
-          apply(subst e2p_p2e) using x by auto
-        thus "x \<in> (\<Union>n. e2p ` A n)" by auto
-      qed
-    qed
-  qed auto
+  proof (rule fprod.measure_space_vimage)
+    show "sigma_algebra borel" by default
+    show "(p2e :: (nat \<Rightarrow> real) \<Rightarrow> 'a) \<in> measurable fprod.P borel" by (rule measurable_p2e)
+    fix A :: "'a set" assume "A \<in> sets borel"
+    show "fprod.measure (e2p ` A) = fprod.measure (p2e -` A \<inter> space fprod.P)"
+      by (simp add: e2p_image_vimage)
+  qed
 qed
 
-lemma e2p_p2e'[simp]: fixes x::"'a::ordered_euclidean_space"
-  assumes "A \<subseteq> extensional {..<DIM('a)}"
-  shows "e2p ` (p2e ` A ::'a set) = A"
-  apply(rule set_eqI) unfolding image_iff Bex_def apply safe defer
-  apply(rule_tac x="p2e x" in exI,safe) using assms by auto
-
-lemma range_p2e:"range (p2e::_\<Rightarrow>'a::ordered_euclidean_space) = UNIV"
-  apply safe defer unfolding image_iff apply(rule_tac x="\<lambda>i. x $$ i" in bexI)
-  unfolding p2e_def by auto
-
-lemma p2e_inv_extensional:"(A::'a::ordered_euclidean_space set)
-  = p2e ` (p2e -` A \<inter> extensional {..<DIM('a)})"
-  unfolding p2e_def_raw apply safe unfolding image_iff
-proof- fix x assume "x\<in>A"
-  let ?y = "\<lambda>i. if i<DIM('a) then x$$i else undefined"
-  have *:"Chi ?y = x" apply(subst euclidean_eq) by auto
-  show "\<exists>xa\<in>Chi -` A \<inter> extensional {..<DIM('a)}. x = Chi xa" apply(rule_tac x="?y" in bexI)
-    apply(subst euclidean_eq) unfolding extensional_def using `x\<in>A` by(auto simp: *)
-qed
+lemma range_e2p:"range (e2p::'a::ordered_euclidean_space \<Rightarrow> _) = extensional {..<DIM('a)}"
+  unfolding e2p_def_raw
+  apply auto
+  by (rule_tac x="\<chi>\<chi> i. x i" in image_eqI) (auto simp: fun_eq_iff extensional_def)
 
 lemma borel_fubini_positiv_integral:
   fixes f :: "'a::ordered_euclidean_space \<Rightarrow> pextreal"
@@ -972,22 +900,27 @@
           borel_product.product_positive_integral {..<DIM('a)} (f \<circ> p2e)"
 proof- def U \<equiv> "extensional {..<DIM('a)} :: (nat \<Rightarrow> real) set"
   interpret fprod: finite_product_sigma_finite "\<lambda>x. borel" "\<lambda>x. lmeasure" "{..<DIM('a)}" by default auto
-  have *:"sigma_algebra.vimage_algebra borel U (p2e:: _ \<Rightarrow> 'a)
-    = sigma (product_algebra (\<lambda>x. borel) {..<DIM('a)})"
-    unfolding U_def product_borel_eq_vimage[symmetric] ..
   show ?thesis
-    unfolding borel.positive_integral_vimage[unfolded space_borel, OF bij_inv_p2e_e2p[THEN bij_inv_bij_betw(1)]]
-    apply(subst fprod.positive_integral_cong_measure[THEN sym, of "\<lambda>A. lmeasure (p2e ` A)"])
-    unfolding U_def[symmetric] *[THEN sym] o_def
-  proof- fix A assume A:"A \<in> sets (sigma_algebra.vimage_algebra borel U (p2e ::_ \<Rightarrow> 'a))"
-    hence *:"A \<subseteq> extensional {..<DIM('a)}" unfolding U_def by auto
-    from A guess B unfolding borel.in_vimage_algebra U_def ..
-    then have "(p2e ` A::'a set) \<in> sets borel"
-      by (simp add: p2e_inv_extensional[of B, symmetric])
-    from lmeasure_measure_eq_borel_prod[OF this] show "lmeasure (p2e ` A::'a set) =
-      finite_product_sigma_finite.measure (\<lambda>x. borel) (\<lambda>x. lmeasure) {..<DIM('a)} A"
-      unfolding e2p_p2e'[OF *] .
-  qed auto
+  proof (subst borel.positive_integral_vimage[symmetric, of _ "e2p :: 'a \<Rightarrow> _" "(\<lambda>x. f (p2e x))", unfolded p2e_e2p])
+    show "(e2p :: 'a \<Rightarrow> _) \<in> measurable borel fprod.P" by (rule measurable_e2p)
+    show "sigma_algebra fprod.P" by default
+    from measurable_comp[OF measurable_p2e f]
+    show "(\<lambda>x. f (p2e x)) \<in> borel_measurable fprod.P" by (simp add: comp_def)
+    let "?L A" = "lmeasure ((e2p::'a \<Rightarrow> (nat \<Rightarrow> real)) -` A \<inter> space borel)"
+    show "measure_space.positive_integral fprod.P ?L (\<lambda>x. f (p2e x)) =
+      fprod.positive_integral (f \<circ> p2e)"
+      unfolding comp_def
+    proof (rule fprod.positive_integral_cong_measure)
+      fix A :: "(nat \<Rightarrow> real) set" assume "A \<in> sets fprod.P"
+      then have A: "(e2p::'a \<Rightarrow> (nat \<Rightarrow> real)) -` A \<inter> space borel \<in> sets borel"
+        by (rule measurable_sets[OF measurable_e2p])
+      have [simp]: "A \<inter> extensional {..<DIM('a)} = A"
+        using `A \<in> sets fprod.P`[THEN fprod.sets_into_space] by auto
+      show "?L A = fprod.measure A"
+        unfolding lmeasure_measure_eq_borel_prod[OF A]
+        by (simp add: range_e2p)
+    qed
+  qed
 qed
 
 lemma borel_fubini:
diff -r 1eef159301df -r 621fa31e1dbd src/HOL/Probability/Measure.thy
--- a/src/HOL/Probability/Measure.thy	Fri Jan 21 10:43:09 2011 +0100
+++ b/src/HOL/Probability/Measure.thy	Tue Jan 25 09:45:45 2011 +0100
@@ -525,6 +525,15 @@
   qed
 qed
 
+lemma True
+proof
+  fix x a b :: nat
+  have "\<And>x a b :: int. x dvd a \<Longrightarrow> x dvd (a + b) \<Longrightarrow> x dvd b"
+    by (metis dvd_mult_div_cancel zadd_commute zdvd_reduce)
+  then have "x dvd a \<Longrightarrow> x dvd (a + b) \<Longrightarrow> x dvd b"
+    unfolding zdvd_int[of x] zadd_int[symmetric] .
+qed
+
 lemma measure_unique_Int_stable:
   fixes M E :: "'a algebra" and A :: "nat \<Rightarrow> 'a set"
   assumes "Int_stable E" "M = sigma E"
@@ -608,45 +617,6 @@
   ultimately show ?thesis by (simp add: isoton_def)
 qed
 
-section "Isomorphisms between measure spaces"
-
-lemma (in measure_space) measure_space_isomorphic:
-  fixes f :: "'c \<Rightarrow> 'a"
-  assumes "bij_betw f S (space M)"
-  shows "measure_space (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A))"
-    (is "measure_space ?T ?\<mu>")
-proof -
-  have "f \<in> S \<rightarrow> space M" using assms unfolding bij_betw_def by auto
-  then interpret T: sigma_algebra ?T by (rule sigma_algebra_vimage)
-  show ?thesis
-  proof
-    show "\<mu> (f`{}) = 0" by simp
-    show "countably_additive ?T (\<lambda>A. \<mu> (f ` A))"
-    proof (unfold countably_additive_def, intro allI impI)
-      fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets ?T" "disjoint_family A"
-      then have "\<forall>i. \<exists>F'. F' \<in> sets M \<and> A i = f -` F' \<inter> S"
-        by (auto simp: image_iff image_subset_iff Bex_def vimage_algebra_def)
-      from choice[OF this] obtain F where F: "\<And>i. F i \<in> sets M" and A: "\<And>i. A i = f -` F i \<inter> S" by auto
-      then have [simp]: "\<And>i. f ` (A i) = F i"
-        using sets_into_space assms
-        by (force intro!: image_vimage_inter_eq[where T="space M"] simp: bij_betw_def)
-      have "disjoint_family F"
-      proof (intro disjoint_family_on_bisimulation[OF `disjoint_family A`])
-        fix n m assume "A n \<inter> A m = {}"
-        then have "f -` (F n \<inter> F m) \<inter> S = {}" unfolding A by auto
-        moreover
-        have "F n \<in> sets M" "F m \<in> sets M" using F by auto
-        then have "f`S = space M" "F n \<inter> F m \<subseteq> space M"
-          using sets_into_space assms by (auto simp: bij_betw_def)
-        note image_vimage_inter_eq[OF this, symmetric]
-        ultimately show "F n \<inter> F m = {}" by simp
-      qed
-      with F show "(\<Sum>\<^isub>\<infinity> i. \<mu> (f ` A i)) = \<mu> (f ` (\<Union>i. A i))"
-        by (auto simp add: image_UN intro!: measure_countably_additive)
-    qed
-  qed
-qed
-
 section "@{text \<mu>}-null sets"
 
 abbreviation (in measure_space) "null_sets \<equiv> {N\<in>sets M. \<mu> N = 0}"
@@ -803,23 +773,17 @@
 lemma (in measure_space) AE_conjI:
   assumes AE_P: "AE x. P x" and AE_Q: "AE x. Q x"
   shows "AE x. P x \<and> Q x"
-proof -
-  from AE_P obtain A where P: "{x\<in>space M. \<not> P x} \<subseteq> A"
-    and A: "A \<in> sets M" "\<mu> A = 0"
-    by (auto elim!: AE_E)
-
-  from AE_Q obtain B where Q: "{x\<in>space M. \<not> Q x} \<subseteq> B"
-    and B: "B \<in> sets M" "\<mu> B = 0"
-    by (auto elim!: AE_E)
+  apply (rule AE_mp[OF AE_P])
+  apply (rule AE_mp[OF AE_Q])
+  by simp
 
-  show ?thesis
-  proof (intro AE_I)
-    show "A \<union> B \<in> sets M" "\<mu> (A \<union> B) = 0" using A B
-      using measure_subadditive[of A B] by auto
-    show "{x\<in>space M. \<not> (P x \<and> Q x)} \<subseteq> A \<union> B"
-      using P Q by auto
-  qed
-qed
+lemma (in measure_space) AE_conj_iff[simp]:
+  shows "(AE x. P x \<and> Q x) \<longleftrightarrow> (AE x. P x) \<and> (AE x. Q x)"
+proof (intro conjI iffI AE_conjI)
+  assume *: "AE x. P x \<and> Q x"
+  from * show "AE x. P x" by (rule AE_mp) auto
+  from * show "AE x. Q x" by (rule AE_mp) auto
+qed auto
 
 lemma (in measure_space) AE_E2:
   assumes "AE x. P x" "{x\<in>space M. P x} \<in> sets M"
@@ -845,14 +809,6 @@
     by (rule AE_mp[OF AE_space]) auto
 qed
 
-lemma (in measure_space) AE_conj_iff[simp]:
-  shows "(AE x. P x \<and> Q x) \<longleftrightarrow> (AE x. P x) \<and> (AE x. Q x)"
-proof (intro conjI iffI AE_conjI)
-  assume *: "AE x. P x \<and> Q x"
-  from * show "AE x. P x" by (rule AE_mp) auto
-  from * show "AE x. Q x" by (rule AE_mp) auto
-qed auto
-
 lemma (in measure_space) all_AE_countable:
   "(\<forall>i::'i::countable. AE x. P i x) \<longleftrightarrow> (AE x. \<forall>i. P i x)"
 proof
@@ -893,27 +849,28 @@
 
 lemma (in measure_space) measure_space_vimage:
   fixes M' :: "'b algebra"
-  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")
+  assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
+    and \<nu>: "\<And>A. A \<in> sets M' \<Longrightarrow> \<nu> A = \<mu> (T -` A \<inter> space M)"
+  shows "measure_space M' \<nu>"
 proof -
   interpret M': sigma_algebra M' by fact
-
   show ?thesis
   proof
-    show "?T {} = 0" by simp
+    show "\<nu> {} = 0" using \<nu>[of "{}"] by simp
 
-    show "countably_additive M' ?T"
-    proof (unfold countably_additive_def, safe)
+    show "countably_additive M' \<nu>"
+    proof (intro countably_additive_def[THEN iffD2] allI impI)
       fix A :: "nat \<Rightarrow> 'b 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"
+      then have A: "\<And>i. A i \<in> sets M'" "(\<Union>i. A i) \<in> sets M'" by auto
+      then have *: "range (\<lambda>i. T -` (A i) \<inter> space M) \<subseteq> sets M"
+        using `T \<in> measurable M M'` by (auto simp: measurable_def)
+      moreover have "(\<Union>i. T -`  A i \<inter> space M) \<in> sets M"
         using * by blast
-      moreover have **: "disjoint_family (\<lambda>i. f -` A i \<inter> space M)"
+      moreover have **: "disjoint_family (\<lambda>i. T -` 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)
+      ultimately show "(\<Sum>\<^isub>\<infinity> i. \<nu> (A i)) = \<nu> (\<Union>i. A i)"
+        using measure_countably_additive[OF _ **] A
+        by (auto simp: comp_def vimage_UN \<nu>)
     qed
   qed
 qed
@@ -1020,29 +977,6 @@
   qed force+
 qed
 
-lemma (in sigma_finite_measure) sigma_finite_measure_isomorphic:
-  assumes f: "bij_betw f S (space M)"
-  shows "sigma_finite_measure (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A))"
-proof -
-  interpret M: measure_space "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
-    using f by (rule measure_space_isomorphic)
-  show ?thesis
-  proof default
-    from sigma_finite guess A::"nat \<Rightarrow> 'a set" .. note A = this
-    show "\<exists>A::nat\<Rightarrow>'b set. range A \<subseteq> sets (vimage_algebra S f) \<and> (\<Union>i. A i) = space (vimage_algebra S f) \<and> (\<forall>i. \<mu> (f ` A i) \<noteq> \<omega>)"
-    proof (intro exI conjI)
-      show "(\<Union>i::nat. f -` A i \<inter> S) = space (vimage_algebra S f)"
-        using A f[THEN bij_betw_imp_funcset] by (auto simp: vimage_UN[symmetric])
-      show "range (\<lambda>i. f -` A i \<inter> S) \<subseteq> sets (vimage_algebra S f)"
-        using A by (auto simp: vimage_algebra_def)
-      have "\<And>i. f ` (f -` A i \<inter> S) = A i"
-        using f A sets_into_space
-        by (intro image_vimage_inter_eq) (auto simp: bij_betw_def)
-      then show "\<forall>i. \<mu> (f ` (f -` A i \<inter> S)) \<noteq> \<omega>"  using A by simp
-    qed
-  qed
-qed
-
 section "Real measure values"
 
 lemma (in measure_space) real_measure_Union:
diff -r 1eef159301df -r 621fa31e1dbd src/HOL/Probability/Probability_Space.thy
--- a/src/HOL/Probability/Probability_Space.thy	Fri Jan 21 10:43:09 2011 +0100
+++ b/src/HOL/Probability/Probability_Space.thy	Tue Jan 25 09:45:45 2011 +0100
@@ -195,8 +195,8 @@
   assumes "random_variable S X"
   shows "prob_space S (distribution X)"
 proof -
-  interpret S: measure_space S "distribution X"
-    using measure_space_vimage[of X S] assms unfolding distribution_def by simp
+  interpret S: measure_space S "distribution X" unfolding distribution_def
+    using assms by (intro measure_space_vimage) auto
   show ?thesis
   proof
     have "X -` space S \<inter> space M = space M"
diff -r 1eef159301df -r 621fa31e1dbd src/HOL/Probability/Product_Measure.thy
--- a/src/HOL/Probability/Product_Measure.thy	Fri Jan 21 10:43:09 2011 +0100
+++ b/src/HOL/Probability/Product_Measure.thy	Tue Jan 25 09:45:45 2011 +0100
@@ -523,22 +523,6 @@
     unfolding * by (rule measurable_comp)
 qed
 
-lemma (in pair_sigma_algebra) pair_sigma_algebra_swap:
-  "sigma (pair_algebra M2 M1) = (vimage_algebra (space M2 \<times> space M1) (\<lambda>(x, y). (y, x)))"
-  unfolding vimage_algebra_def
-  apply (simp add: sets_sigma)
-  apply (subst sigma_sets_vimage[symmetric])
-  apply (fastsimp simp: pair_algebra_def)
-  using M1.sets_into_space M2.sets_into_space apply (fastsimp simp: pair_algebra_def)
-proof -
-  have "(\<lambda>X. (\<lambda>(x, y). (y, x)) -` X \<inter> space M2 \<times> space M1) ` sets E
-    = sets (pair_algebra M2 M1)" (is "?S = _")
-    by (rule pair_algebra_swap)
-  then show "sigma (pair_algebra M2 M1) = \<lparr>space = space M2 \<times> space M1,
-       sets = sigma_sets (space M2 \<times> space M1) ?S\<rparr>"
-    by (simp add: pair_algebra_def sigma_def)
-qed
-
 definition (in pair_sigma_finite)
   "pair_measure A = M1.positive_integral (\<lambda>x.
     M2.positive_integral (\<lambda>y. indicator A (x, y)))"
@@ -644,6 +628,17 @@
   qed
 qed
 
+lemma (in pair_sigma_algebra) sets_swap:
+  assumes "A \<in> sets P"
+  shows "(\<lambda>(x, y). (y, x)) -` A \<inter> space (sigma (pair_algebra M2 M1)) \<in> sets (sigma (pair_algebra M2 M1))"
+    (is "_ -` A \<inter> space ?Q \<in> sets ?Q")
+proof -
+  have *: "(\<lambda>(x, y). (y, x)) -` A \<inter> space ?Q = (\<lambda>(x, y). (y, x)) ` A"
+    using `A \<in> sets P` sets_into_space by (auto simp: space_pair_algebra)
+  show ?thesis
+    unfolding * using assms by (rule sets_pair_sigma_algebra_swap)
+qed
+
 lemma (in pair_sigma_finite) pair_measure_alt2:
   assumes "A \<in> sets P"
   shows "pair_measure A = M2.positive_integral (\<lambda>y. \<mu>1 ((\<lambda>x. (x, y)) -` A))"
@@ -656,29 +651,20 @@
     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
+    interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
+    have P: "sigma_algebra P" by default
     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
+      apply (rule Q.measure_space_vimage[OF P])
+      apply (rule Q.pair_sigma_algebra_swap_measurable)
+    proof -
+      fix A assume "A \<in> sets P"
+      from sets_swap[OF this]
+      show "M2.positive_integral (\<lambda>y. \<mu>1 ((\<lambda>x. (x, y)) -` A)) =
+            Q.pair_measure ((\<lambda>(x, y). (y, x)) -` A \<inter> space Q.P)"
+        using sets_into_space[OF `A \<in> sets P`]
+        by (auto simp add: Q.pair_measure_alt space_pair_algebra
+                 intro!: M2.positive_integral_cong arg_cong[where f=\<mu>1])
     qed
-  next
     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
@@ -802,31 +788,40 @@
     unfolding F_SUPR by simp
 qed
 
+lemma (in pair_sigma_finite) positive_integral_product_swap:
+  assumes f: "f \<in> borel_measurable P"
+  shows "measure_space.positive_integral
+    (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x))) =
+  positive_integral f"
+proof -
+  interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
+  have P: "sigma_algebra P" by default
+  show ?thesis
+    unfolding Q.positive_integral_vimage[OF P Q.pair_sigma_algebra_swap_measurable f, symmetric]
+  proof (rule positive_integral_cong_measure)
+    fix A
+    assume A: "A \<in> sets P"
+    from Q.pair_sigma_algebra_swap_measurable[THEN measurable_sets, OF this] this sets_into_space[OF this]
+    show "Q.pair_measure ((\<lambda>(x, y). (y, x)) -` A \<inter> space Q.P) = pair_measure A"
+      by (auto intro!: M1.positive_integral_cong arg_cong[where f=\<mu>2]
+               simp: pair_measure_alt Q.pair_measure_alt2 space_pair_algebra)
+  qed
+qed
+
 lemma (in pair_sigma_finite) positive_integral_snd_measurable:
   assumes f: "f \<in> borel_measurable P"
   shows "M2.positive_integral (\<lambda>y. M1.positive_integral (\<lambda>x. f (x, y))) =
       positive_integral f"
 proof -
   interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
-  have s: "\<And>x y. (case (x, y) of (x, y) \<Rightarrow> f (y, x)) = f (y, x)" by simp
-  have t: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> (y, x))) = (\<lambda>(x, y). f (y, x))" by (auto simp: fun_eq_iff)
-  have bij: "bij_betw (\<lambda>(x, y). (y, x)) (space M2 \<times> space M1) (space P)"
-    by (auto intro!: inj_onI simp: space_pair_algebra bij_betw_def)
   note pair_sigma_algebra_measurable[OF f]
   from Q.positive_integral_fst_measurable[OF this]
   have "M2.positive_integral (\<lambda>y. M1.positive_integral (\<lambda>x. f (x, y))) =
     Q.positive_integral (\<lambda>(x, y). f (y, x))"
     by simp
-  also have "\<dots> = positive_integral f"
-    unfolding positive_integral_vimage[OF bij, of f] t
-    unfolding pair_sigma_algebra_swap[symmetric]
-  proof (rule Q.positive_integral_cong_measure[symmetric])
-    fix A assume "A \<in> sets Q.P"
-    from this Q.sets_pair_sigma_algebra_swap[OF this]
-    show "pair_measure ((\<lambda>(x, y). (y, x)) ` A) = Q.pair_measure A"
-      by (auto intro!: M1.positive_integral_cong arg_cong[where f=\<mu>2]
-               simp: pair_measure_alt Q.pair_measure_alt2)
-  qed
+  also have "Q.positive_integral (\<lambda>(x, y). f (y, x)) = positive_integral f"
+    unfolding positive_integral_product_swap[OF f, symmetric]
+    by (auto intro!: Q.positive_integral_cong)
   finally show ?thesis .
 qed
 
@@ -863,28 +858,6 @@
   qed
 qed
 
-lemma (in pair_sigma_finite) positive_integral_product_swap:
-  "measure_space.positive_integral
-    (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) f =
-  positive_integral (\<lambda>(x,y). f (y,x))"
-proof -
-  interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
-  have t: "(\<lambda>y. case case y of (y, x) \<Rightarrow> (x, y) of (x, y) \<Rightarrow> f (y, x)) = f"
-    by (auto simp: fun_eq_iff)
-  have bij: "bij_betw (\<lambda>(x, y). (y, x)) (space M2 \<times> space M1) (space P)"
-    by (auto intro!: inj_onI simp: space_pair_algebra bij_betw_def)
-  show ?thesis
-    unfolding positive_integral_vimage[OF bij, of "\<lambda>(y,x). f (x,y)"]
-    unfolding pair_sigma_algebra_swap[symmetric] t
-  proof (rule Q.positive_integral_cong_measure[symmetric])
-    fix A assume "A \<in> sets Q.P"
-    from this Q.sets_pair_sigma_algebra_swap[OF this]
-    show "pair_measure ((\<lambda>(x, y). (y, x)) ` A) = Q.pair_measure A"
-      by (auto intro!: M1.positive_integral_cong arg_cong[where f=\<mu>2]
-               simp: pair_measure_alt Q.pair_measure_alt2)
-  qed
-qed
-
 lemma (in pair_sigma_algebra) measurable_product_swap:
   "f \<in> measurable (sigma (pair_algebra M2 M1)) M \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) \<in> measurable P M"
 proof -
@@ -895,27 +868,42 @@
 qed
 
 lemma (in pair_sigma_finite) integrable_product_swap:
-  "measure_space.integrable
-    (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) f \<longleftrightarrow>
-  integrable (\<lambda>(x,y). f (y,x))"
+  assumes "integrable f"
+  shows "measure_space.integrable
+    (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) (\<lambda>(x,y). f (y,x))"
 proof -
   interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
-  show ?thesis
-    unfolding Q.integrable_def integrable_def
-    unfolding positive_integral_product_swap
-    unfolding measurable_product_swap
-    by (simp add: case_prod_distrib)
+  have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff)
+  show ?thesis unfolding *
+    using assms unfolding Q.integrable_def integrable_def
+    apply (subst (1 2) positive_integral_product_swap)
+    using `integrable f` unfolding integrable_def
+    by (auto simp: *[symmetric] Q.measurable_product_swap[symmetric])
+qed
+
+lemma (in pair_sigma_finite) integrable_product_swap_iff:
+  "measure_space.integrable
+    (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) (\<lambda>(x,y). f (y,x)) \<longleftrightarrow>
+  integrable f"
+proof -
+  interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
+  from Q.integrable_product_swap[of "\<lambda>(x,y). f (y,x)"] integrable_product_swap[of f]
+  show ?thesis by auto
 qed
 
 lemma (in pair_sigma_finite) integral_product_swap:
-  "measure_space.integral
-    (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) f =
-  integral (\<lambda>(x,y). f (y,x))"
+  assumes "integrable f"
+  shows "measure_space.integral
+    (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) (\<lambda>(x,y). f (y,x)) =
+  integral f"
 proof -
   interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
+  have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff)
   show ?thesis
-    unfolding integral_def Q.integral_def positive_integral_product_swap
-    by (simp add: case_prod_distrib)
+    unfolding integral_def Q.integral_def *
+    apply (subst (1 2) positive_integral_product_swap)
+    using `integrable f` unfolding integrable_def
+    by (auto simp: *[symmetric] Q.measurable_product_swap[symmetric])
 qed
 
 lemma (in pair_sigma_finite) integrable_fst_measurable:
@@ -988,10 +976,10 @@
 proof -
   interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
   have Q_int: "Q.integrable (\<lambda>(x, y). f (y, x))"
-    using f unfolding integrable_product_swap by simp
+    using f unfolding integrable_product_swap_iff .
   show ?INT
     using Q.integrable_fst_measurable(2)[OF Q_int]
-    unfolding integral_product_swap by simp
+    using integral_product_swap[OF f] by simp
   show ?AE
     using Q.integrable_fst_measurable(1)[OF Q_int]
     by simp
@@ -1355,18 +1343,6 @@
             pair_algebra_sets_into_space product_algebra_sets_into_space)
      auto
 
-lemma (in product_sigma_algebra) product_product_vimage_algebra:
-  assumes [simp]: "I \<inter> J = {}"
-  shows "sigma_algebra.vimage_algebra
-    (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))
-    (space (sigma (product_algebra M (I \<union> J)))) (\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))) =
-    sigma (product_algebra M (I \<union> J))"
-  unfolding sigma_pair_algebra_sigma_eq using sets_into_space
-  by (intro vimage_algebra_sigma[OF bij_inv_restrict_merge]
-            pair_algebra_sets_into_space product_algebra_sets_into_space
-            measurable_merge_on_generating measurable_restrict_on_generating)
-     auto
-
 lemma (in product_sigma_algebra) pair_product_product_vimage_algebra:
   assumes [simp]: "I \<inter> J = {}"
   shows "sigma_algebra.vimage_algebra (sigma (product_algebra M (I \<union> J)))
@@ -1378,24 +1354,6 @@
             measurable_merge_on_generating measurable_restrict_on_generating)
      auto
 
-lemma (in product_sigma_algebra) pair_product_singleton_vimage_algebra:
-  assumes [simp]: "i \<notin> I"
-  shows "sigma_algebra.vimage_algebra (sigma (pair_algebra (sigma (product_algebra M I)) (M i)))
-    (space (sigma (product_algebra M (insert i I)))) (\<lambda>x. (restrict x I, x i)) =
-    (sigma (product_algebra M (insert i I)))"
-  unfolding sigma_pair_algebra_product_singleton using sets_into_space
-  by (intro vimage_algebra_sigma[OF bij_inv_restrict_insert]
-            pair_algebra_sets_into_space product_algebra_sets_into_space
-            measurable_merge_singleton_on_generating measurable_restrict_singleton_on_generating)
-      auto
-
-lemma (in product_sigma_algebra) singleton_vimage_algebra:
-  "sigma_algebra.vimage_algebra (sigma (product_algebra M {i})) (space (M i)) (\<lambda>x. \<lambda>j\<in>{i}. x) = M i"
-  using sets_into_space
-  by (intro vimage_algebra_sigma[of "M i", unfolded M.sigma_eq, OF bij_inv_singleton[symmetric]]
-             product_algebra_sets_into_space measurable_singleton_on_generator measurable_component_on_generator)
-     auto
-
 lemma (in product_sigma_algebra) measurable_restrict_iff:
   assumes IJ[simp]: "I \<inter> J = {}"
   shows "f \<in> measurable (sigma (pair_algebra
@@ -1430,6 +1388,13 @@
   then show "?f \<in> measurable ?P M'" by (simp add: comp_def)
 qed
 
+lemma (in product_sigma_algebra) singleton_vimage_algebra:
+  "sigma_algebra.vimage_algebra (sigma (product_algebra M {i})) (space (M i)) (\<lambda>x. \<lambda>j\<in>{i}. x) = M i"
+  using sets_into_space
+  by (intro vimage_algebra_sigma[of "M i", unfolded M.sigma_eq, OF bij_inv_singleton[symmetric]]
+            product_algebra_sets_into_space measurable_singleton_on_generator measurable_component_on_generator)
+     auto
+
 lemma (in product_sigma_algebra) measurable_component_singleton:
   "(\<lambda>x. f (x i)) \<in> measurable (sigma (product_algebra M {i})) M' \<longleftrightarrow>
     f \<in> measurable (M i) M'"
@@ -1479,6 +1444,55 @@
   using sets_into_space unfolding measurable_component_singleton[symmetric]
   by (auto intro!: measurable_cong arg_cong[where f=f] simp: fun_eq_iff extensional_def)
 
+
+lemma (in pair_sigma_algebra) measurable_pair_split:
+  assumes "sigma_algebra M1'" "sigma_algebra M2'"
+  assumes f: "f \<in> measurable M1 M1'" and g: "g \<in> measurable M2 M2'"
+  shows "(\<lambda>(x, y). (f x, g y)) \<in> measurable P (sigma (pair_algebra M1' M2'))"
+proof (rule measurable_sigma)
+  interpret M1': sigma_algebra M1' by fact
+  interpret M2': sigma_algebra M2' by fact
+  interpret Q: pair_sigma_algebra M1' M2' by default
+  show "sets Q.E \<subseteq> Pow (space Q.E)"
+    using M1'.sets_into_space M2'.sets_into_space by (auto simp: pair_algebra_def)
+  show "(\<lambda>(x, y). (f x, g y)) \<in> space P \<rightarrow> space Q.E"
+    using f g unfolding measurable_def pair_algebra_def by auto
+  fix A assume "A \<in> sets Q.E"
+  then obtain X Y where A: "A = X \<times> Y" "X \<in> sets M1'" "Y \<in> sets M2'"
+    unfolding pair_algebra_def by auto
+  then have *: "(\<lambda>(x, y). (f x, g y)) -` A \<inter> space P =
+      (f -` X \<inter> space M1) \<times> (g -` Y \<inter> space M2)"
+    by (auto simp: pair_algebra_def)
+  then show "(\<lambda>(x, y). (f x, g y)) -` A \<inter> space P \<in> sets P"
+    using f g A unfolding measurable_def *
+    by (auto intro!: pair_algebraI in_sigma)
+qed
+
+lemma (in product_sigma_algebra) measurable_add_dim:
+  assumes "i \<notin> I" "finite I"
+  shows "(\<lambda>(f, y). f(i := y)) \<in> measurable (sigma (pair_algebra (sigma (product_algebra M I)) (M i)))
+                         (sigma (product_algebra M (insert i I)))"
+proof (subst measurable_cong)
+  interpret I: finite_product_sigma_algebra M I by default fact
+  interpret i: finite_product_sigma_algebra M "{i}" by default auto
+  interpret Ii: pair_sigma_algebra I.P "M i" by default
+  interpret Ii': pair_sigma_algebra I.P i.P by default
+  have disj: "I \<inter> {i} = {}" using `i \<notin> I` by auto
+  have "(\<lambda>(x, y). (id x, \<lambda>_\<in>{i}. y)) \<in> measurable Ii.P Ii'.P"
+  proof (intro Ii.measurable_pair_split I.measurable_ident)
+    show "(\<lambda>y. \<lambda>_\<in>{i}. y) \<in> measurable (M i) i.P"
+      apply (rule measurable_singleton[THEN iffD1])
+      using i.measurable_ident unfolding id_def .
+  qed default
+  from measurable_comp[OF this measurable_merge[OF disj]]
+  show "(\<lambda>(x, y). merge I x {i} y) \<circ> (\<lambda>(x, y). (id x, \<lambda>_\<in>{i}. y))
+    \<in> measurable (sigma (pair_algebra I.P (M i))) (sigma (product_algebra M (insert i I)))"
+    (is "?f \<in> _") by simp
+  fix x assume "x \<in> space Ii.P"
+  with assms show "(\<lambda>(f, y). f(i := y)) x = ?f x"
+    by (cases x) (simp add: merge_def fun_eq_iff pair_algebra_def extensional_def)
+qed
+
 locale product_sigma_finite =
   fixes M :: "'i \<Rightarrow> 'a algebra" and \<mu> :: "'i \<Rightarrow> 'a set \<Rightarrow> pextreal"
   assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i) (\<mu> i)"
@@ -1549,29 +1563,24 @@
   interpret I: sigma_finite_measure P \<nu> by fact
   interpret P: pair_sigma_finite P \<nu> "M i" "\<mu> i" ..
 
-  let ?h = "\<lambda>x. (restrict x I, x i)"
-  let ?\<nu> = "\<lambda>A. P.pair_measure (?h ` A)"
+  let ?h = "(\<lambda>(f, y). f(i := y))"
+  let ?\<nu> = "\<lambda>A. P.pair_measure (?h -` A \<inter> space P.P)"
+  have I': "sigma_algebra I'.P" by default
   interpret I': measure_space "sigma (product_algebra M (insert i I))" ?\<nu>
-    apply (subst pair_product_singleton_vimage_algebra[OF `i \<notin> I`, symmetric])
-    apply (intro P.measure_space_isomorphic bij_inv_bij_betw)
-    unfolding sigma_pair_algebra_product_singleton
-    by (rule bij_inv_restrict_insert[OF `i \<notin> I`])
+    apply (rule P.measure_space_vimage[OF I'])
+    apply (rule measurable_add_dim[OF `i \<notin> I` `finite I`])
+    by simp
   show ?case
   proof (intro exI[of _ ?\<nu>] conjI ballI)
     { fix A assume A: "A \<in> (\<Pi> i\<in>insert i I. sets (M i))"
-      moreover then have "A \<in> (\<Pi> i\<in>I. sets (M i))" by auto
-      moreover have "(\<lambda>x. (restrict x I, x i)) ` Pi\<^isub>E (insert i I) A = Pi\<^isub>E I A \<times> A i"
-        using `i \<notin> I`
-        apply auto
-        apply (rule_tac x="a(i:=b)" in image_eqI)
-        apply (auto simp: extensional_def fun_eq_iff)
-        done
-      ultimately show "?\<nu> (Pi\<^isub>E (insert i I) A) = (\<Prod>i\<in>insert i I. \<mu> i (A i))"
-        apply simp
+      then have *: "?h -` Pi\<^isub>E (insert i I) A \<inter> space P.P = Pi\<^isub>E I A \<times> A i"
+        using `i \<notin> I` M.sets_into_space by (auto simp: pair_algebra_def) blast
+      show "?\<nu> (Pi\<^isub>E (insert i I) A) = (\<Prod>i\<in>insert i I. \<mu> i (A i))"
+        unfolding * using A
         apply (subst P.pair_measure_times)
-        apply fastsimp
-        apply fastsimp
-        using `i \<notin> I` `finite I` prod[of A] by (auto simp: ac_simps) }
+        using A apply fastsimp
+        using A apply fastsimp
+        using `i \<notin> I` `finite I` prod[of A] A by (auto simp: ac_simps) }
     note product = this
     show "sigma_finite_measure I'.P ?\<nu>"
     proof
@@ -1671,7 +1680,7 @@
   shows "pair_sigma_finite.pair_measure
      (sigma (product_algebra M I)) (product_measure I)
      (sigma (product_algebra M J)) (product_measure J)
-     ((\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))) ` A) =
+     ((\<lambda>(x,y). merge I x J y) -` A \<inter> space (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))) =
    product_measure (I \<union> J) A"
 proof -
   interpret I: finite_product_sigma_finite M \<mu> I by default fact
@@ -1679,51 +1688,52 @@
   have "finite (I \<union> J)" using fin by auto
   interpret IJ: finite_product_sigma_finite M \<mu> "I \<union> J" by default fact
   interpret P: pair_sigma_finite I.P I.measure J.P J.measure by default
-  let ?f = "\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))"
-    from IJ.sigma_finite_pairs obtain F where
-      F: "\<And>i. i\<in> I \<union> J \<Longrightarrow> range (F i) \<subseteq> sets (M i)"
-         "(\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k) \<up> space IJ.G"
-         "\<And>k. \<forall>i\<in>I\<union>J. \<mu> i (F i k) \<noteq> \<omega>"
-      by auto
-    let ?F = "\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k"
-  have split_f_image[simp]: "\<And>F. ?f ` (Pi\<^isub>E (I \<union> J) F) = (Pi\<^isub>E I F) \<times> (Pi\<^isub>E J F)"
-    apply auto apply (rule_tac x="merge I a J b" in image_eqI)
-    by (auto dest: extensional_restrict)
-    show "P.pair_measure (?f ` A) = IJ.measure A"
+  let ?g = "\<lambda>(x,y). merge I x J y"
+  let "?X S" = "?g -` S \<inter> space P.P"
+  from IJ.sigma_finite_pairs obtain F where
+    F: "\<And>i. i\<in> I \<union> J \<Longrightarrow> range (F i) \<subseteq> sets (M i)"
+       "(\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k) \<up> space IJ.G"
+       "\<And>k. \<forall>i\<in>I\<union>J. \<mu> i (F i k) \<noteq> \<omega>"
+    by auto
+  let ?F = "\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k"
+  show "P.pair_measure (?X A) = IJ.measure A"
   proof (rule measure_unique_Int_stable[OF _ _ _ _ _ _ _ _ A])
-      show "Int_stable IJ.G" by (simp add: PiE_Int Int_stable_def product_algebra_def) auto
-      show "range ?F \<subseteq> sets IJ.G" using F by (simp add: image_subset_iff product_algebra_def)
-      show "?F \<up> space IJ.G " using F(2) by simp
-      show "measure_space IJ.P (\<lambda>A. P.pair_measure (?f ` A))"
-      apply (subst product_product_vimage_algebra[OF IJ, symmetric])
-      apply (intro P.measure_space_isomorphic bij_inv_bij_betw)
-      unfolding sigma_pair_algebra_sigma_eq
-      by (rule bij_inv_restrict_merge[OF `I \<inter> J = {}`])
-      show "measure_space IJ.P IJ.measure" by fact
-    next
-      fix A assume "A \<in> sets IJ.G"
-      then obtain F where A[simp]: "A = Pi\<^isub>E (I \<union> J) F" "F \<in> (\<Pi> i\<in>I \<union> J. sets (M i))"
-        by (auto simp: product_algebra_def)
-      then have F: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> sets (M i)" "\<And>i. i \<in> J \<Longrightarrow> F i \<in> sets (M i)"
-        by auto
-      have "P.pair_measure (?f ` A) = (\<Prod>i\<in>I. \<mu> i (F i)) * (\<Prod>i\<in>J. \<mu> i (F i))"
-        using `finite J` `finite I` F
-        by (simp add: P.pair_measure_times I.measure_times J.measure_times)
-      also have "\<dots> = (\<Prod>i\<in>I \<union> J. \<mu> i (F i))"
-        using `finite J` `finite I` `I \<inter> J = {}`  by (simp add: setprod_Un_one)
-      also have "\<dots> = IJ.measure A"
-        using `finite J` `finite I` F unfolding A
-        by (intro IJ.measure_times[symmetric]) auto
-      finally show "P.pair_measure (?f ` A) = IJ.measure A" .
-    next
-      fix k
-      have "\<And>i. i \<in> I \<union> J \<Longrightarrow> F i k \<in> sets (M i)" using F by auto
-      then have "P.pair_measure (?f ` ?F k) = (\<Prod>i\<in>I. \<mu> i (F i k)) * (\<Prod>i\<in>J. \<mu> i (F i k))"
-        by (simp add: P.pair_measure_times I.measure_times J.measure_times)
-      then show "P.pair_measure (?f ` ?F k) \<noteq> \<omega>"
-        using `finite I` F by (simp add: setprod_\<omega>)
-    qed simp
-  qed
+    show "Int_stable IJ.G" by (simp add: PiE_Int Int_stable_def product_algebra_def) auto
+    show "range ?F \<subseteq> sets IJ.G" using F by (simp add: image_subset_iff product_algebra_def)
+    show "?F \<up> space IJ.G " using F(2) by simp
+    have "sigma_algebra IJ.P" by default
+    then show "measure_space IJ.P (\<lambda>A. P.pair_measure (?X A))"
+      apply (rule P.measure_space_vimage)
+      apply (rule measurable_merge[OF `I \<inter> J = {}`])
+      by simp
+    show "measure_space IJ.P IJ.measure" by fact
+  next
+    fix A assume "A \<in> sets IJ.G"
+    then obtain F where A[simp]: "A = Pi\<^isub>E (I \<union> J) F"
+      and F: "\<And>i. i \<in> I \<union> J \<Longrightarrow> F i \<in> sets (M i)"
+      by (auto simp: product_algebra_def)
+    then have "?X A = (Pi\<^isub>E I F \<times> Pi\<^isub>E J F)"
+      using sets_into_space by (auto simp: space_pair_algebra) blast+
+    then have "P.pair_measure (?X A) = (\<Prod>i\<in>I. \<mu> i (F i)) * (\<Prod>i\<in>J. \<mu> i (F i))"
+      using `finite J` `finite I` F
+      by (simp add: P.pair_measure_times I.measure_times J.measure_times)
+    also have "\<dots> = (\<Prod>i\<in>I \<union> J. \<mu> i (F i))"
+      using `finite J` `finite I` `I \<inter> J = {}`  by (simp add: setprod_Un_one)
+    also have "\<dots> = IJ.measure A"
+      using `finite J` `finite I` F unfolding A
+      by (intro IJ.measure_times[symmetric]) auto
+    finally show "P.pair_measure (?X A) = IJ.measure A" .
+  next
+    fix k
+    have k: "\<And>i. i \<in> I \<union> J \<Longrightarrow> F i k \<in> sets (M i)" using F by auto
+    then have "?X (?F k) = (\<Pi>\<^isub>E i\<in>I. F i k) \<times> (\<Pi>\<^isub>E i\<in>J. F i k)"
+      using sets_into_space by (auto simp: space_pair_algebra) blast+
+    with k have "P.pair_measure (?X (?F k)) = (\<Prod>i\<in>I. \<mu> i (F i k)) * (\<Prod>i\<in>J. \<mu> i (F i k))"
+     by (simp add: P.pair_measure_times I.measure_times J.measure_times)
+    then show "P.pair_measure (?X (?F k)) \<noteq> \<omega>"
+      using `finite I` F by (simp add: setprod_\<omega>)
+  qed simp
+qed
 
 lemma (in product_sigma_finite) product_positive_integral_fold:
   assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
@@ -1736,23 +1746,18 @@
   have "finite (I \<union> J)" using fin by auto
   interpret IJ: finite_product_sigma_finite M \<mu> "I \<union> J" by default fact
   interpret P: pair_sigma_finite I.P I.measure J.P J.measure by default
-  let ?f = "\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))"
   have P_borel: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> merge I x J y)) \<in> borel_measurable P.P"
     unfolding case_prod_distrib measurable_merge_iff[OF IJ, symmetric] using f .
-  have bij: "bij_betw ?f (space IJ.P) (space P.P)"
-    unfolding sigma_pair_algebra_sigma_eq
-    by (intro bij_inv_bij_betw) (rule bij_inv_restrict_merge[OF IJ])
-  have "IJ.positive_integral f =  IJ.positive_integral (\<lambda>x. f (restrict x (I \<union> J)))"
-    by (auto intro!: IJ.positive_integral_cong arg_cong[where f=f] dest!: extensional_restrict)
-  also have "\<dots> = I.positive_integral (\<lambda>x. J.positive_integral (\<lambda>y. f (merge I x J y)))"
+  show ?thesis
     unfolding P.positive_integral_fst_measurable[OF P_borel, simplified]
-    unfolding P.positive_integral_vimage[OF bij]
-    unfolding product_product_vimage_algebra[OF IJ]
-    apply simp
-    apply (rule IJ.positive_integral_cong_measure[symmetric])
-    apply (rule measure_fold)
-    using assms by auto
-  finally show ?thesis .
+    apply (subst IJ.positive_integral_cong_measure[symmetric])
+    apply (rule measure_fold[OF IJ fin])
+    apply assumption
+  proof (rule P.positive_integral_vimage)
+    show "sigma_algebra IJ.P" by default
+    show "(\<lambda>(x, y). merge I x J y) \<in> measurable P.P IJ.P" by (rule measurable_merge[OF IJ])
+    show "f \<in> borel_measurable IJ.P" using f .
+  qed
 qed
 
 lemma (in product_sigma_finite) product_positive_integral_singleton:
@@ -1760,31 +1765,18 @@
   shows "product_positive_integral {i} (\<lambda>x. f (x i)) = M.positive_integral i f"
 proof -
   interpret I: finite_product_sigma_finite M \<mu> "{i}" by default simp
-  have bij: "bij_betw (\<lambda>x. \<lambda>j\<in>{i}. x) (space (M i)) (space I.P)"
-    by (auto intro!: bij_betwI ext simp: extensional_def)
-  have *: "(\<lambda>x. (\<lambda>x. \<lambda>j\<in>{i}. x) -` Pi\<^isub>E {i} x \<inter> space (M i)) ` (\<Pi> i\<in>{i}. sets (M i)) = sets (M i)"
-  proof (subst image_cong, rule refl)
-    fix x assume "x \<in> (\<Pi> i\<in>{i}. sets (M i))"
-    then show "(\<lambda>x. \<lambda>j\<in>{i}. x) -` Pi\<^isub>E {i} x \<inter> space (M i) = x i"
-      using sets_into_space by auto
-  qed auto
-  have vimage: "I.vimage_algebra (space (M i)) (\<lambda>x. \<lambda>j\<in>{i}. x) = M i"
-    unfolding I.vimage_algebra_def
-    unfolding product_sigma_algebra_def sets_sigma
-    apply (subst sigma_sets_vimage[symmetric])
-    apply (simp_all add: image_image sigma_sets_eq product_algebra_def * del: vimage_Int)
-    using sets_into_space by blast
+  have T: "(\<lambda>x. x i) \<in> measurable (sigma (product_algebra M {i})) (M i)"
+    using measurable_component_singleton[of "\<lambda>x. x" i]
+          measurable_ident[unfolded id_def] by auto
   show "I.positive_integral (\<lambda>x. f (x i)) = M.positive_integral i f"
-    unfolding I.positive_integral_vimage[OF bij]
-    unfolding vimage
-    apply (subst positive_integral_cong_measure)
-  proof -
-    fix A assume A: "A \<in> sets (M i)"
-    have "(\<lambda>x. \<lambda>j\<in>{i}. x) ` A = (\<Pi>\<^isub>E i\<in>{i}. A)"
-      by (auto intro!: image_eqI ext[where 'b='a] simp: extensional_def)
-    with A show "product_measure {i} ((\<lambda>x. \<lambda>j\<in>{i}. x) ` A) = \<mu> i A"
-      using I.measure_times[of "\<lambda>i. A"] by simp
-  qed simp
+    unfolding I.positive_integral_vimage[OF sigma_algebras T f, symmetric]
+  proof (rule positive_integral_cong_measure)
+    fix A let ?P = "(\<lambda>x. x i) -` A \<inter> space (sigma (product_algebra M {i}))"
+    assume A: "A \<in> sets (M i)"
+    then have *: "?P = {i} \<rightarrow>\<^isub>E A" using sets_into_space by auto
+    show "product_measure {i} ?P = \<mu> i A" unfolding *
+      using A I.measure_times[of "\<lambda>_. A"] by auto
+  qed
 qed
 
 lemma (in product_sigma_finite) product_positive_integral_insert:
diff -r 1eef159301df -r 621fa31e1dbd src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Fri Jan 21 10:43:09 2011 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Tue Jan 25 09:45:45 2011 +0100
@@ -1104,38 +1104,6 @@
     unfolding eq[OF A, symmetric] RN_deriv(2)[OF \<nu> A, symmetric] ..
 qed
 
-lemma (in sigma_finite_measure) RN_deriv_vimage:
-  fixes f :: "'b \<Rightarrow> 'a"
-  assumes f: "bij_inv S (space M) f g"
-  assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
-  shows "AE x.
-    sigma_finite_measure.RN_deriv (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>A. \<nu> (f ` A)) (g x) = RN_deriv \<nu> x"
-proof (rule RN_deriv_unique[OF \<nu>])
-  interpret sf: sigma_finite_measure "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
-    using f by (rule sigma_finite_measure_isomorphic[OF bij_inv_bij_betw(1)])
-  interpret \<nu>: measure_space M \<nu> using \<nu>(1) .
-  have \<nu>': "measure_space (vimage_algebra S f) (\<lambda>A. \<nu> (f ` A))"
-    using f by (rule \<nu>.measure_space_isomorphic[OF bij_inv_bij_betw(1)])
-  { fix A assume "A \<in> sets M" then have "f ` (f -` A \<inter> S) = A"
-      using sets_into_space f[THEN bij_inv_bij_betw(1), unfolded bij_betw_def]
-      by (intro image_vimage_inter_eq[where T="space M"]) auto }
-  note A_f = this
-  then have ac: "sf.absolutely_continuous (\<lambda>A. \<nu> (f ` A))"
-    using \<nu>(2) by (auto simp: sf.absolutely_continuous_def absolutely_continuous_def)
-  show "(\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x)) \<in> borel_measurable M"
-    using sf.RN_deriv(1)[OF \<nu>' ac]
-    unfolding measurable_vimage_iff_inv[OF f] comp_def .
-  fix A assume "A \<in> sets M"
-  then have *: "\<And>x. x \<in> space M \<Longrightarrow> indicator (f -` A \<inter> S) (g x) = (indicator A x :: pextreal)"
-    using f by (auto simp: bij_inv_def indicator_def)
-  have "\<nu> (f ` (f -` A \<inter> S)) = sf.positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) x * indicator (f -` A \<inter> S) x)"
-    using `A \<in> sets M` by (force intro!: sf.RN_deriv(2)[OF \<nu>' ac])
-  also have "\<dots> = (\<integral>\<^isup>+x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
-    unfolding positive_integral_vimage_inv[OF f]
-    by (simp add: * cong: positive_integral_cong)
-  finally show "\<nu> A = (\<integral>\<^isup>+x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
-    unfolding A_f[OF `A \<in> sets M`] .
-qed
 
 lemma (in sigma_finite_measure) RN_deriv_finite:
   assumes sfm: "sigma_finite_measure M \<nu>" and ac: "absolutely_continuous \<nu>"