# Theory SN

theory SN
imports Lam_Funs
```theory SN
imports Lam_Funs
begin

text ‹Strong Normalisation proof from the Proofs and Types book›

section ‹Beta Reduction›

lemma subst_rename:
assumes a: "c♯t1"
shows "t1[a::=t2] = ([(c,a)]∙t1)[c::=t2]"
using a
by (nominal_induct t1 avoiding: a c t2 rule: lam.strong_induct)
(auto simp add: calc_atm fresh_atm abs_fresh)

lemma forget:
assumes a: "a♯t1"
shows "t1[a::=t2] = t1"
using a
by (nominal_induct t1 avoiding: a t2 rule: lam.strong_induct)

lemma fresh_fact:
fixes a::"name"
assumes a: "a♯t1" "a♯t2"
shows "a♯t1[b::=t2]"
using a
by (nominal_induct t1 avoiding: a b t2 rule: lam.strong_induct)

lemma fresh_fact':
fixes a::"name"
assumes a: "a♯t2"
shows "a♯t1[a::=t2]"
using a
by (nominal_induct t1 avoiding: a t2 rule: lam.strong_induct)

lemma subst_lemma:
assumes a: "x≠y"
and     b: "x♯L"
shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
using a b
by (nominal_induct M avoiding: x y N L rule: lam.strong_induct)

lemma id_subs:
shows "t[x::=Var x] = t"
by (nominal_induct t avoiding: x rule: lam.strong_induct)

lemma lookup_fresh:
fixes z::"name"
assumes "z♯θ" "z♯x"
shows "z♯ lookup θ x"
using assms
by (induct rule: lookup.induct) (auto simp add: fresh_list_cons)

lemma lookup_fresh':
assumes "z♯θ"
shows "lookup θ z = Var z"
using assms
by (induct rule: lookup.induct)
(auto simp add: fresh_list_cons fresh_prod fresh_atm)

lemma psubst_subst:
assumes h:"c♯θ"
shows "(θ<t>)[c::=s] = ((c,s)#θ)<t>"
using h
by (nominal_induct t avoiding: θ c s rule: lam.strong_induct)
(auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh')

inductive
Beta :: "lam⇒lam⇒bool" (" _ ⟶⇩β _" [80,80] 80)
where
b1[intro!]: "s1 ⟶⇩β s2 ⟹ App s1 t ⟶⇩β App s2 t"
| b2[intro!]: "s1⟶⇩βs2 ⟹ App t s1 ⟶⇩β App t s2"
| b3[intro!]: "s1⟶⇩βs2 ⟹ Lam [a].s1 ⟶⇩β Lam [a].s2"
| b4[intro!]: "a♯s2 ⟹ App (Lam [a].s1) s2⟶⇩β (s1[a::=s2])"

equivariance Beta

nominal_inductive Beta

lemma beta_preserves_fresh:
fixes a::"name"
assumes a: "t⟶⇩β s"
shows "a♯t ⟹ a♯s"
using a
apply(nominal_induct t s avoiding: a rule: Beta.strong_induct)
apply(auto simp add: abs_fresh fresh_fact fresh_atm)
done

lemma beta_abs:
assumes a: "Lam [a].t⟶⇩β t'"
shows "∃t''. t'=Lam [a].t'' ∧ t⟶⇩β t''"
proof -
have "a♯Lam [a].t" by (simp add: abs_fresh)
with a have "a♯t'" by (simp add: beta_preserves_fresh)
with a show ?thesis
by (cases rule: Beta.strong_cases[where a="a" and aa="a"])
(auto simp add: lam.inject abs_fresh alpha)
qed

lemma beta_subst:
assumes a: "M ⟶⇩β M'"
shows "M[x::=N]⟶⇩β M'[x::=N]"
using a
by (nominal_induct M M' avoiding: x N rule: Beta.strong_induct)
(auto simp add: fresh_atm subst_lemma fresh_fact)

section ‹types›

nominal_datatype ty =
TVar "nat"
| TArr "ty" "ty" (infix "→" 200)

lemma fresh_ty:
fixes a ::"name"
and   τ  ::"ty"
shows "a♯τ"
by (nominal_induct τ rule: ty.strong_induct)

(* valid contexts *)

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

equivariance valid

(* typing judgements *)

lemma fresh_context:
fixes  Γ :: "(name×ty)list"
and    a :: "name"
assumes a: "a♯Γ"
shows "¬(∃τ::ty. (a,τ)∈set Γ)"
using a
by (induct Γ)
(auto simp add: fresh_prod fresh_list_cons fresh_atm)

inductive
typing :: "(name×ty) list⇒lam⇒ty⇒bool" ("_ ⊢ _ : _" [60,60,60] 60)
where
t1[intro]: "⟦valid Γ; (a,τ)∈set Γ⟧ ⟹ Γ ⊢ Var a : τ"
| t2[intro]: "⟦Γ ⊢ t1 : τ→σ; Γ ⊢ t2 : τ⟧ ⟹ Γ ⊢ App t1 t2 : σ"
| t3[intro]: "⟦a♯Γ;((a,τ)#Γ) ⊢ t : σ⟧ ⟹ Γ ⊢ Lam [a].t : τ→σ"

equivariance typing

nominal_inductive typing

definition "NORMAL" :: "lam ⇒ bool" where
"NORMAL t ≡ ¬(∃t'. t⟶⇩β t')"

lemma NORMAL_Var:
shows "NORMAL (Var a)"
proof -
{ assume "∃t'. (Var a) ⟶⇩β t'"
then obtain t' where "(Var a) ⟶⇩β t'" by blast
hence False by (cases) (auto)
}
thus "NORMAL (Var a)" by (auto simp add: NORMAL_def)
qed

text ‹Inductive version of Strong Normalisation›
inductive
SN :: "lam ⇒ bool"
where
SN_intro: "(⋀t'. t ⟶⇩β t' ⟹ SN t') ⟹ SN t"

lemma SN_preserved:
assumes a: "SN t1" "t1⟶⇩β t2"
shows "SN t2"
using a
by (cases) (auto)

lemma double_SN_aux:
assumes a: "SN a"
and b: "SN b"
and hyp: "⋀x z.
⟦⋀y. x ⟶⇩β y ⟹ SN y; ⋀y. x ⟶⇩β y ⟹ P y z;
⋀u. z ⟶⇩β u ⟹ SN u; ⋀u. z ⟶⇩β u ⟹ P x u⟧ ⟹ P x z"
shows "P a b"
proof -
from a
have r: "⋀b. SN b ⟹ P a b"
proof (induct a rule: SN.SN.induct)
case (SN_intro x)
note SNI' = SN_intro
have "SN b" by fact
thus ?case
proof (induct b rule: SN.SN.induct)
case (SN_intro y)
show ?case
apply (rule hyp)
apply (erule SNI')
apply (erule SNI')
apply (rule SN.SN_intro)
apply (erule SN_intro)+
done
qed
qed
from b show ?thesis by (rule r)
qed

lemma double_SN[consumes 2]:
assumes a: "SN a"
and     b: "SN b"
and     c: "⋀x z. ⟦⋀y. x ⟶⇩β y ⟹ P y z; ⋀u. z ⟶⇩β u ⟹ P x u⟧ ⟹ P x z"
shows "P a b"
using a b c
apply(rule_tac double_SN_aux)
apply(assumption)+
apply(blast)
done

section ‹Candidates›

nominal_primrec
RED :: "ty ⇒ lam set"
where
"RED (TVar X) = {t. SN(t)}"
| "RED (τ→σ) =   {t. ∀u. (u∈RED τ ⟶ (App t u)∈RED σ)}"
by (rule TrueI)+

text ‹neutral terms›
definition NEUT :: "lam ⇒ bool" where
"NEUT t ≡ (∃a. t = Var a) ∨ (∃t1 t2. t = App t1 t2)"

(* a slight hack to get the first element of applications *)
(* this is needed to get (SN t) from SN (App t s)         *)
inductive
FST :: "lam⇒lam⇒bool" (" _ » _" [80,80] 80)
where
fst[intro!]:  "(App t s) » t"

nominal_primrec
fst_app_aux::"lam⇒lam option"
where
"fst_app_aux (Var a)     = None"
| "fst_app_aux (App t1 t2) = Some t1"
| "fst_app_aux (Lam [x].t) = None"
apply(finite_guess)+
apply(rule TrueI)+
apply(fresh_guess)+
done

definition
fst_app_def[simp]: "fst_app t = the (fst_app_aux t)"

lemma SN_of_FST_of_App:
assumes a: "SN (App t s)"
shows "SN (fst_app (App t s))"
using a
proof -
from a have "∀z. (App t s » z) ⟶ SN z"
by (induct rule: SN.SN.induct)
(blast elim: FST.cases intro: SN_intro)
then have "SN t" by blast
then show "SN (fst_app (App t s))" by simp
qed

section ‹Candidates›

definition "CR1" :: "ty ⇒ bool" where
"CR1 τ ≡ ∀t. (t∈RED τ ⟶ SN t)"

definition "CR2" :: "ty ⇒ bool" where
"CR2 τ ≡ ∀t t'. (t∈RED τ ∧ t ⟶⇩β t') ⟶ t'∈RED τ"

definition "CR3_RED" :: "lam ⇒ ty ⇒ bool" where
"CR3_RED t τ ≡ ∀t'. t⟶⇩β t' ⟶  t'∈RED τ"

definition "CR3" :: "ty ⇒ bool" where
"CR3 τ ≡ ∀t. (NEUT t ∧ CR3_RED t τ) ⟶ t∈RED τ"

definition "CR4" :: "ty ⇒ bool" where
"CR4 τ ≡ ∀t. (NEUT t ∧ NORMAL t) ⟶t∈RED τ"

lemma CR3_implies_CR4:
assumes a: "CR3 τ"
shows "CR4 τ"
using a by (auto simp add: CR3_def CR3_RED_def CR4_def NORMAL_def)

(* sub_induction in the arrow-type case for the next proof *)
lemma sub_induction:
assumes a: "SN(u)"
and     b: "u∈RED τ"
and     c1: "NEUT t"
and     c2: "CR2 τ"
and     c3: "CR3 σ"
and     c4: "CR3_RED t (τ→σ)"
shows "(App t u)∈RED σ"
using a b
proof (induct)
fix u
assume as: "u∈RED τ"
assume ih: " ⋀u'. ⟦u ⟶⇩β u'; u' ∈ RED τ⟧ ⟹ App t u' ∈ RED σ"
have "NEUT (App t u)" using c1 by (auto simp add: NEUT_def)
moreover
have "CR3_RED (App t u) σ" unfolding CR3_RED_def
proof (intro strip)
fix r
assume red: "App t u ⟶⇩β r"
moreover
{ assume "∃t'. t ⟶⇩β t' ∧ r = App t' u"
then obtain t' where a1: "t ⟶⇩β t'" and a2: "r = App t' u" by blast
have "t'∈RED (τ→σ)" using c4 a1 by (simp add: CR3_RED_def)
then have "App t' u∈RED σ" using as by simp
then have "r∈RED σ" using a2 by simp
}
moreover
{ assume "∃u'. u ⟶⇩β u' ∧ r = App t u'"
then obtain u' where b1: "u ⟶⇩β u'" and b2: "r = App t u'" by blast
have "u'∈RED τ" using as b1 c2 by (auto simp add: CR2_def)
with ih have "App t u' ∈ RED σ" using b1 by simp
then have "r∈RED σ" using b2 by simp
}
moreover
{ assume "∃x t'. t = Lam [x].t'"
then obtain x t' where "t = Lam [x].t'" by blast
then have "NEUT (Lam [x].t')" using c1 by simp
then have "False" by (simp add: NEUT_def)
then have "r∈RED σ" by simp
}
ultimately show "r ∈ RED σ" by (cases) (auto simp add: lam.inject)
qed
ultimately show "App t u ∈ RED σ" using c3 by (simp add: CR3_def)
qed

lemma RED_props:
shows "CR1 τ" and "CR2 τ" and "CR3 τ"
proof (nominal_induct τ rule: ty.strong_induct)
case (TVar a)
{ case 1 show "CR1 (TVar a)" by (simp add: CR1_def)
next
case 2 show "CR2 (TVar a)" by (auto intro: SN_preserved simp add: CR2_def)
next
case 3 show "CR3 (TVar a)" by (auto intro: SN_intro simp add: CR3_def CR3_RED_def)
}
next
case (TArr τ1 τ2)
{ case 1
have ih_CR3_τ1: "CR3 τ1" by fact
have ih_CR1_τ2: "CR1 τ2" by fact
have "⋀t. t ∈ RED (τ1 → τ2) ⟹ SN t"
proof -
fix t
assume "t ∈ RED (τ1 → τ2)"
then have a: "∀u. u ∈ RED τ1 ⟶ App t u ∈ RED τ2" by simp
from ih_CR3_τ1 have "CR4 τ1" by (simp add: CR3_implies_CR4)
moreover
fix a have "NEUT (Var a)" by (force simp add: NEUT_def)
moreover
have "NORMAL (Var a)" by (rule NORMAL_Var)
ultimately have "(Var a)∈ RED τ1" by (simp add: CR4_def)
with a have "App t (Var a) ∈ RED τ2" by simp
hence "SN (App t (Var a))" using ih_CR1_τ2 by (simp add: CR1_def)
thus "SN t" by (auto dest: SN_of_FST_of_App)
qed
then show "CR1 (τ1 → τ2)" unfolding CR1_def by simp
next
case 2
have ih_CR2_τ2: "CR2 τ2" by fact
then show "CR2 (τ1 → τ2)" unfolding CR2_def by auto
next
case 3
have ih_CR1_τ1: "CR1 τ1" by fact
have ih_CR2_τ1: "CR2 τ1" by fact
have ih_CR3_τ2: "CR3 τ2" by fact
show "CR3 (τ1 → τ2)" unfolding CR3_def
proof (simp, intro strip)
fix t u
assume a1: "u ∈ RED τ1"
assume a2: "NEUT t ∧ CR3_RED t (τ1 → τ2)"
have "SN(u)" using a1 ih_CR1_τ1 by (simp add: CR1_def)
then show "(App t u)∈RED τ2" using ih_CR2_τ1 ih_CR3_τ2 a1 a2 by (blast intro: sub_induction)
qed
}
qed

text ‹
the next lemma not as simple as on paper, probably because of
the stronger double_SN induction
›
lemma abs_RED:
assumes asm: "∀s∈RED τ. t[x::=s]∈RED σ"
shows "Lam [x].t∈RED (τ→σ)"
proof -
have b1: "SN t"
proof -
have "Var x∈RED τ"
proof -
have "CR4 τ" by (simp add: RED_props CR3_implies_CR4)
moreover
have "NEUT (Var x)" by (auto simp add: NEUT_def)
moreover
have "NORMAL (Var x)" by (auto elim: Beta.cases simp add: NORMAL_def)
ultimately show "Var x∈RED τ" by (simp add: CR4_def)
qed
then have "t[x::=Var x]∈RED σ" using asm by simp
then have "t∈RED σ" by (simp add: id_subs)
moreover
have "CR1 σ" by (simp add: RED_props)
ultimately show "SN t" by (simp add: CR1_def)
qed
show "Lam [x].t∈RED (τ→σ)"
proof (simp, intro strip)
fix u
assume b2: "u∈RED τ"
then have b3: "SN u" using RED_props by (auto simp add: CR1_def)
show "App (Lam [x].t) u ∈ RED σ" using b1 b3 b2 asm
proof(induct t u rule: double_SN)
fix t u
assume ih1: "⋀t'.  ⟦t ⟶⇩β t'; u∈RED τ; ∀s∈RED τ. t'[x::=s]∈RED σ⟧ ⟹ App (Lam [x].t') u ∈ RED σ"
assume ih2: "⋀u'.  ⟦u ⟶⇩β u'; u'∈RED τ; ∀s∈RED τ. t[x::=s]∈RED σ⟧ ⟹ App (Lam [x].t) u' ∈ RED σ"
assume as1: "u ∈ RED τ"
assume as2: "∀s∈RED τ. t[x::=s]∈RED σ"
have "CR3_RED (App (Lam [x].t) u) σ" unfolding CR3_RED_def
proof(intro strip)
fix r
assume red: "App (Lam [x].t) u ⟶⇩β r"
moreover
{ assume "∃t'. t ⟶⇩β t' ∧ r = App (Lam [x].t') u"
then obtain t' where a1: "t ⟶⇩β t'" and a2: "r = App (Lam [x].t') u" by blast
have "App (Lam [x].t') u∈RED σ" using ih1 a1 as1 as2
apply(auto)
apply(drule_tac x="t'" in meta_spec)
apply(simp)
apply(drule meta_mp)
prefer 2
apply(auto)[1]
apply(rule ballI)
apply(drule_tac x="s" in bspec)
apply(simp)
apply(subgoal_tac "CR2 σ")(*A*)
apply(unfold CR2_def)[1]
apply(drule_tac x="t[x::=s]" in spec)
apply(drule_tac x="t'[x::=s]" in spec)
(*A*)
done
then have "r∈RED σ" using a2 by simp
}
moreover
{ assume "∃u'. u ⟶⇩β u' ∧ r = App (Lam [x].t) u'"
then obtain u' where b1: "u ⟶⇩β u'" and b2: "r = App (Lam [x].t) u'" by blast
have "App (Lam [x].t) u'∈RED σ" using ih2 b1 as1 as2
apply(auto)
apply(drule_tac x="u'" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(subgoal_tac "CR2 τ")
apply(unfold CR2_def)[1]
apply(drule_tac x="u" in spec)
apply(drule_tac x="u'" in spec)
apply(simp)
apply(simp)
done
then have "r∈RED σ" using b2 by simp
}
moreover
{ assume "r = t[x::=u]"
then have "r∈RED σ" using as1 as2 by auto
}
ultimately show "r ∈ RED σ"
(* one wants to use the strong elimination principle; for this one
has to know that x♯u *)
apply(cases)
apply(drule beta_abs)
apply(auto)[1]
done
qed
moreover
have "NEUT (App (Lam [x].t) u)" unfolding NEUT_def by (auto)
ultimately show "App (Lam [x].t) u ∈ RED σ"  using RED_props by (simp add: CR3_def)
qed
qed
qed

abbreviation
mapsto :: "(name×lam) list ⇒ name ⇒ lam ⇒ bool" ("_ maps _ to _" [55,55,55] 55)
where
"θ maps x to e ≡ (lookup θ x) = e"

abbreviation
closes :: "(name×lam) list ⇒ (name×ty) list ⇒ bool" ("_ closes _" [55,55] 55)
where
"θ closes Γ ≡ ∀x T. ((x,T) ∈ set Γ ⟶ (∃t. θ maps x to t ∧ t ∈ RED T))"

lemma all_RED:
assumes a: "Γ ⊢ t : τ"
and     b: "θ closes Γ"
shows "θ<t> ∈ RED τ"
using a b
proof(nominal_induct  avoiding: θ rule: typing.strong_induct)
case (t3 a Γ σ t τ θ) ― ‹lambda case›
have ih: "⋀θ. θ closes ((a,σ)#Γ) ⟹ θ<t> ∈ RED τ" by fact
have θ_cond: "θ closes Γ" by fact
have fresh: "a♯Γ" "a♯θ" by fact+
from ih have "∀s∈RED σ. ((a,s)#θ)<t> ∈ RED τ" using fresh θ_cond fresh_context by simp
then have "∀s∈RED σ. θ<t>[a::=s] ∈ RED τ" using fresh by (simp add: psubst_subst)
then have "Lam [a].(θ<t>) ∈ RED (σ → τ)" by (simp only: abs_RED)
then show "θ<(Lam [a].t)> ∈ RED (σ → τ)" using fresh by simp
qed auto

section ‹identity substitution generated from a context Γ›
fun
"id" :: "(name×ty) list ⇒ (name×lam) list"
where
"id []    = []"
| "id ((x,τ)#Γ) = (x,Var x)#(id Γ)"

lemma id_maps:
shows "(id Γ) maps a to (Var a)"
by (induct Γ) (auto)

lemma id_fresh:
fixes a::"name"
assumes a: "a♯Γ"
shows "a♯(id Γ)"
using a
by (induct Γ)

lemma id_apply:
shows "(id Γ)<t> = t"
by (nominal_induct t avoiding: Γ rule: lam.strong_induct)

lemma id_closes:
shows "(id Γ) closes Γ"
apply(auto)
apply(subgoal_tac "CR3 T") ― ‹A›
apply(drule CR3_implies_CR4)
apply(drule_tac x="Var x" in spec)
― ‹A›
apply(rule RED_props)
done

lemma typing_implies_RED:
assumes a: "Γ ⊢ t : τ"
shows "t ∈ RED τ"
proof -
have "(id Γ)<t>∈RED τ"
proof -
have "(id Γ) closes Γ" by (rule id_closes)
with a show ?thesis by (rule all_RED)
qed
thus"t ∈ RED τ" by (simp add: id_apply)
qed

lemma typing_implies_SN:
assumes a: "Γ ⊢ t : τ"
shows "SN(t)"
proof -
from a have "t ∈ RED τ" by (rule typing_implies_RED)
moreover
have "CR1 τ" by (rule RED_props)
ultimately show "SN(t)" by (simp add: CR1_def)
qed

end
```