370 be bound. Another is that each bound variable comes with a kind or type |
370 be bound. Another is that each bound variable comes with a kind or type |
371 annotation. Representing such binders with single binders and reasoning |
371 annotation. Representing such binders with single binders and reasoning |
372 about them in a theorem prover would be a major pain. \medskip |
372 about them in a theorem prover would be a major pain. \medskip |
373 |
373 |
374 \noindent |
374 \noindent |
375 {\bf Contributions:} We provide three novel definitions for when terms |
375 {\bf Contributions:} We provide three new definitions for when terms |
376 involving general binders are $\alpha$-equivalent. These definitions are |
376 involving general binders are $\alpha$-equivalent. These definitions are |
377 inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic |
377 inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic |
378 proofs, we establish a reasoning infrastructure for $\alpha$-equated |
378 proofs, we establish a reasoning infrastructure for $\alpha$-equated |
379 terms, including properties about support, freshness and equality |
379 terms, including properties about support, freshness and equality |
380 conditions for $\alpha$-equated terms. We are also able to derive strong |
380 conditions for $\alpha$-equated terms. We are also able to derive strong |
549 The main point of @{text supports} is that we can establish the following |
549 The main point of @{text supports} is that we can establish the following |
550 two properties. |
550 two properties. |
551 |
551 |
552 \begin{property}\label{supportsprop} |
552 \begin{property}\label{supportsprop} |
553 Given a set @{text "as"} of atoms. |
553 Given a set @{text "as"} of atoms. |
554 {\it i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]} |
554 {\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]} |
555 {\it ii)} @{thm supp_supports[no_vars]}. |
555 {\it (ii)} @{thm supp_supports[no_vars]}. |
556 \end{property} |
556 \end{property} |
557 |
557 |
558 Another important notion in the nominal logic work is \emph{equivariance}. |
558 Another important notion in the nominal logic work is \emph{equivariance}. |
559 For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant |
559 For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant |
560 it is required that every permutation leaves @{text f} unchanged, that is |
560 it is required that every permutation leaves @{text f} unchanged, that is |
1466 $\approx_{\,\textit{res}}$ and $\approx_{\,\textit{list}}$ for the other |
1466 $\approx_{\,\textit{res}}$ and $\approx_{\,\textit{list}}$ for the other |
1467 binding modes). This premise defines $\alpha$-equivalence of two abstractions |
1467 binding modes). This premise defines $\alpha$-equivalence of two abstractions |
1468 involving multiple binders. As above, we first build the tuples @{text "D"} and |
1468 involving multiple binders. As above, we first build the tuples @{text "D"} and |
1469 @{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding |
1469 @{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding |
1470 compound $\alpha$-relation @{text "R"} (shown in \eqref{rempty}). |
1470 compound $\alpha$-relation @{text "R"} (shown in \eqref{rempty}). |
1471 For $\approx_{\,\textit{set}}$ (respectively $\approx_{\,\textit{list}}$ and |
1471 For $\approx_{\,\textit{set}}$ we also need |
1472 $\approx_{\,\textit{res}}$) we also need |
|
1473 a compound free-atom function for the bodies defined as |
1472 a compound free-atom function for the bodies defined as |
1474 % |
1473 % |
1475 \begin{center} |
1474 \begin{center} |
1476 \mbox{@{text "fa \<equiv> (fa_ty\<^isub>1,\<dots>, fa_ty\<^isub>q)"}} |
1475 \mbox{@{text "fa \<equiv> (fa_ty\<^isub>1,\<dots>, fa_ty\<^isub>q)"}} |
1477 \end{center} |
1476 \end{center} |
1478 |
1477 |
1479 \noindent |
1478 \noindent |
1480 with assumption that the @{text "d"}$_{1..q}$ refer to arguments of types @{text "ty"}$_{1..q}$. |
1479 with the assumption that the @{text "d"}$_{1..q}$ refer to arguments of types @{text "ty"}$_{1..q}$. |
1481 The last ingredient we need are the sets of atoms bound in the bodies. |
1480 The last ingredient we need are the sets of atoms bound in the bodies. |
1482 For this we take |
1481 For this we take |
1483 |
1482 |
1484 \begin{center} |
1483 \begin{center} |
1485 @{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> \<dots> \<union> bn_ty\<^isub>p b\<^isub>p"}\;.\\ |
1484 @{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> \<dots> \<union> bn_ty\<^isub>p b\<^isub>p"}\;.\\ |
2177 section {* Conclusion *} |
2176 section {* Conclusion *} |
2178 |
2177 |
2179 text {* |
2178 text {* |
2180 We have presented an extension of Nominal Isabelle for dealing with |
2179 We have presented an extension of Nominal Isabelle for dealing with |
2181 general binders, that is term-constructors having multiple bound |
2180 general binders, that is term-constructors having multiple bound |
2182 variables. For this extension we introduced novel definitions of |
2181 variables. For this extension we introduced new definitions of |
2183 $\alpha$-equivalence and automated all necessary proofs in Isabelle/HOL. |
2182 $\alpha$-equivalence and automated all necessary proofs in Isabelle/HOL. |
2184 To specify general binders we used the specifications from Ott, but extended them |
2183 To specify general binders we used the specifications from Ott, but extended them |
2185 in some places and restricted |
2184 in some places and restricted |
2186 them in others so that they make sense in the context of $\alpha$-equated terms. |
2185 them in others so that they make sense in the context of $\alpha$-equated terms. |
2187 We have tried out the extension with terms from Core-Haskell, type-schemes |
2186 We have tried out the extension with terms from Core-Haskell, type-schemes |