Theory Type_Preservation

theory Type_Preservation
  imports "HOL-Nominal.Nominal"
begin

text ‹

  This theory shows how to prove the type preservation
  property for the simply-typed lambda-calculus and 
  beta-reduction.
 
›

atom_decl name

nominal_datatype lam =
  Var "name"
| App "lam" "lam" 
| Lam "«name»lam" ("Lam [_]._")

text ‹Capture-Avoiding Substitution›

nominal_primrec
  subst :: "lam ⇒ name ⇒ lam ⇒ lam"  ("_[_::=_]")
where
  "(Var x)[y::=s] = (if x=y then s else (Var x))"
| "(App t⇩1 t⇩2)[y::=s] = App (t⇩1[y::=s]) (t⇩2[y::=s])"
| "x♯(y,s) ⟹ (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: abs_fresh)
apply(fresh_guess)+
done

lemma  subst_eqvt[eqvt]:
  fixes pi::"name prm"
  shows "pi∙(t1[x::=t2]) = (pi∙t1)[(pi∙x)::=(pi∙t2)]"
by (nominal_induct t1 avoiding: x t2 rule: lam.strong_induct)
   (auto simp add: perm_bij fresh_atm fresh_bij)

lemma fresh_fact:
  fixes z::"name"
  shows "⟦z♯s; (z=y ∨ z♯t)⟧ ⟹ z♯t[y::=s]"
by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
   (auto simp add: abs_fresh fresh_prod fresh_atm)

text ‹Types›

nominal_datatype ty =
    TVar "string"
  | TArr "ty" "ty" ("_ → _")

lemma ty_fresh:
  fixes x::"name"
  and   T::"ty"
  shows "x♯T"
by (induct T rule: ty.induct)
   (auto simp add: fresh_string)

text ‹Typing Contexts›

type_synonym ctx = "(name×ty) list"

abbreviation
  "sub_ctx" :: "ctx ⇒ ctx ⇒ bool" ("_ ⊆ _") 
where
  "Γ⇩1 ⊆ Γ⇩2 ≡ ∀x. x ∈ set Γ⇩1 ⟶ x ∈ set Γ⇩2"

text ‹Validity of Typing Contexts›

inductive
  valid :: "(name×ty) list ⇒ bool"
where
    v1[intro]: "valid []"
  | v2[intro]: "⟦valid Γ; x♯Γ⟧⟹ valid ((x,T)#Γ)"

equivariance valid

lemma valid_elim[dest]:
  assumes a: "valid ((x,T)#Γ)"
  shows "x♯Γ ∧ valid Γ"
using a by (cases) (auto)

lemma valid_insert:
  assumes a: "valid (Δ@[(x,T)]@Γ)"
  shows "valid (Δ @ Γ)" 
using a
by (induct Δ)
   (auto simp add:  fresh_list_append fresh_list_cons dest!: valid_elim)

lemma fresh_set: 
  shows "y♯xs = (∀x∈set xs. y♯x)"
by (induct xs) (simp_all add: fresh_list_nil fresh_list_cons)

lemma context_unique:
  assumes a1: "valid Γ"
  and     a2: "(x,T) ∈ set Γ"
  and     a3: "(x,U) ∈ set Γ"
  shows "T = U" 
using a1 a2 a3
by (induct) (auto simp add: fresh_set fresh_prod fresh_atm)

text ‹Typing Relation›

inductive
  typing :: "ctx ⇒ lam ⇒ ty ⇒ bool" ("_ ⊢ _ : _") 
where
  t_Var[intro]: "⟦valid Γ; (x,T)∈set Γ⟧ ⟹ Γ ⊢ Var x : T"
| t_App[intro]: "⟦Γ ⊢ t⇩1 : T⇩1→T⇩2; Γ ⊢ t⇩2 : T⇩1⟧ ⟹ Γ ⊢ App t⇩1 t⇩2 : T⇩2"
| t_Lam[intro]: "⟦x♯Γ; (x,T⇩1)#Γ ⊢ t : T⇩2⟧ ⟹ Γ ⊢ Lam [x].t : T⇩1→T⇩2"

equivariance typing
nominal_inductive typing
  by (simp_all add: abs_fresh ty_fresh)

lemma t_Lam_inversion[dest]:
  assumes ty: "Γ ⊢ Lam [x].t : T" 
  and     fc: "x♯Γ" 
  shows "∃T⇩1 T⇩2. T = T⇩1 → T⇩2 ∧ (x,T⇩1)#Γ ⊢ t : T⇩2"
using ty fc 
by (cases rule: typing.strong_cases) 
   (auto simp add: alpha lam.inject abs_fresh ty_fresh)

lemma t_App_inversion[dest]:
  assumes ty: "Γ ⊢ App t1 t2 : T" 
  shows "∃T'. Γ ⊢ t1 : T' → T ∧ Γ ⊢ t2 : T'"
using ty 
by (cases) (auto simp add: lam.inject)

lemma weakening: 
  fixes Γ1 Γ2::"ctx"
  assumes a: "Γ1 ⊢ t : T" 
  and     b: "valid Γ2" 
  and     c: "Γ1 ⊆ Γ2"
  shows "Γ2 ⊢ t : T"
using a b c
by (nominal_induct Γ1 t T avoiding: Γ2 rule: typing.strong_induct)
   (auto | atomize)+

lemma type_substitution_aux:
  assumes a: "(Δ@[(x,T')]@Γ) ⊢ e : T"
  and     b: "Γ ⊢ e' : T'"
  shows "(Δ@Γ) ⊢ e[x::=e'] : T" 
using a b 
proof (nominal_induct "Δ@[(x,T')]@Γ" e T avoiding: x e' Δ rule: typing.strong_induct)
  case (t_Var y T x e' Δ)
  then have a1: "valid (Δ@[(x,T')]@Γ)" 
       and  a2: "(y,T) ∈ set (Δ@[(x,T')]@Γ)" 
       and  a3: "Γ ⊢ e' : T'" .
  from a1 have a4: "valid (Δ@Γ)" by (rule valid_insert)
  { assume eq: "x=y"
    from a1 a2 have "T=T'" using eq by (auto intro: context_unique)
    with a3 have "Δ@Γ ⊢ Var y[x::=e'] : T" using eq a4 by (auto intro: weakening)
  }
  moreover
  { assume ineq: "x≠y"
    from a2 have "(y,T) ∈ set (Δ@Γ)" using ineq by simp
    then have "Δ@Γ ⊢ Var y[x::=e'] : T" using ineq a4 by auto
  }
  ultimately show "Δ@Γ ⊢ Var y[x::=e'] : T" by blast
qed (force simp add: fresh_list_append fresh_list_cons)+

corollary type_substitution:
  assumes a: "(x,T')#Γ ⊢ e : T"
  and     b: "Γ ⊢ e' : T'"
  shows "Γ ⊢ e[x::=e'] : T"
using a b
by (auto intro: type_substitution_aux[where Δ="[]",simplified])

text ‹Beta Reduction›

inductive 
  "beta" :: "lam⇒lam⇒bool" (" _ ⟶⇩β _")
where
  b1[intro]: "t1 ⟶⇩β t2 ⟹ App t1 s ⟶⇩β App t2 s"
| b2[intro]: "s1 ⟶⇩β s2 ⟹ App t s1 ⟶⇩β App t s2"
| b3[intro]: "t1 ⟶⇩β t2 ⟹ Lam [x].t1 ⟶⇩β Lam [x].t2"
| b4[intro]: "x♯s ⟹ App (Lam [x].t) s ⟶⇩β t[x::=s]"

equivariance beta
nominal_inductive beta
  by (auto simp add: abs_fresh fresh_fact)


theorem type_preservation:
  assumes a: "t ⟶⇩β t'"
  and     b: "Γ ⊢ t : T" 
  shows "Γ ⊢ t' : T" 
using a b
proof (nominal_induct avoiding: Γ T rule: beta.strong_induct)
  case (b1 t1 t2 s Γ T)
  have "Γ ⊢ App t1 s : T" by fact
  then obtain T' where a1: "Γ ⊢ t1 : T' → T" and a2: "Γ ⊢ s : T'" by auto
  have ih: "Γ ⊢ t1 : T' → T ⟹ Γ ⊢ t2 : T' → T" by fact
  with a1 a2 show "Γ ⊢ App t2 s : T" by auto
next 
  case (b2 s1 s2 t Γ T)
  have "Γ ⊢ App t s1 : T" by fact
  then obtain T' where a1: "Γ ⊢ t : T' → T" and a2: "Γ ⊢ s1 : T'" by auto
  have ih: "Γ ⊢ s1 : T' ⟹ Γ ⊢ s2 : T'" by fact
  with a1 a2 show "Γ ⊢ App t s2 : T" by auto
next 
  case (b3 t1 t2 x Γ T)
  have vc: "x♯Γ" by fact
  have "Γ ⊢ Lam [x].t1 : T" by fact
  then obtain T1 T2 where a1: "(x,T1)#Γ ⊢ t1 : T2" and a2: "T = T1 → T2" using vc by auto
  have ih: "(x,T1)#Γ ⊢ t1 : T2 ⟹ (x,T1)#Γ ⊢ t2 : T2" by fact
  with a1 a2 show "Γ ⊢ Lam [x].t2 : T" using vc by auto
next
  case (b4 x s t Γ T)
  have vc: "x♯Γ" by fact
  have "Γ ⊢ App (Lam [x].t) s : T" by fact
  then obtain T' where a1: "Γ ⊢ Lam [x].t : T' → T" and a2: "Γ ⊢ s : T'" by auto
  from a1 obtain T1 T2 where a3: "(x,T')#Γ ⊢ t : T" using vc by (auto simp add: ty.inject)
  from a3 a2 show "Γ ⊢ t[x::=s] : T" by (simp add: type_substitution)
qed


theorem type_preservation_automatic:
  assumes a: "t ⟶⇩β t'"
  and     b: "Γ ⊢ t : T" 
  shows "Γ ⊢ t' : T"
using a b
by (nominal_induct avoiding: Γ T rule: beta.strong_induct)
   (auto dest!: t_Lam_inversion t_App_inversion simp add: ty.inject type_substitution)

end