qualified interpretation of sigma_algebra, to avoid name clashes
authorimmler
Tue Nov 27 11:29:47 2012 +0100 (2012-11-27)
changeset 50244de72bbe42190
parent 50243 0d97ef1d6de9
child 50245 dea9363887a6
qualified interpretation of sigma_algebra, to avoid name clashes
src/HOL/Probability/Binary_Product_Measure.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Complete_Measure.thy
src/HOL/Probability/Fin_Map.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Independent_Family.thy
src/HOL/Probability/Infinite_Product_Measure.thy
src/HOL/Probability/Information.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Probability_Measure.thy
src/HOL/Probability/Projective_Family.thy
src/HOL/Probability/Projective_Limit.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/Probability/Regularity.thy
src/HOL/Probability/Sigma_Algebra.thy
     1.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Thu Nov 22 10:09:54 2012 +0100
     1.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Tue Nov 27 11:29:47 2012 +0100
     1.3 @@ -22,7 +22,7 @@
     1.4        (\<lambda>X. \<integral>\<^isup>+x. (\<integral>\<^isup>+y. indicator X (x,y) \<partial>B) \<partial>A)"
     1.5  
     1.6  lemma pair_measure_closed: "{a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B} \<subseteq> Pow (space A \<times> space B)"
     1.7 -  using space_closed[of A] space_closed[of B] by auto
     1.8 +  using sets.space_closed[of A] sets.space_closed[of B] by auto
     1.9  
    1.10  lemma space_pair_measure:
    1.11    "space (A \<Otimes>\<^isub>M B) = space A \<times> space B"
    1.12 @@ -47,7 +47,7 @@
    1.13    assumes 2: "\<And>A B. A \<in> sets M1 \<Longrightarrow> B \<in> sets M2 \<Longrightarrow> f -` (A \<times> B) \<inter> space M \<in> sets M"
    1.14    shows "f \<in> measurable M (M1 \<Otimes>\<^isub>M M2)"
    1.15    unfolding pair_measure_def using 1 2
    1.16 -  by (intro measurable_measure_of) (auto dest: sets_into_space)
    1.17 +  by (intro measurable_measure_of) (auto dest: sets.sets_into_space)
    1.18  
    1.19  lemma measurable_split_replace[measurable (raw)]:
    1.20    "(\<lambda>x. f x (fst (g x)) (snd (g x))) \<in> measurable M N \<Longrightarrow> (\<lambda>x. split (f x) (g x)) \<in> measurable M N"
    1.21 @@ -63,7 +63,7 @@
    1.22    have "(\<lambda>x. (f x, g x)) -` (A \<times> B) \<inter> space M = (f -` A \<inter> space M) \<inter> (g -` B \<inter> space M)"
    1.23      by auto
    1.24    also have "\<dots> \<in> sets M"
    1.25 -    by (rule Int) (auto intro!: measurable_sets * f g)
    1.26 +    by (rule sets.Int) (auto intro!: measurable_sets * f g)
    1.27    finally show "(\<lambda>x. (f x, g x)) -` (A \<times> B) \<inter> space M \<in> sets M" .
    1.28  qed
    1.29  
    1.30 @@ -79,10 +79,12 @@
    1.31    using measurable_Pair[OF assms] by simp
    1.32  
    1.33  lemma measurable_fst[intro!, simp, measurable]: "fst \<in> measurable (M1 \<Otimes>\<^isub>M M2) M1"
    1.34 -  by (auto simp: fst_vimage_eq_Times space_pair_measure sets_into_space times_Int_times measurable_def)
    1.35 +  by (auto simp: fst_vimage_eq_Times space_pair_measure sets.sets_into_space times_Int_times
    1.36 +    measurable_def)
    1.37  
    1.38  lemma measurable_snd[intro!, simp, measurable]: "snd \<in> measurable (M1 \<Otimes>\<^isub>M M2) M2"
    1.39 -  by (auto simp: snd_vimage_eq_Times space_pair_measure sets_into_space times_Int_times measurable_def)
    1.40 +  by (auto simp: snd_vimage_eq_Times space_pair_measure sets.sets_into_space times_Int_times
    1.41 +    measurable_def)
    1.42  
    1.43  lemma 
    1.44    assumes f[measurable]: "f \<in> measurable M (N \<Otimes>\<^isub>M P)" 
    1.45 @@ -122,7 +124,7 @@
    1.46    assumes A: "A \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "Pair x -` A \<in> sets M2"
    1.47  proof -
    1.48    have "Pair x -` A = (if x \<in> space M1 then Pair x -` A \<inter> space M2 else {})"
    1.49 -    using A[THEN sets_into_space] by (auto simp: space_pair_measure)
    1.50 +    using A[THEN sets.sets_into_space] by (auto simp: space_pair_measure)
    1.51    also have "\<dots> \<in> sets M2"
    1.52      using A by (auto simp add: measurable_Pair1' intro!: measurable_sets split: split_if_asm)
    1.53    finally show ?thesis .
    1.54 @@ -134,7 +136,7 @@
    1.55  lemma sets_Pair2: assumes A: "A \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "(\<lambda>x. (x, y)) -` A \<in> sets M1"
    1.56  proof -
    1.57    have "(\<lambda>x. (x, y)) -` A = (if y \<in> space M2 then (\<lambda>x. (x, y)) -` A \<inter> space M1 else {})"
    1.58 -    using A[THEN sets_into_space] by (auto simp: space_pair_measure)
    1.59 +    using A[THEN sets.sets_into_space] by (auto simp: space_pair_measure)
    1.60    also have "\<dots> \<in> sets M1"
    1.61      using A by (auto simp add: measurable_Pair2' intro!: measurable_sets split: split_if_asm)
    1.62    finally show ?thesis .
    1.63 @@ -167,11 +169,11 @@
    1.64    unfolding sets_pair_measure
    1.65  proof (induct rule: sigma_sets_induct_disjoint)
    1.66    case (compl A)
    1.67 -  with sets_into_space have "\<And>x. emeasure M (Pair x -` ((space N \<times> space M) - A)) =
    1.68 +  with sets.sets_into_space have "\<And>x. emeasure M (Pair x -` ((space N \<times> space M) - A)) =
    1.69        (if x \<in> space N then emeasure M (space M) - ?s A x else 0)"
    1.70      unfolding sets_pair_measure[symmetric]
    1.71      by (auto intro!: emeasure_compl simp: vimage_Diff sets_Pair1)
    1.72 -  with compl top show ?case
    1.73 +  with compl sets.top show ?case
    1.74      by (auto intro!: measurable_If simp: space_pair_measure)
    1.75  next
    1.76    case (union F)
    1.77 @@ -189,7 +191,7 @@
    1.78    let ?C = "\<lambda>x i. F i \<inter> Pair x -` Q"
    1.79    { fix i
    1.80      have [simp]: "space N \<times> F i \<inter> space N \<times> space M = space N \<times> F i"
    1.81 -      using F sets_into_space by auto
    1.82 +      using F sets.sets_into_space by auto
    1.83      let ?R = "density M (indicator (F i))"
    1.84      have "finite_measure ?R"
    1.85        using F by (intro finite_measureI) (auto simp: emeasure_restricted subset_eq)
    1.86 @@ -199,7 +201,7 @@
    1.87          = emeasure M (F i \<inter> Pair x -` (space N \<times> space ?R \<inter> Q))"
    1.88        using Q F_sets by (intro emeasure_restricted) (auto intro: sets_Pair1)
    1.89      moreover have "\<And>x. F i \<inter> Pair x -` (space N \<times> space ?R \<inter> Q) = ?C x i"
    1.90 -      using sets_into_space[OF Q] by (auto simp: space_pair_measure)
    1.91 +      using sets.sets_into_space[OF Q] by (auto simp: space_pair_measure)
    1.92      ultimately have "(\<lambda>x. emeasure M (?C x i)) \<in> borel_measurable N"
    1.93        by simp }
    1.94    moreover
    1.95 @@ -213,7 +215,7 @@
    1.96          by (rule disjoint_family_on_bisimulation[OF `disjoint_family F`]) auto
    1.97      qed
    1.98      also have "(\<Union>i. ?C x i) = Pair x -` Q"
    1.99 -      using F sets_into_space[OF `Q \<in> sets (N \<Otimes>\<^isub>M M)`]
   1.100 +      using F sets.sets_into_space[OF `Q \<in> sets (N \<Otimes>\<^isub>M M)`]
   1.101        by (auto simp: space_pair_measure)
   1.102      finally have "emeasure M (Pair x -` Q) = (\<Sum>i. emeasure M (?C x i))"
   1.103        by simp }
   1.104 @@ -255,7 +257,7 @@
   1.105                 intro!: positive_integral_cong positive_integral_indicator[symmetric])
   1.106    qed
   1.107    show "{a \<times> b |a b. a \<in> sets N \<and> b \<in> sets M} \<subseteq> Pow (space N \<times> space M)"
   1.108 -    using space_closed[of N] space_closed[of M] by auto
   1.109 +    using sets.space_closed[of N] sets.space_closed[of M] by auto
   1.110  qed fact
   1.111  
   1.112  lemma (in sigma_finite_measure) emeasure_pair_measure_alt:
   1.113 @@ -296,7 +298,7 @@
   1.114      using Q measurable_pair_swap' by (auto intro: measurable_sets)
   1.115    note M1.measurable_emeasure_Pair[OF this]
   1.116    moreover have "\<And>y. Pair y -` ((\<lambda>(x, y). (y, x)) -` Q \<inter> space (M2 \<Otimes>\<^isub>M M1)) = (\<lambda>x. (x, y)) -` Q"
   1.117 -    using Q[THEN sets_into_space] by (auto simp: space_pair_measure)
   1.118 +    using Q[THEN sets.sets_into_space] by (auto simp: space_pair_measure)
   1.119    ultimately show ?thesis by simp
   1.120  qed
   1.121  
   1.122 @@ -374,7 +376,7 @@
   1.123    show ?thesis
   1.124    proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]])
   1.125      show "?E \<subseteq> Pow (space ?P)"
   1.126 -      using space_closed[of M1] space_closed[of M2] by (auto simp: space_pair_measure)
   1.127 +      using sets.space_closed[of M1] sets.space_closed[of M2] by (auto simp: space_pair_measure)
   1.128      show "sets ?P = sigma_sets (space ?P) ?E"
   1.129        by (simp add: sets_pair_measure space_pair_measure)
   1.130      then show "sets ?D = sigma_sets (space ?P) ?E"
   1.131 @@ -386,7 +388,7 @@
   1.132      fix X assume "X \<in> ?E"
   1.133      then obtain A B where X[simp]: "X = A \<times> B" and A: "A \<in> sets M1" and B: "B \<in> sets M2" by auto
   1.134      have "(\<lambda>(y, x). (x, y)) -` X \<inter> space (M2 \<Otimes>\<^isub>M M1) = B \<times> A"
   1.135 -      using sets_into_space[OF A] sets_into_space[OF B] by (auto simp: space_pair_measure)
   1.136 +      using sets.sets_into_space[OF A] sets.sets_into_space[OF B] by (auto simp: space_pair_measure)
   1.137      with A B show "emeasure (M1 \<Otimes>\<^isub>M M2) X = emeasure ?D X"
   1.138        by (simp add: M2.emeasure_pair_measure_Times M1.emeasure_pair_measure_Times emeasure_distr
   1.139                      measurable_pair_swap' ac_simps)
   1.140 @@ -399,7 +401,7 @@
   1.141      (is "_ = ?\<nu> A")
   1.142  proof -
   1.143    have [simp]: "\<And>y. (Pair y -` ((\<lambda>(x, y). (y, x)) -` A \<inter> space (M2 \<Otimes>\<^isub>M M1))) = (\<lambda>x. (x, y)) -` A"
   1.144 -    using sets_into_space[OF A] by (auto simp: space_pair_measure)
   1.145 +    using sets.sets_into_space[OF A] by (auto simp: space_pair_measure)
   1.146    show ?thesis using A
   1.147      by (subst distr_pair_swap)
   1.148         (simp_all del: vimage_Int add: measurable_sets[OF measurable_pair_swap']
   1.149 @@ -438,7 +440,7 @@
   1.150    shows "AE x in M1 \<Otimes>\<^isub>M M2. P x"
   1.151  proof (subst AE_iff_measurable[OF _ refl])
   1.152    show "{x\<in>space (M1 \<Otimes>\<^isub>M M2). \<not> P x} \<in> sets (M1 \<Otimes>\<^isub>M M2)"
   1.153 -    by (rule sets_Collect) fact
   1.154 +    by (rule sets.sets_Collect) fact
   1.155    then have "emeasure (M1 \<Otimes>\<^isub>M M2) {x \<in> space (M1 \<Otimes>\<^isub>M M2). \<not> P x} =
   1.156        (\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. indicator {x \<in> space (M1 \<Otimes>\<^isub>M M2). \<not> P x} (x, y) \<partial>M2 \<partial>M1)"
   1.157      by (simp add: M2.emeasure_pair_measure)
   1.158 @@ -790,7 +792,7 @@
   1.159    show ?thesis
   1.160    proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]])
   1.161      show "?E \<subseteq> Pow (space ?P)"
   1.162 -      using space_closed[of M1] space_closed[of M2] by (auto simp: space_pair_measure)
   1.163 +      using sets.space_closed[of M1] sets.space_closed[of M2] by (auto simp: space_pair_measure)
   1.164      show "sets ?P = sigma_sets (space ?P) ?E"
   1.165        by (simp add: sets_pair_measure space_pair_measure)
   1.166      then show "sets M = sigma_sets (space ?P) ?E"
     2.1 --- a/src/HOL/Probability/Borel_Space.thy	Thu Nov 22 10:09:54 2012 +0100
     2.2 +++ b/src/HOL/Probability/Borel_Space.thy	Tue Nov 27 11:29:47 2012 +0100
     2.3 @@ -53,7 +53,7 @@
     2.4  
     2.5  lemma borel_singleton[measurable]:
     2.6    "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets (borel :: 'a::t1_space measure)"
     2.7 -  unfolding insert_def by (rule Un) auto
     2.8 +  unfolding insert_def by (rule sets.Un) auto
     2.9  
    2.10  lemma borel_comp[measurable]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
    2.11    unfolding Compl_eq_Diff_UNIV by simp
    2.12 @@ -180,7 +180,7 @@
    2.13  
    2.14  lemma borel_sigma_sets_subset:
    2.15    "A \<subseteq> sets borel \<Longrightarrow> sigma_sets UNIV A \<subseteq> sets borel"
    2.16 -  using sigma_sets_subset[of A borel] by simp
    2.17 +  using sets.sigma_sets_subset[of A borel] by simp
    2.18  
    2.19  lemma borel_eq_sigmaI1:
    2.20    fixes F :: "'i \<Rightarrow> 'a::topological_space set" and X :: "'a::topological_space set set"
    2.21 @@ -276,7 +276,8 @@
    2.22      by blast
    2.23    show "S \<in> ?SIGMA"
    2.24      unfolding *
    2.25 -    by (safe intro!: countable_UN Int countable_INT) (auto intro!: halfspace_gt_in_halfspace)
    2.26 +    by (safe intro!: sets.countable_UN sets.Int sets.countable_INT)
    2.27 +      (auto intro!: halfspace_gt_in_halfspace)
    2.28  qed auto
    2.29  
    2.30  lemma borel_eq_halfspace_le:
    2.31 @@ -299,7 +300,7 @@
    2.32      finally show "x$$i < a" .
    2.33    qed
    2.34    show "{x. x$$i < a} \<in> ?SIGMA" unfolding *
    2.35 -    by (safe intro!: countable_UN) auto
    2.36 +    by (safe intro!: sets.countable_UN) auto
    2.37  qed auto
    2.38  
    2.39  lemma borel_eq_halfspace_ge:
    2.40 @@ -308,7 +309,7 @@
    2.41  proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_less])
    2.42    fix a i have *: "{x::'a. x$$i < a} = space ?SIGMA - {x::'a. a \<le> x$$i}" by auto
    2.43    show "{x. x$$i < a} \<in> ?SIGMA" unfolding *
    2.44 -      by (safe intro!: compl_sets) auto
    2.45 +      by (safe intro!: sets.compl_sets) auto
    2.46  qed auto
    2.47  
    2.48  lemma borel_eq_halfspace_greater:
    2.49 @@ -317,7 +318,7 @@
    2.50  proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_le])
    2.51    fix a i have *: "{x::'a. x$$i \<le> a} = space ?SIGMA - {x::'a. a < x$$i}" by auto
    2.52    show "{x. x$$i \<le> a} \<in> ?SIGMA" unfolding *
    2.53 -    by (safe intro!: compl_sets) auto
    2.54 +    by (safe intro!: sets.compl_sets) auto
    2.55  qed auto
    2.56  
    2.57  lemma borel_eq_atMost:
    2.58 @@ -337,7 +338,7 @@
    2.59          by (auto intro!: exI[of _ k])
    2.60      qed
    2.61      show "{x. x$$i \<le> a} \<in> ?SIGMA" unfolding *
    2.62 -      by (safe intro!: countable_UN) auto
    2.63 +      by (safe intro!: sets.countable_UN) auto
    2.64    qed (auto intro: sigma_sets_top sigma_sets.Empty)
    2.65  qed auto
    2.66  
    2.67 @@ -363,7 +364,7 @@
    2.68      qed
    2.69      finally show "{x. x$$i \<le> a} \<in> ?SIGMA"
    2.70        apply (simp only:)
    2.71 -      apply (safe intro!: countable_UN Diff)
    2.72 +      apply (safe intro!: sets.countable_UN sets.Diff)
    2.73        apply (auto intro: sigma_sets_top)
    2.74        done
    2.75    qed (auto intro: sigma_sets_top sigma_sets.Empty)
    2.76 @@ -391,7 +392,7 @@
    2.77      qed
    2.78      finally show "{x. a \<le> x$$i} \<in> ?SIGMA"
    2.79        apply (simp only:)
    2.80 -      apply (safe intro!: countable_UN Diff)
    2.81 +      apply (safe intro!: sets.countable_UN sets.Diff)
    2.82        apply (auto intro: sigma_sets_top)
    2.83        done
    2.84    qed (auto intro: sigma_sets_top sigma_sets.Empty)
    2.85 @@ -415,7 +416,7 @@
    2.86        by (auto intro!: exI[of _ k])
    2.87    qed
    2.88    show "{..a} \<in> ?SIGMA" unfolding *
    2.89 -    by (safe intro!: countable_UN)
    2.90 +    by (safe intro!: sets.countable_UN)
    2.91         (auto intro!: sigma_sets_top)
    2.92  qed auto
    2.93  
    2.94 @@ -427,7 +428,7 @@
    2.95    then have "open M" by simp
    2.96    show "M \<in> ?SIGMA"
    2.97      apply (subst open_UNION[OF `open M`])
    2.98 -    apply (safe intro!: countable_UN)
    2.99 +    apply (safe intro!: sets.countable_UN)
   2.100      apply auto
   2.101      done
   2.102  qed auto
     3.1 --- a/src/HOL/Probability/Complete_Measure.thy	Thu Nov 22 10:09:54 2012 +0100
     3.2 +++ b/src/HOL/Probability/Complete_Measure.thy	Tue Nov 27 11:29:47 2012 +0100
     3.3 @@ -22,7 +22,7 @@
     3.4  
     3.5  lemma completion_into_space:
     3.6    "{ S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' } \<subseteq> Pow (space M)"
     3.7 -  using sets_into_space by auto
     3.8 +  using sets.sets_into_space by auto
     3.9  
    3.10  lemma space_completion[simp]: "space (completion M) = space M"
    3.11    unfolding completion_def using space_measure_of[OF completion_into_space] by simp
    3.12 @@ -43,7 +43,7 @@
    3.13    unfolding sigma_algebra_iff2
    3.14  proof (intro conjI ballI allI impI)
    3.15    show "?A \<subseteq> Pow (space M)"
    3.16 -    using sets_into_space by auto
    3.17 +    using sets.sets_into_space by auto
    3.18  next
    3.19    show "{} \<in> ?A" by auto
    3.20  next
    3.21 @@ -238,7 +238,7 @@
    3.22        (if x \<in> ?N then ?F undefined \<union> ?N
    3.23         else if f x = undefined then ?F (f x) \<union> ?N
    3.24         else ?F (f x) - ?N)"
    3.25 -      using N(2) sets_into_space by (auto split: split_if_asm simp: null_sets_def)
    3.26 +      using N(2) sets.sets_into_space by (auto split: split_if_asm simp: null_sets_def)
    3.27      moreover { fix y have "?F y \<union> ?N \<in> sets M"
    3.28        proof cases
    3.29          assume y: "y \<in> f`space M"
     4.1 --- a/src/HOL/Probability/Fin_Map.thy	Thu Nov 22 10:09:54 2012 +0100
     4.2 +++ b/src/HOL/Probability/Fin_Map.thy	Tue Nov 27 11:29:47 2012 +0100
     4.3 @@ -620,7 +620,7 @@
     4.4  
     4.5  lemma PiF_gen_subset: "{(\<Pi>' j\<in>J. X j) |X J. J \<in> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))} \<subseteq>
     4.6      Pow (\<Union>J \<in> I. (\<Pi>' j\<in>J. space (M j)))"
     4.7 -  by (auto simp: Pi'_def) (blast dest: sets_into_space)
     4.8 +  by (auto simp: Pi'_def) (blast dest: sets.sets_into_space)
     4.9  
    4.10  lemma space_PiF: "space (PiF I M) = (\<Union>J \<in> I. (\<Pi>' j\<in>J. space (M j)))"
    4.11    unfolding PiF_def using PiF_gen_subset by (rule space_measure_of)
    4.12 @@ -757,7 +757,7 @@
    4.13        done
    4.14    qed
    4.15    also have "\<dots> \<in> sets (PiF I M)"
    4.16 -    apply (intro Int countable_nat_UN subsetI, safe)
    4.17 +    apply (intro sets.Int sets.countable_nat_UN subsetI, safe)
    4.18      apply (case_tac "set (from_nat i) \<in> I")
    4.19      apply simp_all
    4.20      apply (rule singleton_subspace_set_in_sets[OF measurable_sets[OF MN]])
    4.21 @@ -807,7 +807,7 @@
    4.22    case (Union a)
    4.23    have "UNION UNIV a \<inter> {m. domain m \<in> J} = (\<Union>i. (a i \<inter> {m. domain m \<in> J}))"
    4.24      by simp
    4.25 -  also have "\<dots> \<in> sets (PiF J M)" using Union by (intro countable_nat_UN) auto
    4.26 +  also have "\<dots> \<in> sets (PiF J M)" using Union by (intro sets.countable_nat_UN) auto
    4.27    finally show ?case .
    4.28  next
    4.29    case (Compl a)
    4.30 @@ -838,10 +838,10 @@
    4.31    show "(\<lambda>x. finmap_of (J x) (f x)) -` Pi' K S \<inter> space N \<in> sets N"
    4.32      unfolding eq r
    4.33      apply (simp del: INT_simps add: )
    4.34 -    apply (intro conjI impI finite_INT JN Int[OF top])
    4.35 +    apply (intro conjI impI sets.finite_INT JN sets.Int[OF sets.top])
    4.36      apply simp apply assumption
    4.37      apply (subst Int_assoc[symmetric])
    4.38 -    apply (rule Int)
    4.39 +    apply (rule sets.Int)
    4.40      apply (intro measurable_sets[OF f] *) apply force apply assumption
    4.41      apply (intro JN)
    4.42      done
    4.43 @@ -865,7 +865,7 @@
    4.44    assume "i \<in> I"
    4.45    hence "(\<lambda>x. (x)\<^isub>F i) -` A \<inter> space (PiF {I} M) =
    4.46      Pi' I (\<lambda>x. if x = i then A else space (M x))"
    4.47 -    using sets_into_space[OF ] `A \<in> sets (M i)` assms
    4.48 +    using sets.sets_into_space[OF ] `A \<in> sets (M i)` assms
    4.49      by (auto simp: space_PiF Pi'_def)
    4.50    thus ?thesis  using assms `A \<in> sets (M i)`
    4.51      by (intro in_sets_PiFI) auto
    4.52 @@ -934,7 +934,7 @@
    4.53    shows "A \<inter> B \<in> sets M" using assms
    4.54  proof -
    4.55    have "A \<inter> B = (A \<inter> space M) \<inter> B"
    4.56 -    using assms sets_into_space by auto
    4.57 +    using assms sets.sets_into_space by auto
    4.58    thus ?thesis using assms by auto
    4.59  qed
    4.60  
    4.61 @@ -959,7 +959,7 @@
    4.62    show "A \<in> sigma_sets ?\<Omega> ?R"
    4.63    proof -
    4.64      from `I \<noteq> {}` X have "A = (\<Inter>j\<in>I. {f\<in>space (PiF {I} M). f j \<in> X j})"
    4.65 -      using sets_into_space
    4.66 +      using sets.sets_into_space
    4.67        by (auto simp: space_PiF product_def) blast
    4.68      also have "\<dots> \<in> sigma_sets ?\<Omega> ?R"
    4.69        using X `I \<noteq> {}` assms by (intro R.finite_INT) (auto simp: space_PiF)
    4.70 @@ -970,7 +970,7 @@
    4.71    then obtain i B where A: "A = {f\<in>\<Pi>' i\<in>I. space (M i). f i \<in> B}" "i \<in> I" "B \<in> sets (M i)"
    4.72      by auto
    4.73    then have "A = (\<Pi>' j \<in> I. if j = i then B else space (M j))"
    4.74 -    using sets_into_space[OF A(3)]
    4.75 +    using sets.sets_into_space[OF A(3)]
    4.76      apply (auto simp: Pi'_iff split: split_if_asm)
    4.77      apply blast
    4.78      done
    4.79 @@ -1033,7 +1033,7 @@
    4.80        sigma_sets (space ?P) {{f \<in> \<Pi>' i\<in>I. space (M i). f i \<in> A} |i A. i \<in> I \<and> A \<in> sets (M i)}"
    4.81      using sets_PiF_single[of I M] by (simp add: space_P)
    4.82    also have "\<dots> \<subseteq> sets (sigma (space (PiF {I} M)) P)"
    4.83 -  proof (safe intro!: sigma_sets_subset)
    4.84 +  proof (safe intro!: sets.sigma_sets_subset)
    4.85      fix i A assume "i \<in> I" and A: "A \<in> sets (M i)"
    4.86      have "(\<lambda>x. (x)\<^isub>F i) \<in> measurable ?P (sigma (space (M i)) (E i))"
    4.87      proof (subst measurable_iff_measure_of)
    4.88 @@ -1051,7 +1051,7 @@
    4.89            using S_mono
    4.90            by (subst Pi'_UN[symmetric, OF `finite I`]) (auto simp: incseq_def)
    4.91          also have "\<dots> \<in> sets ?P"
    4.92 -        proof (safe intro!: countable_UN)
    4.93 +        proof (safe intro!: sets.countable_UN)
    4.94            fix n show "(\<Pi>' j\<in>I. if i = j then A else S j n) \<in> sets ?P"
    4.95              using A S_in_E
    4.96              by (simp add: P_closed)
    4.97 @@ -1072,7 +1072,7 @@
    4.98      by (simp add: P_closed)
    4.99    show "sigma_sets (space (PiF {I} M)) P \<subseteq> sets (PiF {I} M)"
   4.100      using `finite I` `I \<noteq> {}`
   4.101 -    by (auto intro!: sigma_sets_subset product_in_sets_PiFI simp: E_generates P_def)
   4.102 +    by (auto intro!: sets.sigma_sets_subset product_in_sets_PiFI simp: E_generates P_def)
   4.103  qed
   4.104  
   4.105  lemma enumerable_sigma_fprod_algebra_sigma_eq:
   4.106 @@ -1176,7 +1176,7 @@
   4.107      show "sets (PiF (Collect finite) (\<lambda>_. borel)) \<subseteq> sets (borel::('i \<Rightarrow>\<^isub>F 'a) measure)"
   4.108      proof
   4.109        fix x assume x: "x \<in> sets (PiF (Collect finite::'i set set) (\<lambda>_. borel::'a measure))"
   4.110 -      hence x_sp: "x \<subseteq> space (PiF (Collect finite) (\<lambda>_. borel))" by (rule sets_into_space)
   4.111 +      hence x_sp: "x \<subseteq> space (PiF (Collect finite) (\<lambda>_. borel))" by (rule sets.sets_into_space)
   4.112        let ?x = "\<lambda>J. x \<inter> {x. domain x = J}"
   4.113        have "x = \<Union>{?x J |J. finite J}" by auto
   4.114        also have "\<dots> \<in> sets borel"
   4.115 @@ -1316,7 +1316,7 @@
   4.116    have "mf (fm x) \<in> extensional J"
   4.117      by (auto simp: mf_def extensional_def compose_def)
   4.118    moreover
   4.119 -  have "x \<in> extensional J" using assms sets_into_space
   4.120 +  have "x \<in> extensional J" using assms sets.sets_into_space
   4.121      by (force simp: space_PiM PiE_def)
   4.122    moreover
   4.123    { fix i assume "i \<in> J"
   4.124 @@ -1344,7 +1344,7 @@
   4.125    have "fm ` X = (mf) -` X \<inter> space (PiF {f ` J} (\<lambda>_. M))"
   4.126    proof safe
   4.127      fix x assume "x \<in> X"
   4.128 -    with mf_fm[of x] sets_into_space[OF assms(2)] show "fm x \<in> mf -` X" by auto
   4.129 +    with mf_fm[of x] sets.sets_into_space[OF assms(2)] show "fm x \<in> mf -` X" by auto
   4.130      show "fm x \<in> space (PiF {f ` J} (\<lambda>_. M))" by (simp add: space_PiF assms)
   4.131    next
   4.132      fix y x
   4.133 @@ -1396,7 +1396,7 @@
   4.134    shows "emeasure M X = emeasure (mapmeasure M (\<lambda>_. N)) (fm ` X)"
   4.135    unfolding mapmeasure_def
   4.136  proof (subst emeasure_distr, subst measurable_eqI[OF s1 refl s2 refl], rule fm_measurable)
   4.137 -  have "X \<subseteq> space (Pi\<^isub>M J (\<lambda>_. N))" using assms by (simp add: sets_into_space)
   4.138 +  have "X \<subseteq> space (Pi\<^isub>M J (\<lambda>_. N))" using assms by (simp add: sets.sets_into_space)
   4.139    from assms inj_on_fm[of "\<lambda>_. N"] set_mp[OF this] have "fm -` fm ` X \<inter> space (Pi\<^isub>M J (\<lambda>_. N)) = X"
   4.140      by (auto simp: vimage_image_eq inj_on_def)
   4.141    thus "emeasure M X = emeasure M (fm -` fm ` X \<inter> space M)" using s1
     5.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Thu Nov 22 10:09:54 2012 +0100
     5.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Tue Nov 27 11:29:47 2012 +0100
     5.3 @@ -140,7 +140,7 @@
     5.4  lemma prod_emb_Pi:
     5.5    assumes "X \<in> (\<Pi> j\<in>J. sets (M j))" "J \<subseteq> K"
     5.6    shows "prod_emb K M J (Pi\<^isub>E J X) = (\<Pi>\<^isub>E i\<in>K. if i \<in> J then X i else space (M i))"
     5.7 -  using assms space_closed
     5.8 +  using assms sets.space_closed
     5.9    by (auto simp: prod_emb_def PiE_iff split: split_if_asm) blast+
    5.10  
    5.11  lemma prod_emb_id:
    5.12 @@ -190,14 +190,14 @@
    5.13      by (auto simp: prod_algebra_def)
    5.14    let ?A = "\<Pi>\<^isub>E i\<in>I. if i \<in> J then E i else space (M i)"
    5.15    have A: "A = ?A"
    5.16 -    unfolding A using J by (intro prod_emb_PiE sets_into_space) auto
    5.17 -  show "A \<in> ?R" unfolding A using J top
    5.18 +    unfolding A using J by (intro prod_emb_PiE sets.sets_into_space) auto
    5.19 +  show "A \<in> ?R" unfolding A using J sets.top
    5.20      by (intro CollectI exI[of _ "\<lambda>i. if i \<in> J then E i else space (M i)"]) simp
    5.21  next
    5.22    fix A assume "A \<in> ?R"
    5.23    then obtain X where A: "A = (\<Pi>\<^isub>E i\<in>I. X i)" and X: "X \<in> (\<Pi> j\<in>I. sets (M j))" by auto
    5.24    then have A: "A = prod_emb I M I (\<Pi>\<^isub>E i\<in>I. X i)"
    5.25 -    by (simp add: prod_emb_PiE_same_index[OF sets_into_space] Pi_iff)
    5.26 +    by (simp add: prod_emb_PiE_same_index[OF sets.sets_into_space] Pi_iff)
    5.27    from X I show "A \<in> ?L" unfolding A
    5.28      by (auto simp: prod_algebra_def)
    5.29  qed
    5.30 @@ -209,7 +209,7 @@
    5.31  
    5.32  lemma prod_algebraI_finite:
    5.33    "finite I \<Longrightarrow> (\<forall>i\<in>I. E i \<in> sets (M i)) \<Longrightarrow> (Pi\<^isub>E I E) \<in> prod_algebra I M"
    5.34 -  using prod_algebraI[of I I E M] prod_emb_PiE_same_index[of I E M, OF sets_into_space] by simp
    5.35 +  using prod_algebraI[of I I E M] prod_emb_PiE_same_index[of I E M, OF sets.sets_into_space] by simp
    5.36  
    5.37  lemma Int_stable_PiE: "Int_stable {Pi\<^isub>E J E | E. \<forall>i\<in>I. E i \<in> sets (M i)}"
    5.38  proof (safe intro!: Int_stableI)
    5.39 @@ -232,11 +232,11 @@
    5.40      and J: "J \<subseteq> I" and E: "E \<in> (\<Pi> i\<in>J. sets (M i))"
    5.41      by (auto simp: prod_algebra_def)
    5.42    from E have "\<And>i. i \<in> J \<Longrightarrow> E i \<subseteq> space (M i)"
    5.43 -    using sets_into_space by auto
    5.44 +    using sets.sets_into_space by auto
    5.45    then have "A = (\<Pi>\<^isub>E i\<in>I. if i\<in>J then E i else space (M i))"
    5.46      using A J by (auto simp: prod_emb_PiE)
    5.47    moreover then have "(\<lambda>i. if i\<in>J then E i else space (M i)) \<in> (\<Pi> i\<in>I. sets (M i))"
    5.48 -    using top E by auto
    5.49 +    using sets.top E by auto
    5.50    ultimately show ?thesis using that by auto
    5.51  qed
    5.52  
    5.53 @@ -248,7 +248,8 @@
    5.54    from prod_algebraE[OF this] guess K F . note B = this
    5.55    have "A \<inter> B = prod_emb I M (J \<union> K) (\<Pi>\<^isub>E i\<in>J \<union> K. (if i \<in> J then E i else space (M i)) \<inter> 
    5.56        (if i \<in> K then F i else space (M i)))"
    5.57 -    unfolding A B using A(2,3,4) A(5)[THEN sets_into_space] B(2,3,4) B(5)[THEN sets_into_space]
    5.58 +    unfolding A B using A(2,3,4) A(5)[THEN sets.sets_into_space] B(2,3,4)
    5.59 +      B(5)[THEN sets.sets_into_space]
    5.60      apply (subst (1 2 3) prod_emb_PiE)
    5.61      apply (simp_all add: subset_eq PiE_Int)
    5.62      apply blast
    5.63 @@ -418,14 +419,14 @@
    5.64  lemma sets_PiM_I_finite[measurable]:
    5.65    assumes "finite I" and sets: "(\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i))"
    5.66    shows "(PIE j:I. E j) \<in> sets (PIM i:I. M i)"
    5.67 -  using sets_PiM_I[of I I E M] sets_into_space[OF sets] `finite I` sets by auto
    5.68 +  using sets_PiM_I[of I I E M] sets.sets_into_space[OF sets] `finite I` sets by auto
    5.69  
    5.70  lemma measurable_component_singleton:
    5.71    assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>M I M) (M i)"
    5.72  proof (unfold measurable_def, intro CollectI conjI ballI)
    5.73    fix A assume "A \<in> sets (M i)"
    5.74    then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M I M) = prod_emb I M {i} (\<Pi>\<^isub>E j\<in>{i}. A)"
    5.75 -    using sets_into_space `i \<in> I`
    5.76 +    using sets.sets_into_space `i \<in> I`
    5.77      by (fastforce dest: Pi_mem simp: prod_emb_def space_PiM split: split_if_asm)
    5.78    then show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M I M) \<in> sets (Pi\<^isub>M I M)"
    5.79      using `A \<in> sets (M i)` `i \<in> I` by (auto intro!: sets_PiM_I)
    5.80 @@ -460,7 +461,7 @@
    5.81    fix j A assume j: "j \<in> insert i I" and A: "A \<in> sets (M j)"
    5.82    have "{\<omega> \<in> space ?P. (\<lambda>(f, x). fun_upd f i x) \<omega> j \<in> A} =
    5.83      (if j = i then space (Pi\<^isub>M I M) \<times> A else ((\<lambda>x. x j) \<circ> fst) -` A \<inter> space ?P)"
    5.84 -    using sets_into_space[OF A] by (auto simp add: space_pair_measure space_PiM)
    5.85 +    using sets.sets_into_space[OF A] by (auto simp add: space_pair_measure space_PiM)
    5.86    also have "\<dots> \<in> sets ?P"
    5.87      using A j
    5.88      by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
    5.89 @@ -560,7 +561,7 @@
    5.90      fix i k show "emeasure (M i) (F i k) \<noteq> \<infinity>" by fact
    5.91    next
    5.92      fix x assume "x \<in> (\<Union>i. ?F i)" with F(1) show "x \<in> space (PiM I M)"
    5.93 -      by (auto simp: PiE_def dest!: sets_into_space)
    5.94 +      by (auto simp: PiE_def dest!: sets.sets_into_space)
    5.95    next
    5.96      fix f assume "f \<in> space (PiM I M)"
    5.97      with Pi_UN[OF finite_index, of "\<lambda>k i. F i k"] F
    5.98 @@ -584,7 +585,7 @@
    5.99      show "positive (PiM {} M) ?\<mu>"
   5.100        by (auto simp: positive_def)
   5.101      show "countably_additive (PiM {} M) ?\<mu>"
   5.102 -      by (rule countably_additiveI_finite)
   5.103 +      by (rule sets.countably_additiveI_finite)
   5.104           (auto simp: additive_def positive_def sets_PiM_empty space_PiM_empty intro!: )
   5.105    qed (auto simp: prod_emb_def)
   5.106    also have "(prod_emb {} M {} (\<Pi>\<^isub>E i\<in>{}. {})) = {\<lambda>_. undefined}"
   5.107 @@ -621,13 +622,13 @@
   5.108        emeasure (Pi\<^isub>M I M \<Otimes>\<^isub>M (M i)) (?h -` ?p \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i))"
   5.109        by (intro emeasure_distr measurable_add_dim sets_PiM_I) fact+
   5.110      also have "?h -` ?p \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) = ?p' \<times> (if i \<in> J then E i else space (M i))"
   5.111 -      using J E[rule_format, THEN sets_into_space]
   5.112 +      using J E[rule_format, THEN sets.sets_into_space]
   5.113        by (force simp: space_pair_measure space_PiM prod_emb_iff PiE_def Pi_iff split: split_if_asm)
   5.114      also have "emeasure (Pi\<^isub>M I M \<Otimes>\<^isub>M (M i)) (?p' \<times> (if i \<in> J then E i else space (M i))) =
   5.115        emeasure (Pi\<^isub>M I M) ?p' * emeasure (M i) (if i \<in> J then (E i) else space (M i))"
   5.116        using J E by (intro M.emeasure_pair_measure_Times sets_PiM_I) auto
   5.117      also have "?p' = (\<Pi>\<^isub>E j\<in>I. if j \<in> J-{i} then E j else space (M j))"
   5.118 -      using J E[rule_format, THEN sets_into_space]
   5.119 +      using J E[rule_format, THEN sets.sets_into_space]
   5.120        by (auto simp: prod_emb_iff PiE_def Pi_iff split: split_if_asm) blast+
   5.121      also have "emeasure (Pi\<^isub>M I M) (\<Pi>\<^isub>E j\<in>I. if j \<in> J-{i} then E j else space (M j)) =
   5.122        (\<Prod> j\<in>I. if j \<in> J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))"
   5.123 @@ -640,7 +641,7 @@
   5.124      finally show "?\<mu> ?p = \<dots>" .
   5.125  
   5.126      show "prod_emb (insert i I) M J (Pi\<^isub>E J E) \<in> Pow (\<Pi>\<^isub>E i\<in>insert i I. space (M i))"
   5.127 -      using J E[rule_format, THEN sets_into_space] by (auto simp: prod_emb_iff PiE_def)
   5.128 +      using J E[rule_format, THEN sets.sets_into_space] by (auto simp: prod_emb_iff PiE_def)
   5.129    next
   5.130      show "positive (sets (Pi\<^isub>M (insert i I) M)) ?\<mu>" "countably_additive (sets (Pi\<^isub>M (insert i I) M)) ?\<mu>"
   5.131        using emeasure_positive[of ?P] emeasure_countably_additive[of ?P] by simp_all
   5.132 @@ -650,7 +651,7 @@
   5.133        using insert by auto
   5.134    qed (auto intro!: setprod_cong)
   5.135    with insert show ?case
   5.136 -    by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets_into_space)
   5.137 +    by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets.sets_into_space)
   5.138  qed simp
   5.139  
   5.140  lemma (in product_sigma_finite) sigma_finite: 
   5.141 @@ -750,7 +751,7 @@
   5.142      let ?B = "Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M"
   5.143      let ?X = "?g -` A \<inter> space ?B"
   5.144      have "Pi\<^isub>E I F \<subseteq> space (Pi\<^isub>M I M)" "Pi\<^isub>E J F \<subseteq> space (Pi\<^isub>M J M)"
   5.145 -      using F[rule_format, THEN sets_into_space] by (force simp: space_PiM)+
   5.146 +      using F[rule_format, THEN sets.sets_into_space] by (force simp: space_PiM)+
   5.147      then have X: "?X = (Pi\<^isub>E I F \<times> Pi\<^isub>E J F)"
   5.148        unfolding A_eq by (subst merge_vimage) (auto simp: space_pair_measure space_PiM)
   5.149      have "emeasure ?D A = emeasure ?B ?X"
   5.150 @@ -792,7 +793,7 @@
   5.151    interpret I: finite_product_sigma_finite M "{i}" by default simp
   5.152    fix A assume A: "A \<in> sets (M i)"
   5.153    moreover then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M {i} M) = (\<Pi>\<^isub>E i\<in>{i}. A)"
   5.154 -    using sets_into_space by (auto simp: space_PiM)
   5.155 +    using sets.sets_into_space by (auto simp: space_PiM)
   5.156    ultimately show "emeasure (M i) A = emeasure ?D A"
   5.157      using A I.measure_times[of "\<lambda>_. A"]
   5.158      by (simp add: emeasure_distr measurable_component_singleton)
   5.159 @@ -846,7 +847,7 @@
   5.160    have *: "\<And>x y. (\<Prod>j\<in>I. f j (if j = i then y else x j)) = (\<Prod>j\<in>I. f j (x j))"
   5.161      using insert by (auto intro!: setprod_cong)
   5.162    have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow> (\<lambda>x. (\<Prod>i\<in>J. f i (x i))) \<in> borel_measurable (Pi\<^isub>M J M)"
   5.163 -    using sets_into_space insert
   5.164 +    using sets.sets_into_space insert
   5.165      by (intro borel_measurable_ereal_setprod
   5.166                measurable_comp[OF measurable_component_singleton, unfolded comp_def])
   5.167         auto
   5.168 @@ -1036,7 +1037,7 @@
   5.169        sigma_sets (space ?P) {{f \<in> \<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> A} |i A. i \<in> I \<and> A \<in> sets (M i)}"
   5.170      using sets_PiM_single[of I M] by (simp add: space_P)
   5.171    also have "\<dots> \<subseteq> sets (sigma (space (PiM I M)) P)"
   5.172 -  proof (safe intro!: sigma_sets_subset)
   5.173 +  proof (safe intro!: sets.sigma_sets_subset)
   5.174      fix i A assume "i \<in> I" and A: "A \<in> sets (M i)"
   5.175      then have "(\<lambda>x. x i) \<in> measurable ?P (sigma (space (M i)) (E i))"
   5.176        apply (subst measurable_iff_measure_of)
   5.177 @@ -1059,7 +1060,7 @@
   5.178      by (simp add: P_closed)
   5.179    show "sigma_sets (space (PiM I M)) P \<subseteq> sets (PiM I M)"
   5.180      unfolding P_def space_PiM[symmetric]
   5.181 -    by (intro sigma_sets_subset) (auto simp: E_generates sets_Collect_single)
   5.182 +    by (intro sets.sigma_sets_subset) (auto simp: E_generates sets_Collect_single)
   5.183  qed
   5.184  
   5.185  lemma sigma_prod_algebra_sigma_eq:
   5.186 @@ -1084,7 +1085,7 @@
   5.187        sigma_sets (space ?P) {{f \<in> \<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> A} |i A. i \<in> I \<and> A \<in> sets (M i)}"
   5.188      using sets_PiM_single[of I M] by (simp add: space_P)
   5.189    also have "\<dots> \<subseteq> sets (sigma (space (PiM I M)) P)"
   5.190 -  proof (safe intro!: sigma_sets_subset)
   5.191 +  proof (safe intro!: sets.sigma_sets_subset)
   5.192      fix i A assume "i \<in> I" and A: "A \<in> sets (M i)"
   5.193      have "(\<lambda>x. x i) \<in> measurable ?P (sigma (space (M i)) (E i))"
   5.194      proof (subst measurable_iff_measure_of)
   5.195 @@ -1104,7 +1105,7 @@
   5.196            apply (auto simp: bij_betw_def)
   5.197            done
   5.198          also have "\<dots> \<in> sets ?P"
   5.199 -        proof (safe intro!: countable_UN)
   5.200 +        proof (safe intro!: sets.countable_UN)
   5.201            fix xs show "(\<Pi>\<^isub>E j\<in>I. if i = j then A else S j (xs ! T j)) \<in> sets ?P"
   5.202              using A S_in_E
   5.203              by (simp add: P_closed)
   5.204 @@ -1125,7 +1126,7 @@
   5.205      by (simp add: P_closed)
   5.206    show "sigma_sets (space (PiM I M)) P \<subseteq> sets (PiM I M)"
   5.207      using `finite I`
   5.208 -    by (auto intro!: sigma_sets_subset sets_PiM_I_finite simp: E_generates P_def)
   5.209 +    by (auto intro!: sets.sigma_sets_subset sets_PiM_I_finite simp: E_generates P_def)
   5.210  qed
   5.211  
   5.212  lemma pair_measure_eq_distr_PiM:
   5.213 @@ -1146,7 +1147,7 @@
   5.214    also have "\<dots> = emeasure ?B (Pi\<^isub>E UNIV (bool_case A B))"
   5.215      using A B by (subst B.emeasure_PiM) (auto split: bool.split)
   5.216    also have "Pi\<^isub>E UNIV (bool_case A B) = (\<lambda>x. (x True, x False)) -` (A \<times> B) \<inter> space ?B"
   5.217 -    using A[THEN sets_into_space] B[THEN sets_into_space]
   5.218 +    using A[THEN sets.sets_into_space] B[THEN sets.sets_into_space]
   5.219      by (auto simp: PiE_iff all_bool_eq space_PiM split: bool.split)
   5.220    finally show "emeasure M1 A * emeasure M2 B = emeasure ?D (A \<times> B)"
   5.221      using A B
     6.1 --- a/src/HOL/Probability/Independent_Family.thy	Thu Nov 22 10:09:54 2012 +0100
     6.2 +++ b/src/HOL/Probability/Independent_Family.thy	Tue Nov 27 11:29:47 2012 +0100
     6.3 @@ -186,11 +186,11 @@
     6.4              using G by auto
     6.5            have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) =
     6.6                prob ((\<Inter>j\<in>J. A j) - (\<Inter>i\<in>insert j J. (A(j := X)) i))"
     6.7 -            using A_sets sets_into_space[of _ M] X `J \<noteq> {}`
     6.8 +            using A_sets sets.sets_into_space[of _ M] X `J \<noteq> {}`
     6.9              by (auto intro!: arg_cong[where f=prob] split: split_if_asm)
    6.10            also have "\<dots> = prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)"
    6.11 -            using J `J \<noteq> {}` `j \<notin> J` A_sets X sets_into_space
    6.12 -            by (auto intro!: finite_measure_Diff finite_INT split: split_if_asm)
    6.13 +            using J `J \<noteq> {}` `j \<notin> J` A_sets X sets.sets_into_space
    6.14 +            by (auto intro!: finite_measure_Diff sets.finite_INT split: split_if_asm)
    6.15            finally have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) =
    6.16                prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)" .
    6.17            moreover {
    6.18 @@ -224,7 +224,7 @@
    6.19              show "disjoint_family (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i)"
    6.20                using disj by (rule disjoint_family_on_bisimulation) auto
    6.21              show "range (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i) \<subseteq> events"
    6.22 -              using A_sets F `finite J` `J \<noteq> {}` `j \<notin> J` by (auto intro!: Int)
    6.23 +              using A_sets F `finite J` `J \<noteq> {}` `j \<notin> J` by (auto intro!: sets.Int)
    6.24            qed
    6.25            moreover { fix k
    6.26              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))"
    6.27 @@ -243,7 +243,7 @@
    6.28            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))"
    6.29              by (auto dest!: sums_unique)
    6.30          qed (insert F, auto)
    6.31 -      qed (insert sets_into_space, auto)
    6.32 +      qed (insert sets.sets_into_space, auto)
    6.33        then have mono: "dynkin (space M) (G j) \<subseteq> {E \<in> events. indep_sets (G(j := {E})) K}"
    6.34        proof (rule dynkin_system.dynkin_subset, safe)
    6.35          fix X assume "X \<in> G j"
    6.36 @@ -291,7 +291,7 @@
    6.37    proof (rule indep_sets_mono_sets, subst sigma_eq_dynkin, simp_all add: stable)
    6.38      fix i assume "i \<in> I"
    6.39      with indep have "F i \<subseteq> events" by (auto simp: indep_sets_def)
    6.40 -    with sets_into_space show "F i \<subseteq> Pow (space M)" by auto
    6.41 +    with sets.sets_into_space show "F i \<subseteq> Pow (space M)" by auto
    6.42    qed
    6.43  qed
    6.44  
    6.45 @@ -394,7 +394,7 @@
    6.46      let ?S = "sigma_sets (space M) (\<Union>i\<in>I j. E i)"
    6.47      assume "j \<in> J"
    6.48      from E[OF this] interpret S: sigma_algebra "space M" ?S
    6.49 -      using sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto
    6.50 +      using sets.sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto
    6.51  
    6.52      have "sigma_sets (space M) (\<Union>i\<in>I j. E i) = sigma_sets (space M) (?E j)"
    6.53      proof (rule sigma_sets_eqI)
    6.54 @@ -416,7 +416,7 @@
    6.55    proof (rule indep_sets_sigma)
    6.56      show "indep_sets ?E J"
    6.57      proof (intro indep_setsI)
    6.58 -      fix j assume "j \<in> J" with E show "?E j \<subseteq> events" by (force  intro!: finite_INT)
    6.59 +      fix j assume "j \<in> J" with E show "?E j \<subseteq> events" by (force  intro!: sets.finite_INT)
    6.60      next
    6.61        fix K A assume K: "K \<noteq> {}" "K \<subseteq> J" "finite K"
    6.62          and "\<forall>j\<in>K. A j \<in> ?E j"
    6.63 @@ -533,7 +533,7 @@
    6.64    interpret D: dynkin_system "space M" ?D
    6.65    proof (rule dynkin_systemI)
    6.66      fix D assume "D \<in> ?D" then show "D \<subseteq> space M"
    6.67 -      using sets_into_space by auto
    6.68 +      using sets.sets_into_space by auto
    6.69    next
    6.70      show "space M \<in> ?D"
    6.71        using prob_space `X \<subseteq> space M` by (simp add: Int_absorb2)
    6.72 @@ -546,7 +546,7 @@
    6.73      also have "\<dots> = prob X * prob (space M) - prob X * prob A"
    6.74        using A prob_space by auto
    6.75      also have "\<dots> = prob X * prob (space M - A)"
    6.76 -      using X_in A sets_into_space
    6.77 +      using X_in A sets.sets_into_space
    6.78        by (subst finite_measure_Diff) (auto simp: field_simps)
    6.79      finally show "space M - A \<in> ?D"
    6.80        using A `X \<subseteq> space M` by auto
    6.81 @@ -611,14 +611,14 @@
    6.82    proof (rule sigma_eq_dynkin)
    6.83      { fix B n assume "B \<in> sigma_sets (space M) (\<Union>m\<in>{..n}. A m)"
    6.84        then have "B \<subseteq> space M"
    6.85 -        by induct (insert A sets_into_space[of _ M], auto) }
    6.86 +        by induct (insert A sets.sets_into_space[of _ M], auto) }
    6.87      then show "?A \<subseteq> Pow (space M)" by auto
    6.88      show "Int_stable ?A"
    6.89      proof (rule Int_stableI)
    6.90        fix a assume "a \<in> ?A" then guess n .. note a = this
    6.91        fix b assume "b \<in> ?A" then guess m .. note b = this
    6.92        interpret Amn: sigma_algebra "space M" "sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)"
    6.93 -        using A sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto
    6.94 +        using A sets.sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto
    6.95        have "sigma_sets (space M) (\<Union>i\<in>{..n}. A i) \<subseteq> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)"
    6.96          by (intro sigma_sets_subseteq UN_mono) auto
    6.97        with a have "a \<in> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" by auto
    6.98 @@ -644,7 +644,7 @@
    6.99    have F1: "range F \<subseteq> events"
   6.100      using F2 by (simp add: indep_events_def subset_eq)
   6.101    { fix i show "sigma_algebra (space M) (sigma_sets (space M) {F i})"
   6.102 -      using sigma_algebra_sigma_sets[of "{F i}" "space M"] F1 sets_into_space
   6.103 +      using sigma_algebra_sigma_sets[of "{F i}" "space M"] F1 sets.sets_into_space
   6.104        by auto }
   6.105    show "indep_sets (\<lambda>i. sigma_sets (space M) {F i}) UNIV"
   6.106    proof (rule indep_sets_sigma)
   6.107 @@ -659,12 +659,12 @@
   6.108    proof
   6.109      fix j
   6.110      interpret S: sigma_algebra "space M" "sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})"
   6.111 -      using order_trans[OF F1 space_closed]
   6.112 +      using order_trans[OF F1 sets.space_closed]
   6.113        by (intro sigma_algebra_sigma_sets) (simp add: sigma_sets_singleton subset_eq)
   6.114      have "(\<Inter>n. ?Q n) = (\<Inter>n\<in>{j..}. ?Q n)"
   6.115        by (intro decseq_SucI INT_decseq_offset UN_mono) auto
   6.116      also have "\<dots> \<in> sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})"
   6.117 -      using order_trans[OF F1 space_closed]
   6.118 +      using order_trans[OF F1 sets.space_closed]
   6.119        by (safe intro!: S.countable_INT S.countable_UN)
   6.120           (auto simp: sigma_sets_singleton intro!: sigma_sets.Basic bexI)
   6.121      finally show "(\<Inter>n. ?Q n) \<in> sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})"
   6.122 @@ -688,7 +688,7 @@
   6.123      assume A: "\<forall>j\<in>J. A j \<in> F j"
   6.124      let ?A = "\<lambda>j. if j \<in> J then A j else space M"
   6.125      have "prob (\<Inter>j\<in>I. ?A j) = prob (\<Inter>j\<in>J. A j)"
   6.126 -      using subset_trans[OF F(1) space_closed] J A
   6.127 +      using subset_trans[OF F(1) sets.space_closed] J A
   6.128        by (auto intro!: arg_cong[where f=prob] split: split_if_asm) blast
   6.129      also
   6.130      from A F have "(\<lambda>j. if j \<in> J then A j else space M) \<in> Pi I F" (is "?A \<in> _")
   6.131 @@ -882,7 +882,7 @@
   6.132      show "indep_vars M' X I" unfolding indep_vars_def
   6.133      proof (intro conjI indep_setsI ballI rv)
   6.134        fix i show "sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)} \<subseteq> events"
   6.135 -        by (auto intro!: sigma_sets_subset measurable_sets rv)
   6.136 +        by (auto intro!: sets.sigma_sets_subset measurable_sets rv)
   6.137      next
   6.138        fix J Y' assume J: "J \<noteq> {}" "J \<subseteq> I" "finite J"
   6.139        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)}"
   6.140 @@ -892,7 +892,7 @@
   6.141          from Y'[rule_format, OF this] rv[of j]
   6.142          show "\<exists>Y. Y' j = X j -` Y \<inter> space M \<and> Y \<in> sets (M' j)"
   6.143            by (subst (asm) sigma_sets_vimage_commute[symmetric, of _ _ "space (M' j)"])
   6.144 -             (auto dest: measurable_space simp: sigma_sets_eq)
   6.145 +             (auto dest: measurable_space simp: sets.sigma_sets_eq)
   6.146        qed
   6.147        from bchoice[OF this] obtain Y where
   6.148          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
     7.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Thu Nov 22 10:09:54 2012 +0100
     7.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Nov 27 11:29:47 2012 +0100
     7.3 @@ -311,7 +311,7 @@
     7.4    next
     7.5      fix J X assume J: "(J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))"
     7.6      then show "emb I J (Pi\<^isub>E J X) \<in> Pow (\<Pi>\<^isub>E i\<in>I. space (M i))"
     7.7 -      by (auto simp: Pi_iff prod_emb_def dest: sets_into_space)
     7.8 +      by (auto simp: Pi_iff prod_emb_def dest: sets.sets_into_space)
     7.9      have "emb I J (Pi\<^isub>E J X) \<in> generator"
    7.10        using J `I \<noteq> {}` by (intro generatorI') (auto simp: Pi_iff)
    7.11      then have "\<mu> (emb I J (Pi\<^isub>E J X)) = \<mu>G (emb I J (Pi\<^isub>E J X))"
    7.12 @@ -393,7 +393,7 @@
    7.13  
    7.14  lemma (in finite_product_prob_space) finite_measure_PiM_emb:
    7.15    "(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> measure (PiM I M) (Pi\<^isub>E I A) = (\<Prod>i\<in>I. measure (M i) (A i))"
    7.16 -  using measure_PiM_emb[of I A] finite_index prod_emb_PiE_same_index[OF sets_into_space, of I A M]
    7.17 +  using measure_PiM_emb[of I A] finite_index prod_emb_PiE_same_index[OF sets.sets_into_space, of I A M]
    7.18    by auto
    7.19  
    7.20  lemma (in product_prob_space) PiM_component:
    7.21 @@ -465,7 +465,7 @@
    7.22    then have *: "{\<omega> \<in> space ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)). prod_case (comb_seq i) \<omega> j \<in> A} =
    7.23      (if j < i then {\<omega> \<in> space (\<Pi>\<^isub>M i\<in>UNIV. M). \<omega> j \<in> A} \<times> space (\<Pi>\<^isub>M i\<in>UNIV. M)
    7.24                else space (\<Pi>\<^isub>M i\<in>UNIV. M) \<times> {\<omega> \<in> space (\<Pi>\<^isub>M i\<in>UNIV. M). \<omega> (j - i) \<in> A})"
    7.25 -    by (auto simp: space_PiM space_pair_measure comb_seq_def dest: sets_into_space)
    7.26 +    by (auto simp: space_PiM space_pair_measure comb_seq_def dest: sets.sets_into_space)
    7.27    show "{\<omega> \<in> space ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)). prod_case (comb_seq i) \<omega> j \<in> A} \<in> sets ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M))"
    7.28      unfolding * by (auto simp: A intro!: sets_Collect_single)
    7.29  qed
    7.30 @@ -507,7 +507,7 @@
    7.31    shows "Pi UNIV E \<in> sets S"
    7.32  proof -
    7.33    have "Pi UNIV E = (\<Inter>i. emb UNIV {..i} (\<Pi>\<^isub>E j\<in>{..i}. E j))"
    7.34 -    using E E[THEN sets_into_space]
    7.35 +    using E E[THEN sets.sets_into_space]
    7.36      by (auto simp: prod_emb_def Pi_iff extensional_def) blast
    7.37    with E show ?thesis by auto
    7.38  qed
    7.39 @@ -520,7 +520,7 @@
    7.40    have "\<And>n. (\<Prod>i\<le>n. measure M (E i)) = measure S (?E n)"
    7.41      using E by (simp add: measure_PiM_emb)
    7.42    moreover have "Pi UNIV E = (\<Inter>n. ?E n)"
    7.43 -    using E E[THEN sets_into_space]
    7.44 +    using E E[THEN sets.sets_into_space]
    7.45      by (auto simp: prod_emb_def extensional_def Pi_iff) blast
    7.46    moreover have "range ?E \<subseteq> sets S"
    7.47      using E by auto
    7.48 @@ -544,7 +544,7 @@
    7.49    fix J E assume J: "finite J" "J \<subseteq> ?I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets M"
    7.50    let ?X = "prod_emb ?I ?M J (\<Pi>\<^isub>E j\<in>J. E j)"
    7.51    have "\<And>j x. j \<in> J \<Longrightarrow> x \<in> E j \<Longrightarrow> x \<in> space M"
    7.52 -    using J(3)[THEN sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
    7.53 +    using J(3)[THEN sets.sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
    7.54    with J have "?f -` ?X \<inter> space (S \<Otimes>\<^isub>M S) =
    7.55      (prod_emb ?I ?M (J \<inter> {..<i}) (PIE j:J \<inter> {..<i}. E j)) \<times>
    7.56      (prod_emb ?I ?M ((op + i) -` J) (PIE j:(op + i) -` J. E (i + j)))" (is "_ = ?E \<times> ?F")
    7.57 @@ -576,7 +576,7 @@
    7.58    fix J E assume J: "finite J" "J \<subseteq> ?I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets M"
    7.59    let ?X = "prod_emb ?I ?M J (PIE j:J. E j)"
    7.60    have "\<And>j x. j \<in> J \<Longrightarrow> x \<in> E j \<Longrightarrow> x \<in> space M"
    7.61 -    using J(3)[THEN sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
    7.62 +    using J(3)[THEN sets.sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
    7.63    with J have "?f -` ?X \<inter> space (M \<Otimes>\<^isub>M S) = (if 0 \<in> J then E 0 else space M) \<times>
    7.64      (prod_emb ?I ?M (Suc -` J) (PIE j:Suc -` J. E (Suc j)))" (is "_ = ?E \<times> ?F")
    7.65     by (auto simp: space_pair_measure space_PiM PiE_iff prod_emb_def all_conj_distrib
     8.1 --- a/src/HOL/Probability/Information.thy	Thu Nov 22 10:09:54 2012 +0100
     8.2 +++ b/src/HOL/Probability/Information.thy	Tue Nov 27 11:29:47 2012 +0100
     8.3 @@ -183,7 +183,7 @@
     8.4      proof
     8.5        assume eq_0: "emeasure M {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} = 0"
     8.6        then have disj: "AE x in M. D x = 1 \<or> D x = 0"
     8.7 -        using D(1) by (auto intro!: AE_I[OF subset_refl] sets_Collect)
     8.8 +        using D(1) by (auto intro!: AE_I[OF subset_refl] sets.sets_Collect)
     8.9  
    8.10        have "emeasure M {x\<in>space M. D x = 1} = (\<integral>\<^isup>+ x. indicator {x\<in>space M. D x = 1} x \<partial>M)"
    8.11          using D(1) by auto
    8.12 @@ -198,7 +198,7 @@
    8.13        finally show False using `A \<in> sets M` `emeasure (density M D) A \<noteq> emeasure M A` by simp
    8.14      qed
    8.15      show "{x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<in> sets M"
    8.16 -      using D(1) by (auto intro: sets_Collect_conj)
    8.17 +      using D(1) by (auto intro: sets.sets_Collect_conj)
    8.18  
    8.19      show "AE t in M. t \<in> {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<longrightarrow>
    8.20        D t - indicator ?D_set t \<noteq> D t * (ln b * log b (D t))"
    8.21 @@ -383,7 +383,7 @@
    8.22    interpret sigma_finite_measure T by fact
    8.23    { fix A assume "A \<in> sets S" "emeasure S A = 0"
    8.24      moreover then have "fst -` A \<inter> space (S \<Otimes>\<^isub>M T) = A \<times> space T"
    8.25 -      by (auto simp: space_pair_measure dest!: sets_into_space)
    8.26 +      by (auto simp: space_pair_measure dest!: sets.sets_into_space)
    8.27      ultimately have "emeasure (S \<Otimes>\<^isub>M T) (fst -` A \<inter> space (S \<Otimes>\<^isub>M T)) = 0"
    8.28        by (simp add: emeasure_pair_measure_Times) }
    8.29    then show ?thesis
    8.30 @@ -400,7 +400,7 @@
    8.31    interpret sigma_finite_measure T by fact
    8.32    { fix A assume "A \<in> sets T" "emeasure T A = 0"
    8.33      moreover then have "snd -` A \<inter> space (S \<Otimes>\<^isub>M T) = space S \<times> A"
    8.34 -      by (auto simp: space_pair_measure dest!: sets_into_space)
    8.35 +      by (auto simp: space_pair_measure dest!: sets.sets_into_space)
    8.36      ultimately have "emeasure (S \<Otimes>\<^isub>M T) (snd -` A \<inter> space (S \<Otimes>\<^isub>M T)) = 0"
    8.37        by (simp add: emeasure_pair_measure_Times) }
    8.38    then show ?thesis
    8.39 @@ -1571,7 +1571,7 @@
    8.40      unfolding AE_density[OF distributed_borel_measurable, OF Pxy]
    8.41      unfolding distributed_distr_eq_density[OF Py]
    8.42      apply (rule ST.AE_pair_measure)
    8.43 -    apply (auto intro!: sets_Collect borel_measurable_eq measurable_compose[OF _ distributed_real_measurable[OF Py]]
    8.44 +    apply (auto intro!: sets.sets_Collect borel_measurable_eq measurable_compose[OF _ distributed_real_measurable[OF Py]]
    8.45                          distributed_real_measurable[OF Pxy] distributed_real_AE[OF Py]
    8.46                          borel_measurable_real_of_ereal measurable_compose[OF _ borel_measurable_RN_deriv_density])
    8.47      using distributed_RN_deriv[OF Py]
     9.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Thu Nov 22 10:09:54 2012 +0100
     9.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue Nov 27 11:29:47 2012 +0100
     9.3 @@ -117,7 +117,7 @@
     9.4      using assms unfolding simple_function_def
     9.5      using finite_subset[of "f ` (f -` S \<inter> space M)" "f ` space M"] by auto
     9.6    hence "?U \<in> sets M"
     9.7 -    apply (rule finite_UN)
     9.8 +    apply (rule sets.finite_UN)
     9.9      using assms unfolding simple_function_def by auto
    9.10    thus "f -` S \<inter> space M \<in> sets M" unfolding * .
    9.11  qed
    9.12 @@ -152,7 +152,7 @@
    9.13      (\<Union>x\<in>?G. f -` {x} \<inter> space M)" by auto
    9.14    show "(g \<circ> f) -` {(g \<circ> f) x} \<inter> space M \<in> sets M"
    9.15      using assms unfolding simple_function_def *
    9.16 -    by (rule_tac finite_UN) auto
    9.17 +    by (rule_tac sets.finite_UN) auto
    9.18  qed
    9.19  
    9.20  lemma simple_function_indicator[intro, simp]:
    9.21 @@ -447,7 +447,7 @@
    9.22      then have *: "?IF -` {?IF x} \<inter> space M = (if x \<in> A
    9.23        then ((F (f x) \<inter> (A \<inter> space M)) \<union> (G (f x) - (G (f x) \<inter> (A \<inter> space M))))
    9.24        else ((F (g x) \<inter> (A \<inter> space M)) \<union> (G (g x) - (G (g x) \<inter> (A \<inter> space M)))))"
    9.25 -      using sets_into_space[OF A] by (auto split: split_if_asm simp: G_def F_def)
    9.26 +      using sets.sets_into_space[OF A] by (auto split: split_if_asm simp: G_def F_def)
    9.27      have [intro]: "\<And>x. F x \<in> sets M" "\<And>x. G x \<in> sets M"
    9.28        unfolding F_def G_def using sf[THEN simple_functionD(2)] by auto
    9.29      show "?IF -` {?IF x} \<inter> space M \<in> sets M" unfolding * using A by auto
    9.30 @@ -637,7 +637,7 @@
    9.31          using mono by (auto elim!: AE_E)
    9.32        have "?S x \<subseteq> N" using N `x \<in> space M` False by auto
    9.33        moreover have "?S x \<in> sets M" using assms
    9.34 -        by (rule_tac Int) (auto intro!: simple_functionD)
    9.35 +        by (rule_tac sets.Int) (auto intro!: simple_functionD)
    9.36        ultimately have "(emeasure M) (?S x) \<le> (emeasure M) N"
    9.37          using `N \<in> sets M` by (auto intro!: emeasure_mono)
    9.38        moreover have "0 \<le> (emeasure M) (?S x)"
    9.39 @@ -683,13 +683,13 @@
    9.40    ultimately show ?thesis by (simp add: simple_integral_def)
    9.41  next
    9.42    assume "A \<noteq> space M"
    9.43 -  then obtain x where x: "x \<in> space M" "x \<notin> A" using sets_into_space[OF assms(1)] by auto
    9.44 +  then obtain x where x: "x \<in> space M" "x \<notin> A" using sets.sets_into_space[OF assms(1)] by auto
    9.45    have I: "(\<lambda>x. f x * indicator A x) ` space M = f ` A \<union> {0}" (is "?I ` _ = _")
    9.46    proof safe
    9.47      fix y assume "?I y \<notin> f ` A" hence "y \<notin> A" by auto thus "?I y = 0" by auto
    9.48    next
    9.49      fix y assume "y \<in> A" thus "f y \<in> ?I ` space M"
    9.50 -      using sets_into_space[OF assms(1)] by (auto intro!: image_eqI[of _ _ y])
    9.51 +      using sets.sets_into_space[OF assms(1)] by (auto intro!: image_eqI[of _ _ y])
    9.52    next
    9.53      show "0 \<in> ?I ` space M" using x by (auto intro!: image_eqI[of _ _ x])
    9.54    qed
    9.55 @@ -700,7 +700,7 @@
    9.56      show "finite (f ` space M \<union> {0})"
    9.57        using assms(2) unfolding simple_function_def by auto
    9.58      show "f ` A \<union> {0} \<subseteq> f`space M \<union> {0}"
    9.59 -      using sets_into_space[OF assms(1)] by auto
    9.60 +      using sets.sets_into_space[OF assms(1)] by auto
    9.61      have "\<And>x. f x \<notin> f ` A \<Longrightarrow> f -` {f x} \<inter> space M \<inter> A = {}"
    9.62        by (auto simp: image_iff)
    9.63      thus "\<forall>i\<in>f ` space M \<union> {0} - (f ` A \<union> {0}).
    9.64 @@ -721,13 +721,13 @@
    9.65    assumes "A \<in> sets M"
    9.66    shows "integral\<^isup>S M (indicator A) = emeasure M A"
    9.67  proof cases
    9.68 -  assume "space M = {}" hence "A = {}" using sets_into_space[OF assms] by auto
    9.69 +  assume "space M = {}" hence "A = {}" using sets.sets_into_space[OF assms] by auto
    9.70    thus ?thesis unfolding simple_integral_def using `space M = {}` by auto
    9.71  next
    9.72    assume "space M \<noteq> {}" hence "(\<lambda>x. 1) ` space M = {1::ereal}" by auto
    9.73    thus ?thesis
    9.74      using simple_integral_indicator[OF assms simple_function_const[of _ 1]]
    9.75 -    using sets_into_space[OF assms]
    9.76 +    using sets.sets_into_space[OF assms]
    9.77      by (auto intro!: arg_cong[where f="(emeasure M)"])
    9.78  qed
    9.79  
    9.80 @@ -916,7 +916,7 @@
    9.81      qed }
    9.82    note B_mono = this
    9.83  
    9.84 -  note B_u = Int[OF u(1)[THEN simple_functionD(2)] B]
    9.85 +  note B_u = sets.Int[OF u(1)[THEN simple_functionD(2)] B]
    9.86  
    9.87    let ?B' = "\<lambda>i n. (u -` {i} \<inter> space M) \<inter> ?B n"
    9.88    have measure_conv: "\<And>i. (emeasure M) (u -` {i} \<inter> space M) = (SUP n. (emeasure M) (?B' i n))"
    9.89 @@ -1351,7 +1351,7 @@
    9.90      also have "\<dots> = (emeasure M) (\<Union>n. ?M n \<inter> ?A)"
    9.91      proof (safe intro!: SUP_emeasure_incseq)
    9.92        fix n show "?M n \<inter> ?A \<in> sets M"
    9.93 -        using u by (auto intro!: Int)
    9.94 +        using u by (auto intro!: sets.Int)
    9.95      next
    9.96        show "incseq (\<lambda>n. {x \<in> space M. 1 \<le> real n * u x} \<inter> {x \<in> space M. u x \<noteq> 0})"
    9.97        proof (safe intro!: incseq_SucI)
    9.98 @@ -1401,8 +1401,8 @@
    9.99  
   9.100  lemma AE_iff_positive_integral: 
   9.101    "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> integral\<^isup>P M (indicator {x. \<not> P x}) = 0"
   9.102 -  by (subst positive_integral_0_iff_AE)
   9.103 -     (auto simp: one_ereal_def zero_ereal_def sets_Collect_neg indicator_def[abs_def] measurable_If)
   9.104 +  by (subst positive_integral_0_iff_AE) (auto simp: one_ereal_def zero_ereal_def
   9.105 +    sets.sets_Collect_neg indicator_def[abs_def] measurable_If)
   9.106  
   9.107  lemma positive_integral_const_If:
   9.108    "(\<integral>\<^isup>+x. a \<partial>M) = (if 0 \<le> a then a * (emeasure M) (space M) else 0)"
   9.109 @@ -2463,7 +2463,7 @@
   9.110  
   9.111  lemma density_cong: "f \<in> borel_measurable M \<Longrightarrow> f' \<in> borel_measurable M \<Longrightarrow>
   9.112    (AE x in M. f x = f' x) \<Longrightarrow> density M f = density M f'"
   9.113 -  unfolding density_def by (auto intro!: measure_of_eq positive_integral_cong_AE space_closed)
   9.114 +  unfolding density_def by (auto intro!: measure_of_eq positive_integral_cong_AE sets.space_closed)
   9.115  
   9.116  lemma density_max_0: "density M f = density M (\<lambda>x. max 0 (f x))"
   9.117  proof -
   9.118 @@ -2549,7 +2549,7 @@
   9.119      by (auto simp: eventually_ae_filter)
   9.120    then have *: "{x \<in> space (density M f). \<not> P x} \<subseteq> N \<union> {x\<in>space M. \<not> 0 < f x}"
   9.121      "N \<union> {x\<in>space M. \<not> 0 < f x} \<in> sets M" and ae2: "AE x in M. x \<notin> N"
   9.122 -    using f by (auto simp: subset_eq intro!: sets_Collect_neg AE_not_in)
   9.123 +    using f by (auto simp: subset_eq intro!: sets.sets_Collect_neg AE_not_in)
   9.124    show "AE x in density M f. P x"
   9.125      using ae2
   9.126      unfolding eventually_ae_filter[of _ "density M f"] Bex_def null_sets_density_iff[OF f]
   9.127 @@ -2618,7 +2618,7 @@
   9.128    also have "\<dots> = (\<integral>\<^isup>+x. indicator (S \<inter> X) x \<partial>M)"
   9.129      by (auto intro!: positive_integral_cong simp: indicator_def)
   9.130    also have "\<dots> = emeasure M (S \<inter> X)"
   9.131 -    using S X by (simp add: Int)
   9.132 +    using S X by (simp add: sets.Int)
   9.133    finally show ?thesis .
   9.134  qed
   9.135  
   9.136 @@ -2651,7 +2651,7 @@
   9.137  proof (rule measure_eqI)
   9.138    fix A assume A: "A \<in> sets ?R"
   9.139    { fix x assume "x \<in> space M"
   9.140 -    with sets_into_space[OF A]
   9.141 +    with sets.sets_into_space[OF A]
   9.142      have "indicator (T' -` A \<inter> space M') (T x) = (indicator A x :: ereal)"
   9.143        using T inv by (auto simp: indicator_def measurable_space) }
   9.144    with A T T' f show "emeasure ?R A = emeasure ?L A"
   9.145 @@ -2777,7 +2777,7 @@
   9.146               intro!: positive_integral_cong)
   9.147    also have "\<dots> = emeasure M (A \<inter> B) / emeasure M A"
   9.148      using A B
   9.149 -    by (subst positive_integral_cmult_indicator) (simp_all add: Int emeasure_nonneg)
   9.150 +    by (subst positive_integral_cmult_indicator) (simp_all add: sets.Int emeasure_nonneg)
   9.151    finally show ?thesis .
   9.152  qed
   9.153  
    10.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Thu Nov 22 10:09:54 2012 +0100
    10.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Tue Nov 27 11:29:47 2012 +0100
    10.3 @@ -217,7 +217,7 @@
    10.4    have "s \<in> sigma_sets (space lebesgue) (range (\<lambda>(a, b). {a .. (b :: 'a\<Colon>ordered_euclidean_space)}))"
    10.5      using assms by (simp add: borel_eq_atLeastAtMost)
    10.6    also have "\<dots> \<subseteq> sets lebesgue"
    10.7 -  proof (safe intro!: sigma_sets_subset lebesgueI)
    10.8 +  proof (safe intro!: sets.sigma_sets_subset lebesgueI)
    10.9      fix n :: nat and a b :: 'a
   10.10      let ?N = "\<chi>\<chi> i. max (- real n) (a $$ i)"
   10.11      let ?P = "\<chi>\<chi> i. min (real n) (b $$ i)"
   10.12 @@ -491,7 +491,7 @@
   10.13    and sets_lborel[simp]: "sets lborel = sets borel"
   10.14    and measurable_lborel1[simp]: "measurable lborel = measurable borel"
   10.15    and measurable_lborel2[simp]: "measurable A lborel = measurable A borel"
   10.16 -  using sigma_sets_eq[of borel]
   10.17 +  using sets.sigma_sets_eq[of borel]
   10.18    by (auto simp add: lborel_def measurable_def[abs_def])
   10.19  
   10.20  lemma emeasure_lborel[simp]: "A \<in> sets borel \<Longrightarrow> emeasure lborel A = emeasure lebesgue A"
    11.1 --- a/src/HOL/Probability/Measure_Space.thy	Thu Nov 22 10:09:54 2012 +0100
    11.2 +++ b/src/HOL/Probability/Measure_Space.thy	Tue Nov 27 11:29:47 2012 +0100
    11.3 @@ -449,11 +449,11 @@
    11.4  
    11.5  lemma suminf_emeasure:
    11.6    "range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Sum>i. emeasure M (A i)) = emeasure M (\<Union>i. A i)"
    11.7 -  using countable_UN[of A UNIV M] emeasure_countably_additive[of M]
    11.8 +  using sets.countable_UN[of A UNIV M] emeasure_countably_additive[of M]
    11.9    by (simp add: countably_additive_def)
   11.10  
   11.11  lemma emeasure_additive: "additive (sets M) (emeasure M)"
   11.12 -  by (metis countably_additive_additive emeasure_positive emeasure_countably_additive)
   11.13 +  by (metis sets.countably_additive_additive emeasure_positive emeasure_countably_additive)
   11.14  
   11.15  lemma plus_emeasure:
   11.16    "a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b = {} \<Longrightarrow> emeasure M a + emeasure M b = emeasure M (a \<union> b)"
   11.17 @@ -462,16 +462,16 @@
   11.18  lemma setsum_emeasure:
   11.19    "F`I \<subseteq> sets M \<Longrightarrow> disjoint_family_on F I \<Longrightarrow> finite I \<Longrightarrow>
   11.20      (\<Sum>i\<in>I. emeasure M (F i)) = emeasure M (\<Union>i\<in>I. F i)"
   11.21 -  by (metis additive_sum emeasure_positive emeasure_additive)
   11.22 +  by (metis sets.additive_sum emeasure_positive emeasure_additive)
   11.23  
   11.24  lemma emeasure_mono:
   11.25    "a \<subseteq> b \<Longrightarrow> b \<in> sets M \<Longrightarrow> emeasure M a \<le> emeasure M b"
   11.26 -  by (metis additive_increasing emeasure_additive emeasure_nonneg emeasure_notin_sets
   11.27 +  by (metis sets.additive_increasing emeasure_additive emeasure_nonneg emeasure_notin_sets
   11.28              emeasure_positive increasingD)
   11.29  
   11.30  lemma emeasure_space:
   11.31    "emeasure M A \<le> emeasure M (space M)"
   11.32 -  by (metis emeasure_mono emeasure_nonneg emeasure_notin_sets sets_into_space top)
   11.33 +  by (metis emeasure_mono emeasure_nonneg emeasure_notin_sets sets.sets_into_space sets.top)
   11.34  
   11.35  lemma emeasure_compl:
   11.36    assumes s: "s \<in> sets M" and fin: "emeasure M s \<noteq> \<infinity>"
   11.37 @@ -479,7 +479,7 @@
   11.38  proof -
   11.39    from s have "0 \<le> emeasure M s" by auto
   11.40    have "emeasure M (space M) = emeasure M (s \<union> (space M - s))" using s
   11.41 -    by (metis Un_Diff_cancel Un_absorb1 s sets_into_space)
   11.42 +    by (metis Un_Diff_cancel Un_absorb1 s sets.sets_into_space)
   11.43    also have "... = emeasure M s + emeasure M (space M - s)"
   11.44      by (rule plus_emeasure[symmetric]) (auto simp add: s)
   11.45    finally have "emeasure M (space M) = emeasure M s + emeasure M (space M - s)" .
   11.46 @@ -506,7 +506,8 @@
   11.47  lemma Lim_emeasure_incseq:
   11.48    "range A \<subseteq> sets M \<Longrightarrow> incseq A \<Longrightarrow> (\<lambda>i. (emeasure M (A i))) ----> emeasure M (\<Union>i. A i)"
   11.49    using emeasure_countably_additive
   11.50 -  by (auto simp add: countably_additive_iff_continuous_from_below emeasure_positive emeasure_additive)
   11.51 +  by (auto simp add: sets.countably_additive_iff_continuous_from_below emeasure_positive
   11.52 +    emeasure_additive)
   11.53  
   11.54  lemma incseq_emeasure:
   11.55    assumes "range B \<subseteq> sets M" "incseq B"
   11.56 @@ -595,10 +596,10 @@
   11.57    have "emeasure M (\<Union>i. f i) = emeasure M (\<Union>i. disjointed f i)"
   11.58      unfolding UN_disjointed_eq ..
   11.59    also have "\<dots> = (\<Sum>i. emeasure M (disjointed f i))"
   11.60 -    using range_disjointed_sets[OF assms] suminf_emeasure[of "disjointed f"]
   11.61 +    using sets.range_disjointed_sets[OF assms] suminf_emeasure[of "disjointed f"]
   11.62      by (simp add:  disjoint_family_disjointed comp_def)
   11.63    also have "\<dots> \<le> (\<Sum>i. emeasure M (f i))"
   11.64 -    using range_disjointed_sets[OF assms] assms
   11.65 +    using sets.range_disjointed_sets[OF assms] assms
   11.66      by (auto intro!: suminf_le_pos emeasure_mono disjointed_subset)
   11.67    finally show ?thesis .
   11.68  qed
   11.69 @@ -676,7 +677,8 @@
   11.70    let ?\<mu>  = "emeasure M" and ?\<nu> = "emeasure N"
   11.71    interpret S: sigma_algebra \<Omega> "sigma_sets \<Omega> E" by (rule sigma_algebra_sigma_sets) fact
   11.72    have "space M = \<Omega>"
   11.73 -    using top[of M] space_closed[of M] S.top S.space_closed `sets M = sigma_sets \<Omega> E` by blast
   11.74 +    using sets.top[of M] sets.space_closed[of M] S.top S.space_closed `sets M = sigma_sets \<Omega> E`
   11.75 +    by blast
   11.76  
   11.77    { fix F D assume "F \<in> E" and "?\<mu> F \<noteq> \<infinity>"
   11.78      then have [intro]: "F \<in> sigma_sets \<Omega> E" by auto
   11.79 @@ -724,9 +726,9 @@
   11.80      fix F assume "F \<in> sets M"
   11.81      let ?D = "disjointed (\<lambda>i. F \<inter> A i)"
   11.82      from `space M = \<Omega>` have F_eq: "F = (\<Union>i. ?D i)"
   11.83 -      using `F \<in> sets M`[THEN sets_into_space] A(2)[symmetric] by (auto simp: UN_disjointed_eq)
   11.84 +      using `F \<in> sets M`[THEN sets.sets_into_space] A(2)[symmetric] by (auto simp: UN_disjointed_eq)
   11.85      have [simp, intro]: "\<And>i. ?D i \<in> sets M"
   11.86 -      using range_disjointed_sets[of "\<lambda>i. F \<inter> A i" M] `F \<in> sets M`
   11.87 +      using sets.range_disjointed_sets[of "\<lambda>i. F \<inter> A i" M] `F \<in> sets M`
   11.88        by (auto simp: subset_eq)
   11.89      have "disjoint_family ?D"
   11.90        by (auto simp: disjoint_family_disjointed)
   11.91 @@ -770,7 +772,7 @@
   11.92  interpretation null_sets: ring_of_sets "space M" "null_sets M" for M
   11.93  proof (rule ring_of_setsI)
   11.94    show "null_sets M \<subseteq> Pow (space M)"
   11.95 -    using sets_into_space by auto
   11.96 +    using sets.sets_into_space by auto
   11.97    show "{} \<in> null_sets M"
   11.98      by auto
   11.99    fix A B assume sets: "A \<in> null_sets M" "B \<in> null_sets M"
  11.100 @@ -904,7 +906,7 @@
  11.101  
  11.102  lemma AE_iff_null_sets:
  11.103    "N \<in> sets M \<Longrightarrow> N \<in> null_sets M \<longleftrightarrow> (AE x in M. x \<notin> N)"
  11.104 -  using Int_absorb1[OF sets_into_space, of N M]
  11.105 +  using Int_absorb1[OF sets.sets_into_space, of N M]
  11.106    by (subst AE_iff_null) (auto simp: Int_def[symmetric])
  11.107  
  11.108  lemma AE_not_in:
  11.109 @@ -1033,7 +1035,7 @@
  11.110    have "emeasure M A = emeasure M (A - N)"
  11.111      using N A by (subst emeasure_Diff_null_set) auto
  11.112    also have "emeasure M (A - N) \<le> emeasure M (B - N)"
  11.113 -    using N A B sets_into_space by (auto intro!: emeasure_mono)
  11.114 +    using N A B sets.sets_into_space by (auto intro!: emeasure_mono)
  11.115    also have "emeasure M (B - N) = emeasure M B"
  11.116      using N B by (subst emeasure_Diff_null_set) auto
  11.117    finally show ?thesis .
  11.118 @@ -1062,7 +1064,7 @@
  11.119      space: "(\<Union>i. A i) = space M" and
  11.120      measure: "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
  11.121      using sigma_finite by auto
  11.122 -  note range' = range_disjointed_sets[OF range] range
  11.123 +  note range' = sets.range_disjointed_sets[OF range] range
  11.124    { fix i
  11.125      have "emeasure M (disjointed A i) \<le> emeasure M (A i)"
  11.126        using range' disjointed_subset[of A i] by (auto intro!: emeasure_mono)
  11.127 @@ -1400,7 +1402,7 @@
  11.128  lemma (in finite_measure) finite_measure_compl:
  11.129    assumes S: "S \<in> sets M"
  11.130    shows "measure M (space M - S) = measure M (space M) - measure M S"
  11.131 -  using measure_Diff[OF _ top S sets_into_space] S by simp
  11.132 +  using measure_Diff[OF _ sets.top S sets.sets_into_space] S by simp
  11.133  
  11.134  lemma (in finite_measure) finite_measure_mono_AE:
  11.135    assumes imp: "AE x in M. x \<in> A \<longrightarrow> x \<in> B" and B: "B \<in> sets M"
  11.136 @@ -1497,7 +1499,7 @@
  11.137    shows "measure M e = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
  11.138  proof -
  11.139    have e: "e = (\<Union> i \<in> s. e \<inter> f i)"
  11.140 -    using `e \<in> sets M` sets_into_space upper by blast
  11.141 +    using `e \<in> sets M` sets.sets_into_space upper by blast
  11.142    hence "measure M e = measure M (\<Union> i \<in> s. e \<inter> f i)" by simp
  11.143    also have "\<dots> = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
  11.144    proof (rule finite_measure_finite_Union)
    12.1 --- a/src/HOL/Probability/Probability_Measure.thy	Thu Nov 22 10:09:54 2012 +0100
    12.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Tue Nov 27 11:29:47 2012 +0100
    12.3 @@ -66,7 +66,7 @@
    12.4  proof
    12.5    assume ae: "AE x in M. x \<in> A"
    12.6    have "{x \<in> space M. x \<in> A} = A" "{x \<in> space M. x \<notin> A} = space M - A"
    12.7 -    using `A \<in> events`[THEN sets_into_space] by auto
    12.8 +    using `A \<in> events`[THEN sets.sets_into_space] by auto
    12.9    with AE_E2[OF ae] `A \<in> events` have "1 - emeasure M A = 0"
   12.10      by (simp add: emeasure_compl emeasure_space_1)
   12.11    then show "prob A = 1"
   12.12 @@ -273,7 +273,7 @@
   12.13    assumes Q: "AE x in M. Q x \<longleftrightarrow> Q' x" "{x\<in>space M. Q x} \<in> events" "{x\<in>space M. Q' x} \<in> events"
   12.14    shows "cond_prob M P Q = cond_prob M P' Q'"
   12.15    using P Q
   12.16 -  by (auto simp: cond_prob_def intro!: arg_cong2[where f="op /"] prob_eq_AE sets_Collect_conj)
   12.17 +  by (auto simp: cond_prob_def intro!: arg_cong2[where f="op /"] prob_eq_AE sets.sets_Collect_conj)
   12.18  
   12.19  
   12.20  lemma (in prob_space) joint_distribution_Times_le_fst:
   12.21 @@ -476,7 +476,7 @@
   12.22    show "distr M ?P (\<lambda>x. (X x, Y x)) = density ?P f" (is "?L = ?R")
   12.23    proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of S T]])
   12.24      show "?E \<subseteq> Pow (space ?P)"
   12.25 -      using space_closed[of S] space_closed[of T] by (auto simp: space_pair_measure)
   12.26 +      using sets.space_closed[of S] sets.space_closed[of T] by (auto simp: space_pair_measure)
   12.27      show "sets ?L = sigma_sets (space ?P) ?E"
   12.28        by (simp add: sets_pair_measure space_pair_measure)
   12.29      then show "sets ?R = sigma_sets (space ?P) ?E"
   12.30 @@ -529,7 +529,7 @@
   12.31        using Pxy by auto
   12.32      { fix A assume A: "A \<in> sets (T \<Otimes>\<^isub>M S)"
   12.33        let ?B = "(\<lambda>(x, y). (y, x)) -` A \<inter> space (S \<Otimes>\<^isub>M T)"
   12.34 -      from sets_into_space[OF A]
   12.35 +      from sets.sets_into_space[OF A]
   12.36        have "emeasure M ((\<lambda>x. (Y x, X x)) -` A \<inter> space M) =
   12.37          emeasure M ((\<lambda>x. (X x, Y x)) -` ?B \<inter> space M)"
   12.38          by (auto intro!: arg_cong2[where f=emeasure] simp: space_pair_measure)
   12.39 @@ -849,7 +849,7 @@
   12.40  proof
   12.41    show "emeasure (uniform_measure M A) (space (uniform_measure M A)) = 1"
   12.42      using emeasure_uniform_measure[OF emeasure_neq_0_sets[OF A(1)], of "space M"]
   12.43 -    using sets_into_space[OF emeasure_neq_0_sets[OF A(1)]] A
   12.44 +    using sets.sets_into_space[OF emeasure_neq_0_sets[OF A(1)]] A
   12.45      by (simp add: Int_absorb2 emeasure_nonneg)
   12.46  qed
   12.47  
    13.1 --- a/src/HOL/Probability/Projective_Family.thy	Thu Nov 22 10:09:54 2012 +0100
    13.2 +++ b/src/HOL/Probability/Projective_Family.thy	Tue Nov 27 11:29:47 2012 +0100
    13.3 @@ -25,7 +25,7 @@
    13.4    show "range ?F \<subseteq> ?J" "(\<Union>i. ?F i) = ?\<Omega>"
    13.5      using `finite J` by (auto intro!: prod_algebraI_finite)
    13.6    { fix i show "emeasure ?P (?F i) \<noteq> \<infinity>" by simp }
    13.7 -  show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
    13.8 +  show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets.sets_into_space)
    13.9    show "sets (\<Pi>\<^isub>M i\<in>J. M i) = sigma_sets ?\<Omega> ?J" "sets ?D = sigma_sets ?\<Omega> ?J"
   13.10      using `finite J` by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff)
   13.11  
   13.12 @@ -44,7 +44,7 @@
   13.13    also have "\<dots> = emeasure (Pi\<^isub>M K M) (\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i))"
   13.14      using E by (simp add: K.measure_times)
   13.15    also have "(\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i)) = (\<lambda>f. restrict f J) -` Pi\<^isub>E J E \<inter> (\<Pi>\<^isub>E i\<in>K. space (M i))"
   13.16 -    using `J \<subseteq> K` sets_into_space E by (force simp: Pi_iff PiE_def split: split_if_asm)
   13.17 +    using `J \<subseteq> K` sets.sets_into_space E by (force simp: Pi_iff PiE_def split: split_if_asm)
   13.18    finally show "emeasure (Pi\<^isub>M J M) X = emeasure ?D X"
   13.19      using X `J \<subseteq> K` apply (subst emeasure_distr)
   13.20      by (auto intro!: measurable_restrict_subset simp: space_PiM)
   13.21 @@ -93,10 +93,10 @@
   13.22    shows "emeasure (limP J M P) (Pi\<^isub>E J A) = emeasure (P J) (Pi\<^isub>E J A)"
   13.23  proof -
   13.24    have "Pi\<^isub>E J (restrict A J) \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
   13.25 -    using sets_into_space[OF A] by (auto simp: PiE_iff) blast
   13.26 +    using sets.sets_into_space[OF A] by (auto simp: PiE_iff) blast
   13.27    hence "emeasure (limP J M P) (Pi\<^isub>E J A) =
   13.28      emeasure (limP J M P) (prod_emb J M J (Pi\<^isub>E J A))"
   13.29 -    using assms(1-3) sets_into_space by (auto simp add: prod_emb_id PiE_def Pi_def)
   13.30 +    using assms(1-3) sets.sets_into_space by (auto simp add: prod_emb_id PiE_def Pi_def)
   13.31    also have "\<dots> = emeasure (P J) (Pi\<^isub>E J A)"
   13.32    proof (rule emeasure_extend_measure_Pair[OF limP_def])
   13.33      show "positive (sets (limP J M P)) (P J)" unfolding positive_def by auto
   13.34 @@ -133,12 +133,12 @@
   13.35    then obtain E where X: "X = Pi\<^isub>E J E" and E: "\<forall>i\<in>J. E i \<in> sets (M i)" by auto
   13.36    with `finite J` have "X \<in> sets (limP J M P)" by simp
   13.37    have emb_self: "prod_emb J M J (Pi\<^isub>E J E) = Pi\<^isub>E J E"
   13.38 -    using E sets_into_space
   13.39 +    using E sets.sets_into_space
   13.40      by (auto intro!: prod_emb_PiE_same_index)
   13.41    show "emeasure (limP J M P) X = emeasure (P J) X"
   13.42      unfolding X using E
   13.43      by (intro emeasure_limP assms) simp
   13.44 -qed (auto simp: Pi_iff dest: sets_into_space intro: Int_stable_PiE)
   13.45 +qed (auto simp: Pi_iff dest: sets.sets_into_space intro: Int_stable_PiE)
   13.46  
   13.47  lemma emeasure_fun_emb[simp]:
   13.48    assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" "L \<subseteq> I" and X: "X \<in> sets (PiM J M)"
   13.49 @@ -155,7 +155,7 @@
   13.50    shows "X = Y"
   13.51  proof (rule injective_vimage_restrict)
   13.52    show "X \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
   13.53 -    using sets[THEN sets_into_space] by (auto simp: space_PiM)
   13.54 +    using sets[THEN sets.sets_into_space] by (auto simp: space_PiM)
   13.55    have "\<forall>i\<in>L. \<exists>x. x \<in> space (M i)"
   13.56    proof
   13.57      fix i assume "i \<in> L"
   13.58 @@ -219,7 +219,7 @@
   13.59        fix A assume "A \<in> prod_algebra I M" with `I \<noteq> {}` show "A \<in> generator"
   13.60          by (auto intro!: generatorI' sets_PiM_I_finite elim!: prod_algebraE)
   13.61      qed
   13.62 -  qed (auto simp: generator_def space_PiM[symmetric] intro!: sigma_sets_subset)
   13.63 +  qed (auto simp: generator_def space_PiM[symmetric] intro!: sets.sigma_sets_subset)
   13.64  qed
   13.65  
   13.66  lemma generatorI:
   13.67 @@ -317,14 +317,14 @@
   13.68      have JK_disj: "emb (J \<union> K) J X \<inter> emb (J \<union> K) K Y = {}"
   13.69        apply (rule prod_emb_injective[of "J \<union> K" I])
   13.70        apply (insert `A \<inter> B = {}` JK J K)
   13.71 -      apply (simp_all add: Int prod_emb_Int)
   13.72 +      apply (simp_all add: sets.Int prod_emb_Int)
   13.73        done
   13.74      have AB: "A = emb I (J \<union> K) (emb (J \<union> K) J X)" "B = emb I (J \<union> K) (emb (J \<union> K) K Y)"
   13.75        using J K by simp_all
   13.76      then have "\<mu>G (A \<union> B) = \<mu>G (emb I (J \<union> K) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y))"
   13.77        by simp
   13.78      also have "\<dots> = emeasure (limP (J \<union> K) M P) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)"
   13.79 -      using JK J(1, 4) K(1, 4) by (simp add: \<mu>G_eq Un del: prod_emb_Un)
   13.80 +      using JK J(1, 4) K(1, 4) by (simp add: \<mu>G_eq sets.Un del: prod_emb_Un)
   13.81      also have "\<dots> = \<mu>G A + \<mu>G B"
   13.82        using J K JK_disj by (simp add: plus_emeasure[symmetric])
   13.83      finally show "\<mu>G (A \<union> B) = \<mu>G A + \<mu>G B" .
    14.1 --- a/src/HOL/Probability/Projective_Limit.thy	Thu Nov 22 10:09:54 2012 +0100
    14.2 +++ b/src/HOL/Probability/Projective_Limit.thy	Tue Nov 27 11:29:47 2012 +0100
    14.3 @@ -243,11 +243,8 @@
    14.4          assume "x \<in> K n" hence fm_in: "fm n x \<in> fm n ` B n"
    14.5            using K' by (force simp: K_def)
    14.6          show "x \<in> B n"
    14.7 -          apply (rule inj_on_image_mem_iff[OF inj_on_fm _ fm_in])
    14.8 -          using `x \<in> K n` K_sets J[of n] sets_into_space
    14.9 -          apply (auto simp: proj_space)
   14.10 -          using J[of n] sets_into_space apply auto
   14.11 -          done
   14.12 +          using `x \<in> K n` K_sets sets.sets_into_space J[of n]
   14.13 +          by (intro inj_on_image_mem_iff[OF inj_on_fm _ fm_in, of "\<lambda>_. borel"]) auto
   14.14        qed
   14.15        def Z' \<equiv> "\<lambda>n. emb I (J n) (K n)"
   14.16        have Z': "\<And>n. Z' n \<subseteq> Z n"
   14.17 @@ -263,7 +260,7 @@
   14.18          proof safe
   14.19            fix y assume "y \<in> B n"
   14.20            moreover
   14.21 -          hence "y \<in> space (Pi\<^isub>M (J n) (\<lambda>_. borel))" using J sets_into_space[of "B n" "P (J n)"]
   14.22 +          hence "y \<in> space (Pi\<^isub>M (J n) (\<lambda>_. borel))" using J sets.sets_into_space[of "B n" "P (J n)"]
   14.23              by (auto simp add: proj_space proj_sets)
   14.24            assume "fm n x = fm n y"
   14.25            note inj_onD[OF inj_on_fm[OF space_borel],
   14.26 @@ -314,7 +311,7 @@
   14.27          moreover have "\<mu>G (Z n - Y n) = limP (J n) (\<lambda>_. borel) P
   14.28            (B n - (\<Inter>i\<in>{Suc 0..n}. prod_emb (J n) (\<lambda>_. borel) (J i) (K i)))"
   14.29            unfolding Z_eq Y_emb prod_emb_Diff[symmetric] using J J_mono K_sets `n \<ge> 1`
   14.30 -          by (subst \<mu>G_eq) (auto intro!: Diff)
   14.31 +          by (subst \<mu>G_eq) (auto intro!: sets.Diff)
   14.32          ultimately
   14.33          have "\<mu>G (Z n) - \<mu>G (Y n) = \<mu>G (Z n - Y n)"
   14.34            using J J_mono K_sets `n \<ge> 1`
   14.35 @@ -406,7 +403,7 @@
   14.36          thus "K' (Suc n) \<noteq> {}" by auto
   14.37          fix k
   14.38          assume "k \<in> K' (Suc n)"
   14.39 -        with K'[of "Suc n"] sets_into_space have "k \<in> fm (Suc n) ` B (Suc n)" by auto
   14.40 +        with K'[of "Suc n"] sets.sets_into_space have "k \<in> fm (Suc n) ` B (Suc n)" by auto
   14.41          then obtain b where "k = fm (Suc n) b" by auto
   14.42          thus "domain k = domain (fm (Suc n) (y (Suc n)))"
   14.43            by (simp_all add: fm_def)
    15.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Thu Nov 22 10:09:54 2012 +0100
    15.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Tue Nov 27 11:29:47 2012 +0100
    15.3 @@ -189,13 +189,13 @@
    15.4        fix B assume "B \<in> sets M" "B \<subseteq> space M - A n"
    15.5        from B[OF this] show "-e < ?d B" .
    15.6      next
    15.7 -      show "space M - A n \<in> sets M" by (rule compl_sets) fact
    15.8 +      show "space M - A n \<in> sets M" by (rule sets.compl_sets) fact
    15.9      next
   15.10        show "?d (space M) \<le> ?d (space M - A n)"
   15.11        proof (induct n)
   15.12          fix n assume "?d (space M) \<le> ?d (space M - A n)"
   15.13          also have "\<dots> \<le> ?d (space M - A (Suc n))"
   15.14 -          using A_in_sets sets_into_space dA_mono[of n] finite_measure_compl M'.finite_measure_compl
   15.15 +          using A_in_sets sets.sets_into_space dA_mono[of n] finite_measure_compl M'.finite_measure_compl
   15.16            by (simp del: A_simps add: sets_eq sets_eq_imp_space_eq[OF sets_eq])
   15.17          finally show "?d (space M) \<le> ?d (space M - A (Suc n))" .
   15.18        qed simp
   15.19 @@ -241,7 +241,7 @@
   15.20        by (auto simp: finite_measure_restricted N.finite_measure_restricted sets_eq)
   15.21      from finite_measure.Radon_Nikodym_aux_epsilon[OF this] guess X .. note X = this
   15.22      with S have "?P (S \<inter> X) S n"
   15.23 -      by (simp add: measure_restricted sets_eq Int) (metis inf_absorb2)
   15.24 +      by (simp add: measure_restricted sets_eq sets.Int) (metis inf_absorb2)
   15.25      hence "\<exists>A. ?P A S n" .. }
   15.26    note Ex_P = this
   15.27    def A \<equiv> "nat_rec (space M) (\<lambda>n A. SOME B. ?P B A n)"
   15.28 @@ -309,7 +309,7 @@
   15.29        hence sets: "?A \<inter> A \<in> sets M" "(space M - ?A) \<inter> A \<in> sets M" using `?A \<in> sets M` by auto
   15.30        hence sets': "?A \<inter> A \<in> sets N" "(space M - ?A) \<inter> A \<in> sets N" by (auto simp: sets_eq)
   15.31        have union: "((?A \<inter> A) \<union> ((space M - ?A) \<inter> A)) = A"
   15.32 -        using sets_into_space[OF `A \<in> sets M`] by auto
   15.33 +        using sets.sets_into_space[OF `A \<in> sets M`] by auto
   15.34        have "\<And>x. x \<in> space M \<Longrightarrow> max (g x) (f x) * indicator A x =
   15.35          g x * indicator (?A \<inter> A) x + f x * indicator ((space M - ?A) \<inter> A) x"
   15.36          by (auto simp: indicator_def max_def)
   15.37 @@ -351,7 +351,7 @@
   15.38    have y_le: "?y \<le> N (space M)" unfolding G_def
   15.39    proof (safe intro!: SUP_least)
   15.40      fix g assume "\<forall>A\<in>sets M. (\<integral>\<^isup>+x. g x * indicator A x \<partial>M) \<le> N A"
   15.41 -    from this[THEN bspec, OF top] show "integral\<^isup>P M g \<le> N (space M)"
   15.42 +    from this[THEN bspec, OF sets.top] show "integral\<^isup>P M g \<le> N (space M)"
   15.43        by (simp cong: positive_integral_cong)
   15.44    qed
   15.45    from SUPR_countable_SUPR[OF `G \<noteq> {}`, of "integral\<^isup>P M"] guess ys .. note ys = this
   15.46 @@ -507,7 +507,7 @@
   15.47      with int_f_finite have "?y + 0 < integral\<^isup>P M f + b * emeasure M A0" unfolding int_f_eq_y
   15.48        using `f \<in> G`
   15.49        by (intro ereal_add_strict_mono) (auto intro!: SUP_upper2 positive_integral_positive)
   15.50 -    also have "\<dots> = integral\<^isup>P M ?f0" using f0_eq[OF top] `A0 \<in> sets M` sets_into_space
   15.51 +    also have "\<dots> = integral\<^isup>P M ?f0" using f0_eq[OF sets.top] `A0 \<in> sets M` sets.sets_into_space
   15.52        by (simp cong: positive_integral_cong)
   15.53      finally have "?y < integral\<^isup>P M ?f0" by simp
   15.54      moreover from `?f0 \<in> G` have "integral\<^isup>P M ?f0 \<le> ?y" by (auto intro!: SUP_upper)
   15.55 @@ -536,7 +536,7 @@
   15.56    let ?a = "SUP Q:?Q. emeasure M Q"
   15.57    have "{} \<in> ?Q" by auto
   15.58    then have Q_not_empty: "?Q \<noteq> {}" by blast
   15.59 -  have "?a \<le> emeasure M (space M)" using sets_into_space
   15.60 +  have "?a \<le> emeasure M (space M)" using sets.sets_into_space
   15.61      by (auto intro!: SUP_least emeasure_mono)
   15.62    then have "?a \<noteq> \<infinity>" using finite_emeasure_space
   15.63      by auto
   15.64 @@ -601,7 +601,7 @@
   15.65          next
   15.66            assume "emeasure M A \<noteq> 0" with * have "N A \<noteq> \<infinity>" using emeasure_nonneg[of M A] by auto
   15.67            with A have "emeasure M ?O_0 + emeasure M A = emeasure M (?O_0 \<union> A)"
   15.68 -            using Q' by (auto intro!: plus_emeasure countable_UN)
   15.69 +            using Q' by (auto intro!: plus_emeasure sets.countable_UN)
   15.70            also have "\<dots> = (SUP i. emeasure M (?O i \<union> A))"
   15.71            proof (rule SUP_emeasure_incseq[of "\<lambda>i. ?O i \<union> A", symmetric, simplified])
   15.72              show "range (\<lambda>i. ?O i \<union> A) \<subseteq> sets M"
   15.73 @@ -712,7 +712,7 @@
   15.74        also have "\<dots> = (\<integral>\<^isup>+x. (\<Sum>i. f i x * indicator (Q i \<inter> A) x) \<partial>M) + \<infinity> * emeasure M (Q0 \<inter> A)"
   15.75          using borel Qi Q0(1) `A \<in> sets M`
   15.76          by (subst positive_integral_add) (auto simp del: ereal_infty_mult
   15.77 -            simp add: positive_integral_cmult_indicator Int intro!: suminf_0_le)
   15.78 +            simp add: positive_integral_cmult_indicator sets.Int intro!: suminf_0_le)
   15.79        also have "\<dots> = (\<Sum>i. N (Q i \<inter> A)) + \<infinity> * emeasure M (Q0 \<inter> A)"
   15.80          by (subst integral_eq[OF `A \<in> sets M`], subst positive_integral_suminf) auto
   15.81        finally have "(\<integral>\<^isup>+x. ?f x * indicator A x \<partial>M) = (\<Sum>i. N (Q i \<inter> A)) + \<infinity> * emeasure M (Q0 \<inter> A)" .
   15.82 @@ -727,7 +727,7 @@
   15.83        moreover have "Q0 \<inter> A \<in> sets M" "((\<Union>i. Q i) \<inter> A) \<in> sets M"
   15.84          using Q_sets `A \<in> sets M` Q0(1) by auto
   15.85        moreover have "((\<Union>i. Q i) \<inter> A) \<union> (Q0 \<inter> A) = A" "((\<Union>i. Q i) \<inter> A) \<inter> (Q0 \<inter> A) = {}"
   15.86 -        using `A \<in> sets M` sets_into_space Q0 by auto
   15.87 +        using `A \<in> sets M` sets.sets_into_space Q0 by auto
   15.88        ultimately have "N A = (\<integral>\<^isup>+x. ?f x * indicator A x \<partial>M)"
   15.89          using plus_emeasure[of "(\<Union>i. Q i) \<inter> A" N "Q0 \<inter> A"] by (simp add: sets_eq)
   15.90        with `A \<in> sets M` borel Q Q0(1) show "emeasure (density M ?f) A = N A"
   15.91 @@ -755,7 +755,7 @@
   15.92      fix A assume "A \<in> null_sets ?MT"
   15.93      with borel have "A \<in> sets M" "AE x in M. x \<in> A \<longrightarrow> h x \<le> 0"
   15.94        by (auto simp add: null_sets_density_iff)
   15.95 -    with pos sets_into_space have "AE x in M. x \<notin> A"
   15.96 +    with pos sets.sets_into_space have "AE x in M. x \<notin> A"
   15.97        by (elim eventually_elim1) (auto simp: not_le[symmetric])
   15.98      then have "A \<in> null_sets M"
   15.99        using `A \<in> sets M` by (simp add: AE_iff_null_sets)
  15.100 @@ -784,7 +784,7 @@
  15.101    assume "density M f = density M g"
  15.102    with borel have eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
  15.103      by (simp add: emeasure_density[symmetric])
  15.104 -  from this[THEN bspec, OF top] fin
  15.105 +  from this[THEN bspec, OF sets.top] fin
  15.106    have g_fin: "integral\<^isup>P M g \<noteq> \<infinity>" by (simp cong: positive_integral_cong)
  15.107    { fix f g assume borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  15.108        and pos: "AE x in M. 0 \<le> f x" "AE x in M. 0 \<le> g x"
  15.109 @@ -898,7 +898,7 @@
  15.110    let ?f'M = "density M f'"
  15.111    { fix A assume "A \<in> sets M"
  15.112      then have "{x \<in> space M. h x * indicator A x \<noteq> 0} = A"
  15.113 -      using pos(1) sets_into_space by (force simp: indicator_def)
  15.114 +      using pos(1) sets.sets_into_space by (force simp: indicator_def)
  15.115      then have "(\<integral>\<^isup>+x. h x * indicator A x \<partial>M) = 0 \<longleftrightarrow> A \<in> null_sets M"
  15.116        using h_borel `A \<in> sets M` h_nn by (subst positive_integral_0_iff) auto }
  15.117    note h_null_sets = this
  15.118 @@ -994,7 +994,7 @@
  15.119    def A \<equiv> "\<lambda>i. f -` (case i of 0 \<Rightarrow> {\<infinity>} | Suc n \<Rightarrow> {.. ereal(of_nat (Suc n))}) \<inter> space M"
  15.120    { fix i j have "A i \<inter> Q j \<in> sets M"
  15.121      unfolding A_def using f Q
  15.122 -    apply (rule_tac Int)
  15.123 +    apply (rule_tac sets.Int)
  15.124      by (cases i) (auto intro: measurable_sets[OF f(1)]) }
  15.125    note A_in_sets = this
  15.126    let ?A = "\<lambda>n. case prod_decode n of (i,j) \<Rightarrow> A i \<inter> Q j"
  15.127 @@ -1133,12 +1133,12 @@
  15.128    note sets_eq_imp_space_eq[OF N, simp]
  15.129    have measurable_N[simp]: "\<And>M'. measurable N M' = measurable M M'" by (auto simp: measurable_def)
  15.130    { fix A assume "A \<in> sets M"
  15.131 -    with inv T T' sets_into_space[OF this]
  15.132 +    with inv T T' sets.sets_into_space[OF this]
  15.133      have "T -` T' -` A \<inter> T -` space M' \<inter> space M = A"
  15.134        by (auto simp: measurable_def) }
  15.135    note eq = this[simp]
  15.136    { fix A assume "A \<in> sets M"
  15.137 -    with inv T T' sets_into_space[OF this]
  15.138 +    with inv T T' sets.sets_into_space[OF this]
  15.139      have "(T' \<circ> T) -` A \<inter> space M = A"
  15.140        by (auto simp: measurable_def) }
  15.141    note eq2 = this[simp]
  15.142 @@ -1168,7 +1168,7 @@
  15.143  
  15.144    have "N = distr N M (T' \<circ> T)"
  15.145      by (subst measure_of_of_measure[of N, symmetric])
  15.146 -       (auto simp add: distr_def sigma_sets_eq intro!: measure_of_eq space_closed)
  15.147 +       (auto simp add: distr_def sets.sigma_sets_eq intro!: measure_of_eq sets.space_closed)
  15.148    also have "\<dots> = distr (distr N M' T) M T'"
  15.149      using T T' by (simp add: distr_distr)
  15.150    also have "\<dots> = distr (density (distr M M' T) (RN_deriv (distr M M' T) (distr N M' T))) M T'"
    16.1 --- a/src/HOL/Probability/Regularity.thy	Thu Nov 22 10:09:54 2012 +0100
    16.2 +++ b/src/HOL/Probability/Regularity.thy	Tue Nov 27 11:29:47 2012 +0100
    16.3 @@ -428,9 +428,9 @@
    16.4        have "M ?U - M (\<Union>i. D i) = M (?U - (\<Union>i. D i))" using U  `(\<Union>i. D i) \<in> sets M`
    16.5          by (subst emeasure_Diff) (auto simp: sb)
    16.6        also have "\<dots> \<le> M (\<Union>i. U i - D i)" using U  `range D \<subseteq> sets M`
    16.7 -        by (intro emeasure_mono) (auto simp: sb intro!: countable_nat_UN Diff)
    16.8 +        by (intro emeasure_mono) (auto simp: sb intro!: sets.countable_nat_UN sets.Diff)
    16.9        also have "\<dots> \<le> (\<Sum>i. M (U i - D i))" using U  `range D \<subseteq> sets M`
   16.10 -        by (intro emeasure_subadditive_countably) (auto intro!: Diff simp: sb)
   16.11 +        by (intro emeasure_subadditive_countably) (auto intro!: sets.Diff simp: sb)
   16.12        also have "\<dots> \<le> (\<Sum>i. ereal e/(2 powr Suc i))" using U `range D \<subseteq> sets M`
   16.13          by (intro suminf_le_pos, subst emeasure_Diff)
   16.14             (auto simp: emeasure_Diff emeasure_eq_measure sb measure_nonneg intro: less_imp_le)
    17.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Thu Nov 22 10:09:54 2012 +0100
    17.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue Nov 27 11:29:47 2012 +0100
    17.3 @@ -1026,7 +1026,7 @@
    17.4  lemma measure_space: "measure_space (space M) (sets M) (emeasure M)"
    17.5    by (cases M) (auto simp: space_def sets_def emeasure_def Abs_measure_inverse)
    17.6  
    17.7 -interpretation sigma_algebra "space M" "sets M" for M :: "'a measure"
    17.8 +interpretation sets!: sigma_algebra "space M" "sets M" for M :: "'a measure"
    17.9    using measure_space[of M] by (auto simp: measure_space_def)
   17.10  
   17.11  definition measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> 'a measure" where
   17.12 @@ -1146,7 +1146,7 @@
   17.13  
   17.14  lemma sets_eq_imp_space_eq:
   17.15    "sets M = sets M' \<Longrightarrow> space M = space M'"
   17.16 -  using top[of M] top[of M'] space_closed[of M] space_closed[of M']
   17.17 +  using sets.top[of M] sets.top[of M'] sets.space_closed[of M] sets.space_closed[of M']
   17.18    by blast
   17.19  
   17.20  lemma emeasure_notin_sets: "A \<notin> sets M \<Longrightarrow> emeasure M A = 0"
   17.21 @@ -1225,7 +1225,7 @@
   17.22    shows "f \<in> measurable M N"
   17.23  proof -
   17.24    interpret A: sigma_algebra \<Omega> "sigma_sets \<Omega> A" using B(2) by (rule sigma_algebra_sigma_sets)
   17.25 -  from B top[of N] A.top space_closed[of N] A.space_closed have \<Omega>: "\<Omega> = space N" by force
   17.26 +  from B sets.top[of N] A.top sets.space_closed[of N] A.space_closed have \<Omega>: "\<Omega> = space N" by force
   17.27    
   17.28    { fix X assume "X \<in> sigma_sets \<Omega> A"
   17.29      then have "f -` X \<inter> space M \<in> sets M \<and> X \<subseteq> \<Omega>"
   17.30 @@ -1237,7 +1237,7 @@
   17.31          have [simp]: "f -` \<Omega> \<inter> space M = space M"
   17.32            by (auto simp add: funcset_mem [OF f])
   17.33          then show ?case
   17.34 -          by (auto simp add: vimage_Diff Diff_Int_distrib2 compl_sets Compl)
   17.35 +          by (auto simp add: vimage_Diff Diff_Int_distrib2 sets.compl_sets Compl)
   17.36        next
   17.37          case (Union a)
   17.38          then show ?case
   17.39 @@ -1316,7 +1316,7 @@
   17.40      using measure unfolding measurable_def by (auto split: split_if_asm)
   17.41    show "(\<lambda>x. if P x then f x else g x) -` A \<inter> space M \<in> sets M"
   17.42      using `A \<in> sets M'` measure P unfolding * measurable_def
   17.43 -    by (auto intro!: Un)
   17.44 +    by (auto intro!: sets.Un)
   17.45  qed
   17.46  
   17.47  lemma measurable_If_set:
   17.48 @@ -1348,7 +1348,7 @@
   17.49          by (simp add: set_eq_iff, safe)
   17.50             (insert i, auto dest: Least_le intro: LeastI intro!: Least_equality)
   17.51        with meas show ?thesis
   17.52 -        by (auto intro!: Int)
   17.53 +        by (auto intro!: sets.Int)
   17.54      next
   17.55        assume i: "(LEAST j. False) \<noteq> i"
   17.56        then have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M =
   17.57 @@ -1363,7 +1363,7 @@
   17.58          by auto
   17.59      qed }
   17.60    then have "(\<Union>i\<in>A. (\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M) \<in> sets M"
   17.61 -    by (intro countable_UN) auto
   17.62 +    by (intro sets.countable_UN) auto
   17.63    moreover have "(\<Union>i\<in>A. (\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M) =
   17.64      (\<lambda>x. LEAST j. P j x) -` A \<inter> space M" by auto
   17.65    ultimately show ?thesis by auto
   17.66 @@ -1417,7 +1417,7 @@
   17.67        by (auto dest: finite_subset)
   17.68      moreover assume "\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M"
   17.69      ultimately have "f -` X \<inter> space M \<in> sets M"
   17.70 -      using `X \<subseteq> A` by (auto intro!: finite_UN simp del: UN_simps) }
   17.71 +      using `X \<subseteq> A` by (auto intro!: sets.finite_UN simp del: UN_simps) }
   17.72    then show ?thesis
   17.73      unfolding measurable_def by auto
   17.74  qed
   17.75 @@ -1434,7 +1434,7 @@
   17.76    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))"
   17.77      by auto
   17.78    also have "\<dots> \<in> sets M" using f[THEN measurable_sets, OF A] g[THEN measurable_sets]
   17.79 -    by (auto intro!: countable_UN measurable_sets)
   17.80 +    by (auto intro!: sets.countable_UN measurable_sets)
   17.81    finally show "(\<lambda>x. f (g x) x) -` A \<inter> space M \<in> sets M" .
   17.82  qed
   17.83  
   17.84 @@ -1466,7 +1466,7 @@
   17.85      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> {})}"
   17.86        unfolding UNIV_bool Pow_insert Pow_empty by auto
   17.87      then have "P -` X \<inter> space M \<in> sets M"
   17.88 -      by (auto intro!: sets_Collect_neg sets_Collect_imp sets_Collect_conj sets_Collect_const P) }
   17.89 +      by (auto intro!: sets.sets_Collect_neg sets.sets_Collect_imp sets.sets_Collect_conj sets.sets_Collect_const P) }
   17.90    then show "pred M P"
   17.91      by (auto simp: measurable_def)
   17.92  qed
   17.93 @@ -1714,13 +1714,13 @@
   17.94    measurable_compose_rev[measurable_dest]
   17.95    pred_sets1[measurable_dest]
   17.96    pred_sets2[measurable_dest]
   17.97 -  sets_into_space[measurable_dest]
   17.98 +  sets.sets_into_space[measurable_dest]
   17.99  
  17.100  declare
  17.101 -  top[measurable]
  17.102 -  empty_sets[measurable (raw)]
  17.103 -  Un[measurable (raw)]
  17.104 -  Diff[measurable (raw)]
  17.105 +  sets.top[measurable]
  17.106 +  sets.empty_sets[measurable (raw)]
  17.107 +  sets.Un[measurable (raw)]
  17.108 +  sets.Diff[measurable (raw)]
  17.109  
  17.110  declare
  17.111    measurable_count_space[measurable (raw)]
  17.112 @@ -1777,7 +1777,7 @@
  17.113    shows 
  17.114      "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i. P x i)"
  17.115      "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i. P x i)"
  17.116 -  by (auto intro!: sets_Collect_countable_All sets_Collect_countable_Ex simp: pred_def)
  17.117 +  by (auto intro!: sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex simp: pred_def)
  17.118  
  17.119  lemma pred_intros_countable_bounded[measurable (raw)]:
  17.120    fixes X :: "'i :: countable set"
  17.121 @@ -1793,7 +1793,7 @@
  17.122    "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))"
  17.123    "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)"
  17.124    "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)"
  17.125 -  by (auto intro!: sets_Collect_finite_Ex sets_Collect_finite_All simp: iff_conv_conj_imp pred_def)
  17.126 +  by (auto intro!: sets.sets_Collect_finite_Ex sets.sets_Collect_finite_All simp: iff_conv_conj_imp pred_def)
  17.127  
  17.128  lemma countable_Un_Int[measurable (raw)]:
  17.129    "(\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Union>i\<in>I. N i) \<in> sets M"
  17.130 @@ -1854,7 +1854,7 @@
  17.131    by (auto simp: Int_def conj_commute eq_commute pred_def)
  17.132  
  17.133  declare
  17.134 -  Int[measurable (raw)]
  17.135 +  sets.Int[measurable (raw)]
  17.136  
  17.137  lemma pred_in_If[measurable (raw)]:
  17.138    "(P \<Longrightarrow> pred M (\<lambda>x. x \<in> A x)) \<Longrightarrow> (\<not> P \<Longrightarrow> pred M (\<lambda>x. x \<in> B x)) \<Longrightarrow>