|
1 (* Title: ZF/Coind/Types.thy |
|
2 ID: $Id$ |
|
3 Author: Jacob Frost, Cambridge University Computer Laboratory |
|
4 Copyright 1995 University of Cambridge |
|
5 *) |
|
6 |
|
7 Types = Language + |
|
8 |
|
9 (* Abstract type of type constants *) |
|
10 |
|
11 consts |
|
12 TyConst :: "i" |
|
13 rules |
|
14 tyconstU "tc:TyConst ==> tc:univ(0)" |
|
15 |
|
16 |
|
17 (* Datatype of types *) |
|
18 |
|
19 consts |
|
20 Ty :: "i" |
|
21 datatype |
|
22 "Ty" = |
|
23 t_const("tc:TyConst") | |
|
24 t_fun("t1:Ty","t2:Ty") |
|
25 type_intrs "[tyconstU]" |
|
26 |
|
27 |
|
28 (* Definition of type environments and associated operators *) |
|
29 |
|
30 consts |
|
31 TyEnv :: "i" |
|
32 datatype |
|
33 "TyEnv" = |
|
34 te_emp | |
|
35 te_owr("te:TyEnv","x:ExVar","t:Ty") |
|
36 type_intrs "[exvarU,Ty.dom_subset RS subsetD]" |
|
37 |
|
38 consts |
|
39 te_rec :: "[i,i,[i,i,i,i]=>i] => i" |
|
40 rules |
|
41 te_rec_def |
|
42 "te_rec(te,c,h) == \ |
|
43 \ Vrec(te,%te g.TyEnv_case(c,%tem x t.h(tem,x,t,g`tem),te))" |
|
44 |
|
45 consts |
|
46 te_dom :: "i => i" |
|
47 te_app :: "[i,i] => i" |
|
48 rules |
|
49 te_dom_def "te_dom(te) == te_rec(te,0,% te x t r.r Un {x})" |
|
50 te_app_def "te_app(te,x) == te_rec(te,0, % te y t r.if(x=y,t,r))" |
|
51 |
|
52 |
|
53 end |
|
54 |
|
55 |
|
56 |
|
57 |
|
58 |