Inductive.ML

added IOA to isabelle/HOL

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