1309 simplification is done along the way, |
1310 simplification is done along the way, |
1310 the structure of nested alternatives is never created(we can |
1311 the structure of nested alternatives is never created(we can |
1311 actually prove that simplification function never allows nested |
1312 actually prove that simplification function never allows nested |
1312 alternatives to happen, more on this later). |
1313 alternatives to happen, more on this later). |
1313 |
1314 |
|
1315 How about we do not allow the function $\simp$ |
|
1316 to fuse out the bits when it is unnecessary? |
|
1317 Like, for the above regular expression, we might |
|
1318 just delete the outer layer of alternative |
|
1319 \begin{center} |
|
1320 \st{$ {\oplus[\ZERO \;,}$} $_{bs}\oplus \textit{rs}$ \st{$]$} |
|
1321 \end{center} |
|
1322 and get $_{bs}\oplus \textit{rs}$ instead, without |
|
1323 fusing the bits $\textit{bs}$ inside to every element |
|
1324 of $\textit{rs}$. |
|
1325 This idea can be realized by making the following |
|
1326 changes to the $\simp$-function: |
|
1327 \begin{center} |
|
1328 \begin{tabular}{@{}lcl@{}} |
|
1329 |
|
1330 $\textit{simp} \; (_{\textit{bs}}(a_1 \cdot a_2))$ & $\dn$ & $ (\textit{simp} \; a_1, \textit{simp} \; a_2) \; \textit{match} $ \\ |
|
1331 &&$\quad\textit{case} \; (\ZERO, \_) \Rightarrow \ZERO$ \\ |
|
1332 &&$\quad\textit{case} \; (\_, \ZERO) \Rightarrow \ZERO$ \\ |
|
1333 &&$\quad\textit{case} \; (\ONE, a_2') \Rightarrow \textit{fuse} \; bs \; a_2'$ \\ |
|
1334 &&$\quad\textit{case} \; (a_1', \ONE) \Rightarrow \textit{fuse} \; bs \; a_1'$ \\ |
|
1335 &&$\quad\textit{case} \; (a_1', a_2') \Rightarrow _{\textit{bs}}(a_1' \cdot a_2')$ \\ |
|
1336 |
|
1337 $\textit{simp} \; (bs_\oplus as)$ & $\dn$ & $\textit{distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $ \\ |
|
1338 &&$\quad\textit{case} \; [] \Rightarrow \ZERO$ \\ |
|
1339 &&$\quad\textit{case} \; a :: [] \Rightarrow \textit{fuse bs a}$ \\ |
|
1340 &&$\quad\textit{case} \; as' \Rightarrow \textit{ALTS}\;bs\;as'$\\ |
|
1341 |
|
1342 $\textit{simp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$ |
|
1343 \end{tabular} |
|
1344 \end{center} |
|
1345 |
|
1346 \noindent |
|
1347 |
1314 \subsection{Properties of the Function $\simp$} |
1348 \subsection{Properties of the Function $\simp$} |
1315 |
1349 |
1316 We have proved in Isabelle quite a few properties |
1350 We have proved in Isabelle quite a few properties |
1317 of the $\simp$-function, which helps the proof to go forward |
1351 of the $\simp$-function, which helps the proof to go forward |
1318 and we list them here to aid comprehension. |
1352 and we list them here to aid comprehension. |
1319 |
1353 |
1320 To start, we need a bit of auxiliary notations, |
1354 To start, we need a bit of auxiliary notations, |
1321 which is quite basic and is only written here |
1355 which is quite basic and is only written here |
1322 for clarity. |
1356 for clarity. |
1323 $\textit{sub}(r_1 \cdot r_2) \dn \textit{sub}(r_1) \cup \textit{sub}(r_2) \cup \{r\}$\\ |
1357 |
|
1358 $\textit{sub}(r)$ computes the set of the |
|
1359 sub-regular expression of $r$: |
|
1360 \begin{center} |
|
1361 $\textit{sub}(\ONE) \dn \{\ONE\}$\\ |
|
1362 $\textit{sub}(r_1 \cdot r_2) \dn \textit{sub}(r_1) \cup \textit{sub}(r_2) \cup \{r_1 \cdot r_2\}$\\ |
1324 $\textit{sub}(r_1 + r_2) \dn \textit{sub}(r_1) \cup \textit{sub}(r_2) \cup \{r_1+r_2\}$\\ |
1363 $\textit{sub}(r_1 + r_2) \dn \textit{sub}(r_1) \cup \textit{sub}(r_2) \cup \{r_1+r_2\}$\\ |
1325 |
1364 \end{center} |
1326 $\textit{good}(r) \dn r \neq \ZERO \land \\ |
1365 $\textit{good}(r) \dn r \neq \ZERO \land \\ |
1327 \forall r' \in \textit{sub}(r), \textit{if} \; r' = _{bs_1}\oplus(rs_1), \; |
1366 \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.\; |
1367 \textit{then} \nexists r'' \in \textit{rs}_1 \; s.t.\; |
1329 r'' = _{bs_2}\oplus \textit{rs}_2 $ |
1368 r'' = _{bs_2}\oplus \textit{rs}_2 $ |
1330 |
1369 |