# Theory Lambda

Up to index of Isabelle/HOL/Lambda

theory Lambda
imports Main
begin

    (*  Title:      HOL/Lambda/Lambda.thy
        ID:         $Id: Lambda.thy,v 1.27 2005/06/17 14:13:08 haftmann Exp $
        Author:     Tobias Nipkow
        Copyright   1995 TU Muenchen
    *)

    header {* Basic definitions of Lambda-calculus *}

    theory Lambda imports Main begin

    subsection {* Lambda-terms in de Bruijn notation and substitution *}

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

    consts
      subst :: "[dB, dB, nat] => dB"  ("_[_'/_]" [300, 0, 0] 300)
      lift :: "[dB, nat] => dB"

    primrec
      "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  (* 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}. *}

    consts
      substn :: "[dB, dB, nat] => dB"
      liftn :: "[nat, dB, nat] => dB"

    primrec
      "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 (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 *}

    consts
      beta :: "(dB × dB) set"

    syntax
      "_beta" :: "[dB, dB] => bool"  (infixl "->" 50)
      "_beta_rtrancl" :: "[dB, dB] => bool"  (infixl "->>" 50)
    syntax (latex)
      "_beta" :: "[dB, dB] => bool"  (infixl "->β" 50)
      "_beta_rtrancl" :: "[dB, dB] => bool"  (infixl "->β*" 50)
    translations
      "s ->β t" == "(s, t) ∈ beta"
      "s ->β* t" == "(s, t) ∈ beta^*"

    inductive beta
      intros
        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"

    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 @{text "r_into_rtrancl[intro!]"} *}

    subsection {* Congruence rules *}

    lemma rtrancl_beta_Abs [intro!]:
        "s ->β* s' ==> Abs s ->β* Abs s'"
      apply (erule rtrancl_induct)
       apply (blast intro: rtrancl_into_rtrancl)+
      done

    lemma rtrancl_beta_AppL:
        "s ->β* s' ==> s ° t ->β* s' ° t"
      apply (erule rtrancl_induct)
       apply (blast intro: rtrancl_into_rtrancl)+
      done

    lemma rtrancl_beta_AppR:
        "t ->β* t' ==> s ° t ->β* s ° t'"
      apply (erule rtrancl_induct)
       apply (blast intro: rtrancl_into_rtrancl)+
      done

    lemma rtrancl_beta_App [intro]:
        "[| s ->β* s'; t ->β* t' |] ==> s ° t ->β* s' ° t'"
      apply (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR
        intro: rtrancl_trans)
      done

    subsection {* Substitution-lemmas *}

    lemma subst_eq [simp]: "(Var k)[u/k] = u"
      apply (simp add: subst_Var)
      done

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

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

    lemma lift_lift [rule_format]:
        "∀i k. i < k + 1 --> lift (lift t i) (Suc k) = lift (lift t k) i"
      apply (induct_tac t)
        apply auto
      done

    lemma lift_subst [simp]:
        "∀i j s. j < i + 1 --> lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]"
      apply (induct_tac t)
        apply (simp_all add: diff_Suc subst_Var lift_lift split: nat.split)
      done

    lemma lift_subst_lt:
        "∀i j s. i < j + 1 --> lift (t[s/j]) i = (lift t i) [lift s i / j + 1]"
      apply (induct_tac t)
        apply (simp_all add: subst_Var lift_lift)
      done

    lemma subst_lift [simp]:
        "∀k s. (lift t k)[s/k] = t"
      apply (induct_tac t)
        apply simp_all
      done

    lemma subst_subst [rule_format]:
        "∀i j u v. i < j + 1 --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
      apply (induct_tac t)
        apply (simp_all
          add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
          split: nat.split)
      done

    subsection {* Equivalence proof for optimized substitution *}

    lemma liftn_0 [simp]: "∀k. liftn 0 t k = t"
      apply (induct_tac t)
        apply (simp_all add: subst_Var)
      done

    lemma liftn_lift [simp]:
        "∀k. liftn (Suc n) t k = lift (liftn n t k) k"
      apply (induct_tac t)
        apply (simp_all add: subst_Var)
      done

    lemma substn_subst_n [simp]:
        "∀n. substn t s n = t[liftn n s 0 / n]"
      apply (induct_tac t)
        apply (simp_all add: subst_Var)
      done

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

    subsection {* Preservation theorems *}

    text {* Not used in Church-Rosser proof, but in Strong
      Normalization. \medskip *}

    theorem subst_preserves_beta [simp]:
        "r ->β s ==> (!!t i. r[t/i] ->β s[t/i])"
      apply (induct set: beta)
         apply (simp_all add: subst_subst [symmetric])
      done

    theorem subst_preserves_beta': "r ->β* s ==> r[t/i] ->β* s[t/i]"
      apply (erule rtrancl.induct)
      apply (rule rtrancl_refl)
      apply (erule rtrancl_into_rtrancl)
      apply (erule subst_preserves_beta)
      done

    theorem lift_preserves_beta [simp]:
        "r ->β s ==> (!!i. lift r i ->β lift s i)"
      by (induct set: beta) auto

    theorem lift_preserves_beta': "r ->β* s ==> lift r i ->β* lift s i"
      apply (erule rtrancl.induct)
      apply (rule rtrancl_refl)
      apply (erule rtrancl_into_rtrancl)
      apply (erule lift_preserves_beta)
      done

    theorem subst_preserves_beta2 [simp]:
        "!!r s i. r ->β s ==> t[r/i] ->β* t[s/i]"
      apply (induct t)
        apply (simp add: subst_Var r_into_rtrancl)
       apply (simp add: rtrancl_beta_App)
      apply (simp add: rtrancl_beta_Abs)
      done

    theorem subst_preserves_beta2': "r ->β* s ==> t[r/i] ->β* t[s/i]"
      apply (erule rtrancl.induct)
      apply (rule rtrancl_refl)
      apply (erule rtrancl_trans)
      apply (erule subst_preserves_beta2)
      done

    end

### Lambda-terms in de Bruijn notation and substitution

### Beta-reduction

lemmas beta_cases:

      Var i -> t ==> P

      [| Abs r -> s; !!t. [| r -> t; s = Abs t |] ==> P |] ==> P

      [| s ° t -> u; !!s. [| u = s[t/0]; s = Abs s |] ==> P;
         !!t. [| s -> t; u = t ° t |] ==> P; !!t. [| t -> t; u = s ° t |] ==> P |]
      ==> P

### Congruence rules

lemma rtrancl_beta_Abs:

      s ->> s' ==> Abs s ->> Abs s'

lemma rtrancl_beta_AppL:

      s ->> s' ==> s ° t ->> s' ° t

lemma rtrancl_beta_AppR:

      t ->> t' ==> s ° t ->> s ° t'

lemma rtrancl_beta_App:

      [| s ->> s'; t ->> t' |] ==> s ° t ->> s' ° t'

### Substitution-lemmas

lemma subst_eq:

      Var k[u/k] = u

lemma subst_gt:

      i < j ==> Var j[u/i] = Var (j - 1)

lemma subst_lt:

      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

lemma lift_subst:

      ∀i j s. j < i + 1 --> lift (t[s/j]) i = lift t (i + 1)[lift s i/j]

lemma lift_subst_lt:

      ∀i j s. i < j + 1 --> lift (t[s/j]) i = lift t i[lift s i/j + 1]

lemma subst_lift:

      ∀k s. lift t k[s/k] = t

lemma subst_subst:

      i < j + 1 ==> t[lift v i/Suc j][u[v/j]/i] = t[u/i][v/j]

### Equivalence proof for optimized substitution

lemma liftn_0:

      ∀k. liftn 0 t k = t

lemma liftn_lift:

      ∀k. liftn (Suc n) t k = lift (liftn n t k) k

lemma substn_subst_n:

      ∀n. substn t s n = t[liftn n s 0/n]

theorem substn_subst_0:

      substn t s 0 = t[s/0]

### Preservation theorems

theorem subst_preserves_beta:

      r -> s ==> r[t/i] -> s[t/i]

theorem subst_preserves_beta':

      r ->> s ==> r[t/i] ->> s[t/i]

theorem lift_preserves_beta:

      r -> s ==> lift r i -> lift s i

theorem lift_preserves_beta':

      r ->> s ==> lift r i ->> lift s i

theorem subst_preserves_beta2:

      r -> s ==> t[r/i] ->> t[s/i]

theorem subst_preserves_beta2':

      r ->> s ==> t[r/i] ->> t[s/i]