author | clasohm |
Fri, 15 Jul 1994 13:34:31 +0200 | |
changeset 477 | 53fc8ad84b33 |
parent 120 | 09287f26bfb8 |
child 516 | 1957113f0d7d |
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 |
||
120 | 6 |
(Co)Datatype Definitions for Zermelo-Fraenkel Set Theory |
0 | 7 |
*) |
8 |
||
9 |
||
10 |
(*Datatype definitions use least fixedpoints, standard products and sums*) |
|
11 |
functor Datatype_Fun (Const: CONSTRUCTOR) |
|
12 |
: sig include CONSTRUCTOR_RESULT INTR_ELIM INDRULE end = |
|
13 |
struct |
|
14 |
structure Constructor = Constructor_Fun (structure Const=Const and |
|
15 |
Pr=Standard_Prod and Su=Standard_Sum); |
|
16 |
open Const Constructor; |
|
17 |
||
18 |
structure Inductive = Inductive_Fun |
|
19 |
(val thy = con_thy; |
|
477 | 20 |
val thy_name = thy_name; |
0 | 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 |
||
120 | 32 |
(*Codatatype definitions use greatest fixedpoints, Quine products and sums*) |
33 |
functor CoDatatype_Fun (Const: CONSTRUCTOR) |
|
34 |
: sig include CONSTRUCTOR_RESULT INTR_ELIM COINDRULE end = |
|
0 | 35 |
struct |
36 |
structure Constructor = Constructor_Fun (structure Const=Const and |
|
37 |
Pr=Quine_Prod and Su=Quine_Sum); |
|
38 |
open Const Constructor; |
|
39 |
||
120 | 40 |
structure CoInductive = CoInductive_Fun |
0 | 41 |
(val thy = con_thy; |
477 | 42 |
val thy_name = thy_name; |
0 | 43 |
val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs); |
44 |
val sintrs = sintrs; |
|
45 |
val monos = monos; |
|
46 |
val con_defs = con_defs; |
|
47 |
val type_intrs = type_intrs; |
|
48 |
val type_elims = type_elims); |
|
49 |
||
120 | 50 |
open CoInductive |
0 | 51 |
end; |
52 |
||
53 |
||
54 |
||
55 |
(*For most datatypes involving univ*) |
|
70
8a29f8b4aca1
ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works
lcp
parents:
55
diff
changeset
|
56 |
val datatype_intrs = |
0 | 57 |
[SigmaI, InlI, InrI, |
58 |
Pair_in_univ, Inl_in_univ, Inr_in_univ, |
|
55 | 59 |
zero_in_univ, A_into_univ, nat_into_univ, UnCI]; |
0 | 60 |
|
55 | 61 |
(*Needed for mutual recursion*) |
70
8a29f8b4aca1
ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works
lcp
parents:
55
diff
changeset
|
62 |
val datatype_elims = [make_elim InlD, make_elim InrD]; |
0 | 63 |
|
120 | 64 |
(*For most codatatypes involving quniv*) |
65 |
val codatatype_intrs = |
|
0 | 66 |
[QSigmaI, QInlI, QInrI, |
67 |
QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, |
|
55 | 68 |
zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI]; |
0 | 69 |
|
120 | 70 |
val codatatype_elims = [make_elim QInlD, make_elim QInrD]; |
55 | 71 |