src/HOL/Tools/recdef_package.ML
author wenzelm
Wed Apr 14 19:05:10 1999 +0200 (1999-04-14)
changeset 6429 9771ce553e56
child 6439 7eea9f25dc49
permissions -rw-r--r--
Wrapper module for Konrad Slind's TFL package.
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@6429
    11
  val add_recdef: xstring -> string -> ((bstring * string) * Args.src list) list
wenzelm@6429
    12
    -> string option -> (xstring * Args.src list) list
wenzelm@6429
    13
    -> theory -> theory * {rules: thm list, induct: thm, tcs: term list}
wenzelm@6429
    14
  val add_recdef_i: xstring -> term -> ((bstring * term) * theory attribute list) list
wenzelm@6429
    15
    -> simpset option -> (thm * theory attribute list) list
wenzelm@6429
    16
    -> theory -> theory * {rules: thm list, induct: thm, tcs: term list}
wenzelm@6429
    17
end;
wenzelm@6429
    18
wenzelm@6429
    19
structure RecdefPackage: RECDEF_PACKAGE =
wenzelm@6429
    20
struct
wenzelm@6429
    21
wenzelm@6429
    22
wenzelm@6429
    23
(* messages *)
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@6429
    29
(* add_recdef(_i) *)
wenzelm@6429
    30
wenzelm@6429
    31
fun gen_add_recdef tfl_def prep_att prep_ss app_thms name R eq_srcs raw_ss raw_congs thy =
wenzelm@6429
    32
  let
wenzelm@6429
    33
    val _ = message ("Defining recursive function " ^ quote name ^ " ...");
wenzelm@6429
    34
wenzelm@6429
    35
    val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
wenzelm@6429
    36
    val eq_atts = map (map (prep_att thy)) raw_eq_atts;
wenzelm@6429
    37
    val ss = (case raw_ss of None => Simplifier.simpset_of thy | Some x => prep_ss x);
wenzelm@6429
    38
    val (thy1, congs) = thy |> app_thms raw_congs;
wenzelm@6429
    39
    val (thy2, pats) = tfl_def thy1 name R eqs;
wenzelm@6429
    40
    val (result as {rules, induct, tcs}) = Tfl.simplify_defn (ss, congs) (thy2, (name, pats));
wenzelm@6429
    41
    val thy3 =
wenzelm@6429
    42
      thy2
wenzelm@6429
    43
      |> Theory.add_path name
wenzelm@6429
    44
      |> PureThy.add_thmss [(("rules", rules), [])]
wenzelm@6429
    45
      |> PureThy.add_thms ((("induct", induct), []) :: ((eq_names ~~ rules) ~~ eq_atts))
wenzelm@6429
    46
      |> Theory.parent_path;
wenzelm@6429
    47
  in (thy3, result) end;
wenzelm@6429
    48
wenzelm@6429
    49
val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute
wenzelm@6429
    50
  (Simplifier.simpset_of o ThyInfo.get_theory) IsarThy.apply_theorems;
wenzelm@6429
    51
wenzelm@6429
    52
val add_recdef_i = gen_add_recdef Tfl.define_i (K I) I IsarThy.apply_theorems_i;
wenzelm@6429
    53
wenzelm@6429
    54
wenzelm@6429
    55
(* outer syntax *)
wenzelm@6429
    56
wenzelm@6429
    57
local open OuterParse in
wenzelm@6429
    58
wenzelm@6429
    59
val recdef_decl =
wenzelm@6429
    60
  name -- term -- Scan.repeat1 (opt_thm_name ":" -- term) --
wenzelm@6429
    61
  Scan.optional ($$$ "congs" |-- !!! xthms1) [] --
wenzelm@6429
    62
  Scan.option ($$$ "simpset" |-- !!! name)
wenzelm@6429
    63
  >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef f R (map triple_swap eqs) ss congs);
wenzelm@6429
    64
wenzelm@6429
    65
val recdefP =
wenzelm@6429
    66
  OuterSyntax.command "recdef" "general recursive function definition (TFL)"
wenzelm@6429
    67
    (recdef_decl >> Toplevel.theory);
wenzelm@6429
    68
wenzelm@6429
    69
val _ = OuterSyntax.add_keywords ["congs", "simpset"];
wenzelm@6429
    70
val _ = OuterSyntax.add_parsers [recdefP];
wenzelm@6429
    71
wenzelm@6429
    72
end;
wenzelm@6429
    73
wenzelm@6429
    74
wenzelm@6429
    75
end;