diff -r 61d9684a557a -r 59936c012add Myhill.thy --- a/Myhill.thy Sat Jan 29 11:41:17 2011 +0000 +++ b/Myhill.thy Sun Jan 30 12:22:07 2011 +0000 @@ -444,11 +444,216 @@ subsubsection {* The case for @{const "STAR"} *} text {* - This turned out to be the trickiest case. - Any string @{text "x"} in language @{text "L\<^isub>1\"}, - can be splited into a prefix @{text "xa \ L\<^isub>1\"} and a suffix @{text "x - xa \ L\<^isub>1"}. - For one such @{text "x"}, there can be many such splits. The tagging of @{text "x"} is then - defined by collecting the @{text "L\<^isub>1"}-state of the suffixe from every possible split. + This turned out to be the trickiest case. The essential goal is + to proved @{text "y @ z \ L\<^isub>1*"} under the assumptions that @{text "x @ z \ L\<^isub>1*"} + and that @{text "x"} and @{text "y"} have the same tag. The reasoning goes as the following: + \begin{enumerate} + \item Since @{text "x @ z \ L\<^isub>1*"} holds, a prefix @{text "xa"} of @{text "x"} can be found + such that @{text "xa \ L\<^isub>1*"} and @{text "(x - xa)@z \ 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 \ L\<^isub>1"} and @{text "zb \ 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 \ L\<^isub>1*"}, it can always be split into prefix @{text "a"} + and suffix @{text "b"}, such that @{text "a \ L\<^isub>1"} and @{text "b \ 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 \ L\<^isub>1*"} and @{text "(y - ya)@za \ L\<^isub>1"}. + \item Since we already know @{text "zb \ L\<^isub>1*"}, we get @{text "(y - ya)@za@zb \ L\<^isub>1*"}, + and this is just @{text "(y - ya)@z \ L\<^isub>1*"}. + \item With fact @{text "ya \ L\<^isub>1*"}, we finally get @{text "y@z \ 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 @@ -456,8 +661,6 @@ where "tag_str_STAR L1 = (\x. {\L1 `` {x - xa} | xa. xa < x \ xa \ L1\})" - - text {* A technical lemma. *} lemma finite_set_has_max: "\finite A; A \ {}\ \ (\ max \ A. \ a \ A. f a <= (f max :: nat))" @@ -492,12 +695,6 @@ 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"