Theory 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 ?Q⇩1 = "fId_on (gtt_interface 𝒢⇩1)" let ?Q⇩2 = "fId_on (gtt_interface 𝒢⇩2)" 
  have lan: "agtt_lang 𝒢⇩1 = pair_at_lang 𝒢⇩1 ?Q⇩1" "agtt_lang 𝒢⇩2 = pair_at_lang 𝒢⇩2 ?Q⇩2"
    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 ?Q⇩1 𝒢⇩2 ?Q⇩2)"
    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 ?Q⇩1 𝒢⇩2 ?Q⇩2)"
    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 ?Q⇩1 𝒢⇩2 ?Q⇩2" "(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