Theory CorrectnessOriginal (Isabelle2016: February 2016)

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⇩₁ e⇩₂ Θ v)
  have Gamma_subset: "domA Γ ⊆ domA Δ"
    by (rule reds_doesnt_forget[OF IfThenElse.hyps(1)])

  let ?e = "if b then e⇩₁ else e⇩₂"

  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

  have "⟦ (scrut ? e⇩₁ : e⇩₂) ⟧⇘_{⦃Γ⦄ρ⇙} = B_project⋅(⟦ scrut ⟧⇘_{⦃Γ⦄ρ⇙})⋅(⟦ e⇩₁ ⟧⇘_{⦃Γ⦄ρ⇙})⋅(⟦ e⇩₂ ⟧⇘_{⦃Γ⦄ρ⇙})" by simp
  also have "… = B_project⋅(⟦ Bool b ⟧⇘_{⦃Δ⦄ρ⇙})⋅(⟦ e⇩₁ ⟧⇘_{⦃Γ⦄ρ⇙})⋅(⟦ e⇩₂ ⟧⇘_{⦃Γ⦄ρ⇙})"
    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