Theory PDF_Compiler

(*
  Theory: PDF_Compiler.thy
  Authors: Manuel Eberl

  The concrete compiler that compiles a PDF expression into a target language expression
  that describes a density function on the corresponding measure space.
*)

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_equiv:  "cexpr_equiv f1 f2 ⟹ Γ ⊢ e : t ⟹ is_density_expr (vs,vs',Γ,δ) t f2 ⟹
                       (vs, vs', Γ, δ)  ⊢c e ⇒ f1 ⟹ (vs, vs', Γ, δ)  ⊢c e ⇒ f2"*)
  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. inversec x)) *c (λcx. (inversec x) ^c CInt 2)"
| edc_exp:      "(vs, vs', Γ, δ) ⊢c e ⇒ f ⟹
                     (vs, vs', Γ, δ) ⊢c Exp $$ e ⇒
                         (λcx. IFc CReal 0 <c x THEN (f ∘c lnc x) *c inversec 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_equiv f1 f2 Γ e t vs vs' δ t')
  hence [simp]: "t' = t" by (auto intro!: expr_typing_unique)
  from edc_equiv have "(λρ x. ennreal (eval_cexpr f1 ρ x)) = (λρ x. ennreal (eval_cexpr f2 ρ x))"
    unfolding cexpr_equiv_def eval_cexpr_def by (intro ext) auto
  with edc_equiv show ?case unfolding dens_ctxt_α_def by auto

next*)
  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. inversec x)) *c (λcx. (inversec 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. inversec 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 Γ) (inversec (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. IFc CReal 0 <c x THEN (f ∘c lnc x) *c inversec 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. lnc 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 σ)
                   (IFc CReal 0 <c CVar 0 THEN (f ∘c lnc (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}"


(* Example from the paper by Bhat et.al. *)

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

(* Simplification of constant expression yields:
  ∫b. (IF 0 ≤ x - 1 ∧ x - 1 ≤ 1 THEN 1 ELSE 0) *
      (IF 0 ≤ x - 1 ∧ x - 1 ≤ 1 THEN IF b THEN x - 1 ELSE 1 - (x - 1) ELSE 0) * ⟨b⟩ +
  ∫b. (IF 0 ≤ x ∧ x ≤ 1 THEN 1 ELSE 0) *
      (IF 0 ≤ x ∧ x ≤ 1 THEN IF b THEN x ELSE 1 - x ELSE 0) * ⟨¬b⟩
*)

(* Further simplification yields:
   (∫b. ⟨0 ≤ x-1 ≤ 1⟩ * (IF b THEN x-1 ELSE 2-x) * ⟨b⟩) +
   (∫b. ⟨0 ≤ x ≤ 1⟩ * (IF b THEN x ELSE 1-x) * ⟨¬b⟩)
*)

(* Further simplification yields:
  ⟨1 ≤ x ≤ 2⟩*(x-1) + ⟨0 ≤ x ≤ 1⟩*(1-x)
*)

(* Mathematica input:
   Piecewise[{{x-1, 1 <= x && x <= 2}, {1-x, 0 <= x && x <= 1}}]
*)

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