89 PosOrd_ex ("_ \<prec> _" [77,77] 77) and |
95 PosOrd_ex ("_ \<prec> _" [77,77] 77) and |
90 PosOrd_ex_eq ("_ \<^latex>\<open>\\mbox{$\\preccurlyeq$}\<close> _" [77,77] 77) and |
96 PosOrd_ex_eq ("_ \<^latex>\<open>\\mbox{$\\preccurlyeq$}\<close> _" [77,77] 77) and |
91 pflat_len ("\<parallel>_\<parallel>\<^bsub>_\<^esub>") and |
97 pflat_len ("\<parallel>_\<parallel>\<^bsub>_\<^esub>") and |
92 nprec ("_ \<^latex>\<open>\\mbox{$\\not\\prec$}\<close> _" [77,77] 77) and |
98 nprec ("_ \<^latex>\<open>\\mbox{$\\not\\prec$}\<close> _" [77,77] 77) and |
93 |
99 |
|
100 bder_syn ("_\<^latex>\<open>\\mbox{$\\bbslash$}\<close>_" [79, 1000] 76) and |
|
101 bders_syn ("_\<^latex>\<open>\\mbox{$\\bbslash$}\<close>_" [79, 1000] 76) and |
|
102 intern ("_\<^latex>\<open>\\mbox{$^\\uparrow$}\<close>" [900] 80) and |
|
103 erase ("_\<^latex>\<open>\\mbox{$^\\downarrow$}\<close>" [1000] 74) and |
|
104 bnullable ("nullable\<^latex>\<open>\\mbox{$_b$}\<close> _" [1000] 80) and |
|
105 bmkeps ("mkeps\<^latex>\<open>\\mbox{$_b$}\<close> _" [1000] 80) and |
|
106 blexer ("lexer\<^latex>\<open>\\mbox{$_b$}\<close> _ _" [77, 77] 80) and |
|
107 code ("code _" [79] 74) and |
|
108 |
94 DUMMY ("\<^latex>\<open>\\underline{\\hspace{2mm}}\<close>") |
109 DUMMY ("\<^latex>\<open>\\underline{\\hspace{2mm}}\<close>") |
95 |
110 |
96 |
111 |
97 definition |
112 definition |
98 "match r s \<equiv> nullable (ders s r)" |
113 "match r s \<equiv> nullable (ders s r)" |
708 but our deviation is harmless.} |
723 but our deviation is harmless.} |
709 |
724 |
710 The idea of the @{term inj}-function to ``inject'' a character, say |
725 The idea of the @{term inj}-function to ``inject'' a character, say |
711 @{term c}, into a value can be made precise by the first part of the |
726 @{term c}, into a value can be made precise by the first part of the |
712 following lemma, which shows that the underlying string of an injected |
727 following lemma, which shows that the underlying string of an injected |
713 value has a prepended character @{term c}; the second part shows that the |
728 value has a prepended character @{term c}; the second part shows that |
714 underlying string of an @{const mkeps}-value is always the empty string |
729 the underlying string of an @{const mkeps}-value is always the empty |
715 (given the regular expression is nullable since otherwise @{text mkeps} |
730 string (given the regular expression is nullable since otherwise |
716 might not be defined). |
731 @{text mkeps} might not be defined). |
717 |
732 |
718 \begin{lemma}\mbox{}\smallskip\\\label{Prf_injval_flat} |
733 \begin{lemma}\mbox{}\smallskip\\\label{Prf_injval_flat} |
719 \begin{tabular}{ll} |
734 \begin{tabular}{ll} |
720 (1) & @{thm[mode=IfThen] Prf_injval_flat}\\ |
735 (1) & @{thm[mode=IfThen] Prf_injval_flat}\\ |
721 (2) & @{thm[mode=IfThen] mkeps_flat} |
736 (2) & @{thm[mode=IfThen] mkeps_flat} |
1383 an independent confirmation that our ternary relation formalise the |
1398 an independent confirmation that our ternary relation formalise the |
1384 informal POSIX rules. |
1399 informal POSIX rules. |
1385 |
1400 |
1386 *} |
1401 *} |
1387 |
1402 |
|
1403 section {* Bitcoded Lexing *} |
|
1404 |
|
1405 |
|
1406 text {* |
|
1407 |
|
1408 Incremental calculation of the value. To simplify the proof we first define the function |
|
1409 @{const flex} which calculates the ``iterated'' injection function. With this we can |
|
1410 rewrite the lexer as |
|
1411 |
|
1412 \begin{center} |
|
1413 @{thm lexer_flex} |
|
1414 \end{center} |
|
1415 |
|
1416 \begin{center} |
|
1417 \begin{tabular}{lcl} |
|
1418 @{thm (lhs) code.simps(1)} & $\dn$ & @{thm (rhs) code.simps(1)}\\ |
|
1419 @{thm (lhs) code.simps(2)} & $\dn$ & @{thm (rhs) code.simps(2)}\\ |
|
1420 @{thm (lhs) code.simps(3)} & $\dn$ & @{thm (rhs) code.simps(3)}\\ |
|
1421 @{thm (lhs) code.simps(4)} & $\dn$ & @{thm (rhs) code.simps(4)}\\ |
|
1422 @{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"]}\\ |
|
1423 @{thm (lhs) code.simps(6)} & $\dn$ & @{thm (rhs) code.simps(6)}\\ |
|
1424 @{thm (lhs) code.simps(7)} & $\dn$ & @{thm (rhs) code.simps(7)} |
|
1425 \end{tabular} |
|
1426 \end{center} |
|
1427 |
|
1428 \begin{center} |
|
1429 \begin{tabular}{lcl} |
|
1430 @{term areg} & $::=$ & @{term "AZERO"}\\ |
|
1431 & $\mid$ & @{term "AONE bs"}\\ |
|
1432 & $\mid$ & @{term "ACHAR bs c"}\\ |
|
1433 & $\mid$ & @{term "AALT bs r\<^sub>1 r\<^sub>2"}\\ |
|
1434 & $\mid$ & @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}\\ |
|
1435 & $\mid$ & @{term "ASTAR bs r"} |
|
1436 \end{tabular} |
|
1437 \end{center} |
|
1438 |
|
1439 \begin{center} |
|
1440 \begin{tabular}{lcl} |
|
1441 @{thm (lhs) intern.simps(1)} & $\dn$ & @{thm (rhs) intern.simps(1)}\\ |
|
1442 @{thm (lhs) intern.simps(2)} & $\dn$ & @{thm (rhs) intern.simps(2)}\\ |
|
1443 @{thm (lhs) intern.simps(3)} & $\dn$ & @{thm (rhs) intern.simps(3)}\\ |
|
1444 @{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"]}\\ |
|
1445 @{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"]}\\ |
|
1446 @{thm (lhs) intern.simps(6)} & $\dn$ & @{thm (rhs) intern.simps(6)}\\ |
|
1447 \end{tabular} |
|
1448 \end{center} |
|
1449 |
|
1450 \begin{center} |
|
1451 \begin{tabular}{lcl} |
|
1452 @{thm (lhs) erase.simps(1)} & $\dn$ & @{thm (rhs) erase.simps(1)}\\ |
|
1453 @{thm (lhs) erase.simps(2)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(2)[of bs]}\\ |
|
1454 @{thm (lhs) erase.simps(3)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(3)[of bs]}\\ |
|
1455 @{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"]}\\ |
|
1456 @{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"]}\\ |
|
1457 @{thm (lhs) erase.simps(6)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(6)[of bs]}\\ |
|
1458 \end{tabular} |
|
1459 \end{center} |
|
1460 |
|
1461 Some simple facts about erase |
|
1462 |
|
1463 \begin{lemma}\mbox{}\\ |
|
1464 @{thm erase_bder}\\ |
|
1465 @{thm erase_intern} |
|
1466 \end{lemma} |
|
1467 |
|
1468 \begin{center} |
|
1469 \begin{tabular}{lcl} |
|
1470 @{thm (lhs) bnullable.simps(1)} & $\dn$ & @{thm (rhs) bnullable.simps(1)}\\ |
|
1471 @{thm (lhs) bnullable.simps(2)} & $\dn$ & @{thm (rhs) bnullable.simps(2)}\\ |
|
1472 @{thm (lhs) bnullable.simps(3)} & $\dn$ & @{thm (rhs) bnullable.simps(3)}\\ |
|
1473 @{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"]}\\ |
|
1474 @{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"]}\\ |
|
1475 @{thm (lhs) bnullable.simps(6)} & $\dn$ & @{thm (rhs) bnullable.simps(6)}\medskip\\ |
|
1476 |
|
1477 % \end{tabular} |
|
1478 % \end{center} |
|
1479 |
|
1480 % \begin{center} |
|
1481 % \begin{tabular}{lcl} |
|
1482 |
|
1483 @{thm (lhs) bder.simps(1)} & $\dn$ & @{thm (rhs) bder.simps(1)}\\ |
|
1484 @{thm (lhs) bder.simps(2)} & $\dn$ & @{thm (rhs) bder.simps(2)}\\ |
|
1485 @{thm (lhs) bder.simps(3)} & $\dn$ & @{thm (rhs) bder.simps(3)}\\ |
|
1486 @{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"]}\\ |
|
1487 @{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"]}\\ |
|
1488 @{thm (lhs) bder.simps(6)} & $\dn$ & @{thm (rhs) bder.simps(6)} |
|
1489 \end{tabular} |
|
1490 \end{center} |
|
1491 |
|
1492 |
|
1493 \begin{center} |
|
1494 \begin{tabular}{lcl} |
|
1495 @{thm (lhs) bmkeps.simps(1)} & $\dn$ & @{thm (rhs) bmkeps.simps(1)}\\ |
|
1496 @{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"]}\\ |
|
1497 @{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"]}\\ |
|
1498 @{thm (lhs) bmkeps.simps(4)} & $\dn$ & @{thm (rhs) bmkeps.simps(4)}\medskip\\ |
|
1499 \end{tabular} |
|
1500 \end{center} |
|
1501 |
|
1502 |
|
1503 @{thm [mode=IfThen] bder_retrieve} |
|
1504 |
|
1505 By induction on @{text r} |
|
1506 |
|
1507 \begin{theorem}[Main Lemma]\mbox{}\\ |
|
1508 @{thm [mode=IfThen] MAIN_decode} |
|
1509 \end{theorem} |
|
1510 |
|
1511 \noindent |
|
1512 Definition of the bitcoded lexer |
|
1513 |
|
1514 @{thm blexer_def} |
|
1515 |
|
1516 |
|
1517 \begin{theorem} |
|
1518 @{thm blexer_correctness} |
|
1519 \end{theorem} |
|
1520 |
|
1521 *} |
|
1522 |
1388 section {* Optimisations *} |
1523 section {* Optimisations *} |
1389 |
1524 |
1390 text {* |
1525 text {* |
1391 |
1526 |
1392 Derivatives as calculated by \Brz's method are usually more complex |
1527 Derivatives as calculated by \Brz's method are usually more complex |