44   \item[] in old Nominal: atoms have dif\!ferent type

    44   \item[] in old Nominal: atoms have \underline{dif\!ferent} type\medskip

    48   $[] \act c \dn c$ &

    48   $[]\;\act\;c \dn c$ &

    49   @{text "(a b)::\<pi> \<bullet> c \<equiv>"} 

    49   $(a\;b)\!::\!\pi\;\act\;c \dn$ 

    51   \mbox{@{text "b"}} & \text{if} \mbox{@{text "\<pi> \<bullet> c = a"}}\\

    51   b & \text{if}\; \pi \act c = a\\

    52   \mbox{@{text "a"}} & \text{if} \mbox{@{text "\<pi> \<bullet> c = b"}}\\

    52   a & \text{if}\; \pi \act c = b\\

    53   \mbox{@{text "\<pi> \<bullet> c"}} & \text{otherwise}

    53   \pi \act c & \text{otherwise}

    71   \item $\_ \act \_ :: \alpha perm \Rightarrow \beta \Rightarrow \beta$

    71   \item @{text "_ \<bullet> _ :: \<alpha> perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}\bigskip

    72 

    72 

    73   \item $supp \_ :: \beta \Rightarrow \alpha set$

    73   \item @{text "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}

    74 

    74 

    75   \begin{center}

    75   \begin{center}

    76   $finite (supp x)_{\alpha_1} \ldots finite (supp x)_{\alpha_n}$

    76   $\text{finite} (\text{supp}\;x)_{\,\alpha_1\,\text{set}}$ \ldots 

    77   $\text{finite} (\text{supp}\;x)_{\,\alpha_n\,\text{set}}$

    78   \end{center}\bigskip

    79   

    80   \item $\forall \pi_{\alpha_1} \ldots \pi_{\alpha_n}\;.\; P$\bigskip

    81 

    82   \item type-classes

    83   \end{itemize}

    84 

    85   \end{frame}}

    86   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    87 *}

    88 

    89 text_raw {*

    90   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    91   \mode<presentation>{

    92   \begin{frame}<1-4>

    93   \frametitle{\begin{tabular}{c}Our New Solution\end{tabular}}

    94   \mbox{}\\[-3mm]

    95 *}

    96 datatype atom = Atom string nat

    97 

    98 text_raw {*

    99   \mbox{}\bigskip

   100   \begin{itemize}

   101   \item<2-> permutations are (restricted) bijective functions from @{text "atom \<Rightarrow> atom"}

   102 

   103      \begin{itemize}

   104      \item sort-respecting \hspace{5mm}($\forall a.\;\text{sort}(f a) = \text{sort}(a)$)

   105      \item finite domain \hspace{5mm}($\text{finite} \{a.\;f a \not= a\}$)

   106      \end{itemize}\medskip

   107 

   108   \item<3-> swappings:

   109      \small

   110      \[

   111      \begin{array}{l@ {\hspace{1mm}}l}

   112      (a\;b) \dn & \text{if}\;\text{sort}(a) = \text{sort}(b)\\

   113         & \text{then}\;\lambda  c. \text{if}\;a = c\;\text{then}\;b\;\text{else}\;

   114           \text{if}\;b = c\;\text{then}\;a\;\text{else}\;c\\

   115         & \text{else}\;\only<3>{\mbox{\textcolor{red}{\bf ?}}}\only<4->{\text{id}}

   116      \end{array}

   117      \]

   118   \end{itemize}

   119 

   120   \end{frame}}

   121   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   122 *}

   123 

   124 text_raw {*

   125   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   126   \mode<presentation>{

   127   \begin{frame}<1-4>

   128   \frametitle{\begin{tabular}{c}\LARGE{}A Smoother Nominal Theory\end{tabular}}

   129   \mbox{}\\[-3mm]

   130 

   131   \begin{itemize}

   132   \item<1-> $(a\;b) = (b\;a)$\bigskip  

   133 

   134   \item<2-> permutations are an instance of group\_add\\ $0$, $\pi_1 + \pi_2$, $- \pi$\bigskip

   135 

   136   \item<3-> $\_\;\act\;\_ :: \text{perm} \Rightarrow \alpha \Rightarrow \alpha$\medskip

   137   

   138    \begin{itemize}

   139    \item $0\;\act\;x = x$\\

   140    \item $(\pi_1 + \pi_2)\;\act\;x = \pi_1\;\act\;(\pi_2\;\act\;x)$

   141    \end{itemize}

   142 

   143    \small

   144    \onslide<4->{$\text{finite}(\text{supp}\;x)$, $\forall \pi. P$}

   145   \end{itemize}

   146 

   147   \end{frame}}

   148   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   149 *}

   150 

   151 text_raw {*

   152   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   153   \mode<presentation>{

   154   \begin{frame}<1-3>

   155   \frametitle{\begin{tabular}{c}Very Few Snatches\end{tabular}}

   156   \mbox{}\\[-3mm]

   157 

   158   \begin{itemize}

   159   \item \underline{concrete} atoms:

   160   \end{itemize}

   161 *}

   162 (*<*)

   163 consts sort :: "atom \<Rightarrow> string"

   164 (*>*)

   165 

   166 typedef name = "{a :: atom. sort a = ''name''}"

   167 (*<*)sorry(*>*)

   168 

   169 text_raw {*

   170   \mbox{}\bigskip\bigskip

   171   \begin{itemize}

   172   \item<2-> there is a function \underline{atom}, which injects concrete atoms into generic atoms\medskip 

   173   \begin{center}

   174   \begin{tabular}{l}

   175   $\text{atom}(a) \fresh x$\\

   176   $(a \leftrightarrow b) \dn (\text{atom}(a)\;\;\text{atom}(b))$

   177   \end{tabular}

   178   \end{center}\bigskip\medskip

   179 

   180   \onslide<3->

   181   {I would like to have $a \fresh x$, $(a\; b)$, \ldots}

   182 

   183   \end{itemize}

   184 

   185   \end{frame}}

   186   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   187 *}

   188 

   189 text_raw {*

   190   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   191   \mode<presentation>{

   192   \begin{frame}<1-2>[c]

   193   \frametitle{\begin{tabular}{c}\LARGE{}End of Part I\end{tabular}}

   194   \mbox{}\\[-3mm]

   195 

   196   \begin{itemize}

   197   \item the formalised version of the nominal theory is much nicer to 

   198   work with (no assumptions, just two type classes; sorts are occasionally 

   199   explicit)\bigskip

   200 

   201   \item permutations: ``be as abstract as you can'' (group\_add is a slight oddity)\bigskip

   202 

   203   \item allow sort-disrespecting swappings\onslide<2->{: just define them as the identity}

   204   \end{itemize}

   205 

   206   

   207   \end{frame}}

   208   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   209 *}

   210 

   211 text_raw {*

   212   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   213   \mode<presentation>{

   214   \begin{frame}<1-2>

   215   \frametitle{\begin{tabular}{c}\LARGE{}Part II: General Bindings\end{tabular}}

   216   \mbox{}\\[-3mm]

   217 

   218   \begin{itemize}

   219   \item old Nominal provided single binders

   220   \begin{center}

   221   Lam [a].(Var a)

   222   \end{center}\bigskip

   223 

   224   \item<2-> representing 

   225   \begin{center}

   226   $\forall\{a_1,\ldots,a_n\}.\; T$ 

    78   

   228   is a major pain, take my word for it

    79   \item $\forall \pi_{\alpha_1} \ldots \pi_{\alpha_n}\;.\; P$

   229   \end{itemize}

    80   \end{itemize}

    81 

    82   \end{frame}}

    83   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    84 *}

    85 

    86 

    87 text_raw {*

    88   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    89   \mode<presentation>{

    90   \begin{frame}<1>[c]

    91   \frametitle{\begin{tabular}{c}Part II: General Bindings\end{tabular}}

    92   \mbox{}\\[-3mm]

    93