src/HOL/Tools/recdef_package.ML
author wenzelm
Fri Apr 16 14:49:09 1999 +0200 (1999-04-16)
changeset 6439 7eea9f25dc49
parent 6429 9771ce553e56
child 6458 13c779aec65a
permissions -rw-r--r--
'HOL/recdef' theory data;
     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 -> ((bstring * string) * Args.src list) list
    14     -> string option -> (xstring * Args.src list) list
    15     -> theory -> theory * {rules: thm list, induct: thm, tcs: term list}
    16   val add_recdef_i: xstring -> term -> ((bstring * term) * theory attribute list) list
    17     -> simpset option -> (thm * theory attribute list) list
    18     -> theory -> theory * {rules: thm list, induct: thm, tcs: term list}
    19   val setup: (theory -> theory) list
    20 end;
    21 
    22 structure RecdefPackage: RECDEF_PACKAGE =
    23 struct
    24 
    25 val quiet_mode = Tfl.quiet_mode;
    26 val message = Tfl.message;
    27 
    28 
    29 
    30 (** theory data **)
    31 
    32 (* data kind 'HOL/recdef' *)
    33 
    34 type recdef_info = {rules: thm list, induct: thm, tcs: term list};
    35 
    36 structure RecdefArgs =
    37 struct
    38   val name = "HOL/recdef";
    39   type T = recdef_info Symtab.table;
    40 
    41   val empty = Symtab.empty;
    42   val prep_ext = I;
    43   val merge: T * T -> T = Symtab.merge (K true);
    44 
    45   fun print sg tab =
    46     Pretty.writeln (Pretty.strs ("recdefs:" ::
    47       map (Sign.cond_extern sg Sign.constK o fst) (Symtab.dest tab)));
    48 end;
    49 
    50 structure RecdefData = TheoryDataFun(RecdefArgs);
    51 val print_recdefs = RecdefData.print;
    52 
    53 
    54 (* get and put data *)
    55 
    56 fun get_recdef thy name =
    57   (case Symtab.lookup (RecdefData.get thy, name) of
    58     Some info => info
    59   | None => error ("Unknown recursive function " ^ quote name));
    60 
    61 fun put_recdef name info thy =
    62   let
    63     val tab = Symtab.update_new ((name, info), RecdefData.get thy)
    64       handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name);
    65   in RecdefData.put tab thy end;
    66 
    67 
    68 
    69 (** add_recdef(_i) **)
    70 
    71 fun gen_add_recdef tfl_def prep_att prep_ss app_thms raw_name R eq_srcs raw_ss raw_congs thy =
    72   let
    73     val name = Sign.intern_const (Theory.sign_of thy) raw_name;
    74     val bname = Sign.base_name name;
    75 
    76     val _ = message ("Defining recursive function " ^ quote name ^ " ...");
    77 
    78     val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
    79     val eq_atts = map (map (prep_att thy)) raw_eq_atts;
    80     val ss = (case raw_ss of None => Simplifier.simpset_of thy | Some x => prep_ss x);
    81     val (thy1, congs) = thy |> app_thms raw_congs;
    82     val (thy2, pats) = tfl_def thy1 name R eqs;
    83     val (result as {rules, induct, tcs}) = Tfl.simplify_defn (ss, congs) (thy2, (name, pats));
    84     val thy3 =
    85       thy2
    86       |> Theory.add_path bname
    87       |> PureThy.add_thmss [(("rules", rules), [])]
    88       |> PureThy.add_thms ((("induct", induct), []) :: ((eq_names ~~ rules) ~~ eq_atts))
    89       |> put_recdef name result
    90       |> Theory.parent_path;
    91   in (thy3, result) end;
    92 
    93 val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute
    94   (Simplifier.simpset_of o ThyInfo.get_theory) IsarThy.apply_theorems;
    95 
    96 val add_recdef_i = gen_add_recdef Tfl.define_i (K I) I IsarThy.apply_theorems_i;
    97 
    98 
    99 (** package setup **)
   100 
   101 (* setup theory *)
   102 
   103 val setup = [RecdefData.init];
   104 
   105 
   106 (* outer syntax *)
   107 
   108 local open OuterParse in
   109 
   110 val recdef_decl =
   111   name -- term -- Scan.repeat1 (opt_thm_name ":" -- term) --
   112   Scan.optional ($$$ "congs" |-- !!! xthms1) [] --
   113   Scan.option ($$$ "simpset" |-- !!! name)
   114   >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef f R (map triple_swap eqs) ss congs);
   115 
   116 val recdefP =
   117   OuterSyntax.command "recdef" "define general recursive functions (TFL)"
   118     (recdef_decl >> Toplevel.theory);
   119 
   120 val _ = OuterSyntax.add_keywords ["congs", "simpset"];
   121 val _ = OuterSyntax.add_parsers [recdefP];
   122 
   123 end;
   124 
   125 
   126 end;