--- 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;