
diff -r c1d9a4ac9f8e -r 828ea293b61f Paper/Paper.thy
--- a/Paper/Paper.thy	Fri Feb 04 13:33:18 2011 +0000
+++ b/Paper/Paper.thy	Fri Feb 04 22:54:29 2011 +0000
@@ -7,6 +7,7 @@
 
 consts
  REL :: "(string \<times> string) \<Rightarrow> bool"
+ UPLUS :: "'a set \<Rightarrow> 'a set \<Rightarrow> (nat \<times> 'a) set"
 
 
 notation (latex output)
@@ -16,8 +17,8 @@
   pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and
   Suc ("_+1" [100] 100) and
   quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and
-  REL ("\<approx>")
-
+  REL ("\<approx>") and
+  UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90)
 (*>*)
 
 section {* Introduction *}
@@ -25,77 +26,135 @@
 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
+  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 with this: 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 where
-  there is a finite deterministic automaton that recognises all the strings of
-  the language. This approach has many benefits. One 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 corresponding 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 nor HOLlight support them with libraries.
+  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 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 corresponding automaton to
+  obtain an automaton for the complement language.  The problem, however, 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 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 one atomaton to the 
+  initial state of the other:
   
-  Even worse, reasoning about graphs in typed languages can be a real hassle. 
-  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):
   
   \begin{center}
-  picture
+  \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
-  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. In a theorem
-  prover based on set-theory, this operaton can be more or less
-  straightforwardly implemented. But in a HOL-based theorem prover the
-  standard definition of disjoint unions as pairs
+  On ``paper'' we can build the corresponding graph using the disjoint union of 
+  the state nodes and add 
+  two more nodes for the new initial state and the new accepting 
+  state. Unfortunately in HOL, the definition for disjoint 
+  union, namely 
 
   \begin{center}
-  definition
+  @{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 (from sets of nodes to sets of pairs). This means we
-  cannot formulate in this represeantation any property about \emph{all} 
-  automata---since there is no type quantification available in HOL-based
-  theorem provers. A working alternative is to give every state node an 
-  identity, for example a natural number, and then be careful to rename
-  these indentities appropriately when connecting two automata together. 
-  This results in very clunky side-proofs establishing that properties
-  are invariant under renaming. We are only aware of the formalisation 
-  of automata theory in Nuprl that carries this approach trough and is
-  quite substantial. 
+  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. A working
+  alternative is to give every state node an identity, for example a natural
+  number, and then be careful renaming these identities apart whenever
+  connecting two automata. This results in very clunky proofs
+  establishing that properties are invariant under renaming. Similarly,
+  combining 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 the automata theory in Nuprl \cite{Constable00} and 
+  some smaller in Coq \cite{Filliatre97}.
   
-  We will take a completely different approach to formalising theorems
-  about regular languages. Instead of defining a regular language as one 
-  where there exists an automaton that recognises all of its strings, we 
-  define a regular language as
+  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, if there is a regular expression that matches all
+  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 expressinons, unlike graphs and metrices, can
-  be eaily defined as inductive datatype and this means a reasoning infrastructre
-  comes for them in Isabelle for free. The purpose of this paper is to
-  show that a central and highly non-trivisl result about regular languages, 
-  namely the Myhill-Nerode theorem,  can be recreated only using regular 
-  expressions. In our approach we do not need to formalise graps or
-  metrices.
+  The reason is that regular expressions, unlike graphs and matrices, can
+  be easily defined as inductive datatype. Therefore a corresponding reasoning 
+  infrastructure comes in Isabelle for free. 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. A corollary of this
+  theorem will be the usual closure properties, including complementation,
+  of regular languages.
   
 
   \noindent




