336 |
336 |
337 \noindent |
337 \noindent |
338 are \emph{equal}. We do not have to use the equivalence relation shown |
338 are \emph{equal}. We do not have to use the equivalence relation shown |
339 in~\eqref{permequ} to identify them, as we would if they had been represented |
339 in~\eqref{permequ} to identify them, as we would if they had been represented |
340 as lists of pairs. Another advantage of the function representation is that |
340 as lists of pairs. Another advantage of the function representation is that |
341 they form an (additive non-commutative) group provided we define |
341 they form a (non-commutative) group, provided we define |
342 |
342 |
343 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
343 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
344 \begin{tabular}{@ {}l} |
344 \begin{tabular}{@ {}l} |
345 @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm} |
345 @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm} |
346 @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm} |
346 @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm} |
361 \end{tabular} |
361 \end{tabular} |
362 \end{isabelle} |
362 \end{isabelle} |
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 we can rely on |
367 can rely on Isabelle/HOL's rich simplification infrastructure. This will |
367 Isabelle/HOL's existing simplification infrastructure for groups, which 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---@{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 |
890 \emph{subtypes} of the generic atom type that only include atoms of a single |
888 \emph{subtypes} of the generic atom type that only include atoms of a single |
891 specific sort. We call such subtypes \emph{concrete atom types}. |
889 specific sort. We call such subtypes \emph{concrete atom types}. |
892 |
890 |
893 The following Isabelle/HOL command defines a concrete atom type called |
891 The following Isabelle/HOL command defines a concrete atom type called |
894 \emph{name}, which consists of atoms whose sort equals the string @{term |
892 \emph{name}, which consists of atoms whose sort equals the string @{term |
895 "''name''"}. |
893 "''Thy.name''"}. |
896 |
894 |
897 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
895 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
898 \isacommand{typedef}\ \ @{typ name} = @{term "{a. sort\<iota> a = ''name''}"} |
896 \isacommand{typedef}\ \ @{typ name} = @{term "{a. sort\<iota> a = ''Thy.name''}"} |
899 \end{isabelle} |
897 \end{isabelle} |
900 |
898 |
901 \noindent |
899 \noindent |
902 This command automatically generates injective functions that map from the |
900 This command automatically generates injective functions that map from the |
903 concrete atom type into the generic atom type and back, called |
901 concrete atom type into the generic atom type and back, called |