diff -r 94427db32392 -r 688f6ff859e1 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Dec 01 20:12:53 2010 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Dec 01 21:03:02 2010 +0100
@@ -403,6 +403,12 @@
   shows "sets (sigma N) \<subseteq> sets M"
   by (unfold assms sets_sigma, rule sigma_sets_subset, rule assms)
 
+lemma in_sigma[intro, simp]: "A \<in> sets M \<Longrightarrow> A \<in> sets (sigma M)"
+  unfolding sigma_def by (auto intro!: sigma_sets.Basic)
+
+lemma (in sigma_algebra) sigma_eq[simp]: "sigma M = M"
+  unfolding sigma_def sigma_sets_eq by simp
+
 section {* Measurable functions *}
 
 definition
@@ -865,6 +871,22 @@
   qed
 qed
 
+lemma vimage_algebra_sigma:
+  assumes E: "sets E \<subseteq> Pow (space E)"
+    and f: "f \<in> space F \<rightarrow> space E"
+    and "\<And>A. A \<in> sets F \<Longrightarrow> A \<in> (\<lambda>X. f -` X \<inter> space F) ` sets E"
+    and "\<And>A. A \<in> sets E \<Longrightarrow> f -` A \<inter> space F \<in> sets F"
+  shows "sigma_algebra.vimage_algebra (sigma E) (space F) f = sigma F"
+proof -
+  interpret sigma_algebra "sigma E"
+    using assms by (intro sigma_algebra_sigma) auto
+  have eq: "sets F = (\<lambda>X. f -` X \<inter> space F) ` sets E"
+    using assms by auto
+  show "vimage_algebra (space F) f = sigma F"
+    unfolding vimage_algebra_def using assms
+    by (simp add: sigma_def eq sigma_sets_vimage)
+qed
+
 section {* Conditional space *}
 
 definition (in algebra)