(*<*)

theory Slides6

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

begin

notation (latex output)

  set ("_") and

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

(*>*)

text_raw {*

  \renewcommand{\slidecaption}{London, 3 October 2013}

  \newcommand{\bl}[1]{\textcolor{blue}{#1}}                        

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

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

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}

  \frametitle{%

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

  \\[-3mm]

  \Large A Formalisation of the\\[-1mm] 

  \Large Myhill-Nerode Theorem using\\[-1mm] 

  \Large Regular Expressions only

  \end{tabular}}

  \begin{center}

   Christian Urban\\

  \small King's College London

  \end{center}\bigskip

  \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}<1->[c]

  \frametitle{}

  \mbox{}\\[2mm]

  \begin{itemize}

  \item my background is in: 

    \begin{itemize}

    \item \normalsize programming languages and 

    \item \normalsize theorem provers

    \end{itemize}\medskip

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

  \end{itemize}

  \begin{center}

  \begin{block}{}

  \color{gray}

  \footnotesize

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

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

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

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

  \end{block}

  \end{center}\pause

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

  \begin{itemize}

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

  about LF (and fixed it in three ways)

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{}

  \begin{itemize}

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

  (examined by Henk Barendregt and Andy Pitts)\bigskip

  \item formalised a classic OS scheduling algorithm (priority inversion 

  protocol)

    \begin{itemize}

    \item original algorithm was incorrect even being proved correct (with `pencil-and-paper') 

    \item helped us to implement this algorithm correctly and efficiently\\ 

    \end{itemize}\bigskip\pause

  \item used Isabelle to prove properties about access controls and OSes

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{}

  \begin{textblock}{12.9}(1.5,2.0)

  \begin{block}{}

  \begin{minipage}{12.4cm}\raggedright

  \large {\bf Motivation:}\\[2mm]I want to teach \alert{students} 

  theorem\\ provers (especially for inductions).

  \end{minipage}

  \end{block}

  \end{textblock}\pause

  \mbox{}\\[35mm]\mbox{}

  \begin{itemize}

  \item \only<2>{\smath{\text{fib}}, \smath{\text{even}} and \smath{\text{odd}}}%

        \only<3->{\sout{\smath{\text{fib}}, \smath{\text{even}} and \smath{\text{odd}}}}\medskip

  \item<3-> formal language theory \\

  \mbox{}\;\;@{text "\<Rightarrow>"} nice textbooks: Kozen, Hopcroft \& Ullman\ldots

  \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 \cdot r_2$}\\

           & \bl{$\mid$} & \bl{$r_1 + 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}

   \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

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

  \mbox{}\\[-2mm]

  \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\pause

  \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{if $nullable(r_1)$}\\

  & & \bl{then $(der\,c\,r_1) \cdot r_2 + der\, c\, r_2$}\\ 

  & & \bl{else $(der\, c\, r_1) \cdot r_2$}\\

  \bl{$der\,c\,(r^*)$}          & \bl{$=$} & \bl{$(der\,c\,r) \cdot r^*$} &\smallskip\\\pause

  \bl{$deriv\,[]\,r$}     & \bl{$=$} & \bl{$r$} & \\

  \bl{$deriv\,(c::s)\,r$} & \bl{$=$} & \bl{$deriv\,s\,(der\,c\,r)$} & \\

  \end{tabular}\medskip

  \bl{$match\,r\,s = nullable (deriv\,s\,r)$}

  \only<4>{

  \begin{textblock}{10.5}(2,5)

  \begin{tikzpicture}

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

{\normalsize\color{darkgray}

  \begin{minipage}{10.5cm}

  \begin{center}

  a)\;\; \bl{$nullable(r) \Leftrightarrow ""\in {\cal L}(r)$}\medskip

  \end{center}

  \begin{center}

  b)\;\; \bl{${\cal L}(der\,c\,r) = Der\,c\,({\cal L}(r))$}

  \end{center}

  where

  \begin{center}

  \bl{$Der\,c\,A \dn \{s\,|\, c\!::\!s \in A\}$}

  \end{center}\medskip\pause

  \begin{center}

  c)\;\; \bl{$match\,r\,s \Leftrightarrow s\in{\cal L}(r)$}

  \end{center}

  \end{minipage}};

  \end{tikzpicture}

  \end{textblock}}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[t]

\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}}

\mbox{}\\[-13mm]

\begin{tikzpicture}[y=.2cm, x=.3cm]

 	%axis

	\draw (0,0) -- coordinate (x axis mid) (30,0);

    	\draw (0,0) -- coordinate (y axis mid) (0,30);

    	%ticks

    	\foreach \x in {0,5,...,30}

     		\draw (\x,1pt) -- (\x,-3pt)

			node[anchor=north] {\x};

    	\foreach \y in {0,5,...,30}

     		\draw (1pt,\y) -- (-3pt,\y) 

     			node[anchor=east] {\y}; 

	%labels      

	\node[below=0.6cm] at (x axis mid) {\bl{a}s};

	\node[rotate=90, left=1.2cm] at (y axis mid) {secs};

	%plots

	\draw[color=blue] plot[mark=*, mark options={fill=white}] 

		file {re-python.data};

	\draw[color=brown] plot[mark=pentagon*, mark options={fill=white} ] 

		file {re-ruby.data};

	%legend

	\begin{scope}[shift={(4,20)}] 

	\draw[color=blue] (0,0) -- 

		plot[mark=*, mark options={fill=white}] (0.25,0) -- (0.5,0) 

		node[right]{\small Python};

	\draw[yshift=-\baselineskip, color=brown] (0,0) -- 

		plot[mark=pentagon*, mark options={fill=white}] (0.25,0) -- (0.5,0)

		node[right]{\small Ruby};

	\end{scope}

\end{tikzpicture}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

*}

text_raw {*

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[t]

\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}}

\mbox{}\\[-13mm]

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

\begin{tikzpicture}[y=.2cm, x=.01cm]

 	%axis

	\draw (0,0) -- coordinate (x axis mid) (1000,0);

    	\draw (0,0) -- coordinate (y axis mid) (0,30);

    	%ticks

    	\foreach \x in {0,200,...,1000}

     		\draw (\x,1pt) -- (\x,-3pt)

			node[anchor=north] {\x};

    	\foreach \y in {0,5,...,30}

     		\draw (1pt,\y) -- (-3pt,\y) 

     			node[anchor=east] {\y}; 

	%labels      

	\node[below=0.6cm] at (x axis mid) {\bl{a}s};

	\node[rotate=90, left=1.2cm] at (y axis mid) {secs};

	%plots

	\draw[color=blue] plot[mark=*, mark options={fill=white}] 

		file {re-python.data};

         \draw[color=green] plot[mark=square*, mark options={fill=white} ] 

		file {re2c.data};

         \draw[color=brown] plot[mark=pentagon*, mark options={fill=white} ] 

		file {re-ruby.data};

	%legend

	\begin{scope}[shift={(100,20)}] 

	\draw[color=blue] (0,0) -- 

		plot[mark=*, mark options={fill=white}] (0.25,0) -- (50,0) 

		node[right]{\small Python};

	\draw[yshift=-13, color=brown] (0,0) -- 

		plot[mark=pentagon*, mark options={fill=white}] (0.25,0) -- (50,0)

		node[right]{\small Ruby};

	\draw[yshift=13, color=green] (0,0) -- 

		plot[mark=square*, mark options={fill=white}] (0.25,0) -- (50,0)

		node[right]{\small nullable + der};	

	\end{scope}

\end{tikzpicture}

\end{tabular}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

*}

text_raw{*

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[t]

\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}}

\mbox{}\\[-9mm]

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

\begin{tikzpicture}[y=.2cm, x=.0008cm]

 	%axis

	\draw (0,0) -- coordinate (x axis mid) (12000,0);

    	\draw (0,0) -- coordinate (y axis mid) (0,30);

    	%ticks

    	\foreach \x in {0,2000,...,12000}

     		\draw (\x,1pt) -- (\x,-3pt)

			node[anchor=north] {\x};

    	\foreach \y in {0,5,...,30}

     		\draw (1pt,\y) -- (-3pt,\y) 

     			node[anchor=east] {\y}; 

	%labels      

	\node[below=0.6cm] at (x axis mid) {\bl{a}s};

	\node[rotate=90, left=1.2cm] at (y axis mid) {secs};

	%plots

         \draw[color=green] plot[mark=square*, mark options={fill=white} ] 

		file {re2b.data};

	\draw[color=black] plot[mark=square*, mark options={fill=white} ] 

		file {re3.data};	 

        \draw[color=blue] plot[mark=*, mark options={fill=white}] 

		file {re-python.data};

         \draw[color=brown] plot[mark=pentagon*, mark options={fill=white} ] 

		file {re-ruby.data};

	%legend

	\begin{scope}[shift={(2000,20)}] 

        \draw[color=blue] (0,0) -- 

		plot[mark=*, mark options={fill=white}] (0.25,0) -- (50,0) 

		node[right]{\small Python};

	\draw[yshift=-13, color=brown] (0,0) -- 

		plot[mark=pentagon*, mark options={fill=white}] (0.25,0) -- (50,0)

		node[right]{\small Ruby};

	\draw[yshift=13, color=green] (0,0) -- 

		plot[mark=square*, mark options={fill=white}] (0.25,0) -- (50,0)

		node[right]{\small nullable + der};	

	\draw[yshift=26, color=black] (0,0) -- 

		plot[mark=square*, mark options={fill=white}] (0.25,0) -- (50,0)

		node[right]{\small nullable + der + simplification};	

	\end{scope}

\end{tikzpicture}

\end{tabular}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[t]

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

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

  \begin{center}

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

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

  \end{center}

  \begin{itemize}

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

  \item<2-> combining automata / graphs

  \onslide<2->{

  \begin{center}

  \begin{tabular}{ccc}

  \begin{tikzpicture}[scale=1]

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

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

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

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

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

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

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

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

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

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

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

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

  \end{tikzpicture}}

  & 

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

  &

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  \end{tikzpicture}}

  \end{tabular}

  \end{center}\medskip

  \only<4-5>{

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

  disjoint union:\\[2mm]

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

  \end{tabular}}

  \end{itemize}

  \only<5>{

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

  \begin{block}{}

  \medskip

  \begin{minipage}{14cm}\raggedright

  Already problems with defining regularity:\bigskip\\

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

  \end{minipage}

  \end{block}

  \end{textblock}}

  \medskip

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

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

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[t]

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

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

  \begin{center}

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

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

  \end{center}

  \begin{itemize}

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

  requires absence of \alert{inaccessible states}

  \item complementation of automata only works for \alert{complete} automata

  (need sink states)\medskip

  \end{itemize}\bigskip\bigskip

  \begin{center}

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

  \end{center}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{