# HG changeset patch
# User hoelzl
# Date 1306411921 -7200
# Node ID 43864e7475df708ba48e9eed2844c32651d48cfb
# Parent  685df9c0626de46fc471f3e041489e980a966144
add lemma sigma_sets_singleton

diff -r 685df9c0626d -r 43864e7475df src/HOL/Probability/Binary_Product_Measure.thy
--- a/src/HOL/Probability/Binary_Product_Measure.thy	Thu May 26 14:12:00 2011 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Thu May 26 14:12:01 2011 +0200
@@ -321,12 +321,6 @@
 sublocale pair_sigma_finite \<subseteq> pair_sigma_algebra M1 M2
   by default
 
-lemma sigma_sets_subseteq: assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
-proof
-  fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
-    by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros)
-qed
-
 lemma (in pair_sigma_finite) measure_cut_measurable_fst:
   assumes "Q \<in> sets P" shows "(\<lambda>x. measure M2 (Pair x -` Q)) \<in> borel_measurable M1" (is "?s Q \<in> _")
 proof -
diff -r 685df9c0626d -r 43864e7475df src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Thu May 26 14:12:00 2011 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Thu May 26 14:12:01 2011 +0200
@@ -186,6 +186,11 @@
   "{x\<in>space M. P} \<in> sets M"
   by (cases P) auto
 
+lemma algebra_single_set:
+  assumes "X \<subseteq> S"
+  shows "algebra \<lparr> space = S, sets = { {}, X, S - X, S }\<rparr>"
+  by default (insert `X \<subseteq> S`, auto)
+
 section {* Restricted algebras *}
 
 abbreviation (in algebra)
@@ -201,6 +206,18 @@
   assumes countable_nat_UN [intro]:
          "!!A. range A \<subseteq> sets M \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
 
+lemma (in algebra) is_sigma_algebra:
+  assumes "finite (sets M)"
+  shows "sigma_algebra M"
+proof
+  fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets M"
+  then have "(\<Union>i. A i) = (\<Union>s\<in>sets M \<inter> range A. s)"
+    by auto
+  also have "(\<Union>s\<in>sets M \<inter> range A. s) \<in> sets M"
+    using `finite (sets M)` by (auto intro: finite_UN)
+  finally show "(\<Union>i. A i) \<in> sets M" .
+qed
+
 lemma countable_UN_eq:
   fixes A :: "'i::countable \<Rightarrow> 'a set"
   shows "(range A \<subseteq> sets M \<longrightarrow> (\<Union>i. A i) \<in> sets M) \<longleftrightarrow>
@@ -284,6 +301,11 @@
   sets_Collect_imp sets_Collect_disj sets_Collect_conj sets_Collect_neg sets_Collect_const
   sets_Collect_countable_All sets_Collect_countable_Ex sets_Collect_countable_All
 
+lemma sigma_algebra_single_set:
+  assumes "X \<subseteq> S"
+  shows "sigma_algebra \<lparr> space = S, sets = { {}, X, S - X, S }\<rparr>"
+  using algebra.is_sigma_algebra[OF algebra_single_set[OF `X \<subseteq> S`]] by simp
+
 subsection {* Binary Unions *}
 
 definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"
@@ -441,6 +463,12 @@
     "sets N \<subseteq> sets M \<Longrightarrow> space N = space M \<Longrightarrow> sets (sigma N) \<subseteq> (sets M)"
   by (simp add: sigma_def sigma_sets_subset)
 
+lemma sigma_sets_subseteq: assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
+proof
+  fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
+    by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros)
+qed
+
 lemma (in sigma_algebra) restriction_in_sets:
   fixes A :: "nat \<Rightarrow> 'a set"
   assumes "S \<in> sets M"
@@ -527,6 +555,26 @@
 lemma (in sigma_algebra) sigma_eq[simp]: "sigma M = M"
   unfolding sigma_def sigma_sets_eq by simp
 
+lemma sigma_sets_singleton:
+  assumes "X \<subseteq> S"
+  shows "sigma_sets S { X } = { {}, X, S - X, S }"
+proof -
+  interpret sigma_algebra "\<lparr> space = S, sets = { {}, X, S - X, S }\<rparr>"
+    by (rule sigma_algebra_single_set) fact
+  have "sigma_sets S { X } \<subseteq> sigma_sets S { {}, X, S - X, S }"
+    by (rule sigma_sets_subseteq) simp
+  moreover have "\<dots> = { {}, X, S - X, S }"
+    using sigma_eq unfolding sigma_def by simp
+  moreover
+  { fix A assume "A \<in> { {}, X, S - X, S }"
+    then have "A \<in> sigma_sets S { X }"
+      by (auto intro: sigma_sets.intros sigma_sets_top) }
+  ultimately have "sigma_sets S { X } = sigma_sets S { {}, X, S - X, S }"
+    by (intro antisym) auto
+  with sigma_eq show ?thesis
+    unfolding sigma_def by simp
+qed
+
 lemma restricted_sigma:
   assumes S: "S \<in> sets (sigma M)" and M: "sets M \<subseteq> Pow (space M)"
   shows "algebra.restricted_space (sigma M) S = sigma (algebra.restricted_space M S)"