theory Strongly_Closed
imports
Critical_Pairs
QTRS.More_Abstract_Rewriting
begin
lemma linear_variable_overlap_commute:
assumes st:"(s, t) ∈ rstep_r_p_s R1 (l1, r1) p1 σ1"
and su:"(s, u) ∈ rstep_r_p_s R2 (l2, r2) p2 σ2"
and q:"p2 = p1 <#> q"
and var:"q ∉ funposs l1"
and lin: "linear_trs R1"
shows "∃v. (t, v) ∈ (rstep R2)⇧= ∧ (u, v) ∈ rstep R1"
proof -
from st su have p1: "p1 ∈ poss s" and σ1: "s |_ p1 = l1 ⋅ σ1"
and t: "t = replace_at s p1 (r1 ⋅ σ1)" and lr1: "(l1, r1) ∈ R1" and p2: "p2 ∈ poss s"
and σ2: "s |_ p2 = l2 ⋅ σ2" and u: "u = replace_at s p2 (r2 ⋅ σ2)" and lr2: "(l2, r2) ∈ R2"
unfolding rstep_r_p_s_def' by auto
from q have l2q:"(l1 ⋅ σ1) |_ q = l2 ⋅ σ2" using σ1 σ2 p1 p2 by auto
from q u σ1 have up1:"u = replace_at s p1 (replace_at (l1 ⋅ σ1) q (r2 ⋅ σ2))"
using ctxt_of_pos_term_append[OF p1] ctxt_ctxt by auto
from var have "¬(q ∈ poss l1 ∧ is_Fun (l1 |_ q))"
by (metis DiffI is_Var_def poss_simps(3) varposs_iff)
then obtain q1 q2 x where q12:"q = q1 <#> q2" and q1:"q1 ∈ poss l1" and x:"l1 |_ q1 = Var x"
using σ1 p2 pos_into_subst[of l1 σ1 "s |_ p1" q] poss_append_poss q by auto
then have xq2:"σ1 x |_ q2 = l2 ⋅ σ2" using l2q by auto
have q1l1σ1:"q1 ∈ poss (l1 ⋅ σ1)" using q1 by simp
define τ where "τ ≡ λ y. if y = x then replace_at (σ1 x) q2 (r2 ⋅ σ2) else σ1 y"
let ?cr = "replace_at s p1 (r1 ⋅ τ)"
from lin lr1 have linl1:"linear_term l1" and linr1: "linear_term r1" by (auto dest: linear_trsE)
from linear_term_replace_in_subst[OF linl1 q1 x, of σ1 τ]
have "l1 ⋅ τ = replace_at (l1 ⋅ σ1) q1 (τ x)" by (simp add: τ_def)
also have "... = replace_at (l1 ⋅ σ1) q (r2 ⋅ σ2)"
using q12 q1 x ctxt_of_pos_term_append[OF q1l1σ1] ctxt_ctxt τ_def by auto
finally have "l1 ⋅ τ = replace_at (l1 ⋅ σ1) q (r2 ⋅ σ2)" .
with up1 have "u = replace_at s p1 (l1 ⋅ τ)" by auto
then have ucr:"(u, ?cr) ∈ rstep R1" using subset_rstep lr1 by auto
have tcr:"(t, ?cr) ∈ (rstep R2)⇧="
proof (cases "x ∈ vars_term r1")
case False
then have "r1 ⋅ τ = r1 ⋅ σ1" by (induct r1) (auto simp: τ_def)
then show ?thesis using t by auto
next
case True
obtain q' where q':"q' ∈ poss r1" and q'x:"r1 |_ q' = Var x"
using supteq_imp_subt_at[OF supteq_Var[OF True]] by auto
have qr1σ1:"q' ∈ poss (r1 ⋅ σ1)" using q' by simp
from linear_term_replace_in_subst[OF linr1 q' q'x, of σ1 τ]
have "r1 ⋅ τ = replace_at (r1 ⋅ σ1) q' (τ x)" by (simp add: τ_def)
also have "... = replace_at (r1 ⋅ σ1) q' (replace_at (σ1 x) q2 (r2 ⋅ σ2))" by (simp add: τ_def)
also have "... = replace_at (r1 ⋅ σ1) (q' <#> q2) (r2 ⋅ σ2)"
using q' q'x ctxt_of_pos_term_append[OF qr1σ1] ctxt_ctxt by auto
finally have r1τ:"r1 ⋅ τ = replace_at (r1 ⋅ σ1) (q' <#> q2) (r2 ⋅ σ2)" .
from xq2 q'x have "(r1 ⋅ σ1) |_ (q' <#> q2) = l2 ⋅ σ2"
using q' subt_at_append[OF qr1σ1, of q2] by auto
then have "r1 ⋅ σ1 = (ctxt_of_pos_term (q' <#> q2) (r1 ⋅ σ1))⟨l2 ⋅ σ2⟩"
using qr1σ1 ctxt_supt_id σ1 p2 poss_append_poss q' q'x subt_at_subst q q1 q12 x by metis
from rstepI[OF lr2 this] r1τ have "(r1 ⋅ σ1, r1 ⋅ τ) ∈ rstep R2" by simp
then show ?thesis using t by blast
qed
from tcr ucr show ?thesis by blast
qed
lemma strongly_closed_linear_strongly_commute:
assumes closed_1:"⋀b p q. (b, p, q) ∈ critical_pairs R1 R2 ⟹ ∃v. (p, v) ∈ (rstep R2)⇧= ∧ (q, v) ∈ (rstep R1)⇧*"
assumes closed_2:"⋀b p q. (b, p, q) ∈ critical_pairs R2 R1 ⟹ ∃v. (p, v) ∈ (rstep R1)⇧* ∧ (q, v) ∈ (rstep R2)⇧="
and lin: "linear_trs R1" "linear_trs R2"
shows "strongly_commute (rstep R1) (rstep R2)"
proof
let ?R1 = "rstep R1"
let ?R2 = "rstep R2"
fix s t u
assume "(s, t) ∈ ?R1" and "(s, u) ∈ ?R2"
then obtain l1 r1 p1 σ1 l2 r2 p2 σ2
where st:"(s, t) ∈ rstep_r_p_s R1 (l1, r1) p1 σ1"
and su:"(s, u) ∈ rstep_r_p_s R2 (l2, r2) p2 σ2"
using rstep_iff_rstep_r_p_s by metis
then have p1: "p1 ∈ poss s" and σ1: "s |_ p1 = l1 ⋅ σ1"
and t: "t = replace_at s p1 (r1 ⋅ σ1)" and lr1: "(l1, r1) ∈ R1" and p2: "p2 ∈ poss s"
and σ2: "s |_ p2 = l2 ⋅ σ2" and u: "u = replace_at s p2 (r2 ⋅ σ2)" and lr2: "(l2, r2) ∈ R2"
unfolding rstep_r_p_s_def' by auto
consider (parallel) "p1 ⊥ p2" | (nested1) "p1 ≤ p2" | (nested2) "p2 ≤ p1"
using parallel_pos by auto
then show "∃v. (t, v) ∈ ?R2⇧= ∧ (u, v) ∈ ?R1⇧*"
proof (cases)
case parallel
then show ?thesis using parallel_steps st su by (blast dest: rstep_r_p_s_imp_rstep)
next
case nested1
then obtain q where q:"p2 = p1 <#> q" using less_eq_pos_def by auto
then have l2q:"(l1 ⋅ σ1) |_ q = l2 ⋅ σ2" using σ1 σ2 p1 p2 by auto
from q u σ1 have up1:"u = replace_at s p1 (replace_at (l1 ⋅ σ1) q (r2 ⋅ σ2))"
using ctxt_of_pos_term_append[OF p1] ctxt_ctxt by auto
show ?thesis
proof (cases "q ∈ funposs l1")
case True
then have ql1:"q ∈ poss l1" and l1q:"is_Fun (l1 |_ q)" and l1qs1: "l1 |_ q ⋅ σ1 = l2 ⋅ σ2"
using funposs_fun_conv[OF True] funposs_imp_poss[OF True] l2q subt_at_subst by auto
from mgu_var_disjoint_string_complete[OF l1qs1]
obtain μ1 μ2 δ where mgu: "mgu_var_disjoint_string (l1 |_ q) l2 = Some (μ1,μ2)"
and d1:"σ1 = μ1 ∘⇩s δ" and d2:"σ2 = μ2 ∘⇩s δ" and mu12:"l1 |_ q ⋅ μ1 = l2 ⋅ μ2"
by auto
define t' where "t' ≡ r1 ⋅ μ1"
define u' where "u' ≡ (ctxt_of_pos_term q l1 ⋅⇩c μ1)⟨r2 ⋅ μ2⟩"
from critical_pairsI[OF lr1 lr2 _ l1q mgu] ctxt_supt_id[OF ql1]
have "(ctxt_of_pos_term q l1 = □, t', u') ∈ critical_pairs R1 R2"
unfolding t'_def u'_def by auto
from closed_1[OF this] obtain v where v: "(t', v) ∈ ?R2⇧= ∧ (u', v) ∈ ?R1⇧*" by auto
from d2 d1 have d2:"u' ⋅ δ = replace_at (l1 ⋅ σ1) q (r2 ⋅ σ2)"
unfolding u'_def using ctxt_compose_subst_compose_distrib ctxt_of_pos_term_subst[OF ql1]
subst_apply_term_ctxt_apply_distrib subst_subst by metis
from d1 t'_def have "t' ⋅ δ = r1 ⋅ σ1" by auto
with t have tt':"t = replace_at s p1 (t' ⋅ δ)" by auto
from d2 u up1 have uu':"u = replace_at s p1 (u' ⋅ δ)" by auto
from v have vsteps:"(t' ⋅ δ, v ⋅ δ) ∈ ?R2⇧= ∧ (u' ⋅ δ, v ⋅ δ) ∈ ?R1⇧*"
using rstep.subst rstep_id rstep_union rsteps_closed_subst by metis
from vsteps tt' have "(t, replace_at s p1 (v ⋅ δ)) ∈ ?R2⇧=" by auto
moreover from vsteps uu' have "(u, replace_at s p1 (v ⋅ δ)) ∈ ?R1⇧*"
using rsteps_closed_ctxt by auto
ultimately show ?thesis by blast
next
case False
with linear_variable_overlap_commute st su q lin show ?thesis by blast
qed
next
case nested2
then obtain q where q:"p1 = p2 <#> q" using less_eq_pos_def by auto
then have l1q:"(l2 ⋅ σ2) |_ q = l1 ⋅ σ1" using σ1 σ2 p1 p2 by auto
from q t σ2 have tp2:"t = replace_at s p2 (replace_at (l2 ⋅ σ2) q (r1 ⋅ σ1))"
using ctxt_of_pos_term_append[OF p2] ctxt_ctxt by auto
show ?thesis
proof (cases "q ∈ funposs l2")
case True
then have ql2:"q ∈ poss l2" and l2q:"is_Fun (l2 |_ q)" and l2qs2: "l2 |_ q ⋅ σ2 = l1 ⋅ σ1"
using funposs_fun_conv[OF True] funposs_imp_poss[OF True] l1q subt_at_subst by auto
from mgu_var_disjoint_string_complete[OF l2qs2]
obtain μ1 μ2 δ where mgu: "mgu_var_disjoint_string (l2 |_ q) l1 = Some (μ2, μ1)"
and d1:"σ1 = μ1 ∘⇩s δ" and d2:"σ2 = μ2 ∘⇩s δ" and mu12:"l2 |_ q ⋅ μ2 = l1 ⋅ μ1"
by auto
define u' where "u' ≡ r2 ⋅ μ2"
define t' where "t' ≡ (ctxt_of_pos_term q l2 ⋅⇩c μ2)⟨r1 ⋅ μ1⟩"
from critical_pairsI[OF lr2 lr1 _ l2q mgu] ctxt_supt_id[OF ql2]
have "(ctxt_of_pos_term q l2 = □, u', t') ∈ critical_pairs R2 R1"
unfolding t'_def u'_def by auto
from closed_2[OF this] obtain v where v: "(t', v) ∈ ?R2⇧= ∧ (u', v) ∈ ?R1⇧*" by auto
from d2 d1 have d1:"t' ⋅ δ = replace_at (l2 ⋅ σ2) q (r1 ⋅ σ1)"
unfolding t'_def using ctxt_compose_subst_compose_distrib ctxt_of_pos_term_subst[OF ql2]
subst_apply_term_ctxt_apply_distrib subst_subst by metis
from d2 u'_def have "u' ⋅ δ = r2 ⋅ σ2" by auto
with u have uu':"u = replace_at s p2 (u' ⋅ δ)" by auto
from d1 t tp2 have tt':"t = replace_at s p2 (t' ⋅ δ)" by auto
from v have vsteps:"(t' ⋅ δ, v ⋅ δ) ∈ ?R2⇧= ∧ (u' ⋅ δ, v ⋅ δ) ∈ ?R1⇧*"
using rstep.subst rstep_id rstep_union rsteps_closed_subst by metis
from vsteps tt' have "(t, replace_at s p2 (v ⋅ δ)) ∈ ?R2⇧=" by auto
moreover from vsteps uu' have "(u, replace_at s p2 (v ⋅ δ)) ∈ ?R1⇧*"
using rsteps_closed_ctxt by auto
ultimately show ?thesis by blast
next
case False
with linear_variable_overlap_commute st su q lin show ?thesis by blast
qed
qed
qed
definition strongly_closed :: "('f,string) trs ⇒ bool"
where
"strongly_closed R = (∀ (b, p, q) ∈ critical_pairs R R.
∃s r. (p, r) ∈ (rstep R)⇧* ∧ (q, r) ∈ (rstep R)⇧=
∧ (p, s) ∈ (rstep R)⇧= ∧ (q, s) ∈ (rstep R)⇧*)"
corollary strongly_closed_linear_CR:
assumes "strongly_closed R"
and "linear_trs R"
shows "CR (rstep R)"
using assms unfolding CR_iff_self_commute strongly_closed_def
by (auto intro!: strongly_commute_imp_commute strongly_closed_linear_strongly_commute)
end