# HG changeset patch # User Christian Urban # Date 1291914608 0 # Node ID 431cf4e6a7e28fbbf4e4d8fe24b1126e5831594d # Parent 90779aefbf1ac75b2076d57081fed8600dd2d8a2 brought the paper to 20 pages plus one page appendix diff -r 90779aefbf1a -r 431cf4e6a7e2 Paper/Paper.thy --- a/Paper/Paper.thy Wed Dec 08 17:07:08 2010 +0000 +++ b/Paper/Paper.thy Thu Dec 09 17:10:08 2010 +0000 @@ -99,18 +99,13 @@ Binding multiple variables has interesting properties that cannot be captured easily by iterating single binders. For example in the case of type-schemes we do not want to make a distinction about the order of the bound variables. Therefore - we would like to regard the following two type-schemes as $\alpha$-equivalent + we would like to regard the first pair of type-schemes as $\alpha$-equivalent, + but assuming that @{text x}, @{text y} and @{text z} are distinct variables, + the second pair should \emph{not} be $\alpha$-equivalent: % \begin{equation}\label{ex1} - @{text "\{x, y}. x \ y \\<^isub>\ \{y, x}. x \ y"} - \end{equation} - % - \noindent - but assuming that @{text x}, @{text y} and @{text z} are distinct variables, - the following two should \emph{not} be $\alpha$-equivalent - % - \begin{equation}\label{ex2} - @{text "\{x, y}. x \ y \\<^isub>\ \{z}. z \ z"} + @{text "\{x, y}. x \ y \\<^isub>\ \{y, x}. x \ y"}\hspace{10mm} + @{text "\{x, y}. x \ y \\<^isub>\ \{z}. z \ z"} \end{equation} % \noindent @@ -139,7 +134,7 @@ \noindent we might not care in which order the assignments @{text "x = 3"} and - \mbox{@{text "y = 2"}} are given, but it would be unusual to regard + \mbox{@{text "y = 2"}} are given, but it would be often unusual to regard \eqref{one} as $\alpha$-equivalent with % \begin{center} @@ -382,7 +377,7 @@ The main improvement over Ott is that we introduce three binding modes (only one is present in Ott), provide formalised definitions for $\alpha$-equivalence and for free variables of our terms, and also derive a reasoning infrastructure - for our specifications inside Isabelle/HOL from ``first principles''. + for our specifications from ``first principles''. %\begin{figure} @@ -440,8 +435,8 @@ sort-respecting permutations of atoms. We will use the letters @{text "a, b, c, \"} to stand for atoms and @{text "p, q, \"} to stand for permutations. The purpose of atoms is to represent variables, be they bound or free. - The sorts of atoms can be used to represent different kinds of - variables, such as the term-, coercion- and type-variables in Core-Haskell. + %The sorts of atoms can be used to represent different kinds of + %variables, such as the term-, coercion- and type-variables in Core-Haskell. It is assumed that there is an infinite supply of atoms for each sort. In the interest of brevity, we shall restrict ourselves in what follows to only one sort of atoms. @@ -731,7 +726,7 @@ \end{center} \noindent - Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and + Now recall the examples shown in \eqref{ex1} and \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \ y)"} and @{text "({y, x}, y \ x)"} are $\alpha$-equivalent according to $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{res}}$ by taking @{text p} to @@ -800,9 +795,10 @@ \begin{center} \begin{tabular}{l} - @{thm (lhs) supp_Abs(1)[no_vars]} $=$ - @{thm supp_Abs(2)[no_vars]}, and\\ - @{thm supp_Abs(3)[where bs="as", no_vars]} + @{thm (lhs) supp_Abs(1)[no_vars]} $\;\;=\;\;$ + @{thm (lhs) supp_Abs(2)[no_vars]} $\;\;=\;\;$ @{thm (rhs) supp_Abs(2)[no_vars]}, and\\ + @{thm (lhs) supp_Abs(3)[where bs="as", no_vars]} $\;\;=\;\;$ + @{thm (rhs) supp_Abs(3)[where bs="as", no_vars]} \end{tabular} \end{center} \end{theorem} @@ -810,7 +806,7 @@ \noindent This theorem states that the bound names do not appear in the support. For brevity we omit the proof and again refer the reader to - our formalisation in Isabelle/HOL (or the appendix). + our formalisation in Isabelle/HOL. %\noindent %Below we will show the first equation. The others @@ -1010,20 +1006,19 @@ bound: \begin{center}\small - \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}} + \begin{tabular}{@ {}c@ {\hspace{7mm}}c@ {}} \begin{tabular}{@ {}l} \isacommand{nominal\_datatype} @{text lam} $=$\\ - \hspace{5mm}\phantom{$\mid$}~@{text "Var name"}\\ - \hspace{5mm}$\mid$~@{text "App lam lam"}\\ - \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}\\ - \hspace{24mm}\isacommand{bind} @{text x} \isacommand{in} @{text t}\\ + \hspace{2mm}\phantom{$\mid$}~@{text "Var name"}\\ + \hspace{2mm}$\mid$~@{text "App lam lam"}\\ + \hspace{2mm}$\mid$~@{text "Lam x::name t::lam"}~~\isacommand{bind} @{text x} \isacommand{in} @{text t}\\ \end{tabular} & \begin{tabular}{@ {}l@ {}} \isacommand{nominal\_datatype}~@{text ty} $=$\\ \hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\ \hspace{5mm}$\mid$~@{text "TFun ty ty"}\\ - \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}\\ - \hspace{29mm}\isacommand{bind (res)} @{text xs} \isacommand{in} @{text T}\\ + \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}~~% + \isacommand{bind (res)} @{text xs} \isacommand{in} @{text T}\\ \end{tabular} \end{tabular} \end{center} @@ -1118,7 +1113,7 @@ same time, we cannot have more than one binding function for a deep binder. Consequently we exclude specifications such as % - \begin{center} + \begin{center}\small \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}} @{text "Baz\<^isub>1 p::pat t::trm"} & \isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\ @@ -1921,13 +1916,13 @@ term-constructor \mbox{@{text "C\<^sup>\ x\<^isub>1\x\<^isub>r"}} the induction hypothesis requires us to establish the implications \eqref{weakprem}. The problem with these implications is that in general they are difficult to establish. - The reason is that we cannot make any assumption about the binders that might be in @{text "C\<^sup>\"}. + The reason is that we cannot make any assumption about the bound atoms that might be in @{text "C\<^sup>\"}. %%(for example we cannot assume the variable convention for them). In \cite{UrbanTasson05} we introduced a method for automatically strengthening weak induction principles for terms containing single binders. These stronger induction principles allow the user to make additional - assumptions about binders. + assumptions about bound atoms. %These additional assumptions amount to a formal %version of the informal variable convention for binders. To sketch how this strengthening extends to the case of multiple binders, we use as @@ -1947,7 +1942,7 @@ In \cite{UrbanTasson05} we showed how the weaker induction principles imply the stronger ones. This was done by some quite complicated, nevertheless automated, - induction proofs. In this paper we simplify this work by leveraging the automated proof + induction proof. In this paper we simplify this work by leveraging the automated proof methods from the function package of Isabelle/HOL. The reasoning principle these methods employ is well-founded induction. To use them in our setting, we have to discharge @@ -1956,8 +1951,8 @@ every induction step and the other is that we have covered all cases. As measures we use the size functions @{text "size_ty"}$^\alpha_{1..n}$, which we lifted in the previous section and which are - all well-founded. It is straightforward to establish that these measures decrease - in every induction step. + all well-founded. %It is straightforward to establish that these measures decrease + %in every induction step. What is left to show is that we covered all cases. To do so, we use a cases lemma derived for each type. For the terms in \eqref{letpat} @@ -2009,7 +2004,7 @@ clause @{text "bn (C x\<^isub>1 \ x\<^isub>r) = rhs"}, we define % \begin{center} - @{text "p \\<^bsub>bn\<^esub> (C x\<^isub>1 \ x\<^isub>r) \ C y\<^isub>1 \ y\<^isub>r"} \;\; with + @{text "p \\<^bsub>bn\<^esub> (C x\<^isub>1 \ x\<^isub>r) \ C y\<^isub>1 \ y\<^isub>r"} with $\begin{cases} \text{@{text "y\<^isub>i \ x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}}\\ \text{@{text "y\<^isub>i \ p \\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}}\\ @@ -2248,13 +2243,13 @@ this tool have also put forward (on paper) a definition for $\alpha$-equivalence of terms that can be specified in Ott. This definition is rather different from ours, not using any nominal techniques. To our - knowledge there is also no concrete mathematical result concerning this + knowledge there is no concrete mathematical result concerning this notion of $\alpha$-equivalence. Also the definition for the notion of free variables is work in progress. Although we were heavily inspired by the syntax of Ott, - its definition of $\alpha$-equivalence is unsuitable for our extension of + its definition of $\alpha$-equi\-valence is unsuitable 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 @@ -2340,18 +2335,19 @@ exist in Ott. We have tried out the extension with calculi such as Core-Haskell, type-schemes and approximately a dozen of other typical examples from programming - language research~\cite{SewellBestiary}. The code - will eventually become part of the next Isabelle distribution.\footnote{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}.} + language research~\cite{SewellBestiary}. + %The code + %will eventually become part of the next Isabelle distribution.\footnote{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}.} We have left out a discussion about how functions can be defined over $\alpha$-equated terms involving general binders. In earlier versions of Nominal - Isabelle \cite{UrbanBerghofer06} this turned out to be a thorny issue. We + Isabelle this turned out to be a thorny issue. We hope to do better this time by using the function package that has recently been implemented in Isabelle/HOL and also by restricting function - definitions to equivariant functions (for such functions we can + definitions to equivariant functions (for them we can provide more automation). %There are some restrictions we imposed in this paper that we would like to lift in @@ -2386,7 +2382,7 @@ %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 of the work on the Ott-tool. + also for patiently explaining some of the finer points of the Ott-tool.\\[-7mm] %Stephanie Weirich suggested to separate the subgrammars %of kinds and types in our Core-Haskell example. \\[-6mm] *} diff -r 90779aefbf1a -r 431cf4e6a7e2 Paper/document/root.tex --- a/Paper/document/root.tex Wed Dec 08 17:07:08 2010 +0000 +++ b/Paper/document/root.tex Thu Dec 09 17:10:08 2010 +0000 @@ -60,7 +60,7 @@ %-------------------- environment definitions ----------------- \newenvironment{proof-of}[1]{{\em Proof of #1:}}{} -\addtolength{\textwidth}{2mm} +%\addtolength{\textwidth}{2mm} \addtolength{\parskip}{-0.33mm} \begin{document}