287 |
287 |
288 (* provides perm_simp methods *) |
288 (* provides perm_simp methods *) |
289 use "nominal_permeq.ML" |
289 use "nominal_permeq.ML" |
290 setup Nominal_Permeq.setup |
290 setup Nominal_Permeq.setup |
291 |
291 |
|
292 ML {* |
|
293 val test1 = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) []; |
|
294 val test2 = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- |
|
295 (Scan.repeat (Args.const true))) [] |
|
296 *} |
|
297 |
292 method_setup perm_simp = |
298 method_setup perm_simp = |
293 {* Attrib.thms >> |
299 {* test1 -- test2 >> |
294 (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt thms ["The"]))) *} |
300 (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt [] consts))) *} |
295 {* pushes permutations inside *} |
301 {* pushes permutations inside *} |
296 |
302 |
297 method_setup perm_strict_simp = |
303 method_setup perm_strict_simp = |
298 {* Attrib.thms >> |
304 {* test1 -- test2 >> |
299 (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_strict_tac ctxt thms ["The"]))) *} |
305 (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL |
|
306 (Nominal_Permeq.eqvt_strict_tac ctxt thms consts))) *} |
300 {* pushes permutations inside, raises an error if it cannot solve all permutations *} |
307 {* pushes permutations inside, raises an error if it cannot solve all permutations *} |
301 |
308 |
302 declare [[trace_eqvt = true]] |
309 declare [[trace_eqvt = true]] |
303 |
310 |
304 lemma |
311 lemma |
367 |
374 |
368 declare [[trace_eqvt = false]] |
375 declare [[trace_eqvt = false]] |
369 |
376 |
370 text {* Problem: there is no raw eqvt-rule for The *} |
377 text {* Problem: there is no raw eqvt-rule for The *} |
371 lemma "p \<bullet> (THE x. P x) = foo" |
378 lemma "p \<bullet> (THE x. P x) = foo" |
372 apply(tactic {* Nominal_Permeq.eqvt_tac @{context} [] [@{const_name "The"}] 1*}) |
379 apply(perm_strict_simp exclude: The) |
373 apply(perm_simp) |
380 apply(perm_simp exclude: The) |
374 (* apply(perm_strict_simp) *) |
|
375 oops |
381 oops |
376 |
382 |
377 (* automatic equivariance procedure for |
383 (* automatic equivariance procedure for |
378 inductive definitions *) |
384 inductive definitions *) |
379 use "nominal_eqvt.ML" |
385 use "nominal_eqvt.ML" |