1.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Thu May 26 14:12:00 2011 +0200
     1.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Thu May 26 14:12:01 2011 +0200
     1.3 @@ -186,6 +186,11 @@
     1.4    "{x\<in>space M. P} \<in> sets M"
     1.5    by (cases P) auto
     1.6  
     1.7 +lemma algebra_single_set:
     1.8 +  assumes "X \<subseteq> S"
     1.9 +  shows "algebra \<lparr> space = S, sets = { {}, X, S - X, S }\<rparr>"
    1.10 +  by default (insert `X \<subseteq> S`, auto)
    1.11 +
    1.12  section {* Restricted algebras *}
    1.13  
    1.14  abbreviation (in algebra)
    1.15 @@ -201,6 +206,18 @@
    1.16    assumes countable_nat_UN [intro]:
    1.17           "!!A. range A \<subseteq> sets M \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
    1.18  
    1.19 +lemma (in algebra) is_sigma_algebra:
    1.20 +  assumes "finite (sets M)"
    1.21 +  shows "sigma_algebra M"
    1.22 +proof
    1.23 +  fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets M"
    1.24 +  then have "(\<Union>i. A i) = (\<Union>s\<in>sets M \<inter> range A. s)"
    1.25 +    by auto
    1.26 +  also have "(\<Union>s\<in>sets M \<inter> range A. s) \<in> sets M"
    1.27 +    using `finite (sets M)` by (auto intro: finite_UN)
    1.28 +  finally show "(\<Union>i. A i) \<in> sets M" .
    1.29 +qed
    1.30 +
    1.31  lemma countable_UN_eq:
    1.32    fixes A :: "'i::countable \<Rightarrow> 'a set"
    1.33    shows "(range A \<subseteq> sets M \<longrightarrow> (\<Union>i. A i) \<in> sets M) \<longleftrightarrow>
    1.34 @@ -284,6 +301,11 @@
    1.35    sets_Collect_imp sets_Collect_disj sets_Collect_conj sets_Collect_neg sets_Collect_const
    1.36    sets_Collect_countable_All sets_Collect_countable_Ex sets_Collect_countable_All
    1.37  
    1.38 +lemma sigma_algebra_single_set:
    1.39 +  assumes "X \<subseteq> S"
    1.40 +  shows "sigma_algebra \<lparr> space = S, sets = { {}, X, S - X, S }\<rparr>"
    1.41 +  using algebra.is_sigma_algebra[OF algebra_single_set[OF `X \<subseteq> S`]] by simp
    1.42 +
    1.43  subsection {* Binary Unions *}
    1.44  
    1.45  definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"
    1.46 @@ -441,6 +463,12 @@
    1.47      "sets N \<subseteq> sets M \<Longrightarrow> space N = space M \<Longrightarrow> sets (sigma N) \<subseteq> (sets M)"
    1.48    by (simp add: sigma_def sigma_sets_subset)
    1.49  
    1.50 +lemma sigma_sets_subseteq: assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
    1.51 +proof
    1.52 +  fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
    1.53 +    by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros)
    1.54 +qed
    1.55 +
    1.56  lemma (in sigma_algebra) restriction_in_sets:
    1.57    fixes A :: "nat \<Rightarrow> 'a set"
    1.58    assumes "S \<in> sets M"
    1.59 @@ -527,6 +555,26 @@
    1.60  lemma (in sigma_algebra) sigma_eq[simp]: "sigma M = M"
    1.61    unfolding sigma_def sigma_sets_eq by simp
    1.62  
    1.63 +lemma sigma_sets_singleton:
    1.64 +  assumes "X \<subseteq> S"
    1.65 +  shows "sigma_sets S { X } = { {}, X, S - X, S }"
    1.66 +proof -
    1.67 +  interpret sigma_algebra "\<lparr> space = S, sets = { {}, X, S - X, S }\<rparr>"
    1.68 +    by (rule sigma_algebra_single_set) fact
    1.69 +  have "sigma_sets S { X } \<subseteq> sigma_sets S { {}, X, S - X, S }"
    1.70 +    by (rule sigma_sets_subseteq) simp
    1.71 +  moreover have "\<dots> = { {}, X, S - X, S }"
    1.72 +    using sigma_eq unfolding sigma_def by simp
    1.73 +  moreover
    1.74 +  { fix A assume "A \<in> { {}, X, S - X, S }"
    1.75 +    then have "A \<in> sigma_sets S { X }"
    1.76 +      by (auto intro: sigma_sets.intros sigma_sets_top) }
    1.77 +  ultimately have "sigma_sets S { X } = sigma_sets S { {}, X, S - X, S }"
    1.78 +    by (intro antisym) auto
    1.79 +  with sigma_eq show ?thesis
    1.80 +    unfolding sigma_def by simp
    1.81 +qed
    1.82 +
    1.83  lemma restricted_sigma:
    1.84    assumes S: "S \<in> sets (sigma M)" and M: "sets M \<subseteq> Pow (space M)"
    1.85    shows "algebra.restricted_space (sigma M) S = sigma (algebra.restricted_space M S)"