src/HOL/Probability/Probability_Mass_Function.thy
changeset 60595 804dfdc82835
parent 60495 d7ff0a1df90a
child 60602 37588fbe39f9
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Jun 26 18:54:23 2015 +0200
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Sat Jun 27 00:10:24 2015 +0200
     1.3 @@ -1043,52 +1043,53 @@
     1.4    show "\<And>f::'a \<Rightarrow> 'b. set_pmf \<circ> map_pmf f = op ` f \<circ> set_pmf"
     1.5      by (rule pmf_set_map)
     1.6  
     1.7 -  { fix p :: "'s pmf"
     1.8 +  show "(card_of (set_pmf p), natLeq) \<in> ordLeq" for p :: "'s pmf"
     1.9 +  proof -
    1.10      have "(card_of (set_pmf p), card_of (UNIV :: nat set)) \<in> ordLeq"
    1.11        by (rule card_of_ordLeqI[where f="to_nat_on (set_pmf p)"])
    1.12           (auto intro: countable_set_pmf)
    1.13      also have "(card_of (UNIV :: nat set), natLeq) \<in> ordLeq"
    1.14        by (metis Field_natLeq card_of_least natLeq_Well_order)
    1.15 -    finally show "(card_of (set_pmf p), natLeq) \<in> ordLeq" . }
    1.16 +    finally show ?thesis .
    1.17 +  qed
    1.18  
    1.19    show "\<And>R. rel_pmf R =
    1.20           (BNF_Def.Grp {x. set_pmf x \<subseteq> {(x, y). R x y}} (map_pmf fst))\<inverse>\<inverse> OO
    1.21           BNF_Def.Grp {x. set_pmf x \<subseteq> {(x, y). R x y}} (map_pmf snd)"
    1.22       by (auto simp add: fun_eq_iff BNF_Def.Grp_def OO_def rel_pmf.simps)
    1.23  
    1.24 -  { fix p :: "'a pmf" and f :: "'a \<Rightarrow> 'b" and g x
    1.25 -    assume p: "\<And>z. z \<in> set_pmf p \<Longrightarrow> f z = g z"
    1.26 -      and x: "x \<in> set_pmf p"
    1.27 -    thus "f x = g x" by simp }
    1.28 -
    1.29 -  fix R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
    1.30 -  { fix p q r
    1.31 -    assume pq: "rel_pmf R p q"
    1.32 -      and qr:"rel_pmf S q r"
    1.33 -    from pq obtain pq where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y"
    1.34 -      and p: "p = map_pmf fst pq" and q: "q = map_pmf snd pq" by cases auto
    1.35 -    from qr obtain qr where qr: "\<And>y z. (y, z) \<in> set_pmf qr \<Longrightarrow> S y z"
    1.36 -      and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto
    1.37 -
    1.38 -    def pr \<equiv> "bind_pmf pq (\<lambda>xy. bind_pmf (cond_pmf qr {yz. fst yz = snd xy}) (\<lambda>yz. return_pmf (fst xy, snd yz)))"
    1.39 -    have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {yz. fst yz = y} \<noteq> {}"
    1.40 -      by (force simp: q')
    1.41 -
    1.42 -    have "rel_pmf (R OO S) p r"
    1.43 -    proof (rule rel_pmf.intros)
    1.44 -      fix x z assume "(x, z) \<in> pr"
    1.45 -      then have "\<exists>y. (x, y) \<in> pq \<and> (y, z) \<in> qr"
    1.46 -        by (auto simp: q pr_welldefined pr_def split_beta)
    1.47 -      with pq qr show "(R OO S) x z"
    1.48 -        by blast
    1.49 -    next
    1.50 -      have "map_pmf snd pr = map_pmf snd (bind_pmf q (\<lambda>y. cond_pmf qr {yz. fst yz = y}))"
    1.51 -        by (simp add: pr_def q split_beta bind_map_pmf map_pmf_def[symmetric] map_bind_pmf map_pmf_comp)
    1.52 -      then show "map_pmf snd pr = r"
    1.53 -        unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) (auto simp: eq_commute)
    1.54 -    qed (simp add: pr_def map_bind_pmf split_beta map_pmf_def[symmetric] p map_pmf_comp) }
    1.55 -  then show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)"
    1.56 -    by(auto simp add: le_fun_def)
    1.57 +  show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)"
    1.58 +    for R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
    1.59 +  proof -
    1.60 +    { fix p q r
    1.61 +      assume pq: "rel_pmf R p q"
    1.62 +        and qr:"rel_pmf S q r"
    1.63 +      from pq obtain pq where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y"
    1.64 +        and p: "p = map_pmf fst pq" and q: "q = map_pmf snd pq" by cases auto
    1.65 +      from qr obtain qr where qr: "\<And>y z. (y, z) \<in> set_pmf qr \<Longrightarrow> S y z"
    1.66 +        and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto
    1.67 +  
    1.68 +      def pr \<equiv> "bind_pmf pq (\<lambda>xy. bind_pmf (cond_pmf qr {yz. fst yz = snd xy}) (\<lambda>yz. return_pmf (fst xy, snd yz)))"
    1.69 +      have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {yz. fst yz = y} \<noteq> {}"
    1.70 +        by (force simp: q')
    1.71 +  
    1.72 +      have "rel_pmf (R OO S) p r"
    1.73 +      proof (rule rel_pmf.intros)
    1.74 +        fix x z assume "(x, z) \<in> pr"
    1.75 +        then have "\<exists>y. (x, y) \<in> pq \<and> (y, z) \<in> qr"
    1.76 +          by (auto simp: q pr_welldefined pr_def split_beta)
    1.77 +        with pq qr show "(R OO S) x z"
    1.78 +          by blast
    1.79 +      next
    1.80 +        have "map_pmf snd pr = map_pmf snd (bind_pmf q (\<lambda>y. cond_pmf qr {yz. fst yz = y}))"
    1.81 +          by (simp add: pr_def q split_beta bind_map_pmf map_pmf_def[symmetric] map_bind_pmf map_pmf_comp)
    1.82 +        then show "map_pmf snd pr = r"
    1.83 +          unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) (auto simp: eq_commute)
    1.84 +      qed (simp add: pr_def map_bind_pmf split_beta map_pmf_def[symmetric] p map_pmf_comp)
    1.85 +    }
    1.86 +    then show ?thesis
    1.87 +      by(auto simp add: le_fun_def)
    1.88 +  qed
    1.89  qed (fact natLeq_card_order natLeq_cinfinite)+
    1.90  
    1.91  lemma rel_pmf_conj[simp]: