theory Generic_Reduction_Pair_Processor_Impl
imports
Generic_Usable_Rules_Impl
"Check-NT.Innermost_Usable_Rules_Impl"
"../Orderings/Reduction_Pair_Impl"
Generic_Reduction_Pair_Processor
begin
definition
generic_ur_af_redtriple_proc ::
"('dpp, 'f, string) dpp_ops ⇒ ('f::{show,key}, string) redtriple ⇒
('f,string)rules option ⇒ ('f,string)rules ⇒ 'dpp proc"
where
"generic_ur_af_redtriple_proc I rp U_opt Premove dpp = check_return (do {
redtriple.valid rp;
let (ps, pns) = dpp_ops.split_pairs I dpp Premove;
let P = dpp_ops.pairs I dpp;
U ← smart_usable_rules_checker_impl I dpp (redtriple.af rp) U_opt P;
check_allm (redtriple.ns rp) U
<+? (λs. ''problem when orienting (usable) rules'' +#+ shows_nl +@+ s);
check_allm (redtriple.nst 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 generic reduction pair processor with the following'' +#+ shows_nl +@+
(redtriple.desc rp) +@+ shows_nl +@+ s))
(dpp_spec.delete_pairs I dpp Premove)"
lemma generic_ur_af_redtriple_proc:
assumes I: "dpp_spec I"
and grp: "generic_redtriple_impl grp"
shows "dpp_spec.sound_proc_impl I (generic_ur_af_redtriple_proc I (grp rp) U_opt ps)"
proof -
interpret dpp_spec I by fact
interpret generic_redtriple_impl grp by fact
show ?thesis
proof
fix d d'
assume fin: "finite_dpp (dpp d')"
and ok: "generic_ur_af_redtriple_proc I (grp rp) U_opt ps d = return d'"
let ?rp = "grp rp"
let ?S = "set ps"
let ?P = "set (P d)"
let ?Pw = "set (Pw d)"
let ?Pb = "set (pairs d)"
let ?PP = "?P ∪ ?Pw"
let ?Q = "set (Q d)"
let ?R = "set (R d)"
let ?Rw = "set (Rw d)"
let ?Rb = "set (rules d)"
let ?RR = "set (R d @ Rw d)"
let ?nfs = "NFS d"
let ?m = "M d"
let ?wwf = "wwf_qtrs ?Q ?Rb"
have RR_conv: "?RR = ?Rb" unfolding dpp_spec_sound by auto
have PP_conv: "?PP = ?Pb" unfolding dpp_spec_sound by auto
show "finite_dpp (dpp d)"
proof (cases "split_pairs d ps")
case (Pair Ps Pr)
from split_pairs_sound[OF this] have Ps: "set Ps = (?P ∪ ?Pw) ∩ ?S"
and Pr: "set Pr = (?P ∪ ?Pw) - ?S" by auto
let ?pi = "redtriple.af ?rp"
let ?cpx = "λ cm cc. isOK(redtriple.cpx ?rp cm cc)"
let ?urcheck = "smart_usable_rules_checker_impl I d ?pi U_opt (pairs d)"
note ok = ok[unfolded generic_ur_af_redtriple_proc_def Let_def Pair, simplified]
from ok have valid: "isOK(redtriple.valid ?rp)"
and compat: "isOK(?urcheck)" by auto
from compat obtain U where urc: "?urcheck = return U" by (cases ?urcheck, auto)
note ok = ok[unfolded urc]
from ok have
NS: "isOK (check_allm (redtriple.ns ?rp) U)"
and NST: "isOK (check_allm (redtriple.nst ?rp) Pr)"
and S: "isOK(check_allm (redtriple.s ?rp) Ps)"
and d': "d' = delete_pairs d ps" by auto
from generate_redtriple[OF valid S NS NST, unfolded Ps]
obtain S NS NST where "cpx_ce_af_redtriple_order S NS NST (redtriple.af ?rp) (redtriple.mono_af ?rp) ?cpx"
and S: "(?P ∪ ?Pw) ∩ ?S ⊆ S" and NS: "?P ∪ ?Pw - ?S ⊆ NST" and R: "set U ⊆ NS" by (auto simp: Pr)
hence NS: "?P ∪ ?Pw ⊆ NST ∪ S" by auto
from smart_usable_rules_checker_impl[OF I urc] have ur: "smart_usable_rules_checker ?nfs ?m ?wwf ?pi ?Q (rules d) U_opt ?PP = Some U" by auto
interpret cpx_ce_af_redtriple_order S NS NST ?pi "(redtriple.mono_af ?rp)" ?cpx by fact
have ce: "ce_af_redtriple S NS NST ?pi" ..
note proc = generic_redtriple_proc[OF smart_usable_rules_checker R NS ce, OF ur]
have *: "⋀P Q. (P ⟹ Q) ⟹ ¬ Q ⟹ ¬ P" by blast
show ?thesis
unfolding finite_dpp_def
proof(rule, elim exE)
fix s t σ
assume min: "min_ichain (dpp d) s t σ"
have "∃ i. min_ichain (?nfs,?m,?P - ?S,?Pw - ?S,?Q,?R,?Rw) (shift s i) (shift t i) (shift σ i)"
by (rule min_ichain_split[OF min[unfolded dpp_sound], of ?S "{}", unfolded Int_empty_left Diff_empty],
rule * [OF _ proc[of s t σ, unfolded dpp_spec_sound]], rule min_ichain_mono[of ?nfs ?m "?S ∩ ?PP" "?PP - ?S" ?Q "{}" "?R ∪ ?Rw"], insert S, auto
)
with fin[unfolded d' delete_P_Pw_sound finite_dpp_def] show False by blast
qed
qed
qed
qed
definition root_aft_to_entry where
"root_aft_to_entry s t π ≡ let rt = the (root t); πt = π rt; ts = args t
in map (λ i. (s, ts ! i)) (filter (λ i. i ∈ πt) [0 ..< snd rt])"
definition
generic_ur_af_root_redtriple_proc ::
"('dpp, 'f, string) dpp_ops ⇒ ('f::{show,key}, string) root_redtriple ⇒
('f,string)rules option ⇒ ('f,string)rules ⇒ 'dpp proc"
where
"generic_ur_af_root_redtriple_proc I rp U_opt Premove dpp = check_return (do {
root_redtriple.valid rp;
let (ps, pns) = dpp_ops.split_pairs I dpp Premove;
let P = dpp_ops.pairs I dpp;
let pi = root_redtriple.af rp;
let pi' = root_redtriple.aft rp;
let is_def = dpp_spec.is_defined I dpp;
check_allm (λ(l, r). do {
check_no_var l;
check_no_var r;
check_no_defined_root is_def r
}) P;
check_allm (λ(l, r). do {
check_no_var l
}) (dpp_ops.rules I dpp);
U ← smart_usable_rules_checker_impl I dpp pi U_opt (concat (map (λ (s,t). root_aft_to_entry s t pi') P));
check_allm (root_redtriple.ns rp) U
<+? (λs. ''problem when orienting (usable) rules'' +#+ shows_nl +@+ s);
check_allm (root_redtriple.nst rp) pns
<+? (λs. ''problem when orienting DPs'' +#+ shows_nl +@+ s);
check_allm (root_redtriple.s rp) ps
<+? (λs. ''problem when orienting DPs'' +#+ shows_nl +@+ s)
} <+? (λs. ''could not apply the generic root reduction pair processor with the following'' +#+ shows_nl +@+
(root_redtriple.desc rp) +@+ shows_nl +@+ s))
(dpp_spec.delete_pairs I dpp Premove)"
lemma generic_ur_af_root_redtriple_proc:
assumes I: "dpp_spec I"
and grp: "generic_root_redtriple_impl grp"
shows "dpp_spec.sound_proc_impl I (generic_ur_af_root_redtriple_proc I (grp rp) U_opt ps)"
proof -
interpret dpp_spec I by fact
interpret generic_root_redtriple_impl grp by fact
show ?thesis
proof
fix d d'
assume fin: "finite_dpp (dpp d')"
and ok: "generic_ur_af_root_redtriple_proc I (grp rp) U_opt ps d = return d'"
let ?rp = "grp rp"
let ?S = "set ps"
let ?P = "set (P d)"
let ?Pw = "set (Pw d)"
let ?Pb = "set (pairs d)"
let ?PP = "?P ∪ ?Pw"
let ?Q = "set (Q d)"
let ?R = "set (R d)"
let ?Rw = "set (Rw d)"
let ?Rb = "set (rules d)"
let ?RR = "set (R d @ Rw d)"
let ?nfs = "NFS d"
let ?m = "M d"
let ?wwf = "wwf_qtrs ?Q ?Rb"
have RR_conv: "?RR = ?Rb" unfolding dpp_spec_sound by auto
have PP_conv: "?PP = ?Pb" unfolding dpp_spec_sound by auto
show "finite_dpp (dpp d)"
proof (cases "split_pairs d ps")
case (Pair Ps Pr)
from split_pairs_sound[OF this] have Ps: "set Ps = (?P ∪ ?Pw) ∩ ?S"
and Pr: "set Pr = (?P ∪ ?Pw) - ?S" by auto
let ?pi = "root_redtriple.af ?rp"
let ?pi' = "root_redtriple.aft ?rp"
let ?P' = "concat (map (λ (s,t). root_aft_to_entry s t ?pi') (pairs d))"
let ?R = "rules d"
let ?urcheck = "smart_usable_rules_checker_impl I d ?pi U_opt ?P'"
note ok = ok[unfolded generic_ur_af_root_redtriple_proc_def Let_def Pair, simplified]
from ok have valid: "isOK(root_redtriple.valid ?rp)"
and compat: "isOK(?urcheck)" by auto
from compat obtain U where urc: "?urcheck = return U" by (cases ?urcheck, auto)
note ok = ok[unfolded urc]
from ok have
NS: "isOK (check_allm (root_redtriple.ns ?rp) U)"
and NST: "isOK (check_allm (root_redtriple.nst ?rp) Pr)"
and S: "isOK(check_allm (root_redtriple.s ?rp) Ps)"
and d': "d' = delete_pairs d ps"
and Pcond: "⋀ s t. (s,t) ∈ ?P ∪ ?Pw ⟹ is_Fun s ∧ is_Fun t"
and Rcond: "⋀ l r. (l,r) ∈ ?Rb ⟹ is_Fun l"
and ndef: "∀ (s,t) ∈ ?P ∪ ?Pw. ¬ defined (set ?R) (the (root t))" by auto
from generate_root_redtriple[OF valid S NS NST, unfolded Ps]
obtain S NS NST where "ce_af_root_redtriple_order S NS NST ?pi ?pi'"
and S: "(?P ∪ ?Pw) ∩ ?S ⊆ S" and NS: "?P ∪ ?Pw - ?S ⊆ NST" and R: "set U ⊆ NS" by (auto simp: Pr)
hence NS: "?P ∪ ?Pw ⊆ NST ∪ S" by auto
from smart_usable_rules_checker_impl[OF I urc] have ur: "smart_usable_rules_checker ?nfs ?m ?wwf ?pi ?Q (rules d) U_opt (set ?P') = Some U" by auto
interpret ce_af_root_redtriple_order S NS NST ?pi ?pi' by fact
have ce: "ce_af_root_redtriple S NS NST ?pi ?pi'" ..
note proc = root_redtriple_sound[OF smart_usable_rules_checker _ R NS Pcond Rcond ndef ce, of ?nfs ?m ?Q U_opt]
let ?PP = "?P ∪ ?Pw"
have no_chain: "⋀ s t σ. ¬ min_ichain (?nfs,?m,S ∩ ?PP, ?PP - S, ?Q, {}, set ?R) s t σ"
proof (rule proc, unfold ur[symmetric], rule arg_cong[where f = "smart_usable_rules_checker ?nfs ?m ?wwf ?pi ?Q (rules d) U_opt"])
show "{u. ∃ s f ts i. u = (s, ts ! i) ∧ (s,Fun f ts) ∈ ?P ∪ ?Pw ∧ i < length ts ∧ i ∈ ?pi' (f,length ts)} = set ?P'"
(is "?one = ?two")
proof -
{
fix s f ts i
assume "(s,Fun f ts) ∈ ?P ∪ ?Pw ∧ i < length ts ∧ i ∈ ?pi' (f,length ts)"
hence "(s, ts ! i) ∈ ?two" unfolding root_aft_to_entry_def Let_def unfolding pairs_sound[symmetric] by force
}
hence one: "?one ⊆ ?two" by blast
{
fix s ti
assume "(s,ti) ∈ ?two"
then obtain s' t' where st': "(s',t') ∈ set (pairs d)"
and mem: "(s,ti) ∈ set (root_aft_to_entry s' t' ?pi')" by auto
from Pcond[of s' t'] st' obtain f ts where t': "t' = Fun f ts" by (cases t', auto)
from mem[unfolded t' root_aft_to_entry_def Let_def, simplified]
obtain i where ti: "ti = ts ! i" and i: "i < length ts" and pi: "i ∈ ?pi' (f,length ts)" and s: "s = s'"
by auto
have "(s,ti) ∈ ?one" unfolding ti s
by (rule, intro exI conjI, rule refl, insert st' pi i t', auto)
}
hence two: "?two ⊆ ?one" ..
from one two show ?thesis by blast
qed
qed
have *: "⋀P Q. (P ⟹ Q) ⟹ ¬ Q ⟹ ¬ P" by blast
show ?thesis
unfolding finite_dpp_def
proof(rule, elim exE)
fix s t σ
assume min: "min_ichain (dpp d) s t σ"
have "∃ i. min_ichain (?nfs,?m,?P - ?S,?Pw - ?S,?Q,set (R d),set (Rw d)) (shift s i) (shift t i) (shift σ i)"
by (rule min_ichain_split[OF min[unfolded dpp_sound], of ?S "{}", unfolded Int_empty_left Diff_empty],
rule * [OF _ no_chain[of s t σ]], rule min_ichain_mono[of ?nfs ?m "?S ∩ ?PP" "?PP - ?S" ?Q "{}" "set ?R"],
insert S, auto)
with fin[unfolded d' delete_P_Pw_sound finite_dpp_def] show False by blast
qed
qed
qed
qed
definition
generic_mono_ur_redpair_proc ::
"('dpp, 'f, string) dpp_ops ⇒ ('f::{key,show}, string) redtriple ⇒
('f,string)rules ⇒ ('f,string)rules ⇒ ('f,string)rules ⇒ 'dpp proc"
where
"generic_mono_ur_redpair_proc I rp Premove Rremove ur dpp =
(if dpp_ops.NFQ_subset_NF_rules I dpp then
mono_inn_usable_rules_ce_proc I rp Premove Rremove ur dpp
else (do {
check (dpp_ops.minimal I dpp) (shows ''minimality or innermost required for mon. red. pair proc. with usable rules'');
mono_ur_redpair_proc I rp Premove Rremove ur dpp
}))"
lemma generic_mono_ur_redpair_proc:
assumes I: "dpp_spec I"
and grp: "generic_redtriple_impl grp"
shows "dpp_spec.sound_proc_impl I (generic_mono_ur_redpair_proc I (grp rp) ps rs ur)"
proof -
interpret dpp_spec I by fact
show ?thesis
proof
fix d d'
assume fin: "finite_dpp (dpp d')"
and ok: "generic_mono_ur_redpair_proc I (grp rp) ps rs ur d = return d'"
note ok = ok[unfolded generic_mono_ur_redpair_proc_def]
show "finite_dpp (dpp d)"
proof (cases "NFQ_subset_NF_rules d")
case False
with ok have "mono_ur_redpair_proc I (grp rp) ps rs ur d = return d'"
by auto
with mono_ur_redpair_proc[OF grp, of rp ps rs ur] fin show ?thesis
unfolding sound_proc_impl_def by auto
next
case True
with ok have "mono_inn_usable_rules_ce_proc I (grp rp) ps rs ur d = return d'" by auto
with mono_inn_usable_rules_ce_proc[OF I grp, of rp ps rs ur] fin show ?thesis
unfolding sound_proc_impl_def by auto
qed
qed
qed
end