regexp: comparison Journal/Paper.thy

equal deleted inserted replaced

-:2a5ac68db24b
+:5347d7556487
 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
 @{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
-caracter @{text "c\<^isub>j"}.
+character @{text "c\<^isub>j"}.
 Next we construct an \emph{initial equational system} that
 contains an equation for each equivalence class. We first give
 an informal description of this construction. Suppose we have
 the equivalence classes @{text "X\<^isub>1,\<dots>,X\<^isub>n"}, there must be one and only one that
 @{text "X = \<Union>\<calL> ` (Arden X rhs)"}.
 \end{lmm}
 \noindent
 Our @{text ardenable} condition is slightly stronger than needed for applying Arden's Lemma,
-but we can still ensure that it holds troughout our algorithm of transforming equations
+but we can still ensure that it holds throughout our algorithm of transforming equations
 into solved form. The \emph{substitution-operation} takes an equation
 of the form @{text "X = xrhs"} and substitutes it into the right-hand side @{text rhs}.
 \begin{center}
 \begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
 A\<star>"}, which means @{term "y @ z \<in> A\<star>"}. The last step is to set
 @{text "A"} to @{term "lang r"} and thus complete the proof.
 \end{proof}
 *}
-section {* Second Part proved using Partial Derivatives *}
+section {* Second Part proved using Partial Derivatives\label{derivatives} *}
 text {*
 \noindent
 As we have seen in the previous section, in order to establish
 the second direction of the Myhill-Nerode theorem, we need to find
 \noindent
 Carrying this idea through, we must not consider the set of all derivatives,
 but the ones modulo @{text "ACI"}.  In principle, this can be done formally,
 but it is very painful in a theorem prover (since there is no
-direct characterisation of the set of dissimlar derivatives).
+direct characterisation of the set of dissimilar derivatives).
 Fortunately, there is a much simpler approach using \emph{partial
 derivatives}. They were introduced by Antimirov \cite{Antimirov95} and can be defined
 in Isabelle/HOL as follows:
 \end{equation}
 \begin{proof}
 The first fact is by a simple induction on @{text r}. For the second we slightly
 modify Antimirov's proof by performing an induction on @{text s} where we
-genaralise over all @{text r}. That means in the @{text "cons"}-case the
+generalise over all @{text r}. That means in the @{text "cons"}-case the
 induction hypothesis is
 \begin{center}
 @{text "(IH)"}\hspace{3mm}@{term "\<forall>r. Ders s (lang r) = \<Union> lang ` (pders s r)"}
 \end{center}
 Owens and Slind \cite{OwensSlind08}.
 Our formalisation consists of 780 lines of Isabelle/Isar code for the first
 direction and 460 for the second, plus around 300 lines of standard material
-about regular languages. While this might be seen large, it should be seen
+about regular languages. The formalisation about derivatives and partial
+derivatives shown in Section~\ref{derivatives} consists of 390 lines of code.
+While this might be seen large, it should be seen
 in the context of the work done by Constable at al \cite{Constable00} who
 formalised the Myhill-Nerode theorem in Nuprl using automata. They write
 that their four-member team needed something on the magnitude of 18 months
 for their formalisation. The estimate for our formalisation is that we
 needed approximately 3 months and this included the time to find our proof
 formalisation was not the bottleneck. It is hard to gauge the size of a
 formalisation in Nurpl, but from what is shown in the Nuprl Math Library
 about their development it seems substantially larger than ours. The code of
 ours can be found in the Mercurial Repository at
 \mbox{\url{http://www4.in.tum.de/~urbanc/regexp.html}}.
 Our proof of the first direction is very much inspired by \emph{Brzozowski's
 algebraic method} used to convert a finite automaton to a regular
 expression \cite{Brzozowski64}. The close connection can be seen by considering the equivalence

changeset 194	5347d7556487
parent 193	2a5ac68db24b
child 196	fa8d33d13cb6