diff -r 67deb7bed6d3 -r dfe6449aecd8 src/HOL/Probability/Probability_Mass_Function.thy --- a/src/HOL/Probability/Probability_Mass_Function.thy Wed Feb 11 15:04:23 2015 +0100 +++ b/src/HOL/Probability/Probability_Mass_Function.thy Wed Feb 11 15:22:37 2015 +0100 @@ -502,6 +502,12 @@ shows "(\x. f x \bernoulli_pmf p) = f True * p + f False * (1 - p)" by (subst integral_measure_pmf[of UNIV]) (auto simp: UNIV_bool) +lemma pmf_bernoulli_half [simp]: "pmf (bernoulli_pmf (1 / 2)) x = 1 / 2" +by(cases x) simp_all + +lemma measure_pmf_bernoulli_half: "measure_pmf (bernoulli_pmf (1 / 2)) = uniform_count_measure UNIV" +by(rule measure_eqI)(simp_all add: nn_integral_pmf[symmetric] emeasure_uniform_count_measure nn_integral_count_space_finite sets_uniform_count_measure) + subsubsection \ Geometric Distribution \ lift_definition geometric_pmf :: "nat pmf" is "\n. 1 / 2^Suc n" @@ -639,7 +645,7 @@ "(\x. measure_pmf (M x)) \ measurable (count_space UNIV) (subprob_algebra (count_space UNIV))" by (auto simp: space_subprob_algebra intro!: prob_space_imp_subprob_space) unfold_locales -lemma bind_pmf_cong: +lemma bind_measure_pmf_cong: assumes "\x. A x \ space (subprob_algebra N)" "\x. B x \ space (subprob_algebra N)" assumes "\i. i \ set_pmf x \ A i = B i" shows "bind (measure_pmf x) A = bind (measure_pmf x) B" @@ -879,6 +885,16 @@ unfolding bind_return_pmf''[symmetric] join_eq_bind_pmf bind_assoc_pmf by (simp add: bind_return_pmf'') +lemma bind_pmf_cong: + "\ p = q; \x. x \ set_pmf q \ f x = g x \ + \ bind_pmf p f = bind_pmf q g" +by(simp add: bind_pmf_def cong: map_pmf_cong) + +lemma bind_pmf_cong_simp: + "\ p = q; \x. x \ set_pmf q =simp=> f x = g x \ + \ bind_pmf p f = bind_pmf q g" +by(simp add: simp_implies_def cong: bind_pmf_cong) + definition "pair_pmf A B = bind_pmf A (\x. bind_pmf B (\y. return_pmf (x, y)))" lemma pmf_pair: "pmf (pair_pmf M N) (a, b) = pmf M a * pmf N b" @@ -1235,5 +1251,38 @@ map_pair) qed +lemma rel_pmf_reflI: + assumes "\x. x \ set_pmf p \ P x x" + shows "rel_pmf P p p" +by(rule rel_pmf.intros[where pq="map_pmf (\x. (x, x)) p"])(auto simp add: pmf.map_comp o_def set_map_pmf assms) + +lemma rel_pmf_joinI: + assumes "rel_pmf (rel_pmf P) p q" + shows "rel_pmf P (join_pmf p) (join_pmf q)" +proof - + from assms obtain pq where p: "p = map_pmf fst pq" + and q: "q = map_pmf snd pq" + and P: "\x y. (x, y) \ set_pmf pq \ rel_pmf P x y" + by cases auto + from P obtain PQ + where PQ: "\x y a b. \ (x, y) \ set_pmf pq; (a, b) \ set_pmf (PQ x y) \ \ P a b" + and x: "\x y. (x, y) \ set_pmf pq \ map_pmf fst (PQ x y) = x" + and y: "\x y. (x, y) \ set_pmf pq \ map_pmf snd (PQ x y) = y" + by(metis rel_pmf.simps) + + let ?r = "bind_pmf pq (\(x, y). PQ x y)" + have "\a b. (a, b) \ set_pmf ?r \ P a b" by(auto simp add: set_bind_pmf intro: PQ) + moreover have "map_pmf fst ?r = join_pmf p" "map_pmf snd ?r = join_pmf q" + by(simp_all add: bind_pmf_def map_join_pmf pmf.map_comp o_def split_def p q x y cong: pmf.map_cong) + ultimately show ?thesis .. +qed + +lemma rel_pmf_bindI: + assumes pq: "rel_pmf R p q" + and fg: "\x y. R x y \ rel_pmf P (f x) (g y)" + shows "rel_pmf P (bind_pmf p f) (bind_pmf q g)" +unfolding bind_pmf_def +by(rule rel_pmf_joinI)(auto simp add: pmf.rel_map intro: pmf.rel_mono[THEN le_funD, THEN le_funD, THEN le_boolD, THEN mp, OF _ pq] fg) + end