--- a/Myhill_1.thy	Sun Jan 30 17:24:37 2011 +0000
+++ b/Myhill_1.thy	Mon Jan 31 12:54:31 2011 +0000
@@ -34,7 +34,7 @@
 
 definition Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" (infixr ";;" 100)
 where 
-  "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"
+  "A ;; B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \<in> A \<and> s\<^isub>2 \<in> B}"
 
 text {* 
   Transitive closure of language @{text "L"}. 
@@ -691,7 +691,7 @@
   have "finite ((snd \<circ> the_Trn) ` items_of rhs X)" using finite_items_of[OF finite] by auto
   thus ?thesis
     apply (auto simp:rexp_of_def Seq_def items_of_def)
-    apply (rule_tac x = s1 in exI, rule_tac x = s2 in exI, auto)
+    apply (rule_tac x = "s\<^isub>1" in exI, rule_tac x = "s\<^isub>2" in exI, auto)
     by (rule_tac x= "Trn X r" in exI, auto simp:Seq_def)
 qed
 
@@ -707,7 +707,9 @@
 lemma [simp]:
   " L (attach_rexp r xb) = L xb ;; L r"
 apply (cases xb, auto simp:Seq_def)
-by (rule_tac x = "s1 @ s1a" in exI, rule_tac x = s2a in exI,auto simp:Seq_def)
+apply(rule_tac x = "s\<^isub>1 @ s\<^isub>1'" in exI, rule_tac x = "s\<^isub>2'" in exI)
+apply(auto simp: Seq_def)
+done
 
 lemma lang_of_append_rhs:
   "L (append_rhs_rexp rhs r) = L rhs ;; L r"
@@ -1211,8 +1213,8 @@
   by (auto simp:finals_def quotient_def)   
 
 theorem hard_direction: 
-  assumes finite_CS: "finite (UNIV // (\<approx>Lang))"
-  shows   "\<exists> (reg::rexp). Lang = L reg"
+  assumes finite_CS: "finite (UNIV // \<approx>Lang)"
+  shows   "\<exists> (r::rexp). Lang = L r"
 proof -
   have "\<forall> X \<in> (UNIV // (\<approx>Lang)). \<exists> (reg::rexp). X = L reg" 
     using finite_CS every_eqcl_has_reg by blast

--- 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

--- a/Paper/document/root.tex	Sun Jan 30 17:24:37 2011 +0000
+++ b/Paper/document/root.tex	Mon Jan 31 12:54:31 2011 +0000
@@ -24,7 +24,8 @@
 
 \begin{document}
 
-\title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular Expressions}
+\title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular
+  Expressions (Proof Pearl)}
 \author{Chunhan Wu\inst{1} \and Xingjuan Zhang\inst{1} \and Christian Urban\inst{2}}
 \institute{PLA University, China \and TU Munich, Germany}
 \maketitle

Binary file tphols-2011/myhill.pdf has changed