(*<*)

theory Paper

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"

definition

  Delta :: "'a lang \<Rightarrow> 'a lang"

where

  "Delta A = (if [] \<in> A then {[]} else {})"

notation (latex output)

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

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

  conc (infixr "\<cdot>" 100) and

  star ("_\<^bsup>\<star>\<^esup>" [101] 200) 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

  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

  tag_eq ("\<^raw:$\threesim$>\<^bsub>_\<^esub>" [100] 100) and

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

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

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

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

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

  Derivs ("Ders") and

  ONE ("ONE" 999) and

  ZERO ("ZERO" 999) and

  pderivs_lang ("pdersl") and

  UNIV1 ("UNIV\<^isup>+") and

  Deriv_lang ("Dersl") and

  Derivss ("Derss") and

  deriv ("der") and

  derivs ("ders") and

  pderiv ("pder") and

  pderivs ("pders") and

lemmas Deriv_simps = Deriv_empty Deriv_epsilon Deriv_char Deriv_union

definition

  Der :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"

where

  "Der c A \<equiv> {s. [c] @ s \<in> A}"

definition

  Ders :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"

where

  "Ders s A \<equiv> {s'. s @ s' \<in> A}"

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" ("_")

lemma pow_length:

  assumes a: "[] \<notin> A"

  and     b: "s \<in> A \<up> Suc n"

  shows "n < length s"

using b

proof (induct n arbitrary: s)

  case 0

  have "s \<in> A \<up> Suc 0" by fact

  with a have "s \<noteq> []" by auto

  then show "0 < length s" by auto

next

  case (Suc n)

  have ih: "\<And>s. s \<in> A \<up> Suc n \<Longrightarrow> n < length s" by fact

  have "s \<in> A \<up> Suc (Suc n)" by fact

  then obtain s1 s2 where eq: "s = s1 @ s2" and *: "s1 \<in> A" and **: "s2 \<in> A \<up> Suc n"

    by (auto simp add: Seq_def)

  from ih ** have "n < length s2" by simp

  moreover have "0 < length s1" using * a by auto

  ultimately show "Suc n < length s" unfolding eq 

    by (simp only: length_append)

qed

(*>*)

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 Isabelle/HOL. 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

  of regular languages in it. 

  The typical approach (for example \cite{HopcroftUllman69,Kozen97}) to

  regular languages is to introduce finite deterministic automata and then

  define everything in terms of them.  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}

  & 

  \raisebox{2.1mm}{\bf\Large$\;\;\;\Rightarrow\,\;\;$}

  &

  \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 the states of automata. As a result we will not be able to

  define in our fomalisation 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 only polymorphic in

  the state type, but not in the predicate for regularity; 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 states of 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\smallskip

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

  \noindent

  and\smallskip

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

  \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, e.g.~\cite{Filliatre97,Almeidaetal10}.

  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

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