author | clasohm |
Fri, 01 Dec 1995 12:03:13 +0100 | |
changeset 1376 | 92f83b9d17e1 |
parent 1269 | ee011b365770 |
child 1789 | aade046ec6d5 |
permissions | -rw-r--r-- |
1269 | 1 |
(* Title: HOL/Lambda/Lambda.thy |
1120 | 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 |
|
1376 | 15 |
subst :: [db,db,nat]=>db ("_[_'/_]" [300,0,0] 300) |
16 |
lift :: [db,nat] => db |
|
1153 | 17 |
(* optimized versions *) |
1376 | 18 |
substn :: [db,db,nat] => db |
19 |
liftn :: [nat,db,nat] => db |
|
1153 | 20 |
|
21 |
primrec lift db |
|
22 |
lift_Var "lift (Var i) k = (if i < k then Var i else Var(Suc i))" |
|
23 |
lift_App "lift (s @ t) k = (lift s k) @ (lift t k)" |
|
24 |
lift_Fun "lift (Fun s) k = Fun(lift s (Suc k))" |
|
1120 | 25 |
|
26 |
primrec subst db |
|
1153 | 27 |
subst_Var "(Var i)[s/k] = (if k < i then Var(pred i) |
28 |
else if i = k then s else Var i)" |
|
29 |
subst_App "(t @ u)[s/k] = t[s/k] @ u[s/k]" |
|
30 |
subst_Fun "(Fun t)[s/k] = Fun (t[lift s 0 / Suc k])" |
|
1120 | 31 |
|
1153 | 32 |
primrec liftn db |
33 |
liftn_Var "liftn n (Var i) k = (if i < k then Var i else Var(i+n))" |
|
34 |
liftn_App "liftn n (s @ t) k = (liftn n s k) @ (liftn n t k)" |
|
35 |
liftn_Fun "liftn n (Fun s) k = Fun(liftn n s (Suc k))" |
|
36 |
||
37 |
primrec substn db |
|
38 |
substn_Var "substn (Var i) s k = (if k < i then Var(pred i) |
|
39 |
else if i = k then liftn k s 0 else Var i)" |
|
40 |
substn_App "substn (t @ u) s k = (substn t s k) @ (substn u s k)" |
|
41 |
substn_Fun "substn (Fun t) s k = Fun (substn t s (Suc k))" |
|
1120 | 42 |
|
43 |
consts beta :: "(db * db) set" |
|
44 |
||
1376 | 45 |
syntax "->", "->>" :: [db,db] => bool (infixl 50) |
1120 | 46 |
|
47 |
translations |
|
48 |
"s -> t" == "(s,t) : beta" |
|
49 |
"s ->> t" == "(s,t) : beta^*" |
|
50 |
||
51 |
inductive "beta" |
|
52 |
intrs |
|
1124
a6233ea105a4
Polished the presentation making it completely definitional.
nipkow
parents:
1120
diff
changeset
|
53 |
beta "(Fun s) @ t -> s[t/0]" |
1120 | 54 |
appL "s -> t ==> s@u -> t@u" |
55 |
appR "s -> t ==> u@s -> u@t" |
|
56 |
abs "s -> t ==> Fun s -> Fun t" |
|
57 |
end |