diff -r dd3b9c046c7d -r 4da5c5c29009 Slides/Slides1.thy
--- a/Slides/Slides1.thy	Thu Jun 03 15:02:52 2010 +0200
+++ b/Slides/Slides1.thy	Mon Jun 07 11:43:01 2010 +0200
@@ -41,7 +41,7 @@
   \mbox{}\\[-6mm]
 
   \begin{itemize}
-  \item old Nominal provided a reasoning infrastructure for single binders\medskip
+  \item the old Nominal Isabelle provided a reasoning infrastructure for single binders\medskip
   
   \begin{center}
   Lam [a].(Var a)
@@ -64,7 +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\\
+  \pgfuseshading{smallspherered} & Barendregt-style reasoning about bound variables\\
   \end{tabular}
   \end{textblock}}
   
@@ -235,7 +235,7 @@
 
   \begin{itemize}
   \item this way of specifying binding is inspired by 
-  Ott\onslide<2->{, \alert{\bf but} we made adjustments:}\medskip
+  {\bf Ott}\onslide<2->{, \alert{\bf but} we made some adjustments:}\medskip
   
 
   \only<2>{
@@ -264,11 +264,11 @@
 
   \only<5>{
   \begin{itemize}
-  \item we allow multiple binders and bodies\smallskip
+  \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
+  the reason is that with our definitions of $\alpha$-equivalence
   \begin{center}
   \begin{tabular}{rcl}
   \isacommand{bind\_res} as \isacommand{in} x y & $\not\Leftrightarrow$ &
@@ -296,7 +296,7 @@
   \mbox{}\\[-3mm]
 
   \begin{itemize}
-  \item in old Nominal, we represented single binders as partial functions:\bigskip
+  \item in the old Nominal Isabelle, we represented single binders as partial functions:\bigskip
   
   \begin{center}
   \begin{tabular}{l}
@@ -396,7 +396,7 @@
   \only<1>{
   \begin{textblock}{8}(3,8.5)
   \begin{tabular}{l@ {\hspace{2mm}}p{8cm}}
-  \pgfuseshading{smallspherered} & $as$ is a set of atoms\ldots the binders\\
+  \pgfuseshading{smallspherered} & $as$ is a set of names\ldots the binders\\
   \pgfuseshading{smallspherered} & $x$ is the body\\
   \pgfuseshading{smallspherered} & $\approx_{\text{set}}$ is where the cardinality 
   of the binders has to be the same\\
@@ -415,7 +415,7 @@
   
   \only<8>{
   \begin{textblock}{8}(3,13.8)
-  \footnotesize $^*$ $as$ and $bs$ are \alert{lists} of atoms 
+  \footnotesize $^*$ $as$ and $bs$ are \alert{lists} of names 
   \end{textblock}}
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -424,7 +424,7 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}<1-2>
+  \begin{frame}<1-3>
   \frametitle{\begin{tabular}{c}Examples\end{tabular}}
   \mbox{}\\[-3mm]
 
@@ -445,7 +445,7 @@
   \end{itemize}
 
   
-  \only<2->{
+  \only<3->{
   \begin{textblock}{4}(0.3,12)
   \begin{tikzpicture}
   \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
@@ -461,7 +461,7 @@
   \end{minipage}};
   \end{tikzpicture}
   \end{textblock}}
-  \only<2->{
+  \only<3->{
   \begin{textblock}{4}(5.2,12)
   \begin{tikzpicture}
   \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
@@ -477,7 +477,7 @@
   \end{minipage}};
   \end{tikzpicture}
   \end{textblock}}
-  \only<2->{
+  \only<3->{
   \begin{textblock}{4}(10.2,12)
   \begin{tikzpicture}
   \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
@@ -572,7 +572,7 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}<1>
+  \begin{frame}<1-2>
   \frametitle{\begin{tabular}{c}Examples\end{tabular}}
   \mbox{}\\[-3mm]
 
@@ -635,6 +635,21 @@
   \end{tikzpicture}
   \end{textblock}}
 
+  \only<2>{
+  \begin{textblock}{6}(2.5,4)
+  \begin{tikzpicture}
+  \draw (0,0) node[inner sep=5mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
+  {\normalsize
+  \begin{minipage}{8cm}\raggedright
+  \begin{itemize}
+  \item \color{darkgray}$\alpha$-equivalences coincide when a single name is
+  abstracted
+  \item \color{darkgray}in that case they are equivalent to ``old-fashioned'' definitions of $\alpha$ 
+  \end{itemize}
+  \end{minipage}};
+  \end{tikzpicture}
+  \end{textblock}}
+
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
@@ -647,10 +662,10 @@
   \mbox{}\\[-7mm]
 
   \begin{itemize}
-  \item we take $(as, x) \approx\!\makebox[0mm][l]{${}_{\star}$}^{=,\text{supp}} (bs, y)$\medskip
-  \item they are equivalence relations\medskip
+  \item we take $(as, x) \approx\!\makebox[0mm][l]{${}_{{}*{}}$}^{=,\text{supp}} (bs, y)$\medskip
+  \item they are equivalence relations\medskip  
   \item we can therefore use the quotient package to introduce the 
-  types $\beta\;\text{abs}_\star$\bigskip
+  types $\beta\;\text{abs}_*$\bigskip 
   \begin{center}
   \only<1>{$[as].\,x$}
   \only<2>{$\text{supp}([as].x) = \text{supp}(x) - as$}
@@ -660,11 +675,15 @@
   $\exists \pi.$ & $\text{supp}(x) - as = \text{supp}(y) - bs$\\
   $\wedge$       & $\text{supp}(x) - as \fresh^* \pi$\\
   $\wedge$       & $\pi \act x = y $\\
-  $(\wedge$       & $\pi \act as = bs)\;^\star$\\
+  $(\wedge$       & $\pi \act as = bs)\;^*$\\
   \end{tabular}}
   \end{center}
   \end{itemize}
 
+  \only<1->{
+  \begin{textblock}{8}(12,3.8)
+  \footnotesize $^*$ set, res, list
+  \end{textblock}}
   
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -674,7 +693,7 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}<1>
-  \frametitle{\begin{tabular}{c}One Problem\end{tabular}}
+  \frametitle{\begin{tabular}{c}A Problem\end{tabular}}
   \mbox{}\\[-3mm]
 
   \begin{center}
@@ -824,14 +843,16 @@
   {\text{Let}\;as\;t \approx_\alpha \text{Let}\;as'\;t'}
   {(\text{bn}(as), t) \approx\!\makebox[0mm][l]{${}_{\text{list}}$}
     ^{\approx_\alpha,\text{fv}} (\text{bn}(as'), t') &
-   \onslide<2>{as \approx_\alpha^{\text{bn}} as'}}
-  \]
+   \onslide<2->{as \approx_\alpha^{\text{bn}} as'}}
+  \]\bigskip
 
 
+  \onslide<1->{\small{}bn-function $\Rightarrow$ \alert{deep binders}}
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
 
+
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
@@ -859,6 +880,51 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
 
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1>
+  \frametitle{\begin{tabular}{c}\LARGE``Raw'' Alpha-Equivalence\end{tabular}}
+  \mbox{}\\[6mm]
+
+  \begin{center}
+  LetRec as::assn t::trm \hspace{10mm}\isacommand{bind} bn(as) \isacommand{in} t \alert{as}\\
+  \end{center}
+
+
+  \[\mbox{}\hspace{-4mm}
+  \infer[\text{LetRec-}\!\approx_\alpha]
+  {\text{LetRec}\;as\;t \approx_\alpha \text{LetRec}\;as'\;t'}
+  {(\text{bn}(as), (t, as)) \approx\!\makebox[0mm][l]{${}_{\text{list}}$}
+    ^{R,fv} (\text{bn}(as'), (t', as'))} 
+  \]\bigskip
+  
+  \onslide<1->{\alert{deep recursive binders}}
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->
+  \frametitle{\begin{tabular}{c}Restrictions\end{tabular}}
+  \mbox{}\\[-6mm]
+
+  Our restrictions on binding specifications:
+
+  \begin{itemize}
+  \item a body can only occur once in a list of binding clauses\medskip
+  \item you can only have one binding function for a deep binder\medskip
+  \item binding functions can return: the empty set, singletons, unions (similarly for lists)
+  \end{itemize}
+
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
@@ -868,7 +934,7 @@
 
   \begin{itemize}
   \item we can show that $\alpha$'s are equivalence relations\medskip
-  \item as a result we can use the quotient package to introduce the type(s)
+  \item as a result we can use our quotient package to introduce the type(s)
   of $\alpha$-equated terms
 
   \[
@@ -881,8 +947,7 @@
 
 
   \item the properties for support are implied by the properties of $[\_].\_$
-  \item we can derive strong induction principles (almost automatic---just a matter of
-  another week or two)
+  \item we can derive strong induction principles (almost automatic---matter of time)
   \end{itemize}
 
 
@@ -928,7 +993,10 @@
   \end{center}
 
   \begin{itemize}
-  \item Core Haskell: 11 types, 49 term-constructors, 
+  \item Core Haskell: 11 types, 49 term-constructors, 7 binding functions
+  \begin{center}
+  $\sim$ 1 min
+  \end{center}
   \end{itemize}
 
   \end{frame}}
@@ -992,6 +1060,21 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
 
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[c]
+  \frametitle{\begin{tabular}{c}Questions?\end{tabular}}
+  \mbox{}\\[-6mm]
+
+  \begin{center}
+  \alert{\huge{Thanks!}}
+  \end{center}
+  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
 (*<*)
 end
 (*>*)
\ No newline at end of file