
diff -r 387fcbd33820 -r 13f20fe02ff3 Slides/Slides1.thy
--- a/Slides/Slides1.thy	Wed Jun 02 11:37:51 2010 +0200
+++ b/Slides/Slides1.thy	Thu Jun 03 11:48:44 2010 +0200
@@ -11,7 +11,7 @@
 
 
 text_raw {*
-  \renewcommand{\slidecaption}{TU Munich, 28.~May 2010}
+  \renewcommand{\slidecaption}{Cambridge, 8.~June 2010}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}<1>[t]
@@ -20,10 +20,13 @@
   \\
   \huge Nominal 2\\[-2mm] 
   \large Or, How to Reason Conveniently with\\[-5mm]
-  \large General Bindings in Isabelle\\[15mm]
+  \large General Bindings in Isabelle/HOL\\[5mm]
   \end{tabular}}
   \begin{center}
-  joint work with {\bf Cezary} and Brian Huf\!fman\\[0mm] 
+  Christian Urban
+  \end{center}
+  \begin{center}
+  joint work with {\bf Cezary Kaliszyk}\\[0mm] 
   \end{center}
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -34,197 +37,7 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \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-6>
-  \frametitle{\begin{tabular}{c}\LARGE{}A Smoother Nominal Theory\end{tabular}}
-  \mbox{}\\[-3mm]
-
-  \begin{itemize}
-  \item<1-> $(a\;b) = (b\;a) \onslide<3->{= (a\;c) + (b\;c) + (a\;c)}$\bigskip  
-
-  \item<2-> permutations are an instance of group\_add\\ $0$, $\pi_1 + \pi_2$, $- \pi$\bigskip
-
-  \item<5-> $\_\;\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<6->{$\text{finite}(\text{supp}\;x)$, $\forall \pi. P$}
-  \end{itemize}
-
-  \only<4>{
-  \begin{textblock}{6}(2.5,11)
-  \begin{tikzpicture}
-  \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
-  {\normalsize\color{darkgray}
-  \begin{minipage}{8cm}\raggedright
-  This is slightly odd, since in general: 
-  \begin{center}$\pi_1 + \pi_2 \alert{\not=} \pi_2 + \pi_1$\end{center}
-  \end{minipage}};
-  \end{tikzpicture}
-  \end{textblock}}
-
-  \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(*>*)
-typedef ident = "{a :: atom. sort a = ''ident''}" (*<*)sorry(*>*)
-
-text_raw {*
-  \mbox{}\bigskip\bigskip
-  \begin{itemize}
-  \item<2-> there is an overloaded  function \underline{atom}, which injects concrete 
-  atoms into generic ones\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 now much nicer to 
-  work with (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}}
+  \frametitle{\begin{tabular}{c}Binding in Old Nominal\end{tabular}}
   \mbox{}\\[-6mm]
 
   \begin{itemize}
@@ -240,7 +53,8 @@
   $\forall\{a_1,\ldots,a_n\}.\; T$ 
   \end{center}\medskip
 
-  with single binders is a \alert{major} pain; take my word for it!
+  with single binders and reasoning about it is a \alert{\bf major} pain; 
+  take my word for it!
   \end{itemize}
 
   \only<1>{
@@ -250,6 +64,7 @@
   \begin{tabular}{l@ {\hspace{2mm}}l}
   \pgfuseshading{smallspherered} & a $\fresh$ Lam [a]. t\\
   \pgfuseshading{smallspherered} & Lam [a]. (Var a) \alert{$=$} Lam [b]. (Var b)\\
+  \pgfuseshading{smallspherered} & Barendregt style reasoning about bound variables\\
   \end{tabular}
   \end{textblock}}
   
@@ -362,10 +177,10 @@
 
   \begin{itemize}
   \item the order does not matter and alpha-equivelence is preserved under
-  vacuous binders (restriction)\medskip
+  vacuous binders \textcolor{gray}{(restriction)}\medskip
   
   \item the order does not matter, but the cardinality of the binders 
-  must be the same (abstraction)\medskip
+  must be the same \textcolor{gray}{(abstraction)}\medskip
 
   \item the order does matter
   \end{itemize}
@@ -401,8 +216,8 @@
   \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\
   \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\
   \multicolumn{2}{l}{\onslide<3->{\isacommand{binder} bn \isacommand{where}}}\\
-  \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $\varnothing$}}\\
-  \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}$|$ bn(ACons a t as) $=$ $\{$a$\}$ $\cup$ bn(as)}}\\
+  \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ []}}\\
+  \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}$|$ bn(ACons a t as) $=$ [a] @ bn(as)}}\\
   \end{tabular}
 
 
@@ -414,33 +229,65 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}<1-4>
-  \frametitle{\begin{tabular}{c}Ott\end{tabular}}
+  \begin{frame}<1-5>
+  \frametitle{\begin{tabular}{c}Inspiration from Ott\end{tabular}}
   \mbox{}\\[-3mm]
 
   \begin{itemize}
-  \item this way of specifying binding is pretty much stolen from 
-  Ott\onslide<2->{, \alert{\bf but} with adjustments:}\medskip
+  \item this way of specifying binding is inspired by 
+  Ott\onslide<2->{, \alert{\bf but} we made adjustments:}\medskip
+  
 
+  \only<2>{
   \begin{itemize}
-  \item<2-> Ott allows specifications like\smallskip
+  \item Ott allows specifications like\smallskip
   \begin{center}
   $t ::= t\;t\; |\;\lambda x.t$
-  \end{center}\medskip
+  \end{center}
+  \end{itemize}}
 
-  \item<3-> whether something is bound can depend on other bound things\smallskip
+  \only<3-4>{
+  \begin{itemize}
+  \item whether something is bound can depend in Ott on other bound things\smallskip
   \begin{center}
-  Foo $(\lambda x. t)\; s$ 
-  \end{center}\medskip
-  \onslide<4->{this might make sense for ``raw'' terms, but not at all 
+  \begin{tikzpicture}
+  \node (A) at (-0.5,1) {Foo $(\lambda y. \lambda x. t)$};
+  \node (B) at ( 1.1,1) {$s$};
+  \onslide<4>{\node (C) at (0.5,0) {$\{y, x\}$};}
+  \onslide<4>{\draw[->,red,line width=1mm] (A) -- (C);}
+  \onslide<4>{\draw[->,red,line width=1mm] (C) -- (B);}
+  \end{tikzpicture}
+  \end{center}
+  \onslide<4>{this might make sense for ``raw'' terms, but not at all 
   for $\alpha$-equated terms}
-  \end{itemize}
+  \end{itemize}}
+
+  \only<5>{
+  \begin{itemize}
+  \item we allow multiple binders and bodies\smallskip
+  \begin{center}
+  \isacommand{bind} a b c \isacommand{in} x y z
+  \end{center}\bigskip\medskip
+  the reason is that in general
+  \begin{center}
+  \begin{tabular}{rcl}
+  \isacommand{bind\_res} as \isacommand{in} x y & $\not\Leftrightarrow$ &
+  \begin{tabular}{@ {}l}
+  \isacommand{bind\_res} as \isacommand{in} x,\\
+  \isacommand{bind\_res} as \isacommand{in} y
+  \end{tabular}
+  \end{tabular}
+  \end{center}\smallskip
+
+  same with \isacommand{bind\_set}
+  \end{itemize}}
   \end{itemize}
 
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
+
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
@@ -449,13 +296,13 @@
   \mbox{}\\[-3mm]
 
   \begin{itemize}
-  \item in old Nominal we represented single binders as partial functions:\bigskip
+  \item in old Nominal, we represented single binders as partial functions:\bigskip
   
   \begin{center}
   \begin{tabular}{l}
-  Lam [$a$].$t$ $\;\dn$\\[2mm]
+  Lam [$a$].\,$t$ $\;{^\text{``}}\!\dn{}\!^{\text{''}}$\\[2mm]
   \;\;\;\;$\lambda b.$\;$\text{if}\;a = b\;\text{then}\;t\;\text{else}$\\
-  \phantom{\;\;\;\;$\lambda b.$\;\;\;}$\text{if}\;b \fresh t\;
+  \phantom{\;\;\;\;$\lambda b.$\;\;\;\;\;\;}$\text{if}\;b \fresh t\;
   \text{then}\;(a\;b)\act t\;\text{else}\;\text{error}$ 
   \end{tabular}
   \end{center}
@@ -471,6 +318,66 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
+  \begin{frame}<1->
+  \frametitle{\begin{tabular}{c}New Design\end{tabular}}
+  \mbox{}\\[4mm]
+
+  \begin{center}
+  \begin{tikzpicture}
+  \alt<2>
+  {\draw (0,0) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
+  (A) {\textcolor{red}{\begin{minipage}{1.1cm}bind.\\spec.\end{minipage}}};}
+  {\draw (0,0) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm]
+  (A) {\begin{minipage}{1.1cm}bind.\\spec.\end{minipage}};}
+  
+  \alt<3>
+  {\draw (3,0) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
+  (B) {\textcolor{red}{\begin{minipage}{1.1cm}raw\\terms\end{minipage}}};}
+  {\draw (3,0) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm]
+  (B) {\begin{minipage}{1.1cm}raw\\terms\end{minipage}};}
+
+  \alt<4>
+  {\draw (6,0) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
+  (C) {\textcolor{red}{\begin{minipage}{1.1cm}$\alpha$-\\equiv.\end{minipage}}};}
+  {\draw (6,0) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm]
+  (C) {\begin{minipage}{1.1cm}$\alpha$-\\equiv.\end{minipage}};}
+  
+  \alt<5>
+  {\draw (0,-3) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
+  (D) {\textcolor{red}{\begin{minipage}{1.1cm}quot.\\type\end{minipage}}};}
+  {\draw (0,-3) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm]
+  (D) {\begin{minipage}{1.1cm}quot.\\type\end{minipage}};}
+
+  \alt<6>
+  {\draw (3,-3) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
+  (E) {\textcolor{red}{\begin{minipage}{1.1cm}lift\\thms\end{minipage}}};}
+  {\draw (3,-3) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm]
+  (E) {\begin{minipage}{1.1cm}lift\\thms\end{minipage}};}
+
+  \alt<7>
+  {\draw (6,-3) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
+  (F) {\textcolor{red}{\begin{minipage}{1.1cm}add.\\thms\end{minipage}}};}
+  {\draw (6,-3) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm]
+  (F) {\begin{minipage}{1.1cm}add.\\thms\end{minipage}};}
+  
+  \draw[->,white!50,line width=1mm] (A) -- (B);
+  \draw[->,white!50,line width=1mm] (B) -- (C);
+  \draw[->,white!50,line width=1mm, line join=round, rounded corners=2mm] 
+  (C) -- (8,0) -- (8,-1.5) -- (-2,-1.5) -- (-2,-3) -- (D);
+  \draw[->,white!50,line width=1mm] (D) -- (E);
+  \draw[->,white!50,line width=1mm] (E) -- (F);
+  \end{tikzpicture}
+  \end{center}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
   \begin{frame}<1-9>
   \frametitle{\begin{tabular}{c}Alpha-Equivalence\end{tabular}}
   \mbox{}\\[-3mm]
@@ -815,8 +722,6 @@
   \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\
   \end{tabular}
 
-
-
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
@@ -896,7 +801,7 @@
   \]
 
   \footnotesize
-  where $R =\;\approx_\alpha\times\approx_\alpha$ and $fv = \text{fv}\times\text{fv}$
+  where $R =\;\approx_\alpha\times\approx_\alpha$ and $fv = \text{fv}\cup\text{fv}$
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -988,6 +893,83 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
+  \begin{frame}<1>[t]
+  \frametitle{\begin{tabular}{c}Runtime is Acceptable\end{tabular}}
+  \mbox{}\\[-7mm]\mbox{}
+
+  \footnotesize
+  \begin{center}
+  \begin{tikzpicture}
+  \draw (0,0) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm]
+  (A) {\begin{minipage}{0.8cm}bind.\\spec.\end{minipage}};
+  
+  \draw (2,0) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm]
+  (B) {\begin{minipage}{0.8cm}raw\\terms\end{minipage}};
+
+  \draw (4,0) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm]
+  (C) {\begin{minipage}{0.8cm}$\alpha$-\\equiv.\end{minipage}};
+  
+  \draw (0,-2) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm]
+  (D) {\begin{minipage}{0.8cm}quot.\\type\end{minipage}};
+
+  \draw (2,-2) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm]
+  (E) {\begin{minipage}{0.8cm}lift\\thms\end{minipage}};
+
+  \draw (4,-2) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm]
+  (F) {\begin{minipage}{0.8cm}add.\\thms\end{minipage}};
+  
+  \draw[->,white!50,line width=1mm] (A) -- (B);
+  \draw[->,white!50,line width=1mm] (B) -- (C);
+  \draw[->,white!50,line width=1mm, line join=round, rounded corners=2mm] 
+  (C) -- (5,0) -- (5,-1) -- (-1,-1) -- (-1,-2) -- (D);
+  \draw[->,white!50,line width=1mm] (D) -- (E);
+  \draw[->,white!50,line width=1mm] (E) -- (F);
+  \end{tikzpicture}
+  \end{center}
+
+  \begin{itemize}
+  \item Core Haskell: 11 types, 49 term-constructors, 
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->
+  \frametitle{\begin{tabular}{c}Interesting Phenomenon\end{tabular}}
+  \mbox{}\\[-6mm]
+
+  \small
+  \mbox{}\hspace{10mm}
+  \begin{tabular}{ll}
+  \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\
+  \hspace{5mm}\phantom{$|$} Var name\\
+  \hspace{5mm}$|$ App trm trm\\
+  \hspace{5mm}$|$ Lam x::name t::trm
+  & \isacommand{bind} x \isacommand{in} t\\
+  \hspace{5mm}$|$ Let as::assn t::trm
+  & \isacommand{bind} bn(as) \isacommand{in} t\\
+  \multicolumn{2}{l}{\isacommand{and} assn $=$}\\
+  \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\
+  \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\
+  \multicolumn{2}{l}{\isacommand{binder} bn \isacommand{where}}\\
+  \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\
+  \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\
+  \end{tabular}\bigskip\medskip
+
+  we cannot quotient assn: ACons a \ldots $\not\approx_\alpha$ ACons b \ldots
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
   \begin{frame}<1->
   \frametitle{\begin{tabular}{c}Conclusion\end{tabular}}
   \mbox{}\\[-6mm]
@@ -995,14 +977,14 @@
   \begin{itemize}
   \item the user does not see anything of the raw level\medskip
   \only<1>{\begin{center}
-  Lam [a]. (Var a) \alert{$=$} Lam [b]. (Var b)
+  Lam a (Var a) \alert{$=$} Lam b (Var b)
   \end{center}\bigskip}
 
   \item<2-> we have not yet done function definitions (will come soon and
   we hope to make improvements over the old way there too)\medskip
-  \item<3-> it took quite some time to get here, but it seems worthwhile (POPL 2011 tutorial)\medskip
-  \item<4-> Thanks goes to Cezary!\\ 
-  \only<5->{\hspace{3mm}\ldots{}and of course others $\in$ Isabelle-team!} 
+  \item<3-> it took quite some time to get here, but it seems worthwhile 
+  (Barendregt's variable convention is unsound in general, 
+  found bugs in two paper proofs, quotient package, POPL 2011 tutorial)\medskip
   \end{itemize}
 
 




