src/ZF/Coind/Types.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
clasohm@1478
     1
(*  Title:      ZF/Coind/Types.thy
lcp@916
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Jacob Frost, Cambridge University Computer Laboratory
lcp@916
     4
    Copyright   1995  University of Cambridge
lcp@916
     5
*)
lcp@916
     6
lcp@916
     7
Types = Language +
lcp@916
     8
lcp@916
     9
consts
clasohm@1478
    10
  Ty :: i                       (* Datatype of types *)
clasohm@1478
    11
  TyConst :: i          (* Abstract type of type constants *)
lcp@934
    12
datatype <= "univ(TyConst)"
lcp@934
    13
  "Ty" = t_const("tc:TyConst")
lcp@934
    14
       | t_fun("t1:Ty","t2:Ty")
lcp@916
    15
  
lcp@916
    16
lcp@916
    17
(* Definition of type environments and associated operators *)
lcp@916
    18
lcp@916
    19
consts
clasohm@1401
    20
  TyEnv :: i
lcp@934
    21
datatype <= "univ(Ty Un ExVar)"
lcp@934
    22
  "TyEnv" = te_emp
lcp@934
    23
          | te_owr("te:TyEnv","x:ExVar","t:Ty") 
lcp@916
    24
lcp@916
    25
consts
clasohm@1401
    26
  te_rec :: [i,i,[i,i,i,i]=>i] => i
lcp@934
    27
defs
lcp@916
    28
  te_rec_def
clasohm@1155
    29
    "te_rec(te,c,h) ==   
clasohm@1155
    30
    Vrec(te,%te g.TyEnv_case(c,%tem x t.h(tem,x,t,g`tem),te))"
lcp@916
    31
  
lcp@916
    32
consts
clasohm@1401
    33
  te_dom :: i => i
clasohm@1401
    34
  te_app :: [i,i] => i
lcp@934
    35
defs
lcp@916
    36
  te_dom_def "te_dom(te) == te_rec(te,0,% te x t r.r Un {x})"
lcp@916
    37
  te_app_def "te_app(te,x) == te_rec(te,0, % te y t r.if(x=y,t,r))"
lcp@916
    38
  
lcp@916
    39
lcp@916
    40
end
lcp@916
    41
lcp@916
    42
lcp@916
    43
lcp@916
    44
lcp@916
    45