--- a/Inductive.ML Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,94 +0,0 @@
-(* 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_setT 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);