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