# Theory Regular_Tree_Relations.GTT_Transitive_Closure

```theory GTT_Transitive_Closure
imports GTT_Compose
begin

subsection ‹GTT closure under transitivity›

inductive_set Δ_trancl_set :: "('q, 'f) ta ⇒ ('q, 'f) ta ⇒ ('q × 'q) set" for A B where
Δ_set_cong: "TA_rule f ps p |∈| rules A ⟹ TA_rule f qs q |∈| rules B ⟹ length ps = length qs ⟹
(⋀i. i < length qs ⟹ (ps ! i, qs ! i) ∈ Δ_trancl_set A B) ⟹ (p, q) ∈ Δ_trancl_set A B"
| Δ_set_eps1: "(p, p') |∈| eps A ⟹ (p, q) ∈ Δ_trancl_set A B ⟹ (p', q) ∈ Δ_trancl_set A B"
| Δ_set_eps2: "(q, q') |∈| eps B ⟹ (p, q) ∈ Δ_trancl_set A B ⟹ (p, q') ∈ Δ_trancl_set A B"
| Δ_set_trans: "(p, q) ∈ Δ_trancl_set A B ⟹ (q, r) ∈ Δ_trancl_set A B ⟹ (p, r) ∈ Δ_trancl_set A B"

lemma Δ_trancl_set_states: "Δ_trancl_set 𝒜 ℬ ⊆ fset (𝒬 𝒜 |×| 𝒬 ℬ)"
proof -
{fix p q assume "(p, q) ∈ Δ_trancl_set 𝒜 ℬ" then have "(p, q) ∈ fset (𝒬 𝒜 |×| 𝒬 ℬ)"
by (induct) (auto dest: rule_statesD eps_statesD)}
then show ?thesis by auto
qed

lemma finite_Δ_trancl_set [simp]: "finite (Δ_trancl_set 𝒜 ℬ)"
using finite_subset[OF Δ_trancl_set_states]
by simp

context
includes fset.lifting
begin
lift_definition Δ_trancl :: "('q, 'f) ta ⇒ ('q, 'f) ta ⇒ ('q × 'q) fset" is Δ_trancl_set by simp
lemmas Δ_trancl_cong = Δ_set_cong [Transfer.transferred]
lemmas Δ_trancl_eps1 = Δ_set_eps1 [Transfer.transferred]
lemmas Δ_trancl_eps2 = Δ_set_eps2 [Transfer.transferred]
lemmas Δ_trancl_cases = Δ_trancl_set.cases[Transfer.transferred]
lemmas Δ_trancl_induct [consumes 1, case_names Δ_cong Δ_eps1 Δ_eps2 Δ_trans] = Δ_trancl_set.induct[Transfer.transferred]
lemmas Δ_trancl_intros = Δ_trancl_set.intros[Transfer.transferred]
lemmas Δ_trancl_simps = Δ_trancl_set.simps[Transfer.transferred]
end

lemma Δ_trancl_cl [simp]:
"(Δ_trancl A B)|⇧+| = Δ_trancl A B"
proof -
{fix s t assume "(s, t) |∈| (Δ_trancl A B)|⇧+|" then have "(s, t) |∈| Δ_trancl A B"
by (induct rule: ftrancl_induct) (auto intro: Δ_trancl_intros)}
then show ?thesis by auto
qed

lemma Δ_trancl_states: "Δ_trancl 𝒜 ℬ |⊆| (𝒬 𝒜 |×| 𝒬 ℬ)"
using Δ_trancl_set_states
by (metis Δ_trancl.rep_eq fSigma_cong less_eq_fset.rep_eq)

definition GTT_trancl where
"GTT_trancl G =
(let Δ = Δ_trancl (snd G) (fst G) in
(TA (rules (fst G)) (eps (fst G) |∪| Δ),
TA (rules (snd G)) (eps (snd G) |∪| (Δ|¯|))))"

lemma Δ_trancl_inv:
"(Δ_trancl A B)|¯| = Δ_trancl B A"
proof -
have [dest]: "(p, q) |∈| Δ_trancl A B ⟹ (q, p) |∈| Δ_trancl B A" for p q A B
by (induct rule: Δ_trancl_induct) (auto intro: Δ_trancl_intros)
show ?thesis by auto
qed

lemma gtt_states_GTT_trancl:
"gtt_states (GTT_trancl G) |⊆| gtt_states G"
unfolding GTT_trancl_def
by (auto simp: gtt_states_def 𝒬_def Δ_trancl_inv dest!: fsubsetD[OF Δ_trancl_states])

lemma gtt_syms_GTT_trancl:
"gtt_syms (GTT_trancl G) = gtt_syms G"
by (auto simp: GTT_trancl_def ta_sig_def Δ_trancl_inv)

lemma GTT_trancl_base:
"gtt_lang G ⊆ gtt_lang (GTT_trancl G)"
using gtt_lang_mono[of G "GTT_trancl G"] by (auto simp: Δ_trancl_inv GTT_trancl_def)

lemma GTT_trancl_trans:
"gtt_lang (GTT_comp (GTT_trancl G) (GTT_trancl G)) ⊆ gtt_lang (GTT_trancl G)"
proof -
have [dest]: "(p, q) |∈| Δ⇩ε (TA (rules A) (eps A |∪| (Δ_trancl B A)))
(TA (rules B) (eps B |∪| (Δ_trancl A B))) ⟹ (p, q) |∈| Δ_trancl A B" for p q A B
by (induct rule: Δ⇩ε_induct) (auto intro: Δ_trancl_intros simp: Δ_trancl_inv[of B A, symmetric])
show ?thesis
by (intro gtt_lang_mono[of "GTT_comp (GTT_trancl G) (GTT_trancl G)" "GTT_trancl G"])
(auto simp: GTT_comp_def GTT_trancl_def Δ_trancl_inv)
qed

lemma agtt_lang_base:
"agtt_lang G ⊆ agtt_lang (GTT_trancl G)"
by (rule agtt_lang_mono) (auto simp: GTT_trancl_def Δ_trancl_inv)

lemma Δ⇩ε_tr_incl:
"Δ⇩ε (TA (rules A) (eps A |∪| Δ_trancl B A)) (TA (rules B)  (eps B |∪| Δ_trancl A B)) = Δ_trancl A B"
(is "?LS = ?RS")
proof -
{fix p q assume "(p, q) |∈| ?LS" then have "(p, q) |∈| ?RS"
by (induct rule: Δ⇩ε_induct)
(auto simp: Δ_trancl_inv[of B A, symmetric] intro: Δ_trancl_intros)}
moreover
{fix p q assume "(p, q) |∈| ?RS" then have "(p, q) |∈| ?LS"
by (induct rule: Δ_trancl_induct)
(auto simp: Δ_trancl_inv[of B A, symmetric] intro: Δ⇩ε_intros)}
ultimately show ?thesis
by auto
qed

lemma agtt_lang_trans:
"gcomp_rel UNIV (agtt_lang (GTT_trancl G)) (agtt_lang (GTT_trancl G)) ⊆ agtt_lang (GTT_trancl G)"
proof -
have [intro!, dest]: "(p, q) |∈| Δ⇩ε (TA (rules A) (eps A |∪| (Δ_trancl B A)))
(TA (rules B) (eps B |∪| (Δ_trancl A B))) ⟹ (p, q) |∈| Δ_trancl A B" for p q A B
by (induct rule: Δ⇩ε_induct) (auto intro: Δ_trancl_intros simp: Δ_trancl_inv[of B A, symmetric])
show ?thesis
by (rule subset_trans[OF gtt_comp_acomplete agtt_lang_mono])
(auto simp: GTT_comp_def GTT_trancl_def Δ_trancl_inv)
qed

lemma GTT_trancl_acomplete:
"gtrancl_rel UNIV (agtt_lang G) ⊆ agtt_lang (GTT_trancl G)"
unfolding gtrancl_rel_def
using agtt_lang_base[of G] gmctxt_cl_mono_rel[OF agtt_lang_base[of G], of UNIV]
using agtt_lang_trans[of G]
unfolding gcomp_rel_def
by (intro kleene_trancl_induct) blast+

lemma Restr_rtrancl_gtt_lang_eq_trancl_gtt_lang:
"(gtt_lang G)⇧* = (gtt_lang G)⇧+"
by (auto simp: rtrancl_trancl_reflcl simp del: reflcl_trancl dest: tranclD tranclD2 intro: gmctxt_cl_refl)

lemma GTT_trancl_complete:
"(gtt_lang G)⇧+ ⊆ gtt_lang (GTT_trancl G)"
using GTT_trancl_base subset_trans[OF gtt_comp_lang_complete GTT_trancl_trans]
by (metis trancl_id trancl_mono_set trans_O_iff)

lemma trancl_gtt_lang_arg_closed:
assumes "length ss = length ts" "∀i < length ts. (ss ! i, ts ! i) ∈ (gtt_lang 𝒢)⇧+"
shows "(GFun f ss, GFun f ts) ∈ (gtt_lang 𝒢)⇧+" (is "?e ∈ _")
proof -
have "all_ctxt_closed UNIV ((gtt_lang 𝒢)⇧+)" by (intro all_ctxt_closed_trancl) auto
from all_ctxt_closedD[OF this _ assms] show ?thesis
by auto
qed

lemma Δ_trancl_sound:
assumes "(p, q) |∈| Δ_trancl A B"
obtains s t where "(s, t) ∈ (gtt_lang (B, A))⇧+" "p |∈| gta_der A s" "q |∈| gta_der B t"
using assms
proof (induct arbitrary: thesis rule: Δ_trancl_induct)
case (Δ_cong f ps p qs q)
have "∃si ti. (si, ti) ∈ (gtt_lang (B, A))⇧+ ∧ ps ! i |∈| gta_der A (si) ∧
qs ! i |∈| gta_der B (ti)" if "i < length qs" for i
using Δ_cong(5)[OF that] by metis
then obtain ss ts where
"⋀i. i < length qs ⟹ (ss i, ts i) ∈ (gtt_lang (B, A))⇧+ ∧ ps ! i |∈| gta_der A (ss i) ∧ qs ! i |∈| gta_der B (ts i)" by metis
then show ?case using Δ_cong(1-5)
by (intro Δ_cong(6)[of "GFun f (map ss [0..<length ps])" "GFun f (map ts [0..<length qs])"])
(auto simp: gta_der_def intro!: trancl_gtt_lang_arg_closed)
next
case (Δ_eps1 p p' q) then show ?case
by (metis gta_der_def ta_der_eps)
next
case (Δ_eps2 q q' p) then show ?case
by (metis gta_der_def ta_der_eps)
next
case (Δ_trans p q r)
obtain s1 t1 where "(s1, t1) ∈ (gtt_lang (B, A))⇧+" "p |∈| gta_der A s1" "q |∈| gta_der B t1"
using Δ_trans(2) .note 1 = this
obtain s2 t2 where "(s2, t2) ∈ (gtt_lang (B, A))⇧+" "q |∈| gta_der A s2" "r |∈| gta_der B t2"
using Δ_trans(4) . note 2 = this
have "(t1, s2) ∈ gtt_lang (B, A)" using 1(1,3) 2(1,2)
by (auto simp: Restr_rtrancl_gtt_lang_eq_trancl_gtt_lang[symmetric] gtt_lang_join)
then have "(s1, t2) ∈ (gtt_lang (B, A))⇧+" using 1(1) 2(1)
by (meson trancl.trancl_into_trancl trancl_trans)
then show ?case using 1(2) 2(3) by (auto intro: Δ_trans(5)[of s1 t2])
qed

lemma GTT_trancl_sound_aux:
assumes "p |∈| gta_der (TA (rules A) (eps A |∪| (Δ_trancl B A))) s"
shows "∃t. (s, t) ∈ (gtt_lang (A, B))⇧+ ∧ p |∈| gta_der A t"
using assms
proof (induct s arbitrary: p)
case (GFun f ss)
let ?eps = "eps A |∪| Δ_trancl B A"
obtain qs q where q: "TA_rule f qs q |∈| rules A" "q = p ∨ (q, p) |∈| ?eps|⇧+|" "length qs = length ss"
"⋀i. i < length ss ⟹ qs ! i |∈| gta_der (TA (rules A) ?eps) (ss ! i)"
using GFun(2) by (auto simp: gta_der_def)
have "⋀i. i < length ss ⟹ ∃ti. (ss ! i, ti) ∈ (gtt_lang (A, B))⇧+ ∧ qs ! i |∈| gta_der A (ti)"
using GFun(1)[OF nth_mem q(4)] unfolding gta_der_def by fastforce
then obtain ts where ts: "⋀i. i < length ss ⟹ (ss ! i, ts i) ∈ (gtt_lang (A, B))⇧+ ∧ qs ! i |∈| gta_der A (ts i)"
by metis
then have q': "q |∈| gta_der A (GFun f (map ts [0..<length ss]))"
"(GFun f ss, GFun f (map ts [0..<length ss])) ∈ (gtt_lang (A, B))⇧+" using q(1, 3)
by (auto simp: gta_der_def intro!: exI[of _ qs] exI[of _ q] trancl_gtt_lang_arg_closed)
{fix p q u assume ass: "(p, q) |∈| Δ_trancl B A" "(GFun f ss, u) ∈ (gtt_lang (A, B))⇧+ ∧ p |∈| gta_der A u"
from Δ_trancl_sound[OF this(1)] obtain s t
where "(s, t) ∈ (gtt_lang (A, B))⇧+" "p |∈| gta_der B s" "q |∈| gta_der A t" . note st = this
have "(u, s) ∈ gtt_lang (A, B)" using st conjunct2[OF ass(2)]
by (auto simp: Restr_rtrancl_gtt_lang_eq_trancl_gtt_lang[symmetric] gtt_lang_join)
then have "(GFun f ss, t) ∈ (gtt_lang (A, B))⇧+"
using ass st(1) by (meson trancl_into_trancl2 trancl_trans)
then have "∃ s t. (GFun f ss, t) ∈ (gtt_lang (A, B))⇧+ ∧ q |∈| gta_der A t" using st by blast}
note trancl_step = this
show ?case
proof (cases "q = p")
case True
then show ?thesis using ts q(1, 3)
by (auto simp: gta_der_def intro!: exI[of _"GFun f (map ts [0..< length ss])"] trancl_gtt_lang_arg_closed) blast
next
case False
then have "(q, p) |∈| ?eps|⇧+|" using q(2) by simp
then show ?thesis using q(1) q'
proof (induct rule: ftrancl_induct)
case (Base q p) from Base(1) show ?case
proof
assume "(q, p) |∈| eps A" then show ?thesis using Base(2) ts q(3)
by (auto simp: gta_der_def intro!: exI[of _"GFun f (map ts [0..< length ss])"]
trancl_gtt_lang_arg_closed exI[of _ qs] exI[of _ q])
next
assume "(q, p) |∈| (Δ_trancl B A)"
then have "(q, p) |∈| Δ_trancl B A" by simp
from trancl_step[OF this] show ?thesis using Base(3, 4)
by auto
qed
next
case (Step p q r)
from Step(2, 4-) obtain s' where s': "(GFun f ss, s') ∈ (gtt_lang (A, B))⇧+ ∧ q |∈| gta_der A s'" by auto
show ?case using Step(3)
proof
assume "(q, r) |∈| eps A" then show ?thesis using s'
by (auto simp: gta_der_def ta_der_eps intro!: exI[of _ s'])
next
assume "(q, r) |∈| Δ_trancl B A"
then have "(q, r) |∈| Δ_trancl B A" by simp
from trancl_step[OF this] show ?thesis using s' by auto
qed
qed
qed
qed

lemma GTT_trancl_asound:
"agtt_lang (GTT_trancl G) ⊆ gtrancl_rel UNIV (agtt_lang G)"
proof (intro subrelI, goal_cases LR)
case (LR s t)
then obtain s' q t' where *: "(s, s') ∈ (gtt_lang G)⇧+"
"q |∈| gta_der (fst G) s'" "q |∈| gta_der (snd G) t'" "(t', t) ∈ (gtt_lang G)⇧+"
by (auto simp: agtt_lang_def GTT_trancl_def trancl_converse Δ_trancl_inv
simp flip: gtt_lang_swap[of "fst G" "snd G", unfolded prod.collapse agtt_lang_def, simplified]
dest!: GTT_trancl_sound_aux)
then have "(s', t') ∈ agtt_lang G" using *(2,3)
by (auto simp: agtt_lang_def)
then show ?case using *(1,4) unfolding gtrancl_rel_def
by auto
qed

lemma GTT_trancl_sound:
"gtt_lang (GTT_trancl G) ⊆ (gtt_lang G)⇧+"
proof -
note [dest] = GTT_trancl_sound_aux
have "gtt_accept (GTT_trancl G) s t ⟹ (s, t) ∈ (gtt_lang G)⇧+" for s t unfolding gtt_accept_def
proof (induct rule: gmctxt_cl.induct)
case (base s t)
from base obtain q where join: "q |∈| gta_der (fst (GTT_trancl G)) s" "q |∈| gta_der (snd (GTT_trancl G)) t"
by (auto simp: agtt_lang_def)
obtain s' where "(s, s') ∈ (gtt_lang G)⇧+" "q |∈| gta_der (fst G) s'" using base join
by (auto simp: GTT_trancl_def Δ_trancl_inv agtt_lang_def)
moreover obtain t' where "(t', t) ∈ (gtt_lang G)⇧+" "q |∈| gta_der (snd G) t'" using join
by (auto simp: GTT_trancl_def gtt_lang_swap[of "fst G" "snd G", symmetric] trancl_converse Δ_trancl_inv)
moreover have "(s', t') ∈ gtt_lang G" using calculation
by (auto simp: Restr_rtrancl_gtt_lang_eq_trancl_gtt_lang[symmetric] gtt_lang_join)
ultimately show "(s, t) ∈ (gtt_lang G)⇧+" by (meson trancl.trancl_into_trancl trancl_trans)
qed (auto intro!: trancl_gtt_lang_arg_closed)
then show ?thesis by (auto simp: gtt_accept_def)
qed

lemma GTT_trancl_alang:
"agtt_lang (GTT_trancl G) = gtrancl_rel UNIV (agtt_lang G)"
using GTT_trancl_asound GTT_trancl_acomplete by blast

lemma GTT_trancl_lang:
"gtt_lang (GTT_trancl G) = (gtt_lang G)⇧+"
using GTT_trancl_sound GTT_trancl_complete by blast

end```