str_eq ("_ \<approx>_ _")

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

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

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

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

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

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

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

  \begin{enumerate}

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

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

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

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

    \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 

   f_eq_rel ("=_=")

where

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

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

  by (auto simp:equiv_def f_eq_rel_def refl_on_def sym_def trans_def)

lemma finite_eq_f_rel:

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

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

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

          obtain x y 

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

            unfolding quotient_def Image_def str_eq_rel_def 

                                   str_eq_def image_def f_eq_rel_def

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

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

lemma refined_partition_finite:

  fixes R1 R2 A

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

  and refined: "R1 \<subseteq> R2"

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

  shows "finite (A // R2)"

proof -

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

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

  show ?thesis

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

    show "finite (?f ` ?A)"

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

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

    next

      from eq2

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

        apply (unfold image_def Pow_def quotient_def, auto)

        by (rule_tac x = xb in bexI, simp, 

                 unfold equiv_def sym_def refl_on_def, blast)

    qed

  next

    show "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" (is "?L = ?R")

        have "X = Y" using X_in

        proof(rule quotientE)

          fix x

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

          have x_in: "x \<in> X" 

            by (unfold equiv_def quotient_def refl_on_def, auto)

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

          then obtain y where 

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

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

          proof -

            from x_in X_in y_in Y_in eq2

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

              by (unfold equiv_def quotient_def refl_on_def, auto)

            from eq_equiv_class_iff [OF eq1 this] and eq_r

            show ?thesis by simp

          qed

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

          from quotient_eqI [OF eq2 X_in Y_in x_in y_in this]

          show ?thesis .

        qed

      } thus ?thesis by (auto simp:inj_on_def)

    qed

  qed

qed

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

  apply (unfold equiv_def str_eq_rel_def sym_def refl_on_def trans_def)

  by blast

  fixes tag

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

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

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

proof -

  let ?R1 = "(=tag=)"

  show ?thesis

  proof(rule_tac refined_partition_finite [of _ ?R1])

    from finite_eq_f_rel [OF rng_fnt]

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

   next

     from same_tag_eqvt

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

       by (auto simp:f_eq_rel_def str_eq_def)

   next

     from equiv_f_eq_rel

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

   next

     from equiv_lang_eq

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

  qed

qed

text {*

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

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

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

  \[

  @{thm "finite_imageD" [no_vars]}

  \]

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

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

  *}

lemma 

  fixes tag

  assumes rng_fnt: "finite (range tag)" 

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

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

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

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

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

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

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

  The the final result of this direction is in @{text "easier_direction"}, which

  is an induction on the structure of regular expressions. There is one case 

  for each regular expression operator. For basic operators such as @{text "NULL, EMPTY, CHAR c"},

  the finiteness of their language partition can be established directly with no need

  of taggiing. This section contains several technical lemma for these base cases.

  The inductive cases involve operators @{text "ALT, SEQ"} and @{text "STAR"}. 

  Tagging functions need to be defined individually for each of them. There will be one

  dedicated section for each of these cases, and each section goes virtually the same way:

  gives definition of the tagging function and prove that strings 

  with the same tag are equivalent.

  *}

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

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

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

subsection {* The case for @{text "SEQ"}*}

  "tag_str_SEQ L\<^isub>1 L\<^isub>2 x \<equiv> 

       ((\<approx>L\<^isub>1) `` {x}, {(\<approx>L\<^isub>2) `` {x - xa}| xa.  xa \<le> x \<and> xa \<in> L\<^isub>1})"

lemma tag_str_seq_range_finite:

  "\<lbrakk>finite (UNIV // \<approx>L\<^isub>1); finite (UNIV // \<approx>L\<^isub>2)\<rbrakk> 

                              \<Longrightarrow> finite (range (tag_str_SEQ L\<^isub>1 L\<^isub>2))"

apply (rule_tac B = "(UNIV // \<approx>L\<^isub>1) \<times> (Pow (UNIV // \<approx>L\<^isub>2))" in finite_subset)

by (auto simp:tag_str_SEQ_def Image_def quotient_def split:if_splits)

qed 

lemma quot_seq_finiteI:

  "\<lbrakk>finite (UNIV // \<approx>L\<^isub>1); finite (UNIV // \<approx>L\<^isub>2)\<rbrakk> 

  \<Longrightarrow> finite (UNIV // \<approx>(L\<^isub>1 ;; L\<^isub>2))"

  apply (rule_tac tag = "tag_str_SEQ L\<^isub>1 L\<^isub>2" in tag_finite_imageD)  

  by (auto intro:tag_str_SEQ_injI elim:tag_str_seq_range_finite)

subsection {* The case for @{text "ALT"} *}

  "tag_str_ALT L\<^isub>1 L\<^isub>2 (x::string) \<equiv> ((\<approx>L\<^isub>1) `` {x}, (\<approx>L\<^isub>2) `` {x})"

lemma quot_union_finiteI:

  assumes finite1: "finite (UNIV // \<approx>(L\<^isub>1::string set))"

  and finite2: "finite (UNIV // \<approx>L\<^isub>2)"

  shows "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))"

proof (rule_tac tag = "tag_str_ALT L\<^isub>1 L\<^isub>2" in tag_finite_imageD)

  show "\<And>m n. tag_str_ALT L\<^isub>1 L\<^isub>2 m = tag_str_ALT L\<^isub>1 L\<^isub>2 n \<Longrightarrow> m \<approx>(L\<^isub>1 \<union> L\<^isub>2) n"

    unfolding tag_str_ALT_def str_eq_def Image_def str_eq_rel_def by auto

  show "finite (range (tag_str_ALT L\<^isub>1 L\<^isub>2))" using finite1 finite2

    apply (rule_tac B = "(UNIV // \<approx>L\<^isub>1) \<times> (UNIV // \<approx>L\<^isub>2)" in finite_subset)

    by (auto simp:tag_str_ALT_def Image_def quotient_def)

subsection {*

  The case for @{text "STAR"}

  *}

  Any string @{text "x"} in language @{text "L\<^isub>1\<star>"}, 

  can be splited into a prefix @{text "xa \<in> L\<^isub>1\<star>"} and a suffix @{text "x - xa \<in> L\<^isub>1"}.

  For one such @{text "x"}, there can be many such splits. The tagging of @{text "x"} is then 

  defined by collecting the @{text "L\<^isub>1"}-state of the suffixes from every possible split.

  *} 

(* I will make some illustrations for it. *)

  "tag_str_STAR L\<^isub>1 x \<equiv> {(\<approx>L\<^isub>1) `` {x - xa} | xa. xa < x \<and> xa \<in> L\<^isub>1\<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))"

text {* Technical lemma. *}

text {* 

  The following lemma @{text "tag_str_star_range_finite"} establishes the range finiteness 

  of the tagging function.

  *}

lemma tag_str_star_range_finite:

  "finite (UNIV // \<approx>L\<^isub>1) \<Longrightarrow> finite (range (tag_str_STAR L\<^isub>1))"

apply (rule_tac B = "Pow (UNIV // \<approx>L\<^isub>1)" in finite_subset)

by (auto simp:tag_str_STAR_def Image_def 

                       quotient_def split:if_splits)

text {*

  The following lemma @{text "tag_str_STAR_injI"} establishes the injectivity of 

  the tagging function for case @{text "STAR"}.

  *}

  fixes v w

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

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

    -- {* 

    \begin{minipage}{0.9\textwidth}

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

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

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

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

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

    in the following:

    \end{minipage}

    *}