diff -r c9d3dda79fe3 -r d7dc35222afc Paper/Paper.thy --- a/Paper/Paper.thy Fri Mar 26 16:20:39 2010 +0100 +++ b/Paper/Paper.thy Fri Mar 26 16:46:40 2010 +0100 @@ -3,15 +3,35 @@ imports "../Nominal/Test" "LaTeXsugar" begin +consts + fv :: "'a \ 'b" + abs_set :: "'a \ 'b \ 'c" + Abs_lst :: "'a \ 'b \ 'c" + Abs_res :: "'a \ 'b \ 'c" + +definition + "equal \ (op =)" + notation (latex output) swap ("'(_ _')" [1000, 1000] 1000) and fresh ("_ # _" [51, 51] 50) and fresh_star ("_ #* _" [51, 51] 50) and supp ("supp _" [78] 73) and uminus ("-_" [78] 73) and - If ("if _ then _ else _" 10) + If ("if _ then _ else _" 10) and + alpha_gen ("_ \\<^raw:\makebox[0mm][l]{$\,_{\textit{set}}$}>\<^bsup>_,_,_\<^esup> _") and + alpha_lst ("_ \\<^raw:\makebox[0mm][l]{$\,_{\textit{list}}$}>\<^bsup>_,_,_\<^esup> _") and + alpha_res ("_ \\<^raw:\makebox[0mm][l]{$\,_{\textit{res}}$}>\<^bsup>_,_,_\<^esup> _") and + abs_set ("_ \\<^raw:{$\,_{\textit{abs\_set}}$}> _") and + fv ("fv'(_')" [100] 100) and + equal ("=") and + alpha_abs ("_ \\<^raw:{$\,_{\textit{abs\_set}}$}> _") and + Abs ("[_]\<^raw:$\!$>\<^bsub>set\<^esub>._") and + Abs_lst ("[_]\<^raw:$\!$>\<^bsub>list\<^esub>._") and + Abs_res ("[_]\<^raw:$\!$>\<^bsub>res\<^esub>._") (*>*) + section {* Introduction *} text {* @@ -19,12 +39,12 @@ alpha-equated terms, for example \begin{center} - $t ::= x \mid t\;t \mid \lambda x. t$ + @{text "t ::= x | t t | \x. t"} \end{center} \noindent where free and bound variables have names. For such terms Nominal Isabelle - derives automatically a reasoning infrastructure that has been used + 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 @@ -39,7 +59,8 @@ % \begin{equation}\label{tysch} \begin{array}{l} - T ::= x \mid T \rightarrow T \hspace{5mm} S ::= \forall \{x_1,\ldots, x_n\}. T + @{text "T ::= x | T \ T"}\hspace{5mm} + @{text "S ::= \{x\<^isub>1,\, x\<^isub>n}. T"} \end{array} \end{equation} @@ -59,38 +80,38 @@ we would like to regard the following two type-schemes as alpha-equivalent % \begin{equation}\label{ex1} - \forall \{x, y\}. x \rightarrow y \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x + @{text "\{x,y}. x \ y \\<^isub>\ \{y,x}. y \ x"} \end{equation} \noindent - but assuming that $x$, $y$ and $z$ are distinct variables, + but assuming that @{text x}, @{text y} and @{text z} are distinct variables, the following two should \emph{not} be alpha-equivalent % \begin{equation}\label{ex2} - \forall \{x, y\}. x \rightarrow y \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z + @{text "\{x,y}. x \ y \\<^isub>\ \{z}. z \ z"} \end{equation} \noindent - Moreover, we like to regard type-schemes as - alpha-equivalent, if they differ only on \emph{vacuous} binders, such as + Moreover, we like to regard type-schemes as alpha-equivalent, if they differ + only on \emph{vacuous} binders, such as % \begin{equation}\label{ex3} - \forall \{x\}. x \rightarrow y \;\approx_\alpha\; \forall \{x, z\}. x \rightarrow y + @{text "\{x}. x \ y \\<^isub>\ \{x,z}. x \ y"} \end{equation} \noindent - where $z$ does not occur freely in the type. - In this paper we will give a general binding mechanism and associated - notion of alpha-equivalence that can be used to faithfully represent - this kind of binding in Nominal Isabelle. The difficulty of finding the right notion - for alpha-equivalence can be appreciated in this case by considering that the - definition given by Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). + where @{text z} does not occur freely in the type. In this paper we will + give a general binding mechanism and associated notion of alpha-equivalence + that can be used to faithfully represent this kind of binding in Nominal + Isabelle. The difficulty of finding the right notion for alpha-equivalence + can be appreciated in this case by considering that the definition given by + Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). - However, the notion of alpha-equivalence that is preserved by vacuous binders is not - always wanted. For example in terms like + 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} - \LET x = 3 \AND y = 2 \IN x\,-\,y \END + @{text "\ x = 3 \ y = 2 \ x - y \"} \end{equation} \noindent @@ -99,7 +120,7 @@ with % \begin{center} - $\LET x = 3 \AND y = 2 \AND z = loop \IN x\,-\,y \END$ + @{text "\ x = 3 \ y = 2 \ z = loop \ x - y \"} \end{center} \noindent @@ -109,10 +130,10 @@ However, we found that this is still not sufficient for dealing with language constructs frequently occurring in programming language - research. For example in $\mathtt{let}$s containing patterns + research. For example in @{text "\"}s containing patterns % \begin{equation}\label{two} - \LET (x, y) = (3, 2) \IN x\,-\,y \END + @{text "\ (x, y) = (3, 2) \ x - y \"} \end{equation} \noindent @@ -121,72 +142,79 @@ we do not want to regard \eqref{two} as alpha-equivalent with % \begin{center} - $\LET (y, x) = (3, 2) \IN x\,- y\,\END$ + @{text "\ (y, x) = (3, 2) \ x - y \"} \end{center} \noindent - As a result, we provide three general binding mechanisms each of which binds multiple - variables at once, and let the user chose which one is intended when formalising a - programming language calculus. + As a result, we provide three general binding mechanisms each of which binds + multiple variables at once, and let the user chose which one is intended + when formalising a programming language 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 $\mathtt{let}$-constructs of the form + By providing these general binding mechanisms, however, we have to work + around a problem that has been pointed out by Pottier \cite{Pottier06} and + Cheney \cite{Cheney05}: in @{text "\"}-constructs of the form % \begin{center} - $\LET x_1 = t_1 \AND \ldots \AND x_n = t_n \IN s \END$ + @{text "\ x\<^isub>1 = t\<^isub>1 \ \ \ x\<^isub>n = t\<^isub>n \ s \"} \end{center} \noindent - which bind all the $x_i$ in $s$, we might not care about the order in - which the $x_i = t_i$ are given, but we do care about the information that there are - as many $x_i$ as there are $t_i$. We lose this information if we represent the - $\mathtt{let}$-constructor by something like + which bind all the @{text "x\<^isub>i"} in @{text s}, we might not care + about the order in which the @{text "x\<^isub>i = t\<^isub>i"} are given, + but we do care about the information that there are as many @{text + "x\<^isub>i"} as there are @{text "t\<^isub>i"}. We lose this information if + we represent the @{text "\"}-constructor by something like % \begin{center} - $\LET [x_1,\ldots,x_n].s\;\; [t_1,\ldots,t_n]$ + @{text "\ [x\<^isub>1,\,x\<^isub>n].s [t\<^isub>1,\,t\<^isub>n]"} \end{center} \noindent - where the notation $[\_\!\_].\_\!\_$ indicates that the $x_i$ become bound - in $s$. In this representation the term \mbox{$\LET [x].s\;\;[t_1,t_2]$} - would be a perfectly legal instance. 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 into very messy reasoning (see - for example~\cite{BengtsonParow09}). To avoid this, we will allow type specifications - for $\mathtt{let}$s as follows + where the notation @{text "[_]._"} indicates that the @{text "x\<^isub>i"} + become bound in @{text s}. In this representation the term + \mbox{@{text "\ [x].s [t\<^isub>1,t\<^isub>2]"}} would be a perfectly legal + instance. 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 into very messy reasoning (see for + example~\cite{BengtsonParow09}). To avoid this, we will allow type + specifications for $\mathtt{let}$s as follows % \begin{center} \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l} - $trm$ & $::=$ & \ldots\\ - & $\mid$ & $\mathtt{let}\;a\!::\!assn\;\;s\!::\!trm\quad\mathtt{bind}\;bn\,(a) \IN s$\\[1mm] - $assn$ & $::=$ & $\mathtt{anil}$\\ - & $\mid$ & $\mathtt{acons}\;\;name\;\;trm\;\;assn$ + @{text trm} & @{text "::="} & @{text "\"}\\ + & @{text "|"} & @{text "\ a::assn s::trm"}\hspace{4mm} + \isacommand{bind} @{text "bn(a)"} \isacommand{in} @{text "s"}\\[1mm] + @{text assn} & @{text "::="} & @{text "\"}\\ + & @{text "|"} & @{text "\ name trm assn"} \end{tabular} \end{center} \noindent - where $assn$ is an auxiliary type representing a list of assignments - and $bn$ an auxiliary function identifying the variables to be bound by - the $\mathtt{let}$. This function is defined by recursion over $assn$ as follows + 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 is defined by recursion over @{text + assn} as follows \begin{center} - $bn\,(\mathtt{anil}) = \varnothing \qquad bn\,(\mathtt{acons}\;x\;t\;as) = \{x\} \cup bn\,(as)$ + @{text "bn(\) ="} @{term "{}"} \hspace{5mm} + @{text "bn(\ x t as) = {x} \ bn(as)"} \end{center} \noindent The scope of the binding is indicated by labels given to the types, for - example \mbox{$s\!::\!trm$}, and a binding clause, in this case - $\mathtt{bind}\;bn\,(a) \IN s$, that states to bind in $s$ all the names the - function call $bn\,(a)$ returns. This style of specifying terms and bindings is - heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. + example @{text "s::trm"}, and a binding clause, in this case + \isacommand{bind} @{text "bn(a)"} \isacommand{in} @{text "s"}, that states + to bind in @{text s} all the names the function call @{text "bn(a)"} returns. + This style of specifying terms and bindings is heavily inspired by the + syntax of the Ott-tool \cite{ott-jfp}. + However, we will not be able to deal with all specifications that are allowed by Ott. One reason is that Ott lets the user to specify ``empty'' types like \begin{center} - $t ::= t\;t \mid \lambda x. t$ + @{text "t ::= t t | \x. t"} \end{center} \noindent @@ -204,32 +232,31 @@ two type-schemes (with $x$, $y$ and $z$ being distinct) \begin{center} - $\forall \{x\}. x \rightarrow y \;=\; \forall \{x, z\}. x \rightarrow y$ + @{text "\{x}. x \ y = \{x,z}. x \ y"} \end{center} \noindent - are not just alpha-equal, but actually \emph{equal}. As a - result, we can only support specifications that make sense on the level of - alpha-equated terms (offending specifications, which for example bind a variable - according to a variable bound somewhere else, are not excluded by Ott, but we - have to). Our - insistence on reasoning with alpha-equated terms comes from the wealth of - experience we gained with the older version of Nominal Isabelle: for - non-trivial properties, reasoning about 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. + 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 about 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 the Isabelle/HOL theorem prover is a rather non-trivial task. - For every specification we will need to construct a type 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 HOL can be illustrated by the following picture: - + Although in informal settings a reasoning infrastructure for alpha-equated + terms is nearly always taken for granted, establishing it automatically in + the Isabelle/HOL theorem prover is a rather non-trivial task. For every + specification we will need to construct a type 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 HOL can be illustrated by the following picture: + \begin{center} \begin{tikzpicture} %\draw[step=2mm] (-4,-1) grid (4,1); @@ -255,45 +282,45 @@ \end{center} \noindent - We take as the starting point a definition of raw terms (defined as a - datatype in Isabelle/HOL); identify then the - alpha-equivalence classes in the type of sets of raw terms according to our - alpha-equivalence relation and finally define the new type as these - alpha-equivalence classes (non-emptiness is satisfied whenever the raw terms are - definable as datatype in Isabelle/HOL and the fact that our relation for - alpha-equivalence is indeed an equivalence relation). + We take as the starting point a definition of raw terms (defined as a + datatype in Isabelle/HOL); identify then the alpha-equivalence classes in + the type of sets of raw terms according to our alpha-equivalence relation + and finally define the new type as these alpha-equivalence classes + (non-emptiness is satisfied whenever the raw terms are definable as datatype + in Isabelle/HOL and the fact that our relation for alpha-equivalence is + indeed 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 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 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 + 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 the quotient package + described by Homeier \cite{Homeier05} for the HOL4 system. This package + allows us to lift definitions and theorems involving raw terms to + definitions and theorems involving alpha-equated terms. For example if we + define the free-variable function over raw lambda-terms \begin{center} - $\fv(x) = \{x\}$\hspace{10mm} - $\fv(t_1\;t_2) = \fv(t_1) \cup \fv(t_2)$\\[1mm] - $\fv(\lambda x.t) = \fv(t) - \{x\}$ + @{text "fv(x) = {x}"}\hspace{10mm} + @{text "fv(t\<^isub>1 t\<^isub>2) = fv(t\<^isub>1) \ fv(t\<^isub>2)"}\\[1mm] + @{text "fv(\x.t) = fv(t) - {x}"} \end{center} \noindent - then with not too great effort we obtain a function $\fv^\alpha$ + then with not too great effort we obtain a function @{text "fv\<^sup>\"} operating on quotients, or alpha-equivalence classes of lambda-terms. This lifted function is characterised by the equations \begin{center} - $\fv^\alpha(x) = \{x\}$\hspace{10mm} - $\fv^\alpha(t_1\;t_2) = \fv^\alpha(t_1) \cup \fv^\alpha(t_2)$\\[1mm] - $\fv^\alpha(\lambda x.t) = \fv^\alpha(t) - \{x\}$ + @{text "fv\<^sup>\(x) = {x}"}\hspace{10mm} + @{text "fv\<^sup>\(t\<^isub>1 t\<^isub>2) = fv\<^sup>\(t\<^isub>1) \ fv\<^sup>\(t\<^isub>2)"}\\[1mm] + @{text "fv\<^sup>\(\x.t) = fv\<^sup>\(t) - {x}"} \end{center} \noindent @@ -400,44 +427,47 @@ 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 manageable, we will wherever possible state - definitions and perform proofs inside Isabelle, as opposed to write custom - ML-code that generates them anew for each specification. To that - end, we will consider pairs @{text "(as, x)"} of type @{text "(atom set) \ \"}. - These pairs are intended to represent the abstraction, or binding, of the set @{text "as"} - in the body @{text "x"}. + In order to keep our work with deriving the reasoning infrastructure + manageable, we will wherever possible state definitions and perform proofs + on the user-level of Isabelle/HOL, as opposed to write custom ML-code that + generates them anew for each specification. To that end, we will consider + first pairs @{text "(as, x)"} of type @{text "(atom set) \ \"}. These pairs + are intended to represent the abstraction, or binding, of the set @{text + "as"} in the body @{text "x"}. - The first question we have to answer is when the pairs $(as, x)$ and $(bs, y)$ are - alpha-equivalent? (At the moment we are interested in - the notion of alpha-equivalence that is \emph{not} preserved by adding - vacuous binders.) To answer this, we identify four conditions: {\it i)} given - a free-variable function $\fv$ of type \mbox{@{text "\ \ atom set"}}, then @{text x} and @{text y} - need to have the same set of free variables; moreover there must be a permutation - @{text p} such that {\it ii)} it leaves the free variables of @{text x} and @{text y} unchanged, - but {\it iii)} ``moves'' their bound names so that we obtain modulo a relation, - say \mbox{@{text "_ R _"}}, two equal terms. We also require {\it iv)} that @{text p} makes - the abstracted sets @{text as} and @{text bs} equal. The requirements {\it i)} to {\it iv)} can - be stated formally as follows: + The first question we have to answer is when the pairs @{text "(as, x)"} and + @{text "(bs, y)"} are alpha-equivalent? (At the moment we are interested in + the notion of alpha-equivalence that is \emph{not} preserved by adding + vacuous binders.) To answer this, we identify four conditions: {\it i)} + given a free-variable function @{text "fv"} of type \mbox{@{text "\ \ atom + set"}}, then @{text x} and @{text y} need to have the same set of free + variables; moreover there must be a permutation @{text p} such that {\it + ii)} it leaves the free variables of @{text x} and @{text y} unchanged, but + {\it iii)} ``moves'' their bound names so that we obtain modulo a relation, + say \mbox{@{text "_ R _"}}, two equal terms. We also require {\it iv)} that + @{text p} makes the abstracted sets @{text as} and @{text bs} equal. The + requirements {\it i)} to {\it iv)} can be stated formally as follows: % \begin{equation}\label{alphaset} \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l} - \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{set}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm] - & @{text "fv(x) - as = fv(y) - bs"}\\ - \wedge & @{text "(fv(x) - as) #* p"}\\ - \wedge & @{text "(p \ x) R y"}\\ - \wedge & @{text "(p \ as) = bs"}\\ + \multicolumn{2}{l}{@{term "(as, x) \gen R fv p (bs, y)"} @{text "\"}\hspace{30mm}}\\ + & @{term "fv(x) - as = fv(y) - bs"}\\ + @{text "\"} & @{term "(fv(x) - as) \* p"}\\ + @{text "\"} & @{text "(p \ x) R y"}\\ + @{text "\"} & @{term "(p \ as) = bs"}\\ \end{array} \end{equation} \noindent - Note that this relation is dependent on $p$. Alpha-equivalence is then the relation where - we existentially quantify over this $p$. - Also note that the relation is dependent on a free-variable function $\fv$ and a relation - $R$. The reason for this extra generality is that we will use $\approx_{set}$ for both - ``raw'' terms and alpha-equated terms. In the latter case, $R$ will be replaced by - equality $(op =)$ and we are going to prove that $\fv$ will be equal to the support - of $x$ and $y$. + Note that this relation is dependent on the permutation @{text + "p"}. Alpha-equivalence between two pairs is then the relation where we + existentially quantify over this @{text "p"}. Also note that the relation is + dependent on a free-variable function @{text "fv"} and a relation @{text + "R"}. The reason for this extra generality is that we will use + $\approx_{\textit{set}}$ for both ``raw'' terms and alpha-equated terms. In + the latter case, $R$ will be replaced by equality @{text "="} and for raw terms we + will prove that @{text "fv"} is equal to the support of @{text + x} and @{text y}. The definition in \eqref{alphaset} does not make any distinction between the order of abstracted variables. If we want this, then we can define alpha-equivalence @@ -446,26 +476,27 @@ % \begin{equation}\label{alphalist} \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l} - \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{list}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm] - & @{text "fv(x) - (set as) = fv(y) - (set bs)"}\\ - \wedge & @{text "(fv(x) - set as) #* p"}\\ + \multicolumn{2}{l}{@{term "(as, x) \lst R fv p (bs, y)"} @{text "\"}\hspace{30mm}}\\[1mm] + & @{term "fv(x) - (set as) = fv(y) - (set bs)"}\\ + \wedge & @{term "(fv(x) - set as) \* p"}\\ \wedge & @{text "(p \ x) R y"}\\ - \wedge & @{text "(p \ as) = bs"}\\ + \wedge & @{term "(p \ as) = bs"}\\ \end{array} \end{equation} \noindent - where $set$ is the function that coerces a list of atoms into a set of atoms. + where @{term set} is a function that coerces a list of atoms into a set of atoms. + Now the last clause ensures that the order of the binders matters. - If we do not want to make any difference between the order of binders and + If we do not want to make any difference between the order of binders \emph{and} also allow vacuous binders, then we keep sets of binders, but drop the fourth condition in \eqref{alphaset}: % \begin{equation}\label{alphares} \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l} - \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{res}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm] - & @{text "fv(x) - as = fv(y) - bs"}\\ - \wedge & @{text "(fv(x) - as) #* p"}\\ + \multicolumn{2}{l}{@{term "(as, x) \res R fv p (bs, y)"} @{text "\"}\hspace{30mm}}\\[1mm] + & @{term "fv(x) - as = fv(y) - bs"}\\ + \wedge & @{term "(fv(x) - as) \* p"}\\ \wedge & @{text "(p \ x) R y"}\\ \end{array} \end{equation} @@ -473,52 +504,116 @@ \begin{exmple}\rm It might be useful to consider some examples for how these definitions pan out in practise. For this consider the case of abstracting a set of variables over types (as in type-schemes). - We set $R$ to be the equality and for $\fv(T)$ we define + We set @{text R} to be the equality and for @{text "fv(T)"} we define \begin{center} - $\fv(x) = \{x\} \qquad \fv(T_1 \rightarrow T_2) = \fv(T_1) \cup \fv(T_2)$ + @{text "fv(x) = {x}"} \hspace{5mm} @{text "fv(T\<^isub>1 \ T\<^isub>2) = fv(T\<^isub>1) \ fv(T\<^isub>2)"} \end{center} \noindent - Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and \eqref{ex3}. It can be easily - checked that @{text "({x, y}, x \ y)"} and - @{text "({y, x}, y \ x)"} are equal according to $\approx_{set}$ and $\approx_{res}$ by taking $p$ to - be the swapping @{term "(x \ y)"}. In case of @{text "x \ y"}, then - $([x, y], x \rightarrow y) \not\approx_{list} ([y,x], x \rightarrow 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 examples is - $(\{x\}, x) \approx_{res} (\{x,y\}, x)$ which holds by taking $p$ to be the identity permutation. - However, if @{text "x \ y"}, then - $(\{x\}, x) \not\approx_{set} (\{x,y\}, x)$ since there is no permutation that makes - the sets $\{x\}$ and $\{x,y\}$ equal (similarly for $\approx_{list}$). + Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and + \eqref{ex3}. It can be easily checked that @{text "({x,y}, x \ y)"} and + @{text "({y,x}, y \ x)"} are equal according to $\approx_{\textit{set}}$ and + $\approx_{\textit{res}}$ by taking @{text p} to be the swapping @{term "(x \ + y)"}. In case of @{text "x \ y"}, then @{text "([x, y], x \ y)"} + $\not\approx_{\textit{list}}$ @{text "([y,x], x \ y)"} since there is no permutation + that makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and also + leaves the type \mbox{@{text "x \ y"}} unchanged. Another example is + @{text "({x}, x)"} $\approx_{\textit{res}}$ @{text "({x,y}, x)"} which holds by + taking @{text p} to be the + identity permutation. However, if @{text "x \ y"}, then @{text "({x}, x)"} + $\not\approx_{\textit{set}}$ @{text "({x,y}, x)"} since there is no permutation + that makes the + sets @{text "{x}"} and @{text "{x,y}"} equal (similarly for $\approx_{\textit{list}}$). \end{exmple} + % looks too ugly + %\noindent + %Let $\star$ range over $\{set, res, list\}$. We prove next under which + %conditions the $\approx\hspace{0.05mm}_\star^{\fv, R, p}$ are equivalence + %relations and equivariant: + % + %\begin{lemma} + %{\it i)} Given the fact that $x\;R\;x$ holds, then + %$(as, x) \approx\hspace{0.05mm}^{\fv, R, 0}_\star (as, x)$. {\it ii)} Given + %that @{text "(p \ x) R y"} implies @{text "(-p \ y) R x"}, then + %$(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$ implies + %$(bs, y) \approx\hspace{0.05mm}^{\fv, R, - p}_\star (as, x)$. {\it iii)} Given + %that @{text "(p \ x) R y"} and @{text "(q \ y) R z"} implies + %@{text "((q + p) \ x) R z"}, then $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$ + %and $(bs, y) \approx\hspace{0.05mm}^{\fv, R, q}_\star (cs, z)$ implies + %$(as, x) \approx\hspace{0.05mm}^{\fv, R, q + p}_\star (cs, z)$. Given + %@{text "(q \ x) R y"} implies @{text "(p \ (q \ x)) R (p \ y)"} and + %@{text "p \ (fv x) = fv (p \ x)"} then @{text "p \ (fv y) = fv (p \ y)"}, then + %$(as, x) \approx\hspace{0.05mm}^{\fv, R, q}_\star (bs, y)$ implies + %$(p \;\isasymbullet\; as, p \;\isasymbullet\; x) \approx\hspace{0.05mm}^{\fv, R, q}_\star + %(p \;\isasymbullet\; bs, p \;\isasymbullet\; y)$. + %\end{lemma} + + %\begin{proof} + %All properties are by unfolding the definitions and simple calculations. + %\end{proof} + + + In the rest of this section we are going to introduce a type- and term-constructor + for abstractions. For this we define + % + \begin{equation} + @{term "abs_set (as, x) (bs, x) \ \p. alpha_gen (as, x) equal supp p (bs, x)"} + \end{equation} + \noindent - Let $\star$ range over $\{set, res, list\}$. We prove next under which - conditions the $\approx\hspace{0.05mm}_\star^{\fv, R, p}$ are equivalence - relations and equivariant: + Similarly for @{text "abs_list"} and @{text "abs_res"}. We can show that these + relations are equivalence relations and equivariant + (we only show the $\approx_{\textit{abs\_set}}$-case). \begin{lemma} - {\it i)} Given the fact that $x\;R\;x$ holds, then - $(as, x) \approx\hspace{0.05mm}^{\fv, R, 0}_\star (as, x)$. {\it ii)} Given - that @{text "(p \ x) R y"} implies @{text "(-p \ y) R x"}, then - $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$ implies - $(bs, y) \approx\hspace{0.05mm}^{\fv, R, - p}_\star (as, x)$. {\it iii)} Given - that @{text "(p \ x) R y"} and @{text "(q \ y) R z"} implies - @{text "((q + p) \ x) R z"}, then $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$ - and $(bs, y) \approx\hspace{0.05mm}^{\fv, R, q}_\star (cs, z)$ implies - $(as, x) \approx\hspace{0.05mm}^{\fv, R, q + p}_\star (cs, z)$. Given - @{text "(q \ x) R y"} implies @{text "(p \ (q \ x)) R (p \ y)"} and - @{text "p \ (fv x) = fv (p \ x)"} then @{text "p \ (fv y) = fv (p \ y)"}, then - $(as, x) \approx\hspace{0.05mm}^{\fv, R, q}_\star (bs, y)$ implies - $(p \;\isasymbullet\; as, p \;\isasymbullet\; x) \approx\hspace{0.05mm}^{\fv, R, q}_\star - (p \;\isasymbullet\; bs, p \;\isasymbullet\; y)$. + $\approx_{\textit{abs\_set}}$ is an equivalence + relations, and if @{term "abs_set (as, x) (bs, x)"} then also + @{term "abs_set (p \ as, p \ x) (p \ bs, p \ x)"}. + \end{lemma} + + \begin{proof} + Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have + a permutation @{text p} and for the proof obligation take @{term "-p"}. In case + of transitivity we have two permutations @{text p} and @{text q}, and for the + proof obligation use @{text "q + p"}. All the conditions are then by simple + calculations. + \end{proof} + + \noindent + The following lemma (and similar ones for $\approx_{\textit{abs\_list}}$ and + $\approx_{\textit{abs\_res}}$) will be crucial below: + + \begin{lemma} + @{thm[mode=IfThen] alpha_abs_swap[no_vars]} \end{lemma} - + \begin{proof} - All properties are by unfolding the definitions and simple calculations. + This lemma is straightforward by observing that the assumptions give us + @{term "(a \ b) \ (supp x - bs) = (supp x - bs)"} and that @{text supp} + is equivariant. \end{proof} + \noindent + We are also define the following + + @{text "aux (as, x) \ supp x - as"} + + + + \noindent + This allows us to use our quotient package and introduce new types + @{text "\ abs_set"}, @{text "\ abs_res"} and @{text "\ abs_list"} + representing the alpha-equivalence classes. Elements in these types + we will, respectively, write as: + + \begin{center} + @{term "Abs as x"} \hspace{5mm} + @{term "Abs_lst as x"} \hspace{5mm} + @{term "Abs_res as x"} + \end{center} + \begin{lemma} $supp ([as]set. x) = supp x - as$ @@ -834,7 +929,7 @@ \begin{tabular}{cp{7cm}} $\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\ $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\ - $\bullet$ & @{text "(atoml x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\ + $\bullet$ & @{text "(atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\ $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is a nominal datatype\\ $\bullet$ & @{term "{}"} otherwise \end{tabular}