diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/inductive.ML --- a/src/ZF/inductive.ML Fri Aug 12 12:28:46 1994 +0200 +++ b/src/ZF/inductive.ML Fri Aug 12 12:51:34 1994 +0200 @@ -3,15 +3,17 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge -Inductive Definitions for Zermelo-Fraenkel Set Theory +(Co)Inductive Definitions for Zermelo-Fraenkel Set Theory -Uses least fixedpoints with standard products and sums +Inductive definitions use least fixedpoints with standard products and sums +Coinductive definitions use greatest fixedpoints with Quine products and sums Sums are used only for mutual recursion; Products are used only to derive "streamlined" induction rules for relations *) - +local open Ind_Syntax +in structure Lfp = struct val oper = Const("lfp", [iT,iT-->iT]--->iT) @@ -48,16 +50,179 @@ val distinct = Inl_Inr_iff val distinct' = Inr_Inl_iff end; +end; -functor Inductive_Fun (Ind: INDUCTIVE) : sig include INTR_ELIM INDRULE end = +functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) + : sig include INTR_ELIM INDRULE end = struct structure Intr_elim = - Intr_elim_Fun(structure Ind=Ind and Fp=Lfp and + Intr_elim_Fun(structure Inductive=Inductive and Fp=Lfp and Pr=Standard_Prod and Su=Standard_Sum); -structure Indrule = Indrule_Fun (structure Ind=Ind and +structure Indrule = Indrule_Fun (structure Inductive=Inductive and Pr=Standard_Prod and Intr_elim=Intr_elim); open Intr_elim Indrule end; + +structure Ind = Add_inductive_def_Fun + (structure Fp=Lfp and Pr=Standard_Prod and Su=Standard_Sum); + + +signature INDUCTIVE_STRING = + sig + val thy_name : string (*name of the new theory*) + val rec_doms : (string*string) list (*recursion terms and their domains*) + val sintrs : string list (*desired introduction rules*) + end; + + +(*For upwards compatibility: can be called directly from ML*) +functor Inductive_Fun + (Inductive: sig include INDUCTIVE_STRING INDUCTIVE_ARG end) + : sig include INTR_ELIM INDRULE end = +Ind_section_Fun + (open Inductive Ind_Syntax + val sign = sign_of thy; + val rec_tms = map (readtm sign iT o #1) rec_doms + and domts = map (readtm sign iT o #2) rec_doms + and intr_tms = map (readtm sign propT) sintrs; + val thy = thy |> Ind.add_fp_def_i(rec_tms, domts, intr_tms) + |> add_thyname thy_name); + + + +local open Ind_Syntax +in +structure Gfp = + struct + val oper = Const("gfp", [iT,iT-->iT]--->iT) + val bnd_mono = Const("bnd_mono", [iT,iT-->iT]--->oT) + val bnd_monoI = bnd_monoI + val subs = def_gfp_subset + val Tarski = def_gfp_Tarski + val induct = def_Collect_coinduct + end; + +structure Quine_Prod = + struct + val sigma = Const("QSigma", [iT, iT-->iT]--->iT) + val pair = Const("QPair", [iT,iT]--->iT) + val split_const = Const("qsplit", [[iT,iT]--->iT, iT]--->iT) + val fsplit_const = Const("qfsplit", [[iT,iT]--->oT, iT]--->oT) + val pair_iff = QPair_iff + val split_eq = qsplit + val fsplitI = qfsplitI + val fsplitD = qfsplitD + val fsplitE = qfsplitE + end; + +structure Quine_Sum = + struct + val sum = Const("op <+>", [iT,iT]--->iT) + val inl = Const("QInl", iT-->iT) + val inr = Const("QInr", iT-->iT) + val elim = Const("qcase", [iT-->iT, iT-->iT, iT]--->iT) + val case_inl = qcase_QInl + val case_inr = qcase_QInr + val inl_iff = QInl_iff + val inr_iff = QInr_iff + val distinct = QInl_QInr_iff + val distinct' = QInr_QInl_iff + end; +end; + + +signature COINDRULE = + sig + val coinduct : thm + end; + + +functor CoInd_section_Fun + (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) + : sig include INTR_ELIM COINDRULE end = +struct +structure Intr_elim = + Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp and + Pr=Quine_Prod and Su=Quine_Sum); + +open Intr_elim +val coinduct = raw_induct +end; + + +structure CoInd = + Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and Su=Quine_Sum); + + +(*For upwards compatibility: can be called directly from ML*) +functor CoInductive_Fun + (Inductive: sig include INDUCTIVE_STRING INDUCTIVE_ARG end) + : sig include INTR_ELIM COINDRULE end = +CoInd_section_Fun + (open Inductive Ind_Syntax + val sign = sign_of thy; + val rec_tms = map (readtm sign iT o #1) rec_doms + and domts = map (readtm sign iT o #2) rec_doms + and intr_tms = map (readtm sign propT) sintrs; + val thy = thy |> CoInd.add_fp_def_i(rec_tms, domts, intr_tms) + |> add_thyname thy_name); + + + +(*For installing the theory section. co is either "" or "Co"*) +fun inductive_decl co = + let open ThyParse Ind_Syntax + fun mk_intr_name (s,_) = (*the "op" cancels any infix status*) + if Syntax.is_identifier s then "op " ^ s else "_" + fun mk_params (((((domains: (string*string) list, ipairs), + monos), con_defs), type_intrs), type_elims) = + let val big_rec_name = space_implode "_" + (map (scan_to_id o trim o #1) domains) + and srec_tms = mk_list (map #1 domains) + and sdoms = mk_list (map #2 domains) + and sintrs = mk_big_list (map snd ipairs) + val stri_name = big_rec_name ^ "_Intrnl" + in + (";\n\n\ + \structure " ^ stri_name ^ " =\n\ + \ let open Ind_Syntax in\n\ + \ struct\n\ + \ val rec_tms\t= map (readtm (sign_of thy) iT) " + ^ srec_tms ^ "\n\ + \ and domts\t= map (readtm (sign_of thy) iT) " + ^ sdoms ^ "\n\ + \ and intr_tms\t= map (readtm (sign_of thy) propT)\n" + ^ sintrs ^ "\n\ + \ end\n\ + \ end;\n\n\ + \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n (" ^ + stri_name ^ ".rec_tms, " ^ + stri_name ^ ".domts, " ^ + stri_name ^ ".intr_tms)" + , + "structure " ^ big_rec_name ^ " =\n\ + \ struct\n\ + \ val _ = writeln \"" ^ co ^ + "Inductive definition " ^ big_rec_name ^ "\"\n\ + \ structure Result = " ^ co ^ "Ind_section_Fun\n\ + \ (open " ^ stri_name ^ "\n\ + \ val thy\t\t= thy\n\ + \ val monos\t\t= " ^ monos ^ "\n\ + \ val con_defs\t\t= " ^ con_defs ^ "\n\ + \ val type_intrs\t= " ^ type_intrs ^ "\n\ + \ val type_elims\t= " ^ type_elims ^ ");\n\n\ + \ val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\ + \ open Result\n\ + \ end\n" + ) + end + val domains = "domains" $$-- repeat1 (string --$$ "<=" -- !! string) + val ipairs = "intrs" $$-- repeat1 (ident -- !! string) + fun optstring s = optional (s $$-- string) "\"[]\"" >> trim + in domains -- ipairs -- optstring "monos" -- optstring "con_defs" + -- optstring "type_intrs" -- optstring "type_elims" + >> mk_params + end;