author | lcp |
Fri, 22 Oct 1993 11:34:41 +0100 | |
changeset 70 | 8a29f8b4aca1 |
parent 55 | 331d93292ee0 |
child 120 | 09287f26bfb8 |
permissions | -rw-r--r-- |
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*) |
|
70
8a29f8b4aca1
ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works
lcp
parents:
55
diff
changeset
|
55 |
val datatype_intrs = |
0 | 56 |
[SigmaI, InlI, InrI, |
57 |
Pair_in_univ, Inl_in_univ, Inr_in_univ, |
|
55 | 58 |
zero_in_univ, A_into_univ, nat_into_univ, UnCI]; |
0 | 59 |
|
55 | 60 |
(*Needed for mutual recursion*) |
70
8a29f8b4aca1
ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works
lcp
parents:
55
diff
changeset
|
61 |
val datatype_elims = [make_elim InlD, make_elim InrD]; |
0 | 62 |
|
63 |
(*For most co-datatypes involving quniv*) |
|
70
8a29f8b4aca1
ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works
lcp
parents:
55
diff
changeset
|
64 |
val co_datatype_intrs = |
0 | 65 |
[QSigmaI, QInlI, QInrI, |
66 |
QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, |
|
55 | 67 |
zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI]; |
0 | 68 |
|
70
8a29f8b4aca1
ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works
lcp
parents:
55
diff
changeset
|
69 |
val co_datatype_elims = [make_elim QInlD, make_elim QInrD]; |
55 | 70 |