section ‹Weak Dependency Pairs›
theory WDP_Transformation
imports
TA.Multihole_Context
QTRS.Q_Restricted_Rewriting
begin
context sharp_syntax
begin
adhoc_overloading
SHARP "map (sharp_term shp)"
end
locale pre_wdps =
fixes shp :: "'f ⇒ 'f"
and 𝒞 :: "'f sig" -- ‹constructors and compound symbols›
begin
interpretation sharp_syntax .
abbreviation "ccap ≡ cap_till_funas (- 𝒞) :: ('f, 'v) term ⇒ _"
abbreviation "dmax ≡ uncap_till_funas (- 𝒞) :: ('f, 'v) term ⇒ _"
definition is_WDP_of :: "('f, 'a) rule ⇒ ('f, 'a) rule ⇒ bool"
where
"is_WDP_of p r ⟷
fst p = ♯ (fst r) ∧ (∃C. ground_mctxt C ∧ funas_mctxt C ⊆ 𝒞 ∧ snd p =⇩f (C, ♯(dmax (snd r))))"
end
locale wdps =
pre_wdps shp for shp :: "'f ⇒ 'f" +
fixes ℱ :: "'f sig" -- ‹signature›
and ℛ :: "('f, 'v) trs"
and 𝒬 :: "('f, 'v) terms"
and 𝒬' :: "('f, 'v) terms"
assumes sig_R: "funas_trs ℛ ⊆ ℱ"
and C_fresh: "({f. defined ℛ f} ∪ sharp_sig shp ℱ) ∩ 𝒞 = {}"
and wf_R: "wf_trs ℛ"
and Q': "𝒬' ⊆ 𝒬 ∪ {Fun f ts | f ts. (f, length ts) ∉ ℱ}"
begin
interpretation sharp_syntax shp .
abbreviation le_sharp :: "('f, 'v) term list ⇒ ('f, 'v) term list ⇒ bool" (infix "≤⇩♯" 50)
where
"xs ≤⇩♯ ys ≡ list_all2 (λx y. y = x ∨ y = ♯ x) xs ys"
definition good_for :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ bool" (infix "≪" 55)
where
"s ≪ t ⟷
(∃C ts. ground_mctxt C ∧ funas_mctxt C ⊆ 𝒞 ∧ funas_term s ⊆ ℱ ∧ dmax s ≤⇩♯ ts ∧ t =⇩f (C, ts))"
abbreviation "compose_ccap ≡ compose_cap_till_funas (- 𝒞) :: ('f, 'v) term ⇒ _"
lemma if_Fun_in_set [dest]:
"funas_term t ⊆ ℱ ⟹ if_Fun_in_set ℱ t"
by (cases t) (auto simp:)
lemma dmax_sharp_singleton [simp]:
assumes "funas_term t ⊆ ℱ" and "s ∈ set (dmax t)"
shows "dmax (♯ s) = [♯ s]"
proof -
from funas_uncap_till_subset and assms
have "funas_term s ⊆ ℱ" by blast
moreover from uncap_till and ‹s ∈ set (dmax t)›
have "if_Fun_in_set (- 𝒞) s" by blast
ultimately show ?thesis using C_fresh by (cases s) auto
qed
lemma le_sharp_dmax_singleton:
assumes "funas_term t ⊆ ℱ" and "dmax t ≤⇩♯ us" and "u ∈ set us"
shows "dmax u = [u]"
proof -
from assms(2-) obtain s where "s ∈ set (dmax t)"
and "u = s ∨ u = ♯ s" by (cases rule: list_all2_in_set2)
then show ?thesis
using assms(1) by (elim disjE) (simp_all add: uncap_till_singleton)
qed
lemma le_sharp_map_dmax_sharp [simp]:
assumes "funas_term t ⊆ ℱ" and "dmax t ≤⇩♯ us"
shows "map dmax us = map (λx. [x]) us"
using le_sharp_dmax_singleton [OF assms] by simp
lemma le_sharp_concat_map [simp]:
assumes "∀x ∈ set xs. f x ≤⇩♯ g x"
shows "concat (map f xs) ≤⇩♯ concat (map g xs)"
using assms by (induct xs) (auto intro: list_all2_appendI)
lemma le_sharp_refl [simp]:
"ts ≤⇩♯ ts"
by (metis (mono_tags, lifting) list_all2_all_nthI)
context
fixes R :: "('f, 'v) trs"
and WDP :: "('f, 'v) trs ⇒ ('f, 'v) trs"
assumes WDP: "∀r ∈ R. ∃p ∈ WDP R. is_WDP_of p r"
and "R ⊆ ℛ"
begin
lemma in_R:
"x ∈ R ⟹ x ∈ ℛ"
using ‹R ⊆ ℛ› by auto
lemma le_sharp_dmax_subst:
assumes "funas_term (t ⋅ σ) ⊆ ℱ"
shows "dmax (t ⋅ σ) ≤⇩♯ concat (map dmax (map (λs. s ⋅ σ) (♯(dmax t))))"
using assms
proof (induct t)
case (Fun f ts)
then have "∀t ∈ set ts. dmax (t ⋅ σ) ≤⇩♯ concat (map dmax (map (λs. s ⋅ σ) (♯(dmax t))))"
by fastforce
then have *: "concat (map (dmax ∘ (λs. s ⋅ σ)) ts) ≤⇩♯
concat (map (concat ∘ (map dmax ∘ (map (λs. s ⋅ σ) ∘ (♯ ∘ dmax)))) ts)" by simp
show ?case
proof (cases "(f, length ts) ∈ (- 𝒞)")
case True
with Fun.prems and C_fresh show ?thesis by auto
next
case False
then show ?thesis using * by (simp add: map_concat concat_concat_map)
qed
qed simp
lemma NF_terms_Q':
assumes "t ∈ NF_terms 𝒬" and "funas_term t ⊆ ℱ"
shows "t ∈ NF_terms 𝒬'"
proof
fix C l σ
assume [simp]: "t = C⟨l ⋅ σ⟩" and "l ∈ 𝒬'"
with Q' have "l ∈ 𝒬 ∨ l ∈ {Fun f ts | f ts. (f, length ts) ∉ ℱ}" by blast
then show False using assms by auto
qed
lemma NF_subst_Q':
assumes "⋃(funas_term ` σ ` vars_rule r) ⊆ ℱ" and "NF_subst nfs r σ 𝒬"
shows "NF_subst nfs r σ 𝒬'"
using assms and NF_terms_Q' by (auto simp add: NF_subst_def vars_rule_def UN_subset_iff)
lemma qrstep_good_for:
assumes "(s, t) ∈ qrstep nfs 𝒬 R" and "s ≪ u"
shows "∃v. t ≪ v ∧ (u, v) ∈ qrstep nfs 𝒬' (WDP R ∪ R)"
proof -
from assms obtain C l r σ
where args: "∀u ⊲ l ⋅ σ. u ∈ NF_terms 𝒬" and nfs: "NF_subst nfs (l, r) σ 𝒬"
and rule: "(l, r) ∈ R" and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩" by auto
then obtain f and n where root: "root (l ⋅ σ) = Some (f, n)" and "defined ℛ (f, n)"
using wf_R and sig_R
by (cases l, auto simp: wf_trs_def defined_def dest!: in_R) (metis root.simps(2))
then have "(f, n) ∈ - 𝒞" using C_fresh and sig_R by blast
from in_uncap_till_funas [OF root this s] obtain i and D
where i: "i < length (dmax s)" "dmax s ! i = D⟨l ⋅ σ⟩"
and C: "mctxt_of_ctxt C = compose_ccap s i (mctxt_of_ctxt D)" by blast
def ss⇩1 ≡ "take i (dmax s)"
def ss⇩2 ≡ "drop (Suc i) (dmax s)"
have [simp]: "length ss⇩1 = i" using i by (simp add: ss⇩1_def)
have dmax_s: "dmax s = ss⇩1 @ D⟨l ⋅ σ⟩ # ss⇩2"
using i by (auto simp: ss⇩1_def ss⇩2_def dest: id_take_nth_drop)
have "t =⇩f (compose_ccap s i (mctxt_of_ctxt D), [r ⋅ σ])"
using t unfolding C [symmetric] by (metis mctxt_of_ctxt)
from eqfE [OF this]
have "t =⇩f (ccap s, ss⇩1 @ D⟨r ⋅ σ⟩ # ss⇩2)"
using fill_holes_compose_cap_till [of i "if_Fun_in_set (- 𝒞)" s "mctxt_of_ctxt D" "[r ⋅ σ]"] and i
by (auto simp: ss⇩1_def ss⇩2_def)
from eqfE [OF this]
have t': "t = fill_holes (ccap s) (ss⇩1 @ D⟨r ⋅ σ⟩ # ss⇩2)"
and *: "num_holes (ccap s) = length (ss⇩1 @ D⟨r ⋅ σ⟩ # ss⇩2)" by simp_all
from ‹s ≪ u› obtain F and us
where us: "dmax s ≤⇩♯ us" and u_eqf: "u =⇩f (F, us)" and funas_s: "funas_term s ⊆ ℱ"
and F: "ground_mctxt F" "funas_mctxt F ⊆ 𝒞"
by (auto simp: good_for_def)
moreover then have "u = fill_holes F us" and "num_holes F = length us" by (auto dest: eqfE)
ultimately have dmax_u: "dmax u = us"
using uncap_till_funas_fill_holes_cancel [of _ _ "- 𝒞"] by simp
def us⇩1 ≡ "take i us"
def us⇩2 ≡ "drop (Suc i) us"
from us have le_sharp: "ss⇩1 ≤⇩♯ us⇩1" "ss⇩2 ≤⇩♯ us⇩2"
and shp: "us ! i = D⟨l ⋅ σ⟩ ∨ us ! i = ♯(D⟨l ⋅ σ⟩)"
using i by (auto simp: ss⇩1_def ss⇩2_def us⇩1_def us⇩2_def dest: list_all2_nthD)
have [simp]: "length us = length (dmax s)" using us by (simp add: list_all2_lengthD)
have [simp]: "length us⇩1 = i" "length us⇩2 = length ss⇩2"
using le_sharp by (auto dest: list_all2_lengthD)
have "dmax t = concat (map (dmax) (ss⇩1 @ D⟨r ⋅ σ⟩ # ss⇩2))" using * by (simp add: t')
also have "… = ss⇩1 @ dmax (D⟨r ⋅ σ⟩) @ ss⇩2"
by (simp add: ss⇩1_def ss⇩2_def drop_map [symmetric] take_map [symmetric])
(simp add: drop_map take_map)
finally have dmax_t: "dmax t = ss⇩1 @ dmax (D⟨r ⋅ σ⟩) @ ss⇩2" .
have funas_t: "funas_term t ⊆ ℱ"
using wf_R and sig_R and funas_s and rule
by (auto simp add: s t dest: funas_term_subst_rhs in_R)
then have "funas_ctxt C ⊆ ℱ" and "funas_term (r ⋅ σ) ⊆ ℱ"
by (simp_all add: t)
have "funas_term (D⟨l ⋅ σ⟩) ⊆ ℱ"
using funas_s and i and funas_uncap_till_subset [of "dmax s ! i" "if_Fun_in_set (- 𝒞)" s]
by (auto dest: nth_mem iff: subset_iff)
then have "funas_ctxt D ⊆ ℱ" and "funas_term (l ⋅ σ) ⊆ ℱ" by simp_all
with ‹funas_term (r ⋅ σ) ⊆ ℱ› have funas_i: "funas_term (D⟨r ⋅ σ⟩) ⊆ ℱ" by simp
have "∀u ⊲ l ⋅ σ. u ∈ NF_terms 𝒬'"
using args and NF_terms_Q' and ‹funas_term (l ⋅ σ) ⊆ ℱ› and supt_imp_funas_term_subset [of "l ⋅ σ"]
by (auto) (metis order_trans)
have "NF_subst nfs (l, r) σ 𝒬'"
using ‹funas_term (l ⋅ σ) ⊆ ℱ›
by (intro NF_subst_Q' [OF _ nfs])
(simp add: funas_term_subst vars_rule_lhs [OF wf_R in_R [OF rule]])
show ?thesis using shp
proof
assume us_i: "us ! i = ♯ (D⟨l ⋅ σ⟩)"
show ?thesis
proof (cases "D = □")
case False
with i and uncap_till [of "if_Fun_in_set (- 𝒞)" s]
have [simp]: "dmax (D⟨r ⋅ σ⟩) = [D⟨r ⋅ σ⟩]"
and [simp]: "ccap (D⟨r ⋅ σ⟩) = MHole"
by (case_tac [!] D) (force dest: nth_mem)+
let ?u = "♯ (D⟨r ⋅ σ⟩)"
def v ≡ "fill_holes (ccap u) (us⇩1 @ ?u # us⇩2)"
have **: "fill_holes (ccap u) (us⇩1 @ ?u # us⇩2) =⇩f (ccap u, us⇩1 @ ?u # us⇩2)"
by (auto simp: dmax_u dmax_s)
have "t ≪ v"
proof -
have "funas_mctxt (ccap u) ⊆ 𝒞"
using cap_till_funas [of _ u] by blast
moreover have "ground_mctxt (ccap u)" by auto
moreover have "funas_term t ⊆ ℱ" by fact
moreover have "v =⇩f (ccap u, us⇩1 @ ?u # us⇩2)"
using ** by (auto simp: v_def)
moreover have "dmax t ≤⇩♯ us⇩1 @ ?u # us⇩2"
using le_sharp by (auto simp: dmax_t intro: list_all2_appendI)
ultimately show ?thesis unfolding good_for_def by blast
qed
moreover
have "(u, v) ∈ qrstep nfs 𝒬' (WDP R ∪ R)"
proof -
from fill_holes_ctxt_main [of "ccap u" "us⇩1" "us⇩2"] obtain C
where [simp]: "⋀t. fill_holes (ccap u) (us⇩1 @ t # us⇩2) = C⟨t⟩"
using * by (auto simp: dmax_u)
have "u = fill_holes (ccap u) (us⇩1 @ ♯(D⟨l ⋅ σ⟩) # us⇩2)"
using fill_holes_cap_till_uncap_till_id [of "if_Fun_in_set (- 𝒞)" u]
and us_i and i and id_take_nth_drop [of i us]
by (simp add: dmax_u us⇩1_def us⇩2_def)
then have "u = (C ∘⇩c ♯ D)⟨l ⋅ σ⟩" using False by simp
have "v = fill_holes (ccap u) (us⇩1 @ ?u # us⇩2)" by (simp add: v_def)
then have "v = (C ∘⇩c ♯ D)⟨r ⋅ σ⟩" using False by simp
have "(l, r) ∈ WDP R ∪ R" using rule by blast
show ?thesis by (rule qrstepI) fact+
qed
ultimately
show ?thesis by blast
next
case True
obtain E and q
where wdp: "(♯ l, q) ∈ WDP R"
and E: "ground_mctxt E" "funas_mctxt E ⊆ 𝒞"
and "q =⇩f (E, ♯(dmax r))"
using WDP [THEN bspec, OF rule] by (auto simp: is_WDP_of_def)
then have q: "q = fill_holes E (♯(dmax r))"
and [simp]: "num_holes E = length (♯(dmax r))" by (auto dest: eqfE)
have [simp]: "♯(l ⋅ σ) = (♯ l) ⋅ σ"
using rule and wf_R by (cases l) (auto simp: wf_trs_def dest: in_R)
def v ≡ "fill_holes (ccap u) (us⇩1 @ q ⋅ σ # us⇩2)"
def vs ≡ "concat (map dmax (map (λs. s ⋅ σ) (♯(dmax r))))"
have "t ≪ v"
proof -
def Cs ≡ "map ccap (map (λs. s ⋅ σ) (♯(dmax r)))"
def C ≡ "compose_mctxt (ccap u) i (fill_holes_mctxt E Cs)"
have "funas_mctxt C ⊆ 𝒞"
using cap_till_funas [of "(- 𝒞)" u] and E and cap_till_funas [of "(- 𝒞)"]
and funas_uncap_till_subset [of _ "if_Fun_in_set (- 𝒞)" r]
and ‹funas_term (D⟨r ⋅ σ⟩) ⊆ ℱ›
by (auto simp: C_def True Cs_def) (case_tac "i = x", auto)+
moreover have "ground_mctxt C"
using i and E by (auto simp: C_def dmax_u Cs_def)
moreover have "funas_term t ⊆ ℱ" by fact
moreover have "v =⇩f (C, us⇩1 @ vs @ us⇩2)"
proof (unfold C_def dmax_t True ctxt_apply_term.simps map_append list.map, rule compose_mctxt_sound)
show "v =⇩f (ccap u, us⇩1 @ q ⋅ σ # us⇩2)" by (auto simp: v_def dmax_u dmax_s)
next
have "fill_holes E (map (λs. s ⋅ σ) (♯(dmax r))) =⇩f
(fill_holes_mctxt E Cs, vs)" (is "_ =⇩f (?C, vs)")
unfolding vs_def by (rule fill_holes_mctxt_sound) (auto simp: Cs_def split_term_eqf)
moreover
have "fill_holes E (map (λs. s ⋅ σ) (♯(dmax r))) = fill_holes E (♯(dmax r)) ⋅ σ"
using E by (auto simp: subst_apply_mctxt_fill_holes)
ultimately have "(fill_holes E (♯(dmax r))) ⋅ σ =⇩f (fill_holes_mctxt E Cs, vs)"
unfolding vs_def by auto
then show "q ⋅ σ =⇩f (fill_holes_mctxt E Cs, vs)" by (simp add: q)
next
show "i = length us⇩1" by simp
qed
moreover have "dmax t ≤⇩♯ us⇩1 @ vs @ us⇩2"
proof -
have "dmax (D⟨r ⋅ σ⟩) ≤⇩♯ vs"
using ‹funas_term (D⟨r ⋅ σ⟩) ⊆ ℱ›
using le_sharp_dmax_subst [of r σ] by (simp add: vs_def True)
then show ?thesis using le_sharp by (auto simp: dmax_t intro!: list_all2_appendI)
qed
ultimately show ?thesis unfolding good_for_def by blast
qed
moreover have "(u, v) ∈ qrstep nfs 𝒬' (WDP R ∪ R)"
proof -
obtain C where C: "⋀s. fill_holes (ccap u) (us⇩1 @ s # us⇩2) = C⟨s⟩"
using fill_holes_ctxt_main [of "ccap u" "us⇩1" "us⇩2"] by (auto simp: dmax_u dmax_s)
have u: "u = fill_holes (ccap u) (dmax u)"
by (metis fill_holes_cap_till_uncap_till_id)
have "(u, v) ∈ qrstep nfs 𝒬' (WDP R)"
proof (rule qrstepI [OF _ wdp, of σ 𝒬' u _ v nfs])
show "∀u ⊲ ♯ l ⋅ σ. u ∈ NF_terms 𝒬'"
using args and ‹funas_term (l ⋅ σ) ⊆ ℱ› by (force intro!: NF_terms_Q')
next
have "(⋃t ∈ set (dmax r). vars_term t) ⊆ vars_term r"
by (induct r) auto
then have *: "(⋃t ∈ set (dmax r). vars_term t) ⊆ vars_term l"
using in_R [OF rule] and wf_R by (auto simp: wf_trs_def)
then have "NF_subst nfs (♯ l, q) σ 𝒬"
using nfs and E by (auto simp: q NF_subst_def vars_defs)
moreover have "⋃(funas_term ` σ ` vars_rule (♯ l, q)) ⊆ ℱ"
using E and * and ‹funas_term (l ⋅ σ) ⊆ ℱ›
by (auto simp add: vars_defs q funas_term_subst dest!: contra_subsetD iff: SUP_le_iff)
ultimately show "NF_subst nfs (♯ l, q) σ 𝒬'" by (intro NF_subst_Q') simp_all
next
have "u =⇩f (ccap u, us⇩1 @ ♯ l ⋅ σ # us⇩2)"
using i and us_i
apply (subst u)
apply (auto simp: dmax_u dmax_s True)
by (metis ‹length us = length (dmax s)› dmax_u eq_fill.intros i(1) id_take_nth_drop num_holes_cap_till us⇩1_def us⇩2_def)
then show "u = C⟨♯ l ⋅ σ⟩" using C [of "♯ l ⋅ σ"] by (auto dest: eqfE)
next
have "v =⇩f (ccap u, us⇩1 @ q ⋅ σ # us⇩2)"
by (auto simp: v_def True dmax_s dmax_u)
then show "v = C⟨q ⋅ σ⟩" using C [of "q ⋅ σ"] by (auto dest: eqfE)
qed
then show ?thesis by blast
qed
ultimately show ?thesis by blast
qed
next
assume us_i: "us ! i = D⟨l ⋅ σ⟩"
have us': "us⇩1 @ D⟨l ⋅ σ⟩ # us⇩2 = us"
by (metis ‹length us = length (dmax s)› ‹length us⇩1 = i› append_eq_conv_conj Cons_nth_drop_Suc i(1) us⇩1_def us⇩2_def us_i)
have "i < length us" by (simp add: dmax_s)
let ?D = "ccap (D⟨r ⋅ σ⟩)"
let ?u = "dmax (D⟨r ⋅ σ⟩)"
def G ≡ "compose_mctxt (ccap u) i ?D"
def v ≡ "fill_holes G (us⇩1 @ ?u @ us⇩2)"
have **: "fill_holes (ccap u) (us⇩1 @ D⟨r ⋅ σ⟩ # us⇩2) =⇩f (G, us⇩1 @ ?u @ us⇩2)"
proof (unfold G_def, rule compose_mctxt_sound [OF _ split_term_eqf])
show "fill_holes (ccap u) (us⇩1 @ D⟨r ⋅ σ⟩ # us⇩2) =⇩f (ccap u, us⇩1 @ D⟨r ⋅ σ⟩ # us⇩2)"
by (auto simp: dmax_u dmax_s)
next
show "i = length us⇩1" by simp
qed
then have "v =⇩f (G, us⇩1 @ ?u @ us⇩2)" by (auto simp: v_def dest: eqfE)
moreover have "dmax t ≤⇩♯ us⇩1 @ ?u @ us⇩2"
using le_sharp by (auto simp: dmax_t intro!: list_all2_appendI)
moreover have "ground_mctxt G" by (auto simp: G_def)
moreover
have "funas_mctxt G ⊆ 𝒞"
unfolding G_def
unfolding funas_mctxt_compose_mctxt [of i "ccap u" ?D, unfolded num_holes_cap_till dmax_u, OF ‹i < length us›]
using cap_till_funas [of "(- 𝒞)" u] and cap_till_funas [of "(- 𝒞)"]
and funas_cap_till_subset [of "if_Fun_in_set (- 𝒞)" "D⟨r ⋅ σ⟩"]
and ‹funas_term (D⟨r ⋅ σ⟩) ⊆ ℱ›
by blast
moreover
have "(u, v) ∈ qrstep nfs 𝒬' (WDP R ∪ R)"
proof -
from fill_holes_ctxt_main [of "ccap u" us⇩1 us⇩2] obtain C
where [simp]: "⋀t. fill_holes (ccap u) (us⇩1 @ t # us⇩2) = C⟨t⟩"
using * by (auto simp: dmax_u)
have "u = fill_holes (ccap u) (us⇩1 @ D⟨l ⋅ σ⟩ # us⇩2)"
using fill_holes_cap_till_uncap_till_id [of "if_Fun_in_set (- 𝒞)" u]
and us_i and i
unfolding dmax_u by (simp add: us')
then have "u = (C ∘⇩c D)⟨l ⋅ σ⟩" by simp
have "v = fill_holes (ccap u) (us⇩1 @ D⟨r ⋅ σ⟩ # us⇩2)"
using ** by (auto simp: v_def dest: eqfE)
then have "v = (C ∘⇩c D)⟨r ⋅ σ⟩" by simp
have "(u, v) ∈ qrstep nfs 𝒬' R" by (rule qrstepI) fact+
then show ?thesis by (metis UnI2 qrstep_union)
qed
moreover have "funas_term t ⊆ ℱ" by fact
ultimately
show ?thesis unfolding good_for_def by blast
qed
qed
end
context
fixes S W :: "('f, 'v) trs"
and WDP_S :: "('f, 'v) trs"
and WDP_W :: "('f, 'v) trs"
assumes WDP_S: "∀r ∈ S. ∃p ∈ WDP_S. is_WDP_of p r"
and WDP_W: "∀r ∈ W. ∃p ∈ WDP_W. is_WDP_of p r"
and S: "S ⊆ ℛ"
and W: "W ⊆ ℛ"
begin
lemma rel_qrsteps_good_for:
assumes steps: "(s, t) ∈ (relto (qrstep nfs 𝒬 S) (qrstep nfs 𝒬 W)) ^^ n" (is "_ ∈ ?R ^^ n")
and good: "s ≪ u"
shows "∃v. t ≪ v ∧ (u, v) ∈ (relto (qrstep nfs 𝒬' (WDP_S ∪ S)) (qrstep nfs 𝒬' (WDP_W ∪ W))) ^^ n"
by (rule simulate_conditional_relative_steps_count[of "λ s t. s ≪ t",
OF qrstep_good_for[OF WDP_S S] qrstep_good_for[OF WDP_W W] steps good])
lemma WDPs_sound:
assumes bound: "deriv_bound_measure_class
(relto (qrstep nfs 𝒬' (WDP_S ∪ S)) (qrstep nfs 𝒬' (WDP_W ∪ W)))
(Runtime_Complexity C' D'') cc"
and D': "set D' ∩ 𝒞 = {}"
and CD'_F: "set C' ∪ set D' ⊆ ℱ"
and D'': "set D'' = ♯(set D')"
shows "deriv_bound_measure_class
(relto (qrstep nfs 𝒬 S) (qrstep nfs 𝒬 W))
(Runtime_Complexity C' D') cc"
proof -
let ?D = "relto (qrstep nfs 𝒬' (WDP_S ∪ S)) (qrstep nfs 𝒬' (WDP_W ∪ W))"
let ?R = "relto (qrstep nfs 𝒬 S) (qrstep nfs 𝒬 W)"
let ?T = "terms_of_nat (Runtime_Complexity C' D')"
let ?TS = "terms_of_nat (Runtime_Complexity C' D'')"
note d = deriv_bound_measure_class_def deriv_bound_rel_class_def
note d' = deriv_bound_rel_def
note d'' = deriv_bound_def
from bound [unfolded d] obtain f where
f: "f ∈ O_of cc" and bound: "deriv_bound_rel ?D ?TS f" by blast
show ?thesis unfolding d
proof (intro exI [of _ f] conjI [OF f], unfold d' d'', clarify)
fix n s t
assume sT: "s ∈ ?T n" and st: "(s, t) ∈ ?R ^^ Suc (f n)"
from sT CD'_F have sF: "funas_term s ⊆ ℱ"
by (cases s) (auto simp: funas_args_term_def)
from relpow_Suc_E2 [OF st] obtain u where "(s, u) ∈ ?R" by metis
then have "(s, u) ∈ (qrstep nfs 𝒬 (S ∪ W))⇧+" unfolding qrstep_union by regexp
then obtain u where "(s, u) ∈ qrstep nfs 𝒬 (S ∪ W)" by (induct, auto)
with S W qrstep_all_mono [OF _ subset_refl, of "S ∪ W" ℛ 𝒬 nfs nfs]
have su: "(s, u) ∈ qrstep nfs 𝒬 ℛ" by auto
from sT obtain g ss where [simp]: "s = Fun g ss" and "(g, length ss) ∈ set D'"
by (cases s) simp_all
then have *: "dmax s = [Fun g ss]" using D' by (auto)
have ss: "♯ s ∈ ?TS n"
using sT by (cases s) (auto simp: D'' funas_args_term_def)
have "s ≪ ♯ s"
unfolding good_for_def and *
by (rule exI [of _ MHole], rule exI [of _ "[♯ s]"], insert sF) auto
from rel_qrsteps_good_for [OF st this] obtain v
where "(♯ s, v) ∈ ?D ^^ Suc (f n)" by auto
from deriv_bound_steps [OF this bound [unfolded d', rule_format, OF ss]]
show False by simp
qed
qed
end
end
end