1 (*<*)

     2 theory Slides6

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

     4 begin

     5 

     6 declare [[show_question_marks = false]]

     7 

     8 notation (latex output)

     9   set ("_") and

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

    11 

    12 (*>*)

    13 

    14 text_raw {*

    15   \renewcommand{\slidecaption}{Hefei, 15.~April 2011}

    16 

    17   \newcommand{\abst}[2]{#1.#2}% atom-abstraction

    18   \newcommand{\pair}[2]{\langle #1,#2\rangle} % pairing

    19   \newcommand{\susp}{{\boldsymbol{\cdot}}}% for suspensions

    20   \newcommand{\unit}{\langle\rangle}% unit

    21   \newcommand{\app}[2]{#1\,#2}% application

    22   \newcommand{\eqprob}{\mathrel{{\approx}?}}

    23   \newcommand{\freshprob}{\mathrel{\#?}}

    24   \newcommand{\redu}[1]{\stackrel{#1}{\Longrightarrow}}% reduction

    25   \newcommand{\id}{\varepsilon}% identity substitution

    26   

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

    28   \newcommand{\gr}[1]{\textcolor{gray}{#1}}

    29   \newcommand{\rd}[1]{\textcolor{red}{#1}}

    30 

    31   \newcommand{\ok}{\includegraphics[scale=0.07]{ok.png}}

    32   \newcommand{\notok}{\includegraphics[scale=0.07]{notok.png}}

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

    34 

    35   \renewcommand{\Huge}{\fontsize{61.92}{77}\selectfont}

    36   \newcommand{\veryHuge}{\fontsize{74.3}{93}\selectfont}

    37   \newcommand{\VeryHuge}{\fontsize{89.16}{112}\selectfont}

    38   \newcommand{\VERYHuge}{\fontsize{107}{134}\selectfont}

    39 

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

    41 

    42 

    43   \pgfdeclareradialshading{smallbluesphere}{\pgfpoint{0.5mm}{0.5mm}}%

    44   {rgb(0mm)=(0,0,0.9);

    45   rgb(0.9mm)=(0,0,0.7);

    46   rgb(1.3mm)=(0,0,0.5);

    47   rgb(1.4mm)=(1,1,1)}

    48 

    49   \def\myitemi{\begin{pgfpicture}{-1ex}{-0.55ex}{1ex}{1ex}

    50     \usebeamercolor[fg]{subitem projected}

    51     {\pgftransformscale{0.8}\pgftext{\normalsize\pgfuseshading{bigsphere}}}

    52     \pgftext{%

    53       \usebeamerfont*{subitem projected}}

    54   \end{pgfpicture}}

    55 

    56   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    57   \mode<presentation>{

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

    59   \frametitle{%

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

    61   \\

    62   \LARGE Verifying a Regular Expression\\[-1mm] 

    63   \LARGE Matcher and Formal Language\\[-1mm]

    64   \LARGE Theory\\[5mm]

    65   \end{tabular}}

    66   \begin{center}

    67   Christian Urban\\

    68   \small Technical University of Munich, Germany

    69   \end{center}

    70 

    71 

    72   \begin{center}

    73   \small joint work with Chunhan Wu and Xingyuan Zhang from the PLA

    74   University of Science and Technology in Nanjing

    75   \end{center}

    76   \end{frame}}

    77   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    78 

    79 *}

    80 

    81 

    82 text_raw {*

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

    84   \mode<presentation>{

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

    86   \frametitle{My Background}

    87 

    88   \mbox{}\\[-10mm]

    89   \begin{itemize}

    90   \item My background is in theory and programming languages.\bigskip

    91   \pause

    92 

    93   \item But I am also a programmer with a \alert<2>{software system} of around 800 kloc 

    94   (though I am responsible for only appr.~35 kloc),

    95 

    96   \item and I write papers.

    97   \end{itemize}

    98   

    99   \only<2>{

   100   \begin{textblock}{6}(6.5,11.5)

   101   \begin{tikzpicture}

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

   103   {\color{darkgray}

   104   \begin{minipage}{6.5cm}\raggedright

   105   \begin{tabular}[b]{@ {}p{4.5cm}c@ {}}

   106   \raggedright

   107   The software is a theorem prover, called {\bf Isabelle}. 

   108   & \mbox{}\hspace{-5mm}\raisebox{-14mm}{\includegraphics[scale=0.28]{isabelle1.png}}

   109   \end{tabular}%

   110   \end{minipage}};

   111   \end{tikzpicture}

   112   \end{textblock}}

   113   

   114   \only<4>{

   115   \begin{textblock}{6}(3,11.5)

   116   \begin{tikzpicture}

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

   118   {\color{darkgray}

   119   \begin{minipage}{9.6cm}\raggedright

   120   So I can experience every day that writing error-free code is {\bf very, very hard}

   121   and that papers are also {\bf hard} to get correct.

   122   \end{minipage}};

   123   \end{tikzpicture}

   124   \end{textblock}}

   125 

   126   \end{frame}}

   127   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   128 *}

   129 

   130 

   131 text_raw {*

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

   133   \mode<presentation>{

   134   \begin{frame}[c]

   135   \frametitle{3 Points}

   136   \large

   137   \begin{itemize}

   138   \item It is easy to make mistakes.\bigskip

   139   \item Theorem provers can prevent mistakes, {\bf if} the problem

   140   is formulated so that it is suitable for theorem provers.\bigskip

   141   \item This re-formulation can be done, even in domains where

   142   we do not expect it.

   143   \end{itemize}

   144 

   145   \end{frame}}

   146   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   147 *}

   148 

   149 text_raw {*

   150 

   151   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   152   \mode<presentation>{

   153   \begin{frame}

   154   \frametitle{Getting Papers Correct}

   155 

   156   \begin{minipage}{1.1\textwidth}

   157   My work over the last 5 years.\\

   158   {\small (in the fields of programming languages, logic and lambda-calculi)}

   159   \end{minipage}\bigskip

   160 

   161   \only<1>{

   162   \mbox{}\\[15mm]

   163   \begin{center}

   164   \begin{tikzpicture}[node distance=0.5mm]

   165   \node at (-1.0,-0.3) (proof) [double arrow, fill=gray,text=white, minimum height=2cm]{\bf Proof};

   166   \node [left=of proof]{\Large\bf Specification};

   167   \node [right=of proof]{\Large\bf Code};

   168   \end{tikzpicture}

   169   \end{center}

   170   }

   171   \pause

   172 

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

   174   \begin{tabular}{c}

   175   \includegraphics[scale=0.09]{harper.jpg}\\[-2mm]

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

   177   {\footnotesize (CMU)}

   178   \end{tabular}

   179   \begin{tabular}{c}

   180   \includegraphics[scale=0.31]{pfenning.jpg}\\[-2mm]

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

   182   {\footnotesize (CMU)}

   183   \end{tabular} &

   184 

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

   186   \raggedright\small

   187   \color{gray}{published a proof in ACM Transactions on Computational Logic (2005),

   188   $\sim$31pp}

   189   \end{tabular}\\

   190 

   191   \\[-4mm]

   192   

   193   \begin{tabular}{c}

   194   \includegraphics[scale=0.3]{appel.jpg}\\[-2mm] 

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

   196   {\footnotesize (Princeton)}

   197   \end{tabular} &

   198 

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

   200   \raggedright\small

   201   \color{gray}{relied on their proof in a safety critical system (proof carrying code)}

   202   \end{tabular}

   203 

   204   \end{tabular}\medskip

   205 

   206   \end{frame}}

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

   208 

   209 *}

   210 

   211 

   212 text_raw {*

   213 

   214   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   215   \mode<presentation>{

   216   \begin{frame}

   217   \frametitle{Proof-Carrying Code}

   218 

   219   \begin{textblock}{10}(2.5,2.2)

   220   \begin{block}{Idea:}

   221   \begin{center}

   222   \begin{tikzpicture}

   223   \draw[help lines,cream] (0,0.2) grid (8,4);

   224   

   225   \draw[line width=1mm, red] (5.5,0.6) rectangle (7.5,4);

   226   \node[anchor=base] at (6.5,2.8) 

   227      {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering  user needs to run untrusted code\end{tabular}};

   228 

   229   \draw[line width=1mm, red] (0.5,0.6) rectangle (2.5,4);

   230   \node[anchor=base] at (1.5,2.3) 

   231      {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering  code developer/ web server/ Apple 

   232   Store\end{tabular}};

   233   

   234   \onslide<4->{

   235   \draw[line width=1mm, red, fill=red] (5.5,0.6) rectangle (7.5,1.8);

   236   \node[anchor=base,white] at (6.5,1.1) 

   237      {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\bf\centering proof- checker\end{tabular}};}

   238 

   239   \node at (3.8,3.0) [single arrow, fill=red,text=white, minimum height=3cm]{\bf code};

   240   \onslide<3->{

   241   \node at (3.8,1.3) [single arrow, fill=red,text=white, minimum height=3cm]{\bf LF proof};

   242   \node at (3.8,1.9) {\small certificate};

   243   }

   244 

   245   \onslide<2>{\node at (4.0,1.3) [text=red]{\begin{tabular}{c}\bf Highly\\\bf Dangerous!\end{tabular}};}

   246   

   247   \end{tikzpicture}

   248   \end{center}

   249   \end{block}

   250   \end{textblock}

   251 

   252   \begin{textblock}{15}(2,12)

   253   \small

   254   \begin{itemize}

   255   \item<4-> Appel's checker is $\sim$2700 lines of code (1865 loc of\\ LF definitions; 

   256   803 loc in C including 2 library functions)\\[-3mm]

   257   \item<5-> 167 loc in C implement a type-checker

   258   \end{itemize}

   259   \end{textblock}

   260 

   261   \end{frame}}

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

   263 

   264 *}

   265 

   266 text {*

   267   \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]

   268   \tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick, 

   269                      draw=black!50, top color=white, bottom color=black!20]

   270   \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, 

   271                      draw=red!70, top color=white, bottom color=red!50!black!20]

   272   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   273   \mode<presentation>{

   274   \begin{frame}<2->[squeeze]

   275   \frametitle{Type-Checking in LF} 

   276   

   277   \begin{columns}

   278   

   279   \begin{column}{0.8\textwidth}

   280   \begin{textblock}{0}(1,2)

   281 

   282   \begin{tikzpicture}

   283   \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]

   284   { \&[-10mm] 

   285     \node (def1)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&

   286     \node (proof1) [node1] {\large Proof}; \&

   287     \node (alg1)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\

   288     

   289     \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \&

   290     \onslide<4->{\node (def2)   [node2] {\large Spec$^\text{+ex}$};} \&

   291     \onslide<4->{\node (proof2) [node1] {\large Proof};} \&

   292     \onslide<4->{\node (alg2)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\

   293      

   294     \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&

   295     \onslide<5->{\node (def3)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&

   296     \onslide<5->{\node (proof3) [node1] {\large Proof};} \&

   297     \onslide<5->{\node (alg3)   [node2] {\large Alg$^\text{-ex}$};} \\

   298 

   299     \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&

   300     \onslide<6->{\node (def4)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&

   301     \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \&

   302     \onslide<6->{\node (alg4)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\

   303   };

   304 

   305   \draw[->,black!50,line width=2mm] (proof1) -- (def1);

   306   \draw[->,black!50,line width=2mm] (proof1) -- (alg1);

   307   

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

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

   310 

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

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

   313   

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

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

   316 

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

   318   \end{tikzpicture}

   319 

   320   \end{textblock}

   321   \end{column}

   322   \end{columns}

   323 

   324 

   325   \begin{textblock}{3}(12,3.6)

   326   \onslide<4->{

   327   \begin{tikzpicture}

   328   \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};

   329   \end{tikzpicture}}

   330   \end{textblock}

   331 

   332   \only<7->{

   333   \begin{textblock}{14}(0.6,12.8)

   334   \begin{block}{}

   335   \small Each time one needs to check $\sim$31pp~of informal paper proofs.

   336   You have to be able to keep definitions and proofs consistent.

   337   \end{block}

   338   \end{textblock}}

   339 

   340   \end{frame}}

   341   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   342 

   343 *}

   344 

   345 

   346 text_raw {*

   347   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   348   \mode<presentation>{

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

   350   \frametitle{Lessons Learned}

   351 

   352   \begin{itemize}

   353   \item Theorem provers help with keeping large proofs consistent;

   354   make them modifiable.\medskip

   355   

   356   \item They can ensure that all cases are covered.\medskip

   357 

   358   \item Some reasoning can be automated. 

   359   \end{itemize}\bigskip\pause

   360 

   361   \begin{minipage}{1.1\textwidth}

   362   Formal reasoning needs to be ``smooth''.\\

   363   {\small (ideally as close as possible to reasoning with ``pen-and-paper'')}

   364   \end{minipage}

   365 

   366   \only<2->{

   367   \begin{textblock}{3}(0.1,9.9)

   368   \begin{tikzpicture}

   369   \node at (0,0) [single arrow, shape border rotate=0, fill=red,text=red]{a};

   370   \end{tikzpicture}

   371   \end{textblock}}

   372 

   373   

   374   \end{frame}}

   375   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   376 *}

   377 

   378 

   379 (*<*)

   380 atom_decl name

   381 

   382 nominal_datatype lam = 

   383     Var "name"

   384   | App "lam" "lam"

   385   | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)

   386 

   387 nominal_primrec

   388   subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]")

   389 where

   390   "(Var x)[y::=s] = (if x=y then s else (Var x))"

   391 | "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"

   392 | "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"

   393 apply(finite_guess)+

   394 apply(rule TrueI)+

   395 apply(simp add: abs_fresh)

   396 apply(fresh_guess)+

   397 done

   398 

   399 lemma  subst_eqvt[eqvt]:

   400   fixes pi::"name prm"

   401   shows "pi\<bullet>(t1[x::=t2]) = (pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)]"

   402 by (nominal_induct t1 avoiding: x t2 rule: lam.strong_induct)

   403    (auto simp add: perm_bij fresh_atm fresh_bij)

   404 

   405 lemma fresh_fact:

   406   fixes z::"name"

   407   shows "\<lbrakk>z\<sharp>s; (z=y \<or> z\<sharp>t)\<rbrakk> \<Longrightarrow> z\<sharp>t[y::=s]"

   408 by (nominal_induct t avoiding: z y s rule: lam.strong_induct)

   409    (auto simp add: abs_fresh fresh_prod fresh_atm)

   410 

   411 lemma forget: 

   412   assumes asm: "x\<sharp>L"

   413   shows "L[x::=P] = L"

   414   using asm 

   415 by (nominal_induct L avoiding: x P rule: lam.strong_induct)

   416    (auto simp add: abs_fresh fresh_atm)

   417 (*>*)

   418 

   419 text_raw {*

   420   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   421   \mode<presentation>{

   422   \begin{frame}

   423 

   424   \begin{textblock}{16}(1,1)

   425   \renewcommand{\isasymbullet}{$\cdot$}

   426   \tiny\color{black}

   427 *}

   428 lemma substitution_lemma_not_to_be_tried_at_home: 

   429   assumes asm: "x\<noteq>y" "x\<sharp>L"

   430   shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"

   431 using asm

   432 proof (induct M arbitrary: x y N L rule: lam.induct)

   433   case (Lam z M1) 

   434   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

   435   have "x\<noteq>y" by fact

   436   have "x\<sharp>L" by fact

   437   obtain z'::"name" where fc: "z'\<sharp>(x,y,z,M1,N,L)" by (rule exists_fresh) (auto simp add: fs_name1)

   438   have eq: "Lam [z'].([(z',z)]\<bullet>M1) = Lam [z].M1" using fc 

   439     by (auto simp add: lam.inject alpha fresh_prod fresh_atm)

   440   have fc': "z'\<sharp>N[y::=L]" using fc by (simp add: fresh_fact fresh_prod)

   441   have "([(z',z)]\<bullet>x) \<noteq> ([(z',z)]\<bullet>y)" using `x\<noteq>y` by (auto simp add: calc_atm)

   442   moreover

   443   have "([(z',z)]\<bullet>x)\<sharp>([(z',z)]\<bullet>L)" using `x\<sharp>L` by (simp add: fresh_bij)

   444   ultimately 

   445   have "M1[([(z',z)]\<bullet>x)::=([(z',z)]\<bullet>N)][([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)] 

   446         = 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)]]"

   447     using ih by simp

   448   then have "[(z',z)]\<bullet>(M1[([(z',z)]\<bullet>x)::=([(z',z)]\<bullet>N)][([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)] 

   449         = 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)]])"

   450     by (simp add: perm_bool)

   451   then have ih': "([(z',z)]\<bullet>M1)[x::=N][y::=L] = ([(z',z)]\<bullet>M1)[y::=L][x::=N[y::=L]]"

   452     by (simp add: eqvts perm_swap)

   453   show "(Lam [z].M1)[x::=N][y::=L] = (Lam [z].M1)[y::=L][x::=N[y::=L]]" (is "?LHS=?RHS") 

   454   proof - 

   455     have "?LHS = (Lam [z'].([(z',z)]\<bullet>M1))[x::=N][y::=L]" using eq by simp

   456     also have "\<dots> = Lam [z'].(([(z',z)]\<bullet>M1)[x::=N][y::=L])" using fc by (simp add: fresh_prod)

   457     also from ih have "\<dots> = Lam [z'].(([(z',z)]\<bullet>M1)[y::=L][x::=N[y::=L]])" sorry 

   458     also have "\<dots> = (Lam [z'].([(z',z)]\<bullet>M1))[y::=L][x::=N[y::=L]]" using fc fc' by (simp add: fresh_prod)

   459     also have "\<dots> = ?RHS" using eq by simp

   460     finally show "?LHS = ?RHS" .

   461   qed

   462 qed (auto simp add: forget)

   463 text_raw {*

   464   \end{textblock}

   465   \mbox{}

   466 

   467   \only<2->{

   468   \begin{textblock}{11.5}(4,2.3)

   469   \begin{minipage}{9.3cm}

   470   \begin{block}{}\footnotesize

   471 *}

   472 lemma substitution_lemma\<iota>:

   473   assumes asm: "x \<noteq> y" "x \<sharp> L"

   474   shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"

   475   using asm

   476 by (nominal_induct M avoiding: x y N L rule: lam.strong_induct)

   477      (auto simp add: forget fresh_fact)

   478 text_raw {*  

   479   \end{block}

   480   \end{minipage}

   481   \end{textblock}}

   482   \end{frame}}

   483   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   484 *}

   485 

   486 text_raw {*

   487   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   488   \mode<presentation>{

   489   \begin{frame}<1>[c]

   490   \frametitle{Getting Programs Correct}

   491 

   492   \begin{center}

   493   \begin{tikzpicture}[node distance=0.5mm]

   494   \node at (-1.0,-0.3) (proof) [double arrow, fill=gray,text=white, minimum height=2cm]{\bf Proof};

   495   \node [left=of proof]{\Large\bf Specification};

   496   \node [right=of proof]{\Large\bf Code};

   497   \end{tikzpicture}

   498   \end{center}

   499 

   500 

   501 

   502   \end{frame}}

   503   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   504 *}

   505 

   506 text_raw {*

   507   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   508   \mode<presentation>{

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

   510   \frametitle{Regular Expressions}

   511 

   512   \begin{textblock}{6}(2,4)

   513   \begin{tabular}{@ {}rrl}

   514   \bl{r} & \bl{$::=$}  & \bl{$\varnothing$}\\

   515          & \bl{$\mid$} & \bl{[]}\\

   516          & \bl{$\mid$} & \bl{c}\\

   517          & \bl{$\mid$} & \bl{r$_1$ + r$_2$}\\

   518          & \bl{$\mid$} & \bl{r$_1$ $\cdot$ r$_2$}\\

   519          & \bl{$\mid$} & \bl{r$^*$}\\

   520   \end{tabular}

   521   \end{textblock}

   522 

   523   \begin{textblock}{6}(8,3.5)

   524   \includegraphics[scale=0.35]{Screen1.png}

   525   \end{textblock}

   526 

   527   \begin{textblock}{6}(10.2,2.8)

   528   \footnotesize Isabelle:

   529   \end{textblock}

   530   

   531   \only<2>{

   532   \begin{textblock}{9}(3.6,11.8)

   533   \bl{matches r s $\;\Longrightarrow\;$ true $\vee$ false}\\[3.5mm]

   534 

   535   \hspace{10mm}\begin{tikzpicture}

   536   \coordinate (m1) at (0.4,1);

   537   \draw (0,0.3) node (m2) {\small\color{gray}rexp};

   538   \path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (m2) edge (m1);

   539   

   540   \coordinate (s1) at (0.81,1);

   541   \draw (1.3,0.3) node (s2) {\small\color{gray} string};

   542   \path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (s2) edge (s1);

   543   \end{tikzpicture}

   544   \end{textblock}}

   545 

   546 

   547 

   548   \end{frame}}

   549   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   550 *}

   551 

   552 text_raw {*

   553   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   554   \mode<presentation>{

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

   556   \frametitle{Specification}

   557 

   558   \small

   559   \begin{textblock}{6}(0,3.5)

   560   \begin{tabular}{r@ {\hspace{0.5mm}}r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}

   561   \multicolumn{4}{c}{rexp $\Rightarrow$ set of strings}\bigskip\\

   562   &\bl{\LL ($\varnothing$)}   & \bl{$\dn$} & \bl{$\varnothing$}\\

   563   &\bl{\LL ([])}              & \bl{$\dn$} & \bl{\{[]\}}\\

   564   &\bl{\LL (c)}               & \bl{$\dn$} & \bl{\{c\}}\\

   565   &\bl{\LL (r$_1$ + r$_2$)}   & \bl{$\dn$} & \bl{\LL (r$_1$) $\cup$ \LL (r$_2$)}\\

   566   \rd{$\Rightarrow$} &\bl{\LL (r$_1$ $\cdot$ r$_2$)} & \bl{$\dn$} & \bl{\LL (r$_1$) ;; \LL (r$_2$)}\\

   567   \rd{$\Rightarrow$} &\bl{\LL (r$^*$)}           & \bl{$\dn$} & \bl{(\LL (r))$^\star$}\\

   568   \end{tabular}

   569   \end{textblock}

   570 

   571   \begin{textblock}{9}(7.3,3)

   572   {\mbox{}\hspace{2cm}\footnotesize Isabelle:\smallskip}

   573   \includegraphics[scale=0.325]{Screen3.png}

   574   \end{textblock}

   575 

   576   \end{frame}}

   577   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   578 *}

   579 

   580 

   581 text_raw {*

   582   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   583   \mode<presentation>{

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

   585   \frametitle{Version 1}

   586   \small

   587   \mbox{}\\[-8mm]\mbox{}

   588 

   589   \begin{center}\def\arraystretch{1.05}

   590   \begin{tabular}{@ {\hspace{-5mm}}l@ {\hspace{2.5mm}}c@ {\hspace{2.5mm}}l@ {}}

   591   \bl{match [] []}                   & \bl{$=$} & \bl{true}\\

   592   \bl{match [] (c::s)}               & \bl{$=$} & \bl{false}\\

   593   \bl{match ($\varnothing$::rs) s}   & \bl{$=$} & \bl{false}\\

   594   \bl{match ([]::rs) s}              & \bl{$=$} & \bl{match rs s}\\

   595   \bl{match (c::rs) []}              & \bl{$=$} & \bl{false}\\

   596   \bl{match (c::rs) (d::s)}          & \bl{$=$} & \bl{if c = d then match rs s else false}\\     

   597   \bl{match (r$_1$ + r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::rs) s $\vee$ match (r$_2$::rs) s}\\ 

   598   \bl{match (r$_1$ $\cdot$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::r$_2$::rs) s}\\

   599   \bl{match (r$^*$::rs) s}          & \bl{$=$} & \bl{match rs s $\vee$ match (r::r$^*$::rs) s}\\

   600   \end{tabular}

   601   \end{center}

   602 

   603   \begin{textblock}{9}(0.2,1.6)

   604   \hspace{10mm}\begin{tikzpicture}

   605   \coordinate (m1) at (0.44,-0.5);

   606   \draw (0,0.3) node (m2) {\small\color{gray}\mbox{}\hspace{-9mm}list of rexps};

   607   \path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (m2) edge (m1);

   608   

   609   \coordinate (s1) at (0.86,-0.5);

   610   \draw (1.5,0.3) node (s2) {\small\color{gray} string};

   611   \path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (s2) edge (s1);

   612   \end{tikzpicture}

   613   \end{textblock}

   614 

   615   \begin{textblock}{9}(2.8,11.8)

   616   \bl{matches$_1$ r s $\;=\;$ match [r] s}

   617   \end{textblock}

   618 

   619   \end{frame}}

   620   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   621 *}

   622 

   623 text_raw {*

   624   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   625   \mode<presentation>{

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

   627   \frametitle{Testing}

   628   

   629   \small

   630   Every good programmer should do thourough tests: 

   631 

   632   \begin{center}

   633   \begin{tabular}{@ {\hspace{-20mm}}lcl}

   634   \bl{matches (a$\cdot$b)$^*\;$ []}     & \bl{$\mapsto$} & \bl{true}\\

   635   \bl{matches (a$\cdot$b)$^*\;$ ab}   & \bl{$\mapsto$} & \bl{true}\\ 

   636   \bl{matches (a$\cdot$b)$^*\;$ aba}  & \bl{$\mapsto$} & \bl{false}\\

   637   \bl{matches (a$\cdot$b)$^*\;$ abab} & \bl{$\mapsto$} & \bl{true}\\ 

   638   \bl{matches (a$\cdot$b)$^*\;$ abaa} & \bl{$\mapsto$} & \bl{false}\medskip\\

   639   \onslide<2->{\bl{matches x$\cdot$(0$|$1)$^*\;$ x}   & \bl{$\mapsto$} & \bl{true}}\\

   640   \onslide<2->{\bl{matches x$\cdot$(0$|$1)$^*\;$ x0}  & \bl{$\mapsto$} & \bl{true}}\\

   641   \onslide<2->{\bl{matches x$\cdot$(0$|$1)$^*\;$ x3}  & \bl{$\mapsto$} & \bl{false}}

   642   \end{tabular}

   643   \end{center}

   644  

   645   \onslide<3->

   646   {looks OK \ldots let's ship it to customers\hspace{5mm} 

   647    \raisebox{-5mm}{\includegraphics[scale=0.05]{sun.png}}}

   648   

   649   \end{frame}}

   650   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   651 *}

   652 

   653 text_raw {*

   654   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   655   \mode<presentation>{

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

   657   \frametitle{Version 1}

   658 

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

   660 

   661 

   662   \begin{center}

   663   \begin{tabular}{@ {\hspace{0mm}}lcl}

   664   \bl{matches$_1$ []$^*$ s}     & \bl{$\mapsto$} & loops\\

   665   \onslide<4->{\bl{matches$_1$ ([] + \ldots)$^*$ s}   & \bl{$\mapsto$} & loops\\} 

   666   \end{tabular}

   667   \end{center}

   668 

   669   \small

   670   \onslide<3->{

   671   \begin{center}

   672   \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}

   673   \ldots\\

   674   \bl{match ([]::rs) s}           & \bl{$=$} & \bl{match rs s}\\

   675   \ldots\\

   676   \bl{match (r$^*$::rs) s}        & \bl{$=$} & \bl{match rs s $\vee$ match (r::r$^*$::rs) s}\\

   677   \end{tabular}

   678   \end{center}}

   679   

   680 

   681   \end{frame}}

   682   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   683 *}

   684 

   685 

   686 text_raw {*

   687   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   688   \mode<presentation>{

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

   690   \frametitle{Testing}

   691 

   692   \begin{itemize}

   693   \item While testing is an important part in the process of programming development\pause

   694 

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

   696 

   697   \begin{center}

   698   \colorbox{cream}

   699   {\gr{\begin{minipage}{10cm}

   700   ``Testing can only show the presence of errors, never their

   701   absence'' (Edsger W.~Dijkstra)

   702   \end{minipage}}}

   703   \end{center}\bigskip\pause

   704 

   705   \item In a theorem prover we can establish properties that apply to 

   706   {\bf all} input and {\bf all} output.\pause 

   707 

   708   \end{itemize}

   709 

   710   \end{frame}}

   711   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   712 *}

   713 

   714 

   715 text_raw {*

   716   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   717   \mode<presentation>{

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

   719   \frametitle{Version 2}

   720   \mbox{}\\[-14mm]\mbox{}

   721 

   722   \small

   723   \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}}

   724   \bl{nullable ($\varnothing$)}   & \bl{$=$} & \bl{false} &\\

   725   \bl{nullable ([])}              & \bl{$=$} & \bl{true}  &\\

   726   \bl{nullable (c)}               & \bl{$=$} & \bl{false} &\\

   727   \bl{nullable (r$_1$ + r$_2$)}   & \bl{$=$} & \bl{nullable r$_1$ $\vee$ nullable r$_2$} & \\ 

   728   \bl{nullable (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{nullable r$_1$ $\wedge$ nullable r$_2$} & \\

   729   \bl{nullable (r$^*$)}           & \bl{$=$} & \bl{true} & \\

   730   \end{tabular}\medskip

   731 

   732   \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}

   733   \bl{der c ($\varnothing$)}       & \bl{$=$} & \bl{$\varnothing$} & \\

   734   \bl{der c ([])}                  & \bl{$=$} & \bl{$\varnothing$} & \\

   735   \bl{der c (d)}                   & \bl{$=$} & \bl{if c = d then [] else $\varnothing$} & \\

   736   \bl{der c (r$_1$ + r$_2$)}       & \bl{$=$} & \bl{(der c r$_1$) + (der c r$_2$)} & \\

   737   \bl{der c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{((der c r$_1$) $\cdot$ r$_2$)} & \\

   738        &          & \bl{\;\;+ (if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\

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

   740 

   741   \bl{derivative r []}     & \bl{$=$} & \bl{r} & \\

   742   \bl{derivative r (c::s)} & \bl{$=$} & \bl{derivative (der c r) s} & \\

   743   \end{tabular}\medskip

   744 

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

   746 

   747   \begin{textblock}{6}(9.5,0.9)

   748   \begin{flushright}

   749   \color{gray}``if r matches []'' 

   750   \end{flushright}

   751   \end{textblock}

   752 

   753   \begin{textblock}{6}(9.5,6.18)

   754   \begin{flushright}

   755   \color{gray}``derivative w.r.t.~a char'' 

   756   \end{flushright}

   757   \end{textblock}

   758 

   759   \begin{textblock}{6}(9.5,12.1)

   760   \begin{flushright}

   761   \color{gray}``deriv.~w.r.t.~a string'' 

   762   \end{flushright}

   763   \end{textblock}

   764 

   765   \begin{textblock}{6}(9.5,13.98)

   766   \begin{flushright}

   767   \color{gray}``main'' 

   768   \end{flushright}

   769   \end{textblock}

   770 

   771   \end{frame}}

   772   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   773 *}

   774 

   775 text_raw {*

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

   777   \mode<presentation>{

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

   779   \frametitle{Is the Matcher Error-Free?}

   780 

   781   We expect that

   782 

   783   \begin{center}

   784   \begin{tabular}{lcl}

   785   \bl{matches$_2$ r s = true}  & \only<1>{\rd{$\Longrightarrow\,\,$}}\only<2>{\rd{$\Longleftarrow\,\,$}}% 

   786   \only<3->{\rd{$\Longleftrightarrow$}} & \bl{s $\in$ \LL(r)}\\

   787   \bl{matches$_2$ r s = false} & \only<1>{\rd{$\Longrightarrow\,\,$}}\only<2>{\rd{$\Longleftarrow\,\,$}}%

   788   \only<3->{\rd{$\Longleftrightarrow$}} & \bl{s $\notin$ \LL(r)}\\

   789   \end{tabular}

   790   \end{center}

   791   \pause\pause\bigskip

   792   By \alert<4->{induction}, we can {\bf prove} these properties.\bigskip

   793 

   794   \begin{tabular}{lrcl}

   795   Lemmas:  & \bl{nullable (r)}          & \bl{$\Longleftrightarrow$} & \bl{[] $\in$ \LL (r)}\\

   796            & \bl{s $\in$ \LL (der c r)} & \bl{$\Longleftrightarrow$} & \bl{(c::s) $\in$ \LL (r)}\\

   797   \end{tabular}

   798   

   799   \only<4->{

   800   \begin{textblock}{3}(0.9,4.5)

   801   \rd{\huge$\forall$\large{}r s.}

   802   \end{textblock}}

   803   \end{frame}}

   804   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   805 *}

   806 

   807 text_raw {*

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

   809   \mode<presentation>{

   810   \begin{frame}<1>[c]

   811   \frametitle{

   812   \begin{tabular}{c}

   813   \mbox{}\\[23mm]

   814   \LARGE Demo

   815   \end{tabular}}

   816   

   817   \end{frame}}

   818   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   819 *}

   820 

   821 

   822 text_raw {*

   823   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   824   \mode<presentation>{

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

   826 

   827   \mbox{}\\[-2mm]

   828 

   829   \small

   830   \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}}

   831   \bl{nullable (NULL)}            & \bl{$=$} & \bl{false} &\\

   832   \bl{nullable (EMPTY)}           & \bl{$=$} & \bl{true}  &\\

   833   \bl{nullable (CHR c)}           & \bl{$=$} & \bl{false} &\\

   834   \bl{nullable (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) orelse (nullable r$_2$)} & \\ 

   835   \bl{nullable (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) andalso (nullable r$_2$)} & \\

   836   \bl{nullable (STAR r)}          & \bl{$=$} & \bl{true} & \\

   837   \end{tabular}\medskip

   838 

   839   \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}

   840   \bl{der c (NULL)}            & \bl{$=$} & \bl{NULL} & \\

   841   \bl{der c (EMPTY)}           & \bl{$=$} & \bl{NULL} & \\

   842   \bl{der c (CHR d)}           & \bl{$=$} & \bl{if c=d then EMPTY else NULL} & \\

   843   \bl{der c (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (der c r$_1$) (der c r$_2$)} & \\

   844   \bl{der c (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (SEQ (der c r$_1$) r$_2$)} & \\

   845        &          & \bl{\phantom{ALT} (if nullable r$_1$ then der c r$_2$ else NULL)}\\

   846   \bl{der c (STAR r)}          & \bl{$=$} & \bl{SEQ (der c r) (STAR r)} &\smallskip\\

   847 

   848   \bl{derivative r []}     & \bl{$=$} & \bl{r} & \\

   849   \bl{derivative r (c::s)} & \bl{$=$} & \bl{derivative (der c r) s} & \\

   850   \end{tabular}\medskip

   851 

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

   853   

   854   \only<2>{

   855   \begin{textblock}{8}(1.5,4)

   856   \includegraphics[scale=0.3]{approved.png}

   857   \end{textblock}}

   858   

   859   \end{frame}}

   860   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   861 *}

   862 

   863 

   864 text_raw {*

   865   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   866   \mode<presentation>{

   867   \begin{frame}[c]

   868   \frametitle{No Automata?}

   869 

   870   You might be wondering why I did not use any automata:

   871 

   872   \begin{itemize}

   873   \item A \alert{regular language} is one where there is a DFA that 

   874   recognises it.\bigskip\pause

   875   \end{itemize}

   876 

   877 

   878   There are many reasons why this is a good definition:\medskip

   879   \begin{itemize}

   880   \item pumping lemma

   881   \item closure properties of regular languages\\ (e.g.~closure under complement)

   882   \end{itemize}

   883 

   884   \end{frame}}

   885   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   886 

   887 *}

   888 

   889 text_raw {*

   890   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   891   \mode<presentation>{

   892   \begin{frame}[t]

   893   \frametitle{Really Bad News!}

   894 

   895   DFAs are bad news for formalisations in theorem provers. They might

   896   be represented as:

   897 

   898   \begin{itemize}

   899   \item graphs

   900   \item matrices

   901   \item partial functions

   902   \end{itemize}

   903 

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

   905   \pause

   906 

   907   \small

   908   \only<2>{

   909   Constable et al needed (on and off) 18 months for a 3-person team 

   910   to formalise automata theory in Nuprl including Myhill-Nerode. There is 

   911   only very little other formalised work on regular languages I know of

   912   in Coq, Isabelle and HOL.}

   913   \only<3>{typical textbook reasoning goes like: ``\ldots if \smath{M} and \smath{N} are any two

   914   automata with no inaccessible states \ldots''

   915   }

   916   

   917   \end{frame}}

   918   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   919 

   920 *}

   921 

   922 text_raw {*

   923   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   924   \mode<presentation>{

   925   \begin{frame}[c]

   926   \frametitle{}

   927   \large

   928   \begin{center}

   929   \begin{tabular}{p{9cm}}

   930   My point:\bigskip\\

   931 

   932   The theory about regular languages can be reformulated 

   933   to be more suitable for theorem proving.

   934   \end{tabular}

   935   \end{center}

   936   \end{frame}}

   937   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   938 *}

   939 

   940 text_raw {*

   941   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   942   \mode<presentation>{

   943   \begin{frame}[c]

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

   945 

   946   \begin{itemize}

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

   948   being regular (pumping lemma only necessary)\medskip

   949 

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

   951 

   952   \item key is the equivalence relation:\smallskip

   953   \begin{center}

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

   955   \end{center}

   956   \end{itemize}

   957 

   958   \end{frame}}

   959   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   960 *}

   961 

   962 text_raw {*

   963   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   964   \mode<presentation>{

   965   \begin{frame}[c]

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

   967 

   968   \mbox{}\\[5cm]

   969 

   970   \begin{itemize}

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

   972   \end{itemize}

   973 

   974   \end{frame}}

   975   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   976 

   977 *}

   978 

   979 text_raw {*

   980   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   981   \mode<presentation>{

   982   \begin{frame}[c]

   983   \frametitle{\LARGE Equivalence Classes}

   984 

   985   \begin{itemize}

   986   \item \smath{L = []}

   987   \begin{center}

   988   \smath{\Big\{\{[]\},\; U\!N\!IV - \{[]\}\Big\}}

   989   \end{center}\bigskip\bigskip

   990 

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

   992   \begin{center}

   993   \smath{\Big\{\{[]\},\; \{[c]\},\; U\!N\!IV - \{[], [c]\}\Big\}}

   994   \end{center}\bigskip\bigskip

   995 

   996   \item \smath{L = \varnothing}

   997   \begin{center}

   998   \smath{\Big\{U\!N\!IV\Big\}}

   999   \end{center}

  1000 

  1001   \end{itemize}

  1002 

  1003   \end{frame}}

  1004   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1005 

  1006 *}

  1007 

  1008 text_raw {*

  1009   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1010   \mode<presentation>{

  1011   \begin{frame}[c]

  1012   \frametitle{\LARGE Regular Languages}

  1013 

  1014   \begin{itemize}

  1015   \item \smath{L} is regular \smath{\dn} if there is an automaton \smath{M} 

  1016   such that \smath{\mathbb{L}(M) = L}\\[1.5cm]

  1017 

  1018   \item Myhill-Nerode:

  1019 

  1020   \begin{center}

  1021   \begin{tabular}{l}

  1022   finite $\Rightarrow$ regular\\

  1023   \;\;\;\smath{\text{finite}\,(U\!N\!IV /\!/ \approx_L) \Rightarrow \exists r. L = \mathbb{L}(r)}\\[3mm]

  1024   regular $\Rightarrow$ finite\\

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

  1026   \end{tabular}

  1027   \end{center}

  1028 

  1029   \end{itemize}

  1030 

  1031   \end{frame}}

  1032   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1033 

  1034 *}

  1035 

  1036 text_raw {*

  1037   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1038   \mode<presentation>{

  1039   \begin{frame}[c]

  1040   \frametitle{\LARGE Final States}

  1041 

  1042   \mbox{}\\[3cm]

  1043 

  1044   \begin{itemize}

  1045   \item \smath{\text{final}_L\,X \dn}\\

  1046   \smath{\hspace{6mm}X \in (U\!N\!IV /\!/\approx_L) \;\wedge\; \forall s \in X.\; s \in L}

  1047   \smallskip

  1048   \item we can prove: \smath{L = \bigcup \{X.\;\text{final}_L\,X\}}

  1049 

  1050   \end{itemize}

  1051 

  1052   \end{frame}}

  1053   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1054 *}

  1055 

  1056 text_raw {*

  1057   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1058   \mode<presentation>{

  1059   \begin{frame}[c]

  1060   \frametitle{\LARGE Transitions between\\[-3mm] Equivalence Classes}

  1061 

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

  1063 

  1064   \begin{tabular}{@ {\hspace{-7mm}}cc}

  1065   \begin{tabular}{c}

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

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

  1068 

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

  1070 

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

  1072   \node[state,accepting] (q_1) [above right of=q_0]   {$R_2$};

  1073   \node[state]           (q_2) [below right of=q_0]   {$R_3$};

  1074 

  1075   \path[->] (q_0) edge                node        {c} (q_1)

  1076                   edge                node [swap] {$\Sigma-{c}$} (q_2)

  1077             (q_2) edge [loop below]   node        {$\Sigma$} ()

  1078             (q_1) edge                node        {$\Sigma$} (q_2);

  1079   \end{tikzpicture}

  1080   \end{tabular}

  1081   &

  1082   \begin{tabular}[t]{ll}

  1083   \\[-20mm]

  1084   \multicolumn{2}{l}{\smath{U\!N\!IV /\!/\approx_L} produces}\\[4mm]

  1085 

  1086   \smath{R_1}: & \smath{\{[]\}}\\

  1087   \smath{R_2}: & \smath{\{[c]\}}\\

  1088   \smath{R_3}: & \smath{U\!N\!IV - \{[], [c]\}}\\[6mm]

  1089   \multicolumn{2}{l}{\onslide<2->{\smath{X \stackrel{c}{\longrightarrow} Y \dn X ;; [c] \subseteq Y}}}

  1090   \end{tabular}

  1091 

  1092   \end{tabular}

  1093 

  1094   \end{frame}}

  1095   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1096 *}

  1097 

  1098 

  1099 text_raw {*

  1100   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1101   \mode<presentation>{

  1102   \begin{frame}[c]

  1103   \frametitle{\LARGE Systems of Equations}

  1104 

  1105   Inspired by a method of Brzozowski\;'64, we can build an equational system

  1106   characterising the equivalence classes:

  1107 

  1108   \begin{center}

  1109   \begin{tabular}{@ {\hspace{-20mm}}c}

  1110   \\[-13mm]

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

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

  1113 

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

  1115 

  1116   \node[state,initial]   (p_0)                  {$R_1$};

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

  1118 

  1119   \path[->] (p_0) edge [bend left]   node        {a} (p_1)

  1120                   edge [loop above]   node       {b} ()

  1121             (p_1) edge [loop above]   node       {a} ()

  1122                   edge [bend left]   node        {b} (p_0);

  1123   \end{tikzpicture}\\

  1124   \\[-13mm]

  1125   \end{tabular}

  1126   \end{center}

  1127 

  1128   \begin{center}

  1129   \begin{tabular}{@ {\hspace{-6mm}}ll@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

  1130   & \smath{R_1} & \smath{\equiv} & \smath{R_1;b + R_2;b \onslide<2->{\alert<2>{+ \lambda;[]}}}\\

  1131   & \smath{R_2} & \smath{\equiv} & \smath{R_1;a + R_2;a}\medskip\\

  1132   \onslide<3->{we can prove} 

  1133   & \onslide<3->{\smath{R_1}} & \onslide<3->{\smath{=}} 

  1134       & \onslide<3->{\smath{R_1; \mathbb{L}(b) \,\cup\, R_2;\mathbb{L}(b) \,\cup\, \{[]\};\{[]\}}}\\