Theory CorrectnessOriginal

theory CorrectnessOriginal
imports Denotational Launchbury
begin

text ‹
This is the main correctness theorem, Theorem 2 from \<^cite>‹"launchbury"›.
›

(* Another possible invariant seems to be: "edom ρ - domA Γ ⊆ set L" *)

theorem correctness:
  assumes "Γ : e ⇓⇘L⇙ Δ : v"
  and     "fv (Γ, e) ⊆ set L ∪ domA Γ"
  shows   "⟦e⟧⇘⦃Γ⦄ρ⇙ = ⟦v⟧⇘⦃Δ⦄ρ⇙"
  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 Δ Θ v 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
    from Application.hyps(10)[OF prem1, where ρ = ρ]
    have "((⦃Γ⦄ρ) f|` domA Γ) x  = ((⦃Δ⦄ρ) f|` domA Γ) x" by simp
    with True show ?thesis 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

  text_raw ‹% nice proof start›
  have "⟦ App e x ⟧⇘⦃Γ⦄ρ⇙ = (⟦ e ⟧⇘⦃Γ⦄ρ⇙) ↓Fn (⦃Γ⦄ρ) x"
    by simp
  also have "… = (⟦ Lam [y]. e' ⟧⇘⦃Δ⦄ρ⇙) ↓Fn (⦃Γ⦄ρ) x"
    using Application.hyps(9)[OF prem1] by simp
  also have "… = (⟦ Lam [y]. e' ⟧⇘⦃Δ⦄ρ⇙) ↓Fn (⦃Δ⦄ρ) x"
    unfolding *..
  also have "… = (Fn⋅(Λ z. ⟦ e' ⟧⇘(⦃Δ⦄ρ)(y := z)⇙)) ↓Fn (⦃Δ⦄ρ) x"
    by simp
  also have "… = ⟦ e' ⟧⇘(⦃Δ⦄ρ)(y := (⦃Δ⦄ρ) x)⇙"
    by simp
  also have "… = ⟦ e'[y ::= x] ⟧⇘⦃Δ⦄ρ⇙"
    unfolding ESem_subst..
  also have "… = ⟦ v ⟧⇘⦃Θ⦄ρ⇙"
    by (rule Application.hyps(12)[OF prem2])
  finally
  show "⟦ App e x ⟧⇘⦃Γ⦄ρ⇙ = ⟦ v ⟧⇘⦃Θ⦄ρ⇙".
  text_raw ‹% nice proof end›
  
  show "(⦃Γ⦄ρ) f|` domA Γ = (⦃Θ⦄ρ) f|` domA Γ"
    using Application.hyps(10)[OF prem1]
          env_restr_eq_subset[OF Gamma_subset Application.hyps(13)[OF prem2]]
    by (rule trans)
next
case (Variable Γ x e L Δ v)
  hence [simp]:"x ∈ domA Γ" by (metis domA_from_set map_of_SomeD)

  let ?Γ = "delete x Γ"

  case 2
  have "x ∉ domA Δ"
    by (rule reds_avoids_live[OF Variable.hyps(2)], simp_all)

  have subset: "domA ?Γ ⊆ domA Δ"
    by (rule reds_doesnt_forget[OF Variable.hyps(2)])

  let "?new" = "domA Δ - domA Γ"
  have "fv (?Γ, e) ∪ {x} ⊆ fv (Γ, Var x)"
    by (rule fv_delete_heap[OF ‹map_of Γ x = Some e›])
  hence prem: "fv (?Γ, e) ⊆ set (x # L) ∪ domA ?Γ" using 2 by auto
  hence fv_subset: "fv (?Γ, e) - domA ?Γ ⊆ - ?new"
    using reds_avoids_live'[OF Variable.hyps(2)] by auto

  have "domA Γ ⊆ (-?new)" by auto

  have "⦃Γ⦄ρ = ⦃(x,e) # ?Γ⦄ρ"
    by (rule HSem_reorder[OF map_of_delete_insert[symmetric, OF Variable(1)]])
  also have "… = (μ ρ'. (ρ ++⇘(domA ?Γ)⇙ (⦃?Γ⦄ρ'))( x := ⟦ e ⟧⇘ρ'⇙))"
    by (rule iterative_HSem, simp)
  also have "… = (μ ρ'. (ρ ++⇘(domA ?Γ)⇙ (⦃?Γ⦄ρ'))( x := ⟦ e ⟧⇘⦃?Γ⦄ρ'⇙))"
    by (rule iterative_HSem', simp)
  finally
  have "(⦃Γ⦄ρ)f|` (- ?new) = (...) f|` (- ?new)" by simp
  also have "… = (μ ρ'. (ρ ++⇘domA Δ⇙ (⦃Δ⦄ρ'))( x := ⟦ v ⟧⇘⦃Δ⦄ρ'⇙)) 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 ⟧⇘⦃?Γ⦄σ⇙ = ⟦ e ⟧⇘⦃?Γ⦄σ'⇙"
      and "(⦃?Γ⦄σ) f|` domA ?Γ = (⦃?Γ⦄σ') f|` domA ?Γ"
      using fv_subset by (auto intro: ESem_fresh_cong HSem_fresh_cong  env_restr_eq_subset[OF _ 3])
    from trans[OF this(1) Variable(3)[OF prem]] trans[OF this(2) Variable(4)[OF prem]]
    have  "⟦ e ⟧⇘⦃?Γ⦄σ⇙ = ⟦ v ⟧⇘⦃Δ⦄σ'⇙"
       and "(⦃?Γ⦄σ) f|` domA ?Γ = (⦃Δ⦄σ') f|` domA ?Γ".
    thus ?case
      using subset
      by (fastforce simp add: lookup_override_on_eq  lookup_env_restr_eq dest: env_restr_eqD )
  qed
  also have "… = (μ ρ'. (ρ ++⇘domA Δ⇙ (⦃Δ⦄ρ'))( x := ⟦ v ⟧⇘ρ'⇙)) f|` (-?new)"
    by (rule arg_cong[OF iterative_HSem'[symmetric], OF ‹x ∉ domA Δ›])
  also have "… = (⦃(x,v) # Δ⦄ρ)  f|` (-?new)"
    by (rule arg_cong[OF iterative_HSem[symmetric], OF ‹x ∉ domA Δ›])
  finally
  show le: ?case by (rule env_restr_eq_subset[OF ‹domA Γ ⊆ (-?new)›])

  have "⟦ Var x ⟧⇘⦃Γ⦄ρ⇙ = ⟦ Var x ⟧⇘⦃(x, v) # Δ⦄ρ⇙"
    using env_restr_eqD[OF le, where x = x]
    by simp
  also have "… = ⟦ v ⟧⇘⦃(x, v) # Δ⦄ρ⇙"
    by (auto simp add: lookup_HSem_heap)
  finally
  show "⟦ Var x ⟧⇘⦃Γ⦄ρ⇙ = ⟦ v ⟧⇘⦃(x, v) # Δ⦄ρ⇙".
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 Θ v)
  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

  have "⟦ (scrut ? e⇩1 : e⇩2) ⟧⇘⦃Γ⦄ρ⇙ = B_project⋅(⟦ scrut ⟧⇘⦃Γ⦄ρ⇙)⋅(⟦ e⇩1 ⟧⇘⦃Γ⦄ρ⇙)⋅(⟦ e⇩2 ⟧⇘⦃Γ⦄ρ⇙)" by simp
  also have "… = B_project⋅(⟦ Bool b ⟧⇘⦃Δ⦄ρ⇙)⋅(⟦ e⇩1 ⟧⇘⦃Γ⦄ρ⇙)⋅(⟦ e⇩2 ⟧⇘⦃Γ⦄ρ⇙)"
    unfolding IfThenElse.hyps(2)[OF prem1]..
  also have "… = ⟦ ?e ⟧⇘⦃Γ⦄ρ⇙" by simp
  also have "… = ⟦ ?e ⟧⇘⦃Δ⦄ρ⇙"
    proof(rule ESem_fresh_cong_subset[OF  ‹fv ?e ⊆ domA Γ ∪ set L› env_restr_eqI])
      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 simp
        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 "… = ⟦ v ⟧⇘⦃Θ⦄ρ⇙"
    unfolding IfThenElse.hyps(5)[OF prem2]..
  finally
  show ?case.
  thm env_restr_eq_subset
  show "(⦃Γ⦄ρ) f|` domA Γ = (⦃Θ⦄ρ) f|` domA Γ"
    using IfThenElse.hyps(3)[OF prem1]
          env_restr_eq_subset[OF Gamma_subset IfThenElse.hyps(6)[OF prem2]]
    by (rule trans)
next
case (Let as Γ L body Δ v)
  case 1
  { fix a
    assume a: "a ∈ domA  as"
    have "atom a ♯ Γ" 
      by (rule Let(1)[unfolded fresh_star_def, rule_format, OF imageI[OF a]])
    hence "a ∉ domA Γ"
      by (metis domA_not_fresh)
  }
  note * = this

  
  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 (simp)
  also have "… = ⟦ body ⟧⇘⦃as @ Γ⦄ρ⇙"
    by (rule arg_cong[OF HSem_merge[OF f1]])
  also have "… = ⟦ v ⟧⇘⦃Δ⦄ρ⇙"
    by (rule Let.hyps(4)[OF prem])
  finally
  show ?case.

  have "(⦃Γ⦄ρ) f|` (domA Γ) = (⦃as⦄(⦃Γ⦄ρ)) f|` (domA Γ)"
    apply (rule ext)
    apply (case_tac "x ∈ domA as")
    apply (auto simp add: lookup_HSem_other lookup_env_restr_eq *)
    done
  also have "… = (⦃as @ Γ⦄ρ) f|` (domA Γ)"
    by (rule arg_cong[OF HSem_merge[OF f1]])
  also have "… = (⦃Δ⦄ρ) f|` (domA Γ)"
    by (rule env_restr_eq_subset[OF _ Let.hyps(5)[OF prem]]) simp
  finally
  show "(⦃Γ⦄ρ) f|` domA Γ = (⦃Δ⦄ρ) f|` domA Γ".
qed

end