theory Myhill_2

  imports Myhill_1 List_Prefix Prefix_subtract

begin

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

subsection {* The scheme*}

text {* 

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

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

  language @{text "A"}.

  *}

definition

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

where

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

text {*

  The main lemma (@{text "rexp_imp_finite"}) is proved by a structural

  induction over regular expressions.  where base cases (cases for @{const

  "NULL"}, @{const "EMPTY"}, @{const "CHAR"}) are quite straightforward to

  proof. Real difficulty lies in inductive cases.  By inductive hypothesis,

  languages defined by sub-expressions induce finite partitiions. Under such

  hypothsis, we need to prove that the language defined by the composite

  regular expression gives rise to finite partion.  The basic idea is to

  attach a tag @{text "tag(x)"} to every string @{text "x"}. The tagging

  fuction @{text "tag"} is carefully devised, which returns tags made of

  equivalent classes of the partitions induced by subexpressoins, and

  therefore has a finite range. Let @{text "Lang"} be the composite language,

  it is proved that:

  \begin{quote}

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

  \[

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

  \]

  then the partition induced by @{text "Lang"} must be finite.

  \end{quote}

  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"} (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 \<subseteq> R2"}),

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

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

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

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

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

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

  \end{enumerate}

*}

definition 

   tag_eq_rel :: "(string \<Rightarrow> 'b) \<Rightarrow> (string \<times> string) set" ("=_=")

where

   "=tag= \<equiv> {(x, y) | x y. tag x = tag y}"

lemma finite_eq_tag_rel:

  assumes rng_fnt: "finite (range tag)"

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

proof -

  let "?f" =  "\<lambda>X. tag ` X" and ?A = "(UNIV // =tag=)"

    -- {* The finiteness of @{text "f"}-image is a consequence of @{text "rng_fnt"} *}

  have "finite (?f ` ?A)" 

  proof -

    have "range ?f \<subseteq> (Pow (range tag))" unfolding Pow_def by auto

    moreover 

    have "finite (Pow (range tag))" using rng_fnt by simp

    ultimately 

    have "finite (range ?f)" unfolding image_def by (blast intro: finite_subset)

    moreover

    have "?f ` ?A \<subseteq> range ?f" by auto

    ultimately show "finite (?f ` ?A)" by (rule rev_finite_subset) 

  qed

  moreover

    -- {* The injectivity of @{text "f"}-image follows from the definition of @{text "(=tag=)"} *}

  have "inj_on ?f ?A"

  proof -

    { fix X Y

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

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

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

      then

      obtain x y 

        where "x \<in> X" "y \<in> Y" "tag x = tag y"

        unfolding quotient_def Image_def image_def tag_eq_rel_def

        by (simp) (blast)

      with X_in Y_in 

      have "X = Y"

	unfolding quotient_def tag_eq_rel_def by auto

    } then show "inj_on ?f ?A" unfolding inj_on_def by auto

  qed

  ultimately 

  show "finite (UNIV // =tag=)" by (rule finite_imageD)

qed

lemma refined_partition_finite:

  assumes fnt: "finite (UNIV // R1)"

  and refined: "R1 \<subseteq> R2"

  and eq1: "equiv UNIV R1" and eq2: "equiv UNIV R2"

  shows "finite (UNIV // R2)"

proof -

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

    and ?A = "UNIV // R2" and ?B = "UNIV // R1"

  have "?f ` ?A \<subseteq> Pow ?B"

    unfolding image_def Pow_def quotient_def by auto

  moreover

  have "finite (Pow ?B)" using fnt by simp

  ultimately  

  have "finite (?f ` ?A)" by (rule finite_subset)

  moreover

  have "inj_on ?f ?A"

  proof -

    { fix X Y

      assume X_in: "X \<in> ?A" and Y_in: "Y \<in> ?A" and eq_f: "?f X = ?f Y"

      from quotientE [OF X_in]

      obtain x where "X = R2 `` {x}" by blast

      with equiv_class_self[OF eq2] have x_in: "x \<in> X" by simp

      then have "R1 ``{x} \<in> ?f X" by auto

      with eq_f have "R1 `` {x} \<in> ?f Y" by simp

      then obtain y 

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

      with eq_equiv_class[OF _ eq1] 

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

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

      with quotient_eqI [OF eq2 X_in Y_in x_in y_in]

      have "X = Y" .

    } 

    then show "inj_on ?f ?A" unfolding inj_on_def by blast 

  qed

  ultimately show "finite (UNIV // R2)" by (rule finite_imageD)

qed

lemma tag_finite_imageD:

  assumes rng_fnt: "finite (range tag)" 

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

  shows "finite (UNIV // \<approx>A)"

proof (rule_tac refined_partition_finite [of "=tag="])

  show "finite (UNIV // =tag=)" by (rule finite_eq_tag_rel[OF rng_fnt])

next

  from same_tag_eqvt

  show "=tag= \<subseteq> \<approx>A" unfolding tag_eq_rel_def str_eq_def

    by auto

next

  show "equiv UNIV =tag="

    unfolding equiv_def tag_eq_rel_def refl_on_def sym_def trans_def

    by auto

next

  show "equiv UNIV (\<approx>A)" 

    unfolding equiv_def str_eq_rel_def sym_def refl_on_def trans_def

    by blast

qed

subsection {* The proof*}

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) \<Longrightarrow> x \<approx>Lang y"}

  \]

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

  \[

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

  \]

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

  it is suffcient to show just one direction:

  \[

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

  \]

  This is the pattern followed by every inductive case.

  *}

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

lemma quot_null_eq:

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

  unfolding quotient_def Image_def str_eq_rel_def by auto

lemma quot_null_finiteI [intro]:

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

unfolding quot_null_eq by simp

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

lemma quot_empty_subset:

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

proof

  fix x

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

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

    unfolding quotient_def Image_def by blast

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

  proof (cases "y = []")

    case True with h

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

    thus ?thesis by simp

  next

    case False with h

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

    thus ?thesis by simp

  qed

qed

lemma quot_empty_finiteI [intro]:

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

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

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

lemma quot_char_subset:

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

proof 

  fix x 

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

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

    unfolding quotient_def Image_def by blast

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

  proof -

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

        by (auto simp:str_eq_rel_def)

    } moreover {

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

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

    } moreover {

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

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

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

        by (case_tac p, auto)

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

        by (auto simp add:str_eq_rel_def)

    } ultimately show ?thesis by blast

  qed

qed

lemma quot_char_finiteI [intro]:

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

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

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

definition 

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

where

  "tag_str_ALT A B \<equiv> (\<lambda>x. (\<approx>A `` {x}, \<approx>B `` {x}))"

lemma quot_union_finiteI [intro]:

  fixes L1 L2::"lang"

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

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

  shows "finite (UNIV // \<approx>(A \<union> B))"

proof (rule_tac tag = "tag_str_ALT A B" in tag_finite_imageD)

  have "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))" 

    using finite1 finite2 by auto

  then show "finite (range (tag_str_ALT A B))"

    unfolding tag_str_ALT_def quotient_def

    by (rule rev_finite_subset) (auto)

next

  show "\<And>x y. tag_str_ALT A B x = tag_str_ALT A B y \<Longrightarrow> x \<approx>(A \<union> B) y"

    unfolding tag_str_ALT_def

    unfolding str_eq_def

    unfolding str_eq_rel_def

    by auto

qed

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 \<in> 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 \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)"

where

  "tag_str_SEQ L1 L2 \<equiv>

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

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

lemma append_seq_elim:

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

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

          (\<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> 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 \<in> L\<^isub>1 \<and> s\<^isub>2 \<in> L\<^isub>2" 

    by (auto simp:Seq_def)

  from app_eq_dest [OF eq_xys]

  have

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

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

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

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

  moreover have "?Split2 \<Longrightarrow> \<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> 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 \<approx>(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 \<in> 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 \<in> 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 "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ z \<in> L\<^isub>2) \<or> 

               (\<exists> za \<le> z. (x @ za) \<in> L\<^isub>1 \<and> (z - za) \<in> 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 \<le> x" and h2: "xa \<in> L\<^isub>1" and h3: "(x - xa) @ z \<in> L\<^isub>2"

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

        obtain ya 

          where "ya \<le> y" 

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

          and "(y - ya) @ z \<in> 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 "{\<approx>L\<^isub>2 `` {x - xa} |xa. xa \<le> x \<and> xa \<in> L\<^isub>1} = 

                   {\<approx>L\<^isub>2 `` {y - ya} |ya. ya \<le> y \<and> ya \<in> 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 "\<approx>L\<^isub>2 `` {x - xa} \<in> ?Left" using h1 h2 by auto

            -- {* 

            \begin{minipage}{0.7\textwidth}

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

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

            \end{minipage}

            *}

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

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

          then obtain ya 

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

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

            by simp blast

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

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

          proof -

            from eq_xya have "(x - xa)  \<approx>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 that by blast

        qed

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

        hence "y @ z \<in> 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 \<le> z" and h2: "(x @ za) \<in> L\<^isub>1" and h3: "z - za \<in> L\<^isub>2"

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

        proof-

          have "\<approx>L\<^isub>1 `` {x} = \<approx>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 \<in> 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 // \<approx>L1)" 

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

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

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

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

    by (rule tag_str_SEQ_injI)

next

  have *: "finite ((UNIV // \<approx>L1) \<times> (Pow (UNIV // \<approx>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 

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

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

  \begin{enumerate}

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

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

          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}.

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

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

          Such a split always exists because:

          \begin{enumerate}

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

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

              as shown in Fig. \ref{ab_split}.

            \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}. The detailed steps are:

          \begin{enumerate}

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

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

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

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

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

          \end{enumerate}

  \end{enumerate}

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

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

  \ref{ansfer_step} feasible.

  \input{fig_star}

*} 

definition 

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

where

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

text {* A technical lemma. *}

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

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

proof (induct rule:finite.induct)

  case emptyI thus ?case by simp

next

  case (insertI A a)

  show ?case

  proof (cases "A = {}")

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

  next

    case False

    with insertI.hyps and False  

    obtain max 

      where h1: "max \<in> A" 

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

    show ?thesis

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

      assume "f a \<le> f max"

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

    next

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

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

    qed

  qed

qed

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} \<union> {xs}")