peoper defer_recdef interface;
authorwenzelm
Fri Apr 30 18:10:35 1999 +0200 (1999-04-30)
changeset 6557d7e7532c128a
parent 6556 daa00919502b
child 6558 120ff48e8618
peoper defer_recdef interface;
src/HOL/Tools/recdef_package.ML
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Fri Apr 30 18:10:03 1999 +0200
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Fri Apr 30 18:10:35 1999 +0200
     1.3 @@ -16,6 +16,10 @@
     1.4    val add_recdef_i: xstring -> term -> ((bstring * term) * theory attribute list) list
     1.5      -> simpset option -> (thm * theory attribute list) list
     1.6      -> theory -> theory * {rules: thm list, induct: thm, tcs: term list}
     1.7 +  val defer_recdef: xstring -> string list -> (xstring * Args.src list) list
     1.8 +    -> theory -> theory * {induct_rules: thm}
     1.9 +  val defer_recdef_i: xstring -> term list -> (thm * theory attribute list) list
    1.10 +    -> theory -> theory * {induct_rules: thm}
    1.11    val setup: (theory -> theory) list
    1.12  end;
    1.13  
    1.14 @@ -39,6 +43,7 @@
    1.15    type T = recdef_info Symtab.table;
    1.16  
    1.17    val empty = Symtab.empty;
    1.18 +  val copy = I;
    1.19    val prep_ext = I;
    1.20    val merge: T * T -> T = Symtab.merge (K true);
    1.21  
    1.22 @@ -68,19 +73,21 @@
    1.23  
    1.24  (** add_recdef(_i) **)
    1.25  
    1.26 -fun gen_add_recdef tfl_def prep_att prep_ss app_thms raw_name R eq_srcs raw_ss raw_congs thy =
    1.27 +fun requires_recdef thy = Theory.requires thy "Recdef" "recursive functions";
    1.28 +
    1.29 +fun gen_add_recdef tfl_fn prep_att prep_ss app_thms raw_name R eq_srcs raw_ss raw_congs thy =
    1.30    let
    1.31      val name = Sign.intern_const (Theory.sign_of thy) raw_name;
    1.32      val bname = Sign.base_name name;
    1.33  
    1.34 -    val _ = Theory.requires thy "Recdef" "recursive function definitions";
    1.35 +    val _ = requires_recdef thy;
    1.36      val _ = message ("Defining recursive function " ^ quote name ^ " ...");
    1.37  
    1.38      val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
    1.39      val eq_atts = map (map (prep_att thy)) raw_eq_atts;
    1.40      val ss = (case raw_ss of None => Simplifier.simpset_of thy | Some x => prep_ss x);
    1.41      val (thy1, congs) = thy |> app_thms raw_congs;
    1.42 -    val (thy2, pats) = tfl_def thy1 name R eqs;
    1.43 +    val (thy2, pats) = tfl_fn thy1 name R eqs;
    1.44      val (result as {rules, induct, tcs}) = Tfl.simplify_defn (ss, congs) (thy2, (name, pats));
    1.45      val thy3 =
    1.46        thy2
    1.47 @@ -97,6 +104,31 @@
    1.48  val add_recdef_i = gen_add_recdef Tfl.define_i (K I) I IsarThy.apply_theorems_i;
    1.49  
    1.50  
    1.51 +
    1.52 +(** defer_recdef(_i) **)
    1.53 +
    1.54 +fun gen_defer_recdef tfl_fn app_thms raw_name eqs raw_congs thy =
    1.55 +  let
    1.56 +    val name = Sign.intern_const (Theory.sign_of thy) raw_name;
    1.57 +    val bname = Sign.base_name name;
    1.58 +
    1.59 +    val _ = requires_recdef thy;
    1.60 +    val _ = message ("Deferred recursive function " ^ quote name ^ " ...");
    1.61 +
    1.62 +    val (thy1, congs) = thy |> app_thms raw_congs;
    1.63 +    val (thy2, induct_rules) = tfl_fn thy1 name congs eqs;
    1.64 +    val thy3 =
    1.65 +      thy2
    1.66 +      |> Theory.add_path bname
    1.67 +      |> PureThy.add_thms [(("induct_rules", induct_rules), [])]
    1.68 +      |> Theory.parent_path;
    1.69 +  in (thy3, {induct_rules = induct_rules}) end;
    1.70 +
    1.71 +val defer_recdef = gen_defer_recdef Tfl.defer IsarThy.apply_theorems;
    1.72 +val defer_recdef_i = gen_defer_recdef Tfl.defer_i IsarThy.apply_theorems_i;
    1.73 +
    1.74 +
    1.75 +
    1.76  (** package setup **)
    1.77  
    1.78  (* setup theory *)
    1.79 @@ -118,8 +150,18 @@
    1.80    OuterSyntax.command "recdef" "define general recursive functions (TFL)"
    1.81      (recdef_decl >> Toplevel.theory);
    1.82  
    1.83 +
    1.84 +val defer_recdef_decl =
    1.85 +  name -- Scan.repeat1 term --
    1.86 +  Scan.optional ($$$ "(" |-- $$$ "congs" |-- !!! (xthms1 --| $$$ ")")) []
    1.87 +  >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
    1.88 +
    1.89 +val defer_recdefP =
    1.90 +  OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)"
    1.91 +    (defer_recdef_decl >> Toplevel.theory);
    1.92 +
    1.93  val _ = OuterSyntax.add_keywords ["congs", "simpset"];
    1.94 -val _ = OuterSyntax.add_parsers [recdefP];
    1.95 +val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP];
    1.96  
    1.97  end;
    1.98