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 |