theory Myhill_2

  imports Myhill_1 Prefix_subtract

          "~~/src/HOL/Library/List_Prefix"

begin

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

definition

  str_eq :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<approx>_ _")

where

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

lemma str_eq_def2:

  shows "\<approx>A = {(x, y) | x y. x \<approx>A y}"

unfolding str_eq_def

by simp

definition 

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

where

   "=tag= \<equiv> {(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=)"

  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

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

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

lemma quot_zero_eq:

  shows "UNIV // \<approx>{} = {UNIV}"

unfolding quotient_def Image_def str_eq_rel_def by auto

lemma quot_zero_finiteI [intro]:

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

unfolding quot_zero_eq by simp

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

lemma quot_one_subset:

  shows "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_one_finiteI [intro]:

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

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

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

lemma quot_atom_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_atom_finiteI [intro]:

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

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

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

definition 

  tag_str_Plus :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang)"

where

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

lemma quot_union_finiteI [intro]:

  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_Plus 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_Plus A B))"

    unfolding tag_str_Plus_def quotient_def

    by (rule rev_finite_subset) (auto)

next

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

    unfolding tag_str_Plus_def

    unfolding str_eq_def

    unfolding str_eq_rel_def

    by auto

qed

subsubsection {* The inductive case for @{text "Times"}*}

definition 

  tag_str_Times :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang set)"

where

  "tag_str_Times L1 L2 \<equiv>

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

lemma Seq_in_cases:

  assumes "x @ z \<in> A \<cdot> B"

  shows "(\<exists> x' \<le> x. x' \<in> A \<and> (x - x') @ z \<in> B) \<or> 

         (\<exists> z' \<le> z. (x @ z') \<in> A \<and> (z - z') \<in> B)"

using assms

unfolding conc_def prefix_def

by (auto simp add: append_eq_append_conv2)

lemma tag_str_Times_injI:

  assumes eq_tag: "tag_str_Times A B x = tag_str_Times A B y" 

  shows "x \<approx>(A \<cdot> B) y"

proof -

  { fix x y z

    assume xz_in_seq: "x @ z \<in> A \<cdot> B"

    and tag_xy: "tag_str_Times A B x = tag_str_Times A B y"

    have"y @ z \<in> A \<cdot> B" 

    proof -

      { (* first case with x' in A and (x - x') @ z in B *)

        fix x'

        assume h1: "x' \<le> x" and h2: "x' \<in> A" and h3: "(x - x') @ z \<in> B"

        obtain y' 

          where "y' \<le> y" 

          and "y' \<in> A" 

          and "(y - y') @ z \<in> B"

        proof -

          have "{\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A} = 

                {\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A}" (is "?Left = ?Right")

            using tag_xy unfolding tag_str_Times_def by simp

          moreover 

	  have "\<approx>B `` {x - x'} \<in> ?Left" using h1 h2 by auto

          ultimately 

	  have "\<approx>B `` {x - x'} \<in> ?Right" by simp

          then obtain y' 

            where eq_xy': "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}" 

            and pref_y': "y' \<le> y" and y'_in: "y' \<in> A"

            by simp blast

	  have "(x - x')  \<approx>B (y - y')" using eq_xy'

            unfolding Image_def str_eq_rel_def str_eq_def by auto

          with h3 have "(y - y') @ z \<in> B" 

	    unfolding str_eq_rel_def str_eq_def by simp

          with pref_y' y'_in 

          show ?thesis using that by blast

        qed

	then have "y @ z \<in> A \<cdot> B" by (erule_tac prefixE) (auto simp: Seq_def)

      } 

      moreover 

      { (* second case with x @ z' in A and z - z' in B *)

        fix z'

        assume h1: "z' \<le> z" and h2: "(x @ z') \<in> A" and h3: "z - z' \<in> B"

	 have "\<approx>A `` {x} = \<approx>A `` {y}" 

           using tag_xy unfolding tag_str_Times_def by simp

         with h2 have "y @ z' \<in> A"

            unfolding Image_def str_eq_rel_def str_eq_def by auto

        with h1 h3 have "y @ z \<in> A \<cdot> B"

	  unfolding prefix_def conc_def

	  by (auto) (metis append_assoc)

      }

      ultimately show "y @ z \<in> A \<cdot> B" 

	using Seq_in_cases [OF xz_in_seq] by blast

    qed

  }

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

    show "x \<approx>(A \<cdot> B) y" unfolding str_eq_def str_eq_rel_def by blast

qed 

lemma quot_seq_finiteI [intro]:

  fixes L1 L2::"'a lang"

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

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

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

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

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

    by (rule tag_str_Times_injI)

next

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

    using fin1 fin2 by auto

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

    unfolding tag_str_Times_def

    apply(rule finite_subset[OF _ *])

    unfolding quotient_def

    by auto

qed

subsubsection {* The inductive case for @{const "Star"} *}

definition 

  tag_str_Star :: "'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang) set"

where

  "tag_str_Star L1 \<equiv> (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<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: 

  shows "finite {xa. xa < (x::'a list)}"

apply (induct x rule:rev_induct, simp)

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

by (auto simp:strict_prefix_def)

lemma tag_str_Star_injI:

  fixes L\<^isub>1::"('a::finite) lang"

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

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

proof-

  { fix x y z

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

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

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

    proof(cases "x = []")

      case True

      with tag_xy have "y = []" 

        by (auto simp add: tag_str_Star_def strict_prefix_def)

      thus ?thesis using xz_in_star True by simp

    next

      case False

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

      have "finite ?S"

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

	   (auto simp: finite_strict_prefix_set)

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

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

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

        using finite_set_has_max by blast

      then obtain xa_max 

        where h1: "xa_max < x" 

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

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

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

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

        by blast

      obtain ya 

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

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

      proof-

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

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

          by (auto simp:tag_str_Star_def)

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

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

        thus ?thesis using that 

          apply (simp add:Image_def str_eq_rel_def str_eq_def) by blast

      qed 

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

      proof-

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

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

        proof -

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

            by (auto simp:strict_prefix_def elim:prefixE)

          from star_decom [OF h3 this]

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

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

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

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

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

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

          proof -

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

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

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

            moreover {

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

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

              have "False"

              proof -

                let ?xa_max' = "xa_max @ a"

                have "?xa_max' < x" 

                  using np h1 by (clarsimp simp:strict_prefix_def diff_prefix) 

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

                  using a_in h2 by (auto)

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

                  using b_eqs b_in np h1 by (simp add:diff_diff_append)

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

                  using a_neq by simp

                ultimately show ?thesis using h4 by blast

              qed }

            ultimately show ?P1 and ?P2 by auto

          qed

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

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

            by (auto simp:str_eq_def str_eq_rel_def)

           with eq_z and b_in 

          show ?thesis using that by blast

        qed

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

	  by (rule_tac append_in_starI) (auto)

        with eq_zab show ?thesis by simp

      qed

      with h5 h6 show ?thesis 	

        by (auto simp:strict_prefix_def elim: prefixE)

    qed

  } 

  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_star_finiteI [intro]:

   fixes A::"('a::finite) lang"

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

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

proof (rule_tac tag = "tag_str_Star A" in tag_finite_imageD)

  show "\<And>x y. tag_str_Star A x = tag_str_Star A y \<Longrightarrow> x \<approx>(A\<star>) y"

    by (rule tag_str_Star_injI)

next

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

    using finite1 by auto

  show "finite (range (tag_str_Star A))"

    unfolding tag_str_Star_def

    apply(rule finite_subset[OF _ *])

    unfolding quotient_def

    by auto

qed

subsubsection{* The conclusion *}

lemma Myhill_Nerode2:

  fixes r::"('a::finite) rexp"

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

by (induct r) (auto)

theorem Myhill_Nerode:

  fixes A::"('a::finite) lang"

  shows "(\<exists>r. A = lang r) \<longleftrightarrow> finite (UNIV // \<approx>A)"

using Myhill_Nerode1 Myhill_Nerode2 by auto

end