theory CorrectnessResourced imports "ResourcedDenotational" Launchbury begin theorem correctness: assumes "Γ : e ⇓⇘L⇙ Δ : z" and "fv (Γ, e) ⊆ set L ∪ domA Γ" shows "𝒩⟦e⟧⇘𝒩⦃Γ⦄ρ⇙ ⊑ 𝒩⟦z⟧⇘𝒩⦃Δ⦄ρ⇙" and "(𝒩⦃Γ⦄ρ) f|` domA Γ ⊑ (𝒩⦃Δ⦄ρ) f|` domA Γ" using assms proof(nominal_induct arbitrary: ρ rule:reds.strong_induct) case Lambda case 1 show ?case.. case 2 show ?case.. next case (Application y Γ e x L Δ Θ z e') have Gamma_subset: "domA Γ ⊆ domA Δ" by (rule reds_doesnt_forget[OF Application.hyps(8)]) case 1 hence prem1: "fv (Γ, e) ⊆ set L ∪ domA Γ" and "x ∈ set L ∪ domA Γ" by auto moreover note reds_pres_closed[OF Application.hyps(8) prem1] moreover note reds_doesnt_forget[OF Application.hyps(8)] moreover have "fv (e'[y::=x]) ⊆ fv (Lam [y]. e') ∪ {x}" by (auto simp add: fv_subst_eq) ultimately have prem2: "fv (Δ, e'[y::=x]) ⊆ set L ∪ domA Δ" by auto have *: "(𝒩⦃Γ⦄ρ) x ⊑ (𝒩⦃Δ⦄ρ) x" proof(cases "x ∈ domA Γ") case True thus ?thesis using fun_belowD[OF Application.hyps(10)[OF prem1], where ρ1 = ρ and x = x] by simp next case False from False `x ∈ set L ∪ domA Γ` reds_avoids_live[OF Application.hyps(8)] show ?thesis by (auto simp add: lookup_HSem_other) qed { fix r have "(𝒩⟦ App e x ⟧⇘𝒩⦃Γ⦄ρ⇙)⋅r ⊑ ((𝒩⟦ e ⟧⇘𝒩⦃Γ⦄ρ⇙)⋅r ↓CFn (𝒩⦃Γ⦄ρ) x)⋅r" by (rule CEApp_no_restr) also have "((𝒩⟦ e ⟧⇘𝒩⦃Γ⦄ρ⇙)) ⊑ ((𝒩⟦ Lam [y]. e' ⟧⇘𝒩⦃Δ⦄ρ⇙))" using Application.hyps(9)[OF prem1]. also note `((𝒩⦃Γ⦄ρ) x) ⊑ (𝒩⦃Δ⦄ρ) x` also have "(𝒩⟦ Lam [y]. e' ⟧⇘𝒩⦃Δ⦄ρ⇙)⋅r ⊑ (CFn⋅(Λ v. (𝒩⟦ e' ⟧⇘(𝒩⦃Δ⦄ρ)(y := v)⇙)))" by (rule CELam_no_restr) also have "CFn⋅(Λ v. (𝒩⟦ e' ⟧⇘(𝒩⦃Δ⦄ρ)(y := v)⇙)) ↓CFn ((𝒩⦃Δ⦄ρ) x) = (𝒩⟦ e' ⟧⇘(𝒩⦃Δ⦄ρ)(y := (𝒩⦃Δ⦄ρ) x)⇙)" by simp also have "… = (𝒩⟦ e'[y ::= x] ⟧⇘(𝒩⦃Δ⦄ρ)⇙)" unfolding ESem_subst.. also have "… ⊑ 𝒩⟦ z ⟧⇘𝒩⦃Θ⦄ρ⇙" using Application.hyps(12)[OF prem2]. finally have "(𝒩⟦ App e x ⟧⇘𝒩⦃Γ⦄ρ⇙)⋅r ⊑ (𝒩⟦ z ⟧⇘𝒩⦃Θ⦄ρ⇙)⋅r" by this (intro cont2cont)+ } thus ?case by (rule cfun_belowI) show "(𝒩⦃Γ⦄ρ) f|` (domA Γ) ⊑ (𝒩⦃Θ⦄ρ) f|` (domA Γ)" using Application.hyps(10)[OF prem1] env_restr_below_subset[OF Gamma_subset Application.hyps(13)[OF prem2]] by (rule below_trans) next case (Variable Γ x e L Δ z) hence [simp]:"x ∈ domA Γ" by (metis domA_from_set map_of_SomeD) case 2 have "x ∉ domA Δ" by (rule reds_avoids_live[OF Variable.hyps(2)], simp_all) have subset: "domA (delete x Γ) ⊆ domA Δ" by (rule reds_doesnt_forget[OF Variable.hyps(2)]) let "?new" = "domA Δ - domA Γ" have "fv (delete x Γ, e) ∪ {x} ⊆ fv (Γ, Var x)" by (rule fv_delete_heap[OF `map_of Γ x = Some e`]) hence prem: "fv (delete x Γ, e) ⊆ set (x # L) ∪ domA (delete x Γ)" using 2 by auto hence fv_subset: "fv (delete x Γ, e) - domA (delete x Γ) ⊆ - ?new" using reds_avoids_live'[OF Variable.hyps(2)] by auto have "domA Γ ⊆ (-?new)" by auto have "𝒩⦃Γ⦄ρ = 𝒩⦃(x,e) # delete x Γ⦄ρ" by (rule HSem_reorder[OF map_of_delete_insert[symmetric, OF Variable(1)]]) also have "… = (μ ρ'. (ρ ++⇘(domA (delete x Γ))⇙ (𝒩⦃delete x Γ⦄ρ'))( x := 𝒩⟦ e ⟧⇘ρ'⇙))" by (rule iterative_HSem, simp) also have "… = (μ ρ'. (ρ ++⇘(domA (delete x Γ))⇙ (𝒩⦃delete x Γ⦄ρ'))( x := 𝒩⟦ e ⟧⇘𝒩⦃delete x Γ⦄ρ'⇙))" by (rule iterative_HSem', simp) finally have "(𝒩⦃Γ⦄ρ)f|` (- ?new) ⊑ (...) f|` (- ?new)" by (rule ssubst) (rule below_refl) also have "… ⊑ (μ ρ'. (ρ ++⇘domA Δ⇙ (𝒩⦃Δ⦄ρ'))( x := 𝒩⟦ z ⟧⇘𝒩⦃Δ⦄ρ'⇙)) f|` (- ?new)" proof (induction rule: parallel_fix_ind[where P ="λ x y. x f|` (- ?new) ⊑ y f|` (- ?new)"]) case 1 show ?case by simp next case 2 show ?case .. next case (3 σ σ') hence "𝒩⟦ e ⟧⇘𝒩⦃delete x Γ⦄σ⇙ ⊑ 𝒩⟦ e ⟧⇘𝒩⦃delete x Γ⦄σ'⇙" and "(𝒩⦃delete x Γ⦄σ) f|` domA (delete x Γ) ⊑ (𝒩⦃delete x Γ⦄σ') f|` domA (delete x Γ)" using fv_subset by (auto intro: ESem_fresh_cong_below HSem_fresh_cong_below env_restr_below_subset[OF _ 3]) from below_trans[OF this(1) Variable(3)[OF prem]] below_trans[OF this(2) Variable(4)[OF prem]] have "𝒩⟦ e ⟧⇘𝒩⦃delete x Γ⦄σ⇙ ⊑ 𝒩⟦ z ⟧⇘𝒩⦃Δ⦄σ'⇙" and "(𝒩⦃delete x Γ⦄σ) f|` domA (delete x Γ) ⊑ (𝒩⦃Δ⦄σ') f|` domA (delete x Γ)". thus ?case using subset by (auto intro!: fun_belowI simp add: lookup_override_on_eq lookup_env_restr_eq elim: env_restr_belowD) qed also have "… = (μ ρ'. (ρ ++⇘domA Δ⇙ (𝒩⦃Δ⦄ρ'))( x := 𝒩⟦ z ⟧⇘ρ'⇙)) f|` (-?new)" by (rule arg_cong[OF iterative_HSem'[symmetric], OF `x ∉ domA Δ`]) also have "… = (𝒩⦃(x,z) # Δ⦄ρ) f|` (-?new)" by (rule arg_cong[OF iterative_HSem[symmetric], OF `x ∉ domA Δ`]) finally show le: ?case by (rule env_restr_below_subset[OF `domA Γ ⊆ (-?new)`]) (intro cont2cont)+ have "𝒩⟦ Var x ⟧⇘𝒩⦃Γ⦄ρ⇙ ⊑ (𝒩⦃Γ⦄ρ) x" by (rule CESem_simps_no_tick) also have "… ⊑ (𝒩⦃(x, z) # Δ⦄ρ) x" using fun_belowD[OF le, where x = x] by simp also have "… = 𝒩⟦ z ⟧⇘𝒩⦃(x, z) # Δ⦄ρ⇙" by (simp add: lookup_HSem_heap) finally show "𝒩⟦ Var x ⟧⇘𝒩⦃Γ⦄ρ⇙ ⊑ 𝒩⟦ z ⟧⇘𝒩⦃(x, z) # Δ⦄ρ⇙" by this (intro cont2cont)+ next case (Bool b) case 1 show ?case by simp case 2 show ?case by simp next case (IfThenElse Γ scrut L Δ b e⇩1 e⇩2 Θ z) have Gamma_subset: "domA Γ ⊆ domA Δ" by (rule reds_doesnt_forget[OF IfThenElse.hyps(1)]) let ?e = "if b then e⇩1 else e⇩2" case 1 thm new_free_vars_on_heap[OF IfThenElse.hyps(1)] hence prem1: "fv (Γ, scrut) ⊆ set L ∪ domA Γ" and prem2: "fv (Δ, ?e) ⊆ set L ∪ domA Δ" and "fv ?e ⊆ domA Γ ∪ set L" using new_free_vars_on_heap[OF IfThenElse.hyps(1)] Gamma_subset by auto { fix r have "(𝒩⟦ (scrut ? e⇩1 : e⇩2) ⟧⇘𝒩⦃Γ⦄ρ⇙)⋅r ⊑ CB_project⋅((𝒩⟦ scrut ⟧⇘𝒩⦃Γ⦄ρ⇙)⋅r)⋅((𝒩⟦ e⇩1 ⟧⇘𝒩⦃Γ⦄ρ⇙)⋅r)⋅((𝒩⟦ e⇩2 ⟧⇘𝒩⦃Γ⦄ρ⇙)⋅r)" by (rule CESem_simps_no_tick) also have "… ⊑ CB_project⋅((𝒩⟦ Bool b ⟧⇘𝒩⦃Δ⦄ρ⇙)⋅r)⋅((𝒩⟦ e⇩1 ⟧⇘𝒩⦃Γ⦄ρ⇙)⋅r)⋅((𝒩⟦ e⇩2 ⟧⇘𝒩⦃Γ⦄ρ⇙)⋅r)" by (intro monofun_cfun_fun monofun_cfun_arg IfThenElse.hyps(2)[OF prem1]) also have "… = (𝒩⟦ ?e ⟧⇘𝒩⦃Γ⦄ρ⇙)⋅r" by (cases r) simp_all also have "… ⊑ (𝒩⟦ ?e ⟧⇘𝒩⦃Δ⦄ρ⇙)⋅r" proof(rule monofun_cfun_fun[OF ESem_fresh_cong_below_subset[OF `fv ?e ⊆ domA Γ ∪ set L` Env.env_restr_belowI]]) fix x assume "x ∈ domA Γ ∪ set L" thus "(𝒩⦃Γ⦄ρ) x ⊑ (𝒩⦃Δ⦄ρ) x" proof(cases "x ∈ domA Γ") assume "x ∈ domA Γ" from IfThenElse.hyps(3)[OF prem1] have "((𝒩⦃Γ⦄ρ) f|` domA Γ) x ⊑ ((𝒩⦃Δ⦄ρ) f|` domA Γ) x" by (rule fun_belowD) with `x ∈ domA Γ` show ?thesis by simp next assume "x ∉ domA Γ" from this `x ∈ domA Γ ∪ set L` reds_avoids_live[OF IfThenElse.hyps(1)] show ?thesis by (simp add: lookup_HSem_other) qed qed also have "… ⊑ (𝒩⟦ z ⟧⇘𝒩⦃Θ⦄ρ⇙)⋅r" by (intro monofun_cfun_fun monofun_cfun_arg IfThenElse.hyps(5)[OF prem2]) finally have "(𝒩⟦ (scrut ? e⇩1 : e⇩2) ⟧⇘𝒩⦃Γ⦄ρ⇙)⋅r ⊑ (𝒩⟦ z ⟧⇘𝒩⦃Θ⦄ρ⇙)⋅r" by this (intro cont2cont)+ } thus ?case by (rule cfun_belowI) show "(𝒩⦃Γ⦄ρ) f|` (domA Γ) ⊑ (𝒩⦃Θ⦄ρ) f|` (domA Γ)" using IfThenElse.hyps(3)[OF prem1] env_restr_below_subset[OF Gamma_subset IfThenElse.hyps(6)[OF prem2]] by (rule below_trans) next case (Let as Γ L body Δ z) case 1 have *: "domA as ∩ domA Γ = {}" by (metis Let.hyps(1) fresh_distinct) have "fv (as @ Γ, body) - domA (as @ Γ) ⊆ fv (Γ, Let as body) - domA Γ" by auto with 1 have prem: "fv (as @ Γ, body) ⊆ set L ∪ domA (as @ Γ)" by auto have f1: "atom ` domA as ♯* Γ" using Let(1) by (simp add: set_bn_to_atom_domA) have "𝒩⟦ Let as body ⟧⇘𝒩⦃Γ⦄ρ⇙ ⊑ 𝒩⟦ body ⟧⇘𝒩⦃as⦄𝒩⦃Γ⦄ρ⇙" by (rule CESem_simps_no_tick) also have "… = 𝒩⟦ body ⟧⇘𝒩⦃as @ Γ⦄ρ⇙" by (rule arg_cong[OF HSem_merge[OF f1]]) also have "… ⊑ 𝒩⟦ z ⟧⇘𝒩⦃Δ⦄ρ⇙" by (rule Let.hyps(4)[OF prem]) finally show ?case by this (intro cont2cont)+ have "(𝒩⦃Γ⦄ρ) f|` (domA Γ) = (𝒩⦃as⦄(𝒩⦃Γ⦄ρ)) f|` (domA Γ)" unfolding env_restr_HSem[OF *].. also have "𝒩⦃as⦄(𝒩⦃Γ⦄ρ) = (𝒩⦃as @ Γ⦄ρ)" by (rule HSem_merge[OF f1]) also have "… f|` domA Γ ⊑ (𝒩⦃Δ⦄ρ) f|` domA Γ" by (rule env_restr_below_subset[OF _ Let.hyps(5)[OF prem]]) simp finally show "(𝒩⦃Γ⦄ρ) f|` domA Γ ⊑ (𝒩⦃Δ⦄ρ) f|` domA Γ". qed corollary correctness_empty_env: assumes "Γ : e ⇓⇘L⇙ Δ : z" and "fv (Γ, e) ⊆ set L" shows "𝒩⟦e⟧⇘𝒩⦃Γ⦄⇙ ⊑ 𝒩⟦z⟧⇘𝒩⦃Δ⦄⇙" and "𝒩⦃Γ⦄ ⊑ 𝒩⦃Δ⦄" proof- from assms(2) have "fv (Γ, e) ⊆ set L ∪ domA Γ" by auto note corr = correctness[OF assms(1) this, where ρ = "⊥"] show "𝒩⟦ e ⟧⇘𝒩⦃Γ⦄⇙ ⊑ 𝒩⟦ z ⟧⇘𝒩⦃Δ⦄⇙" using corr(1). have "𝒩⦃Γ⦄ = (𝒩⦃Γ⦄) f|` domA Γ " using env_restr_useless[OF HSem_edom_subset, where ρ1 = "⊥"] by simp also have "… ⊑ (𝒩⦃Δ⦄) f|` domA Γ" using corr(2). also have "… ⊑ 𝒩⦃Δ⦄" by (rule env_restr_below_itself) finally show "𝒩⦃Γ⦄ ⊑ 𝒩⦃Δ⦄" by this (intro cont2cont)+ qed end