diff -r 62f8fa03863e -r fa92124d1fb7 ChengsongTanPhdThesis/Chapters/Finite.tex --- a/ChengsongTanPhdThesis/Chapters/Finite.tex Fri Sep 02 19:18:50 2022 +0100 +++ b/ChengsongTanPhdThesis/Chapters/Finite.tex Fri Sep 02 19:35:55 2022 +0100 @@ -344,13 +344,35 @@ \end{center} %TODO: definition of rsimp (maybe only the alternative clause) \noindent -Notice there is a difference between our $\rdistincts$ and -the Isabelle $\textit {distinct}$ function. -In Isabelle $\textit{distinct}$ is a predicate -that tests if all the elements of a list are unique.\\ -With $\textit{rdistinct}$ one can chain together all the other modules +We would like to make clear +a difference between our $\rdistincts$ and +the Isabelle $\textit {distinct}$ predicate. +In Isabelle $\textit{distinct}$ is a function that returns a boolean +rather than a list. +It tests if all the elements of a list are unique.\\ +With $\textit{rdistinct}$, +and the flatten function for $\rrexp$s: + \begin{center} + \begin{tabular}{@{}lcl@{}} + $\textit{rflts} \; (_{bs}\sum \textit{as}) :: \textit{as'}$ & $\dn$ & $(\textit{map} \; + (\textit{fuse}\;bs)\; \textit{as}) \; @ \; \textit{rflts} \; as' $ \\ + $\textit{rflts} \; \ZERO :: as'$ & $\dn$ & $ \textit{rflts} \; \textit{as'} $ \\ + $\textit{rflts} \; a :: as'$ & $\dn$ & $a :: \textit{rflts} \; \textit{as'}$ \quad(otherwise) +\end{tabular} +\end{center} +\noindent + +one can chain together all the other modules of $\bsimp{\_}$ (removing the functionalities related to bit-sequences) and get $\textit{rsimp}$ and $\rderssimp{\_}{\_}$. +\begin{center} + \begin{tabular}{@{}lcl@{}} + + $\textit{rsimp} \; (_{bs}a_1\cdot a_2)$ & $\dn$ & $ \textit{rsimp}_{ASEQ} \; bs \;(\textit{rsimp} \; a_1) \; (\textit{rsimp} \; a_2) $ \\ + $\textit{rsimp} \; (_{bs}\sum \textit{as})$ & $\dn$ & $\textit{rsimp}_{ALTS} \; \textit{bs} \; (\textit{rdistinct} \; ( \textit{rflts} ( \textit{map} \; rsimp \; as)) \; \rerases \; \varnothing) $ \\ + $\textit{rsimp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$ +\end{tabular} +\end{center} We omit these functions, as they are routine. Please refer to the formalisation (in file BasicIdentities.thy) for the exact definition. With $\rrexp$ the size caclulation of annotated regular expressions'