Theory Adequacy

theory Adequacy
imports ResourcedAdequacy "Denotational-Related"
begin

theorem adequacy:
  assumes "⟦e⟧⇘⦃Γ⦄⇙ ≠ ⊥"
  shows "∃ Δ v. Γ : e ⇓⇘S⇙ Δ : v"
proof-
  have "⦃Γ⦄ ◃▹⇧* 𝒩⦃Γ⦄" by (rule heaps_similar)
  hence  "⟦e⟧⇘⦃Γ⦄⇙ ◃▹ (𝒩⟦e⟧⇘𝒩⦃Γ⦄⇙)⋅C⇧∞" by (rule denotational_semantics_similar)
  from bot_or_not_bot[OF this] assms
  have "(𝒩⟦e⟧⇘𝒩⦃Γ⦄⇙)⋅C⇧∞ ≠ ⊥" by metis
  thus ?thesis by (rule resourced_adequacy)
qed

end