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