src/ZF/Datatype.ML
changeset 1461 6bcb44e4d6e5
parent 802 2f2fbf0a7e4f
child 6053 8a1059aa01f0
equal deleted inserted replaced
1460:5a6f2aabd538 1461:6bcb44e4d6e5
    24 
    24 
    25 val codatatype_elims = [make_elim QInlD, make_elim QInrD];
    25 val codatatype_elims = [make_elim QInlD, make_elim QInrD];
    26 
    26 
    27 signature INDUCTIVE_THMS =
    27 signature INDUCTIVE_THMS =
    28   sig
    28   sig
    29   val monos      : thm list		(*monotonicity of each M operator*)
    29   val monos      : thm list             (*monotonicity of each M operator*)
    30   val type_intrs : thm list		(*type-checking intro rules*)
    30   val type_intrs : thm list             (*type-checking intro rules*)
    31   val type_elims : thm list		(*type-checking elim rules*)
    31   val type_elims : thm list             (*type-checking elim rules*)
    32   end;
    32   end;
    33 
    33 
    34 functor Data_section_Fun
    34 functor Data_section_Fun
    35  (Arg: sig include CONSTRUCTOR_ARG INDUCTIVE_I INDUCTIVE_THMS end)  
    35  (Arg: sig include CONSTRUCTOR_ARG INDUCTIVE_I INDUCTIVE_THMS end)  
    36     : sig include CONSTRUCTOR_RESULT INTR_ELIM INDRULE end =
    36     : sig include CONSTRUCTOR_RESULT INTR_ELIM INDRULE end =
    37 struct
    37 struct
    38 
    38 
    39 structure Con = Constructor_Fun 
    39 structure Con = Constructor_Fun 
    40  	(structure Const = Arg and Pr=Standard_Prod and Su=Standard_Sum);
    40         (structure Const = Arg and Pr=Standard_Prod and Su=Standard_Sum);
    41 
    41 
    42 structure Inductive = Ind_section_Fun
    42 structure Inductive = Ind_section_Fun
    43    (open Arg; 
    43    (open Arg; 
    44     val con_defs = Con.con_defs
    44     val con_defs = Con.con_defs
    45     val type_intrs = Arg.type_intrs @ datatype_intrs
    45     val type_intrs = Arg.type_intrs @ datatype_intrs
    53  (Arg: sig include CONSTRUCTOR_ARG INDUCTIVE_I INDUCTIVE_THMS end)  
    53  (Arg: sig include CONSTRUCTOR_ARG INDUCTIVE_I INDUCTIVE_THMS end)  
    54     : sig include CONSTRUCTOR_RESULT INTR_ELIM COINDRULE end =
    54     : sig include CONSTRUCTOR_RESULT INTR_ELIM COINDRULE end =
    55 struct
    55 struct
    56 
    56 
    57 structure Con = Constructor_Fun 
    57 structure Con = Constructor_Fun 
    58  	(structure Const = Arg and Pr=Quine_Prod and Su=Quine_Sum);
    58         (structure Const = Arg and Pr=Quine_Prod and Su=Quine_Sum);
    59 
    59 
    60 structure CoInductive = CoInd_section_Fun
    60 structure CoInductive = CoInd_section_Fun
    61    (open Arg; 
    61    (open Arg; 
    62     val con_defs = Con.con_defs
    62     val con_defs = Con.con_defs
    63     val type_intrs = Arg.type_intrs @ codatatype_intrs
    63     val type_intrs = Arg.type_intrs @ codatatype_intrs