src/HOL/Lambda/Eta.thy

Quotes now optional around inductive set

(*  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