rel_pmf preserves orders
authorAndreas Lochbihler
Wed Feb 11 18:39:56 2015 +0100 (2015-02-11)
changeset 59527edaabc1ab1ed
parent 59526 af02440afb4a
child 59528 4862f3dc9540
rel_pmf preserves orders
src/HOL/Probability/Probability_Mass_Function.thy
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Wed Feb 11 18:38:34 2015 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Wed Feb 11 18:39:56 2015 +0100
     1.3 @@ -1287,5 +1287,107 @@
     1.4  unfolding bind_pmf_def
     1.5  by(rule rel_pmf_joinI)(auto simp add: pmf.rel_map intro: pmf.rel_mono[THEN le_funD, THEN le_funD, THEN le_boolD, THEN mp, OF _ pq] fg)
     1.6  
     1.7 +text {*
     1.8 +  Proof that @{const rel_pmf} preserves orders.
     1.9 +  Antisymmetry proof follows Thm. 1 in N. Saheb-Djahromi, Cpo's of measures for nondeterminism, 
    1.10 +  Theoretical Computer Science 12(1):19--37, 1980, 
    1.11 +  @{url "http://dx.doi.org/10.1016/0304-3975(80)90003-1"}
    1.12 +*}
    1.13 +
    1.14 +lemma 
    1.15 +  assumes *: "rel_pmf R p q"
    1.16 +  and refl: "reflp R" and trans: "transp R"
    1.17 +  shows measure_Ici: "measure p {y. R x y} \<le> measure q {y. R x y}" (is ?thesis1)
    1.18 +  and measure_Ioi: "measure p {y. R x y \<and> \<not> R y x} \<le> measure q {y. R x y \<and> \<not> R y x}" (is ?thesis2)
    1.19 +proof -
    1.20 +  from * obtain pq
    1.21 +    where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y"
    1.22 +    and p: "p = map_pmf fst pq"
    1.23 +    and q: "q = map_pmf snd pq"
    1.24 +    by cases auto
    1.25 +  show ?thesis1 ?thesis2 unfolding p q map_pmf.rep_eq using refl trans
    1.26 +    by(auto 4 3 simp add: measure_distr reflpD AE_measure_pmf_iff intro!: measure_pmf.finite_measure_mono_AE dest!: pq elim: transpE)
    1.27 +qed
    1.28 +
    1.29 +lemma rel_pmf_inf:
    1.30 +  fixes p q :: "'a pmf"
    1.31 +  assumes 1: "rel_pmf R p q"
    1.32 +  assumes 2: "rel_pmf R q p"
    1.33 +  and refl: "reflp R" and trans: "transp R"
    1.34 +  shows "rel_pmf (inf R R\<inverse>\<inverse>) p q"
    1.35 +proof
    1.36 +  let ?E = "\<lambda>x. {y. R x y \<and> R y x}"
    1.37 +  let ?\<mu>E = "\<lambda>x. measure q (?E x)"
    1.38 +  { fix x
    1.39 +    have "measure p (?E x) = measure p ({y. R x y} - {y. R x y \<and> \<not> R y x})"
    1.40 +      by(auto intro!: arg_cong[where f="measure p"])
    1.41 +    also have "\<dots> = measure p {y. R x y} - measure p {y. R x y \<and> \<not> R y x}"
    1.42 +      by (rule measure_pmf.finite_measure_Diff) auto
    1.43 +    also have "measure p {y. R x y \<and> \<not> R y x} = measure q {y. R x y \<and> \<not> R y x}"
    1.44 +      using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ioi)
    1.45 +    also have "measure p {y. R x y} = measure q {y. R x y}"
    1.46 +      using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ici)
    1.47 +    also have "measure q {y. R x y} - measure q {y. R x y \<and> ~ R y x} =
    1.48 +      measure q ({y. R x y} - {y. R x y \<and> \<not> R y x})"
    1.49 +      by(rule measure_pmf.finite_measure_Diff[symmetric]) auto
    1.50 +    also have "\<dots> = ?\<mu>E x"
    1.51 +      by(auto intro!: arg_cong[where f="measure q"])
    1.52 +    also note calculation }
    1.53 +  note eq = this
    1.54 +
    1.55 +  def pq \<equiv> "bind_pmf p (\<lambda>x. bind_pmf (cond_pmf q (?E x)) (\<lambda>y. return_pmf (x, y)))"
    1.56 +
    1.57 +  show "map_pmf fst pq = p"
    1.58 +    by(simp add: pq_def map_bind_pmf map_return_pmf bind_return_pmf')
    1.59 +
    1.60 +  show "map_pmf snd pq = q"
    1.61 +    unfolding pq_def map_bind_pmf map_return_pmf bind_return_pmf' snd_conv
    1.62 +    by(subst bind_cond_pmf_cancel)(auto simp add: reflpD[OF \<open>reflp R\<close>] eq  intro: transpD[OF \<open>transp R\<close>])
    1.63 +
    1.64 +  fix x y
    1.65 +  assume "(x, y) \<in> set_pmf pq"
    1.66 +  moreover
    1.67 +  { assume "x \<in> set_pmf p"
    1.68 +    hence "measure (measure_pmf p) (?E x) \<noteq> 0"
    1.69 +      by(auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff intro: reflpD[OF \<open>reflp R\<close>])
    1.70 +    hence "measure (measure_pmf q) (?E x) \<noteq> 0" using eq by simp
    1.71 +    hence "set_pmf q \<inter> {y. R x y \<and> R y x} \<noteq> {}" 
    1.72 +      by(auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff) }
    1.73 +  ultimately show "inf R R\<inverse>\<inverse> x y"
    1.74 +    by(auto simp add: pq_def set_bind_pmf set_return_pmf set_cond_pmf)
    1.75 +qed
    1.76 +
    1.77 +lemma rel_pmf_antisym:
    1.78 +  fixes p q :: "'a pmf"
    1.79 +  assumes 1: "rel_pmf R p q"
    1.80 +  assumes 2: "rel_pmf R q p"
    1.81 +  and refl: "reflp R" and trans: "transp R" and antisym: "antisymP R"
    1.82 +  shows "p = q"
    1.83 +proof -
    1.84 +  from 1 2 refl trans have "rel_pmf (inf R R\<inverse>\<inverse>) p q" by(rule rel_pmf_inf)
    1.85 +  also have "inf R R\<inverse>\<inverse> = op ="
    1.86 +    using refl antisym by(auto intro!: ext simp add: reflpD dest: antisymD)
    1.87 +  finally show ?thesis unfolding pmf.rel_eq .
    1.88 +qed
    1.89 +
    1.90 +lemma reflp_rel_pmf: "reflp R \<Longrightarrow> reflp (rel_pmf R)"
    1.91 +by(blast intro: reflpI rel_pmf_reflI reflpD)
    1.92 +
    1.93 +lemma antisymP_rel_pmf:
    1.94 +  "\<lbrakk> reflp R; transp R; antisymP R \<rbrakk>
    1.95 +  \<Longrightarrow> antisymP (rel_pmf R)"
    1.96 +by(rule antisymI)(blast intro: rel_pmf_antisym)
    1.97 +
    1.98 +lemma transp_rel_pmf:
    1.99 +  assumes "transp R"
   1.100 +  shows "transp (rel_pmf R)"
   1.101 +proof (rule transpI)
   1.102 +  fix x y z
   1.103 +  assume "rel_pmf R x y" and "rel_pmf R y z"
   1.104 +  hence "rel_pmf (R OO R) x z" by (simp add: pmf.rel_compp relcompp.relcompI)
   1.105 +  thus "rel_pmf R x z"
   1.106 +    using assms by (metis (no_types) pmf.rel_mono rev_predicate2D transp_relcompp_less_eq)
   1.107 +qed
   1.108 +
   1.109  end
   1.110