diff -r fc571ebb04e1 -r 6eb0725503fc src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -1732,6 +1732,12 @@
 lemma measure_of_subset: "M \<subseteq> Pow \<Omega> \<Longrightarrow> M' \<subseteq> M \<Longrightarrow> sets (measure_of \<Omega> M' \<mu>) \<subseteq> sets (measure_of \<Omega> M \<mu>')"
   by (auto intro!: sigma_sets_subseteq)
 
+lemma emeasure_sigma: "emeasure (sigma \<Omega> A) = (\<lambda>x. 0)"
+  unfolding measure_of_def emeasure_def
+  by (subst Abs_measure_inverse)
+     (auto simp: measure_space_def positive_def countably_additive_def
+           intro!: sigma_algebra_sigma_sets sigma_algebra_trivial)
+
 lemma sigma_sets_mono'':
   assumes "A \<in> sigma_sets C D"
   assumes "B \<subseteq> D"
@@ -1839,10 +1845,6 @@
     by (simp add: measure_measure)
 qed
 
-lemma emeasure_sigma: "A \<subseteq> Pow \<Omega> \<Longrightarrow> emeasure (sigma \<Omega> A) = (\<lambda>_. 0)"
-  using measure_space_0[of A \<Omega>]
-  by (simp add: measure_of_def emeasure_def Abs_measure_inverse)
-
 lemma sigma_eqI:
   assumes [simp]: "M \<subseteq> Pow \<Omega>" "N \<subseteq> Pow \<Omega>" "sigma_sets \<Omega> M = sigma_sets \<Omega> N"
   shows "sigma \<Omega> M = sigma \<Omega> N"
@@ -2115,22 +2117,30 @@
     unfolding measurable_def by auto
 qed
 
-lemma measurable_compose_countable:
-  assumes f: "\<And>i::'i::countable. (\<lambda>x. f i x) \<in> measurable M N" and g: "g \<in> measurable M (count_space UNIV)"
+lemma measurable_compose_countable':
+  assumes f: "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>x. f i x) \<in> measurable M N"
+  and g: "g \<in> measurable M (count_space I)" and I: "countable I"
   shows "(\<lambda>x. f (g x) x) \<in> measurable M N"
   unfolding measurable_def
 proof safe
   fix x assume "x \<in> space M" then show "f (g x) x \<in> space N"
-    using f[THEN measurable_space] g[THEN measurable_space] by auto
+    using measurable_space[OF f] g[THEN measurable_space] by auto
 next
   fix A assume A: "A \<in> sets N"
-  have "(\<lambda>x. f (g x) x) -` A \<inter> space M = (\<Union>i. (g -` {i} \<inter> space M) \<inter> (f i -` A \<inter> space M))"
-    by auto
-  also have "\<dots> \<in> sets M" using f[THEN measurable_sets, OF A] g[THEN measurable_sets]
-    by (auto intro!: sets.countable_UN measurable_sets)
+  have "(\<lambda>x. f (g x) x) -` A \<inter> space M = (\<Union>i\<in>I. (g -` {i} \<inter> space M) \<inter> (f i -` A \<inter> space M))"
+    using measurable_space[OF g] by auto
+  also have "\<dots> \<in> sets M" using f[THEN measurable_sets, OF _ A] g[THEN measurable_sets]
+    apply (auto intro!: sets.countable_UN' measurable_sets I)
+    apply (rule sets.Int)
+    apply auto
+    done
   finally show "(\<lambda>x. f (g x) x) -` A \<inter> space M \<in> sets M" .
 qed
 
+lemma measurable_compose_countable:
+  assumes f: "\<And>i::'i::countable. (\<lambda>x. f i x) \<in> measurable M N" and g: "g \<in> measurable M (count_space UNIV)"
+  shows "(\<lambda>x. f (g x) x) \<in> measurable M N"
+  by (rule measurable_compose_countable'[OF assms]) auto
 lemma measurable_count_space_const:
   "(\<lambda>x. c) \<in> measurable M (count_space UNIV)"
   by (simp add: measurable_const)
@@ -2241,6 +2251,10 @@
 lemma in_Sup_sigma: "m \<in> M \<Longrightarrow> A \<in> sets m \<Longrightarrow> A \<in> sets (Sup_sigma M)"
   unfolding sets_Sup_sigma by auto
 
+lemma SUP_sigma_cong: 
+  assumes *: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (\<Squnion>\<^sub>\<sigma> i\<in>I. M i) = sets (\<Squnion>\<^sub>\<sigma> i\<in>I. N i)"
+  using * sets_eq_imp_space_eq[OF *] by (simp add: Sup_sigma_def)
+
 lemma sets_Sup_in_sets: 
   assumes "M \<noteq> {}"
   assumes "\<And>m. m \<in> M \<Longrightarrow> space m = space N"
@@ -2290,6 +2304,9 @@
   using sigma_sets_vimage_commute[of f X "space M" "sets M"]
   unfolding sets_vimage_algebra sets.sigma_sets_eq by simp
 
+lemma vimage_algebra_cong: "sets M = sets N \<Longrightarrow> sets (vimage_algebra X f M) = sets (vimage_algebra X f N)"
+  by (simp add: sets_vimage_algebra)
+
 lemma in_vimage_algebra: "A \<in> sets M \<Longrightarrow> f -` A \<inter> X \<in> sets (vimage_algebra X f M)"
   by (auto simp: vimage_algebra_def)
 
@@ -2318,6 +2335,34 @@
   finally show "g -` A \<inter> space N \<in> sets N" .
 qed (insert g, auto)
 
+lemma vimage_algebra_vimage_algebra_eq:
+  assumes *: "f \<in> X \<rightarrow> Y" "g \<in> Y \<rightarrow> space M"
+  shows "vimage_algebra X f (vimage_algebra Y g M) = vimage_algebra X (\<lambda>x. g (f x)) M"
+  (is "?VV = ?V")
+proof (rule measure_eqI)
+  have "(\<lambda>x. g (f x)) \<in> X \<rightarrow> space M" "\<And>A. A \<inter> f -` Y \<inter> X = A \<inter> X"
+    using * by auto
+  with * show "sets ?VV = sets ?V"
+    by (simp add: sets_vimage_algebra2 ex_simps[symmetric] vimage_comp comp_def del: ex_simps)
+qed (simp add: vimage_algebra_def emeasure_sigma)
+
+lemma sets_vimage_Sup_eq:
+  assumes *: "M \<noteq> {}" "\<And>m. m \<in> M \<Longrightarrow> f \<in> X \<rightarrow> space m"
+  shows "sets (vimage_algebra X f (Sup_sigma M)) = sets (\<Squnion>\<^sub>\<sigma> m \<in> M. vimage_algebra X f m)"
+  (is "?IS = ?SI")
+proof
+  show "?IS \<subseteq> ?SI"
+    by (intro sets_image_in_sets measurable_Sup_sigma2 measurable_Sup_sigma1)
+       (auto simp: space_Sup_sigma measurable_vimage_algebra1 *)
+  { fix m assume "m \<in> M"
+    moreover then have "f \<in> X \<rightarrow> space (Sup_sigma M)" "f \<in> X \<rightarrow> space m"
+      using * by (auto simp: space_Sup_sigma)
+    ultimately have "f \<in> measurable (vimage_algebra X f (Sup_sigma M)) m"
+      by (auto simp add: measurable_def sets_vimage_algebra2 intro: in_Sup_sigma) }
+  then show "?SI \<subseteq> ?IS"
+    by (auto intro!: sets_image_in_sets sets_Sup_in_sets del: subsetI simp: *)
+qed
+
 subsubsection {* Restricted Space Sigma Algebra *}
 
 definition restrict_space where
@@ -2358,6 +2403,27 @@
     by auto
 qed auto
 
+lemma sets_restrict_space_cong: "sets M = sets N \<Longrightarrow> sets (restrict_space M \<Omega>) = sets (restrict_space N \<Omega>)"
+  by (simp add: sets_restrict_space)
+
+lemma restrict_space_eq_vimage_algebra:
+  "\<Omega> \<subseteq> space M \<Longrightarrow> sets (restrict_space M \<Omega>) = sets (vimage_algebra \<Omega> (\<lambda>x. x) M)"
+  unfolding restrict_space_def
+  apply (subst sets_measure_of)
+  apply (auto simp add: image_subset_iff dest: sets.sets_into_space) []
+  apply (auto simp add: sets_vimage_algebra intro!: arg_cong2[where f=sigma_sets])
+  done
+
+lemma sets_Collect_restrict_space_iff: 
+  assumes "S \<in> sets M"
+  shows "{x\<in>space (restrict_space M S). P x} \<in> sets (restrict_space M S) \<longleftrightarrow> {x\<in>space M. x \<in> S \<and> P x} \<in> sets M"
+proof -
+  have "{x\<in>S. P x} = {x\<in>space M. x \<in> S \<and> P x}"
+    using sets.sets_into_space[OF assms] by auto
+  then show ?thesis
+    by (subst sets_restrict_space_iff) (auto simp add: space_restrict_space assms)
+qed
+
 lemma measurable_restrict_space1:
   assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M" and f: "f \<in> measurable M N"
   shows "f \<in> measurable (restrict_space M \<Omega>) N"