src/HOL/Probability/Sigma_Algebra.thy

 declare [[coercion emeasure]]
 
 lemma measure_space: "measure_space (space M) (sets M) (emeasure M)"
   by (cases M) (auto simp: space_def sets_def emeasure_def Abs_measure_inverse)
 
-interpretation sigma_algebra "space M" "sets M" for M :: "'a measure"
+interpretation sets!: sigma_algebra "space M" "sets M" for M :: "'a measure"
   using measure_space[of M] by (auto simp: measure_space_def)
 
 definition measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> 'a measure" where
   "measure_of \<Omega> A \<mu> = Abs_measure (\<Omega>, sigma_sets \<Omega> A,
     \<lambda>a. if a \<in> sigma_sets \<Omega> A \<and> measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> then \<mu> a else 0)"

   obtains (measure) \<Omega> A \<mu> where "x = Abs_measure (\<Omega>, A, \<mu>)" "\<forall>a\<in>-A. \<mu> a = 0" "measure_space \<Omega> A \<mu>"
   by atomize_elim (cases x, auto)
 
 lemma sets_eq_imp_space_eq:
   "sets M = sets M' \<Longrightarrow> space M = space M'"
-  using top[of M] top[of M'] space_closed[of M] space_closed[of M']
+  using sets.top[of M] sets.top[of M'] sets.space_closed[of M] sets.space_closed[of M']
   by blast
 
 lemma emeasure_notin_sets: "A \<notin> sets M \<Longrightarrow> emeasure M A = 0"
   by (cases M) (auto simp: sets_def emeasure_def Abs_measure_inverse measure_space_def)
 

       and f: "f \<in> space M \<rightarrow> \<Omega>"
       and ba: "\<And>y. y \<in> A \<Longrightarrow> (f -` y) \<inter> space M \<in> sets M"
   shows "f \<in> measurable M N"
 proof -
   interpret A: sigma_algebra \<Omega> "sigma_sets \<Omega> A" using B(2) by (rule sigma_algebra_sigma_sets)
-  from B top[of N] A.top space_closed[of N] A.space_closed have \<Omega>: "\<Omega> = space N" by force
+  from B sets.top[of N] A.top sets.space_closed[of N] A.space_closed have \<Omega>: "\<Omega> = space N" by force
   
   { fix X assume "X \<in> sigma_sets \<Omega> A"
     then have "f -` X \<inter> space M \<in> sets M \<and> X \<subseteq> \<Omega>"
       proof induct
         case (Basic a) then show ?case

       next
         case (Compl a)
         have [simp]: "f -` \<Omega> \<inter> space M = space M"
           by (auto simp add: funcset_mem [OF f])
         then show ?case
-          by (auto simp add: vimage_Diff Diff_Int_distrib2 compl_sets Compl)
+          by (auto simp add: vimage_Diff Diff_Int_distrib2 sets.compl_sets Compl)
       next
         case (Union a)
         then show ?case
           by (simp add: vimage_UN, simp only: UN_extend_simps(4)) blast
       qed auto }

     ((f -` A \<inter> space M) \<inter> {x\<in>space M. P x}) \<union>
     ((g -` A \<inter> space M) \<inter> (space M - {x\<in>space M. P x}))"
     using measure unfolding measurable_def by (auto split: split_if_asm)
   show "(\<lambda>x. if P x then f x else g x) -` A \<inter> space M \<in> sets M"
     using `A \<in> sets M'` measure P unfolding * measurable_def
-    by (auto intro!: Un)
+    by (auto intro!: sets.Un)
 qed
 
 lemma measurable_If_set:
   assumes measure: "f \<in> measurable M M'" "g \<in> measurable M M'"
   assumes P: "A \<inter> space M \<in> sets M"

       have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M =
         {x\<in>space M. P i x} \<inter> (space M - (\<Union>j<i. {x\<in>space M. P j x})) \<union> (space M - (\<Union>i. {x\<in>space M. P i x}))"
         by (simp add: set_eq_iff, safe)
            (insert i, auto dest: Least_le intro: LeastI intro!: Least_equality)
       with meas show ?thesis
-        by (auto intro!: Int)
+        by (auto intro!: sets.Int)
     next
       assume i: "(LEAST j. False) \<noteq> i"
       then have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M =
         {x\<in>space M. P i x} \<inter> (space M - (\<Union>j<i. {x\<in>space M. P j x}))"
       proof (simp add: set_eq_iff, safe)

       qed (auto dest: Least_le intro!: Least_equality)
       with meas show ?thesis
         by auto
     qed }
   then have "(\<Union>i\<in>A. (\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M) \<in> sets M"
-    by (intro countable_UN) auto
+    by (intro sets.countable_UN) auto
   moreover have "(\<Union>i\<in>A. (\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M) =
     (\<lambda>x. LEAST j. P j x) -` A \<inter> space M" by auto
   ultimately show ?thesis by auto
 qed
 

   { fix X assume "X \<subseteq> A" "f \<in> space M \<rightarrow> A"
     with `finite A` have "f -` X \<inter> space M = (\<Union>a\<in>X. f -` {a} \<inter> space M)" "finite X"
       by (auto dest: finite_subset)
     moreover assume "\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M"
     ultimately have "f -` X \<inter> space M \<in> sets M"
-      using `X \<subseteq> A` by (auto intro!: finite_UN simp del: UN_simps) }
+      using `X \<subseteq> A` by (auto intro!: sets.finite_UN simp del: UN_simps) }
   then show ?thesis
     unfolding measurable_def by auto
 qed
 
 lemma measurable_compose_countable:

 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!: countable_UN measurable_sets)
+    by (auto intro!: sets.countable_UN measurable_sets)
   finally show "(\<lambda>x. f (g x) x) -` A \<inter> space M \<in> sets M" .
 qed
 
 subsection {* Measurable method *}
 

   { fix X
     have "X \<in> Pow (UNIV :: bool set)" by simp
     then have "P -` X \<inter> space M = {x\<in>space M. ((X = {True} \<longrightarrow> P x) \<and> (X = {False} \<longrightarrow> \<not> P x) \<and> X \<noteq> {})}"
       unfolding UNIV_bool Pow_insert Pow_empty by auto
     then have "P -` X \<inter> space M \<in> sets M"
-      by (auto intro!: sets_Collect_neg sets_Collect_imp sets_Collect_conj sets_Collect_const P) }
+      by (auto intro!: sets.sets_Collect_neg sets.sets_Collect_imp sets.sets_Collect_conj sets.sets_Collect_const P) }
   then show "pred M P"
     by (auto simp: measurable_def)
 qed
 
 lemma pred_sets1: "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> f \<in> measurable N M \<Longrightarrow> pred N (\<lambda>x. P (f x))"

 
 declare
   measurable_compose_rev[measurable_dest]
   pred_sets1[measurable_dest]
   pred_sets2[measurable_dest]
-  sets_into_space[measurable_dest]
+  sets.sets_into_space[measurable_dest]
 
 declare
-  top[measurable]
-  empty_sets[measurable (raw)]
-  Un[measurable (raw)]
-  Diff[measurable (raw)]
+  sets.top[measurable]
+  sets.empty_sets[measurable (raw)]
+  sets.Un[measurable (raw)]
+  sets.Diff[measurable (raw)]
 
 declare
   measurable_count_space[measurable (raw)]
   measurable_ident[measurable (raw)]
   measurable_ident_sets[measurable (raw)]

 lemma pred_intros_countable[measurable (raw)]:
   fixes P :: "'a \<Rightarrow> 'i :: countable \<Rightarrow> bool"
   shows 
     "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i. P x i)"
     "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i. P x i)"
-  by (auto intro!: sets_Collect_countable_All sets_Collect_countable_Ex simp: pred_def)
+  by (auto intro!: sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex simp: pred_def)
 
 lemma pred_intros_countable_bounded[measurable (raw)]:
   fixes X :: "'i :: countable set"
   shows 
     "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Inter>i\<in>X. N x i))"

 lemma pred_intros_finite[measurable (raw)]:
   "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Inter>i\<in>I. N x i))"
   "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>I. N x i))"
   "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>I. P x i)"
   "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>I. P x i)"
-  by (auto intro!: sets_Collect_finite_Ex sets_Collect_finite_All simp: iff_conv_conj_imp pred_def)
+  by (auto intro!: sets.sets_Collect_finite_Ex sets.sets_Collect_finite_All simp: iff_conv_conj_imp pred_def)
 
 lemma countable_Un_Int[measurable (raw)]:
   "(\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Union>i\<in>I. N i) \<in> sets M"
   "I \<noteq> {} \<Longrightarrow> (\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Inter>i\<in>I. N i) \<in> sets M"
   by auto

   assumes f: "f \<in> measurable M N" and c: "{c <..} \<in> sets N" shows "pred M (\<lambda>x. c < f x)"
   using measurable_sets[OF f c]
   by (auto simp: Int_def conj_commute eq_commute pred_def)
 
 declare
-  Int[measurable (raw)]
+  sets.Int[measurable (raw)]
 
 lemma pred_in_If[measurable (raw)]:
   "(P \<Longrightarrow> pred M (\<lambda>x. x \<in> A x)) \<Longrightarrow> (\<not> P \<Longrightarrow> pred M (\<lambda>x. x \<in> B x)) \<Longrightarrow>
     pred M (\<lambda>x. x \<in> (if P then A x else B x))"
   by auto