theory Myhill_2

begin

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

definition 

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

where

   "=tag= \<equiv> {(x, y). tag x = tag y}"

abbreviation

   tag_eq_applied :: "'a list \<Rightarrow> ('a list \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> bool" ("_ =_= _")

where

   "x =tag= y \<equiv> (x, y) \<in> =tag="

lemma test:

  shows "(\<approx>A) `` {x} = (\<approx>A) `` {y} \<longleftrightarrow> x \<approx>A y"

unfolding str_eq_def

by auto

lemma test_refined_intro:

  assumes "\<And>x y z. \<lbrakk>x =tag= y; x @ z \<in> A\<rbrakk> \<Longrightarrow> y @ z \<in> A"

  shows "=tag= \<subseteq> \<approx>A"

using assms

unfolding str_eq_def tag_eq_def

apply(clarify, simp (no_asm_use))

by metis

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_def

        by (simp) (blast)

      with X_in Y_in 

      have "X = Y"

	unfolding quotient_def tag_eq_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_def str_eq_def

    by blast

next

  show "equiv UNIV =tag="

    unfolding equiv_def tag_eq_def refl_on_def sym_def trans_def

    by auto

next

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

    unfolding equiv_def str_eq_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_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_def)

    thus ?thesis by simp

  next

    case False with h

    have "x = UNIV - {[]}" by (auto simp: str_eq_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_def) } 

    moreover 

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

        by (auto dest!: spec[where x = "[]"] simp: str_eq_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_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_Plus :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang)"

where

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

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

    unfolding tag_Plus_def quotient_def

    by (rule rev_finite_subset) (auto)

next

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

    unfolding tag_Plus_def

    unfolding str_eq_def

    by auto

qed

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

definition

  "Partitions s \<equiv> {(u, v). u @ v = s}"

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

  shows "\<exists>(u, v) \<in> Partitions x. u \<in> A \<and> v \<in> B"

using assms

unfolding conc_def Partitions_def

by auto

  assumes "(u, v) \<in> Partitions x \<and> u \<in> A \<and>  v \<in> B"

  shows "x \<in> A \<cdot> B"

using assms

unfolding conc_def Partitions_def

by auto

done

where

definition 

where

  and     c: "x @ z \<in> A \<cdot> B"

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

proof -

  from c obtain u v where 

    h1: "(u, v) \<in> Partitions (x @ z)" and

    h2: "u \<in> A" and

  from h1 have "x @ z = u @ v" unfolding Partitions_def by simp

  then obtain us 

    where "(x = u @ us \<and> us @ z = v) \<or> (x @ us = u \<and> z = us @ v)"

    by (auto simp add: append_eq_append_conv2)

  moreover

  { assume eq: "x = u @ us" "us @ z = v"

      using b by simp

    then obtain u' us' where

      q1: "\<approx>A `` {u} = \<approx>A `` {u'}" and

      q2: "\<approx>B `` {us} = \<approx>B `` {us'}" and

    from q1 h2 have "u' \<in> A" 

    moreover from q2 h3 eq 

    have "us' @ z \<in> B"

      unfolding Image_def str_eq_def by auto

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

      unfolding Partitions_def by auto

  }

  moreover

  { assume eq: "x @ us = u" "z = us @ v"

      using a by simp

    moreover 

    have "x @ us \<in> A" using h2 eq by simp

    ultimately 

      unfolding Image_def str_eq_def by blast

    then have "(y @ us) @ v \<in> A \<cdot> B" 

      using h3 unfolding conc_def by blast

    then have "y @ z \<in> A \<cdot> B" using eq by simp 

  }

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

qed

lemma quot_conc_finiteI [intro]:

  fixes A B::"'a lang"

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

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

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

proof (rule_tac tag = "tag_Times A B" in tag_finite_imageD)

next

    using fin1 fin2 by auto

  show "finite (range (tag_Times A B))" 

    unfolding tag_Times_def

    apply(rule finite_subset[OF _ *])

    unfolding quotient_def

    by auto

qed

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

using assms

qed

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_Star_injI: