author | nipkow |
Wed, 26 Jul 2000 19:42:19 +0200 | |
changeset 9447 | e5180c869772 |
parent 8734 | b456aba346a6 |
child 9640 | 8c6cf4f01644 |
permissions | -rw-r--r-- |
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 |
8657 | 12 |
val get_recdef: theory -> string |
13 |
-> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option |
|
14 |
val add_recdef: xstring -> string -> ((bstring * string) * Args.src list) list |
|
15 |
-> simpset option -> (xstring * Args.src list) list -> theory |
|
16 |
-> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list} |
|
17 |
val add_recdef_i: xstring -> term -> ((bstring * term) * theory attribute list) list |
|
18 |
-> simpset option -> (thm * theory attribute list) list |
|
19 |
-> theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list} |
|
6557 | 20 |
val defer_recdef: xstring -> string list -> (xstring * Args.src list) list |
21 |
-> theory -> theory * {induct_rules: thm} |
|
22 |
val defer_recdef_i: xstring -> term list -> (thm * theory attribute list) list |
|
23 |
-> theory -> theory * {induct_rules: thm} |
|
6439 | 24 |
val setup: (theory -> theory) list |
6429 | 25 |
end; |
26 |
||
27 |
structure RecdefPackage: RECDEF_PACKAGE = |
|
28 |
struct |
|
29 |
||
30 |
val quiet_mode = Tfl.quiet_mode; |
|
31 |
val message = Tfl.message; |
|
32 |
||
33 |
||
6439 | 34 |
|
35 |
(** theory data **) |
|
36 |
||
37 |
(* data kind 'HOL/recdef' *) |
|
38 |
||
8657 | 39 |
type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list}; |
6439 | 40 |
|
41 |
structure RecdefArgs = |
|
42 |
struct |
|
43 |
val name = "HOL/recdef"; |
|
44 |
type T = recdef_info Symtab.table; |
|
45 |
||
46 |
val empty = Symtab.empty; |
|
6557 | 47 |
val copy = I; |
6439 | 48 |
val prep_ext = I; |
49 |
val merge: T * T -> T = Symtab.merge (K true); |
|
50 |
||
51 |
fun print sg tab = |
|
52 |
Pretty.writeln (Pretty.strs ("recdefs:" :: |
|
6851 | 53 |
map #1 (Sign.cond_extern_table sg Sign.constK tab))); |
6439 | 54 |
end; |
55 |
||
56 |
structure RecdefData = TheoryDataFun(RecdefArgs); |
|
57 |
val print_recdefs = RecdefData.print; |
|
6429 | 58 |
|
6439 | 59 |
|
60 |
(* get and put data *) |
|
61 |
||
8481
89d498a8d3f6
get_recdef now returns None instead of raising ERROR.
berghofe
parents:
8430
diff
changeset
|
62 |
fun get_recdef thy name = Symtab.lookup (RecdefData.get thy, name); |
6439 | 63 |
|
64 |
fun put_recdef name info thy = |
|
6429 | 65 |
let |
6439 | 66 |
val tab = Symtab.update_new ((name, info), RecdefData.get thy) |
67 |
handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name); |
|
68 |
in RecdefData.put tab thy end; |
|
69 |
||
70 |
||
71 |
||
72 |
(** add_recdef(_i) **) |
|
73 |
||
6557 | 74 |
fun requires_recdef thy = Theory.requires thy "Recdef" "recursive functions"; |
75 |
||
8711 | 76 |
fun gen_add_recdef tfl_fn prep_att app_thms raw_name R eq_srcs opt_ss raw_congs thy = |
6439 | 77 |
let |
78 |
val name = Sign.intern_const (Theory.sign_of thy) raw_name; |
|
79 |
val bname = Sign.base_name name; |
|
80 |
||
6557 | 81 |
val _ = requires_recdef thy; |
6429 | 82 |
val _ = message ("Defining recursive function " ^ quote name ^ " ..."); |
83 |
||
8657 | 84 |
val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs); |
85 |
val eq_atts = map (map (prep_att thy)) raw_eq_atts; |
|
8711 | 86 |
val ss = if_none opt_ss (Simplifier.simpset_of thy); |
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7262
diff
changeset
|
87 |
val (thy, congs) = thy |> app_thms raw_congs; |
8657 | 88 |
|
89 |
val (thy, {rules = rules_idx, induct, tcs}) = tfl_fn thy name R (ss, congs) eqs; |
|
90 |
val rules = map (map #1) (Library.partition_eq Library.eq_snd rules_idx); |
|
91 |
val simp_att = if null tcs then [Simplifier.simp_add_global] else []; |
|
92 |
||
8430 | 93 |
val case_numbers = map Library.string_of_int (1 upto Thm.nprems_of induct); |
8657 | 94 |
val (thy, (simps' :: rules', [induct'])) = |
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7262
diff
changeset
|
95 |
thy |
6439 | 96 |
|> Theory.add_path bname |
8657 | 97 |
|> PureThy.add_thmss ((("simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts)) |
8430 | 98 |
|>>> PureThy.add_thms [(("induct", induct), [RuleCases.case_names case_numbers])]; |
8657 | 99 |
val result = {simps = simps', rules = rules', induct = induct', tcs = tcs}; |
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7262
diff
changeset
|
100 |
val thy = |
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7262
diff
changeset
|
101 |
thy |
6439 | 102 |
|> put_recdef name result |
6429 | 103 |
|> Theory.parent_path; |
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7262
diff
changeset
|
104 |
in (thy, result) end; |
6429 | 105 |
|
8711 | 106 |
val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute IsarThy.apply_theorems; |
107 |
val add_recdef_x = gen_add_recdef Tfl.define Attrib.global_attribute IsarThy.apply_theorems; |
|
108 |
val add_recdef_i = gen_add_recdef Tfl.define_i (K I) IsarThy.apply_theorems_i; |
|
6429 | 109 |
|
110 |
||
6557 | 111 |
|
112 |
(** defer_recdef(_i) **) |
|
113 |
||
114 |
fun gen_defer_recdef tfl_fn app_thms raw_name eqs raw_congs thy = |
|
115 |
let |
|
116 |
val name = Sign.intern_const (Theory.sign_of thy) raw_name; |
|
117 |
val bname = Sign.base_name name; |
|
118 |
||
119 |
val _ = requires_recdef thy; |
|
120 |
val _ = message ("Deferred recursive function " ^ quote name ^ " ..."); |
|
121 |
||
122 |
val (thy1, congs) = thy |> app_thms raw_congs; |
|
123 |
val (thy2, induct_rules) = tfl_fn thy1 name congs eqs; |
|
8430 | 124 |
val (thy3, [induct_rules']) = |
6557 | 125 |
thy2 |
126 |
|> Theory.add_path bname |
|
127 |
|> PureThy.add_thms [(("induct_rules", induct_rules), [])] |
|
8430 | 128 |
|>> Theory.parent_path; |
129 |
in (thy3, {induct_rules = induct_rules'}) end; |
|
6557 | 130 |
|
131 |
val defer_recdef = gen_defer_recdef Tfl.defer IsarThy.apply_theorems; |
|
132 |
val defer_recdef_i = gen_defer_recdef Tfl.defer_i IsarThy.apply_theorems_i; |
|
133 |
||
134 |
||
135 |
||
6439 | 136 |
(** package setup **) |
137 |
||
138 |
(* setup theory *) |
|
139 |
||
140 |
val setup = [RecdefData.init]; |
|
141 |
||
142 |
||
6429 | 143 |
(* outer syntax *) |
144 |
||
6723 | 145 |
local structure P = OuterParse and K = OuterSyntax.Keyword in |
6429 | 146 |
|
147 |
val recdef_decl = |
|
8657 | 148 |
P.name -- P.term -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment) -- |
8711 | 149 |
Scan.optional (P.$$$ "congs" |-- P.!!! P.xthms1) [] |
150 |
>> (fn (((f, R), eqs), congs) => #1 o add_recdef_x f R (map P.triple_swap eqs) None congs); |
|
6429 | 151 |
|
152 |
val recdefP = |
|
6723 | 153 |
OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl |
6429 | 154 |
(recdef_decl >> Toplevel.theory); |
155 |
||
6557 | 156 |
|
157 |
val defer_recdef_decl = |
|
8657 | 158 |
P.name -- Scan.repeat1 P.prop -- |
6723 | 159 |
Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) [] |
6557 | 160 |
>> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs); |
161 |
||
162 |
val defer_recdefP = |
|
6723 | 163 |
OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl |
6557 | 164 |
(defer_recdef_decl >> Toplevel.theory); |
165 |
||
8734 | 166 |
val _ = OuterSyntax.add_keywords ["congs"]; |
6557 | 167 |
val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP]; |
6429 | 168 |
|
169 |
end; |
|
170 |
||
171 |
||
172 |
end; |