Theory CR.Critical_Pairs_Impl
theory Critical_Pairs_Impl
imports
TRS.Critical_Pairs_Innermost
Check_Joins
TRS.Q_Restricted_Rewriting_Impl
Show.Shows_Literal
begin
context fixes
ren :: "'v :: infinite renaming2"
begin
definition critical_pairs_impl :: "('f,'v)rules ⇒ ('f,'v)rules ⇒ (bool × ('f,'v)rule)list"
where "critical_pairs_impl P R ≡ concat (map (λ (l,r). concat (map (λ p. let C = ctxt_of_pos_term p l; l'' = l |_ p; b = (C = □) in
if is_Var l'' then [] else concat (map (λ (l',r'). case mgu_vd ren l'' l' of Some (σ,τ) ⇒ [(b, (C ⋅⇩c σ)⟨r' ⋅ τ⟩, r ⋅ σ)] | None ⇒ []) R)) (poss_list l))) P)"
lemma critical_pairs_impl[simp]: "set (critical_pairs_impl P R) = critical_pairs ren (set P) (set R)" (is "?l = ?r")
proof -
note cpdefs = critical_pairs_impl_def critical_pairs_def set_concat
set_map Let_def poss_list_sound
{
fix b s t
assume "(b,s,t) ∈ ?r"
from this[unfolded cpdefs]
obtain l r l' r' l'' C σ τ where
b: "b = (C = □)" and t: "t = r ⋅ σ" and s: "s = (C ⋅⇩c σ)⟨r' ⋅ τ⟩"
and P: "(l,r) ∈ set P" and R: "(l', r') ∈ set R"
and l: "l = C⟨l''⟩" and l'': "is_Fun l''"
and mgu: "mgu_vd ren l'' l' = Some (σ, τ)"
by auto
let ?p = "hole_pos C"
from l have p: "?p ∈ poss l" by auto
from l p have C: "C = ctxt_of_pos_term ?p l" by auto
from l p have l: "l |_ ?p = l''" by auto
have "(b,s,t) ∈ ?l" unfolding cpdefs b s t
by (rule, rule, rule P, unfold cpdefs, rule, rule imageI[OF p],
insert C l R l'' mgu, force)
}
then have "?r ⊆ ?l" by auto
moreover
{
fix b s t
assume "(b,s,t) ∈ ?l"
from this[unfolded cpdefs]
obtain l r p l' r' σ τ where
P: "(l,r) ∈ set P" and p: "p ∈ poss l" and lp: "is_Fun (l |_ p)"
and R: "(l',r') ∈ set R" and mgu: "Some (σ,τ) = mgu_vd ren (l |_ p) l'" and b: "b = (ctxt_of_pos_term p l = □)" and t: "t = r ⋅ σ" and s: "s = (ctxt_of_pos_term p l ⋅⇩c σ)⟨r' ⋅ τ⟩" by force
have "(b,s,t) ∈ ?r"
by (rule critical_pairsI[OF P R _ lp mgu[symmetric] t s b], insert ctxt_supt_id[OF p], simp)
}
then have "?l ⊆ ?r" by auto
ultimately show ?thesis by auto
qed
definition critical_pairs_top_impl :: "('f,'v)rules ⇒ ('f,'v)rules ⇒ (('f,'v)rule)list"
where "critical_pairs_top_impl P R ≡ concat (map (λ (l,r).
if is_Var l then [] else concat (map (λ (l',r'). case mgu_vd ren l l' of Some (σ,τ) ⇒ [(r' ⋅ τ, r ⋅ σ)] | None ⇒ []) R)) P)"
lemma critical_pairs_top_impl[simp]: "set (critical_pairs_top_impl P R) = {(s,t). (True,s,t) ∈ critical_pairs ren (set P) (set R)}" (is "?l = ?r")
proof -
note cpdefs = critical_pairs_top_impl_def critical_pairs_def set_concat
set_map
{
fix s t
assume "(s,t) ∈ ?r"
from this[unfolded cpdefs]
obtain l r l' r' l'' C σ τ where
C: "C = □" and t: "t = r ⋅ σ" and s: "s = (C ⋅⇩c σ)⟨r' ⋅ τ⟩"
and P: "(l,r) ∈ set P" and R: "(l', r') ∈ set R"
and l: "l = C⟨l''⟩" and l'': "is_Fun l''"
and mgu: "mgu_vd ren l'' l' = Some (σ, τ)"
by auto
have "(s,t) ∈ ?l" unfolding cpdefs s t
by (rule, rule, rule P, insert l[unfolded C] l'' mgu[symmetric] R C, force)
}
then have "?r ⊆ ?l" by auto
moreover
{
fix s t
assume st: "(s,t) ∈ ?l"
have id: "⋀ p b t e. p ∈ set (if b then t else e) = (b ∧ p ∈ set t ∨ ¬ b ∧ p ∈ set e)" by auto
from st[unfolded cpdefs]
obtain l r l' r' σ τ where
P: "(l,r) ∈ set P" and lp: "is_Fun l"
and R: "(l',r') ∈ set R" and mgu: "Some (σ,τ) = mgu_vd ren l l'" and t: "t = r ⋅ σ" and s: "s = r' ⋅ τ" by (auto simp: id)
have "(s,t) ∈ ?r" unfolding s t
by (rule, unfold split, rule critical_pairsI[OF P R _ lp mgu[symmetric] refl, of □], auto)
}
then have "?l ⊆ ?r" by auto
ultimately show ?thesis by auto
qed
end
definition showsl_crit_pair :: "('f :: showl,'w :: showl)rule ⇒ showsl"
where "showsl_crit_pair lr ≡
showsl_lit (STR ''('') ∘ showsl (fst lr) ∘ showsl_lit (STR '', '') ∘
showsl (snd lr) ∘ showsl_lit (STR '')'')"
definition check_critical_pairs_cp_info :: "('f :: showl,'v :: showl)rules ⇒ (bool × ('f,'v)rule) list ⇒ ('f, 'v) cp_join_hints ⇒ showsl check"
where "check_critical_pairs_cp_info R cp hints ≡ do {
checker ← is_rsteps_join_one R hints;
check_allm (λ (b,st). checker st) cp
}"
definition check_critical_pairs_NF :: "('f :: showl,'v :: showl)rules ⇒ (bool × ('f,'v)rule) list ⇒ showsl check"
where "check_critical_pairs_NF R cp ≡ do {
check_allm (λ (_,s,t).
if (s = t) then succeed else
check_join_NF R s t
<+? (λ e. showsl_lit (STR ''problem when joining critical pair '') ∘ showsl_crit_pair (s,t) ∘ showsl_nl ∘ e)
) cp
}"