(*<*)
theory Slides1
imports "LaTeXsugar" "Nominal"
begin

notation (latex output)
  set ("_") and
  Cons  ("_::/_" [66,65] 65) 

(*>*)


text_raw {*
  \renewcommand{\slidecaption}{TU Munich, 28.~May 2010}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1>[t]
  \frametitle{%
  \begin{tabular}{@ {\hspace{-3mm}}c@ {}}
  \\
  \huge Nominal 2\\[-2mm] 
  \large Or, How to Reason Conveniently with\\[-5mm]
  \large General Bindings\\[15mm]
  \end{tabular}}
  \begin{center}
  joint work with {\bf Cezary} and Brian Huf\!fman\\[0mm] 
  \end{center}
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1-2>
  \frametitle{\begin{tabular}{c}Part I: Nominal Theory\end{tabular}}
  \mbox{}\\[-3mm]

  \begin{itemize}
  \item sorted atoms and sort-respecting permutations\medskip

  \onslide<2->{
  \item[] in old Nominal: atoms have \underline{dif\!ferent} type\medskip

  \begin{center}
  \begin{tabular}{c@ {\hspace{7mm}}c}
  $[]\;\act\;c \dn c$ &
  $(a\;b)\!::\!\pi\;\act\;c \dn$ 
  $\begin{cases}
  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}}
  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1>
  \frametitle{\begin{tabular}{c}Problems\end{tabular}}
  \mbox{}\\[-3mm]

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

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

  \begin{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$\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-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}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}



(*<*)
end
(*>*)