Theory TRS.Term_Rewriting
chapter ‹Term Rewriting›
theory Term_Rewriting
imports
First_Order_Terms.Subterm_and_Context
Relation_Closure
begin
text ‹
A rewrite rule is a pair of terms. A term rewrite system (TRS) is a set of rewrite rules.
›
type_synonym ('f, 'v) rule = "('f, 'v) term × ('f, 'v) term"
type_synonym ('f, 'v) trs = "('f, 'v) rule set"
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"
lemma rstep_induct_rule [case_names IH, induct set: rstep]:
assumes "(s, t) ∈ rstep R"
and "⋀C σ l r. (l, r) ∈ R ⟹ P (C⟨l ⋅ σ⟩) (C⟨r ⋅ σ⟩)"
shows "P s t"
using assms by (induct) simp
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 rstep_empty [simp]: "rstep {} = {}"
by auto
lemma rstep_mono: "R ⊆ S ⟹ rstep R ⊆ rstep S"
by force
lemma rstep_union: "rstep (R ∪ S) = rstep R ∪ rstep S"
by auto
lemma rstep_converse [simp]: "rstep (R¯) = (rstep R)¯"
by auto
interpretation subst: rel_closure "λσ t. t ⋅ σ" Var "λx y. y ∘⇩s x" by (standard) auto
declare subst.closure.induct [consumes 1, case_names subst, induct pred: subst.closure]
declare subst.closure.cases [consumes 1, case_names subst, cases pred: subst.closure]
interpretation ctxt: rel_closure "ctxt_apply_term" □ "(∘⇩c)" by (standard) auto
declare ctxt.closure.induct [consumes 1, case_names ctxt, induct pred: ctxt.closure]
declare ctxt.closure.cases [consumes 1, case_names ctxt, cases pred: ctxt.closure]
lemma rstep_eq_closure: "rstep R = ctxt.closure (subst.closure R)"
by (force elim: ctxt.closure.cases subst.closure.cases)
lemma ctxt_closed_rstep [intro]: "ctxt.closed (rstep R)"
by (simp add: rstep_eq_closure ctxt.closed_closure)
lemma ctxt_closed_one:
"ctxt.closed r ⟹ (s, t) ∈ r ⟹ (Fun f (ss @ s # ts), Fun f (ss @ t # ts)) ∈ r"
using ctxt.closedD [of r s t "More f ss □ ts"] by auto
lemma args_steps_imp_steps:
assumes "ctxt.closed r"
and len: "length ts = length us"
and "∀i < length us. (ts ! i, us ! i) ∈ r⇧*"
shows "(Fun f ts, Fun f us) ∈ r⇧*"
proof -
have "(Fun f ts, Fun f (take i us @ drop i ts)) ∈ r⇧*" if "i ≤ length us" for i
using that
proof (induct i)
case (Suc i)
then have "(Fun f ts, Fun f (take i us @ drop i ts)) ∈ r⇧*" by simp
moreover have "take i us @ drop i ts = take i us @ ts ! length (take i us) # drop (Suc i) ts"
using Suc and len by (auto simp: Cons_nth_drop_Suc min_def)
moreover have "take (Suc i) us @ drop (Suc i) ts = take i us @ us ! length (take i us) # drop (Suc i) ts"
using Suc and len by (auto simp: min_def take_Suc_conv_app_nth)
moreover have "(Fun f (take i us @ ts ! length (take i us) # drop (Suc i) ts),
Fun f (take i us @ us ! length (take i us) # drop (Suc i) ts)) ∈ r⇧*"
using assms and Suc by (intro ctxt_closed_one) auto
ultimately show ?case by simp
qed simp
note this [of "length us"] and len
then show ?thesis by simp
qed
end