src/HOL/Tools/recdef_package.ML
author wenzelm
Sat Apr 01 20:21:39 2000 +0200 (2000-04-01)
changeset 8657 b9475dad85ed
parent 8625 93a11ebacf32
child 8711 00ec2ba9174d
permissions -rw-r--r--
recdef: admit names/atts;
     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
    13     -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
    14   val add_recdef: xstring -> string -> ((bstring * string) * Args.src list) list
    15     -> simpset option -> (xstring * Args.src list) list -> theory
    16     -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    17   val add_recdef_i: xstring -> term -> ((bstring * term) * theory attribute list) list
    18     -> simpset option -> (thm * theory attribute list) list
    19     -> theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    20   val defer_recdef: xstring -> string list -> (xstring * Args.src list) list
    21     -> theory -> theory * {induct_rules: thm}
    22   val defer_recdef_i: xstring -> term list -> (thm * theory attribute list) list
    23     -> theory -> theory * {induct_rules: thm}
    24   val setup: (theory -> theory) list
    25 end;
    26 
    27 structure RecdefPackage: RECDEF_PACKAGE =
    28 struct
    29 
    30 val quiet_mode = Tfl.quiet_mode;
    31 val message = Tfl.message;
    32 
    33 
    34 
    35 (** theory data **)
    36 
    37 (* data kind 'HOL/recdef' *)
    38 
    39 type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list};
    40 
    41 structure RecdefArgs =
    42 struct
    43   val name = "HOL/recdef";
    44   type T = recdef_info Symtab.table;
    45 
    46   val empty = Symtab.empty;
    47   val copy = I;
    48   val prep_ext = I;
    49   val merge: T * T -> T = Symtab.merge (K true);
    50 
    51   fun print sg tab =
    52     Pretty.writeln (Pretty.strs ("recdefs:" ::
    53       map #1 (Sign.cond_extern_table sg Sign.constK tab)));
    54 end;
    55 
    56 structure RecdefData = TheoryDataFun(RecdefArgs);
    57 val print_recdefs = RecdefData.print;
    58 
    59 
    60 (* get and put data *)
    61 
    62 fun get_recdef thy name = Symtab.lookup (RecdefData.get thy, name);
    63 
    64 fun put_recdef name info thy =
    65   let
    66     val tab = Symtab.update_new ((name, info), RecdefData.get thy)
    67       handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name);
    68   in RecdefData.put tab thy end;
    69 
    70 
    71 
    72 (** add_recdef(_i) **)
    73 
    74 fun requires_recdef thy = Theory.requires thy "Recdef" "recursive functions";
    75 
    76 fun gen_add_recdef tfl_fn prep_att prep_ss app_thms raw_name R eq_srcs raw_ss raw_congs thy =
    77   let
    78     val name = Sign.intern_const (Theory.sign_of thy) raw_name;
    79     val bname = Sign.base_name name;
    80 
    81     val _ = requires_recdef thy;
    82     val _ = message ("Defining recursive function " ^ quote name ^ " ...");
    83 
    84     val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
    85     val eq_atts = map (map (prep_att thy)) raw_eq_atts;
    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 
    89     val (thy, {rules = rules_idx, induct, tcs}) = tfl_fn thy name R (ss, congs) eqs;
    90     val rules = map (map #1) (Library.partition_eq Library.eq_snd rules_idx);
    91     val simp_att = if null tcs then [Simplifier.simp_add_global] else [];
    92 
    93     val case_numbers = map Library.string_of_int (1 upto Thm.nprems_of induct);
    94     val (thy, (simps' :: rules', [induct'])) =
    95       thy
    96       |> Theory.add_path bname
    97       |> PureThy.add_thmss ((("simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
    98       |>>> PureThy.add_thms [(("induct", induct), [RuleCases.case_names case_numbers])];
    99     val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
   100     val thy =
   101       thy
   102       |> put_recdef name result
   103       |> Theory.parent_path;
   104   in (thy, result) end;
   105 
   106 val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute I IsarThy.apply_theorems;
   107 val add_recdef_x = gen_add_recdef Tfl.define Attrib.global_attribute
   108   (Simplifier.simpset_of o ThyInfo.get_theory) IsarThy.apply_theorems;
   109 val add_recdef_i = gen_add_recdef Tfl.define_i (K I) I IsarThy.apply_theorems_i;
   110 
   111 
   112 
   113 (** defer_recdef(_i) **)
   114 
   115 fun gen_defer_recdef tfl_fn app_thms raw_name eqs raw_congs thy =
   116   let
   117     val name = Sign.intern_const (Theory.sign_of thy) raw_name;
   118     val bname = Sign.base_name name;
   119 
   120     val _ = requires_recdef thy;
   121     val _ = message ("Deferred recursive function " ^ quote name ^ " ...");
   122 
   123     val (thy1, congs) = thy |> app_thms raw_congs;
   124     val (thy2, induct_rules) = tfl_fn thy1 name congs eqs;
   125     val (thy3, [induct_rules']) =
   126       thy2
   127       |> Theory.add_path bname
   128       |> PureThy.add_thms [(("induct_rules", induct_rules), [])]
   129       |>> Theory.parent_path;
   130   in (thy3, {induct_rules = induct_rules'}) end;
   131 
   132 val defer_recdef = gen_defer_recdef Tfl.defer IsarThy.apply_theorems;
   133 val defer_recdef_i = gen_defer_recdef Tfl.defer_i IsarThy.apply_theorems_i;
   134 
   135 
   136 
   137 (** package setup **)
   138 
   139 (* setup theory *)
   140 
   141 val setup = [RecdefData.init];
   142 
   143 
   144 (* outer syntax *)
   145 
   146 local structure P = OuterParse and K = OuterSyntax.Keyword in
   147 
   148 val recdef_decl =
   149   P.name -- P.term -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment) --
   150   Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) [] --
   151   Scan.option (P.$$$ "(" |-- P.$$$ "simpset" |-- P.!!! (P.name --| P.$$$ ")"))
   152   >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef_x f R (map P.triple_swap eqs) ss congs);
   153 
   154 val recdefP =
   155   OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl
   156     (recdef_decl >> Toplevel.theory);
   157 
   158 
   159 val defer_recdef_decl =
   160   P.name -- Scan.repeat1 P.prop --
   161   Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) []
   162   >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
   163 
   164 val defer_recdefP =
   165   OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl
   166     (defer_recdef_decl >> Toplevel.theory);
   167 
   168 val _ = OuterSyntax.add_keywords ["congs", "simpset"];
   169 val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP];
   170 
   171 end;
   172 
   173 
   174 end;