3 imports "../Myhill" "LaTeXsugar" |
3 imports "../Myhill" "LaTeXsugar" |
4 begin |
4 begin |
5 |
5 |
6 declare [[show_question_marks = false]] |
6 declare [[show_question_marks = false]] |
7 |
7 |
|
8 consts |
|
9 REL :: "(string \<times> string) \<Rightarrow> bool" |
|
10 |
|
11 |
8 notation (latex output) |
12 notation (latex output) |
9 str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and |
13 str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and |
10 Seq (infixr "\<cdot>" 100) and |
14 Seq (infixr "\<cdot>" 100) and |
11 Star ("_\<^bsup>\<star>\<^esup>") and |
15 Star ("_\<^bsup>\<star>\<^esup>") and |
12 pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and |
16 pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and |
13 Suc ("_+1" [100] 100) and |
17 Suc ("_+1>" [100] 100) and |
14 quotient ("_ \<^raw:\ensuremath{\sslash}> _ " [90, 90] 90) |
18 quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and |
|
19 REL ("\<approx>") |
15 |
20 |
16 |
21 |
17 (*>*) |
22 (*>*) |
18 |
23 |
19 section {* Introduction *} |
24 section {* Introduction *} |
20 |
25 |
21 text {* |
26 text {* |
|
27 |
|
28 Therefore instead of defining a regular language as being one where there exists an |
|
29 automata that regognises all of its strings, we define |
|
30 |
|
31 \begin{definition}[A Regular Language] |
|
32 A language @{text A} is regular, if there is a regular expression that matches all |
|
33 strings of @{text "A"}. |
|
34 \end{definition} |
|
35 |
|
36 \noindent |
|
37 {\bf Contributions:} A proof of the Myhil-Nerode Theorem based on regular expressions. The |
|
38 finiteness part of this theorem is proved using tagging-functions (which to our knowledge |
|
39 are novel in this context). |
22 |
40 |
23 *} |
41 *} |
24 |
42 |
25 section {* Preliminaries *} |
43 section {* Preliminaries *} |
26 |
44 |
27 text {* |
45 text {* |
|
46 Strings in Isabelle/HOL are lists of characters. Therefore the |
|
47 \emph{empty string} is represented by the empty list, written @{term "[]"}. \emph{Languages} are sets of |
|
48 strings. The language containing all strings is abbreviated as @{term "UNIV::string set"} |
|
49 and the notation for the quotient of a language @{text A} according to a relation @{term REL} is |
|
50 @{term "A // REL"}. |
|
51 |
|
52 Set operations |
|
53 |
|
54 \begin{center} |
|
55 @{thm Seq_def} |
|
56 \end{center} |
|
57 |
|
58 \noindent |
|
59 where @{text "@"} is the usual list-append operation. |
|
60 |
|
61 \noindent |
|
62 Regular expressions are defined as the following datatype |
|
63 |
|
64 \begin{center} |
|
65 @{text r} @{text "::="} |
|
66 @{term NULL}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} |
|
67 @{term EMPTY}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} |
|
68 @{term "CHAR c"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} |
|
69 @{term "SEQ r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} |
|
70 @{term "ALT r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} |
|
71 @{term "STAR r"} |
|
72 \end{center} |
|
73 |
28 Central to our proof will be the solution of equational systems |
74 Central to our proof will be the solution of equational systems |
29 involving regular expressions. For this we will use the following ``reverse'' |
75 involving regular expressions. For this we will use the following ``reverse'' |
30 version of Arden's lemma. |
76 version of Arden's lemma. |
31 |
77 |
32 \begin{lemma}[Reverse Arden's Lemma]\mbox{}\\ |
78 \begin{lemma}[Reverse Arden's Lemma]\mbox{}\\ |
61 implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Lemma ??? this |
107 implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Lemma ??? this |
62 is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed |
108 is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed |
63 \end{proof} |
109 \end{proof} |
64 *} |
110 *} |
65 |
111 |
66 section {* Regular expressions have finitely many partitions *} |
112 section {* Finite Partitions Imply Regularity of a Language *} |
|
113 |
|
114 text {* |
|
115 \begin{theorem} |
|
116 Given a language @{text A}. |
|
117 @{thm[mode=IfThen] hard_direction[where Lang="A"]} |
|
118 \end{theorem} |
|
119 *} |
|
120 |
|
121 section {* Regular Expressions Generate Finitely Many Partitions *} |
67 |
122 |
68 text {* |
123 text {* |
69 |
124 |
70 \begin{lemma} |
125 \begin{theorem} |
71 Given @{text "r"} is a regular expressions, then @{thm rexp_imp_finite}. |
126 Given @{text "r"} is a regular expressions, then @{thm rexp_imp_finite}. |
72 \end{lemma} |
127 \end{theorem} |
73 |
128 |
74 \begin{proof} |
129 \begin{proof} |
75 By induction on the structure of @{text r}. The cases for @{const NULL}, @{const EMPTY} |
130 By induction on the structure of @{text r}. The cases for @{const NULL}, @{const EMPTY} |
76 and @{const CHAR} are straightforward, because we can easily establish |
131 and @{const CHAR} are straightforward, because we can easily establish |
77 |
132 |