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