# HG changeset patch # User Chengsong # Date 1656446862 -3600 # Node ID aecf1ddf35415c9f146f66db6b6f14f089559019 # Parent 15d182ffbc7678ad9e97042a29b1a2f24f6c7696 more diff -r 15d182ffbc76 -r aecf1ddf3541 ChengsongTanPhdThesis/Chapters/Finite.tex --- a/ChengsongTanPhdThesis/Chapters/Finite.tex Sun Jun 26 22:22:47 2022 +0100 +++ b/ChengsongTanPhdThesis/Chapters/Finite.tex Tue Jun 28 21:07:42 2022 +0100 @@ -276,7 +276,7 @@ remove duplicates in an \emph{r}$\textit{rexp}$ list, according to the accumulator and leave only one of each different element in a list: -\begin{lemma} +\begin{lemma}\label{rdistinctDoesTheJob} The function $\textit{rdistinct}$ satisfies the following properties: \begin{itemize} @@ -284,12 +284,19 @@ If $a \in acc$ then $a \notin (\rdistinct{rs}{acc})$. \item If list $rs'$ is the result of $\rdistinct{rs}{acc}$, - All the elements in $rs'$ are unique. + then $\textit{isDistinct} \; rs'$. + \item + $\rdistinct{rs}{acc} = rs - acc$ \end{itemize} \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} The first part is by an induction on $rs$. - The second part can be proven by using the + The second and third part can be proven by using the induction rules of $\rdistinct{\_}{\_}$. \end{proof} @@ -338,17 +345,14 @@ when $\rdistinct{\_}{\_}$ becomes an identical mapping for any prefix of an input list, in other words, when can we ``push out" the arguments of $\rdistinct{\_}{\_}$: -\begin{lemma} +\begin{lemma}\label{distinctRdistinctAppend} If $\textit{isDistinct} \; rs_1$, and $rs_1 \cap acc = \varnothing$, - then it can be taken out and left untouched in the output: + then \[\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. +In other words, it can be taken out and left untouched in the output. \begin{proof} By an induction on $rs_1$, where $rsa$ and $acc$ are allowed to be arbitrary. \end{proof} @@ -359,12 +363,12 @@ The two properties hold if $r \in rs$: \begin{itemize} \item - $\rdistinct{rs}{rset} = \rdistinct{(rs @ [r])}{rset}$ - and + $\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{ (rs @ rs') }{rset} = \rdistinct{rs @ [r] @ rs'}{rset}$\\ + and\\ $\rdistinct{(ab :: rs @ [ab] @ rs'')}{rset'} = \rdistinct{(ab :: rs @ rs'')}{rset'}$ \end{itemize} @@ -377,6 +381,33 @@ so that the induction goes through. \end{proof} +\noindent +This allows us to prove ``Idempotency" of $\rdistinct{}{}$ of some kind: +\begin{lemma}\label{rdistinctConcatGeneral} + The following equalities involving multiple applications of $\rdistinct{}{}$ hold: + \begin{itemize} + \item + $\rdistinct{(rs @ rs')}{\varnothing} = \rdistinct{((\rdistinct{rs}{\varnothing})@ rs')}{\varnothing}$ + \item + $\rdistinct{(rs @ rs')}{\varnothing} = \rdistinct{(\rdistinct{rs}{\varnothing} @ rs')}{\varnothing}$ + \item + If $rset' \subseteq rset$, then $\rdistinct{rs}{rset} = + \rdistinct{(\rdistinct{rs}{rset'})}{rset}$. As a corollary + of this, + \item + $\rdistinct{(rs @ rs')}{rset} = \rdistinct{ + (\rdistinct{rs}{\varnothing}) @ rs')}{rset}$. This + gives another corollary use later: + \item + If $a \in rset$, then $\rdistinct{(rs @ rs')}{rset} = \rdistinct{ + (\rdistinct{(a :: rs)}{\varnothing} @ rs')}{rset} $, + + \end{itemize} +\end{lemma} +\begin{proof} + By \ref{rdistinctDoesTheJob} and \ref{distinctRemovesMiddle}. +\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 @@ -403,13 +434,20 @@ \item If $r \neq \RZERO$ and $\nexists rs'. r = \RALTS{rs'}$ then $\rflts \; (rs @ [r]) = (\rflts \; rs) @ [r]$ + \item + If $r = \RALTS{rs}$ and $r \in rs'$ then for all $r_1 \in rs. + r_1 \in \rflts \; rs'$. + \item + $\rflts \; (rs_a @ \RZERO :: rs_b) = \rflts \; (rs_a @ rs_b)$ \end{itemize} \end{lemma} \noindent \begin{proof} - 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. + By induction on $rs_1$ in the first sub-lemma, and induction on $r$ in the second part, + and induction on $rs$, $rs'$, $rs$, $rs'$, $rs_a$ in the third, fourth, fifth, sixth and + last 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. @@ -594,7 +632,30 @@ The lemma \ref{goodaltsNonalt} is used in the alternative case where 2 or more elements are present in the list. \end{proof} +\noindent +Given below is a property involving $\rflts$, $\rdistinct{}{}$, $\rsimp{}$ and $\rsimp_{ALTS}$, +which requires $\ref{good1}$ to go through smoothly. +It says that an application of $\rsimp_{ALTS}$ can be "absorbed", +if it its output is concatenated with a list and then applied to $\rflts$. +\begin{lemma}\label{flattenRsimpalts} + $\rflts \; ( (\rsimp_{ALTS} \; + (\rdistinct{(\rflts \; (\map \; \rsimp{}\; rs))}{\varnothing})) :: + \map \; \rsimp{} \; rs' ) = + \rflts \; ( (\rdistinct{(\rflts \; (\map \; \rsimp{}\; rs))}{\varnothing}) @ ( + \map \; \rsimp{rs'}))$ + +\end{lemma} +\begin{proof} + By \ref{good1}. +\end{proof} +\noindent + + + + + +We are also \subsubsection{$\rsimp$ is Idempotent} The idempotency of $\rsimp$ is very useful in manipulating regular expression terms into desired @@ -617,7 +678,14 @@ 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)$ + The following properties hold, directly from \ref{rsimpIdem}: + + \begin{itemize} + \item + $\map \; \rsimp{(r :: rs)} = \map \; \rsimp{} \; (\rsimp{r} :: rs)$ + \item + $\rsimp{(\RALTS{rs})} = \rsimp{(\RALTS{\map \; \rsimp{} \; rs})}$ + \end{itemize} \end{corollary} \noindent This will be useful in later closed form proof's rewriting steps. @@ -645,42 +713,152 @@ We use $r_1 \sequal r_2 $ here to denote $\rsimp{r_1} = \rsimp{r_2}$. \begin{lemma} \begin{itemize} + The following equivalence hold: \item $\rsimpalts \; (\RZERO :: rs) \sequal \rsimpalts\; rs$ \item $\rsimpalts \; rs \sequal \rsimpalts (\map \; \rsimp{} \; rs)$ \item $\RALTS{\RALTS{rs}} \sequal \RALTS{rs}$ + \item + $\sum ((\sum rs_a) :: rs_b) \sequal \sum rs_a @ rs_b$ + \item + $\RALTS{rs} = \RALTS{\map \; \rsimp{} \; rs}$ \end{itemize} \end{lemma} +\begin{proof} + By induction on the lists involved. +\end{proof} +\noindent +Similarly, +we introduce the equality for $\sum$ when certain child regular expressions +are $\sum$ themselves: +\begin{lemma}\label{simpFlatten3} + One can flatten the inside $\sum$ of a $\sum$ if it is being + simplified. Concretely, + \begin{itemize} + \item + If for all $r \in rs, rs', rs''$, we have $\good \; r $ + or $r = \RZERO$, then $\sum (rs' @ rs @ rs'') \sequal + \sum (rs' @ [\sum rs] @ rs'')$ holds. As a corollary, + \item + $\sum (rs' @ [\sum rs] @ rs'') \sequal \sum (rs' @ rs @ rs'')$ + \end{itemize} +\end{lemma} +\begin{proof} + By rewriting steps involving the use of \ref{test} and \ref{rdistinctConcatGeneral}. + The second sub-lemma is a corollary of the previous. +\end{proof} +%Rewriting steps not put in--too long and complicated------------------------------- +\begin{comment} + \begin{center} + $\rsimp{\sum (rs' @ rs @ rs'')} \stackrel{def of bsimp}{=}$ \\ + $\rsimpalts \; (\rdistinct{\rflts \; ((\map \; \rsimp{}\; rs') @ (\map \; \rsimp{} \; rs ) @ (\map \; \rsimp{} \; rs''))}{\varnothing})$ \\ + $\stackrel{by \ref{test}}{=} + \rsimpalts \; (\rdistinct{(\rflts \; rs' @ \rflts \; rs @ \rflts \; rs'')}{ + \varnothing})$\\ + $\stackrel{by \ref{rdistinctConcatGeneral}}{=} + \rsimpalts \; (\rdistinct{\rflts \; rs'}{\varnothing} @ \rdistinct{( + \rflts\; rs @ \rflts \; rs'')}{\rflts \; rs'})$\\ + + \end{center} +\end{comment} +%Rewriting steps not put in--too long and complicated------------------------------- \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$} +\subsubsection{The rewrite relation $\hrewrite$, $\frewrite$ 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. +a term rewriting system to capture the similarity between terms, +we follow suit here defining simplification +steps as rewriting steps. This allows capturing +similarities between terms that would be otherwise +hard to express. + +We use $\hrewrite$ for one-step atomic rewrite of regular expression simplification, +$\frewrite$ for rewrite of list of regular expressions that +include all operations carried out in $\rflts$, and $\grewrite$ for +rewriting a list of regular expressions possible in both $\rflts$ and $\rdistinct{}{}$. +Their reflexive transitive closures are used to denote zero or many steps, +as was the case in the previous chapter. 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. + + + List of one-step rewrite rules for $\rrexp$ ($\hrewrite$): + + \begin{center} +\begin{mathpar} + \inferrule[RSEQ0L]{}{\RZERO \cdot r_2 \hrewrite \RZERO\\} + + \inferrule[RSEQ0R]{}{r_1 \cdot \RZERO \hrewrite \RZERO\\} + + \inferrule[RSEQ1]{}{(\RONE \cdot r) \hrewrite r\\}\\ + + \inferrule[RSEQL]{ r_1 \hrewrite r_2}{r_1 \cdot r_3 \hrewrite r_2 \cdot r_3\\} + + \inferrule[RSEQR]{ r_3 \hrewrite r_4}{r_1 \cdot r_3 \hrewrite r_1 \cdot r_4\\}\\ + + \inferrule[RALTSChild]{r \hrewrite r'}{\sum (rs_1 @ [r] @ rs_2) \hrewrite \sum (rs_1 @ [r'] @ rs_2)\\} + + \inferrule[RALTS0]{}{\sum (rs_a @ [\RZERO] @ rs_b) \hrewrite \sum (rs_a @ rs_b)} + + \inferrule[RALTSNested]{}{\sum (rs_a @ [\sum rs_1] @ rs_b) \hrewrite \sum (rs_a @ rs_1 @ rs_b)} + + \inferrule[RALTSNil]{}{ \sum [] \hrewrite \RZERO\\} + + \inferrule[RALTSSingle]{}{ \sum [r] \hrewrite r\\} + + \inferrule[RALTSDelete]{\\ r_1 = r_2}{\sum rs_a @ [r_1] @ rs_b @ [r_2] @ rsc \hrewrite \sum rs_a @ [r_1] @ rs_b @ rs_c} + +\end{mathpar} +\end{center} -List of 1-step rewrite rules for regular expressions simplification without bitcodes: -\begin{figure} -\caption{the "h-rewrite" rules} -\[ -r_1 \cdot \ZERO \rightarrow_h \ZERO \] +%frewrite + List of one-step rewrite rules for flattening + a list of regular expressions($\frewrite$): +\begin{center} +\begin{mathpar} + \inferrule{}{\RZERO :: rs \frewrite rs \\} + + \inferrule{}{(\sum rs) :: rs_a \frewrite rs @ rs_a \\} + + \inferrule{rs_1 \frewrite rs_2}{r :: rs_1 \frewrite r :: rs_2} +\end{mathpar} +\end{center} + + Lists of one-step rewrite rules for flattening and de-duplicating + a list of regular expressions ($\grewrite$): +\begin{center} +\begin{mathpar} + \inferrule{}{\RZERO :: rs \frewrite rs \\} -\[ -\ZERO \cdot r_2 \rightarrow \ZERO -\] -\end{figure} + \inferrule{}{(\sum rs) :: rs_a \frewrite rs @ rs_a \\} + + \inferrule{rs_1 \frewrite rs_2}{r :: rs_1 \frewrite r :: rs_2} + + \inferrule[dB]{}{rs_a @ [a] @ rs_b @[a] @ rs_c \grewrite rs_a @ [a] @ rsb @ rsc} +\end{mathpar} +\end{center} + +\noindent +The reason why we take the trouble of defining +two separate list rewriting definitions $\frewrite$ and $\grewrite$ +is that sometimes $\grewrites$ is slightly too powerful +that it renders certain equivalence to break after derivative: + +$\rsimp{(\rsimpalts \; (\map \; (\_ \backslash x) \; (\rdistinct{(\rflts \; (\map \; (\rsimp{} \; \circ \; (\lambda r. \rderssimp{r}{xs}))))}{\varnothing})))} \neq + \rsimp{(\rsimpalts \; (\rdistinct{(\map \; (\_ \backslash x) \; (\rflts \; (\map \; (\rsimp{} \; \circ \; (\lambda r. \rderssimp{r}{xs})))) ) }{\varnothing})} $ + + + And we define an "grewrite" relation that works on lists: \begin{center} \begin{tabular}{lcl} diff -r 15d182ffbc76 -r aecf1ddf3541 ChengsongTanPhdThesis/Chapters/Introduction.tex --- a/ChengsongTanPhdThesis/Chapters/Introduction.tex Sun Jun 26 22:22:47 2022 +0100 +++ b/ChengsongTanPhdThesis/Chapters/Introduction.tex Tue Jun 28 21:07:42 2022 +0100 @@ -30,7 +30,7 @@ \newcommand{\ZERO}{\mbox{\bf 0}} \newcommand{\ONE}{\mbox{\bf 1}} \newcommand{\AALTS}[2]{\oplus {\scriptstyle #1}\, #2} -\newcommand{\rdistinct}[2]{\textit{rdistinct} \; \textit{#1} \; #2} +\newcommand{\rdistinct}[2]{\textit{rdistinct} \;\; #1 \;\; #2} \newcommand\hflat[1]{\llparenthesis #1 \rrparenthesis_*} \newcommand\hflataux[1]{\llparenthesis #1 \rrparenthesis_*'} \newcommand\createdByStar[1]{\textit{createdByStar}(#1)} @@ -58,10 +58,12 @@ \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\frewrite{\rightsquigarrow_f} +\def\hrewrite{\rightsquigarrow_h} +\def\grewrite{\rightsquigarrow_g} +\def\frewrites{\stackrel{*}{\rightsquigarrow_f}} +\def\hrewrites{\stackrel{*}{\rightsquigarrow_h}} +\def\grewrites{\stackrel{*}{\rightsquigarrow_g}} \def\fuse{\textit{fuse}} \def\bder{\textit{bder}} \def\der{\textit{der}} diff -r 15d182ffbc76 -r aecf1ddf3541 ChengsongTanPhdThesis/main.tex --- a/ChengsongTanPhdThesis/main.tex Sun Jun 26 22:22:47 2022 +0100 +++ b/ChengsongTanPhdThesis/main.tex Tue Jun 28 21:07:42 2022 +0100 @@ -42,6 +42,7 @@ \usepackage[T1]{fontenc} % Output font encoding for international characters %\usepackage{fdsymbol} % Loads unicode-math +\usepackage{verbatim} \usepackage{mathpazo} % Use the Palatino font by default \usepackage{hyperref} \usepackage{lipsum} @@ -72,7 +73,7 @@ \usetikzlibrary{fit, shapes.geometric} \usepackage{mathpartir} - +\usepackage{stackrel} \DeclareCaptionType{mytype}[Illustration][] \newenvironment{envForCaption}{\captionsetup{type=mytype} }{} diff -r 15d182ffbc76 -r aecf1ddf3541 thys3/ClosedForms.thy --- a/thys3/ClosedForms.thy Sun Jun 26 22:22:47 2022 +0100 +++ b/thys3/ClosedForms.thy Tue Jun 28 21:07:42 2022 +0100 @@ -1,20 +1,8 @@ theory ClosedForms - imports "BasicIdentities" + imports "HarderProps" begin -lemma flts_middle0: - shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)" - apply(induct rsa) - apply simp - by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) - - - -lemma simp_flatten_aux0: - shows "rsimp (RALTS rs) = rsimp (RALTS (map rsimp rs))" - by (metis append_Nil head_one_more_simp identity_wwo0 list.simps(8) rdistinct.simps(1) rflts.simps(1) rsimp.simps(2) rsimp_ALTs.simps(1) rsimp_ALTs.simps(3) simp_flatten spawn_simp_rsimpalts) - inductive hrewrite:: "rrexp \ rrexp \ bool" ("_ h\ _" [99, 99] 99) @@ -68,44 +56,8 @@ by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2) -lemma simp_removes_duplicate1: - shows " a \ set rsa \ rsimp (RALTS (rsa @ [a])) = rsimp (RALTS (rsa))" -and " rsimp (RALTS (a1 # rsa @ [a1])) = rsimp (RALTS (a1 # rsa))" - apply(induct rsa arbitrary: a1) - apply simp - apply simp - prefer 2 - apply(case_tac "a = aa") - apply simp - apply simp - apply (metis Cons_eq_appendI Cons_eq_map_conv distinct_removes_duplicate_flts list.set_intros(2)) - apply (metis append_Cons append_Nil distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9)) - by (metis (mono_tags, lifting) append_Cons distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9) map_append rsimp.simps(2)) - -lemma simp_removes_duplicate2: - shows "a \ set rsa \ rsimp (RALTS (rsa @ [a] @ rsb)) = rsimp (RALTS (rsa @ rsb))" - apply(induct rsb arbitrary: rsa) - apply simp - using distinct_removes_duplicate_flts apply auto[1] - by (metis append.assoc head_one_more_simp rsimp.simps(2) simp_flatten simp_removes_duplicate1(1)) -lemma simp_removes_duplicate3: - shows "a \ set rsa \ rsimp (RALTS (rsa @ a # rsb)) = rsimp (RALTS (rsa @ rsb))" - using simp_removes_duplicate2 by auto -(* -lemma distinct_removes_middle4: - shows "a \ set rsa \ rdistinct (rsa @ [a] @ rsb) rset = rdistinct (rsa @ rsb) rset" - using distinct_removes_middle(1) by fastforce -*) - -(* -lemma distinct_removes_middle_list: - shows "\a \ set x. a \ set rsa \ rdistinct (rsa @ x @ rsb) rset = rdistinct (rsa @ rsb) rset" - apply(induct x) - apply simp - by (simp add: distinct_removes_middle3) -*) inductive frewrite:: "rrexp list \ rrexp list \ bool" ("_ \f _" [10, 10] 10) where @@ -260,11 +212,6 @@ using grewrites_append apply blast by (meson greal_trans grewrites.simps grewrites_concat) -fun alt_set:: "rrexp \ rrexp set" - where - "alt_set (RALTS rs) = set rs \ \ (alt_set ` (set rs))" -| "alt_set r = {r}" - lemma grewrite_cases_middle: shows "rs1 \g rs2 \ @@ -279,211 +226,6 @@ by blast -lemma good_singleton: - shows "good a \ nonalt a \ rflts [a] = [a]" - using good.simps(1) k0b by blast - - - - - - - - -lemma distinct_early_app1: - shows "rset1 \ rset \ rdistinct rs rset = rdistinct (rdistinct rs rset1) rset" - apply(induct rs arbitrary: rset rset1) - apply simp - apply simp - apply(case_tac "a \ rset1") - apply simp - apply(case_tac "a \ rset") - apply simp+ - - apply blast - apply(case_tac "a \ rset1") - apply simp+ - apply(case_tac "a \ rset") - apply simp - apply (metis insert_subsetI) - apply simp - by (meson insert_mono) - - -lemma distinct_early_app: - shows " rdistinct (rs @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset" - apply(induct rsb) - apply simp - using distinct_early_app1 apply blast - by (metis distinct_early_app1 distinct_once_enough empty_subsetI) - - -lemma distinct_eq_interesting1: - shows "a \ rset \ rdistinct (rs @ rsb) rset = rdistinct (rdistinct (a # rs) {} @ rsb) rset" - apply(subgoal_tac "rdistinct (rdistinct (a # rs) {} @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset") - apply(simp only:) - using distinct_early_app apply blast - by (metis append_Cons distinct_early_app rdistinct.simps(2)) - - - -lemma good_flatten_aux_aux1: - shows "\ size rs \2; -\r \ set rs. good r \ r \ RZERO \ nonalt r; \r \ set rsb. good r \ r \ RZERO \ nonalt r \ - \ rdistinct (rs @ rsb) rset = - rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset" - apply(induct rs arbitrary: rset) - apply simp - apply(case_tac "a \ rset") - apply simp - apply(case_tac "rdistinct rs {a}") - apply simp - apply(subst good_singleton) - apply force - apply simp - apply (meson all_that_same_elem) - apply(subgoal_tac "rflts [rsimp_ALTs (a # rdistinct rs {a})] = a # rdistinct rs {a} ") - prefer 2 - using k0a rsimp_ALTs.simps(3) apply presburger - apply(simp only:) - apply(subgoal_tac "rdistinct (rs @ rsb) rset = rdistinct ((rdistinct (a # rs) {}) @ rsb) rset ") - apply (metis insert_absorb insert_is_Un insert_not_empty rdistinct.simps(2)) - apply (meson distinct_eq_interesting1) - apply simp - apply(case_tac "rdistinct rs {a}") - prefer 2 - apply(subgoal_tac "rsimp_ALTs (a # rdistinct rs {a}) = RALTS (a # rdistinct rs {a})") - apply(simp only:) - apply(subgoal_tac "a # rdistinct (rs @ rsb) (insert a rset) = - rdistinct (rflts [RALTS (a # rdistinct rs {a})] @ rsb) rset") - apply simp - apply (metis append_Cons distinct_early_app empty_iff insert_is_Un k0a rdistinct.simps(2)) - using rsimp_ALTs.simps(3) apply presburger - by (metis Un_insert_left append_Cons distinct_early_app empty_iff good_singleton rdistinct.simps(2) rsimp_ALTs.simps(2) sup_bot_left) - - - - - -lemma good_flatten_aux_aux: - shows "\\a aa lista list. rs = a # list \ list = aa # lista; -\r \ set rs. good r \ r \ RZERO \ nonalt r; \r \ set rsb. good r \ r \ RZERO \ nonalt r \ - \ rdistinct (rs @ rsb) rset = - rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset" - apply(erule exE)+ - apply(subgoal_tac "size rs \ 2") - apply (metis good_flatten_aux_aux1) - by (simp add: Suc_leI length_Cons less_add_Suc1) - - - -lemma good_flatten_aux: - shows " \\r\set rs. good r \ r = RZERO; \r\set rsa . good r \ r = RZERO; - \r\set rsb. good r \ r = RZERO; - 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; - 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) {} = - rdistinct (rflts rsa) {} @ rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))\ - \ rdistinct (rflts rs @ rflts rsb) rset = - rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) rset" - apply simp - apply(case_tac "rflts rs ") - apply simp - apply(case_tac "list") - apply simp - apply(case_tac "a \ rset") - apply simp - apply (metis append.left_neutral append_Cons equals0D k0b list.set_intros(1) nonalt_flts_rd qqq1 rdistinct.simps(2)) - apply simp - apply (metis Un_insert_left append_Cons append_Nil ex_in_conv flts_single1 insertI1 list.simps(15) nonalt_flts_rd nonazero.elims(3) qqq1 rdistinct.simps(2) sup_bot_left) - apply(subgoal_tac "\r \ set (rflts rs). good r \ r \ RZERO \ nonalt r") - prefer 2 - apply (metis Diff_empty flts3 nonalt_flts_rd qqq1 rdistinct_set_equality1) - apply(subgoal_tac "\r \ set (rflts rsb). good r \ r \ RZERO \ nonalt r") - prefer 2 - apply (metis Diff_empty flts3 good.simps(1) nonalt_flts_rd rdistinct_set_equality1) - by (smt (verit, ccfv_threshold) good_flatten_aux_aux) - - - - -lemma good_flatten_middle: - shows "\\r \ set rs. good r \ r = RZERO; \r \ set rsa. good r \ r = RZERO; \r \ set rsb. good r \ r = RZERO\ \ -rsimp (RALTS (rsa @ rs @ rsb)) = rsimp (RALTS (rsa @ [RALTS rs] @ rsb))" - apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @ -map rsimp rs @ map rsimp rsb)) {})") - prefer 2 - apply simp - apply(simp only:) - apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @ -[rsimp (RALTS rs)] @ map rsimp rsb)) {})") - prefer 2 - apply simp - apply(simp only:) - apply(subgoal_tac "map rsimp rsa = rsa") - prefer 2 - apply (metis map_idI rsimp.simps(3) test) - apply(simp only:) - apply(subgoal_tac "map rsimp rsb = rsb") - prefer 2 - apply (metis map_idI rsimp.simps(3) test) - apply(simp only:) - apply(subst flts_append)+ - apply(subgoal_tac "map rsimp rs = rs") - apply(simp only:) - prefer 2 - apply (metis map_idI rsimp.simps(3) test) - apply(subgoal_tac "rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} = -rdistinct (rflts rsa) {} @ rdistinct (rflts rs @ rflts rsb) (set (rflts rsa))") - apply(simp only:) - prefer 2 - using rdistinct_concat_general apply blast - apply(subgoal_tac "rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} = -rdistinct (rflts rsa) {} @ rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))") - apply(simp only:) - prefer 2 - using rdistinct_concat_general apply blast - apply(subgoal_tac "rdistinct (rflts rs @ rflts rsb) (set (rflts rsa)) = - rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))") - apply presburger - using good_flatten_aux by blast - - - -lemma simp_flatten3: - shows "rsimp (RALTS (rsa @ [RALTS rs ] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))" - apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = - rsimp (RALTS (map rsimp rsa @ [rsimp (RALTS rs)] @ map rsimp rsb)) ") - prefer 2 - apply (metis append.left_neutral append_Cons list.simps(9) map_append simp_flatten_aux0) - apply (simp only:) - apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = -rsimp (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb))") - prefer 2 - apply (metis map_append simp_flatten_aux0) - apply(simp only:) - apply(subgoal_tac "rsimp (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb)) = - rsimp (RALTS (map rsimp rsa @ [RALTS (map rsimp rs)] @ map rsimp rsb))") - - apply (metis (no_types, lifting) head_one_more_simp map_append simp_flatten_aux0) - apply(subgoal_tac "\r \ set (map rsimp rsa). good r \ r = RZERO") - apply(subgoal_tac "\r \ set (map rsimp rs). good r \ r = RZERO") - apply(subgoal_tac "\r \ set (map rsimp rsb). good r \ r = RZERO") - - using good_flatten_middle apply presburger - - apply (simp add: good1) - apply (simp add: good1) - apply (simp add: good1) - - done - @@ -1286,6 +1028,16 @@ by fastforce +fun vsuf :: "char list \ rrexp \ char list list" where +"vsuf [] _ = []" +|"vsuf (c#cs) r1 = (if (rnullable r1) then (vsuf cs (rder c r1)) @ [c # cs] + else (vsuf cs (rder c r1)) + ) " + + + + + lemma vsuf_prop1: shows "vsuf (xs @ [x]) r = (if (rnullable (rders r xs)) then [x] # (map (\s. s @ [x]) (vsuf xs r) ) @@ -1533,6 +1285,30 @@ (*AALTS [a\x . b.c, b\x .c, c \x]*) (*AALTS [a\x . b.c, AALTS [b\x .c, c\x]]*) +fun star_update :: "char \ rrexp \ char list list \ char list list" where +"star_update c r [] = []" +|"star_update c r (s # Ss) = (if (rnullable (rders r s)) + then (s@[c]) # [c] # (star_update c r Ss) + else (s@[c]) # (star_update c r Ss) )" + + +fun star_updates :: "char list \ rrexp \ char list list \ char list list" + where +"star_updates [] r Ss = Ss" +| "star_updates (c # cs) r Ss = star_updates cs r (star_update c r Ss)" + + +lemma stupdates_append: shows +"star_updates (s @ [c]) r Ss = star_update c r (star_updates s r Ss)" + apply(induct s arbitrary: Ss) + apply simp + apply simp + done + + + + + lemma stupdate_induct1: shows " concat (map (hflat_aux \ (rder x \ (\s1. RSEQ (rders r0 s1) (RSTAR r0)))) Ss) = map (\s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_update x r0 Ss)"