(* Title: HOL/inductive.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
(Co)Inductive Definitions for HOL
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
fun gen_fp_oper a (X,T,t) =
let val setT = mk_set T
in Const(a, (setT-->setT)-->setT) $ absfree(X, setT, t) end;
structure Lfp_items =
struct
val oper = gen_fp_oper "lfp"
val Tarski = def_lfp_Tarski
val induct = def_induct
end;
structure Gfp_items =
struct
val oper = gen_fp_oper "gfp"
val Tarski = def_gfp_Tarski
val induct = def_Collect_coinduct
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_items);
structure Indrule = Indrule_Fun
(structure Inductive=Inductive and Intr_elim=Intr_elim);
open Intr_elim Indrule
end;
structure Ind = Add_inductive_def_Fun (Lfp_items);
signature INDUCTIVE_STRING =
sig
val thy_name : string (*name of the new theory*)
val srec_tms : string list (*recursion terms*)
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 termTVar) srec_tms
and intr_tms = map (readtm sign propT) sintrs;
val thy = thy |> Ind.add_fp_def_i(rec_tms, intr_tms)
|> add_thyname thy_name);
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_items);
open Intr_elim
val coinduct = raw_induct
end;
structure CoInd = Add_inductive_def_Fun(Gfp_items);
(*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 (((recs, ipairs), monos), con_defs) =
let val big_rec_name = space_implode "_" (map (scan_to_id o trim) recs)
and srec_tms = mk_list recs
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) termTVar) "
^ srec_tms ^ "\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 ^ ".intr_tms)"
,
"structure " ^ big_rec_name ^ " =\n\
\ struct\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\n\
\ val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
\ open Result\n\
\ end\n"
)
end
val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
in repeat1 string -- ipairs -- optstring "monos" -- optstring "con_defs"
>> mk_params
end;