(*<*)

theory Paper

imports "../Closures" "../Attic/Prefix_subtract" 

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> Timess"

abbreviation "STAR \<equiv> Star"

notation (latex output)

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

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

  conc (infixr "\<cdot>" 100) 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}}>" 101) 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_Plus ("+tag _ _" [100, 100] 100) and

  tag_Plus ("+tag _ _ _" [100, 100, 100] 100) and

  tag_Times ("\<times>tag _ _" [100, 100] 100) and

  tag_Times ("\<times>tag _ _ _" [100, 100, 100] 100) and

  tag_Star ("\<star>tag _" [100] 100) and

  tag_Star ("\<star>tag _ _" [100, 100] 100) and

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

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

  Cons ("_ :: _" [100, 100] 100) and

  Rev ("Rev _" [1000] 100) and

  Der ("Der _ _" [1000, 1000] 100) and

  ONE ("ONE" 999) and

lemma meta_eq_app:

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

  by auto

lemma str_eq_def':

  shows "x \<approx>A y \<equiv> (\<forall>z. x @ z \<in> A \<longleftrightarrow> y @ z \<in> A)"

unfolding str_eq_def by simp

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

  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=1]

  %\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 {\small$A_1$};

  \draw ( 0.6,0.0) node {\small$A_2$};

  \end{tikzpicture}

  & 

  &

  \begin{tikzpicture}[scale=1]

  %\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 {\small$A_1$};

  \draw ( 0.6,0.0) node {\small$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}

  @{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 (Definition~\ref{baddef}). This is because we cannot make a definition in HOL that is polymorphic in 

  the state type and there is no type quantification available in HOL (unlike 

  in Coq, for example).\footnote{Slind already pointed out this problem in an email 

  to the HOL4 mailing list on 21st April 2005.}

  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''. Since he does not need to define what regular

  languages are, Nipkow 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 and regular languages as a well-worn

  stock subject where everything is crystal clear. However, paper proofs about

  automata often involve subtle side-conditions which are easily overlooked,

  but which make formal reasoning rather painful. For example Kozen's proof of

  the Myhill-Nerode theorem requires that automata do not have inaccessible

  states \cite{Kozen97}. Another subtle side-condition is completeness of

  automata, that is automata need to have total transition functions and at

  most one `sink' state from which there is no connection to a final state

  (Brzozowski mentions this side-condition in the context of state complexity

  of automata \cite{Brzozowski10}). Such side-conditions mean that if we

  define a regular language as one for which there exists \emph{a} finite

  need a lemma which ensures that another equivalent one can be found

  satisfying the side-condition. Unfortunately, such `little' and `obvious'

  lemmas make a formalisation of automata theory a hair-pulling experience.

  In this paper, we will not attempt to formalise automata theory in

  Isabelle/HOL nor will we attempt to formalise automata proofs from the

  literature, but take a different approach to regular languages than is

  usually taken. Instead of defining a regular language as one where there

  exists an automaton that recognises all its strings, we define a

  regular language as:

  \begin{dfntn}\label{regular}

  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 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 systems.  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 recently quite

  widely in the literature; partial derivatives, in contrast, attract much

  less attention. However, partial derivatives are more suitable in the

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

  formally their finiteness result. We are not aware of any proof that uses

  either of them for proving the Myhill-Nerode theorem.

*}

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 "[]"}.  We assume there

  are only finitely many different characters.  \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}

  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

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

  & @{text "\<equiv>"} & @{thm (rhs) conc_def'[THEN eq_reflection, where A1="A" and B1="B"]}\\

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

  & @{text "\<equiv>"} & @{thm (rhs) lang_pow.simps(1)[THEN eq_reflection, where A1="A"]}\\

  @{thm (lhs) lang_pow.simps(2)[THEN eq_reflection, where A1="A" and n1="n"]}

  & @{text "\<equiv>"} & @{thm (rhs) lang_pow.simps(2)[THEN eq_reflection, where A1="A" and n1="n"]}

  \end{tabular}

  \end{center}

  \noindent

  where @{text "@"} is the list-append operation. The Kleene-star of a language @{text A}

  is defined as the union over all powers, namely @{thm star_def}. In the paper

  we will make use of the following properties of these constructions.

  \begin{prpstn}\label{langprops}\mbox{}\\

  \begin{tabular}{@ {}lp{10cm}}

  (i)   & @{thm star_unfold_left}     \\ 

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

  (iii) & @{thm conc_Union_left} \\ 

  (iv)  & If @{thm (prem 1) star_decom} and @{thm (prem 2) star_decom} then

          there exists an @{text "x\<^isub>p"} and @{text "x\<^isub>s"} with @{text "x = x\<^isub>p @ x\<^isub>s"} 

          and @{term "x\<^isub>p \<noteq> []"} such that @{term "x\<^isub>p \<in> A"} and @{term "x\<^isub>s \<in> A\<star>"}.

  \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}.  

  Property @{text "(iv)"} states that a non-empty string in @{term "A\<star>"} can

  always be split up into a non-empty prefix belonging to @{text "A"} and the

  rest being in @{term "A\<star>"}. 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}"}}, and have @{text "x \<approx> y"} if and only if @{text

  "\<lbrakk>x\<rbrakk>\<^isub>\<approx> = \<lbrakk>y\<rbrakk>\<^isub>\<approx>"}.

  Central to our proof will be the solution of equational systems

  involving equivalence classes of languages. For this we will use Arden's Lemma 

  (see \cite[Page 100]{Sakarovitch09}),

  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> = A \<cdot> A\<star> \<union> {[]}"},

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

  sides gives @{term "B \<cdot> A\<star> = B \<cdot> (A\<star> \<cdot> A \<union> {[]})"}, 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}

  \begin{tabular}{rcl}

  @{text r} & @{text "::="} & @{term ZERO}\\