# Theory Type_Preservation

theory Type_Preservation
imports Nominal
```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(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
```