665 |
665 |
666 \noindent |
666 \noindent |
667 The first two ensure that the equational system is always finite (number of equations |
667 The first two ensure that the equational system is always finite (number of equations |
668 and number of terms in each equation); \ldots |
668 and number of terms in each equation); \ldots |
669 |
669 |
|
670 It is straightforward to prove that the inital equational system satisfies the |
|
671 invariant. |
|
672 |
670 \begin{lemma} |
673 \begin{lemma} |
671 @{thm[mode=IfThen] Init_ES_satisfies_invariant} |
674 @{thm[mode=IfThen] Init_ES_satisfies_invariant} |
672 \end{lemma} |
675 \end{lemma} |
673 |
676 |
|
677 \begin{proof} |
|
678 Finiteness is given by the assumption and the way how we set up the |
|
679 initial equational system. Soundness is proved in Lem.~\ref{inv}. Distinctness |
|
680 follows from the fact that the equivalence classes are disjoint. The ardenable |
|
681 property also follows from the setup of the equational system as does |
|
682 validity.\qed |
|
683 \end{proof} |
|
684 |
674 \begin{lemma} |
685 \begin{lemma} |
675 @{thm[mode=IfThen] iteration_step_invariant[where xrhs="rhs"]} |
686 @{thm[mode=IfThen] iteration_step_invariant[where xrhs="rhs"]} |
676 \end{lemma} |
687 \end{lemma} |
677 |
688 |
678 \begin{lemma} |
689 \begin{lemma} |
679 @{thm[mode=IfThen] iteration_step_measure[simplified (no_asm), where xrhs="rhs"]} |
690 @{thm[mode=IfThen] iteration_step_measure[simplified (no_asm), where xrhs="rhs"]} |
680 \end{lemma} |
691 \end{lemma} |
|
692 |
|
693 \begin{proof} |
|
694 By assumption we know that @{text "ES"} is finite and has more than one element. |
|
695 Therefore there must be an element @{term "(Y, yrhs) \<in> ES"} with |
|
696 @{term "(Y, yrhs) \<noteq> (X, rhs)"}. Using the distictness property we can infer |
|
697 that @{term "Y \<noteq> X"}. We further know that @{text "Remove ES Y yrhs"} |
|
698 removes the equation @{text "Y = yrhs"} from the system, and therefore |
|
699 the cardinality of @{const Iter} strictly decreases.\qed |
|
700 \end{proof} |
681 |
701 |
682 \begin{lemma} |
702 \begin{lemma} |
683 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 |
684 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)}"} |
685 and @{term "invariant {(X, rhs)}"}. |
705 and @{term "invariant {(X, rhs)}"}. |
686 \end{lemma} |
706 \end{lemma} |
687 |
707 |
|
708 \begin{lemma}\label{every_eqcl_has_reg} |
|
709 @{thm[mode=IfThen] every_eqcl_has_reg} |
|
710 \end{lemma} |
|
711 |
|
712 \begin{proof} |
|
713 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"}, |
|
715 and that the invariant holds for this equation. That means we |
|
716 know @{text "X = \<Union>\<calL> ` rhs"}. We further know that |
|
717 this is equal to @{text "\<Union>\<calL> ` (Arden X rhs)"} using ???. |
|
718 |
|
719 \end{proof} |
|
720 |
688 \begin{theorem} |
721 \begin{theorem} |
689 @{thm[mode=IfThen] Myhill_Nerode1} |
722 @{thm[mode=IfThen] Myhill_Nerode1} |
690 \end{theorem} |
723 \end{theorem} |
|
724 |
|
725 \begin{proof} |
|
726 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 |
|
728 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 |
|
730 we know that @{term "finals A"} must be finite, therefore there must be a finite |
|
731 set of regular expressions @{text "rs"} such that |
|
732 |
|
733 \begin{center} |
|
734 @{term "\<Union>(finals A) = L (\<Uplus>rs)"} |
|
735 \end{center} |
|
736 |
|
737 \noindent |
|
738 Since the left-hand side is equal to @{text A}, we can use @{term "\<Uplus>rs"} |
|
739 as the regular expression that solves the goal.\qed |
|
740 \end{proof} |
691 *} |
741 *} |
692 |
742 |
693 |
743 |
694 |
744 |
695 |
745 |