762 permutation. However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"} |
762 permutation. However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"} |
763 $\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no |
763 $\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no |
764 permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal |
764 permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal |
765 (similarly for $\approx_{\,\textit{list}}$). It can also relatively easily be |
765 (similarly for $\approx_{\,\textit{list}}$). It can also relatively easily be |
766 shown that all three notions of alpha-equivalence coincide, if we only |
766 shown that all three notions of alpha-equivalence coincide, if we only |
767 abstract a single atom. |
767 abstract a single atom. In this case they also agree with alpha-equivalence |
|
768 used in older versions of Nominal Isabelle \cite{Urban08}. |
768 |
769 |
769 In the rest of this section we are going to show that the alpha-equivalences |
770 In the rest of this section we are going to show that the alpha-equivalences |
770 really lead to abstractions where some atoms are bound (or more precisely |
771 really lead to abstractions where some atoms are bound (or more precisely |
771 removed from the support). For this we will consider three abstraction |
772 removed from the support). For this we will consider three abstraction |
772 types that are quotients of the relations |
773 types that are quotients of the relations |
1152 compare `plain' @{text "Let"}s and @{text "Let_rec"}s in the following |
1153 compare `plain' @{text "Let"}s and @{text "Let_rec"}s in the following |
1153 specification: |
1154 specification: |
1154 |
1155 |
1155 \begin{equation}\label{letrecs} |
1156 \begin{equation}\label{letrecs} |
1156 \mbox{% |
1157 \mbox{% |
1157 \begin{tabular}{@ {}l@ {}} |
1158 \begin{tabular}{@ {}l@ {}l} |
1158 \isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\ |
1159 \isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\ |
1159 \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"} |
1160 \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"} |
1160 \;\;\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text t}\\ |
1161 & \hspace{-19mm}\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text t}\\ |
1161 \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"} |
1162 \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"} |
1162 \;\;\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\ |
1163 & \hspace{-19mm}\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\ |
1163 \isacommand{and} @{text "assn"} $=$\\ |
1164 \isacommand{and} @{text "assn"} $=$\\ |
1164 \hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\ |
1165 \hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\ |
1165 \hspace{5mm}$\mid$~@{text "ACons name trm assn"}\\ |
1166 \hspace{5mm}$\mid$~@{text "ACons name trm assn"}\\ |
1166 \isacommand{binder} @{text "bn::assn \<Rightarrow> atom list"}\\ |
1167 \isacommand{binder} @{text "bn::assn \<Rightarrow> atom list"}\\ |
1167 \isacommand{where}~@{text "bn(ANil) = []"}\\ |
1168 \isacommand{where}~@{text "bn(ANil) = []"}\\ |