Theory TRS.Critical_Pairs_Innermost
theory Critical_Pairs_Innermost
imports
First_Order_Rewriting.Critical_Pairs
Q_Restricted_Rewriting
begin
context
fixes ren :: "'v :: infinite renaming2"
begin
lemma critical_pairs_innermost_weak_diamond:
fixes R :: "('f, 'v) trs"
assumes cp: "⋀ l r. (True, l, r) ∈ critical_pairs ren R R ⟹ l = r"
and NF_Q_R: "NF_terms Q ⊆ NF_trs R"
and lhss: "⋀ l r. (l, r) ∈ R ⟹ is_Fun l"
shows "w◇ (qrstep nfs Q R)"
unfolding weak_diamond_def
proof
fix t1 t2 :: "('f, 'v) term"
let ?R = "qrstep nfs Q R"
assume "(t1, t2) ∈ ?R^-1 O ?R - Id"
then obtain s where st1: "(s, t1) ∈ ?R" and st2: "(s, t2) ∈ ?R" and t12: "t1 ≠ t2" by auto
let ?Q = "NF_terms Q"
from st1 obtain C1 l1 r1 σ1 where lr1: "(l1, r1) ∈ R" and s1: "s = C1⟨l1 ⋅ σ1⟩" and t1: "t1 = C1⟨r1 ⋅ σ1⟩"
and NF1: "∀ u ⊲ l1 ⋅ σ1. u ∈ ?Q" and nfs1: "NF_subst nfs (l1, r1) σ1 Q" by auto
from st2 obtain C2 l2 r2 σ2 where lr2: "(l2, r2) ∈ R" and s2: "s = C2⟨l2 ⋅ σ2⟩" and t2: "t2 = C2⟨r2 ⋅ σ2⟩"
and NF2: "∀ u ⊲ l2 ⋅ σ2. u ∈ ?Q" and nfs2: "NF_subst nfs (l2, r2) σ2 Q" by auto
from s1 s2 have id: "C1⟨l1 ⋅ σ1⟩ = C2⟨l2 ⋅ σ2⟩" by simp
let ?p = "λ (C1, C2). C1⟨l1 ⋅ σ1⟩ = C2⟨l2 ⋅ σ2⟩ ⟶ (∃ s'. (C1⟨r1 ⋅ σ1⟩, s') ∈ ?R ∧ (C2⟨r2 ⋅ σ2⟩, s') ∈ ?R ∨ C1⟨r1 ⋅ σ1⟩ = C2⟨r2 ⋅ σ2⟩)"
{
fix C12
let ?m = "λ (C1, C2). size C1 + size C2"
have "?p C12"
proof (induct rule: wf_induct [OF wf_measure [of ?m], of ?p])
case (1 C12)
obtain C1 C2 where C12: "C12 = (C1, C2)" by force
show "?p C12" unfolding C12 split
proof (intro impI)
assume id: "C1⟨l1 ⋅ σ1⟩ = C2⟨l2 ⋅ σ2⟩"
show "∃ s'. ( (C1⟨r1 ⋅ σ1⟩, s') ∈ ?R ∧ (C2⟨r2 ⋅ σ2⟩, s') ∈ ?R ∨ C1⟨r1 ⋅ σ1⟩ = C2⟨r2 ⋅ σ2⟩)"
proof (cases C1)
case Hole note C1 = this
with id have id: "l1 ⋅ σ1 = C2⟨l2 ⋅ σ2⟩" by simp
have C2: "C2 = □"
proof (rule ccontr)
assume "C2 ≠ □"
with id have "l2 ⋅ σ2 ⊲ l1 ⋅ σ1" by auto
with NF1 NF_Q_R have "l2 ⋅ σ2 ∈ NF_trs R" by auto
with lr2 show False by auto
qed
with id have ident: "l1 ⋅ σ1 = l2 ⋅ σ2" by simp
from lhss [OF lr1] have nvar: "is_Fun l1" .
from mgu_vd_complete [OF ident]
obtain μ1 μ2 ρ where mgu: "mgu_vd ren l1 l2 = Some (μ1, μ2)" and
μ1: "σ1 = μ1 ∘⇩s ρ"
and μ2: "σ2 = μ2 ∘⇩s ρ"
by blast
have in_cp: "(True, r2 ⋅ μ2, r1 ⋅ μ1) ∈ critical_pairs ren R R"
by (rule critical_pairsI [OF lr1 lr2 _ nvar mgu, of □], auto)
from C2 have C2rσ: "C2⟨r2 ⋅ σ2⟩ = r2 ⋅ σ2" by simp
from C1 have C1rσ: "C1⟨r1 ⋅ σ1⟩ = r1 ⋅ σ1" by simp
from cp [OF in_cp, unfolded instance_rule_def] have id: "r1 ⋅ μ1 = r2 ⋅ μ2" ..
from C1rσ have "C1⟨r1 ⋅ σ1⟩ = r2 ⋅ σ2" unfolding μ1 using id μ2 by simp
also have "... = C2⟨r2 ⋅ σ2⟩" unfolding C2rσ ..
finally show ?thesis by simp
next
case (More f1 bef1 D1 aft1) note C1 = this
show ?thesis
proof (cases C2)
case Hole
with id have "l2 ⋅ σ2 = C1⟨l1 ⋅ σ1⟩" by auto
with C1 have "l1 ⋅ σ1 ⊲ l2 ⋅ σ2" by auto
with NF2 NF_Q_R have "l1 ⋅ σ1 ∈ NF_trs R" by auto
with lr1 have False by auto
then show ?thesis ..
next
case (More f2 bef2 D2 aft2) note C2 = this
let ?n1 = "length bef1"
let ?n2 = "length bef2"
note id = id [unfolded C1 C2]
from id have f: "f1 = f2" by simp
show ?thesis
proof (cases "?n1 = ?n2")
case True
with id have idb: "bef1 = bef2" and ida: "aft1 = aft2"
and idD: "D1⟨l1 ⋅ σ1⟩ = D2⟨l2 ⋅ σ2⟩" by auto
have "((D1, D2), C12) ∈ measure ?m" unfolding C12 C1 C2
by auto
from 1 [rule_format, OF this, unfolded split, rule_format,
OF idD] obtain s'
where disj: "(D1⟨r1 ⋅ σ1⟩, s') ∈ ?R ∧ (D2⟨r2 ⋅ σ2⟩, s') ∈ ?R ∨ D1⟨r1 ⋅ σ1⟩ = D2⟨r2 ⋅ σ2⟩" (is "?seq1 ∧ ?seq2 ∨ ?id") by auto
let ?C = "More f2 bef2 □ aft2"
have id1: "C1 = ?C ∘⇩c D1" unfolding C1 f ida idb by simp
have id2: "C2 = ?C ∘⇩c D2" unfolding C2 by simp
from disj show ?thesis
proof
assume "?seq1 ∧ ?seq2"
then have seq1: "?seq1" and seq2: "?seq2" by auto
from qrstep.ctxt [OF seq1, of ?C]
have seq1: "(C1⟨r1 ⋅ σ1⟩, ?C⟨s'⟩) ∈ ?R" using id1 by auto
from qrstep.ctxt [OF seq2, of ?C]
have seq2: "(C2⟨r2 ⋅ σ2⟩, ?C⟨s'⟩) ∈ ?R" using id2 by auto
from seq1 seq2 show ?thesis by auto
next
assume ?id
then show ?thesis unfolding id1 id2 by simp
qed
next
case False
let ?p1 = "?n1 # hole_pos D1"
let ?p2 = "?n2 # hole_pos D2"
have l2: "C1⟨l1 ⋅ σ1⟩ |_ ?p2 = l2 ⋅ σ2" unfolding C1 id by simp
have p12: "?p1 ⊥ ?p2" using False by simp
have p1: "?p1 ∈ poss (C1⟨l1 ⋅ σ1⟩)" unfolding C1 by simp
have p2: "?p2 ∈ poss (C1⟨l1 ⋅ σ1⟩)" unfolding C1 unfolding id by simp
let ?one = "replace_at (C1⟨l1 ⋅ σ1⟩) ?p1 (r1 ⋅ σ1)"
have one: "C1⟨r1 ⋅ σ1⟩ = ?one" unfolding C1 by simp
from parallel_qrstep [OF p12 p1 p2 l2 NF2 lr2 nfs2]
have "(?one, replace_at ?one ?p2 (r2 ⋅ σ2)) ∈ qrstep nfs Q R" .
then have one: "(C1⟨r1 ⋅ σ1⟩, replace_at ?one ?p2 (r2 ⋅ σ2)) ∈ qrstep nfs Q R" unfolding one by simp
have l1: "C2⟨l2 ⋅ σ2⟩ |_ ?p1 = l1 ⋅ σ1" unfolding C2 id [symmetric] by simp
have p21: "?p2 ⊥ ?p1" using False by simp
have p1': "?p1 ∈ poss (C2⟨l2 ⋅ σ2⟩)" unfolding C2 id [symmetric] by simp
have p2': "?p2 ∈ poss (C2⟨l2 ⋅ σ2⟩)" unfolding C2 by simp
let ?two = "replace_at (C2⟨l2 ⋅ σ2⟩) ?p2 (r2 ⋅ σ2)"
have two: "C2⟨r2 ⋅ σ2⟩ = ?two" unfolding C2 by simp
from parallel_qrstep [OF p21 p2' p1' l1 NF1 lr1 nfs1]
have "(?two, replace_at ?two ?p1 (r1 ⋅ σ1)) ∈ qrstep nfs Q R" .
then have two: "(C2⟨r2 ⋅ σ2⟩, replace_at ?two ?p1 (r1 ⋅ σ1)) ∈ qrstep nfs Q R" unfolding two by simp
have "replace_at ?one ?p2 (r2 ⋅ σ2) = replace_at (replace_at (C1⟨l1 ⋅ σ1⟩) ?p2 (r2 ⋅ σ2)) ?p1 (r1 ⋅ σ1)"
by (rule parallel_replace_at [OF p12 p1 p2])
also have "... = replace_at ?two ?p1 (r1 ⋅ σ1)" unfolding C1 C2 id ..
finally have one_two: "replace_at ?one ?p2 (r2 ⋅ σ2) = replace_at ?two ?p1 (r1 ⋅ σ1)" .
show ?thesis
by (intro exI disjI1 conjI, rule one, unfold one_two, rule two)
qed
qed
qed
qed
qed
}
from this [of "(C1, C2)", unfolded split, rule_format, OF id]
show "(t1, t2) ∈ ?R O ?R^-1" using t12 unfolding t1 t2 by auto
qed
lemma critical_pairs_innermost:
assumes "⋀ l r. (True, l, r) ∈ critical_pairs ren R R ⟹ l = r"
and "NF_terms Q ⊆ NF_trs R"
and "⋀ l r. (l, r) ∈ R ⟹ is_Fun l"
shows "CR (qrstep nfs Q R)"
by (rule weak_diamond_imp_CR [OF critical_pairs_innermost_weak_diamond [OF assms]])
end
end