# HG changeset patch
# User nipkow
# Date 954438437 -7200
# Node ID 93a11ebacf32aa5915635156a93de7efe9cba413
# Parent  69619f870939253d1ad973810dd867cb86eb6682
If all termination conditions are proved automatically,
the recusrion equations are added to the simpset automatically.

recdef.rules -> recdef.simps

diff -r 69619f870939 -r 93a11ebacf32 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Thu Mar 30 19:45:51 2000 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Thu Mar 30 19:47:17 2000 +0200
@@ -9,13 +9,13 @@
 sig
   val quiet_mode: bool ref
   val print_recdefs: theory -> unit
-  val get_recdef: theory -> string -> {rules: thm list, induct: thm, tcs: term list} option
+  val get_recdef: theory -> string -> {simps: thm list, induct: thm, tcs: term list} option
   val add_recdef: xstring -> string -> string list -> simpset option
     -> (xstring * Args.src list) list -> theory
-    -> theory * {rules: thm list, induct: thm, tcs: term list}
+    -> theory * {simps: thm list, induct: thm, tcs: term list}
   val add_recdef_i: xstring -> term -> term list -> simpset option
     -> (thm * theory attribute list) list
-    -> theory -> theory * {rules: thm list, induct: thm, tcs: term list}
+    -> theory -> theory * {simps: 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
@@ -35,7 +35,7 @@
 
 (* data kind 'HOL/recdef' *)
 
-type recdef_info = {rules: thm list, induct: thm, tcs: term list};
+type recdef_info = {simps: thm list, induct: thm, tcs: term list};
 
 structure RecdefArgs =
 struct
@@ -72,6 +72,13 @@
 
 fun requires_recdef thy = Theory.requires thy "Recdef" "recursive functions";
 
+
+fun prepare_simps no_tcs ixsimps =
+  let val partnd = partition_eq (fn ((_,i),(_,j)) => i=j) ixsimps;
+      val attr = if no_tcs then [Simplifier.simp_add_global] else []
+  in map (fn (rl,i)::rls => ((string_of_int i, rl::map fst rls), attr)) partnd
+  end;
+
 fun gen_add_recdef tfl_fn prep_ss app_thms raw_name R eqs raw_ss raw_congs thy =
   let
     val name = Sign.intern_const (Theory.sign_of thy) raw_name;
@@ -83,13 +90,14 @@
     val ss = (case raw_ss of None => Simplifier.simpset_of thy | Some x => prep_ss x);
     val (thy, congs) = thy |> app_thms raw_congs;
     val (thy, {rules, induct, tcs}) = tfl_fn thy name R (ss, congs) eqs;
+    val named_simps = prepare_simps (null tcs) rules
     val case_numbers = map Library.string_of_int (1 upto Thm.nprems_of induct);
-    val (thy, ([rules], [induct])) =
+    val (thy, (simpss, [induct])) =
       thy
       |> Theory.add_path bname
-      |> PureThy.add_thmss [(("rules", rules), [])]
+      |> PureThy.add_thmss named_simps
       |>>> PureThy.add_thms [(("induct", induct), [RuleCases.case_names case_numbers])];
-    val result = {rules = rules, induct = induct, tcs = tcs};
+    val result = {simps = flat simpss, induct = induct, tcs = tcs};
     val thy =
       thy
       |> put_recdef name result