src/HOL/Lambda/Lambda.thy
author nipkow
Thu Jun 22 12:45:08 1995 +0200 (1995-06-22)
changeset 1153 5c5daf97cf2d
parent 1124 a6233ea105a4
child 1269 ee011b365770
permissions -rw-r--r--
Simplified the confluence proofs.
Added optimized substitution.
nipkow@1120
     1
(*  Title:      HOL/Lambda.thy
nipkow@1120
     2
    ID:         $Id$
nipkow@1120
     3
    Author:     Tobias Nipkow
nipkow@1120
     4
    Copyright   1995 TU Muenchen
nipkow@1120
     5
nipkow@1120
     6
Lambda-terms in de Bruijn notation,
nipkow@1120
     7
substitution and beta-reduction.
nipkow@1120
     8
*)
nipkow@1120
     9
nipkow@1120
    10
Lambda = Arith +
nipkow@1120
    11
nipkow@1120
    12
datatype db = Var nat | "@" db db (infixl 200) | Fun db
nipkow@1120
    13
nipkow@1120
    14
consts
nipkow@1124
    15
  subst  :: "[db,db,nat]=>db" ("_[_'/_]" [300,0,0] 300)
nipkow@1120
    16
  lift   :: "[db,nat] => db"
nipkow@1153
    17
  (* optimized versions *)
nipkow@1153
    18
  substn :: "[db,db,nat] => db"
nipkow@1153
    19
  liftn  :: "[nat,db,nat] => db"
nipkow@1153
    20
nipkow@1153
    21
primrec lift db
nipkow@1153
    22
  lift_Var "lift (Var i) k = (if i < k then Var i else Var(Suc i))"
nipkow@1153
    23
  lift_App "lift (s @ t) k = (lift s k) @ (lift t k)"
nipkow@1153
    24
  lift_Fun "lift (Fun s) k = Fun(lift s (Suc k))"
nipkow@1120
    25
nipkow@1120
    26
primrec subst db
nipkow@1153
    27
  subst_Var "(Var i)[s/k] = (if k < i then Var(pred i)
nipkow@1153
    28
                            else if i = k then s else Var i)"
nipkow@1153
    29
  subst_App "(t @ u)[s/k] = t[s/k] @ u[s/k]"
nipkow@1153
    30
  subst_Fun "(Fun t)[s/k] = Fun (t[lift s 0 / Suc k])"
nipkow@1120
    31
nipkow@1153
    32
primrec liftn db
nipkow@1153
    33
  liftn_Var "liftn n (Var i) k = (if i < k then Var i else Var(i+n))"
nipkow@1153
    34
  liftn_App "liftn n (s @ t) k = (liftn n s k) @ (liftn n t k)"
nipkow@1153
    35
  liftn_Fun "liftn n (Fun s) k = Fun(liftn n s (Suc k))"
nipkow@1153
    36
nipkow@1153
    37
primrec substn db
nipkow@1153
    38
  substn_Var "substn (Var i) s k = (if k < i then Var(pred i)
nipkow@1153
    39
                                    else if i = k then liftn k s 0 else Var i)"
nipkow@1153
    40
  substn_App "substn (t @ u) s k = (substn t s k) @ (substn u s k)"
nipkow@1153
    41
  substn_Fun "substn (Fun t) s k = Fun (substn t s (Suc k))"
nipkow@1120
    42
nipkow@1120
    43
consts  beta :: "(db * db) set"
nipkow@1120
    44
nipkow@1120
    45
syntax  "->", "->>" :: "[db,db] => bool" (infixl 50)
nipkow@1120
    46
nipkow@1120
    47
translations
nipkow@1120
    48
  "s -> t"  == "(s,t) : beta"
nipkow@1120
    49
  "s ->> t" == "(s,t) : beta^*"
nipkow@1120
    50
nipkow@1120
    51
inductive "beta"
nipkow@1120
    52
intrs
nipkow@1124
    53
   beta  "(Fun s) @ t -> s[t/0]"
nipkow@1120
    54
   appL  "s -> t ==> s@u -> t@u"
nipkow@1120
    55
   appR  "s -> t ==> u@s -> u@t"
nipkow@1120
    56
   abs   "s -> t ==> Fun s -> Fun t"
nipkow@1120
    57
end