Theory PDF_Compiler_Pred
section ‹Abstract PDF Compiler›
theory PDF_Compiler_Pred
imports PDF_Semantics PDF_Density_Contexts PDF_Transformations Density_Predicates
begin
subsection ‹Density compiler predicate›
text ‹
Predicate version of the probability density compiler that compiles a expression
to a probability density function of its distribution. The density is a HOL function of
type @{typ "val ⇒ ennreal"}.
›
inductive expr_has_density :: "dens_ctxt ⇒ expr ⇒ (state ⇒ val ⇒ ennreal) ⇒ bool"
("(1_ ⊢⇩d/ (_ ⇒/ _))" [50,0,50] 50) where
hd_AE: "⟦(V,V',Γ,δ) ⊢⇩d e ⇒ f; Γ ⊢ e : t;
⋀ρ. ρ ∈ space (state_measure V' Γ) ⟹
AE x in stock_measure t. f ρ x = f' ρ x;
case_prod f' ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t)⟧
⟹ (V,V',Γ,δ) ⊢⇩d e ⇒ f'"
| hd_dens_ctxt_cong:
"(V,V',Γ,δ) ⊢⇩d e ⇒ f ⟹ (⋀σ. σ ∈ space (state_measure (V ∪ V') Γ) ⟹ δ σ = δ' σ)
⟹ (V,V',Γ,δ') ⊢⇩d e ⇒ f"
| hd_val: "countable_type (val_type v) ⟹
(V,V',Γ,δ) ⊢⇩d Val v ⇒ (λρ x. branch_prob (V,V',Γ,δ) ρ * indicator {v} x)"
| hd_var: "x ∈ V ⟹ (V,V',Γ,δ) ⊢⇩d Var x ⇒ marg_dens (V,V',Γ,δ) x"
| hd_let: "⟦({},V∪V',Γ,λ_. 1) ⊢⇩d e1 ⇒ f;
(shift_var_set V,Suc`V',the(expr_type Γ e1) ⋅ Γ,insert_dens V V' f δ) ⊢⇩d e2 ⇒ g⟧
⟹ (V,V',Γ,δ) ⊢⇩d LetVar e1 e2 ⇒ (λρ. g (case_nat undefined ρ))"
| hd_rand: "(V,V',Γ,δ) ⊢⇩d e ⇒ f ⟹ (V,V',Γ,δ) ⊢⇩d Random dst e ⇒ apply_dist_to_dens dst f"
| hd_rand_det: "randomfree e ⟹ free_vars e ⊆ V' ⟹
(V,V',Γ,δ) ⊢⇩d Random dst e ⇒
(λρ x. branch_prob (V,V',Γ,δ) ρ * dist_dens dst (expr_sem_rf ρ e) x)"
| hd_fail: "(V,V',Γ,δ) ⊢⇩d Fail t ⇒ (λ_ _. 0)"
| hd_pair: "x ∈ V ⟹ y ∈ V ⟹ x ≠ y ⟹ (V,V',Γ,δ) ⊢⇩d <Var x, Var y> ⇒ marg_dens2 (V,V',Γ,δ) x y"
| hd_if: "⟦({},V∪V',Γ,λ_. 1) ⊢⇩d b ⇒ f;
(V,V',Γ,if_dens δ f True) ⊢⇩d e1 ⇒ g1; (V,V',Γ,if_dens δ f False) ⊢⇩d e2 ⇒ g2⟧
⟹ (V,V',Γ,δ) ⊢⇩d IF b THEN e1 ELSE e2 ⇒ (λρ x. g1 ρ x + g2 ρ x)"
| hd_if_det: "⟦randomfree b; (V,V',Γ,if_dens_det δ b True) ⊢⇩d e1 ⇒ g1;
(V,V',Γ,if_dens_det δ b False) ⊢⇩d e2 ⇒ g2⟧
⟹ (V,V',Γ,δ) ⊢⇩d IF b THEN e1 ELSE e2 ⇒ (λρ x. g1 ρ x + g2 ρ x)"
| hd_fst: "(V,V',Γ,δ) ⊢⇩d e ⇒ f ⟹
(V,V',Γ,δ) ⊢⇩d Fst $$ e ⇒
(λρ x. ∫⇧+y. f ρ <|x,y|> ∂stock_measure (the (expr_type Γ (Snd $$ e))))"
| hd_snd: "(V,V',Γ,δ) ⊢⇩d e ⇒ f ⟹
(V,V',Γ,δ) ⊢⇩d Snd $$ e ⇒
(λρ y. ∫⇧+x. f ρ <|x,y|> ∂stock_measure (the (expr_type Γ (Fst $$ e))))"
| hd_op_discr: "countable_type (the (expr_type Γ (oper $$ e))) ⟹ (V,V',Γ,δ) ⊢⇩d e ⇒ f ⟹
(V,V',Γ,δ) ⊢⇩d oper $$ e ⇒ (λρ y. ∫⇧+x. (if op_sem oper x = y then 1 else 0) * f ρ x
∂stock_measure (the (expr_type Γ e)))"
| hd_neg: "(V,V',Γ,δ) ⊢⇩d e ⇒ f ⟹
(V,V',Γ,δ) ⊢⇩d Minus $$ e ⇒ (λσ x. f σ (op_sem Minus x))"
| hd_addc: "(V,V',Γ,δ) ⊢⇩d e ⇒ f ⟹ randomfree e' ⟹ free_vars e' ⊆ V' ⟹
(V,V',Γ,δ) ⊢⇩d Add $$ <e, e'> ⇒
(λρ x. f ρ (op_sem Add <|x, expr_sem_rf ρ (Minus $$ e')|>))"
| hd_multc: "(V,V',Γ,δ) ⊢⇩d e ⇒ f ⟹ val_type c = REAL ⟹ c ≠ RealVal 0 ⟹
(V,V',Γ,δ) ⊢⇩d Mult $$ <e, Val c> ⇒
(λρ x. f ρ (op_sem Mult <|x, op_sem Inverse c|>) *
inverse (abs (extract_real c)))"
| hd_exp: "(V,V',Γ,δ) ⊢⇩d e ⇒ f ⟹
(V,V',Γ,δ) ⊢⇩d Exp $$ e ⇒
(λσ x. if extract_real x > 0 then
f σ (lift_RealVal safe_ln x) * inverse (extract_real x) else 0)"
| hd_inv: "(V,V',Γ,δ) ⊢⇩d e ⇒ f ⟹
(V,V',Γ,δ) ⊢⇩d Inverse $$ e ⇒ (λσ x. f σ (op_sem Inverse x) *
inverse (extract_real x) ^ 2)"
| hd_add: "(V,V',Γ,δ) ⊢⇩d e ⇒ f ⟹
(V,V',Γ,δ) ⊢⇩d Add $$ e ⇒ (λσ z. ∫⇧+x. f σ <|x, op_sem Add <|z, op_sem Minus x|>|>
∂stock_measure (val_type z))"
lemmas expr_has_density_intros =
hd_val hd_var hd_let hd_rand hd_rand_det hd_fail hd_pair hd_if hd_if_det
hd_fst hd_snd hd_op_discr hd_neg hd_addc hd_multc hd_exp hd_inv hd_add
subsection ‹Auxiliary lemmas›
lemma has_subprob_density_distr_Fst:
fixes t1 t2 f
defines "N ≡ stock_measure (PRODUCT t1 t2)"
defines "N' ≡ stock_measure t1"
defines "fst' ≡ op_sem Fst"
defines "f' ≡ λx. ∫⇧+y. f <|x,y|> ∂stock_measure t2"
assumes dens: "has_subprob_density M N f"
shows "has_subprob_density (distr M N' fst') N' f'"
proof (intro has_subprob_densityI measure_eqI)
from dens interpret subprob_space M by (rule has_subprob_densityD)
from dens have M_M: "measurable M = measurable N"
by (intro ext measurable_cong_sets) (auto dest: has_subprob_densityD)
hence meas_fst: "fst' ∈ measurable M N'" unfolding fst'_def
by (subst op_sem.simps) (simp add: N'_def N_def M_M)
thus "subprob_space (distr M N' fst')"
by (rule subprob_space_distr) (simp_all add: N'_def)
interpret sigma_finite_measure "stock_measure t2" by simp
have f[measurable]: "f ∈ borel_measurable (stock_measure (PRODUCT t1 t2))"
using dens by (auto simp: has_subprob_density_def has_density_def N_def)
then show meas_f': "f' ∈ borel_measurable N'" unfolding f'_def N'_def
by measurable
let ?M1 = "distr M N' fst'" and ?M2 = "density N' f'"
show "sets ?M1 = sets ?M2" by simp
fix X assume "X ∈ sets ?M1"
hence X: "X ∈ sets N'" "X ∈ sets N'" by (simp_all add: N'_def)
then have [measurable]: "X ∈ sets (stock_measure t1)"
by (simp add: N'_def)
from meas_fst and X(1) have "emeasure ?M1 X = emeasure M (fst' -` X ∩ space M)"
by (rule emeasure_distr)
also from dens have M: "M = density N f" by (rule has_subprob_densityD)
from this and meas_fst have meas_fst': "fst' ∈ measurable N N'" by simp
with dens and X have "emeasure M (fst' -` X ∩ space M) =
∫⇧+x. f x * indicator (fst' -` X ∩ space N) x ∂N"
by (subst (1 2) M, subst space_density, subst emeasure_density)
(erule has_subprob_densityD, erule measurable_sets, simp, simp)
also have "N = distr (N' ⨂⇩M stock_measure t2) N (case_prod PairVal)" (is "_ = ?N")
unfolding N_def N'_def stock_measure.simps by (rule embed_measure_eq_distr) (simp add: inj_PairVal)
hence "⋀f. nn_integral N f = nn_integral ... f" by simp
also from dens and X
have "(∫⇧+x. f x * indicator (fst' -` X ∩ space N) x ∂?N) =
∫⇧+x. f (case_prod PairVal x) * indicator (fst' -` X ∩ space N) (case_prod PairVal x)
∂(N' ⨂⇩M stock_measure t2)"
by (intro nn_integral_distr)
(simp_all add: measurable_embed_measure2 N_def N'_def fst'_def)
also from has_subprob_densityD(1)[OF dens] and X
have "... = ∫⇧+x. ∫⇧+y. f <|x,y|> * indicator (fst' -` X ∩ space N) <|x, y|> ∂stock_measure t2 ∂N'"
(is "_ = ?I")
by (subst sigma_finite_measure.nn_integral_fst[symmetric])
(auto simp: N_def N'_def fst'_def comp_def simp del: space_stock_measure)
also from X have A: "⋀x y. x ∈ space N' ⟹ y ∈ space (stock_measure t2) ⟹
indicator (fst' -` X ∩ space N) <|x, y|> = indicator X x"
by (auto split: split_indicator simp: fst'_def N_def
space_embed_measure space_pair_measure N'_def)
have "?I = ∫⇧+x. ∫⇧+y. f <|x,y|> * indicator X x ∂stock_measure t2 ∂N'" (is "_ = ?I")
by (intro nn_integral_cong) (simp add: A)
also have A: "⋀x. x ∈ space N' ⟹ (λy. f <|x,y|>) = f ∘ case_prod PairVal ∘ (λy. (x,y))"
by (intro ext) simp
from dens have "?I = ∫⇧+x. (∫⇧+y. f <|x,y|> ∂stock_measure t2) * indicator X x ∂N'"
by (intro nn_integral_cong nn_integral_multc, subst A)
(auto intro!: measurable_comp f measurable_PairVal simp: N'_def)
also from meas_f' and X(2) have "... = emeasure ?M2 X" unfolding f'_def
by (rule emeasure_density[symmetric])
finally show "emeasure ?M1 X = emeasure ?M2 X" .
qed
lemma has_subprob_density_distr_Snd:
fixes t1 t2 f
defines "N ≡ stock_measure (PRODUCT t1 t2)"
defines "N' ≡ stock_measure t2"
defines "snd' ≡ op_sem Snd"
defines "f' ≡ λy. ∫⇧+x. f <|x,y|> ∂stock_measure t1"
assumes dens: "has_subprob_density M N f"
shows "has_subprob_density (distr M N' snd') N' f'"
proof (intro has_subprob_densityI measure_eqI)
from dens interpret subprob_space M by (rule has_subprob_densityD)
from dens have M_M: "measurable M = measurable N"
by (intro ext measurable_cong_sets) (auto dest: has_subprob_densityD)
hence meas_snd: "snd' ∈ measurable M N'" unfolding snd'_def
by (subst op_sem.simps) (simp add: N'_def N_def M_M)
thus "subprob_space (distr M N' snd')"
by (rule subprob_space_distr) (simp_all add: N'_def)
interpret t1: sigma_finite_measure "stock_measure t1" by simp
have A: "(λ(x, y). f <| x , y |>) = f ∘ case_prod PairVal"
by (intro ext) (simp add: o_def split: prod.split)
have f[measurable]: "f ∈ borel_measurable (stock_measure (PRODUCT t1 t2))"
using dens by (auto simp: has_subprob_density_def has_density_def N_def)
then show meas_f': "f' ∈ borel_measurable N'" unfolding f'_def N'_def
by measurable
interpret N': sigma_finite_measure N'
unfolding N'_def by (rule sigma_finite_stock_measure)
interpret N'_t1: pair_sigma_finite t1 N' proof qed
let ?M1 = "distr M N' snd'" and ?M2 = "density N' f'"
show "sets ?M1 = sets ?M2" by simp
fix X assume "X ∈ sets ?M1"
hence X: "X ∈ sets N'" "X ∈ sets N'" by (simp_all add: N'_def)
then have [measurable]: "X ∈ sets (stock_measure t2)"
by (simp add: N'_def)
from meas_snd and X(1) have "emeasure ?M1 X = emeasure M (snd' -` X ∩ space M)"
by (rule emeasure_distr)
also from dens have M: "M = density N f" by (rule has_subprob_densityD)
from this and meas_snd have meas_snd': "snd' ∈ measurable N N'" by simp
with dens and X have "emeasure M (snd' -` X ∩ space M) =
∫⇧+x. f x * indicator (snd' -` X ∩ space N) x ∂N"
by (subst (1 2) M, subst space_density, subst emeasure_density)
(erule has_subprob_densityD, erule measurable_sets, simp, simp)
also have "N = distr (stock_measure t1 ⨂⇩M N') N (case_prod PairVal)" (is "_ = ?N")
unfolding N_def N'_def stock_measure.simps by (rule embed_measure_eq_distr) (simp add: inj_PairVal)
hence "⋀f. nn_integral N f = nn_integral ... f" by simp
also from dens and X
have "(∫⇧+x. f x * indicator (snd' -` X ∩ space N) x ∂?N) =
∫⇧+x. f (case_prod PairVal x) * indicator (snd' -` X ∩ space N) (case_prod PairVal x)
∂(stock_measure t1 ⨂⇩M N')"
by (intro nn_integral_distr)
(simp_all add: measurable_embed_measure2 N_def N'_def snd'_def)
also from has_subprob_densityD(1)[OF dens] and X
have "... = ∫⇧+y. ∫⇧+x. f <|x,y|> * indicator (snd' -` X ∩ space N) <|x, y|> ∂stock_measure t1 ∂N'"
(is "… = ?I")
by (subst N'_t1.nn_integral_snd[symmetric])
(auto simp: N_def N'_def snd'_def comp_def simp del: space_stock_measure)
also from X have A: "⋀x y. x ∈ space N' ⟹ y ∈ space (stock_measure t1) ⟹
indicator (snd' -` X ∩ space N) <|y, x|> = indicator X x"
by (auto split: split_indicator simp: snd'_def N_def
space_embed_measure space_pair_measure N'_def)
have "?I = ∫⇧+y. ∫⇧+x. f <|x,y|> * indicator X y ∂stock_measure t1 ∂N'" (is "_ = ?I")
by (intro nn_integral_cong) (simp add: A)
also have A: "⋀y. y ∈ space N' ⟹ (λx. f <|x,y|>) = f ∘ case_prod PairVal ∘ (λx. (x,y))"
by (intro ext) simp
from dens have "?I = ∫⇧+y. (∫⇧+x. f <|x,y|> ∂stock_measure t1) * indicator X y ∂N'"
by (intro nn_integral_cong nn_integral_multc) (auto simp: N'_def)
also from meas_f' and X(2) have "... = emeasure ?M2 X" unfolding f'_def
by (rule emeasure_density[symmetric])
finally show "emeasure ?M1 X = emeasure ?M2 X" .
qed
lemma dens_ctxt_measure_empty_bind:
assumes "ρ ∈ space (state_measure V' Γ)"
assumes f[measurable]: "f ∈ measurable (state_measure V' Γ) (subprob_algebra N)"
shows "dens_ctxt_measure ({},V',Γ,λ_. 1) ρ ⤜ f = f ρ" (is "bind ?M _ = ?R")
proof (intro measure_eqI)
from assms have nonempty: "space ?M ≠ {}"
by (auto simp: dens_ctxt_measure_def state_measure'_def state_measure_def space_PiM)
moreover have meas: "measurable ?M = measurable (state_measure V' Γ)"
by (intro ext measurable_cong_sets) (auto simp: dens_ctxt_measure_def state_measure'_def)
moreover from assms have [simp]: "sets (f ρ) = sets N"
by (intro sets_kernel[OF assms(2)])
ultimately show sets_eq: "sets (?M ⤜ f) = sets ?R" using assms
by (subst sets_bind[OF sets_kernel[OF f]])
(simp_all add: dens_ctxt_measure_def state_measure'_def state_measure_def)
from assms have [simp]: "⋀σ. merge {} V' (σ,ρ) = ρ"
by (intro ext) (auto simp: merge_def state_measure_def space_PiM)
fix X assume X: "X ∈ sets (?M ⤜ f)"
hence "emeasure (?M ⤜ f) X = ∫⇧+x. emeasure (f x) X ∂?M" using assms
by (subst emeasure_bind[OF nonempty]) (simp_all add: nonempty meas sets_eq cong: measurable_cong_sets)
also have "... = ∫⇧+(x::state). emeasure (f ρ) X ∂count_space {λ_. undefined}"
unfolding dens_ctxt_measure_def state_measure'_def state_measure_def using X assms
apply (simp only: prod.case)
apply (subst nn_integral_density)
apply (auto intro!: measurable_compose[OF _ measurable_emeasure_subprob_algebra]
simp: state_measure_def sets_eq PiM_empty) [3]
apply (subst nn_integral_distr)
apply (auto intro!: measurable_compose[OF _ measurable_emeasure_subprob_algebra]
simp: state_measure_def sets_eq PiM_empty)
done
also have "... = emeasure (f ρ) X"
by (subst nn_integral_count_space_finite) (simp_all add: max_def)
finally show "emeasure (?M ⤜ f) X = emeasure (f ρ) X" .
qed
lemma (in density_context) bind_dens_ctxt_measure_cong:
assumes fg: "⋀σ. (⋀x. x ∈ V' ⟹ σ x = ρ x) ⟹ f σ = g σ"
assumes ρ[measurable]: "ρ ∈ space (state_measure V' Γ)"
assumes Mf[measurable]: "f ∈ measurable (state_measure (V ∪ V') Γ) (subprob_algebra N)"
assumes Mg[measurable]: "g ∈ measurable (state_measure (V ∪ V') Γ) (subprob_algebra N)"
defines "M ≡ dens_ctxt_measure (V,V',Γ,δ) ρ"
shows "M ⤜ f = M ⤜ g"
proof -
have [measurable]: "(λσ. merge V V' (σ, ρ)) ∈ measurable (state_measure V Γ) (state_measure (V ∪ V') Γ)"
using ρ unfolding state_measure_def by simp
show ?thesis
using disjoint
apply (simp add: M_def dens_ctxt_measure_def state_measure'_def density_distr)
apply (subst (1 2) bind_distr)
apply measurable
apply (intro bind_cong_AE[where B=N] AE_I2 refl fg)
apply measurable
done
qed
lemma (in density_context) bin_op_randomfree_restructure:
assumes t1: "Γ ⊢ e : t" and t2: "Γ ⊢ e' : t'" and t3: "op_type oper (PRODUCT t t') = Some tr"
assumes rf: "randomfree e'" and vars1: "free_vars e ⊆ V∪V'" and vars2: "free_vars e' ⊆ V'"
assumes ρ: "ρ ∈ space (state_measure V' Γ)"
defines "M ≡ dens_ctxt_measure (V,V',Γ,δ) ρ"
defines "v ≡ expr_sem_rf ρ e'"
shows "M ⤜ (λσ. expr_sem σ (oper $$ <e, e'>)) =
distr (M ⤜ (λσ. expr_sem σ e)) (stock_measure tr) (λw. op_sem oper <|w,v|>)"
proof-
from assms have vars1': "⋀σ. σ ∈ space M ⟹ ∀x∈free_vars e. val_type (σ x) = Γ x"
and vars2': "⋀σ. σ ∈ space M ⟹ ∀x∈free_vars e'. val_type (σ x) = Γ x"
by (auto simp: M_def space_dens_ctxt_measure state_measure_def space_PiM
dest: PiE_mem)
have Me: "(λσ. expr_sem σ e) ∈
measurable (state_measure (V ∪ V') Γ) (subprob_algebra (stock_measure t))"
by (rule measurable_expr_sem[OF t1 vars1])
from assms have e': "⋀σ. σ ∈ space M ⟹ expr_sem σ e' = return_val (expr_sem_rf σ e')"
by (intro expr_sem_rf_sound[symmetric]) (auto simp: M_def space_dens_ctxt_measure)
from assms have vt_e': "⋀σ. σ ∈ space M ⟹ val_type (expr_sem_rf σ e') = t'"
by (intro val_type_expr_sem_rf) (auto simp: M_def space_dens_ctxt_measure)
let ?tt' = "PRODUCT t t'"
{
fix σ assume σ: "σ ∈ space M"
with vars2 have [simp]: "measurable (expr_sem σ e') = measurable (stock_measure t')"
by (intro measurable_expr_sem_eq[OF t2, of _ "V∪V'"]) (auto simp: M_def space_dens_ctxt_measure)
from σ have [simp]: "space (expr_sem σ e) = space (stock_measure t)"
"space (expr_sem σ e') = space (stock_measure t')"
using space_expr_sem[OF t1 vars1'[OF σ]] space_expr_sem[OF t2 vars2'[OF σ]] by simp_all
have "expr_sem σ e ⤜ (λx. expr_sem σ e' ⤜ (λy. return_val <| x , y |>)) =
expr_sem σ e ⤜ (λx. return_val (expr_sem_rf σ e') ⤜ (λy. return_val <| x , y |>))"
by (intro bind_cong refl, subst e'[OF σ]) simp
also have "... = expr_sem σ e ⤜ (λx. return_val <|x , expr_sem_rf σ e'|>)" using σ vars2
by (intro bind_cong refl, subst bind_return_val'[of _ t' _ ?tt'])
(auto simp: vt_e' M_def space_dens_ctxt_measure
intro!: measurable_PairVal)
finally have "expr_sem σ e ⤜ (λx. expr_sem σ e' ⤜ (λy. return_val <|x,y|>)) =
expr_sem σ e ⤜ (λx. return_val <|x, expr_sem_rf σ e'|>)" .
}
hence "M ⤜ (λσ. expr_sem σ (oper $$ <e, e'>)) =
M ⤜ (λσ. (expr_sem σ e ⤜ (λx. return_val <|x, expr_sem_rf σ e'|>))
⤜ (λx. return_val (op_sem oper x)))" (is "_ = ?T")
by (intro bind_cong refl) (simp only: expr_sem.simps)
also have [measurable]: "⋀σ. σ ∈ space M ⟹ expr_sem_rf σ e' ∈ space t'"
by (simp add: type_universe_def vt_e' del: type_universe_type)
note [measurable] = measurable_op_sem[OF t3]
hence "?T = M ⤜ (λσ. expr_sem σ e ⤜ (λx. return_val (op_sem oper <|x, expr_sem_rf σ e'|>)))"
(is "_ = ?T")
by (intro bind_cong[OF refl], subst bind_assoc_return_val[of _ t _ ?tt' _ tr])
(auto simp: sets_expr_sem[OF t1 vars1'])
also have eq: "⋀σ. (⋀x. x ∈ V' ⟹ σ x = ρ x) ⟹ expr_sem_rf σ e' = expr_sem_rf ρ e'"
using vars2 by (intro expr_sem_rf_eq_on_vars) auto
have [measurable]: "(λσ. expr_sem_rf σ e') ∈ measurable (state_measure (V ∪ V') Γ) (stock_measure t')"
using vars2 by (intro measurable_expr_sem_rf[OF t2 rf]) blast
note [measurable] = Me measurable_bind measurable_return_val
have expr_sem_rf_space: "expr_sem_rf ρ e' ∈ space (stock_measure t')"
using val_type_expr_sem_rf[OF t2 rf vars2 ρ]
by (simp add: type_universe_def del: type_universe_type)
hence "?T = M ⤜ (λσ. expr_sem σ e ⤜ (λx. return_val (op_sem oper <|x, expr_sem_rf ρ e'|>)))"
using ρ unfolding M_def
by (intro bind_dens_ctxt_measure_cong, subst eq) (simp, simp, simp, measurable)
also have "... = (M ⤜ (λσ. expr_sem σ e)) ⤜
return_val ∘ (λx. op_sem oper <|x, expr_sem_rf ρ e'|>)"
using expr_sem_rf_space
by (subst bind_assoc[of _ _ "stock_measure t" _ "stock_measure tr", symmetric])
(simp_all add: M_def measurable_dens_ctxt_measure_eq o_def)
also have "... = distr (M ⤜ (λσ. expr_sem σ e)) (stock_measure tr)
(λx. op_sem oper <|x, expr_sem_rf ρ e'|>)" using Me expr_sem_rf_space
by (subst bind_return_val_distr[of _ t _ tr])
(simp_all add: M_def sets_expr_sem[OF t1 vars1'])
finally show ?thesis unfolding v_def .
qed
lemma addc_density_measurable:
assumes Mf: "case_prod f ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t)"
assumes t_disj: "t = REAL ∨ t = INTEG" and t: "Γ ⊢ e' : t"
assumes rf: "randomfree e'" and vars: "free_vars e' ⊆ V'"
defines "f' ≡ (λρ x. f ρ (op_sem Add <|x, expr_sem_rf ρ (Minus $$ e')|>))"
shows "case_prod f' ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t)"
proof (insert t_disj, elim disjE)
assume A: "t = REAL"
from A and t have t': "Γ ⊢ e' : REAL" by simp
with rf vars have vt_e':
"⋀ρ. ρ ∈ space (state_measure V' Γ) ⟹ val_type (expr_sem_rf ρ e') = REAL"
by (intro val_type_expr_sem_rf) simp_all
let ?f' = "λσ x. let c = expr_sem_rf σ e'
in f σ (RealVal (extract_real x - extract_real c))"
note Mf[unfolded A, measurable] and rf[measurable] and vars[measurable] and t[unfolded A, measurable]
have "case_prod ?f' ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t)"
unfolding Let_def A by measurable
also have "case_prod ?f' ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t) ⟷
case_prod f' ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t)"
by (intro measurable_cong)
(auto simp: Let_def space_pair_measure A space_embed_measure f'_def lift_RealIntVal2_def
lift_RealIntVal_def extract_real_def
dest!: vt_e' split: val.split)
finally show ?thesis .
next
assume A: "t = INTEG"
with t have t': "Γ ⊢ e' : INTEG" by simp
with rf vars have vt_e':
"⋀ρ. ρ ∈ space (state_measure V' Γ) ⟹ val_type (expr_sem_rf ρ e') = INTEG"
by (intro val_type_expr_sem_rf) simp_all
let ?f' = "λσ x. let c = expr_sem_rf σ e'
in f σ (IntVal (extract_int x - extract_int c))"
note Mf[unfolded A, measurable] and rf[measurable] and vars[measurable] and t[unfolded A, measurable]
have Mdiff: "case_prod ((-) :: int ⇒ _) ∈
measurable (count_space UNIV ⨂⇩M count_space UNIV) (count_space UNIV)" by simp
have "case_prod ?f' ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t)"
unfolding Let_def A by measurable
also have "case_prod ?f' ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t) ⟷
case_prod f' ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t)"
by (intro measurable_cong)
(auto simp: Let_def space_pair_measure A space_embed_measure f'_def lift_RealIntVal2_def
lift_RealIntVal_def extract_int_def
dest!: vt_e' split: val.split)
finally show ?thesis .
qed
lemma (in density_context) emeasure_bind_if_dens_ctxt_measure:
assumes ρ: "ρ ∈ space (state_measure V' Γ)"
defines "M ≡ dens_ctxt_measure 𝒴 ρ"
assumes Mf[measurable]: "f ∈ measurable M (subprob_algebra (stock_measure BOOL))"
assumes Mg[measurable]: "g ∈ measurable M (subprob_algebra R)"
assumes Mh[measurable]: "h ∈ measurable M (subprob_algebra R)"
assumes densf: "has_parametrized_subprob_density (state_measure (V ∪ V') Γ)
f (stock_measure BOOL) δf"
assumes densg: "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. dens_ctxt_measure (V,V',Γ,λσ. δ σ * δf σ (BoolVal True)) ρ ⤜ g) R δg"
assumes densh: "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. dens_ctxt_measure (V,V',Γ,λσ. δ σ * δf σ (BoolVal False)) ρ ⤜ h) R δh"
defines "P ≡ λb. b = BoolVal True"
shows "M ⤜ (λx. f x ⤜ (λb. if P b then g x else h x)) = density R (λx. δg ρ x + δh ρ x)"
(is "?lhs = ?rhs")
proof (intro measure_eqI)
have sets_lhs: "sets ?lhs = sets R"
apply (subst sets_bind_measurable[of _ _ R])
apply measurable
apply (simp_all add: P_def M_def)
done
thus "sets ?lhs = sets ?rhs" by simp
fix X assume "X ∈ sets ?lhs"
hence X: "X ∈ sets R" by (simp only: sets_lhs)
from Mf have [simp]: "⋀x. x ∈ space M ⟹ sets (f x) = sets (stock_measure BOOL)"
by (rule sets_kernel)
note [simp] = sets_eq_imp_space_eq[OF this]
from has_parametrized_subprob_densityD(3)[OF densf]
have Mδf[measurable]: "(λ(x, y). δf x y)
∈ borel_measurable (state_measure (V ∪ V') Γ ⨂⇩M stock_measure BOOL)"
by (simp add: M_def dens_ctxt_measure_def state_measure'_def)
have [measurable]: "Measurable.pred (stock_measure BOOL) P"
unfolding P_def by simp
have BoolVal_in_space: "BoolVal True ∈ space (stock_measure BOOL)"
"BoolVal False ∈ space (stock_measure BOOL)" by auto
from Mg have Mg'[measurable]: "g ∈ measurable (state_measure (V ∪ V') Γ) (subprob_algebra R)"
by (simp add: M_def measurable_dens_ctxt_measure_eq)
from Mh have Mh'[measurable]: "h ∈ measurable (state_measure (V ∪ V') Γ) (subprob_algebra R)"
by (simp add: M_def measurable_dens_ctxt_measure_eq)
from densf have densf': "has_parametrized_subprob_density M f (stock_measure BOOL) δf"
unfolding has_parametrized_subprob_density_def
apply (subst measurable_cong_sets, subst sets_pair_measure_cong)
apply (unfold M_def dens_ctxt_measure_def state_measure'_def, (subst prod.case)+) []
apply (subst sets_density, subst sets_distr, rule refl, rule refl, rule refl, rule refl)
apply (auto simp: M_def space_dens_ctxt_measure)
done
interpret dc_True: density_context V V' Γ "λσ. δ σ * δf σ (BoolVal True)"
using density_context_if_dens[of _ δf True] densf unfolding if_dens_def by (simp add: stock_measure.simps)
interpret dc_False: density_context V V' Γ "λσ. δ σ * δf σ (BoolVal False)"
using density_context_if_dens[of _ δf False] densf unfolding if_dens_def by (simp add: stock_measure.simps)
have "emeasure (M ⤜ (λx. f x ⤜ (λb. if P b then g x else h x))) X =
∫⇧+x. emeasure (f x ⤜ (λb. if P b then g x else h x)) X ∂M" using X
by (subst emeasure_bind[of _ _ R], simp add: M_def, intro measurable_bind[OF Mf], measurable)
also have "... = ∫⇧+x. ∫⇧+b. emeasure (if P b then g x else h x) X ∂f x ∂M"
by (intro nn_integral_cong) (simp_all add: X emeasure_bind[where N=R])
also have "... = ∫⇧+x. ∫⇧+b. emeasure (if P b then g x else h x) X * δf x b ∂stock_measure BOOL ∂M"
using has_parametrized_subprob_densityD[OF densf]
by (intro nn_integral_cong)
(simp_all add: AE_count_space field_simps nn_integral_density
M_def space_dens_ctxt_measure stock_measure.simps)
also have "... = ∫⇧+x. emeasure (g x) X * δf x (BoolVal True) +
emeasure (h x) X * δf x (BoolVal False) ∂M"
using has_parametrized_subprob_densityD[OF densf']
by (intro nn_integral_cong, subst nn_integral_BoolVal)
(auto simp: P_def nn_integral_BoolVal)
also have "... = (∫⇧+x. emeasure (g x) X * δf x (BoolVal True) ∂M) +
(∫⇧+x. emeasure (h x) X * δf x (BoolVal False) ∂M)" using X
using has_parametrized_subprob_densityD[OF densf'] BoolVal_in_space
by (intro nn_integral_add) (auto simp:)
also have "(∫⇧+x. emeasure (g x) X * δf x (BoolVal True) ∂M) =
∫⇧+x. δ (merge V V' (x, ρ)) * δf (merge V V' (x, ρ)) (BoolVal True) *
(emeasure (g (merge V V' (x, ρ)))) X ∂state_measure V Γ"
using X has_parametrized_subprob_densityD[OF densf] BoolVal_in_space unfolding M_def
by (subst nn_integral_dens_ctxt_measure) (simp_all add: ρ mult_ac)
also have "... = emeasure (density R (δg ρ)) X" using ρ X
apply (subst dc_True.nn_integral_dens_ctxt_measure[symmetric], simp_all) []
apply (subst emeasure_bind[of _ _ R, symmetric], simp_all add: measurable_dens_ctxt_measure_eq) []
apply (subst has_parametrized_subprob_densityD(1)[OF densg], simp_all)
done
also have "(∫⇧+x. emeasure (h x) X * δf x (BoolVal False) ∂M) =
∫⇧+x. δ (merge V V' (x, ρ)) * δf (merge V V' (x, ρ)) (BoolVal False) *
(emeasure (h (merge V V' (x, ρ)))) X ∂state_measure V Γ"
using X has_parametrized_subprob_densityD[OF densf] BoolVal_in_space unfolding M_def
by (subst nn_integral_dens_ctxt_measure) (simp_all add: ρ mult_ac)
also have "... = emeasure (density R (δh ρ)) X" using ρ X
apply (subst dc_False.nn_integral_dens_ctxt_measure[symmetric], simp_all) []
apply (subst emeasure_bind[of _ _ R, symmetric], simp_all add: measurable_dens_ctxt_measure_eq) []
apply (subst has_parametrized_subprob_densityD(1)[OF densh], simp_all)
done
also have "emeasure (density R (δg ρ)) X + emeasure (density R (δh ρ)) X =
emeasure (density R (λx. δg ρ x + δh ρ x)) X" using X ρ
using has_parametrized_subprob_densityD(2,3)[OF densg]
has_parametrized_subprob_densityD(2,3)[OF densh]
by (intro emeasure_density_add) simp_all
finally show "emeasure ?lhs X = emeasure ?rhs X" .
qed
lemma (in density_context) emeasure_bind_if_det_dens_ctxt_measure:
fixes f
assumes ρ: "ρ ∈ space (state_measure V' Γ)"
defines "M ≡ dens_ctxt_measure 𝒴 ρ"
defines "P ≡ λb. f b = BoolVal True" and "P' ≡ λb. f b = BoolVal False"
assumes dc1: "density_context V V' Γ (λσ. δ σ * (if P σ then 1 else 0))"
assumes dc2: "density_context V V' Γ (λσ. δ σ * (if P' σ then 1 else 0))"
assumes Mf[measurable]: "f ∈ measurable M (stock_measure BOOL)"
assumes Mg[measurable]: "g ∈ measurable M (subprob_algebra R)"
assumes Mh[measurable]: "h ∈ measurable M (subprob_algebra R)"
assumes densg: "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. dens_ctxt_measure (V,V',Γ,λσ. δ σ * (if P σ then 1 else 0)) ρ ⤜ g) R δg"
assumes densh: "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. dens_ctxt_measure (V,V',Γ,λσ. δ σ * (if P' σ then 1 else 0)) ρ ⤜ h) R δh"
shows "M ⤜ (λx. if P x then g x else h x) = density R (λx. δg ρ x + δh ρ x)"
(is "?lhs = ?rhs")
proof (intro measure_eqI)
have [measurable]: "Measurable.pred M P"
unfolding P_def by (rule pred_eq_const1[OF Mf]) simp
have [measurable]: "Measurable.pred M P'"
unfolding P'_def by (rule pred_eq_const1[OF Mf]) simp
have sets_lhs: "sets ?lhs = sets R"
by (subst sets_bind_measurable[of _ _ R]) (simp_all, simp add: M_def)
thus "sets ?lhs = sets ?rhs" by simp
from Mg have Mg'[measurable]: "g ∈ measurable (state_measure (V ∪ V') Γ) (subprob_algebra R)"
by (simp add: M_def measurable_dens_ctxt_measure_eq)
from Mh have Mh'[measurable]: "h ∈ measurable (state_measure (V ∪ V') Γ) (subprob_algebra R)"
by (simp add: M_def measurable_dens_ctxt_measure_eq)
have [simp]: "⋀x. x ∈ space M ⟹ sets (g x) = sets R"
by (rule sets_kernel[OF Mg])
have [simp]: "⋀x. x ∈ space M ⟹ sets (h x) = sets R"
by (rule sets_kernel[OF Mh])
have [simp]: "sets M = sets (state_measure (V ∪ V') Γ)"
by (simp add: M_def dens_ctxt_measure_def state_measure'_def)
then have [measurable_cong]: "sets (state_measure (V ∪ V') Γ) = sets M" ..
have [simp]: "range BoolVal = {BoolVal True, BoolVal False}" by auto
fix X assume "X ∈ sets ?lhs"
hence X[measurable]: "X ∈ sets R" by (simp only: sets_lhs)
interpret dc_True: density_context V V' Γ "λσ. δ σ * (if P σ then 1 else 0)" by fact
interpret dc_False: density_context V V' Γ "λσ. δ σ * (if P' σ then 1 else 0)" by fact
have "emeasure (M ⤜ (λx. if P x then g x else h x)) X =
∫⇧+x. (if P x then emeasure (g x) X else emeasure (h x) X) ∂M" using X
by (subst emeasure_bind[of _ _ R], simp add: M_def, measurable)
(intro nn_integral_cong, simp)
also have "... = ∫⇧+x. (if P x then 1 else 0) * emeasure (g x) X +
(if P' x then 1 else 0) * emeasure (h x) X ∂M" using X
using measurable_space[OF Mf]
by (intro nn_integral_cong) (auto simp add: P_def P'_def stock_measure.simps)
also have "... = (∫⇧+x. (if P x then 1 else 0) * emeasure (g x) X ∂M) +
(∫⇧+x. (if P' x then 1 else 0) * emeasure (h x) X ∂M)" using X
by (intro nn_integral_add) (simp_all add:)
also have "... = (∫⇧+ y. δg ρ y * indicator X y ∂R) + (∫⇧+ y. δh ρ y * indicator X y ∂R)"
unfolding M_def using ρ X
apply (simp add: nn_integral_dens_ctxt_measure)
apply (subst (1 2) mult.assoc[symmetric])
apply (subst dc_True.nn_integral_dens_ctxt_measure[symmetric], simp, simp)
apply (subst dc_False.nn_integral_dens_ctxt_measure[symmetric], simp, simp)
apply (subst (1 2) emeasure_bind[symmetric], simp_all add: measurable_dens_ctxt_measure_eq)
apply measurable
apply (subst emeasure_has_parametrized_subprob_density[OF densg], simp, simp)
apply (subst emeasure_has_parametrized_subprob_density[OF densh], simp_all)
done
also have "... = emeasure (density R (λx. δg ρ x + δh ρ x)) X" using X ρ
using has_parametrized_subprob_densityD(2,3)[OF densg]
using has_parametrized_subprob_densityD(2,3)[OF densh]
apply (subst (1 2) emeasure_density[symmetric], simp_all) []
apply (intro emeasure_density_add, simp_all)
done
finally show "emeasure ?lhs X = emeasure ?rhs X" .
qed
subsection ‹Soundness proof›
lemma restrict_state_measure[measurable]:
"(λx. restrict x V') ∈ measurable (state_measure (V ∪ V') Γ) (state_measure V' Γ)"
by (simp add: state_measure_def)
lemma expr_has_density_sound_op:
assumes dens_ctxt: "density_context V V' Γ δ"
assumes dens: "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. dens_ctxt_measure (V,V',Γ,δ) ρ ⤜ (λσ. expr_sem σ e)) (stock_measure t) f"
assumes Mg: "case_prod g ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t')"
assumes dens': "⋀M ρ. has_subprob_density M (stock_measure t) (f ρ) ⟹
has_density (distr M (stock_measure t') (op_sem oper))
(stock_measure t') (g ρ)"
assumes t1: "Γ ⊢ e : t" and t2 : "op_type oper t = Some t'"
assumes free_vars: "free_vars (oper $$ e) ⊆ V ∪ V'"
shows "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. dens_ctxt_measure (V,V',Γ,δ) ρ ⤜ (λσ. expr_sem σ (oper $$ e))) (stock_measure t') g"
proof-
interpret density_context V V' Γ δ by fact
show ?thesis unfolding has_parametrized_subprob_density_def
proof (intro conjI ballI impI)
show "case_prod g ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t')" by fact
fix ρ assume ρ: "ρ ∈ space (state_measure V' Γ)"
let ?M = "dens_ctxt_measure (V,V',Γ,δ) ρ"
have Me: "(λσ. expr_sem σ e) ∈ measurable ?M (subprob_algebra (stock_measure t))"
by (subst measurable_dens_ctxt_measure_eq)
(insert assms t1, auto intro!: measurable_expr_sem)
from dens and ρ have dens: "has_subprob_density (?M ⤜ (λσ. expr_sem σ e)) (stock_measure t) (f ρ)"
unfolding has_parametrized_subprob_density_def by auto
have "has_subprob_density (distr (?M ⤜ (λσ. expr_sem σ e)) (stock_measure t') (op_sem oper))
(stock_measure t') (g ρ)" (is "has_subprob_density ?N _ _")
proof (unfold has_subprob_density_def, intro conjI)
show "subprob_space ?N"
apply (intro subprob_space.subprob_space_distr has_subprob_densityD[OF dens])
apply (subst measurable_cong_sets[OF sets_bind_measurable refl])
apply (rule Me)
apply (simp_all add: measurable_op_sem t2)
done
from dens show "has_density ?N (stock_measure t') (g ρ)"
by (intro dens') (simp add: has_subprob_density_def)
qed
also from assms and ρ
have "?N = ?M ⤜ (λσ. expr_sem σ (oper $$ e))"
by (intro expr_sem_op_eq_distr[symmetric] expr_typing.intros) simp_all
finally show "has_subprob_density ... (stock_measure t') (g ρ)" .
qed
qed
lemma expr_has_density_sound_aux:
assumes "(V,V',Γ,δ) ⊢⇩d e ⇒ f" "Γ ⊢ e : t"
"density_context V V' Γ δ" "free_vars e ⊆ V ∪ V'"
shows "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. do {σ ← dens_ctxt_measure (V,V',Γ,δ) ρ; expr_sem σ e}) (stock_measure t)
(λρ x. f ρ x)"
using assms
proof (induction arbitrary: t rule: expr_has_density.induct[split_format (complete)])
case (hd_AE V V' Γ δ e f t f' t')
from ‹Γ ⊢ e : t'› and ‹Γ ⊢ e : t› have t[simp]: "t' = t"
by (rule expr_typing_unique)
have "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. dens_ctxt_measure (V, V', Γ, δ) ρ ⤜ (λσ. expr_sem σ e)) (stock_measure t) f" (is ?P)
by (intro hd_AE.IH) fact+
from has_parametrized_subprob_density_dens_AE[OF hd_AE.hyps(3,4) this] show ?case by simp
next
case (hd_dens_ctxt_cong V V' Γ δ e f δ' t)
interpret dc': density_context V V' Γ δ' by fact
from hd_dens_ctxt_cong.hyps and dc'.measurable_dens
have [simp]: "δ ∈ borel_measurable (state_measure (V ∪ V') Γ)"
by (erule_tac subst[OF measurable_cong, rotated]) simp
hence "density_context V V' Γ δ"
by (intro density_context_equiv[OF hd_dens_ctxt_cong.hyps(2)[symmetric]])
(insert hd_dens_ctxt_cong.prems hd_dens_ctxt_cong.hyps, simp_all)
hence "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. dens_ctxt_measure (V, V', Γ, δ) ρ ⤜ (λσ. expr_sem σ e)) (stock_measure t) f" (is ?P)
using hd_dens_ctxt_cong.prems hd_dens_ctxt_cong.hyps
by (intro hd_dens_ctxt_cong.IH) simp_all
also have "⋀σ. σ ∈ space (state_measure V' Γ) ⟹
dens_ctxt_measure (V, V', Γ, δ') σ = dens_ctxt_measure (V, V', Γ, δ) σ"
by (auto simp: dens_ctxt_measure_def state_measure'_def AE_distr_iff hd_dens_ctxt_cong.hyps
intro!: density_cong)
hence "?P ⟷ ?case" by (intro has_parametrized_subprob_density_cong) simp
finally show ?case .
next
case (hd_val v V V' Γ δ t)
hence [simp]: "t = val_type v" by auto
interpret density_context V V' Γ δ by fact
show ?case
proof (rule has_parametrized_subprob_densityI)
show "(λ(ρ, y). branch_prob (V,V',Γ,δ) ρ * indicator {v} y) ∈
borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t)"
by (subst measurable_split_conv)
(auto intro!: measurable_compose[OF measurable_snd borel_measurable_indicator]
borel_measurable_times_ennreal)
fix ρ assume ρ: "ρ ∈ space (state_measure V' Γ)"
have return_probspace: "prob_space (return_val v)" unfolding return_val_def
by (simp add: prob_space_return)
thus "subprob_space (dens_ctxt_measure (V,V',Γ,δ) ρ ⤜ (λσ. expr_sem σ (Val v)))" using ρ
by (auto simp: return_val_def
intro!: measurable_compose[OF measurable_const return_measurable] subprob_space_bind
subprob_space_dens hd_val.prems)
from hd_val.hyps have "stock_measure (val_type v) = count_space (type_universe t)"
by (simp add: countable_type_imp_count_space)
thus "dens_ctxt_measure 𝒴 ρ ⤜ (λσ. expr_sem σ (Val v)) =
density (stock_measure t) (λx. branch_prob 𝒴 ρ * indicator {v} x)"
by (subst expr_sem.simps, subst dens_ctxt_measure_bind_const, insert return_probspace)
(auto simp: return_val_def return_count_space_eq_density ρ
density_density_eq field_simps intro!: prob_space_imp_subprob_space)
qed
next
case (hd_var x V V' Γ δ t)
hence t: "t = Γ x" by auto
interpret density_context V V' Γ δ by fact
from hd_var have "x ∈ V" by simp
show ?case
proof (rule has_parametrized_subprob_densityI)
fix ρ assume ρ: "ρ ∈ space (state_measure V' Γ)"
have "subprob_space (dens_ctxt_measure 𝒴 ρ ⤜ (λσ. return (stock_measure t) (σ x)))"
(is "subprob_space (?M ⤜ ?f)") using hd_var ρ
by (intro subprob_space_bind)
(auto simp: return_val_def t intro!: subprob_space_bind subprob_space_dens
measurable_compose[OF measurable_dens_ctxt_measure_component return_measurable])
also from hd_var.hyps have "?M ⤜ ?f = ?M ⤜ (λσ. return_val (σ x))"
by (intro bind_cong) (auto simp: return_val_def t space_dens_ctxt_measure
state_measure_def space_PiM dest!: PiE_mem)
finally show "subprob_space (?M ⤜ (λσ. expr_sem σ (Var x)))" by simp
from hd_var interpret dcm: subprob_space "dens_ctxt_measure 𝒴 ρ"
by (intro subprob_space_dens ρ)
let ?M1 = "dens_ctxt_measure 𝒴 ρ ⤜ (λσ. expr_sem σ (Var x))"
let ?M2 = "density (stock_measure t) (λv. marg_dens 𝒴 x ρ v)"
have "∀σ∈space (dens_ctxt_measure 𝒴 ρ). val_type (σ x) = t" using hd_var
by (auto simp: space_dens_ctxt_measure space_PiM PiE_iff
state_measure_def intro: type_universe_type)
hence "?M1 = dens_ctxt_measure 𝒴 ρ ⤜ (return (stock_measure t) ∘ (λσ. σ x))"
by (intro bind_cong_All) (simp add: return_val_def)
also have "... = distr (dens_ctxt_measure 𝒴 ρ) (stock_measure t) (λσ. σ x)"
using dcm.subprob_not_empty hd_var
by (subst bind_return_distr) (auto intro!: measurable_dens_ctxt_measure_component)
also have "... = ?M2" using density_marg_dens_eq[OF ‹x ∈ V›]
by (simp add: t hd_var.prems ρ)
finally show "?M1 = ?M2" .
qed (auto intro!: measurable_marg_dens' simp: hd_var t)
next
case (hd_let V V' Γ e1 f δ e2 g t)
let ?t = "the (expr_type Γ e1)"
let ?Γ' = "case_nat ?t Γ" and ?δ' = "insert_dens V V' f δ"
let ?𝒴' = "(shift_var_set V, Suc`V', ?Γ', ?δ')"
from hd_let.prems have t1: "Γ ⊢ e1 : ?t" and t2: "?Γ' ⊢ e2 : t"
by (auto simp: expr_type_Some_iff[symmetric] split: option.split_asm)
interpret dc: density_context V V' Γ δ by fact
show ?case unfolding has_parametrized_subprob_density_def
proof (intro ballI conjI)
have "density_context {} (V ∪ V') Γ (λa. 1)" by (rule dc.density_context_empty)
moreover note hd_let.prems
ultimately have "has_parametrized_subprob_density (state_measure (V ∪ V') Γ)
(λρ. dens_ctxt_measure ({},V∪V',Γ,λa. 1) ρ ⤜ (λσ. expr_sem σ e1))
(stock_measure ?t) f" (is "?P")
by (intro hd_let.IH(1)) (auto intro!: t1)
also have "?P ⟷ has_parametrized_subprob_density (state_measure (V ∪ V') Γ)
(λσ. expr_sem σ e1) (stock_measure ?t) f" using hd_let.prems
by (intro has_parametrized_subprob_density_cong dens_ctxt_measure_empty_bind)
(auto simp: dens_ctxt_measure_def state_measure'_def
intro!: measurable_expr_sem[OF t1])
finally have f: "has_parametrized_subprob_density (state_measure (V∪V') Γ)
(λρ. expr_sem ρ e1) (stock_measure ?t) f" .
have g: "has_parametrized_subprob_density (state_measure (Suc`V') ?Γ')
(λρ. dens_ctxt_measure ?𝒴' ρ ⤜ (λσ. expr_sem σ e2)) (stock_measure t) g"
using hd_let.prems hd_let.hyps f subset_shift_var_set
by (intro hd_let.IH(2) t2 dc.density_context_insert)
(auto dest: has_parametrized_subprob_densityD)
note g[measurable]
thus "(λ(ρ, x). g (case_nat undefined ρ) x) ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t)"
by simp
fix ρ assume ρ: "ρ ∈ space (state_measure V' Γ)"
let ?M = "dens_ctxt_measure (V, V', Γ, δ) ρ" and
?N = "state_measure (shift_var_set (V∪V')) ?Γ'"
have M_dcm: "measurable ?M = measurable (state_measure (V∪V') Γ)"
by (intro ext measurable_cong_sets)
(auto simp: dens_ctxt_measure_def state_measure_def state_measure'_def)
have M_dcm': "⋀N. measurable (?M ⨂⇩M N) = measurable (state_measure (V∪V') Γ ⨂⇩M N)"
by (intro ext measurable_cong_sets)
(auto simp: dens_ctxt_measure_def state_measure_def state_measure'_def)
have "?M ⤜ (λσ. expr_sem σ (LetVar e1 e2)) =
do {σ ← ?M; y ← expr_sem σ e1; return ?N (case_nat y σ)} ⤜ (λσ. expr_sem σ e2)"
(is "_ = bind ?R _")
using hd_let.prems subset_shift_var_set
apply (simp only: expr_sem.simps, intro double_bind_assoc)
apply (rule measurable_expr_sem[OF t2], simp)
apply (subst M_dcm, rule measurable_expr_sem[OF t1], simp)
apply (subst M_dcm', simp)
done
also from t1 and hd_let.prems
have "(λσ. expr_sem σ e1) ∈
measurable (state_measure (V ∪ V') Γ) (subprob_algebra (stock_measure ?t))"
by (intro measurable_expr_sem) auto
hence "?R = dens_ctxt_measure ?𝒴' (case_nat undefined ρ)" using hd_let.prems hd_let.hyps f ρ
by (intro dc.dens_ctxt_measure_insert) (auto simp: has_parametrized_subprob_density_def)
also have "case_nat undefined ρ ∈ space (state_measure (Suc`V') ?Γ')"
by (rule measurable_space[OF measurable_case_nat_undefined ρ])
with g have "has_subprob_density (dens_ctxt_measure ?𝒴' (case_nat undefined ρ) ⤜
(λσ. expr_sem σ e2)) (stock_measure t) (g (case_nat undefined ρ))"
using ρ unfolding has_parametrized_subprob_density_def by auto
finally show "has_subprob_density (?M ⤜ (λσ. expr_sem σ (LetVar e1 e2))) (stock_measure t)
(g (case_nat undefined ρ))" .
qed
next
case (hd_rand_det e V' V Γ δ dst t)
then have [measurable]: "Γ ⊢ e : dist_param_type dst" "randomfree e" "free_vars e ⊆ V'"
by auto
interpret density_context V V' Γ δ by fact
from hd_rand_det have t: "t = dist_result_type dst" by auto
{
fix ρ assume ρ: "ρ ∈ space (state_measure V' Γ)"
let ?M = "dens_ctxt_measure (V,V',Γ,δ) ρ" and ?t = "dist_param_type dst"
have "?M ⤜ (λσ. expr_sem σ (Random dst e)) =
?M ⤜ (λσ. return_val (expr_sem_rf σ e) ⤜ dist_measure dst)" (is "_ = ?N")
using hd_rand_det by (subst expr_sem.simps, intro bind_cong refl, subst expr_sem_rf_sound)
(auto simp: dens_ctxt_measure_def state_measure'_def)
also from hd_rand_det have A: "⋀σ. σ ∈ space ?M ⟹ val_type (expr_sem_rf σ e) = ?t"
by (intro val_type_expr_sem_rf) (auto simp: dens_ctxt_measure_def state_measure'_def)
hence "?N = ?M ⤜ (λσ. return (stock_measure ?t) (expr_sem_rf σ e) ⤜ dist_measure dst)"
using hd_rand_det unfolding return_val_def
by (intro bind_cong) (auto simp: dens_ctxt_measure_def state_measure'_def)
also have "... = ?M ⤜ (λσ. dist_measure dst (expr_sem_rf σ e))"
unfolding return_val_def
by (intro bind_cong refl bind_return, rule measurable_dist_measure)
(auto simp: type_universe_def A simp del: type_universe_type)
finally have "?M ⤜ (λσ. expr_sem σ (Random dst e)) =
?M ⤜ (λσ. dist_measure dst (expr_sem_rf σ e))" .
} note A = this
have "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. dens_ctxt_measure 𝒴 ρ ⤜ (λσ. dist_measure dst (expr_sem_rf σ e)))
(stock_measure t) (λρ x. branch_prob 𝒴 ρ * dist_dens dst (expr_sem_rf ρ e) x)"
proof (unfold has_parametrized_subprob_density_def, intro conjI ballI)
show M: "(λ(ρ, v). branch_prob 𝒴 ρ * dist_dens dst (expr_sem_rf ρ e) v)
∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t)"
by (subst t) measurable
fix ρ assume ρ: "ρ ∈ space (state_measure V' Γ)"
let ?M = "dens_ctxt_measure (V,V',Γ,δ) ρ" and ?t = "dist_param_type dst"
have "?M ⤜ (λσ. expr_sem σ (Random dst e)) =
?M ⤜ (λσ. return_val (expr_sem_rf σ e) ⤜ dist_measure dst)" (is "_ = ?N")
using hd_rand_det by (subst expr_sem.simps, intro bind_cong refl, subst expr_sem_rf_sound)
(auto simp: dens_ctxt_measure_def state_measure'_def)
also from hd_rand_det have A: "⋀σ. σ ∈ space ?M ⟹ val_type (expr_sem_rf σ e) = ?t"
by (intro val_type_expr_sem_rf) (auto simp: dens_ctxt_measure_def state_measure'_def)
hence "?N = ?M ⤜ (λσ. return (stock_measure ?t) (expr_sem_rf σ e) ⤜ dist_measure dst)"
using hd_rand_det unfolding return_val_def
by (intro bind_cong) (auto simp: dens_ctxt_measure_def state_measure'_def)
also have "... = ?M ⤜ (λσ. dist_measure dst (expr_sem_rf σ e))"
unfolding return_val_def
by (intro bind_cong refl bind_return, rule measurable_dist_measure)
(auto simp: type_universe_def A simp del: type_universe_type)
also have "has_subprob_density (?M ⤜ (λσ. dist_measure dst (expr_sem_rf σ e))) (stock_measure t)
(λv. ∫⇧+σ. dist_dens dst (expr_sem_rf (restrict σ V') e) v ∂?M)"
(is "has_subprob_density ?N ?R ?f")
proof (rule bind_has_subprob_density)
show "space ?M ≠ {}" unfolding dens_ctxt_measure_def state_measure'_def state_measure_def
by (auto simp: space_PiM PiE_eq_empty_iff)
show "(λσ. dist_measure dst (expr_sem_rf σ e)) ∈ measurable ?M (subprob_algebra (stock_measure t))"
unfolding dens_ctxt_measure_def state_measure'_def
by (subst t, rule measurable_compose[OF _ measurable_dist_measure], simp)
(insert hd_rand_det, auto intro!: measurable_expr_sem_rf)
show "(λ(x, y). dist_dens dst (expr_sem_rf (restrict x V') e) y)
∈ borel_measurable (?M ⨂⇩M stock_measure t)"
unfolding t by measurable
fix σ assume σ: "σ ∈ space ?M"
hence σ': "restrict σ V' ∈ space (state_measure V' Γ)"
unfolding dens_ctxt_measure_def state_measure'_def state_measure_def restrict_def
by (auto simp: space_PiM)
from hd_rand_det have restr: "expr_sem_rf (restrict σ V') e = expr_sem_rf σ e"
by (intro expr_sem_rf_eq_on_vars) auto
from hd_rand_det have "val_type (expr_sem_rf (restrict σ V') e) = dist_param_type dst"
by (auto intro!: val_type_expr_sem_rf[OF _ _ _ σ'])
also note restr
finally have "has_density (dist_measure dst (expr_sem_rf σ e)) (stock_measure t)
(dist_dens dst (expr_sem_rf σ e))" using hd_rand_det
by (subst t, intro dist_measure_has_density)
(auto intro!: val_type_expr_sem_rf simp: type_universe_def dens_ctxt_measure_def
state_measure'_def simp del: type_universe_type)
thus "has_density (dist_measure dst (expr_sem_rf σ e)) (stock_measure t)
(dist_dens dst (expr_sem_rf (restrict σ V') e))" by (simp add: restr)
qed (insert ρ, auto intro!: subprob_space_dens)
moreover have "val_type (expr_sem_rf ρ e) = dist_param_type dst" using hd_rand_det ρ
by (intro val_type_expr_sem_rf) auto
hence "expr_sem_rf ρ e ∈ type_universe (dist_param_type dst)"
by (simp add: type_universe_def del: type_universe_type)
ultimately show "has_subprob_density (?M ⤜ (λσ. dist_measure dst (expr_sem_rf σ e)))
(stock_measure t) (λv. branch_prob 𝒴 ρ * dist_dens dst (expr_sem_rf ρ e) v)"
using hd_rand_det
apply (rule_tac has_subprob_density_equal_on_space, simp)
apply (intro nn_integral_dens_ctxt_measure_restrict)
apply (simp_all add: t ρ)
done
qed
with A show ?case by (subst has_parametrized_subprob_density_cong) (simp_all add: A)
next
case (hd_rand V V' Γ δ e f dst t)
let ?t = "dist_param_type dst"
from hd_rand.prems have t1: "Γ ⊢ e : ?t" and t2: "t = dist_result_type dst" by auto
interpret density_context V V' Γ δ by fact
have dens[measurable]: "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. dens_ctxt_measure (V, V', Γ, δ) ρ ⤜ (λσ. expr_sem σ e)) (stock_measure ?t) f"
using hd_rand.prems by (intro hd_rand.IH) auto
show ?case
proof (unfold has_parametrized_subprob_density_def, intro ballI conjI impI)
interpret sigma_finite_measure "stock_measure (dist_param_type dst)" by simp
show "case_prod (apply_dist_to_dens dst f) ∈
borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t)"
unfolding apply_dist_to_dens_def t2 by measurable
fix ρ assume ρ: "ρ ∈ space (state_measure V' Γ)"
let ?M = "dens_ctxt_measure (V, V', Γ, δ) ρ"
have meas_M: "measurable ?M = measurable (state_measure (V ∪ V') Γ)"
by (intro ext measurable_cong_sets) (auto simp: dens_ctxt_measure_def state_measure'_def)
from hd_rand have Me: "(λσ. expr_sem σ e) ∈ measurable ?M (subprob_algebra (stock_measure ?t))"
by (subst meas_M, intro measurable_expr_sem[OF t1]) auto
hence "?M ⤜ (λσ. expr_sem σ (Random dst e)) = (?M ⤜ (λσ. expr_sem σ e)) ⤜ dist_measure dst"
(is "_ = ?N")
by (subst expr_sem.simps, intro bind_assoc[OF Me, symmetric])
(insert hd_rand, auto intro!: measurable_dist_measure)
also have "space ?M ≠ {}"
by (auto simp: dens_ctxt_measure_def state_measure'_def state_measure_def
space_PiM PiE_eq_empty_iff)
with dens ρ Me have "has_subprob_density ?N (stock_measure t) (apply_dist_to_dens dst f ρ)"
unfolding apply_dist_to_dens_def has_parametrized_subprob_density_def
by (subst t2, intro bind_has_subprob_density')
(auto simp: hd_rand.IH space_bind_measurable
intro!: measurable_dist_dens dist_measure_has_subprob_density)
finally show "has_subprob_density (?M ⤜ (λσ. expr_sem σ (Random dst e))) (stock_measure t)
(apply_dist_to_dens dst f ρ)" .
qed
next
case (hd_fail V V' Γ δ t t')
interpret density_context V V' Γ δ by fact
have "has_parametrized_subprob_density (state_measure V' Γ)
(λ_. null_measure (stock_measure t)) (stock_measure t') (λ_ _. 0)" (is "?P")
using hd_fail by (auto simp: has_parametrized_subprob_density_def
intro!: null_measure_has_subprob_density)
also have "?P ⟷ ?case"
by (intro has_parametrized_subprob_density_cong)
(auto simp: dens_ctxt_measure_bind_const subprob_space_null_measure_iff)
finally show ?case .
next
case (hd_pair x V y V' Γ δ t)
interpret density_context V V' Γ δ by fact
let ?R = "stock_measure t"
from hd_pair.prems have t: "t = PRODUCT (Γ x) (Γ y)" by auto
have meas: "(λσ. <|σ x, σ y|>) ∈ measurable (state_measure (V∪V') Γ) ?R"
using hd_pair unfolding t state_measure_def by simp
have "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. distr (dens_ctxt_measure (V, V', Γ, δ) ρ) ?R (λσ. <|σ x, σ y|>))
(stock_measure t) (marg_dens2 𝒴 x y)"
proof (rule has_parametrized_subprob_densityI)
fix ρ assume ρ: "ρ ∈ space (state_measure V' Γ)"
let ?M = "dens_ctxt_measure (V, V', Γ, δ) ρ"
from hd_pair.hyps ρ show "distr ?M ?R (λσ. <|σ x , σ y |>) = density ?R (marg_dens2 𝒴 x y ρ)"
by (subst (1 2) t, rule density_marg_dens2_eq[symmetric])
from ρ interpret subprob_space ?M by (rule subprob_space_dens)
show "subprob_space (distr (dens_ctxt_measure (V,V',Γ,δ) ρ) ?R (λσ. <|σ x ,σ y|>))"
by (rule subprob_space_distr)
(simp_all add: meas measurable_dens_ctxt_measure_eq)
qed (auto simp: t intro!: measurable_marg_dens2' hd_pair.hyps simp del: stock_measure.simps)
also from hd_pair.hyps
have "(λρ. distr (dens_ctxt_measure (V, V', Γ, δ) ρ) ?R (λσ. <|σ x, σ y|>)) =
(λρ. dens_ctxt_measure (V, V', Γ, δ) ρ ⤜ (λσ. return_val <|σ x, σ y|>))"
by (intro ext bind_return_val[symmetric]) (simp_all add: meas measurable_dens_ctxt_measure_eq)
finally show ?case by (simp only: expr_sem_pair_vars)
next
case (hd_if V V' Γ b f δ e1 g1 e2 g2 t)
interpret dc: density_context V V' Γ δ by fact
from hd_if.prems have tb: "Γ ⊢ b : BOOL" and t1: "Γ ⊢ e1 : t" and t2: "Γ ⊢ e2 : t" by auto
have "has_parametrized_subprob_density (state_measure (V ∪ V') Γ)
(λρ. dens_ctxt_measure ({},V∪V',Γ,λa. 1) ρ ⤜ (λσ. expr_sem σ b)) (stock_measure BOOL) f"
(is "?P") using hd_if.prems tb by (intro hd_if.IH(1)) auto
also have "?P ⟷ has_parametrized_subprob_density (state_measure (V ∪ V') Γ)
(λσ. expr_sem σ b) (stock_measure BOOL) f" (is "_ = ?P") using hd_if.prems
by (intro has_parametrized_subprob_density_cong dens_ctxt_measure_empty_bind)
(auto simp: dens_ctxt_measure_def state_measure'_def
intro!: measurable_expr_sem[OF tb])
finally have f: ?P .
let ?M = "λρ. dens_ctxt_measure (V,V',Γ,δ) ρ"
let ?M' = "λb ρ. dens_ctxt_measure (V,V',Γ,if_dens δ f b) ρ"
from f have dc': "⋀b. density_context V V' Γ (if_dens δ f b)"
by (intro dc.density_context_if_dens) (simp add: stock_measure.simps)
have g1[measurable]: "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. ?M' True ρ ⤜ (λσ. expr_sem σ e1)) (stock_measure t) g1" using hd_if.prems
by (intro hd_if.IH(2)[OF t1 dc']) simp
have g2[measurable]: "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. ?M' False ρ ⤜ (λσ. expr_sem σ e2)) (stock_measure t) g2" using hd_if.prems
by (intro hd_if.IH(3)[OF t2 dc']) simp
show ?case
proof (rule has_parametrized_subprob_densityI)
show "(λ(ρ, x). g1 ρ x + g2 ρ x) ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t)"
by measurable
fix ρ assume ρ: "ρ ∈ space (state_measure V' Γ)"
show "subprob_space (?M ρ ⤜ (λσ. expr_sem σ (IF b THEN e1 ELSE e2)))"
using ρ hd_if.prems
by (intro subprob_space_bind[of _ _ "stock_measure t"], simp add: dc.subprob_space_dens)
(auto intro!: measurable_expr_sem simp: measurable_dens_ctxt_measure_eq
simp del: expr_sem.simps)
show "?M ρ ⤜ (λσ. expr_sem σ (IF b THEN e1 ELSE e2)) =
density (stock_measure t) (λx. g1 ρ x + g2 ρ x)" using ρ hd_if.prems f g1 g2
by (subst expr_sem.simps, intro dc.emeasure_bind_if_dens_ctxt_measure)
(auto simp: measurable_dens_ctxt_measure_eq if_dens_def
simp del: stock_measure.simps intro!: measurable_expr_sem)
qed
next
case (hd_if_det b V V' Γ δ e1 g1 e2 g2 t)
interpret dc: density_context V V' Γ δ by fact
from hd_if_det.prems ‹randomfree b›
have tb[measurable (raw)]: "Γ ⊢ b : BOOL" and [measurable (raw)]: "randomfree b"
and t1[measurable (raw)]: "Γ ⊢ e1 : t"
and t2[measurable (raw)]: "Γ ⊢ e2 : t"
and fv_b[measurable (raw)]: "free_vars b ⊆ V ∪ V'"
and fv_e1[measurable (raw)]: "free_vars e1 ⊆ V ∪ V'"
and fv_e2[measurable (raw)]: "free_vars e2 ⊆ V ∪ V'" by auto
let ?M = "λρ. dens_ctxt_measure (V,V',Γ,δ) ρ"
let ?M' = "λx ρ. dens_ctxt_measure (V,V',Γ,if_dens_det δ b x) ρ"
let ?N = "λρ. ?M ρ⤜ (λσ. if expr_sem_rf σ b = BoolVal True then expr_sem σ e1 else expr_sem σ e2)"
from hd_if_det.hyps hd_if_det.prems tb
have dc': "⋀x. density_context V V' Γ (if_dens_det δ b x)"
by (intro dc.density_context_if_dens_det) simp_all
have g1[measurable]: "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. ?M' True ρ ⤜ (λσ. expr_sem σ e1)) (stock_measure t) g1" using hd_if_det.prems
by (intro hd_if_det.IH(1)[OF]) (simp_all add: dc' t1)
have g2[measurable]: "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. ?M' False ρ ⤜ (λσ. expr_sem σ e2)) (stock_measure t) g2" using hd_if_det.prems
by (intro hd_if_det.IH(2)[OF]) (simp_all add: dc' t2)
note val_type_expr_sem_rf[OF tb, of "V ∪ V'", simp]
have "has_parametrized_subprob_density (state_measure V' Γ) ?N
(stock_measure t) (λa b. g1 a b + g2 a b)" (is "?P")
proof (rule has_parametrized_subprob_densityI)
show "(λ(ρ, x). g1 ρ x + g2 ρ x) ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t)"
by measurable
fix ρ assume ρ: "ρ ∈ space (state_measure V' Γ)"
show "subprob_space (?N ρ)"
using ρ hd_if_det.prems hd_if_det.hyps t1 t2
by (intro subprob_space_bind[of _ _ "stock_measure t"]) (auto simp add: dc.subprob_space_dens)
show "?N ρ = density (stock_measure t) (λx. g1 ρ x + g2 ρ x)"
using ρ hd_if_det.prems g1 g2 dc' hd_if_det.prems unfolding if_dens_det_def
by (intro dc.emeasure_bind_if_det_dens_ctxt_measure)
(simp_all add: space_dens_ctxt_measure)
qed
also from hd_if_det.prems hd_if_det.hyps have "?P ⟷ ?case"
apply (intro has_parametrized_subprob_density_cong bind_cong refl)
apply (subst expr_sem.simps)
apply (subst expr_sem_rf_sound[OF tb, of "V ∪ V'", symmetric]) []
apply (simp_all add: space_dens_ctxt_measure bind_return_val''[where M="stock_measure t"])
done
finally show ?case .
next
case (hd_fst V V' Γ δ e f t)
interpret density_context V V' Γ δ by fact
from hd_fst.prems obtain t' where t: "Γ ⊢ e : PRODUCT t t'"
by (elim expr_typing_opE) (auto split: pdf_type.split_asm)
hence "Γ ⊢ Snd $$ e : t'" by (intro expr_typing.intros) auto
hence t2: "the (expr_type Γ (Snd $$ e)) = t'" by (simp add: expr_type_Some_iff[symmetric])
let ?N = "stock_measure (PRODUCT t t')"
have dens[measurable]: "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. dens_ctxt_measure (V, V', Γ, δ) ρ ⤜ (λσ. expr_sem σ e)) ?N f"
by (intro hd_fst.IH) (insert hd_fst.prems hd_fst.hyps t, auto)
let ?f = "λρ x. ∫⇧+ y. f ρ <|x,y|> ∂stock_measure t'"
have "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. dens_ctxt_measure (V, V', Γ, δ) ρ ⤜ (λσ. expr_sem σ (Fst $$ e))) (stock_measure t) ?f"
unfolding has_parametrized_subprob_density_def
proof (intro conjI ballI impI)
interpret sigma_finite_measure "stock_measure t'" by simp
show "case_prod ?f ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t)"
by measurable
fix ρ assume ρ: "ρ ∈ space (state_measure V' Γ)"
let ?M = "dens_ctxt_measure (V, V', Γ, δ) ρ"
from dens and ρ have "has_subprob_density (?M ⤜ (λσ. expr_sem σ e)) ?N (f ρ)"
unfolding has_parametrized_subprob_density_def by auto
hence "has_subprob_density (distr (?M ⤜ (λσ. expr_sem σ e)) (stock_measure t) (op_sem Fst))
(stock_measure t) (?f ρ)" (is "has_subprob_density ?R _ _")
by (intro has_subprob_density_distr_Fst) simp
also from hd_fst.prems and ρ have "?R = ?M ⤜ (λσ. expr_sem σ (Fst $$ e))"
by (intro expr_sem_op_eq_distr[symmetric]) simp_all
finally show "has_subprob_density ... (stock_measure t) (?f ρ)" .
qed
thus ?case by (subst t2)
next
case (hd_snd V V' Γ δ e f t')
interpret density_context V V' Γ δ by fact
from hd_snd.prems obtain t where t: "Γ ⊢ e : PRODUCT t t'"
by (elim expr_typing_opE) (auto split: pdf_type.split_asm)
hence "Γ ⊢ Fst $$ e : t" by (intro expr_typing.intros) auto
hence t2: "the (expr_type Γ (Fst $$ e)) = t" by (simp add: expr_type_Some_iff[symmetric])
let ?N = "stock_measure (PRODUCT t t')"
have dens[measurable]: "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. dens_ctxt_measure (V, V', Γ, δ) ρ ⤜ (λσ. expr_sem σ e)) ?N f"
by (intro hd_snd.IH) (insert hd_snd.prems hd_snd.hyps t, auto)
let ?f = "λρ y. ∫⇧+ x. f ρ <|x,y|> ∂stock_measure t"
have "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. dens_ctxt_measure (V, V', Γ, δ) ρ ⤜ (λσ. expr_sem σ (Snd $$ e))) (stock_measure t') ?f"
unfolding has_parametrized_subprob_density_def
proof (intro conjI ballI impI)
interpret sigma_finite_measure "stock_measure t" by simp
show "case_prod ?f ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t')"
by measurable
fix ρ assume ρ: "ρ ∈ space (state_measure V' Γ)"
let ?M = "dens_ctxt_measure (V, V', Γ, δ) ρ"
from dens and ρ have "has_subprob_density (?M ⤜ (λσ. expr_sem σ e)) ?N (f ρ)"
unfolding has_parametrized_subprob_density_def by auto
hence "has_subprob_density (distr (?M ⤜ (λσ. expr_sem σ e)) (stock_measure t') (op_sem Snd))
(stock_measure t') (?f ρ)" (is "has_subprob_density ?R _ _")
by (intro has_subprob_density_distr_Snd) simp
also from hd_snd.prems and ρ have "?R = ?M ⤜ (λσ. expr_sem σ (Snd $$ e))"
by (intro expr_sem_op_eq_distr[symmetric]) simp_all
finally show "has_subprob_density ... (stock_measure t') (?f ρ)" .
qed
thus ?case by (subst t2)
next
case (hd_op_discr Γ oper e V V' δ f t')
interpret density_context V V' Γ δ by fact
from hd_op_discr.prems obtain t where t1: "Γ ⊢ e : t" and t2: "op_type oper t = Some t'" by auto
have dens[measurable]: "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. dens_ctxt_measure (V, V', Γ, δ) ρ ⤜ (λσ. expr_sem σ e)) (stock_measure t) f"
by (intro hd_op_discr.IH) (insert hd_op_discr.prems hd_op_discr.hyps t1, auto)
from hd_op_discr t1 have "expr_type Γ e = Some t" and "expr_type Γ (oper $$ e) = Some t'"
by (simp_all add: expr_type_Some_iff[symmetric])
hence t1': "the (expr_type Γ e) = t" and t2': "the (expr_type Γ (oper $$ e)) = t'" by auto
with hd_op_discr have countable: "countable_type t'" by simp
have A: "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. distr (dens_ctxt_measure (V, V', Γ, δ) ρ ⤜ (λσ. expr_sem σ e))
(stock_measure t') (op_sem oper))
(stock_measure t')
(λa b. ∫⇧+x. (if op_sem oper x = b then 1 else 0) * f a x ∂stock_measure t)"
proof (intro has_parametrized_subprob_densityI)
let ?f = "λρ y. ∫⇧+x. (if op_sem oper x = y then 1 else 0) * f ρ x ∂stock_measure t"
note sigma_finite_measure.borel_measurable_nn_integral[OF sigma_finite_stock_measure, measurable]
show "case_prod ?f ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t')"
using measurable_op_sem[OF t2] by measurable
fix ρ assume ρ: "ρ ∈ space (state_measure V' Γ)"
let ?M = "dens_ctxt_measure (V, V', Γ, δ) ρ"
let ?N = "?M ⤜ (λσ. expr_sem σ e)"
from dens and ρ have dens': "has_subprob_density ?N (stock_measure t) (f ρ)"
unfolding has_parametrized_subprob_density_def by auto
from hd_op_discr.prems t1
have M_e: "(λσ. expr_sem σ e) ∈ measurable ?M (subprob_algebra (stock_measure t))"
by (auto simp: measurable_dens_ctxt_measure_eq intro!: measurable_expr_sem)
from M_e have meas_N: "measurable ?N = measurable (stock_measure t)"
by (intro ext measurable_cong_sets) (simp_all add: sets_bind_measurable)
from dens' and t2 show "subprob_space (distr ?N (stock_measure t') (op_sem oper))"
by (intro subprob_space.subprob_space_distr)
(auto dest: has_subprob_densityD intro!: measurable_op_sem simp: meas_N)
from countable have count_space: "stock_measure t' = count_space (type_universe t')"
by (rule countable_type_imp_count_space)
from dens' have "?N = density (stock_measure t) (f ρ)" by (rule has_subprob_densityD)
also {
fix x assume "x ∈ type_universe t"
with M_e have "val_type x = t" by (auto simp:)
hence "val_type (op_sem oper x) = t'" by (intro op_sem_val_type) (simp add: t2)
} note op_sem_type_universe = this
from countable countable_type_countable measurable_op_sem[OF t2] dens'
have "distr ... (stock_measure t') (op_sem oper) = density (stock_measure t') (?f ρ)"
by (subst count_space, subst distr_density_discrete)
(auto simp: meas_N count_space intro!: op_sem_type_universe dest: has_subprob_densityD)
finally show "distr ?N (stock_measure t') (op_sem oper) = density (stock_measure t') (?f ρ)" .
qed
from hd_op_discr.prems
have B: "⋀ρ. ρ ∈ space (state_measure V' Γ) ⟹
distr (dens_ctxt_measure (V,V',Γ,δ) ρ ⤜ (λσ. expr_sem σ e))
(stock_measure t') (op_sem oper) =
dens_ctxt_measure (V,V',Γ,δ) ρ ⤜ (λσ. expr_sem σ (oper $$ e))"
by (intro expr_sem_op_eq_distr[symmetric]) simp_all
show ?case by (simp only: has_parametrized_subprob_density_cong[OF B[symmetric]] t1' A)
next
case (hd_neg V V' Γ δ e f t')
from hd_neg.prems obtain t where t1: "Γ ⊢ e : t" and t2: "op_type Minus t = Some t'" by auto
have dens: "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. dens_ctxt_measure (V, V', Γ, δ) ρ ⤜ (λσ. expr_sem σ e)) (stock_measure t) f"
by (intro hd_neg.IH) (insert hd_neg.prems hd_neg.hyps t1, auto)
with hd_neg and t1 and t2 show ?case
proof (intro expr_has_density_sound_op[where t = t])
from t2 have [measurable]: "lift_RealIntVal uminus uminus ∈ measurable (stock_measure t') (stock_measure t)"
by (simp split: pdf_type.split_asm)
from dens have Mf[measurable]: "case_prod f ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t)"
by (blast dest: has_parametrized_subprob_densityD)
show "(λ(ρ, x). f ρ (op_sem Minus x))
∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t')" by simp
fix M ρ assume dens': "has_subprob_density M (stock_measure t) (f ρ)"
hence space_M: "space M = space (stock_measure t)" by (auto dest: has_subprob_densityD)
from t2 have t_disj: "(t = REAL ∧ t' = REAL) ∨ (t = INTEG ∧ t' = INTEG)"
by (auto split: pdf_type.split_asm)
thus "has_density (distr M (stock_measure t') (op_sem Minus))
(stock_measure t') (λx. f ρ (op_sem Minus x))" (is "?thesis")
proof (elim disjE conjE)
assume A: "t = REAL" "t' = REAL"
have "has_density (distr M (stock_measure t') (lift_RealVal uminus)) (stock_measure t')
((λx. f ρ (RealVal (-x))) ∘ extract_real)" using dens'
by (simp only: A, intro distr_lift_RealVal)
(auto intro!: distr_uminus_real dest: has_subprob_density_imp_has_density)
also have "distr M (stock_measure t') (lift_RealVal uminus) =
distr M (stock_measure t') (lift_RealIntVal uminus uminus)" using dens'
by (intro distr_cong) (auto intro!: lift_RealIntVal_Real[symmetric] simp: space_M A)
also have "has_density ... (stock_measure t') ((λx. f ρ (RealVal (-x))) ∘ extract_real) ⟷
has_density ... (stock_measure t') (λx. f ρ (lift_RealIntVal uminus uminus x))"
by (intro has_density_cong)
(auto simp: lift_RealIntVal_def extract_real_def A space_embed_measure split: val.split)
finally show ?thesis by simp
next
assume A: "t = INTEG" "t' = INTEG"
have "has_density (distr M (stock_measure t') (lift_IntVal uminus)) (stock_measure t')
((λx. f ρ (IntVal (-x))) ∘ extract_int)" using dens'
by (simp only: A, intro distr_lift_IntVal)
(auto intro!: distr_uminus_ring_count_space simp: has_subprob_density_def)
also have "distr M (stock_measure t') (lift_IntVal uminus) =
distr M (stock_measure t') (lift_RealIntVal uminus uminus)" using dens'
by (intro distr_cong) (auto intro!: lift_RealIntVal_Int[symmetric] simp: space_M A)
also have "has_density ... (stock_measure t') ((λx. f ρ (IntVal (-x))) ∘ extract_int) ⟷
has_density ... (stock_measure t') (λx. f ρ (lift_RealIntVal uminus uminus x))"
by (intro has_density_cong)
(auto simp: lift_RealIntVal_def extract_int_def A space_embed_measure split: val.split)
finally show ?thesis by simp
qed
qed auto
next
case (hd_exp V V' Γ δ e f t')
from hd_exp.prems have t1: "Γ ⊢ e : REAL" and t2: "t' = REAL"
by (auto split: pdf_type.split_asm)
have dens[measurable]: "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. dens_ctxt_measure (V, V', Γ, δ) ρ ⤜ (λσ. expr_sem σ e)) (stock_measure REAL) f"
by (intro hd_exp.IH) (insert hd_exp.prems hd_exp.hyps t1, auto)
with hd_exp and t1 and t2 show ?case
proof (intro expr_has_density_sound_op[where t = REAL])
from t2 have [measurable]: "lift_RealVal safe_ln ∈ measurable (stock_measure REAL) (stock_measure REAL)"
by (simp split: pdf_type.split_asm)
from dens have Mf[measurable]: "case_prod f ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure REAL)"
by (blast dest: has_parametrized_subprob_densityD)
let ?f = "λρ x. if extract_real x > 0 then
f ρ (lift_RealVal safe_ln x) * inverse (extract_real x) else 0"
show "case_prod ?f ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t')"
unfolding t2 by measurable
fix M ρ assume dens': "has_subprob_density M (stock_measure REAL) (f ρ)"
hence space_M: "space M = space (stock_measure REAL)" by (auto dest: has_subprob_densityD)
have "has_density (distr M (stock_measure t') (lift_RealVal exp)) (stock_measure t')
((λx. if 0 < x then f ρ (RealVal (ln x)) * ennreal (inverse x) else 0)
∘ extract_real)" (is "has_density _ _ ?f'") using dens'
apply (simp only: t2)
apply (rule distr_lift_RealVal[where g = "λf x. if x > 0 then f (ln x) * ennreal (inverse x) else 0"])
apply (auto intro!: subprob_density_distr_real_exp intro: has_subprob_density_imp_has_density)
done
also have "?f' = ?f ρ"
by (intro ext) (simp add: o_def lift_RealVal_def extract_real_def split: val.split)
finally show "has_density (distr M (stock_measure t') (op_sem Exp)) (stock_measure t') ..."
by simp
qed auto
next
case (hd_inv V V' Γ δ e f t')
from hd_inv.prems have t1: "Γ ⊢ e : REAL" and t2: "t' = REAL"
by (auto split: pdf_type.split_asm)
have dens: "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. dens_ctxt_measure (V, V', Γ, δ) ρ ⤜ (λσ. expr_sem σ e)) (stock_measure REAL) f"
by (intro hd_inv.IH) (insert hd_inv.prems hd_inv.hyps t1, auto)
with hd_inv and t1 and t2 show ?case
proof (intro expr_has_density_sound_op[where t = REAL])
from t2 have [measurable]: "lift_RealVal inverse ∈ measurable (stock_measure REAL) (stock_measure REAL)"
by (simp split: pdf_type.split_asm)
from dens have Mf[measurable]: "case_prod f ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure REAL)"
by (blast dest: has_parametrized_subprob_densityD)
let ?f = "λρ x. f ρ (op_sem Inverse x) * inverse (extract_real x) ^ 2"
have [measurable]: "extract_real ∈ borel_measurable (stock_measure REAL)" by simp
show "case_prod ?f ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t')" by (simp add: t2)
fix M ρ assume dens': "has_subprob_density M (stock_measure REAL) (f ρ)"
hence space_M: "space M = space (stock_measure REAL)" by (auto dest: has_subprob_densityD)
have "has_density (distr M (stock_measure t') (lift_RealVal inverse)) (stock_measure t')
((λx. f ρ (RealVal (inverse x)) * ennreal (inverse (x * x)))
∘ extract_real)" (is "has_density _ _ ?f'") using dens'
apply (simp only: t2)
apply (rule distr_lift_RealVal)
apply (auto intro!: subprob_density_distr_real_inverse intro: has_subprob_density_imp_has_density
simp del: inverse_mult_distrib)
done
also have "?f' = ?f ρ"
by (intro ext) (simp add: o_def lift_RealVal_def extract_real_def power2_eq_square split: val.split)
finally show "has_density (distr M (stock_measure t') (op_sem Inverse)) (stock_measure t') ..."
by simp
qed auto
next
case (hd_addc V V' Γ δ e f e' t)
interpret density_context V V' Γ δ by fact
from hd_addc.prems have t1: "Γ ⊢ e : t" and t2: "Γ ⊢ e' : t" and t_disj: "t = REAL ∨ t = INTEG"
by (elim expr_typing_opE, (auto split: pdf_type.split_asm)[])+
hence t4: "op_type Add (PRODUCT t t) = Some t" by auto
have dens: "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. dens_ctxt_measure (V,V',Γ,δ) ρ ⤜ (λσ. expr_sem σ e)) (stock_measure t) f"
by (rule hd_addc.IH) (insert hd_addc.prems t1, auto)
show ?case (is "has_parametrized_subprob_density _ ?N _ ?f")
proof (unfold has_parametrized_subprob_density_def has_subprob_density_def, intro conjI ballI)
from t2 t_disj hd_addc.prems hd_addc.hyps
show "case_prod ?f ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t)"
by (intro addc_density_measurable has_parametrized_subprob_densityD[OF dens]) auto
fix ρ assume ρ: "ρ ∈ space (state_measure V' Γ)"
let ?M = "dens_ctxt_measure (V, V', Γ, δ) ρ"
let ?v1 = "extract_int (expr_sem_rf ρ e')" and ?v2 = "extract_real (expr_sem_rf ρ e')"
from dens and ρ have dens': "has_subprob_density (?M ⤜ (λσ. expr_sem σ e)) (stock_measure t) (f ρ)"
unfolding has_parametrized_subprob_density_def has_subprob_density_def by auto
have Me: "(λσ. expr_sem σ e) ∈
measurable (state_measure (V ∪ V') Γ) (subprob_algebra (stock_measure t))"
using t1 hd_addc.prems by (intro measurable_expr_sem) simp_all
from hd_addc.prems hd_addc.hyps ρ have vt_e': "val_type (expr_sem_rf ρ e') = t"
by (intro val_type_expr_sem_rf[OF t2]) auto
have space_e: "space (?M ⤜ (λσ. expr_sem σ e)) = type_universe t"
by (subst space_bind_measurable, subst measurable_dens_ctxt_measure_eq)
(rule Me, simp, simp add:)
from hd_addc.prems show "subprob_space (?N ρ)"
by (intro subprob_space_bind subprob_space_dens[OF ρ],
subst measurable_dens_ctxt_measure_eq)
(rule measurable_expr_sem, auto)
let ?N' = "distr (?M ⤜ (λσ. expr_sem σ e)) (stock_measure t)
(lift_RealIntVal ((+) ?v1) ((+) ?v2))"
have "has_density ?N' (stock_measure t) (?f ρ)" using t_disj
proof (elim disjE)
assume t: "t = REAL"
let ?N'' = "distr (?M ⤜ (λσ. expr_sem σ e)) (stock_measure t) (lift_RealVal ((+) ?v2))"
let ?f' = "(λx. f ρ (RealVal (x - ?v2))) ∘ extract_real"
from dens' have "has_density ?N'' (stock_measure t) ?f'"
by (subst (1 2) t, intro distr_lift_RealVal)
(auto simp: t intro!: distr_plus_real dest: has_subprob_density_imp_has_density)
also have "?N'' = ?N'"
by (intro distr_cong)
(auto simp: lift_RealVal_def lift_RealIntVal_def extract_real_def vt_e' space_e t
dest: split: val.split)
also have "has_density ?N' (stock_measure t) ?f' = has_density ?N' (stock_measure t) (?f ρ)"
using vt_e' by (intro has_density_cong)
(auto simp: lift_RealIntVal_def t extract_real_def space_embed_measure
lift_RealIntVal2_def split: val.split)
finally show "has_density ?N' (stock_measure t) (?f ρ)" .
next
assume t: "t = INTEG"
let ?N'' = "distr (?M ⤜ (λσ. expr_sem σ e)) (stock_measure t) (lift_IntVal ((+) ?v1))"
let ?f' = "(λx. f ρ (IntVal (x - ?v1))) ∘ extract_int"
from dens' have "has_density ?N'' (stock_measure t) ?f'"
by (subst (1 2) t, intro distr_lift_IntVal)
(auto simp: t intro!: distr_plus_ring_count_space dest: has_subprob_density_imp_has_density)
also have "?N'' = ?N'"
by (intro distr_cong)
(auto simp: lift_IntVal_def lift_RealIntVal_def extract_real_def vt_e' space_e t
split: val.split)
also have "has_density ?N' (stock_measure t) ?f' = has_density ?N' (stock_measure t) (?f ρ)"
using vt_e' by (intro has_density_cong)
(auto simp: lift_RealIntVal_def t extract_int_def space_embed_measure
lift_RealIntVal2_def split: val.split)
finally show "has_density ?N' (stock_measure t) (?f ρ)" .
qed
also have "?N' = distr (?M ⤜ (λσ. expr_sem σ e)) (stock_measure t)
(λw. op_sem Add <|w, expr_sem_rf ρ e'|>)" using t_disj vt_e'
by (intro distr_cong, simp, simp)
(auto split: val.split simp: lift_RealIntVal_def
lift_RealIntVal2_def space_e extract_real_def extract_int_def)
also have "... = ?N ρ"
using hd_addc.prems hd_addc.hyps t_disj ρ
by (intro bin_op_randomfree_restructure[OF t1 t2, symmetric]) auto
finally show "has_density (?N ρ) (stock_measure t) (?f ρ)" .
qed
next
case (hd_multc V V' Γ δ e f c t)
interpret density_context V V' Γ δ by fact
from hd_multc.prems hd_multc.hyps
have t1: "Γ ⊢ e : REAL" and t2: "val_type c = REAL" and t: "t = REAL"
by (elim expr_typing_opE expr_typing_valE expr_typing_pairE,
(auto split: pdf_type.split_asm) [])+
have t4: "op_type Mult (PRODUCT REAL REAL) = Some REAL" by simp
have dens[measurable]: "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. dens_ctxt_measure (V,V',Γ,δ) ρ ⤜ (λσ. expr_sem σ e)) (stock_measure t) f"
by (rule hd_multc.IH) (insert hd_multc.prems t1 t, auto)
show ?case (is "has_parametrized_subprob_density _ ?N _ ?f")
proof (unfold has_parametrized_subprob_density_def has_subprob_density_def, intro conjI ballI)
let ?MR = "stock_measure t" and ?MP = "stock_measure (PRODUCT t t)"
have M_mult[measurable]: "(op_sem Mult) ∈ measurable ?MP ?MR" by (simp add: measurable_op_sem t)
show "case_prod ?f ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t)"
by measurable (insert t2, auto simp: t val_type_eq_REAL lift_RealVal_def)
fix ρ assume ρ: "ρ ∈ space (state_measure V' Γ)"
let ?M = "dens_ctxt_measure (V, V', Γ, δ) ρ"
from dens and ρ have dens': "has_subprob_density (?M ⤜ (λσ. expr_sem σ e)) (stock_measure t) (f ρ)"
unfolding has_parametrized_subprob_density_def has_subprob_density_def by auto
have Me: "(λσ. expr_sem σ e) ∈
measurable (state_measure (V ∪ V') Γ) (subprob_algebra (stock_measure REAL))"
using t1 hd_multc.prems by (intro measurable_expr_sem) simp_all
have space_e: "space (?M ⤜ (λσ. expr_sem σ e)) = range RealVal"
by (subst space_bind_measurable, subst measurable_dens_ctxt_measure_eq)
(rule Me, simp, simp add: t space_embed_measure type_universe_REAL)
from hd_multc.prems show "subprob_space (?N ρ)"
by (intro subprob_space_bind subprob_space_dens[OF ρ],
subst measurable_dens_ctxt_measure_eq)
(rule measurable_expr_sem, auto)
let ?N' = "distr (?M ⤜ (λσ. expr_sem σ e)) (stock_measure t)
(lift_RealVal ((*) (extract_real c)))"
let ?g = "λf x. f (x / extract_real c) * ennreal (inverse (abs (extract_real c)))"
let ?f' = "(λx. f ρ (RealVal (x / extract_real c)) *
inverse (abs (extract_real c))) ∘ extract_real"
from hd_multc.hyps have "extract_real c ≠ 0"
by (auto simp: extract_real_def split: val.split)
with dens' have "has_density ?N' (stock_measure REAL) ?f'"
by (subst t, intro distr_lift_RealVal[where g = ?g])
(auto simp: t intro!: distr_mult_real dest: has_subprob_density_imp_has_density)
also have "has_density ?N' (stock_measure REAL) ?f' =
has_density ?N' (stock_measure REAL) (?f ρ)"
using hd_multc.hyps
by (intro has_density_cong)
(auto simp: lift_RealVal_def t extract_real_def space_embed_measure
lift_RealIntVal2_def field_simps split: val.split)
finally have "has_density ?N' (stock_measure REAL) (?f ρ)" .
also have "?N' = distr (?M ⤜ (λσ. expr_sem σ e)) (stock_measure t)
(λw. op_sem Mult <|w, expr_sem_rf ρ (Val c)|>)" using hd_multc.hyps
by (intro distr_cong, simp, simp)
(auto simp: lift_RealVal_def lift_RealIntVal2_def space_e extract_real_def
split: val.split)
also have "... = ?N ρ"
using hd_multc.prems hd_multc.hyps ρ
by (intro bin_op_randomfree_restructure[OF t1, symmetric])
(auto simp: t intro!: expr_typing.intros)
finally show "has_density (?N ρ) (stock_measure t) (?f ρ)" by (simp only: t)
qed
next
case (hd_add V V' Γ δ e f t)
interpret density_context V V' Γ δ by fact
from hd_add.prems hd_add.hyps
have t1: "Γ ⊢ e : PRODUCT t t" and t2: "op_type Add (PRODUCT t t) = Some t" and
t_disj: "t = REAL ∨ t = INTEG"
by (elim expr_typing_opE expr_typing_valE expr_typing_pairE,
(auto split: pdf_type.split_asm) [])+
let ?tp = "PRODUCT t t"
have dens[measurable]: "has_parametrized_subprob_density (state_measure V' Γ)
(λρ. dens_ctxt_measure (V,V',Γ,δ) ρ ⤜ (λσ. expr_sem σ e)) (stock_measure ?tp) f"
by (rule hd_add.IH) (insert hd_add.prems t1 t2 t_disj, auto)
from hd_add.prems hd_add.hyps t1 t2 t_disj show ?case (is "has_parametrized_subprob_density _ ?N _ ?f")
proof (intro expr_has_density_sound_op[OF _ dens])
note sigma_finite_measure.borel_measurable_nn_integral[OF sigma_finite_stock_measure, measurable]
have [measurable]: "op_type Minus t = Some t"
using t_disj by auto
note measurable_op_sem[measurable] t2[measurable]
let ?f' = "λρ z. ∫⇧+ x. f ρ <|x , op_sem Add <|z, op_sem Minus x|>|> ∂stock_measure t"
have "case_prod ?f' ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t)"
by measurable
also have "case_prod ?f' ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t) ⟷
case_prod ?f ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t)"
by (intro measurable_cong) (auto simp: space_pair_measure)
finally show "case_prod ?f ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t)" .
fix M ρ assume dens': "has_subprob_density M (stock_measure (PRODUCT t t)) (f ρ)"
hence Mf[measurable]: "f ρ ∈ borel_measurable (stock_measure (PRODUCT t t))" by (rule has_subprob_densityD)
let ?M = "dens_ctxt_measure (V, V', Γ, δ) ρ"
show "has_density (distr M (stock_measure t) (op_sem Add)) (stock_measure t) (?f ρ)"
proof (insert t_disj, elim disjE)
assume t: "t = REAL"
let ?f'' = "(λz. ∫⇧+x. f ρ (RealPairVal (x, z - x)) ∂lborel) ∘ extract_real"
have "has_density (distr M (stock_measure t) (op_sem Add)) (stock_measure t) ?f''"
using dens'
by (simp only: t op_sem.simps, intro distr_lift_RealPairVal)
(simp_all add: borel_prod[symmetric] has_subprob_density_imp_has_density
distr_convolution_real)
also have "?f'' = (λz. ∫⇧+ x. f ρ (RealPairVal (x, extract_real z - x)) ∂lborel)"
(is "_ = ?f''")
by (auto simp add: t space_embed_measure extract_real_def)
also have "⋀z. val_type z = REAL ⟹
(λx. f ρ <|x, op_sem Add <|z, op_sem Minus x|>|>) ∈ borel_measurable (stock_measure REAL)"
by (rule Mf[THEN measurable_compose_rev]) (simp add: t)
hence "has_density (distr M (stock_measure t) (op_sem Add)) (stock_measure t) ?f'' ⟷
has_density (distr M (stock_measure t) (op_sem Add)) (stock_measure t) (?f ρ)"
by (intro has_density_cong, simp add: t space_embed_measure del: op_sem.simps)
(auto simp add: nn_integral_RealVal RealPairVal_def lift_RealIntVal2_def lift_RealIntVal_def val_type_eq_REAL)
finally show "..." .
next
assume t: "t = INTEG"
let ?f'' = "(λz. ∫⇧+x. f ρ (IntPairVal (x, z - x)) ∂count_space UNIV) ∘ extract_int"
have "has_density (distr M (stock_measure t) (op_sem Add)) (stock_measure t) ?f''"
using dens'
by (simp only: t op_sem.simps, intro distr_lift_IntPairVal)
(simp_all add: has_subprob_density_imp_has_density
distr_convolution_ring_count_space)
also have "?f'' = (λz. ∫⇧+ x. f ρ (IntPairVal (x, extract_int z - x)) ∂count_space UNIV)"
(is "_ = ?f''")
by (auto simp add: t space_embed_measure extract_int_def)
also have "has_density (distr M (stock_measure t) (op_sem Add)) (stock_measure t) ?f'' ⟷
has_density (distr M (stock_measure t) (op_sem Add)) (stock_measure t) (?f ρ)"
by (intro has_density_cong, simp add: t space_embed_measure del: op_sem.simps)
(auto simp: nn_integral_IntVal IntPairVal_def val_type_eq_INTEG
lift_RealIntVal2_def lift_RealIntVal_def)
finally show "..." .
qed
qed
qed
lemma hd_cong:
assumes "(V,V',Γ,δ) ⊢⇩d e ⇒ f" "density_context V V' Γ δ" "Γ ⊢ e : t" "free_vars e ⊆ V ∪ V'"
assumes "⋀ρ x. ρ ∈ space (state_measure V' Γ) ⟹ x ∈ space (stock_measure t) ⟹ f ρ x = f' ρ x"
shows "(V,V',Γ,δ) ⊢⇩d e ⇒ f'"
proof (rule hd_AE[OF assms(1,3) AE_I2[OF assms(5)]])
note dens = expr_has_density_sound_aux[OF assms(1,3,2,4)]
note dens' = has_parametrized_subprob_densityD[OF this]
show "(λ(ρ, x). f' ρ x) ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure t)"
using assms(5) dens'(3)
by (subst measurable_cong[of _ _ "case_prod f"]) (auto simp: space_pair_measure)
qed auto
lemma prob_space_empty_dens_ctxt[simp]:
"prob_space (dens_ctxt_measure ({},{},Γ,(λ_. 1)) (λ_. undefined))"
unfolding density_context_def
by (auto simp: dens_ctxt_measure_def state_measure'_def state_measure_def
emeasure_distr emeasure_density PiM_empty intro!: prob_spaceI)
lemma branch_prob_empty_ctxt[simp]: "branch_prob ({},{},Γ,(λ_. 1)) (λ_. undefined) = 1"
unfolding branch_prob_def by (subst prob_space.emeasure_space_1) simp_all
lemma expr_has_density_sound:
assumes "({},{},Γ,(λ_. 1)) ⊢⇩d e ⇒ f" "Γ ⊢ e : t" "free_vars e = {}"
shows "has_subprob_density (expr_sem σ e) (stock_measure t) (f (λ_. undefined))"
proof-
let ?M = "dens_ctxt_measure ({},{},Γ,λ_. 1) (λ_. undefined)"
have "density_context {} {} Γ (λ_. 1)"
unfolding density_context_def
by (auto simp: dens_ctxt_measure_def state_measure'_def state_measure_def
emeasure_distr emeasure_density PiM_empty intro!: subprob_spaceI)
from expr_has_density_sound_aux[OF assms(1,2) this] assms(3)
have "has_parametrized_subprob_density (state_measure {} Γ)
(λρ. dens_ctxt_measure ({},{},Γ,λ_. 1) ρ ⤜ (λσ. expr_sem σ e)) (stock_measure t) f"
by blast
also have "state_measure {} Γ = count_space {λ_. undefined}"
by (rule measure_eqI) (simp_all add: state_measure_def PiM_empty emeasure_density)
finally have "has_subprob_density (?M ⤜ (λσ. expr_sem σ e))
(stock_measure t) (f (λ_. undefined))"
unfolding has_parametrized_subprob_density_def by simp
also from assms have "(λσ. expr_sem σ e) ∈ measurable (state_measure {} Γ)
(subprob_algebra (stock_measure t))"
by (intro measurable_expr_sem) auto
hence "?M ⤜ (λσ. expr_sem σ e) = expr_sem (λ_. undefined) e"
by (intro dens_ctxt_measure_empty_bind) (auto simp: state_measure_def PiM_empty)
also from assms have "... = expr_sem σ e" by (intro expr_sem_eq_on_vars) auto
finally show ?thesis .
qed
end