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,


58 
zero_in_univ, A_into_univ, nat_into_univ, sum_univ RS subsetD];


59 


60 


61 
(*For most codatatypes 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 
