(*<*)
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\\[-6mm]\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{itemize}
  \item \normalsize Aim: develop Nominal Isabelle for reasoning 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 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
  \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\}\}}\\
  \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 like about 
  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=8cm, thick, draw=red, rounded corners=1mm] (nn)
  {The ``new types'' are 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 are incompatible 
  with choice principles\medskip

  \item 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-> defined fv and $\alpha$
  \item<2-> built quotient / new type
  \item<3-> derived 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 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}.\smallskip\\ 

  (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)
  \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
(*>*)