--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/Slides1.thy	Wed Nov 03 21:42:44 2010 +0000
@@ -0,0 +1,137 @@
+(*<*)
+theory Slides1
+imports "LaTeXsugar"
+begin
+
+notation (latex output)
+  set ("_") and
+  Cons  ("_::/_" [66,65] 65) 
+
+(*>*)
+
+
+text_raw {*
+  \renewcommand{\slidecaption}{Cambridge, 9 November 2010}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}
+  \frametitle{%
+  \begin{tabular}{@ {}c@ {}}
+  \Large A Formalisation of the\\[-5mm] 
+  \Large Myhill-Nerode Theorem\\[-5mm] 
+  \Large based on Regular Expressions\\[-3mm] 
+  \large \onslide<2>{or, Regular Languages Done Right}\\
+  \end{tabular}}
+  
+  \begin{center}
+  Christian Urban
+  \end{center}
+ 
+
+  \begin{center}
+  joint work with Chunhan Wu and Xingyuan Zhang from the PLA
+  University of Science and Technology in Nanjing
+  \end{center}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+text_raw {*
+  \renewcommand{\slidecaption}{Cambridge, 9 November 2010}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{In Textbooks\ldots}
+
+  \begin{itemize}
+  \item A \alert{regular language} is one where there is DFA that 
+  recognises it.\pause
+  \item Pumping lemma, closure properties of regular languages (closed 
+  under ``negation'') etc are all described and proved in terms of DFAs\pause
+
+  \item similarly the Myhill-Nerode theorem, which gives necessary and sufficient
+  conditions for a language being regular (also describes a minimal DFA for a language)
+
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+
+text_raw {*
+  \renewcommand{\slidecaption}{Cambridge, 9 November 2010}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Really Bad News!}
+
+  This is bad news for formalisations in theorem provers. DFAs might
+  be represented as
+
+  \begin{itemize}
+  \item graphs
+  \item matrices
+  \item partial functions
+  \end{itemize}
+
+  All constructions are difficult to reason about.\bigskip\bigskip 
+  \pause
+
+  \small
+  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.
+
+
+  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+text_raw {*
+  \renewcommand{\slidecaption}{Cambridge, 9 November 2010}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Regular Expressions}
+
+  \ldots are a simple datatype defined as:
+
+  \only<1>{
+  \begin{center}\color{blue}
+  \begin{tabular}{rcl}
+  rexp & $::=$ & NULL\\
+               & $\mid$ & EMPTY\\
+               & $\mid$ & CHR c\\
+               & $\mid$ & ALT rexp rexp\\
+               & $\mid$ & SEQ rexp rexp\\
+               & $\mid$ & STAR rexp
+  \end{tabular}
+  \end{center}}
+  \only<2->{
+  \begin{center}
+  \begin{tabular}{rcl}
+  \smath{r} & \smath{::=}  & \smath{\varepsilon} \\
+            & \smath{\mid} & \smath{[]}\\
+            & \smath{\mid} & \smath{c}\\
+            & \smath{\mid} & \smath{r_1 + r_2}\\
+            & \smath{\mid} & \smath{r_1 ; r_2}\\
+            & \smath{\mid} & \smath{r^\star}
+  \end{tabular}
+  \end{center}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+
+(*<*)
+end
+(*>*)
\ No newline at end of file