Inductive.ML

+(*  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;