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)"
      by (simp add: fill_gholes_gmctxt_less_eq)
    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)"
      by (simp add: fill_gholes_gmctxt_less_eq)
    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⇧*"
    by (simp add: rtrancl_mono) 
  moreover from gmctxtex_onp_gctxtex_onp_rtrancl[OF assms(1 - 3), of P]
  have "?Ls⇧* ⊆ ?Rs⇧*"
    by (simp add: rtrancl_subset_rtrancl) 
  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]" ℛ])
          (simp add: Id_on_eqI nth_list_update subset_iff)+
      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