Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Paper/Paper.thy
changeset 1741 0c01dda0acd5
parent 1740 2afee29cf81c
child 1742 3f78dc600dce 
--- 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
nominal2