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