projections of pair_pmf (by D. Traytel)
authorhoelzl
Tue Nov 25 17:29:39 2014 +0100 (2014-11-25)
changeset 59052a05c8305781e
parent 59051 d9e124f50d85
child 59053 43e07797269b
projections of pair_pmf (by D. Traytel)
src/HOL/Probability/Probability_Mass_Function.thy
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Mon Nov 24 22:59:20 2014 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Nov 25 17:29:39 2014 +0100
     1.3 @@ -11,7 +11,17 @@
     1.4    "~~/src/HOL/Library/Multiset"
     1.5  begin
     1.6  
     1.7 -lemma (in finite_measure) countable_support: (* replace version in pmf *)
     1.8 +lemma bind_return'': "sets M = sets N \<Longrightarrow> M \<guillemotright>= return N = M"
     1.9 +   by (cases "space M = {}")
    1.10 +      (simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return'
    1.11 +                cong: subprob_algebra_cong)
    1.12 +
    1.13 +
    1.14 +lemma (in prob_space) distr_const[simp]:
    1.15 +  "c \<in> space N \<Longrightarrow> distr M N (\<lambda>x. c) = return N c"
    1.16 +  by (rule measure_eqI) (auto simp: emeasure_distr emeasure_space_1)
    1.17 +
    1.18 +lemma (in finite_measure) countable_support:
    1.19    "countable {x. measure M {x} \<noteq> 0}"
    1.20  proof cases
    1.21    assume "measure M (space M) = 0"
    1.22 @@ -623,6 +633,9 @@
    1.23  lemma map_return_pmf: "map_pmf f (return_pmf x) = return_pmf (f x)"
    1.24    by transfer (simp add: distr_return)
    1.25  
    1.26 +lemma map_pmf_const[simp]: "map_pmf (\<lambda>_. c) M = return_pmf c"
    1.27 +  by transfer (auto simp: prob_space.distr_const)
    1.28 +
    1.29  lemma set_return_pmf: "set_pmf (return_pmf x) = {x}"
    1.30    by transfer (auto simp add: measure_return split: split_indicator)
    1.31  
    1.32 @@ -655,6 +668,12 @@
    1.33  lemma bind_return_pmf: "bind_pmf (return_pmf x) f = f x"
    1.34    unfolding bind_pmf_def map_return_pmf join_return_pmf ..
    1.35  
    1.36 +lemma join_eq_bind_pmf: "join_pmf M = bind_pmf M id"
    1.37 +  by (simp add: bind_pmf_def)
    1.38 +
    1.39 +lemma bind_pmf_const[simp]: "bind_pmf M (\<lambda>x. c) = c"
    1.40 +  unfolding bind_pmf_def map_pmf_const join_return_pmf ..
    1.41 +
    1.42  lemma set_bind_pmf: "set_pmf (bind_pmf M N) = (\<Union>M\<in>set_pmf M. set_pmf (N M))"
    1.43    apply (simp add: set_eq_iff set_pmf_iff pmf_bind)
    1.44    apply (subst integral_nonneg_eq_0_iff_AE)
    1.45 @@ -764,6 +783,11 @@
    1.46  
    1.47  end
    1.48  
    1.49 +lemma map_join_pmf: "map_pmf f (join_pmf AA) = join_pmf (map_pmf (map_pmf f) AA)"
    1.50 +  unfolding bind_pmf_def[symmetric]
    1.51 +  unfolding bind_return_pmf''[symmetric] join_eq_bind_pmf bind_assoc_pmf
    1.52 +  by (simp add: bind_return_pmf'')
    1.53 +
    1.54  definition "pair_pmf A B = bind_pmf A (\<lambda>x. bind_pmf B (\<lambda>y. return_pmf (x, y)))"
    1.55  
    1.56  lemma pmf_pair: "pmf (pair_pmf M N) (a, b) = pmf M a * pmf N b"
    1.57 @@ -811,6 +835,15 @@
    1.58      done
    1.59  qed
    1.60  
    1.61 +lemma join_map_return_pmf: "join_pmf (map_pmf return_pmf A) = A"
    1.62 +  unfolding bind_pmf_def[symmetric] bind_return_pmf' ..
    1.63 +
    1.64 +lemma map_fst_pair_pmf: "map_pmf fst (pair_pmf A B) = A"
    1.65 +  by (simp add: pair_pmf_def bind_return_pmf''[symmetric] bind_assoc_pmf bind_return_pmf bind_return_pmf')
    1.66 +
    1.67 +lemma map_snd_pair_pmf: "map_pmf snd (pair_pmf A B) = B"
    1.68 +  by (simp add: pair_pmf_def bind_return_pmf''[symmetric] bind_assoc_pmf bind_return_pmf bind_return_pmf')
    1.69 +
    1.70  inductive rel_pmf :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a pmf \<Rightarrow> 'b pmf \<Rightarrow> bool"
    1.71  for R p q
    1.72  where