src/HOL/Probability/Probability_Mass_Function.thy
changeset 64634 5bd30359e46e
parent 64267 b9a1486e79be
child 65395 7504569a73c7
equal deleted inserted replaced
64633:5ebcf6c525f1 64634:5bd30359e46e
  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