# Theory Lambda

theory Lambda
imports Main
```(*  Title:      HOL/Proofs/Lambda/Lambda.thy
Author:     Tobias Nipkow
*)

section ‹Basic definitions of Lambda-calculus›

theory Lambda
imports Main
begin

declare [[syntax_ambiguity_warning = false]]

subsection ‹Lambda-terms in de Bruijn notation and substitution›

datatype dB =
Var nat
| App dB dB (infixl "°" 200)
| Abs dB

primrec
lift :: "[dB, nat] => dB"
where
"lift (Var i) k = (if i < k then Var i else Var (i + 1))"
| "lift (s ° t) k = lift s k ° lift t k"
| "lift (Abs s) k = Abs (lift s (k + 1))"

primrec
subst :: "[dB, dB, nat] => dB"  ("_[_'/_]" [300, 0, 0] 300)
where (* FIXME base names *)
subst_Var: "(Var i)[s/k] =
(if k < i then Var (i - 1) else if i = k then s else Var i)"
| subst_App: "(t ° u)[s/k] = t[s/k] ° u[s/k]"
| subst_Abs: "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])"

declare subst_Var [simp del]

text ‹Optimized versions of @{term subst} and @{term lift}.›

primrec
liftn :: "[nat, dB, nat] => dB"
where
"liftn n (Var i) k = (if i < k then Var i else Var (i + n))"
| "liftn n (s ° t) k = liftn n s k ° liftn n t k"
| "liftn n (Abs s) k = Abs (liftn n s (k + 1))"

primrec
substn :: "[dB, dB, nat] => dB"
where
"substn (Var i) s k =
(if k < i then Var (i - 1) else if i = k then liftn k s 0 else Var i)"
| "substn (t ° u) s k = substn t s k ° substn u s k"
| "substn (Abs t) s k = Abs (substn t s (k + 1))"

subsection ‹Beta-reduction›

inductive beta :: "[dB, dB] => bool"  (infixl "→⇩β" 50)
where
beta [simp, intro!]: "Abs s ° t →⇩β s[t/0]"
| appL [simp, intro!]: "s →⇩β t ==> s ° u →⇩β t ° u"
| appR [simp, intro!]: "s →⇩β t ==> u ° s →⇩β u ° t"
| abs [simp, intro!]: "s →⇩β t ==> Abs s →⇩β Abs t"

abbreviation
beta_reds :: "[dB, dB] => bool"  (infixl "→⇩β⇧*" 50) where
"s →⇩β⇧* t == beta⇧*⇧* s t"

inductive_cases beta_cases [elim!]:
"Var i →⇩β t"
"Abs r →⇩β s"
"s ° t →⇩β u"

declare if_not_P [simp] not_less_eq [simp]

subsection ‹Congruence rules›

lemma rtrancl_beta_Abs [intro!]:
"s →⇩β⇧* s' ==> Abs s →⇩β⇧* Abs s'"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma rtrancl_beta_AppL:
"s →⇩β⇧* s' ==> s ° t →⇩β⇧* s' ° t"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma rtrancl_beta_AppR:
"t →⇩β⇧* t' ==> s ° t →⇩β⇧* s ° t'"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma rtrancl_beta_App [intro]:
"[| s →⇩β⇧* s'; t →⇩β⇧* t' |] ==> s ° t →⇩β⇧* s' ° t'"
by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtranclp_trans)

subsection ‹Substitution-lemmas›

lemma subst_eq [simp]: "(Var k)[u/k] = u"

lemma subst_gt [simp]: "i < j ==> (Var j)[u/i] = Var (j - 1)"

lemma subst_lt [simp]: "j < i ==> (Var j)[u/i] = Var j"

lemma lift_lift:
"i < k + 1 ⟹ lift (lift t i) (Suc k) = lift (lift t k) i"
by (induct t arbitrary: i k) auto

lemma lift_subst [simp]:
"j < i + 1 ⟹ lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]"
by (induct t arbitrary: i j s)
(simp_all add: diff_Suc subst_Var lift_lift split: nat.split)

lemma lift_subst_lt:
"i < j + 1 ⟹ lift (t[s/j]) i = (lift t i) [lift s i / j + 1]"
by (induct t arbitrary: i j s) (simp_all add: subst_Var lift_lift)

lemma subst_lift [simp]:
"(lift t k)[s/k] = t"
by (induct t arbitrary: k s) simp_all

lemma subst_subst:
"i < j + 1 ⟹ t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
by (induct t arbitrary: i j u v)
(simp_all add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
split: nat.split)

subsection ‹Equivalence proof for optimized substitution›

lemma liftn_0 [simp]: "liftn 0 t k = t"
by (induct t arbitrary: k) (simp_all add: subst_Var)

lemma liftn_lift [simp]: "liftn (Suc n) t k = lift (liftn n t k) k"
by (induct t arbitrary: k) (simp_all add: subst_Var)

lemma substn_subst_n [simp]: "substn t s n = t[liftn n s 0 / n]"
by (induct t arbitrary: n) (simp_all add: subst_Var)

theorem substn_subst_0: "substn t s 0 = t[s/0]"
by simp

subsection ‹Preservation theorems›

text ‹Not used in Church-Rosser proof, but in Strong
Normalization. \medskip›

theorem subst_preserves_beta [simp]:
"r →⇩β s ==> r[t/i] →⇩β s[t/i]"
by (induct arbitrary: t i set: beta) (simp_all add: subst_subst [symmetric])

theorem subst_preserves_beta': "r →⇩β⇧* s ==> r[t/i] →⇩β⇧* s[t/i]"
apply (induct set: rtranclp)
apply (rule rtranclp.rtrancl_refl)
apply (erule rtranclp.rtrancl_into_rtrancl)
apply (erule subst_preserves_beta)
done

theorem lift_preserves_beta [simp]:
"r →⇩β s ==> lift r i →⇩β lift s i"
by (induct arbitrary: i set: beta) auto

theorem lift_preserves_beta': "r →⇩β⇧* s ==> lift r i →⇩β⇧* lift s i"
apply (induct set: rtranclp)
apply (rule rtranclp.rtrancl_refl)
apply (erule rtranclp.rtrancl_into_rtrancl)
apply (erule lift_preserves_beta)
done

theorem subst_preserves_beta2 [simp]: "r →⇩β s ==> t[r/i] →⇩β⇧* t[s/i]"
apply (induct t arbitrary: r s i)