src/ZF/Coind/Language.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 2874 b1e7e2179597
permissions -rw-r--r--
expanded tabs
     1 (*  Title:      ZF/Coind/Language.thy
     2     ID:         $Id$
     3     Author:     Jacob Frost, Cambridge University Computer Laboratory
     4     Copyright   1995  University of Cambridge
     5 *)
     6 
     7 Language ="Datatype" + QUniv +
     8 
     9 consts
    10   Const :: i                    (* Abstract type of constants *)
    11   c_app :: [i,i] => i           (*Abstract constructor for fun application*)
    12 
    13 rules
    14   constNEE  "c:Const ==> c ~= 0"
    15   c_appI    "[| c1:Const; c2:Const |] ==> c_app(c1,c2):Const"
    16 
    17 
    18 consts
    19   Exp   :: i                    (* Datatype of expressions *)
    20   ExVar :: i                    (* Abstract type of variables *)
    21 datatype <= "univ(Const Un ExVar)"
    22   "Exp" = e_const("c:Const")
    23         | e_var("x:ExVar")
    24         | e_fn("x:ExVar","e:Exp")
    25         | e_fix("x1:ExVar","x2:ExVar","e:Exp")
    26         | e_app("e1:Exp","e2:Exp")
    27 
    28 end