21   \LARGE Proof Pearl:\\[-2mm]

    21   \LARGE Proof Pearl:\\[-0mm]

    37   \begin{frame}<1-2>

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

    38   \frametitle{\begin{tabular}{c}Nominal Isabelle\end{tabular}}

    37   \frametitle{Nominal Isabelle}

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

    38 

    40 

    39   \begin{itemize}

    41   \begin{itemize}

    40   \item \ldots is a definitional extension of Isabelle/HOL

    42   \item sorted atoms and sort-respecting permutations\medskip

    41   (let-polymorphism and type classes)\medskip

    42 

    43   \item \ldots provides a convenient reasoning infrastructure for

    44   terms involving binders (e.g.~lambda calculus, variable convention)\medskip

    45   

    46   \item<2-> \ldots mainly used to find errors in my own 

    47   (published) paper proofs and in that of others \alert{\bf ;o)}

    48   \end{itemize}

    49 

    50   \end{frame}}

    51   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    52 *}

    53  

    54 text_raw {*

    55   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    56   \mode<presentation>{

    57   \begin{frame}<1-3>[c]

    58   \frametitle{Nominal Theory}

    59   

    60   by Pitts; at its core are:\bigskip

    61 

    62   \begin{itemize}

    63   \item sorted atoms and 

    64   \item sort-respecting permutations

    65   \end{itemize}

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

    68   \begin{textblock}{8}(4,11)

    46 

    69   \onslide<3->{$\text{inv\_of\_}\pi \,\act\, ($}\onslide<2->{$\pi \,\act\, x$}%

    47   \begin{center}

    70   \onslide<3->{$) \,=\, x$}

    71   \end{textblock}}

    72 

    73 

    74   \end{frame}}

    75   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    76 *}

    77 

    78 text_raw {*

    79   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    80   \mode<presentation>{

    81   \begin{frame}<1-4>[t]

    82   \frametitle{The ``Old Way''}

    83   

    84   \begin{itemize}

    85   \item sorted atoms\\ \alert{$\quad\mapsto$ separate types}\; (``copies'' of nat)\bigskip 

    86   \item sort-respecting permutations\\ \alert{$\quad\mapsto$ lists of pairs of atoms (list swappings)}

    87   \onslide<2->{

    88   \begin{center} 

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

    90   $\text{[]} \,\act\, c = c$ &

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

    91   $\swap{a}{b}\!::\!\pi \,\act\, c =

    51   $\begin{cases}

    92   \begin{cases}

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

    93   b & \text{if}\, \pi\act c = a\\

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

    94   a & \text{if}\, \pi\act c = b\\

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

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

    60   \end{frame}}

   101   \only<3>{

    61   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   102   \begin{textblock}{14}(1,12.5)

    62 *}

   103   \alert{The big benefit:} the type system takes care of the sort-respecting part.

    63 

   104   \end{textblock}}

    64 text_raw {*

   105   \only<4>{

    65   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   106   \begin{textblock}{14}(1,12.5)

    66   \mode<presentation>{

   107   \alert{A small benefit:} permutation composition is \alert{list append} 

    67   \begin{frame}<1-2>

   108   and permutation inversion is \alert{list reversal}.

    68   \frametitle{\begin{tabular}{c}Nominal Theory\end{tabular}}

   109   \end{textblock}

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

   110   }

    70 

   111 

    71   \begin{itemize}

   112   \end{frame}}

    72   \item sorted atoms and sort-respecting permutations\medskip

   113   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    73 

   114 *}

    74   \onslide<2->{

   115 

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

   116 text_raw {*

    76 

   117   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    77   \begin{center}

   118   \mode<presentation>{

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

   119   \begin{frame}<1-4>

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

   120   \frametitle{Problems}

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

    81   $\begin{cases}

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

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

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

    85   \end{cases}$

    86   \end{tabular}

    87   \end{center}}

    88   \end{itemize}

    89 

    90   \end{frame}}

    91   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    92 *}

    93 

    94 text_raw {*

    95   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    96   \mode<presentation>{

    97   \begin{frame}<1>

    98   \frametitle{\begin{tabular}{c}Problems\end{tabular}}

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

   113   \item type-classes

   134   \item type-classes 

   114   \end{itemize}

   135   \onslide<3>{\small\hspace{5mm}can only have \alert{\bf one} type parameter}

   115 

   136   \begin{itemize}

   116   \end{frame}}

   137   \item<2-> $\text{[]}\,\act\, x = x$

   117   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   138   \item<2-> $(\pi_1 @  \pi_2) \,\act \, x = \pi_1 \,\act\,(\pi_2 \,\act\, x)$

   118 *}

   139   \item<2-> if $\pi_1 \sim \pi_2$ then $\pi_1 \,\act\, x = \pi_2 \,\act\, x$

   119 

   140   \end{itemize}

   120 text_raw {*

   141   \end{itemize}

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

   142 

   122   \mode<presentation>{

   143   \only<4->{

   123   \begin{frame}<1-4>

   144   \begin{textblock}{9}(3,7)\begin{tikzpicture}

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

   145   \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

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

   146   {\normalsize\color{darkgray}

   147   \begin{quote}

   148   \begin{itemize}

   149   \item \alert{lots} of ML-code 

   150   \item \alert{not} pretty 

   151   \item \alert{not a proof pearl} :o( 

   152   \end{itemize}

   153   \end{quote}};

   154   \end{tikzpicture}

   155   \end{textblock}}

   156 

   157   \end{frame}}

   158   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   159 *}

   160 

   161 text_raw {*

   162   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   163   \mode<presentation>{

   164   \begin{frame}<1-5>

   165   \frametitle{A Better Way}

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

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

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

   175      \item sort-respecting \hspace{5mm}($\,\forall a.\;\text{sort}(\pi a) = \text{sort}(a)$)

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

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

   138 

   178      

   139   \item<3-> swappings:

   179   \item<4-> \alert{What about swappings?}

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

   186         & \text{else}\;\only<4>{\raisebox{-5mm}{\textcolor{red}{\huge\bf $?$}}}

   187           \only<5->{\text{\alert{\bf id}}}

   151   \end{frame}}

   192   \only<3>{

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

   193   \begin{textblock}{7}(4,11)

   153 *}

   194   @{text "\<pi> \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}

   154 

   195   \end{textblock}}

   155 text_raw {*

   196   

   156   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   197   \end{frame}}

   157   \mode<presentation>{

   198   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   158   \begin{frame}<1-6>

   199 *}

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

   200 

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

   201 text_raw {*

   161 

   202   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   162   \begin{itemize}

   203   \mode<presentation>{

   163   \item<1-> $(a\;b) = (b\;a) \onslide<3->{= (a\;c) + (b\;c) + (a\;c)}$\bigskip  

   204   \begin{frame}<1-7>

   164 

   205   \frametitle{A Smoother Nominal Theory}

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

   206   

   166 

   207   From there it is essentially plain sailing:\bigskip

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

   208 

   209   \begin{itemize}

   210   \item<2-> $(a\;b) = (b\;a) \onslide<4->{= (a\;c) + (b\;c) + (a\;c)}$\bigskip  

   211 

   212   \item<3-> permutations are an instance of Isabelle's\\  

   213   group\_add ($0$, $\pi_1 + \pi_2$, $- \pi$)\bigskip

   214 

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

   172    \end{itemize}

   220    \end{itemize}\medskip

   173 

   221 

   174    \small

   222    \onslide<7->{\alert{$\;\mapsto\;$}only one type class, $\text{finite}(\text{supp}\;x)$, $\forall \pi. P$}

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

   223   \end{itemize}

   176   \end{itemize}

   224 

   177 

   225   \only<5>{

   178   \only<4>{

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

   245   \frametitle{One Snatch}

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

   246 

   215   \item<2-> there is an overloaded  function \underline{atom}, which injects concrete 

   262   \item<2-> there is an overloaded  function \alert{\bf atom}, which injects concrete 

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

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

   226 

   273   \end{itemize}

   227   \end{itemize}

   274 

   228 

   275   \only<1>{

   276   \begin{textblock}{11}(2.5,8.5)

   277   You like to get the advantages of the old way back: you \alert{cannot mix} atoms

   278   of dif$\!$ferent sort:\bigskip

   279   

   280   \small

   281   e.g.~LF-objects:\\[-9mm]\mbox{} 

   282   \begin{center}$\quad M ::= c \mid x \mid \lambda x\!:\!A. M \mid M_1\;M_2$

   283   \end{center}

   284   \end{textblock}}

   285 

   286   \end{frame}}

   287   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   288 *}

   289 

   290 text_raw {*

   291   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   292   \mode<presentation>{

   293   \begin{frame}<1-4>

   294   \frametitle{Sorts Reloaded}

   295 *}

   296 datatype atom\<iota> = Atom\<iota> string nat

   297 

   298 text_raw {*

   299   \isanewline\isanewline

   300   \pause

   301   \alert{Problem}: HOL-binders or Church-style lambda-terms

   302   \begin{center}

   303   $\lambda x_\alpha.\, x_\alpha\;x_\beta$

   304   \end{center}

   305   \pause

   306   \isanewline\isanewline

   307 

   308 \isacommand{datatype} ty = TVar string $\mid$ ty $\rightarrow$ ty\\

   309 \isacommand{datatype} var = Var name ty\\

   310 \pause

   311 $(x \leftrightarrow y) \,\act\, (x_\alpha, x_\beta) = (y_\alpha, y_\beta)$

   312 

   313   \end{frame}}

   314   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   315 *}

   316 

   317 text_raw {*

   318   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   319   \mode<presentation>{

   320   \begin{frame}<1-3>

   321   \frametitle{Non-Working Solution}

   322 

   323 Instead of\isanewline\isanewline

   324 *}

   325     datatype atom\<iota>\<iota> = Atom\<iota>\<iota> string nat

   326 

   327 text_raw {*

   328 \isanewline\isanewline

   329 have

   330 \isanewline\isanewline

   331 *}

   332 

   333     datatype 'a atom\<iota>\<iota>\<iota> = Atom\<iota>\<iota> 'a nat

   334 text_raw {*

   335   \pause

   336   \isanewline\isanewline

   337   But then

   338   \begin{center}

   339   @{text "_ \<bullet> _ :: \<alpha> perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}

   340   \end{center}

   341   \end{frame}}

   342   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   343 *}

   344 

   345 text_raw {*

   346   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   347   \mode<presentation>{

   348   \begin{frame}<1-3>

   349   \frametitle{A Working Solution}

   350 

   351 *}

   352     datatype sort = Sort string "sort list"

   353     datatype atom\<iota>\<iota> = Atom\<iota>\<iota> string nat

   354 

   355 text_raw {*

   356 \isanewline\isanewline

   357 have

   358 \isanewline\isanewline

   359 *}

   360 

   361     datatype 'a atom\<iota>\<iota>\<iota> = Atom\<iota>\<iota> 'a nat

   362 text_raw {*

   363   \pause

   364   \isanewline\isanewline

   365   But then

   366   \begin{center}

   367   @{text "_ \<bullet> _ :: \<alpha> perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}

   368   \end{center}

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

   377   \frametitle{Conclusion}