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
clasohm@1478
     1
(*  Title:      ZF/Coind/Values.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
Values = Language + Map +
lcp@916
     8
lcp@916
     9
(* Values, values environments and associated operators *)
lcp@916
    10
lcp@916
    11
consts
clasohm@1401
    12
  Val, ValEnv, Val_ValEnv  :: i
lcp@933
    13
codatatype <= "quniv(Const Un ExVar Un Exp)"
lcp@933
    14
    "Val" = v_const("c:Const")
lcp@933
    15
          | v_clos("x:ExVar","e:Exp","ve:ValEnv")
lcp@933
    16
  and
lcp@933
    17
    "ValEnv" = ve_mk("m:PMap(ExVar,Val)")
lcp@933
    18
  monos      "[map_mono]"
lcp@933
    19
  type_intrs "[A_into_univ, mapQU]"
lcp@916
    20
lcp@916
    21
consts
clasohm@1401
    22
  ve_emp :: i
clasohm@1401
    23
  ve_owr :: [i,i,i] => i
clasohm@1401
    24
  ve_dom :: i=>i
clasohm@1401
    25
  ve_app :: [i,i] => i
lcp@933
    26
defs
lcp@916
    27
  ve_emp_def "ve_emp == ve_mk(map_emp)"
lcp@916
    28
  ve_owr_def
clasohm@1155
    29
    "ve_owr(ve,x,v) ==   
clasohm@1155
    30
    ve_mk(Val_ValEnv_case(%x.0,%x y z.0,%m.map_owr(m,x,v),ve))"
lcp@916
    31
  ve_dom_def
lcp@916
    32
    "ve_dom(ve) == Val_ValEnv_case(%x.0,%x y z.0,%m.domain(m),ve)"
lcp@916
    33
  ve_app_def
lcp@916
    34
    "ve_app(ve,a) == Val_ValEnv_case(%x.0,%x y z.0,%m.map_app(m,a),ve)"
lcp@916
    35
lcp@916
    36
end
lcp@916
    37
lcp@916
    38
lcp@916
    39