src/HOL/Probability/Independent_Family.thy
 changeset 62343 24106dc44def parent 61808 fc1556774cfe child 62390 842917225d56
```     1.1 --- a/src/HOL/Probability/Independent_Family.thy	Wed Feb 17 21:51:55 2016 +0100
1.2 +++ b/src/HOL/Probability/Independent_Family.thy	Wed Feb 17 21:51:56 2016 +0100
1.3 @@ -491,11 +491,18 @@
1.4          where a: "a = (\<Inter>k\<in>Ka. Ea k)" "finite Ka" "Ka \<noteq> {}" "Ka \<subseteq> I j" "\<And>k. k\<in>Ka \<Longrightarrow> Ea k \<in> E k" by auto
1.5        fix b assume "b \<in> ?E j" then obtain Kb Eb
1.6          where b: "b = (\<Inter>k\<in>Kb. Eb k)" "finite Kb" "Kb \<noteq> {}" "Kb \<subseteq> I j" "\<And>k. k\<in>Kb \<Longrightarrow> Eb k \<in> E k" by auto
1.7 -      let ?A = "\<lambda>k. (if k \<in> Ka \<inter> Kb then Ea k \<inter> Eb k else if k \<in> Kb then Eb k else if k \<in> Ka then Ea k else {})"
1.8 -      have "a \<inter> b = INTER (Ka \<union> Kb) ?A"
1.9 -        by (simp add: a b set_eq_iff) auto
1.10 +      let ?f = "\<lambda>k. (if k \<in> Ka \<inter> Kb then Ea k \<inter> Eb k else if k \<in> Kb then Eb k else if k \<in> Ka then Ea k else {})"
1.11 +      have "Ka \<union> Kb = (Ka \<inter> Kb) \<union> (Kb - Ka) \<union> (Ka - Kb)"
1.12 +        by blast
1.13 +      moreover have "(\<Inter>x\<in>Ka \<inter> Kb. Ea x \<inter> Eb x) \<inter>
1.14 +        (\<Inter>x\<in>Kb - Ka. Eb x) \<inter> (\<Inter>x\<in>Ka - Kb. Ea x) = (\<Inter>k\<in>Ka. Ea k) \<inter> (\<Inter>k\<in>Kb. Eb k)"
1.15 +        by auto
1.16 +      ultimately have "(\<Inter>k\<in>Ka \<union> Kb. ?f k) = (\<Inter>k\<in>Ka. Ea k) \<inter> (\<Inter>k\<in>Kb. Eb k)" (is "?lhs = ?rhs")
1.17 +        by (simp only: image_Un Inter_Un_distrib) simp
1.18 +      then have "a \<inter> b = (\<Inter>k\<in>Ka \<union> Kb. ?f k)"
1.19 +        by (simp only: a(1) b(1))
1.20        with a b \<open>j \<in> J\<close> Int_stableD[OF Int_stable] show "a \<inter> b \<in> ?E j"
1.21 -        by (intro CollectI exI[of _ "Ka \<union> Kb"] exI[of _ ?A]) auto
1.22 +        by (intro CollectI exI[of _ "Ka \<union> Kb"] exI[of _ ?f]) auto
1.23      qed
1.24    qed
1.25    ultimately show ?thesis
1.26 @@ -804,14 +811,18 @@
1.27  proof -
1.28    have [measurable]: "\<And>m. {x\<in>space M. P m x} \<in> sets M"
1.29      using assms by (auto simp: indep_events_def)
1.30 -  have "prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 0 \<or> prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 1"
1.31 -    by (rule borel_0_1_law) fact
1.32 +  have *: "(\<Inter>n. \<Union>m\<in>{n..}. {x \<in> space M. P m x}) \<in> events"
1.33 +    by simp
1.34 +  from assms have "prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 0 \<or> prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 1"
1.35 +    by (rule borel_0_1_law)
1.36 +  also have "prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 1 \<longleftrightarrow> (AE x in M. infinite {m. P m x})"
1.37 +    using * by (simp add: prob_eq_1)
1.38 +      (simp add: Bex_def infinite_nat_iff_unbounded_le)
1.39    also have "prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 0 \<longleftrightarrow> (AE x in M. finite {m. P m x})"
1.40 -    by (subst prob_eq_0) (auto simp add: finite_nat_iff_bounded Ball_def not_less[symmetric])
1.41 -  also have "prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 1 \<longleftrightarrow> (AE x in M. infinite {m. P m x})"
1.42 -    by (subst prob_eq_1) (simp_all add: Bex_def infinite_nat_iff_unbounded_le)
1.43 +    using * by (simp add: prob_eq_0)
1.44 +      (auto simp add: Ball_def finite_nat_iff_bounded not_less [symmetric])
1.45    finally show ?thesis
1.46 -    by metis
1.47 +    by blast
1.48  qed
1.49
1.50  lemma (in prob_space) indep_sets_finite:
```