1801 Isabelle distribution, but for the moment it can be downloaded from the |
1801 Isabelle distribution, but for the moment it can be downloaded from the |
1802 Mercurial repository linked at |
1802 Mercurial repository linked at |
1803 \href{http://isabelle.in.tum.de/nominal/download} |
1803 \href{http://isabelle.in.tum.de/nominal/download} |
1804 {http://isabelle.in.tum.de/nominal/download}. |
1804 {http://isabelle.in.tum.de/nominal/download}. |
1805 |
1805 |
1806 |
1806 We have left out a discussion about how functions can be defined |
|
1807 over alpha-equated terms. In earlier work \cite{UrbanBerghofer06} |
|
1808 this turned out to be a thorny issue in the old Nominal Isabelle. |
|
1809 We hope to do better this time by using the function package that |
|
1810 has recently been implemented in Isabelle/HOL and by restricting |
|
1811 function definitions to equivariant functions (for such functions |
|
1812 it is possible to provide more automation). |
|
1813 |
|
1814 There are some restrictions we imposed, like absence of nested type |
|
1815 definitions that allow one to specify the function kinds as |
|
1816 @{text "TFun string (ty list)"} instead of the unfolded version |
|
1817 @{text "TFun string ty_list"} in Figure~\ref{nominalcorehas}, that |
|
1818 can be easily lifted. They essentially amount only to a more |
|
1819 clever implementation. More interesting is lifting our restriction |
|
1820 about overlapping deep binders. |
|
1821 |
1807 Complication when the single scopedness restriction is lifted (two |
1822 Complication when the single scopedness restriction is lifted (two |
1808 overlapping permutations) |
1823 overlapping permutations) |
1809 |
1824 |
1810 Future work: distinct list abstraction |
1825 Future work: distinct list abstraction |
1811 |
1826 |
1812 TODO: function definitions: |
|
1813 |
|
1814 |
|
1815 \noindent |
1827 \noindent |
1816 {\bf Acknowledgements:} We are very grateful to Andrew Pitts for |
1828 {\bf Acknowledgements:} We are very grateful to Andrew Pitts for |
1817 many discussions about Nominal Isabelle. We thank Peter Sewell for |
1829 many discussions about Nominal Isabelle. We thank Peter Sewell for |
1818 making the informal notes \cite{SewellBestiary} available to us and |
1830 making the informal notes \cite{SewellBestiary} available to us and |
1819 also for patiently explaining some of the finer points about the abstract |
1831 also for patiently explaining some of the finer points about the abstract |