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