author hoelzl Tue, 25 Nov 2014 17:29:39 +0100 changeset 59052 a05c8305781e parent 59051 d9e124f50d85 child 59053 43e07797269b
projections of pair_pmf (by D. Traytel)
```--- a/src/HOL/Probability/Probability_Mass_Function.thy	Mon Nov 24 22:59:20 2014 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Nov 25 17:29:39 2014 +0100
@@ -11,7 +11,17 @@
"~~/src/HOL/Library/Multiset"
begin

-lemma (in finite_measure) countable_support: (* replace version in pmf *)
+lemma bind_return'': "sets M = sets N \<Longrightarrow> M \<guillemotright>= return N = M"
+   by (cases "space M = {}")
+      (simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return'
+                cong: subprob_algebra_cong)
+
+
+lemma (in prob_space) distr_const[simp]:
+  "c \<in> space N \<Longrightarrow> distr M N (\<lambda>x. c) = return N c"
+  by (rule measure_eqI) (auto simp: emeasure_distr emeasure_space_1)
+
+lemma (in finite_measure) countable_support:
"countable {x. measure M {x} \<noteq> 0}"
proof cases
assume "measure M (space M) = 0"
@@ -623,6 +633,9 @@
lemma map_return_pmf: "map_pmf f (return_pmf x) = return_pmf (f x)"

+lemma map_pmf_const[simp]: "map_pmf (\<lambda>_. c) M = return_pmf c"
+  by transfer (auto simp: prob_space.distr_const)
+
lemma set_return_pmf: "set_pmf (return_pmf x) = {x}"
by transfer (auto simp add: measure_return split: split_indicator)

@@ -655,6 +668,12 @@
lemma bind_return_pmf: "bind_pmf (return_pmf x) f = f x"
unfolding bind_pmf_def map_return_pmf join_return_pmf ..

+lemma join_eq_bind_pmf: "join_pmf M = bind_pmf M id"
+
+lemma bind_pmf_const[simp]: "bind_pmf M (\<lambda>x. c) = c"
+  unfolding bind_pmf_def map_pmf_const join_return_pmf ..
+
lemma set_bind_pmf: "set_pmf (bind_pmf M N) = (\<Union>M\<in>set_pmf M. set_pmf (N M))"
apply (simp add: set_eq_iff set_pmf_iff pmf_bind)
apply (subst integral_nonneg_eq_0_iff_AE)
@@ -764,6 +783,11 @@

end

+lemma map_join_pmf: "map_pmf f (join_pmf AA) = join_pmf (map_pmf (map_pmf f) AA)"
+  unfolding bind_pmf_def[symmetric]
+  unfolding bind_return_pmf''[symmetric] join_eq_bind_pmf bind_assoc_pmf
+
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"
@@ -811,6 +835,15 @@
done
qed

+lemma join_map_return_pmf: "join_pmf (map_pmf return_pmf A) = A"
+  unfolding bind_pmf_def[symmetric] bind_return_pmf' ..
+
+lemma map_fst_pair_pmf: "map_pmf fst (pair_pmf A B) = A"
+  by (simp add: pair_pmf_def bind_return_pmf''[symmetric] bind_assoc_pmf bind_return_pmf bind_return_pmf')
+
+lemma map_snd_pair_pmf: "map_pmf snd (pair_pmf A B) = B"
+  by (simp add: pair_pmf_def bind_return_pmf''[symmetric] bind_assoc_pmf bind_return_pmf bind_return_pmf')
+
inductive rel_pmf :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a pmf \<Rightarrow> 'b pmf \<Rightarrow> bool"
for R p q
where```