(*<*)

theory Paper

imports "../Closures" 

begin

declare [[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"

abbreviation

  "pow" (infixl "\<up>" 100)

where

  "A \<up> n \<equiv> A ^^ n"

syntax (latex output)

  "_Collect" :: "pttrn => bool => 'a set"              ("(1{_ | _})")

  "_CollectIn" :: "pttrn => 'a set => bool => 'a set"   ("(1{_ \<in> _ | _})")

translations

  "_Collect p P"      <= "{p. P}"

  "_Collect p P"      <= "{p|xs. P}"

  "_CollectIn p A P"  <= "{p : A. P}"

abbreviation "ZERO \<equiv> Zero"

abbreviation "ONE \<equiv> One"

abbreviation "ATOM \<equiv> Atom"

abbreviation "PLUS \<equiv> Plus"

abbreviation "TIMES \<equiv> Times"

abbreviation "TIMESS \<equiv> Times_set"

abbreviation "STAR \<equiv> Star"

notation (latex output)

  str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and

  str_eq ("_ \<approx>\<^bsub>_\<^esub> _") and

  conc (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

  lang ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and

  lang_trm ("\<^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_rexp_rhs ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and

  uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and

  tag_str_Plus ("tag\<^bsub>PLUS\<^esub> _ _" [100, 100] 100) and

  tag_str_Plus ("tag\<^bsub>PLUS\<^esub> _ _ _" [100, 100, 100] 100) and

  tag_str_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and

  tag_str_Times ("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) and

  tag_eq_rel ("\<^raw:$\threesim$>\<^bsub>_\<^esub>") and

  Delta ("\<Delta>'(_')") and

  nullable ("\<delta>'(_')")

lemma meta_eq_app:

  shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"

  by auto

lemma conc_def':

  "A \<cdot> B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \<in> A \<and> s\<^isub>2 \<in> B}"

unfolding conc_def by simp

lemma conc_Union_left: 

  shows "B \<cdot> (\<Union>n. A \<up> n) = (\<Union>n. B \<cdot> (A \<up> n))"

unfolding conc_def by auto

lemma test:

  assumes X_in_eqs: "(X, rhs) \<in> Init (UNIV // \<approx>A)"

  shows "X = \<Union> (lang_trm `  rhs)"

using assms l_eq_r_in_eqs by (simp)

(* THEOREMS *)

notation (Rule output)

  "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")

syntax (Rule output)

  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"

  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")

  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 

  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")

  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")

notation (Axiom output)

  "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")

notation (IfThen output)

  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

syntax (IfThen output)

  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"

  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")

  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")

notation (IfThenNoBox output)

  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

syntax (IfThenNoBox output)

  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"

  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")

  "_asm" :: "prop \<Rightarrow> asms" ("_")

(*>*)

section {* Introduction *}

text {*

  \noindent

  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,

  HopcroftUllman69}). It seems natural to exercise theorem provers by

  formalising the theorems and by verifying formally the algorithms.  A

  popular choice for a theorem prover would be one based on Higher-Order Logic

  (HOL), for example HOL4, HOLlight or Isabelle/HOL. For the development

  presented in this paper we will use the latter. HOL is a predicate calculus

  that allows quantification over predicate variables. Its type system is

  based on Church's Simple Theory of Types \cite{Church40}.  Although 

  many mathematical concepts can be conveniently expressed in HOL, there are some

  limitations that hurt badly, if one attempts a simple-minded formalisation

  of regular languages in it.

  The typical approach to regular languages is to introduce finite automata

  and then define everything in terms of them \cite{Kozen97}.  For example, 

  a regular language is normally defined as:

  \begin{dfntn}\label{baddef}

  A language @{text A} is \emph{regular}, provided there is a 

  finite deterministic automaton that recognises all strings of @{text "A"}.

  \end{dfntn}

  \noindent  

  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. 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, because

  we have to be able to combine automata.  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.9]

  %\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.9]

  %\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' or a theorem prover based on set-theory, 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}

  @{text "A\<^isub>1 \<uplus> A\<^isub>2 \<equiv> {(1, x) | x \<in> A\<^isub>1} \<union> {(2, 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. As a result we will not be able to define a regular

  language as one for which there exists an automaton that recognises all its

  strings. This is because we cannot make a definition in HOL that is polymorphic in 

  the state type and also 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}.

  Also one might consider automata theory as well-worn stock material 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

  `sink' state from which there is no connection to a final state (Brozowski

  mentions this side-condition in connection with state complexity

  \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

  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.

  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

  usually taken. 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{dfntn}

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

  strings of @{text "A"}.

  \end{dfntn}

  \noindent

  The reason is that regular expressions, unlike graphs, matrices and

  functions, can be easily defined as an inductive datatype. A reasoning

  infrastructure (like induction and recursion) comes then for free in

  HOL. Moreover, no side-conditions will be needed for regular expressions,

  like we usually need for automata. This convenience of regular expressions 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

  main 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.\medskip

  \noindent 

  {\bf Contributions:} There is an extensive literature on regular languages.

  To our best knowledge, our proof of the Myhill-Nerode theorem is the first

  that is based on regular expressions, only. The part of this theorem stating

  that finitely many partitions imply regularity of the language is proved by

  an argument about solving equational sytems.  This argument appears to be

  folklore. For the other part, we give two proofs: one direct proof using

  certain tagging-functions, and another indirect proof using Antimirov's

  partial derivatives \cite{Antimirov95}. Again to our best knowledge, the

  tagging-functions have not been used before to establish the Myhill-Nerode

  theorem. Derivatives of regular expressions have been used widely in the

  literature about regular expressions. However, partial derivatives are more

  suitable in the context of the Myhill-Nerode theorem, since it is easier to

  establish formally their finiteness result.

*}

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}

  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 \<cdot> B"} and a language raised to the power @{text n} is written 

  @{term "A \<up> n"}. They are defined as usual

  \begin{center}

  @{thm conc_def'[THEN eq_reflection, where A1="A" and B1="B"]}

  \hspace{7mm}

  @{thm lang_pow.simps(1)[THEN eq_reflection, where A1="A"]}

  \hspace{7mm}

  @{thm lang_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{prpstn}\label{langprops}\mbox{}\\

  \begin{tabular}{@ {}ll}

  (i)   & @{thm star_cases}     \\ 

  (ii)  & @{thm[mode=IfThen] pow_length}\\

  (iii) & @{thm conc_Union_left} \\ 

  \end{tabular}

  \end{prpstn}

  \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

  which solves equations of the form @{term "X = A \<cdot> 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 \<cdot> X"} to

  \mbox{@{term "X \<cdot> A"}}).

  \begin{lmm}[Reverse Arden's Lemma]\label{arden}\mbox{}\\

  If @{thm (prem 1) arden} then

  @{thm (lhs) arden} if and only if

  @{thm (rhs) arden}.

  \end{lmm}

  \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 \<cdot> A\<star>"},

  which is equal to @{term "A\<star> = {[]} \<union> A\<star> \<cdot> A"}. Adding @{text B} to both 

  sides gives @{term "B \<cdot> A\<star> = B \<cdot> ({[]} \<union> A\<star> \<cdot> A)"}, whose right-hand side

  is equal to @{term "(B \<cdot> A\<star>) \<cdot> 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 \<cdot> (A \<up> n) \<subseteq> X"} holds for

  all @{text n}. From this we can infer @{term "B \<cdot> 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 \<cdot> (A \<up> Suc k)"} since its length is only @{text k}

  (the strings in @{term "X \<cdot> (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 \<cdot> (A \<up> m))"}. This in turn

  implies that @{term s} is in @{term "(\<Union>n. B \<cdot> (A \<up> n))"}. Using Prop.~\ref{langprops}@{text "(iii)"} 

  this is equal to @{term "B \<cdot> A\<star>"}, as we needed to show.

  \end{proof}

  \noindent

  Regular expressions are defined as the inductive datatype

  \begin{center}

  \end{center}

  \noindent

  and the language matched by a regular expression is defined as

  \begin{center}

  @{thm (lhs) lang.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) lang.simps(1)}\\

  @{thm (lhs) lang.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) lang.simps(2)}\\

  @{thm (lhs) lang.simps(3)[where a="c"]} & @{text "\<equiv>"} & @{thm (rhs) lang.simps(3)[where a="c"]}\\

  @{thm (lhs) lang.simps(4)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]} & @{text "\<equiv>"} &

       @{thm (rhs) lang.simps(4)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]}\\

  @{thm (lhs) lang.simps(5)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]} & @{text "\<equiv>"} &

       @{thm (rhs) lang.simps(5)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]}\\

  @{thm (lhs) lang.simps(6)[where r="r"]} & @{text "\<equiv>"} &

      @{thm (rhs) lang.simps(6)[where r="r"]}\\

  \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