rel_pmf on equivalence relation
authorhoelzl
Thu Mar 12 19:09:18 2015 +0100 (2015-03-12)
changeset 59681f24ab09e4c37
parent 59680 034a4d15b52e
child 59686 68996aa77829
rel_pmf on equivalence relation
src/HOL/Probability/Probability_Mass_Function.thy
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Thu Mar 12 14:08:47 2015 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Thu Mar 12 19:09:18 2015 +0100
     1.3 @@ -884,6 +884,136 @@
     1.4       map_pmf fst pq = p; map_pmf snd pq = q \<rbrakk>
     1.5    \<Longrightarrow> rel_pmf R p q"
     1.6  
     1.7 +lemma rel_pmfI:
     1.8 +  assumes R: "rel_set R (set_pmf p) (set_pmf q)"
     1.9 +  assumes eq: "\<And>x y. x \<in> set_pmf p \<Longrightarrow> y \<in> set_pmf q \<Longrightarrow> R x y \<Longrightarrow>
    1.10 +    measure p {x. R x y} = measure q {y. R x y}"
    1.11 +  shows "rel_pmf R p q"
    1.12 +proof
    1.13 +  let ?pq = "bind_pmf p (\<lambda>x. bind_pmf (cond_pmf q {y. R x y}) (\<lambda>y. return_pmf (x, y)))"
    1.14 +  have "\<And>x. x \<in> set_pmf p \<Longrightarrow> set_pmf q \<inter> {y. R x y} \<noteq> {}"
    1.15 +    using R by (auto simp: rel_set_def)
    1.16 +  then show "\<And>x y. (x, y) \<in> set_pmf ?pq \<Longrightarrow> R x y"
    1.17 +    by auto
    1.18 +  show "map_pmf fst ?pq = p"
    1.19 +    by (simp add: map_bind_pmf map_return_pmf bind_return_pmf')
    1.20 +
    1.21 +  show "map_pmf snd ?pq = q"
    1.22 +    using R eq
    1.23 +    apply (simp add: bind_cond_pmf_cancel map_bind_pmf map_return_pmf bind_return_pmf')
    1.24 +    apply (rule bind_cond_pmf_cancel)
    1.25 +    apply (auto simp: rel_set_def)
    1.26 +    done
    1.27 +qed
    1.28 +
    1.29 +lemma rel_pmf_imp_rel_set: "rel_pmf R p q \<Longrightarrow> rel_set R (set_pmf p) (set_pmf q)"
    1.30 +  by (force simp add: rel_pmf.simps rel_set_def)
    1.31 +
    1.32 +lemma rel_pmfD_measure:
    1.33 +  assumes rel_R: "rel_pmf R p q" and R: "\<And>a b. R a b \<Longrightarrow> R a y \<longleftrightarrow> R x b"
    1.34 +  assumes "x \<in> set_pmf p" "y \<in> set_pmf q"
    1.35 +  shows "measure p {x. R x y} = measure q {y. R x y}"
    1.36 +proof -
    1.37 +  from rel_R obtain pq where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y"
    1.38 +    and eq: "p = map_pmf fst pq" "q = map_pmf snd pq"
    1.39 +    by (auto elim: rel_pmf.cases)
    1.40 +  have "measure p {x. R x y} = measure pq {x. R (fst x) y}"
    1.41 +    by (simp add: eq map_pmf_rep_eq measure_distr)
    1.42 +  also have "\<dots> = measure pq {y. R x (snd y)}"
    1.43 +    by (intro measure_pmf.finite_measure_eq_AE)
    1.44 +       (auto simp: AE_measure_pmf_iff R dest!: pq)
    1.45 +  also have "\<dots> = measure q {y. R x y}"
    1.46 +    by (simp add: eq map_pmf_rep_eq measure_distr)
    1.47 +  finally show "measure p {x. R x y} = measure q {y. R x y}" .
    1.48 +qed
    1.49 +
    1.50 +lemma rel_pmf_iff_measure:
    1.51 +  assumes "symp R" "transp R"
    1.52 +  shows "rel_pmf R p q \<longleftrightarrow>
    1.53 +    rel_set R (set_pmf p) (set_pmf q) \<and>
    1.54 +    (\<forall>x\<in>set_pmf p. \<forall>y\<in>set_pmf q. R x y \<longrightarrow> measure p {x. R x y} = measure q {y. R x y})"
    1.55 +  by (safe intro!: rel_pmf_imp_rel_set rel_pmfI)
    1.56 +     (auto intro!: rel_pmfD_measure dest: sympD[OF \<open>symp R\<close>] transpD[OF \<open>transp R\<close>])
    1.57 +
    1.58 +lemma quotient_rel_set_disjoint:
    1.59 +  "equivp R \<Longrightarrow> C \<in> UNIV // {(x, y). R x y} \<Longrightarrow> rel_set R A B \<Longrightarrow> A \<inter> C = {} \<longleftrightarrow> B \<inter> C = {}"
    1.60 +  using in_quotient_imp_closed[of UNIV "{(x, y). R x y}" C] 
    1.61 +  by (auto 0 0 simp: equivp_equiv rel_set_def set_eq_iff elim: equivpE)
    1.62 +     (blast dest: equivp_symp)+
    1.63 +
    1.64 +lemma quotientD: "equiv X R \<Longrightarrow> A \<in> X // R \<Longrightarrow> x \<in> A \<Longrightarrow> A = R `` {x}"
    1.65 +  by (metis Image_singleton_iff equiv_class_eq_iff quotientE)
    1.66 +
    1.67 +lemma rel_pmf_iff_equivp:
    1.68 +  assumes "equivp R"
    1.69 +  shows "rel_pmf R p q \<longleftrightarrow> (\<forall>C\<in>UNIV // {(x, y). R x y}. measure p C = measure q C)"
    1.70 +    (is "_ \<longleftrightarrow>   (\<forall>C\<in>_//?R. _)")
    1.71 +proof (subst rel_pmf_iff_measure, safe)
    1.72 +  show "symp R" "transp R"
    1.73 +    using assms by (auto simp: equivp_reflp_symp_transp)
    1.74 +next
    1.75 +  fix C assume C: "C \<in> UNIV // ?R" and R: "rel_set R (set_pmf p) (set_pmf q)"
    1.76 +  assume eq: "\<forall>x\<in>set_pmf p. \<forall>y\<in>set_pmf q. R x y \<longrightarrow> measure p {x. R x y} = measure q {y. R x y}"
    1.77 +  
    1.78 +  show "measure p C = measure q C"
    1.79 +  proof cases
    1.80 +    assume "p \<inter> C = {}"
    1.81 +    moreover then have "q \<inter> C = {}"  
    1.82 +      using quotient_rel_set_disjoint[OF assms C R] by simp
    1.83 +    ultimately show ?thesis
    1.84 +      unfolding measure_pmf_zero_iff[symmetric] by simp
    1.85 +  next
    1.86 +    assume "p \<inter> C \<noteq> {}"
    1.87 +    moreover then have "q \<inter> C \<noteq> {}"  
    1.88 +      using quotient_rel_set_disjoint[OF assms C R] by simp
    1.89 +    ultimately obtain x y where in_set: "x \<in> set_pmf p" "y \<in> set_pmf q" and in_C: "x \<in> C" "y \<in> C"
    1.90 +      by auto
    1.91 +    then have "R x y"
    1.92 +      using in_quotient_imp_in_rel[of UNIV ?R C x y] C assms
    1.93 +      by (simp add: equivp_equiv)
    1.94 +    with in_set eq have "measure p {x. R x y} = measure q {y. R x y}"
    1.95 +      by auto
    1.96 +    moreover have "{y. R x y} = C"
    1.97 +      using assms `x \<in> C` C quotientD[of UNIV ?R C x] by (simp add: equivp_equiv)
    1.98 +    moreover have "{x. R x y} = C"
    1.99 +      using assms `y \<in> C` C quotientD[of UNIV "?R" C y] sympD[of R]
   1.100 +      by (auto simp add: equivp_equiv elim: equivpE)
   1.101 +    ultimately show ?thesis
   1.102 +      by auto
   1.103 +  qed
   1.104 +next
   1.105 +  assume eq: "\<forall>C\<in>UNIV // ?R. measure p C = measure q C"
   1.106 +  show "rel_set R (set_pmf p) (set_pmf q)"
   1.107 +    unfolding rel_set_def
   1.108 +  proof safe
   1.109 +    fix x assume x: "x \<in> set_pmf p"
   1.110 +    have "{y. R x y} \<in> UNIV // ?R"
   1.111 +      by (auto simp: quotient_def)
   1.112 +    with eq have *: "measure q {y. R x y} = measure p {y. R x y}"
   1.113 +      by auto
   1.114 +    have "measure q {y. R x y} \<noteq> 0"
   1.115 +      using x assms unfolding * by (auto simp: measure_pmf_zero_iff set_eq_iff dest: equivp_reflp)
   1.116 +    then show "\<exists>y\<in>set_pmf q. R x y"
   1.117 +      unfolding measure_pmf_zero_iff by auto
   1.118 +  next
   1.119 +    fix y assume y: "y \<in> set_pmf q"
   1.120 +    have "{x. R x y} \<in> UNIV // ?R"
   1.121 +      using assms by (auto simp: quotient_def dest: equivp_symp)
   1.122 +    with eq have *: "measure p {x. R x y} = measure q {x. R x y}"
   1.123 +      by auto
   1.124 +    have "measure p {x. R x y} \<noteq> 0"
   1.125 +      using y assms unfolding * by (auto simp: measure_pmf_zero_iff set_eq_iff dest: equivp_reflp)
   1.126 +    then show "\<exists>x\<in>set_pmf p. R x y"
   1.127 +      unfolding measure_pmf_zero_iff by auto
   1.128 +  qed
   1.129 +
   1.130 +  fix x y assume "x \<in> set_pmf p" "y \<in> set_pmf q" "R x y"
   1.131 +  have "{y. R x y} \<in> UNIV // ?R" "{x. R x y} = {y. R x y}"
   1.132 +    using assms `R x y` by (auto simp: quotient_def dest: equivp_symp equivp_transp)
   1.133 +  with eq show "measure p {x. R x y} = measure q {y. R x y}"
   1.134 +    by auto
   1.135 +qed
   1.136 +
   1.137  bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "natLeq" rel: rel_pmf
   1.138  proof -
   1.139    show "map_pmf id = id" by (rule map_pmf_id)
   1.140 @@ -912,7 +1042,7 @@
   1.141        and x: "x \<in> set_pmf p"
   1.142      thus "f x = g x" by simp }
   1.143  
   1.144 -  fix R :: "'a => 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
   1.145 +  fix R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
   1.146    { fix p q r
   1.147      assume pq: "rel_pmf R p q"
   1.148        and qr:"rel_pmf S q r"
   1.149 @@ -1130,46 +1260,31 @@
   1.150    assumes 2: "rel_pmf R q p"
   1.151    and refl: "reflp R" and trans: "transp R"
   1.152    shows "rel_pmf (inf R R\<inverse>\<inverse>) p q"
   1.153 -proof
   1.154 +proof (subst rel_pmf_iff_equivp, safe)
   1.155 +  show "equivp (inf R R\<inverse>\<inverse>)"
   1.156 +    using trans refl by (auto simp: equivp_reflp_symp_transp intro: sympI transpI reflpI dest: transpD reflpD)
   1.157 +  
   1.158 +  fix C assume "C \<in> UNIV // {(x, y). inf R R\<inverse>\<inverse> x y}"
   1.159 +  then obtain x where C: "C = {y. R x y \<and> R y x}"
   1.160 +    by (auto elim: quotientE)
   1.161 +
   1.162    let ?R = "\<lambda>x y. R x y \<and> R y x"
   1.163    let ?\<mu>R = "\<lambda>y. measure q {x. ?R x y}"
   1.164 -  { fix x
   1.165 -    have "measure p {y. ?R x y} = measure p ({y. R x y} - {y. R x y \<and> \<not> R y x})"
   1.166 -      by(auto intro!: arg_cong[where f="measure p"])
   1.167 -    also have "\<dots> = measure p {y. R x y} - measure p {y. R x y \<and> \<not> R y x}"
   1.168 -      by (rule measure_pmf.finite_measure_Diff) auto
   1.169 -    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.170 -      using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ioi)
   1.171 -    also have "measure p {y. R x y} = measure q {y. R x y}"
   1.172 -      using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ici)
   1.173 -    also have "measure q {y. R x y} - measure q {y. R x y \<and> ~ R y x} =
   1.174 -      measure q ({y. R x y} - {y. R x y \<and> \<not> R y x})"
   1.175 -      by(rule measure_pmf.finite_measure_Diff[symmetric]) auto
   1.176 -    also have "\<dots> = ?\<mu>R x"
   1.177 -      by(auto intro!: arg_cong[where f="measure q"])
   1.178 -    also note calculation }
   1.179 -  note eq = this
   1.180 -
   1.181 -  def pq \<equiv> "bind_pmf p (\<lambda>x. bind_pmf (cond_pmf q {y. ?R y x}) (\<lambda>y. return_pmf (x, y)))"
   1.182 -
   1.183 -  show "map_pmf fst pq = p"
   1.184 -    by(simp add: pq_def map_bind_pmf map_return_pmf bind_return_pmf')
   1.185 -
   1.186 -  { fix y assume "y \<in> set_pmf p" then have "set_pmf q \<inter> {x. ?R x y} \<noteq> {}"
   1.187 -      unfolding measure_pmf_zero_iff[symmetric] eq[symmetric] by (auto simp: measure_pmf_zero_iff intro: reflpD[OF refl]) }
   1.188 -  note set_p = this
   1.189 -  moreover
   1.190 -  { fix x assume "x \<in> set_pmf q" then have "set_pmf p \<inter> {y. R x y \<and> R y x} \<noteq> {}"
   1.191 -      unfolding measure_pmf_zero_iff[symmetric] eq by (auto simp: measure_pmf_zero_iff intro: reflpD[OF refl]) }
   1.192 -  ultimately
   1.193 -  show "map_pmf snd pq = q"
   1.194 -    unfolding pq_def map_bind_pmf map_return_pmf bind_return_pmf' snd_conv
   1.195 -    by (subst bind_cond_pmf_cancel)
   1.196 -       (auto simp add: eq AE_measure_pmf_iff dest: transpD[OF trans]
   1.197 -             intro!: measure_pmf.finite_measure_eq_AE)
   1.198 -
   1.199 -  fix x y assume "(x, y) \<in> set_pmf pq" with set_p show "inf R R\<inverse>\<inverse> x y"
   1.200 -    by (auto simp add: pq_def)
   1.201 +  have "measure p {y. ?R x y} = measure p ({y. R x y} - {y. R x y \<and> \<not> R y x})"
   1.202 +    by(auto intro!: arg_cong[where f="measure p"])
   1.203 +  also have "\<dots> = measure p {y. R x y} - measure p {y. R x y \<and> \<not> R y x}"
   1.204 +    by (rule measure_pmf.finite_measure_Diff) auto
   1.205 +  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.206 +    using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ioi)
   1.207 +  also have "measure p {y. R x y} = measure q {y. R x y}"
   1.208 +    using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ici)
   1.209 +  also have "measure q {y. R x y} - measure q {y. R x y \<and> \<not> R y x} =
   1.210 +    measure q ({y. R x y} - {y. R x y \<and> \<not> R y x})"
   1.211 +    by(rule measure_pmf.finite_measure_Diff[symmetric]) auto
   1.212 +  also have "\<dots> = ?\<mu>R x"
   1.213 +    by(auto intro!: arg_cong[where f="measure q"])
   1.214 +  finally show "measure p C = measure q C"
   1.215 +    by (simp add: C conj_commute)
   1.216  qed
   1.217  
   1.218  lemma rel_pmf_antisym: