# HG changeset patch
# User hoelzl
# Date 1305635814 -7200
# Node ID b0746bd57a41a994371353df03c8f426d365a21b
# Parent  36353d913424e4da066d666ed149d7e5730c76a3
the measurable sets with null measure form a ring

diff -r 36353d913424 -r b0746bd57a41 src/HOL/Probability/Complete_Measure.thy
--- a/src/HOL/Probability/Complete_Measure.thy	Tue May 17 12:24:48 2011 +0200
+++ b/src/HOL/Probability/Complete_Measure.thy	Tue May 17 14:36:54 2011 +0200
@@ -144,7 +144,7 @@
   have "(\<Union>i. S i) \<in> sets completion" using S by auto
   from null_part[OF this] guess N' .. note N' = this
   let ?N = "(\<Union>i. N i) \<union> N'"
-  have null_set: "?N \<in> null_sets" using N' UN_N by (intro null_sets_Un) auto
+  have null_set: "?N \<in> null_sets" using N' UN_N by (intro nullsets.Un) auto
   have "main_part (\<Union>i. S i) \<union> ?N = (main_part (\<Union>i. S i) \<union> null_part (\<Union>i. S i)) \<union> ?N"
     using N' by auto
   also have "\<dots> = (\<Union>i. main_part (S i) \<union> null_part (S i)) \<union> ?N"
@@ -212,7 +212,7 @@
   from choice[OF this] obtain N where
     N: "\<And>x. null_part (?F x) \<subseteq> N x" "\<And>x. N x \<in> null_sets" by auto
   let ?N = "\<Union>x\<in>f`space M. N x" let "?f' x" = "if x \<in> ?N then undefined else f x"
-  have sets: "?N \<in> null_sets" using N fin by (intro null_sets_finite_UN) auto
+  have sets: "?N \<in> null_sets" using N fin by (intro nullsets.finite_UN) auto
   show ?thesis unfolding simple_function_def
   proof (safe intro!: exI[of _ ?f'])
     have "?f' ` space M \<subseteq> f`space M \<union> {undefined}" by auto
diff -r 36353d913424 -r b0746bd57a41 src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Tue May 17 12:24:48 2011 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue May 17 14:36:54 2011 +0200
@@ -917,8 +917,9 @@
     with i show "A \<in> sigma_sets ?O ?G"
       by (intro sigma_sets.Basic UN_I[where a="{i}"]) auto
   qed
-  finally show "sets (Pi\<^isub>P I M) = sets ?S"
+  also have "\<dots> = sets ?S"
     by (simp add: sets_sigma)
+  finally show "sets (Pi\<^isub>P I M) = sets ?S" .
 qed simp_all
 
 lemma (in product_prob_space) measurable_into_infprod_algebra:
diff -r 36353d913424 -r b0746bd57a41 src/HOL/Probability/Measure.thy
--- a/src/HOL/Probability/Measure.thy	Tue May 17 12:24:48 2011 +0200
+++ b/src/HOL/Probability/Measure.thy	Tue May 17 14:36:54 2011 +0200
@@ -552,16 +552,20 @@
 
 abbreviation (in measure_space) "null_sets \<equiv> {N\<in>sets M. \<mu> N = 0}"
 
-lemma (in measure_space) null_sets_Un[intro]:
-  assumes "N \<in> null_sets" "N' \<in> null_sets"
-  shows "N \<union> N' \<in> null_sets"
-proof (intro conjI CollectI)
-  show "N \<union> N' \<in> sets M" using assms by auto
-  then have "0 \<le> \<mu> (N \<union> N')" by simp
-  moreover have "\<mu> (N \<union> N') \<le> \<mu> N + \<mu> N'"
-    using assms by (intro measure_subadditive) auto
-  ultimately show "\<mu> (N \<union> N') = 0" using assms by auto
-qed
+sublocale measure_space \<subseteq> nullsets!: ring_of_sets "\<lparr> space = space M, sets = null_sets \<rparr>"
+  where "space \<lparr> space = space M, sets = null_sets \<rparr> = space M"
+  and "sets \<lparr> space = space M, sets = null_sets \<rparr> = null_sets"
+proof -
+  { fix A B assume sets: "A \<in> sets M" "B \<in> sets M"
+    moreover then have "\<mu> (A \<union> B) \<le> \<mu> A + \<mu> B" "\<mu> (A - B) \<le> \<mu> A"
+      by (auto intro!: measure_subadditive measure_mono)
+    moreover assume "\<mu> B = 0" "\<mu> A = 0"
+    ultimately have "\<mu> (A - B) = 0" "\<mu> (A \<union> B) = 0"
+      by (auto intro!: antisym) }
+  note null = this
+  show "ring_of_sets \<lparr> space = space M, sets = null_sets \<rparr>"
+    by default (insert sets_into_space null, auto)
+qed simp_all
 
 lemma UN_from_nat: "(\<Union>i. N i) = (\<Union>i. N (Countable.from_nat i))"
 proof -
@@ -583,17 +587,6 @@
   ultimately show "\<mu> (\<Union>i. N i) = 0" using assms by auto
 qed
 
-lemma (in measure_space) null_sets_finite_UN:
-  assumes "finite S" "\<And>i. i \<in> S \<Longrightarrow> A i \<in> null_sets"
-  shows "(\<Union>i\<in>S. A i) \<in> null_sets"
-proof (intro CollectI conjI)
-  show "(\<Union>i\<in>S. A i) \<in> sets M" using assms by (intro finite_UN) auto
-  then have "0 \<le> \<mu> (\<Union>i\<in>S. A i)" by simp
-  moreover have "\<mu> (\<Union>i\<in>S. A i) \<le> (\<Sum>i\<in>S. \<mu> (A i))"
-    using assms by (intro measure_finitely_subadditive) auto
-  ultimately show "\<mu> (\<Union>i\<in>S. A i) = 0" using assms by auto
-qed
-
 lemma (in measure_space) null_set_Int1:
   assumes "B \<in> null_sets" "A \<in> sets M" shows "A \<inter> B \<in> null_sets"
 using assms proof (intro CollectI conjI)
diff -r 36353d913424 -r b0746bd57a41 src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Tue May 17 12:24:48 2011 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Tue May 17 14:36:54 2011 +0200
@@ -975,7 +975,7 @@
       finally have "Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>} \<in> null_sets" by simp }
     from this[OF borel(1) refl] this[OF borel(2) f]
     have "Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>} \<in> null_sets" "Q0 \<inter> {x\<in>space M. f' x \<noteq> \<infinity>} \<in> null_sets" by simp_all
-    then show "(Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<infinity>}) \<in> null_sets" by (rule null_sets_Un)
+    then show "(Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<infinity>}) \<in> null_sets" by (rule nullsets.Un)
     show "{x \<in> space M. ?f Q0 x \<noteq> ?f' Q0 x} \<subseteq>
       (Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<infinity>})" by (auto simp: indicator_def)
   qed