diff -r 56a408fa2440 -r 28c1f4f5335f src/HOL/Probability/Giry_Monad.thy --- a/src/HOL/Probability/Giry_Monad.thy Sat Aug 12 10:09:29 2023 +0100 +++ b/src/HOL/Probability/Giry_Monad.thy Mon Aug 21 18:38:25 2023 +0100 @@ -31,7 +31,7 @@ qed lemma (in subprob_space) emeasure_subprob_space_less_top: "emeasure M A \ top" - using emeasure_finite[of A] . + by simp lemma prob_space_imp_subprob_space: "prob_space M \ subprob_space M" @@ -44,10 +44,10 @@ by (rule subprob_spaceI) (simp_all add: emeasure_space_1 not_empty) lemma subprob_space_sigma [simp]: "\ \ {} \ subprob_space (sigma \ X)" -by(rule subprob_spaceI)(simp_all add: emeasure_sigma space_measure_of_conv) + by(rule subprob_spaceI)(simp_all add: emeasure_sigma space_measure_of_conv) lemma subprob_space_null_measure: "space M \ {} \ subprob_space (null_measure M)" -by(simp add: null_measure_def) + by(simp add: null_measure_def) lemma (in subprob_space) subprob_space_distr: assumes f: "f \ measurable M M'" and "space M' \ {}" shows "subprob_space (distr M M' f)" @@ -343,7 +343,7 @@ assumes [measurable]: "f \ measurable M N" shows "(\M'. distr M' N f) \ measurable (subprob_algebra M) (subprob_algebra N)" proof (cases "space N = {}") - assume not_empty: "space N \ {}" + case False show ?thesis proof (rule measurable_subprob_algebra) fix A assume A: "A \ sets N" @@ -355,8 +355,8 @@ also have "\" using A by (intro measurable_emeasure_subprob_algebra) simp finally show "(\M'. emeasure (distr M' N f) A) \ borel_measurable (subprob_algebra M)" . - qed (auto intro!: subprob_space.subprob_space_distr simp: space_subprob_algebra not_empty cong: measurable_cong_sets) -qed (insert assms, auto simp: measurable_empty_iff space_subprob_algebra_empty_iff) + qed (auto intro!: subprob_space.subprob_space_distr simp: space_subprob_algebra False cong: measurable_cong_sets) +qed (use assms in \auto simp: measurable_empty_iff space_subprob_algebra_empty_iff\) lemma emeasure_space_subprob_algebra[measurable]: "(\a. emeasure a (space a)) \ borel_measurable (subprob_algebra N)" @@ -565,10 +565,7 @@ lemma subprob_space_return_ne: assumes "space M \ {}" shows "subprob_space (return M x)" -proof - show "emeasure (return M x) (space (return M x)) \ 1" - by (subst emeasure_return) (auto split: split_indicator) -qed (simp, fact) + by (metis assms emeasure_return indicator_simps(2) sets.top space_return subprob_spaceI subprob_space_return zero_le) lemma measure_return: assumes X: "X \ sets M" shows "measure (return M x) X = indicator X x" unfolding measure_def emeasure_return[OF X, of x] by (simp split: split_indicator) @@ -654,8 +651,7 @@ by (auto simp add: emeasure_distr f_M' cong: measurable_cong_sets) also have "\ = (\\<^sup>+M''. emeasure (g x) (f M'' -` A \ space M) \?R)" apply (subst emeasure_pair_measure_alt) - apply (rule measurable_sets[OF _ A]) - apply (auto simp add: f_M' cong: measurable_cong_sets) + apply (force simp add: f_M' cong: measurable_cong_sets intro!: measurable_sets[OF _ A]) apply (intro nn_integral_cong arg_cong[where f="emeasure (g x)"]) apply (auto simp: space_subprob_algebra space_pair_measure) done @@ -668,10 +664,10 @@ qed qed also have "\" - apply (intro measurable_compose[OF measurable_pair_measure measurable_distr]) - apply (rule return_measurable) - apply measurable - done + proof (intro measurable_compose[OF measurable_pair_measure measurable_distr]) + show "return L \ L \\<^sub>M subprob_algebra L" + by (rule return_measurable) + qed measurable finally show ?thesis . qed @@ -703,19 +699,15 @@ have *: "\x. fst x \ space M \ snd x \ A (fst x) \ x \ (SIGMA x:space M. A x)" by (auto simp: fun_eq_iff) - have "(\(x, y). indicator (A x) y::ennreal) \ borel_measurable (M \\<^sub>M N)" + have MN: "Measurable.pred (M \\<^sub>M N) (\w. w \ Sigma (space M) A)" + by auto + then have "(\(x, y). indicator (A x) y::ennreal) \ borel_measurable (M \\<^sub>M N)" apply measurable - apply (subst measurable_cong) - apply (rule *) - apply (auto simp: space_pair_measure) - done + by (smt (verit, best) MN measurable_cong mem_Sigma_iff prod.collapse space_pair_measure) then have "(\x. integral\<^sup>N (L x) (indicator (A x))) \ borel_measurable M" by (intro nn_integral_measurable_subprob_algebra2[where N=N] L) then show "(\x. emeasure (L x) (A x)) \ borel_measurable M" - apply (rule measurable_cong[THEN iffD1, rotated]) - apply (rule nn_integral_indicator) - apply (simp add: subprob_measurableD[OF L] **) - done + by (smt (verit) "**" L measurable_cong_simp nn_integral_indicator sets_kernel) qed lemma measure_measurable_subprob_algebra2: @@ -751,7 +743,7 @@ next assume "space (subprob_algebra N) \ {}" with eq show ?thesis - by (fastforce simp add: space_subprob_algebra) + by (smt (verit) equals0I mem_Collect_eq space_subprob_algebra) qed qed @@ -807,10 +799,11 @@ assume [simp]: "space N \ {}" fix M assume M: "M \ space (subprob_algebra (subprob_algebra N))" then have "(\\<^sup>+M'. emeasure M' (space N) \M) \ (\\<^sup>+M'. 1 \M)" - apply (intro nn_integral_mono) - apply (auto simp: space_subprob_algebra - dest!: sets_eq_imp_space_eq subprob_space.emeasure_space_le_1) - done + proof (intro nn_integral_mono) + show "\x. \M \ space (subprob_algebra (subprob_algebra N)); x \ space M\ + \ emeasure x (space N) \ 1" + by (smt (verit) mem_Collect_eq sets_eq_imp_space_eq space_subprob_algebra subprob_space.subprob_emeasure_le_1) + qed with M show "subprob_space (join M)" by (intro subprob_spaceI) (auto simp: emeasure_join space_subprob_algebra M dest: subprob_space.emeasure_space_le_1) @@ -888,7 +881,7 @@ lemma measurable_join1: "\ f \ measurable N K; sets M = sets (subprob_algebra N) \ \ f \ measurable (join M) K" -by(simp add: measurable_def) + by(simp add: measurable_def) lemma fixes f :: "_ \ real" @@ -1051,12 +1044,15 @@ lemma join_return': assumes "sets N = sets M" shows "join (distr M (subprob_algebra N) (return N)) = M" -apply (rule measure_eqI) -apply (simp add: assms) -apply (subgoal_tac "return N \ measurable M (subprob_algebra N)") -apply (simp add: emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra assms) -apply (subst measurable_cong_sets, rule assms[symmetric], rule refl, rule return_measurable) -done +proof (rule measure_eqI) + fix A + have "return N \ measurable M (subprob_algebra N)" + using assms by auto + moreover + assume "A \ sets (join (distr M (subprob_algebra N) (return N)))" + ultimately show "emeasure (join (distr M (subprob_algebra N) (return N))) A = emeasure M A" + by (simp add: emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra assms) +qed (simp add: assms) lemma join_distr_distr: fixes f :: "'a \ 'b" and M :: "'a measure measure" and N :: "'b measure" @@ -1107,7 +1103,7 @@ by (simp add: bind_def) lemma sets_bind_empty: "sets M = {} \ sets (bind M f) = {{}}" - by (auto simp: bind_def) + by auto lemma space_bind_empty: "space M = {} \ space (bind M f) = {}" by (simp add: bind_def) @@ -1139,11 +1135,12 @@ lemma bind_nonempty': assumes "f \ measurable M (subprob_algebra N)" "x \ space M" shows "bind M f = join (distr M (subprob_algebra N) f)" - using assms - apply (subst bind_nonempty, blast) - apply (subst subprob_algebra_cong[OF sets_kernel[OF assms(1) someI_ex]], blast) - apply (simp add: subprob_algebra_cong[OF sets_kernel[OF assms]]) - done +proof - + have "join (distr M (subprob_algebra (f (SOME x. x \ space M))) f) = join (distr M (subprob_algebra N) f)" + by (metis assms someI_ex subprob_algebra_cong subprob_measurableD(2)) + with assms show ?thesis + by (metis bind_nonempty empty_iff) +qed lemma bind_nonempty'': assumes "f \ measurable M (subprob_algebra N)" "space M \ {}" @@ -1182,14 +1179,15 @@ have "(AE x in M \ N. P x) \ (\\<^sup>+ x. integral\<^sup>N (N x) (indicator {x \ space B. \ P x}) \M) = 0" by (simp add: AE_iff_nn_integral sets_bind[OF _ M] space_bind[OF _ M] * nn_integral_bind[where B=B] del: nn_integral_indicator) - also have "\ = (AE x in M. AE y in N x. P y)" - apply (subst nn_integral_0_iff_AE) + also have "... = (AE x in M. integral\<^sup>N (N x) (indicator {x \ space B. \ P x}) = 0)" + proof (rule nn_integral_0_iff_AE) + show "(\x. integral\<^sup>N (N x) (indicator {x \ space B. \ P x})) \ borel_measurable M" apply (rule measurable_compose[OF N nn_integral_measurable_subprob_algebra]) - apply measurable + by measurable + qed + also have "\ = (AE x in M. AE y in N x. P y)" apply (intro eventually_subst AE_I2) - apply (auto simp add: subprob_measurableD(1)[OF N] - intro!: AE_iff_measurable[symmetric]) - done + by (auto simp add: subprob_measurableD(1)[OF N] intro!: AE_iff_measurable[symmetric]) finally show ?thesis . qed @@ -1351,13 +1349,14 @@ assumes N: "N \ measurable M (subprob_algebra K)" "space M \ {}" assumes f: "f \ measurable K R" shows "distr (M \ N) R f = (M \ (\x. distr (N x) R f))" - unfolding bind_nonempty''[OF N] - apply (subst bind_nonempty''[OF measurable_compose[OF N(1) measurable_distr] N(2)]) - apply (rule f) - apply (simp add: join_distr_distr[OF _ f, symmetric]) - apply (subst distr_distr[OF measurable_distr, OF f N(1)]) - apply (simp add: comp_def) - done +proof - + have "distr (join (distr M (subprob_algebra K) N)) R f = + join (distr M (subprob_algebra R) (\x. distr (N x) R f))" + by (simp add: assms distr_distr[OF measurable_distr] comp_def flip: join_distr_distr) + with assms show ?thesis + unfolding bind_nonempty''[OF N] + by (smt (verit) bind_nonempty sets_distr subprob_algebra_cong) +qed lemma bind_distr: assumes f[measurable]: "f \ measurable M X" @@ -1393,16 +1392,20 @@ show "sets (restrict_space (bind M N) X) = sets (bind M (\x. restrict_space (N x) X))" by (simp add: sets_restrict_space assms(2) sets_bind[OF sets_kernel[OF restrict_space_measurable[OF assms(4,3,1)]]]) fix A assume "A \ sets (restrict_space (M \ N) X)" - with X have "A \ sets K" "A \ X" + with X have A: "A \ sets K" "A \ X" by (auto simp: sets_restrict_space) - then show "emeasure (restrict_space (M \ N) X) A = emeasure (M \ (\x. restrict_space (N x) X)) A" - using assms - apply (subst emeasure_restrict_space) - apply (simp_all add: emeasure_bind[OF assms(2,1)]) - apply (subst emeasure_bind[OF _ restrict_space_measurable[OF _ _ N]]) - apply (auto simp: sets_restrict_space emeasure_restrict_space space_subprob_algebra - intro!: nn_integral_cong dest!: measurable_space) + then have "emeasure (restrict_space (M \ N) X) A = emeasure (M \ N) A" + by (simp add: emeasure_restrict_space) + also have "\ = \\<^sup>+ x. emeasure (N x) A \M" + by (metis \A \ sets K\ N \space M \ {}\ emeasure_bind) + also have "... = \\<^sup>+ x. emeasure (restrict_space (N x) X) A \M" + using A assms by (smt (verit, best) emeasure_restrict_space nn_integral_cong sets.Int_space_eq2 subprob_measurableD(2)) + also have "\ = emeasure (M \ (\x. restrict_space (N x) X)) A" + using A assms + apply (subst emeasure_bind[OF _ restrict_space_measurable]) + apply (auto simp: sets_restrict_space) done + finally show "emeasure (restrict_space (M \ N) X) A = emeasure (M \ (\x. restrict_space (N x) X)) A" . qed lemma bind_restrict_space: @@ -1442,13 +1445,18 @@ (simp_all add: space_subprob_algebra prob_space.not_empty emeasure_bind_const_prob_space) lemma bind_return_distr: - "space M \ {} \ f \ measurable M N \ bind M (return N \ f) = distr M N f" - apply (simp add: bind_nonempty) - apply (subst subprob_algebra_cong) - apply (rule sets_return) - apply (subst distr_distr[symmetric]) - apply (auto intro!: return_measurable simp: distr_distr[symmetric] join_return') - done + assumes "space M \ {}" "f \ measurable M N" + shows "bind M (return N \ f) = distr M N f" +proof - + have "bind M (return N \ f) + = join (distr M (subprob_algebra (return N (f (SOME x. x \ space M)))) (return N \ f))" + by (simp add: Giry_Monad.bind_def assms) + also have "\ = join (distr M (subprob_algebra N) (return N \ f))" + by (metis sets_return subprob_algebra_cong) + also have "\ = distr M N f" + by (metis assms(2) distr_distr join_return' return_measurable sets_distr) + finally show ?thesis . +qed lemma bind_return_distr': "space M \ {} \ f \ measurable M N \ bind M (\x. return N (f x)) = distr M N f" @@ -1469,6 +1477,9 @@ sets_kernel[OF M2 someI_ex[OF ex_in[OF \space N \ {}\]]] note space_some[simp] = sets_eq_imp_space_eq[OF this(1)] sets_eq_imp_space_eq[OF this(2)] + + have *: "(\x. distr x (subprob_algebra R) g) \ f \ M \\<^sub>M subprob_algebra (subprob_algebra R)" + using M1 M2 measurable_comp measurable_distr by blast have "bind M (\x. bind (f x) g) = join (distr M (subprob_algebra R) (join \ (\x. (distr x (subprob_algebra R) g)) \ f))" by (simp add: sets_eq_imp_space_eq[OF sets_fx] bind_nonempty o_def @@ -1478,10 +1489,7 @@ (subprob_algebra (subprob_algebra R)) (\x. distr x (subprob_algebra R) g)) (subprob_algebra R) join" - apply (subst distr_distr, - (blast intro: measurable_comp measurable_distr measurable_join M1 M2)+)+ - apply (simp add: o_assoc) - done + by (simp add: distr_distr M1 M2 measurable_distr measurable_join fun.map_comp *) also have "join ... = bind (bind M f) g" by (simp add: join_assoc join_distr_distr M2 bind_nonempty cong: subprob_algebra_cong) finally show ?thesis .. @@ -1637,7 +1645,7 @@ using measurable_space[OF g] by (auto simp: measurable_restrict_space2_iff prob_algebra_def space_pair_measure Pi_iff intro!: prob_space.prob_space_bind[where S=R] AE_I2) -qed (insert g, simp) +qed (use g in simp) lemma measurable_prob_algebra_generated: @@ -1659,7 +1667,7 @@ by (intro measurable_cong) auto then show "(\a. emeasure (K a) \) \ borel_measurable M" by simp qed -qed (insert subsp, auto) +qed (use subsp in auto) lemma in_space_prob_algebra: "x \ space (prob_algebra M) \ emeasure x (space M) = 1" @@ -1668,13 +1676,7 @@ lemma prob_space_pair: assumes "prob_space M" "prob_space N" shows "prob_space (M \\<^sub>M N)" -proof - - interpret M: prob_space M by fact - interpret N: prob_space N by fact - interpret P: pair_prob_space M N proof qed - show ?thesis - by unfold_locales -qed + by (metis assms measurable_fst prob_space.distr_pair_fst prob_space_distrD) lemma measurable_pair_prob[measurable]: "f \ M \\<^sub>M prob_algebra N \ g \ M \\<^sub>M prob_algebra L \ (\x. f x \\<^sub>M g x) \ M \\<^sub>M prob_algebra (N \\<^sub>M L)" @@ -1738,7 +1740,7 @@ also from assms(3) x have "... = emeasure (distr (density M f') (count_space A) g) {x}" by (subst emeasure_distr) simp_all finally show "f x = emeasure (distr (density M f') (count_space A) g) {x}" . -qed (insert assms, auto) +qed (use assms in auto) lemma bind_cong_AE: assumes "M = N" @@ -1796,7 +1798,6 @@ by eventually_elim auto thus "y \ space M" by simp - show "M = return M y" proof (rule measure_eqI) fix X assume X: "X \ sets M"