regexp: comparison Paper/Paper.thy

equal deleted inserted replaced

-:6f4f9b7b9891
+:212bfa431fa5
 \end{definition}
 \noindent
 It is easy to see that @{term "\<approx>A"} is an equivalence relation, which
 partitions the set of all strings, @{text "UNIV"}, into a set of disjoint
-equivalence classes. To illustrate this quotient construction, let us give an
+equivalence classes. To illustrate this quotient construction, let us give a simple
 example: consider the regular language containing just
 the string @{text "[c]"}. The relation @{term "\<approx>({[c]})"} partitions @{text UNIV}
 into three equivalence classes @{text "X\<^isub>1"}, @{text "X\<^isub>2"} and  @{text "X\<^isub>3"}
 as follows
 \end{equation}
 \noindent
 The reason for adding the @{text \<lambda>}-marker to our initial equational system is
 to obtain this equation: it only holds with the marker, since none of
-the other terms contain the empty string.
+the other terms contain the empty string. The point of the initial equational system is
+that solving it means we will be able to extract a regular expression for every equivalence class.
 Our representation for the equations in Isabelle/HOL are pairs,
-where the first component is an equivalence class and the second component
+where the first component is an equivalence class (a set of strings)
+and the second component
 is a set of terms. Given a set of equivalence
 classes @{text CS}, our initial equational system @{term "Init CS"} is thus
 formally defined as
 %
 \begin{equation}\label{initcs}
 \end{lemma}
 \noindent
 Our proof of Thm.~\ref{myhillnerodeone} will proceed by transforming the
 initial equational system into one in \emph{solved form} maintaining the invariant
-in Lemma \ref{inv}. From the solved form we will be able to read
+in Lem.~\ref{inv}. From the solved form we will be able to read
 off the regular expressions.
 In order to transform an equational system into solved form, we have two
 operations: one that takes an equation of the form @{text "X = rhs"} and removes
-the recursive occurences of @{text X} in the @{text rhs} using our variant of Arden's
+any recursive occurences of @{text X} in the @{text rhs} using our variant of Arden's
 Lemma. The other operation takes an equation @{text "X = rhs"}
 and substitutes @{text X} throughout the rest of the equational system
 adjusting the remaining regular expressions approriately. To define this adjustment
-we define the \emph{append-operation}
+we define the \emph{append-operation} taking a term and a regular expression as argument
 \begin{center}
 @{thm append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\hspace{10mm}
 @{thm append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
 \end{center}
 \noindent
-which we also lift to entire right-hand sides of equations, written as
+We lift this operation to entire right-hand sides of equations, written as
 @{thm (lhs) append_rhs_rexp_def[where rexp="r"]}. With this we can define
 the \emph{arden-operation} for an equation of the form @{text "X = rhs"} as:
 \begin{center}
 \begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
 Finially, we can define how an equational system should be solved. For this
 we will need to iterate the process of eliminating equations until only one equation
 will be left in the system. However, we not just want to have any equation
 as being the last one, but the one involving the equivalence class for
 which we want to calculate the regular
-expression. Let us suppose the equivalence class is @{text X}.
+expression. Let us suppose this equivalence class is @{text X}.
 Since @{text X} is the one to be solved, in every iteration step we have to pick an
-equation to be eliminated that which is different from @{text X}. In this way
+equation to be eliminated that is different from @{text X}. In this way
-@{text X} is kept to the final step. The choice is implemented by Hilbert's choice
+@{text X} is kept to the final step. The choice is implemented using Hilbert's choice
 operator, written @{text SOME} in the definition below.
 \begin{center}
 \begin{tabular}{rc@ {\hspace{4mm}}r@ {\hspace{1mm}}l}
 @{thm (lhs) Iter_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-4mm}}l}{@{text "let"}}\\
 have a well-founded termination order by taking the cardinality
 of the equational system @{text ES}. This enables us to prove
 properties about our definition of @{const Solve} when we ``call'' it with
 the equivalence class @{text X} and the initial equational system
 @{term "Init (UNIV // \<approx>A)"} from
-\eqref{initcs}:
+\eqref{initcs} using the principle:
 \begin{center}
 \begin{tabular}{l}
 @{term "invariant (Init (UNIV // \<approx>A))"} \\
 step @{text "Iter"} preserves the the invariant as long as the condition @{term Cond} holds;
 third that @{text "Iter"} decreases the termination order, and fourth that
 once the condition does not hold anymore then the property @{text P} must hold.
 The property @{term P} in our proof will state that @{term "Solve X (Init (UNIV // \<approx>A))"}
-returns with a single equation @{text "X = xrhs"}, for some @{text "xrhs"} and
+returns with a single equation @{text "X = xrhs"} for some @{text "xrhs"}, and
 that this equational system still satisfies the invariant. In order to get
 the proof through, the invariant is composed of the following six properties:
 \begin{center}
 \begin{tabular}{@ {}rcl@ {\hspace{-13mm}}l @ {}}
 \end{tabular}
 \end{center}
 \noindent
 The first two ensure that the equational system is always finite (number of equations
-and number of terms in each equation); \ldots
+and number of terms in each equation); the second makes sure the ``meaning'' of the
+equations is preserved under our transformations. The other properties are a bit more
+technical, but are needed to get our proof through. Distinctness states that every
+equation in the system is distinct; @{text "ardenable"} ensures that we can always
+apply the arden operation. For this we have to make sure that in every @{text rhs},
+terms of the form @{term "Trn Y r"} cannot have a regular expresion that matches the
+empty string. Therefore @{text "rhs_nonempty"} is defined as
+\begin{center}
+@{thm rhs_nonempty_def}
+\end{center}
+\noindent
+The last property states that every @{text rhs} can only contain equivalence classes
+for which there is an equation. Therefore @{text lhss} is just the set containing
+the first components of an equational system,
+while @{text "rhss"} collects all equivalence classes @{text X} in the terms of the
+form @{term "Trn X r"} (that means @{thm (lhs) lhss_def}~@{text "\<equiv> {X | (X, rhs) \<in> ES}"}
+and @{thm (lhs) rhss_def}~@{text "\<equiv> {X | (X, r) \<in> rhs}"}).
 It is straightforward to prove that the inital equational system satisfies the
 invariant.
 \begin{lemma}

changeset 108	212bfa431fa5
parent 107	6f4f9b7b9891
child 109	79b37ef9505f