1302 generate the nested alternatives structure: |
1302 generate the nested alternatives structure: |
1303 \begin{center} |
1303 \begin{center} |
1304 $ \oplus[\ZERO \;, \; _{bs}\oplus \textit{rs} ]$ |
1304 $ \oplus[\ZERO \;, \; _{bs}\oplus \textit{rs} ]$ |
1305 \end{center} |
1305 \end{center} |
1306 and this will always trigger the $\flatten$ to |
1306 and this will always trigger the $\flatten$ to |
1307 spill out the sequence $\textit{bs}$, |
1307 spill out the inner alternative's bitcode $\textit{bs}$, |
1308 whereas when |
1308 whereas when |
1309 simplification is done along the way, |
1309 simplification is done along the way, |
1310 the structure of nested alternatives is never created(we can |
1310 the structure of nested alternatives is never created(we can |
1311 actually prove that simplification function never allows nested |
1311 actually prove that simplification function never allows nested |
1312 alternatives to happen, more on this later). |
1312 alternatives to happen, more on this later). |
|
1313 |
|
1314 \subsection{Properties of the Function $\simp$} |
|
1315 |
|
1316 We have proved in Isabelle quite a few properties |
|
1317 of the $\simp$-function, which helps the proof to go forward |
|
1318 and we list them here to aid comprehension. |
|
1319 |
|
1320 To start, we need a bit of auxiliary notations, |
|
1321 which is quite basic and is only written here |
|
1322 for clarity. |
|
1323 $\textit{sub}(r_1 \cdot r_2) \dn \textit{sub}(r_1) \cup \textit{sub}(r_2) \cup \{r\}$\\ |
|
1324 $\textit{sub}(r_1 + r_2) \dn \textit{sub}(r_1) \cup \textit{sub}(r_2) \cup \{r_1+r_2\}$\\ |
|
1325 |
|
1326 $\textit{good}(r) \dn r \neq \ZERO \land \\ |
|
1327 \forall r' \in \textit{sub}(r), \textit{if} \; r' = _{bs_1}\oplus(rs_1), \; |
|
1328 \textit{then} \nexists r'' \in \textit{rs}_1 \; s.t.\; |
|
1329 r'' = _{bs_2}\oplus \textit{rs}_2 $ |
|
1330 |
|
1331 The properties are mainly the ones below: |
|
1332 \begin{itemize} |
|
1333 \item |
|
1334 \begin{center} |
|
1335 $\simp(\simp(r)) = \simp(r)$ |
|
1336 \end{center} |
|
1337 \item |
|
1338 \begin{center} |
|
1339 $\textit{if} r = \simp(r') \textit{then} \; \textit{good}(r) $ |
|
1340 \end{center} |
|
1341 \end{itemize} |
1313 |
1342 |
1314 %CONSTRUCTION SITE HERE |
1343 %CONSTRUCTION SITE HERE |
1315 that is to say, despite the bits are being moved around on the regular expression |
1344 that is to say, despite the bits are being moved around on the regular expression |
1316 (difference in bits), the structure of the (unannotated)regular expression |
1345 (difference in bits), the structure of the (unannotated)regular expression |
1317 after one simplification is exactly the same after the |
1346 after one simplification is exactly the same after the |