src/ZF/Resid/Terms.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 3840 e0baea4d485a
permissions -rw-r--r--
expanded tabs
     1 (*  Title:      Terms.thy
     2     ID:         $Id$
     3     Author:     Ole Rasmussen
     4     Copyright   1995  University of Cambridge
     5     Logic Image: ZF
     6 *)
     7 
     8 Terms = Cube+
     9 
    10 consts
    11   lambda        :: i
    12   unmark        :: i=>i
    13   Apl           :: [i,i]=>i
    14 
    15 translations
    16   "Apl(n,m)" == "App(0,n,m)"
    17   
    18 inductive
    19   domains       "lambda" <= "redexes"
    20   intrs
    21     Lambda_Var  "               n:nat ==>     Var(n):lambda"
    22     Lambda_Fun  "            u:lambda ==>     Fun(u):lambda"
    23     Lambda_App  "[|u:lambda; v:lambda|]==> Apl(u,v):lambda"
    24   type_intrs    "redexes.intrs@bool_typechecks"
    25 
    26 defs
    27   unmark_def    "unmark(u) == redex_rec(u,%i.Var(i),   
    28                                           %x m.Fun(m),   
    29                                           %b x y m p.Apl(m,p))"
    30 end
    31 
    32