# HG changeset patch
# User hoelzl
# Date 1475511564 -7200
# Node ID 9c99fccce3cff34c18499e24e6f8948aa2a9191f
# Parent  a5d293f1af80f95707d67d749ab56da0258737c6
Probability: move some theorems from AFP/Density_Compiler

diff -r a5d293f1af80 -r 9c99fccce3cf src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Mon Oct 03 15:46:08 2016 +0200
+++ b/src/HOL/Probability/Giry_Monad.thy	Mon Oct 03 18:19:24 2016 +0200
@@ -1698,7 +1698,7 @@
   using measurable_bind_prob_space[OF measurable_const, OF A B, THEN measurable_space, of undefined "count_space UNIV"]
   by (simp add: space_prob_algebra)
 
-lemma bind_cong_AE:
+lemma bind_cong_AE':
   assumes M: "M \<in> space (prob_algebra L)"
     and f: "f \<in> L \<rightarrow>\<^sub>M prob_algebra N" and g: "g \<in> L \<rightarrow>\<^sub>M prob_algebra N"
     and ae: "AE x in M. f x = g x"
@@ -1712,4 +1712,70 @@
     by (auto intro: nn_integral_cong_AE)
 qed
 
+lemma density_discrete:
+  "countable A \<Longrightarrow> sets N = Set.Pow A \<Longrightarrow> (\<And>x. f x \<ge> 0) \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x = emeasure N {x}) \<Longrightarrow>
+    density (count_space A) f = N"
+  by (rule measure_eqI_countable[of _ A]) (auto simp: emeasure_density)
+
+lemma distr_density_discrete:
+  fixes f'
+  assumes "countable A"
+  assumes "f' \<in> borel_measurable M"
+  assumes "g \<in> measurable M (count_space A)"
+  defines "f \<equiv> \<lambda>x. \<integral>\<^sup>+t. (if g t = x then 1 else 0) * f' t \<partial>M"
+  assumes "\<And>x.  x \<in> space M \<Longrightarrow> g x \<in> A"
+  shows "density (count_space A) (\<lambda>x. f x) = distr (density M f') (count_space A) g"
+proof (rule density_discrete)
+  fix x assume x: "x \<in> A"
+  have "f x = \<integral>\<^sup>+t. indicator (g -` {x} \<inter> space M) t * f' t \<partial>M" (is "_ = ?I") unfolding f_def
+    by (intro nn_integral_cong) (simp split: split_indicator)
+  also from x have in_sets: "g -` {x} \<inter> space M \<in> sets M"
+    by (intro measurable_sets[OF assms(3)]) simp
+  have "?I = emeasure (density M f') (g -` {x} \<inter> space M)" unfolding f_def
+    by (subst emeasure_density[OF assms(2) in_sets], subst mult.commute) (rule refl)
+  also from assms(3) x have "... = emeasure (distr (density M f') (count_space A) g) {x}"
+    by (subst emeasure_distr) simp_all
+  finally show "f x = emeasure (distr (density M f') (count_space A) g) {x}" .
+qed (insert assms, auto)
+
+lemma bind_cong_AE:
+  assumes "M = N"
+  assumes f: "f \<in> measurable N (subprob_algebra B)"
+  assumes g: "g \<in> measurable N (subprob_algebra B)"
+  assumes ae: "AE x in N. f x = g x"
+  shows "bind M f = bind N g"
+proof cases
+  assume "space N = {}" then show ?thesis
+    using `M = N` by (simp add: bind_empty)
+next
+  assume "space N \<noteq> {}"
+  show ?thesis unfolding `M = N`
+  proof (rule measure_eqI)
+    have *: "sets (N \<bind> f) = sets B"
+      using sets_bind[OF sets_kernel[OF f] `space N \<noteq> {}`] by simp
+    then show "sets (N \<bind> f) = sets (N \<bind> g)"
+      using sets_bind[OF sets_kernel[OF g] `space N \<noteq> {}`] by auto
+    fix A assume "A \<in> sets (N \<bind> f)"
+    then have "A \<in> sets B"
+      unfolding * .
+    with ae f g `space N \<noteq> {}` show "emeasure (N \<bind> f) A = emeasure (N \<bind> g) A"
+      by (subst (1 2) emeasure_bind[where N=B]) (auto intro!: nn_integral_cong_AE)
+  qed
+qed
+
+lemma bind_cong_strong: "M = N \<Longrightarrow> (\<And>x. x\<in>space M =simp=> f x = g x) \<Longrightarrow> bind M f = bind N g"
+  by (auto simp: simp_implies_def intro!: bind_cong)
+
+lemma sets_bind_measurable:
+  assumes f: "f \<in> measurable M (subprob_algebra B)"
+  assumes M: "space M \<noteq> {}"
+  shows "sets (M \<bind> f) = sets B"
+  using M by (intro sets_bind[OF sets_kernel[OF f]]) auto
+
+lemma space_bind_measurable:
+  assumes f: "f \<in> measurable M (subprob_algebra B)"
+  assumes M: "space M \<noteq> {}"
+  shows "space (M \<bind> f) = space B"
+  using M by (intro space_bind[OF sets_kernel[OF f]]) auto
+
 end