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: