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 ◃▹ yC"
    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 e1 e2)
  hence IfThenElse':
    " scrut ⟧⇘ρ◃▹ (𝒩⟦ scrut ⟧⇘σ)C"
    " e1 ⟧⇘ρ◃▹ (𝒩⟦ e1 ⟧⇘σ)C"
    " e2 ⟧⇘ρ◃▹ (𝒩⟦ e2 ⟧⇘σ)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 asevalHeap 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