# HG changeset patch # User Christian Urban # Date 1313509689 -7200 # Node ID 5df574281b69d1cc1ae2cd3dd1858e80358b7ce1 # Parent eab84ac2603be6ee124a8f43bccc95269501ded3 more on the intro and correct style-files diff -r eab84ac2603b -r 5df574281b69 LMCS-Paper/Paper.thy --- a/LMCS-Paper/Paper.thy Mon Aug 15 17:42:35 2011 +0200 +++ b/LMCS-Paper/Paper.thy Tue Aug 16 17:48:09 2011 +0200 @@ -59,11 +59,15 @@ section {* Introduction *} text {* + So far, Nominal Isabelle provided a mechanism for constructing alpha-equated + terms, for example lambda-terms - So far, Nominal Isabelle provided a mechanism for constructing - $\alpha$-equated terms, for example lambda-terms, - @{text "t ::= x | t t | \x. t"}, - where free and bound variables have names. For such $\alpha$-equated terms, + \[ + @{text "t ::= x | t t | \x. t"} + \]\smallskip + + \noindent + where free and bound variables have names. For such alpha-equated terms, Nominal Isabelle derives automatically a reasoning infrastructure that has been used successfully in formalisations of an equivalence checking algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed @@ -73,75 +77,71 @@ formalisations in the locally-nameless approach to binding \cite{SatoPollack10}. - However, Nominal Isabelle has fared less well in a formalisation of - the algorithm W \cite{UrbanNipkow09}, where types and type-schemes are, + However, Nominal Isabelle has fared less well in a formalisation of the + algorithm W \cite{UrbanNipkow09}, where types and type-schemes are, respectively, of the form - % + \begin{equation}\label{tysch} \begin{array}{l} - @{text "T ::= x | T \ T"}\hspace{9mm} + @{text "T ::= x | T \ T"}\hspace{15mm} @{text "S ::= \{x\<^isub>1,\, x\<^isub>n}. T"} \end{array} - \end{equation} - % + \end{equation}\smallskip + \noindent and the @{text "\"}-quantification binds a finite (possibly empty) set of type-variables. While it is possible to implement this kind of more general binders by iterating single binders, this leads to a rather clumsy - formalisation of W. - The need of iterating single binders is also one reason - why Nominal Isabelle - and similar theorem provers that only provide - mechanisms for binding single variables - has not fared extremely well with the - more advanced tasks in the POPLmark challenge \cite{challenge05}, because - also there one would like to bind multiple variables at once. + formalisation of W. The need of iterating single binders is also one reason + why Nominal Isabelle and similar theorem provers that only provide + mechanisms for binding single variables has not fared extremely well with + the more advanced tasks in the POPLmark challenge \cite{challenge05}, + because also there one would like to bind multiple variables at once. 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 first pair of 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: - % + the second pair should \emph{not} be alpha-equivalent: + \begin{equation}\label{ex1} @{text "\{x, y}. x \ y \\<^isub>\ \{y, x}. y \ x"}\hspace{10mm} @{text "\{x, y}. x \ y \\<^isub>\ \{z}. z \ z"} - \end{equation} - % + \end{equation}\smallskip + \noindent - Moreover, we like to regard type-schemes as $\alpha$-equivalent, if they differ + Moreover, we like to regard type-schemes as alpha-equivalent, if they differ only on \emph{vacuous} binders, such as - % + \begin{equation}\label{ex3} @{text "\{x}. x \ y \\<^isub>\ \{x, z}. x \ y"} - \end{equation} - % + \end{equation}\smallskip + \noindent where @{text z} does not occur freely in the type. In this paper we will - give a general binding mechanism and associated notion of $\alpha$-equivalence + give a general binding mechanism and associated notion of alpha-equivalence that can be used to faithfully represent this kind of binding in Nominal - Isabelle. - The difficulty of finding the right notion for $\alpha$-equivalence + Isabelle. The difficulty of finding the right notion for alpha-equivalence can be appreciated in this case by considering that the definition given by - Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). + Leroy in \cite[Page ???]{Leroy92} is incorrect (it omits a side-condition). - However, the notion of $\alpha$-equivalence that is preserved by vacuous + However, the notion of alpha-equivalence that is preserved by vacuous binders is not always wanted. For example in terms like - % + \begin{equation}\label{one} @{text "\ x = 3 \ y = 2 \ x - y \"} - \end{equation} + \end{equation}\smallskip \noindent we might not care in which order the assignments @{text "x = 3"} and - \mbox{@{text "y = 2"}} are given, but it would be often unusual to regard - \eqref{one} as $\alpha$-equivalent with - % - \begin{center} + \mbox{@{text "y = 2"}} are given, but it would be often unusual (particularly + in strict languages) to regard \eqref{one} as alpha-equivalent with + + \[ @{text "\ x = 3 \ y = 2 \ z = foo \ x - y \"} - \end{center} - % + \]\smallskip + \noindent Therefore we will also provide a separate binding mechanism for cases in which the order of binders does not matter, but the ``cardinality'' of the @@ -150,134 +150,129 @@ However, we found that this is still not sufficient for dealing with language constructs frequently occurring in programming language research. For example in @{text "\"}s containing patterns like - % + \begin{equation}\label{two} @{text "\ (x, y) = (3, 2) \ x - y \"} - \end{equation} - % + \end{equation}\smallskip + \noindent we want to bind all variables from the pattern inside the body of the $\mathtt{let}$, but we also care about the order of these variables, since - we do not want to regard \eqref{two} as $\alpha$-equivalent with - % - \begin{center} + we do not want to regard \eqref{two} as alpha-equivalent with + + \[ @{text "\ (y, x) = (3, 2) \ x - y \"} - \end{center} - % + \]\smallskip + \noindent As a result, we provide three general binding mechanisms each of which binds multiple variables at once, and let the user chose which one is intended - in a formalisation. - %%when formalising a term-calculus. + when formalising a term-calculus. By providing these general binding mechanisms, however, we have to work around a problem that has been pointed out by Pottier \cite{Pottier06} and Cheney \cite{Cheney05}: in @{text "\"}-constructs of the form - % - \begin{center} + + \[ @{text "\ x\<^isub>1 = t\<^isub>1 \ \ \ x\<^isub>n = t\<^isub>n \ s \"} - \end{center} - % + \]\smallskip + \noindent - we care about the - information that there are as many bound variables @{text + we care about the information that there are as many bound variables @{text "x\<^isub>i"} as there are @{text "t\<^isub>i"}. We lose this information if we represent the @{text "\"}-constructor by something like - % - \begin{center} + + \[ @{text "\ (\x\<^isub>1\x\<^isub>n . s) [t\<^isub>1,\,t\<^isub>n]"} - \end{center} - % + \]\smallskip + \noindent where the notation @{text "\_ . _"} indicates that the list of @{text "x\<^isub>i"} becomes bound in @{text s}. In this representation the term - \mbox{@{text "\ (\x . s) [t\<^isub>1, t\<^isub>2]"}} is a perfectly legal - instance, but the lengths of the two lists do not agree. To exclude such - terms, additional predicates about well-formed terms are needed in order to - ensure that the two lists are of equal length. This can result in very messy - reasoning (see for example~\cite{BengtsonParow09}). To avoid this, we will - allow type specifications for @{text "\"}s as follows - % - \begin{center} - \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}cl} - @{text trm} & @{text "::="} & @{text "\"} - & @{text "|"} @{text "\ as::assn s::trm"}\hspace{2mm} - \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}\\%%%[1mm] - @{text assn} & @{text "::="} & @{text "\"} - & @{text "|"} @{text "\ name trm assn"} - \end{tabular} - \end{center} - % + \mbox{@{text "\ (\x . s) [t\<^isub>1, t\<^isub>2]"}} is a perfectly + legal instance, but the lengths of the two lists do not agree. To exclude + such terms, additional predicates about well-formed terms are needed in + order to ensure that the two lists are of equal length. This can result in + very messy reasoning (see for example~\cite{BengtsonParow09}). To avoid + this, we will allow type specifications for @{text "\"}s as follows + + \[ + \mbox{\begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}ll} + @{text trm} & @{text "::="} & @{text "\"} \\ + & @{text "|"} & @{text "\ as::assn s::trm"}\hspace{2mm} + \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}\\[1mm] + @{text assn} & @{text "::="} & @{text "\"}\\ + & @{text "|"} & @{text "\ name trm assn"} + \end{tabular}} + \]\smallskip + \noindent where @{text assn} is an auxiliary type representing a list of assignments and @{text bn} an auxiliary function identifying the variables to be bound by the @{text "\"}. This function can be defined by recursion over @{text assn} as follows - % - \begin{center} - @{text "bn(\) ="} @{term "{}"} \hspace{5mm} + + \[ + @{text "bn(\) ="} @{term "{}"} \hspace{10mm} @{text "bn(\ x t as) = {x} \ bn(as)"} - \end{center} - % + \]\smallskip + \noindent The scope of the binding is indicated by labels given to the types, for example @{text "s::trm"}, and a binding clause, in this case \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding - clause states that all the names the function @{text - "bn(as)"} returns should be bound in @{text s}. This style of specifying terms and bindings is heavily - inspired by the syntax of the Ott-tool \cite{ott-jfp}. - - Though, Ott - has only one binding mode, namely the one where the order of - binders matters. Consequently, type-schemes with binding sets - of names cannot be modelled in Ott. + clause states that all the names the function @{text "bn(as)"} returns + should be bound in @{text s}. This style of specifying terms and bindings + is heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. Our work + extends Ott in several aspects: one is that we support three binding + modes---Ott has only one, namely the one where the order of binders matters. + Another is that our reasoning infrastructure, like the notion of support and + strong induction principles, is derived from first principles within the + Isabelle/HOL theorem prover. However, we will not be able to cope with all specifications that are - allowed by Ott. One reason is that Ott lets the user specify ``empty'' - types like @{text "t ::= t t | \x. t"} - where no clause for variables is given. Arguably, such specifications make - some sense in the context of Coq's type theory (which Ott supports), but not - at all in a HOL-based environment where every datatype must have a non-empty - set-theoretic model. % \cite{Berghofer99}. + allowed by Ott. One reason is that Ott lets the user specify ``empty'' types + like \mbox{@{text "t ::= t t | \x. t"}} where no clause for variables is + given. Arguably, such specifications make some sense in the context of Coq's + type theory (which Ott supports), but not at all in a HOL-based environment + where every datatype must have a non-empty set-theoretic model + \cite{Berghofer99}. Another reason is that we establish the reasoning + infrastructure for alpha-\emph{equated} terms. In contrast, Ott produces a + reasoning infrastructure in Isabelle/HOL for \emph{non}-alpha-equated, or + ``raw'', terms. While our alpha-equated terms and the raw terms produced by + Ott use names for bound variables, there is a key difference: working with + alpha-equated terms means, for example, that the two type-schemes - Another reason is that we establish the reasoning infrastructure - for $\alpha$-\emph{equated} terms. In contrast, Ott produces a reasoning - infrastructure in Isabelle/HOL for - \emph{non}-$\alpha$-equated, or ``raw'', terms. While our $\alpha$-equated terms - and the raw terms produced by Ott use names for bound variables, - there is a key difference: working with $\alpha$-equated terms means, for example, - that the two type-schemes - - \begin{center} + \[ @{text "\{x}. x \ y = \{x, z}. x \ y"} - \end{center} + \]\smallskip \noindent - are not just $\alpha$-equal, but actually \emph{equal}! As a result, we can - only support specifications that make sense on the level of $\alpha$-equated + are not just alpha-equal, but actually \emph{equal}! As a result, we can + only support specifications that make sense on the level of alpha-equated terms (offending specifications, which for example bind a variable according to a variable bound somewhere else, are not excluded by Ott, but we have to). - Our insistence on reasoning with $\alpha$-equated terms comes from the + Our insistence on reasoning with alpha-equated terms comes from the wealth of experience we gained with the older version of Nominal Isabelle: - for non-trivial properties, reasoning with $\alpha$-equated terms is much + for non-trivial properties, reasoning with alpha-equated terms is much easier than reasoning with raw terms. The fundamental reason for this is that the HOL-logic underlying Nominal Isabelle allows us to replace ``equals-by-equals''. In contrast, replacing - ``$\alpha$-equals-by-$\alpha$-equals'' in a representation based on raw terms + ``alpha-equals-by-alpha-equals'' in a representation based on raw terms requires a lot of extra reasoning work. - Although in informal settings a reasoning infrastructure for $\alpha$-equated + Although in informal settings a reasoning infrastructure for alpha-equated terms is nearly always taken for granted, establishing it automatically in Isabelle/HOL is a rather non-trivial task. For every specification we will need to construct type(s) containing as elements the - $\alpha$-equated terms. To do so, we use the standard HOL-technique of defining + alpha-equated terms. To do so, we use the standard HOL-technique of defining a new type by identifying a non-empty subset of an existing type. The construction we perform in Isabelle/HOL can be illustrated by the following picture: - % - \begin{center} - \begin{tikzpicture}[scale=0.89] + + \[ + \mbox{\begin{tikzpicture}[scale=1.1] %\draw[step=2mm] (-4,-1) grid (4,1); \draw[very thick] (0.7,0.4) circle (4.25mm); @@ -290,28 +285,28 @@ \draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]clas.\end{tabular}}; \draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}}; \draw (1.8, 0.48) node[right=-0.1mm] - {\footnotesize\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}}; + {\small\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}}; \draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}}; - \draw (-3.25, 0.55) node {\footnotesize\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}}; + \draw (-3.25, 0.55) node {\small\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}}; \draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3); \draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism}; - \end{tikzpicture} - \end{center} - % + \end{tikzpicture}} + \]\smallskip + \noindent We take as the starting point a definition of raw terms (defined as a - datatype in Isabelle/HOL); then identify the $\alpha$-equivalence classes in - the type of sets of raw terms according to our $\alpha$-equivalence relation, - and finally define the new type as these $\alpha$-equivalence classes - (non-emptiness is satisfied whenever the raw terms are definable as datatype - in Isabelle/HOL and our relation for $\alpha$-equivalence is - an equivalence relation). + datatype in Isabelle/HOL); then identify the alpha-equivalence classes in + the type of sets of raw terms according to our alpha-equivalence relation, + and finally define the new type as these alpha-equivalence classes (the + non-emptiness requirement is always satisfied whenever the raw terms are + definable as datatype in Isabelle/HOL and our relation for alpha-equivalence + is an equivalence relation). The fact that we obtain an isomorphism between the new type and the non-empty subset shows that the new type is a faithful representation of - $\alpha$-equated terms. That is not the case for example for terms using the + alpha-equated terms. That is not the case for example for terms using the locally nameless representation of binders \cite{McKinnaPollack99}: in this representation there are ``junk'' terms that need to be excluded by reasoning about a well-formedness predicate. @@ -322,18 +317,18 @@ task. To ease it, we re-implemented in Isabelle/HOL \cite{KaliszykUrban11} the quotient package described by Homeier \cite{Homeier05} for the HOL4 system. This package allows us to lift definitions and theorems involving raw terms to - definitions and theorems involving $\alpha$-equated terms. For example if we + definitions and theorems involving alpha-equated terms. For example if we define the free-variable function over raw lambda-terms \begin{center} - @{text "fv(x) = {x}"}\hspace{8mm} - @{text "fv(t\<^isub>1 t\<^isub>2) = fv(t\<^isub>1) \ fv(t\<^isub>2)"}\hspace{8mm} - @{text "fv(\x.t) = fv(t) - {x}"} + @{text "fv(x) \ {x}"}\\ + @{text "fv(t\<^isub>1 t\<^isub>2) \ fv(t\<^isub>1) \ fv(t\<^isub>2)"}\hspace{8mm} + @{text "fv(\x.t) \ fv(t) - {x}"} \end{center} \noindent then with the help of the quotient package we can obtain a function @{text "fv\<^sup>\"} - operating on quotients, or $\alpha$-equivalence classes of lambda-terms. This + operating on quotients, or alpha-equivalence classes of lambda-terms. This lifted function is characterised by the equations \begin{center} @@ -345,16 +340,16 @@ \noindent (Note that this means also the term-constructors for variables, applications and lambda are lifted to the quotient level.) This construction, of course, - only works if $\alpha$-equivalence is indeed an equivalence relation, and the - ``raw'' definitions and theorems are respectful w.r.t.~$\alpha$-equivalence. + only works if alpha-equivalence is indeed an equivalence relation, and the + ``raw'' definitions and theorems are respectful w.r.t.~alpha-equivalence. For example, we will not be able to lift a bound-variable function. Although this function can be defined for raw terms, it does not respect - $\alpha$-equivalence and therefore cannot be lifted. + alpha-equivalence and therefore cannot be lifted. To sum up, every lifting of theorems to the quotient level needs proofs of some respectfulness properties (see \cite{Homeier05}). In the paper we show that we are able to automate these proofs and as a result can automatically establish a reasoning - infrastructure for $\alpha$-equated terms.\smallskip + infrastructure for alpha-equated terms.\smallskip The examples we have in mind where our reasoning infrastructure will be helpful includes the term language of Core-Haskell. This term language @@ -366,17 +361,17 @@ \noindent {\bf Contributions:} We provide three new definitions for when terms - involving general binders are $\alpha$-equivalent. These definitions are + involving general binders are alpha-equivalent. These definitions are inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic - proofs, we establish a reasoning infrastructure for $\alpha$-equated + proofs, we establish a reasoning infrastructure for alpha-equated terms, including properties about support, freshness and equality - conditions for $\alpha$-equated terms. We are also able to derive strong + conditions for alpha-equated terms. We are also able to derive strong induction principles that have the variable convention already built in. The method behind our specification of general binders is taken from the Ott-tool, but we introduce crucial restrictions, and also extensions, so - that our specifications make sense for reasoning about $\alpha$-equated terms. + that our specifications make sense for reasoning about alpha-equated terms. 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 + (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 from ``first principles''. @@ -499,7 +494,7 @@ The most original aspect of the nominal logic work of Pitts is a general definition for the notion of the ``set of free variables of an object @{text "x"}''. This notion, written @{term "supp x"}, is general in the sense that - it applies not only to lambda-terms ($\alpha$-equated or not), but also to lists, + it applies not only to lambda-terms (alpha-equated or not), but also to lists, products, sets and even functions. The definition depends only on the permutation operation and on the notion of equality defined for the type of @{text x}, namely: @@ -520,9 +515,9 @@ @{text x} unchanged, namely if @{text "a \ x"} and @{text "b \ x"} then @{term "(a \ b) \ x = x"}. - \begin{myproperty}\label{swapfreshfresh} + \begin{prop}\label{swapfreshfresh} @{thm[mode=IfThen] swap_fresh_fresh[no_vars]} - \end{myproperty} + \end{prop} While often the support of an object can be relatively easily described, for example for atoms, products, lists, function applications, @@ -553,20 +548,20 @@ such approximations can be simplified with the notion \emph{supports}, defined as follows: - \begin{definition} + \begin{defi} A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b} not in @{text S} we have @{term "(a \ b) \ x = x"}. - \end{definition} + \end{defi} \noindent The main point of @{text supports} is that we can establish the following two properties. - \begin{myproperty}\label{supportsprop} + \begin{prop}\label{supportsprop} Given a set @{text "as"} of atoms. {\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]} {\it (ii)} @{thm supp_supports[no_vars]}. - \end{myproperty} + \end{prop} Another important notion in the nominal logic work is \emph{equivariance}. For a function @{text f}, say of type @{text "\ \ \"}, to be equivariant @@ -605,16 +600,16 @@ proved too unwieldy for dealing with multiple binders. For such binders the following generalisations turned out to be easier to use. - \begin{myproperty}\label{supppermeq} + \begin{prop}\label{supppermeq} @{thm[mode=IfThen] supp_perm_eq[no_vars]} - \end{myproperty} + \end{prop} - \begin{myproperty}\label{avoiding} + \begin{prop}\label{avoiding} For a finite set @{text as} and a finitely supported @{text x} with @{term "as \* x"} and also a finitely supported @{text c}, there exists a permutation @{text p} such that @{term "(p \ as) \* c"} and @{term "supp x \* p"}. - \end{myproperty} + \end{prop} \noindent The idea behind the second property is that given a finite set @{text as} @@ -628,7 +623,7 @@ Most properties given in this section are described in detail in \cite{HuffmanUrban10} and all are formalised in Isabelle/HOL. In the next sections we will make - extensive use of these properties in order to define $\alpha$-equivalence in + extensive use of these properties in order to define alpha-equivalence in the presence of multiple binders. *} @@ -651,8 +646,8 @@ "as"} in the body @{text "x"}. The first question we have to answer is when two pairs @{text "(as, x)"} and - @{text "(bs, y)"} are $\alpha$-equivalent? (For the moment we are interested in - the notion of $\alpha$-equivalence that is \emph{not} preserved by adding + @{text "(bs, y)"} are alpha-equivalent? (For the moment we are interested in + the notion of alpha-equivalence that is \emph{not} preserved by adding vacuous binders.) To answer this question, we identify four conditions: {\it (i)} given a free-atom function @{text "fa"} of type \mbox{@{text "\ \ atom set"}}, then @{text x} and @{text y} need to have the same set of free @@ -675,16 +670,16 @@ % \noindent Note that this relation depends on the permutation @{text - "p"}; $\alpha$-equivalence between two pairs is then the relation where we + "p"}; alpha-equivalence between two pairs is then the relation where we existentially quantify over this @{text "p"}. Also note that the relation is dependent on a free-atom function @{text "fa"} and a relation @{text "R"}. The reason for this extra generality is that we will use - $\approx_{\,\textit{set}}$ for both ``raw'' terms and $\alpha$-equated terms. In + $\approx_{\,\textit{set}}$ for both ``raw'' terms and alpha-equated terms. In the latter case, @{text R} will be replaced by equality @{text "="} and we will prove that @{text "fa"} is equal to @{text "supp"}. The definition in \eqref{alphaset} does not make any distinction between the - order of abstracted atoms. If we want this, then we can define $\alpha$-equivalence + order of abstracted atoms. If we want this, then we can define alpha-equivalence for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \ \"} as follows % @@ -717,7 +712,7 @@ \end{equation} It might be useful to consider first some examples how these definitions - of $\alpha$-equivalence pan out in practice. For this consider the case of + of alpha-equivalence pan out in practice. For this consider the case of abstracting a set of atoms over types (as in type-schemes). We set @{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we define @@ -729,7 +724,7 @@ \noindent 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 + @{text "({y, x}, y \ x)"} are alpha-equivalent according to $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{set+}}$ by taking @{text p} to be the swapping @{term "(x \ y)"}. In case of @{text "x \ y"}, then @{text "([x, y], x \ y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \ y)"} @@ -741,7 +736,7 @@ $\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal (similarly for $\approx_{\,\textit{list}}$). It can also relatively easily be - shown that all three notions of $\alpha$-equivalence coincide, if we only + shown that all three notions of alpha-equivalence coincide, if we only abstract a single atom. In the rest of this section we are going to introduce three abstraction @@ -756,12 +751,12 @@ and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence relations. %% and equivariant. - \begin{lemma}\label{alphaeq} + \begin{lem}\label{alphaeq} The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$ and $\approx_{\,\textit{abs\_set+}}$ are equivalence relations. %, and if %@{term "abs_set (as, x) (bs, y)"} then also %@{term "abs_set (p \ as, p \ x) (p \ bs, p \ y)"} (similarly for the other two relations). - \end{lemma} + \end{lem} \begin{proof} Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have @@ -774,7 +769,7 @@ \noindent This lemma allows us to use our quotient package for introducing new types @{text "\ abs_set"}, @{text "\ abs_set+"} and @{text "\ abs_list"} - representing $\alpha$-equivalence classes of pairs of type + representing alpha-equivalence classes of pairs of type @{text "(atom set) \ \"} (in the first two cases) and of type @{text "(atom list) \ \"} (in the third case). The elements in these types will be, respectively, written as @@ -791,7 +786,7 @@ \emph{abstractions}. The important property we need to derive is the support of abstractions, namely: - \begin{theorem}[Support of Abstractions]\label{suppabs} + \begin{thm}[Support of Abstractions]\label{suppabs} Assuming @{text x} has finite support, then \begin{center} @@ -802,7 +797,7 @@ @{thm (rhs) supp_Abs(3)[where bs="bs", no_vars]} \end{tabular} \end{center} - \end{theorem} + \end{thm} \noindent This theorem states that the bound names do not appear in the support. @@ -828,13 +823,13 @@ \noindent The second fact derives from the definition of permutations acting on pairs - \eqref{permute} and $\alpha$-equivalence being equivariant + \eqref{permute} and alpha-equivalence being equivariant (see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show the following lemma about swapping two atoms in an abstraction. - \begin{lemma} + \begin{lem} @{thm[mode=IfThen] Abs_swap1(1)[where bs="as", no_vars]} - \end{lemma} + \end{lem} \begin{proof} This lemma is straightforward using \eqref{abseqiff} and observing that @@ -886,7 +881,7 @@ properties about them. It would be laborious to write custom ML-code that derives automatically such properties for every term-constructor that binds some atoms. Also the generality of - the definitions for $\alpha$-equivalence will help us in the next sections. + the definitions for alpha-equivalence will help us in the next sections. *} section {* Specifying General Bindings\label{sec:spec} *} @@ -905,7 +900,7 @@ \mbox{\begin{tabular}{@ {}p{2.5cm}l} type \mbox{declaration part} & $\begin{cases} - \mbox{\small\begin{tabular}{l} + \mbox{\begin{tabular}{l} \isacommand{nominal\_datatype} @{text "ty\\<^isub>1 = \"}\\ \isacommand{and} @{text "ty\\<^isub>2 = \"}\\ \raisebox{2mm}{$\ldots$}\\[-2mm] @@ -914,7 +909,7 @@ \end{cases}$\\ binding \mbox{function part} & $\begin{cases} - \mbox{\small\begin{tabular}{l} + \mbox{\begin{tabular}{l} \isacommand{binder} @{text "bn\\<^isub>1"} \isacommand{and} \ldots \isacommand{and} @{text "bn\\<^isub>m"}\\ \isacommand{where}\\ \raisebox{2mm}{$\ldots$}\\[-2mm] @@ -961,7 +956,7 @@ The first mode is for binding lists of atoms (the order of binders matters); the second is for sets of binders (the order does not matter, but the cardinality does) and the last is for sets of binders (with vacuous binders - preserving $\alpha$-equivalence). As indicated, the labels in the ``\isacommand{in}-part'' of a binding + preserving alpha-equivalence). As indicated, the labels in the ``\isacommand{in}-part'' of a binding clause will be called \emph{bodies}; the ``\isacommand{bind}-part'' will be called \emph{binders}. In contrast to Ott, we allow multiple labels in binders and bodies. @@ -983,13 +978,13 @@ Similarly for the other binding modes. Interestingly, in case of \isacommand{bind (set)} and \isacommand{bind (set+)} the binding clauses above will make a difference to the semantics - of the specifications (the corresponding $\alpha$-equivalence will differ). We will + of the specifications (the corresponding alpha-equivalence will differ). We will show this later with an example. There are also some restrictions we need to impose on our binding clauses in comparison to the ones of Ott. The main idea behind these restrictions is that we obtain a sensible notion of - $\alpha$-equivalence where it is ensured that within a given scope an + alpha-equivalence where it is ensured that within a given scope an atom occurrence cannot be both bound and free at the same time. The first restriction is that a body can only occur in \emph{one} binding clause of a term constructor (this ensures that the bound @@ -1006,7 +1001,7 @@ single name is bound, and type-schemes, where a finite set of names is bound: - \begin{center}\small + \begin{center} \begin{tabular}{@ {}c@ {\hspace{7mm}}c@ {}} \begin{tabular}{@ {}l} \isacommand{nominal\_datatype} @{text lam} $=$\\ @@ -1045,7 +1040,7 @@ tuple patterns might be specified as: % \begin{equation}\label{letpat} - \mbox{\small% + \mbox{% \begin{tabular}{l} \isacommand{nominal\_datatype} @{text trm} $=$\\ \hspace{5mm}\phantom{$\mid$}~@{term "Var name"}\\ @@ -1088,7 +1083,7 @@ specification: % \begin{equation}\label{letrecs} - \mbox{\small% + \mbox{% \begin{tabular}{@ {}l@ {}} \isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\ \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"} @@ -1108,13 +1103,13 @@ The difference is that with @{text Let} we only want to bind the atoms @{text "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms inside the assignment. This difference has consequences for the associated - notions of free-atoms and $\alpha$-equivalence. + notions of free-atoms and alpha-equivalence. To make sure that atoms bound by deep binders cannot be free at the same time, we cannot have more than one binding function for a deep binder. Consequently we exclude specifications such as % - \begin{center}\small + \begin{center} \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}\\ @@ -1128,10 +1123,10 @@ Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"} pick out different atoms to become bound, respectively be free, in @{text "p"}. (Since the Ott-tool does not derive a reasoning infrastructure for - $\alpha$-equated terms with deep binders, it can permit such specifications.) + alpha-equated terms with deep binders, it can permit such specifications.) We also need to restrict the form of the binding functions in order - to ensure the @{text "bn"}-functions can be defined for $\alpha$-equated + to ensure the @{text "bn"}-functions can be defined for alpha-equated terms. The main restriction is that we cannot return an atom in a binding function that is also bound in the corresponding term-constructor. That means in \eqref{letpat} that the term-constructors @{text PVar} and @{text PTup} may @@ -1139,7 +1134,7 @@ In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons} may have a binding clause involving the argument @{text trm} (the only one that is \emph{not} used in the definition of the binding function). This restriction - is sufficient for lifting the binding function to $\alpha$-equated terms. + is sufficient for lifting the binding function to alpha-equated terms. In the version of Nominal Isabelle described here, we also adopted the restriction from the @@ -1149,7 +1144,7 @@ (case @{text PTup}). This restriction will simplify some automatic definitions and proofs later on. - In order to simplify our definitions of free atoms and $\alpha$-equivalence, + In order to simplify our definitions of free atoms and alpha-equivalence, we shall assume specifications of term-calculi are implicitly \emph{completed}. By this we mean that for every argument of a term-constructor that is \emph{not} @@ -1157,7 +1152,7 @@ clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case of the lambda-terms, the completion produces - \begin{center}\small + \begin{center} \begin{tabular}{@ {}l@ {\hspace{-1mm}}} \isacommand{nominal\_datatype} @{text lam} =\\ \hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"} @@ -1186,15 +1181,15 @@ result in inadequate representations in cases like @{text "Let x\<^isub>1 = t\<^isub>1\x\<^isub>n = t\<^isub>n in s"}. Therefore we will first extract ``raw'' datatype definitions from the specification and then define - explicitly an $\alpha$-equivalence relation over them. We subsequently - construct the quotient of the datatypes according to our $\alpha$-equivalence. + explicitly an alpha-equivalence relation over them. We subsequently + construct the quotient of the datatypes according to our alpha-equivalence. The ``raw'' datatype definition can be obtained by stripping off the binding clauses and the labels from the types. We also have to invent new names for the types @{text "ty\<^sup>\"} and term-constructors @{text "C\<^sup>\"} given by the user. In our implementation we just use the affix ``@{text "_raw"}''. But for the purpose of this paper, we use the superscript @{text "_\<^sup>\"} to indicate - that a notion is given for $\alpha$-equivalence classes and leave it out + that a notion is given for alpha-equivalence classes and leave it out for the corresponding notion given on the ``raw'' level. So for example we have @{text "ty\<^sup>\ \ ty"} and @{text "C\<^sup>\ \ C"} where @{term ty} is the type used in the quotient construction for @@ -1362,7 +1357,7 @@ "fa\<^bsub>trm\<^esub>"}, @{text "fa\<^bsub>assn\<^esub>"} and @{text "fa\<^bsub>bn\<^esub>"} as follows: % - \begin{center}\small + \begin{center} \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} @{text "fa\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t - set (bn as)) \ fa\<^bsub>bn\<^esub> as"}\\ @{text "fa\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fa\<^bsub>assn\<^esub> as \ fa\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm] @@ -1401,11 +1396,11 @@ Only in the context of a @{text Let} or @{text "Let_rec"}, where the binding clauses are given, will some atoms actually become bound. This is a phenomenon that has also been pointed out in \cite{ott-jfp}. For us this observation is crucial, because we would - not be able to lift the @{text "bn"}-functions to $\alpha$-equated terms if they act on + not be able to lift the @{text "bn"}-functions to alpha-equated terms if they act on atoms that are bound. In that case, these functions would \emph{not} respect - $\alpha$-equivalence. + alpha-equivalence. - Next we define the $\alpha$-equivalence relations for the raw types @{text + Next we define the alpha-equivalence relations for the raw types @{text "ty"}$_{1..n}$ from the specification. We write them as \begin{center} @@ -1414,7 +1409,7 @@ \noindent Like with the free-atom functions, we also need to - define auxiliary $\alpha$-equivalence relations + define auxiliary alpha-equivalence relations \begin{center} @{text "\bn\<^isub>"}$_{1..m}$ @@ -1434,10 +1429,10 @@ \end{center} - The $\alpha$-equivalence relations are defined as inductive predicates + The alpha-equivalence relations are defined as inductive predicates having a single clause for each term-constructor. Assuming a term-constructor @{text C} is of type @{text ty} and has the binding clauses - @{term "bc"}$_{1..k}$, then the $\alpha$-equivalence clause has the form + @{term "bc"}$_{1..k}$, then the alpha-equivalence clause has the form \begin{center} \mbox{\infer{@{text "C z\<^isub>1 \ z\<^isub>n \ty C z\\<^isub>1 \ z\\<^isub>n"}} @@ -1454,11 +1449,11 @@ \end{center} \noindent - In this binding clause no atom is bound and we only have to $\alpha$-relate the bodies. For this + In this binding clause no atom is bound and we only have to alpha-relate the bodies. For this we build first the tuples @{text "D \ (d\<^isub>1,\, d\<^isub>q)"} and @{text "D' \ (d\\<^isub>1,\, d\\<^isub>q)"} whereby the labels @{text "d"}$_{1..q}$ refer to arguments @{text "z"}$_{1..n}$ and respectively @{text "d\"}$_{1..q}$ to @{text "z\"}$_{1..n}$. In order to relate - two such tuples we define the compound $\alpha$-equivalence relation @{text "R"} as follows + two such tuples we define the compound alpha-equivalence relation @{text "R"} as follows \begin{equation}\label{rempty} \mbox{@{text "R \ (R\<^isub>1,\, R\<^isub>q)"}} @@ -1489,10 +1484,10 @@ In this case we define a premise @{text P} using the relation $\approx_{\,\textit{set}}$ given in Section~\ref{sec:binders} (similarly $\approx_{\,\textit{set+}}$ and $\approx_{\,\textit{list}}$ for the other - binding modes). This premise defines $\alpha$-equivalence of two abstractions + binding modes). This premise defines alpha-equivalence of two abstractions involving multiple binders. As above, we first build the tuples @{text "D"} and @{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding - compound $\alpha$-relation @{text "R"} (shown in \eqref{rempty}). + compound alpha-relation @{text "R"} (shown in \eqref{rempty}). For $\approx_{\,\textit{set}}$ we also need a compound free-atom function for the bodies defined as @@ -1518,13 +1513,13 @@ \end{center} \noindent - This premise accounts for $\alpha$-equivalence of the bodies of the binding + This premise accounts for alpha-equivalence of the bodies of the binding clause. However, in case the binders have non-recursive deep binders, this premise is not enough: - we also have to ``propagate'' $\alpha$-equivalence inside the structure of + we also have to ``propagate'' alpha-equivalence inside the structure of these binders. An example is @{text "Let"} where we have to make sure the - right-hand sides of assignments are $\alpha$-equivalent. For this we use + right-hand sides of assignments are alpha-equivalent. For this we use relations @{text "\bn"}$_{1..m}$ (which we will formally define shortly). Let us assume the non-recursive deep binders in @{text "bc\<^isub>i"} are @@ -1542,7 +1537,7 @@ \end{center} \noindent - The auxiliary $\alpha$-equivalence relations @{text "\bn"}$_{1..m}$ + The auxiliary alpha-equivalence relations @{text "\bn"}$_{1..m}$ in @{text "R'"} are defined as follows: assuming a @{text bn}-clause is of the form \begin{center} @@ -1551,7 +1546,7 @@ \noindent where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$, - then the corresponding $\alpha$-equivalence clause for @{text "\bn"} has the form + then the corresponding alpha-equivalence clause for @{text "\bn"} has the form \begin{center} \mbox{\infer{@{text "C z\<^isub>1 \ z\<^isub>s \bn C z\\<^isub>1 \ z\\<^isub>s"}} @@ -1575,7 +1570,7 @@ \end{center} \noindent - This completes the definition of $\alpha$-equivalence. As a sanity check, we can show + This completes the definition of alpha-equivalence. As a sanity check, we can show that the premises of empty binding clauses are a special case of the clauses for non-empty ones (we just have to unfold the definition of $\approx_{\,\textit{set}}$ and take @{text "0"} for the existentially quantified permutation). @@ -1584,7 +1579,7 @@ we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and $\approx_{\textit{bn}}$ with the following clauses: - \begin{center}\small + \begin{center} \begin{tabular}{@ {}c @ {}} \infer{@{text "Let as t \\<^bsub>trm\<^esub> Let as' t'"}} {@{term "\p. (bn as, t) \lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \\<^bsub>bn\<^esub> as'"}}\smallskip\\ @@ -1593,7 +1588,7 @@ \end{tabular} \end{center} - \begin{center}\small + \begin{center} \begin{tabular}{@ {}c @ {}} \infer{@{text "ANil \\<^bsub>assn\<^esub> ANil"}}{}\hspace{9mm} \infer{@{text "ACons a t as \\<^bsub>assn\<^esub> ACons a' t' as"}} @@ -1601,7 +1596,7 @@ \end{tabular} \end{center} - \begin{center}\small + \begin{center} \begin{tabular}{@ {}c @ {}} \infer{@{text "ANil \\<^bsub>bn\<^esub> ANil"}}{}\hspace{9mm} \infer{@{text "ACons a t as \\<^bsub>bn\<^esub> ACons a' t' as"}} @@ -1611,7 +1606,7 @@ \noindent Note the difference between $\approx_{\textit{assn}}$ and - $\approx_{\textit{bn}}$: the latter only ``tracks'' $\alpha$-equivalence of + $\approx_{\textit{bn}}$: the latter only ``tracks'' alpha-equivalence of the components in an assignment that are \emph{not} bound. This is needed in the clause for @{text "Let"} (which has a non-recursive binder). @@ -1624,20 +1619,20 @@ text {* Having made all necessary definitions for raw terms, we can start - with establishing the reasoning infrastructure for the $\alpha$-equated types + with establishing the reasoning infrastructure for the alpha-equated types @{text "ty\"}$_{1..n}$, that is the types the user originally specified. We sketch in this section the proofs we need for establishing this infrastructure. One main point of our work is that we have completely automated these proofs in Isabelle/HOL. First we establish that the - $\alpha$-equivalence relations defined in the previous section are + alpha-equivalence relations defined in the previous section are equivalence relations. - \begin{lemma}\label{equiv} + \begin{lem}\label{equiv} Given the raw types @{text "ty"}$_{1..n}$ and binding functions @{text "bn"}$_{1..m}$, the relations @{text "\ty"}$_{1..n}$ and @{text "\bn"}$_{1..m}$ are equivalence relations. and equivariant. - \end{lemma} + \end{lem} \begin{proof} The proof is by mutual induction over the definitions. The non-trivial @@ -1648,7 +1643,7 @@ \noindent We can feed this lemma into our quotient package and obtain new types @{text - "ty"}$^\alpha_{1..n}$ representing $\alpha$-equated terms of types @{text "ty"}$_{1..n}$. + "ty"}$^\alpha_{1..n}$ representing alpha-equated terms of types @{text "ty"}$_{1..n}$. We also obtain definitions for the term-constructors @{text "C"}$^\alpha_{1..k}$ from the raw term-constructors @{text "C"}$_{1..k}$, and similar definitions for the free-atom functions @{text @@ -1669,7 +1664,7 @@ \noindent whenever @{text "C"}$^\alpha$~@{text "\"}~@{text "D"}$^\alpha$. - In order to derive this fact, we use the definition of $\alpha$-equivalence + In order to derive this fact, we use the definition of alpha-equivalence and establish that \begin{equation}\label{distinctraw} @@ -1680,7 +1675,7 @@ holds for the corresponding raw term-constructors. In order to deduce \eqref{distinctalpha} from \eqref{distinctraw}, our quotient package needs to know that the raw term-constructors @{text "C"} and @{text "D"} - are \emph{respectful} w.r.t.~the $\alpha$-equivalence relations (see \cite{Homeier05}). + are \emph{respectful} w.r.t.~the alpha-equivalence relations (see \cite{Homeier05}). Assuming, for example, @{text "C"} is of type @{text "ty"} with argument types @{text "ty"}$_{1..r}$, respectfulness amounts to showing that @@ -1693,7 +1688,7 @@ "x\<^isub>i \ty\<^isub>i x\\<^isub>i"}} whenever @{text "x\<^isub>i"} and @{text "x\\<^isub>i"} are recursive arguments of @{text C} and @{text "x\<^isub>i = x\\<^isub>i"} whenever they are non-recursive arguments. We can prove this - implication by applying the corresponding rule in our $\alpha$-equivalence + implication by applying the corresponding rule in our alpha-equivalence definition and by establishing the following auxiliary implications %facts % \begin{equation}\label{fnresp} @@ -1715,7 +1710,7 @@ any bound atoms. In Ott, in contrast, the user may define @{text "bn"}$_{1..m}$ so that they return bound atoms and in this case the third implication is \emph{not} true. A - result is that the lifting of the corresponding binding functions in Ott to $\alpha$-equated + result is that the lifting of the corresponding binding functions in Ott to alpha-equated terms is impossible. Having established respectfulness for the raw term-constructors, the @@ -1728,8 +1723,8 @@ \end{center} \noindent - are $\alpha$-equivalent. This gives us conditions when the corresponding - $\alpha$-equated terms are \emph{equal}, namely + are alpha-equivalent. This gives us conditions when the corresponding + alpha-equated terms are \emph{equal}, namely \begin{center} @{text "C\<^sup>\ x\<^isub>1 \ x\<^isub>r = C\<^sup>\ x\\<^isub>1 \ x\\<^isub>r"}. @@ -1737,13 +1732,13 @@ \noindent We call these conditions as \emph{quasi-injectivity}. They correspond to - the premises in our $\alpha$-equivalence relations. + the premises in our alpha-equivalence relations. Next we can lift the permutation operations defined in \eqref{ceqvt}. In order to make this lifting to go through, we have to show that the permutation operations are respectful. This amounts to showing that the - $\alpha$-equivalence relations are equivariant \cite{HuffmanUrban10}. + alpha-equivalence relations are equivariant \cite{HuffmanUrban10}. , which we already established in Lemma~\ref{equiv}. As a result we can add the equations @@ -1782,7 +1777,7 @@ in which the @{text "x"}$_{i..j}$ @{text "\"} @{text "x"}$_{1..r}$ are the recursive arguments of @{text "C\"}. - By working now completely on the $\alpha$-equated level, we + By working now completely on the alpha-equated level, we can first show that the free-atom functions and binding functions are equivariant, namely @@ -1813,12 +1808,12 @@ Lastly, we can show that the support of elements in @{text "ty\"}$_{1..n}$ is the same as @{text "fa_ty\"}$_{1..n}$. This fact is important in a nominal setting, but also provides evidence - that our notions of free-atoms and $\alpha$-equivalence are correct. + that our notions of free-atoms and alpha-equivalence are correct. - \begin{theorem} + \begin{thm} For @{text "x"}$_{1..n}$ with type @{text "ty\"}$_{1..n}$, we have @{text "supp x\<^isub>i = fa_ty\\<^isub>i x\<^isub>i"}. - \end{theorem} + \end{thm} \begin{proof} The proof is by induction. In each case @@ -1911,7 +1906,7 @@ section {* Strong Induction Principles *} text {* - In the previous section we derived induction principles for $\alpha$-equated terms. + In the previous section we derived induction principles for alpha-equated terms. We call such induction principles \emph{weak}, because for a term-constructor \mbox{@{text "C\<^sup>\ x\<^isub>1\x\<^isub>r"}} the induction hypothesis requires us to establish the implications \eqref{weakprem}. @@ -2066,13 +2061,13 @@ \noindent Using again the quotient package we can lift the @{text "_ \\<^bsub>bn\<^esub> _"} function to - $\alpha$-equated terms. We can then prove the following two facts + alpha-equated terms. We can then prove the following two facts - \begin{lemma}\label{permutebn} + \begin{lem}\label{permutebn} Given a binding function @{text "bn\<^sup>\"} then for all @{text p} {\it (i)} @{text "p \ (bn\<^sup>\ x) = bn\<^sup>\ (p \\\<^bsub>bn\<^esub> x)"} and {\it (ii)} @{text "fa_bn\<^isup>\ x = fa_bn\<^isup>\ (p \\\<^bsub>bn\<^esub> x)"}. - \end{lemma} + \end{lem} \begin{proof} By induction on @{text x}. The equations follow by simple unfolding @@ -2241,23 +2236,23 @@ Ott can also generate theorem prover code using a raw representation of terms, and in Coq also a locally nameless representation. The developers of this tool have also put forward (on paper) a definition for - $\alpha$-equivalence of terms that can be specified in Ott. This definition is + 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 no concrete mathematical result concerning this - notion of $\alpha$-equivalence. Also the definition for the + 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$-equi\-valence 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 - sense for our $\alpha$-equated terms. Third, it allows empty types that have no + sense for our alpha-equated terms. Third, it allows empty types that have no meaning in a HOL-based theorem prover. We also had to generalise slightly Ott's binding clauses. In Ott you specify binding clauses with a single body; we allow more than one. We have to do this, because this makes a difference - for our notion of $\alpha$-equivalence in case of \isacommand{bind (set)} and + for our notion of alpha-equivalence in case of \isacommand{bind (set)} and \isacommand{bind (set+)}. Consider the examples @@ -2305,7 +2300,7 @@ inter-translated as long as ours use the binding mode \isacommand{bind} only. However, we have not proved this. Pottier gives a definition for - $\alpha$-equivalence, which also uses a permutation operation (like ours). + alpha-equivalence, which also uses a permutation operation (like ours). Still, this definition is rather different from ours and he only proves that it defines an equivalence relation. A complete reasoning infrastructure is well beyond the purposes of his language. @@ -2313,24 +2308,27 @@ In a slightly different domain (programming with dependent types), the paper \cite{Altenkirch10} presents a calculus with a notion of - $\alpha$-equivalence related to our binding mode \isacommand{bind (set+)}. + alpha-equivalence related to our binding mode \isacommand{bind (set+)}. The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it has a more operational flavour and calculates a partial (renaming) map. In this way, the definition can deal with vacuous binders. However, to our best knowledge, no concrete mathematical result concerning this - definition of $\alpha$-equivalence has been proved.\\[-7mm] + definition of alpha-equivalence has been proved. *} section {* Conclusion *} text {* + Telsescopes by de Bruijn (AUTOMATH project does not provide an automatic infrastructure). + + We have presented an extension of Nominal Isabelle for dealing with general binders, that is term-constructors having multiple bound variables. For this extension we introduced new definitions of - $\alpha$-equivalence and automated all necessary proofs in Isabelle/HOL. + alpha-equivalence and automated all necessary proofs in Isabelle/HOL. To specify general binders we used the specifications from Ott, but extended them in some places and restricted - them in others so that they make sense in the context of $\alpha$-equated terms. + them in others so that they make sense in the context of alpha-equated terms. We also introduced two binding modes (set and set+) that do not exist in Ott. We have tried out the extension with calculi such as Core-Haskell, type-schemes @@ -2343,7 +2341,7 @@ {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 + alpha-equated terms involving general binders. In earlier versions of Nominal 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 @@ -2371,20 +2369,18 @@ allow us to support more interesting binding functions. We have also not yet played with other binding modes. For example we can - imagine that there is need for a binding mode - where instead of lists, we abstract lists of distinct elements. - Once we feel confident about such binding modes, our implementation - can be easily extended to accommodate them. + imagine that there is need for a binding mode where instead of lists, we + abstract lists of distinct elements. Once we feel confident about such + binding modes, our implementation can be easily extended to accommodate + them.\medskip - \smallskip \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 of the Ott-tool.\\[-7mm] - Stephanie Weirich suggested to separate the subgrammars - of kinds and types in our Core-Haskell example. \\[-6mm] + {\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 of the Ott-tool. Stephanie Weirich + suggested to separate the subgrammars of kinds and types in our Core-Haskell + example. *} diff -r eab84ac2603b -r 5df574281b69 LMCS-Paper/document/lmcs.cls --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/LMCS-Paper/document/lmcs.cls Tue Aug 16 17:48:09 2011 +0200 @@ -0,0 +1,512 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% Modification log +%% +%% 2004/03/25 v0.1 based on amsart.cls, inspired by jair.sty +%% 2004/09/01 v0.2 based on amsart.cls +%% 2004/10/12 v0.3 based on amsart.cls +%% 2004/12/16 v0.4 based on amsart.cls +%% 2005/01/24 v0.5 based on amsart.cls +%% 2005/03/10 v0.6 based on amsart.cls +%% 2006/07/24 v0.7 based on amsart.cls +%% 2007/11/13 v0.8 based on amsart.cls +%% +%% Juergen Koslowski, Stefan Milius +%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\NeedsTeXFormat{LaTeX2e} +\ProvidesClass{lmcs} + [2009/05/25 v0.8 LMCS Layout Editor Class] +\DeclareOption*{\PassOptionsToClass{\CurrentOption}{amsart}} +\ProcessOptions\relax + +\LoadClass[11pt,reqno]{amsart} +\usepackage{helvet,cclicenses} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Use of this class, cf. also lmcs-smp.tex +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% This class builds upon the amsart class of AMS-LaTeX and requires use +% of LaTeX 2e. +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Start of the paper +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% \documentclass{lmcs} +% +% without any options followed optionally by +% +% \usepackage{package1,package2,...} +% +% loading additional macro packages you may wish to use, (eg, xypic, etc.) +% (This also is the place to define further theorem-environments, in case +% those provided by default do not suffice, cf. below.) +% +% \begin{document} +% \title[short_title]{real title} +% +% and a list of author information of the form +% +% \author[short_author1]{Author 1} +% \address{address 1} +% \email{author1@email1} +% \thanks{thanks 1} +% +% \author[short_author2]{Author 2} +% \address{address 2} +% \email{author2@email2} +% \thanks{thanks 2} +% +% \author[short_author3]{Author 3} +% \address{address 3} +% \email{author3@email3} +% \thanks{thanks 3} +% +% The \email and \thanks fields are optional. The \thanks fields appear +% in footnotes on the title page, the addresses and email information +% is relegated to the end of the article. The optional arguments to +% the \title and \author macros determine a running head on the odd +% and even pages, respectively. +% +% Lists of keywords and phrases as well as an ACM Subject +% classification are mandatory; these appear in footnotes on the +% title page, preceeding any \thanks fields. +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Body of the paper +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% We encourage the use of LaTeX's crossreferencing capabilities with the +% \label and \ref commands, for sections, subsections, theorems etc., and +% displayed equations and figures. +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Theorems, Definitions etc. +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% The following theorem-like environments are available. The +% numbering is consecutive within sections. +% +% thm Theorem +% cor Corollary +% lem Lemma +% prop Proposition +% asm Asumption +% +% defi Definition +% rem Remark +% rems Remarks (intended for use with itemized remarks) +% exa Example +% exas Examples (intended for use with itemized examples) +% conj Conjecture +% prob Problem +% oprob Open Problem +% algo Algorithm +% obs Observation +% +% If you require additional environments, you can add them before +% \begin{document} by means of +% +% \theoremstyle{plain}\newtheorem{env}[thm]{Environment} +% +% or +% +% \theoremstyle{definition}\newtheorem{env}[thm]{Environment} +% +% In the first case the font within the new environment will be italicised. +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Proofs +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% Proofs start with the command \proof and should be ended by \qed, +% which provides an end-of-proof box at the right margin: +% +% \proof ... \qed +% +% In itemized or enumerated proofs the \qed command has to occur BEFORE +% \end{itemize} or \end{enumerate} to ensure proper placement of the box: +% +% \proof +% \begin{itemize} +% \item[(1)] ... +% \item[(2)] ... +% ... +% \item[(n)] ... \qed +% \end{itemize} +% +% Similarly, the box may be used within theorem environments, when no +% explicit proof is given: +% +% \begin{thm} ... \qed \end{thm} +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Itemized or enumerated environments and proofs +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% By default, the first item of an itemized (or enumerated) environment +% or proof appears inlined on the same line as the environment title. +% This can be prevented by placing \hfill before the itemization, e.g.: +% +% \begin{thm}\label{T:abc}\hfill +% \begin{itemize} ... +% +% \proof\hfill +% \begin{itemize} ... + + +% +% End of the paper +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% Acknowledgements should be placed in a non-numbered section: +% +% \section*{Acknowledgement} +% +% The bibliography uses alpha.bst where references are built from the +% authors' initials and the year of publication. The use of bibtex +% for creating the bibliography is strongly encouraged. Then the +% end of the paper takes the form +% +% \begin{thebibliography}{key} +% \end{thebibliography} +% \end{document} +% +% where ``key'' is the longest alphanumerical key expected to occur. +% +% Optionally, appendices can be inserted after the bibliography by +% means of +% +% \end{thebibliography} +% \appendix +% \section{} % Appendix A +% \section{} % Appendix B +% % etc. +% \end{document} + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%% actual macros +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\count255=\the\catcode`\@ \catcode`\@=11 \edef\catc@de{\the\count255} + +\newif\ifsuPer \suPertrue +\def\rsuper#1{\ifsuPer${\,}^{\MakeLowercase #1}$\fi}% +\def\lsuper#1{\ \hskip-2 pt\ifsuPer\llap{${}^{\MakeLowercase #1}\ $\fi}}% + +\def\titlecomment#1{\def\@titlecomment{#1}} +\let\@titlecomment=\@empty +\renewcommand{\sfdefault}{phv} +\renewcommand*\subjclass[2][1991]{% + \def\@subjclass{#2}% + \@ifundefined{subjclassname@#1}{% + \ClassWarning{\@classname}{Unknown edition (#1) of ACM + Subject Classification; using '1991'.}% + }{% + \@xp\let\@xp\subjclassname\csname subjclassname@1998\endcsname + }% +} +\@namedef{subjclassname@1998}{1998 ACM Subject Classification} +\newcommand{\revisionname}{Revision Note} +\newbox\revisionbox +\newenvironment{revision}{% + \ifx\maketitle\relax + \ClassWarning{\@classname}{Revision should precede + \protect\maketitle\space in LMCS documentclasses; reported}% + \fi + \global\setbox\revisionbox=\vtop \bgroup + \normalfont\Small + \list{}{\labelwidth\z@ + \leftmargin3pc \rightmargin\leftmargin + \listparindent\normalparindent \itemindent\z@ + \parsep\z@ \@plus\p@ + \let\fullwidthdisplay\relax + }% + \item[\hskip\labelsep\scshape\revisionname.]% +}{% + \endlist\egroup + \ifx\@setrevision\relax \@setrevisiona \fi +} +\def\@setrevision{\@setrevisiona \global\let\@setrevision\relax} +\def\@setrevisiona{% + \ifvoid\revisionbox + \else + \skip@20\p@ \advance\skip@-\lastskip + \advance\skip@-\baselineskip \vskip\skip@ + \box\revisionbox + \prevdepth\z@ % because \revisionbox is a vtop + \bigskip\hrule\medskip + \fi +} +\def\@setsubjclass{% + {\itshape\subjclassname:}\enspace\@subjclass\@addpunct.} +\def\@setkeywords{% + {\itshape \keywordsname:}\enspace \@keywords\@addpunct.} +\def\@settitlecomment{\@titlecomment\@addpunct.} +\def\@maketitle{% + \normalfont\normalsize + \let\@makefnmark\relax \let\@thefnmark\relax + \ifx\@empty\@date\else \@footnotetext{\@setdate}\fi + \ifx\@empty\@subjclass\else \@footnotetext{\@setsubjclass}\fi + \ifx\@empty\@keywords\else \@footnotetext{\@setkeywords}\fi + \ifx\@empty\@titlecomment\else \@footnotetext{\@settitlecomment}\fi + \ifx\@empty\thankses\else \@footnotetext{% + \def\par{\let\par\@par}\@setthanks\par}\fi + \@mkboth{\@nx\shortauthors}{\@nx\shorttitle}% + \global\topskip12\p@\relax % 5.5pc " " " " " + \topskip42 pt\@settitle + \ifx\@empty\authors \else \@setauthors \fi + \@setaddresses + \ifx\@empty\@dedicatory + \else + \baselineskip18\p@ + \vtop{\centering{\footnotesize\itshape\@dedicatory\@@par}% + \global\dimen@i\prevdepth}\prevdepth\dimen@i + \fi + \endfront@text + \bigskip\hrule\medskip + \@setrevision + \@setabstract + \vskip-\bigskipamount + \normalsize + \if@titlepage + \newpage + \else + \dimen@34\p@ \advance\dimen@-\baselineskip + \vskip\dimen@\relax + \fi +} +\def\@setaddresses{\par + \nobreak \begingroup +\footnotesize + \def\author##1{\nobreak\addvspace\bigskipamount}% + \def\\{\unskip, \ignorespaces}% + \interlinepenalty\@M + \def\address##1##2{\begingroup + \par\addvspace\bigskipamount\noindent\narrower + \@ifnotempty{##1}{(\ignorespaces##1\unskip) }% + {\ignorespaces##2}\par\endgroup}% + \def\curraddr##1##2{\begingroup + \@ifnotempty{##2}{\nobreak\indent{\itshape Current address}% + \@ifnotempty{##1}{, \ignorespaces##1\unskip}\/:\space + ##2\par}\endgroup}% + \def\email##1##2{\begingroup + \@ifnotempty{##2}{\nobreak\indent{\itshape e-mail address}% + \@ifnotempty{##1}{, \ignorespaces##1\unskip}\/:\space + {##2}\par}\endgroup}% + \def\urladdr##1##2{\begingroup + \@ifnotempty{##2}{\nobreak\indent{\itshape URL}% + \@ifnotempty{##1}{, \ignorespaces##1\unskip}\/:\space + \ttfamily##2\par}\endgroup}% + \addresses + \endgroup +} +\copyrightinfo{}{} + +\newinsert\copyins +\skip\copyins=3pc +\count\copyins=1000 % magnification factor, 1000 = 100% +\dimen\copyins=.5\textheight % maximum allowed per page + +\renewcommand{\topfraction}{0.95} % let figure take up nearly whole page +\renewcommand{\textfraction}{0.05} % let figure take up nearly whole page + +%% Specify the dimensions of each page + +\setlength{\oddsidemargin}{.25 in} % Note \oddsidemargin = \evensidemargin +\setlength{\evensidemargin}{.25 in} +\setlength{\marginparwidth}{0.07 true in} +\setlength{\topmargin}{-0.7 in} +\addtolength{\headheight}{1.84 pt} +\addtolength{\headsep}{0.25in} +\addtolength{\voffset}{0.7 in} +\setlength{\textheight}{8.5 true in} % Height of text (including footnotes & figures) +\setlength{\textwidth}{6.0 true in} % Width of text line. +\setlength{\parindent}{20 pt} % Width of text line. +\widowpenalty=10000 +\clubpenalty=10000 +\@twosidetrue \@mparswitchtrue \def\ds@draft{\overfullrule 5pt} +\raggedbottom + +%% Pagestyle + +%% Defines the pagestyle for the title page. +%% Usage: \lmcsheading{vol}{issue}{year}{pages}{subm}{publ}{rev}{spec_iss}{title} + +\def\lmcsheading#1#2#3#4#5#6#7{\def\ps@firstpage{\let\@mkboth\@gobbletwo% +\def\@oddhead{% +\hbox{% + \vbox to 30 pt{\scriptsize\vfill + \hbox{\textsf{Logical Methods in Computer Science}\hfil} + \hbox{\textsf{Vol.~? (?:?) 2???, ? pages}} + \hbox{\textsf{www.lmcs-online.org}} + \rlap{\vrule width\hsize depth .4 pt}}}\hfill +\raise 4pt +\hbox{% + \vbox to 30 pt{\scriptsize\vfill + \hbox{\textsf{}} + \hbox{\textsf{}}}}\hfill +\raise 4pt +\hbox{% + \vbox to 30 pt{\scriptsize\vfill + \hbox to 94 pt{\textsf{Submitted\hfill date}} + \hbox to 94 pt{\textsf{Published\hfill date}} + }}} +\def\@evenhead{}\def\@evenfoot{}}% +\thispagestyle{firstpage}} + +\def\endfront@text{% + \insert\copyins{\hsize\textwidth + \fontsize{6}{7\p@}\normalfont\upshape + \noindent +\hbox{ + \vbox{\fontsize{6}{8 pt}\baselineskip=6 pt\vss + \hbox{\hbox to 20 pt{\hfill} + \textsf{LOGICAL METHODS}\hfil} + \hbox{\hbox to 20 pt{\phantom{x}} + \textsf{IN COMPUTER SCIENCE}}}} +\hfill\textsf{DOI:10.2168/LMCS-???} +%\hfill\textsf{\copyright\shortauthors} +\hfill +\hbox{ + \vbox{\fontsize{6}{8 pt}\baselineskip=6 pt\vss + \hbox{\textsf{\,\,\copyright\quad \shortauthors}\hfil} + \hbox{\textsf{Creative Commons}\hfil}}} +\par\kern\z@}% +} +%\def\endfront@text{} + +\def\enddoc@text{} + +%% Defines the pagestyle for the rest of the pages +%% Usage: \ShortHeadings{Minimizing Conflicts}{Minton et al} +%% \ShortHeadings{short title}{short authors} + +%\def\firstpageno#1{\setcounter{page}{#1}} +%\def\ShortHeadings#1#2{\def\ps@lmcsps{\let\@mkboth\@gobbletwo% +%\def\@oddhead{\hfill {\small\sc #1} \hfill}% +%\def\@oddfoot{\hfill \small\rm \thepage \hfill}% +%\def\@evenhead{\hfill {\small\sc #2} \hfill}% +%\def\@evenfoot{\hfill \small\rm \thepage \hfill}}% +%\pagestyle{lmcsps}} + +%% MISCELLANY + +\def\@startsection#1#2#3#4#5#6{\bigskip% + \if@noskipsec \leavevmode \fi + \par \@tempskipa #4\relax + \@afterindentfalse + \ifdim \@tempskipa <\z@ \@tempskipa -\@tempskipa \@afterindentfalse\fi + \if@nobreak \everypar{}\else + \addpenalty\@secpenalty\addvspace\@tempskipa\fi + \@ifstar{\@dblarg{\@sect{#1}{\@m}{#3}{#4}{#5}{#6}}}% + {\@dblarg{\@sect{#1}{#2}{#3}{#4}{#5}{#6}}}% +} + +\def\figurecaption#1#2{\noindent\hangindent 40pt + \hbox to 36pt {\small\sl #1 \hfil} + \ignorespaces {\small #2}} +% Figurecenter prints the caption title centered. +\def\figurecenter#1#2{\centerline{{\sl #1} #2}} +\def\figurecenter#1#2{\centerline{{\small\sl #1} {\small #2}}} + +% +% Allow ``hanging indents'' in long captions +% +\long\def\@makecaption#1#2{ + \vskip 10pt + \setbox\@tempboxa\hbox{#1: #2} + \ifdim \wd\@tempboxa >\hsize % IF longer than one line: + \begin{list}{#1:}{ + \settowidth{\labelwidth}{#1:} + \setlength{\leftmargin}{\labelwidth} + \addtolength{\leftmargin}{\labelsep} + }\item #2 \end{list}\par % Output in quote mode + \else % ELSE center. + \hbox to\hsize{\hfil\box\@tempboxa\hfil} + \fi} + + +% Define strut macros for skipping spaces above and below text in a +% tabular environment. +\def\abovestrut#1{\rule[0in]{0in}{#1}\ignorespaces} +\def\belowstrut#1{\rule[-#1]{0in}{#1}\ignorespaces} + +%%% Theorem environments + +% the following environments switch to a slanted font: +\theoremstyle{plain} + +\newtheorem{thm}{Theorem}[section] +\newtheorem{cor}[thm]{Corollary} +\newtheorem{lem}[thm]{Lemma} +\newtheorem{prop}[thm]{Proposition} +\newtheorem{asm}[thm]{Assumption} + +% the following environments keep the roman font: +\theoremstyle{definition} + +\newtheorem{rem}[thm]{Remark} +\newtheorem{rems}[thm]{Remarks} +\newtheorem{exa}[thm]{Example} +\newtheorem{exas}[thm]{Examples} +\newtheorem{defi}[thm]{Definition} +\newtheorem{conv}[thm]{Convention} +\newtheorem{conj}[thm]{Conjecture} +\newtheorem{prob}[thm]{Problem} +\newtheorem{oprob}[thm]{Open Problem} +\newtheorem{algo}[thm]{Algorithm} +\newtheorem{obs}[thm]{Observation} +\newtheorem{qu}[thm]{Question} +\newtheorem{fact}[thm]{Fact} +\newtheorem{pty}[thm]{Property} + +\numberwithin{equation}{section} + +% end-of-proof sign, to appear at right margin +% Paul Taylor and Chris Thompson, Cambridge, 1986 +% +\def\pushright#1{{% set up + \parfillskip=0pt % so \par doesn't push #1 to left + \widowpenalty=10000 % so we dont break the page before #1 + \displaywidowpenalty=10000 % ditto + \finalhyphendemerits=0 % TeXbook exercise 14.32 + % + % horizontal + \leavevmode % \nobreak means lines not pages + \unskip % remove previous space or glue + \nobreak % don't break lines + \hfil % ragged right if we spill over + \penalty50 % discouragement to do so + \hskip.2em % ensure some space + \null % anchor following \hfill + \hfill % push #1 to right + {#1} % the end-of-proof mark (or whatever) + % + % vertical + \par}} % build paragraph + +\def\qEd{{\lower1 pt\hbox{\vbox{\hrule\hbox{\vrule\kern4 pt + \vbox{\kern4 pt\hbox{\hss}\kern4 pt}\kern4 pt\vrule}\hrule}}}} +\def\qed{\pushright{\qEd} + \penalty-700 \par\addvspace{\medskipamount}} + +\newenvironment{Proof}[1][\proofname]{\par + \pushQED{\qed}% + \normalfont \topsep6\p@\@plus6\p@\relax + \trivlist + \item[\hskip\labelsep + \itshape + #1]\ignorespaces +}{% + \popQED\endtrivlist\@endpefalse +} +\newenvironment{iteMize}[1]{\begin{enumerate}[#1]}{\end{enumerate}} +\newenvironment{desCription}{\begin{enumerate}[\hbox to8 pt{\hfill}]}{\end{enumerate}} +% Bibliographystyle + +\bibliographystyle{alpha} + +\endinput diff -r eab84ac2603b -r 5df574281b69 LMCS-Paper/document/root.tex --- a/LMCS-Paper/document/root.tex Mon Aug 15 17:42:35 2011 +0200 +++ b/LMCS-Paper/document/root.tex Tue Aug 16 17:48:09 2011 +0200 @@ -1,5 +1,5 @@ -\documentclass{llncs} -\usepackage{times} +\documentclass{lmcs} +%%\usepackage{times} \usepackage{isabelle} \usepackage{isabellesym} \usepackage{amsmath} @@ -56,7 +56,7 @@ %%\newtheorem{lemma}[thm]{Lemma} %%\spnewtheorem{defn}[theorem]{Definition} %%\spnewtheorem{exmple}[theorem]{Example} -\spnewtheorem{myproperty}{Property}{\bfseries}{\rmfamily} +%%\spnewtheorem{myproperty}{Property}{\bfseries}{\rmfamily} %-------------------- environment definitions ----------------- \newenvironment{proof-of}[1]{{\em Proof of #1:}}{} @@ -64,11 +64,17 @@ \addtolength{\parskip}{-0.33mm} \begin{document} -\title{General Bindings and Alpha-Equivalence\\ in Nominal Isabelle} -\author{Christian Urban and Cezary Kaliszyk} -\institute{TU Munich, Germany} -%%%{\{urbanc, kaliszyk\}@in.tum.de} -\maketitle +\title[Genral Bindings]{General Bindings and Alpha-Equivalence in Nominal Isabelle} +\author{Christian Urban} +\address{Technical University of Munich, Germany} +\email{urbanc@in.tum.de} + +\author{Cezary Kaliszyk} +\address{University of Tsukuba, Japan} +\email{kaliszyk@score.cs.tsukuba.ac.jp} + +\keywords{Nominal Isabelle, variable convention, formal reasoning} +\subjclass{MANDATORY list of acm classifications} \begin{abstract} Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem @@ -79,27 +85,18 @@ term-constructors where multiple variables are bound at once. Such general bindings are ubiquitous in programming language research and only very poorly supported with single binders, such as lambda-abstractions. Our -extension includes new definitions of $\alpha$-equivalence and establishes -automatically the reasoning infrastructure for $\alpha$-equated terms. We +extension includes new definitions of alpha-equivalence and establishes +automatically the reasoning infrastructure for alpha-equated terms. We also prove strong induction principles that have the usual variable convention already built in. \end{abstract} -%\category{F.4.1}{subcategory}{third-level} - -%\terms -%formal reasoning, programming language calculi - -%\keywords -%nominal logic work, variable convention - - +\maketitle \input{session} -\begin{spacing}{0.9} - \bibliographystyle{plain} - \bibliography{root} -\end{spacing} +\bibliographystyle{plain} +\bibliography{root} + %\pagebreak %\input{Appendix}