theory Myhill

  imports Myhill_1

begin

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

subsection {* The scheme for this direction *}

text {* 

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

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

  language @{text "Lang"}.

  *}

definition

where

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

text {*

  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_range_image: "finite (range f) \<Longrightarrow> finite (f ` A)"

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

lemma finite_eq_f_rel:

  assumes rng_fnt: "finite (range tag)"

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

proof -

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

  show ?thesis

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

    -- {* 

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

      *}

    show "finite (?f ` ?A)" 

    proof -

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

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

      ultimately have "finite (range ?f)"

        by (auto simp only:image_def intro:finite_subset)

      from finite_range_image [OF this] show ?thesis .

    qed

  next

    -- {* 

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

      *}

    show "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"

        have "X = Y"

        proof -

          from X_in Y_in tag_eq 

          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

            apply simp by blast

          with X_in Y_in show ?thesis 

            by (auto simp:quotient_def str_eq_rel_def str_eq_def f_eq_rel_def) 

        qed

      } thus ?thesis unfolding inj_on_def by auto

    qed

  qed

qed

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

lemma tag_finite_imageD:

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

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

proof -

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

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

  show ?thesis

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

    -- {* 

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

      *}

    show "finite (?f ` ?A)" 

    proof -

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

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

      ultimately have "finite (range ?f)"

        by (auto simp only:image_def intro:finite_subset)

      from finite_range_image [OF this] show ?thesis .

    qed

  next

    -- {* 

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

      *}

    show "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"

        have "X = Y"

        proof -

          from X_in Y_in tag_eq 

          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

            apply simp by blast 

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

          with X_in Y_in x_in y_in

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

        qed

      } thus ?thesis unfolding inj_on_def by auto

    qed

  qed

qed

subsection {* Lemmas for basic cases *}

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

  proof (cases "y = []")

    case True with h

    thus ?thesis by simp

  next

    case False with h

    thus ?thesis by simp

  qed

qed

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

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

definition 

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

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

    using app_eq_dest by auto

  moreover have "\<lbrakk>x \<le> s\<^isub>1; (s\<^isub>1 - x) @ s\<^isub>2 = y\<rbrakk> \<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 "\<lbrakk>s\<^isub>1 \<le> x; (x - s\<^isub>1) @ y = s\<^isub>2\<rbrakk> \<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:

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

proof-

  { 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-

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

        using xz_in_seq append_seq_elim by simp

      moreover {

        fix xa

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

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

        proof -

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

          proof -

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

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

                          (is "?Left = ?Right") 

              using h1 tag_xy by (auto simp:tag_str_SEQ_def)

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

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

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

          qed

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

        qed

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

      } moreover {

        fix za

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

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

        proof-

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

            using h1 tag_xy by (auto simp:tag_str_SEQ_def)

          with h2 show ?thesis 

            by (auto simp:Image_def str_eq_rel_def str_eq_def) 

        qed

        with h1 h3 have "y @ z \<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

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

    by (auto simp add: str_eq_def str_eq_rel_def)

qed 

definition 

next

qed

text {* 

  This turned out to be the trickiest case. 

  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.

definition 

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 prems 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 {* Technical lemma. *}

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