diff -r d9527f97246e -r 89669c58e506 Inductive.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Inductive.ML Thu Aug 25 11:01:45 1994 +0200 @@ -0,0 +1,141 @@ +(* 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;