# Theory Rewriting

```section ‹Rewriting›

theory Rewriting
imports Regular_Tree_Relations.Term_Context
Regular_Tree_Relations.Ground_Terms
Utils
begin

subsection ‹Type definitions and rewrite relation definitions›
type_synonym 'f sig = "('f × nat) set"
type_synonym ('f, 'v) rule = "('f, 'v) term × ('f, 'v) term"
type_synonym ('f, 'v) trs  = "('f, 'v) rule set"

definition "sig_step ℱ ℛ = {(s, t). funas_term s ⊆ ℱ ∧ funas_term t ⊆ ℱ ∧ (s, t) ∈ ℛ}"

inductive_set rstep :: "_ ⇒ ('f, 'v) term rel" for R :: "('f, 'v) trs"
where
rstep: "⋀C σ l r. (l, r) ∈ R ⟹ s = C⟨l ⋅ σ⟩ ⟹ t = C⟨r ⋅ σ⟩ ⟹ (s, t) ∈ rstep R"

definition rstep_r_p_s :: "('f, 'v) trs ⇒ ('f, 'v) rule ⇒ pos ⇒ ('f, 'v) subst ⇒ ('f, 'v) trs" where
"rstep_r_p_s R r p σ = {(s, t). p ∈ poss s ∧ p ∈ poss t ∧ r ∈ R ∧ ctxt_at_pos s p = ctxt_at_pos t p ∧
s[p ← (fst r ⋅ σ)] = s ∧ t[p ← (snd r ⋅ σ)] = t}"

text ‹Rewriting steps below the root position.›
definition nrrstep :: "('f, 'v) trs ⇒ ('f, 'v) trs" where
"nrrstep R = {(s,t). ∃r i ps σ. (s,t) ∈ rstep_r_p_s R r (i#ps) σ}"

text ‹Rewriting step at the root position.›
definition rrstep :: "('f, 'v) trs ⇒ ('f, 'v) trs" where
"rrstep R = {(s,t). ∃r σ. (s,t) ∈ rstep_r_p_s R r [] σ}"

text ‹the parallel rewrite relation›
inductive_set par_rstep :: "('f,'v)trs ⇒ ('f,'v)trs" for R :: "('f,'v)trs"
where root_step[intro]: "(s,t) ∈ R ⟹ (s ⋅ σ,t ⋅ σ) ∈ par_rstep R"
|  par_step_fun[intro]: "⟦⋀ i. i < length ts ⟹ (ss ! i,ts ! i) ∈ par_rstep R⟧ ⟹ length ss = length ts
⟹ (Fun f ss, Fun f ts) ∈ par_rstep R"
|  par_step_var[intro]: "(Var x, Var x) ∈ par_rstep R"

subsection ‹Ground variants connecting to FORT›

definition grrstep :: "('f, 'v) trs ⇒ 'f gterm rel" where
"grrstep ℛ = inv_image (rrstep ℛ) term_of_gterm"

definition gnrrstep :: "('f, 'v) trs ⇒ 'f gterm rel" where
"gnrrstep ℛ = inv_image (nrrstep ℛ) term_of_gterm"

definition grstep :: "('f, 'v) trs ⇒ 'f gterm rel" where
"grstep ℛ = inv_image (rstep ℛ) term_of_gterm"

definition gpar_rstep :: "('f, 'v) trs ⇒ 'f gterm rel" where
"gpar_rstep ℛ = inv_image (par_rstep ℛ) term_of_gterm"

text ‹
An alternative induction scheme that treats the rule-case, the
substition-case, and the context-case separately.
›
lemma rstep_induct [consumes 1, case_names rule subst ctxt]:
assumes "(s, t) ∈ rstep R"
and rule: "⋀l r. (l, r) ∈ R ⟹ P l r"
and subst: "⋀s t σ. P s t ⟹ P (s ⋅ σ) (t ⋅ σ)"
and ctxt: "⋀s t C. P s t ⟹ P (C⟨s⟩) (C⟨t⟩)"
shows "P s t"
using assms by (induct) auto

lemmas rstepI = rstep.intros [intro]

lemmas rstepE = rstep.cases [elim]

lemma rstep_ctxt [intro]: "(s, t) ∈ rstep R ⟹ (C⟨s⟩, C⟨t⟩) ∈ rstep R"
by (force simp flip: ctxt_ctxt_compose)

lemma rstep_rule [intro]: "(l, r) ∈ R ⟹ (l, r) ∈ rstep R"
using rstep.rstep [where C = □ and σ = Var and R = R] by simp

lemma rstep_subst [intro]: "(s, t) ∈ rstep R ⟹ (s ⋅ σ, t ⋅ σ) ∈ rstep R"
by (force simp flip: subst_subst_compose)

lemma nrrstep_def':
"nrrstep R = {(s, t). ∃l r C σ. (l, r) ∈ R ∧ C ≠ □ ∧ s = C⟨l⋅σ⟩ ∧ t = C⟨r⋅σ⟩}" (is "?Ls = ?Rs")
proof
show "?Ls ⊆ ?Rs"
proof (rule subrelI)
fix s t assume "(s, t) ∈ ?Ls"
then obtain l r i ps σ where step: "(s, t) ∈ rstep_r_p_s R (l, r) (i # ps) σ"
unfolding nrrstep_def by best
let ?C = "ctxt_at_pos s (i # ps)"
from step have"i # ps ∈ poss s" and "(l, r) ∈ R" and "s = ?C⟨l⋅σ⟩" and "t = ?C⟨r⋅σ⟩"
unfolding rstep_r_p_s_def Let_def by (auto simp flip: replace_term_at_replace_at_conv)
moreover from ‹i # ps ∈ poss s› have "?C ≠ □" by (induct s) auto
ultimately show "(s, t) ∈ ?Rs" by auto
qed
next
show "?Rs ⊆ ?Ls"
proof (rule subrelI)
fix s t assume "(s, t) ∈ ?Rs"
then obtain l r C σ where in_R: "(l, r) ∈ R" and "C ≠ □"
and s: "s = C⟨l⋅σ⟩" and t: "t = C⟨r⋅σ⟩" by auto
from ‹C ≠ □› obtain i p where ip: "hole_pos C = i # p" by (induct C) auto
have "i # p ∈ poss s" unfolding s ip[symmetric] by simp
then have C: "C = ctxt_at_pos s (i # p) "
unfolding s ip[symmetric] by simp
from ‹i # p ∈ poss s› in_R s t have "(s, t) ∈ rstep_r_p_s R (l, r) (i # p) σ"
unfolding rstep_r_p_s_def C[symmetric] ip[symmetric] by simp
then show "(s, t) ∈ nrrstep R" unfolding nrrstep_def by best
qed
qed

lemma rrstep_def': "rrstep R = {(s, t). ∃l r σ. (l, r) ∈ R ∧ s = l⋅σ ∧ t = r⋅σ}"
by (auto simp: rrstep_def rstep_r_p_s_def)

lemma rstep_imp_C_s_r:
assumes "(s,t) ∈ rstep R"
shows "∃C σ l r. (l,r) ∈ R ∧ s = C⟨l⋅σ⟩ ∧ t = C⟨r⋅σ⟩" using assms
by (induct) auto

lemma rhs_wf:
assumes R: "(l, r) ∈ R" and "funas_trs R ⊆ F"
shows "funas_term r ⊆ F"
using assms by (force simp: funas_trs_def)

abbreviation "linear_sys ℛ ≡ (∀ (l, r) ∈ ℛ. linear_term l ∧ linear_term r)"
abbreviation "const_subt c ≡ λ x. Fun c []"

end```