1 theory Myhill_2

     2   imports Myhill_1

     3 begin

     4 

     5 section {* Direction @{text "regular language \<Rightarrow>finite partition"} *}

     6 

     7 subsection {* The scheme*}

     8 

     9 text {* 

    10   The following convenient notation @{text "x \<approx>Lang y"} means:

    11   string @{text "x"} and @{text "y"} are equivalent with respect to 

    12   language @{text "Lang"}.

    13   *}

    14 

    15 definition

    16   str_eq :: "string \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> bool" ("_ \<approx>_ _")

    17 where

    18   "x \<approx>Lang y \<equiv> (x, y) \<in> (\<approx>Lang)"

    19 

    20 text {*

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

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

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

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

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

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

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

    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:

    34   \begin{enumerate}

    35     \item First, the tagging function @{text "tag"} induces an equivalent relation @{text "(=tag=)"} 

    36           (defiintion of @{text "f_eq_rel"} and lemma @{text "equiv_f_eq_rel"}).

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

    38            the partition given rise by @{text "(=tag=)"} is finite (lemma @{text "finite_eq_f_rel"}).

    39            Since tags are made from equivalent classes from component partitions, and the inductive

    40            hypothesis ensures the finiteness of these partitions, it is not difficult to prove

    41            the finiteness of @{text "range(tag)"}.

    42     \item It is proved that if equivalent relation @{text "R1"} is more refined than @{text "R2"}

    43            (expressed as @{text "R1 \<subseteq> R2"}),

    44            and the partition induced by @{text "R1"} is finite, then the partition induced by @{text "R2"}

    45            is finite as well (lemma @{text "refined_partition_finite"}).

    46     \item The injectivity assumption @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"} implies that

    47             @{text "(=tag=)"} is more refined than @{text "(\<approx>Lang)"}.

    48     \item Combining the points above, we have: the partition induced by language @{text "Lang"}

    49           is finite (lemma @{text "tag_finite_imageD"}).

    50   \end{enumerate}

    51 *}

    52 

    53 definition 

    54    f_eq_rel ("=_=")

    55 where

    56    "(=f=) = {(x, y) | x y. f x = f y}"

    57 

    58 lemma equiv_f_eq_rel:"equiv UNIV (=f=)"

    59   by (auto simp:equiv_def f_eq_rel_def refl_on_def sym_def trans_def)

    60 

    61 lemma finite_range_image: "finite (range f) \<Longrightarrow> finite (f ` A)"

    62   by (rule_tac B = "{y. \<exists>x. y = f x}" in finite_subset, auto simp:image_def)

    63 

    64 lemma finite_eq_f_rel:

    65   assumes rng_fnt: "finite (range tag)"

    66   shows "finite (UNIV // (=tag=))"

    67 proof -

    68   let "?f" =  "op ` tag" and ?A = "(UNIV // (=tag=))"

    69   show ?thesis

    70   proof (rule_tac f = "?f" and A = ?A in finite_imageD) 

    71     -- {* 

    72       The finiteness of @{text "f"}-image is a simple consequence of assumption @{text "rng_fnt"}:

    73       *}

    74     show "finite (?f ` ?A)" 

    75     proof -

    76       have "\<forall> X. ?f X \<in> (Pow (range tag))" by (auto simp:image_def Pow_def)

    77       moreover from rng_fnt have "finite (Pow (range tag))" by simp

    78       ultimately have "finite (range ?f)"

    79         by (auto simp only:image_def intro:finite_subset)

    80       from finite_range_image [OF this] show ?thesis .

    81     qed

    82   next

    83     -- {* 

    84       The injectivity of @{text "f"}-image is a consequence of the definition of @{text "(=tag=)"}:

    85       *}

    86     show "inj_on ?f ?A" 

    87     proof-

    88       { fix X Y

    89         assume X_in: "X \<in> ?A"

    90           and  Y_in: "Y \<in> ?A"

    91           and  tag_eq: "?f X = ?f Y"

    92         have "X = Y"

    93         proof -

    94           from X_in Y_in tag_eq 

    95           obtain x y 

    96             where x_in: "x \<in> X" and y_in: "y \<in> Y" and eq_tg: "tag x = tag y"

    97             unfolding quotient_def Image_def str_eq_rel_def 

    98                                    str_eq_def image_def f_eq_rel_def

    99             apply simp by blast

   100           with X_in Y_in show ?thesis 

   101             by (auto simp:quotient_def str_eq_rel_def str_eq_def f_eq_rel_def) 

   102         qed

   103       } thus ?thesis unfolding inj_on_def by auto

   104     qed

   105   qed

   106 qed

   107 

   108 lemma finite_image_finite: "\<lbrakk>\<forall> x \<in> A. f x \<in> B; finite B\<rbrakk> \<Longrightarrow> finite (f ` A)"

   109   by (rule finite_subset [of _ B], auto)

   110 

   111 lemma refined_partition_finite:

   112   fixes R1 R2 A

   113   assumes fnt: "finite (A // R1)"

   114   and refined: "R1 \<subseteq> R2"

   115   and eq1: "equiv A R1" and eq2: "equiv A R2"

   116   shows "finite (A // R2)"

   117 proof -

   118   let ?f = "\<lambda> X. {R1 `` {x} | x. x \<in> X}" 

   119     and ?A = "(A // R2)" and ?B = "(A // R1)"

   120   show ?thesis

   121   proof(rule_tac f = ?f and A = ?A in finite_imageD)

   122     show "finite (?f ` ?A)"

   123     proof(rule finite_subset [of _ "Pow ?B"])

   124       from fnt show "finite (Pow (A // R1))" by simp

   125     next

   126       from eq2

   127       show " ?f ` A // R2 \<subseteq> Pow ?B"

   128         unfolding image_def Pow_def quotient_def

   129         apply auto

   130         by (rule_tac x = xb in bexI, simp, 

   131                  unfold equiv_def sym_def refl_on_def, blast)

   132     qed

   133   next

   134     show "inj_on ?f ?A"

   135     proof -

   136       { fix X Y

   137         assume X_in: "X \<in> ?A" and Y_in: "Y \<in> ?A" 

   138           and eq_f: "?f X = ?f Y" (is "?L = ?R")

   139         have "X = Y" using X_in

   140         proof(rule quotientE)

   141           fix x

   142           assume "X = R2 `` {x}" and "x \<in> A" with eq2

   143           have x_in: "x \<in> X" 

   144             unfolding equiv_def quotient_def refl_on_def by auto

   145           with eq_f have "R1 `` {x} \<in> ?R" by auto

   146           then obtain y where 

   147             y_in: "y \<in> Y" and eq_r: "R1 `` {x} = R1 ``{y}" by auto

   148           have "(x, y) \<in> R1"

   149           proof -

   150             from x_in X_in y_in Y_in eq2

   151             have "x \<in> A" and "y \<in> A" 

   152               unfolding equiv_def quotient_def refl_on_def by auto

   153             from eq_equiv_class_iff [OF eq1 this] and eq_r

   154             show ?thesis by simp

   155           qed

   156           with refined have xy_r2: "(x, y) \<in> R2" by auto

   157           from quotient_eqI [OF eq2 X_in Y_in x_in y_in this]

   158           show ?thesis .

   159         qed

   160       } thus ?thesis by (auto simp:inj_on_def)

   161     qed

   162   qed

   163 qed

   164 

   165 lemma equiv_lang_eq: "equiv UNIV (\<approx>Lang)"

   166   unfolding equiv_def str_eq_rel_def sym_def refl_on_def trans_def

   167   by blast

   168 

   169 lemma tag_finite_imageD:

   170   fixes tag

   171   assumes rng_fnt: "finite (range tag)" 

   172   -- {* Suppose the rang of tagging fucntion @{text "tag"} is finite. *}

   173   and same_tag_eqvt: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<approx>Lang n"

   174   -- {* And strings with same tag are equivalent *}

   175   shows "finite (UNIV // (\<approx>Lang))"

   176 proof -

   177   let ?R1 = "(=tag=)"

   178   show ?thesis

   179   proof(rule_tac refined_partition_finite [of _ ?R1])

   180     from finite_eq_f_rel [OF rng_fnt]

   181      show "finite (UNIV // =tag=)" . 

   182    next

   183      from same_tag_eqvt

   184      show "(=tag=) \<subseteq> (\<approx>Lang)"

   185        by (auto simp:f_eq_rel_def str_eq_def)

   186    next

   187      from equiv_f_eq_rel

   188      show "equiv UNIV (=tag=)" by blast

   189    next

   190      from equiv_lang_eq

   191      show "equiv UNIV (\<approx>Lang)" by blast

   192   qed

   193 qed

   194 

   195 text {*

   196   A more concise, but less intelligible argument for @{text "tag_finite_imageD"} 

   197   is given as the following. The basic idea is still using standard library 

   198   lemma @{thm [source] "finite_imageD"}:

   199   \[

   200   @{thm "finite_imageD" [no_vars]}

   201   \]

   202   which says: if the image of injective function @{text "f"} over set @{text "A"} is 

   203   finite, then @{text "A"} must be finte, as we did in the lemmas above.

   204   *}

   205 

   206 lemma 

   207   fixes tag

   208   assumes rng_fnt: "finite (range tag)" 

   209   -- {* Suppose the rang of tagging fucntion @{text "tag"} is finite. *}

   210   and same_tag_eqvt: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<approx>Lang n"

   211   -- {* And strings with same tag are equivalent *}

   212   shows "finite (UNIV // (\<approx>Lang))"

   213   -- {* Then the partition generated by @{text "(\<approx>Lang)"} is finite. *}

   214 proof -

   215   -- {* The particular @{text "f"} and @{text "A"} used in @{thm [source] "finite_imageD"} are:*}

   216   let "?f" =  "op ` tag" and ?A = "(UNIV // \<approx>Lang)"

   217   show ?thesis

   218   proof (rule_tac f = "?f" and A = ?A in finite_imageD) 

   219     -- {* 

   220       The finiteness of @{text "f"}-image is a simple consequence of assumption @{text "rng_fnt"}:

   221       *}

   222     show "finite (?f ` ?A)" 

   223     proof -

   224       have "\<forall> X. ?f X \<in> (Pow (range tag))" by (auto simp:image_def Pow_def)

   225       moreover from rng_fnt have "finite (Pow (range tag))" by simp

   226       ultimately have "finite (range ?f)"

   227         by (auto simp only:image_def intro:finite_subset)

   228       from finite_range_image [OF this] show ?thesis .

   229     qed

   230   next

   231     -- {* 

   232       The injectivity of @{text "f"} is the consequence of assumption @{text "same_tag_eqvt"}:

   233       *}

   234     show "inj_on ?f ?A" 

   235     proof-

   236       { fix X Y

   237         assume X_in: "X \<in> ?A"

   238           and  Y_in: "Y \<in> ?A"

   239           and  tag_eq: "?f X = ?f Y"

   240         have "X = Y"

   241         proof -

   242           from X_in Y_in tag_eq 

   243           obtain x y where x_in: "x \<in> X" and y_in: "y \<in> Y" and eq_tg: "tag x = tag y"

   244             unfolding quotient_def Image_def str_eq_rel_def str_eq_def image_def

   245             apply simp by blast 

   246           from same_tag_eqvt [OF eq_tg] have "x \<approx>Lang y" .

   247           with X_in Y_in x_in y_in

   248           show ?thesis by (auto simp:quotient_def str_eq_rel_def str_eq_def) 

   249         qed

   250       } thus ?thesis unfolding inj_on_def by auto

   251     qed

   252   qed

   253 qed

   254 

   255 subsection {* The proof*}

   256 

   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   For ever inductive case, there are two tasks, the easier one is to show the range finiteness of

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

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

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

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

   266   \[

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

   268   \]

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

   270   \[

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

   272   \]

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

   274   it is suffcient to show just one direction:

   275   \[

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

   277   \]

   278   This is the pattern followed by every inductive case.

   279   *}

   280 

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

   282 

   283 lemma quot_null_eq:

   284   shows "(UNIV // \<approx>{}) = ({UNIV}::lang set)"

   285   unfolding quotient_def Image_def str_eq_rel_def by auto

   286 

   287 lemma quot_null_finiteI [intro]:

   288   shows "finite ((UNIV // \<approx>{})::lang set)"

   289 unfolding quot_null_eq by simp

   290 

   291 

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

   293 

   294 

   295 lemma quot_empty_subset:

   296   "UNIV // (\<approx>{[]}) \<subseteq> {{[]}, UNIV - {[]}}"

   297 proof

   298   fix x

   299   assume "x \<in> UNIV // \<approx>{[]}"

   300   then obtain y where h: "x = {z. (y, z) \<in> \<approx>{[]}}" 

   301     unfolding quotient_def Image_def by blast

   302   show "x \<in> {{[]}, UNIV - {[]}}"

   303   proof (cases "y = []")

   304     case True with h

   305     have "x = {[]}" by (auto simp: str_eq_rel_def)

   306     thus ?thesis by simp

   307   next

   308     case False with h

   309     have "x = UNIV - {[]}" by (auto simp: str_eq_rel_def)

   310     thus ?thesis by simp

   311   qed

   312 qed

   313 

   314 lemma quot_empty_finiteI [intro]:

   315   shows "finite (UNIV // (\<approx>{[]}))"

   316 by (rule finite_subset[OF quot_empty_subset]) (simp)

   317 

   318 

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

   320 

   321 lemma quot_char_subset:

   322   "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}"

   323 proof 

   324   fix x 

   325   assume "x \<in> UNIV // \<approx>{[c]}"

   326   then obtain y where h: "x = {z. (y, z) \<in> \<approx>{[c]}}" 

   327     unfolding quotient_def Image_def by blast

   328   show "x \<in> {{[]},{[c]}, UNIV - {[], [c]}}"

   329   proof -

   330     { assume "y = []" hence "x = {[]}" using h 

   331         by (auto simp:str_eq_rel_def)

   332     } moreover {

   333       assume "y = [c]" hence "x = {[c]}" using h 

   334         by (auto dest!:spec[where x = "[]"] simp:str_eq_rel_def)

   335     } moreover {

   336       assume "y \<noteq> []" and "y \<noteq> [c]"

   337       hence "\<forall> z. (y @ z) \<noteq> [c]" by (case_tac y, auto)

   338       moreover have "\<And> p. (p \<noteq> [] \<and> p \<noteq> [c]) = (\<forall> q. p @ q \<noteq> [c])" 

   339         by (case_tac p, auto)

   340       ultimately have "x = UNIV - {[],[c]}" using h

   341         by (auto simp add:str_eq_rel_def)

   342     } ultimately show ?thesis by blast

   343   qed

   344 qed

   345 

   346 lemma quot_char_finiteI [intro]:

   347   shows "finite (UNIV // (\<approx>{[c]}))"

   348 by (rule finite_subset[OF quot_char_subset]) (simp)

   349 

   350 

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

   352 

   353 definition 

   354   tag_str_ALT :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang)"

   355 where

   356   "tag_str_ALT L1 L2 = (\<lambda>x. (\<approx>L1 `` {x}, \<approx>L2 `` {x}))"

   357 

   358 lemma quot_union_finiteI [intro]:

   359   fixes L1 L2::"lang"

   360   assumes finite1: "finite (UNIV // \<approx>L1)"

   361   and     finite2: "finite (UNIV // \<approx>L2)"

   362   shows "finite (UNIV // \<approx>(L1 \<union> L2))"

   363 proof (rule_tac tag = "tag_str_ALT L1 L2" in tag_finite_imageD)

   364   show "\<And>x y. tag_str_ALT L1 L2 x = tag_str_ALT L1 L2 y \<Longrightarrow> x \<approx>(L1 \<union> L2) y"

   365     unfolding tag_str_ALT_def 

   366     unfolding str_eq_def

   367     unfolding Image_def 

   368     unfolding str_eq_rel_def

   369     by auto

   370 next

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

   372     using finite1 finite2 by auto

   373   show "finite (range (tag_str_ALT L1 L2))"

   374     unfolding tag_str_ALT_def

   375     apply(rule finite_subset[OF _ *])

   376     unfolding quotient_def

   377     by auto

   378 qed

   379 

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

   381 

   382 text {*

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

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

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

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

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

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

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

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

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

   392   of structure transfer will be given their.

   393 \input{fig_seq}

   394 

   395   *}

   396 

   397 definition 

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

   399 where

   400   "tag_str_SEQ L1 L2 = 

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

   402 

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

   404 

   405 lemma append_seq_elim:

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

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

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

   409 proof-

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

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

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

   413     by (auto simp:Seq_def)

   414   from app_eq_dest [OF eq_xys]

   415   have

   416     "(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)" 

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

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

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

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

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

   422   ultimately show ?thesis by blast

   423 qed

   424 

   425 

   426 lemma tag_str_SEQ_injI:

   427   fixes v w 

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

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

   430 proof-

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

   432   { fix x y z

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

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

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

   436     proof-

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

   438       from append_seq_elim [OF xz_in_seq]

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

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

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

   442       moreover {

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

   444         fix xa

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

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

   447         obtain ya 

   448           where "ya \<le> y" 

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

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

   451         proof -

   452         -- {*

   453             \begin{minipage}{0.8\textwidth}

   454             By expanding the definition of 

   455             @{thm [display] "tag_xy"}

   456             and extracting the second compoent, we get:

   457             \end{minipage}

   458             *}

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

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

   461             using tag_xy unfolding tag_str_SEQ_def by simp

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

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

   464             -- {* 

   465             \begin{minipage}{0.7\textwidth}

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

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

   468             \end{minipage}

   469             *}

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

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

   472           then obtain ya 

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

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

   475             by simp blast

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

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

   478           proof -

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

   480               unfolding Image_def str_eq_rel_def str_eq_def by auto

   481             with h3 show ?thesis unfolding str_eq_rel_def str_eq_def by simp

   482           qed

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

   484           with pref_ya ya_in 

   485           show ?thesis using that by blast

   486         qed

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

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

   489       } moreover {

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

   491         fix za

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

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

   494         proof-

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

   496             using tag_xy unfolding tag_str_SEQ_def by simp

   497           with h2 show ?thesis

   498             unfolding Image_def str_eq_rel_def str_eq_def by auto

   499         qed

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

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

   502       }

   503       ultimately show ?thesis by blast

   504     qed

   505   } 

   506   -- {* 

   507       \begin{minipage}{0.8\textwidth}

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

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

   510       \end{minipage}

   511       *}

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

   513     show ?thesis unfolding str_eq_def str_eq_rel_def by blast

   514 qed 

   515 

   516 lemma quot_seq_finiteI [intro]:

   517   fixes L1 L2::"lang"

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

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

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

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

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

   523     by (rule tag_str_SEQ_injI)

   524 next

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

   526     using fin1 fin2 by auto

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

   528     unfolding tag_str_SEQ_def

   529     apply(rule finite_subset[OF _ *])

   530     unfolding quotient_def

   531     by auto

   532 qed

   533 

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

   535 

   536 text {* 

   537   This turned out to be the trickiest case. The essential goal is 

   538   to proved @{text "y @ z \<in>  L\<^isub>1*"} under the assumptions that @{text "x @ z \<in>  L\<^isub>1*"}

   539   and that @{text "x"} and @{text "y"} have the same tag. The reasoning goes as the following:

   540   \begin{enumerate}

   541     \item Since @{text "x @ z \<in>  L\<^isub>1*"} holds, a prefix @{text "xa"} of @{text "x"} can be found

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

   543           Such a prefix always exists, @{text "xa = []"}, for example, is one. 

   544     \item There could be many but fintie many of such @{text "xa"}, from which we can find the longest

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

   546     \item The next step is to split @{text "z"} into @{text "za"} and @{text "zb"} such that

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

   548           Such a split always exists because:

   549           \begin{enumerate}

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

   551               and suffix @{text "b"}, such that @{text "a \<in> L\<^isub>1"} and @{text "b \<in> L\<^isub>1*"},

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

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

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

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

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

   557           \end{enumerate}

   558     \item  \label{tansfer_step} 

   559          By the assumption that @{text "x"} and @{text "y"} have the same tag, the structure on @{text "x @ z"}

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

   561           \begin{enumerate}

   562             \item A @{text "y"}-prefix @{text "ya"} corresponding to @{text "xa"} can be found, 

   563                   which satisfies conditions: @{text "ya \<in> L\<^isub>1*"} and @{text "(y - ya)@za \<in> L\<^isub>1"}.

   564             \item Since we already know @{text "zb \<in> L\<^isub>1*"}, we get @{text "(y - ya)@za@zb \<in> L\<^isub>1*"},

   565                   and this is just @{text "(y - ya)@z \<in> L\<^isub>1*"}.

   566             \item With fact @{text "ya \<in> L\<^isub>1*"}, we finally get @{text "y@z \<in> L\<^isub>1*"}.

   567           \end{enumerate}

   568   \end{enumerate}

   569 

   570   The formal proof of lemma @{text "tag_str_STAR_injI"} faithfully follows this informal argument 

   571   while the tagging function @{text "tag_str_STAR"} is defined to make the transfer in step

   572   \ref{ansfer_step} feasible.

   573 

   574   \input{fig_star}

   575 *} 

   576 

   577 definition 

   578   tag_str_STAR :: "lang \<Rightarrow> string \<Rightarrow> lang set"

   579 where

   580   "tag_str_STAR L1 = (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})"

   581 

   582 text {* A technical lemma. *}

   583 lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> 

   584            (\<exists> max \<in> A. \<forall> a \<in> A. f a <= (f max :: nat))"

   585 proof (induct rule:finite.induct)

   586   case emptyI thus ?case by simp

   587 next

   588   case (insertI A a)

   589   show ?case

   590   proof (cases "A = {}")

   591     case True thus ?thesis by (rule_tac x = a in bexI, auto)

   592   next

   593     case False

   594     with insertI.hyps and False  

   595     obtain max 

   596       where h1: "max \<in> A" 

   597       and h2: "\<forall>a\<in>A. f a \<le> f max" by blast

   598     show ?thesis

   599     proof (cases "f a \<le> f max")

   600       assume "f a \<le> f max"

   601       with h1 h2 show ?thesis by (rule_tac x = max in bexI, auto)

   602     next

   603       assume "\<not> (f a \<le> f max)"

   604       thus ?thesis using h2 by (rule_tac x = a in bexI, auto)

   605     qed

   606   qed

   607 qed

   608 

   609 

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

   611 lemma finite_strict_prefix_set: "finite {xa. xa < (x::string)}"

   612 apply (induct x rule:rev_induct, simp)

   613 apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}")

   614 by (auto simp:strict_prefix_def)

   615 

   616 

   617 lemma tag_str_STAR_injI:

   618   fixes v w

   619   assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_STAR L\<^isub>1 w"

   620   shows "(v::string) \<approx>(L\<^isub>1\<star>) w"

   621 proof-

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

   623   { fix x y z

   624     assume xz_in_star: "x @ z \<in> L\<^isub>1\<star>" 

   625       and tag_xy: "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y"

   626     have "y @ z \<in> L\<^isub>1\<star>"

   627     proof(cases "x = []")

   628       -- {* 

   629         The degenerated case when @{text "x"} is a null string is easy to prove:

   630         *}

   631       case True

   632       with tag_xy have "y = []" 

   633         by (auto simp add: tag_str_STAR_def strict_prefix_def)

   634       thus ?thesis using xz_in_star True by simp

   635     next

   636         -- {* The nontrival case:

   637         *}

   638       case False

   639       -- {* 

   640         \begin{minipage}{0.8\textwidth}

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

   642         by a prefix @{text "xa"} together with its suffix @{text "x - xa"}, such

   643         that both @{text "xa"} and @{text "(x - xa) @ z"} are in @{text "L\<^isub>1\<star>"},

   644         and there could be many such splittings.Therefore, the following set @{text "?S"} 

   645         is nonempty, and finite as well:

   646         \end{minipage}

   647         *}

   648       let ?S = "{xa. xa < x \<and> xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>}"

   649       have "finite ?S"

   650         by (rule_tac B = "{xa. xa < x}" in finite_subset, 

   651           auto simp:finite_strict_prefix_set)

   652       moreover have "?S \<noteq> {}" using False xz_in_star

   653         by (simp, rule_tac x = "[]" in exI, auto simp:strict_prefix_def)

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

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

   656             \end{minipage}

   657           *}

   658       ultimately have "\<exists> xa_max \<in> ?S. \<forall> xa \<in> ?S. length xa \<le> length xa_max" 

   659         using finite_set_has_max by blast

   660       then obtain xa_max 

   661         where h1: "xa_max < x" 

   662         and h2: "xa_max \<in> L\<^isub>1\<star>" 

   663         and h3: "(x - xa_max) @ z \<in> L\<^isub>1\<star>" 

   664         and h4:"\<forall> xa < x. xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>  

   665                                      \<longrightarrow> length xa \<le> length xa_max"

   666         by blast

   667       -- {*

   668           \begin{minipage}{0.8\textwidth}

   669           By the equality of tags, the counterpart of @{text "xa_max"} among 

   670           @{text "y"}-prefixes, named @{text "ya"}, can be found:

   671           \end{minipage}

   672           *}

   673       obtain ya 

   674         where h5: "ya < y" and h6: "ya \<in> L\<^isub>1\<star>" 

   675         and eq_xya: "(x - xa_max) \<approx>L\<^isub>1 (y - ya)"

   676       proof-

   677         from tag_xy have "{\<approx>L\<^isub>1 `` {x - xa} |xa. xa < x \<and> xa \<in> L\<^isub>1\<star>} = 

   678           {\<approx>L\<^isub>1 `` {y - xa} |xa. xa < y \<and> xa \<in> L\<^isub>1\<star>}" (is "?left = ?right")

   679           by (auto simp:tag_str_STAR_def)

   680         moreover have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?left" using h1 h2 by auto

   681         ultimately have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?right" by simp

   682         thus ?thesis using that 

   683           apply (simp add:Image_def str_eq_rel_def str_eq_def) by blast

   684       qed 

   685       -- {*

   686           \begin{minipage}{0.8\textwidth}

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

   688           of the following proposition:

   689           \end{minipage}

   690           *}

   691       have "(y - ya) @ z \<in> L\<^isub>1\<star>" 

   692       proof-

   693         -- {* The idea is to split the suffix @{text "z"} into @{text "za"} and @{text "zb"}, 

   694           such that: *}

   695         obtain za zb where eq_zab: "z = za @ zb" 

   696           and l_za: "(y - ya)@za \<in> L\<^isub>1" and ls_zb: "zb \<in> L\<^isub>1\<star>"

   697         proof -

   698           -- {* 

   699             \begin{minipage}{0.8\textwidth}

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

   701             @{text "a"} and @{text "b"} such that:

   702             \end{minipage}

   703             *}

   704           from h1 have "(x - xa_max) @ z \<noteq> []" 

   705             by (auto simp:strict_prefix_def elim:prefixE)

   706           from star_decom [OF h3 this]

   707           obtain a b where a_in: "a \<in> L\<^isub>1" 

   708             and a_neq: "a \<noteq> []" and b_in: "b \<in> L\<^isub>1\<star>" 

   709             and ab_max: "(x - xa_max) @ z = a @ b" by blast

   710           -- {* Now the candiates for @{text "za"} and @{text "zb"} are found:*}

   711           let ?za = "a - (x - xa_max)" and ?zb = "b"

   712           have pfx: "(x - xa_max) \<le> a" (is "?P1") 

   713             and eq_z: "z = ?za @ ?zb" (is "?P2")

   714           proof -

   715             -- {* 

   716               \begin{minipage}{0.8\textwidth}

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

   718               can be splitted in two ways:

   719               \end{minipage}

   720               *}

   721             have "((x - xa_max) \<le> a \<and> (a - (x - xa_max)) @ b = z) \<or> 

   722               (a < (x - xa_max) \<and> ((x - xa_max) - a) @ z = b)" 

   723               using app_eq_dest[OF ab_max] by (auto simp:strict_prefix_def)

   724             moreover {

   725               -- {* However, the undsired way can be refuted by absurdity: *}

   726               assume np: "a < (x - xa_max)" 

   727                 and b_eqs: "((x - xa_max) - a) @ z = b"

   728               have "False"

   729               proof -

   730                 let ?xa_max' = "xa_max @ a"

   731                 have "?xa_max' < x" 

   732                   using np h1 by (clarsimp simp:strict_prefix_def diff_prefix) 

   733                 moreover have "?xa_max' \<in> L\<^isub>1\<star>" 

   734                   using a_in h2 by (simp add:star_intro3) 

   735                 moreover have "(x - ?xa_max') @ z \<in> L\<^isub>1\<star>" 

   736                   using b_eqs b_in np h1 by (simp add:diff_diff_appd)

   737                 moreover have "\<not> (length ?xa_max' \<le> length xa_max)" 

   738                   using a_neq by simp

   739                 ultimately show ?thesis using h4 by blast

   740               qed }

   741             -- {* Now it can be shown that the splitting goes the way we desired. *}

   742             ultimately show ?P1 and ?P2 by auto

   743           qed

   744           hence "(x - xa_max)@?za \<in> L\<^isub>1" using a_in by (auto elim:prefixE)

   745           -- {* Now candidates @{text "?za"} and @{text "?zb"} have all the requred properteis. *}

   746           with eq_xya have "(y - ya) @ ?za \<in> L\<^isub>1" 

   747             by (auto simp:str_eq_def str_eq_rel_def)

   748            with eq_z and b_in 

   749           show ?thesis using that by blast

   750         qed

   751         -- {* 

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

   753             *}

   754         have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" using  l_za ls_zb by blast

   755         with eq_zab show ?thesis by simp

   756       qed

   757       with h5 h6 show ?thesis 

   758         by (drule_tac star_intro1, auto simp:strict_prefix_def elim:prefixE)

   759     qed

   760   } 

   761   -- {* By instantiating the reasoning pattern just derived for both directions:*} 

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

   763   -- {* The thesis is proved as a trival consequence: *} 

   764     show  ?thesis unfolding str_eq_def str_eq_rel_def by blast

   765 qed

   766 

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

   768   fixes v w

   769   assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_STAR L\<^isub>1 w"

   770   shows "(v::string) \<approx>(L\<^isub>1\<star>) w"

   771 proof-

   772     -- {* 

   773     \begin{minipage}{0.8\textwidth}

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

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

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

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

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

   779     in the following:

   780     \end{minipage}

   781     *}

   782   { fix x y z

   783     assume xz_in_star: "x @ z \<in> L\<^isub>1\<star>" 

   784       and tag_xy: "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y"

   785     have "y @ z \<in> L\<^isub>1\<star>"

   786     proof(cases "x = []")

   787       -- {* 

   788         The degenerated case when @{text "x"} is a null string is easy to prove:

   789         *}

   790       case True

   791       with tag_xy have "y = []" 

   792         by (auto simp:tag_str_STAR_def strict_prefix_def)

   793       thus ?thesis using xz_in_star True by simp

   794     next

   795         -- {*

   796         \begin{minipage}{0.8\textwidth}

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

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

   799         \end{minipage}

   800         *}

   801       case False

   802       obtain x_max 

   803         where h1: "x_max < x" 

   804         and h2: "x_max \<in> L\<^isub>1\<star>" 

   805         and h3: "(x - x_max) @ z \<in> L\<^isub>1\<star>" 

   806         and h4:"\<forall> xa < x. xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star> 

   807                                      \<longrightarrow> length xa \<le> length x_max"

   808       proof-

   809         let ?S = "{xa. xa < x \<and> xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>}"

   810         have "finite ?S"

   811           by (rule_tac B = "{xa. xa < x}" in finite_subset, 

   812                                 auto simp:finite_strict_prefix_set)

   813         moreover have "?S \<noteq> {}" using False xz_in_star

   814           by (simp, rule_tac x = "[]" in exI, auto simp:strict_prefix_def)

   815         ultimately have "\<exists> max \<in> ?S. \<forall> a \<in> ?S. length a \<le> length max" 

   816           using finite_set_has_max by blast

   817         thus ?thesis using that by blast

   818       qed

   819       obtain ya 

   820         where h5: "ya < y" and h6: "ya \<in> L\<^isub>1\<star>" and h7: "(x - x_max) \<approx>L\<^isub>1 (y - ya)"

   821       proof-

   822         from tag_xy have "{\<approx>L\<^isub>1 `` {x - xa} |xa. xa < x \<and> xa \<in> L\<^isub>1\<star>} = 

   823           {\<approx>L\<^isub>1 `` {y - xa} |xa. xa < y \<and> xa \<in> L\<^isub>1\<star>}" (is "?left = ?right")

   824           by (auto simp:tag_str_STAR_def)

   825         moreover have "\<approx>L\<^isub>1 `` {x - x_max} \<in> ?left" using h1 h2 by auto

   826         ultimately have "\<approx>L\<^isub>1 `` {x - x_max} \<in> ?right" by simp

   827         with that show ?thesis apply 

   828           (simp add:Image_def str_eq_rel_def str_eq_def) by blast

   829       qed      

   830       have "(y - ya) @ z \<in> L\<^isub>1\<star>" 

   831       proof-

   832         from h3 h1 obtain a b where a_in: "a \<in> L\<^isub>1" 

   833           and a_neq: "a \<noteq> []" and b_in: "b \<in> L\<^isub>1\<star>" 

   834           and ab_max: "(x - x_max) @ z = a @ b" 

   835           by (drule_tac star_decom, auto simp:strict_prefix_def elim:prefixE)

   836         have "(x - x_max) \<le> a \<and> (a - (x - x_max)) @ b = z" 

   837         proof -

   838           have "((x - x_max) \<le> a \<and> (a - (x - x_max)) @ b = z) \<or> 

   839                             (a < (x - x_max) \<and> ((x - x_max) - a) @ z = b)" 

   840             using app_eq_dest[OF ab_max] by (auto simp:strict_prefix_def)

   841           moreover { 

   842             assume np: "a < (x - x_max)" and b_eqs: " ((x - x_max) - a) @ z = b"

   843             have "False"

   844             proof -

   845               let ?x_max' = "x_max @ a"

   846               have "?x_max' < x" 

   847                 using np h1 by (clarsimp simp:strict_prefix_def diff_prefix) 

   848               moreover have "?x_max' \<in> L\<^isub>1\<star>" 

   849                 using a_in h2 by (simp add:star_intro3) 

   850               moreover have "(x - ?x_max') @ z \<in> L\<^isub>1\<star>" 

   851                 using b_eqs b_in np h1 by (simp add:diff_diff_appd)

   852               moreover have "\<not> (length ?x_max' \<le> length x_max)" 

   853                 using a_neq by simp

   854               ultimately show ?thesis using h4 by blast

   855             qed 

   856           } ultimately show ?thesis by blast

   857         qed

   858         then obtain za where z_decom: "z = za @ b" 

   859           and x_za: "(x - x_max) @ za \<in> L\<^isub>1" 

   860           using a_in by (auto elim:prefixE)        

   861         from x_za h7 have "(y - ya) @ za \<in> L\<^isub>1" 

   862           by (auto simp:str_eq_def str_eq_rel_def)

   863 	with b_in have "((y - ya) @ za) @ b \<in> L\<^isub>1\<star>" by blast

   864         with z_decom show ?thesis by auto 

   865       qed

   866       with h5 h6 show ?thesis 

   867         by (drule_tac star_intro1, auto simp:strict_prefix_def elim:prefixE)

   868     qed

   869   } 

   870   -- {* By instantiating the reasoning pattern just derived for both directions:*} 

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

   872   -- {* The thesis is proved as a trival consequence: *} 

   873     show  ?thesis unfolding str_eq_def str_eq_rel_def by blast

   874 qed

   875 

   876 lemma quot_star_finiteI [intro]:

   877   fixes L1::"lang"

   878   assumes finite1: "finite (UNIV // \<approx>L1)"

   879   shows "finite (UNIV // \<approx>(L1\<star>))"

   880 proof (rule_tac tag = "tag_str_STAR L1" in tag_finite_imageD)

   881   show "\<And>x y. tag_str_STAR L1 x = tag_str_STAR L1 y \<Longrightarrow> x \<approx>(L1\<star>) y"

   882     by (rule tag_str_STAR_injI)

   883 next

   884   have *: "finite (Pow (UNIV // \<approx>L1))" 

   885     using finite1 by auto

   886   show "finite (range (tag_str_STAR L1))"

   887     unfolding tag_str_STAR_def

   888     apply(rule finite_subset[OF _ *])

   889     unfolding quotient_def

   890     by auto

   891 qed

   892 

   893 subsubsection{* The conclusion *}

   894 

   895 lemma rexp_imp_finite:

   896   fixes r::"rexp"

   897   shows "finite (UNIV // \<approx>(L r))"

   898 by (induct r) (auto)

   899 

   900 end