65 |
65 |
66 \noindent |
66 \noindent |
67 At its core Nominal Isabelle is based on the nominal logic work by Pitts at |
67 At its core Nominal Isabelle is based on the nominal logic work by Pitts at |
68 al \cite{GabbayPitts02,Pitts03}, whose most basic notion is a |
68 al \cite{GabbayPitts02,Pitts03}, whose most basic notion is a |
69 sort-respecting permutation operation defined over a countably infinite |
69 sort-respecting permutation operation defined over a countably infinite |
70 collection of sorted atoms. The atoms are used for representing variable names |
70 collection of sorted atoms. The aim of this paper is to describe how to |
71 that might be bound or free. Multiple sorts are necessary for being able to |
71 adapt this work so that it can be implemented in a theorem prover based |
72 represent different kinds of variables. For example, in the language Mini-ML |
72 on Higher-Order Logic (HOL). For this we present the definition we made |
73 there are bound term variables in lambda abstractions and bound type variables in |
73 in the implementation and also review many proofs. There are a two main |
74 type schemes. In order to be able to separate them, each kind of variables needs to be |
74 design choices to be made. One is |
75 represented by a different sort of atoms. |
75 how to represent sorted atoms. We opt here for a single unified atom type to |
|
76 represent atoms of different sorts. The other is how to present sort-respecting |
|
77 permutations. For them we use the standard technique of |
|
78 HOL-formalisations of introducing an appropriate substype of functions from |
|
79 atoms to atoms. |
|
80 |
76 |
81 |
77 The nominal logic work has been the starting point for a number of proving |
82 The nominal logic work has been the starting point for a number of proving |
78 infrastructures, most notable by Norrish \cite{norrish04} in HOL4, by |
83 infrastructures, most notable by Norrish \cite{norrish04} in HOL4, by |
79 Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and the work by Urban |
84 Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and the work by Urban |
80 and Berghofer in Isabelle/HOL \cite{Urban08}. Its key attraction is a very |
85 and Berghofer in Isabelle/HOL \cite{Urban08}. Its key attraction is a very |
149 |
154 |
150 |
155 |
151 |
156 |
152 |
157 |
153 Two binders |
158 Two binders |
|
159 |
|
160 A preliminary version |
154 *} |
161 *} |
155 |
162 |
156 section {* Sorted Atoms and Sort-Respecting Permutations *} |
163 section {* Sorted Atoms and Sort-Respecting Permutations *} |
157 |
164 |
158 text {* |
165 text {* |
159 The two most basic notions in the nominal logic work are a countably |
166 The two most basic notions in the nominal logic work are a countably |
160 infinite collection of sorted atoms and sort-respecting permutations of atoms. |
167 infinite collection of sorted atoms and sort-respecting permutations of atoms. |
|
168 The atoms are used for representing variable names |
|
169 that might be bound or free. Multiple sorts are necessary for being able to |
|
170 represent different kinds of variables. For example, in the language Mini-ML |
|
171 there are bound term variables in lambda abstractions and bound type variables in |
|
172 type schemes. In order to be able to separate them, each kind of variables needs to be |
|
173 represented by a different sort of atoms. |
|
174 |
161 The existing nominal logic work usually leaves implicit |
175 The existing nominal logic work usually leaves implicit |
162 the sorting information for atoms and as far as we know leaves out a |
176 the sorting information for atoms and as far as we know leaves out a |
163 description of how sorts are represented. In our formalisation, we |
177 description of how sorts are represented. In our formalisation, we |
164 therefore have to make a design decision about how to implement sorted atoms |
178 therefore have to make a design decision about how to implement sorted atoms |
165 and sort-respecting permutations. One possibility, which we described in |
179 and sort-respecting permutations. One possibility, which we described in |