section ‹Implementation of the Weak Dependency Pair Processor›
theory WDP_Transformation_Impl
imports
WDP_Transformation
QTRS.QDP_Framework_Impl
begin
datatype ('f, 'v) wdp_trans_info = WDP_Trans_Info
"'f sig" -- ‹compound symbols›
"(('f, 'v) rule × ('f, 'v) rule) list" -- ‹strict rules and corresponding WDPs›
"(('f, 'v) rule × ('f, 'v) rule) list" -- ‹weak rules and corresponding WDPs›
"('f, 'v) term list" -- ‹new Q-component›
fun is_compound_context
where
"is_compound_context CComp C ⟷ ground_mctxt C ∧ funas_mctxt C ⊆ CComp"
context
fixes shp :: "'f ⇒ 'f::show"
begin
interpretation sharp_syntax .
definition
check_rule_wdp ::
"'f sig ⇒ ('f :: show, 'v :: show) rule × ('f, 'v) rule ⇒ shows check"
where
"check_rule_wdp CComp = (λ((l, r), (p, q)). do {
let l' = ♯ l;
check (l' = p) (''wrong lhs, expected '' +#+ shows l' +@+ '' but got '' +#+ shows p);
let us = uncap_till_funas (- CComp) r;
let (C, us') = split_term_funas (- CComp) q;
check (♯ us = us')
(shows ''lists of maximal subterms with defined root differ'');
check (is_compound_context CComp C)
(shows C +@+ '' is not a proper compound context of '' +#+ shows q)
} <+? (λe. ''could not ensure that '' +#+ shows_rule (p, q) +@+
'' is a valid weak dependency pair for '' +#+ shows_rule (l, r) +@+ shows_nl +@+ e))"
lemma check_rule_wdp:
assumes "isOK (check_rule_wdp C (r, p))"
shows "pre_wdps.is_WDP_of (♯ :: 'f ⇒ 'f) C p r"
proof -
interpret pre_wdps shp C .
from assms obtain l u p' q
where [simp]: "r = (l, u)" "p = (p', q)"
and [simp]: "p' = ♯ l" and *: "dmax q = ♯(dmax u)"
and "ground_mctxt (ccap q)" (is "ground_mctxt ?C")
and "funas_mctxt (ccap q) ⊆ C"
by (cases r p rule: prod.exhaust [case_product prod.exhaust]) (auto simp: check_rule_wdp_def)
then show ?thesis
by (auto simp: is_WDP_of_def intro!: exI [of _ "?C"]) (metis * split_term_eqf)
qed
definition
check_wdp_trans ::
"('tp, 'f :: show, 'v :: show) tp_ops ⇒ ('f, 'v) wdp_trans_info ⇒
('f, 'v) complexity_measure ⇒ complexity_class ⇒ 'tp ⇒
(('f, 'v) complexity_measure × 'tp) result"
where
"check_wdp_trans I info cm cc cp =
(case info of
WDP_Trans_Info Comp s_wdps w_wdps Q' ⇒
(case cm of
Runtime_Complexity C' D' ⇒ (do {
let S' = tp_ops.R I cp;
let W' = tp_ops.Rw I cp;
let S = map fst s_wdps;
let W = map fst w_wdps;
let R = S @ W;
let fs = funas_trs_list R;
let ds = defined_list R;
check_allm (λr. check (∃r' ∈ set S. r =⇩v r')
(shows ''could not find weak dependency pair for strict rule '' +@+ shows r)) S';
check_allm (λr. check (∃r' ∈ set W. r =⇩v r')
(shows ''could not find weak dependency pair for weak rule '' +@+ shows r)) W';
let WDP_S = map snd s_wdps;
let WDP_W = map snd w_wdps;
let shpf = (λ(f, n). (♯ f, n));
let F = fs @ C' @ D';
let f_sharps = map shpf F;
let Fs = ♯ (set F);
let CComp = (set fs - set (defined_list R) - set D') ∪ Comp;
check_allm (λq. check (is_Fun q ∧ the (root q) ∉ set F)
(shows ''new Q-term '' +@+ shows q +@+ shows '' not allowed'')) Q';
check_wf_trs R;
check_allm (λf. check (f ∉ CComp) (shows f +@+ shows '' clashes with sharp symbols'')) f_sharps;
check_allm (λf. check (f ∉ CComp) (shows f +@+ shows '' clashes with defined symbols of RC'')) D';
check_allm (λf. check (f ∉ CComp) (shows f +@+ shows '' clashes with defined symbols'')) ds;
check_allm (check_rule_wdp CComp) s_wdps;
check_allm (check_rule_wdp CComp) w_wdps;
return (Runtime_Complexity C' (map shpf D'),
tp_ops.mk I (tp_ops.nfs I cp) (tp_ops.Q I cp @ Q') (WDP_S @ S) (WDP_W @ W))
})
| Derivational_Complexity _ ⇒
error (shows ''only runtime complexity supported for weak dependency pairs'')))
<+? (λe. shows ''error when switching to weak dependency pairs'' +@+ shows_nl +@+ e)"
lemma wdp_trans:
assumes "tp_spec I"
and res: "check_wdp_trans I info cm cc tp = return (cm', 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 -
obtain Comp and s_wdps and w_wdps and Q'
where info: "info = WDP_Trans_Info Comp s_wdps w_wdps Q'" by (cases info) auto
note res = res [unfolded check_wdp_trans_def info]
interpret tp_spec I by fact
from res obtain C' D' where cm: "cm = Runtime_Complexity C' D'" by (cases cm) (simp, blast)
let ?S' = "set (R tp)"
let ?W' = "set (Rw tp)"
let ?S = "fst ` set s_wdps"
let ?W = "fst ` set w_wdps"
let ?R = "?S ∪ ?W"
let ?nfs = "NFS tp"
let ?D = "Collect (defined ?R)"
let ?shp = "λ(f, n). (shp f, n)"
let ?Ds = "?shp ` ?D ∪ ?D"
let ?D'' = "map ?shp D'"
let ?Q = "set (Q tp)"
let ?Q' = "?Q ∪ set Q'"
let ?WDP_S = "snd ` set s_wdps"
let ?WDP_W = "snd ` set w_wdps"
let ?F = "funas_trs ?R ∪ set C' ∪ set D'"
let ?Fs = "?shp ` ?F"
let ?C = "funas_trs ?R - ?D - set D'"
let ?Cs = "?C ∪ Comp"
let ?NF = "NF_terms ((fst ∘ fst) ` set s_wdps ∪ (fst ∘ fst) ` set w_wdps)"
note res = res[unfolded cm Let_def, simplified]
have wf: "wf_trs ?R" and
D': "set D' ∩ ?Cs = {}" and
C_fresh: "(?D ∪ ?Fs) ∩ ?Cs = {}" and
tp': "tp' = mk ?nfs (Q tp @ Q') (map snd s_wdps @ map fst s_wdps) (map snd w_wdps @ map fst w_wdps)" and
cm': "cm' = Runtime_Complexity C' ?D''" and
S: "(∀x∈ ?S'. ∃ lr ∈ ?S. x =⇩v lr)" and
W: "(∀x∈ ?W'. ∃ lr ∈ ?W. x =⇩v lr)" and
check_S: "(∀x∈set s_wdps. isOK (check_rule_wdp ?Cs x))" and
check_W: "(∀x∈set w_wdps. isOK (check_rule_wdp ?Cs x))"
using res by (auto simp: cm Let_def)
interpret wdps ?Cs shp ?F ?R ?Q ?Q'
by (unfold_locales) (force, rule C_fresh, rule wf, insert res, force)
interpret sharp_syntax .
have cpx: "deriv_bound_measure_class
(relto (qrstep ?nfs ?Q' (?WDP_S ∪ ?S)) (qrstep ?nfs ?Q' (?WDP_W ∪ ?W)))
(Runtime_Complexity C' ?D'') cc" using cpx by (simp add: cm' tp')
have subset: "?S ⊆ ?R" "?W ⊆ ?R" by auto
have "set C' ∪ set D' ⊆ ?F" "set ?D'' = ♯(set D')" by force+
note wdps = WDPs_sound [of ?S ?WDP_S ?W ?WDP_W ?nfs C' ?D'' cc D', OF _ _ subset cpx D' this]
show ?thesis
unfolding qreltrs_sound split cm
proof (rule deriv_bound_measure_class_mono [OF relto_mono subset_refl subset_refl wdps])
show "qrstep ?nfs ?Q ?S' ⊆ qrstep ?nfs ?Q ?S"
by (rule qrstep_rename_vars, insert S, force)
next
show "qrstep ?nfs ?Q ?W' ⊆ qrstep ?nfs ?Q ?W"
by (rule qrstep_rename_vars, insert W, force)
next
{ fix r
assume "r ∈ ?S"
with S obtain p where *: "(r, p) ∈ set s_wdps" by auto
then have "p ∈ ?WDP_S" by force
with check_rule_wdp [OF check_S [rule_format, OF *]]
have "∃p ∈ ?WDP_S. is_WDP_of p r" by blast }
then show "∀r ∈ ?S. ∃p ∈ ?WDP_S. is_WDP_of p r" by auto
next
{ fix r
assume "r ∈ ?W"
with W obtain p where *: "(r, p) ∈ set w_wdps" by auto
then have "p ∈ ?WDP_W" by force
with check_rule_wdp [OF check_W [rule_format, OF *]]
have "∃p ∈ ?WDP_W. is_WDP_of p r" by blast }
then show "∀r ∈ ?W. ∃p ∈ ?WDP_W. is_WDP_of p r" by auto
qed
qed
end
end