(*<*)+
−
theory Paper+
−
imports "../Myhill" "LaTeXsugar"+
−
begin+
−
+
−
declare [[show_question_marks = false]]+
−
+
−
consts+
−
 REL :: "(string \<times> string) \<Rightarrow> bool"+
−
+
−
+
−
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>")+
−
+
−
(*>*)+
−
+
−
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 containing 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 with this: the typical approach to regular+
−
  languages is to introduce automata and then define everything in terms of+
−
  them.  For example, a regular language is normally defined as one where+
−
  there is a finite deterministic automaton that recognises all the strings of+
−
  the language. One benefit of this approach is that it is easy to convince+
−
  oneself from the fact that regular languages are closed under+
−
  complementation: one just has to exchange the accepting and non-accepting+
−
  states in the automaton to obtain an automaton for the complement language.+
−
  +
−
  The problem lies with formalising such reasoning in a theorem+
−
  prover, in our case Isabelle/HOL. Automata 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 transitions, but they are also not +
−
  inductive datatypes.} This means we have to build our own reasoning infrastructure+
−
  for them, as neither Isabelle nor HOL4 support them with libraries.+
−
  Even worse, reasoning about graphs in typed languages can be a real hassle+
−
  making proofs quite clunky. Consider for example the operation of combining +
−
  two automata into a new automaton by connecting their+
−
  initial states to a new initial state (similarly with the accepting states):a+
−
  +
−
  \begin{center}+
−
  picture+
−
  \end{center}+
−
+
−
  \noindent+
−
  How should we implement this operation? On paper we can just+
−
  form the disjoint union of the state nodes and add two more nodes---one for the+
−
  new initial state, the other for the new accepting state.+
−
+
−
+
−
  +
−
+
−
  +
−
  +
−
+
−
+
−
+
−
  Therefore instead of defining a regular language as being one where there exists an+
−
  automata that recognises all of its strings, we define +
−
+
−
  \begin{definition}[A Regular Language]+
−
  A language @{text A} is regular, if there is a regular expression that matches all+
−
  strings of @{text "A"}.+
−
  \end{definition}+
−
  +
−
  \noindent+
−
  {\bf Contributions:} A proof of the Myhill-Nerode Theorem based on regular expressions. The +
−
  finiteness part of this theorem is proved using tagging-functions (which to our knowledge+
−
  are novel in this context).+
−
  +
−
*}+
−
+
−
section {* Preliminaries *}+
−
+
−
text {*+
−
  Strings in Isabelle/HOL are lists of characters and the+
−
  \emph{empty string} is 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 notation for the quotient of a language @{text A} according to a relation @{term REL} is+
−
  @{term "A // REL"}. The concatenation of two languages is written @{term "A ;; B"}; a language +
−
  raised  tow the power $n$ is written @{term "A \<up> n"}. Both concepts are defined as+
−
+
−
  \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}.+
−
  +
−
+
−
  Regular expressions are defined as the following 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}+
−
+
−
  Central to our proof will be the solution of equational systems+
−
  involving regular expressions. For this we will use 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 Lemma ??? 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 Lemma ???.+
−
  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 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 Lemma ??? this+
−
  is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed+
−
  \end{proof}+
−
*}+
−
+
−
section {* Finite Partitions Imply Regularity of a Language *}+
−
+
−
text {*+
−
  \begin{theorem}+
−
  Given a language @{text A}.+
−
  @{thm[mode=IfThen] hard_direction[where Lang="A"]}+
−
  \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+
−
(*>*)+
−