src/ZF/Datatype.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 55 331d93292ee0
permissions -rw-r--r--
Initial revision
clasohm@0
     1
(*  Title: 	ZF/datatype.ML
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
(Co-) Datatype Definitions for Zermelo-Fraenkel Set Theory
clasohm@0
     7
clasohm@0
     8
*)
clasohm@0
     9
clasohm@0
    10
clasohm@0
    11
(*Datatype definitions use least fixedpoints, standard products and sums*)
clasohm@0
    12
functor Datatype_Fun (Const: CONSTRUCTOR) 
clasohm@0
    13
         : sig include CONSTRUCTOR_RESULT INTR_ELIM INDRULE end =
clasohm@0
    14
struct
clasohm@0
    15
structure Constructor = Constructor_Fun (structure Const=Const and 
clasohm@0
    16
  		                      Pr=Standard_Prod and Su=Standard_Sum);
clasohm@0
    17
open Const Constructor;
clasohm@0
    18
clasohm@0
    19
structure Inductive = Inductive_Fun
clasohm@0
    20
        (val thy = con_thy;
clasohm@0
    21
	 val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs);
clasohm@0
    22
	 val sintrs = sintrs;
clasohm@0
    23
	 val monos = monos;
clasohm@0
    24
	 val con_defs = con_defs;
clasohm@0
    25
	 val type_intrs = type_intrs;
clasohm@0
    26
	 val type_elims = type_elims);
clasohm@0
    27
clasohm@0
    28
open Inductive
clasohm@0
    29
end;
clasohm@0
    30
clasohm@0
    31
clasohm@0
    32
(*Co-datatype definitions use greatest fixedpoints, Quine products and sums*)
clasohm@0
    33
functor Co_Datatype_Fun (Const: CONSTRUCTOR) 
clasohm@0
    34
         : sig include CONSTRUCTOR_RESULT INTR_ELIM CO_INDRULE end =
clasohm@0
    35
struct
clasohm@0
    36
structure Constructor = Constructor_Fun (structure Const=Const and 
clasohm@0
    37
  		                      Pr=Quine_Prod and Su=Quine_Sum);
clasohm@0
    38
open Const Constructor;
clasohm@0
    39
clasohm@0
    40
structure Co_Inductive = Co_Inductive_Fun
clasohm@0
    41
        (val thy = con_thy;
clasohm@0
    42
	 val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs);
clasohm@0
    43
	 val sintrs = sintrs;
clasohm@0
    44
	 val monos = monos;
clasohm@0
    45
	 val con_defs = con_defs;
clasohm@0
    46
	 val type_intrs = type_intrs;
clasohm@0
    47
	 val type_elims = type_elims);
clasohm@0
    48
clasohm@0
    49
open Co_Inductive
clasohm@0
    50
end;
clasohm@0
    51
clasohm@0
    52
clasohm@0
    53
clasohm@0
    54
(*For most datatypes involving univ*)
clasohm@0
    55
val data_typechecks = 
clasohm@0
    56
    [SigmaI, InlI, InrI,
clasohm@0
    57
     Pair_in_univ, Inl_in_univ, Inr_in_univ, 
clasohm@0
    58
     zero_in_univ, A_into_univ, nat_into_univ, sum_univ RS subsetD];
clasohm@0
    59
clasohm@0
    60
clasohm@0
    61
(*For most co-datatypes involving quniv*)
clasohm@0
    62
val co_data_typechecks = 
clasohm@0
    63
    [QSigmaI, QInlI, QInrI,
clasohm@0
    64
     QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
clasohm@0
    65
     zero_in_quniv, A_into_quniv, nat_into_quniv, qsum_quniv RS subsetD];
clasohm@0
    66