147 Functions are much better supported in Isabelle/HOL, but they still lead to similar |
147 Functions are much better supported in Isabelle/HOL, but they still lead to similar |
148 problems as with graphs. Composing, for example, two non-deterministic automata in parallel |
148 problems as with graphs. Composing, for example, two non-deterministic automata in parallel |
149 requires also the formalisation of disjoint unions. Nipkow \cite{Nipkow98} |
149 requires also the formalisation of disjoint unions. Nipkow \cite{Nipkow98} |
150 dismisses for this the option of using identities, because it leads according to |
150 dismisses for this the option of using identities, because it leads according to |
151 him to ``messy proofs''. He |
151 him to ``messy proofs''. He |
152 opts for a variant of \eqref{disjointunion} using bitlists, but writes |
152 opts for a variant of \eqref{disjointunion} using bit lists, but writes |
153 |
153 |
154 \begin{quote} |
154 \begin{quote} |
155 \it% |
155 \it% |
156 \begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}} |
156 \begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}} |
157 `` & All lemmas appear obvious given a picture of the composition of automata\ldots |
157 `` & All lemmas appear obvious given a picture of the composition of automata\ldots |
480 @{text "X\<^isub>1 = \<calL>(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>i\<^isub>p, CHAR c\<^isub>i\<^isub>p) \<union> \<calL>(\<lambda>(EMPTY))"}. |
480 @{text "X\<^isub>1 = \<calL>(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>i\<^isub>p, CHAR c\<^isub>i\<^isub>p) \<union> \<calL>(\<lambda>(EMPTY))"}. |
481 \end{equation} |
481 \end{equation} |
482 |
482 |
483 \noindent |
483 \noindent |
484 The reason for adding the @{text \<lambda>}-marker to our initial equational system is |
484 The reason for adding the @{text \<lambda>}-marker to our initial equational system is |
485 to obtain this equation: it only holds with the marker since none of |
485 to obtain this equation: it only holds with the marker, since none of |
486 the other terms contain the empty string. |
486 the other terms contain the empty string. |
487 |
487 |
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 |
590 will be left in the system. However, we not just want to have any equation |
590 will be left in the system. However, we not just want to have any equation |
591 as being the last one, but the one for which we want to calculate the regular |
591 as being the last one, but the one for which we want to calculate the regular |
592 expression. Therefore we define the iteration step so that it chooses an |
592 expression. Therefore we define the iteration step so that it chooses an |
593 equation with an equivalence class that is not @{text X}. This allows us to |
593 equation with an equivalence class that is not @{text X}. This allows us to |
594 control, which equation will be the last. We use Hilbert's choice operator, |
594 control, which equation will be the last. We use Hilbert's choice operator, |
595 written @{text SOME}, to chose an equation to be eliminated in @{text ES}. |
595 written @{text SOME}, to choose an equation to be eliminated in @{text ES}. |
596 |
596 |
597 \begin{center} |
597 \begin{center} |
598 \begin{tabular}{rc@ {\hspace{4mm}}r@ {\hspace{1mm}}l} |
598 \begin{tabular}{rc@ {\hspace{4mm}}r@ {\hspace{1mm}}l} |
599 @{thm (lhs) Iter_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-4mm}}l}{@{text "let"}}\\ |
599 @{thm (lhs) Iter_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-4mm}}l}{@{text "let"}}\\ |
600 & & @{text "(Y, yrhs) ="} & @{term "SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y"} \\ |
600 & & @{text "(Y, yrhs) ="} & @{term "SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y"} \\ |
601 & & \multicolumn{2}{@ {\hspace{-4mm}}l}{@{text "in"}~~@{term "Remove ES Y yrhs"}}\\ |
601 & & \multicolumn{2}{@ {\hspace{-4mm}}l}{@{text "in"}~~@{term "Remove ES Y yrhs"}}\\ |
602 \end{tabular} |
602 \end{tabular} |
603 \end{center} |
603 \end{center} |
604 |
604 |
605 \noindent |
605 \noindent |
606 The last definition applies @{term Iter} over and over again a condition |
606 The last definition we need applies @{term Iter} over and over again until a condition |
607 @{text COND} is \emph{not} satisfied anymore. The condition states that there |
607 @{text COND} is \emph{not} satisfied anymore. The condition states that there |
608 are more than one equation in the equational system @{text ES}. The |
608 are more than one equation left in the equational system @{text ES}. For this |
609 iteration is defined in terms of HOL's @{text while}-operator as follows: |
609 we use Isabelle/HOL's @{text while}-operator as follows: |
610 |
610 |
611 \begin{center} |
611 \begin{center} |
612 @{thm Solve_def} |
612 @{thm Solve_def} |
613 \end{center} |
613 \end{center} |
614 |
614 |
615 \noindent |
615 \noindent |
616 We are not concerned here with the definition of this operator in this paper |
616 We are not concerned here with the definition of this operator |
617 (see \cite{BerghoferNipkow00}). |
617 (see \cite{BerghoferNipkow00}), but note that we eliminate |
618 |
618 in each @{const Iter}-step a single equation, and therefore |
619 \begin{center} |
619 have a well-founded termination order by taking the cardinality |
620 @{thm while_rule} |
620 of the equational system @{text ES}. This enables us to prove |
621 \end{center} |
621 properties about our definition of @{const Solve} called with |
|
622 our initial equational system @{term "Init (UNIV // \<approx>A)"} from ??? |
|
623 as follows: |
|
624 |
|
625 |
|
626 \begin{center} |
|
627 \begin{tabular}{l} |
|
628 @{term "invariant (Init (UNIV // \<approx>A))"} \\ |
|
629 @{term "\<forall>ES. invariant ES \<and> Cond ES \<longrightarrow> invariant (Iter X ES)"}\\ |
|
630 @{term "\<forall>ES. invariant ES \<and> Cond ES \<longrightarrow> card (Iter X ES) < card ES"}\\ |
|
631 @{term "\<forall>ES. invariant ES \<and> \<not> Cond ES \<longrightarrow> P ES"}\\ |
|
632 \hline |
|
633 \multicolumn{1}{c}{@{term "P (Solve X (Init (UNIV // \<approx>A)))"}} |
|
634 \end{tabular} |
|
635 \end{center} |
|
636 |
|
637 \noindent |
|
638 This principle states that given an invariant we can prove a property |
|
639 @{text "P"} involving @{const Solve}. For this we have to first show that the |
|
640 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}; |
|
642 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}, |
|
644 then the property must hold. |
|
645 |
|
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 |
|
648 that this equation satisfies also the invariant. The invariant is composed |
|
649 of several properties |
|
650 |
|
651 \begin{center} |
|
652 \begin{tabular}{rcl@ {\hspace{10mm}}l} |
|
653 @{text "invariant X ES"} & @{text "\<equiv>"} & |
|
654 @{term "finite ES"} & @{text "(finiteness)"}\\ |
|
655 & @{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)"}\\ |
|
657 & @{text "\<and>"} & @{thm (rhs) distinct_equas_def} & @{text "(distinctness)"}\\ |
|
658 & @{text "\<and>"} & @{thm (rhs) ardenable_def} & @{text "(ardenable)"}\\ |
|
659 \end{tabular} |
|
660 \end{center} |
|
661 |
622 *} |
662 *} |
623 |
663 |
624 |
664 |
625 |
665 |
626 |
666 |