ZF INDUCTIVE DEFINITIONS: Simplifying the type checking for mutually
recursive datatypes, especially with monotone operators
Inductive_Fun,CoInductive_Fun: deleted as obsolete
inductive_decl: now reads a SINGLE domain for the mutually
recursive construction. This could be a sum, perhaps not! CONCRETE SYNTAX
has changed too (but there are no examples of this to change).
(* Title: ZF/Inductive.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
(Co)Inductive Definitions for Zermelo-Fraenkel Set Theory
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)
val bnd_mono = Const("bnd_mono", [iT,iT-->iT]--->oT)
val bnd_monoI = bnd_monoI
val subs = def_lfp_subset
val Tarski = def_lfp_Tarski
val induct = def_induct
end;
structure Standard_Prod =
struct
val sigma = Const("Sigma", [iT, iT-->iT]--->iT)
val pair = Const("Pair", [iT,iT]--->iT)
val split_const = Const("split", [[iT,iT]--->iT, iT]--->iT)
val fsplit_const = Const("fsplit", [[iT,iT]--->oT, iT]--->oT)
val pair_iff = Pair_iff
val split_eq = split
val fsplitI = fsplitI
val fsplitD = fsplitD
val fsplitE = fsplitE
end;
structure Standard_Sum =
struct
val sum = Const("op +", [iT,iT]--->iT)
val inl = Const("Inl", iT-->iT)
val inr = Const("Inr", iT-->iT)
val elim = Const("case", [iT-->iT, iT-->iT, iT]--->iT)
val case_inl = case_Inl
val case_inr = case_Inr
val inl_iff = Inl_iff
val inr_iff = Inr_iff
val distinct = Inl_Inr_iff
val distinct' = Inr_Inl_iff
end;
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 Inductive=Inductive and Fp=Lfp and
Pr=Standard_Prod and Su=Standard_Sum);
structure Indrule =
Indrule_Fun (structure Inductive=Inductive and
Pr=Standard_Prod and Su=Standard_Sum 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);
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 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 ((((((rec_tms, sdom_sum), ipairs),
monos), con_defs), type_intrs), type_elims) =
let val big_rec_name = space_implode "_"
(map (scan_to_id o trim) rec_tms)
and srec_tms = mk_list rec_tms
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 _ = writeln \"" ^ co ^
"Inductive definition " ^ big_rec_name ^ "\"\n\
\ val rec_tms\t= map (readtm (sign_of thy) iT) "
^ srec_tms ^ "\n\
\ and dom_sum\t= readtm (sign_of thy) iT " ^ sdom_sum ^ "\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 ^ ".dom_sum, " ^
stri_name ^ ".intr_tms)"
,
"structure " ^ big_rec_name ^ " =\n\
\ struct\n\
\ val _ = writeln \"Proofs for " ^ 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" $$-- enum1 "+" 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;