--- a/src/HOL/Probability/Sigma_Algebra.thy Thu May 26 09:42:04 2011 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy Thu May 26 14:11:57 2011 +0200
@@ -417,6 +417,20 @@
by (metis sigma_sets_subset subset_refl)
qed
+lemma sigma_sets_eqI:
+ assumes A: "\<And>a. a \<in> A \<Longrightarrow> a \<in> sigma_sets M B"
+ assumes B: "\<And>b. b \<in> B \<Longrightarrow> b \<in> sigma_sets M A"
+ shows "sigma_sets M A = sigma_sets M B"
+proof (intro set_eqI iffI)
+ fix a assume "a \<in> sigma_sets M A"
+ from this A show "a \<in> sigma_sets M B"
+ by induct (auto intro!: sigma_sets.intros del: sigma_sets.Basic)
+next
+ fix b assume "b \<in> sigma_sets M B"
+ from this B show "b \<in> sigma_sets M A"
+ by induct (auto intro!: sigma_sets.intros del: sigma_sets.Basic)
+qed
+
lemma sigma_algebra_sigma:
"sets M \<subseteq> Pow (space M) \<Longrightarrow> sigma_algebra (sigma M)"
apply (rule sigma_algebra_sigma_sets)
@@ -1297,6 +1311,14 @@
lemma (in algebra) Int_stable: "Int_stable M"
unfolding Int_stable_def by auto
+lemma Int_stableI:
+ "(\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<inter> b \<in> A) \<Longrightarrow> Int_stable \<lparr> space = \<Omega>, sets = A \<rparr>"
+ unfolding Int_stable_def by auto
+
+lemma Int_stableD:
+ "Int_stable M \<Longrightarrow> a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b \<in> sets M"
+ unfolding Int_stable_def by auto
+
lemma (in dynkin_system) sigma_algebra_eq_Int_stable:
"sigma_algebra M \<longleftrightarrow> Int_stable M"
proof