Theory ResourcedDenotational

theory ResourcedDenotational
imports "Abstract-Denotational-Props" "CValue-Nominal" "C-restr"
begin

type_synonym CEnv = "var ⇒ (C → CValue)"

interpretation semantic_domain
  "Λ f . Λ r. CFn⋅(Λ v. (f⋅(v))|⇘r⇙)"
  "Λ x y. (Λ r. (x⋅r ↓CFn y|⇘r⇙)⋅r)"
  "Λ b r. CB⋅b"
  "Λ scrut v1 v2 r. CB_project⋅(scrut⋅r)⋅(v1⋅r)⋅(v2⋅r)"
  "C_case".

abbreviation ESem_syn'' ("𝒩⟦ _ ⟧⇘_⇙"  [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 "𝒩⦃Γ⦄ ≡ 𝒩⦃Γ⦄⊥"

text {*
Here we re-state the simplification rules, cleaned up by beta-reducing the locale parameters.
*}

lemma CESem_simps:
  "𝒩⟦ Lam [x]. e ⟧⇘ρ⇙  = (Λ (C⋅r). CFn⋅(Λ v. (𝒩⟦ e ⟧⇘ρ(x := v)⇙)|⇘r⇙))"
  "𝒩⟦ App e x ⟧⇘ρ⇙     = (Λ (C⋅r). ((𝒩⟦ e ⟧⇘ρ⇙)⋅r ↓CFn ρ x|⇘r⇙)⋅r)"
  "𝒩⟦ Var x ⟧⇘ρ⇙       = (Λ (C⋅r). (ρ  x) ⋅ r)"
  "𝒩⟦ Bool b ⟧⇘ρ⇙      = (Λ (C⋅r). CB⋅(Discr b))"
  "𝒩⟦ (scrut ? e⇩1 : e⇩2) ⟧⇘ρ⇙  = (Λ (C⋅r). CB_project⋅((𝒩⟦ scrut ⟧⇘ρ⇙)⋅r)⋅((𝒩⟦ e⇩1 ⟧⇘ρ⇙)⋅r)⋅((𝒩⟦ e⇩2 ⟧⇘ρ⇙)⋅r))"
  "𝒩⟦ Let as body ⟧⇘ρ⇙ = (Λ (C ⋅ r). (𝒩⟦body⟧⇘𝒩⦃as⦄ρ⇙) ⋅ r)"
  by (auto simp add: eta_cfun)

lemma CESem_bot[simp]:"(𝒩⟦ e ⟧⇘σ⇙)⋅⊥ = ⊥"
  by (nominal_induct e arbitrary: σ rule: exp_strong_induct) auto

lemma CHSem_bot[simp]:"((𝒩⦃ Γ ⦄) x)⋅⊥ = ⊥"
  by (cases "x ∈ domA Γ") (auto simp add: lookup_HSem_heap lookup_HSem_other)

text {*
Sometimes we do not care much about the resource usage and just want a simpler formula.
*}

lemma CESem_simps_no_tick:
  "(𝒩⟦ Lam [x]. e ⟧⇘ρ⇙)⋅r ⊑ CFn⋅(Λ v. (𝒩⟦ e ⟧⇘ρ(x := v)⇙)|⇘r⇙)"
  "(𝒩⟦ App e x ⟧⇘ρ⇙)⋅r    ⊑ ((𝒩⟦ e ⟧⇘ρ⇙)⋅r ↓CFn ρ x|⇘r⇙)⋅r"
  "𝒩⟦ Var x ⟧⇘ρ⇙         ⊑ ρ x"
  "(𝒩⟦ (scrut ? e⇩1 : e⇩2) ⟧⇘ρ⇙)⋅r ⊑ CB_project⋅((𝒩⟦ scrut ⟧⇘ρ⇙)⋅r)⋅((𝒩⟦ e⇩1 ⟧⇘ρ⇙)⋅r)⋅((𝒩⟦ e⇩2 ⟧⇘ρ⇙)⋅r)"
  "𝒩⟦ Let as body ⟧⇘ρ⇙   ⊑  𝒩⟦body⟧⇘𝒩⦃as⦄ρ⇙"
  apply -
  apply (rule below_trans[OF monofun_cfun_arg[OF below_C]], simp)
  apply (rule below_trans[OF monofun_cfun_arg[OF below_C]], simp)
  apply (rule cfun_belowI, rule below_trans[OF monofun_cfun_arg[OF below_C]], simp)
  apply (rule below_trans[OF monofun_cfun_arg[OF below_C]], simp)
  apply (rule cfun_belowI, rule below_trans[OF monofun_cfun_arg[OF below_C]], simp)
  done

lemma CELam_no_restr: "(𝒩⟦ Lam [x]. e ⟧⇘ρ⇙)⋅r ⊑ CFn⋅(Λ v. (𝒩⟦ e ⟧⇘ρ(x := v)⇙))"
proof-
  have "(𝒩⟦ Lam [x]. e ⟧⇘ρ⇙)⋅r ⊑ CFn⋅(Λ v. (𝒩⟦ e ⟧⇘ρ(x := v)⇙)|⇘r⇙)" by (rule CESem_simps_no_tick)
  also have "… ⊑ CFn⋅(Λ v. (𝒩⟦ e ⟧⇘ρ(x := v)⇙))"
    by (intro cont2cont monofun_LAM below_trans[OF C_restr_below] monofun_cfun_arg below_refl fun_upd_mono)
  finally show ?thesis by this (intro cont2cont)
qed

lemma CEApp_no_restr: "(𝒩⟦ App e x ⟧⇘ρ⇙)⋅r    ⊑ ((𝒩⟦ e ⟧⇘ρ⇙)⋅r ↓CFn ρ x)⋅r"
proof-
  have "(𝒩⟦ App e x ⟧⇘ρ⇙)⋅r  ⊑ ((𝒩⟦ e ⟧⇘ρ⇙)⋅r ↓CFn ρ x|⇘r⇙)⋅r" by (rule CESem_simps_no_tick)
  also have "ρ x|⇘r⇙ ⊑ ρ x" by (rule C_restr_below)
  finally show ?thesis by this (intro cont2cont)
qed

end