regexp: comparison Paper/Paper.thy

equal deleted inserted replaced

-:91dc591de63f
+:6f4f9b7b9891
 \end{tabular}
 \end{center}
 \noindent
 Finially, we can define how an equational system should be solved. For this
-we will need to iterate the elimination of an equation until only one equation
+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 for which we want to calculate the regular
+as being the last one, but the one involving the equivalence class for
-expression. Therefore we define the iteration step so that it chooses an
+which we want to calculate the regular
-equation with an equivalence class that is not @{text X}. This allows us to
+expression. Let us suppose the equivalence class is @{text X}.
-control, which equation will be the last. We use Hilbert's choice operator,
+Since @{text X} is the one to be solved, in every iteration step we have to pick an
-written @{text SOME}, to choose an equation to be eliminated in @{text ES}.
+equation to be eliminated that which is different from @{text X}. In this way
+@{text X} is kept to the final step. The choice is implemented by 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"}}\\
 & & @{text "(Y, yrhs) ="} & @{term "SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y"} \\
 \begin{lemma}
 @{thm[mode=IfThen] iteration_step_invariant[where xrhs="rhs"]}
 \end{lemma}
+\begin{proof}
+???
+\end{proof}
 \begin{lemma}
 @{thm[mode=IfThen] iteration_step_measure[simplified (no_asm), where xrhs="rhs"]}
 \end{lemma}
 \begin{proof}
 \begin{lemma}
 If @{thm (prem 1) Solve} and @{thm (prem 2) Solve} then there exists
 a @{text rhs} such that  @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"}
 and @{term "invariant {(X, rhs)}"}.
 \end{lemma}
+\begin{proof}
+???
+\end{proof}
 \noindent
 With this lemma in place we can show that for every equivalence class in @{term "UNIV // \<approx>A"}
 there exists a regular expression.
 @{term "\<Union>(finals A) = L (\<Uplus>rs)"}
 \end{center}
 \noindent
 Since the left-hand side is equal to @{text A}, we can use @{term "\<Uplus>rs"}
-as the regular expression that solves the goal.\qed
+as the regular expression that is needed in the theorem.\qed
 \end{proof}
 *}

changeset 107	6f4f9b7b9891
parent 106	91dc591de63f
child 108	212bfa431fa5