# HG changeset patch # User urbanc # Date 1288820564 0 # Node ID 663816814e3eb5e779bf18f85ea9fae6039f0fd2 # Parent 7f64d98124a830eee3e64e4b1056da58fe16aa48 added initial slides for informal talk in Cambridge diff -r 7f64d98124a8 -r 663816814e3e IsaMakefile --- /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/* diff -r 7f64d98124a8 -r 663816814e3e Slides/ROOT1.ML --- /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 diff -r 7f64d98124a8 -r 663816814e3e Slides/Slides1.thy --- /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{ + \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{ + \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{ + \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{ + \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 diff -r 7f64d98124a8 -r 663816814e3e Slides/document/beamerthemeplaincu.sty --- /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 . +% +% 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 + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% 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 + + + + + + + diff -r 7f64d98124a8 -r 663816814e3e Slides/document/root.beamer.tex --- /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: + diff -r 7f64d98124a8 -r 663816814e3e Slides/document/root.notes.tex --- /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: + diff -r 7f64d98124a8 -r 663816814e3e Slides/document/root.tex --- /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{ +\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
{ +\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: +