section ‹Dependency Tupel Transformation›
theory DT_Transformation
imports
QTRS.Q_Relative_Rewriting
TA.Multihole_Context
QTRS.Complexity
begin
locale pre_innermost_wf =
fixes D :: "'f sig"
and R :: "('f, 'v) trs"
and Q :: "('f, 'v) terms"
begin
abbreviation "rew ≡ qrstep False Q R"
abbreviation "rew_r_p_s ≡ qrstep_r_p_s False Q R"
abbreviation step (infix "→" 55)
where
"step s t ≡ (s, t) ∈ rew"
definition DPos :: "('f, 'v) term ⇒ pos set"
where
"DPos s = {p. p ∈ poss s ∧ (∃ f ∈ D. root (s |_ p) = Some f)}"
definition RPos :: "('f, 'v) term ⇒ pos set"
where
"RPos s = {p. p ∈ DPos s ∧ (∃ u. s |_ p → u)}"
lemma RPos_subseteq_DPos: "RPos s ⊆ DPos s" by (auto simp: RPos_def)
lemma DPos_subseteq_funposs:
"DPos s ⊆ funposs s"
proof
fix p
assume "p ∈ DPos s"
then obtain f and n where "root (s |_ p) = Some (f, n)"
and "p ∈ (funposs s ∪ varposs s)" by (auto simp: DPos_def varposs_iff)
moreover then have "p ∉ varposs s" by (auto simp: varposs_iff)
ultimately show "p ∈ funposs s" by blast
qed
end
locale innermost_wf =
pre_innermost_wf D R Q for D :: "'f sig" and R :: "('f, 'v) trs" and Q :: "('f, 'v) terms" +
assumes defs_R: "{fn. defined R fn} ⊆ D"
and wf_R: "wf_trs R"
and innermost: "NF_terms Q ⊆ NF_trs R"
begin
lemma rew_r_p_s_imp_NF_subst:
assumes "(s, t) ∈ rew_r_p_s lr p σ"
and "x ∈ vars_rule lr"
shows "σ x ∈ NF_trs R"
proof -
let ?l = "fst lr"
have "lr ∈ R" using assms(1)[unfolded qrstep_r_p_s_def] by auto
with assms(2) wf_R[unfolded wf_trs_def'] obtain f ls where
l: "?l = Fun f ls" and x: "x ∈ vars_term ?l"
by (force simp: vars_rule_def)+
have "σ x ∈ NF_terms Q" unfolding l using
subst_image_subterm[OF x[unfolded l], of σ] assms(1)[unfolded qrstep_r_p_s_def] l by auto
thus ?thesis using innermost by auto
qed
lemma step_at_DPos:
assumes "(s,t) ∈ rew_r_p_s lr p σ"
shows "p ∈ DPos s"
proof -
obtain l r where [simp]: "lr = (l,r)" by force
from assms[unfolded qrstep_r_p_s_def] have lr: "(l,r) ∈ R" by auto
from wf_trs_imp_lhs_Fun[OF wf_R lr] obtain f ls where l: "l = Fun f ls" by blast
from assms(1)[unfolded qrstep_r_p_s_def] obtain σ where
s_p: "s |_ p = l ⋅ σ" by auto
have rt_s_p: "root (s |_ p) = root l" unfolding l s_p by auto
obtain f where "root (s |_ p) = Some f" and "f ∈ D"
unfolding rt_s_p
using lr defs_R[unfolded defined_def] unfolding l by fastforce
thus ?thesis unfolding DPos_def l using qrstep_r_p_s_conv(1)[OF assms(1)] by force
qed
lemma step_at_RPos:
assumes "(s,t) ∈ rew_r_p_s lr p σ"
shows "p ∈ RPos s"
unfolding RPos_def
proof (auto)
from step_at_DPos[OF assms] show p_in_dposs_s: "p ∈ DPos s".
from qrstep_subt_at[OF assms] have "s |_ p → t |_ p"
using qrstep_qrstep_r_p_s_conv by blast
thus "∃ u. s |_ p → u" by auto
qed
lemma RPos_step_approx:
assumes pstep: "(s,t) ∈ rew_r_p_s lr p σ"
shows "RPos t ⊆ {q. q ∈ RPos s ∧ (q < p ∨ q ⊥ p)} ∪ {p <#> q | q. q ∈ DPos (snd lr)}" (is "_ ⊆ ?old ∪ ?fresh")
proof
let ?l = "fst lr"
let ?r = "snd lr"
fix q
assume *: "q ∈ RPos t"
show "q ∈ ?old ∪ ?fresh"
proof -
have p_in_poss_s: "p ∈ poss s" and p_in_poss_t : "p ∈ poss t" and shape_s: "s = replace_at s p (?l ⋅ σ)"
using qrstep_r_p_s_conv[OF pstep] by auto
have t_p: "t |_ p = ?r ⋅ σ" using subt_at_ctxt_of_pos_term[OF _ p_in_poss_t] qrstep_r_p_s_conv[OF pstep] by auto
from *[unfolded RPos_def] obtain u where
qstep: "t|_q → u" and
q_in_DPos_t: "q ∈ DPos t"
by auto
then have q_in_poss_t: "q ∈ poss t" unfolding DPos_def by auto
from q_in_DPos_t have q_in_funnpos_t: "q ∈ funposs t" using DPos_subseteq_funposs by auto
{
assume le: "p ≤ q"
obtain p' where p': "q = p <#> p'" using prefix_pos_diff[OF le,symmetric] by auto
hence
t_q: "t |_ q = ?r ⋅ σ |_ p'"
and p'_in_poss_rsigma: "p' ∈ poss (?r ⋅ σ)"
using subterm_poss_conv[OF q_in_poss_t p' t_p] by auto
{
assume p'_notin_funposs_r: "p' ∉ funposs ?r"
obtain p1 p2 x
where p'_decomposed: "p' = p1 <#> p2"
and p1_in_poss_r: "p1 ∈ poss ?r"
and p1_varposs: "?r |_ p1 = Var x"
and p2_in_subst: "p2 ∈ poss (σ x)"
using poss_subst_apply_term[OF p'_in_poss_rsigma p'_notin_funposs_r].
have t_q_in_subst: "σ x ⊵ t |_ q"
unfolding t_q p'_decomposed
subt_at_append[OF poss_imp_subst_poss[OF p1_in_poss_r]]
subt_at_subst[OF p1_in_poss_r]
p1_varposs
using subt_at_imp_supteq[OF p2_in_subst] by auto
have "x ∈ vars_rule lr"
using subt_at_imp_supteq[OF p1_in_poss_r, unfolded p1_varposs] subteq_Var_imp_in_vars_term
unfolding vars_rule_def by force
then have "(σ x) ∈ NF_trs R" using rew_r_p_s_imp_NF_subst[OF pstep, of x] by auto
from NF_subterm[OF this t_q_in_subst] have "t |_q ∈ NF_trs R".
then have t_q_nf: "t |_ q ∈ NF (qrstep False Q R)"
using NF_anti_mono[OF qrstep_subset_rstep] innermost by force
from NF_no_step[OF t_q_nf] qstep have False by blast
}
hence p'_in_funposs_r: "p' ∈ funposs ?r" by auto
have p'_in_poss_r: "p' ∈ poss ?r" using funposs_imp_poss[OF p'_in_funposs_r].
from funposs_fun_conv[OF p'_in_funposs_r] obtain f ts where rp': "?r |_ p' = Fun f ts" by auto
let ?root = "root (?r |_ p')"
from rp' have "?root = root(?r |_ p' ⋅ σ)" unfolding rp' by simp
also have "... = root(t |_ q)" unfolding t_q using p'_in_poss_r by simp
finally have rt_r_p': "?root = root(t |_ q)" .
then obtain f n where "?root = Some (f,n)" and "(f,n) ∈ D" using
q_in_DPos_t[unfolded DPos_def] q_in_poss_t by auto
then have "p' ∈ DPos ?r" unfolding DPos_def using p'_in_poss_r by auto
then have ?thesis using p' by auto
}
note q_geq_p = this
{
assume p_gt_q: "p > q"
then obtain p' where p' : "p = q <#> p'" and ne: "p' ≠ ε" using less_pos_def' by auto
have step_at_q: "(s |_ q, t |_ q) ∈ nrqrstep False Q R"
using qrstep_r_p_s_imp_nrqrstep[OF qrstep_subt_at_gen[OF pstep[unfolded p']] ne] .
from nrqrstep_preserves_root[OF this]
obtain f n where
"root (s |_ q) = Some (f,n)" and
"(f,n) ∈ D"
using q_in_poss_t q_in_DPos_t[unfolded DPos_def] by auto
hence "q ∈ DPos s" unfolding DPos_def
using poss_append_poss p_in_poss_s[unfolded p'] by auto
then have "q ∈ ?old" using step_at_q
unfolding RPos_def
using qrstep_iff_rqrstep_or_nrqrstep p_gt_q
by blast
then have ?thesis by auto
}
note p_gt_q = this
{
assume p_par_q: "p ⊥ q"
have q_in_poss_s: "q ∈ poss s" unfolding shape_s[unfolded qrstep_r_p_s_conv(6)[OF pstep, symmetric]]
using parallel_poss_replace_at[OF p_par_q p_in_poss_t] q_in_poss_t by auto
have "s |_ q = t |_ q" using parallel_qrstep_subt_at[OF pstep p_par_q q_in_poss_s] by auto
then obtain f n where
"root(s |_ q) = Some (f,n)"
and "(f,n) ∈ D"
and step_q: "s |_ q → u"
using *[unfolded RPos_def DPos_def] qstep by auto
then have "q ∈ DPos s"using q_in_poss_s unfolding DPos_def by blast
then have ?thesis using step_q parallel_pos_sym[OF p_par_q] unfolding RPos_def by blast
}
note q_par_q = this
show ?thesis using q_geq_p p_gt_q q_par_q position_cases by auto
qed
qed
end
locale pre_DT_trans =
sharp_syntax shp +
pre_innermost_wf D R Q
for shp :: "'f ⇒ 'f" and D :: "'f sig" and R :: "('f, 'v) trs" and Q :: "('f, 'v) terms" +
fixes F :: "'f sig"
and Ds :: "'f sig"
begin
definition is_DT_of :: "('f, 'v) rule ⇒ ('f, 'v) rule ⇒ bool"
where
"is_DT_of lr uv ⟷
fst uv = ♯(fst lr) ∧ (∃ C qs. snd uv =⇩f (C, [♯(snd lr |_ q). q ← qs]) ∧ set qs = DPos (snd lr))"
definition goodFor :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ bool" (infix "≪" 55)
where
"goodFor t u ⟷ (∃ C ps. u =⇩f (C, [♯(t |_ p). p ← ps]) ∧ RPos t = set ps ∧ funas_term t ⊆ F)"
end
locale DT_trans =
innermost_wf D R Q +
pre_DT_trans shp D R Q F Ds for D :: "'f sig"
and R :: "('f, 'v) trs"
and Q :: "('f, 'v) terms"
and F :: "'f sig"
and shp :: "'f ⇒ 'f"
and Ds :: "'f sig"
and Q' :: "('f, 'v) terms" +
assumes [simp]: "Ds = ♯ D"
and R_sig: "funas_trs R ⊆ F"
and D_subseteq_F: "D ⊆ F"
and Ds_fresh: "Ds ∩ F = {}"
and Q': "Q' ⊆ Q ∪ { Fun f ts | f ts. (f, length ts) ∉ F }"
begin
abbreviation "rew_r_p_s' ≡ qrstep_r_p_s False Q' R"
abbreviation "rew' ≡ qrstep False Q' R"
lemma NF_termsQ'I:
assumes sQ: "s ∈ NF_terms Q" and sF: "funas_term s ⊆ F"
shows "s ∈ NF_terms Q'"
proof -
let ?Q' = "{Fun f ts |f ts. (f, length ts) ∉ F}"
have sQ': "s ∈ NF_terms ?Q'"
proof
fix C l and σ :: "('f,'v)subst"
assume s: "s = C⟨l ⋅ σ⟩" and l: "l ∈ ?Q'"
from sF[unfolded s] have "funas_term l ⊆ F" by (auto simp: funas_term_subst)
with l show False by (cases l, auto)
qed
have s: "s ∈ NF_terms (Q ∪ ?Q')"
unfolding NF_trs_union Id_on_union using sQ' sQ by auto
show ?thesis by (rule set_mp[OF NF_trs_mono s], insert Q', auto)
qed
lemma rew_r_p_s'I:
assumes st: "(s, t) ∈ rew_r_p_s lr p σ"
and F: "p ∈ poss s ⟹ ⋃ (funas_term ` set (args (s |_ p))) ⊆ F"
shows "(s, t) ∈ rew_r_p_s' lr p σ"
proof -
obtain l r where lr: "lr = (l,r)" by force
note d = qrstep_r_p_s_def
from st[unfolded d lr]
have Q: "(∀u⊲l ⋅ σ. u ∈ NF_terms Q)" and p: "p ∈ poss s" and lr': "(l, r) ∈ R" and id: "s |_ p = l ⋅ σ"
and t: "t = (ctxt_of_pos_term p s)⟨r ⋅ σ⟩" by auto
{
fix u
assume u: "u ∈ set (args (s |_ p))"
let ?Q' = "{Fun f ts |f ts. (f, length ts) ∉ F}"
from u Q[folded id NF_terms_args_conv] have Q: "u ∈ NF_terms Q" by auto
from u F[OF p] have F: "funas_term u ⊆ F" by auto
have "u ∈ NF_terms Q'"
by (rule NF_termsQ'I[OF Q F])
}
hence "∀u∈set (args (s |_ p)). u ∈ NF_terms Q'" by auto
from this[unfolded id NF_terms_args_conv] p lr' id t
show ?thesis unfolding d lr by auto
qed
lemma funas_sharp_term: "funas_term ` set (args (♯ s)) = funas_term ` set (args s)"
by (cases s, auto)
lemma rew_r_p_s'I_full:
assumes st: "(s,t) ∈ rew_r_p_s lr p σ"
and F: "⋃ (funas_term ` set (args s)) ⊆ F"
shows "(s,t) ∈ rew_r_p_s' lr p σ"
proof (rule rew_r_p_s'I[OF st subset_trans[OF _ F]], intro subsetI)
fix f
assume p: "p ∈ poss s"
and f: "f ∈ ⋃(funas_term ` set (args (s |_ p)))"
show "f ∈ ⋃(funas_term ` set (args s))"
proof (cases p)
case Empty
thus ?thesis using f by auto
next
case (PCons i q)
with p obtain g ss where s: "s = Fun g ss" and i: "i < length ss" and q: "q ∈ poss (ss ! i)"
by (cases s, auto)
hence mem: "ss ! i ∈ set (args s)" by auto
from PCons have "s |_ p = ss ! i |_ q" unfolding s by simp
from f[unfolded this]
obtain t where "t ∈ set (args (ss ! i |_ q))" and f: "f ∈ funas_term t" by auto
then obtain g ts where sp: "ss ! i |_ q = Fun g ts" and t: "t ∈ set ts" by (cases "ss ! i |_ q", auto)
from ctxt_supt_id[OF q] obtain C where s: "ss ! i = C ⟨ ss ! i |_ q ⟩" by metis
from this[unfolded sp] t f have "f ∈ funas_term (ss ! i)" by auto
with mem show ?thesis by auto
qed
qed
subsection ‹Tuple Transformation›
lemma nrqrstep_r_p_s_imp_sharp_qrstep_r_p_s:
assumes ne: "p ≠ ε"
and step: "(s, t) ∈ rew_r_p_s lr p σ"
shows "(♯ s, ♯ t) ∈ rew_r_p_s lr p σ"
proof -
let ?C = "ctxt_of_pos_term p s"
from qrstep_r_p_s_conv[OF step] have s: "s = ?C⟨fst lr⋅σ⟩" and t: "t = ?C⟨snd lr⋅σ⟩" and p: "p ∈ poss s" by auto
from ne obtain f D bef aft where C: "?C = More f bef D aft"
using hole_pos_ctxt_of_pos_term[OF p] ctxt_to_term_list.cases hole_pos.simps(1) by metis
from s t have s: "s = Fun f (bef @ D⟨fst lr⋅σ⟩ # aft)" and t: "t = Fun f (bef @ D⟨snd lr⋅σ⟩ # aft)" unfolding C ctxt_apply_term.simps(2) by auto
let ?C' = "More (♯ f) bef D aft"
from hole_pos_ctxt_of_pos_term[OF p, unfolded C] have hole_pos_C': "hole_pos ?C' = p" by simp
from s t have
s_sharp: "♯ s = ?C'⟨fst lr⋅σ⟩" and
t_sharp: "♯ t = ?C'⟨snd lr⋅σ⟩" by simp+
moreover have "ctxt_of_pos_term p (♯ s) = ?C'" using s_sharp hole_pos_C' by fastforce
moreover have "♯ s |_ p = fst lr ⋅ σ" and "♯ t |_ p = snd lr ⋅ σ"
unfolding s_sharp t_sharp using hole_pos_C' subt_at_hole_pos by auto
moreover from hole_pos_C' have "p ∈ poss (♯ s)" unfolding s_sharp using hole_pos_in_possc by auto
ultimately show ?thesis using step unfolding qrstep_r_p_s_def by auto
qed
lemma step_to_dt_step:
assumes step: "(s, t) ∈ qrstep_r_p_s False Q'' R lr p σ"
and dt: "is_DT_of lr uv"
obtains C t' qs where
"t' =⇩f(C, [♯(t |_ (p <#> q)) . q ← qs])" and
"set qs = DPos (snd lr)" and
"(♯(s |_ p), t') ∈ qrstep False Q'' {uv}"
proof -
let ?C = "ctxt_of_pos_term p s"
let ?r = "snd lr"
from qrstep_r_p_s_conv[OF step] replace_at_subt_at
have s_p: "s |_ p = fst lr ⋅ σ" and t_p: "t |_ p = ?r ⋅ σ" by metis+
from dt[unfolded is_DT_of_def] have u: "fst uv = ♯ (fst lr)" by auto
have "lr ∈ R" using step[unfolded qrstep_r_p_s_def] by auto
hence wf_l: "is_Fun (fst lr)" using wf_R[unfolded wf_trs_def]
unfolding wf_rule_def by (metis is_FunI surjective_pairing)
hence u_match: "♯ (s |_ p) = fst uv ⋅ σ" proof (cases "fst lr", insert s_p u, auto) qed
from dt[unfolded is_DT_of_def] obtain C qs where
v: "snd uv =⇩f (C,[♯ (?r |_ q) . q ← qs])" (is "snd uv =⇩f (C,?us)") and
qs: "set qs = DPos ?r"
by auto
from wf_l step[unfolded qrstep_r_p_s_def] u have
NF: "∀u⊲ fst uv ⋅ σ. u ∈ NF_terms Q''" proof (cases "fst lr", auto) qed
from qrstep.subst[OF this] NF_subst_False
have dp_step: "(♯ (s |_ p), fill_holes C ?us ⋅ σ) ∈ qrstep False Q'' {uv}"
unfolding u_match eqfE(1)[OF v, symmetric]
using insertI1 surjective_pairing by auto
{
fix q
assume q_in_qs: "q ∈ set qs"
have q_in_fun_r: "q ∈ funposs ?r"
using in_mono[OF DPos_subseteq_funposs] q_in_qs[unfolded qs] by auto
have "(?r |_ q) ⋅ σ = t|_(p <#> q)"
using subt_at_subst[OF funposs_imp_poss[OF q_in_fun_r], symmetric, of σ]
unfolding t_p[symmetric] subt_at_append[OF ‹p ∈ poss t›] by auto
then have "♯ (?r |_ q) ⋅ σ = ♯ (t|_(p <#> q))"
using funposs_fun_conv[OF q_in_fun_r] by auto
} then have "⋀ q. q ∈ set qs ⟶ (λ x . ♯ (?r |_ x) ⋅ σ) q = (λ x . ♯ (t|_(p <#> x))) q" by metis
from subst_apply_mctxt_sound[OF v, of σ, unfolded map_map o_def map_ext[OF this]] qs dp_step that
eqfE(1)[OF v] show ?thesis by auto
qed
lemma subseq_map_same:
assumes "subseq xs ys"
and "∀x ∈ set xs. f x = g x"
shows "subseq (map f xs) (map g ys)"
using assms by (induct) auto
lemma one_step_explicit:
assumes step: "(s,t) ∈ rew_r_p_s lr p σ"
and dt: "is_DT_of lr lr'"
and good: "s ≪ u"
shows "∃ v. t ≪ v ∧ (u,v) ∈ ( rew'⇧* O qrstep False Q' {lr'} )"
proof -
let ?sharp_at = "λ tm q. ♯ (tm |_ q)"
from good[unfolded goodFor_def] obtain C rpos_s_list where
u_decompose: "u =⇩f (C,[?sharp_at s q . q ← rpos_s_list])" and
rpos_s_list: "RPos s = set rpos_s_list" and
sF: "funas_term s ⊆ F"
by auto
from step have ps: "p ∈ poss s" unfolding qrstep_r_p_s_def by auto
from step have step': "(s,t) ∈ rew_r_p_s' lr p σ"
by (rule rew_r_p_s'I_full, insert sF, cases s, auto)
let ?f = "λ q. if q < p ∨ q ⊥ p then ?sharp_at t q else ?sharp_at s q"
let ?us = "[ ?sharp_at s q . q ← rpos_s_list ]"
let ?ws = "[ ?f q . q ← rpos_s_list ]"
let ?w = "fill_holes C ?ws"
{
fix q
assume q_in_rpos_s: "q ∈ set rpos_s_list"
{
assume q: "q < p"
then have q_diff: "p = q <#> pos_diff p q" (is "_ = _ <#> ?q'") by auto
then have ne: "?q' ≠ ε" using q less_simps(1) by force
from ps[unfolded arg_cong[OF q_diff, of "λ p. p ∈ poss s"]] have qs: "q ∈ poss s" by simp
have "(s |_ q, t |_ q) ∈ rew_r_p_s lr ?q' σ" by (metis q_diff qrstep_subt_at_gen step)
from nrqrstep_r_p_s_imp_sharp_qrstep_r_p_s[OF ne this] have
step: "(?sharp_at s q, ?f q) ∈ rew_r_p_s lr ?q' σ" using q by auto
have "(?sharp_at s q, ?f q) ∈ rew_r_p_s' lr ?q' σ"
by (rule rew_r_p_s'I_full[OF step], unfold funas_sharp_term, rule funas_term_subterm_args[OF sF qs])
hence "(?sharp_at s q, ?f q) ∈ rew'" using qrstep_qrstep_r_p_s_conv by blast
hence "(?sharp_at s q, ?f q) ∈ rew'⇧*" by auto
} note q_less_p = this
{
assume q_par_p: "q ⊥ p"
from q_in_rpos_s have "q ∈ poss s"
unfolding rpos_s_list[symmetric] RPos_def DPos_def by auto
from parallel_qrstep_subt_at[OF step _ this] have "?f q = ?sharp_at s q"
using q_par_p parallel_pos_sym by auto
then have "(?sharp_at s q, ?f q) ∈ rew'⇧*" by auto
} note q_par_p_p = this
{
assume q: "¬ (q < p ∨ q ⊥ p)"
then have "?f q = ?sharp_at s q" by auto
then have "(?sharp_at s q, ?f q) ∈ rew'⇧*" by auto
} note q_nless_p = this
have "(?sharp_at s q, ?f q) ∈ rew'⇧*" using q_par_p_p q_less_p q_nless_p by auto
} note repair_step = this
{
fix j
assume "j < length ?ws"
then have "(?us!j,?ws!j) ∈ rew'⇧*" using repair_step rpos_s_list by auto
}
from eqf_all_ctxt_closed_step[OF all_ctxt_closed_qrsteps u_decompose this] length_map
have repair_steps: "(u,?w) ∈ (rew'⇧*)" by auto
obtain Dp t' dpos_r_list where
t': "t' =⇩f (Dp, [?sharp_at t (p <#> q) . q ← dpos_r_list])"
and dpos_r_list_dpos: "set dpos_r_list = DPos (snd lr)"
and p_step: "(?sharp_at s p, t') ∈ qrstep False Q' {lr'}"
using step_to_dt_step[OF step' dt] by metis
let ?rs = "[?sharp_at t (p <#> q) . q ← dpos_r_list]"
obtain i where
rpos_s_list_i: "rpos_s_list!i = p" and
i_index_rpos_s_list: "i < length rpos_s_list"
using rpos_s_list step_at_RPos[OF step] List.in_set_conv_nth[of p rpos_s_list] by auto
let ?rpos_s_left = "take i rpos_s_list"
let ?rpos_s_right = "drop (Suc i) rpos_s_list"
have i_index_ws: "i < length ?ws" using i_index_rpos_s_list by auto
have nh_C_l_ws: "num_holes C = length ?ws" using eqfE[OF u_decompose] length_map by auto
from fill_holes_ctxt[OF this i_index_ws] obtain C' where
C': "⋀ s. fill_holes C (?ws[i := s]) = C' ⟨ s ⟩" by auto
let ?v = "fill_holes C (?ws[i := t'])"
have ws_i: "?ws!i = ?sharp_at s p"
unfolding nth_map[OF i_index_rpos_s_list] rpos_s_list_i
using less_irrefl parallel_pos order_refl by auto
then have "?ws = ?ws[i := ?sharp_at s p]" unfolding ws_i[symmetric] using list_update_id[of ?ws i] by auto
from this C' have C'ws: "?w = C'⟨?sharp_at s p⟩" by (metis (lifting))
from C' have C'vs: "?v = C'⟨t'⟩" by (metis (lifting))
have dp_step: "(fill_holes C ?ws, ?v) ∈ qrstep False Q' {lr'}" unfolding C'ws C'vs using qrstep.ctxt[OF p_step] .
from repair_steps dp_step have step_simulation: "(u,?v) ∈ ( rew'⇧* O qrstep False Q' {lr'} )" by auto
let ?ws_left = "[ ?f q . q ← ?rpos_s_left]"
let ?ws_right = "[ ?f q . q ← ?rpos_s_right]"
have sep: "?ws_left @ t' # ?ws_right = ?ws[i := t']"
unfolding take_map[symmetric] drop_map[symmetric]
using id_take_nth_drop[OF i_index_ws] upd_conv_take_nth_drop[OF i_index_ws] by auto
let ?vs = "?ws_left @ ?rs @ ?ws_right"
let ?D = "compose_mctxt C i Dp"
have len_left: "length ?ws_left = i" using length_take i_index_rpos_s_list by auto
moreover have "?v =⇩f (C,?ws_left @ t' # ?ws_right)" unfolding sep using nh_C_l_ws by auto
ultimately have v_decompose_D: "?v =⇩f (?D, ?vs)"
using compose_mctxt_sound[OF _ t'] by (metis (lifting, no_types))
let ?filter_old = "filter (λ q. q ∈ RPos s ∧ (q < p ∨ q ⊥ p))"
let ?qs = "(?filter_old ?rpos_s_left) @ [p <#> q . q ← dpos_r_list] @ (?filter_old ?rpos_s_right)"
let ?rpos_t_list = "[q ← ?qs. q ∈ RPos t]"
have good_RPos: "RPos t = set ?rpos_t_list" proof
{
fix q
assume q_in_rpos_t: "q ∈ RPos t"
then have q_in_approx: "q ∈ {q. q ∈ RPos s ∧ (q < p ∨ q ⊥ p)} ∨ q ∈ {p <#> q | q. q ∈ DPos (snd lr)}" (is "_ ∈ ?old ∨ _ ∈ ?new")
using RPos_step_approx[OF step] by auto
{
assume q_in_old: "q ∈ ?old"
hence "q < p ∨ q ⊥ p" by auto hence q_noteq_p: "q ≠ p" using less_pos_def parallel_pos by auto
have "q ∈ set rpos_s_list" using q_in_old rpos_s_list by auto
hence "q ∈ set (?rpos_s_left @ rpos_s_list!i # ?rpos_s_right)"
by (metis i_index_rpos_s_list id_take_nth_drop)
hence "q ∈ set (?rpos_s_left @ ?rpos_s_right)"
unfolding rpos_s_list_i using q_noteq_p by auto
hence "q ∈ set ?qs" using q_in_old by auto
} note q_in_old = this
{
assume q_in_new: "q ∈ ?new"
hence "q ∈ set ?qs" unfolding dpos_r_list_dpos[symmetric] by auto
} note q_in_new = this
from q_in_approx q_in_old q_in_new q_in_rpos_t have "q ∈ set ?rpos_t_list" by auto
}
then show "RPos t ⊆ set ?rpos_t_list" by auto
next show "set ?rpos_t_list ⊆ RPos t" by auto
qed
{ fix q
fix pos_lst
assume "q ∈ set (?filter_old pos_lst)"
hence "q < p ∨ q ⊥ p" by auto hence "?sharp_at t q = ?f q" by simp
}
hence f_of_q_in_filter_old: "⋀ pos_lst. ∀ q ∈ set (?filter_old pos_lst). ?sharp_at t q = ?f q" by blast
have good_sharp: "subseq [?sharp_at t q . q ← ?rpos_t_list] ?vs"
proof -
have left: "subseq [ ?sharp_at t q. q ← ?filter_old ?rpos_s_left] ?ws_left" (is "subseq ?lft _")
using subseq_map_same [OF subseq_filter_left f_of_q_in_filter_old] .
have right: "subseq [ ?sharp_at t q. q ← ?filter_old ?rpos_s_right] ?ws_right" (is "subseq ?rght _")
using subseq_map_same [OF subseq_filter_left f_of_q_in_filter_old] .
have middle: "subseq [ ?sharp_at t q . q ← [(p <#> q'). q' ← dpos_r_list]] ?rs" (is "subseq ?mid _")
unfolding map_map comp_def by auto
have "[?sharp_at t q. q ← ?qs ] = ?lft @ ?mid @ ?rght"
unfolding map_append by simp
hence "subseq [?sharp_at t q. q ← ?qs ] ?vs" using left middle right list_emb_append_mono
by (metis (lifting, no_types))
thus ?thesis using subseq_filter_left subseq_map subseq_trans by blast
qed
from step have "(s,t) ∈ qrstep False Q R" unfolding qrstep_qrstep_r_p_s_conv by blast
hence "(s,t) ∈ rstep R" by auto
from rstep_preserves_funas_terms[OF R_sig sF this wf_R] have tF: "funas_term t ⊆ F" .
from mctxt_fill_partially[OF good_sharp v_decompose_D] obtain C' where
"?v =⇩f (C',[?sharp_at t q . q ← ?rpos_t_list])" by auto
from v_decompose_D good_RPos tF this
have good: "t ≪ ?v" unfolding goodFor_def
by (metis (lifting, no_types))
then show ?thesis using step_simulation by auto
qed
context
fixes S W DT_S DT_W :: "('f, 'v) trs" and nfs :: bool
assumes DT_S: "⋀ lr. lr ∈ S ⟹ ∃ dt ∈ DT_S. is_DT_of lr dt"
and DT_W: "⋀ lr. lr ∈ W ⟹ ∃ dt ∈ DT_W. is_DT_of lr dt"
and S: "S ⊆ R"
and W: "W ⊆ R"
and nfs: "nfs = False"
begin
lemma one_step_generic:
assumes good: "s ≪ u"
and step: "(s, t) ∈ qrstep nfs' Q S_W"
and DT: "⋀ lr. lr ∈ S_W ⟹ ∃ dt ∈ DT. is_DT_of lr dt"
and S_W: "S_W ⊆ R"
shows "∃ v. t ≪ v ∧ (u, v) ∈ ( (qrstep nfs Q' R)⇧* O qrstep nfs Q' DT)"
proof -
from step[unfolded qrstep_qrstep_r_p_s_conv] obtain lr p σ
where step: "(s, t) ∈ qrstep_r_p_s nfs' Q S_W lr p σ" by auto
from step have lr: "lr ∈ S_W" unfolding qrstep_r_p_s_def by auto
from DT[OF this] obtain dt where dt: "dt ∈ DT" and dt_of: "is_DT_of lr dt" by auto
from lr S_W step have "(s,t) ∈ qrstep_r_p_s False Q R lr p σ" unfolding qrstep_r_p_s_def by auto
from one_step_explicit[OF this dt_of good]
obtain v where tv: "t ≪ v" and uv: "(u, v) ∈ rew'⇧* O qrstep nfs Q' {dt}" by (auto simp: nfs)
from dt qrstep_mono[OF _ subset_refl] have "qrstep nfs Q' {dt} ⊆ qrstep nfs Q' DT" by blast
with uv have "(u,v) ∈ rew'⇧* O qrstep nfs Q' DT" by auto
with tv show ?thesis unfolding nfs by blast
qed
lemma many_relative_steps:
assumes good: "s ≪ u"
and step: "(s, t) ∈ (relto (qrstep nfs' Q S) (qrstep nfs' Q W))^^n"
shows "∃ v. t ≪ v ∧ (u, v) ∈ (relto (qrstep nfs Q' DT_S) (qrstep nfs Q' (R ∪ DT_W)))^^n"
proof -
let ?S = "qrstep nfs Q' DT_S"
let ?W = "qrstep nfs Q' DT_W"
let ?R = "qrstep nfs Q' R"
let ?RW = "qrstep nfs Q' (R ∪ DT_W)"
have main: "∃ v. t ≪ v ∧ (u, v) ∈ (relto (?R^* O ?S) (?R^* O ?W))^^n"
by (rule simulate_conditional_relative_steps_count[of "λ s t. s ≪ t",
OF one_step_generic[OF _ _ DT_S S] one_step_generic[OF _ _ DT_W W] step good])
have "relto (?R^* O ?S) (?R^* O ?W) ⊆ relto ?S ?RW" unfolding qrstep_union by regexp
from relpow_mono[OF this, of n] main
show ?thesis by blast
qed
lemma dependency_tuples_sound:
assumes bound: "deriv_bound_measure_class
(relto (qrstep nfs Q' DT_S) (qrstep nfs Q' (R ∪ DT_W)))
(Runtime_Complexity C' D'') cc"
and D': "D ⊆ set D'"
and C': "set C' ∩ D = {}"
and CD'_F: "set C' ∪ set D' ⊆ F"
and D'': "set D'' = (λ(f, n). (♯ f, n)) ` set D'"
shows "deriv_bound_measure_class
(relto (qrstep nfs' Q S) (qrstep nfs' Q W))
(Runtime_Complexity C' D') cc"
proof -
let ?D = "relto (qrstep nfs Q' DT_S) (qrstep nfs Q' (R ∪ DT_W))"
let ?R = "relto (qrstep nfs' Q S) (qrstep nfs' Q 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 ⊆ F"
by (cases s) (auto simp: funas_args_term_def)
from relpow_Suc_E2[OF st] obtain u where "(s,u) ∈ ?R" by metis
hence "(s,u) ∈ (qrstep nfs' Q (S ∪ W))^+" unfolding qrstep_union by regexp
then obtain u where "(s,u) ∈ qrstep nfs' Q (S ∪ W)" by (induct, auto)
with S W qrstep_all_mono[OF _ subset_refl, of "S ∪ W" R Q False nfs']
have su: "(s,u) ∈ rew" by auto
let ?s = "♯ s"
have ss: "?s ∈ ?TS n" using sT by (cases s) (auto simp: D'' funas_args_term_def)
have rpos: "RPos s = {ε}"
proof -
from sT obtain f ss where s: "s = Fun f ss" by auto
let ?n = "length ss"
let ?f = "(f,?n)"
from sT s have f: "?f ∈ set D'"
and args: "⋀ s. s ∈ set ss ⟹ funas_term s ⊆ set C'" by (auto simp: funas_args_term_def)
{
fix p
assume "p ∈ RPos s"
with RPos_subseteq_DPos have "p ∈ DPos s" by auto
from this[unfolded DPos_def] obtain g where
p: "p ∈ poss s" and root: "root (s |_ p) = Some g" and g: "g ∈ D" by auto
{
assume "p ≠ ε"
then obtain i q where pq: "p = i <# q" by (cases p, auto)
with p s root have mem: "ss ! i ∈ set ss" and q: "q ∈ poss (ss ! i)"
and root: "root (ss ! i |_ q) = Some g" by auto
from root q have "g ∈ funas_term (ss ! i)" unfolding funas_term_poss_conv
by (cases "ss ! i |_ q", auto)
with args[OF mem] have "g ∈ set C'" by auto
with C' g have False by auto
}
hence "p = ε" by auto
} note eps = this
moreover {
from su[unfolded qrstep_qrstep_r_p_s_conv] obtain lr p σ where
su: "(s, u) ∈ rew_r_p_s lr p σ" by auto
from step_at_RPos[OF this] have "p ∈ RPos s" by auto
with eps[OF this] have "ε ∈ RPos s" by simp
}
ultimately show ?thesis by auto
qed
have "s ≪ ?s" unfolding goodFor_def
by (rule exI[of _ MHole], rule exI[of _ "[ε]"], auto simp: rpos sF)
from many_relative_steps[OF this st] 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