diff -r 1cf129590be8 -r 24106dc44def src/HOL/Probability/Independent_Family.thy
--- a/src/HOL/Probability/Independent_Family.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Probability/Independent_Family.thy Wed Feb 17 21:51:56 2016 +0100
@@ -491,11 +491,18 @@
where a: "a = (\k\Ka. Ea k)" "finite Ka" "Ka \ {}" "Ka \ I j" "\k. k\Ka \ Ea k \ E k" by auto
fix b assume "b \ ?E j" then obtain Kb Eb
where b: "b = (\k\Kb. Eb k)" "finite Kb" "Kb \ {}" "Kb \ I j" "\k. k\Kb \ Eb k \ E k" by auto
- let ?A = "\k. (if k \ Ka \ Kb then Ea k \ Eb k else if k \ Kb then Eb k else if k \ Ka then Ea k else {})"
- have "a \ b = INTER (Ka \ Kb) ?A"
- by (simp add: a b set_eq_iff) auto
+ let ?f = "\k. (if k \ Ka \ Kb then Ea k \ Eb k else if k \ Kb then Eb k else if k \ Ka then Ea k else {})"
+ have "Ka \ Kb = (Ka \ Kb) \ (Kb - Ka) \ (Ka - Kb)"
+ by blast
+ moreover have "(\x\Ka \ Kb. Ea x \ Eb x) \
+ (\x\Kb - Ka. Eb x) \ (\x\Ka - Kb. Ea x) = (\k\Ka. Ea k) \ (\k\Kb. Eb k)"
+ by auto
+ ultimately have "(\k\Ka \ Kb. ?f k) = (\k\Ka. Ea k) \ (\k\Kb. Eb k)" (is "?lhs = ?rhs")
+ by (simp only: image_Un Inter_Un_distrib) simp
+ then have "a \ b = (\k\Ka \ Kb. ?f k)"
+ by (simp only: a(1) b(1))
with a b \j \ J\ Int_stableD[OF Int_stable] show "a \ b \ ?E j"
- by (intro CollectI exI[of _ "Ka \ Kb"] exI[of _ ?A]) auto
+ by (intro CollectI exI[of _ "Ka \ Kb"] exI[of _ ?f]) auto
qed
qed
ultimately show ?thesis
@@ -804,14 +811,18 @@
proof -
have [measurable]: "\m. {x\space M. P m x} \ sets M"
using assms by (auto simp: indep_events_def)
- have "prob (\n. \m\{n..}. ?P m) = 0 \ prob (\n. \m\{n..}. ?P m) = 1"
- by (rule borel_0_1_law) fact
+ have *: "(\n. \m\{n..}. {x \ space M. P m x}) \ events"
+ by simp
+ from assms have "prob (\n. \m\{n..}. ?P m) = 0 \ prob (\n. \m\{n..}. ?P m) = 1"
+ by (rule borel_0_1_law)
+ also have "prob (\n. \m\{n..}. ?P m) = 1 \ (AE x in M. infinite {m. P m x})"
+ using * by (simp add: prob_eq_1)
+ (simp add: Bex_def infinite_nat_iff_unbounded_le)
also have "prob (\n. \m\{n..}. ?P m) = 0 \ (AE x in M. finite {m. P m x})"
- by (subst prob_eq_0) (auto simp add: finite_nat_iff_bounded Ball_def not_less[symmetric])
- also have "prob (\n. \m\{n..}. ?P m) = 1 \ (AE x in M. infinite {m. P m x})"
- by (subst prob_eq_1) (simp_all add: Bex_def infinite_nat_iff_unbounded_le)
+ using * by (simp add: prob_eq_0)
+ (auto simp add: Ball_def finite_nat_iff_bounded not_less [symmetric])
finally show ?thesis
- by metis
+ by blast
qed
lemma (in prob_space) indep_sets_finite: