regexp: comparison Journal/Paper.thy

equal deleted inserted replaced

-:6969de1eb96b
+:50cc1a39c990
 lexing. Berghofer and Reiter \cite{BerghoferReiter09} formalise automata
 working over bit strings in the context of Presburger arithmetic.  The only
 larger formalisations of automata theory are carried out in Nuprl
 \cite{Constable00} and in Coq \cite{Filliatre97}.
-Also one might consider automata theory as well-worn stock material where
+Also one might consider automata theory as a well-worn stock subject where
 everything is crystal clear. However, paper proofs about automata often
 involve subtle side-conditions which are easily overlooked, but which make
 formal reasoning rather painful. For example Kozen's proof of the
 Myhill-Nerode theorem requires that the automata do not have inaccessible
 states \cite{Kozen97}. Another subtle side-condition is completeness of
-automata: automata need to have total transition functions and at most one
+automata, that is automata need to have total transition functions and at most one
 `sink' state from which there is no connection to a final state (Brozowski
-mentions this side-condition in connection with state complexity
+mentions this side-condition in the context of state complexity
-\cite{Brozowski10}). Such side-conditions mean that if we define a regular
+of automata \cite{Brozowski10}). Such side-conditions mean that if we define a regular
 language as one for which there exists \emph{a} finite automaton that
-recognises all its strings (Def.~\ref{baddef}), then we need a lemma which
+recognises all its strings (see Def.~\ref{baddef}), then we need a lemma which
 ensures that another equivalent can be found satisfying the
 side-condition. Unfortunately, such `little' and `obvious' lemmas make
-formalisations of automata theory hair-pulling experiences.
+a formalisation of automata theory a hair-pulling experience.
 In this paper, we will not attempt to formalise automata theory in
 Isabelle/HOL nor will we attempt to formalise automata proofs from the
 literature, but take a different approach to regular languages than is
 section {* Preliminaries *}
 text {*
 \noindent
 Strings in Isabelle/HOL are lists of characters with the \emph{empty string}
-being represented by the empty list, written @{term "[]"}.  \emph{Languages}
+being represented by the empty list, written @{term "[]"}.  We assume there
-are sets of strings. The language containing all strings is written in
+are only finitely many different characters.  \emph{Languages} are sets of
-Isabelle/HOL as @{term "UNIV::string set"}. The concatenation of two languages
+strings. The language containing all strings is written in Isabelle/HOL as
-is written @{term "A \<cdot> B"} and a language raised to the power @{text n} is written
+@{term "UNIV::string set"}. The concatenation of two languages is written
+@{term "A \<cdot> B"} and a language raised to the power @{text n} is written
 @{term "A \<up> n"}. They are defined as usual
 \begin{center}
+\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
-@{thm conc_def'[THEN eq_reflection, where A1="A" and B1="B"]}
+@{thm (lhs) conc_def'[THEN eq_reflection, where A1="A" and B1="B"]}
-\hspace{7mm}
+& @{text "\<equiv>"} & @{thm (rhs) conc_def'[THEN eq_reflection, where A1="A" and B1="B"]}\\
-@{thm lang_pow.simps(1)[THEN eq_reflection, where A1="A"]}
-\hspace{7mm}
+@{thm (lhs) lang_pow.simps(1)[THEN eq_reflection, where A1="A"]}
-@{thm lang_pow.simps(2)[THEN eq_reflection, where A1="A" and n1="n"]}
+& @{text "\<equiv>"} & @{thm (rhs) lang_pow.simps(1)[THEN eq_reflection, where A1="A"]}\\
+@{thm (lhs) lang_pow.simps(2)[THEN eq_reflection, where A1="A" and n1="n"]}
+& @{text "\<equiv>"} & @{thm (rhs) lang_pow.simps(2)[THEN eq_reflection, where A1="A" and n1="n"]}
+\end{tabular}
 \end{center}
 \noindent
 where @{text "@"} is the list-append operation. The Kleene-star of a language @{text A}
 is defined as the union over all powers, namely @{thm star_def}. In the paper
 Regular expressions are defined as the inductive datatype
 \begin{center}
 \begin{tabular}{rcl}
 @{text r} & @{text "::="} & @{term ZERO}\\
-& @{text"|"} & @{term ONE}\\
+& @{text"|"} & @{term One}\\
-& @{text"|"} & @{term "ATOM c"}\\
+& @{text"|"} & @{term "Atom c"}\\
-& @{text"|"} & @{term "TIMES r r"}\\
+& @{text"|"} & @{term "Times r r"}\\
-& @{text"|"} & @{term "PLUS r r"}\\
+& @{text"|"} & @{term "Plus r r"}\\
-& @{text"|"} & @{term "STAR r"}
+& @{text"|"} & @{term "Star r"}
 \end{tabular}
 \end{center}
 \noindent
 and the language matched by a regular expression is defined as
 section {* The Myhill-Nerode Theorem, First Part *}
 text {*
+\noindent
 \footnote{Folklore: Henzinger (arden-DFA-regexp.pdf); Hofmann}
-\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
 language. This can be defined as a tertiary relation.
 \noindent
 In our running example, @{text "X\<^isub>2"} is the only
 equivalence class in @{term "finals {[c]}"}.
 It is straightforward to show that in general
-\begin{center}
+\begin{equation}\label{finalprops}
 @{thm lang_is_union_of_finals}\hspace{15mm}
 @{thm finals_in_partitions}
-\end{center}
+\end{equation}
 \noindent
 hold.
 Therefore if we know that there exists a regular expression for every
 equivalence class in \mbox{@{term "finals A"}} (which by assumption must be
 `terminal' states. We are forced to set up the equational system in our
 way, because the Myhill-Nerode relation determines the `direction' of the
 transitions---the successor `state' of an equivalence class @{text Y} can
 be reached by adding a character to the end of @{text Y}. This is also the
 reason why we have to use our reverse version of Arden's Lemma.}
-%In our initial equation system there can only be
+In our running example we have the initial equational system
-%finitely many terms of the form @{text "(Y\<^isub>i\<^isub>j, ATOM c\<^isub>i\<^isub>j)"} in a right-hand side
-%since by assumption there are only finitely many
+\begin{equation}\label{exmpcs}
-%equivalence classes and only finitely many characters.
+\mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+@{term "X\<^isub>1"} & @{text "="} & @{text "\<lambda>(ONE)"}\\
+@{term "X\<^isub>2"} & @{text "="} & @{text "(X\<^isub>1, ATOM c)"}\\
+@{term "X\<^isub>3"} & @{text "="} & @{text "(X\<^isub>1, ATOM d\<^isub>1) + \<dots> + (X\<^isub>1, ATOM d\<^isub>n)"}\\
+& & \mbox{}\hspace{3mm}@{text "+ (X\<^isub>3, ATOM c\<^isub>1) + \<dots> + (X\<^isub>3, ATOM c\<^isub>m)"}
+\end{tabular}}
+\end{equation}
+\noindent
+where @{text "d\<^isub>1\<dots>d\<^isub>n"} is the sequence of all characters
+except @{text c}, and @{text "c\<^isub>1\<dots>c\<^isub>m"} is the sequence of all
+characters.  In our initial equation systems there can only be finitely many
+terms of the form @{text "(Y\<^isub>i\<^isub>j, ATOM c\<^isub>i\<^isub>j)"},
+since by assumption there are only finitely many equivalence classes and
+only finitely many characters.
 Overloading the function @{text \<calL>} for the two kinds of terms in the
 equational system, we have
 \begin{center}
 @{text "\<calL>(Y, r) \<equiv>"} %
 and substitutes @{text X} throughout the rest of the equational system
 adjusting the remaining regular expressions appropriately. To define this adjustment
 we define the \emph{append-operation} taking a term and a regular expression as argument
 \begin{center}
-@{thm Append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\hspace{10mm}
+\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-@{thm Append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
+@{thm (lhs) Append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
+& @{text "\<equiv>"} &
+@{thm (rhs) Append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\\
+@{thm (lhs) Append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
+& @{text "\<equiv>"} &
+@{thm (rhs) Append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
+\end{tabular}
 \end{center}
 \noindent
 We lift this operation to entire right-hand sides of equations, written as
 @{thm (lhs) Append_rexp_rhs_def[where rexp="r"]}. With this we can define
 %
 \begin{equation}\label{arden_def}
 \mbox{\begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
 @{thm (lhs) Arden_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\
 & & @{text "rhs' ="} & @{term "rhs - {Trn X r | r. Trn X r \<in> rhs}"} \\
-& & @{text "r' ="}   & @{term "STAR (\<Uplus> {r. Trn X r \<in> rhs})"}\\
+& & @{text "r' ="}   & @{term "Star (\<Uplus> {r. Trn X r \<in> rhs})"}\\
-& &  \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "append_rhs_rexp rhs' r'"}}\\
+& &  \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "Append_rexp_rhs rhs' r'"}}\\
 \end{tabular}}
 \end{equation}
 \noindent
 In this definition, we first delete all terms of the form @{text "(X, r)"} from @{text rhs};
 then we calculate the combined regular expressions for all @{text r} coming
-from the deleted @{text "(X, r)"}, and take the @{const STAR} of it;
+from the deleted @{text "(X, r)"}, and take the @{const Star} of it;
 finally we append this regular expression to @{text rhs'}. It can be easily seen
 that this operation mimics Arden's Lemma on the level of equations. To ensure
 the non-emptiness condition of Arden's Lemma we say that a right-hand side is
 @{text ardenable} provided
 \begin{center}
 \begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
 @{thm (lhs) Subst_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\
 & & @{text "rhs' ="} & @{term "rhs - {Trn X r | r. Trn X r \<in> rhs}"} \\
 & & @{text "r' ="}   & @{term "\<Uplus> {r. Trn X r \<in> rhs}"}\\
-& &  \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "rhs' \<union> append_rhs_rexp xrhs r'"}}\\
+& &  \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "rhs' \<union> Append_rexp_rhs xrhs r'"}}\\
 \end{tabular}
 \end{center}
 \noindent
 We again delete first all occurrences of @{text "(X, r)"} in @{text rhs}; we then calculate
 and to show that @{term "Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)"}
 preserves the invariant.
 We prove this as follows:
 \begin{center}
-@{text "\<forall> ES."} @{thm (prem 1) Subst_all_satisfies_invariant} implies
+\begin{tabular}{@ {}l@ {}}
+@{text "\<forall> ES."}\\ \mbox{}\hspace{5mm}@{thm (prem 1) Subst_all_satisfies_invariant} implies
 @{thm (concl) Subst_all_satisfies_invariant}
+\end{tabular}
 \end{center}
 \noindent
 Finiteness is straightforward, as the @{const Subst} and @{const Arden} operations
 keep the equational system finite. These operations also preserve soundness
 with @{term "y @ z \<in> A \<cdot> B"}. We again can complete the @{const TIMES}-case
 by setting @{text A} to @{term "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}.
 \end{proof}
 \noindent
-The case for @{const STAR} is similar to @{const TIMES}, but poses a few extra challenges. When
+The case for @{const Star} is similar to @{const TIMES}, but poses a few extra challenges. When
 we analyse the case that @{text "x @ z"} is an element in @{term "A\<star>"} and @{text x} is not the
 empty string, we
 have the following picture:
 %
 \begin{center}
 %
 \begin{center}
 @{thm tag_str_Star_def[where ?L1.0="A", THEN meta_eq_app]}\smallskip
 \end{center}
-\begin{proof}[@{const STAR}-Case]
+\begin{proof}[@{const Star}-Case]
 If @{term "finite (UNIV // \<approx>A)"}
 then @{term "finite (Pow (UNIV // \<approx>A))"} holds. The range of
-@{term "tag_str_STAR A"} is a subset of this set, and therefore finite.
+@{term "tag_str_Star A"} is a subset of this set, and therefore finite.
 Again we have to show injectivity of this tagging-function as
 %
 \begin{center}
-@{term "\<forall>z. tag_str_STAR A x = tag_str_STAR A y \<and> x @ z \<in> A\<star> \<longrightarrow> y @ z \<in> A\<star>"}
+@{term "\<forall>z. tag_str_Star A x = tag_str_Star A y \<and> x @ z \<in> A\<star> \<longrightarrow> y @ z \<in> A\<star>"}
 \end{center}
 %
 \noindent
 We first need to consider the case that @{text x} is the empty string.
 From the assumption we can infer @{text y} is the empty string and
 \begin{equation}\label{mhders}
 @{term "x \<approx>A y"} \hspace{4mm}\text{if and only if}\hspace{4mm} @{term "Ders x A = Ders y A"}
 \end{equation}
 \noindent
-It is realtively easy to establish the following identidies for left-quotients:
+It is realtively easy to establish the following properties for left-quotients:
 \begin{center}
 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{2mm}}l}
 @{thm (lhs) Der_zero}  & $=$ & @{thm (rhs) Der_zero}\\
 @{thm (lhs) Der_one}   & $=$ & @{thm (rhs) Der_one}\\
 @{thm (lhs) der.simps(2)}  & @{text "\<equiv>"} & @{thm (rhs) der.simps(2)}\\
 @{thm (lhs) der.simps(3)[where c'="d"]}  & @{text "\<equiv>"} & @{thm (rhs) der.simps(3)[where c'="d"]}\\
 @{thm (lhs) der.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
 & @{text "\<equiv>"} & @{thm (rhs) der.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
 @{thm (lhs) der.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
-& @{text "\<equiv>"}\\
+& @{text "\<equiv>"} & @{text "if"}~@{term "nullable r\<^isub>1"}~@{text "then"}~%
-\multicolumn{3}{@ {\hspace{5mm}}l@ {}}{@{thm (rhs) der.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}}\\
+@{term "Plus (Times (der c r\<^isub>1) r\<^isub>2) (der c r\<^isub>2)"}\\
+&             & \phantom{@{text "if"}~@{term "nullable r\<^isub>1"}~}@{text "else"}~%
+@{term "Times (der c r\<^isub>1) r\<^isub>2"}\\
 @{thm (lhs) der.simps(6)}  & @{text "\<equiv>"} & @{thm (rhs) der.simps(6)}\smallskip\\
 @{thm (lhs) ders.simps(1)}  & @{text "\<equiv>"} & @{thm (rhs) ders.simps(1)}\\
 @{thm (lhs) ders.simps(2)}  & @{text "\<equiv>"} & @{thm (rhs) ders.simps(2)}\\
 \end{tabular}
 \end{center}
 \noindent
 The function @{term "nullable r"} tests whether the regular expression
 can recognise the empty string:
 \begin{center}
-\begin{tabular}{cc}
+\begin{tabular}{c@ {\hspace{10mm}}c}
 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
 @{thm (lhs) nullable.simps(1)}  & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(1)}\\
 @{thm (lhs) nullable.simps(2)}  & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(2)}\\
 @{thm (lhs) nullable.simps(3)}  & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(3)}\\
 \end{tabular} &
 @{thm (lhs) pder.simps(2)}  & @{text "\<equiv>"} & @{thm (rhs) pder.simps(2)}\\
 @{thm (lhs) pder.simps(3)[where c'="d"]}  & @{text "\<equiv>"} & @{thm (rhs) pder.simps(3)[where c'="d"]}\\
 @{thm (lhs) pder.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
 & @{text "\<equiv>"} & @{thm (rhs) pder.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
 @{thm (lhs) pder.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
-& @{text "\<equiv>"}\\
+& @{text "\<equiv>"} & @{text "if"}~@{term "nullable r\<^isub>1"}~@{text "then"}~%
-\multicolumn{3}{@ {\hspace{20mm}}l@ {}}{@{thm (rhs) pder.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}}\\
+@{term "(Times_set (pder c r\<^isub>1) r\<^isub>2) \<union> (pder c r\<^isub>2)"}\\
+& & \phantom{@{text "if"}~@{term "nullable r\<^isub>1"}~}@{text "else"}~%
+@{term "Times_set (pder c r\<^isub>1) r\<^isub>2"}\\
 @{thm (lhs) pder.simps(6)}  & @{text "\<equiv>"} & @{thm (rhs) pder.simps(6)}\smallskip\\
 @{thm (lhs) pders.simps(1)}  & @{text "\<equiv>"} & @{thm (rhs) pders.simps(1)}\\
 @{thm (lhs) pders.simps(2)}  & @{text "\<equiv>"} & @{thm (rhs) pders.simps(2)}\\
 \end{tabular}
 \end{center}

changeset 177	50cc1a39c990
parent 176	6969de1eb96b
child 178	c6ebfe052109