section ‹The Critical Pair Lemma (with variables fixed to type string)›
theory Critical_Pairs
imports
QTRS.Q_Restricted_Rewriting
QTRS.Unification_More
begin
">definition
critical_pairs :: "('f, string) trs ⇒ ('f, string) trs ⇒ (bool × ('f, string) rule) set"
where
"critical_pairs P R = { (C = □, r ⋅ σ, (C ⋅⇩c σ)⟨r' ⋅ τ⟩) | l r l' r' l'' C σ τ.
(l, r) ∈ P ∧ (l', r') ∈ R ∧ l = C⟨l''⟩ ∧ is_Fun l'' ∧
mgu_var_disjoint_string l'' l' = Some (σ, τ) }"
lemma critical_pairsI:
assumes "(l, r) ∈ P" and "(l', r') ∈ R" and "l = C⟨l''⟩"
and "is_Fun l''" and "mgu_var_disjoint_string l'' l' = Some (σ, τ)" and "s = r ⋅ σ"
and "t = (C ⋅⇩c σ)⟨r' ⋅ τ⟩" and "b = (C = □)"
shows "(b, s, t) ∈ critical_pairs P R"
using assms unfolding critical_pairs_def by blast
lemma critical_pairs_mono:
assumes "S⇩1 ⊆ R⇩1" and "S⇩2 ⊆ R⇩2" shows "critical_pairs S⇩1 S⇩2 ⊆ critical_pairs R⇩1 R⇩2"
unfolding critical_pairs_def using assms by blast
lemma critical_pairs_main:
fixes R :: "('f, string) trs"
assumes st1: "(s, t1) ∈ rstep R" and st2: "(s, t2) ∈ rstep R"
shows "(t1, t2) ∈ join (rstep R) ∨
(∃ C b l r σ. t1 = C⟨l ⋅ σ⟩ ∧ t2 = C⟨r ⋅ σ⟩ ∧
((b, l, r) ∈ critical_pairs R R ∨ (b, r, l) ∈ critical_pairs R R))"
proof -
let ?R = "rstep R"
let ?CP = "critical_pairs R R"
from st1 obtain C1 l1 r1 σ1 where lr1: "(l1, r1) ∈ R" and s1: "s = C1⟨l1 ⋅ σ1⟩" and t1: "t1 = C1⟨r1 ⋅ σ1⟩" 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⟩" by auto
from s1 s2 have id: "C1⟨l1 ⋅ σ1⟩ = C2⟨l2 ⋅ σ2⟩" by simp
let ?q = "λ s t. (s, t) ∈ join ?R ∨ (∃ C b l r σ. s = C⟨l ⋅ σ⟩ ∧ t = C⟨r ⋅ σ⟩ ∧ ((b, l, r) ∈ ?CP ∨ (b, r, l) ∈ ?CP))"
let ?p = "λ (C1, C2). ∀ l1 r1 l2 r2 σ1 σ2. (l1, r1) ∈ R ⟶ (l2, r2) ∈ R ⟶ C1⟨l1 ⋅ σ1⟩ = C2⟨l2 ⋅ σ2⟩ ⟶ ?q (C1⟨r1 ⋅ σ1⟩) (C2⟨r2 ⋅ σ2⟩)"
{
fix C12
let ?m = "[λ (C1, C2). size C1 + size C2, λ (C1, C2). size C1]"
have "?p C12"
proof (induct rule: wf_induct [OF wf_measures [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 allI impI)
fix l1 r1 l2 r2 σ1 σ2
assume lr1: "(l1, r1) ∈ R" and lr2: "(l2, r2) ∈ R" and id: "C1⟨l1 ⋅ σ1⟩ = C2⟨l2 ⋅ σ2⟩"
show "?q (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
let ?p = "hole_pos C2"
show ?thesis
proof (cases "?p ∈ poss l1 ∧ is_Fun (l1 |_ ?p)")
case True
hence p: "?p ∈ poss l1" by auto
from ctxt_supt_id [OF p] obtain D where Dl1: "D⟨l1 |_ ?p⟩ = l1"
and D: "D = ctxt_of_pos_term (hole_pos C2) l1" by blast
from arg_cong [OF Dl1, of "λ t. t ⋅ σ1"]
have "(D ⋅⇩c σ1)⟨(l1 |_ ?p) ⋅ σ1⟩ = C2⟨l2 ⋅ σ2⟩" unfolding id by simp
from arg_cong [OF this, of "λ t. t |_ ?p"]
have "l2 ⋅ σ2 = (D ⋅⇩c σ1)⟨(l1 |_ ?p) ⋅ σ1⟩ |_ ?p" by simp
also have "... = (D ⋅⇩c σ1)⟨(l1 |_ ?p) ⋅ σ1⟩ |_ (hole_pos (D ⋅⇩c σ1))"
using hole_pos_ctxt_of_pos_term [OF p] unfolding D by simp
also have "... = (l1 |_ ?p) ⋅ σ1" by (rule subt_at_hole_pos)
finally have ident: "l2 ⋅ σ2 = l1 |_ ?p ⋅ σ1" by auto
from mgu_var_disjoint_string_complete [OF ident [symmetric]]
obtain μ1 μ2 ρ where mgu: "mgu_var_disjoint_string (l1 |_ ?p) l2 = Some (μ1, μ2)" and
μ1: "σ1 = μ1 ∘⇩s ρ"
and μ2: "σ2 = μ2 ∘⇩s ρ"
and ident': "l1 |_ ?p ⋅ μ1 = l2 ⋅ μ2" by blast
have in_cp: "(D = □, r1 ⋅ μ1, (D ⋅⇩c μ1)⟨r2 ⋅ μ2⟩) ∈ critical_pairs R R"
by (rule critical_pairsI [OF lr1 lr2 Dl1 [symmetric] True [THEN conjunct2] mgu], auto)
from hole_pos_ctxt_of_pos_term [OF p] D have pD: "?p = hole_pos D" by simp
from id have C2: "C2 = ctxt_of_pos_term ?p (l1 ⋅ σ1)" by simp
have "C2⟨r2 ⋅ σ2⟩ = (ctxt_of_pos_term ?p (l1 ⋅ σ1))⟨r2 ⋅ σ2⟩" using C2 by simp
also have "... = (ctxt_of_pos_term ?p l1 ⋅⇩c σ1)⟨r2 ⋅ σ2⟩" unfolding ctxt_of_pos_term_subst [OF p] ..
also have "... = (D ⋅⇩c σ1)⟨r2 ⋅ σ2⟩" unfolding D ..
finally have C2rσ: "C2⟨r2 ⋅ σ2⟩ = (D ⋅⇩c σ1)⟨r2 ⋅ σ2⟩" .
from C1 have C1rσ: "C1⟨r1 ⋅ σ1⟩ = r1 ⋅ σ1" by simp
show ?thesis unfolding C2rσ C1rσ unfolding μ1 μ2
proof (rule disjI2, intro exI, intro conjI)
show "r1 ⋅ μ1 ∘⇩s ρ = □⟨r1 ⋅ μ1 ⋅ ρ⟩" by simp
qed (insert in_cp, auto)
next
case False
from pos_into_subst [OF id _ False]
obtain q q' x where p: "?p = q <#> q'" and q: "q ∈ poss l1" and l1q: "l1 |_ q = Var x" by auto
have "l2 ⋅ σ2 = C2⟨l2 ⋅ σ2⟩ |_ q <#> q'" unfolding p [symmetric] by simp
also have "... = l1 ⋅ σ1 |_ q <#> q'" unfolding id ..
also have "... = l1 |_ q ⋅ σ1 |_ q'" using q by simp
also have "... = σ1 x |_ q'" unfolding l1q by simp
finally have l2x: "l2 ⋅ σ2 = σ1 x |_ q'" by simp
have pp: "?p ∈ poss (l1 ⋅ σ1)" unfolding id by simp
hence "q <#> q' ∈ poss (l1 ⋅ σ1)" unfolding p .
hence "q' ∈ poss (l1 ⋅ σ1 |_ q)" unfolding poss_append_poss ..
with q have "q' ∈ poss (l1 |_ q ⋅ σ1)" by auto
hence q'x: "q' ∈ poss (σ1 x)" unfolding l1q by simp
from ctxt_supt_id [OF q'x] obtain E where σ1x: "E⟨l2 ⋅ σ2⟩ = σ1 x"
and E: "E = ctxt_of_pos_term q' (σ1 x)"
unfolding l2x by blast
let ?e = "E⟨r2 ⋅ σ2⟩"
from hole_pos_ctxt_of_pos_term [OF q'x] E have q': "q' = hole_pos E" by simp
from σ1x have σ1x': "σ1 x = E⟨l2 ⋅ σ2⟩" by simp
let ?σ = "λ y. if y = x then ?e else σ1 y"
have one: "(r1 ⋅ σ1, r1 ⋅ ?σ) ∈ (rstep R)^*"
proof (rule subst_qrsteps_imp_qrsteps [where Q = "{}", unfolded qrstep_rstep_conv])
fix y
show "(σ1 y, ?σ y) ∈ (rstep R)^*"
proof (cases "y = x")
case False thus ?thesis by simp
next
case True
show ?thesis unfolding True σ1x' using lr2 by auto
qed
qed
show ?thesis
proof (rule disjI1, rule, unfold C1 ctxt_apply_term.simps, rule one)
show "(C2⟨r2 ⋅ σ2⟩, r1 ⋅ ?σ) ∈ ?R^*"
proof (rule rtrancl_trans)
show "(l1 ⋅ ?σ, r1 ⋅ ?σ) ∈ ?R^*" using lr1 by auto
next
from q have ql1: "q ∈ poss (l1 ⋅ σ1)" by simp
have "C2⟨r2 ⋅ σ2⟩ = replace_at (C2⟨l2 ⋅ σ2⟩) ?p (r2 ⋅ σ2)" by simp
also have "... = replace_at (l1 ⋅ σ1) ?p (r2 ⋅ σ2)" unfolding id ..
also have "... = replace_at (l1 ⋅ σ1) q ?e"
proof -
have "E = ctxt_of_pos_term q' (l1 ⋅ σ1 |_ q)"
unfolding subt_at_subst [OF q] l1q E by simp
thus ?thesis
unfolding p
unfolding ctxt_of_pos_term_append [OF ql1]
by simp
qed
finally have CR2: "C2⟨r2 ⋅ σ2⟩ = replace_at (l1 ⋅ σ1) q ?e" .
from q l1q have "(replace_at (l1 ⋅ σ1) q ?e, l1 ⋅ ?σ) ∈ ?R^*"
proof (induct l1 arbitrary: q)
case (Var y)
thus ?case by simp
next
case (Fun f ls)
from Fun(2, 3) obtain i p where q: "q = i <# p" and i: "i < length ls" and p: "p ∈ poss (ls ! i)" and px: "ls ! i |_ p = Var x" by (cases q, auto)
from i have "ls ! i ∈ set ls" by auto
from Fun(1) [OF this p px] have rec: "(replace_at (ls ! i ⋅ σ1) p ?e, ls ! i ⋅ ?σ) ∈ ?R^*" .
let ?lsσ = "map (λ t. t ⋅ σ1) ls"
let ?lsσ' = "map (λ t. t ⋅ ?σ) ls"
have id: "replace_at (Fun f ls ⋅ σ1) q ?e = Fun f (take i ?lsσ @ replace_at (ls ! i ⋅ σ1) p ?e # drop (Suc i) ?lsσ)" (is "_ = Fun f ?r")
unfolding q using i by simp
show ?case unfolding id unfolding subst_apply_term.simps
proof (rule all_ctxt_closedD [of UNIV])
fix j
assume j: "j < length ?r"
show "(?r ! j, ?lsσ' ! j) ∈ ?R^*"
proof (cases "j = i")
case True
show ?thesis using i True using rec by (auto simp: nth_append)
next
case False
have "?r ! j = ?lsσ ! j"
by (rule nth_append_take_drop_is_nth_conv, insert False i j, auto)
also have "... = ls ! j ⋅ σ1" using j i by auto
finally have idr: "?r ! j = ls ! j ⋅ σ1" .
from j i have idl: "?lsσ' ! j = ls ! j ⋅ ?σ" by auto
show ?thesis unfolding idr idl
proof (rule subst_qrsteps_imp_qrsteps [where Q = "{}", unfolded qrstep_rstep_conv])
fix y
show "(σ1 y, ?σ y) ∈ ?R^*"
proof (cases "y = x")
case False thus ?thesis by simp
next
case True thus ?thesis using σ1x' lr2 by auto
qed
qed
qed
qed (insert i, auto)
qed
thus "(C2⟨r2 ⋅ σ2⟩, l1 ⋅ ?σ) ∈ ?R^*" unfolding CR2 .
qed
qed
qed
next
case (More f1 bef1 D1 aft1) note C1 = this
show ?thesis
proof (cases C2)
case Hole note C2 = this
from id have id: "C2⟨l2 ⋅ σ2⟩ = C1⟨l1 ⋅ σ1⟩" by simp
from C1 C2 have "((C2, C1), C12) ∈ measures ?m" unfolding C12 by auto
from 1 [rule_format, OF this, unfolded split, rule_format, OF lr2 lr1 id]
show ?thesis
proof
assume "(C2⟨r2 ⋅ σ2⟩, C1⟨r1 ⋅ σ1⟩) ∈ join ?R"
thus ?thesis by auto
qed blast
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
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
have "((D1, D2), C12) ∈ measures ?m" unfolding C12 C1 C2
by auto
from 1 [rule_format, OF this, unfolded split, rule_format,
OF lr1 lr2 idD] have "?q (D1⟨r1 ⋅ σ1⟩) (D2⟨r2 ⋅ σ2⟩)" by auto
thus ?thesis
proof
assume "(D1⟨r1 ⋅ σ1⟩, D2⟨r2 ⋅ σ2⟩) ∈ join ?R"
then obtain s' where seq1: "(D1⟨r1 ⋅ σ1⟩, s') ∈ ?R^*"
and seq2: "(D2⟨r2 ⋅ σ2⟩, s') ∈ ?R^*" by auto
from rsteps_closed_ctxt [OF seq1, of ?C]
have seq1: "(C1⟨r1 ⋅ σ1⟩, ?C⟨s'⟩) ∈ ?R^*" using id1 by auto
from rsteps_closed_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 "∃ C b l r σ. D1⟨r1 ⋅ σ1⟩ = C⟨l ⋅ σ⟩ ∧ D2⟨r2 ⋅ σ2⟩ = C⟨r ⋅ σ⟩ ∧ ((b, l, r) ∈ ?CP ∨ (b, r, l) ∈ ?CP)"
then obtain C b l r σ where idD: "D1⟨r1 ⋅ σ1⟩ = C⟨l ⋅ σ⟩" "D2⟨r2 ⋅ σ2⟩ = C⟨r ⋅ σ⟩" and mem: "((b, l, r) ∈ ?CP ∨ (b, r, l) ∈ ?CP)" by blast
show ?thesis
by (rule disjI2, unfold id1 id2, rule exI [of _ "?C ∘⇩c C"], intro exI, rule conjI [OF _ conjI [OF _ mem]], insert idD, auto)
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 _ lr2, of "{}" True "r1 ⋅ σ1"]
have "(?one, replace_at ?one ?p2 (r2 ⋅ σ2)) ∈ rstep R" by auto
hence one: "(C1⟨r1 ⋅ σ1⟩, replace_at ?one ?p2 (r2 ⋅ σ2)) ∈ (rstep 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 _ lr1, of "{}" True "r2 ⋅ σ2"]
have "(?two, replace_at ?two ?p1 (r1 ⋅ σ1)) ∈ rstep R" by auto
hence two: "(C2⟨r2 ⋅ σ2⟩, replace_at ?two ?p1 (r1 ⋅ σ1)) ∈ (rstep 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 (rule disjI1, rule, rule one, unfold one_two, rule two)
qed
qed
qed
qed
qed
}
from this [of "(C1, C2)", unfolded split, rule_format, OF lr1 lr2 id]
show ?thesis unfolding t1 t2 by auto
qed
lemma critical_pairs:
fixes R :: "('f, string) trs"
assumes cp: "⋀ l r b. (b, l, r) ∈ critical_pairs R R ⟹ l ≠ r ⟹
∃ l' r' s. instance_rule (l, r) (l', r') ∧ (l', s) ∈ (rstep R)⇧* ∧ (r', s) ∈ (rstep R)⇧*"
shows "WCR (rstep R)"
proof
let ?R = "rstep R"
let ?CP = "critical_pairs R R"
fix s t1 t2
assume steps: "(s, t1) ∈ ?R" "(s, t2) ∈ ?R"
let ?p = "λ s'. (t1, s') ∈ ?R^* ∧ (t2, s') ∈ ?R^*"
from critical_pairs_main [OF steps]
have "∃ s'. ?p s'"
proof
assume "∃ C b l r σ. t1 = C⟨l ⋅ σ⟩ ∧ t2 = C⟨r ⋅ σ⟩ ∧ ((b, l, r) ∈ ?CP ∨ (b, r, l) ∈ ?CP)"
then obtain C b l r σ where id: "t1 = C⟨l ⋅ σ⟩" "t2 = C⟨r ⋅ σ⟩"
and mem: "(b, l, r) ∈ ?CP ∨ (b, r, l) ∈ ?CP" by blast
show ?thesis
proof (cases "l = r")
case True
thus ?thesis unfolding id by auto
next
case False
note sub_ctxt = rsteps_closed_ctxt [OF rsteps_closed_subst [OF rsteps_closed_subst]]
from mem show ?thesis
proof
assume mem: "(b, l, r) ∈ ?CP"
from cp [OF mem False] obtain l' r' s' τ where id2: "l = l' ⋅ τ" "r = r' ⋅ τ" and steps: "(l', s') ∈ ?R^*" "(r', s') ∈ ?R^*"
unfolding instance_rule_def by auto
show "∃ s'. ?p s'" unfolding id id2
by (rule exI [of _ "C⟨s' ⋅ τ ⋅ σ⟩"], rule conjI, rule sub_ctxt [OF steps(1)], rule sub_ctxt [OF steps(2)])
next
assume mem: "(b, r, l) ∈ ?CP"
from cp [OF mem] False obtain l' r' s' τ where id2: "r = l' ⋅ τ" "l = r' ⋅ τ" and steps: "(l', s') ∈ ?R^*" "(r', s') ∈ ?R^*"
unfolding instance_rule_def by auto
show "∃ s'. ?p s'" unfolding id id2
by (rule exI [of _ "C⟨s' ⋅ τ ⋅ σ⟩"], rule conjI, rule sub_ctxt [OF steps(2)], rule sub_ctxt [OF steps(1)])
qed
qed
qed auto
thus "(t1, t2) ∈ join ?R" by auto
qed
lemma critical_pairs_fork:
fixes R :: "('f, string) trs"
assumes cp: "(b, l, r) ∈ critical_pairs R R"
shows "(l, r) ∈ (rstep R)¯ O rstep R"
proof -
from cp [unfolded critical_pairs_def, simplified]
obtain σ1 σ2 l1 l2 r1 r2 C where id: "l = r1 ⋅ σ1" "r = (C ⋅⇩c σ1)⟨r2 ⋅ σ2⟩"
and r1: "(C⟨l1⟩, r1) ∈ R" and r2: "(l2, r2) ∈ R" and mgu: "mgu_var_disjoint_string l1 l2 = Some (σ1, σ2)" by blast
have one: "(l, C⟨l1⟩ ⋅ σ1) ∈ (rstep R)^-1" unfolding reverseTrs id
by (rule rstepI [of r1 "C⟨l1⟩" _ _ □ σ1], insert r1, auto)
from mgu_var_disjoint_generic_sound [OF mgu] have change: "C⟨l1⟩ ⋅ σ1 = (C ⋅⇩c σ1)⟨l2 ⋅ σ2⟩" by simp
have "(C⟨l1⟩ ⋅ σ1, r) ∈ rstep R" unfolding change id
by (rule rstepI [OF r2, of _ _ σ2], auto)
with one show ?thesis by auto
qed
lemma critical_pairs_complete:
fixes R :: "('f, string) trs"
assumes cp: "(b, l, r) ∈ critical_pairs R R"
and no_join: "(l, r) ∉ (rstep R)⇧↓"
shows "¬ WCR (rstep R)"
proof
from critical_pairs_fork [OF cp] obtain u where ul: "(u, l) ∈ rstep R" and ur: "(u, r) ∈ rstep R" by force
assume wcr: "WCR (rstep R)"
with ul ur no_join show False unfolding WCR_on_def by auto
qed
lemma critical_pair_lemma:
fixes R :: "('f, string) trs"
shows "WCR (rstep R) ⟷
(∀ (b, s, t) ∈ critical_pairs R R. (s, t) ∈ (rstep R)⇧↓)"
(is "?l = ?r")
proof
assume ?l
with critical_pairs_complete [where R = R] show ?r by auto
next
assume ?r
show ?l
proof (rule critical_pairs)
fix b s t
assume "(b, s, t) ∈ critical_pairs R R"
with ‹?r› have "(s, t) ∈ join (rstep R)" by auto
then obtain u where s: "(s, u) ∈ (rstep R)^*"
and t: "(t, u) ∈ (rstep R)^*" by auto
show "∃ s' t' u. instance_rule (s, t) (s', t') ∧ (s', u) ∈ (rstep R)^* ∧ (t', u) ∈ (rstep R)^*"
proof (intro exI conjI)
show "instance_rule (s, t) (s, t)" by simp
qed (insert s t, auto)
qed
qed
lemma critical_pairs_innermost_weak_diamond:
fixes R :: "('f, string) trs"
assumes cp: "⋀ l r. (True, l, r) ∈ critical_pairs 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, string) 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_var_disjoint_string_complete [OF ident]
obtain μ1 μ2 ρ where mgu: "mgu_var_disjoint_string l1 l2 = Some (μ1, μ2)" and
μ1: "σ1 = μ1 ∘⇩s ρ"
and μ2: "σ2 = μ2 ∘⇩s ρ"
by blast
have in_cp: "(True, r1 ⋅ μ1, r2 ⋅ μ2) ∈ critical_pairs 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
thus ?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"
hence 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
thus ?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" .
hence 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" .
hence 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 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]])
lemma critical_pairs_exI:
fixes σ :: "('f, string) subst"
assumes P: "(l, r) ∈ P" and R: "(l', r') ∈ R" and l: "l = C⟨l''⟩"
and l'': "is_Fun l''" and unif: "l'' ⋅ σ = l' ⋅ τ"
and b: "b = (C = □)"
shows "∃ s t. (b, s, t) ∈ critical_pairs P R"
proof -
from mgu_var_disjoint_string_complete [OF unif]
obtain μ1 μ2 where mgu: "mgu_var_disjoint_string l'' l' = Some (μ1, μ2)" by blast
show ?thesis
by (intro exI, rule critical_pairsI [OF P R l l'' mgu refl refl b])
qed
end