36 We present a formalisation of this work that differs from our earlier approach |
36 We present a formalisation of this work that differs from our earlier approach |
37 in two important respects: First, instead of representing permutations as |
37 in two important respects: First, instead of representing permutations as |
38 lists of pairs of atoms, we now use a more abstract representation based on |
38 lists of pairs of atoms, we now use a more abstract representation based on |
39 functions. Second, whereas the earlier work modeled different sorts of atoms |
39 functions. Second, whereas the earlier work modeled different sorts of atoms |
40 using different types, we now introduce a unified atom type that includes all |
40 using different types, we now introduce a unified atom type that includes all |
41 sorts of atoms. Interestingly, we allow swappings, that is permutations build up by |
41 sorts of atoms. Interestingly, we allow swappings, that is permutations build from |
42 two atoms, to be ill-sorted. As a result of these design changes, we can iron |
42 two atoms, to be ill-sorted. As a result of these design changes, we can iron |
43 out inconveniences for the user, considerably simplify proofs and also |
43 out inconveniences for the user, considerably simplify proofs and also |
44 drastically reduce the amount of custom ML-code. Furthermore we can extend the |
44 drastically reduce the amount of custom ML-code. Furthermore we can extend the |
45 capabilities of Nominal Isabelle to deal with variables that carry additional |
45 capabilities of Nominal Isabelle to deal with variables that carry additional |
46 information. We end up with a pleasing and formalised theory of permutations |
46 information. We end up with a pleasing and formalised theory of permutations |