regexp: comparison Myhill.thy

equal deleted inserted replaced

-:61d9684a557a
+:59936c012add
 qed
 subsubsection {* The case for @{const "STAR"} *}
 text {*
-This turned out to be the trickiest case.
+This turned out to be the trickiest case. The essential goal is
-Any string @{text "x"} in language @{text "L\<^isub>1\<star>"},
+to proved @{text "y @ z \<in>  L\<^isub>1*"} under the assumptions that @{text "x @ z \<in>  L\<^isub>1*"}
-can be splited into a prefix @{text "xa \<in> L\<^isub>1\<star>"} and a suffix @{text "x - xa \<in> L\<^isub>1"}.
+and that @{text "x"} and @{text "y"} have the same tag. The reasoning goes as the following:
-For one such @{text "x"}, there can be many such splits. The tagging of @{text "x"} is then
+\begin{enumerate}
-defined by collecting the @{text "L\<^isub>1"}-state of the suffixe from every possible split.
+\item Since @{text "x @ z \<in>  L\<^isub>1*"} holds, a prefix @{text "xa"} of @{text "x"} can be found
+such that @{text "xa \<in> L\<^isub>1*"} and @{text "(x - xa)@z \<in> L\<^isub>1*"}, as shown in Fig. \ref{first_split}(a).
+Such a prefix always exists, @{text "xa = []"}, for example, is one.
+\item There could be many but fintie many of such @{text "xa"}, from which we can find the longest
+and name it @{text "xa_max"}, as shown in Fig. \ref{max_split}(b).
+\item The next step is to split @{text "z"} into @{text "za"} and @{text "zb"} such that
+@{text "(x - xa_max) @ za \<in> L\<^isub>1"} and @{text "zb \<in> L\<^isub>1*"}  as shown in Fig. \ref{last_split}(d).
+Such a split always exists because:
+\begin{enumerate}
+\item Because @{text "(x - x_max) @ z \<in> L\<^isub>1*"}, it can always be split into prefix @{text "a"}
+and suffix @{text "b"}, such that @{text "a \<in> L\<^isub>1"} and @{text "b \<in> L\<^isub>1*"},
+as shown in Fig. \ref{ab_split}(c).
+\item But the prefix @{text "a"} CANNOT be shorter than @{text "x - xa_max"}, otherwise
+@{text "xa_max"} is not the max in it's kind.
+\item Now, @{text "za"} is just @{text "a - (x - xa_max)"} and @{text "zb"} is just @{text "b"}.
+\end{enumerate}
+\item  \label{tansfer_step}
+By the assumption that @{text "x"} and @{text "y"} have the same tag, the structure on @{text "x @ z"}
+can be transferred to @{text "y @ z"} as shown in Fig. \ref{trans_split}(e). The detailed steps are:
+\begin{enumerate}
+\item A @{text "y"}-prefix @{text "ya"} corresponding to @{text "xa"} can be found,
+which satisfies conditions: @{text "ya \<in> L\<^isub>1*"} and @{text "(y - ya)@za \<in> L\<^isub>1"}.
+\item Since we already know @{text "zb \<in> L\<^isub>1*"}, we get @{text "(y - ya)@za@zb \<in> L\<^isub>1*"},
+and this is just @{text "(y - ya)@z \<in> L\<^isub>1*"}.
+\item With fact @{text "ya \<in> L\<^isub>1*"}, we finally get @{text "y@z \<in> L\<^isub>1*"}.
+\end{enumerate}
+\end{enumerate}
+The formal proof of lemma @{text "tag_str_STAR_injI"} faithfully follows this informal argument
+while the tagging function @{text "tag_str_STAR"} is defined to make the transfer in step
+\ref{transfer_step}4 feasible.
+\begin{figure}[h!]
+\centering
+\subfigure[First split]{\label{first_split}
+\scalebox{0.9}{
+\begin{tikzpicture}
+\node[draw,minimum height=3.8ex] (xa) {$\hspace{2em}xa\hspace{2em}$};
+\node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{5em}x - xa\hspace{5em}$ };
+\node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{21em}$ };
+\draw[decoration={brace,transform={yscale=3}},decorate]
+(xa.north west) -- ($(xxa.north east)+(0em,0em)$)
+node[midway, above=0.5em]{$x$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+(z.north west) -- ($(z.north east)+(0em,0em)$)
+node[midway, above=0.5em]{$z$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
+node[midway, above=0.8em]{$x @ z \in L_1*$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
+node[midway, below=0.5em]{$(x - xa) @ z \in L_1*$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
+node[midway, below=0.5em]{$xa \in L_1*$};
+\end{tikzpicture}}}
+\subfigure[Max split]{\label{max_split}
+\scalebox{0.9}{
+\begin{tikzpicture}
+\node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}xa\_max\hspace{4em}$ };
+\node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - xa\_max\hspace{0.5em}$ };
+\node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{21em}$ };
+\draw[decoration={brace,transform={yscale=3}},decorate]
+(xa.north west) -- ($(xxa.north east)+(0em,0em)$)
+node[midway, above=0.5em]{$x$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+(z.north west) -- ($(z.north east)+(0em,0em)$)
+node[midway, above=0.5em]{$z$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
+node[midway, above=0.8em]{$x @ z \in L_1*$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
+node[midway, below=0.5em]{$(x - xa\_max) @ z \in L_1*$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
+node[midway, below=0.5em]{$xa \in L_1*$};
+\end{tikzpicture}}}
+\subfigure[Max split with $a$ and $b$]{\label{ab_split}
+\scalebox{0.9}{
+\begin{tikzpicture}
+\node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}xa\_max\hspace{4em}$ };
+\node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - xa\_max\hspace{0.5em}$ };
+\node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{21em}$ };
+\draw[decoration={brace,transform={yscale=3}},decorate]
+(xa.north west) -- ($(xxa.north east)+(0em,0em)$)
+node[midway, above=0.5em]{$x$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+(z.north west) -- ($(z.north east)+(0em,0em)$)
+node[midway, above=0.5em]{$z$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
+node[midway, above=0.8em]{$x @ z \in L_1*$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
+node[midway, below=0.5em]{$(x - xa\_max) @ z \in L_1*$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
+node[midway, below=0.5em]{$xa \in L_1*$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+($(xxa.south east)+(6em,-5ex)$) -- ($(xxa.south west)+(0em,-5ex)$)
+node[midway, below=0.5em]{$a \in L_1$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+($(z.south east)+(0em,-5ex)$) -- ($(xxa.south east)+(6em,-5ex)$)
+node[midway, below=0.5em]{$b \in L_1*$};
+\end{tikzpicture}}}
+\subfigure[Last split]{\label{last_split}
+\scalebox{0.9}{
+\begin{tikzpicture}
+\node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}xa\_max\hspace{4em}$ };
+\node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - xa\_max\hspace{0.5em}$ };
+\node[draw,minimum height=3.8ex, right=-0.03em of xxa] (za) { $\hspace{2em}za\hspace{2em}$ };
+\node[draw,minimum height=3.8ex, right=-0.03em of za] (zb) { $\hspace{7em}zb\hspace{7em}$ };
+\draw[decoration={brace,transform={yscale=3}},decorate]
+(xa.north west) -- ($(xxa.north east)+(0em,0em)$)
+node[midway, above=0.5em]{$x$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+(za.north west) -- ($(zb.north east)+(0em,0em)$)
+node[midway, above=0.5em]{$z$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+($(xa.north west)+(0em,3ex)$) -- ($(zb.north east)+(0em,3ex)$)
+node[midway, above=0.8em]{$x @ z \in L_1*$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
+node[midway, below=0.5em]{$(x - xa\_max) @ za \in L_1$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
+node[midway, below=0.5em]{$xa\_max \in L_1*$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)
+node[midway, below=0.5em]{$zb \in L_1*$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$)
+node[midway, below=0.5em]{$(x - xa\_max)@z \in L_1*$};
+\end{tikzpicture}}}
+\subfigure[Transferring to $y$]{\label{trans_split}
+\scalebox{0.9}{
+\begin{tikzpicture}
+\node[draw,minimum height=3.8ex] (xa) { $\hspace{5em}ya\hspace{5em}$ };
+\node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{2em}y - ya\hspace{2em}$ };
+\node[draw,minimum height=3.8ex, right=-0.03em of xxa] (za) { $\hspace{2em}za\hspace{2em}$ };
+\node[draw,minimum height=3.8ex, right=-0.03em of za] (zb) { $\hspace{7em}zb\hspace{7em}$ };
+\draw[decoration={brace,transform={yscale=3}},decorate]
+(xa.north west) -- ($(xxa.north east)+(0em,0em)$)
+node[midway, above=0.5em]{$y$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+(za.north west) -- ($(zb.north east)+(0em,0em)$)
+node[midway, above=0.5em]{$z$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+($(xa.north west)+(0em,3ex)$) -- ($(zb.north east)+(0em,3ex)$)
+node[midway, above=0.8em]{$y @ z \in L_1*$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
+node[midway, below=0.5em]{$(y - ya) @ za \in L_1$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
+node[midway, below=0.5em]{$ya \in L_1*$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)
+node[midway, below=0.5em]{$zb \in L_1*$};
+\draw[decoration={brace,transform={yscale=3}},decorate]
+($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$)
+node[midway, below=0.5em]{$(y - ya)@z \in L_1*$};
+\end{tikzpicture}}}
+\caption{The case for $STAR$}
+\end{figure}
 *}
 definition
 tag_str_STAR :: "lang \<Rightarrow> string \<Rightarrow> lang set"
 where
 "tag_str_STAR L1 = (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})"
 text {* A technical lemma. *}
 lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow>
 (\<exists> max \<in> A. \<forall> a \<in> A. f a <= (f max :: nat))"
 proof (induct rule:finite.induct)
 text {* Technical lemma. *}
 lemma finite_strict_prefix_set: "finite {xa. xa < (x::string)}"
 apply (induct x rule:rev_induct, simp)
 apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}")
 by (auto simp:strict_prefix_def)
-text {*
-The following lemma @{text "tag_str_STAR_injI"} establishes the injectivity of
-the tagging function for case @{text "STAR"}.
-*}
 lemma tag_str_STAR_injI:
 fixes v w
 assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_STAR L\<^isub>1 w"

changeset 49	59936c012add
parent 48	61d9684a557a
child 55	d71424eb5d0c