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