# HG changeset patch # User Christian Urban # Date 1301435534 -7200 # Node ID 6f38e357b3378cd3629edd170a28946cd174348e # Parent a5da7b6aff8fe3cd0ed0fb06e202d166576da100 rearranged directories and updated to new Isabelle diff -r a5da7b6aff8f -r 6f38e357b337 ESOP-Paper/Appendix.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ESOP-Paper/Appendix.thy Tue Mar 29 23:52:14 2011 +0200 @@ -0,0 +1,135 @@ +(*<*) +theory Appendix +imports "../Nominal/Nominal2" "~~/src/HOL/Library/LaTeXsugar" +begin + +consts + fv :: "'a \ 'b" + abs_set :: "'a \ 'b \ 'c" + alpha_bn :: "'a \ 'a \ bool" + abs_set2 :: "'a \ perm \ 'b \ 'c" + Abs_dist :: "'a \ 'b \ 'c" + Abs_print :: "'a \ 'b \ 'c" + +definition + "equal \ (op =)" + +notation (latex output) + swap ("'(_ _')" [1000, 1000] 1000) and + fresh ("_ # _" [51, 51] 50) and + fresh_star ("_ #\<^sup>* _" [51, 51] 50) and + supp ("supp _" [78] 73) and + uminus ("-_" [78] 73) and + If ("if _ then _ else _" 10) and + alpha_set ("_ \\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and + alpha_lst ("_ \\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and + alpha_res ("_ \\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and + abs_set ("_ \\<^raw:{$\,_{\textit{abs\_set}}$}> _") and + abs_set2 ("_ \\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup> _") and + fv ("fa'(_')" [100] 100) and + equal ("=") and + alpha_abs_set ("_ \\<^raw:{$\,_{\textit{abs\_set}}$}> _") and + Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and + Abs_lst ("[_]\<^bsub>list\<^esub>._") and + Abs_dist ("[_]\<^bsub>#list\<^esub>._") and + Abs_res ("[_]\<^bsub>res\<^esub>._") and + Abs_print ("_\<^bsub>set\<^esub>._") and + Cons ("_::_" [78,77] 73) and + supp_set ("aux _" [1000] 10) and + alpha_bn ("_ \bn _") + +consts alpha_trm ::'a +consts fa_trm :: 'a +consts alpha_trm2 ::'a +consts fa_trm2 :: 'a +consts ast :: 'a +consts ast' :: 'a +notation (latex output) + alpha_trm ("\\<^bsub>trm\<^esub>") and + fa_trm ("fa\<^bsub>trm\<^esub>") and + alpha_trm2 ("'(\\<^bsub>assn\<^esub>, \\<^bsub>trm\<^esub>')") and + fa_trm2 ("'(fa\<^bsub>assn\<^esub>, fa\<^bsub>trm\<^esub>')") and + ast ("'(as, t')") and + ast' ("'(as', t\ ')") + +(*>*) + +text {* +\appendix +\section*{Appendix} + + Details for one case in Theorem \ref{suppabs}, which the reader might like to ignore. + By definition of the abstraction type @{text "abs_set"} + we have + % + \begin{equation}\label{abseqiff} + @{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\; + @{thm (rhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} + \end{equation} + + \noindent + and also + + \begin{equation}\label{absperm} + @{thm permute_Abs(1)[no_vars]}% + \end{equation} + + \noindent + The second fact derives from the definition of permutations acting on pairs + and $\alpha$-equivalence being equivariant. With these two facts at our disposal, we can show + the following lemma about swapping two atoms in an abstraction. + + \begin{lemma} + @{thm[mode=IfThen] Abs_swap1(1)[where bs="as", no_vars]} + \end{lemma} + + \begin{proof} + This lemma is straightforward using \eqref{abseqiff} and observing that + the assumptions give us @{term "(a \ b) \ (supp x - as) = (supp x - as)"}. + Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}). + \end{proof} + + \noindent + Assuming that @{text "x"} has finite support, this lemma together + with \eqref{absperm} allows us to show + + \begin{equation}\label{halfone} + @{thm Abs_supports(1)[no_vars]} + \end{equation} + + \noindent + which gives us ``one half'' of + Theorem~\ref{suppabs} (the notion of supports is defined in \cite{HuffmanUrban10}). + The ``other half'' is a bit more involved. To establish + it, we use a trick from \cite{Pitts04} and first define an auxiliary + function @{text aux}, taking an abstraction as argument: + @{thm supp_set.simps[THEN eq_reflection, no_vars]}. + + We can show that + @{text "aux"} is equivariant (since @{term "p \ (supp x - as) = (supp (p \ x)) - (p \ as)"}) + and therefore has empty support. + This in turn means + + \begin{center} + @{text "supp (aux ([as]\<^bsub>set\<^esub>. x)) \ supp ([as]\<^bsub>set\<^esub> x)"} + \end{center} + + \noindent + Assuming @{term "supp x - as"} is a finite set, + we further obtain + + \begin{equation}\label{halftwo} + @{thm (concl) Abs_supp_subset1(1)[no_vars]} + \end{equation} + + \noindent + since for finite sets of atoms, @{text "bs"}, we have + @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}. + Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes + Theorem~\ref{suppabs}. + +*} + +(*<*) +end +(*>*) diff -r a5da7b6aff8f -r 6f38e357b337 ESOP-Paper/Paper.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ESOP-Paper/Paper.thy Tue Mar 29 23:52:14 2011 +0200 @@ -0,0 +1,2393 @@ +(*<*) +theory Paper +imports "../Nominal/Nominal2" + "~~/src/HOL/Library/LaTeXsugar" +begin + +consts + fv :: "'a \ 'b" + abs_set :: "'a \ 'b \ 'c" + alpha_bn :: "'a \ 'a \ bool" + abs_set2 :: "'a \ perm \ 'b \ 'c" + Abs_dist :: "'a \ 'b \ 'c" + Abs_print :: "'a \ 'b \ 'c" + +definition + "equal \ (op =)" + +notation (latex output) + swap ("'(_ _')" [1000, 1000] 1000) and + fresh ("_ # _" [51, 51] 50) and + fresh_star ("_ #\<^sup>* _" [51, 51] 50) and + supp ("supp _" [78] 73) and + uminus ("-_" [78] 73) and + If ("if _ then _ else _" 10) and + alpha_set ("_ \\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and + alpha_lst ("_ \\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and + alpha_res ("_ \\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set+}}$}}>\<^bsup>_, _, _\<^esup> _") and + abs_set ("_ \\<^raw:{$\,_{\textit{abs\_set}}$}> _") and + abs_set2 ("_ \\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup> _") and + fv ("fa'(_')" [100] 100) and + equal ("=") and + alpha_abs_set ("_ \\<^raw:{$\,_{\textit{abs\_set}}$}> _") and + Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and + Abs_lst ("[_]\<^bsub>list\<^esub>._") and + Abs_dist ("[_]\<^bsub>#list\<^esub>._") and + Abs_res ("[_]\<^bsub>set+\<^esub>._") and + Abs_print ("_\<^bsub>set\<^esub>._") and + Cons ("_::_" [78,77] 73) and + supp_set ("aux _" [1000] 10) and + alpha_bn ("_ \bn _") + +consts alpha_trm ::'a +consts fa_trm :: 'a +consts alpha_trm2 ::'a +consts fa_trm2 :: 'a +consts ast :: 'a +consts ast' :: 'a +notation (latex output) + alpha_trm ("\\<^bsub>trm\<^esub>") and + fa_trm ("fa\<^bsub>trm\<^esub>") and + alpha_trm2 ("'(\\<^bsub>assn\<^esub>, \\<^bsub>trm\<^esub>')") and + fa_trm2 ("'(fa\<^bsub>assn\<^esub>, fa\<^bsub>trm\<^esub>')") and + ast ("'(as, t')") and + ast' ("'(as', t\ ')") + +(*>*) + + +section {* Introduction *} + +text {* + + 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, + Nominal Isabelle derives automatically a reasoning infrastructure that has + been used successfully in formalisations of an equivalence checking + algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed + Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency + \cite{BengtsonParow09} and a strong normalisation result for cut-elimination + in classical logic \cite{UrbanZhu08}. It has also been used by Pollack for + 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, + respectively, of the form + % + \begin{equation}\label{tysch} + \begin{array}{l} + @{text "T ::= x | T \ T"}\hspace{9mm} + @{text "S ::= \{x\<^isub>1,\, x\<^isub>n}. T"} + \end{array} + \end{equation} + % + \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. + + 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, + 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}. y \ x"}\hspace{10mm} + @{text "\{x, y}. x \ y \\<^isub>\ \{z}. z \ z"} + \end{equation} + % + \noindent + 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} + % + \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 + that can be used to faithfully represent this kind of binding in Nominal + 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). + + 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} + + \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} + @{text "\ x = 3 \ y = 2 \ z = foo \ x - y \"} + \end{center} + % + \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 + binders has to agree. + + 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} + % + \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} + @{text "\ (y, x) = (3, 2) \ x - y \"} + \end{center} + % + \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. + + 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} + % + \noindent + 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} + % + \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} + % + \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(\ x t as) = {x} \ bn(as)"} + \end{center} + % + \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. + + 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}. + + 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} + + \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 + 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 + %wealth of experience we gained with the older version of Nominal Isabelle: + %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 + %requires a lot of extra reasoning work. + + 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 + 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] + %\draw[step=2mm] (-4,-1) grid (4,1); + + \draw[very thick] (0.7,0.4) circle (4.25mm); + \draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9); + \draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05); + + \draw (-2.0, 0.845) -- (0.7,0.845); + \draw (-2.0,-0.045) -- (0.7,-0.045); + + \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}}; + \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[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3); + \draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism}; + + \end{tikzpicture} + \end{center} + % + \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). + + %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 + %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. + + The problem with introducing a new type in Isabelle/HOL is that in order to + be useful, a reasoning infrastructure needs to be ``lifted'' from the + underlying subset to the new type. This is usually a tricky and arduous + 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 + 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}"} + \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 + lifted function is characterised by the equations + + \begin{center} + @{text "fv\<^sup>\(x) = {x}"}\hspace{8mm} + @{text "fv\<^sup>\(t\<^isub>1 t\<^isub>2) = fv\<^sup>\(t\<^isub>1) \ fv\<^sup>\(t\<^isub>2)"}\hspace{8mm} + @{text "fv\<^sup>\(\x.t) = fv\<^sup>\(t) - {x}"} + \end{center} + + \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. + %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. + 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 + + %The examples we have in mind where our reasoning infrastructure will be + %helpful includes the term language of Core-Haskell. This term language + %involves patterns that have lists of type-, coercion- and term-variables, + %all of which are bound in @{text "\"}-expressions. In these + %patterns we do not know in advance how many variables need to + %be bound. Another example is the specification of SML, which includes + %includes bindings as in type-schemes.\medskip + + \noindent + {\bf Contributions:} We provide three new definitions for when terms + 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 + terms, including properties about support, freshness and equality + 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. + 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 from ``first principles''. + + + %\begin{figure} + %\begin{boxedminipage}{\linewidth} + %%\begin{center} + %\begin{tabular}{r@ {\hspace{1mm}}r@ {\hspace{2mm}}l} + %\multicolumn{3}{@ {}l}{Type Kinds}\\ + %@{text "\"} & @{text "::="} & @{text "\ | \\<^isub>1 \ \\<^isub>2"}\smallskip\\ + %\multicolumn{3}{@ {}l}{Coercion Kinds}\\ + %@{text "\"} & @{text "::="} & @{text "\\<^isub>1 \ \\<^isub>2"}\smallskip\\ + %\multicolumn{3}{@ {}l}{Types}\\ + %@{text "\"} & @{text "::="} & @{text "a | T | \\<^isub>1 \\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\"}}$@{text "\<^sup>n"} + %@{text "| \a:\. \ | \ \ \"}\smallskip\\ + %\multicolumn{3}{@ {}l}{Coercion Types}\\ + %@{text "\"} & @{text "::="} & @{text "c | C | \\<^isub>1 \\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\"}}$@{text "\<^sup>n"} + %@{text "| \c:\. \ | \ \ \ "}\\ + %& @{text "|"} & @{text "refl \ | sym \ | \\<^isub>1 \ \\<^isub>2 | \ @ \ | left \ | right \"}\\ + %& @{text "|"} & @{text "\\<^isub>1 \ \\<^isub>2 | rightc \ | leftc \ | \\<^isub>1 \ \\<^isub>2"}\smallskip\\ + %\multicolumn{3}{@ {}l}{Terms}\\ + %@{text "e"} & @{text "::="} & @{text "x | K | \a:\. e | \c:\. e | e \ | e \"}\\ + %& @{text "|"} & @{text "\x:\. e | e\<^isub>1 e\<^isub>2 | \ x:\ = e\<^isub>1 \ e\<^isub>2"}\\ + %& @{text "|"} & @{text "\ e\<^isub>1 \"}$\;\overline{@{text "p \ e\<^isub>2"}}$ @{text "| e \ \"}\smallskip\\ + %\multicolumn{3}{@ {}l}{Patterns}\\ + %@{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\"}}\;\overline{@{text "c:\"}}\;\overline{@{text "x:\"}}$\smallskip\\ + %\multicolumn{3}{@ {}l}{Constants}\\ + %& @{text C} & coercion constants\\ + %& @{text T} & value type constructors\\ + %& @{text "S\<^isub>n"} & n-ary type functions (which need to be fully applied)\\ + %& @{text K} & data constructors\smallskip\\ + %\multicolumn{3}{@ {}l}{Variables}\\ + %& @{text a} & type variables\\ + %& @{text c} & coercion variables\\ + %& @{text x} & term variables\\ + %\end{tabular} + %\end{center} + %\end{boxedminipage} + %\caption{The System @{text "F\<^isub>C"} + %\cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this + %version of @{text "F\<^isub>C"} we made a modification by separating the + %grammars for type kinds and coercion kinds, as well as for types and coercion + %types. For this paper the interesting term-constructor is @{text "\"}, + %which binds multiple type-, coercion- and term-variables.\label{corehas}} + %\end{figure} +*} + +section {* A Short Review of the Nominal Logic Work *} + +text {* + At its core, Nominal Isabelle is an adaption of the nominal logic work by + Pitts \cite{Pitts03}. This adaptation for Isabelle/HOL is described in + \cite{HuffmanUrban10} (including proofs). We shall briefly review this work + to aid the description of what follows. + + Two central notions in the nominal logic work are sorted atoms and + 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. + 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. + + Permutations are bijective functions from atoms to atoms that are + the identity everywhere except on a finite number of atoms. There is a + two-place permutation operation written + @{text "_ \ _ :: perm \ \ \ \"} + where the generic type @{text "\"} is the type of the object + over which the permutation + acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"}, + the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}}, + and the inverse permutation of @{term p} as @{text "- p"}. The permutation + operation is defined over the type-hierarchy \cite{HuffmanUrban10}; + for example permutations acting on products, lists, sets, functions and booleans are + given by: + % + %\begin{equation}\label{permute} + %\mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}} + %\begin{tabular}{@ {}l@ {}} + %@{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm] + %@{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\ + %@{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\ + %\end{tabular} & + %\begin{tabular}{@ {}l@ {}} + %@{thm permute_set_eq[no_vars, THEN eq_reflection]}\\ + %@{text "p \ f \ \x. p \ (f (- p \ x))"}\\ + %@{thm permute_bool_def[no_vars, THEN eq_reflection]} + %\end{tabular} + %\end{tabular}} + %\end{equation} + % + \begin{center} + \mbox{\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {\hspace{4mm}}c@ {}} + \begin{tabular}{@ {}l@ {}} + @{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\ + @{thm permute_bool_def[no_vars, THEN eq_reflection]} + \end{tabular} & + \begin{tabular}{@ {}l@ {}} + @{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\ + @{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\ + \end{tabular} & + \begin{tabular}{@ {}l@ {}} + @{thm permute_set_eq[no_vars, THEN eq_reflection]}\\ + @{text "p \ f \ \x. p \ (f (- p \ x))"}\\ + \end{tabular} + \end{tabular}} + \end{center} + + \noindent + Concrete permutations in Nominal Isabelle are built up from swappings, + written as \mbox{@{text "(a b)"}}, which are permutations that behave + as follows: + % + \begin{center} + @{text "(a b) = \c. if a = c then b else if b = c then a else c"} + \end{center} + + 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, + 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: + % + \begin{equation}\label{suppdef} + @{thm supp_def[no_vars, THEN eq_reflection]} + \end{equation} + + \noindent + There is also the derived notion for when an atom @{text a} is \emph{fresh} + for an @{text x}, defined as @{thm fresh_def[no_vars]}. + We use for sets of atoms the abbreviation + @{thm (lhs) fresh_star_def[no_vars]}, defined as + @{thm (rhs) fresh_star_def[no_vars]}. + A striking consequence of these definitions is that we can prove + without knowing anything about the structure of @{term x} that + swapping two fresh atoms, say @{text a} and @{text b}, leaves + @{text x} unchanged, namely if @{text "a \ x"} and @{text "b \ x"} + then @{term "(a \ b) \ x = x"}. + % + %\begin{myproperty}\label{swapfreshfresh} + %@{thm[mode=IfThen] swap_fresh_fresh[no_vars]} + %\end{myproperty} + % + %While often the support of an object can be relatively easily + %described, for example for atoms, products, lists, function applications, + %booleans and permutations as follows + %% + %\begin{center} + %\begin{tabular}{c@ {\hspace{10mm}}c} + %\begin{tabular}{rcl} + %@{term "supp a"} & $=$ & @{term "{a}"}\\ + %@{term "supp (x, y)"} & $=$ & @{term "supp x \ supp y"}\\ + %@{term "supp []"} & $=$ & @{term "{}"}\\ + %@{term "supp (x#xs)"} & $=$ & @{term "supp x \ supp xs"}\\ + %\end{tabular} + %& + %\begin{tabular}{rcl} + %@{text "supp (f x)"} & @{text "\"} & @{term "supp f \ supp x"}\\ + %@{term "supp b"} & $=$ & @{term "{}"}\\ + %@{term "supp p"} & $=$ & @{term "{a. p \ a \ a}"} + %\end{tabular} + %\end{tabular} + %\end{center} + % + %\noindent + %in some cases it can be difficult to characterise the support precisely, and + %only an approximation can be established (as for functions above). + % + %Reasoning about + %such approximations can be simplified with the notion \emph{supports}, defined + %as follows: + % + %\begin{definition} + %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} + % + %\noindent + %The main point of @{text supports} is that we can establish the following + %two properties. + % + %\begin{myproperty}\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} + % + %Another important notion in the nominal logic work is \emph{equivariance}. + %For a function @{text f}, say of type @{text "\ \ \"}, to be equivariant + %it is required that every permutation leaves @{text f} unchanged, that is + %% + %\begin{equation}\label{equivariancedef} + %@{term "\p. p \ f = f"} + %\end{equation} + % + %\noindent or equivalently that a permutation applied to the application + %@{text "f x"} can be moved to the argument @{text x}. That means for equivariant + %functions @{text f}, we have for all permutations @{text p}: + %% + %\begin{equation}\label{equivariance} + %@{text "p \ f = f"} \;\;\;\textit{if and only if}\;\;\; + %@{text "p \ (f x) = f (p \ x)"} + %\end{equation} + % + %\noindent + %From property \eqref{equivariancedef} and the definition of @{text supp}, we + %can easily deduce that equivariant functions have empty support. There is + %also a similar notion for equivariant relations, say @{text R}, namely the property + %that + %% + %\begin{center} + %@{text "x R y"} \;\;\textit{implies}\;\; @{text "(p \ x) R (p \ y)"} + %\end{center} + % + %Using freshness, the nominal logic work provides us with general means for renaming + %binders. + % + %\noindent + While in the older version of Nominal Isabelle, we used extensively + %Property~\ref{swapfreshfresh} + this property to rename single binders, it %%this property + 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} + @{thm[mode=IfThen] supp_perm_eq[no_vars]} + \end{myproperty} + + \begin{myproperty}\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} + + \noindent + The idea behind the second property is that given a finite set @{text as} + of binders (being bound, or fresh, in @{text x} is ensured by the + assumption @{term "as \* x"}), then there exists a permutation @{text p} such that + the renamed binders @{term "p \ as"} avoid @{text c} (which can be arbitrarily chosen + as long as it is finitely supported) and also @{text "p"} does not affect anything + in the support of @{text x} (that is @{term "supp x \* p"}). The last + fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders + @{text as} in @{text x}, because @{term "p \ x = x"}. + + 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 + the presence of multiple binders. +*} + + +section {* General Bindings\label{sec:binders} *} + +text {* + In Nominal Isabelle, the user is expected to write down a specification of a + term-calculus and then a reasoning infrastructure is automatically derived + from this specification (remember that Nominal Isabelle is a definitional + extension of Isabelle/HOL, which does not introduce any new axioms). + + In order to keep our work with deriving the reasoning infrastructure + manageable, we will wherever possible state definitions and perform proofs + on the ``user-level'' of Isabelle/HOL, as opposed to write custom ML-code. % that + %generates them anew for each specification. + To that end, we will consider + first pairs @{text "(as, x)"} of type @{text "(atom set) \ \"}. These pairs + are intended to represent the abstraction, or binding, of the set of atoms @{text + "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 + 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 + atoms; moreover there must be a permutation @{text p} such that {\it + (ii)} @{text p} leaves the free atoms of @{text x} and @{text y} unchanged, but + {\it (iii)} ``moves'' their bound names so that we obtain modulo a relation, + say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)} + @{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The + requirements {\it (i)} to {\it (iv)} can be stated formally as the conjunction of: + % + \begin{equation}\label{alphaset} + \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l} + \multicolumn{4}{l}{@{term "(as, x) \set R fa p (bs, y)"}\hspace{2mm}@{text "\"}}\\[1mm] + \mbox{\it (i)} & @{term "fa(x) - as = fa(y) - bs"} & + \mbox{\it (iii)} & @{text "(p \ x) R y"} \\ + \mbox{\it (ii)} & @{term "(fa(x) - as) \* p"} & + \mbox{\it (iv)} & @{term "(p \ as) = bs"} \\ + \end{array} + \end{equation} + % + \noindent + Note that this relation depends on the permutation @{text + "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 + 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 + for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \ \"} + as follows + % + \begin{equation}\label{alphalist} + \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l} + \multicolumn{4}{l}{@{term "(as, x) \lst R fa p (bs, y)"}\hspace{2mm}@{text "\"}}\\[1mm] + \mbox{\it (i)} & @{term "fa(x) - (set as) = fa(y) - (set bs)"} & + \mbox{\it (iii)} & @{text "(p \ x) R y"}\\ + \mbox{\it (ii)} & @{term "(fa(x) - set as) \* p"} & + \mbox{\it (iv)} & @{term "(p \ as) = bs"}\\ + \end{array} + \end{equation} + % + \noindent + where @{term set} is the function that coerces a list of atoms into a set of atoms. + Now the last clause ensures that the order of the binders matters (since @{text as} + and @{text bs} are lists of atoms). + + If we do not want to make any difference between the order of binders \emph{and} + also allow vacuous binders, that means \emph{restrict} names, then we keep sets of binders, but drop + condition {\it (iv)} in \eqref{alphaset}: + % + \begin{equation}\label{alphares} + \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l} + \multicolumn{2}{l}{@{term "(as, x) \res R fa p (bs, y)"}\hspace{2mm}@{text "\"}}\\[1mm] + \mbox{\it (i)} & @{term "fa(x) - as = fa(y) - bs"} & + \mbox{\it (iii)} & @{text "(p \ x) R y"}\\ + \mbox{\it (ii)} & @{term "(fa(x) - as) \* p"}\\ + \end{array} + \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 + 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 + % + \begin{center} + @{text "fa(x) = {x}"} \hspace{5mm} @{text "fa(T\<^isub>1 \ T\<^isub>2) = fa(T\<^isub>1) \ fa(T\<^isub>2)"} + \end{center} + + \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 + $\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)"} + since there is no permutation that makes the lists @{text "[x, y]"} and + @{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \ y"}} + unchanged. Another example is @{text "({x}, x)"} $\approx_{\,\textit{set+}}$ + @{text "({x, y}, x)"} which holds by taking @{text p} to be the identity + permutation. However, if @{text "x \ y"}, then @{text "({x}, x)"} + $\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 + abstract a single atom. + + In the rest of this section we are going to introduce three abstraction + types. For this we define + % + \begin{equation} + @{term "abs_set (as, x) (bs, x) \ \p. alpha_set (as, x) equal supp p (bs, x)"} + \end{equation} + + \noindent + (similarly for $\approx_{\,\textit{abs\_set+}}$ + and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence + relations. %% and equivariant. + + \begin{lemma}\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} + + \begin{proof} + Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have + a permutation @{text p} and for the proof obligation take @{term "-p"}. In case + of transitivity, we have two permutations @{text p} and @{text q}, and for the + proof obligation use @{text "q + p"}. All conditions are then by simple + calculations. + \end{proof} + + \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 + @{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 + % + %\begin{center} + @{term "Abs_set as x"}, %\hspace{5mm} + @{term "Abs_res as x"} and %\hspace{5mm} + @{term "Abs_lst as x"}, + %\end{center} + % + %\noindent + indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will + call the types \emph{abstraction types} and their elements + \emph{abstractions}. The important property we need to derive is the support of + abstractions, namely: + + \begin{theorem}[Support of Abstractions]\label{suppabs} + Assuming @{text x} has finite support, then + + \begin{center} + \begin{tabular}{l} + @{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="bs", no_vars]} $\;\;=\;\;$ + @{thm (rhs) supp_Abs(3)[where bs="bs", no_vars]} + \end{tabular} + \end{center} + \end{theorem} + + \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. + + %\noindent + %Below we will show the first equation. The others + %follow by similar arguments. By definition of the abstraction type @{text "abs_set"} + %we have + %% + %\begin{equation}\label{abseqiff} + %@{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\; + %@{thm (rhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} + %\end{equation} + % + %\noindent + %and also + % + %\begin{equation}\label{absperm} + %%@%{%thm %permute_Abs[no_vars]}% + %\end{equation} + + %\noindent + %The second fact derives from the definition of permutations acting on pairs + %\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} + %@{thm[mode=IfThen] Abs_swap1(1)[where bs="as", no_vars]} + %\end{lemma} + % + %\begin{proof} + %This lemma is straightforward using \eqref{abseqiff} and observing that + %the assumptions give us @{term "(a \ b) \ (supp x - as) = (supp x - as)"}. + %Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}). + %\end{proof} + % + %\noindent + %Assuming that @{text "x"} has finite support, this lemma together + %with \eqref{absperm} allows us to show + % + %\begin{equation}\label{halfone} + %@{thm Abs_supports(1)[no_vars]} + %\end{equation} + % + %\noindent + %which by Property~\ref{supportsprop} gives us ``one half'' of + %Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish + %it, we use a trick from \cite{Pitts04} and first define an auxiliary + %function @{text aux}, taking an abstraction as argument: + %@{thm supp_set.simps[THEN eq_reflection, no_vars]}. + % + %Using the second equation in \eqref{equivariance}, we can show that + %@{text "aux"} is equivariant (since @{term "p \ (supp x - as) = (supp (p \ x)) - (p \ as)"}) + %and therefore has empty support. + %This in turn means + % + %\begin{center} + %@{term "supp (supp_gen (Abs_set as x)) \ supp (Abs_set as x)"} + %\end{center} + % + %\noindent + %using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set, + %we further obtain + % + %\begin{equation}\label{halftwo} + %@{thm (concl) Abs_supp_subset1(1)[no_vars]} + %\end{equation} + % + %\noindent + %since for finite sets of atoms, @{text "bs"}, we have + %@{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}. + %Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes + %Theorem~\ref{suppabs}. + + The method of first considering abstractions of the + form @{term "Abs_set as x"} etc is motivated by the fact that + we can conveniently establish at the Isabelle/HOL level + 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. +*} + +section {* Specifying General Bindings\label{sec:spec} *} + +text {* + Our choice of syntax for specifications is influenced by the existing + datatype package of Isabelle/HOL %\cite{Berghofer99} + and by the syntax of the + Ott-tool \cite{ott-jfp}. For us a specification of a term-calculus is a + collection of (possibly mutual recursive) type declarations, say @{text + "ty\\<^isub>1, \, ty\\<^isub>n"}, and an associated collection of + binding functions, say @{text "bn\\<^isub>1, \, bn\\<^isub>m"}. The + syntax in Nominal Isabelle for such specifications is roughly as follows: + % + \begin{equation}\label{scheme} + \mbox{\begin{tabular}{@ {}p{2.5cm}l} + type \mbox{declaration part} & + $\begin{cases} + \mbox{\small\begin{tabular}{l} + \isacommand{nominal\_datatype} @{text "ty\\<^isub>1 = \"}\\ + \isacommand{and} @{text "ty\\<^isub>2 = \"}\\ + \raisebox{2mm}{$\ldots$}\\[-2mm] + \isacommand{and} @{text "ty\\<^isub>n = \"}\\ + \end{tabular}} + \end{cases}$\\ + binding \mbox{function part} & + $\begin{cases} + \mbox{\small\begin{tabular}{l} + \isacommand{binder} @{text "bn\\<^isub>1"} \isacommand{and} \ldots \isacommand{and} @{text "bn\\<^isub>m"}\\ + \isacommand{where}\\ + \raisebox{2mm}{$\ldots$}\\[-2mm] + \end{tabular}} + \end{cases}$\\ + \end{tabular}} + \end{equation} + + \noindent + Every type declaration @{text ty}$^\alpha_{1..n}$ consists of a collection of + term-constructors, each of which comes with a list of labelled + types that stand for the types of the arguments of the term-constructor. + For example a term-constructor @{text "C\<^sup>\"} might be specified with + + \begin{center} + @{text "C\<^sup>\ label\<^isub>1::ty"}$'_1$ @{text "\ label\<^isub>l::ty"}$'_l\;\;$ @{text "binding_clauses"} + \end{center} + + \noindent + whereby some of the @{text ty}$'_{1..l}$ %%(or their components) + can be contained + in the collection of @{text ty}$^\alpha_{1..n}$ declared in + \eqref{scheme}. + In this case we will call the corresponding argument a + \emph{recursive argument} of @{text "C\<^sup>\"}. + %The types of such recursive + %arguments need to satisfy a ``positivity'' + %restriction, which ensures that the type has a set-theoretic semantics + %\cite{Berghofer99}. + The labels + annotated on the types are optional. Their purpose is to be used in the + (possibly empty) list of \emph{binding clauses}, which indicate the binders + and their scope in a term-constructor. They come in three \emph{modes}: + % + \begin{center} + \begin{tabular}{@ {}l@ {}} + \isacommand{bind} {\it binders} \isacommand{in} {\it bodies}\;\;\;\, + \isacommand{bind (set)} {\it binders} \isacommand{in} {\it bodies}\;\;\;\, + \isacommand{bind (set+)} {\it binders} \isacommand{in} {\it bodies} + \end{tabular} + \end{center} + % + \noindent + 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 + 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. + + %For example we allow + %binding clauses of the form: + % + %\begin{center} + %\begin{tabular}{@ {}ll@ {}} + %@{text "Foo\<^isub>1 x::name y::name t::trm s::trm"} & + % \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}\\ + %@{text "Foo\<^isub>2 x::name y::name t::trm s::trm"} & + % \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t"}, + % \isacommand{bind} @{text "x y"} \isacommand{in} @{text "s"}\\ + %\end{tabular} + %\end{center} + + \noindent + %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 + %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 + 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 + atoms of a body cannot be free at the same time by specifying an + alternative binder for the same body). + + For binders we distinguish between + \emph{shallow} and \emph{deep} binders. Shallow binders are just + labels. The restriction we need to impose on them is that in case of + \isacommand{bind (set)} and \isacommand{bind (set+)} the labels must either + refer to atom types or to sets of atom types; in case of \isacommand{bind} + the labels must refer to atom types or lists of atom types. Two examples for + the use of shallow binders are the specification of lambda-terms, where a + single name is bound, and type-schemes, where a finite set of names is + bound: + + \begin{center}\small + \begin{tabular}{@ {}c@ {\hspace{7mm}}c@ {}} + \begin{tabular}{@ {}l} + \isacommand{nominal\_datatype} @{text lam} $=$\\ + \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"}~~% + \isacommand{bind (set+)} @{text xs} \isacommand{in} @{text T}\\ + \end{tabular} + \end{tabular} + \end{center} + + \noindent + In these specifications @{text "name"} refers to an atom type, and @{text + "fset"} to the type of finite sets. + Note that for @{text lam} it does not matter which binding mode we use. The + reason is that we bind only a single @{text name}. However, having + \isacommand{bind (set)} or \isacommand{bind} in the second case makes a + difference to the semantics of the specification (which we will define in the next section). + + + A \emph{deep} binder uses an auxiliary binding function that ``picks'' out + the atoms in one argument of the term-constructor, which can be bound in + other arguments and also in the same argument (we will call such binders + \emph{recursive}, see below). The binding functions are + expected to return either a set of atoms (for \isacommand{bind (set)} and + \isacommand{bind (set+)}) or a list of atoms (for \isacommand{bind}). They can + be defined by recursion over the corresponding type; the equations + must be given in the binding function part of the scheme shown in + \eqref{scheme}. For example a term-calculus containing @{text "Let"}s with + tuple patterns might be specified as: + % + \begin{equation}\label{letpat} + \mbox{\small% + \begin{tabular}{l} + \isacommand{nominal\_datatype} @{text trm} $=$\\ + \hspace{5mm}\phantom{$\mid$}~@{term "Var name"}\\ + \hspace{5mm}$\mid$~@{term "App trm trm"}\\ + \hspace{5mm}$\mid$~@{text "Lam x::name t::trm"} + \;\;\isacommand{bind} @{text x} \isacommand{in} @{text t}\\ + \hspace{5mm}$\mid$~@{text "Let p::pat trm t::trm"} + \;\;\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}\\ + \isacommand{and} @{text pat} $=$ + @{text PNil} + $\mid$~@{text "PVar name"} + $\mid$~@{text "PTup pat pat"}\\ + \isacommand{binder}~@{text "bn::pat \ atom list"}\\ + \isacommand{where}~@{text "bn(PNil) = []"}\\ + \hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\ + \hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\smallskip\\ + \end{tabular}} + \end{equation} + % + \noindent + In this specification the function @{text "bn"} determines which atoms of + the pattern @{text p} are bound in the argument @{text "t"}. Note that in the + second-last @{text bn}-clause the function @{text "atom"} coerces a name + into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This + allows us to treat binders of different atom type uniformly. + + As said above, for deep binders we allow binding clauses such as + % + %\begin{center} + %\begin{tabular}{ll} + @{text "Bar p::pat t::trm"} %%%& + \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"} %%\\ + %\end{tabular} + %\end{center} + % + %\noindent + where the argument of the deep binder also occurs in the body. We call such + binders \emph{recursive}. To see the purpose of such recursive binders, + compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s in the following + specification: + % + \begin{equation}\label{letrecs} + \mbox{\small% + \begin{tabular}{@ {}l@ {}} + \isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\ + \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"} + \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t}\\ + \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"} + \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\ + \isacommand{and} @{text "assn"} $=$ + @{text "ANil"} + $\mid$~@{text "ACons name trm assn"}\\ + \isacommand{binder} @{text "bn::assn \ atom list"}\\ + \isacommand{where}~@{text "bn(ANil) = []"}\\ + \hspace{5mm}$\mid$~@{text "bn(ACons a t as) = [atom a] @ bn(as)"}\\ + \end{tabular}} + \end{equation} + % + \noindent + 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. + + 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{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}\\ + @{text "Baz\<^isub>2 p::pat t\<^isub>1::trm t\<^isub>2::trm"} & + \isacommand{bind} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "t\<^isub>1"}, + \isacommand{bind} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "t\<^isub>2"}\\ + \end{tabular} + \end{center} + + \noindent + 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.) + + 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 + 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 + not have a binding clause (all arguments are used to define @{text "bn"}). + 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. + + In the version of + Nominal Isabelle described here, we also adopted the restriction from the + Ott-tool that binding functions can only return: the empty set or empty list + (as in case @{text PNil}), a singleton set or singleton list containing an + atom (case @{text PVar}), or unions of atom sets or appended atom lists + (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, + 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} + already part of a binding clause given by the user, we add implicitly a special \emph{empty} binding + clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case + of the lambda-terms, the completion produces + + \begin{center}\small + \begin{tabular}{@ {}l@ {\hspace{-1mm}}} + \isacommand{nominal\_datatype} @{text lam} =\\ + \hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"} + \;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "x"}\\ + \hspace{5mm}$\mid$~@{text "App t\<^isub>1::lam t\<^isub>2::lam"} + \;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>1 t\<^isub>2"}\\ + \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"} + \;\;\isacommand{bind}~@{text x} \isacommand{in} @{text t}\\ + \end{tabular} + \end{center} + + \noindent + The point of completion is that we can make definitions over the binding + clauses and be sure to have captured all arguments of a term constructor. +*} + +section {* Alpha-Equivalence and Free Atoms\label{sec:alpha} *} + +text {* + Having dealt with all syntax matters, the problem now is how we can turn + specifications into actual type definitions in Isabelle/HOL and then + establish a reasoning infrastructure for them. As + Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, just + re-arranging the arguments of + term-constructors so that binders and their bodies are next to each other will + 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. + + 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 + 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 + @{text "ty\<^sup>\"} and @{text "C"} is the term-constructor on the ``raw'' type @{text "ty"}. + + %The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are + %non-empty and the types in the constructors only occur in positive + %position (see \cite{Berghofer99} for an in-depth description of the datatype package + %in Isabelle/HOL). + We subsequently define each of the user-specified binding + functions @{term "bn"}$_{1..m}$ by recursion over the corresponding + raw datatype. We can also easily define permutation operations by + recursion so that for each term constructor @{text "C"} we have that + % + \begin{equation}\label{ceqvt} + @{text "p \ (C z\<^isub>1 \ z\<^isub>n) = C (p \ z\<^isub>1) \ (p \ z\<^isub>n)"} + \end{equation} + + The first non-trivial step we have to perform is the generation of + free-atom functions from the specification. For the + \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions + % + %\begin{equation}\label{fvars} + @{text "fa_ty\<^isub>"}$_{1..n}$ + %\end{equation} + % + %\noindent + by recursion. + We define these functions together with auxiliary free-atom functions for + the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$ + we define + % + %\begin{center} + @{text "fa_bn\<^isub>"}$_{1..m}$. + %\end{center} + % + %\noindent + The reason for this setup is that in a deep binder not all atoms have to be + bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function + that calculates those free atoms in a deep binder. + + While the idea behind these free-atom functions is clear (they just + collect all atoms that are not bound), because of our rather complicated + binding mechanisms their definitions are somewhat involved. Given + a term-constructor @{text "C"} of type @{text ty} and some associated + binding clauses @{text "bc\<^isub>1\bc\<^isub>k"}, the result of @{text + "fa_ty (C z\<^isub>1 \ z\<^isub>n)"} will be the union @{text + "fa(bc\<^isub>1) \ \ \ fa(bc\<^isub>k)"} where we will define below what @{text "fa"} for a binding + clause means. We only show the details for the mode \isacommand{bind (set)} (the other modes are similar). + Suppose the binding clause @{text bc\<^isub>i} is of the form + % + %\begin{center} + \mbox{\isacommand{bind (set)} @{text "b\<^isub>1\b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\d\<^isub>q"}} + %\end{center} + % + %\noindent + in which the body-labels @{text "d"}$_{1..q}$ refer to types @{text ty}$_{1..q}$, + and the binders @{text b}$_{1..p}$ + either refer to labels of atom types (in case of shallow binders) or to binding + functions taking a single label as argument (in case of deep binders). Assuming + @{text "D"} stands for the set of free atoms of the bodies, @{text B} for the + set of binding atoms in the binders and @{text "B'"} for the set of free atoms in + non-recursive deep binders, + then the free atoms of the binding clause @{text bc\<^isub>i} are\\[-2mm] + % + \begin{equation}\label{fadef} + \mbox{@{text "fa(bc\<^isub>i) \ (D - B) \ B'"}}. + \end{equation} + % + \noindent + The set @{text D} is formally defined as + % + %\begin{center} + @{text "D \ fa_ty\<^isub>1 d\<^isub>1 \ ... \ fa_ty\<^isub>q d\<^isub>q"} + %\end{center} + % + %\noindent + where in case @{text "d\<^isub>i"} refers to one of the raw types @{text "ty"}$_{1..n}$ from the + specification, the function @{text "fa_ty\<^isub>i"} is the corresponding free-atom function + we are defining by recursion; + %(see \eqref{fvars}); + otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}. + + In order to formally define the set @{text B} we use the following auxiliary @{text "bn"}-functions + for atom types to which shallow binders may refer\\[-4mm] + % + %\begin{center} + %\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} + %@{text "bn_atom a"} & @{text "\"} & @{text "{atom a}"}\\ + %@{text "bn_atom_set as"} & @{text "\"} & @{text "atoms as"}\\ + %@{text "bn_atom_list as"} & @{text "\"} & @{text "atoms (set as)"} + %\end{tabular} + %\end{center} + % + \begin{center} + @{text "bn\<^bsub>atom\<^esub> a \ {atom a}"}\hfill + @{text "bn\<^bsub>atom_set\<^esub> as \ atoms as"}\hfill + @{text "bn\<^bsub>atom_list\<^esub> as \ atoms (set as)"} + \end{center} + % + \noindent + Like the function @{text atom}, the function @{text "atoms"} coerces + a set of atoms to a set of the generic atom type. + %It is defined as @{text "atoms as \ {atom a | a \ as}"}. + The set @{text B} is then formally defined as\\[-4mm] + % + \begin{center} + @{text "B \ bn_ty\<^isub>1 b\<^isub>1 \ ... \ bn_ty\<^isub>p b\<^isub>p"} + \end{center} + % + \noindent + where we use the auxiliary binding functions for shallow binders. + The set @{text "B'"} collects all free atoms in non-recursive deep + binders. Let us assume these binders in @{text "bc\<^isub>i"} are + % + %\begin{center} + \mbox{@{text "bn\<^isub>1 l\<^isub>1, \, bn\<^isub>r l\<^isub>r"}} + %\end{center} + % + %\noindent + with @{text "l"}$_{1..r}$ $\subseteq$ @{text "b"}$_{1..p}$ and none of the + @{text "l"}$_{1..r}$ being among the bodies @{text + "d"}$_{1..q}$. The set @{text "B'"} is defined as\\[-5mm] + % + \begin{center} + @{text "B' \ fa_bn\<^isub>1 l\<^isub>1 \ ... \ fa_bn\<^isub>r l\<^isub>r"}\\[-9mm] + \end{center} + % + \noindent + This completes the definition of the free-atom functions @{text "fa_ty"}$_{1..n}$. + + Note that for non-recursive deep binders, we have to add in \eqref{fadef} + the set of atoms that are left unbound by the binding functions @{text + "bn"}$_{1..m}$. We used for the definition of + this set the functions @{text "fa_bn"}$_{1..m}$, which are also defined by mutual + recursion. Assume the user specified a @{text bn}-clause of the form + % + %\begin{center} + @{text "bn (C z\<^isub>1 \ z\<^isub>s) = rhs"} + %\end{center} + % + %\noindent + where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$. For each of + the arguments we calculate the free atoms as follows: + % + \begin{center} + \begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}} + $\bullet$ & @{term "fa_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"} + (that means nothing is bound in @{text "z\<^isub>i"} by the binding function),\\ + $\bullet$ & @{term "fa_bn\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} occurs in @{text "rhs"} + with the recursive call @{text "bn\<^isub>i z\<^isub>i"}, and\\ + $\bullet$ & @{term "{}"} provided @{text "z\<^isub>i"} occurs in @{text "rhs"}, + but without a recursive call. + \end{tabular} + \end{center} + % + \noindent + For defining @{text "fa_bn (C z\<^isub>1 \ z\<^isub>n)"} we just union up all these sets. + + To see how these definitions work in practice, let us reconsider the + term-constructors @{text "Let"} and @{text "Let_rec"} shown in + \eqref{letrecs} together with the term-constructors for assignments @{text + "ANil"} and @{text "ACons"}. Since there is a binding function defined for + assignments, we have three free-atom functions, namely @{text + "fa\<^bsub>trm\<^esub>"}, @{text "fa\<^bsub>assn\<^esub>"} and @{text + "fa\<^bsub>bn\<^esub>"} as follows: + % + \begin{center}\small + \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] + + @{text "fa\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\ + @{text "fa\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(supp a) \ (fa\<^bsub>trm\<^esub> t) \ (fa\<^bsub>assn\<^esub> as)"}\\[1mm] + + @{text "fa\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\ + @{text "fa\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t) \ (fa\<^bsub>bn\<^esub> as)"} + \end{tabular} + \end{center} + + \noindent + Recall that @{text ANil} and @{text "ACons"} have no + binding clause in the specification. The corresponding free-atom + function @{text "fa\<^bsub>assn\<^esub>"} therefore returns all free atoms + of an assignment (in case of @{text "ACons"}, they are given in + terms of @{text supp}, @{text "fa\<^bsub>trm\<^esub>"} and @{text "fa\<^bsub>assn\<^esub>"}). + The binding only takes place in @{text Let} and + @{text "Let_rec"}. In case of @{text "Let"}, the binding clause specifies + that all atoms given by @{text "set (bn as)"} have to be bound in @{text + t}. Therefore we have to subtract @{text "set (bn as)"} from @{text + "fa\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are + free in @{text "as"}. This is + in contrast with @{text "Let_rec"} where we have a recursive + binder to bind all occurrences of the atoms in @{text + "set (bn as)"} also inside @{text "as"}. Therefore we have to subtract + @{text "set (bn as)"} from both @{text "fa\<^bsub>trm\<^esub> t"} and @{text "fa\<^bsub>assn\<^esub> as"}. + %Like the function @{text "bn"}, the function @{text "fa\<^bsub>bn\<^esub>"} traverses the + %list of assignments, but instead returns the free atoms, which means in this + %example the free atoms in the argument @{text "t"}. + + An interesting point in this + example is that a ``naked'' assignment (@{text "ANil"} or @{text "ACons"}) does not bind any + atoms, even if the binding function is specified over assignments. + 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 + atoms that are bound. In that case, these functions would \emph{not} respect + $\alpha$-equivalence. + + Next we define the $\alpha$-equivalence relations for the raw types @{text + "ty"}$_{1..n}$ from the specification. We write them as + % + %\begin{center} + @{text "\ty"}$_{1..n}$. + %\end{center} + % + %\noindent + Like with the free-atom functions, we also need to + define auxiliary $\alpha$-equivalence relations + % + %\begin{center} + @{text "\bn\<^isub>"}$_{1..m}$ + %\end{center} + % + %\noindent + for the binding functions @{text "bn"}$_{1..m}$, + To simplify our definitions we will use the following abbreviations for + \emph{compound equivalence relations} and \emph{compound free-atom functions} acting on tuples. + % + \begin{center} + \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} + @{text "(x\<^isub>1,\, x\<^isub>n) (R\<^isub>1,\, R\<^isub>n) (x\\<^isub>1,\, x\\<^isub>n)"} & @{text "\"} & + @{text "x\<^isub>1 R\<^isub>1 x\\<^isub>1 \ \ \ x\<^isub>n R\<^isub>n x\\<^isub>n"}\\ + @{text "(fa\<^isub>1,\, fa\<^isub>n) (x\<^isub>1,\, x\<^isub>n)"} & @{text "\"} & @{text "fa\<^isub>1 x\<^isub>1 \ \ \ fa\<^isub>n x\<^isub>n"}\\ + \end{tabular} + \end{center} + + + 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 + % + \begin{center} + \mbox{\infer{@{text "C z\<^isub>1 \ z\<^isub>n \ty C z\\<^isub>1 \ z\\<^isub>n"}} + {@{text "prems(bc\<^isub>1) \ prems(bc\<^isub>k)"}}} + \end{center} + + \noindent + The task below is to specify what the premises of a binding clause are. As a + special instance, we first treat the case where @{text "bc\<^isub>i"} is the + empty binding clause of the form + % + \begin{center} + \mbox{\isacommand{bind (set)} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\d\<^isub>q"}.} + \end{center} + + \noindent + 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 + % + \begin{equation}\label{rempty} + \mbox{@{text "R \ (R\<^isub>1,\, R\<^isub>q)"}} + \end{equation} + + \noindent + with @{text "R\<^isub>i"} being @{text "\ty\<^isub>i"} if the corresponding labels @{text "d\<^isub>i"} and + @{text "d\\<^isub>i"} refer + to a recursive argument of @{text C} with type @{text "ty\<^isub>i"}; otherwise + we take @{text "R\<^isub>i"} to be the equality @{text "="}. This lets us define + the premise for an empty binding clause succinctly as @{text "prems(bc\<^isub>i) \ D R D'"}, + which can be unfolded to the series of premises + % + %\begin{center} + @{text "d\<^isub>1 R\<^isub>1 d\\<^isub>1 \ d\<^isub>q R\<^isub>q d\\<^isub>q"}. + %\end{center} + % + %\noindent + We will use the unfolded version in the examples below. + + Now suppose the binding clause @{text "bc\<^isub>i"} is of the general form + % + \begin{equation}\label{nonempty} + \mbox{\isacommand{bind (set)} @{text "b\<^isub>1\b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\d\<^isub>q"}.} + \end{equation} + + \noindent + 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 + 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}). + For $\approx_{\,\textit{set}}$ we also need + a compound free-atom function for the bodies defined as + % + \begin{center} + \mbox{@{text "fa \ (fa_ty\<^isub>1,\, fa_ty\<^isub>q)"}} + \end{center} + + \noindent + with the assumption that the @{text "d"}$_{1..q}$ refer to arguments of types @{text "ty"}$_{1..q}$. + The last ingredient we need are the sets of atoms bound in the bodies. + For this we take + + \begin{center} + @{text "B \ bn_ty\<^isub>1 b\<^isub>1 \ \ \ bn_ty\<^isub>p b\<^isub>p"}\;.\\ + \end{center} + + \noindent + Similarly for @{text "B'"} using the labels @{text "b\"}$_{1..p}$. This + lets us formally define the premise @{text P} for a non-empty binding clause as: + % + \begin{center} + \mbox{@{term "P \ \p. (B, D) \set R fa p (B', D')"}}\;. + \end{center} + + \noindent + 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 + 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 + 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 + % + %\begin{center} + @{text "bn\<^isub>1 l\<^isub>1, \, bn\<^isub>r l\<^isub>r"}. + %\end{center} + % + %\noindent + The tuple @{text L} is then @{text "(l\<^isub>1,\,l\<^isub>r)"} (similarly @{text "L'"}) + and the compound equivalence relation @{text "R'"} is @{text "(\bn\<^isub>1,\,\bn\<^isub>r)"}. + All premises for @{text "bc\<^isub>i"} are then given by + % + \begin{center} + @{text "prems(bc\<^isub>i) \ P \ L R' L'"} + \end{center} + + \noindent + 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} + @{text "bn (C z\<^isub>1 \ z\<^isub>s) = rhs"} + %\end{center} + % + %\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 + % + \begin{center} + \mbox{\infer{@{text "C z\<^isub>1 \ z\<^isub>s \bn C z\\<^isub>1 \ z\\<^isub>s"}} + {@{text "z\<^isub>1 R\<^isub>1 z\\<^isub>1 \ z\<^isub>s R\<^isub>s z\\<^isub>s"}}} + \end{center} + + \noindent + In this clause the relations @{text "R"}$_{1..s}$ are given by + + \begin{center} + \begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}} + $\bullet$ & @{text "z\<^isub>i \ty z\\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text rhs} and + is a recursive argument of @{text C},\\ + $\bullet$ & @{text "z\<^isub>i = z\\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text rhs} + and is a non-recursive argument of @{text C},\\ + $\bullet$ & @{text "z\<^isub>i \bn\<^isub>i z\\<^isub>i"} provided @{text "z\<^isub>i"} occurs in @{text rhs} + with the recursive call @{text "bn\<^isub>i x\<^isub>i"} and\\ + $\bullet$ & @{text True} provided @{text "z\<^isub>i"} occurs in @{text rhs} but without a + recursive call. + \end{tabular} + \end{center} + + \noindent + 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). + + Again let us take a look at a concrete example for these definitions. For \eqref{letrecs} + we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and + $\approx_{\textit{bn}}$ with the following clauses: + + \begin{center}\small + \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\\ + \makebox[0mm]{\infer{@{text "Let_rec as t \\<^bsub>trm\<^esub> Let_rec as' t'"}} + {@{term "\p. (bn as, ast) \lst alpha_trm2 fa_trm2 p (bn as', ast')"}}} + \end{tabular} + \end{center} + + \begin{center}\small + \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"}} + {@{text "a = a'"} & @{text "t \\<^bsub>trm\<^esub> t'"} & @{text "as \\<^bsub>assn\<^esub> as'"}} + \end{tabular} + \end{center} + + \begin{center}\small + \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"}} + {@{text "t \\<^bsub>trm\<^esub> t'"} & @{text "as \\<^bsub>bn\<^esub> as'"}} + \end{tabular} + \end{center} + + \noindent + Note the difference between $\approx_{\textit{assn}}$ and + $\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). + %The underlying reason is that the terms inside an assignment are not meant + %to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"}, + %because there all components of an assignment are ``under'' the binder. +*} + +section {* Establishing the Reasoning Infrastructure *} + +text {* + Having made all necessary definitions for raw terms, we can start + 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 + equivalence relations. + + \begin{lemma}\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} + + \begin{proof} + The proof is by mutual induction over the definitions. The non-trivial + cases involve premises built up by $\approx_{\textit{set}}$, + $\approx_{\textit{set+}}$ and $\approx_{\textit{list}}$. They + can be dealt with as in Lemma~\ref{alphaeq}. + \end{proof} + + \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}$. + 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 + "fa_ty"}$^\alpha_{1..n}$ and @{text "fa_bn"}$^\alpha_{1..m}$ as well as the binding functions @{text + "bn"}$^\alpha_{1..m}$. However, these definitions are not really useful to the + user, since they are given in terms of the isomorphisms we obtained by + creating new types in Isabelle/HOL (recall the picture shown in the + Introduction). + + The first useful property for the user is the fact that distinct + term-constructors are not + equal, that is + % + \begin{equation}\label{distinctalpha} + \mbox{@{text "C"}$^\alpha$~@{text "x\<^isub>1 \ x\<^isub>r"}~@{text "\"}~% + @{text "D"}$^\alpha$~@{text "y\<^isub>1 \ y\<^isub>s"}} + \end{equation} + + \noindent + whenever @{text "C"}$^\alpha$~@{text "\"}~@{text "D"}$^\alpha$. + In order to derive this fact, we use the definition of $\alpha$-equivalence + and establish that + % + \begin{equation}\label{distinctraw} + \mbox{@{text "C x\<^isub>1 \ x\<^isub>r"}\;$\not\approx$@{text ty}\;@{text "D y\<^isub>1 \ y\<^isub>s"}} + \end{equation} + + \noindent + 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}). + Assuming, for example, @{text "C"} is of type @{text "ty"} with argument types + @{text "ty"}$_{1..r}$, respectfulness amounts to showing that + % + \begin{center} + @{text "C x\<^isub>1 \ x\<^isub>r \ty C x\\<^isub>1 \ x\\<^isub>r"} + \end{center} + + \noindent + holds under the assumptions that we have \mbox{@{text + "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 + definition and by establishing the following auxiliary implications %facts + % + \begin{equation}\label{fnresp} + \mbox{% + \begin{tabular}{ll@ {\hspace{7mm}}ll} + \mbox{\it (i)} & @{text "x \ty\<^isub>i x\"}~~@{text "\"}~~@{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x\"} & + \mbox{\it (iii)} & @{text "x \ty\<^isub>j x\"}~~@{text "\"}~~@{text "bn\<^isub>j x = bn\<^isub>j x\"}\\ + + \mbox{\it (ii)} & @{text "x \ty\<^isub>j x\"}~~@{text "\"}~~@{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x\"} & + \mbox{\it (iv)} & @{text "x \ty\<^isub>j x\"}~~@{text "\"}~~@{text "x \bn\<^isub>j x\"}\\ + \end{tabular}} + \end{equation} + + \noindent + They can be established by induction on @{text "\ty"}$_{1..n}$. Whereas the first, + second and last implication are true by how we stated our definitions, the + third \emph{only} holds because of our restriction + imposed on the form of the binding functions---namely \emph{not} returning + 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 lifing of the corresponding binding functions in Ott to $\alpha$-equated + terms is impossible. + + Having established respectfulness for the raw term-constructors, the + quotient package is able to automatically deduce \eqref{distinctalpha} from + \eqref{distinctraw}. Having the facts \eqref{fnresp} at our disposal, we can + also lift properties that characterise when two raw terms of the form + % + \begin{center} + @{text "C x\<^isub>1 \ x\<^isub>r \ty C x\\<^isub>1 \ x\\<^isub>r"} + \end{center} + + \noindent + 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"}. + %\end{center} + % + %\noindent + We call these conditions as \emph{quasi-injectivity}. They correspond to + 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}. + %, which we already established + %in Lemma~\ref{equiv}. + As a result we can add the equations + % + \begin{equation}\label{calphaeqvt} + @{text "p \ (C\<^sup>\ x\<^isub>1 \ x\<^isub>r) = C\<^sup>\ (p \ x\<^isub>1) \ (p \ x\<^isub>r)"} + \end{equation} + + \noindent + to our infrastructure. In a similar fashion we can lift the defining equations + of the free-atom functions @{text "fn_ty\"}$_{1..n}$ and + @{text "fa_bn\"}$_{1..m}$ as well as of the binding functions @{text + "bn\"}$_{1..m}$ and the size functions @{text "size_ty\"}$_{1..n}$. + The latter are defined automatically for the raw types @{text "ty"}$_{1..n}$ + by the datatype package of Isabelle/HOL. + + Finally we can add to our infrastructure a cases lemma (explained in the next section) + and a structural induction principle + for the types @{text "ty\"}$_{1..n}$. The conclusion of the induction principle is + of the form + % + %\begin{equation}\label{weakinduct} + \mbox{@{text "P\<^isub>1 x\<^isub>1 \ \ \ P\<^isub>n x\<^isub>n "}} + %\end{equation} + % + %\noindent + whereby the @{text P}$_{1..n}$ are predicates and the @{text x}$_{1..n}$ + have types @{text "ty\"}$_{1..n}$. This induction principle has for each + term constructor @{text "C"}$^\alpha$ a premise of the form + % + \begin{equation}\label{weakprem} + \mbox{@{text "\x\<^isub>1\x\<^isub>r. P\<^isub>i x\<^isub>i \ \ \ P\<^isub>j x\<^isub>j \ P (C\<^sup>\ x\<^isub>1 \ x\<^isub>r)"}} + \end{equation} + + \noindent + 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 + can first show that the free-atom functions and binding functions are + equivariant, namely + % + \begin{center} + \begin{tabular}{rcl@ {\hspace{10mm}}rcl} + @{text "p \ (fa_ty\\<^isub>i x)"} & $=$ & @{text "fa_ty\\<^isub>i (p \ x)"} & + @{text "p \ (bn\\<^isub>j x)"} & $=$ & @{text "bn\\<^isub>j (p \ x)"}\\ + @{text "p \ (fa_bn\\<^isub>j x)"} & $=$ & @{text "fa_bn\\<^isub>j (p \ x)"}\\ + \end{tabular} + \end{center} + % + \noindent + These properties can be established using the induction principle for the types @{text "ty\"}$_{1..n}$. + %%in \eqref{weakinduct}. + Having these equivariant properties established, we can + show that the support of term-constructors @{text "C\<^sup>\"} is included in + the support of its arguments, that means + + \begin{center} + @{text "supp (C\<^sup>\ x\<^isub>1 \ x\<^isub>r) \ (supp x\<^isub>1 \ \ \ supp x\<^isub>r)"} + \end{center} + + \noindent + holds. This allows us to prove by induction that + every @{text x} of type @{text "ty\"}$_{1..n}$ is finitely supported. + %This can be again shown by induction + %over @{text "ty\"}$_{1..n}$. + 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. + + \begin{theorem} + 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} + + \begin{proof} + The proof is by induction. In each case + we unfold the definition of @{text "supp"}, move the swapping inside the + term-constructors and then use the quasi-injectivity lemmas in order to complete the + proof. For the abstraction cases we use the facts derived in Theorem~\ref{suppabs}. + \end{proof} + + \noindent + To sum up this section, we can establish automatically a reasoning infrastructure + for the types @{text "ty\"}$_{1..n}$ + by first lifting definitions from the raw level to the quotient level and + then by establishing facts about these lifted definitions. All necessary proofs + are generated automatically by custom ML-code. + + %This code can deal with + %specifications such as the one shown in Figure~\ref{nominalcorehas} for Core-Haskell. + + %\begin{figure}[t!] + %\begin{boxedminipage}{\linewidth} + %\small + %\begin{tabular}{l} + %\isacommand{atom\_decl}~@{text "var cvar tvar"}\\[1mm] + %\isacommand{nominal\_datatype}~@{text "tkind ="}\\ + %\phantom{$|$}~@{text "KStar"}~$|$~@{text "KFun tkind tkind"}\\ + %\isacommand{and}~@{text "ckind ="}\\ + %\phantom{$|$}~@{text "CKSim ty ty"}\\ + %\isacommand{and}~@{text "ty ="}\\ + %\phantom{$|$}~@{text "TVar tvar"}~$|$~@{text "T string"}~$|$~@{text "TApp ty ty"}\\ + %$|$~@{text "TFun string ty_list"}~% + %$|$~@{text "TAll tv::tvar tkind ty::ty"} \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text ty}\\ + %$|$~@{text "TArr ckind ty"}\\ + %\isacommand{and}~@{text "ty_lst ="}\\ + %\phantom{$|$}~@{text "TNil"}~$|$~@{text "TCons ty ty_lst"}\\ + %\isacommand{and}~@{text "cty ="}\\ + %\phantom{$|$}~@{text "CVar cvar"}~% + %$|$~@{text "C string"}~$|$~@{text "CApp cty cty"}~$|$~@{text "CFun string co_lst"}\\ + %$|$~@{text "CAll cv::cvar ckind cty::cty"} \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text cty}\\ + %$|$~@{text "CArr ckind cty"}~$|$~@{text "CRefl ty"}~$|$~@{text "CSym cty"}~$|$~@{text "CCirc cty cty"}\\ + %$|$~@{text "CAt cty ty"}~$|$~@{text "CLeft cty"}~$|$~@{text "CRight cty"}~$|$~@{text "CSim cty cty"}\\ + %$|$~@{text "CRightc cty"}~$|$~@{text "CLeftc cty"}~$|$~@{text "Coerce cty cty"}\\ + %\isacommand{and}~@{text "co_lst ="}\\ + %\phantom{$|$}@{text "CNil"}~$|$~@{text "CCons cty co_lst"}\\ + %\isacommand{and}~@{text "trm ="}\\ + %\phantom{$|$}~@{text "Var var"}~$|$~@{text "K string"}\\ + %$|$~@{text "LAM_ty tv::tvar tkind t::trm"} \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text t}\\ + %$|$~@{text "LAM_cty cv::cvar ckind t::trm"} \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text t}\\ + %$|$~@{text "App_ty trm ty"}~$|$~@{text "App_cty trm cty"}~$|$~@{text "App trm trm"}\\ + %$|$~@{text "Lam v::var ty t::trm"} \isacommand{bind}~@{text "v"}~\isacommand{in}~@{text t}\\ + %$|$~@{text "Let x::var ty trm t::trm"} \isacommand{bind}~@{text x}~\isacommand{in}~@{text t}\\ + %$|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\ + %\isacommand{and}~@{text "assoc_lst ="}\\ + %\phantom{$|$}~@{text ANil}~% + %$|$~@{text "ACons p::pat t::trm assoc_lst"} \isacommand{bind}~@{text "bv p"}~\isacommand{in}~@{text t}\\ + %\isacommand{and}~@{text "pat ="}\\ + %\phantom{$|$}~@{text "Kpat string tvtk_lst tvck_lst vt_lst"}\\ + %\isacommand{and}~@{text "vt_lst ="}\\ + %\phantom{$|$}~@{text VTNil}~$|$~@{text "VTCons var ty vt_lst"}\\ + %\isacommand{and}~@{text "tvtk_lst ="}\\ + %\phantom{$|$}~@{text TVTKNil}~$|$~@{text "TVTKCons tvar tkind tvtk_lst"}\\ + %\isacommand{and}~@{text "tvck_lst ="}\\ + %\phantom{$|$}~@{text TVCKNil}~$|$ @{text "TVCKCons cvar ckind tvck_lst"}\\ + %\isacommand{binder}\\ + %@{text "bv :: pat \ atom list"}~\isacommand{and}~% + %@{text "bv1 :: vt_lst \ atom list"}~\isacommand{and}\\ + %@{text "bv2 :: tvtk_lst \ atom list"}~\isacommand{and}~% + %@{text "bv3 :: tvck_lst \ atom list"}\\ + %\isacommand{where}\\ + %\phantom{$|$}~@{text "bv (K s tvts tvcs vs) = (bv3 tvts) @ (bv2 tvcs) @ (bv1 vs)"}\\ + %$|$~@{text "bv1 VTNil = []"}\\ + %$|$~@{text "bv1 (VTCons x ty tl) = (atom x)::(bv1 tl)"}\\ + %$|$~@{text "bv2 TVTKNil = []"}\\ + %$|$~@{text "bv2 (TVTKCons a ty tl) = (atom a)::(bv2 tl)"}\\ + %$|$~@{text "bv3 TVCKNil = []"}\\ + %$|$~@{text "bv3 (TVCKCons c cty tl) = (atom c)::(bv3 tl)"}\\ + %\end{tabular} + %\end{boxedminipage} + %\caption{The nominal datatype declaration for Core-Haskell. For 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 in Nominal Isabelle, + %one obtains automatically a reasoning infrastructure for Core-Haskell. + %\label{nominalcorehas}} + %\end{figure} +*} + + +section {* Strong Induction Principles *} + +text {* + 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}. + 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 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 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 + running example the term-constructors @{text "Lam"} and @{text "Let"} + from example \eqref{letpat}. Instead of establishing @{text " P\<^bsub>trm\<^esub> t \ P\<^bsub>pat\<^esub> p"}, + the stronger induction principle for \eqref{letpat} establishes properties @{text " P\<^bsub>trm\<^esub> c t \ P\<^bsub>pat\<^esub> c p"} + where the additional parameter @{text c} controls + which freshness assumptions the binders should satisfy. For the two term constructors + this means that the user has to establish in inductions the implications + % + \begin{center} + \begin{tabular}{l} + @{text "\a t c. {atom a} \\<^sup>* c \ (\d. P\<^bsub>trm\<^esub> d t) \ P\<^bsub>trm\<^esub> c (Lam a t)"}\\ + @{text "\p t c. (set (bn p)) \\<^sup>* c \ (\d. P\<^bsub>pat\<^esub> d p) \ (\d. P\<^bsub>trm\<^esub> d t) \ \ P\<^bsub>trm\<^esub> c (Let p t)"}\\%[-0mm] + \end{tabular} + \end{center} + + In \cite{UrbanTasson05} we showed how the weaker induction principles imply + the stronger ones. This was done by some quite complicated, nevertheless automated, + 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 + two proof obligations: one is that we have + well-founded measures (for each type @{text "ty"}$^\alpha_{1..n}$) that decrease in + 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. + + What is left to show is that we covered all cases. To do so, we use + a \emph{cases lemma} derived for each type. For the terms in \eqref{letpat} + this lemma is of the form + % + \begin{equation}\label{weakcases} + \infer{@{text "P\<^bsub>trm\<^esub>"}} + {\begin{array}{l@ {\hspace{9mm}}l} + @{text "\x. t = Var x \ P\<^bsub>trm\<^esub>"} & @{text "\a t'. t = Lam a t' \ P\<^bsub>trm\<^esub>"}\\ + @{text "\t\<^isub>1 t\<^isub>2. t = App t\<^isub>1 t\<^isub>2 \ P\<^bsub>trm\<^esub>"} & @{text "\p t'. t = Let p t' \ P\<^bsub>trm\<^esub>"}\\ + \end{array}}\\[-1mm] + \end{equation} + % + where we have a premise for each term-constructor. + The idea behind such cases lemmas is that we can conclude with a property @{text "P\<^bsub>trm\<^esub>"}, + provided we can show that this property holds if we substitute for @{text "t"} all + possible term-constructors. + + The only remaining difficulty is that in order to derive the stronger induction + principles conveniently, the cases lemma in \eqref{weakcases} is too weak. For this note that + in order to apply this lemma, we have to establish @{text "P\<^bsub>trm\<^esub>"} for \emph{all} @{text Lam}- and + \emph{all} @{text Let}-terms. + What we need instead is a cases lemma where we only have to consider terms that have + binders that are fresh w.r.t.~a context @{text "c"}. This gives the implications + % + \begin{center} + \begin{tabular}{l} + @{text "\a t'. t = Lam a t' \ {atom a} \\<^sup>* c \ P\<^bsub>trm\<^esub>"}\\ + @{text "\p t'. t = Let p t' \ (set (bn p)) \\<^sup>* c \ P\<^bsub>trm\<^esub>"}\\%[-2mm] + \end{tabular} + \end{center} + % + \noindent + which however can be relatively easily be derived from the implications in \eqref{weakcases} + by a renaming using Properties \ref{supppermeq} and \ref{avoiding}. In the first case we know + that @{text "{atom a} \\<^sup>* Lam a t"}. Property \eqref{avoiding} provides us therefore with + a permutation @{text q}, such that @{text "{atom (q \ a)} \\<^sup>* c"} and + @{text "supp (Lam a t) \\<^sup>* q"} hold. + By using Property \ref{supppermeq}, we can infer from the latter + that @{text "Lam (q \ a) (q \ t) = Lam a t"} + and we are done with this case. + + The @{text Let}-case involving a (non-recursive) deep binder is a bit more complicated. + The reason is that the we cannot apply Property \ref{avoiding} to the whole term @{text "Let p t"}, + because @{text p} might contain names that are bound (by @{text bn}) and so are + free. To solve this problem we have to introduce a permutation function that only + permutes names bound by @{text bn} and leaves the other names unchanged. We do this again + by lifting. For a + 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 + $\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"}}\\ + \text{@{text "y\<^isub>i \ p \ x\<^isub>i"} otherwise} + \end{cases}$ + \end{center} + % + %\noindent + %with @{text "y\<^isub>i"} determined as follows: + % + %\begin{center} + %\begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}} + %$\bullet$ & @{text "y\<^isub>i \ x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\ + %$\bullet$ & @{text "y\<^isub>i \ p \\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\ + %$\bullet$ & @{text "y\<^isub>i \ p \ x\<^isub>i"} otherwise + %\end{tabular} + %\end{center} + % + \noindent + Now Properties \ref{supppermeq} and \ref{avoiding} give us a permutation @{text q} such that + @{text "(set (bn (q \\<^bsub>bn\<^esub> p)) \\<^sup>* c"} holds and such that @{text "[q \\<^bsub>bn\<^esub> p]\<^bsub>list\<^esub>.(q \ t)"} + is equal to @{text "[p]\<^bsub>list\<^esub>. t"}. We can also show that @{text "(q \\<^bsub>bn\<^esub> p) \\<^bsub>bn\<^esub> p"}. + These facts establish that @{text "Let (q \\<^bsub>bn\<^esub> p) (p \ t) = Let p t"}, as we need. This + completes the non-trivial cases in \eqref{letpat} for strengthening the corresponding induction + principle. + + + + %A natural question is + %whether we can also strengthen the weak induction principles involving + %the general binders presented here. We will indeed be able to so, but for this we need an + %additional notion for permuting deep binders. + + %Given a binding function @{text "bn"} we define an auxiliary permutation + %operation @{text "_ \\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder. + %Assuming a clause of @{text bn} is given as + % + %\begin{center} + %@{text "bn (C x\<^isub>1 \ x\<^isub>r) = rhs"}, + %\end{center} + + %\noindent + %then we define + % + %\begin{center} + %@{text "p \\<^bsub>bn\<^esub> (C x\<^isub>1 \ x\<^isub>r) \ C y\<^isub>1 \ y\<^isub>r"} + %\end{center} + + %\noindent + %with @{text "y\<^isub>i"} determined as follows: + % + %\begin{center} + %\begin{tabular}{c@ {\hspace{2mm}}p{7cm}} + %$\bullet$ & @{text "y\<^isub>i \ x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\ + %$\bullet$ & @{text "y\<^isub>i \ p \\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\ + %$\bullet$ & @{text "y\<^isub>i \ p \ x\<^isub>i"} otherwise + %\end{tabular} + %\end{center} + + %\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 + + %\begin{lemma}\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} + + %\begin{proof} + %By induction on @{text x}. The equations follow by simple unfolding + %of the definitions. + %\end{proof} + + %\noindent + %The first property states that a permutation applied to a binding function is + %equivalent to first permuting the binders and then calculating the bound + %atoms. The second amounts to the fact that permuting the binders has no + %effect on the free-atom function. The main point of this permutation + %function, however, is that if we have a permutation that is fresh + %for the support of an object @{text x}, then we can use this permutation + %to rename the binders in @{text x}, without ``changing'' @{text x}. In case of the + %@{text "Let"} term-constructor from the example shown + %in \eqref{letpat} this means for a permutation @{text "r"} + %% + %\begin{equation}\label{renaming} + %\begin{array}{l} + %\mbox{if @{term "supp (Abs_lst (bn p) t\<^isub>2) \* r"}}\\ + %\qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \\\<^bsub>bn_pat\<^esub> p) t\<^isub>1 (r \ t\<^isub>2)"}} + %\end{array} + %\end{equation} + + %\noindent + %This fact will be crucial when establishing the strong induction principles below. + + + %In our running example about @{text "Let"}, the strong induction + %principle means that instead + %of establishing the implication + % + %\begin{center} + %@{text "\p t\<^isub>1 t\<^isub>2. P\<^bsub>pat\<^esub> p \ P\<^bsub>trm\<^esub> t\<^isub>1 \ P\<^bsub>trm\<^esub> t\<^isub>2 \ P\<^bsub>trm\<^esub> (Let p t\<^isub>1 t\<^isub>2)"} + %\end{center} + % + %\noindent + %it is sufficient to establish the following implication + % + %\begin{equation}\label{strong} + %\mbox{\begin{tabular}{l} + %@{text "\p t\<^isub>1 t\<^isub>2 c."}\\ + %\hspace{5mm}@{text "set (bn p) #\<^sup>* c \"}\\ + %\hspace{5mm}@{text "(\d. P\<^bsub>pat\<^esub> d p) \ (\d. P\<^bsub>trm\<^esub> d t\<^isub>1) \ (\d. P\<^bsub>trm\<^esub> d t\<^isub>2)"}\\ + %\hspace{15mm}@{text "\ P\<^bsub>trm\<^esub> c (Let p t\<^isub>1 t\<^isub>2)"} + %\end{tabular}} + %\end{equation} + % + %\noindent + %While this implication contains an additional argument, namely @{text c}, and + %also additional universal quantifications, it is usually easier to establish. + %The reason is that we have the freshness + %assumption @{text "set (bn\<^sup>\ p) #\<^sup>* c"}, whereby @{text c} can be arbitrarily + %chosen by the user as long as it has finite support. + % + %Let us now show how we derive the strong induction principles from the + %weak ones. In case of the @{text "Let"}-example we derive by the weak + %induction the following two properties + % + %\begin{equation}\label{hyps} + %@{text "\q c. P\<^bsub>trm\<^esub> c (q \ t)"} \hspace{4mm} + %@{text "\q\<^isub>1 q\<^isub>2 c. P\<^bsub>pat\<^esub> (q\<^isub>1 \\\<^bsub>bn\<^esub> (q\<^isub>2 \ p))"} + %\end{equation} + % + %\noindent + %For the @{text Let} term-constructor we therefore have to establish @{text "P\<^bsub>trm\<^esub> c (q \ Let p t\<^isub>1 t\<^isub>2)"} + %assuming \eqref{hyps} as induction hypotheses (the first for @{text t\<^isub>1} and @{text t\<^isub>2}). + %By Property~\ref{avoiding} we + %obtain a permutation @{text "r"} such that + % + %\begin{equation}\label{rprops} + %@{term "(r \ set (bn (q \ p))) \* c "}\hspace{4mm} + %@{term "supp (Abs_lst (bn (q \ p)) (q \ t\<^isub>2)) \* r"} + %\end{equation} + % + %\noindent + %hold. The latter fact and \eqref{renaming} give us + %% + %\begin{center} + %\begin{tabular}{l} + %@{text "Let (q \ p) (q \ t\<^isub>1) (q \ t\<^isub>2) ="} \\ + %\hspace{15mm}@{text "Let (r \\\<^bsub>bn\<^esub> (q \ p)) (q \ t\<^isub>1) (r \ (q \ t\<^isub>2))"} + %\end{tabular} + %\end{center} + % + %\noindent + %So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \ Let p t\<^isub>1 t\<^isub>2)"}, we can equally + %establish @{text "P\<^bsub>trm\<^esub> c (Let (r \\\<^bsub>bn\<^esub> (q \ p)) (q \ t\<^isub>1) (r \ (q \ t\<^isub>2)))"}. + %To do so, we will use the implication \eqref{strong} of the strong induction + %principle, which requires us to discharge + %the following four proof obligations: + %% + %\begin{center} + %\begin{tabular}{rl} + %{\it (i)} & @{text "set (bn (r \\\<^bsub>bn\<^esub> (q \ p))) #\<^sup>* c"}\\ + %{\it (ii)} & @{text "\d. P\<^bsub>pat\<^esub> d (r \\\<^bsub>bn\<^esub> (q \ p))"}\\ + %{\it (iii)} & @{text "\d. P\<^bsub>trm\<^esub> d (q \ t\<^isub>1)"}\\ + %{\it (iv)} & @{text "\d. P\<^bsub>trm\<^esub> d (r \ (q \ t\<^isub>2))"}\\ + %\end{tabular} + %\end{center} + % + %\noindent + %The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it (i)}; the + %others from the induction hypotheses in \eqref{hyps} (in the fourth case + %we have to use the fact that @{term "(r \ (q \ t\<^isub>2)) = (r + q) \ t\<^isub>2"}). + % + %Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps}, + %we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}. + %This completes the proof showing that the weak induction principles imply + %the strong induction principles. +*} + + +section {* Related Work\label{related} *} + +text {* + To our knowledge the earliest usage of general binders in a theorem prover + is described in \cite{NaraschewskiNipkow99} about a formalisation of the + algorithm W. This formalisation implements binding in type-schemes using a + de-Bruijn indices representation. Since type-schemes in W contain only a single + place where variables are bound, different indices do not refer to different binders (as in the usual + de-Bruijn representation), but to different bound variables. A similar idea + has been recently explored for general binders in the locally nameless + approach to binding \cite{chargueraud09}. There, de-Bruijn indices consist + of two numbers, one referring to the place where a variable is bound, and the + other to which variable is bound. The reasoning infrastructure for both + representations of bindings comes for free in theorem provers like Isabelle/HOL or + Coq, since the corresponding term-calculi can be implemented as ``normal'' + datatypes. However, in both approaches it seems difficult to achieve our + fine-grained control over the ``semantics'' of bindings (i.e.~whether the + order of binders should matter, or vacuous binders should be taken into + account). %To do so, one would require additional predicates that filter out + %unwanted terms. Our guess is that such predicates result in rather + %intricate formal reasoning. + + Another technique for representing binding is higher-order abstract syntax + (HOAS). %, which for example is implemented in the Twelf system. + This %%representation + technique supports very elegantly many aspects of \emph{single} binding, and + impressive work has been done that uses HOAS for mechanising the metatheory + of SML~\cite{LeeCraryHarper07}. We are, however, not aware how multiple + binders of SML are represented in this work. Judging from the submitted + Twelf-solution for the POPLmark challenge, HOAS cannot easily deal with + binding constructs where the number of bound variables is not fixed. %For example + In the second part of this challenge, @{text "Let"}s involve + patterns that bind multiple variables at once. In such situations, HOAS + seems to have to resort to the iterated-single-binders-approach with + all the unwanted consequences when reasoning about the resulting terms. + + %Two formalisations involving general binders have been + %performed in older + %versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W + %\cite{BengtsonParow09,UrbanNipkow09}). Both + %use the approach based on iterated single binders. Our experience with + %the latter formalisation has been disappointing. The major pain arose from + %the need to ``unbind'' variables. This can be done in one step with our + %general binders described in this paper, but needs a cumbersome + %iteration with single binders. The resulting formal reasoning turned out to + %be rather unpleasant. The hope is that the extension presented in this paper + %is a substantial improvement. + + The most closely related work to the one presented here is the Ott-tool + \cite{ott-jfp} and the C$\alpha$ml language \cite{Pottier06}. Ott is a nifty + front-end for creating \LaTeX{} documents from specifications of + term-calculi involving general binders. For a subset of the specifications + 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 + 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 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 + 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 + 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 + \isacommand{bind (set+)}. + % + %Consider the examples + % + %\begin{center} + %\begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}} + %@{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} & + % \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t s"}\\ + %@{text "Foo\<^isub>2 xs::name fset t::trm s::trm"} & + % \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t"}, + % \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "s"}\\ + %\end{tabular} + %\end{center} + % + %\noindent + %In the first term-constructor we have a single + %body that happens to be ``spread'' over two arguments; in the second term-constructor we have + %two independent bodies in which the same variables are bound. As a result we + %have + % + %\begin{center} + %\begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l} + %@{text "Foo\<^isub>1 {a, b} (a, b) (a, b)"} & $\not=$ & + %@{text "Foo\<^isub>1 {a, b} (a, b) (b, a)"}\\ + %@{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ & + %@{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\ + %\end{tabular} + %\end{center} + % + %\noindent + %and therefore need the extra generality to be able to distinguish between + %both specifications. + Because of how we set up our definitions, we also had to impose some restrictions + (like a single binding function for a deep binder) that are not present in Ott. + %Our + %expectation is that we can still cover many interesting term-calculi from + %programming language research, for example Core-Haskell. + + Pottier presents in \cite{Pottier06} a language, called C$\alpha$ml, for + representing terms with general binders inside OCaml. This language is + implemented as a front-end that can be translated to OCaml with the help of + a library. He presents a type-system in which the scope of general binders + can be specified using special markers, written @{text "inner"} and + @{text "outer"}. It seems our and his specifications can be + 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). + 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. + Similar work for Haskell with similar results was reported by Cheney \cite{Cheney05a}. + + 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+)}. + 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] +*} + +section {* Conclusion *} + +text {* + 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. + 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. + 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 + 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}.} + + 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 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 them we can + provide more automation). + + %There are some restrictions we imposed in this paper that we would like to lift in + %future work. One is the exclusion of nested datatype definitions. Nested + %datatype definitions allow one to specify, for instance, the function kinds + %in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded + %version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). To + %achieve this, we need a slightly more clever implementation than we have at the moment. + + %A more interesting line of investigation is whether we can go beyond the + %simple-minded form of binding functions that we adopted from Ott. At the moment, binding + %functions can only return the empty set, a singleton atom set or unions + %of atom sets (similarly for lists). It remains to be seen whether + %properties like + %% + %\begin{center} + %@{text "fa_ty x = bn x \ fa_bn x"}. + %\end{center} + % + %\noindent + %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. + % + \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] +*} + + +(*<*) +end +(*>*) diff -r a5da7b6aff8f -r 6f38e357b337 ESOP-Paper/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ESOP-Paper/ROOT.ML Tue Mar 29 23:52:14 2011 +0200 @@ -0,0 +1,4 @@ +quick_and_dirty := true; +no_document use_thys ["~~/src/HOL/Library/LaTeXsugar", + "../Nominal/Nominal2"]; +use_thys ["Paper"]; \ No newline at end of file diff -r a5da7b6aff8f -r 6f38e357b337 ESOP-Paper/ROOTa.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ESOP-Paper/ROOTa.ML Tue Mar 29 23:52:14 2011 +0200 @@ -0,0 +1,4 @@ +quick_and_dirty := true; +no_document use_thys ["~~/src/HOL/Library/LaTeXsugar", + "../Nominal/Nominal2"]; +use_thys ["Appendix"]; \ No newline at end of file diff -r a5da7b6aff8f -r 6f38e357b337 ESOP-Paper/document/llncs.cls --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ESOP-Paper/document/llncs.cls Tue Mar 29 23:52:14 2011 +0200 @@ -0,0 +1,1207 @@ +% LLNCS DOCUMENT CLASS -- version 2.17 (12-Jul-2010) +% Springer Verlag LaTeX2e support for Lecture Notes in Computer Science +% +%% +%% \CharacterTable +%% {Upper-case \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z +%% Lower-case \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z +%% Digits \0\1\2\3\4\5\6\7\8\9 +%% Exclamation \! Double quote \" Hash (number) \# +%% Dollar \$ Percent \% Ampersand \& +%% Acute accent \' Left paren \( Right paren \) +%% Asterisk \* Plus \+ Comma \, +%% Minus \- Point \. Solidus \/ +%% Colon \: Semicolon \; Less than \< +%% Equals \= Greater than \> Question mark \? +%% Commercial at \@ Left bracket \[ Backslash \\ +%% Right bracket \] Circumflex \^ Underscore \_ +%% Grave accent \` Left brace \{ Vertical bar \| +%% Right brace \} Tilde \~} +%% +\NeedsTeXFormat{LaTeX2e}[1995/12/01] +\ProvidesClass{llncs}[2010/07/12 v2.17 +^^J LaTeX document class for Lecture Notes in Computer Science] +% Options +\let\if@envcntreset\iffalse +\DeclareOption{envcountreset}{\let\if@envcntreset\iftrue} +\DeclareOption{citeauthoryear}{\let\citeauthoryear=Y} +\DeclareOption{oribibl}{\let\oribibl=Y} +\let\if@custvec\iftrue +\DeclareOption{orivec}{\let\if@custvec\iffalse} +\let\if@envcntsame\iffalse +\DeclareOption{envcountsame}{\let\if@envcntsame\iftrue} +\let\if@envcntsect\iffalse +\DeclareOption{envcountsect}{\let\if@envcntsect\iftrue} +\let\if@runhead\iffalse +\DeclareOption{runningheads}{\let\if@runhead\iftrue} + +\let\if@openright\iftrue +\let\if@openbib\iffalse +\DeclareOption{openbib}{\let\if@openbib\iftrue} + +% languages +\let\switcht@@therlang\relax +\def\ds@deutsch{\def\switcht@@therlang{\switcht@deutsch}} +\def\ds@francais{\def\switcht@@therlang{\switcht@francais}} + +\DeclareOption*{\PassOptionsToClass{\CurrentOption}{article}} + +\ProcessOptions + +\LoadClass[twoside]{article} +\RequirePackage{multicol} % needed for the list of participants, index +\RequirePackage{aliascnt} + +\setlength{\textwidth}{12.2cm} +\setlength{\textheight}{19.3cm} +\renewcommand\@pnumwidth{2em} +\renewcommand\@tocrmarg{3.5em} +% +\def\@dottedtocline#1#2#3#4#5{% + \ifnum #1>\c@tocdepth \else + \vskip \z@ \@plus.2\p@ + {\leftskip #2\relax \rightskip \@tocrmarg \advance\rightskip by 0pt plus 2cm + \parfillskip -\rightskip \pretolerance=10000 + \parindent #2\relax\@afterindenttrue + \interlinepenalty\@M + \leavevmode + \@tempdima #3\relax + \advance\leftskip \@tempdima \null\nobreak\hskip -\leftskip + {#4}\nobreak + \leaders\hbox{$\m@th + \mkern \@dotsep mu\hbox{.}\mkern \@dotsep + mu$}\hfill + \nobreak + \hb@xt@\@pnumwidth{\hfil\normalfont \normalcolor #5}% + \par}% + \fi} +% +\def\switcht@albion{% +\def\abstractname{Abstract.} +\def\ackname{Acknowledgement.} +\def\andname{and} +\def\lastandname{\unskip, and} +\def\appendixname{Appendix} +\def\chaptername{Chapter} +\def\claimname{Claim} +\def\conjecturename{Conjecture} +\def\contentsname{Table of Contents} +\def\corollaryname{Corollary} +\def\definitionname{Definition} +\def\examplename{Example} +\def\exercisename{Exercise} +\def\figurename{Fig.} +\def\keywordname{{\bf Keywords:}} +\def\indexname{Index} +\def\lemmaname{Lemma} +\def\contriblistname{List of Contributors} +\def\listfigurename{List of Figures} +\def\listtablename{List of Tables} +\def\mailname{{\it Correspondence to\/}:} +\def\noteaddname{Note added in proof} +\def\notename{Note} +\def\partname{Part} +\def\problemname{Problem} +\def\proofname{Proof} +\def\propertyname{Property} +\def\propositionname{Proposition} +\def\questionname{Question} +\def\remarkname{Remark} +\def\seename{see} +\def\solutionname{Solution} +\def\subclassname{{\it Subject Classifications\/}:} +\def\tablename{Table} +\def\theoremname{Theorem}} +\switcht@albion +% Names of theorem like environments are already defined +% but must be translated if another language is chosen +% +% French section +\def\switcht@francais{%\typeout{On parle francais.}% + \def\abstractname{R\'esum\'e.}% + \def\ackname{Remerciements.}% + \def\andname{et}% + \def\lastandname{ et}% + \def\appendixname{Appendice} + \def\chaptername{Chapitre}% + \def\claimname{Pr\'etention}% + \def\conjecturename{Hypoth\`ese}% + \def\contentsname{Table des mati\`eres}% + \def\corollaryname{Corollaire}% + \def\definitionname{D\'efinition}% + \def\examplename{Exemple}% + \def\exercisename{Exercice}% + \def\figurename{Fig.}% + \def\keywordname{{\bf Mots-cl\'e:}} + \def\indexname{Index} + \def\lemmaname{Lemme}% + \def\contriblistname{Liste des contributeurs} + \def\listfigurename{Liste des figures}% + \def\listtablename{Liste des tables}% + \def\mailname{{\it Correspondence to\/}:} + \def\noteaddname{Note ajout\'ee \`a l'\'epreuve}% + \def\notename{Remarque}% + \def\partname{Partie}% + \def\problemname{Probl\`eme}% + \def\proofname{Preuve}% + \def\propertyname{Caract\'eristique}% +%\def\propositionname{Proposition}% + \def\questionname{Question}% + \def\remarkname{Remarque}% + \def\seename{voir} + \def\solutionname{Solution}% + \def\subclassname{{\it Subject Classifications\/}:} + \def\tablename{Tableau}% + \def\theoremname{Th\'eor\`eme}% +} +% +% German section +\def\switcht@deutsch{%\typeout{Man spricht deutsch.}% + \def\abstractname{Zusammenfassung.}% + \def\ackname{Danksagung.}% + \def\andname{und}% + \def\lastandname{ und}% + \def\appendixname{Anhang}% + \def\chaptername{Kapitel}% + \def\claimname{Behauptung}% + \def\conjecturename{Hypothese}% + \def\contentsname{Inhaltsverzeichnis}% + \def\corollaryname{Korollar}% +%\def\definitionname{Definition}% + \def\examplename{Beispiel}% + \def\exercisename{\"Ubung}% + \def\figurename{Abb.}% + \def\keywordname{{\bf Schl\"usselw\"orter:}} + \def\indexname{Index} +%\def\lemmaname{Lemma}% + \def\contriblistname{Mitarbeiter} + \def\listfigurename{Abbildungsverzeichnis}% + \def\listtablename{Tabellenverzeichnis}% + \def\mailname{{\it Correspondence to\/}:} + \def\noteaddname{Nachtrag}% + \def\notename{Anmerkung}% + \def\partname{Teil}% +%\def\problemname{Problem}% + \def\proofname{Beweis}% + \def\propertyname{Eigenschaft}% +%\def\propositionname{Proposition}% + \def\questionname{Frage}% + \def\remarkname{Anmerkung}% + \def\seename{siehe} + \def\solutionname{L\"osung}% + \def\subclassname{{\it Subject Classifications\/}:} + \def\tablename{Tabelle}% +%\def\theoremname{Theorem}% +} + +% Ragged bottom for the actual page +\def\thisbottomragged{\def\@textbottom{\vskip\z@ plus.0001fil +\global\let\@textbottom\relax}} + +\renewcommand\small{% + \@setfontsize\small\@ixpt{11}% + \abovedisplayskip 8.5\p@ \@plus3\p@ \@minus4\p@ + \abovedisplayshortskip \z@ \@plus2\p@ + \belowdisplayshortskip 4\p@ \@plus2\p@ \@minus2\p@ + \def\@listi{\leftmargin\leftmargini + \parsep 0\p@ \@plus1\p@ \@minus\p@ + \topsep 8\p@ \@plus2\p@ \@minus4\p@ + \itemsep0\p@}% + \belowdisplayskip \abovedisplayskip +} + +\frenchspacing +\widowpenalty=10000 +\clubpenalty=10000 + +\setlength\oddsidemargin {63\p@} +\setlength\evensidemargin {63\p@} +\setlength\marginparwidth {90\p@} + +\setlength\headsep {16\p@} + +\setlength\footnotesep{7.7\p@} +\setlength\textfloatsep{8mm\@plus 2\p@ \@minus 4\p@} +\setlength\intextsep {8mm\@plus 2\p@ \@minus 2\p@} + +\setcounter{secnumdepth}{2} + +\newcounter {chapter} +\renewcommand\thechapter {\@arabic\c@chapter} + +\newif\if@mainmatter \@mainmattertrue +\newcommand\frontmatter{\cleardoublepage + \@mainmatterfalse\pagenumbering{Roman}} +\newcommand\mainmatter{\cleardoublepage + \@mainmattertrue\pagenumbering{arabic}} +\newcommand\backmatter{\if@openright\cleardoublepage\else\clearpage\fi + \@mainmatterfalse} + +\renewcommand\part{\cleardoublepage + \thispagestyle{empty}% + \if@twocolumn + \onecolumn + \@tempswatrue + \else + \@tempswafalse + \fi + \null\vfil + \secdef\@part\@spart} + +\def\@part[#1]#2{% + \ifnum \c@secnumdepth >-2\relax + \refstepcounter{part}% + \addcontentsline{toc}{part}{\thepart\hspace{1em}#1}% + \else + \addcontentsline{toc}{part}{#1}% + \fi + \markboth{}{}% + {\centering + \interlinepenalty \@M + \normalfont + \ifnum \c@secnumdepth >-2\relax + \huge\bfseries \partname~\thepart + \par + \vskip 20\p@ + \fi + \Huge \bfseries #2\par}% + \@endpart} +\def\@spart#1{% + {\centering + \interlinepenalty \@M + \normalfont + \Huge \bfseries #1\par}% + \@endpart} +\def\@endpart{\vfil\newpage + \if@twoside + \null + \thispagestyle{empty}% + \newpage + \fi + \if@tempswa + \twocolumn + \fi} + +\newcommand\chapter{\clearpage + \thispagestyle{empty}% + \global\@topnum\z@ + \@afterindentfalse + \secdef\@chapter\@schapter} +\def\@chapter[#1]#2{\ifnum \c@secnumdepth >\m@ne + \if@mainmatter + \refstepcounter{chapter}% + \typeout{\@chapapp\space\thechapter.}% + \addcontentsline{toc}{chapter}% + {\protect\numberline{\thechapter}#1}% + \else + \addcontentsline{toc}{chapter}{#1}% + \fi + \else + \addcontentsline{toc}{chapter}{#1}% + \fi + \chaptermark{#1}% + \addtocontents{lof}{\protect\addvspace{10\p@}}% + \addtocontents{lot}{\protect\addvspace{10\p@}}% + \if@twocolumn + \@topnewpage[\@makechapterhead{#2}]% + \else + \@makechapterhead{#2}% + \@afterheading + \fi} +\def\@makechapterhead#1{% +% \vspace*{50\p@}% + {\centering + \ifnum \c@secnumdepth >\m@ne + \if@mainmatter + \large\bfseries \@chapapp{} \thechapter + \par\nobreak + \vskip 20\p@ + \fi + \fi + \interlinepenalty\@M + \Large \bfseries #1\par\nobreak + \vskip 40\p@ + }} +\def\@schapter#1{\if@twocolumn + \@topnewpage[\@makeschapterhead{#1}]% + \else + \@makeschapterhead{#1}% + \@afterheading + \fi} +\def\@makeschapterhead#1{% +% \vspace*{50\p@}% + {\centering + \normalfont + \interlinepenalty\@M + \Large \bfseries #1\par\nobreak + \vskip 40\p@ + }} + +\renewcommand\section{\@startsection{section}{1}{\z@}% + {-18\p@ \@plus -4\p@ \@minus -4\p@}% + {12\p@ \@plus 4\p@ \@minus 4\p@}% + {\normalfont\large\bfseries\boldmath + \rightskip=\z@ \@plus 8em\pretolerance=10000 }} +\renewcommand\subsection{\@startsection{subsection}{2}{\z@}% + {-18\p@ \@plus -4\p@ \@minus -4\p@}% + {8\p@ \@plus 4\p@ \@minus 4\p@}% + {\normalfont\normalsize\bfseries\boldmath + \rightskip=\z@ \@plus 8em\pretolerance=10000 }} +\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}% + {-18\p@ \@plus -4\p@ \@minus -4\p@}% + {-0.5em \@plus -0.22em \@minus -0.1em}% + {\normalfont\normalsize\bfseries\boldmath}} +\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}% + {-12\p@ \@plus -4\p@ \@minus -4\p@}% + {-0.5em \@plus -0.22em \@minus -0.1em}% + {\normalfont\normalsize\itshape}} +\renewcommand\subparagraph[1]{\typeout{LLNCS warning: You should not use + \string\subparagraph\space with this class}\vskip0.5cm +You should not use \verb|\subparagraph| with this class.\vskip0.5cm} + +\DeclareMathSymbol{\Gamma}{\mathalpha}{letters}{"00} +\DeclareMathSymbol{\Delta}{\mathalpha}{letters}{"01} +\DeclareMathSymbol{\Theta}{\mathalpha}{letters}{"02} +\DeclareMathSymbol{\Lambda}{\mathalpha}{letters}{"03} +\DeclareMathSymbol{\Xi}{\mathalpha}{letters}{"04} +\DeclareMathSymbol{\Pi}{\mathalpha}{letters}{"05} +\DeclareMathSymbol{\Sigma}{\mathalpha}{letters}{"06} +\DeclareMathSymbol{\Upsilon}{\mathalpha}{letters}{"07} +\DeclareMathSymbol{\Phi}{\mathalpha}{letters}{"08} +\DeclareMathSymbol{\Psi}{\mathalpha}{letters}{"09} +\DeclareMathSymbol{\Omega}{\mathalpha}{letters}{"0A} + +\let\footnotesize\small + +\if@custvec +\def\vec#1{\mathchoice{\mbox{\boldmath$\displaystyle#1$}} +{\mbox{\boldmath$\textstyle#1$}} +{\mbox{\boldmath$\scriptstyle#1$}} +{\mbox{\boldmath$\scriptscriptstyle#1$}}} +\fi + +\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}} +\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil +\penalty50\hskip1em\null\nobreak\hfil\squareforqed +\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi} + +\def\getsto{\mathrel{\mathchoice {\vcenter{\offinterlineskip +\halign{\hfil +$\displaystyle##$\hfil\cr\gets\cr\to\cr}}} +{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr\gets +\cr\to\cr}}} +{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr\gets +\cr\to\cr}}} +{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr +\gets\cr\to\cr}}}}} +\def\lid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil +$\displaystyle##$\hfil\cr<\cr\noalign{\vskip1.2pt}=\cr}}} +{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr<\cr +\noalign{\vskip1.2pt}=\cr}}} +{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr<\cr +\noalign{\vskip1pt}=\cr}}} +{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr +<\cr +\noalign{\vskip0.9pt}=\cr}}}}} +\def\gid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil +$\displaystyle##$\hfil\cr>\cr\noalign{\vskip1.2pt}=\cr}}} +{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr>\cr +\noalign{\vskip1.2pt}=\cr}}} +{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr>\cr +\noalign{\vskip1pt}=\cr}}} +{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr +>\cr +\noalign{\vskip0.9pt}=\cr}}}}} +\def\grole{\mathrel{\mathchoice {\vcenter{\offinterlineskip +\halign{\hfil +$\displaystyle##$\hfil\cr>\cr\noalign{\vskip-1pt}<\cr}}} +{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr +>\cr\noalign{\vskip-1pt}<\cr}}} +{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr +>\cr\noalign{\vskip-0.8pt}<\cr}}} +{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr +>\cr\noalign{\vskip-0.3pt}<\cr}}}}} +\def\bbbr{{\rm I\!R}} %reelle Zahlen +\def\bbbm{{\rm I\!M}} +\def\bbbn{{\rm I\!N}} %natuerliche Zahlen +\def\bbbf{{\rm I\!F}} +\def\bbbh{{\rm I\!H}} +\def\bbbk{{\rm I\!K}} +\def\bbbp{{\rm I\!P}} +\def\bbbone{{\mathchoice {\rm 1\mskip-4mu l} {\rm 1\mskip-4mu l} +{\rm 1\mskip-4.5mu l} {\rm 1\mskip-5mu l}}} +\def\bbbc{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm C$}\hbox{\hbox +to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}} +{\setbox0=\hbox{$\textstyle\rm C$}\hbox{\hbox +to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}} +{\setbox0=\hbox{$\scriptstyle\rm C$}\hbox{\hbox +to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}} +{\setbox0=\hbox{$\scriptscriptstyle\rm C$}\hbox{\hbox +to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}}} +\def\bbbq{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm +Q$}\hbox{\raise +0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}} +{\setbox0=\hbox{$\textstyle\rm Q$}\hbox{\raise +0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}} +{\setbox0=\hbox{$\scriptstyle\rm Q$}\hbox{\raise +0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}} +{\setbox0=\hbox{$\scriptscriptstyle\rm Q$}\hbox{\raise +0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}}} +\def\bbbt{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm +T$}\hbox{\hbox to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}} +{\setbox0=\hbox{$\textstyle\rm T$}\hbox{\hbox +to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}} +{\setbox0=\hbox{$\scriptstyle\rm T$}\hbox{\hbox +to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}} +{\setbox0=\hbox{$\scriptscriptstyle\rm T$}\hbox{\hbox +to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}}} +\def\bbbs{{\mathchoice +{\setbox0=\hbox{$\displaystyle \rm S$}\hbox{\raise0.5\ht0\hbox +to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox +to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}} +{\setbox0=\hbox{$\textstyle \rm S$}\hbox{\raise0.5\ht0\hbox +to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox +to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}} +{\setbox0=\hbox{$\scriptstyle \rm S$}\hbox{\raise0.5\ht0\hbox +to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox +to0pt{\kern0.5\wd0\vrule height0.45\ht0\hss}\box0}} +{\setbox0=\hbox{$\scriptscriptstyle\rm S$}\hbox{\raise0.5\ht0\hbox +to0pt{\kern0.4\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox +to0pt{\kern0.55\wd0\vrule height0.45\ht0\hss}\box0}}}} +\def\bbbz{{\mathchoice {\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}} +{\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}} +{\hbox{$\mathsf\scriptstyle Z\kern-0.3em Z$}} +{\hbox{$\mathsf\scriptscriptstyle Z\kern-0.2em Z$}}}} + +\let\ts\, + +\setlength\leftmargini {17\p@} +\setlength\leftmargin {\leftmargini} +\setlength\leftmarginii {\leftmargini} +\setlength\leftmarginiii {\leftmargini} +\setlength\leftmarginiv {\leftmargini} +\setlength \labelsep {.5em} +\setlength \labelwidth{\leftmargini} +\addtolength\labelwidth{-\labelsep} + +\def\@listI{\leftmargin\leftmargini + \parsep 0\p@ \@plus1\p@ \@minus\p@ + \topsep 8\p@ \@plus2\p@ \@minus4\p@ + \itemsep0\p@} +\let\@listi\@listI +\@listi +\def\@listii {\leftmargin\leftmarginii + \labelwidth\leftmarginii + \advance\labelwidth-\labelsep + \topsep 0\p@ \@plus2\p@ \@minus\p@} +\def\@listiii{\leftmargin\leftmarginiii + \labelwidth\leftmarginiii + \advance\labelwidth-\labelsep + \topsep 0\p@ \@plus\p@\@minus\p@ + \parsep \z@ + \partopsep \p@ \@plus\z@ \@minus\p@} + +\renewcommand\labelitemi{\normalfont\bfseries --} +\renewcommand\labelitemii{$\m@th\bullet$} + +\setlength\arraycolsep{1.4\p@} +\setlength\tabcolsep{1.4\p@} + +\def\tableofcontents{\chapter*{\contentsname\@mkboth{{\contentsname}}% + {{\contentsname}}} + \def\authcount##1{\setcounter{auco}{##1}\setcounter{@auth}{1}} + \def\lastand{\ifnum\value{auco}=2\relax + \unskip{} \andname\ + \else + \unskip \lastandname\ + \fi}% + \def\and{\stepcounter{@auth}\relax + \ifnum\value{@auth}=\value{auco}% + \lastand + \else + \unskip, + \fi}% + \@starttoc{toc}\if@restonecol\twocolumn\fi} + +\def\l@part#1#2{\addpenalty{\@secpenalty}% + \addvspace{2em plus\p@}% % space above part line + \begingroup + \parindent \z@ + \rightskip \z@ plus 5em + \hrule\vskip5pt + \large % same size as for a contribution heading + \bfseries\boldmath % set line in boldface + \leavevmode % TeX command to enter horizontal mode. + #1\par + \vskip5pt + \hrule + \vskip1pt + \nobreak % Never break after part entry + \endgroup} + +\def\@dotsep{2} + +\let\phantomsection=\relax + +\def\hyperhrefextend{\ifx\hyper@anchor\@undefined\else +{}\fi} + +\def\addnumcontentsmark#1#2#3{% +\addtocontents{#1}{\protect\contentsline{#2}{\protect\numberline + {\thechapter}#3}{\thepage}\hyperhrefextend}}% +\def\addcontentsmark#1#2#3{% +\addtocontents{#1}{\protect\contentsline{#2}{#3}{\thepage}\hyperhrefextend}}% +\def\addcontentsmarkwop#1#2#3{% +\addtocontents{#1}{\protect\contentsline{#2}{#3}{0}\hyperhrefextend}}% + +\def\@adcmk[#1]{\ifcase #1 \or +\def\@gtempa{\addnumcontentsmark}% + \or \def\@gtempa{\addcontentsmark}% + \or \def\@gtempa{\addcontentsmarkwop}% + \fi\@gtempa{toc}{chapter}% +} +\def\addtocmark{% +\phantomsection +\@ifnextchar[{\@adcmk}{\@adcmk[3]}% +} + +\def\l@chapter#1#2{\addpenalty{-\@highpenalty} + \vskip 1.0em plus 1pt \@tempdima 1.5em \begingroup + \parindent \z@ \rightskip \@tocrmarg + \advance\rightskip by 0pt plus 2cm + \parfillskip -\rightskip \pretolerance=10000 + \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip + {\large\bfseries\boldmath#1}\ifx0#2\hfil\null + \else + \nobreak + \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern + \@dotsep mu$}\hfill + \nobreak\hbox to\@pnumwidth{\hss #2}% + \fi\par + \penalty\@highpenalty \endgroup} + +\def\l@title#1#2{\addpenalty{-\@highpenalty} + \addvspace{8pt plus 1pt} + \@tempdima \z@ + \begingroup + \parindent \z@ \rightskip \@tocrmarg + \advance\rightskip by 0pt plus 2cm + \parfillskip -\rightskip \pretolerance=10000 + \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip + #1\nobreak + \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern + \@dotsep mu$}\hfill + \nobreak\hbox to\@pnumwidth{\hss #2}\par + \penalty\@highpenalty \endgroup} + +\def\l@author#1#2{\addpenalty{\@highpenalty} + \@tempdima=15\p@ %\z@ + \begingroup + \parindent \z@ \rightskip \@tocrmarg + \advance\rightskip by 0pt plus 2cm + \pretolerance=10000 + \leavevmode \advance\leftskip\@tempdima %\hskip -\leftskip + \textit{#1}\par + \penalty\@highpenalty \endgroup} + +\setcounter{tocdepth}{0} +\newdimen\tocchpnum +\newdimen\tocsecnum +\newdimen\tocsectotal +\newdimen\tocsubsecnum +\newdimen\tocsubsectotal +\newdimen\tocsubsubsecnum +\newdimen\tocsubsubsectotal +\newdimen\tocparanum +\newdimen\tocparatotal +\newdimen\tocsubparanum +\tocchpnum=\z@ % no chapter numbers +\tocsecnum=15\p@ % section 88. plus 2.222pt +\tocsubsecnum=23\p@ % subsection 88.8 plus 2.222pt +\tocsubsubsecnum=27\p@ % subsubsection 88.8.8 plus 1.444pt +\tocparanum=35\p@ % paragraph 88.8.8.8 plus 1.666pt +\tocsubparanum=43\p@ % subparagraph 88.8.8.8.8 plus 1.888pt +\def\calctocindent{% +\tocsectotal=\tocchpnum +\advance\tocsectotal by\tocsecnum +\tocsubsectotal=\tocsectotal +\advance\tocsubsectotal by\tocsubsecnum +\tocsubsubsectotal=\tocsubsectotal +\advance\tocsubsubsectotal by\tocsubsubsecnum +\tocparatotal=\tocsubsubsectotal +\advance\tocparatotal by\tocparanum} +\calctocindent + +\def\l@section{\@dottedtocline{1}{\tocchpnum}{\tocsecnum}} +\def\l@subsection{\@dottedtocline{2}{\tocsectotal}{\tocsubsecnum}} +\def\l@subsubsection{\@dottedtocline{3}{\tocsubsectotal}{\tocsubsubsecnum}} +\def\l@paragraph{\@dottedtocline{4}{\tocsubsubsectotal}{\tocparanum}} +\def\l@subparagraph{\@dottedtocline{5}{\tocparatotal}{\tocsubparanum}} + +\def\listoffigures{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn + \fi\section*{\listfigurename\@mkboth{{\listfigurename}}{{\listfigurename}}} + \@starttoc{lof}\if@restonecol\twocolumn\fi} +\def\l@figure{\@dottedtocline{1}{0em}{1.5em}} + +\def\listoftables{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn + \fi\section*{\listtablename\@mkboth{{\listtablename}}{{\listtablename}}} + \@starttoc{lot}\if@restonecol\twocolumn\fi} +\let\l@table\l@figure + +\renewcommand\listoffigures{% + \section*{\listfigurename + \@mkboth{\listfigurename}{\listfigurename}}% + \@starttoc{lof}% + } + +\renewcommand\listoftables{% + \section*{\listtablename + \@mkboth{\listtablename}{\listtablename}}% + \@starttoc{lot}% + } + +\ifx\oribibl\undefined +\ifx\citeauthoryear\undefined +\renewenvironment{thebibliography}[1] + {\section*{\refname} + \def\@biblabel##1{##1.} + \small + \list{\@biblabel{\@arabic\c@enumiv}}% + {\settowidth\labelwidth{\@biblabel{#1}}% + \leftmargin\labelwidth + \advance\leftmargin\labelsep + \if@openbib + \advance\leftmargin\bibindent + \itemindent -\bibindent + \listparindent \itemindent + \parsep \z@ + \fi + \usecounter{enumiv}% + \let\p@enumiv\@empty + \renewcommand\theenumiv{\@arabic\c@enumiv}}% + \if@openbib + \renewcommand\newblock{\par}% + \else + \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}% + \fi + \sloppy\clubpenalty4000\widowpenalty4000% + \sfcode`\.=\@m} + {\def\@noitemerr + {\@latex@warning{Empty `thebibliography' environment}}% + \endlist} +\def\@lbibitem[#1]#2{\item[{[#1]}\hfill]\if@filesw + {\let\protect\noexpand\immediate + \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces} +\newcount\@tempcntc +\def\@citex[#1]#2{\if@filesw\immediate\write\@auxout{\string\citation{#2}}\fi + \@tempcnta\z@\@tempcntb\m@ne\def\@citea{}\@cite{\@for\@citeb:=#2\do + {\@ifundefined + {b@\@citeb}{\@citeo\@tempcntb\m@ne\@citea\def\@citea{,}{\bfseries + ?}\@warning + {Citation `\@citeb' on page \thepage \space undefined}}% + {\setbox\z@\hbox{\global\@tempcntc0\csname b@\@citeb\endcsname\relax}% + \ifnum\@tempcntc=\z@ \@citeo\@tempcntb\m@ne + \@citea\def\@citea{,}\hbox{\csname b@\@citeb\endcsname}% + \else + \advance\@tempcntb\@ne + \ifnum\@tempcntb=\@tempcntc + \else\advance\@tempcntb\m@ne\@citeo + \@tempcnta\@tempcntc\@tempcntb\@tempcntc\fi\fi}}\@citeo}{#1}} +\def\@citeo{\ifnum\@tempcnta>\@tempcntb\else + \@citea\def\@citea{,\,\hskip\z@skip}% + \ifnum\@tempcnta=\@tempcntb\the\@tempcnta\else + {\advance\@tempcnta\@ne\ifnum\@tempcnta=\@tempcntb \else + \def\@citea{--}\fi + \advance\@tempcnta\m@ne\the\@tempcnta\@citea\the\@tempcntb}\fi\fi} +\else +\renewenvironment{thebibliography}[1] + {\section*{\refname} + \small + \list{}% + {\settowidth\labelwidth{}% + \leftmargin\parindent + \itemindent=-\parindent + \labelsep=\z@ + \if@openbib + \advance\leftmargin\bibindent + \itemindent -\bibindent + \listparindent \itemindent + \parsep \z@ + \fi + \usecounter{enumiv}% + \let\p@enumiv\@empty + \renewcommand\theenumiv{}}% + \if@openbib + \renewcommand\newblock{\par}% + \else + \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}% + \fi + \sloppy\clubpenalty4000\widowpenalty4000% + \sfcode`\.=\@m} + {\def\@noitemerr + {\@latex@warning{Empty `thebibliography' environment}}% + \endlist} + \def\@cite#1{#1}% + \def\@lbibitem[#1]#2{\item[]\if@filesw + {\def\protect##1{\string ##1\space}\immediate + \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces} + \fi +\else +\@cons\@openbib@code{\noexpand\small} +\fi + +\def\idxquad{\hskip 10\p@}% space that divides entry from number + +\def\@idxitem{\par\hangindent 10\p@} + +\def\subitem{\par\setbox0=\hbox{--\enspace}% second order + \noindent\hangindent\wd0\box0}% index entry + +\def\subsubitem{\par\setbox0=\hbox{--\,--\enspace}% third + \noindent\hangindent\wd0\box0}% order index entry + +\def\indexspace{\par \vskip 10\p@ plus5\p@ minus3\p@\relax} + +\renewenvironment{theindex} + {\@mkboth{\indexname}{\indexname}% + \thispagestyle{empty}\parindent\z@ + \parskip\z@ \@plus .3\p@\relax + \let\item\par + \def\,{\relax\ifmmode\mskip\thinmuskip + \else\hskip0.2em\ignorespaces\fi}% + \normalfont\small + \begin{multicols}{2}[\@makeschapterhead{\indexname}]% + } + {\end{multicols}} + +\renewcommand\footnoterule{% + \kern-3\p@ + \hrule\@width 2truecm + \kern2.6\p@} + \newdimen\fnindent + \fnindent1em +\long\def\@makefntext#1{% + \parindent \fnindent% + \leftskip \fnindent% + \noindent + \llap{\hb@xt@1em{\hss\@makefnmark\ }}\ignorespaces#1} + +\long\def\@makecaption#1#2{% + \small + \vskip\abovecaptionskip + \sbox\@tempboxa{{\bfseries #1.} #2}% + \ifdim \wd\@tempboxa >\hsize + {\bfseries #1.} #2\par + \else + \global \@minipagefalse + \hb@xt@\hsize{\hfil\box\@tempboxa\hfil}% + \fi + \vskip\belowcaptionskip} + +\def\fps@figure{htbp} +\def\fnum@figure{\figurename\thinspace\thefigure} +\def \@floatboxreset {% + \reset@font + \small + \@setnobreak + \@setminipage +} +\def\fps@table{htbp} +\def\fnum@table{\tablename~\thetable} +\renewenvironment{table} + {\setlength\abovecaptionskip{0\p@}% + \setlength\belowcaptionskip{10\p@}% + \@float{table}} + {\end@float} +\renewenvironment{table*} + {\setlength\abovecaptionskip{0\p@}% + \setlength\belowcaptionskip{10\p@}% + \@dblfloat{table}} + {\end@dblfloat} + +\long\def\@caption#1[#2]#3{\par\addcontentsline{\csname + ext@#1\endcsname}{#1}{\protect\numberline{\csname + the#1\endcsname}{\ignorespaces #2}}\begingroup + \@parboxrestore + \@makecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par + \endgroup} + +% LaTeX does not provide a command to enter the authors institute +% addresses. The \institute command is defined here. + +\newcounter{@inst} +\newcounter{@auth} +\newcounter{auco} +\newdimen\instindent +\newbox\authrun +\newtoks\authorrunning +\newtoks\tocauthor +\newbox\titrun +\newtoks\titlerunning +\newtoks\toctitle + +\def\clearheadinfo{\gdef\@author{No Author Given}% + \gdef\@title{No Title Given}% + \gdef\@subtitle{}% + \gdef\@institute{No Institute Given}% + \gdef\@thanks{}% + \global\titlerunning={}\global\authorrunning={}% + \global\toctitle={}\global\tocauthor={}} + +\def\institute#1{\gdef\@institute{#1}} + +\def\institutename{\par + \begingroup + \parskip=\z@ + \parindent=\z@ + \setcounter{@inst}{1}% + \def\and{\par\stepcounter{@inst}% + \noindent$^{\the@inst}$\enspace\ignorespaces}% + \setbox0=\vbox{\def\thanks##1{}\@institute}% + \ifnum\c@@inst=1\relax + \gdef\fnnstart{0}% + \else + \xdef\fnnstart{\c@@inst}% + \setcounter{@inst}{1}% + \noindent$^{\the@inst}$\enspace + \fi + \ignorespaces + \@institute\par + \endgroup} + +\def\@fnsymbol#1{\ensuremath{\ifcase#1\or\star\or{\star\star}\or + {\star\star\star}\or \dagger\or \ddagger\or + \mathchar "278\or \mathchar "27B\or \|\or **\or \dagger\dagger + \or \ddagger\ddagger \else\@ctrerr\fi}} + +\def\inst#1{\unskip$^{#1}$} +\def\fnmsep{\unskip$^,$} +\def\email#1{{\tt#1}} +\AtBeginDocument{\@ifundefined{url}{\def\url#1{#1}}{}% +\@ifpackageloaded{babel}{% +\@ifundefined{extrasenglish}{}{\addto\extrasenglish{\switcht@albion}}% +\@ifundefined{extrasfrenchb}{}{\addto\extrasfrenchb{\switcht@francais}}% +\@ifundefined{extrasgerman}{}{\addto\extrasgerman{\switcht@deutsch}}% +}{\switcht@@therlang}% +\providecommand{\keywords}[1]{\par\addvspace\baselineskip +\noindent\keywordname\enspace\ignorespaces#1}% +} +\def\homedir{\~{ }} + +\def\subtitle#1{\gdef\@subtitle{#1}} +\clearheadinfo +% +%%% to avoid hyperref warnings +\providecommand*{\toclevel@author}{999} +%%% to make title-entry parent of section-entries +\providecommand*{\toclevel@title}{0} +% +\renewcommand\maketitle{\newpage +\phantomsection + \refstepcounter{chapter}% + \stepcounter{section}% + \setcounter{section}{0}% + \setcounter{subsection}{0}% + \setcounter{figure}{0} + \setcounter{table}{0} + \setcounter{equation}{0} + \setcounter{footnote}{0}% + \begingroup + \parindent=\z@ + \renewcommand\thefootnote{\@fnsymbol\c@footnote}% + \if@twocolumn + \ifnum \col@number=\@ne + \@maketitle + \else + \twocolumn[\@maketitle]% + \fi + \else + \newpage + \global\@topnum\z@ % Prevents figures from going at top of page. + \@maketitle + \fi + \thispagestyle{empty}\@thanks +% + \def\\{\unskip\ \ignorespaces}\def\inst##1{\unskip{}}% + \def\thanks##1{\unskip{}}\def\fnmsep{\unskip}% + \instindent=\hsize + \advance\instindent by-\headlineindent + \if!\the\toctitle!\addcontentsline{toc}{title}{\@title}\else + \addcontentsline{toc}{title}{\the\toctitle}\fi + \if@runhead + \if!\the\titlerunning!\else + \edef\@title{\the\titlerunning}% + \fi + \global\setbox\titrun=\hbox{\small\rm\unboldmath\ignorespaces\@title}% + \ifdim\wd\titrun>\instindent + \typeout{Title too long for running head. Please supply}% + \typeout{a shorter form with \string\titlerunning\space prior to + \string\maketitle}% + \global\setbox\titrun=\hbox{\small\rm + Title Suppressed Due to Excessive Length}% + \fi + \xdef\@title{\copy\titrun}% + \fi +% + \if!\the\tocauthor!\relax + {\def\and{\noexpand\protect\noexpand\and}% + \protected@xdef\toc@uthor{\@author}}% + \else + \def\\{\noexpand\protect\noexpand\newline}% + \protected@xdef\scratch{\the\tocauthor}% + \protected@xdef\toc@uthor{\scratch}% + \fi + \addtocontents{toc}{\noexpand\protect\noexpand\authcount{\the\c@auco}}% + \addcontentsline{toc}{author}{\toc@uthor}% + \if@runhead + \if!\the\authorrunning! + \value{@inst}=\value{@auth}% + \setcounter{@auth}{1}% + \else + \edef\@author{\the\authorrunning}% + \fi + \global\setbox\authrun=\hbox{\small\unboldmath\@author\unskip}% + \ifdim\wd\authrun>\instindent + \typeout{Names of authors too long for running head. Please supply}% + \typeout{a shorter form with \string\authorrunning\space prior to + \string\maketitle}% + \global\setbox\authrun=\hbox{\small\rm + Authors Suppressed Due to Excessive Length}% + \fi + \xdef\@author{\copy\authrun}% + \markboth{\@author}{\@title}% + \fi + \endgroup + \setcounter{footnote}{\fnnstart}% + \clearheadinfo} +% +\def\@maketitle{\newpage + \markboth{}{}% + \def\lastand{\ifnum\value{@inst}=2\relax + \unskip{} \andname\ + \else + \unskip \lastandname\ + \fi}% + \def\and{\stepcounter{@auth}\relax + \ifnum\value{@auth}=\value{@inst}% + \lastand + \else + \unskip, + \fi}% + \begin{center}% + \let\newline\\ + {\Large \bfseries\boldmath + \pretolerance=10000 + \@title \par}\vskip .8cm +\if!\@subtitle!\else {\large \bfseries\boldmath + \vskip -.65cm + \pretolerance=10000 + \@subtitle \par}\vskip .8cm\fi + \setbox0=\vbox{\setcounter{@auth}{1}\def\and{\stepcounter{@auth}}% + \def\thanks##1{}\@author}% + \global\value{@inst}=\value{@auth}% + \global\value{auco}=\value{@auth}% + \setcounter{@auth}{1}% +{\lineskip .5em +\noindent\ignorespaces +\@author\vskip.35cm} + {\small\institutename} + \end{center}% + } + +% definition of the "\spnewtheorem" command. +% +% Usage: +% +% \spnewtheorem{env_nam}{caption}[within]{cap_font}{body_font} +% or \spnewtheorem{env_nam}[numbered_like]{caption}{cap_font}{body_font} +% or \spnewtheorem*{env_nam}{caption}{cap_font}{body_font} +% +% New is "cap_font" and "body_font". It stands for +% fontdefinition of the caption and the text itself. +% +% "\spnewtheorem*" gives a theorem without number. +% +% A defined spnewthoerem environment is used as described +% by Lamport. +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\def\@thmcountersep{} +\def\@thmcounterend{.} + +\def\spnewtheorem{\@ifstar{\@sthm}{\@Sthm}} + +% definition of \spnewtheorem with number + +\def\@spnthm#1#2{% + \@ifnextchar[{\@spxnthm{#1}{#2}}{\@spynthm{#1}{#2}}} +\def\@Sthm#1{\@ifnextchar[{\@spothm{#1}}{\@spnthm{#1}}} + +\def\@spxnthm#1#2[#3]#4#5{\expandafter\@ifdefinable\csname #1\endcsname + {\@definecounter{#1}\@addtoreset{#1}{#3}% + \expandafter\xdef\csname the#1\endcsname{\expandafter\noexpand + \csname the#3\endcsname \noexpand\@thmcountersep \@thmcounter{#1}}% + \expandafter\xdef\csname #1name\endcsname{#2}% + \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}% + \global\@namedef{end#1}{\@endtheorem}}} + +\def\@spynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname + {\@definecounter{#1}% + \expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}% + \expandafter\xdef\csname #1name\endcsname{#2}% + \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#3}{#4}}% + \global\@namedef{end#1}{\@endtheorem}}} + +\def\@spothm#1[#2]#3#4#5{% + \@ifundefined{c@#2}{\@latexerr{No theorem environment `#2' defined}\@eha}% + {\expandafter\@ifdefinable\csname #1\endcsname + {\newaliascnt{#1}{#2}% + \expandafter\xdef\csname #1name\endcsname{#3}% + \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}% + \global\@namedef{end#1}{\@endtheorem}}}} + +\def\@spthm#1#2#3#4{\topsep 7\p@ \@plus2\p@ \@minus4\p@ +\refstepcounter{#1}% +\@ifnextchar[{\@spythm{#1}{#2}{#3}{#4}}{\@spxthm{#1}{#2}{#3}{#4}}} + +\def\@spxthm#1#2#3#4{\@spbegintheorem{#2}{\csname the#1\endcsname}{#3}{#4}% + \ignorespaces} + +\def\@spythm#1#2#3#4[#5]{\@spopargbegintheorem{#2}{\csname + the#1\endcsname}{#5}{#3}{#4}\ignorespaces} + +\def\@spbegintheorem#1#2#3#4{\trivlist + \item[\hskip\labelsep{#3#1\ #2\@thmcounterend}]#4} + +\def\@spopargbegintheorem#1#2#3#4#5{\trivlist + \item[\hskip\labelsep{#4#1\ #2}]{#4(#3)\@thmcounterend\ }#5} + +% definition of \spnewtheorem* without number + +\def\@sthm#1#2{\@Ynthm{#1}{#2}} + +\def\@Ynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname + {\global\@namedef{#1}{\@Thm{\csname #1name\endcsname}{#3}{#4}}% + \expandafter\xdef\csname #1name\endcsname{#2}% + \global\@namedef{end#1}{\@endtheorem}}} + +\def\@Thm#1#2#3{\topsep 7\p@ \@plus2\p@ \@minus4\p@ +\@ifnextchar[{\@Ythm{#1}{#2}{#3}}{\@Xthm{#1}{#2}{#3}}} + +\def\@Xthm#1#2#3{\@Begintheorem{#1}{#2}{#3}\ignorespaces} + +\def\@Ythm#1#2#3[#4]{\@Opargbegintheorem{#1} + {#4}{#2}{#3}\ignorespaces} + +\def\@Begintheorem#1#2#3{#3\trivlist + \item[\hskip\labelsep{#2#1\@thmcounterend}]} + +\def\@Opargbegintheorem#1#2#3#4{#4\trivlist + \item[\hskip\labelsep{#3#1}]{#3(#2)\@thmcounterend\ }} + +\if@envcntsect + \def\@thmcountersep{.} + \spnewtheorem{theorem}{Theorem}[section]{\bfseries}{\itshape} +\else + \spnewtheorem{theorem}{Theorem}{\bfseries}{\itshape} + \if@envcntreset + \@addtoreset{theorem}{section} + \else + \@addtoreset{theorem}{chapter} + \fi +\fi + +%definition of divers theorem environments +\spnewtheorem*{claim}{Claim}{\itshape}{\rmfamily} +\spnewtheorem*{proof}{Proof}{\itshape}{\rmfamily} +\if@envcntsame % alle Umgebungen wie Theorem. + \def\spn@wtheorem#1#2#3#4{\@spothm{#1}[theorem]{#2}{#3}{#4}} +\else % alle Umgebungen mit eigenem Zaehler + \if@envcntsect % mit section numeriert + \def\spn@wtheorem#1#2#3#4{\@spxnthm{#1}{#2}[section]{#3}{#4}} + \else % nicht mit section numeriert + \if@envcntreset + \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4} + \@addtoreset{#1}{section}} + \else + \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4} + \@addtoreset{#1}{chapter}}% + \fi + \fi +\fi +\spn@wtheorem{case}{Case}{\itshape}{\rmfamily} +\spn@wtheorem{conjecture}{Conjecture}{\itshape}{\rmfamily} +\spn@wtheorem{corollary}{Corollary}{\bfseries}{\itshape} +\spn@wtheorem{definition}{Definition}{\bfseries}{\itshape} +\spn@wtheorem{example}{Example}{\itshape}{\rmfamily} +\spn@wtheorem{exercise}{Exercise}{\itshape}{\rmfamily} +\spn@wtheorem{lemma}{Lemma}{\bfseries}{\itshape} +\spn@wtheorem{note}{Note}{\itshape}{\rmfamily} +\spn@wtheorem{problem}{Problem}{\itshape}{\rmfamily} +\spn@wtheorem{property}{Property}{\itshape}{\rmfamily} +\spn@wtheorem{proposition}{Proposition}{\bfseries}{\itshape} +\spn@wtheorem{question}{Question}{\itshape}{\rmfamily} +\spn@wtheorem{solution}{Solution}{\itshape}{\rmfamily} +\spn@wtheorem{remark}{Remark}{\itshape}{\rmfamily} + +\def\@takefromreset#1#2{% + \def\@tempa{#1}% + \let\@tempd\@elt + \def\@elt##1{% + \def\@tempb{##1}% + \ifx\@tempa\@tempb\else + \@addtoreset{##1}{#2}% + \fi}% + \expandafter\expandafter\let\expandafter\@tempc\csname cl@#2\endcsname + \expandafter\def\csname cl@#2\endcsname{}% + \@tempc + \let\@elt\@tempd} + +\def\theopargself{\def\@spopargbegintheorem##1##2##3##4##5{\trivlist + \item[\hskip\labelsep{##4##1\ ##2}]{##4##3\@thmcounterend\ }##5} + \def\@Opargbegintheorem##1##2##3##4{##4\trivlist + \item[\hskip\labelsep{##3##1}]{##3##2\@thmcounterend\ }} + } + +\renewenvironment{abstract}{% + \list{}{\advance\topsep by0.35cm\relax\small + \leftmargin=1cm + \labelwidth=\z@ + \listparindent=\z@ + \itemindent\listparindent + \rightmargin\leftmargin}\item[\hskip\labelsep + \bfseries\abstractname]} + {\endlist} + +\newdimen\headlineindent % dimension for space between +\headlineindent=1.166cm % number and text of headings. + +\def\ps@headings{\let\@mkboth\@gobbletwo + \let\@oddfoot\@empty\let\@evenfoot\@empty + \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}% + \leftmark\hfil} + \def\@oddhead{\normalfont\small\hfil\rightmark\hspace{\headlineindent}% + \llap{\thepage}} + \def\chaptermark##1{}% + \def\sectionmark##1{}% + \def\subsectionmark##1{}} + +\def\ps@titlepage{\let\@mkboth\@gobbletwo + \let\@oddfoot\@empty\let\@evenfoot\@empty + \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}% + \hfil} + \def\@oddhead{\normalfont\small\hfil\hspace{\headlineindent}% + \llap{\thepage}} + \def\chaptermark##1{}% + \def\sectionmark##1{}% + \def\subsectionmark##1{}} + +\if@runhead\ps@headings\else +\ps@empty\fi + +\setlength\arraycolsep{1.4\p@} +\setlength\tabcolsep{1.4\p@} + +\endinput +%end of file llncs.cls diff -r a5da7b6aff8f -r 6f38e357b337 ESOP-Paper/document/proof.sty --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ESOP-Paper/document/proof.sty Tue Mar 29 23:52:14 2011 +0200 @@ -0,0 +1,278 @@ +% proof.sty (Proof Figure Macros) +% +% version 3.0 (for both LaTeX 2.09 and LaTeX 2e) +% Mar 6, 1997 +% Copyright (C) 1990 -- 1997, Makoto Tatsuta (tatsuta@kusm.kyoto-u.ac.jp) +% +% This program is free software; you can redistribute it or modify +% it under the terms of the GNU General Public License as published by +% the Free Software Foundation; either versions 1, or (at your option) +% any later version. +% +% This program is distributed in the hope that it will be useful +% but WITHOUT ANY WARRANTY; without even the implied warranty of +% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +% GNU General Public License for more details. +% +% Usage: +% In \documentstyle, specify an optional style `proof', say, +% \documentstyle[proof]{article}. +% +% The following macros are available: +% +% In all the following macros, all the arguments such as +% and are processed in math mode. +% +% \infer +% draws an inference. +% +% Use & in to delimit upper formulae. +% consists more than 0 formulae. +% +% \infer returns \hbox{ ... } or \vbox{ ... } and +% sets \@LeftOffset and \@RightOffset globally. +% +% \infer[