422 sort-respecting permutations of atoms. We will use the letters @{text "a, |
422 sort-respecting permutations of atoms. We will use the letters @{text "a, |
423 b, c, \<dots>"} to stand for atoms and @{text "p, q, \<dots>"} to stand for |
423 b, c, \<dots>"} to stand for atoms and @{text "p, q, \<dots>"} to stand for |
424 permutations. The sorts of atoms can be used to represent different kinds of |
424 permutations. The sorts of atoms can be used to represent different kinds of |
425 variables, such as the term-, coercion- and type-variables in Core-Haskell. |
425 variables, such as the term-, coercion- and type-variables in Core-Haskell. |
426 It is assumed that there is an infinite supply of atoms for each |
426 It is assumed that there is an infinite supply of atoms for each |
427 sort. However, in the intrest of brevity, we shall restrict ourselves |
427 sort. However, in the interest of brevity, we shall restrict ourselves |
428 in what follows to only one sort of atoms. |
428 in what follows to only one sort of atoms. |
429 |
429 |
430 Permutations are bijective functions from atoms to atoms that are |
430 Permutations are bijective functions from atoms to atoms that are |
431 the identity everywhere except on a finite number of atoms. There is a |
431 the identity everywhere except on a finite number of atoms. There is a |
432 two-place permutation operation written |
432 two-place permutation operation written |
1030 coerces a name into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This allows |
1030 coerces a name into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This allows |
1031 us to treat binders of different atom type uniformly. |
1031 us to treat binders of different atom type uniformly. |
1032 |
1032 |
1033 As will shortly become clear, we cannot return an atom in a binding function |
1033 As will shortly become clear, we cannot return an atom in a binding function |
1034 that is also bound in the corresponding term-constructor. That means in the |
1034 that is also bound in the corresponding term-constructor. That means in the |
1035 example above that the term-constructors @{text PVar} and @{text PTup} must not have a |
1035 example above that the term-constructors @{text PVar} and @{text PTup} may not have a |
1036 binding clause. In the version of Nominal Isabelle described here, we also adopted |
1036 binding clause. In the version of Nominal Isabelle described here, we also adopted |
1037 the restriction from the Ott-tool that binding functions can only return: |
1037 the restriction from the Ott-tool that binding functions can only return: |
1038 the empty set or empty list (as in case @{text PNil}), a singleton set or singleton |
1038 the empty set or empty list (as in case @{text PNil}), a singleton set or singleton |
1039 list containing an atom (case @{text PVar}), or unions of atom sets or appended atom |
1039 list containing an atom (case @{text PVar}), or unions of atom sets or appended atom |
1040 lists (case @{text PTup}). This restriction will simplify definitions and |
1040 lists (case @{text PTup}). This restriction will simplify definitions and |
2017 hope to do better this time by using the function package that has recently |
2017 hope to do better this time by using the function package that has recently |
2018 been implemented in Isabelle/HOL and also by restricting function |
2018 been implemented in Isabelle/HOL and also by restricting function |
2019 definitions to equivariant functions (for such functions it is possible to |
2019 definitions to equivariant functions (for such functions it is possible to |
2020 provide more automation). |
2020 provide more automation). |
2021 |
2021 |
2022 There are some restrictions we imposed in this paper, we like to lift in |
2022 There are some restrictions we imposed in this paper, that we would like to lift in |
2023 future work. One is the exclusion of nested datatype definitions. Nested |
2023 future work. One is the exclusion of nested datatype definitions. Nested |
2024 datatype definitions allow one to specify, for instance, the function kinds |
2024 datatype definitions allow one to specify, for instance, the function kinds |
2025 in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded |
2025 in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded |
2026 version @{text "TFun string ty_list"} in Figure~\ref{nominalcorehas}. For |
2026 version @{text "TFun string ty_list"} in Figure~\ref{nominalcorehas}. For |
2027 them we need a more clever implementation than we have at the moment. |
2027 them we need a more clever implementation than we have at the moment. |