author | nipkow |
Mon, 04 Nov 1996 17:23:37 +0100 | |
changeset 2159 | e650a3f6f600 |
parent 1974 | b50f96543dec |
child 4360 | 40e5c97e988d |
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 |
||
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1974
diff
changeset
|
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 |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1974
diff
changeset
|
21 |
primrec lift dB |
1900 | 22 |
"lift (Var i) k = (if i < k then Var i else Var(Suc i))" |
23 |
"lift (s @ t) k = (lift s k) @ (lift t k)" |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1974
diff
changeset
|
24 |
"lift (Abs s) k = Abs(lift s (Suc k))" |
1120 | 25 |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1974
diff
changeset
|
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]" |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1974
diff
changeset
|
30 |
subst_Abs "(Abs t)[s/k] = Abs (t[lift s 0 / Suc k])" |
1120 | 31 |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1974
diff
changeset
|
32 |
primrec liftn dB |
1900 | 33 |
"liftn n (Var i) k = (if i < k then Var i else Var(i+n))" |
34 |
"liftn n (s @ t) k = (liftn n s k) @ (liftn n t k)" |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1974
diff
changeset
|
35 |
"liftn n (Abs s) k = Abs(liftn n s (Suc k))" |
1153 | 36 |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1974
diff
changeset
|
37 |
primrec substn dB |
1900 | 38 |
"substn (Var i) s k = (if k < i then Var(pred i) |
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)" |
1900 | 40 |
"substn (t @ u) s k = (substn t s k) @ (substn u s k)" |
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1974
diff
changeset
|
41 |
"substn (Abs t) s k = Abs (substn t s (Suc k))" |
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 |
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1974
diff
changeset
|
53 |
beta "(Abs s) @ t -> s[t/0]" |
1120 | 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 |