703 If @{thm (prem 1) Solve} and @{thm (prem 2) Solve} then there exists |
703 If @{thm (prem 1) Solve} and @{thm (prem 2) Solve} then there exists |
704 a @{text rhs} such that @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"} |
704 a @{text rhs} such that @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"} |
705 and @{term "invariant {(X, rhs)}"}. |
705 and @{term "invariant {(X, rhs)}"}. |
706 \end{lemma} |
706 \end{lemma} |
707 |
707 |
|
708 \noindent |
|
709 With this lemma in place we can show that for every equivalence class in @{term "UNIV // \<approx>A"} |
|
710 there exists a regular expression. |
|
711 |
708 \begin{lemma}\label{every_eqcl_has_reg} |
712 \begin{lemma}\label{every_eqcl_has_reg} |
709 @{thm[mode=IfThen] every_eqcl_has_reg} |
713 @{thm[mode=IfThen] every_eqcl_has_reg} |
710 \end{lemma} |
714 \end{lemma} |
711 |
715 |
712 \begin{proof} |
716 \begin{proof} |
713 By the preceeding Lemma, we know that there exists a @{text "rhs"} such |
717 By the preceeding Lemma, we know that there exists a @{text "rhs"} such |
714 that @{term "Solve X (Init (UNIV // \<approx>A))"} returns the equation @{text "X = rhs"}, |
718 that @{term "Solve X (Init (UNIV // \<approx>A))"} returns the equation @{text "X = rhs"}, |
715 and that the invariant holds for this equation. That means we |
719 and that the invariant holds for this equation. That means we |
716 know @{text "X = \<Union>\<calL> ` rhs"}. We further know that |
720 know @{text "X = \<Union>\<calL> ` rhs"}. We further know that |
717 this is equal to @{text "\<Union>\<calL> ` (Arden X rhs)"} using ???. |
721 this is equal to \mbox{@{text "\<Union>\<calL> ` (Arden X rhs)"}} using the properties in the |
718 |
722 invariant and Lem.~???. Using the validity property for the equation @{text "X = rhs"}, |
|
723 we can infer that @{term "rhss rhs \<subseteq> {X}"} and because the arden operation |
|
724 removes that @{text X} from @{text rhs}, that @{term "rhss (Arden X rhs) = {}"}. |
|
725 That means @{term "Arden X rhs"} can only consist of terms of the form @{term "Lam r"}. |
|
726 So we can collect those (finitely many) regular expressions and have @{term "X = L (\<Uplus>rs)"}. |
|
727 With this we can conclude the proof.\qed |
719 \end{proof} |
728 \end{proof} |
720 |
729 |
721 \begin{theorem} |
730 \noindent |
722 @{thm[mode=IfThen] Myhill_Nerode1} |
731 Lem.~\ref{every_eqcl_has_reg} allows us to finally give a proof for the first direction |
723 \end{theorem} |
732 of the Myhill-Nerode theorem. |
724 |
733 |
725 \begin{proof} |
734 \begin{proof}[of Thm.~\ref{myhillnerodeone}] |
726 By Lem.~\ref{every_eqcl_has_reg} we know that there exists a regular language for |
735 By Lem.~\ref{every_eqcl_has_reg} we know that there exists a regular language for |
727 every equivalence class in @{term "UNIV // \<approx>A"}. Since @{text "finals A"} is |
736 every equivalence class in @{term "UNIV // \<approx>A"}. Since @{text "finals A"} is |
728 a subset of @{term "UNIV // \<approx>A"}, we also know that for every equvalence class |
737 a subset of @{term "UNIV // \<approx>A"}, we also know that for every equvalence class |
729 in @{term "finals A"} there exists a regular language. Moreover by assumption |
738 in @{term "finals A"} there exists a regular language. Moreover by assumption |
730 we know that @{term "finals A"} must be finite, therefore there must be a finite |
739 we know that @{term "finals A"} must be finite, and therefore there must be a finite |
731 set of regular expressions @{text "rs"} such that |
740 set of regular expressions @{text "rs"} such that |
732 |
741 |
733 \begin{center} |
742 \begin{center} |
734 @{term "\<Union>(finals A) = L (\<Uplus>rs)"} |
743 @{term "\<Union>(finals A) = L (\<Uplus>rs)"} |
735 \end{center} |
744 \end{center} |