760 @{term "alpha_abs_lst (as, x) (bs, y)"}~~@{text "\<equiv>"}~~@{term "alpha_lst_ex (as, x) equal supp (bs, y)"}\\ |
760 @{term "alpha_abs_lst (as, x) (bs, y)"}~~@{text "\<equiv>"}~~@{term "alpha_lst_ex (as, x) equal supp (bs, y)"}\\ |
761 \end{array} |
761 \end{array} |
762 \end{equation}\smallskip |
762 \end{equation}\smallskip |
763 |
763 |
764 \noindent |
764 \noindent |
765 In these relation we replaced the free-atom function @{text "fa"} with @{term "supp"} and the |
765 Note that in these relation we replaced the free-atom function @{text "fa"} |
766 relation @{text R} with equality. We can show the following properties: |
766 with @{term "supp"} and the relation @{text R} with equality. We can show |
|
767 the following properties: |
|
768 |
767 |
769 |
768 \begin{lem}\label{alphaeq} |
770 \begin{lem}\label{alphaeq} |
769 The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_set+}}$ |
771 The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_set+}}$ |
770 and $\approx_{\,\textit{abs\_list}}$ are equivalence relations and equivariant. |
772 and $\approx_{\,\textit{abs\_list}}$ are equivalence relations and equivariant. |
771 \end{lem} |
773 \end{lem} |
1173 \noindent |
1175 \noindent |
1174 In this example the term constructor @{text "ACons"} contains a binding |
1176 In this example the term constructor @{text "ACons"} contains a binding |
1175 clause, and also is used in the definition of the binding function. The |
1177 clause, and also is used in the definition of the binding function. The |
1176 restriction we have to impose is that the binding function can only return |
1178 restriction we have to impose is that the binding function can only return |
1177 free atoms, that is the ones that are not mentioned in a binding clause. |
1179 free atoms, that is the ones that are not mentioned in a binding clause. |
1178 Therefore @{text "y"} cannot be used in the binding function, @{text "bn"} |
1180 Therefore @{text "y"} cannot be used in the binding function @{text "bn"} |
1179 (since it is bound in @{text "ACons"} by the binding clause), but @{text x} |
1181 (since it is bound in @{text "ACons"} by the binding clause), but @{text x} |
1180 can (since it is a free atom). This restriction is sufficient for lifting |
1182 can (since it is a free atom). This restriction is sufficient for lifting |
1181 the binding function to alpha-equated terms. If we would allow that @{text "bn"} |
1183 the binding function to alpha-equated terms. If we would permit that @{text "bn"} |
1182 can return also @{text "y"}, then it would not be respectful and therefore |
1184 can also return @{text "y"}, then it would not be respectful and therefore |
1183 cannot be lifted. |
1185 cannot be lifted. |
1184 |
1186 |
1185 In the version of Nominal Isabelle described here, we also adopted the |
1187 In the version of Nominal Isabelle described here, we also adopted the |
1186 restriction from the Ott-tool that binding functions can only return: the |
1188 restriction from the Ott-tool that binding functions can only return: the |
1187 empty set or empty list (as in case @{text ANil}), a singleton set or |
1189 empty set or empty list (as in case @{text ANil}), a singleton set or |