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

end