theory AC_Reduction_Pair_Processor_Impl
imports
AC_Reduction_Pair_Processor
"Check-NT.AC_Dependency_Pair_Problem_Spec"
"../Framework/AC_Termination_Problem_Spec"
"Check-NT.Term_Order_Impl"
Usable_Rules_Impl
"../AC_Rewriting/AC_Rewriting_Impl"
begin
definition
ac_mono_ur_redpair_proc ::
"('dpp, 'f, 'v) ac_dpp_ops ⇒ ('f::show, 'v::show) redtriple ⇒
('f,'v)rules ⇒ ('f,'v)rules ⇒ ('f,'v)rules ⇒ 'dpp proc"
where
"ac_mono_ur_redpair_proc I rp P_remove R_remove ur dpp = check_return (do {
let P = ac_dpp_ops.pairs I dpp;
let R = ac_dpp_ops.rules I dpp;
let E = ac_dpp_ops.E I dpp;
let Premove = set P_remove;
let Rremove = set R_remove;
let us = ⋃ set (map (funas_term o snd) (P @ ur));
let filt = (λ lr. (∀ f ∈ funas_term (fst lr). f ∈ us));
let (ps, pns) = partition (λ lr. lr ∈ Premove ∧ filt lr) P;
let (urs, urns) = partition (λ lr. lr ∈ Rremove ∧ filt lr) ur;
let rm = ac_dpp_ops.eq_rules_map I dpp;
redtriple.valid rp;
redtriple.mono rp (ps @ urs @ urns @ pns);
check_symmetric_AC_theory E
<+? (λ s. shows ''usable rules demand symmetric AC theory⏎'' o s);
check_allm (λ (l,r). check (is_Fun l) (shows ''variables as lhss not allowed''))
(ac_dpp_ops.R I dpp @ ac_dpp_ops.Rw I dpp);
check_ur_P_closed_rm_af rm ur full_af P;
check_allm (redtriple.ns rp) urns
<+? (λs. shows ''problem when orienting usable rules⏎'' o s);
check_allm (redtriple.s rp) urs
<+? (λs. shows ''problem when orienting usable rules⏎'' o s);
check_allm (redtriple.ns rp) pns
<+? (λs. shows ''problem when orienting DPs⏎'' o s);
check_allm (redtriple.s rp) ps
<+? (λs. shows ''problem when orienting DPs⏎'' o s)
} <+? (λs. shows ''could not apply the monotonic AC reduction pair processor with usable rules and the following⏎''
o redtriple.desc rp o shows_nl o s))
(ac_dpp_ops.delete_pairs_rules I dpp P_remove R_remove)"
lemma (in ac_dpp_spec) ac_mono_ur_redpair_proc:
assumes grp: "generic_redtriple_impl grp"
shows "sound_proc_impl (ac_mono_ur_redpair_proc I (grp rp) ps rs ur)"
proof
fix d d'
assume fin: "finite_rel_dpp (ac_dpp d')"
and ok: "ac_mono_ur_redpair_proc I (grp rp) ps rs ur d = return d'"
let ?rp = "grp rp"
let ?P = "set (P d)"
let ?Pw = "set (Pw d)"
let ?PP = "?P ∪ ?Pw"
let ?R = "set (R d)"
let ?Rw = "set (Rw d)"
interpret generic_redtriple_impl grp by (rule grp)
obtain us where us: "us = ⋃ ( set (map (funas_term o snd) (ac_dpp_ops.pairs I d @ ur)))" by auto
let ?filt = "λ lr. (∀ f ∈ funas_term (fst lr). f ∈ us)"
let ?filtP = "λ lr. lr ∈ set ps ∧ ?filt lr"
let ?filtR = "λ lr. lr ∈ set rs ∧ ?filt lr"
obtain Ps Pns where p: "partition ?filtP (pairs d) = (Ps,Pns)" by force
obtain Rs Rns where r: "partition ?filtR ur = (Rs,Rns)" by force
note ok = ok[unfolded ac_mono_ur_redpair_proc_def Let_def us[symmetric] p split r, simplified]
let ?π = "full_af"
let ?all = "Ps @ Rs @ Rns @ Pns"
from ok have valid: "isOK(redtriple.valid ?rp)"
and mono: "isOK(redtriple.mono ?rp ?all)"
and compat: "isOK(check_ur_P_closed_rm_af (ac_dpp_ops.eq_rules_map I d) ur ?π (ac_dpp_ops.pairs I d))"
and NS: "isOK (check_allm (redtriple.ns ?rp) (Rns @ Pns))"
and S: "isOK(check_allm (redtriple.s ?rp) (Ps @ Rs))"
and var: "(∀(l, r)∈set (R d) ∪ (set (Rw d)). is_Fun l)"
and AC: "AC_theory (set (E d))"
and sym: "symmetric_trs (set (E d))"
and d': "d' = ac_dpp_ops.delete_pairs_rules I d ps rs"
by auto
let ?E = "set (E d)"
let ?RE = "?R ∪ ?Rw ∪ ?E"
have id: "?PP = set (pairs d)" "?RE = set (R d @ Rw d @ E d)" by auto
have ur_cl: "ur_closed_af ?RE (set ur) us ?π ∧
ur_P_closed_af ?RE (set ur) us ?π ?PP " (is "?ur1 ∧ ?ur2")
unfolding us id
by (rule check_ur_P_closed_rm_af_sound[OF _ _ compat], insert var AC_theory.no_left_var[OF AC], force+)
hence ?ur1 and ?ur2 by auto
from generate_redtriple[OF valid S NS, of Nil] mono
obtain S NS NST where "mono_ce_af_redtriple_order S NS NST (redtriple.af ?rp)" and S: "set Ps ∪ set Rs ⊆ S"
and NS: "set Rns ∪ set Pns ⊆ NS" and mono: "ctxt.closed S"
by auto
then interpret old: mono_ce_af_redtriple_order S NS NST "redtriple.af ?rp" by simp
have redt: "mono_ce_af_redtriple S NS NST full_af"
by (unfold_locales, rule full_af)
from partition_filter1[of ?filtP "pairs d", unfolded p] S
have ps: "set ps ∩ ?PP - {lr |lr. ¬ funas_term (fst lr) ⊆ us} ⊆ S" by auto
from partition_filter1[of ?filtR ur, unfolded r] S
have rs: "set rs ∩ set ur - {lr |lr. ¬ funas_term (fst lr) ⊆ us} ⊆ S" by auto
from S NS have ur: "set ur ⊆ NS ∪ S" using partition_set[OF r] by auto
from S NS have p: "?PP ⊆ NS ∪ S" using partition_set[OF p] by auto
note fin = fin[unfolded d' delete_pairs_rules_sound]
have finR: "finite (?R ∪ ?Rw)" by auto
show "finite_rel_dpp (ac_dpp d)" unfolding ac_dpp_sound
by (rule ac_redtriple_mono_proc[OF finR sym AC ur p ps rs mono redt ‹?ur1› ‹?ur2› refl fin])
qed
definition
ac_ur_redpair_proc ::
"('dpp, 'f, 'v) ac_dpp_ops ⇒ ('f::show, 'v::show) redtriple ⇒
('f,'v)rules ⇒ ('f,'v)rules ⇒ 'dpp proc"
where
"ac_ur_redpair_proc I rp P_remove ur dpp = check_return (do {
let P = ac_dpp_ops.pairs I dpp;
let R = ac_dpp_ops.rules I dpp;
let E = ac_dpp_ops.E I dpp;
let Premove = set P_remove;
let (ps, pns) = partition (λ lr. lr ∈ Premove) P;
let rm = ac_dpp_ops.eq_rules_map I dpp;
let pi = redtriple.af rp;
redtriple.valid rp;
check_symmetric_AC_theory E
<+? (λ s. shows ''usable rules demand symmetric AC theory⏎'' o s);
check_allm (λ (l,r). check (is_Fun l) (shows ''variables as lhss not allowed''))
(ac_dpp_ops.R I dpp @ ac_dpp_ops.Rw I dpp);
check_ur_P_closed_rm_af rm ur pi P;
check_allm (redtriple.ns rp) ur
<+? (λs. shows ''problem when orienting usable rules⏎'' o s);
check_allm (redtriple.nst rp) pns
<+? (λs. shows ''problem when orienting DPs⏎'' o s);
check_allm (redtriple.s rp) ps
<+? (λs. shows ''problem when orienting DPs⏎'' o s)
} <+? (λs. shows ''could not apply the AC reduction pair processor with usable rules and the following⏎''
o redtriple.desc rp o shows_nl o s))
(ac_dpp_ops.delete_pairs_rules I dpp P_remove [])"
lemma (in ac_dpp_spec) ac_ur_redpair_proc:
assumes grp: "generic_redtriple_impl grp"
shows "sound_proc_impl (ac_ur_redpair_proc I (grp rp) ps ur)"
proof
fix d d'
assume fin: "finite_rel_dpp (ac_dpp d')"
and ok: "ac_ur_redpair_proc I (grp rp) ps ur d = return d'"
let ?rp = "grp rp"
let ?P = "set (P d)"
let ?Pw = "set (Pw d)"
let ?PP = "?P ∪ ?Pw"
let ?R = "set (R d)"
let ?Rw = "set (Rw d)"
interpret generic_redtriple_impl grp by (rule grp)
obtain Ps Pns where p: "partition (λ lr. lr ∈ set ps) (pairs d) = (Ps,Pns)" by force
note ok = ok[unfolded ac_ur_redpair_proc_def Let_def p split, simplified]
let ?π = "redtriple.af (grp rp)"
from ok have valid: "isOK(redtriple.valid ?rp)"
and compat: "isOK(check_ur_P_closed_rm_af (ac_dpp_ops.eq_rules_map I d) ur ?π (ac_dpp_ops.pairs I d))"
and NS: "isOK (check_allm (redtriple.ns ?rp) ur)"
and NST: "isOK (check_allm (redtriple.nst ?rp) Pns)"
and S: "isOK(check_allm (redtriple.s ?rp) Ps)"
and var: "(∀(l, r)∈set (R d) ∪ (set (Rw d)). is_Fun l)"
and AC: "AC_theory (set (E d))"
and sym: "symmetric_trs (set (E d))"
and d': "d' = ac_dpp_ops.delete_pairs_rules I d ps []"
by auto
let ?E = "set (E d)"
let ?RE = "?R ∪ ?Rw ∪ ?E"
have id: "?PP = set (pairs d)" "?RE = set (R d @ Rw d @ E d)" by auto
def us ≡ "⋃ ( set (map (funas_term o snd) (ac_dpp_ops.pairs I d @ ur)))"
have ur_cl: "ur_closed_af ?RE (set ur) us ?π ∧
ur_P_closed_af ?RE (set ur) us ?π ?PP " (is "?ur1 ∧ ?ur2")
unfolding us_def id
by (rule check_ur_P_closed_rm_af_sound[OF _ _ compat], insert var AC_theory.no_left_var[OF AC], force+)
hence ?ur1 and ?ur2 by auto
from generate_redtriple[OF valid S NS NST]
obtain S NS NST mono cpx where "cpx_ce_af_redtriple_order S NS NST ?π mono cpx" and S: "set Ps ⊆ S"
and NS: "set ur ⊆ NS" and NST: "set Pns ⊆ NST"
by auto
then interpret cpx_ce_af_redtriple_order S NS NST ?π mono cpx by simp
from S NST have NST: "?PP ⊆ NST ∪ S" using partition_set[OF p] by auto
from S have S: "set ps ∩ ?PP ⊆ S" using partition_filter1[of "λ lr. lr ∈ set ps" "pairs d", unfolded p]
by auto
have redt: "ce_af_redtriple S NS NST ?π" ..
note fin = fin[unfolded d' delete_pairs_rules_sound, simplified]
have finR: "finite (?R ∪ ?Rw)" by auto
show "finite_rel_dpp (ac_dpp d)" unfolding ac_dpp_sound
by (rule ac_redtriple_proc[OF finR sym AC NS NST S redt ‹?ur1› ‹?ur2› refl fin])
qed
definition
ac_rule_removal ::
"('tp, 'f, 'v) ac_tp_ops ⇒ ('f::show, 'v::show) redtriple ⇒
('f,'v)rules ⇒ 'tp ⇒ 'tp result"
where
"ac_rule_removal I rp R_remove tp = check_return (do {
let R = ac_tp_ops.R I tp;
let E = ac_tp_ops.E I tp;
let Rremove = set R_remove;
let rns = filter (λ lr. lr ∉ Rremove) R;
redtriple.valid rp;
redtriple.mono rp (R_remove @ rns @ E);
check_allm (redtriple.ns rp) rns
<+? (λs. shows ''problem when orienting weak rules⏎'' o s);
check_allm (redtriple.ns rp) E
<+? (λs. shows ''problem when orienting equations⏎'' o s);
check_allm (redtriple.s rp) R_remove
<+? (λs. shows ''problem when orienting strict rules⏎'' o s)
} <+? (λs. shows ''could not apply AC rule removal with the following⏎''
o redtriple.desc rp o shows_nl o s))
(ac_tp_ops.delete_rules I tp R_remove)"
lemma (in ac_tp_spec) ac_rule_removal:
assumes grp: "generic_redtriple_impl grp"
and rr: "ac_rule_removal I (grp rp) rs tp = return tp'"
and SN_tp': "SN (relation_ac_tp (ac_tp_ops.ac_tp I tp'))"
shows "SN (relation_ac_tp (ac_tp_ops.ac_tp I tp))"
proof -
let ?rp = "grp rp"
let ?A = "set (A tp)"
let ?C = "set (C tp)"
let ?R = "set (R tp)"
let ?E = "set (E tp)"
let ?Rns = "filter (λ lr. lr ∉ set rs) (R tp)"
interpret aoc_rewriting ?A ?C .
interpret generic_redtriple_impl grp by (rule grp)
note rr = rr[unfolded ac_rule_removal_def Let_def split, simplified]
let ?π = "redtriple.af (grp rp)"
from rr have valid: "isOK(redtriple.valid ?rp)"
and NS: "isOK (check_allm (redtriple.ns ?rp) (?Rns @ E tp))"
and S: "isOK(check_allm (redtriple.s ?rp) rs)"
and NST: "isOK(check_allm (redtriple.nst ?rp) [])"
and tp': "tp' = ac_tp_ops.delete_rules I tp rs"
and mono: "isOK (redtriple.mono ?rp (rs @ ?Rns @ E tp))"
by auto
have tp': "ac_tp tp' = (?R - set rs, ?A, ?C)" unfolding tp' delete_rules_sound ..
from generate_redtriple[OF valid S NS NST] mono
obtain S NS NST where "mono_ce_af_redtriple_order S NS NST ?π" and S: "set rs ⊆ S"
and NS: "set ?Rns ∪ ?E ⊆ NS" and mono: "ctxt.closed S"
by auto
from S NS have RE: "?R ∪ ?E ⊆ NS ∪ S" by auto
interpret mono_ce_af_redtriple_order S NS NST ?π by fact
show ?thesis unfolding SN_relation_ac_tp
by (rule ac_rule_removal[OF RE S _ mono], insert SN_tp'[unfolded tp'], auto simp: relaoc_def SN_rel_defs)
qed
end