335 |
335 |
336 \noindent |
336 \noindent |
337 are \emph{equal}. We do not have to use the equivalence relation shown |
337 are \emph{equal}. We do not have to use the equivalence relation shown |
338 in~\eqref{permequ} to identify them, as we would if they had been represented |
338 in~\eqref{permequ} to identify them, as we would if they had been represented |
339 as lists of pairs. Another advantage of the function representation is that |
339 as lists of pairs. Another advantage of the function representation is that |
340 they form an (additive non-commutative) group provided we define |
340 they form a (non-commutative) group, provided we define |
341 |
341 |
342 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
342 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
343 \begin{tabular}{@ {}l} |
343 \begin{tabular}{@ {}l} |
344 @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm} |
344 @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm} |
345 @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm} |
345 @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm} |
360 \end{tabular} |
360 \end{tabular} |
361 \end{isabelle} |
361 \end{isabelle} |
362 |
362 |
363 \noindent |
363 \noindent |
364 Again this is in contrast to the list-of-pairs representation which does not |
364 Again this is in contrast to the list-of-pairs representation which does not |
365 form a group. The technical importance of this fact is that for groups we |
365 form a group. The technical importance of this fact is that we can rely on |
366 can rely on Isabelle/HOL's rich simplification infrastructure. This will |
366 Isabelle/HOL's existing simplification infrastructure for groups, which will |
367 come in handy when we have to do calculations with permutations. However, |
367 come in handy when we have to do calculations with permutations. |
368 note that in this case Isabelle/HOL neglects well-entrenched mathematical |
368 Note that Isabelle/HOL defies standard conventions of mathematical notation |
369 terminology that associates with an additive group a commutative |
369 by using additive syntax even for non-commutative groups. Obviously, |
370 operation. Obviously, permutations are not commutative in general---@{text |
370 composition of permutations is not commutative in general---@{text |
371 "p + q \<noteq> q + p"}. However, it is quite difficult to work around this |
371 "\<pi>\<^sub>1 + \<pi>\<^sub>2 \<noteq> \<pi>\<^sub>2 + \<pi>\<^sub>1"}. But since the point of this paper is to implement the |
372 idiosyncrasy of Isabelle/HOL, unless we develop our own algebraic hierarchy |
372 nominal theory as smoothly as possible in Isabelle/HOL, we tolerate |
373 and infrastructure. But since the point of this paper is to implement the |
373 the non-standard notation in order to reuse the existing libraries. |
374 nominal theory as smoothly as possible in Isabelle/HOL, we will follow its |
|
375 characterisation of additive groups. |
|
376 |
374 |
377 By formalising permutations abstractly as functions, and using a single type |
375 By formalising permutations abstractly as functions, and using a single type |
378 for all atoms, we can now restate the \emph{permutation properties} from |
376 for all atoms, we can now restate the \emph{permutation properties} from |
379 \eqref{permprops} as just the two equations |
377 \eqref{permprops} as just the two equations |
380 |
378 |