theory Usable_Replacement_Map_Impl
imports
"Check-NT.Icap_Impl"
"Check-NT.Term_Order_Impl"
"QTRS.QDP_Framework_Impl"
QTRS.Map_Choice
"Check-NT.Inductive_Set_Impl"
Usable_Replacement_Map
Complexity_Framework_Impl
"Check-NT.Innermost_Usable_Rules_Impl"
begin
definition "full_empty fs = (let fs' = filter (λ (f,n). n ≠ 0) fs in (fs', λ f. if f ∈ set fs' then full_af f else {}, ''full AF''))"
fun get_args_impl where
"get_args_impl True t = args t"
| "get_args_impl False t = [t]"
lemma get_args_impl[simp]: "set (get_args_impl b t) = get_args b t"
by (cases b, auto)
locale usable_replacement_map =
fixes R :: "('f :: {show,key},string)rules"
and Q :: "('f,string)term list"
and ecap :: "('f,string)term list ⇒ ('f, string) term ⇒ ('f, unit + string) term"
begin
definition innermost_repl_map_impl where
"innermost_repl_map_impl P ≡ remdups [(f,i) . ((l,r),b) <- [(lr,True) . lr <- R] @ [(st,False) . st <- P], u <- supteq_list r, is_Fun u, rs <- [args u], f <- [the (root u)],
n <- [snd f], i <- [0..< n], Inl () ∈ vars_term (ecap (get_args_impl b l) (rs ! i)) ]"
definition μ_i_P_impl :: "('f,string)rules ⇒ (('f × nat)list × 'f af × string)" where
"μ_i_P_impl P ≡ let fis = innermost_repl_map_impl P;
fs = remdups (map fst fis);
μ = (λ f. set (map snd (filter (λ (g,i). g = f) fis)))
in (fs,precompute_fun μ fs, ''innermost URM'')"
definition μ_i_impl :: "(('f × nat)list × 'f af × string)" where
"μ_i_impl = μ_i_P_impl []"
definition "default_fs ≡ funas_trs_list R"
lemma full_empty: assumes fe: "full_empty fs = (fs',μ,info)"
and defa: "set default_fs ⊆ set fs"
and sig: "set (get_signature_of_cm cm) ⊆ set fs"
and wf: "wf_trs (set R)"
shows "⋀ f. f ∉ set fs' ⟹ μ f = {}"
and "usable_replacement_map μ (terms_of cm) nfs (set R) (set Q) (set R)"
proof -
let ?fs = "filter (λ (f,n). n ≠ 0) fs"
from fe[unfolded full_empty_def, simplified]
have μ: "μ = (λf. if f ∈ set ?fs then full_af f else {})" and fs: "fs' = ?fs" by auto
show "⋀ f. f ∉ set fs' ⟹ μ f = {}" unfolding fs μ by auto
let ?T = "terms_of cm"
let ?R = "qrstep nfs (set Q) (set R)"
from defa[unfolded default_fs_def] have R: "funas_trs (set R) ⊆ set fs" by auto
show "usable_replacement_map μ ?T nfs (set R) (set Q) (set R)"
unfolding usable_replacement_map_def
proof
fix t
assume "t ∈ ?R^* `` ?T"
then obtain u where steps: "(u,t) ∈ ?R^*" and u: "u ∈ ?T" by auto
then obtain n where "u ∈ terms_of_nat cm n" by (auto simp: terms_of)
from set_mp[OF get_signature_of_cm this]
have "funas_term u ⊆ set (get_signature_of_cm cm)" by auto
with sig have "funas_term u ⊆ set fs" by auto
from rsteps_preserve_funas_terms[OF R this set_mp[OF rtrancl_mono steps] wf]
have t: "funas_term t ⊆ set fs" by auto
{
fix C s
assume id: "t = C⟨s⟩"
with t have "funas_ctxt C ⊆ set fs" by auto
hence "af_regarded_pos μ t (hole_pos C)" unfolding id
proof (induct C)
case (More f bef C aft)
let ?i = "length bef"
let ?n = "Suc (?i + length aft)"
from More
have IH: "af_regarded_pos μ C⟨s⟩ (hole_pos C)" and
f: "(f,?n) ∈ set fs" by auto
from f have "?i ∈ μ (f,?n)" unfolding μ full_af_def by auto
with IH show ?case by auto
qed simp
}
thus "t ∈ af_nf_compatible_terms μ ?R" unfolding af_nf_compatible_terms_def by auto
qed
qed
fun get_fs_μ :: "bool ⇒ ('f,string)complexity_measure ⇒ (('f × nat)list × 'f af × string)" where
"get_fs_μ inn (Derivational_Complexity F) = (full_empty (remdups (F @ default_fs)))"
| "get_fs_μ inn (Runtime_Complexity C D) =
(if inn ∧ set C ∩ set (defined_list R) ⊆ {} then μ_i_impl
else full_empty (remdups (C @ D @ default_fs))
)"
definition get_fs_μ_DP :: "bool ⇒ ('f,string)rules ⇒ ('f,string)complexity_measure ⇒ (('f × nat)list × 'f af × string)" where
"get_fs_μ_DP inn S cm = (
let (fs,μ,info) = get_fs_μ inn cm
in (case check_DP_complexity R cm of
Inr (RS, R', Cp, FS, F) ⇒ if set S ⊆ set RS then (list_inter fs Cp, λ f. if f ∈ set Cp then μ f else {}, info @ '' with DPs'') else (fs,μ,info)
| _ ⇒ (fs,μ,info)))"
context
assumes ecap: "ecap = icap_impl' (λ t. t ∈ NF_terms (set Q)) R"
begin
lemma innermost_repl_map_impl[simp]: "set (innermost_repl_map_impl P) = innermost_repl_map icap' (set R) (set Q) (set P)"
(is "?l = ?r")
proof -
note d = innermost_repl_map_impl_def
def RR ≡ "set R × {True} ∪ set P × {False}"
def RR' ≡ "(map (λlr. (lr, True)) R @ map (λst. (st, False)) P)"
have [simp]: "set RR' = RR" unfolding RR_def RR'_def by auto
have "?r = { ((f,length rs),i) | l C f rs i b. ((l,C⟨Fun f rs⟩),b) ∈ RR ∧
i < length rs ∧ Inl () ∈ vars_term (ecap (get_args_impl b l) (rs ! i))}" (is "_ = ?m")
unfolding innermost_repl_map_def RR_def
unfolding icap' icap_mv_def[symmetric] icap_impl'_sound[symmetric]
ecap[symmetric] get_args_impl[symmetric]
by (rule refl)
also have "?m = ?l"
proof -
{
fix f n i
assume "((f,n),i) ∈ ?m"
then obtain l C rs b where lr: "((l,C⟨Fun f rs⟩),b) ∈ RR"
and *: "i < length rs ∧ Inl () ∈ vars_term (ecap (get_args_impl b l) (rs ! i))"
and n: "n = length rs" by auto
have "((f,n),i) ∈ ?l" unfolding d n RR'_def[symmetric]
by (clarsimp, rule bexI[OF _ lr], rule exI, rule exI, rule exI, rule conjI[OF refl],
rule bexI[of _ "Fun f rs"], insert *, auto)
}
hence one: "?m ⊆ ?l" by force
{
fix fn i
assume "(fn,i) ∈ ?l"
from this[unfolded d, folded RR'_def]
obtain l r u b where
lr: "((l,r),b) ∈ RR"
and supt: "r ⊵ u" and u: "is_Fun u"
and f: "fn = the (root u)"
and i: "i < snd (the (root u))"
and cap: "Inl () ∈ vars_term (ecap (get_args_impl b l) (args u ! i))" by auto
from supt obtain C where r: "r = C ⟨ u ⟩" by auto
from u obtain f rs where u: "u = Fun f rs" by auto
have "(fn,i) ∈ ?m" using lr i cap unfolding u r f by auto
}
hence "?l ⊆ ?m" by auto
with one show ?thesis by blast
qed
finally show ?thesis by simp
qed
lemma μ_i_P_impl: assumes impl: "μ_i_P_impl P = (fs,μ,info)"
shows "μ = μ_i_P icap' (set R) (set Q) (set P) ∧ (∀ f. f ∉ set fs ⟶ μ f = {})"
proof -
note d = μ_i_P_impl_def Let_def
show ?thesis
proof (intro conjI allI impI)
fix f
assume "f ∉ set fs"
thus "μ f = {}"
using impl by (auto simp: d)
next
show "μ = μ_i_P icap' (set R) (set Q) (set P)" using impl unfolding d
by (intro ext, auto simp: μ_i_P_def)
qed
qed
lemma μ_i_impl: assumes impl: "μ_i_impl = (fs,μ,info)"
shows "μ = μ_i icap' (set R) (set Q) ∧ (∀ f. f ∉ set fs ⟶ μ f = {})"
unfolding μ_i_def using μ_i_P_impl[OF impl[unfolded μ_i_impl_def]] by auto
lemma get_fs_μ: assumes split: "get_fs_μ inn cm = (fs,μ,info)"
and wf: "wf_trs (set R)"
and inn: "inn = (NF_terms (set Q) ⊆ NF_trs (set R))"
shows "⋀ f. f ∉ set fs ⟹ μ f = {}"
and "usable_replacement_map μ (terms_of cm) nfs (set R) (set Q) (set R)"
proof -
have "(∀ f. f ∉ set fs ⟶ μ f = {}) ∧ usable_replacement_map μ (terms_of cm) nfs (set R) (set Q) (set R)"
proof (cases cm)
case (Derivational_Complexity F) note cm = this
from split[unfolded cm]
have "full_empty (remdups (F @ default_fs)) = (fs, μ, info)" by simp
from full_empty[OF this _ _ wf, of cm]
show ?thesis unfolding cm by auto
next
case (Runtime_Complexity C D) note cm = this
let ?cond = "inn ∧ set C ∩ {fn. defined (set R) fn} = {}"
show ?thesis
proof (cases ?cond)
case False
with split[unfolded cm]
obtain info where "full_empty (remdups (C @ D @ default_fs)) = (fs, μ, info)" by auto
from full_empty[OF this _ _ wf, of cm]
show ?thesis unfolding cm by auto
next
case True
with split[unfolded cm]
have "μ_i_impl = (fs,μ,info)" by auto
from μ_i_impl[OF this] have μ: "μ = μ_i icap' (set R) (set Q)" and
fs: "(∀f. f ∉ set fs ⟶ μ f = {})" by auto
show ?thesis
by (rule conjI[OF fs], unfold μ cm, rule hirokawa_moser_4_8_1[OF _ icap],
insert True[unfolded inn] wf_trs_imp_wwf_qtrs[OF wf], auto)
qed
qed
thus "⋀ f. f ∉ set fs ⟹ μ f = {}"
and "usable_replacement_map μ (terms_of cm) nfs (set R) (set Q) (set R)"
by blast+
qed
lemma get_fs_μ_DP: assumes get: "get_fs_μ_DP inn S cm = (fs,μ,info)"
and wf: "wf_trs (set R)"
and S: "set S ⊆ set R"
and inn: "inn = (NF_terms (set Q) ⊆ NF_trs (set R))"
shows "⋀ f. f ∉ set fs ⟹ μ f = {}"
and "usable_replacement_map μ (terms_of cm) nfs (set R) (set Q) (set S)"
proof -
note d = get_fs_μ_DP_def
obtain fs' μ' info where get': "get_fs_μ inn cm = (fs',μ',info)" by (cases "get_fs_μ inn cm")
from get_fs_μ[OF this wf inn] have f: "⋀ f. f ∉ set fs' ⟹ μ' f = {}"
and urm: "usable_replacement_map μ' (terms_of cm) nfs (set R) (set Q) (set R)" by auto
from usable_replacement_map_mono[OF _ _ S urm]
have urm: "usable_replacement_map μ' (terms_of cm) nfs (set R) (set Q) (set S)" by auto
have "(∀ f. f ∉ set fs ⟶ μ f = {}) ∧ usable_replacement_map μ (terms_of cm) nfs (set R) (set Q) (set S)"
proof (cases "(fs,μ,info) = (fs',μ',info)")
case True
with f urm show ?thesis by auto
next
case False
note get = get[unfolded d get' Let_def split]
from get False obtain res where check: "check_DP_complexity R cm = Inr res" by (cases "check_DP_complexity R cm", auto)
obtain RS R' Cp FS F where res: "res = (RS, R', Cp, FS, F)" by (cases res, auto)
from get[unfolded check res, simplified] False have S: "set S ⊆ set RS"
and fs: "fs = list_inter fs' Cp" and μ: "μ = (λf. if f ∈ set Cp then μ' f else {})"
by (auto split: if_splits)
from check_DP_complexity[OF check[unfolded res] wf]
have R: "set R = set RS ∪ set R'" and dp: "is_DP_complexity (set Cp) (set FS) (set F) (set RS) (set R') cm"
by auto
have urm: "usable_replacement_map μ (terms_of cm) nfs (set R) (set Q) (set S)"
by (rule avanzini_14_34[OF urm[unfolded R] dp S, folded R], auto simp: μ)
show ?thesis
by (rule conjI[OF _ urm], auto simp: fs μ f)
qed
thus "⋀ f. f ∉ set fs ⟹ μ f = {}" and "usable_replacement_map μ (terms_of cm) nfs (set R) (set Q) (set S)"
by auto
qed
end
end
declare usable_replacement_map.get_fs_μ.simps[code]
declare usable_replacement_map.get_fs_μ_DP_def[code]
declare usable_replacement_map.μ_i_impl_def[code]
declare usable_replacement_map.μ_i_P_impl_def[code]
declare usable_replacement_map.default_fs_def[code]
declare usable_replacement_map.innermost_repl_map_impl_def[code]
section ‹Computation of AProVE's urms›
locale urm_computation =
fixes ecap :: "('f :: key,string)cap_fun"
and R :: "('f,string)trs"
and Q :: "('f,string)terms"
and U :: "('f,string)term list ⇒ ('f,string)term ⇒ ('f,string)trs"
and init :: "(('f,string)term list × ('f,string)term × ('f,string)rule)set"
begin
abbreviation "approx_cond' ≡ approx_cond ecap R Q U init"
abbreviation "μ_cond' ≡ μ_cond ecap R Q U init"
abbreviation "μ_approx' ≡ μ_approx ecap R Q U init"
abbreviation "rule_match' ≡ rule_match R Q ecap"
lemmas approx_cond_rec = approx_cond_rec[of ecap R Q U init]
lemmas approx_cond_sub = approx_cond_sub[of ecap R Q U init]
lemmas approx_cond_init = approx_cond_init[of _ _ _ init ecap R Q U]
lemmas μ_cond = μ_cond[of ecap R Q U init]
definition "all_terms = {(ss,t) | ss t lr. (ss,t,lr) ∈ init} ∪ {(args l, r) | l r. (l,r) ∈ R}"
definition "all_subterms = {(ss,t) | ss s t. (ss,s) ∈ all_terms ∧ s ⊵ t}"
definition "everything ≡ Inl ` {(ss,t,lr) | ss t lr. (ss,t) ∈ all_subterms ∧ (∃ ss t. (ss,t,lr) ∈ init)}
∪ Inr ` { ((f,length ts),i) | f ts i . i < length ts ∧ Fun f ts ∈ snd ` all_subterms}"
abbreviation "gen_a ss f ts l r ≡ Inl ` {(ss, ts ! i, (l,r)) | i. i < length ts ∧ (l,r) ∈ U ss (ts ! i)}"
abbreviation "gen_b ss f ts l r ≡ Inl ` {(args l', r', (l,r)) | l' r'. (l',r') ∈ R ∧ rule_match' (mv_xvar ` (set ss)) f (map mv_xvar ts) l' ∧ (l,r) ∈ U (args l') r'}"
abbreviation "gen_c ss f ts l r ≡ Inr ` {((f,length ts),i) | i. i < length ts ∧ (l,r) ∈ U ss (ts ! i)}"
fun generate where
"generate (Inl (ss, Fun f ts,(l,r))) = gen_a ss f ts l r ∪ gen_b ss f ts l r ∪ gen_c ss f ts l r"
| "generate _ = {}"
interpretation gen_set: generic_inductive_set everything "op =" generate .
definition "check_approx = gen_set.the_set"
lemma check_approx_sound: assumes "check_approx t_lr s"
and "t_lr ∈ Inl ` init"
shows "(∀ ss' t' lr'. s = Inl (ss', t',lr') ⟶ approx_cond' ss' t' lr') ∧
(∀ f i. s = Inr (f,i) ⟶ μ_cond' f i)"
proof -
from assms(2) have "t_lr ∈ Inl ` {(ss,t,lr). approx_cond' ss t lr} ∪ Inr ` {(f,i). μ_cond' f i}" (is "_ ∈ ?sound")
by (cases t_lr, auto intro: approx_cond_init)
from assms(1) this show ?thesis unfolding check_approx_def
proof (induct t_lr s rule: gen_set.the_set_induct)
case (rec t1_lr1 copy t2_lr2 t3_lr3)
note IH = rec(5)[unfolded rec(2)]
note prems = rec(3,6)[unfolded rec(2)]
show ?case
proof (rule IH)
from prems(1) obtain t_lr1 where "t1_lr1 = Inl t_lr1" by (cases t1_lr1, auto)
then obtain ss1 t1 l1 r1 where "t1_lr1 = Inl (ss1,t1,(l1,r1))" by (cases t_lr1, auto)
note prems = prems[unfolded this]
from prems(1) obtain f ts where t1: "t1 = Fun f ts" by (cases t1, auto)
with prems(2) have cond: "approx_cond' ss1 (Fun f ts) (l1,r1)" by auto
note prems = prems(1)[unfolded t1]
show "t2_lr2 ∈ ?sound"
proof (cases t2_lr2)
case (Inr g_i)
with prems obtain i where g_i: "g_i = ((f,length ts),i)"
and i: "i < length ts" and U: "(l1, r1) ∈ U ss1 (ts ! i)" by auto
have "μ_cond' (f,length ts) i"
by (rule μ_cond[OF cond i U])
with Inr g_i show ?thesis by auto
next
case (Inl t_lr2)
with prems obtain ss2 t2 where 2: "t2_lr2 = Inl (ss2,t2,(l1,r1))" by (cases t_lr2, auto)
have "approx_cond' ss2 t2 (l1,r1)"
proof (cases "ss2 = ss1 ∧ (∃ i. t2 = ts ! i ∧ i < length ts ∧ (l1, r1) ∈ U ss1 (ts ! i))")
case True
then obtain i where ss2: "ss2 = ss1" and t2: "t2 = ts ! i" and i: "i < length ts" and U: "(l1,r1) ∈ U ss1 (ts ! i)" by auto
show "approx_cond' ss2 t2 (l1,r1)" unfolding t2 ss2
by (rule approx_cond_sub[OF cond i U])
next
case False
with prems[unfolded 2]
obtain l' r'
where ss2: "ss2 = args l'" and t2: "t2 = r'" and lr: "(l', r') ∈ R"
and match: "rule_match' (mv_xvar ` (set ss1)) f (map mv_xvar ts) l'" and U: "(l1, r1) ∈ U (args l') r'"
by auto
show "approx_cond' ss2 t2 (l1,r1)" unfolding t2 ss2
by (rule approx_cond_rec[OF cond lr match U])
qed
thus ?thesis unfolding 2 by simp
qed
qed
qed auto
qed
lemmas every_defs = everything_def all_subterms_def all_terms_def
lemma the_set_refl: "a ∈ everything ⟹ gen_set.the_set a a"
by (rule gen_set.non_rec, auto)
lemma check_approx_complete:
"approx_cond' ss t lr ⟹ Inl (ss,t,lr) ∈ everything ∧ (∃ t_lr ∈ Inl ` init. check_approx t_lr (Inl (ss,t,lr)))"
"μ_cond' f i ⟹ ∃ t_lr ∈ Inl ` init. check_approx t_lr (Inr (f,i))"
unfolding check_approx_def
proof (induct ss t lr and f i rule: approx_cond_μ_cond.inducts)
case (approx_cond_init ss t lr)
note IH = this
from IH have 1: "(ss,t) ∈ all_subterms" unfolding every_defs by blast
from IH have 2: "∃ ss t. (ss,t,lr) ∈ init" unfolding o_def by force
from 1 2 have every: "Inl (ss,t,lr) ∈ everything" unfolding everything_def by blast
show ?case
by (rule conjI[OF every], rule bexI, rule the_set_refl[OF every],
insert IH, auto)
next
case (μ_cond ss f ts l r i)
note IH = this
let ?t = "Fun f ts"
let ?lr = "(l,r)"
let ?f = "(f,length ts)"
from IH(2) obtain t_lr where tlr: "t_lr ∈ Inl ` init"
and the_set: "gen_set.the_set t_lr (Inl (ss, ?t, ?lr))"
and every: "Inl (ss, ?t, ?lr) ∈ everything" by auto
have gen: "Inr (?f, i) ∈ generate (Inl (ss, ?t, ?lr))"
using IH(3-4) by auto
from every IH(3) have f: "Inr (?f, i) ∈ everything" unfolding everything_def by force
show ?case
by (rule bexI[OF _ tlr], rule gen_set.rec_rec[OF the_set gen the_set_refl[OF f]])
next
case (approx_cond_sub ss f ts l r i)
note IH = this
let ?t = "Fun f ts"
let ?lr = "(l,r)"
let ?f = "(f,length ts)"
from IH(2) obtain t_lr where tlr: "t_lr ∈ Inl ` init"
and the_set: "gen_set.the_set t_lr (Inl (ss, ?t, ?lr))"
and every: "Inl (ss, ?t, ?lr) ∈ everything" by auto
have gen: "Inl (ss, ts ! i, ?lr) ∈ generate (Inl (ss, ?t, ?lr))"
using IH(3-4) by auto
from every have sub: "(ss,?t) ∈ all_subterms" and lr: "∃ s t. (s,t,?lr) ∈ init"
unfolding everything_def by auto
from sub[unfolded all_subterms_def] obtain s where s: "(ss,s) ∈ all_terms" and sub: "s ⊵ ?t" by auto
from IH(3) have "?t ⊵ ts ! i" by auto
with sub have "s ⊵ ts ! i" by (rule supteq_trans)
with s have "(ss,ts ! i) ∈ all_subterms" unfolding all_subterms_def by auto
with lr have every: "Inl (ss,ts ! i, ?lr) ∈ everything" unfolding everything_def by auto
show ?case
by (rule conjI[OF every], rule bexI[OF gen_set.rec_rec[OF _ gen] tlr], rule the_set,
rule the_set_refl[OF every])
next
case (approx_cond_rec ss f ts l r l' r')
note IH = this
let ?t = "Fun f ts"
let ?lr = "(l,r)"
let ?f = "(f,length ts)"
from IH(2) obtain t_lr where tlr: "t_lr ∈ Inl ` init"
and the_set: "gen_set.the_set t_lr (Inl (ss, ?t, ?lr))"
and every: "Inl (ss, ?t, ?lr) ∈ everything" by auto
have gen: "Inl (args l', r', ?lr) ∈ generate (Inl (ss, ?t, ?lr))"
using IH(3-5) by auto
from every have lr: "∃ s t. (s,t,?lr) ∈ init" unfolding everything_def by auto
from IH(3) have "(args l', r') ∈ all_subterms" unfolding every_defs by auto
with lr have every: "Inl (args l', r', ?lr) ∈ everything" unfolding everything_def by auto
show ?case
by (rule conjI[OF every], rule bexI[OF gen_set.rec_rec[OF _ gen] tlr], rule the_set,
rule the_set_refl[OF every])
qed
lemma μ_approx: "μ_approx' f = {i . ∃ t_lr ∈ init. check_approx (Inl t_lr) (Inr (f,i))}" (is "?l = ?r")
proof -
{
fix i
assume "i ∈ ?r"
then obtain t_lr where "check_approx (Inl t_lr) (Inr (f,i))" "t_lr ∈ init" by auto
from check_approx_sound[OF this(1)] this(2) have "μ_cond' f i" by auto
hence "i ∈ ?l" unfolding μ_approx_def by blast
}
moreover
{
fix i
assume "i ∈ ?l"
from this[unfolded μ_approx_def] have "μ_cond' f i" by blast
from check_approx_complete(2)[OF this]
have "i ∈ ?r" by auto
}
ultimately show ?thesis by auto
qed
context
fixes RR :: "('f,string)rules"
and initt :: "(('f,string)term list × ('f,string)term × ('f,string)rule)list"
and U_impl :: "('f,string)term list ⇒ ('f,string)term ⇒ ('f,string)rules"
and NFQ :: "('f,string)term ⇒ bool"
and e_cap :: "('f,string)term list ⇒ ('f,string)term ⇒ ('f, unit + string)term"
begin
definition "all_terms_impl = remdups (map (λ (ss,t,lr). (ss,t)) initt @ map (λ (l,r). (args l,r)) RR)"
definition "all_subterms_impl = remdups [ (ss,t). (ss,s) <- all_terms_impl, t <- supteq_list s]"
definition "everything_impl ≡ map Inl ([(ss,t,lr) . (ss,t) <- all_subterms_impl, lr <- remdups (map (snd o snd) initt)])
@ remdups (map Inr [((f,length ts),i). t <- remdups (map snd all_subterms_impl), is_Fun t, (f,ts) <- (case t of Fun f ts ⇒ [(f,ts)]),
i <- [0..<length ts]])"
abbreviation "gen_ac_impl UU ss f ts l r ≡ [u . i <- [0 ..< length ts], (l,r) ∈ set (UU ss (ts ! i)), u <- [Inl (ss, ts ! i, (l,r)), Inr ((f,length ts), i)]]"
abbreviation "gen_b_impl UU ss f ts l r ≡ [Inl (args l', r', (l,r)) . (l',r') <- RR, mss <- [map mv_xvar ss], rule_match_impl NFQ (e_cap mss) mss f (map mv_xvar ts) l', (l,r) ∈ set (UU (args l') r')]"
fun generate_impl where
"generate_impl UU (Inl (ss, Fun f ts,(l,r))) =
gen_ac_impl UU ss f ts l r @ gen_b_impl UU ss f ts l r"
| "generate_impl UU _ = []"
definition μ_approx_impl where
"μ_approx_impl ≡ let
UU' = precompute_fun (λ (ss,t). U_impl ss t) all_subterms_impl;
UU = λ s t. UU' (s,t);
fis = remdups [fi.
entry <- inductive_set_impl everything_impl op = (generate_impl UU) (map Inl initt),
fi <- (case entry of Inl _ ⇒ [] | Inr fi ⇒ [fi])];
fs = remdups (map fst fis);
μ = (λ f. set (map snd (filter (λ (g,i). g = f) fis)))
in (fs, precompute_fun μ fs, ''innermost URM wrt. specific rules'')"
lemmas μ_approx_impl_code =
μ_approx_impl_def
generate_impl.simps
all_subterms_impl_def
all_terms_impl_def
everything_impl_def
context
assumes RR: "set RR = R"
and initt: "set initt = init"
and U_impl: "⋀ ss t. set (U_impl ss t) = U ss t"
and NFQ: "NFQ = (λ t. t ∈ NF_terms Q)"
and e_cap: "⋀ ss t. e_cap (map mv_xvar ss) (mv_xvar t) = ecap R Q (mv_xvar ` set ss) (mv_xvar t)"
begin
lemma rule_match_impl_e_cap[simp]:
"rule_match_impl NFQ (e_cap (map mv_xvar ss)) (map mv_xvar ss) f (map mv_xvar ts) = rule_match R Q ecap (mv_xvar ` set ss) f (map mv_xvar ts)"
proof -
let ?ss = "map mv_xvar ss"
let ?ts = "map mv_xvar ts"
have "rule_match_impl NFQ (e_cap ?ss) ?ss f ?ts =
rule_match_impl NFQ (ecap R Q (set ?ss)) ?ss f ?ts"
by (rule rule_match_impl_cong, insert e_cap[of ss], auto)
also have "… = rule_match R Q ecap (mv_xvar ` set ss) f ?ts"
unfolding rule_match_impl[of Q _ R ?ss, folded NFQ] by simp
finally show ?thesis .
qed
lemma all_terms_impl[simp]: "set all_terms_impl = all_terms"
unfolding all_terms_def all_terms_impl_def by (force simp: RR initt)
lemma all_subterms_impl[simp]: "set all_subterms_impl = all_subterms"
unfolding all_subterms_def all_subterms_impl_def by auto
lemma everything_impl[simp]: "set everything_impl = everything"
proof -
have cong: "⋀ a b c d. a = b ⟹ c = d ⟹ Inl ` a ∪ Inr ` c = Inl ` b ∪ Inr ` d" by auto
show ?thesis
unfolding everything_impl_def everything_def set_map set_append set_remdups set_concat all_subterms_impl
by (rule cong, (force simp: initt)+)
qed
lemma generate_impl[simp]: "set (generate_impl U_impl t) = generate t"
proof (induct t rule: generate.induct)
case (1 ss f ts l r)
have "set (generate_impl U_impl (Inl (ss, Fun f ts, l, r))) =
set (gen_ac_impl U_impl ss f ts l r) ∪ set (gen_b_impl U_impl ss f ts l r)" (is "_ = ?ac ∪ ?b") by auto
also have "?b = gen_b ss f ts l r" by (auto simp: RR U_impl)
also have "?ac = gen_a ss f ts l r ∪ gen_c ss f ts l r"
by (force simp: U_impl RR)
finally
show ?case by auto
qed auto
lemma μ_approx_impl: assumes "μ_approx_impl = (fs,μ,info)"
shows "μ = μ_approx' ∧ (∀ f. f ∉ set fs ⟶ μ f = {})"
proof -
def fis ≡ "remdups
(concat (map (λentry. map (λfi. fi) (case entry of Inl x ⇒ [] | Inr fi ⇒ [fi]))
(inductive_set_impl everything_impl op = (generate_impl U_impl)
(map Inl initt))))"
note μ = assms[unfolded μ_approx_impl_def precompute_fun Let_def split, folded fis_def]
{
fix i f
assume f: "f ∉ set fs" and i: "i ∈ μ f"
from i have "(f,i) ∈ set fis" using μ by auto
with μ have "f ∈ set fs" by auto
with f have False by auto
}
moreover
{
fix f
from μ have μ: "μ f = {i . (f, i) ∈ set fis}" by auto
have "μ f = μ_approx' f"
unfolding μ fis_def μ_approx[unfolded check_approx_def]
unfolding set_remdups set_concat set_map
unfolding inductive_set_impl[OF everything_impl refl generate_impl]
unfolding set_map initt
by (cases f, auto)
}
hence "μ = μ_approx'" by auto
ultimately
show ?thesis by auto
qed
end
end
end
declare urm_computation.μ_approx_impl_code[code]
definition get_innermost_strict_repl_map_dpp where
"get_innermost_strict_repl_map_dpp I d S ≡ let
r = dpp_ops.rules I d;
p = dpp_ops.pairs I d;
isNF = dpp_ops.is_QNF I d;
U = inn_usable_rules_wf_dpp I d True;
ic = icap_impl_dpp I d
in urm_computation.μ_approx_impl r
[([s],t,lr) . (s,t) <- p, lr <- S]
(λ ss t. U (ss,t))
isNF ic
"
lemma get_innermost_strict_repl_map_dpp: assumes I: "dpp_spec I"
and inn: "NF_terms (set (dpp_ops.Q I d)) ⊆ NF_trs (set (dpp_ops.rules I d))"
and wfP: "wf_trs (set (dpp_ops.pairs I d))"
and wf: "wwf_qtrs (set (dpp_ops.Q I d)) (set (dpp_ops.rules I d))"
and S: "set S ⊆ (set (dpp_ops.rules I d))"
and res: "get_innermost_strict_repl_map_dpp I d S = (fs, μ, info)"
shows "⋀ f. f ∉ set fs ⟹ μ f = {}"
and "(s,t) ∈ set (dpp_ops.pairs I d) ⟹ s ⋅ σ ∈ NF_terms (set (dpp_ops.Q I d)) ⟹ usable_replacement_map μ {t ⋅ σ} (dpp_ops.nfs I d) (set (dpp_ops.rules I d)) (set (dpp_ops.Q I d)) (set S)"
proof -
interpret dpp_spec I by fact
let ?R = "set (rules d)"
let ?P = "set (pairs d)"
let ?nfs = "NFS d"
let ?Q = "set (Q d)"
let ?S = "set S"
note res = res[unfolded get_innermost_strict_repl_map_dpp_def Let_def]
let ?init = "concat (map (λ(s, t). map (λlr. ([s], t, lr)) S) (pairs d))"
let ?Init = "{([s],t,lr) | s t lr. (s,t) ∈ ?P ∧ lr ∈ ?S}"
let ?U = "(λss t. set (inn_usable_rules_wf_dpp I d True (ss, t)))"
have init: "set ?init = ?Init" by auto
from res have res: "urm_computation.μ_approx_impl (rules d) ?init
(λss t. inn_usable_rules_wf_dpp I d True (ss, t)) (λ t. t ∈ NF_terms ?Q) (icap_impl_dpp I d) =
(fs, μ, info)" by simp
from inn_usable_rules_wf_dpp_approx[OF I inn wf, of True]
have U: "usable_rules_approx ?Q ?R True ?U" by auto
from urm_computation.μ_approx_impl[OF refl init refl refl _ res, of icap',
unfolded icap_impl_dpp_icap[OF I]] icap'[of ?R ?Q]
have μ: "μ = μ_approx icap' ?R ?Q ?U ?Init" and fs: "⋀ f. f ∉ set fs ⟹ μ f = {}" by auto
show "⋀ f. f ∉ set fs ⟹ μ f = {}" by fact
assume P: "(s,t) ∈ set (dpp_ops.pairs I d)" and NF: "s ⋅ σ ∈ NF_terms (set (dpp_ops.Q I d))"
from P have mem: "{[s]} × {t} × ?S ⊆ ?Init" by auto
note urm = aprove_urm_for_DP[OF inn icap wf U S P NF mem wfP, of ?nfs]
from aprove_urm_for_DP[OF inn icap wf U S P NF mem wfP, of ?nfs, folded μ]
show "usable_replacement_map μ {t ⋅ σ} ?nfs ?R ?Q ?S" .
qed
fun get_innermost_strict_repl_map_rc where
"get_innermost_strict_repl_map_rc I d S (Derivational_Complexity F) = (full_empty (remdups (F @
usable_replacement_map.default_fs (tp_ops.rules I d))))"
| "get_innermost_strict_repl_map_rc I d S (Runtime_Complexity C D) = (
let r = tp_ops.rules I d in
if tp_ops.NFQ_subset_NF_rules I d ∧ set C ∩ set (defined_list r) ⊆ {}
then (let
isNF = tp_ops.is_QNF I d;
U = inn_usable_rules_wf_tp I d True;
ic = icap_impl_tp I d
in
urm_computation.μ_approx_impl r
[(xs,Fun f xs,lr) . (f,n) <- D, xs <- [map Var (x⇩1_to_x⇩n n)], lr <- S]
(λ ss t. U (ss,t))
isNF ic)
else
full_empty (remdups (C @ D @
usable_replacement_map.default_fs r)))
"
lemma get_innermost_strict_repl_map_rc: assumes I: "tp_spec I"
and wf: "wf_trs (set (tp_ops.rules I d))"
and S: "set S ⊆ (set (tp_ops.rules I d))"
and res: "get_innermost_strict_repl_map_rc I d S T = (fs, μ, info)"
shows "⋀ f. f ∉ set fs ⟹ μ f = {}"
and "usable_replacement_map μ (terms_of T) (tp_ops.nfs I d)
(set (tp_ops.rules I d)) (set (tp_ops.Q I d)) (set S)" (is ?goal)
proof -
interpret tp_spec I by fact
interpret usable_replacement_map "rules d" "Q d" undefined .
let ?R = "set (rules d)"
let ?nfs = "NFS d"
let ?Q = "set (Q d)"
let ?S = "set S"
{
assume "usable_replacement_map μ (terms_of T) ?nfs ?R ?Q ?R"
from usable_replacement_map_mono[OF subset_refl subset_refl S this]
have "usable_replacement_map μ (terms_of T) ?nfs ?R ?Q ?S" .
} note switch = this
have "?goal ∧ (∀ f. f ∉ set fs ⟶ μ f = {})"
proof (cases T)
case (Derivational_Complexity F)
note dc = this
from res[unfolded dc] have "full_empty (remdups (F @ usable_replacement_map.default_fs (rules d))) = (fs, μ, info)"
by auto
from full_empty[OF this _ _ wf, of T, unfolded dc]
show ?thesis
by (intro conjI switch, auto simp: dc)
next
case (Runtime_Complexity C D)
note rc = this
note res = res[unfolded rc get_innermost_strict_repl_map_rc.simps Let_def]
let ?test = "NFQ_subset_NF_rules d ∧ set C ∩ set (defined_list (rules d)) ⊆ {}"
show ?thesis
proof (cases ?test)
case False
with res have "full_empty (remdups (C @ D @ usable_replacement_map.default_fs (rules d))) = (fs, μ, info)"
by (auto split: if_splits)
note fe = full_empty[OF this _ _ wf, of T, unfolded rc]
show ?thesis
by (intro conjI switch, insert fe, auto simp: rc)
next
case True
hence "?test = True" by simp
note res = res[unfolded this if_True]
from True have inn: "NF_terms ?Q ⊆ NF_trs ?R" by auto
let ?init = "(concat (map (λ(f, n). concat (map (λxs. map (λlr. (xs, Fun f xs, lr)) S) [map Var (x⇩1_to_x⇩n n)])) D))"
let ?Init = "{(map Var (x⇩1_to_x⇩n n), Fun f (map Var (x⇩1_to_x⇩n n)),lr) | f n lr. (f,n) ∈ set D ∧ lr ∈ ?S}"
let ?U = "(λss t. set (inn_usable_rules_wf_tp I d True (ss, t)))"
have init: "set ?init = ?Init" by auto
from res have res: "urm_computation.μ_approx_impl (rules d) ?init
(λss t. inn_usable_rules_wf_tp I d True (ss, t)) (λ t. t ∈ NF_terms ?Q) (icap_impl_tp I d) =
(fs, μ, info)" by simp
from inn_usable_rules_wf_tp_approx[OF I inn wf_trs_imp_wwf_qtrs[OF wf], of True]
have U: "usable_rules_approx ?Q ?R True ?U" by auto
from urm_computation.μ_approx_impl[OF refl init refl refl _ res, of icap',
unfolded icap_impl_tp_icap[OF I]] icap'[of ?R ?Q]
have μ: "μ = μ_approx icap' ?R ?Q ?U ?Init" and fs: "⋀ f. f ∉ set fs ⟹ μ f = {}" by auto
show ?thesis
proof
show "usable_replacement_map μ (terms_of T) (NFS d) (set (rules d)) (set (Q d)) (set S)"
unfolding rc μ
by (rule aprove_urm_complexity[OF inn icap wf_trs_imp_wwf_qtrs[OF wf] U S],
insert True, auto)
qed (insert fs, auto)
qed
qed
thus "⋀ f. f ∉ set fs ⟹ μ f = {}" ?goal by auto
qed
definition get_innermost_strict_repl_map_rc_DP where
"get_innermost_strict_repl_map_rc_DP I d S T = (
let (fs,μ,info) = get_innermost_strict_repl_map_rc I d S T
in (case check_DP_complexity (tp_ops.rules I d) T of
Inr (RS, R', Cp, FS, F) ⇒ if set S ⊆ set RS then (list_inter fs Cp, λ f. if f ∈ set Cp then μ f else {}, info @ '' with DPs'') else (fs,μ,info)
| _ ⇒ (fs,μ,info)))"
lemma get_innermost_strict_repl_map_rc_DP: assumes I: "tp_spec I"
and wf: "wf_trs (set (tp_ops.rules I d))"
and S: "set S ⊆ (set (tp_ops.rules I d))"
and res: "get_innermost_strict_repl_map_rc_DP I d S T = (fs, μ, info)"
shows "⋀ f. f ∉ set fs ⟹ μ f = {}"
and "usable_replacement_map μ (terms_of T) (tp_ops.nfs I d)
(set (tp_ops.rules I d)) (set (tp_ops.Q I d)) (set S)" (is ?goal)
proof -
interpret tp_spec I by fact
let ?R = "set (rules d)"
let ?inn = "get_innermost_strict_repl_map_rc I d S T"
obtain fs' μ' info' where inn: "?inn = (fs',μ',info')" by (cases ?inn)
note res = res[unfolded get_innermost_strict_repl_map_rc_DP_def Let_def inn split]
note inn2 = get_innermost_strict_repl_map_rc[OF I wf S inn]
let ?check = "check_DP_complexity (rules d) T"
have "?goal ∧ (∀ f. f ∉ set fs ⟶ μ f = {})"
proof (cases "(fs,μ,info) = (fs',μ',info')")
case True
with inn2 show ?thesis by auto
next
case False
then obtain tuple where check: "?check = Inr tuple" using res by (cases ?check, auto)
obtain RS R' Cp FS F where tuple: "tuple = (RS, R', Cp, FS, F)" by (cases tuple)
from res[unfolded check tuple, simplified] False have S: "set S ⊆ set RS"
and fs: "fs = list_inter fs' Cp" and μ: "μ = (λf. if f ∈ set Cp then μ' f else {})"
by (auto split: if_splits)
from check_DP_complexity[OF check[unfolded tuple] wf]
have R: "?R = set RS ∪ set R'" and dp: "is_DP_complexity (set Cp) (set FS) (set F) (set RS) (set R') T"
by auto
have urm: "usable_replacement_map μ (terms_of T) (NFS d) ?R (set (Q d)) (set S)"
by (rule avanzini_14_34[OF inn2(2)[unfolded R] dp S, folded R], auto simp: μ)
show ?thesis
by (rule conjI[OF urm], auto simp: fs μ inn2(1))
qed
thus "⋀ f. f ∉ set fs ⟹ μ f = {}" ?goal by auto
qed
section ‹Processors›
definition show_position_set :: "'f × nat ⇒ nat set ⇒ shows" where
"show_position_set f s = shows_list [Suc i . i <- [0 ..< snd f], i ∈ s]"
definition
rule_shift_complexity_urm_tt ::
"('tp, 'f, string) tp_ops ⇒ ('f::{show,key}, string) redtriple ⇒ ('f,string)rules ⇒
('f,string)complexity_measure ⇒ complexity_class ⇒ 'tp proc"
where
"rule_shift_complexity_urm_tt I rp Rdelete 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 ;
Q = tp_ops.Q 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;
let (fs,μ,info) = get_innermost_strict_repl_map_rc_DP I tp Rdelete cm;
redtriple.valid rp;
(check_allm (λ f. check (μ f ⊆ redtriple.mono_af rp f)
(shows ''error in monotonicity: strict order for '' o shows f
o shows '' ensures monotonicity in positions '' o show_position_set f (redtriple.mono_af rp f)
o shows ''⏎but usable replacement map is ''
o show_position_set f (μ f))) fs) <+?
(λ s. s o shows ''⏎the computed usable replacement map ('' o shows info o shows '') is⏎'' o
shows_sep (λ f. shows ''mu('' o shows f o shows '') = '' o show_position_set f (μ f)) shows_nl fs
o shows ''⏎and mu(f) = {} for all other symbols f'');
check_allm (redtriple.s rp) Rdelete
<+? (λs. shows ''problem when orienting strict TRS⏎'' o s);
check_allm (redtriple.ns rp) (Rw @ R2)
<+? (λs. shows ''problem when orienting non-strict TRS⏎'' o s);
redtriple.cpx rp cm cc
<+? (λs. shows ''problem when ensuring complexity of order⏎'' o s)
} <+? (λs. shows ''could not derive the intended complexity '' o shows cc o shows '' from the following⏎'' o
(redtriple.desc rp) o shows_nl o s))
(tp_ops.mk I (tp_ops.nfs I tp) (tp_ops.Q I tp) R2 (list_union Rw Rdelete))"
lemma rule_shift_complexity_urm_tt:
assumes I: "tp_spec I"
and grp: "generic_redtriple_impl grp"
and res: "rule_shift_complexity_urm_tt I (grp rp) Rdelete 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_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 ?Q = "qrstep ?nfs (set (Q tp))"
let ?us = "get_innermost_strict_repl_map_rc_DP I tp Rdelete cm"
let ?pi = "mono_af (grp rp)"
obtain fs μ info where us: "?us = (fs,μ,info)" by (cases ?us)
note res = res[unfolded us, simplified]
from res have valid: "isOK (redtriple.valid ?rp)"
and S: "isOK(check_allm (redtriple.s ?rp) Rdelete)"
and NS: "isOK(check_allm (redtriple.ns ?rp) ?RwD)"
and af: "⋀ f. f ∈ set fs ⟹ μ f ⊆ ?pi f"
and wf: "wf_trs (set (rules tp))"
and subset: "set Rdelete ∪ (?Rw ∪ set ?D) ⊆ ?R ∪ ?Rw" "set Rdelete ⊆ ?R ∪ ?Rw" "set Rdelete ⊆ set (rules tp)"
by auto
have rules: "set (rules tp) = ?R ∪ ?Rw" by auto
note urm = get_innermost_strict_repl_map_rc_DP[OF I wf subset(3) us, unfolded rules]
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"
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 (?Q (?R - set Rdelete)) (?Q (?Rw ∪ set Rdelete))) cm cc" .
from res have cpx: "isOK (?cpx cc)" by auto
let ?Cpx = "λ cm cc. isOK(redtriple.cpx ?rp cm cc)"
from generate_redtriple[OF valid S NS, of Nil]
obtain S NS NST where "cpx_ce_af_redtriple_order S NS NST (redtriple.af ?rp) (redtriple.mono_af ?rp) ?Cpx"
and S: "set Rdelete ⊆ S" and NS: "?Rw ∪ set ?D ⊆ NS"
by auto
interpret cpx_ce_af_redtriple_order S NS NST "redtriple.af ?rp" "(redtriple.mono_af ?rp)" ?Cpx by fact
have bound1: "deriv_bound_measure_class (relto (?Q (set Rdelete)) (?Q (?Rw ∪ set ?D))) cm cc"
by (rule avanzini_14_10[OF S NS usable_replacement_map_mono[OF _ subset(1) _ urm(2)] af cpx], auto)
have bound: "deriv_bound_measure_class (relto (?Q (set Rdelete ∪ set ?D)) (?Q ?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 (?Q ?R) (?Q ?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
end