theory Usable_Rules_Complexity_Impl
imports
Usable_Rules_Complexity
Usable_Replacement_Map_Impl
"Check-NT.Innermost_Usable_Rules_Impl"
QTRS.Termination_Problem_Spec
QTRS.QDP_Framework_Impl
begin
definition usable_rules_complexity_usymbols ::
"('tp, 'f::show, 'v::show) tp_ops ⇒ ('f,'v)rules ⇒
('f,'v)complexity_measure ⇒ complexity_class ⇒ 'tp proc"
where "usable_rules_complexity_usymbols I NUr cm cc cp ≡ do {
let S = tp_ops.R I cp;
let W = tp_ops.Rw I cp;
let R = S @ W;
check_subseteq NUr R <+? (λ lr. shows ''rule '' +@+ shows_rules NUr +@+ shows '' does not occur in problem'');
let Ur = list_diff R NUr;
let US = set (concat (map (funas_term_list o snd) Ur) @ get_signature_of_cm cm);
let Urs = set Ur;
check_varcond_subset Ur;
check_allm (λ lr. check (funas_term (fst lr) ⊆ US ⟶ lr ∈ Urs) (shows ''rule ''
+@+ shows_rule lr +@+ shows '' should be usable'')) R;
return (tp_ops.mk I (tp_ops.nfs I cp) (tp_ops.Q I cp) (list_diff S NUr) (list_diff W NUr))
}
<+? (λ e. shows ''error when restricting to usable rules w.r.t. usable symbols'' +@+ shows_nl +@+ e)"
lemma usable_rules_complexity_usymbols:
assumes "tp_spec I"
and res: "usable_rules_complexity_usymbols I NUr cm cc tp = return 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 -
note res = res[unfolded usable_rules_complexity_usymbols_def Let_def, simplified]
interpret tp_spec I by fact
let ?S = "set (R tp)"
let ?W = "set (Rw tp)"
let ?R = "?S ∪ ?W"
let ?nfs = "NFS tp"
let ?Q = "set (Q tp)"
let ?Ur = "list_diff (R tp @ Rw tp) NUr"
let ?US = "(⋃x∈ set ?Ur. funas_term (snd x)) ∪ set (get_signature_of_cm cm)"
have US: "usable_symbols_closed ?US (set ?Ur)"
unfolding usable_symbols_closed_def usable_symbols_rule_closed_def by auto
from res have NUr: "set NUr ⊆ ?R" and
wf: "⋀ l r. (l,r) ∈ set ?Ur ⟹ vars_term r ⊆ vars_term l" and
tp': "tp' = mk (NFS tp) (Q tp) (list_diff (R tp) NUr) (list_diff (Rw tp) NUr)" and
Ur: "⋀ lr. lr ∈ ?R ⟹
funas_term (fst lr) ⊆ ?US ⟹ lr ∈ set ?Ur" by force+
from NUr have id: "?S - set NUr = ?S ∩ set ?Ur" "?W - set NUr = ?W ∩ set ?Ur" by auto
note bound = cpx[unfolded tp' mk_sound split set_list_diff, unfolded id]
show ?thesis unfolding qreltrs_sound split
proof (rule usable_rules_complexity[OF _ US wf _ _ _ bound])
show "U_usable ?US (set ?Ur) ?R" using Ur unfolding U_usable_def by auto
qed auto
qed
fun extract_rt_C_D :: "('f,'v)complexity_measure ⇒ (('f × nat) list × ('f × nat) list) result" where
"extract_rt_C_D (Runtime_Complexity C D) = return (C,D)"
| "extract_rt_C_D _ = error (shows ''runtime complexity required'')"
definition usable_rules_complexity_innermost ::
"('tp, 'f::{show,key}, string) tp_ops ⇒ ('f,string)rules ⇒
('f,string)complexity_measure ⇒ complexity_class ⇒ 'tp proc"
where "usable_rules_complexity_innermost I NUr cm cc cp ≡ do {
let S = tp_ops.R I cp;
let W = tp_ops.Rw I cp;
let R = S @ W;
check (tp_ops.NFQ_subset_NF_rules I cp) (shows ''innermost required'');
check_wf_trs R;
(Cl,Dl) <- extract_rt_C_D cm;
let C = set Cl;
let D = set Dl;
let isnf = tp_ops.is_QNF I cp;
check (list_inter Cl (defined_list R) = []) (shows ''constructors '' +@+ shows Cl +@+ shows '' must not be defined'');
check_subseteq NUr R <+? (λ lr. shows ''rule '' +@+ shows_rules NUr +@+ shows '' does not occur in problem'');
let Ur = list_diff R NUr;
check_allm (λ (l,r). check (¬ (the (root l) ∈ D ∧ (⋃ (set (map funas_term (args l))) ⊆ C)))
(shows_rule (l,r) +@+ shows '' should be usable'')) NUr;
let (fs,μ,info) = usable_replacement_map.get_fs_μ R (icap_impl' isnf R) True cm;
let is_urc = is_ur_closed_af_impl_tp_mv I cp μ Ur;
check_allm (λ (l,r). check (is_urc (args l) r) (shows ''problem with closure properties of usable rule ''
+@+ shows_rule (l,r) +@+ shows '': rhs is not closed under usable rules'')) Ur;
return (tp_ops.mk I (tp_ops.nfs I cp) (tp_ops.Q I cp) (list_diff S NUr) (list_diff W NUr))
}
<+? (λ e. shows ''error when restricting to innermost usable rules'' +@+ shows_nl +@+ e)"
lemma usable_rules_complexity_innermost:
assumes I: "tp_spec I"
and res: "usable_rules_complexity_innermost I NUr cm cc tp = return 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 -
note res = res[unfolded usable_rules_complexity_innermost_def Let_def, simplified]
interpret tp_spec I by fact
let ?S = "set (R tp)"
let ?W = "set (Rw tp)"
let ?R = "?S ∪ ?W"
let ?RR = "R tp @ Rw tp"
let ?nfs = "NFS tp"
let ?Q = "set (Q tp)"
let ?nf = "λ t. t ∈ NF_terms ?Q"
let ?Ur = "list_diff (R tp @ Rw tp) NUr"
let ?us = "usable_replacement_map.get_fs_μ ?RR (icap_impl' ?nf ?RR)
True cm"
from res obtain Cl Dl where ex: "extract_rt_C_D cm = return (Cl,Dl)" by auto
obtain fs μ info where us: "?us = (fs,μ,info)" by (cases ?us)
from ex have cm: "cm = Runtime_Complexity Cl Dl" by (cases cm, auto)
note res = res[unfolded ex, simplified, unfolded us, simplified]
from res have NUr: "set NUr ⊆ ?R" and
wf: "wf_trs ?R" and
tp': "tp' = mk (NFS tp) (Q tp) (list_diff (R tp) NUr) (list_diff (Rw tp) NUr)" and
inn: "NF_terms ?Q ⊆ NF_trs ?R" and
d: "list_inter Cl (defined_list (R tp @ Rw tp)) = []"
by force+
from usable_replacement_map.get_fs_μ[OF refl us] wf inn
have urm: "usable_replacement_map μ (terms_of cm) (NFS tp) ?R (set (Q tp)) ?R" by auto
from NUr have id: "?S - set NUr = ?S ∩ set ?Ur" "?W - set NUr = ?W ∩ set ?Ur" by auto
from arg_cong[OF d, of set] have d: "⋀ c. c ∈ set Cl ⟹ ¬ defined (set (R tp) ∪ set (Rw tp)) c" by auto
note bound = cpx[unfolded tp' mk_sound split set_list_diff, unfolded id]
interpret R_Q_U_ecap ?R "set ?Ur" ?Q icap'
by (unfold_locales, rule icap, rule inn)
show ?thesis unfolding qreltrs_sound split
proof (rule usable_rules_innermost_complexity_urm[OF _ wf cm d _ _ urm bound])
fix l r
assume "(l, r) ∈ set ?Ur"
with res have "is_ur_closed_af_impl_tp_mv I tp μ (list_diff (R tp @ Rw tp) NUr) (args l) r" by auto
from this[unfolded is_ur_closed_af_impl_tp_mv[OF I]]
show "is_ur_closed_term' ?R (set ?Ur) ?Q icap'
μ (map_vars_term (op # CHR ''x'') ` set (args l)) (map_vars_term (op # CHR ''x'') r)" by auto
qed (insert res, auto)
qed
definition usable_rules_complexity ::
"('tp, 'f::{show,key}, string) tp_ops ⇒ ('f,string)rules ⇒
('f,string)complexity_measure ⇒ complexity_class ⇒ 'tp proc"
where "usable_rules_complexity I NUr cm cc cp ≡
case usable_rules_complexity_usymbols I NUr cm cc cp of
Inr cp' ⇒ Inr cp'
| Inl e ⇒ (case usable_rules_complexity_innermost I NUr cm cc cp of
Inr cp' ⇒ Inr cp'
| Inl e' ⇒ Inl (shows ''neither of the usable rules processors is applicable: '' +@+ shows_nl
+@+ shows ''the one via usable symbols complains as follows'' +@+ shows_nl +@+ e +@+
shows_nl +@+ shows_nl +@+ shows ''and the one via icap and innermost says '' +@+ shows_nl +@+ e'))"
lemma usable_rules_complexity:
assumes I: "tp_spec I"
and res: "usable_rules_complexity I NUr cm cc cp = return cp'"
and cpx: "deriv_bound_measure_class (rel_qrstep (tp_ops.qreltrs I cp')) cm cc"
shows "deriv_bound_measure_class (rel_qrstep (tp_ops.qreltrs I cp)) cm cc"
proof -
let ?one = "usable_rules_complexity_usymbols I NUr cm cc cp"
let ?two = "usable_rules_complexity_innermost I NUr cm cc cp"
note res = res[unfolded usable_rules_complexity_def]
show ?thesis
proof (cases ?one)
case (Inr cpp)
with res usable_rules_complexity_usymbols[OF I Inr] cpx
show ?thesis by auto
next
case (Inl e)
note res = res[unfolded this]
show ?thesis
proof (cases ?two)
case (Inr cpp)
with res usable_rules_complexity_innermost[OF I Inr] cpx
show ?thesis by auto
qed (insert res, auto)
qed
qed
definition
rule_shift_complexity_urm_ur_tt ::
"('tp, 'f, string) tp_ops ⇒ ('f::{show,key}, string) redtriple ⇒ ('f,string)rules ⇒ ('f,string)rules
⇒ ('f,string)complexity_measure ⇒ complexity_class ⇒ 'tp proc"
where
"rule_shift_complexity_urm_ur_tt I rp Rdelete Ur cm cc tp = (let
Rb = tp_ops.rules I tp;
R = tp_ops.R I tp;
Rw = tp_ops.Rw I tp;
R2 = ceta_list_diff R Rdelete;
Rremain = Rw @ R2;
isnf = tp_ops.is_QNF I tp;
inn = tp_ops.NFQ_subset_NF_rules I tp in
check_return (do {
check_subseteq Rdelete Rb
<+? (λ lr. ''rule '' +#+ shows_rule lr +@+
shows '' should be deleted, but does not occur in problem'');
check_wf_trs Rb;
check (tp_ops.NFQ_subset_NF_rules I tp) (shows ''innermost required'');
let (fs,μ,info) = usable_replacement_map.get_fs_μ_DP Rb (icap_impl' isnf Rb) inn Rdelete cm;
let (fs',π',info') = usable_replacement_map.get_fs_μ_DP Rb (icap_impl' isnf Rb) inn Rremain cm;
(Cl,Dl) <- extract_rt_C_D cm;
let C = set Cl;
let D = set Dl;
check (list_inter Cl (defined_list Rb) = []) (shows ''constructors '' +@+ shows Cl +@+ shows '' must not be defined'');
redtriple.valid rp;
check_allm (λ (l,r). check (¬ (the (root l) ∈ D ∧ (⋃ (set (map funas_term (args l))) ⊆ C)))
(shows_rule (l,r) +@+ shows '' should be usable'')) (list_diff Rb Ur);
let is_urc = is_ur_closed_af_impl_tp_mv I tp μ Ur;
let π = af_inter (redtriple.af rp) π';
let is_urcπ = is_ur_closed_af_impl_tp_mv I tp π Ur;
check_allm (λ (l,r). check (is_urc (args l) r ∧ is_urcπ (args l) r)
(shows ''problem with closure properties of usable rule ''
+@+ shows_rule (l,r) +@+ shows '': rhs is not closed under usable rules'')) Ur;
(check_allm (λ f. check (μ f ⊆ redtriple.mono_af rp f)
(''error in monotonicity: strict order for '' +#+ shows f
+@+ '' ensures monotonicity in positions '' +#+ show_position_set f (redtriple.mono_af rp f)
+@+ ''⏎but usable replacement map is '' +#+ show_position_set f (μ f))) fs) <+?
(λ s. s +@+ ''⏎the computed usable replacement map ('' +#+ info +#+ '') is⏎'' +#+
shows_sep (λ f. shows ''mu('' +@+ shows f +@+ shows '') = '' +@+ show_position_set f (μ f)) shows_nl fs
+@+ shows ''⏎and mu(f) = {} for all other symbols f'');
check_allm (redtriple.s rp) (list_inter Rdelete Ur)
<+? (λs. ''problem when orienting strict TRS⏎'' +#+ s);
check_allm (redtriple.ns rp) (list_inter Rremain Ur)
<+? (λs. ''problem when orienting non-strict TRS⏎'' +#+ s);
redtriple.cpx rp cm cc
<+? (λs. shows ''problem when ensuring complexity of order⏎'' o s)
} <+? (λs. ''could not derive the intended complexity '' +#+ shows cc +@+ '' from the following⏎'' +#+
(redtriple.desc rp) +@+ shows_nl +@+ s +@+ ''⏎with usable rules⏎'' +#+ shows_trs Ur))
(tp_ops.mk I (tp_ops.nfs I tp) (tp_ops.Q I tp) R2 (list_union Rw Rdelete)))"
definition "is_ur_closed_af_impl_tp_mv_impl ic qnf r π =
(let urc = (λ S. is_ur_closed_term_af_impl qnf (ic S) π r)
in (λ U S. let S' = map mv_xvar S in (λ t. urc S' U S' (mv_xvar t))))"
lemma rule_shift_complexity_urm_ur_tt_code[code]:
"rule_shift_complexity_urm_ur_tt I rp Rdelete Ur cm cc tp = (let
Rb = tp_ops.rules I tp;
R = tp_ops.R I tp;
Rw = tp_ops.Rw I tp;
R2 = ceta_list_diff R Rdelete;
Rremain = Rw @ R2;
isnf = tp_ops.is_QNF I tp;
inn = tp_ops.NFQ_subset_NF_rules I tp in
check_return (do {
check_subseteq Rdelete Rb
<+? (λ lr. ''rule '' +#+ shows_rule lr +@+
shows '' should be deleted, but does not occur in problem'');
check_wf_trs Rb;
check (tp_ops.NFQ_subset_NF_rules I tp) (shows ''innermost required'');
let (fs,μ,info) = usable_replacement_map.get_fs_μ_DP Rb (icap_impl' isnf Rb) inn Rdelete cm;
let (fs',π',info') = usable_replacement_map.get_fs_μ_DP Rb (icap_impl' isnf Rb) inn Rremain cm;
(Cl,Dl) <- extract_rt_C_D cm;
let C = set Cl;
let D = set Dl;
check (list_inter Cl (defined_list Rb) = []) (shows ''constructors '' +@+ shows Cl +@+ shows '' must not be defined'');
redtriple.valid rp;
check_allm (λ (l,r). check (¬ (the (root l) ∈ D ∧ (⋃ (set (map funas_term (args l))) ⊆ C)))
(shows_rule (l,r) +@+ shows '' should be usable'')) (list_diff Rb Ur);
let ic = icap_impl_tp I tp;
let qnf = tp_ops.is_QNF I tp;
let r = tp_ops.rules I tp;
let UU = set Ur;
let is_urc = is_ur_closed_af_impl_tp_mv_impl ic qnf r μ UU;
let π = af_inter (redtriple.af rp) π';
let is_urcπ = is_ur_closed_af_impl_tp_mv_impl ic qnf r π UU;
check_allm (λ (l,r). check (is_urc (args l) r ∧ is_urcπ (args l) r)
(shows ''problem with closure properties of usable rule ''
+@+ shows_rule (l,r) +@+ shows '': rhs is not closed under usable rules'')) Ur;
(check_allm (λ f. check (μ f ⊆ redtriple.mono_af rp f)
(''error in monotonicity: strict order for '' +#+ shows f
+@+ '' ensures monotonicity in positions '' +#+ show_position_set f (redtriple.mono_af rp f)
+@+ ''⏎but usable replacement map is '' +#+ show_position_set f (μ f))) fs) <+?
(λ s. s +@+ ''⏎the computed usable replacement map ('' +#+ info +#+ '') is⏎'' +#+
shows_sep (λ f. shows ''mu('' +@+ shows f +@+ shows '') = '' +@+ show_position_set f (μ f)) shows_nl fs
+@+ shows ''⏎and mu(f) = {} for all other symbols f'');
check_allm (redtriple.s rp) (list_inter Rdelete Ur)
<+? (λs. ''problem when orienting strict TRS⏎'' +#+ s);
check_allm (redtriple.ns rp) (list_inter Rremain Ur)
<+? (λs. ''problem when orienting non-strict TRS⏎'' +#+ s);
redtriple.cpx rp cm cc
<+? (λs. shows ''problem when ensuring complexity of order⏎'' o s)
} <+? (λs. ''could not derive the intended complexity '' +#+ shows cc +@+ '' from the following⏎'' +#+
(redtriple.desc rp) +@+ shows_nl +@+ s +@+ ''⏎with usable rules⏎'' +#+ shows_trs Ur))
(tp_ops.mk I (tp_ops.nfs I tp) (tp_ops.Q I tp) R2 (list_union Rw Rdelete)))"
unfolding rule_shift_complexity_urm_ur_tt_def Let_def is_ur_closed_af_impl_tp_mv_impl_def
is_ur_closed_af_impl_tp_mv_def by simp
lemma rule_shift_complexity_urm_ur_tt:
assumes I: "tp_spec I"
and grp: "generic_redtriple_impl grp"
and res: "rule_shift_complexity_urm_ur_tt I (grp rp) Rdelete Ur cm cc tp = return 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 -
interpret tp_spec I by fact
interpret generic_redtriple_impl grp by (rule grp)
note res = res[unfolded rule_shift_complexity_urm_ur_tt_def Let_def, simplified]
let ?rp = "grp rp"
let ?R = "set (R tp)"
let ?Rw = "set (Rw tp)"
let ?D = "ceta_list_diff (R tp) Rdelete"
let ?RwD = "Rw tp @ ?D"
let ?nfs = "NFS tp"
let ?U = "set Ur"
let ?Q = "set (Q tp)"
let ?nf = "λ t. t ∈ NF_terms ?Q"
let ?QS = "qrstep ?nfs ?Q"
let ?usgen = "λ rls. usable_replacement_map.get_fs_μ_DP (rules tp) (icap_impl' ?nf (rules tp))
(NF_terms (set (Q tp)) ⊆ NF_trs (set (R tp) ∪ set (Rw tp))) rls cm"
let ?us = "?usgen Rdelete"
let ?usW = "?usgen ?RwD"
let ?pi = "mono_af (grp rp)"
from res obtain Cl Dl where ex: "extract_rt_C_D cm = return (Cl,Dl)" by auto
obtain fs μ info where us: "?us = (fs,μ,info)" by (cases ?us)
obtain fs' π' info' where usW: "?usW = (fs',π',info')" by (cases ?usW)
let ?π = "af_inter (redtriple.af (grp rp)) π'"
note res = res[unfolded us usW ex, simplified]
from res have valid: "isOK (redtriple.valid ?rp)"
and S: "isOK(check_allm (redtriple.s ?rp) (list_inter Rdelete Ur))"
and NS: "isOK(check_allm (redtriple.ns ?rp) (list_inter ?RwD Ur))"
and af: "⋀ f. f ∈ set fs ⟹ μ f ⊆ ?pi f"
and inn: "NF_terms ?Q ⊆ NF_trs (?R ∪ ?Rw)"
and wf: "wf_trs (set (rules tp))" "wf_trs (?R ∪ ?Rw)"
and subset: "set Rdelete ∪ (?Rw ∪ set ?D) ⊆ ?R ∪ ?Rw" "set Rdelete ⊆ ?R ∪ ?Rw" "set ?RwD ⊆ ?R ∪ ?Rw"
and init: "(∀(l, r)∈ (?R ∪ ?Rw) - ?U.
the (root l) ∈ set Dl ⟶ ¬ UNION (set (args l)) funas_term ⊆ set Cl)"
and Ur: "(∀(l, r) ∈ ?U.
is_ur_closed_af_impl_tp_mv I tp μ Ur (args l) r ∧
is_ur_closed_af_impl_tp_mv I tp ?π Ur (args l) r)"
by auto
from ex have cm: "cm = Runtime_Complexity Cl Dl" by (cases cm, auto)
have rules: "set (rules tp) = ?R ∪ ?Rw" by auto
note urm = usable_replacement_map.get_fs_μ_DP[OF refl us wf(1), unfolded rules, OF subset(2) refl]
note urm2 = usable_replacement_map.get_fs_μ_DP(2)[OF refl usW wf(1), unfolded rules, OF subset(3) refl]
interpret R_Q_U_ecap "?R ∪ ?Rw" ?U ?Q icap'
by (unfold_locales, rule icap, rule inn)
have af: "af_subset μ ?pi" unfolding af_subset_def
proof
fix f
show "μ f ⊆ ?pi f"
by (cases "f ∈ set fs", rule af, insert urm(1), auto)
qed
let ?cpx = "redtriple.cpx (grp rp) cm"
let ?Cpx = "λ cm cc. isOK(redtriple.cpx ?rp cm cc)"
from res have tp': "tp' = mk ?nfs (Q tp) ?D (list_union (Rw tp) Rdelete)" by simp
from cpx[unfolded tp', simplified]
have bound: "deriv_bound_measure_class (relto (?QS (?R - set Rdelete)) (?QS (?Rw ∪ set Rdelete))) cm cc" .
from res have cpx: "isOK(?cpx cc)" by auto
from res have d: "list_inter Cl (defined_list (rules tp)) = []" by auto
from arg_cong[OF this, of set] have c: "⋀ c. c ∈ set Cl ⟹ ¬ defined (set (R tp) ∪ set (Rw tp)) c" by auto
from generate_redtriple[OF valid S NS, of Nil]
obtain S NS NST where redpair: "cpx_ce_af_redtriple_order S NS NST (redtriple.af ?rp) (redtriple.mono_af ?rp) ?Cpx"
and S: "set Rdelete ∩ ?U ⊆ S" and NS: "(?Rw ∪ set ?D) ∩ ?U ⊆ NS"
by auto
interpret rp: cpx_ce_af_redtriple_order S NS NST "redtriple.af ?rp" "redtriple.mono_af ?rp" ?Cpx by fact
let ?full = "(λ _. UNIV) :: 'f af"
have full: "⋀ μ. af_subset μ ?full" unfolding af_subset_def by auto
have mono: "af_monotone ?full NS" using ctxt_closed_one[OF rp.wm_NS] unfolding af_monotone_def by blast
have bound1: "deriv_bound_measure_class (relto (?QS (set Rdelete)) (?QS (?Rw ∪ set ?D))) cm cc"
proof (rule usable_rules_innermost_complexity_urm_redpair[
OF subset(1) wf(2) cm c _ S NS af_subset_af_monotone[OF af rp.μ] af_subset_af_monotone[OF full mono] cpx urm(2) _ _ _ redpair])
fix l r
assume "(l, r) ∈ ?R ∪ ?Rw" and "the (root l) ∈ set Dl" and "⋃(funas_term ` set (args l)) ⊆ set Cl"
thus "(l, r) ∈ ?U"
using init by force
next
fix l r
assume lr: "(l, r) ∈ ?U"
note Ur = Ur[rule_format, OF lr, unfolded split, unfolded is_ur_closed_af_impl_tp_mv[OF I]]
show "is_ur_closed_term' (?R ∪ ?Rw) ?U ?Q icap' μ (mv_xvar ` set (args l)) (mv_xvar r)"
using Ur by auto
show "is_ur_closed_term' (?R ∪ ?Rw) ?U ?Q icap' ?π (mv_xvar ` set (args l)) (mv_xvar r)"
using Ur by auto
qed (insert urm2, auto)
have bound: "deriv_bound_measure_class (relto (?QS (set Rdelete ∪ set ?D)) (?QS ?Rw)) cm cc"
unfolding qrstep_union
by (rule deriv_bound_relto_measure_class_union, insert bound bound1, auto simp: qrstep_union)
have bound: "deriv_bound_measure_class (relto (?QS ?R) (?QS ?Rw)) cm cc"
by (rule deriv_bound_measure_class_mono[OF relto_mono[OF qrstep_mono[OF _ subset_refl] subset_refl] subset_refl subset_refl bound], auto)
thus ?thesis by simp
qed
fun smart_rule_shift_complexity :: "('tp, 'f, string) tp_ops ⇒ ('f::{show,key}, string) redtriple ⇒ ('f,string)rules
⇒ ('f,string)rules option
⇒ ('f,string)complexity_measure ⇒ complexity_class ⇒ 'tp proc" where
"smart_rule_shift_complexity I rp Rdelete (Some Ur) cm cc tp = rule_shift_complexity_urm_ur_tt I rp Rdelete Ur cm cc tp"
| "smart_rule_shift_complexity I rp Rdelete None cm cc tp = rule_shift_complexity_urm_tt I rp Rdelete cm cc tp"
lemma smart_rule_shift_complexity:
assumes I: "tp_spec I"
and grp: "generic_redtriple_impl grp"
and res: "smart_rule_shift_complexity I (grp rp) Rdelete Ur_opt cm cc tp = return 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"
using rule_shift_complexity_urm_ur_tt[OF I grp _ cpx]
rule_shift_complexity_urm_tt[OF I grp _ cpx]
res
by (cases Ur_opt, auto)
end