|
1 (* Title: ZF/datatype.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 (Co-) Datatype Definitions for Zermelo-Fraenkel Set Theory |
|
7 |
|
8 *) |
|
9 |
|
10 |
|
11 (*Datatype definitions use least fixedpoints, standard products and sums*) |
|
12 functor Datatype_Fun (Const: CONSTRUCTOR) |
|
13 : sig include CONSTRUCTOR_RESULT INTR_ELIM INDRULE end = |
|
14 struct |
|
15 structure Constructor = Constructor_Fun (structure Const=Const and |
|
16 Pr=Standard_Prod and Su=Standard_Sum); |
|
17 open Const Constructor; |
|
18 |
|
19 structure Inductive = Inductive_Fun |
|
20 (val thy = con_thy; |
|
21 val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs); |
|
22 val sintrs = sintrs; |
|
23 val monos = monos; |
|
24 val con_defs = con_defs; |
|
25 val type_intrs = type_intrs; |
|
26 val type_elims = type_elims); |
|
27 |
|
28 open Inductive |
|
29 end; |
|
30 |
|
31 |
|
32 (*Co-datatype definitions use greatest fixedpoints, Quine products and sums*) |
|
33 functor Co_Datatype_Fun (Const: CONSTRUCTOR) |
|
34 : sig include CONSTRUCTOR_RESULT INTR_ELIM CO_INDRULE end = |
|
35 struct |
|
36 structure Constructor = Constructor_Fun (structure Const=Const and |
|
37 Pr=Quine_Prod and Su=Quine_Sum); |
|
38 open Const Constructor; |
|
39 |
|
40 structure Co_Inductive = Co_Inductive_Fun |
|
41 (val thy = con_thy; |
|
42 val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs); |
|
43 val sintrs = sintrs; |
|
44 val monos = monos; |
|
45 val con_defs = con_defs; |
|
46 val type_intrs = type_intrs; |
|
47 val type_elims = type_elims); |
|
48 |
|
49 open Co_Inductive |
|
50 end; |
|
51 |
|
52 |
|
53 |
|
54 (*For most datatypes involving univ*) |
|
55 val data_typechecks = |
|
56 [SigmaI, InlI, InrI, |
|
57 Pair_in_univ, Inl_in_univ, Inr_in_univ, |
|
58 zero_in_univ, A_into_univ, nat_into_univ, sum_univ RS subsetD]; |
|
59 |
|
60 |
|
61 (*For most co-datatypes involving quniv*) |
|
62 val co_data_typechecks = |
|
63 [QSigmaI, QInlI, QInrI, |
|
64 QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, |
|
65 zero_in_quniv, A_into_quniv, nat_into_quniv, qsum_quniv RS subsetD]; |
|
66 |