src/HOL/Lambda/Eta.thy
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2159 e650a3f6f600
child 5146 1ea751ae62b2
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     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 => 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 j) i = (j=i)"
    24   "free (s @ t) i = (free s i | free t i)"
    25   "free (Abs s) i = free s (Suc i)"
    26 
    27 inductive eta
    28 intrs
    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"
    32    abs   "s -e> t ==> Abs s -e> Abs t"
    33 end
    34