747 \begin{proof} |
747 \begin{proof} |
748 By the preceeding Lemma, we know that there exists a @{text "rhs"} such |
748 By the preceeding Lemma, we know that there exists a @{text "rhs"} such |
749 that @{term "Solve X (Init (UNIV // \<approx>A))"} returns the equation @{text "X = rhs"}, |
749 that @{term "Solve X (Init (UNIV // \<approx>A))"} returns the equation @{text "X = rhs"}, |
750 and that the invariant holds for this equation. That means we |
750 and that the invariant holds for this equation. That means we |
751 know @{text "X = \<Union>\<calL> ` rhs"}. We further know that |
751 know @{text "X = \<Union>\<calL> ` rhs"}. We further know that |
752 this is equal to \mbox{@{text "\<Union>\<calL> ` (Arden X rhs)"}} using the properties in the |
752 this is equal to \mbox{@{text "\<Union>\<calL> ` (Arden X rhs)"}} using the properties of the |
753 invariant and Lem.~???. Using the validity property for the equation @{text "X = rhs"}, |
753 invariant and Lem.~???. Using the validity property for the equation @{text "X = rhs"}, |
754 we can infer that @{term "rhss rhs \<subseteq> {X}"} and because the arden operation |
754 we can infer that @{term "rhss rhs \<subseteq> {X}"} and because the arden operation |
755 removes that @{text X} from @{text rhs}, that @{term "rhss (Arden X rhs) = {}"}. |
755 removes that @{text X} from @{text rhs}, that @{term "rhss (Arden X rhs) = {}"}. |
756 That means @{term "Arden X rhs"} can only consist of terms of the form @{term "Lam r"}. |
756 That means @{term "Arden X rhs"} can only consist of terms of the form @{term "Lam r"}. |
757 So we can collect those (finitely many) regular expressions and have @{term "X = L (\<Uplus>rs)"}. |
757 So we can collect those (finitely many) regular expressions and have @{term "X = L (\<Uplus>rs)"}. |
802 @{thm quot_char_subset} |
802 @{thm quot_char_subset} |
803 \end{tabular} |
803 \end{tabular} |
804 \end{center} |
804 \end{center} |
805 |
805 |
806 \end{proof} |
806 \end{proof} |
|
807 |
|
808 |
|
809 @{thm tag_str_ALT_def[where ?L1.0="A" and ?L2.0="B"]} |
|
810 |
|
811 @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B"]} |
|
812 |
|
813 @{thm tag_str_STAR_def[where ?L1.0="A"]} |
807 *} |
814 *} |
808 |
815 |
809 |
816 |
810 section {* Conclusion and Related Work *} |
817 section {* Conclusion and Related Work *} |
811 |
818 |
812 text {* |
819 text {* |
813 In this paper we took the view that a regular language as one where there exists |
820 In this paper we took the view that a regular language is one where there exists |
814 a regular expression that matches all its strings. For us it was important to find |
821 a regular expression that matches all its strings. For us it was important to find |
815 out how far we can push this point of view. Having formalised the Myhill-Nerode |
822 out how far we can push this point of view. Having formalised the Myhill-Nerode |
816 theorem means pushed very far. Having the Myhill-Nerode theorem means we can |
823 theorem means pushed quite far. Having the Myhill-Nerode theorem means we can |
817 formalise much of the textbook results in this subject. |
824 formalise much of the textbook results in this subject. |
818 |
825 |
819 |
826 |
820 *} |
827 *} |
821 |
828 |