peoper defer_recdef interface;

--- a/src/HOL/Tools/recdef_package.ML	Fri Apr 30 18:10:03 1999 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Fri Apr 30 18:10:35 1999 +0200
@@ -16,6 +16,10 @@
   val add_recdef_i: xstring -> term -> ((bstring * term) * theory attribute list) list
     -> simpset option -> (thm * theory attribute list) list
     -> theory -> theory * {rules: thm list, induct: thm, tcs: term list}
+  val defer_recdef: xstring -> string list -> (xstring * Args.src list) list
+    -> theory -> theory * {induct_rules: thm}
+  val defer_recdef_i: xstring -> term list -> (thm * theory attribute list) list
+    -> theory -> theory * {induct_rules: thm}
   val setup: (theory -> theory) list
 end;
 
@@ -39,6 +43,7 @@
   type T = recdef_info Symtab.table;
 
   val empty = Symtab.empty;
+  val copy = I;
   val prep_ext = I;
   val merge: T * T -> T = Symtab.merge (K true);
 
@@ -68,19 +73,21 @@
 
 (** add_recdef(_i) **)
 
-fun gen_add_recdef tfl_def prep_att prep_ss app_thms raw_name R eq_srcs raw_ss raw_congs thy =
+fun requires_recdef thy = Theory.requires thy "Recdef" "recursive functions";
+
+fun gen_add_recdef tfl_fn prep_att prep_ss app_thms raw_name R eq_srcs raw_ss raw_congs thy =
   let
     val name = Sign.intern_const (Theory.sign_of thy) raw_name;
     val bname = Sign.base_name name;
 
-    val _ = Theory.requires thy "Recdef" "recursive function definitions";
+    val _ = requires_recdef thy;
     val _ = message ("Defining recursive function " ^ quote name ^ " ...");
 
     val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
     val eq_atts = map (map (prep_att thy)) raw_eq_atts;
     val ss = (case raw_ss of None => Simplifier.simpset_of thy | Some x => prep_ss x);
     val (thy1, congs) = thy |> app_thms raw_congs;
-    val (thy2, pats) = tfl_def thy1 name R eqs;
+    val (thy2, pats) = tfl_fn thy1 name R eqs;
     val (result as {rules, induct, tcs}) = Tfl.simplify_defn (ss, congs) (thy2, (name, pats));
     val thy3 =
       thy2
@@ -97,6 +104,31 @@
 val add_recdef_i = gen_add_recdef Tfl.define_i (K I) I IsarThy.apply_theorems_i;
 
 
+
+(** defer_recdef(_i) **)
+
+fun gen_defer_recdef tfl_fn app_thms raw_name eqs raw_congs thy =
+  let
+    val name = Sign.intern_const (Theory.sign_of thy) raw_name;
+    val bname = Sign.base_name name;
+
+    val _ = requires_recdef thy;
+    val _ = message ("Deferred recursive function " ^ quote name ^ " ...");
+
+    val (thy1, congs) = thy |> app_thms raw_congs;
+    val (thy2, induct_rules) = tfl_fn thy1 name congs eqs;
+    val thy3 =
+      thy2
+      |> Theory.add_path bname
+      |> PureThy.add_thms [(("induct_rules", induct_rules), [])]
+      |> Theory.parent_path;
+  in (thy3, {induct_rules = induct_rules}) end;
+
+val defer_recdef = gen_defer_recdef Tfl.defer IsarThy.apply_theorems;
+val defer_recdef_i = gen_defer_recdef Tfl.defer_i IsarThy.apply_theorems_i;
+
+
+
 (** package setup **)
 
 (* setup theory *)
@@ -118,8 +150,18 @@
   OuterSyntax.command "recdef" "define general recursive functions (TFL)"
     (recdef_decl >> Toplevel.theory);
 
+
+val defer_recdef_decl =
+  name -- Scan.repeat1 term --
+  Scan.optional ($$$ "(" |-- $$$ "congs" |-- !!! (xthms1 --| $$$ ")")) []
+  >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
+
+val defer_recdefP =
+  OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)"
+    (defer_recdef_decl >> Toplevel.theory);
+
 val _ = OuterSyntax.add_keywords ["congs", "simpset"];
-val _ = OuterSyntax.add_parsers [recdefP];
+val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP];
 
 end;