Theory GTT_Transitive_Closure

theory GTT_Transitive_Closure
  imports GTT_Compose
begin

inductive_set Δ_trancl :: "('q, 'f) ta ⇒ ('q, 'f) ta ⇒ ('q × 'q) set" for A B where
  Δ_cong: "f ps → p ∈ ta_rules A ⟹ f qs → q ∈ ta_rules B ⟹ length ps = length qs ⟹
   (⋀i. i < length qs ⟹ (ps ! i, qs ! i) ∈ Δ_trancl A B) ⟹ (p, q) ∈ Δ_trancl A B"
| Δ_eps1: "(p, p') ∈ ta_eps A ⟹ (p, q) ∈ Δ_trancl A B ⟹ (p', q) ∈ Δ_trancl A B"
| Δ_eps2: "(q, q') ∈ ta_eps B ⟹ (p, q) ∈ Δ_trancl A B ⟹ (p, q') ∈ Δ_trancl A B"
| Δ_trans: "(p, q) ∈ Δ_trancl A B ⟹ (q, r) ∈ Δ_trancl A B ⟹ (p, r) ∈ Δ_trancl A B"

definition GTT_trancl where
  "GTT_trancl G = (ta.make {} (ta_rules (fst G)) (ta_eps (fst G) ∪ Δ_trancl (snd G) (fst G)),
                   ta.make {} (ta_rules (snd G)) (ta_eps (snd G) ∪ Δ_trancl (fst G) (snd G)))"

lemma Δ_trancl_subset_states:
  "Δ_trancl A B ⊆ ta_states A × ta_states B"
  apply standard
  subgoal for p q by (induct rule: Δ_trancl.induct)
    (auto simp: ta_states_def r_states_def r_rhs_def split: prod.splits ta_rule.splits)
  done

lemma gtt_syms_GTT_trancl:
  "gtt_syms (GTT_trancl G) = gtt_syms G"
  by (auto simp: GTT_trancl_def ta_syms_def)

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_trancl_base:
  "gtt_lang G ⊆ gtt_lang (GTT_trancl G)"
  using gtt_accept_mono[of G "GTT_trancl G"] by (auto simp: 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.make {} (ta_rules A) (ta_eps A ∪ Δ_trancl B A))
    (ta.make {} (ta_rules B) (ta_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 (auto intro!: gtt_accept_mono[of "GTT_comp (GTT_trancl G) (GTT_trancl G)" "GTT_trancl G"])
      (auto simp: GTT_comp_def GTT_trancl_def)
qed

lemma Restr_rtrancl_gtt_lang_eq_trancl_gtt_lang:
  "Restr ((gtt_lang G)⇧*) {t. ground t} = (gtt_lang G)⇧+"
  by (auto simp: rtrancl_trancl_reflcl simp del: reflcl_trancl dest: tranclD tranclD2)

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 gtt_lang_ground_ctxt_closed:
  assumes "ground_ctxt C" "(s, t) ∈ gtt_lang 𝒢"
  shows "(C⟨s⟩, C⟨t⟩) ∈ gtt_lang 𝒢"
proof -
  { fix i s and ss1 ss2 :: "('f, 'v) term list" assume "i < Suc (length ss1 + length ss2)"
    then have "fill_holes ((map mctxt_of_term ss1 @ MHole # map mctxt_of_term ss2) ! i)
     ((replicate (length ss1) [] @ [s] # replicate (length ss2) []) ! i) = (ss1 @ s # ss2) ! i"
      by (cases "i = length ss1") (auto simp del: upt_Suc simp: nth_append) (* slow *)
  } note [simp] = this
  have *: "fill_holes (MFun f (map mctxt_of_term ss1 @ MHole # map mctxt_of_term ss2)) [s] = Fun f (ss1 @ s # ss2)"
    for f ss1 s ss2 by (auto simp del: upt_Suc intro!: nth_equalityI)
  then have "ctxt.closed {(s, t). gtt_accept 𝒢 s t}"
    using accept'_closed_ctxt[of "[_]" "[_]" 𝒢 "MFun _ ((map mctxt_of_term _) @ MHole # (map mctxt_of_term _))"]
    unfolding * by (auto simp: gtt_accept_equiv intro!: one_imp_ctxt_closed)
  then show ?thesis using assms by auto
qed

lemma gtt_langs_ground_ctxt_closed:
  assumes "ground_ctxt C" "(s, t) ∈ (gtt_lang 𝒢)⇧*"
  shows "(C⟨s⟩, C⟨t⟩) ∈ (gtt_lang 𝒢)⇧*"
  using assms(2) gtt_lang_ground_ctxt_closed[OF assms(1), of _ _ 𝒢]
  by (induct rule: rtrancl_induct) (auto intro: rtrancl.intros(2))

(* move *)
lemma ground_ctxt_closed_imp_ground_mctxt_closed:
  assumes "⋀C s t. ground_ctxt C ⟹ (s, t) ∈ R⇧* ⟹ (C⟨s⟩, C⟨t⟩) ∈ R⇧*"
    "length ss = num_holes C" "length ts = num_holes C" "ground_mctxt C"
    "⋀i. i < num_holes C ⟹ (ss ! i, ts ! i) ∈ Restr (R⇧*) {t. ground t}"
  shows "(fill_holes C ss, fill_holes C ts) ∈ R⇧*"
proof -
  have "i ≤ num_holes C ⟹ (fill_holes C ss, fill_holes C (take i ts @ drop i ss)) ∈ R⇧*" for i
  proof (induct i)
    case (Suc i)
    have "num_holes C = Suc (length (take i ts) + length (drop (Suc i) ss))"
      using Suc(2) assms(2,3) by auto
    from fill_holes_ctxt_main[OF this]
    obtain D where [simp]: "⋀s. D⟨s⟩ = fill_holes C (take i ts @ s # drop (Suc i) ss)" by metis
    have [simp]: "take i ts @ ss ! i # drop (Suc i) ss = take i ts @ drop i ss"
      "take i ts @ ts ! i # drop (Suc i) ss = take (Suc i) ts @ drop (Suc i) ss"
      using Suc(2) assms(2,3)
      by (simp_all add: Cons_nth_drop_Suc Suc.prems Suc_le_lessD assms(3) take_Suc_conv_app_nth)
    have "ground D⟨ss ! i⟩" using assms(2-5) by (auto simp: ground_fill_holes in_set_conv_nth)
    then have "ground_ctxt D" by (metis ground_ctxt_apply)
    then show ?case using Suc(1,2) assms(1)[of D "ss ! i" "ts ! i"] assms(5) by auto
  qed auto
  from this[of "num_holes C"] show ?thesis using assms(2,3) by auto
qed

(* move *)
lemma partition_by_singles:
  "length xs = n ⟹ partition_by xs (replicate n (Suc 0)) = map (λx. [x]) xs"
  by (induct xs arbitrary: n) auto

(* move *)
lemma map_nth':
  "length xs = n ⟹ map ((!) xs) [0..<n] = xs"
  by (auto simp: map_nth)

(* move *)
lemma ground_ctxt_closed_imp_arg_closed:
  assumes "⋀C s t. ground_ctxt C ⟹ (s, t) ∈ R⇧* ⟹ (C⟨s⟩, C⟨t⟩) ∈ R⇧*"
    "length ss = length ts"
    "⋀i. i < length ts ⟹ (ss ! i, ts ! i) ∈ Restr (R⇧*) {t. ground t}"
  shows "(Fun f ss, Fun f ts) ∈ R⇧*"
  using ground_ctxt_closed_imp_ground_mctxt_closed[of R ss "MFun f (replicate (length ts) MHole)" ts]
    assms(2,3) by (auto simp: assms(1) partition_by_singles map_nth' cong: list.map_cong_simp)

lemma trancl_gtt_lang_arg_closed:
  assumes "length ss = length ts" "∀i < length ts. (ss ! i, ts ! i) ∈ (gtt_lang 𝒢)⇧+"
  shows "(Fun f ss, Fun f ts) ∈ (gtt_lang 𝒢)⇧+"
  using assms(1,2) ground_ctxt_closed_imp_arg_closed[OF _ assms(1), of "gtt_lang 𝒢"]
  by (auto simp: gtt_langs_ground_ctxt_closed in_set_conv_nth Restr_rtrancl_gtt_lang_eq_trancl_gtt_lang[symmetric])

lemma Δ_trancl_sound:
  assumes "(p, q) ∈ Δ_trancl A B"
  obtains s t where "(s, t) ∈ (gtt_lang (B, A))⇧+" "p ∈ ta_res A s" "q ∈ ta_res 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 ∈ ta_res A (si) ∧
      qs ! i ∈ ta_res 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 ∈ ta_res A (ss i) ∧ qs ! i ∈ ta_res B (ts i)" by metis
  then show ?case using Δ_cong(1-5)
    by (intro Δ_cong(6)[of "Fun f (map ss [0..<length ps])" "Fun f (map ts [0..<length qs])"])
      (auto intro!: trancl_gtt_lang_arg_closed)
next
  case (Δ_eps1 p p' q) then show ?case by (metis r_into_rtrancl ta_res_eps)
next
  case (Δ_eps2 q q' p) then show ?case by (metis r_into_rtrancl ta_res_eps)
next
  case (Δ_trans p q r)
  guess s1 t1 using Δ_trans(2) . note 1 = this
  guess s2 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])
  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 ∈ ta_res (ta.make {} (ta_rules A) (ta_eps A ∪ Δ_trancl B A)) s" "ground s"
  shows "∃t. (s, t) ∈ (gtt_lang (A, B))⇧+ ∧ p ∈ ta_res A t"
  using assms
proof (induct s arbitrary: p)
  case (Fun f ss)
  obtain qs q where q: "f qs → q ∈ ta_rules A" "(q, p) ∈ (ta_eps A ∪ Δ_trancl B A)⇧*" "length qs = length ss"
   "⋀i. i < length ss ⟹ qs ! i ∈ ta_res (ta.make {} (ta_rules A) (ta_eps A ∪ Δ_trancl B A)) (ss ! i)"
    using Fun(2) by auto
  have "⋀i. i < length ss ⟹ ∃ti. (ss ! i, ti) ∈ (gtt_lang (A, B))⇧+ ∧ qs ! i ∈ ta_res A (ti)"
    using Fun(1)[OF nth_mem q(4)] Fun(3) by fastforce
  then obtain ts where ts: "⋀i. i < length ss ⟹ (ss ! i, ts i) ∈ (gtt_lang (A, B))⇧+ ∧ qs ! i ∈ ta_res A (ts i)"
    by metis
  show ?case using q(2)
  proof (induct rule: rtrancl_induct)
    case base then show ?case using ts q(1,3)
      by (auto intro!: trancl_gtt_lang_arg_closed exI[of _ "Fun f (map ts [0..<length ss])"] exI[of _ qs] exI[of _ q])
  next
    case (step p p')
    guess s' using step(3) .. note s' = this
    show ?case using step(2)
    proof
      assume "(p, p') ∈ ta_eps A" then show ?thesis using s'
        by (auto intro!: exI[of _ s'] simp: r_into_rtrancl ta_res_eps)
    next
      assume "(p, p') ∈ Δ_trancl B A"
      from Δ_trancl_sound[OF this] guess s t . note st = this
      have "(s', s) ∈ gtt_lang (A, B)" using st s'
        by (auto simp: Restr_rtrancl_gtt_lang_eq_trancl_gtt_lang[symmetric])
      then have "(Fun f ss, t) ∈ (gtt_lang (A, B))⇧+"
        using s' st(1) by (meson trancl.trancl_into_trancl trancl_trans)
      then show ?thesis using st(3) by auto
    qed
  qed
qed auto

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 ⟹ ground s ⟹ ground t ⟹ (s, t) ∈ (gtt_lang G)⇧+" for s t
  proof (induct rule: gtt_accept.induct)
    case (join q s t)
    obtain s' where "(s, s') ∈ (gtt_lang G)⇧+" "q ∈ ta_res (fst G) s'" using join(1,3)
      by (auto simp: GTT_trancl_def)
    moreover obtain t' where "(t', t) ∈ (gtt_lang G)⇧+" "q ∈ ta_res (snd G) t'" using join(2,4)
      by (auto simp: GTT_trancl_def gtt_lang_swap[of "fst G" "snd G", symmetric] trancl_converse)
    moreover have "(s', t') ∈ gtt_lang G" using calculation
      by (auto simp: Restr_rtrancl_gtt_lang_eq_trancl_gtt_lang[symmetric])
    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
qed

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

end