Theory CorrectnessResourced

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

  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