0
|
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 |
|