488 Our representation for the equations in Isabelle/HOL are pairs, |
488 Our representation for the equations in Isabelle/HOL are pairs, |
489 where the first component is an equivalence class and the second component |
489 where the first component is an equivalence class and the second component |
490 is a set of terms. Given a set of equivalence |
490 is a set of terms. Given a set of equivalence |
491 classes @{text CS}, our initial equational system @{term "Init CS"} is thus |
491 classes @{text CS}, our initial equational system @{term "Init CS"} is thus |
492 formally defined as |
492 formally defined as |
493 |
493 % |
494 \begin{center} |
494 \begin{equation}\label{initcs} |
495 \begin{tabular}{rcl} |
495 \mbox{\begin{tabular}{rcl} |
496 @{thm (lhs) Init_rhs_def} & @{text "\<equiv>"} & |
496 @{thm (lhs) Init_rhs_def} & @{text "\<equiv>"} & |
497 @{text "if"}~@{term "[] \<in> X"}\\ |
497 @{text "if"}~@{term "[] \<in> X"}\\ |
498 & & @{text "then"}~@{term "{Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X} \<union> {Lam EMPTY}"}\\ |
498 & & @{text "then"}~@{term "{Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X} \<union> {Lam EMPTY}"}\\ |
499 & & @{text "else"}~@{term "{Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}"}\\ |
499 & & @{text "else"}~@{term "{Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}"}\\ |
500 @{thm (lhs) Init_def} & @{text "\<equiv>"} & @{thm (rhs) Init_def} |
500 @{thm (lhs) Init_def} & @{text "\<equiv>"} & @{thm (rhs) Init_def} |
501 \end{tabular} |
501 \end{tabular}} |
502 \end{center} |
502 \end{equation} |
503 |
503 |
504 |
504 |
505 |
505 |
506 \noindent |
506 \noindent |
507 Because we use sets of terms |
507 Because we use sets of terms |
616 We are not concerned here with the definition of this operator |
616 We are not concerned here with the definition of this operator |
617 (see \cite{BerghoferNipkow00}), but note that we eliminate |
617 (see \cite{BerghoferNipkow00}), but note that we eliminate |
618 in each @{const Iter}-step a single equation, and therefore |
618 in each @{const Iter}-step a single equation, and therefore |
619 have a well-founded termination order by taking the cardinality |
619 have a well-founded termination order by taking the cardinality |
620 of the equational system @{text ES}. This enables us to prove |
620 of the equational system @{text ES}. This enables us to prove |
621 properties about our definition of @{const Solve} called with |
621 properties about our definition of @{const Solve} when we ``call'' it with |
622 our initial equational system @{term "Init (UNIV // \<approx>A)"} from ??? |
622 the equivalence class @{text X} and the initial equational system |
623 as follows: |
623 @{term "Init (UNIV // \<approx>A)"} from |
|
624 \eqref{initcs}: |
624 |
625 |
625 |
626 |
626 \begin{center} |
627 \begin{center} |
627 \begin{tabular}{l} |
628 \begin{tabular}{l} |
628 @{term "invariant (Init (UNIV // \<approx>A))"} \\ |
629 @{term "invariant (Init (UNIV // \<approx>A))"} \\ |
633 \multicolumn{1}{c}{@{term "P (Solve X (Init (UNIV // \<approx>A)))"}} |
634 \multicolumn{1}{c}{@{term "P (Solve X (Init (UNIV // \<approx>A)))"}} |
634 \end{tabular} |
635 \end{tabular} |
635 \end{center} |
636 \end{center} |
636 |
637 |
637 \noindent |
638 \noindent |
638 This principle states that given an invariant we can prove a property |
639 This principle states that given an invariant (which we will specify below) |
639 @{text "P"} involving @{const Solve}. For this we have to first show that the |
640 we can prove a property |
|
641 @{text "P"} involving @{const Solve}. For this we have to discharge the following |
|
642 proof obligations: first the |
640 initial equational system satisfies the invariant; second that the iteration |
643 initial equational system satisfies the invariant; second that the iteration |
641 step @{text "Iter"} preserves the the invariant as long as the condition @{term Cond}; |
644 step @{text "Iter"} preserves the the invariant as long as the condition @{term Cond} holds; |
642 third that @{text "Iter"} decreases the termination order, and fourth that |
645 third that @{text "Iter"} decreases the termination order, and fourth that |
643 once the condition does not hold for an invariant equational system @{text ES}, |
646 once the condition does not hold anymore then the property @{text P} must hold. |
644 then the property must hold. |
647 |
645 |
648 The property @{term P} in our proof will state that @{term "Solve X (Init (UNIV // \<approx>A))"} |
646 The property @{term P} we will show states that @{term "Solve X (Init (UNIV // \<approx>A))"} |
|
647 returns with a single equation @{text "X = xrhs"}, for some @{text "xrhs"} and |
649 returns with a single equation @{text "X = xrhs"}, for some @{text "xrhs"} and |
648 that this equation satisfies also the invariant. The invariant is composed |
650 that this equational system still satisfies the invariant. In order to get |
649 of several properties |
651 the proof through, the invariant is composed of the following six properties: |
650 |
652 |
651 \begin{center} |
653 \begin{center} |
652 \begin{tabular}{rcl@ {\hspace{10mm}}l} |
654 \begin{tabular}{@ {}rcl@ {\hspace{-13mm}}l @ {}} |
653 @{text "invariant X ES"} & @{text "\<equiv>"} & |
655 @{text "invariant ES"} & @{text "\<equiv>"} & |
654 @{term "finite ES"} & @{text "(finiteness)"}\\ |
656 @{term "finite ES"} & @{text "(finiteness)"}\\ |
655 & @{text "\<and>"} & @{thm (rhs) finite_rhs_def} & @{text "(finiteness rhs)"}\\ |
657 & @{text "\<and>"} & @{thm (rhs) finite_rhs_def} & @{text "(finiteness rhs)"}\\ |
656 & @{text "\<and>"} & @{text "\<forall>(X, rhs)\<in>ES. X = \<Union>\<calL> ` rhs"} & @{text "(validity)"}\\ |
658 & @{text "\<and>"} & @{text "\<forall>(X, rhs)\<in>ES. X = \<Union>\<calL> ` rhs"} & @{text "(soundness)"}\\ |
657 & @{text "\<and>"} & @{thm (rhs) distinct_equas_def} & @{text "(distinctness)"}\\ |
659 & @{text "\<and>"} & @{thm (rhs) distinct_equas_def}\\ |
|
660 & & & @{text "(distinctness)"}\\ |
658 & @{text "\<and>"} & @{thm (rhs) ardenable_def} & @{text "(ardenable)"}\\ |
661 & @{text "\<and>"} & @{thm (rhs) ardenable_def} & @{text "(ardenable)"}\\ |
|
662 & @{text "\<and>"} & @{thm (rhs) valid_eqs_def} & @{text "(validity)"}\\ |
659 \end{tabular} |
663 \end{tabular} |
660 \end{center} |
664 \end{center} |
661 |
665 |
|
666 \noindent |
|
667 The first two ensure that the equational system is always finite (number of equations |
|
668 and number of terms in each equation); \ldots |
|
669 |
|
670 \begin{lemma} |
|
671 @{thm[mode=IfThen] Init_ES_satisfies_invariant} |
|
672 \end{lemma} |
|
673 |
|
674 \begin{lemma} |
|
675 @{thm[mode=IfThen] iteration_step_invariant[where xrhs="rhs"]} |
|
676 \end{lemma} |
|
677 |
|
678 \begin{lemma} |
|
679 @{thm[mode=IfThen] iteration_step_measure[simplified (no_asm), where xrhs="rhs"]} |
|
680 \end{lemma} |
|
681 |
|
682 \begin{lemma} |
|
683 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)}"} |
|
685 and @{term "invariant {(X, rhs)}"}. |
|
686 \end{lemma} |
|
687 |
|
688 \begin{theorem} |
|
689 @{thm[mode=IfThen] Myhill_Nerode1} |
|
690 \end{theorem} |
662 *} |
691 *} |
663 |
692 |
664 |
693 |
665 |
694 |
666 |
695 |