# HG changeset patch
# User wenzelm
# Date 924266896 -7200
# Node ID 9bdfe07ba8e98e26e4c225e7671681ef745735f0
# Parent  90eab99706e3d8bd89e88e70a3748d358a8b1d72
'HOL/inductive' theory data;

diff -r 90eab99706e3 -r 9bdfe07ba8e9 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Fri Apr 16 14:43:26 1999 +0200
+++ b/src/HOL/Inductive.thy	Fri Apr 16 14:48:16 1999 +0200
@@ -1,2 +1,6 @@
 
-Inductive = Gfp + Prod + Sum
+Inductive = Gfp + Prod + Sum +
+
+setup InductivePackage.setup
+
+end
diff -r 90eab99706e3 -r 9bdfe07ba8e9 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Apr 16 14:43:26 1999 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Fri Apr 16 14:48:16 1999 +0200
@@ -31,14 +31,19 @@
 signature INDUCTIVE_PACKAGE =
 sig
   val quiet_mode: bool ref
+  val get_inductive: theory -> string ->
+    {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
+      induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
+  val print_inductives: theory -> unit
   val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
     ((bstring * term) * theory attribute list) list -> thm list -> thm list -> theory -> theory *
       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
-       intrs: thm list, mk_cases: string -> thm, mono: thm, unfold:thm}
+       intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
   val add_inductive: bool -> bool -> string list -> ((bstring * string) * Args.src list) list ->
     (xstring * Args.src list) list -> (xstring * Args.src list) list -> theory -> theory *
       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
-       intrs:thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
+       intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
+  val setup: (theory -> theory) list
 end;
 
 structure InductivePackage: INDUCTIVE_PACKAGE =
@@ -140,6 +145,48 @@
 
 
 
+(*** theory data ***)
+
+(* data kind 'HOL/inductive' *)
+
+type inductive_info =
+  {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
+    induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
+
+structure InductiveArgs =
+struct
+  val name = "HOL/inductive";
+  type T = inductive_info Symtab.table;
+
+  val empty = Symtab.empty;
+  val prep_ext = I;
+  val merge: T * T -> T = Symtab.merge (K true);
+
+  fun print sg tab =
+    Pretty.writeln (Pretty.strs ("(co)inductives:" ::
+      map (Sign.cond_extern sg Sign.constK o fst) (Symtab.dest tab)));
+end;
+
+structure InductiveData = TheoryDataFun(InductiveArgs);
+val print_inductives = InductiveData.print;
+
+
+(* get and put data *)
+
+fun get_inductive thy name =
+  (case Symtab.lookup (InductiveData.get thy, name) of
+    Some info => info
+  | None => error ("Unknown (co)inductive set " ^ quote name));
+
+fun put_inductives names info thy =
+  let
+    fun upd (tab, name) = Symtab.update_new ((name, info), tab);
+    val tab = foldl upd (InductiveData.get thy, names)
+      handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
+  in InductiveData.put tab thy end;
+
+
+
 (*** properties of (co)inductive sets ***)
 
 (** elimination rules **)
@@ -578,17 +625,20 @@
     val cTs = map (try' (HOLogic.dest_setT o fastype_of)
       "Recursive component not of type set: " sign) cs;
 
-    val cnames = map (try' (Sign.base_name o fst o dest_Const o head_of)
+    val full_cnames = map (try' (fst o dest_Const o head_of)
       "Recursive set not previously declared as constant: " sign) cs;
+    val cnames = map Sign.base_name full_cnames;
 
     val _ = assert_all Syntax.is_identifier cnames	(* FIXME why? *)
        (fn a => "Base name of recursive set not an identifier: " ^ a);
     val _ = seq (check_rule sign cs o snd o fst) intros;
-  in
-    (if ! quick_and_dirty then add_ind_axm else add_ind_def)
-      verbose declare_consts alt_name coind no_elim no_ind cs intros monos
-      con_defs thy params paramTs cTs cnames
-  end;
+
+    val (thy1, result) =
+      (if ! quick_and_dirty then add_ind_axm else add_ind_def)
+        verbose declare_consts alt_name coind no_elim no_ind cs intros monos
+        con_defs thy params paramTs cTs cnames;
+    val thy2 = thy1 |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result);
+  in (thy2, result) end;
 
 
 
@@ -641,7 +691,14 @@
 
 
 
-(** outer syntax **)
+(** package setup **)
+
+(* setup theory *)
+
+val setup = [InductiveData.init];
+
+
+(* outer syntax *)
 
 local open OuterParse in