Theory Rewriting

section ‹Rewriting›
theory Rewriting
  imports Terms_Positions
begin

subsection ‹Basic rewrite definitions›

subsubsection ‹Rewrite steps with implicit signature declaration (encoded in the type)›

inductive_set rrstep :: "('f, 'v) term rel ⇒ ('f, 'v) term rel" for ℛ where
  [intro]: "(l, r) ∈ ℛ ⟹ (l ⋅ σ, r ⋅ σ) ∈ rrstep ℛ"

inductive_set rstep :: "('f, 'v) term rel ⇒ ('f, 'v) term rel" for ℛ where
  "(s, t) ∈ rrstep ℛ ⟹ (C⟨s⟩, C⟨t⟩) ∈ rstep ℛ"


subsubsection ‹Restrict relations to terms induced by a given signature›

definition "sig_step ℱ ℛ = Restr ℛ (Collect (λ s. funas_term s ⊆ ℱ))"

subsubsection ‹Rewriting under a given signature/restricted to ground terms›

abbreviation "srrstep ℱ ℛ ≡ sig_step ℱ (rrstep ℛ)"
abbreviation "srstep ℱ ℛ ≡ sig_step ℱ (rstep ℛ)"
abbreviation "gsrstep ℱ ℛ ≡ Restr (sig_step ℱ (rstep ℛ)) (Collect ground)"


subsubsection ‹Rewriting sequences involving a root step›

abbreviation (input) relto :: "'a rel ⇒ 'a rel ⇒ 'a rel" where
  "relto R S ≡ S^* O R O S^*"
definition "srsteps_with_root_step ℱ ℛ ≡ relto (sig_step ℱ (rrstep ℛ)) (srstep ℱ ℛ)"


subsection ‹Monotonicity laws›

lemma Restr_mono: "Restr r A ⊆ r" by auto

lemma Restr_trancl_mono_set: "(Restr r A)⇧+ ⊆ A × A"
  by (simp add: trancl_subset_Sigma)

lemma rrstep_rstep_mono: "rrstep ℛ ⊆ rstep ℛ"
  by (auto intro: rstep.intros[where ?C = □, simplified])

lemma sig_step_mono:
  "ℱ ⊆ 𝒢 ⟹ sig_step ℱ ℛ ⊆ sig_step 𝒢 ℛ"
  by (auto simp: sig_step_def)

lemma sig_step_mono2:
  "ℛ ⊆ ℒ ⟹ sig_step ℱ ℛ ⊆ sig_step ℱ ℒ"
  by (auto simp: sig_step_def)

lemma srrstep_monp:
  "ℱ ⊆ 𝒢 ⟹ srrstep ℱ ℛ ⊆ srrstep 𝒢 ℛ"
  by (simp add: sig_step_mono)

lemma srstep_monp:
  "ℱ ⊆ 𝒢 ⟹ srstep ℱ ℛ ⊆ srstep 𝒢 ℛ"
  by (simp add: sig_step_mono)

lemma srsteps_monp:
  "ℱ ⊆ 𝒢 ⟹ (srstep ℱ ℛ)⇧+ ⊆ (srstep 𝒢 ℛ)⇧+"
  by (simp add: sig_step_mono trancl_mono_set)

lemma srsteps_eq_monp:
  "ℱ ⊆ 𝒢 ⟹ (srstep ℱ ℛ)⇧* ⊆ (srstep 𝒢 ℛ)⇧*"
  by (meson rtrancl_mono sig_step_mono subrelI subsetD trancl_into_rtrancl)
  
lemma srsteps_with_root_step_sig_mono:
   "ℱ ⊆ 𝒢 ⟹ srsteps_with_root_step ℱ ℛ ⊆ srsteps_with_root_step 𝒢 ℛ"
  unfolding srsteps_with_root_step_def
  by (simp add: relcomp_mono srrstep_monp srsteps_eq_monp)


subsection ‹Introduction, elimination, and destruction rules for @{const sig_step}, @{const rstep}, @{const rrstep},
   @{const srrstep}, and @{const srstep}›

lemma sig_stepE [elim, consumes 1]:
  "(s, t) ∈ sig_step ℱ ℛ ⟹ ⟦(s, t) ∈ ℛ ⟹ funas_term s ⊆ ℱ ⟹ funas_term t ⊆ ℱ ⟹ P⟧ ⟹ P"
  by (auto simp: sig_step_def)

lemma sig_stepI [intro]:
  "funas_term s ⊆ ℱ ⟹ funas_term t ⊆ ℱ ⟹ (s, t) ∈ ℛ ⟹ (s, t) ∈ sig_step ℱ ℛ"
  by (auto simp: sig_step_def)

lemma rrstep_subst [elim, consumes 1]:
  assumes "(s, t) ∈ rrstep ℛ"
  obtains l r σ where "(l, r) ∈ ℛ" "s = l ⋅ σ" "t = r ⋅ σ" using assms
  by (meson rrstep.simps)
  
lemma rstep_imp_C_s_r:
  assumes "(s, t) ∈ rstep ℛ"
  shows "∃C σ l r. (l,r) ∈ ℛ ∧ s = C⟨l⋅σ⟩ ∧ t = C⟨r⋅σ⟩"using assms
  by (metis rrstep.cases rstep.simps)

  
lemma rstep_imp_C_s_r' [elim, consumes 1]:
  assumes "(s, t) ∈ rstep ℛ"
  obtains C l r σ where "(l,r) ∈ ℛ" "s = C⟨l⋅σ⟩" "t = C⟨r⋅σ⟩" using assms
  using rstep_imp_C_s_r by blast

lemma rrstep_basicI [intro]:
  "(l, r) ∈ ℛ ⟹ (l, r) ∈ rrstep ℛ"
  by (metis rrstepp.intros rrstepp_rrstep_eq subst_apply_term_empty)

lemma rstep_ruleI [intro]:
  "(l, r) ∈ ℛ ⟹ (l, r) ∈ rstep ℛ"
  using rrstep_rstep_mono by blast

lemma rstepI [intro]:
  "(l, r) ∈ ℛ ⟹ s = C⟨l ⋅ σ⟩ ⟹ t = C⟨r ⋅ σ⟩ ⟹ (s, t) ∈ rstep ℛ"
  by (simp add: rrstep.intros rstep.intros)

lemma rstep_substI [intro]:
  "(s, t) ∈ rstep ℛ ⟹ (s ⋅ σ, t ⋅ σ) ∈ rstep ℛ"
  by (auto elim!: rstep_imp_C_s_r' simp flip: subst_subst_compose)

lemma rstep_ctxtI [intro]:
  "(s, t) ∈ rstep ℛ ⟹ (C⟨s⟩, C⟨t⟩) ∈ rstep ℛ"
  by (auto elim!: rstep_imp_C_s_r' simp flip: ctxt_ctxt_compose)

lemma srrstepD:
  "(s, t) ∈ srrstep ℱ ℛ ⟹ (s, t) ∈ rrstep ℛ ∧ funas_term s ⊆ ℱ ∧ funas_term t ⊆ ℱ"
  by (auto simp: sig_step_def)

lemma srstepD:
  "(s, t) ∈ (srstep ℱ ℛ) ⟹ (s, t) ∈ rstep ℛ ∧ funas_term s ⊆ ℱ ∧ funas_term t ⊆ ℱ"
  by (auto simp: sig_step_def)

lemma srstepsD:
  "(s, t) ∈ (srstep ℱ ℛ)⇧+ ⟹ (s, t) ∈ (rstep ℛ)⇧+ ∧ funas_term s ⊆ ℱ ∧ funas_term t ⊆ ℱ"
  unfolding sig_step_def using trancl_mono_set[OF Restr_mono] 
  by (auto simp: sig_step_def dest: subsetD[OF Restr_trancl_mono_set])


subsubsection ‹Transitive and relfexive closure distribution over @{const sig_step}›

lemma funas_rel_converse:
  "funas_rel ℛ ⊆ ℱ ⟹ funas_rel (ℛ¯) ⊆ ℱ" unfolding funas_rel_def
  by auto

lemma rstep_term_to_sig_r:
  assumes "(s, t) ∈ rstep ℛ" and "funas_rel ℛ ⊆ ℱ" and "funas_term s ⊆ ℱ"
  shows "(s, term_to_sig ℱ v t) ∈ rstep ℛ"
proof -
  from assms(1) obtain C l r σ where
    *: "s = C⟨l ⋅ σ⟩" "t = C⟨r ⋅ σ⟩" "(l, r) ∈ ℛ" by auto
  from assms(2, 3) *(3) have "funas_ctxt C ⊆ ℱ" "funas_term l ⊆ ℱ" "funas_term r ⊆ ℱ"
    by (auto simp: *(1) funas_rel_def funas_term_subst subset_eq)
  then have "(term_to_sig ℱ v s, term_to_sig ℱ v t) ∈ rstep ℛ" using *(3)
    by (auto simp: *(1, 2) funas_ctxt_ctxt_well_def_hole_path)
  then show ?thesis using assms(3) by auto
qed

lemma rstep_term_to_sig_l:
  assumes "(s, t) ∈ rstep ℛ" and "funas_rel ℛ ⊆ ℱ" and "funas_term t ⊆ ℱ"
  shows "(term_to_sig ℱ v s, t) ∈ rstep ℛ"
proof -
  from assms(1) obtain C l r σ where
    *: "s = C⟨l ⋅ σ⟩" "t = C⟨r ⋅ σ⟩" "(l, r) ∈ ℛ" by auto
  from assms(2, 3) *(3) have "funas_ctxt C ⊆ ℱ" "funas_term l ⊆ ℱ" "funas_term r ⊆ ℱ"
    by (auto simp: *(2) funas_rel_def funas_term_subst subset_eq)
  then have "(term_to_sig ℱ v s, term_to_sig ℱ v t) ∈ rstep ℛ" using *(3)
    by (auto simp: *(1, 2) funas_ctxt_ctxt_well_def_hole_path)
  then show ?thesis using assms(3) by auto
qed

lemma rstep_trancl_sig_step_r:
  assumes "(s, t) ∈ (rstep ℛ)⇧+" and "funas_rel ℛ ⊆ ℱ" and "funas_term s ⊆ ℱ"
  shows "(s, term_to_sig ℱ v t) ∈ (srstep ℱ ℛ)⇧+" using assms
proof (induct)
  case (base t)
  then show ?case using subsetD[OF fuans_term_term_to_sig, of _ ℱ v]
    by (auto simp: rstep_term_to_sig_r sig_step_def intro!: r_into_trancl)
next
  case (step t u)
  then have st: "(s, term_to_sig ℱ v t) ∈ (srstep ℱ ℛ)⇧+" by auto
  from step(2) obtain  C l r σ where
    *: "t = C⟨l ⋅ σ⟩" "u = C⟨r ⋅ σ⟩" "(l, r) ∈ ℛ" by auto
  show ?case
  proof (cases "ctxt_well_def_hole_path ℱ C")
    case True
    from *(3) step(4) have "funas_term l ⊆ ℱ" "funas_term r ⊆ ℱ" by (auto simp: funas_rel_def)
    then have "(term_to_sig ℱ v t, term_to_sig ℱ v u) ∈ rstep ℛ"
      using True step(2) *(3) unfolding *
      by auto
    then have "(term_to_sig ℱ v t, term_to_sig ℱ v u) ∈ srstep ℱ ℛ"
      by (auto simp:_ sig_step_def)
    then show ?thesis using st by auto
  next
    case False
    then have "term_to_sig ℱ v t = term_to_sig ℱ v u" unfolding * by auto
    then show ?thesis using st by auto
  qed
qed

lemma rstep_trancl_sig_step_l:
  assumes "(s, t) ∈ (rstep ℛ)⇧+" and "funas_rel ℛ ⊆ ℱ" and "funas_term t ⊆ ℱ"
  shows "(term_to_sig ℱ v s, t) ∈ (srstep ℱ ℛ)⇧+" using assms
proof (induct rule: converse_trancl_induct)
  case (base t)
  then show ?case using subsetD[OF fuans_term_term_to_sig, of _ ℱ v]
    by (auto simp: rstep_term_to_sig_l sig_step_def intro!: r_into_trancl)
next
  case (step s u)
  then have st: "(term_to_sig ℱ v u, t) ∈ (srstep ℱ ℛ)⇧+" by auto
  from step(1) obtain C l r σ where
    *: "s = C⟨l ⋅ σ⟩" "u = C⟨r ⋅ σ⟩" "(l, r) ∈ ℛ" by auto
  show ?case
  proof (cases "ctxt_well_def_hole_path ℱ C")
    case True
    from *(3) step(4) have "funas_term l ⊆ ℱ" "funas_term r ⊆ ℱ" by (auto simp: funas_rel_def)
    then have "(term_to_sig ℱ v s, term_to_sig ℱ v u) ∈ rstep ℛ"
      using True step(2) *(3) unfolding *
      by auto
    then have "(term_to_sig ℱ v s, term_to_sig ℱ v u) ∈ srstep ℱ ℛ"
      by (auto simp:_ sig_step_def)
    then show ?thesis using st by auto
  next
    case False
    then have "term_to_sig ℱ v s = term_to_sig ℱ v u" unfolding * by auto
    then show ?thesis using st by auto
  qed
qed

lemma rstep_srstepI [intro]:
  "funas_rel ℛ ⊆ ℱ ⟹ funas_term s ⊆ ℱ ⟹ funas_term t ⊆ ℱ ⟹ (s, t) ∈ rstep ℛ ⟹ (s, t) ∈ srstep ℱ ℛ"
  by blast

lemma rsteps_srstepsI [intro]:
  "funas_rel ℛ ⊆ ℱ ⟹ funas_term s ⊆ ℱ ⟹ funas_term t ⊆ ℱ ⟹ (s, t) ∈ (rstep ℛ)⇧+ ⟹ (s, t) ∈ (srstep ℱ ℛ)⇧+"
  using rstep_trancl_sig_step_r[of s t ℛ ℱ]
  by auto


lemma rsteps_eq_srsteps_eqI [intro]:
  "funas_rel ℛ ⊆ ℱ ⟹ funas_term s ⊆ ℱ ⟹ funas_term t ⊆ ℱ ⟹ (s, t) ∈ (rstep ℛ)⇧* ⟹ (s, t) ∈ (srstep ℱ ℛ)⇧*"
  by (auto simp add: rtrancl_eq_or_trancl)

lemma rsteps_eq_relcomp_srsteps_eq_relcompI [intro]:
  assumes "funas_rel ℛ ⊆ ℱ" "funas_rel 𝒮 ⊆ ℱ"
    and funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ"
    and steps: "(s, t) ∈ (rstep ℛ)⇧* O (rstep 𝒮)⇧*"
  shows "(s, t) ∈ (srstep ℱ ℛ)⇧* O (srstep ℱ 𝒮)⇧*"
proof -
  from steps obtain u where "(s, u) ∈ (rstep ℛ)⇧*" "(u, t) ∈ (rstep 𝒮)⇧*" by auto
  then have "(s, term_to_sig ℱ v u) ∈ (srstep ℱ ℛ)⇧*" "(term_to_sig ℱ v u, t) ∈ (srstep ℱ 𝒮)⇧*"
    using rstep_trancl_sig_step_l[OF _ assms(2) funas(2), of u v]
    using rstep_trancl_sig_step_r[OF _ assms(1) funas(1), of u v] funas
    by (auto simp: rtrancl_eq_or_trancl)
  then show ?thesis by auto
qed    


subsubsection ‹Distributivity laws›

lemma rstep_smycl_dist:
  "(rstep ℛ)⇧↔ = rstep (ℛ⇧↔)"
  by (auto simp: sig_step_def)

lemma sig_step_symcl_dist:
  "(sig_step ℱ ℛ)⇧↔ = sig_step ℱ (ℛ⇧↔)"
  by (auto simp: sig_step_def)

lemma srstep_symcl_dist:
  "(srstep ℱ ℛ)⇧↔ = srstep ℱ (ℛ⇧↔)"
  by (auto simp: sig_step_def)

lemma Restr_smycl_dist:
  "(Restr ℛ 𝒜)⇧↔ = Restr (ℛ⇧↔) 𝒜"
  by auto

lemmas rew_symcl_inwards = rstep_smycl_dist sig_step_symcl_dist srstep_symcl_dist Restr_smycl_dist
lemmas rew_symcl_outwards = rew_symcl_inwards[symmetric]

lemma rstep_converse_dist:
  "(rstep ℛ)¯ = rstep (ℛ¯)"
  by auto

lemma srrstep_converse_dist:
  "(srrstep ℱ ℛ)¯ = srrstep ℱ (ℛ¯)"
  by (fastforce simp: sig_step_def)

lemma sig_step_converse_rstep:
  "(srstep ℱ ℛ)¯ = sig_step ℱ ((rstep ℛ)¯)"
  by (meson converse.simps set_eq_subset sig_stepE(1) sig_stepE sig_stepI subrelI)

lemma srstep_converse_dist:
  "(srstep ℱ ℛ)¯ = srstep ℱ (ℛ¯)"
  by (auto simp: sig_step_def)

lemma Restr_converse: "(Restr ℛ A)¯ = Restr (ℛ¯) A"
  by auto

lemmas rew_converse_inwards = rstep_converse_dist srrstep_converse_dist sig_step_converse_rstep
   srstep_converse_dist Restr_converse trancl_converse[symmetric] rtrancl_converse[symmetric]
lemmas rew_converse_outwards = rew_converse_inwards[symmetric]

lemma sig_step_rsteps_dist:
  "funas_rel ℛ ⊆ ℱ ⟹ sig_step ℱ ((rstep ℛ)⇧+) = (srstep ℱ ℛ)⇧+"
  by (auto elim!: sig_stepE dest: srstepsD)

lemma sig_step_rsteps_eq_dist:
  "funas_rel ℛ ⊆ ℱ ⟹ sig_step ℱ ((rstep ℛ)⇧+) ∪ Id = (srstep ℱ ℛ)⇧*"
  by (auto simp: rtrancl_eq_or_trancl sig_step_rsteps_dist)

lemma sig_step_conversion_dist:
  "(srstep ℱ ℛ)⇧↔⇧* = (srstep ℱ (ℛ⇧↔))⇧*"
  by (auto simp: rtrancl_eq_or_trancl sig_step_rsteps_dist conversion_def srstep_symcl_dist)

lemma gsrstep_conversion_dist:
  "(gsrstep ℱ ℛ)⇧↔⇧* = (gsrstep ℱ (ℛ⇧↔))⇧*"
  by (auto simp: conversion_def rew_symcl_inwards)
                                                                                         
lemma sig_step_grstep_dist:
  "gsrstep ℱ ℛ = sig_step ℱ (Restr (rstep ℛ) (Collect ground))"
  by (auto simp: sig_step_def)

subsection ‹Substitution closure of @{const srstep}›

lemma srstep_subst_closed:
  assumes "(s, t) ∈ srstep ℱ ℛ" "⋀ x. funas_term (σ x) ⊆ ℱ"
  shows "(s ⋅ σ, t ⋅ σ) ∈ srstep ℱ ℛ" using assms
  by (auto simp: sig_step_def funas_term_subst)

lemma srsteps_subst_closed:
  assumes "(s, t) ∈ (srstep ℱ ℛ)⇧+" "⋀ x. funas_term (σ x) ⊆ ℱ"
  shows "(s ⋅ σ, t ⋅ σ) ∈ (srstep ℱ ℛ)⇧+" using assms(1)
proof (induct rule: trancl.induct)
  case (r_into_trancl s t) show ?case
    using srstep_subst_closed[OF r_into_trancl assms(2)]
    by auto
next
  case (trancl_into_trancl s t u)
  from trancl_into_trancl(2) show ?case
    using srstep_subst_closed[OF trancl_into_trancl(3) assms(2)]
    by (meson rtrancl_into_trancl1 trancl_into_rtrancl)  
qed

lemma srsteps_eq_subst_closed:
  assumes "(s, t) ∈ (srstep ℱ ℛ)⇧*" "⋀ x. funas_term (σ x) ⊆ ℱ"
  shows "(s ⋅ σ, t ⋅ σ) ∈ (srstep ℱ ℛ)⇧*" using assms srsteps_subst_closed
  by (metis rtrancl_eq_or_trancl)

lemma srsteps_eq_subst_relcomp_closed:
  assumes "(s, t) ∈ (srstep ℱ ℛ)⇧* O (srstep ℱ 𝒮)⇧*" "⋀ x. funas_term (σ x) ⊆ ℱ"
  shows "(s ⋅ σ, t ⋅ σ) ∈ (srstep ℱ ℛ)⇧* O (srstep ℱ 𝒮)⇧*"
proof -
  from assms(1) obtain u where "(s, u) ∈ (srstep ℱ ℛ)⇧*" "(u, t) ∈ (srstep ℱ 𝒮)⇧*" by auto
  then have "(s ⋅ σ, u ⋅ σ) ∈ (srstep ℱ ℛ)⇧*" "(u ⋅ σ, t ⋅ σ) ∈ (srstep ℱ 𝒮)⇧*"
    using assms srsteps_eq_subst_closed
    by metis+
  then show ?thesis by auto
qed


subsection ‹Context closure of @{const srstep}›

lemma srstep_ctxt_closed:
  assumes "funas_ctxt C ⊆ ℱ" and "(s, t) ∈ srstep ℱ ℛ"
  shows "(C⟨s⟩, C⟨t⟩) ∈ srstep ℱ ℛ" using assms
  by (intro sig_stepI) (auto dest: srstepD)

lemma srsteps_ctxt_closed:
  assumes "funas_ctxt C ⊆ ℱ" and "(s, t) ∈ (srstep ℱ ℛ)⇧+"
  shows "(C⟨s⟩, C⟨t⟩) ∈ (srstep ℱ ℛ)⇧+" using assms(2) srstep_ctxt_closed[OF assms(1)]
  by (induct) force+

lemma srsteps_eq_ctxt_closed:
  assumes "funas_ctxt C ⊆ ℱ" and "(s, t) ∈ (srstep ℱ ℛ)⇧*"
  shows "(C⟨s⟩, C⟨t⟩) ∈ (srstep ℱ ℛ)⇧*" using srsteps_ctxt_closed[OF assms(1)] assms(2)
  by (metis rtrancl_eq_or_trancl)

lemma sig_steps_join_ctxt_closed:
  assumes "funas_ctxt C ⊆ ℱ" and "(s, t) ∈ (srstep ℱ ℛ)⇧↓"
  shows "(C⟨s⟩, C⟨t⟩) ∈ (srstep ℱ ℛ)⇧↓" using srsteps_eq_ctxt_closed[OF assms(1)] assms(2)
  unfolding join_def rew_converse_inwards
  by auto
                                 

text ‹The following lemma shows that every rewrite sequence either contains a root step or is root stable›

lemma nsrsteps_with_root_step_step_on_args:
  assumes "(s, t) ∈ (srstep ℱ ℛ)⇧+" "(s, t) ∉ srsteps_with_root_step ℱ ℛ"
  shows "∃ f ss ts. s = Fun f ss ∧ t = Fun f ts ∧ length ss = length ts ∧
    (∀ i < length ts. (ss ! i, ts ! i) ∈ (srstep ℱ ℛ)⇧*)" using assms
proof (induct)
  case (base t)
  obtain C l r σ where [simp]: "s = C⟨l ⋅ σ⟩" "t = C⟨r ⋅ σ⟩" and r: "(l, r) ∈ ℛ"
    using base(1) unfolding sig_step_def
    by blast
  then have funas: "funas_ctxt C ⊆ ℱ" "funas_term (l ⋅ σ) ⊆ ℱ" "funas_term (r ⋅ σ) ⊆ ℱ"
    using base(1) by (auto simp: sig_step_def)
  from funas(2-) r have "(l ⋅ σ, r ⋅ σ) ∈ srrstep ℱ ℛ"
    by (auto simp: sig_step_def)
  then have "C = Hole ⟹ False" using base(2) r
    by (auto simp: srsteps_with_root_step_def)
  then obtain f ss D ts where [simp]: "C = More f ss D ts" by (cases C) auto
  have "(D⟨l ⋅ σ⟩, D⟨r ⋅ σ⟩) ∈ (srstep ℱ ℛ)" using base(1) r funas
    by (auto simp: sig_step_def)
  then show ?case using funas by (auto simp: nth_append_Cons)
next
  case (step t u) show ?case
  proof (cases "(s, t) ∈ srsteps_with_root_step ℱ ℛ ∨ (t, u) ∈ sig_step ℱ (rrstep ℛ)")
    case True then show ?thesis using step(1, 2, 4)
      by (auto simp add: relcomp3_I rtrancl.rtrancl_into_rtrancl srsteps_with_root_step_def)
  next
    case False
    obtain C l r σ where *[simp]: "t = C⟨l ⋅ σ⟩" "u = C⟨r ⋅ σ⟩" and r: "(l, r) ∈ ℛ"
      using step(2) unfolding sig_step_def by blast
    then have funas: "funas_ctxt C ⊆ ℱ" "funas_term (l ⋅ σ) ⊆ ℱ" "funas_term (r ⋅ σ) ⊆ ℱ"
      using step(2) by (auto simp: sig_step_def)
    from False have "C ≠ Hole" using funas r by (force simp: sig_step_def)
    then obtain f ss D ts where c[simp]: "C = More f ss D ts" by (cases C) auto
    from step(3, 1) False obtain g sss tss where
      **[simp]: "s = Fun g sss" "t = Fun g tss" and l: "length sss = length tss" and
      inv: "∀ i < length tss. (sss ! i, tss ! i) ∈ (srstep ℱ ℛ)⇧*"
      by auto
    have [simp]: "g = f" and lc: "Suc (length ss + length ts) = length sss"
      using l *(1) unfolding c using **(2) by auto
    then have "∀ i < Suc (length ss + length ts). ((ss @ D⟨l ⋅ σ⟩ # ts) ! i, (ss @ D⟨r ⋅ σ⟩ # ts) ! i) ∈ (srstep ℱ ℛ)⇧*"
      using * funas r by (auto simp: nth_append_Cons r_into_rtrancl rstep.intros rstepI sig_stepI)
    then have "i < length tss ⟹ (sss ! i, (ss @ D⟨r ⋅ σ⟩ # ts) ! i) ∈ (srstep ℱ ℛ)⇧*" for i
      using inv * l lc funas **
      by (auto simp: nth_append_Cons simp del: ** * split!: if_splits)
    then show ?thesis using inv l lc * unfolding c
      by auto
  qed
qed

lemma rstep_to_pos_replace:
  assumes "(s, t) ∈ rstep ℛ"
  shows "∃ p l r σ. p ∈ poss s ∧ (l, r) ∈ ℛ ∧ s |_ p = l ⋅ σ ∧ t = s[p ← r ⋅ σ]"
proof -
  from assms obtain C l r σ where st: "(l, r) ∈ ℛ" "s = C⟨l ⋅ σ⟩" "t = C⟨r ⋅ σ⟩"
    using rstep_imp_C_s_r by fastforce
  from st(2, 3) have *: "t = s[hole_pos C ← r ⋅ σ]" by simp
  from this st show ?thesis unfolding *
    by (intro exI[of _ "hole_pos C"]) auto
qed

lemma pos_replace_to_rstep:
  assumes "p ∈ poss s" "(l, r) ∈ ℛ" 
    and "s |_ p = l ⋅ σ" "t = s[p ← r ⋅ σ]"
  shows "(s, t) ∈ rstep ℛ"
  using assms(1, 3-) replace_term_at_subt_at_id [of s p]
  by (intro rstepI[OF assms(2), of s "ctxt_at_pos s p" σ])
     (auto simp add: ctxt_of_pos_term_apply_replace_at_ident)

end