--- a/Paper/Paper.thy	Sun Jan 30 17:24:37 2011 +0000
+++ b/Paper/Paper.thy	Mon Jan 31 12:54:31 2011 +0000
@@ -5,13 +5,18 @@
 
 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)
+  Suc ("_+1>" [100] 100) and
+  quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and
+  REL ("\<approx>")
 
 
 (*>*)
@@ -19,12 +24,53 @@
 section {* Introduction *}
 
 text {*
+
+  Therefore instead of defining a regular language as being one where there exists an
+  automata that regognises 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 Myhil-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. Therefore the
+  \emph{empty string} is represented by the empty list, written @{term "[]"}. \emph{Languages} are sets of 
+  strings. The language containing all strings is abbreviated as @{term "UNIV::string set"}
+  and the notation for the quotient of a language @{text A} according to a relation @{term REL} is
+  @{term "A // REL"}.
+  
+  Set operations
+
+  \begin{center}
+  @{thm Seq_def}
+  \end{center}
+
+  \noindent
+  where @{text "@"} is the usual list-append operation.
+
+  \noindent
+  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.
@@ -63,13 +109,22 @@
   \end{proof}
 *}
 
-section {* Regular expressions have finitely many partitions *}
+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{lemma}
+  \begin{theorem}
   Given @{text "r"} is a regular expressions, then @{thm rexp_imp_finite}.
-  \end{lemma}  
+  \end{theorem}  
 
   \begin{proof}
   By induction on the structure of @{text r}. The cases for @{const NULL}, @{const EMPTY}
@@ -83,13 +138,12 @@
   \end{tabular}
   \end{center}
 
-  
-
   \end{proof}
-
 *}
 
 
+section {* Conclusion and Related Work *}
+
 (*<*)
 end
 (*>*)
\ No newline at end of file