diff -r 186d8486dfd5 -r 23480003f9c5 Paper/Paper.thy --- a/Paper/Paper.thy Mon Apr 26 13:08:14 2010 +0200 +++ b/Paper/Paper.thy Mon Apr 26 20:17:41 2010 +0200 @@ -363,7 +363,7 @@ inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic proofs, we establish a reasoning infrastructure for alpha-equated terms, including properties about support, freshness and equality - conditions for alpha-equated terms. We are also able to derive, at the moment + conditions for alpha-equated terms. We are also able to derive, for the moment only manually, strong induction principles that have the variable convention already built in. @@ -490,7 +490,7 @@ \end{center} \noindent - We also use for sets of atoms the abbreviation + 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 @@ -682,7 +682,7 @@ It might be useful to consider some examples for how these definitions of alpha-equivalence pan out in practice. For this consider the case of abstracting a set of variables over types (as in type-schemes). - We set @{text R} to be the equality and for @{text "fv(T)"} we define + We set @{text R} to be the usual equality @{text "="} and for @{text "fv(T)"} we define \begin{center} @{text "fv(x) = {x}"} \hspace{5mm} @{text "fv(T\<^isub>1 \ T\<^isub>2) = fv(T\<^isub>1) \ fv(T\<^isub>2)"} @@ -764,13 +764,14 @@ \noindent This lemma allows us to use our quotient package and introduce new types @{text "\ abs_set"}, @{text "\ abs_res"} and @{text "\ abs_list"} - representing alpha-equivalence classes of pairs. The elements in these types - will be, respectively, written as: + representing alpha-equivalence classes of pairs of type + @{text "(atom set) \ \"} (in the first two cases) and of type @{text "(atom list) \ \"}. + The elements in these types will be, respectively, written as: \begin{center} @{term "Abs as x"} \hspace{5mm} - @{term "Abs_lst as x"} \hspace{5mm} - @{term "Abs_res as x"} + @{term "Abs_res as x"} \hspace{5mm} + @{term "Abs_lst as x"} \end{center} \noindent @@ -784,8 +785,8 @@ \begin{center} \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l} @{thm (lhs) supp_abs(1)[no_vars]} & $=$ & @{thm (rhs) supp_abs(1)[no_vars]}\\ - @{thm (lhs) supp_abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_abs(3)[where bs="as", no_vars]}\\ - @{thm (lhs) supp_abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_abs(2)[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{tabular} \end{center} \end{thm} @@ -851,7 +852,7 @@ \end{center} \noindent - using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set + using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set, we further obtain % \begin{equation}\label{halftwo} @@ -897,7 +898,7 @@ binding \mbox{function part} & $\begin{cases} \mbox{\begin{tabular}{l} - \isacommand{with} @{text "bn\\<^isub>1"} \isacommand{and} \ldots \isacommand{and} @{text "bn\\<^isub>m"}\\ + \isacommand{binder} @{text "bn\\<^isub>1"} \isacommand{and} \ldots \isacommand{and} @{text "bn\\<^isub>m"}\\ \isacommand{where}\\ $\ldots$\\ \end{tabular}} @@ -943,8 +944,10 @@ 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). The ``\isacommand{in}-part'' of a binding - clause will be called \emph{body}; the ``\isacommand{bind}-part'' will - be called \emph{binder}. + clause will be called \emph{bodies} (there can be more than one); the + ``\isacommand{bind}-part'' will be called \emph{binders}. A body can only occur + in \emph{one} binding clause. A binder, in contrast, may occur in several binding + clauses, but cannot occur as a body. In addition we distinguish between \emph{shallow} and \emph{deep} binders. Shallow binders are of the form \isacommand{bind}\; {\it labels}\; @@ -976,22 +979,16 @@ \noindent Note that in this specification \emph{name} refers to an atom type. - If we have shallow binders that ``share'' a body, for instance $t$ in - the following term-constructor + Shallow binders may also ``share'' several bodies, for instance @{text t} + and @{text s} in the following term-constructor \begin{center} \begin{tabular}{ll} - @{text "Foo x::name y::name t::lam"} & - \isacommand{bind} @{text x} \isacommand{in} @{text t},\; - \isacommand{bind} @{text y} \isacommand{in} @{text t} + @{text "Foo x::name y::name t::lam s::lam"} & + \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"} \end{tabular} \end{center} - \noindent - then we have to make sure the modes of the binders agree. We cannot - have, for instance, in the first binding clause the mode \isacommand{bind} - and in the second \isacommand{bind\_set}. - 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 @@ -1017,7 +1014,7 @@ \hspace{5mm}\phantom{$\mid$}~@{text PNil}\\ \hspace{5mm}$\mid$~@{text "PVar name"}\\ \hspace{5mm}$\mid$~@{text "PTup pat pat"}\\ - \isacommand{with}~@{text "bn::pat \ atom list"}\\ + \isacommand{binder}~@{text "bn::pat \ atom list"}\\ \isacommand{where}~@{text "bn(PNil) = []"}\\ \hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\ \hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\\ @@ -1046,18 +1043,16 @@ \begin{center} \begin{tabular}{ll} - @{text "Foo p::pat q::pat t::trm"} & - \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t},\; - \isacommand{bind} @{text "bn(q)"} \isacommand{in} @{text t}\\ - @{text "Foo' x::name p::pat t::trm"} & - \isacommand{bind} @{text x} \isacommand{in} @{text t},\; - \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t} + @{text "Foo\<^isub>1 p::pat q::pat t::trm"} & + \isacommand{bind} @{text "bn(p) bn(q)"} \isacommand{in} @{text t}\\ + @{text "Foo\<^isub>2 x::name p::pat t::trm"} & + \isacommand{bind} @{text "x bn(p)"} \isacommand{in} @{text t}\\ \end{tabular} \end{center} \noindent - In the first case we might bind all atoms from the pattern @{text p} in @{text t} - and also all atoms from @{text q} in @{text t}. As a result we have no way + In the first case the intention is to bind all atoms from the pattern @{text p} in @{text t} + and also all atoms from @{text q} in @{text t}. Unfortunately, we have no way to determine whether the binder came from the binding function @{text "bn(p)"} or @{text "bn(q)"}. Similarly in the second case. The reason why we must exclude such specifications is that they cannot be represent by @@ -1066,19 +1061,17 @@ \begin{center} \begin{tabular}{ll} - @{text "Bar p::pat t::trm s::trm"} & - \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t},\; - \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text s}\\ - @{text "Bar' p::pat t::trm"} & - \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text p},\; - \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}\\ + @{text "Bar\<^isub>1 p::pat t::trm s::trm"} & + \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "t s"}\\ + @{text "Bar\<^isub>2 p::pat t::trm"} & + \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"}\\ \end{tabular} \end{center} \noindent since there is no overlap of binders. - Note that in the last example we wrote {\it\isacommand{bind}\;bn(p)\;\isacommand{in}\;p}. + Note that in the last example we wrote \isacommand{bind}~@{text "bn(p)"}~\isacommand{in}~@{text "p.."}. Whenever such a binding clause is present, we will call the corresponding binder \emph{recursive}. To see the purpose of such recursive binders, compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s in the following specification: @@ -1090,13 +1083,12 @@ \hspace{5mm}\phantom{$\mid$}\ldots\\ \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"} \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t}\\ - \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}\\ - \hspace{20mm}\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t}, - \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text as}\\ - \isacommand{and} {\it assn} =\\ + \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"} + \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\ + \isacommand{and} @{text "ass"} =\\ \hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\ \hspace{5mm}$\mid$~@{text "ACons name trm assn"}\\ - \isacommand{with} @{text "bn::assn \ atom list"}\\ + \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}} @@ -1109,14 +1101,39 @@ function and alpha-equivalence relation, which we are going to describe in the rest of this section. + In order to simplify matters below, we shall assume specifications + of term-calculi are \emph{completed}. By this we mean that + for every argument of a term-constructor that is \emph{not} + already part of a binding clause, we add implicitly a special \emph{empty} binding + clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "\"}. In case + of the lambda-calculus, the comletion is as follows: + + \begin{center} + \begin{tabular}{@ {}l@ {\hspace{-1mm}}} + \isacommand{nominal\_datatype} @{text lam} =\\ + \hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"} + \;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "x"}\\ + \hspace{5mm}$\mid$~@{text "App t\<^isub>1::lam t\<^isub>2::lam"} + \;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>1"}, + \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>2"}\\ + \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"} + \;\;\isacommand{bind}~@{text x} \isacommand{in} @{text t}\\ + \end{tabular} + \end{center} + + \noindent + The point of completion is that we can make definitions over the binding + clauses, which defined purely over arguments, turned out to be unwieldy. + Having dealt with all syntax matters, the problem now is how we can turn specifications into actual type definitions in Isabelle/HOL and then establish a reasoning infrastructure for them. As - Pottier and Cheney pointed out \cite{Pottier06,Cheney5}, we cannot in general - re-arrange arguments of + Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, by just + re-arranging the arguments of term-constructors so that binders and their bodies are next to each other, and - then use the type constructors @{text "abs_set"}, @{text "abs_res"} and - @{text "abs_list"} from Section \ref{sec:binders}. Therefore we will first + then use directly the type constructors @{text "abs_set"}, @{text "abs_res"} and + @{text "abs_list"} from Section \ref{sec:binders}, will result in an inadequate + representatation. Therefore we will first extract datatype definitions from the specification and then define expicitly an alpha-equivalence relation over them. @@ -1152,8 +1169,24 @@ \end{equation} The first non-trivial step we have to perform is the generation free-variable - functions from the specifications. Given the raw types @{text "ty\<^isub>1 \ ty\<^isub>n"} - we need to define free-variable functions + functions from the specifications. For atomic types we define the auxilary + free variable functions: + + \begin{center} + \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} + @{text "fv_atom a"} & @{text "="} & @{text "atom a"}\\ + @{text "fv_atom_set as"} & @{text "="} & @{text "atoms as"}\\ + @{text "fv_atom_list as"} & @{text "="} & @{text "atoms (set as)"}\\ + \end{tabular} + \end{center} + + \noindent + Like the coercion function @{text atom} used earlier, @{text "atoms"} coerces + the set of atoms to a set of the generic atom type. + It is defined as @{text "atoms as \ {atom a | a \ as}"}. + + Given the raw types @{text "ty\<^isub>1 \ ty\<^isub>n"} + we define now free-variable functions \begin{center} @{text "fv_ty\<^isub>1, \, fv_ty\<^isub>n"} @@ -1173,92 +1206,65 @@ bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function that calculates those unbound atoms. - While the idea behind these - free-variable functions is clear (they just collect all atoms that are not bound), - because of our rather complicated binding mechanisms their definitions are - somewhat involved. - Given a term-constructor @{text "C"} of type @{text ty} with argument types - \mbox{@{text "ty\<^isub>1 \ ty\<^isub>n"}}, the function - @{text "fv_ty (C x\<^isub>1 \ x\<^isub>n)"} will be the union of the values, @{text v}, - calculated below for each argument. - First we deal with the case that @{text "x\<^isub>i"} is a binder. From the binding clauses, - we can determine whether the argument is a shallow or deep - binder, and in the latter case also whether it is a recursive or - non-recursive binder. - % + While the idea behind these free-variable functions is clear (they just + collect all atoms that are not bound), because of our rather complicated + binding mechanisms their definitions are somewhat involved. Given a + term-constructor @{text "C"} of type @{text ty} and some associated binding + clauses, the function @{text "fv_ty (C x\<^isub>1 \ x\<^isub>n)"} will be + the union of the values, @{text v}, calculated below for each binding + clause. + \begin{equation}\label{deepbinder} \mbox{% \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} - $\bullet$ & @{term "v = {}"} provided @{text "x\<^isub>i"} is a shallow binder\\ - $\bullet$ & @{text "v = fv_bn x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep - non-recursive binder with the auxiliary binding function @{text "bn"}\\ - $\bullet$ & @{text "v = fv_ty\<^isub>i x\<^isub>i - bn x\<^isub>i"} provided @{text "x\<^isub>i"} is - a deep recursive binder with the auxiliary binding function @{text "bn"} + \multicolumn{2}{@ {}l}{Empty binding clauses of the form + \isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\ + $\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} is of type @{text "ty"}\smallskip\\ + \multicolumn{2}{@ {}l}{Shallow binders of the form + \isacommand{bind\_set}~@{text "x\<^isub>1\x\<^isub>n"}~\isacommand{in}~@{text "y\<^isub>1\y\<^isub>m"}:}\\ + $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \ fv_ty\<^isub>m y\<^isub>m) - (x\<^isub>1 \ \ \ x\<^isub>n)"} + provided the @{text "y\<^isub>i"} are of type @{text "ty\<^isub>i"}\smallskip\\ + \multicolumn{2}{@ {}l}{Deep binders of the form + \isacommand{bind\_set}~@{text "bn x"}~\isacommand{in}~@{text "y\<^isub>1\y\<^isub>m"}:}\\ + $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \ fv_ty\<^isub>m y\<^isub>m) - (bn x) \ (fv_bn x)"}\\ + $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \ fv_ty\<^isub>m y\<^isub>m) - (bn x)"}\\ + & provided the @{text "y\<^isub>i"} are of type @{text "ty\<^isub>i"}; the first + clause applies for @{text x} being a non-recursive deep binder, the + second for a recursive deep binder \end{tabular}} \end{equation} \noindent - The first clause states that shallow binders do not contribute to the - free variables; in the second clause, we have to collect all - variables that are left unbound by the binding function @{text "bn"}---this - is done with function @{text "fv_bn"}; in the third clause, since the - binder is recursive, we need to bind all variables specified by - @{text "bn"}---therefore we subtract @{text "bn x\<^isub>i"} from the free - variables of @{text "x\<^isub>i"}. + Similarly for the other binding modes. Note that in a non-recursive deep + binder, we have to add all atoms that are left unbound by the binding + function @{text "bn"}. For this we use the function @{text "fv_bn"}. Assume + for the constructor @{text "C"} the binding function equation is of the form @{text + "bn\<^isub>j (C x\<^isub>1 \ x\<^isub>n) = rhs"}. We again define a value + @{text v} which is exactly as in \eqref{deepbinder} for shallow and deep + binders. We only modify the clause for empty binding clauses as follows: - In case the argument is \emph{not} a binder, we need to consider - whether the @{text "x\<^isub>i"} is the body of one or more binding clauses. - In this case we first calculate the set @{text "bnds"} as follows: - either the corresponding binders are all shallow or there is a single deep binder. - In the former case we take @{text bnds} to be the union of all shallow - binders; in the latter case, we just take the set of atoms specified by the - corresponding binding function. The value for @{text "x\<^isub>i"} is then given by: - % - \begin{equation}\label{deepbody} + + \begin{equation}\label{bnemptybinder} \mbox{% \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} - $\bullet$ & @{text "v = {atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\ - $\bullet$ & @{text "v = (atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\ - $\bullet$ & @{text "v = (atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\ - $\bullet$ & @{text "v = (fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is one of the raw datatypes - corresponding to the types specified by the user\\ -% $\bullet$ & @{text "(fv\<^isup>\ x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a defined nominal datatype -% with a free-variable function @{text "fv\<^isup>\"}\\ - $\bullet$ & @{term "v = {}"} otherwise + \multicolumn{2}{@ {}l}{Empty binding clauses of the form + \isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\ + $\bullet$ & @{term "v = fv_ty\<^isub>i y"} provided @{text "y"} does not occur in @{text "rhs"} + and the free-variable function for the type of @{text "y"} is @{text "fv_ty\<^isub>i"}\\ + $\bullet$ & @{term "v = fv_bn\<^isub>i y"} provided @{text "y"} occurs in @{text "rhs"} + with a recursive call @{text "bn\<^isub>i y"}\\ + $\bullet$ & @{term "v = {}"} provided @{text "y"} occurs in @{text "rhs"}, + but without a recursive call\\ \end{tabular}} \end{equation} - \noindent - Like the coercion function @{text atom} used earlier, @{text "atoms"} coerces - the set of atoms to a set of the generic atom type. - It is defined as @{text "atoms as \ {atom a | a \ as}"}. - - The last case we need to consider is when @{text "x\<^isub>i"} is neither - a binder nor a body of an abstraction. In this case it is defined - as in \eqref{deepbody}, except that we do not need to subtract the - set @{text bnds}. + \noindent + The reason why we only have to treat the empty binding clauses specially in + the definition of @{text "fv_bn"} is that binding functions can only use arguments + that do not occur in binding clauses. Otherwise the @{text "bn"} function cannot + be lifted to alpha-equated terms. - The definitions of the free-variable functions for binding - functions are similar. For each binding function - @{text "bn\<^isub>j"} we need to define a free-variable function - @{text "fv_bn\<^isub>j"}. Given a term-constructor @{term "C"}, the - function @{text "fv_bn\<^isub>j(C x\<^isub>1 \ x\<^isub>n)"} is the union of the - values calculated for the arguments. For each argument @{term "x\<^isub>i"} - we know whether it appears in the @{term "rhs"} of the binding - function equation @{text "bn\<^isub>j (C x\<^isub>1 \ x\<^isub>n) = rhs"}. If it does not - appear in @{text "rhs"} we generate the premise according to the - rules for @{text "fv_ty"} described above in (\ref{deepbinder}--\ref{deepbody}). Otherwise: - \begin{center} - \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} - $\bullet$ & @{text "v = fv_bn x\<^isub>i"} provided @{text "rhs"} contains the - recursive call @{text "bn x\<^isub>i"}\medskip\\ - $\bullet$ & @{term "v = {}"} provided @{text "rhs"} contains - @{term "x\<^isub>i"} and @{term "x\<^isub>i"} is of atom type. - \end{tabular} - \end{center} - - \noindent To see how these definitions work in practice, let us reconsider the term-constructors @{text "Let"} and @{text "Let_rec"} from the example shown in \eqref{letrecs}. For this specification we need to define three free-variable functions, namely @@ -1266,20 +1272,19 @@ % \begin{center} \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} - @{text "fv\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "fv\<^bsub>bn\<^esub> as \ (fv\<^bsub>trm\<^esub> t - set (bn as))"}\\ - @{text "fv\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} &\\ - \multicolumn{3}{r}{@{text "(fv\<^bsub>assn\<^esub> as - set (bn as)) \ (fv\<^bsub>trm\<^esub> t - set (bn as))"}}\\[1mm] + @{text "fv\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fv\<^bsub>trm\<^esub> t - set (bn as)) \ fv\<^bsub>bn\<^esub> as"}\\ + @{text "fv\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fv\<^bsub>assn\<^esub> as \ fv\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm] - @{text "fv\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{text "[]"}\\ + @{text "fv\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\ @{text "fv\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "{atom a} \ (fv\<^bsub>trm\<^esub> t) \ (fv\<^bsub>assn\<^esub> as)"}\\[1mm] - @{text "fv\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{text "[]"}\\ + @{text "fv\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\ @{text "fv\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fv\<^bsub>trm\<^esub> t) \ (fv\<^bsub>bn\<^esub> as)"} \end{tabular} \end{center} \noindent - Since there are no binding clauses for the term-constructors @{text ANil} + Since there are only (implicit) empty binding clauses for the term-constructors @{text ANil} and @{text "ACons"}, the corresponding free-variable function @{text "fv\<^bsub>assn\<^esub>"} returns all atoms occuring in an assignment. The binding only takes place in @{text Let} and @{text "Let_rec"}. In the @{text @@ -1290,12 +1295,15 @@ "fv\<^bsub>bn\<^esub>"} is. In contrast, in @{text "Let_rec"} we have a recursive binder where we want to also bind all occurrences of the atoms in @{text "set (bn as)"} inside @{text "as"}. Therefore we have to subtract @{text - "set (bn as)"} from @{text "fv\<^bsub>assn\<^esub> as"}, as well as from - @{text "fv\<^bsub>trm\<^esub> t"}. An interesting point in this example is + "set (bn as)"} from @{text "fv\<^bsub>trm\<^esub> t"}, as well as from + @{text "fv\<^bsub>assn\<^esub> as"}. An interesting point in this example is that an assignment ``alone'' does not have any bound variables. Only in the context of a @{text Let} or @{text "Let_rec"} will some atoms become bound. This is a phenomenon - that has also been pointed out in \cite{ott-jfp}. We can also see that + that has also been pointed out in \cite{ott-jfp}. For us it is crucial, because + we would not be able to lift a @{text "bn"}-function that is defined over + arguments that are either binders or bodies. In that case @{text "bn"} would + not respect alpha-equivalence. We can also see that % \begin{equation}\label{bnprop} @{text "fv_ty x = bn x \ fv_bn x"}. @@ -1307,7 +1315,7 @@ Next we define alpha-equivalence relations for the types @{text "ty\<^isub>1, \, ty\<^isub>n"}. We call them @{text "\ty\<^isub>1, \, \ty\<^isub>n"}. Like with the free-variable functions, we also need to define auxiliary alpha-equivalence relations for the binding functions. - Say we have @{text "bn\<^isub>1, \, bn\<^isub>m"}, then we also define @{text "\bn\<^isub>1, \, \bn\<^isub>m"}. + Say we have binding functions @{text "bn\<^isub>1, \, bn\<^isub>m"}, then we also define @{text "\bn\<^isub>1, \, \bn\<^isub>m"}. To simplify our definitions we will use the following abbreviations for relations and free-variable acting on products. % @@ -1327,12 +1335,9 @@ \end{center} \noindent - For what follows, let us assume - @{text C} is of type @{text ty} and its arguments are given by @{text "C ty\<^isub>1 \ ty\<^isub>n"}. - The task is to specify what the premises of these clauses are. For this we - consider the pairs \mbox{@{text "(x\<^isub>i, y\<^isub>i)"}}, but instead of considering them in turn, it will - be easier to analyse these pairs according to ``clusters'' of the binding clauses. - Therefore we distinguish the following cases: + For what follows, let us assume @{text C} is of type @{text ty}. The task + is to specify what the premises of these clauses are. Again for this we + analyse the binding clauses and produce a corresponding premise. *} (*<*) consts alpha_ty ::'a @@ -1348,59 +1353,42 @@ fv_trm2 ("fv\<^bsub>assn\<^esub> \ fv\<^bsub>trm\<^esub>") (*>*) text {* - \begin{itemize} - \item The @{text "(x\<^isub>i, y\<^isub>i)"} is a body of shallow binder with type @{text "ty"}. We assume the - \mbox{@{text "(u\<^isub>1, v\<^isub>1),\,(u\<^isub>m, v\<^isub>m)"}} are the corresponding binders. For the binding mode - \isacommand{bind\_set} we generate the premise + \begin{equation}\label{alpha} + \mbox{% + \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} + \multicolumn{2}{@ {}l}{Empty binding clauses of the form + \isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "x\<^isub>i"}:}\\ + $\bullet$ & @{text "x\<^isub>i \ty y\<^isub>i"} provided @{text "x\<^isub>i"} and @{text "y\<^isub>i"} + are recursive arguments of @{text "C"}\\ + $\bullet$ & @{term "x\<^isub>i = y\<^isub>i"} provided @{text "x\<^isub>i"} and @{text "y\<^isub>i"} are + non-recursive arguments\smallskip\\ + \multicolumn{2}{@ {}l}{Shallow binders of the form + \isacommand{bind\_set}~@{text "x\<^isub>1\x\<^isub>n"}~\isacommand{in}~@{text "x'\<^isub>1\x'\<^isub>m"}:}\\ + $\bullet$ & Assume the bodies @{text "x'\<^isub>1\x'\<^isub>m"} are of type @{text "ty\<^isub>1\ty\<^isub>m"}, + @{text "R"} is @{text "\ty\<^isub>1 \ ... \ \ty\<^isub>m"} and @{text fv} is + @{text "fv_ty\<^isub>1 \ ... \ fv_ty\<^isub>m"}, then \begin{center} - @{term "\p. (u\<^isub>1 \ \ \ u\<^isub>m, x\<^isub>i) \gen alpha_ty fv_ty p (v\<^isub>1 \ \ \ v\<^isub>m, y\<^isub>i)"} - \end{center} - - For the binding mode \isacommand{bind}, we use $\approx_{\textit{list}}$, and for - binding mode \isacommand{bind\_res} we use $\approx_{\textit{res}}$ instead. - - \item The @{text "(x\<^isub>i, y\<^isub>i)"} is a deep non-recursive binder with type @{text "ty"} - and @{text bn} is corresponding the binding function. We assume - @{text "(u\<^isub>1, v\<^isub>1),\,(u\<^isub>m, v\<^isub>m)"} are the corresponding bodies with types @{text "ty\<^isub>1,\, ty\<^isub>m"}. - For the binding mode \isacommand{bind\_set} we generate two premises - % + @{term "\p. (x\<^isub>1 \ \ \ x\<^isub>n, (x'\<^isub>1,\,x'\<^isub>m)) \gen R fv p (y\<^isub>1 \ \ \ y\<^isub>n, (y'\<^isub>1,\,y'\<^isub>m))"} + \end{center}\\ + \multicolumn{2}{@ {}l}{Deep binders of the form + \isacommand{bind\_set}~@{text "bn x"}~\isacommand{in}~@{text "x'\<^isub>1\x'\<^isub>m"}:}\\ + $\bullet$ & Assume the bodies @{text "x'\<^isub>1\x'\<^isub>m"} are of type @{text "ty\<^isub>1\ty\<^isub>m"}, + @{text "R"} is @{text "\ty\<^isub>1 \ ... \ \ty\<^isub>m"} and @{text fv} is + @{text "fv_ty\<^isub>1 \ ... \ fv_ty\<^isub>m"}, then for recursive deep binders \begin{center} - @{text "x\<^isub>i \bn y\<^isub>i"}\hfill - @{term "\p. (bn x\<^isub>i, (u\<^isub>1,\,u\<^isub>m)) \gen R fv p (bn y\<^isub>i, (v\<^isub>1,\,v\<^isub>m))"} - \end{center} + @{term "\p. (bn x, (x'\<^isub>1,\,x'\<^isub>m)) \gen R fv p (bn y, (y'\<^isub>1,\,y'\<^isub>m))"} + \end{center}\\ + $\bullet$ & for non-recursive binders we generate in addition @{text "x \bn y"}\\ + \end{tabular}} + \end{equation} \noindent - where @{text R} is @{text "\ty\<^isub>1 \ ... \ \ty\<^isub>m"} and @{text fv} is - @{text "fv_ty\<^isub>1 \ ... \ fv_ty\<^isub>m"}. Similarly for the other binding modes. - - \item The @{text "(x\<^isub>i, y\<^isub>i)"} is a deep recursive binders with type @{text "ty"} - and @{text bn} is the corresponding binding function. We assume - @{text "(u\<^isub>1, v\<^isub>1),\,(u\<^isub>m, v\<^isub>m)"} are the corresponding bodies with types @{text "ty\<^isub>1,\, ty\<^isub>m"}. - For the binding mode \isacommand{bind\_set} we generate the premise - % - \begin{center} - @{term "\p. (bn x\<^isub>i, (x\<^isub>i, u\<^isub>1,\,u\<^isub>m)) \gen R fv p (bn y\<^isub>i, (y\<^isub>i, v\<^isub>1,\,v\<^isub>m))"} - \end{center} - - \noindent - where @{text R} is @{text "\ty \ \ty\<^isub>1 \ ... \ \ty\<^isub>m"} and @{text fv} is - @{text "fv_ty \ fv_ty\<^isub>1 \ ... \ fv_ty\<^isub>m"}. Similarly for the other modes. - \end{itemize} - - \noindent - From this definition it is clear why we can only support one binding mode per binder - and body, as we cannot mix the relations $\approx_{\textit{set}}$, $\approx_{\textit{list}}$ - and $\approx_{\textit{res}}$. It is also clear why we have to impose the restriction - of excluding overlapping binders, as these would need to be translated into separate + Similarly for the other binding modes. + From this definition it is clear why we have to impose the restriction + of excluding overlapping deep binders, as these would need to be translated into separate abstractions. - The only cases that are not covered by the rules above are the cases where @{text "(x\<^isub>i, y\<^isub>i)"} is - neither a binder nor a body in a binding clause. Then we just generate @{text "x\<^isub>i \ty y\<^isub>i"} provided - the type of @{text "x\<^isub>i"} and @{text "y\<^isub>i"} is @{text ty} and the arguments are - recursive arguments of the term-constructor. If they are non-recursive arguments, - then we generate the premise @{text "x\<^isub>i = y\<^isub>i"}. - The alpha-equivalence relations @{text "\bn\<^isub>j"} for binding functions are similar. We again have conclusions of the form \mbox{@{text "C x\<^isub>1 \ x\<^isub>n \bn C y\<^isub>1 \ y\<^isub>n"}}