285 |
285 |
286 (* provides perm_simp methods *) |
286 (* provides perm_simp methods *) |
287 use "nominal_permeq.ML" |
287 use "nominal_permeq.ML" |
288 setup Nominal_Permeq.setup |
288 setup Nominal_Permeq.setup |
289 |
289 |
290 ML {* |
|
291 val add_thms = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) []; |
|
292 val exclude_consts = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- |
|
293 (Scan.repeat (Args.const true))) [] |
|
294 |
|
295 val parser = |
|
296 add_thms -- exclude_consts || |
|
297 exclude_consts -- add_thms >> swap |
|
298 *} |
|
299 |
|
300 method_setup perm_simp = |
290 method_setup perm_simp = |
301 {* parser >> |
291 {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *} |
302 (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL |
292 {* pushes permutations inside. *} |
303 (Nominal_Permeq.eqvt_tac ctxt [] consts))) *} |
|
304 {* pushes permutations inside *} |
|
305 |
293 |
306 method_setup perm_strict_simp = |
294 method_setup perm_strict_simp = |
307 {* parser >> |
295 {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *} |
308 (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL |
296 {* pushes permutations inside, raises an error if it cannot solve all permutations. *} |
309 (Nominal_Permeq.eqvt_strict_tac ctxt thms consts))) *} |
|
310 {* pushes permutations inside, raises an error if it cannot solve all permutations *} |
|
311 |
297 |
312 declare [[trace_eqvt = true]] |
298 declare [[trace_eqvt = true]] |
313 |
299 |
314 lemma |
300 lemma |
315 fixes B::"'a::pt" |
301 fixes B::"'a::pt" |