--- a/Paper/Paper.thy	Sun Feb 06 10:28:29 2011 +0000
+++ b/Paper/Paper.thy	Sun Feb 06 11:21:12 2011 +0000
@@ -9,6 +9,8 @@
  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
@@ -19,9 +21,11 @@
   quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and
   REL ("\<approx>") and
   UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90) and
-  L ("L '(_')" [0] 101)
+  L ("L '(_')" [0] 101) and
+  EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) 
 (*>*)
 
+
 section {* Introduction *}
 
 text {*
@@ -41,8 +45,8 @@
   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 consist of states and transitions. They need to be represented 
-  as graphs or matrices, neither
+  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
@@ -125,7 +129,7 @@
   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 renaming these identities apart whenever
+  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
@@ -134,7 +138,7 @@
   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 
+  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 
@@ -150,10 +154,10 @@
   \noindent
   The reason is that regular expressions, unlike graphs and matrices, can
   be easily defined as inductive datatype. Therefore a corresponding reasoning 
-  infrastructure comes for free. This has recently been used for formalising regular 
-  expression matching in HOL4 \cite{OwensSlind08}.  The purpose of this paper is to
+  infrastructure comes for free. This has recently been used in HOL4 for formalising 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 give a necessary
+  can be recreated by only using regular expressions. This theorem gives a necessary
   and sufficient condition 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
@@ -261,14 +265,27 @@
   \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}
+
+  \begin{definition} @{text "finals A"} are the equivalence classes that contain
+  strings from @{text A}\\
+  @{thm finals_def}
+  \end{definition}
+
+  @{thm lang_is_union_of_finals}
+
+
   \begin{theorem}
   Given a language @{text A}.
-  @{thm[mode=IfThen] hard_direction[where Lang="A"]}
+  @{thm[mode=IfThen] hard_direction}
   \end{theorem}
 *}