Theory Myhill_2

(* Author: Xingyuan Zhang, Chunhan Wu, Christian Urban *)
theory Myhill_2
  imports Myhill_1 "HOL-Library.Sublist"
begin

section ‹Second direction of MN: ‹regular language ⇒ finite partition››

subsection ‹Tagging functions›

definition 
   tag_eq :: "('a list ⇒ 'b) ⇒ ('a list × 'a list) set" ("=_=")
where
   "=tag= ≡ {(x, y). tag x = tag y}"

abbreviation
   tag_eq_applied :: "'a list ⇒ ('a list ⇒ 'b) ⇒ 'a list ⇒ bool" ("_ =_= _")
where
   "x =tag= y ≡ (x, y) ∈ =tag="

lemma [simp]:
  shows "(≈A) `` {x} = (≈A) `` {y} ⟷ x ≈A y"
unfolding str_eq_def by auto

lemma refined_intro:
  assumes "⋀x y z. ⟦x =tag= y; x @ z ∈ A⟧ ⟹ y @ z ∈ A"
  shows "=tag= ⊆ ≈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" =  "λX. tag ` X" and ?A = "(UNIV // =tag=)"
  have "finite (?f ` ?A)" 
  proof -
    have "range ?f ⊆ (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 ⊆ 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 ∈ ?A"
        and  Y_in: "Y ∈ ?A"
        and  tag_eq: "?f X = ?f Y"
      then obtain x y 
        where "x ∈ X" "y ∈ 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 ⊆ R2"
  and eq1: "equiv UNIV R1" and eq2: "equiv UNIV R2"
  shows "finite (UNIV // R2)"
proof -
  let ?f = "λX. {R1 `` {x} | x. x ∈ X}" 
    and ?A = "UNIV // R2" and ?B = "UNIV // R1"
  have "?f ` ?A ⊆ 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 ∈ ?A" and Y_in: "Y ∈ ?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 ∈ X" by simp
      then have "R1 ``{x} ∈ ?f X" by auto
      with eq_f have "R1 `` {x} ∈ ?f Y" by simp
      then obtain y 
        where y_in: "y ∈ Y" and eq_r1_xy: "R1 `` {x} = R1 `` {y}" by auto
      with eq_equiv_class[OF _ eq1] 
      have "(x, y) ∈ R1" by blast
      with refined have "(x, y) ∈ 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     refined: "=tag=  ⊆ ≈A"
  shows "finite (UNIV // ≈A)"
proof (rule_tac refined_partition_finite [of "=tag="])
  show "finite (UNIV // =tag=)" by (rule finite_eq_tag_rel[OF rng_fnt])
next
  show "=tag= ⊆ ≈A" using refined .
next
  show "equiv UNIV =tag="
  and  "equiv UNIV (≈A)" 
    unfolding equiv_def str_eq_def tag_eq_def refl_on_def sym_def trans_def
    by auto
qed


subsection ‹Base cases: @{const Zero}, @{const One} and @{const Atom}›

lemma quot_zero_eq:
  shows "UNIV // ≈{} = {UNIV}"
unfolding quotient_def Image_def str_eq_def by auto

lemma quot_zero_finiteI [intro]:
  shows "finite (UNIV // ≈{})"
unfolding quot_zero_eq by simp


lemma quot_one_subset:
  shows "UNIV // ≈{[]} ⊆ {{[]}, UNIV - {[]}}"
proof
  fix x
  assume "x ∈ UNIV // ≈{[]}"
  then obtain y where h: "x = {z. y ≈{[]} z}" 
    unfolding quotient_def Image_def by blast
  { assume "y = []"
    with h have "x = {[]}" by (auto simp: str_eq_def)
    then have "x ∈ {{[]}, UNIV - {[]}}" by simp }
  moreover
  { assume "y ≠ []"
    with h have "x = UNIV - {[]}" by (auto simp: str_eq_def)
    then have "x ∈ {{[]}, UNIV - {[]}}" by simp }
  ultimately show "x ∈ {{[]}, UNIV - {[]}}" by blast
qed

lemma quot_one_finiteI [intro]:
  shows "finite (UNIV // ≈{[]})"
by (rule finite_subset[OF quot_one_subset]) (simp)


lemma quot_atom_subset:
  "UNIV // (≈{[c]}) ⊆ {{[]},{[c]}, UNIV - {[], [c]}}"
proof 
  fix x 
  assume "x ∈ UNIV // ≈{[c]}"
  then obtain y where h: "x = {z. (y, z) ∈ ≈{[c]}}" 
    unfolding quotient_def Image_def by blast
  show "x ∈ {{[]},{[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 ≠ []" and "y ≠ [c]"
      hence "∀ z. (y @ z) ≠ [c]" by (case_tac y, auto)
      moreover have "⋀ p. (p ≠ [] ∧ p ≠ [c]) = (∀ q. p @ q ≠ [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 // ≈{[c]})"
by (rule finite_subset[OF quot_atom_subset]) (simp)


subsection ‹Case for @{const Plus}›

definition 
  tag_Plus :: "'a lang ⇒ 'a lang ⇒ 'a list ⇒ ('a lang × 'a lang)"
where
  "tag_Plus A B ≡ λx. (≈A `` {x}, ≈B `` {x})"

lemma quot_plus_finiteI [intro]:
  assumes finite1: "finite (UNIV // ≈A)"
  and     finite2: "finite (UNIV // ≈B)"
  shows "finite (UNIV // ≈(A ∪ B))"
proof (rule_tac tag = "tag_Plus A B" in tag_finite_imageD)
  have "finite ((UNIV // ≈A) × (UNIV // ≈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 "=tag_Plus A B= ⊆ ≈(A ∪ B)"
    unfolding tag_eq_def tag_Plus_def str_eq_def by auto
qed


subsection ‹Case for ‹Times››

definition
  "Partitions x ≡ {(x⇩p, x⇩s). x⇩p @ x⇩s = x}"

lemma conc_partitions_elim:
  assumes "x ∈ A ⋅ B"
  shows "∃(u, v) ∈ Partitions x. u ∈ A ∧ v ∈ B"
using assms unfolding conc_def Partitions_def
by auto

lemma conc_partitions_intro:
  assumes "(u, v) ∈ Partitions x ∧ u ∈ A ∧  v ∈ B"
  shows "x ∈ A ⋅ B"
using assms unfolding conc_def Partitions_def
by auto

lemma equiv_class_member:
  assumes "x ∈ A"
  and "≈A `` {x} = ≈A `` {y}" 
  shows "y ∈ A"
using assms
apply(simp)
apply(simp add: str_eq_def)
apply(metis append_Nil2)
done

definition 
  tag_Times :: "'a lang ⇒ 'a lang ⇒ 'a list ⇒ 'a lang × 'a lang set"
where
  "tag_Times A B ≡ λx. (≈A `` {x}, {(≈B `` {x⇩s}) | x⇩p x⇩s. x⇩p ∈ A ∧ (x⇩p, x⇩s) ∈ Partitions x})"

lemma tag_Times_injI:
  assumes a: "tag_Times A B x = tag_Times A B y"
  and     c: "x @ z ∈ A ⋅ B"
  shows "y @ z ∈ A ⋅ B"
proof -
  from c obtain u v where 
    h1: "(u, v) ∈ Partitions (x @ z)" and
    h2: "u ∈ A" and
    h3: "v ∈ B" by (auto dest: conc_partitions_elim)
  from h1 have "x @ z = u @ v" unfolding Partitions_def by simp
  then obtain us 
    where "(x = u @ us ∧ us @ z = v) ∨ (x @ us = u ∧ z = us @ v)"
    by (auto simp add: append_eq_append_conv2)
  moreover
  { assume eq: "x = u @ us" "us @ z = v"
    have "(≈B `` {us}) ∈ snd (tag_Times A B x)"
      unfolding Partitions_def tag_Times_def using h2 eq 
      by (auto simp add: str_eq_def)
    then have "(≈B `` {us}) ∈ snd (tag_Times A B y)"
      using a by simp
    then obtain u' us' where
      q1: "u' ∈ A" and
      q2: "≈B `` {us} = ≈B `` {us'}" and
      q3: "(u', us') ∈ Partitions y" 
      unfolding tag_Times_def by auto
    from q2 h3 eq 
    have "us' @ z ∈ B"
      unfolding Image_def str_eq_def by auto
    then have "y @ z ∈ A ⋅ B" using q1 q3 
      unfolding Partitions_def by auto
  }
  moreover
  { assume eq: "x @ us = u" "z = us @ v"
    have "(≈A `` {x}) = fst (tag_Times A B x)" 
      by (simp add: tag_Times_def)
    then have "(≈A `` {x}) = fst (tag_Times A B y)"
      using a by simp
    then have "≈A `` {x} = ≈A `` {y}" 
      by (simp add: tag_Times_def)
    moreover 
    have "x @ us ∈ A" using h2 eq by simp
    ultimately 
    have "y @ us ∈ A" using equiv_class_member 
      unfolding Image_def str_eq_def by blast
    then have "(y @ us) @ v ∈ A ⋅ B" 
      using h3 unfolding conc_def by blast
    then have "y @ z ∈ A ⋅ B" using eq by simp 
  }
  ultimately show "y @ z ∈ A ⋅ B" by blast
qed

lemma quot_conc_finiteI [intro]:
  assumes fin1: "finite (UNIV // ≈A)" 
  and     fin2: "finite (UNIV // ≈B)" 
  shows "finite (UNIV // ≈(A ⋅ B))"
proof (rule_tac tag = "tag_Times A B" in tag_finite_imageD)
  have "⋀x y z. ⟦tag_Times A B x = tag_Times A B y; x @ z ∈ A ⋅ B⟧ ⟹ y @ z ∈ A ⋅ B"
    by (rule tag_Times_injI)
       (auto simp add: tag_Times_def tag_eq_def)
  then show "=tag_Times A B= ⊆ ≈(A ⋅ B)"
    by (rule refined_intro)
       (auto simp add: tag_eq_def)
next
  have *: "finite ((UNIV // ≈A) × (Pow (UNIV // ≈B)))" 
    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


subsection ‹Case for @{const "Star"}›

lemma star_partitions_elim:
  assumes "x @ z ∈ A⋆" "x ≠ []"
  shows "∃(u, v) ∈ Partitions (x @ z). strict_prefix u x ∧ u ∈ A⋆ ∧ v ∈ A⋆"
proof -
  have "([], x @ z) ∈ Partitions (x @ z)" "strict_prefix [] x" "[] ∈ A⋆" "x @ z ∈ A⋆"
    using assms by (auto simp add: Partitions_def strict_prefix_def)
  then show "∃(u, v) ∈ Partitions (x @ z). strict_prefix u x ∧ u ∈ A⋆ ∧ v ∈ A⋆"
    by blast
qed

lemma finite_set_has_max2: 
  "⟦finite A; A ≠ {}⟧ ⟹ ∃ max ∈ A. ∀ a ∈ A. length a ≤ length max"
apply(induct rule:finite.induct)
apply(simp)
by (metis (no_types) all_not_in_conv insert_iff linorder_le_cases order_trans)

lemma finite_strict_prefix_set: 
  shows "finite {xa. strict_prefix xa (x::'a list)}"
apply (induct x rule:rev_induct, simp)
apply (subgoal_tac "{xa. strict_prefix xa (xs @ [x])} = {xa. strict_prefix xa xs} ∪ {xs}")
by (auto simp:strict_prefix_def)

lemma append_eq_cases:
  assumes a: "x @ y = m @ n" "m ≠ []"  
  shows "prefix x m ∨ strict_prefix m x"
unfolding prefix_def strict_prefix_def using a
by (auto simp add: append_eq_append_conv2)

lemma star_spartitions_elim2:
  assumes a: "x @ z ∈ A⋆" 
  and     b: "x ≠ []"
  shows "∃(u, v) ∈ Partitions x. ∃ (u', v') ∈ Partitions z. strict_prefix u x ∧ u ∈ A⋆ ∧ v @ u' ∈ A ∧ v' ∈ A⋆"
proof -
  define S where "S = {u | u v. (u, v) ∈ Partitions x ∧ strict_prefix u x ∧ u ∈ A⋆ ∧ v @ z ∈ A⋆}"
  have "finite {u. strict_prefix u x}" by (rule finite_strict_prefix_set)
  then have "finite S" unfolding S_def
    by (rule rev_finite_subset) (auto)
  moreover 
  have "S ≠ {}" using a b unfolding S_def Partitions_def
    by (auto simp: strict_prefix_def)
  ultimately have "∃ u_max ∈ S. ∀ u ∈ S. length u ≤ length u_max"  
    using finite_set_has_max2 by blast
  then obtain u_max v 
    where h0: "(u_max, v) ∈ Partitions x"
    and h1: "strict_prefix u_max x" 
    and h2: "u_max ∈ A⋆" 
    and h3: "v @ z ∈ A⋆"  
    and h4: "∀ u v. (u, v) ∈ Partitions x ∧ strict_prefix u x ∧ u ∈ A⋆ ∧ v @ z ∈ A⋆ ⟶ length u ≤ length u_max"
    unfolding S_def Partitions_def by blast
  have q: "v ≠ []" using h0 h1 b unfolding Partitions_def by auto
  from h3 obtain a b
    where i1: "(a, b) ∈ Partitions (v @ z)"
    and   i2: "a ∈ A"
    and   i3: "b ∈ A⋆"
    and   i4: "a ≠ []"
    unfolding Partitions_def
    using q by (auto dest: star_decom)
  have "prefix v a"
  proof (rule ccontr)
    assume a: "¬(prefix v a)"
    from i1 have i1': "a @ b = v @ z" unfolding Partitions_def by simp
    then have "prefix a v ∨ strict_prefix v a" using append_eq_cases q by blast
    then have q: "strict_prefix a v" using a unfolding strict_prefix_def prefix_def by auto
    then obtain as where eq: "a @ as = v" unfolding strict_prefix_def prefix_def by auto
    have "(u_max @ a, as) ∈ Partitions x" using eq h0 unfolding Partitions_def by auto
    moreover
    have "strict_prefix (u_max @ a) x" using h0 eq q unfolding Partitions_def prefix_def strict_prefix_def by auto
    moreover
    have "u_max @ a ∈ A⋆" using i2 h2 by simp
    moreover
    have "as @ z ∈ A⋆" using i1' i2 i3 eq by auto
    ultimately have "length (u_max @ a) ≤ length u_max" using h4 by blast
    with i4 show "False" by auto
  qed
  with i1 obtain za zb
    where k1: "v @ za = a"
    and   k2: "(za, zb) ∈ Partitions z" 
    and   k4: "zb = b" 
    unfolding Partitions_def prefix_def
    by (auto simp add: append_eq_append_conv2)
  show "∃ (u, v) ∈ Partitions x. ∃ (u', v') ∈ Partitions z. strict_prefix u x ∧ u ∈ A⋆ ∧ v @ u' ∈ A ∧ v' ∈ A⋆"
    using h0 h1 h2 i2 i3 k1 k2 k4 unfolding Partitions_def by blast
qed

definition 
  tag_Star :: "'a lang ⇒ 'a list ⇒ ('a lang) set"
where
  "tag_Star A ≡ λx. {≈A `` {v} | u v. strict_prefix u x ∧ u ∈ A⋆ ∧ (u, v) ∈ Partitions x}"

lemma tag_Star_non_empty_injI:
  assumes a: "tag_Star A x = tag_Star A y"
  and     c: "x @ z ∈ A⋆"
  and     d: "x ≠ []"
  shows "y @ z ∈ A⋆"
proof -
  obtain u v u' v' 
    where a1: "(u,  v) ∈ Partitions x" "(u', v')∈ Partitions z"
    and   a2: "strict_prefix u x"
    and   a3: "u ∈ A⋆"
    and   a4: "v @ u' ∈ A" 
    and   a5: "v' ∈ A⋆"
    using c d by (auto dest: star_spartitions_elim2)
  have "(≈A) `` {v} ∈ tag_Star A x" 
    apply(simp add: tag_Star_def Partitions_def str_eq_def)
    using a1 a2 a3 by (auto simp add: Partitions_def)
  then have "(≈A) `` {v} ∈ tag_Star A y" using a by simp
  then obtain u1 v1 
    where b1: "v ≈A v1"
    and   b3: "u1 ∈ A⋆"
    and   b4: "(u1, v1) ∈ Partitions y"
    unfolding tag_Star_def by auto
  have c: "v1 @ u' ∈ A⋆" using b1 a4 unfolding str_eq_def by simp
  have "u1 @ (v1 @ u') @ v' ∈ A⋆"
    using b3 c a5 by (simp only: append_in_starI)
  then show "y @ z ∈ A⋆" using b4 a1 
    unfolding Partitions_def by auto
qed
    
lemma tag_Star_empty_injI:
  assumes a: "tag_Star A x = tag_Star A y"
  and     c: "x @ z ∈ A⋆"
  and     d: "x = []"
  shows "y @ z ∈ A⋆"
proof -
  from a have "{} = tag_Star A y" unfolding tag_Star_def using d by auto 
  then have "y = []"
    unfolding tag_Star_def Partitions_def strict_prefix_def prefix_def
    by (auto) (metis Nil_in_star append_self_conv2)
  then show "y @ z ∈ A⋆" using c d by simp
qed

lemma quot_star_finiteI [intro]:
  assumes finite1: "finite (UNIV // ≈A)"
  shows "finite (UNIV // ≈(A⋆))"
proof (rule_tac tag = "tag_Star A" in tag_finite_imageD)
  have "⋀x y z. ⟦tag_Star A x = tag_Star A y; x @ z ∈ A⋆⟧ ⟹ y @ z ∈ A⋆"
    by (case_tac "x = []") (blast intro: tag_Star_empty_injI tag_Star_non_empty_injI)+
  then show "=(tag_Star A)= ⊆ ≈(A⋆)"
    by (rule refined_intro) (auto simp add: tag_eq_def)
next
  have *: "finite (Pow (UNIV // ≈A))" 
     using finite1 by auto
  show "finite (range (tag_Star A))"
    unfolding tag_Star_def 
    by (rule finite_subset[OF _ *])
       (auto simp add: quotient_def)
qed

subsection ‹The conclusion of the second direction›

lemma Myhill_Nerode2:
  fixes r::"'a rexp"
  shows "finite (UNIV // ≈(lang r))"
by (induct r) (auto)

end