(*<*)

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 dif\!ferent type

  \begin{center}

  \begin{tabular}{c@ {\hspace{7mm}}c}

  $[] \act c \dn c$ &

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

  $\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}

  \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 $\_ \act \_ :: \alpha perm \Rightarrow \beta \Rightarrow \beta$

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

  \begin{center}

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

  \end{center}

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

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}<1>[c]

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

  \mbox{}\\[-3mm]

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

(*<*)

end

(*>*)