equal
deleted
inserted
replaced
263 |-> (fn defs => `(fn lthy => (prefix, prove lthy defs))) |
263 |-> (fn defs => `(fn lthy => (prefix, prove lthy defs))) |
264 end; |
264 end; |
265 |
265 |
266 local |
266 local |
267 |
267 |
|
268 fun specs_of simps = |
|
269 let |
|
270 val eqns = maps snd simps |
|
271 fun dest_eqn th = fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))) |
|
272 val t = distinct (op =) (map dest_eqn eqns) |
|
273 in |
|
274 (t, eqns) |
|
275 end |
|
276 |
268 fun gen_primrec prep_spec raw_fixes raw_spec lthy = |
277 fun gen_primrec prep_spec raw_fixes raw_spec lthy = |
269 let |
278 let |
270 val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy); |
279 val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy); |
271 fun attr_bindings prefix = map (fn ((b, attrs), _) => |
280 fun attr_bindings prefix = map (fn ((b, attrs), _) => |
272 (Binding.qualify false prefix b, Code.add_default_eqn_attrib :: attrs)) spec; |
281 (Binding.qualify false prefix b, Code.add_default_eqn_attrib :: attrs)) spec; |
275 map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]); |
284 map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]); |
276 in |
285 in |
277 lthy |
286 lthy |
278 |> add_primrec_simple fixes (map snd spec) |
287 |> add_primrec_simple fixes (map snd spec) |
279 |-> (fn (prefix, simps) => fold_map Local_Theory.note (attr_bindings prefix ~~ simps) |
288 |-> (fn (prefix, simps) => fold_map Local_Theory.note (attr_bindings prefix ~~ simps) |
280 #-> (fn simps' => Local_Theory.note (simp_attr_binding prefix, maps snd simps'))) |
289 #-> (fn simps' => Local_Theory.note (simp_attr_binding prefix, maps snd simps') |
|
290 ##> (Spec_Rules.add Spec_Rules.Equational (specs_of simps')))) |
281 |>> snd |
291 |>> snd |
282 end; |
292 end; |
283 |
293 |
284 in |
294 in |
285 |
295 |