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