more lemmas
authorAndreas Lochbihler
Wed Feb 11 15:22:37 2015 +0100 (2015-02-11)
changeset 59525dfe6449aecd8
parent 59524 67deb7bed6d3
child 59526 af02440afb4a
more lemmas
src/HOL/Probability/Giry_Monad.thy
src/HOL/Probability/Probability_Mass_Function.thy
     1.1 --- a/src/HOL/Probability/Giry_Monad.thy	Wed Feb 11 15:04:23 2015 +0100
     1.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Wed Feb 11 15:22:37 2015 +0100
     1.3 @@ -142,6 +142,20 @@
     1.4      "subprob_space (null_measure M) \<longleftrightarrow> space M \<noteq> {}"
     1.5    by (auto intro!: subprob_spaceI dest: subprob_space.subprob_not_empty)
     1.6  
     1.7 +lemma subprob_space_restrict_space:
     1.8 +  assumes M: "subprob_space M"
     1.9 +  and A: "A \<inter> space M \<in> sets M" "A \<inter> space M \<noteq> {}"
    1.10 +  shows "subprob_space (restrict_space M A)"
    1.11 +proof(rule subprob_spaceI)
    1.12 +  have "emeasure (restrict_space M A) (space (restrict_space M A)) = emeasure M (A \<inter> space M)"
    1.13 +    using A by(simp add: emeasure_restrict_space space_restrict_space)
    1.14 +  also have "\<dots> \<le> 1" by(rule subprob_space.subprob_emeasure_le_1)(rule M)
    1.15 +  finally show "emeasure (restrict_space M A) (space (restrict_space M A)) \<le> 1" .
    1.16 +next
    1.17 +  show "space (restrict_space M A) \<noteq> {}"
    1.18 +    using A by(simp add: space_restrict_space)
    1.19 +qed
    1.20 +
    1.21  definition subprob_algebra :: "'a measure \<Rightarrow> 'a measure measure" where
    1.22    "subprob_algebra K =
    1.23      (\<Squnion>\<^sub>\<sigma> A\<in>sets K. vimage_algebra {M. subprob_space M \<and> sets M = sets K} (\<lambda>M. emeasure M A) borel)"
     2.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Wed Feb 11 15:04:23 2015 +0100
     2.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Wed Feb 11 15:22:37 2015 +0100
     2.3 @@ -502,6 +502,12 @@
     2.4    shows "(\<integral>x. f x \<partial>bernoulli_pmf p) = f True * p + f False * (1 - p)"
     2.5    by (subst integral_measure_pmf[of UNIV]) (auto simp: UNIV_bool)
     2.6  
     2.7 +lemma pmf_bernoulli_half [simp]: "pmf (bernoulli_pmf (1 / 2)) x = 1 / 2"
     2.8 +by(cases x) simp_all
     2.9 +
    2.10 +lemma measure_pmf_bernoulli_half: "measure_pmf (bernoulli_pmf (1 / 2)) = uniform_count_measure UNIV"
    2.11 +by(rule measure_eqI)(simp_all add: nn_integral_pmf[symmetric] emeasure_uniform_count_measure nn_integral_count_space_finite sets_uniform_count_measure)
    2.12 +
    2.13  subsubsection \<open> Geometric Distribution \<close>
    2.14  
    2.15  lift_definition geometric_pmf :: "nat pmf" is "\<lambda>n. 1 / 2^Suc n"
    2.16 @@ -639,7 +645,7 @@
    2.17    "(\<lambda>x. measure_pmf (M x)) \<in> measurable (count_space UNIV) (subprob_algebra (count_space UNIV))"
    2.18    by (auto simp: space_subprob_algebra intro!: prob_space_imp_subprob_space) unfold_locales
    2.19  
    2.20 -lemma bind_pmf_cong:
    2.21 +lemma bind_measure_pmf_cong:
    2.22    assumes "\<And>x. A x \<in> space (subprob_algebra N)" "\<And>x. B x \<in> space (subprob_algebra N)"
    2.23    assumes "\<And>i. i \<in> set_pmf x \<Longrightarrow> A i = B i"
    2.24    shows "bind (measure_pmf x) A = bind (measure_pmf x) B"
    2.25 @@ -879,6 +885,16 @@
    2.26    unfolding bind_return_pmf''[symmetric] join_eq_bind_pmf bind_assoc_pmf
    2.27    by (simp add: bind_return_pmf'')
    2.28  
    2.29 +lemma bind_pmf_cong:
    2.30 +  "\<lbrakk> p = q; \<And>x. x \<in> set_pmf q \<Longrightarrow> f x = g x \<rbrakk>
    2.31 +  \<Longrightarrow> bind_pmf p f = bind_pmf q g"
    2.32 +by(simp add: bind_pmf_def cong: map_pmf_cong)
    2.33 +
    2.34 +lemma bind_pmf_cong_simp:
    2.35 +  "\<lbrakk> p = q; \<And>x. x \<in> set_pmf q =simp=> f x = g x \<rbrakk>
    2.36 +  \<Longrightarrow> bind_pmf p f = bind_pmf q g"
    2.37 +by(simp add: simp_implies_def cong: bind_pmf_cong)
    2.38 +
    2.39  definition "pair_pmf A B = bind_pmf A (\<lambda>x. bind_pmf B (\<lambda>y. return_pmf (x, y)))"
    2.40  
    2.41  lemma pmf_pair: "pmf (pair_pmf M N) (a, b) = pmf M a * pmf N b"
    2.42 @@ -1235,5 +1251,38 @@
    2.43                     map_pair)
    2.44  qed
    2.45  
    2.46 +lemma rel_pmf_reflI: 
    2.47 +  assumes "\<And>x. x \<in> set_pmf p \<Longrightarrow> P x x"
    2.48 +  shows "rel_pmf P p p"
    2.49 +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)
    2.50 +
    2.51 +lemma rel_pmf_joinI:
    2.52 +  assumes "rel_pmf (rel_pmf P) p q"
    2.53 +  shows "rel_pmf P (join_pmf p) (join_pmf q)"
    2.54 +proof -
    2.55 +  from assms obtain pq where p: "p = map_pmf fst pq"
    2.56 +    and q: "q = map_pmf snd pq"
    2.57 +    and P: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> rel_pmf P x y"
    2.58 +    by cases auto
    2.59 +  from P obtain PQ 
    2.60 +    where PQ: "\<And>x y a b. \<lbrakk> (x, y) \<in> set_pmf pq; (a, b) \<in> set_pmf (PQ x y) \<rbrakk> \<Longrightarrow> P a b"
    2.61 +    and x: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> map_pmf fst (PQ x y) = x"
    2.62 +    and y: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> map_pmf snd (PQ x y) = y"
    2.63 +    by(metis rel_pmf.simps)
    2.64 +
    2.65 +  let ?r = "bind_pmf pq (\<lambda>(x, y). PQ x y)"
    2.66 +  have "\<And>a b. (a, b) \<in> set_pmf ?r \<Longrightarrow> P a b" by(auto simp add: set_bind_pmf intro: PQ)
    2.67 +  moreover have "map_pmf fst ?r = join_pmf p" "map_pmf snd ?r = join_pmf q"
    2.68 +    by(simp_all add: bind_pmf_def map_join_pmf pmf.map_comp o_def split_def p q x y cong: pmf.map_cong)
    2.69 +  ultimately show ?thesis ..
    2.70 +qed
    2.71 +
    2.72 +lemma rel_pmf_bindI:
    2.73 +  assumes pq: "rel_pmf R p q"
    2.74 +  and fg: "\<And>x y. R x y \<Longrightarrow> rel_pmf P (f x) (g y)"
    2.75 +  shows "rel_pmf P (bind_pmf p f) (bind_pmf q g)"
    2.76 +unfolding bind_pmf_def
    2.77 +by(rule rel_pmf_joinI)(auto simp add: pmf.rel_map intro: pmf.rel_mono[THEN le_funD, THEN le_funD, THEN le_boolD, THEN mp, OF _ pq] fg)
    2.78 +
    2.79  end
    2.80