author | nipkow |
Mon, 22 May 1995 14:12:40 +0200 | |
changeset 1124 | a6233ea105a4 |
parent 1120 | ff7dd80513e6 |
child 1153 | 5c5daf97cf2d |
permissions | -rw-r--r-- |
1120 | 1 |
(* Title: HOL/Lambda.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1995 TU Muenchen |
|
5 |
||
6 |
Lambda-terms in de Bruijn notation, |
|
7 |
substitution and beta-reduction. |
|
8 |
*) |
|
9 |
||
10 |
Lambda = Arith + |
|
11 |
||
12 |
datatype db = Var nat | "@" db db (infixl 200) | Fun db |
|
13 |
||
14 |
consts |
|
1124
a6233ea105a4
Polished the presentation making it completely definitional.
nipkow
parents:
1120
diff
changeset
|
15 |
subst :: "[db,db,nat]=>db" ("_[_'/_]" [300,0,0] 300) |
1120 | 16 |
lift :: "[db,nat] => db" |
17 |
||
18 |
primrec subst db |
|
1124
a6233ea105a4
Polished the presentation making it completely definitional.
nipkow
parents:
1120
diff
changeset
|
19 |
subst_Var "(Var i)[s/n] = (if n < i then Var(pred i) |
a6233ea105a4
Polished the presentation making it completely definitional.
nipkow
parents:
1120
diff
changeset
|
20 |
else if i = n then s else Var i)" |
a6233ea105a4
Polished the presentation making it completely definitional.
nipkow
parents:
1120
diff
changeset
|
21 |
subst_App "(t @ u)[s/n] = t[s/n] @ u[s/n]" |
a6233ea105a4
Polished the presentation making it completely definitional.
nipkow
parents:
1120
diff
changeset
|
22 |
subst_Fun "(Fun t)[s/n] = Fun (t[lift s 0 / Suc n])" |
1120 | 23 |
|
24 |
primrec lift db |
|
25 |
lift_Var "lift (Var i) n = (if i < n then Var i else Var(Suc i))" |
|
26 |
lift_App "lift (s @ t) n = (lift s n) @ (lift t n)" |
|
27 |
lift_Fun "lift (Fun s) n = Fun(lift s (Suc n))" |
|
28 |
||
29 |
consts beta :: "(db * db) set" |
|
30 |
||
31 |
syntax "->", "->>" :: "[db,db] => bool" (infixl 50) |
|
32 |
||
33 |
translations |
|
34 |
"s -> t" == "(s,t) : beta" |
|
35 |
"s ->> t" == "(s,t) : beta^*" |
|
36 |
||
37 |
inductive "beta" |
|
38 |
intrs |
|
1124
a6233ea105a4
Polished the presentation making it completely definitional.
nipkow
parents:
1120
diff
changeset
|
39 |
beta "(Fun s) @ t -> s[t/0]" |
1120 | 40 |
appL "s -> t ==> s@u -> t@u" |
41 |
appR "s -> t ==> u@s -> u@t" |
|
42 |
abs "s -> t ==> Fun s -> Fun t" |
|
43 |
end |