236 which solves equations of the form @{term "X = A ;; X \<union> B"} provided |
236 which solves equations of the form @{term "X = A ;; X \<union> B"} provided |
237 @{term "[] \<notin> A"}. However we will need the following ``reverse'' |
237 @{term "[] \<notin> A"}. However we will need the following ``reverse'' |
238 version of Arden's lemma. |
238 version of Arden's lemma. |
239 |
239 |
240 \begin{lemma}[Reverse Arden's Lemma]\label{arden}\mbox{}\\ |
240 \begin{lemma}[Reverse Arden's Lemma]\label{arden}\mbox{}\\ |
241 If @{thm (prem 1) ardens_revised} then |
241 If @{thm (prem 1) arden} then |
242 @{thm (lhs) ardens_revised} has the unique solution |
242 @{thm (lhs) arden} has the unique solution |
243 @{thm (rhs) ardens_revised}. |
243 @{thm (rhs) arden}. |
244 \end{lemma} |
244 \end{lemma} |
245 |
245 |
246 \begin{proof} |
246 \begin{proof} |
247 For the right-to-left direction we assume @{thm (rhs) ardens_revised} and show |
247 For the right-to-left direction we assume @{thm (rhs) arden} and show |
248 that @{thm (lhs) ardens_revised} holds. From Prop.~\ref{langprops}@{text "(i)"} |
248 that @{thm (lhs) arden} holds. From Prop.~\ref{langprops}@{text "(i)"} |
249 we have @{term "A\<star> = {[]} \<union> A ;; A\<star>"}, |
249 we have @{term "A\<star> = {[]} \<union> A ;; A\<star>"}, |
250 which is equal to @{term "A\<star> = {[]} \<union> A\<star> ;; A"}. Adding @{text B} to both |
250 which is equal to @{term "A\<star> = {[]} \<union> A\<star> ;; A"}. Adding @{text B} to both |
251 sides gives @{term "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"}, whose right-hand side |
251 sides gives @{term "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"}, whose right-hand side |
252 is equal to @{term "(B ;; A\<star>) ;; A \<union> B"}. This completes this direction. |
252 is equal to @{term "(B ;; A\<star>) ;; A \<union> B"}. This completes this direction. |
253 |
253 |
254 For the other direction we assume @{thm (lhs) ardens_revised}. By a simple induction |
254 For the other direction we assume @{thm (lhs) arden}. By a simple induction |
255 on @{text n}, we can establish the property |
255 on @{text n}, we can establish the property |
256 |
256 |
257 \begin{center} |
257 \begin{center} |
258 @{text "(*)"}\hspace{5mm} @{thm (concl) ardens_helper} |
258 @{text "(*)"}\hspace{5mm} @{thm (concl) arden_helper} |
259 \end{center} |
259 \end{center} |
260 |
260 |
261 \noindent |
261 \noindent |
262 Using this property we can show that @{term "B ;; (A \<up> n) \<subseteq> X"} holds for |
262 Using this property we can show that @{term "B ;; (A \<up> n) \<subseteq> X"} holds for |
263 all @{text n}. From this we can infer @{term "B ;; A\<star> \<subseteq> X"} using the definition |
263 all @{text n}. From this we can infer @{term "B ;; A\<star> \<subseteq> X"} using the definition |
264 of @{text "\<star>"}. |
264 of @{text "\<star>"}. |
265 For the inclusion in the other direction we assume a string @{text s} |
265 For the inclusion in the other direction we assume a string @{text s} |
266 with length @{text k} is element in @{text X}. Since @{thm (prem 1) ardens_revised} |
266 with length @{text k} is element in @{text X}. Since @{thm (prem 1) arden} |
267 we know by Prop.~\ref{langprops}@{text "(ii)"} that |
267 we know by Prop.~\ref{langprops}@{text "(ii)"} that |
268 @{term "s \<notin> X ;; (A \<up> Suc k)"} since its length is only @{text k} |
268 @{term "s \<notin> X ;; (A \<up> Suc k)"} since its length is only @{text k} |
269 (the strings in @{term "X ;; (A \<up> Suc k)"} are all longer). |
269 (the strings in @{term "X ;; (A \<up> Suc k)"} are all longer). |
270 From @{text "(*)"} it follows then that |
270 From @{text "(*)"} it follows then that |
271 @{term s} must be element in @{term "(\<Union>m\<in>{0..k}. B ;; (A \<up> m))"}. This in turn |
271 @{term s} must be element in @{term "(\<Union>m\<in>{0..k}. B ;; (A \<up> m))"}. This in turn |
390 the method by Brzozowski \cite{Brzozowski64}, since for his purposes he needs to mark |
390 the method by Brzozowski \cite{Brzozowski64}, since for his purposes he needs to mark |
391 the ``terminal'' states.) Overloading the function @{text L} for the two kinds of terms in the |
391 the ``terminal'' states.) Overloading the function @{text L} for the two kinds of terms in the |
392 equational system as follows |
392 equational system as follows |
393 |
393 |
394 \begin{center} |
394 \begin{center} |
395 @{thm L_rhs_e.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm} |
395 @{thm L_rhs_item.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm} |
396 @{thm L_rhs_e.simps(1)[where r="r", THEN eq_reflection]} |
396 @{thm L_rhs_item.simps(1)[where r="r", THEN eq_reflection]} |
397 \end{center} |
397 \end{center} |
398 |
398 |
399 \noindent |
399 \noindent |
400 we can prove for @{text "X\<^isub>2\<^isub>.\<^isub>.\<^isub>n"} that the following equations |
400 we can prove for @{text "X\<^isub>2\<^isub>.\<^isub>.\<^isub>n"} that the following equations |
401 % |
401 % |