Theory PDF_Compiler
section ‹Concrete PDF Compiler›
theory PDF_Compiler
imports PDF_Compiler_Pred PDF_Target_Density_Contexts
begin
inductive expr_has_density_cexpr :: "cdens_ctxt ⇒ expr ⇒ cexpr ⇒ bool"
(‹(1_/ ⊢⇩c/ (_ ⇒/ _))› [50,0,50] 50) where
edc_val: "countable_type (val_type v) ⟹
(vs, vs', Γ, δ) ⊢⇩c Val v ⇒
map_vars Suc (branch_prob_cexpr (vs, vs', Γ, δ)) *⇩c ⟨CVar 0 =⇩c CVal v⟩⇩c"
| edc_var: "x ∈ set vs ⟹ (vs, vs', Γ, δ) ⊢⇩c Var x ⇒ marg_dens_cexpr Γ vs x δ"
| edc_pair: "x ∈ set vs ⟹ y ∈ set vs ⟹ x ≠ y ⟹
(vs, vs', Γ, δ) ⊢⇩c <Var x, Var y> ⇒ marg_dens2_cexpr Γ vs x y δ"
| edc_fail: "(vs, vs', Γ, δ) ⊢⇩c Fail t ⇒ CReal 0"
| edc_let: "([], vs @ vs', Γ, CReal 1) ⊢⇩c e ⇒ f ⟹
(shift_vars vs, map Suc vs', the (expr_type Γ e) ⋅ Γ,
map_vars Suc δ *⇩c f) ⊢⇩c e' ⇒ g ⟹
(vs, vs', Γ, δ) ⊢⇩c LET e IN e' ⇒ map_vars (λx. x - 1) g"
| edc_rand: "(vs, vs', Γ, δ) ⊢⇩c e ⇒ f ⟹
(vs, vs', Γ, δ) ⊢⇩c Random dst e ⇒
∫⇩c map_vars (case_nat 0 (λx. x + 2)) f *⇩c
dist_dens_cexpr dst (CVar 0) (CVar 1) ∂dist_param_type dst"
| edc_rand_det: "randomfree e ⟹ free_vars e ⊆ set vs' ⟹
(vs, vs', Γ, δ) ⊢⇩c Random dst e ⇒
map_vars Suc (branch_prob_cexpr (vs, vs', Γ, δ)) *⇩c
dist_dens_cexpr dst (map_vars Suc (expr_rf_to_cexpr e)) (CVar 0)"
| edc_if_det: "randomfree b ⟹
(vs, vs', Γ, δ *⇩c ⟨expr_rf_to_cexpr b⟩⇩c) ⊢⇩c e1 ⇒ f1 ⟹
(vs, vs', Γ, δ *⇩c ⟨¬⇩c expr_rf_to_cexpr b⟩⇩c) ⊢⇩c e2 ⇒ f2 ⟹
(vs, vs', Γ, δ) ⊢⇩c IF b THEN e1 ELSE e2 ⇒ f1 +⇩c f2"
| edc_if: "([], vs @ vs', Γ, CReal 1) ⊢⇩c b ⇒ f ⟹
(vs, vs', Γ, δ *⇩c cexpr_subst_val f TRUE) ⊢⇩c e1 ⇒ g1 ⟹
(vs, vs', Γ, δ *⇩c cexpr_subst_val f FALSE) ⊢⇩c e2 ⇒ g2 ⟹
(vs, vs', Γ, δ) ⊢⇩c IF b THEN e1 ELSE e2 ⇒ g1 +⇩c g2"
| edc_op_discr: "(vs, vs', Γ, δ) ⊢⇩c e ⇒ f ⟹ Γ ⊢ e : t ⟹
op_type oper t = Some t' ⟹ countable_type t' ⟹
(vs, vs', Γ, δ) ⊢⇩c oper $$ e ⇒
∫⇩c ⟨(oper $$⇩c (CVar 0)) =⇩c CVar 1⟩⇩c *⇩c map_vars (case_nat 0 (λx. x+2)) f ∂t"
| edc_fst: "(vs, vs', Γ, δ) ⊢⇩c e ⇒ f ⟹ Γ ⊢ e : PRODUCT t t' ⟹
(vs, vs', Γ, δ) ⊢⇩c Fst $$ e ⇒
∫⇩c (map_vars (case_nat 0 (λx. x + 2)) f ∘⇩c <CVar 1, CVar 0>⇩c) ∂t'"
| edc_snd: "(vs, vs', Γ, δ) ⊢⇩c e ⇒ f ⟹ Γ ⊢ e : PRODUCT t t' ⟹
(vs, vs', Γ, δ) ⊢⇩c Snd $$ e ⇒
∫⇩c (map_vars (case_nat 0 (λx. x + 2)) f ∘⇩c <CVar 0, CVar 1>⇩c) ∂t"
| edc_neg: "(vs, vs', Γ, δ) ⊢⇩c e ⇒ f ⟹
(vs, vs', Γ, δ) ⊢⇩c Minus $$ e ⇒ f ∘⇩c (λ⇩cx. -⇩c x)"
| edc_addc: "(vs, vs', Γ, δ) ⊢⇩c e ⇒ f ⟹ randomfree e' ⟹ free_vars e' ⊆ set vs' ⟹
(vs, vs', Γ, δ) ⊢⇩c Add $$ <e, e'> ⇒
f ∘⇩c (λ⇩cx. x -⇩c map_vars Suc (expr_rf_to_cexpr e'))"
| edc_multc: "(vs, vs', Γ, δ) ⊢⇩c e ⇒ f ⟹ c ≠ 0 ⟹
(vs, vs', Γ, δ) ⊢⇩c Mult $$ <e, Val (RealVal c)> ⇒
(f ∘⇩c (λ⇩cx. x *⇩c CReal (inverse c))) *⇩c CReal (inverse (abs c))"
| edc_add: "(vs, vs', Γ, δ) ⊢⇩c e ⇒ f ⟹ Γ ⊢ e : PRODUCT t t ⟹
(vs, vs', Γ, δ) ⊢⇩c Add $$ e ⇒
∫⇩c (map_vars (case_nat 0 (λx. x+2)) f ∘⇩c (λ⇩cx. <x, CVar 1 -⇩c x>⇩c)) ∂t"
| edc_inv: "(vs, vs', Γ, δ) ⊢⇩c e ⇒ f ⟹
(vs, vs', Γ, δ) ⊢⇩c Inverse $$ e ⇒
(f ∘⇩c (λ⇩cx. inverse⇩c x)) *⇩c (λ⇩cx. (inverse⇩c x) ^⇩c CInt 2)"
| edc_exp: "(vs, vs', Γ, δ) ⊢⇩c e ⇒ f ⟹
(vs, vs', Γ, δ) ⊢⇩c Exp $$ e ⇒
(λ⇩cx. IF⇩c CReal 0 <⇩c x THEN (f ∘⇩c ln⇩c x) *⇩c inverse⇩c x ELSE CReal 0)"
code_pred expr_has_density_cexpr .
text ‹Auxiliary lemmas›
lemma cdens_ctxt_invar_insert:
assumes inv: "cdens_ctxt_invar vs vs' Γ δ"
assumes t : "Γ ⊢ e : t'"
assumes free_vars: "free_vars e ⊆ set vs ∪ set vs'"
assumes hd: "dens_ctxt_α ([], vs @ vs', Γ, CReal 1) ⊢⇩d e ⇒ (λx xa. ennreal (eval_cexpr f x xa))"
notes invar = cdens_ctxt_invarD[OF inv]
assumes wf1: "is_density_expr ([], vs @ vs', Γ, CReal 1) t' f"
shows "cdens_ctxt_invar (shift_vars vs) (map Suc vs') (t' ⋅ Γ) (map_vars Suc δ *⇩c f)"
proof (intro cdens_ctxt_invarI)
show t': "case_nat t' Γ ⊢⇩c map_vars Suc δ *⇩c f : REAL" using invar wf1
by (intro cet_op[where t = "PRODUCT REAL REAL"])
(auto intro!: cexpr_typing.intros cexpr_typing_map_vars simp: o_def dest: is_density_exprD)
let ?vs = "shift_var_set (set vs)" and ?vs' = "Suc ` set vs'" and ?Γ = "case_nat t' Γ" and
?δ = "insert_dens (set vs) (set vs') (λσ x. ennreal (eval_cexpr f σ x))
(λx. ennreal (extract_real (cexpr_sem x δ)))"
interpret density_context "set vs" "set vs'" Γ "λσ. extract_real (cexpr_sem σ δ)"
by (rule density_context_α[OF inv])
have dc: "density_context {} (set vs ∪ set vs') Γ (λ_. 1)"
by (rule density_context_empty)
hence dens: "has_parametrized_subprob_density (state_measure (set vs ∪ set vs') Γ)
(λρ. dens_ctxt_measure ({}, set vs ∪ set vs', Γ, λ_. 1) ρ ⤜ (λσ. expr_sem σ e))
(stock_measure t') (λσ x. ennreal (eval_cexpr f σ x))"
using hd free_vars by (intro expr_has_density_sound_aux[OF _ t dc])
(auto simp: shift_var_set_def dens_ctxt_α_def simp: extract_real_def one_ennreal_def)
from density_context.density_context_insert[OF density_context_α[OF inv] this]
have "density_context ?vs ?vs' ?Γ ?δ" .
have dc: "density_context (shift_var_set (set vs)) (Suc ` set vs') (case_nat t' Γ)
(λσ. extract_real (cexpr_sem σ (map_vars Suc δ *⇩c f)))"
proof (rule density_context_equiv)
show "density_context (shift_var_set (set vs)) (Suc ` set vs') (case_nat t' Γ) ?δ" by fact
show "(λx. ennreal (extract_real (cexpr_sem x (map_vars Suc δ *⇩c f))))
∈ borel_measurable (state_measure (?vs ∪ ?vs') ?Γ)"
apply (rule measurable_compose[OF _ measurable_ennreal], rule measurable_compose[OF _ measurable_extract_real])
apply (rule measurable_cexpr_sem[OF t'])
apply (insert invar is_density_exprD[OF wf1], auto simp: shift_var_set_def)
done
next
fix σ assume σ: "σ ∈ space (state_measure (?vs ∪ ?vs') ?Γ)"
have [simp]: "case_nat (σ 0) (λx. σ (Suc x)) = σ" by (intro ext) (simp split: nat.split)
from σ show "insert_dens (set vs) (set vs') (λσ x. ennreal (eval_cexpr f σ x))
(λx. ennreal (extract_real (cexpr_sem x δ))) σ =
ennreal (extract_real (cexpr_sem σ (map_vars Suc δ *⇩c f)))"
unfolding insert_dens_def using invar is_density_exprD[OF wf1]
apply (subst ennreal_mult'[symmetric])
apply (erule nonneg_cexprD)
apply (rule measurable_space[OF measurable_remove_var[where t=t']])
apply simp
apply (subst cexpr_sem_Mult[of ?Γ _ _ _ "?vs ∪ ?vs'"])
apply (auto intro!: cexpr_typing_map_vars ennreal_mult'[symmetric]
simp: o_def shift_var_set_def eval_cexpr_def
cexpr_sem_map_vars remove_var_def)
done
qed
from subprob_imp_subprob_cexpr[OF this]
show "subprob_cexpr (set (shift_vars vs)) (set (map Suc vs')) (case_nat t' Γ)
(map_vars Suc δ *⇩c f)" by simp
have "Suc -` shift_var_set (set vs ∪ set vs') = set vs ∪ set vs'"
by (auto simp: shift_var_set_def)
moreover have "nonneg_cexpr (shift_var_set (set vs ∪ set vs')) (case_nat t' Γ) f"
using wf1[THEN is_density_exprD_nonneg] by simp
ultimately show "nonneg_cexpr (set (shift_vars vs) ∪ set (map Suc vs')) (case_nat t' Γ) (map_vars Suc δ *⇩c f)"
using invar is_density_exprD[OF wf1]
by (intro nonneg_cexpr_Mult)
(auto intro!: cexpr_typing_map_vars nonneg_cexpr_map_vars
simp: o_def shift_var_set_def image_Un)
qed (insert invar is_density_exprD[OF wf1],
auto simp: shift_vars_def shift_var_set_def distinct_map intro!: cexpr_typing_map_vars)
lemma cdens_ctxt_invar_insert_bool:
assumes dens: "dens_ctxt_α ([], vs @ vs', Γ, CReal 1) ⊢⇩d b ⇒ (λρ x. ennreal (eval_cexpr f ρ x))"
assumes wf: "is_density_expr ([], vs @ vs', Γ, CReal 1) BOOL f"
assumes t: "Γ ⊢ b : BOOL" and vars: "free_vars b ⊆ set vs ∪ set vs'"
assumes invar: "cdens_ctxt_invar vs vs' Γ δ"
shows "cdens_ctxt_invar vs vs' Γ (δ *⇩c cexpr_subst_val f (BoolVal v))"
proof (intro cdens_ctxt_invarI nonneg_cexpr_Mult nonneg_cexpr_subst_val)
note invar' = cdens_ctxt_invarD[OF invar] and wf' = is_density_exprD[OF wf]
show "Γ ⊢⇩c δ *⇩c cexpr_subst_val f (BoolVal v) : REAL" using invar' wf'
by (intro cet_op[where t = "PRODUCT REAL REAL"] cet_pair cexpr_typing_subst_val) simp_all
let ?M = "λρ. dens_ctxt_measure ({}, set vs ∪ set vs', Γ, λ_. 1) ρ ⤜ (λσ. expr_sem σ b)"
have dens': "has_parametrized_subprob_density (state_measure (set vs ∪ set vs') Γ) ?M
(stock_measure BOOL) (λσ v. ennreal (eval_cexpr f σ v))"
using density_context_α[OF invar] t vars dens unfolding dens_ctxt_α_def
by (intro expr_has_density_sound_aux density_context.density_context_empty)
(auto simp: extract_real_def one_ennreal_def)
thus nonneg: "nonneg_cexpr (shift_var_set (set vs ∪ set vs')) (case_nat BOOL Γ) f"
using wf[THEN is_density_exprD_nonneg] by simp
show "subprob_cexpr (set vs) (set vs') Γ (δ *⇩c cexpr_subst_val f (BoolVal v))"
proof (intro subprob_cexprI)
fix ρ assume ρ: "ρ ∈ space (state_measure (set vs') Γ)"
let ?eval = "λe σ. extract_real (cexpr_sem (merge (set vs) (set vs') (σ, ρ)) e)"
{
fix σ assume σ : "σ ∈ space (state_measure (set vs) Γ)"
have A: "?eval (δ *⇩c cexpr_subst_val f (BoolVal v)) σ =
?eval δ σ * ?eval (cexpr_subst_val f (BoolVal v)) σ" using wf' invar' σ ρ
by (subst cexpr_sem_Mult[where Γ = Γ and V = "set vs ∪ set vs'"])
(auto intro: merge_in_state_measure simp: shift_var_set_def)
have "?eval δ σ ≥ 0" using σ ρ invar'
by (blast dest: nonneg_cexprD intro: merge_in_state_measure)
moreover have "?eval (cexpr_subst_val f (BoolVal v)) σ ≥ 0" using σ ρ nonneg
by (intro nonneg_cexprD nonneg_cexpr_subst_val) (auto intro: merge_in_state_measure)
moreover have B: "ennreal (?eval (cexpr_subst_val f (BoolVal v)) σ) =
ennreal (eval_cexpr f (merge (set vs) (set vs') (σ, ρ)) (BoolVal v))"
(is "_ = ?f (BoolVal v)") by (simp add: eval_cexpr_def)
hence "ennreal (?eval (cexpr_subst_val f (BoolVal v)) σ) ≤ 1"
using σ ρ dens' unfolding has_parametrized_subprob_density_def
by (subst B, intro subprob_count_space_density_le_1[of _ _ ?f])
(auto intro: merge_in_state_measure simp: stock_measure.simps)
ultimately have "?eval (δ *⇩c cexpr_subst_val f (BoolVal v)) σ ≤ ?eval δ σ"
by (subst A, intro mult_right_le_one_le) simp_all
}
hence "(∫⇧+σ. ?eval (δ *⇩c cexpr_subst_val f (BoolVal v)) σ ∂state_measure (set vs) Γ) ≤
(∫⇧+σ. ?eval δ σ ∂state_measure (set vs) Γ)" by (intro nn_integral_mono) (simp add: ennreal_leI)
also have "... ≤ 1" using invar' ρ by (intro subprob_cexprD)
finally show "(∫⇧+σ. ?eval (δ *⇩c cexpr_subst_val f (BoolVal v)) σ ∂state_measure (set vs) Γ) ≤ 1" .
qed
qed (insert cdens_ctxt_invarD[OF invar] is_density_exprD[OF wf],
auto simp: shift_var_set_def)
lemma space_state_measureD_shift:
"σ ∈ space (state_measure (shift_var_set V) (case_nat t Γ)) ⟹
∃x σ'. x ∈ type_universe t ∧ σ' ∈ space (state_measure V Γ) ∧ σ = case_nat x σ' "
by (intro exI[of _ "σ 0"] exI[of _ "σ ∘ Suc"])
(auto simp: fun_eq_iff PiE_iff space_state_measure extensional_def split: nat.split)
lemma space_state_measure_shift_iff:
"σ ∈ space (state_measure (shift_var_set V) (case_nat t Γ)) ⟷
(∃x σ'. x ∈ type_universe t ∧ σ' ∈ space (state_measure V Γ) ∧ σ = case_nat x σ')"
by (auto dest!: space_state_measureD_shift)
lemma nonneg_cexprI_shift:
assumes "⋀x σ. x ∈ type_universe t ⟹ σ ∈ space (state_measure V Γ) ⟹
0 ≤ extract_real (cexpr_sem (case_nat x σ) e)"
shows "nonneg_cexpr (shift_var_set V) (case_nat t Γ) e"
by (auto intro!: nonneg_cexprI assms dest!: space_state_measureD_shift)
lemma nonneg_cexpr_shift_iff:
"nonneg_cexpr (shift_var_set V) (case_nat t Γ) (map_vars Suc e) ⟷ nonneg_cexpr V Γ e"
apply (auto simp: cexpr_sem_map_vars o_def nonneg_cexpr_def space_state_measure_shift_iff)
subgoal for σ
apply (drule bspec[of _ _ "case_nat (SOME x. x ∈ type_universe t) σ"])
using type_universe_nonempty[of t]
unfolding ex_in_conv[symmetric]
apply (auto intro!: case_nat_in_state_measure intro: someI)
done
done
lemma case_nat_case_nat: "case_nat x n (case_nat y m i) = case_nat (case_nat x n y) (λi'. case_nat x n (m i')) i"
by (rule nat.case_distrib)
lemma nonneg_cexpr_shift_iff2:
"nonneg_cexpr (shift_var_set (shift_var_set V))
(case_nat t1 (case_nat t2 Γ)) (map_vars (case_nat 0 (λx. Suc (Suc x))) e) ⟷
nonneg_cexpr (shift_var_set V) (case_nat t1 Γ) e"
apply (auto simp: cexpr_sem_map_vars o_def nonneg_cexpr_def space_state_measure_shift_iff)
subgoal for x σ
apply (drule bspec[of _ _ "case_nat x (case_nat (SOME x. x ∈ type_universe t2) σ)"])
using type_universe_nonempty[of t2]
unfolding ex_in_conv[symmetric]
apply (auto simp: case_nat_case_nat cong: nat.case_cong
intro!: case_nat_in_state_measure intro: someI_ex someI)
done
apply (erule bspec)
subgoal for x1 x2 σ
by (auto simp add: space_state_measure_shift_iff fun_eq_iff split: nat.split
intro!: exI[of _ x1] exI[of _ σ])
done
lemma nonneg_cexpr_Add:
assumes "Γ ⊢⇩c e1 : REAL" "Γ ⊢⇩c e2 : REAL"
assumes "free_vars e1 ⊆ V" "free_vars e2 ⊆ V"
assumes N1: "nonneg_cexpr V Γ e1" and N2: "nonneg_cexpr V Γ e2"
shows "nonneg_cexpr V Γ (e1 +⇩c e2)"
proof (rule nonneg_cexprI)
fix σ assume σ: "σ ∈ space (state_measure V Γ)"
hence "extract_real (cexpr_sem σ (e1 +⇩c e2)) = extract_real (cexpr_sem σ e1) + extract_real (cexpr_sem σ e2)"
using assms by (subst cexpr_sem_Add[of Γ _ _ _ V]) simp_all
also have "... ≥ 0" using σ N1 N2 by (intro add_nonneg_nonneg nonneg_cexprD)
finally show "extract_real (cexpr_sem σ (e1 +⇩c e2)) ≥ 0" .
qed
lemma expr_has_density_cexpr_sound_aux:
assumes "Γ ⊢ e : t" "(vs, vs', Γ, δ) ⊢⇩c e ⇒ f" "cdens_ctxt_invar vs vs' Γ δ"
"free_vars e ⊆ set vs ∪ set vs'"
shows "dens_ctxt_α (vs,vs',Γ,δ) ⊢⇩d e ⇒ eval_cexpr f ∧ is_density_expr (vs,vs',Γ,δ) t f"
using assms(2,1,3,4)
proof (induction arbitrary: t rule: expr_has_density_cexpr.induct[split_format (complete)])
case (edc_val v vs vs' Γ δ)
from edc_val.prems have [simp]: "t = val_type v" by auto
note invar = cdens_ctxt_invarD[OF edc_val.prems(2)]
let ?e1 = "map_vars Suc (branch_prob_cexpr (vs, vs', Γ, δ))" and ?e2 = "⟨CVar 0 =⇩c CVal v⟩⇩c"
have ctype1: "case_nat t Γ ⊢⇩c ?e1 : REAL" and ctype2: "case_nat t Γ ⊢⇩c ?e2: REAL" using invar
by (auto intro!: cexpr_typing.intros cexpr_typing_map_vars simp: o_def)
hence ctype: "case_nat t Γ ⊢⇩c ?e1 *⇩c ?e2 : REAL" by (auto intro!: cexpr_typing.intros)
{
fix ρ x assume x: "x ∈ type_universe (val_type v)"
and ρ: "ρ ∈ space (state_measure (set vs') Γ)"
hence "case_nat x ρ ∈ space (state_measure (shift_var_set (set vs')) (case_nat (val_type v) Γ))"
by (rule case_nat_in_state_measure)
hence "ennreal (eval_cexpr (?e1 *⇩c ?e2) ρ x) =
ennreal (extract_real (cexpr_sem (case_nat x ρ)
(map_vars Suc (branch_prob_cexpr (vs, vs', Γ, δ))))) *
ennreal (extract_real (RealVal (bool_to_real (x = v))))" (is "_ = ?a * ?b")
using invar unfolding eval_cexpr_def
apply (subst ennreal_mult''[symmetric])
apply (simp add: bool_to_real_def)
apply (subst cexpr_sem_Mult[of "case_nat t Γ" _ _ _ "shift_var_set (set vs')"])
apply (insert invar ctype1 ctype2)
apply (auto simp: shift_var_set_def)
done
also have "?a = branch_prob (dens_ctxt_α (vs,vs',Γ,δ)) ρ"
by (subst cexpr_sem_map_vars, subst cexpr_sem_branch_prob) (simp_all add: o_def ρ edc_val.prems)
also have "?b = indicator {v} x"
by (simp add: extract_real_def bool_to_real_def split: split_indicator)
finally have "ennreal (eval_cexpr (?e1 *⇩c ?e2) ρ x) =
branch_prob (dens_ctxt_α (vs,vs',Γ,δ)) ρ * indicator {v} x" .
} note e = this
have meas: "(λ(σ, x). ennreal (eval_cexpr (?e1 *⇩c ?e2) σ x))
∈ borel_measurable (state_measure (set vs') Γ ⨂⇩M stock_measure (val_type v))"
apply (subst measurable_split_conv, rule measurable_compose[OF _ measurable_ennreal])
apply (subst measurable_split_conv[symmetric], rule measurable_eval_cexpr)
apply (insert ctype invar, auto simp: shift_var_set_def)
done
have *: "Suc -` shift_var_set (set vs') = set vs'" "case_nat (val_type v) Γ ∘ Suc = Γ"
by (auto simp: shift_var_set_def)
have nn: "nonneg_cexpr (shift_var_set (set vs')) (case_nat t Γ)
(map_vars Suc (branch_prob_cexpr (vs, vs', Γ, δ)) *⇩c ⟨CVar 0 =⇩c CVal v⟩⇩c)"
using invar ctype1 ctype2
by (fastforce intro!: nonneg_cexpr_Mult nonneg_indicator nonneg_cexpr_map_vars
cexpr_typing.intros nonneg_cexpr_sem_integrate_vars'
simp: branch_prob_cexpr_def *)
show ?case unfolding dens_ctxt_α_def
apply (simp only: prod.case, intro conjI)
apply (rule hd_AE[OF hd_val et_val AE_I2])
apply (insert edc_val, simp_all add: e dens_ctxt_α_def meas) [4]
apply (intro is_density_exprI)
using ctype
apply simp
apply (insert invar nn, auto simp: shift_var_set_def)
done
next
case (edc_var x vs vs' Γ δ t)
hence t: "t = Γ x" by auto
note invar = cdens_ctxt_invarD[OF edc_var.prems(2)]
from invar have ctype: "case_nat t Γ ⊢⇩c marg_dens_cexpr Γ vs x δ : REAL" by (auto simp: t)
show ?case unfolding dens_ctxt_α_def
proof (simp only: prod.case, intro conjI is_density_exprI, rule hd_AE[OF hd_var edc_var.prems(1)])
show "case_nat t Γ ⊢⇩c marg_dens_cexpr Γ vs x δ : REAL" by fact
next
show "free_vars (marg_dens_cexpr Γ vs x δ) ⊆ shift_var_set (set vs')"
using edc_var.prems(2) by (rule free_vars_marg_dens_cexpr)
next
have free_vars: "free_vars (marg_dens_cexpr Γ vs x δ) ⊆ shift_var_set (set vs')"
using edc_var.prems(2) by (rule free_vars_marg_dens_cexpr)
show "(λ(ρ, y). ennreal (eval_cexpr (marg_dens_cexpr Γ vs x δ) ρ y))
∈ borel_measurable (state_measure (set vs') Γ ⨂⇩M stock_measure t)"
apply (subst measurable_split_conv, rule measurable_compose[OF _ measurable_ennreal])
apply (subst measurable_split_conv[symmetric], rule measurable_eval_cexpr)
apply (insert ctype free_vars, auto simp: shift_var_set_def)
done
next
fix ρ assume "ρ ∈ space (state_measure (set vs') Γ)"
hence "AE y in stock_measure t.
marg_dens (dens_ctxt_α (vs, vs', Γ, δ)) x ρ y =
ennreal (eval_cexpr (marg_dens_cexpr Γ vs x δ) ρ y)"
using edc_var unfolding eval_cexpr_def by (subst t, subst eq_commute, intro cexpr_sem_marg_dens)
thus "AE y in stock_measure t.
marg_dens (set vs, set vs', Γ, λx. ennreal (extract_real (cexpr_sem x δ))) x ρ y =
ennreal (eval_cexpr (marg_dens_cexpr Γ vs x δ) ρ y)"
by (simp add: dens_ctxt_α_def)
next
show "x ∈ set vs"
by (insert edc_var.prems edc_var.hyps, auto simp: eval_cexpr_def intro!: nonneg_cexpr_sem_marg_dens)
show "nonneg_cexpr (shift_var_set (set vs')) (case_nat t Γ) (marg_dens_cexpr Γ vs x δ)"
by (intro nonneg_cexprI_shift nonneg_cexpr_sem_marg_dens[OF edc_var.prems(2) ‹x ∈ set vs›])
(auto simp: t)
qed
next
case (edc_pair x vs y vs' Γ δ t)
hence t[simp]: "t = PRODUCT (Γ x) (Γ y)" by auto
note invar = cdens_ctxt_invarD[OF edc_pair.prems(2)]
from invar have ctype: "case_nat t Γ ⊢⇩c marg_dens2_cexpr Γ vs x y δ : REAL" by auto
from edc_pair.prems have vars: "free_vars (marg_dens2_cexpr Γ vs x y δ) ⊆ shift_var_set (set vs')"
using free_vars_marg_dens2_cexpr by simp
show ?case unfolding dens_ctxt_α_def
proof (simp only: prod.case, intro conjI is_density_exprI, rule hd_AE[OF hd_pair edc_pair.prems(1)])
fix ρ assume ρ: "ρ ∈ space (state_measure (set vs') Γ)"
show "AE z in stock_measure t.
marg_dens2 (set vs, set vs', Γ, λx. ennreal (extract_real (cexpr_sem x δ))) x y ρ z =
ennreal (eval_cexpr (marg_dens2_cexpr Γ vs x y δ) ρ z)"
using cexpr_sem_marg_dens2[OF edc_pair.prems(2) edc_pair.hyps ρ] unfolding eval_cexpr_def
by (subst t, subst eq_commute) (simp add: dens_ctxt_α_def)
next
show "nonneg_cexpr (shift_var_set (set vs')) (case_nat t Γ) (marg_dens2_cexpr Γ vs x y δ)"
by (intro nonneg_cexprI_shift nonneg_cexpr_sem_marg_dens2[OF edc_pair.prems(2) ‹x ∈ set vs› ‹y∈set vs›])
auto
qed (insert edc_pair invar ctype vars, auto simp: dens_ctxt_α_def)
next
case (edc_fail vs vs' Γ δ t t')
hence [simp]: "t = t'" by auto
have ctype: "case_nat t' Γ ⊢⇩c CReal 0 : REAL"
by (subst val_type.simps[symmetric]) (rule cexpr_typing.intros)
thus ?case by (auto simp: dens_ctxt_α_def eval_cexpr_def extract_real_def
zero_ennreal_def[symmetric] hd_fail
intro!: is_density_exprI nonneg_cexprI)
next
case (edc_let vs vs' Γ e f δ e' g t)
then obtain t' where t1: "Γ ⊢ e : t'" and t2: "case_nat t' Γ ⊢ e' : t" by auto
note invar = cdens_ctxt_invarD[OF edc_let.prems(2)]
from t1 have t1': "the (expr_type Γ e) = t'" by (auto simp: expr_type_Some_iff[symmetric])
have dens1: "dens_ctxt_α ([], vs @ vs', Γ, CReal 1) ⊢⇩d e ⇒
(λx xa. ennreal (eval_cexpr f x xa))" and
wf1: "is_density_expr ([], vs @ vs', Γ, CReal 1) t' f"
using edc_let.IH(1)[OF t1] edc_let.prems by (auto dest: cdens_ctxt_invar_empty)
have invf: "cdens_ctxt_invar (shift_vars vs) (map Suc vs') (case_nat t' Γ) (map_vars Suc δ *⇩c f)"
using edc_let.prems edc_let.hyps dens1 wf1 invar
by (intro cdens_ctxt_invar_insert[OF _ t1]) (auto simp: dens_ctxt_α_def)
let ?𝒴 = "(shift_vars vs, map Suc vs', case_nat t' Γ, map_vars Suc δ *⇩c f)"
have "set (shift_vars vs) ∪ set (map Suc vs') = shift_var_set (set vs ∪ set vs')"
by (simp add: shift_var_set_def image_Un)
hence "dens_ctxt_α (shift_vars vs, map Suc vs', case_nat t' Γ, map_vars Suc δ *⇩c f) ⊢⇩d
e' ⇒ (λx xa. ennreal (eval_cexpr g x xa)) ∧
is_density_expr (shift_vars vs, map Suc vs', case_nat t' Γ, map_vars Suc δ *⇩c f) t g"
using invf t2 edc_let.prems subset_shift_var_set
by (simp only: t1'[symmetric], intro edc_let.IH(2)) simp_all
hence dens2: "dens_ctxt_α ?𝒴 ⊢⇩d e' ⇒ (λx xa. ennreal (eval_cexpr g x xa))" and
wf2: "is_density_expr (shift_vars vs, map Suc vs', case_nat t' Γ, map_vars Suc δ *⇩c f) t g"
by simp_all
have cexpr_eq: "cexpr_sem (case_nat x ρ ∘ (λx. x - Suc 0)) g =
cexpr_sem (case_nat x (case_nat undefined ρ)) g" for x ρ
using is_density_exprD[OF wf2]
by (intro cexpr_sem_eq_on_vars) (auto split: nat.split simp: shift_var_set_def)
have [simp]: "⋀σ. case_nat (σ 0) (λx. σ (Suc x)) = σ" by (intro ext) (simp split: nat.split)
hence "(shift_var_set (set vs), Suc ` set vs', case_nat t' Γ,
insert_dens (set vs) (set vs') (λx xa. ennreal (eval_cexpr f x xa))
(λx. ennreal (extract_real (cexpr_sem x δ))))
⊢⇩d e' ⇒ (λa aa. ennreal (eval_cexpr g a aa))" using dens2
apply (simp only: dens_ctxt_α_def prod.case set_shift_vars set_map)
apply (erule hd_dens_ctxt_cong)
apply (insert invar is_density_exprD[OF wf1])
unfolding insert_dens_def
apply (subst ennreal_mult'[symmetric])
apply (erule nonneg_cexprD)
apply (rule measurable_space[OF measurable_remove_var[where t=t']])
apply simp
apply (simp add: shift_var_set_def image_Un)
apply (subst cexpr_sem_Mult[of "case_nat t' Γ"])
apply (auto intro!: cexpr_typing_map_vars simp: o_def shift_var_set_def image_Un
cexpr_sem_map_vars insert_dens_def eval_cexpr_def remove_var_def)
done
hence "dens_ctxt_α (vs, vs', Γ, δ) ⊢⇩d LET e IN e' ⇒
(λρ x. ennreal (eval_cexpr g (case_nat undefined ρ) x))"
unfolding dens_ctxt_α_def
by (simp only: prod.case, intro hd_let[where f = "λx xa. ennreal (eval_cexpr f x xa)"])
(insert dens1 dens2, simp_all add: dens_ctxt_α_def extract_real_def one_ennreal_def t1')
hence "dens_ctxt_α (vs, vs', Γ, δ) ⊢⇩d LET e IN e' ⇒
(λρ x. ennreal (eval_cexpr (map_vars (λx. x - 1) g) ρ x))"
proof (simp only: dens_ctxt_α_def prod.case, erule_tac hd_cong[OF _ _ edc_let.prems(1,3)])
fix ρ x assume ρ: "ρ ∈ space (state_measure (set vs') Γ)"
and x: "x ∈ space (stock_measure t)"
have "eval_cexpr (map_vars (λx. x - 1) g) ρ x =
extract_real (cexpr_sem (case_nat x ρ ∘ (λx. x - Suc 0)) g)"
unfolding eval_cexpr_def by (simp add: cexpr_sem_map_vars)
also note cexpr_eq[of x ρ]
finally show "ennreal (eval_cexpr g (case_nat undefined ρ) x) =
ennreal (eval_cexpr (map_vars (λx. x - 1) g) ρ x)"
by (simp add: eval_cexpr_def)
qed (simp_all add: density_context_α[OF edc_let.prems(2)])
moreover have "is_density_expr (vs, vs', Γ, δ) t (map_vars (λx. x - 1) g)"
proof (intro is_density_exprI)
note wf = is_density_exprD[OF wf2]
show "case_nat t Γ ⊢⇩c map_vars (λx. x - 1) g : REAL"
by (rule cexpr_typing_map_vars, rule cexpr_typing_cong'[OF wf(1)])
(insert wf(2), auto split: nat.split simp: shift_var_set_def)
from wf(2) show "free_vars (map_vars (λx. x - 1) g)
⊆ shift_var_set (set vs')"
by (auto simp: shift_var_set_def)
next
show "nonneg_cexpr (shift_var_set (set vs')) (case_nat t Γ) (map_vars (λx. x - 1) g)"
apply (intro nonneg_cexprI_shift)
apply (simp add: cexpr_sem_map_vars cexpr_eq)
apply (rule nonneg_cexprD[OF wf2[THEN is_density_exprD_nonneg]])
apply (auto simp: space_state_measure PiE_iff extensional_def split: nat.splits)
done
qed
ultimately show ?case by (rule conjI)
next
case (edc_rand vs vs' Γ δ e f dst t')
define t where "t = dist_param_type dst"
note invar = cdens_ctxt_invarD[OF edc_rand.prems(2)]
from edc_rand have t1: "Γ ⊢ e : t" and t2: "t' = dist_result_type dst" by (auto simp: t_def)
have dens: "dens_ctxt_α (vs, vs', Γ, δ) ⊢⇩d e ⇒ (λx xa. ennreal (eval_cexpr f x xa))" and
wf: "is_density_expr (vs, vs', Γ, δ) t f" using edc_rand t1 t2 by auto
from wf have tf: "case_nat t Γ ⊢⇩c f : REAL" and varsf: "free_vars f ⊆ shift_var_set (set vs')"
unfolding is_density_expr_def by simp_all
let ?M = "(λρ. dens_ctxt_measure (dens_ctxt_α (vs,vs',Γ,δ)) ρ ⤜ (λσ. expr_sem σ e))"
have dens': "has_parametrized_subprob_density (state_measure (set vs') Γ) ?M (stock_measure t)
(λρ x. ennreal (eval_cexpr f ρ x))" using dens t1 edc_rand.prems
by (simp_all add: dens_ctxt_α_def expr_has_density_sound_aux density_context_α)
let ?shift = "case_nat 0 (λx. Suc (Suc x))"
let ?e1 = "map_vars ?shift f"
let ?e2 = "dist_dens_cexpr dst (CVar 0) (CVar 1)"
let ?e = "(∫⇩c ?e1 *⇩c ?e2 ∂t)"
have [simp]: "⋀t t' Γ. case_nat t (case_nat t' Γ) ∘ ?shift = case_nat t Γ"
by (intro ext) (simp split: nat.split add: o_def)
have te1: "case_nat t (case_nat t' Γ) ⊢⇩c ?e1 : REAL" using tf
by (auto intro!: cexpr_typing.intros cexpr_typing_dist_dens_cexpr cet_var'
cexpr_typing_map_vars simp: t_def t2)
have te2: "case_nat t (case_nat t' Γ) ⊢⇩c ?e2 : REAL"
by (intro cexpr_typing_dist_dens_cexpr cet_var') (simp_all add: t_def t2)
have te: "case_nat t' Γ ⊢⇩c ?e : REAL" using te1 te2
by (intro cet_int cet_op[where t = "PRODUCT REAL REAL"] cet_pair) (simp_all add: t2 t_def)
have vars_e1: "free_vars ?e1 ⊆ shift_var_set (shift_var_set (set vs'))"
using varsf by (auto simp: shift_var_set_def)
have "(case_nat 0 (λx. Suc (Suc x)) -` shift_var_set (shift_var_set (set vs'))) =
shift_var_set (set vs')" by (auto simp: shift_var_set_def split: nat.split_asm)
have nonneg_e1: "nonneg_cexpr (shift_var_set (shift_var_set (set vs'))) (case_nat t (case_nat t' Γ)) ?e1"
by (auto intro!: nonneg_cexprI wf[THEN is_density_exprD_nonneg, THEN nonneg_cexprD] case_nat_in_state_measure
dest!: space_state_measureD_shift simp: cexpr_sem_map_vars)
have vars_e2: "free_vars ?e2 ⊆ shift_var_set (shift_var_set (set vs'))"
by (intro order.trans[OF free_vars_dist_dens_cexpr]) (auto simp: shift_var_set_def)
have nonneg_e2: "nonneg_cexpr (shift_var_set (shift_var_set (set vs')))
(case_nat t (case_nat t' Γ)) ?e2"
by (intro nonneg_dist_dens_cexpr cet_var') (auto simp: t2 t_def shift_var_set_def)
let ?f = "λρ x. ∫⇧+y. ennreal (eval_cexpr f ρ y) * dist_dens dst y x∂stock_measure t"
let ?M = "(λρ. dens_ctxt_measure (dens_ctxt_α (vs,vs',Γ,δ)) ρ ⤜ (λσ. expr_sem σ (Random dst e)))"
have dens': "dens_ctxt_α (vs, vs', Γ, δ) ⊢⇩d Random dst e ⇒ ?f" using dens
by (simp only: dens_ctxt_α_def prod.case t_def hd_rand[unfolded apply_dist_to_dens_def])
hence dens'': "has_parametrized_subprob_density (state_measure (set vs') Γ) ?M (stock_measure t') ?f"
using edc_rand.prems invar
by (simp only: dens_ctxt_α_def prod.case, intro expr_has_density_sound_aux)
(auto intro!: density_context_α)
{
fix ρ assume ρ: "ρ ∈ space (state_measure (set vs') Γ)"
fix x assume x: "x ∈ type_universe t'"
fix y assume y: "y ∈ type_universe t"
let ?ρ'' = "case_nat y (case_nat x ρ)" and ?Γ'' = "case_nat t (case_nat t' Γ)"
let ?V'' = "shift_var_set (shift_var_set (set vs'))"
have ρ'': "?ρ'' ∈ space (state_measure (shift_var_set (shift_var_set (set vs'))) ?Γ'')"
using ρ x y by (intro case_nat_in_state_measure) simp_all
have A: "extract_real (cexpr_sem ?ρ'' (?e1 *⇩c ?e2)) =
extract_real (cexpr_sem ?ρ'' ?e1) * extract_real (cexpr_sem ?ρ'' ?e2)"
by (rule cexpr_sem_Mult[OF te1 te2 ρ'' vars_e1 vars_e2])
also have "... ≥ 0" using nonneg_e1 nonneg_e2 ρ''
by (blast intro: mult_nonneg_nonneg dest: nonneg_cexprD)
finally have B: "extract_real (cexpr_sem ?ρ'' (?e1 *⇩c ?e2)) ≥ 0" .
note A
hence "eval_cexpr f ρ y * dist_dens dst y x = extract_real (cexpr_sem ?ρ'' (?e1 *⇩c ?e2))"
using ρ''
apply (subst A)
apply (subst ennreal_mult'')
using nonneg_e2
apply (erule nonneg_cexprD)
apply (subst cexpr_sem_dist_dens_cexpr[of ?Γ'' _ _ _ ?V''])
apply (force simp: cexpr_sem_map_vars eval_cexpr_def t2 t_def intro!: cet_var')+
done
note this B
} note e1e2 = this
{
fix ρ assume ρ: "ρ ∈ space (state_measure (set vs') Γ)"
have "AE x in stock_measure t'.
apply_dist_to_dens dst (λρ x. ennreal (eval_cexpr f ρ x)) ρ x = eval_cexpr ?e ρ x"
proof (rule AE_mp[OF _ AE_I2[OF impI]])
from has_parametrized_subprob_density_integral[OF dens'' ρ]
have "(∫⇧+x. ?f ρ x ∂stock_measure t') ≠ ∞" by auto
thus "AE x in stock_measure t'. ?f ρ x ≠ ∞"
using has_parametrized_subprob_densityD(3)[OF dens''] ρ
by (intro nn_integral_PInf_AE ) simp_all
next
fix x assume x: "x ∈ space (stock_measure t')" and finite: "?f ρ x ≠ ∞"
let ?ρ' = "case_nat x ρ"
have ρ': "?ρ' ∈ space (state_measure (shift_var_set (set vs')) (case_nat t' Γ))"
using ρ x by (intro case_nat_in_state_measure) simp_all
hence *: "(∫⇧+y. ennreal (eval_cexpr f ρ y) * dist_dens dst y x ∂stock_measure t) =
∫⇧+y. extract_real (cexpr_sem (case_nat y ?ρ') (?e1 *⇩c ?e2)) ∂stock_measure t" (is "_ = ?I")
using ρ x by (intro nn_integral_cong) (simp add: e1e2)
also from * and finite have finite': "?I < ∞" by (simp add: less_top)
have "?I = ennreal (eval_cexpr ?e ρ x)" using ρ' te te1 te2 vars_e1 vars_e2 nonneg_e1 nonneg_e2
unfolding eval_cexpr_def
by (subst cexpr_sem_integral_nonneg[OF finite'])
(auto simp: eval_cexpr_def t2 t_def intro!: nonneg_cexpr_Mult)
finally show "apply_dist_to_dens dst (λρ x. ennreal (eval_cexpr f ρ x)) ρ x =
ennreal (eval_cexpr ?e ρ x)"
unfolding apply_dist_to_dens_def by (simp add: t_def)
qed
} note AE_eq = this
have meas: "(λ(ρ, x). ennreal (eval_cexpr ?e ρ x))
∈ borel_measurable (state_measure (set vs') Γ ⨂⇩M stock_measure t')"
apply (subst measurable_split_conv, rule measurable_compose[OF _ measurable_ennreal])
apply (subst measurable_split_conv[symmetric], rule measurable_eval_cexpr[OF te])
apply (insert vars_e1 vars_e2, auto simp: shift_var_set_def)
done
show ?case
proof (intro conjI is_density_exprI, simp only: dens_ctxt_α_def prod.case,
rule hd_AE[OF hd_rand edc_rand.prems(1)])
from dens show "(set vs, set vs', Γ, λx. ennreal (extract_real (cexpr_sem x δ))) ⊢⇩d
e ⇒ (λx xa. ennreal (eval_cexpr f x xa))"
unfolding dens_ctxt_α_def by simp
next
have "nonneg_cexpr (shift_var_set (set vs')) (case_nat t' Γ) (∫⇩c ?e1 *⇩c ?e2 ∂t)"
by (intro nonneg_cexpr_int nonneg_cexpr_Mult nonneg_dist_dens_cexpr te1 te2 vars_e1 vars_e2 nonneg_e1)
(auto simp: t_def t2 intro!: cet_var')
then show "nonneg_cexpr (shift_var_set (set vs')) (case_nat t' Γ)
(∫⇩c map_vars (case_nat 0 (λx. x + 2)) f *⇩c ?e2 ∂dist_param_type dst)"
by (simp add: t_def)
qed (insert AE_eq meas te vars_e1 vars_e2, auto simp: t_def t2 shift_var_set_def)
next
case (edc_rand_det e vs' vs Γ δ dst t')
define t where "t = dist_param_type dst"
note invar = cdens_ctxt_invarD[OF edc_rand_det.prems(2)]
from edc_rand_det have t1: "Γ ⊢ e : t" and t2: "t' = dist_result_type dst" by (auto simp: t_def)
let ?e1 = "map_vars Suc (branch_prob_cexpr (vs, vs', Γ, δ))" and
?e2 = "dist_dens_cexpr dst (map_vars Suc (expr_rf_to_cexpr e)) (CVar 0)"
have ctype1: "case_nat t' Γ ⊢⇩c ?e1 : REAL"
using invar by (auto intro!: cexpr_typing_map_vars simp: o_def)
have vars2': "free_vars (map_vars Suc (expr_rf_to_cexpr e)) ⊆ shift_var_set (set vs')"
unfolding shift_var_set_def using free_vars_expr_rf_to_cexpr edc_rand_det.hyps by auto
have vars2: "free_vars ?e2 ⊆ shift_var_set (free_vars e)"
unfolding shift_var_set_def using free_vars_expr_rf_to_cexpr edc_rand_det.hyps
by (intro order.trans[OF free_vars_dist_dens_cexpr]) auto
have ctype2: "case_nat t' Γ ⊢⇩c ?e2 : REAL" using t1 edc_rand_det.hyps
by (intro cexpr_typing_dist_dens_cexpr cexpr_typing_map_vars)
(auto simp: o_def t_def t2 intro!: cet_var')
have nonneg_e2: "nonneg_cexpr (shift_var_set (set vs')) (case_nat t' Γ) ?e2"
using t1 ‹randomfree e› free_vars_expr_rf_to_cexpr[of e] edc_rand_det.hyps
apply (intro nonneg_dist_dens_cexpr cexpr_typing_map_vars)
apply (auto simp add: o_def t_def t2 intro!: cet_var')
done
have nonneg_e1: "nonneg_cexpr (shift_var_set (set vs')) (case_nat t' Γ) ?e1"
using invar
by (auto simp add: branch_prob_cexpr_def nonneg_cexpr_shift_iff intro!: nonneg_cexpr_sem_integrate_vars')
{
fix ρ x
assume x: "x ∈ type_universe t'" and ρ: "ρ ∈ space (state_measure (set vs') Γ)"
hence ρ': "case_nat x ρ ∈ space (state_measure (shift_var_set (set vs')) (case_nat t' Γ))"
by (rule case_nat_in_state_measure)
hence "eval_cexpr (?e1 *⇩c ?e2) ρ x =
ennreal (extract_real (cexpr_sem (case_nat x ρ)
(map_vars Suc (branch_prob_cexpr (vs, vs', Γ, δ))))) *
ennreal (extract_real (cexpr_sem (case_nat x ρ) ?e2))" (is "_ = ?a * ?b")
using invar
apply (subst ennreal_mult''[symmetric])
apply (rule nonneg_cexprD[OF nonneg_e2])
apply simp
unfolding eval_cexpr_def
apply (subst cexpr_sem_Mult[of "case_nat t' Γ" _ _ _ "shift_var_set (set vs')"])
apply (insert invar ctype1 vars2 ctype2 edc_rand_det.hyps(2))
apply (auto simp: shift_var_set_def)
done
also have "?a = branch_prob (dens_ctxt_α (vs,vs',Γ,δ)) ρ" (is "_ = ?c")
by (subst cexpr_sem_map_vars, subst cexpr_sem_branch_prob) (simp_all add: o_def ρ edc_rand_det.prems)
also have "?b = dist_dens dst (expr_sem_rf ρ e) x" (is "_ = ?d") using t1 edc_rand_det.hyps
by (subst cexpr_sem_dist_dens_cexpr[of "case_nat t' Γ"], insert ρ' vars2')
(auto intro!: cexpr_typing_map_vars cet_var'
simp: o_def t_def t2 cexpr_sem_map_vars cexpr_sem_expr_rf_to_cexpr)
finally have A: "ennreal (eval_cexpr (?e1 *⇩c ?e2) ρ x) = ?c * ?d" .
} note A = this
have meas: "(λ(ρ, x). ennreal (eval_cexpr (?e1 *⇩c ?e2) ρ x))
∈ borel_measurable (state_measure (set vs') Γ ⨂⇩M stock_measure t')"
using ctype1 ctype2 vars2 invar edc_rand_det.hyps
by (subst measurable_split_conv, intro measurable_compose[OF _ measurable_ennreal],
subst measurable_split_conv[symmetric], intro measurable_eval_cexpr)
(auto intro!: cexpr_typing.intros simp: shift_var_set_def)
from ctype1 ctype2 vars2 invar edc_rand_det.hyps
have wf: "is_density_expr (vs, vs', Γ, δ) t' (?e1 *⇩c ?e2)"
proof (intro is_density_exprI)
show "nonneg_cexpr (shift_var_set (set vs')) (case_nat t' Γ) (?e1 *⇩c ?e2)"
using invar(2)
order_trans[OF free_vars_expr_rf_to_cexpr[OF ‹randomfree e›] ‹free_vars e ⊆ set vs'›]
by (intro nonneg_cexpr_Mult ctype1 ctype2 nonneg_e2 nonneg_e1
free_vars_dist_dens_cexpr[THEN order_trans])
(auto simp: intro: order_trans)
qed (auto intro!: cexpr_typing.intros simp: shift_var_set_def)
show ?case using edc_rand_det.prems edc_rand_det.hyps meas wf A
apply (intro conjI, simp add: dens_ctxt_α_def)
apply (intro hd_AE[OF hd_rand_det[OF edc_rand_det.hyps] edc_rand_det.prems(1) AE_I2])
apply (simp_all add: dens_ctxt_α_def)
done
next
case (edc_if_det b vs vs' Γ δ e1 f1 e2 f2 t)
hence tb: "Γ ⊢ b : BOOL" and t1: "Γ ⊢ e1 : t" and t2: "Γ ⊢ e2 : t" by auto
from edc_if_det have b: "randomfree b" "free_vars b ⊆ set vs ∪ set vs'" by simp_all
note invar = cdens_ctxt_invarD[OF edc_if_det.prems(2)]
let ?ind1 = "⟨expr_rf_to_cexpr b⟩⇩c" and ?ind2 = "⟨¬⇩c expr_rf_to_cexpr b⟩⇩c"
have tind1: "Γ ⊢⇩c ?ind1 : REAL" and tind2: "Γ ⊢⇩c ?ind2 : REAL"
using edc_if_det.hyps tb by (auto intro!: cexpr_typing.intros)
have tδ1: "Γ ⊢⇩c δ *⇩c ?ind1 : REAL" and tδ2: "Γ ⊢⇩c δ *⇩c ?ind2 : REAL"
using invar(3) edc_if_det.hyps tb by (auto intro!: cexpr_typing.intros)
have nonneg_ind1: "nonneg_cexpr (set vs ∪ set vs') Γ ?ind1" and
nonneg_ind2: "nonneg_cexpr (set vs ∪ set vs') Γ ?ind2"
using tind1 tind2 edc_if_det.hyps tb
by (auto intro!: nonneg_cexprI simp: cexpr_sem_expr_rf_to_cexpr bool_to_real_def extract_real_def
dest: val_type_expr_sem_rf[OF tb b] elim!: BOOL_E split: if_split)
have subprob1: "subprob_cexpr (set vs) (set vs') Γ (δ *⇩c ?ind1)" and
subprob2: "subprob_cexpr (set vs) (set vs') Γ (δ *⇩c ?ind2)"
using invar tb edc_if_det.hyps edc_if_det.prems free_vars_expr_rf_to_cexpr[OF edc_if_det.hyps(1)]
by (auto intro!: subprob_indicator cet_op)
have vars1: "free_vars (δ *⇩c ?ind1) ⊆ set vs ∪ set vs'" and
vars2: "free_vars (δ *⇩c ?ind2) ⊆ set vs ∪ set vs'"
using invar edc_if_det.hyps edc_if_det.prems free_vars_expr_rf_to_cexpr by auto
have inv1: "cdens_ctxt_invar vs vs' Γ (δ *⇩c ?ind1)"
using invar edc_if_det.hyps edc_if_det.prems tind1 tδ1 subprob1 nonneg_ind1 vars1
by (intro cdens_ctxt_invarI nonneg_cexpr_Mult) auto
have inv2: "cdens_ctxt_invar vs vs' Γ (δ *⇩c ?ind2)"
using invar edc_if_det.hyps edc_if_det.prems tind2 tδ2 subprob2 nonneg_ind2 vars2
by (intro cdens_ctxt_invarI nonneg_cexpr_Mult) auto
have dens1: "dens_ctxt_α (vs, vs', Γ, δ *⇩c ?ind1) ⊢⇩d e1 ⇒ (λρ x. eval_cexpr f1 ρ x)" and
wf1: "is_density_expr (vs, vs', Γ, δ *⇩c ?ind1) t f1"
using edc_if_det.IH(1)[OF t1 inv1] edc_if_det.prems by auto
have dens2: "dens_ctxt_α (vs, vs', Γ, δ *⇩c ?ind2) ⊢⇩d e2 ⇒ (λρ x. eval_cexpr f2 ρ x)" and
wf2: "is_density_expr (vs, vs', Γ, δ *⇩c ?ind2) t f2"
using edc_if_det.IH(2)[OF t2 inv2] edc_if_det.prems by auto
show ?case
proof (rule conjI, simp only: dens_ctxt_α_def prod.case, rule hd_cong[OF hd_if_det])
let ?𝒴 = "(set vs, set vs', Γ, if_dens_det (λx. ennreal (extract_real (cexpr_sem x δ))) b True)"
show "?𝒴 ⊢⇩d e1 ⇒ (λρ x. eval_cexpr f1 ρ x)"
proof (rule hd_dens_ctxt_cong)
let ?δ = "λσ. ennreal (extract_real (cexpr_sem σ (δ *⇩c ?ind1)))"
show "(set vs, set vs', Γ, ?δ) ⊢⇩d e1 ⇒ (λρ x. ennreal (eval_cexpr f1 ρ x))"
using dens1 by (simp add: dens_ctxt_α_def)
fix σ assume σ: "σ ∈ space (state_measure (set vs ∪ set vs') Γ)"
have "extract_real (cexpr_sem σ (δ *⇩c ?ind1)) =
extract_real (cexpr_sem σ δ) * extract_real (cexpr_sem σ ?ind1)" using invar vars1
by (subst cexpr_sem_Mult[OF invar(3) tind1 σ]) simp_all
also have "extract_real (cexpr_sem σ ?ind1) = (if expr_sem_rf σ b = TRUE then 1 else 0)"
using edc_if_det.hyps val_type_expr_sem_rf[OF tb b σ]
by (auto simp: cexpr_sem_expr_rf_to_cexpr extract_real_def bool_to_real_def elim!: BOOL_E)
finally show "?δ σ = if_dens_det (λσ. ennreal (extract_real (cexpr_sem σ δ))) b True σ"
by (simp add: if_dens_det_def)
qed
next
let ?𝒴 = "(set vs, set vs', Γ, if_dens_det (λx. ennreal (extract_real (cexpr_sem x δ))) b False)"
show "?𝒴 ⊢⇩d e2 ⇒ (λρ x. eval_cexpr f2 ρ x)"
proof (rule hd_dens_ctxt_cong)
let ?δ = "λσ. ennreal (extract_real (cexpr_sem σ (δ *⇩c ?ind2)))"
show "(set vs, set vs', Γ, ?δ) ⊢⇩d e2 ⇒ (λρ x. ennreal (eval_cexpr f2 ρ x))"
using dens2 by (simp add: dens_ctxt_α_def)
fix σ assume σ: "σ ∈ space (state_measure (set vs ∪ set vs') Γ)"
have "extract_real (cexpr_sem σ (δ *⇩c ?ind2)) =
extract_real (cexpr_sem σ δ) * extract_real (cexpr_sem σ ?ind2)" using invar vars1
by (subst cexpr_sem_Mult[OF invar(3) tind2 σ]) simp_all
also have "extract_real (cexpr_sem σ ?ind2) = (if expr_sem_rf σ b = FALSE then 1 else 0)"
using edc_if_det.hyps val_type_expr_sem_rf[OF tb b σ]
by (auto simp: cexpr_sem_expr_rf_to_cexpr extract_real_def bool_to_real_def elim!: BOOL_E)
finally show "?δ σ = if_dens_det (λσ. ennreal (extract_real (cexpr_sem σ δ))) b False σ"
by (simp add: if_dens_det_def)
qed
next
fix ρ x assume ρ: "ρ ∈ space (state_measure (set vs') Γ)" and x : "x ∈ space (stock_measure t)"
hence "eval_cexpr (f1 +⇩c f2) ρ x = eval_cexpr f1 ρ x + eval_cexpr f2 ρ x"
using wf1 wf2 unfolding eval_cexpr_def is_density_expr_def
by (subst cexpr_sem_Add[where Γ = "case_nat t Γ" and V = "shift_var_set (set vs')"]) auto
moreover have "0 ≤ eval_cexpr f1 ρ x" "0 ≤ eval_cexpr f2 ρ x"
unfolding eval_cexpr_def
using ρ x wf1[THEN is_density_exprD_nonneg, THEN nonneg_cexprD] wf2[THEN is_density_exprD_nonneg, THEN nonneg_cexprD]
unfolding space_state_measure_shift_iff by auto
ultimately show "ennreal (eval_cexpr f1 ρ x) + ennreal (eval_cexpr f2 ρ x) = ennreal (eval_cexpr (f1 +⇩c f2) ρ x)"
by simp
next
show "is_density_expr (vs, vs', Γ, δ) t (f1 +⇩c f2)" using wf1 wf2
using wf1[THEN is_density_exprD_nonneg] wf2[THEN is_density_exprD_nonneg]
by (auto simp: is_density_expr_def intro!: cet_op[where t = "PRODUCT REAL REAL"] cet_pair nonneg_cexpr_Add)
qed (insert edc_if_det.prems edc_if_det.hyps, auto intro!: density_context_α)
next
case (edc_if vs vs' Γ b f δ e1 g1 e2 g2 t)
hence tb: "Γ ⊢ b : BOOL" and t1: "Γ ⊢ e1 : t" and t2: "Γ ⊢ e2 : t" by auto
note invar = cdens_ctxt_invarD[OF edc_if.prems(2)]
have densb: "dens_ctxt_α ([], vs @ vs', Γ, CReal 1) ⊢⇩d b ⇒ (λρ b. ennreal (eval_cexpr f ρ b))" and
wfb: "is_density_expr ([], vs @ vs', Γ, CReal 1) BOOL f"
using edc_if.IH(1)[OF tb] edc_if.prems by (simp_all add: cdens_ctxt_invar_empty)
have inv1: "cdens_ctxt_invar vs vs' Γ (δ *⇩c cexpr_subst_val f TRUE)" and
inv2: "cdens_ctxt_invar vs vs' Γ (δ *⇩c cexpr_subst_val f FALSE)"
using tb densb wfb edc_if.prems by (auto intro!: cdens_ctxt_invar_insert_bool)
let ?δ1 = "cexpr_subst_val f TRUE" and ?δ2 = "cexpr_subst_val f FALSE"
have tδ1: "Γ ⊢⇩c δ *⇩c ?δ1 : REAL" and tδ2: "Γ ⊢⇩c δ *⇩c ?δ2 : REAL"
using is_density_exprD[OF wfb] invar
by (auto intro!: cet_op[where t = "PRODUCT REAL REAL"] cet_pair)
have vars1: "free_vars (δ *⇩c ?δ1) ⊆ set vs ∪ set vs'" and
vars2: "free_vars (δ *⇩c ?δ2) ⊆ set vs ∪ set vs'"
using invar is_density_exprD[OF wfb] by (auto simp: shift_var_set_def)
have dens1: "dens_ctxt_α (vs, vs', Γ, δ *⇩c ?δ1) ⊢⇩d e1 ⇒ (λx xa. ennreal (eval_cexpr g1 x xa))" and
wf1: "is_density_expr (vs, vs', Γ, δ *⇩c ?δ1) t g1" and
dens2: "dens_ctxt_α (vs, vs', Γ, δ *⇩c ?δ2) ⊢⇩d e2 ⇒ (λx xa. ennreal (eval_cexpr g2 x xa))" and
wf2: "is_density_expr (vs, vs', Γ, δ *⇩c ?δ2) t g2"
using edc_if.IH(2)[OF t1 inv1] edc_if.IH(3)[OF t2 inv2] edc_if.prems by simp_all
have f_nonneg[simp]: "σ ∈ space (state_measure (set vs ∪ set vs') Γ) ⟹
0 ≤ extract_real (cexpr_sem (case_nat (BoolVal b) σ) f)" for b σ
using wfb[THEN is_density_exprD_nonneg] by (rule nonneg_cexprD) auto
let ?δ' = "λσ. ennreal (extract_real (cexpr_sem σ δ))" and ?f = "λσ x. ennreal (eval_cexpr f σ x)"
show ?case
proof (rule conjI, simp only: dens_ctxt_α_def prod.case, rule hd_cong[OF hd_if])
let ?𝒴 = "(set vs, set vs', Γ, if_dens ?δ' ?f True)"
show "?𝒴 ⊢⇩d e1 ⇒ (λρ x. eval_cexpr g1 ρ x)"
proof (rule hd_dens_ctxt_cong)
let ?δ = "λσ. ennreal (extract_real (cexpr_sem σ (δ *⇩c ?δ1)))"
show "(set vs, set vs', Γ, ?δ) ⊢⇩d e1 ⇒ (λρ x. ennreal (eval_cexpr g1 ρ x))"
using dens1 by (simp add: dens_ctxt_α_def)
fix σ assume σ: "σ ∈ space (state_measure (set vs ∪ set vs') Γ)"
have "extract_real (cexpr_sem σ (δ *⇩c ?δ1)) =
extract_real (cexpr_sem σ δ) * extract_real (cexpr_sem σ ?δ1)"
using invar vars1 is_density_exprD[OF wfb] by (subst cexpr_sem_Mult[OF invar(3) _ σ]) auto
also have "... = if_dens ?δ' ?f True σ" unfolding if_dens_def by (simp add: eval_cexpr_def ennreal_mult'' σ)
finally show "?δ σ = if_dens ?δ' ?f True σ" by (simp add: if_dens_det_def)
qed
next
let ?𝒴 = "(set vs, set vs', Γ, if_dens ?δ' ?f False)"
show "?𝒴 ⊢⇩d e2 ⇒ (λρ x. eval_cexpr g2 ρ x)"
proof (rule hd_dens_ctxt_cong)
let ?δ = "λσ. ennreal (extract_real (cexpr_sem σ (δ *⇩c ?δ2)))"
show "(set vs, set vs', Γ, ?δ) ⊢⇩d e2 ⇒ (λρ x. ennreal (eval_cexpr g2 ρ x))"
using dens2 by (simp add: dens_ctxt_α_def)
fix σ assume σ: "σ ∈ space (state_measure (set vs ∪ set vs') Γ)"
have "extract_real (cexpr_sem σ (δ *⇩c ?δ2)) =
extract_real (cexpr_sem σ δ) * extract_real (cexpr_sem σ ?δ2)"
using invar vars1 is_density_exprD[OF wfb] by (subst cexpr_sem_Mult[OF invar(3) _ σ]) auto
also have "... = if_dens ?δ' ?f False σ" unfolding if_dens_def by (simp add: eval_cexpr_def ennreal_mult'' σ)
finally show "?δ σ = if_dens ?δ' ?f False σ" by (simp add: if_dens_det_def)
qed
next
fix ρ x assume ρ: "ρ ∈ space (state_measure (set vs') Γ)" and x : "x ∈ space (stock_measure t)"
hence "eval_cexpr (g1 +⇩c g2) ρ x = eval_cexpr g1 ρ x + eval_cexpr g2 ρ x"
using wf1 wf2 unfolding eval_cexpr_def is_density_expr_def
by (subst cexpr_sem_Add[where Γ = "case_nat t Γ" and V = "shift_var_set (set vs')"]) auto
moreover have "0 ≤ eval_cexpr g1 ρ x" "0 ≤ eval_cexpr g2 ρ x"
unfolding eval_cexpr_def
using ρ x wf1[THEN is_density_exprD_nonneg, THEN nonneg_cexprD] wf2[THEN is_density_exprD_nonneg, THEN nonneg_cexprD]
unfolding space_state_measure_shift_iff by auto
ultimately show "ennreal (eval_cexpr g1 ρ x) + ennreal (eval_cexpr g2 ρ x) = ennreal (eval_cexpr (g1 +⇩c g2) ρ x)"
by simp
next
show "is_density_expr (vs, vs', Γ, δ) t (g1 +⇩c g2)" using wf1 wf2
by (auto simp: is_density_expr_def intro!: cet_op[where t = "PRODUCT REAL REAL"] cet_pair nonneg_cexpr_Add)
next
show "({}, set vs ∪ set vs', Γ, λ_. 1) ⊢⇩d b ⇒ (λσ x. ennreal (eval_cexpr f σ x))"
using densb unfolding dens_ctxt_α_def by (simp add: extract_real_def one_ennreal_def)
qed (insert edc_if.prems edc_if.hyps, auto intro!: density_context_α)
next
case (edc_op_discr vs vs' Γ δ e f t oper t' t'')
let ?expr' = "⟨(oper $$⇩c (CVar 0)) =⇩c CVar 1⟩⇩c *⇩c map_vars (case_nat 0 (λx. x+2)) f"
let ?expr = "∫⇩c ?expr' ∂t" and ?shift = "case_nat 0 (λx. x + 2)"
from edc_op_discr.prems(1) edc_op_discr.hyps
have t: "Γ ⊢ e : t" by (elim expr_typing_opE, fastforce split: pdf_type.split_asm)
with edc_op_discr.prems(1) and edc_op_discr.hyps have [simp]: "t'' = t'"
by (intro expr_typing_unique) (auto intro: et_op)
from t and edc_op_discr.prems(1)
have the_t1: "the (expr_type Γ e) = t" and the_t2: "the (expr_type Γ (oper $$ e)) = t'"
by (simp_all add: expr_type_Some_iff[symmetric])
from edc_op_discr.prems edc_op_discr.IH[OF t]
have dens: "dens_ctxt_α (vs, vs', Γ, δ) ⊢⇩d e ⇒ (λx xa. ennreal (eval_cexpr f x xa))" and
wf: "is_density_expr (vs, vs', Γ, δ) t f" by simp_all
note wf' = is_density_exprD[OF wf]
have ctype''': "case_nat t (case_nat t' Γ) ⊢⇩c (oper $$⇩c (CVar 0)) =⇩c CVar 1 : BOOL" and
ctype'': "case_nat t (case_nat t' Γ) ⊢⇩c ⟨(oper $$⇩c (CVar 0)) =⇩c CVar 1⟩⇩c : REAL" and
ctype': "case_nat t (case_nat t' Γ) ⊢⇩c ?expr' : REAL" using wf' edc_op_discr.hyps
by ((intro cet_op_intros cexpr_typing_map_vars cet_var' cet_pair cet_eq,
auto intro!: cet_op cet_var') [])+
from ctype' have ctype: "case_nat t' Γ ⊢⇩c ?expr : REAL" by (rule cet_int)
have vars': "free_vars ?expr' ⊆ shift_var_set (shift_var_set (set vs'))" using wf'
by (auto split: nat.split simp: shift_var_set_def)
hence vars: "free_vars ?expr ⊆ shift_var_set (set vs')" by (auto split: nat.split_asm)
let ?𝒴 = "(set vs, set vs', Γ, λρ. ennreal (extract_real (cexpr_sem ρ δ)))"
let ?M = "λρ. dens_ctxt_measure ?𝒴 ρ ⤜ (λσ. expr_sem σ e)"
have "nonneg_cexpr (shift_var_set (set vs')) (case_nat t Γ) f"
using wf[THEN is_density_exprD_nonneg] .
hence nonneg: "nonneg_cexpr (shift_var_set (shift_var_set (set vs')))
(case_nat t (case_nat t' Γ)) ?expr'"
using wf' vars' ctype''' by (intro nonneg_cexpr_Mult[OF ctype''] cexpr_typing_map_vars
nonneg_cexpr_map_vars nonneg_indicator)
(auto dest: nonneg_cexprD simp: extract_real_def bool_to_real_def)
let ?M = "λρ. dens_ctxt_measure ?𝒴 ρ ⤜ (λσ. expr_sem σ (oper $$ e))"
let ?f = "λρ x y. (if op_sem oper y = x then 1 else 0) * ennreal (eval_cexpr f ρ y)"
have "?𝒴 ⊢⇩d oper $$ e ⇒ (λρ x. ∫⇧+y. ?f ρ x y ∂stock_measure t)" using dens t edc_op_discr.hyps
by (subst the_t1[symmetric], intro hd_op_discr)
(simp_all add: dens_ctxt_α_def the_t1 expr_type_Some_iff[symmetric])
hence dens: "?𝒴 ⊢⇩d oper $$ e ⇒ (λρ x. ∫⇧+y. eval_cexpr ?expr' (case_nat x ρ) y ∂stock_measure t)"
proof (rule hd_cong[OF _ _ _ _ nn_integral_cong])
fix ρ x y let ?P = "λx M. x ∈ space M"
assume A: "?P ρ (state_measure (set vs') Γ)" "?P x (stock_measure t')" "?P y (stock_measure t)"
hence "val_type (cexpr_sem (case_nat y ρ) f) = REAL" using wf' by (intro val_type_cexpr_sem) auto
thus "?f ρ x y = ennreal (eval_cexpr ?expr' (case_nat x ρ) y)"
by (auto simp: eval_cexpr_def extract_real_def lift_RealIntVal2_def
bool_to_real_def cexpr_sem_map_vars elim!: REAL_E)
qed (insert edc_op_discr.prems, auto intro!: density_context_α)
hence dens': "has_parametrized_subprob_density (state_measure (set vs') Γ) ?M (stock_measure t')
(λρ x. ∫⇧+y. eval_cexpr ?expr' (case_nat x ρ) y ∂stock_measure t)"
using edc_op_discr.prems by (intro expr_has_density_sound_aux density_context_α) simp_all
show ?case
proof (intro conjI is_density_exprI, simp only: dens_ctxt_α_def prod.case, rule hd_AE[OF dens])
fix ρ assume ρ: "ρ ∈ space (state_measure (set vs') Γ)"
let ?dens = "λx. ∫⇧+y. eval_cexpr ?expr' (case_nat x ρ) y ∂stock_measure t"
show "AE x in stock_measure t'. ?dens x = ennreal (eval_cexpr ?expr ρ x)"
proof (rule AE_mp[OF _ AE_I2[OF impI]])
from has_parametrized_subprob_density_integral[OF dens' ρ] and
has_parametrized_subprob_densityD(3)[OF dens'] and ρ
show "AE x in stock_measure t'. ?dens x ≠ ∞" by (intro nn_integral_PInf_AE) auto
next
fix x assume x: "x ∈ space (stock_measure t')" and fin: "?dens x ≠ ∞"
thus "?dens x = ennreal (eval_cexpr ?expr ρ x)"
using ρ vars' ctype' ctype' nonneg unfolding eval_cexpr_def
by (subst cexpr_sem_integral_nonneg) (auto intro!: nonneg_cexpr_map_vars simp: less_top)
qed
next
show "nonneg_cexpr (shift_var_set (set vs')) (case_nat t'' Γ) (∫⇩c ?expr' ∂t)"
using nonneg by (intro nonneg_cexpr_int) simp
qed (insert vars ctype edc_op_discr.prems, auto)
next
case (edc_fst vs vs' Γ δ e f t'' t' t)
hence [simp]: "t'' = t" by (auto intro!: expr_typing_unique et_op)
from edc_fst.hyps have t': "the (expr_type Γ (Snd $$ e)) = t'"
by (simp add: expr_type_Some_iff[symmetric])
let ?shift = "case_nat 0 (λx. x + 2)"
have [simp]: "⋀t t'. case_nat t (case_nat t' Γ) ∘ case_nat 0 (λx. Suc (Suc x)) = case_nat t Γ"
by (intro ext) (simp split: nat.split add: o_def)
note invar = cdens_ctxt_invarD[OF edc_fst.prems(2)]
have dens: "dens_ctxt_α (vs, vs', Γ, δ) ⊢⇩d e ⇒ (λρ x. ennreal (eval_cexpr f ρ x))" and
wf: "is_density_expr (vs, vs', Γ, δ) (PRODUCT t t') f" using edc_fst by auto
let ?M = "λρ. dens_ctxt_measure (set vs, set vs', Γ, λρ. ennreal (extract_real (cexpr_sem ρ δ))) ρ
⤜ (λσ. expr_sem σ e)"
have nonneg: "nonneg_cexpr (shift_var_set (set vs')) (case_nat (PRODUCT t t') Γ) f"
using wf by (rule is_density_exprD_nonneg)
note wf' = is_density_exprD[OF wf]
let ?expr = "map_vars ?shift f ∘⇩c <CVar 1, CVar 0>⇩c"
have ctype: "case_nat t' (case_nat t Γ) ⊢⇩c ?expr : REAL"
using wf' by (auto intro!: cexpr_typing.intros cexpr_typing_map_vars)
have vars: "free_vars ?expr ⊆ shift_var_set (shift_var_set (set vs'))" using free_vars_cexpr_comp wf'
by (intro subset_shift_var_set) (force simp: shift_var_set_def)
let ?M = "λρ. dens_ctxt_measure (set vs, set vs', Γ, λρ. ennreal (extract_real (cexpr_sem ρ δ))) ρ
⤜ (λσ. expr_sem σ (Fst $$ e))"
have A: "⋀x y ρ. ((case_nat x (case_nat y ρ))(0 := <|y, x|>)) ∘ ?shift = case_nat <|y, x|> ρ"
by (intro ext) (simp split: nat.split add: o_def)
have dens': "(set vs, set vs', Γ, λρ. ennreal (extract_real (cexpr_sem ρ δ))) ⊢⇩d Fst $$ e ⇒
(λρ x. (∫⇧+y. eval_cexpr f ρ (<|x, y|>) ∂stock_measure t'))" (is "?𝒴 ⊢⇩d _ ⇒ ?f")
using dens by (subst t'[symmetric], intro hd_fst) (simp add: dens_ctxt_α_def)
hence dens': "?𝒴 ⊢⇩d Fst $$ e ⇒ (λρ x. (∫⇧+y. eval_cexpr ?expr (case_nat x ρ) y ∂stock_measure t'))"
(is "_ ⊢⇩d _ ⇒ ?f") by (rule hd_cong, intro density_context_α, insert edc_fst.prems A)
(auto intro!: nn_integral_cong simp: eval_cexpr_def cexpr_sem_cexpr_comp cexpr_sem_map_vars)
hence dens'': "has_parametrized_subprob_density (state_measure (set vs') Γ) ?M (stock_measure t) ?f"
using edc_fst.prems by (intro expr_has_density_sound_aux density_context_α) simp_all
have "⋀V. ?shift -` shift_var_set (shift_var_set V) = shift_var_set V"
by (auto simp: shift_var_set_def split: nat.split_asm)
hence nonneg': "nonneg_cexpr (shift_var_set (shift_var_set (set vs'))) (case_nat t' (case_nat t Γ)) ?expr"
by (auto intro!: nonneg_cexpr_comp nonneg_cexpr_map_vars nonneg cexpr_typing.intros cet_var')
show ?case
proof (intro conjI is_density_exprI, simp only: dens_ctxt_α_def prod.case, rule hd_AE[OF dens'])
fix ρ assume ρ: "ρ ∈ space (state_measure (set vs') Γ)"
thus "AE x in stock_measure t. ?f ρ x = ennreal (eval_cexpr (∫⇩c ?expr ∂t') ρ x)"
using ctype vars edc_fst.hyps nonneg'
by (intro has_parametrized_subprob_density_cexpr_sem_integral[OF dens'']) auto
next
show "nonneg_cexpr (shift_var_set (set vs')) (case_nat t Γ)
(∫⇩c (map_vars (case_nat 0 (λx. x + 2)) f ∘⇩c <CVar 1, CVar 0>⇩c) ∂t')"
using nonneg' by (intro nonneg_cexpr_int)
qed (insert edc_fst.prems ctype vars, auto simp: measurable_split_conv
intro!: cet_int measurable_compose[OF _ measurable_ennreal]
measurable_Pair_compose_split[OF measurable_eval_cexpr])
next
case (edc_snd vs vs' Γ δ e f t t' t'')
hence [simp]: "t'' = t'" by (auto intro!: expr_typing_unique et_op)
from edc_snd.hyps have t': "the (expr_type Γ (Fst $$ e)) = t"
by (simp add: expr_type_Some_iff[symmetric])
let ?shift = "case_nat 0 (λx. x + 2)"
have [simp]: "⋀t t'. case_nat t (case_nat t' Γ) ∘ case_nat 0 (λx. Suc (Suc x)) = case_nat t Γ"
by (intro ext) (simp split: nat.split add: o_def)
note invar = cdens_ctxt_invarD[OF edc_snd.prems(2)]
have dens: "dens_ctxt_α (vs, vs', Γ, δ) ⊢⇩d e ⇒ (λρ x. ennreal (eval_cexpr f ρ x))" and
wf: "is_density_expr (vs, vs', Γ, δ) (PRODUCT t t') f" using edc_snd by auto
let ?M = "λρ. dens_ctxt_measure (set vs, set vs', Γ, λρ. ennreal (extract_real (cexpr_sem ρ δ))) ρ
⤜ (λσ. expr_sem σ e)"
have nonneg: "nonneg_cexpr (shift_var_set (set vs')) (case_nat (PRODUCT t t') Γ) f"
using wf by (rule is_density_exprD_nonneg)
note wf' = is_density_exprD[OF wf]
let ?expr = "map_vars ?shift f ∘⇩c <CVar 0, CVar 1>⇩c"
have ctype: "case_nat t (case_nat t' Γ) ⊢⇩c ?expr : REAL"
using wf' by (auto intro!: cexpr_typing.intros cexpr_typing_map_vars)
have vars: "free_vars ?expr ⊆ shift_var_set (shift_var_set (set vs'))" using free_vars_cexpr_comp wf'
by (intro subset_shift_var_set) (force simp: shift_var_set_def)
let ?M = "λρ. dens_ctxt_measure (set vs, set vs', Γ, λρ. ennreal (extract_real (cexpr_sem ρ δ))) ρ
⤜ (λσ. expr_sem σ (Snd $$ e))"
have A: "⋀x y ρ. ((case_nat y (case_nat x ρ))(0 := <|y, x|>)) ∘ ?shift = case_nat <|y, x|> ρ"
by (intro ext) (simp split: nat.split add: o_def)
have dens': "(set vs, set vs', Γ, λρ. ennreal (extract_real (cexpr_sem ρ δ))) ⊢⇩d Snd $$ e ⇒
(λρ y. (∫⇧+x. eval_cexpr f ρ (<|x, y|>) ∂stock_measure t))" (is "?𝒴 ⊢⇩d _ ⇒ ?f")
using dens by (subst t'[symmetric], intro hd_snd) (simp add: dens_ctxt_α_def)
hence dens': "?𝒴 ⊢⇩d Snd $$ e ⇒ (λρ y. (∫⇧+x. eval_cexpr ?expr (case_nat y ρ) x ∂stock_measure t))"
(is "_ ⊢⇩d _ ⇒ ?f") by (rule hd_cong, intro density_context_α, insert edc_snd.prems A)
(auto intro!: nn_integral_cong simp: eval_cexpr_def cexpr_sem_cexpr_comp cexpr_sem_map_vars)
hence dens'': "has_parametrized_subprob_density (state_measure (set vs') Γ) ?M (stock_measure t') ?f"
using edc_snd.prems by (intro expr_has_density_sound_aux density_context_α) simp_all
have "⋀V. ?shift -` shift_var_set (shift_var_set V) = shift_var_set V"
by (auto simp: shift_var_set_def split: nat.split_asm)
hence nonneg': "nonneg_cexpr (shift_var_set (shift_var_set (set vs'))) (case_nat t (case_nat t' Γ)) ?expr"
by (auto intro!: nonneg_cexpr_comp nonneg_cexpr_map_vars nonneg cexpr_typing.intros cet_var')
show ?case
proof (intro conjI is_density_exprI , simp only: dens_ctxt_α_def prod.case, rule hd_AE[OF dens'])
fix ρ assume ρ: "ρ ∈ space (state_measure (set vs') Γ)"
thus "AE x in stock_measure t'. ?f ρ x = ennreal (eval_cexpr (∫⇩c ?expr ∂t) ρ x)"
using ctype vars edc_snd.hyps nonneg'
by (intro has_parametrized_subprob_density_cexpr_sem_integral[OF dens'']) auto
next
show "nonneg_cexpr (shift_var_set (set vs')) (case_nat t'' Γ) (∫⇩c ?expr ∂t)"
using nonneg' by (intro nonneg_cexpr_int) simp
qed (insert edc_snd.prems ctype vars, auto simp: measurable_split_conv
intro!: cet_int measurable_compose[OF _ measurable_ennreal]
measurable_Pair_compose_split[OF measurable_eval_cexpr])
next
case (edc_neg vs vs' Γ δ e f t)
from edc_neg.prems(1) have t: "Γ ⊢ e : t" by (cases t) (auto split: pdf_type.split_asm)
from edc_neg.prems(1) have t_disj: "t = REAL ∨ t = INTEG"
by (cases t) (auto split: pdf_type.split_asm)
from edc_neg.prems edc_neg.IH[OF t]
have dens: "dens_ctxt_α (vs, vs', Γ, δ) ⊢⇩d e ⇒ (λx xa. ennreal (eval_cexpr f x xa))" and
wf: "is_density_expr (vs, vs', Γ, δ) t f" by simp_all
have "dens_ctxt_α (vs, vs', Γ, δ) ⊢⇩d Minus $$ e ⇒ (λσ x. ennreal (eval_cexpr f σ (op_sem Minus x)))"
using dens by (simp only: dens_ctxt_α_def prod.case, intro hd_neg) simp_all
also have "(λσ x. ennreal (eval_cexpr f σ (op_sem Minus x))) =
(λσ x. ennreal (eval_cexpr (f ∘⇩c -⇩c CVar 0) σ x))"
by (intro ext) (auto simp: eval_cexpr_comp)
finally have "dens_ctxt_α (vs, vs', Γ, δ) ⊢⇩d Minus $$ e ⇒
(λσ x. ennreal (eval_cexpr (f ∘⇩c -⇩c CVar 0) σ x))" .
moreover have "is_density_expr (vs, vs', Γ, δ) t (f ∘⇩c -⇩c CVar 0)"
proof (intro is_density_exprI)
from t_disj have t_minus: "case_nat t Γ ⊢⇩c -⇩c CVar 0 : t"
by (intro cet_op[where t = t]) (auto simp: cexpr_type_Some_iff[symmetric])
thus "case_nat t Γ ⊢⇩c f ∘⇩c -⇩c CVar 0 : REAL" using is_density_exprD(1)[OF wf]
by (intro cexpr_typing_cexpr_comp[of _ _ _ t])
show "free_vars (f ∘⇩c -⇩c CVar 0) ⊆ shift_var_set (set vs')" using is_density_exprD(2)[OF wf]
by (intro order.trans[OF free_vars_cexpr_comp]) (auto simp: shift_var_set_def)
show "nonneg_cexpr (shift_var_set (set vs')) (case_nat t Γ) (f ∘⇩c -⇩c CVar 0)"
using wf[THEN is_density_exprD_nonneg] t_disj
by (intro nonneg_cexpr_comp)
(auto intro!: cet_var' cet_minus_real cet_minus_int)
qed
ultimately show ?case by (rule conjI)
next
case (edc_addc vs vs' Γ δ e f e' t)
let ?expr = "f ∘⇩c (λ⇩cx. x -⇩c map_vars Suc (expr_rf_to_cexpr e'))"
from edc_addc.prems(1)
have t1: "Γ ⊢ e : t" and t2: "Γ ⊢ e' : t" and t3: "op_type Add (PRODUCT t t) = Some t"
by (elim expr_typing_opE expr_typing_pairE, fastforce split: pdf_type.split_asm)+
from edc_addc.prems(1) have t_disj: "t = REAL ∨ t = INTEG"
by (cases t) (auto split: pdf_type.split_asm)
hence t3': "op_type Minus t = Some t" by auto
from edc_addc.prems edc_addc.IH[OF t1]
have dens: "dens_ctxt_α (vs, vs', Γ, δ) ⊢⇩d e ⇒ (λx xa. ennreal (eval_cexpr f x xa))" and
wf: "is_density_expr (vs, vs', Γ, δ) t f" by simp_all
hence ctype: "case_nat t Γ ⊢⇩c ?expr : REAL" using t1 t2 t3 t3' edc_addc.hyps edc_addc.prems
by (intro cexpr_typing_cexpr_comp cet_op[where t = "PRODUCT t t"] cet_var')
(auto intro!: cet_pair cexpr_typing_map_vars cet_var' cet_op dest: is_density_exprD simp: o_def)
have vars: "free_vars ?expr ⊆ shift_var_set (set vs')" using edc_addc.prems edc_addc.hyps
using free_vars_expr_rf_to_cexpr is_density_exprD[OF wf]
by (intro order.trans[OF free_vars_cexpr_comp subset_shift_var_set]) auto
have cet_e': "Γ ⊢ e' : t"
using edc_addc.prems(1)
apply (cases)
apply (erule expr_typing.cases)
apply (auto split: pdf_type.splits)
done
have "dens_ctxt_α (vs, vs', Γ, δ) ⊢⇩d Add $$ <e, e'> ⇒
(λσ x. ennreal (eval_cexpr f σ (op_sem Add <|x, expr_sem_rf σ (Minus $$ e')|>)))"
(is "?𝒴 ⊢⇩d _ ⇒ ?f") using dens edc_addc.hyps
by (simp only: dens_ctxt_α_def prod.case, intro hd_addc) simp_all
also have "?f = (λσ x. ennreal (eval_cexpr ?expr σ x))" using edc_addc.hyps
by (intro ext) (auto simp: eval_cexpr_comp cexpr_sem_map_vars o_def cexpr_sem_expr_rf_to_cexpr)
finally have "dens_ctxt_α (vs, vs', Γ, δ) ⊢⇩d Add $$ <e, e'> ⇒
(λσ x. ennreal (eval_cexpr ?expr σ x))" .
moreover have "is_density_expr (vs, vs', Γ, δ) t ?expr" using ctype vars
proof (intro is_density_exprI)
show "nonneg_cexpr (shift_var_set (set vs')) (case_nat t Γ) ?expr"
using t_disj edc_addc.hyps edc_addc.prems cet_e' free_vars_expr_rf_to_cexpr[of e']
by (intro nonneg_cexpr_comp[OF wf[THEN is_density_exprD_nonneg]])
(auto intro!: cet_add_int cet_add_real cet_minus_int cet_minus_real cet_var' cexpr_typing_map_vars
simp: o_def)
qed auto
ultimately show ?case by (rule conjI)
next
case (edc_multc vs vs' Γ δ e f c t)
let ?expr = "(f ∘⇩c (λ⇩cx. x *⇩c CReal (inverse c))) *⇩c CReal (inverse (abs c))"
from edc_multc.prems(1) edc_multc.hyps have t1: "Γ ⊢ e : REAL" and [simp]: "t = REAL"
by (elim expr_typing_opE expr_typing_pairE, force split: pdf_type.split_asm)+
from edc_multc.prems edc_multc.IH[OF t1]
have dens: "dens_ctxt_α (vs, vs', Γ, δ) ⊢⇩d e ⇒ (λx xa. ennreal (eval_cexpr f x xa))" and
wf: "is_density_expr (vs, vs', Γ, δ) REAL f" by simp_all
have ctype': "case_nat t Γ ⊢⇩c f ∘⇩c (λ⇩cx. x *⇩c CReal (inverse c)) : REAL"
using t1 edc_multc.hyps edc_multc.prems is_density_exprD[OF wf]
by (intro cexpr_typing_cexpr_comp)
(auto intro!: cet_pair cexpr_typing_map_vars cet_var' cet_val' cet_op_intros)
hence ctype: "case_nat t Γ ⊢⇩c ?expr : REAL"
by (auto intro!: cet_op_intros cet_pair cet_val')
have vars': "free_vars (f ∘⇩c (λ⇩cx. x *⇩c CReal (inverse c))) ⊆ shift_var_set (set vs')"
using edc_multc.prems edc_multc.hyps free_vars_expr_rf_to_cexpr is_density_exprD[OF wf]
by (intro order.trans[OF free_vars_cexpr_comp subset_shift_var_set]) auto
hence vars: "free_vars ?expr ⊆ shift_var_set (set vs')" by simp
have "dens_ctxt_α (vs, vs', Γ, δ) ⊢⇩d Mult $$ <e, Val (RealVal c)> ⇒
(λσ x. ennreal (eval_cexpr f σ (op_sem Mult <|x, op_sem Inverse (RealVal c)|>)) *
ennreal (inverse (abs (extract_real (RealVal c)))))"
(is "?𝒴 ⊢⇩d _ ⇒ ?f") using dens edc_multc.hyps
by (simp only: dens_ctxt_α_def prod.case, intro hd_multc) simp_all
hence "dens_ctxt_α (vs, vs', Γ, δ) ⊢⇩d Mult $$ <e, Val (RealVal c)> ⇒
(λσ x. ennreal (eval_cexpr ?expr σ x))"
proof (simp only: dens_ctxt_α_def prod.case, erule_tac hd_cong)
fix ρ x assume ρ: "ρ ∈ space (state_measure (set vs') Γ)" and x: "x ∈ space (stock_measure REAL)"
hence "eval_cexpr ?expr ρ x =
extract_real (cexpr_sem (case_nat x ρ) (f ∘⇩c CVar 0 *⇩c CReal (inverse c))) * inverse ¦c¦"
(is "_ = ?a * ?b") unfolding eval_cexpr_def
by (subst cexpr_sem_Mult[OF ctype' cet_val' _ vars'])
(auto simp: extract_real_def simp del: stock_measure.simps)
also hence "?a = eval_cexpr f ρ (op_sem Mult <|x, op_sem Inverse (RealVal c)|>)"
by (auto simp: cexpr_sem_cexpr_comp eval_cexpr_def lift_RealVal_def lift_RealIntVal2_def)
finally show "ennreal (eval_cexpr f ρ (op_sem Mult <|x, op_sem Inverse (RealVal c)|>)) *
ennreal (inverse ¦extract_real (RealVal c)¦) = ennreal (eval_cexpr ?expr ρ x)"
by (simp add: extract_real_def ennreal_mult'')
qed (insert edc_multc.prems, auto intro!: density_context_α)
moreover have "is_density_expr (vs, vs', Γ, δ) t ?expr" using ctype vars
proof (intro is_density_exprI)
show "nonneg_cexpr (shift_var_set (set vs')) (case_nat t Γ) ?expr"
using is_density_exprD[OF wf] vars vars'
by (intro nonneg_cexpr_comp[OF wf[THEN is_density_exprD_nonneg]] nonneg_cexpr_Mult ctype')
(auto intro!: nonneg_cexprI cet_var' cet_val' cet_op_intros)
qed auto
ultimately show ?case by (rule conjI)
next
case (edc_add vs vs' Γ δ e f t t')
note t = ‹Γ ⊢ e : PRODUCT t t›
note invar = cdens_ctxt_invarD[OF edc_add.prems(2)]
from edc_add.prems and t have "op_type Add (PRODUCT t t) = Some t'"
by (elim expr_typing_opE) (auto dest: expr_typing_unique)
hence [simp]: "t' = t" and t_disj: "t = INTEG ∨ t = REAL" by (auto split: pdf_type.split_asm)
have dens: "dens_ctxt_α (vs, vs', Γ, δ) ⊢⇩d e ⇒ (λx xa. ennreal (eval_cexpr f x xa))" and
wf: "is_density_expr (vs, vs', Γ, δ) (PRODUCT t t) f"
using edc_add by simp_all
note wf' = is_density_exprD[OF wf]
let ?𝒴 = "(set vs, set vs', Γ, λρ. ennreal (extract_real (cexpr_sem ρ δ)))"
let ?M = "λρ. dens_ctxt_measure ?𝒴 ρ ⤜ (λσ. expr_sem σ e)"
have nonneg: "nonneg_cexpr (shift_var_set (set vs')) (case_nat (PRODUCT t t) Γ) f"
using wf by (rule is_density_exprD_nonneg)
let ?shift = "case_nat 0 (λx. x + 2)"
let ?expr' = "map_vars ?shift f ∘⇩c (λ⇩cx. <x, CVar 1 -⇩c x>⇩c)"
let ?expr = "∫⇩c ?expr' ∂t"
have [simp]: "⋀t t' Γ. case_nat t (case_nat t' Γ) ∘ case_nat 0 (λx. Suc (Suc x)) = case_nat t Γ"
by (intro ext) (simp split: nat.split add: o_def)
have ctype'': "case_nat t (case_nat t Γ) ⊢⇩c <CVar 0, CVar 1 -⇩c CVar 0>⇩c : PRODUCT t t"
by (rule cet_pair, simp add: cet_var', rule cet_op[where t = "PRODUCT t t"], rule cet_pair)
(insert t_disj, auto intro!: cet_var' cet_op[where t = t])
hence ctype': "case_nat t (case_nat t Γ) ⊢⇩c ?expr' : REAL" using wf'
by (intro cexpr_typing_cexpr_comp cexpr_typing_map_vars) simp_all
hence ctype: "case_nat t Γ ⊢⇩c ?expr : REAL" by (rule cet_int)
have vars': "free_vars ?expr' ⊆ shift_var_set (shift_var_set (set vs'))" using wf'
by (intro order.trans[OF free_vars_cexpr_comp]) (auto split: nat.split simp: shift_var_set_def)
hence vars: "free_vars ?expr ⊆ shift_var_set (set vs')" by auto
let ?M = "λρ. dens_ctxt_measure ?𝒴 ρ ⤜ (λσ. expr_sem σ (Add $$ e))"
let ?f = "λρ x y. eval_cexpr f ρ <|y, op_sem Add <|x, op_sem Minus y|>|>"
have "?𝒴 ⊢⇩d Add $$ e ⇒ (λρ x. ∫⇧+y. ?f ρ x y ∂stock_measure (val_type x))" using dens
by (intro hd_add) (simp add: dens_ctxt_α_def)
hence dens: "?𝒴 ⊢⇩d Add $$ e ⇒ (λρ x. ∫⇧+y. eval_cexpr ?expr' (case_nat x ρ) y ∂stock_measure t)"
by (rule hd_cong) (insert edc_add.prems, auto intro!: density_context_α nn_integral_cong
simp: eval_cexpr_def cexpr_sem_cexpr_comp cexpr_sem_map_vars)
hence dens': "has_parametrized_subprob_density (state_measure (set vs') Γ) ?M (stock_measure t)
(λρ x. ∫⇧+y. eval_cexpr ?expr' (case_nat x ρ) y ∂stock_measure t)"
using edc_add.prems by (intro expr_has_density_sound_aux density_context_α) simp_all
show ?case
proof (intro conjI is_density_exprI, simp only: dens_ctxt_α_def prod.case, rule hd_AE[OF dens])
fix ρ assume ρ: "ρ ∈ space (state_measure (set vs') Γ)"
let ?dens = "λx. ∫⇧+y. eval_cexpr ?expr' (case_nat x ρ) y ∂stock_measure t"
show "AE x in stock_measure t. ?dens x = ennreal (eval_cexpr ?expr ρ x)"
proof (rule AE_mp[OF _ AE_I2[OF impI]])
from has_parametrized_subprob_density_integral[OF dens' ρ] and
has_parametrized_subprob_densityD(3)[OF dens'] and ρ
show "AE x in stock_measure t. ?dens x ≠ ∞" by (intro nn_integral_PInf_AE) auto
next
fix x assume x: "x ∈ space (stock_measure t)" and fin: "?dens x ≠ ∞"
thus "?dens x = ennreal (eval_cexpr ?expr ρ x)"
using ρ vars' ctype' ctype'' nonneg unfolding eval_cexpr_def
by (subst cexpr_sem_integral_nonneg) (auto intro!: nonneg_cexpr_comp nonneg_cexpr_map_vars simp: less_top)
qed
next
show "nonneg_cexpr (shift_var_set (set vs')) (case_nat t' Γ) ?expr"
using ctype'' nonneg
by (intro nonneg_cexpr_int nonneg_cexpr_comp[of _ "PRODUCT t t"] nonneg_cexpr_map_vars)
auto
qed (insert vars ctype edc_add.prems, auto)
next
case (edc_inv vs vs' Γ δ e f t)
hence t: "Γ ⊢ e : t" and [simp]: "t = REAL"
by (elim expr_typing_opE, force split: pdf_type.split_asm)+
note invar = cdens_ctxt_invarD[OF edc_inv.prems(2)]
let ?expr = "(f ∘⇩c (λ⇩cx. inverse⇩c x)) *⇩c (λ⇩cx. (inverse⇩c x) ^⇩c CInt 2)"
have dens: "dens_ctxt_α (vs, vs', Γ, δ) ⊢⇩d e ⇒ (λρ x. ennreal (eval_cexpr f ρ x))" and
wf: "is_density_expr (vs, vs', Γ, δ) REAL f" using edc_inv t by simp_all
note wf' = is_density_exprD[OF wf]
from wf' have ctype: "case_nat REAL Γ ⊢⇩c ?expr : REAL"
by (auto intro!: cet_op_intros cexpr_typing_cexpr_comp cet_var' cet_val')
from wf' have vars': "free_vars (f ∘⇩c (λ⇩cx. inverse⇩c x)) ⊆ shift_var_set (set vs')"
by (intro order.trans[OF free_vars_cexpr_comp]) auto
hence vars: "free_vars ?expr ⊆ shift_var_set (set vs')" using free_vars_cexpr_comp by simp
show ?case
proof (intro conjI is_density_exprI, simp only: dens_ctxt_α_def prod.case, rule hd_cong[OF hd_inv])
fix ρ x assume ρ: "ρ ∈ space (state_measure (set vs') Γ)"
and x: "x ∈ space (stock_measure REAL)"
from x obtain x' where [simp]: "x = RealVal x'" by (auto simp: val_type_eq_REAL)
from ρ and wf' have "val_type (cexpr_sem (case_nat (RealVal (inverse x')) ρ) f) = REAL"
by (intro val_type_cexpr_sem[OF _ _ case_nat_in_state_measure ])
(auto simp: type_universe_def simp del: type_universe_type)
thus "ennreal (eval_cexpr f ρ (op_sem Inverse x)) * ennreal ((inverse (extract_real x))⇧2) =
ennreal (eval_cexpr ?expr ρ x)"
by (auto simp: eval_cexpr_def lift_RealVal_def lift_RealIntVal2_def ennreal_mult''
extract_real_def cexpr_sem_cexpr_comp elim!: REAL_E)
next
have "nonneg_cexpr (shift_var_set (set vs')) (case_nat REAL Γ) (inverse⇩c (CVar 0) ^⇩c CInt 2)"
by (auto intro!: nonneg_cexprI simp: space_state_measure_shift_iff val_type_eq_REAL lift_RealVal_eq)
then show "nonneg_cexpr (shift_var_set (set vs')) (case_nat t Γ) ?expr"
using wf'
by (intro nonneg_cexpr_Mult nonneg_cexpr_comp vars')
(auto intro!: cet_op_intros cexpr_typing_cexpr_comp cet_var' cet_val')
qed (insert edc_inv.prems ctype vars dens,
auto intro!: density_context_α simp: dens_ctxt_α_def)
next
case (edc_exp vs vs' Γ δ e f t)
hence t: "Γ ⊢ e : t" and [simp]: "t = REAL"
by (elim expr_typing_opE, force split: pdf_type.split_asm)+
note invar = cdens_ctxt_invarD[OF edc_exp.prems(2)]
let ?expr = "(λ⇩cx. IF⇩c CReal 0 <⇩c x THEN (f ∘⇩c ln⇩c x) *⇩c inverse⇩c x ELSE CReal 0)"
have dens: "dens_ctxt_α (vs, vs', Γ, δ) ⊢⇩d e ⇒ (λρ x. ennreal (eval_cexpr f ρ x))" and
wf: "is_density_expr (vs, vs', Γ, δ) REAL f" using edc_exp t by simp_all
note wf' = is_density_exprD[OF wf]
from wf' have ctype: "case_nat REAL Γ ⊢⇩c ?expr : REAL"
by (auto intro!: cet_if cet_op_intros cet_var' cet_val' cexpr_typing_cexpr_comp)
from wf' have "free_vars (f ∘⇩c (λ⇩cx. ln⇩c x)) ⊆ shift_var_set (set vs')"
by (intro order.trans[OF free_vars_cexpr_comp]) auto
hence vars: "free_vars ?expr ⊆ shift_var_set (set vs')" using free_vars_cexpr_comp by simp
show ?case
proof (intro conjI is_density_exprI, simp only: dens_ctxt_α_def prod.case, rule hd_cong[OF hd_exp])
fix ρ x assume ρ: "ρ ∈ space (state_measure (set vs') Γ)"
and x: "x ∈ space (stock_measure REAL)"
from x obtain x' where [simp]: "x = RealVal x'" by (auto simp: val_type_eq_REAL)
from ρ and wf' have "val_type (cexpr_sem (case_nat (RealVal (ln x')) ρ) f) = REAL"
by (intro val_type_cexpr_sem[OF _ _ case_nat_in_state_measure ])
(auto simp: type_universe_def simp del: type_universe_type)
thus "(if 0 < extract_real x then ennreal (eval_cexpr f ρ (lift_RealVal safe_ln x)) *
ennreal (inverse (extract_real x)) else 0) = ennreal (eval_cexpr ?expr ρ x)"
by (auto simp: eval_cexpr_def lift_RealVal_def lift_RealIntVal2_def lift_Comp_def ennreal_mult''
extract_real_def cexpr_sem_cexpr_comp elim!: REAL_E)
next
show "nonneg_cexpr (shift_var_set (set vs')) (case_nat t Γ) ?expr"
proof (rule nonneg_cexprI_shift)
fix x σ assume "x ∈ type_universe t" and σ: "σ ∈ space (state_measure (set vs') Γ)"
then obtain r where "x = RealVal r"
by (auto simp: val_type_eq_REAL)
moreover note σ nonneg_cexprD[OF is_density_exprD_nonneg[OF wf], of "case_nat (RealVal (ln r)) σ"]
moreover have "val_type (cexpr_sem (case_nat (RealVal (ln r)) σ) f) = REAL"
using σ by (intro val_type_cexpr_sem[OF wf'(1,2)] case_nat_in_state_measure) auto
ultimately show "0 ≤ extract_real
(cexpr_sem (case_nat x σ)
(IF⇩c CReal 0 <⇩c CVar 0 THEN (f ∘⇩c ln⇩c (CVar 0)) /⇩c CVar 0 ELSE CReal 0))"
by (auto simp: lift_Comp_def lift_RealVal_eq cexpr_sem_cexpr_comp val_type_eq_REAL
case_nat_in_state_measure lift_RealIntVal2_def)
qed
qed (insert edc_exp.prems ctype vars dens,
auto intro!: density_context_α simp: dens_ctxt_α_def)
qed
lemma expr_has_density_cexpr_sound:
assumes "([], [], Γ, CReal 1) ⊢⇩c e ⇒ f" "Γ ⊢ e : t" "free_vars e = {}"
shows "has_subprob_density (expr_sem σ e) (stock_measure t) (λx. ennreal (eval_cexpr f σ x))"
"∀x∈type_universe t. 0 ≤ extract_real (cexpr_sem (case_nat x σ) f)"
"Γ' 0 = t ⟹ Γ' ⊢⇩c f : REAL"
"free_vars f ⊆ {0}"
proof-
have "dens_ctxt_α ([], [], Γ, CReal 1) ⊢⇩d e ⇒ (λρ x. ennreal (eval_cexpr f ρ x)) ∧
is_density_expr ([], [], Γ, CReal 1) t f" using assms
by (intro expr_has_density_cexpr_sound_aux assms cdens_ctxt_invarI nonneg_cexprI subprob_cexprI)
(auto simp: state_measure_def PiM_empty cexpr_type_Some_iff[symmetric] extract_real_def)
hence dens: "dens_ctxt_α ([], [], Γ, CReal 1) ⊢⇩d e ⇒ (λρ x. ennreal (eval_cexpr f ρ x))"
and wf: "is_density_expr ([], [], Γ, CReal 1) t f" using assms by blast+
have "has_subprob_density (expr_sem σ e) (stock_measure t)
(λx. ennreal (eval_cexpr f (λ_. undefined) x))" (is ?P) using dens assms
by (intro expr_has_density_sound) (auto simp: dens_ctxt_α_def extract_real_def one_ennreal_def)
also have "⋀x. cexpr_sem (case_nat x (λ_. undefined)) f = cexpr_sem (case_nat x σ) f"
using is_density_exprD[OF wf]
by (intro cexpr_sem_eq_on_vars) (auto split: nat.split simp: shift_var_set_def)
hence "?P ⟷ has_subprob_density (expr_sem σ e) (stock_measure t)
(λx. ennreal (eval_cexpr f σ x))"
by (intro has_subprob_density_cong) (simp add: eval_cexpr_def)
finally show "..." .
from is_density_exprD[OF wf] show vars: "free_vars f ⊆ {0}" by (auto simp: shift_var_set_def)
show "∀x∈type_universe t. 0 ≤ extract_real (cexpr_sem (case_nat x σ) f)"
proof
fix v assume v: "v ∈ type_universe t"
then have "0 ≤ extract_real (cexpr_sem (case_nat v (λ_. undefined)) f)"
by (intro nonneg_cexprD[OF wf[THEN is_density_exprD_nonneg]] case_nat_in_state_measure)
(auto simp: space_state_measure)
also have "cexpr_sem (case_nat v (λ_. undefined)) f = cexpr_sem (case_nat v σ) f"
using ‹free_vars f ⊆ {0}› by (intro cexpr_sem_eq_on_vars) auto
finally show "0 ≤ extract_real (cexpr_sem (case_nat v σ) f)" .
qed
assume "Γ' 0 = t"
thus "Γ' ⊢⇩c f : REAL"
by (intro cexpr_typing_cong'[OF is_density_exprD(1)[OF wf]])
(insert vars, auto split: nat.split)
qed
inductive expr_compiles_to :: "expr ⇒ pdf_type ⇒ cexpr ⇒ bool" (‹_ : _ ⇒⇩c _› [10,0,10] 10)
for e t f where
"(λ_. UNIT) ⊢ e : t ⟹ free_vars e = {} ⟹
([], [], λ_. UNIT, CReal 1) ⊢⇩c e ⇒ f ⟹
e : t ⇒⇩c f"
code_pred expr_compiles_to .
lemma expr_compiles_to_sound:
assumes "e : t ⇒⇩c f"
shows "expr_sem σ e = density (stock_measure t) (λx. ennreal (eval_cexpr f σ' x))"
"∀x∈type_universe t. eval_cexpr f σ' x ≥ 0"
"Γ ⊢ e : t"
"t ⋅ Γ' ⊢⇩c f : REAL"
"free_vars f ⊆ {0}"
proof-
let ?Γ = "λ_. UNIT"
from assms have A: "([], [], ?Γ, CReal 1) ⊢⇩c e ⇒ f" "?Γ ⊢ e : t" "free_vars e = {}"
by (simp_all add: expr_compiles_to.simps)
hence "expr_sem σ e = expr_sem σ' e" by (intro expr_sem_eq_on_vars) simp
with expr_has_density_cexpr_sound[OF A]
show "expr_sem σ e = density (stock_measure t) (λx. ennreal (eval_cexpr f σ' x))"
"∀x∈type_universe t. eval_cexpr f σ' x ≥ 0"
"t ⋅ Γ' ⊢⇩c f : REAL"
"free_vars f ⊆ {0}" unfolding has_subprob_density_def has_density_def eval_cexpr_def
by (auto intro!: nonneg_cexprD case_nat_in_state_measure)
from assms have "(λ_. UNIT) ⊢ e : t" by (simp add: expr_compiles_to.simps)
from this and assms show "Γ ⊢ e : t"
by (subst expr_typing_cong) (auto simp: expr_compiles_to.simps)
qed
section ‹Tests›
values "{(t, f) |t f. Val (IntVal 42) : t ⇒⇩c f}"
values "{(t, f) |t f. Minus $$ (Val (IntVal 42)) : t ⇒⇩c f}"
values "{(t, f) |t f. Fst $$ (Val <|IntVal 13, IntVal 37|>) : t ⇒⇩c f}"
values "{(t, f) |t f. Random Bernoulli (Val (RealVal 0.5)) : t ⇒⇩c f}"
values "{(t, f) |t f. Add $$ <Val (IntVal 37), Minus $$ (Val (IntVal 13))> : t ⇒⇩c f}"
values "{(t, f) |t f. LET Val (IntVal 13) IN LET Minus $$ (Val (IntVal 37)) IN
Add $$ <Var 0, Var 1> : t ⇒⇩c f}"
values "{(t, f) |t f. IF Random Bernoulli (Val (RealVal 0.5)) THEN
Random Bernoulli (Val (RealVal 0.25))
ELSE
Random Bernoulli (Val (RealVal 0.75)) : t ⇒⇩c f}"
values "{(t, f) |t f. LET Random Bernoulli (Val (RealVal 0.5)) IN
IF Var 0 THEN
Random Bernoulli (Val (RealVal 0.25))
ELSE
Random Bernoulli (Val (RealVal 0.75)) : t ⇒⇩c f}"
values "{(t, f) |t f. LET Random Gaussian <Val (RealVal 0), Val (RealVal 1)> IN
LET Random Gaussian <Val (RealVal 0), Val (RealVal 1)> IN
Add $$ <Var 0, Var 1> : t ⇒⇩c f}"
values "{(t, f) |t f. LET Random UniformInt <Val (IntVal 1), Val (IntVal 6)> IN
LET Random UniformInt <Val (IntVal 1), Val (IntVal 6)> IN
Add $$ <Var 0, Var 1> : t ⇒⇩c f}"
values "{(t, f) |t f. LET Random UniformReal <Val (RealVal 0), Val (RealVal 1)> IN
LET Random Bernoulli (Var 0) IN
IF Var 0 THEN Add $$ <Var 1, Val (RealVal 1)> ELSE Var 1 : t ⇒⇩c f}"
definition "cthulhu skill ≡
LET Random UniformInt (Val <|IntVal 1, IntVal 100|>)
IN IF Less $$ <Val (IntVal skill), Var 0> THEN
Val (IntVal skill)
ELSE IF Or $$ <Less $$ <Var 0, Val (IntVal 6)>,
Less $$ <Mult $$ <Var 0, Val (IntVal 5)>,
Add $$ <Val (IntVal skill), Val (IntVal 1)> > > THEN
Add $$ <IF Less $$ <Val (IntVal skill),
Random UniformInt <Val (IntVal 1), Val (IntVal 100)> > THEN
Random UniformInt <Val (IntVal 1), Val (IntVal 10)>
ELSE
Val (IntVal 0),
Val (IntVal skill)>
ELSE Val (IntVal skill)"
definition "cthulhu' (skill :: int) =
LET Random UniformInt (Val <|IntVal 1, IntVal 100|>)
IN IF Less $$ <Val (IntVal skill), Var 0> THEN
Val (IntVal skill)
ELSE IF Or $$ <Less $$ <Var 0, Val (IntVal 6)>,
Less $$ <Mult $$ <Var 0, Val (IntVal 5)>,
Add $$ <Val (IntVal skill), Val (IntVal 1)> > > THEN
LET Random UniformInt (Val <|IntVal 1, IntVal 100|>)
IN Add $$ <IF Less $$ <Val (IntVal skill), Var 1 > THEN
Random UniformInt (Val <|IntVal 1, IntVal 10|>)
ELSE
Val (IntVal 0),
Val (IntVal skill)>
ELSE Val (IntVal skill)"
values "{(t, f) |t f. cthulhu' 42 : t ⇒⇩c f}"
end