12 notation (latex output) |
12 notation (latex output) |
13 str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and |
13 str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and |
14 Seq (infixr "\<cdot>" 100) and |
14 Seq (infixr "\<cdot>" 100) and |
15 Star ("_\<^bsup>\<star>\<^esup>") and |
15 Star ("_\<^bsup>\<star>\<^esup>") and |
16 pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and |
16 pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and |
17 Suc ("_+1>" [100] 100) and |
17 Suc ("_+1" [100] 100) and |
18 quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and |
18 quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and |
19 REL ("\<approx>") |
19 REL ("\<approx>") |
20 |
|
21 |
20 |
22 (*>*) |
21 (*>*) |
23 |
22 |
24 section {* Introduction *} |
23 section {* Introduction *} |
25 |
24 |
26 text {* |
25 text {* |
|
26 Regular languages are an important and well-understood subject in Computer |
|
27 Science with many beautiful theorems and many useful algorithms. There is a |
|
28 wide range of textbooks about this subject. Many of these textbooks, such as |
|
29 \cite{Kozen97}, are aimed at students and contain very detailed |
|
30 ``pencil-and-paper'' proofs. It seems natural to exercise theorem provers by |
|
31 formalising these theorems and by verifying formally the algorithms. There |
|
32 is however a problem: the typical approach to regular languages is to start |
|
33 with finite automata. |
|
34 |
|
35 |
|
36 |
|
37 |
|
38 |
27 |
39 |
28 Therefore instead of defining a regular language as being one where there exists an |
40 Therefore instead of defining a regular language as being one where there exists an |
29 automata that regognises all of its strings, we define |
41 automata that regognises all of its strings, we define |
30 |
42 |
31 \begin{definition}[A Regular Language] |
43 \begin{definition}[A Regular Language] |
41 *} |
53 *} |
42 |
54 |
43 section {* Preliminaries *} |
55 section {* Preliminaries *} |
44 |
56 |
45 text {* |
57 text {* |
46 Strings in Isabelle/HOL are lists of characters. Therefore the |
58 Strings in Isabelle/HOL are lists of characters and the |
47 \emph{empty string} is represented by the empty list, written @{term "[]"}. \emph{Languages} are sets of |
59 \emph{empty string} is the empty list, written @{term "[]"}. \emph{Languages} are sets of |
48 strings. The language containing all strings is abbreviated as @{term "UNIV::string set"} |
60 strings. The language containing all strings is written in Isabelle/HOL as @{term "UNIV::string set"}. |
49 and the notation for the quotient of a language @{text A} according to a relation @{term REL} is |
61 The notation for the quotient of a language @{text A} according to a relation @{term REL} is |
50 @{term "A // REL"}. |
62 @{term "A // REL"}. The concatenation of two languages is written @{term "A ;; B"}; a language |
51 |
63 raised tow the power $n$ is written @{term "A \<up> n"}. Both concepts are defined as |
52 Set operations |
|
53 |
64 |
54 \begin{center} |
65 \begin{center} |
55 @{thm Seq_def} |
66 @{thm Seq_def[THEN eq_reflection, where A1="A" and B1="B"]} |
|
67 \hspace{7mm} |
|
68 @{thm pow.simps(1)[THEN eq_reflection, where A1="A"]} |
|
69 \hspace{7mm} |
|
70 @{thm pow.simps(2)[THEN eq_reflection, where A1="A" and n1="n"]} |
56 \end{center} |
71 \end{center} |
57 |
72 |
58 \noindent |
73 \noindent |
59 where @{text "@"} is the usual list-append operation. |
74 where @{text "@"} is the usual list-append operation. The Kleene-star of a language @{text A} |
|
75 is defined as the union over all powers, namely @{thm Star_def}. |
|
76 |
60 |
77 |
61 \noindent |
|
62 Regular expressions are defined as the following datatype |
78 Regular expressions are defined as the following datatype |
63 |
79 |
64 \begin{center} |
80 \begin{center} |
65 @{text r} @{text "::="} |
81 @{text r} @{text "::="} |
66 @{term NULL}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} |
82 @{term NULL}\hspace{1.5mm}@{text"|"}\hspace{1.5mm} |