(*<*)
theory Slides7
imports "~~/src/HOL/Library/LaTeXsugar" "Main"
begin

declare [[show_question_marks = false]]

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

(*>*)

text_raw {*
  \renewcommand{\slidecaption}{Beijing, 29.~April 2011}

  \newcommand{\abst}[2]{#1.#2}% atom-abstraction
  \newcommand{\pair}[2]{\langle #1,#2\rangle} % pairing
  \newcommand{\susp}{{\boldsymbol{\cdot}}}% for suspensions
  \newcommand{\unit}{\langle\rangle}% unit
  \newcommand{\app}[2]{#1\,#2}% application
  \newcommand{\eqprob}{\mathrel{{\approx}?}}
  \newcommand{\freshprob}{\mathrel{\#?}}
  \newcommand{\redu}[1]{\stackrel{#1}{\Longrightarrow}}% reduction
  \newcommand{\id}{\varepsilon}% identity substitution
  
  \newcommand{\bl}[1]{\textcolor{blue}{#1}}
  \newcommand{\gr}[1]{\textcolor{gray}{#1}}
  \newcommand{\rd}[1]{\textcolor{red}{#1}}

  \newcommand{\ok}{\includegraphics[scale=0.07]{ok.png}}
  \newcommand{\notok}{\includegraphics[scale=0.07]{notok.png}}
  \newcommand{\largenotok}{\includegraphics[scale=1]{notok.png}}

  \renewcommand{\Huge}{\fontsize{61.92}{77}\selectfont}
  \newcommand{\veryHuge}{\fontsize{74.3}{93}\selectfont}
  \newcommand{\VeryHuge}{\fontsize{89.16}{112}\selectfont}
  \newcommand{\VERYHuge}{\fontsize{107}{134}\selectfont}

  \newcommand{\LL}{$\mathbb{L}\,$}


  \pgfdeclareradialshading{smallbluesphere}{\pgfpoint{0.5mm}{0.5mm}}%
  {rgb(0mm)=(0,0,0.9);
  rgb(0.9mm)=(0,0,0.7);
  rgb(1.3mm)=(0,0,0.5);
  rgb(1.4mm)=(1,1,1)}

  \def\myitemi{\begin{pgfpicture}{-1ex}{-0.55ex}{1ex}{1ex}
    \usebeamercolor[fg]{subitem projected}
    {\pgftransformscale{0.8}\pgftext{\normalsize\pgfuseshading{bigsphere}}}
    \pgftext{%
      \usebeamerfont*{subitem projected}}
  \end{pgfpicture}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1>[t]
  \frametitle{%
  \begin{tabular}{@ {\hspace{-3mm}}c@ {}}
  \\
  \LARGE Verifying a Regular Expression\\[-1mm] 
  \LARGE Matcher and Formal Language\\[-1mm]
  \LARGE Theory\\[5mm]
  \end{tabular}}
  \begin{center}
  Christian Urban\\
  \small Technical University of Munich, Germany
  \end{center}


  \begin{center}
  \small joint work with Chunhan Wu and Xingyuan Zhang from the PLA
  University of Science and Technology in Nanjing
  \end{center}
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{This Talk: 3 Points}
  \large
  \begin{itemize}
  \item It is easy to make mistakes.\bigskip
  \item Theorem provers can prevent mistakes, {\bf if} the problem
  is formulated so that it is suitable for theorem provers.\bigskip
  \item This re-formulation can be done, even in domains where
  we least expect it.
  \end{itemize}

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

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

  \begin{textblock}{6}(2,4)
  \begin{tabular}{@ {}rrl}
  \bl{r} & \bl{$::=$}  & \bl{$\varnothing$}\\
         & \bl{$\mid$} & \bl{[]}\\
         & \bl{$\mid$} & \bl{c}\\
         & \bl{$\mid$} & \bl{r$_1$ + r$_2$}\\
         & \bl{$\mid$} & \bl{r$_1$ $\cdot$ r$_2$}\\
         & \bl{$\mid$} & \bl{r$^*$}\\
  \end{tabular}
  \end{textblock}

  \begin{textblock}{6}(8,3.5)
  \includegraphics[scale=0.35]{Screen1.png}
  \end{textblock}

  \begin{textblock}{6}(10.2,2.8)
  \footnotesize Isabelle:
  \end{textblock}
  
  \only<2>{
  \begin{textblock}{9}(3.6,11.8)
  \bl{matches r s $\;\Longrightarrow\;$ true $\vee$ false}\\[3.5mm]

  \hspace{10mm}\begin{tikzpicture}
  \coordinate (m1) at (0.4,1);
  \draw (0,0.3) node (m2) {\small\color{gray}rexp};
  \path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (m2) edge (m1);
  
  \coordinate (s1) at (0.81,1);
  \draw (1.3,0.3) node (s2) {\small\color{gray} string};
  \path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (s2) edge (s1);
  \end{tikzpicture}
  \end{textblock}}



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

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

  \small
  \begin{textblock}{6}(0,3.5)
  \begin{tabular}{r@ {\hspace{0.5mm}}r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}
  \multicolumn{4}{c}{rexp $\Rightarrow$ set of strings}\bigskip\\
  &\bl{\LL ($\varnothing$)}   & \bl{$\dn$} & \bl{$\varnothing$}\\
  &\bl{\LL ([])}              & \bl{$\dn$} & \bl{\{[]\}}\\
  &\bl{\LL (c)}               & \bl{$\dn$} & \bl{\{c\}}\\
  &\bl{\LL (r$_1$ + r$_2$)}   & \bl{$\dn$} & \bl{\LL (r$_1$) $\cup$ \LL (r$_2$)}\\
  \rd{$\Rightarrow$} &\bl{\LL (r$_1$ $\cdot$ r$_2$)} & \bl{$\dn$} & \bl{\LL (r$_1$) ;; \LL (r$_2$)}\\
  \rd{$\Rightarrow$} &\bl{\LL (r$^*$)}           & \bl{$\dn$} & \bl{(\LL (r))$^\star$}\\
  \end{tabular}
  \end{textblock}

  \begin{textblock}{9}(7.3,3)
  {\mbox{}\hspace{2cm}\footnotesize Isabelle:\smallskip}
  \includegraphics[scale=0.325]{Screen3.png}
  \end{textblock}

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


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1->[t]
  \frametitle{Version 1}
  \small
  \mbox{}\\[-8mm]\mbox{}

  \begin{center}\def\arraystretch{1.05}
  \begin{tabular}{@ {\hspace{-5mm}}l@ {\hspace{2.5mm}}c@ {\hspace{2.5mm}}l@ {}}
  \bl{match [] []}                   & \bl{$=$} & \bl{true}\\
  \bl{match [] (c::s)}               & \bl{$=$} & \bl{false}\\
  \bl{match ($\varnothing$::rs) s}   & \bl{$=$} & \bl{false}\\
  \bl{match ([]::rs) s}              & \bl{$=$} & \bl{match rs s}\\
  \bl{match (c::rs) []}              & \bl{$=$} & \bl{false}\\
  \bl{match (c::rs) (d::s)}          & \bl{$=$} & \bl{if c = d then match rs s else false}\\     
  \bl{match (r$_1$ + r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::rs) s $\vee$ match (r$_2$::rs) s}\\ 
  \bl{match (r$_1$ $\cdot$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::r$_2$::rs) s}\\
  \bl{match (r$^*$::rs) s}          & \bl{$=$} & \bl{match rs s $\vee$ match (r::r$^*$::rs) s}\\
  \end{tabular}
  \end{center}

  \begin{textblock}{9}(0.2,1.6)
  \hspace{10mm}\begin{tikzpicture}
  \coordinate (m1) at (0.44,-0.5);
  \draw (0,0.3) node (m2) {\small\color{gray}\mbox{}\hspace{-9mm}list of rexps};
  \path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (m2) edge (m1);
  
  \coordinate (s1) at (0.86,-0.5);
  \draw (1.5,0.3) node (s2) {\small\color{gray} string};
  \path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (s2) edge (s1);
  \end{tikzpicture}
  \end{textblock}

  \begin{textblock}{9}(2.8,11.8)
  \bl{matches$_1$ r s $\;=\;$ match [r] s}
  \end{textblock}

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

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1->[c]
  \frametitle{Testing}
  
  \small
  Every good programmer should do thourough tests: 

  \begin{center}
  \begin{tabular}{@ {\hspace{-20mm}}lcl}
  \bl{matches$_1$ (a$\cdot$b)$^*\;$ []}     & \bl{$\mapsto$} & \bl{true}\\
  \bl{matches$_1$ (a$\cdot$b)$^*\;$ ab}   & \bl{$\mapsto$} & \bl{true}\\ 
  \bl{matches$_1$ (a$\cdot$b)$^*\;$ aba}  & \bl{$\mapsto$} & \bl{false}\\
  \bl{matches$_1$ (a$\cdot$b)$^*\;$ abab} & \bl{$\mapsto$} & \bl{true}\\ 
  \bl{matches$_1$ (a$\cdot$b)$^*\;$ abaa} & \bl{$\mapsto$} & \bl{false}\medskip\\
  \onslide<2->{\bl{matches$_1$ x$\cdot$(0$|$1)$^*\;$ x}   & \bl{$\mapsto$} & \bl{true}}\\
  \onslide<2->{\bl{matches$_1$ x$\cdot$(0$|$1)$^*\;$ x0}  & \bl{$\mapsto$} & \bl{true}}\\
  \onslide<2->{\bl{matches$_1$ x$\cdot$(0$|$1)$^*\;$ x3}  & \bl{$\mapsto$} & \bl{false}}
  \end{tabular}
  \end{center}
 
  \onslide<3->
  {Looks OK \ldots let's ship it to customers\hspace{5mm} 
   \raisebox{-5mm}{\includegraphics[scale=0.05]{sun.png}}}
  
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

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

  \only<1->{Several hours later\ldots}\pause


  \begin{center}
  \begin{tabular}{@ {\hspace{0mm}}lcl}
  \bl{matches$_1$ []$^*$ s}     & \bl{$\mapsto$} & loops\\
  \onslide<4->{\bl{matches$_1$ ([] + \ldots)$^*$ s}   & \bl{$\mapsto$} & loops\\} 
  \end{tabular}
  \end{center}

  \small
  \onslide<3->{
  \begin{center}
  \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
  \ldots\\
  \bl{match ([]::rs) s}           & \bl{$=$} & \bl{match rs s}\\
  \ldots\\
  \bl{match (r$^*$::rs) s}        & \bl{$=$} & \bl{match rs s $\vee$ match (r::r$^*$::rs) s}\\
  \end{tabular}
  \end{center}}
  

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


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

  \begin{itemize}
  \item While testing is an important part in the process of programming development\pause\ldots

  \item we can only test a {\bf finite} amount of examples.\bigskip\pause

  \begin{center}
  \colorbox{cream}
  {\gr{\begin{minipage}{10cm}
  ``Testing can only show the presence of errors, never their
  absence.'' (Edsger W.~Dijkstra)
  \end{minipage}}}
  \end{center}\bigskip\pause

  \item In a theorem prover we can establish properties that apply to 
  {\bf all} input and {\bf all} output. 

  \end{itemize}

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


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1->[t]
  \frametitle{Version 2}
  \mbox{}\\[-14mm]\mbox{}

  \small
  \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}}
  \bl{nullable ($\varnothing$)}   & \bl{$=$} & \bl{false} &\\
  \bl{nullable ([])}              & \bl{$=$} & \bl{true}  &\\
  \bl{nullable (c)}               & \bl{$=$} & \bl{false} &\\
  \bl{nullable (r$_1$ + r$_2$)}   & \bl{$=$} & \bl{nullable r$_1$ $\vee$ nullable r$_2$} & \\ 
  \bl{nullable (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{nullable r$_1$ $\wedge$ nullable r$_2$} & \\
  \bl{nullable (r$^*$)}           & \bl{$=$} & \bl{true} & \\
  \end{tabular}\medskip

  \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
  \bl{der c ($\varnothing$)}       & \bl{$=$} & \bl{$\varnothing$} & \\
  \bl{der c ([])}                  & \bl{$=$} & \bl{$\varnothing$} & \\
  \bl{der c (d)}                   & \bl{$=$} & \bl{if c = d then [] else $\varnothing$} & \\
  \bl{der c (r$_1$ + r$_2$)}       & \bl{$=$} & \bl{(der c r$_1$) + (der c r$_2$)} & \\
  \bl{der c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{((der c r$_1$) $\cdot$ r$_2$)} & \\
       &          & \bl{\;\;\;\;+ (if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\
  \bl{der c (r$^*$)}          & \bl{$=$} & \bl{(der c r) $\cdot$ r$^*$} &\smallskip\\

  \bl{derivative r []}     & \bl{$=$} & \bl{r} & \\
  \bl{derivative r (c::s)} & \bl{$=$} & \bl{derivative (der c r) s} & \\
  \end{tabular}\medskip

  \bl{matches$_2$ r s $=$ nullable (derivative r s)}

  \begin{textblock}{6}(9.5,0.9)
  \begin{flushright}
  \color{gray}``if r matches []'' 
  \end{flushright}
  \end{textblock}

  \begin{textblock}{6}(9.5,6.18)
  \begin{flushright}
  \color{gray}``derivative w.r.t.~a char'' 
  \end{flushright}
  \end{textblock}

  \begin{textblock}{6}(9.5,12.1)
  \begin{flushright}
  \color{gray}``deriv.~w.r.t.~a string'' 
  \end{flushright}
  \end{textblock}

  \begin{textblock}{6}(9.5,13.98)
  \begin{flushright}
  \color{gray}``main'' 
  \end{flushright}
  \end{textblock}

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

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1->[t]
  \frametitle{Is the Matcher Error-Free?}

  We expect that

  \begin{center}
  \begin{tabular}{lcl}
  \bl{matches$_2$ r s = true}  & \only<1>{\rd{$\Longrightarrow\,\,$}}\only<2>{\rd{$\Longleftarrow\,\,$}}% 
  \only<3->{\rd{$\Longleftrightarrow$}} & \bl{s $\in$ \LL(r)}\\
  \bl{matches$_2$ r s = false} & \only<1>{\rd{$\Longrightarrow\,\,$}}\only<2>{\rd{$\Longleftarrow\,\,$}}%
  \only<3->{\rd{$\Longleftrightarrow$}} & \bl{s $\notin$ \LL(r)}\\
  \end{tabular}
  \end{center}
  \pause\pause\bigskip
  By \alert<4->{induction}, we can {\bf prove} these properties.\bigskip

  \begin{tabular}{lrcl}
  Lemmas:  & \bl{nullable (r)}          & \bl{$\Longleftrightarrow$} & \bl{[] $\in$ \LL (r)}\\
           & \bl{s $\in$ \LL (der c r)} & \bl{$\Longleftrightarrow$} & \bl{(c::s) $\in$ \LL (r)}\\
  \end{tabular}
  
  \only<4->{
  \begin{textblock}{3}(0.9,4.5)
  \rd{\huge$\forall$\large{}r s.}
  \end{textblock}}
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1>[c]
  \frametitle{
  \begin{tabular}{c}
  \mbox{}\\[23mm]
  \LARGE Demo
  \end{tabular}}
  
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}


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

  \mbox{}\\[-2mm]

  \small
  \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}}
  \bl{nullable (NULL)}            & \bl{$=$} & \bl{false} &\\
  \bl{nullable (EMPTY)}           & \bl{$=$} & \bl{true}  &\\
  \bl{nullable (CHR c)}           & \bl{$=$} & \bl{false} &\\
  \bl{nullable (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) orelse (nullable r$_2$)} & \\ 
  \bl{nullable (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) andalso (nullable r$_2$)} & \\
  \bl{nullable (STAR r)}          & \bl{$=$} & \bl{true} & \\
  \end{tabular}\medskip

  \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
  \bl{der c (NULL)}            & \bl{$=$} & \bl{NULL} & \\
  \bl{der c (EMPTY)}           & \bl{$=$} & \bl{NULL} & \\
  \bl{der c (CHR d)}           & \bl{$=$} & \bl{if c=d then EMPTY else NULL} & \\
  \bl{der c (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (der c r$_1$) (der c r$_2$)} & \\
  \bl{der c (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (SEQ (der c r$_1$) r$_2$)} & \\
       &          & \bl{\phantom{ALT} (if nullable r$_1$ then der c r$_2$ else NULL)}\\
  \bl{der c (STAR r)}          & \bl{$=$} & \bl{SEQ (der c r) (STAR r)} &\smallskip\\

  \bl{derivative r []}     & \bl{$=$} & \bl{r} & \\
  \bl{derivative r (c::s)} & \bl{$=$} & \bl{derivative (der c r) s} & \\
  \end{tabular}\medskip

  \bl{matches r s $=$ nullable (derivative r s)}
  
  \only<2>{
  \begin{textblock}{8}(1.5,4)
  \includegraphics[scale=0.3]{approved.png}
  \end{textblock}}
  
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{No Automata?}

  You might be wondering why I did not use any automata?

  \begin{itemize}
  \item {\bf Def.:} A \alert{regular language} is one where there is a DFA that 
  recognises it.\bigskip\pause
  \end{itemize}


  There are many reasons why this is a good definition:\medskip
  \begin{itemize}
  \item pumping lemma
  \item closure properties of regular languages\\ (e.g.~closure under complement)
  \end{itemize}

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

*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[t]
  \frametitle{Really Bad News!}

  DFAs are bad news for formalisations in theorem provers. They might
  be represented as:

  \begin{itemize}
  \item graphs
  \item matrices
  \item partial functions
  \end{itemize}

  All constructions are messy to reason about.\bigskip\bigskip 
  \pause

  \small
  \only<2>{
  Constable et al needed (on and off) 18 months for a 3-person team 
  to formalise automata theory in Nuprl including Myhill-Nerode. There is 
  only very little other formalised work on regular languages I know of
  in Coq, Isabelle and HOL.}
  \only<3>{Typical textbook reasoning goes like: ``\ldots if \smath{M} and \smath{N} are any two
  automata with no inaccessible states \ldots''
  }
  
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{}
  \large
  \begin{center}
  \begin{tabular}{p{9cm}}
  My point:\bigskip\\

  The theory about regular languages can be reformulated 
  to be more\\ suitable for theorem proving.
  \end{tabular}
  \end{center}
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{\LARGE The Myhill-Nerode Theorem}

  \begin{itemize}
  \item provides necessary and suf\!ficient conditions for a language 
  being regular (pumping lemma only necessary)\medskip

  \item will help with closure properties of regular languages\bigskip\pause

  \item key is the equivalence relation:\smallskip
  \begin{center}
  \smath{x \approx_{L} y \,\dn\, \forall z.\; x @ z \in L \Leftrightarrow y @ z \in L}
  \end{center}
  \end{itemize}

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

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{\LARGE The Myhill-Nerode Theorem}

  \mbox{}\\[5cm]

  \begin{itemize}
  \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_L) \;\Leftrightarrow\; L\; \text{is regular}}
  \end{itemize}

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

*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{\LARGE Equivalence Classes}

  \begin{itemize}
  \item \smath{L = []}
  \begin{center}
  \smath{\Big\{\{[]\},\; U\!N\!IV - \{[]\}\Big\}}
  \end{center}\bigskip\bigskip

  \item \smath{L = [c]}
  \begin{center}
  \smath{\Big\{\{[]\},\; \{[c]\},\; U\!N\!IV - \{[], [c]\}\Big\}}
  \end{center}\bigskip\bigskip

  \item \smath{L = \varnothing}
  \begin{center}
  \smath{\Big\{U\!N\!IV\Big\}}
  \end{center}

  \end{itemize}

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

*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{\LARGE Regular Languages}

  \begin{itemize}
  \item \smath{L} is regular \smath{\dn} if there is an automaton \smath{M} 
  such that \smath{\mathbb{L}(M) = L}\\[1.5cm]

  \item Myhill-Nerode:

  \begin{center}
  \begin{tabular}{l}
  finite $\Rightarrow$ regular\\
  \;\;\;\smath{\text{finite}\,(U\!N\!IV /\!/ \approx_L) \Rightarrow \exists r.\; L = \mathbb{L}(r)}\\[3mm]
  regular $\Rightarrow$ finite\\
  \;\;\;\smath{\text{finite}\, (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}
  \end{tabular}
  \end{center}

  \end{itemize}

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

*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{\LARGE Final Equiv.~Classes}

  \mbox{}\\[3cm]

  \begin{itemize}
  \item \smath{\text{finals}\,L \dn 
     \{{\lbrack\mkern-2mu\lbrack{s}\rbrack\mkern-2mu\rbrack}_\approx\;|\; s \in L\}}\\
  \medskip

  \item we can prove: \smath{L = \bigcup (\text{finals}\,L)}

  \end{itemize}

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

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{\LARGE Transitions between ECs}

  \smath{L = \{[c]\}}

  \begin{tabular}{@ {\hspace{-7mm}}cc}
  \begin{tabular}{c}
  \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick]
  \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]

  %\draw[help lines] (0,0) grid (3,2);

  \node[state,initial]   (q_0)                        {$R_1$};
  \node[state,accepting] (q_1) [above right of=q_0]   {$R_2$};
  \node[state]           (q_2) [below right of=q_0]   {$R_3$};

  \path[->] (q_0) edge                node        {c} (q_1)
                  edge                node [swap] {$\Sigma-{c}$} (q_2)
            (q_2) edge [loop below]   node        {$\Sigma$} ()
            (q_1) edge                node        {$\Sigma$} (q_2);
  \end{tikzpicture}
  \end{tabular}
  &
  \begin{tabular}[t]{ll}
  \\[-20mm]
  \multicolumn{2}{l}{\smath{U\!N\!IV /\!/\approx_L} produces}\\[4mm]

  \smath{R_1}: & \smath{\{[]\}}\\
  \smath{R_2}: & \smath{\{[c]\}}\\
  \smath{R_3}: & \smath{U\!N\!IV - \{[], [c]\}}\\[6mm]
  \multicolumn{2}{l}{\onslide<2->{\smath{X \stackrel{c}{\longrightarrow} Y \dn X ;; [c] \subseteq Y}}}
  \end{tabular}

  \end{tabular}

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


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{\LARGE Systems of Equations}

  Inspired by a method of Brzozowski\;'64, we can build an equational system
  characterising the equivalence classes:

  \begin{center}
  \begin{tabular}{@ {\hspace{-20mm}}c}
  \\[-13mm]
  \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick]
  \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]

  %\draw[help lines] (0,0) grid (3,2);

  \node[state,initial]   (p_0)                  {$R_1$};
  \node[state,accepting] (p_1) [right of=q_0]   {$R_2$};

  \path[->] (p_0) edge [bend left]   node        {a} (p_1)
                  edge [loop above]   node       {b} ()
            (p_1) edge [loop above]   node       {a} ()
                  edge [bend left]   node        {b} (p_0);
  \end{tikzpicture}\\
  \\[-13mm]
  \end{tabular}
  \end{center}

  \begin{center}
  \begin{tabular}{@ {\hspace{-6mm}}ll@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
  & \smath{R_1} & \smath{\equiv} & \smath{R_1;b + R_2;b \onslide<2->{\alert<2>{+ \lambda;[]}}}\\
  & \smath{R_2} & \smath{\equiv} & \smath{R_1;a + R_2;a}\medskip\\
  \onslide<3->{we can prove} 
  & \onslide<3->{\smath{R_1}} & \onslide<3->{\smath{=}} 
      & \onslide<3->{\smath{R_1;; \mathbb{L}(b) \,\cup\, R_2;;\mathbb{L}(b) \,\cup\, \{[]\}}}\\
  & \onslide<3->{\smath{R_2}} & \onslide<3->{\smath{=}}    
      & \onslide<3->{\smath{R_1;; \mathbb{L}(a) \,\cup\, R_2;;\mathbb{L}(a)}}\\
  \end{tabular}
  \end{center}

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


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1>[t]
  \small

  \begin{center}
  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}
  \onslide<1->{\smath{R_1}} & \onslide<1->{\smath{=}} 
      & \onslide<1->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
  \onslide<1->{\smath{R_2}} & \onslide<1->{\smath{=}}    
      & \onslide<1->{\smath{R_1; a + R_2; a}}\\

  & & & \onslide<2->{by Arden}\\

  \onslide<2->{\smath{R_1}} & \onslide<2->{\smath{=}} 
      & \onslide<2->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
  \onslide<2->{\smath{R_2}} & \onslide<2->{\smath{=}}    
      & \only<2>{\smath{R_1; a + R_2; a}}%
        \only<3->{\smath{R_1; a\cdot a^\star}}\\

  & & & \onslide<4->{by Arden}\\

  \onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}} 
      & \onslide<4->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\
  \onslide<4->{\smath{R_2}} & \onslide<4->{\smath{=}}    
      & \onslide<4->{\smath{R_1; a\cdot a^\star}}\\

  & & & \onslide<5->{by substitution}\\

  \onslide<5->{\smath{R_1}} & \onslide<5->{\smath{=}} 
      & \onslide<5->{\smath{R_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\
  \onslide<5->{\smath{R_2}} & \onslide<5->{\smath{=}}    
      & \onslide<5->{\smath{R_1; a\cdot a^\star}}\\

  & & & \onslide<6->{by Arden}\\

  \onslide<6->{\smath{R_1}} & \onslide<6->{\smath{=}} 
      & \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
  \onslide<6->{\smath{R_2}} & \onslide<6->{\smath{=}}    
      & \onslide<6->{\smath{R_1; a\cdot a^\star}}\\

  & & & \onslide<7->{by substitution}\\

  \onslide<7->{\smath{R_1}} & \onslide<7->{\smath{=}} 
      & \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
  \onslide<7->{\smath{R_2}} & \onslide<7->{\smath{=}}    
      & \onslide<7->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star 
          \cdot a\cdot a^\star}}\\
  \end{tabular}
  \end{center}

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

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{\LARGE A Variant of Arden's Lemma}

  {\bf Arden's Lemma:}\smallskip 

  If \smath{[] \not\in A} then
  \begin{center}
  \smath{X = X; A + \text{something}}
  \end{center}
  has the (unique) solution
  \begin{center}
  \smath{X = \text{something} ; A^\star}
  \end{center}


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


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

  \begin{center}
  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}
  \onslide<1->{\smath{R_1}} & \onslide<1->{\smath{=}} 
      & \onslide<1->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
  \onslide<1->{\smath{R_2}} & \onslide<1->{\smath{=}}    
      & \onslide<1->{\smath{R_1; a + R_2; a}}\\

  & & & \onslide<2->{by Arden}\\

  \onslide<2->{\smath{R_1}} & \onslide<2->{\smath{=}} 
      & \onslide<2->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
  \onslide<2->{\smath{R_2}} & \onslide<2->{\smath{=}}    
      & \only<2>{\smath{R_1; a + R_2; a}}%
        \only<3->{\smath{R_1; a\cdot a^\star}}\\

  & & & \onslide<4->{by Arden}\\

  \onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}} 
      & \onslide<4->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\
  \onslide<4->{\smath{R_2}} & \onslide<4->{\smath{=}}    
      & \onslide<4->{\smath{R_1; a\cdot a^\star}}\\

  & & & \onslide<5->{by substitution}\\

  \onslide<5->{\smath{R_1}} & \onslide<5->{\smath{=}} 
      & \onslide<5->{\smath{R_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\
  \onslide<5->{\smath{R_2}} & \onslide<5->{\smath{=}}    
      & \onslide<5->{\smath{R_1; a\cdot a^\star}}\\

  & & & \onslide<6->{by Arden}\\

  \onslide<6->{\smath{R_1}} & \onslide<6->{\smath{=}} 
      & \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
  \onslide<6->{\smath{R_2}} & \onslide<6->{\smath{=}}    
      & \onslide<6->{\smath{R_1; a\cdot a^\star}}\\

  & & & \onslide<7->{by substitution}\\

  \onslide<7->{\smath{R_1}} & \onslide<7->{\smath{=}} 
      & \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
  \onslide<7->{\smath{R_2}} & \onslide<7->{\smath{=}}    
      & \onslide<7->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star 
          \cdot a\cdot a^\star}}\\
  \end{tabular}
  \end{center}

  \only<8->{
  \begin{textblock}{6}(2.5,4)
  \begin{block}{}
  \begin{minipage}{8cm}\raggedright
  
  \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick, inner sep=1mm]
  \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]

  %\draw[help lines] (0,0) grid (3,2);

  \node[state,initial]   (p_0)                  {$R_1$};
  \node[state,accepting] (p_1) [right of=q_0]   {$R_2$};

  \path[->] (p_0) edge [bend left]   node        {a} (p_1)
                  edge [loop above]   node       {b} ()
            (p_1) edge [loop above]   node       {a} ()
                  edge [bend left]   node        {b} (p_0);
  \end{tikzpicture}

  \end{minipage}
  \end{block}
  \end{textblock}}

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


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{\LARGE The Equ's Solving Algorithm}

  \begin{itemize}
  \item The algorithm must terminate: Arden makes one equation smaller; 
  substitution deletes one variable from the right-hand sides.\bigskip

  \item We need to maintain the invariant that Arden is applicable
  (if \smath{[] \not\in A} then \ldots):\medskip

  \begin{center}\small
  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}
  \smath{R_1} & \smath{=} & \smath{R_1; b + R_2; b + \lambda;[]}\\
  \smath{R_2} & \smath{=} & \smath{R_1; a + R_2; a}\\

  & & & by Arden\\

  \smath{R_1} & \smath{=} & \smath{R_1; b + R_2; b + \lambda;[]}\\
  \smath{R_2} & \smath{=} & \smath{R_1; a\cdot a^\star}\\
  \end{tabular}
  \end{center}

  \end{itemize}


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



text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{\LARGE The Other Direction}
  
  One has to prove

  \begin{center}
  \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}
  \end{center}

  by induction on \smath{r}. This is straightforward for \\the base cases:\small

  \begin{center}
  \begin{tabular}{l@ {\hspace{1mm}}l}
  \smath{U\!N\!IV /\!/ \!\approx_{\emptyset}} & \smath{= \{U\!N\!IV\}}\smallskip\\
  \smath{U\!N\!IV /\!/ \!\approx_{\{[]\}}} & \smath{\subseteq \{\{[]\}, U\!N\!IV - \{[]\}\}}\smallskip\\
  \smath{U\!N\!IV /\!/ \!\approx_{\{[c]\}}} & \smath{\subseteq \{\{[]\}, \{[c]\}, U\!N\!IV - \{[], [c]\}\}}
  \end{tabular}
  \end{center}

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


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[t]
  \frametitle{\LARGE The Other Direction}

  More complicated are the inductive cases:\\ one needs to prove that if

  \begin{center}
  \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1)})}\hspace{3mm}
  \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_2)})}
  \end{center}

  then

  \begin{center}
  \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1) \,\cup\, \mathbb{L}(r_2)})}
  \end{center}
  
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[t]
  \frametitle{\LARGE Helper Lemma}

  \begin{center}
  \begin{tabular}{p{10cm}}
  %If \smath{\text{finite} (f\;' A)} and \smath{f} is injective 
  %(on \smath{A}),\\ then \smath{\text{finite}\,A}.
  Given two equivalence relations \smath{R_1} and \smath{R_2} with
  \smath{R_1} refining \smath{R_2} (\smath{R_1 \subseteq R_2}).\\ 
  Then\medskip\\
  \smath{\;\;\text{finite} (U\!N\!IV /\!/ R_1) \Rightarrow \text{finite} (U\!N\!IV /\!/ R_2)}
  \end{tabular}
  \end{center}
  
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{\Large Derivatives and Left-Quotients}
  \small
  Work by Brozowski ('64) and Antimirov ('96):\pause\smallskip


  \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
  \multicolumn{4}{@ {}l}{Left-Quotient:}\\
  \multicolumn{4}{@ {}l}{\bl{$\text{Ders}\;\text{s}\,A \dn \{\text{s'} \;|\; \text{s @ s'} \in A\}$}}\bigskip\\

  \multicolumn{4}{@ {}l}{Derivative:}\\
  \bl{der c ($\varnothing$)}       & \bl{$=$} & \bl{$\varnothing$} & \\
  \bl{der c ([])}                  & \bl{$=$} & \bl{$\varnothing$} & \\
  \bl{der c (d)}                   & \bl{$=$} & \bl{if c = d then [] else $\varnothing$} & \\
  \bl{der c (r$_1$ + r$_2$)}       & \bl{$=$} & \bl{(der c r$_1$) + (der c r$_2$)} & \\
  \bl{der c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{((der c r$_1$) $\cdot$ r$_2$)} & \\
       &          & \bl{\;\;\;\;+ (if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\
  \bl{der c (r$^*$)}          & \bl{$=$} & \bl{(der c r) $\cdot$ r$^*$} &\smallskip\\

  \bl{ders [] r}     & \bl{$=$} & \bl{r} & \\
  \bl{ders (s @ [c]) r} & \bl{$=$} & \bl{der c (ders s r)} & \\
  \end{tabular}\pause

  \begin{center}
  \alert{$\Rightarrow$}\smath{\;\;\text{Ders}\,\text{s}\,(\mathbb{L}(\text{r})) = \mathbb{L} (\text{ders s r})}
  \end{center}
  
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{\LARGE Left-Quotients and MN-Rels}

  \begin{itemize}
  \item \smath{x \approx_{A} y \,\dn\, \forall z.\; x @ z \in A \Leftrightarrow y @ z \in A}\medskip
  \item \bl{$\text{Ders}\;s\,A \dn \{s' \;|\; s @ s' \in A\}$}
  \end{itemize}\bigskip

  \begin{center}
  \smath{x \approx_A y  \Longleftrightarrow \text{Ders}\;x\;A = \text{Ders}\;y\;A}
  \end{center}\bigskip\pause\small

  which means

  \begin{center}
  \smath{x \approx_{\mathbb{L}(r)} y  \Longleftrightarrow 
  \mathbb{L}(\text{ders}\;x\;r) = \mathbb{L}(\text{ders}\;y\;r)}
  \end{center}\pause

  \hspace{8.8mm}or
  \smath{\;x \approx_{\mathbb{L}(r)} y  \Longleftarrow 
  \text{ders}\;x\;r = \text{ders}\;y\;r}

  

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

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{\LARGE Partial Derivatives}

  Antimirov: \bl{pder : rexp $\Rightarrow$ rexp set}\bigskip

  \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
  \bl{pder c ($\varnothing$)}       & \bl{$=$} & \bl{\{$\varnothing$\}} & \\
  \bl{pder c ([])}                  & \bl{$=$} & \bl{\{$\varnothing$\}} & \\
  \bl{pder c (d)}                   & \bl{$=$} & \bl{if c = d then \{[]\} else \{$\varnothing$\}} & \\
  \bl{pder c (r$_1$ + r$_2$)}       & \bl{$=$} & \bl{(pder c r$_1$) $\cup$ (pder c r$_2$)} & \\
  \bl{pder c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{(pder c r$_1$) $\odot$ r$_2$} & \\
       &          & \bl{\hspace{-10mm}$\cup$ (if nullable r$_1$ then pder c r$_2$ else $\varnothing$)}\\
  \bl{pder c (r$^*$)}          & \bl{$=$} & \bl{(pder c r) $\odot$ r$^*$} &\smallskip\\
  \end{tabular}

  \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
  \bl{pders [] r}     & \bl{$=$} & \bl{r} & \\
  \bl{pders (s @ [c]) r} & \bl{$=$} & \bl{pder c (pders s r)} & \\
  \end{tabular}\pause

  \begin{center}
  \alert{$\Rightarrow$}\smath{\;\;\text{Ders}\,\text{s}\,(\mathbb{L}(\text{r})) = \bigcup (\mathbb{L}\;`\; (\text{pders s r}))}
  \end{center}

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

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[t]
  \frametitle{\LARGE Final Result}
  
  \mbox{}\\[7mm]

  \begin{itemize}
  \item \alt<1>{\smath{\text{pders x r \mbox{$=$} pders y r}}}
            {\smath{\underbrace{\text{pders x r \mbox{$=$} pders y r}}_{R_1}}} 
        refines \bl{x $\approx_{\mathbb{L}(\text{r})}$ y}\pause
  \item \smath{\text{finite} (U\!N\!IV /\!/ R_1)} \bigskip\pause
  \item Therefore \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}. Qed.
  \end{itemize}
  
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{\LARGE What Have We Achieved?}

  \begin{itemize}
  \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_L) \;\Leftrightarrow\; L\; \text{is regular}}
  \bigskip\pause
  \item regular languages are closed under complementation; this is now easy\medskip
  \begin{center}
  \smath{U\!N\!IV /\!/ \approx_L \;\;=\;\; U\!N\!IV /\!/ \approx_{-L}}
  \end{center}
  \end{itemize}

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

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

  \begin{itemize}
  \item \smath{L \equiv \Sigma^\star 0 \Sigma} is regular
  \begin{quote}\small
  \begin{tabular}{lcl}
  \smath{A_1} & \smath{=} & \smath{\Sigma^\star 00}\\
  \smath{A_2} & \smath{=} & \smath{\Sigma^\star 01}\\
  \smath{A_3} & \smath{=} & \smath{\Sigma^\star 10 \cup \{0\}}\\
  \smath{A_4} & \smath{=} & \smath{\Sigma^\star 11 \cup \{1\} \cup \{[]\}}\\
  \end{tabular}
  \end{quote}

  \item \smath{L \equiv \{ 0^n 1^n \,|\, n \ge 0\}} is not regular
  \begin{quote}\small
  \begin{tabular}{lcl}
  \smath{B_0} & \smath{=} & \smath{\{0^n 1^n \,|\,     n \ge 0\}}\\
  \smath{B_1} & \smath{=} & \smath{\{0^n 1^{(n-1)} \,|\, n \ge 1\}}\\
  \smath{B_2} & \smath{=} & \smath{\{0^n 1^{(n-2)} \,|\, n \ge 2\}}\\
  \smath{B_3} & \smath{=} & \smath{\{0^n 1^{(n-3)} \,|\, n \ge 3\}}\\
              & \smath{\vdots} &\\
  \end{tabular}
  \end{quote}
  \end{itemize}

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


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{\LARGE What We Have Not Achieved}

  \begin{itemize}
  \item regular expressions are not good if you look for a minimal
  one for a language (DFAs have this notion)\pause\bigskip

  \item Is there anything to be said about context free languages:\medskip
  
  \begin{quote}
  A context free language is where every string can be recognised by
  a pushdown automaton.\bigskip
  \end{quote}
  \end{itemize}

  \textcolor{gray}{\footnotesize Yes. Derivatives also work for c-f grammars. Ongoing work.}

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


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

  \begin{itemize}
  \item We formalised the Myhill-Nerode theorem based on 
  regular expressions only (DFAs are difficult to deal with in a theorem prover).\smallskip

  \item Seems to be a common theme: algorithms need to be reformulated
  to better suit formal treatment.\smallskip

  \item The most interesting aspect is that we are able to
  implement the matcher directly inside the theorem prover
  (ongoing work).\smallskip

  \item Parsing is a vast field which seem to offer new results. 
  \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
(*>*)