(*<*)
theory SlidesB
imports "~~/src/HOL/Library/LaTeXsugar" "../Nominal/Nominal2"
begin

notation (latex output)
  set ("_") and
  Cons  ("_::/_" [66,65] 65) 

(*>*)


text_raw {*
  %% was \begin{colormixin}{20!averagebackgroundcolor}
  %% 
  %% is \begin{colormixin}{50!averagebackgroundcolor}
  \renewcommand{\slidecaption}{Dagstuhl, 14 October 2013}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}
  \frametitle{%
  \begin{tabular}{@ {}c@ {}}
  \Huge Nominal Isabelle\\[0mm]
  \Large or, How Not to be Intimidated by\\[-3mm]
  \Large the Variable Convention\\[-5mm]
  \end{tabular}}
  
  \begin{center}
  Christian Urban\\[1mm]
  King's College London\\[-4mm]\mbox{}
  \end{center}
 
  \begin{center}
  \begin{block}{}
  \color{gray}
  \small
  {\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[1mm] 
  If $M_1,\ldots,M_n$ occur in a certain mathematical context
  (e.g. definition, proof), then in these terms all bound variables 
  are chosen to be different from the free variables.\\[2mm]
  
  \footnotesize\hfill Henk Barendregt in ``The Lambda-Calculus: Its Syntax and Semantics''
  \end{block}
  \end{center}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1->[c]
  \frametitle{}

  \begin{center}
  \begin{tabular}{@ {\hspace{-2mm}}c@ {}}
  \includegraphics[scale=0.36]{phd-2.jpg}\,
  \includegraphics[scale=0.36]{phd-1.jpg}\\
  \hfill\textcolor{gray}{\small dinner after my PhD examination}
  \end{tabular}
  \end{center}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1->[c]
  \frametitle{}

  \begin{itemize}
  \item \normalsize Aim: develop Nominal Isabelle for reasoning formally about 
  programming languages\\[-10mm]\mbox{}
  \end{itemize}
  
  \begin{center}
  \begin{block}{}
  \color{gray}
  \footnotesize
  {\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[0mm] 
  If $M_1,\ldots,M_n$ occur in a certain mathematical context
  (e.g. definition, proof), then in these terms all bound variables 
  are chosen to be different from the free variables.\hfill ---Henk Barendregt
  \end{block}
  \end{center}\pause

  \mbox{}\\[-19mm]\mbox{}

  \begin{itemize}
  \item found an error in an ACM journal paper by Bob Harper and Frank Pfenning 
  about LF (and fixed it in three ways)
  \item found also fixable errors in my Ph.D.-thesis about cut-elimination
  (examined by Henk Barendregt and Andy Pitts)
  \item found that the variable convention can in principle be used for proving false
  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1->[c]
  \frametitle{Nominal Techniques}

  \begin{itemize}
  \item Andy Pitts showed me that permutations\\ preserve $\alpha$-equivalence:
  \begin{center}
  \smath{t_1 \approx_{\alpha} t_2 \quad \Rightarrow\quad \pi \act t_1 \approx_{\alpha} \pi \act t_2} 
  \end{center}

  \item also permutations and substitutions commute, if you suspend permutations
  in front of variables
  \begin{center}
  \smath{\pi\act\sigma(t) = \sigma(\pi\act t)}
  \end{center}\medskip\medskip

  \item this allowed us to define as simple Nominal Unification algorithm\medskip
  \begin{center}
  \smath{\nabla \vdash t \approx^?_{\alpha} t'}\hspace{2cm}
  \smath{\nabla \vdash a \fresh^? t}
  \end{center}
  \end{itemize}

  %\begin{textblock}{3}(13.1,1.3)
  %\includegraphics[scale=0.26]{andrewpitts.jpg}
  %\end{textblock}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Nominal Isabelle}

  \begin{itemize}
  \item a general theory about atoms and permutations\medskip
  \begin{itemize}
  \item sorted atoms and
  \item sort-respecting permutations\bigskip
  \end{itemize}
  
  \item support and freshness
  \begin{center}
  \begin{tabular}{l}
  \smath{\textit{supp}(x) \dn \{ a \mid \textit{infinite}\,\{ b \mid \swap{a}{b}\act x \not= x\}\}}\\[2mm]
  \smath{a \fresh x \dn a \notin \textit{supp}(x)}
  \end{tabular}
  \end{center}\bigskip\pause

  \item allow users to reason about alpha-equivalence classes as if they were 
  syntax trees
  %
  %\item $\alpha$-equivalence
  %\begin{center}
  %\begin{tabular}{l}
  %\smath{as.x \approx_\alpha bs.y \dn}\\[2mm]
  %\hspace{2cm}\smath{\exists \pi.\;\text{supp}(x) - as = \text{supp}(y) - bs}\\ 
  %\hspace{2cm}\smath{\;\wedge\; \text{supp}(x) - as \fresh \pi}\\
  %\hspace{2cm}\smath{\;\wedge\; \pi \act x = y}
  %\end{tabular}
  %\end{center}
  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1-7>
  \frametitle{New Types in HOL}

   \begin{center}
  \begin{tikzpicture}[scale=1.5]
  %%%\draw[step=2mm] (-4,-1) grid (4,1);
  
  \onslide<2-4,6->{\draw[very thick] (0.7,0.4) circle (4.25mm);}
  \onslide<1-4,6->{\draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);}
  \onslide<3-5,6->{\draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);}
  
  \onslide<3-4,6->{\draw (-2.0, 0.845) --  (0.7,0.845);}
  \onslide<3-4,6->{\draw (-2.0,-0.045)  -- (0.7,-0.045);}

  \onslide<4-4,6->{\alert{\draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]classes\end{tabular}};}}
  \onslide<4-5,6->{\alert{\draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};}}
  \onslide<1-4,6->{\draw (1.8, 0.48) node[right=-0.1mm]
    {\footnotesize\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ \onslide<4-4,6->{\alert{(sets of raw terms)}}\end{tabular}};}
  \onslide<2-4,6->{\draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};}
  \onslide<3-5,6->{\draw (-3.25, 0.55) node {\footnotesize\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};}
  
  \onslide<3-4,6->{\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);}
  \onslide<3-4,6->{\draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};}

  \onslide<6->{\draw[->, line width=2mm, red] (-1.0,-0.4) -- (0.35,0.16);}
  \end{tikzpicture}
  \end{center}
  
  \begin{center}
  \textcolor{red}{\large\bf\onslide<6->{define \boldmath$\alpha$-equivalence}}
  \end{center}

  \begin{textblock}{9}(2.8,12.5)
  \only<7>{
  \begin{tikzpicture}
  \draw (0,0) node[fill=cream, text width=8.5cm, thick, draw=red, rounded corners=1mm] (nn)
  {The ``new types mechanism'' is the reason why there is no Nominal Coq.};
  \end{tikzpicture}}
  \end{textblock}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1-3>[c]
  \frametitle{HOL vs.~Nominal}

  \begin{itemize}
  \item Nominal logic by Pitts is incompatible 
  with choice principles\medskip

  \item but HOL includes Hilbert's epsilon\pause\bigskip

  \item The solution: Do not require that everything has finite support\medskip

  \begin{center}
  \smath{\onslide<1-2>{\textit{finite}(\textit{supp}(x))  \quad\Rightarrow\quad} a \fresh a.x}
  \end{center}
  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1-5>
  \frametitle{\begin{tabular}{c}Our Work\end{tabular}}
  \mbox{}\\[-6mm]

    \begin{center}
  \begin{tikzpicture}[scale=1.5]
  %%%\draw[step=2mm] (-4,-1) grid (4,1);
  
  \onslide<1>{\draw[very thick] (0.7,0.4) circle (4.25mm);}
  \onslide<1>{\draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);}
  \onslide<1->{\draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);}
  
  \onslide<1>{\draw (-2.0, 0.845) --  (0.7,0.845);}
  \onslide<1>{\draw (-2.0,-0.045)  -- (0.7,-0.045);}

  \onslide<1>{\alert{\draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]classes\end{tabular}};}}
  \onslide<1->{\alert{\draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};}}
  \onslide<1>{\draw (1.8, 0.48) node[right=-0.1mm]
    {\footnotesize\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ \onslide<1>{\alert{(sets of raw terms)}}\end{tabular}};}
  \onslide<1>{\draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};}
  \onslide<1->{\draw (-3.25, 0.55) node {\footnotesize\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};}
  
  \onslide<1>{\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);}
  \onslide<1>{\draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};}

  %%\onslide<1>{\draw[->, line width=2mm, red] (-1.0,-0.4) -- (0.35,0.16);}
  \end{tikzpicture}
  \end{center}
  
  \begin{textblock}{9.5}(6,3.5)
  \begin{itemize}
  \item<1-> define fv and $\alpha$
  \item<2-> build quotient / new type
  \item<3-> derive a reasoning infrastructure ($\fresh$, distinctness, injectivity, cases,\ldots) 
  \item<4-> derive a {\bf stronger} cases lemma
  \item<5-> from this, a {\bf stronger} induction principle (Barendregt variable convention built in)\\
  \begin{center}
  \textcolor{blue}{Foo ($\lambda x. \lambda y. t$) ($\lambda u. \lambda v. s$)} 
  \end{center}
  \end{itemize}
  \end{textblock}


  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}
  \frametitle{Nominal Isabelle} 

  \begin{itemize}
  \item Users can for example define lambda-terms as:
  \end{itemize}
*}
      
 atom_decl name   text_raw {*\medskip\isanewline *}
	nominal_datatype lam =
	    Var name
	  | App lam lam 
	  | Lam x::name t::lam   binds x in t ("Lam _. _")


text_raw {*
  \mbox{}\bigskip

  \begin{itemize}
  \item These are \underline{\bf named} alpha-equivalence classes, for example
  \end{itemize}

  \begin{center}
  \gb{@{text "Lam a.(Var a)"}} \alert{$\,=\,$} \gb{@{text "Lam b.(Var b)"}}
  \end{center}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}
  \frametitle{\Large (Weak) Induction Principles} 

  \begin{itemize}
  \item The usual induction principle for lambda-terms is as follows:

  \begin{center}
  \mbox{}\hspace{-1mm}\begin{beamercolorbox}[sep=1mm, wd=9cm]{boxcolor}
  \centering\smath{%
  \infer{P\,t}
  {\begin{array}{l}
  \forall x.\;P\,x\\[2mm]
  \forall t_1\,t_2.\;P\,t_1\wedge P\,t_2\Rightarrow P\,(t_1\;t_2)\\[2mm]
  \forall x\,t.\;P\,t\Rightarrow P\,(\lambda x.t)\\
  \end{array}
  }}
  \end{beamercolorbox}
  \end{center}

  \item It requires us in the lambda-case to show the property \smath{P} for
  all binders \smath{x}.\medskip\\ 

  (This nearly always requires renamings and they can be 
  tricky to automate.)
  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}


text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}
  \frametitle{\Large Strong Induction Principles} 

  \begin{itemize}
  \item Therefore we introduced the following strong induction principle:

  \begin{center}
  \mbox{}\hspace{-2mm}\begin{beamercolorbox}[sep=1mm, wd=11.5cm]{boxcolor}
  \centering\smath{%
  \infer{\tikz[remember picture] \node[inner sep=1mm] (n1a) {\alert<4>{$P$}};%
         \tikz[remember picture] \node[inner sep=1mm] (n2a) {\alert<3>{$c$}};%
         \tikz[remember picture] \node[inner sep=1mm] (n3a) {\alert<2>{$t$}};}
  {\begin{array}{l}
  \forall x\,c.\;P\,c\;x\\[2mm]
  \forall t_1\,t_2\,c.\;(\forall d.\,P d\,t_1)\wedge (\forall d. P\,d\,t_2)
  \Rightarrow P\,c\;(t_1\,t_2)\\[2mm]
  \forall x\,t\,c.\;\alert<1>{x\fresh \alert<3>{c}} 
  \wedge (\forall d. P\,d\,t)\Rightarrow P\,c\;(\lambda x.t)
  \end{array}
  }}
  \end{beamercolorbox}
  \end{center}
  \end{itemize}

  \begin{textblock}{11}(0.9,10.9)
  \only<2>{
  \begin{tikzpicture}[remember picture]
  \draw (0,0) node[fill=cream, text width=10.5cm, thick, draw=red, rounded corners=1mm] (n3b)
  { The variable over which the induction proceeds:\\[2mm]
    \hspace{3mm}``\ldots By induction over the structure of \smath{M}\ldots''};

  \path[overlay, ->, ultra thick, red] (n3b) edge[out=90, in=-110] (n3a);
  \end{tikzpicture}}

  \only<3>{
  \begin{tikzpicture}[remember picture]
  \draw (0,0) node[fill=cream, text width=11cm, thick, draw=red, rounded corners=1mm] (n2b)
  {The {\bf context} of the induction; i.e.~what the binder should be fresh for
   $\quad\Rightarrow$ \smath{(x,y,N,L)}:\\[2mm]
   ``\ldots By the variable convention we can assume \mbox{\smath{z\not\equiv x,y}} 
     and \smath{z} not free in \smath{N}$\!$,\,\smath{L}\ldots''};

  \path[overlay, ->, ultra thick, red] (n2b) edge[out=90, in=-100] (n2a);
  \end{tikzpicture}}

  \only<4>{
  \begin{tikzpicture}[remember picture]
  \draw (0,0) node[fill=cream, text width=11cm, thick, draw=red, rounded corners=1mm] (n1b)
  {The property to be proved by induction:\\[-3mm]
  \begin{center}\small
  \begin{tabular}{l}
  \smath{\!\!\lambda
  (x,\!y,\!N\!,\!L).\,\lambda M.\;\,x\not=y\,\wedge\,x\fresh L\,\Rightarrow}\\[1mm]
  \hspace{8mm}
  \smath{M[x\!:=\!N][y\!:=\!L] = M[y\!:=\!L][x\!:=\!N[y\!:=\!L]]}  
  \end{tabular}
  \end{center}};

  \path[overlay, ->, ultra thick, red] (n1b) edge[out=90, in=-70] (n1a);
  \end{tikzpicture}}
  \end{textblock}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1-4>
  \frametitle{\begin{tabular}{c}Binding Sets of Names\end{tabular}}
  \mbox{}\\[-3mm]

  \begin{itemize}
  \item binding sets of names has some interesting properties:\medskip
  
  \begin{center}
  \begin{tabular}{l}
  \textcolor{blue}{$\forall\{x, y\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{y, x\}.\, y \rightarrow x$}
  \bigskip\smallskip\\

  \onslide<2->{%
  \textcolor{blue}{$\forall\{x, y\}.\, x \rightarrow y \;\;\not\approx_\alpha\;\; \forall\{z\}.\, z \rightarrow z$}
  }\bigskip\smallskip\\

  \onslide<3->{%
  \textcolor{blue}{$\forall\{x\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{x, \alert{z}\}.\, x \rightarrow y$}
  }\medskip\\
  \onslide<3->{\hspace{4cm}\small provided $z$ is fresh for the type}
  \end{tabular}
  \end{center}
  \end{itemize}
  
  \begin{textblock}{8}(2,14.5)
  \footnotesize $^*$ $x$, $y$, $z$ are assumed to be distinct
  \end{textblock}

  \only<4>{
  \begin{textblock}{6}(2.5,4)
  \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
  For type-schemes the order of bound names does not matter, and
  $\alpha$-equivalence is preserved under \alert{vacuous} binders.
  \end{minipage}};
  \end{tikzpicture}
  \end{textblock}}
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1-3>
  \frametitle{\begin{tabular}{c}Other Binding Modes\end{tabular}}
  \mbox{}\\[-3mm]

  \begin{itemize}
  \item alpha-equivalence being preserved under vacuous binders is \underline{not} always
  wanted:\bigskip\bigskip\normalsize
  
  \textcolor{blue}{\begin{tabular}{@ {\hspace{-8mm}}l}
  $\text{let}\;x = 3\;\text{and}\;y = 2\;\text{in}\;x - y\;\text{end}$\medskip\\
  \onslide<2->{$\;\;\;\only<2>{\approx_\alpha}\only<3>{\alert{\not\approx_\alpha}}
   \text{let}\;y = 2\;\text{and}\;x = 3\only<3->{\alert{\;\text{and}
    \;z = \text{loop}}}\;\text{in}\;x - y\;\text{end}$}
  \end{tabular}}
  

  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1>
  \frametitle{\begin{tabular}{c}\Large{}Even Another Binding Mode\end{tabular}}
  \mbox{}\\[-3mm]

  \begin{itemize}
  \item sometimes one wants to abstract more than one name, but the order \underline{does} matter\bigskip
  
  \begin{center}
  \textcolor{blue}{\begin{tabular}{@ {\hspace{-8mm}}l}
  $\text{let}\;(x, y) = (3, 2)\;\text{in}\;x - y\;\text{end}$\medskip\\
  $\;\;\;\not\approx_\alpha
   \text{let}\;(y, x) = (3, 2)\;\text{in}\;x - y\;\text{end}$
  \end{tabular}}
  \end{center}
  

  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<2-3>
  \frametitle{\begin{tabular}{c}Specification of Binding\end{tabular}}
  \mbox{}\\[-6mm]

  \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 \only<2->{x::}name \only<2->{t::}trm
  & \onslide<2->{\isacommand{bind} x \isacommand{in} t}\\
  \hspace{5mm}$|$ Let \only<2->{as::}assns \only<2->{t::}trm
  & \onslide<2->{\isacommand{bind} bn(as) \isacommand{in} t}\\
  \multicolumn{2}{l}{\isacommand{and} assns $=$}\\
  \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\
  \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assns}\\
  \multicolumn{2}{l}{\onslide<3->{\isacommand{binder} bn \isacommand{where}}}\\
  \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}



  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}


text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}
  \frametitle{So Far So Good}

  \begin{itemize}
  \item A Faulty Lemma with the Variable Convention?\\[-8mm]\mbox{}
  \end{itemize}

  \begin{center}
  \begin{block}{}
  \color{gray}
  \small%
  {\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[1mm] 
  If $M_1,\ldots,M_n$ occur in a certain mathematical context
  (e.g. definition, proof), then in these terms all bound variables 
  are chosen to be different from the free variables.\\[2mm]
  
  \footnotesize\hfill Barendregt in ``The Lambda-Calculus: Its Syntax and Semantics''
  \end{block}
  \end{center}

  \mbox{}\\[-18mm]\mbox{}

  \begin{columns}
  \begin{column}[t]{4.7cm}
  Inductive Definitions:\\
  \begin{center}
  \smath{\infer{\text{concl}}{\text{prem}_1 \ldots \text{prem}_n\;\text{scs}}}
  \end{center}
  \end{column}
  \begin{column}[t]{7cm}
  Rule Inductions:\\[2mm]
  \begin{tabular}{l@ {\hspace{2mm}}p{5.5cm}}
  1.) & Assume the property for\\ & the premises. Assume \\ & the side-conditions.\\[1mm]
  2.) & Show the property for\\ & the conclusion.\\
  \end{tabular}
  \end{column}
  \end{columns}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \setbeamerfont{itemize/enumerate subbody}{size=\normalsize}
  \begin{frame}[sqeeze]
  \frametitle{Faulty Reasoning} 

  %\mbox{}

  \begin{itemize}
  \item Consider the two-place relation \smath{\text{foo}}:\medskip
  \begin{center}
  \begin{tabular}{ccc}
  \raisebox{2.5mm}{\colorbox{cream}{%
  \smath{\;\infer{x\mapsto x}{}}}}\hspace{2mm}
  &
  \raisebox{2mm}{\colorbox{cream}{%
  \smath{\infer{t_1\;t_2\mapsto t_1\;t_2}{}}}}\hspace{2mm}
  &
  \colorbox{cream}{%
  \smath{\infer{\lambda x.t\mapsto t'}{t\mapsto t'}}}\\[5mm]
  \end{tabular}
  \end{center}

  \pause

  \item The lemma we going to prove:\smallskip
  \begin{center}
  Let \smath{t\mapsto t'}. If \smath{y\fresh t} then \smath{y\fresh t'}.
  \end{center}\bigskip

  \only<3>{
  \item Cases 1 and 2 are trivial:\medskip
  \begin{itemize}
  \item If \smath{y\fresh x} then \smath{y\fresh x}.
  \item If \smath{y\fresh t_1\,t_2} then \smath{y\fresh t_1\,t_2}.
  \end{itemize}
  }

  \only<4->{
  \item Case 3:
  \begin{itemize}
  \item We know \tikz[remember picture,baseline=(ta.base)] \node (ta) {\smath{y\fresh \lambda x.t}.}; 
  We have to show \smath{y\fresh t'}.$\!\!\!\!$ 
  \item The IH says: if \smath{y\fresh t} then \smath{y\fresh t'}.
  \item<7,8> So we have \smath{y\fresh t}. Hence \smath{y\fresh t'} by IH. Done!
  \end{itemize}
  }
  \end{itemize}
  
  \begin{textblock}{11.3}(0.7,0.6)
  \only<5-7>{
  \begin{tikzpicture}
  \draw (0,0) node[fill=cream, text width=11.2cm, thick, draw=red, rounded corners=1mm] (nn)
  {{\bf Variable Convention:}\\[2mm] 
  \small
   If $M_1,\ldots,M_n$ occur in a certain mathematical context
   (e.g. definition, proof), then in these terms all bound variables 
   are chosen to be different from the free variables.\smallskip

  \normalsize
   {\bf In our case:}\\[2mm]
   The free variables are \smath{y} and \smath{t'}; the bound one is 
   \smath{x}.\medskip
          
   By the variable convention we conclude that \smath{x\not= y}.
  };
  \end{tikzpicture}}
  \end{textblock}

  \begin{textblock}{9.2}(3.6,9.2)
  \only<6,7>{
  \begin{tikzpicture}[remember picture]
  \draw (0,0) node[fill=cream, text width=9cm, thick, draw=red, rounded corners=1mm] (tb)
  {\small\smath{y\!\not\in\! \text{fv}(\lambda x.t) \Longleftrightarrow
          y\!\not\in\! \text{fv}(t)\!-\!\{x\}
          \stackrel{x\not=y}{\Longleftrightarrow}
          y\!\not\in\! \text{fv}(t)}};

  \path[overlay, ->, ultra thick, red] (tb) edge[out=-120, in=75] (ta);
  \end{tikzpicture}}
  \end{textblock}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}


text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}
  \frametitle{Conclusions} 

  \begin{itemize}
  \item The user does not see anything of the ``raw'' level.
  \item The Nominal Isabelle automatically derives the strong structural
  induction principle for \underline{\bf all} nominal datatypes (not just the 
  lambda-calculus)

  \item They are easy to use: you just have to think carefully what the variable
  convention should be.

  \item We can explore the \colorbox{black}{\textcolor{white}{dark}} corners 
  of the variable convention: when and where it can be used safely.
  
  \item<2> \alert{\bf Main Point:} Actually these proofs using the
  variable convention are all trivial / obvious / routine\ldots {\bf provided} 
  you use Nominal Isabelle. ;o)
 
  \end{itemize}


  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1>[b]
  \frametitle{
  \begin{tabular}{c}
  \mbox{}\\[13mm]
  \alert{\LARGE Thank you very much!}\\
  \alert{\Large Questions?}
  \end{tabular}}


  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

(*<*)
end
(*>*)