# Theory Lift_Root_Step

```section ‹Lifting root steps to single/parallel root/non-root steps›
theory Lift_Root_Step
imports
Rewriting
FOR_Certificate
Context_Extensions
Multihole_Context
begin

text ‹Closure under all contexts›
abbreviation "gctxtcl ℛ ≡ gctxtex_onp (λ C. True) ℛ"
abbreviation "gmctxtcl ℛ ≡ gctxtex_onp (λ C. True) ℛ"

text ‹Extension under all non empty contexts›
abbreviation "gctxtex_nempty ℛ ≡ gctxtex_onp (λ C. C ≠ □⇩G) ℛ"
abbreviation "gmctxtex_nempty ℛ ≡ gmctxtex_onp (λ C. C ≠ GMHole) ℛ"

text ‹Closure under all contexts respecting the signature›
abbreviation "gctxtcl_funas ℱ ℛ ≡ gctxtex_onp (λ C. funas_gctxt C ⊆ ℱ) ℛ"
abbreviation "gmctxtcl_funas ℱ ℛ ≡ gmctxtex_onp (λ C. funas_gmctxt C ⊆ ℱ) ℛ"

text ‹Closure under all multihole contexts with at least one hole respecting the signature›
abbreviation "gmctxtcl_funas_strict ℱ ℛ ≡ gmctxtex_onp (λ C. 0 < num_gholes C ∧ funas_gmctxt C ⊆ ℱ) ℛ"

text ‹Extension under all non empty contexts respecting the signature›
abbreviation "gctxtex_funas_nroot ℱ ℛ ≡ gctxtex_onp (λ C. funas_gctxt C ⊆ ℱ ∧ C ≠ □⇩G) ℛ"
abbreviation "gmctxtex_funas_nroot ℱ ℛ ≡ gmctxtex_onp (λ C. funas_gmctxt C ⊆ ℱ ∧ C ≠ GMHole) ℛ"

text ‹Extension under all non empty contexts respecting the signature›
abbreviation "gmctxtex_funas_nroot_strict ℱ ℛ ≡
gmctxtex_onp (λ C.  0 < num_gholes C ∧ funas_gmctxt C ⊆ ℱ ∧ C ≠ GMHole) ℛ"

subsection ‹Rewrite steps equivalent definitions›

definition gsubst_cl :: "('f, 'v) trs ⇒ 'f gterm rel" where
"gsubst_cl ℛ = {(gterm_of_term (l ⋅ σ), gterm_of_term (r ⋅ σ)) |
l r (σ :: 'v ⇒ ('f, 'v) Term.term). (l, r) ∈ ℛ ∧ ground (l ⋅ σ) ∧ ground (r ⋅ σ)}"

definition gnrrstepD :: "'f sig ⇒ 'f gterm rel ⇒ 'f gterm rel" where
"gnrrstepD ℱ ℛ = gctxtex_funas_nroot ℱ ℛ"

definition grstepD :: "'f sig ⇒ 'f gterm rel ⇒ 'f gterm rel" where
"grstepD ℱ ℛ = gctxtcl_funas ℱ ℛ"

definition gpar_rstepD :: "'f sig ⇒ 'f gterm rel ⇒ 'f gterm rel" where
"gpar_rstepD ℱ ℛ = gmctxtcl_funas ℱ ℛ"

inductive_set gpar_rstepD' :: "'f sig ⇒ 'f gterm rel ⇒ 'f gterm rel" for ℱ :: "'f sig" and ℛ :: "'f gterm rel"
where groot_step [intro]: "(s, t) ∈ ℛ ⟹ (s, t) ∈ gpar_rstepD' ℱ ℛ"
|  gpar_step_fun [intro]: "⟦⋀ i. i < length ts ⟹ (ss ! i, ts ! i) ∈ gpar_rstepD' ℱ ℛ⟧ ⟹ length ss = length ts
⟹ (f, length ts) ∈ ℱ ⟹ (GFun f ss, GFun f ts) ∈ gpar_rstepD' ℱ ℛ"

subsection ‹Interface between rewrite step definitions and sets›

fun lift_root_step :: "('f × nat) set ⇒ pos_step ⇒ ext_step ⇒ 'f gterm rel ⇒ 'f gterm rel" where
"lift_root_step ℱ PAny ESingle ℛ = gctxtcl_funas ℱ ℛ"
| "lift_root_step ℱ PAny EStrictParallel ℛ = gmctxtcl_funas_strict ℱ ℛ"
| "lift_root_step ℱ PAny EParallel ℛ = gmctxtcl_funas ℱ ℛ"
| "lift_root_step ℱ PNonRoot ESingle ℛ = gctxtex_funas_nroot ℱ ℛ"
| "lift_root_step ℱ PNonRoot EStrictParallel ℛ = gmctxtex_funas_nroot_strict ℱ ℛ"
| "lift_root_step ℱ PNonRoot EParallel ℛ = gmctxtex_funas_nroot ℱ ℛ"
| "lift_root_step ℱ PRoot ESingle ℛ = ℛ"
| "lift_root_step ℱ PRoot EStrictParallel ℛ = ℛ"
| "lift_root_step ℱ PRoot EParallel ℛ = ℛ ∪ Restr Id (𝒯⇩G ℱ)"

subsection ‹Compatibility of used predicate extensions and signature closure›

lemma compatible_p [simp]:
"compatible_p (λ C. C ≠ □⇩G) (λ C. C ≠ GMHole)"
"compatible_p (λ C. funas_gctxt C ⊆ ℱ) (λ C. funas_gmctxt C ⊆ ℱ)"
"compatible_p (λ C. funas_gctxt C ⊆ ℱ ∧ C ≠ □⇩G) (λ C. funas_gmctxt C ⊆ ℱ ∧ C ≠ GMHole)"
unfolding compatible_p_def
by rule (case_tac C, auto)+

lemma gmctxtcl_funas_sigcl:
"all_ctxt_closed ℱ (gmctxtcl_funas ℱ ℛ)"
by (intro gmctxtex_onp_sig_closed) auto

lemma gctxtex_funas_nroot_sigcl:
"all_ctxt_closed ℱ (gmctxtex_funas_nroot ℱ ℛ)"
by (intro gmctxtex_onp_sig_closed) auto

lemma gmctxtcl_funas_strict_funcl:
"function_closed ℱ (gmctxtcl_funas_strict ℱ ℛ)"
by (intro gmctxtex_onp_fun_closed) (auto dest: list.set_sel)

lemma gmctxtex_funas_nroot_strict_funcl:
"function_closed ℱ (gmctxtex_funas_nroot_strict ℱ ℛ)"
by (intro gmctxtex_onp_fun_closed) (auto dest: list.set_sel)

lemma gctxtcl_funas_dist:
"gctxtcl_funas ℱ ℛ = gctxtex_onp (λ C. C = □⇩G) ℛ ∪ gctxtex_funas_nroot ℱ ℛ"
by (intro gctxtex_onp_pred_dist) auto

lemma gmctxtex_funas_nroot_dist:
"gmctxtex_funas_nroot ℱ ℛ = gmctxtex_funas_nroot_strict ℱ ℛ ∪
gmctxtex_onp (λ C. num_gholes C = 0 ∧ funas_gmctxt C ⊆ ℱ) ℛ"
by (intro gmctxtex_onp_pred_dist) auto

lemma gmctxtcl_funas_dist:
"gmctxtcl_funas ℱ ℛ = gmctxtex_onp (λ C. num_gholes C = 0 ∧ funas_gmctxt C ⊆ ℱ) ℛ ∪
gmctxtex_onp (λ C. 0 < num_gholes C ∧ funas_gmctxt C ⊆ ℱ) ℛ"
by (intro gmctxtex_onp_pred_dist) auto

lemma gmctxtcl_funas_strict_dist:
"gmctxtcl_funas_strict ℱ ℛ = gmctxtex_funas_nroot_strict ℱ ℛ ∪ gmctxtex_onp (λ C. C = GMHole) ℛ"
by (intro gmctxtex_onp_pred_dist) auto

lemma gmctxtex_onpzero_num_gholes_id [simp]:
"gmctxtex_onp (λ C. num_gholes C = 0 ∧ funas_gmctxt C ⊆ ℱ) ℛ = Restr Id (𝒯⇩G ℱ)" (is "?Ls = ?Rs")
proof -
{fix s t assume "(s, t) ∈ ?Ls" from gmctxtex_onpE[OF this] obtain C us vs where
*: "s = fill_gholes C us" "t = fill_gholes C vs" and
len: "num_gholes C = length us" "length us = length vs" and
inv: "num_gholes C = 0 ∧ funas_gmctxt C ⊆ ℱ" by auto
then have "(s, t) ∈ ?Rs" using len inv unfolding *
by (cases us; cases vs) (auto simp: 𝒯⇩G_funas_gterm_conv)}
moreover have "?Rs ⊆ ?Ls"
by (intro Restr_id_subset_gmctxtex_onp) auto
ultimately show ?thesis by auto
qed

lemma gctxtex_onp_sign_trans_fst:
assumes "(s, t) ∈ gctxtex_onp P R" and "s ∈ 𝒯⇩G ℱ"
shows "(s, t) ∈ gctxtex_onp (λ C. funas_gctxt C ⊆ ℱ ∧ P C) R"
using assms
by (auto simp: 𝒯⇩G_equivalent_def elim!: gctxtex_onpE)

lemma gctxtex_onp_sign_trans_snd:
assumes "(s, t) ∈ gctxtex_onp P R" and "t ∈ 𝒯⇩G ℱ"
shows "(s, t) ∈ gctxtex_onp (λ C. funas_gctxt C ⊆ ℱ ∧ P C) R"
using assms
by (auto simp: 𝒯⇩G_equivalent_def elim!: gctxtex_onpE)

lemma gmctxtex_onp_sign_trans_fst:
assumes "(s, t) ∈ gmctxtex_onp P R" and "s ∈ 𝒯⇩G ℱ"
shows "(s, t) ∈ gmctxtex_onp (λ C. P C ∧ funas_gmctxt C ⊆ ℱ) R"
using assms
by (auto simp: 𝒯⇩G_equivalent_def simp add: gmctxtex_onpI)

lemma gmctxtex_onp_sign_trans_snd:
assumes "(s, t) ∈ gmctxtex_onp P R" and "t ∈ 𝒯⇩G ℱ"
shows "(s, t) ∈ gmctxtex_onp (λ C. P C ∧ funas_gmctxt C ⊆ ℱ) R"
using assms
by (auto simp: 𝒯⇩G_equivalent_def simp add: gmctxtex_onpI)

subsection ‹Basic lemmas›

lemma gsubst_cl:
fixes ℛ :: "('f, 'v) trs" and σ :: "'v ⇒ ('f, 'v) term"
assumes "(l, r) ∈ ℛ" and "ground (l ⋅ σ)" "ground (r ⋅ σ)"
shows "(gterm_of_term (l ⋅ σ), gterm_of_term (r ⋅ σ)) ∈ gsubst_cl ℛ"
using assms unfolding gsubst_cl_def by auto

lemma grstepD [simp]:
"(s, t) ∈ ℛ ⟹ (s, t) ∈ grstepD ℱ ℛ"
by (auto simp: grstepD_def gctxtex_onp_def intro!: exI[of _ "□⇩G"])

lemma grstepD_ctxtI [intro]:
"(l, r) ∈ ℛ ⟹ funas_gctxt C ⊆ ℱ ⟹ (C⟨l⟩⇩G, C⟨r⟩⇩G) ∈ grstepD ℱ ℛ"
by (auto simp: grstepD_def gctxtex_onp_def intro!: exI[of _ "C"])

lemma gctxtex_funas_nroot_gctxtcl_funas_subseteq:
"gctxtex_funas_nroot ℱ (grstepD ℱ ℛ) ⊆ grstepD ℱ ℛ"
unfolding grstepD_def
by (intro gctxtex_pred_cmp_subseteq) auto

lemma Restr_gnrrstepD_dist [simp]:
"Restr (gnrrstepD ℱ ℛ) (𝒯⇩G 𝒢) = gnrrstepD (ℱ ∩ 𝒢) (Restr ℛ (𝒯⇩G 𝒢))"

lemma Restr_grstepD_dist [simp]:
"Restr (grstepD ℱ ℛ) (𝒯⇩G 𝒢) = grstepD (ℱ ∩ 𝒢) (Restr ℛ (𝒯⇩G 𝒢))"

lemma Restr_gpar_rstepD_dist [simp]:
"Restr (gpar_rstepD ℱ ℛ) (𝒯⇩G 𝒢) = gpar_rstepD (ℱ ∩ 𝒢) (Restr ℛ (𝒯⇩G 𝒢))" (is "?Ls = ?Rs")
by (auto simp: gpar_rstepD_def)

subsection ‹Equivalence lemmas›

lemma grrstep_subst_cl_conv:
"grrstep ℛ = gsubst_cl ℛ"
unfolding gsubst_cl_def grrstep_def rrstep_def rstep_r_p_s_def
by (auto, metis ground_substI ground_term_of_gterm term_of_gterm_inv) blast

lemma gnrrstepD_gnrrstep_conv:
"gnrrstep ℛ = gnrrstepD UNIV (gsubst_cl ℛ)" (is "?Ls = ?Rs")
proof -
{fix s t assume "(s, t) ∈ ?Ls" then obtain l r C σ where
mem: "(l, r) ∈ ℛ" "C ≠ □" "term_of_gterm s = C⟨l ⋅ (σ :: 'b ⇒ ('a, 'b) term)⟩" "term_of_gterm t = C⟨r ⋅ σ⟩"
unfolding gnrrstep_def inv_image_def nrrstep_def' by auto
then have "(s, t) ∈ ?Rs" using gsubst_cl[OF mem(1)]
using gctxtex_onpI[of "λ C. funas_gctxt C ⊆ UNIV ∧ C ≠ □⇩G" "gctxt_of_ctxt C" "gterm_of_term (l ⋅ σ)"
"gterm_of_term (r ⋅ σ)" "gsubst_cl ℛ"]
by (auto simp: gnrrstepD_def)}
moreover
{fix s t assume "(s, t) ∈ ?Rs" then have "(s, t) ∈ ?Ls"
unfolding gnrrstepD_def gctxtex_onp_def gnrrstep_def inv_image_def nrrstep_def' gsubst_cl_def
by auto (metis ctxt_of_gctxt.simps(1) ctxt_of_gctxt_inv ground_ctxt_of_gctxt ground_gctxt_of_ctxt_apply ground_substI)}
ultimately show ?thesis by auto
qed

lemma grstepD_grstep_conv:
"grstep ℛ = grstepD UNIV (gsubst_cl ℛ)" (is "?Ls = ?Rs")
proof -
{fix s t assume "(s, t) ∈ ?Ls" then obtain C l r σ where
mem: "(l, r) ∈ ℛ" "term_of_gterm s = C⟨l ⋅ (σ :: 'b ⇒ ('a, 'b) term)⟩" "term_of_gterm t = C⟨r ⋅ σ⟩"
unfolding grstep_def inv_image_def by auto
then have "(s, t) ∈ ?Rs" using grstepD_ctxtI[OF gsubst_cl[OF mem(1)], of σ "gctxt_of_ctxt C" UNIV]
by (auto simp: grstepD_def gctxtex_onp_def)}
moreover
{fix s t assume "(s, t) ∈ ?Rs" then have "(s, t) ∈ ?Ls"
by (auto simp: gctxtex_onp_def grstepD_def grstep_def gsubst_cl_def)
(metis ctxt_of_gctxt_apply_gterm ground_ctxt_apply
ground_ctxt_of_gctxt ground_substI gterm_of_term_inv rstep.intros)}
ultimately show ?thesis by auto
qed

lemma gpar_rstep_gpar_rstepD_conv:
"gpar_rstep ℛ = gpar_rstepD' UNIV (gsubst_cl ℛ)" (is "?Ls = ?Rs")
proof -
{fix s t assume "(s, t) ∈ ?Rs"
then have "(s, t) ∈ gpar_rstep ℛ"
by induct (auto simp: gpar_rstep_def gsubst_cl_def)}
moreover
{fix s t assume ass: "(s, t) ∈ ?Ls" then obtain u v where
"(u, v) ∈ par_rstep ℛ" "u = term_of_gterm s" "v = term_of_gterm t"
then have "(s, t) ∈ ?Rs"
proof (induct arbitrary: s t)
case (root_step u v σ)
then have "(s, t) ∈ gsubst_cl ℛ" unfolding gsubst_cl_def
by auto (metis ground_substI ground_term_of_gterm term_of_gterm_inv)
then show ?case by auto
next
case (par_step_fun ts ss f)
then show ?case by (cases s; cases t) auto
next
case (par_step_var x)
then show ?case by (cases s) auto
qed}
ultimately show ?thesis by auto
qed

lemma gmctxtcl_funas_idem:
"gmctxtcl_funas ℱ (gmctxtcl_funas ℱ ℛ) ⊆ gmctxtcl_funas ℱ ℛ"
by (intro gmctxtex_pred_cmp_subseteq)
(auto elim!: less_eq_to_sup_mctxt_args, blast+)

lemma gpar_rstepD_gpar_rstepD'_conv:
"gpar_rstepD ℱ ℛ = gpar_rstepD' ℱ ℛ" (is "?Ls = ?Rs")
proof -
{fix s t assume "(s, t) ∈ ?Rs" then have "(s, t) ∈ ?Ls"
proof induct
case (groot_step s t) then show ?case unfolding gpar_rstepD_def
using gmctxtex_onpI[of _ GMHole  "[s]" "[t]"]
by auto
next
case (gpar_step_fun ts ss f)
show ?case using gpar_step_fun(2-) unfolding gpar_rstepD_def
using subsetD[OF gmctxtcl_funas_idem, of "(GFun f ss, GFun f ts)" ℱ ℛ]
using gmctxtex_onpI[of _ "GMFun f (replicate (length ss) GMHole)" ss ts "gmctxtcl_funas ℱ ℛ"]
by (auto simp del: fill_gholes.simps)
qed}
moreover
{fix s t assume "(s, t) ∈ ?Ls" then obtain C ss ts where
t: "s = fill_gholes C ss" "t = fill_gholes C ts" and
inv: "num_gholes C = length ss" "num_gholes C = length ts" and
pred: "funas_gmctxt C ⊆ ℱ" and rel: "∀ i < length ts. (ss ! i, ts ! i) ∈ ℛ"
unfolding gpar_rstepD_def by auto
have "(s, t) ∈ ?Rs" using inv pred rel unfolding t
proof (induct rule: fill_gholes_induct2)
case (GMHole x) then show ?case
by (cases ts) auto
next
case (GMFun f Cs xs ys)
from GMFun(1, 2, 5) have "i < length Cs ⟹ ∀ j < length (partition_gholes ys Cs ! i).
(partition_gholes xs Cs ! i ! j, partition_gholes ys Cs ! i ! j) ∈ ℛ" for i
by (auto simp: length_partition_by_nth partition_by_nth_nth(1, 2))
from GMFun this show ?case unfolding partition_holes_fill_gholes_conv'
by (intro gpar_step_fun) (auto, meson UN_I nth_mem subset_iff)
qed}
ultimately show ?thesis by auto
qed

subsection ‹Signature preserving lemmas›

lemma 𝒯⇩G_trans_closure_id [simp]:
"(𝒯⇩G ℱ × 𝒯⇩G ℱ)⇧+ = 𝒯⇩G ℱ × 𝒯⇩G ℱ"
by (auto simp: trancl_full_on)

lemma signature_pres_funas_cl [simp]:
"ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ ⟹ gctxtcl_funas ℱ ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
"ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ ⟹ gmctxtcl_funas ℱ ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
apply (intro gctxtex_onp_in_signature) apply blast+
apply (intro gmctxtex_onp_in_signature) apply blast+
done

lemma relf_on_gmctxtcl_funas:
assumes "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
shows "refl_on (𝒯⇩G ℱ) (gmctxtcl_funas ℱ ℛ)"
proof -
have "t ∈ 𝒯⇩G ℱ ⟹ (t, t) ∈ gmctxtcl_funas ℱ ℛ" for t
using gmctxtex_onpI[of _ "gmctxt_of_gterm t"]
by (auto simp: 𝒯⇩G_funas_gterm_conv)
then show ?thesis using assms
by (auto simp: refl_on_def)
qed

lemma gtrancl_rel_sound:
"ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ ⟹ gtrancl_rel ℱ ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
unfolding gtrancl_rel_def
by (intro Restr_tracl_comp_simps(3)) (auto simp: gmctxt_cl_gmctxtex_onp_conv)

subsection ‹@{const gcomp_rel} and @{const gtrancl_rel} lemmas›

lemma gcomp_rel:
"lift_root_step ℱ PAny EParallel (gcomp_rel ℱ ℛ 𝒮) = lift_root_step ℱ PAny EParallel ℛ O lift_root_step ℱ PAny EParallel 𝒮" (is "?Ls = ?Rs")
proof
{ fix s u assume "(s, u) ∈ gpar_rstepD' ℱ (ℛ O gpar_rstepD' ℱ 𝒮 ∪ gpar_rstepD' ℱ ℛ O 𝒮)"
then have "∃t. (s, t) ∈ gpar_rstepD' ℱ ℛ ∧ (t, u) ∈ gpar_rstepD' ℱ 𝒮"
proof (induct)
case (gpar_step_fun ts ss f)
from Ex_list_of_length_P[of _ "λ u i. (ss ! i, u) ∈ gpar_rstepD' ℱ ℛ ∧ (u, ts ! i) ∈ gpar_rstepD' ℱ 𝒮"]
obtain us where l: "length us = length ts" and
inv: "∀ i < length ts. (ss ! i, us ! i) ∈ gpar_rstepD' ℱ ℛ ∧ (us ! i, ts ! i) ∈ gpar_rstepD' ℱ 𝒮"
using gpar_step_fun(2, 3) by blast
then show ?case using gpar_step_fun(3, 4)
by (auto intro!: exI[of _ "GFun f us"])
qed auto}
then show "?Ls ⊆ ?Rs" unfolding gcomp_rel_def
by (auto simp: gmctxt_cl_gmctxtex_onp_conv simp flip: gpar_rstepD_gpar_rstepD'_conv[unfolded gpar_rstepD_def])
next
{fix s t u assume "(s, t) ∈ gpar_rstepD' ℱ ℛ" "(t, u) ∈ gpar_rstepD' ℱ 𝒮"
then have "(s, u) ∈ gpar_rstepD' ℱ (ℛ O gpar_rstepD' ℱ 𝒮 ∪ gpar_rstepD' ℱ ℛ O 𝒮)"
proof (induct arbitrary: u rule: gpar_rstepD'.induct)
case (gpar_step_fun ts ss f) note IS = this
show ?case
proof (cases "(GFun f ts, u) ∈ 𝒮")
case True
then have "(GFun f ss, u) ∈ gpar_rstepD' ℱ ℛ O 𝒮" using IS(1, 3, 4)
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 IS(5) by (cases u) (auto elim!: gpar_rstepD'.cases)
have "i < length us ⟹
(ss ! i, us ! i) ∈ gpar_rstepD' ℱ (ℛ O gpar_rstepD' ℱ 𝒮 ∪ gpar_rstepD' ℱ ℛ O 𝒮)" for i
using IS(2, 5) False
by (auto elim!: gpar_rstepD'.cases)
then show ?thesis using l IS(3, 4) unfolding u
by auto
qed
qed auto}
then show "?Rs ⊆ ?Ls"
by (auto simp: gmctxt_cl_gmctxtex_onp_conv gcomp_rel_def gpar_rstepD_gpar_rstepD'_conv[unfolded gpar_rstepD_def])
qed

lemma gmctxtcl_funas_in_rtrancl_gctxtcl_funas:
assumes "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
shows "gmctxtcl_funas ℱ ℛ ⊆ (gctxtcl_funas ℱ ℛ)⇧*" using assms
by (intro gmctxtex_onp_gctxtex_onp_rtrancl) (auto simp: gmctxt_p_inv_def)

lemma R_in_gtrancl_rel:
assumes "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
shows "ℛ ⊆ gtrancl_rel ℱ ℛ"
proof
fix s t assume ass: "(s, t) ∈ ℛ"
then have "(s, s) ∈ gmctxtcl_funas ℱ ℛ" "(t, t) ∈ gmctxtcl_funas ℱ ℛ" using assms
using all_ctxt_closed_imp_reflx_on_sig[OF gmctxtcl_funas_sigcl, of ℱ ℛ]
by auto
then show "(s, t) ∈ gtrancl_rel ℱ ℛ" using ass
by (auto simp: gmctxt_cl_gmctxtex_onp_conv relcomp_unfold gtrancl_rel_def)
qed

lemma trans_gtrancl_rel [simp]:
"trans (gtrancl_rel ℱ ℛ)"
proof -
have "(s, t) ∈ ℛ ⟹ (s, t) ∈ gmctxtcl_funas ℱ ℛ" for s t
by (metis bot.extremum funas_gmctxt.simps(2) gmctxtex_closure subsetD)
then show ?thesis unfolding trans_def gtrancl_rel_def
by (auto simp: gmctxt_cl_gmctxtex_onp_conv, meson relcomp3_I trancl_into_trancl2 trancl_trans)
qed

lemma gtrancl_rel_cl:
assumes "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
shows "gmctxtcl_funas ℱ (gtrancl_rel ℱ ℛ) ⊆ (gmctxtcl_funas ℱ ℛ)⇧+"
proof -
have *:"(s, t) ∈ ℛ ⟹ (s, t) ∈ gmctxtcl_funas ℱ ℛ" for s t
by (metis bot.extremum funas_gmctxt.simps(2) gmctxtex_closure subsetD)
have "gmctxtcl_funas ℱ ((gmctxtcl_funas ℱ ℛ)⇧+) ⊆ (gmctxtcl_funas ℱ ℛ)⇧+"
unfolding gtrancl_rel_def using relf_on_gmctxtcl_funas[OF assms]
by (intro gmctxtex_onp_substep_trancl, intro gmctxtex_pred_cmp_subseteq2)
(auto simp: less_sup_gmctxt_args_funas_gmctxt refl_on_def)
moreover have "gtrancl_rel ℱ ℛ ⊆ (gmctxtcl_funas ℱ ℛ)⇧+"
unfolding gtrancl_rel_def using *
by (auto simp: gmctxt_cl_gmctxtex_onp_conv, meson trancl.trancl_into_trancl trancl_trans)
ultimately show ?thesis using gmctxtex_onp_rel_mono by blast
qed

lemma gtrancl_rel_aux:
"ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ ⟹ gmctxtcl_funas ℱ (gtrancl_rel ℱ ℛ) O gtrancl_rel ℱ ℛ ⊆ gtrancl_rel ℱ ℛ"
"ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ ⟹ gtrancl_rel ℱ ℛ O gmctxtcl_funas ℱ (gtrancl_rel ℱ ℛ) ⊆ gtrancl_rel ℱ ℛ"
using subsetD[OF gtrancl_rel_cl[of ℛ ℱ]] unfolding gtrancl_rel_def
by (auto simp: gmctxt_cl_gmctxtex_onp_conv) (meson relcomp3_I trancl_trans)+

declare subsetI [rule del]
lemma gtrancl_rel:
assumes "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ" "compatible_p Q P"
and "⋀ C. P C ⟹ funas_gmctxt C ⊆ ℱ"
and "⋀ C D. P C ⟹ P D ⟹ (C, D) ∈ comp_gmctxt ⟹ P (C ⊓ D)"
shows "(gctxtex_onp Q ℛ)⇧+ ⊆ gmctxtex_onp P (gtrancl_rel ℱ ℛ)"
proof -
have fst: "gctxtex_onp Q ℛ ⊆ gctxtex_onp Q (gtrancl_rel ℱ ℛ)"
using R_in_gtrancl_rel[OF assms(1)]
have snd: "gctxtex_onp Q (gtrancl_rel ℱ ℛ) ⊆ gmctxtex_onp P (gtrancl_rel ℱ ℛ)"
using assms(2)
by auto
have "(gmctxtex_onp P (gtrancl_rel ℱ ℛ))⇧+ = gmctxtex_onp P (gtrancl_rel ℱ ℛ)"
by (intro gmctxtex_onp_substep_tranclE[of _ "λ C. funas_gmctxt C ⊆ ℱ"])
(auto simp: gtrancl_rel_aux[OF assms(1)] assms(3, 4) intro: funas_gmctxt_poss_gmctxt_subgm_at_funas)
then show ?thesis using subset_trans[OF fst snd]
using trancl_mono_set by fastforce
qed

lemma gtrancl_rel_subseteq_trancl_gctxtcl_funas:
assumes "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
shows "gtrancl_rel ℱ ℛ ⊆ (gctxtcl_funas ℱ ℛ)⇧+"
proof -
have [dest!]: "(s, t) ∈ ℛ ⟹ (s, t) ∈ (gctxtcl_funas ℱ ℛ)⇧+" for s t
using grstepD grstepD_def by blast
have [dest!]: "(s, t) ∈ (gmctxtcl_funas ℱ ℛ)⇧+ ⟹ (s, t) ∈ (gctxtcl_funas ℱ ℛ)⇧+ ∪ Restr Id (𝒯⇩G ℱ)"
for s t
using gmctxtcl_funas_in_rtrancl_gctxtcl_funas[OF assms]
using signature_pres_funas_cl[OF assms]
apply (auto simp: gtrancl_rel_def rtrancl_eq_or_trancl intro!: subsetI)
apply (metis rtranclD rtrancl_trancl_absorb trancl_mono)
apply (metis mem_Sigma_iff trancl_full_on trancl_mono)+
done
then show ?thesis using gtrancl_rel_sound[OF assms]
by (auto simp: gtrancl_rel_def rtrancl_eq_or_trancl gmctxt_cl_gmctxtex_onp_conv intro!: subsetI)
qed

lemma gmctxtex_onp_gtrancl_rel:
assumes "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ" and "⋀ C D. Q C ⟹ funas_gctxt D ⊆ ℱ ⟹ Q (C ∘⇩G⇩c D)"
and "⋀C. P C ⟹ 0 < num_gholes C ∧ funas_gmctxt C ⊆ ℱ"
and "⋀C. P C ⟹ gmctxt_p_inv C ℱ Q"
shows "gmctxtex_onp P (gtrancl_rel ℱ ℛ) ⊆ (gctxtex_onp Q ℛ)⇧+"
proof -
{fix s t assume ass: "(s, t) ∈ gctxtex_onp Q ((gctxtcl_funas ℱ ℛ)⇧+)"
from gctxtex_onpE[OF ass] obtain C u v where
*: "s = C⟨u⟩⇩G" "t = C⟨v⟩⇩G" and
inv: "Q C" "(u, v) ∈ (gctxtcl_funas ℱ ℛ)⇧+" by blast
from inv(2) have "(s, t) ∈ (gctxtex_onp Q ℛ)⇧+" unfolding *
proof induct
case (base y)
then show ?case using assms(2)[OF inv(1)]
by (auto elim!: gctxtex_onpE) (metis ctxt_ctxt_compose gctxtex_onpI trancl.r_into_trancl)
next
case (step y z)
from step(2) have "(C⟨y⟩⇩G, C⟨z⟩⇩G) ∈  gctxtex_onp Q ℛ" using assms(2)[OF inv(1)]
by (auto elim!: gctxtex_onpE) (metis ctxt_ctxt_compose gctxtex_onpI)
then show ?case using step(3)
by auto
qed}
then have con: "gctxtex_onp Q ((gctxtcl_funas ℱ ℛ)⇧+) ⊆ (gctxtex_onp Q ℛ)⇧+"
using subrelI by blast
have snd: "gmctxtex_onp P ((gctxtcl_funas ℱ ℛ)⇧+) ⊆ (gctxtex_onp Q ((gctxtcl_funas ℱ ℛ)⇧+))⇧+"
using assms(1)
by (intro gmctxtex_onp_gctxtex_onp_trancl[OF assms(3) _ assms(4)]) auto
have fst: "gmctxtex_onp P (gtrancl_rel ℱ ℛ) ⊆ gmctxtex_onp P ((gctxtcl_funas ℱ ℛ)⇧+)"
using gtrancl_rel_subseteq_trancl_gctxtcl_funas[OF assms(1)]
show ?thesis using subset_trans[OF fst snd] con
by (auto intro!: subsetI)
(metis (no_types, lifting) in_mono rtrancl_trancl_trancl tranclD2 trancl_mono trancl_rtrancl_absorb)
qed

lemma gmctxtcl_funas_strict_gtrancl_rel:
assumes "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
shows "gmctxtcl_funas_strict ℱ (gtrancl_rel ℱ ℛ) = (gctxtcl_funas ℱ ℛ)⇧+" (is "?Ls = ?Rs")
proof
show "?Ls ⊆ ?Rs"
by (intro gmctxtex_onp_gtrancl_rel[OF assms]) (auto simp: gmctxt_p_inv_def)
next
show "?Rs ⊆ ?Ls"
by (intro gtrancl_rel[OF assms])
(auto simp: compatible_p_def num_gholes_at_least1
intro: subset_trans[OF inf_funas_gmctxt_subset2])
qed

lemma gmctxtex_funas_nroot_strict_gtrancl_rel:
assumes "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
shows "gmctxtex_funas_nroot_strict ℱ (gtrancl_rel ℱ ℛ) = (gctxtex_funas_nroot ℱ ℛ)⇧+"
(is "?Ls = ?Rs")
proof
show "?Ls ⊆ ?Rs"
by (intro gmctxtex_onp_gtrancl_rel[OF assms])
(auto simp: gmctxt_p_inv_def gmctxt_closing_def
dest!: less_eq_gmctxt_Hole gctxt_of_gmctxt_hole_dest gctxt_compose_HoleE(1))
next
show "?Rs ⊆ ?Ls"
by (intro gtrancl_rel[OF assms])
(auto simp: compatible_p_def num_gholes_at_least1
elim!: comp_gmctxt.cases
dest: gmctxt_of_gctxt_GMHole_Hole
intro: subset_trans[OF inf_funas_gmctxt_subset2])
qed

lemma lift_root_step_sig':
assumes "ℛ ⊆ 𝒯⇩G 𝒢 × 𝒯⇩G ℋ" "ℱ ⊆ 𝒢" "ℱ ⊆ ℋ"
shows "lift_root_step ℱ W X ℛ ⊆ 𝒯⇩G 𝒢 × 𝒯⇩G ℋ"
using assms 𝒯⇩G_mono
by (cases W; cases X) (auto simp add: Sigma_mono 𝒯⇩G_mono inf.coboundedI2)

lemmas lift_root_step_sig = lift_root_step_sig'[OF _ subset_refl subset_refl]

lemma lift_root_step_incr:
"ℛ ⊆ 𝒮 ⟹ lift_root_step ℱ W X ℛ ⊆ lift_root_step ℱ W X 𝒮"
by (cases W; cases X) (auto simp add: le_supI1 gctxtex_onp_rel_mono gmctxtex_onp_rel_mono)

lemma Restr_id_mono:
"ℱ ⊆ 𝒢 ⟹ Restr Id (𝒯⇩G ℱ) ⊆ Restr Id (𝒯⇩G 𝒢)"
by (meson Sigma_mono 𝒯⇩G_mono inf_mono subset_refl)

lemma lift_root_step_mono:
"ℱ ⊆ 𝒢 ⟹ lift_root_step ℱ W X ℛ ⊆ lift_root_step 𝒢 W X ℛ"
by (cases W; cases X) (auto simp: Restr_id_mono intro: gmctxtex_onp_mono gctxtex_onp_mono,
metis Restr_id_mono sup.coboundedI1 sup_commute)

lemma grstep_lift_root_step:
"lift_root_step ℱ PAny ESingle (Restr (grrstep ℛ) (𝒯⇩G ℱ)) = Restr (grstep ℛ) (𝒯⇩G ℱ)"
unfolding grstepD_grstep_conv grstepD_def grrstep_subst_cl_conv
by auto

lemma prod_swap_id_on_refl [simp]:
"Restr Id (𝒯⇩G ℱ) ⊆ prod.swap ` (ℛ ∪ Restr Id (𝒯⇩G ℱ))"
by (auto intro: subsetI)

lemma swap_lift_root_step:
"lift_root_step ℱ W X (prod.swap ` ℛ) = prod.swap ` lift_root_step ℱ W X ℛ"
by (cases W; cases X) (auto simp add: image_mono swap_gmctxtex_onp swap_gctxtex_onp intro: subsetI)

lemma converse_lift_root_step:
"(lift_root_step ℱ W X R)¯ = lift_root_step ℱ W X (R¯)"
by (cases W; cases X) (auto simp add: converse_gctxtex_onp converse_gmctxtex_onp intro: subsetI)

lemma lift_root_step_sig_transfer:
assumes "p ∈ lift_root_step ℱ W X R" "snd ` R ⊆ 𝒯⇩G ℱ" "funas_gterm (fst p) ⊆ 𝒢"
shows "p ∈ lift_root_step 𝒢 W X R" using assms
proof -
from assms have "p ∈ lift_root_step (ℱ ∩ 𝒢) W X R"
by (cases p; cases W; cases X)
(auto simp: gctxtex_onp_sign_trans_fst[of _ _ _ R 𝒢] gctxtex_onp_sign_trans_snd[of _ _ _ R 𝒢]
gmctxtex_onp_sign_trans_fst gmctxtex_onp_sign_trans_snd simp flip: 𝒯⇩G_equivalent_def 𝒯⇩G_funas_gterm_conv
intro: basic_trans_rules(30)[OF gctxtex_onp_sign_trans_fst[of _ _ _ R 𝒢],
where ?B = "gctxtex_onp P R" for P]
basic_trans_rules(30)[OF gmctxtex_onp_sign_trans_fst[of _ _ _ R 𝒢],
where ?B = "gmctxtex_onp P R" for P])
then show ?thesis
by (meson inf.cobounded2 lift_root_step_mono subsetD)
qed

lemma lift_root_step_sig_transfer2:
assumes "p ∈ lift_root_step ℱ W X R" "snd ` R ⊆ 𝒯⇩G 𝒢" "funas_gterm (fst p) ⊆ 𝒢"
shows "p ∈ lift_root_step 𝒢 W X R"
proof -
from assms have "p ∈ lift_root_step (ℱ ∩ 𝒢) W X R"
by (cases p; cases W; cases X)
(auto simp: gctxtex_onp_sign_trans_fst[of _ _ _ R 𝒢] gctxtex_onp_sign_trans_snd[of _ _ _ R 𝒢]
gmctxtex_onp_sign_trans_fst gmctxtex_onp_sign_trans_snd simp flip: 𝒯⇩G_equivalent_def 𝒯⇩G_funas_gterm_conv
intro: basic_trans_rules(30)[OF gctxtex_onp_sign_trans_fst[of _ _ _ R 𝒢],
where ?B = "gctxtex_onp P R" for P]
basic_trans_rules(30)[OF gmctxtex_onp_sign_trans_fst[of _ _ _ R 𝒢],
where ?B = "gmctxtex_onp P R" for P])
then show ?thesis
by (meson inf.cobounded2 lift_root_step_mono subsetD)
qed

lemma lift_root_steps_sig_transfer:
assumes "(s, t) ∈ (lift_root_step ℱ W X R)⇧+" "snd ` R ⊆ 𝒯⇩G 𝒢" "funas_gterm s ⊆ 𝒢"
shows "(s, t) ∈ (lift_root_step 𝒢 W X R)⇧+"
using assms(1,3)
proof (induct rule: converse_trancl_induct)
case (base s)
show ?case using lift_root_step_sig_transfer2[OF base(1) assms(2)] base(2) by (simp add: r_into_trancl)
next
case (step s s')
show ?case using lift_root_step_sig_transfer2[OF step(1) assms(2)] step(3,4)
lift_root_step_sig'[of R UNIV 𝒢 𝒢 W X, THEN subsetD, of "(s, s')"] assms(2)
by (auto simp: 𝒯⇩G_funas_gterm_conv 𝒯⇩G_equivalent_def)
(smt SigmaI UNIV_I image_subset_iff snd_conv subrelI trancl_into_trancl2)
qed

lemma lift_root_stepseq_sig_transfer:
assumes "(s, t) ∈ (lift_root_step ℱ W X R)⇧*" "snd ` R ⊆ 𝒯⇩G 𝒢" "funas_gterm s ⊆ 𝒢"
shows "(s, t) ∈ (lift_root_step 𝒢 W X R)⇧*"
using assms by (auto simp flip: reflcl_trancl simp: lift_root_steps_sig_transfer)

lemmas lift_root_step_sig_transfer' = lift_root_step_sig_transfer[of "prod.swap p" ℱ W X "prod.swap ` R" 𝒢 for p ℱ W X 𝒢 R,
unfolded swap_lift_root_step, OF imageI, THEN imageI [of _ _ prod.swap],
unfolded image_comp comp_def fst_swap snd_swap swap_swap image_ident]

lemmas lift_root_steps_sig_transfer' = lift_root_steps_sig_transfer[of t s ℱ W X "prod.swap ` R" 𝒢 for t s ℱ W X 𝒢 R,
THEN imageI [of _ _ prod.swap], unfolded swap_lift_root_step swap_trancl pair_in_swap_image
image_comp comp_def snd_swap swap_swap swap_simp image_ident]

lemmas lift_root_stepseq_sig_transfer' = lift_root_stepseq_sig_transfer[of t s ℱ W X "prod.swap ` R" 𝒢 for t s ℱ W X 𝒢 R,
THEN imageI [of _ _ prod.swap], unfolded swap_lift_root_step swap_rtrancl pair_in_swap_image
image_comp comp_def snd_swap swap_swap swap_simp image_ident]

lemma lift_root_step_PRoot_ESingle [simp]:
"lift_root_step ℱ PRoot ESingle ℛ = ℛ"
by auto

lemma lift_root_step_PRoot_EStrictParallel [simp]:
"lift_root_step ℱ PRoot EStrictParallel ℛ = ℛ"
by auto

lemma lift_root_step_Parallel_conv:
shows "lift_root_step ℱ W EParallel ℛ = lift_root_step ℱ W EStrictParallel ℛ ∪ Restr Id (𝒯⇩G ℱ)"
by (cases W) (auto simp: gmctxtcl_funas_dist gmctxtex_funas_nroot_dist)

lemma relax_pos_lift_root_step:
"lift_root_step ℱ W X R ⊆ lift_root_step ℱ PAny X R"
by (cases W; cases X) (auto simp: gctxtex_closure gmctxtex_closure)

lemma relax_pos_lift_root_steps:
"(lift_root_step ℱ W X R)⇧+ ⊆ (lift_root_step ℱ PAny X R)⇧+"

lemma relax_ext_lift_root_step:
"lift_root_step ℱ W X R ⊆ lift_root_step ℱ W EParallel R"
by (cases W; cases X) (auto simp: compatible_p_gctxtex_gmctxtex_subseteq)

lemma lift_root_step_StrictParallel_seq:
assumes "R ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
shows "lift_root_step ℱ PAny EStrictParallel R ⊆ (lift_root_step ℱ PAny ESingle R)⇧+"
using assms
by (auto simp: gmctxt_p_inv_def intro!: gmctxtex_onp_gctxtex_onp_trancl)

lemma lift_root_step_Parallel_seq:
assumes "R ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
shows "lift_root_step ℱ PAny EParallel R ⊆ (lift_root_step ℱ PAny ESingle R)⇧+ ∪ Restr Id (𝒯⇩G ℱ)"
unfolding lift_root_step_Parallel_conv using lift_root_step_StrictParallel_seq[OF assms]
using Un_mono by blast

lemma lift_root_step_Single_to_Parallel:
shows "lift_root_step ℱ PAny ESingle R ⊆ lift_root_step ℱ PAny EParallel R"

lemma trancl_partial_reflcl:
"(X ∪ Restr Id Y)⇧+ = X⇧+ ∪ Restr Id Y"
proof (intro equalityI subrelI, goal_cases LR RL)
case (LR a b) then show ?case by (induct) (auto dest: trancl_into_trancl)
qed (auto intro: trancl_mono)

lemma lift_root_step_Parallels_single:
assumes "R ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
shows "(lift_root_step ℱ PAny EParallel R)⇧+ = (lift_root_step ℱ PAny ESingle R)⇧+ ∪ Restr Id (𝒯⇩G ℱ)"
using trancl_mono_set[OF lift_root_step_Parallel_seq[OF assms]]
using trancl_mono_set[OF lift_root_step_Single_to_Parallel, of ℱ R]
by (auto simp: lift_root_step_Parallel_conv trancl_partial_reflcl)

lemma lift_root_Any_Single_eq:
shows "lift_root_step ℱ PAny ESingle R = R ∪ lift_root_step ℱ PNonRoot ESingle R"
by (auto simp: gctxtcl_funas_dist intro!: gctxtex_closure)

lemma lift_root_Any_EStrict_eq [simp]:
shows "lift_root_step ℱ PAny EStrictParallel R = R ∪ lift_root_step ℱ PNonRoot EStrictParallel R"
by (auto simp: gmctxtcl_funas_strict_dist)

lemma gar_rstep_lift_root_step:
"lift_root_step ℱ PAny EParallel (Restr (grrstep ℛ) (𝒯⇩G ℱ)) = Restr (gpar_rstep ℛ) (𝒯⇩G ℱ)"
unfolding grrstep_subst_cl_conv gpar_rstep_gpar_rstepD_conv
unfolding gpar_rstepD_gpar_rstepD'_conv[symmetric]
by (auto simp: gpar_rstepD_def)

lemma grrstep_lift_root_gnrrstep:
"lift_root_step ℱ PNonRoot ESingle (Restr (grrstep ℛ) (𝒯⇩G ℱ)) = Restr (gnrrstep ℛ) (𝒯⇩G ℱ)"
unfolding gnrrstepD_gnrrstep_conv grrstep_subst_cl_conv