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)".

abbreviation
  ESem_syn'' :: "exp ⇒ (var => Value) ⇒ Value" ("⟦ _ ⟧⇘_⇙"  [60,60] 60)
  where "⟦ e ⟧⇘ρ⇙ ≡ ESem e ⋅ ρ"

abbreviation EvalHeapSem_syn''  ("❙⟦ _ ❙⟧⇘_⇙"  [0,0] 110)  where "❙⟦Γ❙⟧⇘ρ⇙ ≡ evalHeap Γ (λ e. ⟦e⟧⇘ρ⇙)"
abbreviation HSem_syn' ("⦃_⦄_"  [60,60] 60) where "⦃Γ⦄ρ ≡ HSem Γ ⋅ ρ"
abbreviation HSem_bot  ("⦃_⦄"  [60] 60) where "⦃Γ⦄ ≡ ⦃Γ⦄⊥"

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