author immler Tue Nov 27 11:29:47 2012 +0100 (2012-11-27) changeset 50244 de72bbe42190 parent 50243 0d97ef1d6de9 child 50245 dea9363887a6
qualified interpretation of sigma_algebra, to avoid name clashes
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.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.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.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.30 @@ -79,10 +79,12 @@
1.31    using measurable_Pair[OF assms] by simp
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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.80 @@ -916,7 +916,7 @@
9.81      qed }
9.82    note B_mono = this
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.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.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.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.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.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.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
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.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.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.11  lemma emeasure_additive: "additive (sets M) (emeasure M)"
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.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.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.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.51 +  by (auto simp add: sets.countably_additive_iff_continuous_from_below emeasure_positive
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.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.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.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.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.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
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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.133  declare
17.134 -  Int[measurable (raw)]
17.135 +  sets.Int[measurable (raw)]
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>