342 r::\rdistinct{rs}{(rset \cup \{r\})}$ |
342 r::\rdistinct{rs}{(rset \cup \{r\})}$ |
343 \end{tabular} |
343 \end{tabular} |
344 \end{center} |
344 \end{center} |
345 %TODO: definition of rsimp (maybe only the alternative clause) |
345 %TODO: definition of rsimp (maybe only the alternative clause) |
346 \noindent |
346 \noindent |
347 Notice there is a difference between our $\rdistincts$ and |
347 We would like to make clear |
348 the Isabelle $\textit {distinct}$ function. |
348 a difference between our $\rdistincts$ and |
349 In Isabelle $\textit{distinct}$ is a predicate |
349 the Isabelle $\textit {distinct}$ predicate. |
350 that tests if all the elements of a list are unique.\\ |
350 In Isabelle $\textit{distinct}$ is a function that returns a boolean |
351 With $\textit{rdistinct}$ one can chain together all the other modules |
351 rather than a list. |
|
352 It tests if all the elements of a list are unique.\\ |
|
353 With $\textit{rdistinct}$, |
|
354 and the flatten function for $\rrexp$s: |
|
355 \begin{center} |
|
356 \begin{tabular}{@{}lcl@{}} |
|
357 $\textit{rflts} \; (_{bs}\sum \textit{as}) :: \textit{as'}$ & $\dn$ & $(\textit{map} \; |
|
358 (\textit{fuse}\;bs)\; \textit{as}) \; @ \; \textit{rflts} \; as' $ \\ |
|
359 $\textit{rflts} \; \ZERO :: as'$ & $\dn$ & $ \textit{rflts} \; \textit{as'} $ \\ |
|
360 $\textit{rflts} \; a :: as'$ & $\dn$ & $a :: \textit{rflts} \; \textit{as'}$ \quad(otherwise) |
|
361 \end{tabular} |
|
362 \end{center} |
|
363 \noindent |
|
364 |
|
365 one can chain together all the other modules |
352 of $\bsimp{\_}$ (removing the functionalities related to bit-sequences) |
366 of $\bsimp{\_}$ (removing the functionalities related to bit-sequences) |
353 and get $\textit{rsimp}$ and $\rderssimp{\_}{\_}$. |
367 and get $\textit{rsimp}$ and $\rderssimp{\_}{\_}$. |
|
368 \begin{center} |
|
369 \begin{tabular}{@{}lcl@{}} |
|
370 |
|
371 $\textit{rsimp} \; (_{bs}a_1\cdot a_2)$ & $\dn$ & $ \textit{rsimp}_{ASEQ} \; bs \;(\textit{rsimp} \; a_1) \; (\textit{rsimp} \; a_2) $ \\ |
|
372 $\textit{rsimp} \; (_{bs}\sum \textit{as})$ & $\dn$ & $\textit{rsimp}_{ALTS} \; \textit{bs} \; (\textit{rdistinct} \; ( \textit{rflts} ( \textit{map} \; rsimp \; as)) \; \rerases \; \varnothing) $ \\ |
|
373 $\textit{rsimp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$ |
|
374 \end{tabular} |
|
375 \end{center} |
354 We omit these functions, as they are routine. Please refer to the formalisation |
376 We omit these functions, as they are routine. Please refer to the formalisation |
355 (in file BasicIdentities.thy) for the exact definition. |
377 (in file BasicIdentities.thy) for the exact definition. |
356 With $\rrexp$ the size caclulation of annotated regular expressions' |
378 With $\rrexp$ the size caclulation of annotated regular expressions' |
357 simplification and derivatives can be done by the size of their unlifted |
379 simplification and derivatives can be done by the size of their unlifted |
358 counterpart with the unlifted version of simplification and derivatives applied. |
380 counterpart with the unlifted version of simplification and derivatives applied. |