--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/Eta.thy	Fri Oct 06 10:45:11 1995 +0100
@@ -0,0 +1,36 @@
+(*  Title:      HOL/Lambda/Eta.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1995 TU Muenchen
+
+Eta-reduction and relatives.
+*)
+
+Eta = ParRed + Commutation +
+consts free :: "db => nat => bool"
+       decr :: "[db,nat] => db"
+       eta  :: "(db * db) set"
+
+syntax  "-e>", "-e>>", "-e>=" , "->=" :: "[db,db] => bool" (infixl 50)
+
+translations
+  "s -e>  t" == "(s,t) : eta"
+  "s -e>> t" == "(s,t) : eta^*"
+  "s -e>= t" == "(s,t) : eta^="
+  "s ->=  t" == "(s,t) : beta^="
+
+primrec free Lambda.db
+  free_Var "free (Var j) i = (j=i)"
+  free_App "free (s @ t) i = (free s i | free t i)"
+  free_Fun "free (Fun s) i = free s (Suc i)"
+
+defs
+  decr_def "decr t i == t[Var i/i]"
+
+inductive "eta"
+intrs
+   eta  "~free s 0 ==> Fun(s @ Var 0) -e> decr s 0"
+   appL  "s -e> t ==> s@u -e> t@u"
+   appR  "s -e> t ==> u@s -e> u@t"
+   abs   "s -e> t ==> Fun s -e> Fun t"
+end