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: