(*<*)
theory Paper
imports "../Myhill" "LaTeXsugar"
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}"

notation (latex output)
  str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and
  Seq (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
  L ("L '(_')" [0] 101) and
  EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and
  transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longrightarrow}}> _" [100, 100, 100] 100)
(*>*)


section {* Introduction *}

text {*
  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}). It seems natural to exercise theorem provers by
  formalising these theorems and by verifying formally the algorithms.

  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 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, in our case
  Isabelle/HOL. Automata are build up from states and transitions that 
  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 $A_1$ to the initial state of $A_2$:
  
  
  \begin{center}
  \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}
  \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 definition for disjoint 
  union, namely 

  \begin{center}
  @{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}"}
  \end{center}

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

  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 automata theory in Nuprl \cite{Constable00} and 
  some smaller formalisations in Coq (for example \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:

  \begin{definition}[A Regular Language]
  A language @{text A} is regular, provided there is a regular expression that matches all
  strings of @{text "A"}.
  \end{definition}
  
  \noindent
  The reason is that regular expressions, unlike graphs and matrices, can
  be easily defined as inductive datatype. Consequently a corresponding reasoning 
  infrastructure comes for free. This has recently been exploited in HOL4 with a formalisation
  of regular expression matching based on derivatives \cite{OwensSlind08}.  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. 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.\smallskip
  
  \noindent
  {\bf Contributions:} To our knowledge, our proof of the Myhill-Nerode theorem is the
  first that is based on regular expressions, only. We prove the part of this theorem 
  stating that a regular expression has only finitely many partitions using certain 
  tagging-functions. Again to our best knowledge, these tagging functions have
  not been used before to establish the Myhill-Nerode theorem.
*}

section {* Preliminaries *}

text {*
  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 ;; B"} and a language raised to the power $n$ is written 
  @{term "A \<up> n"}. Their definitions are

  \begin{center}
  @{thm Seq_def[THEN eq_reflection, where A1="A" and B1="B"]}
  \hspace{7mm}
  @{thm pow.simps(1)[THEN eq_reflection, where A1="A"]}
  \hspace{7mm}
  @{thm pow.simps(2)[THEN eq_reflection, where A1="A" and n1="n"]}
  \end{center}

  \noindent
  where @{text "@"} is the usual 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 often make use of the following properties.
  
  \begin{proposition}\label{langprops}\mbox{}\\
  \begin{tabular}{@ {}ll@ {\hspace{10mm}}ll}
  (i)   & @{thm star_cases}      & (ii)  & @{thm[mode=IfThen] pow_length}\\
  (iii) & @{thm seq_Union_left}  & 
  \end{tabular}
  \end{proposition}

  \noindent
  We omit the proofs of these properties, but invite the reader to consult
  our formalisation.\footnote{Available at ???}


  The notation 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 @{text "{y | y \<approx> x}"}.


  Central to our proof will be the solution of equational systems
  involving regular expressions. For this we will use Arden's lemma \cite{}
  which solves equations of the form @{term "X = A ;; X \<union> B"} provided
  @{term "[] \<notin> A"}. However we will need the following ``reverse'' 
  version of Arden's lemma.

  \begin{lemma}[Reverse Arden's Lemma]\mbox{}\\
  If @{thm (prem 1) ardens_revised} then
  @{thm (lhs) ardens_revised} has the unique solution
  @{thm (rhs) ardens_revised}.
  \end{lemma}

  \begin{proof}
  For the right-to-left direction we assume @{thm (rhs) ardens_revised} and show
  that @{thm (lhs) ardens_revised} holds. From Prop.~\ref{langprops}$(i)$ 
  we have @{term "A\<star> = {[]} \<union> A ;; A\<star>"},
  which is equal to @{term "A\<star> = {[]} \<union> A\<star> ;; A"}. Adding @{text B} to both 
  sides gives @{term "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"}, whose right-hand side
  is equal to @{term "(B ;; A\<star>) ;; A \<union> B"}. This completes this direction. 

  For the other direction we assume @{thm (lhs) ardens_revised}. By a simple induction
  on @{text n}, we can establish the property

  \begin{center}
  @{text "(*)"}\hspace{5mm} @{thm (concl) ardens_helper}
  \end{center}
  
  \noindent
  Using this property we can show that @{term "B ;; (A \<up> n) \<subseteq> X"} holds for
  all @{text n}. From this we can infer @{term "B ;; 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 element in @{text X}. Since @{thm (prem 1) ardens_revised}
  we know by Prop.~\ref{langprops}$(ii)$ that 
  @{term "s \<notin> X ;; (A \<up> Suc k)"} since its length is only @{text k}
  (the strings in @{term "X ;; (A \<up> Suc k)"} are all longer). 
  From @{text "(*)"} it follows then that
  @{term s} must be element in @{term "(\<Union>m\<in>{0..k}. B ;; (A \<up> m))"}. This in turn
  implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Prop.~\ref{langprops}$(iii)$ 
  this is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed
  \end{proof}

  \noindent
  Regular expressions are defined as the following inductive datatype

  \begin{center}
  @{text r} @{text "::="}
  @{term NULL}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} 
  @{term EMPTY}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} 
  @{term "CHAR c"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} 
  @{term "SEQ r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} 
  @{term "ALT r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} 
  @{term "STAR r"}
  \end{center}

  \noindent
  The language matched by a regular expression is defined as usual:

  \begin{center}
  \begin{tabular}{c@ {\hspace{10mm}}c}
  \begin{tabular}{rcl}
  @{thm (lhs) L_rexp.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(1)}\\
  @{thm (lhs) L_rexp.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(2)}\\
  @{thm (lhs) L_rexp.simps(3)[where c="c"]} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(3)[where c="c"]}\\
  \end{tabular}
  &
  \begin{tabular}{rcl}
  @{thm (lhs) L_rexp.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &
       @{thm (rhs) L_rexp.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
  @{thm (lhs) L_rexp.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &
       @{thm (rhs) L_rexp.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
  @{thm (lhs) L_rexp.simps(6)[where r="r"]} & @{text "\<equiv>"} &
      @{thm (rhs) L_rexp.simps(6)[where r="r"]}\\
  \end{tabular}
  \end{tabular}
  \end{center}

*}

section {* Finite Partitions Imply Regularity of a Language *}

text {*
  \begin{definition}[Myhill-Nerode Relation]\mbox{}\\
  @{thm str_eq_rel_def[simplified]}
  \end{definition}

  \noindent
  It is easy to see that @{term "\<approx>A"} is an equivalence relation, which partitions
  the set of all string, @{text "UNIV"}, into a set of equivalence classed. We define
  the set @{term "finals A"} as those equivalence classes that contain strings of 
  @{text A}, namely

  \begin{equation} 
  @{thm finals_def}
  \end{equation}

  \noindent
  It is easy to show that @{thm lang_is_union_of_finals} holds. We can also define 
  a notion of \emph{transition} between equivalence classes as

  \begin{equation} 
  @{thm transition_def}
  \end{equation}

  \noindent
  which means if we add the character @{text c} to all strings in the equivalence
  class @{text Y} HERE

  \begin{theorem}
  Given a language @{text A}.
  @{thm[mode=IfThen] hard_direction}
  \end{theorem}
*}

section {* Regular Expressions Generate Finitely Many Partitions *}

text {*

  \begin{theorem}
  Given @{text "r"} is a regular expressions, then @{thm rexp_imp_finite}.
  \end{theorem}  

  \begin{proof}
  By induction on the structure of @{text r}. The cases for @{const NULL}, @{const EMPTY}
  and @{const CHAR} are straightforward, because we can easily establish

  \begin{center}
  \begin{tabular}{l}
  @{thm quot_null_eq}\\
  @{thm quot_empty_subset}\\
  @{thm quot_char_subset}
  \end{tabular}
  \end{center}

  \end{proof}
*}


section {* Conclusion and Related Work *}

(*<*)
end
(*>*)