21 *} |
21 *} |
22 |
22 |
23 section {* Preliminaries *} |
23 section {* Preliminaries *} |
24 |
24 |
25 text {* |
25 text {* |
26 A central technique in our proof is the solution of equational systems |
26 Central to our proof will be the solution of equational systems |
27 involving regular expressions. For this we will use the following ``reverse'' |
27 involving regular expressions. For this we will use the following ``reverse'' |
28 version of Arden's lemma. |
28 version of Arden's lemma. |
29 |
29 |
30 \begin{lemma}[Reverse Arden's Lemma]\mbox{}\\ |
30 \begin{lemma}[Reverse Arden's Lemma]\mbox{}\\ |
31 If @{thm (prem 1) ardens_revised} then |
31 If @{thm (prem 1) ardens_revised} then |
32 @{thm (lhs) ardens_revised} has the unique solution |
32 @{thm (lhs) ardens_revised} has the unique solution |
33 @{thm (rhs) ardens_revised}. |
33 @{thm (rhs) ardens_revised}. |
34 \end{lemma} |
34 \end{lemma} |
35 |
35 |
36 \begin{proof} |
36 \begin{proof} |
37 For right-to-left direction we assume @{thm (rhs) ardens_revised} and show |
37 For the 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>"}, |
38 that @{thm (lhs) ardens_revised} holds. 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 |
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 |
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. |
41 is equal to @{term "(B ;; A\<star>) ;; A \<union> B"}. This completes this direction. |
42 |
42 |
43 For the other direction we assume @{thm (lhs) ardens_revised}. By a simple induction |
43 For the other direction we assume @{thm (lhs) ardens_revised}. By a simple induction |
44 on @{text n}, we can show the property |
44 on @{text n}, we can establish the property |
45 |
45 |
46 \begin{center} |
46 \begin{center} |
47 @{text "(*)"}\hspace{5mm} @{thm (concl) ardens_helper} |
47 @{text "(*)"}\hspace{5mm} @{thm (concl) ardens_helper} |
48 \end{center} |
48 \end{center} |
49 |
49 |
50 \noindent |
50 \noindent |
51 Using this property we can show that @{term "B ;; (A \<up> n) \<subseteq> X"} holds for |
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 ???. |
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} |
53 For the inclusion in the other direction we assume a string @{text s} |
54 with length @{text k} is element in @{text X}. Since @{thm (prem 1) ardens_revised} |
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}. |
55 we know that @{term "s \<notin> X ;; (A \<up> Suc k)"} since its length is only @{text k} |
|
56 (the strings in @{term "X ;; (A \<up> Suc k)"} are all longer). |
56 From @{text "(*)"} it follows that |
57 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 @{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 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 is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed |
60 \end{proof} |
61 \end{proof} |