diff -r 157e8a4a6556 -r f11dd09fa3a7 Paper/Paper.thy --- a/Paper/Paper.thy Sun May 23 16:45:00 2010 +0100 +++ b/Paper/Paper.thy Mon May 24 22:47:06 2010 +0100 @@ -556,7 +556,7 @@ \noindent From property \eqref{equivariancedef} and the definition of @{text supp}, we - can be easily deduce that equivariant functions have empty support. There is + can easily deduce that equivariant functions have empty support. There is also a similar notion for equivariant relations, say @{text R}, namely the property that % @@ -593,7 +593,7 @@ Most properties given in this section are described in detail in \cite{HuffmanUrban10} and of course all are formalised in Isabelle/HOL. In the next sections we will make - extensively use of these properties in order to define alpha-equivalence in + extensive use of these properties in order to define alpha-equivalence in the presence of multiple binders. *} @@ -623,7 +623,7 @@ variables; moreover there must be a permutation @{text p} such that {\it ii)} @{text p} 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 equivalent terms. We also require {\it iv)} that + say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it iv)} @{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The requirements {\it i)} to {\it iv)} can be stated formally as follows: % @@ -638,7 +638,7 @@ \end{equation} \noindent - Note that this relation is dependent on the permutation @{text + Note that this relation depends on the permutation @{text "p"}. Alpha-equivalence between two pairs is then the relation where we existentially quantify over this @{text "p"}. Also note that the relation is dependent on a free-variable function @{text "fv"} and a relation @{text @@ -692,20 +692,20 @@ \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 alpha-equivalent 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}}$). - It can also relatively easily be shown that all tree notions of alpha-equivalence - coincide, if we only abstract a single atom. + @{text "({y, x}, y \ x)"} are alpha-equivalent 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}}$). It can also relatively easily be + shown that all tree notions of alpha-equivalence coincide, if we only + abstract a single atom. In the rest of this section we are going to introduce three abstraction types. For this we define @@ -941,16 +941,16 @@ of the specification (the corresponding alpha-equivalence will differ). We will show this later with an example. - There are some restrictions we need to impose: First, a body can only occur - in \emph{one} binding clause of a term constructor. For binders we - distinguish between \emph{shallow} and \emph{deep} binders. Shallow binders - are just labels. The restriction we need to impose on them is that in case - of \isacommand{bind\_set} and \isacommand{bind\_res} the labels must either - refer to atom types or to sets of atom types; in case of \isacommand{bind} - the labels must refer to atom types or lists of atom types. Two examples for - the use of shallow binders are the specification of lambda-terms, where a - single name is bound, and type-schemes, where a finite set of names is - bound: + There are some restrictions we need to impose on binding clasues: First, a + body can only occur in \emph{one} binding clause of a term constructor. For + binders we distinguish between \emph{shallow} and \emph{deep} binders. + Shallow binders are just labels. The restriction we need to impose on them + is that in case of \isacommand{bind\_set} and \isacommand{bind\_res} the + labels must either refer to atom types or to sets of atom types; in case of + \isacommand{bind} the labels must refer to atom types or lists of atom + types. Two examples for the use of shallow binders are the specification of + lambda-terms, where a single name is bound, and type-schemes, where a finite + set of names is bound: \begin{center} \begin{tabular}{@ {}cc@ {}} @@ -974,7 +974,7 @@ \noindent Note that for @{text lam} it does not matter which binding mode we use. The reason is that we bind only a single @{text name}. However, having - \isacommand{bind\_set} or \isacommand{bind} in the second case makes again a + \isacommand{bind\_set} or \isacommand{bind} in the second case makes a difference to the semantics of the specification. Note also that in these specifications @{text "name"} refers to an atom type, and @{text "fset"} to the type of finite sets.