simp rules for return_pmf
authorhoelzl
Fri Jan 30 17:29:51 2015 +0100 (2015-01-30)
changeset 594758300c4ddf493
parent 59474 4475b1a0141d
child 59476 90f5bab83c31
simp rules for return_pmf
src/HOL/Probability/Probability_Mass_Function.thy
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Jan 30 17:29:41 2015 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Jan 30 17:29:51 2015 +0100
     1.3 @@ -717,6 +717,9 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma return_pmf_inj[simp]: "return_pmf x = return_pmf y \<longleftrightarrow> x = y"
     1.8 +  by (metis insertI1 set_return_pmf singletonD)
     1.9 +
    1.10  definition "bind_pmf M f = join_pmf (map_pmf f M)"
    1.11  
    1.12  lemma (in pmf_as_measure) bind_transfer[transfer_rule]:
    1.13 @@ -1133,6 +1136,12 @@
    1.14  lemma rel_pmf_return_pmf2: "rel_pmf R M (return_pmf x) \<longleftrightarrow> (\<forall>a\<in>M. R a x)"
    1.15    by (subst pmf.rel_flip[symmetric]) (simp add: rel_pmf_return_pmf1)
    1.16  
    1.17 +lemma rel_return_pmf[simp]: "rel_pmf R (return_pmf x1) (return_pmf x2) = R x1 x2"
    1.18 +  unfolding rel_pmf_return_pmf2 set_return_pmf by simp
    1.19 +
    1.20 +lemma rel_pmf_False[simp]: "rel_pmf (\<lambda>x y. False) x y = False"
    1.21 +  unfolding pmf.in_rel fun_eq_iff using set_pmf_not_empty by fastforce
    1.22 +
    1.23  lemma rel_pmf_rel_prod:
    1.24    "rel_pmf (rel_prod R S) (pair_pmf A A') (pair_pmf B B') \<longleftrightarrow> rel_pmf R A B \<and> rel_pmf S A' B'"
    1.25  proof safe