diff -r c19d2fc2cc69 -r d71424eb5d0c Myhill.thy --- a/Myhill.thy Mon Jan 31 12:54:31 2011 +0000 +++ b/Myhill.thy Mon Jan 31 14:51:47 2011 +0000 @@ -18,19 +18,27 @@ "x \Lang y \ (x, y) \ (\Lang)" text {* - The basic idea to show the finiteness of the partition induced by relation @{text "\Lang"} - is to attach a tag @{text "tag(x)"} to every string @{text "x"}, the set of tags are carfully - choosen, so that the range of tagging function @{text "tag"} (denoted @{text "range(tag)"}) is finite. - If strings with the same tag are equivlent with respect @{text "\Lang"}, - i.e. @{text "tag(x) = tag(y) \ x \Lang y"} (this property is named `injectivity' in the following), - then it can be proved that: the partition given rise by @{text "(\Lang)"} is finite. - - There are two arguments for this. The first goes as the following: + The main lemma (@{text "rexp_imp_finite"}) is proved by a structural induction over regular expressions. + While base cases (cases for @{const "NULL"}, @{const "EMPTY"}, @{const "CHAR"}) are quite straight forward, + the inductive cases are rather involved. What we have when starting to prove these inductive caes is that + the partitions induced by the componet language are finite. The basic idea to show the finiteness of the + partition induced by the composite language is to attach a tag @{text "tag(x)"} to every string + @{text "x"}. The tags are made of equivalent classes from the component partitions. Let @{text "tag"} + be the tagging function and @{text "Lang"} be the composite language, it can be proved that + if strings with the same tag are equivalent with respect to @{text "Lang"}, expressed as: + \[ + @{text "tag(x) = tag(y) \ x \Lang y"} + \] + then the partition induced by @{text "Lang"} must be finite. There are two arguments for this. + The first goes as the following: \begin{enumerate} \item First, the tagging function @{text "tag"} induces an equivalent relation @{text "(=tag=)"} (defiintion of @{text "f_eq_rel"} and lemma @{text "equiv_f_eq_rel"}). - \item It is shown that: if the range of @{text "tag"} is finite, + \item It is shown that: if the range of @{text "tag"} (denoted @{text "range(tag)"}) is finite, the partition given rise by @{text "(=tag=)"} is finite (lemma @{text "finite_eq_f_rel"}). + Since tags are made from equivalent classes from component partitions, and the inductive + hypothesis ensures the finiteness of these partitions, it is not difficult to prove + the finiteness of @{text "range(tag)"}. \item It is proved that if equivalent relation @{text "R1"} is more refined than @{text "R2"} (expressed as @{text "R1 \ R2"}), and the partition induced by @{text "R1"} is finite, then the partition induced by @{text "R2"} @@ -117,7 +125,8 @@ next from eq2 show " ?f ` A // R2 \ Pow ?B" - apply (unfold image_def Pow_def quotient_def, auto) + unfolding image_def Pow_def quotient_def + apply auto by (rule_tac x = xb in bexI, simp, unfold equiv_def sym_def refl_on_def, blast) qed @@ -132,7 +141,7 @@ fix x assume "X = R2 `` {x}" and "x \ A" with eq2 have x_in: "x \ X" - by (unfold equiv_def quotient_def refl_on_def, auto) + unfolding equiv_def quotient_def refl_on_def by auto with eq_f have "R1 `` {x} \ ?R" by auto then obtain y where y_in: "y \ Y" and eq_r: "R1 `` {x} = R1 ``{y}" by auto @@ -140,7 +149,7 @@ proof - from x_in X_in y_in Y_in eq2 have "x \ A" and "y \ A" - by (unfold equiv_def quotient_def refl_on_def, auto) + unfolding equiv_def quotient_def refl_on_def by auto from eq_equiv_class_iff [OF eq1 this] and eq_r show ?thesis by simp qed @@ -154,7 +163,7 @@ qed lemma equiv_lang_eq: "equiv UNIV (\Lang)" - apply (unfold equiv_def str_eq_rel_def sym_def refl_on_def trans_def) + unfolding equiv_def str_eq_rel_def sym_def refl_on_def trans_def by blast lemma tag_finite_imageD: @@ -245,7 +254,32 @@ subsection {* The proof*} -subsubsection {* The case for @{const "NULL"} *} +text {* + Each case is given in a separate section, as well as the final main lemma. Detailed explainations accompanied by + illustrations are given for non-trivial cases. + + + For ever inductive case, there are two tasks, the easier one is to show the range finiteness of + of the tagging function based on the finiteness of component partitions, the + difficult one is to show that strings with the same tag are equivalent with respect to the + composite language. Suppose the composite language be @{text "Lang"}, tagging function be + @{text "tag"}, it amounts to show: + \[ + @{text "tag(x) = tag(y) \ x \Lang y"} + \] + expanding the definition of @{text "\Lang"}, it amounts to show: + \[ + @{text "tag(x) = tag(y) \ (\ z. x@z \ Lang \ y@z \ Lang)"} + \] + Because the assumed tag equlity @{text "tag(x) = tag(y)"} is symmetric, + it is suffcient to show just one direction: + \[ + @{text "\ x y z. \tag(x) = tag(y); x@z \ Lang\ \ y@z \ Lang"} + \] + This is the pattern followed by every inductive case. + *} + +subsubsection {* The base case for @{const "NULL"} *} lemma quot_null_eq: shows "(UNIV // \{}) = ({UNIV}::lang set)" @@ -256,7 +290,7 @@ unfolding quot_null_eq by simp -subsubsection {* The case for @{const "EMPTY"} *} +subsubsection {* The base case for @{const "EMPTY"} *} lemma quot_empty_subset: @@ -283,7 +317,7 @@ by (rule finite_subset[OF quot_empty_subset]) (simp) -subsubsection {* The case for @{const "CHAR"} *} +subsubsection {* The base case for @{const "CHAR"} *} lemma quot_char_subset: "UNIV // (\{[c]}) \ {{[]},{[c]}, UNIV - {[], [c]}}" @@ -315,110 +349,13 @@ by (rule finite_subset[OF quot_char_subset]) (simp) - -subsubsection {* The case for @{text "SEQ"}*} - -definition - tag_str_SEQ :: "lang \ lang \ string \ (lang \ lang set)" -where - "tag_str_SEQ L1 L2 = - (\x. (\L1 `` {x}, {(\L2 `` {x - xa}) | xa. xa \ x \ xa \ L1}))" - - -lemma append_seq_elim: - assumes "x @ y \ L\<^isub>1 ;; L\<^isub>2" - shows "(\ xa \ x. xa \ L\<^isub>1 \ (x - xa) @ y \ L\<^isub>2) \ - (\ ya \ y. (x @ ya) \ L\<^isub>1 \ (y - ya) \ L\<^isub>2)" -proof- - from assms obtain s\<^isub>1 s\<^isub>2 - where "x @ y = s\<^isub>1 @ s\<^isub>2" - and in_seq: "s\<^isub>1 \ L\<^isub>1 \ s\<^isub>2 \ L\<^isub>2" - by (auto simp:Seq_def) - hence "(x \ s\<^isub>1 \ (s\<^isub>1 - x) @ s\<^isub>2 = y) \ (s\<^isub>1 \ x \ (x - s\<^isub>1) @ y = s\<^isub>2)" - using app_eq_dest by auto - moreover have "\x \ s\<^isub>1; (s\<^isub>1 - x) @ s\<^isub>2 = y\ \ - \ ya \ y. (x @ ya) \ L\<^isub>1 \ (y - ya) \ L\<^isub>2" - using in_seq by (rule_tac x = "s\<^isub>1 - x" in exI, auto elim:prefixE) - moreover have "\s\<^isub>1 \ x; (x - s\<^isub>1) @ y = s\<^isub>2\ \ - \ xa \ x. xa \ L\<^isub>1 \ (x - xa) @ y \ L\<^isub>2" - using in_seq by (rule_tac x = s\<^isub>1 in exI, auto) - ultimately show ?thesis by blast -qed - -lemma tag_str_SEQ_injI: - "tag_str_SEQ L\<^isub>1 L\<^isub>2 m = tag_str_SEQ L\<^isub>1 L\<^isub>2 n \ m \(L\<^isub>1 ;; L\<^isub>2) n" -proof- - { fix x y z - assume xz_in_seq: "x @ z \ L\<^isub>1 ;; L\<^isub>2" - and tag_xy: "tag_str_SEQ L\<^isub>1 L\<^isub>2 x = tag_str_SEQ L\<^isub>1 L\<^isub>2 y" - have"y @ z \ L\<^isub>1 ;; L\<^isub>2" - proof- - have "(\ xa \ x. xa \ L\<^isub>1 \ (x - xa) @ z \ L\<^isub>2) \ - (\ za \ z. (x @ za) \ L\<^isub>1 \ (z - za) \ L\<^isub>2)" - using xz_in_seq append_seq_elim by simp - moreover { - fix xa - assume h1: "xa \ x" and h2: "xa \ L\<^isub>1" and h3: "(x - xa) @ z \ L\<^isub>2" - obtain ya where "ya \ y" and "ya \ L\<^isub>1" and "(y - ya) @ z \ L\<^isub>2" - proof - - have "\ ya. ya \ y \ ya \ L\<^isub>1 \ (x - xa) \L\<^isub>2 (y - ya)" - proof - - have "{\L\<^isub>2 `` {x - xa} |xa. xa \ x \ xa \ L\<^isub>1} = - {\L\<^isub>2 `` {y - xa} |xa. xa \ y \ xa \ L\<^isub>1}" - (is "?Left = ?Right") - using h1 tag_xy by (auto simp:tag_str_SEQ_def) - moreover have "\L\<^isub>2 `` {x - xa} \ ?Left" using h1 h2 by auto - ultimately have "\L\<^isub>2 `` {x - xa} \ ?Right" by simp - thus ?thesis by (auto simp:Image_def str_eq_rel_def str_eq_def) - qed - with prems show ?thesis by (auto simp:str_eq_rel_def str_eq_def) - qed - hence "y @ z \ L\<^isub>1 ;; L\<^isub>2" by (erule_tac prefixE, auto simp:Seq_def) - } moreover { - fix za - assume h1: "za \ z" and h2: "(x @ za) \ L\<^isub>1" and h3: "z - za \ L\<^isub>2" - hence "y @ za \ L\<^isub>1" - proof- - have "\L\<^isub>1 `` {x} = \L\<^isub>1 `` {y}" - using h1 tag_xy by (auto simp:tag_str_SEQ_def) - with h2 show ?thesis - by (auto simp:Image_def str_eq_rel_def str_eq_def) - qed - with h1 h3 have "y @ z \ L\<^isub>1 ;; L\<^isub>2" - by (drule_tac A = L\<^isub>1 in seq_intro, auto elim:prefixE) - } - ultimately show ?thesis by blast - qed - } thus "tag_str_SEQ L\<^isub>1 L\<^isub>2 m = tag_str_SEQ L\<^isub>1 L\<^isub>2 n \ m \(L\<^isub>1 ;; L\<^isub>2) n" - by (auto simp add: str_eq_def str_eq_rel_def) -qed - -lemma quot_seq_finiteI [intro]: - fixes L1 L2::"lang" - assumes fin1: "finite (UNIV // \L1)" - and fin2: "finite (UNIV // \L2)" - shows "finite (UNIV // \(L1 ;; L2))" -proof (rule_tac tag = "tag_str_SEQ L1 L2" in tag_finite_imageD) - show "\x y. tag_str_SEQ L1 L2 x = tag_str_SEQ L1 L2 y \ x \(L1 ;; L2) y" - by (rule tag_str_SEQ_injI) -next - have *: "finite ((UNIV // \L1) \ (Pow (UNIV // \L2)))" - using fin1 fin2 by auto - show "finite (range (tag_str_SEQ L1 L2))" - unfolding tag_str_SEQ_def - apply(rule finite_subset[OF _ *]) - unfolding quotient_def - by auto -qed - -subsubsection {* The case for @{const ALT} *} +subsubsection {* The inductive case for @{const ALT} *} definition tag_str_ALT :: "lang \ lang \ string \ (lang \ lang)" where "tag_str_ALT L1 L2 = (\x. (\L1 `` {x}, \L2 `` {x}))" - lemma quot_union_finiteI [intro]: fixes L1 L2::"lang" assumes finite1: "finite (UNIV // \L1)" @@ -441,7 +378,161 @@ by auto qed -subsubsection {* The case for @{const "STAR"} *} +subsubsection {* The inductive case for @{text "SEQ"}*} + +text {* + For case @{const "SEQ"}, the language @{text "L"} is @{text "L\<^isub>1 ;; L\<^isub>2"}. + Given @{text "x @ z \ L\<^isub>1 ;; L\<^isub>2"}, according to the defintion of @{text " L\<^isub>1 ;; L\<^isub>2"}, + string @{text "x @ z"} can be splitted with the prefix in @{text "L\<^isub>1"} and suffix in @{text "L\<^isub>2"}. + The split point can either be in @{text "x"} (as shown in Fig. \ref{seq_first_split}), + or in @{text "z"} (as shown in Fig. \ref{seq_snd_split}). Whichever way it goes, the structure + on @{text "x @ z"} cn be transfered faithfully onto @{text "y @ z"} + (as shown in Fig. \ref{seq_trans_first_split} and \ref{seq_trans_snd_split}) with the the help of the assumed + tag equality. The following tag function @{text "tag_str_SEQ"} is such designed to facilitate + such transfers and lemma @{text "tag_str_SEQ_injI"} formalizes the informal argument above. The details + of structure transfer will be given their. +\input{fig_seq} + + *} + +definition + tag_str_SEQ :: "lang \ lang \ string \ (lang \ lang set)" +where + "tag_str_SEQ L1 L2 = + (\x. (\L1 `` {x}, {(\L2 `` {x - xa}) | xa. xa \ x \ xa \ L1}))" + +text {* The following is a techical lemma which helps to split the @{text "x @ z \ L\<^isub>1 ;; L\<^isub>2"} mentioned above.*} + +lemma append_seq_elim: + assumes "x @ y \ L\<^isub>1 ;; L\<^isub>2" + shows "(\ xa \ x. xa \ L\<^isub>1 \ (x - xa) @ y \ L\<^isub>2) \ + (\ ya \ y. (x @ ya) \ L\<^isub>1 \ (y - ya) \ L\<^isub>2)" +proof- + from assms obtain s\<^isub>1 s\<^isub>2 + where eq_xys: "x @ y = s\<^isub>1 @ s\<^isub>2" + and in_seq: "s\<^isub>1 \ L\<^isub>1 \ s\<^isub>2 \ L\<^isub>2" + by (auto simp:Seq_def) + from app_eq_dest [OF eq_xys] + have + "(x \ s\<^isub>1 \ (s\<^isub>1 - x) @ s\<^isub>2 = y) \ (s\<^isub>1 \ x \ (x - s\<^isub>1) @ y = s\<^isub>2)" + (is "?Split1 \ ?Split2") . + moreover have "?Split1 \ \ ya \ y. (x @ ya) \ L\<^isub>1 \ (y - ya) \ L\<^isub>2" + using in_seq by (rule_tac x = "s\<^isub>1 - x" in exI, auto elim:prefixE) + moreover have "?Split2 \ \ xa \ x. xa \ L\<^isub>1 \ (x - xa) @ y \ L\<^isub>2" + using in_seq by (rule_tac x = s\<^isub>1 in exI, auto) + ultimately show ?thesis by blast +qed + + +lemma tag_str_SEQ_injI: + fixes v w + assumes eq_tag: "tag_str_SEQ L\<^isub>1 L\<^isub>2 v = tag_str_SEQ L\<^isub>1 L\<^isub>2 w" + shows "v \(L\<^isub>1 ;; L\<^isub>2) w" +proof- + -- {* As explained before, a pattern for just one direction needs to be dealt with:*} + { fix x y z + assume xz_in_seq: "x @ z \ L\<^isub>1 ;; L\<^isub>2" + and tag_xy: "tag_str_SEQ L\<^isub>1 L\<^isub>2 x = tag_str_SEQ L\<^isub>1 L\<^isub>2 y" + have"y @ z \ L\<^isub>1 ;; L\<^isub>2" + proof- + -- {* There are two ways to split @{text "x@z"}: *} + from append_seq_elim [OF xz_in_seq] + have "(\ xa \ x. xa \ L\<^isub>1 \ (x - xa) @ z \ L\<^isub>2) \ + (\ za \ z. (x @ za) \ L\<^isub>1 \ (z - za) \ L\<^isub>2)" . + -- {* It can be shown that @{text "?thesis"} holds in either case: *} + moreover { + -- {* The case for the first split:*} + fix xa + assume h1: "xa \ x" and h2: "xa \ L\<^isub>1" and h3: "(x - xa) @ z \ L\<^isub>2" + -- {* The following subgoal implements the structure transfer:*} + obtain ya + where "ya \ y" + and "ya \ L\<^isub>1" + and "(y - ya) @ z \ L\<^isub>2" + proof - + -- {* + \begin{minipage}{0.8\textwidth} + By expanding the definition of + @{thm [display] "tag_xy"} + and extracting the second compoent, we get: + \end{minipage} + *} + have "{\L\<^isub>2 `` {x - xa} |xa. xa \ x \ xa \ L\<^isub>1} = + {\L\<^isub>2 `` {y - ya} |ya. ya \ y \ ya \ L\<^isub>1}" (is "?Left = ?Right") + using tag_xy unfolding tag_str_SEQ_def by simp + -- {* Since @{thm "h1"} and @{thm "h2"} hold, it is not difficult to show: *} + moreover have "\L\<^isub>2 `` {x - xa} \ ?Left" using h1 h2 by auto + -- {* + \begin{minipage}{0.7\textwidth} + Through tag equality, equivalent class @{term "\L\<^isub>2 `` {x - xa}"} also + belongs to the @{text "?Right"}: + \end{minipage} + *} + ultimately have "\L\<^isub>2 `` {x - xa} \ ?Right" by simp + -- {* From this, the counterpart of @{text "xa"} in @{text "y"} is obtained:*} + then obtain ya + where eq_xya: "\L\<^isub>2 `` {x - xa} = \L\<^isub>2 `` {y - ya}" + and pref_ya: "ya \ y" and ya_in: "ya \ L\<^isub>1" + by simp blast + -- {* It can be proved that @{text "ya"} has the desired property:*} + have "(y - ya)@z \ L\<^isub>2" + proof - + from eq_xya have "(x - xa) \L\<^isub>2 (y - ya)" + unfolding Image_def str_eq_rel_def str_eq_def by auto + with h3 show ?thesis unfolding str_eq_rel_def str_eq_def by simp + qed + -- {* Now, @{text "ya"} has all properties to be a qualified candidate:*} + with pref_ya ya_in + show ?thesis using prems by blast + qed + -- {* From the properties of @{text "ya"}, @{text "y @ z \ L\<^isub>1 ;; L\<^isub>2"} is derived easily.*} + hence "y @ z \ L\<^isub>1 ;; L\<^isub>2" by (erule_tac prefixE, auto simp:Seq_def) + } moreover { + -- {* The other case is even more simpler: *} + fix za + assume h1: "za \ z" and h2: "(x @ za) \ L\<^isub>1" and h3: "z - za \ L\<^isub>2" + have "y @ za \ L\<^isub>1" + proof- + have "\L\<^isub>1 `` {x} = \L\<^isub>1 `` {y}" + using tag_xy unfolding tag_str_SEQ_def by simp + with h2 show ?thesis + unfolding Image_def str_eq_rel_def str_eq_def by auto + qed + with h1 h3 have "y @ z \ L\<^isub>1 ;; L\<^isub>2" + by (drule_tac A = L\<^isub>1 in seq_intro, auto elim:prefixE) + } + ultimately show ?thesis by blast + qed + } + -- {* + \begin{minipage}{0.8\textwidth} + @{text "?thesis"} is proved by exploiting the symmetry of + @{thm [source] "eq_tag"}: + \end{minipage} + *} + from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]] + show ?thesis unfolding str_eq_def str_eq_rel_def by blast +qed + +lemma quot_seq_finiteI [intro]: + fixes L1 L2::"lang" + assumes fin1: "finite (UNIV // \L1)" + and fin2: "finite (UNIV // \L2)" + shows "finite (UNIV // \(L1 ;; L2))" +proof (rule_tac tag = "tag_str_SEQ L1 L2" in tag_finite_imageD) + show "\x y. tag_str_SEQ L1 L2 x = tag_str_SEQ L1 L2 y \ x \(L1 ;; L2) y" + by (rule tag_str_SEQ_injI) +next + have *: "finite ((UNIV // \L1) \ (Pow (UNIV // \L2)))" + using fin1 fin2 by auto + show "finite (range (tag_str_SEQ L1 L2))" + unfolding tag_str_SEQ_def + apply(rule finite_subset[OF _ *]) + unfolding quotient_def + by auto +qed + +subsubsection {* The inductive case for @{const "STAR"} *} text {* This turned out to be the trickiest case. The essential goal is @@ -449,24 +540,25 @@ 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 that @{text "xa \ L\<^isub>1*"} and @{text "(x - xa)@z \ L\<^isub>1*"}, as shown in Fig. \ref{first_split}. 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). + and name it @{text "xa_max"}, as shown in Fig. \ref{max_split}. \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). + @{text "(x - xa_max) @ za \ L\<^isub>1"} and @{text "zb \ L\<^isub>1*"} as shown in Fig. \ref{last_split}. 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"} + \item Because @{text "(x - x_max) @ z \ L\<^isub>1*"}, it can always be splitted 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"}. + as shown in Fig. \ref{ab_split}. + \item But the prefix @{text "a"} CANNOT be shorter than @{text "x - xa_max"} + (as shown in Fig. \ref{ab_split_wrong}), becasue otherwise, + @{text "ma_max@a"} would be in the same kind as @{text "xa_max"} but with + a larger size, conflicting with the fact that @{text "xa_max"} is the longest. \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: + can be transferred to @{text "y @ z"} as shown in Fig. \ref{trans_split}. 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"}. @@ -478,182 +570,9 @@ 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*$}; + \ref{ansfer_step} feasible. - \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} - + \input{fig_star} *} definition @@ -688,7 +607,7 @@ qed -text {* Technical lemma. *} +text {* The following is a technical lemma.which helps to show the range finiteness of tag function. *} 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} \ {xs}") @@ -700,16 +619,7 @@ assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_STAR L\<^isub>1 w" shows "(v::string) \(L\<^isub>1\) w" proof- - -- {* - \begin{minipage}{0.9\textwidth} - According to the definition of @{text "\Lang"}, - proving @{text "v \(L\<^isub>1\) w"} amounts to - showing: for any string @{text "u"}, - if @{text "v @ u \ (L\<^isub>1\)"} then @{text "w @ u \ (L\<^isub>1\)"} and vice versa. - The reasoning pattern for both directions are the same, as derived - in the following: - \end{minipage} - *} + -- {* As explained before, a pattern for just one direction needs to be dealt with:*} { fix x y z assume xz_in_star: "x @ z \ L\<^isub>1\" and tag_xy: "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y" @@ -723,16 +633,12 @@ by (auto simp:tag_str_STAR_def strict_prefix_def) thus ?thesis using xz_in_star True by simp next - -- {* - \begin{minipage}{0.9\textwidth} - The case when @{text "x"} is not null, and - @{text "x @ z"} is in @{text "L\<^isub>1\"}, - \end{minipage} + -- {* The nontrival case: *} case False -- {* - \begin{minipage}{0.9\textwidth} - Since @{text "x @ z \ L\<^isub>1\"}, @{text "x"} can always be splited + \begin{minipage}{0.8\textwidth} + Since @{text "x @ z \ L\<^isub>1\"}, @{text "x"} can always be splitted by a prefix @{text "xa"} together with its suffix @{text "x - xa"}, such that both @{text "xa"} and @{text "(x - xa) @ z"} are in @{text "L\<^isub>1\"}, and there could be many such splittings.Therefore, the following set @{text "?S"} @@ -745,8 +651,9 @@ auto simp:finite_strict_prefix_set) moreover have "?S \ {}" using False xz_in_star by (simp, rule_tac x = "[]" in exI, auto simp:strict_prefix_def) - -- {* Since @{text "?S"} is finite, we can always single out the longest - and name it @{text "xa_max"}: + -- {* \begin{minipage}{0.7\textwidth} + Since @{text "?S"} is finite, we can always single out the longest and name it @{text "xa_max"}: + \end{minipage} *} ultimately have "\ xa_max \ ?S. \ xa \ ?S. length xa \ length xa_max" using finite_set_has_max by blast @@ -758,7 +665,7 @@ \ length xa \ length xa_max" by blast -- {* - \begin{minipage}{0.9\textwidth} + \begin{minipage}{0.8\textwidth} By the equality of tags, the counterpart of @{text "xa_max"} among @{text "y"}-prefixes, named @{text "ya"}, can be found: \end{minipage} @@ -776,9 +683,9 @@ (simp add:Image_def str_eq_rel_def str_eq_def) by blast qed -- {* - \begin{minipage}{0.9\textwidth} - If the following proposition can be proved, then the @{text "?thesis"}: - @{text "y @ z \ L\<^isub>1\"} is just a simple consequence. + \begin{minipage}{0.8\textwidth} + The @{text "?thesis"}, @{prop "y @ z \ L\<^isub>1\"}, is a simple consequence + of the following proposition: \end{minipage} *} have "(y - ya) @ z \ L\<^isub>1\" @@ -789,8 +696,8 @@ and l_za: "(y - ya)@za \ L\<^isub>1" and ls_zb: "zb \ L\<^isub>1\" proof - -- {* - \begin{minipage}{0.9\textwidth} - Since @{text "(x - xa_max) @ z"} is in @{text "L\<^isub>1\"}, it can be split into + \begin{minipage}{0.8\textwidth} + Since @{thm "h1"}, @{text "x"} can be splitted into @{text "a"} and @{text "b"} such that: \end{minipage} *} @@ -806,9 +713,9 @@ and eq_z: "z = ?za @ ?zb" (is "?P2") proof - -- {* - \begin{minipage}{0.9\textwidth} - Since @{text "(x - xa_max) @ z = a @ b"}, the string @{text "(x - xa_max) @ z"} - could be splited in two ways: + \begin{minipage}{0.8\textwidth} + Since @{text "(x - xa_max) @ z = a @ b"}, string @{text "(x - xa_max) @ z"} + can be splitted in two ways: \end{minipage} *} have "((x - xa_max) \ a \ (a - (x - xa_max)) @ b = z) \ @@ -842,10 +749,7 @@ show ?thesis by blast qed -- {* - \begin{minipage}{0.9\textwidth} - From the properties of @{text "za"} and @{text "zb"} such obtained, - @{text "?thesis"} can be shown easily. - \end{minipage} + @{text "?thesis"} can easily be shown using properties of @{text "za"} and @{text "zb"}: *} from step [OF l_za ls_zb] have "((y - ya) @ za) @ zb \ L\<^isub>1\" . @@ -858,17 +762,17 @@ -- {* By instantiating the reasoning pattern just derived for both directions:*} from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]] -- {* The thesis is proved as a trival consequence: *} - show ?thesis by (unfold str_eq_def str_eq_rel_def, blast) + show ?thesis unfolding str_eq_def str_eq_rel_def by blast qed -lemma -- {* The oringal version with a poor readability*} +lemma -- {* The oringal version with less explicit details. *} fixes v w assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_STAR L\<^isub>1 w" shows "(v::string) \(L\<^isub>1\) w" proof- -- {* - \begin{minipage}{0.9\textwidth} + \begin{minipage}{0.8\textwidth} According to the definition of @{text "\Lang"}, proving @{text "v \(L\<^isub>1\) w"} amounts to showing: for any string @{text "u"}, @@ -891,7 +795,7 @@ thus ?thesis using xz_in_star True by simp next -- {* - \begin{minipage}{0.9\textwidth} + \begin{minipage}{0.8\textwidth} The case when @{text "x"} is not null, and @{text "x @ z"} is in @{text "L\<^isub>1\"}, \end{minipage} @@ -967,7 +871,7 @@ -- {* By instantiating the reasoning pattern just derived for both directions:*} from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]] -- {* The thesis is proved as a trival consequence: *} - show ?thesis by (unfold str_eq_def str_eq_rel_def, blast) + show ?thesis unfolding str_eq_def str_eq_rel_def by blast qed lemma quot_star_finiteI [intro]: