# HG changeset patch
# User hoelzl
# Date 1425984992 -3600
# Node ID 37adca7fd48ff367a116f2ddaac77a619f055c56
# Parent  224741ede5ae1d604c82c0cdb8abb0df218c189c
add set_pmf lemmas to simpset

diff -r 224741ede5ae -r 37adca7fd48f src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Mar 10 10:53:48 2015 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Mar 10 11:56:32 2015 +0100
@@ -384,7 +384,7 @@
 lemma bind_pmf_const[simp]: "bind_pmf M (\<lambda>x. c) = c"
   by transfer (simp add: bind_const' prob_space_imp_subprob_space)
 
-lemma set_bind_pmf: "set_pmf (bind_pmf M N) = (\<Union>M\<in>set_pmf M. set_pmf (N M))"
+lemma set_bind_pmf[simp]: "set_pmf (bind_pmf M N) = (\<Union>M\<in>set_pmf M. set_pmf (N M))"
   unfolding set_pmf_eq ereal_eq_0(1)[symmetric] ereal_pmf_bind  
   by (auto simp add: nn_integral_0_iff_AE AE_measure_pmf_iff set_pmf_eq not_le less_le pmf_nonneg)
 
@@ -424,7 +424,7 @@
      (auto intro!: prob_space_imp_subprob_space bind_return[where N="count_space UNIV"]
            simp: space_subprob_algebra)
 
-lemma set_return_pmf: "set_pmf (return_pmf x) = {x}"
+lemma set_return_pmf[simp]: "set_pmf (return_pmf x) = {x}"
   by transfer (auto simp add: measure_return split: split_indicator)
 
 lemma bind_return_pmf': "bind_pmf N return_pmf = N"
@@ -477,9 +477,9 @@
   unfolding map_pmf_def by (rule bind_pmf_cong) auto
 
 lemma pmf_set_map: "set_pmf \<circ> map_pmf f = op ` f \<circ> set_pmf"
-  by (auto simp add: comp_def fun_eq_iff map_pmf_def set_bind_pmf set_return_pmf)
+  by (auto simp add: comp_def fun_eq_iff map_pmf_def)
 
-lemma set_map_pmf: "set_pmf (map_pmf f M) = f`set_pmf M"
+lemma set_map_pmf[simp]: "set_pmf (map_pmf f M) = f`set_pmf M"
   using pmf_set_map[of f] by (auto simp: comp_def fun_eq_iff)
 
 lemma emeasure_map_pmf[simp]: "emeasure (map_pmf f M) X = emeasure M (f -` X)"
@@ -529,6 +529,18 @@
 lemma return_pmf_inj[simp]: "return_pmf x = return_pmf y \<longleftrightarrow> x = y"
   by (metis insertI1 set_return_pmf singletonD)
 
+lemma map_pmf_eq_return_pmf_iff:
+  "map_pmf f p = return_pmf x \<longleftrightarrow> (\<forall>y \<in> set_pmf p. f y = x)"
+proof
+  assume "map_pmf f p = return_pmf x"
+  then have "set_pmf (map_pmf f p) = set_pmf (return_pmf x)" by simp
+  then show "\<forall>y \<in> set_pmf p. f y = x" by auto
+next
+  assume "\<forall>y \<in> set_pmf p. f y = x"
+  then show "map_pmf f p = return_pmf x"
+    unfolding map_pmf_const[symmetric, of _ p] by (intro map_pmf_cong) auto
+qed
+
 definition "pair_pmf A B = bind_pmf A (\<lambda>x. bind_pmf B (\<lambda>y. return_pmf (x, y)))"
 
 lemma pmf_pair: "pmf (pair_pmf M N) (a, b) = pmf M a * pmf N b"
@@ -539,7 +551,7 @@
   apply (auto simp: indicator_eq_0_iff setsum_nonneg_eq_0_iff pmf_nonneg)
   done
 
-lemma set_pair_pmf: "set_pmf (pair_pmf A B) = set_pmf A \<times> set_pmf B"
+lemma set_pair_pmf[simp]: "set_pmf (pair_pmf A B) = set_pmf A \<times> set_pmf B"
   unfolding pair_pmf_def set_bind_pmf set_return_pmf by auto
 
 lemma measure_pmf_in_subprob_space[measurable (raw)]:
@@ -550,7 +562,7 @@
 proof -
   have "(\<integral>\<^sup>+x. f x \<partial>pair_pmf A B) = (\<integral>\<^sup>+x. max 0 (f x) * indicator (A \<times> B) x \<partial>pair_pmf A B)"
     by (subst nn_integral_max_0[symmetric])
-       (auto simp: AE_measure_pmf_iff set_pair_pmf intro!: nn_integral_cong_AE)
+       (auto simp: AE_measure_pmf_iff intro!: nn_integral_cong_AE)
   also have "\<dots> = (\<integral>\<^sup>+a. \<integral>\<^sup>+b. max 0 (f (a, b)) * indicator (A \<times> B) (a, b) \<partial>B \<partial>A)"
     by (simp add: pair_pmf_def)
   also have "\<dots> = (\<integral>\<^sup>+a. \<integral>\<^sup>+b. max 0 (f (a, b)) \<partial>B \<partial>A)"
@@ -581,7 +593,7 @@
   then show "emeasure ?L X = emeasure ?R X"
     apply (simp add: emeasure_bind[OF _ M' X])
     apply (simp add: nn_integral_bind[where B="count_space UNIV"] pair_pmf_def measure_pmf_bind[of A]
-      nn_integral_measure_pmf_finite set_return_pmf emeasure_nonneg pmf_return one_ereal_def[symmetric])
+                     nn_integral_measure_pmf_finite emeasure_nonneg pmf_return one_ereal_def[symmetric])
     apply (subst emeasure_bind[OF _ _ X])
     apply measurable
     apply (subst emeasure_bind[OF _ _ X])
@@ -814,7 +826,7 @@
 lemma pmf_cond: "pmf cond_pmf x = (if x \<in> s then pmf p x / measure p s else 0)"
   by transfer (simp add: emeasure_measure_pmf_not_zero pmf.rep_eq)
 
-lemma set_cond_pmf: "set_pmf cond_pmf = set_pmf p \<inter> s"
+lemma set_cond_pmf[simp]: "set_pmf cond_pmf = set_pmf p \<inter> s"
   by (auto simp add: set_pmf_iff pmf_cond measure_measure_pmf_not_zero split: split_if_asm)
 
 end
@@ -824,7 +836,7 @@
   shows "cond_pmf (map_pmf f p) s = map_pmf f (cond_pmf p (f -` s))"
 proof -
   have *: "set_pmf (map_pmf f p) \<inter> s \<noteq> {}"
-    using assms by (simp add: set_map_pmf) auto
+    using assms by auto
   { fix x
     have "ereal (pmf (map_pmf f (cond_pmf p (f -` s))) x) =
       emeasure p (f -` s \<inter> f -` {x}) / emeasure p (f -` s)"
@@ -919,13 +931,13 @@
 
     def pr \<equiv> "bind_pmf pq (\<lambda>(x, y). bind_pmf (cond_pmf qr {(y', z). y' = y}) (\<lambda>(y', z). return_pmf (x, z)))"
     have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {(y', z). y' = y} \<noteq> {}"
-      by (force simp: q' set_map_pmf)
+      by (force simp: q')
 
     have "rel_pmf (R OO S) p r"
     proof (rule rel_pmf.intros)
       fix x z assume "(x, z) \<in> pr"
       then have "\<exists>y. (x, y) \<in> pq \<and> (y, z) \<in> qr"
-        by (auto simp: q pr_welldefined pr_def set_bind_pmf split_beta set_return_pmf set_cond_pmf set_map_pmf)
+        by (auto simp: q pr_welldefined pr_def split_beta)
       with pq qr show "(R OO S) x z"
         by blast
     next
@@ -938,6 +950,15 @@
     by(auto simp add: le_fun_def)
 qed (fact natLeq_card_order natLeq_cinfinite)+
 
+lemma rel_pmf_conj[simp]:
+  "rel_pmf (\<lambda>x y. P \<and> Q x y) x y \<longleftrightarrow> P \<and> rel_pmf Q x y"
+  "rel_pmf (\<lambda>x y. Q x y \<and> P) x y \<longleftrightarrow> P \<and> rel_pmf Q x y"
+  using set_pmf_not_empty by (fastforce simp: pmf.in_rel subset_eq)+
+
+lemma rel_pmf_top[simp]: "rel_pmf top = top"
+  by (auto simp: pmf.in_rel[abs_def] fun_eq_iff map_fst_pair_pmf map_snd_pair_pmf
+           intro: exI[of _ "pair_pmf x y" for x y])
+
 lemma rel_pmf_return_pmf1: "rel_pmf R (return_pmf x) M \<longleftrightarrow> (\<forall>a\<in>M. R x a)"
 proof safe
   fix a assume "a \<in> M" "rel_pmf R (return_pmf x) M"
@@ -945,13 +966,13 @@
     and eq: "return_pmf x = map_pmf fst pq" "M = map_pmf snd pq"
     by (force elim: rel_pmf.cases)
   moreover have "set_pmf (return_pmf x) = {x}"
-    by (simp add: set_return_pmf)
+    by simp
   with `a \<in> M` have "(x, a) \<in> pq"
-    by (force simp: eq set_map_pmf)
+    by (force simp: eq)
   with * show "R x a"
     by auto
 qed (auto intro!: rel_pmf.intros[where pq="pair_pmf (return_pmf x) M"]
-          simp: map_fst_pair_pmf map_snd_pair_pmf set_pair_pmf set_return_pmf)
+          simp: map_fst_pair_pmf map_snd_pair_pmf)
 
 lemma rel_pmf_return_pmf2: "rel_pmf R M (return_pmf x) \<longleftrightarrow> (\<forall>a\<in>M. R a x)"
   by (subst pmf.rel_flip[symmetric]) (simp add: rel_pmf_return_pmf1)
@@ -982,7 +1003,7 @@
 
     fix a b assume "(a, b) \<in> set_pmf (map_pmf ?f pq)"
     then obtain c d where "((a, c), (b, d)) \<in> set_pmf pq"
-      by (auto simp: set_map_pmf)
+      by auto
     from pq[OF this] show "R a b" ..
   qed
   show "rel_pmf S A' B'"
@@ -998,7 +1019,7 @@
 
     fix c d assume "(c, d) \<in> set_pmf (map_pmf ?f pq)"
     then obtain a b where "((a, c), (b, d)) \<in> set_pmf pq"
-      by (auto simp: set_map_pmf)
+      by auto
     from pq[OF this] show "S c d" ..
   qed
 next
@@ -1017,14 +1038,15 @@
 
   show "rel_pmf (rel_prod R S) (pair_pmf A A') (pair_pmf B B')"
     by (rule rel_pmf.intros[where pq="?pq"])
-       (auto simp: map_snd_pair_pmf map_fst_pair_pmf set_pair_pmf set_map_pmf map_pmf_comp Rpq Spq
+       (auto simp: map_snd_pair_pmf map_fst_pair_pmf map_pmf_comp Rpq Spq
                    map_pair)
 qed
 
 lemma rel_pmf_reflI: 
   assumes "\<And>x. x \<in> set_pmf p \<Longrightarrow> P x x"
   shows "rel_pmf P p p"
-by(rule rel_pmf.intros[where pq="map_pmf (\<lambda>x. (x, x)) p"])(auto simp add: pmf.map_comp o_def set_map_pmf assms)
+  by (rule rel_pmf.intros[where pq="map_pmf (\<lambda>x. (x, x)) p"])
+     (auto simp add: pmf.map_comp o_def assms)
 
 context
 begin
@@ -1045,8 +1067,8 @@
 lemma ereal_pmf_join: "ereal (pmf (join_pmf N) i) = (\<integral>\<^sup>+M. pmf M i \<partial>measure_pmf N)"
   unfolding join_pmf_def ereal_pmf_bind ..
 
-lemma set_pmf_join_pmf: "set_pmf (join_pmf f) = (\<Union>p\<in>set_pmf f. set_pmf p)"
-  by (simp add: join_pmf_def set_bind_pmf)
+lemma set_pmf_join_pmf[simp]: "set_pmf (join_pmf f) = (\<Union>p\<in>set_pmf f. set_pmf p)"
+  by (simp add: join_pmf_def)
 
 lemma join_return_pmf: "join_pmf (return_pmf M) = M"
   by (simp add: integral_return pmf_eq_iff pmf_join return_pmf.rep_eq)
@@ -1074,7 +1096,7 @@
     by(metis rel_pmf.simps)
 
   let ?r = "bind_pmf pq (\<lambda>(x, y). PQ x y)"
-  have "\<And>a b. (a, b) \<in> set_pmf ?r \<Longrightarrow> P a b" by(auto simp add: set_bind_pmf intro: PQ)
+  have "\<And>a b. (a, b) \<in> set_pmf ?r \<Longrightarrow> P a b" by (auto intro: PQ)
   moreover have "map_pmf fst ?r = join_pmf p" "map_pmf snd ?r = join_pmf q"
     by (simp_all add: p q x y join_pmf_def map_bind_pmf bind_map_pmf split_def cong: bind_pmf_cong)
   ultimately show ?thesis ..
@@ -1150,12 +1172,12 @@
   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>])
+      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) }
+      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)
+    by (auto simp add: pq_def)
 qed
 
 lemma rel_pmf_antisym:
@@ -1167,7 +1189,7 @@
 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)
+    using refl antisym by (auto intro!: ext simp add: reflpD dest: antisymD)
   finally show ?thesis unfolding pmf.rel_eq .
 qed