302 \draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05); |
302 \draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05); |
303 |
303 |
304 \draw (-2.0, 0.845) -- (0.7,0.845); |
304 \draw (-2.0, 0.845) -- (0.7,0.845); |
305 \draw (-2.0,-0.045) -- (0.7,-0.045); |
305 \draw (-2.0,-0.045) -- (0.7,-0.045); |
306 |
306 |
307 \draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]clas.\end{tabular}}; |
307 \draw ( 0.7, 0.5) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]classes\end{tabular}}; |
308 \draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}}; |
308 \draw (-2.4, 0.5) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}}; |
309 \draw (1.8, 0.48) node[right=-0.1mm] |
309 \draw (1.8, 0.48) node[right=-0.1mm] |
310 {\small\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}}; |
310 {\small\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}}; |
311 \draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}}; |
311 \draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}}; |
312 \draw (-3.25, 0.55) node {\small\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}}; |
312 \draw (-3.25, 0.55) node {\small\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}}; |
313 |
313 |
659 from this specification (remember that Nominal Isabelle is a definitional |
659 from this specification (remember that Nominal Isabelle is a definitional |
660 extension of Isabelle/HOL, which does not introduce any new axioms). |
660 extension of Isabelle/HOL, which does not introduce any new axioms). |
661 |
661 |
662 In order to keep our work with deriving the reasoning infrastructure |
662 In order to keep our work with deriving the reasoning infrastructure |
663 manageable, we will wherever possible state definitions and perform proofs |
663 manageable, we will wherever possible state definitions and perform proofs |
664 on the ``user-level'' of Isabelle/HOL, as opposed to write custom ML-code that |
664 on the ``user-level'' of Isabelle/HOL, as opposed to writing custom ML-code that |
665 generates them anew for each specification. |
665 generates them anew for each specification. |
666 To that end, we will consider |
666 To that end, we will consider |
667 first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}. These pairs |
667 first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}. These pairs |
668 are intended to represent the abstraction, or binding, of the set of atoms @{text |
668 are intended to represent the abstraction, or binding, of the set of atoms @{text |
669 "as"} in the body @{text "x"}. |
669 "as"} in the body @{text "x"}. |
1282 new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"} |
1282 new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"} |
1283 given by the user. In our implementation we just use the affix ``@{text "_raw"}''. |
1283 given by the user. In our implementation we just use the affix ``@{text "_raw"}''. |
1284 But for the purpose of this paper, we use the superscript @{text "_\<^sup>\<alpha>"} to indicate |
1284 But for the purpose of this paper, we use the superscript @{text "_\<^sup>\<alpha>"} to indicate |
1285 that a notion is given for alpha-equivalence classes and leave it out |
1285 that a notion is given for alpha-equivalence classes and leave it out |
1286 for the corresponding notion given on the ``raw'' level. So for example |
1286 for the corresponding notion given on the ``raw'' level. So for example |
1287 we have @{text "ty\<^sup>\<alpha> \<mapsto> ty"} and @{text "C\<^sup>\<alpha> \<mapsto> C"} |
1287 we have @{text "ty\<^sup>\<alpha> / ty"} and @{text "C\<^sup>\<alpha> / C"} |
1288 where @{term ty} is the type used in the quotient construction for |
1288 where @{term ty} is the type used in the quotient construction for |
1289 @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor of the ``raw'' type @{text "ty"}, |
1289 @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor of the ``raw'' type @{text "ty"}, |
1290 respectively @{text "C\<^sup>\<alpha>"} is the corresponding term-constructor of @{text "ty\<^sup>\<alpha>"}. |
1290 respectively @{text "C\<^sup>\<alpha>"} is the corresponding term-constructor of @{text "ty\<^sup>\<alpha>"}. |
1291 |
1291 |
1292 The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are |
1292 The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are |
2592 *} |
2592 *} |
2593 |
2593 |
2594 section {* Conclusion *} |
2594 section {* Conclusion *} |
2595 |
2595 |
2596 text {* |
2596 text {* |
2597 %%Telsescopes by de Bruijn (AUTOMATH project does not provide an automatic infrastructure). |
|
2598 |
|
2599 |
2597 |
2600 We have presented an extension of Nominal Isabelle for dealing with general |
2598 We have presented an extension of Nominal Isabelle for dealing with general |
2601 binders, that is term-constructors having multiple bound variables. For this |
2599 binders, that is term-constructors having multiple bound variables. For this |
2602 extension we introduced new definitions of alpha-equivalence and automated |
2600 extension we introduced new definitions of alpha-equivalence and automated |
2603 all necessary proofs in Isabelle/HOL. To specify general binders we used |
2601 all necessary proofs in Isabelle/HOL. To specify general binders we used |
2651 {\bf Acknowledgements:} We are very grateful to Andrew Pitts for many |
2649 {\bf Acknowledgements:} We are very grateful to Andrew Pitts for many |
2652 discussions about Nominal Isabelle. We thank Peter Sewell for making the |
2650 discussions about Nominal Isabelle. We thank Peter Sewell for making the |
2653 informal notes \cite{SewellBestiary} available to us and also for patiently |
2651 informal notes \cite{SewellBestiary} available to us and also for patiently |
2654 explaining some of the finer points of the Ott-tool. Stephanie Weirich |
2652 explaining some of the finer points of the Ott-tool. Stephanie Weirich |
2655 suggested to separate the subgrammars of kinds and types in our Core-Haskell |
2653 suggested to separate the subgrammars of kinds and types in our Core-Haskell |
2656 example. |
2654 example. Ramana Kumar helped us with comments about an earlier version of |
|
2655 this paper. |
2657 *} |
2656 *} |
2658 |
2657 |
2659 |
2658 |
2660 (*<*) |
2659 (*<*) |
2661 end |
2660 end |