# HG changeset patch # User urbanc # Date 1296478471 0 # Node ID c19d2fc2cc69d51926b3df572a0107c5bdc86330 # Parent da85feadb8e329cf2d2fd85673d2540ac211484d a bit more on the paper diff -r da85feadb8e3 -r c19d2fc2cc69 Myhill_1.thy --- 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 \ lang \ lang" (infixr ";;" 100) where - "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \ L1 \ s2 \ L2}" + "A ;; B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \ A \ s\<^isub>2 \ B}" text {* Transitive closure of language @{text "L"}. @@ -691,7 +691,7 @@ have "finite ((snd \ 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 // (\Lang))" - shows "\ (reg::rexp). Lang = L reg" + assumes finite_CS: "finite (UNIV // \Lang)" + shows "\ (r::rexp). Lang = L r" proof - have "\ X \ (UNIV // (\Lang)). \ (reg::rexp). X = L reg" using finite_CS every_eqcl_has_reg by blast diff -r da85feadb8e3 -r c19d2fc2cc69 Paper/Paper.thy --- 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 \ string) \ bool" + + notation (latex output) str_eq_rel ("\\<^bsub>_\<^esub>") and Seq (infixr "\" 100) and Star ("_\<^bsup>\\<^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 ("\") (*>*) @@ -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 diff -r da85feadb8e3 -r c19d2fc2cc69 Paper/document/root.tex --- 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 diff -r da85feadb8e3 -r c19d2fc2cc69 tphols-2011/myhill.pdf Binary file tphols-2011/myhill.pdf has changed