Quelle  Lambda.thy

(*  Title:      HOL/Proofs/Lambda/Lambda.thy
  Author: Tobias Nipkow
  Copyright 1995 TU Muenchen
*)

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 🍋‹subst› and 🍋‹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]
  🍋 ‹don't add ‹r_into_rtrancl[intro!]›\

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"
  by (simp add: subst_Var)

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

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

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]"
proof (induct set: rtranclp)
  case base
  then show ?case
    by (iprover intro: rtrancl_refl)
next
  case (step y z)
  then show ?case
    by (iprover intro: rtranclp.simps subst_preserves_beta)
qed

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"
proof (induct set: rtranclp)
  case base
  then show ?case
    by (iprover intro: rtrancl_refl)
next
  case (step y z)
  then show ?case
    by (iprover intro: lift_preserves_beta rtranclp.simps)
qed

theorem subst_preserves_beta2 [simp]: "r →🪙β s ==> t[r/i] →🪙β🪙* t[s/i]"
proof (induct t arbitrary: r s i)
  case (Var x)
  then show ?case
    by (simp add: subst_Var r_into_rtranclp)
next
  case (App t1 t2)
  then show ?case 
    by (simp add: rtrancl_beta_App)
next
  case (Abs t)
  then show ?case by (simp add: rtrancl_beta_Abs)
qed


theorem subst_preserves_beta2': "r →🪙β🪙* s ==> t[r/i] →🪙β🪙* t[s/i]"
proof (induct set: rtranclp)
  case base
  then show ?case by (iprover intro: rtrancl_refl)
next
  case (step y z)
  then show ?case
    by (iprover intro: rtranclp_trans subst_preserves_beta2)
qed

end