27 \title{Proof Pearl: A New Foundation for Nominal Isabelle}

    27 \title{Implementing the Nominal Logic Work in Isabelle/HOL}

    34 notions of permutation and support. The engineering challenge is to smoothly

    34 notions of atoms, permutations and support. The engineering challenge

    35 adapt this theory to a theorem prover environment, in our case Isabelle/HOL.

    35 is to smoothly adapt this theory to a theorem prover environment, in our case

    36 We present a formalisation of this work that differs from our earlier approach

    36 Isabelle/HOL.  We present a formalisation of this work that is based on a

    37 in two important respects: First, instead of representing permutations as

    37 unified atom type (that includes all sorts of atoms) and that represents

    38 lists of pairs of atoms, we now use a more abstract representation based on

    38 permutations by bijective functions from atoms to atoms. Interestingly, we

    39 functions.  Second, whereas the earlier work modeled different sorts of atoms

    39 allow swappings, which are permutations build from two atoms, to be

    40 using different types, we now introduce a unified atom type that includes all

    40 ill-sorted.  Furthermore we can extend the nominal logic with names that carry

    41 sorts of atoms. Interestingly, we allow swappings, that is permutations build from

    41 additional information.

    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

    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

    46 information. We end up with a pleasing and formalised theory of permutations

    47 and support, on which we can build an improved and more powerful version of

    48 Nominal Isabelle.