nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:2afee29cf81c
+:0c01dda0acd5
 \caption{The nominal datatype declaration for Core-Haskell. At the moment we
 do not support nested types; therefore we explicitly have to unfold the
 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
+point of our work is that having made such a declaration in Nominal Isabelle,
-automatically a reasoning infrastructure for Core-Haskell.\label{nominalcorehas}}
+one obtains automatically a reasoning infrastructure for Core-Haskell.
+\label{nominalcorehas}}
 \end{figure}
 *}
 (* @{thm "ACons_subst[no_vars]"}*)
 unpleasant. The hope is that the extension presented in this paper is a
 substantial improvement.
 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,
+documents from term-calculi specifications. For a subset of the
-Ott can also generate theorem prover code using a raw representation and
+specifications, Ott can also generate theorem prover code using a raw
-a locally nameless representation for terms. The developers of this tool
+representation and a locally nameless representation for terms. The
-have also put forward a definition for the notion of
+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
+techniques; it also aims for maximum expressivity, covering as many binding
-as many binding structures from programming language research as possible.
+structures from programming language research as possible.  Although we were
-Although we were heavily inspired by their syntax, their definition of
+heavily inspired by their syntax, their definition of alpha-equivalence was
-alpha-equivalence was no use at all for our extension of Nominal Isabelle.
+no use at all for our extension of Nominal Isabelle. First, it is far too
-First, it is far too complicated to be a basis for automated proofs
+complicated to be a basis for automated proofs implemented on the ML-level
-implemented on the ML-level of Isabelle/HOL. Second, it covers cases of
+of Isabelle/HOL. Second, it covers cases of binders depending on other
-binders depending on other binders, which just do not make sense for
+binders, which just do not make sense for our alpha-equated terms, and it
-our alpha-equated terms, and it also allows empty types that have no meaning
+also allows empty types that have no meaning in a HOL-based theorem
-in a HOL-based theorem prover. For features of Ott, like subgrammars, the
+prover. Because of how we set up our definitions, we had to impose some
-datatype infrastructure in Isabelle/HOL is unfortunately not powerful
+restrictions, like excluding overlapping deep binders, which are not present
-enough. On the other hand we are not aware that Ott can make any distinction
+in Ott. Our motivation is that we can still cover interesting term-calculi
-between our three different binding modes. Also, definitions for notions like
+from programming language research, like Core-Haskell. For features of Ott,
-free-variables are work in progress in 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)
 Future work: distinct list abstraction
 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
 making the informal notes \cite{SewellBestiary} available to us and
 also for patiently explaining some of the finer points about the abstract

changeset 1741	0c01dda0acd5
parent 1740	2afee29cf81c
child 1742	3f78dc600dce