Theory Denotational-Related

theory "Denotational-Related"
imports Denotational ResourcedDenotational ValueSimilarity
begin

text ‹
Given the similarity relation it is straight-forward to prove that the standard
and the resourced denotational semantics produce similar results. (Theorem 10 in
|cite{functionspaces}).
›

theorem denotational_semantics_similar: 
  assumes "ρ ◃▹⇧* σ"
  shows "⟦e⟧⇘ρ⇙ ◃▹ (𝒩⟦e⟧⇘σ⇙)⋅C⇧∞"
using assms
proof(induct e arbitrary: ρ σ rule:exp_induct)
  case (Var v)
  from Var have "ρ v ◃▹ (σ v)⋅C⇧∞" by cases auto
  thus ?case by simp
next
  case (Lam v e)
  { fix x y
    assume "x ◃▹ y⋅C⇧∞"
    with ‹ρ ◃▹⇧* σ›
    have "ρ(v := x) ◃▹⇧* σ(v := y)"
      by (auto 1 4)
    hence "⟦e⟧⇘ρ(v := x)⇙ ◃▹ (𝒩⟦e⟧⇘σ(v := y)⇙)⋅C⇧∞"
      by (rule Lam.hyps)
  }
  thus ?case by auto
next
  case (App e v ρ σ)
  hence App': "⟦e⟧⇘ρ⇙ ◃▹ (𝒩⟦e⟧⇘σ⇙)⋅C⇧∞" by auto
  thus ?case
  proof (cases rule: slimilar_bot_cases)
    case (Fn f g)
    from ‹ρ ◃▹⇧* σ›
    have "ρ v ◃▹ (σ v)⋅C⇧∞"  by auto
    thus ?thesis using Fn App' by auto
  qed auto
next
  case (Bool b)
  thus "⟦Bool b⟧⇘ρ⇙ ◃▹ (𝒩⟦Bool b⟧⇘σ⇙)⋅C⇧∞" by auto
next
  case (IfThenElse scrut e⇩1 e⇩2)
  hence IfThenElse':
    "⟦ scrut ⟧⇘ρ⇙ ◃▹ (𝒩⟦ scrut ⟧⇘σ⇙)⋅C⇧∞"
    "⟦ e⇩1 ⟧⇘ρ⇙ ◃▹ (𝒩⟦ e⇩1 ⟧⇘σ⇙)⋅C⇧∞"
    "⟦ e⇩2 ⟧⇘ρ⇙ ◃▹ (𝒩⟦ e⇩2 ⟧⇘σ⇙)⋅C⇧∞" by auto
  from IfThenElse'(1)
  show ?case
  proof (cases rule: slimilar_bot_cases)
    case (bool b)
    thus ?thesis using IfThenElse' by auto
  qed auto
next
  case (Let as e ρ σ)
  have "⦃as⦄ρ ◃▹⇧* 𝒩⦃as⦄σ"
  proof (rule parallel_HSem_ind_different_ESem[OF pointwise_adm[OF similar_admI] fun_similar_fmap_bottom])
    fix ρ' :: "var ⇒ Value" and σ' :: "var ⇒ C → CValue"
    assume "ρ' ◃▹⇧* σ'"
    show "ρ ++⇘domA as⇙ ❙⟦ as ❙⟧⇘ρ'⇙ ◃▹⇧* σ ++⇘domA as⇙ evalHeap as (λe. 𝒩⟦ e ⟧⇘σ'⇙)"
    proof(rule pointwiseI, goal_cases)
      case (1 x)
      show ?case using ‹ρ ◃▹⇧* σ›
        by (auto simp add: lookup_override_on_eq lookupEvalHeap elim: Let(1)[OF _  ‹ρ' ◃▹⇧* σ'›] )
    qed
  qed auto
  hence "⟦e⟧⇘⦃as⦄ρ⇙ ◃▹ (𝒩⟦e⟧⇘𝒩⦃as⦄σ⇙)⋅C⇧∞" by (rule Let(2))
  thus ?case by simp
qed

corollary evalHeap_similar:
  "⋀y z. y ◃▹⇧* z ⟹ ❙⟦ Γ ❙⟧⇘y⇙ ◃▹⇧* ❙𝒩⟦ Γ ❙⟧⇘z⇙"
  by (rule pointwiseI)
     (case_tac "x ∈ domA Γ", auto simp add: lookupEvalHeap denotational_semantics_similar)

theorem heaps_similar: "⦃Γ⦄ ◃▹⇧* 𝒩⦃Γ⦄"
  by (rule parallel_HSem_ind_different_ESem[OF pointwise_adm[OF similar_admI]])
     (auto simp add: evalHeap_similar)

end