theory Reduction_Pair_Impl
imports
"Check-NT.Reduction_Pair"
"Check-NT.Term_Order_Impl"
QTRS.QDP_Framework_Impl
QTRS.Map_Choice
"Check-NT.Q_Restricted_Rewriting_Impl"
"../Termination_and_Complexity/Usable_Replacement_Map_Impl"
begin
definition
mono_redpair_proc ::
"('dpp, 'f, 'v) dpp_ops ⇒ ('f::show, 'v::show) redtriple ⇒
('f, 'v) rules ⇒ ('f, 'v) rules ⇒ 'dpp proc"
where
"mono_redpair_proc I rp Premove Rremove dpp = check_return (do {
let (ps,pns) = dpp_ops.split_pairs I dpp Premove;
let (rs,rns) = dpp_ops.split_rules I dpp Rremove;
redtriple.valid rp;
redtriple.mono rp (ps @ rs @ pns @ rns)
<+? (λs. ''problem with monotonicity of strict order'' +#+ shows_nl +@+ s);
check_allm (redtriple.ns rp) rns
<+? (λs. ''problem when orienting TRS'' +#+ shows_nl +@+ s);
check_allm (redtriple.s rp) rs
<+? (λs. ''problem when orienting TRS'' +#+ shows_nl +@+ s);
check_allm (redtriple.ns rp) pns
<+? (λs. ''problem when orienting DPs'' +#+ shows_nl +@+ s);
check_allm (redtriple.s rp) ps
<+? (λs. ''problem when orienting DPs'' +#+ shows_nl +@+ s)
} <+? (λs. ''could not apply the reduction pair processor with the following'' +#+ shows_nl +@+
(redtriple.desc rp) +@+ shows_nl +@+ s))
(dpp_spec.delete_pairs_rules I dpp Premove Rremove)"
definition
mono_urm_redpair_proc ::
"('dpp, 'f, string) dpp_ops ⇒ ('f::{key,show}, string) redtriple ⇒
('f, string) rules ⇒ ('f, string) rules ⇒ 'dpp proc"
where
"mono_urm_redpair_proc I rp Premove Rremove dpp = check_return (do {
let (ps,pns) = dpp_ops.split_pairs I dpp Premove;
let (rs,rns) = dpp_ops.split_rules I dpp Rremove;
let r = dpp_ops.rules I dpp;
let q = dpp_ops.Q I dpp;
let p = dpp_ops.pairs I dpp;
check_wf_trs p;
check_wf_trs r;
check (dpp_ops.NFQ_subset_NF_rules I dpp) (shows ''innermost required'');
let (fs,μ,info) = get_innermost_strict_repl_map_dpp I dpp rs;
redtriple.valid rp;
let μ' = redtriple.mono_af rp;
(check_allm (λ f. check (μ f ⊆ μ' f)
(''error in monotonicity: strict order for '' +#+ shows f
+@+ '' ensures monotonicity in positions '' +#+ show_position_set f (μ' f)
+@+ ''⏎but usable replacement map is '' +#+ show_position_set f (μ f))) fs) <+?
(λ s. s +@+ ''⏎the computed usable replacement map ('' +#+ info +#+ '') is⏎'' +#+
shows_sep (λ f. shows ''mu('' +@+ shows f +@+ shows '') = '' +@+ show_position_set f (μ f)) shows_nl fs
+@+ shows ''⏎and mu(f) = {} for all other symbols f'');
check_allm (redtriple.ns rp) rns
<+? (λs. ''problem when orienting TRS'' +#+ shows_nl +@+ s);
check_allm (redtriple.s rp) rs
<+? (λs. ''problem when orienting TRS'' +#+ shows_nl +@+ s);
check_allm (redtriple.ns rp) pns
<+? (λs. ''problem when orienting DPs'' +#+ shows_nl +@+ s);
check_allm (redtriple.s rp) ps
<+? (λs. ''problem when orienting DPs'' +#+ shows_nl +@+ s)
} <+? (λs. ''could not apply the reduction pair processor with usable repl. maps and the following'' +#+ shows_nl +@+
(redtriple.desc rp) +@+ shows_nl +@+ s))
(dpp_spec.delete_pairs_rules I dpp Premove Rremove)"
definition
rule_removal_tt ::
"('tp, 'f, 'v) tp_ops ⇒ ('f::show, 'v::show) redtriple ⇒
('f, 'v) rules ⇒ 'tp proc"
where
"rule_removal_tt I rp Rremove trs = check_return (do {
let (rs,rns) = tp_ops.split_rules I trs Rremove;
redtriple.valid rp;
redtriple.mono rp (rs @ rns)
<+? (λs. ''problem with monotonicity of strict order'' +#+ shows_nl +@+ s);
check_allm (redtriple.ns rp) rns
<+? (λs. ''problem when orienting TRS'' +#+ shows_nl +@+ s);
check_allm (redtriple.s rp) rs
<+? (λs. ''problem when orienting TRS'' +#+ shows_nl +@+ s)
} <+? (λs. ''could not apply the reduction pair processor with the following'' +#+ shows_nl +@+
(redtriple.desc rp) +@+ shows_nl +@+ s))
(tp_spec.delete_rules I trs Rremove)"
definition
rule_shift_complexity_tt ::
"('tp, 'f, 'v) tp_ops ⇒ ('f::{show,key}, 'v::{show,key}) redtriple ⇒ ('f,'v)rules ⇒
('f,'v)complexity_measure ⇒ complexity_class ⇒ 'tp proc"
where
"rule_shift_complexity_tt I rp Rdelete cm cc tp ≡ let
R = tp_ops.R I tp;
Rw = tp_ops.Rw I tp;
R2 = ceta_list_diff R Rdelete in
check_return (do {
redtriple.valid rp;
redtriple.mono rp (Rdelete @ Rw @ R2)
<+? (λs. ''problem with monotonicity of strict order'' +#+ shows_nl +@+ s);
check_allm (redtriple.s rp) Rdelete
<+? (λs. ''problem when orienting strict TRS'' +#+ shows_nl +@+ s);
check_allm (redtriple.ns rp) (Rw @ R2)
<+? (λs. ''problem when orienting non-strict TRS'' +#+ shows_nl +@+ s);
redtriple.cpx rp cm cc
<+? (λs. shows ''problem when ensuring complexity of order⏎'' o s)
} <+? (λs. ''could not derive the intended complexity '' +#+ shows cc +@+ shows '' from the following'' +@+ shows_nl +@+
(redtriple.desc rp) +@+ shows_nl +@+ s))
(tp_ops.mk I (tp_ops.nfs I tp) (tp_ops.Q I tp) R2 (list_union Rw Rdelete))"
context dpp_spec
begin
lemma mono_redpair_proc:
assumes grp: "generic_redtriple_impl grp"
shows "sound_proc_impl (mono_redpair_proc I (grp rp) ps rs)"
proof
fix d d'
assume fin: "finite_dpp (dpp d')"
and ok: "mono_redpair_proc I (grp rp) ps rs d = return d'"
let ?rp = "grp rp"
let ?Ps = "set ps"
let ?Rs = "set rs"
let ?P = "set (P d)"
let ?Pw = "set (Pw d)"
let ?Q = "set (Q d)"
let ?R = "set (R d)"
let ?Rw = "set (Rw d)"
let ?nfs = "NFS d"
let ?m = "M d"
interpret generic_redtriple_impl grp by (rule grp)
obtain Ps Pr where p: "split_pairs d ps = (Ps,Pr)" by force
from split_pairs_sound[OF this] have Ps: "set Ps = (?P ∪ ?Pw) ∩ ?Ps"
and Pr: "set Pr = (?P ∪ ?Pw) - ?Ps" by auto
obtain Rs Rr where r: "split_rules d rs = (Rs,Rr)" by force
from split_rules_sound[OF this] have Rs: "set Rs = (?R ∪ ?Rw) ∩ ?Rs"
and Rr: "set Rr = (?R ∪ ?Rw) - ?Rs" by auto
note ok = ok[unfolded mono_redpair_proc_def, simplified, simplified p r split]
from ok have valid: "isOK(redtriple.valid ?rp)"
and mono: "isOK(redtriple.mono ?rp ((Ps @ Rs) @ (Pr @ Rr) @ []))"
and NS: "isOK (check_allm (redtriple.ns ?rp) (Pr @ Rr))"
and S: "isOK(check_allm (redtriple.s ?rp) (Ps @ Rs))"
and d': "d' = delete_pairs_rules d ps rs" by auto
from generate_redtriple[OF valid S NS, of Nil] mono
obtain S NS NST where S: "(?P ∪ ?Pw) ∩ ?Ps ⊆ S" "(?R ∪ ?Rw) ∩ ?Rs ⊆ S" and
NS: "?P ∪ ?Pw - ?Ps ⊆ NS" "?R ∪ ?Rw - ?Rs ⊆ NS"
and "mono_ce_af_redtriple_order S NS NST (redtriple.af ?rp)"
and mono: "ctxt.closed S" by (auto simp: Pr Ps Rr Rs)
have proc: "Reduction_Pair.mono_redpair_proc S NS ?Ps ?Rs (?nfs,?m,?P,?Pw,?Q,?R,?Rw) (?nfs,?m,?P-?Ps,?Pw-?Ps,?Q,?R-?Rs,?Rw-?Rs)" using NS S mono by auto
interpret mono_ce_af_redtriple_order S NS NST "redtriple.af ?rp" by fact
note fin = fin[unfolded d' delete_simps]
show "finite_dpp (dpp d)" unfolding d' dpp_sound
by (rule subset_proc[OF fin proc mono_redpair_proc_subset])
qed
end
lemma mono_urm_redpair_proc:
assumes "generic_redtriple_impl grp"
and I: "dpp_spec I"
shows "dpp_spec.sound_proc_impl I (mono_urm_redpair_proc I (grp rp) ps rs)"
proof -
interpret dpp_spec I by fact
show ?thesis
proof
fix d d'
assume fin: "finite_dpp (dpp d')"
and ok: "mono_urm_redpair_proc I (grp rp) ps rs d = return d'"
let ?rp = "grp rp"
let ?Ps = "set ps"
let ?Rs = "set rs"
let ?P = "set (P d)"
let ?Pw = "set (Pw d)"
let ?Q = "set (Q d)"
let ?R = "set (R d)"
let ?Rw = "set (Rw d)"
let ?nfs = "NFS d"
let ?m = "M d"
interpret generic_redtriple_impl grp by fact
obtain Ps Pr where p: "split_pairs d ps = (Ps,Pr)" by force
from split_pairs_sound[OF this] have Ps: "set Ps = (?P ∪ ?Pw) ∩ ?Ps"
and Pr: "set Pr = (?P ∪ ?Pw) - ?Ps" by auto
obtain Rs Rr where r: "split_rules d rs = (Rs,Rr)" by force
from split_rules_sound[OF this] have Rs: "set Rs = (?R ∪ ?Rw) ∩ ?Rs"
and Rr: "set Rr = (?R ∪ ?Rw) - ?Rs" and Rs_sub: "set Rs ⊆ ?R ∪ ?Rw" by auto
let ?urm = "get_innermost_strict_repl_map_dpp I d Rs"
obtain fs μ info where urm: "?urm = (fs,μ,info)" by (cases ?urm, auto)
let ?μ = "redtriple.mono_af ?rp"
let ?cpx = "λ cm cc. isOK(redtriple.cpx ?rp cm cc)"
let ?af = "redtriple.af ?rp"
note ok = ok[unfolded mono_urm_redpair_proc_def, simplified, simplified p r split urm]
from ok have valid: "isOK(redtriple.valid ?rp)"
and NS: "isOK (check_allm (redtriple.ns ?rp) (Pr @ Rr))"
and S: "isOK(check_allm (redtriple.s ?rp) (Ps @ Rs))"
and inn: "NF_terms ?Q ⊆ NF_trs (?R ∪ ?Rw)"
and wfR: "wf_trs (?R ∪ ?Rw)"
and wfP: "wf_trs (?P ∪ ?Pw)"
and d': "d' = delete_pairs_rules d ps rs" by auto
from generate_redtriple[OF valid S NS, of Nil]
obtain S NS NST where S: "set Ps ⊆ S" "set Rs ⊆ S"
and NS: "set Pr ∪ set Rr ⊆ NS"
and cpx: "cpx_ce_af_redtriple_order S NS NST ?af ?μ ?cpx"
by (auto simp: Pr Ps Rr Rs)
have NSR: "?R ∪ ?Rw - set Rs ⊆ NS" using NS unfolding Rr Rs by auto
have NSP: "?P ∪ ?Pw ⊆ NS ∪ S" using NS S(1) unfolding Pr Ps by auto
interpret cpx_ce_af_redtriple_order S NS NST ?af ?μ ?cpx by fact
note urm = get_innermost_strict_repl_map_dpp[OF I, of d, unfolded dpp_spec_sound,
OF inn wfP wf_trs_imp_wwf_qtrs[OF wfR] Rs_sub urm]
have μ': "af_subset μ ?μ" using urm ok unfolding af_subset_def by auto
{
fix s t σ
assume st: "(s, t) ∈ ?P ∪ ?Pw"
and sQ: "s ⋅ σ ∈ NF_terms ?Q"
from Rs_sub have id: "set Rs ∩ (?R ∪ ?Rw) = set Rs" by auto
from urm(2)[OF st sQ] have "usable_replacement_map μ {t ⋅ σ} ?nfs (?R ∪ ?Rw) ?Q (set Rs)" .
hence "usable_replacement_map μ {t ⋅ σ} ?nfs (?R ∪ ?Rw) ?Q (set Rs ∩ (?R ∪ ?Rw))" unfolding id .
} note urm = this
note main = urm_mono_redpair_sound[of ?R ?Rw "set Rs" ?P ?Pw "set Ps" ?Q μ ?nfs ?μ ?m,
OF NSR NSP S inn urm μ' μ]
let ?d = "(NFS d, M d, set (P d) - set Ps, set (Pw d) - set Ps, set (Q d), set (R d) - set Rs, set (Rw d) - set Rs)"
from d' Rs Rr Ps Pr have d': "dpp d' = ?d" by auto
show "finite_dpp (dpp d)" unfolding finite_dpp_def
proof (rule, elim exE)
fix s t σ
assume "min_ichain (dpp d) s t σ"
from main[OF _ _ this[unfolded dpp_sound]]
have "∃ j. min_ichain ?d (shift s j) (shift t j) (shift σ j)" .
with fin[unfolded d'] show False unfolding finite_dpp_def by blast
qed
qed
qed
context tp_spec
begin
lemma rule_removal_tt:
assumes grp: "generic_redtriple_impl grp"
shows "sound_tt_impl (rule_removal_tt I (grp rp) rs)"
proof
fix trs trs'
assume fin: "SN_qrel (qreltrs trs')"
and ok: "rule_removal_tt I (grp rp) rs trs = return trs'"
let ?rp = "grp rp"
let ?Rs = "set rs"
let ?Q = "set (Q trs)"
let ?R = "set (R trs)"
let ?Rw = "set (Rw trs)"
let ?nfs = "NFS trs"
interpret generic_redtriple_impl grp by (rule grp)
show "SN_qrel (qreltrs trs)"
proof (cases "split_rules trs rs")
case (Pair Rs Rr)
from split_rules_sound[OF this] have Rs: "set Rs = (?R ∪ ?Rw) ∩ ?Rs"
and Rr: "set Rr = (?R ∪ ?Rw) - ?Rs" by auto
note ok = ok[unfolded rule_removal_tt_def,simplified, simplified Pair]
from ok have valid: "isOK (redtriple.valid ?rp)"
and mono: "isOK(redtriple.mono ?rp (Rs @ Rr @ []))"
and NS: "isOK (check_allm (redtriple.ns ?rp) Rr)"
and S: "isOK(check_allm (redtriple.s ?rp) Rs)"
and trs': "trs' = delete_rules trs rs" by auto
from generate_redtriple[OF valid S NS, of Nil] mono
obtain S NS NST where S: "(?R ∪ ?Rw) ∩ ?Rs ⊆ S"
and NS: "?R ∪ ?Rw - ?Rs ⊆ NS" and "mono_ce_af_redtriple_order S NS NST (redtriple.af ?rp)"
and mono: "ctxt.closed S" by (auto simp: Rr Rs)
have proc: "mono_redpair_tt S NS ?Rs (?nfs,?Q,?R,?Rw) (?nfs,?Q,?R-?Rs,?Rw-?Rs)" using NS S mono by auto
interpret mono_ce_af_redtriple_order S NS NST "redtriple.af ?rp" by fact
note fin = fin[unfolded trs' delete_R_Rw_sound]
show ?thesis unfolding trs' qreltrs_sound
by (rule rel_tt[OF mono_redpair_tt _ fin], rule proc)
qed
qed
end
lemma rule_shift_complexity_tt:
assumes "tp_spec I"
and grp: "generic_redtriple_impl grp"
and res: "rule_shift_complexity_tt I (grp rp) Rdelete cm cc tp = return tp'"
and cpx: "deriv_bound_measure_class (rel_qrstep (tp_ops.qreltrs I tp')) cm cc"
shows "deriv_bound_measure_class (rel_qrstep (tp_ops.qreltrs I tp)) cm cc"
proof -
interpret tp_spec I by fact
interpret generic_redtriple_impl grp by (rule grp)
note res = res[unfolded rule_shift_complexity_tt_def Let_def, simplified]
let ?rp = "grp rp"
let ?R = "set (R tp)"
let ?Rw = "set (Rw tp)"
let ?D = "ceta_list_diff (R tp) Rdelete"
let ?RwD = "Rw tp @ ?D"
let ?nfs = "NFS tp"
let ?Q = "qrstep ?nfs (set (Q tp))"
from res have valid: "isOK (redtriple.valid ?rp)"
and mono: "isOK(redtriple.mono ?rp (Rdelete @ ?RwD @ []))"
and S: "isOK(check_allm (redtriple.s ?rp) Rdelete)"
and NS: "isOK(check_allm (redtriple.ns ?rp) ?RwD)"
by auto
let ?cpx = "redtriple.cpx (grp rp) cm"
let ?Cpx = "λ cm cc. isOK(redtriple.cpx (grp rp) cm cc)"
from res have tp': "tp' = mk ?nfs (Q tp) ?D (list_union (Rw tp) Rdelete)" by simp
from cpx[unfolded tp', simplified]
have bound: "deriv_bound_measure_class (relto (?Q (?R - set Rdelete)) (?Q (?Rw ∪ set Rdelete))) cm cc" .
from res have cpx: "isOK(?cpx cc)" by auto
from generate_redtriple[OF valid S NS, of Nil] mono
obtain S NS NST where "cpx_ce_af_redtriple_order S NS NST (redtriple.af ?rp) (redtriple.mono_af ?rp) ?Cpx"
and S: "set Rdelete ⊆ S" and NS: "?Rw ∪ set ?D ⊆ NS" and
"mono_ce_af_redtriple_order S NS NST (redtriple.af ?rp)" and mono: "ctxt.closed S"
by auto
interpret cpx_ce_af_redtriple_order S NS NST "redtriple.af ?rp" "(redtriple.mono_af ?rp)" ?Cpx by fact
from rule_shift_complexity[OF mono S NS cpx, of cc ?nfs "set (Q tp)"] bound
have bound: "deriv_bound_measure_class (relto (?Q (set Rdelete ∪ set ?D)) (?Q ?Rw)) cm cc" by simp
have bound: "deriv_bound_measure_class (relto (?Q ?R) (?Q ?Rw)) cm cc"
by (rule deriv_bound_measure_class_mono[OF relto_mono[OF qrstep_mono[OF _ subset_refl] subset_refl] subset_refl subset_refl bound], auto)
thus ?thesis by simp
qed
end