--- 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}
--- 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}}
--- 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} }{}
--- 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 \<Rightarrow> rrexp \<Rightarrow> bool" ("_ h\<leadsto> _" [99, 99] 99)
@@ -68,44 +56,8 @@
by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2)
-lemma simp_removes_duplicate1:
- shows " a \<in> set rsa \<Longrightarrow> 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 \<in> set rsa \<Longrightarrow> 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 \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ a # rsb)) = rsimp (RALTS (rsa @ rsb))"
- using simp_removes_duplicate2 by auto
-(*
-lemma distinct_removes_middle4:
- shows "a \<in> set rsa \<Longrightarrow> rdistinct (rsa @ [a] @ rsb) rset = rdistinct (rsa @ rsb) rset"
- using distinct_removes_middle(1) by fastforce
-*)
-
-(*
-lemma distinct_removes_middle_list:
- shows "\<forall>a \<in> set x. a \<in> set rsa \<Longrightarrow> rdistinct (rsa @ x @ rsb) rset = rdistinct (rsa @ rsb) rset"
- apply(induct x)
- apply simp
- by (simp add: distinct_removes_middle3)
-*)
inductive frewrite:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>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 \<Rightarrow> rrexp set"
- where
- "alt_set (RALTS rs) = set rs \<union> \<Union> (alt_set ` (set rs))"
-| "alt_set r = {r}"
-
lemma grewrite_cases_middle:
shows "rs1 \<leadsto>g rs2 \<Longrightarrow>
@@ -279,211 +226,6 @@
by blast
-lemma good_singleton:
- shows "good a \<and> nonalt a \<Longrightarrow> rflts [a] = [a]"
- using good.simps(1) k0b by blast
-
-
-
-
-
-
-
-
-lemma distinct_early_app1:
- shows "rset1 \<subseteq> rset \<Longrightarrow> rdistinct rs rset = rdistinct (rdistinct rs rset1) rset"
- apply(induct rs arbitrary: rset rset1)
- apply simp
- apply simp
- apply(case_tac "a \<in> rset1")
- apply simp
- apply(case_tac "a \<in> rset")
- apply simp+
-
- apply blast
- apply(case_tac "a \<in> rset1")
- apply simp+
- apply(case_tac "a \<in> 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 \<in> rset \<Longrightarrow> 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 "\<lbrakk> size rs \<ge>2;
-\<forall>r \<in> set rs. good r \<and> r \<noteq> RZERO \<and> nonalt r; \<forall>r \<in> set rsb. good r \<and> r \<noteq> RZERO \<and> nonalt r \<rbrakk>
- \<Longrightarrow> rdistinct (rs @ rsb) rset =
- rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset"
- apply(induct rs arbitrary: rset)
- apply simp
- apply(case_tac "a \<in> 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 "\<lbrakk>\<exists>a aa lista list. rs = a # list \<and> list = aa # lista;
-\<forall>r \<in> set rs. good r \<and> r \<noteq> RZERO \<and> nonalt r; \<forall>r \<in> set rsb. good r \<and> r \<noteq> RZERO \<and> nonalt r \<rbrakk>
- \<Longrightarrow> rdistinct (rs @ rsb) rset =
- rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset"
- apply(erule exE)+
- apply(subgoal_tac "size rs \<ge> 2")
- apply (metis good_flatten_aux_aux1)
- by (simp add: Suc_leI length_Cons less_add_Suc1)
-
-
-
-lemma good_flatten_aux:
- shows " \<lbrakk>\<forall>r\<in>set rs. good r \<or> r = RZERO; \<forall>r\<in>set rsa . good r \<or> r = RZERO;
- \<forall>r\<in>set rsb. good r \<or> 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))\<rbrakk>
- \<Longrightarrow> 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 \<in> 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 "\<forall>r \<in> set (rflts rs). good r \<and> r \<noteq> RZERO \<and> nonalt r")
- prefer 2
- apply (metis Diff_empty flts3 nonalt_flts_rd qqq1 rdistinct_set_equality1)
- apply(subgoal_tac "\<forall>r \<in> set (rflts rsb). good r \<and> r \<noteq> RZERO \<and> 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 "\<lbrakk>\<forall>r \<in> set rs. good r \<or> r = RZERO; \<forall>r \<in> set rsa. good r \<or> r = RZERO; \<forall>r \<in> set rsb. good r \<or> r = RZERO\<rbrakk> \<Longrightarrow>
-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 "\<forall>r \<in> set (map rsimp rsa). good r \<or> r = RZERO")
- apply(subgoal_tac "\<forall>r \<in> set (map rsimp rs). good r \<or> r = RZERO")
- apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsb). good r \<or> 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 \<Rightarrow> rrexp \<Rightarrow> 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 (\<lambda>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 \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> 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 \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> 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 \<circ> (rder x \<circ> (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)))) Ss) =
map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_update x r0 Ss)"