src/HOL/Tools/recdef_package.ML
author wenzelm
Mon Mar 13 13:18:59 2000 +0100 (2000-03-13)
changeset 8430 dbd897e0d804
parent 7798 42e94b618f34
child 8481 89d498a8d3f6
permissions -rw-r--r--
adapted to new PureThy.add_thms etc.;
number cases;
     1 (*  Title:      HOL/Tools/recdef_package.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Wrapper module for Konrad Slind's TFL package.
     6 *)
     7 
     8 signature RECDEF_PACKAGE =
     9 sig
    10   val quiet_mode: bool ref
    11   val print_recdefs: theory -> unit
    12   val get_recdef: theory -> string -> {rules: thm list, induct: thm, tcs: term list}
    13   val add_recdef: xstring -> string -> string list -> simpset option
    14     -> (xstring * Args.src list) list -> theory
    15     -> theory * {rules: thm list, induct: thm, tcs: term list}
    16   val add_recdef_i: xstring -> term -> term list -> simpset option
    17     -> (thm * theory attribute list) list
    18     -> theory -> theory * {rules: thm list, induct: thm, tcs: term list}
    19   val defer_recdef: xstring -> string list -> (xstring * Args.src list) list
    20     -> theory -> theory * {induct_rules: thm}
    21   val defer_recdef_i: xstring -> term list -> (thm * theory attribute list) list
    22     -> theory -> theory * {induct_rules: thm}
    23   val setup: (theory -> theory) list
    24 end;
    25 
    26 structure RecdefPackage: RECDEF_PACKAGE =
    27 struct
    28 
    29 val quiet_mode = Tfl.quiet_mode;
    30 val message = Tfl.message;
    31 
    32 
    33 
    34 (** theory data **)
    35 
    36 (* data kind 'HOL/recdef' *)
    37 
    38 type recdef_info = {rules: thm list, induct: thm, tcs: term list};
    39 
    40 structure RecdefArgs =
    41 struct
    42   val name = "HOL/recdef";
    43   type T = recdef_info Symtab.table;
    44 
    45   val empty = Symtab.empty;
    46   val copy = I;
    47   val prep_ext = I;
    48   val merge: T * T -> T = Symtab.merge (K true);
    49 
    50   fun print sg tab =
    51     Pretty.writeln (Pretty.strs ("recdefs:" ::
    52       map #1 (Sign.cond_extern_table sg Sign.constK tab)));
    53 end;
    54 
    55 structure RecdefData = TheoryDataFun(RecdefArgs);
    56 val print_recdefs = RecdefData.print;
    57 
    58 
    59 (* get and put data *)
    60 
    61 fun get_recdef thy name =
    62   (case Symtab.lookup (RecdefData.get thy, name) of
    63     Some info => info
    64   | None => error ("Unknown recursive function " ^ quote name));
    65 
    66 fun put_recdef name info thy =
    67   let
    68     val tab = Symtab.update_new ((name, info), RecdefData.get thy)
    69       handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name);
    70   in RecdefData.put tab thy end;
    71 
    72 
    73 
    74 (** add_recdef(_i) **)
    75 
    76 fun requires_recdef thy = Theory.requires thy "Recdef" "recursive functions";
    77 
    78 fun gen_add_recdef tfl_fn prep_ss app_thms raw_name R eqs raw_ss raw_congs thy =
    79   let
    80     val name = Sign.intern_const (Theory.sign_of thy) raw_name;
    81     val bname = Sign.base_name name;
    82 
    83     val _ = requires_recdef thy;
    84     val _ = message ("Defining recursive function " ^ quote name ^ " ...");
    85 
    86     val ss = (case raw_ss of None => Simplifier.simpset_of thy | Some x => prep_ss x);
    87     val (thy, congs) = thy |> app_thms raw_congs;
    88     val (thy, {rules, induct, tcs}) = tfl_fn thy name R (ss, congs) eqs;
    89     val case_numbers = map Library.string_of_int (1 upto Thm.nprems_of induct);
    90     val (thy, ([rules], [induct])) =
    91       thy
    92       |> Theory.add_path bname
    93       |> PureThy.add_thmss [(("rules", rules), [])]
    94       |>>> PureThy.add_thms [(("induct", induct), [RuleCases.case_names case_numbers])];
    95     val result = {rules = rules, induct = induct, tcs = tcs};
    96     val thy =
    97       thy
    98       |> put_recdef name result
    99       |> Theory.parent_path;
   100   in (thy, result) end;
   101 
   102 val add_recdef = gen_add_recdef Tfl.define I IsarThy.apply_theorems;
   103 val add_recdef_x = gen_add_recdef Tfl.define (Simplifier.simpset_of o ThyInfo.get_theory)
   104   IsarThy.apply_theorems;
   105 val add_recdef_i = gen_add_recdef Tfl.define_i I IsarThy.apply_theorems_i;
   106 
   107 
   108 
   109 (** defer_recdef(_i) **)
   110 
   111 fun gen_defer_recdef tfl_fn app_thms raw_name eqs raw_congs thy =
   112   let
   113     val name = Sign.intern_const (Theory.sign_of thy) raw_name;
   114     val bname = Sign.base_name name;
   115 
   116     val _ = requires_recdef thy;
   117     val _ = message ("Deferred recursive function " ^ quote name ^ " ...");
   118 
   119     val (thy1, congs) = thy |> app_thms raw_congs;
   120     val (thy2, induct_rules) = tfl_fn thy1 name congs eqs;
   121     val (thy3, [induct_rules']) =
   122       thy2
   123       |> Theory.add_path bname
   124       |> PureThy.add_thms [(("induct_rules", induct_rules), [])]
   125       |>> Theory.parent_path;
   126   in (thy3, {induct_rules = induct_rules'}) end;
   127 
   128 val defer_recdef = gen_defer_recdef Tfl.defer IsarThy.apply_theorems;
   129 val defer_recdef_i = gen_defer_recdef Tfl.defer_i IsarThy.apply_theorems_i;
   130 
   131 
   132 
   133 (** package setup **)
   134 
   135 (* setup theory *)
   136 
   137 val setup = [RecdefData.init];
   138 
   139 
   140 (* outer syntax *)
   141 
   142 local structure P = OuterParse and K = OuterSyntax.Keyword in
   143 
   144 val recdef_decl =
   145   P.name -- P.term -- Scan.repeat1 (P.term --| P.marg_comment) --
   146   Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) [] --
   147   Scan.option (P.$$$ "(" |-- P.$$$ "simpset" |-- P.!!! (P.name --| P.$$$ ")"))
   148   >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef_x f R eqs ss congs);
   149 
   150 val recdefP =
   151   OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl
   152     (recdef_decl >> Toplevel.theory);
   153 
   154 
   155 val defer_recdef_decl =
   156   P.name -- Scan.repeat1 P.term --
   157   Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) []
   158   >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
   159 
   160 val defer_recdefP =
   161   OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl
   162     (defer_recdef_decl >> Toplevel.theory);
   163 
   164 val _ = OuterSyntax.add_keywords ["congs", "simpset"];
   165 val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP];
   166 
   167 end;
   168 
   169 
   170 end;