theory Myhill

  imports Myhill_1

begin

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

subsection {* The scheme*}

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

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

where

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

text {*

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

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

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

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

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

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

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

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

   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"

        unfolding image_def Pow_def quotient_def

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

            unfolding equiv_def quotient_def refl_on_def by 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" 

              unfolding equiv_def quotient_def refl_on_def by 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)"

  unfolding 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 {* 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 L1 L2 = (\<lambda>x. (\<approx>L1 `` {x}, \<approx>L2 `` {x}))"

lemma quot_union_finiteI [intro]:

  fixes L1 L2::"lang"

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

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

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

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

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

    unfolding tag_str_ALT_def 

    unfolding str_eq_def

    unfolding Image_def 

    unfolding str_eq_rel_def

    by auto

next

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

    using finite1 finite2 by auto

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

    unfolding tag_str_ALT_def

    apply(rule finite_subset[OF _ *])

    unfolding quotient_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 = 

     (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa.  xa \<le> x \<and> xa \<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 prems 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 {