equal
deleted
inserted
replaced
383 lemma swap_eqvt: |
383 lemma swap_eqvt: |
384 shows "p \<bullet> (a \<rightleftharpoons> b) = (p \<bullet> a \<rightleftharpoons> p \<bullet> b)" |
384 shows "p \<bullet> (a \<rightleftharpoons> b) = (p \<bullet> a \<rightleftharpoons> p \<bullet> b)" |
385 unfolding permute_perm_def |
385 unfolding permute_perm_def |
386 by (auto simp add: swap_atom expand_perm_eq) |
386 by (auto simp add: swap_atom expand_perm_eq) |
387 |
387 |
|
388 lemma uminus_eqvt: |
|
389 fixes p q::"perm" |
|
390 shows "p \<bullet> (- q) = - (p \<bullet> q)" |
|
391 unfolding permute_perm_def |
|
392 by (simp add: diff_minus minus_add add_assoc) |
388 |
393 |
389 subsection {* Permutations for functions *} |
394 subsection {* Permutations for functions *} |
390 |
395 |
391 instantiation "fun" :: (pt, pt) pt |
396 instantiation "fun" :: (pt, pt) pt |
392 begin |
397 begin |