--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/IsaMakefile	Wed Nov 03 21:42:44 2010 +0000
@@ -0,0 +1,33 @@
+
+## targets
+
+default: slides
+all: slides 
+
+## global settings
+
+SRC = $(ISABELLE_HOME)/src
+OUT = $(ISABELLE_OUTPUT)
+LOG = $(OUT)/log
+
+
+USEDIR = $(ISABELLE_TOOL) usedir -v true -t true 
+## Slides
+
+session1: Slides/ROOT1.ML \
+         Slides/document/root* \
+         Slides/Slides1.thy
+	@$(USEDIR) -D generated1 -f ROOT1.ML HOL Slides
+
+slides1: session1 
+	rm -f Slides/generated1/*.aux # otherwise latex will fall over
+	cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex 
+	cp Slides/generated1/root.beamer.pdf Slides/slides.pdf     
+
+slides: slides1 
+
+
+## clean
+
+clean:
+	rm -rf Slides/generated1/*

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/ROOT1.ML	Wed Nov 03 21:42:44 2010 +0000
@@ -0,0 +1,5 @@
+(*show_question_marks := false;*)
+
+no_document use_thy "LaTeXsugar";
+quick_and_dirty := true;
+use_thy "Slides1"
\ No newline at end of file

--- /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

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/document/beamerthemeplaincu.sty	Wed Nov 03 21:42:44 2010 +0000
@@ -0,0 +1,126 @@
+\ProvidesPackage{beamerthemeplaincu}[2003/11/07 ver 0.93]
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+
+% Copyright 2003 by Till Tantau <tantau@cs.tu-berlin.de>.
+%
+% This program can be redistributed and/or modified under the terms
+% of the LaTeX Project Public License Distributed from CTAN
+% archives in directory macros/latex/base/lppl.txt.
+
+\newcommand{\slidecaption}{}
+
+\mode<presentation>
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% comic fonts fonts
+\DeclareFontFamily{T1}{comic}{}%
+\DeclareFontShape{T1}{comic}{m}{n}{<->s*[.9]comic8t}{}%
+\DeclareFontShape{T1}{comic}{m}{it}{<->s*[.9]comic8t}{}%
+\DeclareFontShape{T1}{comic}{m}{sc}{<->s*[.9]comic8t}{}%
+\DeclareFontShape{T1}{comic}{b}{n}{<->s*[.9]comicbd8t}{}%
+\DeclareFontShape{T1}{comic}{b}{it}{<->s*[.9]comicbd8t}{}%
+\DeclareFontShape{T1}{comic}{m}{sl}{<->ssub * comic/m/it}{}%
+\DeclareFontShape{T1}{comic}{b}{sc}{<->sub * comic/m/sc}{}%
+\DeclareFontShape{T1}{comic}{b}{sl}{<->ssub * comic/b/it}{}%
+\DeclareFontShape{T1}{comic}{bx}{n}{<->ssub * comic/b/n}{}%
+\DeclareFontShape{T1}{comic}{bx}{it}{<->ssub * comic/b/it}{}%
+\DeclareFontShape{T1}{comic}{bx}{sc}{<->sub * comic/m/sc}{}%
+\DeclareFontShape{T1}{comic}{bx}{sl}{<->ssub * comic/b/it}{}%
+%
+\renewcommand{\rmdefault}{comic}%
+\renewcommand{\sfdefault}{comic}%
+\renewcommand{\mathfamilydefault}{cmr}% mathfont should be still the old one
+%
+\DeclareMathVersion{bold}% mathfont needs to be bold
+\DeclareSymbolFont{operators}{OT1}{cmr}{b}{n}%
+\SetSymbolFont{operators}{bold}{OT1}{cmr}{b}{n}%
+\DeclareSymbolFont{letters}{OML}{cmm}{b}{it}%
+\SetSymbolFont{letters}{bold}{OML}{cmm}{b}{it}%
+\DeclareSymbolFont{symbols}{OMS}{cmsy}{b}{n}%
+\SetSymbolFont{symbols}{bold}{OMS}{cmsy}{b}{n}%
+\DeclareSymbolFont{largesymbols}{OMX}{cmex}{b}{n}%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                              % Title page  
+%\usetitlepagetemplate{
+%  \vbox{}
+%  \vfill
+%  \begin{centering}
+%    \Large\structure{\textrm{\textit{{\inserttitle}}}}
+%    \vskip1em\par
+%    \normalsize\insertauthor\vskip1em\par
+%    {\scriptsize\insertinstitute\par}\par\vskip1em
+%    \insertdate\par\vskip1.5em
+%    \inserttitlegraphic
+%  \end{centering}
+%  \vfill
+%  }
+
+                                % Part page  
+%\usepartpagetemplate{
+%  \begin{centering}
+%    \Large\structure{\textrm{\textit{\partname~\@Roman\c@part}}}
+%    \vskip1em\par
+%    \textrm{\textit{\insertpart}}\par
+%  \end{centering}
+%  }
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Frametitles
+\setbeamerfont{frametitle}{size={\huge}}
+\setbeamerfont{frametitle}{family={\usefont{T1}{ptm}{b}{n}}}
+\setbeamercolor{frametitle}{fg=gray,bg=white}
+
+\setbeamertemplate{frametitle}{%
+\vskip 2mm  % distance from the top margin
+\hskip -3mm % distance from left margin
+\vbox{%
+\begin{minipage}{1.05\textwidth}%
+\centering%
+\insertframetitle%
+\end{minipage}}%
+}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Foot
+%
+\setbeamertemplate{navigation symbols}{} 
+\usefoottemplate{%
+\vbox{%
+  \tinyline{%
+    \tiny\hfill\textcolor{gray!50}{\slidecaption{} --
+      p.~\insertframenumber/\inserttotalframenumber}}}%
+}
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\beamertemplateballitem
+\setlength\leftmargini{2mm}
+\setlength\leftmarginii{0.6cm}
+\setlength\leftmarginiii{1.5cm}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% blocks
+%\definecolor{cream}{rgb}{1,1,.65}
+\definecolor{cream}{rgb}{1,1,.8}
+\setbeamerfont{block title}{size=\normalsize}
+\setbeamercolor{block title}{fg=black,bg=cream}
+\setbeamercolor{block body}{fg=black,bg=cream}
+
+\setbeamertemplate{blocks}[rounded][shadow=true]
+
+\setbeamercolor{boxcolor}{fg=black,bg=cream}
+
+\mode
+<all>
+
+
+
+
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/document/root.beamer.tex	Wed Nov 03 21:42:44 2010 +0000
@@ -0,0 +1,12 @@
+\documentclass[14pt,t]{beamer}
+%%%\usepackage{pstricks}
+
+\input{root.tex}
+
+%%% Local Variables:  
+%%% mode: latex
+%%% TeX-master: t
+%%% TeX-command-default: "Slides"
+%%% TeX-view-style: (("." "kghostview --landscape --scale 0.45 --geometry 605x505 %f"))
+%%% End: 
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/document/root.notes.tex	Wed Nov 03 21:42:44 2010 +0000
@@ -0,0 +1,18 @@
+\documentclass[11pt]{article}
+%%\usepackage{pstricks}
+\usepackage{dina4}
+\usepackage{beamerarticle}
+\usepackage{times}
+\usepackage{hyperref}
+\usepackage{pgf}
+\usepackage{amssymb}
+\setjobnamebeamerversion{root.beamer}
+\input{root.tex}
+
+%%% Local Variables:  
+%%% mode: latex
+%%% TeX-master: t
+%%% TeX-command-default: "Slides"
+%%% TeX-view-style: (("." "kghostview --landscape --scale 0.45 --geometry 605x505 %f"))
+%%% End: 
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/document/root.tex	Wed Nov 03 21:42:44 2010 +0000
@@ -0,0 +1,144 @@
+\usepackage{beamerthemeplaincu}
+\usepackage[T1]{fontenc}
+\usepackage{proof}
+\usepackage[latin1]{inputenc}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{mathpartir}
+\usepackage[absolute, overlay]{textpos}
+\usepackage{proof}
+\usepackage{ifthen}
+\usepackage{animate}
+\usepackage{tikz}
+\usepackage{pgf}
+\usetikzlibrary{arrows}
+\usetikzlibrary{automata}
+\usetikzlibrary{shapes}
+\usetikzlibrary{shadows}
+
+% Isabelle configuration
+%%\urlstyle{rm}
+\isabellestyle{rm}
+\renewcommand{\isastyle}{\rm}%
+\renewcommand{\isastyleminor}{\rm}%
+\renewcommand{\isastylescript}{\footnotesize\rm\slshape}%
+\renewcommand{\isatagproof}{}
+\renewcommand{\endisatagproof}{}
+\renewcommand{\isamarkupcmt}[1]{#1}
+
+% Isabelle characters
+\renewcommand{\isacharunderscore}{\_}
+\renewcommand{\isacharbar}{\isamath{\mid}}
+\renewcommand{\isasymiota}{}
+\renewcommand{\isacharbraceleft}{\{}
+\renewcommand{\isacharbraceright}{\}}
+\renewcommand{\isacharless}{$\langle$}
+\renewcommand{\isachargreater}{$\rangle$}
+\renewcommand{\isasymsharp}{\isamath{\#}}
+\renewcommand{\isasymdots}{\isamath{...}}
+\renewcommand{\isasymbullet}{\act}
+
+% mathpatir
+\mprset{sep=1em}
+
+% general math stuff
+\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
+\newcommand{\dnn}{\stackrel{\mbox{\Large def}}{=}}
+\renewcommand{\emptyset}{\varnothing}% nice round empty set
+\renewcommand{\Gamma}{\varGamma} 
+\DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}
+\DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}
+\newcommand{\smath}[1]{\textcolor{blue}{\ensuremath{#1}}}
+\newcommand{\fresh}{\mathrel{\#}}
+\newcommand{\act}{{\raisebox{-0.5mm}{\Large$\boldsymbol{\cdot}$}}}% swapping action
+\newcommand{\swap}[2]{(#1\,#2)}% swapping operation
+
+% beamer stuff 
+\renewcommand{\slidecaption}{Salvador, 26.~August 2008}
+
+
+% colours for Isar Code (in article mode everything is black and white)
+\mode<presentation>{
+\definecolor{isacol:brown}{rgb}{.823,.411,.117}
+\definecolor{isacol:lightblue}{rgb}{.274,.509,.705}
+\definecolor{isacol:green}{rgb}{0,.51,0.14}
+\definecolor{isacol:red}{rgb}{.803,0,0}
+\definecolor{isacol:blue}{rgb}{0,0,.803}
+\definecolor{isacol:darkred}{rgb}{.545,0,0}
+\definecolor{isacol:black}{rgb}{0,0,0}}
+\mode<article>{
+\definecolor{isacol:brown}{rgb}{0,0,0}
+\definecolor{isacol:lightblue}{rgb}{0,0,0}
+\definecolor{isacol:green}{rgb}{0,0,0}
+\definecolor{isacol:red}{rgb}{0,0,0}
+\definecolor{isacol:blue}{rgb}{0,0,0}
+\definecolor{isacol:darkred}{rgb}{0,0,0}
+\definecolor{isacol:black}{rgb}{0,0,0}
+}
+
+
+\newcommand{\strong}[1]{{\bfseries {#1}}}
+\newcommand{\bluecmd}[1]{{\color{isacol:lightblue}{\strong{#1}}}}
+\newcommand{\browncmd}[1]{{\color{isacol:brown}{\strong{#1}}}}
+\newcommand{\redcmd}[1]{{\color{isacol:red}{\strong{#1}}}}
+
+\renewcommand{\isakeyword}[1]{%
+\ifthenelse{\equal{#1}{show}}{\browncmd{#1}}{%
+\ifthenelse{\equal{#1}{case}}{\browncmd{#1}}{%
+\ifthenelse{\equal{#1}{assume}}{\browncmd{#1}}{%
+\ifthenelse{\equal{#1}{obtain}}{\browncmd{#1}}{%
+\ifthenelse{\equal{#1}{fix}}{\browncmd{#1}}{%
+\ifthenelse{\equal{#1}{oops}}{\redcmd{#1}}{%
+\ifthenelse{\equal{#1}{thm}}{\redcmd{#1}}{%
+{\bluecmd{#1}}}}}}}}}}%
+
+% inner syntax colour
+\chardef\isachardoublequoteopen=`\"%
+\chardef\isachardoublequoteclose=`\"%
+\chardef\isacharbackquoteopen=`\`%
+\chardef\isacharbackquoteclose=`\`%
+\newenvironment{innersingle}%
+{\isacharbackquoteopen\color{isacol:green}}%
+{\color{isacol:black}\isacharbackquoteclose}
+\newenvironment{innerdouble}%
+{\isachardoublequoteopen\color{isacol:green}}%
+{\color{isacol:black}\isachardoublequoteclose}
+
+%% misc
+\newcommand{\gb}[1]{\textcolor{isacol:green}{#1}}
+\newcommand{\rb}[1]{\textcolor{red}{#1}}
+
+%% animations
+\newcounter{growcnt}
+\newcommand{\grow}[2]
+{\begin{tikzpicture}[baseline=(n.base)]%
+    \node[scale=(0.1 *#1 + 0.001),inner sep=0pt] (n) {#2};
+  \end{tikzpicture}%
+}
+
+%% isatabbing
+%\renewcommand{\isamarkupcmt}[1]%
+%{\ifthenelse{\equal{TABSET}{#1}}{\=}%
+% {\ifthenelse{\equal{TAB}{#1}}{\>}%
+%  {\ifthenelse{\equal{NEWLINE}{#1}}{\\}%
+%   {\ifthenelse{\equal{DOTS}{#1}}{\ldots}{\isastylecmt--- {#1}}}%
+%  }%
+% }%
+%}%
+
+
+\newenvironment{isatabbing}%
+{\renewcommand{\isanewline}{\\}\begin{tabbing}}%
+{\end{tabbing}}
+
+\begin{document}
+\input{session}
+\end{document}
+
+%%% Local Variables:  
+%%% mode: latex
+%%% TeX-master: t
+%%% TeX-command-default: "Slides"
+%%% TeX-view-style: (("." "kghostview --landscape --scale 0.45 --geometry 605x505 %f"))
+%%% End: 
+