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 ? e1 : e2) ⟧⇘ρ= B_project( scrut ⟧⇘ρ)( e1 ⟧⇘ρ)( e2 ⟧⇘ρ)"
  " 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 ? e1 : e2) ⟧⇘ρ= B_project( scrut ⟧⇘ρ)( e1 ⟧⇘ρ)( e2 ⟧⇘ρ)"
  " 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