recdef: admit names/atts;
authorwenzelm
Sat Apr 01 20:21:39 2000 +0200 (2000-04-01)
changeset 8657b9475dad85ed
parent 8656 1062572b5b37
child 8658 3cf533397c5a
recdef: admit names/atts;
doc-src/IsarRef/hol.tex
src/HOL/Tools/recdef_package.ML
src/HOL/thy_syntax.ML
     1.1 --- a/doc-src/IsarRef/hol.tex	Sat Apr 01 20:18:52 2000 +0200
     1.2 +++ b/doc-src/IsarRef/hol.tex	Sat Apr 01 20:21:39 2000 +0200
     1.3 @@ -129,9 +129,14 @@
     1.4  \end{matharray}
     1.5  
     1.6  \begin{rail}
     1.7 -  'primrec' parname? (thmdecl? prop comment? + )
     1.8 +  'primrec' parname? (equation + )
     1.9 +  ;
    1.10 +  'recdef' name term (equation +) hints
    1.11    ;
    1.12 -  'recdef' name term (term comment? +) \\ ('congs' thmrefs)? ('simpset' name)?
    1.13 +
    1.14 +  equation: thmdecl? prop comment?
    1.15 +  ;
    1.16 +  hints: ('congs' thmrefs)? ('simpset' name)?
    1.17    ;
    1.18  \end{rail}
    1.19  
    1.20 @@ -149,6 +154,12 @@
    1.21  $\isarkeyword{primrec}$ are that of the datatypes involved, while those of
    1.22  $\isarkeyword{recdef}$ are numbered (starting from $1$).
    1.23  
    1.24 +The equations provided by these packages may be referred later as theorem list
    1.25 +$f\mathord.simps$, where $f$ is the (collective) name of the functions
    1.26 +defined.  Individual equations may be named explicitly as well; note that for
    1.27 +$\isarkeyword{recdef}$ each specification given by the user may result in
    1.28 +several theorems.
    1.29 +
    1.30  See \cite{isabelle-HOL} for further information on recursive function
    1.31  definitions in HOL.
    1.32  
     2.1 --- a/src/HOL/Tools/recdef_package.ML	Sat Apr 01 20:18:52 2000 +0200
     2.2 +++ b/src/HOL/Tools/recdef_package.ML	Sat Apr 01 20:21:39 2000 +0200
     2.3 @@ -9,13 +9,14 @@
     2.4  sig
     2.5    val quiet_mode: bool ref
     2.6    val print_recdefs: theory -> unit
     2.7 -  val get_recdef: theory -> string -> {simps: thm list, induct: thm, tcs: term list} option
     2.8 -  val add_recdef: xstring -> string -> string list -> simpset option
     2.9 -    -> (xstring * Args.src list) list -> theory
    2.10 -    -> theory * {simps: thm list, induct: thm, tcs: term list}
    2.11 -  val add_recdef_i: xstring -> term -> term list -> simpset option
    2.12 -    -> (thm * theory attribute list) list
    2.13 -    -> theory -> theory * {simps: thm list, induct: thm, tcs: term list}
    2.14 +  val get_recdef: theory -> string
    2.15 +    -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
    2.16 +  val add_recdef: xstring -> string -> ((bstring * string) * Args.src list) list
    2.17 +    -> simpset option -> (xstring * Args.src list) list -> theory
    2.18 +    -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    2.19 +  val add_recdef_i: xstring -> term -> ((bstring * term) * theory attribute list) list
    2.20 +    -> simpset option -> (thm * theory attribute list) list
    2.21 +    -> theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    2.22    val defer_recdef: xstring -> string list -> (xstring * Args.src list) list
    2.23      -> theory -> theory * {induct_rules: thm}
    2.24    val defer_recdef_i: xstring -> term list -> (thm * theory attribute list) list
    2.25 @@ -35,7 +36,7 @@
    2.26  
    2.27  (* data kind 'HOL/recdef' *)
    2.28  
    2.29 -type recdef_info = {simps: thm list, induct: thm, tcs: term list};
    2.30 +type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list};
    2.31  
    2.32  structure RecdefArgs =
    2.33  struct
    2.34 @@ -72,14 +73,7 @@
    2.35  
    2.36  fun requires_recdef thy = Theory.requires thy "Recdef" "recursive functions";
    2.37  
    2.38 -
    2.39 -fun prepare_simps no_tcs ixsimps =
    2.40 -  let val partnd = partition_eq (fn ((_,i),(_,j)) => i=j) ixsimps;
    2.41 -      val attr = if no_tcs then [Simplifier.simp_add_global] else []
    2.42 -  in map (fn (rl,i)::rls => ((string_of_int i, rl::map fst rls), attr)) partnd
    2.43 -  end;
    2.44 -
    2.45 -fun gen_add_recdef tfl_fn prep_ss app_thms raw_name R eqs raw_ss raw_congs thy =
    2.46 +fun gen_add_recdef tfl_fn prep_att prep_ss app_thms raw_name R eq_srcs raw_ss raw_congs thy =
    2.47    let
    2.48      val name = Sign.intern_const (Theory.sign_of thy) raw_name;
    2.49      val bname = Sign.base_name name;
    2.50 @@ -87,27 +81,32 @@
    2.51      val _ = requires_recdef thy;
    2.52      val _ = message ("Defining recursive function " ^ quote name ^ " ...");
    2.53  
    2.54 +    val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
    2.55 +    val eq_atts = map (map (prep_att thy)) raw_eq_atts;
    2.56      val ss = (case raw_ss of None => Simplifier.simpset_of thy | Some x => prep_ss x);
    2.57      val (thy, congs) = thy |> app_thms raw_congs;
    2.58 -    val (thy, {rules, induct, tcs}) = tfl_fn thy name R (ss, congs) eqs;
    2.59 -    val named_simps = prepare_simps (null tcs) rules
    2.60 +
    2.61 +    val (thy, {rules = rules_idx, induct, tcs}) = tfl_fn thy name R (ss, congs) eqs;
    2.62 +    val rules = map (map #1) (Library.partition_eq Library.eq_snd rules_idx);
    2.63 +    val simp_att = if null tcs then [Simplifier.simp_add_global] else [];
    2.64 +
    2.65      val case_numbers = map Library.string_of_int (1 upto Thm.nprems_of induct);
    2.66 -    val (thy, (simpss, [induct])) =
    2.67 +    val (thy, (simps' :: rules', [induct'])) =
    2.68        thy
    2.69        |> Theory.add_path bname
    2.70 -      |> PureThy.add_thmss named_simps
    2.71 +      |> PureThy.add_thmss ((("simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
    2.72        |>>> PureThy.add_thms [(("induct", induct), [RuleCases.case_names case_numbers])];
    2.73 -    val result = {simps = flat simpss, induct = induct, tcs = tcs};
    2.74 +    val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
    2.75      val thy =
    2.76        thy
    2.77        |> put_recdef name result
    2.78        |> Theory.parent_path;
    2.79    in (thy, result) end;
    2.80  
    2.81 -val add_recdef = gen_add_recdef Tfl.define I IsarThy.apply_theorems;
    2.82 -val add_recdef_x = gen_add_recdef Tfl.define (Simplifier.simpset_of o ThyInfo.get_theory)
    2.83 -  IsarThy.apply_theorems;
    2.84 -val add_recdef_i = gen_add_recdef Tfl.define_i I IsarThy.apply_theorems_i;
    2.85 +val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute I IsarThy.apply_theorems;
    2.86 +val add_recdef_x = gen_add_recdef Tfl.define Attrib.global_attribute
    2.87 +  (Simplifier.simpset_of o ThyInfo.get_theory) IsarThy.apply_theorems;
    2.88 +val add_recdef_i = gen_add_recdef Tfl.define_i (K I) I IsarThy.apply_theorems_i;
    2.89  
    2.90  
    2.91  
    2.92 @@ -147,10 +146,10 @@
    2.93  local structure P = OuterParse and K = OuterSyntax.Keyword in
    2.94  
    2.95  val recdef_decl =
    2.96 -  P.name -- P.term -- Scan.repeat1 (P.term --| P.marg_comment) --
    2.97 +  P.name -- P.term -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment) --
    2.98    Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) [] --
    2.99    Scan.option (P.$$$ "(" |-- P.$$$ "simpset" |-- P.!!! (P.name --| P.$$$ ")"))
   2.100 -  >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef_x f R eqs ss congs);
   2.101 +  >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef_x f R (map P.triple_swap eqs) ss congs);
   2.102  
   2.103  val recdefP =
   2.104    OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl
   2.105 @@ -158,7 +157,7 @@
   2.106  
   2.107  
   2.108  val defer_recdef_decl =
   2.109 -  P.name -- Scan.repeat1 P.term --
   2.110 +  P.name -- Scan.repeat1 P.prop --
   2.111    Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) []
   2.112    >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
   2.113  
     3.1 --- a/src/HOL/thy_syntax.ML	Sat Apr 01 20:18:52 2000 +0200
     3.2 +++ b/src/HOL/thy_syntax.ML	Sat Apr 01 20:21:39 2000 +0200
     3.3 @@ -193,19 +193,17 @@
     3.4  
     3.5  (** primrec **)
     3.6  
     3.7 +fun mk_patterns eqns = mk_list (map (fn (s, _) => if s = "" then "_" else s) eqns);
     3.8 +fun mk_eqns eqns = mk_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) eqns);
     3.9 +
    3.10  fun mk_primrec_decl (alt_name, eqns) =
    3.11 -  let
    3.12 -    val names = map (fn (s, _) => if s = "" then "_" else s) eqns
    3.13 -  in
    3.14 -    ";\nval (thy, " ^ mk_list names ^ ") = PrimrecPackage.add_primrec " ^ alt_name ^ " " ^
    3.15 -    mk_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) eqns) ^
    3.16 -    " " ^ " thy;\n\
    3.17 -    \val thy = thy\n"
    3.18 -  end;
    3.19 +  ";\nval (thy, " ^ mk_patterns eqns ^ ") = PrimrecPackage.add_primrec " ^ alt_name ^ " "
    3.20 +  ^ mk_eqns eqns ^ " " ^ " thy;\n\
    3.21 +  \val thy = thy\n"
    3.22  
    3.23  (* either names and axioms or just axioms *)
    3.24 -val primrec_decl = (optional ("(" $$-- name --$$ ")") "\"\"" --
    3.25 -  (repeat1 ((ident -- string) || (string >> pair "")))) >> mk_primrec_decl;
    3.26 +val primrec_decl = optional ("(" $$-- name --$$ ")") "\"\"" --
    3.27 +  repeat1 (ident -- string || (string >> pair "")) >> mk_primrec_decl;
    3.28  
    3.29  
    3.30  (*** recdef: interface to Slind's TFL ***)
    3.31 @@ -213,21 +211,20 @@
    3.32  (** TFL with explicit WF relations **)
    3.33  
    3.34  (*fname: name of function being defined; rel: well-founded relation*)
    3.35 -fun mk_recdef_decl ((((fname, rel), congs), ss), axms) =
    3.36 +fun mk_recdef_decl ((((fname, rel), congs), ss), eqns) =
    3.37    let
    3.38      val fid = unenclose fname;
    3.39      val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
    3.40 -    val axms_text = mk_big_list axms;
    3.41    in
    3.42      ";\n\n\
    3.43      \local\n\
    3.44      \fun simpset() = Simplifier.simpset_of thy;\n\
    3.45      \val (thy, result) = thy |> RecdefPackage.add_recdef " ^ quote fid ^ " " ^ rel ^ "\n" ^
    3.46 -    axms_text ^ "\n(Some (" ^ ss ^ "))\n" ^ congs_text ^ ";\n\
    3.47 +    mk_eqns eqns ^ "\n(Some (" ^ ss ^ "))\n" ^ congs_text ^ ";\n\
    3.48      \in\n\
    3.49      \structure " ^ fid ^ " =\n\
    3.50      \struct\n\
    3.51 -    \  val {simps, induct, tcs} = result;\n\
    3.52 +    \  val {simps, rules = " ^ mk_patterns eqns ^ ", induct, tcs} = result;\n\
    3.53      \end;\n\
    3.54      \val thy = thy;\n\
    3.55      \end;\n\
    3.56 @@ -235,10 +232,10 @@
    3.57    end;
    3.58  
    3.59  val recdef_decl =
    3.60 -  (name -- string --
    3.61 +  name -- string --
    3.62      optional ("congs" $$-- list1 name) [] --
    3.63      optional ("simpset" $$-- string >> unenclose) "simpset()" --
    3.64 -    repeat1 string >> mk_recdef_decl);
    3.65 +    repeat1 (ident -- string || (string >> pair "")) >> mk_recdef_decl;
    3.66  
    3.67  
    3.68  (** TFL with no WF relation supplied **)