Theory Regular_Tree_Relations.Ground_Closure

theory Ground_Closure
  imports Ground_Terms
begin

subsubsection ‹Multihole context closure›

text ‹Computing the multihole context closure of a given relation›
inductive_set gmctxt_cl :: "('f × nat) set ⇒ 'f gterm rel ⇒ 'f gterm rel" for ℱ ℛ where
  base [intro]: "(s, t) ∈ ℛ ⟹ (s, t) ∈ gmctxt_cl ℱ ℛ"
| step [intro]: "length ss = length ts ⟹ (∀ i < length ts. (ss ! i, ts ! i) ∈ gmctxt_cl ℱ ℛ) ⟹ (f, length ss) ∈ ℱ ⟹
    (GFun f ss, GFun f ts) ∈ gmctxt_cl ℱ ℛ"

lemma gmctxt_cl_idemp [simp]:
  "gmctxt_cl ℱ (gmctxt_cl ℱ ℛ) = gmctxt_cl ℱ ℛ"
proof -
  {fix s t assume "(s, t) ∈ gmctxt_cl ℱ (gmctxt_cl ℱ ℛ)"
    then have "(s, t) ∈ gmctxt_cl ℱ ℛ"
      by (induct) (auto intro: gmctxt_cl.step)}
  then show ?thesis by auto
qed

lemma gmctxt_cl_refl:
  "funas_gterm t ⊆ ℱ ⟹ (t, t) ∈ gmctxt_cl ℱ ℛ"
  by (induct t) (auto simp: SUP_le_iff intro!: gmctxt_cl.step)

lemma gmctxt_cl_swap:
  "gmctxt_cl ℱ (prod.swap ` ℛ) = prod.swap ` gmctxt_cl ℱ ℛ" (is "?Ls = ?Rs")
proof -
  {fix s t assume "(s, t) ∈ ?Ls" then have "(s, t) ∈ ?Rs"
      by induct auto}
  moreover
  {fix s t assume "(s, t) ∈ ?Rs"
    then have "(t, s) ∈ gmctxt_cl ℱ ℛ" by auto
    then have "(s, t) ∈ ?Ls" by induct auto}
  ultimately show ?thesis by auto
qed

lemma gmctxt_cl_mono_funas:
  assumes "ℱ ⊆ 𝒢" shows "gmctxt_cl ℱ ℛ ⊆ gmctxt_cl 𝒢 ℛ"
proof -
  {fix s t assume "(s, t) ∈ gmctxt_cl ℱ ℛ" then have "(s, t) ∈ gmctxt_cl 𝒢 ℛ"
      by induct (auto simp: subsetD[OF assms])}
  then show ?thesis by auto
qed

lemma gmctxt_cl_mono_rel:
  assumes "𝒫 ⊆ ℛ" shows "gmctxt_cl ℱ 𝒫 ⊆ gmctxt_cl ℱ ℛ"
proof -
  {fix s t assume "(s, t) ∈ gmctxt_cl ℱ 𝒫" then have "(s, t) ∈ gmctxt_cl ℱ ℛ" using assms
      by induct auto}
  then show ?thesis by auto
qed

definition gcomp_rel :: "('f × nat) set ⇒ 'f gterm rel ⇒ 'f gterm rel ⇒ 'f gterm rel" where
  "gcomp_rel ℱ R S = (R O gmctxt_cl ℱ S) ∪ (gmctxt_cl ℱ R O S)"

definition gtrancl_rel :: "('f × nat) set ⇒ 'f gterm rel ⇒ 'f gterm rel" where
  "gtrancl_rel ℱ ℛ = (gmctxt_cl ℱ ℛ)⇧+ O ℛ O (gmctxt_cl ℱ ℛ)⇧+"

lemma gcomp_rel:
  "gmctxt_cl ℱ (gcomp_rel ℱ ℛ 𝒮) = gmctxt_cl ℱ ℛ O gmctxt_cl ℱ 𝒮" (is "?Ls = ?Rs")
proof
  { fix s u assume "(s, u) ∈ gmctxt_cl ℱ (ℛ O gmctxt_cl ℱ 𝒮 ∪ gmctxt_cl ℱ ℛ O 𝒮)"
     then have "∃t. (s, t) ∈ gmctxt_cl ℱ ℛ ∧ (t, u) ∈ gmctxt_cl ℱ 𝒮"
    proof (induct)
      case (step ss ts f)
      from Ex_list_of_length_P[of _ "λ u i. (ss ! i, u) ∈ gmctxt_cl ℱ ℛ ∧ (u, ts ! i) ∈ gmctxt_cl ℱ 𝒮"]
      obtain us where l: "length us = length ts" and
        inv: "∀ i < length ts. (ss ! i, us ! i) ∈ gmctxt_cl ℱ ℛ ∧ (us ! i, ts ! i) ∈ gmctxt_cl ℱ 𝒮"
        using step(2, 3) by blast
      then show ?case using step(1, 3)
        by (intro exI[of _ "GFun f us"]) auto
    qed auto}
  then show "?Ls ⊆ ?Rs" unfolding gcomp_rel_def
    by auto
next
  {fix s t u assume "(s, t) ∈ gmctxt_cl ℱ ℛ" "(t, u) ∈ gmctxt_cl ℱ 𝒮"
    then have "(s, u) ∈ gmctxt_cl ℱ (ℛ O gmctxt_cl ℱ 𝒮 ∪ gmctxt_cl ℱ ℛ O 𝒮)"
    proof (induct arbitrary: u rule: gmctxt_cl.induct)
      case (step ss ts f)
      then show ?case
      proof (cases "(GFun f ts, u) ∈ 𝒮")
        case True
        then have "(GFun f ss, u) ∈ gmctxt_cl ℱ ℛ O 𝒮" using gmctxt_cl.step[OF step(1) _ step(3)] step(2)
          by auto
        then show ?thesis by auto
      next
        case False
        then obtain us where u[simp]: "u = GFun f us" and l: "length ts = length us"
          using step(4) by (cases u) (auto elim: gmctxt_cl.cases)
        have "i < length us ⟹
         (ss ! i, us ! i) ∈ gmctxt_cl ℱ (ℛ O gmctxt_cl ℱ 𝒮 ∪ gmctxt_cl ℱ ℛ O 𝒮)" for i
          using step(1, 2, 4) False by (auto elim: gmctxt_cl.cases)
        then show ?thesis using l step(1, 3)
          by auto
      qed
    qed auto}
  then show "?Rs ⊆ ?Ls"
    by (auto simp: gcomp_rel_def)
qed

subsubsection ‹Signature closed property›

definition all_ctxt_closed :: "('f × nat) set ⇒ 'f gterm rel ⇒ bool" where
  "all_ctxt_closed F r ⟷ (∀ f ts ss. (f, length ss) ∈ F ⟶ length ss = length ts ⟶
    (∀i. i < length ts ⟶ (ss ! i, ts ! i) ∈ r) ⟶
    (GFun f ss, GFun f ts) ∈ r)"

lemma all_ctxt_closedI:
  assumes "⋀ f ss ts. (f, length ss) ∈ ℱ ⟹ length ss = length ts ⟹
     (∀ i < length ts. (ss ! i, ts ! i) ∈ r) ⟹ (GFun f ss, GFun f ts) ∈ r"
  shows "all_ctxt_closed ℱ r" using assms
  unfolding all_ctxt_closed_def by auto

lemma all_ctxt_closedD:
  "all_ctxt_closed F r ⟹ (f, length ss) ∈ F ⟹ length ss = length ts ⟹
    (∀ i < length ts. (ss ! i, ts ! i) ∈ r) ⟹ (GFun f ss, GFun f ts) ∈ r"
  by (auto simp: all_ctxt_closed_def)

lemma all_ctxt_closed_refl_on:
  assumes "all_ctxt_closed ℱ r" "s ∈ 𝒯⇩G ℱ"
  shows "(s, s) ∈ r" using assms(2)
  by (induct) (auto simp: all_ctxt_closedD[OF assms(1)])

lemma gmctxt_cl_is_all_ctxt_closed [simp]:
  "all_ctxt_closed ℱ (gmctxt_cl ℱ ℛ)"
  unfolding all_ctxt_closed_def
  by auto

lemma all_ctxt_closed_gmctxt_cl_idem [simp]:
  assumes "all_ctxt_closed ℱ ℛ"
  shows "gmctxt_cl ℱ ℛ = ℛ"
proof -
  {fix s t assume "(s, t) ∈ gmctxt_cl ℱ ℛ" then have "(s, t) ∈ ℛ"
    proof (induct)
      case (step ss ts f)
      show ?case using step(2) all_ctxt_closedD[OF assms step(3, 1)]
        by auto
    qed auto}
  then show ?thesis by auto
qed


subsubsection ‹Transitive closure preserves @{const all_ctxt_closed}›

text ‹induction scheme for transitive closures of lists›

inductive_set trancl_list for ℛ where
  base[intro, Pure.intro] : "length xs = length ys ⟹
      (∀ i < length ys. (xs ! i, ys ! i) ∈ ℛ) ⟹ (xs, ys) ∈ trancl_list ℛ"
| list_trancl [Pure.intro]: "(xs, ys) ∈ trancl_list ℛ ⟹ i < length ys ⟹ (ys ! i, z) ∈ ℛ ⟹
    (xs, ys[i := z]) ∈ trancl_list ℛ"

lemma trancl_list_appendI [simp, intro]:
  "(xs, ys) ∈ trancl_list ℛ ⟹ (x, y) ∈ ℛ ⟹ (x # xs, y # ys) ∈ trancl_list ℛ"
proof (induct rule: trancl_list.induct)
  case (base xs ys)
  then show ?case using less_Suc_eq_0_disj
    by (intro trancl_list.base) auto
next
  case (list_trancl xs ys i z)
  from list_trancl(3) have *: "y # ys[i := z] = (y # ys)[Suc i := z]" by auto
  show ?case using list_trancl unfolding *
    by (intro trancl_list.list_trancl) auto
qed

lemma trancl_list_append_tranclI [intro]:
  "(x, y) ∈ ℛ⇧+ ⟹ (xs, ys) ∈ trancl_list ℛ ⟹ (x # xs, y # ys) ∈ trancl_list ℛ"
proof (induct rule: trancl.induct)
  case (trancl_into_trancl a b c)
  then have "(a # xs, b # ys) ∈ trancl_list ℛ" by auto
  from trancl_list.list_trancl[OF this, of 0 c]
  show ?case using trancl_into_trancl(3)
    by auto
qed auto

lemma trancl_list_conv:
  "(xs, ys) ∈ trancl_list ℛ ⟷ length xs = length ys ∧ (∀ i < length ys. (xs ! i, ys ! i) ∈ ℛ⇧+)" (is "?Ls ⟷ ?Rs")
proof
  assume "?Ls" then show ?Rs
  proof (induct)
    case (list_trancl xs ys i z)
    then show ?case
      by auto (metis nth_list_update trancl.trancl_into_trancl)
  qed auto
next
  assume ?Rs then show ?Ls
  proof (induct ys arbitrary: xs)
    case Nil
    then show ?case by (cases xs) auto
  next
    case (Cons y ys)
    from Cons(2) obtain x xs' where *: "xs = x # xs'" and
      inv: "(x, y) ∈ ℛ⇧+"
      by (cases xs) auto
    show ?case using Cons(1)[of "tl xs"] Cons(2) unfolding *
      by (intro trancl_list_append_tranclI[OF inv]) force
  qed
qed

lemma trancl_list_induct [consumes 2, case_names base step]:
  assumes "length ss = length ts" "∀ i < length ts. (ss ! i, ts ! i) ∈ ℛ⇧+"
    and "⋀xs ys. length xs = length ys ⟹ ∀ i < length ys. (xs ! i, ys ! i) ∈ ℛ ⟹ P xs ys"
    and "⋀xs ys i z. length xs = length ys ⟹ ∀ i < length ys. (xs ! i, ys ! i) ∈ ℛ⇧+ ⟹ P xs ys
      ⟹ i < length ys ⟹ (ys ! i, z) ∈ ℛ ⟹ P xs (ys[i := z])"
  shows "P ss ts" using assms
  by (intro trancl_list.induct[of ss ts ℛ P]) (auto simp: trancl_list_conv)

lemma trancl_list_all_step_induct [consumes 2, case_names base step]:
  assumes "length ss = length ts" "∀ i < length ts. (ss ! i, ts ! i) ∈ ℛ⇧+"
    and base: "⋀xs ys. length xs = length ys ⟹ ∀ i < length ys. (xs ! i, ys ! i) ∈ ℛ ⟹ P xs ys"
    and steps: "⋀xs ys zs. length xs = length ys ⟹ length ys = length zs ⟹
       ∀ i < length zs. (xs ! i, ys ! i) ∈ ℛ⇧+ ⟹ ∀ i < length zs. (ys ! i, zs ! i) ∈ ℛ ∨ ys ! i = zs ! i ⟹
       P xs ys ⟹ P xs zs"
  shows "P ss ts" using assms(1, 2)
proof (induct rule: trancl_list_induct)
case (step xs ys i z)
  then show ?case
    by (intro steps[of xs ys "ys[i := z]"])
       (auto simp: nth_list_update)
qed (auto simp: base)

lemma all_ctxt_closed_trancl:
  assumes  "all_ctxt_closed ℱ ℛ" "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
  shows "all_ctxt_closed ℱ (ℛ⇧+)"
proof -
  {fix f ss ts assume sig: "(f, length ss) ∈ ℱ" and
      steps: "length ss = length ts" "∀i<length ts. (ss ! i, ts ! i) ∈ ℛ⇧+"
    have "(GFun f ss, GFun f ts) ∈ ℛ⇧+" using steps sig
    proof (induct rule: trancl_list_induct)
      case (base ss ts)
      then show ?case using all_ctxt_closedD[OF assms(1) base(3, 1, 2)]
        by auto
    next
      case (step ss ts i t')
      from step(2) have "j < length ts ⟹ ts ! j ∈ 𝒯⇩G ℱ" for j using assms(2)
        by (metis (no_types, lifting) SigmaD2 subset_iff trancl.simps)
      from this[THEN all_ctxt_closed_refl_on[OF assms(1)]]
      have "(GFun f ts, GFun f (ts[i := t'])) ∈ ℛ" using step(1, 4-)
        by (intro all_ctxt_closedD[OF assms(1)]) (auto simp: nth_list_update)
      then show ?case using step(3, 6)
        by auto
    qed}
  then show ?thesis by (intro all_ctxt_closedI)
qed

end