
diff -r a0bcf886b8ef -r 8c4b6fb43ebe Journal/Paper.thy
--- a/Journal/Paper.thy	Fri Jul 05 12:07:48 2013 +0100
+++ b/Journal/Paper.thy	Fri Jul 05 17:19:17 2013 +0100
@@ -3,6 +3,18 @@
 imports "../Closures2" "../Attic/Prefix_subtract" 
 begin
 
+lemma nullable_iff:
+  shows "nullable r \<longleftrightarrow> [] \<in> lang r"
+by (induct r) (auto simp add: conc_def split: if_splits)
+
+lemma Deriv_deriv:
+  shows "Deriv c (lang r) = lang (deriv c r)"
+by (induct r) (simp_all add: nullable_iff)
+
+lemma Derivs_derivs:
+  shows "Derivs s (lang r) = lang (derivs s r)"
+by (induct s arbitrary: r) (simp_all add: Deriv_deriv)
+
 declare [[show_question_marks = false]]
 
 consts
@@ -218,7 +230,7 @@
 
   A popular choice for a theorem prover would be one based on Higher-Order
   Logic (HOL), for example HOL4, HOLlight or Isabelle/HOL. For the development
-  presented in this paper we will use the Isabelle/HOL. HOL is a predicate calculus
+  presented in this paper we will use the Isabelle/HOL system. HOL is a predicate calculus
   that allows quantification over predicate variables. Its type system is
   based on the Simple Theory of Types by \citeN{Church40}.  Although many
   mathematical concepts can be conveniently expressed in HOL, there are some
@@ -231,10 +243,10 @@
   define most notions in terms of them.  For example, a regular language is
   normally defined as:
 
-  \begin{dfntn}\label{baddef}
+  \begin{definition}\label{baddef}
   A language @{text A} is \emph{regular}, provided there is a 
   finite deterministic automaton that recognises all strings of @{text "A"}.
-  \end{dfntn}
+  \end{definition}
 
   \noindent  
   This approach has many benefits. Among them is the fact that it is easy to
@@ -388,9 +400,9 @@
   the link between regular expressions and automata in the context of
   lexing. \citeN{BerghoferReiter09} use functions as well for formalising automata
   working over bit strings in the context of Presburger arithmetic.  
-  A Larger formalisation of automata theory, including the Myhill-Nerode theorem, 
+  A larger formalisation of automata theory, including the Myhill-Nerode theorem, 
   was carried out in Nuprl by \citeN{Constable00} which also uses functions.
-  Other large formailsations of automata theory in Coq are by 
+  Other large formalisations of automata theory in Coq are by 
   \citeN{Filliatre97} who essentially uses graphs and by \citeN{Almeidaetal10}
   and \citeN{Braibant12}, who both use matrices. Many of these works,
   like \citeN{Nipkow98} or \citeN{Braibant12}, mention intrinsic problems with 
@@ -423,24 +435,45 @@
   exists an automaton that recognises all its strings, we define a
   regular language as:
 
-  \begin{dfntn}\label{regular}
+  \begin{definition}\label{regular}
   A language @{text A} is \emph{regular}, provided there is a regular expression 
   that matches all strings of @{text "A"}.
-  \end{dfntn}
+  \end{definition}
   
   \noindent
-  And then `forget' automata completely.
-  The reason is that regular expressions %, unlike graphs, matrices and
-  %functions, 
-  can be defined as an inductive datatype and a reasoning
-  infrastructure for them (like induction and recursion) comes for free in
-  HOL. %Moreover, no side-conditions will be needed for regular expressions,
+  We then want to `forget' automata completely and see how far we come
+  with formalising results from regular language theory.  The reason 
+  is that regular expressions, unlike graphs, matrices and
+  functions, can be defined as an inductive datatype and a reasoning
+  infrastructure for them (like induction and recursion) comes for
+  free in HOL. But this question whether formal language theory can be
+  done without automata crops up also in non-theorem prover
+  contexts. For example, Gasarch asked in the Computational Complexity
+  blog by \citeN{GasarchBlog} whether the complementation of
+  regular-expression languages can be proved without using
+  automata. He concluded
+
+  \begin{quote}
+  ``{\it \ldots it can't be done}''
+  \end{quote} 
+
+  \noindent
+  and even pondered
+
+  \begin{quote}
+  ``{\it \ldots [b]ut is there a rigorous way to even state that?}'' 
+  \end{quote} 
+
+  %Moreover, no side-conditions will be needed for regular expressions,
   %like we need for automata. 
-  This convenience of regular expressions has
+  \noindent
+  We will give an answer to these questions in this paper.
+
+  The convenience of regular expressions has
   recently been exploited in HOL4 with a formalisation of regular expression
   matching based on derivatives by \citeN{OwensSlind08}, and with an equivalence
   checker for regular expressions in Isabelle/HOL by \citeN{KraussNipkow11}
-  and in Matida by \citeN{Asperti12} and in Coq by \citeN{CoquandSiles12}.  The
+  and in Matita by \citeN{Asperti12} and in Coq by \citeN{CoquandSiles12}.  The
   main purpose of this paper is to show that a central result about regular
   languages---the Myhill-Nerode Theorem---can be recreated by only using
   regular expressions. This theorem gives necessary and sufficient conditions
@@ -458,13 +491,13 @@
   an argument about solving equational systems.  This argument appears to be
   folklore. For the other part, we give two proofs: one direct proof using
   certain tagging-functions, and another indirect proof using Antimirov's
-  partial derivatives \citeyear{Antimirov95}. Again to our best knowledge, the
+  partial derivatives (\citeyear{Antimirov95}). Again to our best knowledge, the
   tagging-functions have not been used before for establishing the Myhill-Nerode
   Theorem. Derivatives of regular expressions have been used recently quite
   widely in the literature; partial derivatives, in contrast, attract much
   less attention. However, partial derivatives are more suitable in the
-  context of the Myhill-Nerode Theorem, since it is easier to establish
-  formally their finiteness result. We are not aware of any proof that uses
+  context of the Myhill-Nerode Theorem, since it is easier to 
+  formally establish their finiteness result. We are not aware of any proof that uses
   either of them for proving the Myhill-Nerode Theorem.
 *}
 
@@ -499,16 +532,16 @@
   In the paper
   we will make use of the following properties of these constructions.
   
-  \begin{prpstn}\label{langprops}\mbox{}\\
+  \begin{proposition}\label{langprops}\mbox{}\\
   \begin{tabular}{@ {}lp{10cm}}
   (i)   & @{thm star_unfold_left}     \\ 
   (ii)  & @{thm[mode=IfThen] pow_length}\\
   (iii) & @{thm conc_Union_left} \\ 
   (iv)  & If @{thm (prem 1) star_decom} and @{thm (prem 2) star_decom} then
           there exists an @{text "x\<^isub>p"} and @{text "x\<^isub>s"} with @{text "x = x\<^isub>p @ x\<^isub>s"} 
-          and @{term "x\<^isub>p \<noteq> []"} such that @{term "x\<^isub>p \<in> A"} and @{term "x\<^isub>s \<in> A\<star>"}.
+          and \mbox{@{term "x\<^isub>p \<noteq> []"}} such that @{term "x\<^isub>p \<in> A"} and @{term "x\<^isub>s \<in> A\<star>"}.
   \end{tabular}
-  \end{prpstn}
+  \end{proposition}
 
   \noindent
   In @{text "(ii)"} we use the notation @{term "length s"} for the length of a
@@ -534,16 +567,19 @@
   which solves equations of the form @{term "X = A \<cdot> X \<union> B"} provided
   @{term "[] \<notin> A"}. However we will need the following `reversed' 
   version of Arden's Lemma (`reversed' in the sense of changing the order of @{term "A \<cdot> X"} to
-  \mbox{@{term "X \<cdot> A"}}).\footnote{The details of the proof for the reversed Arden's Lemma
-  are given in the Appendix.}
+  \mbox{@{term "X \<cdot> A"}}).
+  %\footnote{The details of the proof for the reversed Arden's Lemma
+  %are given in the Appendix.}
 
-  \begin{lmm}[Reversed Arden's Lemma]\label{arden}\mbox{}\\
+  \begin{lemma}[Reversed Arden's Lemma]\label{arden}\mbox{}\\
   If @{thm (prem 1) reversed_Arden} then
   @{thm (lhs) reversed_Arden} if and only if
   @{thm (rhs) reversed_Arden}.
-  \end{lmm}
+  \end{lemma}
 
   \noindent
+  The proof of this reversed version of Arden's lemma follows the proof of the
+  original version.
   Regular expressions are defined as the inductive datatype
 
   \begin{center}
@@ -576,7 +612,7 @@
 
   Given a finite set of regular expressions @{text rs}, we will make use of the operation of generating 
   a regular expression that matches the union of all languages of @{text rs}. 
-  This definion is not trivial in a theorem prover, because @{text rs} (being a set) is unordered, 
+  This definition is not trivial in a theorem prover, because @{text rs} (being a set) is unordered, 
   but the regular expression needs an order. Since 
   we only need to know the 
   existence
@@ -607,17 +643,17 @@
 text {*
   \noindent
   The key definition in the Myhill-Nerode Theorem is the
-  \emph{Myhill-Nerode Relation}, which states that w.r.t.~a language two 
-  strings are related, provided there is no distinguishing extension in this
+  \emph{Myhill-Nerode Relation}, which states that  two 
+  strings are related w.r.t.~a language, provided there is no distinguishing extension in this
   language. This can be defined as a ternary relation.
 
-  \begin{dfntn}[Myhill-Nerode Relation]\label{myhillneroderel} 
+  \begin{definition}[Myhill-Nerode Relation]\label{myhillneroderel} 
   Given a language @{text A}, two strings @{text x} and
   @{text y} are Myhill-Nerode related provided
   \begin{center}
   @{thm str_eq_def'}
   \end{center}
-  \end{dfntn}
+  \end{definition}
 
   \noindent
   It is easy to see that @{term "\<approx>A"} is an equivalence relation, which
@@ -640,13 +676,13 @@
   that if there are finitely many equivalence classes, like in the example above, then 
   the language is regular. In our setting we therefore have to show:
   
-  \begin{thrm}\label{myhillnerodeone}
+  \begin{theorem}\label{myhillnerodeone}
   @{thm[mode=IfThen] Myhill_Nerode1}
-  \end{thrm}
+  \end{theorem}
 
   \noindent
   To prove this theorem, we first define the set @{term "finals A"} as those equivalence
-  classes from @{term "UNIV // \<approx>A"} that contain strings of @{text A}, namely
+  classes from \mbox{@{term "UNIV // \<approx>A"}} that contain strings of @{text A}, namely
   %
   \begin{equation} 
   @{thm finals_def}
@@ -683,8 +719,11 @@
   \noindent
   which means that if we append the character @{text c} to the end of all 
   strings in the equivalence class @{text Y}, we obtain a subset of 
-  @{text X}. Note that we do not define an automaton here, we merely relate two sets
-  (with the help of a character). In our concrete example we have 
+  @{text X}. 
+  %Note that we do not define formally an automaton here, 
+  %we merely relate two sets
+  %(with the help of a character). 
+  In our concrete example we have 
   @{term "X\<^isub>1 \<Turnstile>c\<Rightarrow> X\<^isub>2"}, @{term "X\<^isub>1 \<Turnstile>d\<^isub>i\<Rightarrow> X\<^isub>3"} with @{text "d\<^isub>i"} being any 
   other character than @{text c}, and @{term "X\<^isub>3 \<Turnstile>c\<^isub>j\<Rightarrow> X\<^isub>3"} for any 
   character @{text "c\<^isub>j"}.
@@ -706,7 +745,7 @@
   \end{center}
 
   \noindent
-  where the terms @{text "(Y\<^isub>i\<^isub>j, ATOM c\<^isub>i\<^isub>j)"} are pairs consiting of an equivalence class and
+  where the terms @{text "(Y\<^isub>i\<^isub>j, ATOM c\<^isub>i\<^isub>j)"} are pairs consisting of an equivalence class and
   a regular expression. In the initial equational system, they
   stand for all transitions @{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow>
   X\<^isub>i"}. 
@@ -796,9 +835,9 @@
   for representing the right-hand sides of equations, we can 
   prove \eqref{inv1} and \eqref{inv2} more concisely as
   %
-  \begin{lmm}\label{inv}
+  \begin{lemma}\label{inv}
   If @{thm (prem 1) test} then @{text "X = \<Union> \<calL> ` rhs"}.
-  \end{lmm}
+  \end{lemma}
 
   \noindent
   Our proof of Theorem~\ref{myhillnerodeone} will proceed by transforming the
@@ -876,13 +915,13 @@
   \noindent
   This allows us to prove a version of Arden's Lemma on the level of equations.
 
-  \begin{lmm}\label{ardenable}
+  \begin{lemma}\label{ardenable}
   Given an equation @{text "X = rhs"}.
   If @{text "X = \<Union>\<calL> ` rhs"},
   @{thm (prem 2) Arden_preserves_soundness}, and
   @{thm (prem 3) Arden_preserves_soundness}, then
   @{text "X = \<Union>\<calL> ` (Arden X rhs)"}.
-  \end{lmm}
+  \end{lemma}
   
   \noindent
   Our @{text ardenable} condition is slightly stronger than needed for applying Arden's Lemma,
@@ -1027,9 +1066,9 @@
   It is straightforward to prove that the initial equational system satisfies the
   invariant.
 
-  \begin{lmm}\label{invzero}
+  \begin{lemma}\label{invzero}
   @{thm[mode=IfThen] Init_ES_satisfies_invariant}
-  \end{lmm}
+  \end{lemma}
 
   \begin{proof}
   Finiteness is given by the assumption and the way how we set up the 
@@ -1042,12 +1081,12 @@
   \noindent
   Next we show that @{text Iter} preserves the invariant.
 
-  \begin{lmm}\label{iterone} If
+  \begin{lemma}\label{iterone} If
   @{thm (prem 1) iteration_step_invariant[where xrhs="rhs"]},
   @{thm (prem 2) iteration_step_invariant[where xrhs="rhs"]} and
   @{thm (prem 3) iteration_step_invariant[where xrhs="rhs"]}, then
   @{thm (concl) iteration_step_invariant[where xrhs="rhs"]}.
-  \end{lmm}
+  \end{lemma}
 
   \begin{proof} 
   The argument boils down to choosing an equation @{text "Y = yrhs"} to be eliminated
@@ -1079,12 +1118,12 @@
   \noindent
   We also need the fact that @{text Iter} decreases the termination measure.
 
-  \begin{lmm}\label{itertwo} If
+  \begin{lemma}\label{itertwo} If
   @{thm (prem 1) iteration_step_measure[simplified (no_asm), where xrhs="rhs"]},
   @{thm (prem 2) iteration_step_measure[simplified (no_asm), where xrhs="rhs"]} and
   @{thm (prem 3) iteration_step_measure[simplified (no_asm), where xrhs="rhs"]}, then\\
   \mbox{@{thm (concl) iteration_step_measure[simplified (no_asm), where xrhs="rhs"]}}.
-  \end{lmm}
+  \end{lemma}
 
   \begin{proof}
   By assumption we know that @{text "ES"} is finite and has more than one element.
@@ -1099,11 +1138,11 @@
   This brings us to our property we want to establish for @{text Solve}.
 
 
-  \begin{lmm}
+  \begin{lemma}
   If @{thm (prem 1) Solve} and @{thm (prem 2) Solve} then there exists
   a @{text rhs} such that  @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"}
   and @{term "invariant {(X, rhs)}"}.
-  \end{lmm}
+  \end{lemma}
 
   \begin{proof} 
   In order to prove this lemma using \eqref{whileprinciple}, we have to use a slightly
@@ -1119,7 +1158,7 @@
   Premise 3 of~\eqref{whileprinciple} is by Lemma~\ref{itertwo}. Now in premise 4
   we like to show that there exists a @{text rhs} such that @{term "ES = {(X, rhs)}"}
   and that @{text "invariant {(X, rhs)}"} holds, provided the condition @{text "Cond"}
-  does not holds. By the stronger invariant we know there exists such a @{text "rhs"}
+  does not hold. By the stronger invariant we know there exists such a @{text "rhs"}
   with @{term "(X, rhs) \<in> ES"}. Because @{text Cond} is not true, we know the cardinality
   of @{text ES} is @{text 1}. This means @{text "ES"} must actually be the set @{text "{(X, rhs)}"},
   for which the invariant holds. This allows us to conclude that 
@@ -1131,9 +1170,9 @@
   With this lemma in place we can show that for every equivalence class in @{term "UNIV // \<approx>A"}
   there exists a regular expression.
 
-  \begin{lmm}\label{every_eqcl_has_reg}
+  \begin{lemma}\label{every_eqcl_has_reg}
   @{thm[mode=IfThen] every_eqcl_has_reg}
-  \end{lmm}
+  \end{lemma}
 
   \begin{proof}
   By the preceding lemma, we know that there exists a @{text "rhs"} such
@@ -1181,9 +1220,9 @@
   In this section we will give a proof for establishing the second 
   part of the Myhill-Nerode Theorem. It can be formulated in our setting as follows:
 
-  \begin{thrm}\label{myhillnerodetwo}
+  \begin{theorem}\label{myhillnerodetwo}
   Given @{text "r"} is a regular expression, then @{thm Myhill_Nerode2}.
-  \end{thrm}  
+  \end{theorem}  
 
   \noindent
   The proof will be by induction on the structure of @{text r}. It turns out
@@ -1209,7 +1248,7 @@
   \noindent
   Much more interesting, however, are the inductive cases. They seem hard to be solved 
   directly. The reader is invited to try.\footnote{The induction hypothesis is not strong enough 
-  to make any progress with the TIME and STAR cases.} 
+  to make any progress with the @{text TIMES} and @{text STAR} cases.} 
 
   In order to see how our proof proceeds consider the following suggestive picture 
   given by \citeN{Constable00}:
@@ -1250,10 +1289,10 @@
   suffices to show in each induction step that another relation, say @{text
   R}, has finitely many equivalence classes and refines @{term "\<approx>(lang r)"}. 
 
-  \begin{dfntn}
+  \begin{definition}
   A relation @{text "R\<^isub>1"} \emph{refines} @{text "R\<^isub>2"}
   provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}. 
-  \end{dfntn}
+  \end{definition}
 
   \noindent
   For constructing @{text R}, we will rely on some \emph{tagging-functions}
@@ -1275,12 +1314,12 @@
   as follows.
 
 
-  \begin{dfntn}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x}
+  \begin{definition}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x}
   and @{text y} are \emph{tag-related} provided
   \begin{center}
   @{text "x \<^raw:$\threesim$>\<^bsub>tag\<^esub> y \<equiv> tag x = tag y"}\;.
   \end{center}
-  \end{dfntn}
+  \end{definition}
 
 
   In order to establish finiteness of a set @{text A}, we shall use the following powerful
@@ -1295,9 +1334,9 @@
   is finite, then the set @{text A} itself must be finite. We can use it to establish the following 
   two lemmas.
 
-  \begin{lmm}\label{finone}
+  \begin{lemma}\label{finone}
   @{thm[mode=IfThen] finite_eq_tag_rel}
-  \end{lmm}
+  \end{lemma}
 
   \begin{proof}
   We set in \eqref{finiteimageD}, @{text f} to be @{text "X \<mapsto> tag ` X"}. We have
@@ -1312,12 +1351,12 @@
   with @{thm (concl) finite_eq_tag_rel}.
   \end{proof}
 
-  \begin{lmm}\label{fintwo} 
+  \begin{lemma}\label{fintwo} 
   Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, whereby
   @{text "R\<^isub>1"} refines @{text "R\<^isub>2"}.
   If @{thm (prem 1) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}
   then @{thm (concl) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}.
-  \end{lmm}
+  \end{lemma}
 
   \begin{proof}
   We prove this lemma again using \eqref{finiteimageD}. This time we set @{text f} to
@@ -1368,11 +1407,11 @@
   The @{const TIMES}-case is slightly more complicated. We first prove the
   following lemma, which will aid the proof about refinement.
 
-  \begin{lmm}\label{refinement}
+  \begin{lemma}\label{refinement}
   The relation @{text "\<^raw:$\threesim$>\<^bsub>tag\<^esub>"} refines @{term "\<approx>A"}, provided for
   all strings @{text x}, @{text y} and @{text z} we have that \mbox{@{text "x \<^raw:$\threesim$>\<^bsub>tag\<^esub> y"}}
   and @{term "x @ z \<in> A"} imply @{text "y @ z \<in> A"}.
-  \end{lmm}
+  \end{lemma}
 
 
   \noindent
@@ -1390,7 +1429,9 @@
   refer to @{text "x\<^isub>p"} as the \emph{prefix} of the string @{text x},
   and respectively to @{text "x\<^isub>s"} as the \emph{suffix}.
 
+*}
 
+text {*
   Now assuming  @{term "x @ z \<in> A \<cdot> B"}, there are only two possible ways of how to `split' 
   this string to be in @{term "A \<cdot> B"}:
   %
@@ -1452,18 +1493,20 @@
   \end{tabular}
   \end{center}
   %
+
   \noindent
   Either @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B} 
   (first picture) or there is a prefix of @{text x} in @{text A} and the rest is in @{text B} 
   (second picture). In both cases we have to show that @{term "y @ z \<in> A \<cdot> B"}. The first case
-  we will only go through if we know that  @{term "x \<approx>A y"} holds @{text "(*)"}. Because then 
+  we will only go through if we know that  @{term "x \<approx>A y"} holds @{text "("}@{text "*"}@{text ")"}.  
+  Because then 
   we can infer from @{term "x @ z\<^isub>p \<in> A"} that @{term "y @ z\<^isub>p \<in> A"} holds for all @{text "z\<^isub>p"}.
   In the second case we only know that @{text "x\<^isub>p"} and @{text "x\<^isub>s"} is one possible partition
   of the string @{text x}. We have to know that both @{text "x\<^isub>p"} and the
   corresponding partition @{text "y\<^isub>p"} are in @{text "A"}, and that @{text "x\<^isub>s"} is `@{text B}-related' 
-  to @{text "y\<^isub>s"} @{text "(**)"}. From the latter fact we can infer that @{text "y\<^isub>s @ z \<in> B"}.
+  to @{text "y\<^isub>s"} @{text "("}@{text "**"}@{text ")"}. From the latter fact we can infer that @{text "y\<^isub>s @ z \<in> B"}.
   This will solve the second case.
-  Taking the two requirements, @{text "(*)"} and @{text "(**)"}, together we define the
+  Taking the two requirements, @{text "("}@{text "*"}@{text ")"} and @{text "(**)"}, together we define the
   tagging-function in the @{const Times}-case as:
 
   \begin{center}
@@ -1476,7 +1519,6 @@
   not know anything about how the string @{term x} is partitioned.
   With this definition in place, let us prove the @{const "Times"}-case.
 
-
   \begin{proof}[@{const TIMES}-Case]
   If @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
   then @{term "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))"} holds. The range of
@@ -1884,7 +1926,7 @@
   induction hypothesis is
 
   \begin{center}
-  @{text "(IH)"}\hspace{3mm}@{term "\<forall>r. Derivs s (lang r) = \<Union> lang ` (pderivs s r)"}
+  @{text "(IH)"}\hspace{3mm}@{term "\<forall>r. Derivs s (lang r) = \<Union> (lang ` (pderivs s r))"}
   \end{center}
 
   \noindent
@@ -1894,10 +1936,10 @@
   \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}ll}
   @{term "Derivs (c # s) (lang r)"} 
     & @{text "="} & @{term "Derivs s (Deriv c (lang r))"} & by def.\\
-    & @{text "="} & @{term "Derivs s (\<Union> lang ` (pderiv c r))"} & by @{text "("}\ref{Derspders}@{text ".i)"}\\
-    & @{text "="} & @{term "\<Union> (Derivs s) ` (lang ` (pderiv c r))"} & by def.~of @{text "Ders"}\\
-    & @{text "="} & @{term "\<Union> lang ` (\<Union> pderivs s ` (pderiv c r))"} & by IH\\
-    & @{text "="} & @{term "\<Union> lang ` (pderivs (c # s) r)"} & by def.\\
+    & @{text "="} & @{term "Derivs s (\<Union> (lang ` (pderiv c r)))"} & by @{text "("}\ref{Derspders}@{text ".i)"}\\
+    & @{text "="} & @{term "\<Union> ((Derivs s) ` (lang ` (pderiv c r)))"} & by def.~of @{text "Ders"}\\
+    & @{text "="} & @{term "\<Union> (lang ` (\<Union> (pderivs s ` (pderiv c r))))"} & by IH\\
+    & @{text "="} & @{term "\<Union> (lang ` (pderivs (c # s) r))"} & by def.\\
   \end{tabular}
   \end{center}
   
@@ -1931,10 +1973,10 @@
   @{thm pderivs_lang_def}
   \end{equation}
 
-  \begin{thrm}[\cite{Antimirov95}]\label{antimirov}
+  \begin{theorem}[\cite{Antimirov95}]\label{antimirov}
   For every language @{text A} and every regular expression @{text r}, 
   \mbox{@{thm finite_pderivs_lang}}.
-  \end{thrm}
+  \end{theorem}
 
   \noindent
   Antimirov's proof first establishes this theorem for the language @{term UNIV1}, 
@@ -2101,7 +2143,7 @@
   and \eqref{Derspders} we have
   %
   \begin{equation}\label{eqq}
-  @{term "Deriv_lang B (lang r) = (\<Union> lang ` (pderivs_lang B r))"}
+  @{term "Deriv_lang B (lang r) = (\<Union> (lang ` (pderivs_lang B r)))"}
   \end{equation}
 
   \noindent
@@ -2145,11 +2187,11 @@
   \noindent
   We like to establish
 
-  \begin{thrm}[\cite{Haines69}]\label{subseqreg}
+  \begin{theorem}[\cite{Haines69}]\label{subseqreg}
   For every language @{text A}, the languages @{text "(i)"} @{term "SUBSEQ A"} and 
   @{text "(ii)"} @{term "SUPSEQ A"}
   are regular.
-  \end{thrm}
+  \end{theorem}
 
   \noindent
   Our proof follows the one given by \citeN[Pages 92--95]{Shallit08}, except that we use
@@ -2182,9 +2224,9 @@
   whereby the last equation follows from the fact that @{term "A\<star>"} contains the
   empty string. With these properties at our disposal we can establish the lemma
 
-  \begin{lmm}
+  \begin{lemma}
   If @{text A} is regular, then also @{term "SUPSEQ A"}.
-  \end{lmm}
+  \end{lemma}
 
   \begin{proof}
   Since our alphabet is finite, we have a regular expression, written @{text ALL}, that
@@ -2212,12 +2254,12 @@
   \noindent
   Now we can prove the main lemma w.r.t.~@{const "SUPSEQ"}, namely
 
-  \begin{lmm}\label{mset}
+  \begin{lemma}\label{mset}
   For every language @{text A}, there exists a finite language @{text M} such that
   \begin{center}
   \mbox{@{term "SUPSEQ M = SUPSEQ A"}}\;.
   \end{center}
-  \end{lmm}
+  \end{lemma}
 
   \begin{proof}
   For @{text M} we take the set of all minimal elements of @{text A}. An element @{text x} 
@@ -2275,11 +2317,11 @@
   the non-regularity of languages. For this we use the following version of the Continuation
   Lemma (see for example~\cite{Rosenberg06}).
 
-  \begin{lmm}[Continuation Lemma]
+  \begin{lemma}[Continuation Lemma]
   If a language @{text A} is regular and a set of strings @{text B} is infinite,
   then there exist two distinct strings @{text x} and @{text y} in @{text B} 
   such that @{term "x \<approx>A y"}.
-  \end{lmm}
+  \end{lemma}
 
   \noindent
   This lemma can be easily deduced from the Myhill-Nerode Theorem and the Pigeonhole
@@ -2293,9 +2335,9 @@
   for the strings consisting of @{text n} times the character a; similarly for
   @{text "b\<^isup>n"}). For this consider the infinite set @{text "B \<equiv> \<Union>\<^isub>n a\<^sup>n"}.
 
-  \begin{lmm}
+  \begin{lemma}
   No two distinct strings in set @{text "B"} are Myhill-Nerode related by language @{text A}.
-  \end{lmm} 
+  \end{lemma} 
 
   \begin{proof}
   After unfolding the definition of @{text "B"}, we need to establish that given @{term "i \<noteq> j"},
@@ -2344,9 +2386,9 @@
   We have established in Isabelle/HOL both directions 
   of the Myhill-Nerode Theorem.
   %
-  \begin{thrm}[Myhill-Nerode Theorem]\mbox{}\\
+  \begin{theorem}[Myhill-Nerode Theorem]\mbox{}\\
   A language @{text A} is regular if and only if @{thm (rhs) Myhill_Nerode}.
-  \end{thrm}
+  \end{theorem}
   
   \noindent
   Having formalised this theorem means we pushed our point of view quite
@@ -2452,8 +2494,8 @@
   algorithm is still executable. Given the infrastructure for
   executable sets  introduced by \citeN{Haftmann09} in Isabelle/HOL, it should.
 
-  We started out by claiming that in a theorem prover it is eaiser to
-  reason about regular expressions than about automta. Here are some
+  We started out by claiming that in a theorem prover it is easier to
+  reason about regular expressions than about automata. Here are some
   numbers: Our formalisation of the Myhill-Nerode Theorem consists of
   780 lines of Isabelle/Isar code for the first direction and 460 for
   the second (the one based on tagging-functions), plus around 300
@@ -2536,50 +2578,50 @@
   We are grateful for the comments we received from Larry Paulson.  Tobias
   Nipkow made us aware of the properties in Theorem~\ref{subseqreg} and Tjark
   Weber helped us with proving them. Christian Sternagel provided us with a
-  version of Higman's Lemma that applies to arbtrary, but finite alphabets. 
+  version of Higman's Lemma that applies to arbitrary, but finite alphabets. 
 
   \bibliographystyle{acmtrans}
   \bibliography{root}
 
-  \newpage
-  \begin{appendix}
-  \section{Appendix$^\star$}
+  %\newpage
+  %\begin{appendix}
+  %\section{Appendix$^\star$}
 
-  \renewcommand{\thefootnote}{\mbox{$\star$}}
-  \footnotetext{If the reviewers deem more suitable, the authors are
-  prepared to drop material or move it to an electronic appendix.}
+  %\renewcommand{\thefootnote}{\mbox{$\star$}}
+  %\footnotetext{If the reviewers deem more suitable, the authors are
+  %prepared to drop material or move it to an electronic appendix.}
   
-  \begin{proof}[of Lemma~\ref{arden}]
-  For the right-to-left direction we assume @{thm (rhs) reversed_Arden} and show
-  that @{thm (lhs) reversed_Arden} holds. From Property~\ref{langprops}@{text "(i)"} 
-  we have @{term "A\<star> = A \<cdot> A\<star> \<union> {[]}"},
-  which is equal to @{term "A\<star> = A\<star> \<cdot> A \<union> {[]}"}. Adding @{text B} to both 
-  sides gives @{term "B \<cdot> A\<star> = B \<cdot> (A\<star> \<cdot> A \<union> {[]})"}, whose right-hand side
-  is equal to @{term "(B \<cdot> A\<star>) \<cdot> A \<union> B"}. Applying the assumed equation 
-  completes this direction. 
+  %\begin{proof}[of Lemma~\ref{arden}]
+  %For the right-to-left direction we assume @{thm (rhs) reversed_Arden} and show
+  %that @{thm (lhs) reversed_Arden} holds. From Property~\ref{langprops}@{text "(i)"} 
+  %we have @{term "A\<star> = A \<cdot> A\<star> \<union> {[]}"},
+  %which is equal to @{term "A\<star> = A\<star> \<cdot> A \<union> {[]}"}. Adding @{text B} to both 
+  %sides gives @{term "B \<cdot> A\<star> = B \<cdot> (A\<star> \<cdot> A \<union> {[]})"}, whose right-hand side
+  %is equal to @{term "(B \<cdot> A\<star>) \<cdot> A \<union> B"}. Applying the assumed equation 
+  %completes this direction. 
 
-  For the other direction we assume @{thm (lhs) reversed_Arden}. By a simple induction
-  on @{text n}, we can establish the property
+  %For the other direction we assume @{thm (lhs) reversed_Arden}. By a simple induction
+  %on @{text n}, we can establish the property
 
-  \begin{center}
-  @{text "(*)"}\hspace{5mm} @{thm (concl) reversed_arden_helper}
-  \end{center}
+  %\begin{center}
+  %@{text "("}@{text "*"}@{text ")"}\hspace{5mm} @{thm (concl) reversed_arden_helper}
+  %\end{center}
   
-  \noindent
-  Using this property we can show that @{term "B \<cdot> (A \<up> n) \<subseteq> X"} holds for
-  all @{text n}. From this we can infer @{term "B \<cdot> A\<star> \<subseteq> X"} using the definition
-  of @{text "\<star>"}.
-  For the inclusion in the other direction we assume a string @{text s}
-  with length @{text k} is an element in @{text X}. Since @{thm (prem 1) reversed_Arden}
-  we know by Property~\ref{langprops}@{text "(ii)"} that 
-  @{term "s \<notin> X \<cdot> (A \<up> Suc k)"} since its length is only @{text k}
-  (the strings in @{term "X \<cdot> (A \<up> Suc k)"} are all longer). 
-  From @{text "(*)"} it follows then that
-  @{term s} must be an element in @{term "(\<Union>m\<le>k. B \<cdot> (A \<up> m))"}. This in turn
-  implies that @{term s} is in @{term "(\<Union>n. B \<cdot> (A \<up> n))"}. Using Property~\ref{langprops}@{text "(iii)"} 
-  this is equal to @{term "B \<cdot> A\<star>"}, as we needed to show.
-  \end{proof}
-  \end{appendix}
+  %\noindent
+  %Using this property we can show that @{term "B \<cdot> (A \<up> n) \<subseteq> X"} holds for
+  %all @{text n}. From this we can infer @{term "B \<cdot> A\<star> \<subseteq> X"} using the definition
+  %of @{text "\<star>"}.
+  %For the inclusion in the other direction we assume a string @{text s}
+  %with length @{text k} is an element in @{text X}. Since @{thm (prem 1) reversed_Arden}
+  %we know by Property~\ref{langprops}@{text "(ii)"} that 
+  %@{term "s \<notin> X \<cdot> (A \<up> Suc k)"} since its length is only @{text k}
+  %(the strings in @{term "X \<cdot> (A \<up> Suc k)"} are all longer). 
+  %From @{text "("}@{text "*"}@{text ")"} it follows then that
+  %@{term s} must be an element in @{term "(\<Union>m\<le>k. B \<cdot> (A \<up> m))"}. This in turn
+  %implies that @{term s} is in @{term "(\<Union>n. B \<cdot> (A \<up> n))"}. Using Property~\ref{langprops}@{text "(iii)"} 
+  %this is equal to @{term "B \<cdot> A\<star>"}, as we needed to show.
+  %\end{proof}
+  % \end{appendix}
 *}
 
 




