diff -r f9ff311992b6 -r 3e39b0e730d6 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Feb 02 10:35:41 2011 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Feb 02 12:34:45 2011 +0100
@@ -29,7 +29,7 @@
   sets :: "'a set set"
 
 locale algebra =
-  fixes M :: "'a algebra"
+  fixes M :: "('a, 'b) algebra_scheme"
   assumes space_closed: "sets M \<subseteq> Pow (space M)"
      and  empty_sets [iff]: "{} \<in> sets M"
      and  compl_sets [intro]: "!!a. a \<in> sets M \<Longrightarrow> space M - a \<in> sets M"
@@ -104,7 +104,7 @@
 section {* Restricted algebras *}
 
 abbreviation (in algebra)
-  "restricted_space A \<equiv> \<lparr> space = A, sets = (\<lambda>S. (A \<inter> S)) ` sets M \<rparr>"
+  "restricted_space A \<equiv> \<lparr> space = A, sets = (\<lambda>S. (A \<inter> S)) ` sets M, \<dots> = more M \<rparr>"
 
 lemma (in algebra) restricted_algebra:
   assumes "A \<in> sets M" shows "algebra (restricted_space A)"
@@ -222,7 +222,7 @@
   | Union: "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Union>i. a i) \<in> sigma_sets sp A"
 
 definition
-  "sigma M = \<lparr> space = space M, sets = sigma_sets (space M) (sets M) \<rparr>"
+  "sigma M = \<lparr> space = space M, sets = sigma_sets (space M) (sets M), \<dots> = more M \<rparr>"
 
 lemma (in sigma_algebra) sigma_sets_subset:
   assumes a: "a \<subseteq> sets M"
@@ -354,12 +354,12 @@
 qed
 
 lemma sigma_sets_Int:
-  assumes "A \<in> sigma_sets sp st"
-  shows "op \<inter> A ` sigma_sets sp st = sigma_sets (A \<inter> sp) (op \<inter> A ` st)"
+  assumes "A \<in> sigma_sets sp st" "A \<subseteq> sp"
+  shows "op \<inter> A ` sigma_sets sp st = sigma_sets A (op \<inter> A ` st)"
 proof (intro equalityI subsetI)
   fix x assume "x \<in> op \<inter> A ` sigma_sets sp st"
   then obtain y where "y \<in> sigma_sets sp st" "x = y \<inter> A" by auto
-  then show "x \<in> sigma_sets (A \<inter> sp) (op \<inter> A ` st)"
+  then have "x \<in> sigma_sets (A \<inter> sp) (op \<inter> A ` st)"
   proof (induct arbitrary: x)
     case (Compl a)
     then show ?case
@@ -370,13 +370,15 @@
       by (auto intro!: sigma_sets.Union
                simp add: UN_extend_simps simp del: UN_simps)
   qed (auto intro!: sigma_sets.intros)
+  then show "x \<in> sigma_sets A (op \<inter> A ` st)"
+    using `A \<subseteq> sp` by (simp add: Int_absorb2)
 next
-  fix x assume "x \<in> sigma_sets (A \<inter> sp) (op \<inter> A ` st)"
+  fix x assume "x \<in> sigma_sets A (op \<inter> A ` st)"
   then show "x \<in> op \<inter> A ` sigma_sets sp st"
   proof induct
     case (Compl a)
     then obtain x where "a = A \<inter> x" "x \<in> sigma_sets sp st" by auto
-    then show ?case
+    then show ?case using `A \<subseteq> sp`
       by (force simp add: image_iff intro!: bexI[of _ "sp - x"] sigma_sets.Compl)
   next
     case (Union a)
@@ -707,7 +709,7 @@
 subsection {* Sigma algebra generated by function preimages *}
 
 definition (in sigma_algebra)
-  "vimage_algebra S f = \<lparr> space = S, sets = (\<lambda>A. f -` A \<inter> S) ` sets M \<rparr>"
+  "vimage_algebra S f = \<lparr> space = S, sets = (\<lambda>A. f -` A \<inter> S) ` sets M, \<dots> = more M \<rparr>"
 
 lemma (in sigma_algebra) in_vimage_algebra[simp]:
   "A \<in> sets (vimage_algebra S f) \<longleftrightarrow> (\<exists>B\<in>sets M. A = f -` B \<inter> S)"
@@ -870,7 +872,7 @@
 section {* Conditional space *}
 
 definition (in algebra)
-  "image_space X = \<lparr> space = X`space M, sets = (\<lambda>S. X`S) ` sets M \<rparr>"
+  "image_space X = \<lparr> space = X`space M, sets = (\<lambda>S. X`S) ` sets M, \<dots> = more M \<rparr>"
 
 definition (in algebra)
   "conditional_space X A = algebra.image_space (restricted_space A) X"
@@ -1158,7 +1160,7 @@
 section {* Dynkin systems *}
 
 locale dynkin_system =
-  fixes M :: "'a algebra"
+  fixes M :: "('a, 'b) algebra_scheme"
   assumes space_closed: "sets M \<subseteq> Pow (space M)"
     and   space: "space M \<in> sets M"
     and   compl[intro!]: "\<And>A. A \<in> sets M \<Longrightarrow> space M - A \<in> sets M"
@@ -1239,12 +1241,12 @@
 
 subsection "Smallest Dynkin systems"
 
-definition dynkin :: "'a algebra \<Rightarrow> 'a algebra" where
+definition dynkin where
   "dynkin M = \<lparr> space = space M,
-     sets =  \<Inter>{D. dynkin_system \<lparr> space = space M, sets = D\<rparr> \<and> sets M \<subseteq> D}\<rparr>"
+     sets = \<Inter>{D. dynkin_system \<lparr> space = space M, sets = D \<rparr> \<and> sets M \<subseteq> D},
+     \<dots> = more M \<rparr>"
 
 lemma dynkin_system_dynkin:
-  fixes M :: "'a algebra"
   assumes "sets M \<subseteq> Pow (space M)"
   shows "dynkin_system (dynkin M)"
 proof (rule dynkin_systemI)
@@ -1311,21 +1313,17 @@
 qed
 
 lemma (in dynkin_system) dynkin_subset:
-  fixes N :: "'a algebra"
   assumes "sets N \<subseteq> sets M"
   assumes "space N = space M"
   shows "sets (dynkin N) \<subseteq> sets M"
 proof -
-  have *: "\<lparr>space = space N, sets = sets M\<rparr> = M"
-    unfolding `space N = space M` by simp
   have "dynkin_system M" by default
-  then have "dynkin_system \<lparr>space = space N, sets = sets M\<rparr>"
-    using assms unfolding * by simp
+  then have "dynkin_system \<lparr>space = space N, sets = sets M \<rparr>"
+    using assms unfolding dynkin_system_def by simp
   with `sets N \<subseteq> sets M` show ?thesis by (auto simp add: dynkin_def)
 qed
 
 lemma sigma_eq_dynkin:
-  fixes M :: "'a algebra"
   assumes sets: "sets M \<subseteq> Pow (space M)"
   assumes "Int_stable M"
   shows "sigma M = dynkin M"
@@ -1367,7 +1365,7 @@
   have "sigma_sets (space M) (sets M) \<subseteq> sets (dynkin M)" by auto
   ultimately have "sigma_sets (space M) (sets M) = sets (dynkin M)" by auto
   then show ?thesis
-    by (intro algebra.equality) (simp_all add: sigma_def)
+    by (auto intro!: algebra.equality simp: sigma_def dynkin_def)
 qed
 
 lemma (in dynkin_system) dynkin_idem:
@@ -1381,23 +1379,22 @@
       by (intro dynkin_subset) auto
   qed
   then show ?thesis
-    by (auto intro!: algebra.equality)
+    by (auto intro!: algebra.equality simp: dynkin_def)
 qed
 
 lemma (in dynkin_system) dynkin_lemma:
-  fixes E :: "'a algebra"
-  assumes "Int_stable E" and E: "sets E \<subseteq> sets M" "space E = space M"
-  and "sets M \<subseteq> sets (sigma E)"
-  shows "sigma E = M"
+  assumes "Int_stable E"
+  and E: "sets E \<subseteq> sets M" "space E = space M" "sets M \<subseteq> sets (sigma E)"
+  shows "sets (sigma E) = sets M"
 proof -
   have "sets E \<subseteq> Pow (space E)"
-    using E sets_into_space by auto
+    using E sets_into_space by force
   then have "sigma E = dynkin E"
     using `Int_stable E` by (rule sigma_eq_dynkin)
   moreover then have "sets (dynkin E) = sets M"
-    using assms dynkin_subset[OF E] by simp
+    using assms dynkin_subset[OF E(1,2)] by simp
   ultimately show ?thesis
-    using E by simp
+    using assms by (auto intro!: algebra.equality simp: dynkin_def)
 qed
 
 subsection "Sigma algebras on finite sets"
@@ -1467,6 +1464,7 @@
 lemma vimage_algebra_sigma:
   assumes bi: "bij_inv (space (sigma F)) (space (sigma E)) f e"
     and "sets E \<subseteq> Pow (space E)" and F: "sets F \<subseteq> Pow (space F)"
+    and "more E = more F"
     and "f \<in> measurable F E" "e \<in> measurable E F"
   shows "sigma_algebra.vimage_algebra (sigma E) (space (sigma F)) f = sigma F"
 proof -
@@ -1486,8 +1484,8 @@
       using `f \<in> measurable F E` unfolding measurable_def by auto
   qed
   show "vimage_algebra (space (sigma F)) f = sigma F"
-    unfolding vimage_algebra_def
-    using assms by (auto simp: bij_inv_def eq sigma_sets_vimage[symmetric] sigma_def)
+    unfolding vimage_algebra_def using assms
+    by (auto simp: bij_inv_def eq sigma_sets_vimage[symmetric] sigma_def)
 qed
 
 lemma measurable_sigma_sigma: