544 in some cases it can be difficult to characterise the support precisely, and |
544 in some cases it can be difficult to characterise the support precisely, and |
545 only an approximation can be established (see \eqref{suppfun} above). Reasoning about |
545 only an approximation can be established (see \eqref{suppfun} above). Reasoning about |
546 such approximations can be simplified with the notion \emph{supports}, defined |
546 such approximations can be simplified with the notion \emph{supports}, defined |
547 as follows: |
547 as follows: |
548 |
548 |
549 \begin{defn} |
549 \begin{definition} |
550 A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b} |
550 A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b} |
551 not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}. |
551 not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}. |
552 \end{defn} |
552 \end{definition} |
553 |
553 |
554 \noindent |
554 \noindent |
555 The main point of @{text supports} is that we can establish the following |
555 The main point of @{text supports} is that we can establish the following |
556 two properties. |
556 two properties. |
557 |
557 |
777 indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will |
777 indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will |
778 call the types \emph{abstraction types} and their elements |
778 call the types \emph{abstraction types} and their elements |
779 \emph{abstractions}. The important property we need to derive is the support of |
779 \emph{abstractions}. The important property we need to derive is the support of |
780 abstractions, namely: |
780 abstractions, namely: |
781 |
781 |
782 \begin{thm}[Support of Abstractions]\label{suppabs} |
782 \begin{theorem}[Support of Abstractions]\label{suppabs} |
783 Assuming @{text x} has finite support, then\\[-6mm] |
783 Assuming @{text x} has finite support, then\\[-6mm] |
784 \begin{center} |
784 \begin{center} |
785 \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l} |
785 \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l} |
786 @{thm (lhs) supp_Abs(1)[no_vars]} & $=$ & @{thm (rhs) supp_Abs(1)[no_vars]}\\ |
786 @{thm (lhs) supp_Abs(1)[no_vars]} & $=$ & @{thm (rhs) supp_Abs(1)[no_vars]}\\ |
787 @{thm (lhs) supp_Abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_Abs(2)[no_vars]}\\ |
787 @{thm (lhs) supp_Abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_Abs(2)[no_vars]}\\ |
788 @{thm (lhs) supp_Abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_Abs(3)[where bs="as", no_vars]} |
788 @{thm (lhs) supp_Abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_Abs(3)[where bs="as", no_vars]} |
789 \end{tabular} |
789 \end{tabular} |
790 \end{center} |
790 \end{center} |
791 \end{thm} |
791 \end{theorem} |
792 |
792 |
793 \noindent |
793 \noindent |
794 Below we will show the first equation. The others |
794 Below we will show the first equation. The others |
795 follow by similar arguments. By definition of the abstraction type @{text "abs_set"} |
795 follow by similar arguments. By definition of the abstraction type @{text "abs_set"} |
796 we have |
796 we have |
2086 all the unwanted consequences when reasoning about the resulting terms. |
2086 all the unwanted consequences when reasoning about the resulting terms. |
2087 |
2087 |
2088 Two formalisations involving general binders have been |
2088 Two formalisations involving general binders have been |
2089 performed in older |
2089 performed in older |
2090 versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W |
2090 versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W |
2091 \cite{BengtsonParow09, UrbanNipkow09}). Both |
2091 \cite{BengtsonParow09,UrbanNipkow09}). Both |
2092 use the approach based on iterated single binders. Our experience with |
2092 use the approach based on iterated single binders. Our experience with |
2093 the latter formalisation has been disappointing. The major pain arose from |
2093 the latter formalisation has been disappointing. The major pain arose from |
2094 the need to ``unbind'' variables. This can be done in one step with our |
2094 the need to ``unbind'' variables. This can be done in one step with our |
2095 general binders described in this paper, but needs a cumbersome |
2095 general binders described in this paper, but needs a cumbersome |
2096 iteration with single binders. The resulting formal reasoning turned out to |
2096 iteration with single binders. The resulting formal reasoning turned out to |