section ‹Critical Pairs›
theory CP
imports
QTRS.Unification_More
QTRS.Renaming_Interpretations
begin
definition
overlap ::
"('f, 'v :: infinite) trs ⇒ ('f, 'v) trs ⇒ ('f, 'v) rule ⇒ pos ⇒ ('f, 'v) rule ⇒ bool"
where
"overlap R R' r p r' ⟷
(∃p. p ∙ r ∈ R) ∧
(∃p. p ∙ r' ∈ R') ∧
vars_rule r ∩ vars_rule r' = {} ∧
p ∈ funposs (fst r') ∧
(∃σ :: ('f, 'v) subst. fst r ⋅ σ = (fst r' |_ p) ⋅ σ) ∧
(p = ε ⟶ ¬ (∃p. p ∙ r = r'))"
lemma overlap_right:
fixes R⇩1 R⇩2 :: "('f, 'v::infinite) trs"
assumes "overlap R⇩1 R⇩2 r⇩1 p r⇩2"
obtains π where "overlap R⇩1 R⇩2 (π ∙ r⇩1) p (π ∙ r⇩2)" and "(π ∙ r⇩2) ∈ R⇩2"
proof -
obtain π⇩1 and π⇩2
where "π⇩1 ∙ r⇩1 ∈ R⇩1" and "π⇩2 ∙ r⇩2 ∈ R⇩2"
and "vars_rule r⇩1 ∩ vars_rule r⇩2 = {}"
and "p ∈ funposs (fst r⇩2)"
and "∃σ::('f, 'v) subst. fst r⇩1 ⋅ σ = (fst r⇩2 |_ p) ⋅ σ"
and "p = ε ⟶ ¬ (∃p. p ∙ r⇩1 = r⇩2)"
using assms unfolding overlap_def by blast
then have "(π⇩1 + -π⇩2) ∙ (π⇩2 ∙ r⇩1) ∈ R⇩1" and "0 ∙ (π⇩2 ∙ r⇩2) ∈ R⇩2"
and "vars_rule (π⇩2 ∙ r⇩1) ∩ vars_rule (π⇩2 ∙ r⇩2) = {}"
and "p ∈ funposs (fst (π⇩2 ∙ r⇩2))"
and "∃σ::('f, 'v) subst. fst (π⇩2 ∙ r⇩1) ⋅ σ = (fst (π⇩2 ∙ r⇩2) |_ p) ⋅ σ"
and "p = ε ⟶ ¬ (∃p. p ∙ (π⇩2 ∙ r⇩1) = π⇩2 ∙ r⇩2)"
apply (auto simp: eqvt [symmetric])
apply (rule_tac x = "sop (-π⇩2) ∘⇩s σ" in exI)
apply (simp add: funposs_imp_poss subt_at_eqvt)
apply (rule_tac x = "sop (-π⇩2) ∘⇩s σ" in exI)
apply (simp add: funposs_imp_poss subt_at_eqvt)
by (metis rule_pt.permute_minus_cancel(2) rule_pt.permute_plus)
then show thesis
apply (intro that [of π⇩2])
apply (unfold overlap_def)
apply blast
apply auto
done
qed
text ‹Critical peaks are single-step rewrite peaks originating from overlaps.›
definition
cpeaks2 ::
"('f, 'v :: infinite) trs ⇒ ('f, 'v) trs ⇒
(('f, 'v) term × pos × ('f, 'v) term × ('f, 'v) term) set"
where
"cpeaks2 R R' = {(replace_at (fst r') p (snd r) ⋅ σ, p, fst r' ⋅ σ, snd r' ⋅ σ) |
r p r' σ. overlap R R' r p r' ∧ σ = the_mgu (fst r) (fst r' |_ p)}"
abbreviation "cpeaks R ≡ cpeaks2 R R"
lemma cpeaks2_I:
assumes "overlap R R' r p r'" and "σ = the_mgu (fst r) (fst r' |_ p)"
shows "(replace_at (fst r') p (snd r) ⋅ σ, p, fst r' ⋅ σ, snd r' ⋅ σ) ∈ cpeaks2 R R'"
using assms by (force simp: cpeaks2_def)
inductive_set S3 for A
where
subst: "(t, p, s, u) ∈ A ⟹ (t ⋅ σ, p, s ⋅ σ, u ⋅ σ) ∈ S3 A"
lemma peak_above_imp_join_or_cpeaks:
fixes R :: "('f, 'v :: infinite) trs"
and σ⇩1 σ⇩2 :: "('f, 'v) subst"
assumes rule_variants: "∃π. π ∙ (l⇩1, r⇩1) ∈ R" "∃π. π ∙ (l⇩2, r⇩2) ∈ R"
and disj: "vars_rule (l⇩1, r⇩1) ∩ vars_rule (l⇩2, r⇩2) = {}"
and "p⇩2 ≤ p⇩1"
and "vars_term r⇩1 ⊆ vars_term l⇩1"
and p⇩1: "p⇩1 ∈ poss s"
and sp⇩1: "s |_ p⇩1 = l⇩1 ⋅ σ⇩1"
and t: "t = replace_at s p⇩1 (r⇩1 ⋅ σ⇩1)"
and p⇩2: "p⇩2 ∈ poss s"
and sp⇩2: "s |_ p⇩2 = l⇩2 ⋅ σ⇩2"
and u: "u = replace_at s p⇩2 (r⇩2 ⋅ σ⇩2)"
shows "(t, u) ∈ (rstep R)⇧↓ ∨
(p⇩2 ∈ poss s ∧
(ctxt_of_pos_term p⇩2 s)⟨t |_ p⇩2⟩ = t ∧
(ctxt_of_pos_term p⇩2 s)⟨u |_ p⇩2⟩ = u ∧
(t |_ p⇩2, pos_diff p⇩1 p⇩2, s |_ p⇩2, u |_ p⇩2) ∈ S3 (cpeaks R))"
proof -
define p where "p = pos_diff p⇩1 p⇩2"
have p⇩1_eq: "p⇩1 = p⇩2 <#> p" using ‹p⇩2 ≤ p⇩1› by (simp add: p_def)
then have t: "t = replace_at s p⇩2 (replace_at (l⇩2 ⋅ σ⇩2) p (r⇩1 ⋅ σ⇩1))"
by (simp add: t ctxt_of_pos_term_append p⇩2 sp⇩2)
show ?thesis
proof (cases "p ∈ funposs l⇩2 ∧ (p = ε ⟶ ¬ (∃π. π ∙ (l⇩1, r⇩1) = (l⇩2, r⇩2)))")
case True
define σ' where "σ' x = (if x ∈ vars_rule (l⇩1, r⇩1) then σ⇩1 x else σ⇩2 x)" for x
have p: "p ∈ funposs l⇩2" and "p = ε ⟹ ¬ (∃π. π ∙ (l⇩1, r⇩1) = (l⇩2, r⇩2))" using True by auto
moreover
have unif: "l⇩1 ⋅ σ' = (l⇩2 |_ p) ⋅ σ'"
proof -
note coinc = coincidence_lemma' [of l⇩1 "vars_rule (l⇩1, r⇩1)"]
have disj: "vars_rule (l⇩1, r⇩1) ∩ vars_term (l⇩2 |_ p) = {}"
using vars_term_subt_at [OF funposs_imp_poss [OF p]] and disj
by (auto simp: vars_rule_def)
have "l⇩1 ⋅ σ' = l⇩1 ⋅ (σ' |s vars_rule (l⇩1, r⇩1))"
using coinc by (simp add: vars_rule_def)
also have "… = l⇩1 ⋅ (σ⇩1 |s vars_rule (l⇩1, r⇩1))" by (simp add: σ'_def [abs_def])
also have "… = l⇩1 ⋅ σ⇩1" using coinc by (simp add: vars_rule_def)
also have "… = (l⇩2 ⋅ σ⇩2) |_ p" using subt_at_append [OF p⇩2] and sp⇩1 by (simp add: p⇩1_eq sp⇩2)
also have "… = (l⇩2 |_ p) ⋅ σ⇩2" using funposs_imp_poss [OF p] by simp
also have "… = (l⇩2 |_ p) ⋅ (σ⇩2 |s vars_term (l⇩2 |_ p))"
by (simp add: coincidence_lemma [symmetric])
also have "… = (l⇩2 |_ p) ⋅ (σ' |s vars_term (l⇩2 |_ p))" using disj by (simp add: σ'_def [abs_def])
finally show ?thesis by (simp add: coincidence_lemma [symmetric])
qed
ultimately
have overlap: "overlap R R (l⇩1, r⇩1) p (l⇩2, r⇩2)"
using disj and rule_variants by (auto simp: overlap_def)
define σ where "σ = the_mgu l⇩1 (l⇩2 |_ p)"
have cpeaks: "(replace_at l⇩2 p r⇩1 ⋅ σ, p, l⇩2 ⋅ σ, r⇩2 ⋅ σ) ∈ cpeaks R"
using cpeaks2_I [OF overlap refl] by (simp add: σ_def)
have "is_mgu σ {(l⇩1, l⇩2 |_ p)}" by (rule is_mguI) (insert unif the_mgu, auto simp: σ_def)
with unif obtain τ where σ': "σ' = σ ∘⇩s τ" by (auto simp: is_mgu_def unifiers_def)
have "(replace_at (l⇩2 ⋅ σ⇩2) p (r⇩1 ⋅ σ⇩1), p, l⇩2 ⋅ σ⇩2, r⇩2 ⋅ σ⇩2) ∈ S3 (cpeaks R)"
proof -
have "l⇩2 ⋅ σ⇩2 = l⇩2 ⋅ σ'"
proof -
have disj: "vars_rule (l⇩1, r⇩1) ∩ vars_term l⇩2 = {}" using disj by (auto simp: vars_rule_def)
have "l⇩2 ⋅ σ' = l⇩2 ⋅ (σ' |s vars_term l⇩2)" by (rule coincidence_lemma)
also have "… = l⇩2 ⋅ (σ⇩2 |s vars_term l⇩2)" using disj by (simp add: σ'_def [abs_def])
also have "… = l⇩2 ⋅ σ⇩2" by (simp add: coincidence_lemma [symmetric])
finally show ?thesis ..
qed
moreover
have "r⇩1 ⋅ σ⇩1 = r⇩1 ⋅ σ'"
proof -
note coinc = coincidence_lemma' [of r⇩1 "vars_rule (l⇩1, r⇩1)"]
have "r⇩1 ⋅ σ' = r⇩1 ⋅ (σ' |s vars_rule (l⇩1, r⇩1))"
using coinc by (simp add: vars_rule_def)
also have "… = r⇩1 ⋅ (σ⇩1 |s vars_rule (l⇩1, r⇩1))" by (simp add: σ'_def [abs_def])
also have "… = r⇩1 ⋅ σ⇩1" using coinc by (simp add: vars_rule_def)
finally show ?thesis ..
qed
moreover
have "r⇩2 ⋅ σ⇩2 = r⇩2 ⋅ σ'"
proof -
have disj: "vars_rule (l⇩1, r⇩1) ∩ vars_term r⇩2 = {}" using disj by (auto simp: vars_rule_def)
have "r⇩2 ⋅ σ' = r⇩2 ⋅ (σ' |s vars_term r⇩2)" by (rule coincidence_lemma)
also have "… = r⇩2 ⋅ (σ⇩2 |s vars_term r⇩2)" using disj by (simp add: σ'_def [abs_def])
also have "… = r⇩2 ⋅ σ⇩2" by (simp add: coincidence_lemma [symmetric])
finally show ?thesis ..
qed
ultimately
show ?thesis using cpeaks
using S3.intros [OF cpeaks, of τ]
and funposs_imp_poss [OF p]
by (simp add: σ' ctxt_of_pos_term_subst)
qed
moreover have "p⇩2 ∈ poss s" by fact
ultimately show ?thesis using p⇩2 and sp⇩2 by (auto simp: t u p_def replace_at_subt_at)
next
case False
then have "(p = ε ∧ (∃π. π ∙ (l⇩1, r⇩1) = (l⇩2, r⇩2))) ∨ p ∉ funposs l⇩2" by blast
then show ?thesis
proof (elim disjE conjE exE)
txt ‹The variable condition is only needed here.›
fix π
assume [simp]: "p = ε" and "π ∙ (l⇩1, r⇩1) = (l⇩2, r⇩2)"
then have "p⇩2 = p⇩1" and "l⇩2 = π ∙ l⇩1" and [simp]: "r⇩2 = π ∙ r⇩1" by (simp_all add: p⇩1_eq eqvt)
then have "l⇩1 ⋅ σ⇩1 = l⇩1 ⋅ (σ⇩2 ∘ Rep_perm π)"
using sp⇩1 and sp⇩2 by (simp add: permute_term_subst_apply_term)
moreover
have "vars_term r⇩1 ⊆ vars_term l⇩1" by fact
ultimately
have "r⇩1 ⋅ σ⇩1 = r⇩1 ⋅ (σ⇩2 ∘ Rep_perm π)" using vars_term_subset_subst_eq by blast
then have "r⇩1 ⋅ σ⇩1 = π ∙ r⇩1 ⋅ σ⇩2" by (simp add: permute_term_subst_apply_term)
then show ?thesis by (auto simp: t u)
next
txt ‹Variable overlap.›
have step1: "(l⇩1, r⇩1) ∈ rstep R" and step2: "(l⇩2, r⇩2) ∈ rstep R"
using rule_variants by (auto simp: eqvt) (metis rstep.rule rstep_permute_iff)+
have "p ∈ poss (l⇩2 ⋅ σ⇩2)" by (metis p⇩1_eq p⇩1 poss_append_poss sp⇩2)
moreover
assume "p ∉ funposs l⇩2"
ultimately
obtain q⇩1 q⇩2 x
where [simp]: "p = q⇩1 <#> q⇩2" and q⇩1: "q⇩1 ∈ poss l⇩2"
and l⇩2q⇩1: "l⇩2 |_ q⇩1 = Var x" and q⇩2: "q⇩2 ∈ poss (σ⇩2 x)"
by (rule poss_subst_apply_term)
moreover
have [simp]: "l⇩2 ⋅ σ⇩2 |_ p = l⇩1 ⋅ σ⇩1" by (metis p⇩1_eq p⇩2 sp⇩1 sp⇩2 subt_at_append)
ultimately
have [simp]: "σ⇩2 x |_ q⇩2 = l⇩1 ⋅ σ⇩1" by simp
define σ⇩2' where "σ⇩2' y = (if y = x then replace_at (σ⇩2 x) q⇩2 (r⇩1 ⋅ σ⇩1) else σ⇩2 y)" for y
have "(σ⇩2 x, σ⇩2' x) ∈ rstep R"
proof -
let ?C = "ctxt_of_pos_term q⇩2 (σ⇩2 x)"
have "(?C⟨l⇩1 ⋅ σ⇩1⟩, ?C⟨r⇩1 ⋅ σ⇩1⟩) ∈ rstep R" using step1 by blast
then show ?thesis using q⇩2 by (simp add: σ⇩2'_def replace_at_ident)
qed
then have *: "⋀x. (σ⇩2 x, σ⇩2' x) ∈ (rstep R)⇧*" by (auto simp: σ⇩2'_def)
then have "(r⇩2 ⋅ σ⇩2, r⇩2 ⋅ σ⇩2') ∈ (rstep R)⇧*" by (rule substs_rsteps)
then have "(u, replace_at s p⇩2 (r⇩2 ⋅ σ⇩2')) ∈ (rstep R)⇧*" by (auto simp: u rsteps_closed_ctxt)
moreover
have "(t, replace_at s p⇩2 (r⇩2 ⋅ σ⇩2')) ∈ (rstep R)⇧*"
proof -
have "replace_at (l⇩2 ⋅ σ⇩2) p (r⇩1 ⋅ σ⇩1) = replace_at (l⇩2 ⋅ σ⇩2) q⇩1 (σ⇩2' x)"
using q⇩1 and q⇩2 by (simp add: σ⇩2'_def ctxt_of_pos_term_append l⇩2q⇩1)
moreover
have "(replace_at (l⇩2 ⋅ σ⇩2) q⇩1 (σ⇩2' x), l⇩2 ⋅ σ⇩2') ∈ (rstep R)⇧*"
by (rule replace_at_subst_rsteps [OF * q⇩1 l⇩2q⇩1])
moreover
have "(l⇩2 ⋅ σ⇩2', r⇩2 ⋅ σ⇩2') ∈ rstep R" using step2 by blast
ultimately
have "(replace_at (l⇩2 ⋅ σ⇩2) p (r⇩1 ⋅ σ⇩1), r⇩2 ⋅ σ⇩2') ∈ (rstep R)⇧*" by auto
then show ?thesis by (auto simp: p⇩2 t rsteps_closed_ctxt)
qed
ultimately show ?thesis by blast
qed
qed
qed
lemma parallel_peak_imp_join:
fixes p⇩1 p⇩2 :: "pos"
assumes parallel: "p⇩1 ⊥ p⇩2"
and peak: "(s, t) ∈ rstep_pos R p⇩1" "(s, u) ∈ rstep_pos R p⇩2"
shows "(t, u) ∈ (rstep R)⇧↓"
using parallel_steps [OF _ _ parallel, of s t R _ _ _ u] and peak
apply (auto simp: join_def rstep_pos_rstep_r_p_s_conv simp del: reverseTrs)
apply (intro relcompI r_into_rtrancl)
by (fastforce simp add: rstep_iff_rstep_r_p_s)+
text ‹Peaks are either joinable or contain an instance of a critical peak.›
lemma peak_imp_join_or_S3_cpeaks:
fixes R :: "('f, 'v :: infinite) trs"
assumes variable_condition: "∀(l, r)∈R. vars_term r ⊆ vars_term l"
and peak: "(s, t) ∈ rstep_pos R p⇩1" "(s, u) ∈ rstep_pos R p⇩2"
shows "(t, u) ∈ (rstep R)⇧↓ ∨ (
(p⇩2 ≤ p⇩1 ∧ (ctxt_of_pos_term p⇩2 s)⟨t |_ p⇩2⟩ = t ∧ (ctxt_of_pos_term p⇩2 s)⟨u |_ p⇩2⟩ = u ∧
(t |_ p⇩2, pos_diff p⇩1 p⇩2, s |_ p⇩2, u |_ p⇩2) ∈ S3 (cpeaks R)) ∨
(p⇩1 ≤ p⇩2 ∧ (ctxt_of_pos_term p⇩1 s)⟨t |_ p⇩1⟩ = t ∧ (ctxt_of_pos_term p⇩1 s)⟨u |_ p⇩1⟩ = u ∧
(u |_ p⇩1, pos_diff p⇩2 p⇩1, s |_ p⇩1, t |_ p⇩1) ∈ S3 (cpeaks R)))"
proof -
obtain l⇩1' r⇩1' σ⇩1' l⇩2 r⇩2 σ⇩2
where rule1': "(l⇩1', r⇩1') ∈ R" and rule2: "(l⇩2, r⇩2) ∈ R"
and p⇩1: "p⇩1 ∈ poss s" and p⇩2: "p⇩2 ∈ poss s"
and s1': "replace_at s p⇩1 (l⇩1' ⋅ σ⇩1') = s" and t': "t = replace_at s p⇩1 (r⇩1' ⋅ σ⇩1')"
and s2: "replace_at s p⇩2 (l⇩2 ⋅ σ⇩2) = s" and u: "u = replace_at s p⇩2 (r⇩2 ⋅ σ⇩2)"
using rstep_pos.cases [OF peak(1)]
and rstep_pos.cases [OF peak(2)]
by (metis ctxt_supt_id)
from vars_rule_disjoint obtain π⇩1
where π⇩1: "vars_rule (π⇩1 ∙ (l⇩1', r⇩1')) ∩ vars_rule (l⇩2, r⇩2) = {}" ..
define l⇩1 and r⇩1 and σ⇩1
where "l⇩1 = π⇩1 ∙ l⇩1'" and "r⇩1 = π⇩1 ∙ r⇩1'" and "σ⇩1 = (Var ∘ Rep_perm (-π⇩1)) ∘⇩s σ⇩1'"
note rename = l⇩1_def r⇩1_def σ⇩1_def
have disj: "vars_rule (l⇩1, r⇩1) ∩ vars_rule (l⇩2, r⇩2) = {}" using π⇩1 by (auto simp: eqvt rename)
have s1: "replace_at s p⇩1 (l⇩1 ⋅ σ⇩1) = s" and t: "t = replace_at s p⇩1 (r⇩1 ⋅ σ⇩1)"
by (simp_all add: s1' t' rename)
have "-π⇩1 ∙ (l⇩1, r⇩1) ∈ R" and "0 ∙ (l⇩2, r⇩2) ∈ R"
using rule1' and rule2 by (simp_all add: rename)
then have rule_variants: "∃π. π ∙ (l⇩1, r⇩1) ∈ R" "∃π. π ∙ (l⇩2, r⇩2) ∈ R" by blast+
show ?thesis
proof (cases "p⇩1 ⊥ p⇩2")
assume "p⇩1 ⊥ p⇩2"
moreover
have "(s, t) ∈ rstep_r_p_s R (l⇩1', r⇩1') p⇩1 σ⇩1'"
by (simp add: p⇩1 rstep_r_p_s_def s1' t' rule1')
moreover
have "(s, u) ∈ rstep_r_p_s R (l⇩2, r⇩2) p⇩2 σ⇩2"
by (simp add: p⇩2 rstep_r_p_s_def s2 u rule2)
ultimately
obtain v where "(t, v) ∈ rstep R" and "(u, v) ∈ rstep R"
by (blast dest: parallel_steps rstep_r_p_s_imp_rstep)
then show ?thesis by blast
next
have sp⇩1: "s |_ p⇩1 = l⇩1 ⋅ σ⇩1" using s1 and p⇩1 by (metis replace_at_subt_at)
have sp⇩2: "s |_ p⇩2 = l⇩2 ⋅ σ⇩2" using s2 and p⇩2 by (metis replace_at_subt_at)
assume "¬ (p⇩1 ⊥ p⇩2)"
then have "p⇩1 ≤ p⇩2 ∨ p⇩2 ≤ p⇩1" by (metis parallel_pos)
then show ?thesis
proof
have vars: "vars_term r⇩1 ⊆ vars_term l⇩1"
using variable_condition [THEN bspec, OF rule1']
and atom_set_pt.permute_set_subset [of "vars_term r⇩1'" "vars_term l⇩1'"]
by (auto simp add: rename supp_vars_term_eq [symmetric] term_fs.supp_eqvt [symmetric])
assume "p⇩2 ≤ p⇩1"
with peak_above_imp_join_or_cpeaks [OF rule_variants disj this vars p⇩1 sp⇩1 t p⇩2 sp⇩2 u]
show ?thesis by (auto simp: s2)
next
have vars: "vars_term r⇩2 ⊆ vars_term l⇩2"
using variable_condition [THEN bspec, OF rule2] by blast
have disj: "vars_rule (l⇩2, r⇩2) ∩ vars_rule (l⇩1, r⇩1) = {}" using disj by blast
assume "p⇩1 ≤ p⇩2"
with peak_above_imp_join_or_cpeaks [OF rule_variants(2, 1) disj this vars p⇩2 sp⇩2 u p⇩1 sp⇩1 t]
show ?thesis by (auto simp: s1)
qed
qed
qed
inductive_set CS3 for A
where
"(t, p, s, u) ∈ A ⟹ (C⟨t ⋅ σ⟩, hole_pos C <#> p, C⟨s ⋅ σ⟩, C⟨u ⋅ σ⟩) ∈ CS3 A"
lemma CS3_imp_rstep:
assumes "(t, p, s, u) ∈ CS3 A"
shows "(t, u) ∈ rstep ((λ(w, x, y, z). (w, z)) ` A)"
using assms by (cases) force
lemma S3_imp_CS3:
assumes "p ∈ poss s"
and S3: "(v, q, s |_ p, w) ∈ S3 A"
shows "((ctxt_of_pos_term p s)⟨v⟩, p <#> q, s, (ctxt_of_pos_term p s)⟨w⟩) ∈ CS3 A"
using S3
proof (cases)
case (subst t' s' u' σ)
with CS3.intros [OF subst(4), of "ctxt_of_pos_term p s" σ]
show ?thesis by (simp add: assms replace_at_ident)
qed
lemma peak_imp_join_or_CS3_cpeaks:
fixes R :: "('f, 'v :: infinite) trs"
assumes vc: "∀(l, r)∈R. vars_term r ⊆ vars_term l"
and peak: "(s, t) ∈ rstep R" "(s, u) ∈ rstep R"
shows "(t, u) ∈ (rstep R)⇧↓ ∨ (∃p. (t, p, s, u) ∈ CS3 (cpeaks R) ∨ (u, p, s, t) ∈ CS3 (cpeaks R))"
proof -
from peak obtain p q
where peak: "(s, t) ∈ rstep_pos R p" "(s, u) ∈ rstep_pos R q"
by (auto simp: rstep_rstep_pos_conv)
then have "p ∈ poss s" and "q ∈ poss s" by (auto elim: rstep_pos.cases)
with peak_imp_join_or_S3_cpeaks [OF vc peak]
show ?thesis by (auto dest: S3_imp_CS3)
qed
definition
CP2 :: "('f, 'v::infinite) trs ⇒ ('f, 'v) trs ⇒ ('f, 'v) rule set"
where
"CP2 R R' = {(replace_at (fst r') p (snd r) ⋅ σ, snd r' ⋅ σ) |
r p r' σ. overlap R R' r p r' ∧ σ = the_mgu (fst r) (fst r' |_ p)}"
abbreviation "CP R ≡ CP2 R R"
lemma CP2_I:
assumes "overlap R R' r p r'" and "σ = the_mgu (fst r) (fst r' |_ p)"
shows "(replace_at (fst r') p (snd r) ⋅ σ, snd r' ⋅ σ) ∈ CP2 R R'"
using assms by (force simp: CP2_def)
lemma CP2_cpeaks2_conv:
"CP2 R R' = (λ(t, p, s, u). (t, u)) ` cpeaks2 R R'"
by (force simp: CP2_def cpeaks2_def)
lemma peak_imp_join_or_CP:
fixes R :: "('f, 'v :: infinite) trs"
assumes "∀(l, r)∈R. vars_term r ⊆ vars_term l"
and "(s, t) ∈ rstep R" "(s, u) ∈ rstep R"
shows "(t, u) ∈ (rstep R)⇧↓ ∨ (t, u) ∈ (rstep (CP R))⇧↔"
using peak_imp_join_or_CS3_cpeaks [OF assms]
by (auto simp: CP2_cpeaks2_conv dest: CS3_imp_rstep simp del: reverseTrs)
lemma CP_join_imp_peak_join:
assumes "∀(l, r)∈R. vars_term r ⊆ vars_term l"
and *: "∀(s, t)∈CP R. (s, t) ∈ (rstep R)⇧↓"
shows "(rstep R)¯ O (rstep R) ⊆ (rstep R)⇧↓"
proof -
have "(rstep (CP R))⇧↔ ⊆ (rstep R)⇧↓"
proof (intro subrelI)
fix s t
assume "(s, t) ∈ (rstep (CP R))⇧↔"
then have "(s, t) ∈ rstep (CP R) ∨ (t, s) ∈ rstep (CP R)" by auto
then show "(s, t) ∈ (rstep R)⇧↓"
proof
assume "(s, t) ∈ rstep (CP R)"
then obtain C σ u v where cp: "(u, v) ∈ CP R"
and [simp]: "s = C⟨u ⋅ σ⟩" "t = C⟨v ⋅ σ⟩" by auto
from * [THEN bspec, OF cp] show ?thesis by auto
next
assume "(t, s) ∈ rstep (CP R)"
then obtain C σ u v where cp: "(u, v) ∈ CP R"
and [simp]: "t = C⟨u ⋅ σ⟩" "s = C⟨v ⋅ σ⟩" by auto
show ?thesis by (rule join_sym) (insert * [THEN bspec, OF cp], auto)
qed
qed
with peak_imp_join_or_CP [OF assms(1)] show ?thesis by blast
qed
lemma CP2_imp_peak:
fixes R :: "('f, 'v :: infinite) trs"
assumes "(s, t) ∈ CP2 R S"
shows "(s, t) ∈ (rstep R)¯ O (rstep S)"
proof -
from assms obtain r p r' σ
where overlap: "overlap R S r p r'"
and σ: "σ = the_mgu (fst r) (fst r' |_ p)"
and s: "s = replace_at (fst r') p (snd r) ⋅ σ"
and t: "t = snd r' ⋅ σ"
by (auto simp: CP2_def)
obtain l⇩1 r⇩1 l⇩2 r⇩2
where [simp]: "r = (l⇩1, r⇩1)" "r' = (l⇩2, r⇩2)" by (cases r, cases r') auto
from overlap obtain π⇩1 π⇩2 and τ :: "('f, 'v) subst"
where "π⇩1 ∙ (l⇩1, r⇩1) ∈ R" and "π⇩2 ∙ (l⇩2, r⇩2) ∈ S"
and p: "p ∈ funposs l⇩2"
and unif: "l⇩1 ⋅ τ = l⇩2 |_ p ⋅ τ"
by (auto simp: overlap_def)
then have "π⇩1 ∙ (l⇩1, r⇩1) ∈ rstep R" and "π⇩2 ∙ (l⇩2, r⇩2) ∈ rstep S"
by (metis rstep.rule surjective_pairing)+
then have "(l⇩1, r⇩1) ∈ rstep R" and "(l⇩2, r⇩2) ∈ rstep S"
by (metis perm_rstep_imp_rstep rule_pt.permute_prod.simps)+
then have "((ctxt_of_pos_term p l⇩2)⟨l⇩1⟩ ⋅ σ, s) ∈ rstep R"
and "(l⇩2 ⋅ σ, t) ∈ rstep S" by (auto simp: s t)
moreover
have "replace_at (l⇩2) p (l⇩1) ⋅ σ = l⇩2 ⋅ σ"
using the_mgu [OF unif] and funposs_imp_poss [OF p]
by (auto simp: σ) (metis replace_at_ident subst_apply_term_ctxt_apply_distrib)
ultimately
show ?thesis by (auto) blast
qed
lemma WCR_imp_CP_join:
assumes "(rstep R)¯ O (rstep R) ⊆ (rstep R)⇧↓"
and "(s, t) ∈ CP R"
shows "(s, t) ∈ (rstep R)⇧↓"
using CP2_imp_peak [OF assms(2)] and assms(1) by blast
text ‹The Critical Pair Lemma›
lemma CP:
assumes "∀(l, r)∈R. vars_term r ⊆ vars_term l"
shows "(rstep R)¯ O (rstep R) ⊆ (rstep R)⇧↓ ⟷ (∀(s, t)∈CP R. (s, t) ∈ (rstep R)⇧↓)"
using CP_join_imp_peak_join [OF assms] and WCR_imp_CP_join [of R] by auto
text ‹A terminating TRS is confluent iff all critical pairs are joinable.›
corollary SN_imp_CR_iff_CP_join:
assumes "∀(l, r)∈R. vars_term r ⊆ vars_term l"
and "SN (rstep R)"
shows "CR (rstep R) ⟷ (∀(s, t)∈CP R. (s, t) ∈ (rstep R)⇧↓)"
using Newman [OF assms(2)] and CP [OF assms(1)]
unfolding WCR_alt_def [symmetric]
by (simp) (metis CR_on_def WCR_onI r_into_rtrancl)
definition
"CP2_rules_pos R R' r p r' =
{(replace_at (fst (π⇩2 ∙ r')) p (snd (π⇩1 ∙ r)) ⋅ σ, snd (π⇩2 ∙ r') ⋅ σ) | π⇩1 π⇩2 σ.
mgu (fst (π⇩1 ∙ r)) (fst (π⇩2 ∙ r') |_ p) = Some σ ∧
overlap R R' (π⇩1 ∙ r) p (π⇩2 ∙ r')}"
definition
CP2' :: "('f, 'v::infinite) trs ⇒ ('f, 'v) trs ⇒ ('f, 'v) rule set set"
where
"CP2' R R' = {CP2_rules_pos R R' r p r' | r p r'. r ∈ R ∧ r' ∈ R' ∧ p ∈ funposs (fst r')}"
lemma finite_CP2':
assumes "finite R" and "finite R'"
shows "finite (CP2' R R')"
proof -
let ?R = "{(r, p, r'). r ∈ R ∧ r' ∈ R' ∧ p ∈ funposs (fst r')}"
have *: "CP2' R R' = (λ(r, p, r'). {(replace_at (fst (π⇩2 ∙ r')) p (snd (π⇩1 ∙ r)) ⋅ σ, snd (π⇩2 ∙ r') ⋅ σ) |
π⇩1 π⇩2 σ. mgu (fst (π⇩1 ∙ r)) (fst (π⇩2 ∙ r') |_ p) = Some σ ∧
overlap R R' (π⇩1 ∙ r) p (π⇩2 ∙ r')}) ` ?R"
by (fastforce simp: CP2'_def CP2_rules_pos_def)
have "{(r, p, r'). r ∈ R ∧ r' ∈ R' ∧ p ∈ funposs (fst r')} ⊆ R × ⋃(funposs ` lhss R') × R'"
by auto
moreover have "finite (R × ⋃(funposs ` lhss R') × R')"
using assms and finite_funposs by auto
ultimately have "finite ?R" by (rule finite_subset)
then show ?thesis unfolding * by (rule finite_imageI)
qed
lemma overlap_permute_rules:
fixes R :: "('f, 'v :: infinite) trs"
assumes "overlap R R' r p r'"
shows "overlap R R' (π ∙ r) p (π ∙ r')"
(is "overlap R R' ?r p ?r'")
proof -
obtain π⇩1' π⇩2' and σ :: "('f, 'v) subst"
where rules: "π⇩1' ∙ r ∈ R" "π⇩2' ∙ r' ∈ R'"
and disj: "vars_rule r ∩ vars_rule r' = {}"
and pos: "p ∈ funposs (fst r')"
and unif: "fst r ⋅ σ = fst r' |_ p ⋅ σ"
and triv: "p = ε ⟹ ¬ (∃π. π ∙ r = r')"
using assms by (auto simp: overlap_def)
have "(π⇩1' + -π) ∙ ?r ∈ R" and "(π⇩2' + -π) ∙ ?r' ∈ R'"
using rules by auto
then have "∃π. π ∙ ?r ∈ R" and "∃π. π ∙ ?r' ∈ R'" by blast+
moreover have "vars_rule ?r ∩ vars_rule ?r' = {}"
unfolding vars_rule_eqvt [symmetric] using disj
unfolding atom_set_pt.inter_eqvt [symmetric] by (simp)
moreover have pos': "p ∈ funposs (fst ?r')" using pos by (simp add: rule_pt.fst_eqvt [symmetric])
moreover have "fst ?r ⋅ conjugate_subst π σ = fst ?r' |_ p ⋅ conjugate_subst π σ"
using unif and funposs_imp_poss [OF pos'] and funposs_imp_poss [OF pos]
by (simp add: eqvt [symmetric])
moreover have "p = ε ⟹ ¬ (∃π. π ∙ ?r = ?r')"
using triv by (auto) (metis left_minus rule_pt.permute_plus rule_pt.permute_zero)
ultimately show ?thesis
by (auto simp: overlap_def)
qed
lemma overlap_permuted_rules:
fixes R :: "('f, 'v :: infinite) trs"
assumes "overlap R R' (π ∙ r) p (π ∙ r')" (is "overlap R R' ?r p ?r'")
shows "overlap R R' r p r'"
proof -
obtain π⇩1' π⇩2' and σ :: "('f, 'v) subst"
where rules: "π⇩1' ∙ ?r ∈ R" "π⇩2' ∙ ?r' ∈ R'"
and disj: "vars_rule ?r ∩ vars_rule ?r' = {}"
and pos: "p ∈ funposs (fst ?r')"
and unif: "fst ?r ⋅ σ = fst ?r' |_ p ⋅ σ"
and triv: "p = ε ⟹ ¬ (∃π. π ∙ ?r = ?r')"
using assms by (auto simp: overlap_def)
have "(π⇩1' + π) ∙ r ∈ R" and "(π⇩2' + π) ∙ r' ∈ R'"
using rules by auto
then have "∃π. π ∙ r ∈ R" and "∃π. π ∙ r' ∈ R'" by blast+
moreover have "vars_rule r ∩ vars_rule r' = {}"
using disj unfolding eqvt [symmetric]
by (metis atom_set_pt.empty_eqvt atom_set_pt.permute_eq_iff)
moreover have pos': "p ∈ funposs (fst r')" using pos by (simp add: rule_pt.fst_eqvt [symmetric])
moreover have "fst r ⋅ ((Var ∘ Rep_perm π) ∘⇩s σ) = fst r' |_ p ⋅ ((Var ∘ Rep_perm π) ∘⇩s σ)"
using unif and funposs_imp_poss [OF pos'] by (simp add: eqvt [symmetric])
moreover have "p = ε ⟹ ¬ (∃π. π ∙ r = r')"
using triv by (auto) (metis diff_add_cancel rule_pt.permute_plus)
ultimately show ?thesis
unfolding overlap_def by blast
qed
lemma overlap_perm_simp [simp]:
"overlap R R' (π ∙ r) p (π ∙ r') = overlap R R' r p r'"
by (metis overlap_permute_rules overlap_permuted_rules)
text ‹Overlaps that origin from the same rules at the same position are variants.›
lemma same_rule_pos_overlap_imp_perm:
fixes R :: "('f, 'v :: infinite) trs"
assumes "overlap R R' (π⇩1 ∙ r) p (π⇩2 ∙ r')"
and "overlap R R' (π⇩3 ∙ r) p (π⇩4 ∙ r')"
shows "∃π. π ∙ (π⇩1 ∙ r) = π⇩3 ∙ r ∧ π ∙ (π⇩2 ∙ r') = π⇩4 ∙ r'"
proof -
from assms obtain τ τ' :: "('f, 'v) subst"
where "vars_rule (π⇩1 ∙ r) ∩ vars_rule (π⇩2 ∙ r') = {}"
and "vars_rule (π⇩3 ∙ r) ∩ vars_rule (π⇩4 ∙ r') = {}"
by (auto simp: overlap_def dest!: funposs_imp_poss)
from rule_variants_imp_perm [OF this(2, 1)] show ?thesis .
qed
text ‹Critical pairs that origin from overlaps which are variants are also variants
of each other.›
lemma overlap_variants_imp_CP_variants:
fixes R R' :: "('f, 'v :: infinite) trs"
assumes ol: "overlap R R' (π⇩1 ∙ r) p (π⇩2 ∙ r')"
"overlap R R' (π⇩3 ∙ r) p (π⇩4 ∙ r')"
and mgu: "mgu (fst (π⇩1 ∙ r)) (fst (π⇩2 ∙ r') |_ p) = Some σ" (is "mgu ?s ?t = _")
"mgu (fst (π⇩3 ∙ r)) (fst (π⇩4 ∙ r') |_ p) = Some σ'" (is "mgu ?u ?v = _")
shows "∃π.
replace_at (fst (π⇩2 ∙ r')) p (snd (π⇩1 ∙ r)) ⋅ σ =
π ∙ (replace_at (fst (π⇩4 ∙ r')) p (snd (π⇩3 ∙ r)) ⋅ σ') ∧
snd (π⇩2 ∙ r') ⋅ σ = π ∙ (snd (π⇩4 ∙ r') ⋅ σ')"
proof -
have "p ∈ poss (fst (π⇩2 ∙ r'))" using ol(1) by (auto simp: overlap_def dest: funposs_imp_poss)
then have p: "p ∈ poss (fst r')" by (simp add: eqvt [symmetric])
have mgu': "is_mgu σ {(?s, ?t)}" "is_mgu σ' {(?u, ?v)}"
using mgu_sound [THEN is_imgu_imp_is_mgu] and mgu by auto
have unif: "?s ⋅ σ = ?t ⋅ σ" "?u ⋅ σ' = ?v ⋅ σ'"
using mgu' by (auto simp: is_mgu_def)
define s and t where "s = fst r" and "t = fst r' |_ p"
have unif: "(π⇩1 ∙ s) ⋅ σ = (π⇩2 ∙ t) ⋅ σ" "(π⇩3 ∙ s) ⋅ σ' = (π⇩4 ∙ t) ⋅ σ'"
using unif and p by (simp add: s_def t_def eqvt)+
have mgu': "is_mgu σ {(π⇩1 ∙ s, π⇩2 ∙ t)}" "is_mgu σ' {(π⇩3 ∙ s, π⇩4 ∙ t)}"
using mgu' and p by (simp add: s_def t_def eqvt)+
from same_rule_pos_overlap_imp_perm [OF ol(2, 1)] obtain π :: "'v perm"
where 0: "π⇩1 ∙ r = π ∙ π⇩3 ∙ r" "π⇩2 ∙ r' = π ∙ π⇩4 ∙ r'" by metis
then have *: "π⇩1 ∙ s = π ∙ π⇩3 ∙ s" "π⇩2 ∙ t = π ∙ π⇩4 ∙ t"
using p by (simp_all add: s_def t_def eqvt)
then have **: "π⇩3 ∙ s = (-π) ∙ π⇩1 ∙ s" "π⇩4 ∙ t = (-π) ∙ π⇩2 ∙ t" by auto
have "is_mgu (sop π ∘⇩s σ) {(π⇩3 ∙ s, π⇩4 ∙ t)}"
proof (unfold is_mgu_def, intro conjI ballI)
fix τ :: "('f, 'v) subst"
assume "τ ∈ unifiers {(π⇩3 ∙ s, π⇩4 ∙ t)}"
then have "π⇩3 ∙ s ⋅ τ = π⇩4 ∙ t ⋅ τ" by (simp add: unifiers_def)
then have "(-π) ∙ π⇩1 ∙ s ⋅ τ = (-π) ∙ π⇩2 ∙ t ⋅ τ" by (simp add: ** )
then have "π⇩1 ∙ s ⋅ sop (-π) ∘⇩s τ = π⇩2 ∙ t ⋅ sop (-π) ∘⇩s τ" by simp
with mgu'(1) obtain μ :: "('f, 'v) subst"
where "sop (-π) ∘⇩s τ = σ ∘⇩s μ"
unfolding is_mgu_def and unifiers_def by force
then have "sop π ∘⇩s sop (-π) ∘⇩s τ = sop π ∘⇩s σ ∘⇩s μ" by (simp add: ac_simps)
then have "τ = sop π ∘⇩s σ ∘⇩s μ" by (simp add: subst_compose_def)
then show "∃μ. τ = sop π ∘⇩s σ ∘⇩s μ" by blast
qed (simp add: unif ** unifiers_def)
moreover have "finite (subst_domain (sop π ∘⇩s σ))"
proof -
have "subst_domain (sop π ∘⇩s σ) ⊆ subst_domain (sop π :: ('f, 'v) subst) ∪ subst_domain σ"
using subst_domain_compose [of "sop π" σ] using [[show_sorts]] .
moreover have "finite (subst_domain (sop π))" by (metis finite_subst_domain_sop)
moreover have "finite (subst_domain σ)" using mgu_finite_subst_domain [OF mgu(1)] .
ultimately show ?thesis by (metis infinite_Un infinite_super)
qed
moreover have "finite (subst_domain σ')" using mgu_finite_subst_domain [OF mgu(2)] .
ultimately obtain π' where 1: "π' ∙ σ' = sop π ∘⇩s σ"
using is_mgu_imp_perm [OF mgu'(2)] by blast
have "replace_at (fst (π⇩2 ∙ r') ⋅ σ) p (snd (π⇩1 ∙ r) ⋅ σ) =
π' ∙ (replace_at (fst (π⇩4 ∙ r')) p (snd (π⇩3 ∙ r)) ⋅ σ')"
proof -
have "replace_at (fst (π⇩2 ∙ r') ⋅ σ) p (snd (π⇩1 ∙ r) ⋅ σ) =
π ∙ replace_at (fst (π⇩4 ∙ r')) p (snd (π⇩3 ∙ r)) ⋅ σ"
using p by (simp add: 0 eqvt ctxt_of_pos_term_subst)
also have "… = π' ∙ (replace_at (fst (π⇩4 ∙ r')) p (snd (π⇩3 ∙ r)) ⋅ σ')"
using 1 apply auto
by (metis permute_subst_subst_compose subst_apply_term_ctxt_apply_distrib subst_subst term_apply_subst_Var_Rep_perm)
finally show ?thesis .
qed
moreover
have "snd (π⇩2 ∙ r') ⋅ σ = π' ∙ (snd (π⇩4 ∙ r') ⋅ σ')"
proof -
have "snd (π⇩2 ∙ r') ⋅ σ = π ∙ snd (π⇩4 ∙ r') ⋅ σ" by (simp add: 0 eqvt)
also have "… = π' ∙ (snd (π⇩4 ∙ r') ⋅ σ')"
using 1 by (metis permute_subst_subst_compose subst_subst term_apply_subst_Var_Rep_perm)
finally show ?thesis .
qed
ultimately show ?thesis
by (metis ctxt_of_pos_term_subst p poss_perm_prod_simps(1) subst_apply_term_ctxt_apply_distrib)
qed
lemma CP2_Union_CP2':
"CP2 R R' = ⋃(CP2' R R')"
proof
show "⋃(CP2' R R') ⊆ CP2 R R'"
proof
fix s t
assume "(s, t) ∈ ⋃(CP2' R R')"
then obtain r p r' π⇩1 π⇩2 σ
where "r ∈ R" and "r' ∈ R'" and p: "p ∈ funposs (fst (π⇩2 ∙ r'))"
and "mgu (π⇩1 ∙ fst r) (π⇩2 ∙ fst r' |_ p) = Some σ"
and ol: "overlap R R' (π⇩1 ∙ r) p (π⇩2 ∙ r')"
and s: "s = replace_at (fst (π⇩2 ∙ r')) p (snd (π⇩1 ∙ r)) ⋅ σ"
and t: "t = snd (π⇩2 ∙ r') ⋅ σ"
by (auto simp: CP2'_def CP2_rules_pos_def eqvt)
then have "σ = the_mgu (π⇩1 ∙ fst r) (π⇩2 ∙ fst r' |_ p)" by (simp add: the_mgu_def)
with ol show "(s, t) ∈ CP2 R R'"
using funposs_imp_poss [OF p]
unfolding CP2_def s t by (force simp add: eqvt ctxt_of_pos_term_subst)
qed
next
show "CP2 R R' ⊆ ⋃(CP2' R R')"
proof
fix s t
assume "(s, t) ∈ CP2 R R'"
then obtain r p r' σ
where ol: "overlap R R' r p r'"
and "σ = the_mgu (fst r) (fst r' |_ p)"
and s: "s = replace_at (fst r') p (snd r) ⋅ σ"
and t: "t = snd r' ⋅ σ"
by (auto simp: CP2_def)
then have mgu: "mgu (fst r) (fst r' |_ p) = Some σ"
unfolding overlap_def the_mgu_def
using unify_complete and unify_sound by (force split: option.splits simp: is_imgu_def unifiers_def)
from ol obtain π⇩1 π⇩2
where "π⇩1 ∙ r ∈ R" (is "?r ∈ R")
and "π⇩2 ∙ r' ∈ R'" (is "?r' ∈ R'")
and p: "p ∈ funposs (fst r')" by (auto simp: overlap_def)
moreover
have "overlap R R' (-π⇩1 ∙ ?r) p (-π⇩2 ∙ ?r')" using ol by simp
moreover
have "s = (ctxt_of_pos_term p (fst (-π⇩2 ∙ ?r')))⟨snd (-π⇩1 ∙ ?r)⟩ ⋅ σ"
and "t = snd (-π⇩2 ∙ ?r') ⋅ σ"
using funposs_imp_poss [OF p] by (simp_all add: s t ctxt_of_pos_term_subst)
moreover
have "mgu (fst (-π⇩1 ∙ ?r)) (fst (-π⇩2 ∙ ?r') |_ p) = Some σ" using mgu by simp
moreover have "p ∈ funposs (fst ?r')" using p by (simp add: eqvt [symmetric])
ultimately show "(s, t) ∈ ⋃(CP2' R R')"
unfolding CP2'_def CP2_rules_pos_def by blast
qed
qed
lemma CP2_rules_pos_perm:
fixes R R' :: "('f, 'v :: infinite) trs"
assumes "x ∈ CP2_rules_pos R R' r p r'"
and "y ∈ CP2_rules_pos R R' r p r'"
shows "∃π. π ∙ x = y"
proof -
from assms [unfolded CP2_rules_pos_def] obtain π⇩1 π⇩2 π⇩3 π⇩4 and σ σ' :: "('f, 'v) subst"
where mgu: "mgu (fst (π⇩1 ∙ r)) (fst (π⇩2 ∙ r') |_ p) = Some σ"
"mgu (fst (π⇩3 ∙ r)) (fst (π⇩4 ∙ r') |_ p) = Some σ'"
and ol: "overlap R R' (π⇩1 ∙ r) p (π⇩2 ∙ r')"
"overlap R R' (π⇩3 ∙ r) p (π⇩4 ∙ r')"
and x: "x = (replace_at (fst (π⇩2 ∙ r')) p (snd (π⇩1 ∙ r)) ⋅ σ, snd (π⇩2 ∙ r') ⋅ σ)"
and y: "y = (replace_at (fst (π⇩4 ∙ r')) p (snd (π⇩3 ∙ r)) ⋅ σ', snd (π⇩4 ∙ r') ⋅ σ')"
by blast
show ?thesis
using overlap_variants_imp_CP_variants [OF ol(2, 1) mgu(2, 1)]
by (auto simp: x y eqvt)
qed
lemma CP2_rules_pos_join:
assumes "x ∈ CP2_rules_pos R R' r p r'"
and "y ∈ CP2_rules_pos R R' r p r'"
shows "x ∈ (rstep S)⇧↓ ⟷ y ∈ (rstep S)⇧↓"
using CP2_rules_pos_perm [OF assms] by auto
abbreviation "CP' R ≡ CP2' R R"
text ‹If @{term R} and @{term R'} are finite, then @{term "CP2' R R'"} is finite
by @{thm finite_CP2'}. Thus it suffices to prove joinability of finitely many
critical pairs in order to conclude joinability of all critical pairs @{term "CP2 R R'"}.›
lemma CP2'_representatives_join_imp_CP2_join:
assumes "∀C∈CP2' R R'. ∃(s, t)∈C. (s, t) ∈ (rstep S)⇧↓"
shows "∀(s, t)∈CP2 R R'. (s, t) ∈ (rstep S)⇧↓"
using assms
by (auto simp: CP2'_def CP2_Union_CP2')
(blast dest: CP2_rules_pos_join [of _ R R' _ _ _ _ S])
lemma CS3_ctxt:
assumes "(t, p, s, u) ∈ CS3 A"
shows "(C⟨t⟩, hole_pos C <#> p, C⟨s⟩, C⟨u⟩) ∈ CS3 A"
proof -
from assms obtain D σ t' s' u' p'
where "(t', p', s', u') ∈ A" and "t = D⟨t' ⋅ σ⟩" "s = D⟨s' ⋅ σ⟩" "u = D⟨u' ⋅ σ⟩"
and "p = hole_pos D <#> p'"
by (cases)
with CS3.intros [OF this(1), of "C ∘⇩c D" σ] show ?thesis by simp
qed
lemma overlap_imp_rstep:
assumes "overlap R R' r p r'"
shows "r ∈ rstep R" and "r' ∈ rstep R'"
apply (insert assms)
apply (case_tac [!] r, case_tac [!] r')
apply (auto simp: overlap_def)
by (metis perm_rstep_conv rstep.rule surj_pair)+
lemma overlap_imp_rstep_pos_Empty:
fixes R :: "('f, 'v :: infinite) trs"
assumes "overlap R R' r p r'"
shows "r ∈ rstep_pos R ε" and "r' ∈ rstep_pos R' ε"
proof -
from assms [unfolded overlap_def] obtain π⇩1 π⇩2 l⇩1 r⇩1 l⇩2 r⇩2 and σ :: "('f, 'v) subst"
where p: "p ∈ poss l⇩2"
and [simp]: "r = (l⇩1, r⇩1)" "r' = (l⇩2, r⇩2)"
and 1: "(l⇩1, r⇩1) ∈ -π⇩1 ∙ R" and 2: "(l⇩2, r⇩2) ∈ -π⇩2 ∙ R'"
by (cases r, cases r') (fastforce dest: funposs_imp_poss)
from rstep_pos.intros [OF 1, of ε l⇩1 Var]
show "r ∈ rstep_pos R ε" by simp
from rstep_pos.intros [OF 2, of ε l⇩2 Var]
show "r' ∈ rstep_pos R' ε" by simp
qed
lemma overlap_source_eq:
fixes R :: "('f, 'v :: infinite) trs" and r p r'
defines "σ ≡ the_mgu (fst r) (fst r' |_ p)"
assumes "overlap R R' r p r'"
shows "p ∈ poss (fst r')" (is ?A)
and "fst r' ⋅ σ = replace_at (fst r') p (fst r) ⋅ σ" (is ?B)
proof -
from assms obtain τ :: "('f, 'v) subst"
where p: "p ∈ poss (fst r')"
and "fst r ⋅ τ = (fst r' |_ p) ⋅ τ"
by (auto simp: overlap_def dest: funposs_imp_poss)
from the_mgu [OF this(2)] and assms
have "fst r ⋅ σ = (fst r' |_ p) ⋅ σ" by simp
with p show ?B by (metis ctxt_supt_id subst_apply_term_ctxt_apply_distrib)
show ?A by fact
qed
lemma overlap_rstep_pos_right:
fixes R :: "('f, 'v :: infinite) trs" and r p r'
defines "σ ≡ the_mgu (fst r) (fst r' |_ p)"
assumes ol: "overlap R R' r p r'"
shows "(fst r' ⋅ σ, snd r' ⋅ σ) ∈ rstep_pos R' ε"
using overlap_imp_rstep_pos_Empty(2) [OF ol]
and overlap_source_eq [OF ol, folded σ_def]
and rstep_pos_subst [of "fst r'" "snd r'" R' ε σ]
by simp
lemma overlap_rstep_pos_left:
fixes R :: "('f, 'v :: infinite) trs" and r p r'
defines "σ ≡ the_mgu (fst r) (fst r' |_ p)"
assumes ol: "overlap R R' r p r'"
shows "(fst r' ⋅ σ, (ctxt_of_pos_term p (fst r'))⟨snd r⟩ ⋅ σ) ∈ rstep_pos R p"
using overlap_imp_rstep_pos_Empty(1) [OF ol]
and overlap_source_eq [OF ol, folded σ_def]
and rstep_pos_supt [of "fst r ⋅ σ" "snd r ⋅ σ" R ε p "fst r' ⋅ σ"]
apply (cases r, cases r')
apply auto
by (metis ctxt_of_pos_term_subst poss_imp_subst_poss rstep_pos_subst subt_at_ctxt_of_pos_term)
end