213 We define rewriting relations for $\rrexp$s, which allows us to do the |
213 We define rewriting relations for $\rrexp$s, which allows us to do the |
214 same trick as we did for the correctness proof, |
214 same trick as we did for the correctness proof, |
215 but this time we will have stronger equalities established. |
215 but this time we will have stronger equalities established. |
216 \subsection{"hrewrite" relation} |
216 \subsection{"hrewrite" relation} |
217 List of 1-step rewrite rules for regular expressions simplification without bitcodes: |
217 List of 1-step rewrite rules for regular expressions simplification without bitcodes: |
218 \ |
218 \begin{center} |
219 |
219 \begin{tabular}{lcl} |
220 |
220 $r_1 \cdot \ZERO$ & $\rightarrow$ & $\ZERO$ |
221 |
221 \end{tabular} |
|
222 \end{center} |
|
223 |
|
224 And we define an "grewrite" relation that works on lists: |
|
225 \begin{center} |
|
226 \begin{tabular}{lcl} |
|
227 $ \ZERO :: rs$ & $\rightarrow_g$ & $rs$ |
|
228 \end{tabular} |
|
229 \end{center} |
|
230 |
|
231 |
|
232 |
|
233 With these relations we prove |
|
234 \begin{lemma} |
|
235 $rs \rightarrow rs' \implies \RALTS{rs} \rightarrow \RALTS{rs'}$ |
|
236 \end{lemma} |
|
237 which enables us to prove "closed forms" equalities such as |
|
238 \begin{lemma} |
|
239 $\sflat{(r_1 \cdot r_2) \backslash s} = \RALTS{ (r_1 \backslash s) \cdot r_2 :: (\map (r_2 \backslash \_) (\vsuf{s}{r_1}))}$ |
|
240 \end{lemma} |
|
241 |
|
242 But the most involved part of the above lemma is proving the following: |
|
243 \begin{lemma} |
|
244 $\bsimp{\RALTS{rs @ \RALTS{rs_1} @ rs'}} = \bsimp{\RALTS{rs @rs_1 @ rs'}} $ |
|
245 \end{lemma} |
|
246 which is needed in proving things like |
|
247 \begin{lemma} |
|
248 $r \rightarrow_f r' \implies \rsimp{r} \rightarrow \rsimp{r'}$ |
|
249 \end{lemma} |
|
250 . |
|
251 Fortunately this is provable by induction on the list $rs$ |
222 |
252 |
223 %---------------------------------------------------------------------------------------- |
253 %---------------------------------------------------------------------------------------- |
224 % SECTION ?? |
254 % SECTION ?? |
225 %---------------------------------------------------------------------------------------- |
255 %---------------------------------------------------------------------------------------- |
226 |
256 |