src/ZF/Datatype.ML
changeset 0 a5a9c433f639
child 55 331d93292ee0
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/Datatype.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,66 @@
     1.4 +(*  Title: 	ZF/datatype.ML
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +(Co-) Datatype Definitions for Zermelo-Fraenkel Set Theory
    1.10 +
    1.11 +*)
    1.12 +
    1.13 +
    1.14 +(*Datatype definitions use least fixedpoints, standard products and sums*)
    1.15 +functor Datatype_Fun (Const: CONSTRUCTOR) 
    1.16 +         : sig include CONSTRUCTOR_RESULT INTR_ELIM INDRULE end =
    1.17 +struct
    1.18 +structure Constructor = Constructor_Fun (structure Const=Const and 
    1.19 +  		                      Pr=Standard_Prod and Su=Standard_Sum);
    1.20 +open Const Constructor;
    1.21 +
    1.22 +structure Inductive = Inductive_Fun
    1.23 +        (val thy = con_thy;
    1.24 +	 val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs);
    1.25 +	 val sintrs = sintrs;
    1.26 +	 val monos = monos;
    1.27 +	 val con_defs = con_defs;
    1.28 +	 val type_intrs = type_intrs;
    1.29 +	 val type_elims = type_elims);
    1.30 +
    1.31 +open Inductive
    1.32 +end;
    1.33 +
    1.34 +
    1.35 +(*Co-datatype definitions use greatest fixedpoints, Quine products and sums*)
    1.36 +functor Co_Datatype_Fun (Const: CONSTRUCTOR) 
    1.37 +         : sig include CONSTRUCTOR_RESULT INTR_ELIM CO_INDRULE end =
    1.38 +struct
    1.39 +structure Constructor = Constructor_Fun (structure Const=Const and 
    1.40 +  		                      Pr=Quine_Prod and Su=Quine_Sum);
    1.41 +open Const Constructor;
    1.42 +
    1.43 +structure Co_Inductive = Co_Inductive_Fun
    1.44 +        (val thy = con_thy;
    1.45 +	 val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs);
    1.46 +	 val sintrs = sintrs;
    1.47 +	 val monos = monos;
    1.48 +	 val con_defs = con_defs;
    1.49 +	 val type_intrs = type_intrs;
    1.50 +	 val type_elims = type_elims);
    1.51 +
    1.52 +open Co_Inductive
    1.53 +end;
    1.54 +
    1.55 +
    1.56 +
    1.57 +(*For most datatypes involving univ*)
    1.58 +val data_typechecks = 
    1.59 +    [SigmaI, InlI, InrI,
    1.60 +     Pair_in_univ, Inl_in_univ, Inr_in_univ, 
    1.61 +     zero_in_univ, A_into_univ, nat_into_univ, sum_univ RS subsetD];
    1.62 +
    1.63 +
    1.64 +(*For most co-datatypes involving quniv*)
    1.65 +val co_data_typechecks = 
    1.66 +    [QSigmaI, QInlI, QInrI,
    1.67 +     QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
    1.68 +     zero_in_quniv, A_into_quniv, nat_into_quniv, qsum_quniv RS subsetD];
    1.69 +