# Theory Context_Extensions

```theory Context_Extensions
imports Regular_Tree_Relations.Ground_Ctxt
Regular_Tree_Relations.Ground_Closure
Ground_MCtxt
begin

section ‹Multihole context and context closures over predicates›

definition gctxtex_onp where
"gctxtex_onp P ℛ = {(C⟨s⟩⇩G, C⟨t⟩⇩G) | C s t. P C ∧ (s, t) ∈ ℛ}"

definition gmctxtex_onp where
"gmctxtex_onp P ℛ = {(fill_gholes C ss, fill_gholes C ts) | C ss ts.
num_gholes C = length ss ∧ length ss = length ts ∧ P C ∧ (∀ i < length ts. (ss ! i , ts ! i) ∈ ℛ)}"

definition compatible_p where
"compatible_p P Q ≡ (∀ C. P C ⟶ Q (gmctxt_of_gctxt C))"

subsection ‹Elimination and introduction rules for the extensions›

lemma gctxtex_onpE [elim]:
assumes "(s, t) ∈ gctxtex_onp P ℛ"
obtains C u v where "s = C⟨u⟩⇩G" "t = C⟨v⟩⇩G" "P C" "(u, v) ∈ ℛ"
using assms unfolding gctxtex_onp_def by auto

lemma gctxtex_onp_neq_rootE [elim]:
assumes "(GFun f ss, GFun g ts) ∈ gctxtex_onp P ℛ" and "f ≠ g"
shows "(GFun f ss, GFun g ts) ∈ ℛ"
proof -
obtain C u v where "GFun f ss = C⟨u⟩⇩G" "GFun g ts = C⟨v⟩⇩G" "(u, v) ∈ ℛ"
using assms(1) by auto
then show ?thesis using assms(2)
by (cases C) auto
qed

lemma gctxtex_onp_neq_lengthE [elim]:
assumes "(GFun f ss, GFun g ts) ∈ gctxtex_onp P ℛ" and "length ss ≠ length ts"
shows "(GFun f ss, GFun g ts) ∈ ℛ"
proof -
obtain C u v where "GFun f ss = C⟨u⟩⇩G" "GFun g ts = C⟨v⟩⇩G" "(u, v) ∈ ℛ"
using assms(1) by auto
then show ?thesis using assms(2)
by (cases C) auto
qed

lemma gmctxtex_onpE [elim]:
assumes "(s, t) ∈ gmctxtex_onp P ℛ"
obtains C us vs where "s = fill_gholes C us" "t = fill_gholes C vs" "num_gholes C = length us"
"length us = length vs" "P C" "∀ i < length vs. (us ! i, vs ! i) ∈ ℛ"
using assms unfolding gmctxtex_onp_def by auto

lemma gmctxtex_onpE2 [elim]:
assumes "(s, t) ∈ gmctxtex_onp P ℛ"
obtains C us vs where "s =⇩G⇩f (C, us)" "t =⇩G⇩f (C, vs)"
"P C" "∀ i < length vs. (us ! i, vs ! i) ∈ ℛ"
using gmctxtex_onpE[OF assms] by (metis eq_gfill.intros)

lemma gmctxtex_onp_neq_rootE [elim]:
assumes "(GFun f ss, GFun g ts) ∈ gmctxtex_onp P ℛ" and "f ≠ g"
shows "(GFun f ss, GFun g ts) ∈ ℛ"
proof -
obtain C us vs where "GFun f ss = fill_gholes C us" "GFun g ts = fill_gholes C vs"
"num_gholes C = length us" "length us = length vs" "∀ i < length vs. (us ! i, vs ! i) ∈ ℛ"
using assms(1) by auto
then show ?thesis using assms(2)
by (cases C; cases us; cases vs) auto
qed

lemma gmctxtex_onp_neq_lengthE [elim]:
assumes "(GFun f ss, GFun g ts) ∈ gmctxtex_onp P ℛ" and "length ss ≠ length ts"
shows "(GFun f ss, GFun g ts) ∈ ℛ"
proof -
obtain C us vs where "GFun f ss = fill_gholes C us" "GFun g ts = fill_gholes C vs"
"num_gholes C = length us" "length us = length vs" "∀ i < length vs. (us ! i, vs ! i) ∈ ℛ"
using assms(1) by auto
then show ?thesis using assms(2)
by (cases C; cases us; cases vs) auto
qed

lemma gmctxtex_onp_listE:
assumes "∀ i < length ts. (ss ! i, ts ! i) ∈ gmctxtex_onp Q ℛ" "length ss = length ts"
obtains Ds sss tss where "length ts = length Ds" "length Ds = length sss" "length sss = length tss"
"∀ i < length tss. length (sss ! i) = length (tss ! i)" "∀ D ∈ set Ds. Q D"
"∀ i < length tss. ss ! i =⇩G⇩f (Ds ! i, sss ! i)" "∀ i < length tss. ts ! i =⇩G⇩f (Ds ! i, tss ! i)"
"∀ i < length (concat tss). (concat sss ! i, concat tss ! i) ∈ ℛ"
proof -
let ?P = "λ W i. ss ! i =⇩G⇩f (fst W, fst (snd W)) ∧ ts ! i =⇩G⇩f (fst W, snd (snd W)) ∧
Q (fst W) ∧ (∀ i < length (snd (snd W)). (fst (snd W) ! i, snd (snd W) ! i) ∈ ℛ)"
have "∀ i < length ts. ∃ x. ?P x i" using assms gmctxtex_onpE2[of "ss ! i" "ts ! i" Q ℛ for i]
by auto metis
from Ex_list_of_length_P[OF this] obtain W where
P: "length W = length ts" "∀ i < length ts. ?P (W ! i) i" by blast
define Ds sss tss where "Ds ≡ map fst W" and "sss ≡ map (fst ∘ snd) W" and "tss ≡ map (snd ∘ snd) W"
from P have len: "length ts = length Ds" "length Ds = length sss" "length sss = length tss" and
pred: "∀ D ∈ set Ds. Q D" and
split: "∀ i < length Ds. ss ! i =⇩G⇩f (Ds ! i, sss ! i) ∧ ts ! i =⇩G⇩f (Ds ! i, tss ! i)"and
rec: "∀i < length Ds. ∀ j < length (tss ! i). (sss ! i ! j, tss ! i ! j) ∈ ℛ"
using assms(2) by (auto simp: Ds_def sss_def tss_def dest!: in_set_idx)
from len split have inn: "∀ i < length tss. length (sss ! i) = length (tss ! i)"
by auto (metis eqgfE(2))
from inn len rec have "∀ i < length (concat tss). (concat sss ! i, concat tss ! i) ∈ ℛ"
by (intro concat_nth_nthI) auto
then show "(⋀Ds sss tss. length ts = length Ds ⟹ length Ds = length sss ⟹ length sss = length tss ⟹
∀i<length tss. length (sss ! i) = length (tss ! i) ⟹ ∀D∈set Ds. Q D ⟹
∀i<length tss. ss ! i =⇩G⇩f (Ds ! i, sss ! i) ⟹ ∀i<length tss. ts ! i =⇩G⇩f (Ds ! i, tss ! i) ⟹
∀i<length (concat tss). (concat sss ! i, concat tss ! i) ∈ ℛ ⟹ thesis) ⟹ thesis"
using pred split inn len by auto
qed

lemma gmctxtex_onp_doubleE [elim]:
assumes "(s, t) ∈ gmctxtex_onp P (gmctxtex_onp Q ℛ)"
obtains C Ds ss ts us vs where "s =⇩G⇩f (C, ss)" "t =⇩G⇩f (C, ts)" "P C" "∀ D ∈ set Ds. Q D"
"num_gholes C = length Ds" "length Ds = length ss" "length ss = length ts" "length ts = length us" "length us = length vs"
"∀ i < length Ds. ss ! i =⇩G⇩f (Ds ! i, us ! i) ∧ ts ! i =⇩G⇩f (Ds ! i, vs ! i)"
"∀ i < length Ds. ∀ j < length (vs ! i). (us ! i ! j, vs ! i ! j) ∈ ℛ"
proof -
from gmctxtex_onpE2[OF assms] obtain C ss ts where
split: "s =⇩G⇩f (C, ss)" "t =⇩G⇩f (C, ts)" and
len: "num_gholes C = length ss" "length ss = length ts" and
pred: "P C" and rec: "∀ i < length ts. (ss ! i, ts ! i) ∈ gmctxtex_onp Q ℛ"
by (metis eqgfE(2))
let ?P = "λ W i. ss ! i =⇩G⇩f (fst W, fst (snd W)) ∧ ts ! i =⇩G⇩f (fst W, snd (snd W)) ∧
Q (fst W) ∧ (∀ i < length (snd (snd W)). (fst (snd W) ! i, snd (snd W) ! i) ∈ ℛ)"
have "∀ i < length ts. ∃ x. ?P x i" using rec gmctxtex_onpE2[of "ss ! i" "ts ! i" Q ℛ for i]
by auto metis
from Ex_list_of_length_P[OF this] obtain W where
P: "length W = length ts" "∀ i < length ts. ?P (W ! i) i" by blast
define Ds us vs where "Ds ≡ map fst W" and "us ≡ map (fst ∘ snd) W" and "vs ≡ map (snd ∘ snd) W"
from P have len': "length Ds = length ss" "length ss = length ts" "length ts = length us" "length us = length vs" and
pred': "∀ D ∈ set Ds. Q D" and
split': "∀ i < length Ds. ss ! i =⇩G⇩f (Ds ! i, us ! i) ∧ ts ! i =⇩G⇩f (Ds ! i, vs ! i)"and
rec': "∀i < length Ds. ∀ j < length (vs ! i). (us ! i ! j, vs ! i ! j) ∈ ℛ"
using len by (auto simp: Ds_def us_def vs_def dest!: in_set_idx)
from len' len have "num_gholes C = length Ds" by simp
from this split pred pred' len' split' rec' len
show "(⋀C ss ts Ds us vs. s =⇩G⇩f (C, ss) ⟹ t =⇩G⇩f (C, ts) ⟹ P C ⟹
∀D∈set Ds. Q D ⟹ num_gholes C = length Ds ⟹ length Ds = length ss ⟹ length ss = length ts ⟹
length ts = length us ⟹ length us = length vs ⟹
∀i<length Ds. ss ! i =⇩G⇩f (Ds ! i, us ! i) ∧ ts ! i =⇩G⇩f (Ds ! i, vs ! i) ⟹
∀i<length Ds. ∀j<length (vs ! i). (us ! i ! j, vs ! i ! j) ∈ ℛ ⟹ thesis) ⟹ thesis"
by blast
qed

lemma gctxtex_onpI [intro]:
assumes "P C" and "(s, t) ∈ ℛ"
shows "(C⟨s⟩⇩G, C⟨t⟩⇩G) ∈ gctxtex_onp P ℛ"
using assms by (auto simp: gctxtex_onp_def)

lemma gmctxtex_onpI [intro]:
assumes "P C" and "num_gholes C = length us" and "length us = length vs"
and "∀ i < length vs. (us ! i, vs ! i) ∈ ℛ"
shows "(fill_gholes C us, fill_gholes C vs) ∈ gmctxtex_onp P ℛ"
using assms unfolding gmctxtex_onp_def
by force

lemma gmctxtex_onp_arg_monoI:
assumes "P GMHole"
shows "ℛ ⊆ gmctxtex_onp P ℛ" using assms
proof (intro subsetI)
fix s assume mem: "s ∈ ℛ"
have *: "(fill_gholes GMHole [fst s], fill_gholes GMHole [snd s]) = s" by auto
have "(fill_gholes GMHole [fst s], fill_gholes GMHole [snd s]) ∈ gmctxtex_onp P ℛ"
by (intro gmctxtex_onpI) (auto simp: assms mem)
then show "s ∈ gmctxtex_onp P ℛ" unfolding * .
qed

lemma gmctxtex_onpI2 [intro]:
assumes "P C" and "s =⇩G⇩f (C, ss)" "t =⇩G⇩f (C, ts)"
and "∀ i < length ts. (ss ! i, ts ! i) ∈ ℛ"
shows "(s, t) ∈ gmctxtex_onp P ℛ"
using eqgfE[OF assms(2)] eqgfE[OF assms(3)]
using gmctxtex_onpI[of P, OF assms(1) _ _ assms(4)]
by (simp add: ‹num_gholes C = length ss›)

lemma gctxtex_onp_hold_cond [simp]:
"(s, t) ∈ gctxtex_onp P ℛ ⟹ groot s ≠ groot t ⟹ P □⇩G"
"(s, t) ∈ gctxtex_onp P ℛ ⟹ length (gargs s) ≠ length (gargs t) ⟹ P □⇩G"
by (auto elim!: gctxtex_onpE, case_tac C; auto)+

subsection ‹Monotonicity rules for the extensions›

lemma gctxtex_onp_rel_mono:
"ℒ ⊆ ℛ ⟹ gctxtex_onp P ℒ ⊆ gctxtex_onp P ℛ"
unfolding gctxtex_onp_def by auto

lemma gmctxtex_onp_rel_mono:
"ℒ ⊆ ℛ ⟹ gmctxtex_onp P ℒ ⊆ gmctxtex_onp P ℛ"
unfolding gmctxtex_onp_def
by auto (metis subsetD)

lemma compatible_p_gctxtex_gmctxtex_subseteq [dest]:
"compatible_p P Q ⟹ gctxtex_onp P ℛ ⊆ gmctxtex_onp Q ℛ"
unfolding compatible_p_def
by (auto simp: apply_gctxt_fill_gholes gmctxtex_onpI)

lemma compatible_p_mono1:
"P ≤ R ⟹ compatible_p R Q ⟹ compatible_p P Q"
unfolding compatible_p_def by auto

lemma compatible_p_mono2:
"Q ≤ R ⟹ compatible_p P Q ⟹ compatible_p P R"
unfolding compatible_p_def by auto

lemma gctxtex_onp_mono [intro]:
"P ≤ Q ⟹ gctxtex_onp P ℛ ⊆ gctxtex_onp Q ℛ"
by auto

lemma gctxtex_onp_mem:
"P ≤ Q ⟹ (s, t) ∈ gctxtex_onp P ℛ ⟹ (s, t) ∈ gctxtex_onp Q ℛ"
by auto

lemma gmctxtex_onp_mono [intro]:
"P ≤ Q ⟹ gmctxtex_onp P ℛ ⊆ gmctxtex_onp Q ℛ"
by (auto elim!: gmctxtex_onpE)

lemma gmctxtex_onp_mem:
"P ≤ Q ⟹ (s, t) ∈ gmctxtex_onp P ℛ ⟹ (s, t) ∈ gmctxtex_onp Q ℛ"
by (auto dest!: gmctxtex_onp_mono)

lemma gctxtex_eqI [intro]:
"P = Q ⟹ ℛ = ℒ ⟹ gctxtex_onp P ℛ = gctxtex_onp Q ℒ"
by auto

lemma gmctxtex_eqI [intro]:
"P = Q ⟹ ℛ = ℒ ⟹ gmctxtex_onp P ℛ = gmctxtex_onp Q ℒ"
by auto

subsection ‹Relation swap and converse›

lemma swap_gctxtex_onp:
"gctxtex_onp P (prod.swap ` ℛ) = prod.swap ` gctxtex_onp P ℛ"
by (auto simp: gctxtex_onp_def image_def) force+

lemma swap_gmctxtex_onp:
"gmctxtex_onp P (prod.swap ` ℛ) = prod.swap ` gmctxtex_onp P ℛ"
by (auto simp: gmctxtex_onp_def image_def) force+

lemma converse_gctxtex_onp:
"(gctxtex_onp P ℛ)¯ = gctxtex_onp P (ℛ¯)"
by (auto simp: gctxtex_onp_def)

lemma converse_gmctxtex_onp:
"(gmctxtex_onp P ℛ)¯ = gmctxtex_onp P (ℛ¯)"
by (auto simp: gmctxtex_onp_def) force+

subsection ‹Subset equivalence for context extensions over predicates›

lemma gctxtex_onp_closure_predI:
assumes "⋀ C s t. P C ⟹ (s, t) ∈ ℛ ⟹ (C⟨s⟩⇩G, C⟨t⟩⇩G) ∈ ℛ"
shows "gctxtex_onp P ℛ ⊆ ℛ"
using assms by auto

lemma gmctxtex_onp_closure_predI:
assumes "⋀ C ss ts. P C ⟹ num_gholes C = length ss ⟹ length ss = length ts ⟹
(∀ i < length ts. (ss ! i, ts ! i) ∈ ℛ) ⟹ (fill_gholes C ss, fill_gholes C ts) ∈ ℛ"
shows "gmctxtex_onp P ℛ ⊆ ℛ"
using assms by auto

lemma gctxtex_onp_closure_predE:
assumes "gctxtex_onp P ℛ ⊆ ℛ"
shows  "⋀ C s t. P C ⟹ (s, t) ∈ ℛ ⟹ (C⟨s⟩⇩G, C⟨t⟩⇩G) ∈ ℛ"
using assms by auto

lemma gctxtex_closure [intro]:
"P □⇩G ⟹ ℛ ⊆ gctxtex_onp P ℛ"
by (auto simp: gctxtex_onp_def) force

lemma gmctxtex_closure [intro]:
assumes "P GMHole"
shows "ℛ ⊆ (gmctxtex_onp P ℛ)"
proof -
{fix s t assume "(s, t) ∈ ℛ" then have "(s, t) ∈ gmctxtex_onp P ℛ"
using gmctxtex_onpI[of P GMHole "[s]" "[t]"] assms by auto}
then show ?thesis by auto
qed

lemma gctxtex_pred_cmp_subseteq:
assumes "⋀ C D. P C ⟹ Q D ⟹ Q (C ∘⇩G⇩c D)"
shows "gctxtex_onp P (gctxtex_onp Q ℛ) ⊆ gctxtex_onp Q ℛ"
using assms by (auto simp: gctxtex_onp_def) (metis ctxt_ctxt_compose)

lemma gctxtex_pred_cmp_subseteq2:
assumes "⋀ C D. P C ⟹ Q D ⟹ P (C ∘⇩G⇩c D)"
shows "gctxtex_onp P (gctxtex_onp Q ℛ) ⊆ gctxtex_onp P ℛ"
using assms by (auto simp: gctxtex_onp_def) (metis ctxt_ctxt_compose)

lemma gmctxtex_pred_cmp_subseteq:
assumes "⋀ C D. C ≤ D ⟹ P C ⟹ (∀ Ds ∈ set (sup_gmctxt_args C D). Q Ds) ⟹ Q D"
shows "gmctxtex_onp P (gmctxtex_onp Q ℛ) ⊆ gmctxtex_onp Q ℛ" (is "?Ls ⊆ ?Rs")
proof -
{fix s t assume "(s, t) ∈ ?Ls"
then obtain C Ds ss ts us vs where
split: "s =⇩G⇩f (C, ss)" "t =⇩G⇩f (C, ts)" and
len: "num_gholes C = length Ds" "length Ds = length ss" "length ss = length ts"
"length ts = length us" "length us = length vs" and
pred: "P C" "∀ D ∈ set Ds. Q D" and
split': "∀ i < length Ds. ss ! i =⇩G⇩f (Ds ! i, us ! i) ∧ ts ! i =⇩G⇩f (Ds ! i, vs ! i)" and
rec: " ∀i<length Ds. ∀j<length (vs ! i). (us ! i ! j, vs ! i ! j) ∈ ℛ"
by auto
from pred(2) assms[OF _ pred(1), of "fill_gholes_gmctxt C Ds"] len
have P: "Q (fill_gholes_gmctxt C Ds)"
have mem: "∀ i < length (concat vs). (concat us ! i, concat vs ! i) ∈ ℛ"
using rec split' len
by (intro concat_nth_nthI) (auto, metis eqgfE(2))
have "(s, t) ∈ ?Rs" using split' split len
by (intro gmctxtex_onpI2[of Q, OF P _ _ mem])
(metis eqgfE(1) fill_gholes_gmctxt_sound)+}
then show ?thesis by auto
qed

lemma gmctxtex_pred_cmp_subseteq2:
assumes "⋀ C D. C ≤ D ⟹ P C ⟹ (∀ Ds ∈ set (sup_gmctxt_args C D). Q Ds) ⟹ P D"
shows "gmctxtex_onp P (gmctxtex_onp Q ℛ) ⊆ gmctxtex_onp P ℛ" (is "?Ls ⊆ ?Rs")
proof -
{fix s t assume "(s, t) ∈ ?Ls"
then obtain C Ds ss ts us vs where
split: "s =⇩G⇩f (C, ss)" "t =⇩G⇩f (C, ts)" and
len: "num_gholes C = length Ds" "length Ds = length ss" "length ss = length ts"
"length ts = length us" "length us = length vs" and
pred: "P C" "∀ D ∈ set Ds. Q D" and
split': "∀ i < length Ds. ss ! i =⇩G⇩f (Ds ! i, us ! i) ∧ ts ! i =⇩G⇩f (Ds ! i, vs ! i)" and
rec: " ∀i<length Ds. ∀j<length (vs ! i). (us ! i ! j, vs ! i ! j) ∈ ℛ"
by auto
from pred(2) assms[OF _ pred(1), of "fill_gholes_gmctxt C Ds"] len
have P: "P (fill_gholes_gmctxt C Ds)"
have mem: "∀ i < length (concat vs). (concat us ! i, concat vs ! i) ∈ ℛ" using rec split' len
by (intro concat_nth_nthI) (auto, metis eqgfE(2))
have "(s, t) ∈ ?Rs" using split' split len
by (intro gmctxtex_onpI2[of P, OF P _ _ mem])
(metis eqgfE(1) fill_gholes_gmctxt_sound)+}
then show ?thesis by auto
qed

lemma gctxtex_onp_idem [simp]:
assumes "P □⇩G" and "⋀ C D. P C ⟹ Q D ⟹ Q (C ∘⇩G⇩c D)"
shows "gctxtex_onp P (gctxtex_onp Q ℛ) = gctxtex_onp Q ℛ" (is "?Ls = ?Rs")
by (simp add: assms gctxtex_pred_cmp_subseteq gctxtex_closure subset_antisym)

lemma gctxtex_onp_idem2 [simp]:
assumes "Q □⇩G" and "⋀ C D. P C ⟹ Q D ⟹ P (C ∘⇩G⇩c D)"
shows "gctxtex_onp P (gctxtex_onp Q ℛ) = gctxtex_onp P ℛ" (is "?Ls = ?Rs")
using gctxtex_pred_cmp_subseteq2[of P Q, OF assms(2)]
using gctxtex_closure[of Q, OF assms(1)] in_mono
by auto fastforce

lemma gmctxtex_onp_idem [simp]:
assumes "P GMHole"
and "⋀ C D. C ≤ D ⟹ P C ⟹ (∀ Ds ∈ set (sup_gmctxt_args C D). Q Ds) ⟹ Q D"
shows "gmctxtex_onp P (gmctxtex_onp Q ℛ) = gmctxtex_onp Q ℛ"
using gmctxtex_pred_cmp_subseteq[of P Q ℛ] gmctxtex_closure[of P] assms
by auto

subsection ‹@{const gmctxtex_onp} subset equivalence @{const gctxtex_onp} transitive closure›

text ‹The following definition demands that if we arbitrarily fill a multihole context C with terms
induced by signature F such that one hole remains then the predicate Q holds›
definition "gmctxt_p_inv C ℱ Q ≡ (∀ D. gmctxt_closing C D ⟶ num_gholes D = 1 ⟶ funas_gmctxt D ⊆ ℱ
⟶ Q (gctxt_of_gmctxt D))"

lemma gmctxt_p_invE:
"gmctxt_p_inv C ℱ Q ⟹ C ≤ D ⟹ ghole_poss D ⊆ ghole_poss C ⟹ num_gholes D = 1 ⟹
funas_gmctxt D ⊆ ℱ ⟹ Q (gctxt_of_gmctxt D)"
unfolding gmctxt_closing_def gmctxt_p_inv_def
using less_eq_gmctxt_prime by blast

lemma gmctxt_closing_gmctxt_p_inv_comp:
"gmctxt_closing C D ⟹ gmctxt_p_inv C ℱ Q ⟹ gmctxt_p_inv D ℱ Q"
unfolding gmctxt_closing_def gmctxt_p_inv_def
by auto (meson less_eq_gmctxt_prime order_trans)

lemma GMHole_gmctxt_p_inv_GHole [simp]:
"gmctxt_p_inv GMHole ℱ Q ⟹ Q □⇩G"
by (auto dest: gmctxt_p_invE)

lemma gmctxtex_onp_gctxtex_onp_trancl:
assumes sig: "⋀ C. P C ⟹ 0 < num_gholes C ∧ funas_gmctxt C ⊆ ℱ" "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
and "⋀ C. P C ⟹ gmctxt_p_inv C ℱ Q"
shows "gmctxtex_onp P ℛ ⊆ (gctxtex_onp Q ℛ)⇧+"
proof
fix s t assume "(s, t) ∈ gmctxtex_onp P ℛ"
then obtain C ss ts where
split: "s = fill_gholes C ss" "t = fill_gholes C ts" and
inv: "num_gholes C = length ss" "num_gholes C = length ts" and
pred: "P C" and rec: "∀ i < length ts. (ss ! i, ts ! i) ∈ ℛ"
by auto
from pred have "0 < num_gholes C" "funas_gmctxt C ⊆ ℱ" using sig by auto
from this inv assms(3)[OF pred] rec show "(s, t) ∈ (gctxtex_onp Q ℛ)⇧+" unfolding split
proof (induct "num_gholes C" arbitrary: C ss ts)
case (Suc x) note IS = this then show ?case
proof (cases C)
case GMHole then show ?thesis
using IS(2-) gctxtex_closure unfolding gmctxt_p_inv_def gmctxt_closing_def
by (metis One_nat_def fill_gholes_GMHole gctxt_of_gmctxt.simps(1)
gmctxt_order_bot.bot.extremum_unique less_eq_gmctxt_prime num_gholes.simps(1) r_into_trancl' subsetD subsetI)
next
case [simp]: (GMFun f Cs) note IS = IS[unfolded GMFun]
let ?rep = "λ x. replicate (num_gholes (GMFun f Cs) - 1) x"
let ?Ds1 = "?rep GMHole @ [gmctxt_of_gterm (last ss)]"
let ?Ds2 = "map gmctxt_of_gterm (butlast ts) @ [GMHole]"
let ?D1 = "fill_gholes_gmctxt (GMFun f Cs) ?Ds1"
let ?D2 = "fill_gholes_gmctxt (GMFun f Cs) ?Ds2"
have holes: "num_gholes (GMFun f Cs) = length ?Ds1" "num_gholes (GMFun f Cs) = length ?Ds2"
using IS(2, 5, 6) by auto
from holes(2) have [simp]: "num_gholes ?D2 = Suc 0"
by (auto simp: num_gholes_fill_gholes_gmctxt simp del: fill_gholes_gmctxt.simps)
from holes(1) have h: "x = num_gholes ?D1" using IS(2)
by (auto simp: num_gholes_fill_gholes_gmctxt simp del: fill_gholes_gmctxt.simps)
from holes have less: "GMFun f Cs ≤ ?D1" "GMFun f Cs ≤ ?D2"
by (auto simp del: fill_gholes_gmctxt.simps intro: fill_gholes_gmctxt_less_eq)
have "ghole_poss ?D1 ⊆ ghole_poss (GMFun f Cs)" using less(1) IS(2, 3)
by (intro fill_gholes_gmctxt_ghole_poss_subseteq) (auto simp: nth_append)
then have ext: "gmctxt_p_inv ?D1 ℱ Q" using less(1) IS(7)
using gmctxt_closing_def gmctxt_closing_gmctxt_p_inv_comp less_eq_gmctxt_prime
by blast
have split_last_D1_ss: "fill_gholes C (butlast ts @ [last ss]) =⇩G⇩f (?D1, concat (map (λ x. [x]) (butlast ts) @ [[]]))"
using holes(1) IS(2, 5, 6) unfolding GMFun
by (intro fill_gholes_gmctxt_sound)
(auto simp: nth_append eq_gfill.simps nth_butlast)
have split_last_D2_ss: "fill_gholes C (butlast ts @ [last ss]) =⇩G⇩f (?D2, concat (?rep [] @ [[last ss]]))"
using holes(2) IS(2, 5, 6) unfolding GMFun
by (intro fill_gholes_gmctxt_sound) (auto simp: nth_append
eq_gfill.simps nth_butlast last_conv_nth intro: last_nthI)
have split_last_ts: "fill_gholes C ts =⇩G⇩f (?D2, concat (?rep [] @ [[last ts]]))"
using holes(2) IS(2, 5, 6) unfolding GMFun
by (intro fill_gholes_gmctxt_sound) (auto simp: nth_append
eq_gfill.simps nth_butlast last_conv_nth intro: last_nthI)
from eqgfE[OF split_last_ts] have last_eq: "fill_gholes C ts = fill_gholes ?D2 [last ts]"
by (auto simp del: fill_gholes.simps fill_gholes_gmctxt.simps)
have trans: "fill_gholes ?D1 (butlast ts) = fill_gholes ?D2 [last ss]"
using eqgfE[OF split_last_D1_ss] eqgfE[OF split_last_D2_ss]
by (auto simp del: fill_gholes.simps fill_gholes_gmctxt.simps)
have "ghole_poss ?D2 ⊆ ghole_poss (GMFun f Cs)" using less(2) IS(2, 3, 6)
by (intro fill_gholes_gmctxt_ghole_poss_subseteq) (auto simp: nth_append)
then have "Q (gctxt_of_gmctxt ?D2)" using less(2)
using subsetD[OF assms(2)] IS(2 -  6, 8) holes(2)
by (intro gmctxt_p_invE[OF IS(7)])
(auto simp del: fill_gholes_gmctxt.simps simp: num_gholes_fill_gholes_gmctxt
in_set_conv_nth 𝒯⇩G_equivalent_def nth_butlast, metis less_SucI subsetD)
from gctxtex_onpI[of Q _ "last ss" "last ts" ℛ, OF this] IS(2, 3, 5, 6, 8)
have mem: "(fill_gholes ?D2 [last ss], fill_gholes ?D2 [last ts]) ∈ gctxtex_onp Q ℛ"
using fill_gholes_apply_gctxt[of ?D2 "last ss"]
using fill_gholes_apply_gctxt[of ?D2 "last ts"]
by (auto simp del: gctxt_of_gmctxt.simps fill_gholes_gmctxt.simps fill_gholes.simps)
(metis IS(2) IS(3) append_butlast_last_id diff_Suc_1 length_butlast
length_greater_0_conv lessI nth_append_length)
show ?thesis
proof (cases x)
case 0 then show ?thesis using mem IS(2 - 6) eqgfE[OF split_last_D2_ss] last_eq
by (cases ss; cases ts)
(auto simp del: gctxt_of_gmctxt.simps fill_gholes_gmctxt.simps fill_gholes.simps,
metis IS(3, 5) length_0_conv less_not_refl)
next
case [simp]: (Suc nat)
have "fill_gholes C ss =⇩G⇩f (?D1, concat (map (λ x. [x]) (butlast ss) @ [[]]))"
using holes(1) IS(2, 5, 6) unfolding GMFun
by (intro fill_gholes_gmctxt_sound)
(auto simp del: fill_gholes_gmctxt.simps fill_gholes.simps
simp: nth_append nth_butlast eq_gfill.intros last_nthI)
from eqgfE[OF this] have l: "fill_gholes C ss = fill_gholes ?D1 (butlast ss)"
by (auto simp del: fill_gholes_gmctxt.simps fill_gholes.simps)
from IS(1)[OF h _ _ _ _ ext, of "butlast ss" "butlast ts"] IS(2-) holes(2) h assms(2)
have "(fill_gholes ?D1 (butlast ss), fill_gholes ?D1 (butlast ts)) ∈ (gctxtex_onp Q ℛ)⇧+"
by (auto simp del: gctxt_of_gmctxt.simps fill_gholes_gmctxt.simps fill_gholes.simps
simp: 𝒯⇩G_equivalent_def)
(smt Suc.prems(1) Suc.prems(4) diff_Suc_1 last_conv_nth length_butlast
length_greater_0_conv lessI less_SucI mem_Sigma_iff nth_butlast sig(2) subset_iff 𝒯⇩G_funas_gterm_conv)
then have "(fill_gholes ?D1 (butlast ss), fill_gholes ?D2 [last ts]) ∈ (gctxtex_onp Q ℛ)⇧+"
using mem unfolding trans
by (auto simp del: gctxt_of_gmctxt.simps fill_gholes_gmctxt.simps fill_gholes.simps)
then show ?thesis unfolding last_eq l
by (auto simp del:  fill_gholes_gmctxt.simps fill_gholes.simps)
qed
qed
qed auto
qed

lemma gmctxtex_onp_gctxtex_onp_rtrancl:
assumes sig: "⋀ C. P C ⟹ funas_gmctxt C ⊆ ℱ" "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
and "⋀ C D. P C ⟹ gmctxt_p_inv C ℱ Q"
shows "gmctxtex_onp P ℛ ⊆ (gctxtex_onp Q ℛ)⇧*"
proof
fix s t assume "(s, t) ∈ gmctxtex_onp P ℛ"
then obtain C ss ts where
split: "s = fill_gholes C ss" "t = fill_gholes C ts" and
inv: "num_gholes C = length ss" "num_gholes C = length ts" and
pred: "P C" and rec: "∀ i < length ts. (ss ! i, ts ! i) ∈ ℛ"
by auto
then show "(s, t) ∈ (gctxtex_onp Q ℛ)⇧*"
proof (cases "num_gholes C")
case 0 then show ?thesis using inv unfolding split
by auto
next
case (Suc nat)
from split inv pred rec assms
have "(s, t) ∈ gmctxtex_onp (λ C. P C ∧ 0 < num_gholes C) ℛ" unfolding split
by auto (metis (no_types, lifting) Suc gmctxtex_onpI zero_less_Suc)
moreover have "gmctxtex_onp (λ C. P C ∧ 0 < num_gholes C) ℛ ⊆ (gctxtex_onp Q ℛ)⇧+" using assms
by (intro gmctxtex_onp_gctxtex_onp_trancl) auto
ultimately show ?thesis by auto
qed
qed

lemma rtrancl_gmctxtex_onp_rtrancl_gctxtex_onp_eq:
assumes sig: "⋀ C. P C ⟹ funas_gmctxt C ⊆ ℱ" "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
and "⋀ C D. P C ⟹ gmctxt_p_inv C ℱ Q"
and "compatible_p Q P"
shows "(gmctxtex_onp P ℛ)⇧* = (gctxtex_onp Q ℛ)⇧*" (is "?Ls⇧* = ?Rs⇧*")
proof -
from assms(4) have "?Rs ⊆ ?Ls" by auto
then have "?Rs⇧* ⊆ ?Ls⇧*"
moreover from gmctxtex_onp_gctxtex_onp_rtrancl[OF assms(1 - 3), of P]
have "?Ls⇧* ⊆ ?Rs⇧*"
ultimately show ?thesis by blast
qed

subsection ‹Extensions to reflexive transitive closures›

lemma gctxtex_onp_substep_trancl:
assumes "gctxtex_onp P ℛ ⊆ ℛ"
shows "gctxtex_onp P (ℛ⇧+) ⊆ ℛ⇧+"
proof -
{fix s t assume "(s, t) ∈ gctxtex_onp P (ℛ⇧+)"
then obtain C u v where rec: "(u, v) ∈ ℛ⇧+" "P C" and t: "s = C⟨u⟩⇩G" "t = C⟨v⟩⇩G"
by auto
from rec have "(s, t) ∈ ℛ⇧+" unfolding t
proof (induct)
case (base y)
then show ?case using assms by auto
next
case (step y z)
from assms step(2, 4) have "(C⟨y⟩⇩G, C⟨z⟩⇩G) ∈ ℛ" by auto
then show ?case using step by auto
qed}
then show ?thesis by auto
qed

lemma gctxtex_onp_substep_rtrancl:
assumes "gctxtex_onp P ℛ ⊆ ℛ"
shows "gctxtex_onp P (ℛ⇧*) ⊆ ℛ⇧*"
using gctxtex_onp_substep_trancl[OF assms]
by (smt gctxtex_onpE gctxtex_onpI rtrancl_eq_or_trancl subrelI subset_eq)

lemma gctxtex_onp_substep_trancl_diff_pred [intro]:
assumes "⋀ C D. P C ⟹ Q D ⟹ Q (D ∘⇩G⇩c C)"
shows "gctxtex_onp Q ((gctxtex_onp P ℛ)⇧+) ⊆ (gctxtex_onp Q ℛ)⇧+"
proof
fix s t assume "(s, t) ∈ gctxtex_onp Q ((gctxtex_onp P ℛ)⇧+)"
from gctxtex_onpE[OF this] obtain C u v where
*: "s = C⟨u⟩⇩G" "t = C⟨v⟩⇩G" and inv: "Q C" and mem: "(u, v) ∈ (gctxtex_onp P ℛ)⇧+"
by blast
show "(s, t) ∈ (gctxtex_onp Q ℛ)⇧+" using mem * inv
proof (induct arbitrary: s t)
case (base y)
then show ?case using assms
by (auto elim!: gctxtex_onpE intro!: r_into_trancl) (metis ctxt_ctxt_compose gctxtex_onpI)
next
case (step y z)
from step(2) have "(C⟨y⟩⇩G, C⟨z⟩⇩G) ∈ gctxtex_onp Q ℛ"
using assms[OF _ step(6)]
by (auto elim!: gctxtex_onpE) (metis ctxt_ctxt_compose gctxtex_onpI)
then show ?case using step(3)[of s "C⟨y⟩⇩G"] step(1, 2, 4-)
by auto
qed
qed

lemma gctxtcl_pres_trancl:
assumes "(s, t) ∈ ℛ⇧+" and "gctxtex_onp P ℛ ⊆ ℛ" and "P C"
shows "(C⟨s⟩⇩G, C⟨t⟩⇩G) ∈ ℛ⇧+"
using gctxtex_onp_substep_trancl [OF assms(2)] assms(1, 3)
by auto

lemma gctxtcl_pres_rtrancl:
assumes "(s, t) ∈ ℛ⇧*" and "gctxtex_onp P ℛ ⊆ ℛ" and "P C"
shows "(C⟨s⟩⇩G, C⟨t⟩⇩G) ∈ ℛ⇧*"
using assms(1) gctxtcl_pres_trancl[OF _ assms(2, 3)]
unfolding rtrancl_eq_or_trancl
by (cases "s = t") auto

lemma gmctxtex_onp_substep_trancl:
assumes "gmctxtex_onp P ℛ ⊆ ℛ"
and "Id_on (snd ` ℛ) ⊆ ℛ"
shows "gmctxtex_onp P (ℛ⇧+) ⊆ ℛ⇧+"
proof -
{fix s t assume "(s, t) ∈ gmctxtex_onp P (ℛ⇧+)"
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: "P C" "∀ i < length vs. (us ! i, vs ! i) ∈ ℛ⇧+" by auto
have "(s, t) ∈ ℛ⇧+" using len(2) inv(2) len(1) inv(1) unfolding *
proof (induction rule: trancl_list_induct)
case (base xs ys)
then have "(fill_gholes C xs, fill_gholes C ys) ∈ ℛ" using assms(1)
by blast
then show ?case by auto
next
case (step xs ys i z)
have sub: "set ys ⊆ snd ` ℛ" using step(1, 2)
by (auto simp: image_def) (metis in_set_idx snd_conv tranclD2)
from step have lft: "(fill_gholes C xs, fill_gholes C ys) ∈ ℛ⇧+" by auto
have "(fill_gholes C ys, fill_gholes C (ys[i := z])) ∈ gmctxtex_onp P ℛ"
using step(3, 4) sub assms step(1, 6)
by (intro gmctxtex_onpI[of P, OF step(7), of ys "ys[i := z]" ℛ])
then have "(fill_gholes C ys, fill_gholes C (ys[i := z])) ∈ ℛ" using assms(1) by blast
then show ?case using lft by auto
qed}
then show ?thesis by auto
qed

lemma gmctxtex_onp_substep_tranclE:
assumes "trans ℛ" and "gmctxtex_onp Q ℛ O ℛ ⊆ ℛ" and "ℛ O gmctxtex_onp Q ℛ ⊆ ℛ"
and "⋀ p C. P C ⟹ p ∈ poss_gmctxt C ⟹ Q (subgm_at C p)"
and "⋀ C D. P C ⟹ P D ⟹ (C, D) ∈ comp_gmctxt ⟹ P (C ⊓ D)"
shows "(gmctxtex_onp P ℛ)⇧+ = gmctxtex_onp P ℛ" (is "?Ls = ?Rs")
proof
show "?Rs ⊆ ?Ls" using trancl_mono_set by fastforce
next
{fix s t assume "(s, t) ∈ ?Ls" then have "(s, t) ∈ ?Rs"
proof induction
case (step t u)
from step(3) obtain C us vs where
*: "s = fill_gholes C us" "t = fill_gholes C vs" and
l: "num_gholes C = length us" "length us = length vs" and
inv: "P C" "∀i<length vs. (us ! i, vs ! i) ∈ ℛ"
by auto
from step(2) obtain D xs ys where
**: "t = fill_gholes D xs" "u = fill_gholes D ys" and
l': "num_gholes D = length xs" "length xs = length ys" and
inv': "P D" "∀i<length ys. (xs ! i, ys ! i) ∈ ℛ"
by auto
let ?C' = "C ⊓ D"
let ?sss = "unfill_gholes ?C' s" let ?uss = "unfill_gholes ?C' u"
have less: "?C' ≤ gmctxt_of_gterm s" "?C' ≤ gmctxt_of_gterm u"
using eq_gfill.intros eqgf_less_eq inf.coboundedI1 inf.coboundedI2 l(1) l'(1)
unfolding * ** unfolding l'(2)
by metis+
from *(2) **(1) have comp: "(C, D) ∈ comp_gmctxt" using l l'
using eqgf_comp_gmctxt by fastforce
then have P: "P ?C'" using inv(1) inv'(1) assms(5) by blast
moreover have l'': "num_gholes ?C' = length ?sss" "length ?sss = length ?uss"
using less by auto
moreover have fill: "fill_gholes ?C' ?sss = s" "fill_gholes ?C' ?uss = u"
using less by (simp add: fill_unfill_gholes)+
moreover have "∀ i < length ?uss. (?sss ! i, ?uss ! i) ∈ ℛ"
proof (rule, rule)
fix i assume i: "i < length (unfill_gholes ?C' u)"
then obtain p where pos: "p ∈ ghole_poss ?C'"
"unfill_gholes ?C' s ! i = gsubt_at (fill_gholes ?C' ?sss) p"
"unfill_gholes ?C' u ! i = gsubt_at (fill_gholes ?C' ?uss) p"
using fill l'' fill_gholes_ghole_poss
by (metis eq_gfill.intros ghole_poss_ghole_poss_list_conv length_ghole_poss_list_num_gholes nth_mem)
from comp_gmctxt_inf_ghole_poss_cases[OF comp pos(1)]
consider (a) "p ∈ ghole_poss C ∧ p ∈ ghole_poss D" |
(b) "p ∈ ghole_poss C ∧ p ∈ poss_gmctxt D" |
(c) "p ∈ ghole_poss D ∧ p ∈ poss_gmctxt C" by blast
then show "(unfill_gholes ?C' s ! i, unfill_gholes ?C' u ! i) ∈ ℛ" unfolding pos fill
proof cases
case a
then show "(gsubt_at s p, gsubt_at u p) ∈ ℛ"
using assms(1) *(2) l l' inv(2) inv'(2) unfolding * **
using ghole_poss_nth_subt_at
by (metis "*"(2) "**"(1) eq_gfill.intros trancl_id trancl_into_trancl2)
next
case b
then have sp: "gsubt_at t p =⇩G⇩f (subgm_at D p, gmctxt_subtgm_at_fill_args p D xs)"
"gsubt_at u p =⇩G⇩f (subgm_at D p, gmctxt_subtgm_at_fill_args p D ys)"
using poss_gmctxt_fill_gholes_split[of _ D _ p] ** l'
by force+
have "(gsubt_at t p, gsubt_at u p) ∈ gmctxtex_onp Q ℛ" using inv'(2)
using assms(4)[OF inv'(1) conjunct2[OF b]] eqgfE[OF sp(1)] eqgfE[OF sp(2)]
by (auto simp: gmctxt_subtgm_at_fill_args_def intro!: gmctxtex_onpI)
moreover have "(gsubt_at s p, gsubt_at t p) ∈ ℛ"
using * l inv(2)
using ghole_poss_nth_subt_at[OF _ conjunct1[OF b]]
by auto (metis eq_gfill.intros)
ultimately show "(gsubt_at s p, gsubt_at u p) ∈ ℛ"
using assms(3) by auto
next
case c
then have sp: "gsubt_at s p =⇩G⇩f (subgm_at C p, gmctxt_subtgm_at_fill_args p C us)"
"gsubt_at t p =⇩G⇩f (subgm_at C p, gmctxt_subtgm_at_fill_args p C vs)"
using poss_gmctxt_fill_gholes_split[of _ C _ p] * l
by force+
have "(gsubt_at s p, gsubt_at t p) ∈ gmctxtex_onp Q ℛ" using inv(2)
using assms(4)[OF inv(1) conjunct2[OF c]] eqgfE[OF sp(1)] eqgfE[OF sp(2)]
by (auto simp: gmctxt_subtgm_at_fill_args_def intro!: gmctxtex_onpI)
moreover have "(gsubt_at t p, gsubt_at u p) ∈ ℛ"
using ** l' inv'(2)
using ghole_poss_nth_subt_at[OF _ conjunct1[OF c]]
by auto (metis eq_gfill.intros)
ultimately show "(gsubt_at s p, gsubt_at u p) ∈ ℛ"
using assms(2) by auto
qed
qed
ultimately show ?case by (metis gmctxtex_onpI)
qed simp}
then show "?Ls ⊆ ?Rs" by auto
qed

subsection ‹Restr to set, union and predicate distribution›

lemma Restr_gctxtex_onp_dist [simp]:
"Restr (gctxtex_onp P ℛ) (𝒯⇩G ℱ) =
gctxtex_onp (λ C. funas_gctxt C ⊆ ℱ ∧ P C) (Restr ℛ (𝒯⇩G ℱ))"
by (auto simp: gctxtex_onp_def 𝒯⇩G_equivalent_def) blast

lemma Restr_gmctxtex_onp_dist [simp]:
"Restr (gmctxtex_onp P ℛ) (𝒯⇩G ℱ) =
gmctxtex_onp  (λ C. funas_gmctxt C ⊆ ℱ ∧ P C) (Restr ℛ (𝒯⇩G ℱ))"
by (auto elim!: gmctxtex_onpE simp: 𝒯⇩G_equivalent_def SUP_le_iff gmctxtex_onpI)
(metis in_set_idx subsetD)+

lemma Restr_id_subset_gmctxtex_onp [intro]:
assumes "⋀ C. num_gholes C = 0 ∧ funas_gmctxt C ⊆ ℱ ⟹ P C"
shows "Restr Id (𝒯⇩G ℱ) ⊆ gmctxtex_onp P ℛ"
proof
fix s t assume "(s, t) ∈ Restr Id (𝒯⇩G ℱ)"
then show "(s, t) ∈ gmctxtex_onp P ℛ" using assms[of "gmctxt_of_gterm t"]
using gmctxtex_onpI[of P "gmctxt_of_gterm t" "[]" "[]" ℛ]
by (auto simp: 𝒯⇩G_equivalent_def)
qed

lemma Restr_id_subset_gmctxtex_onp2 [intro]:
assumes "⋀ f n. (f, n) ∈ ℱ ⟹ P (GMFun f (replicate n GMHole))"
and "⋀ C Ds. num_gholes C = length Ds ⟹ P C ⟹ ∀ D ∈ set Ds. P D ⟹ P (fill_gholes_gmctxt C Ds)"
shows "Restr Id (𝒯⇩G ℱ) ⊆ gmctxtex_onp P ℛ"
proof
fix s t assume "(s, t) ∈ Restr Id (𝒯⇩G ℱ)"
then have *: "s = t" "t ∈ 𝒯⇩G ℱ" by auto
have "P (gmctxt_of_gterm t)" using *(2)
proof (induct)
case (const a)
show ?case using assms(1)[OF const] by auto
next
case (ind f n ss)
let ?C = "GMFun f (replicate (length ss) GMHole)"
have "P (fill_gholes_gmctxt ?C (map gmctxt_of_gterm ss))"
using assms(1)[OF ind(1)] ind
by (intro assms(2)) (auto simp: in_set_conv_nth)
then show ?case
by (metis fill_gholes_gmctxt_GMFun_replicate_length gmctxt_of_gterm.simps length_map)
qed
from gmctxtex_onpI[of P, OF this] show "(s, t) ∈ gmctxtex_onp P ℛ" unfolding *
by auto
qed

lemma gctxtex_onp_union [simp]:
"gctxtex_onp P (ℛ ∪ ℒ) = gctxtex_onp P ℛ ∪ gctxtex_onp P ℒ"
by auto

lemma gctxtex_onp_pred_dist:
assumes "⋀ C. P C ⟷ Q C ∨ R C"
shows "gctxtex_onp P ℛ = gctxtex_onp Q ℛ ∪ gctxtex_onp R ℛ"
using assms by auto fastforce

lemma gmctxtex_onp_pred_dist:
assumes "⋀ C. P C ⟷ Q C ∨ R C"
shows "gmctxtex_onp P ℛ = gmctxtex_onp Q ℛ ∪ gmctxtex_onp R ℛ"
using assms by (auto elim!: gmctxtex_onpE)

lemma trivial_gctxtex_onp [simp]: "gctxtex_onp (λ C. C = □⇩G) ℛ = ℛ"
using gctxtex_closure by force

lemma trivial_gmctxtex_onp [simp]: "gmctxtex_onp (λ C. C = GMHole) ℛ = ℛ"
proof
show "gmctxtex_onp (λC. C = GMHole) ℛ ⊆ ℛ"
by (auto elim!: gmctxtex_onpE) force
next
show "ℛ ⊆ gmctxtex_onp (λC. C = GMHole) ℛ"
by (intro gmctxtex_closure) auto
qed

subsection ‹Distribution of context closures over relation composition›

lemma gctxtex_onp_relcomp_inner:
"gctxtex_onp P (ℛ O ℒ) ⊆ gctxtex_onp P ℛ O gctxtex_onp P ℒ"
by auto

lemma gmctxtex_onp_relcomp_inner:
"gmctxtex_onp P (ℛ O ℒ) ⊆ gmctxtex_onp P ℛ O gmctxtex_onp P ℒ"
proof
fix s t
assume "(s, t) ∈ gmctxtex_onp P (ℛ O ℒ)"
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: "P C" "∀ i < length vs. (us ! i, vs ! i) ∈ ℛ O ℒ" by blast
obtain zs where l: "length vs = length zs" and
rel: "∀ i < length zs. (us ! i, zs ! i) ∈ ℛ" "∀ i < length zs. (zs ! i, vs ! i) ∈ ℒ"
using len(2) inv(2) Ex_list_of_length_P[of _ "λ y i. (us ! i, y) ∈ ℛ ∧ (y, vs ! i) ∈ ℒ"]
by (auto simp: relcomp_unfold) metis
from len l rel inv have "(s, fill_gholes C zs) ∈ gmctxtex_onp P ℛ" unfolding *
by auto
moreover from len l rel inv have "(fill_gholes C zs, t) ∈ gmctxtex_onp P ℒ" unfolding *
by auto
ultimately show "(s, t) ∈ gmctxtex_onp P ℛ O gmctxtex_onp P ℒ"
by auto
qed

subsection ‹Signature preserving and signature closed›

definition function_closed where
"function_closed ℱ ℛ ⟷ (∀ f ss ts. (f, length ts) ∈ ℱ ⟶ 0 ≠ length ts ⟶
length ss = length ts ⟶ (∀ i. i < length ts ⟶ (ss ! i, ts ! i) ∈ ℛ) ⟶
(GFun f ss, GFun f ts) ∈ ℛ)"

lemma function_closedD: "function_closed ℱ ℛ ⟹
(f,length ts) ∈ ℱ ⟹ 0 ≠ length ts ⟹ length ss = length ts ⟹
⟦⋀ i. i < length ts ⟹ (ss ! i, ts ! i) ∈ ℛ⟧ ⟹
(GFun f ss, GFun f ts) ∈ ℛ"
unfolding function_closed_def by blast

lemma all_ctxt_closed_imp_function_closed:
"all_ctxt_closed ℱ ℛ ⟹ function_closed ℱ ℛ"
unfolding all_ctxt_closed_def function_closed_def
by auto

lemma all_ctxt_closed_imp_reflx_on_sig:
assumes "all_ctxt_closed ℱ ℛ"
shows "Restr Id (𝒯⇩G ℱ) ⊆ ℛ"
proof -
{fix s assume "(s, s) ∈ Restr Id (𝒯⇩G ℱ)" then have "(s, s) ∈ ℛ"
proof (induction s)
case (GFun f ts)
then show ?case using all_ctxt_closedD[OF assms]
by (auto simp: 𝒯⇩G_equivalent_def UN_subset_iff)
qed}
then show ?thesis by auto
qed

lemma function_closed_un_id_all_ctxt_closed:
"function_closed ℱ ℛ ⟹ Restr Id (𝒯⇩G ℱ) ⊆ ℛ ⟹ all_ctxt_closed ℱ ℛ"
unfolding all_ctxt_closed_def
by (auto dest: function_closedD simp: subsetD)

lemma gctxtex_onp_in_signature [intro]:
assumes "⋀ C. P C ⟹ funas_gctxt C ⊆ ℱ" "⋀ C. P C ⟹ funas_gctxt C ⊆ 𝒢"
and "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G 𝒢"
shows "gctxtex_onp P ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G 𝒢" using assms
by (auto simp: gctxtex_onp_def 𝒯⇩G_equivalent_def) blast+

lemma gmctxtex_onp_in_signature [intro]:
assumes "⋀ C. P C ⟹ funas_gmctxt C ⊆ ℱ" "⋀ C. P C ⟹ funas_gmctxt C ⊆ 𝒢"
and "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G 𝒢"
shows "gmctxtex_onp P ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G 𝒢" using assms
by (auto simp: gmctxtex_onp_def 𝒯⇩G_equivalent_def in_set_conv_nth) force+

lemma gctxtex_onp_in_signature_tranc [intro]:
"gctxtex_onp P ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ ⟹ (gctxtex_onp P ℛ)⇧+ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
by (auto simp: Restr_simps)

lemma gmctxtex_onp_in_signature_tranc [intro]:
"gmctxtex_onp P ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ ⟹ (gmctxtex_onp P ℛ)⇧+ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
by (auto simp: Restr_simps)

lemma gmctxtex_onp_fun_closed [intro!]:
assumes "⋀ f n. (f, n) ∈ ℱ ⟹ n ≠ 0 ⟹ P (GMFun f (replicate n GMHole))"
and "⋀ C Ds. P C ⟹ num_gholes C = length Ds ⟹ 0 < num_gholes C ⟹
∀ D ∈ set Ds. P D ⟹ P (fill_gholes_gmctxt C Ds)"
shows "function_closed ℱ (gmctxtex_onp P ℛ)" unfolding function_closed_def
proof (rule allI, intro allI, intro impI)
fix f ss ts assume sig: "(f, length ts) ∈ ℱ"
and len: "0 ≠ length ts" "length ss = length ts"
and mem: "∀ i < length ts. (ss ! i, ts ! i) ∈ gmctxtex_onp P ℛ"
let ?C = "GMFun f (replicate (length ts) GMHole)"
from mem len obtain Ds sss tss where
l': "length ts = length Ds" "length Ds = length sss" "length sss = length tss" and
inn: "∀ i < length tss. length (sss ! i) = length (tss ! i)" and
eq: "∀ i < length tss. ss ! i =⇩G⇩f (Ds ! i, sss ! i)" "∀ i < length tss. ts ! i =⇩G⇩f (Ds ! i, tss ! i)" and
inv: "∀ i < length (concat tss). (concat sss ! i, concat tss ! i) ∈ ℛ" "∀ D ∈ set Ds. P D"
by (auto elim!: gmctxtex_onp_listE)
have *: "fill_gholes ?C ss = GFun f ss" "fill_gholes ?C ts = GFun f ts"
using len assms(1) by (auto simp del: fill_gholes.simps)
have s: "GFun f ss =⇩G⇩f (fill_gholes_gmctxt ?C Ds, concat sss)"
using assms(1) l' eq(1) inn len inv(1) unfolding *[symmetric]
by (intro fill_gholes_gmctxt_sound) auto
have t: "GFun f ts =⇩G⇩f (fill_gholes_gmctxt ?C Ds, concat tss)"
using assms(1) eq l' inn len inv(1) unfolding *[symmetric]
by (intro fill_gholes_gmctxt_sound) auto
then show "(GFun f ss, GFun f ts) ∈ gmctxtex_onp P ℛ"
unfolding eqgfE[OF s] eqgfE[OF t]
using eqgfE(2)[OF s] eqgfE(2)[OF t] sig len l' inv
using assms(1)[OF sig] assms(2)[of "GMFun f (replicate (length ts) GMHole)" Ds]
using gmctxtex_onpI[of P "fill_gholes_gmctxt (GMFun f (replicate (length ts) GMHole)) Ds" "concat sss" "concat tss" ℛ]
by (auto simp del: fill_gholes_gmctxt.simps fill_gholes.simps)
qed

declare subsetI[rule del]
lemma gmctxtex_onp_sig_closed [intro]:
assumes "⋀ f n. (f, n) ∈ ℱ ⟹ P (GMFun f (replicate n GMHole))"
and  "⋀ C Ds. num_gholes C = length Ds ⟹ P C ⟹ ∀ D ∈ set Ds. P D ⟹ P (fill_gholes_gmctxt C Ds)"
shows "all_ctxt_closed ℱ (gmctxtex_onp P ℛ)" using assms
by (intro function_closed_un_id_all_ctxt_closed) auto
declare subsetI[intro!]

lemma gmctxt_cl_gmctxtex_onp_conv:
"gmctxt_cl ℱ ℛ = gmctxtex_onp (λ C. funas_gmctxt C ⊆ ℱ) ℛ" (is "?Ls = ?Rs")
proof -
have sig_cl: "all_ctxt_closed ℱ (?Rs)" by (intro gmctxtex_onp_sig_closed) auto
{fix s t assume "(s, t) ∈ ?Ls" then have "(s, t) ∈ ?Rs"
proof induct
case (step ss ts f)
then show ?case using all_ctxt_closedD[OF sig_cl]
by force
qed (intro subsetD[OF gmctxtex_onp_arg_monoI], auto)}
moreover
{fix s t assume "(s, t) ∈ ?Rs"
from gmctxtex_onpE[OF this] obtain C us vs where
terms: "s = fill_gholes C us" "t = fill_gholes C vs" and
fill_inv: "num_gholes C = length us" "length us = length vs" and
rel: "funas_gmctxt C ⊆ ℱ" "∀ i < length vs. (us ! i, vs ! i) ∈ ℛ" by blast
have "(s, t) ∈ ?Ls" unfolding terms using fill_inv rel
proof (induct C arbitrary: us vs)
case GMHole
then show ?case using rel(2) by (cases vs; cases us) auto
next
case (GMFun f Ds)
show ?case using GMFun(2-) unfolding partition_holes_fill_gholes_conv'
by (intro all_ctxt_closedD[OF gmctxt_cl_is_all_ctxt_closed[of ℱ ℛ]])
(auto simp: partition_by_nth_nth SUP_le_iff length_partition_gholes_nth intro!: GMFun(1))
qed}
ultimately show ?thesis by auto
qed

end```