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

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"
begin

lemma qbs_prob_space_X[simp]:
"qbs_prob_space_qbs s = X"

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

lemma(in qbs_prob) qbs_prob_space_in_Px:

shows "∃α μ. s = qbs_prob_space (X, α, μ) ∧ qbs_prob X α μ"
using rep_qbs_prob_space' assms in_Px.qbs_prob_space_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

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))

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"
show "β r ∈ monadP_qbs_Px X"
qed

apply(rule qbs_closed1I)
subgoal for α f
apply auto
subgoal for β g
apply(auto intro!: bexI[where x=β] bexI[where x="g∘f"])
done
done
done

unfolding qbs_closed2_def
proof
fix s
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 μ]
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

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"
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))"
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 g⇩P⇩(⇩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]
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
interpret pps: pair_prob_space "return nat_borel (P r)" "g (P r) r"
using prob_space_return[of "P r" nat_borel]
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))"
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))"
also have "... = (∫⇧+x. f x ∂ (distr (g' r) (qbs_to_measure X) α'))"
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"
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"
qed

"qbs_space X = {} ⟷ qbs_space (monadP_qbs X) = {}"
proof auto
fix x
assume 1:"qbs_space X = {}"
then obtain α μ where "qbs_prob X α μ"
thus False
using empty_quasi_borel_iff[of X] qbs_empty_not_qbs_prob[of α μ] 1(1)
by auto
next
fix 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"
thus False
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 β
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) α"
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:
apply standard
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)"

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

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"
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]]

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))"

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' α' μ'
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]
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)"
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)))"
also have "... = μ' ⤜ (λx. (qbs_prob_measure ∘ f)  (α' x))"
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]
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)))"
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"
proof(rule qbs_morphismI,simp)
fix β
then obtain α g where hb:
"α ∈ qbs_Mx X" "g ∈ real_borel →⇩M prob_algebra real_borel"
"β = (λr. qbs_prob_space (X, α, g r))"
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"
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':
shows "x ⤜ qbs_return X = x"
proof -
obtain α μ where h1:"qbs_prob X α μ" "x = qbs_prob_space (X, α, μ)"
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, β, μ)"
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 μ
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:
"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, α, μ)"
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"
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 μ
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
qed

lemma qbs_bind_cong:
"⋀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, α, μ)"
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"

assumes "f ∈ X →⇩Q Y"
by(rule qbs_bind_morphism'[OF qbs_morphism_comp[OF assms qbs_return_morphism]])

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.›
shows "monadP_qbs_Pf X X id s = s"

"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, α, μ)"
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
show ?thesis
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:

lemma qbs_join_computation:
assumes "qbs_prob (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)" μ
(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"
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,β,ν)"
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)),ν)"

have "map_prod f (monadP_qbs_Pf Y Y' g) (x,sy) = (f x,qbs_prob_space (Y',g ∘ β,ν))"
"qbs_prob Y' (g ∘ β) ν"
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
qed

lemma qbs_strength_ab_r:
assumes "α ∈ qbs_Mx X"
"γ ∈ 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]
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)"
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'"
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"
then obtain γ g where hb:
"γ ∈ qbs_Mx Y" "g ∈ real_borel →⇩M prob_algebra real_borel"
"β = (λr. qbs_prob_space (Y, γ, g r))"
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"]
qed

lemma qbs_bind_morphism'':
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"
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

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
by(auto intro!: qbs_morphism_comp simp: qbs_strength_morphism)
qed

lemma qbs_bind_morphism''':
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'']

lemma qbs_bind_morphism'''':
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]
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:
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, β, μ)"
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"
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"
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)"
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
qed
qed

lemma qbs_bind_return_rotate:
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, α, μ)"
obtain β ν where hq:
"qbs_prob Y β ν" "q = qbs_prob_space (Y, β, ν)"
interpret pqp: pair_qbs_probs X α μ Y β ν
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"
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"
qbs_morphism_Pair1'[OF _ qbs_return_morphism[of "X ⨂`