4 begin |
4 begin |
5 |
5 |
6 declare [[show_question_marks = false]] |
6 declare [[show_question_marks = false]] |
7 |
7 |
8 notation (latex output) |
8 notation (latex output) |
9 str_eq_rel ("\<approx>\<^bsub>_\<^esub>") |
9 str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and |
|
10 Seq (infixr "\<cdot>" 100) and |
|
11 Star ("_\<^bsup>\<star>\<^esup>") and |
|
12 pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and |
|
13 Suc ("_+1" [100] 100) |
10 |
14 |
11 (*>*) |
15 (*>*) |
12 |
16 |
13 section {* Introduction *} |
17 section {* Introduction *} |
14 |
18 |
15 text {* |
19 text {* |
16 |
20 |
17 *} |
21 *} |
18 |
22 |
|
23 section {* Preliminaries *} |
|
24 |
|
25 text {* |
|
26 A central technique in our proof is the solution of equational systems |
|
27 involving regular expressions. For this we will use the following ``reverse'' |
|
28 version of Arden's lemma. |
|
29 |
|
30 \begin{lemma}[Reverse Arden's Lemma]\mbox{}\\ |
|
31 If @{thm (prem 1) ardens_revised} then |
|
32 @{thm (lhs) ardens_revised} has the unique solution |
|
33 @{thm (rhs) ardens_revised}. |
|
34 \end{lemma} |
|
35 |
|
36 \begin{proof} |
|
37 For right-to-left direction we assume @{thm (rhs) ardens_revised} and show |
|
38 @{thm (lhs) ardens_revised}. From Lemma ??? we have @{term "A\<star> = {[]} \<union> A ;; A\<star>"}, |
|
39 which is equal to @{term "A\<star> = {[]} \<union> A\<star> ;; A"}. Adding @{text B} to both |
|
40 sides gives @{term "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"}, whose right-hand side |
|
41 is @{term "B \<union> (B ;; A\<star>) ;; A"}. This completes this direction. |
|
42 |
|
43 For the other direction we assume @{thm (lhs) ardens_revised}. By a simple induction |
|
44 on @{text n}, we can show the property |
|
45 |
|
46 \begin{center} |
|
47 @{text "(*)"}\hspace{5mm} @{thm (concl) ardens_helper} |
|
48 \end{center} |
|
49 |
|
50 \noindent |
|
51 Using this property we can show that @{term "B ;; (A \<up> n) \<subseteq> X"} holds for |
|
52 all @{text n}. From this we can infer @{term "B ;; A\<star> \<subseteq> X"} using Lemma ???. |
|
53 The inclusion in the other direction we establishing by assuming a string @{text s} |
|
54 with length @{text k} is element in @{text X}. Since @{thm (prem 1) ardens_revised} |
|
55 we know that @{term "s \<notin> X ;; (A \<up> Suc k)"} as its length is only @{text k}. |
|
56 From @{text "(*)"} it follows that |
|
57 @{term s} must be element in @{term "(\<Union>m\<in>{0..k}. B ;; (A \<up> m))"}. This in turn |
|
58 implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Lemma ??? this |
|
59 is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed |
|
60 \end{proof} |
|
61 *} |
19 |
62 |
20 section {* Regular expressions have finitely many partitions *} |
63 section {* Regular expressions have finitely many partitions *} |
21 |
64 |
22 text {* |
65 text {* |
23 |
66 |
25 Given @{text "r"} is a regular expressions, then @{thm rexp_imp_finite}. |
68 Given @{text "r"} is a regular expressions, then @{thm rexp_imp_finite}. |
26 \end{lemma} |
69 \end{lemma} |
27 |
70 |
28 \begin{proof} |
71 \begin{proof} |
29 By induction on the structure of @{text r}. The cases for @{const NULL}, @{const EMPTY} |
72 By induction on the structure of @{text r}. The cases for @{const NULL}, @{const EMPTY} |
30 and @{const CHAR} are starightforward, because we can easily establish |
73 and @{const CHAR} are straightforward, because we can easily establish |
31 |
74 |
32 \begin{center} |
75 \begin{center} |
33 \begin{tabular}{l} |
76 \begin{tabular}{l} |
34 @{thm quot_null_eq}\\ |
77 @{thm quot_null_eq}\\ |
35 @{thm quot_empty_subset}\\ |
78 @{thm quot_empty_subset}\\ |