src/ZF/Coind/Types.thy

if-then-else syntax for ZF

(*  Title:      ZF/Coind/Types.thy
    ID:         $Id$
    Author:     Jacob Frost, Cambridge University Computer Laboratory
    Copyright   1995  University of Cambridge
*)

Types = Language +

consts
  Ty :: i                       (* Datatype of types *)
  TyConst :: i          (* Abstract type of type constants *)
datatype <= "univ(TyConst)"
  "Ty" = t_const("tc:TyConst")
       | t_fun("t1:Ty","t2:Ty")
  

(* Definition of type environments and associated operators *)

consts
  TyEnv :: i
datatype <= "univ(Ty Un ExVar)"
  "TyEnv" = te_emp
          | te_owr("te:TyEnv","x:ExVar","t:Ty") 

consts
  te_dom :: i => i
  te_app :: [i,i] => i


primrec (*domain of the type environment*)
  "te_dom (te_emp) = 0"
  "te_dom(te_owr(te,x,v)) = te_dom(te) Un {x}"

primrec (*lookup up identifiers in the type environment*)
  "te_app (te_emp,x) = 0"
  "te_app (te_owr(te,y,t),x) = (if x=y then t else te_app(te,x))"

end