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 +
|
|
10 |
consts free :: "db => nat => bool"
|
|
11 |
decr :: "[db,nat] => db"
|
|
12 |
eta :: "(db * db) set"
|
|
13 |
|
|
14 |
syntax "-e>", "-e>>", "-e>=" , "->=" :: "[db,db] => bool" (infixl 50)
|
|
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 |
|
|
22 |
primrec free Lambda.db
|
|
23 |
free_Var "free (Var j) i = (j=i)"
|
|
24 |
free_App "free (s @ t) i = (free s i | free t i)"
|
|
25 |
free_Fun "free (Fun s) i = free s (Suc i)"
|
|
26 |
|
|
27 |
defs
|
|
28 |
decr_def "decr t i == t[Var i/i]"
|
|
29 |
|
|
30 |
inductive "eta"
|
|
31 |
intrs
|
|
32 |
eta "~free s 0 ==> Fun(s @ Var 0) -e> decr s 0"
|
|
33 |
appL "s -e> t ==> s@u -e> t@u"
|
|
34 |
appR "s -e> t ==> u@s -e> u@t"
|
|
35 |
abs "s -e> t ==> Fun s -e> Fun t"
|
|
36 |
end
|