(*<*)theory Paperimports "../Myhill" "LaTeXsugar"begindeclare [[show_question_marks = false]]consts REL :: "(string \<times> string) \<Rightarrow> bool" UPLUS :: "'a set \<Rightarrow> 'a set \<Rightarrow> (nat \<times> 'a) set"notation (latex output) str_eq_rel ("\<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)(*>*)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 these 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 that it is easy to convince oneself from the fact 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 theorem prover, in our case Isabelle/HOL. Automata need to be represented as graphs or matrices, neither of which can be defined as inductive datatype.\footnote{In some works functions are used to represent state transitions, but also they are not inductive datatypes.} 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 one atomaton to the initial state of the other: \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 build the corresponding graph using the disjoint union of the state nodes and add two more nodes for the new initial state and the new accepting state. Unfortunately in HOL, the definition for disjoint union, namely \begin{center} @{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{center} \noindent changes the type---the disjoint union is not a set, but a set of pairs. Using this definition for disjoint unions means we do not have a single type for automata and hence will not be able to state properties about \emph{all} automata, since there is no type quantification available in HOL. A working alternative is to give every state node an identity, for example a natural number, and then be careful renaming these identities apart whenever connecting two automata. This results in very clunky proofs establishing that properties are invariant under renaming. Similarly, combining two automata represented as matrices results in very adhoc constructions, which are not pleasant to reason about. 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 a HOL-based theorem prover. We are only aware of the large formalisation of the automata theory in Nuprl \cite{Constable00} and some smaller in Coq \cite{Filliatre97}. In this paper, we will not attempt to formalise automata theory, 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 Regular Language] A language @{text A} is 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 and matrices, can be easily defined as inductive datatype. Therefore a corresponding reasoning infrastructure comes in Isabelle for free. 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. A corollary of this theorem will be the usual closure properties, including complementation, of regular languages. \noindent {\bf Contributions:} A proof of the Myhill-Nerode Theorem based on regular expressions. The finiteness part of this theorem is proved using tagging-functions (which to our knowledge are novel in this context).*}section {* Preliminaries *}text {* Strings in Isabelle/HOL are lists of characters and the \emph{empty string} is 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 notation for the quotient of a language @{text A} according to a relation @{term REL} is @{term "A // REL"}. The concatenation of two languages is written @{term "A ;; B"}; a language raised tow the power $n$ is written @{term "A \<up> n"}. Both concepts are defined as \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 usual list-append operation. The Kleene-star of a language @{text A} is defined as the union over all powers, namely @{thm Star_def}. Regular expressions are defined as the following 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} Central to our proof will be the solution of equational systems involving regular expressions. For this we will use the following ``reverse'' version of Arden's lemma. \begin{lemma}[Reverse Arden's Lemma]\mbox{}\\ If @{thm (prem 1) ardens_revised} then @{thm (lhs) ardens_revised} has the unique solution @{thm (rhs) ardens_revised}. \end{lemma} \begin{proof} For the right-to-left direction we assume @{thm (rhs) ardens_revised} and show that @{thm (lhs) ardens_revised} holds. From Lemma ??? 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) ardens_revised}. By a simple induction on @{text n}, we can establish the property \begin{center} @{text "(*)"}\hspace{5mm} @{thm (concl) ardens_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 Lemma ???. For the inclusion in the other direction we assume a string @{text s} with length @{text k} is element in @{text X}. Since @{thm (prem 1) ardens_revised} we know 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 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 Lemma ??? this is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed \end{proof}*}section {* Finite Partitions Imply Regularity of a Language *}text {* \begin{theorem} Given a language @{text A}. @{thm[mode=IfThen] hard_direction[where Lang="A"]} \end{theorem}*}section {* Regular Expressions Generate Finitely Many Partitions *}text {* \begin{theorem} Given @{text "r"} is a regular expressions, then @{thm rexp_imp_finite}. \end{theorem} \begin{proof} By induction on the structure of @{text r}. The cases for @{const NULL}, @{const EMPTY} and @{const CHAR} are straightforward, because we can easily establish \begin{center} \begin{tabular}{l} @{thm quot_null_eq}\\ @{thm quot_empty_subset}\\ @{thm quot_char_subset} \end{tabular} \end{center} \end{proof}*}section {* Conclusion and Related Work *}(*<*)end(*>*)