src/HOL/Tools/recdef_package.ML
author wenzelm
Thu Apr 13 17:49:42 2000 +0200 (2000-04-13)
changeset 8711 00ec2ba9174d
parent 8657 b9475dad85ed
child 8734 b456aba346a6
permissions -rw-r--r--
outer syntax: no simps;
     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 app_thms raw_name R eq_srcs opt_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 = if_none opt_ss (Simplifier.simpset_of thy);
    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 IsarThy.apply_theorems;
   107 val add_recdef_x = gen_add_recdef Tfl.define Attrib.global_attribute IsarThy.apply_theorems;
   108 val add_recdef_i = gen_add_recdef Tfl.define_i (K I) IsarThy.apply_theorems_i;
   109 
   110 
   111 
   112 (** defer_recdef(_i) **)
   113 
   114 fun gen_defer_recdef tfl_fn app_thms raw_name eqs raw_congs thy =
   115   let
   116     val name = Sign.intern_const (Theory.sign_of thy) raw_name;
   117     val bname = Sign.base_name name;
   118 
   119     val _ = requires_recdef thy;
   120     val _ = message ("Deferred recursive function " ^ quote name ^ " ...");
   121 
   122     val (thy1, congs) = thy |> app_thms raw_congs;
   123     val (thy2, induct_rules) = tfl_fn thy1 name congs eqs;
   124     val (thy3, [induct_rules']) =
   125       thy2
   126       |> Theory.add_path bname
   127       |> PureThy.add_thms [(("induct_rules", induct_rules), [])]
   128       |>> Theory.parent_path;
   129   in (thy3, {induct_rules = induct_rules'}) end;
   130 
   131 val defer_recdef = gen_defer_recdef Tfl.defer IsarThy.apply_theorems;
   132 val defer_recdef_i = gen_defer_recdef Tfl.defer_i IsarThy.apply_theorems_i;
   133 
   134 
   135 
   136 (** package setup **)
   137 
   138 (* setup theory *)
   139 
   140 val setup = [RecdefData.init];
   141 
   142 
   143 (* outer syntax *)
   144 
   145 local structure P = OuterParse and K = OuterSyntax.Keyword in
   146 
   147 val recdef_decl =
   148   P.name -- P.term -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment) --
   149   Scan.optional (P.$$$ "congs" |-- P.!!! P.xthms1) []
   150   >> (fn (((f, R), eqs), congs) => #1 o add_recdef_x f R (map P.triple_swap eqs) None congs);
   151 
   152 val recdefP =
   153   OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl
   154     (recdef_decl >> Toplevel.theory);
   155 
   156 
   157 val defer_recdef_decl =
   158   P.name -- Scan.repeat1 P.prop --
   159   Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) []
   160   >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
   161 
   162 val defer_recdefP =
   163   OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl
   164     (defer_recdef_decl >> Toplevel.theory);
   165 
   166 val _ = OuterSyntax.add_keywords ["congs", "simpset"];
   167 val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP];
   168 
   169 end;
   170 
   171 
   172 end;