theory Myhill_2

  imports Myhill_1 Prefix_subtract

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

begin

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

definition 

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"

        by (simp) (blast)

      with X_in Y_in 

      have "X = Y"

    } 

    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

next

  show "equiv UNIV =tag="

    by auto

next

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

    by blast

qed

subsection {* The proof *}

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

lemma quot_zero_eq:

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

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

    thus ?thesis by simp

  next

    case False with h

    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 

    moreover 

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

    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

    } 

    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 

where

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

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

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

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

    using finite1 finite2 by auto

    by (rule rev_finite_subset) (auto)

next

    unfolding str_eq_def

    by auto

qed

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

definition 

where

  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)

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

proof -

  { fix x y z

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

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

          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'

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

          with pref_y' y'_in 

          show ?thesis using that by blast

        qed

      } 

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

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

        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" 

    qed

  }

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

qed 

next

    using fin1 fin2 by auto

    apply(rule finite_subset[OF _ *])

    unfolding quotient_def

    by auto

qed

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

definition 

where

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