UPLUS :: "'a set \<Rightarrow> 'a set \<Rightarrow> (nat \<times> 'a) set"

  REL ("\<approx>") and

  UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90)

  wide range of textbooks on this subject, many of which are aimed at students

  and contain very detailed ``pencil-and-paper'' proofs

  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{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}

  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 

  @{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}"}

  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

  A language @{text A} is regular, provided there is a regular expression that matches all

  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.