src/HOL/Probability/Probability_Mass_Function.thy
changeset 64634 5bd30359e46e
parent 64267 b9a1486e79be
child 65395 7504569a73c7
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Wed Dec 21 21:26:26 2016 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Thu Dec 22 08:43:30 2016 +0100
     1.3 @@ -1573,34 +1573,29 @@
     1.4    fixes p q :: "'a pmf"
     1.5    assumes 1: "rel_pmf R p q"
     1.6    assumes 2: "rel_pmf R q p"
     1.7 -  and refl: "reflp R" and trans: "transp R" and antisym: "antisymP R"
     1.8 +  and refl: "reflp R" and trans: "transp R" and antisym: "antisymp R"
     1.9    shows "p = q"
    1.10  proof -
    1.11    from 1 2 refl trans have "rel_pmf (inf R R\<inverse>\<inverse>) p q" by(rule rel_pmf_inf)
    1.12    also have "inf R R\<inverse>\<inverse> = op ="
    1.13 -    using refl antisym by (auto intro!: ext simp add: reflpD dest: antisymD)
    1.14 +    using refl antisym by (auto intro!: ext simp add: reflpD dest: antisympD)
    1.15    finally show ?thesis unfolding pmf.rel_eq .
    1.16  qed
    1.17  
    1.18  lemma reflp_rel_pmf: "reflp R \<Longrightarrow> reflp (rel_pmf R)"
    1.19 -by(blast intro: reflpI rel_pmf_reflI reflpD)
    1.20 +  by (fact pmf.rel_reflp)
    1.21  
    1.22 -lemma antisymP_rel_pmf:
    1.23 -  "\<lbrakk> reflp R; transp R; antisymP R \<rbrakk>
    1.24 -  \<Longrightarrow> antisymP (rel_pmf R)"
    1.25 -by(rule antisymI)(blast intro: rel_pmf_antisym)
    1.26 +lemma antisymp_rel_pmf:
    1.27 +  "\<lbrakk> reflp R; transp R; antisymp R \<rbrakk>
    1.28 +  \<Longrightarrow> antisymp (rel_pmf R)"
    1.29 +by(rule antisympI)(blast intro: rel_pmf_antisym)
    1.30  
    1.31  lemma transp_rel_pmf:
    1.32    assumes "transp R"
    1.33    shows "transp (rel_pmf R)"
    1.34 -proof (rule transpI)
    1.35 -  fix x y z
    1.36 -  assume "rel_pmf R x y" and "rel_pmf R y z"
    1.37 -  hence "rel_pmf (R OO R) x z" by (simp add: pmf.rel_compp relcompp.relcompI)
    1.38 -  thus "rel_pmf R x z"
    1.39 -    using assms by (metis (no_types) pmf.rel_mono rev_predicate2D transp_relcompp_less_eq)
    1.40 -qed
    1.41 +  using assms by (fact pmf.rel_transp)
    1.42  
    1.43 +    
    1.44  subsection \<open> Distributions \<close>
    1.45  
    1.46  context