diff -r 0d97ef1d6de9 -r de72bbe42190 src/HOL/Probability/Independent_Family.thy
--- a/src/HOL/Probability/Independent_Family.thy	Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Independent_Family.thy	Tue Nov 27 11:29:47 2012 +0100
@@ -186,11 +186,11 @@
             using G by auto
           have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) =
               prob ((\<Inter>j\<in>J. A j) - (\<Inter>i\<in>insert j J. (A(j := X)) i))"
-            using A_sets sets_into_space[of _ M] X `J \<noteq> {}`
+            using A_sets sets.sets_into_space[of _ M] X `J \<noteq> {}`
             by (auto intro!: arg_cong[where f=prob] split: split_if_asm)
           also have "\<dots> = prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)"
-            using J `J \<noteq> {}` `j \<notin> J` A_sets X sets_into_space
-            by (auto intro!: finite_measure_Diff finite_INT split: split_if_asm)
+            using J `J \<noteq> {}` `j \<notin> J` A_sets X sets.sets_into_space
+            by (auto intro!: finite_measure_Diff sets.finite_INT split: split_if_asm)
           finally have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) =
               prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)" .
           moreover {
@@ -224,7 +224,7 @@
             show "disjoint_family (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i)"
               using disj by (rule disjoint_family_on_bisimulation) auto
             show "range (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i) \<subseteq> events"
-              using A_sets F `finite J` `J \<noteq> {}` `j \<notin> J` by (auto intro!: Int)
+              using A_sets F `finite J` `J \<noteq> {}` `j \<notin> J` by (auto intro!: sets.Int)
           qed
           moreover { fix k
             from J A `j \<in> K` have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * (\<Prod>i\<in>J. prob (A i))"
@@ -243,7 +243,7 @@
           show "prob ((\<Inter>j\<in>J. A j) \<inter> (\<Union>k. F k)) = prob (\<Union>k. F k) * (\<Prod>j\<in>J. prob (A j))"
             by (auto dest!: sums_unique)
         qed (insert F, auto)
-      qed (insert sets_into_space, auto)
+      qed (insert sets.sets_into_space, auto)
       then have mono: "dynkin (space M) (G j) \<subseteq> {E \<in> events. indep_sets (G(j := {E})) K}"
       proof (rule dynkin_system.dynkin_subset, safe)
         fix X assume "X \<in> G j"
@@ -291,7 +291,7 @@
   proof (rule indep_sets_mono_sets, subst sigma_eq_dynkin, simp_all add: stable)
     fix i assume "i \<in> I"
     with indep have "F i \<subseteq> events" by (auto simp: indep_sets_def)
-    with sets_into_space show "F i \<subseteq> Pow (space M)" by auto
+    with sets.sets_into_space show "F i \<subseteq> Pow (space M)" by auto
   qed
 qed
 
@@ -394,7 +394,7 @@
     let ?S = "sigma_sets (space M) (\<Union>i\<in>I j. E i)"
     assume "j \<in> J"
     from E[OF this] interpret S: sigma_algebra "space M" ?S
-      using sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto
+      using sets.sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto
 
     have "sigma_sets (space M) (\<Union>i\<in>I j. E i) = sigma_sets (space M) (?E j)"
     proof (rule sigma_sets_eqI)
@@ -416,7 +416,7 @@
   proof (rule indep_sets_sigma)
     show "indep_sets ?E J"
     proof (intro indep_setsI)
-      fix j assume "j \<in> J" with E show "?E j \<subseteq> events" by (force  intro!: finite_INT)
+      fix j assume "j \<in> J" with E show "?E j \<subseteq> events" by (force  intro!: sets.finite_INT)
     next
       fix K A assume K: "K \<noteq> {}" "K \<subseteq> J" "finite K"
         and "\<forall>j\<in>K. A j \<in> ?E j"
@@ -533,7 +533,7 @@
   interpret D: dynkin_system "space M" ?D
   proof (rule dynkin_systemI)
     fix D assume "D \<in> ?D" then show "D \<subseteq> space M"
-      using sets_into_space by auto
+      using sets.sets_into_space by auto
   next
     show "space M \<in> ?D"
       using prob_space `X \<subseteq> space M` by (simp add: Int_absorb2)
@@ -546,7 +546,7 @@
     also have "\<dots> = prob X * prob (space M) - prob X * prob A"
       using A prob_space by auto
     also have "\<dots> = prob X * prob (space M - A)"
-      using X_in A sets_into_space
+      using X_in A sets.sets_into_space
       by (subst finite_measure_Diff) (auto simp: field_simps)
     finally show "space M - A \<in> ?D"
       using A `X \<subseteq> space M` by auto
@@ -611,14 +611,14 @@
   proof (rule sigma_eq_dynkin)
     { fix B n assume "B \<in> sigma_sets (space M) (\<Union>m\<in>{..n}. A m)"
       then have "B \<subseteq> space M"
-        by induct (insert A sets_into_space[of _ M], auto) }
+        by induct (insert A sets.sets_into_space[of _ M], auto) }
     then show "?A \<subseteq> Pow (space M)" by auto
     show "Int_stable ?A"
     proof (rule Int_stableI)
       fix a assume "a \<in> ?A" then guess n .. note a = this
       fix b assume "b \<in> ?A" then guess m .. note b = this
       interpret Amn: sigma_algebra "space M" "sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)"
-        using A sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto
+        using A sets.sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto
       have "sigma_sets (space M) (\<Union>i\<in>{..n}. A i) \<subseteq> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)"
         by (intro sigma_sets_subseteq UN_mono) auto
       with a have "a \<in> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" by auto
@@ -644,7 +644,7 @@
   have F1: "range F \<subseteq> events"
     using F2 by (simp add: indep_events_def subset_eq)
   { fix i show "sigma_algebra (space M) (sigma_sets (space M) {F i})"
-      using sigma_algebra_sigma_sets[of "{F i}" "space M"] F1 sets_into_space
+      using sigma_algebra_sigma_sets[of "{F i}" "space M"] F1 sets.sets_into_space
       by auto }
   show "indep_sets (\<lambda>i. sigma_sets (space M) {F i}) UNIV"
   proof (rule indep_sets_sigma)
@@ -659,12 +659,12 @@
   proof
     fix j
     interpret S: sigma_algebra "space M" "sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})"
-      using order_trans[OF F1 space_closed]
+      using order_trans[OF F1 sets.space_closed]
       by (intro sigma_algebra_sigma_sets) (simp add: sigma_sets_singleton subset_eq)
     have "(\<Inter>n. ?Q n) = (\<Inter>n\<in>{j..}. ?Q n)"
       by (intro decseq_SucI INT_decseq_offset UN_mono) auto
     also have "\<dots> \<in> sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})"
-      using order_trans[OF F1 space_closed]
+      using order_trans[OF F1 sets.space_closed]
       by (safe intro!: S.countable_INT S.countable_UN)
          (auto simp: sigma_sets_singleton intro!: sigma_sets.Basic bexI)
     finally show "(\<Inter>n. ?Q n) \<in> sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})"
@@ -688,7 +688,7 @@
     assume A: "\<forall>j\<in>J. A j \<in> F j"
     let ?A = "\<lambda>j. if j \<in> J then A j else space M"
     have "prob (\<Inter>j\<in>I. ?A j) = prob (\<Inter>j\<in>J. A j)"
-      using subset_trans[OF F(1) space_closed] J A
+      using subset_trans[OF F(1) sets.space_closed] J A
       by (auto intro!: arg_cong[where f=prob] split: split_if_asm) blast
     also
     from A F have "(\<lambda>j. if j \<in> J then A j else space M) \<in> Pi I F" (is "?A \<in> _")
@@ -882,7 +882,7 @@
     show "indep_vars M' X I" unfolding indep_vars_def
     proof (intro conjI indep_setsI ballI rv)
       fix i show "sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)} \<subseteq> events"
-        by (auto intro!: sigma_sets_subset measurable_sets rv)
+        by (auto intro!: sets.sigma_sets_subset measurable_sets rv)
     next
       fix J Y' assume J: "J \<noteq> {}" "J \<subseteq> I" "finite J"
       assume Y': "\<forall>j\<in>J. Y' j \<in> sigma_sets (space M) {X j -` A \<inter> space M |A. A \<in> sets (M' j)}"
@@ -892,7 +892,7 @@
         from Y'[rule_format, OF this] rv[of j]
         show "\<exists>Y. Y' j = X j -` Y \<inter> space M \<and> Y \<in> sets (M' j)"
           by (subst (asm) sigma_sets_vimage_commute[symmetric, of _ _ "space (M' j)"])
-             (auto dest: measurable_space simp: sigma_sets_eq)
+             (auto dest: measurable_space simp: sets.sigma_sets_eq)
       qed
       from bchoice[OF this] obtain Y where
         Y: "\<And>j. j \<in> J \<Longrightarrow> Y' j = X j -` Y j \<inter> space M" "\<And>j. j \<in> J \<Longrightarrow> Y j \<in> sets (M' j)" by auto