diff -r 3c8d3aaf292c -r 8d7d85e915b5 LMCS-Paper/Paper.thy --- a/LMCS-Paper/Paper.thy Tue Sep 06 12:18:02 2011 +0100 +++ b/LMCS-Paper/Paper.thy Wed Sep 07 12:38:32 2011 +0100 @@ -101,7 +101,7 @@ 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 below the first pair of type-schemes as alpha-equivalent, + 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: @@ -378,7 +378,7 @@ 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''. + for our specifications from ``first principles'' inside a theorem prover. \begin{figure} @@ -431,14 +431,14 @@ 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 "\, \"} to stand for - permutations. 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. + sort-respecting permutations of atoms. We will use the letters @{text "a, b, + c, \"} to stand for atoms and @{text "\, \"} 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 @@ -487,7 +487,7 @@ \begin{equation}\label{suppdef} @{thm supp_def[no_vars, THEN eq_reflection]} - \end{equation} + \end{equation}\smallskip \noindent There is also the derived notion for when an atom @{text a} is \emph{fresh} @@ -508,7 +508,7 @@ \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]} + then @{thm (concl) swap_fresh_fresh[no_vars]}. \end{prop} While often the support of an object can be relatively easily @@ -539,7 +539,7 @@ 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} + 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} @@ -548,8 +548,10 @@ two properties. \begin{prop}\label{supportsprop} - Given a set @{text "as"} of atoms. - {\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]} + Given a set @{text "as"} of atoms.\\ + {\it (i)} If @{thm (prem 1) supp_is_subset[where S="as", no_vars]} + and @{thm (prem 2) supp_is_subset[where S="as", no_vars]} then + @{thm (concl) supp_is_subset[where S="as", no_vars]}.\\ {\it (ii)} @{thm supp_supports[no_vars]}. \end{prop} @@ -558,17 +560,17 @@ it is required that every permutation leaves @{text f} unchanged, that is \begin{equation}\label{equivariancedef} - @{term "\p. p \ f = f"} - \end{equation} + @{term "\\. \ \ f = f"} + \end{equation}\smallskip \noindent or equivalently that a permutation applied to the application @{text "f x"} can be moved to the argument @{text x}. That means for equivariant - functions @{text f}, we have for all permutations @{text p}: + functions @{text f}, we have for all permutations @{text "\"}: \begin{equation}\label{equivariance} - @{text "p \ f = f"} \;\;\;\textit{if and only if}\;\;\; - @{text "p \ (f x) = f (p \ x)"} - \end{equation} + @{text "\ \ f = f"} \;\;\;\;\textit{if and only if}\;\;\;\; + @{text "\ \ (f x) = f (\ \ x)"} + \end{equation}\smallskip \noindent From property \eqref{equivariancedef} and the definition of @{text supp}, we @@ -577,7 +579,7 @@ that \begin{center} - @{text "x R y"} \;\;\textit{implies}\;\; @{text "(p \ x) R (p \ y)"} + @{text "x R y"} \;\;\textit{implies}\;\; @{text "(\ \ x) R (\ \ y)"} \end{center} Using freshness, the nominal logic work provides us with general means for renaming @@ -585,35 +587,34 @@ \noindent While in the older version of Nominal Isabelle, we used extensively - Property~\ref{swapfreshfresh} - this property to rename single binders, it this property + Property~\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[no_vars]} + @{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 p} such that @{term "(p \ as) \* c"} and - @{term "supp x \* p"}. + 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 p} such that - the renamed binders @{term "p \ as"} avoid @{text c} (which can be arbitrarily chosen - as long as it is finitely supported) and also @{text "p"} does not affect anything - in the support of @{text x} (that is @{term "supp x \* p"}). The last + 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 "p \ x = x"}. + @{text as} in @{text x}, because @{term "\ \ x = x"}. 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 - extensive use of these properties in order to define alpha-equivalence in + use of these properties in order to define alpha-equivalence in the presence of multiple binders. *} @@ -628,7 +629,7 @@ 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 + 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 @@ -641,48 +642,48 @@ 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 x} and @{text y} need to have the same set of free - atoms; moreover there must be a permutation @{text p} such that {\it - (ii)} @{text p} leaves the free atoms of @{text x} and @{text y} unchanged, but + atoms; moreover there must be a permutation @{text \} such that {\it + (ii)} @{text \} leaves the free atoms 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 that {\it (iv)} - @{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The + @{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 the conjunction of: - % - \begin{equation}\label{alphaset} - \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l} - \multicolumn{4}{l}{@{term "(as, x) \set R fa p (bs, y)"}\hspace{2mm}@{text "\"}}\\[1mm] - \mbox{\it (i)} & @{term "fa(x) - as = fa(y) - bs"} & - \mbox{\it (iii)} & @{text "(p \ x) R y"} \\ - \mbox{\it (ii)} & @{term "(fa(x) - as) \* p"} & - \mbox{\it (iv)} & @{term "(p \ as) = bs"} \\ - \end{array} - \end{equation} - % + + \begin{defi}[Alpha-Equivalence for Set-Bindings]\label{alphaset}\mbox{}\\ + \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl} + @{term "(as, x) \set R fa \ (bs, y)"}\hspace{2mm}@{text "\"} + & \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 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 + "\"}; alpha-equivalence between two pairs is then the relation where we + existentially quantify over this @{text "\"}. Also 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}}$ 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"}. - The definition in \eqref{alphaset} does not make any distinction between the + 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{equation}\label{alphalist} - \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l} - \multicolumn{4}{l}{@{term "(as, x) \lst R fa p (bs, y)"}\hspace{2mm}@{text "\"}}\\[1mm] - \mbox{\it (i)} & @{term "fa(x) - (set as) = fa(y) - (set bs)"} & - \mbox{\it (iii)} & @{text "(p \ x) R y"}\\ - \mbox{\it (ii)} & @{term "(fa(x) - set as) \* p"} & - \mbox{\it (iv)} & @{term "(p \ as) = bs"}\\ - \end{array} - \end{equation} - % + + \begin{defi}[Alpha-Equivalence for List-Bindings]\label{alphalist}\mbox{}\\ + \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl} + @{term "(as, x) \lst R fa \ (bs, y)"}\hspace{2mm}@{text "\"} + & \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} @@ -690,38 +691,39 @@ If we do not want to make any difference between the order of binders \emph{and} also allow vacuous binders, that means \emph{restrict} names, then we keep sets of binders, but drop - condition {\it (iv)} in \eqref{alphaset}: - % - \begin{equation}\label{alphares} - \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l} - \multicolumn{2}{l}{@{term "(as, x) \res R fa p (bs, y)"}\hspace{2mm}@{text "\"}}\\[1mm] - \mbox{\it (i)} & @{term "fa(x) - as = fa(y) - bs"} & - \mbox{\it (iii)} & @{text "(p \ x) R y"}\\ - \mbox{\it (ii)} & @{term "(fa(x) - as) \* p"}\\ - \end{array} - \end{equation} + 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 "(as, x) \res R fa \ (bs, y)"}\hspace{2mm}@{text "\"} + & \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 - % - \begin{center} + + \[ @{text "fa(x) = {x}"} \hspace{5mm} @{text "fa(T\<^isub>1 \ T\<^isub>2) = fa(T\<^isub>1) \ fa(T\<^isub>2)"} - \end{center} + \]\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 "({y, x}, y \ x)"} are alpha-equivalent according to - $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{set+}}$ by taking @{text p} 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 p} to be the identity + @{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 @@ -731,15 +733,18 @@ In the rest of this section we are going to introduce three abstraction types. For this we define - % + \begin{equation} - @{term "abs_set (as, x) (bs, x) \ \p. alpha_set (as, x) equal supp p (bs, x)"} + \begin{array}{l} + @{term "abs_set (as, x) (bs, x) \ \\. alpha_set (as, x) equal supp \ (bs, x)"}\\ + @{term "abs_res (as, x) (bs, x) \ \\. alpha_res (as, x) equal supp \ (bs, x)"}\\ + @{term "abs_lst (as, x) (bs, x) \ \\. alpha_lst (as, x) equal supp \ (bs, x)"}\\ + \end{array} \end{equation} \noindent - (similarly for $\approx_{\,\textit{abs\_set+}}$ - and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence - relations. %% and equivariant. + We can show that these relations are equivalence + relations and equivariant. \begin{lem}\label{alphaeq} The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$ @@ -749,10 +754,10 @@ \end{lem} \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 conditions are then by simple + Reflexivity is by taking @{text "\"} to be @{text "0"}. For symmetry we have + a permutation @{text p} 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"}. All conditions are then by simple calculations. \end{proof}