diff -r fb201e383f1b -r da575186d492 LMCS-Paper/Paper.thy --- a/LMCS-Paper/Paper.thy Tue Feb 19 05:38:46 2013 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2766 +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" - equ2 :: "'a \ 'a \ bool" - Abs_dist :: "'a \ 'b \ 'c" - Abs_print :: "'a \ 'b \ 'c" - -definition - "equal \ (op =)" - -fun alpha_set_ex where - "alpha_set_ex (bs, x) R f (cs, y) = (\pi. alpha_set (bs, x) R f pi (cs, y))" - -fun alpha_res_ex where - "alpha_res_ex (bs, x) R f pi (cs, y) = (\pi. alpha_res (bs, x) R f pi (cs, y))" - -fun alpha_lst_ex where - "alpha_lst_ex (bs, x) R f pi (cs, y) = (\pi. alpha_lst (bs, x) R f pi (cs, y))" - - - -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_ex ("_ \\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _\<^esup> _") and - alpha_lst_ex ("_ \\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _\<^esup> _") and - alpha_res_ex ("_ \\<^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 - alpha_abs_lst ("_ \\<^raw:{$\,_{\textit{abs\_list}}$}> _") and - alpha_abs_res ("_ \\<^raw:{$\,_{\textit{abs\_set+}}$}> _") and - Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and - Abs_lst ("[_]\<^bsub>list\<^esub>._" [20, 101] 999) and - Abs_dist ("[_]\<^bsub>#list\<^esub>._" [20, 101] 999) 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 fa_trm_al :: 'a -consts alpha_trm2 ::'a -consts fa_trm2 :: 'a -consts fa_trm2_al :: 'a -consts supp2 :: 'a -consts ast :: 'a -consts ast' :: 'a -consts bn_al :: "'b \ 'a" -notation (latex output) - alpha_trm ("\\<^bsub>trm\<^esub>") and - fa_trm ("fa\<^bsub>trm\<^esub>") and - fa_trm_al ("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 - fa_trm2_al ("'(fa\\<^bsub>assn\<^esub>, fa\\<^bsub>trm\<^esub>')") and - ast ("'(as, t')") and - ast' ("'(as', t\ ')") and - equ2 ("'(=, =')") and - supp2 ("'(supp, supp')") and - bn_al ("bn\<^sup>\ _" [100] 100) -(*>*) - - -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"} - \]\smallskip - - \noindent - where free and bound variables have names. For such alpha-equated terms, - Nominal Isabelle derives automatically a reasoning infrastructure that has - been used successfully in formalisations of an equivalence checking - algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed - 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{15mm} - @{text "S ::= \{x\<^isub>1,\, x\<^isub>n}. T"} - \end{array} - \end{equation}\smallskip - - \noindent - and the @{text "\"}-quantification binds a finite (possibly empty) set of - type-variables. While it is possible to implement this kind of more general - binders by iterating single binders, like @{text "\x\<^isub>1.\x\<^isub>2...\x\<^isub>n.T"}, this leads to a rather clumsy - formalisation of W. For example, the usual definition for a - type being an instance of a type-scheme requires in the iterated version - the following auxiliary \emph{unbinding relation}: - - \[ - \infer{@{text T} \hookrightarrow ([], @{text T})}{}\qquad - \infer{\forall @{text x.S} \hookrightarrow (@{text x}\!::\!@{text xs}, @{text T})} - {@{text S} \hookrightarrow (@{text xs}, @{text T})} - \]\smallskip - - \noindent - Its purpose is to relate a type-scheme with a list of type-variables and a type. It is used to - address the following problem: - Given a type-scheme, say @{text S}, how does one get access to the bound type-variables - and the type-part of @{text S}? The unbinding relation gives an answer to this problem, though - in general it will only provide \emph{a} list of type-variables together with \emph{a} type that are - ``alpha-equivalent'' to @{text S}. This is because unbinding is a relation; it cannot be a function - for alpha-equated type-schemes. With the unbinding relation - in place, we can define when a type @{text T} is an instance of a type-scheme @{text S} as follows: - - \[ - @{text "T \ S \ \xs T' \. S \ (xs, T') \ dom \ = set xs \ \(T') = T"} - \]\smallskip - - \noindent - This means there exists a list of type-variables @{text xs} and a type @{text T'} to which - the type-scheme @{text S} unbinds, and there exists a substitution @{text "\"} whose domain is - @{text xs} (seen as set) such that @{text "\(T') = T"}. - The problem with this definition is that we cannot follow the usual proofs - that are by induction on the type-part of the type-scheme (since it is under - an existential quantifier and only an alpha-variant). The implementation of - type-schemes using iterations of single binders - prevents us from directly ``unbinding'' the bound type-variables and the type-part. - Clearly, a more dignified approach for formalising algorithm W is desirable. - The purpose of this paper is to introduce general binders, which - allow us to represent type-schemes so that they can bind multiple variables at once - and as a result solve this problem more straightforwardly. - The need of iterating single binders is also one reason - why the existing Nominal Isabelle and similar theorem provers that only provide - mechanisms for binding single variables have so far not fared very 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 in \eqref{ex1} below 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>\ \{x, y}. y \ x"}\hspace{10mm} - @{text "\{x, y}. x \ y \\<^isub>\ \{z}. z \ z"} - \end{equation}\smallskip - - \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}\smallskip - - \noindent - where @{text z} does not occur freely in the type. In this paper we will - give a general binding mechanism and associated notion of alpha-equivalence - 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 for - type-schemes by Leroy in \cite[Page 18--19]{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}\smallskip - - \noindent - we might not care in which order the assignments @{text "x = 3"} and - \mbox{@{text "y = 2"}} are given, but it would be often unusual (particularly - in strict languages) to regard \eqref{one} as alpha-equivalent with - - \[ - @{text "\ x = 3 \ y = 2 \ z = foo \ x - y \"} - \]\smallskip - - \noindent - Therefore we will also provide a separate binding mechanism for cases in - which the order of binders does not matter, but the `cardinality' of the - 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}\smallskip - - \noindent - we want to bind all variables from the pattern inside the body of the - $\mathtt{let}$, but we also care about the order of these variables, since - we do not want to regard \eqref{two} as alpha-equivalent with - - \[ - @{text "\ (y, x) = (3, 2) \ x - y \"} - \]\smallskip - - \noindent - As a result, we provide three general binding mechanisms each of which binds - multiple variables at once, and let the user choose which one is intended - 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 - - \[ - @{text "\ x\<^isub>1 = t\<^isub>1 \ \ \ x\<^isub>n = t\<^isub>n \ s \"} - \]\smallskip - - \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 - - \[ - @{text "\ (\x\<^isub>1\x\<^isub>n . s) [t\<^isub>1,\,t\<^isub>n]"} - \]\smallskip - - \noindent - where the notation @{text "\_ . _"} indicates that the list of @{text - "x\<^isub>i"} becomes bound in @{text s}. In this representation the term - \mbox{@{text "\ (\x . s) [t\<^isub>1, t\<^isub>2]"}} is a perfectly - legal instance, but the lengths of the two lists do not agree. To exclude - such terms, additional predicates about well-formed terms are needed in - order to ensure that the two lists are of equal length. This can result in - very messy reasoning (see for example~\cite{BengtsonParow09}). To avoid - this, we will allow type specifications for @{text "\"}s as follows - - \[ - \mbox{\begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}ll} - @{text trm} & @{text "::="} & @{text "\"} \\ - & @{text "|"} & @{text "\ as::assn s::trm"}\hspace{2mm} - \isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text "s"}\\[1mm] - @{text assn} & @{text "::="} & @{text "\"}\\ - & @{text "|"} & @{text "\ name trm assn"} - \end{tabular}} - \]\smallskip - - \noindent - where @{text assn} is an auxiliary type representing a list of assignments - and @{text bn} an auxiliary function identifying the variables to be bound - by the @{text "\"}. This function can be defined by recursion over @{text - assn} as follows - - \[ - @{text "bn(\) ="}~@{term "{}"} \hspace{10mm} - @{text "bn(\ x t as) = {x} \ bn(as)"} - \]\smallskip - - \noindent - The scope of the binding is indicated by labels given to the types, for - example @{text "s::trm"}, and a binding clause, in this case - \isacommand{binds} @{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}. Our work - extends Ott in several aspects: one is that we support three binding - modes---Ott has only one, namely the one where the order of binders matters. - Another is that our reasoning infrastructure, like strong induction principles - and the notion of free variables, is derived from first principles within - the Isabelle/HOL theorem prover. - - However, we will not be able to cope with all specifications that are - allowed by Ott. One reason is that Ott lets the user specify `empty' types - like \mbox{@{text "t ::= t t | \x. t"}} where no clause for variables is - given. Arguably, such specifications make some sense in the context of Coq's - type theory (which Ott supports), but not at all in a HOL-based environment - where every datatype must have a non-empty set-theoretic model - \cite{Berghofer99}. Another reason is that we establish the reasoning - infrastructure for alpha-\emph{equated} terms. In contrast, Ott produces a - reasoning infrastructure in Isabelle/HOL for \emph{non}-alpha-equated, or - `raw', terms. While our alpha-equated terms and the `raw' terms produced by - Ott use names for bound variables, there is a key difference: working with - alpha-equated terms means, for example, that the two type-schemes - - \[ - @{text "\{x}. x \ y = \{x, z}. x \ y"} - \]\smallskip - - \noindent - are not just alpha-equal, but actually \emph{equal}! As a result, we can - only support specifications that make sense on the level of alpha-equated - 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{equation}\label{picture} - \mbox{\begin{tikzpicture}[scale=1.1] - %\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.5) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]classes\end{tabular}}; - \draw (-2.4, 0.5) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}}; - \draw (1.8, 0.48) node[right=-0.1mm] - {\small\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}}; - \draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}}; - \draw (-3.25, 0.55) node {\small\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}}; - - \draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3); - \draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism}; - - \end{tikzpicture}} - \end{equation}\smallskip - - \noindent - We take as the starting point a definition of raw terms (defined as a - datatype in Isabelle/HOL); then identify the alpha-equivalence classes in - the type of sets of raw terms according to our alpha-equivalence relation, - and finally define the new type as these alpha-equivalence classes (the - non-emptiness requirement is always satisfied whenever the raw terms are - definable as datatype in Isabelle/HOL and our relation for alpha-equivalence - is an equivalence relation). - - The fact that we obtain an isomorphism between the new type and the - non-empty subset shows that the new type is a faithful representation of - alpha-equated terms. That is not the case for example for terms using the - 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 - as follows - - \[ - \mbox{\begin{tabular}{l@ {\hspace{1mm}}r@ {\hspace{1mm}}l} - @{text "fv(x)"} & @{text "\"} & @{text "{x}"}\\ - @{text "fv(t\<^isub>1 t\<^isub>2)"} & @{text "\"} & @{text "fv(t\<^isub>1) \ fv(t\<^isub>2)"}\\ - @{text "fv(\x.t)"} & @{text "\"} & @{text "fv(t) - {x}"} - \end{tabular}} - \]\smallskip - - \noindent - then with the help of the quotient package we can obtain a function @{text "fv\<^sup>\"} - operating on quotients, that is alpha-equivalence classes of lambda-terms. This - lifted function is characterised by the equations - - \[ - \mbox{\begin{tabular}{l@ {\hspace{1mm}}r@ {\hspace{1mm}}l} - @{text "fv\<^sup>\(x)"} & @{text "="} & @{text "{x}"}\\ - @{text "fv\<^sup>\(t\<^isub>1 t\<^isub>2)"} & @{text "="} & @{text "fv\<^sup>\(t\<^isub>1) \ fv\<^sup>\(t\<^isub>2)"}\\ - @{text "fv\<^sup>\(\x.t)"} & @{text "="} & @{text "fv\<^sup>\(t) - {x}"} - \end{tabular}} - \]\smallskip - - \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 include the term language of Core-Haskell (see - Figure~\ref{corehas}). 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 algorithm W, - which includes multiple binders 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 automati\-cally-generated - 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 automatically derive strong - induction principles that have the variable convention already built in. - For this we simplify the earlier automated proofs by using the proving tools - from the function package~\cite{Krauss09} of Isabelle/HOL. 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' inside a theorem prover. - - - \begin{figure}[t] - \begin{boxedminipage}{\linewidth} - \begin{center} - \begin{tabular}{@ {\hspace{8mm}}r@ {\hspace{2mm}}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:\. \ | \ \ \ | refl \ | sym \ | \\<^isub>1 \ \\<^isub>2"}\\ - & @{text "|"} & @{text "\ @ \ | left \ | right \ | \\<^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 \ | \x:\. e | e\<^isub>1 e\<^isub>2"}\\ - & @{text "|"} & @{text "\ x:\ = e\<^isub>1 \ e\<^isub>2 | \ 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 (the overlines stand for lists).\label{corehas}} - \end{figure} -*} - -section {* A Short Review of the Nominal Logic Work *} - -text {* - At its core, Nominal Isabelle is an adaptation 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 "\, \\<^isub>1, \"} to stand for permutations, - which in Nominal Isabelle have type @{typ perm}. 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 "_ \ _ "} and having the type @{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 "\\<^isub>1"} and @{term "\\<^isub>2"} as \mbox{@{term "\\<^isub>1 + \\<^isub>2"}} - (even if this operation is non-commutative), - and the inverse permutation of @{term "\"} as @{text "- \"}. The permutation - operation is defined over Isabelle/HOL's type-hierarchy \cite{HuffmanUrban10}; - for example permutations acting on atoms, products, lists, permutations, sets, - functions and booleans are given by: - - \begin{equation}\label{permute} - \mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}} - \begin{tabular}{@ {}l@ {}} - @{text "\ \ a \ \ a"}\\ - @{thm permute_prod.simps[where p="\", no_vars, THEN eq_reflection]}\\[2mm] - @{thm permute_list.simps(1)[where p="\", no_vars, THEN eq_reflection]}\\ - @{thm permute_list.simps(2)[where p="\", no_vars, THEN eq_reflection]}\\ - \end{tabular} & - \begin{tabular}{@ {}l@ {}} - @{thm permute_perm_def[where p="\" and q="\'", no_vars, THEN eq_reflection]}\\ - @{thm permute_set_def[where p="\", no_vars, THEN eq_reflection]}\\ - @{text "\ \ f \ \x. \ \ (f (- \ \ x))"}\\ - @{thm permute_bool_def[where p="\", no_vars, THEN eq_reflection]} - \end{tabular} - \end{tabular}} - \end{equation}\smallskip - - \noindent - Concrete permutations in Nominal Isabelle are built up from swappings, - written as \mbox{@{text "(a b)"}}, which are permutations that behave - as follows: - - \[ - @{text "(a b) = \c. if a = c then b else if b = c then a else c"} - \]\smallskip - - 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. Its 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}\smallskip - - \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]} - \]\smallskip - - \noindent - 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 - - \begin{prop}\label{swapfreshfresh} - If @{thm (prem 1) swap_fresh_fresh[no_vars]} and @{thm (prem 2) swap_fresh_fresh[no_vars]} - then @{thm (concl) swap_fresh_fresh[no_vars]}. - \end{prop} - - 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{equation}\label{supps}\mbox{ - \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 \"} & $=$ & @{term "{a. \ \ a \ a}"} - \end{tabular} - \end{tabular}} - \end{equation}\smallskip - - \noindent - in some cases it can be difficult to characterise the support precisely, and - only an approximation can be established (as for function applications - above). Reasoning about such approximations can be simplified with the - notion \emph{supports}, defined as follows: - - \begin{defi} - A set @{text S} \emph{supports} @{text x}, if for all atoms @{text a} and @{text b} - not in @{text S} we have @{term "(a \ b) \ x = x"}. - \end{defi} - - \noindent - The main point of @{text supports} is that we can establish the following - two properties. - - \begin{prop}\label{supportsprop} - Given a set @{text "bs"} of atoms.\\ - {\it (i)} If @{thm (prem 1) supp_is_subset[where S="bs", no_vars]} - and @{thm (prem 2) supp_is_subset[where S="bs", no_vars]} then - @{thm (concl) supp_is_subset[where S="bs", no_vars]}.\\ - {\it (ii)} @{thm supp_supports[no_vars]}. - \end{prop} - - Another important notion in the nominal logic work is \emph{equivariance}. - For a function @{text f} to be equivariant - it is required that every permutation leaves @{text f} unchanged, that is - - \begin{equation}\label{equivariancedef} - @{term "\\. \ \ f = f"}\;. - \end{equation}\smallskip - - \noindent - If a function is of type @{text "\ \ \"}, say, this definition is equivalent to - the fact that a permutation applied to the application - @{text "f x"} can be moved to the argument @{text x}. That means for - such functions, we have for all permutations @{text "\"}: - - \begin{equation}\label{equivariance} - @{text "\ \ f = f"} \;\;\;\;\textit{if and only if}\;\;\;\; - @{text "\x. \ \ (f x) = f (\ \ x)"}\;. - \end{equation}\smallskip - - \noindent - There is - also a similar property for relations, which are in HOL functions of type @{text "\ \ \ \ bool"}. - Suppose a relation @{text R}, then for all permutations @{text \}: - - \[ - @{text "\ \ R = R"} \;\;\;\;\textit{if and only if}\;\;\;\; - @{text "\x y."}~~@{text "x R y"} \;\textit{implies}\; @{text "(\ \ x) R (\ \ y)"}\;. - \]\smallskip - - \noindent - Note that from property \eqref{equivariancedef} and the definition of @{text supp}, we - can easily deduce that for a function being equivariant is equivalent to having empty support. - - 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 - Proposition~\ref{swapfreshfresh} to rename single binders, this property - proved too unwieldy for dealing with multiple binders. For such binders the - following generalisations turned out to be easier to use. - - \begin{prop}\label{supppermeq} - @{thm[mode=IfThen] supp_perm_eq[where p="\", no_vars]} - \end{prop} - - \begin{prop}\label{avoiding} - For a finite set @{text as} and a finitely supported @{text x} with - @{term "as \* x"} and also a finitely supported @{text c}, there - exists a permutation @{text "\"} such that @{term "(\ \ as) \* c"} and - @{term "supp x \* \"}. - \end{prop} - - \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 "\"} such that - the renamed binders @{term "\ \ as"} avoid @{text c} (which can be arbitrarily chosen - as long as it is finitely supported) and also @{text "\"} does not affect anything - in the support of @{text x} (that is @{term "supp x \* \"}). The last - fact and Property~\ref{supppermeq} allow us to `rename' just the binders - @{text as} in @{text x}, because @{term "\ \ x = x"}. - - Note that @{term "supp x \* \"} - is equivalent with @{term "supp \ \* x"}, which means we could also formulate - Propositions \ref{supppermeq} and \ref{avoiding} in the other `direction'; however the - reasoning infrastructure of Nominal Isabelle is set up so that it provides more - automation for the formulation given above. - - 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 - use of these properties in order to define alpha-equivalence in - the presence of multiple binders. -*} - - -section {* Abstractions\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 writing 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 "(as, x)"} and @{text "(bs, y)"} need to have the same set of free - atoms; moreover there must be a permutation @{text \} such that {\it - (ii)} @{text \} leaves the free atoms of @{text "(as, x)"} and @{text "(bs, 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 \} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The - requirements {\it (i)} to {\it (iv)} can be stated formally as: - - \begin{defi}[Alpha-Equivalence for Set-Bindings]\label{alphaset}\mbox{}\\ - \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl} - @{term "alpha_set_ex (as, x) R fa (bs, y)"}\hspace{2mm}@{text "\"} & - \multicolumn{2}{@ {}l}{if there exists a @{text "\"} such that:}\\ - & \mbox{\it (i)} & @{term "fa(x) - as = fa(y) - bs"}\\ - & \mbox{\it (ii)} & @{term "(fa(x) - as) \* \"}\\ - & \mbox{\it (iii)} & @{text "(\ \ x) R y"} \\ - & \mbox{\it (iv)} & @{term "(\ \ as) = bs"} \\ - \end{tabular} - \end{defi} - - \noindent - 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}}^{\textit{R}, \textit{fa}}$ 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"}. - - Definition \ref{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{defi}[Alpha-Equivalence for List-Bindings]\label{alphalist}\mbox{}\\ - \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl} - @{term "alpha_lst_ex (as, x) R fa (bs, y)"}\hspace{2mm}@{text "\"} & - \multicolumn{2}{@ {}l}{if there exists a @{text "\"} such that:}\\ - & \mbox{\it (i)} & @{term "fa(x) - (set as) = fa(y) - (set bs)"}\\ - & \mbox{\it (ii)} & @{term "(fa(x) - set as) \* \"}\\ - & \mbox{\it (iii)} & @{text "(\ \ x) R y"}\\ - & \mbox{\it (iv)} & @{term "(\ \ as) = bs"}\\ - \end{tabular} - \end{defi} - - \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 according to Pitts~\cite{Pitts04} - \emph{restrict} atoms, then we keep sets of binders, but drop - condition {\it (iv)} in Definition~\ref{alphaset}: - - \begin{defi}[Alpha-Equivalence for Set+-Bindings]\label{alphares}\mbox{}\\ - \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl} - @{term "alpha_res_ex (as, x) R fa (bs, y)"}\hspace{2mm}@{text "\"} & - \multicolumn{2}{@ {}l}{if there exists a @{text "\"} such that:}\\ - & \mbox{\it (i)} & @{term "fa(x) - as = fa(y) - bs"}\\ - & \mbox{\it (ii)} & @{term "(fa(x) - as) \* \"}\\ - & \mbox{\it (iii)} & @{text "(\ \ x) R y"}\\ - \end{tabular} - \end{defi} - - - 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 - - \[ - @{text "fa(x) \ {x}"} \hspace{10mm} @{text "fa(T\<^isub>1 \ T\<^isub>2) \ fa(T\<^isub>1) \ fa(T\<^isub>2)"} - \]\smallskip - - \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 "({x, y}, y \ x)"} are alpha-equivalent according to - $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{set+}}$ by taking @{text "\"} 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 "\"} 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 this case they also agree with the alpha-equivalence - used in older versions of Nominal Isabelle \cite{Urban08}.\footnote{We omit a - proof of this fact since the details are hairy and not really important for the - purpose of this paper.} - - In the rest of this section we are going to show that the alpha-equivalences - really lead to abstractions where some atoms are bound (or more precisely - removed from the support). For this we will consider three abstraction - types that are quotients of the relations - - \begin{equation} - \begin{array}{r} - @{term "alpha_set_ex (as, x) equal supp (bs, y)"}\smallskip\\ - @{term "alpha_res_ex (as, x) equal supp (bs, y)"}\smallskip\\ - @{term "alpha_lst_ex (as, x) equal supp (bs, y)"}\\ - \end{array} - \end{equation}\smallskip - - \noindent - Note that in these relations we replaced the free-atom function @{text "fa"} - with @{term "supp"} and the relation @{text R} with equality. We can show - the following two properties: - - \begin{lem}\label{alphaeq} - The relations $\approx_{\,\textit{set}}^{=, \textit{supp}}$, - $\approx_{\,\textit{set+}}^{=, \textit{supp}}$ - and $\approx_{\,\textit{list}}^{=, \textit{supp}}$ are - equivalence relations and equivariant. - \end{lem} - - \begin{proof} - Reflexivity is by taking @{text "\"} to be @{text "0"}. For symmetry we have - a permutation @{text "\"} and for the proof obligation take @{term "- - \"}. In case of transitivity, we have two permutations @{text "\\<^isub>1"} - and @{text "\\<^isub>2"}, and for the proof obligation use @{text - "\\<^isub>1 + \\<^isub>2"}. Equivariance means @{term "alpha_set_ex (\ \ as, - \ \ x) equal supp (\ \ bs, \ \ y)"} holds provided \mbox{@{term - "alpha_set_ex (as, x) equal supp(bs, y)"}} holds. From the assumption we - have a permutation @{text "\'"} and for the proof obligation use @{text "\ \ - \'"}. To show equivariance, we need to `pull out' the permutations, - which is possible since all operators, namely as @{text "#\<^sup>*, -, =, \, - set"} and @{text "supp"}, are equivariant (see - \cite{HuffmanUrban10}). Finally, we apply the permutation operation on - booleans. - \end{proof} - - \noindent - Recall the picture shown in \eqref{picture} about new types in HOL. - The lemma above allows us to use our quotient package for introducing - new types @{text "\ abs\<^bsub>set\<^esub>"}, @{text "\ abs\<^bsub>set+\<^esub>"} and @{text "\ abs\<^bsub>list\<^esub>"} - 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 - - \[ - @{term "Abs_set as x"} \hspace{10mm} - @{term "Abs_res as x"} \hspace{10mm} - @{term "Abs_lst as x"} - \]\smallskip - - \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{thm}[Support of Abstractions]\label{suppabs} - Assuming @{text x} has finite support, then - - \[ - \begin{array}{l@ {\;=\;}l} - @{thm (lhs) supp_Abs(1)[no_vars]} & @{thm (rhs) supp_Abs(1)[no_vars]}\\ - @{thm (lhs) supp_Abs(2)[no_vars]} & @{thm (rhs) supp_Abs(2)[no_vars]}\\ - @{thm (lhs) supp_Abs(3)[where bs="as", no_vars]} & - @{thm (rhs) supp_Abs(3)[where bs="as", no_vars]}\\ - \end{array} - \]\smallskip - \end{thm} - - \noindent - In effect, this theorem states that the atoms @{text "as"} are bound in the - abstraction. As stated earlier, this can be seen as a litmus test that our - Definitions \ref{alphaset}, \ref{alphalist} and \ref{alphares} capture the - idea of alpha-equivalence relations. Below we will give the proof for the - first equation of Theorem \ref{suppabs}. The others follow by similar - arguments. By definition of the abstraction type @{text - "abs\<^bsub>set\<^esub>"} 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}\;\;\; - @{term "alpha_set_ex (as, x) equal supp (bs, y)"} - \end{equation}\smallskip - - \noindent - and also set - - \begin{equation}\label{absperm} - @{thm permute_Abs(1)[where p="\", no_vars, THEN eq_reflection]} - \end{equation}\smallskip - - \noindent - With this at our disposal, we can show - the following lemma about swapping two atoms in an abstraction. - - \begin{lem} - If @{thm (prem 1) Abs_swap1(1)[where bs="as", no_vars]} and - @{thm (prem 2) Abs_swap1(1)[where bs="as", no_vars]} then - @{thm (concl) Abs_swap1(1)[where bs="as", no_vars]} - \end{lem} - - \begin{proof} - If @{term "a = b"} the lemma is immediate, since @{term "(a \ b)"} is then - the identity permutation. - Also in the other case the lemma is straightforward using \eqref{abseqiff} - and observing that the assumptions give us @{term "(a \ b) \ (supp x - as) = - (supp x - as)"}. We therefore can use the swapping @{term "(a \ b)"} as - the permutation for the proof obligation. - \end{proof} - - \noindent - This lemma together - with \eqref{absperm} allows us to show - - \begin{equation}\label{halfone} - @{thm Abs_supports(1)[no_vars]} - \end{equation}\smallskip - - \noindent - which by Property~\ref{supportsprop} gives us `one half' of - Theorem~\ref{suppabs}. To establish the `other half', 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]} - \]\smallskip - - \noindent - Using the second equation in \eqref{equivariance}, we can show that - @{text "aux"} is equivariant (since @{term "\ \ (supp x - as) = (supp (\ \ x)) - (\ \ as)"}) - and therefore has empty support. - This in turn means - - \[ - @{term "supp (supp_set (Abs_set as x)) \ supp (Abs_set as x)"} - \]\smallskip - - \noindent - using the fact about the support of function applications in \eqref{supps}. 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}\smallskip - - \noindent - This is because for every finite set of atoms, say @{text "bs"}, we have - @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.\footnote{Note that this is not - the case for infinite sets.} - Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes - the first equation of Theorem~\ref{suppabs}. The others are similar. - - Recall the definition of support given in \eqref{suppdef}, and note the difference between - the support of a raw pair and an abstraction - - \[ - @{term "supp (as, x) = supp as \ supp x"}\hspace{15mm} - @{term "supp (Abs_set as x) = supp x - as"} - \]\smallskip - - \noindent - While the permutation operations behave in both cases the same (a permutation - is just moved to the arguments), the notion of equality is different for pairs and - abstractions. Therefore we have different supports. In case of abstractions, - we have established in Theorem~\ref{suppabs} that bound atoms are removed from - the support of the abstractions' bodies. - - 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 extremely 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 mutually 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 schematically as follows: - - \begin{equation}\label{scheme} - \mbox{\begin{tabular}{@ {}p{2.5cm}l} - type \mbox{declaration part} & - $\begin{cases} - \mbox{\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}$\\[2mm] - binding \mbox{function part} & - $\begin{cases} - \mbox{\begin{tabular}{l} - \isacommand{binder} @{text "bn\\<^isub>1"} \isacommand{and} \ldots \isacommand{and} @{text "bn\\<^isub>m"}\\ - \isacommand{where}\\ - \raisebox{2mm}{$\ldots$}\\[-2mm] - \end{tabular}} - \end{cases}$\\ - \end{tabular}} - \end{equation}\smallskip - - \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 - - \[ - @{text "C\<^sup>\ label\<^isub>1::ty"}\mbox{$'_1$} @{text "\ label\<^isub>l::ty"}\mbox{$'_l\;\;\;\;\;$} - @{text "binding_clauses"} - \]\smallskip - - \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 (see - \cite{Berghofer99}). If the types are polymorphic, we require the - type variables to stand for types that are finitely supported and over which - a permutation operation is defined. - The labels @{text "label"}$_{1..l}$ 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}: - - - \[\mbox{ - \begin{tabular}{@ {}l@ {}} - \isacommand{binds} {\it binders} \isacommand{in} {\it bodies}\\ - \isacommand{binds (set)} {\it binders} \isacommand{in} {\it bodies}\\ - \isacommand{binds (set+)} {\it binders} \isacommand{in} {\it bodies} - \end{tabular}} - \]\smallskip - - \noindent - The first mode is for binding lists of atoms (the order of bound atoms - 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{binds}-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: - - \[\mbox{ - \begin{tabular}{@ {}ll@ {}} - @{text "Foo\<^isub>1 x::name y::name t::trm s::trm"} & - \isacommand{binds} @{text "x y"} \isacommand{in} @{text "t s"}\\ - @{text "Foo\<^isub>2 x::name y::name t::trm s::trm"} & - \isacommand{binds} @{text "x y"} \isacommand{in} @{text "t"}, - \isacommand{binds} @{text "x y"} \isacommand{in} @{text "s"}\\ - \end{tabular}} - \]\smallskip - - \noindent - Similarly for the other binding modes. Interestingly, in case of - \isacommand{binds (set)} and \isacommand{binds (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 Ott. The main idea behind these restrictions is - that we obtain a 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. So for example - - \[\mbox{ - @{text "Foo x::name y::name t::trm"}\hspace{3mm} - \isacommand{binds} @{text "x"} \isacommand{in} @{text "t"}, - \isacommand{binds} @{text "y"} \isacommand{in} @{text "t"}} - \]\smallskip - - \noindent - is not allowed. 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{binds (set)} and \isacommand{binds (set+)} the - labels must either refer to atom types or to sets of atom types; in case of - \isacommand{binds} the labels must refer to atom types or to 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: - - \[\mbox{ - \begin{tabular}{@ {}c@ {\hspace{8mm}}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"}\hspace{3mm}% - \isacommand{binds} @{text x} \isacommand{in} @{text t}\\ - \\ - \end{tabular} & - \begin{tabular}{@ {}l@ {}} - \isacommand{nominal\_datatype}~@{text ty} $=$\\ - \hspace{2mm}\phantom{$\mid$}~@{text "TVar name"}\\ - \hspace{2mm}$\mid$~@{text "TFun ty ty"}\\ - \isacommand{and}~@{text "tsc ="}\\ - \hspace{2mm}\phantom{$\mid$}~@{text "TAll xs::(name fset) T::ty"}\hspace{3mm}% - \isacommand{binds (set+)} @{text xs} \isacommand{in} @{text T}\\ - \end{tabular} - \end{tabular}} - \]\smallskip - - - \noindent - In these specifications @{text "name"} refers to a (concrete) 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}, in which case all three binding modes coincide. However, having - \isacommand{binds (set)} or just \isacommand{binds} - 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{binds (set)} and - \isacommand{binds (set+)}) or a list of atoms (for \isacommand{binds}). They need - to 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 may be specified as: - - \begin{equation}\label{letpat} - \mbox{% - \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{binds} @{text x} \isacommand{in} @{text t}\\ - \hspace{5mm}$\mid$~@{text "Let_pat p::pat trm t::trm"} - \;\;\isacommand{binds} @{text "bn(p)"} \isacommand{in} @{text t}\\ - \isacommand{and} @{text pat} $=$\\ - \hspace{5mm}\phantom{$\mid$}~@{text "PVar name"}\\ - \hspace{5mm}$\mid$~@{text "PTup pat pat"}\\ - \isacommand{binder}~@{text "bn::pat \ atom list"}\\ - \isacommand{where}~@{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}\smallskip - - \noindent - In this specification the function @{text "bn"} determines which atoms of - the pattern @{text p} (fifth line) 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. - - For deep binders we allow binding clauses such as - - \[\mbox{ - \begin{tabular}{ll} - @{text "Bar p::pat t::trm"} & - \isacommand{binds} @{text "bn(p)"} \isacommand{in} @{text "p t"} \\ - \end{tabular}} - \]\smallskip - - - \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{% - \begin{tabular}{@ {}l@ {}l} - \isacommand{nominal\_datatype}~@{text "trm ="}\\ - \hspace{5mm}\phantom{$\mid$}~\ldots\\ - \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"} - & \hspace{-19mm}\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text t}\\ - \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"} - & \hspace{-19mm}\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\ - \isacommand{and} @{text "assn"} $=$\\ - \hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\ - \hspace{5mm}$\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}\smallskip - - \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 - - \[\mbox{ - \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}} - @{text "Baz\<^isub>1 p::pat t::trm"} & - \isacommand{binds} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text "p t"}\\ - @{text "Baz\<^isub>2 p::pat t\<^isub>1::trm t\<^isub>2::trm"} & - \isacommand{binds} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "p t\<^isub>1"}, - \isacommand{binds} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "p t\<^isub>2"}\\ - \end{tabular}} - \]\smallskip - - \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"}.\footnote{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. - Consider again the specification for @{text "trm"} and a contrived - version for assignments @{text "assn"}: - - \begin{equation}\label{bnexp} - \mbox{% - \begin{tabular}{@ {}l@ {}} - \isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\ - \isacommand{and} @{text "assn"} $=$\\ - \hspace{5mm}\phantom{$\mid$}~@{text "ANil'"}\\ - \hspace{5mm}$\mid$~@{text "ACons' x::name y::name t::trm assn"} - \;\;\isacommand{binds} @{text "y"} \isacommand{in} @{text t}\\ - \isacommand{binder} @{text "bn::assn \ atom list"}\\ - \isacommand{where}~@{text "bn(ANil') = []"}\\ - \hspace{5mm}$\mid$~@{text "bn(ACons' x y t as) = [atom x] @ bn(as)"}\\ - \end{tabular}} - \end{equation}\smallskip - - \noindent - In this example the term constructor @{text "ACons'"} has four arguments with - a binding clause involving two of them. This constructor is also used in the definition - of the binding function. The restriction we have to impose is that the - binding function can only return free atoms, that is the ones that are \emph{not} - mentioned in a binding clause. Therefore @{text "y"} cannot be used in the - binding function @{text "bn"} (since it is bound in @{text "ACons'"} by the - binding clause), but @{text x} can (since it is a free atom). This - restriction is sufficient for lifting the binding function to alpha-equated - terms. If we would permit @{text "bn"} to return @{text "y"}, - then it would not be respectful and therefore cannot be lifted to - alpha-equated lambda-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 ANil'}), a singleton set or - singleton list containing an atom (case @{text PVar} in \eqref{letpat}), or - unions of atom sets or appended atom lists (case @{text ACons'}). This - restriction will simplify some automatic definitions and proofs later on. - - To sum up this section, we introduced nominal datatype - specifications, which are like standard datatype specifications in - Isabelle/HOL but extended with binding clauses and specifications for binding - functions. Each constructor argument in our specification can also - have an optional label. These labels are used in the binding clauses - of a constructor; there can be several binding clauses for each - constructor, but bodies of binding clauses can only occur in a - single one. Binding clauses come in three modes: \isacommand{binds}, - \isacommand{binds (set)} and \isacommand{binds (set+)}. Binders - fall into two categories: shallow binders and deep binders. Shallow - binders can occur in more than one binding clause and only have to - respect the binding mode (i.e.~be of the right type). Deep binders - can also occur in more than one binding clause, unless they are - recursive in which case they can only occur once. Each of the deep - binders can only have a single binding function. Binding functions - are defined by recursion over a nominal datatype. They can - return the empty set, singleton atoms and unions of sets of atoms - (for binding modes \isacommand{binds (set)} and \isacommand{binds - (set+)}), and the empty list, singleton atoms and appended lists of - atoms (for mode \isacommand{bind}). However, they can only return - atoms that are not mentioned in any binding clause. - - In order to - simplify our definitions of free atoms and alpha-equivalence we define next, 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{binds}~@{term - "{}"}~\isacommand{in}~@{text "labels"}. In case of the lambda-terms, - the completion produces - - \[\mbox{ - \begin{tabular}{@ {}l@ {\hspace{-1mm}}} - \isacommand{nominal\_datatype} @{text lam} =\\ - \hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"} - \;\;\isacommand{binds}~@{term "{}"}~\isacommand{in}~@{text "x"}\\ - \hspace{5mm}$\mid$~@{text "App t\<^isub>1::lam t\<^isub>2::lam"} - \;\;\isacommand{binds}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>1 t\<^isub>2"}\\ - \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"} - \;\;\isacommand{binds}~@{text x} \isacommand{in} @{text t}\\ - \end{tabular}} - \]\smallskip - - \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{Cheney05,Pottier06}, 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 \mbox{@{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 given by the user. We also have to invent - new names for the types @{text "ty\<^sup>\"} and the term-constructors @{text "C\<^sup>\"}. - 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 of the raw type @{text "ty"}, - respectively @{text "C\<^sup>\"} is the corresponding term-constructor of @{text "ty\<^sup>\"}. - - 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 also define permutation operations by - recursion so that for each term constructor @{text "C"} we have that - - \begin{equation}\label{ceqvt} - @{text "\ \ (C z\<^isub>1 \ z\<^isub>n) = C (\ \ z\<^isub>1) \ (\ \ z\<^isub>n)"} - \end{equation}\smallskip - - \noindent - We will need this operation later when we define the notion of alpha-equivalence. - - The first non-trivial step we have to perform is the generation of - \emph{free-atom functions} from the specifications.\footnote{Admittedly, the - details of our definitions will be somewhat involved. However they are still - conceptually simple in comparison with the `positional' approach taken in - Ott \cite[Pages 88--95]{ott-jfp}, which uses the notions of \emph{occurrences} and - \emph{partial equivalence relations} over sets of occurrences.} For the - \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions - - \begin{equation}\label{fvars} - \mbox{@{text "fa_ty"}$_{1..n}$} - \end{equation}\smallskip - - \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 - - \[ - @{text "fa_bn"}\mbox{$_{1..m}$}. - \]\smallskip - - \noindent - The reason for this setup is that in a deep binder not all atoms have to be - bound, as we saw in \eqref{letrecs} with the example of `plain' @{text Let}s. We need - therefore functions that calculate those free atoms in deep binders. - - While the idea behind these free-atom functions is simple (they just - collect all atoms that are not bound), because of our rather complicated - binding mechanisms their definitions are somewhat involved. Given - a raw 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{binds (set)} (the other modes are similar). - Suppose a binding clause @{text bc\<^isub>i} is of the form - - \[ - \mbox{\isacommand{binds (set)} @{text "b\<^isub>1\b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\d\<^isub>q"}} - \]\smallskip - - \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 - - \begin{equation}\label{fadef} - \mbox{@{text "fa(bc\<^isub>i) \ (D - B) \ B'"}}. - \end{equation}\smallskip - - \noindent - The set @{text D} is formally defined as - - \[ - @{text "D \ fa_ty\<^isub>1 d\<^isub>1 \ ... \ fa_ty\<^isub>q d\<^isub>q"} - \]\smallskip - - \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; otherwise we set \mbox{@{text "fa_ty\<^isub>i \ supp"}}. The reason - for the latter is that @{text "ty"}$_i$ is not a type that is part of the specification, and - we assume @{text supp} is the generic function that characterises the free variables of - a type (in fact in the next section we will show that the free-variable functions we - define here, are equal to the support once lifted to alpha-equivalence classes). - - 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{equation}\label{bnaux}\mbox{ - \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} - @{text "bn\<^bsub>atom\<^esup> a"} & @{text "\"} & @{text "{atom a}"}\\ - @{text "bn\<^bsub>atom_set\<^esup> as"} & @{text "\"} & @{text "atoms as"}\\ - @{text "bn\<^bsub>atom_list\<^esub> as"} & @{text "\"} & @{text "atoms (set as)"} - \end{tabular}} - \end{equation}\smallskip - - \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} in \eqref{fadef} is then formally defined as - - \begin{equation}\label{bdef} - @{text "B \ bn_ty\<^isub>1 b\<^isub>1 \ ... \ bn_ty\<^isub>p b\<^isub>p"} - \end{equation}\smallskip - - \noindent - where we use the auxiliary binding functions from \eqref{bnaux} for shallow - binders (that means when @{text "ty"}$_i$ is of type @{text "atom"}, @{text "atom set"} or - @{text "atom list"}). - - The set @{text "B'"} in \eqref{fadef} collects all free atoms in - non-recursive deep binders. Let us assume these binders in the binding - clause @{text "bc\<^isub>i"} are - - \[ - \mbox{@{text "bn\<^isub>1 l\<^isub>1, \, bn\<^isub>r l\<^isub>r"}} - \]\smallskip - - \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 - - \begin{equation}\label{bprimedef} - @{text "B' \ fa_bn\<^isub>1 l\<^isub>1 \ ... \ fa_bn\<^isub>r l\<^isub>r"} - \end{equation}\smallskip - - \noindent - This completes all clauses for 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}$. The - definition for those functions needs to be extracted from the clauses the - user provided for @{text "bn"}$_{1..m}$ Assume the user specified a @{text - bn}-clause of the form - - \[ - @{text "bn (C z\<^isub>1 \ z\<^isub>s) = rhs"} - \]\smallskip - - \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: - - \[\mbox{ - \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),\smallskip\\ - $\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"}\\ - & (that means whatever is `left over' from the @{text "bn"}-function is free)\smallskip\\ - $\bullet$ & @{term "{}"} provided @{text "z\<^isub>i"} occurs in @{text "rhs"}, - but without a recursive call\\ - & (that means @{text "z\<^isub>i"} is supposed to become bound by the binding function)\\ - \end{tabular}} - \]\smallskip - - \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: - - \[\mbox{ - \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)"}\smallskip\\ - - @{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)"}\smallskip\\ - - @{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}} - \]\smallskip - - - \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. - - Having the free-atom functions at our disposal, we can next define the - alpha-equivalence relations for the raw types @{text - "ty"}$_{1..n}$. We write them as - - \[ - \mbox{@{text "\ty"}$_{1..n}$}. - \]\smallskip - - \noindent - Like with the free-atom functions, we also need to - define auxiliary alpha-equivalence relations - - \[ - \mbox{@{text "\bn\<^isub>"}$_{1..m}$} - \]\smallskip - - \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. - - \[\mbox{ - \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} - @{text "(x\<^isub>1,\, x\<^isub>n) (R\<^isub>1,\, R\<^isub>n) (y\<^isub>1,\, y\<^isub>n)"} & @{text "\"} & - @{text "x\<^isub>1 R\<^isub>1 y\<^isub>1 \ \ \ x\<^isub>n R\<^isub>n y\<^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}} - \]\smallskip - - - 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{equation}\label{gform} - \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{equation}\smallskip - - \noindent - The task below is to specify what the premises corresponding to a binding - clause are. To understand better what the general pattern is, let us first - treat the special instance where @{text "bc\<^isub>i"} is the empty binding clause - of the form - - \[ - \mbox{\isacommand{binds (set)} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\d\<^isub>q"}.} - \]\smallskip - - \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 some of the arguments @{text - "z"}$_{1..n}$ and respectively @{text "d\"}$_{1..q}$ to some of the @{text - "z\"}$_{1..n}$ in \eqref{gform}. 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}\smallskip - - \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} and have type @{text "ty\<^isub>i"}; otherwise - we take @{text "R\<^isub>i"} to be the equality @{text "="}. Again the - latter is because @{text "ty\<^isub>i"} is then not part of the specified types - and alpha-equivalence of any previously defined type is supposed to coincide - with equality. This lets us now 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 - - \[ - @{text "d\<^isub>1 R\<^isub>1 d\\<^isub>1 \ d\<^isub>q R\<^isub>q d\\<^isub>q"}. - \]\smallskip - - \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{binds (set)} @{text "b\<^isub>1\b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\d\<^isub>q"}.} - \end{equation}\smallskip - - \noindent - In this case we define a premise @{text P} using the relation - $\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$ given in Section~\ref{sec:binders} (similarly - $\approx_{\,\textit{set+}}^{\textit{R}, \textit{fa}}$ and - $\approx_{\,\textit{list}}^{\textit{R}, \textit{fa}}$ for the other - binding modes). 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}}^{\textit{R}, \textit{fa}}$ we also need - a compound free-atom function for the bodies defined as - - \[ - \mbox{@{text "fa \ (fa_ty\<^isub>1,\, fa_ty\<^isub>q)"}} - \]\smallskip - - \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 - - \[ - @{text "B \ bn_ty\<^isub>1 b\<^isub>1 \ \ \ bn_ty\<^isub>p b\<^isub>p"}\;.\\ - \]\smallskip - - \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: - - \[ - \mbox{@{term "P \ alpha_set_ex (B, D) R fa (B', D')"}}\;. - \]\smallskip - - \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 define shortly). Let us assume the non-recursive deep binders - in @{text "bc\<^isub>i"} are - - \[ - @{text "bn\<^isub>1 l\<^isub>1, \, bn\<^isub>r l\<^isub>r"}. - \]\smallskip - - \noindent - The tuple @{text L} consists then of all these binders @{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 - - \[ - @{text "prems(bc\<^isub>i) \ P \ L R' L'"} - \]\smallskip - - \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 - - \[ - @{text "bn (C z\<^isub>1 \ z\<^isub>s) = rhs"} - \]\smallskip - - \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 - - \[ - \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"}}} - \]\smallskip - - \noindent - In this clause the relations @{text "R"}$_{1..s}$ are given by - - \[\mbox{ - \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},\smallskip\\ - $\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},\smallskip\\ - $\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\smallskip\\ - $\bullet$ & @{text True} provided @{text "z\<^isub>i"} occurs in @{text rhs} but without a - recursive call. - \end{tabular}} - \]\smallskip - - \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}}^{\textit{R}, \textit{fa}}$ and take @{text "0"} - for the existentially quantified permutation). - - Again let us take a look at a concrete example for these definitions. For - the specification shown in \eqref{letrecs} - we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and - $\approx_{\textit{bn}}$ with the following rules: - - \begin{equation}\label{rawalpha}\mbox{ - \begin{tabular}{@ {}c @ {}} - \infer{@{text "Let as t \\<^bsub>trm\<^esub> Let as' t'"}} - {@{term "alpha_lst_ex (bn as, t) alpha_trm fa_trm (bn as', t')"} & - \hspace{5mm}@{text "as \\<^bsub>bn\<^esub> as'"}}\\ - \\ - \makebox[0mm]{\infer{@{text "Let_rec as t \\<^bsub>trm\<^esub> Let_rec as' t'"}} - {@{term "alpha_lst_ex (bn as, ast) alpha_trm2 fa_trm2 (bn as', ast')"}}}\\ - \\ - - \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'"} & \hspace{5mm}@{text "t \\<^bsub>trm\<^esub> t'"} & \hspace{5mm}@{text "as \\<^bsub>assn\<^esub> as'"}} - \end{tabular}\\ - \\ - - \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'"} & \hspace{5mm}@{text "as \\<^bsub>bn\<^esub> as'"}} - \end{tabular} - \end{tabular}} - \end{equation}\smallskip - - \noindent - Notice 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. - Note also that in case of more than one body (that is in the @{text "Let_rec"}-case above) - we need to parametrise the relation $\approx_{\textit{list}}$ with a compound - equivalence relation and a compound free-atom function. This is because the - corresponding binding clause specifies a binder with two bodies, namely - @{text "as"} and @{text "t"}. -*} - -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 - give in this section and the next the proofs we need for establishing this - infrastructure. One point of our work is that we have completely - automated these proofs in Isabelle/HOL. - - First we establish that the free-variable functions, the binding functions and the - alpha-equi\-va\-lences are equivariant. - - \begin{lem}\mbox{}\\ - @{text "(i)"} The functions @{text "fa_ty"}$_{1..n}$, @{text "fa_bn"}$_{1..m}$ and - @{text "bn"}$_{1..m}$ are equivariant.\\ - @{text "(ii)"} The relations @{text "\ty"}$_{1..n}$ and - @{text "\bn"}$_{1..m}$ are equivariant. - \end{lem} - - \begin{proof} - The function package of Isabelle/HOL allows us to prove the first part by - mutual induction over the definitions of the functions.\footnote{We have - that the free-atom functions are terminating. From this the function - package derives an induction principle~\cite{Krauss09}.} The second is by a - straightforward induction over the rules of @{text "\ty"}$_{1..n}$ and - @{text "\bn"}$_{1..m}$ using the first part. - \end{proof} - - \noindent - Next we establish that the alpha-equivalence relations defined in the - previous section are indeed equivalence relations. - - \begin{lem}\label{equiv} - The relations @{text "\ty"}$_{1..n}$ and @{text "\bn"}$_{1..m}$ are - equivalence relations. - \end{lem} - - \begin{proof} - The proofs are by induction. 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}. However, the transitivity - case needs in addition the fact that the relations are equivariant. - \end{proof} - - \noindent - We can feed the last 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 the property - - \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}\smallskip - - \noindent - whenever @{text "C"}$^\alpha$~@{text "\"}~@{text "D"}$^\alpha$. - In order to derive this property, 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}\smallskip - - \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}). - Given, for example, @{text "C"} is of type @{text "ty"} with argument types - @{text "ty"}$_{1..r}$, respectfulness amounts to showing that - - \[\mbox{ - @{text "C x\<^isub>1 \ x\<^isub>r \ty C x\\<^isub>1 \ x\\<^isub>r"} - }\]\smallskip - - \noindent - holds under the assumptions \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 - (similarly for @{text "D"}). For this we have to show - by induction over the definitions of alpha-equivalences the following - auxiliary implications - - \begin{equation}\label{fnresp}\mbox{ - \begin{tabular}{lll} - @{text "x \ty\<^isub>i x'"} & implies & @{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x'"}\\ - @{text "x \ty\<^isub>l x'"} & implies & @{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x'"}\\ - @{text "x \ty\<^isub>l x'"} & implies & @{text "bn\<^isub>j x = bn\<^isub>j x'"}\\ - @{text "x \ty\<^isub>l x'"} & implies & @{text "x \bn\<^isub>j x'"}\\ - \end{tabular} - }\end{equation}\smallskip - - \noindent - whereby @{text "ty\<^isub>l"} is the type over which @{text "bn\<^isub>j"} - is defined. 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} - to return 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 in general 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}. - - 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, which - we already established in Lemma~\ref{equiv}. As a result we can add the - equations - - \begin{equation}\label{calphaeqvt} - @{text "\ \ (C\<^sup>\ x\<^isub>1 \ x\<^isub>r) = C\<^sup>\ (\ \ x\<^isub>1) \ (\ \ x\<^isub>r)"} - \end{equation}\smallskip - - \noindent - to our infrastructure. In a similar fashion we can lift the defining equations - of the free-atom functions @{text "fa_ty\"}$_{1..n}$ and - @{text "fa_bn\"}$_{1..m}$ as well as of the binding functions @{text - "bn\"}$_{1..m}$ and 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. - - We also need to lift the properties that characterise when two raw terms of the form - - \[ - \mbox{@{text "C x\<^isub>1 \ x\<^isub>r \ty C x\\<^isub>1 \ x\\<^isub>r"}} - \]\smallskip - - \noindent - are alpha-equivalent. This gives us conditions when the corresponding - alpha-equated terms are \emph{equal}, namely - - \[ - @{text "C\<^sup>\ x\<^isub>1 \ x\<^isub>r = C\<^sup>\ x\\<^isub>1 \ x\\<^isub>r"}. - \]\smallskip - - \noindent - We call these conditions \emph{quasi-injectivity}. They correspond to the - premises in our alpha-equiva\-lence relations, except that the - relations @{text "\ty"}$_{1..n}$ are all replaced by equality (and similarly - the free-atom and binding functions are replaced by their lifted - counterparts). Recall the alpha-equivalence rules for @{text "Let"} and - @{text "Let_rec"} shown in \eqref{rawalpha}. For @{text "Let\<^sup>\"} and - @{text "Let_rec\<^sup>\"} we have - - \begin{equation}\label{alphalift}\mbox{ - \begin{tabular}{@ {}c @ {}} - \infer{@{text "Let\<^sup>\ as t = Let\<^sup>\ as' t'"}} - {@{term "alpha_lst_ex (bn_al as, t) equal fa_trm_al (bn as', t')"} & - \hspace{5mm}@{text "as \\\<^bsub>bn\<^esub> as'"}}\\ - \\ - \makebox[0mm]{\infer{@{text "Let_rec\<^sup>\ as t = Let_rec\<^sup>\ as' t'"}} - {@{term "alpha_lst_ex (bn_al as, ast) equ2 fa_trm2_al (bn_al as', ast')"}}}\\ - \end{tabular}} - \end{equation}\smallskip - - We can also add to our infrastructure cases lemmas and a (mutual) - induction principle for the types @{text "ty\"}$_{1..n}$. The cases - lemmas allow the user to deduce a property @{text "P"} by exhaustively - analysing how an element of a type, say @{text "ty\"}$_i$, can be - constructed (that means one case for each of the term-constructors in @{text - "ty\"}$_i\,$). The lifted cases lemma for a type @{text - "ty\"}$_i\,$ looks as follows - - \begin{equation}\label{cases} - \infer{P} - {\begin{array}{l} - @{text "\x\<^isub>1\x\<^isub>k. y = C\\<^isub>1 x\<^isub>1 \ x\<^isub>k \ P"}\\ - \hspace{5mm}\vdots\\ - @{text "\x\<^isub>1\x\<^isub>l. y = C\\<^isub>m x\<^isub>1 \ x\<^isub>l \ P"}\\ - \end{array}} - \end{equation}\smallskip - - \noindent - where @{text "y"} is a variable of type @{text "ty\"}$_i$ and @{text "P"} is the - property that is established by the case analysis. Similarly, we have a (mutual) - induction principle for the types @{text "ty\"}$_{1..n}$, which is of the - form - - \begin{equation}\label{induct} - \infer{@{text "P\<^isub>1 y\<^isub>1 \ \ \ P\<^isub>n y\<^isub>n "}} - {\begin{array}{l} - @{text "\x\<^isub>1\x\<^isub>k. P\<^isub>i x\<^isub>i \ \ \ P\<^isub>j x\<^isub>j \ P (C\\<^isub>1 x\<^isub>1 \ x\<^isub>k)"}\\ - \hspace{5mm}\vdots\\ - @{text "\x\<^isub>1\x\<^isub>l. P\<^isub>r x\<^isub>r \ \ \ P\<^isub>s x\<^isub>s \ P (C\\<^isub>m x\<^isub>1 \ x\<^isub>l)"}\\ - \end{array}} - \end{equation}\smallskip - - \noindent - whereby the @{text P}$_{1..n}$ are the properties established by the - induction, and the @{text y}$_{1..n}$ are of type @{text - "ty\"}$_{1..n}$. Note that for the term constructor @{text - "C"}$^\alpha_1$ the induction principle has a hypothesis of the form - - \[ - \mbox{@{text "\x\<^isub>1\x\<^isub>k. P\<^isub>i x\<^isub>i \ \ \ P\<^isub>j x\<^isub>j \ P (C\\<^sub>1 x\<^isub>1 \ x\<^isub>k)"}} - \]\smallskip - - \noindent - in which the @{text "x"}$_{i..j}$ @{text "\"} @{text "x"}$_{1..k}$ are the - recursive arguments of this term constructor (similarly for the other - term-constructors). - - Recall the lambda-calculus with @{text "Let"}-patterns shown in - \eqref{letpat}. The cases lemmas and the induction principle shown in - \eqref{cases} and \eqref{induct} boil down in that example to the following three inference - rules: - - \begin{equation}\label{inductex}\mbox{ - \begin{tabular}{c} - \multicolumn{1}{@ {\hspace{-5mm}}l}{cases lemmas:}\smallskip\\ - \infer{@{text "P\<^bsub>trm\<^esub>"}} - {\begin{array}{@ {}l@ {}} - @{text "\x. y = Var\<^sup>\ x \ P\<^bsub>trm\<^esub>"}\\ - @{text "\x\<^isub>1 x\<^isub>2. y = App\<^sup>\ x\<^isub>1 x\<^isub>2 \ P\<^bsub>trm\<^esub>"}\\ - @{text "\x\<^isub>1 x\<^isub>2. y = Lam\<^sup>\ x\<^isub>1 x\<^isub>2 \ P\<^bsub>trm\<^esub>"}\\ - @{text "\x\<^isub>1 x\<^isub>2 x\<^isub>3. y = Let_pat\<^sup>\ x\<^isub>1 x\<^isub>2 x\<^isub>3 \ P\<^bsub>trm\<^esub>"} - \end{array}}\hspace{10mm} - - \infer{@{text "P\<^bsub>pat\<^esub>"}} - {\begin{array}{@ {}l@ {}} - @{text "\x. y = PVar\<^sup>\ x \ P\<^bsub>pat\<^esub>"}\\ - @{text "\x\<^isub>1 x\<^isub>2. y = PTup\<^sup>\ x\<^isub>1 x\<^isub>2 \ P\<^bsub>pat\<^esub>"} - \end{array}}\medskip\\ - - \multicolumn{1}{@ {\hspace{-5mm}}l}{induction principle:}\smallskip\\ - - \infer{@{text "P\<^bsub>trm\<^esub> y\<^isub>1 \ P\<^bsub>pat\<^esub> y\<^isub>2"}} - {\begin{array}{@ {}l@ {}} - @{text "\x. P\<^bsub>trm\<^esub> (Var\<^sup>\ x)"}\\ - @{text "\x\<^isub>1 x\<^isub>2. P\<^bsub>trm\<^esub> x\<^isub>1 \ P\<^bsub>trm\<^esub> x\<^isub>2 \ P\<^bsub>trm\<^esub> (App\<^sup>\ x\<^isub>1 x\<^isub>2)"}\\ - @{text "\x\<^isub>1 x\<^isub>2. P\<^bsub>trm\<^esub> x\<^isub>2 \ P\<^bsub>trm\<^esub> (Lam\<^sup>\ x\<^isub>1 x\<^isub>2)"}\\ - @{text "\x\<^isub>1 x\<^isub>2 x\<^isub>3. P\<^bsub>pat\<^esub> x\<^isub>1 \ P\<^bsub>trm\<^esub> x\<^isub>2 \ P\<^bsub>trm\<^esub> x\<^isub>3 \ P\<^bsub>trm\<^esub> (Let_pat\<^sup>\ x\<^isub>1 x\<^isub>2 x\<^isub>3)"}\\ - @{text "\x. P\<^bsub>pat\<^esub> (PVar\<^sup>\ x)"}\\ - @{text "\x\<^isub>1 x\<^isub>2. P\<^bsub>pat\<^esub> x\<^isub>1 \ P\<^bsub>pat\<^esub> x\<^isub>2 \ P\<^bsub>pat\<^esub> (PTup\<^sup>\ x\<^isub>1 x\<^isub>2)"} - \end{array}} - \end{tabular}} - \end{equation}\smallskip - - By working now completely on the alpha-equated level, we - can first show using \eqref{calphaeqvt} and Property~\ref{swapfreshfresh} that the support of each term - constructor is included in the support of its arguments, - namely - - \[ - @{text "(supp x\<^isub>1 \ \ \ supp x\<^isub>r) supports (C\<^sup>\ x\<^isub>1 \ x\<^isub>r)"} - \]\smallskip - - \noindent - This allows us to prove using the induction principle for @{text "ty\"}$_{1..n}$ - that every element of type @{text "ty\"}$_{1..n}$ is finitely supported - (using Proposition~\ref{supportsprop}{\it (i)}). - Similarly, we can establish by induction that the free-atom functions and binding - functions are equivariant, namely - - \[\mbox{ - \begin{tabular}{rcl} - @{text "\ \ (fa_ty\\<^isub>i x)"} & $=$ & @{text "fa_ty\\<^isub>i (\ \ x)"}\\ - @{text "\ \ (fa_bn\\<^isub>j x)"} & $=$ & @{text "fa_bn\\<^isub>j (\ \ x)"}\\ - @{text "\ \ (bn\\<^isub>j x)"} & $=$ & @{text "bn\\<^isub>j (\ \ x)"}\\ - \end{tabular}} - \]\smallskip - - - \noindent - Lastly, we can show that the support of elements in @{text - "ty\"}$_{1..n}$ is the same as the free-atom functions @{text - "fa_ty\"}$_{1..n}$. This fact is important in the nominal setting where - the general theory is formulated in terms of support and freshness, but also - provides evidence that our notions of free-atoms and alpha-equivalence - `match up' correctly. - - \begin{thm}\label{suppfa} - 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{thm} - - \begin{proof} - The proof is by induction on @{text "x"}$_{1..n}$. 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 then the facts derived in Theorem~\ref{suppabs}, - for which we have to know that every body of an abstraction is finitely supported. - This, we have proved earlier. - \end{proof} - - \noindent - Consequently, we can replace the free-atom functions by @{text "supp"} in - our quasi-injection lemmas. In the examples shown in \eqref{alphalift}, for instance, - we obtain for @{text "Let\<^sup>\"} and @{text "Let_rec\<^sup>\"} - - \[\mbox{ - \begin{tabular}{@ {}c @ {}} - \infer{@{text "Let\<^sup>\ as t = Let\<^sup>\ as' t'"}} - {@{term "alpha_lst_ex (bn_al as, t) equal supp (bn_al as', t')"} & - \hspace{5mm}@{text "as \\\<^bsub>bn\<^esub> as'"}}\\ - \\ - \makebox[0mm]{\infer{@{text "Let_rec\<^sup>\ as t = Let_rec\<^sup>\ as' t'"}} - {@{term "alpha_lst_ex (bn_al as, ast) equ2 supp2 (bn_al as', ast')"}}}\\ - \end{tabular}} - \]\smallskip - - \noindent - Taking into account that the compound equivalence relation @{term - "equ2"} and the compound free-atom function @{term "supp2"} are by - definition equal to @{term "equal"} and @{term "supp"}, respectively, the - above rules simplify further to - - \[\mbox{ - \begin{tabular}{@ {}c @ {}} - \infer{@{text "Let\<^sup>\ as t = Let\<^sup>\ as' t'"}} - {@{term "Abs_lst (bn_al as) t = Abs_lst (bn_al as') t'"} & - \hspace{5mm}@{text "as \\\<^bsub>bn\<^esub> as'"}}\\ - \\ - \makebox[0mm]{\infer{@{text "Let_rec\<^sup>\ as t = Let_rec\<^sup>\ as' t'"}} - {@{term "Abs_lst (bn_al as) ast = Abs_lst (bn_al as') ast'"}}}\\ - \end{tabular}} - \]\smallskip - - \noindent - which means we can characterise equality between term-constructors (on the - alpha-equated level) in terms of equality between the abstractions defined - in Section~\ref{sec:binders}. From this we can deduce the support for @{text - "Let\<^sup>\"} and @{text "Let_rec\<^sup>\"}, namely - - - \[\mbox{ - \begin{tabular}{l@ {\hspace{2mm}}l@ {\hspace{2mm}}l} - @{text "supp (Let\<^sup>\ as t)"} & @{text "="} & @{text "(supp t - set (bn\<^sup>\ as)) \ fa\\<^bsub>bn\<^esub> as"}\\ - @{text "supp (Let_rec\<^sup>\ as t)"} & @{text "="} & @{text "(supp t \ supp as) - set (bn\<^sup>\ as)"}\\ - \end{tabular}} - \]\smallskip - - \noindent - using the support of abstractions derived in Theorem~\ref{suppabs}. - - To sum up this section, we have established 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 proving facts about - these lifted definitions. All necessary proofs are generated automatically - by custom ML-code. -*} - - -section {* Strong Induction Principles *} - -text {* - In the previous section we derived induction principles for alpha-equated - terms (see \eqref{induct} for the general form and \eqref{inductex} for an - example). This was done by lifting the corresponding inductions principles - for `raw' terms. We already employed these induction principles for - deriving several facts about alpha-equated terms, including the property that - the free-atom functions and the notion of support coincide. Still, we - call these induction principles \emph{weak}, because for a term-constructor, - say \mbox{@{text "C\<^sup>\ x\<^isub>1\x\<^isub>r"}}, the induction - hypothesis requires us to establish (under some assumptions) a property - @{text "P (C\<^sup>\ x\<^isub>1\x\<^isub>r)"} for \emph{all} @{text - "x"}$_{1..r}$. The problem with this is that in the presence of binders we cannot make - any assumptions about the atoms that are bound---for example assuming the variable convention. - One obvious way around this - problem is to rename bound atoms. Unfortunately, this leads to very clunky proofs - and makes formalisations grievous experiences (especially in the context of - multiple bound atoms). - - For the older versions of Nominal Isabelle we described in \cite{Urban08} a - method for automatically strengthening weak induction principles. These - stronger induction principles allow the user to make additional assumptions - about bound atoms. The advantage of these assumptions is that they make in - most cases any renaming of bound atoms unnecessary. To explain how the - strengthening works, we use as running example the lambda-calculus with - @{text "Let"}-patterns shown in \eqref{letpat}. Its weak induction principle - is given in \eqref{inductex}. The stronger induction principle is as - follows: - - \begin{equation}\label{stronginduct} - \mbox{ - \begin{tabular}{@ {}c@ {}} - \infer{@{text "P\<^bsub>trm\<^esub> c y\<^isub>1 \ P\<^bsub>pat\<^esub> c y\<^isub>2"}} - {\begin{array}{l} - @{text "\x c. P\<^bsub>trm\<^esub> c (Var\<^sup>\ x)"}\\ - @{text "\x\<^isub>1 x\<^isub>2 c. (\d. P\<^bsub>trm\<^esub> d x\<^isub>1) \ (\d. P\<^bsub>trm\<^esub> d x\<^isub>2) \ P\<^bsub>trm\<^esub> c (App\<^sup>\ x\<^isub>1 x\<^isub>2)"}\\ - @{text "\x\<^isub>1 x\<^isub>2 c. atom x\<^isub>1 # c \ (\d. P\<^bsub>trm\<^esub> d x\<^isub>2) \ P\<^bsub>trm\<^esub> c (Lam\<^sup>\ x\<^isub>1 x\<^isub>2)"}\\ - @{text "\x\<^isub>1 x\<^isub>2 x\<^isub>3 c. (set (bn\<^sup>\ x\<^isub>1)) #\<^sup>* c \"}\\ - \hspace{10mm}@{text "(\d. P\<^bsub>pat\<^esub> d x\<^isub>1) \ (\d. P\<^bsub>trm\<^esub> d x\<^isub>2) \ (\d. P\<^bsub>trm\<^esub> d x\<^isub>3) \ P\<^bsub>trm\<^esub> c (Let_pat\<^sup>\ x\<^isub>1 x\<^isub>2 x\<^isub>3)"}\\ - @{text "\x c. P\<^bsub>pat\<^esub> c (PVar\<^sup>\ x)"}\\ - @{text "\x\<^isub>1 x\<^isub>2 c. (\d. P\<^bsub>pat\<^esub> d x\<^isub>1) \ (\d. P\<^bsub>pat\<^esub> d x\<^isub>2) \ P\<^bsub>pat\<^esub> c (PTup\<^sup>\ x\<^isub>1 x\<^isub>2)"} - \end{array}} - \end{tabular}} - \end{equation}\smallskip - - - \noindent - Notice that instead of establishing two properties of the form @{text " - P\<^bsub>trm\<^esub> y\<^isub>1 \ P\<^bsub>pat\<^esub> y\<^isub>2"}, as the - weak one does, the stronger induction principle establishes the properties - of the form @{text " P\<^bsub>trm\<^esub> c y\<^isub>1 \ - P\<^bsub>pat\<^esub> c y\<^isub>2"} in which the additional parameter @{text - c} is assumed to be of finite support. The purpose of @{text "c"} is to - `control' which freshness assumptions the binders should satisfy in the - @{text "Lam\<^sup>\"} and @{text "Let_pat\<^sup>\"} cases: for @{text - "Lam\<^sup>\"} we can assume the bound atom @{text "x\<^isub>1"} is fresh - for @{text "c"} (third line); for @{text "Let_pat\<^sup>\"} we can assume - all bound atoms from an assignment are fresh for @{text "c"} (fourth - line). In order to see how an instantiation for @{text "c"} in the - conclusion `controls' the premises, one has to take into account that - Isabelle/HOL is a typed logic. That means if @{text "c"} is instantiated - with, for example, a pair, then this type-constraint will be propagated to - the premises. The main point is that if @{text "c"} is instantiated - appropriately, then the user can mimic the usual convenient `pencil-and-paper' - reasoning employing the variable convention about bound and free variables - being distinct \cite{Urban08}. - - In what follows we will show that the weak induction principle in - \eqref{inductex} implies the strong one \eqref{stronginduct}. This fact was established for - single binders in \cite{Urban08} by some quite involved, nevertheless - automated, induction proof. In this paper we simplify the proof by - leveraging the automated proving tools from the function package of - Isabelle/HOL \cite{Krauss09}. The reasoning principle behind these tools - 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 (one for - each type @{text "ty"}$^\alpha_{1..n}$) that decrease in every induction - step and the other is that we have covered all cases in the induction - principle. Once these two proof obligations are discharged, the reasoning - infrastructure of the function package will automatically derive the - stronger induction principle. This way of establishing the stronger induction - principle is considerably simpler than the earlier work presented in \cite{Urban08}. - - As measures we can 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 the sizes decrease in every - induction step. What is left to show is that we covered all cases. - To do so, we have to derive stronger cases lemmas, which look in our - running example as follows: - - \[\mbox{ - \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}} - \infer{@{text "P\<^bsub>trm\<^esub>"}} - {\begin{array}{@ {}l@ {}} - @{text "\x. y = Var\<^sup>\ x \ P\<^bsub>trm\<^esub>"}\\ - @{text "\x\<^isub>1 x\<^isub>2. y = App\<^sup>\ x\<^isub>1 x\<^isub>2 \ P\<^bsub>trm\<^esub>"}\\ - @{text "\x\<^isub>1 x\<^isub>2. atom x\<^isub>1 # c \ y = Lam\<^sup>\ x\<^isub>1 x\<^isub>2 \ P\<^bsub>trm\<^esub>"}\\ - @{text "\x\<^isub>1 x\<^isub>2 x\<^isub>3. set (bn\<^sup>\ x\<^isub>1) #\<^sup>* c \ y = Let_pat\<^sup>\ x\<^isub>1 x\<^isub>2 x\<^isub>3 \ P\<^bsub>trm\<^esub>"} - \end{array}} & - - \infer{@{text "P\<^bsub>pat\<^esub>"}} - {\begin{array}{@ {}l@ {}} - @{text "\x. y = PVar\<^sup>\ x \ P\<^bsub>pat\<^esub>"}\\ - @{text "\x\<^isub>1 x\<^isub>2. y = PTup\<^sup>\ x\<^isub>1 x\<^isub>2 \ P\<^bsub>pat\<^esub>"} - \end{array}} - \end{tabular}} - \]\smallskip - - \noindent - They are stronger in the sense that they allow us to assume in the @{text - "Lam\<^sup>\"} and @{text "Let_pat\<^sup>\"} cases that the bound atoms - avoid, or are fresh for, a context @{text "c"} (which is assumed to be finitely supported). - - These stronger cases lemmas can be derived from the `weak' cases lemmas - given in \eqref{inductex}. This is trivial in case of patterns (the one on - the right-hand side) since the weak and strong cases lemma coincide (there - is no binding in patterns). Interesting are only the cases for @{text - "Lam\<^sup>\"} and @{text "Let_pat\<^sup>\"}, where we have some binders and - therefore have an additional assumption about avoiding @{text "c"}. Let us - first establish the case for @{text "Lam\<^sup>\"}. By the weak cases lemma - \eqref{inductex} we can assume that - - \begin{equation}\label{assm} - @{text "y = Lam\<^sup>\ x\<^isub>1 x\<^isub>2"} - \end{equation}\smallskip - - \noindent - holds, and need to establish @{text "P\<^bsub>trm\<^esub>"}. The stronger cases lemma has the - corresponding implication - - \begin{equation}\label{imp} - @{text "\x\<^isub>1 x\<^isub>2. atom x\<^isub>1 # c \ y = Lam\<^sup>\ x\<^isub>1 x\<^isub>2 \ P\<^bsub>trm\<^esub>"} - \end{equation}\smallskip - - \noindent - which we must use in order to infer @{text "P\<^bsub>trm\<^esub>"}. Clearly, we cannot - use this implication directly, because we have no information whether or not @{text - "x\<^isub>1"} is fresh for @{text "c"}. However, we can use Properties - \ref{supppermeq} and \ref{avoiding} to rename @{text "x\<^isub>1"}. We know - by Theorem~\ref{suppfa} that @{text "{atom x\<^isub>1} #\<^sup>* Lam\<^sup>\ - x\<^isub>1 x\<^isub>2"} (since its support is @{text "supp x\<^isub>2 - - {atom x\<^isub>1}"}). Property \ref{avoiding} provides us then with a - permutation @{text "\"}, such that @{text "{atom (\ \ x\<^isub>1)} #\<^sup>* - c"} and \mbox{@{text "supp (Lam\<^sup>\ x\<^isub>1 x\<^isub>2) #\<^sup>* \"}} hold. - By using Property \ref{supppermeq}, we can infer from the latter that - - \[ - @{text "Lam\<^sup>\ (\ \ x\<^isub>1) (\ \ x\<^isub>2) = Lam\<^sup>\ x\<^isub>1 x\<^isub>2"} - \]\smallskip - - \noindent - holds. We can use this equation in the assumption \eqref{assm}, and hence - use the implication \eqref{imp} with the renamed @{text "\ \ x\<^isub>1"} - and @{text "\ \ x\<^isub>2"} for concluding this case. - - The @{text "Let_pat\<^sup>\"}-case involving a deep binder is slightly more complicated. - We have the assumption - - \begin{equation}\label{assmtwo} - @{text "y = Let_pat\<^sup>\ x\<^isub>1 x\<^isub>2 x\<^isub>3"} - \end{equation}\smallskip - - \noindent - and the implication from the stronger cases lemma - - \begin{equation}\label{impletpat} - @{text "\x\<^isub>1 x\<^isub>2 x\<^isub>3. set (bn\<^sup>\ x\<^isub>1) #\<^sup>* c \ y = Let_pat\<^sup>\ x\<^isub>1 x\<^isub>2 x\<^isub>3 \ P\<^bsub>trm\<^esub>"} - \end{equation}\smallskip - - \noindent - The reason that this case is more complicated is that we cannot directly apply Property - \ref{avoiding} for obtaining a renaming permutation. Property \ref{avoiding} requires - that the binders are fresh for the term in which we want to perform the renaming. But - this is not true in terms such as (using an informal notation) - - \[ - @{text "Let (x, y) := (x, y) in (x, y)"} - \]\smallskip - - \noindent - where @{text x} and @{text y} are bound in the term, but are also free - in the right-hand side of the assignment. We can, however, obtain such a renaming permutation, say - @{text "\"}, for the abstraction @{term "Abs_lst (bn_al x\<^isub>1) - x\<^isub>3"}. As a result we have \mbox{@{term "set (bn_al (\ \ x\<^isub>1)) - \* c"}} and @{term "Abs_lst (bn_al (\ \ x\<^isub>1)) (\ \ x\<^isub>3) = - Abs_lst (bn_al x\<^isub>1) x\<^isub>3"} (remember @{text "set"} and @{text - "bn\<^sup>\"} are equivariant). Now the quasi-injective property for @{text - "Let_pat\<^sup>\"} states that - - \[ - \infer{@{text "Let_pat\<^sup>\ p t\<^isub>1 t\<^isub>2 = Let_pat\<^sup>\ p\ t\\<^isub>1 t\\<^isub>2"}} - {@{text "[bn\<^sup>\ p]\<^bsub>list\<^esub>. t\<^isub>2 = [bn\<^sup>\ p']\<^bsub>list\<^esub>. t\\<^isub>2"}\;\; & - @{text "p \\\<^bsub>bn\<^esub> p\"}\;\; & @{text "t\<^isub>1 = t\\<^isub>1"}} - \]\smallskip - - \noindent - Since all atoms in a pattern are bound by @{text "Let_pat\<^sup>\"}, we can infer - that @{text "(\ \ x\<^isub>1) \\\<^bsub>bn\<^esub> x\<^isub>1"} holds for every @{text "\"}. Therefore we have that - - \[ - @{text "Let_pat\<^sup>\ (\ \ x\<^isub>1) x\<^isub>2 (\ \ x\<^isub>3) = Let_pat\<^sup>\ x\<^isub>1 x\<^isub>2 x\<^isub>3"} - \]\smallskip - - \noindent - Taking the left-hand side in the assumption shown in \eqref{assmtwo}, we can use - the implication \eqref{impletpat} from the stronger cases lemma to infer @{text "P\<^bsub>trm\<^esub>"}, as needed. - - The remaining difficulty is when a deep binder contains some atoms that are - bound and some that are free. An example is @{text "Let\<^sup>\"} in - \eqref{letrecs}. In such cases @{text "(\ \ x\<^isub>1) - \\\<^bsub>bn\<^esub> x\<^isub>1"} does not hold in general. The idea however is - that @{text "\"} only renames atoms that become bound. In this way @{text "\"} - does not affect @{text "\\\<^bsub>bn\<^esub>"} (which only tracks alpha-equivalence of terms that are not - under the binder). However, the problem is that the - permutation operation @{text "\ \ x\<^isub>1"} applies to all atoms in @{text "x\<^isub>1"}. To avoid this - we introduce an auxiliary permutation operations, written @{text "_ - \\<^bsub>bn\<^esub> _"}, for deep binders that only permutes bound atoms (or - more precisely the atoms specified by the @{text "bn"}-functions) and leaves - the other atoms unchanged. Like the functions @{text "fa_bn"}$_{1..m}$, we - can define these permutation operations over raw terms analysing how the functions @{text - "bn"}$_{1..m}$ are defined. Assuming the user specified a clause - - \[ - @{text "bn (C x\<^isub>1 \ x\<^isub>r) = rhs"} - \]\smallskip - - \noindent - we define @{text "\ \\<^bsub>bn\<^esub> (C x\<^isub>1 \ x\<^isub>r) \ C y\<^isub>1 \ y\<^isub>r"} with @{text "y\<^isub>i"} determined as follows: - - \[\mbox{ - \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 \ \ \\<^bsub>bn\<^esub> x\<^isub>i"} provided @{text "bn x\<^isub>i"} is in @{text "rhs"}\\ - $\bullet$ & @{text "y\<^isub>i \ \ \ x\<^isub>i"} otherwise - \end{tabular}} - \]\smallskip - - \noindent - Using again the quotient package we can lift the auxiliary permutation operations - @{text "_ \\<^bsub>bn\<^esub> _"} - to alpha-equated terms. Moreover we can prove the following two properties: - - \begin{lem}\label{permutebn} - Given a binding function @{text "bn\<^sup>\"} and auxiliary equivalence @{text "\\\<^bsub>bn\<^esub>"} - then for all @{text "\"}\smallskip\\ - {\it (i)} @{text "\ \ (bn\<^sup>\ x) = bn\<^sup>\ (\ \\\<^bsub>bn\<^esub> x)"} and\\ - {\it (ii)} @{text "(\ \\\<^bsub>bn\<^esub> x) \\\<^bsub>bn\<^esub> x"}. - \end{lem} - - \begin{proof} - By induction on @{text x}. The properties follow by 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 states that @{text "_ \\\<^bsub>bn\<^esub> _"} preserves - @{text "\\\<^bsub>bn\<^esub>"}. The main point of the auxiliary - permutation functions is that they allow us to rename just the bound atoms in a - term, without changing anything else. - - Having the auxiliary permutation function in place, we can now solve all remaining cases. - For the @{text "Let\<^sup>\"} term-constructor, for example, we can by Property \ref{avoiding} - obtain a @{text "\"} such that - - \[ - @{text "(\ \ (set (bn\<^sup>\ x\<^isub>1)) #\<^sup>* c"} \hspace{10mm} - @{text "\ \ [bn\<^sup>\ x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2 = [bn\<^sup>\ x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2"} - \]\smallskip - - \noindent - hold. Using the first part of Lemma \ref{permutebn}, we can simplify this - to @{text "set (bn\<^sup>\ (\ \\\<^bsub>bn\<^esub> x\<^isub>1)) #\<^sup>* c"} and - \mbox{@{text "[bn\<^sup>\ (\ \\\<^bsub>bn\<^esub> x\<^isub>1)]\<^bsub>list\<^esub>. (\ \ x\<^isub>2) = [bn\<^sup>\ x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2"}}. Since - @{text "(\ \\\<^bsub>bn\<^esub> x\<^isub>1) \\\<^bsub>bn\<^esub> x\<^isub>1"} holds by the second part, - we can infer that - - \[ - @{text "Let\<^sup>\ (\ \\\<^bsub>bn\<^esub> x\<^isub>1) (\ \ x\<^isub>2) = Let\<^sup>\ x\<^isub>1 x\<^isub>2"} - \]\smallskip - - \noindent - holds. This allows us to use the implication from the strong cases - lemma, and we are done. - - Consequently, we can discharge all proof-obligations about having `covered all - cases'. This completes the proof establishing that the weak induction principles imply - the strong induction principles. These strong induction principles have already proved - being very useful in practice, particularly for proving properties about - capture-avoiding substitution \cite{Urban08}. -*} - - -section {* Related Work\label{related} *} - -text {* - To our knowledge the earliest usage of general binders in a theorem prover - is described by Nara\-schew\-ski and Nipkow \cite{NaraschewskiNipkow99} with 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 by Chargu\'eraud \cite{chargueraud09} - in the locally nameless approach to - binding. 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 and 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. We are not aware of any formalisation of - a non-trivial language that uses Chargu\'eraud's idea. - - Another technique for representing binding is higher-order abstract syntax - (HOAS), which for example is implemented in the Twelf system \cite{pfenningsystem}. - This representation technique supports very elegantly many aspects of - \emph{single} binding, and impressive work by Lee et al~\cite{LeeCraryHarper07} - has been done that uses HOAS for mechanising the metatheory of SML. 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' bound variables and the resulting formal reasoning turned out to - be rather unpleasant. In contrast, the unbinding can be - done in one step with our - general binders described in this paper. - - The most closely related work to the one presented here is the Ott-tool by - Sewell et al \cite{ott-jfp} and the C$\alpha$ml language by Pottier - \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 and free variables for 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 and free variables. We - have proved that our definitions lead to alpha-equated terms, whose support - is as expected (that means bound atoms are removed from the support). We - also showed that our specifications lift from `raw' terms to - alpha-equivalence classes. For this we have established (automatically) that every - term-constructor and function defined for `raw' terms - is respectful w.r.t.~alpha-equivalence. - - 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 (the corresponding @{text "fa"}-functions would not lift). - 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 one specifies 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{binds (set)} and - \isacommand{binds (set+)}. Consider the examples - - \[\mbox{ - \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}} - @{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} & - \isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "t s"}\\ - @{text "Foo\<^isub>2 xs::name fset t::trm s::trm"} & - \isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "t"}, - \isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "s"}\\ - \end{tabular}} - \]\smallskip - - \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\footnote{Assuming @{term "a \ b"}, there is no permutation that can - make @{text "(a, b)"} equal with both @{text "(a, b)"} and @{text "(b, a)"}, but - there are two permutations so that we can make @{text "(a, b)"} and @{text - "(a, b)"} equal with one permutation, and @{text "(a, b)"} and @{text "(b, - a)"} with the other.} - - - \[\mbox{ - \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)"} - \end{tabular}} - \]\smallskip - - \noindent - but - - \[\mbox{ - \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l} - @{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ & - @{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\ - \end{tabular}} - \]\smallskip - - \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 the Core-Haskell - language from the Introduction. With the work presented in this - paper we can define it formally as shown in - Figure~\ref{nominalcorehas} and then Nominal Isabelle derives - automatically a corresponding reasoning infrastructure. However we - have found out that telescopes seem to not easily be representable - in our framework. The reason is that we need to be able to lift our - @{text bn}-functions to alpha-equated lambda-terms and therefore - need to restrict what these @{text bn}-functions can return. - Telescopes can be represented in the framework described in - \cite{WeirichYorgeySheard11} using an extension of the usual - locally-nameless representation. - - \begin{figure}[p] - \begin{boxedminipage}{\linewidth} - \small - \begin{tabular}{l} - \isacommand{atom\_decl}~@{text "var cvar tvar"}\\[1mm] - \isacommand{nominal\_datatype}~@{text "tkind ="}~@{text "KStar"}~$|$~@{text "KFun tkind tkind"}\\ - \isacommand{and}~@{text "ckind ="}~@{text "CKSim ty ty"}\\ - \isacommand{and}~@{text "ty ="}~@{text "TVar tvar"}~$|$~@{text "T string"}~$|$~@{text "TApp ty ty"}\\ - $|$~@{text "TFun string ty_list"}~% - $|$~@{text "TAll tv::tvar tkind ty::ty"}\hspace{3mm}\isacommand{binds}~@{text "tv"}~\isacommand{in}~@{text ty}\\ - $|$~@{text "TArr ckind ty"}\\ - \isacommand{and}~@{text "ty_lst ="}~@{text "TNil"}~$|$~@{text "TCons ty ty_lst"}\\ - \isacommand{and}~@{text "cty ="}~@{text "CVar cvar"}~% - $|$~@{text "C string"}~$|$~@{text "CApp cty cty"}~$|$~@{text "CFun string co_lst"}\\ - $|$~@{text "CAll cv::cvar ckind cty::cty"}\hspace{3mm}\isacommand{binds}~@{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 ="}~@{text "CNil"}~$|$~@{text "CCons cty co_lst"}\\ - \isacommand{and}~@{text "trm ="}~@{text "Var var"}~$|$~@{text "K string"}\\ - $|$~@{text "LAM_ty tv::tvar tkind t::trm"}\hspace{3mm}\isacommand{binds}~@{text "tv"}~\isacommand{in}~@{text t}\\ - $|$~@{text "LAM_cty cv::cvar ckind t::trm"}\hspace{3mm}\isacommand{binds}~@{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"}\hspace{3mm}\isacommand{binds}~@{text "v"}~\isacommand{in}~@{text t}\\ - $|$~@{text "Let x::var ty trm t::trm"}\hspace{3mm}\isacommand{binds}~@{text x}~\isacommand{in}~@{text t}\\ - $|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\ - \isacommand{and}~@{text "assoc_lst ="}~@{text ANil}~% - $|$~@{text "ACons p::pat t::trm assoc_lst"}\hspace{3mm}\isacommand{binds}~@{text "bv p"}~\isacommand{in}~@{text t}\\ - \isacommand{and}~@{text "pat ="}~@{text "Kpat string tvtk_lst tvck_lst vt_lst"}\\ - \isacommand{and}~@{text "vt_lst ="}~@{text VTNil}~$|$~@{text "VTCons var ty vt_lst"}\\ - \isacommand{and}~@{text "tvtk_lst ="}~@{text TVTKNil}~$|$~@{text "TVTKCons tvar tkind tvtk_lst"}\\ - \isacommand{and}~@{text "tvck_lst ="}~@{text TVCKNil}~$|$ @{text "TVCKCons cvar ckind tvck_lst"}\\ - \isacommand{binder}\\ - \;@{text "bv :: pat \ atom list"}~\isacommand{and}\\ - \;@{text "bv\<^isub>1 :: vt_lst \ atom list"}~\isacommand{and}\\ - \;@{text "bv\<^isub>2 :: tvtk_lst \ atom list"}~\isacommand{and}\\ - \;@{text "bv\<^isub>3 :: tvck_lst \ atom list"}\\ - \isacommand{where}\\ - \phantom{$|$}~@{text "bv (K s tvts tvcs vs) = (bv\<^isub>3 tvts) @ (bv\<^isub>2 tvcs) @ (bv\<^isub>1 vs)"}\\ - $|$~@{text "bv\<^isub>1 VTNil = []"}\\ - $|$~@{text "bv\<^isub>1 (VTCons x ty tl) = (atom x)::(bv\<^isub>1 tl)"}\\ - $|$~@{text "bv\<^isub>2 TVTKNil = []"}\\ - $|$~@{text "bv\<^isub>2 (TVTKCons a ty tl) = (atom a)::(bv\<^isub>2 tl)"}\\ - $|$~@{text "bv\<^isub>3 TVCKNil = []"}\\ - $|$~@{text "bv\<^isub>3 (TVCKCons c cty tl) = (atom c)::(bv\<^isub>3 tl)"}\\ - \end{tabular} - \end{boxedminipage} - \caption{A definition for Core-Haskell in Nominal Isabelle. 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. Apart from that limitation, the - definition follows closely the original shown in Figure~\ref{corehas}. The - point of our work is that having made such a definition in Nominal Isabelle, - one obtains automatically a reasoning infrastructure for Core-Haskell. - \label{nominalcorehas}} - \end{figure} - \afterpage{\clearpage} - - Pottier presents a programming language, called C$\alpha$ml, for - representing terms with general binders inside OCaml \cite{Pottier06}. 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{binds} - 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} and more recently - by Weirich et al \cite{WeirichYorgeySheard11}. - - In a slightly different domain (programming with dependent types), - Altenkirch et al \cite{Altenkirch10} present a calculus with a notion of - alpha-equivalence related to our binding mode \isacommand{binds (set+)}. - Their definition 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. -*} - -section {* Conclusion *} - -text {* - - We have presented an extension of Nominal Isabelle for dealing with general - binders, that is where term-constructors have multiple bound atoms. 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 syntax from Ott, but extended it in some places and restricted - it in others so that the definitions 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 Isabelle distribution.\footnote{It - can be downloaded already from \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 \cite{Krauss09} 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 had - to impose in this paper that can be lifted using - a recent reimplementation \cite{Traytel12} of the datatype package for Isabelle/HOL, which - however is not yet part of the stable distribution. - This reimplementation allows nested - datatype definitions and would 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}). We can - also use it to represent the @{text "Let"}-terms from the Introduction where - the order of @{text "let"}-assignments does not matter. This means we can represent @{text "Let"}s - such that the following two terms are equal - - \[ - @{text "Let x\<^isub>1 = t\<^isub>1 and x\<^isub>2 = t\<^isub>2 in s"} \;\;=\;\; - @{text "Let x\<^isub>2 = t\<^isub>2 and x\<^isub>1 = t\<^isub>1 in s"} - \]\smallskip - - \noindent - For this we have to represent the @{text "Let"}-assignments as finite sets - of pair and a binding function that picks out the left components to be bound in @{text s}. - - One line of future 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 - - \[ - \mbox{@{text "fa_ty x = bn x \ fa_bn x"}} - \]\smallskip - - \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 usual lists, - we abstract lists of distinct elements (the corresponding type @{text - "dlist"} already exists in the library of Isabelle/HOL). We expect the - presented work can be extended to accommodate such binding modes.\medskip - - \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. Stephanie Weirich - suggested to separate the subgrammars of kinds and types in our Core-Haskell - example. Ramana Kumar and Andrei Popescu helped us with comments for - an earlier version of this paper. -*} - - -(*<*) -end -(*>*)