# HG changeset patch # User Chengsong # Date 1656278567 -3600 # Node ID 15d182ffbc7678ad9e97042a29b1a2f24f6c7696 # Parent 0f00d440f48471822ca965ca69ee76a92831db2d more diff -r 0f00d440f484 -r 15d182ffbc76 ChengsongTanPhdThesis/Chapters/Finite.tex --- a/ChengsongTanPhdThesis/Chapters/Finite.tex Fri Jun 24 21:49:23 2022 +0100 +++ b/ChengsongTanPhdThesis/Chapters/Finite.tex Sun Jun 26 22:22:47 2022 +0100 @@ -136,6 +136,7 @@ \begin{lemma} $\rsize{\rerase a} = \asize a$ \end{lemma} +\noindent This does not hold for plain $\rexp$s. Similarly we could define the derivative and simplification on @@ -197,6 +198,9 @@ \end{center} %TODO: definition of rsimp (maybe only the alternative clause) \noindent +The prefix $r$ in front of $\rdistinct{}{}$ is used mainly to +differentiate with $\textit{distinct}$, which is a built-in predicate +in Isabelle that says all the elements of a list are unique. With $\textit{rdistinct}$ one can chain together all the other modules of $\bsimp{\_}$ (removing the functionalities related to bit-sequences) and get $\textit{rsimp}$ and $\rderssimp{\_}{\_}$. @@ -209,10 +213,10 @@ The following equalities hold: \begin{itemize} \item -$\asize{\bsimp{a}} = \rsize{\rsimp{\rerase{a}}}$ -\item -$\asize{\bderssimp{r}{s}} = \rsize{\rderssimp{\rerase{r}}{s}}$ -\end{itemize} + $\asize{\bsimp{a}} = \rsize{\rsimp{\rerase{a}}}$ + \item + $\asize{\bderssimp{r}{s}} = \rsize{\rderssimp{\rerase{r}}{s}}$ + \end{itemize} \end{lemma} \noindent In the following content, we will focus on $\rrexp$'s size bound. @@ -297,9 +301,18 @@ on the resulting list, the output will be as if we had called $\rdistinct{\_}{\_}$ without the prepending of $rs$: \begin{lemma} - If $rs \subseteq rset$, then - $\rdistinct{rs@rsa }{acc} = \rdistinct{rsa }{acc}$. + The elements appearing in the accumulator will always be removed. + More precisely, + \begin{itemize} + \item + If $rs \subseteq rset$, then + $\rdistinct{rs@rsa }{acc} = \rdistinct{rsa }{acc}$. + \item + Furthermore, if $a \in rset$ and $\rdistinct{rs}{\{a\}} = []$, + then $\rdistinct{(rs @ rs')}{rset} = \rdistinct{rs'}{rset}$ + \end{itemize} \end{lemma} + \begin{proof} By induction on $rs$. \end{proof} @@ -326,15 +339,44 @@ for any prefix of an input list, in other words, when can we ``push out" the arguments of $\rdistinct{\_}{\_}$: \begin{lemma} - If $rs_1$'s elements are all unique, and not appearing in the accumulator $acc$, + If $\textit{isDistinct} \; rs_1$, and $rs_1 \cap acc = \varnothing$, then it can be taken out and left untouched in the output: \[\textit{rdistinct}\; (rs_1 @ rsa)\;\, acc = rs_1@(\textit{rdistinct} rsa \; (acc \cup rs_1))\] \end{lemma} - +\noindent +The predicate $\textit{isDistinct}$ is for testing +whether a list's elements are all unique. It is defined +recursively on the structure of a regular expression, +and we omit the precise definition here. \begin{proof} By an induction on $rs_1$, where $rsa$ and $acc$ are allowed to be arbitrary. \end{proof} +\noindent +$\rdistinct{}{}$ removes any element in anywhere of a list, if it +had appeared previously: +\begin{lemma}\label{distinctRemovesMiddle} + The two properties hold if $r \in rs$: + \begin{itemize} + \item + $\rdistinct{rs}{rset} = \rdistinct{(rs @ [r])}{rset}$ + and + $\rdistinct{(ab :: rs @ [ab])}{rset'} = \rdistinct{(ab :: rs)}{rset'}$ + \item + $\rdistinct{ (rs @ rs') }{rset} = \rdistinct{rs @ [r] @ rs'}{rset}$ + and + $\rdistinct{(ab :: rs @ [ab] @ rs'')}{rset'} = + \rdistinct{(ab :: rs @ rs'')}{rset'}$ + \end{itemize} +\end{lemma} +\noindent +\begin{proof} +By induction on $rs$. All other variables are allowed to be arbitrary. +The second half of the lemma requires the first half. +Note that for each half's two sub-propositions need to be proven concurrently, +so that the induction goes through. +\end{proof} + \subsubsection{The Properties of $\backslash_r$, $\backslash_{rsimp}$, $\textit{Rflts}$ and $\textit{Rsimp}_{ALTS}$} We give in this subsection some properties of how $\backslash_r$, $\backslash_{rsimp}$, $\textit{Rflts}$ and $\textit{Rsimp}_{ALTS} $ interact with each other and with $@$, the concatenation operator. These will be helpful in later closed form proofs, when @@ -345,41 +387,290 @@ When the function $\textit{Rflts}$ is applied to the concatenation of two lists, the output can be calculated by first applying the functions on two lists separately, and then concatenating them together. -\begin{lemma} +\begin{lemma}\label{rfltsProps} The function $\rflts$ has the below properties:\\ \begin{itemize} \item - $\rflts \; (rs_1 @ rs_2) = \rflts \; rs_1 @ \rflts \; rs_2$ -\item - If $r \neq \RZERO$ and $\nexists rs_1. r = \RALTS{rs}_1$, then $\rflts \; (r::rs) = r :: \rflts \; rs$ + $\rflts \; (rs_1 @ rs_2) = \rflts \; rs_1 @ \rflts \; rs_2$ + \item + If $r \neq \RZERO$ and $\nexists rs_1. r = \RALTS{rs}_1$, then $\rflts \; (r::rs) = r :: \rflts \; rs$ + \item + $\rflts \; (rs @ [\RZERO]) = \rflts \; rs$ + \item + $\rflts \; (rs' @ [\RALTS{rs}]) = \rflts \; rs'@rs$ + \item + $\rflts \; (rs @ [\RONE]) = \rflts \; rs @ [\RONE]$ + \item + If $r \neq \RZERO$ and $\nexists rs'. r = \RALTS{rs'}$ then $\rflts \; (rs @ [r]) + = (\rflts \; rs) @ [r]$ \end{itemize} \end{lemma} \noindent \begin{proof} - By induction on $rs_1$. + By induction on $rs_1$ in the first part, and induction on $r$ in the second part, + and induction on $rs$, $rs'$ in the third and fourth sub-lemma. \end{proof} - +\subsubsection{The $RL$ Function: Language Interpretation of $\textit{Rrexp}$s} +Much like the definition of $L$ on plain regular expressions, one could also +define the language interpretation of $\rrexp$s. +\begin{center} +\begin{tabular}{lcl} +$RL \; (\ZERO)$ & $\dn$ & $\phi$\\ +$RL \; (\ONE)$ & $\dn$ & $\{[]\}$\\ +$RL \; (c)$ & $\dn$ & $\{[c]\}$\\ +$RL \; \sum rs$ & $\dn$ & $ \bigcup_{r \in rs} (RL \; r)$\\ +$RL \; (r_1 \cdot r_2)$ & $\dn$ & $ RL \; (r_1) @ RL \; (r_2)$\\ +$RL \; (r^*)$ & $\dn$ & $ (RL(r))^*$ +\end{tabular} +\end{center} +\noindent +The main use of $RL$ is to establish some connections between $\rsimp{}$ +and $\rnullable{}$: +\begin{lemma} + The following properties hold: + \begin{itemize} + \item + If $\rnullable{r}$, then $\rsimp{r} \neq \RZERO$. + \item + $\rnullable{r \backslash s} \quad $ if and only if $\quad \rnullable{\rderssimp{r}{s}}$. + \end{itemize} +\end{lemma} +\begin{proof} + The first part is by induction on $r$. + The second part is true because property + \[ RL \; r = RL \; (\rsimp{r})\] holds. +\end{proof} + +\subsubsection{$\rsimp{}$ is Non-Increasing} +In this subsection, we prove that the function $\rsimp{}$ does not +make the $\llbracket \rrbracket_r$ size increase. -\subsection{A Closed Form for the Sequence Regular Expression} -\begin{quote}\it - Claim: For regular expressions $r_1 \cdot r_2$, we claim that - \begin{center} - $ \rderssimp{r_1 \cdot r_2}{s} = - \rsimp{(\sum (r_1 \backslash s \cdot r_2 ) \; :: \;(\map \; \rderssimp{r2}{\_} \;(\vsuf{s}{r_1})))}$ - \end{center} -\end{quote} +\begin{lemma}\label{rsimpSize} + $\llbracket \rsimp{r} \rrbracket_r \leq \llbracket r \rrbracket_r$ +\end{lemma} +\subsubsection{Simplified $\textit{Rrexp}$s are Good} +We formalise the notion of ``good" regular expressions, +which means regular expressions that +are not fully simplified. For alternative regular expressions that means they +do not contain any nested alternatives like +\[ r_1 + (r_2 + r_3) \], un-removed $\RZERO$s like \[\RZERO + r\] +or duplicate elements in a children regular expression list like \[ \sum [r, r, \ldots]\]: +\begin{center} + \begin{tabular}{@{}lcl@{}} + $\good\; \RZERO$ & $\dn$ & $\textit{false}$\\ + $\good\; \RONE$ & $\dn$ & $\textit{true}$\\ + $\good\; \RCHAR{c}$ & $\dn$ & $\btrue$\\ + $\good\; \RALTS{[]}$ & $\dn$ & $\bfalse$\\ + $\good\; \RALTS{[r]}$ & $\dn$ & $\bfalse$\\ + $\good\; \RALTS{r_1 :: r_2 :: rs}$ & $\dn$ & + $\textit{isDistinct} \; (r_1 :: r_2 :: rs) \;$\\ + & & $\textit{and}\; (\forall r' \in (r_1 :: r_2 :: rs).\; \good \; r'\; \, \textit{and}\; \, \textit{nonAlt}\; r')$\\ + $\good \; \RSEQ{\RZERO}{r}$ & $\dn$ & $\bfalse$\\ + $\good \; \RSEQ{\RONE}{r}$ & $\dn$ & $\bfalse$\\ + $\good \; \RSEQ{r}{\RZERO}$ & $\dn$ & $\bfalse$\\ + $\good \; \RSEQ{r_1}{r_2}$ & $\dn$ & $\good \; r_1 \;\, \textit{and} \;\, \good \; r_2$\\ + $\good \; \RSTAR{r}$ & $\dn$ & $\btrue$\\ + \end{tabular} +\end{center} +\noindent +The predicate $\textit{nonAlt}$ evaluates to true when the regular expression is not an +alternative, and false otherwise. +The $\good$ property is preserved under $\rsimp_{ALTS}$, provided that +its non-empty argument list of expressions are all good themsleves, and $\textit{nonAlt}$, +and unique: +\begin{lemma}\label{rsimpaltsGood} + If $rs \neq []$ and forall $r \in rs. \textit{nonAlt} \; r$ and $\textit{isDistinct} \; rs$, + then $\good \; (\rsimpalts \; rs)$ if and only if forall $r \in rs. \; \good \; r$. +\end{lemma} +\noindent +We also note that +if a regular expression $r$ is good, then $\rflts$ on the singleton +list $[r]$ will not break goodness: +\begin{lemma}\label{flts2} + If $\good \; r$, then forall $r' \in \rflts \; [r]. \; \good \; r'$ and $\textit{nonAlt} \; r'$. +\end{lemma} +\begin{proof} + By an induction on $r$. +\end{proof} \noindent +The other observation we make about $\rsimp{r}$ is that it never +comes with nested alternatives, which we describe as the $\nonnested$ +property: +\begin{center} + \begin{tabular}{lcl} + $\nonnested \; \, \sum []$ & $\dn$ & $\btrue$\\ + $\nonnested \; \, \sum ((\sum rs_1) :: rs_2)$ & $\dn$ & $\bfalse$\\ + $\nonnested \; \, \sum (r :: rs)$ & $\dn$ & $\nonnested (\sum rs)$\\ + $\nonnested \; \, r $ & $\dn$ & $\btrue$ + \end{tabular} +\end{center} +\noindent +The $\rflts$ function +always opens up nested alternatives, +which enables $\rsimp$ to be non-nested: + +\begin{lemma}\label{nonnestedRsimp} + $\nonnested \; (\rsimp{r})$ +\end{lemma} +\begin{proof} + By an induction on $r$. +\end{proof} +\noindent +With this we could prove that a regular expressions +after simplification and flattening and de-duplication, +will not contain any alternative regular expression directly: +\begin{lemma}\label{nonaltFltsRd} + If $x \in \rdistinct{\rflts\; (\map \; \rsimp{} \; rs)}{\varnothing}$ + then $\textit{nonAlt} \; x$. +\end{lemma} +\begin{proof} + By \ref{nonnestedRsimp}. +\end{proof} +\noindent +The other thing we know is that once $\rsimp{}$ had finished +processing an alternative regular expression, it will not +contain any $\RZERO$s, this is because all the recursive +calls to the simplification on the children regular expressions +make the children good, and $\rflts$ will not take out +any $\RZERO$s out of a good regular expression list, +and $\rdistinct{}$ will not mess with the result. +\begin{lemma}\label{flts3Obv} + The following are true: + \begin{itemize} + \item + If for all $r \in rs. \, \good \; r $ or $r = \RZERO$, + then for all $r \in \rflts\; rs. \, \good \; r$. + \item + If $x \in \rdistinct{\rflts\; (\map \; rsimp{}\; rs)}{\varnothing}$ + and for all $y$ such that $\llbracket y \rrbracket_r$ less than + $\llbracket rs \rrbracket_r + 1$, either + $\good \; (\rsimp{y})$ or $\rsimp{y} = \RZERO$, + then $\good \; x$. + \end{itemize} +\end{lemma} +\begin{proof} + The first part is by induction on $rs$, where the induction + rule is the inductive cases for $\rflts$. + The second part is a corollary from the first part. +\end{proof} -Before we get to the proof that says the intermediate result of our lexer will -remain finitely bounded, which is an important efficiency/liveness guarantee, -we shall first develop a few preparatory properties and definitions to -make the process of proving that a breeze. +And this leads to good structural property of $\rsimp{}$, +that after simplification, a regular expression is +either good or $\RZERO$: +\begin{lemma}\label{good1} + For any r-regular expression $r$, $\good \; \rsimp{r}$ or $\rsimp{r} = \RZERO$. +\end{lemma} +\begin{proof} + By an induction on $r$. The inductive measure is the size $\llbracket \rrbracket_r$. + Lemma \ref{rsimpSize} says that + $\llbracket \rsimp{r}\rrbracket_r$ is smaller than or equal to + $\llbracket r \rrbracket_r$. + Therefore, in the $r_1 \cdot r_2$ and $\sum rs$ case, + Inductive hypothesis applies to the children regular expressions + $r_1$, $r_2$, etc. The lemma \ref{flts3Obv}'s precondition is satisfied + by that as well. + The lemmas \ref{nonnestedRsimp} and \ref{nonaltFltsRd} are used + to ensure that goodness is preserved at the topmost level. +\end{proof} +We shall prove that any good regular expression is +a fixed-point for $\rsimp{}$. +First we prove an auxiliary lemma: +\begin{lemma}\label{goodaltsNonalt} + If $\good \; \sum rs$, then $\rflts\; rs = rs$. +\end{lemma} +\begin{proof} + By an induction on $\sum rs$. The inductive rules are the cases + for $\good$. +\end{proof} +\noindent +Now we are ready to prove that good regular expressions are invariant +of $\rsimp{}$ application: +\begin{lemma}\label{test} + If $\good \;r$ then $\rsimp{r} = r$. +\end{lemma} +\begin{proof} + By an induction on the inductive cases of $\good$. + The lemma \ref{goodaltsNonalt} is used in the alternative + case where 2 or more elements are present in the list. +\end{proof} + +\subsubsection{$\rsimp$ is Idempotent} +The idempotency of $\rsimp$ is very useful in +manipulating regular expression terms into desired +forms so that key steps allowing further rewriting to closed forms +are possible. +\begin{lemma}\label{rsimpIdem} +$\rsimp{r} = \rsimp{\rsimp{r}}$ +\end{lemma} + +\begin{proof} + By \ref{test} and \ref{good1}. +\end{proof} +\noindent +This property means we do not have to repeatedly +apply simplification in each step, which justifies +our definition of $\blexersimp$. + -We define rewriting relations for $\rrexp$s, which allows us to do the -same trick as we did for the correctness proof, -but this time we will have stronger equalities established. -\subsection{"hrewrite" relation} +On the other hand, we could repeat the same $\rsimp{}$ applications +on regular expressions as many times as we want, if we have at least +one simplification applied to it, and apply it wherever we would like to: +\begin{corollary}\label{headOneMoreSimp} + $\map \; \rsimp{(r :: rs)} = \map \; \rsimp{} \; (\rsimp{r} :: rs)$ +\end{corollary} +\noindent +This will be useful in later closed form proof's rewriting steps. +Similarly, we point out the following useful facts below: +\begin{lemma} + The following equalities hold if $r = \rsimp{r'}$ for some $r'$: + \begin{itemize} + \item + If $r = \sum rs$ then $\rsimpalts \; rs = \sum rs$. + \item + If $r = \sum rs$ then $\rdistinct{rs}{\varnothing} = rs$. + \item + $\rsimpalts \; (\rdistinct{\rflts \; [r]}{\varnothing}) = r$. + \end{itemize} +\end{lemma} +\begin{proof} + By application of \ref{rsimpIdem} and \ref{good1}. +\end{proof} + +\noindent +With the idempotency of $\rsimp{}$ and its corollaries, +we can start proving some key equalities leading to the +closed forms. +Now presented are a few equivalent terms under $\rsimp{}$. +We use $r_1 \sequal r_2 $ here to denote $\rsimp{r_1} = \rsimp{r_2}$. +\begin{lemma} +\begin{itemize} + \item + $\rsimpalts \; (\RZERO :: rs) \sequal \rsimpalts\; rs$ + \item + $\rsimpalts \; rs \sequal \rsimpalts (\map \; \rsimp{} \; rs)$ + \item + $\RALTS{\RALTS{rs}} \sequal \RALTS{rs}$ +\end{itemize} +\end{lemma} +\noindent +We need more equalities like the above to enable a closed form, +but to proceed we need to introduce two rewrite relations, +to make things smoother. +\subsubsection{The rewrite relation $\hrewrite$ and $\grewrite$} +Insired by the success we had in the correctness proof +in \ref{Bitcoded2}, where we invented +a term rewriting system to capture the similarity between terms +and prove equivalence, we follow suit here defining simplification +steps as rewriting steps. +The presentation will be more concise than that in \ref{Bitcoded2}. +To differentiate between the rewriting steps for annotated regular expressions +and $\rrexp$s, we add characters $h$ and $g$ below the squig arrow symbol +to mean atomic simplification transitions +of $\rrexp$s and $\rrexp$ lists, respectively. + +\begin{center} + List of 1-step rewrite rules for regular expressions simplification without bitcodes: \begin{figure} \caption{the "h-rewrite" rules} @@ -419,6 +710,25 @@ Fortunately this is provable by induction on the list $rs$ +\subsection{A Closed Form for the Sequence Regular Expression} +\begin{quote}\it + Claim: For regular expressions $r_1 \cdot r_2$, we claim that + \begin{center} + $ \rderssimp{r_1 \cdot r_2}{s} = + \rsimp{(\sum (r_1 \backslash s \cdot r_2 ) \; :: \;(\map \; \rderssimp{r2}{\_} \;(\vsuf{s}{r_1})))}$ + \end{center} +\end{quote} +\noindent + +Before we get to the proof that says the intermediate result of our lexer will +remain finitely bounded, which is an important efficiency/liveness guarantee, +we shall first develop a few preparatory properties and definitions to +make the process of proving that a breeze. + +We define rewriting relations for $\rrexp$s, which allows us to do the +same trick as we did for the correctness proof, +but this time we will have stronger equalities established. + \section{Estimating the Closed Forms' sizes} @@ -787,11 +1097,8 @@ \begin{lemma} $\rsimp{\sflat{(r_1 \cdot r_2) \backslash s} }= \rsimp{\AALTS{[[]}{ (r_1 \backslash s) \cdot r_2 :: (\map (r_2 \backslash \_) (\vsuf{s}{r_1}))}}$ \end{lemma} -Together with the idempotency property of $\rsimp$, +Together with the idempotency property of $\rsimp{}$\ref{rsimpIdem}, %TODO: state the idempotency property of rsimp -\begin{lemma} -$\rsimp{r} = \rsimp{\rsimp{r}}$ -\end{lemma} it is possible to convert the above lemma to obtain a "closed form" for derivatives nested with simplification: \begin{lemma} @@ -1088,17 +1395,6 @@ % SECTION 1 %---------------------------------------------------------------------------------------- -\section{Idempotency of $\simp$} - -\begin{equation} - \simp \;r = \simp\; \simp \; r -\end{equation} -This property means we do not have to repeatedly -apply simplification in each step, which justifies -our definition of $\blexersimp$. -It will also be useful in future proofs where properties such as -closed forms are needed. -The proof is by structural induction on $r$. %----------------------------------- % SUBSECTION 1 diff -r 0f00d440f484 -r 15d182ffbc76 ChengsongTanPhdThesis/Chapters/Introduction.tex --- a/ChengsongTanPhdThesis/Chapters/Introduction.tex Fri Jun 24 21:49:23 2022 +0100 +++ b/ChengsongTanPhdThesis/Chapters/Introduction.tex Sun Jun 26 22:22:47 2022 +0100 @@ -23,7 +23,7 @@ \newcommand{\rderssimp}[2]{#1 \backslash_{rsimp} #2} \newcommand{\bders}[2]{#1 \backslash #2} \newcommand{\bsimp}[1]{\textit{bsimp}(#1)} -\newcommand{\rsimp}[1]{\textit{rsimp}(#1)} +\newcommand{\rsimp}[1]{\textit{rsimp}\; #1} \newcommand{\sflataux}[1]{\llparenthesis #1 \rrparenthesis'} \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% \newcommand{\denote}{\stackrel{\mbox{\scriptsize denote}}{=}}% @@ -37,6 +37,11 @@ \newcommand\myequiv{\mathrel{\stackrel{\makebox[0pt]{\mbox{\normalfont\tiny equiv}}}{=}}} +\def\sequal{\stackrel{\mbox{\scriptsize rsimp}}{=}} +\def\rsimpalts{\textit{rsimp}_{ALTS}} +\def\good{\textit{good}} +\def\btrue{\textit{true}} +\def\bfalse{\textit{false}} \def\bnullable{\textit{bnullable}} \def\bnullables{\textit{bnullables}} \def\Some{\textit{Some}} @@ -48,10 +53,15 @@ \def\mkeps{\textit{mkeps}} \newcommand{\rder}[2]{#2 \backslash #1} +\def\nonnested{\textit{nonnested}} \def\AZERO{\textit{AZERO}} \def\AONE{\textit{AONE}} \def\ACHAR{\textit{ACHAR}} +\def\hrewrite{\stackrel[h]{\rightsquigarrow}} +\def\hrewrites{\stackrel[h]{*}{\rightsquigarrow} } +\def\grewrite{\stackrel[g]{\rightsquigarrow}} +\def\grewrites{\stackrel[g]{*}{\rightsquigarrow}} \def\fuse{\textit{fuse}} \def\bder{\textit{bder}} \def\der{\textit{der}} @@ -96,7 +106,7 @@ %\def\vsuf{\textit{vsuf}} %\def\sflataux{\textit{sflat}\_\textit{aux}} \def\rrexp{\textit{rrexp}} -\newcommand\rnullable[1]{\textit{rnullable}(#1)} +\newcommand\rnullable[1]{\textit{rnullable} \; #1 } \newcommand\rsize[1]{\llbracket #1 \rrbracket_r} \newcommand\asize[1]{\llbracket #1 \rrbracket} \newcommand\rerase[1]{ (#1)_{\downarrow_r}} diff -r 0f00d440f484 -r 15d182ffbc76 ChengsongTanPhdThesis/main.tex --- a/ChengsongTanPhdThesis/main.tex Fri Jun 24 21:49:23 2022 +0100 +++ b/ChengsongTanPhdThesis/main.tex Sun Jun 26 22:22:47 2022 +0100 @@ -274,6 +274,9 @@ \newtheorem{lemma}{Lemma} \newtheorem{definition}{Definition} \newtheorem{conjecture}{Conjecture} +\newtheorem{corollary}{Corollary} +\newtheorem{property}{Property} +\newtheorem{proposition}{Proposition} %proof diff -r 0f00d440f484 -r 15d182ffbc76 thys3/ClosedForms.thy --- a/thys3/ClosedForms.thy Fri Jun 24 21:49:23 2022 +0100 +++ b/thys3/ClosedForms.thy Sun Jun 26 22:22:47 2022 +0100 @@ -2,6 +2,7 @@ imports "BasicIdentities" begin + lemma flts_middle0: shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)" apply(induct rsa) @@ -288,14 +289,6 @@ -lemma all_that_same_elem: - shows "\ a \ rset; rdistinct rs {a} = []\ - \ rdistinct (rs @ rsb) rset = rdistinct rsb rset" - apply(induct rs) - apply simp - apply(subgoal_tac "aa = a") - apply simp - by (metis empty_iff insert_iff list.discI rdistinct.simps(2)) lemma distinct_early_app1: shows "rset1 \ rset \ rdistinct rs rset = rdistinct (rdistinct rs rset1) rset" @@ -390,7 +383,9 @@ rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (rsa @ rs @ rsb)) {}); rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp_ALTs (rdistinct (rflts (rsa @ [rsimp (RALTS rs)] @ rsb)) {}); - map rsimp rsa = rsa; map rsimp rsb = rsb; map rsimp rs = rs; + map rsimp rsa = rsa; + map rsimp rsb = rsb; + map rsimp rs = rs; rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} = rdistinct (rflts rsa) {} @ rdistinct (rflts rs @ rflts rsb) (set (rflts rsa)); rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} = @@ -439,7 +434,7 @@ prefer 2 apply (metis map_idI rsimp.simps(3) test) apply(simp only:) - apply(subst k00)+ + apply(subst flts_append)+ apply(subgoal_tac "map rsimp rs = rs") apply(simp only:) prefer 2 @@ -460,15 +455,6 @@ using good_flatten_aux by blast -lemma simp_flatten3: - shows "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))" -proof - - have "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = - rsimp (RALTS (map rsimp rsa @ [rsimp (RALTS rs)] @ map rsimp rsb)) " - by (metis append_Cons append_Nil list.simps(9) map_append simp_flatten_aux0) - apply(simp only:) - -oops lemma simp_flatten3: shows "rsimp (RALTS (rsa @ [RALTS rs ] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))" @@ -876,39 +862,8 @@ by (metis append.right_neutral grewrite.intros(2) grewrite_simpalts rsimp_ALTs.simps(2) simp_der_flts) -lemma basic_regex_property1: - shows "rnullable r \ rsimp r \ RZERO" - apply(induct r rule: rsimp.induct) - apply(auto) - apply (metis idiot idiot2 rrexp.distinct(5)) - by (metis der_simp_nullability rnullable.simps(1) rnullable.simps(4) rsimp.simps(2)) -lemma inside_simp_seq_nullable: - shows -"\r1 r2. - \rsimp (rder x (rsimp r1)) = rsimp (rder x r1); rsimp (rder x (rsimp r2)) = rsimp (rder x r2); - rnullable r1\ - \ rsimp (rder x (rsimp_SEQ (rsimp r1) (rsimp r2))) = - rsimp_ALTs (rdistinct (rflts [rsimp_SEQ (rsimp (rder x r1)) (rsimp r2), rsimp (rder x r2)]) {})" - apply(case_tac "rsimp r1 = RONE") - apply(simp) - apply(subst basic_rsimp_SEQ_property1) - apply (simp add: idem_after_simp1) - apply(case_tac "rsimp r1 = RZERO") - - using basic_regex_property1 apply blast - apply(case_tac "rsimp r2 = RZERO") - - apply (simp add: basic_rsimp_SEQ_property3) - apply(subst idiot2) - apply simp+ - apply(subgoal_tac "rnullable (rsimp r1)") - apply simp - using rsimp_idem apply presburger - using der_simp_nullability by presburger - - lemma grewrite_ralts: shows "rs \g rs' \ RALTS rs h\* RALTS rs'" @@ -1118,6 +1073,30 @@ +lemma inside_simp_seq_nullable: + shows +"\r1 r2. + \rsimp (rder x (rsimp r1)) = rsimp (rder x r1); rsimp (rder x (rsimp r2)) = rsimp (rder x r2); + rnullable r1\ + \ rsimp (rder x (rsimp_SEQ (rsimp r1) (rsimp r2))) = + rsimp_ALTs (rdistinct (rflts [rsimp_SEQ (rsimp (rder x r1)) (rsimp r2), rsimp (rder x r2)]) {})" + apply(case_tac "rsimp r1 = RONE") + apply(simp) + apply(subst basic_rsimp_SEQ_property1) + apply (simp add: idem_after_simp1) + apply(case_tac "rsimp r1 = RZERO") + using basic_regex_property1 apply blast + apply(case_tac "rsimp r2 = RZERO") + apply (simp add: basic_rsimp_SEQ_property3) + apply(subst idiot2) + apply simp+ + apply(subgoal_tac "rnullable (rsimp r1)") + apply simp + using rsimp_idem apply presburger + using der_simp_nullability by presburger + + + lemma inside_simp_removal: shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)" apply(induct r)