Theory PDF_Target_Semantics

(*
  Theory: PDF_Target_Semantics.thy
  Authors: Manuel Eberl

  The semantics of the target language.
*)

section ‹Target Language Syntax and Semantics›

theory PDF_Target_Semantics
imports PDF_Semantics
begin

datatype cexpr =
    CVar vname
  | CVal val
  | CPair cexpr cexpr ("<_, _>c" [0, 0] 1000)
  | COperator pdf_operator cexpr (infixl "$$c" 999)
  | CIf cexpr cexpr cexpr ("IFc _ THEN _ ELSE _" [0, 0, 10] 10)
  | CIntegral cexpr pdf_type ("∫c _ ∂_" [61] 110)

abbreviation (input) cexpr_fun :: "(cexpr ⇒ cexpr) ⇒ cexpr" (binder "λc" 10) where
  "cexpr_fun f ≡ f (CVar 0)"
abbreviation cexpr_Add (infixl "+c" 65) where
  "cexpr_Add a b ≡ Add $$c <a, b>c"
abbreviation cexpr_Minus ("-c _" [81] 80) where
  "cexpr_Minus a ≡ Minus $$c a"
abbreviation cexpr_Sub (infixl "-c" 65) where
  "cexpr_Sub a b ≡ a +c -cb"
abbreviation cexpr_Mult (infixl "*c" 70) where
  "cexpr_Mult a b ≡ Mult $$c <a, b>c"
abbreviation "inversec e ≡Inverse $$c e"
abbreviation cexpr_Div (infixl "'/c" 70) where
  "cexpr_Div a b ≡ a *c inversec b"
abbreviation "factc e ≡ Fact $$c e"
abbreviation "sqrtc e ≡ Sqrt $$c e"
abbreviation "expc e ≡ Exp $$c e"
abbreviation "lnc e ≡ Ln $$c e"
abbreviation "fstc e ≡ Fst $$c e"
abbreviation "sndc e ≡ Snd $$c e"
abbreviation cexpr_Pow (infixl "^c" 75) where
  "cexpr_Pow a b ≡ Pow $$c <a, b>c"
abbreviation cexpr_And (infixl "∧c" 35) where
  "cexpr_And a b ≡ And $$c <a, b>c"
abbreviation cexpr_Or (infixl "∨c" 30) where
  "cexpr_Or a b ≡ Or $$c <a, b>c"
abbreviation cexpr_Not ("¬c _" [40] 40) where
  "cexpr_Not a ≡ Not $$c a"
abbreviation cexpr_Equals (infixl "=c" 70) where
  "cexpr_Equals a b ≡ Equals $$c <a, b>c"
abbreviation cexpr_Less (infixl "<c" 70) where
  "cexpr_Less a b ≡ Less $$c <a, b>c"
abbreviation cexpr_LessEq (infixl "≤c" 70) where
  "cexpr_LessEq a b ≡ a =c b ∨c a <c b"
abbreviation cexpr_RealCast ("⟨_⟩c" [0] 90) where
  "cexpr_RealCast a ≡ Cast REAL $$c a"
abbreviation CReal where
  "CReal x ≡ CVal (RealVal x)"
abbreviation CInt where
  "CInt x ≡ CVal (IntVal x)"
abbreviation πc where
  "πc ≡ Pi $$c (CVal UnitVal)"

instantiation cexpr :: expr
begin

primrec free_vars_cexpr :: "cexpr ⇒ vname set" where
  "free_vars_cexpr (CVar x) = {x}"
| "free_vars_cexpr (CVal _) = {}"
| "free_vars_cexpr (oper $$c e) = free_vars_cexpr e"
| "free_vars_cexpr (<e1, e2>c) = free_vars_cexpr e1 ∪ free_vars_cexpr e2"
| "free_vars_cexpr (IFc b THEN e1 ELSE e2) =
       free_vars_cexpr b ∪ free_vars_cexpr e1 ∪ free_vars_cexpr e2"
| "free_vars_cexpr (∫c e ∂t) = Suc -` free_vars_cexpr e"

instance ..
end

inductive cexpr_typing :: "tyenv ⇒ cexpr ⇒ pdf_type ⇒ bool" ("(1_/ ⊢c/ (_ :/ _))" [50,0,50] 50) where
  cet_val:    "Γ ⊢c CVal v: val_type v"
| cet_var:    "Γ ⊢c CVar x : Γ x"
| cet_pair:   "Γ ⊢c e1 : t1 ⟹ Γ ⊢c e2 : t2 ⟹ Γ ⊢c <e1, e2>c : PRODUCT t1 t2"
| cet_op:     "Γ ⊢c e : t ⟹ op_type oper t = Some t' ⟹ Γ ⊢c oper $$c e : t'"
| cet_if:     "Γ ⊢c b : BOOL ⟹ Γ ⊢c e1 : t ⟹ Γ ⊢c e2 : t
                   ⟹ Γ ⊢c IFc b THEN e1 ELSE e2 : t"
| cet_int:    "t ⋅ Γ ⊢c e : REAL ⟹ Γ ⊢c ∫c e ∂t : REAL"

lemma cet_val': "t = val_type v ⟹ Γ ⊢c CVal v : t"
  by (simp add: cet_val)

lemma cet_var': "t = Γ x ⟹ Γ ⊢c CVar x : t"
  by (simp add: cet_var)

lemma cet_not: "Γ ⊢c e : BOOL ⟹ Γ ⊢c ¬c e : BOOL"
  by (intro cet_op[where t = "BOOL"] cet_pair, simp, simp)

lemma cet_and: "Γ ⊢c e1 : BOOL ⟹ Γ ⊢c e2 : BOOL ⟹ Γ ⊢c e1 ∧c e2 : BOOL" and
      cet_or: "Γ ⊢c e1 : BOOL ⟹ Γ ⊢c e2 : BOOL ⟹ Γ ⊢c e1 ∨c e2 : BOOL"
  by (intro cet_op[where t = "PRODUCT BOOL BOOL"] cet_pair, simp, simp, simp)+

lemma cet_minus_real: "Γ ⊢c e : REAL ⟹ Γ ⊢c -ce : REAL" and
      cet_inverse: "Γ ⊢c e : REAL ⟹ Γ ⊢c inversec e : REAL" and
      cet_sqrt: "Γ ⊢c e : REAL ⟹ Γ ⊢c sqrtc e : REAL" and
      cet_exp: "Γ ⊢c e : REAL ⟹ Γ ⊢c expc e : REAL" and
      cet_ln: "Γ ⊢c e : REAL ⟹ Γ ⊢c lnc e : REAL"
  by (rule cet_op[where t = "REAL"], simp, simp)+

lemma cet_pow_real: "Γ ⊢c e1 : REAL ⟹ Γ ⊢c e2 : INTEG ⟹ Γ ⊢c e1 ^c e2 : REAL"
  by (intro cet_op[where t = "PRODUCT REAL INTEG"] cet_pair) simp_all

lemma cet_add_real: "Γ ⊢c e1 : REAL ⟹ Γ ⊢c e2 : REAL ⟹ Γ ⊢c e1 +c e2 : REAL" and
      cet_mult_real: "Γ ⊢c e1 : REAL ⟹ Γ ⊢c e2 : REAL ⟹ Γ ⊢c e1 *c e2 : REAL" and
      cet_less_real: "Γ ⊢c e1 : REAL ⟹ Γ ⊢c e2 : REAL ⟹ Γ ⊢c e1 <c e2 : BOOL"
  by (intro cet_op[where t = "PRODUCT REAL REAL"] cet_pair, simp, simp, simp)+


lemma cet_eq: "Γ ⊢c e1 : t ⟹ Γ ⊢c e2 : t ⟹ Γ ⊢c e1 =c e2 : BOOL"
  by (intro cet_op[where t = "PRODUCT t t"] cet_pair, simp, simp, simp)+

lemma cet_less_eq_real: "Γ ⊢c e1 : REAL ⟹ Γ ⊢c e2 : REAL ⟹ Γ ⊢c e1 ≤c e2 : BOOL"
  by (intro cet_less_real cet_or cet_eq)

lemma cet_minus_int: "Γ ⊢c e : INTEG ⟹ Γ ⊢c -ce : INTEG"
  by (rule cet_op[where t = "INTEG"], simp, simp)+

lemma cet_add_int: "Γ ⊢c e1 : INTEG ⟹ Γ ⊢c e2 : INTEG ⟹ Γ ⊢c e1 +c e2 : INTEG" and
      cet_mult_int: "Γ ⊢c e1 : INTEG ⟹ Γ ⊢c e2 : INTEG ⟹ Γ ⊢c e1 *c e2 : INTEG" and
      cet_less_int: "Γ ⊢c e1 : INTEG ⟹ Γ ⊢c e2 : INTEG ⟹ Γ ⊢c e1 <c e2 : BOOL"
  by (intro cet_op[where t = "PRODUCT INTEG INTEG"] cet_pair, simp, simp, simp)+

lemma cet_less_eq_int: "Γ ⊢c e1 : INTEG ⟹ Γ ⊢c e2 : INTEG ⟹ Γ ⊢c e1 ≤c e2 : BOOL"
  by (intro cet_less_int cet_or cet_eq)

lemma cet_sub_int: "Γ ⊢c e1 : INTEG ⟹ Γ ⊢c e2 : INTEG ⟹ Γ ⊢c e1 -c e2 : INTEG"
  by (intro cet_minus_int cet_add_int)

lemma cet_fst: "Γ ⊢c e : PRODUCT t t' ⟹ Γ ⊢c fstc e : t" and
      cet_snd: "Γ ⊢c e : PRODUCT t t' ⟹ Γ ⊢c sndc e : t'"
  by (erule cet_op, simp)+

lemma cet_cast_real: "Γ ⊢c e : BOOL ⟹ Γ ⊢c ⟨e⟩c : REAL"
  by (intro cet_op[where t = BOOL]) simp_all

lemma cet_cast_real_int: "Γ ⊢c e : INTEG ⟹ Γ ⊢c ⟨e⟩c : REAL"
  by (intro cet_op[where t = INTEG]) simp_all

lemma cet_sub_real: "Γ ⊢c e1 : REAL ⟹ Γ ⊢c e2 : REAL ⟹ Γ ⊢c e1 -c e2 : REAL"
  by (intro cet_minus_real cet_add_real)

lemma cet_pi: "Γ ⊢c πc : REAL"
  by (rule cet_op, rule cet_val, simp)

lemmas cet_op_intros =
  cet_minus_real cet_exp cet_sqrt cet_ln cet_inverse cet_pow_real cet_pi
  cet_cast_real cet_add_real cet_mult_real cet_less_real
  cet_not cet_and cet_or

inductive_cases cexpr_typing_valE[elim]:  "Γ ⊢c CVal v : t"
inductive_cases cexpr_typing_varE[elim]:  "Γ ⊢c CVar x : t"
inductive_cases cexpr_typing_pairE[elim]: "Γ ⊢c <e1, e2>c : t"
inductive_cases cexpr_typing_opE[elim]:   "Γ ⊢c oper $$c e : t"
inductive_cases cexpr_typing_ifE[elim]:   "Γ ⊢c IFc b THEN e1 ELSE e2 : t"
inductive_cases cexpr_typing_intE[elim]:  "Γ ⊢c ∫c e ∂t : t'"

primrec cexpr_type :: "tyenv ⇒ cexpr ⇒ pdf_type option" where
  "cexpr_type _ (CVal v) = Some (val_type v)"
| "cexpr_type Γ (CVar x) = Some (Γ x)"
| "cexpr_type Γ (<e1, e2>c) = (case (cexpr_type Γ e1, cexpr_type Γ e2) of
                                (Some t1, Some t2) ⇒ Some (PRODUCT t1 t2)
                              | _ ⇒ None)"
| "cexpr_type Γ (oper $$c e) = (case cexpr_type Γ e of
                                 Some t ⇒ op_type oper t
                               | _ ⇒ None)"
| "cexpr_type Γ (IFc b THEN e1 ELSE e2) =
                              (if cexpr_type Γ b = Some BOOL then
                                 case (cexpr_type Γ e1, cexpr_type Γ e2) of
                                   (Some t, Some t') ⇒ if t = t' then Some t else None
                                 | _ ⇒ None
                               else None)"
| "cexpr_type Γ (∫c e ∂t) =
      (if cexpr_type (case_nat t Γ) e = Some REAL then Some REAL else None)"

lemma cexpr_type_Some_iff: "cexpr_type Γ e = Some t ⟷ Γ ⊢c e : t"
  apply rule
  apply (induction e arbitrary: Γ t,
         auto intro!: cexpr_typing.intros split: option.split_asm if_split_asm) []
  apply (induction rule: cexpr_typing.induct, auto)
  done

lemmas cexpr_typing_code[code_unfold] = cexpr_type_Some_iff[symmetric]

lemma cexpr_typing_cong':
  assumes "Γ ⊢c e : t" "⋀x. x ∈ free_vars e ⟹ Γ x = Γ' x"
  shows "Γ' ⊢c e : t"
using assms
proof (induction arbitrary: Γ' rule: cexpr_typing.induct)
  case (cet_int t Γ e Γ')
  hence "⋀x. x ∈ free_vars e ⟹ case_nat t Γ x = case_nat t Γ' x"
    by (auto split: nat.split)
  from cet_int.IH[OF this] show ?case by (auto intro!: cexpr_typing.intros)
qed (auto intro!: cexpr_typing.intros)

lemma cexpr_typing_cong:
  assumes "⋀x. x ∈ free_vars e ⟹ Γ x = Γ' x"
  shows "Γ ⊢c e : t ⟷ Γ' ⊢c e : t"
  by (rule iffI) (erule cexpr_typing_cong', simp add: assms)+


primrec cexpr_sem :: "state ⇒ cexpr ⇒ val" where
  "cexpr_sem σ (CVal v) = v"
| "cexpr_sem σ (CVar x) = σ x"
| "cexpr_sem σ <e1, e2>c = <|cexpr_sem σ e1, cexpr_sem σ e2|>"
| "cexpr_sem σ (oper $$c e) = op_sem oper (cexpr_sem σ e)"
| "cexpr_sem σ (IFc b THEN e1 ELSE e2) = (if cexpr_sem σ b = TRUE then cexpr_sem σ e1 else cexpr_sem σ e2)"
| "cexpr_sem σ (∫c e ∂t) = RealVal (∫x. extract_real (cexpr_sem (x ⋅ σ) e) ∂(stock_measure t))"

definition cexpr_equiv :: "cexpr ⇒ cexpr ⇒ bool" where
  "cexpr_equiv e1 e2 ≡ ∀σ. cexpr_sem σ e1 = cexpr_sem σ e2"

lemma cexpr_equiv_commute: "cexpr_equiv e1 e2 ⟷ cexpr_equiv e2 e1"
  by (auto simp: cexpr_equiv_def)


lemma val_type_cexpr_sem[simp]:
  assumes "Γ ⊢c e : t" "free_vars e ⊆ V" "σ ∈ space (state_measure V Γ)"
  shows "val_type (cexpr_sem σ e) = t"
using assms by (induction arbitrary: σ V rule: cexpr_typing.induct)
               (auto intro: state_measure_var_type op_sem_val_type)

lemma cexpr_sem_eq_on_vars:
  assumes "⋀x. x ∈ free_vars e ⟹ σ x = σ' x"
  shows "cexpr_sem σ e = cexpr_sem σ' e"
using assms
proof (induction e arbitrary: σ σ')
  case (CPair e1 e2 σ σ')
  from CPair.prems show ?case by (auto intro!: CPair.IH)
next
  case (COperator oper e σ σ')
  from COperator.prems show ?case by (auto simp: COperator.IH[of σ σ'])
next
  case (CIf b e1 e2 σ σ')
  from CIf.prems show ?case by (auto simp: CIf.IH[of σ σ'])
next
  case (CIntegral e t σ σ')
  have "cexpr_sem σ (∫c e ∂t) = RealVal (∫x. extract_real (cexpr_sem (case_nat x σ) e) ∂stock_measure t)"
    by simp
  also from CIntegral.prems have A: "(λv. cexpr_sem (case_nat v σ) e) = (λv. cexpr_sem (case_nat v σ') e)"
    by (intro ext CIntegral.IH) (auto split: nat.split)
  also have "RealVal (∫x. extract_real (cexpr_sem (case_nat x σ') e) ∂stock_measure t) = cexpr_sem σ' (∫c e ∂t)"
    by simp
  finally show ?case .
qed simp_all


definition eval_cexpr :: "cexpr ⇒ state ⇒ val ⇒ real" where
  "eval_cexpr e σ v = extract_real (cexpr_sem (case_nat v σ) e)"

lemma measurable_cexpr_sem[measurable]:
  "Γ ⊢c e : t ⟹ free_vars e ⊆ V ⟹
      (λσ. cexpr_sem σ e) ∈ measurable (state_measure V Γ) (stock_measure t)"
proof (induction arbitrary: V rule: cexpr_typing.induct)
  case (cet_op oper t t' Γ e)
      thus ?case using measurable_op_sem by simp
next
  case (cet_int t Γ e)
  interpret sigma_finite_measure "stock_measure t" by simp
  let ?M = "(ΠM x∈V. stock_measure (Γ x)) ⨂M stock_measure t"
  let ?N = "embed_measure lborel RealVal"
  have *[measurable]: "(λa. cexpr_sem a e) ∈ measurable (state_measure (shift_var_set V) (case_nat t Γ)) REAL"
    using cet_int.prems subset_shift_var_set
    by (intro cet_int.IH) simp
  show ?case
    by simp
qed (simp_all add: state_measure_def inj_PairVal)

lemma measurable_eval_cexpr[measurable]:
  assumes "case_nat t Γ ⊢c e : REAL"
  assumes "free_vars e ⊆ shift_var_set V"
  shows "case_prod (eval_cexpr e) ∈ borel_measurable (state_measure V Γ ⨂M stock_measure t)"
  unfolding eval_cexpr_def[abs_def] using measurable_cexpr_sem[OF assms] by simp

lemma cexpr_sem_Add:
  assumes "Γ ⊢c e1 : REAL" "Γ ⊢c e2 : REAL"
  assumes "σ ∈ space (state_measure V Γ)" "free_vars e1 ⊆ V" "free_vars e2 ⊆ V"
  shows "extract_real (cexpr_sem σ (e1 +c e2)) = extract_real (cexpr_sem σ e1) + extract_real (cexpr_sem σ e2)"
  using val_type_cexpr_sem[OF assms(1,4,3)] val_type_cexpr_sem[OF assms(2,5,3)]
  by (auto simp: lift_RealIntVal2_def extract_real_def split: val.split)

lemma cexpr_sem_Mult:
  assumes "Γ ⊢c e1 : REAL" "Γ ⊢c e2 : REAL"
  assumes "σ ∈ space (state_measure V Γ)" "free_vars e1 ⊆ V" "free_vars e2 ⊆ V"
  shows "extract_real (cexpr_sem σ (e1 *c e2)) = extract_real (cexpr_sem σ e1) * extract_real (cexpr_sem σ e2)"
  using val_type_cexpr_sem[OF assms(1,4,3)] val_type_cexpr_sem[OF assms(2,5,3)]
  by (auto simp: lift_RealIntVal2_def extract_real_def split: val.split)


subsection ‹General functions on Expressions›

text ‹
   Transform variable names in an expression.
›
primrec map_vars :: "(vname ⇒ vname) ⇒ cexpr ⇒ cexpr" where
  "map_vars f (CVal v) = CVal v"
| "map_vars f (CVar x) = CVar (f x)"
| "map_vars f (<e1, e2>c) = <map_vars f e1, map_vars f e2>c"
| "map_vars f (oper $$c e) = oper $$c (map_vars f e)"
| "map_vars f (IFc b THEN e1 ELSE e2) = (IFc map_vars f b THEN map_vars f e1 ELSE map_vars f e2)"
| "map_vars f (∫c e ∂t) = ∫c map_vars (case_nat 0 (λx. Suc (f x))) e ∂t"

lemma free_vars_map_vars[simp]:
  "free_vars (map_vars f e) = f ` free_vars e"
proof (induction e arbitrary: f)
  case (CIntegral e t f)
  {
    fix x A assume "Suc x ∈ A"
    hence "Suc (f x) ∈ case_nat 0 (λx. Suc (f x)) ` A"
      by (subst image_iff, intro bexI[of _ "Suc x"]) (simp split: nat.split)
  }
  with CIntegral show ?case by (auto split: nat.split_asm)
qed auto

lemma cexpr_typing_map_vars:
  "Γ ∘ f ⊢c e : t ⟹ Γ ⊢c map_vars f e : t"
proof (induction "Γ ∘ f" e t arbitrary: Γ f rule: cexpr_typing.induct)
  case (cet_int t e Γ)
  have "case_nat t (Γ ∘ f) = case_nat t Γ ∘ (case_nat 0 (λx. Suc (f x)))"
    by (intro ext) (auto split: nat.split)
  from cet_int(2)[OF this] show ?case by (auto intro!: cexpr_typing.intros)
qed (auto intro!: cexpr_typing.intros)

lemma cexpr_sem_map_vars:
  "cexpr_sem σ (map_vars f e) = cexpr_sem (σ ∘ f) e"
proof (induction e arbitrary: σ f)
  case (CIntegral e t σ f)
  {
    fix x
    have "cexpr_sem (case_nat x σ) (map_vars (case_nat 0 (λx. Suc (f x))) e) =
                 cexpr_sem (case_nat x σ ∘ case_nat 0 (λx. Suc (f x))) e"
      by (rule CIntegral.IH)
    also have "case_nat x σ ∘ case_nat 0 (λx. Suc (f x)) = case_nat x (λa. σ (f a))"
      by (intro ext) (auto simp add: o_def split: nat.split)
    finally have "cexpr_sem (case_nat x σ) (map_vars (case_nat 0 (λx. Suc (f x))) e) =
                      cexpr_sem (case_nat x (λa. σ (f a))) e" .
  }
  thus ?case by simp
qed simp_all

definition insert_var :: "vname ⇒ (vname ⇒ 'a) ⇒ 'a ⇒ vname ⇒ 'a" where
  "insert_var v f x w ≡ if w = v then x else if w > v then f (w - 1) else f w"

lemma insert_var_0[simp]: "insert_var 0 f x = case_nat x f"
  by (intro ext) (simp add: insert_var_def split: nat.split)

text ‹
  Substitutes expression e for variable x in e'.
›
primrec cexpr_subst :: "vname ⇒ cexpr ⇒ cexpr ⇒ cexpr" where
  "cexpr_subst _ _ (CVal v) = CVal v"
| "cexpr_subst x e (CVar y) = insert_var x CVar e y"
| "cexpr_subst x e <e1, e2>c = <cexpr_subst x e e1, cexpr_subst x e e2>c"
| "cexpr_subst x e (oper $$c e') = oper $$c (cexpr_subst x e e')"
| "cexpr_subst x e (IFc b THEN e1 ELSE e2) =
      (IFc cexpr_subst x e b THEN cexpr_subst x e e1 ELSE cexpr_subst x e e2)"
| "cexpr_subst x e (∫c e' ∂t) = (∫c cexpr_subst (Suc x) (map_vars Suc e) e' ∂t)"

lemma cexpr_sem_cexpr_subst_aux:
    "cexpr_sem σ (cexpr_subst x e e') = cexpr_sem (insert_var x σ (cexpr_sem σ e)) e'"
proof (induction e' arbitrary: x e σ)
  case (CIntegral e' t x e σ)
    have A: "⋀y. insert_var (Suc x) (case_nat y σ) (cexpr_sem σ e) =
                    case_nat y (insert_var x σ (cexpr_sem σ e))"
      by (intro ext) (simp add: insert_var_def split: nat.split)
  show ?case by (simp add: o_def A cexpr_sem_map_vars CIntegral.IH)
qed (simp_all add: insert_var_def)

text ‹
   This corresponds to a Let-binding; the variable with index 0 is substituted
   with the given expression.
›
lemma cexpr_sem_cexpr_subst:
    "cexpr_sem σ (cexpr_subst 0 e e') = cexpr_sem (case_nat (cexpr_sem σ e) σ) e'"
  using cexpr_sem_cexpr_subst_aux by simp

lemma cexpr_typing_subst_aux:
  assumes "insert_var x Γ t ⊢c e' : t'" "Γ ⊢c e : t"
  shows "Γ ⊢c cexpr_subst x e e' : t'"
using assms
proof (induction e' arbitrary: x Γ e t')
  case CVar
  thus ?case by (auto intro!: cexpr_typing.intros simp: insert_var_def)
next
  case COperator
  thus ?case by (auto simp: cexpr_type_Some_iff[symmetric] split: option.split_asm)
next
  case (CIntegral e' t'')
  have t': "t' = REAL" using CIntegral.prems(1) by auto
  have "case_nat t'' (insert_var x Γ t) ⊢c e' : t'" using CIntegral.prems(1) by auto
  also have "case_nat t'' (insert_var x Γ t) = insert_var (Suc x) (case_nat t'' Γ) t"
    by (intro ext) (simp add: insert_var_def split: nat.split)
  finally have "insert_var (Suc x) (case_nat t'' Γ) t ⊢c e' : t'" .
  moreover from CIntegral.prems(2) have "case_nat t'' Γ ⊢c map_vars Suc e : t"
    by (intro cexpr_typing_map_vars) (simp add: o_def)
  ultimately have "case_nat t'' Γ ⊢c cexpr_subst (Suc x) (map_vars Suc e) e' : t'"
    by (rule CIntegral.IH)
  thus ?case by (auto intro: cet_int simp: t')
qed (auto intro!: cexpr_typing.intros)

lemma cexpr_typing_subst[intro]:
  assumes "Γ ⊢c e : t" "case_nat t Γ ⊢c e' : t'"
  shows "Γ ⊢c cexpr_subst 0 e e' : t'"
  using cexpr_typing_subst_aux assms by simp


lemma free_vars_cexpr_subst_aux:
  "free_vars (cexpr_subst x e e') ⊆ (λy. if y ≥ x then y + 1 else y) -` free_vars e' ∪ free_vars e"
    (is "free_vars _ ⊆ ?f x -` _ ∪ _")
proof (induction e' arbitrary: x e)
  case (CVar y x e)
  show ?case by (auto simp: insert_var_def)
next
  case (CPair e'1 e'2 x e)
  from CPair.IH[of x e] show ?case by auto
next
  case (COperator _ _ x e)
  from COperator.IH[of x e] show ?case by auto
next
  case (CIf b e'1 e'2 x e)
  from CIf.IH[of x e] show ?case by auto
next
  case (CIntegral e' t x e)
  have "free_vars (cexpr_subst x e (∫c e' ∂t)) ⊆
          Suc -` (?f (Suc x) -` free_vars e') ∪
          Suc -` (free_vars (map_vars Suc e))" (is "_ ⊆ ?A ∪ ?B")
    by (simp only: cexpr_subst.simps free_vars_cexpr.simps
                   vimage_mono CIntegral.IH vimage_Un[symmetric])
  also have "?B = free_vars e" by (simp add: inj_vimage_image_eq)
  also have "?A ⊆ ?f x -` free_vars (∫c e' ∂t)" by auto
  finally show ?case by blast
qed simp_all

lemma free_vars_cexpr_subst:
    "free_vars (cexpr_subst 0 e e') ⊆ Suc -` free_vars e' ∪ free_vars e"
  by (rule order.trans[OF free_vars_cexpr_subst_aux]) (auto simp: shift_var_set_def)



primrec cexpr_comp_aux :: "vname ⇒ cexpr ⇒ cexpr ⇒ cexpr" where
  "cexpr_comp_aux _ _ (CVal v) = CVal v"
| "cexpr_comp_aux x e (CVar y) = (if x = y then e else CVar y)"
| "cexpr_comp_aux x e <e1, e2>c = <cexpr_comp_aux x e e1, cexpr_comp_aux x e e2>c"
| "cexpr_comp_aux x e (oper $$c e') = oper $$c (cexpr_comp_aux x e e')"
| "cexpr_comp_aux x e (IFc b THEN e1 ELSE e2) =
      (IFc cexpr_comp_aux x e b THEN cexpr_comp_aux x e e1 ELSE cexpr_comp_aux x e e2)"
| "cexpr_comp_aux x e (∫c e' ∂t) = (∫c cexpr_comp_aux (Suc x) (map_vars Suc e) e' ∂t)"

lemma cexpr_sem_cexpr_comp_aux:
    "cexpr_sem σ (cexpr_comp_aux x e e') = cexpr_sem (σ(x := cexpr_sem σ e)) e'"
proof (induction e' arbitrary: x e σ)
  case (CIntegral e' t x e σ)
  have "⋀y. (case_nat y σ)(Suc x := cexpr_sem (case_nat y σ) (map_vars Suc e)) =
                 case_nat y (σ(x := cexpr_sem σ e))"
    by (intro ext) (auto simp: cexpr_sem_map_vars o_def split: nat.split)
  thus ?case by (auto intro!: integral_cong simp: CIntegral.IH simp del: fun_upd_apply)
qed (simp_all add: insert_var_def)

definition cexpr_comp (infixl "∘c" 55) where
  "cexpr_comp b a ≡ cexpr_comp_aux 0 a b"

lemma cexpr_typing_cexpr_comp_aux:
  assumes "Γ(x := t1) ⊢c e' : t2" "Γ ⊢c e : t1"
  shows "Γ ⊢c cexpr_comp_aux x e e' : t2"
using assms
proof (induction e' arbitrary: Γ e x t2)
  case COperator
  thus ?case by (elim cexpr_typing_opE) (auto intro!: cexpr_typing.intros) []
next
  case CPair
  thus ?case by (elim cexpr_typing_pairE) (auto intro!: cexpr_typing.intros) []
next
  case (CIntegral e' t Γ e x t2)
  from CIntegral.prems have [simp]: "t2 = REAL" by auto
  from CIntegral.prems have "case_nat t (Γ(x := t1)) ⊢c e' : REAL" by (elim cexpr_typing_intE)
  also have "case_nat t (Γ(x := t1)) = (case_nat t Γ)(Suc x := t1)"
    by (intro ext) (simp split: nat.split)
  finally have "... ⊢c e' : REAL" .
  thus "Γ ⊢c cexpr_comp_aux x e (∫c e' ∂t) : t2"
    by (auto intro!: cexpr_typing.intros CIntegral.IH cexpr_typing_map_vars
             simp: o_def CIntegral.prems)
qed (auto intro!: cexpr_typing.intros)

lemma cexpr_typing_cexpr_comp[intro]:
  assumes "case_nat t1 Γ ⊢c g : t2"
  assumes "case_nat t2 Γ ⊢c f : t3"
  shows "case_nat t1 Γ ⊢c f ∘c g : t3"
proof (unfold cexpr_comp_def, intro cexpr_typing_cexpr_comp_aux)
  have "(case_nat t1 Γ)(0 := t2) = case_nat t2 Γ"
    by (intro ext) (simp split: nat.split)
  with assms show "(case_nat t1 Γ)(0 := t2) ⊢c f : t3" by simp
qed (insert assms)


lemma free_vars_cexpr_comp_aux:
  "free_vars (cexpr_comp_aux x e e') ⊆ (free_vars e' - {x}) ∪ free_vars e"
proof (induction e' arbitrary: x e)
  case (CIntegral e' t x e)
  note IH = CIntegral.IH[of "Suc x" "map_vars Suc e"]
  have "free_vars (cexpr_comp_aux x e (∫c e' ∂t)) =
           Suc -` free_vars (cexpr_comp_aux (Suc x) (map_vars Suc e) e')" by simp
  also have "... ⊆ Suc -` (free_vars e' - {Suc x} ∪ free_vars (map_vars Suc e))"
    by (rule vimage_mono, rule CIntegral.IH)
  also have "... ⊆ free_vars (∫c e' ∂t) - {x} ∪ free_vars e"
    by (auto simp add: vimage_Diff vimage_image_eq)
  finally show ?case .
qed (simp, blast?)+

lemma free_vars_cexpr_comp:
  "free_vars (cexpr_comp e e') ⊆ (free_vars e - {0}) ∪ free_vars e'"
  by (simp add: free_vars_cexpr_comp_aux cexpr_comp_def)

lemma free_vars_cexpr_comp':
  "free_vars (cexpr_comp e e') ⊆ free_vars e ∪ free_vars e'"
  using free_vars_cexpr_comp by blast

lemma cexpr_sem_cexpr_comp:
    "cexpr_sem σ (f ∘c g) = cexpr_sem (σ(0 := cexpr_sem σ g)) f"
  unfolding cexpr_comp_def by (simp add: cexpr_sem_cexpr_comp_aux)

lemma eval_cexpr_comp:
    "eval_cexpr (f ∘c g) σ x = eval_cexpr f σ (cexpr_sem (case_nat x σ) g)"
proof-
  have "(case_nat x σ)(0 := cexpr_sem (case_nat x σ) g) = case_nat (cexpr_sem (case_nat x σ) g) σ"
    by (intro ext) (auto split: nat.split)
  thus ?thesis by (simp add: eval_cexpr_def cexpr_sem_cexpr_comp)
qed

primrec cexpr_subst_val_aux :: "nat ⇒ cexpr ⇒ val ⇒ cexpr" where
  "cexpr_subst_val_aux _ (CVal v) _ = CVal v"
| "cexpr_subst_val_aux x (CVar y) v = insert_var x CVar (CVal v) y"
| "cexpr_subst_val_aux x (IFc b THEN e1 ELSE e2) v =
    (IFc cexpr_subst_val_aux x b v THEN cexpr_subst_val_aux x e1 v ELSE cexpr_subst_val_aux x e2 v)"
| "cexpr_subst_val_aux x (oper $$c e) v = oper $$c (cexpr_subst_val_aux x e v)"
| "cexpr_subst_val_aux x <e1, e2>c v = <cexpr_subst_val_aux x e1 v, cexpr_subst_val_aux x e2 v>c"
| "cexpr_subst_val_aux x (∫c e ∂t) v = ∫c cexpr_subst_val_aux (Suc x) e v ∂t"

lemma cexpr_subst_val_aux_eq_cexpr_subst:
    "cexpr_subst_val_aux x e v = cexpr_subst x (CVal v) e"
  by (induction e arbitrary: x) simp_all

definition cexpr_subst_val :: "cexpr ⇒ val ⇒ cexpr" where
  "cexpr_subst_val e v ≡ cexpr_subst_val_aux 0 e v"

lemma cexpr_sem_cexpr_subst_val[simp]:
    "cexpr_sem σ (cexpr_subst_val e v) = cexpr_sem (case_nat v σ) e"
  by (simp add: cexpr_subst_val_def cexpr_subst_val_aux_eq_cexpr_subst cexpr_sem_cexpr_subst)

lemma cexpr_typing_subst_val[intro]:
    "case_nat t Γ ⊢c e : t' ⟹ val_type v = t ⟹ Γ ⊢c cexpr_subst_val e v : t'"
  by (auto simp: cexpr_subst_val_def cexpr_subst_val_aux_eq_cexpr_subst intro!: cet_val')

lemma free_vars_cexpr_subst_val_aux:
    "free_vars (cexpr_subst_val_aux x e v) = (λy. if y ≥ x then Suc y else y) -` free_vars e"
  by (induction e arbitrary: x) (auto simp: insert_var_def split: if_split_asm)

lemma free_vars_cexpr_subst_val[simp]:
    "free_vars (cexpr_subst_val e v) = Suc -` free_vars e"
  by (simp add: cexpr_subst_val_def free_vars_cexpr_subst_val_aux)


subsection ‹Nonnegative expressions›

definition "nonneg_cexpr V Γ e ≡
    ∀σ ∈ space (state_measure V Γ). extract_real (cexpr_sem σ e) ≥ 0"

lemma nonneg_cexprI:
    "(⋀σ. σ ∈ space (state_measure V Γ) ⟹ extract_real (cexpr_sem σ e) ≥ 0) ⟹ nonneg_cexpr V Γ e"
  unfolding nonneg_cexpr_def by simp

lemma nonneg_cexprD:
    "nonneg_cexpr V Γ e ⟹ σ ∈ space (state_measure V Γ) ⟹ extract_real (cexpr_sem σ e) ≥ 0"
  unfolding nonneg_cexpr_def by simp

lemma nonneg_cexpr_map_vars:
  assumes "nonneg_cexpr (f -` V) (Γ ∘ f) e"
  shows "nonneg_cexpr V Γ (map_vars f e)"
  by (intro nonneg_cexprI, subst cexpr_sem_map_vars, intro nonneg_cexprD[OF assms])
     (auto simp: state_measure_def space_PiM)

lemma nonneg_cexpr_subset:
  assumes "nonneg_cexpr V Γ e" "V ⊆ V'" "free_vars e ⊆ V"
  shows "nonneg_cexpr V' Γ e"
proof (intro nonneg_cexprI)
  fix σ assume "σ ∈ space (state_measure V' Γ)"
  with assms(2) have "restrict σ V ∈ space (state_measure V Γ)"
    by (auto simp: state_measure_def space_PiM restrict_def)
  from nonneg_cexprD[OF assms(1) this] have "extract_real (cexpr_sem (restrict σ V) e) ≥ 0" .
  also have "cexpr_sem (restrict σ V) e = cexpr_sem σ e" using assms(3)
    by (intro cexpr_sem_eq_on_vars) auto
  finally show "extract_real (cexpr_sem σ e) ≥ 0" .
qed

lemma nonneg_cexpr_Mult:
  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_Mult[of Γ _ _ _ V]) simp_all
  also have "... ≥ 0" using σ N1 N2 by (intro mult_nonneg_nonneg nonneg_cexprD)
  finally show "extract_real (cexpr_sem σ (e1 *c e2)) ≥ 0" .
qed

lemma nonneg_indicator:
  assumes "Γ ⊢c e : BOOL" "free_vars e ⊆ V"
  shows "nonneg_cexpr V Γ (⟨e⟩c)"
proof (intro nonneg_cexprI)
  fix ρ assume "ρ ∈ space (state_measure V Γ)"
  with assms have "val_type (cexpr_sem ρ e) = BOOL" by (rule val_type_cexpr_sem)
  thus "extract_real (cexpr_sem ρ (⟨e⟩c)) ≥ 0"
    by (auto simp: extract_real_def bool_to_real_def split: val.split)
qed

lemma nonneg_cexpr_comp_aux:
  assumes nonneg: "nonneg_cexpr V (Γ(x := t1)) e"  and x:"x ∈ V"
  assumes t2: "Γ(x:=t1) ⊢c e : t2" and t1: "Γ ⊢c f : t1" and vars: "free_vars f ⊆ V"
  shows "nonneg_cexpr V Γ (cexpr_comp_aux x f e)"
proof (intro nonneg_cexprI)
  fix σ assume σ: "σ ∈ space (state_measure V Γ)"
  have "extract_real (cexpr_sem σ (cexpr_comp_aux x f e)) =
            extract_real (cexpr_sem (σ(x := cexpr_sem σ f)) e)"
    by (simp add: cexpr_sem_cexpr_comp_aux)
  also from val_type_cexpr_sem[OF t1 vars σ] have "cexpr_sem σ f ∈ type_universe t1" by auto
  with σ x have "σ(x := cexpr_sem σ f) ∈ space (state_measure V (Γ(x := t1)))"
    by (auto simp: state_measure_def space_PiM shift_var_set_def split: if_split_asm)
  hence "extract_real (cexpr_sem (σ(x := cexpr_sem σ f)) e) ≥ 0"
    by(intro nonneg_cexprD[OF assms(1)])
  finally show "extract_real (cexpr_sem σ (cexpr_comp_aux x f e)) ≥ 0" .
qed

lemma nonneg_cexpr_comp:
  assumes "nonneg_cexpr (shift_var_set V) (case_nat t2 Γ) e"
  assumes "case_nat t1 Γ ⊢c f : t2" "free_vars f ⊆ shift_var_set V"
  shows "nonneg_cexpr (shift_var_set V) (case_nat t1 Γ) (e ∘c f)"
proof (intro nonneg_cexprI)
  fix σ assume σ: "σ ∈ space (state_measure (shift_var_set V) (case_nat t1 Γ))"
  have "extract_real (cexpr_sem σ (e ∘c f)) = extract_real (cexpr_sem (σ(0 := cexpr_sem σ f)) e)"
    by (simp add: cexpr_sem_cexpr_comp)
  also from val_type_cexpr_sem[OF assms(2,3) σ] have "cexpr_sem σ f ∈ type_universe t2" by auto
  with σ have "σ(0 := cexpr_sem σ f) ∈ space (state_measure (shift_var_set V) (case_nat t2 Γ))"
    by (auto simp: state_measure_def space_PiM shift_var_set_def split: if_split_asm)
  hence "extract_real (cexpr_sem (σ(0 := cexpr_sem σ f)) e) ≥ 0"
    by(intro nonneg_cexprD[OF assms(1)])
  finally show "extract_real (cexpr_sem σ (e ∘c f)) ≥ 0" .
qed

lemma nonneg_cexpr_subst_val:
  assumes "nonneg_cexpr (shift_var_set V) (case_nat t Γ) e" "val_type v = t"
  shows "nonneg_cexpr V Γ (cexpr_subst_val e v)"
proof (intro nonneg_cexprI)
  fix σ assume σ: "σ ∈ space (state_measure V Γ)"
  moreover from assms(2) have "v ∈ type_universe t" by auto
  ultimately show "extract_real (cexpr_sem σ (cexpr_subst_val e v)) ≥ 0"
    by (auto intro!: nonneg_cexprD[OF assms(1)])
qed

lemma nonneg_cexpr_int:
  assumes "nonneg_cexpr (shift_var_set V) (case_nat t Γ) e"
  shows "nonneg_cexpr V Γ (∫c e ∂t)"
proof (intro nonneg_cexprI)
  fix σ assume σ: "σ ∈ space (state_measure V Γ)"
  have "extract_real (cexpr_sem σ (∫c e ∂t)) = ∫x. extract_real (cexpr_sem (case_nat x σ) e) ∂stock_measure t"
    by (simp add: extract_real_def)
  also from σ have "... ≥ 0"
    by (intro integral_nonneg_AE AE_I2 nonneg_cexprD[OF assms]) auto
  finally show "extract_real (cexpr_sem σ (∫c e ∂t)) ≥ 0" .
qed


text ‹Subprobability density expressions›

definition "subprob_cexpr V V' Γ e ≡
    ∀ρ ∈ space (state_measure V' Γ).
      (∫+σ. extract_real (cexpr_sem (merge V V' (σ, ρ)) e) ∂state_measure V Γ) ≤ 1"

lemma subprob_cexprI:
  assumes "⋀ρ. ρ ∈ space (state_measure V' Γ) ⟹
                 (∫+σ. extract_real (cexpr_sem (merge V V' (σ, ρ)) e) ∂state_measure V Γ) ≤ 1"
  shows "subprob_cexpr V V' Γ e"
  using assms unfolding subprob_cexpr_def by simp

lemma subprob_cexprD:
  assumes "subprob_cexpr V V' Γ e"
  shows "⋀ρ. ρ ∈ space (state_measure V' Γ) ⟹
               (∫+σ. extract_real (cexpr_sem (merge V V' (σ, ρ)) e) ∂state_measure V Γ) ≤ 1"
  using assms unfolding subprob_cexpr_def by simp

lemma subprob_indicator:
  assumes subprob: "subprob_cexpr V V' Γ e1" and nonneg: "nonneg_cexpr (V ∪ V') Γ e1"
  assumes t1: "Γ ⊢c e1 : REAL" and t2: "Γ ⊢c e2 : BOOL"
  assumes vars1: "free_vars e1 ⊆ V ∪ V'" and vars2: "free_vars e2 ⊆ V ∪ V'"
  shows "subprob_cexpr V V' Γ (e1 *c ⟨e2⟩c)"
proof (intro subprob_cexprI)
  fix ρ assume ρ: "ρ ∈ space (state_measure V' Γ)"
  from t2 have t2': "Γ ⊢c ⟨e2⟩c : REAL" by (rule cet_op) simp_all
  from vars2 have vars2': "free_vars (⟨e2⟩c) ⊆ V ∪ V'" by simp
  let ?eval = "λσ e. extract_real (cexpr_sem (merge V V' (σ, ρ)) e)"
  have "(∫+σ. ?eval σ (e1 *c ⟨e2⟩c) ∂state_measure V Γ) =
            (∫+σ. ?eval σ e1 * ?eval σ (⟨e2⟩c) ∂state_measure V Γ)"
    by (intro nn_integral_cong)
       (simp only: cexpr_sem_Mult[OF t1 t2' merge_in_state_measure[OF _ ρ] vars1 vars2'])
  also {
    fix σ assume σ: "σ ∈ space (state_measure V Γ)"
    with ρ have "val_type (cexpr_sem (merge V V' (σ,ρ)) e2) = BOOL"
      by (intro val_type_cexpr_sem[OF t2 vars2] merge_in_state_measure)
    hence "?eval σ (⟨e2⟩c) ∈ {0,1}"
      by (cases "cexpr_sem (merge V V' (σ,ρ)) e2") (auto simp: extract_real_def bool_to_real_def)
    moreover have "?eval σ e1 ≥ 0" using nonneg ρ σ
      by (auto intro!: nonneg_cexprD merge_in_state_measure)
    ultimately have "?eval σ e1 * ?eval σ (⟨e2⟩c) ≤ ?eval σ e1"
      by (intro mult_right_le_one_le) auto
  }
  hence "(∫+σ. ?eval σ e1 * ?eval σ (⟨e2⟩c) ∂state_measure V Γ) ≤
             (∫+σ. ?eval σ e1 ∂state_measure V Γ)"
    by (intro nn_integral_mono) (simp add: ennreal_leI)
  also from subprob and ρ have "... ≤ 1" by (rule subprob_cexprD)
  finally show "(∫+σ. ?eval σ (e1 *c ⟨e2⟩c) ∂state_measure V Γ)  ≤ 1" .
qed

lemma measurable_cexpr_sem':
  assumes ρ: "ρ ∈ space (state_measure V' Γ)"
  assumes e: "Γ ⊢c e : REAL" "free_vars e ⊆ V ∪ V'"
  shows "(λσ. extract_real (cexpr_sem (merge V V' (σ, ρ)) e))
            ∈ borel_measurable (state_measure V Γ)"
  apply (rule measurable_compose[OF _ measurable_extract_real])
  apply (rule measurable_compose[OF _ measurable_cexpr_sem[OF e]])
  apply (insert ρ, unfold state_measure_def, rule measurable_compose[OF _ measurable_merge], simp)
  done

lemma measurable_fun_upd_state_measure[measurable]:
  assumes "v ∉ V"
  shows "(λ(x,y). y(v := x)) ∈ measurable (stock_measure (Γ v) ⨂M state_measure V Γ)
                                          (state_measure (insert v V) Γ)"
  unfolding state_measure_def by simp


lemma integrable_cexpr_projection:
  assumes fin: "finite V"
  assumes disjoint: "V ∩ V' = {}" "v ∉ V" "v ∉ V'"
  assumes ρ: "ρ ∈ space (state_measure V' Γ)"
  assumes e: "Γ ⊢c e : REAL" "free_vars e ⊆ insert v V ∪ V'"
  assumes int: "integrable (state_measure (insert v V) Γ)
                    (λσ. extract_real (cexpr_sem (merge (insert v V) V' (σ, ρ)) e))"
                (is "integrable _ ?f'")
  shows "AE x in stock_measure (Γ v).
           integrable (state_measure V Γ)
               (λσ. extract_real (cexpr_sem (merge V (insert v V') (σ, ρ(v := x))) e))"
    (is "AE x in ?N. integrable ?M (?f x)")
proof (unfold real_integrable_def, intro AE_conjI)
  show "AE x in ?N. ?f x ∈ borel_measurable ?M" using ρ e disjoint
    by (intro AE_I2 measurable_cexpr_sem')
       (auto simp: state_measure_def space_PiM dest: PiE_mem split: if_split_asm)

  let ?f'' = "λx σ. extract_real (cexpr_sem (merge (insert v V) V' (σ(v := x), ρ)) e)"
  {
    fix x σ assume "x ∈ space ?N" "σ ∈ space ?M"
    hence "merge (insert v V) V' (σ(v := x), ρ) = merge V (insert v V') (σ, ρ(v := x))"
      using disjoint by (intro ext) (simp add: merge_def split: if_split_asm)
    hence "?f'' x σ = ?f x σ" by simp
  } note f''_eq_f = this

  interpret product_sigma_finite "(λv. stock_measure (Γ v))"
    by (simp add: product_sigma_finite_def)
  interpret sigma_finite_measure "state_measure V Γ"
    by (rule sigma_finite_state_measure[OF fin])

  from int have "(∫+σ. ennreal (?f' σ) ∂state_measure (insert v V) Γ) ≠ ∞"
    by (simp add: real_integrable_def)
  also have "(∫+σ. ennreal (?f' σ) ∂state_measure (insert v V) Γ) =
                 ∫+x. ∫+σ. ennreal (?f'' x σ) ∂?M ∂?N" (is "_ = ?I")
    using fin disjoint e ρ
    by (unfold state_measure_def, subst product_nn_integral_insert_rev)
       (auto intro!: measurable_compose[OF _ measurable_ennreal] measurable_cexpr_sem'[unfolded state_measure_def])
  finally have "AE x in ?N. (∫+σ. ennreal (?f'' x σ) ∂?M) ≠ ∞" (is ?P) using e disjoint
    by (intro nn_integral_PInf_AE)
       (auto simp: measurable_split_conv intro!: borel_measurable_nn_integral measurable_compose[OF _ measurable_ennreal]
                   measurable_compose[OF _ measurable_cexpr_sem'[OF ρ]])
  moreover have "⋀x. x ∈ space ?N ⟹ (∫+σ. ennreal (?f'' x σ) ∂?M) = (∫+σ. ennreal (?f x σ) ∂?M)"
    by (intro nn_integral_cong) (simp add: f''_eq_f)
  hence "?P ⟷ (AE x in ?N. (∫+σ. ennreal (?f x σ) ∂?M) ≠ ∞)" by (intro AE_cong) simp
  ultimately show "AE x in ?N. (∫+σ. ennreal (?f x σ) ∂?M) ≠ ∞" by simp

  from int have "(∫+σ. ennreal (-?f' σ) ∂state_measure (insert v V) Γ) ≠ ∞"
    by (simp add: real_integrable_def)
  also have "(∫+σ. ennreal (-?f' σ) ∂state_measure (insert v V) Γ) =
                 ∫+x. ∫+σ. ennreal (-?f'' x σ) ∂?M ∂?N" (is "_ = ?I")
    using fin disjoint e ρ
    by (unfold state_measure_def, subst product_nn_integral_insert_rev)
       (auto intro!: measurable_compose[OF _ measurable_ennreal] borel_measurable_uminus
                     measurable_cexpr_sem'[unfolded state_measure_def])
  finally have "AE x in ?N. (∫+σ. ennreal (-?f'' x σ) ∂?M) ≠ ∞" (is ?P) using e disjoint
    by (intro nn_integral_PInf_AE)
       (auto simp: measurable_split_conv intro!: borel_measurable_nn_integral measurable_compose[OF _ measurable_ennreal]
                   measurable_compose[OF _ measurable_cexpr_sem'[OF ρ]] borel_measurable_uminus)
  moreover have "⋀x. x ∈ space ?N ⟹ (∫+σ. ennreal (-?f'' x σ) ∂?M) = (∫+σ. ennreal (-?f x σ) ∂?M)"
    by (intro nn_integral_cong) (simp add: f''_eq_f)
  hence "?P ⟷ (AE x in ?N. (∫+σ. ennreal (-?f x σ) ∂?M) ≠ ∞)" by (intro AE_cong) simp
  ultimately show "AE x in ?N. (∫+σ. ennreal (-?f x σ) ∂?M) ≠ ∞" by simp
qed


definition cdens_ctxt_invar :: "vname list ⇒ vname list ⇒ tyenv ⇒ cexpr ⇒ bool" where
  "cdens_ctxt_invar vs vs' Γ δ ≡
       distinct (vs @ vs') ∧
       free_vars δ ⊆ set (vs @ vs') ∧
       Γ ⊢c δ : REAL ∧
       nonneg_cexpr (set vs ∪ set vs') Γ δ ∧
       subprob_cexpr (set vs) (set vs') Γ δ"

lemma cdens_ctxt_invarI:
  "⟦distinct (vs @ vs'); free_vars δ ⊆ set (vs @ vs'); Γ ⊢c δ : REAL;
    nonneg_cexpr (set vs ∪ set vs') Γ δ;
    subprob_cexpr (set vs) (set vs') Γ δ ⟧ ⟹
      cdens_ctxt_invar vs vs' Γ δ"
  by (simp add: cdens_ctxt_invar_def)

lemma cdens_ctxt_invarD:
  assumes "cdens_ctxt_invar vs vs' Γ δ"
  shows "distinct (vs @ vs')" "free_vars δ ⊆ set (vs @ vs')" "Γ ⊢c δ : REAL"
        "nonneg_cexpr (set vs ∪ set vs') Γ δ" "subprob_cexpr (set vs) (set vs') Γ δ"
  using assms by (simp_all add: cdens_ctxt_invar_def)

lemma cdens_ctxt_invar_empty:
  assumes "cdens_ctxt_invar vs vs' Γ δ"
  shows "cdens_ctxt_invar [] (vs @ vs') Γ (CReal 1)"
  using cdens_ctxt_invarD[OF assms]
  by (intro cdens_ctxt_invarI)
     (auto simp: cexpr_type_Some_iff[symmetric] extract_real_def state_measure_def PiM_empty
           intro!: nonneg_cexprI subprob_cexprI)

lemma cdens_ctxt_invar_imp_integrable:
  assumes "cdens_ctxt_invar vs vs' Γ δ" and ρ: "ρ ∈ space (state_measure (set vs') Γ)"
  shows "integrable (state_measure (set vs) Γ)
             (λσ. extract_real (cexpr_sem (merge (set vs) (set vs') (σ, ρ)) δ))" (is "integrable ?M ?f")
  unfolding integrable_iff_bounded
proof (intro conjI)
  note invar = cdens_ctxt_invarD[OF assms(1)]
  show "?f ∈ borel_measurable ?M"
    apply (rule measurable_compose[OF _ measurable_extract_real])
    apply (rule measurable_compose[OF _ measurable_cexpr_sem[OF invar(3,2)]])
    apply (simp only: state_measure_def set_append, rule measurable_compose[OF _ measurable_merge])
    apply (rule measurable_Pair, simp, insert assms(2), simp add: state_measure_def)
    done

  have nonneg: "⋀σ. σ ∈ space ?M ⟹ ?f σ ≥ 0"
    using ‹nonneg_cexpr (set vs ∪ set vs') Γ δ›
    by (rule nonneg_cexprD, intro merge_in_state_measure[OF _ ρ])
  with ‹subprob_cexpr (set vs) (set vs') Γ δ› and ρ
  show "(∫+σ. ennreal (norm (?f σ)) ∂?M) < ∞" unfolding subprob_cexpr_def
    by (auto simp: less_top[symmetric] top_unique cong: nn_integral_cong)
qed


subsection ‹Randomfree expressions›

text ‹
  Translates an expression with no occurrences of Random or Fail into an
  equivalent target language expression.
›
primrec expr_rf_to_cexpr :: "expr ⇒ cexpr" where
  "expr_rf_to_cexpr (Val v) = CVal v"
| "expr_rf_to_cexpr (Var x) = CVar x"
| "expr_rf_to_cexpr <e1, e2> = <expr_rf_to_cexpr e1, expr_rf_to_cexpr e2>c"
| "expr_rf_to_cexpr (oper $$ e) = oper $$c (expr_rf_to_cexpr e)"
| "expr_rf_to_cexpr (IF b THEN e1 ELSE e2) =
      (IFc expr_rf_to_cexpr b THEN expr_rf_to_cexpr e1 ELSE expr_rf_to_cexpr e2)"
| "expr_rf_to_cexpr (LET e1 IN e2) =
      cexpr_subst 0 (expr_rf_to_cexpr e1) (expr_rf_to_cexpr e2)"
| "expr_rf_to_cexpr (Random _ _) = undefined"
| "expr_rf_to_cexpr (Fail _) = undefined"

lemma cexpr_sem_expr_rf_to_cexpr:
     "randomfree e ⟹ cexpr_sem σ (expr_rf_to_cexpr e) = expr_sem_rf σ e"
  by (induction e arbitrary: σ) (auto simp: cexpr_sem_cexpr_subst)

lemma cexpr_typing_expr_rf_to_cexpr[intro]:
    assumes "Γ ⊢ e : t" "randomfree e"
    shows "Γ ⊢c expr_rf_to_cexpr e : t"
  using assms by (induction rule: expr_typing.induct) (auto intro!: cexpr_typing.intros)

lemma free_vars_expr_rf_to_cexpr:
  "randomfree e ⟹ free_vars (expr_rf_to_cexpr e) ⊆ free_vars e"
proof (induction e)
  case (LetVar e1 e2)
  thus ?case
    by (simp only: free_vars_cexpr.simps expr_rf_to_cexpr.simps,
        intro order.trans[OF free_vars_cexpr_subst]) auto
qed auto

subsection ‹Builtin density expressions›

primrec dist_dens_cexpr :: "pdf_dist ⇒ cexpr ⇒ cexpr ⇒ cexpr" where
  "dist_dens_cexpr Bernoulli p x = (IFc CReal 0 ≤c p ∧c p ≤c CReal 1 THEN
                                       IFc x THEN p ELSE CReal 1 -c p
                                    ELSE CReal 0)"
| "dist_dens_cexpr UniformInt p x = (IFc fstc p ≤c sndc p ∧c fstc p ≤c x ∧c x ≤c sndc p THEN
                                         inversec (⟨sndc p -c fstc p +c CInt 1⟩c) ELSE CReal 0)"
| "dist_dens_cexpr UniformReal p x = (IFc fstc p <c sndc p ∧c fstc p ≤c x ∧c x ≤c sndc p THEN
                                         inversec (sndc p -c fstc p) ELSE CReal 0)"
| "dist_dens_cexpr Gaussian p x = (IFc CReal 0 <c sndc p THEN
                                     expc (-c((x -c fstc p)^cCInt 2 /c (CReal 2 *c sndc p^cCInt 2))) /c
                                         sqrtc (CReal 2 *c πc *c sndc p ^c CInt 2) ELSE CReal 0)"
| "dist_dens_cexpr Poisson p x = (IFc CReal 0 <c p ∧c CInt 0 ≤c x THEN
                                    p ^c x /c ⟨factc x⟩c *c expc (-c p) ELSE CReal 0)"

lemma free_vars_dist_dens_cexpr:
    "free_vars (dist_dens_cexpr dst e1 e2) ⊆ free_vars e1 ∪ free_vars e2"
  by (subst dist_dens_cexpr_def, cases dst) simp_all

lemma cexpr_typing_dist_dens_cexpr:
    assumes "Γ ⊢c e1 : dist_param_type dst" "Γ ⊢c e2 : dist_result_type dst"
    shows "Γ ⊢c dist_dens_cexpr dst e1 e2 : REAL"
  using assms
  apply (subst dist_dens_cexpr_def, cases dst)
  (* Bernoulli *)
  apply (simp, intro cet_op_intros cet_if cet_val' cet_var' cet_eq, simp_all) []
  (* Uniform int *)
  apply (simp, intro cet_if cet_and cet_or cet_less_int cet_eq)
  apply (erule cet_fst cet_snd | simp)+
  apply (rule cet_inverse, rule cet_op[where t = INTEG], intro cet_add_int cet_minus_int)
  apply (simp_all add: cet_val' cet_fst cet_snd) [5]
  (* Uniform real *)
  apply (simp, intro cet_if cet_op_intros cet_eq cet_fst cet_snd, simp_all add: cet_val') []
  (* Poisson *)
  apply (simp, intro cet_if cet_and, rule cet_less_real, simp add: cet_val', simp)
  apply (rule cet_less_eq_int, simp add: cet_val', simp)
  apply (intro cet_mult_real cet_pow_real cet_inverse cet_cast_real_int cet_exp cet_minus_real
               cet_op[where oper = Fact and t = INTEG] cet_var', simp_all add: cet_val') [2]
  (* Gaussian *)
  apply (simp, intro cet_if cet_op_intros cet_val', simp_all add: cet_fst cet_snd)
  done


lemma val_type_eq_BOOL: "val_type x = BOOL ⟷ x ∈ BoolVal`UNIV"
  by (cases x) auto

lemma val_type_eq_INTEG: "val_type x = INTEG ⟷ x ∈ IntVal`UNIV"
  by (cases x) auto

lemma val_type_eq_PRODUCT: "val_type x = PRODUCT t1 t2 ⟷
  (∃a b. val_type a = t1 ∧ val_type b = t2 ∧ x = <| a, b |>)"
  by (cases x) auto

lemma cexpr_sem_dist_dens_cexpr_nonneg:
  assumes "Γ ⊢c e1 : dist_param_type dst" "Γ ⊢c e2 : dist_result_type dst"
  assumes "free_vars e1 ⊆ V" "free_vars e2 ⊆ V"
  assumes "σ ∈ space (state_measure V Γ)"
  shows "ennreal (extract_real (cexpr_sem σ (dist_dens_cexpr dst e1 e2))) =
           dist_dens dst (cexpr_sem σ e1) (cexpr_sem σ e2) ∧
           0 ≤ extract_real (cexpr_sem σ (dist_dens_cexpr dst e1 e2))"
proof-
  from val_type_cexpr_sem[OF assms(1,3,5)] and val_type_cexpr_sem[OF assms(2,4,5)]
    have "cexpr_sem σ e1 ∈ space (stock_measure (dist_param_type dst))" and
         "cexpr_sem σ e2 ∈ space (stock_measure (dist_result_type dst))"
    by (auto simp: type_universe_def simp del: type_universe_type)
  thus ?thesis
    by (subst dist_dens_cexpr_def, cases dst)
       (auto simp:
            lift_Comp_def lift_RealVal_def lift_RealIntVal_def lift_RealIntVal2_def
            bernoulli_density_def val_type_eq_REAL val_type_eq_BOOL val_type_eq_PRODUCT val_type_eq_INTEG
            uniform_int_density_def uniform_real_density_def
            lift_IntVal_def poisson_density'_def one_ennreal_def
            field_simps gaussian_density_def)
qed

lemma cexpr_sem_dist_dens_cexpr:
  assumes "Γ ⊢c e1 : dist_param_type dst" "Γ ⊢c e2 : dist_result_type dst"
  assumes "free_vars e1 ⊆ V" "free_vars e2 ⊆ V"
  assumes "σ ∈ space (state_measure V Γ)"
  shows "ennreal (extract_real (cexpr_sem σ (dist_dens_cexpr dst e1 e2))) =
           dist_dens dst (cexpr_sem σ e1) (cexpr_sem σ e2)"
  using cexpr_sem_dist_dens_cexpr_nonneg[OF assms] by simp

lemma nonneg_dist_dens_cexpr:
  assumes "Γ ⊢c e1 : dist_param_type dst" "Γ ⊢c e2 : dist_result_type dst"
  assumes "free_vars e1 ⊆ V" "free_vars e2 ⊆ V"
  shows "nonneg_cexpr V Γ (dist_dens_cexpr dst e1 e2)"
proof (intro nonneg_cexprI)
  fix σ assume ρ: "σ ∈ space (state_measure V Γ)"
  from cexpr_sem_dist_dens_cexpr_nonneg[OF assms this]
  show "0 ≤ extract_real (cexpr_sem σ (dist_dens_cexpr dst e1 e2))"
    by simp
qed

subsection ‹Integral expressions›

definition integrate_var :: "tyenv ⇒ vname ⇒ cexpr ⇒ cexpr" where
  "integrate_var Γ v e = ∫c map_vars (λw. if v = w then 0 else Suc w) e ∂(Γ v)"

definition integrate_vars :: "tyenv ⇒ vname list ⇒ cexpr ⇒ cexpr" where
  "integrate_vars Γ = foldr (integrate_var Γ)"

lemma cexpr_sem_integrate_var:
  "cexpr_sem σ (integrate_var Γ v e) =
    RealVal (∫x. extract_real (cexpr_sem (σ(v := x)) e) ∂stock_measure (Γ v))"
proof-
  let ?f = "(λw. if v = w then 0 else Suc w)"
  have "cexpr_sem σ (integrate_var Γ v e) =
          RealVal (∫x. extract_real (cexpr_sem (case_nat x σ ∘ ?f) e) ∂stock_measure (Γ v))"
    by (simp add: extract_real_def integrate_var_def cexpr_sem_map_vars)
  also have "(λx. case_nat x σ ∘ ?f) = (λx. σ(v := x))"
    by (intro ext) (simp add: o_def split: if_split)
  finally show ?thesis .
qed

lemma cexpr_sem_integrate_var':
  "extract_real (cexpr_sem σ (integrate_var Γ v e)) =
      (∫x. extract_real (cexpr_sem (σ(v := x)) e) ∂stock_measure (Γ v))"
  by (subst cexpr_sem_integrate_var, simp add: extract_real_def)

lemma cexpr_typing_integrate_var[simp]:
    "Γ ⊢c e : REAL ⟹ Γ ⊢c integrate_var Γ v e : REAL"
  unfolding integrate_var_def
  by (rule cexpr_typing.intros, rule cexpr_typing_map_vars)
     (erule cexpr_typing_cong', simp split: nat.split)

lemma cexpr_typing_integrate_vars[simp]:
    "Γ ⊢c e : REAL ⟹ Γ ⊢c integrate_vars Γ vs e : REAL"
  by (induction vs arbitrary: e)
     (simp_all add: integrate_vars_def)

lemma free_vars_integrate_var[simp]:
    "free_vars (integrate_var Γ v e) = free_vars e - {v}"
  by (auto simp: integrate_var_def)

lemma free_vars_integrate_vars[simp]:
    "free_vars (integrate_vars Γ vs e) = free_vars e - set vs"
  by (induction vs arbitrary: e) (auto simp: integrate_vars_def)

lemma (in product_sigma_finite) product_integral_insert':
  fixes f :: "_ ⇒ real"
  assumes "finite I" "i ∉ I" "integrable (PiM (insert i I) M) f"
  shows "integralL (PiM (insert i I) M) f = LINT y|M i. LINT x|PiM I M. f (x(i := y))"
proof-
  interpret pair_sigma_finite "M i" "PiM I M"
    by (simp_all add: sigma_finite assms pair_sigma_finite_def sigma_finite_measures)
  interpret Mi: sigma_finite_measure "M i"
    by (simp add: assms sigma_finite_measures)
  from assms(3) have int: "integrable (M i ⨂M PiM I M) (λ(x, y). f (y(i := x)))"
  unfolding real_integrable_def
    apply (elim conjE)
    apply (subst (1 2) nn_integral_snd[symmetric])
    apply ((subst (asm) (1 2) product_nn_integral_insert[OF assms(1,2)],
           auto intro!: measurable_compose[OF _ measurable_ennreal] borel_measurable_uminus) [])+
    done
  from assms have "integralL (PiM (insert i I) M) f = LINT x|PiM I M. LINT y|M i. f (x(i := y))"
    by (rule product_integral_insert)
  also from int have "... = LINT y|M i. LINT x|PiM I M. f (x(i := y))"
    by (rule Fubini_integral)
  finally show ?thesis .
qed


lemma cexpr_sem_integrate_vars:
  assumes ρ: "ρ ∈ space (state_measure V' Γ)"
  assumes disjoint: "distinct vs" "set vs ∩ V' = {}"
  assumes "integrable (state_measure (set vs) Γ)
               (λσ. extract_real (cexpr_sem (merge (set vs) V' (σ, ρ)) e))"
  assumes e: "Γ ⊢c e : REAL" "free_vars e ⊆ set vs ∪ V'"
  shows "extract_real (cexpr_sem ρ (integrate_vars Γ vs e)) =
           ∫σ. extract_real (cexpr_sem (merge (set vs) V' (σ, ρ)) e) ∂state_measure (set vs) Γ"
using assms
proof (induction vs arbitrary: ρ V')
  case Nil
  hence "⋀v. (if v ∈ V' then ρ v else undefined) = ρ v"
    by (auto simp: state_measure_def space_PiM)
  thus ?case by (auto simp: integrate_vars_def state_measure_def merge_def PiM_empty)
next
  case (Cons v vs ρ V')
  interpret product_sigma_finite "λv. stock_measure (Γ v)"
    by (simp add: product_sigma_finite_def)
  interpret sigma_finite_measure "state_measure (set vs) Γ"
    by (simp add: sigma_finite_state_measure)
  have ρ': "⋀x. x ∈ type_universe (Γ v) ⟹ ρ(v := x) ∈ space (state_measure (insert v V') Γ)"
    using Cons.prems(1) by (auto simp: state_measure_def space_PiM split: if_split_asm)
  have "extract_real (cexpr_sem ρ (integrate_vars Γ (v # vs) e)) =
          ∫x. extract_real (cexpr_sem (ρ(v := x)) (integrate_vars Γ vs e)) ∂stock_measure (Γ v)"
    (is "_ = ?I") by (simp add: integrate_vars_def cexpr_sem_integrate_var extract_real_def)
  also from Cons.prems(4) have int: "integrable (state_measure (insert v (set vs)) Γ)
      (λσ. extract_real (cexpr_sem (merge (insert v (set vs)) V' (σ, ρ)) e))" by simp
  have "AE x in stock_measure (Γ v).
                extract_real (cexpr_sem (ρ(v := x)) (integrate_vars Γ vs e)) =
                  ∫σ. extract_real (cexpr_sem (merge (set vs) (insert v V') (σ, ρ(v := x))) e)
                      ∂state_measure (set vs) Γ"
    apply (rule AE_mp[OF _ AE_I2[OF impI]])
    apply (rule integrable_cexpr_projection[OF _ _ _ _ _ _ _ int])
    apply (insert Cons.prems, auto) [7]
    apply (subst Cons.IH, rule ρ', insert Cons.prems, auto)
    done
  hence "?I = ∫x. ∫σ. extract_real (cexpr_sem (merge (set vs) (insert v V') (σ, ρ(v := x))) e)
                  ∂state_measure (set vs) Γ ∂stock_measure (Γ v)" using Cons.prems
    apply (intro integral_cong_AE)
    apply (rule measurable_compose[OF measurable_Pair_compose_split[OF
                measurable_fun_upd_state_measure[of v V' Γ]]])
    apply (simp, simp, simp, rule measurable_compose[OF _ measurable_extract_real])
    apply (rule measurable_cexpr_sem, simp, (auto) [])
    apply (rule borel_measurable_lebesgue_integral)
    apply (subst measurable_split_conv)
    apply (rule measurable_compose[OF _ measurable_extract_real])
    apply (rule measurable_compose[OF _ measurable_cexpr_sem[of Γ _ _  "set vs ∪ insert v V'"]])
    apply (unfold state_measure_def, rule measurable_compose[OF _ measurable_merge])
    apply simp_all
    done
  also have "(λx σ. merge (set vs) (insert v V') (σ, ρ(v := x))) =
                 (λx σ. merge (set (v#vs)) V' (σ(v := x), ρ))"
    using Cons.prems by (intro ext) (auto simp: merge_def split: if_split)
  also have "(∫x. ∫σ. extract_real (cexpr_sem (merge (set (v#vs)) V' (σ(v := x), ρ)) e)
                  ∂state_measure (set vs) Γ ∂stock_measure (Γ v)) =
               ∫σ. extract_real (cexpr_sem (merge (set (v#vs)) V' (σ, ρ)) e)
                  ∂state_measure (set (v#vs)) Γ"
    using Cons.prems unfolding state_measure_def
    by (subst (2) set_simps, subst product_integral_insert') simp_all
  finally show ?case .
qed

lemma cexpr_sem_integrate_vars':
  assumes ρ: "ρ ∈ space (state_measure V' Γ)"
  assumes disjoint: "distinct vs" "set vs ∩ V' = {}"
  assumes nonneg: "nonneg_cexpr (set vs ∪ V') Γ e"
  assumes "integrable (state_measure (set vs) Γ)
               (λσ. extract_real (cexpr_sem (merge (set vs) V' (σ, ρ)) e))"
  assumes e: "Γ ⊢c e : REAL" "free_vars e ⊆ set vs ∪ V'"
  shows "ennreal (extract_real (cexpr_sem ρ (integrate_vars Γ vs e))) =
           ∫+σ. extract_real (cexpr_sem (merge (set vs) V' (σ, ρ)) e) ∂state_measure (set vs) Γ"
proof-
  from assms have "extract_real (cexpr_sem ρ (integrate_vars Γ vs e)) =
      ∫σ. extract_real (cexpr_sem (merge (set vs) V' (σ, ρ)) e) ∂state_measure (set vs) Γ"
    by (intro cexpr_sem_integrate_vars)
  also have "ennreal ... =
      ∫+σ. extract_real (cexpr_sem (merge (set vs) V' (σ, ρ)) e) ∂state_measure (set vs) Γ"
    using assms
    by (intro nn_integral_eq_integral[symmetric] AE_I2)
       (auto intro!: nonneg_cexprD merge_in_state_measure)
  finally show ?thesis .
qed

lemma nonneg_cexpr_sem_integrate_vars:
  assumes ρ: "ρ ∈ space (state_measure V' Γ)"
  assumes disjoint: "distinct vs" "set vs ∩ V' = {}"
  assumes nonneg: "nonneg_cexpr (set vs ∪ V') Γ e"
  assumes e: "Γ ⊢c e : REAL" "free_vars e ⊆ set vs ∪ V'"
  shows "extract_real (cexpr_sem ρ (integrate_vars Γ vs e)) ≥ 0"
using assms
proof (induction vs arbitrary: ρ V')
  case Nil
  hence "⋀v. (if v ∈ V' then ρ v else undefined) = ρ v"
    by (auto simp: state_measure_def space_PiM)
  with Nil show ?case
    by (auto simp: integrate_vars_def state_measure_def merge_def PiM_empty nonneg_cexprD)
next
  case (Cons v vs ρ V')
  have ρ': "⋀x. x ∈ type_universe (Γ v) ⟹ ρ(v := x) ∈ space (state_measure (insert v V') Γ)"
    using Cons.prems(1) by (auto simp: state_measure_def space_PiM split: if_split_asm)
  have "extract_real (cexpr_sem ρ (integrate_vars Γ (v # vs) e)) =
          ∫x. extract_real (cexpr_sem (ρ(v := x)) (integrate_vars Γ vs e)) ∂stock_measure (Γ v)"
    by (simp add: integrate_vars_def cexpr_sem_integrate_var extract_real_def)
  also have "... ≥ 0"
    by (rule integral_nonneg_AE, rule AE_I2, subst Cons.IH[OF ρ']) (insert Cons.prems, auto)
  finally show "extract_real (cexpr_sem ρ (integrate_vars Γ (v # vs) e)) ≥ 0" .
qed

lemma nonneg_cexpr_sem_integrate_vars':
  "distinct vs ⟹ set vs ∩ V' = {} ⟹ nonneg_cexpr (set vs ∪ V') Γ e ⟹ Γ ⊢c e : REAL ⟹
    free_vars e ⊆ set vs ∪ V' ⟹ nonneg_cexpr V' Γ (integrate_vars Γ vs e)"
  apply (intro nonneg_cexprI allI)
  apply (rule nonneg_cexpr_sem_integrate_vars[where V'=V'])
  apply auto
  done

lemma cexpr_sem_integral_nonneg:
  assumes finite: "(∫+x. extract_real (cexpr_sem (case_nat x σ) e) ∂stock_measure t) < ∞"
  assumes nonneg: "nonneg_cexpr (shift_var_set V) (case_nat t Γ) e"
  assumes t: "case_nat t Γ ⊢c e : REAL" and vars: "free_vars e ⊆ shift_var_set V"
  assumes ρ: "σ ∈ space (state_measure V Γ)"
  shows "ennreal (extract_real (cexpr_sem σ (∫c e ∂t))) =
             ∫+x. extract_real (cexpr_sem (case_nat x σ) e) ∂stock_measure t"
proof-
  let ?f = "λx. extract_real (cexpr_sem (case_nat x σ) e)"
  have meas: "?f ∈ borel_measurable (stock_measure t)"
    apply (rule measurable_compose[OF _ measurable_extract_real])
    apply (rule measurable_compose[OF measurable_case_nat' measurable_cexpr_sem])
    apply (rule measurable_ident_sets[OF refl], rule measurable_const[OF ρ])
    apply (simp_all add: t vars)
    done
  from this and finite and nonneg have int: "integrable (stock_measure t) ?f"
    by (auto intro!: integrableI_nonneg nonneg_cexprD case_nat_in_state_measure[OF _ ρ])

  have "extract_real (cexpr_sem σ (∫c e ∂t)) =
          ∫x. extract_real (cexpr_sem (case_nat x σ) e) ∂stock_measure t"
    by (simp add: extract_real_def)
  also have "ennreal ... = ∫+x. extract_real (cexpr_sem (case_nat x σ) e) ∂stock_measure t"
    by (subst nn_integral_eq_integral[OF int AE_I2])
       (auto intro!: nonneg_cexprD[OF nonneg] case_nat_in_state_measure[OF _ ρ])
  finally show ?thesis .
qed

lemma has_parametrized_subprob_density_cexpr_sem_integral:
  assumes dens: "has_parametrized_subprob_density (state_measure V' Γ) M (stock_measure t)
                   (λρ x. ∫+y. eval_cexpr f (case_nat x ρ) y ∂stock_measure t')"
  assumes nonneg: "nonneg_cexpr (shift_var_set (shift_var_set V')) (case_nat t' (case_nat t Γ)) f"
  assumes tf: "case_nat t' (case_nat t Γ) ⊢c f : REAL"
  assumes varsf: "free_vars f ⊆ shift_var_set (shift_var_set V')"
  assumes ρ: "ρ ∈ space (state_measure V' Γ)"
  shows "AE x in stock_measure t.
          (∫+y. eval_cexpr f (case_nat x ρ) y ∂stock_measure t') = ennreal (eval_cexpr (∫c f ∂t') ρ x)"
proof (rule AE_mp[OF _ AE_I2[OF impI]])
  interpret sigma_finite_measure "stock_measure t'" by simp
  let ?f = "λx. ∫+y. eval_cexpr f (case_nat x ρ) y ∂stock_measure t'"
  from has_parametrized_subprob_density_integral[OF dens ρ]
    have "(∫+x. ?f x ∂stock_measure t) ≠ ∞" by (auto simp: eval_cexpr_def top_unique)
  thus "AE x in stock_measure t. ?f x ≠ ∞" using ρ tf varsf by (intro nn_integral_PInf_AE) simp_all
  fix x assume x: "x ∈ space (stock_measure t)" and finite: "?f x ≠ ∞"
  have nonneg': "AE y in stock_measure t'. eval_cexpr f (case_nat x ρ) y ≥ 0"
    unfolding eval_cexpr_def using ρ x
    by (intro AE_I2 nonneg_cexprD[OF nonneg]) (auto intro!: case_nat_in_state_measure)
  hence "integrable (stock_measure t') (λy. eval_cexpr f (case_nat x ρ) y)"
    using x ρ tf varsf finite by (intro integrableI_nonneg) (simp_all add: top_unique less_top)
  thus "?f x = ennreal (eval_cexpr (∫c f ∂t') ρ x)" using nonneg'
    by (simp add: extract_real_def nn_integral_eq_integral eval_cexpr_def)
qed

end