# HG changeset patch # User Christian Urban # Date 1270094683 -7200 # Node ID 0c01dda0acd579969679aa1f31410be011ab7ebc # Parent 2afee29cf81cb4eab37cbb4010827d8938bc7c2e more on the conclusion diff -r 2afee29cf81c -r 0c01dda0acd5 Paper/Paper.thy --- a/Paper/Paper.thy Thu Apr 01 05:40:12 2010 +0200 +++ b/Paper/Paper.thy Thu Apr 01 06:04:43 2010 +0200 @@ -1707,8 +1707,9 @@ lists @{text "co_lst"}, @{text "assoc_lst"} and so on. This will be improved in a future version of Nominal Isabelle. Apart from that, the declaration follows closely the original in Figure~\ref{corehas}. The - point of our work is that having made such a declaration one obtains - automatically a reasoning infrastructure for Core-Haskell.\label{nominalcorehas}} + point of our work is that having made such a declaration in Nominal Isabelle, + one obtains automatically a reasoning infrastructure for Core-Haskell. + \label{nominalcorehas}} \end{figure} *} @@ -1762,30 +1763,47 @@ The most closely related work is the description of the Ott-tool \cite{ott-jfp}. This tool is a nifty front end for creating \LaTeX{} - documents from term-calculi specifications. For a subset of the specifications, - Ott can also generate theorem prover code using a raw representation and - a locally nameless representation for terms. The developers of this tool - have also put forward a definition for the notion of + documents from term-calculi specifications. For a subset of the + specifications, Ott can also generate theorem prover code using a raw + representation and a locally nameless representation for terms. The + developers of this tool have also put forward a definition for the notion of alpha-equivalence of the term-calculi that can be specified in Ott. This - definition is rather different from ours, not using any of the nominal - techniques; it also aims for maximum expressivity, covering - as many binding structures from programming language research as possible. - Although we were heavily inspired by their syntax, their definition of - alpha-equivalence was no use at all for our extension of Nominal Isabelle. - First, it is far too complicated to be a basis for automated proofs - implemented on the ML-level of Isabelle/HOL. Second, it covers cases of - binders depending on other binders, which just do not make sense for - our alpha-equated terms, and it also allows empty types that have no meaning - in a HOL-based theorem prover. For features of Ott, like subgrammars, the - datatype infrastructure in Isabelle/HOL is unfortunately not powerful - enough. On the other hand we are not aware that Ott can make any distinction - between our three different binding modes. Also, definitions for notions like - free-variables are work in progress in Ott. + definition is rather different from ours, not using any of the nominal + techniques; it also aims for maximum expressivity, covering as many binding + structures from programming language research as possible. Although we were + heavily inspired by their syntax, their definition of alpha-equivalence was + no use at all for our extension of Nominal Isabelle. First, it is far too + complicated to be a basis for automated proofs implemented on the ML-level + of Isabelle/HOL. Second, it covers cases of binders depending on other + binders, which just do not make sense for our alpha-equated terms, and it + also allows empty types that have no meaning in a HOL-based theorem + prover. Because of how we set up our definitions, we had to impose some + restrictions, like excluding overlapping deep binders, which are not present + in Ott. Our motivation is that we can still cover interesting term-calculi + from programming language research, like Core-Haskell. For features of Ott, + like subgrammars, the datatype infrastructure in Isabelle/HOL is + unfortunately not yet powerful enough. On the other hand we are not aware + that Ott can make any distinction between our three different binding + modes. Also, definitions for notions like free-variables are work in + progress in Ott. *} section {* Conclusion *} text {* + We have presented an extension for Nominal Isabelle in order to derive a + convenient reasoning infrastructure for term-constuctors binding multiple + variables at once. This extension can deal with term-calculi, such as + Core-Haskell. For such calculi, we can also derive strong induction + principles that have the usual variable already built in. At the moment we + can do so only with some manual help, but future work will automate them + completely. The code underlying this extension will become part of the + Isabelle distribution, but for the moment it can be downloaded from the + Mercurial repository linked at + \href{http://isabelle.in.tum.de/nominal/download} + {http://isabelle.in.tum.de/nominal/download}. + + Complication when the single scopedness restriction is lifted (two overlapping permutations) @@ -1793,12 +1811,7 @@ TODO: function definitions: - The formalisation presented here will eventually become part of the - Isabelle distribution, but for the moment it can be downloaded from - the Mercurial repository linked at - \href{http://isabelle.in.tum.de/nominal/download} - {http://isabelle.in.tum.de/nominal/download}.\medskip - + \noindent {\bf Acknowledgements:} We are very grateful to Andrew Pitts for many discussions about Nominal Isabelle. We thank Peter Sewell for