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