Theory Monad_QuasiBorel

(*  Title:   Monad_QuasiBorel.thy
    Author:  Michikazu Hirata, Tetsuya Sato, Tokyo Institute of Technology
*)

subsection ‹The Probability Monad›

theory Monad_QuasiBorel
  imports "Probability_Space_QuasiBorel"
begin

subsubsection ‹ The Probability Monad $P$ ›
definition monadP_qbs_Px :: "'a quasi_borel  'a qbs_prob_space set" where
"monadP_qbs_Px X  {s. qbs_prob_space_qbs s = X}"

locale in_Px =
  fixes X :: "'a quasi_borel" and s :: "'a qbs_prob_space" 
  assumes in_Px:"s  monadP_qbs_Px X"
begin

lemma qbs_prob_space_X[simp]:
 "qbs_prob_space_qbs s = X"
  using in_Px by(simp add: monadP_qbs_Px_def)

end

locale in_MPx =
  fixes X :: "'a quasi_borel" and β :: "real  'a qbs_prob_space"
  assumes ex:"α qbs_Mx X. g  real_borel M prob_algebra real_borel.
                         r. β r = qbs_prob_space (X,α,g r)"
begin

lemma rep_inMPx:
 "α g. α  qbs_Mx X  g  real_borel M prob_algebra real_borel 
        β = (λr. qbs_prob_space (X,α,g r))"
proof -
  obtain α g where hb:
   "α  qbs_Mx X" "g  real_borel M prob_algebra real_borel"
        "β = (λr. qbs_prob_space (X,α,g r))"
    using ex by auto
  thus ?thesis
    by(auto intro!: exI[where x=α] exI[where x=g] simp: hb)
qed

end

definition monadP_qbs_MPx :: "'a quasi_borel  (real  'a qbs_prob_space) set" where
"monadP_qbs_MPx X  {β. in_MPx X β}"

definition monadP_qbs :: "'a quasi_borel  'a qbs_prob_space quasi_borel" where
"monadP_qbs X  Abs_quasi_borel (monadP_qbs_Px X, monadP_qbs_MPx X)"

lemma(in qbs_prob) qbs_prob_space_in_Px:
  "qbs_prob_space (X,α,μ)  monadP_qbs_Px X"
  using qbs_prob_axioms by(simp add: monadP_qbs_Px_def)

lemma rep_monadP_qbs_Px:
  assumes "s  monadP_qbs_Px X"
  shows "α μ. s = qbs_prob_space (X, α, μ)  qbs_prob X α μ"
  using rep_qbs_prob_space' assms in_Px.qbs_prob_space_X
  by(auto simp: monadP_qbs_Px_def)

lemma rep_monadP_qbs_MPx:
  assumes "β  monadP_qbs_MPx X"
  shows "α g. α  qbs_Mx X  g  real_borel M prob_algebra real_borel 
        β = (λr. qbs_prob_space (X,α,g r))"
  using assms in_MPx.rep_inMPx
  by(auto simp: monadP_qbs_MPx_def)

lemma qbs_prob_MPx:
  assumes "α  qbs_Mx X"
      and "g  real_borel M prob_algebra real_borel"
    shows "qbs_prob X α (g r)"
  using measurable_space[OF assms(2)]
  by(auto intro!: qbs_prob.intro simp: space_prob_algebra in_Mx_def real_distribution_def real_distribution_axioms_def assms(1))

lemma monadP_qbs_f[simp]: "monadP_qbs_MPx X  UNIV  monadP_qbs_Px X"
  unfolding monadP_qbs_MPx_def
proof auto
  fix β r
  assume "in_MPx X β"
  then obtain α g where hb:
   "α  qbs_Mx X" "g  real_borel M prob_algebra real_borel"
        "β = (λr. qbs_prob_space (X,α,g r))"
    using in_MPx.rep_inMPx by blast
  then interpret qp : qbs_prob X α "g r"
    by(simp add: qbs_prob_MPx)
  show "β r  monadP_qbs_Px X"
    by(simp add: hb(3) qp.qbs_prob_space_in_Px)
qed

lemma monadP_qbs_closed1: "qbs_closed1 (monadP_qbs_MPx X)"
  unfolding monadP_qbs_MPx_def in_MPx_def
  apply(rule qbs_closed1I)
  subgoal for α f
    apply auto
    subgoal for β g
      apply(auto intro!: bexI[where x=β] bexI[where x="gf"])
      done
    done
  done

lemma monadP_qbs_closed2: "qbs_closed2 (monadP_qbs_Px X) (monadP_qbs_MPx X)"
  unfolding qbs_closed2_def
proof
  fix s
  assume "s  monadP_qbs_Px X"
  then obtain α μ where h:
   "qbs_prob X α μ" "s = qbs_prob_space (X, α, μ)"
    using rep_qbs_prob_space'[of s X] monadP_qbs_Px_def by blast
  then interpret qp : qbs_prob X α μ
    by simp
  define g :: "real  real measure"
    where "g  (λ_. μ)"
  have "g  real_borel M prob_algebra real_borel"
    using h prob_algebra_real_prob_measure[of μ]
    by(simp add: qbs_prob_def g_def)
  thus "(λr. s)  monadP_qbs_MPx X"
    by(auto intro!: bexI[where x=α] bexI[where x=g] simp: monadP_qbs_MPx_def in_MPx_def g_def h)
qed

lemma monadP_qbs_closed3: "qbs_closed3 (monadP_qbs_MPx (X :: 'a quasi_borel))"
proof(rule qbs_closed3I)
  fix P :: "real  nat"
  fix Fi
  assume "i. P -` {i}  sets real_borel"
  then have HP_mble[measurable] : "P  real_borel M nat_borel"
    by (simp add: separate_measurable)
  assume "i :: nat. Fi i  monadP_qbs_MPx X"
  then have "i. αi. gi. αi  qbs_Mx X  gi  real_borel M prob_algebra real_borel 
                    Fi i = (λr. qbs_prob_space (X, αi, gi r))"
    using in_MPx.rep_inMPx[of X] by(simp add: monadP_qbs_MPx_def)
  hence "α. i. gi. α i  qbs_Mx X  gi  real_borel M prob_algebra real_borel 
                    Fi i = (λr. qbs_prob_space (X, α i, gi r))"
    by(rule choice)
  then obtain α :: "nat  real  _" where
       "i. gi. α i  qbs_Mx X  gi  real_borel M prob_algebra real_borel 
                     Fi i = (λr. qbs_prob_space (X, α i, gi r))"
    by auto
  hence  "g. i. α i  qbs_Mx X  g i  real_borel M prob_algebra real_borel 
                  Fi i = (λr. qbs_prob_space (X, α i, g i r))"
    by(rule choice)
  then obtain g :: "nat  real  real measure" where 
       H0: "i. α i  qbs_Mx X" "i. g i  real_borel M prob_algebra real_borel"
           "i. Fi i = (λr. qbs_prob_space (X, α i, g i r))"
    by blast
  hence LHS: "(λr. Fi (P r) r) = (λr. qbs_prob_space (X, α (P r), g (P r) r))"
    by auto

  ― ‹ Since ℕ×ℝ› is standard, we have measurable functions
        nat_real.f ∈ ℕ ⨂M ℝ →M ℝ› and nat_real.g ∈ ℝ →M ℕ ⨂M ℝ›
       such that @{thm nat_real.gf_comp_id'(1)}. ›
       
  ― ‹ The proof is divided into 3 steps.
       \begin{enumerate}
       \item  Let α'' = uncurry α ∘ nat_real.g›. Then α'' ∈ qbs_Mx X›.
       \item Let g'' = G(nat_real.f) ∘ (λr. δP(r)M gP(r) r›.
               Then g''› is ℝ›/G(ℝ)› measurable. 
       \item Show that (λr. Fi (P r) r) = (λr. qbs_prob_space (X, α'', g'' r))›.
       \end{enumerate}›

  ― ‹ Step 1.›
  define α' :: "nat × real  'a"
    where "α'  case_prod α"
  define α'' :: "real  'a"
    where "α''  α'  nat_real.g"

  have α_morp: "α  Q Q exp_qbs Q X"
    using qbs_Mx_is_morphisms[of X] H0(1)
    by(auto intro!: nat_qbs_morphism)
  hence α'_morp: "α'  Q Q Q  Q X"
    unfolding α'_def
    by(intro uncurry_preserves_morphisms)
  hence [measurable]:"α'  nat_borel M real_borel M qbs_to_measure X"
    using l_preserves_morphisms[of "Q Q Q" X]
    by(auto simp add: r_preserves_product)
  have H_Mx:"α''  qbs_Mx X"
    unfolding α''_def
    using qbs_morphism_comp[OF real.qbs_morphism_measurable_intro[OF nat_real.g_meas,simplified r_preserves_product] α'_morp] qbs_Mx_is_morphisms[of X]
    by simp


  ― ‹ Step 2.›
  define g' :: "real  (nat × real) measure"
    where "g'  (λr. return nat_borel (P r) M g (P r) r)"
  define g'' :: "real  real measure"
    where "g''  (λM. distr M real_borel nat_real.f)  g'"

  have [measurable]:"(λnr. g (fst nr) (snd nr))  nat_borel M real_borel M prob_algebra real_borel"
    using measurable_pair_measure_countable1[of "UNIV :: nat set" "λnr. g (fst nr) (snd nr)",simplified,OF H0(2)] measurable_cong_sets[OF sets_pair_measure_cong[of nat_borel "count_space UNIV" real_borel real_borel,OF sets_borel_eq_count_space refl] refl,of "prob_algebra real_borel"]
    by auto    
  hence [measurable]:"(λr. g (P r) r)  real_borel M prob_algebra real_borel"
  proof -
    have "(λr. g (P r) r) = (λnr. g (fst nr) (snd nr))  (λr. (P r, r))" by auto
    also have "...  real_borel M prob_algebra real_borel"
      by simp
    finally show ?thesis .
  qed
  have g'_mble[measurable]:"g'  real_borel M prob_algebra (nat_borel M real_borel)"
    unfolding g'_def by simp
  have H_mble: "g''  real_borel M prob_algebra real_borel"
    unfolding g''_def by simp

  ― ‹ Step 3.›
  have H_equiv: 
       "qbs_prob_space (X, α (P r), g (P r) r) = qbs_prob_space (X, α'', g'' r)" for r
  proof -
    interpret pqp: pair_qbs_prob X "α (P r)" "g (P r) r" X α'' "g'' r"
      using qbs_prob_MPx[OF H0(1,2)] measurable_space[OF H_mble,of r] space_prob_algebra[of real_borel] H_Mx
      by (simp add: pair_qbs_prob.intro qbs_probI)
    interpret pps: pair_prob_space "return nat_borel (P r)" "g (P r) r"
      using prob_space_return[of "P r" nat_borel]
      by(simp add: pair_prob_space_def pair_sigma_finite_def prob_space_imp_sigma_finite)
    have [measurable_cong]: "sets (return nat_borel (P r)) = sets nat_borel"
                            "sets (g' r) = sets (nat_borel M real_borel)"
      using measurable_space[OF g'_mble,of r] space_prob_algebra by auto
    show "qbs_prob_space (X, α (P r), g (P r) r) = qbs_prob_space (X, α'', g'' r)"
    proof(rule pqp.qbs_prob_space_eq4)
      fix f
      assume [measurable]:"f  qbs_to_measure X  M ennreal_borel"
      show "(+ x. f (α (P r) x) g (P r) r) = (+ x. f (α'' x) g'' r)"
           (is "?lhs = ?rhs")
      proof -
        have "?lhs = (+s. f (α' ((P r),s))  (g (P r) r))"
          by(simp add: α'_def)
        also have "... = (+s. (+i. f (α' (i, s))  (return nat_borel (P r)))   (g (P r) r))"
          by(auto intro!: nn_integral_cong simp: nn_integral_return[of "P r" nat_borel])
        also have "... = (+k. (f  α') k  ((return nat_borel (P r)) M (g (P r) r)))"
          by(auto intro!: pps.nn_integral_snd)
        also have "... = (+k. f (α' k)  (g' r))"
          by(simp add: g'_def)
        also have "... = (+x. f x  (distr (g' r) (qbs_to_measure X) α'))"
          by(simp add: nn_integral_distr)
        also have "... = (+x. f x  (distr (g'' r) (qbs_to_measure X) α''))"
          by(simp add: distr_distr comp_def g''_def α''_def)
        also have "... = ?rhs"
          by(simp add: nn_integral_distr)
        finally show ?thesis .
      qed
    qed simp
  qed

  have "r. Fi (P r) r = qbs_prob_space (X, α'', g'' r)"
    by (metis H_equiv LHS)
  thus "(λr. Fi (P r) r)  monadP_qbs_MPx X"
    using H_mble H_Mx by(auto simp add: monadP_qbs_MPx_def in_MPx_def)
qed

lemma monadP_qbs_correct: "Rep_quasi_borel (monadP_qbs X) = (monadP_qbs_Px X, monadP_qbs_MPx X)"
  by(auto intro!: Abs_quasi_borel_inverse monadP_qbs_f simp: monadP_qbs_closed2 monadP_qbs_closed1 monadP_qbs_closed3 monadP_qbs_def)

lemma monadP_qbs_space[simp] : "qbs_space (monadP_qbs X) = monadP_qbs_Px X"
  by(simp add: qbs_space_def monadP_qbs_correct)

lemma monadP_qbs_Mx[simp] : "qbs_Mx (monadP_qbs X) = monadP_qbs_MPx X"
  by(simp add: qbs_Mx_def monadP_qbs_correct)

lemma monadP_qbs_empty_iff:
 "qbs_space X = {}  qbs_space (monadP_qbs X) = {}"
proof auto
  fix x
  assume 1:"qbs_space X = {}"
           "x  monadP_qbs_Px X"
  then obtain α μ where "qbs_prob X α μ"
    using rep_monadP_qbs_Px by blast
  thus False
    using empty_quasi_borel_iff[of X] qbs_empty_not_qbs_prob[of α μ] 1(1)
    by auto
next
  fix x
  assume 1:"monadP_qbs_Px X = {}"
           "x  qbs_space X"
  then interpret qp: qbs_prob X "λr. x" "return real_borel 0"
    by(auto intro!: qbs_probI prob_space_return)
  have "qbs_prob_space (X,λr. x,return real_borel 0)  monadP_qbs_Px X"
    by(simp add: monadP_qbs_Px_def)
  thus False
    by(simp add: 1)
qed

text ‹ If β ∈ MPx›, there exists X› α› g› s.t.β r = [X,α,g r]›.
       We define a function which picks X› α› g› from β ∈ MPx›.›
definition rep_monadP_qbs_MPx :: "(real  'a qbs_prob_space)  'a quasi_borel × (real  'a) × (real  real measure)" where
"rep_monadP_qbs_MPx β  let X = qbs_prob_space_qbs (β undefined);
                            αg = (SOME k. (fst k)  qbs_Mx X  (snd k)  real_borel M prob_algebra real_borel
                                           β = (λr. qbs_prob_space (X,fst k,snd k r)))
                         in (X,αg)"

lemma qbs_prob_measure_measurable[measurable]:
 "qbs_prob_measure  qbs_to_measure (monadP_qbs (X :: 'a quasi_borel)) M prob_algebra (qbs_to_measure X)"
proof(rule qbs_morphism_dest,rule qbs_morphismI,simp)
  fix β
  assume "β  monadP_qbs_MPx X"
  then obtain α g where hb:
  "α  qbs_Mx X" "β = (λr. qbs_prob_space (X, α, g r))"
   and g[measurable]: "g  real_borel M prob_algebra real_borel"  
    using in_MPx.rep_inMPx[of X β] monadP_qbs_MPx_def by blast
  have "qbs_prob_measure  β = (λr. distr (g r) (qbs_to_measure X) α)"
  proof 
    fix r
    interpret qp : qbs_prob X α "g r"
      using qbs_prob_MPx[OF hb(1) g]  by simp
    show "(qbs_prob_measure  β) r = distr (g r) (qbs_to_measure X) α"
      by(simp add: hb(2))
  qed
  also have "...  real_borel M prob_algebra (qbs_to_measure X) "
    using hb by simp
  finally show "qbs_prob_measure  β  real_borel M prob_algebra (qbs_to_measure X)" .
qed

lemma qbs_l_inj:
  "inj_on qbs_prob_measure (monadP_qbs_Px X)"
  apply standard
  apply (unfold monadP_qbs_Px_def)
  apply simp
  apply transfer
  apply (auto simp: qbs_prob_eq_def qbs_prob_t_measure_def)
  done

lemma qbs_prob_measure_measurable'[measurable]:
 "qbs_prob_measure  qbs_to_measure (monadP_qbs (X :: 'a quasi_borel)) M subprob_algebra (qbs_to_measure X)"
  by(auto simp: measurable_prob_algebraD)

subsubsection ‹ Return ›
definition qbs_return :: "['a quasi_borel, 'a]  'a qbs_prob_space" where
"qbs_return X x  qbs_prob_space (X,λr. x,Eps real_distribution)"

lemma(in real_distribution) qbs_return_qbs_prob:
  assumes "x  qbs_space X"
  shows "qbs_prob X (λr. x) M"
  using assms 
  by(simp add: qbs_prob_def in_Mx_def real_distribution_axioms)

lemma(in real_distribution) qbs_return_computation :
  assumes "x  qbs_space X"
  shows "qbs_return X x = qbs_prob_space (X,λr. x,M)"
  unfolding qbs_return_def
proof(rule someI2[where a=M])
  fix N
  assume "real_distribution N"
  then interpret pqp: pair_qbs_prob X "λr. x" N X "λr. x" M
    by(simp_all add: pair_qbs_prob_def real_distribution_axioms real_distribution.qbs_return_qbs_prob[OF _ assms])
  show "qbs_prob_space (X, λr. x, N) = qbs_prob_space (X, λr. x, M)"
    by(auto intro!: pqp.qbs_prob_space_eq simp: distr_const[of x "qbs_to_measure X"] assms)
qed (rule real_distribution_axioms)

lemma qbs_return_morphism:
  "qbs_return X  X Q monadP_qbs X"
proof -
  interpret rr : real_distribution "return real_borel 0"
    by(simp add: real_distribution_def real_distribution_axioms_def prob_space_return)
  show ?thesis
  proof(rule qbs_morphismI,simp)
    fix α
    assume h:"α  qbs_Mx X"
    then have h':"l:: real. α l  qbs_space X"
      by auto
    have "l. (qbs_return X  α) l = qbs_prob_space (X, α, return real_borel l)"
    proof -
      fix l
      interpret pqp: pair_qbs_prob X "λr. α l" "return real_borel 0" X α "return real_borel l"
        using h' by(simp add: pair_qbs_prob_def qbs_prob_def in_Mx_def h real_distribution_def prob_space_return real_distribution_axioms_def)
      have "(qbs_return X  α) l = qbs_prob_space (X,λr. α l,return real_borel 0)"
        using rr.qbs_return_computation[OF h'[of l]] by simp
      also have "... = qbs_prob_space (X, α, return real_borel l)"
        by(auto intro!: pqp.qbs_prob_space_eq simp: distr_return)
      finally show "(qbs_return X  α) l = qbs_prob_space (X, α, return real_borel l)" .
    qed
    thus "qbs_return X  α  monadP_qbs_MPx X"
      by(auto intro!: bexI[where x="α"] bexI[where x="λl. return real_borel l"] simp: h  monadP_qbs_MPx_def in_MPx_def)
  qed
qed

lemma qbs_return_morphism':
  assumes "f  X Q Y"
  shows "(λx. qbs_return Y (f x))  X Q monadP_qbs Y"
  using qbs_morphism_comp[OF assms(1) qbs_return_morphism[of Y]]
  by (simp add: comp_def)

subsubsection ‹Bind›
definition qbs_bind :: "'a qbs_prob_space  ('a  'b qbs_prob_space)   'b qbs_prob_space" where
"qbs_bind s f  (let (qbsx,α,μ) = rep_qbs_prob_space s;
                      (qbsy,β,g) = rep_monadP_qbs_MPx (f  α) 
                     in qbs_prob_space (qbsy,β,μ  g))"

adhoc_overloading Monad_Syntax.bind qbs_bind

lemma(in qbs_prob) qbs_bind_computation:
  assumes"s = qbs_prob_space (X,α,μ)"
         "f  X Q monadP_qbs Y"
         "β  qbs_Mx Y"
   and [measurable]: "g  real_borel M prob_algebra real_borel"
      and "(f  α) = (λr. qbs_prob_space (Y,β, g r))"
    shows "qbs_prob Y β (μ  g)"
          "s  f = qbs_prob_space (Y,β,μ  g)"
proof -
  interpret qp_bind: qbs_prob Y β "μ  g"
    using assms(3,4) space_prob_algebra[of real_borel] measurable_space[OF assms(4)] events_eq_borel measurable_cong_sets[OF events_eq_borel refl,of "subprob_algebra real_borel"] measurable_prob_algebraD[OF assms(4)]
    by(auto intro!: prob_space_bind[of g real_borel] simp: qbs_prob_def in_Mx_def real_distribution_def real_distribution_axioms_def)
  show "qbs_prob Y β (μ  g)"
    by (rule qp_bind.qbs_prob_axioms)
  show "s  f = qbs_prob_space (Y, β, μ  g)"
    apply(simp add: assms(1) qbs_bind_def rep_qbs_prob_space_def qbs_prob_space.rep_def)
    apply(rule someI2[where a= "(X, α, μ)"])
  proof auto
    fix X' α' μ'
    assume h':"(X',α',μ')  Rep_qbs_prob_space (qbs_prob_space (X, α, μ))"
    from if_in_Rep[OF this] interpret pqp1: pair_qbs_prob X α μ X' α' μ'
      by(simp add: pair_qbs_prob_def qbs_prob_axioms)
    have h_eq: "qbs_prob_space (X, α, μ) = qbs_prob_space (X',α',μ')"
      using if_in_Rep(3)[OF h'] by (simp add: qbs_prob_space_eq)
    note [simp] = if_in_Rep(1)[OF h']
    then obtain β' g' where hb':
     "β'  qbs_Mx Y" "g'  real_borel M prob_algebra real_borel"
       "f  α' = (λr. qbs_prob_space (Y, β', g' r))"
      using in_MPx.rep_inMPx[of Y "f  α'"] qbs_morphismE(3)[OF assms(2),of α'] pqp1.qp2.qbs_prob_axioms[simplified qbs_prob_def in_Mx_def]
      by(auto simp: monadP_qbs_MPx_def)
    note [measurable] = hb'(2)
    have [simp]:"r. qbs_prob_space_qbs (f (α' r)) = Y"
      subgoal for r
        using fun_cong[OF hb'(3)] qbs_prob.qbs_prob_space_qbs_computation[OF qbs_prob_MPx[OF hb'(1,2),of r]]
        by simp
      done
    show "(case rep_monadP_qbs_MPx (λa. f (α' a)) of (qbsy, β, g)  qbs_prob_space (qbsy, β, μ'  g)) =
                 qbs_prob_space (Y, β, μ  g)"
      unfolding rep_monadP_qbs_MPx_def Let_def
    proof(rule someI2[where a="(β',g')"],auto simp: hb'[simplified comp_def])
      fix α'' g''
      assume h'':"α''  qbs_Mx Y"
                 "g''  real_borel M prob_algebra real_borel"
                 "(λr. qbs_prob_space (Y, β', g' r)) = (λr. qbs_prob_space (Y, α'', g'' r))"
      then interpret pqp2: pair_qbs_prob Y α'' "μ'  g''" Y β "μ  g"
        using space_prob_algebra[of real_borel] measurable_space[OF h''(2)] events_eq_borel measurable_cong_sets[OF events_eq_borel refl,of "subprob_algebra real_borel"] measurable_prob_algebraD[OF h''(2)] h''(3)
        by (meson pair_qbs_prob_def in_Mx_def pqp1.qp2.real_distribution_axioms prob_algebra_real_prob_measure prob_space_bind' qbs_probI qbs_prob_def qp_bind.qbs_prob_axioms sets_bind')
      note [measurable] = h''(2)
      have [measurable]:"f  qbs_to_measure X M qbs_to_measure (monadP_qbs Y)"
        using assms(2) l_preserves_morphisms by auto
      show "qbs_prob_space (Y, α'', μ'  g'') = qbs_prob_space (Y, β, μ  g)"
      proof(rule pqp2.qbs_prob_space_eq)
        show "distr (μ'  g'') (qbs_to_measure Y) α'' = distr (μ  g) (qbs_to_measure Y) β"
             (is "?lhs = ?rhs")
        proof -
          have "?lhs = μ'  (λx. distr (g'' x) (qbs_to_measure Y) α'')"
            by(auto intro!: distr_bind[where K=real_borel] simp: measurable_prob_algebraD)
          also have "... = μ'  (λx. qbs_prob_measure (qbs_prob_space (Y,α'',g'' x)))"
            by(auto intro!: bind_cong simp: qbs_prob_MPx[OF h''(1,2)] qbs_prob.qbs_prob_measure_computation)
          also have "... = μ'  (λx. (qbs_prob_measure  ((f  α') x)))"
            by(simp add: hb'(3) h''(3))
          also have "... = μ'  (λx. (qbs_prob_measure  f)  (α' x))"
            by(simp add: comp_def)
          also have "... = distr μ' (qbs_to_measure X) α'  qbs_prob_measure  f"
            by(rule bind_distr[where K="qbs_to_measure Y",symmetric],auto)
          also have "... = distr μ (qbs_to_measure X) α  qbs_prob_measure  f"
            using pqp1.qbs_prob_space_eq_inverse(1)[OF h_eq]
            by(simp add: qbs_prob_eq_def)
          also have "... = μ  (λx. (qbs_prob_measure  f)  (α x))"
            by(rule bind_distr[where K="qbs_to_measure Y"],auto)
          also have "... = μ  (λx. (qbs_prob_measure  ((f  α) x)))"
            by(simp add: comp_def)
          also have "... = μ  (λx. qbs_prob_measure (qbs_prob_space (Y,β,g x)))"
            by(auto simp: assms(5))
          also have "... = μ  (λx. distr (g x) (qbs_to_measure Y) β)"
            by(auto intro!: bind_cong simp: qbs_prob_MPx[OF assms(3)] qbs_prob.qbs_prob_measure_computation)
          also have "... = ?rhs"
            by(auto intro!: distr_bind[where K=real_borel,symmetric] simp: measurable_prob_algebraD)
          finally show ?thesis .
        qed
      qed simp
    qed
  qed (rule in_Rep)
qed

lemma qbs_bind_morphism':
  assumes "f  X Q monadP_qbs Y"
  shows "(λx. x  f)  monadP_qbs X Q monadP_qbs Y"
proof(rule qbs_morphismI,simp)
  fix β
  assume "β  monadP_qbs_MPx X"
  then obtain α g where hb:
   "α  qbs_Mx X" "g  real_borel M prob_algebra real_borel"
   "β = (λr. qbs_prob_space (X, α, g r))"
    using rep_monadP_qbs_MPx by blast
  obtain γ g' where hc:
   "γ  qbs_Mx Y" "g'  real_borel M prob_algebra real_borel"
   "f  α = (λr. qbs_prob_space (Y, γ, g' r))"
    using rep_monadP_qbs_MPx[of "f  α" Y] qbs_morphismE(3)[OF assms hb(1),simplified]
    by auto
  note [measurable] = hb(2) hc(2)
  show "(λx. x  f)  β  monadP_qbs_MPx Y"
  proof -
    have "(λx. x  f)  β = (λr. β r  f)"
      by auto
    also have "...  monadP_qbs_MPx Y"
      unfolding monadP_qbs_MPx_def in_MPx_def
      by(auto intro!: bexI[where x="γ"] bexI[where x="λr. g r  g'"] simp: hc(1) hb(3) qbs_prob.qbs_bind_computation[OF qbs_prob_MPx[OF hb(1,2)] _ assms hc])
    finally show ?thesis .
  qed
qed

lemma qbs_return_comp:
  assumes "α  qbs_Mx X"
  shows "(qbs_return X  α) = (λr. qbs_prob_space (X,α,return real_borel r))"
proof
  fix r
  interpret pqp: pair_qbs_prob X "λk. α r" "return real_borel 0" X α "return real_borel r"
    by(simp add: assms qbs_Mx_to_X(2)[OF assms] pair_qbs_prob_def qbs_prob_def in_Mx_def real_distribution_def real_distribution_axioms_def prob_space_return)
  show "(qbs_return X  α) r = qbs_prob_space (X, α, return real_borel r)"
    by(auto intro!: pqp.qbs_prob_space_eq simp: distr_return pqp.qp1.qbs_return_computation qbs_Mx_to_X(2)[OF assms])
qed

lemma qbs_bind_return':
  assumes "x  monadP_qbs_Px X"
  shows "x  qbs_return X = x"
proof -
  obtain α μ where h1:"qbs_prob X α μ" "x = qbs_prob_space (X, α, μ)"
    using assms rep_monadP_qbs_Px by blast
  then interpret qp: qbs_prob X α μ
    by simp
  show ?thesis
    using qp.qbs_bind_computation[OF h1(2) qbs_return_morphism _ measurable_return_prob_space qbs_return_comp[OF qp.in_Mx]]
    by(simp add: h1(2) bind_return'' prob_space_return qbs_probI)
qed

lemma qbs_bind_return:
  assumes "f  X Q monadP_qbs Y"
      and "x  qbs_space X"
    shows "qbs_return X x  f = f x"
proof -
  have "f x  monadP_qbs_Px Y"
    using assms by auto
  then obtain β μ where hf:"qbs_prob Y β μ" "f x = qbs_prob_space (Y, β, μ)"
    using rep_monadP_qbs_Px by blast
  then interpret rd: real_distribution "return real_borel 0"
    by(simp add: qbs_prob_def prob_space_return real_distribution_def real_distribution_axioms_def)
  interpret rd': real_distribution μ
    using hf(1) by(simp add: qbs_prob_def)
  interpret qp: qbs_prob X "λr. x" "return real_borel 0"
    using assms(2) by(auto simp: qbs_prob_def in_Mx_def rd.real_distribution_axioms)
  show ?thesis
    by(auto intro!: qp.qbs_bind_computation(2)[OF rd.qbs_return_computation[OF assms(2)] assms(1) _ measurable_const[of μ],of β,simplified bind_const'[OF rd.prob_space_axioms rd'.subprob_space_axioms]]
              simp: hf[simplified qbs_prob_def in_Mx_def] prob_algebra_real_prob_measure)
qed

lemma qbs_bind_assoc:
  assumes "s  monadP_qbs_Px X"
          "f  X Q monadP_qbs Y"
      and "g  Y Q monadP_qbs Z"
   shows "s  (λx. f x  g) = (s  f)  g"
proof -
  obtain α μ where H0:"qbs_prob X α μ" "s = qbs_prob_space (X, α, μ)"
    using assms rep_monadP_qbs_Px by blast
  then have "f  α  monadP_qbs_MPx Y"
    using assms(2) by(auto simp: qbs_prob_def in_Mx_def)
  from rep_monadP_qbs_MPx[OF this] obtain β g1 where H1:
   "β  qbs_Mx Y" "g1  real_borel M prob_algebra real_borel"
   " (f  α) = (λr. qbs_prob_space (Y, β, g1 r))"
    by auto
  hence "g  β  monadP_qbs_MPx Z"
    using assms by(simp add: qbs_morphism_def)
  from rep_monadP_qbs_MPx[OF this] obtain γ g2 where H2:
   "γ  qbs_Mx Z" "g2  real_borel M prob_algebra real_borel"
   "(g  β) = (λr. qbs_prob_space (Z, γ, g2 r))"
    by auto
  note [measurable] = H1(2) H2(2)
  interpret rd: real_distribution μ
    using H0(1) by(simp add: qbs_prob_def)
  have LHS: "(s  f)  g = qbs_prob_space (Z, γ, μ  g1  g2)"
    by(rule qbs_prob.qbs_bind_computation(2)[OF qbs_prob.qbs_bind_computation[OF H0 assms(2) H1] assms(3) H2])
  have RHS: "s  (λx. f x  g) =  qbs_prob_space (Z, γ, μ  (λx. g1 x  g2))"
    apply(auto intro!: qbs_prob.qbs_bind_computation[OF H0 qbs_morphism_comp[OF assms(2) qbs_bind_morphism'[OF assms(3)],simplified comp_def]]
                 simp: real_distribution_def real_distribution_axioms_def qbs_prob_def qbs_prob_MPx[OF H2(1,2),simplified qbs_prob_def] sets_bind'[OF measurable_space[OF H1(2)] H2(2)] prob_space_bind'[OF measurable_space[OF H1(2)] H2(2)] measurable_space[OF H2(2)] space_prob_algebra[of real_borel] H2(1))
  proof
    fix r
    show "((λx. f x  g)  α) r = qbs_prob_space (Z, γ, g1 r  g2)" (is "?lhs = ?rhs") for r
      by(auto intro!: qbs_prob.qbs_bind_computation(2)[of Y β]
                simp: qbs_prob_MPx[OF H1(1,2),of r] assms(3) H2 fun_cong[OF H1(3),simplified comp_def])
  qed
  have ba: "μ  g1  g2 = μ  (λx. g1 x  g2)"
    by(auto intro!: bind_assoc[where N=real_borel and R=real_borel] simp: measurable_prob_algebraD)
  show ?thesis
    by(simp add: LHS RHS ba)
qed

lemma qbs_bind_cong:
  assumes "s  monadP_qbs_Px X"
          "x. x  qbs_space X  f x = g x"
      and "f  X Q monadP_qbs Y"
    shows "s  f = s  g"
proof -
  obtain α μ where h0:
  "qbs_prob X α μ"  "s = qbs_prob_space (X, α, μ)"
    using rep_monadP_qbs_Px[OF assms(1)] by auto
  then have "f  α  monadP_qbs_MPx Y"
    using assms(3) h0(1) by(auto simp: qbs_prob_def in_Mx_def)
  from rep_monadP_qbs_MPx[OF this] obtain γ k where h1:
   "γ  qbs_Mx Y" "k  real_borel M prob_algebra real_borel"
   "(f  α) = (λr. qbs_prob_space (Y, γ, k r))"
    by auto
  have hg:"g  X Q monadP_qbs Y"
    using qbs_morphism_cong[OF assms(2,3)] by simp
  have hgs: "f  α = g  α"
    using h0(1) assms(2) by(force simp: qbs_prob_def in_Mx_def)

  show ?thesis
    by(simp add: qbs_prob.qbs_bind_computation(2)[OF h0 assms(3) h1]
                 qbs_prob.qbs_bind_computation(2)[OF h0 hg h1[simplified hgs]])
qed

subsubsection ‹ The Functorial Action $P(f)$›
definition monadP_qbs_Pf :: "['a quasi_borel, 'b quasi_borel,'a  'b,'a qbs_prob_space]  'b qbs_prob_space" where
"monadP_qbs_Pf _ Y f sx  sx  qbs_return Y  f"

lemma monadP_qbs_Pf_morphism:
  assumes "f  X Q Y"
  shows "monadP_qbs_Pf X Y f  monadP_qbs X Q monadP_qbs Y"
  unfolding monadP_qbs_Pf_def
  by(rule qbs_bind_morphism'[OF qbs_morphism_comp[OF assms qbs_return_morphism]])

lemma(in qbs_prob) monadP_qbs_Pf_computation:
  assumes "s = qbs_prob_space (X,α,μ)"
      and "f  X Q Y"
    shows "qbs_prob Y (f  α) μ"
      and "monadP_qbs_Pf X Y f s = qbs_prob_space (Y,f  α,μ)"
   by(auto intro!: qbs_bind_computation[OF assms(1) qbs_morphism_comp[OF assms(2) qbs_return_morphism],of "f  α" "return real_borel" ,simplified bind_return''[OF M_is_borel]]
             simp: monadP_qbs_Pf_def qbs_return_comp[OF qbs_morphismE(3)[OF assms(2) in_Mx],simplified comp_assoc[symmetric]] qbs_morphismE(3)[OF assms(2) in_Mx] prob_space_return)

text ‹ We show that P is a functor i.e. P preserves identity and composition.›
lemma monadP_qbs_Pf_id:
  assumes "s  monadP_qbs_Px X"
  shows "monadP_qbs_Pf X X id s = s"
  using qbs_bind_return'[OF assms] by(simp add: monadP_qbs_Pf_def)

lemma monadP_qbs_Pf_comp:
  assumes "s  monadP_qbs_Px X"
          "f  X Q Y"
      and "g  Y Q Z" 
    shows "((monadP_qbs_Pf Y Z g)  (monadP_qbs_Pf X Y f)) s = monadP_qbs_Pf X Z (g  f) s"
proof -
  obtain α μ where h:
  "qbs_prob X α μ" "s = qbs_prob_space (X, α, μ)"
    using rep_monadP_qbs_Px[OF assms(1)] by auto
  hence "qbs_prob Y (f  α) μ"
        "monadP_qbs_Pf X Y f s = qbs_prob_space (Y,f  α,μ)"
    using qbs_prob.monadP_qbs_Pf_computation[OF _ _ assms(2)] by auto
  from qbs_prob.monadP_qbs_Pf_computation[OF this assms(3)] qbs_prob.monadP_qbs_Pf_computation[OF h qbs_morphism_comp[OF assms(2,3)]]
  show ?thesis
    by(simp add: comp_assoc)
qed

subsubsection ‹ Join ›
definition qbs_join :: "'a qbs_prob_space qbs_prob_space  'a qbs_prob_space" where
"qbs_join  (λsst. sst  id)"

lemma qbs_join_morphism:
  "qbs_join  monadP_qbs (monadP_qbs X) Q monadP_qbs X"
  by(simp add: qbs_join_def qbs_bind_morphism'[OF qbs_morphism_ident])

lemma qbs_join_computation:
  assumes "qbs_prob (monadP_qbs X) β μ"
          "ssx = qbs_prob_space (monadP_qbs X,β,μ)"
          "α  qbs_Mx X"
          "g  real_borel M prob_algebra real_borel"
      and "β =(λr.  qbs_prob_space (X,α,g r))"
    shows "qbs_prob X α (μ  g)" "qbs_join ssx = qbs_prob_space (X,α, μ  g)"
  using qbs_prob.qbs_bind_computation[OF assms(1,2) qbs_morphism_ident assms(3,4)]
  by(auto simp: assms(5) qbs_join_def)

subsubsection ‹ Strength ›
definition qbs_strength :: "['a quasi_borel,'b quasi_borel,'a × 'b qbs_prob_space]  ('a × 'b) qbs_prob_space" where
"qbs_strength W X = (λ(w,sx). let (_,α,μ) = rep_qbs_prob_space sx
                         in qbs_prob_space (W Q X, λr. (w,α r), μ))"

lemma(in qbs_prob) qbs_strength_computation:
  assumes "w  qbs_space W"
      and "sx = qbs_prob_space (X,α,μ)"
    shows "qbs_prob (W Q X) (λr. (w,α r)) μ"
          "qbs_strength W X (w,sx) = qbs_prob_space (W Q X, λr. (w,α r), μ)"
proof -
  interpret qp1: qbs_prob "W Q X" "λr. (w,α r)" μ
    by(auto intro!: qbs_probI simp: assms(1) pair_qbs_Mx_def comp_def)
  show "qbs_prob (W Q X) (λr. (w,α r)) μ"
       "qbs_strength W X (w,sx) = qbs_prob_space (W Q X, λr. (w,α r), μ)"
     apply(simp_all add: qp1.qbs_prob_axioms qbs_strength_def rep_qbs_prob_space_def qbs_prob_space.rep_def)
    apply(rule someI2[where a="(X,α,μ)"])
  proof(auto simp: in_Rep assms(2))
    fix X' α' μ'
    assume h:"(X',α',μ')  Rep_qbs_prob_space (qbs_prob_space (X, α, μ))"
    from if_in_Rep(1,2)[OF this] interpret pqp: pair_qbs_prob "W Q X" "λr. (w, α' r)" μ' "W Q X" "λr. (w,α r)" μ
      by(simp add: pair_qbs_prob_def qp1.qbs_prob_axioms)
       (auto intro!: qbs_probI simp: pair_qbs_Mx_def comp_def assms(1) qbs_prob_def in_Mx_def)
    note [simp] = qbs_prob_eq2_dest[OF if_in_Rep(3)[OF h,simplified qbs_prob_eq_equiv12]]
    show "qbs_prob_space (W Q X, λr. (w, α' r), μ') = qbs_prob_space (W Q X, λr. (w, α r), μ)"
    proof(rule pqp.qbs_prob_space_eq2)
      fix f
      assume "f  qbs_to_measure (W Q X) M real_borel"
      note qbs_morphism_dest[OF qbs_morphismE(2)[OF curry_preserves_morphisms[OF qbs_morphism_measurable_intro[OF this]] assms(1),simplified]]
      show "(y. f ((λr. (w, α' r)) y)  μ') = (y. f ((λr. (w, α r)) y)  μ)"
           (is "?lhs = ?rhs")
      proof -
        have "?lhs = (y. curry f w (α' y)  μ')" by auto
        also have "... = (y. curry f w (α y)  μ)"
          by(rule qbs_prob_eq2_dest(4)[OF if_in_Rep(3)[OF h,simplified qbs_prob_eq_equiv12],symmetric]) fact
        also have "... = ?rhs" by auto
        finally show ?thesis .
      qed
    qed simp
  qed
qed

lemma qbs_strength_natural:
  assumes "f  X Q X'"
          "g  Y Q Y'"
          "x  qbs_space X"
      and "sy  monadP_qbs_Px Y"
    shows "(monadP_qbs_Pf (X Q Y) (X' Q Y') (map_prod f g)  qbs_strength X Y) (x,sy) = (qbs_strength X' Y'  map_prod f (monadP_qbs_Pf Y Y' g)) (x,sy)"
          (is "?lhs = ?rhs")
proof -
  obtain β ν where hy:
   "qbs_prob Y β ν" "sy = qbs_prob_space (Y,β,ν)"
    using rep_monadP_qbs_Px[OF assms(4)] by auto
  have "qbs_prob (X Q Y) (λr. (x, β r)) ν"
       "qbs_strength X Y (x, sy) = qbs_prob_space (X Q Y, λr. (x, β r), ν)"
    using qbs_prob.qbs_strength_computation[OF hy(1) assms(3) hy(2)] by auto
  hence LHS:"?lhs = qbs_prob_space (X' Q Y',map_prod f g  (λr. (x, β r)),ν)"
    by(simp add: qbs_prob.monadP_qbs_Pf_computation[OF _ _ qbs_morphism_map_prod[OF assms(1,2)]])

  have "map_prod f (monadP_qbs_Pf Y Y' g) (x,sy) = (f x,qbs_prob_space (Y',g  β,ν))"
       "qbs_prob Y' (g  β) ν"
    by(auto simp: qbs_prob.monadP_qbs_Pf_computation[OF hy assms(2)])
  hence RHS:"?rhs = qbs_prob_space (X' Q Y',λr. (f x, (g  β) r),ν)"
    using qbs_prob.qbs_strength_computation[OF _ _ refl,of Y' "g  β" ν "f x" X'] assms(1,3)
    by auto

  show "?lhs = ?rhs"
    unfolding LHS RHS
    by(simp add: comp_def)
qed

lemma qbs_strength_ab_r:
  assumes "α  qbs_Mx X"
          "β  monadP_qbs_MPx Y"
          "γ  qbs_Mx Y"
 and [measurable]:"g  real_borel M prob_algebra real_borel"
      and "β = (λr. qbs_prob_space (Y,γ,g r))"
    shows "qbs_prob (X Q Y) (map_prod α γ  real_real.g) (distr (return real_borel r M g r) real_borel real_real.f)"         
          "qbs_strength X Y (α r, β r) = qbs_prob_space (X Q Y, map_prod α γ  real_real.g, distr (return real_borel r M g r) real_borel real_real.f)"
proof -
  have [measurable_cong]: "sets (g r) = sets real_borel"
                          "sets (return real_borel r) = sets real_borel"
    using measurable_space[OF assms(4),of r]
    by(simp_all add: space_prob_algebra)
  interpret qp: qbs_prob "X Q Y" "map_prod α γ  real_real.g" "distr (return real_borel r M g r) real_borel real_real.f"
  proof(auto intro!: qbs_probI)
    show "map_prod α γ  real_real.g  pair_qbs_Mx X Y"
      using qbs_closed1_dest[OF assms(1)] qbs_closed1_dest[OF assms(3)]
      by(auto simp: comp_def qbs_prob_def in_Mx_def pair_qbs_Mx_def)
  next
    show "prob_space (distr (return real_borel r M g r) real_borel real_real.f) "
      using measurable_space[OF assms(4),of r]
      by(auto intro!: prob_space.prob_space_distr simp: prob_algebra_real_prob_measure prob_space_pair prob_space_return real_distribution.axioms(1))
  qed
  interpret pqp: pair_qbs_prob "X Q Y" "λl. (α r, γ l)" "g r" "X Q Y" "map_prod α γ  real_real.g" "distr (return real_borel r M g r) real_borel real_real.f"
    by(simp add: qbs_prob.qbs_strength_computation[OF qbs_prob_MPx[OF assms(3,4)] qbs_Mx_to_X(2)[OF assms(1)] fun_cong[OF assms(5)],of r] pair_qbs_prob_def qp.qbs_prob_axioms)
  have [measurable]: "map_prod α γ  real_borel M real_borel M qbs_to_measure (X Q Y)"
  proof -
    have "map_prod α γ  Q Q Q Q X Q Y"
      using assms(1,3) by(auto intro!: qbs_morphism_map_prod simp: qbs_Mx_is_morphisms)
    hence "map_prod α γ  qbs_to_measure (Q Q Q) M qbs_to_measure (X Q Y)"
      using l_preserves_morphisms by auto
    thus ?thesis
      by simp
  qed
  hence [measurable]:"(λl. (α r, γ l))  real_borel M qbs_to_measure (X Q Y)"
    using pqp.qp1.in_Mx qbs_Mx_are_measurable by blast

  show "qbs_prob (X Q Y) (map_prod α γ  real_real.g) (distr (return real_borel r M g r) real_borel real_real.f)"         
       "qbs_strength X Y (α r, β r) = qbs_prob_space (X Q Y, map_prod α γ  real_real.g, distr (return real_borel r M g r) real_borel real_real.f)"
     apply(simp_all add: qp.qbs_prob_axioms qbs_prob.qbs_strength_computation(2)[OF qbs_prob_MPx[OF assms(3,4)] qbs_Mx_to_X(2)[OF assms(1)] fun_cong[OF assms(5)],of r])
  proof(rule pqp.qbs_prob_space_eq)
    show "distr (g r) (qbs_to_measure (X Q Y)) (λl. (α r, γ l)) = distr (distr (return real_borel r M g r) real_borel real_real.f) (qbs_to_measure (X Q Y)) (map_prod α γ  real_real.g)"
         (is "?lhs = ?rhs")
    proof -
      have "?lhs = distr (g r) (qbs_to_measure (X Q Y)) (map_prod α γ  Pair r)"
        by(simp add: comp_def)
      also have "... = distr (distr (g r) (real_borel M real_borel) (Pair r)) (qbs_to_measure (X Q Y)) (map_prod α γ)"
        by(auto intro!: distr_distr[symmetric])
      also have "... = distr (return real_borel r M g r) (qbs_to_measure (X Q Y)) (map_prod α γ)"
      proof -
        have "return real_borel r M g r = distr (g r) (real_borel M real_borel) (λl. (r,l))"
        proof(auto intro!: measure_eqI)
          fix A
          assume h':"A  sets (real_borel M real_borel)"
          show "emeasure (return real_borel r M g r) A = emeasure (distr (g r) (real_borel M real_borel) (Pair r)) A"
                (is "?lhs' = ?rhs'")
          proof -
            have "?lhs' = + x. emeasure (g r) (Pair x -` A) return real_borel r"
              by(auto intro!: pqp.qp1.emeasure_pair_measure_alt simp: h')
            also have "... = emeasure (g r) (Pair r -` A)"
              by(auto intro!: nn_integral_return pqp.qp1.measurable_emeasure_Pair simp: h')
            also have "... = ?rhs'"
              by(simp add: emeasure_distr[OF _ h'])
            finally show ?thesis .
          qed
        qed
        thus ?thesis by simp
      qed
      also have "... = ?rhs"
        by(rule distr_distr[of "map_prod α γ  real_real.g" real_borel "qbs_to_measure (X Q Y)" real_real.f "return real_borel r M g r",simplified comp_assoc,simplified,symmetric])
      finally show ?thesis .
    qed
  qed simp
qed


lemma qbs_strength_morphism:
 "qbs_strength X Y  X Q monadP_qbs Y Q monadP_qbs (X Q Y)"
proof(rule pair_qbs_morphismI,simp)
  fix α β
  assume h:"α  qbs_Mx X"
           "β  monadP_qbs_MPx Y"
  then obtain γ g where hb:
    "γ  qbs_Mx Y" "g  real_borel M prob_algebra real_borel"
    "β = (λr. qbs_prob_space (Y, γ, g r))"
    using rep_monadP_qbs_MPx[of β] by blast
  note [measurable] = hb(2)
  show "qbs_strength X Y  (λr. (α r, β r))  monadP_qbs_MPx (X Q Y)"
    using qbs_strength_ab_r[OF h hb]
    by(auto intro!: bexI[where x="map_prod α γ  real_real.g"] bexI[where x="λr. distr (return real_borel r M g r) real_borel real_real.f"]
              simp: monadP_qbs_MPx_def in_MPx_def qbs_prob_def in_Mx_def)
qed

lemma qbs_bind_morphism'':
 "(λ(f,x). x  f)  exp_qbs X (monadP_qbs Y) Q (monadP_qbs X) Q (monadP_qbs Y)"
proof(rule qbs_morphism_cong[of _ "qbs_join  (monadP_qbs_Pf (exp_qbs X (monadP_qbs Y) Q X) (monadP_qbs Y) qbs_eval)  (qbs_strength (exp_qbs X (monadP_qbs Y)) X)"], auto)
  fix f
  fix sx
  assume h:"f  X Q monadP_qbs Y"
           "sx  monadP_qbs_Px X"
  then obtain α μ where h0:"qbs_prob X α μ" "sx = qbs_prob_space (X, α, μ)"
    using rep_monadP_qbs_Px[of sx X] by auto
  hence "f  α  monadP_qbs_MPx Y"
    using h(1) by(auto simp: qbs_prob_def in_Mx_def)
  then obtain β g where h1: 
  "β  qbs_Mx Y" "g  real_borel M prob_algebra real_borel"
  "(f  α) = (λr. qbs_prob_space (Y, β, g r))"
    using rep_monadP_qbs_MPx[of "f  α" Y] by blast

  show "qbs_join (monadP_qbs_Pf (exp_qbs X (monadP_qbs Y) Q X) (monadP_qbs Y) qbs_eval (qbs_strength (exp_qbs X (monadP_qbs Y)) X (f, sx))) =
           sx  f"
    by(simp add: qbs_join_computation[OF qbs_prob.monadP_qbs_Pf_computation[OF qbs_prob.qbs_strength_computation[OF h0(1) _ h0(2),of f "exp_qbs X (monadP_qbs Y)"] qbs_eval_morphism] h1(1,2),simplified qbs_eval_def comp_def,simplified,OF h(1) h1(3)[simplified comp_def]] qbs_prob.qbs_bind_computation[OF h0 h(1) h1])
next
  show "qbs_join   monadP_qbs_Pf (exp_qbs X (monadP_qbs Y) Q X) (monadP_qbs Y) qbs_eval  qbs_strength (exp_qbs X (monadP_qbs Y)) X  exp_qbs X (monadP_qbs Y) Q monadP_qbs X Q monadP_qbs Y"
    using qbs_join_morphism monadP_qbs_Pf_morphism[OF qbs_eval_morphism]
    by(auto intro!: qbs_morphism_comp simp: qbs_strength_morphism)
qed

lemma qbs_bind_morphism''':
  "(λf x. x  f)  exp_qbs X (monadP_qbs Y) Q exp_qbs (monadP_qbs X) (monadP_qbs Y)"
  using qbs_bind_morphism'' curry_preserves_morphisms[of "λ(f, x). qbs_bind x f"]
  by fastforce

lemma qbs_bind_morphism:
  assumes "f  X Q monadP_qbs Y"
      and "g  X Q exp_qbs Y (monadP_qbs Z)"
    shows "(λx. f x  g x)  X Q monadP_qbs Z"
  using qbs_morphism_comp[OF qbs_morphism_tuple[OF assms(2,1)] qbs_bind_morphism'']
  by(simp add: comp_def)

lemma qbs_bind_morphism'''':
  assumes "x  monadP_qbs_Px X"
  shows "(λf. x  f)  exp_qbs X (monadP_qbs Y) Q monadP_qbs Y"
  by(rule qbs_morphismE(2)[OF arg_swap_morphism[OF qbs_bind_morphism'''],simplified,OF assms])

lemma qbs_strength_law1:
  assumes "x  qbs_space (unit_quasi_borel Q monadP_qbs X)"
  shows "snd x = (monadP_qbs_Pf (unit_quasi_borel Q X) X snd  qbs_strength unit_quasi_borel X) x"
proof -
  obtain α μ where h:
   "qbs_prob X α μ" "(snd x) = qbs_prob_space (X, α, μ)"
    using rep_monadP_qbs_Px[of "snd x" X] assms by auto
  have [simp]: "((),snd x) = x"
    using SigmaE assms by auto
  show ?thesis
    using qbs_prob.monadP_qbs_Pf_computation[OF qbs_prob.qbs_strength_computation[OF h(1) _ h(2),of "fst x" "unit_quasi_borel",simplified] snd_qbs_morphism]
    by(simp add: h(2) comp_def)
qed

lemma qbs_strength_law2:
  assumes "x  qbs_space ((X Q Y) Q monadP_qbs Z)"
  shows "(qbs_strength X (Y Q Z)  (map_prod id (qbs_strength Y Z))  (λ((x,y),z). (x,(y,z)))) x =
         (monadP_qbs_Pf ((X Q Y) Q Z) (X Q (Y Q Z)) (λ((x,y),z). (x,(y,z)))  qbs_strength (X Q Y) Z) x"
         (is "?lhs = ?rhs")
proof -
  obtain α μ where h:
   "qbs_prob Z α μ" "snd x = qbs_prob_space (Z, α, μ)"
    using rep_monadP_qbs_Px[of "snd x" Z] assms by auto
  have "?lhs = qbs_prob_space (X Q Y Q Z, λr. (fst (fst x), snd (fst x), α r), μ)"
    using assms  qbs_prob.qbs_strength_computation[OF h(1) _ h(2),of "snd (fst x)" Y]
    by(auto intro!: qbs_prob.qbs_strength_computation)
  also have "... = ?rhs"
    using qbs_prob.monadP_qbs_Pf_computation[OF qbs_prob.qbs_strength_computation[OF h(1) _ h(2),of "fst x" "X Q Y"] qbs_morphism_pair_assoc1] assms
    by(auto simp: comp_def)
  finally show ?thesis .
qed

lemma qbs_strength_law3:
  assumes "x  qbs_space (X Q Y)"
  shows "qbs_return (X Q Y) x = (qbs_strength X Y  (map_prod id (qbs_return Y))) x"
proof -
  interpret qp: qbs_prob Y "λr. snd x" "return real_borel 0"
    using assms by(auto intro!: qbs_probI simp: prob_space_return)
  show ?thesis
    using qp.qbs_strength_computation[OF _ qp.qbs_return_computation[of "snd x" Y],of "fst x" X] assms
    by(auto simp: qp.qbs_return_computation[OF assms])
qed

lemma qbs_strength_law4:
  assumes "x  qbs_space (X Q monadP_qbs (monadP_qbs Y))"
  shows "(qbs_strength X Y  map_prod id qbs_join) x = (qbs_join  monadP_qbs_Pf (X Q monadP_qbs Y) (monadP_qbs (X Q Y))(qbs_strength X Y)  qbs_strength X (monadP_qbs Y)) x"
        (is "?lhs = ?rhs")
proof -
  obtain β μ where h0:
  "qbs_prob (monadP_qbs Y) β μ" "snd x = qbs_prob_space (monadP_qbs Y, β, μ)"
    using rep_monadP_qbs_Px[of "snd x" "monadP_qbs Y"] assms by auto
  then obtain γ g where h1:
   "γ  qbs_Mx Y" "g  real_borel M prob_algebra real_borel"
   "β = (λr. qbs_prob_space (Y, γ, g r))"
    using rep_monadP_qbs_MPx[of β Y] by(auto simp: qbs_prob_def in_Mx_def)
  have "?lhs = qbs_prob_space (X Q Y, λr. (fst x, γ r), μ  g)"
    using qbs_prob.qbs_strength_computation[OF qbs_join_computation(1)[OF h0 h1] _ qbs_join_computation(2)[OF h0 h1],of "fst x" X] assms
    by auto
  also have "... = ?rhs"
  proof -
    have "qbs_strength X Y  (λr. (fst x, β r)) = (λr. qbs_prob_space (X Q Y, λr. (fst x, γ r), g r))"
    proof
      show "(qbs_strength X Y  (λr. (fst x, β r))) r = qbs_prob_space (X Q Y, λr. (fst x, γ r), g r)" for r
        using qbs_prob.qbs_strength_computation(2)[OF qbs_prob_MPx[OF h1(1,2),of r] _ fun_cong[OF h1(3)],of "fst x" X] assms
        by auto
    qed
    thus ?thesis
      using qbs_join_computation(2)[OF qbs_prob.monadP_qbs_Pf_computation[OF qbs_prob.qbs_strength_computation[OF h0(1) _ h0(2),of "fst x" X] qbs_strength_morphism] _ h1(2),of "λr. (fst x, γ r)",symmetric] assms h1(1)
      by(auto simp: pair_qbs_Mx_def comp_def)
  qed
  finally show ?thesis .
qed


lemma qbs_return_Mxpair:
  assumes "α  qbs_Mx X"
      and "β  qbs_Mx Y"
    shows "qbs_return (X Q Y) (α r, β k) = qbs_prob_space (X Q Y,map_prod α β  real_real.g, distr (return real_borel r M return real_borel k) real_borel real_real.f)"
          "qbs_prob (X Q Y) (map_prod α β  real_real.g) (distr (return real_borel r M return real_borel k) real_borel real_real.f)"
proof -
  note [measurable_cong] = sets_return[of real_borel]
  interpret qp: qbs_prob "X Q Y" "map_prod α β  real_real.g" "distr (return real_borel r M return real_borel k) real_borel real_real.f"
    using qbs_closed1_dest[OF assms(1)] qbs_closed1_dest[OF assms(2)]
    by(auto intro!: qbs_probI prob_space.prob_space_distr prob_space_pair
              simp: pair_qbs_Mx_def comp_def prob_space_return)
  show "qbs_return (X Q Y) (α r, β k) = qbs_prob_space (X Q Y,map_prod α β  real_real.g, distr (return real_borel r M return real_borel k) real_borel real_real.f)"
       "qbs_prob (X Q Y) (map_prod α β  real_real.g) (distr (return real_borel r M return real_borel k) real_borel real_real.f)"
  proof -
    show "qbs_return (X Q Y) (α r, β k) = qbs_prob_space (X Q Y, map_prod α β  real_real.g, distr (return real_borel r M return real_borel k) real_borel real_real.f)"
         (is "?lhs = ?rhs")
    proof -
      have 1:"(λr. qbs_prob_space (Y, β, return real_borel k))  monadP_qbs_MPx Y"
        by(auto intro!: in_MPx.intro bexI[where x=β] bexI[where x="λr. return real_borel k"] simp: monadP_qbs_MPx_def assms(2))
      have "?lhs = (qbs_strength X Y  map_prod id (qbs_return Y)) (α r, β k)"
        by(intro qbs_strength_law3[of "(α r, β k)" X Y]) (use assms in auto)
      also have "... = qbs_strength X Y (α r, qbs_prob_space (Y, β, return real_borel k))"
        using fun_cong[OF qbs_return_comp[OF assms(2)]] by simp
      also have "... = ?rhs"
        by(intro qbs_strength_ab_r(2)[OF assms(1) 1 assms(2) _ refl,of r]) auto
      finally show ?thesis .
    qed
  qed(rule qp.qbs_prob_axioms)
qed


lemma pair_return_return:
  assumes "l  space M"
      and "r  space N"
    shows "return M l M return N r = return (M M N) (l,r)"
proof(auto intro!: measure_eqI)
  fix A
  assume h:"A  sets (M M N)"
  show "emeasure (return M l M return N r) A = indicator A (l, r)"
       (is "?lhs = ?rhs")
  proof -
    have "?lhs = (+ x. + y. indicator A (x, y) return N r return M l)"
      by(auto intro!: sigma_finite_measure.emeasure_pair_measure prob_space_imp_sigma_finite simp: h prob_space_return assms)
    also have "... = (+ x. indicator A (x, r) return M l)"
      using h by(auto intro!: nn_integral_cong nn_integral_return simp: assms(2))
    also have "... = ?rhs"
      using h by(auto intro!: nn_integral_return simp: assms)
    finally show ?thesis .
  qed
qed

lemma bind_bind_return_distr:
  assumes "real_distribution μ"
      and "real_distribution ν"
    shows "μ  (λr. ν  (λl. distr (return real_borel r M return real_borel l) real_borel real_real.f))
           = distr (μ M ν) real_borel real_real.f"
    (is "?lhs = ?rhs")
proof -
  interpret rd1: real_distribution μ by fact
  interpret rd2: real_distribution ν by fact
  interpret pp: pair_prob_space μ ν
    by (simp add: pair_prob_space.intro pair_sigma_finite_def rd1.prob_space_axioms rd1.sigma_finite_measure_axioms rd2.prob_space_axioms rd2.sigma_finite_measure_axioms)
  have "?lhs = μ  (λr. ν  (λl. distr (return (real_borel M real_borel) (r,l)) real_borel real_real.f))"
    using pair_return_return[of _ real_borel _ real_borel] by simp
  also have "... = μ  (λr. ν  (λl. distr (return (μ M ν) (r, l)) real_borel real_real.f))"
  proof -
    have "return (real_borel M real_borel) = return (μ M ν)"
      by(auto intro!: return_sets_cong sets_pair_measure_cong)
    thus ?thesis by simp
  qed
  also have "... = μ  (λr. distr (ν  (λl. (return (μ M ν) (r, l)))) real_borel real_real.f)"
    by(auto intro!: bind_cong distr_bind[symmetric,where K="μ M ν"])
  also have "... = distr (μ  (λr. ν  (λl. return (μ M ν) (r, l)))) real_borel real_real.f"
    by(auto intro!: distr_bind[symmetric,where K="μ M ν"])
  also have "... = ?rhs"
    by(simp add: pp.pair_measure_eq_bind[symmetric])
  finally show ?thesis .
qed

lemma(in pair_qbs_probs) qbs_bind_return_qp:
  shows "qbs_prob_space (Y, β, ν)  (λy. qbs_prob_space (X, α, μ)  (λx. qbs_return (X Q Y) (x,y))) = qbs_prob_space (X Q Y, map_prod α β  real_real.g, distr (μ M ν) real_borel real_real.f)"
        "qbs_prob (X Q Y) (map_prod α β  real_real.g) (distr (μ M ν) real_borel real_real.f)"
proof -
  show "qbs_prob_space (Y, β, ν)  (λy. qbs_prob_space (X, α, μ)  (λx. qbs_return (X Q Y) (x, y))) = qbs_prob_space (X Q Y, map_prod α β  real_real.g, distr (μ M ν) real_borel real_real.f)"
       (is "?lhs = ?rhs")
  proof -
    have "?lhs = qbs_prob_space (X Q Y, map_prod α β  real_real.g, ν  (λl. μ  (λr. distr (return real_borel r M return real_borel l) real_borel real_real.f)))"
    proof(auto intro!: qp2.qbs_bind_computation(2) measurable_bind_prob_space2[where N=real_borel] simp: in_Mx[simplified])
      show "(λy. qbs_prob_space (X, α, μ)  (λx. qbs_return (X Q Y) (x, y)))  Y Q monadP_qbs (X Q Y)"
        using qbs_morphism_const[of _ "monadP_qbs X" Y,simplified,OF qp1.qbs_prob_space_in_Px] curry_preserves_morphisms[OF qbs_morphism_pair_swap[OF qbs_return_morphism[of "X Q Y"]]]
        by (auto intro!: qbs_bind_morphism)
    next
      show "(λy. qbs_prob_space (X, α, μ)  (λx. qbs_return (X Q Y) (x, y)))  β = (λr. qbs_prob_space (X Q Y, map_prod α β  real_real.g, μ  (λl. distr (return real_borel l M return real_borel r) real_borel real_real.f)))"
        by standard
           (auto intro!: qp1.qbs_bind_computation(2) qbs_morphism_comp[OF qbs_morphism_Pair2[of _ Y] qbs_return_morphism[of "X Q Y"],simplified comp_def]
                  simp: in_Mx[simplified] qbs_return_Mxpair[OF qp1.in_Mx qp2.in_Mx] qbs_Mx_to_X(2))
    qed
    also have "... = ?rhs"
    proof -
      have "ν  (λl. μ  (λr. distr (return real_borel r M return real_borel l) real_borel real_real.f)) = distr (μ M ν) real_borel real_real.f"
        by(auto intro!: bind_rotate[symmetric,where N=real_borel] measurable_prob_algebraD
                  simp: bind_bind_return_distr[symmetric,OF qp1.real_distribution_axioms qp2.real_distribution_axioms])
      thus ?thesis by simp
    qed
    finally show ?thesis .
  qed
  show "qbs_prob (X Q Y) (map_prod α β  real_real.g) (distr (μ M ν) real_borel real_real.f)"
    by(rule qbs_prob_axioms)
qed

lemma(in pair_qbs_probs) qbs_bind_return_pq:
  shows "qbs_prob_space (X, α, μ)  (λx. qbs_prob_space (Y, β, ν)  (λy. qbs_return (X Q Y) (x,y))) = qbs_prob_space (X Q Y, map_prod α β  real_real.g, distr (μ M ν) real_borel real_real.f)"
        "qbs_prob (X Q Y) (map_prod α β  real_real.g) (distr (μ M ν) real_borel real_real.f)"
proof(simp_all add: qbs_bind_return_qp(2))
  show "qbs_prob_space (X, α, μ)  (λx. qbs_prob_space (Y, β, ν)  (λy. qbs_return (X Q Y) (x, y))) = qbs_prob_space (X Q Y, map_prod α β  real_real.g, distr (μ M ν) real_borel real_real.f)"
       (is "?lhs = _")
  proof -
    have "?lhs = qbs_prob_space (X Q Y, map_prod α β  real_real.g, μ  (λr. ν  (λl. distr (return real_borel r M return real_borel l) real_borel real_real.f)))"
    proof(auto intro!: qp1.qbs_bind_computation(2) measurable_bind_prob_space2[where N=real_borel])
      show "(λx. qbs_prob_space (Y, β, ν)  (λy. qbs_return (X Q Y) (x, y)))  X Q monadP_qbs (X Q Y)"
        using qbs_morphism_const[of _ "monadP_qbs Y" X,simplified,OF qp2.qbs_prob_space_in_Px] curry_preserves_morphisms[OF qbs_return_morphism[of "X Q Y"]]
        by(auto intro!: qbs_bind_morphism simp: curry_def)
    next
      show "(λx. qbs_prob_space (Y, β, ν)  (λy. qbs_return (X Q Y) (x, y)))  α = (λr. qbs_prob_space (X Q Y, map_prod α β  real_real.g, ν  (λl. distr (return real_borel r M return real_borel l) real_borel real_real.f)))"
        by standard
          (auto intro!: qp2.qbs_bind_computation(2) qbs_morphism_comp[OF qbs_morphism_Pair1[of _ X] qbs_return_morphism[of "X Q Y"],simplified comp_def]
                  simp:  qbs_return_Mxpair[OF qp1.in_Mx qp2.in_Mx] qbs_Mx_to_X(2))
    qed
    thus ?thesis
      by(simp add: bind_bind_return_distr[OF qp1.real_distribution_axioms qp2.real_distribution_axioms])
  qed
qed

lemma qbs_bind_return_rotate:
  assumes "p  monadP_qbs_Px X"
      and "q  monadP_qbs_Px Y"
    shows "q  (λy. p  (λx. qbs_return (X Q Y) (x,y))) = p  (λx. q  (λy. qbs_return (X Q Y) (x,y)))"
proof -
  obtain α μ where hp:
    "qbs_prob X α μ" "p = qbs_prob_space (X, α, μ)"
    using rep_monadP_qbs_Px[OF assms(1)] by auto
  obtain β ν where hq:
    "qbs_prob Y β ν" "q = qbs_prob_space (Y, β, ν)"
    using rep_monadP_qbs_Px[OF assms(2)] by auto
  interpret pqp: pair_qbs_probs X α μ Y β ν
    by(simp add: pair_qbs_probs_def hp hq)
  show ?thesis
    by(simp add: hp(2) hq(2) pqp.qbs_bind_return_pq(1) pqp.qbs_bind_return_qp)
qed

lemma qbs_pair_bind_return1:
  assumes "f   X Q Y Q monadP_qbs Z"
          "p  monadP_qbs_Px X"
      and "q  monadP_qbs_Px Y"
    shows "q  (λy. p  (λx. f (x,y))) = (q  (λy. p  (λx. qbs_return (X Q Y) (x,y))))  f"
          (is "?lhs = ?rhs")
proof -
  note [simp] = qbs_morphism_const[of _ "monadP_qbs X",simplified,OF assms(2)]
                qbs_morphism_Pair1'[OF _ assms(1)] qbs_morphism_Pair2'[OF _ assms(1)]
                curry_preserves_morphisms[OF qbs_morphism_pair_swap[OF qbs_return_morphism[of "X Q Y"]],simplified curry_def,simplified]
                qbs_morphism_Pair2'[OF _ qbs_return_morphism[of "X Q Y"]]
                arg_swap_morphism[OF curry_preserves_morphisms[OF assms(1)],simplified curry_def]
                curry_preserves_morphisms[OF qbs_morphism_comp[OF qbs_morphism_pair_swap[OF qbs_return_morphism[of "X Q Y"]] qbs_bind_morphism'[OF assms(1)]],simplified curry_def comp_def,simplified]
  have [simp]:"(λy. p  (λx. f (x,y)))  Y Q monadP_qbs Z"
              "(λy. p  (λx. qbs_return (X Q Y) (x,y)  f))  Y Q monadP_qbs Z"
    by(auto intro!: qbs_bind_morphism[where Y=X] simp: curry_def)
  have "?lhs = q  (λy. p  (λx. qbs_return (X Q Y) (x,y)  f))"
    by(auto intro!: qbs_bind_cong[OF assms(3),where Y=Z] qbs_bind_cong[OF assms(2),where Y=Z] simp: qbs_bind_return[OF assms(1)])
  also have "... = q  (λy. (p  (λx. qbs_return (X Q Y) (x,y)))  f)"
    by(auto intro!: qbs_bind_cong[OF assms(3),where Y=Z] qbs_bind_assoc[OF assms(2) _ assms(1)] simp: )
  also have "... = ?rhs"
    by(auto intro!: qbs_bind_assoc[OF assms(3)_ assms(1)] qbs_bind_morphism[where Y=X])
  finally show ?thesis .
qed

lemma qbs_pair_bind_return2:
  assumes "f   X Q Y Q monadP_qbs Z"
          "p  monadP_qbs_Px X"
      and "q  monadP_qbs_Px Y"
    shows "p  (λx. q  (λy. f (x,y))) = (p  (λx. q  (λy. qbs_return (X Q Y) (x,y))))  f"
          (is "?lhs = ?rhs")      
proof -
  note [simp] = qbs_morphism_const[of _ "monadP_qbs Y",simplified,OF assms(3)]
                qbs_morphism_Pair1'[OF _ assms(1)] curry_preserves_morphisms[OF assms(1),simplified curry_def]
                qbs_morphism_Pair1'[OF _ qbs_return_morphism[of "X