# Theory WeakNorm

theory WeakNorm
imports LambdaType NormalForm Old_Datatype Code_Target_Int
(*  Title:      HOL/Proofs/Lambda/WeakNorm.thy
Author:     Stefan Berghofer
*)

section ‹Weak normalization for simply-typed lambda calculus›

theory WeakNorm
imports LambdaType NormalForm "HOL-Library.Old_Datatype" "HOL-Library.Code_Target_Int"
begin

text ‹
Formalization by Stefan Berghofer. Partly based on a paper proof by
Felix Joachimski and Ralph Matthes @{cite "Matthes-Joachimski-AML"}.
›

subsection ‹Main theorems›

lemma norm_list:
assumes f_compat: "⋀t t'. t →⇩β⇧* t' ⟹ f t →⇩β⇧* f t'"
and f_NF: "⋀t. NF t ⟹ NF (f t)"
and uNF: "NF u" and uT: "e ⊢ u : T"
shows "⋀Us. e⟨i:T⟩ ⊩ as : Us ⟹
listall (λt. ∀e T' u i. e⟨i:T⟩ ⊢ t : T' ⟶
NF u ⟶ e ⊢ u : T ⟶ (∃t'. t[u/i] →⇩β⇧* t' ∧ NF t')) as ⟹
∃as'. ∀j. Var j °° map (λt. f (t[u/i])) as →⇩β⇧*
Var j °° map f as' ∧ NF (Var j °° map f as')"
(is "⋀Us. _ ⟹ listall ?R as ⟹ ∃as'. ?ex Us as as'")
proof (induct as rule: rev_induct)
case (Nil Us)
with Var_NF have "?ex Us [] []" by simp
thus ?case ..
next
case (snoc b bs Us)
have "e⟨i:T⟩ ⊩ bs  @ [b] : Us" by fact
then obtain Vs W where Us: "Us = Vs @ [W]"
and bs: "e⟨i:T⟩ ⊩ bs : Vs" and bT: "e⟨i:T⟩ ⊢ b : W"
by (rule types_snocE)
from snoc have "listall ?R bs" by simp
with bs have "∃bs'. ?ex Vs bs bs'" by (rule snoc)
then obtain bs' where bsred: "Var j °° map (λt. f (t[u/i])) bs →⇩β⇧* Var j °° map f bs'"
and bsNF: "NF (Var j °° map f bs')" for j
by iprover
from snoc have "?R b" by simp
with bT and uNF and uT have "∃b'. b[u/i] →⇩β⇧* b' ∧ NF b'"
by iprover
then obtain b' where bred: "b[u/i] →⇩β⇧* b'" and bNF: "NF b'"
by iprover
from bsNF [of 0] have "listall NF (map f bs')"
by (rule App_NF_D)
moreover have "NF (f b')" using bNF by (rule f_NF)
ultimately have "listall NF (map f (bs' @ [b']))"
by simp
hence "⋀j. NF (Var j °° map f (bs' @ [b']))" by (rule NF.App)
moreover from bred have "f (b[u/i]) →⇩β⇧* f b'"
by (rule f_compat)
with bsred have
"⋀j. (Var j °° map (λt. f (t[u/i])) bs) ° f (b[u/i]) →⇩β⇧*
(Var j °° map f bs') ° f b'" by (rule rtrancl_beta_App)
ultimately have "?ex Us (bs @ [b]) (bs' @ [b'])" by simp
thus ?case ..
qed

lemma subst_type_NF:
"⋀t e T u i. NF t ⟹ e⟨i:U⟩ ⊢ t : T ⟹ NF u ⟹ e ⊢ u : U ⟹ ∃t'. t[u/i] →⇩β⇧* t' ∧ NF t'"
(is "PROP ?P U" is "⋀t e T u i. _ ⟹ PROP ?Q t e T u i U")
proof (induct U)
fix T t
let ?R = "λt. ∀e T' u i.
e⟨i:T⟩ ⊢ t : T' ⟶ NF u ⟶ e ⊢ u : T ⟶ (∃t'. t[u/i] →⇩β⇧* t' ∧ NF t')"
assume MI1: "⋀T1 T2. T = T1 ⇒ T2 ⟹ PROP ?P T1"
assume MI2: "⋀T1 T2. T = T1 ⇒ T2 ⟹ PROP ?P T2"
assume "NF t"
thus "⋀e T' u i. PROP ?Q t e T' u i T"
proof induct
fix e T' u i assume uNF: "NF u" and uT: "e ⊢ u : T"
{
case (App ts x e1 T'1 u1 i1)
assume "e⟨i:T⟩ ⊢ Var x °° ts : T'"
then obtain Us
where varT: "e⟨i:T⟩ ⊢ Var x : Us ⇛ T'"
and argsT: "e⟨i:T⟩ ⊩ ts : Us"
by (rule var_app_typesE)
from nat_eq_dec show "∃t'. (Var x °° ts)[u/i] →⇩β⇧* t' ∧ NF t'"
proof
assume eq: "x = i"
show ?thesis
proof (cases ts)
case Nil
with eq have "(Var x °° [])[u/i] →⇩β⇧* u" by simp
with Nil and uNF show ?thesis by simp iprover
next
case (Cons a as)
with argsT obtain T'' Ts where Us: "Us = T'' # Ts"
by (cases Us) (rule FalseE, simp)
from varT and Us have varT: "e⟨i:T⟩ ⊢ Var x : T'' ⇒ Ts ⇛ T'"
by simp
from varT eq have T: "T = T'' ⇒ Ts ⇛ T'" by cases auto
with uT have uT': "e ⊢ u : T'' ⇒ Ts ⇛ T'" by simp
from argsT Us Cons have argsT': "e⟨i:T⟩ ⊩ as : Ts" by simp
from argsT Us Cons have argT: "e⟨i:T⟩ ⊢ a : T''" by simp
from argT uT refl have aT: "e ⊢ a[u/i] : T''" by (rule subst_lemma)
from App and Cons have "listall ?R as" by simp (iprover dest: listall_conj2)
with lift_preserves_beta' lift_NF uNF uT argsT'
have "∃as'. ∀j. Var j °° map (λt. lift (t[u/i]) 0) as →⇩β⇧*
Var j °° map (λt. lift t 0) as' ∧
NF (Var j °° map (λt. lift t 0) as')" by (rule norm_list)
then obtain as' where
asred: "Var 0 °° map (λt. lift (t[u/i]) 0) as →⇩β⇧*
Var 0 °° map (λt. lift t 0) as'"
and asNF: "NF (Var 0 °° map (λt. lift t 0) as')" by iprover
from App and Cons have "?R a" by simp
with argT and uNF and uT have "∃a'. a[u/i] →⇩β⇧* a' ∧ NF a'"
by iprover
then obtain a' where ared: "a[u/i] →⇩β⇧* a'" and aNF: "NF a'" by iprover
from uNF have "NF (lift u 0)" by (rule lift_NF)
hence "∃u'. lift u 0 ° Var 0 →⇩β⇧* u' ∧ NF u'" by (rule app_Var_NF)
then obtain u' where ured: "lift u 0 ° Var 0 →⇩β⇧* u'" and u'NF: "NF u'"
by iprover
from T and u'NF have "∃ua. u'[a'/0] →⇩β⇧* ua ∧ NF ua"
proof (rule MI1)
have "e⟨0:T''⟩ ⊢ lift u 0 ° Var 0 : Ts ⇛ T'"
proof (rule typing.App)
from uT' show "e⟨0:T''⟩ ⊢ lift u 0 : T'' ⇒ Ts ⇛ T'" by (rule lift_type)
show "e⟨0:T''⟩ ⊢ Var 0 : T''" by (rule typing.Var) simp
qed
with ured show "e⟨0:T''⟩ ⊢ u' : Ts ⇛ T'" by (rule subject_reduction')
from ared aT show "e ⊢ a' : T''" by (rule subject_reduction')
show "NF a'" by fact
qed
then obtain ua where uared: "u'[a'/0] →⇩β⇧* ua" and uaNF: "NF ua"
by iprover
from ared have "(lift u 0 ° Var 0)[a[u/i]/0] →⇩β⇧* (lift u 0 ° Var 0)[a'/0]"
by (rule subst_preserves_beta2')
also from ured have "(lift u 0 ° Var 0)[a'/0] →⇩β⇧* u'[a'/0]"
by (rule subst_preserves_beta')
also note uared
finally have "(lift u 0 ° Var 0)[a[u/i]/0] →⇩β⇧* ua" .
hence uared': "u ° a[u/i] →⇩β⇧* ua" by simp
from T asNF _ uaNF have "∃r. (Var 0 °° map (λt. lift t 0) as')[ua/0] →⇩β⇧* r ∧ NF r"
proof (rule MI2)
have "e⟨0:Ts ⇛ T'⟩ ⊢ Var 0 °° map (λt. lift (t[u/i]) 0) as : T'"
proof (rule list_app_typeI)
show "e⟨0:Ts ⇛ T'⟩ ⊢ Var 0 : Ts ⇛ T'" by (rule typing.Var) simp
from uT argsT' have "e ⊩ map (λt. t[u/i]) as : Ts"
by (rule substs_lemma)
hence "e⟨0:Ts ⇛ T'⟩ ⊩ map (λt. lift t 0) (map (λt. t[u/i]) as) : Ts"
by (rule lift_types)
thus "e⟨0:Ts ⇛ T'⟩ ⊩ map (λt. lift (t[u/i]) 0) as : Ts"
qed
with asred show "e⟨0:Ts ⇛ T'⟩ ⊢ Var 0 °° map (λt. lift t 0) as' : T'"
by (rule subject_reduction')
from argT uT refl have "e ⊢ a[u/i] : T''" by (rule subst_lemma)
with uT' have "e ⊢ u ° a[u/i] : Ts ⇛ T'" by (rule typing.App)
with uared' show "e ⊢ ua : Ts ⇛ T'" by (rule subject_reduction')
qed
then obtain r where rred: "(Var 0 °° map (λt. lift t 0) as')[ua/0] →⇩β⇧* r"
and rnf: "NF r" by iprover
from asred have
"(Var 0 °° map (λt. lift (t[u/i]) 0) as)[u ° a[u/i]/0] →⇩β⇧*
(Var 0 °° map (λt. lift t 0) as')[u ° a[u/i]/0]"
by (rule subst_preserves_beta')
also from uared' have "(Var 0 °° map (λt. lift t 0) as')[u ° a[u/i]/0] →⇩β⇧*
(Var 0 °° map (λt. lift t 0) as')[ua/0]" by (rule subst_preserves_beta2')
also note rred
finally have "(Var 0 °° map (λt. lift (t[u/i]) 0) as)[u ° a[u/i]/0] →⇩β⇧* r" .
with rnf Cons eq show ?thesis
qed
next
assume neq: "x ≠ i"
from App have "listall ?R ts" by (iprover dest: listall_conj2)
with uNF uT argsT
have "∃ts'. ∀j. Var j °° map (λt. t[u/i]) ts →⇩β⇧* Var j °° ts' ∧
NF (Var j °° ts')" (is "∃ts'. ?ex ts'")
by (rule norm_list [of "λt. t", simplified])
then obtain ts' where NF: "?ex ts'" ..
from nat_le_dec show ?thesis
proof
assume "i < x"
with NF show ?thesis by simp iprover
next
assume "¬ (i < x)"
with NF neq show ?thesis by (simp add: subst_Var) iprover
qed
qed
next
case (Abs r e1 T'1 u1 i1)
assume absT: "e⟨i:T⟩ ⊢ Abs r : T'"
then obtain R S where "e⟨0:R⟩⟨Suc i:T⟩  ⊢ r : S" by (rule abs_typeE) simp
moreover have "NF (lift u 0)" using ‹NF u› by (rule lift_NF)
moreover have "e⟨0:R⟩ ⊢ lift u 0 : T" using uT by (rule lift_type)
ultimately have "∃t'. r[lift u 0/Suc i] →⇩β⇧* t' ∧ NF t'" by (rule Abs)
thus "∃t'. Abs r[u/i] →⇩β⇧* t' ∧ NF t'"
by simp (iprover intro: rtrancl_beta_Abs NF.Abs)
}
qed
qed

― ‹A computationally relevant copy of @{term "e ⊢ t : T"}›
inductive rtyping :: "(nat ⇒ type) ⇒ dB ⇒ type ⇒ bool"  ("_ ⊢⇩R _ : _" [50, 50, 50] 50)
where
Var: "e x = T ⟹ e ⊢⇩R Var x : T"
| Abs: "e⟨0:T⟩ ⊢⇩R t : U ⟹ e ⊢⇩R Abs t : (T ⇒ U)"
| App: "e ⊢⇩R s : T ⇒ U ⟹ e ⊢⇩R t : T ⟹ e ⊢⇩R (s ° t) : U"

lemma rtyping_imp_typing: "e ⊢⇩R t : T ⟹ e ⊢ t : T"
apply (induct set: rtyping)
apply (erule typing.Var)
apply (erule typing.Abs)
apply (erule typing.App)
apply assumption
done

theorem type_NF:
assumes "e ⊢⇩R t : T"
shows "∃t'. t →⇩β⇧* t' ∧ NF t'" using assms
proof induct
case Var
show ?case by (iprover intro: Var_NF)
next
case Abs
thus ?case by (iprover intro: rtrancl_beta_Abs NF.Abs)
next
case (App e s T U t)
from App obtain s' t' where
sred: "s →⇩β⇧* s'" and "NF s'"
and tred: "t →⇩β⇧* t'" and tNF: "NF t'" by iprover
have "∃u. (Var 0 ° lift t' 0)[s'/0] →⇩β⇧* u ∧ NF u"
proof (rule subst_type_NF)
have "NF (lift t' 0)" using tNF by (rule lift_NF)
hence "listall NF [lift t' 0]" by (rule listall_cons) (rule listall_nil)
hence "NF (Var 0 °° [lift t' 0])" by (rule NF.App)
thus "NF (Var 0 ° lift t' 0)" by simp
show "e⟨0:T ⇒ U⟩ ⊢ Var 0 ° lift t' 0 : U"
proof (rule typing.App)
show "e⟨0:T ⇒ U⟩ ⊢ Var 0 : T ⇒ U"
by (rule typing.Var) simp
from tred have "e ⊢ t' : T"
by (rule subject_reduction') (rule rtyping_imp_typing, rule App.hyps)
thus "e⟨0:T ⇒ U⟩ ⊢ lift t' 0 : T"
by (rule lift_type)
qed
from sred show "e ⊢ s' : T ⇒ U"
by (rule subject_reduction') (rule rtyping_imp_typing, rule App.hyps)
show "NF s'" by fact
qed
then obtain u where ured: "s' ° t' →⇩β⇧* u" and unf: "NF u" by simp iprover
from sred tred have "s ° t →⇩β⇧* s' ° t'" by (rule rtrancl_beta_App)
hence "s ° t →⇩β⇧* u" using ured by (rule rtranclp_trans)
with unf show ?case by iprover
qed

subsection ‹Extracting the program›

declare NF.induct [ind_realizer]
declare rtranclp.induct [ind_realizer irrelevant]
declare rtyping.induct [ind_realizer]
lemmas [extraction_expand] = conj_assoc listall_cons_eq

extract type_NF

lemma rtranclR_rtrancl_eq: "rtranclpR r a b = r⇧*⇧* a b"
apply (rule iffI)
apply (erule rtranclpR.induct)
apply (rule rtranclp.rtrancl_refl)
apply (erule rtranclp.rtrancl_into_rtrancl)
apply assumption
apply (erule rtranclp.induct)
apply (rule rtranclpR.rtrancl_refl)
apply (erule rtranclpR.rtrancl_into_rtrancl)
apply assumption
done

lemma NFR_imp_NF: "NFR nf t ⟹ NF t"
apply (erule NFR.induct)
apply (rule NF.intros)
apply (erule NF.intros)
done

text_raw ‹
\begin{figure}
\renewcommand{\isastyle}{\scriptsize\it}%
@{thm [display,eta_contract=false,margin=100] subst_type_NF_def}
\renewcommand{\isastyle}{\small\it}%
\caption{Program extracted from ‹subst_type_NF›}
\label{fig:extr-subst-type-nf}
\end{figure}

\begin{figure}
\renewcommand{\isastyle}{\scriptsize\it}%
@{thm [display,margin=100] subst_Var_NF_def}
@{thm [display,margin=100] app_Var_NF_def}
@{thm [display,margin=100] lift_NF_def}
@{thm [display,eta_contract=false,margin=100] type_NF_def}
\renewcommand{\isastyle}{\small\it}%
\caption{Program extracted from lemmas and main theorem}
\label{fig:extr-type-nf}
\end{figure}
›

text ‹
The program corresponding to the proof of the central lemma, which
performs substitution and normalization, is shown in Figure
\ref{fig:extr-subst-type-nf}. The correctness
theorem corresponding to the program ‹subst_type_NF› is
@{thm [display,margin=100] subst_type_NF_correctness
[simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]}
where ‹NFR› is the realizability predicate corresponding to
the datatype ‹NFT›, which is inductively defined by the rules
\pagebreak
@{thm [display,margin=90] NFR.App [of ts nfs x] NFR.Abs [of nf t]}

The programs corresponding to the main theorem ‹type_NF›, as
well as to some lemmas, are shown in Figure \ref{fig:extr-type-nf}.
The correctness statement for the main function ‹type_NF› is
@{thm [display,margin=100] type_NF_correctness
[simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]}
where the realizability predicate ‹rtypingR› corresponding to the
computationally relevant version of the typing judgement is inductively
defined by the rules
@{thm [display,margin=100] rtypingR.Var [no_vars]
rtypingR.Abs [of ty, no_vars] rtypingR.App [of ty e s T U ty' t]}
›

subsection ‹Generating executable code›

instantiation NFT :: default
begin

definition "default = Dummy ()"

instance ..

end

instantiation dB :: default
begin

definition "default = dB.Var 0"

instance ..

end

instantiation prod :: (default, default) default
begin

definition "default = (default, default)"

instance ..

end

instantiation list :: (type) default
begin

definition "default = []"

instance ..

end

instantiation "fun" :: (type, default) default
begin

definition "default = (λx. default)"

instance ..

end

definition int_of_nat :: "nat ⇒ int" where
"int_of_nat = of_nat"

text ‹
The following functions convert between Isabelle's built-in {\tt term}
datatype and the generated {\tt dB} datatype. This allows to
generate example terms using Isabelle's parser and inspect
normalized terms using Isabelle's pretty printer.
›

ML ‹
val nat_of_integer = @{code nat} o @{code int_of_integer};

fun dBtype_of_typ (Type ("fun", [T, U])) =
@{code Fun} (dBtype_of_typ T, dBtype_of_typ U)
| dBtype_of_typ (TFree (s, _)) = (case raw_explode s of
["'", a] => @{code Atom} (nat_of_integer (ord a - 97))
| _ => error "dBtype_of_typ: variable name")
| dBtype_of_typ _ = error "dBtype_of_typ: bad type";

fun dB_of_term (Bound i) = @{code dB.Var} (nat_of_integer i)
| dB_of_term (t $u) = @{code dB.App} (dB_of_term t, dB_of_term u) | dB_of_term (Abs (_, _, t)) = @{code dB.Abs} (dB_of_term t) | dB_of_term _ = error "dB_of_term: bad term"; fun term_of_dB Ts (Type ("fun", [T, U])) (@{code dB.Abs} dBt) = Abs ("x", T, term_of_dB (T :: Ts) U dBt) | term_of_dB Ts _ dBt = term_of_dB' Ts dBt and term_of_dB' Ts (@{code dB.Var} n) = Bound (@{code integer_of_nat} n) | term_of_dB' Ts (@{code dB.App} (dBt, dBu)) = let val t = term_of_dB' Ts dBt in case fastype_of1 (Ts, t) of Type ("fun", [T, _]) => t$ term_of_dB Ts T dBu
| _ => error "term_of_dB: function type expected"
end
| term_of_dB' _ _ = error "term_of_dB: term not in normal form";

fun typing_of_term Ts e (Bound i) =
@{code Var} (e, nat_of_integer i, dBtype_of_typ (nth Ts i))
| typing_of_term Ts e (t \$ u) = (case fastype_of1 (Ts, t) of
Type ("fun", [T, U]) => @{code App} (e, dB_of_term t,
dBtype_of_typ T, dBtype_of_typ U, dB_of_term u,
typing_of_term Ts e t, typing_of_term Ts e u)
| _ => error "typing_of_term: function type expected")
| typing_of_term Ts e (Abs (_, T, t)) =
let val dBT = dBtype_of_typ T
in @{code Abs} (e, dBT, dB_of_term t,
dBtype_of_typ (fastype_of1 (T :: Ts, t)),
typing_of_term (T :: Ts) (@{code shift} e @{code "0::nat"} dBT) t)
end
| typing_of_term _ _ _ = error "typing_of_term: bad term";

fun dummyf _ = error "dummy";

val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
val (dB1, _) = @{code type_NF} (typing_of_term [] dummyf (Thm.term_of ct1));
val ct1' = Thm.cterm_of @{context} (term_of_dB [] (Thm.typ_of_cterm ct1) dB1);

val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"};
val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (Thm.term_of ct2));
val ct2' = Thm.cterm_of @{context} (term_of_dB [] (Thm.typ_of_cterm ct2) dB2);
›

end