--- a/IsaMakefile Thu Nov 18 11:39:17 2010 +0000
+++ b/IsaMakefile Thu Nov 25 18:54:45 2010 +0000
@@ -1,8 +1,8 @@
## targets
-default: slides
-all: slides
+default: paper
+all: slides paper
## global settings
@@ -12,22 +12,36 @@
USEDIR = $(ISABELLE_TOOL) usedir -v true -t true
+
+
## Slides
-session1: Slides/ROOT1.ML \
+session1: Slides/ROOT.ML \
Slides/document/root* \
- Slides/Slides1.thy
- @$(USEDIR) -D generated1 -f ROOT1.ML HOL Slides
+ Slides/Slides.thy
+ @$(USEDIR) -D generated -f ROOT.ML HOL Slides
+
+slides: session1
+ rm -f Slides/generated/*.aux # otherwise latex will fall over
+ cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+ cp Slides/generated/root.beamer.pdf Slides/slides.pdf
+
-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
+## Paper
-slides: slides1
+session2: Paper/ROOT.ML \
+ Paper/document/root* \
+ Paper/Paper.thy
+ @$(USEDIR) -D generated -f ROOT.ML HOL Paper
+
+paper: session2
+ rm -f Paper/generated/*.aux # otherwise latex will fall over
+ cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
+ cp Paper/generated/root.pdf Paper/paper.pdf
## clean
clean:
- rm -rf Slides/generated1/*
+ rm -rf Slides/generated/*
+ rm -rf Paper/generated/*
--- a/Matcher.thy Thu Nov 18 11:39:17 2010 +0000
+++ b/Matcher.thy Thu Nov 25 18:54:45 2010 +0000
@@ -21,7 +21,7 @@
| step[intro]: "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> L\<star>"
-text {* A standard property of star *}
+text {* A standard property of Star *}
lemma lang_star_cases:
shows "L\<star> = {[]} \<union> L ; L\<star>"
--- a/My.thy Thu Nov 18 11:39:17 2010 +0000
+++ b/My.thy Thu Nov 25 18:54:45 2010 +0000
@@ -1,12 +1,12 @@
theory My
-imports Main
+imports Main Infinite_Set
begin
definition
- lang_seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ; _" [100,100] 100)
+ Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
where
- "L1 ; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"
+ "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"
inductive_set
Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
@@ -15,6 +15,32 @@
start[intro]: "[] \<in> L\<star>"
| step[intro]: "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1@s2 \<in> L\<star>"
+lemma lang_star_cases:
+ shows "L\<star> = {[]} \<union> L ;; L\<star>"
+unfolding Seq_def
+by (auto) (metis Star.simps)
+
+lemma lang_star_cases2:
+ shows "L ;; L\<star> = L\<star> ;; L"
+sorry
+
+
+theorem ardens_revised:
+ assumes nemp: "[] \<notin> A"
+ shows "(X = X ;; A \<union> B) \<longleftrightarrow> (X = B ;; A\<star>)"
+proof
+ assume eq: "X = B ;; A\<star>"
+ have "A\<star> = {[]} \<union> A\<star> ;; A" sorry
+ then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)" unfolding Seq_def by simp
+ also have "\<dots> = B \<union> B ;; (A\<star> ;; A)" unfolding Seq_def by auto
+ also have "\<dots> = B \<union> (B ;; A\<star>) ;; A" unfolding Seq_def
+ by (auto) (metis append_assoc)+
+ finally show "X = X ;; A \<union> B" using eq by auto
+next
+ assume "X = X ;; A \<union> B"
+ then have "B \<subseteq> X" "X ;; A \<subseteq> X" by auto
+ show "X = B ;; A\<star>" sorry
+qed
datatype rexp =
NULL
@@ -25,14 +51,14 @@
| STAR rexp
fun
- L_rexp :: "rexp \<Rightarrow> string set"
+ Sem :: "rexp \<Rightarrow> string set" ("\<lparr>_\<rparr>" [0] 1000)
where
- "L_rexp (NULL) = {}"
- | "L_rexp (EMPTY) = {[]}"
- | "L_rexp (CHAR c) = {[c]}"
- | "L_rexp (SEQ r1 r2) = (L_rexp r1) ; (L_rexp r2)"
- | "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)"
- | "L_rexp (STAR r) = (L_rexp r)\<star>"
+ "\<lparr>NULL\<rparr> = {}"
+ | "\<lparr>EMPTY\<rparr> = {[]}"
+ | "\<lparr>CHAR c\<rparr> = {[c]}"
+ | "\<lparr>SEQ r1 r2\<rparr> = \<lparr>r1\<rparr> ;; \<lparr>r2\<rparr>"
+ | "\<lparr>ALT r1 r2\<rparr> = \<lparr>r1\<rparr> \<union> \<lparr>r2\<rparr>"
+ | "\<lparr>STAR r\<rparr> = \<lparr>r\<rparr>\<star>"
definition
folds :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"
@@ -40,7 +66,7 @@
"folds f z S \<equiv> SOME x. fold_graph f z S x"
lemma folds_simp_null [simp]:
- "finite rs \<Longrightarrow> x \<in> L_rexp (folds ALT NULL rs) = (\<exists>r \<in> rs. x \<in> L_rexp r)"
+ "finite rs \<Longrightarrow> x \<in> \<lparr>folds ALT NULL rs\<rparr> \<longleftrightarrow> (\<exists>r \<in> rs. x \<in> \<lparr>r\<rparr>)"
apply (simp add: folds_def)
apply (rule someI2_ex)
apply (erule finite_imp_fold_graph)
@@ -49,7 +75,7 @@
done
lemma folds_simp_empty [simp]:
- "finite rs \<Longrightarrow> x \<in> L_rexp (folds ALT EMPTY rs) = ((\<exists>r \<in> rs. x \<in> L_rexp r) \<or> x = [])"
+ "finite rs \<Longrightarrow> x \<in> \<lparr>folds ALT EMPTY rs\<rparr> \<longleftrightarrow> (\<exists>r \<in> rs. x \<in> \<lparr>r\<rparr>) \<or> x = []"
apply (simp add: folds_def)
apply (rule someI2_ex)
apply (erule finite_imp_fold_graph)
@@ -58,7 +84,7 @@
done
lemma [simp]:
- "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
+ shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
by simp
definition
@@ -103,11 +129,11 @@
qed
lemma all_rexp:
- "\<lbrakk>finite (UNIV // \<approx>Lang); X \<in> (UNIV // \<approx>Lang)\<rbrakk> \<Longrightarrow> \<exists>r. X = L_rexp r"
+ "\<lbrakk>finite (UNIV // \<approx>Lang); X \<in> (UNIV // \<approx>Lang)\<rbrakk> \<Longrightarrow> \<exists>r. X = \<lparr>r\<rparr>"
sorry
lemma final_rexp:
- "\<lbrakk>finite (UNIV // (\<approx>Lang)); final X Lang\<rbrakk> \<Longrightarrow> \<exists>r. X = L_rexp r"
+ "\<lbrakk>finite (UNIV // (\<approx>Lang)); final X Lang\<rbrakk> \<Longrightarrow> \<exists>r. X = \<lparr>r\<rparr>"
unfolding final_def
using all_rexp by blast
@@ -132,12 +158,12 @@
lemma finite_regular_aux:
fixes Lang :: "string set"
assumes "finite (UNIV // (\<approx>Lang))"
- shows "\<exists>rs. Lang = L_rexp (folds ALT NULL rs)"
+ shows "\<exists>rs. Lang = \<lparr>folds ALT NULL rs\<rparr>"
apply(subst lang_is_union_of_finals)
using assms
apply -
apply(drule finite_final)
-apply(drule_tac f="L_rexp" in finite_f_one_to_one)
+apply(drule_tac f="Sem" in finite_f_one_to_one)
apply(clarify)
apply(drule final_rexp[OF assms])
apply(auto)[1]
@@ -151,7 +177,7 @@
lemma finite_regular:
fixes Lang :: "string set"
assumes "finite (UNIV // (\<approx>Lang))"
- shows "\<exists>r. Lang = L_rexp r"
+ shows "\<exists>r. Lang = \<lparr>r\<rparr>"
using assms finite_regular_aux
by auto
@@ -239,7 +265,7 @@
definition
transitions :: "string set \<Rightarrow> string set \<Rightarrow> rexp set" ("_\<Turnstile>\<Rightarrow>_")
where
- "Y \<Turnstile>\<Rightarrow> X \<equiv> {CHAR c | c. Y ; {[c]} \<subseteq> X}"
+ "Y \<Turnstile>\<Rightarrow> X \<equiv> {CHAR c | c. Y ;; {[c]} \<subseteq> X}"
definition
transitions_rexp ("_ \<turnstile>\<rightarrow> _")
@@ -250,7 +276,7 @@
"rhs CS X \<equiv> if X = {[]} then {({[]}, EMPTY)} else {(Y, Y \<turnstile>\<rightarrow>X) | Y. Y \<in> CS}"
definition
- "rhs_sem CS X \<equiv> \<Union> {(Y; L_rexp r) | Y r . (Y, r) \<in> rhs CS X}"
+ "rhs_sem CS X \<equiv> \<Union> {(Y;; \<lparr>r\<rparr>) | Y r . (Y, r) \<in> rhs CS X}"
definition
"eqs CS \<equiv> (\<Union>X \<in> CS. {(X, rhs CS X)})"
@@ -276,7 +302,7 @@
lemma every_eqclass_has_transition:
assumes has_str: "s @ [c] \<in> X"
and in_CS: "X \<in> UNIV // (\<approx>Lang)"
- obtains Y where "Y \<in> UNIV // (\<approx>Lang)" and "Y ; {[c]} \<subseteq> X" and "s \<in> Y"
+ obtains Y where "Y \<in> UNIV // (\<approx>Lang)" and "Y ;; {[c]} \<subseteq> X" and "s \<in> Y"
proof -
def Y \<equiv> "(\<approx>Lang) `` {s}"
have "Y \<in> UNIV // (\<approx>Lang)"
@@ -284,22 +310,21 @@
moreover
have "X = (\<approx>Lang) `` {s @ [c]}"
using has_str in_CS defined_by_str by blast
- then have "Y ; {[c]} \<subseteq> X"
- unfolding Y_def Image_def lang_seq_def
+ then have "Y ;; {[c]} \<subseteq> X"
+ unfolding Y_def Image_def Seq_def
unfolding str_eq_rel_def
by (auto) (simp add: str_eq_def)
moreover
have "s \<in> Y" unfolding Y_def
unfolding Image_def str_eq_rel_def str_eq_def by simp
- moreover
- have "True" by simp (* FIXME *)
- note that
- ultimately show thesis by blast
+ (*moreover
+ have "True" by simp FIXME *)
+ ultimately show thesis by (blast intro: that)
qed
lemma test:
assumes "[] \<in> X"
- shows "[] \<in> L_rexp (Y \<turnstile>\<rightarrow> X)"
+ shows "[] \<in> \<lparr>Y \<turnstile>\<rightarrow> X\<rparr>"
using assms
by (simp add: transitions_rexp_def)
@@ -308,7 +333,7 @@
shows "X \<subseteq> rhs_sem (UNIV // (\<approx>Lang)) X"
apply(case_tac "X = {[]}")
apply(simp)
-apply(simp add: rhs_sem_def rhs_def lang_seq_def)
+apply(simp add: rhs_sem_def rhs_def Seq_def)
apply(rule subsetI)
apply(case_tac "x = []")
apply(simp add: rhs_sem_def rhs_def)
@@ -317,4 +342,48 @@
apply(rule_tac x = "X" in exI)
apply(simp add: assms)
apply(simp add: transitions_rexp_def)
-oops
\ No newline at end of file
+oops
+
+
+(*
+fun
+ power :: "string \<Rightarrow> nat \<Rightarrow> string" (infixr "\<Up>" 100)
+where
+ "s \<Up> 0 = s"
+| "s \<Up> (Suc n) = s @ (s \<Up> n)"
+
+definition
+ "Lone = {(''0'' \<Up> n) @ (''1'' \<Up> n) | n. True }"
+
+lemma
+ "infinite (UNIV // (\<approx>Lone))"
+unfolding infinite_iff_countable_subset
+apply(rule_tac x="\<lambda>n. {(''0'' \<Up> n) @ (''1'' \<Up> i) | i. i \<in> {..n} }" in exI)
+apply(auto)
+prefer 2
+unfolding Lone_def
+unfolding quotient_def
+unfolding Image_def
+apply(simp)
+unfolding str_eq_rel_def
+unfolding str_eq_def
+apply(auto)
+apply(rule_tac x="''0'' \<Up> n" in exI)
+apply(auto)
+unfolding infinite_nat_iff_unbounded
+unfolding Lone_def
+*)
+
+
+
+text {* Derivatives *}
+
+definition
+ DERS :: "string \<Rightarrow> string set \<Rightarrow> string set"
+where
+ "DERS s L \<equiv> {s'. s @ s' \<in> L}"
+
+lemma
+ shows "x \<approx>L y \<longleftrightarrow> DERS x L = DERS y L"
+unfolding DERS_def str_eq_def
+by auto
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/Paper.thy Thu Nov 25 18:54:45 2010 +0000
@@ -0,0 +1,15 @@
+(*<*)
+theory Paper
+imports Main
+begin
+(*>*)
+
+section {* Introduction *}
+
+text {*
+
+*}
+
+(*<*)
+end
+(*>*)
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/ROOT.ML Thu Nov 25 18:54:45 2010 +0000
@@ -0,0 +1,2 @@
+no_document use_thy "LaTeXsugar";
+use_thy "Paper"
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/document/llncs.cls Thu Nov 25 18:54:45 2010 +0000
@@ -0,0 +1,1189 @@
+% LLNCS DOCUMENT CLASS -- version 2.13 (28-Jan-2002)
+% Springer Verlag LaTeX2e support for Lecture Notes in Computer Science
+%
+%%
+%% \CharacterTable
+%% {Upper-case \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
+%% Lower-case \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
+%% Digits \0\1\2\3\4\5\6\7\8\9
+%% Exclamation \! Double quote \" Hash (number) \#
+%% Dollar \$ Percent \% Ampersand \&
+%% Acute accent \' Left paren \( Right paren \)
+%% Asterisk \* Plus \+ Comma \,
+%% Minus \- Point \. Solidus \/
+%% Colon \: Semicolon \; Less than \<
+%% Equals \= Greater than \> Question mark \?
+%% Commercial at \@ Left bracket \[ Backslash \\
+%% Right bracket \] Circumflex \^ Underscore \_
+%% Grave accent \` Left brace \{ Vertical bar \|
+%% Right brace \} Tilde \~}
+%%
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+\ProvidesClass{llncs}[2002/01/28 v2.13
+^^J LaTeX document class for Lecture Notes in Computer Science]
+% Options
+\let\if@envcntreset\iffalse
+\DeclareOption{envcountreset}{\let\if@envcntreset\iftrue}
+\DeclareOption{citeauthoryear}{\let\citeauthoryear=Y}
+\DeclareOption{oribibl}{\let\oribibl=Y}
+\let\if@custvec\iftrue
+\DeclareOption{orivec}{\let\if@custvec\iffalse}
+\let\if@envcntsame\iffalse
+\DeclareOption{envcountsame}{\let\if@envcntsame\iftrue}
+\let\if@envcntsect\iffalse
+\DeclareOption{envcountsect}{\let\if@envcntsect\iftrue}
+\let\if@runhead\iffalse
+\DeclareOption{runningheads}{\let\if@runhead\iftrue}
+
+\let\if@openbib\iffalse
+\DeclareOption{openbib}{\let\if@openbib\iftrue}
+
+% languages
+\let\switcht@@therlang\relax
+\def\ds@deutsch{\def\switcht@@therlang{\switcht@deutsch}}
+\def\ds@francais{\def\switcht@@therlang{\switcht@francais}}
+
+\DeclareOption*{\PassOptionsToClass{\CurrentOption}{article}}
+
+\ProcessOptions
+
+\LoadClass[twoside]{article}
+\RequirePackage{multicol} % needed for the list of participants, index
+
+\setlength{\textwidth}{12.2cm}
+\setlength{\textheight}{19.3cm}
+\renewcommand\@pnumwidth{2em}
+\renewcommand\@tocrmarg{3.5em}
+%
+\def\@dottedtocline#1#2#3#4#5{%
+ \ifnum #1>\c@tocdepth \else
+ \vskip \z@ \@plus.2\p@
+ {\leftskip #2\relax \rightskip \@tocrmarg \advance\rightskip by 0pt plus 2cm
+ \parfillskip -\rightskip \pretolerance=10000
+ \parindent #2\relax\@afterindenttrue
+ \interlinepenalty\@M
+ \leavevmode
+ \@tempdima #3\relax
+ \advance\leftskip \@tempdima \null\nobreak\hskip -\leftskip
+ {#4}\nobreak
+ \leaders\hbox{$\m@th
+ \mkern \@dotsep mu\hbox{.}\mkern \@dotsep
+ mu$}\hfill
+ \nobreak
+ \hb@xt@\@pnumwidth{\hfil\normalfont \normalcolor #5}%
+ \par}%
+ \fi}
+%
+\def\switcht@albion{%
+\def\abstractname{Abstract.}
+\def\ackname{Acknowledgement.}
+\def\andname{and}
+\def\lastandname{\unskip, and}
+\def\appendixname{Appendix}
+\def\chaptername{Chapter}
+\def\claimname{Claim}
+\def\conjecturename{Conjecture}
+\def\contentsname{Table of Contents}
+\def\corollaryname{Corollary}
+\def\definitionname{Definition}
+\def\examplename{Example}
+\def\exercisename{Exercise}
+\def\figurename{Fig.}
+\def\keywordname{{\bf Key words:}}
+\def\indexname{Index}
+\def\lemmaname{Lemma}
+\def\contriblistname{List of Contributors}
+\def\listfigurename{List of Figures}
+\def\listtablename{List of Tables}
+\def\mailname{{\it Correspondence to\/}:}
+\def\noteaddname{Note added in proof}
+\def\notename{Note}
+\def\partname{Part}
+\def\problemname{Problem}
+\def\proofname{Proof}
+\def\propertyname{Property}
+\def\propositionname{Proposition}
+\def\questionname{Question}
+\def\remarkname{Remark}
+\def\seename{see}
+\def\solutionname{Solution}
+\def\subclassname{{\it Subject Classifications\/}:}
+\def\tablename{Table}
+\def\theoremname{Theorem}}
+\switcht@albion
+% Names of theorem like environments are already defined
+% but must be translated if another language is chosen
+%
+% French section
+\def\switcht@francais{%\typeout{On parle francais.}%
+ \def\abstractname{R\'esum\'e.}%
+ \def\ackname{Remerciements.}%
+ \def\andname{et}%
+ \def\lastandname{ et}%
+ \def\appendixname{Appendice}
+ \def\chaptername{Chapitre}%
+ \def\claimname{Pr\'etention}%
+ \def\conjecturename{Hypoth\`ese}%
+ \def\contentsname{Table des mati\`eres}%
+ \def\corollaryname{Corollaire}%
+ \def\definitionname{D\'efinition}%
+ \def\examplename{Exemple}%
+ \def\exercisename{Exercice}%
+ \def\figurename{Fig.}%
+ \def\keywordname{{\bf Mots-cl\'e:}}
+ \def\indexname{Index}
+ \def\lemmaname{Lemme}%
+ \def\contriblistname{Liste des contributeurs}
+ \def\listfigurename{Liste des figures}%
+ \def\listtablename{Liste des tables}%
+ \def\mailname{{\it Correspondence to\/}:}
+ \def\noteaddname{Note ajout\'ee \`a l'\'epreuve}%
+ \def\notename{Remarque}%
+ \def\partname{Partie}%
+ \def\problemname{Probl\`eme}%
+ \def\proofname{Preuve}%
+ \def\propertyname{Caract\'eristique}%
+%\def\propositionname{Proposition}%
+ \def\questionname{Question}%
+ \def\remarkname{Remarque}%
+ \def\seename{voir}
+ \def\solutionname{Solution}%
+ \def\subclassname{{\it Subject Classifications\/}:}
+ \def\tablename{Tableau}%
+ \def\theoremname{Th\'eor\`eme}%
+}
+%
+% German section
+\def\switcht@deutsch{%\typeout{Man spricht deutsch.}%
+ \def\abstractname{Zusammenfassung.}%
+ \def\ackname{Danksagung.}%
+ \def\andname{und}%
+ \def\lastandname{ und}%
+ \def\appendixname{Anhang}%
+ \def\chaptername{Kapitel}%
+ \def\claimname{Behauptung}%
+ \def\conjecturename{Hypothese}%
+ \def\contentsname{Inhaltsverzeichnis}%
+ \def\corollaryname{Korollar}%
+%\def\definitionname{Definition}%
+ \def\examplename{Beispiel}%
+ \def\exercisename{\"Ubung}%
+ \def\figurename{Abb.}%
+ \def\keywordname{{\bf Schl\"usselw\"orter:}}
+ \def\indexname{Index}
+%\def\lemmaname{Lemma}%
+ \def\contriblistname{Mitarbeiter}
+ \def\listfigurename{Abbildungsverzeichnis}%
+ \def\listtablename{Tabellenverzeichnis}%
+ \def\mailname{{\it Correspondence to\/}:}
+ \def\noteaddname{Nachtrag}%
+ \def\notename{Anmerkung}%
+ \def\partname{Teil}%
+%\def\problemname{Problem}%
+ \def\proofname{Beweis}%
+ \def\propertyname{Eigenschaft}%
+%\def\propositionname{Proposition}%
+ \def\questionname{Frage}%
+ \def\remarkname{Anmerkung}%
+ \def\seename{siehe}
+ \def\solutionname{L\"osung}%
+ \def\subclassname{{\it Subject Classifications\/}:}
+ \def\tablename{Tabelle}%
+%\def\theoremname{Theorem}%
+}
+
+% Ragged bottom for the actual page
+\def\thisbottomragged{\def\@textbottom{\vskip\z@ plus.0001fil
+\global\let\@textbottom\relax}}
+
+\renewcommand\small{%
+ \@setfontsize\small\@ixpt{11}%
+ \abovedisplayskip 8.5\p@ \@plus3\p@ \@minus4\p@
+ \abovedisplayshortskip \z@ \@plus2\p@
+ \belowdisplayshortskip 4\p@ \@plus2\p@ \@minus2\p@
+ \def\@listi{\leftmargin\leftmargini
+ \parsep 0\p@ \@plus1\p@ \@minus\p@
+ \topsep 8\p@ \@plus2\p@ \@minus4\p@
+ \itemsep0\p@}%
+ \belowdisplayskip \abovedisplayskip
+}
+
+\frenchspacing
+\widowpenalty=10000
+\clubpenalty=10000
+
+\setlength\oddsidemargin {63\p@}
+\setlength\evensidemargin {63\p@}
+\setlength\marginparwidth {90\p@}
+
+\setlength\headsep {16\p@}
+
+\setlength\footnotesep{7.7\p@}
+\setlength\textfloatsep{8mm\@plus 2\p@ \@minus 4\p@}
+\setlength\intextsep {8mm\@plus 2\p@ \@minus 2\p@}
+
+\setcounter{secnumdepth}{2}
+
+\newcounter {chapter}
+\renewcommand\thechapter {\@arabic\c@chapter}
+
+\newif\if@mainmatter \@mainmattertrue
+\newcommand\frontmatter{\cleardoublepage
+ \@mainmatterfalse\pagenumbering{Roman}}
+\newcommand\mainmatter{\cleardoublepage
+ \@mainmattertrue\pagenumbering{arabic}}
+\newcommand\backmatter{\if@openright\cleardoublepage\else\clearpage\fi
+ \@mainmatterfalse}
+
+\renewcommand\part{\cleardoublepage
+ \thispagestyle{empty}%
+ \if@twocolumn
+ \onecolumn
+ \@tempswatrue
+ \else
+ \@tempswafalse
+ \fi
+ \null\vfil
+ \secdef\@part\@spart}
+
+\def\@part[#1]#2{%
+ \ifnum \c@secnumdepth >-2\relax
+ \refstepcounter{part}%
+ \addcontentsline{toc}{part}{\thepart\hspace{1em}#1}%
+ \else
+ \addcontentsline{toc}{part}{#1}%
+ \fi
+ \markboth{}{}%
+ {\centering
+ \interlinepenalty \@M
+ \normalfont
+ \ifnum \c@secnumdepth >-2\relax
+ \huge\bfseries \partname~\thepart
+ \par
+ \vskip 20\p@
+ \fi
+ \Huge \bfseries #2\par}%
+ \@endpart}
+\def\@spart#1{%
+ {\centering
+ \interlinepenalty \@M
+ \normalfont
+ \Huge \bfseries #1\par}%
+ \@endpart}
+\def\@endpart{\vfil\newpage
+ \if@twoside
+ \null
+ \thispagestyle{empty}%
+ \newpage
+ \fi
+ \if@tempswa
+ \twocolumn
+ \fi}
+
+\newcommand\chapter{\clearpage
+ \thispagestyle{empty}%
+ \global\@topnum\z@
+ \@afterindentfalse
+ \secdef\@chapter\@schapter}
+\def\@chapter[#1]#2{\ifnum \c@secnumdepth >\m@ne
+ \if@mainmatter
+ \refstepcounter{chapter}%
+ \typeout{\@chapapp\space\thechapter.}%
+ \addcontentsline{toc}{chapter}%
+ {\protect\numberline{\thechapter}#1}%
+ \else
+ \addcontentsline{toc}{chapter}{#1}%
+ \fi
+ \else
+ \addcontentsline{toc}{chapter}{#1}%
+ \fi
+ \chaptermark{#1}%
+ \addtocontents{lof}{\protect\addvspace{10\p@}}%
+ \addtocontents{lot}{\protect\addvspace{10\p@}}%
+ \if@twocolumn
+ \@topnewpage[\@makechapterhead{#2}]%
+ \else
+ \@makechapterhead{#2}%
+ \@afterheading
+ \fi}
+\def\@makechapterhead#1{%
+% \vspace*{50\p@}%
+ {\centering
+ \ifnum \c@secnumdepth >\m@ne
+ \if@mainmatter
+ \large\bfseries \@chapapp{} \thechapter
+ \par\nobreak
+ \vskip 20\p@
+ \fi
+ \fi
+ \interlinepenalty\@M
+ \Large \bfseries #1\par\nobreak
+ \vskip 40\p@
+ }}
+\def\@schapter#1{\if@twocolumn
+ \@topnewpage[\@makeschapterhead{#1}]%
+ \else
+ \@makeschapterhead{#1}%
+ \@afterheading
+ \fi}
+\def\@makeschapterhead#1{%
+% \vspace*{50\p@}%
+ {\centering
+ \normalfont
+ \interlinepenalty\@M
+ \Large \bfseries #1\par\nobreak
+ \vskip 40\p@
+ }}
+
+\renewcommand\section{\@startsection{section}{1}{\z@}%
+ {-18\p@ \@plus -4\p@ \@minus -4\p@}%
+ {12\p@ \@plus 4\p@ \@minus 4\p@}%
+ {\normalfont\large\bfseries\boldmath
+ \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
+\renewcommand\subsection{\@startsection{subsection}{2}{\z@}%
+ {-18\p@ \@plus -4\p@ \@minus -4\p@}%
+ {8\p@ \@plus 4\p@ \@minus 4\p@}%
+ {\normalfont\normalsize\bfseries\boldmath
+ \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
+\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}%
+ {-18\p@ \@plus -4\p@ \@minus -4\p@}%
+ {-0.5em \@plus -0.22em \@minus -0.1em}%
+ {\normalfont\normalsize\bfseries\boldmath}}
+\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}%
+ {-12\p@ \@plus -4\p@ \@minus -4\p@}%
+ {-0.5em \@plus -0.22em \@minus -0.1em}%
+ {\normalfont\normalsize\itshape}}
+\renewcommand\subparagraph[1]{\typeout{LLNCS warning: You should not use
+ \string\subparagraph\space with this class}\vskip0.5cm
+You should not use \verb|\subparagraph| with this class.\vskip0.5cm}
+
+\DeclareMathSymbol{\Gamma}{\mathalpha}{letters}{"00}
+\DeclareMathSymbol{\Delta}{\mathalpha}{letters}{"01}
+\DeclareMathSymbol{\Theta}{\mathalpha}{letters}{"02}
+\DeclareMathSymbol{\Lambda}{\mathalpha}{letters}{"03}
+\DeclareMathSymbol{\Xi}{\mathalpha}{letters}{"04}
+\DeclareMathSymbol{\Pi}{\mathalpha}{letters}{"05}
+\DeclareMathSymbol{\Sigma}{\mathalpha}{letters}{"06}
+\DeclareMathSymbol{\Upsilon}{\mathalpha}{letters}{"07}
+\DeclareMathSymbol{\Phi}{\mathalpha}{letters}{"08}
+\DeclareMathSymbol{\Psi}{\mathalpha}{letters}{"09}
+\DeclareMathSymbol{\Omega}{\mathalpha}{letters}{"0A}
+
+\let\footnotesize\small
+
+\if@custvec
+\def\vec#1{\mathchoice{\mbox{\boldmath$\displaystyle#1$}}
+{\mbox{\boldmath$\textstyle#1$}}
+{\mbox{\boldmath$\scriptstyle#1$}}
+{\mbox{\boldmath$\scriptscriptstyle#1$}}}
+\fi
+
+\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}}
+\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil
+\penalty50\hskip1em\null\nobreak\hfil\squareforqed
+\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}
+
+\def\getsto{\mathrel{\mathchoice {\vcenter{\offinterlineskip
+\halign{\hfil
+$\displaystyle##$\hfil\cr\gets\cr\to\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr\gets
+\cr\to\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr\gets
+\cr\to\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+\gets\cr\to\cr}}}}}
+\def\lid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
+$\displaystyle##$\hfil\cr<\cr\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr<\cr
+\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr<\cr
+\noalign{\vskip1pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+<\cr
+\noalign{\vskip0.9pt}=\cr}}}}}
+\def\gid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
+$\displaystyle##$\hfil\cr>\cr\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr>\cr
+\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr>\cr
+\noalign{\vskip1pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+>\cr
+\noalign{\vskip0.9pt}=\cr}}}}}
+\def\grole{\mathrel{\mathchoice {\vcenter{\offinterlineskip
+\halign{\hfil
+$\displaystyle##$\hfil\cr>\cr\noalign{\vskip-1pt}<\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr
+>\cr\noalign{\vskip-1pt}<\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr
+>\cr\noalign{\vskip-0.8pt}<\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+>\cr\noalign{\vskip-0.3pt}<\cr}}}}}
+\def\bbbr{{\rm I\!R}} %reelle Zahlen
+\def\bbbm{{\rm I\!M}}
+\def\bbbn{{\rm I\!N}} %natuerliche Zahlen
+\def\bbbf{{\rm I\!F}}
+\def\bbbh{{\rm I\!H}}
+\def\bbbk{{\rm I\!K}}
+\def\bbbp{{\rm I\!P}}
+\def\bbbone{{\mathchoice {\rm 1\mskip-4mu l} {\rm 1\mskip-4mu l}
+{\rm 1\mskip-4.5mu l} {\rm 1\mskip-5mu l}}}
+\def\bbbc{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}}}
+\def\bbbq{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
+Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle\rm Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle\rm Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}}}
+\def\bbbt{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
+T$}\hbox{\hbox to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle\rm T$}\hbox{\hbox
+to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle\rm T$}\hbox{\hbox
+to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm T$}\hbox{\hbox
+to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}}}
+\def\bbbs{{\mathchoice
+{\setbox0=\hbox{$\displaystyle \rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
+to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle \rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
+to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle \rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
+to0pt{\kern0.5\wd0\vrule height0.45\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.4\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
+to0pt{\kern0.55\wd0\vrule height0.45\ht0\hss}\box0}}}}
+\def\bbbz{{\mathchoice {\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}}
+{\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}}
+{\hbox{$\mathsf\scriptstyle Z\kern-0.3em Z$}}
+{\hbox{$\mathsf\scriptscriptstyle Z\kern-0.2em Z$}}}}
+
+\let\ts\,
+
+\setlength\leftmargini {17\p@}
+\setlength\leftmargin {\leftmargini}
+\setlength\leftmarginii {\leftmargini}
+\setlength\leftmarginiii {\leftmargini}
+\setlength\leftmarginiv {\leftmargini}
+\setlength \labelsep {.5em}
+\setlength \labelwidth{\leftmargini}
+\addtolength\labelwidth{-\labelsep}
+
+\def\@listI{\leftmargin\leftmargini
+ \parsep 0\p@ \@plus1\p@ \@minus\p@
+ \topsep 8\p@ \@plus2\p@ \@minus4\p@
+ \itemsep0\p@}
+\let\@listi\@listI
+\@listi
+\def\@listii {\leftmargin\leftmarginii
+ \labelwidth\leftmarginii
+ \advance\labelwidth-\labelsep
+ \topsep 0\p@ \@plus2\p@ \@minus\p@}
+\def\@listiii{\leftmargin\leftmarginiii
+ \labelwidth\leftmarginiii
+ \advance\labelwidth-\labelsep
+ \topsep 0\p@ \@plus\p@\@minus\p@
+ \parsep \z@
+ \partopsep \p@ \@plus\z@ \@minus\p@}
+
+\renewcommand\labelitemi{\normalfont\bfseries --}
+\renewcommand\labelitemii{$\m@th\bullet$}
+
+\setlength\arraycolsep{1.4\p@}
+\setlength\tabcolsep{1.4\p@}
+
+\def\tableofcontents{\chapter*{\contentsname\@mkboth{{\contentsname}}%
+ {{\contentsname}}}
+ \def\authcount##1{\setcounter{auco}{##1}\setcounter{@auth}{1}}
+ \def\lastand{\ifnum\value{auco}=2\relax
+ \unskip{} \andname\
+ \else
+ \unskip \lastandname\
+ \fi}%
+ \def\and{\stepcounter{@auth}\relax
+ \ifnum\value{@auth}=\value{auco}%
+ \lastand
+ \else
+ \unskip,
+ \fi}%
+ \@starttoc{toc}\if@restonecol\twocolumn\fi}
+
+\def\l@part#1#2{\addpenalty{\@secpenalty}%
+ \addvspace{2em plus\p@}% % space above part line
+ \begingroup
+ \parindent \z@
+ \rightskip \z@ plus 5em
+ \hrule\vskip5pt
+ \large % same size as for a contribution heading
+ \bfseries\boldmath % set line in boldface
+ \leavevmode % TeX command to enter horizontal mode.
+ #1\par
+ \vskip5pt
+ \hrule
+ \vskip1pt
+ \nobreak % Never break after part entry
+ \endgroup}
+
+\def\@dotsep{2}
+
+\def\hyperhrefextend{\ifx\hyper@anchor\@undefined\else
+{chapter.\thechapter}\fi}
+
+\def\addnumcontentsmark#1#2#3{%
+\addtocontents{#1}{\protect\contentsline{#2}{\protect\numberline
+ {\thechapter}#3}{\thepage}\hyperhrefextend}}
+\def\addcontentsmark#1#2#3{%
+\addtocontents{#1}{\protect\contentsline{#2}{#3}{\thepage}\hyperhrefextend}}
+\def\addcontentsmarkwop#1#2#3{%
+\addtocontents{#1}{\protect\contentsline{#2}{#3}{0}\hyperhrefextend}}
+
+\def\@adcmk[#1]{\ifcase #1 \or
+\def\@gtempa{\addnumcontentsmark}%
+ \or \def\@gtempa{\addcontentsmark}%
+ \or \def\@gtempa{\addcontentsmarkwop}%
+ \fi\@gtempa{toc}{chapter}}
+\def\addtocmark{\@ifnextchar[{\@adcmk}{\@adcmk[3]}}
+
+\def\l@chapter#1#2{\addpenalty{-\@highpenalty}
+ \vskip 1.0em plus 1pt \@tempdima 1.5em \begingroup
+ \parindent \z@ \rightskip \@tocrmarg
+ \advance\rightskip by 0pt plus 2cm
+ \parfillskip -\rightskip \pretolerance=10000
+ \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip
+ {\large\bfseries\boldmath#1}\ifx0#2\hfil\null
+ \else
+ \nobreak
+ \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern
+ \@dotsep mu$}\hfill
+ \nobreak\hbox to\@pnumwidth{\hss #2}%
+ \fi\par
+ \penalty\@highpenalty \endgroup}
+
+\def\l@title#1#2{\addpenalty{-\@highpenalty}
+ \addvspace{8pt plus 1pt}
+ \@tempdima \z@
+ \begingroup
+ \parindent \z@ \rightskip \@tocrmarg
+ \advance\rightskip by 0pt plus 2cm
+ \parfillskip -\rightskip \pretolerance=10000
+ \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip
+ #1\nobreak
+ \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern
+ \@dotsep mu$}\hfill
+ \nobreak\hbox to\@pnumwidth{\hss #2}\par
+ \penalty\@highpenalty \endgroup}
+
+\def\l@author#1#2{\addpenalty{\@highpenalty}
+ \@tempdima=\z@ %15\p@
+ \begingroup
+ \parindent \z@ \rightskip \@tocrmarg
+ \advance\rightskip by 0pt plus 2cm
+ \pretolerance=10000
+ \leavevmode \advance\leftskip\@tempdima %\hskip -\leftskip
+ \textit{#1}\par
+ \penalty\@highpenalty \endgroup}
+
+%\setcounter{tocdepth}{0}
+\newdimen\tocchpnum
+\newdimen\tocsecnum
+\newdimen\tocsectotal
+\newdimen\tocsubsecnum
+\newdimen\tocsubsectotal
+\newdimen\tocsubsubsecnum
+\newdimen\tocsubsubsectotal
+\newdimen\tocparanum
+\newdimen\tocparatotal
+\newdimen\tocsubparanum
+\tocchpnum=\z@ % no chapter numbers
+\tocsecnum=15\p@ % section 88. plus 2.222pt
+\tocsubsecnum=23\p@ % subsection 88.8 plus 2.222pt
+\tocsubsubsecnum=27\p@ % subsubsection 88.8.8 plus 1.444pt
+\tocparanum=35\p@ % paragraph 88.8.8.8 plus 1.666pt
+\tocsubparanum=43\p@ % subparagraph 88.8.8.8.8 plus 1.888pt
+\def\calctocindent{%
+\tocsectotal=\tocchpnum
+\advance\tocsectotal by\tocsecnum
+\tocsubsectotal=\tocsectotal
+\advance\tocsubsectotal by\tocsubsecnum
+\tocsubsubsectotal=\tocsubsectotal
+\advance\tocsubsubsectotal by\tocsubsubsecnum
+\tocparatotal=\tocsubsubsectotal
+\advance\tocparatotal by\tocparanum}
+\calctocindent
+
+\def\l@section{\@dottedtocline{1}{\tocchpnum}{\tocsecnum}}
+\def\l@subsection{\@dottedtocline{2}{\tocsectotal}{\tocsubsecnum}}
+\def\l@subsubsection{\@dottedtocline{3}{\tocsubsectotal}{\tocsubsubsecnum}}
+\def\l@paragraph{\@dottedtocline{4}{\tocsubsubsectotal}{\tocparanum}}
+\def\l@subparagraph{\@dottedtocline{5}{\tocparatotal}{\tocsubparanum}}
+
+\def\listoffigures{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
+ \fi\section*{\listfigurename\@mkboth{{\listfigurename}}{{\listfigurename}}}
+ \@starttoc{lof}\if@restonecol\twocolumn\fi}
+\def\l@figure{\@dottedtocline{1}{0em}{1.5em}}
+
+\def\listoftables{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
+ \fi\section*{\listtablename\@mkboth{{\listtablename}}{{\listtablename}}}
+ \@starttoc{lot}\if@restonecol\twocolumn\fi}
+\let\l@table\l@figure
+
+\renewcommand\listoffigures{%
+ \section*{\listfigurename
+ \@mkboth{\listfigurename}{\listfigurename}}%
+ \@starttoc{lof}%
+ }
+
+\renewcommand\listoftables{%
+ \section*{\listtablename
+ \@mkboth{\listtablename}{\listtablename}}%
+ \@starttoc{lot}%
+ }
+
+\ifx\oribibl\undefined
+\ifx\citeauthoryear\undefined
+\renewenvironment{thebibliography}[1]
+ {\section*{\refname}
+ \def\@biblabel##1{##1.}
+ \small
+ \list{\@biblabel{\@arabic\c@enumiv}}%
+ {\settowidth\labelwidth{\@biblabel{#1}}%
+ \leftmargin\labelwidth
+ \advance\leftmargin\labelsep
+ \if@openbib
+ \advance\leftmargin\bibindent
+ \itemindent -\bibindent
+ \listparindent \itemindent
+ \parsep \z@
+ \fi
+ \usecounter{enumiv}%
+ \let\p@enumiv\@empty
+ \renewcommand\theenumiv{\@arabic\c@enumiv}}%
+ \if@openbib
+ \renewcommand\newblock{\par}%
+ \else
+ \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}%
+ \fi
+ \sloppy\clubpenalty4000\widowpenalty4000%
+ \sfcode`\.=\@m}
+ {\def\@noitemerr
+ {\@latex@warning{Empty `thebibliography' environment}}%
+ \endlist}
+\def\@lbibitem[#1]#2{\item[{[#1]}\hfill]\if@filesw
+ {\let\protect\noexpand\immediate
+ \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces}
+\newcount\@tempcntc
+\def\@citex[#1]#2{\if@filesw\immediate\write\@auxout{\string\citation{#2}}\fi
+ \@tempcnta\z@\@tempcntb\m@ne\def\@citea{}\@cite{\@for\@citeb:=#2\do
+ {\@ifundefined
+ {b@\@citeb}{\@citeo\@tempcntb\m@ne\@citea\def\@citea{,}{\bfseries
+ ?}\@warning
+ {Citation `\@citeb' on page \thepage \space undefined}}%
+ {\setbox\z@\hbox{\global\@tempcntc0\csname b@\@citeb\endcsname\relax}%
+ \ifnum\@tempcntc=\z@ \@citeo\@tempcntb\m@ne
+ \@citea\def\@citea{,}\hbox{\csname b@\@citeb\endcsname}%
+ \else
+ \advance\@tempcntb\@ne
+ \ifnum\@tempcntb=\@tempcntc
+ \else\advance\@tempcntb\m@ne\@citeo
+ \@tempcnta\@tempcntc\@tempcntb\@tempcntc\fi\fi}}\@citeo}{#1}}
+\def\@citeo{\ifnum\@tempcnta>\@tempcntb\else
+ \@citea\def\@citea{,\,\hskip\z@skip}%
+ \ifnum\@tempcnta=\@tempcntb\the\@tempcnta\else
+ {\advance\@tempcnta\@ne\ifnum\@tempcnta=\@tempcntb \else
+ \def\@citea{--}\fi
+ \advance\@tempcnta\m@ne\the\@tempcnta\@citea\the\@tempcntb}\fi\fi}
+\else
+\renewenvironment{thebibliography}[1]
+ {\section*{\refname}
+ \small
+ \list{}%
+ {\settowidth\labelwidth{}%
+ \leftmargin\parindent
+ \itemindent=-\parindent
+ \labelsep=\z@
+ \if@openbib
+ \advance\leftmargin\bibindent
+ \itemindent -\bibindent
+ \listparindent \itemindent
+ \parsep \z@
+ \fi
+ \usecounter{enumiv}%
+ \let\p@enumiv\@empty
+ \renewcommand\theenumiv{}}%
+ \if@openbib
+ \renewcommand\newblock{\par}%
+ \else
+ \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}%
+ \fi
+ \sloppy\clubpenalty4000\widowpenalty4000%
+ \sfcode`\.=\@m}
+ {\def\@noitemerr
+ {\@latex@warning{Empty `thebibliography' environment}}%
+ \endlist}
+ \def\@cite#1{#1}%
+ \def\@lbibitem[#1]#2{\item[]\if@filesw
+ {\def\protect##1{\string ##1\space}\immediate
+ \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces}
+ \fi
+\else
+\@cons\@openbib@code{\noexpand\small}
+\fi
+
+\def\idxquad{\hskip 10\p@}% space that divides entry from number
+
+\def\@idxitem{\par\hangindent 10\p@}
+
+\def\subitem{\par\setbox0=\hbox{--\enspace}% second order
+ \noindent\hangindent\wd0\box0}% index entry
+
+\def\subsubitem{\par\setbox0=\hbox{--\,--\enspace}% third
+ \noindent\hangindent\wd0\box0}% order index entry
+
+\def\indexspace{\par \vskip 10\p@ plus5\p@ minus3\p@\relax}
+
+\renewenvironment{theindex}
+ {\@mkboth{\indexname}{\indexname}%
+ \thispagestyle{empty}\parindent\z@
+ \parskip\z@ \@plus .3\p@\relax
+ \let\item\par
+ \def\,{\relax\ifmmode\mskip\thinmuskip
+ \else\hskip0.2em\ignorespaces\fi}%
+ \normalfont\small
+ \begin{multicols}{2}[\@makeschapterhead{\indexname}]%
+ }
+ {\end{multicols}}
+
+\renewcommand\footnoterule{%
+ \kern-3\p@
+ \hrule\@width 2truecm
+ \kern2.6\p@}
+ \newdimen\fnindent
+ \fnindent1em
+\long\def\@makefntext#1{%
+ \parindent \fnindent%
+ \leftskip \fnindent%
+ \noindent
+ \llap{\hb@xt@1em{\hss\@makefnmark\ }}\ignorespaces#1}
+
+\long\def\@makecaption#1#2{%
+ \vskip\abovecaptionskip
+ \sbox\@tempboxa{{\bfseries #1.} #2}%
+ \ifdim \wd\@tempboxa >\hsize
+ {\bfseries #1.} #2\par
+ \else
+ \global \@minipagefalse
+ \hb@xt@\hsize{\hfil\box\@tempboxa\hfil}%
+ \fi
+ \vskip\belowcaptionskip}
+
+\def\fps@figure{htbp}
+\def\fnum@figure{\figurename\thinspace\thefigure}
+\def \@floatboxreset {%
+ \reset@font
+ \small
+ \@setnobreak
+ \@setminipage
+}
+\def\fps@table{htbp}
+\def\fnum@table{\tablename~\thetable}
+\renewenvironment{table}
+ {\setlength\abovecaptionskip{0\p@}%
+ \setlength\belowcaptionskip{10\p@}%
+ \@float{table}}
+ {\end@float}
+\renewenvironment{table*}
+ {\setlength\abovecaptionskip{0\p@}%
+ \setlength\belowcaptionskip{10\p@}%
+ \@dblfloat{table}}
+ {\end@dblfloat}
+
+\long\def\@caption#1[#2]#3{\par\addcontentsline{\csname
+ ext@#1\endcsname}{#1}{\protect\numberline{\csname
+ the#1\endcsname}{\ignorespaces #2}}\begingroup
+ \@parboxrestore
+ \@makecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par
+ \endgroup}
+
+% LaTeX does not provide a command to enter the authors institute
+% addresses. The \institute command is defined here.
+
+\newcounter{@inst}
+\newcounter{@auth}
+\newcounter{auco}
+\newdimen\instindent
+\newbox\authrun
+\newtoks\authorrunning
+\newtoks\tocauthor
+\newbox\titrun
+\newtoks\titlerunning
+\newtoks\toctitle
+
+\def\clearheadinfo{\gdef\@author{No Author Given}%
+ \gdef\@title{No Title Given}%
+ \gdef\@subtitle{}%
+ \gdef\@institute{No Institute Given}%
+ \gdef\@thanks{}%
+ \global\titlerunning={}\global\authorrunning={}%
+ \global\toctitle={}\global\tocauthor={}}
+
+\def\institute#1{\gdef\@institute{#1}}
+
+\def\institutename{\par
+ \begingroup
+ \parskip=\z@
+ \parindent=\z@
+ \setcounter{@inst}{1}%
+ \def\and{\par\stepcounter{@inst}%
+ \noindent$^{\the@inst}$\enspace\ignorespaces}%
+ \setbox0=\vbox{\def\thanks##1{}\@institute}%
+ \ifnum\c@@inst=1\relax
+ \gdef\fnnstart{0}%
+ \else
+ \xdef\fnnstart{\c@@inst}%
+ \setcounter{@inst}{1}%
+ \noindent$^{\the@inst}$\enspace
+ \fi
+ \ignorespaces
+ \@institute\par
+ \endgroup}
+
+\def\@fnsymbol#1{\ensuremath{\ifcase#1\or\star\or{\star\star}\or
+ {\star\star\star}\or \dagger\or \ddagger\or
+ \mathchar "278\or \mathchar "27B\or \|\or **\or \dagger\dagger
+ \or \ddagger\ddagger \else\@ctrerr\fi}}
+
+\def\inst#1{\unskip$^{#1}$}
+\def\fnmsep{\unskip$^,$}
+\def\email#1{{\tt#1}}
+\AtBeginDocument{\@ifundefined{url}{\def\url#1{#1}}{}%
+\@ifpackageloaded{babel}{%
+\@ifundefined{extrasenglish}{}{\addto\extrasenglish{\switcht@albion}}%
+\@ifundefined{extrasfrenchb}{}{\addto\extrasfrenchb{\switcht@francais}}%
+\@ifundefined{extrasgerman}{}{\addto\extrasgerman{\switcht@deutsch}}%
+}{\switcht@@therlang}%
+}
+\def\homedir{\~{ }}
+
+\def\subtitle#1{\gdef\@subtitle{#1}}
+\clearheadinfo
+
+\renewcommand\maketitle{\newpage
+ \refstepcounter{chapter}%
+ \stepcounter{section}%
+ \setcounter{section}{0}%
+ \setcounter{subsection}{0}%
+ \setcounter{figure}{0}
+ \setcounter{table}{0}
+ \setcounter{equation}{0}
+ \setcounter{footnote}{0}%
+ \begingroup
+ \parindent=\z@
+ \renewcommand\thefootnote{\@fnsymbol\c@footnote}%
+ \if@twocolumn
+ \ifnum \col@number=\@ne
+ \@maketitle
+ \else
+ \twocolumn[\@maketitle]%
+ \fi
+ \else
+ \newpage
+ \global\@topnum\z@ % Prevents figures from going at top of page.
+ \@maketitle
+ \fi
+ \thispagestyle{empty}\@thanks
+%
+ \def\\{\unskip\ \ignorespaces}\def\inst##1{\unskip{}}%
+ \def\thanks##1{\unskip{}}\def\fnmsep{\unskip}%
+ \instindent=\hsize
+ \advance\instindent by-\headlineindent
+% \if!\the\toctitle!\addcontentsline{toc}{title}{\@title}\else
+% \addcontentsline{toc}{title}{\the\toctitle}\fi
+ \if@runhead
+ \if!\the\titlerunning!\else
+ \edef\@title{\the\titlerunning}%
+ \fi
+ \global\setbox\titrun=\hbox{\small\rm\unboldmath\ignorespaces\@title}%
+ \ifdim\wd\titrun>\instindent
+ \typeout{Title too long for running head. Please supply}%
+ \typeout{a shorter form with \string\titlerunning\space prior to
+ \string\maketitle}%
+ \global\setbox\titrun=\hbox{\small\rm
+ Title Suppressed Due to Excessive Length}%
+ \fi
+ \xdef\@title{\copy\titrun}%
+ \fi
+%
+ \if!\the\tocauthor!\relax
+ {\def\and{\noexpand\protect\noexpand\and}%
+ \protected@xdef\toc@uthor{\@author}}%
+ \else
+ \def\\{\noexpand\protect\noexpand\newline}%
+ \protected@xdef\scratch{\the\tocauthor}%
+ \protected@xdef\toc@uthor{\scratch}%
+ \fi
+% \addcontentsline{toc}{author}{\toc@uthor}%
+ \if@runhead
+ \if!\the\authorrunning!
+ \value{@inst}=\value{@auth}%
+ \setcounter{@auth}{1}%
+ \else
+ \edef\@author{\the\authorrunning}%
+ \fi
+ \global\setbox\authrun=\hbox{\small\unboldmath\@author\unskip}%
+ \ifdim\wd\authrun>\instindent
+ \typeout{Names of authors too long for running head. Please supply}%
+ \typeout{a shorter form with \string\authorrunning\space prior to
+ \string\maketitle}%
+ \global\setbox\authrun=\hbox{\small\rm
+ Authors Suppressed Due to Excessive Length}%
+ \fi
+ \xdef\@author{\copy\authrun}%
+ \markboth{\@author}{\@title}%
+ \fi
+ \endgroup
+ \setcounter{footnote}{\fnnstart}%
+ \clearheadinfo}
+%
+\def\@maketitle{\newpage
+ \markboth{}{}%
+ \def\lastand{\ifnum\value{@inst}=2\relax
+ \unskip{} \andname\
+ \else
+ \unskip \lastandname\
+ \fi}%
+ \def\and{\stepcounter{@auth}\relax
+ \ifnum\value{@auth}=\value{@inst}%
+ \lastand
+ \else
+ \unskip,
+ \fi}%
+ \begin{center}%
+ \let\newline\\
+ {\Large \bfseries\boldmath
+ \pretolerance=10000
+ \@title \par}\vskip .8cm
+\if!\@subtitle!\else {\large \bfseries\boldmath
+ \vskip -.65cm
+ \pretolerance=10000
+ \@subtitle \par}\vskip .8cm\fi
+ \setbox0=\vbox{\setcounter{@auth}{1}\def\and{\stepcounter{@auth}}%
+ \def\thanks##1{}\@author}%
+ \global\value{@inst}=\value{@auth}%
+ \global\value{auco}=\value{@auth}%
+ \setcounter{@auth}{1}%
+{\lineskip .5em
+\noindent\ignorespaces
+\@author\vskip.35cm}
+ {\small\institutename}
+ \end{center}%
+ }
+
+% definition of the "\spnewtheorem" command.
+%
+% Usage:
+%
+% \spnewtheorem{env_nam}{caption}[within]{cap_font}{body_font}
+% or \spnewtheorem{env_nam}[numbered_like]{caption}{cap_font}{body_font}
+% or \spnewtheorem*{env_nam}{caption}{cap_font}{body_font}
+%
+% New is "cap_font" and "body_font". It stands for
+% fontdefinition of the caption and the text itself.
+%
+% "\spnewtheorem*" gives a theorem without number.
+%
+% A defined spnewthoerem environment is used as described
+% by Lamport.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\@thmcountersep{}
+\def\@thmcounterend{.}
+
+\def\spnewtheorem{\@ifstar{\@sthm}{\@Sthm}}
+
+% definition of \spnewtheorem with number
+
+\def\@spnthm#1#2{%
+ \@ifnextchar[{\@spxnthm{#1}{#2}}{\@spynthm{#1}{#2}}}
+\def\@Sthm#1{\@ifnextchar[{\@spothm{#1}}{\@spnthm{#1}}}
+
+\def\@spxnthm#1#2[#3]#4#5{\expandafter\@ifdefinable\csname #1\endcsname
+ {\@definecounter{#1}\@addtoreset{#1}{#3}%
+ \expandafter\xdef\csname the#1\endcsname{\expandafter\noexpand
+ \csname the#3\endcsname \noexpand\@thmcountersep \@thmcounter{#1}}%
+ \expandafter\xdef\csname #1name\endcsname{#2}%
+ \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}%
+ \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@spynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
+ {\@definecounter{#1}%
+ \expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}%
+ \expandafter\xdef\csname #1name\endcsname{#2}%
+ \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#3}{#4}}%
+ \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@spothm#1[#2]#3#4#5{%
+ \@ifundefined{c@#2}{\@latexerr{No theorem environment `#2' defined}\@eha}%
+ {\expandafter\@ifdefinable\csname #1\endcsname
+ {\global\@namedef{the#1}{\@nameuse{the#2}}%
+ \expandafter\xdef\csname #1name\endcsname{#3}%
+ \global\@namedef{#1}{\@spthm{#2}{\csname #1name\endcsname}{#4}{#5}}%
+ \global\@namedef{end#1}{\@endtheorem}}}}
+
+\def\@spthm#1#2#3#4{\topsep 7\p@ \@plus2\p@ \@minus4\p@
+\refstepcounter{#1}%
+\@ifnextchar[{\@spythm{#1}{#2}{#3}{#4}}{\@spxthm{#1}{#2}{#3}{#4}}}
+
+\def\@spxthm#1#2#3#4{\@spbegintheorem{#2}{\csname the#1\endcsname}{#3}{#4}%
+ \ignorespaces}
+
+\def\@spythm#1#2#3#4[#5]{\@spopargbegintheorem{#2}{\csname
+ the#1\endcsname}{#5}{#3}{#4}\ignorespaces}
+
+\def\@spbegintheorem#1#2#3#4{\trivlist
+ \item[\hskip\labelsep{#3#1\ #2\@thmcounterend}]#4}
+
+\def\@spopargbegintheorem#1#2#3#4#5{\trivlist
+ \item[\hskip\labelsep{#4#1\ #2}]{#4(#3)\@thmcounterend\ }#5}
+
+% definition of \spnewtheorem* without number
+
+\def\@sthm#1#2{\@Ynthm{#1}{#2}}
+
+\def\@Ynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
+ {\global\@namedef{#1}{\@Thm{\csname #1name\endcsname}{#3}{#4}}%
+ \expandafter\xdef\csname #1name\endcsname{#2}%
+ \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@Thm#1#2#3{\topsep 7\p@ \@plus2\p@ \@minus4\p@
+\@ifnextchar[{\@Ythm{#1}{#2}{#3}}{\@Xthm{#1}{#2}{#3}}}
+
+\def\@Xthm#1#2#3{\@Begintheorem{#1}{#2}{#3}\ignorespaces}
+
+\def\@Ythm#1#2#3[#4]{\@Opargbegintheorem{#1}
+ {#4}{#2}{#3}\ignorespaces}
+
+\def\@Begintheorem#1#2#3{#3\trivlist
+ \item[\hskip\labelsep{#2#1\@thmcounterend}]}
+
+\def\@Opargbegintheorem#1#2#3#4{#4\trivlist
+ \item[\hskip\labelsep{#3#1}]{#3(#2)\@thmcounterend\ }}
+
+\if@envcntsect
+ \def\@thmcountersep{.}
+ \spnewtheorem{theorem}{Theorem}[section]{\bfseries}{\itshape}
+\else
+ \spnewtheorem{theorem}{Theorem}{\bfseries}{\itshape}
+ \if@envcntreset
+ \@addtoreset{theorem}{section}
+ \else
+ \@addtoreset{theorem}{chapter}
+ \fi
+\fi
+
+%definition of divers theorem environments
+\spnewtheorem*{claim}{Claim}{\itshape}{\rmfamily}
+\spnewtheorem*{proof}{Proof}{\itshape}{\rmfamily}
+\if@envcntsame % alle Umgebungen wie Theorem.
+ \def\spn@wtheorem#1#2#3#4{\@spothm{#1}[theorem]{#2}{#3}{#4}}
+\else % alle Umgebungen mit eigenem Zaehler
+ \if@envcntsect % mit section numeriert
+ \def\spn@wtheorem#1#2#3#4{\@spxnthm{#1}{#2}[section]{#3}{#4}}
+ \else % nicht mit section numeriert
+ \if@envcntreset
+ \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4}
+ \@addtoreset{#1}{section}}
+ \else
+ \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4}
+ \@addtoreset{#1}{chapter}}%
+ \fi
+ \fi
+\fi
+\spn@wtheorem{case}{Case}{\itshape}{\rmfamily}
+\spn@wtheorem{conjecture}{Conjecture}{\itshape}{\rmfamily}
+\spn@wtheorem{corollary}{Corollary}{\bfseries}{\itshape}
+\spn@wtheorem{definition}{Definition}{\bfseries}{\itshape}
+\spn@wtheorem{example}{Example}{\itshape}{\rmfamily}
+\spn@wtheorem{exercise}{Exercise}{\itshape}{\rmfamily}
+\spn@wtheorem{lemma}{Lemma}{\bfseries}{\itshape}
+\spn@wtheorem{note}{Note}{\itshape}{\rmfamily}
+\spn@wtheorem{problem}{Problem}{\itshape}{\rmfamily}
+\spn@wtheorem{property}{Property}{\itshape}{\rmfamily}
+\spn@wtheorem{proposition}{Proposition}{\bfseries}{\itshape}
+\spn@wtheorem{question}{Question}{\itshape}{\rmfamily}
+\spn@wtheorem{solution}{Solution}{\itshape}{\rmfamily}
+\spn@wtheorem{remark}{Remark}{\itshape}{\rmfamily}
+
+\def\@takefromreset#1#2{%
+ \def\@tempa{#1}%
+ \let\@tempd\@elt
+ \def\@elt##1{%
+ \def\@tempb{##1}%
+ \ifx\@tempa\@tempb\else
+ \@addtoreset{##1}{#2}%
+ \fi}%
+ \expandafter\expandafter\let\expandafter\@tempc\csname cl@#2\endcsname
+ \expandafter\def\csname cl@#2\endcsname{}%
+ \@tempc
+ \let\@elt\@tempd}
+
+\def\theopargself{\def\@spopargbegintheorem##1##2##3##4##5{\trivlist
+ \item[\hskip\labelsep{##4##1\ ##2}]{##4##3\@thmcounterend\ }##5}
+ \def\@Opargbegintheorem##1##2##3##4{##4\trivlist
+ \item[\hskip\labelsep{##3##1}]{##3##2\@thmcounterend\ }}
+ }
+
+\renewenvironment{abstract}{%
+ \list{}{\advance\topsep by0.35cm\relax\small
+ \leftmargin=1cm
+ \labelwidth=\z@
+ \listparindent=\z@
+ \itemindent\listparindent
+ \rightmargin\leftmargin}\item[\hskip\labelsep
+ \bfseries\abstractname]}
+ {\endlist}
+
+\newdimen\headlineindent % dimension for space between
+\headlineindent=1.166cm % number and text of headings.
+
+\def\ps@headings{\let\@mkboth\@gobbletwo
+ \let\@oddfoot\@empty\let\@evenfoot\@empty
+ \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}%
+ \leftmark\hfil}
+ \def\@oddhead{\normalfont\small\hfil\rightmark\hspace{\headlineindent}%
+ \llap{\thepage}}
+ \def\chaptermark##1{}%
+ \def\sectionmark##1{}%
+ \def\subsectionmark##1{}}
+
+\def\ps@titlepage{\let\@mkboth\@gobbletwo
+ \let\@oddfoot\@empty\let\@evenfoot\@empty
+ \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}%
+ \hfil}
+ \def\@oddhead{\normalfont\small\hfil\hspace{\headlineindent}%
+ \llap{\thepage}}
+ \def\chaptermark##1{}%
+ \def\sectionmark##1{}%
+ \def\subsectionmark##1{}}
+
+\if@runhead\ps@headings\else
+\ps@empty\fi
+
+\setlength\arraycolsep{1.4\p@}
+\setlength\tabcolsep{1.4\p@}
+
+\endinput
+%end of file llncs.cls
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/document/root.tex Thu Nov 25 18:54:45 2010 +0000
@@ -0,0 +1,57 @@
+\documentclass{llncs}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{tikz}
+\usepackage{pgf}
+\usepackage{pdfsetup}
+\usepackage{ot1patch}
+\usepackage{times}
+\usepackage{proof}
+
+
+\urlstyle{rm}
+\isabellestyle{it}
+\renewcommand{\isastyleminor}{\it}%
+\renewcommand{\isastyle}{\normalsize\it}%
+
+
+\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
+\renewcommand{\isasymequiv}{$\dn$}
+\renewcommand{\isasymemptyset}{$\varnothing$}
+\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
+
+\begin{document}
+
+\title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular Expressions}
+\author{Chunhan Wu\inst{1} \and Xingjuan Zhang\inst{1} \and Christian Urban\inst{2}}
+\institute{PLA University, China \and TU Munich, Germany}
+\maketitle
+
+\begin{abstract}
+There are numerous textbooks on regular languages. Nearly all of them
+introduce the subject by describing finite automata and
+only mentioning on the side a connection with regular expressions.
+Unfortunately, automata are a hassle for formalisations in HOL-based
+theorem provers. The reason is they need to be represented as graphs
+or matrices, neither of which can be easily defined as datatype. Also
+operations, such as disjoint union of graphs, are not easily formalisiable
+in HOL. In contrast, regular expressions can be defined easily
+as datatype and a corresponding reasoning infrastructure comes for
+free. We show in this paper that a central result from formal
+language theory---the Myhill-Nerode theorem---can be recreated
+using only regular expressions.
+\end{abstract}
+
+\input{session}
+
+\bibliographystyle{plain}
+\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/ROOT.ML Thu Nov 25 18:54:45 2010 +0000
@@ -0,0 +1,5 @@
+(*show_question_marks := false;*)
+
+no_document use_thy "LaTeXsugar";
+quick_and_dirty := true;
+use_thy "Slides"
\ No newline at end of file
--- a/Slides/ROOT1.ML Thu Nov 18 11:39:17 2010 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-(*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/Slides.thy Thu Nov 25 18:54:45 2010 +0000
@@ -0,0 +1,790 @@
+(*<*)
+theory Slides
+imports "LaTeXsugar"
+begin
+
+notation (latex output)
+ set ("_") and
+ Cons ("_::/_" [66,65] 65)
+
+(*>*)
+
+
+text_raw {*
+ %\renewcommand{\slidecaption}{Cambridge, 9 November 2010}
+ \renewcommand{\slidecaption}{Munich, 17 November 2010}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}
+ \frametitle{%
+ \begin{tabular}{@ {}c@ {}}
+ \LARGE A Formalisation of the\\[-3mm]
+ \LARGE Myhill-Nerode Theorem\\[-3mm]
+ \LARGE based on Regular Expressions\\[-3mm]
+ \large \onslide<2>{\alert{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 {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{In Most Textbooks\ldots}
+
+ \begin{itemize}
+ \item A \alert{regular language} is one where there is a DFA that
+ recognises it.\bigskip\pause
+ \end{itemize}
+
+
+ I can think of three reasons why this is a good definition:\medskip
+ \begin{itemize}
+ \item string matching via DFAs (yacc)
+ \item pumping lemma
+ \item closure properties of regular languages (closed under complement)
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[t]
+ \frametitle{Really Bad News!}
+
+ DFAs are bad news for formalisations in theorem provers. They might
+ be represented as:
+
+ \begin{itemize}
+ \item graphs
+ \item matrices
+ \item partial functions
+ \end{itemize}
+
+ All constructions are messy to reason about.\bigskip\bigskip
+ \pause
+
+ \small
+ \only<2>{Alexander and Tobias: ``\ldots automata theory \ldots does not come for free \ldots''}
+ \only<3>{
+ 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.}
+ \only<4>{typical textbook reasoning goes like: ``\ldots if \smath{M} and \smath{N} are any two
+ automata with no inaccessible states \ldots''
+ }
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[t]
+ \frametitle{Regular Expressions}
+
+ \ldots are a simple datatype:
+
+ \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{0} \\
+ & \smath{\mid} & \smath{[]}\\
+ & \smath{\mid} & \smath{c}\\
+ & \smath{\mid} & \smath{r_1 + r_2}\\
+ & \smath{\mid} & \smath{r_1 \cdot r_2}\\
+ & \smath{\mid} & \smath{r^\star}
+ \end{tabular}
+ \end{center}}
+
+ \only<3->{Induction and recursion principles come for free.}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Semantics of Rexps}
+
+ \begin{center}
+ \begin{tabular}{rcl}
+ \smath{\mathbb{L}(0)} & \smath{=} & \smath{\varnothing}\\
+ \smath{\mathbb{L}([])} & \smath{=} & \smath{\{[]\}}\\
+ \smath{\mathbb{L}(c)} & \smath{=} & \smath{\{[c]\}}\\
+ \smath{\mathbb{L}(r_1 + r_2)} & \smath{=} & \smath{\mathbb{L}(r_1) \cup \mathbb{L}(r_2)}\\
+ \smath{\mathbb{L}(r_1 \cdot r_2)} & \smath{=} & \smath{\mathbb{L}(r_1)\; ;\; \mathbb{L} (r_2)}\\
+ \smath{\mathbb{L}(r^\star)} & \smath{=} & \smath{\mathbb{L}(r)^\star}
+ \end{tabular}
+ \end{center}
+
+ \small
+ \begin{center}
+ \begin{tabular}{rcl}
+ \smath{L_1 ; L_2} & \smath{\dn} & \smath{\{ s_1 @ s_2 \mid s_1 \in L_1 \wedge s_2 \in L_2\}}\bigskip\\
+ \multicolumn{3}{c}{
+ \smath{\infer{[] \in L^\star}{}} \hspace{10mm}
+ \smath{\infer{s_1 @ s_2 \in L^\star}{s_1 \in L & s_2 \in L^\star}}
+ }
+ \end{tabular}
+ \end{center}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{\LARGE Regular Expression Matching}
+
+ \begin{itemize}
+ \item Harper in JFP'99: ``Functional Pearl: Proof- Directed Debugging''\medskip
+ \item Yi in JFP'06: ``Educational Pearl: `Proof-Directed Debugging' revisited
+ for a first-order version''\medskip
+ \item Owens et al in JFP'09: ``Regular-expression derivatives re-examined''\bigskip\pause
+
+ \begin{quote}\small
+ ``Unfortunately, regular expression derivatives have been lost in the
+ sands of time, and few computer scientists are aware of them.''
+ \end{quote}
+ \end{itemize}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+
+ \begin{center}
+ \huge\bf Demo
+ \end{center}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{\LARGE The Myhill-Nerode Theorem}
+
+ \begin{itemize}
+ \item provides necessary and suf\!ficient conditions for a language
+ being regular (pumping lemma only necessary)\medskip
+
+ \item will help with closure properties of regular languages\bigskip\pause
+
+ \item key is the equivalence relation:\smallskip
+ \begin{center}
+ \smath{x \approx_{L} y \,\dn\, \forall z.\; x @ z \in L \Leftrightarrow y @ z \in L}
+ \end{center}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{\LARGE The Myhill-Nerode Theorem}
+
+ \mbox{}\\[5cm]
+
+ \begin{itemize}
+ \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_L) \;\Leftrightarrow\; L\; \text{is regular}}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{\LARGE Equivalence Classes}
+
+ \begin{itemize}
+ \item \smath{L = []}
+ \begin{center}
+ \smath{\Big\{\{[]\},\; U\!N\!IV - \{[]\}\Big\}}
+ \end{center}\bigskip\bigskip
+
+ \item \smath{L = [c]}
+ \begin{center}
+ \smath{\Big\{\{[]\},\; \{[c]\},\; U\!N\!IV - \{[], [c]\}\Big\}}
+ \end{center}\bigskip\bigskip
+
+ \item \smath{L = \varnothing}
+ \begin{center}
+ \smath{\Big\{U\!N\!IV\Big\}}
+ \end{center}
+
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{\LARGE Regular Languages}
+
+ \begin{itemize}
+ \item \smath{L} is regular \smath{\dn} if there is an automaton \smath{M}
+ such that \smath{\mathbb{L}(M) = L}\\[1.5cm]
+
+ \item Myhill-Nerode:
+
+ \begin{center}
+ \begin{tabular}{l}
+ finite $\Rightarrow$ regular\\
+ \;\;\;\smath{\text{finite}\,(U\!N\!IV /\!/ \approx_L) \Rightarrow \exists r. L = \mathbb{L}(r)}\\[3mm]
+ regular $\Rightarrow$ finite\\
+ \;\;\;\smath{\text{finite}\, (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}
+ \end{tabular}
+ \end{center}
+
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{\LARGE Final States}
+
+ \mbox{}\\[3cm]
+
+ \begin{itemize}
+ \item \smath{\text{final}_L\,X \dn}\\
+ \smath{\hspace{6mm}X \in (U\!N\!IV /\!/\approx_L) \;\wedge\; \forall s \in X.\; s \in L}
+ \smallskip
+ \item we can prove: \smath{L = \bigcup \{X.\;\text{final}_L\,X\}}
+
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{\LARGE Transitions between\\[-3mm] Equivalence Classes}
+
+ \smath{L = \{[c]\}}
+
+ \begin{tabular}{@ {\hspace{-7mm}}cc}
+ \begin{tabular}{c}
+ \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick]
+ \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
+
+ %\draw[help lines] (0,0) grid (3,2);
+
+ \node[state,initial] (q_0) {$R_1$};
+ \node[state,accepting] (q_1) [above right of=q_0] {$R_2$};
+ \node[state] (q_2) [below right of=q_0] {$R_3$};
+
+ \path[->] (q_0) edge node {c} (q_1)
+ edge node [swap] {$\Sigma-{c}$} (q_2)
+ (q_2) edge [loop below] node {$\Sigma$} ()
+ (q_1) edge node {$\Sigma$} (q_2);
+ \end{tikzpicture}
+ \end{tabular}
+ &
+ \begin{tabular}[t]{ll}
+ \\[-20mm]
+ \multicolumn{2}{l}{\smath{U\!N\!IV /\!/\approx_L} produces}\\[4mm]
+
+ \smath{R_1}: & \smath{\{[]\}}\\
+ \smath{R_2}: & \smath{\{[c]\}}\\
+ \smath{R_3}: & \smath{U\!N\!IV - \{[], [c]\}}\\[6mm]
+ \multicolumn{2}{l}{\onslide<2->{\smath{X \stackrel{c}{\longrightarrow} Y \dn X ; [c] \subseteq Y}}}
+ \end{tabular}
+
+ \end{tabular}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{\LARGE Systems of Equations}
+
+ Inspired by a method of Brzozowski\;'64, we can build an equational system
+ characterising the equivalence classes:
+
+ \begin{center}
+ \begin{tabular}{@ {\hspace{-20mm}}c}
+ \\[-13mm]
+ \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick]
+ \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
+
+ %\draw[help lines] (0,0) grid (3,2);
+
+ \node[state,initial] (p_0) {$R_1$};
+ \node[state,accepting] (p_1) [right of=q_0] {$R_2$};
+
+ \path[->] (p_0) edge [bend left] node {a} (p_1)
+ edge [loop above] node {b} ()
+ (p_1) edge [loop above] node {a} ()
+ edge [bend left] node {b} (p_0);
+ \end{tikzpicture}\\
+ \\[-13mm]
+ \end{tabular}
+ \end{center}
+
+ \begin{center}
+ \begin{tabular}{@ {\hspace{-6mm}}ll@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+ & \smath{R_1} & \smath{\equiv} & \smath{R_1;b + R_2;b \onslide<2->{\alert<2>{+ \lambda;[]}}}\\
+ & \smath{R_2} & \smath{\equiv} & \smath{R_1;a + R_2;a}\medskip\\
+ \onslide<3->{we can prove}
+ & \onslide<3->{\smath{R_1}} & \onslide<3->{\smath{=}}
+ & \onslide<3->{\smath{R_1; \mathbb{L}(b) \,\cup\, R_2;\mathbb{L}(b) \,\cup\, \{[]\};\{[]\}}}\\
+ & \onslide<3->{\smath{R_2}} & \onslide<3->{\smath{=}}
+ & \onslide<3->{\smath{R_1; \mathbb{L}(a) \,\cup\, R_2;\mathbb{L}(a)}}\\
+ \end{tabular}
+ \end{center}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1>[t]
+ \small
+
+ \begin{center}
+ \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}
+ \onslide<1->{\smath{R_1}} & \onslide<1->{\smath{=}}
+ & \onslide<1->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
+ \onslide<1->{\smath{R_2}} & \onslide<1->{\smath{=}}
+ & \onslide<1->{\smath{R_1; a + R_2; a}}\\
+
+ & & & \onslide<2->{by Arden}\\
+
+ \onslide<2->{\smath{R_1}} & \onslide<2->{\smath{=}}
+ & \onslide<2->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
+ \onslide<2->{\smath{R_2}} & \onslide<2->{\smath{=}}
+ & \only<2>{\smath{R_1; a + R_2; a}}%
+ \only<3->{\smath{R_1; a\cdot a^\star}}\\
+
+ & & & \onslide<4->{by Arden}\\
+
+ \onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}}
+ & \onslide<4->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\
+ \onslide<4->{\smath{R_2}} & \onslide<4->{\smath{=}}
+ & \onslide<4->{\smath{R_1; a\cdot a^\star}}\\
+
+ & & & \onslide<5->{by substitution}\\
+
+ \onslide<5->{\smath{R_1}} & \onslide<5->{\smath{=}}
+ & \onslide<5->{\smath{R_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\
+ \onslide<5->{\smath{R_2}} & \onslide<5->{\smath{=}}
+ & \onslide<5->{\smath{R_1; a\cdot a^\star}}\\
+
+ & & & \onslide<6->{by Arden}\\
+
+ \onslide<6->{\smath{R_1}} & \onslide<6->{\smath{=}}
+ & \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
+ \onslide<6->{\smath{R_2}} & \onslide<6->{\smath{=}}
+ & \onslide<6->{\smath{R_1; a\cdot a^\star}}\\
+
+ & & & \onslide<7->{by substitution}\\
+
+ \onslide<7->{\smath{R_1}} & \onslide<7->{\smath{=}}
+ & \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
+ \onslide<7->{\smath{R_2}} & \onslide<7->{\smath{=}}
+ & \onslide<7->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star
+ \cdot a\cdot a^\star}}\\
+ \end{tabular}
+ \end{center}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{\LARGE A Variant of Arden's Lemma}
+
+ {\bf Arden's Lemma:}\smallskip
+
+ If \smath{[] \not\in A} then
+ \begin{center}
+ \smath{X = X; A + \text{something}}
+ \end{center}
+ has the (unique) solution
+ \begin{center}
+ \smath{X = \text{something} ; A^\star}
+ \end{center}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->[t]
+ \small
+
+ \begin{center}
+ \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}
+ \onslide<1->{\smath{R_1}} & \onslide<1->{\smath{=}}
+ & \onslide<1->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
+ \onslide<1->{\smath{R_2}} & \onslide<1->{\smath{=}}
+ & \onslide<1->{\smath{R_1; a + R_2; a}}\\
+
+ & & & \onslide<2->{by Arden}\\
+
+ \onslide<2->{\smath{R_1}} & \onslide<2->{\smath{=}}
+ & \onslide<2->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
+ \onslide<2->{\smath{R_2}} & \onslide<2->{\smath{=}}
+ & \only<2>{\smath{R_1; a + R_2; a}}%
+ \only<3->{\smath{R_1; a\cdot a^\star}}\\
+
+ & & & \onslide<4->{by Arden}\\
+
+ \onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}}
+ & \onslide<4->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\
+ \onslide<4->{\smath{R_2}} & \onslide<4->{\smath{=}}
+ & \onslide<4->{\smath{R_1; a\cdot a^\star}}\\
+
+ & & & \onslide<5->{by substitution}\\
+
+ \onslide<5->{\smath{R_1}} & \onslide<5->{\smath{=}}
+ & \onslide<5->{\smath{R_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\
+ \onslide<5->{\smath{R_2}} & \onslide<5->{\smath{=}}
+ & \onslide<5->{\smath{R_1; a\cdot a^\star}}\\
+
+ & & & \onslide<6->{by Arden}\\
+
+ \onslide<6->{\smath{R_1}} & \onslide<6->{\smath{=}}
+ & \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
+ \onslide<6->{\smath{R_2}} & \onslide<6->{\smath{=}}
+ & \onslide<6->{\smath{R_1; a\cdot a^\star}}\\
+
+ & & & \onslide<7->{by substitution}\\
+
+ \onslide<7->{\smath{R_1}} & \onslide<7->{\smath{=}}
+ & \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
+ \onslide<7->{\smath{R_2}} & \onslide<7->{\smath{=}}
+ & \onslide<7->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star
+ \cdot a\cdot a^\star}}\\
+ \end{tabular}
+ \end{center}
+
+ \only<8->{
+ \begin{textblock}{6}(2.5,4)
+ \begin{block}{}
+ \begin{minipage}{8cm}\raggedright
+
+ \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick, inner sep=1mm]
+ \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
+
+ %\draw[help lines] (0,0) grid (3,2);
+
+ \node[state,initial] (p_0) {$R_1$};
+ \node[state,accepting] (p_1) [right of=q_0] {$R_2$};
+
+ \path[->] (p_0) edge [bend left] node {a} (p_1)
+ edge [loop above] node {b} ()
+ (p_1) edge [loop above] node {a} ()
+ edge [bend left] node {b} (p_0);
+ \end{tikzpicture}
+
+ \end{minipage}
+ \end{block}
+ \end{textblock}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{\LARGE The Equ's Solving Algorithm}
+
+ \begin{itemize}
+ \item The algorithm must terminate: Arden makes one equation smaller;
+ substitution deletes one variable from the right-hand sides.\bigskip
+
+ \item We need to maintain the invariant that Arden is applicable
+ (if \smath{[] \not\in A} then \ldots):\medskip
+
+ \begin{center}\small
+ \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}
+ \smath{R_1} & \smath{=} & \smath{R_1; b + R_2; b + \lambda;[]}\\
+ \smath{R_2} & \smath{=} & \smath{R_1; a + R_2; a}\\
+
+ & & & by Arden\\
+
+ \smath{R_1} & \smath{=} & \smath{R_1; b + R_2; b + \lambda;[]}\\
+ \smath{R_2} & \smath{=} & \smath{R_1; a\cdot a^\star}\\
+ \end{tabular}
+ \end{center}
+
+ \end{itemize}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{\LARGE The Equ's Solving Algorithm}
+
+ \begin{itemize}
+ \item The algorithm is still a bit hairy to formalise because of our set-representation
+ for equations:
+
+ \begin{center}
+ \begin{tabular}{ll}
+ \smath{\big\{ (X, \{(Y_1, r_1), (Y_2, r_2), \ldots\}),}\\
+ \mbox{}\hspace{5mm}\smath{\ldots}\\
+ & \smath{\big\}}
+ \end{tabular}
+ \end{center}\bigskip\pause
+
+ \small
+ they are generated from \smath{U\!N\!IV /\!/ \approx_L}
+
+ \end{itemize}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{\LARGE Other Direction}
+
+ One has to prove
+
+ \begin{center}
+ \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}
+ \end{center}
+
+ by induction on \smath{r}. Not trivial, but after a bit
+ of thinking (by Chunhan), one can prove that if
+
+ \begin{center}
+ \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1)})}\hspace{5mm}
+ \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_2)})}
+ \end{center}
+
+ then
+
+ \begin{center}
+ \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1) \,\cup\, \mathbb{L}(r_2)})}
+ \end{center}
+
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{\LARGE What Have We Achieved?}
+
+ \begin{itemize}
+ \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_L) \;\Leftrightarrow\; L\; \text{is regular}}
+ \bigskip\pause
+ \item regular languages are closed under complementation; this is easy
+ \begin{center}
+ \smath{U\!N\!IV /\!/ \approx_L \;\;=\;\; U\!N\!IV /\!/ \approx_{-L}}
+ \end{center}\pause\bigskip
+
+ \item if you want to do regular expression matching (see Scott's paper)\pause\bigskip
+
+ \item I cannot yet give definite numbers
+ \end{itemize}
+
+ \only<2>{
+ \begin{textblock}{10}(4,14)
+ \small
+ \smath{x \approx_{L} y \,\dn\, \forall z.\; x @ z \in L \Leftrightarrow y @ z \in L}
+ \end{textblock}
+ }
+
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{\LARGE Examples}
+
+ \begin{itemize}
+ \item \smath{L \equiv \Sigma^\star 0 \Sigma} is regular
+ \begin{quote}\small
+ \begin{tabular}{lcl}
+ \smath{A_1} & \smath{=} & \smath{\Sigma^\star 00}\\
+ \smath{A_2} & \smath{=} & \smath{\Sigma^\star 01}\\
+ \smath{A_3} & \smath{=} & \smath{\Sigma^\star 10 \cup \{0\}}\\
+ \smath{A_4} & \smath{=} & \smath{\Sigma^\star 11 \cup \{1\} \cup \{[]\}}\\
+ \end{tabular}
+ \end{quote}
+
+ \item \smath{L \equiv \{ 0^n 1^n \,|\, n \ge 0\}} is not regular
+ \begin{quote}\small
+ \begin{tabular}{lcl}
+ \smath{B_0} & \smath{=} & \smath{\{0^n 1^n \,|\, n \ge 0\}}\\
+ \smath{B_1} & \smath{=} & \smath{\{0^n 1^{(n-1)} \,|\, n \ge 1\}}\\
+ \smath{B_2} & \smath{=} & \smath{\{0^n 1^{(n-2)} \,|\, n \ge 2\}}\\
+ \smath{B_3} & \smath{=} & \smath{\{0^n 1^{(n-3)} \,|\, n \ge 3\}}\\
+ & \smath{\vdots} &\\
+ \end{tabular}
+ \end{quote}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{\LARGE What We Have Not Achieved}
+
+ \begin{itemize}
+ \item regular expressions are not good if you look for a minimal
+ one for a language (DFAs have this notion)\pause\bigskip
+
+ \item Is there anything to be said about context free languages:\medskip
+
+ \begin{quote}
+ A context free language is where every string can be recognised by
+ a pushdown automaton.
+ \end{quote}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{\LARGE Conclusion}
+
+ \begin{itemize}
+ \item on balance regular expression are superior
+ to DFAs, in my opinion\bigskip
+
+ \item I cannot think of a reason to not teach regular languages
+ to students this way (!?)\bigskip
+
+ \item I have never ever seen a proof of Myhill-Nerode based on
+ regular expressions\bigskip
+
+ \item no application, but lots of fun\bigskip
+
+ \item great source of examples
+
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+(*<*)
+end
+(*>*)
\ No newline at end of file
--- a/Slides/Slides1.thy Thu Nov 18 11:39:17 2010 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,699 +0,0 @@
-(*<*)
-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\\[-3mm]
- \LARGE Myhill-Nerode Theorem\\[-3mm]
- \LARGE based on Regular Expressions\\[-3mm]
- \large \onslide<2>{\alert{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 {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \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 {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[t]
- \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
- \only<2>{
- 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.}
- \only<3>{typical textbook reasoning goes like: ``\ldots if \smath{M} and \smath{N} are any two
- automata with no inaccessible states \ldots''
- }
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[t]
- \frametitle{Regular Expressions}
-
- \ldots are a simple datatype:
-
- \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{0} \\
- & \smath{\mid} & \smath{[]}\\
- & \smath{\mid} & \smath{c}\\
- & \smath{\mid} & \smath{r_1 + r_2}\\
- & \smath{\mid} & \smath{r_1 \cdot r_2}\\
- & \smath{\mid} & \smath{r^\star}
- \end{tabular}
- \end{center}}
-
- \only<3->{Induction and recursion principles come for free.}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Semantics of Rexps}
-
- \begin{center}
- \begin{tabular}{rcl}
- \smath{\mathbb{L}(0)} & \smath{=} & \smath{\varnothing}\\
- \smath{\mathbb{L}([])} & \smath{=} & \smath{\{[]\}}\\
- \smath{\mathbb{L}(c)} & \smath{=} & \smath{\{[c]\}}\\
- \smath{\mathbb{L}(r_1 + r_2)} & \smath{=} & \smath{\mathbb{L}(r_1) \cup \mathbb{L}(r_2)}\\
- \smath{\mathbb{L}(r_1 \cdot r_2)} & \smath{=} & \smath{\mathbb{L}(r_1)\; ;\; \mathbb{L} (r_2)}\\
- \smath{\mathbb{L}(r^\star)} & \smath{=} & \smath{\mathbb{L}(r)^\star}
- \end{tabular}
- \end{center}
-
- \small
- \begin{center}
- \begin{tabular}{rcl}
- \smath{L_1 ; L_2} & \smath{\dn} & \smath{\{ s_1 @ s_2 \mid s_1 \in L_1 \wedge s_2 \in L_2\}}\bigskip\\
- \multicolumn{3}{c}{
- \smath{\infer{[] \in L^\star}{}} \hspace{10mm}
- \smath{\infer{s_1 @ s_2 \in L^\star}{s_1 \in L & s_2 \in L^\star}}
- }
- \end{tabular}
- \end{center}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE Regular Expression Matching}
-
- \begin{itemize}
- \item Harper in JFP'99: ``Functional Pearl: Proof- Directed Debugging''\medskip
- \item Yi in JFP'06: ``Educational Pearl: `Proof-Directed Debugging' revisited
- for a first-order version''\medskip
- \item Owens et al in JFP'09: ``Regular-expression derivatives re-examined''\bigskip\pause
-
- \begin{quote}\small
- ``Unfortunately, regular expression derivatives have been lost in the
- sands of time, and few computer scientists are aware of them.''
- \end{quote}
- \end{itemize}
-
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
-
- \begin{center}
- \huge\bf Demo
- \end{center}
-
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE The Myhill-Nerode Theorem}
-
- \begin{itemize}
- \item will help with closure properties of regular languages and
- with the pumping lemma.\medskip
-
- \item provides necessary and suf\!ficient conditions for a language being
- regular\bigskip\pause
-
- \begin{center}
- \smath{x \approx_{L} y \,\dn\, \forall z.\; x @ z \in L \Leftrightarrow y @ z \in L}
- \end{center}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE The Myhill-Nerode Theorem}
-
- \mbox{}\\[5cm]
-
- \begin{itemize}
- \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_L) \;\Leftrightarrow\; L\; \text{is regular}}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE Equivalence Classes}
-
- \begin{itemize}
- \item \smath{L = []}
- \begin{center}
- \smath{\Big\{\{[]\},\; U\!N\!IV - \{[]\}\Big\}}
- \end{center}\bigskip\bigskip
-
- \item \smath{L = [c]}
- \begin{center}
- \smath{\Big\{\{[]\},\; \{[c]\},\; U\!N\!IV - \{[], [c]\}\Big\}}
- \end{center}\bigskip\bigskip
-
- \item \smath{L = \varnothing}
- \begin{center}
- \smath{\Big\{U\!N\!IV\Big\}}
- \end{center}
-
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE Regular Languages}
-
- \begin{itemize}
- \item \smath{L} is regular \smath{\dn} if there is an automaton \smath{M}
- such that \smath{\mathbb{L}(M) = L}\\[1.5cm]
-
- \item Myhill-Nerode:
-
- \begin{center}
- \begin{tabular}{l}
- finite $\Rightarrow$ regular\\
- \;\;\;\smath{\text{finite}\,(U\!N\!IV /\!/ \approx_L) \Rightarrow \exists r. L = \mathbb{L}(r)}\\[3mm]
- regular $\Rightarrow$ finite\\
- \;\;\;\smath{\text{finite}\, (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}
- \end{tabular}
- \end{center}
-
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE Final States}
-
- \mbox{}\\[3cm]
-
- \begin{itemize}
- \item \smath{\text{final}_L\,X \dn}\\
- \smath{\hspace{6mm}X \in (U\!N\!IV /\!/\approx_L) \;\wedge\; \forall s \in X.\; s \in L}
- \smallskip
- \item we can prove: \smath{L = \bigcup \{X.\;\text{final}_L\,X\}}
-
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE Transitions between\\[-3mm] Equivalence Classes}
-
- \smath{L = \{[c]\}}
-
- \begin{tabular}{@ {\hspace{-7mm}}cc}
- \begin{tabular}{c}
- \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick]
- \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
-
- %\draw[help lines] (0,0) grid (3,2);
-
- \node[state,initial] (q_0) {$R_1$};
- \node[state,accepting] (q_1) [above right of=q_0] {$R_2$};
- \node[state] (q_2) [below right of=q_0] {$R_3$};
-
- \path[->] (q_0) edge node {c} (q_1)
- edge node [swap] {$\Sigma-{c}$} (q_2)
- (q_2) edge [loop below] node {$\Sigma$} ();
- \end{tikzpicture}
- \end{tabular}
- &
- \begin{tabular}[t]{ll}
- \\[-20mm]
- \multicolumn{2}{l}{\smath{U\!N\!IV /\!/\approx_L} produces}\\[4mm]
-
- \smath{R_1}: & \smath{\{[]\}}\\
- \smath{R_2}: & \smath{\{[c]\}}\\
- \smath{R_3}: & \smath{U\!N\!IV - \{[], [c]\}}\\[6mm]
- \multicolumn{2}{l}{\onslide<2->{\smath{X \stackrel{c}{\longrightarrow} Y \dn X ; [c] \subseteq Y}}}
- \end{tabular}
-
- \end{tabular}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE Systems of Equations}
-
- Inspired by a method of Brzozowski\;'64, we can build an equational system
- characterising the equivalence classes:
-
- \begin{center}
- \begin{tabular}{@ {\hspace{-20mm}}c}
- \\[-13mm]
- \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick]
- \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
-
- %\draw[help lines] (0,0) grid (3,2);
-
- \node[state,initial] (p_0) {$R_1$};
- \node[state,accepting] (p_1) [right of=q_0] {$R_2$};
-
- \path[->] (p_0) edge [bend left] node {a} (p_1)
- edge [loop above] node {b} ()
- (p_1) edge [loop above] node {a} ()
- edge [bend left] node {b} (p_0);
- \end{tikzpicture}\\
- \\[-13mm]
- \end{tabular}
- \end{center}
-
- \begin{center}
- \begin{tabular}{@ {\hspace{-6mm}}ll@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
- & \smath{R_1} & \smath{\equiv} & \smath{R_1;b + R_2;b \onslide<2->{\alert<2>{+ \lambda;[]}}}\\
- & \smath{R_2} & \smath{\equiv} & \smath{R_1;a + R_2;a}\medskip\\
- \onslide<3->{we can prove}
- & \onslide<3->{\smath{R_1}} & \onslide<3->{\smath{=}}
- & \onslide<3->{\smath{R_1; \mathbb{L}(b) \,\cup\, R_2;\mathbb{L}(b) \,\cup\, \{[]\};\{[]\}}}\\
- & \onslide<3->{\smath{R_2}} & \onslide<3->{\smath{=}}
- & \onslide<3->{\smath{R_1; \mathbb{L}(a) \,\cup\, R_2;\mathbb{L}(a)}}\\
- \end{tabular}
- \end{center}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1>[t]
- \small
-
- \begin{center}
- \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}
- \onslide<1->{\smath{R_1}} & \onslide<1->{\smath{=}}
- & \onslide<1->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
- \onslide<1->{\smath{R_2}} & \onslide<1->{\smath{=}}
- & \onslide<1->{\smath{R_1; a + R_2; a}}\\
-
- & & & \onslide<2->{by Arden}\\
-
- \onslide<2->{\smath{R_1}} & \onslide<2->{\smath{=}}
- & \onslide<2->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
- \onslide<2->{\smath{R_2}} & \onslide<2->{\smath{=}}
- & \only<2>{\smath{R_1; a + R_2; a}}%
- \only<3->{\smath{R_1; a\cdot a^\star}}\\
-
- & & & \onslide<3->{by Arden}\\
-
- \onslide<3->{\smath{R_1}} & \onslide<3->{\smath{=}}
- & \onslide<3->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\
- \onslide<3->{\smath{R_2}} & \onslide<3->{\smath{=}}
- & \onslide<3->{\smath{R_1; a\cdot a^\star}}\\
-
- & & & \onslide<4->{by substitution}\\
-
- \onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}}
- & \onslide<4->{\smath{R_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\
- \onslide<4->{\smath{R_2}} & \onslide<4->{\smath{=}}
- & \onslide<4->{\smath{R_1; a\cdot a^\star}}\\
-
- & & & \onslide<5->{by Arden}\\
-
- \onslide<5->{\smath{R_1}} & \onslide<5->{\smath{=}}
- & \onslide<5->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
- \onslide<5->{\smath{R_2}} & \onslide<5->{\smath{=}}
- & \onslide<5->{\smath{R_1; a\cdot a^\star}}\\
-
- & & & \onslide<6->{by substitution}\\
-
- \onslide<6->{\smath{R_1}} & \onslide<6->{\smath{=}}
- & \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
- \onslide<6->{\smath{R_2}} & \onslide<6->{\smath{=}}
- & \onslide<6->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star
- \cdot a\cdot a^\star}}\\
- \end{tabular}
- \end{center}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE A Variant of Arden's Lemma}
-
- {\bf Arden's Lemma:}
-
- If \smath{[] \not\in A} then
- \begin{center}
- \smath{X = X; A + \text{something}}
- \end{center}
- has the (unique) solution
- \begin{center}
- \smath{X = \text{something} ; A^\star}
- \end{center}
-
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1->[t]
- \small
-
- \begin{center}
- \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}
- \onslide<1->{\smath{R_1}} & \onslide<1->{\smath{=}}
- & \onslide<1->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
- \onslide<1->{\smath{R_2}} & \onslide<1->{\smath{=}}
- & \onslide<1->{\smath{R_1; a + R_2; a}}\\
-
- & & & \onslide<2->{by Arden}\\
-
- \onslide<2->{\smath{R_1}} & \onslide<2->{\smath{=}}
- & \onslide<2->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
- \onslide<2->{\smath{R_2}} & \onslide<2->{\smath{=}}
- & \only<2>{\smath{R_1; a + R_2; a}}%
- \only<3->{\smath{R_1; a\cdot a^\star}}\\
-
- & & & \onslide<3->{by Arden}\\
-
- \onslide<3->{\smath{R_1}} & \onslide<3->{\smath{=}}
- & \onslide<3->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\
- \onslide<3->{\smath{R_2}} & \onslide<3->{\smath{=}}
- & \onslide<3->{\smath{R_1; a\cdot a^\star}}\\
-
- & & & \onslide<4->{by substitution}\\
-
- \onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}}
- & \onslide<4->{\smath{R_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\
- \onslide<4->{\smath{R_2}} & \onslide<4->{\smath{=}}
- & \onslide<4->{\smath{R_1; a\cdot a^\star}}\\
-
- & & & \onslide<5->{by Arden}\\
-
- \onslide<5->{\smath{R_1}} & \onslide<5->{\smath{=}}
- & \onslide<5->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
- \onslide<5->{\smath{R_2}} & \onslide<5->{\smath{=}}
- & \onslide<5->{\smath{R_1; a\cdot a^\star}}\\
-
- & & & \onslide<6->{by substitution}\\
-
- \onslide<6->{\smath{R_1}} & \onslide<6->{\smath{=}}
- & \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
- \onslide<6->{\smath{R_2}} & \onslide<6->{\smath{=}}
- & \onslide<6->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star
- \cdot a\cdot a^\star}}\\
-
- & & & \onslide<7->{\alert{solved form}}\\
- \end{tabular}
- \end{center}
-
- \only<8->{
- \begin{textblock}{6}(2.5,4)
- \begin{block}{}
- \begin{minipage}{8cm}\raggedright
-
- \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick, inner sep=1mm]
- \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
-
- %\draw[help lines] (0,0) grid (3,2);
-
- \node[state,initial] (p_0) {$R_1$};
- \node[state,accepting] (p_1) [right of=q_0] {$R_2$};
-
- \path[->] (p_0) edge [bend left] node {a} (p_1)
- edge [loop above] node {b} ()
- (p_1) edge [loop above] node {a} ()
- edge [bend left] node {b} (p_0);
- \end{tikzpicture}
-
- \end{minipage}
- \end{block}
- \end{textblock}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE The Equ's Solving Algorithm}
-
- \begin{itemize}
- \item The algorithm must terminate: Arden makes one equation smaller;
- substitution deletes one variable from the right-hand sides.\bigskip
-
- \item This is still a bit hairy to formalise because of our set-representation
- for equations:
-
- \begin{center}
- \begin{tabular}{ll}
- \smath{\big\{ (X, \{(Y_1, r_1), (Y_2, r_2), \ldots\}),}\\
- \mbox{}\hspace{5mm}\smath{\ldots}\\
- & \smath{\big\}}
- \end{tabular}
- \end{center}\pause
-
- \small
- They are generated from \smath{U\!N\!IV /\!/ \approx_L}
-
- \end{itemize}
-
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE Other Direction}
-
- One has to prove
-
- \begin{center}
- \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}
- \end{center}
-
- by induction on \smath{r}. Not trivial, but after a bit
- of thinking (by Chunhan), one can prove that if
-
- \begin{center}
- \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1)})}\hspace{5mm}
- \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_2)})}
- \end{center}
-
- then
-
- \begin{center}
- \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1) \,\cup\, \mathbb{L}(r_2)})}
- \end{center}
-
-
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE What Have We Achieved?}
-
- \begin{itemize}
- \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_L) \;\Leftrightarrow\; L\; \text{is regular}}
- \bigskip\pause
- \item regular languages are closed under `inversion'
- \begin{center}
- \smath{U\!N\!IV /\!/ \approx_L \;\;=\;\; U\!N\!IV /\!/ \approx_{-L}}
- \end{center}\pause\bigskip
-
- \item regular expressions are not good if you look for a minimal
- one of a language (DFA have this notion)\pause\bigskip
-
- \item if you want to do regular expression matching (see Scott's paper)
- \end{itemize}
-
-
-
- \only<2>{
- \begin{textblock}{10}(4,14)
- \small
- \smath{x \approx_{L} y \,\dn\, \forall z.\; x @ z \in L \Leftrightarrow y @ z \in L}
- \end{textblock}
- }
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE Conclusion}
-
- \begin{itemize}
- \item on balance regular expression are superior to DFAs\bigskip
-
- \item I cannot think of a reason to not teach regular languages
- to students this way\bigskip
-
- \item I have never ever seen a proof of Myhill-Nerode based on
- regular expressions\bigskip
-
- \item no application, but a lot of fun\bigskip
-
- \item great source of examples
-
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-(*<*)
-end
-(*>*)
\ No newline at end of file