Theory Multistep

section ‹Multi-Step Rewriting›

theory Multistep
  imports Trs
begin

text ‹Multi-step rewriting (without proof terms).›
inductive_set
  mstep :: "('f, 'v) trs ⇒ ('f, 'v) term rel"
  for R
  where
    Var: "(Var x, Var x) ∈ mstep R" |
    args: "⋀f n ss ts. ⟦length ss = n; length ts = n;
    ∀i<n. (ss ! i, ts ! i) ∈ mstep R⟧ ⟹
    (Fun f ss, Fun f ts) ∈ mstep R" |
    rule: "⋀l r σ τ. ⟦(l, r) ∈ R; ∀x∈vars_term l. (σ x, τ x) ∈ mstep R⟧ ⟹
    (l ⋅ σ, r ⋅ τ) ∈ mstep R"

lemma mstep_refl [simp]:
  "(t, t) ∈ mstep R"
  by (induct t) (auto intro: mstep.intros)

lemma mstep_ctxt:
  assumes "(s, t) ∈ mstep R"
  shows "(C⟨s⟩, C⟨t⟩) ∈ mstep R"
proof (induction C)
  case Hole with assms show ?case by simp
next
  case (More f ss C ts)
  let ?ss = "ss @ C⟨s⟩ # ts"
  let ?ts = "ss @ C⟨t⟩ # ts"
  { fix i assume "i = length ss"
    then have "(?ss ! i, ?ts ! i) ∈ mstep R"
      using More.IH by simp }
  moreover
  { fix i assume "i < length ss"
    then have "(?ss ! i, ?ts ! i) ∈ mstep R"
      by (simp add: nth_append) }
  moreover
  { fix i assume "i < length ?ss" and "i > length ss"
    then have "(?ss ! i, ?ts ! i) ∈ mstep R"
      by (simp add: nth_append) }
  ultimately
  have "∀i<length ?ss.  (?ss ! i, ?ts ! i) ∈ mstep R"
    by (metis linorder_neqE_nat)
  from mstep.args [OF _ _ this, simplified]
  show ?case by simp
qed

lemma rstep_imp_mstep:
  assumes "(s, t) ∈ rstep R"
  shows "(s, t) ∈ mstep R"
  using assms
proof (induct)
  case (IH C σ l r)
  have "∀x∈vars_term l. (σ x, σ x) ∈ mstep R" by simp
  from mstep.rule [OF ‹(l, r) ∈ R› this]
  have "(l ⋅ σ, r ⋅ σ) ∈ mstep R" by simp
  from mstep_ctxt [OF this] show ?case by blast
qed

lemma rstep_mstep_subset:
  "rstep R ⊆ mstep R"
  by (auto simp: rstep_imp_mstep)

lemma subst_rsteps_imp_rule_rsteps:
  assumes "∀x∈vars_term l. (σ x, τ x) ∈ (rstep R)⇧*"
    and "(l, r) ∈ R"
  shows "(l ⋅ σ, r ⋅ τ) ∈ (rstep R)⇧*"
proof -
  let ?σ="λx. (if x ∈ vars_term l then σ x else τ x)"
  have "l ⋅ σ = l ⋅ ?σ" 
    by (simp add: term_subst_eq_conv)
  with ‹(l, r) ∈ R› have "(l ⋅ σ, r ⋅ ?σ) ∈ rstep R"
    by auto
  moreover have "(r ⋅ ?σ, r ⋅ τ) ∈ (rstep R)⇧*"
    by (rule subst_rsteps_imp_rsteps) (insert assms, auto)
  ultimately show ?thesis by auto
qed

lemma mstep_imp_rsteps:
  assumes "(s, t) ∈ mstep R"
  shows "(s, t) ∈ (rstep R)⇧*"
  using assms
proof (induct)
  case (args f n ss ts)
  then show ?case by (metis args_rsteps_imp_rsteps)
next
  case (rule l r σ τ)
  then show ?case using ‹(l, r) ∈ R› by (metis subst_rsteps_imp_rule_rsteps)
qed simp

lemma mstep_rsteps_subset:
  shows "mstep R ⊆ (rstep R)⇧*"
  by (auto simp: mstep_imp_rsteps)

lemma mstep_mono: "R ⊆ S ⟹ mstep R ⊆ mstep S" 
proof -
  have "(s,t) ∈ mstep R ⟹ R ⊆ S ⟹ (s,t) ∈ mstep S" for s t
    by (induct rule: mstep.induct, auto intro: mstep.intros)
  thus "R ⊆ S ⟹ mstep R ⊆ mstep S" by auto
qed


text ‹Thus if @{term " mstep R"} has the diamond property,
then @{term "rstep R"} is confluent.›

lemma Var_mstep:
  assumes *: "⋀l r. (l, r) ∈ R ⟹ ¬ is_Var l"
    and "(Var x, t) ∈ mstep R"
  shows "t = Var x"
  using assms(2-) 
proof cases
  case (rule l r σ τ)
  then show ?thesis using * by (cases l, auto)
qed auto


subsection ‹Maximal multi-step rewriting.›
inductive_set
  mmstep :: "('f, 'v) trs ⇒ ('f, 'v) term rel"
  for R
  where
    Var: "(Var x, Var x) ∈ mmstep R" |
    args: "⋀f n ss ts. ⟦length ss = n; length ts = n;
    ¬ (∃(l, r)∈R. ∃σ. Fun f ss = l ⋅ σ);
    ∀i<n. (ss ! i, ts ! i) ∈ mmstep R⟧ ⟹
    (Fun f ss, Fun f ts) ∈ mmstep R" |
    rule: "⋀l r σ τ. ⟦(l, r) ∈ R; ∀x∈vars_term l. (σ x, τ x) ∈ mmstep R⟧ ⟹
    (l ⋅ σ, r ⋅ τ) ∈ mmstep R"

lemma mmstep_imp_mstep:
  assumes "(s, t) ∈ mmstep R"
  shows "(s, t) ∈ mstep R"
  using assms by (induct) (auto intro: mstep.intros)

lemma mmstep_mstep_subset:
  "mmstep R ⊆ mstep R"
  by (auto simp: mmstep_imp_mstep)


end