(*<*)theory Paperimports "../Myhill_2" "~~/src/HOL/Library/LaTeXsugar" begindeclare [[show_question_marks = false]]consts REL :: "(string \<times> string) \<Rightarrow> bool" UPLUS :: "'a set \<Rightarrow> 'a set \<Rightarrow> (nat \<times> 'a) set"abbreviation "EClass x R \<equiv> R `` {x}"abbreviation "append_rexp2 r_itm r \<equiv> append_rexp r r_itm"notation (latex output) str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and str_eq ("_ \<approx>\<^bsub>_\<^esub> _") and Seq (infixr "\<cdot>" 100) and Star ("_\<^bsup>\<star>\<^esup>") and pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and Suc ("_+1" [100] 100) and quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and REL ("\<approx>") and UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90) and L ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and Lam ("\<lambda>'(_')" [100] 100) and Trn ("'(_, _')" [100, 100] 100) and EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and append_rhs_rexp ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _" [100, 100] 100) and tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [100, 100, 100] 100) and tag_str_SEQ ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and tag_str_SEQ ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and tag_str_STAR ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _" [100] 100) and tag_str_STAR ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100)lemma meta_eq_app: shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x" by auto(*>*)section {* Introduction *}text {* Regular languages are an important and well-understood subject in Computer Science, with many beautiful theorems and many useful algorithms. There is a wide range of textbooks on this subject, many of which are aimed at students and contain very detailed `pencil-and-paper' proofs (e.g.~\cite{Kozen97}). It seems natural to exercise theorem provers by formalising the theorems and by verifying formally the algorithms. There is however a problem: the typical approach to regular languages is to introduce finite automata and then define everything in terms of them. For example, a regular language is normally defined as one whose strings are recognised by a finite deterministic automaton. This approach has many benefits. Among them is the fact that it is easy to convince oneself that regular languages are closed under complementation: one just has to exchange the accepting and non-accepting states in the corresponding automaton to obtain an automaton for the complement language. The problem, however, lies with formalising such reasoning in a HOL-based theorem prover, in our case Isabelle/HOL. Automata are built up from states and transitions that need to be represented as graphs, matrices or functions, none of which can be defined as an inductive datatype. In case of graphs and matrices, this means we have to build our own reasoning infrastructure for them, as neither Isabelle/HOL nor HOL4 nor HOLlight support them with libraries. Even worse, reasoning about graphs and matrices can be a real hassle in HOL-based theorem provers. Consider for example the operation of sequencing two automata, say $A_1$ and $A_2$, by connecting the accepting states of $A_1$ to the initial state of $A_2$: \begin{center} \begin{tabular}{ccc} \begin{tikzpicture}[scale=0.8] %\draw[step=2mm] (-1,-1) grid (1,1); \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3); \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3); \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; \draw (-0.6,0.0) node {\footnotesize$A_1$}; \draw ( 0.6,0.0) node {\footnotesize$A_2$}; \end{tikzpicture} & \raisebox{1.1mm}{\bf\Large$\;\;\;\Rightarrow\,\;\;$} & \begin{tikzpicture}[scale=0.8] %\draw[step=2mm] (-1,-1) grid (1,1); \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3); \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3); \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; \draw (C) to [very thick, bend left=45] (B); \draw (D) to [very thick, bend right=45] (B); \draw (-0.6,0.0) node {\footnotesize$A_1$}; \draw ( 0.6,0.0) node {\footnotesize$A_2$}; \end{tikzpicture} \end{tabular} \end{center} \noindent On `paper' we can define the corresponding graph in terms of the disjoint union of the state nodes. Unfortunately in HOL, the standard definition for disjoint union, namely % \begin{equation}\label{disjointunion} @{term "UPLUS A\<^isub>1 A\<^isub>2 \<equiv> {(1, x) | x. x \<in> A\<^isub>1} \<union> {(2, y) | y. y \<in> A\<^isub>2}"} \end{equation} \noindent changes the type---the disjoint union is not a set, but a set of pairs. Using this definition for disjoint union means we do not have a single type for automata and hence will not be able to state certain properties about \emph{all} automata, since there is no type quantification available in HOL (unlike in Coq, for example). An alternative, which provides us with a single type for automata, is to give every state node an identity, for example a natural number, and then be careful to rename these identities apart whenever connecting two automata. This results in clunky proofs establishing that properties are invariant under renaming. Similarly, connecting two automata represented as matrices results in very adhoc constructions, which are not pleasant to reason about. Functions are much better supported in Isabelle/HOL, but they still lead to similar problems as with graphs. Composing, for example, two non-deterministic automata in parallel requires also the formalisation of disjoint unions. Nipkow \cite{Nipkow98} dismisses for this the option of using identities, because it leads according to him to ``messy proofs''. He opts for a variant of \eqref{disjointunion} using bit lists, but writes \begin{quote} \it% \begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}} `` & All lemmas appear obvious given a picture of the composition of automata\ldots Yet their proofs require a painful amount of detail.'' \end{tabular} \end{quote} \noindent and \begin{quote} \it% \begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}} `` & If the reader finds the above treatment in terms of bit lists revoltingly concrete, I cannot disagree. A more abstract approach is clearly desirable.'' \end{tabular} \end{quote} \noindent Moreover, it is not so clear how to conveniently impose a finiteness condition upon functions in order to represent \emph{finite} automata. The best is probably to resort to more advanced reasoning frameworks, such as \emph{locales} or \emph{type classes}, which are \emph{not} available in all HOL-based theorem provers. Because of these problems to do with representing automata, there seems to be no substantial formalisation of automata theory and regular languages carried out in HOL-based theorem provers. Nipkow \cite{Nipkow98} establishes the link between regular expressions and automata in the context of 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}. In this paper, we will not attempt to formalise automata theory in Isabelle/HOL, but take a completely different approach to regular languages. Instead of defining a regular language as one where there exists an automaton that recognises all strings of the language, we define a regular language as: \begin{definition} A language @{text A} is \emph{regular}, provided there is a regular expression that matches all strings of @{text "A"}. \end{definition} \noindent The reason is that regular expressions, unlike graphs, matrices and functions, can be easily defined as inductive datatype. Consequently a corresponding reasoning infrastructure comes for free. This has recently been exploited in HOL4 with a formalisation of regular expression matching based on derivatives \cite{OwensSlind08} and with an equivalence checker for regular expressions in Isabelle/HOL \cite{KraussNipkow11}. The 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 for when a language is regular. As a corollary of this theorem we can easily establish the usual closure properties, including complementation, for regular languages.\smallskip \noindent {\bf Contributions:} There is an extensive literature on regular languages. To our knowledge, our proof of the Myhill-Nerode theorem is the first that is based on regular expressions, only. We prove the part of this theorem stating that a regular expression has only finitely many partitions using certain tagging-functions. Again to our best knowledge, these tagging-functions have not been used before to establish the Myhill-Nerode theorem.*}section {* Preliminaries *}text {* Strings in Isabelle/HOL are lists of characters with the \emph{empty string} being represented by the empty list, written @{term "[]"}. \emph{Languages} are sets of strings. The language containing all strings is written in Isabelle/HOL as @{term "UNIV::string set"}. The concatenation of two languages is written @{term "A ;; B"} and a language raised to the power @{text n} is written @{term "A \<up> n"}. They are defined as usual \begin{center} @{thm Seq_def[THEN eq_reflection, where A1="A" and B1="B"]} \hspace{7mm} @{thm pow.simps(1)[THEN eq_reflection, where A1="A"]} \hspace{7mm} @{thm pow.simps(2)[THEN eq_reflection, where A1="A" and n1="n"]} \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 we will make use of the following properties of these constructions. \begin{proposition}\label{langprops}\mbox{}\\ \begin{tabular}{@ {}ll} (i) & @{thm star_cases} \\ (ii) & @{thm[mode=IfThen] pow_length}\\ (iii) & @{thm seq_Union_left} \\ \end{tabular} \end{proposition} \noindent In @{text "(ii)"} we use the notation @{term "length s"} for the length of a string; this property states that if \mbox{@{term "[] \<notin> A"}} then the lengths of the strings in @{term "A \<up> (Suc n)"} must be longer than @{text n}. We omit the proofs for these properties, but invite the reader to consult our formalisation.\footnote{Available at \url{http://www4.in.tum.de/~urbanc/regexp.html}} The notation in Isabelle/HOL for the quotient of a language @{text A} according to an equivalence relation @{term REL} is @{term "A // REL"}. We will write @{text "\<lbrakk>x\<rbrakk>\<^isub>\<approx>"} for the equivalence class defined as \mbox{@{text "{y | y \<approx> x}"}}. Central to our proof will be the solution of equational systems involving equivalence classes of languages. For this we will use Arden's Lemma \cite{Brzozowski64}, which solves equations of the form @{term "X = A ;; X \<union> B"} provided @{term "[] \<notin> A"}. However we will need the following `reverse' version of Arden's Lemma (`reverse' in the sense of changing the order of @{term "A ;; X"} to \mbox{@{term "X ;; A"}}). \begin{lemma}[Reverse Arden's Lemma]\label{arden}\mbox{}\\ If @{thm (prem 1) arden} then @{thm (lhs) arden} if and only if @{thm (rhs) arden}. \end{lemma} \begin{proof} For the right-to-left direction we assume @{thm (rhs) arden} and show that @{thm (lhs) arden} holds. From Prop.~\ref{langprops}@{text "(i)"} we have @{term "A\<star> = {[]} \<union> A ;; A\<star>"}, which is equal to @{term "A\<star> = {[]} \<union> A\<star> ;; A"}. Adding @{text B} to both sides gives @{term "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"}, whose right-hand side is equal to @{term "(B ;; A\<star>) ;; A \<union> B"}. This completes this direction. For the other direction we assume @{thm (lhs) arden}. By a simple induction on @{text n}, we can establish the property \begin{center} @{text "(*)"}\hspace{5mm} @{thm (concl) arden_helper} \end{center} \noindent Using this property we can show that @{term "B ;; (A \<up> n) \<subseteq> X"} holds for all @{text n}. From this we can infer @{term "B ;; 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) arden} we know by Prop.~\ref{langprops}@{text "(ii)"} that @{term "s \<notin> X ;; (A \<up> Suc k)"} since its length is only @{text k} (the strings in @{term "X ;; (A \<up> Suc k)"} are all longer). From @{text "(*)"} it follows then that @{term s} must be an element in @{term "(\<Union>m\<in>{0..k}. B ;; (A \<up> m))"}. This in turn implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Prop.~\ref{langprops}@{text "(iii)"} this is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed \end{proof} \noindent Regular expressions are defined as the inductive datatype \begin{center} @{text r} @{text "::="} @{term NULL}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} @{term EMPTY}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} @{term "CHAR c"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} @{term "SEQ r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} @{term "ALT r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} @{term "STAR r"} \end{center} \noindent and the language matched by a regular expression is defined as \begin{center} \begin{tabular}{c@ {\hspace{10mm}}c} \begin{tabular}{rcl} @{thm (lhs) L_rexp.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(1)}\\ @{thm (lhs) L_rexp.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(2)}\\ @{thm (lhs) L_rexp.simps(3)[where c="c"]} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(3)[where c="c"]}\\ \end{tabular} & \begin{tabular}{rcl} @{thm (lhs) L_rexp.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\ @{thm (lhs) L_rexp.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\ @{thm (lhs) L_rexp.simps(6)[where r="r"]} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(6)[where r="r"]}\\ \end{tabular} \end{tabular} \end{center} 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}. We only need to know the existence of such a regular expression and therefore we use Isabelle/HOL's @{const "fold_graph"} and Hilbert's @{text "\<epsilon>"} to define @{term "\<Uplus>rs"}. This operation, roughly speaking, folds @{const ALT} over the set @{text rs} with @{const NULL} for the empty set. We can prove that for a finite set @{text rs} % \begin{equation}\label{uplus} \mbox{@{thm (lhs) folds_alt_simp} @{text "= \<Union> (\<calL> ` rs)"}} \end{equation} \noindent holds, whereby @{text "\<calL> ` rs"} stands for the image of the set @{text rs} under function @{text "\<calL>"}.*}section {* The Myhill-Nerode Theorem, First Part *}text {* 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. \begin{definition}[Myhill-Nerode Relation] Given a language @{text A}, two strings @{text x} and @{text y} are Myhill-Nerode related provided \begin{center} @{thm str_eq_def[simplified str_eq_rel_def Pair_Collect]} \end{center} \end{definition} \noindent It is easy to see that @{term "\<approx>A"} is an equivalence relation, which partitions the set of all strings, @{text "UNIV"}, into a set of disjoint equivalence classes. To illustrate this quotient construction, let us give a simple example: consider the regular language containing just the string @{text "[c]"}. The relation @{term "\<approx>({[c]})"} partitions @{text UNIV} into three equivalence classes @{text "X\<^isub>1"}, @{text "X\<^isub>2"} and @{text "X\<^isub>3"} as follows \begin{center} @{text "X\<^isub>1 = {[]}"}\hspace{5mm} @{text "X\<^isub>2 = {[c]}"}\hspace{5mm} @{text "X\<^isub>3 = UNIV - {[], [c]}"} \end{center} One direction of the Myhill-Nerode theorem establishes 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{theorem}\label{myhillnerodeone} @{thm[mode=IfThen] Myhill_Nerode1} \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 % \begin{equation} @{thm finals_def} \end{equation} \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 @{thm lang_is_union_of_finals} and @{thm finals_in_partitions} 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 a finite set), then we can use @{text "\<bigplus>"} to obtain a regular expression that matches every string in @{text A}. Our proof of Thm.~\ref{myhillnerodeone} relies on a method that can calculate a regular expression for \emph{every} equivalence class, not just the ones in @{term "finals A"}. We first define the notion of \emph{one-character-transition} between two equivalence classes % \begin{equation} @{thm transition_def} \end{equation} \noindent which means that if we concatenate 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 @{term "X\<^isub>1 \<Turnstile>c\<Rightarrow> X\<^isub>2"}, @{term "X\<^isub>1 \<Turnstile>d\<Rightarrow> X\<^isub>3"} with @{text d} being any other character than @{text c}, and @{term "X\<^isub>3 \<Turnstile>d\<Rightarrow> X\<^isub>3"} for any @{text d}. 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 contains the empty string @{text "[]"} (since equivalence classes are disjoint). Let us assume @{text "[] \<in> X\<^isub>1"}. We build the following equational system \begin{center} \begin{tabular}{rcl} @{text "X\<^isub>1"} & @{text "="} & @{text "(Y\<^isub>1\<^isub>1, CHAR c\<^isub>1\<^isub>1) + \<dots> + (Y\<^isub>1\<^isub>p, CHAR c\<^isub>1\<^isub>p) + \<lambda>(EMPTY)"} \\ @{text "X\<^isub>2"} & @{text "="} & @{text "(Y\<^isub>2\<^isub>1, CHAR c\<^isub>2\<^isub>1) + \<dots> + (Y\<^isub>2\<^isub>o, CHAR c\<^isub>2\<^isub>o)"} \\ & $\vdots$ \\ @{text "X\<^isub>n"} & @{text "="} & @{text "(Y\<^isub>n\<^isub>1, CHAR c\<^isub>n\<^isub>1) + \<dots> + (Y\<^isub>n\<^isub>q, CHAR c\<^isub>n\<^isub>q)"}\\ \end{tabular} \end{center} \noindent where the terms @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} stand for all transitions @{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow> X\<^isub>i"}. In terms of finite automata, every equation @{text "X\<^isub>i = rhs\<^isub>i"} in this system corresponds very roughly to a state whose name is @{text X\<^isub>i} and its predecessor states are the @{text "Y\<^isub>i\<^isub>j"}; the @{text "c\<^isub>i\<^isub>j"} are the labels of the transitions from these predecessor states to @{text X\<^isub>i}. In our initial equation system there can only be finitely many terms of the form @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} in a right-hand side since by assumption there are only finitely many equivalence classes and only finitely many characters. The term @{text "\<lambda>(EMPTY)"} in the first equation acts as a marker for the equivalence class containing @{text "[]"}.\footnote{Note that we mark, roughly speaking, the single `initial' state in the equational system, which is different from the method by Brzozowski \cite{Brzozowski64}, where he marks the `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.} Overloading the function @{text \<calL>} for the two kinds of terms in the equational system, we have \begin{center} @{text "\<calL>(Y, r) \<equiv>"} % @{thm (rhs) L_rhs_item.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm} @{thm L_rhs_item.simps(1)[where r="r", THEN eq_reflection]} \end{center} \noindent and we can prove for @{text "X\<^isub>2\<^isub>.\<^isub>.\<^isub>n"} that the following equations % \begin{equation}\label{inv1} @{text "X\<^isub>i = \<calL>(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>i\<^isub>q, CHAR c\<^isub>i\<^isub>q)"}. \end{equation} \noindent hold. Similarly for @{text "X\<^isub>1"} we can show the following equation % \begin{equation}\label{inv2} @{text "X\<^isub>1 = \<calL>(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>i\<^isub>p, CHAR c\<^isub>i\<^isub>p) \<union> \<calL>(\<lambda>(EMPTY))"}. \end{equation} \noindent The reason for adding the @{text \<lambda>}-marker to our initial equational system is to obtain this equation: it only holds with the marker, since none of the other terms contain the empty string. The point of the initial equational system is that solving it means we will be able to extract a regular expression for every equivalence class. Our representation for the equations in Isabelle/HOL are pairs, where the first component is an equivalence class (a set of strings) and the second component is a set of terms. Given a set of equivalence classes @{text CS}, our initial equational system @{term "Init CS"} is thus formally defined as % \begin{equation}\label{initcs} \mbox{\begin{tabular}{rcl} @{thm (lhs) Init_rhs_def} & @{text "\<equiv>"} & @{text "if"}~@{term "[] \<in> X"}\\ & & @{text "then"}~@{term "{Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X} \<union> {Lam EMPTY}"}\\ & & @{text "else"}~@{term "{Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}"}\\ @{thm (lhs) Init_def} & @{text "\<equiv>"} & @{thm (rhs) Init_def} \end{tabular}} \end{equation} \noindent Because we use sets of terms for representing the right-hand sides of equations, we can prove \eqref{inv1} and \eqref{inv2} more concisely as % \begin{lemma}\label{inv} If @{thm (prem 1) test} then @{text "X = \<Union> \<calL> ` rhs"}. \end{lemma} \noindent Our proof of Thm.~\ref{myhillnerodeone} will proceed by transforming the initial equational system into one in \emph{solved form} maintaining the invariant in Lem.~\ref{inv}. From the solved form we will be able to read off the regular expressions. In order to transform an equational system into solved form, we have two operations: one that takes an equation of the form @{text "X = rhs"} and removes any recursive occurrences of @{text X} in the @{text rhs} using our variant of Arden's Lemma. The other operation takes an equation @{text "X = rhs"} 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} @{thm append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]} \end{center} \noindent We lift this operation to entire right-hand sides of equations, written as @{thm (lhs) append_rhs_rexp_def[where rexp="r"]}. With this we can define the \emph{arden-operation} for an equation of the form @{text "X = rhs"} as: % \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})"}\\ & & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "append_rhs_rexp 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; 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} @{thm ardenable_def} \end{center} \noindent This allows us to prove a version of Arden's Lemma on the level of equations. \begin{lemma}\label{ardenable} Given an equation @{text "X = rhs"}. If @{text "X = \<Union>\<calL> ` rhs"}, @{thm (prem 2) Arden_keeps_eq}, and @{thm (prem 3) Arden_keeps_eq}, then @{text "X = \<Union>\<calL> ` (Arden X rhs)"}. \end{lemma} \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 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} @{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'"}}\\ \end{tabular} \end{center} \noindent We again delete first all occurrences of @{text "(X, r)"} in @{text rhs}; we then calculate the regular expression corresponding to the deleted terms; finally we append this regular expression to @{text "xrhs"} and union it up with @{text rhs'}. When we use the substitution operation we will arrange it so that @{text "xrhs"} does not contain any occurrence of @{text X}. With these two operations in place, we can define the operation that removes one equation from an equational systems @{text ES}. The operation @{const Subst_all} substitutes an equation @{text "X = xrhs"} throughout an equational system @{text ES}; @{const Remove} then completely removes such an equation from @{text ES} by substituting it to the rest of the equational system, but first eliminating all recursive occurrences of @{text X} by applying @{const Arden} to @{text "xrhs"}. \begin{center} \begin{tabular}{rcl} @{thm (lhs) Subst_all_def} & @{text "\<equiv>"} & @{thm (rhs) Subst_all_def}\\ @{thm (lhs) Remove_def} & @{text "\<equiv>"} & @{thm (rhs) Remove_def} \end{tabular} \end{center} \noindent Finally, we can define how an equational system should be solved. For this we will need to iterate the process of eliminating equations until only one equation will be left in the system. However, we do not just want to have any equation as being the last one, but the one involving the equivalence class for which we want to calculate the regular expression. Let us suppose this equivalence class is @{text X}. Since @{text X} is the one to be solved, in every iteration step we have to pick an equation to be eliminated that is different from @{text X}. In this way @{text X} is kept to the final step. The choice is implemented using Hilbert's choice operator, written @{text SOME} in the definition below. \begin{center} \begin{tabular}{rc@ {\hspace{4mm}}r@ {\hspace{1mm}}l} @{thm (lhs) Iter_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-4mm}}l}{@{text "let"}}\\ & & @{text "(Y, yrhs) ="} & @{term "SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y"} \\ & & \multicolumn{2}{@ {\hspace{-4mm}}l}{@{text "in"}~~@{term "Remove ES Y yrhs"}}\\ \end{tabular} \end{center} \noindent The last definition we need applies @{term Iter} over and over until a condition @{text Cond} is \emph{not} satisfied anymore. The condition states that there are more than one equation left in the equational system @{text ES}. To solve an equational system we use Isabelle/HOL's @{text while}-operator as follows: \begin{center} @{thm Solve_def} \end{center} \noindent We are not concerned here with the definition of this operator (see Berghofer and Nipkow \cite{BerghoferNipkow00}), but note that we eliminate in each @{const Iter}-step a single equation, and therefore have a well-founded termination order by taking the cardinality of the equational system @{text ES}. This enables us to prove properties about our definition of @{const Solve} when we `call' it with the equivalence class @{text X} and the initial equational system @{term "Init (UNIV // \<approx>A)"} from \eqref{initcs} using the principle: % \begin{equation}\label{whileprinciple} \mbox{\begin{tabular}{l} @{term "invariant (Init (UNIV // \<approx>A))"} \\ @{term "\<forall>ES. invariant ES \<and> Cond ES \<longrightarrow> invariant (Iter X ES)"}\\ @{term "\<forall>ES. invariant ES \<and> Cond ES \<longrightarrow> card (Iter X ES) < card ES"}\\ @{term "\<forall>ES. invariant ES \<and> \<not> Cond ES \<longrightarrow> P ES"}\\ \hline \multicolumn{1}{c}{@{term "P (Solve X (Init (UNIV // \<approx>A)))"}} \end{tabular}} \end{equation} \noindent This principle states that given an invariant (which we will specify below) we can prove a property @{text "P"} involving @{const Solve}. For this we have to discharge the following proof obligations: first the initial equational system satisfies the invariant; second the iteration step @{text "Iter"} preserves the invariant as long as the condition @{term Cond} holds; third @{text "Iter"} decreases the termination order, and fourth that once the condition does not hold anymore then the property @{text P} must hold. The property @{term P} in our proof will state that @{term "Solve X (Init (UNIV // \<approx>A))"} returns with a single equation @{text "X = xrhs"} for some @{text "xrhs"}, and that this equational system still satisfies the invariant. In order to get the proof through, the invariant is composed of the following six properties: \begin{center} \begin{tabular}{@ {}rcl@ {\hspace{-13mm}}l @ {}} @{text "invariant ES"} & @{text "\<equiv>"} & @{term "finite ES"} & @{text "(finiteness)"}\\ & @{text "\<and>"} & @{thm (rhs) finite_rhs_def} & @{text "(finiteness rhs)"}\\ & @{text "\<and>"} & @{text "\<forall>(X, rhs)\<in>ES. X = \<Union>\<calL> ` rhs"} & @{text "(soundness)"}\\ & @{text "\<and>"} & @{thm (rhs) distinct_equas_def}\\ & & & @{text "(distinctness)"}\\ & @{text "\<and>"} & @{thm (rhs) ardenable_all_def} & @{text "(ardenable)"}\\ & @{text "\<and>"} & @{thm (rhs) valid_eqs_def} & @{text "(validity)"}\\ \end{tabular} \end{center} \noindent The first two ensure that the equational system is always finite (number of equations and number of terms in each equation); the second makes sure the `meaning' of the equations is preserved under our transformations. The other properties are a bit more technical, but are needed to get our proof through. Distinctness states that every equation in the system is distinct. @{text Ardenable} ensures that we can always apply the @{text Arden} operation. The last property states that every @{text rhs} can only contain equivalence classes for which there is an equation. Therefore @{text lhss} is just the set containing the first components of an equational system, while @{text "rhss"} collects all equivalence classes @{text X} in the terms of the form @{term "Trn X r"}. That means formally @{thm (lhs) lhss_def}~@{text "\<equiv> {X | (X, rhs) \<in> ES}"} and @{thm (lhs) rhss_def}~@{text "\<equiv> {X | (X, r) \<in> rhs}"}. It is straightforward to prove that the initial equational system satisfies the invariant. \begin{lemma}\label{invzero} @{thm[mode=IfThen] Init_ES_satisfies_invariant} \end{lemma} \begin{proof} Finiteness is given by the assumption and the way how we set up the initial equational system. Soundness is proved in Lem.~\ref{inv}. Distinctness follows from the fact that the equivalence classes are disjoint. The @{text ardenable} property also follows from the setup of the initial equational system, as does validity.\qed \end{proof} \noindent Next we show that @{text Iter} preserves the invariant. \begin{lemma}\label{iterone} @{thm[mode=IfThen] iteration_step_invariant[where xrhs="rhs"]} \end{lemma} \begin{proof} The argument boils down to choosing an equation @{text "Y = yrhs"} to be eliminated 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 @{thm (concl) Subst_all_satisfies_invariant} \end{center} \noindent Finiteness is straightforward, as the @{const Subst} and @{const Arden} operations keep the equational system finite. These operations also preserve soundness and distinctness (we proved soundness for @{const Arden} in Lem.~\ref{ardenable}). The property @{text ardenable} is clearly preserved because the append-operation cannot make a regular expression to match the empty string. Validity is given because @{const Arden} removes an equivalence class from @{text yrhs} and then @{const Subst_all} removes @{text Y} from the equational system. Having proved the implication above, we can instantiate @{text "ES"} with @{text "ES - {(Y, yrhs)}"} which matches with our proof-obligation of @{const "Subst_all"}. Since \mbox{@{term "ES = ES - {(Y, yrhs)} \<union> {(Y, yrhs)}"}}, we can use the assumption to complete the proof.\qed \end{proof} \noindent We also need the fact that @{text Iter} decreases the termination measure. \begin{lemma}\label{itertwo} @{thm[mode=IfThen] iteration_step_measure[simplified (no_asm), where xrhs="rhs"]} \end{lemma} \begin{proof} By assumption we know that @{text "ES"} is finite and has more than one element. Therefore there must be an element @{term "(Y, yrhs) \<in> ES"} with @{term "(Y, yrhs) \<noteq> (X, rhs)"}. Using the distinctness property we can infer that @{term "Y \<noteq> X"}. We further know that @{text "Remove ES Y yrhs"} removes the equation @{text "Y = yrhs"} from the system, and therefore the cardinality of @{const Iter} strictly decreases.\qed \end{proof} \noindent This brings us to our property we want to establish for @{text Solve}. \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{lemma} \begin{proof} In order to prove this lemma using \eqref{whileprinciple}, we have to use a slightly stronger invariant since Lem.~\ref{iterone} and \ref{itertwo} have the precondition that @{term "(X, rhs) \<in> ES"} for some @{text rhs}. This precondition is needed in order to choose in the @{const Iter}-step an equation that is not \mbox{@{term "X = rhs"}}. Therefore our invariant cannot be just @{term "invariant ES"}, but must be @{term "invariant ES \<and> (\<exists>rhs. (X, rhs) \<in> ES)"}. By assumption @{thm (prem 2) Solve} and Lem.~\ref{invzero}, the more general invariant holds for the initial equational system. This is premise 1 of~\eqref{whileprinciple}. Premise 2 is given by Lem.~\ref{iterone} and the fact that @{const Iter} might modify the @{text rhs} in the equation @{term "X = rhs"}, but does not remove it. Premise 3 of~\eqref{whileprinciple} is by Lem.~\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"} 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 @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"} and @{term "invariant {(X, rhs)}"} hold, as needed.\qed \end{proof} \noindent With this lemma in place we can show that for every equivalence class in @{term "UNIV // \<approx>A"} there exists a regular expression. \begin{lemma}\label{every_eqcl_has_reg} @{thm[mode=IfThen] every_eqcl_has_reg} \end{lemma} \begin{proof} By the preceding lemma, we know that there exists a @{text "rhs"} such that @{term "Solve X (Init (UNIV // \<approx>A))"} returns the equation @{text "X = rhs"}, and that the invariant holds for this equation. That means we know @{text "X = \<Union>\<calL> ` rhs"}. We further know that this is equal to \mbox{@{text "\<Union>\<calL> ` (Arden X rhs)"}} using the properties of the invariant and Lem.~\ref{ardenable}. Using the validity property for the equation @{text "X = rhs"}, we can infer that @{term "rhss rhs \<subseteq> {X}"} and because the @{text Arden} operation removes that @{text X} from @{text rhs}, that @{term "rhss (Arden X rhs) = {}"}. This means the right-hand side @{term "Arden X rhs"} can only consist of terms of the form @{term "Lam r"}. So we can collect those (finitely many) regular expressions @{text rs} and have @{term "X = L (\<Uplus>rs)"}. With this we can conclude the proof.\qed \end{proof} \noindent Lem.~\ref{every_eqcl_has_reg} allows us to finally give a proof for the first direction of the Myhill-Nerode theorem. \begin{proof}[of Thm.~\ref{myhillnerodeone}] By Lem.~\ref{every_eqcl_has_reg} we know that there exists a regular expression for every equivalence class in @{term "UNIV // \<approx>A"}. Since @{text "finals A"} is a subset of @{term "UNIV // \<approx>A"}, we also know that for every equivalence class in @{term "finals A"} there exists a regular expression. Moreover by assumption we know that @{term "finals A"} must be finite, and therefore there must be a finite set of regular expressions @{text "rs"} such that \begin{center} @{term "\<Union>(finals A) = L (\<Uplus>rs)"} \end{center} \noindent Since the left-hand side is equal to @{text A}, we can use @{term "\<Uplus>rs"} as the regular expression that is needed in the theorem.\qed \end{proof}*}section {* Myhill-Nerode, Second Part *}text {* We will prove in this section the second part of the Myhill-Nerode theorem. It can be formulated in our setting as follows. \begin{theorem} Given @{text "r"} is a regular expression, then @{thm Myhill_Nerode2}. \end{theorem} \noindent The proof will be by induction on the structure of @{text r}. It turns out the base cases are straightforward. \begin{proof}[Base Cases] The cases for @{const NULL}, @{const EMPTY} and @{const CHAR} are routine, because we can easily establish that \begin{center} \begin{tabular}{l} @{thm quot_null_eq}\\ @{thm quot_empty_subset}\\ @{thm quot_char_subset} \end{tabular} \end{center} \noindent hold, which shows that @{term "UNIV // \<approx>(L r)"} must be finite.\qed \end{proof} \noindent Much more interesting, however, are the inductive cases. They seem hard to solve directly. The reader is invited to try. Our proof will rely on some \emph{tagging-functions} defined over strings. Given the inductive hypothesis, it will be easy to prove that the \emph{range} of these tagging-functions is finite (the range of a function @{text f} is defined as @{text "range f \<equiv> f ` UNIV"}). With this we will be able to infer that the tagging-functions, seen as relations, give rise to finitely many equivalence classes of @{const UNIV}. Finally we will show that the tagging-relations are more refined than @{term "\<approx>(L r)"}, which implies that @{term "UNIV // \<approx>(L r)"} must also be finite (a relation @{text "R\<^isub>1"} is said to \emph{refine} @{text "R\<^isub>2"} provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}). We formally define the notion of a \emph{tagging-relation} as follows. \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 =tag= y \<equiv> tag x = tag y"}. \end{center} \end{definition} In order to establish finiteness of a set @{text A}, we shall use the following powerful principle from Isabelle/HOL's library. % \begin{equation}\label{finiteimageD} @{thm[mode=IfThen] finite_imageD} \end{equation} \noindent It states that if an image of a set under an injective function @{text f} (injective over this set) is finite, then the set @{text A} itself must be finite. We can use it to establish the following two lemmas. \begin{lemma}\label{finone} @{thm[mode=IfThen] finite_eq_tag_rel} \end{lemma} \begin{proof} We set in \eqref{finiteimageD}, @{text f} to be @{text "X \<mapsto> tag ` X"}. We have @{text "range f"} to be a subset of @{term "Pow (range tag)"}, which we know must be finite by assumption. Now @{term "f (UNIV // =tag=)"} is a subset of @{text "range f"}, and so also finite. Injectivity amounts to showing that @{text "X = Y"} under the assumptions that @{text "X, Y \<in> "}~@{term "UNIV // =tag="} and @{text "f X = f Y"}. From the assumptions we can obtain @{text "x \<in> X"} and @{text "y \<in> Y"} with @{text "tag x = tag y"}. Since @{text x} and @{text y} are tag-related, this in turn means that the equivalence classes @{text X} and @{text Y} must be equal.\qed \end{proof} \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{lemma} \begin{proof} We prove this lemma again using \eqref{finiteimageD}. This time we set @{text f} to be @{text "X \<mapsto>"}~@{term "{R\<^isub>1 `` {x} | x. x \<in> X}"}. It is easy to see that @{term "finite (f ` (UNIV // R\<^isub>2))"} because it is a subset of @{term "Pow (UNIV // R\<^isub>1)"}, which is finite by assumption. What remains to be shown is that @{text f} is injective on @{term "UNIV // R\<^isub>2"}. This is equivalent to showing that two equivalence classes, say @{text "X"} and @{text Y}, in @{term "UNIV // R\<^isub>2"} are equal, provided @{text "f X = f Y"}. For @{text "X = Y"} to be equal, we have to find two elements @{text "x \<in> X"} and @{text "y \<in> Y"} such that they are @{text R\<^isub>2} related. We know there exists a @{text "x \<in> X"} with \mbox{@{term "X = R\<^isub>2 `` {x}"}}. From the latter fact we can infer that @{term "R\<^isub>1 ``{x} \<in> f X"} and further @{term "R\<^isub>1 ``{x} \<in> f Y"}. This means we can obtain a @{text y} such that @{term "R\<^isub>1 `` {x} = R\<^isub>1 `` {y}"} holds. Consequently @{text x} and @{text y} are @{text "R\<^isub>1"}-related. Since by assumption @{text "R\<^isub>1"} refines @{text "R\<^isub>2"}, they must also be @{text "R\<^isub>2"}-related, as we need to show.\qed \end{proof} \noindent Chaining Lem.~\ref{finone} and \ref{fintwo} together, means in order to show that @{term "UNIV // \<approx>(L r)"} is finite, we have to find a tagging-function whose range can be shown to be finite and whose tagging-relation refines @{term "\<approx>(L r)"}. Let us attempt the @{const ALT}-case first. \begin{proof}[@{const "ALT"}-Case] We take as tagging-function % \begin{center} @{thm tag_str_ALT_def[where A="A" and B="B", THEN meta_eq_app]} \end{center} \noindent where @{text "A"} and @{text "B"} are some arbitrary languages. We can show in general, if @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"} then @{term "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))"} holds. The range of @{term "tag_str_ALT A B"} is a subset of this product set---so finite. It remains to be shown that @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} refines @{term "\<approx>(A \<union> B)"}. This amounts to showing % \begin{center} @{term "tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<longrightarrow> x \<approx>(A \<union> B) y"} \end{center} % \noindent which by unfolding the Myhill-Nerode relation is identical to % \begin{equation}\label{pattern} @{text "\<forall>z. tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<and> x @ z \<in> A \<union> B \<longrightarrow> y @ z \<in> A \<union> B"} \end{equation} % \noindent since both @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} and @{term "\<approx>(A \<union> B)"} are symmetric. To solve \eqref{pattern} we just have to unfold the definition of the tagging-function and analyse in which set, @{text A} or @{text B}, the string @{term "x @ z"} is. The definition of the tagging-function will give us in each case the information to infer that @{text "y @ z \<in> A \<union> B"}. Finally we can discharge this case by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed \end{proof} \noindent The pattern in \eqref{pattern} is repeated for the other two cases. Unfortunately, they are slightly more complicated. In the @{const SEQ}-case we essentially have to be able to infer that % \begin{center} @{text "\<dots>"}@{term "x @ z \<in> A ;; B \<longrightarrow> y @ z \<in> A ;; B"} \end{center} % \noindent using the information given by the appropriate tagging-function. The complication is to find out what the possible splits of @{text "x @ z"} are to be in @{term "A ;; B"} (this was easy in case of @{term "A \<union> B"}). To deal with this complication we define the notions of \emph{string prefixes} % \begin{center} @{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\hspace{10mm} @{text "x < y \<equiv> x \<le> y \<and> x \<noteq> y"} \end{center} % \noindent and \emph{string subtraction}: % \begin{center} \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l} @{text "[] - y"} & @{text "\<equiv>"} & @{text "[]"}\\ @{text "x - []"} & @{text "\<equiv>"} & @{text x}\\ @{text "cx - dy"} & @{text "\<equiv>"} & @{text "if c = d then x - y else cx"}\\ \end{tabular} \end{center} % \noindent where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings. Now assuming @{term "x @ z \<in> A ;; B"} there are only two possible ways of how to `split' this string to be in @{term "A ;; B"}: % \begin{center} \scalebox{0.7}{ \begin{tikzpicture} \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}@{text "x'"}\hspace{4em}$ }; \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}@{text "x - x'"}\hspace{0.5em}$ }; \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{10.1em}@{text z}\hspace{10.1em}$ }; \draw[decoration={brace,transform={yscale=3}},decorate] (xa.north west) -- ($(xxa.north east)+(0em,0em)$) node[midway, above=0.5em]{@{text x}}; \draw[decoration={brace,transform={yscale=3}},decorate] (z.north west) -- ($(z.north east)+(0em,0em)$) node[midway, above=0.5em]{@{text z}}; \draw[decoration={brace,transform={yscale=3}},decorate] ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$) node[midway, above=0.8em]{@{term "x @ z \<in> A ;; B"}}; \draw[decoration={brace,transform={yscale=3}},decorate] ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$) node[midway, below=0.5em]{@{term "(x - x') @ z \<in> B"}}; \draw[decoration={brace,transform={yscale=3}},decorate] ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$) node[midway, below=0.5em]{@{term "x' \<in> A"}}; \end{tikzpicture}} \scalebox{0.7}{ \begin{tikzpicture} \node[draw,minimum height=3.8ex] (x) { $\hspace{6.5em}@{text x}\hspace{6.5em}$ }; \node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{2em}@{text "z'"}\hspace{2em}$ }; \node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{6.1em}@{text "z - z'"}\hspace{6.1em}$ }; \draw[decoration={brace,transform={yscale=3}},decorate] (x.north west) -- ($(za.north west)+(0em,0em)$) node[midway, above=0.5em]{@{text x}}; \draw[decoration={brace,transform={yscale=3}},decorate] ($(za.north west)+(0em,0ex)$) -- ($(zza.north east)+(0em,0ex)$) node[midway, above=0.5em]{@{text z}}; \draw[decoration={brace,transform={yscale=3}},decorate] ($(x.north west)+(0em,3ex)$) -- ($(zza.north east)+(0em,3ex)$) node[midway, above=0.8em]{@{term "x @ z \<in> A ;; B"}}; \draw[decoration={brace,transform={yscale=3}},decorate] ($(za.south east)+(0em,0ex)$) -- ($(x.south west)+(0em,0ex)$) node[midway, below=0.5em]{@{text "x @ z' \<in> A"}}; \draw[decoration={brace,transform={yscale=3}},decorate] ($(zza.south east)+(0em,0ex)$) -- ($(za.south east)+(0em,0ex)$) node[midway, below=0.5em]{@{text "(z - z') \<in> B"}}; \end{tikzpicture}} \end{center} % \noindent Either there is a prefix of @{text x} in @{text A} and the rest is in @{text B} (first picture), or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B} (second picture). In both cases we have to show that @{term "y @ z \<in> A ;; B"}. For this we use the following tagging-function % \begin{center} @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B", THEN meta_eq_app]} \end{center} \noindent with the idea that in the first split we have to make sure that @{text "(x - x') @ z"} is in the language @{text B}. \begin{proof}[@{const SEQ}-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 @{term "tag_str_SEQ A B"} is a subset of this product set, and therefore finite. We have to show injectivity of this tagging-function as % \begin{center} @{term "\<forall>z. tag_str_SEQ A B x = tag_str_SEQ A B y \<and> x @ z \<in> A ;; B \<longrightarrow> y @ z \<in> A ;; B"} \end{center} % \noindent There are two cases to be considered (see pictures above). First, there exists a @{text "x'"} such that @{text "x' \<in> A"}, @{text "x' \<le> x"} and @{text "(x - x') @ z \<in> B"} hold. We therefore have % \begin{center} @{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A})"} \end{center} % \noindent and by the assumption about @{term "tag_str_SEQ A B"} also % \begin{center} @{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A})"} \end{center} % \noindent That means there must be a @{text "y'"} such that @{text "y' \<in> A"} and @{term "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}"}. This equality means that @{term "(x - x') \<approx>B (y - y')"} holds. Unfolding the Myhill-Nerode relation and together with the fact that @{text "(x - x') @ z \<in> B"}, we have @{text "(y - y') @ z \<in> B"}. We already know @{text "y' \<in> A"}, therefore @{term "y @ z \<in> A ;; B"}, as needed in this case. Second, there exists a @{text "z'"} such that @{term "x @ z' \<in> A"} and @{text "z - z' \<in> B"}. By the assumption about @{term "tag_str_SEQ A B"} we have @{term "\<approx>A `` {x} = \<approx>A `` {y}"} and thus @{term "x \<approx>A y"}. Which means by the Myhill-Nerode relation that @{term "y @ z' \<in> A"} holds. Using @{text "z - z' \<in> B"}, we can conclude also in this case with @{term "y @ z \<in> A ;; B"}. We again can complete the @{const SEQ}-case by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed \end{proof} \noindent The case for @{const STAR} is similar to @{const SEQ}, 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} \scalebox{0.7}{ \begin{tikzpicture} \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}@{text "x'\<^isub>m\<^isub>a\<^isub>x"}\hspace{4em}$ }; \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}@{text "x - x'\<^isub>m\<^isub>a\<^isub>x"}\hspace{0.5em}$ }; \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (za) { $\hspace{2em}@{text "z\<^isub>a"}\hspace{2em}$ }; \node[draw,minimum height=3.8ex, right=-0.03em of za] (zb) { $\hspace{7em}@{text "z\<^isub>b"}\hspace{7em}$ }; \draw[decoration={brace,transform={yscale=3}},decorate] (xa.north west) -- ($(xxa.north east)+(0em,0em)$) node[midway, above=0.5em]{@{text x}}; \draw[decoration={brace,transform={yscale=3}},decorate] (za.north west) -- ($(zb.north east)+(0em,0em)$) node[midway, above=0.5em]{@{text z}}; \draw[decoration={brace,transform={yscale=3}},decorate] ($(xa.north west)+(0em,3ex)$) -- ($(zb.north east)+(0em,3ex)$) node[midway, above=0.8em]{@{term "x @ z \<in> A\<star>"}}; \draw[decoration={brace,transform={yscale=3}},decorate] ($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$) node[midway, below=0.5em]{@{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"}}; \draw[decoration={brace,transform={yscale=3}},decorate] ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$) node[midway, below=0.5em]{@{term "x'\<^isub>m\<^isub>a\<^isub>x \<in> A\<star>"}}; \draw[decoration={brace,transform={yscale=3}},decorate] ($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$) node[midway, below=0.5em]{@{term "z\<^isub>b \<in> A\<star>"}}; \draw[decoration={brace,transform={yscale=3}},decorate] ($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$) node[midway, below=0.5em]{@{term "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z \<in> A\<star>"}}; \end{tikzpicture}} \end{center} % \noindent We can find a strict prefix @{text "x'"} of @{text x} such that @{term "x' \<in> A\<star>"}, @{text "x' < x"} and the rest @{term "(x - x') @ z \<in> A\<star>"}. For example the empty string @{text "[]"} would do. There are potentially many such prefixes, but there can only be finitely many of them (the string @{text x} is finite). Let us therefore choose the longest one and call it @{text "x'\<^isub>m\<^isub>a\<^isub>x"}. Now for the rest of the string @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z"} we know it is in @{term "A\<star>"}. By definition of @{term "A\<star>"}, we can separate this string into two parts, say @{text "a"} and @{text "b"}, such that @{text "a \<in> A"} and @{term "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x - x'\<^isub>m\<^isub>a\<^isub>x"}, otherwise @{text "x'\<^isub>m\<^isub>a\<^isub>x"} is not the longest prefix. That means @{text a} `overlaps' with @{text z}, splitting it into two components @{text "z\<^isub>a"} and @{text "z\<^isub>b"}. For this we know that @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"} and @{term "z\<^isub>b \<in> A\<star>"}. To cut a story short, we have divided @{term "x @ z \<in> A\<star>"} such that we have a string @{text a} with @{text "a \<in> A"} that lies just on the `border' of @{text x} and @{text z}. This string is @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a"}. In order to show that @{term "x @ z \<in> A\<star>"} implies @{term "y @ z \<in> A\<star>"}, we use the following tagging-function: % \begin{center} @{thm tag_str_STAR_def[where ?L1.0="A", THEN meta_eq_app]}\smallskip \end{center} \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. 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>"} \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 clearly have @{term "y @ z \<in> A\<star>"}. In case @{text x} is not the empty string, we can divide the string @{text "x @ z"} as shown in the picture above. By the tagging-function we have % \begin{center} @{term "\<approx>A `` {(x - x'\<^isub>m\<^isub>a\<^isub>x)} \<in> ({\<approx>A `` {x - x'} |x'. x' < x \<and> x' \<in> A\<star>})"} \end{center} % \noindent which by assumption is equal to % \begin{center} @{term "\<approx>A `` {(x - x'\<^isub>m\<^isub>a\<^isub>x)} \<in> ({\<approx>A `` {y - y'} |y'. y' < y \<and> y' \<in> A\<star>})"} \end{center} % \noindent and we know that we have a @{term "y' \<in> A\<star>"} and @{text "y' < y"} and also know @{term "(x - x'\<^isub>m\<^isub>a\<^isub>x) \<approx>A (y - y')"}. Unfolding the Myhill-Nerode relation we know @{term "(y - y') @ z\<^isub>a \<in> A"}. We also know that @{term "z\<^isub>b \<in> A\<star>"}. Therefore @{term "y' @ ((y - y') @ z\<^isub>a) @ z\<^isub>b \<in> A\<star>"}, which means @{term "y @ z \<in> A\<star>"}. As the last step we have to set @{text "A"} to @{term "L r"} and complete the proof.\qed \end{proof}*}section {* Conclusion and Related Work *}text {* In this paper we took the view that a regular language is one where there exists a regular expression that matches all of its strings. Regular expressions can conveniently be defined as a datatype in HOL-based theorem provers. For us it was therefore interesting to find out how far we can push this point of view. We have established in Isabelle/HOL both directions of the Myhill-Nerode theorem. % \begin{theorem}[The Myhill-Nerode Theorem]\mbox{}\\ A language @{text A} is regular if and only if @{thm (rhs) Myhill_Nerode}. \end{theorem} % \noindent Having formalised this theorem means we pushed our point of view quite far. Using this theorem we can obviously prove when a language is \emph{not} regular---by establishing that it has infinitely many equivalence classes generated by the Myhill-Nerode relation (this is usually the purpose of the pumping lemma \cite{Kozen97}). We can also use it to establish the standard textbook results about closure properties of regular languages. Interesting is the case of closure under complement, because it seems difficult to construct a regular expression for the complement language by direct means. However the existence of such a regular expression can be easily proved using the Myhill-Nerode theorem since % \begin{center} @{term "s\<^isub>1 \<approx>A s\<^isub>2"} if and only if @{term "s\<^isub>1 \<approx>(-A) s\<^isub>2"} \end{center} % \noindent holds for any strings @{text "s\<^isub>1"} and @{text "s\<^isub>2"}. Therefore @{text A} and the complement language @{term "-A"} give rise to the same partitions. Proving the existence of such a regular expression via automata would be quite involved. It includes the steps: regular expression @{text "\<Rightarrow>"} non-deterministic automaton @{text "\<Rightarrow>"} deterministic automaton @{text "\<Rightarrow>"} complement automaton @{text "\<Rightarrow>"} regular expression. While regular expressions are convenient in formalisations, they have some limitations. One is that there seems to be no method of calculating a minimal regular expression (for example in terms of length) for a regular language, like there is for automata. On the other hand, efficient regular expression matching, without using automata, poses no problem \cite{OwensReppyTuron09}. For an implementation of a simple regular expression matcher, whose correctness has been formally established, we refer the reader to 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 as too large to count as a concise proof pearl, this 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 arguments. Unlike Constable et al, who were able to follow the proofs from \cite{HopcroftUllman69}, we had to find our own arguments. So for us the 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 classes as the states of the minimal automaton for the regular language. However there are some subtle differences. Since we identify equivalence classes with the states of the automaton, then the most natural choice is to characterise each state with the set of strings starting from the initial state leading up to that state. Usually, however, the states are characterised as the strings starting from that state leading to the terminal states. The first choice has consequences about how the initial equational system is set up. We have the $\lambda$-term on our `initial state', while Brzozowski has it on the terminal states. This means we also need to reverse the direction of Arden's Lemma. We briefly considered using the method Brzozowski presented in the Appendix of~\cite{Brzozowski64} in order to prove the second direction of the Myhill-Nerode theorem. There he calculates the derivatives for regular expressions and shows that there can be only finitely many of them with respect to a language (if regarded equal modulo ACI). We could have used as the tag of a string @{text s} the set of derivatives of a regular expression generated by a language. Using the fact that two strings are Myhill-Nerode related whenever their derivative is the same, together with the fact that there are only finitely such derivatives would give us a similar argument as ours. However it seems not so easy to calculate the set of derivatives modulo ACI and then to count them. Therefore we preferred our direct method of using tagging-functions. This is also where our method shines, because we can completely side-step the standard argument \cite{Kozen97} where automata need to be composed, which as stated in the Introduction is not so convenient to formalise in a HOL-based theorem prover. However, it is also the direction where we had to spend most of the `conceptual' time, as our proof-argument based on tagging-functions is new for establishing the Myhill-Nerode theorem. All standard proofs of this direction proceed by arguments over automata.*}(*<*)end(*>*)