1 (*<*)

     2 theory SlidesB

     3 imports "~~/src/HOL/Library/LaTeXsugar" "../Nominal/Nominal2"

     4 begin

     5 

     6 notation (latex output)

     7   set ("_") and

     8   Cons  ("_::/_" [66,65] 65) 

     9 

    10 (*>*)

    11 

    12 

    13 text_raw {*

    14   %% was \begin{colormixin}{20!averagebackgroundcolor}

    15   %% 

    16   %% is \begin{colormixin}{50!averagebackgroundcolor}

    17   \renewcommand{\slidecaption}{Dagstuhl, 14 October 2013}

    18   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    19   \mode<presentation>{

    20   \begin{frame}

    21   \frametitle{%

    22   \begin{tabular}{@ {}c@ {}}

    23   \Huge Nominal Isabelle\\[0mm]

    24   \Large or, How Not to be Intimidated by\\[-3mm]

    25   \Large the Variable Convention\\[-5mm]

    26   \end{tabular}}

    27   

    28   \begin{center}

    29   Christian Urban\\[1mm]

    30   King's College London\\[-6mm]\mbox{}

    31   \end{center}

    32  

    33   \begin{center}

    34   \begin{block}{}

    35   \color{gray}

    36   \small

    37   {\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[1mm] 

    38   If $M_1,\ldots,M_n$ occur in a certain mathematical context

    39   (e.g. definition, proof), then in these terms all bound variables 

    40   are chosen to be different from the free variables.\\[2mm]

    41   

    42   \footnotesize\hfill Henk Barendregt in ``The Lambda-Calculus: Its Syntax and Semantics''

    43   \end{block}

    44   \end{center}

    45 

    46   \end{frame}}

    47   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    48 

    49 *}

    50 

    51 text_raw {*

    52   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    53   \mode<presentation>{

    54   \begin{frame}<1->[c]

    55   \frametitle{}

    56 

    57   \begin{itemize}

    58   \item \normalsize Aim: develop Nominal Isabelle for reasoning about programming languages\\[-10mm]\mbox{}

    59   \end{itemize}

    60   

    61   \begin{center}

    62   \begin{block}{}

    63   \color{gray}

    64   \footnotesize

    65   {\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[0mm] 

    66   If $M_1,\ldots,M_n$ occur in a certain mathematical context

    67   (e.g. definition, proof), then in these terms all bound variables 

    68   are chosen to be different from the free variables.\hfill ---Henk Barendregt

    69   \end{block}

    70   \end{center}\pause

    71 

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

    73 

    74   \begin{itemize}

    75   \item found an error in an ACM journal paper by Bob Harper and Frank Pfenning 

    76   about LF (and fixed it in three ways)

    77   \item found also fixable errors in my Ph.D.-thesis about cut-elimination

    78   (examined by Henk Barendregt and Andy Pitts)

    79   \item found the variable convention can in principle be used for proving false

    80   \end{itemize}

    81 

    82   \end{frame}}

    83   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    84 *}

    85 

    86 

    87 text_raw {*

    88   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    89   \mode<presentation>{

    90   \begin{frame}<1->[c]

    91   \frametitle{Nominal Techniques}

    92 

    93   \begin{itemize}

    94   \item Andy Pitts showed me that permutations\\ preserve $\alpha$-equivalence:

    95   \begin{center}

    96   \smath{t_1 \approx_{\alpha} t_2 \quad \Rightarrow\quad \pi \act t_1 \approx_{\alpha} \pi \act t_2} 

    97   \end{center}

    98 

    99   \item also permutations and substitutions commute, if you suspend permutations

   100   in front of variables

   101   \begin{center}

   102   \smath{\pi\act\sigma(t) = \sigma(\pi\act t)}

   103   \end{center}\medskip\medskip

   104 

   105   \item this allowed us to define as simple Nominal Unification algorithm\medskip

   106   \begin{center}

   107   \smath{\nabla \vdash t \approx^?_{\alpha} t'}\hspace{2cm}

   108   \smath{\nabla \vdash a \fresh^? t}

   109   \end{center}

   110   \end{itemize}

   111 

   112   %\begin{textblock}{3}(13.1,1.3)

   113   %\includegraphics[scale=0.26]{andrewpitts.jpg}

   114   %\end{textblock}

   115 

   116   \end{frame}}

   117   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   118 *}

   119 

   120 text_raw {*

   121   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   122   \mode<presentation>{

   123   \begin{frame}[c]

   124   \frametitle{Nominal Isabelle}

   125 

   126   \begin{itemize}

   127   \item a general theory about atoms and permutations\medskip

   128   \begin{itemize}

   129   \item sorted atoms and

   130   \item sort-respecting permutations

   131   \end{itemize}

   132   

   133   \item support and freshness

   134   \begin{center}

   135   \begin{tabular}{l}

   136   \smath{\textit{supp}(x) \dn \{ a \mid \textit{infinite}\,\{ b \mid \swap{a}{b}\act x \not= x\}\}}\\

   137   \smath{a \fresh x \dn a \notin \textit{supp}(x)}

   138   \end{tabular}

   139   \end{center}\bigskip\pause

   140 

   141   \item allow users to reason about alpha-equivalence classes like about 

   142   syntax trees

   143   %

   144   %\item $\alpha$-equivalence

   145   %\begin{center}

   146   %\begin{tabular}{l}

   147   %\smath{as.x \approx_\alpha bs.y \dn}\\[2mm]

   148   %\hspace{2cm}\smath{\exists \pi.\;\text{supp}(x) - as = \text{supp}(y) - bs}\\ 

   149   %\hspace{2cm}\smath{\;\wedge\; \text{supp}(x) - as \fresh \pi}\\

   150   %\hspace{2cm}\smath{\;\wedge\; \pi \act x = y}

   151   %\end{tabular}

   152   %\end{center}

   153   \end{itemize}

   154 

   155   \end{frame}}

   156   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   157 *}

   158 

   159 text_raw {*

   160   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   161   \mode<presentation>{

   162   \begin{frame}<1-7>

   163   \frametitle{New Types in HOL}

   164 

   165    \begin{center}

   166   \begin{tikzpicture}[scale=1.5]

   167   %%%\draw[step=2mm] (-4,-1) grid (4,1);

   168   

   169   \onslide<2-4,6->{\draw[very thick] (0.7,0.4) circle (4.25mm);}

   170   \onslide<1-4,6->{\draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);}

   171   \onslide<3-5,6->{\draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);}

   172   

   173   \onslide<3-4,6->{\draw (-2.0, 0.845) --  (0.7,0.845);}

   174   \onslide<3-4,6->{\draw (-2.0,-0.045)  -- (0.7,-0.045);}

   175 

   176   \onslide<4-4,6->{\alert{\draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]classes\end{tabular}};}}

   177   \onslide<4-5,6->{\alert{\draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};}}

   178   \onslide<1-4,6->{\draw (1.8, 0.48) node[right=-0.1mm]

   179     {\footnotesize\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ \onslide<4-4,6->{\alert{(sets of raw terms)}}\end{tabular}};}

   180   \onslide<2-4,6->{\draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};}

   181   \onslide<3-5,6->{\draw (-3.25, 0.55) node {\footnotesize\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};}

   182   

   183   \onslide<3-4,6->{\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);}

   184   \onslide<3-4,6->{\draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};}

   185 

   186   \onslide<6->{\draw[->, line width=2mm, red] (-1.0,-0.4) -- (0.35,0.16);}

   187   \end{tikzpicture}

   188   \end{center}

   189   

   190   \begin{center}

   191   \textcolor{red}{\large\bf\onslide<6->{define \boldmath$\alpha$-equivalence}}

   192   \end{center}

   193 

   194   \begin{textblock}{9}(2.8,12.5)

   195   \only<7>{

   196   \begin{tikzpicture}

   197   \draw (0,0) node[fill=cream, text width=8cm, thick, draw=red, rounded corners=1mm] (nn)

   198   {The ``new types'' are the reason why there is no Nominal Coq.};

   199   \end{tikzpicture}}

   200   \end{textblock}

   201 

   202   \end{frame}}

   203   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   204 *}

   205 

   206 text_raw {*

   207   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   208   \mode<presentation>{

   209   \begin{frame}<1-3>[c]

   210   \frametitle{HOL vs.~Nominal}

   211 

   212   \begin{itemize}

   213   \item Nominal logic by Pitts are incompatible 

   214   with choice principles\medskip

   215 

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

   217 

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

   219 

   220   \begin{center}

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

   222   \end{center}

   223   \end{itemize}

   224 

   225   \end{frame}}

   226   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   227 *}

   228 

   229 text_raw {*

   230   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   231   \mode<presentation>{

   232   \begin{frame}<1-5>

   233   \frametitle{\begin{tabular}{c}Our Work\end{tabular}}

   234   \mbox{}\\[-6mm]

   235 

   236     \begin{center}

   237   \begin{tikzpicture}[scale=1.5]

   238   %%%\draw[step=2mm] (-4,-1) grid (4,1);

   239   

   240   \onslide<1>{\draw[very thick] (0.7,0.4) circle (4.25mm);}

   241   \onslide<1>{\draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);}

   242   \onslide<1->{\draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);}

   243   

   244   \onslide<1>{\draw (-2.0, 0.845) --  (0.7,0.845);}

   245   \onslide<1>{\draw (-2.0,-0.045)  -- (0.7,-0.045);}

   246 

   247   \onslide<1>{\alert{\draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]classes\end{tabular}};}}

   248   \onslide<1->{\alert{\draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};}}

   249   \onslide<1>{\draw (1.8, 0.48) node[right=-0.1mm]

   250     {\footnotesize\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ \onslide<1>{\alert{(sets of raw terms)}}\end{tabular}};}

   251   \onslide<1>{\draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};}

   252   \onslide<1->{\draw (-3.25, 0.55) node {\footnotesize\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};}

   253   

   254   \onslide<1>{\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);}

   255   \onslide<1>{\draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};}

   256 

   257   \onslide<1>{\draw[->, line width=2mm, red] (-1.0,-0.4) -- (0.35,0.16);}

   258   \end{tikzpicture}

   259   \end{center}

   260   

   261   \begin{textblock}{9.5}(6,3.5)

   262   \begin{itemize}

   263   \item<1-> defined fv and $\alpha$

   264   \item<2-> built quotient / new type

   265   \item<3-> derived a reasoning infrastructure ($\fresh$, distinctness, injectivity, cases,\ldots) 

   266   \item<4-> derive a {\bf stronger} cases lemma

   267   \item<5-> from this, a {\bf stronger} induction principle (Barendregt variable convention built in)\\

   268   \begin{center}

   269   \textcolor{blue}{Foo ($\lambda x. \lambda y. t$) ($\lambda u. \lambda v. s$)} 

   270   \end{center}

   271   \end{itemize}

   272   \end{textblock}

   273 

   274 

   275   \end{frame}}

   276   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   277 *}

   278 

   279 text_raw {*

   280 

   281   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   282   \mode<presentation>{

   283   \begin{frame}

   284   \frametitle{Nominal Isabelle} 

   285 

   286   \begin{itemize}

   287   \item Users can define lambda-terms as:

   288   \end{itemize}

   289 *}

   290       

   291  atom_decl name   text_raw {*\medskip\isanewline *}

   292 	nominal_datatype lam =

   293 	    Var "name"

   294 	  | App "lam" "lam" 

   295 	  | Lam x::"name" t::"lam" binds x in t ("Lam _. _")

   296 

   297 

   298 text_raw {*

   299   \mbox{}\bigskip

   300 

   301   \begin{itemize}

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

   303   \end{itemize}

   304 

   305   \begin{center}

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

   307   \end{center}

   308 

   309   \end{frame}}

   310   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   311 

   312 *}

   313 

   314 text_raw {*

   315 

   316   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   317   \mode<presentation>{

   318   \begin{frame}

   319   \frametitle{\Large (Weak) Induction Principles} 

   320 

   321   \begin{itemize}

   322   \item The usual induction principle for lambda-terms is as follows:

   323 

   324   \begin{center}

   325   \mbox{}\hspace{-1mm}\begin{beamercolorbox}[sep=1mm, wd=9cm]{boxcolor}

   326   \centering\smath{%

   327   \infer{P\,t}

   328   {\begin{array}{l}

   329   \forall x.\;P\,x\\[2mm]

   330   \forall t_1\,t_2.\;P\,t_1\wedge P\,t_2\Rightarrow P\,(t_1\;t_2)\\[2mm]

   331   \forall x\,t.\;P\,t\Rightarrow P\,(\lambda x.t)\\

   332   \end{array}

   333   }}

   334   \end{beamercolorbox}

   335   \end{center}

   336 

   337   \item It requires us in the lambda-case to show the property \smath{P} for

   338   all binders \smath{x}.\smallskip\\ 

   339 

   340   (This nearly always requires renamings and they can be 

   341   tricky to automate.)

   342   \end{itemize}

   343 

   344   \end{frame}}

   345   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   346 

   347 *}

   348 

   349 

   350 text_raw {*

   351 

   352   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   353   \mode<presentation>{

   354   \begin{frame}

   355   \frametitle{\Large Strong Induction Principles} 

   356 

   357   \begin{itemize}

   358   \item Therefore we introduced the following strong induction principle:

   359 

   360   \begin{center}

   361   \mbox{}\hspace{-2mm}\begin{beamercolorbox}[sep=1mm, wd=11.5cm]{boxcolor}

   362   \centering\smath{%

   363   \infer{\tikz[remember picture] \node[inner sep=1mm] (n1a) {\alert<4>{$P$}};%

   364          \tikz[remember picture] \node[inner sep=1mm] (n2a) {\alert<3>{$c$}};%

   365          \tikz[remember picture] \node[inner sep=1mm] (n3a) {\alert<2>{$t$}};}

   366   {\begin{array}{l}

   367   \forall x\,c.\;P\,c\;x\\[2mm]

   368   \forall t_1\,t_2\,c.\;(\forall d.\,P d\,t_1)\wedge (\forall d. P\,d\,t_2)

   369   \Rightarrow P\,c\;(t_1\,t_2)\\[2mm]

   370   \forall x\,t\,c.\;\alert<1>{x\fresh \alert<3>{c}} 

   371   \wedge (\forall d. P\,d\,t)\Rightarrow P\,c\;(\lambda x.t)

   372   \end{array}

   373   }}

   374   \end{beamercolorbox}

   375   \end{center}

   376   \end{itemize}

   377 

   378   \begin{textblock}{11}(0.9,10.9)

   379   \only<2>{

   380   \begin{tikzpicture}[remember picture]

   381   \draw (0,0) node[fill=cream, text width=10.5cm, thick, draw=red, rounded corners=1mm] (n3b)

   382   { The variable over which the induction proceeds:\\[2mm]

   383     \hspace{3mm}``\ldots By induction over the structure of \smath{M}\ldots''};

   384 

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

   386   \end{tikzpicture}}

   387 

   388   \only<3>{

   389   \begin{tikzpicture}[remember picture]

   390   \draw (0,0) node[fill=cream, text width=11cm, thick, draw=red, rounded corners=1mm] (n2b)

   391   {The {\bf context} of the induction; i.e.~what the binder should be fresh for

   392    $\quad\Rightarrow$ \smath{(x,y,N,L)}:\\[2mm]

   393    ``\ldots By the variable convention we can assume \mbox{\smath{z\not\equiv x,y}} 

   394      and \smath{z} not free in \smath{N}$\!$,\,\smath{L}\ldots''};

   395 

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

   397   \end{tikzpicture}}

   398 

   399   \only<4>{

   400   \begin{tikzpicture}[remember picture]

   401   \draw (0,0) node[fill=cream, text width=11cm, thick, draw=red, rounded corners=1mm] (n1b)

   402   {The property to be proved by induction:\\[-3mm]

   403   \begin{center}\small

   404   \begin{tabular}{l}

   405   \smath{\!\!\lambda

   406   (x,\!y,\!N\!,\!L).\,\lambda M.\;\,x\not=y\,\wedge\,x\fresh L\,\Rightarrow}\\[1mm]

   407   \hspace{8mm}

   408   \smath{M[x\!:=\!N][y\!:=\!L] = M[y\!:=\!L][x\!:=\!N[y\!:=\!L]]}  

   409   \end{tabular}

   410   \end{center}};

   411 

   412   \path[overlay, ->, ultra thick, red] (n1b) edge[out=90, in=-70] (n1a);

   413   \end{tikzpicture}}

   414   \end{textblock}

   415 

   416   \end{frame}}

   417   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   418 

   419 *}

   420 

   421 text_raw {*

   422   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   423   \mode<presentation>{

   424   \begin{frame}<1-4>

   425   \frametitle{\begin{tabular}{c}Binding Sets of Names\end{tabular}}

   426   \mbox{}\\[-3mm]

   427 

   428   \begin{itemize}

   429   \item binding sets of names has some interesting properties:\medskip

   430   

   431   \begin{center}

   432   \begin{tabular}{l}

   433   \textcolor{blue}{$\forall\{x, y\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{y, x\}.\, y \rightarrow x$}

   434   \bigskip\smallskip\\

   435 

   436   \onslide<2->{%

   437   \textcolor{blue}{$\forall\{x, y\}.\, x \rightarrow y \;\;\not\approx_\alpha\;\; \forall\{z\}.\, z \rightarrow z$}

   438   }\bigskip\smallskip\\

   439 

   440   \onslide<3->{%

   441   \textcolor{blue}{$\forall\{x\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{x, \alert{z}\}.\, x \rightarrow y$}

   442   }\medskip\\

   443   \onslide<3->{\hspace{4cm}\small provided $z$ is fresh for the type}

   444   \end{tabular}

   445   \end{center}

   446   \end{itemize}

   447   

   448   \begin{textblock}{8}(2,14.5)

   449   \footnotesize $^*$ $x$, $y$, $z$ are assumed to be distinct

   450   \end{textblock}

   451 

   452   \only<4>{

   453   \begin{textblock}{6}(2.5,4)

   454   \begin{tikzpicture}

   455   \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   456   {\normalsize\color{darkgray}

   457   \begin{minipage}{8cm}\raggedright

   458   For type-schemes the order of bound names does not matter, and

   459   $\alpha$-equivalence is preserved under \alert{vacuous} binders.

   460   \end{minipage}};

   461   \end{tikzpicture}

   462   \end{textblock}}

   463   \end{frame}}

   464   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   465 *}

   466 

   467 text_raw {*

   468   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   469   \mode<presentation>{

   470   \begin{frame}<1-3>

   471   \frametitle{\begin{tabular}{c}Other Binding Modes\end{tabular}}

   472   \mbox{}\\[-3mm]

   473 

   474   \begin{itemize}

   475   \item alpha-equivalence being preserved under vacuous binders is \underline{not} always

   476   wanted:\bigskip\bigskip\normalsize

   477   

   478   \textcolor{blue}{\begin{tabular}{@ {\hspace{-8mm}}l}

   479   $\text{let}\;x = 3\;\text{and}\;y = 2\;\text{in}\;x - y\;\text{end}$\medskip\\

   480   \onslide<2->{$\;\;\;\only<2>{\approx_\alpha}\only<3>{\alert{\not\approx_\alpha}}

   481    \text{let}\;y = 2\;\text{and}\;x = 3\only<3->{\alert{\;\text{and}

   482     \;z = \text{loop}}}\;\text{in}\;x - y\;\text{end}$}

   483   \end{tabular}}

   484   

   485 

   486   \end{itemize}

   487 

   488   \end{frame}}

   489   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   490 *}

   491 

   492 text_raw {*

   493   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   494   \mode<presentation>{

   495   \begin{frame}<1>

   496   \frametitle{\begin{tabular}{c}\Large{}Even Another Binding Mode\end{tabular}}

   497   \mbox{}\\[-3mm]

   498 

   499   \begin{itemize}

   500   \item sometimes one wants to abstract more than one name, but the order \underline{does} matter\bigskip

   501   

   502   \begin{center}

   503   \textcolor{blue}{\begin{tabular}{@ {\hspace{-8mm}}l}

   504   $\text{let}\;(x, y) = (3, 2)\;\text{in}\;x - y\;\text{end}$\medskip\\

   505   $\;\;\;\not\approx_\alpha

   506    \text{let}\;(y, x) = (3, 2)\;\text{in}\;x - y\;\text{end}$

   507   \end{tabular}}

   508   \end{center}

   509   

   510 

   511   \end{itemize}

   512 

   513   \end{frame}}

   514   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   515 *}

   516 

   517 

   518 text_raw {*

   519   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   520   \mode<presentation>{

   521   \begin{frame}<2-3>

   522   \frametitle{\begin{tabular}{c}Specification of Binding\end{tabular}}

   523   \mbox{}\\[-6mm]

   524 

   525   \mbox{}\hspace{10mm}

   526   \begin{tabular}{ll}

   527   \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\

   528   \hspace{5mm}\phantom{$|$} Var name\\

   529   \hspace{5mm}$|$ App trm trm\\

   530   \hspace{5mm}$|$ Lam \only<2->{x::}name \only<2->{t::}trm

   531   & \onslide<2->{\isacommand{bind} x \isacommand{in} t}\\

   532   \hspace{5mm}$|$ Let \only<2->{as::}assns \only<2->{t::}trm

   533   & \onslide<2->{\isacommand{bind} bn(as) \isacommand{in} t}\\

   534   \multicolumn{2}{l}{\isacommand{and} assns $=$}\\

   535   \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\

   536   \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assns}\\

   537   \multicolumn{2}{l}{\onslide<3->{\isacommand{binder} bn \isacommand{where}}}\\

   538   \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}}\\

   539   \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}}\\

   540   \end{tabular}

   541 

   542 

   543 

   544   \end{frame}}

   545   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   546 *}

   547 

   548 

   549 text_raw {*

   550 

   551   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   552   \mode<presentation>{

   553   \begin{frame}

   554   \frametitle{So Far So Good}

   555 

   556   \begin{itemize}

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

   558   \end{itemize}

   559 

   560   \begin{center}

   561   \begin{block}{}

   562   \color{gray}

   563   \small%

   564   {\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[1mm] 

   565   If $M_1,\ldots,M_n$ occur in a certain mathematical context

   566   (e.g. definition, proof), then in these terms all bound variables 

   567   are chosen to be different from the free variables.\\[2mm]

   568   

   569   \footnotesize\hfill Barendregt in ``The Lambda-Calculus: Its Syntax and Semantics''

   570   \end{block}

   571   \end{center}

   572 

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

   574 

   575   \begin{columns}

   576   \begin{column}[t]{4.7cm}

   577   Inductive Definitions:\\

   578   \begin{center}

   579   \smath{\infer{\text{concl}}{\text{prem}_1 \ldots \text{prem}_n\;\text{scs}}}

   580   \end{center}

   581   \end{column}

   582   \begin{column}[t]{7cm}

   583   Rule Inductions:\\[2mm]

   584   \begin{tabular}{l@ {\hspace{2mm}}p{5.5cm}}

   585   1.) & Assume the property for\\ & the premises. Assume \\ & the side-conditions.\\[1mm]

   586   2.) & Show the property for\\ & the conclusion.\\

   587   \end{tabular}

   588   \end{column}

   589   \end{columns}

   590 

   591   \end{frame}}

   592   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   593 

   594 *}

   595 

   596 text_raw {*

   597 

   598   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   599   \mode<presentation>{

   600   \setbeamerfont{itemize/enumerate subbody}{size=\normalsize}

   601   \begin{frame}[sqeeze]

   602   \frametitle{Faulty Reasoning} 

   603 

   604   %\mbox{}

   605 

   606   \begin{itemize}

   607   \item Consider the two-place relation \smath{\text{foo}}:\medskip

   608   \begin{center}

   609   \begin{tabular}{ccc}

   610   \raisebox{2.5mm}{\colorbox{cream}{%

   611   \smath{\;\infer{x\mapsto x}{}}}}\hspace{2mm}

   612   &

   613   \raisebox{2mm}{\colorbox{cream}{%

   614   \smath{\infer{t_1\;t_2\mapsto t_1\;t_2}{}}}}\hspace{2mm}

   615   &

   616   \colorbox{cream}{%

   617   \smath{\infer{\lambda x.t\mapsto t'}{t\mapsto t'}}}\\[5mm]

   618   \end{tabular}

   619   \end{center}

   620 

   621   \pause

   622 

   623   \item The lemma we going to prove:\smallskip

   624   \begin{center}

   625   Let \smath{t\mapsto t'}. If \smath{y\fresh t} then \smath{y\fresh t'}.

   626   \end{center}\bigskip

   627 

   628   \only<3>{

   629   \item Cases 1 and 2 are trivial:\medskip

   630   \begin{itemize}

   631   \item If \smath{y\fresh x} then \smath{y\fresh x}.

   632   \item If \smath{y\fresh t_1\,t_2} then \smath{y\fresh t_1\,t_2}.

   633   \end{itemize}

   634   }

   635 

   636   \only<4->{

   637   \item Case 3:

   638   \begin{itemize}

   639   \item We know \tikz[remember picture,baseline=(ta.base)] \node (ta) {\smath{y\fresh \lambda x.t}.}; 

   640   We have to show \smath{y\fresh t'}.$\!\!\!\!$ 

   641   \item The IH says: if \smath{y\fresh t} then \smath{y\fresh t'}.

   642   \item<7,8> So we have \smath{y\fresh t}. Hence \smath{y\fresh t'} by IH. Done!

   643   \end{itemize}

   644   }

   645   \end{itemize}

   646   

   647   \begin{textblock}{11.3}(0.7,0.6)

   648   \only<5-7>{

   649   \begin{tikzpicture}

   650   \draw (0,0) node[fill=cream, text width=11.2cm, thick, draw=red, rounded corners=1mm] (nn)

   651   {{\bf Variable Convention:}\\[2mm] 

   652   \small

   653    If $M_1,\ldots,M_n$ occur in a certain mathematical context

   654    (e.g. definition, proof), then in these terms all bound variables 

   655    are chosen to be different from the free variables.\smallskip

   656 

   657   \normalsize

   658    {\bf In our case:}\\[2mm]

   659    The free variables are \smath{y} and \smath{t'}; the bound one is 

   660    \smath{x}.\medskip

   661           

   662    By the variable convention we conclude that \smath{x\not= y}.

   663   };

   664   \end{tikzpicture}}

   665   \end{textblock}

   666 

   667   \begin{textblock}{9.2}(3.6,9)

   668   \only<6,7>{

   669   \begin{tikzpicture}[remember picture]

   670   \draw (0,0) node[fill=cream, text width=9cm, thick, draw=red, rounded corners=1mm] (tb)

   671   {\small\smath{y\!\not\in\! \text{fv}(\lambda x.t) \Longleftrightarrow

   672           y\!\not\in\! \text{fv}(t)\!-\!\{x\}

   673           \stackrel{x\not=y}{\Longleftrightarrow}

   674           y\!\not\in\! \text{fv}(t)}};

   675 

   676   \path[overlay, ->, ultra thick, red] (tb) edge[out=-120, in=75] (ta);

   677   \end{tikzpicture}}

   678   \end{textblock}

   679 

   680   \end{frame}}

   681   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   682 

   683 *}

   684 

   685 

   686 text_raw {*

   687 

   688   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   689   \mode<presentation>{

   690   \begin{frame}

   691   \frametitle{Conclusions} 

   692 

   693   \begin{itemize}

   694   \item The user does not see anything of the ``raw'' level.

   695   \item The Nominal Isabelle automatically derives the strong structural

   696   induction principle for \underline{\bf all} nominal datatypes (not just the 

   697   lambda-calculus)

   698 

   699   \item They are easy to use: you just have to think carefully what the variable

   700   convention should be.

   701 

   702   \item We can explore the \colorbox{black}{\textcolor{white}{dark}} corners 

   703   of the variable convention: when and where it can be used safely.

   704   

   705   \item<2> \alert{\bf Main Point:} Actually these proofs using the

   706   variable convention are all trivial / obvious / routine\ldots {\bf provided} 

   707   you use Nominal Isabelle. ;o)

   708  

   709   \end{itemize}

   710 

   711 

   712   \end{frame}}

   713   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   714 

   715 *}

   716 

   717 text_raw {*

   718   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   719   \mode<presentation>{

   720   \begin{frame}<1>[b]

   721   \frametitle{

   722   \begin{tabular}{c}

   723   \mbox{}\\[13mm]

   724   \alert{\LARGE Thank you very much!}\\

   725   \alert{\Large Questions?}

   726   \end{tabular}}

   727 

   728 

   729   \end{frame}}

   730   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   731 *}

   732 

   733 (*<*)

   734 end

   735 (*>*)