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    (ClG, CrG)  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 𝒢))"
  by (auto simp add: gnrrstepD_def)

lemma Restr_grstepD_dist [simp]:
  "Restr (grstepD  ) (𝒯G 𝒢) = grstepD (  𝒢) (Restr  (𝒯G 𝒢))"
  by (auto simp add: grstepD_def)

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 = Cl  (σ :: 'b  ('a, 'b) term)" "term_of_gterm t = Cr  σ"
      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 = Cl  (σ :: 'b  ('a, 'b) term)" "term_of_gterm t = Cr  σ"
      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"
        by (simp add: gpar_rstep_def inv_image_def)
    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)]
    by (simp add: gctxtex_onp_rel_mono)
  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 Gc 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 = CuG" "t = CvG" 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 "(CyG, CzG)   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)]
    by (simp add: gmctxtex_onp_rel_mono)
  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)+"
  by (simp add: relax_pos_lift_root_step trancl_mono_set)

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"
  by (simp add: compatible_p_gctxtex_gmctxtex_subseteq)

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
  by (simp add: gnrrstepD_def)

(* Restoring Isabelle standard attributes to lemmas *)
declare subsetI [intro!] 
declare lift_root_step.simps[simp del]

lemma gpar_rstepD_grstepD_rtrancl_subseteq:
  assumes "  𝒯G  × 𝒯G "
  shows "gpar_rstepD    (grstepD  )*"
  using assms unfolding gpar_rstepD_def grstepD_def
  by (intro gmctxtex_onp_gctxtex_onp_rtrancl) (auto simp: 𝒯G_equivalent_def gmctxt_p_inv_def)
end