24
+ − 1 (*<*)
+ − 2 theory Paper
94
+ − 3 imports "../Myhill" "LaTeXsugar"
24
+ − 4 begin
39
+ − 5
+ − 6 declare [[show_question_marks = false]]
+ − 7
54
+ − 8 consts
+ − 9 REL :: "(string \<times> string) \<Rightarrow> bool"
66
+ − 10 UPLUS :: "'a set \<Rightarrow> 'a set \<Rightarrow> (nat \<times> 'a) set"
54
+ − 11
70
+ − 12 abbreviation
+ − 13 "EClass x R \<equiv> R `` {x}"
54
+ − 14
92
+ − 15 abbreviation
+ − 16 "append_rexp2 r_itm r \<equiv> append_rexp r r_itm"
+ − 17
+ − 18
39
+ − 19 notation (latex output)
50
+ − 20 str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and
75
+ − 21 str_eq ("_ \<approx>\<^bsub>_\<^esub> _") and
50
+ − 22 Seq (infixr "\<cdot>" 100) and
+ − 23 Star ("_\<^bsup>\<star>\<^esup>") and
+ − 24 pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and
58
+ − 25 Suc ("_+1" [100] 100) and
54
+ − 26 quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and
66
+ − 27 REL ("\<approx>") and
67
+ − 28 UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90) and
82
+ − 29 L ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and
75
+ − 30 Lam ("\<lambda>'(_')" [100] 100) and
89
+ − 31 Trn ("'(_, _')" [100, 100] 100) and
71
+ − 32 EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and
88
+ − 33 transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and
92
+ − 34 Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and
+ − 35 append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and
112
+ − 36 append_rhs_rexp ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
119
+ − 37 uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and
+ − 38 tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _" [100, 100] 100) and
121
+ − 39 tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [100, 100, 100] 100) and
+ − 40 tag_str_SEQ ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and
+ − 41 tag_str_SEQ ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and
+ − 42 tag_str_STAR ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _" [100] 100) and
+ − 43 tag_str_STAR ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100)
119
+ − 44 lemma meta_eq_app:
+ − 45 shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
+ − 46 by auto
+ − 47
24
+ − 48 (*>*)
+ − 49
70
+ − 50
24
+ − 51 section {* Introduction *}
+ − 52
+ − 53 text {*
58
+ − 54 Regular languages are an important and well-understood subject in Computer
60
+ − 55 Science, with many beautiful theorems and many useful algorithms. There is a
66
+ − 56 wide range of textbooks on this subject, many of which are aimed at students
115
+ − 57 and contain very detailed `pencil-and-paper' proofs
60
+ − 58 (e.g.~\cite{Kozen97}). It seems natural to exercise theorem provers by
101
+ − 59 formalising the theorems and by verifying formally the algorithms.
59
+ − 60
66
+ − 61 There is however a problem: the typical approach to regular languages is to
+ − 62 introduce finite automata and then define everything in terms of them. For
+ − 63 example, a regular language is normally defined as one whose strings are
+ − 64 recognised by a finite deterministic automaton. This approach has many
71
+ − 65 benefits. Among them is the fact that it is easy to convince oneself that
66
+ − 66 regular languages are closed under complementation: one just has to exchange
+ − 67 the accepting and non-accepting states in the corresponding automaton to
+ − 68 obtain an automaton for the complement language. The problem, however, lies with
67
+ − 69 formalising such reasoning in a HOL-based theorem prover, in our case
115
+ − 70 Isabelle/HOL. Automata are built up from states and transitions that
82
+ − 71 need to be represented as graphs, matrices or functions, none
+ − 72 of which can be defined as inductive datatype.
66
+ − 73
82
+ − 74 In case of graphs and matrices, this means we have to build our own
+ − 75 reasoning infrastructure for them, as neither Isabelle/HOL nor HOL4 nor
+ − 76 HOLlight support them with libraries. Even worse, reasoning about graphs and
+ − 77 matrices can be a real hassle in HOL-based theorem provers. Consider for
+ − 78 example the operation of sequencing two automata, say $A_1$ and $A_2$, by
+ − 79 connecting the accepting states of $A_1$ to the initial state of $A_2$:
60
+ − 80
+ − 81 \begin{center}
66
+ − 82 \begin{tabular}{ccc}
+ − 83 \begin{tikzpicture}[scale=0.8]
+ − 84 %\draw[step=2mm] (-1,-1) grid (1,1);
+ − 85
+ − 86 \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
+ − 87 \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);
+ − 88
+ − 89 \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 90 \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 91
+ − 92 \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 93 \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 94
+ − 95 \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 96 \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 97 \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 98
+ − 99 \draw (-0.6,0.0) node {\footnotesize$A_1$};
+ − 100 \draw ( 0.6,0.0) node {\footnotesize$A_2$};
+ − 101 \end{tikzpicture}
+ − 102
+ − 103 &
+ − 104
+ − 105 \raisebox{1.1mm}{\bf\Large$\;\;\;\Rightarrow\,\;\;$}
+ − 106
+ − 107 &
+ − 108
+ − 109 \begin{tikzpicture}[scale=0.8]
+ − 110 %\draw[step=2mm] (-1,-1) grid (1,1);
+ − 111
+ − 112 \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
+ − 113 \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);
+ − 114
+ − 115 \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 116 \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 117
+ − 118 \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 119 \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 120
+ − 121 \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 122 \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 123 \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ − 124
+ − 125 \draw (C) to [very thick, bend left=45] (B);
+ − 126 \draw (D) to [very thick, bend right=45] (B);
+ − 127
+ − 128 \draw (-0.6,0.0) node {\footnotesize$A_1$};
+ − 129 \draw ( 0.6,0.0) node {\footnotesize$A_2$};
+ − 130 \end{tikzpicture}
+ − 131
+ − 132 \end{tabular}
60
+ − 133 \end{center}
+ − 134
+ − 135 \noindent
115
+ − 136 On `paper' we can define the corresponding graph in terms of the disjoint
88
+ − 137 union of the state nodes. Unfortunately in HOL, the standard definition for disjoint
66
+ − 138 union, namely
82
+ − 139 %
+ − 140 \begin{equation}\label{disjointunion}
66
+ − 141 @{term "UPLUS A\<^isub>1 A\<^isub>2 \<equiv> {(1, x) | x. x \<in> A\<^isub>1} \<union> {(2, y) | y. y \<in> A\<^isub>2}"}
82
+ − 142 \end{equation}
60
+ − 143
61
+ − 144 \noindent
66
+ − 145 changes the type---the disjoint union is not a set, but a set of pairs.
+ − 146 Using this definition for disjoint unions means we do not have a single type for automata
92
+ − 147 and hence will not be able to state certain properties about \emph{all}
67
+ − 148 automata, since there is no type quantification available in HOL. An
+ − 149 alternative, which provides us with a single type for automata, is to give every
+ − 150 state node an identity, for example a natural
70
+ − 151 number, and then be careful to rename these identities apart whenever
67
+ − 152 connecting two automata. This results in clunky proofs
66
+ − 153 establishing that properties are invariant under renaming. Similarly,
67
+ − 154 connecting two automata represented as matrices results in very adhoc
66
+ − 155 constructions, which are not pleasant to reason about.
+ − 156
82
+ − 157 Functions are much better supported in Isabelle/HOL, but they still lead to similar
88
+ − 158 problems as with graphs. Composing, for example, two non-deterministic automata in parallel
93
+ − 159 requires also the formalisation of disjoint unions. Nipkow \cite{Nipkow98}
101
+ − 160 dismisses for this the option of using identities, because it leads according to
+ − 161 him to ``messy proofs''. He
103
+ − 162 opts for a variant of \eqref{disjointunion} using bit lists, but writes
82
+ − 163
+ − 164 \begin{quote}
93
+ − 165 \it%
+ − 166 \begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}}
101
+ − 167 `` & All lemmas appear obvious given a picture of the composition of automata\ldots
+ − 168 Yet their proofs require a painful amount of detail.''
+ − 169 \end{tabular}
+ − 170 \end{quote}
+ − 171
+ − 172 \noindent
+ − 173 and
+ − 174
+ − 175 \begin{quote}
+ − 176 \it%
+ − 177 \begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}}
93
+ − 178 `` & If the reader finds the above treatment in terms of bit lists revoltingly
101
+ − 179 concrete, I cannot disagree. A more abstract approach is clearly desirable.''
93
+ − 180 \end{tabular}
82
+ − 181 \end{quote}
101
+ − 182
+ − 183
82
+ − 184 \noindent
+ − 185 Moreover, it is not so clear how to conveniently impose a finiteness condition
+ − 186 upon functions in order to represent \emph{finite} automata. The best is
92
+ − 187 probably to resort to more advanced reasoning frameworks, such as \emph{locales}
+ − 188 or \emph{type classes},
110
+ − 189 which are \emph{not} avaiable in all HOL-based theorem provers.
82
+ − 190
66
+ − 191 Because of these problems to do with representing automata, there seems
+ − 192 to be no substantial formalisation of automata theory and regular languages
115
+ − 193 carried out in HOL-based theorem provers. Nipkow \cite{Nipkow98} establishes
+ − 194 the link between regular expressions and automata in
+ − 195 the context of lexing. Berghofer and Reiter \cite{BerghoferReiter09}
+ − 196 formalise automata working over
+ − 197 bit strings in the context of Presburger arithmetic.
114
+ − 198 The only larger formalisations of automata theory
115
+ − 199 are carried out in Nuprl \cite{Constable00} and in Coq \cite{Filliatre97}.
58
+ − 200
82
+ − 201 In this paper, we will not attempt to formalise automata theory in
+ − 202 Isabelle/HOL, but take a completely different approach to regular
+ − 203 languages. Instead of defining a regular language as one where there exists
+ − 204 an automaton that recognises all strings of the language, we define a
+ − 205 regular language as:
54
+ − 206
82
+ − 207 \begin{definition}
77
+ − 208 A language @{text A} is \emph{regular}, provided there is a regular expression that matches all
54
+ − 209 strings of @{text "A"}.
+ − 210 \end{definition}
+ − 211
+ − 212 \noindent
110
+ − 213 The reason is that regular expressions, unlike graphs, matrices and functions, can
71
+ − 214 be easily defined as inductive datatype. Consequently a corresponding reasoning
+ − 215 infrastructure comes for free. This has recently been exploited in HOL4 with a formalisation
101
+ − 216 of regular expression matching based on derivatives \cite{OwensSlind08} and
+ − 217 with an equivalence checker for regular expressions in Isabelle/HOL \cite{KraussNipkow11}.
+ − 218 The purpose of this paper is to
71
+ − 219 show that a central result about regular languages---the Myhill-Nerode theorem---can
+ − 220 be recreated by only using regular expressions. This theorem gives necessary
+ − 221 and sufficient conditions for when a language is regular. As a corollary of this
67
+ − 222 theorem we can easily establish the usual closure properties, including
+ − 223 complementation, for regular languages.\smallskip
61
+ − 224
+ − 225 \noindent
88
+ − 226 {\bf Contributions:}
+ − 227 There is an extensive literature on regular languages.
+ − 228 To our knowledge, our proof of the Myhill-Nerode theorem is the
67
+ − 229 first that is based on regular expressions, only. We prove the part of this theorem
+ − 230 stating that a regular expression has only finitely many partitions using certain
+ − 231 tagging-functions. Again to our best knowledge, these tagging functions have
+ − 232 not been used before to establish the Myhill-Nerode theorem.
24
+ − 233 *}
+ − 234
50
+ − 235 section {* Preliminaries *}
+ − 236
+ − 237 text {*
67
+ − 238 Strings in Isabelle/HOL are lists of characters with the \emph{empty string}
92
+ − 239 being represented by the empty list, written @{term "[]"}. \emph{Languages}
67
+ − 240 are sets of strings. The language containing all strings is written in
71
+ − 241 Isabelle/HOL as @{term "UNIV::string set"}. The concatenation of two languages
90
+ − 242 is written @{term "A ;; B"} and a language raised to the power @{text n} is written
93
+ − 243 @{term "A \<up> n"}. They are defined as usual
54
+ − 244
+ − 245 \begin{center}
58
+ − 246 @{thm Seq_def[THEN eq_reflection, where A1="A" and B1="B"]}
+ − 247 \hspace{7mm}
+ − 248 @{thm pow.simps(1)[THEN eq_reflection, where A1="A"]}
+ − 249 \hspace{7mm}
+ − 250 @{thm pow.simps(2)[THEN eq_reflection, where A1="A" and n1="n"]}
54
+ − 251 \end{center}
+ − 252
+ − 253 \noindent
113
+ − 254 where @{text "@"} is the list-append operation. The Kleene-star of a language @{text A}
71
+ − 255 is defined as the union over all powers, namely @{thm Star_def}. In the paper
88
+ − 256 we will make use of the following properties of these constructions.
58
+ − 257
71
+ − 258 \begin{proposition}\label{langprops}\mbox{}\\
92
+ − 259 \begin{tabular}{@ {}ll}
+ − 260 (i) & @{thm star_cases} \\
+ − 261 (ii) & @{thm[mode=IfThen] pow_length}\\
+ − 262 (iii) & @{thm seq_Union_left} \\
71
+ − 263 \end{tabular}
+ − 264 \end{proposition}
+ − 265
+ − 266 \noindent
100
+ − 267 In @{text "(ii)"} we use the notation @{term "length s"} for the length of a
113
+ − 268 string; this property states that if @{term "[] \<notin> A"} then the lengths of
100
+ − 269 the strings in @{term "A \<up> (Suc n)"} must be longer than @{text n}. We omit
+ − 270 the proofs for these properties, but invite the reader to consult our
121
+ − 271 formalisation.\footnote{Available at \url{http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/regexp/}}
71
+ − 272
90
+ − 273 The notation in Isabelle/HOL for the quotient of a language @{text A} according to an
+ − 274 equivalence relation @{term REL} is @{term "A // REL"}. We will write
71
+ − 275 @{text "\<lbrakk>x\<rbrakk>\<^isub>\<approx>"} for the equivalence class defined
+ − 276 as @{text "{y | y \<approx> x}"}.
+ − 277
+ − 278
51
+ − 279 Central to our proof will be the solution of equational systems
115
+ − 280 involving equivalence classes of languages. For this we will use Arden's lemma \cite{Brzozowski64},
93
+ − 281 which solves equations of the form @{term "X = A ;; X \<union> B"} provided
115
+ − 282 @{term "[] \<notin> A"}. However we will need the following `reverse'
116
+ − 283 version of Arden's lemma (`reverse' in the sense of changing the order of @{text "\<cdot>"}).
50
+ − 284
75
+ − 285 \begin{lemma}[Reverse Arden's Lemma]\label{arden}\mbox{}\\
86
+ − 286 If @{thm (prem 1) arden} then
115
+ − 287 @{thm (lhs) arden} if and only if
86
+ − 288 @{thm (rhs) arden}.
50
+ − 289 \end{lemma}
+ − 290
+ − 291 \begin{proof}
86
+ − 292 For the right-to-left direction we assume @{thm (rhs) arden} and show
+ − 293 that @{thm (lhs) arden} holds. From Prop.~\ref{langprops}@{text "(i)"}
71
+ − 294 we have @{term "A\<star> = {[]} \<union> A ;; A\<star>"},
50
+ − 295 which is equal to @{term "A\<star> = {[]} \<union> A\<star> ;; A"}. Adding @{text B} to both
+ − 296 sides gives @{term "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"}, whose right-hand side
51
+ − 297 is equal to @{term "(B ;; A\<star>) ;; A \<union> B"}. This completes this direction.
50
+ − 298
86
+ − 299 For the other direction we assume @{thm (lhs) arden}. By a simple induction
51
+ − 300 on @{text n}, we can establish the property
50
+ − 301
+ − 302 \begin{center}
86
+ − 303 @{text "(*)"}\hspace{5mm} @{thm (concl) arden_helper}
50
+ − 304 \end{center}
+ − 305
+ − 306 \noindent
+ − 307 Using this property we can show that @{term "B ;; (A \<up> n) \<subseteq> X"} holds for
71
+ − 308 all @{text n}. From this we can infer @{term "B ;; A\<star> \<subseteq> X"} using the definition
+ − 309 of @{text "\<star>"}.
51
+ − 310 For the inclusion in the other direction we assume a string @{text s}
86
+ − 311 with length @{text k} is element in @{text X}. Since @{thm (prem 1) arden}
75
+ − 312 we know by Prop.~\ref{langprops}@{text "(ii)"} that
71
+ − 313 @{term "s \<notin> X ;; (A \<up> Suc k)"} since its length is only @{text k}
51
+ − 314 (the strings in @{term "X ;; (A \<up> Suc k)"} are all longer).
53
+ − 315 From @{text "(*)"} it follows then that
50
+ − 316 @{term s} must be element in @{term "(\<Union>m\<in>{0..k}. B ;; (A \<up> m))"}. This in turn
75
+ − 317 implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Prop.~\ref{langprops}@{text "(iii)"}
71
+ − 318 this is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed
50
+ − 319 \end{proof}
67
+ − 320
+ − 321 \noindent
88
+ − 322 Regular expressions are defined as the inductive datatype
67
+ − 323
+ − 324 \begin{center}
+ − 325 @{text r} @{text "::="}
+ − 326 @{term NULL}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
+ − 327 @{term EMPTY}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
+ − 328 @{term "CHAR c"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
+ − 329 @{term "SEQ r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
+ − 330 @{term "ALT r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
+ − 331 @{term "STAR r"}
+ − 332 \end{center}
+ − 333
+ − 334 \noindent
88
+ − 335 and the language matched by a regular expression is defined as
67
+ − 336
+ − 337 \begin{center}
+ − 338 \begin{tabular}{c@ {\hspace{10mm}}c}
+ − 339 \begin{tabular}{rcl}
+ − 340 @{thm (lhs) L_rexp.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(1)}\\
+ − 341 @{thm (lhs) L_rexp.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(2)}\\
+ − 342 @{thm (lhs) L_rexp.simps(3)[where c="c"]} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(3)[where c="c"]}\\
+ − 343 \end{tabular}
+ − 344 &
+ − 345 \begin{tabular}{rcl}
+ − 346 @{thm (lhs) L_rexp.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &
+ − 347 @{thm (rhs) L_rexp.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ − 348 @{thm (lhs) L_rexp.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &
+ − 349 @{thm (rhs) L_rexp.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ − 350 @{thm (lhs) L_rexp.simps(6)[where r="r"]} & @{text "\<equiv>"} &
+ − 351 @{thm (rhs) L_rexp.simps(6)[where r="r"]}\\
+ − 352 \end{tabular}
+ − 353 \end{tabular}
+ − 354 \end{center}
70
+ − 355
100
+ − 356 Given a finite set of regular expressions @{text rs}, we will make use of the operation of generating
92
+ − 357 a regular expression that matches all languages of @{text rs}. We only need to know the existence
+ − 358 of such a regular expression and therefore we use Isabelle/HOL's @{const "fold_graph"} and Hilbert's
93
+ − 359 @{text "\<epsilon>"} to define @{term "\<Uplus>rs"}. This operation, roughly speaking, folds @{const ALT} over the
100
+ − 360 set @{text rs} with @{const NULL} for the empty set. We can prove that for a finite set @{text rs}
110
+ − 361 %
+ − 362 \begin{equation}\label{uplus}
+ − 363 \mbox{@{thm (lhs) folds_alt_simp} @{text "= \<Union> (\<calL> ` rs)"}}
+ − 364 \end{equation}
88
+ − 365
+ − 366 \noindent
90
+ − 367 holds, whereby @{text "\<calL> ` rs"} stands for the
+ − 368 image of the set @{text rs} under function @{text "\<calL>"}.
50
+ − 369 *}
39
+ − 370
100
+ − 371 section {* The Myhill-Nerode Theorem, First Part *}
54
+ − 372
+ − 373 text {*
77
+ − 374 The key definition in the Myhill-Nerode theorem is the
75
+ − 375 \emph{Myhill-Nerode relation}, which states that w.r.t.~a language two
+ − 376 strings are related, provided there is no distinguishing extension in this
117
+ − 377 language. This can be defined as tertiary relation.
75
+ − 378
117
+ − 379 \begin{definition}[Myhill-Nerode Relation] Given a language @{text A}, two strings @{text x} and
+ − 380 @{text y} are related provided
+ − 381 \begin{center}
75
+ − 382 @{thm str_eq_def[simplified str_eq_rel_def Pair_Collect]}
117
+ − 383 \end{center}
70
+ − 384 \end{definition}
+ − 385
71
+ − 386 \noindent
75
+ − 387 It is easy to see that @{term "\<approx>A"} is an equivalence relation, which
+ − 388 partitions the set of all strings, @{text "UNIV"}, into a set of disjoint
108
+ − 389 equivalence classes. To illustrate this quotient construction, let us give a simple
101
+ − 390 example: consider the regular language containing just
92
+ − 391 the string @{text "[c]"}. The relation @{term "\<approx>({[c]})"} partitions @{text UNIV}
101
+ − 392 into three equivalence classes @{text "X\<^isub>1"}, @{text "X\<^isub>2"} and @{text "X\<^isub>3"}
90
+ − 393 as follows
+ − 394
+ − 395 \begin{center}
+ − 396 @{text "X\<^isub>1 = {[]}"}\hspace{5mm}
+ − 397 @{text "X\<^isub>2 = {[c]}"}\hspace{5mm}
+ − 398 @{text "X\<^isub>3 = UNIV - {[], [c]}"}
+ − 399 \end{center}
+ − 400
+ − 401 One direction of the Myhill-Nerode theorem establishes
93
+ − 402 that if there are finitely many equivalence classes, like in the example above, then
+ − 403 the language is regular. In our setting we therefore have to show:
75
+ − 404
+ − 405 \begin{theorem}\label{myhillnerodeone}
96
+ − 406 @{thm[mode=IfThen] Myhill_Nerode1}
75
+ − 407 \end{theorem}
71
+ − 408
75
+ − 409 \noindent
90
+ − 410 To prove this theorem, we first define the set @{term "finals A"} as those equivalence
100
+ − 411 classes from @{term "UNIV // \<approx>A"} that contain strings of @{text A}, namely
75
+ − 412 %
71
+ − 413 \begin{equation}
70
+ − 414 @{thm finals_def}
71
+ − 415 \end{equation}
+ − 416
+ − 417 \noindent
92
+ − 418 In our running example, @{text "X\<^isub>2"} is the only equivalence class in @{term "finals {[c]}"}.
90
+ − 419 It is straightforward to show that in general @{thm lang_is_union_of_finals} and
79
+ − 420 @{thm finals_in_partitions} hold.
75
+ − 421 Therefore if we know that there exists a regular expression for every
100
+ − 422 equivalence class in \mbox{@{term "finals A"}} (which by assumption must be
93
+ − 423 a finite set), then we can use @{text "\<bigplus>"} to obtain a regular expression
98
+ − 424 that matches every string in @{text A}.
70
+ − 425
75
+ − 426
90
+ − 427 Our proof of Thm.~\ref{myhillnerodeone} relies on a method that can calculate a
79
+ − 428 regular expression for \emph{every} equivalence class, not just the ones
77
+ − 429 in @{term "finals A"}. We
93
+ − 430 first define the notion of \emph{one-character-transition} between
+ − 431 two equivalence classes
75
+ − 432 %
71
+ − 433 \begin{equation}
+ − 434 @{thm transition_def}
+ − 435 \end{equation}
70
+ − 436
71
+ − 437 \noindent
92
+ − 438 which means that if we concatenate the character @{text c} to the end of all
+ − 439 strings in the equivalence class @{text Y}, we obtain a subset of
77
+ − 440 @{text X}. Note that we do not define an automaton here, we merely relate two sets
110
+ − 441 (with the help of a character). In our concrete example we have
92
+ − 442 @{term "X\<^isub>1 \<Turnstile>c\<Rightarrow> X\<^isub>2"}, @{term "X\<^isub>1 \<Turnstile>d\<Rightarrow> X\<^isub>3"} with @{text d} being any
93
+ − 443 other character than @{text c}, and @{term "X\<^isub>3 \<Turnstile>d\<Rightarrow> X\<^isub>3"} for any @{text d}.
75
+ − 444
110
+ − 445 Next we build an \emph{initial equational system} that
75
+ − 446 contains an equation for each equivalence class. Suppose we have
+ − 447 the equivalence classes @{text "X\<^isub>1,\<dots>,X\<^isub>n"}, there must be one and only one that
+ − 448 contains the empty string @{text "[]"} (since equivalence classes are disjoint).
77
+ − 449 Let us assume @{text "[] \<in> X\<^isub>1"}. We build the following equational system
75
+ − 450
+ − 451 \begin{center}
+ − 452 \begin{tabular}{rcl}
+ − 453 @{text "X\<^isub>1"} & @{text "="} & @{text "(Y\<^isub>1\<^isub>1, CHAR c\<^isub>1\<^isub>1) + \<dots> + (Y\<^isub>1\<^isub>p, CHAR c\<^isub>1\<^isub>p) + \<lambda>(EMPTY)"} \\
+ − 454 @{text "X\<^isub>2"} & @{text "="} & @{text "(Y\<^isub>2\<^isub>1, CHAR c\<^isub>2\<^isub>1) + \<dots> + (Y\<^isub>2\<^isub>o, CHAR c\<^isub>2\<^isub>o)"} \\
+ − 455 & $\vdots$ \\
+ − 456 @{text "X\<^isub>n"} & @{text "="} & @{text "(Y\<^isub>n\<^isub>1, CHAR c\<^isub>n\<^isub>1) + \<dots> + (Y\<^isub>n\<^isub>q, CHAR c\<^isub>n\<^isub>q)"}\\
+ − 457 \end{tabular}
+ − 458 \end{center}
70
+ − 459
75
+ − 460 \noindent
100
+ − 461 where the terms @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"}
+ − 462 stand for all transitions @{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow>
+ − 463 X\<^isub>i"}. There can only be
110
+ − 464 finitely many such terms in a right-hand side since by assumption there are only finitely many
100
+ − 465 equivalence classes and only finitely many characters. The term @{text
+ − 466 "\<lambda>(EMPTY)"} in the first equation acts as a marker for the equivalence class
+ − 467 containing @{text "[]"}.\footnote{Note that we mark, roughly speaking, the
115
+ − 468 single `initial' state in the equational system, which is different from
100
+ − 469 the method by Brzozowski \cite{Brzozowski64}, where he marks the
115
+ − 470 `terminal' states. We are forced to set up the equational system in our
+ − 471 way, because the Myhill-Nerode relation determines the `direction' of the
+ − 472 transitions. The successor `state' of an equivalence class @{text Y} can
100
+ − 473 be reached by adding characters to the end of @{text Y}. This is also the
+ − 474 reason why we have to use our reverse version of Arden's lemma.}
+ − 475 Overloading the function @{text \<calL>} for the two kinds of terms in the
92
+ − 476 equational system, we have
75
+ − 477
+ − 478 \begin{center}
92
+ − 479 @{text "\<calL>(Y, r) \<equiv>"} %
+ − 480 @{thm (rhs) L_rhs_item.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
86
+ − 481 @{thm L_rhs_item.simps(1)[where r="r", THEN eq_reflection]}
75
+ − 482 \end{center}
+ − 483
+ − 484 \noindent
100
+ − 485 and we can prove for @{text "X\<^isub>2\<^isub>.\<^isub>.\<^isub>n"} that the following equations
75
+ − 486 %
+ − 487 \begin{equation}\label{inv1}
83
+ − 488 @{text "X\<^isub>i = \<calL>(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>i\<^isub>q, CHAR c\<^isub>i\<^isub>q)"}.
75
+ − 489 \end{equation}
+ − 490
+ − 491 \noindent
+ − 492 hold. Similarly for @{text "X\<^isub>1"} we can show the following equation
+ − 493 %
+ − 494 \begin{equation}\label{inv2}
83
+ − 495 @{text "X\<^isub>1 = \<calL>(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>i\<^isub>p, CHAR c\<^isub>i\<^isub>p) \<union> \<calL>(\<lambda>(EMPTY))"}.
75
+ − 496 \end{equation}
+ − 497
+ − 498 \noindent
101
+ − 499 The reason for adding the @{text \<lambda>}-marker to our initial equational system is
103
+ − 500 to obtain this equation: it only holds with the marker, since none of
108
+ − 501 the other terms contain the empty string. The point of the initial equational system is
+ − 502 that solving it means we will be able to extract a regular expression for every equivalence class.
100
+ − 503
101
+ − 504 Our representation for the equations in Isabelle/HOL are pairs,
108
+ − 505 where the first component is an equivalence class (a set of strings)
+ − 506 and the second component
101
+ − 507 is a set of terms. Given a set of equivalence
100
+ − 508 classes @{text CS}, our initial equational system @{term "Init CS"} is thus
101
+ − 509 formally defined as
104
+ − 510 %
+ − 511 \begin{equation}\label{initcs}
+ − 512 \mbox{\begin{tabular}{rcl}
100
+ − 513 @{thm (lhs) Init_rhs_def} & @{text "\<equiv>"} &
+ − 514 @{text "if"}~@{term "[] \<in> X"}\\
+ − 515 & & @{text "then"}~@{term "{Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X} \<union> {Lam EMPTY}"}\\
+ − 516 & & @{text "else"}~@{term "{Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}"}\\
+ − 517 @{thm (lhs) Init_def} & @{text "\<equiv>"} & @{thm (rhs) Init_def}
104
+ − 518 \end{tabular}}
+ − 519 \end{equation}
100
+ − 520
+ − 521
+ − 522
+ − 523 \noindent
+ − 524 Because we use sets of terms
101
+ − 525 for representing the right-hand sides of equations, we can
100
+ − 526 prove \eqref{inv1} and \eqref{inv2} more concisely as
93
+ − 527 %
100
+ − 528 \begin{lemma}\label{inv}
+ − 529 If @{thm (prem 1) test} then @{text "X = \<Union> \<calL> ` rhs"}.
+ − 530 \end{lemma}
77
+ − 531
93
+ − 532 \noindent
92
+ − 533 Our proof of Thm.~\ref{myhillnerodeone} will proceed by transforming the
100
+ − 534 initial equational system into one in \emph{solved form} maintaining the invariant
108
+ − 535 in Lem.~\ref{inv}. From the solved form we will be able to read
89
+ − 536 off the regular expressions.
+ − 537
100
+ − 538 In order to transform an equational system into solved form, we have two
89
+ − 539 operations: one that takes an equation of the form @{text "X = rhs"} and removes
110
+ − 540 any recursive occurrences of @{text X} in the @{text rhs} using our variant of Arden's
92
+ − 541 Lemma. The other operation takes an equation @{text "X = rhs"}
89
+ − 542 and substitutes @{text X} throughout the rest of the equational system
110
+ − 543 adjusting the remaining regular expressions appropriately. To define this adjustment
108
+ − 544 we define the \emph{append-operation} taking a term and a regular expression as argument
89
+ − 545
+ − 546 \begin{center}
92
+ − 547 @{thm append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\hspace{10mm}
+ − 548 @{thm append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
89
+ − 549 \end{center}
+ − 550
92
+ − 551 \noindent
108
+ − 552 We lift this operation to entire right-hand sides of equations, written as
93
+ − 553 @{thm (lhs) append_rhs_rexp_def[where rexp="r"]}. With this we can define
101
+ − 554 the \emph{arden-operation} for an equation of the form @{text "X = rhs"} as:
110
+ − 555 %
+ − 556 \begin{equation}\label{arden_def}
+ − 557 \mbox{\begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
94
+ − 558 @{thm (lhs) Arden_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\
+ − 559 & & @{text "rhs' ="} & @{term "rhs - {Trn X r | r. Trn X r \<in> rhs}"} \\
+ − 560 & & @{text "r' ="} & @{term "STAR (\<Uplus> {r. Trn X r \<in> rhs})"}\\
+ − 561 & & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "append_rhs_rexp rhs' r'"}}\\
110
+ − 562 \end{tabular}}
+ − 563 \end{equation}
93
+ − 564
+ − 565 \noindent
101
+ − 566 In this definition, we first delete all terms of the form @{text "(X, r)"} from @{text rhs};
110
+ − 567 then we calculate the combined regular expressions for all @{text r} coming
94
+ − 568 from the deleted @{text "(X, r)"}, and take the @{const STAR} of it;
+ − 569 finally we append this regular expression to @{text rhs'}. It can be easily seen
110
+ − 570 that this operation mimics Arden's lemma on the level of equations. To ensure
+ − 571 the non-emptiness condition of Arden's lemma we say that a right-hand side is
+ − 572 \emph{ardenable} provided
+ − 573
+ − 574 \begin{center}
+ − 575 @{thm ardenable_def}
+ − 576 \end{center}
+ − 577
+ − 578 \noindent
+ − 579 This allows us to prove
+ − 580
+ − 581 \begin{lemma}\label{ardenable}
113
+ − 582 Given an equation @{text "X = rhs"}.
110
+ − 583 If @{text "X = \<Union>\<calL> ` rhs"},
115
+ − 584 @{thm (prem 2) Arden_keeps_eq}, and
110
+ − 585 @{thm (prem 3) Arden_keeps_eq}, then
+ − 586 @{text "X = \<Union>\<calL> ` (Arden X rhs)"}
+ − 587 \end{lemma}
+ − 588
+ − 589 \noindent
95
+ − 590 The \emph{substituion-operation} takes an equation
+ − 591 of the form @{text "X = xrhs"} and substitutes it into the right-hand side @{text rhs}.
94
+ − 592
+ − 593 \begin{center}
95
+ − 594 \begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
+ − 595 @{thm (lhs) Subst_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\
+ − 596 & & @{text "rhs' ="} & @{term "rhs - {Trn X r | r. Trn X r \<in> rhs}"} \\
+ − 597 & & @{text "r' ="} & @{term "\<Uplus> {r. Trn X r \<in> rhs}"}\\
+ − 598 & & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "rhs' \<union> append_rhs_rexp xrhs r'"}}\\
+ − 599 \end{tabular}
94
+ − 600 \end{center}
95
+ − 601
+ − 602 \noindent
110
+ − 603 We again delete first all occurrence of @{text "(X, r)"} in @{text rhs}; we then calculate
95
+ − 604 the regular expression corresponding to the deleted terms; finally we append this
+ − 605 regular expression to @{text "xrhs"} and union it up with @{text rhs'}. When we use
+ − 606 the substitution operation we will arrange it so that @{text "xrhs"} does not contain
110
+ − 607 any occurrence of @{text X}.
96
+ − 608
100
+ − 609 With these two operation in place, we can define the operation that removes one equation
+ − 610 from an equational systems @{text ES}. The operation @{const Subst_all}
96
+ − 611 substitutes an equation @{text "X = xrhs"} throughout an equational system @{text ES};
100
+ − 612 @{const Remove} then completely removes such an equation from @{text ES} by substituting
110
+ − 613 it to the rest of the equational system, but first eliminating all recursive occurrences
96
+ − 614 of @{text X} by applying @{const Arden} to @{text "xrhs"}.
+ − 615
+ − 616 \begin{center}
+ − 617 \begin{tabular}{rcl}
+ − 618 @{thm (lhs) Subst_all_def} & @{text "\<equiv>"} & @{thm (rhs) Subst_all_def}\\
+ − 619 @{thm (lhs) Remove_def} & @{text "\<equiv>"} & @{thm (rhs) Remove_def}
+ − 620 \end{tabular}
+ − 621 \end{center}
100
+ − 622
+ − 623 \noindent
110
+ − 624 Finally, we can define how an equational system should be solved. For this
107
+ − 625 we will need to iterate the process of eliminating equations until only one equation
100
+ − 626 will be left in the system. However, we not just want to have any equation
107
+ − 627 as being the last one, but the one involving the equivalence class for
+ − 628 which we want to calculate the regular
108
+ − 629 expression. Let us suppose this equivalence class is @{text X}.
107
+ − 630 Since @{text X} is the one to be solved, in every iteration step we have to pick an
108
+ − 631 equation to be eliminated that is different from @{text X}. In this way
+ − 632 @{text X} is kept to the final step. The choice is implemented using Hilbert's choice
107
+ − 633 operator, written @{text SOME} in the definition below.
100
+ − 634
+ − 635 \begin{center}
+ − 636 \begin{tabular}{rc@ {\hspace{4mm}}r@ {\hspace{1mm}}l}
+ − 637 @{thm (lhs) Iter_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-4mm}}l}{@{text "let"}}\\
+ − 638 & & @{text "(Y, yrhs) ="} & @{term "SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y"} \\
+ − 639 & & \multicolumn{2}{@ {\hspace{-4mm}}l}{@{text "in"}~~@{term "Remove ES Y yrhs"}}\\
+ − 640 \end{tabular}
+ − 641 \end{center}
+ − 642
+ − 643 \noindent
110
+ − 644 The last definition we need applies @{term Iter} over and over until a condition
+ − 645 @{text Cond} is \emph{not} satisfied anymore. The condition states that there
+ − 646 are more than one equation left in the equational system @{text ES}. To solve
+ − 647 an equational system we use Isabelle/HOL's @{text while}-operator as follows:
101
+ − 648
100
+ − 649 \begin{center}
+ − 650 @{thm Solve_def}
+ − 651 \end{center}
+ − 652
101
+ − 653 \noindent
103
+ − 654 We are not concerned here with the definition of this operator
115
+ − 655 (see Berghofer and Nipkow \cite{BerghoferNipkow00}), but note that we eliminate
103
+ − 656 in each @{const Iter}-step a single equation, and therefore
+ − 657 have a well-founded termination order by taking the cardinality
+ − 658 of the equational system @{text ES}. This enables us to prove
115
+ − 659 properties about our definition of @{const Solve} when we `call' it with
104
+ − 660 the equivalence class @{text X} and the initial equational system
+ − 661 @{term "Init (UNIV // \<approx>A)"} from
108
+ − 662 \eqref{initcs} using the principle:
110
+ − 663 %
+ − 664 \begin{equation}\label{whileprinciple}
+ − 665 \mbox{\begin{tabular}{l}
103
+ − 666 @{term "invariant (Init (UNIV // \<approx>A))"} \\
+ − 667 @{term "\<forall>ES. invariant ES \<and> Cond ES \<longrightarrow> invariant (Iter X ES)"}\\
+ − 668 @{term "\<forall>ES. invariant ES \<and> Cond ES \<longrightarrow> card (Iter X ES) < card ES"}\\
+ − 669 @{term "\<forall>ES. invariant ES \<and> \<not> Cond ES \<longrightarrow> P ES"}\\
+ − 670 \hline
+ − 671 \multicolumn{1}{c}{@{term "P (Solve X (Init (UNIV // \<approx>A)))"}}
110
+ − 672 \end{tabular}}
+ − 673 \end{equation}
103
+ − 674
+ − 675 \noindent
104
+ − 676 This principle states that given an invariant (which we will specify below)
+ − 677 we can prove a property
+ − 678 @{text "P"} involving @{const Solve}. For this we have to discharge the following
+ − 679 proof obligations: first the
113
+ − 680 initial equational system satisfies the invariant; second the iteration
104
+ − 681 step @{text "Iter"} preserves the the invariant as long as the condition @{term Cond} holds;
113
+ − 682 third @{text "Iter"} decreases the termination order, and fourth that
104
+ − 683 once the condition does not hold anymore then the property @{text P} must hold.
103
+ − 684
104
+ − 685 The property @{term P} in our proof will state that @{term "Solve X (Init (UNIV // \<approx>A))"}
108
+ − 686 returns with a single equation @{text "X = xrhs"} for some @{text "xrhs"}, and
104
+ − 687 that this equational system still satisfies the invariant. In order to get
+ − 688 the proof through, the invariant is composed of the following six properties:
103
+ − 689
+ − 690 \begin{center}
104
+ − 691 \begin{tabular}{@ {}rcl@ {\hspace{-13mm}}l @ {}}
+ − 692 @{text "invariant ES"} & @{text "\<equiv>"} &
103
+ − 693 @{term "finite ES"} & @{text "(finiteness)"}\\
+ − 694 & @{text "\<and>"} & @{thm (rhs) finite_rhs_def} & @{text "(finiteness rhs)"}\\
104
+ − 695 & @{text "\<and>"} & @{text "\<forall>(X, rhs)\<in>ES. X = \<Union>\<calL> ` rhs"} & @{text "(soundness)"}\\
+ − 696 & @{text "\<and>"} & @{thm (rhs) distinct_equas_def}\\
+ − 697 & & & @{text "(distinctness)"}\\
110
+ − 698 & @{text "\<and>"} & @{thm (rhs) ardenable_all_def} & @{text "(ardenable)"}\\
104
+ − 699 & @{text "\<and>"} & @{thm (rhs) valid_eqs_def} & @{text "(validity)"}\\
103
+ − 700 \end{tabular}
+ − 701 \end{center}
+ − 702
104
+ − 703 \noindent
+ − 704 The first two ensure that the equational system is always finite (number of equations
115
+ − 705 and number of terms in each equation); the second makes sure the `meaning' of the
108
+ − 706 equations is preserved under our transformations. The other properties are a bit more
+ − 707 technical, but are needed to get our proof through. Distinctness states that every
110
+ − 708 equation in the system is distinct. Ardenable ensures that we can always
+ − 709 apply the arden operation.
108
+ − 710 The last property states that every @{text rhs} can only contain equivalence classes
+ − 711 for which there is an equation. Therefore @{text lhss} is just the set containing
+ − 712 the first components of an equational system,
+ − 713 while @{text "rhss"} collects all equivalence classes @{text X} in the terms of the
110
+ − 714 form @{term "Trn X r"}. That means @{thm (lhs) lhss_def}~@{text "\<equiv> {X | (X, rhs) \<in> ES}"}
+ − 715 and @{thm (lhs) rhss_def}~@{text "\<equiv> {X | (X, r) \<in> rhs}"}.
108
+ − 716
104
+ − 717
110
+ − 718 It is straightforward to prove that the initial equational system satisfies the
105
+ − 719 invariant.
+ − 720
110
+ − 721 \begin{lemma}\label{invzero}
104
+ − 722 @{thm[mode=IfThen] Init_ES_satisfies_invariant}
+ − 723 \end{lemma}
+ − 724
105
+ − 725 \begin{proof}
+ − 726 Finiteness is given by the assumption and the way how we set up the
+ − 727 initial equational system. Soundness is proved in Lem.~\ref{inv}. Distinctness
+ − 728 follows from the fact that the equivalence classes are disjoint. The ardenable
113
+ − 729 property also follows from the setup of the initial equational system, as does
105
+ − 730 validity.\qed
+ − 731 \end{proof}
+ − 732
113
+ − 733 \noindent
+ − 734 Next we show that @{text Iter} preserves the invariant.
+ − 735
110
+ − 736 \begin{lemma}\label{iterone}
104
+ − 737 @{thm[mode=IfThen] iteration_step_invariant[where xrhs="rhs"]}
+ − 738 \end{lemma}
+ − 739
107
+ − 740 \begin{proof}
110
+ − 741 This boils down to choosing an equation @{text "Y = yrhs"} to be eliminated
+ − 742 and to show that @{term "Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)"}
+ − 743 preserves the invariant.
+ − 744 We prove this as follows:
+ − 745
+ − 746 \begin{center}
+ − 747 @{text "\<forall> ES."} @{thm (prem 1) Subst_all_satisfies_invariant} implies
+ − 748 @{thm (concl) Subst_all_satisfies_invariant}
+ − 749 \end{center}
+ − 750
+ − 751 \noindent
+ − 752 Finiteness is straightforward, as @{const Subst} and @{const Arden} operations
116
+ − 753 keep the equational system finite. These operations also preserve soundness
113
+ − 754 and distinctness (we proved soundness for @{const Arden} in Lem.~\ref{ardenable}).
+ − 755 The property ardenable is clearly preserved because the append-operation
110
+ − 756 cannot make a regular expression to match the empty string. Validity is
+ − 757 given because @{const Arden} removes an equivalence class from @{text yrhs}
+ − 758 and then @{const Subst_all} removes @{text Y} from the equational system.
+ − 759 Having proved the implication above, we can replace @{text "ES"} with @{text "ES - {(Y, yrhs)}"}
+ − 760 which matches with our proof-obligation of @{const "Subst_all"}. Since
+ − 761 \mbox{@{term "ES = ES - {(Y, yrhs)} \<union> {(Y, yrhs)}"}}, we can use our assumption
+ − 762 to complete the proof.\qed
107
+ − 763 \end{proof}
+ − 764
113
+ − 765 \noindent
+ − 766 We also need the fact that @{text Iter} decreases the termination measure.
+ − 767
110
+ − 768 \begin{lemma}\label{itertwo}
104
+ − 769 @{thm[mode=IfThen] iteration_step_measure[simplified (no_asm), where xrhs="rhs"]}
+ − 770 \end{lemma}
+ − 771
105
+ − 772 \begin{proof}
+ − 773 By assumption we know that @{text "ES"} is finite and has more than one element.
+ − 774 Therefore there must be an element @{term "(Y, yrhs) \<in> ES"} with
110
+ − 775 @{term "(Y, yrhs) \<noteq> (X, rhs)"}. Using the distinctness property we can infer
105
+ − 776 that @{term "Y \<noteq> X"}. We further know that @{text "Remove ES Y yrhs"}
+ − 777 removes the equation @{text "Y = yrhs"} from the system, and therefore
+ − 778 the cardinality of @{const Iter} strictly decreases.\qed
+ − 779 \end{proof}
+ − 780
113
+ − 781 \noindent
+ − 782 This brings us to our property we want establish for @{text Solve}.
+ − 783
+ − 784
104
+ − 785 \begin{lemma}
+ − 786 If @{thm (prem 1) Solve} and @{thm (prem 2) Solve} then there exists
+ − 787 a @{text rhs} such that @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"}
+ − 788 and @{term "invariant {(X, rhs)}"}.
+ − 789 \end{lemma}
+ − 790
107
+ − 791 \begin{proof}
110
+ − 792 In order to prove this lemma using \eqref{whileprinciple}, we have to use a slightly
+ − 793 stronger invariant since Lem.~\ref{iterone} and \ref{itertwo} have the precondition
+ − 794 that @{term "(X, rhs) \<in> ES"} for some @{text rhs}. This precondition is needed
+ − 795 in order to choose in the @{const Iter}-step an equation that is not \mbox{@{term "X = rhs"}}.
113
+ − 796 Therefore our invariant cannot be just @{term "invariant ES"}, but must be
110
+ − 797 @{term "invariant ES \<and> (\<exists>rhs. (X, rhs) \<in> ES)"}. By assumption
+ − 798 @{thm (prem 2) Solve} and Lem.~\ref{invzero}, the more general invariant holds for
+ − 799 the initial equational system. This is premise 1 of~\eqref{whileprinciple}.
+ − 800 Premise 2 is given by Lem.~\ref{iterone} and the fact that @{const Iter} might
+ − 801 modify the @{text rhs} in the equation @{term "X = rhs"}, but does not remove it.
+ − 802 Premise 3 of~\eqref{whileprinciple} is by Lem.~\ref{itertwo}. Now in premise 4
+ − 803 we like to show that there exists a @{text rhs} such that @{term "ES = {(X, rhs)}"}
+ − 804 and that @{text "invariant {(X, rhs)}"} holds, provided the condition @{text "Cond"}
113
+ − 805 does not holds. By the stronger invariant we know there exists such a @{text "rhs"}
110
+ − 806 with @{term "(X, rhs) \<in> ES"}. Because @{text Cond} is not true, we know the cardinality
+ − 807 of @{text ES} is @{text 1}. This means @{text "ES"} must actually be the equation @{text "X = rhs"},
+ − 808 for which the invariant holds. This allows us to conclude that
113
+ − 809 @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"} and @{term "invariant {(X, rhs)}"} hold,
+ − 810 as needed.\qed
107
+ − 811 \end{proof}
+ − 812
106
+ − 813 \noindent
+ − 814 With this lemma in place we can show that for every equivalence class in @{term "UNIV // \<approx>A"}
+ − 815 there exists a regular expression.
+ − 816
105
+ − 817 \begin{lemma}\label{every_eqcl_has_reg}
+ − 818 @{thm[mode=IfThen] every_eqcl_has_reg}
+ − 819 \end{lemma}
+ − 820
+ − 821 \begin{proof}
+ − 822 By the preceeding Lemma, we know that there exists a @{text "rhs"} such
+ − 823 that @{term "Solve X (Init (UNIV // \<approx>A))"} returns the equation @{text "X = rhs"},
+ − 824 and that the invariant holds for this equation. That means we
+ − 825 know @{text "X = \<Union>\<calL> ` rhs"}. We further know that
109
+ − 826 this is equal to \mbox{@{text "\<Union>\<calL> ` (Arden X rhs)"}} using the properties of the
110
+ − 827 invariant and Lem.\ref{ardenable}. Using the validity property for the equation @{text "X = rhs"},
106
+ − 828 we can infer that @{term "rhss rhs \<subseteq> {X}"} and because the arden operation
+ − 829 removes that @{text X} from @{text rhs}, that @{term "rhss (Arden X rhs) = {}"}.
113
+ − 830 This means the right-hand side @{term "Arden X rhs"} can only consist of terms of the form @{term "Lam r"}.
106
+ − 831 So we can collect those (finitely many) regular expressions and have @{term "X = L (\<Uplus>rs)"}.
+ − 832 With this we can conclude the proof.\qed
105
+ − 833 \end{proof}
+ − 834
106
+ − 835 \noindent
+ − 836 Lem.~\ref{every_eqcl_has_reg} allows us to finally give a proof for the first direction
+ − 837 of the Myhill-Nerode theorem.
105
+ − 838
106
+ − 839 \begin{proof}[of Thm.~\ref{myhillnerodeone}]
105
+ − 840 By Lem.~\ref{every_eqcl_has_reg} we know that there exists a regular language for
+ − 841 every equivalence class in @{term "UNIV // \<approx>A"}. Since @{text "finals A"} is
110
+ − 842 a subset of @{term "UNIV // \<approx>A"}, we also know that for every equivalence class
105
+ − 843 in @{term "finals A"} there exists a regular language. Moreover by assumption
106
+ − 844 we know that @{term "finals A"} must be finite, and therefore there must be a finite
105
+ − 845 set of regular expressions @{text "rs"} such that
+ − 846
+ − 847 \begin{center}
+ − 848 @{term "\<Union>(finals A) = L (\<Uplus>rs)"}
+ − 849 \end{center}
+ − 850
+ − 851 \noindent
+ − 852 Since the left-hand side is equal to @{text A}, we can use @{term "\<Uplus>rs"}
107
+ − 853 as the regular expression that is needed in the theorem.\qed
105
+ − 854 \end{proof}
54
+ − 855 *}
+ − 856
100
+ − 857
+ − 858
+ − 859
+ − 860 section {* Myhill-Nerode, Second Part *}
39
+ − 861
+ − 862 text {*
116
+ − 863 We will prove in this section the second part of the Myhill-Nerode
+ − 864 theorem. It can be formulated in our setting as follows.
39
+ − 865
54
+ − 866 \begin{theorem}
112
+ − 867 Given @{text "r"} is a regular expressions, then @{thm Myhill_Nerode2}.
54
+ − 868 \end{theorem}
39
+ − 869
116
+ − 870 \noindent
+ − 871 The proof will be by induction on the structure of @{text r}. It turns out
+ − 872 the base cases are straightforward.
+ − 873
+ − 874
+ − 875 \begin{proof}[Base Cases]
+ − 876 The cases for @{const NULL}, @{const EMPTY} and @{const CHAR} are routine, because
+ − 877 we can easily establish
39
+ − 878
114
+ − 879 \begin{center}
+ − 880 \begin{tabular}{l}
+ − 881 @{thm quot_null_eq}\\
+ − 882 @{thm quot_empty_subset}\\
+ − 883 @{thm quot_char_subset}
+ − 884 \end{tabular}
+ − 885 \end{center}
+ − 886
116
+ − 887 \noindent
+ − 888 hold, which shows that @{term "UNIV // \<approx>(L r)"} must be finite.\qed
114
+ − 889 \end{proof}
109
+ − 890
116
+ − 891 \noindent
117
+ − 892 Much more interesting, however, are the inductive cases. They seem hard to be solved
+ − 893 directly. The reader is invited to try.
+ − 894
+ − 895 Our method will rely on some
118
+ − 896 \emph{tagging functions} defined over strings. Given the inductive hypothesis, it will
119
+ − 897 be easy to prove that the range of these tagging functions is finite
+ − 898 (the range of a function @{text f} is defined as @{text "range f \<equiv> f ` UNIV"}).
117
+ − 899 With this we will be able to infer that the tagging functions, seen as a relation,
+ − 900 give rise to finitely many equivalence classes of @{const UNIV}. Finally we
+ − 901 will show that the tagging relation is more refined than @{term "\<approx>(L r)"}, which
118
+ − 902 implies that @{term "UNIV // \<approx>(L r)"} must also be finite.
+ − 903 A relation @{text "R\<^isub>1"} is said to \emph{refine} @{text "R\<^isub>2"} provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}.
119
+ − 904 We formally define the notion of a \emph{tag-relation} as follows.
117
+ − 905
119
+ − 906 \begin{definition}[Tagging-Relation] Given a tag-function @{text tag}, then two strings @{text x}
+ − 907 and @{text y} are \emph{tag-related} provided
117
+ − 908 \begin{center}
+ − 909 @{text "x =tag= y \<equiv> tag x = tag y"}
+ − 910 \end{center}
+ − 911 \end{definition}
+ − 912
118
+ − 913 \noindent
119
+ − 914 In order to establish finiteness of a set @{text A} we shall use the following powerful
118
+ − 915 principle from Isabelle/HOL's library.
+ − 916 %
+ − 917 \begin{equation}\label{finiteimageD}
+ − 918 @{thm[mode=IfThen] finite_imageD}
+ − 919 \end{equation}
+ − 920
+ − 921 \noindent
+ − 922 It states that if an image of a set under an injective function @{text f} (over this set)
+ − 923 is finite, then @{text A} itself must be finite. We can use it to establish the following
+ − 924 two lemmas.
+ − 925
117
+ − 926 \begin{lemma}\label{finone}
+ − 927 @{thm[mode=IfThen] finite_eq_tag_rel}
+ − 928 \end{lemma}
+ − 929
+ − 930 \begin{proof}
119
+ − 931 We set in \eqref{finiteimageD}, @{text f} to be @{text "X \<mapsto> tag ` X"}. We have
+ − 932 @{text "range f"} to be subset of @{term "Pow (range tag)"}, which we know must be
+ − 933 finite by assumption. Now @{term "f (UNIV // =tag=)"} is a subset of @{text "range f"},
+ − 934 and so also finite. Injectivity amounts to showing that @{text "X = Y"} under the
+ − 935 assumptions that @{text "X, Y \<in> "}~@{term "UNIV // =tag="} and @{text "f X = f Y"}.
+ − 936 From the assumption we can obtain a @{text "x \<in> X"} and @{text "y \<in> Y"} with
+ − 937 @{text "tag x = tag y"}. This in turn means that the equivalence classes @{text X}
+ − 938 and @{text Y} must be equal.\qed
117
+ − 939 \end{proof}
+ − 940
+ − 941 \begin{lemma}\label{fintwo}
118
+ − 942 Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, where
+ − 943 @{text "R\<^isub>1"} refines @{text "R\<^isub>2"}.
+ − 944 If @{thm (prem 1) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}
+ − 945 then @{thm (concl) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}.
117
+ − 946 \end{lemma}
+ − 947
+ − 948 \begin{proof}
118
+ − 949 We prove this lemma again using \eqref{finiteimageD}. For this we set @{text f} to
+ − 950 be @{text "X \<mapsto>"}~@{term "{R\<^isub>1 `` {x} | x. x \<in> X}"}. It is easy to see that
+ − 951 @{text "finite (f ` (UNIV // R\<^isub>2))"} because it is a subset of @{text "Pow (UNIV // R\<^isub>1)"},
+ − 952 which is finite by assumption. What remains to be shown is that @{text f} is injective
+ − 953 on @{term "UNIV // R\<^isub>2"}. This is equivalent to showing that two equivalence
+ − 954 classes, say @{text "X"} and @{text Y}, in @{term "UNIV // R\<^isub>2"} are equal, provided
+ − 955 @{text "f X = f Y"}. For @{text "X = Y"} to be equal, we have to find two elements
+ − 956 @{text "x \<in> X"} and @{text "y \<in> Y"} such that they are @{text R\<^isub>2} related.
+ − 957 We know there exists a @{text x} with @{term "X = R\<^isub>2 `` {x}"}
+ − 958 and @{text "x \<in> X"}. From the latter fact we can infer that @{term "R\<^isub>1 ``{x} \<in> f X"}
+ − 959 and further @{term "R\<^isub>1 ``{x} \<in> f Y"}. From this we can obtain a @{text y}
+ − 960 such that @{term "R\<^isub>1 `` {x} = R\<^isub>1 `` {y}"} holds. This means @{text x} and @{text y}
+ − 961 are @{text "R\<^isub>1"}-related. Since by assumption @{text "R\<^isub>1"} refines @{text "R\<^isub>2"},
+ − 962 they must also be @{text "R\<^isub>2"}-related, as we need to show.\qed
117
+ − 963 \end{proof}
+ − 964
+ − 965 \noindent
119
+ − 966 Chaining Lem.~\ref{finone} and \ref{fintwo} together, means in order to show
117
+ − 967 that @{term "UNIV // \<approx>(L r)"} is finite, we have to find a tagging function whose
119
+ − 968 range can be shown to be finite and whose tagging-relation refines @{term "\<approx>(L r)"}.
+ − 969 Let us attempt the @{const ALT}-case.
+ − 970
+ − 971 \begin{proof}[@{const "ALT"}-Case]
+ − 972 We take as tagging function
+ − 973
+ − 974 \begin{center}
+ − 975 @{thm tag_str_ALT_def[where A="A" and B="B", THEN meta_eq_app]}
+ − 976 \end{center}
117
+ − 977
119
+ − 978 \noindent
+ − 979 where @{text "A"} and @{text "B"} are some arbitrary languages.
+ − 980 We can show in general, if @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
+ − 981 then @{term "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))"} holds. The range of
120
+ − 982 @{term "tag_str_ALT A B"} is a subset of this product set. It remains to show
+ − 983 that @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} refines @{term "\<approx>(A \<union> B)"}. This amounts to
+ − 984 showing
+ − 985 %
+ − 986 \begin{center}
+ − 987 @{term "tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<longrightarrow> x \<approx>(A \<union> B) y"}
+ − 988 \end{center}
109
+ − 989
120
+ − 990 \noindent
+ − 991 which by unfolding the Myhill-Nerode relation is identical to
+ − 992 %
+ − 993 \begin{equation}\label{pattern}
+ − 994 @{text "\<forall>z. tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<and> x @ z \<in> A \<union> B \<longrightarrow> y @ z \<in> A \<union> B"}
+ − 995 \end{equation}
+ − 996
+ − 997 \noindent
+ − 998 since both @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} and @{term "\<approx>(A \<union> B)"} are symmetric. To solve
+ − 999 \eqref{pattern} we just have to unfold the tagging-relation and analyse
+ − 1000 in which set, @{text A} or @{text B}, the string @{term "x @ z"} is. Fianlly we
+ − 1001 can discharge this case by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed
119
+ − 1002 \end{proof}
+ − 1003
109
+ − 1004
121
+ − 1005 \noindent
+ − 1006 The pattern in \eqref{pattern} is repeated for the other two cases. Unfortunately,
+ − 1007 they are slightly more complicated.
+ − 1008
+ − 1009
+ − 1010 \begin{proof}[@{const SEQ}-Case]
+ − 1011
+ − 1012 \begin{center}
+ − 1013 @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B", THEN meta_eq_app]}
+ − 1014 \end{center}
+ − 1015 \end{proof}
+ − 1016
+ − 1017 \begin{proof}[@{const STAR}-Case]
+ − 1018
+ − 1019 \begin{center}
+ − 1020 @{thm tag_str_STAR_def[where ?L1.0="A", THEN meta_eq_app]}
+ − 1021 \end{center}
+ − 1022 \end{proof}
39
+ − 1023 *}
+ − 1024
+ − 1025
117
+ − 1026
54
+ − 1027 section {* Conclusion and Related Work *}
+ − 1028
92
+ − 1029 text {*
112
+ − 1030 In this paper we took the view that a regular language is one where there
115
+ − 1031 exists a regular expression that matches all of its strings. Regular
+ − 1032 expressions can conveniently be defined as a datatype in a HOL-based theorem
112
+ − 1033 prover. For us it was therefore interesting to find out how far we can push
+ − 1034 this point of view.
+ − 1035
+ − 1036 Having formalised the Myhill-Nerode theorem means we
+ − 1037 pushed quite far. Using this theorem we can obviously prove when a language
+ − 1038 is \emph{not} regular---by establishing that it has infinitely many
+ − 1039 equivalence classes generated by the Myhill-Nerode relation (this is usually
+ − 1040 the purpose of the pumping lemma \cite{Kozen97}). We can also use it to
+ − 1041 establish the standard textbook results about closure properties of regular
+ − 1042 languages. Interesting is the case of closure under complement, because
+ − 1043 it seems difficult to construct a regular expression for the complement
113
+ − 1044 language by direct means. However the existence of such a regular expression
+ − 1045 can be easily proved using the Myhill-Nerode theorem since
92
+ − 1046
112
+ − 1047 \begin{center}
+ − 1048 @{term "s\<^isub>1 \<approx>A s\<^isub>2"} if and only if @{term "s\<^isub>1 \<approx>(-A) s\<^isub>2"}
+ − 1049 \end{center}
+ − 1050
+ − 1051 \noindent
+ − 1052 holds for any strings @{text "s\<^isub>1"} and @{text
114
+ − 1053 "s\<^isub>2"}. Therefore @{text A} and the complement language @{term "-A"} give rise to the same
+ − 1054 partitions. Proving the existence of such a regular expression via automata would
+ − 1055 be quite involved. It includes the
112
+ − 1056 steps: regular expression @{text "\<Rightarrow>"} non-deterministic automaton @{text
+ − 1057 "\<Rightarrow>"} deterministic automaton @{text "\<Rightarrow>"} complement automaton @{text "\<Rightarrow>"}
+ − 1058 regular expression.
+ − 1059
116
+ − 1060 While regular expressions are convenient in formalisations, they have some
+ − 1061 limitations. One is that there seems to be no notion of a minimal regular
+ − 1062 expression, like there is for automata. For an implementation of a simple
+ − 1063 regular expression matcher, whose correctness has been formally
+ − 1064 established, we refer the reader to Owens and Slind \cite{OwensSlind08}.
+ − 1065
+ − 1066
121
+ − 1067 Our formalisation consists of 790 lines of Isabelle/Isar code for the first
+ − 1068 direction and 475 for the second, plus standard material about regular languages.
+ − 1069 While this might be seen as too large to
113
+ − 1070 count as a concise proof pearl, this should be seen in the context of the
+ − 1071 work done by Constable at al \cite{Constable00} who formalised the
114
+ − 1072 Myhill-Nerode theorem in Nuprl using automata.
113
+ − 1073 They write that their
114
+ − 1074 four-member team needed something on the magnitute of 18 months for their
+ − 1075 formalisation. The estimate for our formalisation is that we
113
+ − 1076 needed approximately 3 months and this included the time to find our proof
+ − 1077 arguments. Unlike Constable et al, who were able to follow the proofs from
114
+ − 1078 \cite{HopcroftUllman69}, we had to find our own arguments. So for us the formalisation
113
+ − 1079 was not the bottleneck. It is hard to gauge the size of a formalisation in
+ − 1080 Nurpl, but from what is shown in the Nuprl Math Library about their
+ − 1081 development it seems substantially larger than ours. The code of
121
+ − 1082 ours can be found in the Mercurial Repository at
113
+ − 1083
+ − 1084 \begin{center}
121
+ − 1085 \url{http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/regexp/}
113
+ − 1086 \end{center}
+ − 1087
112
+ − 1088
+ − 1089 Our proof of the first direction is very much inspired by \emph{Brzozowski's
+ − 1090 algebraic mehod} used to convert a finite automaton to a regular
113
+ − 1091 expression \cite{Brzozowski64}. The close connection can be seen by considering the equivalence
111
+ − 1092 classes as the states of the minimal automaton for the regular language.
114
+ − 1093 However there are some subtle differences. Since we identify equivalence
111
+ − 1094 classes with the states of the automaton, then the most natural choice is to
+ − 1095 characterise each state with the set of strings starting from the initial
113
+ − 1096 state leading up to that state. Usually, however, the states are characterised as the
111
+ − 1097 ones starting from that state leading to the terminal states. The first
+ − 1098 choice has consequences how the initial equational system is set up. We have
115
+ − 1099 the $\lambda$-term on our `initial state', while Brzozowski has it on the
111
+ − 1100 terminal states. This means we also need to reverse the direction of Arden's
+ − 1101 lemma.
92
+ − 1102
112
+ − 1103 We briefly considered using the method Brzozowski presented in the Appendix
113
+ − 1104 of~\cite{Brzozowski64} in order to prove the second direction of the
112
+ − 1105 Myhill-Nerode theorem. There he calculates the derivatives for regular
+ − 1106 expressions and shows that there can be only finitely many of them. We could
114
+ − 1107 have used as the tag of a string @{text s} the derivative of a regular expression
112
+ − 1108 generated with respect to @{text s}. Using the fact that two strings are
+ − 1109 Myhill-Nerode related whenever their derivative is the same together with
+ − 1110 the fact that there are only finitely many derivatives for a regular
113
+ − 1111 expression would give us the same argument as ours. However it seems not so easy to
112
+ − 1112 calculate the derivatives and then to count them. Therefore we preferred our
+ − 1113 direct method of using tagging-functions involving equivalence classes. This
+ − 1114 is also where our method shines, because we can completely side-step the
+ − 1115 standard argument \cite{Kozen97} where automata need to be composed, which
113
+ − 1116 as stated in the Introduction is not so convenient to formalise in a
121
+ − 1117 HOL-based theorem prover. However, it is also the direction where we had to
+ − 1118 spend most of the `conceptual' time, as our proof-argument based on tagging functions
+ − 1119 is new for establishing the Myhill-Nerode theorem.
111
+ − 1120
92
+ − 1121 *}
+ − 1122
+ − 1123
24
+ − 1124 (*<*)
+ − 1125 end
+ − 1126 (*>*)