src/HOL/Probability/Probability_Mass_Function.thy
changeset 62026 ea3b1b0413b4
parent 61808 fc1556774cfe
child 62083 7582b39f51ed
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Jan 01 11:27:29 2016 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Jan 01 14:44:52 2016 +0100
     1.3 @@ -334,13 +334,13 @@
     1.4    assumes "\<And>i. i \<in> set_pmf x \<Longrightarrow> A i = B i"
     1.5    shows "bind (measure_pmf x) A = bind (measure_pmf x) B"
     1.6  proof (rule measure_eqI)
     1.7 -  show "sets (measure_pmf x \<guillemotright>= A) = sets (measure_pmf x \<guillemotright>= B)"
     1.8 +  show "sets (measure_pmf x \<bind> A) = sets (measure_pmf x \<bind> B)"
     1.9      using assms by (subst (1 2) sets_bind) (auto simp: space_subprob_algebra)
    1.10  next
    1.11 -  fix X assume "X \<in> sets (measure_pmf x \<guillemotright>= A)"
    1.12 +  fix X assume "X \<in> sets (measure_pmf x \<bind> A)"
    1.13    then have X: "X \<in> sets N"
    1.14      using assms by (subst (asm) sets_bind) (auto simp: space_subprob_algebra)
    1.15 -  show "emeasure (measure_pmf x \<guillemotright>= A) X = emeasure (measure_pmf x \<guillemotright>= B) X"
    1.16 +  show "emeasure (measure_pmf x \<bind> A) X = emeasure (measure_pmf x \<bind> B) X"
    1.17      using assms
    1.18      by (subst (1 2) emeasure_bind[where N=N, OF _ _ X])
    1.19         (auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff)
    1.20 @@ -362,13 +362,13 @@
    1.21    have [measurable]: "g \<in> measurable f (subprob_algebra (count_space UNIV))"
    1.22      by (auto simp: measurable_def space_subprob_algebra prob_space_imp_subprob_space g)
    1.23  
    1.24 -  show "prob_space (f \<guillemotright>= g)"
    1.25 +  show "prob_space (f \<bind> g)"
    1.26      using g by (intro f.prob_space_bind[where S="count_space UNIV"]) auto
    1.27 -  then interpret fg: prob_space "f \<guillemotright>= g" .
    1.28 -  show [simp]: "sets (f \<guillemotright>= g) = UNIV"
    1.29 +  then interpret fg: prob_space "f \<bind> g" .
    1.30 +  show [simp]: "sets (f \<bind> g) = UNIV"
    1.31      using sets_eq_imp_space_eq[OF s_f]
    1.32      by (subst sets_bind[where N="count_space UNIV"]) auto
    1.33 -  show "AE x in f \<guillemotright>= g. measure (f \<guillemotright>= g) {x} \<noteq> 0"
    1.34 +  show "AE x in f \<bind> g. measure (f \<bind> g) {x} \<noteq> 0"
    1.35      apply (simp add: fg.prob_eq_0 AE_bind[where B="count_space UNIV"])
    1.36      using ae_f
    1.37      apply eventually_elim
    1.38 @@ -408,7 +408,7 @@
    1.39    "p = q \<Longrightarrow> (\<And>x. x \<in> set_pmf q =simp=> f x = g x) \<Longrightarrow> bind_pmf p f = bind_pmf q g"
    1.40    by (simp add: simp_implies_def cong: bind_pmf_cong)
    1.41  
    1.42 -lemma measure_pmf_bind: "measure_pmf (bind_pmf M f) = (measure_pmf M \<guillemotright>= (\<lambda>x. measure_pmf (f x)))"
    1.43 +lemma measure_pmf_bind: "measure_pmf (bind_pmf M f) = (measure_pmf M \<bind> (\<lambda>x. measure_pmf (f x)))"
    1.44    by transfer simp
    1.45  
    1.46  lemma nn_integral_bind_pmf[simp]: "(\<integral>\<^sup>+x. f x \<partial>bind_pmf M N) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)"
    1.47 @@ -437,7 +437,7 @@
    1.48  
    1.49  lemma bind_return_pmf': "bind_pmf N return_pmf = N"
    1.50  proof (transfer, clarify)
    1.51 -  fix N :: "'a measure" assume "sets N = UNIV" then show "N \<guillemotright>= return (count_space UNIV) = N"
    1.52 +  fix N :: "'a measure" assume "sets N = UNIV" then show "N \<bind> return (count_space UNIV) = N"
    1.53      by (subst return_sets_cong[where N=N]) (simp_all add: bind_return')
    1.54  qed
    1.55  
    1.56 @@ -458,7 +458,7 @@
    1.57    "rel_fun op = (rel_fun cr_pmf cr_pmf) (\<lambda>f M. distr M (count_space UNIV) f) map_pmf"
    1.58  proof -
    1.59    have "rel_fun op = (rel_fun pmf_as_measure.cr_pmf pmf_as_measure.cr_pmf)
    1.60 -     (\<lambda>f M. M \<guillemotright>= (return (count_space UNIV) o f)) map_pmf"
    1.61 +     (\<lambda>f M. M \<bind> (return (count_space UNIV) o f)) map_pmf"
    1.62      unfolding map_pmf_def[abs_def] comp_def by transfer_prover
    1.63    then show ?thesis
    1.64      by (force simp: rel_fun_def cr_pmf_def bind_return_distr)
    1.65 @@ -584,7 +584,7 @@
    1.66  
    1.67  lemma bind_pair_pmf:
    1.68    assumes M[measurable]: "M \<in> measurable (count_space UNIV \<Otimes>\<^sub>M count_space UNIV) (subprob_algebra N)"
    1.69 -  shows "measure_pmf (pair_pmf A B) \<guillemotright>= M = (measure_pmf A \<guillemotright>= (\<lambda>x. measure_pmf B \<guillemotright>= (\<lambda>y. M (x, y))))"
    1.70 +  shows "measure_pmf (pair_pmf A B) \<bind> M = (measure_pmf A \<bind> (\<lambda>x. measure_pmf B \<bind> (\<lambda>y. M (x, y))))"
    1.71      (is "?L = ?R")
    1.72  proof (rule measure_eqI)
    1.73    have M'[measurable]: "M \<in> measurable (pair_pmf A B) (subprob_algebra N)"