--- /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
--- 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,
--- /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
--- 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 \<Longrightarrow> map rerase (map bsimp rs) = map rerase rs"
+ oops
+
+inductive leq1 ("_ \<le>1 _" [80, 80] 80) where
+ "r1 \<le>1 r1"
+| "AZERO \<le>1 ASEQ bs AZERO r"
+| "AZERO \<le>1 ASEQ bs r AZERO"
+| "fuse (bs @ bs1) r2 \<le>1 ASEQ bs (AONE bs1) r2"
+| " AALTs bs (rs1 @ rs) \<le>1 AALTs bs (rs1 @( AZERO # rs))"
+| "r2 \<le>1 r1 \<Longrightarrow> AALTs bs (rs1 @ r2 # rs) \<le>1 AALTs bs (rs1 @ r1 # rs)"
+| "AALTs bs1 (rsa @ (map (fuse bs1) rs1) @ rsb) \<le>1 AALTs bs1 (rsa @ (AALTs bs1 rs1) # rsb)"
+| "rerase a1 = rerase a2 \<Longrightarrow> AALTs bs (rsa @ [a1] @ rsb @ rsc) \<le>1 AALTs bs (rsa @ [a1] @ rsb @ [a2] @ rsc) "
+| "r1 \<le>1 r2 \<Longrightarrow> r1 \<le>1 ASEQ bs (AONE bs1) r2"
+
+lemma leq1_less_or_equal: shows
+"r1 \<le>1 r2 \<Longrightarrow> r1 = r2 \<or> rerase r1 \<noteq> rerase r2"
+ apply(induct rule: leq1.induct)
+ apply simp+
+ sorry
+
+lemma bsimp_leq1:
+ shows "bsimp r \<le>1 r"
+
+ sorry
+
+
+lemma arexpfiniteaux4_aux:
+ shows" \<lbrakk>rerase (bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {})) = RALTS (map rerase rs) \<rbrakk>
+ \<Longrightarrow> map rerase (map bsimp rs) = map rerase rs"
+ apply(induct rs)
+ apply simp
+ apply simp
+ apply auto
+ prefer 2
+
+ sorry
+
+lemma arexpfiniteaux4:
+ shows"
+ \<lbrakk>\<And>x. \<lbrakk>x \<in> set rs; rerase (bsimp x) = rerase x\<rbrakk> \<Longrightarrow> bsimp x = x;
+ rerase (bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {})) = RALTS (map rerase rs)\<rbrakk>
+ \<Longrightarrow> 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 \<Longrightarrow> 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"