diff -r a6f3e1b08494 -r b6873d123f9b ESOP-Paper/Paper.thy --- a/ESOP-Paper/Paper.thy Sat May 12 21:05:59 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2394 +0,0 @@ - -(*<*) -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 bs'="bs", no_vars]} \;\;\text{if and only if}\;\; - %@{thm (rhs) Abs_eq_iff(1)[where bs="as" and bs'="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 lifting 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 bound by @{text bn}, but also some that 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 -(*>*)