Theory Myhill_Nerode

theory Myhill_Nerode
  imports Tree_Automata Ground_Ctxt
begin

subsection β€ΉMyhill Nerode characterization for regular tree languagesβ€Ί

lemma ground_ctxt_apply_pres_der:
  assumes "ta_der π’œ (term_of_gterm s) = ta_der π’œ (term_of_gterm t)"
  shows "ta_der π’œ (term_of_gterm C⟨s⟩G) = ta_der π’œ (term_of_gterm C⟨t⟩G)" using assms
  by (induct C) (auto, (metis append_Cons_nth_not_middle nth_append_length)+)

locale myhill_nerode =
  fixes β„± β„’ assumes term_subset: "β„’ βŠ† 𝒯G β„±"
begin

definition myhill (β€Ή_ ≑ℒ _β€Ί) where
  "myhill s t ≑ s ∈ 𝒯G β„± ∧ t ∈ 𝒯G β„± ∧ (βˆ€ C. C⟨s⟩G ∈ β„’ ∧ C⟨t⟩G ∈ β„’ ∨ C⟨s⟩G βˆ‰ β„’ ∧ C⟨t⟩G βˆ‰ β„’)"

lemma myhill_sound: "s ≑ℒ t ⟹ s ∈ 𝒯G β„±"  "s ≑ℒ t ⟹ t ∈ 𝒯G β„±"
  unfolding myhill_def by auto

lemma myhill_refl [simp]: "s ∈ 𝒯G β„± ⟹ s ≑ℒ s"
  unfolding myhill_def by auto

lemma myhill_symmetric: "s ≑ℒ t ⟹ t ≑ℒ s"
  unfolding myhill_def by auto

lemma myhill_trans [trans]:
  "s ≑ℒ t ⟹ t ≑ℒ u ⟹ s ≑ℒ u"
  unfolding myhill_def by auto

abbreviation myhill_r (β€ΉMNβ„’β€Ί) where
  "myhill_r ≑ {(s, t) | s t. s ≑ℒ t}"

lemma myhill_equiv:
  "equiv (𝒯G β„±) MNβ„’"
  apply (intro equivI) apply (auto simp: myhill_sound myhill_symmetric sym_def trans_def refl_on_def)
  using myhill_trans by blast

lemma rtl_der_image_on_myhill_inj:
  assumes "gta_lang Qf π’œ = β„’"
  shows "inj_on (Ξ» X. gta_der π’œ ` X) (𝒯G β„± // MNβ„’)" (is "inj_on ?D ?R")
proof -
  {fix S T assume eq_rel: "S ∈ ?R" "T ∈ ?R" "?D S = ?D T"
    have "β‹€ s t. s ∈ S ⟹ t ∈ T ⟹ s ≑ℒ t"
    proof -
      fix s t assume mem: "s ∈ S" "t ∈ T"
      then obtain t' where res: "t' ∈ T" "gta_der π’œ s = gta_der π’œ t'" using eq_rel(3)
        by (metis image_iff)
      from res(1) mem have "s ∈ 𝒯G β„±" "t ∈ 𝒯G β„±" "t' ∈ 𝒯G β„±" using eq_rel(1, 2)
        using in_quotient_imp_subset myhill_equiv by blast+
      then have "s ≑ℒ t'" using assms res ground_ctxt_apply_pres_der[of π’œ s]
        by (auto simp: myhill_def gta_der_def simp flip: ctxt_of_gctxt_apply
         elim!: gta_langE intro: gta_langI)
      moreover have "t' ≑ℒ t" using quotient_eq_iff[OF myhill_equiv eq_rel(2) eq_rel(2) res(1) mem(2)]
        by simp
      ultimately show "s ≑ℒ t" using myhill_trans by blast
    qed
    then have "β‹€ s t. s ∈ S ⟹ t ∈ T ⟹ (s, t) ∈ MNβ„’" by blast
    then have "S = T" using quotient_eq_iff[OF myhill_equiv eq_rel(1, 2)]
      using eq_rel(3) by fastforce}
  then show inj: "inj_on ?D ?R" by (meson inj_onI)
qed

lemma rtl_implies_finite_indexed_myhill_relation:
  assumes "gta_lang Qf π’œ = β„’"
  shows "finite (𝒯G β„± // MNβ„’)" (is "finite ?R")
proof -
  let ?D = "Ξ» X. gta_der π’œ ` X"
  have image: "?D ` ?R βŠ† Pow (fset (fPow (𝒬 π’œ)))" unfolding gta_der_def
    by (meson PowI fPowI ground_ta_der_states ground_term_of_gterm image_subsetI)
  then have "finite (Pow (fset (fPow (𝒬 π’œ))))" by simp
  then have "finite (?D ` ?R)" using finite_subset[OF image] by fastforce
  then show ?thesis using finite_image_iff[OF rtl_der_image_on_myhill_inj[OF assms]]
    by blast
qed

end

end