add lemma indep_distribution_eq_measure
authorhoelzl
Thu May 26 17:40:01 2011 +0200 (2011-05-26)
changeset 42988d8f3fc934ff6
parent 42987 73e2d802ea41
child 42989 40adeda9a8d2
add lemma indep_distribution_eq_measure
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Independent_Family.thy
src/HOL/Probability/Probability_Measure.thy
src/HOL/Probability/Sigma_Algebra.thy
     1.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Thu May 26 14:12:06 2011 +0200
     1.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Thu May 26 17:40:01 2011 +0200
     1.3 @@ -325,6 +325,10 @@
     1.4    "\<lbrakk> \<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i) \<rbrakk> \<Longrightarrow> Pi\<^isub>E I A \<in> sets P"
     1.5    by (auto simp: sets_product_algebra)
     1.6  
     1.7 +lemma Int_stable_product_algebra_generator:
     1.8 +  "(\<And>i. i \<in> I \<Longrightarrow> Int_stable (M i)) \<Longrightarrow> Int_stable (product_algebra_generator I M)"
     1.9 +  by (auto simp add: product_algebra_generator_def Int_stable_def PiE_Int Pi_iff)
    1.10 +
    1.11  section "Generating set generates also product algebra"
    1.12  
    1.13  lemma sigma_product_algebra_sigma_eq:
    1.14 @@ -478,6 +482,32 @@
    1.15      using `A \<in> sets (M i)` by (auto intro!: product_algebraI)
    1.16  qed (insert `i \<in> I`, auto)
    1.17  
    1.18 +lemma (in sigma_algebra) measurable_restrict:
    1.19 +  assumes I: "finite I"
    1.20 +  assumes "\<And>i. i \<in> I \<Longrightarrow> sets (N i) \<subseteq> Pow (space (N i))"
    1.21 +  assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable M (N i)"
    1.22 +  shows "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> measurable M (Pi\<^isub>M I N)"
    1.23 +  unfolding product_algebra_def
    1.24 +proof (simp, rule measurable_sigma)
    1.25 +  show "sets (product_algebra_generator I N) \<subseteq> Pow (space (product_algebra_generator I N))"
    1.26 +    by (rule product_algebra_generator_sets_into_space) fact
    1.27 +  show "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> space M \<rightarrow> space (product_algebra_generator I N)"
    1.28 +    using X by (auto simp: measurable_def)
    1.29 +  fix E assume "E \<in> sets (product_algebra_generator I N)"
    1.30 +  then obtain F where "E = Pi\<^isub>E I F" and F: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> sets (N i)"
    1.31 +    by (auto simp: product_algebra_generator_def)
    1.32 +  then have "(\<lambda>x. \<lambda>i\<in>I. X i x) -` E \<inter> space M = (\<Inter>i\<in>I. X i -` F i \<inter> space M) \<inter> space M"
    1.33 +    by (auto simp: Pi_iff)
    1.34 +  also have "\<dots> \<in> sets M"
    1.35 +  proof cases
    1.36 +    assume "I = {}" then show ?thesis by simp
    1.37 +  next
    1.38 +    assume "I \<noteq> {}" with X F I show ?thesis
    1.39 +      by (intro finite_INT measurable_sets Int) auto
    1.40 +  qed
    1.41 +  finally show "(\<lambda>x. \<lambda>i\<in>I. X i x) -` E \<inter> space M \<in> sets M" .
    1.42 +qed
    1.43 +
    1.44  locale product_sigma_finite =
    1.45    fixes M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme"
    1.46    assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i)"
    1.47 @@ -719,9 +749,8 @@
    1.48        using A unfolding product_algebra_def by auto
    1.49    next
    1.50      show "Int_stable IJ.G"
    1.51 -      by (simp add: PiE_Int Int_stable_def product_algebra_def
    1.52 -                    product_algebra_generator_def)
    1.53 -          auto
    1.54 +      by (rule Int_stable_product_algebra_generator)
    1.55 +         (auto simp: Int_stable_def)
    1.56      show "range ?F \<subseteq> sets IJ.G" using F
    1.57        by (simp add: image_subset_iff product_algebra_def
    1.58                      product_algebra_generator_def)
     2.1 --- a/src/HOL/Probability/Independent_Family.thy	Thu May 26 14:12:06 2011 +0200
     2.2 +++ b/src/HOL/Probability/Independent_Family.thy	Thu May 26 17:40:01 2011 +0200
     2.3 @@ -120,19 +120,6 @@
     2.4      and indep_setD_ev2: "B \<subseteq> events"
     2.5    using indep unfolding indep_set_def indep_sets_def UNIV_bool by auto
     2.6  
     2.7 -lemma dynkin_systemI':
     2.8 -  assumes 1: "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
     2.9 -  assumes empty: "{} \<in> sets M"
    2.10 -  assumes Diff: "\<And> A. A \<in> sets M \<Longrightarrow> space M - A \<in> sets M"
    2.11 -  assumes 2: "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M
    2.12 -          \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
    2.13 -  shows "dynkin_system M"
    2.14 -proof -
    2.15 -  from Diff[OF empty] have "space M \<in> sets M" by auto
    2.16 -  from 1 this Diff 2 show ?thesis
    2.17 -    by (intro dynkin_systemI) auto
    2.18 -qed
    2.19 -
    2.20  lemma (in prob_space) indep_sets_dynkin:
    2.21    assumes indep: "indep_sets F I"
    2.22    shows "indep_sets (\<lambda>i. sets (dynkin \<lparr> space = space M, sets = F i \<rparr>)) I"
    2.23 @@ -714,7 +701,7 @@
    2.24      and Int_stable: "\<And>i. i \<in> I \<Longrightarrow> Int_stable (M' i)"
    2.25      and space: "\<And>i. i \<in> I \<Longrightarrow> space (M' i) \<in> sets (M' i)"
    2.26    shows "indep_rv (\<lambda>i. sigma (M' i)) X I \<longleftrightarrow>
    2.27 -    (\<forall>A\<in>(\<Pi> i\<in>I. sets (M' i)). prob (\<Inter>j\<in>I. X j -` A j \<inter> space M) = (\<Prod>j\<in>I. distribution (X j) (A j)))"
    2.28 +    (\<forall>A\<in>(\<Pi> i\<in>I. sets (M' i)). prob (\<Inter>j\<in>I. X j -` A j \<inter> space M) = (\<Prod>j\<in>I. prob (X j -` A j \<inter> space M)))"
    2.29  proof -
    2.30    from rv have X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> space M \<rightarrow> space (M' i)"
    2.31      unfolding measurable_def by simp
    2.32 @@ -774,7 +761,138 @@
    2.33        by simp
    2.34    qed
    2.35    then show ?thesis using `I \<noteq> {}`
    2.36 -    by (simp add: rv distribution_def indep_rv_def)
    2.37 +    by (simp add: rv indep_rv_def)
    2.38 +qed
    2.39 +
    2.40 +lemma (in prob_space) indep_rv_compose:
    2.41 +  assumes "indep_rv M' X I"
    2.42 +  assumes rv:
    2.43 +    "\<And>i. i \<in> I \<Longrightarrow> sigma_algebra (N i)"
    2.44 +    "\<And>i. i \<in> I \<Longrightarrow> Y i \<in> measurable (M' i) (N i)"
    2.45 +  shows "indep_rv N (\<lambda>i. Y i \<circ> X i) I"
    2.46 +  unfolding indep_rv_def
    2.47 +proof
    2.48 +  from rv `indep_rv M' X I`
    2.49 +  show "\<forall>i\<in>I. random_variable (N i) (Y i \<circ> X i)"
    2.50 +    by (auto intro!: measurable_comp simp: indep_rv_def)
    2.51 +
    2.52 +  have "indep_sets (\<lambda>i. sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}) I"
    2.53 +    using `indep_rv M' X I` by (simp add: indep_rv_def)
    2.54 +  then show "indep_sets (\<lambda>i. sigma_sets (space M) {(Y i \<circ> X i) -` A \<inter> space M |A. A \<in> sets (N i)}) I"
    2.55 +  proof (rule indep_sets_mono_sets)
    2.56 +    fix i assume "i \<in> I"
    2.57 +    with `indep_rv M' X I` have X: "X i \<in> space M \<rightarrow> space (M' i)"
    2.58 +      unfolding indep_rv_def measurable_def by auto
    2.59 +    { fix A assume "A \<in> sets (N i)"
    2.60 +      then have "\<exists>B. (Y i \<circ> X i) -` A \<inter> space M = X i -` B \<inter> space M \<and> B \<in> sets (M' i)"
    2.61 +        by (intro exI[of _ "Y i -` A \<inter> space (M' i)"])
    2.62 +           (auto simp: vimage_compose intro!: measurable_sets rv `i \<in> I` funcset_mem[OF X]) }
    2.63 +    then show "sigma_sets (space M) {(Y i \<circ> X i) -` A \<inter> space M |A. A \<in> sets (N i)} \<subseteq>
    2.64 +      sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}"
    2.65 +      by (intro sigma_sets_subseteq) (auto simp: vimage_compose)
    2.66 +  qed
    2.67 +qed
    2.68 +
    2.69 +lemma (in prob_space) indep_rvD:
    2.70 +  assumes X: "indep_rv M' X I"
    2.71 +  assumes I: "I \<noteq> {}" "finite I" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M' i)"
    2.72 +  shows "prob (\<Inter>i\<in>I. X i -` A i \<inter> space M) = (\<Prod>i\<in>I. prob (X i -` A i \<inter> space M))"
    2.73 +proof (rule indep_setsD)
    2.74 +  show "indep_sets (\<lambda>i. sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}) I"
    2.75 +    using X by (auto simp: indep_rv_def)
    2.76 +  show "I \<subseteq> I" "I \<noteq> {}" "finite I" using I by auto
    2.77 +  show "\<forall>i\<in>I. X i -` A i \<inter> space M \<in> sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}"
    2.78 +    using I by (auto intro: sigma_sets.Basic)
    2.79 +qed
    2.80 +
    2.81 +lemma (in prob_space) indep_distribution_eq_measure:
    2.82 +  assumes I: "I \<noteq> {}" "finite I"
    2.83 +  assumes rv: "\<And>i. random_variable (M' i) (X i)"
    2.84 +  shows "indep_rv M' X I \<longleftrightarrow>
    2.85 +    (\<forall>A\<in>sets (\<Pi>\<^isub>M i\<in>I. (M' i \<lparr> measure := extreal\<circ>distribution (X i) \<rparr>)).
    2.86 +      distribution (\<lambda>x. \<lambda>i\<in>I. X i x) A =
    2.87 +      finite_measure.\<mu>' (\<Pi>\<^isub>M i\<in>I. (M' i \<lparr> measure := extreal\<circ>distribution (X i) \<rparr>)) A)"
    2.88 +    (is "_ \<longleftrightarrow> (\<forall>X\<in>_. distribution ?D X = finite_measure.\<mu>' (Pi\<^isub>M I ?M) X)")
    2.89 +proof -
    2.90 +  interpret M': prob_space "?M i" for i
    2.91 +    using rv by (rule distribution_prob_space)
    2.92 +  interpret P: finite_product_prob_space ?M I
    2.93 +    proof qed fact
    2.94 +
    2.95 +  let ?D' = "(Pi\<^isub>M I ?M) \<lparr> measure := extreal \<circ> distribution ?D \<rparr>"
    2.96 +  have "random_variable P.P ?D"
    2.97 +    using `finite I` rv by (intro random_variable_restrict) auto
    2.98 +  then interpret D: prob_space ?D'
    2.99 +    by (rule distribution_prob_space)
   2.100 +
   2.101 +  show ?thesis
   2.102 +  proof (intro iffI ballI)
   2.103 +    assume "indep_rv M' X I"
   2.104 +    fix A assume "A \<in> sets P.P"
   2.105 +    moreover
   2.106 +    have "D.prob A = P.prob A"
   2.107 +    proof (rule prob_space_unique_Int_stable)
   2.108 +      show "prob_space ?D'" by default
   2.109 +      show "prob_space (Pi\<^isub>M I ?M)" by default
   2.110 +      show "Int_stable P.G" using M'.Int
   2.111 +        by (intro Int_stable_product_algebra_generator) (simp add: Int_stable_def)
   2.112 +      show "space P.G \<in> sets P.G"
   2.113 +        using M'.top by (simp add: product_algebra_generator_def)
   2.114 +      show "space ?D' = space P.G"  "sets ?D' = sets (sigma P.G)"
   2.115 +        by (simp_all add: product_algebra_def product_algebra_generator_def sets_sigma)
   2.116 +      show "space P.P = space P.G" "sets P.P = sets (sigma P.G)"
   2.117 +        by (simp_all add: product_algebra_def)
   2.118 +      show "A \<in> sets (sigma P.G)"
   2.119 +        using `A \<in> sets P.P` by (simp add: product_algebra_def)
   2.120 +    
   2.121 +      fix E assume E: "E \<in> sets P.G"
   2.122 +      then have "E \<in> sets P.P"
   2.123 +        by (simp add: sets_sigma sigma_sets.Basic product_algebra_def)
   2.124 +      then have "D.prob E = distribution ?D E"
   2.125 +        unfolding D.\<mu>'_def by simp
   2.126 +      also
   2.127 +      from E obtain F where "E = Pi\<^isub>E I F" and F: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> sets (M' i)"
   2.128 +        by (auto simp: product_algebra_generator_def)
   2.129 +      with `I \<noteq> {}` have "distribution ?D E = prob (\<Inter>i\<in>I. X i -` F i \<inter> space M)"
   2.130 +        using `I \<noteq> {}` by (auto intro!: arg_cong[where f=prob] simp: Pi_iff distribution_def)
   2.131 +      also have "\<dots> = (\<Prod>i\<in>I. prob (X i -` F i \<inter> space M))"
   2.132 +        using `indep_rv M' X I` I F by (rule indep_rvD)
   2.133 +      also have "\<dots> = P.prob E"
   2.134 +        using F by (simp add: `E = Pi\<^isub>E I F` P.prob_times M'.\<mu>'_def distribution_def)
   2.135 +      finally show "D.prob E = P.prob E" .
   2.136 +    qed
   2.137 +    ultimately show "distribution ?D A = P.prob A"
   2.138 +      by (simp add: D.\<mu>'_def)
   2.139 +  next
   2.140 +    assume eq: "\<forall>A\<in>sets P.P. distribution ?D A = P.prob A"
   2.141 +    have [simp]: "\<And>i. sigma (M' i) = M' i"
   2.142 +      using rv by (intro sigma_algebra.sigma_eq) simp
   2.143 +    have "indep_rv (\<lambda>i. sigma (M' i)) X I"
   2.144 +    proof (subst indep_rv_finite[OF I])
   2.145 +      fix i assume [simp]: "i \<in> I"
   2.146 +      show "random_variable (sigma (M' i)) (X i)"
   2.147 +        using rv[of i] by simp
   2.148 +      show "Int_stable (M' i)" "space (M' i) \<in> sets (M' i)"
   2.149 +        using M'.Int[of _ i] M'.top by (auto simp: Int_stable_def)
   2.150 +    next
   2.151 +      show "\<forall>A\<in>\<Pi> i\<in>I. sets (M' i). prob (\<Inter>j\<in>I. X j -` A j \<inter> space M) = (\<Prod>j\<in>I. prob (X j -` A j \<inter> space M))"
   2.152 +      proof
   2.153 +        fix A assume A: "A \<in> (\<Pi> i\<in>I. sets (M' i))"
   2.154 +        then have A_in_P: "(Pi\<^isub>E I A) \<in> sets P.P"
   2.155 +          by (auto intro!: product_algebraI)
   2.156 +        have "prob (\<Inter>j\<in>I. X j -` A j \<inter> space M) = distribution ?D (Pi\<^isub>E I A)"
   2.157 +          using `I \<noteq> {}`by (auto intro!: arg_cong[where f=prob] simp: Pi_iff distribution_def)
   2.158 +        also have "\<dots> = P.prob (Pi\<^isub>E I A)" using A_in_P eq by simp
   2.159 +        also have "\<dots> = (\<Prod>i\<in>I. M'.prob i (A i))"
   2.160 +          using A by (intro P.prob_times) auto
   2.161 +        also have "\<dots> = (\<Prod>i\<in>I. prob (X i -` A i \<inter> space M))"
   2.162 +          using A by (auto intro!: setprod_cong simp: M'.\<mu>'_def Pi_iff distribution_def)
   2.163 +        finally show "prob (\<Inter>j\<in>I. X j -` A j \<inter> space M) = (\<Prod>j\<in>I. prob (X j -` A j \<inter> space M))" .
   2.164 +      qed
   2.165 +    qed
   2.166 +    then show "indep_rv M' X I"
   2.167 +      by simp
   2.168 +  qed
   2.169  qed
   2.170  
   2.171  end
     3.1 --- a/src/HOL/Probability/Probability_Measure.thy	Thu May 26 14:12:06 2011 +0200
     3.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Thu May 26 17:40:01 2011 +0200
     3.3 @@ -188,6 +188,37 @@
     3.4    qed
     3.5  qed
     3.6  
     3.7 +lemma prob_space_unique_Int_stable:
     3.8 +  fixes E :: "('a, 'b) algebra_scheme" and A :: "nat \<Rightarrow> 'a set"
     3.9 +  assumes E: "Int_stable E" "space E \<in> sets E"
    3.10 +  and M: "prob_space M" "space M = space E" "sets M = sets (sigma E)"
    3.11 +  and N: "prob_space N" "space N = space E" "sets N = sets (sigma E)"
    3.12 +  and eq: "\<And>X. X \<in> sets E \<Longrightarrow> finite_measure.\<mu>' M X = finite_measure.\<mu>' N X"
    3.13 +  assumes "X \<in> sets (sigma E)"
    3.14 +  shows "finite_measure.\<mu>' M X = finite_measure.\<mu>' N X"
    3.15 +proof -
    3.16 +  interpret M!: prob_space M by fact
    3.17 +  interpret N!: prob_space N by fact
    3.18 +  have "measure M X = measure N X"
    3.19 +  proof (rule measure_unique_Int_stable[OF `Int_stable E`])
    3.20 +    show "range (\<lambda>i. space M) \<subseteq> sets E" "incseq (\<lambda>i. space M)" "(\<Union>i. space M) = space E"
    3.21 +      using E M N by auto
    3.22 +    show "\<And>i. M.\<mu> (space M) \<noteq> \<infinity>"
    3.23 +      using M.measure_space_1 by simp
    3.24 +    show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure_space.measure = M.\<mu>\<rparr>"
    3.25 +      using E M N by (auto intro!: M.measure_space_cong)
    3.26 +    show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure_space.measure = N.\<mu>\<rparr>"
    3.27 +      using E M N by (auto intro!: N.measure_space_cong)
    3.28 +    { fix X assume "X \<in> sets E"
    3.29 +      then have "X \<in> sets (sigma E)"
    3.30 +        by (auto simp: sets_sigma sigma_sets.Basic)
    3.31 +      with eq[OF `X \<in> sets E`] M N show "M.\<mu> X = N.\<mu> X"
    3.32 +        by (simp add: M.finite_measure_eq N.finite_measure_eq) }
    3.33 +  qed fact
    3.34 +  with `X \<in> sets (sigma E)` M N show ?thesis
    3.35 +    by (simp add: M.finite_measure_eq N.finite_measure_eq)
    3.36 +qed
    3.37 +
    3.38  lemma (in prob_space) distribution_prob_space:
    3.39    assumes X: "random_variable S X"
    3.40    shows "prob_space (S\<lparr>measure := extreal \<circ> distribution X\<rparr>)" (is "prob_space ?S")
    3.41 @@ -359,6 +390,50 @@
    3.42    shows "prob_space ((MX \<Otimes>\<^isub>M MY) \<lparr> measure := extreal \<circ> joint_distribution X Y\<rparr>)"
    3.43    using random_variable_pairI[OF assms] by (rule distribution_prob_space)
    3.44  
    3.45 +
    3.46 +locale finite_product_prob_space =
    3.47 +  fixes M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme"
    3.48 +    and I :: "'i set"
    3.49 +  assumes prob_space: "\<And>i. prob_space (M i)" and finite_index: "finite I"
    3.50 +
    3.51 +sublocale finite_product_prob_space \<subseteq> M: prob_space "M i" for i
    3.52 +  by (rule prob_space)
    3.53 +
    3.54 +sublocale finite_product_prob_space \<subseteq> finite_product_sigma_finite M I
    3.55 +  by default (rule finite_index)
    3.56 +
    3.57 +sublocale finite_product_prob_space \<subseteq> prob_space "\<Pi>\<^isub>M i\<in>I. M i"
    3.58 +  proof qed (simp add: measure_times M.measure_space_1 setprod_1)
    3.59 +
    3.60 +lemma (in finite_product_prob_space) prob_times:
    3.61 +  assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets (M i)"
    3.62 +  shows "prob (\<Pi>\<^isub>E i\<in>I. X i) = (\<Prod>i\<in>I. M.prob i (X i))"
    3.63 +proof -
    3.64 +  have "extreal (\<mu>' (\<Pi>\<^isub>E i\<in>I. X i)) = \<mu> (\<Pi>\<^isub>E i\<in>I. X i)"
    3.65 +    using X by (intro finite_measure_eq[symmetric] in_P) auto
    3.66 +  also have "\<dots> = (\<Prod>i\<in>I. M.\<mu> i (X i))"
    3.67 +    using measure_times X by simp
    3.68 +  also have "\<dots> = extreal (\<Prod>i\<in>I. M.\<mu>' i (X i))"
    3.69 +    using X by (simp add: M.finite_measure_eq setprod_extreal)
    3.70 +  finally show ?thesis by simp
    3.71 +qed
    3.72 +
    3.73 +lemma (in prob_space) random_variable_restrict:
    3.74 +  assumes I: "finite I"
    3.75 +  assumes X: "\<And>i. i \<in> I \<Longrightarrow> random_variable (N i) (X i)"
    3.76 +  shows "random_variable (Pi\<^isub>M I N) (\<lambda>x. \<lambda>i\<in>I. X i x)"
    3.77 +proof
    3.78 +  { fix i assume "i \<in> I"
    3.79 +    with X interpret N: sigma_algebra "N i" by simp
    3.80 +    have "sets (N i) \<subseteq> Pow (space (N i))" by (rule N.space_closed) }
    3.81 +  note N_closed = this
    3.82 +  then show "sigma_algebra (Pi\<^isub>M I N)"
    3.83 +    by (simp add: product_algebra_def)
    3.84 +       (intro sigma_algebra_sigma product_algebra_generator_sets_into_space)
    3.85 +  show "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> measurable M (Pi\<^isub>M I N)"
    3.86 +    using X by (intro measurable_restrict[OF I N_closed]) auto
    3.87 +qed
    3.88 +
    3.89  section "Probability spaces on finite sets"
    3.90  
    3.91  locale finite_prob_space = prob_space + finite_measure_space
     4.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Thu May 26 14:12:06 2011 +0200
     4.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Thu May 26 17:40:01 2011 +0200
     4.3 @@ -1406,6 +1406,19 @@
     4.4    shows "dynkin_system M"
     4.5    using assms by (auto simp: dynkin_system_def dynkin_system_axioms_def subset_class_def)
     4.6  
     4.7 +lemma dynkin_systemI':
     4.8 +  assumes 1: "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
     4.9 +  assumes empty: "{} \<in> sets M"
    4.10 +  assumes Diff: "\<And> A. A \<in> sets M \<Longrightarrow> space M - A \<in> sets M"
    4.11 +  assumes 2: "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M
    4.12 +          \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
    4.13 +  shows "dynkin_system M"
    4.14 +proof -
    4.15 +  from Diff[OF empty] have "space M \<in> sets M" by auto
    4.16 +  from 1 this Diff 2 show ?thesis
    4.17 +    by (intro dynkin_systemI) auto
    4.18 +qed
    4.19 +
    4.20  lemma dynkin_system_trivial:
    4.21    shows "dynkin_system \<lparr> space = A, sets = Pow A \<rparr>"
    4.22    by (rule dynkin_systemI) auto