53 that might be bound. Multiple sorts are necessary for being able to |
53 that might be bound. Multiple sorts are necessary for being able to |
54 represent different kinds of variables. For example, in the language Mini-ML |
54 represent different kinds of variables. For example, in the language Mini-ML |
55 there are bound term variables and bound type variables; each kind needs to |
55 there are bound term variables and bound type variables; each kind needs to |
56 be represented by a different sort of atoms. |
56 be represented by a different sort of atoms. |
57 |
57 |
58 Unfortunately, the type system of Isabelle/HOL is not a good fit for the way |
58 In our formalisation of the nominal logic work, we have to make a design decision |
59 atoms and sorts are used in the original formulation of the nominal logic work. |
59 about how to represent sorted atoms and sort-respecting permutations. One possibility |
60 The reason is that one has to ensure that permutations are sort-respecting. |
60 is to |
61 This was done implicitly in the original nominal logic work \cite{Pitts03}. |
61 |
|
62 |
|
63 |
|
64 % Unfortunately, the type system of Isabelle/HOL is not a good fit for the way |
|
65 % atoms and sorts are used in the original formulation of the nominal logic work. |
|
66 % The reason is that one has to ensure that permutations are sort-respecting. |
|
67 % This was done implicitly in the original nominal logic work \cite{Pitts03}. |
62 |
68 |
63 |
69 |
64 Isabelle used the two-place permutation operation with the generic type |
70 Isabelle used the two-place permutation operation with the generic type |
65 |
71 |
66 @{text [display,indent=10] "_ \<bullet> _ :: (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} |
72 @{text [display,indent=10] "_ \<bullet> _ :: (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} |