(*<*)

theory Paper

imports "../Closures2" "../Attic/Prefix_subtract" 

begin

declare [[show_question_marks = false]]

consts

 REL :: "(string \<times> string) set"

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

syntax (latex output)

  "_UNION_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00\<^bsub>_ \<le> _\<^esub>)/ _)" [0, 0, 10] 10)

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"

abbreviation "ALLS \<equiv> Star Allreg"

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

  uminus ("\<^raw:\ensuremath{\overline{\isa{>_\<^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

  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

  pderivs_set ("pderss") and

  SUBSEQ ("Sub") and

  SUPSEQ ("Sup") and

  UP ("'(_')\<up>") and

  ALLS ("ALL")

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)

abbreviation

  notprec ("_ \<^raw:\mbox{$\not\preceq$}>_")

where

 "notprec x y \<equiv> \<not>(x \<preceq> y)"

abbreviation

  minimal_syn ("min\<^bsub>_\<^esub> _")

where

  "minimal_syn A x \<equiv> minimal x A"   

(* 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.~the textbooks by \citeN{HopcroftUllman69} and by \citeN{Kozen97}). 

  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 the Simple Theory of Types by \citeN{Church40}.  Although many

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

  limitations that hurt when attempting a simple-minded formalisation

  of regular languages in it. 

  The typical approach to

  regular languages, taken for example by \citeN{HopcroftUllman69}

  and by \citeN{Kozen97},  is to introduce finite deterministic automata and then

  define most notions 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 

  theorem prover. Automata are built up from states and transitions that are 

  commonly represented as graphs, matrices or functions, none of which, unfortunately, 

  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. Also, reasoning about graphs and

  matrices can be a hassle in 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 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.}

  %$^,$\footnote{While in Coq one can avoid 

  %this particular problem, all other difficulties we point out below still apply.}

  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. \citeN{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. \citeN{Nipkow98} establishes

  the link between regular expressions and automata in the context of

  lexing. \citeN{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 by

  \citeN{Constable00} and in Coq by \citeN{Filliatre97}, \citeN{Almeidaetal10}

  and \citeN{Braibant12}.

  %Also, one might consider automata as just convenient `vehicles' for

  %establishing properties about regular languages.  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}, but it is also needed

  %in the usual construction of the complement automaton). 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 (see

  %Definition~\ref{baddef}), then we need a lemma which ensures that another

  %equivalent one can be found satisfying the side-condition, and also need to

  %make sure our operations on automata preserve them. 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 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

  And then `forget' automata completely.

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

  %functions, 

  can be defined as an inductive datatype and a reasoning

  infrastructure for them (like induction and recursion) comes 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 by \citeN{OwensSlind08}, and with an equivalence

  checker for regular expressions in Isabelle/HOL by \citeN{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. We use the Continuation Lemma, which is also a corollary 

  of the Myhill-Nerode Theorem, for establishing 

  the non-regularity of the language @{text "a\<^isup>nb\<^isup>n"}.\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 \citeyear{Antimirov95}. Again to our best knowledge, the

  tagging-functions have not been used before for establishing 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