equal
deleted
inserted
replaced
|
1 theory CoreHaskell2 |
|
2 imports "../Nominal2" |
|
3 begin |
|
4 |
|
5 (* Core Haskell by John Matthews *) |
|
6 |
|
7 atom_decl var |
|
8 atom_decl cvar |
|
9 atom_decl tvar |
|
10 |
|
11 |
|
12 nominal_datatype kinds: |
|
13 Kind = |
|
14 Klifted |
|
15 | Kunlifted |
|
16 | Kopen |
|
17 | Karrow Kind Kind |
|
18 | Keq Ty Ty |
|
19 and Ty = |
|
20 Tvar tvar |
|
21 | Tcon string |
|
22 | Tapp Ty Ty |
|
23 | Tforall pb::PBind ty::Ty bind "bind_pb pb" in ty |
|
24 and PBind = |
|
25 Pbind tvar Kind |
|
26 binder |
|
27 bind_pb |
|
28 where |
|
29 "bind_pb (Pbind tv k) = [atom tv]" |
|
30 |
|
31 nominal_datatype expressions: |
|
32 Bind = |
|
33 Vb var Ty |
|
34 | Tb tvar Kind |
|
35 and Exp = |
|
36 Var var |
|
37 | Dcon string |
|
38 | App Exp Exp |
|
39 | Appt Exp Ty |
|
40 | Lam b::Bind e::Exp bind "bind_b b" in e |
|
41 binder |
|
42 bind_b |
|
43 where |
|
44 "bind_b (Vb v ty) = [atom v]" |
|
45 | "bind_b (Tb tv kind) = [atom tv]" |
|
46 |
|
47 thm kinds.distinct |
|
48 thm kinds.induct |
|
49 thm kinds.inducts |
|
50 thm kinds.exhaust |
|
51 thm kinds.strong_exhaust |
|
52 thm kinds.fv_defs |
|
53 thm kinds.bn_defs |
|
54 thm kinds.perm_simps |
|
55 thm kinds.eq_iff |
|
56 thm kinds.fv_bn_eqvt |
|
57 thm kinds.size_eqvt |
|
58 thm kinds.supports |
|
59 thm kinds.fsupp |
|
60 thm kinds.supp |
|
61 thm kinds.fresh |
|
62 |
|
63 thm expressions.distinct |
|
64 thm expressions.induct |
|
65 thm expressions.inducts |
|
66 thm expressions.exhaust |
|
67 thm expressions.fv_defs |
|
68 thm expressions.bn_defs |
|
69 thm expressions.perm_simps |
|
70 thm expressions.eq_iff |
|
71 thm expressions.fv_bn_eqvt |
|
72 thm expressions.size_eqvt |
|
73 thm expressions.supports |
|
74 thm expressions.fsupp |
|
75 thm expressions.supp |
|
76 thm expressions.fresh |
|
77 |
|
78 end |
|
79 |