(*<*)
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
(*>*)