21   The basic idea to show the finiteness of the partition induced by relation @{text "\<approx>Lang"}

    21   The main lemma (@{text "rexp_imp_finite"}) is proved by a structural induction over regular expressions.

    22   is to attach a tag @{text "tag(x)"} to every string @{text "x"}, the set of tags are carfully 

    22   While base cases (cases for @{const "NULL"}, @{const "EMPTY"}, @{const "CHAR"}) are quite straight forward,

    23   choosen, so that the range of tagging function @{text "tag"} (denoted @{text "range(tag)"}) is finite. 

    23   the inductive cases are rather involved. What we have when starting to prove these inductive caes is that

    24   If strings with the same tag are equivlent with respect @{text "\<approx>Lang"},

    24   the partitions induced by the componet language are finite. The basic idea to show the finiteness of the 

    25   i.e. @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"} (this property is named `injectivity' in the following), 

    25   partition induced by the composite language is to attach a tag @{text "tag(x)"} to every string 

    26   then it can be proved that: the partition given rise by @{text "(\<approx>Lang)"} is finite. 

    26   @{text "x"}. The tags are made of equivalent classes from the component partitions. Let @{text "tag"}

    27   

    27   be the tagging function and @{text "Lang"} be the composite language, it can be proved that

    28   There are two arguments for this. The first goes as the following:

    28   if strings with the same tag are equivalent with respect to @{text "Lang"}, expressed as:

    29   \[

    30   @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"}

    31   \]

    32   then the partition induced by @{text "Lang"} must be finite. There are two arguments for this. 

    33   The first goes as the following:

    32     \item It is shown that: if the range of @{text "tag"} is finite, 

    37     \item It is shown that: if the range of @{text "tag"} (denoted @{text "range(tag)"}) is finite, 

   120         apply (unfold image_def Pow_def quotient_def, auto)

   128         unfolding image_def Pow_def quotient_def

   129         apply auto

   135             by (unfold equiv_def quotient_def refl_on_def, auto)

   144             unfolding equiv_def quotient_def refl_on_def by auto

   143               by (unfold equiv_def quotient_def refl_on_def, auto)

   152               unfolding equiv_def quotient_def refl_on_def by auto

   157   apply (unfold equiv_def str_eq_rel_def sym_def refl_on_def trans_def)

   166   unfolding equiv_def str_eq_rel_def sym_def refl_on_def trans_def

   248 subsubsection {* The case for @{const "NULL"} *}

   257 text {*

   258   Each case is given in a separate section, as well as the final main lemma. Detailed explainations accompanied by

   259   illustrations are given for non-trivial cases.

   260 

   261   

   262   For ever inductive case, there are two tasks, the easier one is to show the range finiteness of

   263   of the tagging function based on the finiteness of component partitions, the

   264   difficult one is to show that strings with the same tag are equivalent with respect to the 

   265   composite language. Suppose the composite language be @{text "Lang"}, tagging function be 

   266   @{text "tag"}, it amounts to show:

   267   \[

   268   @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"}

   269   \]

   270   expanding the definition of @{text "\<approx>Lang"}, it amounts to show:

   271   \[

   272   @{text "tag(x) = tag(y) \<Longrightarrow> (\<forall> z. x@z \<in> Lang \<longleftrightarrow> y@z \<in> Lang)"}

   273   \]

   274   Because the assumed tag equlity @{text "tag(x) = tag(y)"} is symmetric,

   275   it is suffcient to show just one direction:

   276   \[

   277   @{text "\<And> x y z. \<lbrakk>tag(x) = tag(y); x@z \<in> Lang\<rbrakk> \<Longrightarrow> y@z \<in> Lang"}

   278   \]

   279   This is the pattern followed by every inductive case.

   280   *}

   281 

   282 subsubsection {* The base case for @{const "NULL"} *}

   259 subsubsection {* The case for @{const "EMPTY"} *}

   293 subsubsection {* The base case for @{const "EMPTY"} *}

   286 subsubsection {* The case for @{const "CHAR"} *}

   320 subsubsection {* The base case for @{const "CHAR"} *}

   318 

   352 subsubsection {* The inductive case for @{const ALT} *}

   319 subsubsection {* The case for @{text "SEQ"}*}

   320 

   321 definition 

   322   tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)"

   323 where

   324   "tag_str_SEQ L1 L2 = 

   325      (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa.  xa \<le> x \<and> xa \<in> L1}))"

   326 

   327 

   328 lemma append_seq_elim:

   329   assumes "x @ y \<in> L\<^isub>1 ;; L\<^isub>2"

   330   shows "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2) \<or> 

   331           (\<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2)"

   332 proof-

   333   from assms obtain s\<^isub>1 s\<^isub>2 

   334     where "x @ y = s\<^isub>1 @ s\<^isub>2" 

   335     and in_seq: "s\<^isub>1 \<in> L\<^isub>1 \<and> s\<^isub>2 \<in> L\<^isub>2" 

   336     by (auto simp:Seq_def)

   337   hence "(x \<le> s\<^isub>1 \<and> (s\<^isub>1 - x) @ s\<^isub>2 = y) \<or> (s\<^isub>1 \<le> x \<and> (x - s\<^isub>1) @ y = s\<^isub>2)"

   338     using app_eq_dest by auto

   339   moreover have "\<lbrakk>x \<le> s\<^isub>1; (s\<^isub>1 - x) @ s\<^isub>2 = y\<rbrakk> \<Longrightarrow> 

   340                        \<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2" 

   341     using in_seq by (rule_tac x = "s\<^isub>1 - x" in exI, auto elim:prefixE)

   342   moreover have "\<lbrakk>s\<^isub>1 \<le> x; (x - s\<^isub>1) @ y = s\<^isub>2\<rbrakk> \<Longrightarrow> 

   343                     \<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2" 

   344     using in_seq by (rule_tac x = s\<^isub>1 in exI, auto)

   345   ultimately show ?thesis by blast

   346 qed

   347 

   348 lemma tag_str_SEQ_injI:

   349   "tag_str_SEQ L\<^isub>1 L\<^isub>2 m = tag_str_SEQ L\<^isub>1 L\<^isub>2 n \<Longrightarrow> m \<approx>(L\<^isub>1 ;; L\<^isub>2) n"

   350 proof-

   351   { fix x y z

   352     assume xz_in_seq: "x @ z \<in> L\<^isub>1 ;; L\<^isub>2"

   353     and tag_xy: "tag_str_SEQ L\<^isub>1 L\<^isub>2 x = tag_str_SEQ L\<^isub>1 L\<^isub>2 y"

   354     have"y @ z \<in> L\<^isub>1 ;; L\<^isub>2" 

   355     proof-

   356       have "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ z \<in> L\<^isub>2) \<or> 

   357                (\<exists> za \<le> z. (x @ za) \<in> L\<^isub>1 \<and> (z - za) \<in> L\<^isub>2)"

   358         using xz_in_seq append_seq_elim by simp

   359       moreover {

   360         fix xa

   361         assume h1: "xa \<le> x" and h2: "xa \<in> L\<^isub>1" and h3: "(x - xa) @ z \<in> L\<^isub>2"

   362         obtain ya where "ya \<le> y" and "ya \<in> L\<^isub>1" and "(y - ya) @ z \<in> L\<^isub>2" 

   363         proof -

   364           have "\<exists> ya.  ya \<le> y \<and> ya \<in> L\<^isub>1 \<and> (x - xa) \<approx>L\<^isub>2 (y - ya)"

   365           proof -

   366             have "{\<approx>L\<^isub>2 `` {x - xa} |xa. xa \<le> x \<and> xa \<in> L\<^isub>1} = 

   367                   {\<approx>L\<^isub>2 `` {y - xa} |xa. xa \<le> y \<and> xa \<in> L\<^isub>1}" 

   368                           (is "?Left = ?Right") 

   369               using h1 tag_xy by (auto simp:tag_str_SEQ_def)

   370             moreover have "\<approx>L\<^isub>2 `` {x - xa} \<in> ?Left" using h1 h2 by auto

   371             ultimately have "\<approx>L\<^isub>2 `` {x - xa} \<in> ?Right" by simp

   372             thus ?thesis by (auto simp:Image_def str_eq_rel_def str_eq_def)

   373           qed

   374           with prems show ?thesis by (auto simp:str_eq_rel_def str_eq_def)

   375         qed

   376         hence "y @ z \<in> L\<^isub>1 ;; L\<^isub>2" by (erule_tac prefixE, auto simp:Seq_def)          

   377       } moreover {

   378         fix za

   379         assume h1: "za \<le> z" and h2: "(x @ za) \<in> L\<^isub>1" and h3: "z - za \<in> L\<^isub>2"

   380         hence "y @ za \<in> L\<^isub>1"

   381         proof-

   382           have "\<approx>L\<^isub>1 `` {x} = \<approx>L\<^isub>1 `` {y}" 

   383             using h1 tag_xy by (auto simp:tag_str_SEQ_def)

   384           with h2 show ?thesis 

   385             by (auto simp:Image_def str_eq_rel_def str_eq_def) 

   386         qed

   387         with h1 h3 have "y @ z \<in> L\<^isub>1 ;; L\<^isub>2" 

   388           by (drule_tac A = L\<^isub>1 in seq_intro, auto elim:prefixE)

   389       }

   390       ultimately show ?thesis by blast

   391     qed

   392   } thus "tag_str_SEQ L\<^isub>1 L\<^isub>2 m = tag_str_SEQ L\<^isub>1 L\<^isub>2 n \<Longrightarrow> m \<approx>(L\<^isub>1 ;; L\<^isub>2) n" 

   393     by (auto simp add: str_eq_def str_eq_rel_def)

   394 qed 

   395 

   396 lemma quot_seq_finiteI [intro]:

   397   fixes L1 L2::"lang"

   398   assumes fin1: "finite (UNIV // \<approx>L1)" 

   399   and     fin2: "finite (UNIV // \<approx>L2)" 

   400   shows "finite (UNIV // \<approx>(L1 ;; L2))"

   401 proof (rule_tac tag = "tag_str_SEQ L1 L2" in tag_finite_imageD)

   402   show "\<And>x y. tag_str_SEQ L1 L2 x = tag_str_SEQ L1 L2 y \<Longrightarrow> x \<approx>(L1 ;; L2) y"

   403     by (rule tag_str_SEQ_injI)

   404 next

   405   have *: "finite ((UNIV // \<approx>L1) \<times> (Pow (UNIV // \<approx>L2)))" 

   406     using fin1 fin2 by auto

   407   show "finite (range (tag_str_SEQ L1 L2))" 

   408     unfolding tag_str_SEQ_def

   409     apply(rule finite_subset[OF _ *])

   410     unfolding quotient_def

   411     by auto

   412 qed

   413 

   414 subsubsection {* The case for @{const ALT} *}

   444 subsubsection {* The case for @{const "STAR"} *}

   381 subsubsection {* The inductive case for @{text "SEQ"}*}

   382 

   383 text {*

   384   For case @{const "SEQ"}, the language @{text "L"} is @{text "L\<^isub>1 ;; L\<^isub>2"}.

   385   Given @{text "x @ z \<in> L\<^isub>1 ;; L\<^isub>2"}, according to the defintion of @{text " L\<^isub>1 ;; L\<^isub>2"},

   386   string @{text "x @ z"} can be splitted with the prefix in @{text "L\<^isub>1"} and suffix in @{text "L\<^isub>2"}.

   387   The split point can either be in @{text "x"} (as shown in Fig. \ref{seq_first_split}),

   388   or in @{text "z"} (as shown in Fig. \ref{seq_snd_split}). Whichever way it goes, the structure

   389   on @{text "x @ z"} cn be transfered faithfully onto @{text "y @ z"} 

   390   (as shown in Fig. \ref{seq_trans_first_split} and \ref{seq_trans_snd_split}) with the the help of the assumed 

   391   tag equality. The following tag function @{text "tag_str_SEQ"} is such designed to facilitate

   392   such transfers and lemma @{text "tag_str_SEQ_injI"} formalizes the informal argument above. The details 

   393   of structure transfer will be given their.

   394 \input{fig_seq}

   395 

   396   *}

   397 

   398 definition 

   399   tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)"

   400 where

   401   "tag_str_SEQ L1 L2 = 

   402      (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa.  xa \<le> x \<and> xa \<in> L1}))"

   403 

   404 text {* The following is a techical lemma which helps to split the @{text "x @ z \<in> L\<^isub>1 ;; L\<^isub>2"} mentioned above.*}

   405 

   406 lemma append_seq_elim:

   407   assumes "x @ y \<in> L\<^isub>1 ;; L\<^isub>2"

   408   shows "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2) \<or> 

   409           (\<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2)"

   410 proof-

   411   from assms obtain s\<^isub>1 s\<^isub>2 

   412     where eq_xys: "x @ y = s\<^isub>1 @ s\<^isub>2" 

   413     and in_seq: "s\<^isub>1 \<in> L\<^isub>1 \<and> s\<^isub>2 \<in> L\<^isub>2" 

   414     by (auto simp:Seq_def)

   415   from app_eq_dest [OF eq_xys]

   416   have

   417     "(x \<le> s\<^isub>1 \<and> (s\<^isub>1 - x) @ s\<^isub>2 = y) \<or> (s\<^isub>1 \<le> x \<and> (x - s\<^isub>1) @ y = s\<^isub>2)" 

   418                (is "?Split1 \<or> ?Split2") .

   419   moreover have "?Split1 \<Longrightarrow> \<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2" 

   420     using in_seq by (rule_tac x = "s\<^isub>1 - x" in exI, auto elim:prefixE)

   421   moreover have "?Split2 \<Longrightarrow> \<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2" 

   422     using in_seq by (rule_tac x = s\<^isub>1 in exI, auto)

   423   ultimately show ?thesis by blast

   424 qed

   425 

   426 

   427 lemma tag_str_SEQ_injI:

   428   fixes v w 

   429   assumes eq_tag: "tag_str_SEQ L\<^isub>1 L\<^isub>2 v = tag_str_SEQ L\<^isub>1 L\<^isub>2 w" 

   430   shows "v \<approx>(L\<^isub>1 ;; L\<^isub>2) w"

   431 proof-

   432     -- {* As explained before, a pattern for just one direction needs to be dealt with:*}

   433   { fix x y z

   434     assume xz_in_seq: "x @ z \<in> L\<^isub>1 ;; L\<^isub>2"

   435     and tag_xy: "tag_str_SEQ L\<^isub>1 L\<^isub>2 x = tag_str_SEQ L\<^isub>1 L\<^isub>2 y"

   436     have"y @ z \<in> L\<^isub>1 ;; L\<^isub>2" 

   437     proof-

   438       -- {* There are two ways to split @{text "x@z"}: *}

   439       from append_seq_elim [OF xz_in_seq]

   440       have "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ z \<in> L\<^isub>2) \<or> 

   441                (\<exists> za \<le> z. (x @ za) \<in> L\<^isub>1 \<and> (z - za) \<in> L\<^isub>2)" .

   442       -- {* It can be shown that @{text "?thesis"} holds in either case: *}

   443       moreover {

   444         -- {* The case for the first split:*}

   445         fix xa

   446         assume h1: "xa \<le> x" and h2: "xa \<in> L\<^isub>1" and h3: "(x - xa) @ z \<in> L\<^isub>2"

   447         -- {* The following subgoal implements the structure transfer:*}

   448         obtain ya 

   449           where "ya \<le> y" 

   450           and "ya \<in> L\<^isub>1" 

   451           and "(y - ya) @ z \<in> L\<^isub>2"

   452         proof -

   453         -- {*

   454             \begin{minipage}{0.8\textwidth}

   455             By expanding the definition of 

   456             @{thm [display] "tag_xy"}

   457             and extracting the second compoent, we get:

   458             \end{minipage}

   459             *}

   460           have "{\<approx>L\<^isub>2 `` {x - xa} |xa. xa \<le> x \<and> xa \<in> L\<^isub>1} = 

   461                    {\<approx>L\<^isub>2 `` {y - ya} |ya. ya \<le> y \<and> ya \<in> L\<^isub>1}" (is "?Left = ?Right")

   462             using tag_xy unfolding tag_str_SEQ_def by simp

   463             -- {* Since @{thm "h1"} and @{thm "h2"} hold, it is not difficult to show: *}

   464           moreover have "\<approx>L\<^isub>2 `` {x - xa} \<in> ?Left" using h1 h2 by auto

   465             -- {* 

   466             \begin{minipage}{0.7\textwidth}

   467             Through tag equality, equivalent class @{term "\<approx>L\<^isub>2 `` {x - xa}"} also 

   468                   belongs to the @{text "?Right"}:

   469             \end{minipage}

   470             *}

   471           ultimately have "\<approx>L\<^isub>2 `` {x - xa} \<in> ?Right" by simp

   472             -- {* From this, the counterpart of @{text "xa"} in @{text "y"} is obtained:*}

   473           then obtain ya 

   474             where eq_xya: "\<approx>L\<^isub>2 `` {x - xa} = \<approx>L\<^isub>2 `` {y - ya}" 

   475             and pref_ya: "ya \<le> y" and ya_in: "ya \<in> L\<^isub>1"

   476             by simp blast

   477           -- {* It can be proved that @{text "ya"} has the desired property:*}

   478           have "(y - ya)@z \<in> L\<^isub>2" 

   479           proof -

   480             from eq_xya have "(x - xa)  \<approx>L\<^isub>2 (y - ya)" 

   481               unfolding Image_def str_eq_rel_def str_eq_def by auto

   482             with h3 show ?thesis unfolding str_eq_rel_def str_eq_def by simp

   483           qed

   484           -- {* Now, @{text "ya"} has all properties to be a qualified candidate:*}

   485           with pref_ya ya_in 

   486           show ?thesis using prems by blast

   487         qed

   488           -- {* From the properties of @{text "ya"}, @{text "y @ z \<in> L\<^isub>1 ;; L\<^isub>2"} is derived easily.*}

   489         hence "y @ z \<in> L\<^isub>1 ;; L\<^isub>2" by (erule_tac prefixE, auto simp:Seq_def)

   490       } moreover {

   491         -- {* The other case is even more simpler: *}

   492         fix za

   493         assume h1: "za \<le> z" and h2: "(x @ za) \<in> L\<^isub>1" and h3: "z - za \<in> L\<^isub>2"

   494         have "y @ za \<in> L\<^isub>1"

   495         proof-

   496           have "\<approx>L\<^isub>1 `` {x} = \<approx>L\<^isub>1 `` {y}" 

   497             using tag_xy unfolding tag_str_SEQ_def by simp

   498           with h2 show ?thesis

   499             unfolding Image_def str_eq_rel_def str_eq_def by auto

   500         qed

   501         with h1 h3 have "y @ z \<in> L\<^isub>1 ;; L\<^isub>2" 

   502           by (drule_tac A = L\<^isub>1 in seq_intro, auto elim:prefixE)

   503       }

   504       ultimately show ?thesis by blast

   505     qed

   506   } 

   507   -- {* 

   508       \begin{minipage}{0.8\textwidth}

   509       @{text "?thesis"} is proved by exploiting the symmetry of 

   510       @{thm [source] "eq_tag"}:

   511       \end{minipage}

   512       *}

   513   from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]

   514     show ?thesis unfolding str_eq_def str_eq_rel_def by blast

   515 qed 

   516 

   517 lemma quot_seq_finiteI [intro]:

   518   fixes L1 L2::"lang"

   519   assumes fin1: "finite (UNIV // \<approx>L1)" 

   520   and     fin2: "finite (UNIV // \<approx>L2)" 

   521   shows "finite (UNIV // \<approx>(L1 ;; L2))"

   522 proof (rule_tac tag = "tag_str_SEQ L1 L2" in tag_finite_imageD)

   523   show "\<And>x y. tag_str_SEQ L1 L2 x = tag_str_SEQ L1 L2 y \<Longrightarrow> x \<approx>(L1 ;; L2) y"

   524     by (rule tag_str_SEQ_injI)

   525 next

   526   have *: "finite ((UNIV // \<approx>L1) \<times> (Pow (UNIV // \<approx>L2)))" 

   527     using fin1 fin2 by auto

   528   show "finite (range (tag_str_SEQ L1 L2))" 

   529     unfolding tag_str_SEQ_def

   530     apply(rule finite_subset[OF _ *])

   531     unfolding quotient_def

   532     by auto

   533 qed

   534 

   535 subsubsection {* The inductive case for @{const "STAR"} *}

   452           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).

   543           such that @{text "xa \<in> L\<^isub>1*"} and @{text "(x - xa)@z \<in> L\<^isub>1*"}, as shown in Fig. \ref{first_split}.

   455           and name it @{text "xa_max"}, as shown in Fig. \ref{max_split}(b).

   546           and name it @{text "xa_max"}, as shown in Fig. \ref{max_split}.

   457            @{text "(x - xa_max) @ za \<in> L\<^isub>1"} and @{text "zb \<in> L\<^isub>1*"}  as shown in Fig. \ref{last_split}(d).

   548            @{text "(x - xa_max) @ za \<in> L\<^isub>1"} and @{text "zb \<in> L\<^isub>1*"}  as shown in Fig. \ref{last_split}.

   460             \item Because @{text "(x - x_max) @ z \<in> L\<^isub>1*"}, it can always be split into prefix @{text "a"}

   551             \item Because @{text "(x - x_max) @ z \<in> L\<^isub>1*"}, it can always be splitted into prefix @{text "a"}

   462               as shown in Fig. \ref{ab_split}(c).

   553               as shown in Fig. \ref{ab_split}.

   463             \item But the prefix @{text "a"} CANNOT be shorter than @{text "x - xa_max"}, otherwise

   554             \item But the prefix @{text "a"} CANNOT be shorter than @{text "x - xa_max"} 

   464                    @{text "xa_max"} is not the max in it's kind.

   555               (as shown in Fig. \ref{ab_split_wrong}), becasue otherwise,

   465             \item Now, @{text "za"} is just @{text "a - (x - xa_max)"} and @{text "zb"} is just @{text "b"}.

   556                    @{text "ma_max@a"} would be in the same kind as @{text "xa_max"} but with 

   557                    a larger size, conflicting with the fact that @{text "xa_max"} is the longest.

   469           can be transferred to @{text "y @ z"} as shown in Fig. \ref{trans_split}(e). The detailed steps are:

   561           can be transferred to @{text "y @ z"} as shown in Fig. \ref{trans_split}. The detailed steps are:

   481   \ref{transfer_step}4 feasible.

   573   \ref{ansfer_step} feasible.

   482 

   574 

   483    

   575   \input{fig_star}

   484 \begin{figure}[h!]

   485 \centering

   486 \subfigure[First split]{\label{first_split}

   487 \scalebox{0.9}{

   488 \begin{tikzpicture}

   489     \node[draw,minimum height=3.8ex] (xa) {$\hspace{2em}xa\hspace{2em}$};

   490     \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{5em}x - xa\hspace{5em}$ };

   491     \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{21em}$ };

   492 

   493     \draw[decoration={brace,transform={yscale=3}},decorate]

   494            (xa.north west) -- ($(xxa.north east)+(0em,0em)$)

   495                node[midway, above=0.5em]{$x$};

   496 

   497     \draw[decoration={brace,transform={yscale=3}},decorate]

   498            (z.north west) -- ($(z.north east)+(0em,0em)$)

   499                node[midway, above=0.5em]{$z$};

   500 

   501     \draw[decoration={brace,transform={yscale=3}},decorate]

   502            ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)

   503                node[midway, above=0.8em]{$x @ z \in L_1*$};

   504 

   505     \draw[decoration={brace,transform={yscale=3}},decorate]

   506            ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)

   507                node[midway, below=0.5em]{$(x - xa) @ z \in L_1*$};

   508 

   509     \draw[decoration={brace,transform={yscale=3}},decorate]

   510            ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)

   511                node[midway, below=0.5em]{$xa \in L_1*$};

   512 \end{tikzpicture}}}

   513 

   514 \subfigure[Max split]{\label{max_split}

   515 \scalebox{0.9}{

   516 \begin{tikzpicture}

   517     \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}xa\_max\hspace{4em}$ };

   518     \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - xa\_max\hspace{0.5em}$ };

   519     \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{21em}$ };

   520 

   521     \draw[decoration={brace,transform={yscale=3}},decorate]

   522            (xa.north west) -- ($(xxa.north east)+(0em,0em)$)

   523                node[midway, above=0.5em]{$x$};

   524 

   525     \draw[decoration={brace,transform={yscale=3}},decorate]

   526            (z.north west) -- ($(z.north east)+(0em,0em)$)

   527                node[midway, above=0.5em]{$z$};

   528 

   529     \draw[decoration={brace,transform={yscale=3}},decorate]

   530            ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)

   531                node[midway, above=0.8em]{$x @ z \in L_1*$};

   532 

   533     \draw[decoration={brace,transform={yscale=3}},decorate]

   534            ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)

   535                node[midway, below=0.5em]{$(x - xa\_max) @ z \in L_1*$};

   536 

   537     \draw[decoration={brace,transform={yscale=3}},decorate]

   538            ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)

   539                node[midway, below=0.5em]{$xa \in L_1*$};

   540 \end{tikzpicture}}}

   541 

   542 \subfigure[Max split with $a$ and $b$]{\label{ab_split}

   543 \scalebox{0.9}{

   544 \begin{tikzpicture}

   545     \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}xa\_max\hspace{4em}$ };

   546     \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - xa\_max\hspace{0.5em}$ };

   547     \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{21em}$ };

   548 

   549     \draw[decoration={brace,transform={yscale=3}},decorate]

   550            (xa.north west) -- ($(xxa.north east)+(0em,0em)$)

   551                node[midway, above=0.5em]{$x$};

   552 

   553     \draw[decoration={brace,transform={yscale=3}},decorate]

   554            (z.north west) -- ($(z.north east)+(0em,0em)$)

   555                node[midway, above=0.5em]{$z$};

   556 

   557     \draw[decoration={brace,transform={yscale=3}},decorate]

   558            ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)

   559                node[midway, above=0.8em]{$x @ z \in L_1*$};

   560 

   561     \draw[decoration={brace,transform={yscale=3}},decorate]

   562            ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)

   563                node[midway, below=0.5em]{$(x - xa\_max) @ z \in L_1*$};

   564 

   565     \draw[decoration={brace,transform={yscale=3}},decorate]

   566            ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)

   567                node[midway, below=0.5em]{$xa \in L_1*$};

   568 

   569     \draw[decoration={brace,transform={yscale=3}},decorate]

   570            ($(xxa.south east)+(6em,-5ex)$) -- ($(xxa.south west)+(0em,-5ex)$)

   571                node[midway, below=0.5em]{$a \in L_1$};

   572 

   573     \draw[decoration={brace,transform={yscale=3}},decorate]

   574            ($(z.south east)+(0em,-5ex)$) -- ($(xxa.south east)+(6em,-5ex)$)

   575                node[midway, below=0.5em]{$b \in L_1*$};

   576 

   577 \end{tikzpicture}}}

   578 

   579 \subfigure[Last split]{\label{last_split}

   580 \scalebox{0.9}{

   581 \begin{tikzpicture}

   582     \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}xa\_max\hspace{4em}$ };

   583     \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - xa\_max\hspace{0.5em}$ };

   584     \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (za) { $\hspace{2em}za\hspace{2em}$ };

   585     \node[draw,minimum height=3.8ex, right=-0.03em of za] (zb) { $\hspace{7em}zb\hspace{7em}$ };

   586 

   587     \draw[decoration={brace,transform={yscale=3}},decorate]

   588            (xa.north west) -- ($(xxa.north east)+(0em,0em)$)

   589                node[midway, above=0.5em]{$x$};

   590 

   591     \draw[decoration={brace,transform={yscale=3}},decorate]

   592            (za.north west) -- ($(zb.north east)+(0em,0em)$)

   593                node[midway, above=0.5em]{$z$};

   594 

   595     \draw[decoration={brace,transform={yscale=3}},decorate]

   596            ($(xa.north west)+(0em,3ex)$) -- ($(zb.north east)+(0em,3ex)$)

   597                node[midway, above=0.8em]{$x @ z \in L_1*$};

   598 

   599     \draw[decoration={brace,transform={yscale=3}},decorate]

   600            ($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)

   601                node[midway, below=0.5em]{$(x - xa\_max) @ za \in L_1$};

   602 

   603     \draw[decoration={brace,transform={yscale=3}},decorate]

   604            ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)

   605                node[midway, below=0.5em]{$xa\_max \in L_1*$};

   606 

   607     \draw[decoration={brace,transform={yscale=3}},decorate]

   608            ($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)

   609                node[midway, below=0.5em]{$zb \in L_1*$};

   610 

   611     \draw[decoration={brace,transform={yscale=3}},decorate]

   612            ($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$)

   613                node[midway, below=0.5em]{$(x - xa\_max)@z \in L_1*$};

   614 \end{tikzpicture}}}

   615 

   616 

   617 \subfigure[Transferring to $y$]{\label{trans_split}

   618 \scalebox{0.9}{

   619 \begin{tikzpicture}

   620     \node[draw,minimum height=3.8ex] (xa) { $\hspace{5em}ya\hspace{5em}$ };

   621     \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{2em}y - ya\hspace{2em}$ };

   622     \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (za) { $\hspace{2em}za\hspace{2em}$ };

   623     \node[draw,minimum height=3.8ex, right=-0.03em of za] (zb) { $\hspace{7em}zb\hspace{7em}$ };

   624 

   625     \draw[decoration={brace,transform={yscale=3}},decorate]

   626            (xa.north west) -- ($(xxa.north east)+(0em,0em)$)

   627                node[midway, above=0.5em]{$y$};

   628 

   629     \draw[decoration={brace,transform={yscale=3}},decorate]

   630            (za.north west) -- ($(zb.north east)+(0em,0em)$)

   631                node[midway, above=0.5em]{$z$};

   632 

   633     \draw[decoration={brace,transform={yscale=3}},decorate]

   634            ($(xa.north west)+(0em,3ex)$) -- ($(zb.north east)+(0em,3ex)$)

   635                node[midway, above=0.8em]{$y @ z \in L_1*$};

   636 

   637     \draw[decoration={brace,transform={yscale=3}},decorate]

   638            ($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)

   639                node[midway, below=0.5em]{$(y - ya) @ za \in L_1$};

   640 

   641     \draw[decoration={brace,transform={yscale=3}},decorate]

   642            ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)

   643                node[midway, below=0.5em]{$ya \in L_1*$};

   644 

   645     \draw[decoration={brace,transform={yscale=3}},decorate]

   646            ($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)

   647                node[midway, below=0.5em]{$zb \in L_1*$};

   648 

   649     \draw[decoration={brace,transform={yscale=3}},decorate]

   650            ($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$)

   651                node[midway, below=0.5em]{$(y - ya)@z \in L_1*$};

   652 \end{tikzpicture}}}

   653 

   654 \caption{The case for $STAR$}

   655 \end{figure}

   656 

   691 text {* Technical lemma. *}

   610 text {* The following is a technical lemma.which helps to show the range finiteness of tag function. *}

   703     -- {* 

   622     -- {* As explained before, a pattern for just one direction needs to be dealt with:*}

   704     \begin{minipage}{0.9\textwidth}

   705     According to the definition of @{text "\<approx>Lang"}, 

   706     proving @{text "v \<approx>(L\<^isub>1\<star>) w"} amounts to

   707     showing: for any string @{text "u"},

   708     if @{text "v @ u \<in> (L\<^isub>1\<star>)"} then @{text "w @ u \<in> (L\<^isub>1\<star>)"} and vice versa.

   709     The reasoning pattern for both directions are the same, as derived

   710     in the following:

   711     \end{minipage}

   712     *}

   726         -- {*

   636         -- {* The nontrival case:

   727         \begin{minipage}{0.9\textwidth}

   728         The case when @{text "x"} is not null, and

   729         @{text "x @ z"} is in @{text "L\<^isub>1\<star>"}, 

   730         \end{minipage}

   734         \begin{minipage}{0.9\textwidth}

   640         \begin{minipage}{0.8\textwidth}

   735         Since @{text "x @ z \<in> L\<^isub>1\<star>"}, @{text "x"} can always be splited

   641         Since @{text "x @ z \<in> L\<^isub>1\<star>"}, @{text "x"} can always be splitted

   748       -- {* Since @{text "?S"} is finite, we can always single out the longest

   654       -- {* \begin{minipage}{0.7\textwidth} 

   749           and name it @{text "xa_max"}:

   655             Since @{text "?S"} is finite, we can always single out the longest and name it @{text "xa_max"}: 

   656             \end{minipage}

   761           \begin{minipage}{0.9\textwidth}

   668           \begin{minipage}{0.8\textwidth}

   779           \begin{minipage}{0.9\textwidth}

   686           \begin{minipage}{0.8\textwidth}

   780           If the following proposition can be proved, then the @{text "?thesis"}:

   687           The @{text "?thesis"}, @{prop "y @ z \<in> L\<^isub>1\<star>"}, is a simple consequence

   781           @{text "y @ z \<in> L\<^isub>1\<star>"} is just a simple consequence.

   688           of the following proposition:

   792             \begin{minipage}{0.9\textwidth}

   699             \begin{minipage}{0.8\textwidth}

   793             Since @{text  "(x - xa_max) @ z"} is in @{text "L\<^isub>1\<star>"}, it can be split into

   700             Since @{thm "h1"}, @{text "x"} can be splitted into

   809               \begin{minipage}{0.9\textwidth}

   716               \begin{minipage}{0.8\textwidth}

   810               Since @{text "(x - xa_max) @ z = a @ b"}, the string @{text "(x - xa_max) @ z"}

   717               Since @{text "(x - xa_max) @ z = a @ b"}, string @{text "(x - xa_max) @ z"}

   811               could be splited in two ways:

   718               can be splitted in two ways:

   845             \begin{minipage}{0.9\textwidth}

   752            @{text "?thesis"} can easily be shown using properties of @{text "za"} and @{text "zb"}:

   846             From the properties of @{text "za"} and @{text "zb"} such obtained,

   847               @{text "?thesis"} can be shown easily. 

   848             \end{minipage}

   861     show  ?thesis by (unfold str_eq_def str_eq_rel_def, blast)

   765     show  ?thesis unfolding str_eq_def str_eq_rel_def by blast

   862 qed

   766 qed

   863 

   767 

   864 

   768 

   865 lemma -- {* The oringal version with a poor readability*}

   769 lemma -- {* The oringal version with less explicit details. *}

   871     \begin{minipage}{0.9\textwidth}

   775     \begin{minipage}{0.8\textwidth}

   894         \begin{minipage}{0.9\textwidth}

   798         \begin{minipage}{0.8\textwidth}

   970     show  ?thesis by (unfold str_eq_def str_eq_rel_def, blast)

   874     show  ?thesis unfolding str_eq_def str_eq_rel_def by blast