--- a/Paper/Paper.thy	Wed Feb 02 13:54:07 2011 +0000
+++ b/Paper/Paper.thy	Wed Feb 02 15:43:22 2011 +0000
@@ -25,12 +25,29 @@
 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 about this subject. Many of these textbooks, such as
+  wide range of textbooks about this subject. Many of which, such as
   \cite{Kozen97}, are aimed at students and contain very detailed
   ``pencil-and-paper'' proofs. 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 start
-  with finite automata.
+  formalising these theorems and by verifying formally the algorithms. 
+
+  There is however a problem: the typical approach to the subject of regular
+  languages is to introduce finite automata and define everything in terms of
+  automata.  For example, a regular language is nearly always defined as one
+  where there is a finite deterministic automata that recognises all the
+  strings of the language. One benefit of this approach is that it is easy
+  to prove on paper that regular languages are closed under complementation: 
+  one just has to exchange the accepting and non-accepting states in the corresponding 
+  automata into non-accepting.  The problem with automata is that they need
+  to be represented as graphs (nodes represent states and edges, transitions)
+  or as matrices (recording the transitions between states). Both representations
+  cannot be defined in terms of inductive datatypes, and a reasoning infrastructure
+  must be established manually. To our knowledge neither 
+  Isabelle nor HOL4 nor Coq have a readily usable reasoning library for graphs
+  and matrices. Moreover, the reasoning about graphs can be quite cumbersome.
+  Cosider for example the frequently used operation of combinding two automata
+  into a new compound automaton. While on paper, this can be done by just forming
+  the disjoint union of the nodes, this does not work in typed systems \dots
+