# HG changeset patch
# User hoelzl
# Date 1422635391 -3600
# Node ID 8300c4ddf4938f94d7e103b876d2b2397a86160c
# Parent  4475b1a0141d682a02943d4e63221a1e41c281a4
simp rules for return_pmf

diff -r 4475b1a0141d -r 8300c4ddf493 src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Jan 30 17:29:41 2015 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Jan 30 17:29:51 2015 +0100
@@ -717,6 +717,9 @@
 
 end
 
+lemma return_pmf_inj[simp]: "return_pmf x = return_pmf y \<longleftrightarrow> x = y"
+  by (metis insertI1 set_return_pmf singletonD)
+
 definition "bind_pmf M f = join_pmf (map_pmf f M)"
 
 lemma (in pmf_as_measure) bind_transfer[transfer_rule]:
@@ -1133,6 +1136,12 @@
 lemma rel_pmf_return_pmf2: "rel_pmf R M (return_pmf x) \<longleftrightarrow> (\<forall>a\<in>M. R a x)"
   by (subst pmf.rel_flip[symmetric]) (simp add: rel_pmf_return_pmf1)
 
+lemma rel_return_pmf[simp]: "rel_pmf R (return_pmf x1) (return_pmf x2) = R x1 x2"
+  unfolding rel_pmf_return_pmf2 set_return_pmf by simp
+
+lemma rel_pmf_False[simp]: "rel_pmf (\<lambda>x y. False) x y = False"
+  unfolding pmf.in_rel fun_eq_iff using set_pmf_not_empty by fastforce
+
 lemma rel_pmf_rel_prod:
   "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'"
 proof safe