theory Equational_Reasoning
imports
QTRS.Trs
First_Order_Terms.Option_Monad
begin
text ‹
The following datatype represents proofs in equational logic
using the following rules:
\begin{itemize}
\item reflexivity: $E \vdash t = t$
\item symmetry: $E \vdash s = t$ implies $E \vdash t = s$
\item transitivity: $E \vdash s = t$ and $E \vdash t = u$
implies $E \vdash s = u$
\item assumption: for every $(s, t) \in E$ and substitution
$\sigma$, we have $E \vdash s\sigma = t\sigma$ (Note that this
rules combines the instantiation and assumption rules that are
for example found in \emph{Term Rewriting and All That}.)
\item congruence: for every $n$-ary function symbol $f$ and
$E \vdash s_1 = t_1$, \ldots, $E \vdash s_n = t_n$, we have
$E \vdash f(s_1, \ldots, s_n) = f(t_1, \ldots, t_n)$
\end{itemize}
›
datatype (dead 'f, 'v) eq_proof =
Refl "('f, 'v) term"
| Sym "('f, 'v) eq_proof"
| Trans "('f, 'v) eq_proof" "('f, 'v) eq_proof"
| Assm "('f, 'v) rule" "('f, 'v) subst"
| Cong 'f "('f, 'v) eq_proof list"
lemma
fixes P :: "('f, 'v) eq_proof ⇒ bool"
assumes "⋀t. P (Refl t)" and "⋀p. P p ⟹ P (Sym p)"
and "⋀p1 p2. P p1 ⟹ P p2 ⟹ P (Trans p1 p2)"
and "⋀l r σ. P (Assm (l, r) σ)"
and "⋀f ps. (⋀p. p ∈ set ps ⟹ P p) ⟹ P (Cong f ps)"
shows eq_proof_induct[case_names Refl Sym Trans Assm Cong, induct type: eq_proof]:
"P p"
by (induct p, insert assms, auto)
type_synonym ('f, 'v) equation = "('f, 'v) rule"
text ‹
Given an equational system @{term E} and an equational logic proof @{term p},
@{term "proves E p"} obtains the equation which is proved, simultaneously checking
the correctness of @{term p}. If @{term p} is not correct the result is @{term None},
otherwise the result is the proved equation.
›
fun
proves :: "('f, 'v) trs ⇒ ('f, 'v) eq_proof ⇒ ('f, 'v) equation option"
where
"proves E (Refl s) = Some (s, s)"
| "proves E (Sym p) = do {
(s, t) ← proves E p;
Some (t, s) }"
| "proves E (Trans p1 p2) = do {
(s, t) ← proves E p1;
(t', u) ← proves E p2;
guard (t = t');
Some (s, u)
}"
| "proves E (Assm (l, r) σ) = do {
guard ((l, r) ∈ E);
Some (l ⋅ σ, r ⋅ σ)
}"
| "proves E (Cong f ps) = do {
sts ← mapM (proves E) ps;
Some (Fun f (map fst sts), Fun f (map snd sts))
}"
text ‹
The \emph{equational theory} of an equational system @{term E} is the set
of all provable equations.
›
definition eq_theory :: "('f, 'v) trs ⇒ ('f, 'v) equation set" where
"eq_theory E ≡ {e. ∃p. proves E p = Some e}"
text ‹
In contrast to applying rules of term rewriting, for applying equations
the direction does not matter.
›
definition estep :: "('f, 'v) trs ⇒ ('f, 'v) trs" where
"estep E ≡ rstep (E ∪ E^-1)"
lemma estep_sym_closure_conv: "estep E = (rstep E)⇧↔"
unfolding estep_def rstep_union reverseTrs ..
lemma join_conversion: "join (rstep R) ⊆ (estep R)^*"
proof
fix a b
assume "(a,b) ∈ join (rstep R)"
hence steps: "(a,b) ∈ (rstep R)^* O ((rstep R)^*)^-1" by auto
show "(a,b) ∈ (estep R)^*"
by (rule set_mp[OF _ steps], unfold rtrancl_converse[symmetric] estep_sym_closure_conv, regexp)
qed
lemma esteps_is_conversion: "(estep E)^* = conversion (rstep E)"
unfolding conversion_def estep_sym_closure_conv ..
lemma sym_estep: "sym (estep E)"
unfolding estep_sym_closure_conv sym_def by auto
lemma sym_esteps: "sym ((estep E)^*)"
by (rule sym_rtrancl, rule sym_estep)
lemma subst_closed_estep: "subst.closed (estep E)"
unfolding estep_def rstep_union by blast
lemma ctxt_closed_estep [intro]: "ctxt.closed (estep E)"
unfolding estep_def rstep_union by blast
lemma sym_esteps_pair: "(s,t) ∈ (estep E)^* ⟹ (t,s) ∈ (estep E)^*"
using sym_esteps[unfolded sym_def] by auto
lemma all_ctxt_closed_esteps[intro]: "all_ctxt_closed F ((estep E)^*)"
unfolding estep_def by auto
lemma ctxt_closed_eq_theory: "ctxt.closed (eq_theory E)"
proof (rule one_imp_ctxt_closed)
fix f bef s t aft
assume "(s,t) ∈ eq_theory E"
from this[unfolded eq_theory_def] obtain p where p: "proves E p = Some (s,t)" by auto
show "(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ eq_theory E" (is "?pair ∈ _")
unfolding eq_theory_def
proof(rule, rule exI)
have id: "mapM (proves E) (map Refl bef @ p # map Refl aft) = (Some (map (λ b. (b,b)) bef @ (s,t) # map (λ a. (a,a)) aft))"
proof (induct bef)
case (Cons b bef)
thus ?case by auto
next
case Nil
have "mapM (proves E) (map Refl aft) = Some (map (λ a. (a,a)) aft)"
by (induct aft, auto)
thus ?case unfolding list.map append_Nil mapM.simps p by simp
qed
thus "proves E (Cong f (map (λ b. Refl b) bef @ p # map (λ a. Refl a) aft)) = Some ?pair" by (auto simp: o_def)
qed
qed
text ‹
For every sentence of the equational theory of @{term E},
the left-hand side can be transformed into the right-hand side by
applying equations from @{term E}.
›
lemma eq_theory_is_esteps: "eq_theory E = (estep E)^*" (is "?P = ?E")
proof -
let ?p = "proves E"
note conv = esteps_is_conversion conversion_def
{
fix s t
assume "(s,t) ∈ eq_theory E"
from this[unfolded eq_theory_def] obtain p where
"proves E p = Some (s,t)" by auto
hence "(s,t) ∈ ?E"
proof (induct p arbitrary: s t)
case (Refl s)
thus ?case unfolding conv by auto
next
case (Sym p)
from Sym(2) have p: "?p p = Some (t,s)" by (cases "?p p", auto)
from Sym(1)[OF p] have ts: "(t,s) ∈ ?E" .
from sym_esteps[of E] ts
show ?case unfolding sym_def by auto
next
case (Trans p1 p2)
from Trans(3) obtain s1 t1 where p1: "?p p1 = Some (s1,t1)" by (cases "?p p1", auto)
from Trans(3) obtain s2 t2 where p2: "?p p2 = Some (s2,t2)" using p1 by (cases "?p p2", auto)
from Trans(3) have t1s2: "t1 = s2" using p1 p2 by (cases "t1 = s2", auto)
from Trans(3) p1 p2 t1s2 have p1: "?p p1 = Some (s,t1)" and p2: "?p p2 = Some (t1,t)" by auto
from Trans(1)[OF p1] Trans(2)[OF p2] show ?case by auto
next
case (Assm l r σ)
from Assm have mem: "(l,r) ∈ E" by (cases "(l,r) ∈ E", auto)
from Assm mem have id: "s = l ⋅ σ" "t = r ⋅ σ" by auto
have "(s,t) ∈ rstep E" unfolding id using mem by auto
thus ?case unfolding conv by auto
next
case (Cong f ps)
from Cong(2) obtain sts where sts: "mapM ?p ps = Some sts" by (cases "mapM ?p ps", auto)
let ?ss = "map fst sts"
let ?ts = "map snd sts"
from Cong(2) sts
have id: "s = Fun f ?ss" "t = Fun f ?ts" by auto
note sts' = mapM_Some[OF sts]
show ?case unfolding id
proof (rule all_ctxt_closedD[of UNIV], unfold length_map)
fix i
assume i: "i < length sts"
have psi: "ps ! i ∈ set ps" using sts sts' i by auto
show "(?ss ! i, ?ts ! i) ∈ ?E" unfolding nth_map[OF i]
proof (rule Cong(1)[OF psi])
from sts' psi have "?p (ps ! i) ≠ None" by auto
thus "?p (ps ! i) = Some (fst (sts ! i), snd (sts ! i))"
using sts' i by (cases "?p (ps ! i)", auto)
qed
qed auto
qed
}
hence "?P ⊆ ?E" by auto
moreover
{
fix s t
assume "(s,t) ∈ ?E"
hence "(s,t) ∈ ?P" unfolding eq_theory_def
proof (induct)
case base
have "proves E (Refl s) = Some (s,s)" by simp
thus ?case by blast
next
case (step t u)
from step(3) obtain p where st: "?p p = Some (s,t)" by auto
obtain l r C σ where lr: "(l,r) ∈ E^<->" and t: "t = C⟨l ⋅ σ⟩" and u: "u = C⟨r ⋅ σ⟩" by (rule rstepE[OF step(2)[unfolded estep_def]])
from lr
have "∃ p. ?p p = Some (l ⋅ σ, r ⋅ σ)"
proof
assume "(l,r) ∈ E"
hence "?p (Assm (l,r) σ) = Some (l ⋅ σ, r ⋅ σ)" by simp
thus ?thesis ..
next
assume "(l,r) ∈ E^-1"
hence "(r,l) ∈ E" by simp
hence "?p (Sym (Assm (r,l) σ)) = Some (l ⋅ σ, r ⋅ σ)" by simp
thus ?thesis ..
qed
hence "(l ⋅ σ, r ⋅ σ) ∈ ?P" unfolding eq_theory_def by auto
from ctxt.closedD[OF ctxt_closed_eq_theory this, of C]
obtain p2 where tu: "?p p2 = Some (t,u)" unfolding t u unfolding eq_theory_def by auto
from st tu have "?p (Trans p p2) = Some (s,u)" by simp
thus ?case by blast
qed
}
hence "?E ⊆ ?P" by auto
ultimately show ?thesis by auto
qed
type_synonym ('f, 'a) eq_inter = "'f ⇒ 'a list ⇒ 'a"
type_synonym ('v, 'a) eq_assign = "'v ⇒ 'a"
definition eq_inter :: "'a set ⇒ ('f, 'a) eq_inter ⇒ bool" where
"eq_inter U I ≡ ∀f as. set as ⊆ U ⟶ I f as ∈ U"
definition eq_assign :: "'a set ⇒ ('v, 'a) eq_assign ⇒ bool" where
"eq_assign U α ≡ range α ⊆ U"
text ‹
We evaluate terms w.r.t\ an interpretation @{term I} on function symbols
and an assignment @{term α} on variables.
›
fun
eq_eval :: "('f, 'a) eq_inter ⇒ ('v, 'a) eq_assign ⇒ ('f, 'v) term ⇒ 'a"
where
"eq_eval I α (Var x) = α x"
| "eq_eval I α (Fun f ts) = I f (map (eq_eval I α) ts)"
fun
eq_model_eqn :: "'a set ⇒ ('f, 'a) eq_inter ⇒ ('f, 'v) equation ⇒ bool"
where
"eq_model_eqn U I (l, r) = (∀α. eq_assign U α ⟶ eq_eval I α l = eq_eval I α r)"
text ‹
The algebra given by the carrier @{term U} and where function symbols are interpreted
by @{term I} is a \emph{model} of an equational system @{term E} if all its equations
are satisfied for arbitrary assignments.
›
definition models :: "'a set ⇒ ('f, 'a) eq_inter ⇒ ('f, 'v) trs ⇒ bool" where
"models U I E ≡ (∀e∈E. eq_model_eqn U I e)"
text ‹
The equational system @{term E} \emph{entails} the equation @{term e}, if every
model of @{term E} is also a model of @{term e}.
›
definition entails :: "'a ⇒ ('f, 'v) trs ⇒ ('f, 'v) equation ⇒ bool" where
"entails a E e ≡ ∀U::'a set. ∀I. eq_inter U I ⟶ models U I E ⟶ eq_model_eqn U I e"
lemma eq_subst_lemma: "eq_eval I α (t ⋅ σ) = eq_eval I (λx. eq_eval I α (σ x)) t"
proof (induct t)
case (Var x) thus ?case by simp
next
case (Fun f ts)
have id: "map (λx. eq_eval I α (x ⋅ σ)) ts =
map (eq_eval I (λx. eq_eval I α (σ x))) ts"
using Fun by (induct ts, auto)
show ?case unfolding eq_eval.simps id[symmetric]
by (simp add: o_def)
qed
lemma eq_inter_assign:
assumes I: "eq_inter U I" and α: "eq_assign U α"
shows "eq_eval I α t ∈ U"
proof (induct t)
case (Var x)
show ?case using α[unfolded eq_assign_def] by auto
next
case (Fun f ts)
hence "eq_eval I α ` set ts ⊆ U" by auto
with I[unfolded eq_inter_def] show ?case by auto
qed
text ‹
Every conversion is also
a semantic consequence of @{term E}.
›
lemma esteps_imp_entails:
fixes E :: "('f, 'v) trs" and a :: "'a"
assumes "(s, t) ∈ (estep E)^*"
shows "entails a E (s, t)"
proof -
let ?p = "proves E"
from assms[folded eq_theory_is_esteps, unfolded eq_theory_def]
obtain p where eq: "?p p = Some (s,t)" by auto
show ?thesis unfolding entails_def
proof (intro impI allI)
fix U :: "'a set" and I
assume I: "models U I E" "eq_inter U I"
let ?J = "eq_eval I"
show "eq_model_eqn U I (s,t)"
unfolding eq_model_eqn.simps
proof (intro impI allI)
fix α :: "('v,'a)eq_assign"
assume α: "eq_assign U α"
from eq
show "?J α s = ?J α t" (is "?I s = _")
proof (induct p arbitrary: s t)
case (Refl u s t)
thus ?case by auto
next
case (Sym p)
from Sym(2) have p: "?p p = Some (t,s)" by (cases "?p p", auto)
from Sym(1)[OF p] show ?case by simp
next
case (Trans p1 p2)
from Trans(3) obtain s1 t1 where p1: "?p p1 = Some (s1,t1)" by (cases "?p p1", auto)
from Trans(3) obtain s2 t2 where p2: "?p p2 = Some (s2,t2)" using p1 by (cases "?p p2", auto)
from Trans(3) have t1s2: "t1 = s2" using p1 p2 by (cases "t1 = s2", auto)
from Trans(3) p1 p2 t1s2 have p1: "?p p1 = Some (s,t1)" and p2: "?p p2 = Some (t1,t)" by auto
from Trans(1)[OF p1] Trans(2)[OF p2] show ?case by auto
next
case (Assm l r σ)
from Assm have mem: "(l,r) ∈ E" by (cases "(l,r) ∈ E", auto)
from Assm mem have id: "s = l ⋅ σ" "t = r ⋅ σ" by auto
from I[unfolded models_def] mem have "eq_model_eqn U I (l,r)" by auto
from this[unfolded eq_model_eqn.simps] have lr: "⋀ α. eq_assign U α ⟹ ?J α l = ?J α r" by simp
show ?case unfolding id eq_subst_lemma
proof (rule lr, unfold eq_assign_def, rule)
fix a
assume "a ∈ range (λ x. ?I (σ x))"
then obtain t where a: "a = ?I t" by auto
show "a ∈ U" unfolding a
by (rule eq_inter_assign[OF I(2) α])
qed
next
case (Cong f ps)
from Cong(2) obtain sts where sts: "mapM ?p ps = Some sts" by (cases "mapM ?p ps", auto)
let ?ss = "map fst sts"
let ?ts = "map snd sts"
from Cong(2) sts
have id: "s = Fun f ?ss" "t = Fun f ?ts" by auto
note sts' = mapM_Some[OF sts]
show ?case unfolding id eq_eval.simps
proof (rule arg_cong[where f = "I f"], rule nth_map_conv, simp,
unfold length_map, intro allI impI)
fix i
assume i: "i < length sts"
have psi: "ps ! i ∈ set ps" using sts sts' i by auto
show "?I (?ss ! i) = ?I (?ts ! i)" unfolding nth_map[OF i]
proof (rule Cong(1)[OF psi])
from sts' psi have "?p (ps ! i) ≠ None" by auto
thus "?p (ps ! i) = Some (fst (sts ! i), snd (sts ! i))"
using sts' i by (cases "?p (ps ! i)", auto)
qed
qed
qed
qed
qed
qed
text ‹
Every equation that is semantic consequence of @{term E} is
yields a converion w.r.t. @{term E}.
›
lemma entails_imp_esteps:
fixes E :: "('f, 'v) trs" and a :: "('f, 'v) terms"
assumes entails: "entails a E (s, t)"
shows "(s, t) ∈ (estep E)^*"
proof -
let ?E = "(estep E)^*"
obtain cl where cl: "cl ≡ λ t. {s. (t,s) ∈ ?E}" by auto
{
fix s t
have "((s,t) ∈ ?E) = (cl s = cl t)"
proof
assume st: "(s,t) ∈ ?E"
from st sym_esteps_pair[OF st]
show "cl s = cl t" unfolding cl by auto
next
assume "cl s = cl t"
thus "(s,t) ∈ ?E"
unfolding cl by auto
qed
} note esteps_iff_cl = this
note cl_iff_esteps = esteps_iff_cl[symmetric]
let ?U = "range cl"
obtain cl' where cl': "cl' ≡ λ eqc. SOME (t :: ('f,'v)term). t ∈ eqc" by auto
obtain a_to_s where a_to_s: "a_to_s ≡ λ α :: ('v,('f,'v)terms)eq_assign. λ x. cl' (α x)" by auto
obtain I where I: "I ≡ λ f eqs. cl (Fun f (map cl' eqs))" by auto
let ?I = "eq_eval I"
have I_inter: "eq_inter ?U I"
unfolding eq_inter_def cl I by auto
note entails = entails[unfolded entails_def, rule_format, OF I_inter]
{
fix t
let ?P = "λ s. (t,s) ∈ ?E"
let ?s = "SOME s. ?P s"
have id: "cl' (cl t) = ?s" unfolding cl' cl by auto
have "cl (cl' (cl t)) = cl t"
unfolding id cl_iff_esteps
by (rule sym_esteps_pair, rule someI[of ?P t], simp)
} note cl_cl' = this
{
fix s and α :: "('v,('f,'v)terms)eq_assign"
assume α: "eq_assign ?U α"
have "?I α s = cl (s ⋅ a_to_s α)"
proof (induct s)
case (Var x)
from α[unfolded eq_assign_def] obtain t where αx: "α x = cl t" by auto
show ?case unfolding a_to_s eq_eval.simps subst_apply_term.simps
unfolding αx cl_cl' by simp
next
case (Fun f ss)
from I have id: "I f = (λ eqs. cl (Fun f (map cl' eqs)))" by auto
show ?case unfolding eq_eval.simps subst_apply_term.simps id map_map o_def
unfolding cl_iff_esteps
proof (rule all_ctxt_closedD[of UNIV], unfold length_map)
fix i
assume i: "i < length ss"
from Fun[unfolded set_conv_nth, of "ss ! i"] i have id: "?I α (ss ! i) =
cl (ss ! i ⋅ a_to_s α)" by auto
show "(map (λ x. cl' (?I α x)) ss ! i, map (λ t. t ⋅ a_to_s α) ss ! i) ∈ ?E"
unfolding nth_map[OF i]
unfolding esteps_iff_cl
unfolding id cl_cl' ..
qed auto
qed
} note eq_eval_id = this
have model: "models ?U I E"
unfolding models_def
proof(rule, clarify)
fix s t
assume st: "(s,t) ∈ E"
show "eq_model_eqn ?U I (s,t)" unfolding eq_model_eqn.simps
proof (intro allI impI)
fix α :: "('v,('f,'v)terms)eq_assign"
assume α: "eq_assign ?U α"
from st have "(s ⋅ a_to_s α, t ⋅ a_to_s α) ∈ estep E"
"(t ⋅ a_to_s α, s ⋅ a_to_s α) ∈ estep E"
unfolding estep_def by auto
thus "eq_eval I α s = eq_eval I α t"
unfolding eq_eval_id[OF α]
unfolding cl by auto
qed
qed
note entails = entails[OF model, unfolded eq_model_eqn.simps, rule_format]
obtain α where α: "α ≡ λ x. cl (Var x)" by simp
have α_inter: "eq_assign ?U α" unfolding eq_assign_def α by auto
note entails = entails[OF this]
{
fix s
have "cl(s ⋅ a_to_s α) = cl s"
proof (induct s)
case (Var x)
show ?case unfolding a_to_s α
by (simp add: cl_cl')
next
case (Fun f ss)
show ?case unfolding subst_apply_term.simps
unfolding cl_iff_esteps
proof (rule all_ctxt_closedD[of UNIV], unfold length_map)
fix i
assume i: "i < length ss"
have "map (λ t. t ⋅ a_to_s α) ss ! i = ss ! i ⋅ a_to_s α" using i by simp
also have "(ss ! i ⋅ a_to_s α, ss ! i) ∈ ?E" using Fun[unfolded set_conv_nth cl_iff_esteps, of "ss ! i"] i by auto
finally show "(map (λ t. t ⋅ a_to_s α) ss ! i, ss ! i) ∈ ?E" .
qed auto
qed
} note a_to_s = this
from entails have "?I α s = ?I α t" .
from this[unfolded eq_eval_id[OF α_inter] a_to_s]
show ?thesis unfolding esteps_iff_cl .
qed
text ‹
Syntactic consequence (convertability) and
semantic consequence (entailment) coincide.
›
lemma birkhoff:
fixes E :: "('f, 'v) trs" and a :: "('f, 'v) terms"
shows "entails a E (s, t) ⟷ (s, t) ∈ (estep E)^*"
using esteps_imp_entails[of s t E a]
and entails_imp_esteps[of a E s t] by auto
text ‹
Two equational systems are \emph{equivalent} if they prove
same equations, i.e., have the same conversions
›
definition equivalent :: "('f, 'v) trs ⇒ ('f, 'v) trs ⇒ bool" where
"equivalent E E' ≡ (estep E)^* = (estep E')^*"
text ‹
The equational system @{term E} \emph{subsumes} the equational system
@{term E'} when all equations that are provable using @{term E'} are
also provable using @{term E}.
›
definition subsumes :: "('f, 'v) trs ⇒ ('f, 'v) trs ⇒ bool" where
"subsumes E E' ≡ (estep E')^* ⊆ (estep E)^*"
lemma equivalent_subsumes:
"equivalent E E' ⟷ subsumes E E' ∧ subsumes E' E"
unfolding subsumes_def equivalent_def by auto
lemma subsumes_via_rule_conversion:
"subsumes E E' = (∀(s, t)∈E'. (s, t) ∈ (estep E)^*)"
proof
assume subs: "subsumes E E'"
show "∀ (s,t) ∈ E'. (s,t) ∈ (estep E)^*"
proof(clarify)
fix s t
assume "(s,t) ∈ E'"
hence "(s,t) ∈ (estep E')^*" unfolding estep_def by auto
with subs show "(s,t) ∈ (estep E)^*" unfolding subsumes_def by auto
qed
next
assume "∀(s, t)∈E'. (s,t) ∈ (estep E)^*"
hence steps: "⋀s t. (s, t) ∈ E' ⟹ (s, t) ∈ (estep E)^*" by auto
show "subsumes E E'"
unfolding subsumes_def
proof
fix s t
assume "(s,t) ∈ (estep E')^*"
thus "(s,t) ∈ (estep E)^*"
proof(induct)
case base
show ?case unfolding estep_def by auto
next
case (step t u)
from step(2)[unfolded estep_def] obtain l r C σ where t: "t = C⟨l⋅σ⟩"
and u: "u = C⟨r ⋅ σ⟩" and lr: "(l,r) ∈ E' ∪ E'^-1" by auto
from lr have steps: "(l,r) ∈ (estep E)^*"
proof
assume "(l,r) ∈ E'"
from steps[OF this] show ?thesis .
next
assume "(l,r) ∈ E'^-1"
hence "(r,l) ∈ E'" by simp
from steps[OF this] have "(r,l) ∈ (estep E)^*" .
with sym_rtrancl[OF sym_estep, of E]
show ?thesis unfolding sym_def by auto
qed
with subst.closed_rtrancl[OF subst_closed_estep[of E], unfolded subst.closed_def] have steps: "(l ⋅ σ, r ⋅ σ) ∈ (estep E)^*" by auto
have "(t,u) ∈ (estep E)^*" unfolding t u
by (rule ctxt.closedD[OF _ steps], blast)
with step(3) show ?case by simp
qed
qed
qed
text ‹
We say that the TRS @{term R} is a complete rewrite system for the
equational system @{term E} iff their respective equational
theories are the same and @{term R} is convergent, i.e., confluent
and terminating.
›
definition
completed_rewrite_system :: "('f, 'v) trs ⇒ ('f, 'v) trs ⇒ bool"
where
"completed_rewrite_system E R ≡ equivalent E R ∧ CR (rstep R) ∧ SN (rstep R)"
lemma completion_via_WCR_SN_simulation:
assumes 1: "subsumes E R"
and 2: "subsumes R E"
and 3: "WCR (rstep R)"
and 4: "SN (rstep R)"
shows "completed_rewrite_system E R"
unfolding completed_rewrite_system_def equivalent_subsumes
using Newman[OF 4 3] 1 2 4 by auto
end