(*<*)
theory Slides8
imports "~~/src/HOL/Library/LaTeXsugar" "Nominal"
begin

declare [[show_question_marks = false]]

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

(*>*)

text_raw {*
  \renewcommand{\slidecaption}{Copenhagen, 23rd~May 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: 4 Points}
  \large
  \begin{itemize}
  \item It is easy to make mistakes.\medskip
  \item Theorem provers can prevent mistakes, {\bf if} the problem
  is formulated so that it is suitable for theorem provers.\medskip
  \item This re-formulation can be done, even in domains where
  we least expect it.\medskip 
  \item Where theorem provers are superior to the {\color{gray}{(best)}} human reasoners. ;o)
  \end{itemize}

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


text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{}

  \begin{tabular}{c@ {\hspace{2mm}}c}
  \\[6mm]
  \begin{tabular}{c}
  \includegraphics[scale=0.12]{harper.jpg}\\[-2mm]
  {\footnotesize Bob Harper}\\[-2.5mm]
  {\footnotesize (CMU)}
  \end{tabular}
  \begin{tabular}{c}
  \includegraphics[scale=0.36]{pfenning.jpg}\\[-2mm]
  {\footnotesize Frank Pfenning}\\[-2.5mm]
  {\footnotesize (CMU)}
  \end{tabular} &

  \begin{tabular}{p{6cm}}
  \raggedright
  \color{gray}{published a proof in\\ {\bf ACM Transactions on Computational Logic} (2005),
  $\sim$31pp}
  \end{tabular}\\

  \pause
  \\[0mm]
  
  \begin{tabular}{c}
  \includegraphics[scale=0.36]{appel.jpg}\\[-2mm] 
  {\footnotesize Andrew Appel}\\[-2.5mm]
  {\footnotesize (Princeton)}
  \end{tabular} &

  \begin{tabular}{p{6cm}}
  \raggedright
  \color{gray}{relied on their proof in a\\ {\bf security} critical application}
  \end{tabular}
  \end{tabular}


  


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

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}
  \frametitle{Proof-Carrying Code}

  \begin{textblock}{10}(2.5,2.2)
  \begin{block}{Idea:}
  \begin{center}
  \begin{tikzpicture}
  \draw[help lines,cream] (0,0.2) grid (8,4);
  
  \draw[line width=1mm, red] (5.5,0.6) rectangle (7.5,4);
  \node[anchor=base] at (6.5,2.8) 
     {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering  user: untrusted code\end{tabular}};

  \draw[line width=1mm, red] (0.5,0.6) rectangle (2.5,4);
  \node[anchor=base] at (1.5,2.3) 
     {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering  developer ---\\ web server\end{tabular}};
  
  \onslide<3->{
  \draw[line width=1mm, red, fill=red] (5.5,0.6) rectangle (7.5,1.8);
  \node[anchor=base,white] at (6.5,1.1) 
     {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\bf\centering proof- checker\end{tabular}};}

  \node at (3.8,3.0) [single arrow, fill=red,text=white, minimum height=3cm]{\bf code};
  \onslide<2->{
  \node at (3.8,1.3) [single arrow, fill=red,text=white, minimum height=3cm]{\bf certificate};
  \node at (3.8,1.9) {\small\color{gray}{\mbox{}\hspace{-1mm}a proof in LF}};
  }

  
  \end{tikzpicture}
  \end{center}
  \end{block}
  \end{textblock}

  %\begin{textblock}{15}(2,12)
  %\small
  %\begin{itemize}
  %\item<4-> Appel's checker is $\sim$2700 lines of code (1865 loc of\\ LF definitions; 
  %803 loc in C including 2 library functions)\\[-3mm]
  %\item<5-> 167 loc in C implement a type-checker
  %\end{itemize}
  %\end{textblock}

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

*}

text {*
  \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]
  \tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick, 
                     draw=black!50, top color=white, bottom color=black!20]
  \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, 
                     draw=red!70, top color=white, bottom color=red!50!black!20]
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<2->[squeeze]
  \frametitle{} 
  
  \begin{columns}
  
  \begin{column}{0.8\textwidth}
  \begin{textblock}{0}(1,2)

  \begin{tikzpicture}
  \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]
  { \&[-10mm] 
    \node (def1)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&
    \node (proof1) [node1] {\large Proof}; \&
    \node (alg1)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\
    
    \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
    \onslide<4->{\node (def2)   [node2] {\large Spec$^\text{+ex}$};} \&
    \onslide<4->{\node (proof2) [node1] {\large Proof};} \&
    \onslide<4->{\node (alg2)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
     
    \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
    \onslide<5->{\node (def3)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
    \onslide<5->{\node (proof3) [node1] {\large Proof};} \&
    \onslide<5->{\node (alg3)   [node2] {\large Alg$^\text{-ex}$};} \\

    \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
    \onslide<6->{\node (def4)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
    \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \&
    \onslide<6->{\node (alg4)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
  };

  \draw[->,black!50,line width=2mm] (proof1) -- (def1);
  \draw[->,black!50,line width=2mm] (proof1) -- (alg1);
  
  \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);}
  \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);}

  \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);}
  \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);}
  
  \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);}
  \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);}

  \onslide<3->{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);} 
  \end{tikzpicture}

  \end{textblock}
  \end{column}
  \end{columns}


  \begin{textblock}{3}(12,3.6)
  \onslide<4->{
  \begin{tikzpicture}
  \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};
  \end{tikzpicture}}
  \end{textblock}

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

*}


(*<*)
atom_decl name

nominal_datatype lam = 
    Var "name"
  | App "lam" "lam"
  | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)

nominal_primrec
  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]")
where
  "(Var x)[y::=s] = (if x=y then s else (Var x))"
| "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
| "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: abs_fresh)
apply(fresh_guess)+
done

lemma  subst_eqvt[eqvt]:
  fixes pi::"name prm"
  shows "pi\<bullet>(t1[x::=t2]) = (pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)]"
by (nominal_induct t1 avoiding: x t2 rule: lam.strong_induct)
   (auto simp add: perm_bij fresh_atm fresh_bij)

lemma fresh_fact:
  fixes z::"name"
  shows "\<lbrakk>z\<sharp>s; (z=y \<or> z\<sharp>t)\<rbrakk> \<Longrightarrow> z\<sharp>t[y::=s]"
by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
   (auto simp add: abs_fresh fresh_prod fresh_atm)

lemma forget: 
  assumes asm: "x\<sharp>L"
  shows "L[x::=P] = L"
  using asm 
by (nominal_induct L avoiding: x P rule: lam.strong_induct)
   (auto simp add: abs_fresh fresh_atm)
(*>*)

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}

  \begin{textblock}{16}(1,1)
  \renewcommand{\isasymbullet}{$\cdot$}
  \tiny\color{black}
*}
lemma substitution_lemma_not_to_be_tried_at_home: 
  assumes asm: "x\<noteq>y" "x\<sharp>L"
  shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
using asm
proof (induct M arbitrary: x y N L rule: lam.induct)
  case (Lam z M1) 
  have ih: "\<And>x y N L. \<lbrakk>x\<noteq>y; x\<sharp>L\<rbrakk> \<Longrightarrow> M1[x::=N][y::=L] = M1[y::=L][x::=N[y::=L]]" by fact
  have "x\<noteq>y" by fact
  have "x\<sharp>L" by fact
  obtain z'::"name" where fc: "z'\<sharp>(x,y,z,M1,N,L)" by (rule exists_fresh) (auto simp add: fs_name1)
  have eq: "Lam [z'].([(z',z)]\<bullet>M1) = Lam [z].M1" using fc 
    by (auto simp add: lam.inject alpha fresh_prod fresh_atm)
  have fc': "z'\<sharp>N[y::=L]" using fc by (simp add: fresh_fact fresh_prod)
  have "([(z',z)]\<bullet>x) \<noteq> ([(z',z)]\<bullet>y)" using `x\<noteq>y` by (auto simp add: calc_atm)
  moreover
  have "([(z',z)]\<bullet>x)\<sharp>([(z',z)]\<bullet>L)" using `x\<sharp>L` by (simp add: fresh_bij)
  ultimately 
  have "M1[([(z',z)]\<bullet>x)::=([(z',z)]\<bullet>N)][([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)] 
        = M1[([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)][([(z',z)]\<bullet>x)::=([(z',z)]\<bullet>N)[([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)]]"
    using ih by simp
  then have "[(z',z)]\<bullet>(M1[([(z',z)]\<bullet>x)::=([(z',z)]\<bullet>N)][([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)] 
        = M1[([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)][([(z',z)]\<bullet>x)::=([(z',z)]\<bullet>N)[([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)]])"
    by (simp add: perm_bool)
  then have ih': "([(z',z)]\<bullet>M1)[x::=N][y::=L] = ([(z',z)]\<bullet>M1)[y::=L][x::=N[y::=L]]"
    by (simp add: eqvts perm_swap)
  show "(Lam [z].M1)[x::=N][y::=L] = (Lam [z].M1)[y::=L][x::=N[y::=L]]" (is "?LHS=?RHS") 
  proof - 
    have "?LHS = (Lam [z'].([(z',z)]\<bullet>M1))[x::=N][y::=L]" using eq by simp
    also have "\<dots> = Lam [z'].(([(z',z)]\<bullet>M1)[x::=N][y::=L])" using fc by (simp add: fresh_prod)
    also from ih have "\<dots> = Lam [z'].(([(z',z)]\<bullet>M1)[y::=L][x::=N[y::=L]])" sorry 
    also have "\<dots> = (Lam [z'].([(z',z)]\<bullet>M1))[y::=L][x::=N[y::=L]]" using fc fc' by (simp add: fresh_prod)
    also have "\<dots> = ?RHS" using eq by simp
    finally show "?LHS = ?RHS" .
  qed
qed (auto simp add: forget)
text_raw {*
  \end{textblock}
  \mbox{}

  \only<2->{
  \begin{textblock}{11.5}(4,2.3)
  \begin{minipage}{9.3cm}
  \begin{block}{}\footnotesize
*}
lemma substitution_lemma\<iota>:
  assumes asm: "x \<noteq> y" "x \<sharp> L"
  shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
  using asm
by (nominal_induct M avoiding: x y N L rule: lam.strong_induct)
     (auto simp add: forget fresh_fact)
text_raw {*  
  \end{block}
  \end{minipage}
  \end{textblock}}
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}


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

  \begin{textblock}{11.5}(1.2,5)
  \begin{minipage}{10.5cm}
  \begin{block}{}
  Theorem provers can keep large proofs and definitions consistent and
  make them modifiable.
   \end{block}
  \end{minipage}
  \end{textblock}

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

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}
  \frametitle{}

  \begin{textblock}{11.5}(0.8,2.3)
  \begin{minipage}{11.2cm}
  In most papers/books: 
  \begin{block}{}
  \color{darkgray}
  ``\ldots this necessary hygienic discipline is somewhat swept under the carpet via
  the so-called `{\bf variable convention}' \ldots
  The {\color{black}{\bf belief}} that this is {\bf sound} came from the calculus 
  with nameless binders in de Bruijn'' 
  \end{block}\medskip
  \end{minipage}
  \end{textblock}

  \begin{textblock}{11.5}(0.8,10)
  \includegraphics[scale=0.25]{LambdaBook.jpg}\hspace{-3mm}\includegraphics[scale=0.3]{barendregt.jpg}
  \end{textblock}
  \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->[c]
  \frametitle{Testing}

  \begin{itemize}
  \item We can only test a {\bf finite} amount of examples:\bigskip

  \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 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}. Not trivial, but after a bit 
  of thinking, one can prove that if

  \begin{center}
  \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1)})}\hspace{5mm}
  \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}[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
(*>*)