# HG changeset patch # User Chengsong # Date 1661859712 -3600 # Node ID 80e1114d6421ce73f791bc3513e3043d7b1dfc08 # Parent 3198605ac6480e9123b37c17e551922e061b8bdf data diff -r 3198605ac648 -r 80e1114d6421 ChengsongTanPhdThesis/BetterWaterloo1.data --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ChengsongTanPhdThesis/BetterWaterloo1.data Tue Aug 30 12:41:52 2022 +0100 @@ -0,0 +1,19 @@ +1 16 +2 43 +3 97 +4 205 +5 421 +6 853 +7 1717 +8 3445 +9 6901 +10 13813 +11 27637 +12 55285 +13 110581 +14 221173 +15 442357 +16 884725 +17 1769461 +18 3538933 +19 7077877 \ No newline at end of file diff -r 3198605ac648 -r 80e1114d6421 ChengsongTanPhdThesis/Chapters/Bitcoded2.tex --- a/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex Mon Aug 29 23:16:28 2022 +0100 +++ b/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex Tue Aug 30 12:41:52 2022 +0100 @@ -872,57 +872,71 @@ The rewritability relation $\rightsquigarrow$ is preserved under derivatives-- it is just that we might need multiple steps -where originally only one step was needed. +where originally only one step was needed: \begin{lemma}\label{rewriteBder} - $r_1 \rightsquigarrow r_2 \implies r_1 \backslash c \stackrel{*}{\rightsquigarrow} r_2 \backslash c$ - and - $rs_1 \stackrel{s}{\rightsquigarrow} rs_2 \implies - \map \; (\_\backslash c) \; rs_1 \stackrel{s*}{\rightsquigarrow} \map \; (\_ \backslash c) \; rs_2$ -\end{lemma} -\begin{proof} - By induction on $\rightsquigarrow$ and $\stackrel{s}{\rightsquigarrow}$, using a number of the previous lemmas. -\end{proof} -Now we can prove that once we could rewrite from one expression to another in many steps, -then after a derivative on both sides we could still rewrite one to another in many steps: -\begin{lemma} - $r_1 \stackrel{*}{\rightsquigarrow} r_2 \implies r_1 \backslash c \stackrel{*}{\rightsquigarrow} r_2 \backslash c$ + \hspace{0em} + \begin{itemize} + \item + If $r_1 \rightsquigarrow r_2$, then $r_1 \backslash c + \rightsquigarrow^* r_2 \backslash c$ + \item + If $rs_1 \stackrel{s}{\rightsquigarrow} rs_2$, then $ + \map \; (\_\backslash c) \; rs_1 + \stackrel{s*}{\rightsquigarrow} \map \; (\_ \backslash c) \; rs_2$ + \end{itemize} \end{lemma} \begin{proof} - By rule induction of $\stackrel{*}{\rightsquigarrow} $ and using the previous lemma :\ref{rewriteBder}. + By induction on $\rightsquigarrow$ + and $\stackrel{s}{\rightsquigarrow}$, using a number of the previous lemmas. +\end{proof} +\noindent +Now we can prove property 3, as an immediate corollary: +\begin{corollary}\label{rewritesBder} + $r_1 \rightsquigarrow^* r_2 \implies r_1 \backslash c \rightsquigarrow^* + r_2 \backslash c$ +\end{corollary} +\begin{proof} + By rule induction of $\stackrel{*}{\rightsquigarrow} $ and using the previous lemma \ref{rewriteBder}. \end{proof} \noindent -This can be extended and combined with the previous two important properties -so that a regular expression's successivve derivatives can be rewritten in many steps -to its simplified counterpart: +This can be extended and combined with $r \rightsquigarrow^* \textit{bsimp} \; r$ +to obtain the rewritability between +$\blexer$ and $\blexersimp$'s intermediate +derivative regular expressions \begin{lemma}\label{bderBderssimp} - $a \backslash s \stackrel{*}{\rightsquigarrow} \bderssimp{a}{s} $ + $a \backslash s \rightsquigarrow^* \bderssimp{a}{s} $ \end{lemma} +\begin{proof} + By an induction on $s$. +\end{proof} \subsection{Main Theorem} -Now with \ref{bdersBderssimp} we are ready for the main theorem. -To link $\blexersimp$ and $\blexer$, -we first say that they give out the same bits, if the lexing result is a match: -\begin{lemma} - $\bnullable \; (a \backslash s) \implies \bmkeps \; (a \backslash s) = \bmkeps \; (\bderssimp{a}{s})$ -\end{lemma} -\noindent -Now that they give out the same bits, we know that they give the same value after decoding, -which we know is correct value as $\blexer$ is correct: +Now with \ref{bderBderssimp} we are ready for the main theorem. \begin{theorem} $\blexer \; r \; s = \blexersimp{r}{s}$ \end{theorem} \noindent \begin{proof} - One can rewrite in many steps from the original lexer's derivative regular expressions to the - lexer with simplification applied: - $a \backslash s \stackrel{*}{\rightsquigarrow} \bderssimp{a}{s} $. - If two regular expressions are rewritable, then they produce the same bits. - Under the condition that $ r_1$ is nullable, we have - $\text{If} \;\; r \stackrel{*}{\rightsquigarrow} r', \;\;\text{then} \;\; \bmkeps \; r = \bmkeps \; r'$. - We have that - $\bmkeps \; (r \backslash s) = \bmkeps \; \bderssimp{r}{s}$ holds. - This proves the \emph{if} branch of - $\blexer \; r \; s = \blexersimp{r}{s}$. - + One can rewrite in many steps from the original lexer's + derivative regular expressions to the + lexer with simplification applied (by lemma \ref{bderBderssimp}): + \begin{center} + $a \backslash s \stackrel{*}{\rightsquigarrow} \bderssimp{a}{s} $. + \end{center} + we know that they give out the same bits, if the lexing result is a match: + \begin{center} + $\bnullable \; (a \backslash s) + \implies \bmkeps \; (a \backslash s) = \bmkeps \; (\bderssimp{a}{s})$ + \end{center} + Now that they give out the same bits, we know that they give the same value after decoding. + \begin{center} + $\bnullable \; (a \backslash s) + \implies \decode \; r \; (\bmkeps \; (a \backslash s)) = + \decode \; r \; (\bmkeps \; (\bderssimp{a}{s}))$ + \end{center} + Which is equivalent to our proof goal: + \begin{center} + $\blexer \; r \; s = \blexersimp \; r \; s$. + \end{center} \end{proof} \noindent As a corollary, diff -r 3198605ac648 -r 80e1114d6421 ChengsongTanPhdThesis/SulzmannLuLexerTime.data --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ChengsongTanPhdThesis/SulzmannLuLexerTime.data Tue Aug 30 12:41:52 2022 +0100 @@ -0,0 +1,19 @@ +1 0.00113925 +2 0.001390393 +3 0.00113369 +4 0.001611037 +5 0.00320043 +6 0.004299621 +7 0.009503939 +8 0.012337418 +9 0.028872115 +10 0.078161428 +11 0.147121003 +12 0.241872536 +13 0.546760917 +14 1.241357992 +15 2.935996717 +16 6.732515184 +17 15.095000451 +18 33.060935265 +19 74.823744749 \ No newline at end of file diff -r 3198605ac648 -r 80e1114d6421 thys4/posix/FBound.thy --- a/thys4/posix/FBound.thy Mon Aug 29 23:16:28 2022 +0100 +++ b/thys4/posix/FBound.thy Tue Aug 30 12:41:52 2022 +0100 @@ -247,9 +247,73 @@ apply simp done +lemma aux_aux_aux: + shows "map rerase (flts (map bsimp rs)) = map rerase rs \ map rerase (map bsimp rs) = map rerase rs" + oops + +inductive leq1 ("_ \1 _" [80, 80] 80) where + "r1 \1 r1" +| "AZERO \1 ASEQ bs AZERO r" +| "AZERO \1 ASEQ bs r AZERO" +| "fuse (bs @ bs1) r2 \1 ASEQ bs (AONE bs1) r2" +| " AALTs bs (rs1 @ rs) \1 AALTs bs (rs1 @( AZERO # rs))" +| "r2 \1 r1 \ AALTs bs (rs1 @ r2 # rs) \1 AALTs bs (rs1 @ r1 # rs)" +| "AALTs bs1 (rsa @ (map (fuse bs1) rs1) @ rsb) \1 AALTs bs1 (rsa @ (AALTs bs1 rs1) # rsb)" +| "rerase a1 = rerase a2 \ AALTs bs (rsa @ [a1] @ rsb @ rsc) \1 AALTs bs (rsa @ [a1] @ rsb @ [a2] @ rsc) " +| "r1 \1 r2 \ r1 \1 ASEQ bs (AONE bs1) r2" + +lemma leq1_less_or_equal: shows +"r1 \1 r2 \ r1 = r2 \ rerase r1 \ rerase r2" + apply(induct rule: leq1.induct) + apply simp+ + sorry + +lemma bsimp_leq1: + shows "bsimp r \1 r" + + sorry + + +lemma arexpfiniteaux4_aux: + shows" \rerase (bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {})) = RALTS (map rerase rs) \ + \ map rerase (map bsimp rs) = map rerase rs" + apply(induct rs) + apply simp + apply simp + apply auto + prefer 2 + + sorry + +lemma arexpfiniteaux4: + shows" + \\x. \x \ set rs; rerase (bsimp x) = rerase x\ \ bsimp x = x; + rerase (bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {})) = RALTS (map rerase rs)\ + \ bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {}) = AALTs bs1 rs" + apply(induct rs) + apply simp + + + + + + + sorry + + + lemma arexp_finite1: shows "rerase (bsimp b) = rerase b \ bsimp b = b" + apply(induct rule: bsimp.induct) + apply simp + apply (smt (verit) arexpfiniteaux1 arexpfiniteaux2 arexpfiniteaux3 bsimp_ASEQ1 rerase.simps(5) rrexp.inject(2)) + apply simp + + using arexpfiniteaux4 apply blast + apply simp+ + done +(* apply(induct b) apply simp+ apply(case_tac "bsimp b2 = AZERO") @@ -265,6 +329,8 @@ apply simp sorry +*) + lemma bitcodes_unchanging2: assumes "bsimp a = b"