# Theory Density_Predicates

(*
Theory: Density_Predicates.thy
Authors: Manuel Eberl
*)

section ‹Density Predicates›

theory Density_Predicates
imports "HOL-Probability.Probability"
begin

subsection ‹Probability Densities›

definition is_subprob_density :: "'a measure ⇒ ('a ⇒ ennreal) ⇒ bool" where
"is_subprob_density M f ≡ (f ∈ borel_measurable M) ∧ space M ≠ {} ∧
(∀x∈space M. f x ≥ 0) ∧ (∫⇧+x. f x ∂M) ≤ 1"

lemma is_subprob_densityI[intro]:
"⟦f ∈ borel_measurable M; ⋀x. x ∈ space M ⟹ f x ≥ 0; space M ≠ {}; (∫⇧+x. f x ∂M) ≤ 1⟧
⟹ is_subprob_density M f"
unfolding is_subprob_density_def by simp

lemma is_subprob_densityD[dest]:
"is_subprob_density M f ⟹ f ∈ borel_measurable M"
"is_subprob_density M f ⟹ x ∈ space M ⟹ f x ≥ 0"
"is_subprob_density M f ⟹ space M ≠ {}"
"is_subprob_density M f ⟹ (∫⇧+x. f x ∂M) ≤ 1"
unfolding is_subprob_density_def by simp_all

subsection ‹Measure spaces with densities›

definition has_density :: "'a measure ⇒ 'a measure ⇒ ('a ⇒ ennreal) ⇒ bool" where
"has_density M N f ⟷ (f ∈ borel_measurable N) ∧ space N ≠ {} ∧ M = density N f"

lemma has_densityI[intro]:
"⟦f ∈ borel_measurable N; M = density N f; space N ≠ {}⟧ ⟹ has_density M N f"
unfolding has_density_def by blast

lemma has_densityD:
assumes "has_density M N f"
shows "f ∈ borel_measurable N" "M = density N f" "space N ≠ {}"
using assms unfolding has_density_def by simp_all

lemma has_density_sets: "has_density M N f ⟹ sets M = sets N"
unfolding has_density_def by simp

lemma has_density_space: "has_density M N f ⟹ space M = space N"
unfolding has_density_def by simp

lemma has_density_emeasure:
"has_density M N f ⟹ X ∈ sets M ⟹ emeasure M X = ∫⇧+x. f x * indicator X x ∂N"
unfolding has_density_def by (simp_all add: emeasure_density)

lemma nn_integral_cong': "(⋀x. x ∈ space N =simp=> f x = g x) ⟹ (∫⇧+x. f x ∂N) = (∫⇧+x. g x ∂N)"
by (simp add: simp_implies_def cong: nn_integral_cong)

lemma has_density_emeasure_space:
"has_density M N f ⟹ emeasure M (space M) = (∫⇧+x. f x ∂N)"

lemma has_density_emeasure_space':
"has_density M N f ⟹ emeasure (density N f) (space (density N f)) = ∫⇧+x. f x ∂N"
by (frule has_densityD(2)[symmetric]) (simp add: has_density_emeasure_space)

lemma has_density_imp_is_subprob_density:
"⟦has_density M N f; (∫⇧+x. f x ∂N) = 1⟧ ⟹ is_subprob_density N f"
by (auto dest: has_densityD)

lemma has_density_imp_is_subprob_density':
"⟦has_density M N f; prob_space M⟧ ⟹ is_subprob_density N f"
by (auto intro!: has_density_imp_is_subprob_density dest: prob_space.emeasure_space_1
simp: has_density_emeasure_space)

lemma has_density_equal_on_space:
assumes "has_density M N f" "⋀x. x ∈ space N ⟹ f x = g x"
shows "has_density M N g"
proof
from assms show "g ∈ borel_measurable N"
by (subst measurable_cong[of _ _ f]) (auto dest: has_densityD)
with assms show "M = density N g"
by (subst density_cong[of _ _ f]) (auto dest: has_densityD)
from assms(1) show "space N ≠ {}" by (rule has_densityD)
qed

lemma has_density_cong:
assumes "⋀x. x ∈ space N ⟹ f x = g x"
shows "has_density M N f = has_density M N g"
using assms by (intro iffI) (erule has_density_equal_on_space, simp)+

lemma has_density_dens_AE:
"⟦AE y in N. f y = f' y; f' ∈ borel_measurable N;
⋀x. x ∈ space M ⟹ f' x ≥ 0; has_density M N f⟧
⟹ has_density M N f'"
unfolding has_density_def by (simp cong: density_cong)

subsection ‹Probability spaces with densities›

lemma is_subprob_density_imp_has_density:
"⟦is_subprob_density N f; M = density N f⟧ ⟹ has_density M N f"
by (rule has_densityI) auto

lemma has_subprob_density_imp_subprob_space':
"⟦has_density M N f; is_subprob_density N f⟧ ⟹ subprob_space M"
proof (rule subprob_spaceI)
assume "has_density M N f"
hence "M = density N f" by (simp add: has_density_def)
also from ‹has_density M N f› have "space ... ≠ {}" by (simp add: has_density_def)
finally show "space M ≠ {}" .
qed (auto simp add: has_density_emeasure_space dest: has_densityD)

lemma has_subprob_density_imp_subprob_space[dest]:
"is_subprob_density M f ⟹ subprob_space (density M f)"
by (rule has_subprob_density_imp_subprob_space') auto

definition "has_subprob_density M N f ≡ has_density M N f ∧ subprob_space M"

(* TODO: Move *)
lemma subprob_space_density_not_empty: "subprob_space (density M f) ⟹ space M ≠ {}"
by (subst space_density[symmetric], subst subprob_space.subprob_not_empty, assumption) simp

lemma has_subprob_densityI:
"⟦f ∈ borel_measurable N; M = density N f; subprob_space M⟧ ⟹ has_subprob_density M N f"
unfolding has_subprob_density_def by (auto simp: subprob_space_density_not_empty)

lemma has_subprob_densityI':
assumes "f ∈ borel_measurable N" "space N ≠ {}"
"M = density N f" "(∫⇧+x. f x ∂N) ≤ 1"
shows "has_subprob_density M N f"
proof-
from assms have D: "has_density M N f" by blast
moreover from D and assms have "subprob_space M"
by (auto intro!: subprob_spaceI simp: has_density_emeasure_space emeasure_density
cong: nn_integral_cong')
ultimately show ?thesis unfolding has_subprob_density_def by simp
qed

lemma has_subprob_densityD:
assumes "has_subprob_density M N f"
shows "f ∈ borel_measurable N" "⋀x. x ∈ space N ⟹ f x ≥ 0" "M = density N f" "subprob_space M"
using assms unfolding has_subprob_density_def by (auto dest: has_densityD)

lemma has_subprob_density_measurable[measurable_dest]:
"has_subprob_density M N f ⟹ f ∈ N →⇩M borel"
by (auto dest: has_subprob_densityD)

lemma has_subprob_density_imp_has_density:
"has_subprob_density M N f ⟹ has_density M N f" by (simp add: has_subprob_density_def)

lemma has_subprob_density_equal_on_space:
assumes "has_subprob_density M N f" "⋀x. x ∈ space N ⟹ f x = g x"
shows "has_subprob_density M N g"
using assms unfolding has_subprob_density_def by (auto dest: has_density_equal_on_space)

lemma has_subprob_density_cong:
assumes "⋀x. x ∈ space N ⟹ f x = g x"
shows "has_subprob_density M N f = has_subprob_density M N g"
using assms by (intro iffI) (erule has_subprob_density_equal_on_space, simp)+

lemma has_subprob_density_dens_AE:
"⟦AE y in N. f y = f' y; f' ∈ borel_measurable N;
⋀x. x ∈ space M ⟹ f' x ≥ 0; has_subprob_density M N f⟧
⟹ has_subprob_density M N f'"
unfolding has_subprob_density_def by (simp add: has_density_dens_AE)

subsection ‹Parametrized probability densities›

definition
"has_parametrized_subprob_density M N R f ≡
(∀x ∈ space M. has_subprob_density (N x) R (f x)) ∧ case_prod f ∈ borel_measurable (M ⨂⇩M R)"

lemma has_parametrized_subprob_densityI:
assumes "⋀x. x ∈ space M ⟹ N x = density R (f x)"
assumes "⋀x. x ∈ space M ⟹ subprob_space (N x)"
assumes "case_prod f ∈ borel_measurable (M ⨂⇩M R)"
shows "has_parametrized_subprob_density M N R f"
unfolding has_parametrized_subprob_density_def using assms
by (intro ballI conjI has_subprob_densityI) simp_all

lemma has_parametrized_subprob_densityD:
assumes "has_parametrized_subprob_density M N R f"
shows "⋀x. x ∈ space M ⟹ N x = density R (f x)"
and "⋀x. x ∈ space M ⟹ subprob_space (N x)"
and [measurable_dest]: "case_prod f ∈ borel_measurable (M ⨂⇩M R)"
using assms unfolding has_parametrized_subprob_density_def
by (auto dest: has_subprob_densityD)

lemma has_parametrized_subprob_density_integral:
assumes "has_parametrized_subprob_density M N R f" "x ∈ space M"
shows "(∫⇧+y. f x y ∂R) ≤ 1"
proof-
have "(∫⇧+y. f x y ∂R) = emeasure (density R (f x)) (space (density R (f x)))" using assms
by (auto simp: emeasure_density cong: nn_integral_cong' dest: has_parametrized_subprob_densityD)
also have "density R (f x) = (N x)" using assms by (auto dest: has_parametrized_subprob_densityD)
also have "emeasure ... (space ...) ≤ 1" using assms
by (subst subprob_space.emeasure_space_le_1) (auto dest: has_parametrized_subprob_densityD)
finally show ?thesis .
qed

lemma has_parametrized_subprob_density_cong:
assumes "⋀x. x ∈ space M ⟹ N x = N' x"
shows "has_parametrized_subprob_density M N R f = has_parametrized_subprob_density M N' R f"
using assms unfolding has_parametrized_subprob_density_def by auto

lemma has_parametrized_subprob_density_dens_AE:
assumes "⋀x. x ∈ space M ⟹ AE y in R. f x y = f' x y"
"case_prod f' ∈ borel_measurable (M ⨂⇩M R)"
"has_parametrized_subprob_density M N R f"
shows   "has_parametrized_subprob_density M N R f'"
unfolding has_parametrized_subprob_density_def
proof (intro conjI ballI)
fix x assume x: "x ∈ space M"
with assms(3) have "space (N x) = space R"
by (auto dest!: has_parametrized_subprob_densityD(1))
with assms and x show "has_subprob_density (N x) R (f' x)"
by (rule_tac has_subprob_density_dens_AE[of "f x"])
(auto simp: has_parametrized_subprob_density_def)
qed fact

subsection ‹Density in the Giry monad›

lemma emeasure_bind_density:
assumes "space M ≠ {}" "⋀x. x ∈ space M ⟹ has_density (f x) N (g x)"
"f ∈ measurable M (subprob_algebra N)" "X ∈ sets N"
shows "emeasure (M ⤜ f) X = ∫⇧+x. ∫⇧+y. g x y * indicator X y ∂N ∂M"
proof-
from assms have "emeasure (M ⤜ f) X = ∫⇧+x. emeasure (f x) X ∂M"
by (intro emeasure_bind)
also have "... = ∫⇧+x. ∫⇧+y. g x y * indicator X y ∂N ∂M" using assms
by (intro nn_integral_cong) (simp add: has_density_emeasure sets_kernel)
finally show ?thesis .
qed

lemma bind_density:
assumes "sigma_finite_measure M" "sigma_finite_measure N"
"space M ≠ {}" "⋀x. x ∈ space M ⟹ has_density (f x) N (g x)"
and [measurable]: "case_prod g ∈ borel_measurable (M ⨂⇩M N)" "f ∈ measurable M (subprob_algebra N)"
shows "(M ⤜ f) = density N (λy. ∫⇧+x. g x y ∂M)"
proof (rule measure_eqI)
interpret sfN: sigma_finite_measure N by fact
interpret sfNM: pair_sigma_finite N M unfolding pair_sigma_finite_def using assms by simp
show eq: "sets (M ⤜ f) = sets (density N (λy. ∫⇧+x. g x y ∂M))"
using sets_bind[OF sets_kernel[OF assms(6)] assms(3)] by auto
fix X assume "X ∈ sets (M ⤜ f)"
with eq have [measurable]: "X ∈ sets N" by auto
with assms have "emeasure (M ⤜ f) X = ∫⇧+x. ∫⇧+y. g x y * indicator X y ∂N ∂M"
by (intro emeasure_bind_density) simp_all
also from ‹X ∈ sets N› have "... = ∫⇧+y. ∫⇧+x. g x y * indicator X y ∂M ∂N"
by (intro sfNM.Fubini') measurable
also {
fix y assume "y ∈ space N"
have "(λx. g x y) = case_prod g ∘ (λx. (x, y))" by (rule ext) simp
also from ‹y ∈ space N› have "... ∈ borel_measurable M"
by (intro measurable_comp[OF _ assms(5)] measurable_Pair2')
finally have "(λx. g x y) ∈ borel_measurable M" .
}
hence "... = ∫⇧+y. (∫⇧+x. g x y ∂M) * indicator X y ∂N"
by (intro nn_integral_cong nn_integral_multc)  simp_all
also from ‹X ∈ sets N› and assms have "... = emeasure (density N (λy. ∫⇧+x. g x y ∂M)) X"
by (subst emeasure_density) (simp_all add: sfN.borel_measurable_nn_integral)
finally show "emeasure (M ⤜ f) X = emeasure (density N (λy. ∫⇧+x. g x y ∂M)) X" .
qed

lemma bind_has_density:
assumes "sigma_finite_measure M" "sigma_finite_measure N"
"space M ≠ {}" "⋀x. x ∈ space M ⟹ has_density (f x) N (g x)"
"case_prod g ∈ borel_measurable (M ⨂⇩M N)"
"f ∈ measurable M (subprob_algebra N)"
shows "has_density (M ⤜ f) N (λy. ∫⇧+x. g x y ∂M)"
proof
interpret sigma_finite_measure M by fact
show "(λy. ∫⇧+ x. g x y ∂M) ∈ borel_measurable N" using assms
by (intro borel_measurable_nn_integral, subst measurable_pair_swap_iff) simp
show "M ⤜ f = density N (λy. ∫⇧+ x. g x y ∂M)"
by (intro bind_density) (simp_all add: assms)
from ‹space M ≠ {}› obtain x where "x ∈ space M" by blast
with assms have "has_density (f x) N (g x)" by simp
thus "space N ≠ {}" by (rule has_densityD)
qed

lemma bind_has_density':
assumes sfM: "sigma_finite_measure M"
and sfR: "sigma_finite_measure R"
and not_empty: "space M ≠ {}" and dens_M: "has_density M N δM"
and dens_f: "⋀x. x ∈ space M ⟹ has_density (f x) R (δf x)"
and Mδf: "case_prod δf ∈ borel_measurable (N ⨂⇩M R)"
and Mf: "f ∈ measurable N (subprob_algebra R)"
shows "has_density (M ⤜ f) R (λy. ∫⇧+x. δM x * δf x y ∂N)"
proof-
from dens_M have M_M: "measurable M = measurable N"
by (intro ext measurable_cong_sets) (auto dest: has_densityD)
from dens_M have M_MR: "measurable (M ⨂⇩M R) = measurable (N ⨂⇩M R)"
by (intro ext measurable_cong_sets sets_pair_measure_cong) (auto dest: has_densityD)
have "has_density (M ⤜ f) R (λy. ∫⇧+x. δf x y ∂M)"
by (rule bind_has_density) (auto simp: assms M_MR M_M)
moreover {
fix y assume A: "y ∈ space R"
have "(λx. δf x y) = case_prod δf ∘ (λx. (x,y))" by (rule ext) (simp add: o_def)
also have "... ∈ borel_measurable N" by (intro measurable_comp[OF _ Mδf] measurable_Pair2' A)
finally have M_δf': "(λx. δf x y) ∈ borel_measurable N" .

from dens_M have "M = density N δM" by (auto dest: has_densityD)
also from dens_M have "(∫⇧+x. δf x y ∂...) = ∫⇧+x. δM x * δf x y ∂N"
by (subst nn_integral_density) (auto dest: has_densityD simp: M_δf')
finally have "(∫⇧+x. δf x y ∂M) = ∫⇧+x. δM x * δf x y ∂N" .
}
ultimately show "has_density (M ⤜ f) R (λy. ∫⇧+x. δM x * δf x y ∂N)"
by (rule has_density_equal_on_space) simp_all
qed

lemma bind_has_subprob_density:
assumes "subprob_space M" "sigma_finite_measure N"
"space M ≠ {}" "⋀x. x ∈ space M ⟹ has_density (f x) N (g x)"
"case_prod g ∈ borel_measurable (M ⨂⇩M N)"
"f ∈ measurable M (subprob_algebra N)"
shows "has_subprob_density (M ⤜ f) N (λy. ∫⇧+x. g x y ∂M)"
proof (unfold has_subprob_density_def, intro conjI)
from assms show "has_density (M ⤜ f) N (λy. ∫⇧+x. g x y ∂M)"
by (intro bind_has_density) (auto simp: subprob_space_imp_sigma_finite)
from assms show "subprob_space (M ⤜ f)" by (intro subprob_space_bind)
qed

lemma bind_has_subprob_density':
assumes "has_subprob_density M N δM" "space R ≠ {}" "sigma_finite_measure R"
"⋀x. x ∈ space M ⟹ has_subprob_density (f x) R (δf x)"
"case_prod δf ∈ borel_measurable (N ⨂⇩M R)" "f ∈ measurable N (subprob_algebra R)"
shows "has_subprob_density (M ⤜ f) R (λy. ∫⇧+x. δM x * δf x y ∂N)"
proof (unfold has_subprob_density_def, intro conjI)
from assms(1) have "space M ≠ {}" by (intro subprob_space.subprob_not_empty has_subprob_densityD)
with assms show "has_density (M ⤜ f) R (λy. ∫⇧+x. δM x * δf x y ∂N)"
by (intro bind_has_density' has_densityI)
(auto simp: subprob_space_imp_sigma_finite dest: has_subprob_densityD)
from assms show "subprob_space (M ⤜ f)"
by (intro subprob_space_bind) (auto dest: has_subprob_densityD)
qed

lemma null_measure_has_subprob_density:
"space M ≠ {} ⟹ has_subprob_density (null_measure M) M (λ_. 0)"
by (intro has_subprob_densityI)
(auto intro: null_measure_eq_density simp: subprob_space_null_measure_iff)

lemma emeasure_has_parametrized_subprob_density:
assumes "has_parametrized_subprob_density M N R f"
assumes "x ∈ space M" "X ∈ sets R"
shows "emeasure (N x) X = ∫⇧+y. f x y * indicator X y ∂R"
proof-
from has_parametrized_subprob_densityD(3)[OF assms(1)] and assms(2)
have Mf: "f x ∈ borel_measurable R" by simp
have "N x = density R (f x)"
by (rule has_parametrized_subprob_densityD(1)[OF assms(1,2)])
also from Mf and assms(3) have "emeasure ... X = ∫⇧+y. f x y * indicator X y ∂R"
by (rule emeasure_density)
finally show ?thesis .
qed

lemma emeasure_count_space_density_singleton:
assumes "x ∈ A" "has_density M (count_space A) f"
shows "emeasure M {x} = f x"
proof-
from has_densityD[OF assms(2)] have nonneg: "⋀x. x ∈ A ⟹ f x ≥ 0" by simp
from assms have M: "M = density (count_space A) f" by (intro has_densityD)
from assms have "emeasure M {x} = ∫⇧+y. f y * indicator {x} y ∂count_space A"
also from assms and nonneg have "... = f x"
by (subst nn_integral_indicator_singleton) auto
finally show ?thesis .
qed

lemma subprob_count_space_density_le_1:
assumes "has_subprob_density M (count_space A) f" "x ∈ A"
shows "f x ≤ 1"
proof (cases "f x > 0")
assume "f x > 0"
from assms interpret subprob_space M by (intro has_subprob_densityD)
from assms have M: "M = density (count_space A) f" by (intro has_subprob_densityD)
from assms have "f x = emeasure M {x}"
by (intro emeasure_count_space_density_singleton[symmetric])
(auto simp: has_subprob_density_def)
also have "... ≤ 1" by (rule subprob_emeasure_le_1)
finally show ?thesis .
qed (auto simp: not_less intro: order.trans[of _ 0 1])

lemma has_density_embed_measure:
assumes inj: "inj f" and inv: "⋀x. x ∈ space N ⟹ f' (f x) = x"
shows "has_density (embed_measure M f) (embed_measure N f) (δ ∘ f') ⟷ has_density M N δ"
(is "has_density ?M' ?N' ?δ' ⟷ has_density M N δ")
proof
assume dens: "has_density ?M' ?N' ?δ'"
show "has_density M N δ"
proof
from dens show "space N ≠ {}" by (auto simp: space_embed_measure dest: has_densityD)
from dens have Mδf': "δ ∘ f' ∈ borel_measurable ?N'" by (rule has_densityD)
hence Mδf'f: "δ ∘ f' ∘ f ∈ borel_measurable N"
by (rule_tac measurable_comp, rule_tac measurable_embed_measure2[OF inj])
thus Mδ: "δ ∈ borel_measurable N" by (simp cong: measurable_cong add: inv)
from dens have "embed_measure M f = density (embed_measure N f) (δ ∘ f')" by (rule has_densityD)
also have "... = embed_measure (density N (δ ∘ f' ∘ f)) f"
by (simp only: density_embed_measure[OF inj Mδf'])
also have "density N (δ ∘ f' ∘ f) = density N δ"
by (intro density_cong[OF Mδf'f Mδ]) (simp_all add: inv)
finally show "M = density N δ" by (simp add: embed_measure_eq_iff[OF inj])
qed
next
assume dens: "has_density M N δ"
show "has_density ?M' ?N' ?δ'"
proof
from dens show "space ?N' ≠ {}" by (auto simp: space_embed_measure dest: has_densityD)
have Mf'f: "(λx. f' (f x)) ∈ measurable N N" by (subst measurable_cong[OF inv]) simp_all
from dens have Mδ: "δ ∈ borel_measurable N" by (auto dest: has_densityD)
from Mf'f and dens show Mδf': "δ ∘ f' ∈ borel_measurable (embed_measure N f)"
by (intro measurable_comp) (erule measurable_embed_measure1, rule has_densityD)
have "embed_measure M f = embed_measure (density N δ) f"
by (simp only: has_densityD[OF dens])
also from inv and dens and measurable_comp[OF Mf'f Mδ]
have "density N δ = density N (?δ' ∘ f)"
also have "embed_measure (density N (?δ' ∘ f)) f = density (embed_measure N f) (δ ∘ f')"
by (simp only: density_embed_measure[OF inj Mδf', symmetric])
finally show "embed_measure M f = density (embed_measure N f) (δ ∘ f')" .
qed
qed

lemma has_density_embed_measure':
assumes inj: "inj f" and inv: "⋀x. x ∈ space N ⟹ f' (f x) = x" and
sets_M: "sets M = sets (embed_measure N f)"
shows "has_density (distr M N f') N (δ ∘ f) ⟷ has_density M (embed_measure N f) δ"
proof-
have sets': "sets (embed_measure (distr M N f') f) = sets (embed_measure N f)"
have Mff': "(λx. f' (f x)) ∈ measurable N N" by (subst measurable_cong[OF inv]) simp_all
have inv': "⋀x. x ∈ space M ⟹ f (f' x) = x"
by (subst (asm) sets_eq_imp_space_eq[OF sets_M]) (auto simp: space_embed_measure inv)
have "M = distr M (embed_measure (distr M N f') f) (λx. f (f' x))"
by (subst distr_cong[OF refl _ inv', of _ M]) (simp_all add: sets_embed_measure inj sets_M)
also have "... = embed_measure (distr M N f') f"
apply (subst (2) embed_measure_eq_distr[OF inj], subst distr_distr)
apply (subst measurable_cong_sets[OF refl sets'], rule measurable_embed_measure2[OF inj])
apply (subst measurable_cong_sets[OF sets_M refl], rule measurable_embed_measure1, rule Mff')
apply (simp cong: distr_cong add: inv)
done
finally have M: "M = embed_measure (distr M N f') f" .
show ?thesis by (subst (2) M, subst has_density_embed_measure[OF inj inv, symmetric])
(auto simp: space_embed_measure inv intro!: has_density_cong)
qed

lemma has_density_embed_measure'':
assumes inj: "inj f" and inv: "⋀x. x ∈ space N ⟹ f' (f x) = x" and
"has_density M (embed_measure N f) δ"
shows "has_density (distr M N f') N (δ ∘ f)"
proof (subst has_density_embed_measure')
from assms(3) show "sets M = sets (embed_measure N f)" by (auto dest: has_densityD)
qed (insert assms)

lemma has_subprob_density_embed_measure'':
assumes inj: "inj f" and inv: "⋀x. x ∈ space N ⟹ f' (f x) = x" and
"has_subprob_density M (embed_measure N f) δ"
shows "has_subprob_density (distr M N f') N (δ ∘ f)"
proof (unfold has_subprob_density_def, intro conjI)
from assms show "has_density (distr M N f') N (δ ∘ f)"
by (intro has_density_embed_measure'' has_subprob_density_imp_has_density)
from assms(3) have "sets M = sets (embed_measure N f)" by (auto dest: has_subprob_densityD)
hence M: "measurable M = measurable (embed_measure N f)"
by (intro ext measurable_cong_sets) simp_all
have "(λx. f' (f x)) ∈ measurable N N" by (simp cong: measurable_cong add: inv)
moreover from assms have "space (embed_measure N f) ≠ {}"
unfolding has_subprob_density_def has_density_def by simp
ultimately show "subprob_space (distr M N f')" using assms
by (intro subprob_space.subprob_space_distr has_subprob_densityD)
(auto simp: M space_embed_measure intro!: measurable_embed_measure1 dest: has_subprob_densityD)
qed (insert assms)

end


# Theory PDF_Transformations

(*
Theory: PDF_Transformations.thy
Author: Manuel Eberl

Provides lemmas for transformations of measure spaces with a density.
*)

section ‹Measure Space Transformations›

theory PDF_Transformations
imports Density_Predicates
begin

lemma not_top_le_1_ennreal[simp]: "¬ top ≤ (1::ennreal)"

lemma range_int: "range int = {n. n ≥ 0}"
proof (intro equalityI subsetI)
fix n :: int assume "n ∈ {n. n ≥ 0}"
hence "n = int (nat n)" by simp
thus "n ∈ range int" by blast
qed auto

lemma range_exp: "range (exp :: real ⇒ real) = {x. x > 0}"
proof (intro equalityI subsetI)
fix x :: real assume "x ∈ {x. x > 0}"
hence "x = exp (ln x)" by simp
thus "x ∈ range exp" by blast
qed auto

lemma Int_stable_Icc: "Int_stable (range (λ(a, b). {a .. b::real}))"
by (auto simp: Int_stable_def)

lemma distr_mult_real:
assumes "c ≠ 0" "has_density M lborel (f :: real ⇒ ennreal)"
shows "has_density (distr M borel ((*) c)) lborel (λx. f (x / c) * inverse (abs c))"
(is "has_density ?M' _ ?f'")
proof
from assms(2) have "M = density lborel f" by (rule has_densityD)
also from assms have Mf[measurable]: "f ∈ borel_measurable borel"
by (auto dest: has_densityD)
hence "distr (density lborel f) borel ((*) c) = density lborel ?f'" (is "?M1 = ?M2")
proof (intro measure_eqI)
fix X assume X[measurable]: "X ∈ sets (distr (density lborel f) borel ((*) c))"
with assms have "emeasure ?M1 X = ∫⇧+x. f x * indicator X (c * x) ∂lborel"
by (subst emeasure_distr, simp, simp, subst emeasure_density)
(auto dest: has_densityD intro!: measurable_sets_borel nn_integral_cong
split: split_indicator)
also from assms(1) and X have "... = ∫⇧+x. ?f' x * indicator X x ∂lborel"
apply (subst lborel_distr_mult'[of "inverse c"])
apply simp
apply (subst nn_integral_density)
done
also from X have "... = emeasure ?M2 X"
by (subst emeasure_density) auto
finally show "emeasure ?M1 X = emeasure ?M2 X" .
qed simp
finally show "distr M borel ((*) c) = density lborel ?f'" .
qed (insert assms, auto dest: has_densityD)

lemma distr_uminus_real:
assumes "has_density M lborel (f :: real ⇒ ennreal)"
shows "has_density (distr M borel uminus) lborel (λx. f (- x))"
proof-
from assms have "has_density (distr M borel ((*) (- 1))) lborel
(λx. f (x / -1) * ennreal (inverse (abs (-1))))"
by (intro distr_mult_real) simp_all
also have "(*) (-1) = (uminus :: real ⇒ real)" by (intro ext) simp
also have "(λx. f (x / -1) * ennreal (inverse (abs (-1)))) = (λx. f (-x))"
by (intro ext) (simp add: one_ennreal_def[symmetric])
finally show ?thesis .
qed

lemma distr_plus_real:
assumes "has_density M lborel (f :: real ⇒ ennreal)"
shows "has_density (distr M borel ((+) c)) lborel (λx. f (x - c))"
proof
from assms have "M = density lborel f" by (rule has_densityD)
also from assms have Mf[measurable]: "f ∈ borel_measurable borel"
by (auto dest: has_densityD)
hence "distr (density lborel f) borel ((+) c) = density lborel (λx. f (x - c))" (is "?M1 = ?M2")
proof (intro measure_eqI)
fix X assume X: "X ∈ sets (distr (density lborel f) borel ((+) c))"
with assms have "emeasure ?M1 X = ∫⇧+x. f x * indicator X (c + x) ∂lborel"
by (subst emeasure_distr, simp, simp, subst emeasure_density)
(auto dest: has_densityD intro!: measurable_sets_borel nn_integral_cong
split: split_indicator)
also from X have "... = ∫⇧+x. f (x - c) * indicator X x ∂lborel"
by (subst lborel_distr_plus[where c = "-c", symmetric], subst nn_integral_distr) auto
also from X have "... = emeasure ?M2 X"
by (subst emeasure_density)
(auto simp: emeasure_density intro!: measurable_compose[OF borel_measurable_diff Mf])
finally show "emeasure ?M1 X = emeasure ?M2 X" .
qed simp
finally show "distr M borel ((+) c) = density lborel (λx. f (x - c))" .
qed (insert assms, auto dest: has_densityD)

lemma count_space_uminus:
"count_space UNIV = distr (count_space UNIV) (count_space UNIV) (uminus :: ('a :: ring ⇒ _))"
proof (rule distr_bij_count_space[symmetric])
show "bij (uminus :: 'a ⇒ 'a)"
by (auto intro!: o_bij[where g=uminus])
qed

lemma count_space_plus:
"count_space UNIV = distr (count_space UNIV) (count_space UNIV) ((+) (c :: ('a :: ring)))"
by (rule distr_bij_count_space [symmetric]) simp

lemma distr_uminus_ring_count_space:
assumes "has_density M (count_space UNIV) (f :: _ :: ring ⇒ ennreal)"
shows "has_density (distr M (count_space UNIV) uminus) (count_space UNIV) (λx. f (- x))"
proof
from assms have "M = density (count_space UNIV) f" by (rule has_densityD)
also have "distr (density (count_space UNIV) f) (count_space UNIV) uminus =
density (count_space UNIV)(λx. f (- x))" (is "?M1 = ?M2")
proof (intro measure_eqI)
fix X assume X: "X ∈ sets (distr (density (count_space UNIV) f) (count_space UNIV) uminus)"
with assms have "emeasure ?M1 X = ∫⇧+x. f x * indicator X (-x) ∂count_space UNIV"
by (subst emeasure_distr, simp, simp, subst emeasure_density)
(auto dest: has_densityD intro!: measurable_sets_borel nn_integral_cong
split: split_indicator)
also from X have "... = emeasure ?M2 X"
by (subst count_space_uminus) (simp_all add: nn_integral_distr emeasure_density)
finally show "emeasure ?M1 X = emeasure ?M2 X" .
qed simp
finally show "distr M (count_space UNIV) uminus = density (count_space UNIV) (λx. f (- x))" .
qed (insert assms, auto dest: has_densityD)

lemma distr_plus_ring_count_space:
assumes "has_density M (count_space UNIV) (f :: _ :: ring ⇒ ennreal)"
shows "has_density (distr M (count_space UNIV) ((+) c)) (count_space UNIV) (λx. f (x - c))"
proof
from assms have "M = density (count_space UNIV) f" by (rule has_densityD)
also have "distr (density (count_space UNIV) f) (count_space UNIV) ((+) c) =
density (count_space UNIV)(λx. f (x - c))" (is "?M1 = ?M2")
proof (intro measure_eqI)
fix X assume X: "X ∈ sets (distr (density (count_space UNIV) f) (count_space UNIV) ((+) c))"
with assms have "emeasure ?M1 X = ∫⇧+x. f x * indicator X (c + x) ∂count_space UNIV"
by (subst emeasure_distr, simp, simp, subst emeasure_density)
(auto dest: has_densityD intro!: measurable_sets_borel nn_integral_cong
split: split_indicator)
also from X have "... = emeasure ?M2 X"
by (subst count_space_plus[of "-c"]) (simp_all add: nn_integral_distr emeasure_density)
finally show "emeasure ?M1 X = emeasure ?M2 X" .
qed simp
finally show "distr M (count_space UNIV) ((+) c) = density (count_space UNIV) (λx. f (x - c))" .
qed (insert assms, auto dest: has_densityD)

lemma subprob_density_distr_real_eq:
assumes dens: "has_subprob_density M lborel f"
assumes Mh: "h ∈ borel_measurable borel"
assumes Mg: "g ∈ borel_measurable borel"
assumes measure_eq:
"⋀a b. a ≤ b ⟹ emeasure (distr (density lborel f) lborel h) {a..b} =
emeasure (density lborel g) {a..b}"
shows "has_subprob_density (distr M borel (h :: real ⇒ real)) lborel g"
proof (rule has_subprob_densityI)
from dens have sets_M: "sets M = sets borel" by (auto dest: has_subprob_densityD)
have meas_M[simp]: "measurable M = measurable borel"
by (intro ext, subst measurable_cong_sets[OF sets_M refl]) auto
from Mh and dens show subprob_space: "subprob_space (distr M borel h)"
by (intro subprob_space.subprob_space_distr) (auto dest: has_subprob_densityD)
show "distr M borel h = density lborel g"
proof (rule measure_eqI_generator_eq[OF Int_stable_Icc, of UNIV])
{
fix x :: real
obtain n :: nat where "n > abs x" using reals_Archimedean2 by auto
hence "∃n::nat. x ∈ {-real n..real n}" by (intro exI[of _ n]) auto
}
thus "(⋃i::nat. {-real i..real i}) = UNIV" by blast
next
fix i :: nat
from subprob_space have "emeasure (distr M borel h) {-real i..real i} ≤ 1"
by (intro subprob_space.subprob_emeasure_le_1) (auto dest: has_subprob_densityD)
thus "emeasure (distr M borel h) {- real i..real i} ≠ ∞" by auto
next
fix X :: "real set" assume "X ∈ range (λ(a,b). {a..b})"
then obtain a b where "X = {a..b}" by auto
with dens have "emeasure (distr M lborel h) X = emeasure (density lborel g) X"
by (cases "a ≤ b") (auto simp: measure_eq dest: has_subprob_densityD)
also have "distr M lborel h = distr M borel h"
by (rule distr_cong) auto
finally show "emeasure (distr M borel h) X = emeasure (density lborel g) X" .
qed (auto simp: borel_eq_atLeastAtMost)
qed (insert assms, auto)

lemma subprob_density_distr_real_exp:
assumes dens: "has_subprob_density M lborel f"
shows "has_subprob_density (distr M borel exp) lborel
(λx. if x > 0 then f (ln x) * ennreal (inverse x) else 0)"
(is "has_subprob_density _ _ ?g")
proof (rule subprob_density_distr_real_eq[OF dens])
from dens have [measurable]: "f ∈ borel_measurable borel"
by (auto dest: has_subprob_densityD)

have Mf: "(λx. f (ln x) * ennreal (inverse x)) ∈ borel_measurable borel" by simp

fix a b :: real assume "a ≤ b"

let ?A = "λi. {inverse (Suc i) :: real ..}"
let ?M1 = "distr (density lborel f) lborel exp" and ?M2 = "density lborel ?g"
{
fix x :: real assume "∀i. x < inverse (Suc i)"
hence "x ≤ 0" by (intro tendsto_lowerbound[OF LIMSEQ_inverse_real_of_nat])
(auto intro!: always_eventually less_imp_le)
}
hence decomp: "{a..b} = {x∈{a..b}. x ≤ 0} ∪ (⋃i. ?A i ∩ {a..b})" (is "_ = ?C ∪ ?D")
by (auto simp: not_le)
have inv_le: "⋀x i. x ≥ inverse (real (Suc i)) ⟹ ¬(x ≤ 0)"
by (subst not_le, erule dual_order.strict_trans1, simp)
hence "emeasure ?M1 {a..b} = emeasure ?M1 ?C + emeasure ?M1 ?D"
by (subst decomp, intro plus_emeasure[symmetric]) auto
also have "emeasure ?M1 ?C = 0" by (subst emeasure_distr) auto
also have "0 = emeasure ?M2 ?C"
by (subst emeasure_density, simp, simp, rule sym, subst nn_integral_0_iff) auto
also have "emeasure ?M1 (⋃i. ?A i ∩ {a..b}) = (SUP i. emeasure ?M1 (?A i ∩ {a..b}))"
by (rule SUP_emeasure_incseq[symmetric])
(auto simp: incseq_def max_def not_le dest: order.strict_trans1)
also have "⋀i. emeasure ?M1 (?A i ∩ {a..b}) = emeasure ?M2 (?A i ∩ {a..b})"
proof (case_tac "inverse (Suc i) ≤ b")
fix i assume True: "inverse (Suc i) ≤ b"
let ?a = "inverse (Suc i)"
from ‹a ≤ b› have A: "?A i ∩ {a..b} = {max ?a a..b}" (is "?E = ?F") by auto
hence "emeasure ?M1 ?E = emeasure ?M1 ?F" by simp
also have "strict_mono_on ln {max (inverse (real (Suc i))) a..b}"
by (rule strict_mono_onI, subst ln_less_cancel_iff)
(auto dest: inv_le simp del: of_nat_Suc)
with ‹a ≤ b› True dens
have "emeasure ?M1 ?F = emeasure (density lborel (λx. f (ln x) * inverse x)) ?F"
by (intro emeasure_density_distr_interval)
(auto simp: Mf not_less not_le range_exp dest: has_subprob_densityD dest!: inv_le
intro!: DERIV_ln continuous_on_inverse continuous_on_id simp del: of_nat_Suc)
also note A[symmetric]
also have "emeasure (density lborel (λx. f (ln x) * inverse x)) ?E = emeasure ?M2 ?E"
by (subst (1 2) emeasure_density)
(auto intro!: nn_integral_cong split: split_indicator dest!: inv_le simp del: of_nat_Suc)
finally show "emeasure ?M1 (?A i ∩ {a..b}) = emeasure ?M2 (?A i ∩ {a..b})" .
qed simp
hence "(SUP i. emeasure ?M1 (?A i ∩ {a..b})) = (SUP i. emeasure ?M2 (?A i ∩ {a..b}))" by simp
also have "... = emeasure ?M2 (⋃i. ?A i ∩ {a..b})"
by (rule SUP_emeasure_incseq)
(auto simp: incseq_def max_def not_le dest: order.strict_trans1)
also have "emeasure ?M2 ?C + emeasure ?M2 ?D = emeasure ?M2 (?C ∪ ?D)"
by (rule plus_emeasure) (auto dest: inv_le simp del: of_nat_Suc)
also note decomp[symmetric]
finally show "emeasure ?M1 {a..b} = emeasure ?M2 {a..b}" .
qed (insert dens, auto dest!: has_subprob_densityD(1))

lemma subprob_density_distr_real_inverse_aux:
assumes dens: "has_subprob_density M lborel f"
shows "has_subprob_density (distr M borel (λx. - inverse x)) lborel
(λx. f (-inverse x) * ennreal (inverse (x * x)))"
(is "has_subprob_density _ _ ?g")
proof (rule subprob_density_distr_real_eq[OF dens])
from dens have Mf[measurable]: "f ∈ borel_measurable borel" by (auto dest: has_subprob_densityD)
show Mg: "?g ∈ borel_measurable borel" by measurable

have surj[simp]: "surj (λx. - inverse x :: real)"
by (intro surjI[of _ "λx. - inverse x"]) (simp add: field_simps)
fix a b :: real assume "a ≤ b"
let ?A1 = "λi. {..-inverse (Suc i) :: real}" and  ?A2 = "λi. {inverse (Suc i) :: real ..}"
let ?C = "if 0 ∈ {a..b} then {0} else {}"
let ?M1 = "distr (density lborel f) lborel (λx. - inverse x)" and ?M2 = "density lborel ?g"
have inv_le: "⋀x i. x ≥ inverse (real (Suc i)) ⟹ ¬(x ≤ 0)"
by (subst not_le, erule dual_order.strict_trans1, simp)
have "⋀x. x > 0 ⟹ ∃i. x ≥ inverse (Suc i)"
proof (rule ccontr)
fix x :: real assume "x > 0" "¬(∃i. x ≥ inverse (Suc i))"
hence "x ≤ 0" by (intro tendsto_lowerbound[OF LIMSEQ_inverse_real_of_nat])
(auto intro!: always_eventually less_imp_le simp: not_le)
with ‹x > 0› show False by simp
qed
hence A: "(⋃i. ?A2 i) = {0<..}" by (auto dest: inv_le simp del: of_nat_Suc)
moreover have "⋀x. x < 0 ⟹ ∃i. x ≤ -inverse (Suc i)"
proof (rule ccontr)
fix x :: real assume "x < 0" "¬(∃i. x ≤ -inverse (Suc i))"
hence "x ≥ 0"
by (intro tendsto_upperbound, simp)
(auto intro!: always_eventually less_imp_le LIMSEQ_inverse_real_of_nat_add_minus simp: not_le)
with ‹x < 0› show False by simp
qed
hence B: "(⋃i. ?A1 i) = {..<0}"
by (auto simp: le_minus_iff[of _ "inverse x" for x] dest!: inv_le simp del: of_nat_Suc)
ultimately have C: "UNIV = (⋃i. ?A1 i) ∪ (⋃i. ?A2 i) ∪ {0}" by (subst A, subst B) force
have UN_Int_distrib: "⋀f A. (⋃i. f i) ∩ A = (⋃i. f i ∩ A)" by blast
have decomp: "{a..b} = (⋃i. ?A1 i ∩ {a..b}) ∪ (⋃i. ?A2 i ∩ {a..b}) ∪ ?C" (is "_ = ?D ∪ ?E ∪ _")
by (subst Int_UNIV_left[symmetric], simp only: C Int_Un_distrib2 UN_Int_distrib)
(simp split: if_split)
have "emeasure ?M1 {a..b} = emeasure ?M1 ?D + emeasure ?M1 ?E + emeasure ?M1 ?C"
apply (subst decomp)
apply (subst plus_emeasure[symmetric], simp, simp, simp)
apply (subst plus_emeasure[symmetric])
apply (auto dest!: inv_le simp: not_le le_minus_iff[of _ "inverse x" for x] simp del: of_nat_Suc)
done
also have "(λx. - inverse x) - {0 :: real} = {0}" by (auto simp: field_simps)
hence "emeasure ?M1 ?C = 0"
by (subst emeasure_distr)  (auto split: if_split simp: emeasure_density Mf)
also have "emeasure ?M2 {0} = 0" by (simp add: emeasure_density)
hence "0 = emeasure ?M2 ?C"
by (rule_tac sym, rule_tac order.antisym, rule_tac order.trans, rule_tac emeasure_mono[of _ "{0}"]) simp_all
also have "emeasure ?M1 (⋃i. ?A1 i ∩ {a..b}) = (SUP i. emeasure ?M1 (?A1 i ∩ {a..b}))"
by (rule SUP_emeasure_incseq[symmetric])
(auto simp: incseq_def max_def not_le dest: order.strict_trans1)
also have "⋀i. emeasure ?M1 (?A1 i ∩ {a..b}) = emeasure ?M2 (?A1 i ∩ {a..b})"
proof (case_tac "-inverse (Suc i) ≥ a")
fix i assume True: "-inverse (Suc i) ≥ a"
let ?a = "-inverse (Suc i)"
from ‹a ≤ b› have A: "?A1 i ∩ {a..b} = {a..min ?a b}" (is "?F = ?G") by auto
hence "emeasure ?M1 ?F = emeasure ?M1 ?G" by simp
also have "strict_mono_on (λx. -inverse x) {a..min ?a b}"
by (rule strict_mono_onI)
(auto simp: le_minus_iff[of _ "inverse x" for x] dest!: inv_le simp del: of_nat_Suc)
with ‹a ≤ b› True dens
have "emeasure ?M1 ?G = emeasure ?M2 ?G"
by (intro emeasure_density_distr_interval)
(auto simp: Mf not_less dest: has_subprob_densityD inv_le
intro!: derivative_eq_intros continuous_on_mult continuous_on_inverse continuous_on_id)
also note A[symmetric]
finally show "emeasure ?M1 (?A1 i ∩ {a..b}) = emeasure ?M2 (?A1 i ∩ {a..b})" .
qed simp
hence "(SUP i. emeasure ?M1 (?A1 i ∩ {a..b})) = (SUP i. emeasure ?M2 (?A1 i ∩ {a..b}))" by simp
also have "... = emeasure ?M2 (⋃i. ?A1 i ∩ {a..b})"
by (rule SUP_emeasure_incseq)
(auto simp: incseq_def max_def not_le dest: order.strict_trans1)
also have "emeasure ?M1 (⋃i. ?A2 i ∩ {a..b}) = (SUP i. emeasure ?M1 (?A2 i ∩ {a..b}))"
by (rule SUP_emeasure_incseq[symmetric])
(auto simp: incseq_def max_def not_le dest: order.strict_trans1)
also have "⋀i. emeasure ?M1 (?A2 i ∩ {a..b}) = emeasure ?M2 (?A2 i ∩ {a..b})"
proof (case_tac "inverse (Suc i) ≤ b")
fix i assume True: "inverse (Suc i) ≤ b"
let ?a = "inverse (Suc i)"
from ‹a ≤ b› have A: "?A2 i ∩ {a..b} = {max ?a a..b}" (is "?F = ?G") by auto
hence "emeasure ?M1 ?F = emeasure ?M1 ?G" by simp
also have "strict_mono_on (λx. -inverse x) {max ?a a..b}"
by (rule strict_mono_onI) (auto dest!: inv_le simp: not_le simp del: of_nat_Suc)
with ‹a ≤ b› True dens
have "emeasure ?M1 ?G = emeasure ?M2 ?G"
by (intro emeasure_density_distr_interval)
(auto simp: Mf not_less dest: has_subprob_densityD inv_le
intro!: derivative_eq_intros continuous_on_mult continuous_on_inverse continuous_on_id)
also note A[symmetric]
finally show "emeasure ?M1 (?A2 i ∩ {a..b}) = emeasure ?M2 (?A2 i ∩ {a..b})" .
qed simp
hence "(SUP i. emeasure ?M1 (?A2 i ∩ {a..b})) = (SUP i. emeasure ?M2 (?A2 i ∩ {a..b}))" by simp
also have "... = emeasure ?M2 (⋃i. ?A2 i ∩ {a..b})"
by (rule SUP_emeasure_incseq)
(auto simp: incseq_def max_def not_le dest: order.strict_trans1)
also have "emeasure ?M2 ?D + emeasure ?M2 ?E + emeasure ?M2 ?C = emeasure ?M2 {a..b}"
apply (subst (4) decomp)
apply (subst plus_emeasure, simp, simp)
apply (auto dest!: inv_le simp: not_le le_minus_iff[of _ "inverse x" for x] simp del: of_nat_Suc)
apply (subst plus_emeasure)
apply (auto dest!: inv_le simp: not_le le_minus_iff[of _ "inverse x" for x])
done
finally show "emeasure ?M1 {a..b} = emeasure ?M2 {a..b}" .
qed simp

lemma subprob_density_distr_real_inverse:
assumes dens: "has_subprob_density M lborel f"
shows "has_subprob_density (distr M borel inverse) lborel (λx. f (inverse x) * ennreal (inverse (x * x)))"
proof (unfold has_subprob_density_def, intro conjI)
let ?g' = "(λx. f (-inverse x) * ennreal (inverse (x * x)))"
have prob: "has_subprob_density (distr M borel (λx. -inverse x)) lborel ?g'"
by (rule subprob_density_distr_real_inverse_aux[OF assms])
from assms have sets_M: "sets M = sets borel" by (auto dest: has_subprob_densityD)
have [simp]: "measurable M = measurable borel"
by (intro ext, subst measurable_cong_sets[OF sets_M refl]) auto
from prob have dens: "has_density (distr M lborel (λx. -inverse x)) lborel
(λx. f (-inverse x) * ennreal (inverse (x * x)))"
unfolding has_subprob_density_def by (simp cong: distr_cong)
from distr_uminus_real[OF this]
show "has_density (distr M borel inverse) lborel
(λx. f (inverse x) * ennreal (inverse (x * x)))"
by (simp add: distr_distr o_def cong: distr_cong)
show "subprob_space (distr M borel inverse)"
by (intro subprob_space.subprob_space_distr has_subprob_densityD[OF assms]) simp_all
qed

lemma distr_convolution_real:
assumes "has_density M lborel (f :: (real × real) ⇒ ennreal)"
shows "has_density (distr M borel (case_prod (+))) lborel (λz. ∫⇧+x. f (x, z - x) ∂lborel)"
(is "has_density ?M' _ ?f'")
proof
from has_densityD[OF assms] have Mf[measurable]: "f ∈ borel_measurable borel" by simp
show Mf': "(λz. ∫⇧+ x. f (x, z - x) ∂lborel) ∈ borel_measurable lborel" by measurable

from assms have sets_M: "sets M = sets borel" by (auto dest: has_densityD)
hence [simp]: "space M = UNIV" by (subst sets_eq_imp_space_eq[OF sets_M]) simp
from sets_M have [simp]: "measurable M = measurable borel"
by (intro ext measurable_cong_sets) simp_all
have M_add: "case_prod (+) ∈ borel_measurable (borel :: (real × real) measure)"

show "distr M borel (case_prod (+)) = density lborel ?f'"
proof (rule measure_eqI)
fix X :: "real set" assume X[measurable]: "X ∈ sets (distr M borel (case_prod (+)))"
hence "emeasure (distr M borel (case_prod (+))) X = emeasure M ((λ(x, y). x + y) - X)"
also from X have "... = ∫⇧+z. f z * indicator ((λ(x, y). x + y) - X) z ∂(lborel ⨂⇩M lborel)"
by (simp add: emeasure_density has_densityD[OF assms]
also have "... = ∫⇧+x. ∫⇧+y. f (x, y) * indicator ((λ(x, y). x + y) - X) (x,y) ∂lborel ∂lborel"
apply (rule lborel.nn_integral_fst[symmetric])
apply measurable
done
also have "... = ∫⇧+x. ∫⇧+y. f (x, y) * indicator ((λ(x, y). x + y) - X) (x,y)
∂distr lborel borel ((+) (-x)) ∂lborel"
by (rule nn_integral_cong, subst lborel_distr_plus) simp
also have "... = ∫⇧+x. ∫⇧+z. f (x, z-x) * indicator ((λ(x, y). x + y) - X) (x, z-x)
∂lborel ∂lborel"
apply (rule nn_integral_cong)
apply (subst nn_integral_distr)
apply simp_all
apply measurable
apply (subst space_count_space)
apply auto
done
also have "... = ∫⇧+x. ∫⇧+z. f (x, z-x) * indicator X z ∂lborel ∂lborel"
by (intro nn_integral_cong) (simp split: split_indicator)
also have "... = ∫⇧+z. ∫⇧+x. f (x, z-x) * indicator X z ∂lborel ∂lborel" using X
by (subst lborel_pair.Fubini')
also have "... = ∫⇧+z. (∫⇧+x. f (x, z-x) ∂lborel) * indicator X z ∂lborel"
by (rule nn_integral_cong) (simp split: split_indicator)
also have "... = emeasure (density lborel ?f') X" using X
finally show "emeasure (distr M borel (case_prod (+))) X = emeasure (density lborel ?f') X" .
qed (insert assms, auto dest: has_densityD)
qed simp_all

lemma distr_convolution_ring_count_space:
assumes C: "countable (UNIV :: 'a set)"
assumes "has_density M (count_space UNIV) (f :: (('a :: ring) × 'a) ⇒ ennreal)"
shows "has_density (distr M (count_space UNIV) (case_prod (+))) (count_space UNIV)
(λz. ∫⇧+x. f (x, z - x) ∂count_space UNIV)"
(is "has_density ?M' _ ?f'")
proof
let ?CS = "count_space UNIV :: 'a measure" and ?CSP = "count_space UNIV :: ('a × 'a) measure"
show Mf': "(λz. ∫⇧+ x. f (x, z - x) ∂count_space UNIV) ∈ borel_measurable ?CS" by simp

from assms have sets_M: "sets M = UNIV" and [simp]: "space M = UNIV"
by (auto dest: has_densityD)
from assms have [simp]: "measurable M = measurable (count_space UNIV)"
by (intro ext measurable_cong_sets) (simp_all add: sets_M)

interpret sigma_finite_measure ?CS by (rule sigma_finite_measure_count_space_countable[OF C])
show "distr M ?CS (case_prod (+)) = density ?CS ?f'"
proof (rule measure_eqI)
fix X :: "'a set" assume X: "X ∈ sets (distr M ?CS (case_prod (+)))"
hence "emeasure (distr M ?CS (case_prod (+))) X = emeasure M ((λ(x, y). x + y) - X)"
also from X have "... = ∫⇧+z. f z * indicator ((λ(x, y). x + y) - X) z ∂(?CS ⨂⇩M ?CS)"
by (simp add: emeasure_density has_densityD[OF assms(2)]
sets_M pair_measure_countable C)
also have "... = ∫⇧+x. ∫⇧+y. f (x, y) * indicator ((λ(x, y). x + y) - X) (x,y) ∂?CS ∂?CS"
by (rule nn_integral_fst[symmetric]) (simp add: pair_measure_countable C)
also have "... = ∫⇧+x. ∫⇧+y. f (x, y) * indicator ((λ(x, y). x + y) - X) (x,y)
∂distr ?CS ?CS ((+) (-x)) ∂?CS"
by (rule nn_integral_cong, subst count_space_plus) simp
also have "... = ∫⇧+x. ∫⇧+z. f (x, z-x) * indicator ((λ(x, y). x + y) - X) (x, z-x) ∂?CS ∂?CS"
by (rule nn_integral_cong) (simp_all add: nn_integral_distr)
also have "... = ∫⇧+x. ∫⇧+z. f (x, z-x) * indicator X z ∂?CS ∂?CS"
by (intro nn_integral_cong) (simp split: split_indicator)
also have "... = ∫⇧+z. ∫⇧+x. f (x, z-x) * indicator X z ∂?CS ∂?CS" using X
by (subst pair_sigma_finite.Fubini')
C pair_measure_countable)
also have "... = ∫⇧+z. (∫⇧+x. f (x, z-x) ∂?CS) * indicator X z ∂?CS"
by (rule nn_integral_cong) (simp split: split_indicator)
also have "... = emeasure (density ?CS ?f') X" using X by (simp add: emeasure_density)
finally show "emeasure (distr M ?CS (case_prod (+))) X = emeasure (density ?CS ?f') X" .
qed (insert assms, auto dest: has_densityD)
qed simp_all

end


# Theory PDF_Values

(*
Theory: PDF_Values.thy
Author: Manuel Eberl

Defines the values and types in the PDF language and the corresponding stock measure spaces.
Additionally, some functions and lemmas for lifting functions on the HOL types (int, real, …)
to PDF values are provided.
*)

section ‹Source Language Values›

theory PDF_Values
imports Density_Predicates
begin

subsection ‹Values and stock measures›

datatype pdf_type =  UNIT | BOOL | INTEG | REAL | PRODUCT pdf_type pdf_type

datatype val = UnitVal
| BoolVal (extract_bool: bool)
| IntVal (extract_int: int)
| RealVal (extract_real: real)
| PairVal (extract_fst: val) (extract_snd: val)  ("<|_, _|>"  [0, 61] 1000)
where
"extract_bool UnitVal = False"
| "extract_bool (IntVal i) = False"
| "extract_bool (RealVal r) = False"
| "extract_bool (PairVal x y) = False"
| "extract_int UnitVal = 0"
| "extract_int (BoolVal b) = 0"
| "extract_int (RealVal r) = 0"
| "extract_int (PairVal x y) = 0"
| "extract_real UnitVal = 0"
| "extract_real (BoolVal b) = 0"
| "extract_real (IntVal i) = 0"
| "extract_real (PairVal x y) = 0"

primrec extract_pair' where
"extract_pair' f s <| x, y |> = (f x, s y)"

definition map_int_pair where
"map_int_pair f g x = (case x of <| IntVal a, IntVal b |> ⇒ f a b | _ ⇒ g x)"

definition map_real_pair where
"map_real_pair f g x = (case x of <| RealVal a, RealVal b |> ⇒ f a b | _ ⇒ g x)"

abbreviation "TRUE ≡ BoolVal True"
abbreviation "FALSE ≡ BoolVal False"

type_synonym vname = "nat"
type_synonym state = "vname ⇒ val"

lemma map_int_pair[simp]: "map_int_pair f g <| IntVal i, IntVal j |> = f i j"

lemma map_int_pair_REAL[simp]: "map_int_pair f g <| RealVal i, RealVal j |> = g <| RealVal i, RealVal j |>"

lemma map_real_pair[simp]: "map_real_pair f g <| RealVal i, RealVal j |> = f i j"

abbreviation "extract_pair ≡ extract_pair' id id"
abbreviation "extract_real_pair ≡ extract_pair' extract_real extract_real"
abbreviation "extract_int_pair ≡ extract_pair' extract_int extract_int"

definition "RealPairVal ≡ λ(x,y). <|RealVal x, RealVal y|>"

definition "IntPairVal ≡ λ(x,y). <|IntVal x, IntVal y|>"

lemma inj_RealPairVal: "inj RealPairVal" by (auto simp: RealPairVal_def intro!: injI)
lemma inj_IntPairVal: "inj IntPairVal" by (auto simp: IntPairVal_def intro!: injI)

fun val_type :: "val ⇒ pdf_type" where
"val_type (BoolVal b) = BOOL"
| "val_type (IntVal i) = INTEG"
| "val_type UnitVal = UNIT"
| "val_type (RealVal r) = REAL"
| "val_type (<|v1 , v2|>) = (PRODUCT (val_type v1) (val_type v2))"

lemma val_type_eq_REAL: "val_type x = REAL ⟷ x ∈ RealValUNIV"
by (cases x) auto

lemma val_type_eq_INTEG: "val_type x = INTEG ⟷ x ∈ IntValUNIV"
by (cases x) auto

definition "type_universe t = {v. val_type v = t}"

lemma type_universe_nonempty[simp]: "type_universe t ≠ {}"
by (induction t) (auto intro: val_type.simps simp: type_universe_def)

lemma val_in_type_universe[simp]:
"v ∈ type_universe (val_type v)"

lemma BoolVal_in_type_universe[simp]: "BoolVal v ∈ type_universe BOOL"

lemma IntVal_in_type_universe[simp]: "IntVal v ∈ type_universe INTEG"

lemma type_universe_type[simp]:
"w ∈ type_universe t ⟷ val_type w = t"

lemma type_universe_REAL: "type_universe REAL = RealVal  UNIV"
apply (auto simp add: set_eq_iff image_iff)
apply (case_tac x)
apply auto
done

lemma type_universe_eq_imp_type_eq:
assumes "type_universe t1 = type_universe t2"
shows "t1 = t2"
proof-
from type_universe_nonempty obtain v where A: "v ∈ type_universe t1" by blast
hence "t1 = val_type v" by simp
also from A and assms have "v ∈ type_universe t2" by simp
hence "val_type v = t2" by simp
finally show ?thesis .
qed

lemma type_universe_eq_iff[simp]: "type_universe t1 = type_universe t2 ⟷ t1 = t2"
by (blast intro: type_universe_eq_imp_type_eq)

primrec stock_measure :: "pdf_type ⇒ val measure" where
"stock_measure UNIT = count_space {UnitVal}"
| "stock_measure INTEG = count_space (range IntVal)"
| "stock_measure BOOL = count_space (range BoolVal)"
| "stock_measure REAL = embed_measure lborel RealVal"
| "stock_measure (PRODUCT t1 t2) =
embed_measure (stock_measure t1 ⨂⇩M stock_measure t2) (λ(a, b). <|a, b|>)"

declare [[coercion stock_measure]]

lemma sigma_finite_stock_measure[simp]: "sigma_finite_measure (stock_measure t)"
by (induction t)
(auto intro!: sigma_finite_measure_count_space_countable sigma_finite_pair_measure
sigma_finite_embed_measure injI sigma_finite_lborel)

lemma val_case_stock_measurable:
assumes "t = UNIT ⟹ c ∈ space M"
assumes "⋀b. t = BOOL ⟹ g b ∈ space M"
assumes "⋀i. t = INTEG ⟹ h i ∈ space M"
assumes "t = REAL ⟹ j ∈ measurable borel M"
assumes *: "⋀t1 t2. t = PRODUCT t1 t2 ⟹ case_prod k ∈ measurable (stock_measure t1 ⨂⇩M stock_measure t2) M"
shows "(λx. case x of UnitVal ⇒ c | BoolVal b ⇒ g b | IntVal i ⇒ h i | RealVal r ⇒ j r
| PairVal y z ⇒ k y z) ∈ measurable t M"
proof (cases t)
case (PRODUCT t1 t2) with *[of t1 t2] show ?thesis
by (auto intro!: measurable_embed_measure1 simp: split_beta')
qed (auto intro!: measurable_embed_measure1 assms)

lemma space_stock_measure[simp]: "space (stock_measure t) = type_universe t"
by (induction t)
(auto simp add: type_universe_def space_pair_measure space_embed_measure
simp del: type_universe_type elim: val_type.elims)

lemma type_universe_stock_measure[measurable]: "type_universe t ∈ sets (stock_measure t)"
using sets.top[of "stock_measure t"] by simp

lemma inj_RealVal[simp]: "inj RealVal" by (auto intro!: inj_onI)
lemma inj_IntVal[simp]: "inj IntVal" by (auto intro!: inj_onI)
lemma inj_BoolVal[simp]: "inj BoolVal" by (auto intro!: inj_onI)
lemma inj_PairVal[simp]: "inj (λ(x, y). <| x ,  y |>)" by (auto intro: injI)

lemma measurable_PairVal[measurable]:
fixes t1 t2 :: pdf_type
shows "case_prod PairVal ∈ measurable (t1 ⨂⇩M t2) (PRODUCT t1 t2)"
using measurable_embed_measure2[measurable] by simp

lemma measurable_RealVal[measurable]: "RealVal ∈ measurable borel REAL"
using measurable_embed_measure2[measurable] by simp

lemma nn_integral_BoolVal:
assumes "⋀x. f (BoolVal x) ≥ 0"
shows "(∫⇧+x. f x ∂BOOL) = f (BoolVal True) + f (BoolVal False)"
proof-
have A: "range BoolVal = {BoolVal True, BoolVal False}" by auto
from assms show ?thesis
by (subst stock_measure.simps, subst A, subst nn_integral_count_space_finite)
qed

lemma nn_integral_RealVal:
"f ∈ borel_measurable REAL ⟹ (∫⇧+x. f x ∂REAL) = (∫⇧+x. f (RealVal x) ∂lborel)"
unfolding stock_measure.simps using measurable_embed_measure2[measurable]
by (subst embed_measure_eq_distr, simp_all add: nn_integral_distr)

lemma nn_integral_IntVal: "(∫⇧+x. f x ∂INTEG) = (∫⇧+x. f (IntVal x) ∂count_space UNIV)"
using measurable_embed_measure1[measurable (raw)]
unfolding stock_measure.simps embed_measure_count_space[OF inj_IntVal, symmetric]
by (subst embed_measure_eq_distr[OF inj_IntVal], simp add: nn_integral_distr space_embed_measure)

lemma nn_integral_PairVal:
"f ∈ borel_measurable (PRODUCT t1 t2) ⟹
(∫⇧+x. f x ∂PRODUCT t1 t2) = (∫⇧+x. f (PairVal (fst x) (snd x)) ∂(t1 ⨂⇩M t2))"
unfolding stock_measure.simps
by (subst nn_integral_embed_measure) (simp_all add: split_beta' inj_on_def)

lemma BOOL_E: "⟦val_type v = BOOL; ⋀b. v = BoolVal b ⟹ P⟧ ⟹ P"
by (cases v) auto

lemma PROD_E: "⟦val_type v = PRODUCT t1 t2 ;
⋀a b. val_type a = t1 ⟹ val_type b = t2 ⟹ v = <| a, b |> ⟹ P⟧ ⟹ P"
by (cases v) auto

lemma REAL_E: "⟦val_type v = REAL; ⋀b. v = RealVal b ⟹ P⟧ ⟹ P"
by (cases v) auto

lemma INTEG_E: "⟦val_type v = INTEG; ⋀i. v = IntVal i ⟹ P⟧ ⟹ P"
by (cases v) auto

lemma measurable_extract_pair'[measurable (raw)]:
fixes t1 t2 :: pdf_type
assumes [measurable]: "f ∈ measurable t1 M"
assumes [measurable]: "g ∈ measurable t2 N"
assumes h: "h ∈ measurable K (PRODUCT t1 t2)"
shows "(λx. extract_pair' f g (h x)) ∈ measurable K (M ⨂⇩M N)"
by (rule measurable_compose[OF h[unfolded stock_measure.simps] measurable_embed_measure1])

lemma measurable_extract_pair[measurable]: "extract_pair ∈ measurable (PRODUCT t1 t2) (t1 ⨂⇩M t2)"
by measurable

lemma measurable_extract_real[measurable]: "extract_real ∈ measurable REAL borel"
apply simp
apply measurable
apply (rule measurable_embed_measure1)
apply simp
done

lemma measurable_extract_int[measurable]: "extract_int ∈ measurable INTEG (count_space UNIV)"
by simp measurable

lemma measurable_extract_int_pair[measurable]:
"extract_int_pair ∈ measurable (PRODUCT INTEG INTEG) (count_space UNIV ⨂⇩M count_space UNIV)"
by measurable

lemma measurable_extract_real_pair[measurable]:
"extract_real_pair ∈ measurable (PRODUCT REAL REAL) (borel ⨂⇩M borel)"
by measurable

lemma measurable_extract_real_pair'[measurable]:
"extract_real_pair ∈ measurable (PRODUCT REAL REAL) borel"
by (subst borel_prod[symmetric]) measurable

lemma measurable_extract_bool[measurable]: "extract_bool ∈ measurable BOOL (count_space UNIV)"
by simp

lemma map_int_pair_measurable[measurable]:
assumes f: "case_prod f ∈ measurable (count_space UNIV ⨂⇩M count_space UNIV) M"
shows "map_int_pair f g ∈ measurable (PRODUCT INTEG INTEG) M"
proof (subst measurable_cong)
fix w assume "w ∈ space (PRODUCT INTEG INTEG)"
then show "map_int_pair f g w = (case_prod f o extract_int_pair) w"
by (auto simp: space_embed_measure space_pair_measure)
next
show "(λ(x, y). f x y) ∘ extract_int_pair ∈ measurable (stock_measure (PRODUCT INTEG INTEG)) M"
using measurable_extract_int_pair f by (rule measurable)
qed

lemma map_int_pair_measurable_REAL[measurable]:
assumes "g ∈ measurable (PRODUCT REAL REAL) M"
shows "map_int_pair f g ∈ measurable (PRODUCT REAL REAL) M"
proof (subst measurable_cong)
fix w assume "w ∈ space (PRODUCT REAL REAL)"
then show "map_int_pair f g w = g w"
by (auto simp: space_embed_measure space_pair_measure map_int_pair_def)
qed fact

lemma map_real_pair_measurable[measurable]:
assumes f: "case_prod f ∈ measurable (borel ⨂⇩M borel) M"
shows "map_real_pair f g ∈ measurable (PRODUCT REAL REAL) M"
proof (subst measurable_cong)
fix w assume "w ∈ space (PRODUCT REAL REAL)"
then show "map_real_pair f g w = (case_prod f o extract_real_pair) w"
by (auto simp: space_embed_measure space_pair_measure)
next
show "(λ(x, y). f x y) ∘ extract_real_pair ∈ measurable (stock_measure (PRODUCT REAL REAL)) M"
using measurable_extract_real_pair f by (rule measurable)
qed

lemma count_space_IntVal_prod[simp]: "INTEG ⨂⇩M INTEG = count_space (range IntVal × range IntVal)"
by (auto intro!: pair_measure_countable)

lemma count_space_BoolVal_prod[simp]: "BOOL ⨂⇩M BOOL = count_space (range BoolVal × range BoolVal)"
by (auto intro!: pair_measure_countable)

lemma measurable_stock_measure_val_type:
assumes "f ∈ measurable M (stock_measure t)" "x ∈ space M"
shows "val_type (f x) = t"
using assms by (auto dest!: measurable_space)

lemma singleton_in_stock_measure[simp]: "val_type v = t ⟹ {v} ∈ sets t"
proof (induction v arbitrary: t)
case (PairVal v1 v2)
have A: "{<|v1, v2|>} = (λ(v1,v2). <|v1,v2|>)  ({v1}×{v2})" by simp
from pair_measureI[OF PairVal.IH, OF refl refl] PairVal.prems[symmetric] show ?case
by (simp only: val_type.simps stock_measure.simps A in_sets_embed_measure)
qed (auto simp: sets_embed_measure)

lemma emeasure_stock_measure_singleton_finite[simp]:
"emeasure (stock_measure (val_type v)) {v} ≠ ∞"
proof (induction v)
case (RealVal r)
have A: "{RealVal r} = RealVal  {r}" by simp
have "RealVal  {r} ∈ sets (embed_measure lborel RealVal)"
by (rule in_sets_embed_measure) simp
thus ?case by (simp only: A val_type.simps stock_measure.simps emeasure_embed_measure
inj_RealVal inj_vimage_image_eq) simp
next
case (PairVal v1 v2)
let ?M = "λx. stock_measure (val_type x)"
interpret sigma_finite_measure "stock_measure (val_type v2)"
by (rule sigma_finite_stock_measure)
have A: "{<|v1, v2|>} = (λ(v1,v2). <|v1,v2|>)  ({v1}×{v2})" by simp
have B: "{v1}×{v2} ∈ ?M v1 ⨂⇩M ?M v2"
by (intro pair_measureI singleton_in_stock_measure) simp_all
hence "emeasure (?M (<|v1,v2|>)) {<|v1,v2|>} = emeasure (?M v1) {v1} * emeasure (?M v2) {v2}"
by (simp only: stock_measure.simps val_type.simps A emeasure_embed_measure_image inj_PairVal
inj_vimage_image_eq emeasure_pair_measure_Times singleton_in_stock_measure B)
with PairVal.IH show ?case by (simp add: ennreal_mult_eq_top_iff)
qed simp_all

subsection ‹Measures on states›

definition state_measure :: "vname set ⇒ (vname ⇒ pdf_type) ⇒ state measure" where
"state_measure V Γ ≡ Π⇩M y∈V. Γ y"

lemma state_measure_nonempty[simp]: "space (state_measure V Γ) ≠ {}"
by (simp add: state_measure_def space_PiM PiE_eq_empty_iff)

lemma space_state_measure: "space (state_measure V Γ) = (Π⇩E y∈V. type_universe (Γ y))"
by (simp add: state_measure_def space_PiM PiE_eq_empty_iff)

lemma state_measure_var_type:
"σ ∈ space (state_measure V Γ) ⟹ x ∈ V ⟹ val_type (σ x) = Γ x"
by (auto simp: state_measure_def space_PiM dest!: PiE_mem)

lemma merge_in_state_measure:
"x ∈ space (state_measure A Γ) ⟹ y ∈ space (state_measure B Γ) ⟹
merge A B (x, y) ∈ space (state_measure (A∪B) Γ)" unfolding state_measure_def
by (rule measurable_space, rule measurable_merge) (simp add: space_pair_measure)

lemma measurable_merge_stock[measurable (raw)]:
"f ∈ N →⇩M state_measure V Γ ⟹ g ∈ N →⇩M state_measure V' Γ ⟹
(λx. merge V V' (f x, g x)) ∈ N →⇩M state_measure (V ∪ V') Γ"
by (auto simp: state_measure_def)

lemma comp_in_state_measure:
assumes "σ ∈ space (state_measure V Γ)"
shows "σ ∘ f ∈ space (state_measure (f - V) (Γ ∘ f))"
using assms by (auto simp: state_measure_def space_PiM)

lemma sigma_finite_state_measure[intro]:
"finite V ⟹ sigma_finite_measure (state_measure V Γ)" unfolding state_measure_def
by (auto intro!: product_sigma_finite.sigma_finite simp: product_sigma_finite_def)

subsection ‹Equalities of measure embeddings›

lemma embed_measure_RealPairVal:
"stock_measure (PRODUCT REAL REAL) = embed_measure lborel RealPairVal"
proof-
have [simp]: "(λ(x, y). <| x ,  y |>) ∘ (λ(x, y). (RealVal x, RealVal y)) = RealPairVal"
unfolding RealPairVal_def by auto
have "stock_measure (PRODUCT REAL REAL) =
embed_measure (embed_measure lborel (λ(x, y). (RealVal x, RealVal y))) (case_prod PairVal)"
by (auto simp: embed_measure_prod sigma_finite_lborel lborel_prod)
also have "... = embed_measure lborel RealPairVal"
by (subst embed_measure_comp) (auto intro!: injI)
finally show ?thesis .
qed

lemma embed_measure_IntPairVal:
"stock_measure (PRODUCT INTEG INTEG) = count_space (range IntPairVal)"
proof-
have [simp]: "(λ(x, y). <| x ,  y |>)  (range IntVal × range IntVal) = range IntPairVal"
by (auto simp: IntPairVal_def)
show ?thesis
using count_space_IntVal_prod by (auto simp: embed_measure_prod embed_measure_count_space)
qed

definition "return_val x = return (stock_measure (val_type x)) x"

lemma sets_return_val[measurable_cong]: "sets (return_val x) = sets (stock_measure (val_type x))"

lemma measurable_return_val[simp]:
"return_val ∈ measurable (stock_measure t) (subprob_algebra (stock_measure t))"
unfolding return_val_def[abs_def]
apply (subst measurable_cong)
apply (subst type_universe_type[THEN iffD1])
apply simp
apply (rule refl)
apply (rule return_measurable)
done

lemma bind_return_val:
assumes "space M ≠ {}" "f ∈ measurable M (stock_measure t')"
shows "M ⤜ (λx. return_val (f x)) = distr M (stock_measure t') f"
using assms
by (subst bind_return_distr[symmetric])
(auto simp: return_val_def intro!: bind_cong dest: measurable_stock_measure_val_type)

lemma bind_return_val':
assumes "val_type x = t" "f ∈ measurable (stock_measure t) (stock_measure t')"
shows "return_val x ⤜ (λx. return_val (f x)) = return_val (f x)"
proof-
have "return_val x ⤜ (λx. return_val (f x)) = return (stock_measure t') (f x)"
apply (subst bind_return_val, unfold return_val_def, simp)
apply (insert assms, simp cong: measurable_cong_sets) []
apply (subst distr_return, simp_all add: assms type_universe_def
del: type_universe_type)
done
also from assms(2) have "f x ∈ space (stock_measure t')"
by (rule measurable_space)
(simp add: assms(1) type_universe_def del: type_universe_type)
hence "return (stock_measure t') (f x) = return_val (f x)"
finally show ?thesis .
qed

lemma bind_return_val'':
assumes "f ∈ measurable (stock_measure (val_type x)) (subprob_algebra M)"
shows "return_val x ⤜ f = f x"
unfolding return_val_def by (subst bind_return[OF assms]) simp_all

lemma bind_assoc_return_val:
assumes sets_M: "sets M = sets (stock_measure t)"
assumes Mf: "f ∈ measurable (stock_measure t) (stock_measure t')"
assumes Mg: "g ∈ measurable (stock_measure t') (stock_measure t'')"
shows "(M ⤜ (λx. return_val (f x))) ⤜ (λx. return_val (g x)) =
M ⤜ (λx. return_val (g (f x)))"
proof-
have "(M ⤜ (λx. return_val (f x))) ⤜ (λx. return_val (g x)) =
M ⤜ (λx. return_val (f x) ⤜ (λx. return_val (g x)))"
apply (subst bind_assoc)
apply (rule measurable_compose[OF _ measurable_return_val])
apply (subst measurable_cong_sets[OF sets_M refl], rule Mf)
apply (rule measurable_compose[OF Mg measurable_return_val], rule refl)
done
also have "... = M ⤜ (λx. return_val (g (f x)))"
apply (intro bind_cong refl)
apply (subst (asm) sets_eq_imp_space_eq[OF sets_M])
apply (drule measurable_space[OF Mf])
apply (subst bind_return_val'[where t = t' and t' = t''])
done
finally show ?thesis .
qed

lemma bind_return_val_distr:
assumes sets_M: "sets M = sets (stock_measure t)"
assumes Mf: "f ∈ measurable (stock_measure t) (stock_measure t')"
shows "M ⤜ return_val ∘ f = distr M (stock_measure t') f"
proof-
have "M ⤜ return_val ∘ f = M ⤜ return (stock_measure t') ∘ f"
apply (intro bind_cong refl)
apply (subst (asm) sets_eq_imp_space_eq[OF sets_M])
apply (drule measurable_space[OF Mf])
done
also have "... = distr M (stock_measure t') f"
apply (rule bind_return_distr)
apply (subst measurable_cong_sets[OF sets_M refl], rule Mf)
done
finally show ?thesis .
qed

subsection ‹Lifting of functions›

definition lift_RealVal where
"lift_RealVal f ≡ λ RealVal v ⇒ RealVal (f v) | _ ⇒ RealVal (f 0)"
definition lift_IntVal where
"lift_IntVal f ≡ λ IntVal v ⇒ IntVal (f v) | _ ⇒ IntVal (f 0)"
definition lift_RealIntVal where
"lift_RealIntVal f g ≡ λ IntVal v ⇒ IntVal (f v) | RealVal v ⇒ RealVal (g v)"

definition lift_RealIntVal2 where
"lift_RealIntVal2 f g ≡
map_int_pair (λa b. IntVal (f a b))
(map_real_pair (λa b. RealVal (g a b))
id)"

definition  lift_Comp where
"lift_Comp f g ≡ map_int_pair (λa b. BoolVal (f a b))
(map_real_pair (λa b. BoolVal (g a b))
(λ_. FALSE))"

lemma lift_RealVal_eq: "lift_RealVal f (RealVal x) = RealVal (f x)"

lemma lift_RealIntVal_Real:
"x ∈ space (stock_measure REAL) ⟹ lift_RealIntVal f g x = lift_RealVal g x"
by (auto simp: space_embed_measure lift_RealIntVal_def lift_RealVal_def)

lemma lift_RealIntVal_Int:
"x ∈ space (stock_measure INTEG) ⟹ lift_RealIntVal f g x = lift_IntVal f x"
by (auto simp: space_embed_measure lift_RealIntVal_def lift_IntVal_def)

declare stock_measure.simps[simp del]

lemma measurable_lift_RealVal[measurable]:
assumes [measurable]: "f ∈ borel_measurable borel"
shows "lift_RealVal f ∈ measurable REAL REAL"
unfolding lift_RealVal_def
by (auto intro!: val_case_stock_measurable)

lemma measurable_lift_IntVal[simp]: "lift_IntVal f ∈ range IntVal → range IntVal"
by (auto simp: lift_IntVal_def)

lemma measurable_lift_IntVal'[measurable]: "lift_IntVal f ∈ measurable INTEG INTEG"
unfolding lift_IntVal_def
by (auto intro!: val_case_stock_measurable)

lemma split_apply: "(case x of (a, b) ⇒ f a b) y = (case x of (a, b) ⇒ f a b y)"
by (cases x) simp

lemma measurable_lift_Comp_RealVal[measurable]:
assumes [measurable]: "Measurable.pred (borel ⨂⇩M borel) (case_prod g)"
shows "lift_Comp f g ∈ measurable (PRODUCT REAL REAL) BOOL"
unfolding lift_Comp_def by measurable

lemma measurable_lift_Comp_IntVal[simp]:
"lift_Comp f g ∈ measurable (PRODUCT INTEG INTEG) BOOL"
unfolding lift_Comp_def
by (auto intro!: val_case_stock_measurable)

lemma measurable_lift_RealIntVal_IntVal[simp]: "lift_RealIntVal f g ∈ range IntVal → range IntVal"
by (auto simp: embed_measure_count_space lift_RealIntVal_def)

lemma measurable_lift_RealIntVal_IntVal'[measurable]:
"lift_RealIntVal f g ∈ measurable INTEG INTEG"
by (auto simp: lift_RealIntVal_def intro!: val_case_stock_measurable)

lemma measurable_lift_RealIntVal_RealVal[measurable]:
assumes [measurable]: "g ∈ borel_measurable borel"
shows "lift_RealIntVal f g ∈ measurable REAL REAL"
unfolding lift_RealIntVal_def
by (auto intro!: val_case_stock_measurable)

lemma measurable_lift_RealIntVal2_IntVal[measurable]:
"lift_RealIntVal2 f g ∈ measurable (PRODUCT INTEG INTEG) INTEG"
unfolding lift_RealIntVal2_def
by (auto intro!: val_case_stock_measurable)

lemma measurable_lift_RealIntVal2_RealVal[measurable]:
assumes [measurable]: "case_prod g ∈ borel_measurable (borel ⨂⇩M borel)"
shows "lift_RealIntVal2 f g ∈ measurable (PRODUCT REAL REAL) REAL"
unfolding lift_RealIntVal2_def by measurable

lemma distr_lift_RealVal:
fixes f
assumes Mf[measurable]: "f ∈ borel_measurable borel"
assumes pdens: "has_subprob_density M (stock_measure REAL) δ"
assumes dens': "⋀M δ. has_subprob_density M lborel δ ⟹ has_density (distr M borel f) lborel (g δ)"
defines "N ≡ distr M (stock_measure REAL) (lift_RealVal f)"
shows "has_density N (stock_measure REAL) (g (λx. δ (RealVal x)) ∘ extract_real)"
proof (rule has_densityI)
from assms(2) have dens: "has_density M (stock_measure REAL) δ"
unfolding has_subprob_density_def by simp
from dens have sets_M[measurable_cong]: "sets M = sets REAL" by (auto dest: has_densityD)

note measurable_embed_measure1[measurable del]

have "N = distr M (stock_measure REAL) (lift_RealVal f)" by (simp add: N_def)
also have "… = distr M (stock_measure REAL) (RealVal ∘ f ∘ extract_real)"
using sets_eq_imp_space_eq[OF sets_M]
by (intro distr_cong) (auto simp: lift_RealVal_def stock_measure.simps space_embed_measure)
also have "... = distr (distr (distr M lborel extract_real) borel f) (stock_measure REAL) RealVal"
by (subst distr_distr)
(simp_all add: distr_distr[OF _ measurable_comp[OF _ Mf]] comp_assoc)
also have dens'': "has_density (distr (distr M lborel extract_real) borel f) lborel (g (δ ∘ RealVal))"
by (intro dens' has_subprob_density_embed_measure'') (insert pdens, simp_all add: extract_real_def stock_measure.simps)
hence "distr (distr M lborel extract_real) borel f = density lborel (g (δ ∘ RealVal))"
by (rule has_densityD)
also have "distr ... (stock_measure REAL) RealVal = embed_measure ... RealVal" (is "_ = ?M")
by (subst embed_measure_eq_distr[OF inj_RealVal], intro distr_cong)
also have "... = density (embed_measure lborel RealVal) (g (λx. δ (RealVal x)) ∘ extract_real)"
using dens''[unfolded o_def]
apply (subst density_embed_measure', simp, simp add: extract_real_def)
apply (erule has_densityD, simp add: o_def)
done
finally show "N = density (stock_measure REAL) (g (λx. δ (RealVal x)) ∘ extract_real)"

from dens''[unfolded o_def, THEN has_densityD(1)]  measurable_extract_real
show "g (λx. δ (RealVal x)) ∘ extract_real ∈ borel_measurable (stock_measure REAL)"
by (intro measurable_comp) auto
qed (subst space_stock_measure, simp)

lemma distr_lift_IntVal:
fixes f
assumes pdens: "has_density M (stock_measure INTEG) δ"
assumes dens': "⋀M δ. has_density M (count_space UNIV) δ ⟹
has_density (distr M (count_space UNIV) f) (count_space UNIV) (g δ)"
defines "N ≡ distr M (stock_measure INTEG) (lift_IntVal f)"
shows "has_density N (stock_measure INTEG) (g (λx. δ (IntVal x)) ∘ extract_int)"
proof (rule has_densityI)
let ?R = "count_space UNIV" and ?S = "count_space (range IntVal)"
have Mf: "f ∈ measurable ?R ?R" by simp
from assms(1) have dens: "has_density M (stock_measure INTEG) δ"
unfolding has_subprob_density_def by simp
from dens have sets_M[measurable_cong]: "sets M = sets INTEG" by (auto dest!: has_densityD(2))

have "N = distr M (stock_measure INTEG) (lift_IntVal f)" by (simp add: N_def)
also have "… = distr M (stock_measure INTEG) (IntVal ∘ f ∘ extract_int)"
using sets_eq_imp_space_eq[OF sets_M]
by (intro distr_cong) (auto simp: space_embed_measure lift_IntVal_def stock_measure.simps)
also have "… = distr (distr (distr M ?R extract_int) ?R f) (stock_measure INTEG) IntVal"
by (subst distr_distr) (simp_all add: distr_distr[OF _ measurable_comp[OF _ Mf]] comp_assoc)
also have dens'': "has_density (distr (distr M ?R extract_int) ?R f) ?R (g (δ ∘ IntVal))"
by (intro dens' has_density_embed_measure'')
(insert dens, simp_all add: extract_int_def embed_measure_count_space stock_measure.simps)
hence "distr (distr M ?R extract_int) ?R f = density ?R (g (δ ∘ IntVal))"
by (rule has_densityD)
also have "distr ... (stock_measure INTEG) IntVal = embed_measure ... IntVal" (is "_ = ?M")
by (subst embed_measure_eq_distr[OF inj_IntVal], intro distr_cong)
(auto simp: sets_embed_measure subset_image_iff stock_measure.simps)
also have "... = density (embed_measure ?R IntVal) (g (λx. δ (IntVal x)) ∘ extract_int)"
using dens''[unfolded o_def]
apply (subst density_embed_measure', simp, simp add: extract_int_def)
apply (erule has_densityD, simp add: o_def)
done
finally show "N = density (stock_measure INTEG) (g (λx. δ (IntVal x)) ∘ extract_int)"

from dens''[unfolded o_def]
show "g (λx. δ (IntVal x)) ∘ extract_int ∈ borel_measurable (stock_measure INTEG)"
qed (subst space_stock_measure, simp)

lemma distr_lift_RealPairVal:
fixes f f' g
assumes Mf[measurable]: "case_prod f ∈ borel_measurable borel"
assumes pdens: "has_subprob_density M (stock_measure (PRODUCT REAL REAL)) δ"
assumes dens': "⋀M δ. has_subprob_density M lborel δ ⟹ has_density (distr M borel (case_prod f)) lborel (g δ)"
defines "N ≡ distr M (stock_measure REAL) (lift_RealIntVal2 f' f)"
shows "has_density N (stock_measure REAL) (g (λx. δ (RealPairVal x)) ∘ extract_real)"
proof (rule has_densityI)
from assms(2) have dens: "has_density M (stock_measure (PRODUCT REAL REAL)) δ"
unfolding has_subprob_density_def by simp
have sets_M[measurable_cong]: "sets M = sets (stock_measure (PRODUCT REAL REAL))"
by (auto simp: has_subprob_densityD[OF pdens])

have "N = distr M (stock_measure REAL) (lift_RealIntVal2 f' f)" by (simp add: N_def)
also have "... = distr M (stock_measure REAL) (RealVal ∘ case_prod f ∘ extract_real_pair)"
using sets_eq_imp_space_eq[OF sets_M]
by (intro distr_cong) (auto simp: lift_RealIntVal2_def space_embed_measure space_pair_measure stock_measure.simps)
also have "... = distr (distr (distr M lborel extract_real_pair) borel (case_prod f)) REAL RealVal"
by (subst distr_distr) (simp_all add: distr_distr[OF _ measurable_comp[OF _ Mf]] comp_assoc)
also have dens'': "has_density (distr (distr M lborel extract_real_pair) borel (case_prod f)) lborel
(g (δ ∘ RealPairVal))" using inj_RealPairVal embed_measure_RealPairVal
by (intro dens' has_subprob_density_embed_measure'')
(insert pdens, simp_all add: RealPairVal_def split: prod.split)
hence "distr (distr M lborel extract_real_pair) borel (case_prod f) =
density lborel (g (δ ∘ RealPairVal))" by (rule has_densityD)
also have "distr ... (stock_measure REAL) RealVal = embed_measure ... RealVal" (is "_ = ?M")
by (subst embed_measure_eq_distr[OF inj_RealVal], intro distr_cong)
also have "... = density (embed_measure lborel RealVal) (g (λx. δ (RealPairVal x)) ∘ extract_real)"
using dens''[unfolded o_def]
by (subst density_embed_measure', simp, simp add: extract_real_def)
finally show "N = density (stock_measure REAL) (g (λx. δ (RealPairVal x)) ∘ extract_real)"

from dens''[unfolded o_def]
show "g (λx. δ (RealPairVal x)) ∘ extract_real ∈ borel_measurable (stock_measure REAL)"
by (intro measurable_comp)
(rule measurable_extract_real, subst measurable_lborel2[symmetric], erule has_densityD)
qed (subst space_stock_measure, simp)

lemma distr_lift_IntPairVal:
fixes f f'
assumes pdens: "has_density M (stock_measure (PRODUCT INTEG INTEG)) δ"
assumes dens': "⋀M δ. has_density M (count_space UNIV) δ ⟹
has_density (distr M (count_space UNIV) (case_prod f))
(count_space UNIV) (g δ)"
defines "N ≡ distr M (stock_measure INTEG) (lift_RealIntVal2 f f')"
shows "has_density N (stock_measure INTEG) (g (λx. δ (IntPairVal x)) ∘ extract_int)"
proof (rule has_densityI)
let ?R = "count_space UNIV" and ?S = "count_space (range IntVal)"
and ?T = "count_space (range IntPairVal)" and ?tp = "PRODUCT INTEG INTEG"
have Mf: "f ∈ measurable ?R ?R" by simp
have MIV: "IntVal ∈ measurable ?R ?S" by simp
from assms(1) have dens: "has_density M (stock_measure ?tp) δ"
unfolding has_subprob_density_def by simp
from dens have "M = density (stock_measure ?tp) δ" by (rule has_densityD)
hence sets_M: "sets M = sets ?T" by (subst embed_measure_IntPairVal[symmetric]) auto
hence [simp]: "space M = space ?T" by (rule sets_eq_imp_space_eq)
from sets_M have [simp]: "measurable M = measurable (count_space (range IntPairVal))"
by (intro ext measurable_cong_sets) simp_all

have "N = distr M (stock_measure INTEG) (lift_RealIntVal2 f f')" by (simp add: N_def)

also have "... = distr M (stock_measure INTEG) (IntVal ∘ case_prod f ∘ extract_int_pair)"
by (intro distr_cong) (auto simp: lift_RealIntVal2_def space_embed_measure space_pair_measure IntPairVal_def)
also have "... = distr (distr (distr M (count_space UNIV) extract_int_pair)
(count_space UNIV) (case_prod f)) (stock_measure INTEG) IntVal"
apply (subst distr_distr[of _ ?R, symmetric], simp, simp)
apply (subst distr_distr[symmetric], subst stock_measure.simps, rule MIV,
done
also have dens'': "has_density (distr (distr M (count_space UNIV) extract_int_pair) ?R (case_prod f)) ?R
(g (δ ∘ IntPairVal))" using inj_IntPairVal embed_measure_IntPairVal
by (intro dens' has_density_embed_measure'')
(insert dens, simp_all add: extract_int_def embed_measure_count_space IntPairVal_def split: prod.split)
hence "distr (distr M (count_space UNIV) extract_int_pair) ?R (case_prod f) =
density ?R (g (δ ∘ IntPairVal))" by (rule has_densityD)
also have "distr ... (stock_measure INTEG) IntVal = embed_measure ... IntVal" (is "_ = ?M")
by (subst embed_measure_eq_distr[OF inj_IntVal], intro distr_cong)
(auto simp: sets_embed_measure subset_image_iff stock_measure.simps)
also have "... = density (embed_measure ?R IntVal) (g (λx. δ (IntPairVal x)) ∘ extract_int)"
using dens''[unfolded o_def]
by (subst density_embed_measure', simp, simp add: extract_int_def)
finally show "N = density (stock_measure INTEG) (g (λx. δ (IntPairVal x)) ∘ extract_int)"

from dens''[unfolded o_def]
show "g (λx. δ (IntPairVal x)) ∘ extract_int ∈ borel_measurable (stock_measure INTEG)"
qed (subst space_stock_measure, simp)

end


# Theory PDF_Semantics

(*
Theory: PDF_Semantics.thy
Author: Manuel Eberl

Defines the expressions of the PDF language and their typing rules and semantics
as well as a number of standard semantics-related theorems such as substitution.
*)

theory PDF_Semantics
imports PDF_Values
begin

lemma measurable_subprob_algebra_density:
assumes "sigma_finite_measure N"
assumes "space N ≠ {}"
assumes [measurable]: "case_prod f ∈ borel_measurable (M ⨂⇩M N)"
assumes "⋀x. x ∈ space M ⟹ (∫⇧+y. f x y ∂N) ≤ 1"
shows "(λx. density N (f x)) ∈ measurable M (subprob_algebra N)"
proof (rule measurable_subprob_algebra)
fix x assume "x ∈ space M"
with assms show "subprob_space (density N (f x))"
by (intro subprob_spaceI) (auto simp: emeasure_density cong: nn_integral_cong')
next
interpret sigma_finite_measure N by fact
fix X assume X: "X ∈ sets N"
hence "(λx. (∫⇧+y. f x y * indicator X y ∂N)) ∈ borel_measurable M" by simp
moreover from X and assms have
"⋀x. x ∈ space M ⟹ emeasure (density N (f x)) X = (∫⇧+y. f x y * indicator X y ∂N)"
ultimately show "(λx. emeasure (density N (f x)) X) ∈ borel_measurable M"
by (simp only: cong: measurable_cong)
qed simp_all

section ‹Built-in Probability Distributions›

subsection ‹Bernoulli›

definition bernoulli_density :: "real ⇒ bool ⇒ ennreal" where
"bernoulli_density p b = (if p ∈ {0..1} then (if b then p else 1 - p) else 0)"

definition bernoulli :: "val ⇒ val measure" where
"bernoulli p = density BOOL (bernoulli_density (extract_real p) o extract_bool)"

lemma measurable_bernoulli_density[measurable]:
"case_prod bernoulli_density ∈ borel_measurable (borel ⨂⇩M count_space UNIV)"
unfolding bernoulli_density_def[abs_def] by measurable

lemma measurable_bernoulli[measurable]: "bernoulli ∈ measurable REAL (subprob_algebra BOOL)"
unfolding bernoulli_def[abs_def]
by (auto intro!: measurable_subprob_algebra_density
simp: measurable_split_conv nn_integral_BoolVal bernoulli_density_def
ennreal_plus[symmetric]
simp del: ennreal_plus)

subsection ‹Uniform›

definition uniform_real_density :: "real × real ⇒ real ⇒ ennreal" where
"uniform_real_density ≡ λ(a,b) x. ennreal (if a < b ∧ x ∈ {a..b} then inverse (b - a) else 0)"

definition uniform_int_density :: "int × int ⇒ int ⇒ ennreal" where
"uniform_int_density ≡ λ(a,b) x. (if x ∈ {a..b} then inverse (nat (b - a + 1)) else 0)"

lemma measurable_uniform_density_int[measurable]:
"(case_prod uniform_int_density)
∈ borel_measurable ((count_space UNIV ⨂⇩M count_space UNIV) ⨂⇩M count_space UNIV)"

lemma measurable_uniform_density_real[measurable]:
"(case_prod uniform_real_density) ∈ borel_measurable (borel ⨂⇩M borel)"
proof-
have "(case_prod uniform_real_density) =
(λx. uniform_real_density (fst (fst x), snd (fst x)) (snd x))"
by (rule ext) (simp split: prod.split)
also have "... ∈ borel_measurable (borel ⨂⇩M borel)"
unfolding uniform_real_density_def
by (simp only: prod.case) (simp add: borel_prod[symmetric])
finally show ?thesis .
qed

definition uniform_int :: "val ⇒ val measure" where
"uniform_int = map_int_pair (λl u. density INTEG (uniform_int_density (l,u) o extract_int)) (λ_. undefined)"

definition uniform_real :: "val ⇒ val measure" where
"uniform_real = map_real_pair (λl u. density REAL (uniform_real_density (l,u) o extract_real)) (λ_. undefined)"

lemma if_bounded: "(if a ≤ i ∧ i ≤ b then v else 0) = (v::real) * indicator {a .. b} i"
by auto

lemma measurable_uniform_int[measurable]:
"uniform_int ∈ measurable (PRODUCT INTEG INTEG) (subprob_algebra INTEG)"
unfolding uniform_int_def
proof (rule measurable measurable_subprob_algebra_density)+
fix x :: "int × int"

show "integral⇧N INTEG (uniform_int_density (fst x, snd x) ∘ extract_int) ≤ 1"
proof cases
assume "fst x ≤ snd x" then show ?thesis
by (cases x)
(simp add: uniform_int_density_def comp_def nn_integral_IntVal nn_integral_cmult
nn_integral_set_ennreal[symmetric] ennreal_of_nat_eq_real_of_nat
if_bounded[where 'a=int] ennreal_mult[symmetric]
del: ennreal_plus)
qed (simp add: uniform_int_density_def comp_def split_beta' if_bounded[where 'a=int])
qed (auto simp: comp_def)

lemma density_cong':
"(⋀x. x ∈ space M ⟹ f x = g x) ⟹ density M f = density M g"
unfolding density_def
by (auto dest: sets.sets_into_space intro!: nn_integral_cong measure_of_eq)

lemma measurable_uniform_real[measurable]:
"uniform_real ∈ measurable (PRODUCT REAL REAL) (subprob_algebra REAL)"
unfolding uniform_real_def
proof (rule measurable measurable_subprob_algebra_density)+
fix x :: "real × real"
obtain l u where [simp]: "x = (l, u)"
by (cases x) auto
show "(∫⇧+y. (uniform_real_density (fst x, snd x) o extract_real) y ∂REAL) ≤ 1"
proof cases
assume "l < u" then show ?thesis
by (simp add: nn_integral_RealVal uniform_real_density_def if_bounded nn_integral_cmult
nn_integral_set_ennreal[symmetric] ennreal_mult[symmetric])
qed (auto simp: comp_def borel_prod)

subsection ‹Gaussian›

definition gaussian_density :: "real × real ⇒ real ⇒ ennreal" where
"gaussian_density ≡
λ(m,s) x. (if s > 0 then exp (-(x - m)⇧2 / (2 * s⇧2)) / sqrt (2 * pi * s⇧2) else 0)"

lemma measurable_gaussian_density[measurable]:
"case_prod gaussian_density ∈ borel_measurable (borel ⨂⇩M borel)"
proof-
have "case_prod gaussian_density =
(λ(x,y). (if snd x > 0 then exp (-((y - fst x)^2) / (2 * snd x^2)) /
sqrt (2 * pi * snd x^2) else 0))"
unfolding gaussian_density_def by (intro ext) (simp split: prod.split)
also have "... ∈ borel_measurable (borel ⨂⇩M borel)"
finally show ?thesis .
qed

definition gaussian :: "val ⇒ val measure" where
"gaussian = map_real_pair (λm s. density REAL (gaussian_density (m,s) o extract_real)) undefined"

lemma measurable_gaussian[measurable]: "gaussian ∈ measurable (PRODUCT REAL REAL) (subprob_algebra REAL)"
unfolding gaussian_def
proof (rule measurable measurable_subprob_algebra_density)+
fix x :: "real × real"
show "integral⇧N (stock_measure REAL) (gaussian_density (fst x, snd x) ∘ extract_real) ≤ 1"
proof cases
assume "snd x > 0"
then have "integral⇧N lborel (gaussian_density x) = (∫⇧+y. normal_density (fst x) (snd x) y ∂lborel)"
by (auto simp add: gaussian_density_def normal_density_def split_beta' intro!: nn_integral_cong)
also have "… = 1"
using ‹snd x > 0›
by (subst nn_integral_eq_integral) (auto intro!: normal_density_nonneg)
finally show ?thesis
by (cases x) (simp add: nn_integral_RealVal comp_def)
next
assume "¬ snd x > 0" then show ?thesis
by (cases x)
(simp add: nn_integral_RealVal comp_def gaussian_density_def zero_ennreal_def[symmetric])
qed
qed (auto simp: comp_def borel_prod)

subsection ‹Poisson›

definition poisson_density' :: "real ⇒ int ⇒ ennreal" where
"poisson_density' rate k = pmf (poisson_pmf rate) (nat k) * indicator ({0 <..} × {0..}) (rate, k)"

lemma measurable_poisson_density'[measurable]:
"case_prod poisson_density' ∈ borel_measurable (borel ⨂⇩M count_space UNIV)"
proof -
have "case_prod poisson_density' =
(λ(rate, k). rate ^ nat k / real_of_nat (fact (nat k)) * exp (-rate) * indicator ({0 <..} × {0..}) (rate, k))"
by (auto split: split_indicator simp: fun_eq_iff poisson_density'_def)
then show ?thesis
by simp
qed

definition poisson :: "val ⇒ val measure" where
"poisson rate = density INTEG (poisson_density' (extract_real rate) o extract_int)"

lemma measurable_poisson[measurable]: "poisson ∈ measurable REAL (subprob_algebra INTEG)"
unfolding poisson_def[abs_def]
proof (rule measurable measurable_subprob_algebra_density)+
fix r :: real
have [simp]: "nat  {0..} = UNIV"
by (auto simp: image_iff intro!: bexI[of _ "int x" for x])

{ assume "0 < r"
then have "(∫⇧+ x. ennreal (r ^ nat x * exp (- r) * indicator ({0<..} × {0..}) (r, x) / (fact (nat x))) ∂count_space UNIV)
= (∫⇧+ x. ennreal (pmf (poisson_pmf r) (nat x)) ∂count_space {0 ..})"
by (auto intro!: nn_integral_cong simp add: nn_integral_count_space_indicator split: split_indicator)
also have "… = 1"
using measure_pmf.emeasure_space_1[of "poisson_pmf r"]
by (subst nn_integral_pmf') (auto simp: inj_on_def)
finally have "(∫⇧+ x. ennreal (r ^ nat x * exp (- r) * indicator ({0<..} × {0..}) (r, x) / (fact (nat x))) ∂count_space UNIV) = 1"
. }
then show "integral⇧N INTEG (poisson_density' r ∘ extract_int) ≤ 1"
by (cases "0 < r")
(auto simp: nn_integral_IntVal poisson_density'_def zero_ennreal_def[symmetric])
qed (auto simp: comp_def)

section ‹Source Language Syntax and Semantics›

subsection ‹Expressions›

class expr = fixes free_vars :: "'a ⇒ vname set"

datatype pdf_dist = Bernoulli | UniformInt | UniformReal | Poisson | Gaussian

datatype pdf_operator = Fst | Snd | Add | Mult | Minus | Less | Equals | And | Not | Or | Pow |
Sqrt | Exp | Ln | Fact | Inverse | Pi | Cast pdf_type

datatype expr =
Var vname
| Val val
| LetVar expr expr ("LET _ IN _" [0, 60] 61)
| Operator pdf_operator expr (infixl "$$" 999) | Pair expr expr ("<_ , _>" [0, 60] 1000) | Random pdf_dist expr | IfThenElse expr expr expr ("IF _ THEN _ ELSE _" [0, 0, 70] 71) | Fail pdf_type type_synonym tyenv = "vname ⇒ pdf_type" instantiation expr :: expr begin primrec free_vars_expr :: "expr ⇒ vname set" where "free_vars_expr (Var x) = {x}" | "free_vars_expr (Val _) = {}" | "free_vars_expr (LetVar e1 e2) = free_vars_expr e1 ∪ Suc - free_vars_expr e2" | "free_vars_expr (Operator _ e) = free_vars_expr e" | "free_vars_expr (<e1, e2>) = free_vars_expr e1 ∪ free_vars_expr e2" | "free_vars_expr (Random _ e) = free_vars_expr e" | "free_vars_expr (IF b THEN e1 ELSE e2) = free_vars_expr b ∪ free_vars_expr e1 ∪ free_vars_expr e2" | "free_vars_expr (Fail _) = {}" instance .. end primrec free_vars_expr_code :: "expr ⇒ vname set" where "free_vars_expr_code (Var x) = {x}" | "free_vars_expr_code (Val _) = {}" | "free_vars_expr_code (LetVar e1 e2) = free_vars_expr_code e1 ∪ (λx. x - 1)  (free_vars_expr_code e2 - {0})" | "free_vars_expr_code (Operator _ e) = free_vars_expr_code e" | "free_vars_expr_code (<e1, e2>) = free_vars_expr_code e1 ∪ free_vars_expr_code e2" | "free_vars_expr_code (Random _ e) = free_vars_expr_code e" | "free_vars_expr_code (IF b THEN e1 ELSE e2) = free_vars_expr_code b ∪ free_vars_expr_code e1 ∪ free_vars_expr_code e2" | "free_vars_expr_code (Fail _) = {}" lemma free_vars_expr_code[code]: "free_vars (e::expr) = free_vars_expr_code e" proof- have "⋀A. Suc - A = (λx. x - 1)  (A - {0})" by force thus ?thesis by (induction e) simp_all qed primrec dist_param_type where "dist_param_type Bernoulli = REAL" | "dist_param_type Poisson = REAL" | "dist_param_type Gaussian = PRODUCT REAL REAL" | "dist_param_type UniformInt = PRODUCT INTEG INTEG" | "dist_param_type UniformReal = PRODUCT REAL REAL" primrec dist_result_type where "dist_result_type Bernoulli = BOOL" | "dist_result_type UniformInt = INTEG" | "dist_result_type UniformReal = REAL" | "dist_result_type Poisson = INTEG" | "dist_result_type Gaussian = REAL" primrec dist_measure :: "pdf_dist ⇒ val ⇒ val measure" where "dist_measure Bernoulli = bernoulli" | "dist_measure UniformInt = uniform_int" | "dist_measure UniformReal = uniform_real" | "dist_measure Poisson = poisson" | "dist_measure Gaussian = gaussian" lemma measurable_dist_measure[measurable]: "dist_measure d ∈ measurable (dist_param_type d) (subprob_algebra (dist_result_type d))" by (cases d) simp_all lemma sets_dist_measure[simp]: "val_type x = dist_param_type dst ⟹ sets (dist_measure dst x) = sets (stock_measure (dist_result_type dst))" by (rule sets_kernel[OF measurable_dist_measure]) simp lemma space_dist_measure[simp]: "val_type x = dist_param_type dst ⟹ space (dist_measure dst x) = type_universe (dist_result_type dst)" by (subst space_stock_measure[symmetric]) (intro sets_eq_imp_space_eq sets_dist_measure) primrec dist_dens :: "pdf_dist ⇒ val ⇒ val ⇒ ennreal" where "dist_dens Bernoulli x y = bernoulli_density (extract_real x) (extract_bool y)" | "dist_dens UniformInt x y = uniform_int_density (extract_int_pair x) (extract_int y)" | "dist_dens UniformReal x y = uniform_real_density (extract_real_pair x) (extract_real y)" | "dist_dens Gaussian x y = gaussian_density (extract_real_pair x) (extract_real y)" | "dist_dens Poisson x y = poisson_density' (extract_real x) (extract_int y)" lemma measurable_dist_dens[measurable]: assumes "f ∈ measurable M (stock_measure (dist_param_type dst))" (is "_ ∈ measurable M ?N") assumes "g ∈ measurable M (stock_measure (dist_result_type dst))" (is "_ ∈ measurable M ?R") shows "(λx. dist_dens dst (f x) (g x)) ∈ borel_measurable M" apply (rule measurable_Pair_compose_split[of "dist_dens dst", OF _ assms]) apply (subst dist_dens_def, cases dst, simp_all) done lemma dist_measure_has_density: "v ∈ type_universe (dist_param_type dst) ⟹ has_density (dist_measure dst v) (stock_measure (dist_result_type dst)) (dist_dens dst v)" proof (intro has_densityI) fix v assume "v ∈ type_universe (dist_param_type dst)" thus "dist_measure dst v = density (stock_measure (dist_result_type dst)) (dist_dens dst v)" by (cases dst) (auto simp: bernoulli_def uniform_int_def uniform_real_def poisson_def gaussian_def intro!: density_cong' elim!: PROD_E REAL_E INTEG_E) qed simp_all lemma subprob_space_dist_measure: "v ∈ type_universe (dist_param_type dst) ⟹ subprob_space (dist_measure dst v)" using subprob_space_kernel[OF measurable_dist_measure, of v dst] by simp lemma dist_measure_has_subprob_density: "v ∈ type_universe (dist_param_type dst) ⟹ has_subprob_density (dist_measure dst v) (stock_measure (dist_result_type dst)) (dist_dens dst v)" unfolding has_subprob_density_def by (auto intro: subprob_space_dist_measure dist_measure_has_density) lemma dist_dens_integral_space: assumes "v ∈ type_universe (dist_param_type dst)" shows "(∫⇧+u. dist_dens dst v u ∂stock_measure (dist_result_type dst)) ≤ 1" proof- let ?M = "density (stock_measure (dist_result_type dst)) (dist_dens dst v)" from assms have "(∫⇧+u. dist_dens dst v u ∂stock_measure (dist_result_type dst)) = emeasure ?M (space ?M)" by (subst space_density, subst emeasure_density) (auto intro!: measurable_dist_dens cong: nn_integral_cong') also have "?M = dist_measure dst v" using dist_measure_has_density[OF assms] by (auto dest: has_densityD) also from assms have "emeasure ... (space ...) ≤ 1" by (intro subprob_space.emeasure_space_le_1 subprob_space_dist_measure) finally show ?thesis . qed subsection ‹Typing› primrec op_type :: "pdf_operator ⇒ pdf_type ⇒ pdf_type option" where "op_type Add x = (case x of PRODUCT INTEG INTEG ⇒ Some INTEG | PRODUCT REAL REAL ⇒ Some REAL | _ ⇒ None)" | "op_type Mult x = (case x of PRODUCT INTEG INTEG ⇒ Some INTEG | PRODUCT REAL REAL ⇒ Some REAL | _ ⇒ None)" | "op_type Minus x = (case x of INTEG ⇒ Some INTEG | REAL ⇒ Some REAL | _ ⇒ None)" | "op_type Equals x = (case x of PRODUCT t1 t2 ⇒ if t1 = t2 then Some BOOL else None | _ ⇒ None)" | "op_type Less x = (case x of PRODUCT INTEG INTEG ⇒ Some BOOL | PRODUCT REAL REAL ⇒ Some BOOL | _ ⇒ None)" | "op_type (Cast t) x = (case (x, t) of (BOOL, INTEG) ⇒ Some INTEG | (BOOL, REAL) ⇒ Some REAL | (INTEG, REAL) ⇒ Some REAL | (REAL, INTEG) ⇒ Some INTEG | _ ⇒ None)" | "op_type Or x = (case x of PRODUCT BOOL BOOL ⇒ Some BOOL | _ ⇒ None)" | "op_type And x = (case x of PRODUCT BOOL BOOL ⇒ Some BOOL | _ ⇒ None)" | "op_type Not x = (case x of BOOL ⇒ Some BOOL | _ ⇒ None)" | "op_type Inverse x = (case x of REAL ⇒ Some REAL | _ ⇒ None)" | "op_type Fact x = (case x of INTEG ⇒ Some INTEG | _ ⇒ None)" | "op_type Sqrt x = (case x of REAL ⇒ Some REAL | _ ⇒ None)" | "op_type Exp x = (case x of REAL ⇒ Some REAL | _ ⇒ None)" | "op_type Ln x = (case x of REAL ⇒ Some REAL | _ ⇒ None)" | "op_type Pi x = (case x of UNIT ⇒ Some REAL | _ ⇒ None)" | "op_type Pow x = (case x of PRODUCT REAL INTEG ⇒ Some REAL | PRODUCT INTEG INTEG ⇒ Some INTEG | _ ⇒ None)" | "op_type Fst x = (case x of PRODUCT t _ ⇒ Some t | _ ⇒ None)" | "op_type Snd x = (case x of PRODUCT _ t ⇒ Some t | _ ⇒ None)" subsection ‹Semantics› abbreviation (input) de_bruijn_insert (infixr "⋅" 65) where "de_bruijn_insert x f ≡ case_nat x f" inductive expr_typing :: "tyenv ⇒ expr ⇒ pdf_type ⇒ bool" ("(1_/ ⊢/ (_ :/ _))" [50,0,50] 50) where et_var: "Γ ⊢ Var x : Γ x" | et_val: "Γ ⊢ Val v : val_type v" | et_let: "Γ ⊢ e1 : t1 ⟹ t1 ⋅ Γ ⊢ e2 : t2 ⟹ Γ ⊢ LetVar e1 e2 : t2" | et_op: "Γ ⊢ e : t ⟹ op_type oper t = Some t' ⟹ Γ ⊢ Operator oper e : t'" | et_pair: "Γ ⊢ e1 : t1 ⟹ Γ ⊢ e2 : t2 ⟹ Γ ⊢ <e1, e2> : PRODUCT t1 t2" | et_rand: "Γ ⊢ e : dist_param_type dst ⟹ Γ ⊢ Random dst e : dist_result_type dst" | et_if: "Γ ⊢ b : BOOL ⟹ Γ ⊢ e1 : t ⟹ Γ ⊢ e2 : t ⟹ Γ ⊢ IF b THEN e1 ELSE e2 : t" | et_fail: "Γ ⊢ Fail t : t" lemma expr_typing_cong': "Γ ⊢ e : t ⟹ (⋀x. x ∈ free_vars e ⟹ Γ x = Γ' x) ⟹ Γ' ⊢ e : t" proof (induction arbitrary: Γ' rule: expr_typing.induct) case (et_let Γ e1 t1 e2 t2 Γ') have "Γ' ⊢ e1 : t1" using et_let.prems by (intro et_let.IH(1)) auto moreover have "case_nat t1 Γ' ⊢ e2 : t2" using et_let.prems by (intro et_let.IH(2)) (auto split: nat.split) ultimately show ?case by (auto intro!: expr_typing.intros) qed (auto intro!: expr_typing.intros) lemma expr_typing_cong: "(⋀x. x ∈ free_vars e ⟹ Γ x = Γ' x) ⟹ Γ ⊢ e : t ⟷ Γ' ⊢ e : t" by (intro iffI) (simp_all add: expr_typing_cong') inductive_cases expr_typing_valE[elim]: "Γ ⊢ Val v : t" inductive_cases expr_typing_varE[elim]: "Γ ⊢ Var x : t" inductive_cases expr_typing_letE[elim]: "Γ ⊢ LetVar e1 e2 : t" inductive_cases expr_typing_ifE[elim]: "Γ ⊢ IfThenElse b e1 e2 : t" inductive_cases expr_typing_opE[elim]: "Γ ⊢ Operator oper e : t" inductive_cases expr_typing_pairE[elim]: "Γ ⊢ <e1, e2> : t" inductive_cases expr_typing_randE[elim]: "Γ ⊢ Random dst e : t" inductive_cases expr_typing_failE[elim]: "Γ ⊢ Fail t : t'" lemma expr_typing_unique: "Γ ⊢ e : t ⟹ Γ ⊢ e : t' ⟹ t = t'" apply (induction arbitrary: t' rule: expr_typing.induct) apply blast apply blast apply (erule expr_typing_letE, blast) apply (erule expr_typing_opE, simp) apply (erule expr_typing_pairE, blast) apply (erule expr_typing_randE, blast) apply (erule expr_typing_ifE, blast) apply blast done fun expr_type :: "tyenv ⇒ expr ⇒ pdf_type option" where "expr_type Γ (Var x) = Some (Γ x)" | "expr_type Γ (Val v) = Some (val_type v)" | "expr_type Γ (LetVar e1 e2) = (case expr_type Γ e1 of Some t ⇒ expr_type (case_nat t Γ) e2 | None ⇒ None)" | "expr_type Γ (Operator oper e) = (case expr_type Γ e of Some t ⇒ op_type oper t | None ⇒ None)" | "expr_type Γ (<e1, e2>) = (case (expr_type Γ e1, expr_type Γ e2) of (Some t1, Some t2) ⇒ Some (PRODUCT t1 t2) | _ ⇒ None)" | "expr_type Γ (Random dst e) = (if expr_type Γ e = Some (dist_param_type dst) then Some (dist_result_type dst) else None)" | "expr_type Γ (IF b THEN e1 ELSE e2) = (if expr_type Γ b = Some BOOL then (case (expr_type Γ e1, expr_type Γ e2) of (Some t, Some t') ⇒ if t = t' then Some t else None | _ ⇒ None) else None)" | "expr_type Γ (Fail t) = Some t" lemma expr_type_Some_iff: "expr_type Γ e = Some t ⟷ Γ ⊢ e : t" apply rule apply (induction e arbitrary: Γ t, auto intro!: expr_typing.intros split: option.split_asm if_split_asm) [] apply (induction rule: expr_typing.induct, auto simp del: fun_upd_apply) done lemmas expr_typing_code[code_unfold] = expr_type_Some_iff[symmetric] subsubsection ‹Countable types› primrec countable_type :: "pdf_type ⇒ bool" where "countable_type UNIT = True" | "countable_type BOOL = True" | "countable_type INTEG = True" | "countable_type REAL = False" | "countable_type (PRODUCT t1 t2) = (countable_type t1 ∧ countable_type t2)" lemma countable_type_countable[dest]: "countable_type t ⟹ countable (space (stock_measure t))" by (induction t) (auto simp: pair_measure_countable space_embed_measure space_pair_measure stock_measure.simps) lemma countable_type_imp_count_space: "countable_type t ⟹ stock_measure t = count_space (type_universe t)" proof (subst space_stock_measure[symmetric], induction t) case (PRODUCT t1 t2) hence countable: "countable_type t1" "countable_type t2" by simp_all note A = PRODUCT.IH(1)[OF countable(1)] and B = PRODUCT.IH(2)[OF countable(2)] show "stock_measure (PRODUCT t1 t2) = count_space (space (stock_measure (PRODUCT t1 t2)))" apply (subst (1 2) stock_measure.simps) apply (subst (1 2) A, subst (1 2) B) apply (subst (1 2) pair_measure_countable) apply (auto intro: countable_type_countable simp: countable simp del: space_stock_measure) [2] apply (subst (1 2) embed_measure_count_space, force intro: injI) apply simp done qed (simp_all add: stock_measure.simps) lemma return_val_countable: assumes "countable_type (val_type v)" shows "return_val v = density (stock_measure (val_type v)) (indicator {v})" (is "?M1 = ?M2") proof (rule measure_eqI) let ?M3 = "count_space (type_universe (val_type v))" fix X assume asm: "X ∈ ?M1" with assms have "emeasure ?M2 X = ∫⇧+ x. indicator {v} x * indicator X x ∂count_space (type_universe (val_type v))" by (simp add: return_val_def emeasure_density countable_type_imp_count_space) also have "(λx. indicator {v} x * indicator X x :: ennreal) = (λx. indicator (X ∩ {v}) x)" by (rule ext, subst Int_commute) (simp split: split_indicator) also have "nn_integral ?M3 ... = emeasure ?M3 (X ∩ {v})" by (subst nn_integral_indicator[symmetric]) auto also from asm have "... = emeasure ?M1 X" by (auto simp: return_val_def split: split_indicator) finally show "emeasure ?M1 X = emeasure ?M2 X" .. qed (simp add: return_val_def) subsection ‹Semantics› definition bool_to_int :: "bool ⇒ int" where "bool_to_int b = (if b then 1 else 0)" lemma measurable_bool_to_int[measurable]: "bool_to_int ∈ measurable (count_space UNIV) (count_space UNIV)" by (rule measurable_count_space) definition bool_to_real :: "bool ⇒ real" where "bool_to_real b = (if b then 1 else 0)" lemma measurable_bool_to_real[measurable]: "bool_to_real ∈ borel_measurable (count_space UNIV)" by (rule borel_measurable_count_space) definition safe_ln :: "real ⇒ real" where "safe_ln x = (if x > 0 then ln x else 0)" lemma safe_ln_gt_0[simp]: "x > 0 ⟹ safe_ln x = ln x" by (simp add: safe_ln_def) lemma borel_measurable_safe_ln[measurable]: "safe_ln ∈ borel_measurable borel" unfolding safe_ln_def[abs_def] by simp definition safe_sqrt :: "real ⇒ real" where "safe_sqrt x = (if x ≥ 0 then sqrt x else 0)" lemma safe_sqrt_ge_0[simp]: "x ≥ 0 ⟹ safe_sqrt x = sqrt x" by (simp add: safe_sqrt_def) lemma borel_measurable_safe_sqrt[measurable]: "safe_sqrt ∈ borel_measurable borel" unfolding safe_sqrt_def[abs_def] by simp fun op_sem :: "pdf_operator ⇒ val ⇒ val" where "op_sem Add = lift_RealIntVal2 (+) (+)" | "op_sem Mult = lift_RealIntVal2 (*) (*)" | "op_sem Minus = lift_RealIntVal uminus uminus" | "op_sem Equals = (λ <|v1, v2|> ⇒ BoolVal (v1 = v2))" | "op_sem Less = lift_Comp (<) (<)" | "op_sem Or = (λ <|BoolVal a, BoolVal b|> ⇒ BoolVal (a ∨ b))" | "op_sem And = (λ <|BoolVal a, BoolVal b|> ⇒ BoolVal (a ∧ b))" | "op_sem Not = (λ BoolVal a ⇒ BoolVal (¬a))" | "op_sem (Cast t) = (case t of INTEG ⇒ (λ BoolVal b ⇒ IntVal (bool_to_int b) | RealVal r ⇒ IntVal (floor r)) | REAL ⇒ (λ BoolVal b ⇒ RealVal (bool_to_real b) | IntVal i ⇒ RealVal (real_of_int i)))" | "op_sem Inverse = lift_RealVal inverse" | "op_sem Fact = lift_IntVal (λi::int. fact (nat i))" | "op_sem Sqrt = lift_RealVal safe_sqrt" | "op_sem Exp = lift_RealVal exp" | "op_sem Ln = lift_RealVal safe_ln" | "op_sem Pi = (λ_. RealVal pi)" | "op_sem Pow = (λ <|RealVal x, IntVal n|> ⇒ if n < 0 then RealVal 0 else RealVal (x ^ nat n) | <|IntVal x, IntVal n|> ⇒ if n < 0 then IntVal 0 else IntVal (x ^ nat n))" | "op_sem Fst = fst ∘ extract_pair" | "op_sem Snd = snd ∘ extract_pair" text ‹The semantics of expressions. Assumes that the expression given is well-typed.› primrec expr_sem :: "state ⇒ expr ⇒ val measure" where "expr_sem σ (Var x) = return_val (σ x)" | "expr_sem σ (Val v) = return_val v" | "expr_sem σ (LET e1 IN e2) = do { v ← expr_sem σ e1; expr_sem (v ⋅ σ) e2 }" | "expr_sem σ (oper$$ e) =
do {
x ← expr_sem σ e;
return_val (op_sem oper x)
}"
| "expr_sem σ <v, w> =
do {
x ← expr_sem σ v;
y ← expr_sem σ w;
return_val <|x, y|>
}"
| "expr_sem σ (IF b THEN e1 ELSE e2) =
do {
b' ← expr_sem σ b;
if b' = TRUE then expr_sem σ e1 else expr_sem σ e2
}"
| "expr_sem σ (Random dst e) =
do {
x ← expr_sem σ e;
dist_measure dst x
}"
| "expr_sem σ (Fail t) = null_measure (stock_measure t)"

lemma expr_sem_pair_vars: "expr_sem σ <Var x, Var y> = return_val <|σ x, σ y|>"
by (simp add: return_val_def bind_return[where N="PRODUCT (val_type (σ x)) (val_type (σ y))"]
cong: bind_cong_simp)

text ‹
Well-typed expressions produce a result in the measure space that corresponds to their type
›

lemma op_sem_val_type:
"op_type oper (val_type v) = Some t' ⟹ val_type (op_sem oper v) = t'"
by (cases oper) (auto split: val.split if_split_asm pdf_type.split_asm
simp: lift_RealIntVal_def lift_Comp_def
lift_IntVal_def lift_RealVal_def lift_RealIntVal2_def
elim!: PROD_E INTEG_E REAL_E)

lemma sets_expr_sem:
"Γ ⊢ w : t ⟹ (∀x ∈ free_vars w. val_type (σ x) = Γ x) ⟹
sets (expr_sem σ w) = sets (stock_measure t)"
proof (induction arbitrary: σ rule: expr_typing.induct)
case (et_var Γ x σ)
thus ?case by (simp add: return_val_def)
next
case (et_val Γ v σ)
thus ?case by (simp add: return_val_def)
next
case (et_let Γ e1 t1 e2 t2 σ)
hence "sets (expr_sem σ e1) = sets (stock_measure t1)" by simp
from sets_eq_imp_space_eq[OF this]
have A: "space (expr_sem σ e1) = type_universe t1" by (simp add:)
hence B: "(SOME x. x ∈ space (expr_sem σ e1)) ∈ space (expr_sem σ e1)" (is "?v ∈ _")
unfolding some_in_eq by simp
with A et_let have "sets (expr_sem (case_nat ?v σ) e2) = sets (stock_measure t2)"
by (intro et_let.IH(2)) (auto split: nat.split)
with B show "sets (expr_sem σ (LetVar e1 e2)) = sets (stock_measure t2)"
by (subst expr_sem.simps, subst bind_nonempty) auto
next
case (et_op Γ e t oper t' σ)
from et_op.IH[of σ] and et_op.prems
have [simp]: "sets (expr_sem σ e) = sets (stock_measure t)" by simp
from sets_eq_imp_space_eq[OF this]
have [simp]: "space (expr_sem σ e) = type_universe t" by (simp add:)
have "(SOME x. x ∈ space (expr_sem σ e)) ∈ space (expr_sem σ e)"
unfolding some_in_eq by simp
with et_op show ?case by (simp add: bind_nonempty return_val_def op_sem_val_type)
next
case (et_pair Γ e1 t1 e2 t2 σ)
hence [simp]: "space (expr_sem σ e1) = type_universe t1"
"space (expr_sem σ e2) = type_universe t2"
have "(SOME x. x ∈ space (expr_sem σ e1)) ∈ space (expr_sem σ e1)"
"(SOME x. x ∈ space (expr_sem σ e2)) ∈ space (expr_sem σ e2)"
unfolding some_in_eq by simp_all
with et_pair.hyps show ?case by (simp add: bind_nonempty return_val_def)
next
case (et_rand Γ e dst σ)
from et_rand.IH[of σ] et_rand.prems
have "sets (expr_sem σ e) = sets (stock_measure (dist_param_type dst))" by simp
from this sets_eq_imp_space_eq[OF this]
show ?case
apply simp_all
apply (subst sets_bind)
apply auto
done
next
case (et_if Γ b e1 t e2 σ)
have "sets (expr_sem σ b) = sets (stock_measure BOOL)"
using et_if.prems by (intro et_if.IH) simp
from sets_eq_imp_space_eq[OF this]
have "space (expr_sem σ b) ≠ {}" by simp
moreover have "sets (expr_sem σ e1) = sets (stock_measure t)"
"sets (expr_sem σ e2) = sets (stock_measure t)"
using et_if.prems by (intro et_if.IH, simp)+
ultimately show ?case by (simp add: bind_nonempty)
qed simp_all

lemma space_expr_sem:
"Γ ⊢ w : t ⟹ (∀x ∈ free_vars w. val_type (σ x) = Γ x)
⟹ space (expr_sem σ w) = type_universe t"
by (subst space_stock_measure[symmetric]) (intro sets_expr_sem sets_eq_imp_space_eq)

lemma measurable_expr_sem_eq:
"Γ ⊢ e : t ⟹ σ ∈ space (state_measure V Γ) ⟹ free_vars e ⊆ V ⟹
measurable (expr_sem σ e) = measurable (stock_measure t)"
by (intro ext measurable_cong_sets sets_expr_sem)
(auto simp: state_measure_def space_PiM dest: PiE_mem)

lemma measurable_expr_semI:
"Γ ⊢ e : t ⟹ σ ∈ space (state_measure V Γ) ⟹ free_vars e ⊆ V ⟹
f ∈ measurable (stock_measure t) M ⟹ f ∈ measurable (expr_sem σ e) M"
by (subst measurable_expr_sem_eq)

lemma expr_sem_eq_on_vars:
"(⋀x. x∈free_vars e ⟹ σ⇩1 x = σ⇩2 x) ⟹ expr_sem σ⇩1 e = expr_sem σ⇩2 e"
proof (induction e arbitrary: σ⇩1 σ⇩2)
case (LetVar e1 e2 σ1 σ2)
from LetVar.prems have A: "expr_sem σ1 e1 = expr_sem σ2 e1" by (rule LetVar.IH(1)) simp_all
from LetVar.prems show ?case
by (subst (1 2) expr_sem.simps, subst A)
(auto intro!: bind_cong LetVar.IH(2) split: nat.split)
next
case (Operator oper e σ1 σ2)
from Operator.IH[OF Operator.prems] show ?case by simp
next
case (Pair e1 e2 σ1 σ2)
from Pair.prems have "expr_sem σ1 e1 = expr_sem σ2 e1" by (intro Pair.IH) auto
moreover from Pair.prems have "expr_sem σ1 e2 = expr_sem σ2 e2" by (intro Pair.IH) auto
ultimately show ?case by simp
next
case (Random dst e σ1 σ2)
from Random.prems have A: "expr_sem σ1 e = expr_sem σ2 e" by (rule Random.IH) simp_all
show ?case
by (subst (1 2) expr_sem.simps, subst A) (auto intro!: bind_cong)
next
case (IfThenElse b e1 e2 σ1 σ2)
have A: "expr_sem σ1 b = expr_sem σ2 b"
"expr_sem σ1 e1 = expr_sem σ2 e1"
"expr_sem σ1 e2 = expr_sem σ2 e2"
using IfThenElse.prems by (intro IfThenElse.IH, simp)+
thus ?case by (simp only: expr_sem.simps A)
qed simp_all

subsection ‹Measurability›

lemma borel_measurable_eq[measurable (raw)]:
assumes [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
shows "Measurable.pred M (λx. f x = (g x::real))"
proof -
have *: "(λx. f x = g x) = (λx. f x - g x = 0)"
by simp
show ?thesis
unfolding * by measurable
qed

lemma measurable_equals:
"(λ(x,y). x = y) ∈ measurable (stock_measure t ⨂⇩M stock_measure t) (count_space UNIV)"
proof (induction t)
case REAL
let ?f = "λx. extract_real (fst x) = extract_real (snd x)"
show ?case
proof (subst measurable_cong)
fix x assume "x ∈ space (stock_measure REAL ⨂⇩M stock_measure REAL)"
thus "(λ(x,y). x = y) x = ?f x"
by (auto simp: space_pair_measure elim!: REAL_E)
next
show "?f ∈ measurable (stock_measure REAL ⨂⇩M stock_measure REAL) (count_space UNIV)"
by measurable
qed
next
case (PRODUCT t1 t2)
let ?g = "λ(x,y). x = y"
let ?f = "λx. ?g (fst (extract_pair (fst x)), fst (extract_pair (snd x))) ∧
?g (snd (extract_pair (fst x)), snd (extract_pair (snd x)))"
show ?case
proof (subst measurable_cong)
fix x assume "x ∈ space (stock_measure (PRODUCT t1 t2) ⨂⇩M stock_measure (PRODUCT t1 t2))"
thus "(λ(x,y). x = y) x = ?f x"
apply (auto simp: space_pair_measure)
apply (elim PROD_E)
apply simp
done
next
note PRODUCT[measurable]
show "Measurable.pred (stock_measure (PRODUCT t1 t2) ⨂⇩M stock_measure (PRODUCT t1 t2)) ?f"
by measurable
qed

lemma measurable_equals_stock_measure[measurable (raw)]:
assumes "f ∈ measurable M (stock_measure t)" "g ∈ measurable M (stock_measure t)"
shows "Measurable.pred M (λx. f x = g x)"
using measurable_compose[OF measurable_Pair[OF assms] measurable_equals] by simp

lemma measurable_op_sem:
assumes "op_type oper t = Some t'"
shows "op_sem oper ∈ measurable (stock_measure t) (stock_measure t')"
proof (cases oper)
case Fst with assms show ?thesis by (simp split: pdf_type.split_asm)
next
case Snd with assms show ?thesis by (simp split: pdf_type.split_asm)
next
case Equals with assms show ?thesis
by (auto intro!: val_case_stock_measurable split: if_split_asm)
next
case Pow with assms show ?thesis
apply (auto intro!: val_case_stock_measurable split: pdf_type.splits)
apply (subst measurable_cong[where
g="λ(x, n). if extract_int n < 0 then RealVal 0 else RealVal (extract_real x ^ nat (extract_int n))"])
apply (auto simp: space_pair_measure elim!: REAL_E INTEG_E)
done
next
case Less with assms show ?thesis
by (auto split: pdf_type.splits)
qed (insert assms, auto split: pdf_type.split_asm intro!: val_case_stock_measurable)

definition shift_var_set :: "vname set ⇒ vname set" where
"shift_var_set V = insert 0 (Suc  V)"

lemma shift_var_set_0[simp]: "0 ∈ shift_var_set V"

lemma shift_var_set_Suc[simp]: "Suc x ∈ shift_var_set V ⟷ x ∈ V"

lemma case_nat_update_0[simp]: "(case_nat x σ)(0 := y) = case_nat y σ"
by (intro ext) (simp split: nat.split)

lemma case_nat_delete_var_1[simp]:
"case_nat x (case_nat y σ) ∘ case_nat 0 (λx. Suc (Suc x)) = case_nat x σ"
by (intro ext) (simp split: nat.split)

lemma delete_var_1_vimage[simp]:
"case_nat 0 (λx. Suc (Suc x)) - (shift_var_set (shift_var_set V)) = shift_var_set V"
by (auto simp: shift_var_set_def split: nat.split_asm)

lemma measurable_case_nat[measurable]:
assumes "g ∈ measurable R N" "h ∈ measurable R (Pi⇩M V M)"
shows "(λx. case_nat (g x) (h x)) ∈ measurable R (Pi⇩M (shift_var_set V) (case_nat N M))"
proof (rule measurable_Pair_compose_split[OF _ assms])
have "(λ(t,f). λx∈shift_var_set V. case_nat t f x)
∈ measurable (N ⨂⇩M PiM V M) (PiM (shift_var_set V) (case_nat N M))" (is ?P)
unfolding shift_var_set_def
by (subst measurable_split_conv, rule measurable_restrict) (auto split: nat.split_asm)
also have "⋀x f. f ∈ space (PiM V M) ⟹ x ∉ V ⟹ undefined = f x"
by (rule sym, subst (asm) space_PiM, erule PiE_arb)
hence "?P ⟷ (λ(t,f). case_nat t f)
∈ measurable (N ⨂⇩M PiM V M) (PiM (shift_var_set V) (case_nat N M))" (is "_ = ?P")
by (intro measurable_cong ext)
(auto split: nat.split simp: inj_image_mem_iff space_pair_measure shift_var_set_def)
finally show ?P .
qed

lemma measurable_case_nat'[measurable]:
assumes "g ∈ measurable R (stock_measure t)" "h ∈ measurable R (state_measure V Γ)"
shows "(λx. case_nat (g x) (h x)) ∈
measurable R (state_measure (shift_var_set V) (case_nat t Γ))"
proof-
have A: "(λx. stock_measure (case_nat t Γ x)) =
case_nat (stock_measure t) (λx. stock_measure (Γ x))"
by (intro ext) (simp split: nat.split)
show ?thesis using assms unfolding state_measure_def by (simp add: A)
qed

lemma case_nat_in_state_measure[intro]:
assumes "x ∈ type_universe t1" "σ ∈ space (state_measure V Γ)"
shows "case_nat x σ ∈ space (state_measure (shift_var_set V) (case_nat t1 Γ))"
apply (rule measurable_space[OF measurable_case_nat'])
apply (rule measurable_ident_sets[OF refl], rule measurable_const[OF assms(2)])
using assms
apply simp
done

lemma subset_shift_var_set:
"Suc - A ⊆ V ⟹ A ⊆ shift_var_set V"
by (rule subsetI, rename_tac x, case_tac x) (auto simp: shift_var_set_def)

lemma measurable_expr_sem[measurable]:
assumes "Γ ⊢ e : t" and "free_vars e ⊆ V"
shows "(λσ. expr_sem σ e) ∈ measurable (state_measure V Γ)
(subprob_algebra (stock_measure t))"
using assms
proof (induction arbitrary: V rule: expr_typing.induct)
case (et_var Γ x)
have A: "(λσ. expr_sem σ (Var x)) = return_val ∘ (λσ. σ x)" by (simp add: o_def)
with et_var show ?case unfolding state_measure_def
by (subst A) (rule measurable_comp[OF measurable_component_singleton], simp_all)
next
case (et_val Γ v)
thus ?case by (auto intro!: measurable_const subprob_space_return
simp: space_subprob_algebra return_val_def)
next
case (et_let Γ e1 t1 e2 t2 V)
have A: "(λv. stock_measure (case_nat t1 Γ v)) =
case_nat (stock_measure t1) (λv. stock_measure (Γ v))"
by (rule ext) (simp split: nat.split)
from et_let.prems and et_let.hyps show ?case
apply (subst expr_sem.simps, intro measurable_bind)
apply (rule et_let.IH(1), simp)
apply (rule measurable_compose[OF _ et_let.IH(2)[of "shift_var_set V"]])
done
next
case (et_op Γ e t oper t')
thus ?case by (auto intro!: measurable_bind2 measurable_compose[OF _ measurable_return_val]
measurable_op_sem cong: measurable_cong)
next
case (et_pair t t1 t2 Γ e1 e2)
have "inj (λ(a,b). <|a, b|>)" by (auto intro: injI)
with et_pair show ?case
apply (subst expr_sem.simps)
apply (rule measurable_bind, (auto) [])
apply (rule measurable_bind[OF measurable_compose[OF measurable_fst]], (auto) [])
apply (rule measurable_compose[OF _ measurable_return_val], simp)
done
next
case (et_rand Γ e dst V)
from et_rand.prems and et_rand.hyps show ?case
by (auto intro!: et_rand.IH measurable_compose[OF measurable_snd]
measurable_bind measurable_dist_measure)
next
case (et_if Γ b e1 t e2 V)
let ?M = "λe t. (λσ. expr_sem σ e) ∈
measurable (state_measure V Γ) (subprob_algebra (stock_measure t))"
from et_if.prems have A[measurable]: "?M b BOOL" "?M e1 t" "?M e2 t" by (intro et_if.IH, simp)+
show ?case by (subst expr_sem.simps, rule measurable_bind[OF A(1)]) simp_all
next
case (et_fail Γ t V)
show ?case
by (auto intro!: measurable_subprob_algebra subprob_spaceI simp:)
qed

subsection ‹Randomfree expressions›

fun randomfree :: "expr ⇒ bool" where
"randomfree (Val _) = True"
| "randomfree (Var _) = True"
| "randomfree (Pair e1 e2) = (randomfree e1 ∧ randomfree e2)"
| "randomfree (Operator _ e) = randomfree e"
| "randomfree (LetVar e1 e2) = (randomfree e1 ∧ randomfree e2)"
| "randomfree (IfThenElse b e1 e2) = (randomfree b ∧ randomfree e1 ∧ randomfree e2)"
| "randomfree (Random _ _) = False"
| "randomfree (Fail _) = False"

primrec expr_sem_rf :: "state ⇒ expr ⇒ val" where
"expr_sem_rf _ (Val v) = v"
| "expr_sem_rf σ (Var x) = σ x"
| "expr_sem_rf σ (<e1, e2>) = <|expr_sem_rf σ e1, expr_sem_rf σ e2|>"
| "expr_sem_rf σ (Operator oper e) = op_sem oper (expr_sem_rf σ e)"
| "expr_sem_rf σ (LetVar e1 e2) = expr_sem_rf (expr_sem_rf σ e1 ⋅ σ) e2"
| "expr_sem_rf σ (IfThenElse b e1 e2) =
(if expr_sem_rf σ b = BoolVal True then expr_sem_rf σ e1 else expr_sem_rf σ e2)"
| "expr_sem_rf _ (Random _ _) = undefined"
| "expr_sem_rf _ (Fail _) = undefined"

lemma measurable_expr_sem_rf[measurable]:
"Γ ⊢ e : t ⟹ randomfree e ⟹ free_vars e ⊆ V ⟹
(λσ. expr_sem_rf σ e) ∈ measurable (state_measure V Γ) (stock_measure t)"
proof (induction arbitrary: V rule: expr_typing.induct)
case (et_val Γ v V)
thus ?case by (auto intro!: measurable_const simp:)
next
case (et_var Γ x V)
thus ?case by (auto simp: state_measure_def intro!: measurable_component_singleton)
next
case (et_pair Γ e1 t1 e2 t2 V)
have "inj (λ(x,y). <|x, y|>)" by (auto intro: injI)
with et_pair show ?case by simp
next
case (et_op Γ e t oper t' V)
thus ?case by (auto intro!: measurable_compose[OF _ measurable_op_sem])
next
case (et_let Γ e1 t1 e2 t2 V)
hence M1: "(λσ. expr_sem_rf σ e1) ∈ measurable (state_measure V Γ) (stock_measure t1)"
and M2: "(λσ. expr_sem_rf σ e2) ∈ measurable (state_measure (shift_var_set V) (case_nat t1 Γ))
(stock_measure t2)"
using subset_shift_var_set
by (auto intro!: et_let.IH(1)[of V] et_let.IH(2)[of "shift_var_set V"])
have "(λσ. expr_sem_rf σ (LetVar e1 e2)) =
(λσ. expr_sem_rf σ e2) ∘ (λ(σ,y). case_nat y σ) ∘ (λσ. (σ, expr_sem_rf σ e1))" (is "_ = ?f")
by (intro ext) simp
also have "?f ∈ measurable (state_measure V Γ) (stock_measure t2)"
apply (intro measurable_comp, rule measurable_Pair, rule measurable_ident_sets[OF refl])
apply (rule M1, subst measurable_split_conv, rule measurable_case_nat')
apply (rule measurable_snd, rule measurable_fst, rule M2)
done
finally show ?case .

lemma expr_sem_rf_sound:
"Γ ⊢ e : t ⟹ randomfree e ⟹ free_vars e ⊆ V ⟹ σ ∈ space (state_measure V Γ) ⟹
return_val (expr_sem_rf σ e) = expr_sem σ e"
proof (induction arbitrary: V σ rule: expr_typing.induct)
case (et_val Γ v)
thus ?case by simp
next
case (et_var Γ x)
thus ?case by simp
next
case (et_pair Γ e1 t1 e2 t2 V σ)
let ?M = "state_measure V Γ"
from et_pair.hyps and et_pair.prems
have e1: "return_val (expr_sem_rf σ e1) = expr_sem σ e1" and
e2: "return_val (expr_sem_rf σ e2) = expr_sem σ e2"
by (auto intro!: et_pair.IH[of V])

from e1 and et_pair.prems have "space (return_val (expr_sem_rf σ e1)) = type_universe t1"
by (subst e1, subst space_expr_sem[OF et_pair.hyps(1)])
(auto dest: state_measure_var_type)
hence A: "val_type (expr_sem_rf σ e1) = t1" "expr_sem_rf σ e1 ∈ type_universe t1"
from e2 and et_pair.prems have "space (return_val (expr_sem_rf σ e2)) = type_universe t2"
by (subst e2, subst space_expr_sem[OF et_pair.hyps(2)])
(auto dest: state_measure_var_type)
hence B: "val_type (expr_sem_rf σ e2) = t2" "expr_sem_rf σ e2 ∈ type_universe t2"

have "expr_sem σ (<e1, e2>) = expr_sem σ e1 ⤜
(λv. expr_sem σ e2 ⤜ (λw. return_val (<|v,w|>)))" by simp
also have "expr_sem σ e1 = return (stock_measure t1) (expr_sem_rf σ e1)"
using e1 by (simp add: et_pair.prems return_val_def A)
also have "... ⤜ (λv. expr_sem σ e2 ⤜ (λw. return_val (<|v,w|>))) =
... ⤜ (λv. return_val (<|v, expr_sem_rf σ e2|>))"
proof (intro bind_cong refl)
fix v assume "v ∈ space (return (stock_measure t1) (expr_sem_rf σ e1))"
hence v: "val_type v = t1" "v ∈ type_universe t1" by (simp_all add:)
have "expr_sem σ e2 ⤜ (λw. return_val (<|v,w|>)) =
return (stock_measure t2) (expr_sem_rf σ e2) ⤜ (λw. return_val (<|v,w|>))"
using e2 by (simp add: et_pair.prems return_val_def B)
also have "... = return (stock_measure t2) (expr_sem_rf σ e2) ⤜
(λw. return (stock_measure (PRODUCT t1 t2)) (<|v,w|>))"
proof (intro bind_cong refl)
fix w assume "w ∈ space (return (stock_measure t2) (expr_sem_rf σ e2))"
hence w: "val_type w = t2" by (simp add:)
thus "return_val (<|v,w|>) = return (stock_measure (PRODUCT t1 t2)) (<|v,w|>)"
by (auto simp: return_val_def v w)
qed
also have "... = return_val (<|v, expr_sem_rf σ e2|>)"
using v B
by (subst bind_return[where N="PRODUCT t1 t2"]) (auto simp: return_val_def)
finally show "expr_sem σ e2 ⤜ (λw. return_val (<|v,w|>)) = return_val (<|v, expr_sem_rf σ e2|>)" .
qed
also have "(λv. <|v, expr_sem_rf σ e2|>) ∈ measurable (stock_measure t1) (stock_measure (PRODUCT t1 t2))"
using B by (auto intro!: injI)
hence "return (stock_measure t1) (expr_sem_rf σ e1) ⤜ (λv. return_val (<|v, expr_sem_rf σ e2|>)) =
return_val (<|expr_sem_rf σ e1, expr_sem_rf σ e2|>)"
by (subst bind_return, rule measurable_compose[OF _ measurable_return_val])
(auto simp: A)
finally show "return_val (expr_sem_rf σ (<e1,e2>)) = expr_sem σ (<e1, e2>)" by simp
next
case (et_if Γ b e1 t e2 V σ)
let ?P = "λe. expr_sem σ e = return_val (expr_sem_rf σ e)"
from et_if.prems have A: "?P b" "?P e1" "?P e2" by ((intro et_if.IH[symmetric], simp_all) [])+
from et_if.prems and et_if.hyps have "space (expr_sem σ b) = type_universe BOOL"
by (intro space_expr_sem) (auto simp: state_measure_var_type)
hence [simp]: "val_type (expr_sem_rf σ b) = BOOL" by (simp add: A return_val_def)
have B: "return_val (expr_sem_rf σ e1) ∈ space (subprob_algebra (stock_measure t))"
"return_val (expr_sem_rf σ e2) ∈ space (subprob_algebra (stock_measure t))"
using et_if.hyps and et_if.prems
by ((subst A[symmetric], intro measurable_space[OF measurable_expr_sem], auto) [])+
thus ?case
by (auto simp: A bind_return_val''[where M=t])
next
case (et_op Γ e t oper t' V)
let ?M = "PiM V (λx. stock_measure (Γ x))"
from et_op.prems have e: "return_val (expr_sem_rf σ e) = expr_sem σ e"
by (intro et_op.IH[of V]) auto

with et_op.prems have "space (return_val (expr_sem_rf σ e)) = type_universe t"
by (subst e, subst space_expr_sem[OF et_op.hyps(1)])
(auto dest: state_measure_var_type)
hence A: "val_type (expr_sem_rf σ e) = t" "expr_sem_rf σ e ∈ type_universe t"
from et_op.prems e
have "expr_sem σ (Operator oper e) =
return_val (expr_sem_rf σ e) ⤜ (λv. return_val (op_sem oper v))" by simp
also have "... = return_val (op_sem oper (expr_sem_rf σ e))"
by (subst return_val_def, rule bind_return,
rule measurable_compose[OF measurable_op_sem measurable_return_val])
(auto simp: A et_op.hyps)
finally show "return_val (expr_sem_rf σ (Operator oper e)) = expr_sem σ (Operator oper e)" by simp
next
case (et_let Γ e1 t1 e2 t2 V)
let ?M = "state_measure V Γ" and ?N = "state_measure (shift_var_set V) (case_nat t1 Γ)"
let ?σ' = "case_nat (expr_sem_rf σ e1) σ"
from et_let.prems have e1: "return_val (expr_sem_rf σ e1) = expr_sem σ e1"
by (auto intro!: et_let.IH(1)[of V])
from et_let.prems have S: "space (return_val (expr_sem_rf σ e1)) = type_universe t1"
by (subst e1, subst space_expr_sem[OF et_let.hyps(1)])
(auto dest: state_measure_var_type)
hence A: "val_type (expr_sem_rf σ e1) = t1" "expr_sem_rf σ e1 ∈ type_universe t1"
with et_let.prems have e2: "⋀σ. σ ∈ space ?N ⟹ return_val (expr_sem_rf σ e2) = expr_sem σ e2"
using subset_shift_var_set
by (intro et_let.IH(2)[of "shift_var_set V"]) (auto simp del: fun_upd_apply)

from et_let.prems have "expr_sem σ (LetVar e1 e2) =
return_val (expr_sem_rf σ e1) ⤜ (λv. expr_sem (case_nat v σ) e2)"
also from et_let.prems
have "... = return_val (expr_sem_rf σ e1) ⤜ (λv. return_val (expr_sem_rf (case_nat v σ) e2))"
by (intro bind_cong refl, subst e2) (auto simp: S)
also from et_let have Me2[measurable]: "(λσ. expr_sem_rf σ e2) ∈ measurable ?N (stock_measure t2)"
using subset_shift_var_set by (intro measurable_expr_sem_rf) auto
have "(λ(σ,y). case_nat y σ) ∘ (λy. (σ, y)) ∈ measurable (stock_measure t1) ?N"
using ‹σ ∈ space ?M› by simp
have  "return_val (expr_sem_rf σ e1) ⤜ (λv. return_val (expr_sem_rf (case_nat v σ) e2)) =
return_val (expr_sem_rf ?σ' e2)" using ‹σ ∈ space ?M›
by (subst return_val_def, intro bind_return, subst A)
(rule measurable_compose[OF _ measurable_return_val[of t2]], simp_all)
finally show ?case by simp
qed simp_all

lemma val_type_expr_sem_rf:
assumes "Γ ⊢ e : t" "randomfree e" "free_vars e ⊆ V" "σ ∈ space (state_measure V Γ)"
shows "val_type (expr_sem_rf σ e) = t"
proof-
have "type_universe (val_type (expr_sem_rf σ e)) = space (return_val (expr_sem_rf σ e))"
also from assms have "return_val (expr_sem_rf σ e) = expr_sem σ e"
by (intro expr_sem_rf_sound) auto
also from assms have "space ... = type_universe t"
by (intro space_expr_sem[of Γ])
(auto simp: state_measure_def space_PiM  dest: PiE_mem)
finally show ?thesis by simp
qed

lemma expr_sem_rf_eq_on_vars:
"(⋀x. x∈free_vars e ⟹ σ1 x = σ2 x) ⟹ expr_sem_rf σ1 e = expr_sem_rf σ2 e"
proof (induction e arbitrary: σ1 σ2)
case (Operator oper e σ1 σ2)
hence "expr_sem_rf σ1 e = expr_sem_rf σ2 e" by (intro Operator.IH) auto
thus ?case by simp
next
case (LetVar e1 e2 σ1 σ2)
hence A: "expr_sem_rf σ1 e1 = expr_sem_rf σ2 e1" by (intro LetVar.IH) auto
{
fix y assume "y ∈ free_vars e2"
hence "case_nat (expr_sem_rf σ1 e1) σ1 y = case_nat (expr_sem_rf σ2 e1) σ2 y"
using LetVar(3) by (auto simp add: A split: nat.split)
}
hence "expr_sem_rf (case_nat (expr_sem_rf σ1 e1) σ1) e2 =
expr_sem_rf (case_nat (expr_sem_rf σ2 e1) σ2) e2" by (intro LetVar.IH) simp
thus ?case by simp
next
case (Pair e1 e2 σ1 σ2)
have "expr_sem_rf σ1 e1 = expr_sem_rf σ2 e1" "expr_sem_rf σ1 e2 = expr_sem_rf σ2 e2"
by (intro Pair.IH, simp add: Pair)+
thus ?case by simp
next
case (IfThenElse b e1 e2 σ1 σ2)
have "expr_sem_rf σ1 b = expr_sem_rf σ2 b" "expr_sem_rf σ1 e1 = expr_sem_rf σ2 e1"
"expr_sem_rf σ1 e2 = expr_sem_rf σ2 e2" by (intro IfThenElse.IH, simp add: IfThenElse)+
thus ?case by simp
next
case (Random dst e σ1 σ2)
have "expr_sem_rf σ1 e = expr_sem_rf σ2 e" by (intro Random.IH) (simp add: Random)
thus ?case by simp
qed auto

(*
subsection {* Substitution of free variables *}

primrec expr_subst :: "expr ⇒ expr ⇒ vname ⇒ expr" ("_⟨_'/_⟩" [1000,0,0] 999) where
"(Val v)⟨_/_⟩ = Val v"
| "(Var y)⟨f/x⟩ = (if y = x then f else Var y)"
| "<e1,e2>⟨f/x⟩ = <e1⟨f/x⟩, e2⟨f/x⟩>"
| "(<oper> e)⟨f/x⟩ = <oper> (e⟨f/x⟩)"
| "(LET e1 IN e2)⟨f/x⟩ = LET y = e1⟨f/x⟩ IN if y = x then e2 else e2⟨f/x⟩"
| "(IF b THEN e1 ELSE e2)⟨f/x⟩ = IF b⟨f/x⟩ THEN e1⟨f/x⟩ ELSE e2⟨f/x⟩"
| "(Random dst e)⟨f/x⟩ = Random dst (e⟨f/x⟩)"
| "(Fail t)⟨f/x⟩ = Fail t"

primrec bound_vars :: "expr ⇒ vname set" where
"bound_vars (Val _) = {}"
| "bound_vars (Var _) = {}"
| "bound_vars <e1,e2> = bound_vars e1 ∪ bound_vars e2"
| "bound_vars (<_> e) = bound_vars e"
| "bound_vars (LET x = e1 IN e2) = {x} ∪ bound_vars e1 ∪ bound_vars e2"
| "bound_vars (IF b THEN e1 ELSE e2) = bound_vars b ∪ bound_vars e1 ∪ bound_vars e2"
| "bound_vars (Random _ e) = bound_vars e"
| "bound_vars (Fail _) = {}"

lemma expr_typing_eq_on_free_vars:
"Γ1 ⊢ e : t ⟹ (⋀x. x ∈ free_vars e ⟹ Γ1 x = Γ2 x) ⟹ Γ2 ⊢ e : t"
proof (induction arbitrary: Γ2 rule: expr_typing.induct)
case et_let
thus ?case by (intro expr_typing.intros) auto
qed (auto intro!: expr_typing.intros simp del: fun_upd_apply)

lemma expr_typing_subst:
assumes "Γ ⊢ e : t1" "Γ ⊢ f : t'" "Γ x = t'" "free_vars f ∩ bound_vars e = {}"
shows "Γ ⊢ e⟨f/x⟩ : t1"
using assms
proof (induction rule: expr_typing.induct)
case (et_let Γ e1 t1 y e2 t2)
from et_let.prems have A: "Γ ⊢ e1⟨f/x⟩ : t1" by (intro et_let.IH) auto
show ?case
proof (cases "y = x")
assume "y ≠ x"
from et_let.prems have "Γ(y := t1) ⊢ f : t'"
by (intro expr_typing_eq_on_free_vars[OF Γ ⊢ f : t']) auto
moreover from y ≠ x have "(Γ(y := t1)) x = Γ x" by simp
ultimately have "Γ(y := t1) ⊢ e2⟨f/x⟩ : t2" using et_let.prems
by (intro et_let.IH) (auto simp del: fun_upd_apply)
with A and y ≠ x show ?thesis by (auto intro: expr_typing.intros)
qed (insert et_let, auto intro!: expr_typing.intros simp del: fun_upd_apply)
qed (insert assms(2), auto intro: expr_typing.intros)

lemma expr_subst_randomfree:
assumes "Γ ⊢ f : t" "randomfree f" "free_vars f ⊆ V" "free_vars f ∩ bound_vars e = {}"
"σ ∈ space (state_measure V Γ)"
shows   "expr_sem σ (e⟨f/x⟩) = expr_sem (σ(x := expr_sem_rf f σ)) e"
using assms(1,3,4,5)
proof (induction e arbitrary: σ V Γ)
case (Pair e1 e2 σ V Γ)
from Pair.prems have "expr_sem σ (e1⟨f/x⟩) = expr_sem (σ(x := expr_sem_rf f σ)) e1"
and "expr_sem σ (e2⟨f/x⟩) = expr_sem (σ(x := expr_sem_rf f σ)) e2"
by (auto intro!: Pair.IH[of Γ V σ])
thus ?case by (simp del: fun_upd_apply)
next
case (IfThenElse b e1 e2 σ V Γ)
from IfThenElse.prems
have "expr_sem σ (b⟨f/x⟩) = expr_sem (σ(x := expr_sem_rf f σ)) b"
"expr_sem σ (e1⟨f/x⟩) = expr_sem (σ(x := expr_sem_rf f σ)) e1"
"expr_sem σ (e2⟨f/x⟩) = expr_sem (σ(x := expr_sem_rf f σ)) e2"
by (auto intro!: IfThenElse.IH[of Γ V σ])
thus ?case by (simp only: expr_sem.simps expr_subst.simps)
next
case (LetVar y e1 e2)
from LetVar.prems have A: "expr_sem σ (e1⟨f/x⟩) = expr_sem (σ(x := expr_sem_rf f σ)) e1"
by (intro LetVar.IH) auto
show ?case
proof (cases "y = x")
assume "y = x"
with LetVar.prems show ?case by (auto simp add: A simp del: fun_upd_apply)
next
assume "y ≠ x"
{
fix v assume "v ∈ space (expr_sem (σ(x := expr_sem_rf f σ)) e1)"
let ?σ' = "σ(y := v)" and ?Γ' = "Γ(y := val_type v)"
from LetVar.prems have "Γ(y := val_type v) ⊢ f : t" by (auto intro: expr_typing_eq_on_free_vars)
moreover from LetVar.prems have "?σ' ∈ space (state_measure (insert y V) ?Γ')"
by (auto simp: state_measure_def space_PiM split: if_split_asm)
ultimately have "expr_sem ?σ' (e2⟨f/x⟩) = expr_sem (?σ'(x := expr_sem_rf f ?σ')) e2"
using LetVar.prems and y ≠ x
by (intro LetVar.IH(2)[of "Γ(y := val_type v)" "insert y V"]) (auto simp del: fun_upd_apply)
also from LetVar.prems have "expr_sem_rf f ?σ' = expr_sem_rf f σ"
by (intro expr_sem_rf_eq_on_vars) auto
finally have "expr_sem (σ(y := v)) (e2⟨f/x⟩) = expr_sem (σ(x := expr_sem_rf f σ, y := v)) e2"
using y ≠ x by (subst fun_upd_twist) (simp_all del: fun_upd_apply)
}
with A and y ≠ x show ?thesis by (auto simp del: fun_upd_apply intro!: bind_cong)
qed

lemma stock_measure_context_upd:
"(λy. stock_measure ((Γ(x := t)) y)) = (λy. stock_measure (Γ y))(x := stock_measure t)"
by (intro ext) simp

lemma Let_det_eq_subst:
assumes "Γ ⊢ LET x = f IN e : t" "randomfree f" "free_vars (LET x = f IN e) ⊆ V"
"free_vars f ∩ bound_vars e = {}" "σ ∈ space (state_measure V Γ)"
shows   "expr_sem σ (LET x = f IN e) = expr_sem σ (e⟨f/x⟩)"
proof-
from assms(1) obtain t' where t1: "Γ ⊢ f : t'" and t2: "Γ(x := t') ⊢ e : t" by auto
with assms have "expr_sem σ (LET x = f IN e) =
return_val (expr_sem_rf f σ) ⤜ (λv. expr_sem (σ(x := v)) e)" (is "_ = ?M")
by (auto simp: expr_sem_rf_sound)
also have "(λσ. expr_sem σ e) ∘ (λ(σ,v). σ(x := v)) ∘ (λv. (σ,v)) ∈
measurable (stock_measure ((Γ(x := t')) x)) (subprob_algebra (stock_measure t))"
apply (intro measurable_comp, rule measurable_Pair1', rule assms)
apply (subst fun_upd_same, unfold state_measure_def)
apply (insert assms, auto intro!: measurable_expr_sem[unfolded state_measure_def] t1 t2
simp del: fun_upd_apply)
done
hence "(λv. expr_sem (σ(x := v)) e) ∈
measurable (stock_measure ((Γ(x := t')) x)) (subprob_algebra (stock_measure t))"
with assms have "?M = expr_sem (σ(x := expr_sem_rf f σ)) e"
unfolding return_val_def
by (intro bind_return) (auto simp: val_type_expr_sem_rf[OF t1]
type_universe_def simp del: type_universe_type)
also from assms t1 t2 have "... = expr_sem σ (e⟨f/x⟩)"
by (intro expr_subst_randomfree[symmetric]) auto
finally show ?thesis .
qed *)

end


# Theory PDF_Density_Contexts

(*
Theory: PDF_Density_Contexts.thy
Authors: Manuel Eberl
*)

section ‹Density Contexts›

theory PDF_Density_Contexts
imports PDF_Semantics
begin

lemma measurable_proj_state_measure[measurable (raw)]:
"i ∈ V ⟹ (λx. x i) ∈ measurable (state_measure V Γ) (Γ i)"
unfolding state_measure_def by measurable

lemma measurable_dens_ctxt_fun_upd[measurable (raw)]:
"f ∈ N →⇩M state_measure V' Γ ⟹ V = V' ∪ {x} ⟹
g ∈ N →⇩M stock_measure (Γ x) ⟹
(λω. (f ω)(x := g ω)) ∈ N →⇩M state_measure V Γ"
unfolding state_measure_def
by (rule measurable_fun_upd[where J=V']) auto

lemma measurable_case_nat_Suc_PiM:
"(λσ. σ ∘ Suc) ∈ measurable (PiM (Suc  A) (case_nat M N)) (PiM A N)"
proof-
have "(λσ. λx∈A. σ (Suc x)) ∈ measurable
(PiM (Suc  A) (case_nat M N)) (PiM A (λx. case_nat M N (Suc x)))" (is "?A")
by measurable
also have "?A ⟷ ?thesis"
by (force intro!: measurable_cong ext simp: state_measure_def space_PiM dest: PiE_mem)
finally show ?thesis .
qed

lemma measurable_case_nat_Suc:
"(λσ. σ ∘ Suc) ∈ measurable (state_measure (Suc  A) (case_nat t Γ)) (state_measure A Γ)"
proof-
have "(λσ. λx∈A. σ (Suc x)) ∈ measurable
(state_measure (Suc  A) (case_nat t Γ)) (state_measure A (λi. case_nat t Γ (Suc i)))" (is "?A")
unfolding state_measure_def by measurable
also have "?A ⟷ ?thesis"
by (force intro!: measurable_cong ext simp: state_measure_def space_PiM dest: PiE_mem)
finally show ?thesis .
qed

text ‹A density context holds a set of variables @{term V}, their types (using @{term Γ}), and a
common density function @{term δ} of the finite product space of all the variables in @{term V}.
@{term δ} takes a state @{term "σ ∈ (Π⇩E x∈V. type_universe (Γ x))"} and returns the common density
of these variables.›

type_synonym dens_ctxt = "vname set × vname set × (vname ⇒ pdf_type) × (state ⇒ ennreal)"
type_synonym expr_density = "state ⇒ val ⇒ ennreal"

definition empty_dens_ctxt :: dens_ctxt where
"empty_dens_ctxt = ({}, {}, λ_. undefined, λ_. 1)"

definition state_measure'
:: "vname set ⇒ vname set ⇒ (vname ⇒ pdf_type) ⇒ state ⇒ state measure" where
"state_measure' V V' Γ ρ =
distr (state_measure V Γ) (state_measure (V∪V') Γ) (λσ. merge V V' (σ, ρ))"

text ‹The marginal density of a variable @{term x} is obtained by integrating the common density
@{term δ} over all the remaining variables.›

definition marg_dens :: "dens_ctxt ⇒ vname ⇒ expr_density" where
"marg_dens = (λ(V,V',Γ,δ) x ρ v. ∫⇧+σ. δ (merge V V' (σ(x := v), ρ)) ∂state_measure (V-{x}) Γ)"

definition marg_dens2 :: "dens_ctxt ⇒ vname ⇒ vname ⇒ expr_density" where
"marg_dens2 ≡ (λ(V,V',Γ,δ) x y ρ v.
∫⇧+σ. δ (merge V V' (σ(x := fst (extract_pair v), y := snd (extract_pair v)), ρ))
∂state_measure (V-{x,y}) Γ)"

definition dens_ctxt_measure :: "dens_ctxt ⇒ state ⇒ state measure" where
"dens_ctxt_measure ≡ λ(V,V',Γ,δ) ρ. density (state_measure' V V' Γ ρ) δ"

definition branch_prob :: "dens_ctxt ⇒ state ⇒ ennreal" where
"branch_prob 𝒴 ρ = emeasure (dens_ctxt_measure 𝒴 ρ) (space (dens_ctxt_measure 𝒴 ρ))"

lemma dens_ctxt_measure_nonempty[simp]:
"space (dens_ctxt_measure 𝒴 ρ) ≠ {}"
unfolding dens_ctxt_measure_def state_measure'_def by (cases 𝒴) simp

lemma sets_dens_ctxt_measure_eq[measurable_cong]:
"sets (dens_ctxt_measure (V,V',Γ,δ) ρ) = sets (state_measure (V∪V') Γ)"

lemma measurable_dens_ctxt_measure_eq:
"measurable (dens_ctxt_measure (V,V',Γ,δ) ρ) = measurable (state_measure (V∪V') Γ)"
by (intro ext measurable_cong_sets)

lemma space_dens_ctxt_measure:
"space (dens_ctxt_measure (V,V',Γ,δ) ρ) = space (state_measure (V∪V') Γ)"
unfolding dens_ctxt_measure_def state_measure'_def by simp

definition apply_dist_to_dens :: "pdf_dist ⇒ (state ⇒ val ⇒ ennreal) ⇒ (state ⇒ val ⇒ ennreal)" where
"apply_dist_to_dens dst f = (λρ y. ∫⇧+x. f ρ x * dist_dens dst x y ∂stock_measure (dist_param_type dst))"

definition remove_var :: "state ⇒ state" where
"remove_var σ = (λx. σ (Suc x))"

lemma measurable_remove_var[measurable]:
"remove_var ∈ measurable (state_measure (shift_var_set V) (case_nat t Γ)) (state_measure V Γ)"
proof-
have "(λσ. λx∈V. σ (Suc x)) ∈ measurable
(state_measure (shift_var_set V) (case_nat t Γ)) (state_measure V (λx. case_nat t Γ (Suc x)))"
(is "?f ∈ ?M")
unfolding state_measure_def shift_var_set_def by measurable
also have "⋀x f. x ∉ V ⟹ f ∈ space (state_measure (shift_var_set V) (case_nat t Γ)) ⟹
f (Suc x) = undefined" unfolding state_measure_def
by (subst (asm) space_PiM, drule PiE_arb[of _ _ _ "Suc x" for x])
hence "?f ∈ ?M ⟷ remove_var ∈ ?M" unfolding remove_var_def[abs_def] state_measure_def
by (intro measurable_cong ext) (auto simp: space_PiM intro!: sym[of _ undefined])
finally show ?thesis by simp
qed

lemma measurable_case_nat_undefined[measurable]:
"case_nat undefined ∈ measurable (state_measure A Γ) (state_measure (SucA) (case_nat t Γ))" (is "_ ∈ ?M")
proof-
have "(λσ. λx∈SucA. case_nat undefined σ x) ∈ ?M" (is "?f ∈ _")
unfolding state_measure_def by (rule measurable_restrict) auto
also have "?f ∈ ?M ⟷ ?thesis"
by (intro measurable_cong ext)
(auto simp: state_measure_def space_PiM dest: PiE_mem split: nat.split)
finally show ?thesis .
qed

definition insert_dens
:: "vname set ⇒ vname set ⇒ expr_density ⇒ (state ⇒ ennreal) ⇒ state ⇒ ennreal" where
"insert_dens V V' f δ ≡ λσ. δ (remove_var σ) * f (remove_var σ) (σ 0)"

definition if_dens :: "(state ⇒ ennreal) ⇒ (state ⇒ val ⇒ ennreal) ⇒ bool ⇒ (state ⇒ ennreal)" where
"if_dens δ f b ≡ λσ. δ σ * f σ (BoolVal b)"

definition if_dens_det :: "(state ⇒ ennreal) ⇒ expr ⇒ bool ⇒ (state ⇒ ennreal)" where
"if_dens_det δ e b ≡ λσ. δ σ * (if expr_sem_rf σ e = BoolVal b then 1 else 0)"

lemma measurable_if_dens:
assumes [measurable]: "δ ∈ borel_measurable M"
assumes [measurable]: "case_prod f ∈ borel_measurable (M ⨂⇩M count_space (range BoolVal))"
shows "if_dens δ f b ∈ borel_measurable M"
unfolding if_dens_def by measurable

lemma measurable_if_dens_det:
assumes e: "Γ ⊢ e : BOOL" "randomfree e" "free_vars e ⊆ V"
assumes [measurable]: "δ ∈ borel_measurable (state_measure V Γ)"
shows "if_dens_det δ e b ∈ borel_measurable (state_measure V Γ)"
unfolding if_dens_det_def
proof (intro borel_measurable_times_ennreal assms measurable_If)
have "{x ∈ space (state_measure V Γ). expr_sem_rf x e = BoolVal b} =
(λσ. expr_sem_rf σ e) - {BoolVal b} ∩ space (state_measure V Γ)" by auto
also have "... ∈ sets (state_measure V Γ)"
by (rule measurable_sets, rule measurable_expr_sem_rf[OF e]) simp_all
finally show "{x ∈ space (state_measure V Γ). expr_sem_rf x e = BoolVal b}
∈ sets (state_measure V Γ)" .
qed simp_all

locale density_context =
fixes V V' Γ δ
assumes subprob_space_dens:
"⋀ρ. ρ ∈ space (state_measure V' Γ) ⟹ subprob_space (dens_ctxt_measure (V,V',Γ,δ) ρ)"
and finite_vars[simp]:     "finite V" "finite V'"
and measurable_dens[measurable]:
"δ ∈ borel_measurable (state_measure (V ∪ V') Γ)"
and disjoint:              "V ∩ V' = {}"
begin

abbreviation "𝒴 ≡ (V,V',Γ,δ)"

lemma branch_prob_altdef:
assumes ρ: "ρ ∈ space (state_measure V' Γ)"
shows "branch_prob 𝒴 ρ = ∫⇧+ x. δ (merge V V' (x, ρ)) ∂state_measure V Γ"
proof-
have "branch_prob 𝒴 ρ =
∫⇧+ x. δ (merge V V' (x, ρ)) * indicator (space (state_measure (V ∪ V') Γ))
(merge V V' (x, ρ)) ∂state_measure V Γ"
using ρ unfolding branch_prob_def[abs_def] dens_ctxt_measure_def state_measure'_def
by (simp add: emeasure_density ennreal_mult'' ennreal_indicator nn_integral_distr)
also from ρ have "... = ∫⇧+ x. δ (merge V V' (x, ρ)) ∂state_measure V Γ"
by (intro nn_integral_cong) (simp split: split_indicator add: merge_in_state_measure)
finally show ?thesis .
qed

lemma measurable_branch_prob[measurable]:
"branch_prob 𝒴 ∈ borel_measurable (state_measure V' Γ)"
proof-
interpret sigma_finite_measure "state_measure V Γ" by auto
show ?thesis
by (simp add: branch_prob_altdef cong: measurable_cong)
qed

lemma measurable_marg_dens':
assumes [simp]: "x ∈ V"
shows "case_prod (marg_dens 𝒴 x) ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure (Γ x))"
proof-
interpret sigma_finite_measure "state_measure (V - {x}) Γ"
unfolding state_measure_def
by (rule product_sigma_finite.sigma_finite, simp_all add: product_sigma_finite_def)
from assms have "V = insert x (V - {x})" by blast
hence A: "PiM V = PiM ..." by simp
show ?thesis unfolding marg_dens_def
qed

lemma insert_Diff: "insert x (A - B) = insert x A - (B - {x})"
by auto

lemma measurable_marg_dens2':
assumes "x ∈ V" "y ∈ V"
shows "case_prod (marg_dens2 𝒴 x y) ∈
borel_measurable (state_measure V' Γ ⨂⇩M stock_measure (PRODUCT (Γ x) (Γ y)))"
proof-
interpret sigma_finite_measure "state_measure (V - {x, y}) Γ"
unfolding state_measure_def
by (rule product_sigma_finite.sigma_finite, simp_all add: product_sigma_finite_def)
have [measurable]: "V = insert x (V - {x, y}) ∪ {y}"
using assms by blast
show ?thesis unfolding marg_dens2_def
by simp
qed

lemma measurable_marg_dens:
assumes "x ∈ V" "ρ ∈ space (state_measure V' Γ)"
shows "marg_dens 𝒴 x ρ ∈ borel_measurable (stock_measure (Γ x))"
using assms by (intro measurable_Pair_compose_split[OF measurable_marg_dens']) simp_all

lemma measurable_marg_dens2:
assumes "x ∈ V" "y ∈ V" "x ≠ y" "ρ ∈ space (state_measure V' Γ)"
shows "marg_dens2 𝒴 x y ρ ∈ borel_measurable (stock_measure (PRODUCT (Γ x) (Γ y)))"
using assms by (intro measurable_Pair_compose_split[OF measurable_marg_dens2']) simp_all

lemma measurable_state_measure_component:
"x ∈ V ⟹ (λσ. σ x) ∈ measurable (state_measure V Γ) (stock_measure (Γ x))"
unfolding state_measure_def
by (auto intro!: measurable_component_singleton)

lemma measurable_dens_ctxt_measure_component:
"x ∈ V ⟹ (λσ. σ x) ∈ measurable (dens_ctxt_measure (V,V',Γ,δ) ρ) (stock_measure (Γ x))"
unfolding dens_ctxt_measure_def state_measure'_def state_measure_def
by (auto intro!: measurable_component_singleton)

lemma space_dens_ctxt_measure_dens_ctxt_measure':
assumes "x ∈ V"
shows "space (state_measure V Γ) =
{σ(x := y) |σ y. σ ∈ space (state_measure (V-{x}) Γ) ∧ y ∈ type_universe (Γ x)}"
proof-
from assms have "insert x (V-{x}) = V" by auto
hence "state_measure V Γ = Pi⇩M (insert x (V-{x})) (λy. stock_measure (Γ y))"
unfolding state_measure_def by simp
also have "space ... = {σ(x := y) |σ y. σ ∈ space (state_measure (V-{x}) Γ) ∧ y ∈ type_universe (Γ x)}"
unfolding state_measure_def space_PiM PiE_insert_eq
by (simp add: image_def Bex_def) blast
finally show ?thesis .
qed

lemma state_measure_integral_split:
assumes "x ∈ A" "finite A"
assumes "f ∈ borel_measurable (state_measure A Γ)"
shows "(∫⇧+σ. f σ ∂state_measure A Γ) =
(∫⇧+y. ∫⇧+σ. f (σ(x := y)) ∂state_measure (A-{x}) Γ ∂stock_measure (Γ x))"
proof-
interpret product_sigma_finite "λy. stock_measure (Γ y)"
unfolding product_sigma_finite_def by auto
from assms have [simp]: "insert x A = A" by auto
have "(∫⇧+σ. f σ ∂state_measure A Γ) = (∫⇧+σ. f σ ∂Π⇩M v∈insert x (A-{x}). stock_measure (Γ v))"
unfolding state_measure_def by simp
also have "... = ∫⇧+y. ∫⇧+σ. f (σ(x := y)) ∂state_measure (A-{x}) Γ ∂stock_measure (Γ x)"
using assms unfolding state_measure_def
by (subst product_nn_integral_insert_rev) simp_all
finally show ?thesis .
qed

lemma fun_upd_in_state_measure:
"⟦σ ∈ space (state_measure A Γ); y ∈ space (stock_measure (Γ x))⟧
⟹ σ(x := y) ∈ space (state_measure (insert x A) Γ)"
unfolding state_measure_def by (auto simp: space_PiM split: if_split_asm)

lemma marg_dens_integral:
fixes X :: "val set" assumes "x ∈ V" and [measurable]: "X ∈ sets (stock_measure (Γ x))"
assumes "ρ`