129 *) |
129 *) |
130 |
130 |
131 |
131 |
132 (*>*) |
132 (*>*) |
133 |
133 |
134 |
134 section\<open>Core of the proof\<close> |
135 |
|
136 section \<open>Introduction\<close> |
|
137 |
|
138 |
|
139 text \<open> |
135 text \<open> |
140 Trying out after lualatex. |
136 This paper builds on previous work by Ausaf and Urban using |
141 |
|
142 |
|
143 uhuhuhu |
|
144 This works builds on previous work by Ausaf and Urban using |
|
145 regular expression'd bit-coded derivatives to do lexing that |
137 regular expression'd bit-coded derivatives to do lexing that |
146 is both fast and satisfied the POSIX specification. |
138 is both fast and satisfies the POSIX specification. |
147 In their work, a bit-coded algorithm introduced by Sulzmann and Lu |
139 In their work, a bit-coded algorithm introduced by Sulzmann and Lu |
148 was formally verified in Isabelle, by a very clever use of |
140 was formally verified in Isabelle, by a very clever use of |
149 flex function and retrieve to carefully mimic the way a value is |
141 flex function and retrieve to carefully mimic the way a value is |
150 built up by the injection funciton. |
142 built up by the injection funciton. |
151 |
143 |
152 In the previous work, Ausaf and Urban established the below equality: |
144 In the previous work, Ausaf and Urban established the below equality: |
153 \begin{lemma} |
145 \begin{lemma} |
154 @{thm [mode=IfThen] bder_retrieve} |
146 @{thm [mode=IfThen] MAIN_decode} |
155 \end{lemma} |
147 \end{lemma} |
156 |
148 |
157 This lemma links the regular expression |
149 This lemma establishes a link with the lexer without bit-codes. |
|
150 |
|
151 With it we get the correctness of bit-coded algorithm. |
|
152 \begin{lemma} |
|
153 @{thm [mode=IfThen] blexer_correctness} |
|
154 \end{lemma} |
|
155 |
|
156 However what is not certain is whether we can add simplification |
|
157 to the bit-coded algorithm, without breaking the correct lexing output. |
|
158 |
|
159 |
|
160 The reason that we do need to add a simplification phase |
|
161 after each derivative step of $\textit{blexer}$ is |
|
162 because it produces intermediate |
|
163 regular expressions that can grow exponentially. |
|
164 For example, the regular expression $(a+aa)^*$ after taking |
|
165 derivative against just 10 $a$s will have size 8192. |
|
166 |
|
167 %TODO: add figure for this? |
|
168 |
|
169 |
|
170 Therefore, we insert a simplification phase |
|
171 after each derivation step, as defined below: |
|
172 \begin{lemma} |
|
173 @{thm blexer_simp_def} |
|
174 \end{lemma} |
|
175 |
|
176 The simplification function is given as follows: |
|
177 |
|
178 \begin{center} |
|
179 \begin{tabular}{lcl} |
|
180 @{thm (lhs) bsimp.simps(1)[of "bs" "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bsimp.simps(1)[of "bs" "r\<^sub>1" "r\<^sub>2"]}\\ |
|
181 @{thm (lhs) bsimp.simps(2)} & $\dn$ & @{thm (rhs) bsimp.simps(2)}\\ |
|
182 @{thm (lhs) bsimp.simps(3)} & $\dn$ & @{thm (rhs) bsimp.simps(3)}\\ |
|
183 |
|
184 \end{tabular} |
|
185 \end{center} |
|
186 |
|
187 And the two helper functions are: |
|
188 \begin{center} |
|
189 \begin{tabular}{lcl} |
|
190 @{thm (lhs) bsimp_AALTs.simps(2)[of "bs\<^sub>1" "r" ]} & $\dn$ & @{thm (rhs) bsimp.simps(1)[of "bs\<^sub>1" "r" ]}\\ |
|
191 @{thm (lhs) bsimp_AALTs.simps(2)} & $\dn$ & @{thm (rhs) bsimp.simps(2)}\\ |
|
192 @{thm (lhs) bsimp_AALTs.simps(3)} & $\dn$ & @{thm (rhs) bsimp.simps(3)}\\ |
|
193 |
|
194 \end{tabular} |
|
195 \end{center} |
|
196 |
|
197 |
|
198 This might sound trivial in the case of producing a YES/NO answer, |
|
199 but once we require a lexing output to be produced (which is required |
|
200 in applications like compiler front-end, malicious attack domain extraction, |
|
201 etc.), it is not straightforward if we still extract what is needed according |
|
202 to the POSIX standard. |
|
203 |
|
204 |
|
205 |
|
206 |
|
207 |
|
208 By simplification, we mean specifically the following rules: |
|
209 |
|
210 \begin{center} |
|
211 \begin{tabular}{lcl} |
|
212 @{thm[mode=Axiom] rrewrite.intros(1)[of "bs" "r\<^sub>2"]}\\ |
|
213 @{thm[mode=Axiom] rrewrite.intros(2)[of "bs" "r\<^sub>1"]}\\ |
|
214 @{thm[mode=Axiom] rrewrite.intros(3)[of "bs" "bs\<^sub>1" "r\<^sub>1"]}\\ |
|
215 @{thm[mode=Rule] rrewrite.intros(4)[of "r\<^sub>1" "r\<^sub>2" "bs" "r\<^sub>3"]}\\ |
|
216 @{thm[mode=Rule] rrewrite.intros(5)[of "r\<^sub>3" "r\<^sub>4" "bs" "r\<^sub>1"]}\\ |
|
217 @{thm[mode=Rule] rrewrite.intros(6)[of "r" "r'" "bs" "rs\<^sub>1" "rs\<^sub>2"]}\\ |
|
218 @{thm[mode=Axiom] rrewrite.intros(7)[of "bs" "rs\<^sub>a" "rs\<^sub>b"]}\\ |
|
219 @{thm[mode=Axiom] rrewrite.intros(8)[of "bs" "rs\<^sub>a" "bs\<^sub>1" "rs\<^sub>1" "rs\<^sub>b"]}\\ |
|
220 @{thm[mode=Axiom] rrewrite.intros(9)[of "bs" "bs\<^sub>1" "rs"]}\\ |
|
221 @{thm[mode=Axiom] rrewrite.intros(10)[of "bs" ]}\\ |
|
222 @{thm[mode=Axiom] rrewrite.intros(11)[of "bs" "r\<^sub>1"]}\\ |
|
223 @{thm[mode=Rule] rrewrite.intros(12)[of "a\<^sub>1" "a\<^sub>2" "bs" "rs\<^sub>a" "rs\<^sub>b" "rs\<^sub>c"]}\\ |
|
224 |
|
225 \end{tabular} |
|
226 \end{center} |
|
227 |
|
228 |
|
229 And these can be made compact by the following simplification function: |
|
230 |
|
231 where the function $\mathit{bsimp_AALTs}$ |
|
232 |
|
233 The core idea of the proof is that two regular expressions, |
|
234 if "isomorphic" up to a finite number of rewrite steps, will |
|
235 remain "isomorphic" when we take the same sequence of |
|
236 derivatives on both of them. |
|
237 This can be expressed by the following rewrite relation lemma: |
|
238 \begin{lemma} |
|
239 @{thm [mode=IfThen] central} |
|
240 \end{lemma} |
|
241 |
|
242 This isomorphic relation implies a property that leads to the |
|
243 correctness result: |
|
244 if two (nullable) regular expressions are "rewritable" in many steps |
|
245 from one another, |
|
246 then a call to function $\textit{bmkeps}$ gives the same |
|
247 bit-sequence : |
|
248 \begin{lemma} |
|
249 @{thm [mode=IfThen] rewrites_bmkeps} |
|
250 \end{lemma} |
|
251 |
|
252 Given the same bit-sequence, the decode function |
|
253 will give out the same value, which is the output |
|
254 of both lexers: |
|
255 \begin{lemma} |
|
256 @{thm blexer_def} |
|
257 \end{lemma} |
|
258 |
|
259 \begin{lemma} |
|
260 @{thm blexer_simp_def} |
|
261 \end{lemma} |
|
262 |
|
263 And that yields the correctness result: |
|
264 \begin{lemma} |
|
265 @{thm blexersimp_correctness} |
|
266 \end{lemma} |
|
267 |
|
268 The nice thing about the aove |
|
269 \<close> |
|
270 |
|
271 |
|
272 |
|
273 section \<open>Introduction\<close> |
|
274 |
|
275 |
|
276 text \<open> |
|
277 |
158 |
278 |
159 Brzozowski \cite{Brzozowski1964} introduced the notion of the {\em |
279 Brzozowski \cite{Brzozowski1964} introduced the notion of the {\em |
160 derivative} @{term "der c r"} of a regular expression \<open>r\<close> w.r.t.\ |
280 derivative} @{term "der c r"} of a regular expression \<open>r\<close> w.r.t.\ |
161 a character~\<open>c\<close>, and showed that it gave a simple solution to the |
281 a character~\<open>c\<close>, and showed that it gave a simple solution to the |
162 problem of matching a string @{term s} with a regular expression @{term |
282 problem of matching a string @{term s} with a regular expression @{term |
1414 |
1537 |
1415 \begin{center} |
1538 \begin{center} |
1416 @{thm lexer_flex} |
1539 @{thm lexer_flex} |
1417 \end{center} |
1540 \end{center} |
1418 |
1541 |
1419 \begin{center} |
|
1420 \begin{tabular}{lcl} |
|
1421 @{thm (lhs) code.simps(1)} & $\dn$ & @{thm (rhs) code.simps(1)}\\ |
|
1422 @{thm (lhs) code.simps(2)} & $\dn$ & @{thm (rhs) code.simps(2)}\\ |
|
1423 @{thm (lhs) code.simps(3)} & $\dn$ & @{thm (rhs) code.simps(3)}\\ |
|
1424 @{thm (lhs) code.simps(4)} & $\dn$ & @{thm (rhs) code.simps(4)}\\ |
|
1425 @{thm (lhs) code.simps(5)[of "v\<^sub>1" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) code.simps(5)[of "v\<^sub>1" "v\<^sub>2"]}\\ |
|
1426 @{thm (lhs) code.simps(6)} & $\dn$ & @{thm (rhs) code.simps(6)}\\ |
|
1427 @{thm (lhs) code.simps(7)} & $\dn$ & @{thm (rhs) code.simps(7)} |
|
1428 \end{tabular} |
|
1429 \end{center} |
|
1430 |
|
1431 \begin{center} |
|
1432 \begin{tabular}{lcl} |
|
1433 @{term areg} & $::=$ & @{term "AZERO"}\\ |
|
1434 & $\mid$ & @{term "AONE bs"}\\ |
|
1435 & $\mid$ & @{term "ACH bs c"}\\ |
|
1436 & $\mid$ & @{term "AALT bs r1 r2"}\\ |
|
1437 & $\mid$ & @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}\\ |
|
1438 & $\mid$ & @{term "ASTAR bs r"} |
|
1439 \end{tabular} |
|
1440 \end{center} |
|
1441 |
|
1442 |
|
1443 \begin{center} |
|
1444 \begin{tabular}{lcl} |
|
1445 @{thm (lhs) intern.simps(1)} & $\dn$ & @{thm (rhs) intern.simps(1)}\\ |
|
1446 @{thm (lhs) intern.simps(2)} & $\dn$ & @{thm (rhs) intern.simps(2)}\\ |
|
1447 @{thm (lhs) intern.simps(3)} & $\dn$ & @{thm (rhs) intern.simps(3)}\\ |
|
1448 @{thm (lhs) intern.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) intern.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\ |
|
1449 @{thm (lhs) intern.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) intern.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\ |
|
1450 @{thm (lhs) intern.simps(6)} & $\dn$ & @{thm (rhs) intern.simps(6)}\\ |
|
1451 \end{tabular} |
|
1452 \end{center} |
|
1453 |
|
1454 \begin{center} |
|
1455 \begin{tabular}{lcl} |
|
1456 @{thm (lhs) erase.simps(1)} & $\dn$ & @{thm (rhs) erase.simps(1)}\\ |
|
1457 @{thm (lhs) erase.simps(2)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(2)[of bs]}\\ |
|
1458 @{thm (lhs) erase.simps(3)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(3)[of bs]}\\ |
|
1459 @{thm (lhs) erase.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) erase.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
1460 @{thm (lhs) erase.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) erase.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
1461 @{thm (lhs) erase.simps(6)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(6)[of bs]}\\ |
|
1462 \end{tabular} |
|
1463 \end{center} |
|
1464 |
|
1465 Some simple facts about erase |
|
1466 |
|
1467 \begin{lemma}\mbox{}\\ |
|
1468 @{thm erase_bder}\\ |
|
1469 @{thm erase_intern} |
|
1470 \end{lemma} |
|
1471 |
|
1472 \begin{center} |
|
1473 \begin{tabular}{lcl} |
|
1474 @{thm (lhs) bnullable.simps(1)} & $\dn$ & @{thm (rhs) bnullable.simps(1)}\\ |
|
1475 @{thm (lhs) bnullable.simps(2)} & $\dn$ & @{thm (rhs) bnullable.simps(2)}\\ |
|
1476 @{thm (lhs) bnullable.simps(3)} & $\dn$ & @{thm (rhs) bnullable.simps(3)}\\ |
|
1477 @{thm (lhs) bnullable.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bnullable.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
1478 @{thm (lhs) bnullable.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bnullable.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
1479 @{thm (lhs) bnullable.simps(6)} & $\dn$ & @{thm (rhs) bnullable.simps(6)}\medskip\\ |
|
1480 |
|
1481 % \end{tabular} |
|
1482 % \end{center} |
|
1483 |
|
1484 % \begin{center} |
|
1485 % \begin{tabular}{lcl} |
|
1486 |
|
1487 @{thm (lhs) bder.simps(1)} & $\dn$ & @{thm (rhs) bder.simps(1)}\\ |
|
1488 @{thm (lhs) bder.simps(2)} & $\dn$ & @{thm (rhs) bder.simps(2)}\\ |
|
1489 @{thm (lhs) bder.simps(3)} & $\dn$ & @{thm (rhs) bder.simps(3)}\\ |
|
1490 @{thm (lhs) bder.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bder.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
1491 @{thm (lhs) bder.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bder.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
1492 @{thm (lhs) bder.simps(6)} & $\dn$ & @{thm (rhs) bder.simps(6)} |
|
1493 \end{tabular} |
|
1494 \end{center} |
|
1495 |
|
1496 |
|
1497 \begin{center} |
|
1498 \begin{tabular}{lcl} |
|
1499 @{thm (lhs) bmkeps.simps(1)} & $\dn$ & @{thm (rhs) bmkeps.simps(1)}\\ |
|
1500 @{thm (lhs) bmkeps.simps(2)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bmkeps.simps(2)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
1501 @{thm (lhs) bmkeps.simps(3)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bmkeps.simps(3)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
1502 @{thm (lhs) bmkeps.simps(4)} & $\dn$ & @{thm (rhs) bmkeps.simps(4)}\medskip\\ |
|
1503 \end{tabular} |
|
1504 \end{center} |
|
1505 |
|
1506 |
|
1507 @{thm [mode=IfThen] bder_retrieve} |
|
1508 |
|
1509 By induction on \<open>r\<close> |
|
1510 |
|
1511 \begin{theorem}[Main Lemma]\mbox{}\\ |
|
1512 @{thm [mode=IfThen] MAIN_decode} |
|
1513 \end{theorem} |
|
1514 |
|
1515 \noindent |
|
1516 Definition of the bitcoded lexer |
|
1517 |
|
1518 @{thm blexer_def} |
|
1519 |
|
1520 |
|
1521 \begin{theorem} |
|
1522 @{thm blexer_correctness} |
|
1523 \end{theorem} |
|
1524 |
1542 |
1525 \<close> |
1543 \<close> |
1526 |
1544 |
1527 section \<open>Optimisations\<close> |
1545 section \<open>Optimisations\<close> |
1528 |
1546 |
1975 |
1993 |
1976 |
1994 |
1977 section \<open>HERE\<close> |
1995 section \<open>HERE\<close> |
1978 |
1996 |
1979 text \<open> |
1997 text \<open> |
1980 \begin{center} |
|
1981 \begin{tabular}{llcl} |
|
1982 1) & @{thm (lhs) erase.simps(1)} & $\dn$ & @{thm (rhs) erase.simps(1)}\\ |
|
1983 2) & @{thm (lhs) erase.simps(2)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(2)[of bs]}\\ |
|
1984 3) & @{thm (lhs) erase.simps(3)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(3)[of bs]}\\ |
|
1985 4a) & @{term "erase (AALTs bs [])"} & $\dn$ & @{term ZERO}\\ |
|
1986 4b) & @{term "erase (AALTs bs [r])"} & $\dn$ & @{term "erase r"}\\ |
|
1987 4c) & @{term "erase (AALTs bs (r\<^sub>1#r\<^sub>2#rs))"} & $\dn$ & |
|
1988 @{term "ALT (erase r\<^sub>1) (erase (AALTs bs (r\<^sub>2#rs)))"}\\ |
|
1989 5) & @{thm (lhs) erase.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) erase.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
1990 6) & @{thm (lhs) erase.simps(6)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(6)[of bs]}\\ |
|
1991 \end{tabular} |
|
1992 \end{center} |
|
1993 |
1998 |
1994 \begin{lemma} |
1999 \begin{lemma} |
1995 @{thm [mode=IfThen] bder_retrieve} |
2000 @{thm [mode=IfThen] bder_retrieve} |
1996 \end{lemma} |
2001 \end{lemma} |
1997 |
2002 |
1998 \begin{proof} |
2003 \begin{proof} |
1999 By induction on the definition of @{term "erase r"}. The cases for rule 1) and 2) are |
2004 By induction on the definition of @{term "erase r"}. The cases for rule 1) and 2) are |
2000 straightforward as @{term "der c ZERO"} and @{term "der c ONE"} are both equal to |
2005 straightforward as @{term "der c ZERO"} and @{term "der c ONE"} are both equal to |
2001 @{term ZERO}. This means @{term "\<Turnstile> v : ZERO"} cannot hold. Similarly in case of rule 3) |
2006 @{term ZERO}. This means @{term "\<Turnstile> v : ZERO"} cannot hold. Similarly in case of rule 3) |
2002 where @{term r} is of the form @{term "ACH d"} with @{term "c = d"}. Then by assumption |
2007 where @{term r} is of the form @{term "ACHAR d"} with @{term "c = d"}. Then by assumption |
2003 we know @{term "\<Turnstile> v : ONE"}, which implies @{term "v = Void"}. The equation follows by |
2008 we know @{term "\<Turnstile> v : ONE"}, which implies @{term "v = Void"}. The equation follows by |
2004 simplification of left- and right-hand side. In case @{term "c \<noteq> d"} we have again |
2009 simplification of left- and right-hand side. In case @{term "c \<noteq> d"} we have again |
2005 @{term "\<Turnstile> v : ZERO"}, which cannot hold. |
2010 @{term "\<Turnstile> v : ZERO"}, which cannot hold. |
2006 |
2011 |
2007 For rule 4a) we have again @{term "\<Turnstile> v : ZERO"}. The property holds by IH for rule 4b). |
2012 For rule 4a) we have again @{term "\<Turnstile> v : ZERO"}. The property holds by IH for rule 4b). |
2038 \] |
2043 \] |
2039 We can move out the @{term "fuse [Z]"} and then use the IH to show that left-hand side |
2044 We can move out the @{term "fuse [Z]"} and then use the IH to show that left-hand side |
2040 and right-hand side are equal. This completes the proof. |
2045 and right-hand side are equal. This completes the proof. |
2041 \end{proof} |
2046 \end{proof} |
2042 |
2047 |
2043 |
2048 |
2044 |
2049 |
2045 \bibliographystyle{plain} |
2050 \bibliographystyle{plain} |
2046 \bibliography{root} |
2051 \bibliography{root} |
2047 |
2052 |
2048 \<close> |
2053 \<close> |
2049 (*<*) |
2054 (*<*) |
2050 end |
2055 end |
2051 (*>*) |
2056 (*>*) |
|
2057 |
|
2058 (* |
|
2059 |
|
2060 \begin{center} |
|
2061 \begin{tabular}{lcl} |
|
2062 @{thm (lhs) code.simps(1)} & $\dn$ & @{thm (rhs) code.simps(1)}\\ |
|
2063 @{thm (lhs) code.simps(2)} & $\dn$ & @{thm (rhs) code.simps(2)}\\ |
|
2064 @{thm (lhs) code.simps(3)} & $\dn$ & @{thm (rhs) code.simps(3)}\\ |
|
2065 @{thm (lhs) code.simps(4)} & $\dn$ & @{thm (rhs) code.simps(4)}\\ |
|
2066 @{thm (lhs) code.simps(5)[of "v\<^sub>1" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) code.simps(5)[of "v\<^sub>1" "v\<^sub>2"]}\\ |
|
2067 @{thm (lhs) code.simps(6)} & $\dn$ & @{thm (rhs) code.simps(6)}\\ |
|
2068 @{thm (lhs) code.simps(7)} & $\dn$ & @{thm (rhs) code.simps(7)} |
|
2069 \end{tabular} |
|
2070 \end{center} |
|
2071 |
|
2072 \begin{center} |
|
2073 \begin{tabular}{lcl} |
|
2074 @{term areg} & $::=$ & @{term "AZERO"}\\ |
|
2075 & $\mid$ & @{term "AONE bs"}\\ |
|
2076 & $\mid$ & @{term "ACHAR bs c"}\\ |
|
2077 & $\mid$ & @{term "AALT bs r1 r2"}\\ |
|
2078 & $\mid$ & @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}\\ |
|
2079 & $\mid$ & @{term "ASTAR bs r"} |
|
2080 \end{tabular} |
|
2081 \end{center} |
|
2082 |
|
2083 |
|
2084 \begin{center} |
|
2085 \begin{tabular}{lcl} |
|
2086 @{thm (lhs) intern.simps(1)} & $\dn$ & @{thm (rhs) intern.simps(1)}\\ |
|
2087 @{thm (lhs) intern.simps(2)} & $\dn$ & @{thm (rhs) intern.simps(2)}\\ |
|
2088 @{thm (lhs) intern.simps(3)} & $\dn$ & @{thm (rhs) intern.simps(3)}\\ |
|
2089 @{thm (lhs) intern.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) intern.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\ |
|
2090 @{thm (lhs) intern.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) intern.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\ |
|
2091 @{thm (lhs) intern.simps(6)} & $\dn$ & @{thm (rhs) intern.simps(6)}\\ |
|
2092 \end{tabular} |
|
2093 \end{center} |
|
2094 |
|
2095 \begin{center} |
|
2096 \begin{tabular}{lcl} |
|
2097 @{thm (lhs) erase.simps(1)} & $\dn$ & @{thm (rhs) erase.simps(1)}\\ |
|
2098 @{thm (lhs) erase.simps(2)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(2)[of bs]}\\ |
|
2099 @{thm (lhs) erase.simps(3)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(3)[of bs]}\\ |
|
2100 @{thm (lhs) erase.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) erase.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
2101 @{thm (lhs) erase.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) erase.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
2102 @{thm (lhs) erase.simps(6)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(6)[of bs]}\\ |
|
2103 \end{tabular} |
|
2104 \end{center} |
|
2105 |
|
2106 Some simple facts about erase |
|
2107 |
|
2108 \begin{lemma}\mbox{}\\ |
|
2109 @{thm erase_bder}\\ |
|
2110 @{thm erase_intern} |
|
2111 \end{lemma} |
|
2112 |
|
2113 \begin{center} |
|
2114 \begin{tabular}{lcl} |
|
2115 @{thm (lhs) bnullable.simps(1)} & $\dn$ & @{thm (rhs) bnullable.simps(1)}\\ |
|
2116 @{thm (lhs) bnullable.simps(2)} & $\dn$ & @{thm (rhs) bnullable.simps(2)}\\ |
|
2117 @{thm (lhs) bnullable.simps(3)} & $\dn$ & @{thm (rhs) bnullable.simps(3)}\\ |
|
2118 @{thm (lhs) bnullable.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bnullable.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
2119 @{thm (lhs) bnullable.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bnullable.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
2120 @{thm (lhs) bnullable.simps(6)} & $\dn$ & @{thm (rhs) bnullable.simps(6)}\medskip\\ |
|
2121 |
|
2122 % \end{tabular} |
|
2123 % \end{center} |
|
2124 |
|
2125 % \begin{center} |
|
2126 % \begin{tabular}{lcl} |
|
2127 |
|
2128 @{thm (lhs) bder.simps(1)} & $\dn$ & @{thm (rhs) bder.simps(1)}\\ |
|
2129 @{thm (lhs) bder.simps(2)} & $\dn$ & @{thm (rhs) bder.simps(2)}\\ |
|
2130 @{thm (lhs) bder.simps(3)} & $\dn$ & @{thm (rhs) bder.simps(3)}\\ |
|
2131 @{thm (lhs) bder.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bder.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
2132 @{thm (lhs) bder.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bder.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
2133 @{thm (lhs) bder.simps(6)} & $\dn$ & @{thm (rhs) bder.simps(6)} |
|
2134 \end{tabular} |
|
2135 \end{center} |
|
2136 |
|
2137 |
|
2138 \begin{center} |
|
2139 \begin{tabular}{lcl} |
|
2140 @{thm (lhs) bmkeps.simps(1)} & $\dn$ & @{thm (rhs) bmkeps.simps(1)}\\ |
|
2141 @{thm (lhs) bmkeps.simps(2)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bmkeps.simps(2)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
2142 @{thm (lhs) bmkeps.simps(3)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bmkeps.simps(3)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
2143 @{thm (lhs) bmkeps.simps(4)} & $\dn$ & @{thm (rhs) bmkeps.simps(4)}\medskip\\ |
|
2144 \end{tabular} |
|
2145 \end{center} |
|
2146 |
|
2147 |
|
2148 @{thm [mode=IfThen] bder_retrieve} |
|
2149 |
|
2150 By induction on \<open>r\<close> |
|
2151 |
|
2152 \begin{theorem}[Main Lemma]\mbox{}\\ |
|
2153 @{thm [mode=IfThen] MAIN_decode} |
|
2154 \end{theorem} |
|
2155 |
|
2156 \noindent |
|
2157 Definition of the bitcoded lexer |
|
2158 |
|
2159 @{thm blexer_def} |
|
2160 |
|
2161 |
|
2162 \begin{theorem} |
|
2163 @{thm blexer_correctness} |
|
2164 \end{theorem} |
|
2165 |
|
2166 |
|
2167 |
|
2168 |
|
2169 |
|
2170 \begin{center} |
|
2171 \begin{tabular}{lcl} |
|
2172 @{thm (lhs) code.simps(1)} & $\dn$ & @{thm (rhs) code.simps(1)}\\ |
|
2173 @{thm (lhs) code.simps(2)} & $\dn$ & @{thm (rhs) code.simps(2)}\\ |
|
2174 @{thm (lhs) code.simps(3)} & $\dn$ & @{thm (rhs) code.simps(3)}\\ |
|
2175 @{thm (lhs) code.simps(4)} & $\dn$ & @{thm (rhs) code.simps(4)}\\ |
|
2176 @{thm (lhs) code.simps(5)[of "v\<^sub>1" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) code.simps(5)[of "v\<^sub>1" "v\<^sub>2"]}\\ |
|
2177 @{thm (lhs) code.simps(6)} & $\dn$ & @{thm (rhs) code.simps(6)}\\ |
|
2178 @{thm (lhs) code.simps(7)} & $\dn$ & @{thm (rhs) code.simps(7)} |
|
2179 \end{tabular} |
|
2180 \end{center} |
|
2181 |
|
2182 \begin{center} |
|
2183 \begin{tabular}{lcl} |
|
2184 @{term areg} & $::=$ & @{term "AZERO"}\\ |
|
2185 & $\mid$ & @{term "AONE bs"}\\ |
|
2186 & $\mid$ & @{term "ACHAR bs c"}\\ |
|
2187 & $\mid$ & @{term "AALT bs r1 r2"}\\ |
|
2188 & $\mid$ & @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}\\ |
|
2189 & $\mid$ & @{term "ASTAR bs r"} |
|
2190 \end{tabular} |
|
2191 \end{center} |
|
2192 |
|
2193 |
|
2194 \begin{center} |
|
2195 \begin{tabular}{lcl} |
|
2196 @{thm (lhs) intern.simps(1)} & $\dn$ & @{thm (rhs) intern.simps(1)}\\ |
|
2197 @{thm (lhs) intern.simps(2)} & $\dn$ & @{thm (rhs) intern.simps(2)}\\ |
|
2198 @{thm (lhs) intern.simps(3)} & $\dn$ & @{thm (rhs) intern.simps(3)}\\ |
|
2199 @{thm (lhs) intern.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) intern.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\ |
|
2200 @{thm (lhs) intern.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) intern.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\ |
|
2201 @{thm (lhs) intern.simps(6)} & $\dn$ & @{thm (rhs) intern.simps(6)}\\ |
|
2202 \end{tabular} |
|
2203 \end{center} |
|
2204 |
|
2205 \begin{center} |
|
2206 \begin{tabular}{lcl} |
|
2207 @{thm (lhs) erase.simps(1)} & $\dn$ & @{thm (rhs) erase.simps(1)}\\ |
|
2208 @{thm (lhs) erase.simps(2)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(2)[of bs]}\\ |
|
2209 @{thm (lhs) erase.simps(3)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(3)[of bs]}\\ |
|
2210 @{thm (lhs) erase.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) erase.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
2211 @{thm (lhs) erase.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) erase.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
2212 @{thm (lhs) erase.simps(6)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(6)[of bs]}\\ |
|
2213 \end{tabular} |
|
2214 \end{center} |
|
2215 |
|
2216 Some simple facts about erase |
|
2217 |
|
2218 \begin{lemma}\mbox{}\\ |
|
2219 @{thm erase_bder}\\ |
|
2220 @{thm erase_intern} |
|
2221 \end{lemma} |
|
2222 |
|
2223 \begin{center} |
|
2224 \begin{tabular}{lcl} |
|
2225 @{thm (lhs) bnullable.simps(1)} & $\dn$ & @{thm (rhs) bnullable.simps(1)}\\ |
|
2226 @{thm (lhs) bnullable.simps(2)} & $\dn$ & @{thm (rhs) bnullable.simps(2)}\\ |
|
2227 @{thm (lhs) bnullable.simps(3)} & $\dn$ & @{thm (rhs) bnullable.simps(3)}\\ |
|
2228 @{thm (lhs) bnullable.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bnullable.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
2229 @{thm (lhs) bnullable.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bnullable.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
2230 @{thm (lhs) bnullable.simps(6)} & $\dn$ & @{thm (rhs) bnullable.simps(6)}\medskip\\ |
|
2231 |
|
2232 % \end{tabular} |
|
2233 % \end{center} |
|
2234 |
|
2235 % \begin{center} |
|
2236 % \begin{tabular}{lcl} |
|
2237 |
|
2238 @{thm (lhs) bder.simps(1)} & $\dn$ & @{thm (rhs) bder.simps(1)}\\ |
|
2239 @{thm (lhs) bder.simps(2)} & $\dn$ & @{thm (rhs) bder.simps(2)}\\ |
|
2240 @{thm (lhs) bder.simps(3)} & $\dn$ & @{thm (rhs) bder.simps(3)}\\ |
|
2241 @{thm (lhs) bder.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bder.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
2242 @{thm (lhs) bder.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bder.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
2243 @{thm (lhs) bder.simps(6)} & $\dn$ & @{thm (rhs) bder.simps(6)} |
|
2244 \end{tabular} |
|
2245 \end{center} |
|
2246 |
|
2247 |
|
2248 \begin{center} |
|
2249 \begin{tabular}{lcl} |
|
2250 @{thm (lhs) bmkeps.simps(1)} & $\dn$ & @{thm (rhs) bmkeps.simps(1)}\\ |
|
2251 @{thm (lhs) bmkeps.simps(2)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bmkeps.simps(2)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
2252 @{thm (lhs) bmkeps.simps(3)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bmkeps.simps(3)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ |
|
2253 @{thm (lhs) bmkeps.simps(4)} & $\dn$ & @{thm (rhs) bmkeps.simps(4)}\medskip\\ |
|
2254 \end{tabular} |
|
2255 \end{center} |
|
2256 |
|
2257 |
|
2258 @{thm [mode=IfThen] bder_retrieve} |
|
2259 |
|
2260 By induction on \<open>r\<close> |
|
2261 |
|
2262 \begin{theorem}[Main Lemma]\mbox{}\\ |
|
2263 @{thm [mode=IfThen] MAIN_decode} |
|
2264 \end{theorem} |
|
2265 |
|
2266 \noindent |
|
2267 Definition of the bitcoded lexer |
|
2268 |
|
2269 @{thm blexer_def} |
|
2270 |
|
2271 |
|
2272 \begin{theorem} |
|
2273 @{thm blexer_correctness} |
|
2274 \end{theorem} |
|
2275 |
|
2276 \<close> |
|
2277 \<close>*) |