equal
deleted
inserted
replaced
1773 by (simp add: set_pmf_binomial_eq) |
1773 by (simp add: set_pmf_binomial_eq) |
1774 |
1774 |
1775 lemma set_pmf_binomial[simp]: "0 < p \<Longrightarrow> p < 1 \<Longrightarrow> set_pmf (binomial_pmf n p) = {..n}" |
1775 lemma set_pmf_binomial[simp]: "0 < p \<Longrightarrow> p < 1 \<Longrightarrow> set_pmf (binomial_pmf n p) = {..n}" |
1776 by (simp add: set_pmf_binomial_eq) |
1776 by (simp add: set_pmf_binomial_eq) |
1777 |
1777 |
1778 context begin interpretation lifting_syntax . |
1778 context includes lifting_syntax |
|
1779 begin |
1779 |
1780 |
1780 lemma bind_pmf_parametric [transfer_rule]: |
1781 lemma bind_pmf_parametric [transfer_rule]: |
1781 "(rel_pmf A ===> (A ===> rel_pmf B) ===> rel_pmf B) bind_pmf bind_pmf" |
1782 "(rel_pmf A ===> (A ===> rel_pmf B) ===> rel_pmf B) bind_pmf bind_pmf" |
1782 by(blast intro: rel_pmf_bindI dest: rel_funD) |
1783 by(blast intro: rel_pmf_bindI dest: rel_funD) |
1783 |
1784 |