# 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```