src/HOL/Probability/Independent_Family.thy
changeset 42861 16375b493b64
child 42981 fe7f5a26e4c6
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Probability/Independent_Family.thy	Tue May 17 11:47:36 2011 +0200
     1.3 @@ -0,0 +1,312 @@
     1.4 +(*  Title:      HOL/Probability/Independent_Family.thy
     1.5 +    Author:     Johannes Hölzl, TU München
     1.6 +*)
     1.7 +
     1.8 +header {* Independent families of events, event sets, and random variables *}
     1.9 +
    1.10 +theory Independent_Family
    1.11 +  imports Probability_Measure
    1.12 +begin
    1.13 +
    1.14 +definition (in prob_space)
    1.15 +  "indep_events A I \<longleftrightarrow> (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j)))"
    1.16 +
    1.17 +definition (in prob_space)
    1.18 +  "indep_sets F I \<longleftrightarrow> (\<forall>i\<in>I. F i \<subseteq> events) \<and> (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow>
    1.19 +    (\<forall>A\<in>(\<Pi> j\<in>J. F j). prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))))"
    1.20 +
    1.21 +definition (in prob_space)
    1.22 +  "indep_sets2 A B \<longleftrightarrow> indep_sets (bool_case A B) UNIV"
    1.23 +
    1.24 +definition (in prob_space)
    1.25 +  "indep_rv M' X I \<longleftrightarrow>
    1.26 +    (\<forall>i\<in>I. random_variable (M' i) (X i)) \<and>
    1.27 +    indep_sets (\<lambda>i. sigma_sets (space M) { X i -` A \<inter> space M | A. A \<in> sets (M' i)}) I"
    1.28 +
    1.29 +lemma (in prob_space) indep_sets_finite_index_sets:
    1.30 +  "indep_sets F I \<longleftrightarrow> (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> indep_sets F J)"
    1.31 +proof (intro iffI allI impI)
    1.32 +  assume *: "\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> indep_sets F J"
    1.33 +  show "indep_sets F I" unfolding indep_sets_def
    1.34 +  proof (intro conjI ballI allI impI)
    1.35 +    fix i assume "i \<in> I"
    1.36 +    with *[THEN spec, of "{i}"] show "F i \<subseteq> events"
    1.37 +      by (auto simp: indep_sets_def)
    1.38 +  qed (insert *, auto simp: indep_sets_def)
    1.39 +qed (auto simp: indep_sets_def)
    1.40 +
    1.41 +lemma (in prob_space) indep_sets_mono_index:
    1.42 +  "J \<subseteq> I \<Longrightarrow> indep_sets F I \<Longrightarrow> indep_sets F J"
    1.43 +  unfolding indep_sets_def by auto
    1.44 +
    1.45 +lemma (in prob_space) indep_sets_mono_sets:
    1.46 +  assumes indep: "indep_sets F I"
    1.47 +  assumes mono: "\<And>i. i\<in>I \<Longrightarrow> G i \<subseteq> F i"
    1.48 +  shows "indep_sets G I"
    1.49 +proof -
    1.50 +  have "(\<forall>i\<in>I. F i \<subseteq> events) \<Longrightarrow> (\<forall>i\<in>I. G i \<subseteq> events)"
    1.51 +    using mono by auto
    1.52 +  moreover have "\<And>A J. J \<subseteq> I \<Longrightarrow> A \<in> (\<Pi> j\<in>J. G j) \<Longrightarrow> A \<in> (\<Pi> j\<in>J. F j)"
    1.53 +    using mono by (auto simp: Pi_iff)
    1.54 +  ultimately show ?thesis
    1.55 +    using indep by (auto simp: indep_sets_def)
    1.56 +qed
    1.57 +
    1.58 +lemma (in prob_space) indep_setsI:
    1.59 +  assumes "\<And>i. i \<in> I \<Longrightarrow> F i \<subseteq> events"
    1.60 +    and "\<And>A J. J \<noteq> {} \<Longrightarrow> J \<subseteq> I \<Longrightarrow> finite J \<Longrightarrow> (\<forall>j\<in>J. A j \<in> F j) \<Longrightarrow> prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))"
    1.61 +  shows "indep_sets F I"
    1.62 +  using assms unfolding indep_sets_def by (auto simp: Pi_iff)
    1.63 +
    1.64 +lemma (in prob_space) indep_setsD:
    1.65 +  assumes "indep_sets F I" and "J \<subseteq> I" "J \<noteq> {}" "finite J" "\<forall>j\<in>J. A j \<in> F j"
    1.66 +  shows "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))"
    1.67 +  using assms unfolding indep_sets_def by auto
    1.68 +
    1.69 +lemma dynkin_systemI':
    1.70 +  assumes 1: "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
    1.71 +  assumes empty: "{} \<in> sets M"
    1.72 +  assumes Diff: "\<And> A. A \<in> sets M \<Longrightarrow> space M - A \<in> sets M"
    1.73 +  assumes 2: "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M
    1.74 +          \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
    1.75 +  shows "dynkin_system M"
    1.76 +proof -
    1.77 +  from Diff[OF empty] have "space M \<in> sets M" by auto
    1.78 +  from 1 this Diff 2 show ?thesis
    1.79 +    by (intro dynkin_systemI) auto
    1.80 +qed
    1.81 +
    1.82 +lemma (in prob_space) indep_sets_dynkin:
    1.83 +  assumes indep: "indep_sets F I"
    1.84 +  shows "indep_sets (\<lambda>i. sets (dynkin \<lparr> space = space M, sets = F i \<rparr>)) I"
    1.85 +    (is "indep_sets ?F I")
    1.86 +proof (subst indep_sets_finite_index_sets, intro allI impI ballI)
    1.87 +  fix J assume "finite J" "J \<subseteq> I" "J \<noteq> {}"
    1.88 +  with indep have "indep_sets F J"
    1.89 +    by (subst (asm) indep_sets_finite_index_sets) auto
    1.90 +  { fix J K assume "indep_sets F K"
    1.91 +    let "?G S i" = "if i \<in> S then ?F i else F i"
    1.92 +    assume "finite J" "J \<subseteq> K"
    1.93 +    then have "indep_sets (?G J) K"
    1.94 +    proof induct
    1.95 +      case (insert j J)
    1.96 +      moreover def G \<equiv> "?G J"
    1.97 +      ultimately have G: "indep_sets G K" "\<And>i. i \<in> K \<Longrightarrow> G i \<subseteq> events" and "j \<in> K"
    1.98 +        by (auto simp: indep_sets_def)
    1.99 +      let ?D = "{E\<in>events. indep_sets (G(j := {E})) K }"
   1.100 +      { fix X assume X: "X \<in> events"
   1.101 +        assume indep: "\<And>J A. J \<noteq> {} \<Longrightarrow> J \<subseteq> K \<Longrightarrow> finite J \<Longrightarrow> j \<notin> J \<Longrightarrow> (\<forall>i\<in>J. A i \<in> G i)
   1.102 +          \<Longrightarrow> prob ((\<Inter>i\<in>J. A i) \<inter> X) = prob X * (\<Prod>i\<in>J. prob (A i))"
   1.103 +        have "indep_sets (G(j := {X})) K"
   1.104 +        proof (rule indep_setsI)
   1.105 +          fix i assume "i \<in> K" then show "(G(j:={X})) i \<subseteq> events"
   1.106 +            using G X by auto
   1.107 +        next
   1.108 +          fix A J assume J: "J \<noteq> {}" "J \<subseteq> K" "finite J" "\<forall>i\<in>J. A i \<in> (G(j := {X})) i"
   1.109 +          show "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))"
   1.110 +          proof cases
   1.111 +            assume "j \<in> J"
   1.112 +            with J have "A j = X" by auto
   1.113 +            show ?thesis
   1.114 +            proof cases
   1.115 +              assume "J = {j}" then show ?thesis by simp
   1.116 +            next
   1.117 +              assume "J \<noteq> {j}"
   1.118 +              have "prob (\<Inter>i\<in>J. A i) = prob ((\<Inter>i\<in>J-{j}. A i) \<inter> X)"
   1.119 +                using `j \<in> J` `A j = X` by (auto intro!: arg_cong[where f=prob] split: split_if_asm)
   1.120 +              also have "\<dots> = prob X * (\<Prod>i\<in>J-{j}. prob (A i))"
   1.121 +              proof (rule indep)
   1.122 +                show "J - {j} \<noteq> {}" "J - {j} \<subseteq> K" "finite (J - {j})" "j \<notin> J - {j}"
   1.123 +                  using J `J \<noteq> {j}` `j \<in> J` by auto
   1.124 +                show "\<forall>i\<in>J - {j}. A i \<in> G i"
   1.125 +                  using J by auto
   1.126 +              qed
   1.127 +              also have "\<dots> = prob (A j) * (\<Prod>i\<in>J-{j}. prob (A i))"
   1.128 +                using `A j = X` by simp
   1.129 +              also have "\<dots> = (\<Prod>i\<in>J. prob (A i))"
   1.130 +                unfolding setprod.insert_remove[OF `finite J`, symmetric, of "\<lambda>i. prob  (A i)"]
   1.131 +                using `j \<in> J` by (simp add: insert_absorb)
   1.132 +              finally show ?thesis .
   1.133 +            qed
   1.134 +          next
   1.135 +            assume "j \<notin> J"
   1.136 +            with J have "\<forall>i\<in>J. A i \<in> G i" by (auto split: split_if_asm)
   1.137 +            with J show ?thesis
   1.138 +              by (intro indep_setsD[OF G(1)]) auto
   1.139 +          qed
   1.140 +        qed }
   1.141 +      note indep_sets_insert = this
   1.142 +      have "dynkin_system \<lparr> space = space M, sets = ?D \<rparr>"
   1.143 +      proof (rule dynkin_systemI', simp_all, safe)
   1.144 +        show "indep_sets (G(j := {{}})) K"
   1.145 +          by (rule indep_sets_insert) auto
   1.146 +      next
   1.147 +        fix X assume X: "X \<in> events" and G': "indep_sets (G(j := {X})) K"
   1.148 +        show "indep_sets (G(j := {space M - X})) K"
   1.149 +        proof (rule indep_sets_insert)
   1.150 +          fix J A assume J: "J \<noteq> {}" "J \<subseteq> K" "finite J" "j \<notin> J" and A: "\<forall>i\<in>J. A i \<in> G i"
   1.151 +          then have A_sets: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> events"
   1.152 +            using G by auto
   1.153 +          have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) =
   1.154 +              prob ((\<Inter>j\<in>J. A j) - (\<Inter>i\<in>insert j J. (A(j := X)) i))"
   1.155 +            using A_sets sets_into_space X `J \<noteq> {}`
   1.156 +            by (auto intro!: arg_cong[where f=prob] split: split_if_asm)
   1.157 +          also have "\<dots> = prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)"
   1.158 +            using J `J \<noteq> {}` `j \<notin> J` A_sets X sets_into_space
   1.159 +            by (auto intro!: finite_measure_Diff finite_INT split: split_if_asm)
   1.160 +          finally have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) =
   1.161 +              prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)" .
   1.162 +          moreover {
   1.163 +            have "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))"
   1.164 +              using J A `finite J` by (intro indep_setsD[OF G(1)]) auto
   1.165 +            then have "prob (\<Inter>j\<in>J. A j) = prob (space M) * (\<Prod>i\<in>J. prob (A i))"
   1.166 +              using prob_space by simp }
   1.167 +          moreover {
   1.168 +            have "prob (\<Inter>i\<in>insert j J. (A(j := X)) i) = (\<Prod>i\<in>insert j J. prob ((A(j := X)) i))"
   1.169 +              using J A `j \<in> K` by (intro indep_setsD[OF G']) auto
   1.170 +            then have "prob (\<Inter>i\<in>insert j J. (A(j := X)) i) = prob X * (\<Prod>i\<in>J. prob (A i))"
   1.171 +              using `finite J` `j \<notin> J` by (auto intro!: setprod_cong) }
   1.172 +          ultimately have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) = (prob (space M) - prob X) * (\<Prod>i\<in>J. prob (A i))"
   1.173 +            by (simp add: field_simps)
   1.174 +          also have "\<dots> = prob (space M - X) * (\<Prod>i\<in>J. prob (A i))"
   1.175 +            using X A by (simp add: finite_measure_compl)
   1.176 +          finally show "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) = prob (space M - X) * (\<Prod>i\<in>J. prob (A i))" .
   1.177 +        qed (insert X, auto)
   1.178 +      next
   1.179 +        fix F :: "nat \<Rightarrow> 'a set" assume disj: "disjoint_family F" and "range F \<subseteq> ?D"
   1.180 +        then have F: "\<And>i. F i \<in> events" "\<And>i. indep_sets (G(j:={F i})) K" by auto
   1.181 +        show "indep_sets (G(j := {\<Union>k. F k})) K"
   1.182 +        proof (rule indep_sets_insert)
   1.183 +          fix J A assume J: "j \<notin> J" "J \<noteq> {}" "J \<subseteq> K" "finite J" and A: "\<forall>i\<in>J. A i \<in> G i"
   1.184 +          then have A_sets: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> events"
   1.185 +            using G by auto
   1.186 +          have "prob ((\<Inter>j\<in>J. A j) \<inter> (\<Union>k. F k)) = prob (\<Union>k. (\<Inter>i\<in>insert j J. (A(j := F k)) i))"
   1.187 +            using `J \<noteq> {}` `j \<notin> J` `j \<in> K` by (auto intro!: arg_cong[where f=prob] split: split_if_asm)
   1.188 +          moreover have "(\<lambda>k. prob (\<Inter>i\<in>insert j J. (A(j := F k)) i)) sums prob (\<Union>k. (\<Inter>i\<in>insert j J. (A(j := F k)) i))"
   1.189 +          proof (rule finite_measure_UNION)
   1.190 +            show "disjoint_family (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i)"
   1.191 +              using disj by (rule disjoint_family_on_bisimulation) auto
   1.192 +            show "range (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i) \<subseteq> events"
   1.193 +              using A_sets F `finite J` `J \<noteq> {}` `j \<notin> J` by (auto intro!: Int)
   1.194 +          qed
   1.195 +          moreover { fix k
   1.196 +            from J A `j \<in> K` have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * (\<Prod>i\<in>J. prob (A i))"
   1.197 +              by (subst indep_setsD[OF F(2)]) (auto intro!: setprod_cong split: split_if_asm)
   1.198 +            also have "\<dots> = prob (F k) * prob (\<Inter>i\<in>J. A i)"
   1.199 +              using J A `j \<in> K` by (subst indep_setsD[OF G(1)]) auto
   1.200 +            finally have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * prob (\<Inter>i\<in>J. A i)" . }
   1.201 +          ultimately have "(\<lambda>k. prob (F k) * prob (\<Inter>i\<in>J. A i)) sums (prob ((\<Inter>j\<in>J. A j) \<inter> (\<Union>k. F k)))"
   1.202 +            by simp
   1.203 +          moreover
   1.204 +          have "(\<lambda>k. prob (F k) * prob (\<Inter>i\<in>J. A i)) sums (prob (\<Union>k. F k) * prob (\<Inter>i\<in>J. A i))"
   1.205 +            using disj F(1) by (intro finite_measure_UNION sums_mult2) auto
   1.206 +          then have "(\<lambda>k. prob (F k) * prob (\<Inter>i\<in>J. A i)) sums (prob (\<Union>k. F k) * (\<Prod>i\<in>J. prob (A i)))"
   1.207 +            using J A `j \<in> K` by (subst indep_setsD[OF G(1), symmetric]) auto
   1.208 +          ultimately
   1.209 +          show "prob ((\<Inter>j\<in>J. A j) \<inter> (\<Union>k. F k)) = prob (\<Union>k. F k) * (\<Prod>j\<in>J. prob (A j))"
   1.210 +            by (auto dest!: sums_unique)
   1.211 +        qed (insert F, auto)
   1.212 +      qed (insert sets_into_space, auto)
   1.213 +      then have mono: "sets (dynkin \<lparr>space = space M, sets = G j\<rparr>) \<subseteq>
   1.214 +        sets \<lparr>space = space M, sets = {E \<in> events. indep_sets (G(j := {E})) K}\<rparr>"
   1.215 +      proof (rule dynkin_system.dynkin_subset, simp_all, safe)
   1.216 +        fix X assume "X \<in> G j"
   1.217 +        then show "X \<in> events" using G `j \<in> K` by auto
   1.218 +        from `indep_sets G K`
   1.219 +        show "indep_sets (G(j := {X})) K"
   1.220 +          by (rule indep_sets_mono_sets) (insert `X \<in> G j`, auto)
   1.221 +      qed
   1.222 +      have "indep_sets (G(j:=?D)) K"
   1.223 +      proof (rule indep_setsI)
   1.224 +        fix i assume "i \<in> K" then show "(G(j := ?D)) i \<subseteq> events"
   1.225 +          using G(2) by auto
   1.226 +      next
   1.227 +        fix A J assume J: "J\<noteq>{}" "J \<subseteq> K" "finite J" and A: "\<forall>i\<in>J. A i \<in> (G(j := ?D)) i"
   1.228 +        show "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))"
   1.229 +        proof cases
   1.230 +          assume "j \<in> J"
   1.231 +          with A have indep: "indep_sets (G(j := {A j})) K" by auto
   1.232 +          from J A show ?thesis
   1.233 +            by (intro indep_setsD[OF indep]) auto
   1.234 +        next
   1.235 +          assume "j \<notin> J"
   1.236 +          with J A have "\<forall>i\<in>J. A i \<in> G i" by (auto split: split_if_asm)
   1.237 +          with J show ?thesis
   1.238 +            by (intro indep_setsD[OF G(1)]) auto
   1.239 +        qed
   1.240 +      qed
   1.241 +      then have "indep_sets (G(j:=sets (dynkin \<lparr>space = space M, sets = G j\<rparr>))) K"
   1.242 +        by (rule indep_sets_mono_sets) (insert mono, auto)
   1.243 +      then show ?case
   1.244 +        by (rule indep_sets_mono_sets) (insert `j \<in> K` `j \<notin> J`, auto simp: G_def)
   1.245 +    qed (insert `indep_sets F K`, simp) }
   1.246 +  from this[OF `indep_sets F J` `finite J` subset_refl]
   1.247 +  show "indep_sets (\<lambda>i. sets (dynkin \<lparr> space = space M, sets = F i \<rparr>)) J"
   1.248 +    by (rule indep_sets_mono_sets) auto
   1.249 +qed
   1.250 +
   1.251 +lemma (in prob_space) indep_sets_sigma:
   1.252 +  assumes indep: "indep_sets F I"
   1.253 +  assumes stable: "\<And>i. i \<in> I \<Longrightarrow> Int_stable \<lparr> space = space M, sets = F i \<rparr>"
   1.254 +  shows "indep_sets (\<lambda>i. sets (sigma \<lparr> space = space M, sets = F i \<rparr>)) I"
   1.255 +proof -
   1.256 +  from indep_sets_dynkin[OF indep]
   1.257 +  show ?thesis
   1.258 +  proof (rule indep_sets_mono_sets, subst sigma_eq_dynkin, simp_all add: stable)
   1.259 +    fix i assume "i \<in> I"
   1.260 +    with indep have "F i \<subseteq> events" by (auto simp: indep_sets_def)
   1.261 +    with sets_into_space show "F i \<subseteq> Pow (space M)" by auto
   1.262 +  qed
   1.263 +qed
   1.264 +
   1.265 +lemma (in prob_space) indep_sets_sigma_sets:
   1.266 +  assumes "indep_sets F I"
   1.267 +  assumes "\<And>i. i \<in> I \<Longrightarrow> Int_stable \<lparr> space = space M, sets = F i \<rparr>"
   1.268 +  shows "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I"
   1.269 +  using indep_sets_sigma[OF assms] by (simp add: sets_sigma)
   1.270 +
   1.271 +lemma (in prob_space) indep_sets2_eq:
   1.272 +  "indep_sets2 A B \<longleftrightarrow> A \<subseteq> events \<and> B \<subseteq> events \<and> (\<forall>a\<in>A. \<forall>b\<in>B. prob (a \<inter> b) = prob a * prob b)"
   1.273 +  unfolding indep_sets2_def
   1.274 +proof (intro iffI ballI conjI)
   1.275 +  assume indep: "indep_sets (bool_case A B) UNIV"
   1.276 +  { fix a b assume "a \<in> A" "b \<in> B"
   1.277 +    with indep_setsD[OF indep, of UNIV "bool_case a b"]
   1.278 +    show "prob (a \<inter> b) = prob a * prob b"
   1.279 +      unfolding UNIV_bool by (simp add: ac_simps) }
   1.280 +  from indep show "A \<subseteq> events" "B \<subseteq> events"
   1.281 +    unfolding indep_sets_def UNIV_bool by auto
   1.282 +next
   1.283 +  assume *: "A \<subseteq> events \<and> B \<subseteq> events \<and> (\<forall>a\<in>A. \<forall>b\<in>B. prob (a \<inter> b) = prob a * prob b)"
   1.284 +  show "indep_sets (bool_case A B) UNIV"
   1.285 +  proof (rule indep_setsI)
   1.286 +    fix i show "(case i of True \<Rightarrow> A | False \<Rightarrow> B) \<subseteq> events"
   1.287 +      using * by (auto split: bool.split)
   1.288 +  next
   1.289 +    fix J X assume "J \<noteq> {}" "J \<subseteq> UNIV" and X: "\<forall>j\<in>J. X j \<in> (case j of True \<Rightarrow> A | False \<Rightarrow> B)"
   1.290 +    then have "J = {True} \<or> J = {False} \<or> J = {True,False}"
   1.291 +      by (auto simp: UNIV_bool)
   1.292 +    then show "prob (\<Inter>j\<in>J. X j) = (\<Prod>j\<in>J. prob (X j))"
   1.293 +      using X * by auto
   1.294 +  qed
   1.295 +qed
   1.296 +
   1.297 +lemma (in prob_space) indep_sets2_sigma_sets:
   1.298 +  assumes "indep_sets2 A B"
   1.299 +  assumes A: "Int_stable \<lparr> space = space M, sets = A \<rparr>"
   1.300 +  assumes B: "Int_stable \<lparr> space = space M, sets = B \<rparr>"
   1.301 +  shows "indep_sets2 (sigma_sets (space M) A) (sigma_sets (space M) B)"
   1.302 +proof -
   1.303 +  have "indep_sets (\<lambda>i. sigma_sets (space M) (case i of True \<Rightarrow> A | False \<Rightarrow> B)) UNIV"
   1.304 +  proof (rule indep_sets_sigma_sets)
   1.305 +    show "indep_sets (bool_case A B) UNIV"
   1.306 +      by (rule `indep_sets2 A B`[unfolded indep_sets2_def])
   1.307 +    fix i show "Int_stable \<lparr>space = space M, sets = case i of True \<Rightarrow> A | False \<Rightarrow> B\<rparr>"
   1.308 +      using A B by (cases i) auto
   1.309 +  qed
   1.310 +  then show ?thesis
   1.311 +    unfolding indep_sets2_def
   1.312 +    by (rule indep_sets_mono_sets) (auto split: bool.split)
   1.313 +qed
   1.314 +
   1.315 +end