diff -r 6df6468f3c05 -r 028705c98304 Paper/Paper.thy --- a/Paper/Paper.thy Mon Apr 26 20:19:42 2010 +0200 +++ b/Paper/Paper.thy Tue Apr 27 12:23:06 2010 +0200 @@ -706,34 +706,6 @@ It can also relatively easily be shown that all tree notions of alpha-equivalence coincide, if we only abstract a single atom. - % 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 three abstraction types. For this we define % @@ -742,8 +714,8 @@ \end{equation} \noindent - (similarly for $\approx_{\textit{abs\_list}}$ - and $\approx_{\textit{abs\_res}}$). We can show that these relations are equivalence + (similarly for $\approx_{\textit{abs\_res}}$ + and $\approx_{\textit{abs\_list}}$). We can show that these relations are equivalence relations and equivariant. \begin{lemma}\label{alphaeq} @@ -866,11 +838,12 @@ Theorem~\ref{suppabs}. The method of first considering abstractions of the - form @{term "Abs as x"} etc is motivated by the fact that properties about them - can be conveninetly established at the Isabelle/HOL level. It would be - difficult to write custom ML-code that derives automatically such properties + form @{term "Abs as x"} etc is motivated by the fact that + we can conveniently establish at the Isabelle/HOL level + properties about them. It would be + laborious to write custom ML-code that derives automatically such properties for every term-constructor that binds some atoms. Also the generality of - the definitions for alpha-equivalence will help us in definitions in the next section. + the definitions for alpha-equivalence will help us in the next section. *} section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *} @@ -945,9 +918,22 @@ 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{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. + ``\isacommand{bind}-part'' will be called \emph{binders}. + + In contrast to Ott, we allow multiple labels in binders and bodies. For example + we permit binding clauses as follows: + + \begin{center} + \begin{tabular}{ll} + @{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 + There are a few restrictions we need to impose: First, a body can only occur in + \emph{one} binding clause of a term constructor. 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}\; @@ -978,17 +964,9 @@ \end{center} \noindent - Note that in this specification \emph{name} refers to an atom type. - 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 s::lam"} & - \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"} - \end{tabular} - \end{center} - + Note that in this specification @{text "name"} refers to an atom type, and + @{text "fset"} to the type of finite sets. + 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 @@ -1055,7 +1033,7 @@ 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 + we must exclude such specifications is that they cannot be represented by the general binders described in Section \ref{sec:binders}. However the following two term-constructors are allowed @@ -1071,10 +1049,11 @@ \noindent since there is no overlap of binders. - 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: + 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: % \begin{equation}\label{letrecs} \mbox{% @@ -1101,12 +1080,12 @@ 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 + In order to simplify some definitions, 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: + clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "label"}. In case + of the lambda-calculus, the completion produces \begin{center} \begin{tabular}{@ {}l@ {\hspace{-1mm}}} @@ -1123,17 +1102,15 @@ \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. + clauses and be sure to capture all arguments of a term constructor. Having dealt with all syntax matters, the problem now is how we can turn specifications into actual type definitions in Isabelle/HOL and then establish a reasoning infrastructure for them. As - Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, by just + Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, just re-arranging the arguments of - term-constructors so that binders and their bodies are next to each other, and - 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 + term-constructors so that binders and their bodies are next to each other will + result in inadequate representations. Therefore we will first extract datatype definitions from the specification and then define expicitly an alpha-equivalence relation over them. @@ -1181,12 +1158,12 @@ \end{center} \noindent - Like the coercion function @{text atom} used earlier, @{text "atoms"} coerces + Like the coercion function @{text atom}, @{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 + Given the raw types @{text "ty\<^isub>1 \ ty\<^isub>n"} we define now the + free-variable functions \begin{center} @{text "fv_ty\<^isub>1, \, fv_ty\<^isub>n"} @@ -1210,24 +1187,25 @@ 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. - + clauses @{text bcs}, the result of the @{text "fv_ty (C x\<^isub>1 \ x\<^isub>n)"} will be + the union of the values, @{text v}, calculated by the rules for empty, shallow and + deep binding clauses: + % \begin{equation}\label{deepbinder} \mbox{% \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} - \multicolumn{2}{@ {}l}{Empty binding clauses of the form - \isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\ + \multicolumn{2}{@ {}l}{\isacommand{bind}~@{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)"}\\ + + \multicolumn{2}{@ {}l}{\isacommand{bind}~@{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)"}\\ + & \hspace{10mm}@{text "- (fv_aty\<^isub>1 x\<^isub>1 \ .. \ fv_aty\<^isub>n x\<^isub>n)"}\\ + & provided the bodies @{text "y"}$_{1..m}$ are of type @{text "ty"}$_{1..m}$ and the + binders @{text "x"}$_{1..n}$ of atomic types @{text "aty"}$_{1..n}$\smallskip\\ + + \multicolumn{2}{@ {}l}{\isacommand{bind}~@{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 @@ -1237,22 +1215,20 @@ \noindent 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 + function @{text "bn"}. For this we define the function @{text "fv_bn"}. Assume + for the constructor @{text "C"} the binding function 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: - - + binding clauses, except for empty binding clauses are defined as follows: + % \begin{equation}\label{bnemptybinder} \mbox{% \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} - \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"}\\ + \multicolumn{2}{@ {}l}{\isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\ + $\bullet$ & @{term "v = fv_ty 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"}\\ + $\bullet$ & @{term "v = fv_bn y"} provided @{text "y"} occurs in @{text "rhs"} + with a recursive call @{text "bn y"}\\ $\bullet$ & @{term "v = {}"} provided @{text "y"} occurs in @{text "rhs"}, but without a recursive call\\ \end{tabular}} @@ -1559,7 +1535,7 @@ alpha-equivalence relations are equivariant, which we already established in Lemma~\ref{equiv}. As a result we can establish the equations - \begin{equation}\label{ceqvt} + \begin{equation}\label{calphaeqvt} @{text "p \ (C\<^sup>\ x\<^isub>1 \ x\<^isub>n) = C\<^sup>\ (p \ x\<^isub>1) \ (p \ x\<^isub>n)"} \end{equation}