1571 |
1571 |
1572 lemma rel_pmf_antisym: |
1572 lemma rel_pmf_antisym: |
1573 fixes p q :: "'a pmf" |
1573 fixes p q :: "'a pmf" |
1574 assumes 1: "rel_pmf R p q" |
1574 assumes 1: "rel_pmf R p q" |
1575 assumes 2: "rel_pmf R q p" |
1575 assumes 2: "rel_pmf R q p" |
1576 and refl: "reflp R" and trans: "transp R" and antisym: "antisymP R" |
1576 and refl: "reflp R" and trans: "transp R" and antisym: "antisymp R" |
1577 shows "p = q" |
1577 shows "p = q" |
1578 proof - |
1578 proof - |
1579 from 1 2 refl trans have "rel_pmf (inf R R\<inverse>\<inverse>) p q" by(rule rel_pmf_inf) |
1579 from 1 2 refl trans have "rel_pmf (inf R R\<inverse>\<inverse>) p q" by(rule rel_pmf_inf) |
1580 also have "inf R R\<inverse>\<inverse> = op =" |
1580 also have "inf R R\<inverse>\<inverse> = op =" |
1581 using refl antisym by (auto intro!: ext simp add: reflpD dest: antisymD) |
1581 using refl antisym by (auto intro!: ext simp add: reflpD dest: antisympD) |
1582 finally show ?thesis unfolding pmf.rel_eq . |
1582 finally show ?thesis unfolding pmf.rel_eq . |
1583 qed |
1583 qed |
1584 |
1584 |
1585 lemma reflp_rel_pmf: "reflp R \<Longrightarrow> reflp (rel_pmf R)" |
1585 lemma reflp_rel_pmf: "reflp R \<Longrightarrow> reflp (rel_pmf R)" |
1586 by(blast intro: reflpI rel_pmf_reflI reflpD) |
1586 by (fact pmf.rel_reflp) |
1587 |
1587 |
1588 lemma antisymP_rel_pmf: |
1588 lemma antisymp_rel_pmf: |
1589 "\<lbrakk> reflp R; transp R; antisymP R \<rbrakk> |
1589 "\<lbrakk> reflp R; transp R; antisymp R \<rbrakk> |
1590 \<Longrightarrow> antisymP (rel_pmf R)" |
1590 \<Longrightarrow> antisymp (rel_pmf R)" |
1591 by(rule antisymI)(blast intro: rel_pmf_antisym) |
1591 by(rule antisympI)(blast intro: rel_pmf_antisym) |
1592 |
1592 |
1593 lemma transp_rel_pmf: |
1593 lemma transp_rel_pmf: |
1594 assumes "transp R" |
1594 assumes "transp R" |
1595 shows "transp (rel_pmf R)" |
1595 shows "transp (rel_pmf R)" |
1596 proof (rule transpI) |
1596 using assms by (fact pmf.rel_transp) |
1597 fix x y z |
1597 |
1598 assume "rel_pmf R x y" and "rel_pmf R y z" |
1598 |
1599 hence "rel_pmf (R OO R) x z" by (simp add: pmf.rel_compp relcompp.relcompI) |
|
1600 thus "rel_pmf R x z" |
|
1601 using assms by (metis (no_types) pmf.rel_mono rev_predicate2D transp_relcompp_less_eq) |
|
1602 qed |
|
1603 |
|
1604 subsection \<open> Distributions \<close> |
1599 subsection \<open> Distributions \<close> |
1605 |
1600 |
1606 context |
1601 context |
1607 begin |
1602 begin |
1608 |
1603 |