363 |
363 |
364 \noindent |
364 \noindent |
365 Again this is in contrast to the list-of-pairs representation which does not |
365 Again this is in contrast to the list-of-pairs representation which does not |
366 form a group. The technical importance of this fact is that for groups we |
366 form a group. The technical importance of this fact is that for groups we |
367 can rely on Isabelle/HOL's rich simplification infrastructure. This will |
367 can rely on Isabelle/HOL's rich simplification infrastructure. This will |
368 come in handy when we have to do calculations with permutations. However, |
368 come in handy when we have to do calculations with permutations. |
369 note that in this case Isabelle/HOL neglects well-entrenched mathematical |
369 Note that Isabelle/HOL defies standard conventions of mathematical notation |
370 terminology that associates with an additive group a commutative |
370 by using additive syntax even for non-commutative groups. Obviously, |
371 operation. Obviously, permutations are not commutative in general, because @{text |
371 composition of permutations is not commutative in general, because @{text |
372 "p + q \<noteq> q + p"}. However, it is quite difficult to work around this |
372 "\<pi>\<^sub>1 + \<pi>\<^sub>2 \<noteq> \<pi>\<^sub>2 + \<pi>\<^sub>1"}. But since the point of this paper is to implement the |
373 idiosyncrasy of Isabelle/HOL, unless we develop our own algebraic hierarchy |
373 nominal theory as smoothly as possible in Isabelle/HOL, we tolerate |
374 and infrastructure. But since the point of this paper is to implement the |
374 the non-standard notation in order to reuse the existing libraries. |
375 nominal theory as smoothly as possible in Isabelle/HOL, we will follow its |
|
376 characterisation of additive groups. |
|
377 |
375 |
378 By formalising permutations abstractly as functions, and using a single type |
376 By formalising permutations abstractly as functions, and using a single type |
379 for all atoms, we can now restate the \emph{permutation properties} from |
377 for all atoms, we can now restate the \emph{permutation properties} from |
380 \eqref{permprops} as just the two equations |
378 \eqref{permprops} as just the two equations |
381 |
379 |