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 ZermeloFraenkel 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 
(*Codatatype 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,

55

58 
zero_in_univ, A_into_univ, nat_into_univ, UnCI];

0

59 

55

60 
(*Needed for mutual recursion*)


61 
val data_elims = [make_elim InlD, make_elim InrD];

0

62 


63 
(*For most codatatypes involving quniv*)


64 
val co_data_typechecks =


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 

55

69 
val co_data_elims = [make_elim QInlD, make_elim QInrD];


70 
