# HG changeset patch
# User hoelzl
# Date 1335374787 -7200
# Node ID d31085f07f6042948235fef3e9e9f30006edd822
# Parent  dfe747e72fa8739b8a4720aa4bda4caa85e7e717
add Caratheodories theorem for semi-rings of sets

diff -r dfe747e72fa8 -r d31085f07f60 src/HOL/Probability/Caratheodory.thy
--- a/src/HOL/Probability/Caratheodory.thy	Wed Apr 25 19:26:00 2012 +0200
+++ b/src/HOL/Probability/Caratheodory.thy	Wed Apr 25 19:26:27 2012 +0200
@@ -655,7 +655,7 @@
   by (simp add: measure_space_def positive_def countably_additive_def)
      blast
 
-theorem (in ring_of_sets) caratheodory:
+theorem (in ring_of_sets) caratheodory':
   assumes posf: "positive M f" and ca: "countably_additive M f"
   shows "\<exists>\<mu> :: 'a set \<Rightarrow> ereal. (\<forall>s \<in> M. \<mu> s = f s) \<and> measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>"
 proof -
@@ -828,8 +828,327 @@
   assumes f: "positive M f" "additive M f" and fin: "\<And>A. A \<in> M \<Longrightarrow> f A \<noteq> \<infinity>"
   assumes cont: "\<And>A. range A \<subseteq> M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) ----> 0"
   shows "\<exists>\<mu> :: 'a set \<Rightarrow> ereal. (\<forall>s \<in> M. \<mu> s = f s) \<and> measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>"
-proof (intro caratheodory empty_continuous_imp_countably_additive f)
+proof (intro caratheodory' empty_continuous_imp_countably_additive f)
   show "\<forall>A\<in>M. f A \<noteq> \<infinity>" using fin by auto
 qed (rule cont)
 
+section {* Volumes *}
+
+definition volume :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where
+  "volume M f \<longleftrightarrow>
+  (f {} = 0) \<and> (\<forall>a\<in>M. 0 \<le> f a) \<and>
+  (\<forall>C\<subseteq>M. disjoint C \<longrightarrow> finite C \<longrightarrow> \<Union>C \<in> M \<longrightarrow> f (\<Union>C) = (\<Sum>c\<in>C. f c))"
+
+lemma volumeI:
+  assumes "f {} = 0"
+  assumes "\<And>a. a \<in> M \<Longrightarrow> 0 \<le> f a"
+  assumes "\<And>C. C \<subseteq> M \<Longrightarrow> disjoint C \<Longrightarrow> finite C \<Longrightarrow> \<Union>C \<in> M \<Longrightarrow> f (\<Union>C) = (\<Sum>c\<in>C. f c)"
+  shows "volume M f"
+  using assms by (auto simp: volume_def)
+
+lemma volume_positive:
+  "volume M f \<Longrightarrow> a \<in> M \<Longrightarrow> 0 \<le> f a"
+  by (auto simp: volume_def)
+
+lemma volume_empty:
+  "volume M f \<Longrightarrow> f {} = 0"
+  by (auto simp: volume_def)
+
+lemma volume_finite_additive:
+  assumes "volume M f" 
+  assumes A: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M" "disjoint_family_on A I" "finite I" "UNION I A \<in> M"
+  shows "f (UNION I A) = (\<Sum>i\<in>I. f (A i))"
+proof -
+  have "A`I \<subseteq> M" "disjoint (A`I)" "finite (A`I)" "\<Union>A`I \<in> M"
+    using A unfolding SUP_def by (auto simp: disjoint_family_on_disjoint_image)
+  with `volume M f` have "f (\<Union>A`I) = (\<Sum>a\<in>A`I. f a)"
+    unfolding volume_def by blast
+  also have "\<dots> = (\<Sum>i\<in>I. f (A i))"
+  proof (subst setsum_reindex_nonzero)
+    fix i j assume "i \<in> I" "j \<in> I" "i \<noteq> j" "A i = A j"
+    with `disjoint_family_on A I` have "A i = {}"
+      by (auto simp: disjoint_family_on_def)
+    then show "f (A i) = 0"
+      using volume_empty[OF `volume M f`] by simp
+  qed (auto intro: `finite I`)
+  finally show "f (UNION I A) = (\<Sum>i\<in>I. f (A i))"
+    by simp
+qed
+
+lemma (in ring_of_sets) volume_additiveI:
+  assumes pos: "\<And>a. a \<in> M \<Longrightarrow> 0 \<le> \<mu> a" 
+  assumes [simp]: "\<mu> {} = 0"
+  assumes add: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<inter> b = {} \<Longrightarrow> \<mu> (a \<union> b) = \<mu> a + \<mu> b"
+  shows "volume M \<mu>"
+proof (unfold volume_def, safe)
+  fix C assume "finite C" "C \<subseteq> M" "disjoint C"
+  then show "\<mu> (\<Union>C) = setsum \<mu> C"
+  proof (induct C)
+    case (insert c C)
+    from insert(1,2,4,5) have "\<mu> (\<Union>insert c C) = \<mu> c + \<mu> (\<Union>C)"
+      by (auto intro!: add simp: disjoint_def)
+    with insert show ?case
+      by (simp add: disjoint_def)
+  qed simp
+qed fact+
+
+lemma (in semiring_of_sets) extend_volume:
+  assumes "volume M \<mu>"
+  shows "\<exists>\<mu>'. volume generated_ring \<mu>' \<and> (\<forall>a\<in>M. \<mu>' a = \<mu> a)"
+proof -
+  let ?R = generated_ring
+  have "\<forall>a\<in>?R. \<exists>m. \<exists>C\<subseteq>M. a = \<Union>C \<and> finite C \<and> disjoint C \<and> m = (\<Sum>c\<in>C. \<mu> c)"
+    by (auto simp: generated_ring_def)
+  from bchoice[OF this] guess \<mu>' .. note \<mu>'_spec = this
+  
+  { fix C assume C: "C \<subseteq> M" "finite C" "disjoint C"
+    fix D assume D: "D \<subseteq> M" "finite D" "disjoint D"
+    assume "\<Union>C = \<Union>D"
+    have "(\<Sum>d\<in>D. \<mu> d) = (\<Sum>d\<in>D. \<Sum>c\<in>C. \<mu> (c \<inter> d))"
+    proof (intro setsum_cong refl)
+      fix d assume "d \<in> D"
+      have Un_eq_d: "(\<Union>c\<in>C. c \<inter> d) = d"
+        using `d \<in> D` `\<Union>C = \<Union>D` by auto
+      moreover have "\<mu> (\<Union>c\<in>C. c \<inter> d) = (\<Sum>c\<in>C. \<mu> (c \<inter> d))"
+      proof (rule volume_finite_additive)
+        { fix c assume "c \<in> C" then show "c \<inter> d \<in> M"
+            using C D `d \<in> D` by auto }
+        show "(\<Union>a\<in>C. a \<inter> d) \<in> M"
+          unfolding Un_eq_d using `d \<in> D` D by auto
+        show "disjoint_family_on (\<lambda>a. a \<inter> d) C"
+          using `disjoint C` by (auto simp: disjoint_family_on_def disjoint_def)
+      qed fact+
+      ultimately show "\<mu> d = (\<Sum>c\<in>C. \<mu> (c \<inter> d))" by simp
+    qed }
+  note split_sum = this
+
+  { fix C assume C: "C \<subseteq> M" "finite C" "disjoint C"
+    fix D assume D: "D \<subseteq> M" "finite D" "disjoint D"
+    assume "\<Union>C = \<Union>D"
+    with split_sum[OF C D] split_sum[OF D C]
+    have "(\<Sum>d\<in>D. \<mu> d) = (\<Sum>c\<in>C. \<mu> c)"
+      by (simp, subst setsum_commute, simp add: ac_simps) }
+  note sum_eq = this
+
+  { fix C assume C: "C \<subseteq> M" "finite C" "disjoint C"
+    then have "\<Union>C \<in> ?R" by (auto simp: generated_ring_def)
+    with \<mu>'_spec[THEN bspec, of "\<Union>C"]
+    obtain D where
+      D: "D \<subseteq> M" "finite D" "disjoint D" "\<Union>C = \<Union>D" and "\<mu>' (\<Union>C) = (\<Sum>d\<in>D. \<mu> d)"
+      by blast
+    with sum_eq[OF C D] have "\<mu>' (\<Union>C) = (\<Sum>c\<in>C. \<mu> c)" by simp }
+  note \<mu>' = this
+
+  show ?thesis
+  proof (intro exI conjI ring_of_sets.volume_additiveI[OF generating_ring] ballI)
+    fix a assume "a \<in> M" with \<mu>'[of "{a}"] show "\<mu>' a = \<mu> a"
+      by (simp add: disjoint_def)
+  next
+    fix a assume "a \<in> ?R" then guess Ca .. note Ca = this
+    with \<mu>'[of Ca] `volume M \<mu>`[THEN volume_positive]
+    show "0 \<le> \<mu>' a"
+      by (auto intro!: setsum_nonneg)
+  next
+    show "\<mu>' {} = 0" using \<mu>'[of "{}"] by auto
+  next
+    fix a assume "a \<in> ?R" then guess Ca .. note Ca = this
+    fix b assume "b \<in> ?R" then guess Cb .. note Cb = this
+    assume "a \<inter> b = {}"
+    with Ca Cb have "Ca \<inter> Cb \<subseteq> {{}}" by auto
+    then have C_Int_cases: "Ca \<inter> Cb = {{}} \<or> Ca \<inter> Cb = {}" by auto
+
+    from `a \<inter> b = {}` have "\<mu>' (\<Union> (Ca \<union> Cb)) = (\<Sum>c\<in>Ca \<union> Cb. \<mu> c)"
+      using Ca Cb by (intro \<mu>') (auto intro!: disjoint_union)
+    also have "\<dots> = (\<Sum>c\<in>Ca \<union> Cb. \<mu> c) + (\<Sum>c\<in>Ca \<inter> Cb. \<mu> c)"
+      using C_Int_cases volume_empty[OF `volume M \<mu>`] by (elim disjE) simp_all
+    also have "\<dots> = (\<Sum>c\<in>Ca. \<mu> c) + (\<Sum>c\<in>Cb. \<mu> c)"
+      using Ca Cb by (simp add: setsum_Un_Int)
+    also have "\<dots> = \<mu>' a + \<mu>' b"
+      using Ca Cb by (simp add: \<mu>')
+    finally show "\<mu>' (a \<union> b) = \<mu>' a + \<mu>' b"
+      using Ca Cb by simp
+  qed
+qed
+
+section {* Caratheodory on semirings *}
+
+theorem (in semiring_of_sets) caratheodory:
+  assumes pos: "positive M \<mu>" and ca: "countably_additive M \<mu>"
+  shows "\<exists>\<mu>' :: 'a set \<Rightarrow> ereal. (\<forall>s \<in> M. \<mu>' s = \<mu> s) \<and> measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>'"
+proof -
+  have "volume M \<mu>"
+  proof (rule volumeI)
+    { fix a assume "a \<in> M" then show "0 \<le> \<mu> a"
+        using pos unfolding positive_def by auto }
+    note p = this
+
+    fix C assume sets_C: "C \<subseteq> M" "\<Union>C \<in> M" and "disjoint C" "finite C"
+    have "\<exists>F'. bij_betw F' {..<card C} C"
+      by (rule finite_same_card_bij[OF _ `finite C`]) auto
+    then guess F' .. note F' = this
+    then have F': "C = F' ` {..< card C}" "inj_on F' {..< card C}"
+      by (auto simp: bij_betw_def)
+    { fix i j assume *: "i < card C" "j < card C" "i \<noteq> j"
+      with F' have "F' i \<in> C" "F' j \<in> C" "F' i \<noteq> F' j"
+        unfolding inj_on_def by auto
+      with `disjoint C`[THEN disjointD]
+      have "F' i \<inter> F' j = {}"
+        by auto }
+    note F'_disj = this
+    def F \<equiv> "\<lambda>i. if i < card C then F' i else {}"
+    then have "disjoint_family F"
+      using F'_disj by (auto simp: disjoint_family_on_def)
+    moreover from F' have "(\<Union>i. F i) = \<Union>C"
+      by (auto simp: F_def set_eq_iff split: split_if_asm)
+    moreover have sets_F: "\<And>i. F i \<in> M"
+      using F' sets_C by (auto simp: F_def)
+    moreover note sets_C
+    ultimately have "\<mu> (\<Union>C) = (\<Sum>i. \<mu> (F i))"
+      using ca[unfolded countably_additive_def, THEN spec, of F] by auto
+    also have "\<dots> = (\<Sum>i<card C. \<mu> (F' i))"
+    proof -
+      have "(\<lambda>i. if i \<in> {..< card C} then \<mu> (F' i) else 0) sums (\<Sum>i<card C. \<mu> (F' i))"
+        by (rule sums_If_finite_set) auto
+      also have "(\<lambda>i. if i \<in> {..< card C} then \<mu> (F' i) else 0) = (\<lambda>i. \<mu> (F i))"
+        using pos by (auto simp: positive_def F_def)
+      finally show "(\<Sum>i. \<mu> (F i)) = (\<Sum>i<card C. \<mu> (F' i))"
+        by (simp add: sums_iff)
+    qed
+    also have "\<dots> = (\<Sum>c\<in>C. \<mu> c)"
+      using F'(2) by (subst (2) F') (simp add: setsum_reindex)
+    finally show "\<mu> (\<Union>C) = (\<Sum>c\<in>C. \<mu> c)" .
+  next
+    show "\<mu> {} = 0"
+      using `positive M \<mu>` by (rule positiveD1)
+  qed
+  from extend_volume[OF this] obtain \<mu>_r where
+    V: "volume generated_ring \<mu>_r" "\<And>a. a \<in> M \<Longrightarrow> \<mu> a = \<mu>_r a"
+    by auto
+
+  interpret G: ring_of_sets \<Omega> generated_ring
+    by (rule generating_ring)
+
+  have pos: "positive generated_ring \<mu>_r"
+    using V unfolding positive_def by (auto simp: positive_def intro!: volume_positive volume_empty)
+
+  have "countably_additive generated_ring \<mu>_r"
+  proof (rule countably_additiveI)
+    fix A' :: "nat \<Rightarrow> 'a set" assume A': "range A' \<subseteq> generated_ring" "disjoint_family A'"
+      and Un_A: "(\<Union>i. A' i) \<in> generated_ring"
+
+    from generated_ringE[OF Un_A] guess C' . note C' = this
+
+    { fix c assume "c \<in> C'"
+      moreover def A \<equiv> "\<lambda>i. A' i \<inter> c"
+      ultimately have A: "range A \<subseteq> generated_ring" "disjoint_family A"
+        and Un_A: "(\<Union>i. A i) \<in> generated_ring"
+        using A' C'
+        by (auto intro!: G.Int G.finite_Union intro: generated_ringI_Basic simp: disjoint_family_on_def)
+      from A C' `c \<in> C'` have UN_eq: "(\<Union>i. A i) = c"
+        by (auto simp: A_def)
+
+      have "\<forall>i::nat. \<exists>f::nat \<Rightarrow> 'a set. \<mu>_r (A i) = (\<Sum>j. \<mu>_r (f j)) \<and> disjoint_family f \<and> \<Union>range f = A i \<and> (\<forall>j. f j \<in> M)"
+        (is "\<forall>i. ?P i")
+      proof
+        fix i
+        from A have Ai: "A i \<in> generated_ring" by auto
+        from generated_ringE[OF this] guess C . note C = this
+
+        have "\<exists>F'. bij_betw F' {..<card C} C"
+          by (rule finite_same_card_bij[OF _ `finite C`]) auto
+        then guess F .. note F = this
+        def f \<equiv> "\<lambda>i. if i < card C then F i else {}"
+        then have f: "bij_betw f {..< card C} C"
+          by (intro bij_betw_cong[THEN iffD1, OF _ F]) auto
+        with C have "\<forall>j. f j \<in> M"
+          by (auto simp: Pi_iff f_def dest!: bij_betw_imp_funcset)
+        moreover
+        from f C have d_f: "disjoint_family_on f {..<card C}"
+          by (intro disjoint_image_disjoint_family_on) (auto simp: bij_betw_def)
+        then have "disjoint_family f"
+          by (auto simp: disjoint_family_on_def f_def)
+        moreover
+        have Ai_eq: "A i = (\<Union> x<card C. f x)"
+          using f C Ai unfolding bij_betw_def by (simp add: Union_image_eq[symmetric])
+        then have "\<Union>range f = A i"
+          using f C Ai unfolding bij_betw_def by (auto simp: f_def)
+        moreover 
+        { have "(\<Sum>j. \<mu>_r (f j)) = (\<Sum>j. if j \<in> {..< card C} then \<mu>_r (f j) else 0)"
+            using volume_empty[OF V(1)] by (auto intro!: arg_cong[where f=suminf] simp: f_def)
+          also have "\<dots> = (\<Sum>j<card C. \<mu>_r (f j))"
+            by (rule sums_If_finite_set[THEN sums_unique, symmetric]) simp
+          also have "\<dots> = \<mu>_r (A i)"
+            using C f[THEN bij_betw_imp_funcset] unfolding Ai_eq
+            by (intro volume_finite_additive[OF V(1) _ d_f, symmetric])
+               (auto simp: Pi_iff Ai_eq intro: generated_ringI_Basic)
+          finally have "\<mu>_r (A i) = (\<Sum>j. \<mu>_r (f j))" .. }
+        ultimately show "?P i"
+          by blast
+      qed
+      from choice[OF this] guess f .. note f = this
+      then have UN_f_eq: "(\<Union>i. split f (prod_decode i)) = (\<Union>i. A i)"
+        unfolding UN_extend_simps surj_prod_decode by (auto simp: set_eq_iff)
+
+      have d: "disjoint_family (\<lambda>i. split f (prod_decode i))"
+        unfolding disjoint_family_on_def
+      proof (intro ballI impI)
+        fix m n :: nat assume "m \<noteq> n"
+        then have neq: "prod_decode m \<noteq> prod_decode n"
+          using inj_prod_decode[of UNIV] by (auto simp: inj_on_def)
+        show "split f (prod_decode m) \<inter> split f (prod_decode n) = {}"
+        proof cases
+          assume "fst (prod_decode m) = fst (prod_decode n)"
+          then show ?thesis
+            using neq f by (fastforce simp: disjoint_family_on_def)
+        next
+          assume neq: "fst (prod_decode m) \<noteq> fst (prod_decode n)"
+          have "split f (prod_decode m) \<subseteq> A (fst (prod_decode m))"
+            "split f (prod_decode n) \<subseteq> A (fst (prod_decode n))"
+            using f[THEN spec, of "fst (prod_decode m)"]
+            using f[THEN spec, of "fst (prod_decode n)"]
+            by (auto simp: set_eq_iff)
+          with f A neq show ?thesis
+            by (fastforce simp: disjoint_family_on_def subset_eq set_eq_iff)
+        qed
+      qed
+      from f have "(\<Sum>n. \<mu>_r (A n)) = (\<Sum>n. \<mu>_r (split f (prod_decode n)))"
+        by (intro suminf_ereal_2dimen[symmetric] positiveD2[OF pos] generated_ringI_Basic)
+         (auto split: prod.split)
+      also have "\<dots> = (\<Sum>n. \<mu> (split f (prod_decode n)))"
+        using f V(2) by (auto intro!: arg_cong[where f=suminf] split: prod.split)
+      also have "\<dots> = \<mu> (\<Union>i. split f (prod_decode i))"
+        using f `c \<in> C'` C'
+        by (intro ca[unfolded countably_additive_def, rule_format])
+           (auto split: prod.split simp: UN_f_eq d UN_eq)
+      finally have "(\<Sum>n. \<mu>_r (A' n \<inter> c)) = \<mu> c"
+        using UN_f_eq UN_eq by (simp add: A_def) }
+    note eq = this
+
+    have "(\<Sum>n. \<mu>_r (A' n)) = (\<Sum>n. \<Sum>c\<in>C'. \<mu>_r (A' n \<inter> c))"
+      using C' A' find_theorems "\<Union> _ ` _"
+      by (subst volume_finite_additive[symmetric, OF V(1)])
+         (auto simp: disjoint_def disjoint_family_on_def Union_image_eq[symmetric] simp del: Union_image_eq
+               intro!: G.Int G.finite_Union arg_cong[where f="\<lambda>X. suminf (\<lambda>i. \<mu>_r (X i))"] ext
+               intro: generated_ringI_Basic)
+    also have "\<dots> = (\<Sum>c\<in>C'. \<Sum>n. \<mu>_r (A' n \<inter> c))"
+      using C' A'
+      by (intro suminf_setsum_ereal positiveD2[OF pos] G.Int G.finite_Union)
+         (auto intro: generated_ringI_Basic)
+    also have "\<dots> = (\<Sum>c\<in>C'. \<mu>_r c)"
+      using eq V C' by (auto intro!: setsum_cong)
+    also have "\<dots> = \<mu>_r (\<Union>C')"
+      using C' Un_A
+      by (subst volume_finite_additive[symmetric, OF V(1)])
+         (auto simp: disjoint_family_on_def disjoint_def Union_image_eq[symmetric] simp del: Union_image_eq 
+               intro: generated_ringI_Basic)
+    finally show "(\<Sum>n. \<mu>_r (A' n)) = \<mu>_r (\<Union>i. A' i)"
+      using C' by simp
+  qed
+  from G.caratheodory'[OF `positive generated_ring \<mu>_r` `countably_additive generated_ring \<mu>_r`]
+  guess \<mu>' ..
+  with V show ?thesis
+    unfolding sigma_sets_generated_ring_eq
+    by (intro exI[of _ \<mu>']) (auto intro: generated_ringI_Basic)
+qed
+
 end
diff -r dfe747e72fa8 -r d31085f07f60 src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Apr 25 19:26:00 2012 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Apr 25 19:26:27 2012 +0200
@@ -8,21 +8,6 @@
   imports Probability_Measure Caratheodory
 begin
 
-lemma sigma_sets_mono: assumes "A \<subseteq> sigma_sets X 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> sigma_sets X B`, auto intro: sigma_sets.intros)
-qed
-
-lemma sigma_sets_mono': 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 sigma_sets_superset_generator: "A \<subseteq> sigma_sets X A"
-  by (auto intro: sigma_sets.Basic)
-
 lemma (in product_sigma_finite)
   assumes IJ: "I \<inter> J = {}" "finite I" "finite J" and A: "A \<in> sets (Pi\<^isub>M (I \<union> J) M)"
   shows emeasure_fold_integral:
@@ -187,7 +172,8 @@
 
 lemma (in product_prob_space) algebra_generator:
   assumes "I \<noteq> {}" shows "algebra (\<Pi>\<^isub>E i\<in>I. space (M i)) generator" (is "algebra ?\<Omega> ?G")
-proof
+  unfolding algebra_def algebra_axioms_def ring_of_sets_iff
+proof (intro conjI ballI)
   let ?G = generator
   show "?G \<subseteq> Pow ?\<Omega>"
     by (auto simp: generator_def prod_emb_def)
diff -r dfe747e72fa8 -r d31085f07f60 src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Wed Apr 25 19:26:00 2012 +0200
+++ b/src/HOL/Probability/Measure_Space.thy	Wed Apr 25 19:26:27 2012 +0200
@@ -636,7 +636,7 @@
   unfolding null_sets_def by simp
 
 interpretation null_sets: ring_of_sets "space M" "null_sets M" for M
-proof
+proof (rule ring_of_setsI)
   show "null_sets M \<subseteq> Pow (space M)"
     using sets_into_space by auto
   show "{} \<in> null_sets M"
diff -r dfe747e72fa8 -r d31085f07f60 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Apr 25 19:26:00 2012 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Apr 25 19:26:27 2012 +0200
@@ -24,7 +24,7 @@
   subsets of the universe. A sigma algebra is such a set that has
   three very natural and desirable properties. *}
 
-subsection {* Algebras *}
+subsection {* Families of sets *}
 
 locale subset_class =
   fixes \<Omega> :: "'a set" and M :: "'a set set"
@@ -33,20 +33,85 @@
 lemma (in subset_class) sets_into_space: "x \<in> M \<Longrightarrow> x \<subseteq> \<Omega>"
   by (metis PowD contra_subsetD space_closed)
 
-locale ring_of_sets = subset_class +
-  assumes empty_sets [iff]: "{} \<in> M"
-     and  Diff [intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a - b \<in> M"
-     and  Un [intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<union> b \<in> M"
+subsection {* Semiring of sets *}
+
+subsubsection {* Disjoint sets *}
+
+definition "disjoint A \<longleftrightarrow> (\<forall>a\<in>A. \<forall>b\<in>A. a \<noteq> b \<longrightarrow> a \<inter> b = {})"
+
+lemma disjointI:
+  "(\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}) \<Longrightarrow> disjoint A"
+  unfolding disjoint_def by auto
+
+lemma disjointD:
+  "disjoint A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}"
+  unfolding disjoint_def by auto
+
+lemma disjoint_empty[iff]: "disjoint {}"
+  by (auto simp: disjoint_def)
 
-lemma (in ring_of_sets) Int [intro]:
-  assumes a: "a \<in> M" and b: "b \<in> M" shows "a \<inter> b \<in> M"
+lemma disjoint_union: 
+  assumes C: "disjoint C" and B: "disjoint B" and disj: "\<Union>C \<inter> \<Union>B = {}"
+  shows "disjoint (C \<union> B)"
+proof (rule disjointI)
+  fix c d assume sets: "c \<in> C \<union> B" "d \<in> C \<union> B" and "c \<noteq> d"
+  show "c \<inter> d = {}"
+  proof cases
+    assume "(c \<in> C \<and> d \<in> C) \<or> (c \<in> B \<and> d \<in> B)"
+    then show ?thesis
+    proof 
+      assume "c \<in> C \<and> d \<in> C" with `c \<noteq> d` C show "c \<inter> d = {}"
+        by (auto simp: disjoint_def)
+    next
+      assume "c \<in> B \<and> d \<in> B" with `c \<noteq> d` B show "c \<inter> d = {}"
+        by (auto simp: disjoint_def)
+    qed
+  next
+    assume "\<not> ((c \<in> C \<and> d \<in> C) \<or> (c \<in> B \<and> d \<in> B))"
+    with sets have "(c \<subseteq> \<Union>C \<and> d \<subseteq> \<Union>B) \<or> (c \<subseteq> \<Union>B \<and> d \<subseteq> \<Union>C)"
+      by auto
+    with disj show "c \<inter> d = {}" by auto
+  qed
+qed
+
+locale semiring_of_sets = subset_class +
+  assumes empty_sets[iff]: "{} \<in> M"
+  assumes Int[intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<inter> b \<in> M"
+  assumes Diff_cover:
+    "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> \<exists>C\<subseteq>M. finite C \<and> disjoint C \<and> a - b = \<Union>C"
+
+lemma (in semiring_of_sets) finite_INT[intro]:
+  assumes "finite I" "I \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M"
+  shows "(\<Inter>i\<in>I. A i) \<in> M"
+  using assms by (induct rule: finite_ne_induct) auto
+
+lemma (in semiring_of_sets) Int_space_eq1 [simp]: "x \<in> M \<Longrightarrow> \<Omega> \<inter> x = x"
+  by (metis Int_absorb1 sets_into_space)
+
+lemma (in semiring_of_sets) Int_space_eq2 [simp]: "x \<in> M \<Longrightarrow> x \<inter> \<Omega> = x"
+  by (metis Int_absorb2 sets_into_space)
+
+lemma (in semiring_of_sets) sets_Collect_conj:
+  assumes "{x\<in>\<Omega>. P x} \<in> M" "{x\<in>\<Omega>. Q x} \<in> M"
+  shows "{x\<in>\<Omega>. Q x \<and> P x} \<in> M"
 proof -
-  have "a \<inter> b = a - (a - b)"
+  have "{x\<in>\<Omega>. Q x \<and> P x} = {x\<in>\<Omega>. Q x} \<inter> {x\<in>\<Omega>. P x}"
     by auto
-  then show "a \<inter> b \<in> M"
-    using a b by auto
+  with assms show ?thesis by auto
 qed
 
+lemma (in semiring_of_sets) sets_Collect_finite_All:
+  assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S" "S \<noteq> {}"
+  shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M"
+proof -
+  have "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} = (\<Inter>i\<in>S. {x\<in>\<Omega>. P i x})"
+    using `S \<noteq> {}` by auto
+  with assms show ?thesis by auto
+qed
+
+locale ring_of_sets = semiring_of_sets +
+  assumes Un [intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<union> b \<in> M"
+
 lemma (in ring_of_sets) finite_Union [intro]:
   "finite X \<Longrightarrow> X \<subseteq> M \<Longrightarrow> Union X \<in> M"
   by (induct set: finite) (auto simp add: Un)
@@ -56,10 +121,32 @@
   shows "(\<Union>i\<in>I. A i) \<in> M"
   using assms by induct auto
 
-lemma (in ring_of_sets) finite_INT[intro]:
-  assumes "finite I" "I \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M"
-  shows "(\<Inter>i\<in>I. A i) \<in> M"
-  using assms by (induct rule: finite_ne_induct) auto
+lemma (in ring_of_sets) Diff [intro]:
+  assumes "a \<in> M" "b \<in> M" shows "a - b \<in> M"
+  using Diff_cover[OF assms] by auto
+
+lemma ring_of_setsI:
+  assumes space_closed: "M \<subseteq> Pow \<Omega>"
+  assumes empty_sets[iff]: "{} \<in> M"
+  assumes Un[intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<union> b \<in> M"
+  assumes Diff[intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a - b \<in> M"
+  shows "ring_of_sets \<Omega> M"
+proof
+  fix a b assume ab: "a \<in> M" "b \<in> M"
+  from ab show "\<exists>C\<subseteq>M. finite C \<and> disjoint C \<and> a - b = \<Union>C"
+    by (intro exI[of _ "{a - b}"]) (auto simp: disjoint_def)
+  have "a \<inter> b = a - (a - b)" by auto
+  also have "\<dots> \<in> M" using ab by auto
+  finally show "a \<inter> b \<in> M" .
+qed fact+
+
+lemma ring_of_sets_iff: "ring_of_sets \<Omega> M \<longleftrightarrow> M \<subseteq> Pow \<Omega> \<and> {} \<in> M \<and> (\<forall>a\<in>M. \<forall>b\<in>M. a \<union> b \<in> M) \<and> (\<forall>a\<in>M. \<forall>b\<in>M. a - b \<in> M)"
+proof
+  assume "ring_of_sets \<Omega> M"
+  then interpret ring_of_sets \<Omega> M .
+  show "M \<subseteq> Pow \<Omega> \<and> {} \<in> M \<and> (\<forall>a\<in>M. \<forall>b\<in>M. a \<union> b \<in> M) \<and> (\<forall>a\<in>M. \<forall>b\<in>M. a - b \<in> M)"
+    using space_closed by auto
+qed (auto intro!: ring_of_setsI)
 
 lemma (in ring_of_sets) insert_in_sets:
   assumes "{x} \<in> M" "A \<in> M" shows "insert x A \<in> M"
@@ -68,21 +155,6 @@
   thus ?thesis by auto
 qed
 
-lemma (in ring_of_sets) Int_space_eq1 [simp]: "x \<in> M \<Longrightarrow> \<Omega> \<inter> x = x"
-  by (metis Int_absorb1 sets_into_space)
-
-lemma (in ring_of_sets) Int_space_eq2 [simp]: "x \<in> M \<Longrightarrow> x \<inter> \<Omega> = x"
-  by (metis Int_absorb2 sets_into_space)
-
-lemma (in ring_of_sets) sets_Collect_conj:
-  assumes "{x\<in>\<Omega>. P x} \<in> M" "{x\<in>\<Omega>. Q x} \<in> M"
-  shows "{x\<in>\<Omega>. Q x \<and> P x} \<in> M"
-proof -
-  have "{x\<in>\<Omega>. Q x \<and> P x} = {x\<in>\<Omega>. Q x} \<inter> {x\<in>\<Omega>. P x}"
-    by auto
-  with assms show ?thesis by auto
-qed
-
 lemma (in ring_of_sets) sets_Collect_disj:
   assumes "{x\<in>\<Omega>. P x} \<in> M" "{x\<in>\<Omega>. Q x} \<in> M"
   shows "{x\<in>\<Omega>. Q x \<or> P x} \<in> M"
@@ -92,15 +164,6 @@
   with assms show ?thesis by auto
 qed
 
-lemma (in ring_of_sets) sets_Collect_finite_All:
-  assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S" "S \<noteq> {}"
-  shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M"
-proof -
-  have "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} = (\<Inter>i\<in>S. {x\<in>\<Omega>. P i x})"
-    using `S \<noteq> {}` by auto
-  with assms show ?thesis by auto
-qed
-
 lemma (in ring_of_sets) sets_Collect_finite_Ex:
   assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S"
   shows "{x\<in>\<Omega>. \<exists>i\<in>S. P i x} \<in> M"
@@ -129,9 +192,10 @@
   show ?Un using sets_into_space by auto
 next
   assume ?Un
-  show "algebra \<Omega> M"
-  proof
-    show \<Omega>: "M \<subseteq> Pow \<Omega>" "{} \<in> M" "\<Omega> \<in> M"
+  then have "\<Omega> \<in> M" by auto
+  interpret ring_of_sets \<Omega> M
+  proof (rule ring_of_setsI)
+    show \<Omega>: "M \<subseteq> Pow \<Omega>" "{} \<in> M"
       using `?Un` by auto
     fix a b assume a: "a \<in> M" and b: "b \<in> M"
     then show "a \<union> b \<in> M" using `?Un` by auto
@@ -140,6 +204,7 @@
     then show "a - b \<in> M"
       using a b  `?Un` by auto
   qed
+  show "algebra \<Omega> M" proof qed fact
 qed
 
 lemma algebra_iff_Int:
@@ -184,9 +249,8 @@
   by (cases P) auto
 
 lemma algebra_single_set:
-  assumes "X \<subseteq> S"
-  shows "algebra S { {}, X, S - X, S }"
-  by default (insert `X \<subseteq> S`, auto)
+  "X \<subseteq> S \<Longrightarrow> algebra S { {}, X, S - X, S }"
+  by (auto simp: algebra_iff_Int)
 
 section {* Restricted algebras *}
 
@@ -195,7 +259,7 @@
 
 lemma (in algebra) restricted_algebra:
   assumes "A \<in> M" shows "algebra A (restricted_space A)"
-  using assms by unfold_locales auto
+  using assms by (auto simp: algebra_iff_Int)
 
 subsection {* Sigma Algebras *}
 
@@ -261,19 +325,19 @@
 qed
 
 lemma ring_of_sets_Pow: "ring_of_sets sp (Pow sp)"
-  by default auto
+  by (auto simp: ring_of_sets_iff)
 
 lemma algebra_Pow: "algebra sp (Pow sp)"
-  by default auto
-
-lemma sigma_algebra_Pow: "sigma_algebra sp (Pow sp)"
-  by default auto
+  by (auto simp: algebra_iff_Un)
 
 lemma sigma_algebra_iff:
   "sigma_algebra \<Omega> M \<longleftrightarrow>
     algebra \<Omega> M \<and> (\<forall>A. range A \<subseteq> M \<longrightarrow> (\<Union>i::nat. A i) \<in> M)"
   by (simp add: sigma_algebra_def sigma_algebra_axioms_def)
 
+lemma sigma_algebra_Pow: "sigma_algebra sp (Pow sp)"
+  by (auto simp: sigma_algebra_iff algebra_iff_Int)
+
 lemma (in sigma_algebra) sets_Collect_countable_All:
   assumes "\<And>i. {x\<in>\<Omega>. P i x} \<in> M"
   shows "{x\<in>\<Omega>. \<forall>i::'i::countable. P i x} \<in> M"
@@ -452,6 +516,21 @@
     by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros(2-))
 qed
 
+lemma sigma_sets_mono: assumes "A \<subseteq> sigma_sets X 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> sigma_sets X B`, auto intro: sigma_sets.intros(2-))
+qed
+
+lemma sigma_sets_mono': 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(2-))
+qed
+
+lemma sigma_sets_superset_generator: "A \<subseteq> sigma_sets X A"
+  by (auto intro: sigma_sets.Basic)
+
 lemma (in sigma_algebra) restriction_in_sets:
   fixes A :: "nat \<Rightarrow> 'a set"
   assumes "S \<in> M"
@@ -762,6 +841,150 @@
   thus "(\<Union>i::nat. A i) \<in> M" by (simp add: UN_disjointed_eq)
 qed
 
+lemma disjoint_family_on_disjoint_image:
+  "disjoint_family_on A I \<Longrightarrow> disjoint (A ` I)"
+  unfolding disjoint_family_on_def disjoint_def by force
+
+lemma disjoint_image_disjoint_family_on:
+  assumes d: "disjoint (A ` I)" and i: "inj_on A I"
+  shows "disjoint_family_on A I"
+  unfolding disjoint_family_on_def
+proof (intro ballI impI)
+  fix n m assume nm: "m \<in> I" "n \<in> I" and "n \<noteq> m"
+  with i[THEN inj_onD, of n m] show "A n \<inter> A m = {}"
+    by (intro disjointD[OF d]) auto
+qed
+
+section {* Ring generated by a semiring *}
+
+definition (in semiring_of_sets)
+  "generated_ring = { \<Union>C | C. C \<subseteq> M \<and> finite C \<and> disjoint C }"
+
+lemma (in semiring_of_sets) generated_ringE[elim?]:
+  assumes "a \<in> generated_ring"
+  obtains C where "finite C" "disjoint C" "C \<subseteq> M" "a = \<Union>C"
+  using assms unfolding generated_ring_def by auto
+
+lemma (in semiring_of_sets) generated_ringI[intro?]:
+  assumes "finite C" "disjoint C" "C \<subseteq> M" "a = \<Union>C"
+  shows "a \<in> generated_ring"
+  using assms unfolding generated_ring_def by auto
+
+lemma (in semiring_of_sets) generated_ringI_Basic:
+  "A \<in> M \<Longrightarrow> A \<in> generated_ring"
+  by (rule generated_ringI[of "{A}"]) (auto simp: disjoint_def)
+
+lemma (in semiring_of_sets) generated_ring_disjoint_Un[intro]:
+  assumes a: "a \<in> generated_ring" and b: "b \<in> generated_ring"
+  and "a \<inter> b = {}"
+  shows "a \<union> b \<in> generated_ring"
+proof -
+  from a guess Ca .. note Ca = this
+  from b guess Cb .. note Cb = this
+  show ?thesis
+  proof
+    show "disjoint (Ca \<union> Cb)"
+      using `a \<inter> b = {}` Ca Cb by (auto intro!: disjoint_union)
+  qed (insert Ca Cb, auto)
+qed
+
+lemma (in semiring_of_sets) generated_ring_empty: "{} \<in> generated_ring"
+  by (auto simp: generated_ring_def disjoint_def)
+
+lemma (in semiring_of_sets) generated_ring_disjoint_Union:
+  assumes "finite A" shows "A \<subseteq> generated_ring \<Longrightarrow> disjoint A \<Longrightarrow> \<Union>A \<in> generated_ring"
+  using assms by (induct A) (auto simp: disjoint_def intro!: generated_ring_disjoint_Un generated_ring_empty)
+
+lemma (in semiring_of_sets) generated_ring_disjoint_UNION:
+  "finite I \<Longrightarrow> disjoint (A ` I) \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> A i \<in> generated_ring) \<Longrightarrow> UNION I A \<in> generated_ring"
+  unfolding SUP_def by (intro generated_ring_disjoint_Union) auto
+
+lemma (in semiring_of_sets) generated_ring_Int:
+  assumes a: "a \<in> generated_ring" and b: "b \<in> generated_ring"
+  shows "a \<inter> b \<in> generated_ring"
+proof -
+  from a guess Ca .. note Ca = this
+  from b guess Cb .. note Cb = this
+  def C \<equiv> "(\<lambda>(a,b). a \<inter> b)` (Ca\<times>Cb)"
+  show ?thesis
+  proof
+    show "disjoint C"
+    proof (simp add: disjoint_def C_def, intro ballI impI)
+      fix a1 b1 a2 b2 assume sets: "a1 \<in> Ca" "b1 \<in> Cb" "a2 \<in> Ca" "b2 \<in> Cb"
+      assume "a1 \<inter> b1 \<noteq> a2 \<inter> b2"
+      then have "a1 \<noteq> a2 \<or> b1 \<noteq> b2" by auto
+      then show "(a1 \<inter> b1) \<inter> (a2 \<inter> b2) = {}"
+      proof
+        assume "a1 \<noteq> a2"
+        with sets Ca have "a1 \<inter> a2 = {}"
+          by (auto simp: disjoint_def)
+        then show ?thesis by auto
+      next
+        assume "b1 \<noteq> b2"
+        with sets Cb have "b1 \<inter> b2 = {}"
+          by (auto simp: disjoint_def)
+        then show ?thesis by auto
+      qed
+    qed
+  qed (insert Ca Cb, auto simp: C_def)
+qed
+
+lemma (in semiring_of_sets) generated_ring_Inter:
+  assumes "finite A" "A \<noteq> {}" shows "A \<subseteq> generated_ring \<Longrightarrow> \<Inter>A \<in> generated_ring"
+  using assms by (induct A rule: finite_ne_induct) (auto intro: generated_ring_Int)
+
+lemma (in semiring_of_sets) generated_ring_INTER:
+  "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> A i \<in> generated_ring) \<Longrightarrow> INTER I A \<in> generated_ring"
+  unfolding INF_def by (intro generated_ring_Inter) auto
+
+lemma (in semiring_of_sets) generating_ring:
+  "ring_of_sets \<Omega> generated_ring"
+proof (rule ring_of_setsI)
+  let ?R = generated_ring
+  show "?R \<subseteq> Pow \<Omega>"
+    using sets_into_space by (auto simp: generated_ring_def generated_ring_empty)
+  show "{} \<in> ?R" by (rule generated_ring_empty)
+
+  { fix a assume a: "a \<in> ?R" then guess Ca .. note Ca = this
+    fix b assume b: "b \<in> ?R" then guess Cb .. note Cb = this
+  
+    show "a - b \<in> ?R"
+    proof cases
+      assume "Cb = {}" with Cb `a \<in> ?R` show ?thesis
+        by simp
+    next
+      assume "Cb \<noteq> {}"
+      with Ca Cb have "a - b = (\<Union>a'\<in>Ca. \<Inter>b'\<in>Cb. a' - b')" by auto
+      also have "\<dots> \<in> ?R"
+      proof (intro generated_ring_INTER generated_ring_disjoint_UNION)
+        fix a b assume "a \<in> Ca" "b \<in> Cb"
+        with Ca Cb Diff_cover[of a b] show "a - b \<in> ?R"
+          by (auto simp add: generated_ring_def)
+      next
+        show "disjoint ((\<lambda>a'. \<Inter>b'\<in>Cb. a' - b')`Ca)"
+          using Ca by (auto simp add: disjoint_def `Cb \<noteq> {}`)
+      next
+        show "finite Ca" "finite Cb" "Cb \<noteq> {}" by fact+
+      qed
+      finally show "a - b \<in> ?R" .
+    qed }
+  note Diff = this
+
+  fix a b assume sets: "a \<in> ?R" "b \<in> ?R"
+  have "a \<union> b = (a - b) \<union> (a \<inter> b) \<union> (b - a)" by auto
+  also have "\<dots> \<in> ?R"
+    by (intro sets generated_ring_disjoint_Un generated_ring_Int Diff) auto
+  finally show "a \<union> b \<in> ?R" .
+qed
+
+lemma (in semiring_of_sets) sigma_sets_generated_ring_eq: "sigma_sets \<Omega> generated_ring = sigma_sets \<Omega> M"
+proof
+  interpret M: sigma_algebra \<Omega> "sigma_sets \<Omega> M"
+    using space_closed by (rule sigma_algebra_sigma_sets)
+  show "sigma_sets \<Omega> generated_ring \<subseteq> sigma_sets \<Omega> M"
+    by (blast intro!: sigma_sets_mono elim: generated_ringE)
+qed (auto intro!: generated_ringI_Basic sigma_sets_mono)
+
 section {* Measure type *}
 
 definition positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where
@@ -777,7 +1000,7 @@
 typedef (open) 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
 proof
   have "sigma_algebra UNIV {{}, UNIV}"
-    proof qed auto
+    by (auto simp: sigma_algebra_iff2)
   then show "(UNIV, {{}, UNIV}, \<lambda>A. 0) \<in> {(\<Omega>, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu>} "
     by (auto simp: measure_space_def positive_def countably_additive_def)
 qed