--- a/Slides/Slides1.thy	Wed May 26 15:37:56 2010 +0200
+++ b/Slides/Slides1.thy	Thu May 27 18:37:52 2010 +0200
@@ -41,16 +41,16 @@
   \item sorted atoms and sort-respecting permutations\medskip
 
   \onslide<2->{
-  \item[] in old Nominal: atoms have dif\!ferent type
+  \item[] in old Nominal: atoms have \underline{dif\!ferent} type\medskip
 
   \begin{center}
   \begin{tabular}{c@ {\hspace{7mm}}c}
-  $[] \act c \dn c$ &
-  @{text "(a b)::\<pi> \<bullet> c \<equiv>"} 
+  $[]\;\act\;c \dn c$ &
+  $(a\;b)\!::\!\pi\;\act\;c \dn$ 
   $\begin{cases}
-  \mbox{@{text "b"}} & \text{if} \mbox{@{text "\<pi> \<bullet> c = a"}}\\
-  \mbox{@{text "a"}} & \text{if} \mbox{@{text "\<pi> \<bullet> c = b"}}\\
-  \mbox{@{text "\<pi> \<bullet> c"}} & \text{otherwise}
+  b & \text{if}\; \pi \act c = a\\
+  a & \text{if}\; \pi \act c = b\\
+  \pi \act c & \text{otherwise}
   \end{cases}$
   \end{tabular}
   \end{center}}
@@ -68,29 +68,165 @@
   \mbox{}\\[-3mm]
 
   \begin{itemize}
-  \item $\_ \act \_ :: \alpha perm \Rightarrow \beta \Rightarrow \beta$
+  \item @{text "_ \<bullet> _ :: \<alpha> perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}\bigskip
 
-  \item $supp \_ :: \beta \Rightarrow \alpha set$
+  \item @{text "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}
 
   \begin{center}
-  $finite (supp x)_{\alpha_1} \ldots finite (supp x)_{\alpha_n}$
-  \end{center}
+  $\text{finite} (\text{supp}\;x)_{\,\alpha_1\,\text{set}}$ \ldots 
+  $\text{finite} (\text{supp}\;x)_{\,\alpha_n\,\text{set}}$
+  \end{center}\bigskip
   
-  \item $\forall \pi_{\alpha_1} \ldots \pi_{\alpha_n}\;.\; P$
+  \item $\forall \pi_{\alpha_1} \ldots \pi_{\alpha_n}\;.\; P$\bigskip
+
+  \item type-classes
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-4>
+  \frametitle{\begin{tabular}{c}Our New Solution\end{tabular}}
+  \mbox{}\\[-3mm]
+*}
+datatype atom = Atom string nat
+
+text_raw {*
+  \mbox{}\bigskip
+  \begin{itemize}
+  \item<2-> permutations are (restricted) bijective functions from @{text "atom \<Rightarrow> atom"}
+
+     \begin{itemize}
+     \item sort-respecting \hspace{5mm}($\forall a.\;\text{sort}(f a) = \text{sort}(a)$)
+     \item finite domain \hspace{5mm}($\text{finite} \{a.\;f a \not= a\}$)
+     \end{itemize}\medskip
+
+  \item<3-> swappings:
+     \small
+     \[
+     \begin{array}{l@ {\hspace{1mm}}l}
+     (a\;b) \dn & \text{if}\;\text{sort}(a) = \text{sort}(b)\\
+        & \text{then}\;\lambda  c. \text{if}\;a = c\;\text{then}\;b\;\text{else}\;
+          \text{if}\;b = c\;\text{then}\;a\;\text{else}\;c\\
+        & \text{else}\;\only<3>{\mbox{\textcolor{red}{\bf ?}}}\only<4->{\text{id}}
+     \end{array}
+     \]
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-4>
+  \frametitle{\begin{tabular}{c}\LARGE{}A Smoother Nominal Theory\end{tabular}}
+  \mbox{}\\[-3mm]
+
+  \begin{itemize}
+  \item<1-> $(a\;b) = (b\;a)$\bigskip  
+
+  \item<2-> permutations are an instance of group\_add\\ $0$, $\pi_1 + \pi_2$, $- \pi$\bigskip
+
+  \item<3-> $\_\;\act\;\_ :: \text{perm} \Rightarrow \alpha \Rightarrow \alpha$\medskip
+  
+   \begin{itemize}
+   \item $0\;\act\;x = x$\\
+   \item $(\pi_1 + \pi_2)\;\act\;x = \pi_1\;\act\;(\pi_2\;\act\;x)$
+   \end{itemize}
+
+   \small
+   \onslide<4->{$\text{finite}(\text{supp}\;x)$, $\forall \pi. P$}
   \end{itemize}
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
 
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-3>
+  \frametitle{\begin{tabular}{c}Very Few Snatches\end{tabular}}
+  \mbox{}\\[-3mm]
+
+  \begin{itemize}
+  \item \underline{concrete} atoms:
+  \end{itemize}
+*}
+(*<*)
+consts sort :: "atom \<Rightarrow> string"
+(*>*)
+
+typedef name = "{a :: atom. sort a = ''name''}"
+(*<*)sorry(*>*)
+
+text_raw {*
+  \mbox{}\bigskip\bigskip
+  \begin{itemize}
+  \item<2-> there is a function \underline{atom}, which injects concrete atoms into generic atoms\medskip 
+  \begin{center}
+  \begin{tabular}{l}
+  $\text{atom}(a) \fresh x$\\
+  $(a \leftrightarrow b) \dn (\text{atom}(a)\;\;\text{atom}(b))$
+  \end{tabular}
+  \end{center}\bigskip\medskip
+
+  \onslide<3->
+  {I would like to have $a \fresh x$, $(a\; b)$, \ldots}
+
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
 
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}<1>[c]
-  \frametitle{\begin{tabular}{c}Part II: General Bindings\end{tabular}}
+  \begin{frame}<1-2>[c]
+  \frametitle{\begin{tabular}{c}\LARGE{}End of Part I\end{tabular}}
   \mbox{}\\[-3mm]
 
+  \begin{itemize}
+  \item the formalised version of the nominal theory is much nicer to 
+  work with (no assumptions, just two type classes; sorts are occasionally 
+  explicit)\bigskip
+
+  \item permutations: ``be as abstract as you can'' (group\_add is a slight oddity)\bigskip
+
+  \item allow sort-disrespecting swappings\onslide<2->{: just define them as the identity}
+  \end{itemize}
+
+  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-2>
+  \frametitle{\begin{tabular}{c}\LARGE{}Part II: General Bindings\end{tabular}}
+  \mbox{}\\[-3mm]
+
+  \begin{itemize}
+  \item old Nominal provided single binders
+  \begin{center}
+  Lam [a].(Var a)
+  \end{center}\bigskip
+
+  \item<2-> representing 
+  \begin{center}
+  $\forall\{a_1,\ldots,a_n\}.\; T$ 
+  \end{center}
+  is a major pain, take my word for it
+  \end{itemize}
   
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%