# HG changeset patch
# User Andreas Lochbihler
# Date 1423676396 -3600
# Node ID edaabc1ab1ed5dd616f6306392bae35372973723
# Parent  af02440afb4a35899e86260e4a9f9da4b335c982
rel_pmf preserves orders

diff -r af02440afb4a -r edaabc1ab1ed src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Wed Feb 11 18:38:34 2015 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Wed Feb 11 18:39:56 2015 +0100
@@ -1287,5 +1287,107 @@
 unfolding bind_pmf_def
 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)
 
+text {*
+  Proof that @{const rel_pmf} preserves orders.
+  Antisymmetry proof follows Thm. 1 in N. Saheb-Djahromi, Cpo's of measures for nondeterminism, 
+  Theoretical Computer Science 12(1):19--37, 1980, 
+  @{url "http://dx.doi.org/10.1016/0304-3975(80)90003-1"}
+*}
+
+lemma 
+  assumes *: "rel_pmf R p q"
+  and refl: "reflp R" and trans: "transp R"
+  shows measure_Ici: "measure p {y. R x y} \<le> measure q {y. R x y}" (is ?thesis1)
+  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)
+proof -
+  from * obtain pq
+    where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y"
+    and p: "p = map_pmf fst pq"
+    and q: "q = map_pmf snd pq"
+    by cases auto
+  show ?thesis1 ?thesis2 unfolding p q map_pmf.rep_eq using refl trans
+    by(auto 4 3 simp add: measure_distr reflpD AE_measure_pmf_iff intro!: measure_pmf.finite_measure_mono_AE dest!: pq elim: transpE)
+qed
+
+lemma rel_pmf_inf:
+  fixes p q :: "'a pmf"
+  assumes 1: "rel_pmf R p q"
+  assumes 2: "rel_pmf R q p"
+  and refl: "reflp R" and trans: "transp R"
+  shows "rel_pmf (inf R R\<inverse>\<inverse>) p q"
+proof
+  let ?E = "\<lambda>x. {y. R x y \<and> R y x}"
+  let ?\<mu>E = "\<lambda>x. measure q (?E x)"
+  { fix x
+    have "measure p (?E x) = measure p ({y. R x y} - {y. R x y \<and> \<not> R y x})"
+      by(auto intro!: arg_cong[where f="measure p"])
+    also have "\<dots> = measure p {y. R x y} - measure p {y. R x y \<and> \<not> R y x}"
+      by (rule measure_pmf.finite_measure_Diff) auto
+    also have "measure p {y. R x y \<and> \<not> R y x} = measure q {y. R x y \<and> \<not> R y x}"
+      using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ioi)
+    also have "measure p {y. R x y} = measure q {y. R x y}"
+      using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ici)
+    also have "measure q {y. R x y} - measure q {y. R x y \<and> ~ R y x} =
+      measure q ({y. R x y} - {y. R x y \<and> \<not> R y x})"
+      by(rule measure_pmf.finite_measure_Diff[symmetric]) auto
+    also have "\<dots> = ?\<mu>E x"
+      by(auto intro!: arg_cong[where f="measure q"])
+    also note calculation }
+  note eq = this
+
+  def pq \<equiv> "bind_pmf p (\<lambda>x. bind_pmf (cond_pmf q (?E x)) (\<lambda>y. return_pmf (x, y)))"
+
+  show "map_pmf fst pq = p"
+    by(simp add: pq_def map_bind_pmf map_return_pmf bind_return_pmf')
+
+  show "map_pmf snd pq = q"
+    unfolding pq_def map_bind_pmf map_return_pmf bind_return_pmf' snd_conv
+    by(subst bind_cond_pmf_cancel)(auto simp add: reflpD[OF \<open>reflp R\<close>] eq  intro: transpD[OF \<open>transp R\<close>])
+
+  fix x y
+  assume "(x, y) \<in> set_pmf pq"
+  moreover
+  { assume "x \<in> set_pmf p"
+    hence "measure (measure_pmf p) (?E x) \<noteq> 0"
+      by(auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff intro: reflpD[OF \<open>reflp R\<close>])
+    hence "measure (measure_pmf q) (?E x) \<noteq> 0" using eq by simp
+    hence "set_pmf q \<inter> {y. R x y \<and> R y x} \<noteq> {}" 
+      by(auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff) }
+  ultimately show "inf R R\<inverse>\<inverse> x y"
+    by(auto simp add: pq_def set_bind_pmf set_return_pmf set_cond_pmf)
+qed
+
+lemma rel_pmf_antisym:
+  fixes p q :: "'a pmf"
+  assumes 1: "rel_pmf R p q"
+  assumes 2: "rel_pmf R q p"
+  and refl: "reflp R" and trans: "transp R" and antisym: "antisymP R"
+  shows "p = q"
+proof -
+  from 1 2 refl trans have "rel_pmf (inf R R\<inverse>\<inverse>) p q" by(rule rel_pmf_inf)
+  also have "inf R R\<inverse>\<inverse> = op ="
+    using refl antisym by(auto intro!: ext simp add: reflpD dest: antisymD)
+  finally show ?thesis unfolding pmf.rel_eq .
+qed
+
+lemma reflp_rel_pmf: "reflp R \<Longrightarrow> reflp (rel_pmf R)"
+by(blast intro: reflpI rel_pmf_reflI reflpD)
+
+lemma antisymP_rel_pmf:
+  "\<lbrakk> reflp R; transp R; antisymP R \<rbrakk>
+  \<Longrightarrow> antisymP (rel_pmf R)"
+by(rule antisymI)(blast intro: rel_pmf_antisym)
+
+lemma transp_rel_pmf:
+  assumes "transp R"
+  shows "transp (rel_pmf R)"
+proof (rule transpI)
+  fix x y z
+  assume "rel_pmf R x y" and "rel_pmf R y z"
+  hence "rel_pmf (R OO R) x z" by (simp add: pmf.rel_compp relcompp.relcompI)
+  thus "rel_pmf R x z"
+    using assms by (metis (no_types) pmf.rel_mono rev_predicate2D transp_relcompp_less_eq)
+qed
+
 end