Theory Launchbury

theory Launchbury
imports Terms Substitution
begin

subsubsection ‹The natural semantics›

text ‹This is the semantics as in \<^cite>‹"launchbury"›, with two differences:
\begin{itemize}
\item Explicit freshness requirements for bound variables in the application and the Let rule.
\item An additional parameter that stores variables that have to be avoided, but do not occur
in the judgement otherwise, follwing \<^cite>‹"sestoft"›.
\end{itemize}
›

inductive
  reds :: "heap ⇒ exp ⇒ var list ⇒ heap ⇒ exp ⇒ bool"
  ("_ : _ ⇓⇘_⇙ _ : _" [50,50,50,50] 50)
where
  Lambda:
    "Γ : (Lam [x]. e) ⇓⇘L⇙ Γ : (Lam [x]. e)" 
 | Application: "⟦
    atom y ♯ (Γ,e,x,L,Δ,Θ,z) ;
    Γ : e ⇓⇘L⇙ Δ : (Lam [y]. e');
    Δ : e'[y ::= x] ⇓⇘L⇙ Θ : z
  ⟧  ⟹
    Γ : App e x ⇓⇘L⇙ Θ : z" 
 | Variable: "⟦
    map_of Γ x = Some e; delete x Γ : e ⇓⇘x#L⇙ Δ : z
  ⟧ ⟹
    Γ : Var x ⇓⇘L⇙ (x, z) # Δ : z"
 | Let: "⟦
    atom ` domA Δ ♯* (Γ, L);
    Δ @ Γ : body ⇓⇘L⇙ Θ : z
  ⟧ ⟹
    Γ : Let Δ body ⇓⇘L⇙ Θ : z"
 | Bool:
    "Γ : Bool b ⇓⇘L⇙ Γ : Bool b"
 | IfThenElse: "⟦
    Γ : scrut ⇓⇘L⇙ Δ : (Bool b);
    Δ : (if b then e⇩1 else e⇩2) ⇓⇘L⇙ Θ : z
  ⟧  ⟹
    Γ : (scrut ? e⇩1 : e⇩2) ⇓⇘L⇙ Θ : z"

equivariance reds

nominal_inductive reds
  avoids Application: "y"
  by (auto simp add: fresh_star_def fresh_Pair)

subsubsection ‹Example evaluations›

lemma eval_test:
  "[] : (Let [(x, Lam [y]. Var y)] (Var x)) ⇓⇘[]⇙ [(x, Lam [y]. Var y)] : (Lam [y]. Var y)"
apply(auto intro!: Lambda Application Variable Let
 simp add: fresh_Pair fresh_Cons fresh_Nil fresh_star_def)
done

lemma eval_test2:
  "y ≠ x ⟹ n ≠ y ⟹ n ≠ x ⟹[] : (Let [(x, Lam [y]. Var y)] (App (Var x) x)) ⇓⇘[]⇙ [(x, Lam [y]. Var y)] : (Lam [y]. Var y)"
  by (auto intro!: Lambda Application Variable Let simp add: fresh_Pair fresh_at_base fresh_Cons fresh_Nil fresh_star_def pure_fresh)

subsubsection ‹Better introduction rules›

text ‹
This variant do not require freshness.
›

lemma reds_ApplicationI:
  assumes "Γ : e ⇓⇘L⇙ Δ : Lam [y]. e'"
  assumes "Δ : e'[y::=x] ⇓⇘L⇙ Θ : z"
  shows "Γ : App e x ⇓⇘L⇙ Θ : z"
proof-
  obtain y' :: var where "atom y' ♯ (Γ, e, x, L, Δ, Θ, z, e')" by (rule obtain_fresh)

  have a: "Lam [y']. ((y' ↔ y) ∙ e') = Lam [y]. e'"
    using ‹atom y' ♯ _›
    by (auto simp add: Abs1_eq_iff fresh_Pair fresh_at_base)

  have b: "((y' ↔ y) ∙ e')[y'::=x] = e'[y::=x]"
  proof(cases "x = y")
    case True
    have "atom y' ♯ e'" using ‹atom y' ♯ _› by simp
    thus ?thesis
      by (simp add: True subst_swap_same  subst_subst_back)
  next
    case False
    hence "atom y ♯ x" by simp

    have [simp]: "(y' ↔ y) ∙ x = x" using ‹atom y ♯ _›  ‹atom y' ♯ _›
        by (simp add: flip_fresh_fresh fresh_Pair fresh_at_base)

    have "((y' ↔ y) ∙ e')[y'::=x] = (y' ↔ y) ∙ (e'[y::=x])" by simp
    also have "… = e'[y::=x]"
      using ‹atom y ♯ _›  ‹atom y' ♯ _›
      by (simp add: flip_fresh_fresh fresh_Pair fresh_at_base subst_pres_fresh)
    finally
    show ?thesis.
  qed
  have "atom y' ♯ (Γ, e, x, L, Δ, Θ, z)" using  ‹atom y' ♯ _› by (simp add: fresh_Pair)
  from this assms[folded a b]
  show ?thesis ..
qed

lemma reds_SmartLet: "⟦
    atom ` domA Δ ♯* (Γ, L);
    Δ @ Γ : body ⇓⇘L⇙ Θ : z
  ⟧ ⟹
    Γ : SmartLet Δ body ⇓⇘L⇙ Θ : z"
unfolding SmartLet_def
by (auto intro: reds.Let)

text ‹
A single rule for values
›
lemma reds_isValI:
  "isVal z ⟹ Γ : z ⇓⇘L⇙ Γ : z"
by (cases z rule:isVal.cases) (auto intro: reds.intros)


subsubsection ‹Properties of the semantics›

text ‹
Heap entries are never removed.
›

lemma reds_doesnt_forget:
  "Γ : e ⇓⇘L⇙ Δ : z ⟹ domA Γ ⊆ domA Δ"
by(induct rule: reds.induct) auto

text ‹
Live variables are not added to the heap.
›

lemma reds_avoids_live':
 assumes "Γ : e ⇓⇘L⇙ Δ : z"
 shows "(domA Δ - domA Γ) ∩ set L = {}"
using assms
by(induct rule:reds.induct)
  (auto dest: map_of_domAD fresh_distinct_list simp add: fresh_star_Pair)

lemma reds_avoids_live:
  "⟦ Γ : e ⇓⇘L⇙ Δ : z;
   x ∈ set L;
   x ∉ domA Γ
  ⟧ ⟹ x ∉ domA Δ"
using reds_avoids_live' by blast

text ‹
Fresh variables either stay fresh or are added to the heap.
›

lemma reds_fresh:" ⟦ Γ : e ⇓⇘L⇙ Δ : z;
   atom (x::var) ♯ (Γ, e)
  ⟧ ⟹ atom x ♯ (Δ, z) ∨ x ∈ (domA Δ - set L)"
proof(induct rule: reds.induct)
case (Lambda Γ x e) thus ?case by auto
next
case (Application y Γ e x' L Δ Θ z e')
  hence "atom x ♯ (Δ, Lam [y]. e') ∨ x ∈ domA Δ - set (x' # L)" by (auto simp add: fresh_Pair)

  thus ?case
  proof
    assume  "atom x ♯ (Δ, Lam [y]. e')"
    hence "atom x ♯ e'[y ::= x']"
      using Application.prems
      by (auto intro: subst_pres_fresh simp add: fresh_Pair)
    thus ?thesis using Application.hyps(5) ‹atom x ♯ (Δ, Lam [y]. e')› by auto
  next
    assume "x ∈ domA Δ - set (x' # L)"
    thus ?thesis using reds_doesnt_forget[OF Application.hyps(4)] by auto
  qed
next

case(Variable Γ v e L Δ z)
  have "atom x ♯ Γ" and "atom x ♯ v" using Variable.prems(1) by (auto simp add: fresh_Pair)
  from fresh_delete[OF this(1)]
  have "atom x ♯ delete v Γ".
  moreover
  have "v ∈ domA Γ" using Variable.hyps(1) by (metis domA_from_set map_of_SomeD)
  from fresh_map_of[OF this  ‹atom x ♯ Γ›]
  have "atom x ♯ the (map_of Γ v)".
  hence "atom x ♯ e" using ‹map_of Γ v = Some e› by simp
  ultimately
  have "atom x ♯ (Δ, z) ∨ x ∈ domA Δ - set (v # L)"  using Variable.hyps(3) by (auto simp add: fresh_Pair)
  thus ?case using ‹atom x ♯ v› by (auto simp add: fresh_Pair fresh_Cons fresh_at_base)
next

case (Bool Γ b L)
  thus ?case by auto
next

case (IfThenElse Γ scrut L Δ b e⇩1 e⇩2 Θ z)
  from ‹atom x ♯ (Γ, scrut ? e⇩1 : e⇩2)›
  have "atom x ♯ (Γ, scrut)" and "atom x ♯ (e⇩1, e⇩2)" by (auto simp add: fresh_Pair)
  from IfThenElse.hyps(2)[OF this(1)]
  show ?case
  proof
    assume "atom x ♯ (Δ, Bool b)" with ‹atom x ♯ (e⇩1, e⇩2)›
    have "atom x ♯ (Δ, if b then e⇩1 else e⇩2)" by auto
    from IfThenElse.hyps(4)[OF this]
    show ?thesis.
  next
    assume "x ∈ domA Δ - set L"
    with reds_doesnt_forget[OF ‹Δ : (if b then e⇩1 else e⇩2) ⇓⇘L⇙ Θ : z›]
    show ?thesis by auto
  qed
next

case (Let Δ Γ L body Θ z)
  show ?case
  proof (cases "x ∈ domA Δ")
    case False
      hence "atom x ♯ Δ" using Let.prems by(auto simp add: fresh_Pair)      
      show ?thesis
        apply(rule Let.hyps(3))
        using Let.prems ‹atom x ♯ Δ› False
        by (auto simp add: fresh_Pair fresh_append)
  next
    case True
      hence "x ∉ set L"
        using Let(1)
        by (metis fresh_PairD(2) fresh_star_def image_eqI set_not_fresh)
      with True
      show ?thesis
      using reds_doesnt_forget[OF Let.hyps(2)] by auto
  qed
qed

lemma reds_fresh_fv: "⟦ Γ : e ⇓⇘L⇙ Δ : z;
   x ∈ fv (Δ, z) ∧ (x ∉ domA Δ ∨  x ∈ set L)
  ⟧ ⟹ x ∈ fv (Γ, e)"
using reds_fresh
unfolding fv_def fresh_def
by blast

lemma new_free_vars_on_heap:
  assumes "Γ : e ⇓⇘L⇙ Δ : z"
  shows "fv (Δ, z) - domA Δ ⊆ fv (Γ, e) - domA Γ"
using reds_fresh_fv[OF assms(1)] reds_doesnt_forget[OF assms(1)] by auto

lemma reds_pres_closed:
  assumes "Γ : e ⇓⇘L⇙ Δ : z"
  and     "fv (Γ, e) ⊆ set L ∪ domA Γ"
  shows   "fv (Δ, z) ⊆ set L ∪ domA Δ"
using new_free_vars_on_heap[OF assms(1)] assms(2) by auto

text ‹
Reducing the set of variables to avoid is always possible.
› 

lemma reds_smaller_L: "⟦ Γ : e ⇓⇘L⇙ Δ : z;
   set L' ⊆ set L
  ⟧ ⟹ Γ : e ⇓⇘L'⇙ Δ : z"
proof(nominal_induct avoiding : L' rule: reds.strong_induct)
case (Lambda Γ x e L L')
  show ?case
    by (rule reds.Lambda)
next
case (Application y Γ e xa L Δ Θ z e' L')
  from Application.hyps(10)[OF Application.prems] Application.hyps(12)[OF Application.prems]
  show ?case
    by (rule reds_ApplicationI)
next 
case (Variable Γ xa e L Δ z L')
  have "set (xa # L') ⊆ set (xa # L)"
    using Variable.prems by auto
  thus ?case
    by (rule reds.Variable[OF Variable(1) Variable.hyps(3)])
next
case (Bool b)
  show ?case..
next
case (IfThenElse Γ scrut L Δ b e⇩1 e⇩2 Θ z L')
  thus ?case by (metis  reds.IfThenElse)
next
case (Let Δ Γ  L body Θ z L')
  have "atom ` domA Δ ♯* (Γ, L')"
    using Let(1-3) Let.prems
    by (auto simp add: fresh_star_Pair  fresh_star_set_subset)
  thus ?case
    by (rule reds.Let[OF _ Let.hyps(4)[OF Let.prems]])
qed

text ‹Things are evaluated to a lambda expression, and the variable can be freely chose.›

lemma result_evaluated:
  "Γ : e ⇓⇘L⇙ Δ : z ⟹ isVal z"
by (induct Γ e L Δ z rule:reds.induct) (auto dest: reds_doesnt_forget)


lemma result_evaluated_fresh:
  assumes "Γ : e ⇓⇘L⇙ Δ : z"
  obtains y e'
  where "z = (Lam [y]. e')" and "atom y ♯ (c::'a::fs)" | b where "z = Bool b"
proof-
  from assms
  have "isVal z" by (rule result_evaluated)
  hence "(∃ y e'. z = Lam [y]. e' ∧ atom y ♯ c) ∨ (∃ b. z = Bool b)"
    by (nominal_induct z avoiding: c rule:exp_strong_induct) auto
  thus thesis using that by blast
qed

end