src/ZF/Coind/Values.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:      ZF/Coind/Values.thy
     2     ID:         $Id$
     3     Author:     Jacob Frost, Cambridge University Computer Laboratory
     4     Copyright   1995  University of Cambridge
     5 *)
     6 
     7 Values = Language + Map +
     8 
     9 (* Values, values environments and associated operators *)
    10 
    11 consts
    12   Val, ValEnv, Val_ValEnv  :: i
    13 codatatype <= "quniv(Const Un ExVar Un Exp)"
    14     "Val" = v_const("c:Const")
    15           | v_clos("x:ExVar","e:Exp","ve:ValEnv")
    16   and
    17     "ValEnv" = ve_mk("m:PMap(ExVar,Val)")
    18   monos      "[map_mono]"
    19   type_intrs "[A_into_univ, mapQU]"
    20 
    21 consts
    22   ve_emp :: i
    23   ve_owr :: [i,i,i] => i
    24   ve_dom :: i=>i
    25   ve_app :: [i,i] => i
    26 defs
    27   ve_emp_def "ve_emp == ve_mk(map_emp)"
    28   ve_owr_def
    29     "ve_owr(ve,x,v) ==   
    30     ve_mk(Val_ValEnv_case(%x.0,%x y z.0,%m.map_owr(m,x,v),ve))"
    31   ve_dom_def
    32     "ve_dom(ve) == Val_ValEnv_case(%x.0,%x y z.0,%m.domain(m),ve)"
    33   ve_app_def
    34     "ve_app(ve,a) == Val_ValEnv_case(%x.0,%x y z.0,%m.map_app(m,a),ve)"
    35 
    36 end
    37 
    38 
    39