--- a/src/HOL/Probability/Sigma_Algebra.thy Wed Feb 02 10:35:41 2011 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy Wed Feb 02 12:34:45 2011 +0100
@@ -29,7 +29,7 @@
sets :: "'a set set"
locale algebra =
- fixes M :: "'a algebra"
+ fixes M :: "('a, 'b) algebra_scheme"
assumes space_closed: "sets M \<subseteq> Pow (space M)"
and empty_sets [iff]: "{} \<in> sets M"
and compl_sets [intro]: "!!a. a \<in> sets M \<Longrightarrow> space M - a \<in> sets M"
@@ -104,7 +104,7 @@
section {* Restricted algebras *}
abbreviation (in algebra)
- "restricted_space A \<equiv> \<lparr> space = A, sets = (\<lambda>S. (A \<inter> S)) ` sets M \<rparr>"
+ "restricted_space A \<equiv> \<lparr> space = A, sets = (\<lambda>S. (A \<inter> S)) ` sets M, \<dots> = more M \<rparr>"
lemma (in algebra) restricted_algebra:
assumes "A \<in> sets M" shows "algebra (restricted_space A)"
@@ -222,7 +222,7 @@
| Union: "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Union>i. a i) \<in> sigma_sets sp A"
definition
- "sigma M = \<lparr> space = space M, sets = sigma_sets (space M) (sets M) \<rparr>"
+ "sigma M = \<lparr> space = space M, sets = sigma_sets (space M) (sets M), \<dots> = more M \<rparr>"
lemma (in sigma_algebra) sigma_sets_subset:
assumes a: "a \<subseteq> sets M"
@@ -354,12 +354,12 @@
qed
lemma sigma_sets_Int:
- assumes "A \<in> sigma_sets sp st"
- shows "op \<inter> A ` sigma_sets sp st = sigma_sets (A \<inter> sp) (op \<inter> A ` st)"
+ assumes "A \<in> sigma_sets sp st" "A \<subseteq> sp"
+ shows "op \<inter> A ` sigma_sets sp st = sigma_sets A (op \<inter> A ` st)"
proof (intro equalityI subsetI)
fix x assume "x \<in> op \<inter> A ` sigma_sets sp st"
then obtain y where "y \<in> sigma_sets sp st" "x = y \<inter> A" by auto
- then show "x \<in> sigma_sets (A \<inter> sp) (op \<inter> A ` st)"
+ then have "x \<in> sigma_sets (A \<inter> sp) (op \<inter> A ` st)"
proof (induct arbitrary: x)
case (Compl a)
then show ?case
@@ -370,13 +370,15 @@
by (auto intro!: sigma_sets.Union
simp add: UN_extend_simps simp del: UN_simps)
qed (auto intro!: sigma_sets.intros)
+ then show "x \<in> sigma_sets A (op \<inter> A ` st)"
+ using `A \<subseteq> sp` by (simp add: Int_absorb2)
next
- fix x assume "x \<in> sigma_sets (A \<inter> sp) (op \<inter> A ` st)"
+ fix x assume "x \<in> sigma_sets A (op \<inter> A ` st)"
then show "x \<in> op \<inter> A ` sigma_sets sp st"
proof induct
case (Compl a)
then obtain x where "a = A \<inter> x" "x \<in> sigma_sets sp st" by auto
- then show ?case
+ then show ?case using `A \<subseteq> sp`
by (force simp add: image_iff intro!: bexI[of _ "sp - x"] sigma_sets.Compl)
next
case (Union a)
@@ -707,7 +709,7 @@
subsection {* Sigma algebra generated by function preimages *}
definition (in sigma_algebra)
- "vimage_algebra S f = \<lparr> space = S, sets = (\<lambda>A. f -` A \<inter> S) ` sets M \<rparr>"
+ "vimage_algebra S f = \<lparr> space = S, sets = (\<lambda>A. f -` A \<inter> S) ` sets M, \<dots> = more M \<rparr>"
lemma (in sigma_algebra) in_vimage_algebra[simp]:
"A \<in> sets (vimage_algebra S f) \<longleftrightarrow> (\<exists>B\<in>sets M. A = f -` B \<inter> S)"
@@ -870,7 +872,7 @@
section {* Conditional space *}
definition (in algebra)
- "image_space X = \<lparr> space = X`space M, sets = (\<lambda>S. X`S) ` sets M \<rparr>"
+ "image_space X = \<lparr> space = X`space M, sets = (\<lambda>S. X`S) ` sets M, \<dots> = more M \<rparr>"
definition (in algebra)
"conditional_space X A = algebra.image_space (restricted_space A) X"
@@ -1158,7 +1160,7 @@
section {* Dynkin systems *}
locale dynkin_system =
- fixes M :: "'a algebra"
+ fixes M :: "('a, 'b) algebra_scheme"
assumes space_closed: "sets M \<subseteq> Pow (space M)"
and space: "space M \<in> sets M"
and compl[intro!]: "\<And>A. A \<in> sets M \<Longrightarrow> space M - A \<in> sets M"
@@ -1239,12 +1241,12 @@
subsection "Smallest Dynkin systems"
-definition dynkin :: "'a algebra \<Rightarrow> 'a algebra" where
+definition dynkin where
"dynkin M = \<lparr> space = space M,
- sets = \<Inter>{D. dynkin_system \<lparr> space = space M, sets = D\<rparr> \<and> sets M \<subseteq> D}\<rparr>"
+ sets = \<Inter>{D. dynkin_system \<lparr> space = space M, sets = D \<rparr> \<and> sets M \<subseteq> D},
+ \<dots> = more M \<rparr>"
lemma dynkin_system_dynkin:
- fixes M :: "'a algebra"
assumes "sets M \<subseteq> Pow (space M)"
shows "dynkin_system (dynkin M)"
proof (rule dynkin_systemI)
@@ -1311,21 +1313,17 @@
qed
lemma (in dynkin_system) dynkin_subset:
- fixes N :: "'a algebra"
assumes "sets N \<subseteq> sets M"
assumes "space N = space M"
shows "sets (dynkin N) \<subseteq> sets M"
proof -
- have *: "\<lparr>space = space N, sets = sets M\<rparr> = M"
- unfolding `space N = space M` by simp
have "dynkin_system M" by default
- then have "dynkin_system \<lparr>space = space N, sets = sets M\<rparr>"
- using assms unfolding * by simp
+ then have "dynkin_system \<lparr>space = space N, sets = sets M \<rparr>"
+ using assms unfolding dynkin_system_def by simp
with `sets N \<subseteq> sets M` show ?thesis by (auto simp add: dynkin_def)
qed
lemma sigma_eq_dynkin:
- fixes M :: "'a algebra"
assumes sets: "sets M \<subseteq> Pow (space M)"
assumes "Int_stable M"
shows "sigma M = dynkin M"
@@ -1367,7 +1365,7 @@
have "sigma_sets (space M) (sets M) \<subseteq> sets (dynkin M)" by auto
ultimately have "sigma_sets (space M) (sets M) = sets (dynkin M)" by auto
then show ?thesis
- by (intro algebra.equality) (simp_all add: sigma_def)
+ by (auto intro!: algebra.equality simp: sigma_def dynkin_def)
qed
lemma (in dynkin_system) dynkin_idem:
@@ -1381,23 +1379,22 @@
by (intro dynkin_subset) auto
qed
then show ?thesis
- by (auto intro!: algebra.equality)
+ by (auto intro!: algebra.equality simp: dynkin_def)
qed
lemma (in dynkin_system) dynkin_lemma:
- fixes E :: "'a algebra"
- assumes "Int_stable E" and E: "sets E \<subseteq> sets M" "space E = space M"
- and "sets M \<subseteq> sets (sigma E)"
- shows "sigma E = M"
+ assumes "Int_stable E"
+ and E: "sets E \<subseteq> sets M" "space E = space M" "sets M \<subseteq> sets (sigma E)"
+ shows "sets (sigma E) = sets M"
proof -
have "sets E \<subseteq> Pow (space E)"
- using E sets_into_space by auto
+ using E sets_into_space by force
then have "sigma E = dynkin E"
using `Int_stable E` by (rule sigma_eq_dynkin)
moreover then have "sets (dynkin E) = sets M"
- using assms dynkin_subset[OF E] by simp
+ using assms dynkin_subset[OF E(1,2)] by simp
ultimately show ?thesis
- using E by simp
+ using assms by (auto intro!: algebra.equality simp: dynkin_def)
qed
subsection "Sigma algebras on finite sets"
@@ -1467,6 +1464,7 @@
lemma vimage_algebra_sigma:
assumes bi: "bij_inv (space (sigma F)) (space (sigma E)) f e"
and "sets E \<subseteq> Pow (space E)" and F: "sets F \<subseteq> Pow (space F)"
+ and "more E = more F"
and "f \<in> measurable F E" "e \<in> measurable E F"
shows "sigma_algebra.vimage_algebra (sigma E) (space (sigma F)) f = sigma F"
proof -
@@ -1486,8 +1484,8 @@
using `f \<in> measurable F E` unfolding measurable_def by auto
qed
show "vimage_algebra (space (sigma F)) f = sigma F"
- unfolding vimage_algebra_def
- using assms by (auto simp: bij_inv_def eq sigma_sets_vimage[symmetric] sigma_def)
+ unfolding vimage_algebra_def using assms
+ by (auto simp: bij_inv_def eq sigma_sets_vimage[symmetric] sigma_def)
qed
lemma measurable_sigma_sigma: