src/HOL/Probability/Probability_Mass_Function.thy
changeset 58730 b3fd0628f849
parent 58606 9c66f7c541fb
child 59000 6eb0725503fc
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Mon Oct 20 18:33:14 2014 +0200
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Oct 21 17:00:42 2014 +0200
     1.3 @@ -234,7 +234,7 @@
     1.4  end
     1.5  
     1.6  lemma embed_pmf_transfer:
     1.7 -  "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"
     1.8 +  "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"
     1.9    by (auto simp: rel_fun_def eq_onp_def embed_pmf.transfer)
    1.10  
    1.11  lemma td_pmf_embed_pmf:
    1.12 @@ -263,6 +263,13 @@
    1.13  
    1.14  setup_lifting td_pmf_embed_pmf
    1.15  
    1.16 +lemma set_pmf_transfer[transfer_rule]: 
    1.17 +  assumes "bi_total A"
    1.18 +  shows "rel_fun (pcr_pmf A) (rel_set A) (\<lambda>f. {x. f x \<noteq> 0}) set_pmf"  
    1.19 +  using `bi_total A`
    1.20 +  by (auto simp: pcr_pmf_def cr_pmf_def rel_fun_def rel_set_def bi_total_def Bex_def set_pmf_iff)
    1.21 +     metis+
    1.22 +
    1.23  end 
    1.24  
    1.25  (*