20 If ("if _ then _ else _" 10) and |
22 If ("if _ then _ else _" 10) and |
21 alpha_gen ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and |
23 alpha_gen ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and |
22 alpha_lst ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and |
24 alpha_lst ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and |
23 alpha_res ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and |
25 alpha_res ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and |
24 abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and |
26 abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and |
|
27 abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup> _") and |
|
28 alpha2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{\#{}list}}$}}>\<^bsup>_, _, _\<^esup> _") and |
25 fv ("fv'(_')" [100] 100) and |
29 fv ("fv'(_')" [100] 100) and |
26 equal ("=") and |
30 equal ("=") and |
27 alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and |
31 alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and |
28 Abs ("[_]\<^raw:$\!$>\<^bsub>set\<^esub>._" [20, 101] 999) and |
32 Abs ("[_]\<^raw:$\!$>\<^bsub>set\<^esub>._" [20, 101] 999) and |
29 Abs_lst ("[_]\<^raw:$\!$>\<^bsub>list\<^esub>._") and |
33 Abs_lst ("[_]\<^raw:$\!$>\<^bsub>list\<^esub>._") and |
1880 We have presented an extension for Nominal Isabelle in order to derive a |
1883 We have presented an extension for Nominal Isabelle in order to derive a |
1881 convenient reasoning infrastructure for term-constructors binding multiple |
1884 convenient reasoning infrastructure for term-constructors binding multiple |
1882 variables at once. This extension can deal with term-calculi such as |
1885 variables at once. This extension can deal with term-calculi such as |
1883 Core-Haskell. For such calculi, we can also derive strong induction |
1886 Core-Haskell. For such calculi, we can also derive strong induction |
1884 principles that have the usual variable already built in. At the moment we |
1887 principles that have the usual variable already built in. At the moment we |
1885 can do so only with some manual help, but future work will automate them |
1888 can do so only with manual help, but future work will automate them |
1886 completely. The code underlying this extension will become part of the |
1889 completely. The code underlying this extension will become part of the |
1887 Isabelle distribution, but for the moment it can be downloaded from the |
1890 Isabelle distribution, but for the moment it can be downloaded from the |
1888 Mercurial repository linked at |
1891 Mercurial repository linked at |
1889 \href{http://isabelle.in.tum.de/nominal/download} |
1892 \href{http://isabelle.in.tum.de/nominal/download} |
1890 {http://isabelle.in.tum.de/nominal/download}. |
1893 {http://isabelle.in.tum.de/nominal/download}. |
1891 |
1894 |
1892 We have left out a discussion about how functions can be defined |
1895 We have left out a discussion about how functions can be defined |
1893 over alpha-equated terms. In earlier work \cite{UrbanBerghofer06} |
1896 over alpha-equated terms with general binders. In earlier work \cite{UrbanBerghofer06} |
1894 this turned out to be a thorny issue in the old Nominal Isabelle. |
1897 this turned out to be a thorny issue for Nominal Isabelle. |
1895 We hope to do better this time by using the function package that |
1898 We hope to do better this time by using the function package that |
1896 has recently been implemented in Isabelle/HOL and by restricting |
1899 has recently been implemented in Isabelle/HOL and also by restricting |
1897 function definitions to equivariant functions (for such functions |
1900 function definitions to equivariant functions (for such functions |
1898 it is possible to provide more automation). |
1901 it is possible to provide more automation). |
1899 |
1902 |
1900 There are some restrictions we imposed, like absence of nested type |
1903 There are some restrictions we imposed, like the absence of nested type |
1901 definitions that allow one to specify the function kinds as |
1904 definitions that allow one to specify the function kinds as |
1902 @{text "TFun string (ty list)"} instead of the unfolded version |
1905 @{text "TFun string (ty list)"} instead of the unfolded version |
1903 @{text "TFun string ty_list"} in Figure~\ref{nominalcorehas}, that |
1906 @{text "TFun string ty_list"} in Figure~\ref{nominalcorehas}; such |
1904 can be easily lifted. They essentially amount only to a more |
1907 restrictions can be easily lifted. They essentially amount to a more |
1905 clever implementation. More interesting is lifting our restriction |
1908 clever implementation than we have at the moment. More interesting is |
1906 about overlapping deep binders. |
1909 lifting our restriction about overlapping deep binders. Given our |
1907 |
1910 current setup, we cannot deal with specifications such as |
1908 Complication when the single scopedness restriction is lifted (two |
1911 |
1909 overlapping permutations) |
1912 \begin{center} |
1910 |
1913 \begin{tabular}{ll} |
1911 Future work: distinct list abstraction |
1914 @{text "Foo r::pat s::pat t::trm"} & |
1912 |
1915 \isacommand{bind} @{text "bn(r)"} \isacommand{in} @{text t},\; |
|
1916 \isacommand{bind} @{text "bn(s)"} \isacommand{in} @{text t} |
|
1917 \end{tabular} |
|
1918 \end{center} |
|
1919 |
|
1920 \noindent |
|
1921 where the deep binders @{text "bn(r)"} and @{text "bn(s)"} overlap.. |
|
1922 We would need to implement such bindings with alpha-equivalences like |
|
1923 |
|
1924 \begin{center} |
|
1925 @{term "\<exists>p q. abs_set2 (bn r\<^isub>1, t\<^isub>1) p (bn r\<^isub>2, t\<^isub>2) \<and> abs_set2 (bn s\<^isub>1, t\<^isub>1) q (bn s\<^isub>2, t\<^isub>2)"} |
|
1926 \end{center} |
|
1927 |
|
1928 \noindent |
|
1929 or |
|
1930 |
|
1931 \begin{center} |
|
1932 @{term "\<exists>p q. abs_set2 (bn r\<^isub>1 \<union> bn s\<^isub>1, t\<^isub>1) (p + q) (bn r\<^isub>2 \<union> bn s\<^isub>2, t\<^isub>2)"} |
|
1933 \end{center} |
|
1934 |
|
1935 \noindent |
|
1936 Both versions require two permutations (for each binding). But unfortunately the |
|
1937 first version cannot not work since it leaves unbound atoms that should be |
|
1938 bound by the respective other binder. This problem is avoided in the second |
|
1939 version, but at the expense that the two permutations can interfere with each |
|
1940 other. We have not yet been able to find a way to avoid such interferences. |
|
1941 On the other hand, such bindings can be made sense of \cite{SewellBestiary}. |
|
1942 This clearly needs more investigation. |
|
1943 |
|
1944 We have also not yet played with other binding modes. For example we can |
|
1945 imagine that the here is a mode \isacommand{bind\_\#list} with the associated |
|
1946 alpha-equivalence definition |
|
1947 % |
|
1948 \begin{center} |
|
1949 $\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l} |
|
1950 \multicolumn{2}{l}{@{term "alpha2 (as, x) R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm] |
|
1951 & @{term "fv(x) - (set as) = fv(y) - (set bs)"}\\ |
|
1952 \wedge & @{term "(fv(x) - set as) \<sharp>* p"}\\ |
|
1953 \wedge & @{text "(p \<bullet> x) R y"}\\ |
|
1954 \wedge & @{term "(p \<bullet> as) = bs"}\\ |
|
1955 \wedge & @{term "distinct as"} |
|
1956 \end{array}$ |
|
1957 \end{center} |
|
1958 |
|
1959 \noindent |
|
1960 In this definition we added the requirement that all bound variables |
|
1961 in a list are distinct. We can imagine applications for such a notion |
|
1962 of binding, but have not explored them yet. Our implementation can |
|
1963 easily extended to accommodate further binding modes. |
|
1964 |
|
1965 \medskip |
1913 \noindent |
1966 \noindent |
1914 {\bf Acknowledgements:} We are very grateful to Andrew Pitts for |
1967 {\bf Acknowledgements:} We are very grateful to Andrew Pitts for |
1915 many discussions about Nominal Isabelle. We thank Peter Sewell for |
1968 many discussions about Nominal Isabelle. We thank Peter Sewell for |
1916 making the informal notes \cite{SewellBestiary} available to us and |
1969 making the informal notes \cite{SewellBestiary} available to us and |
1917 also for patiently explaining some of the finer points about the abstract |
1970 also for patiently explaining some of the finer points about the abstract |
1918 definitions and about the implementation of the Ott-tool. We |
1971 definitions and about the implementation of the Ott-tool. We |
1919 also thank Stephanie Weirich for suggesting to separate the subgrammars |
1972 also thank Stephanie Weirich for suggesting to separate the subgrammars |
1920 of kinds and types in our Core-Haskell example. |
1973 of kinds and types in our Core-Haskell example. |
1921 *} |
1974 *} |
1922 |
1975 |
1923 text {* |
|
1924 %%% FIXME: The restricions should have already been described in previous sections? |
|
1925 Restrictions |
|
1926 |
|
1927 \begin{itemize} |
|
1928 \item non-emptiness |
|
1929 \item positive datatype definitions |
|
1930 \item finitely supported abstractions |
|
1931 \item respectfulness of the bn-functions\bigskip |
|
1932 \item binders can only have a ``single scope'' |
|
1933 \item in particular "bind a in b, bind b in c" is not allowed. |
|
1934 \item all bindings must have the same mode |
|
1935 \end{itemize} |
|
1936 *} |
|
1937 |
|
1938 (*<*) |
1976 (*<*) |
1939 end |
1977 end |
1940 (*>*) |
1978 (*>*) |