Theory Denotational

theory Denotational
  imports "Abstract-Denotational-Props" "Value-Nominal"
begin

text ‹
This is the actual denotational semantics as found in \<^cite>‹"launchbury"›.
›

interpretation semantic_domain Fn Fn_project B B_project "(Λ x. x)".

notation ESem_syn ("⟦ _ ⟧⇘_⇙"  [60,60] 60)
notation EvalHeapSem_syn  ("❙⟦ _ ❙⟧⇘_⇙"  [0,0] 110)
notation HSem_syn ("⦃_⦄_"  [60,60] 60)
notation AHSem_bot ("⦃_⦄"  [60] 60)

lemma ESem_simps_as_defined:
  "⟦ Lam [x]. e ⟧⇘ρ⇙ =  Fn⋅(Λ v. ⟦ e ⟧⇘(ρ f|` (fv (Lam [x].e)))(x := v)⇙)"
  "⟦ App e x ⟧⇘ρ⇙    =  ⟦ e ⟧⇘ρ⇙ ↓Fn ρ x"
  "⟦ Var x ⟧⇘ρ⇙      =  ρ  x"
  "⟦ Bool b ⟧⇘ρ⇙     =  B⋅(Discr b)"
  "⟦ (scrut ? e⇩1 : e⇩2) ⟧⇘ρ⇙ = B_project⋅(⟦ scrut ⟧⇘ρ⇙)⋅(⟦ e⇩1 ⟧⇘ρ⇙)⋅(⟦ e⇩2 ⟧⇘ρ⇙)"
  "⟦ Let Γ body ⟧⇘ρ⇙ = ⟦body⟧⇘⦃Γ⦄(ρ f|` fv (Let Γ body))⇙"
  by (simp_all del: ESem_Lam ESem_Let add: ESem.simps(1,4) )


lemma ESem_simps:
  "⟦ Lam [x]. e ⟧⇘ρ⇙ =  Fn⋅(Λ v. ⟦ e ⟧⇘ρ(x := v)⇙)"
  "⟦ App e x ⟧⇘ρ⇙    =  ⟦ e ⟧⇘ρ⇙ ↓Fn ρ x"
  "⟦ Var x ⟧⇘ρ⇙      =  ρ  x"
  "⟦ Bool b ⟧⇘ρ⇙     =  B⋅(Discr b)"
  "⟦ (scrut ? e⇩1 : e⇩2) ⟧⇘ρ⇙ = B_project⋅(⟦ scrut ⟧⇘ρ⇙)⋅(⟦ e⇩1 ⟧⇘ρ⇙)⋅(⟦ e⇩2 ⟧⇘ρ⇙)"
  "⟦ Let Γ body ⟧⇘ρ⇙ = ⟦body⟧⇘⦃Γ⦄ρ⇙"
  by simp_all
(*<*)

text ‹
Excluded from the document, as these are unused in the current development.
›

subsubsection ‹Replacing subexpressions by variables›

lemma HSem_subst_var_app:
  assumes fresh: "atom n ♯ x"
  shows "⦃(x, App (Var n) y) # (n, e) # Γ⦄ρ = ⦃(x, App e y) # (n, e) # Γ⦄ρ "
proof(rule HSem_subst_expr)
  from fresh have [simp]: "n ≠ x" by (simp add: fresh_at_base)
  have ne: "(n,e) ∈ set ((x, App e y) # (n, e) # Γ)" by simp

  have "⟦ Var n ⟧⇘⦃(x, App e y) # (n, e) # Γ⦄ρ⇙ = (⦃(x, App e y) # (n, e) # Γ⦄ρ) n"
    by simp
  also have "... = ⟦ e ⟧⇘(⦃(x, App e y) # (n, e) # Γ⦄ρ)⇙"
    by (subst HSem_eq, simp)
  finally
  show "⟦ App (Var n) y ⟧⇘⦃(x, App e y) # (n, e) # Γ⦄ρ⇙ ⊑ ⟦ App e y ⟧⇘⦃(x, App e y) # (n, e) # Γ⦄ρ⇙"
    by simp

 have "⟦ Var n ⟧⇘⦃(x, App (Var n) y) # (n, e) # Γ⦄ρ⇙ = (⦃(x, App (Var n) y) # (n, e) # Γ⦄ρ) n"
    by simp
  also have "... = ⟦ e ⟧⇘(⦃(x, App (Var n) y) # (n, e) # Γ⦄ρ)⇙"
    by (subst HSem_eq, simp)
  finally
  show "⟦ App e y ⟧⇘⦃(x, App (Var n) y) # (n, e) # Γ⦄ρ⇙ ⊑ ⟦ App (Var n) y ⟧⇘⦃(x, App (Var n) y) # (n, e) # Γ⦄ρ⇙"
    by simp
qed

lemma HSem_subst_var_var:
  assumes fresh: "atom n ♯ x"
  shows "⦃(x, Var n) # (n, e) # Γ⦄ρ = ⦃(x, e) # (n, e) # Γ⦄ρ "
proof(rule HSem_subst_expr)
  from fresh have [simp]: "n ≠ x" by (simp add: fresh_at_base)
  have ne: "(n,e) ∈ set ((x, e) # (n, e) # Γ)" by simp

  have "⟦ Var n ⟧⇘⦃(x, e) # (n, e) # Γ⦄ρ⇙ = (⦃(x, e) # (n, e) # Γ⦄ρ) n"
    by simp
  also have "... = ⟦ e ⟧⇘(⦃(x, e) # (n, e) # Γ⦄ρ)⇙"
    by (subst HSem_eq, simp)
  finally
  show "⟦ Var n ⟧⇘⦃(x, e) # (n, e) # Γ⦄ρ⇙ ⊑ ⟦ e ⟧⇘⦃(x, e) # (n, e) # Γ⦄ρ⇙"
    by simp

  have "⟦ Var n ⟧⇘⦃(x, Var n) # (n, e) # Γ⦄ρ⇙ = (⦃(x, Var n) # (n, e) # Γ⦄ρ) n"
    by simp
  also have "... = ⟦ e ⟧⇘(⦃(x, Var n) # (n, e) # Γ⦄ρ)⇙"
    by (subst HSem_eq, simp)
  finally
  show "⟦ e ⟧⇘⦃(x, Var n) # (n, e) # Γ⦄ρ⇙ ⊑ ⟦ Var n ⟧⇘⦃(x, Var n) # (n, e) # Γ⦄ρ⇙"
    by simp
qed
(*>*)


end