equal
deleted
inserted
replaced
925 In the second clause we first calculate the derivative @{term "der c r"} |
925 In the second clause we first calculate the derivative @{term "der c r"} |
926 and then simplify the result. This gives us a simplified derivative |
926 and then simplify the result. This gives us a simplified derivative |
927 @{text "r\<^sub>s"} and a rectification function @{text "f\<^sub>r"}. The lexer |
927 @{text "r\<^sub>s"} and a rectification function @{text "f\<^sub>r"}. The lexer |
928 is then recursively called with the simplified derivative, but before |
928 is then recursively called with the simplified derivative, but before |
929 we inject the character @{term c} into the value @{term v}, we need to rectify |
929 we inject the character @{term c} into the value @{term v}, we need to rectify |
930 @{term v} (that is construct @{term "f\<^sub>r v"}). We can prove that |
930 @{term v} (that is construct @{term "f\<^sub>r v"}). Before we can establish the correctness |
|
931 of @{const "slexer"}, we need to show that simplification preserves the language |
|
932 and the relation between simplification and our posix definition: |
|
933 |
|
934 \begin{lemma}\mbox{}\smallskip\\ |
|
935 \begin{tabular}{ll} |
|
936 (1) & @{thm L_fst_simp[symmetric]}\\ |
|
937 (2) & @{thm[mode=IfThen] Posix_simp} |
|
938 \end{tabular} |
|
939 \end{lemma} |
|
940 |
|
941 \noindent |
|
942 We can now prove that |
931 |
943 |
932 \begin{theorem} |
944 \begin{theorem} |
933 @{thm slexer_correctness} |
945 @{thm slexer_correctness} |
934 \end{theorem} |
946 \end{theorem} |
935 |
947 |