equal
deleted
inserted
replaced
280 |
280 |
281 lemma eqvt_bound: |
281 lemma eqvt_bound: |
282 shows "p \<bullet> unpermute p x \<equiv> x" |
282 shows "p \<bullet> unpermute p x \<equiv> x" |
283 unfolding unpermute_def by simp |
283 unfolding unpermute_def by simp |
284 |
284 |
285 ML {* @{const Trueprop} *} |
|
286 |
|
287 use "nominal_permeq.ML" |
285 use "nominal_permeq.ML" |
288 setup Nominal_Permeq.setup |
286 setup Nominal_Permeq.setup |
289 |
287 |
290 method_setup perm_simp = |
288 method_setup perm_simp = |
291 {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt thms))) *} |
289 {* Attrib.thms >> |
|
290 (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt thms ["The"]))) *} |
292 {* pushes permutations inside *} |
291 {* pushes permutations inside *} |
|
292 |
|
293 method_setup perm_strict_simp = |
|
294 {* Attrib.thms >> |
|
295 (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_strict_tac ctxt thms ["The"]))) *} |
|
296 {* pushes permutations inside, raises an error if it cannot solve all permutations *} |
293 |
297 |
294 declare [[trace_eqvt = true]] |
298 declare [[trace_eqvt = true]] |
295 |
299 |
296 lemma |
300 lemma |
297 fixes B::"'a::pt" |
301 fixes B::"'a::pt" |
350 shows "p \<bullet> (\<lambda>q::perm. q \<bullet> (r \<bullet> x)) = foo" |
354 shows "p \<bullet> (\<lambda>q::perm. q \<bullet> (r \<bullet> x)) = foo" |
351 apply (perm_simp) |
355 apply (perm_simp) |
352 oops |
356 oops |
353 |
357 |
354 lemma |
358 lemma |
355 fixes p q r::"perm" |
|
356 and x::"'a::pt" |
|
357 shows "p \<bullet> (q \<bullet> r \<bullet> x) = foo" |
|
358 apply(perm_simp) |
|
359 oops |
|
360 |
|
361 lemma |
|
362 fixes C D::"bool" |
359 fixes C D::"bool" |
363 shows "B (p \<bullet> (C = D))" |
360 shows "B (p \<bullet> (C = D))" |
364 apply(perm_simp) |
361 apply(perm_simp) |
365 oops |
362 oops |
366 |
363 |
367 declare [[trace_eqvt = false]] |
364 declare [[trace_eqvt = false]] |
368 |
365 |
369 text {* Problem: there is no raw eqvt-rule for The *} |
366 text {* Problem: there is no raw eqvt-rule for The *} |
370 lemma "p \<bullet> (THE x. P x) = foo" |
367 lemma "p \<bullet> (THE x. P x) = foo" |
371 apply(perm_simp) |
368 apply(perm_simp) |
|
369 (* apply(perm_strict_simp) *) |
372 oops |
370 oops |
373 |
371 |
374 |
372 |
375 end |
373 end |