src/HOL/Tools/recdef_package.ML
changeset 6429 9771ce553e56
child 6439 7eea9f25dc49
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Wed Apr 14 19:05:10 1999 +0200
     1.3 @@ -0,0 +1,75 @@
     1.4 +(*  Title:      HOL/Tools/recdef_package.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Wrapper module for Konrad Slind's TFL package.
     1.9 +*)
    1.10 +
    1.11 +signature RECDEF_PACKAGE =
    1.12 +sig
    1.13 +  val quiet_mode: bool ref
    1.14 +  val add_recdef: xstring -> string -> ((bstring * string) * Args.src list) list
    1.15 +    -> string option -> (xstring * Args.src list) list
    1.16 +    -> theory -> theory * {rules: thm list, induct: thm, tcs: term list}
    1.17 +  val add_recdef_i: xstring -> term -> ((bstring * term) * theory attribute list) list
    1.18 +    -> simpset option -> (thm * theory attribute list) list
    1.19 +    -> theory -> theory * {rules: thm list, induct: thm, tcs: term list}
    1.20 +end;
    1.21 +
    1.22 +structure RecdefPackage: RECDEF_PACKAGE =
    1.23 +struct
    1.24 +
    1.25 +
    1.26 +(* messages *)
    1.27 +
    1.28 +val quiet_mode = Tfl.quiet_mode;
    1.29 +val message = Tfl.message;
    1.30 +
    1.31 +
    1.32 +(* add_recdef(_i) *)
    1.33 +
    1.34 +fun gen_add_recdef tfl_def prep_att prep_ss app_thms name R eq_srcs raw_ss raw_congs thy =
    1.35 +  let
    1.36 +    val _ = message ("Defining recursive function " ^ quote name ^ " ...");
    1.37 +
    1.38 +    val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
    1.39 +    val eq_atts = map (map (prep_att thy)) raw_eq_atts;
    1.40 +    val ss = (case raw_ss of None => Simplifier.simpset_of thy | Some x => prep_ss x);
    1.41 +    val (thy1, congs) = thy |> app_thms raw_congs;
    1.42 +    val (thy2, pats) = tfl_def thy1 name R eqs;
    1.43 +    val (result as {rules, induct, tcs}) = Tfl.simplify_defn (ss, congs) (thy2, (name, pats));
    1.44 +    val thy3 =
    1.45 +      thy2
    1.46 +      |> Theory.add_path name
    1.47 +      |> PureThy.add_thmss [(("rules", rules), [])]
    1.48 +      |> PureThy.add_thms ((("induct", induct), []) :: ((eq_names ~~ rules) ~~ eq_atts))
    1.49 +      |> Theory.parent_path;
    1.50 +  in (thy3, result) end;
    1.51 +
    1.52 +val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute
    1.53 +  (Simplifier.simpset_of o ThyInfo.get_theory) IsarThy.apply_theorems;
    1.54 +
    1.55 +val add_recdef_i = gen_add_recdef Tfl.define_i (K I) I IsarThy.apply_theorems_i;
    1.56 +
    1.57 +
    1.58 +(* outer syntax *)
    1.59 +
    1.60 +local open OuterParse in
    1.61 +
    1.62 +val recdef_decl =
    1.63 +  name -- term -- Scan.repeat1 (opt_thm_name ":" -- term) --
    1.64 +  Scan.optional ($$$ "congs" |-- !!! xthms1) [] --
    1.65 +  Scan.option ($$$ "simpset" |-- !!! name)
    1.66 +  >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef f R (map triple_swap eqs) ss congs);
    1.67 +
    1.68 +val recdefP =
    1.69 +  OuterSyntax.command "recdef" "general recursive function definition (TFL)"
    1.70 +    (recdef_decl >> Toplevel.theory);
    1.71 +
    1.72 +val _ = OuterSyntax.add_keywords ["congs", "simpset"];
    1.73 +val _ = OuterSyntax.add_parsers [recdefP];
    1.74 +
    1.75 +end;
    1.76 +
    1.77 +
    1.78 +end;