equal
deleted
inserted
replaced
912 \begin{center} |
912 \begin{center} |
913 @{text "x =tag= y \<equiv> tag x = tag y"}. |
913 @{text "x =tag= y \<equiv> tag x = tag y"}. |
914 \end{center} |
914 \end{center} |
915 \end{definition} |
915 \end{definition} |
916 |
916 |
917 \noindent |
917 |
918 In order to establish finiteness of a set @{text A}, we shall use the following powerful |
918 In order to establish finiteness of a set @{text A}, we shall use the following powerful |
919 principle from Isabelle/HOL's library. |
919 principle from Isabelle/HOL's library. |
920 % |
920 % |
921 \begin{equation}\label{finiteimageD} |
921 \begin{equation}\label{finiteimageD} |
922 @{thm[mode=IfThen] finite_imageD} |
922 @{thm[mode=IfThen] finite_imageD} |
1216 otherwise @{text "x'\<^isub>m\<^isub>a\<^isub>x"} is not the longest prefix. That means @{text a} |
1216 otherwise @{text "x'\<^isub>m\<^isub>a\<^isub>x"} is not the longest prefix. That means @{text a} |
1217 `overlaps' with @{text z}, splitting it into two components @{text "z\<^isub>a"} and |
1217 `overlaps' with @{text z}, splitting it into two components @{text "z\<^isub>a"} and |
1218 @{text "z\<^isub>b"}. For this we know that @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"} and |
1218 @{text "z\<^isub>b"}. For this we know that @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"} and |
1219 @{term "z\<^isub>b \<in> A\<star>"}. To cut a story short, we have divided @{term "x @ z \<in> A\<star>"} |
1219 @{term "z\<^isub>b \<in> A\<star>"}. To cut a story short, we have divided @{term "x @ z \<in> A\<star>"} |
1220 such that we have a string @{text a} with @{text "a \<in> A"} that lies just on the |
1220 such that we have a string @{text a} with @{text "a \<in> A"} that lies just on the |
1221 `border' of @{text x} and @{text z}. This string is @{text "(x - x') @ z\<^isub>a"}. |
1221 `border' of @{text x} and @{text z}. This string is @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a"}. |
1222 |
1222 |
1223 In order to show that @{term "x @ z \<in> A\<star>"} implies @{term "y @ z \<in> A\<star>"}, we use |
1223 In order to show that @{term "x @ z \<in> A\<star>"} implies @{term "y @ z \<in> A\<star>"}, we use |
1224 the following tagging-function: |
1224 the following tagging-function: |
1225 % |
1225 % |
1226 \begin{center} |
1226 \begin{center} |
1270 section {* Conclusion and Related Work *} |
1270 section {* Conclusion and Related Work *} |
1271 |
1271 |
1272 text {* |
1272 text {* |
1273 In this paper we took the view that a regular language is one where there |
1273 In this paper we took the view that a regular language is one where there |
1274 exists a regular expression that matches all of its strings. Regular |
1274 exists a regular expression that matches all of its strings. Regular |
1275 expressions can conveniently be defined as a datatype in a HOL-based theorem |
1275 expressions can conveniently be defined as a datatype in HOL-based theorem |
1276 prover. For us it was therefore interesting to find out how far we can push |
1276 provers. For us it was therefore interesting to find out how far we can push |
1277 this point of view. We have established both directions of the Myhill-Nerode |
1277 this point of view. We have established both directions of the Myhill-Nerode |
1278 theorem. |
1278 theorem. |
1279 % |
1279 % |
1280 \begin{theorem}[The Myhill-Nerode Theorem]\mbox{}\\ |
1280 \begin{theorem}[The Myhill-Nerode Theorem]\mbox{}\\ |
1281 A language @{text A} is regular if and only if @{thm (rhs) Myhill_Nerode}. |
1281 A language @{text A} is regular if and only if @{thm (rhs) Myhill_Nerode}. |