
diff -r f961a32eb0d9 -r ac064c47138b Slides/Slides2.thy
--- a/Slides/Slides2.thy	Sat Jul 10 15:50:33 2010 +0100
+++ b/Slides/Slides2.thy	Sat Jul 10 23:36:45 2010 +0100
@@ -18,12 +18,11 @@
   \frametitle{%
   \begin{tabular}{@ {\hspace{-3mm}}c@ {}}
   \\
-  \LARGE Proof Pearl:\\[-2mm]
+  \LARGE Proof Pearl:\\[-0mm]
   \LARGE A New Foundation for\\[-2mm] 
   \LARGE Nominal Isabelle\\[12mm]
   \end{tabular}}
   \begin{center}
-  \small
   Brian Huf\!fman and {\bf Christian Urban}\\[0mm] 
   \end{center}
   \end{frame}}
@@ -34,28 +33,43 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}<1-2>
-  \frametitle{\begin{tabular}{c}Nominal Isabelle\end{tabular}}
-  \mbox{}\\[-3mm]
+  \begin{frame}<1-2>[c]
+  \frametitle{Nominal Isabelle}
 
   \begin{itemize}
-  \item sorted atoms and sort-respecting permutations\medskip
+  \item \ldots is a definitional extension of Isabelle/HOL
+  (let-polymorphism and type classes)\medskip
+
+  \item \ldots provides a convenient reasoning infrastructure for
+  terms involving binders (e.g.~lambda calculus, variable convention)\medskip
+  
+  \item<2-> \ldots mainly used to find errors in my own 
+  (published) paper proofs and in that of others \alert{\bf ;o)}
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+ 
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-3>[c]
+  \frametitle{Nominal Theory}
+  
+  by Pitts; at its core are:\bigskip
+
+  \begin{itemize}
+  \item sorted atoms and 
+  \item sort-respecting permutations
+  \end{itemize}
 
   \onslide<2->{
-  \item[] in old Nominal: atoms have \underline{dif\!ferent} type\medskip
+  \begin{textblock}{8}(4,11)
+  \onslide<3->{$\text{inv\_of\_}\pi \,\act\, ($}\onslide<2->{$\pi \,\act\, x$}%
+  \onslide<3->{$) \,=\, x$}
+  \end{textblock}}
 
-  \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}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -64,29 +78,37 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}<1-2>
-  \frametitle{\begin{tabular}{c}Nominal Theory\end{tabular}}
-  \mbox{}\\[-3mm]
-
+  \begin{frame}<1-4>[t]
+  \frametitle{The ``Old Way''}
+  
   \begin{itemize}
-  \item sorted atoms and sort-respecting permutations\medskip
-
+  \item sorted atoms\\ \alert{$\quad\mapsto$ separate types}\; (``copies'' of nat)\bigskip 
+  \item sort-respecting permutations\\ \alert{$\quad\mapsto$ lists of pairs of atoms (list swappings)}
   \onslide<2->{
-  \item[] in old Nominal: atoms have \underline{dif\!ferent} type\medskip
-
-  \begin{center}
+  \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}
+  $\text{[]} \,\act\, c = c$ &
+  $\swap{a}{b}\!::\!\pi \,\act\, c =
+  \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}
 
+  \only<3>{
+  \begin{textblock}{14}(1,12.5)
+  \alert{The big benefit:} the type system takes care of the sort-respecting part.
+  \end{textblock}}
+  \only<4>{
+  \begin{textblock}{14}(1,12.5)
+  \alert{A small benefit:} permutation composition is \alert{list append} 
+  and permutation inversion is \alert{list reversal}.
+  \end{textblock}
+  }
+
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
@@ -94,9 +116,8 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}<1>
-  \frametitle{\begin{tabular}{c}Problems\end{tabular}}
-  \mbox{}\\[-3mm]
+  \begin{frame}<1-4>
+  \frametitle{Problems}
 
   \begin{itemize}
   \item @{text "_ \<bullet> _ :: \<alpha> perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}\bigskip
@@ -110,9 +131,29 @@
   
   \item $\forall \pi_{\alpha_1} \ldots \pi_{\alpha_n}\;.\; P$\bigskip
 
-  \item type-classes
+  \item type-classes 
+  \onslide<3>{\small\hspace{5mm}can only have \alert{\bf one} type parameter}
+  \begin{itemize}
+  \item<2-> $\text{[]}\,\act\, x = x$
+  \item<2-> $(\pi_1 @  \pi_2) \,\act \, x = \pi_1 \,\act\,(\pi_2 \,\act\, x)$
+  \item<2-> if $\pi_1 \sim \pi_2$ then $\pi_1 \,\act\, x = \pi_2 \,\act\, x$
+  \end{itemize}
   \end{itemize}
 
+  \only<4->{
+  \begin{textblock}{9}(3,7)\begin{tikzpicture}
+  \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
+  {\normalsize\color{darkgray}
+  \begin{quote}
+  \begin{itemize}
+  \item \alert{lots} of ML-code 
+  \item \alert{not} pretty 
+  \item \alert{not a proof pearl} :o( 
+  \end{itemize}
+  \end{quote}};
+  \end{tikzpicture}
+  \end{textblock}}
+
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
@@ -120,34 +161,39 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}<1-4>
-  \frametitle{\begin{tabular}{c}Our New Solution\end{tabular}}
-  \mbox{}\\[-3mm]
+  \begin{frame}<1-5>
+  \frametitle{A Better Way}
 *}
 datatype atom = Atom string nat
 
 text_raw {*
   \mbox{}\bigskip
   \begin{itemize}
-  \item<2-> permutations are (restricted) bijective functions from @{text "atom \<Rightarrow> atom"}
+  \item<3-> 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\}$)
+     \item sort-respecting \hspace{5mm}($\,\forall a.\;\text{sort}(\pi a) = \text{sort}(a)$)
+     \item finite domain \hspace{5mm}($\text{finite} \{a.\;\pi a \not= a\}$)
      \end{itemize}\medskip
-
-  \item<3-> swappings:
+     
+  \item<4-> \alert{What about 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}}
+        & \text{else}\;\only<4>{\raisebox{-5mm}{\textcolor{red}{\huge\bf $?$}}}
+          \only<5->{\text{\alert{\bf id}}}
      \end{array}
      \]
   \end{itemize}
 
+  \only<3>{
+  \begin{textblock}{7}(4,11)
+  @{text "\<pi> \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+  \end{textblock}}
+  
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
@@ -155,27 +201,28 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}<1-6>
-  \frametitle{\begin{tabular}{c}\LARGE{}A Smoother Nominal Theory\end{tabular}}
-  \mbox{}\\[-3mm]
+  \begin{frame}<1-7>
+  \frametitle{A Smoother Nominal Theory}
+  
+  From there it is essentially plain sailing:\bigskip
 
   \begin{itemize}
-  \item<1-> $(a\;b) = (b\;a) \onslide<3->{= (a\;c) + (b\;c) + (a\;c)}$\bigskip  
+  \item<2-> $(a\;b) = (b\;a) \onslide<4->{= (a\;c) + (b\;c) + (a\;c)}$\bigskip  
 
-  \item<2-> permutations are an instance of group\_add\\ $0$, $\pi_1 + \pi_2$, $- \pi$\bigskip
+  \item<3-> permutations are an instance of Isabelle's\\  
+  group\_add ($0$, $\pi_1 + \pi_2$, $- \pi$)\bigskip
 
-  \item<5-> $\_\;\act\;\_ :: \text{perm} \Rightarrow \alpha \Rightarrow \alpha$\medskip
+  \item<6-> $\_\;\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}
+   \end{itemize}\medskip
 
-   \small
-   \onslide<6->{$\text{finite}(\text{supp}\;x)$, $\forall \pi. P$}
+   \onslide<7->{\alert{$\;\mapsto\;$}only one type class, $\text{finite}(\text{supp}\;x)$, $\forall \pi. P$}
   \end{itemize}
 
-  \only<4>{
+  \only<5>{
   \begin{textblock}{6}(2.5,11)
   \begin{tikzpicture}
   \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
@@ -195,8 +242,8 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}<1-3>
-  \frametitle{\begin{tabular}{c}Very Few Snatches\end{tabular}}
-  \mbox{}\\[-3mm]
+  \frametitle{One Snatch}
+
 
   \begin{itemize}
   \item \underline{concrete} atoms:
@@ -212,7 +259,7 @@
 text_raw {*
   \mbox{}\bigskip\bigskip
   \begin{itemize}
-  \item<2-> there is an overloaded  function \underline{atom}, which injects concrete 
+  \item<2-> there is an overloaded  function \alert{\bf atom}, which injects concrete 
   atoms into generic ones\medskip 
   \begin{center}
   \begin{tabular}{l}
@@ -222,9 +269,46 @@
   \end{center}\bigskip\medskip
 
   \onslide<3->
-  {I would like to have $a \fresh x$, $(a\; b)$, \ldots}
+  {One would like to have $a \fresh x$, $(a\; b)$, \ldots}
+  \end{itemize}
+
+  \only<1>{
+  \begin{textblock}{11}(2.5,8.5)
+  You like to get the advantages of the old way back: you \alert{cannot mix} atoms
+  of dif$\!$ferent sort:\bigskip
+  
+  \small
+  e.g.~LF-objects:\\[-9mm]\mbox{} 
+  \begin{center}$\quad M ::= c \mid x \mid \lambda x\!:\!A. M \mid M_1\;M_2$
+  \end{center}
+  \end{textblock}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
 
-  \end{itemize}
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-4>
+  \frametitle{Sorts Reloaded}
+*}
+datatype atom\<iota> = Atom\<iota> string nat
+
+text_raw {*
+  \isanewline\isanewline
+  \pause
+  \alert{Problem}: HOL-binders or Church-style lambda-terms
+  \begin{center}
+  $\lambda x_\alpha.\, x_\alpha\;x_\beta$
+  \end{center}
+  \pause
+  \isanewline\isanewline
+
+\isacommand{datatype} ty = TVar string $\mid$ ty $\rightarrow$ ty\\
+\isacommand{datatype} var = Var name ty\\
+\pause
+$(x \leftrightarrow y) \,\act\, (x_\alpha, x_\beta) = (y_\alpha, y_\beta)$
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -233,8 +317,64 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
+  \begin{frame}<1-3>
+  \frametitle{Non-Working Solution}
+
+Instead of\isanewline\isanewline
+*}
+    datatype atom\<iota>\<iota> = Atom\<iota>\<iota> string nat
+
+text_raw {*
+\isanewline\isanewline
+have
+\isanewline\isanewline
+*}
+
+    datatype 'a atom\<iota>\<iota>\<iota> = Atom\<iota>\<iota> 'a nat
+text_raw {*
+  \pause
+  \isanewline\isanewline
+  But then
+  \begin{center}
+  @{text "_ \<bullet> _ :: \<alpha> perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+  \end{center}
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-3>
+  \frametitle{A Working Solution}
+
+*}
+    datatype sort = Sort string "sort list"
+    datatype atom\<iota>\<iota> = Atom\<iota>\<iota> string nat
+
+text_raw {*
+\isanewline\isanewline
+have
+\isanewline\isanewline
+*}
+
+    datatype 'a atom\<iota>\<iota>\<iota> = Atom\<iota>\<iota> 'a nat
+text_raw {*
+  \pause
+  \isanewline\isanewline
+  But then
+  \begin{center}
+  @{text "_ \<bullet> _ :: \<alpha> perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+  \end{center}
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
   \begin{frame}<1-2>[c]
-  \frametitle{\begin{tabular}{c}\LARGE{}End of Part I\end{tabular}}
+  \frametitle{Conclusion}
   \mbox{}\\[-3mm]
 
   \begin{itemize}




