1 (*<*)

     2 theory Slides9

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

     4 begin

     5 

     6 notation (latex output)

     7   set ("_") and

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

     9 

    10 (*>*)

    11 

    12 

    13 text_raw {*

    14   %% shallow, deep, and recursive binders

    15   %%

    16   %%\renewcommand{\slidecaption}{Cambridge, 8.~June 2010}

    17   %%\renewcommand{\slidecaption}{Uppsala, 3.~March 2011}

    18   \renewcommand{\slidecaption}{Leicester, 23.~November 2011}

    19   \newcommand{\soutt}[1]{\tikz[baseline=(X.base), inner sep=-0.1pt, outer sep=0pt]

    20   \node [cross out,red, ultra thick, draw] (X) {\textcolor{black}{#1}};}

    21   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    22   \mode<presentation>{

    23   \begin{frame}<1>[t]

    24   \frametitle{%

    25   \begin{tabular}{@ {\hspace{-3mm}}c@ {}}

    26   \\

    27   \LARGE General Binding Structures\\[-1mm] 

    28   \LARGE in Nominal Isabelle 2\\

    29   \end{tabular}}

    30   \begin{center}

    31   Christian Urban

    32   \end{center}

    33   \begin{center}

    34   joint work with {\bf Cezary Kaliszyk}\\[0mm] 

    35   \end{center}

    36   \end{frame}}

    37   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    38 

    39 *}

    40 

    41 text_raw {*

    42   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    43   \mode<presentation>{

    44   \begin{frame}<1>

    45   \frametitle{\begin{tabular}{c}Binding in Old Nominal\end{tabular}}

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

    47 

    48   \begin{itemize}

    49   \item the old Nominal Isabelle provided a reasoning infrastructure for single binders\medskip

    50   

    51   \begin{center}

    52   Lam [a].(Var a)

    53   \end{center}\bigskip

    54 

    55   \item<2-> but representing 

    56 

    57   \begin{center}

    58   $\forall\{a_1,\ldots,a_n\}.\; T$ 

    59   \end{center}\medskip

    60 

    61   with single binders and reasoning about it is a \alert{\bf major} pain; 

    62   take my word for it!

    63   \end{itemize}

    64 

    65   \only<1>{

    66   \begin{textblock}{6}(1.5,11)

    67   \small

    68   for example\\

    69   \begin{tabular}{l@ {\hspace{2mm}}l}

    70    & a $\fresh$ Lam [a]. t\\

    71    & Lam [a]. (Var a) \alert{$=$} Lam [b]. (Var b)\\

    72    & Barendregt-style reasoning about bound variables\\

    73    & (variable convention can lead to faulty reasoning)

    74   \end{tabular}

    75   \end{textblock}}

    76   

    77   \end{frame}}

    78   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    79 *}

    80 

    81 text_raw {*

    82   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    83   \mode<presentation>{

    84   \begin{frame}[c]

    85   \frametitle{}

    86 

    87   \begin{tabular}{c@ {\hspace{2mm}}c}

    88   \\[6mm]

    89   \begin{tabular}{c}

    90   \includegraphics[scale=0.11]{harper.jpg}\\[-2mm]

    91   {\footnotesize Bob Harper}\\[-2.5mm]

    92   {\footnotesize (CMU)}

    93   \end{tabular}

    94   \begin{tabular}{c}

    95   \includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm]

    96   {\footnotesize Frank Pfenning}\\[-2.5mm]

    97   {\footnotesize (CMU)}

    98   \end{tabular} &

    99 

   100   \begin{tabular}{p{6cm}}

   101   \raggedright

   102   \color{gray}{published a proof in\\ {\bf ACM Transactions on Computational Logic}, 2005,

   103   $\sim$31pp}

   104   \end{tabular}\\

   105 

   106   \pause

   107   \\[0mm]

   108   

   109   \begin{tabular}{c}

   110   \includegraphics[scale=0.36]{appel.jpg}\\[-2mm] 

   111   {\footnotesize Andrew Appel}\\[-2.5mm]

   112   {\footnotesize (Princeton)}

   113   \end{tabular} &

   114 

   115   \begin{tabular}{p{6cm}}

   116   \raggedright

   117   \color{gray}{relied on their proof in a\\ {\bf security} critical application}

   118   \end{tabular}

   119   \end{tabular}\medskip\pause

   120 

   121   \small

   122   \begin{minipage}{1.0\textwidth}

   123   (I also found an {\bf error} in my Ph.D.-thesis about cut-elimination

   124   examined by Henk Barendregt and Andy Pitts.)

   125   \end{minipage}

   126 

   127   \end{frame}}

   128   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   129 *}

   130 

   131 text_raw {*

   132   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   133   \mode<presentation>{

   134   \begin{frame}[c]

   135   \frametitle{\begin{tabular}{c}Binding in Old Nominal\end{tabular}}

   136 

   137   \begin{itemize}

   138   \item<1-> but representing 

   139 

   140   \begin{center}

   141   $\forall\{a_1,\ldots,a_n\}.\; T$ 

   142   \end{center}\medskip

   143 

   144   with single binders and reasoning about it was a \alert{\bf major} pain; 

   145   take my word for it!

   146   \end{itemize}

   147 

   148   

   149   \end{frame}}

   150   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   151 *}

   152 

   153 text_raw {*

   154   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   155   \mode<presentation>{

   156   \begin{frame}<1-6>

   157   \frametitle{New Types in HOL}

   158 

   159    \begin{center}

   160   \begin{tikzpicture}[scale=1.5]

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

   162   

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

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

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

   166   

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

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

   169 

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

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

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

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

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

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

   176   

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

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

   179 

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

   181   \end{tikzpicture}

   182   \end{center}

   183   

   184   \begin{center}

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

   186   \end{center}

   187 

   188   \end{frame}}

   189   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   190 *}

   191 

   192 

   193 

   194 text_raw {*

   195   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   196   \mode<presentation>{

   197   \begin{frame}<1-4>

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

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

   200 

   201   \begin{itemize}

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

   203   

   204   \begin{center}

   205   \begin{tabular}{l}

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

   207   \bigskip\smallskip\\

   208 

   209   \onslide<2->{%

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

   211   }\bigskip\smallskip\\

   212 

   213   \onslide<3->{%

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

   215   }\medskip\\

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

   217   \end{tabular}

   218   \end{center}

   219   \end{itemize}

   220   

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

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

   223   \end{textblock}

   224 

   225   \only<4>{

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

   227   \begin{tikzpicture}

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

   229   {\normalsize\color{darkgray}

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

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

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

   233   \end{minipage}};

   234   \end{tikzpicture}

   235   \end{textblock}}

   236   \end{frame}}

   237   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   238 *}

   239 

   240 text_raw {*

   241   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   242   \mode<presentation>{

   243   \begin{frame}<1-3>

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

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

   246 

   247   \begin{itemize}

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

   249   wanted:\bigskip\bigskip\normalsize

   250   

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

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

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

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

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

   256   \end{tabular}}

   257   

   258 

   259   \end{itemize}

   260 

   261   \end{frame}}

   262   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   263 *}

   264 

   265 text_raw {*

   266   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   267   \mode<presentation>{

   268   \begin{frame}<1>

   269   \frametitle{\begin{tabular}{c}\LARGE{}Even Another Binding Mode\end{tabular}}

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

   271 

   272   \begin{itemize}

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

   274   

   275   \begin{center}

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

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

   278   $\;\;\;\not\approx_\alpha

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

   280   \end{tabular}}

   281   \end{center}

   282   

   283 

   284   \end{itemize}

   285 

   286   \end{frame}}

   287   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   288 *}

   289 

   290 text_raw {*

   291   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   292   \mode<presentation>{

   293   \begin{frame}<1-2>

   294   \frametitle{\begin{tabular}{c}\LARGE{}Three Binding Modes\end{tabular}}

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

   296 

   297   \begin{itemize}

   298   \item the order does not matter and alpha-equivelence is preserved under

   299   vacuous binders \textcolor{gray}{(restriction)}\medskip

   300   

   301   \item the order does not matter, but the cardinality of the binders 

   302   must be the same \textcolor{gray}{(abstraction)}\medskip

   303 

   304   \item the order does matter \textcolor{gray}{(iterated single binders)}

   305   \end{itemize}

   306 

   307   \onslide<2->{

   308   \begin{center}

   309   \isacommand{bind (set+)}\hspace{6mm}

   310   \isacommand{bind (set)}\hspace{6mm}

   311   \isacommand{bind}

   312   \end{center}}

   313 

   314   \end{frame}}

   315   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   316 *}

   317 

   318 text_raw {*

   319   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   320   \mode<presentation>{

   321   \begin{frame}<1-3>

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

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

   324 

   325   \mbox{}\hspace{10mm}

   326   \begin{tabular}{ll}

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

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

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

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

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

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

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

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

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

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

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

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

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

   340   \end{tabular}

   341 

   342 

   343 

   344   \end{frame}}

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

   346 *}

   347 

   348 

   349 text_raw {*

   350   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   351   \mode<presentation>{

   352   \begin{frame}<1-2,4-8>

   353   \frametitle{\begin{tabular}{c}Alpha-Equivalence\end{tabular}}

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

   355 

   356   \begin{itemize}

   357   \item lets first look at pairs\bigskip\medskip

   358 

   359   \textcolor{blue}{\begin{tabular}{@ {\hspace{1cm}}l}

   360   $(as, x) \onslide<2->{\approx\!}\makebox[5mm][l]{\only<2-6>{${}_{\text{set}}$}%

   361            \only<7>{${}_{\text{\alert{list}}}$}%

   362            \only<8>{${}_{\text{\alert{set+}}}$}}%

   363            \,\onslide<2->{(bs,y)}$

   364   \end{tabular}}\bigskip

   365   \end{itemize}

   366 

   367   \only<1>{

   368   \begin{textblock}{8}(3,8.5)

   369   \begin{tabular}{l@ {\hspace{2mm}}p{8cm}}

   370    & \textcolor{blue}{$as$} is a set of names\ldots the binders\\

   371    & \textcolor{blue}{$x$} is the body (might be a tuple)\\

   372    & \textcolor{blue}{$\approx_{\text{set}}$} is where the cardinality 

   373   of the binders has to be the same\\

   374   \end{tabular}

   375   \end{textblock}}

   376 

   377   \only<4->{

   378   \begin{textblock}{12}(5,8)

   379   \textcolor{blue}{

   380   \begin{tabular}{ll@ {\hspace{1mm}}l}

   381   $\dn$ & \onslide<5->{$\exists \pi.\,$} & $\text{fv}(x) - as = \text{fv}(y) - bs$\\[1mm]

   382         & \onslide<5->{$\;\;\;\wedge$} & \onslide<5->{$\text{fv}(x) - as \fresh^* \pi$}\\[1mm]

   383         & \onslide<5->{$\;\;\;\wedge$} & \onslide<5->{$(\pi \act x) = y$}\\[1mm]

   384         & \only<6-7>{$\;\;\;\wedge$}\only<8>{\textcolor{gray}{\xout{$\;\;\;\wedge$}}} & 

   385           \only<6-7>{$\pi \act as = bs$}\only<8>{\textcolor{gray}{\xout{$\pi \act as = bs$}}}\\

   386   \end{tabular}}

   387   \end{textblock}}

   388   

   389   \only<7>{

   390   \begin{textblock}{7}(3,13.8)

   391   \footnotesize $^*$ $as$ and $bs$ are \alert{lists} of names 

   392   \end{textblock}}

   393   \end{frame}}

   394   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   395 *}

   396 

   397 text_raw {*

   398   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   399   \mode<presentation>{

   400   \begin{frame}<1-3>

   401   \frametitle{\begin{tabular}{c}Examples\end{tabular}}

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

   403 

   404   \begin{itemize}

   405   \item lets look at type-schemes:\medskip\medskip

   406 

   407   \begin{center}

   408   \textcolor{blue}{$(as, x) \approx\!\makebox[5mm][l]{${}_{\text{set}}$} (bs, y)$}

   409   \end{center}\medskip

   410 

   411   \onslide<2->{

   412   \begin{center}

   413   \textcolor{blue}{

   414   \begin{tabular}{l}

   415   $\text{fv}(x) = \{x\}$\\[1mm]

   416   $\text{fv}(T_1 \rightarrow T_2) = \text{fv}(T_1) \cup \text{fv}(T_2)$\\

   417   \end{tabular}}

   418   \end{center}}

   419   \end{itemize}

   420 

   421   

   422   \only<3->{

   423   \begin{textblock}{4}(0.3,12)

   424   \begin{tikzpicture}

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

   426   {\tiny\color{darkgray}

   427   \begin{minipage}{3.4cm}\raggedright

   428   \begin{tabular}{r@ {\hspace{1mm}}l}

   429   \multicolumn{2}{@ {}l}{set+:}\\

   430   $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\

   431   $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\

   432   $\wedge$ & $\pi \cdot x = y$\\

   433   \\

   434   \end{tabular}

   435   \end{minipage}};

   436   \end{tikzpicture}

   437   \end{textblock}}

   438   \only<3->{

   439   \begin{textblock}{4}(5.2,12)

   440   \begin{tikzpicture}

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

   442   {\tiny\color{darkgray}

   443   \begin{minipage}{3.4cm}\raggedright

   444   \begin{tabular}{r@ {\hspace{1mm}}l}

   445   \multicolumn{2}{@ {}l}{set:}\\

   446   $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\

   447   $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\

   448   $\wedge$ & $\pi \cdot x = y$\\

   449   $\wedge$ & $\pi \cdot as = bs$\\

   450   \end{tabular}

   451   \end{minipage}};

   452   \end{tikzpicture}

   453   \end{textblock}}

   454   \only<3->{

   455   \begin{textblock}{4}(10.2,12)

   456   \begin{tikzpicture}

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

   458   {\tiny\color{darkgray}

   459   \begin{minipage}{3.4cm}\raggedright

   460   \begin{tabular}{r@ {\hspace{1mm}}l}

   461   \multicolumn{2}{@ {}l}{list:}\\

   462   $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\

   463   $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\

   464   $\wedge$ & $\pi \cdot x = y$\\

   465   $\wedge$ & $\pi \cdot as = bs$\\

   466   \end{tabular}

   467   \end{minipage}};

   468   \end{tikzpicture}

   469   \end{textblock}}

   470 

   471   \end{frame}}

   472   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   473 *}

   474 

   475 text_raw {*

   476   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   477   \mode<presentation>{

   478   \begin{frame}<1-2>

   479   \frametitle{\begin{tabular}{c}Examples\end{tabular}}

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

   481 

   482   \begin{center}

   483   \textcolor{blue}{

   484   \only<1>{$(\{x, y\}, x \rightarrow y) \approx_? (\{x, y\}, y \rightarrow x)$}

   485   \only<2>{$([x, y], x \rightarrow y) \approx_? ([x, y], y \rightarrow x)$}}

   486   \end{center}

   487 

   488   \begin{itemize}

   489   \item \textcolor{blue}{$\approx_{\text{set+}}$, $\approx_{\text{set}}$% 

   490   \only<2>{, \alert{$\not\approx_{\text{list}}$}}}

   491   \end{itemize}

   492 

   493   

   494   \only<1->{

   495   \begin{textblock}{4}(0.3,12)

   496   \begin{tikzpicture}

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

   498   {\tiny\color{darkgray}

   499   \begin{minipage}{3.4cm}\raggedright

   500   \begin{tabular}{r@ {\hspace{1mm}}l}

   501   \multicolumn{2}{@ {}l}{set+:}\\

   502   $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\

   503   $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\

   504   $\wedge$ & $\pi \cdot x = y$\\

   505   \\

   506   \end{tabular}

   507   \end{minipage}};

   508   \end{tikzpicture}

   509   \end{textblock}}

   510   \only<1->{

   511   \begin{textblock}{4}(5.2,12)

   512   \begin{tikzpicture}

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

   514   {\tiny\color{darkgray}

   515   \begin{minipage}{3.4cm}\raggedright

   516   \begin{tabular}{r@ {\hspace{1mm}}l}

   517   \multicolumn{2}{@ {}l}{set:}\\

   518   $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\

   519   $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\

   520   $\wedge$ & $\pi \cdot x = y$\\

   521   $\wedge$ & $\pi \cdot as = bs$\\

   522   \end{tabular}

   523   \end{minipage}};

   524   \end{tikzpicture}

   525   \end{textblock}}

   526   \only<1->{

   527   \begin{textblock}{4}(10.2,12)

   528   \begin{tikzpicture}

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

   530   {\tiny\color{darkgray}

   531   \begin{minipage}{3.4cm}\raggedright

   532   \begin{tabular}{r@ {\hspace{1mm}}l}

   533   \multicolumn{2}{@ {}l}{list:}\\

   534   $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\

   535   $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\

   536   $\wedge$ & $\pi \cdot x = y$\\

   537   $\wedge$ & $\pi \cdot as = bs$\\

   538   \end{tabular}

   539   \end{minipage}};

   540   \end{tikzpicture}

   541   \end{textblock}}

   542 

   543   \end{frame}}

   544   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   545 *}

   546 

   547 text_raw {*

   548   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   549   \mode<presentation>{

   550   \begin{frame}<1-2>

   551   \frametitle{\begin{tabular}{c}Examples\end{tabular}}

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

   553 

   554   \begin{center}

   555   \textcolor{blue}{\only<1>{$(\{x\}, x) \approx_? (\{x, y\}, x)$}}

   556   \end{center}

   557 

   558   \begin{itemize}

   559   \item \textcolor{blue}{$\approx_{\text{set+}}$, $\not\approx_{\text{set}}$,

   560         $\not\approx_{\text{list}}$}

   561   \end{itemize}

   562 

   563   

   564   \only<1->{

   565   \begin{textblock}{4}(0.3,12)

   566   \begin{tikzpicture}

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

   568   {\tiny\color{darkgray}

   569   \begin{minipage}{3.4cm}\raggedright

   570   \begin{tabular}{r@ {\hspace{1mm}}l}

   571   \multicolumn{2}{@ {}l}{set+:}\\

   572   $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\

   573   $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\

   574   $\wedge$ & $\pi \cdot x = y$\\

   575   \\

   576   \end{tabular}

   577   \end{minipage}};

   578   \end{tikzpicture}

   579   \end{textblock}}

   580   \only<1->{

   581   \begin{textblock}{4}(5.2,12)

   582   \begin{tikzpicture}

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

   584   {\tiny\color{darkgray}

   585   \begin{minipage}{3.4cm}\raggedright

   586   \begin{tabular}{r@ {\hspace{1mm}}l}

   587   \multicolumn{2}{@ {}l}{set:}\\

   588   $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\

   589   $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\

   590   $\wedge$ & $\pi \cdot x = y$\\

   591   $\wedge$ & $\pi \cdot as = bs$\\

   592   \end{tabular}

   593   \end{minipage}};

   594   \end{tikzpicture}

   595   \end{textblock}}

   596   \only<1->{

   597   \begin{textblock}{4}(10.2,12)

   598   \begin{tikzpicture}

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

   600   {\tiny\color{darkgray}

   601   \begin{minipage}{3.4cm}\raggedright

   602   \begin{tabular}{r@ {\hspace{1mm}}l}

   603   \multicolumn{2}{@ {}l}{list:}\\

   604   $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\

   605   $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\

   606   $\wedge$ & $\pi \cdot x = y$\\

   607   $\wedge$ & $\pi \cdot as = bs$\\

   608   \end{tabular}

   609   \end{minipage}};

   610   \end{tikzpicture}

   611   \end{textblock}}

   612 

   613   \only<2>{

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

   615   \begin{tikzpicture}

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

   617   {\normalsize

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

   619   \begin{itemize}

   620   \item \color{darkgray}$\alpha$-equivalences coincide when a single name is

   621   abstracted

   622   \item \color{darkgray}in that case they are equivalent to ``old-fashioned'' definitions of $\alpha$ 

   623   \end{itemize}

   624   \end{minipage}};

   625   \end{tikzpicture}

   626   \end{textblock}}

   627 

   628   \end{frame}}

   629   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   630 *}

   631 

   632 text_raw {*

   633   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   634   \mode<presentation>{

   635   \begin{frame}<1->

   636   \frametitle{\begin{tabular}{c}Our Specifications\end{tabular}}

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

   638 

   639   \mbox{}\hspace{10mm}

   640   \begin{tabular}{ll}

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

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

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

   644   \hspace{5mm}$|$ Lam x::name t::trm

   645   & \isacommand{bind} x \isacommand{in} t\\

   646   \hspace{5mm}$|$ Let as::assns t::trm

   647   & \isacommand{bind} bn(as) \isacommand{in} t\\

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

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

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

   651   \multicolumn{2}{l}{\isacommand{binder} bn \isacommand{where}}\\

   652   \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\

   653   \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\

   654   \end{tabular}

   655 

   656   \end{frame}}

   657   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   658 *}

   659 

   660 

   661 text_raw {*

   662   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   663   \mode<presentation>{

   664   \begin{frame}<1->[t]

   665   \frametitle{\begin{tabular}{c}Binder Clauses\end{tabular}}

   666 

   667   \begin{itemize}

   668   \item We need  to have a `clear scope' for a bound variable, and bound

   669   variables should not be free and bound at the same time.\bigskip

   670   \end{itemize}

   671 

   672   \begin{center}

   673   \only<1>{

   674   \begin{tabular}{@ {\hspace{-5mm}}l}

   675   \alert{\bf shallow binders}\\ 

   676   \hspace{4mm}Lam x::name t::trm\hspace{4mm} \isacommand{bind} x \isacommand{in} t\\

   677   \hspace{4mm}All xs::name set T::ty\hspace{4mm} \isacommand{bind} xs \isacommand{in} T\\

   678   \hspace{4mm}Foo x::name t$_1$::trm t$_2$::trm\hspace{4mm} 

   679      \isacommand{bind} x \isacommand{in} t$_1$, \isacommand{bind} x \isacommand{in} t$_2$\\

   680   \hspace{4mm}Bar x::name t$_1$::trm t$_2$::trm\hspace{4mm} 

   681      \isacommand{bind} x \isacommand{in} t$_1$ t$_2$\\

   682   \end{tabular}}

   683   \only<2>{

   684   \begin{tabular}{@ {\hspace{-5mm}}l}

   685   \alert{\bf deep binders} \\

   686   \hspace{4mm}Let as::assns t::trm\hspace{4mm} \isacommand{bind} bn(as) \isacommand{in} t\\

   687   \hspace{4mm}Foo as::assns t$_1$::trm t$_2$::trm\\

   688   \hspace{20mm}\isacommand{bind} bn(as) \isacommand{in} t$_1$, \isacommand{bind} bn(as) \isacommand{in} t$_2$\\[4mm]

   689   \makebox[0mm][l]{\alert{$\times$}}\hspace{4mm}Bar as::assns t$_1$::trm t$_2$::trm\\

   690   \hspace{20mm}\isacommand{bind} bn$_1$(as) \isacommand{in} t$_1$, \isacommand{bind} bn$_2$(as) \isacommand{in} t$_2$\\

   691   \end{tabular}}

   692   \only<3>{

   693   \begin{tabular}{@ {\hspace{-5mm}}l}

   694   {\bf deep \alert{recursive} binders} \\

   695   \hspace{4mm}Let\_rec as::assns t::trm\hspace{4mm} \isacommand{bind} bn(as) \isacommand{in} t as\\[4mm]

   696 

   697   \makebox[0mm][l]{\alert{$\times$}}\hspace{4mm}Foo\_rec as::assns t$_1$::trm t$_2$::trm\hspace{4mm}\\ 

   698   \hspace{20mm}\isacommand{bind} bn(as) \isacommand{in} t$_1$ as, \isacommand{bind} bn(as) \isacommand{in} t$_2$\\

   699 

   700   \end{tabular}}

   701   \end{center}

   702   

   703   \end{frame}}

   704   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   705 *}

   706 

   707 text_raw {*

   708   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   709   \mode<presentation>{

   710   \begin{frame}<1-5>

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

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

   713 

   714     \begin{center}

   715   \begin{tikzpicture}[scale=1.5]

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

   717   

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

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

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

   721   

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

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

   724 

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

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

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

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

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

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

   731   

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

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

   734 

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

   736   \end{tikzpicture}

   737   \end{center}

   738   

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

   740   \begin{itemize}

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

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

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

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

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

   746   \begin{center}

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

   748   \end{center}

   749   \end{itemize}

   750   \end{textblock}

   751 

   752 

   753   \end{frame}}

   754   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   755 *}

   756 

   757 

   758 text_raw {*

   759   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   760   \mode<presentation>{

   761   \begin{frame}<1->

   762   \frametitle{\begin{tabular}{c}Part I: Conclusion\end{tabular}}

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

   764 

   765   \begin{itemize}

   766   \item the user does not see anything of the raw level\medskip

   767   \only<1>{\begin{center}

   768   Lam a (Var a) \alert{$=$} Lam b (Var b)

   769   \end{center}\bigskip}

   770 

   771   \item<2-> \textcolor{blue}{http://isabelle.in.tum.de/nominal/}

   772   \end{itemize}

   773 

   774   

   775   \end{frame}}

   776   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   777 *}

   778 

   779 text_raw {*

   780   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   781   \mode<presentation>{

   782   \begin{frame}<1->

   783   \frametitle{\begin{tabular}{c}Part II: $\alpha\beta$-Equal Terms\end{tabular}}

   784 

   785   \begin{itemize}

   786   \item we have implemented a quotient package for Isabelle;

   787   \item can now introduce the type of $\alpha\beta$-equal terms (starting

   788   from $\alpha$-equal terms).

   789   \item on paper this looks easy\pause\bigskip

   790   \end{itemize}

   791 

   792   \begin{center}

   793   \begin{tabular}{lll}

   794   \smath{x \approx_{\alpha\beta} y} & \smath{\;\not\Rightarrow\;} & 

   795   \smath{\text{supp}(x) = \text{supp}(y)}\\

   796   & \smath{\;\not\Rightarrow\;} & 

   797   \smath{\text{size}(x) = \text{size}(y)}\\

   798   \end{tabular}

   799   \end{center}\pause

   800 

   801   \small

   802   \begin{center}

   803   Andy: \smath{\;\;\text{supp}\mbox{\isasymlbrakk}x\mbox{\isasymrbrakk}_{\approx_{\alpha\beta}} = 

   804   {\text{\large$\bigcap$}} \{ \text{supp}(y) \;|\; y \approx_{\alpha\beta} x\}}

   805   \end{center}

   806 

   807   \end{frame}}

   808   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   809 *}

   810 

   811 text_raw {*

   812   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   813   \mode<presentation>{

   814   \begin{frame}[c]

   815   \frametitle{}

   816 

   817   \begin{center}

   818   \begin{tabular}{rcl}

   819   \smath{x\;[y := s]} &           \smath{\dn} & \smath{\text{if}\;x=y\;\text{then}\;s\;\text{else}\;x}\bigskip\\

   820   \smath{t_1 t_2\;[y := s]} &     \smath{\dn} & \smath{t_1[y := s]\;t_2[y := s]}\bigskip\\

   821   \smath{\lambda x.t\;[y := s]} & \smath{\dn} & \smath{\lambda x.\; t[y := s]}\\

   822   \multicolumn{3}{r}{provided \smath{x \fresh (y, s)}}

   823   \end{tabular}

   824   \end{center}

   825 

   826   \end{frame}}

   827   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   828 *}

   829 

   830 text_raw {*

   831   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   832   \mode<presentation>{

   833   \begin{frame}[t]

   834   \frametitle{\begin{tabular}{c}Part III: Regular Languages\\[-8mm]\end{tabular}}

   835 

   836   \begin{center}

   837   \huge\bf\textcolor{gray}{in Theorem Provers}\\

   838   \footnotesize\textcolor{gray}{e.g.~Isabelle, Coq, HOL4, \ldots}

   839   \end{center}

   840 

   841   \begin{itemize}

   842   \item automata @{text "\<Rightarrow>"} graphs, matrices, functions

   843   \item<2-> combining automata/graphs

   844 

   845   \onslide<2->{

   846   \begin{center}

   847   \begin{tabular}{ccc}

   848   \begin{tikzpicture}[scale=1]

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

   850   

   851   \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);

   852   \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);

   853 

   854   \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   855   \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   856   

   857   \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   858   \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   859 

   860   \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   861   \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   862   \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   863 

   864   \draw (-0.6,0.0) node {\small$A_1$};

   865   \draw ( 0.6,0.0) node {\small$A_2$};

   866   \end{tikzpicture}}

   867 

   868   & 

   869 

   870   \onslide<3->{\raisebox{1.1mm}{\bf\Large$\;\Rightarrow\,$}}

   871 

   872   &

   873 

   874   \onslide<3->{\begin{tikzpicture}[scale=1]

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

   876   

   877   \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);

   878   \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);

   879 

   880   \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   881   \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   882   

   883   \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   884   \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   885 

   886   \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   887   \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   888   \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   889   

   890   \draw (C) to [red, very thick, bend left=45] (B);

   891   \draw (D) to [red, very thick, bend right=45] (B);

   892 

   893   \draw (-0.6,0.0) node {\small$A_1$};

   894   \draw ( 0.6,0.0) node {\small$A_2$};

   895   \end{tikzpicture}}

   896 

   897   \end{tabular}

   898   \end{center}\medskip

   899 

   900   \only<4-5>{

   901   \begin{tabular}{@ {\hspace{-5mm}}l@ {}}

   902   disjoint union:\\[2mm]

   903   \smath{A_1\uplus A_2 \dn \{(1, x)\,|\, x \in A_1\} \,\cup\, \{(2, y)\,|\, y \in A_2\}}

   904   \end{tabular}}

   905   \end{itemize}

   906 

   907   \only<5>{

   908   \begin{textblock}{13.9}(0.7,7.7)

   909   \begin{block}{}

   910   \medskip

   911   \begin{minipage}{14cm}\raggedright

   912   Problems with definition for regularity:\bigskip\\

   913   \smath{\;\text{is\_regular}(A) \dn \exists M.\;\text{is\_dfa}(M) \wedge {\cal L} (M) = A}\bigskip

   914   \end{minipage}

   915   \end{block}

   916   \end{textblock}}

   917   \medskip

   918 

   919   \only<6->{\underline{A solution}:\;\;use \smath{\text{nat}}s \;@{text "\<Rightarrow>"}\; state nodes\medskip}

   920 

   921   \only<7->{You have to \alert{rename} states!}

   922 

   923   \end{frame}}

   924   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   925 *}

   926 

   927 text_raw {*

   928   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   929   \mode<presentation>{

   930   \begin{frame}[t]

   931   \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}}

   932   \mbox{}\\[-15mm]\mbox{}

   933 

   934   \begin{center}

   935   \huge\bf\textcolor{gray}{in Theorem Provers}\\

   936   \footnotesize\textcolor{gray}{e.g.~Isabelle, Coq, HOL4, \ldots}

   937   \end{center}

   938 

   939   \begin{itemize}

   940   \item Kozen's ``paper'' proof of Myhill-Nerode:\\ 

   941   \hspace{2cm}requires absence of \alert{inaccessible states}

   942   \end{itemize}\bigskip\bigskip

   943 

   944   \begin{center}

   945   \smath{\;\text{is\_regular}(A) \dn \exists M.\;\text{is\_dfa}(M) \wedge {\cal L} (M) = A}

   946   \end{center}

   947 

   948 

   949   \end{frame}}

   950   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   951 *}

   952 

   953 text_raw {*

   954   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   955   \mode<presentation>{

   956   \begin{frame}[t]

   957   \frametitle{}

   958   \mbox{}\\[25mm]\mbox{}

   959 

   960   \begin{textblock}{13.9}(0.7,1.2)

   961   \begin{block}{}

   962   \begin{minipage}{13.4cm}\raggedright

   963   {\bf Definition:}\smallskip\\

   964   

   965   A language \smath{A} is \alert{regular}, provided there exists a\\ 

   966   \alert{regular expression} that matches all strings of \smath{A}.

   967   \end{minipage}

   968   \end{block}

   969   \end{textblock}\pause

   970   

   971   {\noindent\large\bf\alert{\ldots{}and forget about automata}}\bigskip\bigskip\pause

   972 

   973   Infrastructure for free. But do we lose anything?\medskip\pause

   974 

   975   \begin{minipage}{1.1\textwidth}

   976   \begin{itemize}

   977   \item pumping lemma\pause

   978   \item closure under complementation\pause

   979   \item \only<6>{regular expression matching}%

   980        \only<7->{\soutt{regular expression matching}

   981   {\footnotesize(@{text "\<Rightarrow>"}Brozowski'64, Owens et al '09)}}

   982   \item<8-> most textbooks are about automata

   983   \end{itemize}

   984   \end{minipage}

   985 

   986   

   987   \end{frame}}

   988   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   989 

   990 *}

   991 

   992 text_raw {*

   993   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   994   \mode<presentation>{

   995   \begin{frame}[c]

   996   \frametitle{\LARGE The Myhill-Nerode Theorem}

   997 

   998   \begin{itemize}

   999   \item provides necessary and suf\!ficient conditions\\ for a language 

  1000   being regular\\ \textcolor{gray}{(pumping lemma only necessary)}\bigskip

  1001 

  1002   \item key is the equivalence relation:\medskip

  1003   \begin{center}

  1004   \smath{x \approx_{A} y \,\dn\, \forall z.\; x @ z \in A \Leftrightarrow y @ z \in A}

  1005   \end{center}

  1006   \end{itemize}

  1007 

  1008  

  1009   \end{frame}}

  1010   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1011 

  1012 *}

  1013 

  1014 text_raw {*

  1015   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1016   \mode<presentation>{

  1017   \begin{frame}[c]

  1018   \frametitle{\LARGE The Myhill-Nerode Theorem}

  1019 

  1020   \begin{center}

  1021   \only<1>{%

  1022   \begin{tikzpicture}[scale=3]

  1023   \draw[very thick] (0.5,0.5) circle (.6cm);

  1024   \end{tikzpicture}}%

  1025   \only<2->{%

  1026   \begin{tikzpicture}[scale=3]

  1027   \draw[very thick] (0.5,0.5) circle (.6cm);

  1028   \clip[draw] (0.5,0.5) circle (.6cm);

  1029   \draw[step=2mm, very thick] (-1.4,-1.4) grid (1.4,1.4);

  1030   \end{tikzpicture}}

  1031   \end{center}

  1032   

  1033   \begin{itemize}

  1034   \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_A) \;\Leftrightarrow\; A\; \text{is regular}}

  1035   \end{itemize}

  1036 

  1037   \begin{textblock}{5}(2.1,5.3)

  1038   \begin{tikzpicture}

  1039   \node at (0,0) [single arrow, fill=red,text=white, minimum height=2cm]

  1040   {$U\!N\!IV$};

  1041   \draw (-0.3,-1.1) node {\begin{tabular}{l}set of all\\[-1mm] strings\end{tabular}};

  1042   \end{tikzpicture}

  1043   \end{textblock}

  1044 

  1045   \only<2->{%

  1046   \begin{textblock}{5}(9.1,7.2)

  1047   \begin{tikzpicture}

  1048   \node at (0,0) [shape border rotate=180,single arrow, fill=red,text=white, minimum height=2cm]

  1049   {@{text "\<lbrakk>x\<rbrakk>"}$_{\approx_{A}}$};

  1050   \draw (0.9,-1.1) node {\begin{tabular}{l}an equivalence class\end{tabular}};

  1051   \end{tikzpicture}

  1052   \end{textblock}}

  1053 

  1054   \only<3->{

  1055   \begin{textblock}{11.9}(1.7,3)

  1056   \begin{block}{}

  1057   \begin{minipage}{11.4cm}\raggedright

  1058   Two directions:\medskip\\

  1059   \begin{tabular}{@ {}ll}

  1060   1.)\;finite $\Rightarrow$ regular\\

  1061   \;\;\;\smath{\text{finite}\,(U\!N\!IV /\!/ \approx_A) \Rightarrow \exists r.\;A = {\cal L}(r)}\\[3mm]

  1062   2.)\;regular $\Rightarrow$ finite\\

  1063   \;\;\;\smath{\text{finite}\, (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}

  1064   \end{tabular}

  1065 

  1066   \end{minipage}

  1067   \end{block}

  1068   \end{textblock}}

  1069 

  1070   \end{frame}}

  1071   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1072 

  1073 *}

  1074 

  1075 

  1076 

  1077 text_raw {*

  1078   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1079   \mode<presentation>{

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

  1081   \frametitle{\begin{tabular}{@ {}l}\LARGE% 

  1082   Transitions between Eq-Classes\end{tabular}}

  1083 

  1084   \begin{center}

  1085   \begin{tikzpicture}[scale=3]

  1086   \draw[very thick] (0.5,0.5) circle (.6cm);

  1087   \clip[draw] (0.5,0.5) circle (.6cm);

  1088   \draw[step=2mm, very thick] (-1.4,-1.4) grid (1.4,1.4);

  1089   \draw[blue, fill] (0.0, 0.6) rectangle (0.2, 0.8);

  1090   \draw[blue, fill] (0.8, 0.4) rectangle (1.0, 0.6);

  1091   \draw[white] (0.1,0.7) node (X) {$X$};

  1092   \draw[white] (0.9,0.5) node (Y) {$Y$};

  1093   \draw[blue, ->, line width = 2mm, bend left=45] (X) -- (Y);

  1094   \node [inner sep=1pt,label=above:\textcolor{blue}{$c$}] at ($ (X)!.5!(Y) $) {};

  1095   \end{tikzpicture}

  1096   \end{center}

  1097 

  1098   \begin{center}

  1099   \smath{X \stackrel{c}{\longrightarrow} Y \;\dn\; X ; c \subseteq Y}

  1100   \end{center}

  1101 

  1102   \onslide<8>{

  1103   \begin{tabular}{c}

  1104   \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick]

  1105   \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]

  1106   \node[state,initial] (q_0) {$R_1$};

  1107   \end{tikzpicture}

  1108   \end{tabular}}

  1109 

  1110   \end{frame}}

  1111   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1112 *}

  1113 

  1114 text_raw {*

  1115   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1116   \mode<presentation>{

  1117   \begin{frame}[c]

  1118   \frametitle{\LARGE The Other Direction}

  1119 

  1120   One has to prove

  1121 

  1122   \begin{center}

  1123   \smath{\text{finite} (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}

  1124   \end{center}

  1125 

  1126   by induction on \smath{r}. Not trivial, but after a bit 

  1127   of thinking, one can find a \alert{refined} relation:\bigskip

  1128 

  1129   

  1130   \begin{center}

  1131   \mbox{\begin{tabular}{c@ {\hspace{7mm}}c@ {\hspace{7mm}}c}

  1132   \begin{tikzpicture}[scale=1.1]

  1133   %Circle

  1134   \draw[thick] (0,0) circle (1.1);