# HG changeset patch
# User wenzelm
# Date 954613299 -7200
# Node ID b9475dad85ed5ebd09b2fdd59a70a9d3f542a5bb
# Parent  1062572b5b3700082eceaccc64805df97b10db85
recdef: admit names/atts;

diff -r 1062572b5b37 -r b9475dad85ed doc-src/IsarRef/hol.tex
--- a/doc-src/IsarRef/hol.tex	Sat Apr 01 20:18:52 2000 +0200
+++ b/doc-src/IsarRef/hol.tex	Sat Apr 01 20:21:39 2000 +0200
@@ -129,9 +129,14 @@
 \end{matharray}
 
 \begin{rail}
-  'primrec' parname? (thmdecl? prop comment? + )
+  'primrec' parname? (equation + )
+  ;
+  'recdef' name term (equation +) hints
   ;
-  'recdef' name term (term comment? +) \\ ('congs' thmrefs)? ('simpset' name)?
+
+  equation: thmdecl? prop comment?
+  ;
+  hints: ('congs' thmrefs)? ('simpset' name)?
   ;
 \end{rail}
 
@@ -149,6 +154,12 @@
 $\isarkeyword{primrec}$ are that of the datatypes involved, while those of
 $\isarkeyword{recdef}$ are numbered (starting from $1$).
 
+The equations provided by these packages may be referred later as theorem list
+$f\mathord.simps$, where $f$ is the (collective) name of the functions
+defined.  Individual equations may be named explicitly as well; note that for
+$\isarkeyword{recdef}$ each specification given by the user may result in
+several theorems.
+
 See \cite{isabelle-HOL} for further information on recursive function
 definitions in HOL.
 
diff -r 1062572b5b37 -r b9475dad85ed src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Sat Apr 01 20:18:52 2000 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Sat Apr 01 20:21:39 2000 +0200
@@ -9,13 +9,14 @@
 sig
   val quiet_mode: bool ref
   val print_recdefs: theory -> unit
-  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 * {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 * {simps: thm list, induct: thm, tcs: term list}
+  val get_recdef: theory -> string
+    -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
+  val add_recdef: xstring -> string -> ((bstring * string) * Args.src list) list
+    -> simpset option -> (xstring * Args.src list) list -> theory
+    -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
+  val add_recdef_i: xstring -> term -> ((bstring * term) * theory attribute list) list
+    -> simpset option -> (thm * theory attribute list) list
+    -> theory -> theory * {simps: thm list, rules: thm list 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 +36,7 @@
 
 (* data kind 'HOL/recdef' *)
 
-type recdef_info = {simps: thm list, induct: thm, tcs: term list};
+type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list};
 
 structure RecdefArgs =
 struct
@@ -72,14 +73,7 @@
 
 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 =
+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;
@@ -87,27 +81,32 @@
     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 (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 (thy, {rules = rules_idx, induct, tcs}) = tfl_fn thy name R (ss, congs) eqs;
+    val rules = map (map #1) (Library.partition_eq Library.eq_snd rules_idx);
+    val simp_att = if null tcs then [Simplifier.simp_add_global] else [];
+
     val case_numbers = map Library.string_of_int (1 upto Thm.nprems_of induct);
-    val (thy, (simpss, [induct])) =
+    val (thy, (simps' :: rules', [induct'])) =
       thy
       |> Theory.add_path bname
-      |> PureThy.add_thmss named_simps
+      |> PureThy.add_thmss ((("simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
       |>>> PureThy.add_thms [(("induct", induct), [RuleCases.case_names case_numbers])];
-    val result = {simps = flat simpss, induct = induct, tcs = tcs};
+    val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
     val thy =
       thy
       |> put_recdef name result
       |> Theory.parent_path;
   in (thy, result) end;
 
-val add_recdef = gen_add_recdef Tfl.define I IsarThy.apply_theorems;
-val add_recdef_x = gen_add_recdef Tfl.define (Simplifier.simpset_of o ThyInfo.get_theory)
-  IsarThy.apply_theorems;
-val add_recdef_i = gen_add_recdef Tfl.define_i I IsarThy.apply_theorems_i;
+val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute I IsarThy.apply_theorems;
+val add_recdef_x = gen_add_recdef Tfl.define Attrib.global_attribute
+  (Simplifier.simpset_of o ThyInfo.get_theory) IsarThy.apply_theorems;
+val add_recdef_i = gen_add_recdef Tfl.define_i (K I) I IsarThy.apply_theorems_i;
 
 
 
@@ -147,10 +146,10 @@
 local structure P = OuterParse and K = OuterSyntax.Keyword in
 
 val recdef_decl =
-  P.name -- P.term -- Scan.repeat1 (P.term --| P.marg_comment) --
+  P.name -- P.term -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment) --
   Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) [] --
   Scan.option (P.$$$ "(" |-- P.$$$ "simpset" |-- P.!!! (P.name --| P.$$$ ")"))
-  >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef_x f R eqs ss congs);
+  >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef_x f R (map P.triple_swap eqs) ss congs);
 
 val recdefP =
   OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl
@@ -158,7 +157,7 @@
 
 
 val defer_recdef_decl =
-  P.name -- Scan.repeat1 P.term --
+  P.name -- Scan.repeat1 P.prop --
   Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) []
   >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
 
diff -r 1062572b5b37 -r b9475dad85ed src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Sat Apr 01 20:18:52 2000 +0200
+++ b/src/HOL/thy_syntax.ML	Sat Apr 01 20:21:39 2000 +0200
@@ -193,19 +193,17 @@
 
 (** primrec **)
 
+fun mk_patterns eqns = mk_list (map (fn (s, _) => if s = "" then "_" else s) eqns);
+fun mk_eqns eqns = mk_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) eqns);
+
 fun mk_primrec_decl (alt_name, eqns) =
-  let
-    val names = map (fn (s, _) => if s = "" then "_" else s) eqns
-  in
-    ";\nval (thy, " ^ mk_list names ^ ") = PrimrecPackage.add_primrec " ^ alt_name ^ " " ^
-    mk_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) eqns) ^
-    " " ^ " thy;\n\
-    \val thy = thy\n"
-  end;
+  ";\nval (thy, " ^ mk_patterns eqns ^ ") = PrimrecPackage.add_primrec " ^ alt_name ^ " "
+  ^ mk_eqns eqns ^ " " ^ " thy;\n\
+  \val thy = thy\n"
 
 (* either names and axioms or just axioms *)
-val primrec_decl = (optional ("(" $$-- name --$$ ")") "\"\"" --
-  (repeat1 ((ident -- string) || (string >> pair "")))) >> mk_primrec_decl;
+val primrec_decl = optional ("(" $$-- name --$$ ")") "\"\"" --
+  repeat1 (ident -- string || (string >> pair "")) >> mk_primrec_decl;
 
 
 (*** recdef: interface to Slind's TFL ***)
@@ -213,21 +211,20 @@
 (** TFL with explicit WF relations **)
 
 (*fname: name of function being defined; rel: well-founded relation*)
-fun mk_recdef_decl ((((fname, rel), congs), ss), axms) =
+fun mk_recdef_decl ((((fname, rel), congs), ss), eqns) =
   let
     val fid = unenclose fname;
     val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
-    val axms_text = mk_big_list axms;
   in
     ";\n\n\
     \local\n\
     \fun simpset() = Simplifier.simpset_of thy;\n\
     \val (thy, result) = thy |> RecdefPackage.add_recdef " ^ quote fid ^ " " ^ rel ^ "\n" ^
-    axms_text ^ "\n(Some (" ^ ss ^ "))\n" ^ congs_text ^ ";\n\
+    mk_eqns eqns ^ "\n(Some (" ^ ss ^ "))\n" ^ congs_text ^ ";\n\
     \in\n\
     \structure " ^ fid ^ " =\n\
     \struct\n\
-    \  val {simps, induct, tcs} = result;\n\
+    \  val {simps, rules = " ^ mk_patterns eqns ^ ", induct, tcs} = result;\n\
     \end;\n\
     \val thy = thy;\n\
     \end;\n\
@@ -235,10 +232,10 @@
   end;
 
 val recdef_decl =
-  (name -- string --
+  name -- string --
     optional ("congs" $$-- list1 name) [] --
     optional ("simpset" $$-- string >> unenclose) "simpset()" --
-    repeat1 string >> mk_recdef_decl);
+    repeat1 (ident -- string || (string >> pair "")) >> mk_recdef_decl;
 
 
 (** TFL with no WF relation supplied **)