Theory Regular_Tree_Relations.AGTT

theory AGTT
  imports GTT GTT_Transitive_Closure Pair_Automaton
begin


definition AGTT_union where
  "AGTT_union 𝒒1 𝒒2 ≑ (ta_union (fst 𝒒1) (fst 𝒒2),
                       ta_union (snd 𝒒1) (snd 𝒒2))"

abbreviation AGTT_union' where
  "AGTT_union' 𝒒1 𝒒2 ≑ AGTT_union (fmap_states_gtt Inl 𝒒1) (fmap_states_gtt Inr 𝒒2)"

lemma disj_gtt_states_disj_fst_ta_states:
  assumes dist_st: "gtt_states 𝒒1 |∩| gtt_states 𝒒2 = {||}"
  shows "𝒬 (fst 𝒒1) |∩| 𝒬 (fst 𝒒2) = {||}"
  using assms unfolding gtt_states_def by auto

lemma disj_gtt_states_disj_snd_ta_states:
  assumes dist_st: "gtt_states 𝒒1 |∩| gtt_states 𝒒2 = {||}"
  shows "𝒬 (snd 𝒒1) |∩| 𝒬 (snd 𝒒2) = {||}"
  using assms unfolding gtt_states_def by auto

lemma ta_der_not_contains_undefined_state:
  assumes "q |βˆ‰| 𝒬 T" and "ground t"
  shows "q |βˆ‰| ta_der T t"
  using ground_ta_der_states[OF assms(2)] assms(1)
  by blast

lemma AGTT_union_sound1:
  assumes dist_st: "gtt_states 𝒒1 |∩| gtt_states 𝒒2 = {||}"
  shows "agtt_lang (AGTT_union 𝒒1 𝒒2) βŠ† agtt_lang 𝒒1 βˆͺ agtt_lang 𝒒2"
proof -
  let ?TA_A = "ta_union (fst 𝒒1) (fst 𝒒2)"
  let ?TA_B = "ta_union (snd 𝒒1) (snd 𝒒2)"
  {fix s t assume ass: "(s, t) ∈ agtt_lang (AGTT_union 𝒒1 𝒒2)"
    then obtain q where ls: "q |∈| ta_der ?TA_A (term_of_gterm s)" and
      rs: "q |∈| ta_der ?TA_B (term_of_gterm t)"
      by (auto simp add: AGTT_union_def agtt_lang_def gta_der_def)
    then have "(s, t) ∈ agtt_lang 𝒒1 ∨ (s, t) ∈ agtt_lang 𝒒2"
    proof (cases "q |∈| gtt_states 𝒒1")
      case True
      then have "q |βˆ‰| gtt_states 𝒒2" using dist_st
        by blast
      then have nt_fst_st: "q |βˆ‰| 𝒬 (fst 𝒒2)" and
        nt_snd_state: "q |βˆ‰| 𝒬 (snd 𝒒2)" by (auto simp add: gtt_states_def)
      from True show ?thesis
        using ls rs
        using ta_der_not_contains_undefined_state[OF nt_fst_st]
        using ta_der_not_contains_undefined_state[OF nt_snd_state]
        unfolding gtt_states_def agtt_lang_def gta_der_def
        using ta_union_der_disj_states[OF disj_gtt_states_disj_fst_ta_states[OF dist_st]]
        using ta_union_der_disj_states[OF disj_gtt_states_disj_snd_ta_states[OF dist_st]]
        using ground_term_of_gterm by blast
    next
      case False
      then have "q |βˆ‰| gtt_states 𝒒1" by (metis IntI dist_st emptyE)
      then have nt_fst_st: "q |βˆ‰| 𝒬 (fst 𝒒1)" and
        nt_snd_state: "q |βˆ‰| 𝒬 (snd 𝒒1)" by (auto simp add: gtt_states_def)
      from False show ?thesis
        using ls rs
        using ta_der_not_contains_undefined_state[OF nt_fst_st]
        using ta_der_not_contains_undefined_state[OF nt_snd_state]
        unfolding gtt_states_def agtt_lang_def gta_der_def
        using ta_union_der_disj_states[OF disj_gtt_states_disj_fst_ta_states[OF dist_st]]
        using ta_union_der_disj_states[OF disj_gtt_states_disj_snd_ta_states[OF dist_st]]
        using ground_term_of_gterm by blast
    qed}
  then show ?thesis by auto
qed

lemma AGTT_union_sound2:
  shows "agtt_lang 𝒒1 βŠ† agtt_lang (AGTT_union 𝒒1 𝒒2)"
    "agtt_lang 𝒒2 βŠ† agtt_lang (AGTT_union 𝒒1 𝒒2)"
  unfolding agtt_lang_def gta_der_def AGTT_union_def
  by auto (meson fin_mono ta_der_mono' ta_union_ta_subset)+

lemma AGTT_union_sound:
  assumes dist_st: "gtt_states 𝒒1 |∩| gtt_states 𝒒2 = {||}"
  shows "agtt_lang (AGTT_union 𝒒1 𝒒2) = agtt_lang 𝒒1 βˆͺ agtt_lang 𝒒2"
  using AGTT_union_sound1[OF assms] AGTT_union_sound2 by blast

lemma AGTT_union'_sound:
  fixes 𝒒1 :: "('q, 'f) gtt" and 𝒒2 :: "('q, 'f) gtt"
  shows "agtt_lang (AGTT_union' 𝒒1 𝒒2) = agtt_lang 𝒒1 βˆͺ agtt_lang 𝒒2"
proof -
  have map: "agtt_lang (AGTT_union' 𝒒1 𝒒2) =
    agtt_lang (fmap_states_gtt CInl 𝒒1) βˆͺ agtt_lang (fmap_states_gtt CInr 𝒒2)"
    by (intro  AGTT_union_sound) (auto simp add: agtt_lang_fmap_states_gtt)
  then show ?thesis by (simp add: agtt_lang_fmap_states_gtt finj_CInl_CInr)
qed

subsection β€ΉAnchord gtt compositonβ€Ί

definition AGTT_comp :: "('q, 'f) gtt β‡’ ('q, 'f) gtt β‡’ ('q, 'f) gtt" where
  "AGTT_comp 𝒒1 𝒒2 = (let (π’œ, ℬ) = (fst 𝒒1, snd 𝒒2) in
    (TA (rules π’œ) (eps π’œ |βˆͺ| (ΔΡ (snd 𝒒1) (fst 𝒒2) |∩| (gtt_interface 𝒒1 |Γ—| gtt_interface 𝒒2))),
     TA (rules ℬ) (eps ℬ)))"

abbreviation AGTT_comp' where
  "AGTT_comp' 𝒒1 𝒒2 ≑ AGTT_comp (fmap_states_gtt Inl 𝒒1) (fmap_states_gtt Inr 𝒒2)"

lemma AGTT_comp_sound:
  assumes "gtt_states 𝒒1 |∩| gtt_states 𝒒2 = {||}"
  shows "agtt_lang (AGTT_comp 𝒒1 𝒒2) = agtt_lang 𝒒1 O agtt_lang 𝒒2"
proof -
  let ?Q1 = "fId_on (gtt_interface 𝒒1)" let ?Q2 = "fId_on (gtt_interface 𝒒2)" 
  have lan: "agtt_lang 𝒒1 = pair_at_lang 𝒒1 ?Q1" "agtt_lang 𝒒2 = pair_at_lang 𝒒2 ?Q2"
    using pair_at_agtt[of 𝒒1] pair_at_agtt[of 𝒒2]
    by auto
  have "agtt_lang 𝒒1 O agtt_lang 𝒒2 = pair_at_lang (fst 𝒒1, snd 𝒒2) (Ξ”_eps_pair 𝒒1 ?Q1 𝒒2 ?Q2)"
    using pair_comp_sound1 pair_comp_sound2
    by (auto simp add: lan pair_comp_sound1 pair_comp_sound2 relcomp.simps)
  moreover have "AGTT_comp 𝒒1 𝒒2 = pair_at_to_agtt (fst 𝒒1, snd 𝒒2) (Ξ”_eps_pair 𝒒1 ?Q1 𝒒2 ?Q2)"
    by (auto simp: AGTT_comp_def pair_at_to_agtt_def gtt_interface_def ΔΡ_def' Ξ”_eps_pair_def)
  ultimately show ?thesis using pair_at_agtt_conv[of "Ξ”_eps_pair 𝒒1 ?Q1 𝒒2 ?Q2" "(fst 𝒒1, snd 𝒒2)"]
    using assms
    by (auto simp: Ξ”_eps_pair_def gtt_states_def gtt_interface_def)
qed

lemma AGTT_comp'_sound:
  "agtt_lang (AGTT_comp' 𝒒1 𝒒2) = agtt_lang 𝒒1 O agtt_lang 𝒒2"
  using AGTT_comp_sound[of "fmap_states_gtt (Inl :: 'b β‡’ 'b + 'c) 𝒒1"
    "fmap_states_gtt (Inr :: 'c β‡’ 'b + 'c) 𝒒2"]
  by (auto simp add: agtt_lang_fmap_states_gtt disjoint_iff_not_equal agtt_lang_Inl_Inr_states_agtt)

subsection β€ΉAnchord gtt transitivityβ€Ί

definition AGTT_trancl :: "('q, 'f) gtt β‡’ ('q + 'q, 'f) gtt" where
  "AGTT_trancl 𝒒 = (let π’œ = fmap_states_ta Inl (fst 𝒒) in
    (TA (rules π’œ) (eps π’œ |βˆͺ| map_prod CInl CInr |`| (Ξ”_Atrans_gtt 𝒒 (fId_on (gtt_interface 𝒒)))),
     TA (map_ta_rule CInr id |`| (rules (snd 𝒒))) (map_both CInr |`| (eps (snd 𝒒)))))"

lemma AGTT_trancl_sound:
  shows "agtt_lang (AGTT_trancl 𝒒) = (agtt_lang 𝒒)+"
proof -
  let ?P = "map_prod (fmap_states_ta CInl) (fmap_states_ta CInr) 𝒒"
  let ?Q = "fId_on (gtt_interface 𝒒)" let ?Q' = "map_prod CInl CInr |`| ?Q"
  have inv: "finj_on CInl (𝒬 (fst 𝒒))" "finj_on CInr (𝒬 (snd 𝒒))"
    "?Q |βŠ†| 𝒬 (fst 𝒒) |Γ—| 𝒬 (snd 𝒒)"
    by (auto simp: gtt_interface_def finj_CInl_CInr)
  have *: "fst |`| map_prod CInl CInr |`| Ξ”_Atrans_gtt 𝒒 (fId_on (gtt_interface 𝒒)) |βŠ†| CInl |`| 𝒬 (fst 𝒒)"
    using fsubsetD[OF Ξ”_Atrans_states_stable[OF inv(3)]]
    by (auto simp add: gtt_interface_def)
  from pair_at_lang_fun_states[OF inv]
  have "agtt_lang 𝒒 = pair_at_lang ?P ?Q'" using pair_at_agtt[of 𝒒] by auto
  moreover then have "(agtt_lang 𝒒)+ = pair_at_lang ?P (Ξ”_Atrans_gtt ?P ?Q')"
    by (simp add: pair_trancl_sound)
  moreover have "AGTT_trancl 𝒒 = pair_at_to_agtt ?P (Ξ”_Atrans_gtt ?P ?Q')"
    using Ξ”_Atrans_states_stable[OF inv(3)] Ξ”_Atrans_map_prod[OF inv, symmetric]
    using fId_on_frelcomp_id[OF *]
    by (auto simp: AGTT_trancl_def pair_at_to_agtt_def gtt_interface_def Let_def fmap_states_ta_def)
       (metis fmap_prod_fimageI fmap_states fmap_states_ta_def)
  moreover have "gtt_interface (map_prod (fmap_states_ta CInl) (fmap_states_ta CInr) 𝒒) = {||}"
    by (auto simp: gtt_interface_def)
  ultimately show ?thesis using pair_at_agtt_conv[of "Ξ”_Atrans_gtt ?P ?Q'" ?P] Ξ”_Atrans_states_stable[OF inv(3)]
    unfolding Ξ”_Atrans_map_prod[OF inv, symmetric]
    by (simp add: fimage_mono gtt_interface_def map_prod_ftimes)
qed

subsection β€ΉAnchord gtt intersectionβ€Ί

definition AGTT_inter where
  "AGTT_inter 𝒒1 𝒒2 ≑ (prod_ta (fst 𝒒1) (fst 𝒒2),
                       prod_ta (snd 𝒒1) (snd 𝒒2))"

lemma AGTT_inter_sound:
  "agtt_lang (AGTT_inter 𝒒1 𝒒2) = agtt_lang 𝒒1 ∩ agtt_lang 𝒒2" (is "?Ls = ?Rs")
proof -
  let ?TA_A = "prod_ta (fst 𝒒1) (fst 𝒒2)"
  let ?TA_B = "prod_ta (snd 𝒒1) (snd 𝒒2)"
  {fix s t assume ass: "(s, t) ∈ agtt_lang (AGTT_inter 𝒒1 𝒒2)"
    then obtain q where ls: "q |∈| ta_der ?TA_A (term_of_gterm s)" and
      rs: "q |∈| ta_der ?TA_B (term_of_gterm t)"
      by (auto simp add: AGTT_inter_def agtt_lang_def gta_der_def)
    then have "(s, t) ∈ agtt_lang 𝒒1 ∧ (s, t) ∈ agtt_lang 𝒒2"
      using prod_ta_der_to_π’œ_ℬ_der1[of q] prod_ta_der_to_π’œ_ℬ_der2[of q]
      by (auto simp: agtt_lang_def gta_der_def) blast}
  then have f: "?Ls βŠ† ?Rs" by auto
  moreover have "?Rs βŠ† ?Ls" using π’œ_ℬ_der_to_prod_ta
    by (fastforce simp: agtt_lang_def AGTT_inter_def gta_der_def)
  ultimately show ?thesis by blast
qed

subsection β€ΉAnchord gtt trimingβ€Ί

abbreviation "trim_agtt ≑ trim_gtt"

lemma agtt_only_prod_lang:
  "agtt_lang (gtt_only_prod 𝒒) = agtt_lang 𝒒" (is "?Ls = ?Rs")
proof -
  let ?A = "fst 𝒒" let ?B = "snd 𝒒"
  have "?Ls βŠ† ?Rs" unfolding agtt_lang_def gtt_only_prod_def
    by (auto simp: Let_def gta_der_def dest: ta_der_ta_only_prod_ta_der)
  moreover
  {fix s t assume "(s, t) ∈ ?Rs"
    then obtain q where r: "q |∈| ta_der (fst 𝒒) (term_of_gterm s)" "q |∈| ta_der (snd 𝒒) (term_of_gterm t)"
      by (auto simp: agtt_lang_def gta_der_def)
    then have " q |∈| gtt_interface 𝒒" by (auto simp: gtt_interface_def)
    then have "(s, t) ∈ ?Ls" using r
      by (auto simp: agtt_lang_def gta_der_def gtt_only_prod_def Let_def intro!: exI[of _ q] ta_der_only_prod ta_productive_setI)}
  ultimately show ?thesis by auto
qed

lemma agtt_only_reach_lang:
  "agtt_lang (gtt_only_reach 𝒒) = agtt_lang 𝒒"
  unfolding agtt_lang_def gtt_only_reach_def
  by (auto simp: gta_der_def simp flip: ta_der_gterm_only_reach)

lemma trim_agtt_lang [simp]:
  "agtt_lang (trim_agtt G) = agtt_lang G"
  unfolding trim_gtt_def comp_def agtt_only_prod_lang agtt_only_reach_lang ..


end