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