# HG changeset patch # User Christian Urban # Date 1315609422 -3600 # Node ID c5de60da0bcf0f95b176d4e1ab9f5cb5e6de8c58 # Parent 4baa2fccfb6142f89682faa55068a5aabab8e687 more diff -r 4baa2fccfb61 -r c5de60da0bcf LMCS-Paper/Paper.thy --- a/LMCS-Paper/Paper.thy Fri Sep 09 17:11:38 2011 +0100 +++ b/LMCS-Paper/Paper.thy Sat Sep 10 00:03:42 2011 +0100 @@ -762,8 +762,10 @@ \end{equation}\smallskip \noindent - In these relation we replaced the free-atom function @{text "fa"} with @{term "supp"} and the - relation @{text R} with equality. We can show the following properties: + Note that in these relation we replaced the free-atom function @{text "fa"} + with @{term "supp"} and the relation @{text R} with equality. We can show + the following properties: + \begin{lem}\label{alphaeq} The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_set+}}$ @@ -1175,11 +1177,11 @@ clause, and also is used in the definition of the binding function. The restriction we have to impose is that the binding function can only return free atoms, that is the ones that are not mentioned in a binding clause. - Therefore @{text "y"} cannot be used in the binding function, @{text "bn"} + Therefore @{text "y"} cannot be used in the binding function @{text "bn"} (since it is bound in @{text "ACons"} by the binding clause), but @{text x} can (since it is a free atom). This restriction is sufficient for lifting - the binding function to alpha-equated terms. If we would allow that @{text "bn"} - can return also @{text "y"}, then it would not be respectful and therefore + the binding function to alpha-equated terms. If we would permit that @{text "bn"} + can also return @{text "y"}, then it would not be respectful and therefore cannot be lifted. In the version of Nominal Isabelle described here, we also adopted the