theory DT_Transformation_Impl
imports
DT_Transformation
QTRS.Termination_Problem_Spec
QTRS.Map_Choice
QTRS.QDP_Framework_Impl
"HOL-Library.Permutation"
"Check-NT.Q_Restricted_Rewriting_Impl"
begin
datatype ('f, 'v) dt_transformation_info = DT_Transformation_Info
"(('f, 'v) rule × ('f, 'v) rule) list" -- ‹map strict rules to DTs›
"(('f, 'v) rule × ('f, 'v) rule) list" -- ‹map weak rules to DTs›
"(('f, 'v) term list)" -- ‹new Q-components›
context
fixes shp :: "'f ⇒ 'f"
begin
interpretation sharp_syntax .
fun DPos_impl :: "('f × nat) set ⇒ ('f, 'v) term ⇒ (pos × ('f, 'v) term) list"
where
"DPos_impl D (Var x) = []" |
"DPos_impl D (Fun f ts) =
(let n = length ts in
(if (f, n) ∈ D then Cons (ε, Fun (♯ f) ts) else id)
(concat (map (λ (i, ti). map (λ (p, t).
(PCons i p, t)) (DPos_impl D ti)) (zip [0 ..< n] ts))))"
end
lemma (in pre_innermost_wf) DPos_Fun:
"DPos (Fun f ss) =
(if (f,length ss) ∈ D then insert ε else id)
{PCons i p | i p. i < length ss ∧ p ∈ DPos (ss ! i)}" (is "?l = ?r")
proof -
note d = DPos_def
let ?n = "length ss"
{
fix p
assume p: "p ∈ ?l"
from this[unfolded d] obtain g where p: "p ∈ poss (Fun f ss)" and g: "g ∈ D"
and root: "root (Fun f ss |_ p) = Some g" by auto
hence "p ∈ ?r"
proof (cases p)
case Empty
from root[unfolded Empty] have "g = (f,?n)" by auto
with g show "p ∈ ?r" unfolding Empty by auto
next
case (PCons i q)
with p have i: "i < ?n" and q: "q ∈ poss (ss ! i)" by auto
with root g PCons have "q ∈ DPos (ss ! i)" unfolding d by auto
with i show "p ∈ ?r" unfolding PCons by auto
qed
}
moreover
{
fix p
assume p: "p ∈ ?r"
have "p ∈ ?l"
proof (cases p)
case Empty
with p have "(f,?n) ∈ D" by (auto split: if_splits)
thus "p ∈ ?l" unfolding d Empty by auto
next
case (PCons i q)
with p have i: "i < ?n" and q: "q ∈ DPos (ss ! i)" by (auto split: if_splits)
from q[unfolded d] obtain g where q: "q ∈ poss (ss ! i)"
and g: "g∈D" and root: "root (ss ! i |_ q) = Some g" by auto
show "p ∈ ?l" unfolding d using root q i g PCons by auto
qed
}
ultimately show ?thesis by blast
qed
lemma (in pre_innermost_wf) DPos_impl:
"set (DPos_impl shp D s) = { (p, sharp_term shp (s |_ p)) | p. p ∈ DPos s}"
proof (induct s)
case (Var x)
thus ?case by (auto simp: DPos_def)
next
interpret sharp_syntax .
case (Fun f ss)
let ?n = "length ss"
{
fix i
assume "i < ?n"
hence "ss ! i ∈ set ss" by auto
note Fun[OF this]
} note IH = this
let ?l = "concat (map (λ(i, ti). map (λ(p, y). (i <# p, y)) (DPos_impl ♯ D ti))
(zip [0..<?n] ss))"
let ?r = "{i <# p |i p. i < ?n ∧ p ∈ DPos (ss ! i)}"
let ?f = "(if (f,?n) ∈ D then insert (ε, Fun (♯ f) ss) else id)"
have "set ((if (f,?n) ∈ D then op # (ε, Fun (♯ f) ss) else id)
?l) = ?f (set ?l)" by auto
also have "… = ?f {(p, ♯ (Fun f ss |_ p)) | p. p ∈ ?r}"
proof (rule arg_cong[where f = ?f])
show "set ?l = {(p, ♯ (Fun f ss |_ p)) | p. p ∈ ?r}"
by (force simp: set_zip IH)
qed
also have "… = {(p, ♯ (Fun f ss |_ p)) |p. p ∈ (if (f,?n) ∈ D then insert ε else id) ?r}"
by auto
finally show ?case unfolding DPos_Fun DPos_impl.simps Let_def by auto
qed
fun check_tup :: "'f set ⇒ ('f, 'v) term ⇒ bool"
where
"check_tup T (Var x) ⟷ False" |
"check_tup T (Fun f ts) ⟷ f ∈ T"
context
fixes shp :: "'f ⇒ 'f::show"
begin
interpretation sharp_syntax .
definition
check_rule_dt ::
"'f sig ⇒ 'f set ⇒ ('f :: show, 'v :: show) rule × ('f, 'v) rule ⇒ shows check"
where
"check_rule_dt D Ds = (λ((l, r), (dl, dr)). do {
let sl = ♯ l;
check (sl = dl) (''wrong lhs, expected '' +#+ shows sl +@+ '' but got '' +#+ shows dl);
let pts = DPos_impl ♯ D r;
let spts = map snd pts;
let (C, dts) = split_term (check_tup Ds) dr;
check (mset dts = mset spts)
(shows ''multiset of subterms with defined roots differs'')
} <+? (λ e. ''could not ensure that '' +#+ shows_rule (dl, dr) +@+
'' is a valid dependency tuple for '' +#+ shows_rule (l, r) +@+ shows_nl +@+ e))"
lemma check_rule_dt:
assumes ok: "isOK (check_rule_dt D Ds (lr, dt))"
shows "pre_DT_trans.is_DT_of (♯ :: 'f ⇒ 'f) D lr dt"
proof -
interpret pre_DT_trans ♯ D undefined undefined undefined undefined .
obtain l r where lr: "lr = (l, r)" by force
obtain dl dr where dt: "dt = (dl, dr)" by force
obtain C dts where sg: "split_term (check_tup Ds) dr = (C, dts)" by force
from split_term_eqf [of dr "check_tup Ds"] and sg
have dr: "dr =⇩f (C, dts)" by (simp)
note ok = ok [unfolded lr dt check_rule_dt_def sg split, simplified]
let ?ps = "map fst (DPos_impl ♯ D r)"
let ?dts = "map snd (DPos_impl ♯ D r)"
from ok have id: "mset dts = mset ?dts" by auto
from mset_eq_length [OF id] have len: "length dts = length (DPos_impl ♯ D r)" by simp
from id [unfolded mset_eq_perm] have "dts <~~> ?dts" .
from permutation_Ex_bij [OF this] len obtain f where
bij: "bij_betw f {..<length dts} {..<length dts}" and
f: "⋀ i. i<length dts ⟹ dts ! i = map snd (DPos_impl ♯ D r) ! f i" by auto
from bij_betw_imp_surj_on[OF bij] have bij: "f ` {..< length dts} = {..< length dts}" .
let ?pps = "map (λ i. fst (DPos_impl ♯ D r ! f i)) [0 ..< length dts]"
from ok have l: "dl = ♯ l" by simp
let ?pps' = "(λi. fst (DPos_impl ♯ D r ! f i)) ` {0 ..< length dts}"
let ?ps' = "fst ` {DPos_impl ♯ D r ! i |i. i < length dts}"
{
fix p
assume "p ∈ ?pps'"
then obtain i where p: "p = fst (DPos_impl ♯ D r ! f i)" and i: "i < length dts" by auto
from i bij have "f i < length dts" by auto
hence "p ∈ ?ps'" unfolding p by auto
}
moreover
{
fix p
assume "p ∈ ?ps'"
then obtain i where p: "p = fst (DPos_impl ♯ D r ! i)" and i: "i < length dts" by auto
from i bij have "i ∈ f ` {..<length dts}" by auto
then obtain j where i: "i = f j" and j: "j < length dts" by auto
have "p ∈ ?pps'" unfolding p i using j by auto
}
ultimately have pps: "?pps' = ?ps'" by blast
show ?thesis unfolding lr dt is_DT_of_def fst_conv snd_conv
proof (rule conjI[OF l], rule exI[of _ C], rule exI[of _ ?pps], rule conjI)
have "set ?pps = set ?ps"
unfolding set_map set_upt
unfolding set_conv_nth pps
by (simp add: len)
also have "… = DPos r"
by (auto simp: DPos_impl)
finally show "set ?pps = DPos r" .
next
have "dr =⇩f (C, dts)" by fact
also have "dts = map (λq. ♯ (r |_ q)) ?pps"
proof (rule nth_equalityI, simp, intro allI impI)
fix i
assume i: "i < length dts"
with bij have fi: "f i < length dts" by auto
let ?goal = "dts ! i = map (λq. ♯ (r |_ q)) ?pps ! i"
have "?goal =
(map snd (DPos_impl ♯ D r) ! f i = ♯ (r |_ fst (DPos_impl ♯ D r ! f i)))"
unfolding f[OF i] using i by simp
also have "…" using fi by (insert DPos_impl[of ♯ r, unfolded set_conv_nth] len, auto)
finally show ?goal by simp
qed
finally show "dr =⇩f (C, map (λq. ♯ (r |_ q)) ?pps)" .
qed
qed
definition dt_transformation ::
"('tp, 'f::show, 'v::show) tp_ops ⇒ ('f, 'v) dt_transformation_info ⇒
('f, 'v) complexity_measure ⇒ complexity_class ⇒ 'tp ⇒
(('f, 'v) complexity_measure × 'tp) result"
where
"dt_transformation I info cm cc cp =
(case info of DT_Transformation_Info S_DT_s W_DT_w 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_DT_s;
let W = map fst W_DT_w;
let R = S @ W;
let DD = defined_list R;
let DD' = set D';
check_allm (λ lr. check (∃ lr' ∈ set S. lr =⇩v lr') (shows ''could not find DT for strict rule '' +@+ shows lr)) S';
check_allm (λ lr. check (∃ lr' ∈ set W. lr =⇩v lr') (shows ''could not find DT for weak rule '' +@+ shows lr)) W';
check_allm (λ f. check (f ∈ DD') (shows ''defined symbol '' +@+ shows f +@+
shows '' does not occur in defined symbols from RC'')) DD;
let DTs = map snd S_DT_s;
let DTw = map snd W_DT_w;
let D = set DD;
let shpf = (λ (f, n :: nat). (♯ f, n));
let Ds = shpf ` D;
let DDD = (♯ o fst) ` D;
let F = funas_trs_list R @ C' @ D';
let Fs = set F;
check_allm (λ q. check (is_Fun q ∧ the (root q) ∉ Fs) (shows ''new Q-term '' +@+ shows q +@+ shows '' not allowed'')) Q';
check_wf_trs R;
check_NF_terms_subset (tp_ops.is_QNF I cp) (map fst R) <+? (λ s. shows ''innermost required'');
check_allm (λ f. check (f ∉ Ds) (shows f +@+ shows '' as sharped symbol is not fresh'')) F;
check (set C' ∩ D = {}) (shows ''constructors of RC and defined symbols of TRSs are not disjoint'');
check_allm (check_rule_dt D DDD) S_DT_s;
check_allm (check_rule_dt D DDD) W_DT_w;
return (Runtime_Complexity C' (map shpf D'), tp_ops.mk I False (tp_ops.Q I cp @ Q') DTs (R @ DTw))
})
| Derivational_Complexity _ ⇒
error (shows ''only runtime complexity supported for dependency tuples'')))
<+? (λ e. shows ''error when switching to dependency tuples'' +@+ shows_nl +@+ e)"
lemma dt_transformation:
assumes "tp_spec I"
and res: "dt_transformation 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 S_DT_s W_DT_w Q' where info: "info = DT_Transformation_Info S_DT_s W_DT_w Q'"
by (cases info, auto)
note res = res[unfolded dt_transformation_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_DT_s"
let ?W = "fst ` set W_DT_w"
let ?R = "?S ∪ ?W"
let ?nfs = "NFS tp"
let ?D = "Collect (defined ?R)"
let ?DDD = "(♯ ∘ fst) ` ?D"
let ?shp = "λ (f, n :: nat). (shp f, n)"
let ?Ds = "?shp ` ?D"
let ?D'' = "map ?shp D'"
let ?Q = "set (Q tp)"
let ?Q' = "?Q ∪ set Q'"
let ?DT_S = "snd ` set S_DT_s"
let ?DT_W = "snd ` set W_DT_w"
let ?F = "funas_trs ?R ∪ set C' ∪ set D'"
let ?NF = "NF_terms ((fst ∘ fst) ` set S_DT_s ∪ (fst ∘ fst) ` set W_DT_w)"
note res = res[unfolded cm Let_def, simplified]
from res have wf: "wf_trs ?R" and
D: "set C' ∩ ?D = {}" and
inn: "NF_terms ?Q ⊆ ?NF" and
Ds: "?Ds ∩ ?F = {}" and
D': "?D ⊆ set D'" and
tp': "tp' = mk False (Q tp @ Q') (map snd S_DT_s) (map fst S_DT_s @ map fst W_DT_w @ map snd W_DT_w)" and
cm': "cm' = Runtime_Complexity C' ?D''" and
DT_S: "(∀x∈ ?S'. ∃ lr ∈ ?S. x =⇩v lr)" and
DT_W: "(∀x∈ ?W'. ∃ lr ∈ ?W. x =⇩v lr)" and
check_S: "(∀x∈set S_DT_s. isOK (check_rule_dt ?D ?DDD x))" and
check_W: "(∀x∈set W_DT_w. isOK (check_rule_dt ?D ?DDD x))"
by auto
have "?NF = NF_trs ?R" unfolding NF_terms_lhss[of ?R, symmetric]
by (rule arg_cong[of _ _ NF_terms], force)
with inn have inn: "NF_terms ?Q ⊆ NF_trs ?R" by simp
have DF: "?D ⊆ ?F" using defined_funas_trs by blast
interpret innermost_wf ?D ?R ?Q
by (unfold_locales, insert wf inn, auto)
interpret DT_trans ?D ?R ?Q ?F shp ?Ds ?Q'
by (unfold_locales, force, force, rule DF, rule Ds, insert res, force)
have subset: "?S ⊆ ?R" "?W ⊆ ?R" by auto
from cpx[unfolded cm' tp' mk_sound]
have cpx: "deriv_bound_measure_class
((qrstep False ?Q' (?R ∪ ?DT_W))⇧* O
qrstep False ?Q' ?DT_S O
(qrstep False ?Q' (?R ∪ ?DT_W))⇧*)
(Runtime_Complexity C' ?D'') cc" by (simp add: ac_simps)
show ?thesis unfolding qreltrs_sound split cm
proof (rule deriv_bound_measure_class_mono[OF relto_mono subset_refl subset_refl dependency_tuples_sound[of ?S ?DT_S ?W ?DT_W _ C' ?D'' cc D', OF _ _ subset refl cpx D' D]])
show "qrstep ?nfs ?Q ?S' ⊆ qrstep ?nfs ?Q ?S"
by (rule qrstep_rename_vars, insert DT_S, force)
show "qrstep ?nfs ?Q ?W' ⊆ qrstep ?nfs ?Q ?W"
by (rule qrstep_rename_vars, insert DT_W, force)
next
fix lr
assume "lr ∈ ?S"
with DT_S obtain dt where lr_dt: "(lr,dt) ∈ set S_DT_s" by auto
hence dt: "dt ∈ ?DT_S" by auto
with check_rule_dt[OF check_S[rule_format, OF lr_dt]]
show "∃ dt ∈ ?DT_S. is_DT_of lr dt" by blast
next
fix lr
assume "lr ∈ ?W"
with DT_W obtain dt where lr_dt: "(lr,dt) ∈ set W_DT_w" by auto
hence dt: "dt ∈ ?DT_W" by auto
with check_rule_dt[OF check_W[rule_format, OF lr_dt]]
show "∃ dt ∈ ?DT_W. is_DT_of lr dt" by blast
qed auto
qed
end
end