author | paulson |
Tue, 23 May 2000 18:06:22 +0200 | |
changeset 8935 | 548901d05a0e |
parent 6307 | fdf236c98914 |
child 9102 | c7ba07e3bbe8 |
permissions | -rw-r--r-- |
1269 | 1 |
(* Title: HOL/Lambda/Eta.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1995 TU Muenchen |
|
5 |
||
6 |
Eta-reduction and relatives. |
|
7 |
*) |
|
8 |
||
9 |
Eta = ParRed + Commutation + |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1900
diff
changeset
|
10 |
consts free :: dB => nat => bool |
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1900
diff
changeset
|
11 |
decr :: dB => dB |
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1900
diff
changeset
|
12 |
eta :: "(dB * dB) set" |
1269 | 13 |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1900
diff
changeset
|
14 |
syntax "-e>", "-e>>", "-e>=" , "->=" :: [dB,dB] => bool (infixl 50) |
1269 | 15 |
|
16 |
translations |
|
17 |
"s -e> t" == "(s,t) : eta" |
|
18 |
"s -e>> t" == "(s,t) : eta^*" |
|
19 |
"s -e>= t" == "(s,t) : eta^=" |
|
20 |
"s ->= t" == "(s,t) : beta^=" |
|
21 |
||
5184 | 22 |
primrec |
1900 | 23 |
"free (Var j) i = (j=i)" |
5146 | 24 |
"free (s $ t) i = (free s i | free t i)" |
6307 | 25 |
"free (Abs s) i = free s (i+1)" |
1269 | 26 |
|
1789 | 27 |
inductive eta |
1269 | 28 |
intrs |
5146 | 29 |
eta "~free s 0 ==> Abs(s $ Var 0) -e> s[dummy/0]" |
30 |
appL "s -e> t ==> s$u -e> t$u" |
|
31 |
appR "s -e> t ==> u$s -e> u$t" |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
1900
diff
changeset
|
32 |
abs "s -e> t ==> Abs s -e> Abs t" |
1269 | 33 |
end |
1900 | 34 |