equal
deleted
inserted
replaced
214 with the large amounts of custom ML-code for generating multiple variants |
214 with the large amounts of custom ML-code for generating multiple variants |
215 for some basic definitions. The result is that we can implement a pleasingly |
215 for some basic definitions. The result is that we can implement a pleasingly |
216 simple formalisation of the nominal logic work.\smallskip |
216 simple formalisation of the nominal logic work.\smallskip |
217 |
217 |
218 \noindent |
218 \noindent |
219 {\bf Contributions of the paper:} Our use of a single atom type for representing |
219 {\bf Contributions of the paper:} The main contribution of this paper is in |
220 atoms of different sorts and of functions for representing |
220 showing an example of how theorem proving tools can be improved by getting |
221 permutations is not novel, but drastically reduces the number of type classes to just |
221 the right level of abstraction for the underlying theory. |
222 two (permutation types and finitely supported types) that we need in order |
222 The novel |
223 reason abstractly about properties from the nominal logic work. The novel |
223 technical contribution is a mechanism for dealing with |
224 technical contribution of this paper is a mechanism for dealing with |
|
225 ``Church-style'' lambda-terms \cite{Church40} and HOL-based languages |
224 ``Church-style'' lambda-terms \cite{Church40} and HOL-based languages |
226 \cite{PittsHOL4} where variables and variable binding depend on type |
225 \cite{PittsHOL4} where variables and variable binding depend on type |
227 annotations. |
226 annotations. |
228 *} |
227 *} |
229 |
228 |
499 %section { * Equivariance * } |
498 %section { * Equivariance * } |
500 % |
499 % |
501 %text { * |
500 %text { * |
502 |
501 |
503 One huge advantage of using bijective permutation functions (as opposed to |
502 One huge advantage of using bijective permutation functions (as opposed to |
504 non-bijective renaming substitutions employed in traditional works syntax) is |
503 non-bijective renaming substitutions employed in traditional works on syntax) is |
505 the property of \emph{equivariance} |
504 the property of \emph{equivariance} |
506 and the fact that most HOL-functions (this includes constants) whose argument |
505 and the fact that most HOL-functions (this includes constants) whose argument |
507 and result types are permutation types satisfy this property: |
506 and result types are permutation types satisfy this property: |
508 |
507 |
509 \begin{definition}\label{equivariance} |
508 \begin{definition}\label{equivariance} |
888 \emph{subtypes} of the generic atom type that only include atoms of a single |
887 \emph{subtypes} of the generic atom type that only include atoms of a single |
889 specific sort. We call such subtypes \emph{concrete atom types}. |
888 specific sort. We call such subtypes \emph{concrete atom types}. |
890 |
889 |
891 The following Isabelle/HOL command defines a concrete atom type called |
890 The following Isabelle/HOL command defines a concrete atom type called |
892 \emph{name}, which consists of atoms whose sort equals the string @{term |
891 \emph{name}, which consists of atoms whose sort equals the string @{term |
893 "''Thy.name''"}. |
892 "''name''"}. |
894 |
893 |
895 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
894 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
896 \isacommand{typedef}\ \ @{typ name} = @{term "{a. sort\<iota> a = ''Thy.name''}"} |
895 \isacommand{typedef}\ \ @{typ name} = @{term "{a. sort\<iota> a = ''name''}"} |
897 \end{isabelle} |
896 \end{isabelle} |
898 |
897 |
899 \noindent |
898 \noindent |
900 This command automatically generates injective functions that map from the |
899 This command automatically generates injective functions that map from the |
901 concrete atom type into the generic atom type and back, called |
900 concrete atom type into the generic atom type and back, called |