equal
deleted
inserted
replaced
411 A language @{text A} is \emph{regular}, provided there is a regular expression |
411 A language @{text A} is \emph{regular}, provided there is a regular expression |
412 that matches all strings of @{text "A"}. |
412 that matches all strings of @{text "A"}. |
413 \end{dfntn} |
413 \end{dfntn} |
414 |
414 |
415 \noindent |
415 \noindent |
416 And then `forget' automata. |
416 And then `forget' automata completely. |
417 The reason is that regular expressions, unlike graphs, matrices and |
417 The reason is that regular expressions, unlike graphs, matrices and |
418 functions, can be easily defined as an inductive datatype. A reasoning |
418 functions, can be easily defined as an inductive datatype. A reasoning |
419 infrastructure (like induction and recursion) comes for free in |
419 infrastructure (like induction and recursion) comes for free in |
420 HOL. Moreover, no side-conditions will be needed for regular expressions, |
420 HOL. Moreover, no side-conditions will be needed for regular expressions, |
421 like we need for automata. This convenience of regular expressions has |
421 like we need for automata. This convenience of regular expressions has |
2112 the right-hand side of \eqref{eqq} is equal to the language \mbox{@{term "lang (\<Uplus>(pderivs_lang B |
2112 the right-hand side of \eqref{eqq} is equal to the language \mbox{@{term "lang (\<Uplus>(pderivs_lang B |
2113 r))"}}. Thus the regular expression @{term "\<Uplus>(pderivs_lang B r)"} verifies that |
2113 r))"}}. Thus the regular expression @{term "\<Uplus>(pderivs_lang B r)"} verifies that |
2114 @{term "Deriv_lang B A"} is regular. |
2114 @{term "Deriv_lang B A"} is regular. |
2115 |
2115 |
2116 Even more surprising is the fact that for \emph{every} language @{text A}, the language |
2116 Even more surprising is the fact that for \emph{every} language @{text A}, the language |
2117 consisting of all substrings of @{text A} is regular \cite{Haines69} (see also |
2117 consisting of all (scattered) substrings of @{text A} is regular \cite{Haines69} (see also |
2118 \cite{Shallit08, Gasarch09}). |
2118 \cite{Shallit08, Gasarch09}). |
2119 A \emph{substring} can be obtained |
2119 A \emph{(scattered) substring} can be obtained |
2120 by striking out zero or more characters from a string. This can be defined |
2120 by striking out zero or more characters from a string. This can be defined |
2121 inductively in Isabelle/HOL by the following three rules: |
2121 inductively in Isabelle/HOL by the following three rules: |
2122 |
2122 |
2123 \begin{center} |
2123 \begin{center} |
2124 @{thm[mode=Axiom] emb0[where bs="x"]}\hspace{10mm} |
2124 @{thm[mode=Axiom] emb0[where bs="x"]}\hspace{10mm} |