1.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Thu May 26 14:12:00 2011 +0200
     1.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Thu May 26 14:12:01 2011 +0200
     1.3 @@ -321,12 +321,6 @@
     1.4  sublocale pair_sigma_finite \<subseteq> pair_sigma_algebra M1 M2
     1.5    by default
     1.6  
     1.7 -lemma sigma_sets_subseteq: assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
     1.8 -proof
     1.9 -  fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
    1.10 -    by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros)
    1.11 -qed
    1.12 -
    1.13  lemma (in pair_sigma_finite) measure_cut_measurable_fst:
    1.14    assumes "Q \<in> sets P" shows "(\<lambda>x. measure M2 (Pair x -` Q)) \<in> borel_measurable M1" (is "?s Q \<in> _")
    1.15  proof -

     2.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Thu May 26 14:12:00 2011 +0200
     2.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Thu May 26 14:12:01 2011 +0200
     2.3 @@ -186,6 +186,11 @@
     2.4    "{x\<in>space M. P} \<in> sets M"
     2.5    by (cases P) auto
     2.6  
     2.7 +lemma algebra_single_set:
     2.8 +  assumes "X \<subseteq> S"
     2.9 +  shows "algebra \<lparr> space = S, sets = { {}, X, S - X, S }\<rparr>"
    2.10 +  by default (insert `X \<subseteq> S`, auto)
    2.11 +
    2.12  section {* Restricted algebras *}
    2.13  
    2.14  abbreviation (in algebra)
    2.15 @@ -201,6 +206,18 @@
    2.16    assumes countable_nat_UN [intro]:
    2.17           "!!A. range A \<subseteq> sets M \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
    2.18  
    2.19 +lemma (in algebra) is_sigma_algebra:
    2.20 +  assumes "finite (sets M)"
    2.21 +  shows "sigma_algebra M"
    2.22 +proof
    2.23 +  fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets M"
    2.24 +  then have "(\<Union>i. A i) = (\<Union>s\<in>sets M \<inter> range A. s)"
    2.25 +    by auto
    2.26 +  also have "(\<Union>s\<in>sets M \<inter> range A. s) \<in> sets M"
    2.27 +    using `finite (sets M)` by (auto intro: finite_UN)
    2.28 +  finally show "(\<Union>i. A i) \<in> sets M" .
    2.29 +qed
    2.30 +
    2.31  lemma countable_UN_eq:
    2.32    fixes A :: "'i::countable \<Rightarrow> 'a set"
    2.33    shows "(range A \<subseteq> sets M \<longrightarrow> (\<Union>i. A i) \<in> sets M) \<longleftrightarrow>
    2.34 @@ -284,6 +301,11 @@
    2.35    sets_Collect_imp sets_Collect_disj sets_Collect_conj sets_Collect_neg sets_Collect_const
    2.36    sets_Collect_countable_All sets_Collect_countable_Ex sets_Collect_countable_All
    2.37  
    2.38 +lemma sigma_algebra_single_set:
    2.39 +  assumes "X \<subseteq> S"
    2.40 +  shows "sigma_algebra \<lparr> space = S, sets = { {}, X, S - X, S }\<rparr>"
    2.41 +  using algebra.is_sigma_algebra[OF algebra_single_set[OF `X \<subseteq> S`]] by simp
    2.42 +
    2.43  subsection {* Binary Unions *}
    2.44  
    2.45  definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"
    2.46 @@ -441,6 +463,12 @@
    2.47      "sets N \<subseteq> sets M \<Longrightarrow> space N = space M \<Longrightarrow> sets (sigma N) \<subseteq> (sets M)"
    2.48    by (simp add: sigma_def sigma_sets_subset)
    2.49  
    2.50 +lemma sigma_sets_subseteq: assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
    2.51 +proof
    2.52 +  fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
    2.53 +    by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros)
    2.54 +qed
    2.55 +
    2.56  lemma (in sigma_algebra) restriction_in_sets:
    2.57    fixes A :: "nat \<Rightarrow> 'a set"
    2.58    assumes "S \<in> sets M"
    2.59 @@ -527,6 +555,26 @@
    2.60  lemma (in sigma_algebra) sigma_eq[simp]: "sigma M = M"
    2.61    unfolding sigma_def sigma_sets_eq by simp
    2.62  
    2.63 +lemma sigma_sets_singleton:
    2.64 +  assumes "X \<subseteq> S"
    2.65 +  shows "sigma_sets S { X } = { {}, X, S - X, S }"
    2.66 +proof -
    2.67 +  interpret sigma_algebra "\<lparr> space = S, sets = { {}, X, S - X, S }\<rparr>"
    2.68 +    by (rule sigma_algebra_single_set) fact
    2.69 +  have "sigma_sets S { X } \<subseteq> sigma_sets S { {}, X, S - X, S }"
    2.70 +    by (rule sigma_sets_subseteq) simp
    2.71 +  moreover have "\<dots> = { {}, X, S - X, S }"
    2.72 +    using sigma_eq unfolding sigma_def by simp
    2.73 +  moreover
    2.74 +  { fix A assume "A \<in> { {}, X, S - X, S }"
    2.75 +    then have "A \<in> sigma_sets S { X }"
    2.76 +      by (auto intro: sigma_sets.intros sigma_sets_top) }
    2.77 +  ultimately have "sigma_sets S { X } = sigma_sets S { {}, X, S - X, S }"
    2.78 +    by (intro antisym) auto
    2.79 +  with sigma_eq show ?thesis
    2.80 +    unfolding sigma_def by simp
    2.81 +qed
    2.82 +
    2.83  lemma restricted_sigma:
    2.84    assumes S: "S \<in> sets (sigma M)" and M: "sets M \<subseteq> Pow (space M)"
    2.85    shows "algebra.restricted_space (sigma M) S = sigma (algebra.restricted_space M S)"