equal
deleted
inserted
replaced
283 |
283 |
284 lemma eqvt_bound: |
284 lemma eqvt_bound: |
285 shows "p \<bullet> unpermute p x \<equiv> x" |
285 shows "p \<bullet> unpermute p x \<equiv> x" |
286 unfolding unpermute_def by simp |
286 unfolding unpermute_def by simp |
287 |
287 |
|
288 (* provides perm_simp methods *) |
288 use "nominal_permeq.ML" |
289 use "nominal_permeq.ML" |
289 setup Nominal_Permeq.setup |
290 setup Nominal_Permeq.setup |
290 |
|
291 use "nominal_eqvt.ML" |
|
292 |
|
293 |
291 |
294 method_setup perm_simp = |
292 method_setup perm_simp = |
295 {* Attrib.thms >> |
293 {* Attrib.thms >> |
296 (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt thms ["The"]))) *} |
294 (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt thms ["The"]))) *} |
297 {* pushes permutations inside *} |
295 {* pushes permutations inside *} |
373 lemma "p \<bullet> (THE x. P x) = foo" |
371 lemma "p \<bullet> (THE x. P x) = foo" |
374 apply(perm_simp) |
372 apply(perm_simp) |
375 (* apply(perm_strict_simp) *) |
373 (* apply(perm_strict_simp) *) |
376 oops |
374 oops |
377 |
375 |
378 |
376 (* automatic equivariance procedure for |
|
377 inductive definitions *) |
|
378 use "nominal_eqvt.ML" |
379 |
379 |
380 end |
380 end |