theory Complexity_Framework_Impl
imports
Complexity_Framework
QTRS.QDP_Framework_Impl
QTRS.Trs_Impl
begin
fun is_Fsharp_term :: "'f sig ⇒ 'f sig ⇒ ('f,'v)term ⇒ bool" where
"is_Fsharp_term _ _ (Var _) = False"
| "is_Fsharp_term FS F (Fun f ts) = ( (f,length ts) ∈ FS ∧ set (concat (map funas_term_list ts)) ⊆ F)"
lemma is_Fsharp_term[simp]: "is_Fsharp_term FS F t = (t ∈ Fsharp_terms FS F)"
by (cases t, auto simp: Fsharp_terms.simps)
definition split_DP :: "'f sig ⇒ ('f, 'v) rule ⇒ ('f, 'v) mctxt × ('f, 'v) term list"
where
"split_DP FS = (λr. split_term (λt. is_Fun t ∧ the (root t) ∈ FS) (snd r))"
primrec
check_DP_complexity ::
"('f :: show, 'v :: show) rules ⇒ ('f, 'v) complexity_measure ⇒
shows + ('f, 'v) rules × ('f, 'v) rules × ('f × nat) list × ('f × nat) list × ('f × nat) list"
where
"check_DP_complexity P (Derivational_Complexity _) = error (shows ''require runtime complexity'')" |
"check_DP_complexity P (Runtime_Complexity C FS) = do {
let FS' = set FS;
let (RS, R) = partition (λ lr. the (root (fst lr)) ∈ FS') P;
let Cs_ts = map (split_DP FS') RS;
let Cp = remdups (concat (map (funas_mctxt_list o fst) Cs_ts));
let Cp' = set Cp;
let F = remdups (C @ funas_trs_list R @
concat [funas_term_list s. (fs, _) ← RS, s ← args fs] @
concat [funas_term_list s. (_, ts) ← Cs_ts, t ← ts, s ← args t]);
let F' = set F;
check (F' ∩ FS' = {} ∧ F' ∩ Cp' = {} ∧ FS' ∩ Cp' = {}) (shows ''symbols are not disjoint'');
check (∀ lr ∈ set RS. is_Fsharp_term FS' F' (fst lr)) (shows ''lhss of RS are not sharp terms'');
return (RS, R, Cp, FS, F)
}"
lemma check_DP_complexity:
assumes check: "check_DP_complexity P cm = return (RS, R, Cp, FS, F)"
and wf: "wf_trs (set P)"
shows "set P = set RS ∪ set R ∧ is_DP_complexity (set Cp) (set FS) (set F) (set RS) (set R) cm"
proof -
from check obtain C FS' where cm: "cm = Runtime_Complexity C FS'" by (cases cm, auto)
let ?FS = "set FS'"
note check = check[unfolded cm check_DP_complexity.simps]
obtain RS' R' where part: "partition (λlr. the (root (fst lr)) ∈ ?FS) P = (RS',R')" by force
let ?Cs_ts = "map (split_DP ?FS) RS'"
def F' ≡ "remdups (C @ funas_trs_list R' @
concat [funas_term_list s. (fs, _) ← RS', s ← args fs] @
concat [funas_term_list s. (_, ts) ← ?Cs_ts, t ← ts, s ← args t])"
def Cp' ≡ "remdups (concat (map (funas_mctxt_list ∘ fst) ?Cs_ts))"
let ?RS = "set RS'"
let ?R = "set R'"
let ?Cp = "set Cp'"
let ?F = "set F'"
let ?FST = "Fsharp_terms ?FS ?F"
note check = check[unfolded Let_def part split F'_def[symmetric] Cp'_def[symmetric], simplified]
from check have id: "RS = RS'" "R = R'" "FS = FS'" "Cp = Cp'" "F = F'" by auto
from part have p: "set P = ?RS ∪ ?R" by auto
with wf have wf: "wf_trs ?RS" "wf_trs ?R" unfolding wf_trs_def by auto
from F'_def have RF: "funas_trs ?R ⊆ ?F" by auto
from check have disj: "?FS ∩ ?Cp = {}" "?FS ∩ ?F = {}" "?Cp ∩ ?F = {}" by auto
from check have lhss: "lhss ?RS ⊆ ?FST" by auto
show ?thesis unfolding id
proof (rule conjI[OF p], rule is_DP_complexity[OF wf RF lhss _ disj])
fix l r
assume lr: "(l, r) ∈ ?RS"
let ?test = "(λt. is_Fun t ∧ the (root t) ∈ ?FS)"
obtain C ts where split_lr: "split_DP ?FS (l, r) = (C, ts)" by force
note split = this [unfolded split_DP_def, simplified]
from split split_term_eqf [of r ?test] have eq: "r =⇩f (C, ts)" by simp
from uncap_till [of ?test r]
have ts: "⋀t. t ∈ set ts ⟹ is_Fun t ∧ the (root t) ∈ ?FS" using split by auto
have "?Cp = (⋃lr∈set RS'. funas_mctxt (fst (split_DP (set FS') lr)))" unfolding Cp'_def by simp
with lr split_lr have C: "funas_mctxt C ⊆ ?Cp" by auto
show "∃C ts. r =⇩f (C, ts) ∧ funas_mctxt C ⊆ ?Cp ∧ set ts ⊆ ?FST"
proof (intro exI conjI, rule eq, rule C, rule)
fix t
assume t: "t ∈ set ts"
from ts [OF t] obtain f ss where tf: "t = Fun f ss" and f: "(f, length ss) ∈ ?FS" by auto
show "t ∈ ?FST" unfolding tf
proof (rule Fsharp_term[OF f])
fix s
assume "s ∈ set ss"
with tf have "s ∈ set (args t)" by auto
with lr split_lr t
show "funas_term s ⊆ ?F" unfolding F'_def by force
qed
qed
qed (simp add: cm F'_def)
qed
definition split_proc_complexity ::
"('tp, 'f::show, 'v::show) tp_ops ⇒ ('f,'v)rules ⇒
'tp ⇒ ('tp × 'tp)result"
where "split_proc_complexity I S1 cp ≡ do {
let S = tp_ops.R I cp;
let W = tp_ops.Rw I cp;
let nfs = tp_ops.nfs I cp;
let Q = tp_ops.Q I cp;
check_subseteq S1 S <+? (λ lr. shows ''rule '' +@+ shows_rule lr +@+ shows '' is not a strict rule'');
let S2 = list_diff S S1;
return (tp_ops.mk I nfs Q S1 (S2 @ W), tp_ops.mk I nfs Q S2 (S1 @ W))
}
<+? (λ e. shows ''error when splitting complexity problem'' +@+ shows_nl +@+ e)"
lemma split_proc_complexity: assumes "tp_spec I"
and res: "split_proc_complexity I S1 tp = return (tp1,tp2)"
and cpx1: "deriv_bound_measure_class (rel_qrstep (tp_ops.qreltrs I tp1)) cm cc"
and cpx2: "deriv_bound_measure_class (rel_qrstep (tp_ops.qreltrs I tp2)) cm cc"
shows "deriv_bound_measure_class (rel_qrstep (tp_ops.qreltrs I tp)) cm cc"
proof -
interpret tp_spec I by fact
obtain nfs q s w where tp: "qreltrs tp = (nfs,q,s,w)" by cases auto
hence id [simp]: "NFS tp = nfs" "set (Q tp) = q" "set (R tp) = s" "set (Rw tp) = w" by auto
def S2 ≡ "list_diff (R tp) S1"
note res = res[unfolded split_proc_complexity_def Let_def, simplified, folded S2_def]
from res have s: "s = set S1 ∪ set S2" using S2_def by auto
from res have tp1: "qreltrs tp1 = (nfs,q,set S1, w ∪ set S2)" by auto
from res have tp2: "qreltrs tp2 = (nfs,q,set S2, w ∪ set S1)" by auto
show ?thesis using cpx1 cpx2 unfolding tp tp1 tp2 split s qrstep_union
by (rule deriv_bound_relto_measure_class_union)
qed
end