9 sig |
9 sig |
10 val quiet_mode: bool ref |
10 val quiet_mode: bool ref |
11 val print_recdefs: theory -> unit |
11 val print_recdefs: theory -> unit |
12 val get_recdef: theory -> string |
12 val get_recdef: theory -> string |
13 -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option |
13 -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option |
14 val simp_add: Context.generic attribute |
14 val simp_add: attribute |
15 val simp_del: Context.generic attribute |
15 val simp_del: attribute |
16 val cong_add: Context.generic attribute |
16 val cong_add: attribute |
17 val cong_del: Context.generic attribute |
17 val cong_del: attribute |
18 val wf_add: Context.generic attribute |
18 val wf_add: attribute |
19 val wf_del: Context.generic attribute |
19 val wf_del: attribute |
20 val add_recdef: bool -> xstring -> string -> ((bstring * string) * Attrib.src list) list -> |
20 val add_recdef: bool -> xstring -> string -> ((bstring * string) * Attrib.src list) list -> |
21 Attrib.src option -> theory -> theory |
21 Attrib.src option -> theory -> theory |
22 * {simps: thm list, rules: thm list list, induct: thm, tcs: term list} |
22 * {simps: thm list, rules: thm list list, induct: thm, tcs: term list} |
23 val add_recdef_i: bool -> xstring -> term -> ((bstring * term) * theory attribute list) list -> |
23 val add_recdef_i: bool -> xstring -> term -> ((bstring * term) * attribute list) list -> |
24 theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list} |
24 theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list} |
25 val defer_recdef: xstring -> string list -> (thmref * Attrib.src list) list |
25 val defer_recdef: xstring -> string list -> (thmref * Attrib.src list) list |
26 -> theory -> theory * {induct_rules: thm} |
26 -> theory -> theory * {induct_rules: thm} |
27 val defer_recdef_i: xstring -> term list -> (thm list * theory attribute list) list |
27 val defer_recdef_i: xstring -> term list -> (thm list * attribute list) list |
28 -> theory -> theory * {induct_rules: thm} |
28 -> theory -> theory * {induct_rules: thm} |
29 val recdef_tc: bstring * Attrib.src list -> xstring -> int option -> theory -> Proof.state |
29 val recdef_tc: bstring * Attrib.src list -> xstring -> int option -> theory -> Proof.state |
30 val recdef_tc_i: bstring * theory attribute list -> string -> int option |
30 val recdef_tc_i: bstring * attribute list -> string -> int option -> theory -> Proof.state |
31 -> theory -> Proof.state |
|
32 val setup: theory -> theory |
31 val setup: theory -> theory |
33 end; |
32 end; |
34 |
33 |
35 structure RecdefPackage: RECDEF_PACKAGE = |
34 structure RecdefPackage: RECDEF_PACKAGE = |
36 struct |
35 struct |
146 (* attributes *) |
145 (* attributes *) |
147 |
146 |
148 fun map_hints f (Context.Theory thy) = Context.Theory (map_global_hints f thy) |
147 fun map_hints f (Context.Theory thy) = Context.Theory (map_global_hints f thy) |
149 | map_hints f (Context.Proof ctxt) = Context.Proof (map_local_hints f ctxt); |
148 | map_hints f (Context.Proof ctxt) = Context.Proof (map_local_hints f ctxt); |
150 |
149 |
151 fun attrib f = Attrib.declaration (map_hints o f); |
150 fun attrib f = Thm.declaration_attribute (map_hints o f); |
152 |
151 |
153 val simp_add = attrib (map_simps o Drule.add_rule); |
152 val simp_add = attrib (map_simps o Drule.add_rule); |
154 val simp_del = attrib (map_simps o Drule.del_rule); |
153 val simp_del = attrib (map_simps o Drule.del_rule); |
155 val cong_add = attrib (map_congs o add_cong); |
154 val cong_add = attrib (map_congs o add_cong); |
156 val cong_del = attrib (map_congs o del_cong); |
155 val cong_del = attrib (map_congs o del_cong); |
163 val recdef_simpN = "recdef_simp"; |
162 val recdef_simpN = "recdef_simp"; |
164 val recdef_congN = "recdef_cong"; |
163 val recdef_congN = "recdef_cong"; |
165 val recdef_wfN = "recdef_wf"; |
164 val recdef_wfN = "recdef_wf"; |
166 |
165 |
167 val recdef_modifiers = |
166 val recdef_modifiers = |
168 [Args.$$$ recdef_simpN -- Args.colon >> K ((I, Attrib.context simp_add): Method.modifier), |
167 [Args.$$$ recdef_simpN -- Args.colon >> K ((I, simp_add): Method.modifier), |
169 Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (I, Attrib.context simp_add), |
168 Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (I, simp_add), |
170 Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (I, Attrib.context simp_del), |
169 Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (I, simp_del), |
171 Args.$$$ recdef_congN -- Args.colon >> K (I, Attrib.context cong_add), |
170 Args.$$$ recdef_congN -- Args.colon >> K (I, cong_add), |
172 Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (I, Attrib.context cong_add), |
171 Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (I, cong_add), |
173 Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (I, Attrib.context cong_del), |
172 Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (I, cong_del), |
174 Args.$$$ recdef_wfN -- Args.colon >> K (I, Attrib.context wf_add), |
173 Args.$$$ recdef_wfN -- Args.colon >> K (I, wf_add), |
175 Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (I, Attrib.context wf_add), |
174 Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (I, wf_add), |
176 Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (I, Attrib.context wf_del)] @ |
175 Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (I, wf_del)] @ |
177 Clasimp.clasimp_modifiers; |
176 Clasimp.clasimp_modifiers; |
178 |
177 |
179 |
178 |
180 |
179 |
181 (** prepare_hints(_i) **) |
180 (** prepare_hints(_i) **) |
221 give rise to looping conditional rewriting.*) |
220 give rise to looping conditional rewriting.*) |
222 val (thy, {rules = rules_idx, induct, tcs}) = |
221 val (thy, {rules = rules_idx, induct, tcs}) = |
223 tfl_fn not_permissive thy cs (ss delcongs [imp_cong]) |
222 tfl_fn not_permissive thy cs (ss delcongs [imp_cong]) |
224 congs wfs name R eqs; |
223 congs wfs name R eqs; |
225 val rules = map (map #1) (Library.partition_eq (Library.eq_snd (op =)) rules_idx); |
224 val rules = map (map #1) (Library.partition_eq (Library.eq_snd (op =)) rules_idx); |
226 val simp_att = if null tcs then |
225 val simp_att = if null tcs then [Simplifier.simp_add, RecfunCodegen.add NONE] else []; |
227 [Attrib.theory Simplifier.simp_add, RecfunCodegen.add NONE] else []; |
|
228 |
226 |
229 val ((simps' :: rules', [induct']), thy) = |
227 val ((simps' :: rules', [induct']), thy) = |
230 thy |
228 thy |
231 |> Theory.add_path bname |
229 |> Theory.add_path bname |
232 |> PureThy.add_thmss |
230 |> PureThy.add_thmss |
237 thy |
235 thy |
238 |> put_recdef name result |
236 |> put_recdef name result |
239 |> Theory.parent_path; |
237 |> Theory.parent_path; |
240 in (thy, result) end; |
238 in (thy, result) end; |
241 |
239 |
242 val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute prepare_hints; |
240 val add_recdef = gen_add_recdef Tfl.define Attrib.attribute prepare_hints; |
243 fun add_recdef_i x y z w = gen_add_recdef Tfl.define_i (K I) prepare_hints_i x y z w (); |
241 fun add_recdef_i x y z w = gen_add_recdef Tfl.define_i (K I) prepare_hints_i x y z w (); |
244 |
242 |
245 |
243 |
246 |
244 |
247 (** defer_recdef(_i) **) |
245 (** defer_recdef(_i) **) |
282 val tc = List.nth (tcs, i - 1) handle Subscript => |
280 val tc = List.nth (tcs, i - 1) handle Subscript => |
283 error ("No termination condition #" ^ string_of_int i ^ |
281 error ("No termination condition #" ^ string_of_int i ^ |
284 " in recdef definition of " ^ quote name); |
282 " in recdef definition of " ^ quote name); |
285 in IsarThy.theorem_i Drule.internalK (bname, atts) (HOLogic.mk_Trueprop tc, ([], [])) thy end; |
283 in IsarThy.theorem_i Drule.internalK (bname, atts) (HOLogic.mk_Trueprop tc, ([], [])) thy end; |
286 |
284 |
287 val recdef_tc = gen_recdef_tc Attrib.global_attribute Sign.intern_const; |
285 val recdef_tc = gen_recdef_tc Attrib.attribute Sign.intern_const; |
288 val recdef_tc_i = gen_recdef_tc (K I) (K I); |
286 val recdef_tc_i = gen_recdef_tc (K I) (K I); |
289 |
287 |
290 |
288 |
291 |
289 |
292 (** package setup **) |
290 (** package setup **) |
295 |
293 |
296 val setup = |
294 val setup = |
297 GlobalRecdefData.init #> |
295 GlobalRecdefData.init #> |
298 LocalRecdefData.init #> |
296 LocalRecdefData.init #> |
299 Attrib.add_attributes |
297 Attrib.add_attributes |
300 [(recdef_simpN, Attrib.common (Attrib.add_del_args simp_add simp_del), |
298 [(recdef_simpN, Attrib.add_del_args simp_add simp_del, "declaration of recdef simp rule"), |
301 "declaration of recdef simp rule"), |
299 (recdef_congN, Attrib.add_del_args cong_add cong_del, "declaration of recdef cong rule"), |
302 (recdef_congN, Attrib.common (Attrib.add_del_args cong_add cong_del), |
300 (recdef_wfN, Attrib.add_del_args wf_add wf_del, "declaration of recdef wf rule")]; |
303 "declaration of recdef cong rule"), |
|
304 (recdef_wfN, Attrib.common (Attrib.add_del_args wf_add wf_del), |
|
305 "declaration of recdef wf rule")]; |
|
306 |
301 |
307 |
302 |
308 (* outer syntax *) |
303 (* outer syntax *) |
309 |
304 |
310 local structure P = OuterParse and K = OuterKeyword in |
305 local structure P = OuterParse and K = OuterKeyword in |