author | oheimb |
Fri, 28 Jan 2000 11:22:02 +0100 | |
changeset 8148 | 5ef0b624aadb |
parent 6453 | c97d80581572 |
child 9811 | 39ffdb8cab03 |
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 |
||
6453 | 10 |
Lambda = Main + |
1120 | 11 |
|
5146 | 12 |
datatype dB = Var nat | "$" dB dB (infixl 200) | Abs dB |
1120 | 13 |
|
14 |
consts |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1974
diff
changeset
|
15 |
subst :: [dB,dB,nat]=>dB ("_[_'/_]" [300,0,0] 300) |
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1974
diff
changeset
|
16 |
lift :: [dB,nat] => dB |
1153 | 17 |
(* optimized versions *) |
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1974
diff
changeset
|
18 |
substn :: [dB,dB,nat] => dB |
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1974
diff
changeset
|
19 |
liftn :: [nat,dB,nat] => dB |
1153 | 20 |
|
5184 | 21 |
primrec |
6307 | 22 |
"lift (Var i) k = (if i < k then Var i else Var(i+1))" |
5146 | 23 |
"lift (s $ t) k = (lift s k) $ (lift t k)" |
6307 | 24 |
"lift (Abs s) k = Abs(lift s (k+1))" |
1120 | 25 |
|
5184 | 26 |
primrec |
4360 | 27 |
subst_Var "(Var i)[s/k] = (if k < i then Var(i-1) |
1153 | 28 |
else if i = k then s else Var i)" |
5146 | 29 |
subst_App "(t $ u)[s/k] = t[s/k] $ u[s/k]" |
6307 | 30 |
subst_Abs "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])" |
1120 | 31 |
|
5184 | 32 |
primrec |
1900 | 33 |
"liftn n (Var i) k = (if i < k then Var i else Var(i+n))" |
5146 | 34 |
"liftn n (s $ t) k = (liftn n s k) $ (liftn n t k)" |
6307 | 35 |
"liftn n (Abs s) k = Abs(liftn n s (k+1))" |
1153 | 36 |
|
5184 | 37 |
primrec |
4360 | 38 |
"substn (Var i) s k = (if k < i then Var(i-1) |
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1900
diff
changeset
|
39 |
else if i = k then liftn k s 0 else Var i)" |
5146 | 40 |
"substn (t $ u) s k = (substn t s k) $ (substn u s k)" |
6307 | 41 |
"substn (Abs t) s k = Abs (substn t s (k+1))" |
1120 | 42 |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1974
diff
changeset
|
43 |
consts beta :: "(dB * dB) set" |
1120 | 44 |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1974
diff
changeset
|
45 |
syntax "->", "->>" :: [dB,dB] => bool (infixl 50) |
1120 | 46 |
|
47 |
translations |
|
48 |
"s -> t" == "(s,t) : beta" |
|
49 |
"s ->> t" == "(s,t) : beta^*" |
|
50 |
||
1789 | 51 |
inductive beta |
1120 | 52 |
intrs |
5146 | 53 |
beta "(Abs s) $ t -> s[t/0]" |
54 |
appL "s -> t ==> s$u -> t$u" |
|
55 |
appR "s -> t ==> u$s -> u$t" |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1974
diff
changeset
|
56 |
abs "s -> t ==> Abs s -> Abs t" |
1120 | 57 |
end |