# HG changeset patch
# User hoelzl
# Date 1413903642 -7200
# Node ID b3fd0628f84968fcb28c0d08d268c0961ac64abb
# Parent  e8ecc79aee432d084a1539f69bb95a656f4140fd
add transfer rule for set_pmf

diff -r e8ecc79aee43 -r b3fd0628f849 src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Mon Oct 20 18:33:14 2014 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Oct 21 17:00:42 2014 +0200
@@ -234,7 +234,7 @@
 end
 
 lemma embed_pmf_transfer:
-  "rel_fun (eq_onp (\<lambda>f::'a \<Rightarrow> real. (\<forall>x. 0 \<le> f x) \<and> (\<integral>\<^sup>+x. ereal (f x) \<partial>count_space UNIV) = 1)) pmf_as_measure.cr_pmf (\<lambda>f. density (count_space UNIV) (ereal \<circ> f)) embed_pmf"
+  "rel_fun (eq_onp (\<lambda>f. (\<forall>x. 0 \<le> f x) \<and> (\<integral>\<^sup>+x. ereal (f x) \<partial>count_space UNIV) = 1)) pmf_as_measure.cr_pmf (\<lambda>f. density (count_space UNIV) (ereal \<circ> f)) embed_pmf"
   by (auto simp: rel_fun_def eq_onp_def embed_pmf.transfer)
 
 lemma td_pmf_embed_pmf:
@@ -263,6 +263,13 @@
 
 setup_lifting td_pmf_embed_pmf
 
+lemma set_pmf_transfer[transfer_rule]: 
+  assumes "bi_total A"
+  shows "rel_fun (pcr_pmf A) (rel_set A) (\<lambda>f. {x. f x \<noteq> 0}) set_pmf"  
+  using `bi_total A`
+  by (auto simp: pcr_pmf_def cr_pmf_def rel_fun_def rel_set_def bi_total_def Bex_def set_pmf_iff)
+     metis+
+
 end 
 
 (*