theory Usable_Replacement_Map
imports
QTRS.Term_Order
QTRS.Q_Relative_Rewriting
"Check-NT.Icap"
QTRS.QDP_Framework
"Check-NT.Name"
Complexity_Framework
"Check-NT.Innermost_Usable_Rules"
begin
subsection ‹usable replacement maps and compatibility, taken from Diss Avanzini›
context
fixes μ :: "'f af"
begin
definition af_nf_compatible_terms :: "('f,'v)trs ⇒ ('f,'v)terms" where
"af_nf_compatible_terms rel ≡ { t . ∀ C s. t = C⟨s⟩ ⟶ af_regarded_pos μ t (hole_pos C) ∨ s ∈ NF rel}"
lemma af_nf_compatible_terms_full_af: assumes full: "μ = full_af"
shows "s ∈ af_nf_compatible_terms rel"
unfolding af_nf_compatible_terms_def
by (auto simp: af_regarded_full full)
lemma af_nf_compatible_terms_mono: assumes rel: "rel' ⊆ rel"
shows "af_nf_compatible_terms rel ⊆ af_nf_compatible_terms rel'"
unfolding af_nf_compatible_terms_def using NF_anti_mono[OF rel] by blast
definition usable_replacement_map :: "('f,'v)terms ⇒ bool ⇒ ('f,'v)trs ⇒ ('f,'v)terms ⇒ ('f,'v)trs ⇒ bool" where
"usable_replacement_map T nfs P Q R ≡
(qrstep nfs Q P) ^* `` T ⊆ af_nf_compatible_terms (qrstep nfs Q R)"
lemma usable_replacement_map_mono: assumes T: "T' ⊆ T" and P: "P' ⊆ P" and R: "R' ⊆ R"
shows "usable_replacement_map T nfs P Q R ⟹ usable_replacement_map T' nfs P' Q R'"
unfolding usable_replacement_map_def
using rtrancl_mono[OF qrstep_mono[OF P subset_refl, of nfs Q]] T
af_nf_compatible_terms_mono[OF qrstep_mono[OF R subset_refl, of nfs Q]] by blast
lemma avanzini_14_9_1:
assumes us: "usable_replacement_map T nfs (S ∪ W) Q R" and "R ⊆ S ∪ W"
and R: "R ⊆ ord" and mono: "af_monotone π ord" and af: "af_subset μ π" and subst: "subst.closed ord"
and s: "s ∈ (qrstep nfs Q (S ∪ W))^* `` T" and step: "(s,t) ∈ qrstep nfs Q R"
shows "(s,t) ∈ ord"
proof -
from us[unfolded usable_replacement_map_def] s have
s_af: "s ∈ af_nf_compatible_terms (qrstep nfs Q R)" by auto
from qrstepE[OF step] obtain l r C σ where
nf: "∀u⊲l ⋅ σ. u ∈ NF_terms Q" and
lr: "(l, r) ∈ R" and
s: "s = C⟨l ⋅ σ⟩" and
t: "t = C⟨r ⋅ σ⟩" and
nfs: "NF_subst nfs (l, r) σ Q" .
hence "(l ⋅ σ, r ⋅ σ) ∈ qrstep nfs Q R" (is "(?l,?r) ∈ _") by auto
with s_af[unfolded af_nf_compatible_terms_def, simplified, rule_format, OF s]
have rp: "af_regarded_pos μ C⟨l ⋅ σ⟩ (hole_pos C)" by auto
from lr R have "(l,r) ∈ ord" by auto
from subst.closedD[OF subst this] have lr: "(?l,?r) ∈ ord" by auto
have "(C⟨?l⟩, C⟨?r⟩) ∈ ord"
by (rule af_monotone_af_regarded_posD[OF af_subset_af_monotone[OF af mono] rp lr])
with s t show ?thesis by auto
qed
end
lemma usable_replacement_map_full_af[simp]: "usable_replacement_map full_af T nfs R Q R'"
unfolding usable_replacement_map_def using af_nf_compatible_terms_full_af[OF refl] by auto
context cpx_ce_af_redtriple_order
begin
definition NS_μ :: "'f af" where "NS_μ = full_af"
lemma NS_μ: "af_monotone NS_μ NS"
by (rule ctxt_closed_imp_af_monotone[OF wm_NS])
lemma usable_replacement_map_NS: "usable_replacement_map NS_μ T nfs P Q R"
unfolding usable_replacement_map_def
using af_nf_compatible_terms_full_af[OF NS_μ_def] by blast
lemma avanzini_14_9_2: assumes compatR: "Rs ⊆ S" "Rw ⊆ NS" and
usable: "usable_replacement_map μ' T nfs (Rs ∪ Rw) Q Rs"
and af: "af_subset μ' μ"
and step: "(s,t) ∈ relto (qrstep nfs Q Rs) (qrstep nfs Q Rw)"
and s: "s ∈ (qrstep nfs Q (Rs ∪ Rw))^* `` T" (is "s ∈ ?T")
shows "(s,t) ∈ S"
proof -
have subset: "Rs ⊆ Rs ∪ Rw" "Rw ⊆ Rs ∪ Rw" by auto
note strict = avanzini_14_9_1[OF usable subset(1) compatR(1) μ af subst_S]
note weak = avanzini_14_9_1[OF usable_replacement_map_NS subset(2) compatR(2) NS_μ af_subset_refl subst_NS, of _ nfs Q T]
let ?Rs = "qrstep nfs Q Rs" let ?Rw = "qrstep nfs Q Rw" let ?P = "qrstep nfs Q (Rs ∪ Rw)"
from step obtain u v where su: "(s,u) ∈ ?Rw^*" and uv: "(u,v) ∈ ?Rs" and vt: "(v,t) ∈ ?Rw^*" by auto
have [simp]: "⋀ s. (s,s) ∈ NS" using refl_NS[unfolded refl_on_def] by auto
{
fix s t R
assume s: "s ∈ ?T" and R: "(s,t) ∈ qrstep nfs Q R"
"R ⊆ Rs ∪ Rw"
from qrstep_mono[OF R(2)] R(1) have "(s,t) ∈ ?P" by blast
with s have "t ∈ ?T"
by (metis r_into_rtrancl rtrancl_Image_step)
} note T = this
{
fix s u
assume s: "s ∈ ?T" and su: "(s,u) ∈ ?Rw^*"
from su have "(s,u) ∈ NS ∧ u ∈ ?T"
proof (induct)
case (step t u)
from weak[OF _ step(2)] step(3) have "(t,u) ∈ NS" by auto
from trans_NS_point[OF _ this] step(3) have su: "(s,u) ∈ NS" by auto
from T[OF _ step(2)] step(3) have "u ∈ ?T" by auto
with su show ?case by auto
qed (insert s, auto)
hence "(s,u) ∈ NS" "u ∈ ?T" by auto
} note steps = this
from steps[OF s su] have su: "(s,u) ∈ NS" and u: "u ∈ ?T" .
from T[OF u uv] have v: "v ∈ ?T" by auto
from strict[OF u uv] have uv: "(u,v) ∈ S" .
from steps[OF v vt] have vt: "(v,t) ∈ NS" by auto
from compat_NS_S_point[OF su uv] have sv: "(s,v) ∈ S" .
from compat_S_NS_point[OF sv vt] show "(s,t) ∈ S" .
qed
theorem avanzini_14_10: assumes compatR: "Rs ⊆ S" "Rw ⊆ NS" and
usable: "usable_replacement_map μ' (terms_of cm) nfs (Rs ∪ Rw) Q Rs" and
af: "af_subset μ' μ" and
cpx: "cpx_class cm cc"
shows "deriv_bound_measure_class (relto (qrstep nfs Q Rs) (qrstep nfs Q Rw)) cm cc"
(is "deriv_bound_measure_class ?P cm cc")
proof -
let ?T = "(qrstep nfs Q (Rs ∪ Rw))^* `` terms_of cm"
from cpx_class[OF cpx] have bound: "deriv_bound_measure_class S cm cc" .
note d = deriv_bound_measure_class_def deriv_bound_rel_class_def deriv_bound_rel_def
from bound[unfolded d] obtain f where f: "f ∈ O_of cc"
and bound: "⋀ n t. t ∈ terms_of_nat cm n ⟹ deriv_bound S t (f n)"
by auto
show ?thesis unfolding d
proof (intro exI conjI allI impI, rule f)
fix n t
assume t: "t ∈ terms_of_nat cm n"
from bound[OF t] have bound: "deriv_bound S t (f n)" by auto
from t have t: "t ∈ ?T" by (auto simp: terms_of)
note d = deriv_bound_def
note main = avanzini_14_9_2[OF compatR usable af]
show "deriv_bound ?P t (f n)"
proof (rule ccontr)
assume "¬ ?thesis"
from this[unfolded d]
obtain s where ts: "(t,s) ∈ ?P ^^ (Suc (f n))" by auto
def m ≡ "Suc (f n)"
from ts have "(t,s) ∈ S ^^ (Suc (f n)) ∧ s ∈ ?T" unfolding m_def[symmetric]
proof (induct m arbitrary: s)
case (Suc m s)
from Suc(2)[simplified] obtain u where tus: "(t,u) ∈ ?P^^m" and uss: "(u,s) ∈ ?P" by auto
from Suc(1)[OF tus] have tu: "(t,u) ∈ S^^m" and u: "u ∈ ?T" by auto
from main[OF uss u] have us: "(u,s) ∈ S" .
from tu us have ts: "(t,s) ∈ S^^(Suc m)" by auto
from uss have "(u,s) ∈ (qrstep nfs Q (Rs ∪ Rw))^*" unfolding qrstep_union by regexp
with u have "s ∈ ?T" by (metis rtrancl_Image_step)
with ts show ?case by auto
qed (insert t, auto)
with bound show False unfolding d by blast
qed
qed
qed
lemma (in redtriple) urm_mono_redpair_sound:
assumes weakR: "(R ∪ Rw) - Rs ⊆ NS"
and nonStrict: "P ∪ Pw ⊆ NS ∪ S"
and strictP: "Ps ⊆ S"
and strictR: "Rs ⊆ S"
and inn: "NF_terms Q ⊆ NF_trs (R ∪ Rw)"
and urm: "⋀ s t σ. (s,t) ∈ P ∪ Pw ⟹ s ⋅ σ ∈ NF_terms Q ⟹ usable_replacement_map μ' {t ⋅ σ} nfs (R ∪ Rw) Q (Rs ∩ (R ∪ Rw))"
and af: "af_subset μ' μ"
and mono: "af_monotone μ S"
and chain: "min_ichain (nfs,m,P,Pw,Q,R,Rw) s t σ"
shows "∃ j. min_ichain (nfs,m,P - Ps, Pw - Ps, Q, R - Rs, Rw - Rs) (shift s j) (shift t j) (shift σ j)"
proof (rule min_ichain_split[OF chain], rule)
let ?R = "R ∪ Rw"
let ?P = "P ∪ Pw"
assume chain: "min_ichain (nfs,m,Ps ∩ ?P, ?P - Ps, Q, Rs ∩ ?R, ?R - Rs) s t σ"
have id: "Ps ∩ ?P ∪ (?P - Ps) = ?P" by auto
have idR: "Rs ∩ ?R ∪ (?R - Rs) = ?R" by auto
have idS: "S ∪ NS = NS ∪ S" by auto
note chain = chain[unfolded min_ichain.simps ichain.simps minimal_cond_def id idR]
from chain have P: "⋀ i. (s i, t i) ∈ ?P" by auto
from chain have steps: "⋀ i. (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ (qrstep nfs Q ?R)^*" by auto
from chain have Q: "⋀ i. s i ⋅ σ i ∈ NF_terms Q" by auto
{
fix i u v
assume tu: "(t i ⋅ σ i, u) ∈ (qrstep nfs Q ?R)^*"
and uv: "(u,v) ∈ qrstep nfs Q (Rs ∩ ?R)"
hence "u ∈ (qrstep nfs Q ?R)⇧* `` {t i ⋅ σ i}" by auto
from avanzini_14_9_1[OF urm[OF P Q] _ _ mono af subst_S this uv] strictR have "(u,v) ∈ S" by auto
hence "(u,v) ∈ S" by auto
} note S = this
{
fix u v
assume uv: "(u,v) ∈ qrstep nfs Q (?R - Rs)"
hence "(u,v) ∈ rstep (?R - Rs)" by auto
with rstep_subset[OF wm_NS subst_NS weakR] have "(u,v) ∈ NS" by auto
hence "(u,v) ∈ NS" by auto
} note NS = this
{
fix i u v
assume tu: "(t i ⋅ σ i, u) ∈ (qrstep nfs Q ?R)^*"
and uv: "(u,v) ∈ qrstep nfs Q ?R"
have "(u,v) ∈ NS ∪ S"
proof (cases "(u,v) ∈ qrstep nfs Q (Rs ∩ ?R)")
case True
show ?thesis using S[OF tu True] by auto
next
case False
with uv have uv: "(u,v) ∈ qrstep nfs Q (?R - Rs)"
unfolding arg_cong[OF idR[symmetric], of "qrstep nfs Q"]
unfolding qrstep_union by auto
thus ?thesis using NS[OF uv] by auto
qed
} note both = this
{
fix i u v
assume tu: "(t i ⋅ σ i, u) ∈ (qrstep nfs Q ?R)^*"
and uv: "(u,v) ∈ (qrstep nfs Q ?R)^*"
from uv have "(u, v) ∈ (NS ∪ S)^*"
proof (induct rule: rtrancl_induct)
case (step v w)
from tu step(1) have "(t i ⋅ σ i, v) ∈ (qrstep nfs Q ?R)⇧*" by auto
from rtrancl_into_rtrancl[OF step(3) both[OF this step(2)]] show ?case .
qed simp
} note both_steps_gen = this
{
fix i u
assume tu: "(t i ⋅ σ i, u) ∈ (qrstep nfs Q ?R)^*"
have "(t i ⋅ σ i, u) ∈ (NS ∪ S)^*"
by (rule both_steps_gen[OF _ tu], auto)
} note both_steps = this
{
fix i
from P nonStrict have "(s i, t i) ∈ NS ∪ S" by auto
with subst.closedD subst_NS subst_S have "(s i ⋅ σ i, t i ⋅ σ i) ∈ NS ∪ S" by auto
} note both_P = this
let ?NSS = "NS ∪ S"
let ?S = "?NSS^* O S O ?NSS^*"
let ?NS = "?NSS^*"
let ?t = "λ i. t i ⋅ σ i"
let ?s = "λ i. s i ⋅ σ i"
have "∀ i. (?s i, ?s (Suc i)) ∈ ?NS ∪ ?S"
proof
fix i
from both_P[of i] both_steps[OF steps[of i]]
have "(?s i, ?s (Suc i)) ∈ ?NSS O ?NS" by auto
thus "(?s i, ?s (Suc i)) ∈ ?NS ∪ ?S" by regexp
qed
note main = non_strict_ending[OF this]
have "?NS O ?S ⊆ ?S" by regexp
note main = main[OF this]
have "SN ?S"
by (rule compatible_SN'[OF NS.compat SN])
hence "⋀ T. SN_on ?S T" unfolding SN_defs by blast
note main = main[OF this]
from main obtain n where n: "⋀ m. m ≥ n ⟹ (?s m, ?s (Suc m)) ∉ ?S" by blast
let ?Q = "qrstep nfs Q ?R"
let ?QQ = "?Q^* O qrstep nfs Q (Rs ∩ ?R) O ?Q^*"
from chain
have "(INFM i. (s i, t i) ∈ Ps ∩ ?P) ∨
(INFM i. (?t i, ?s (Suc i)) ∈ ?QQ)" by blast
from this[unfolded INFM_disj_distrib[symmetric], unfolded INFM_nat]
obtain m where m: "n < m" and alt:"(s m, t m) ∈ Ps ∩ ?P ∨
(?t m, ?s (Suc m)) ∈ ?QQ" by blast
from n[of m] m have noS: "(?s m, ?s (Suc m)) ∉ ?S" by auto
from alt have "(?s m, ?s (Suc m)) ∈ ?S"
proof
assume "(s m, t m) ∈ Ps ∩ ?P"
with strictP have "(s m, t m) ∈ S" by auto
from subst.closedD[OF subst_S this] have "(?s m, ?t m) ∈ S" by auto
with both_steps[OF steps[of m]] have "(?s m, ?s (Suc m)) ∈ S O ?NS" by auto
thus ?thesis by regexp
next
assume "(?t m, ?s (Suc m)) ∈ ?QQ"
then obtain u v where tu: "(?t m, u) ∈ ?Q^*" and uv: "(u,v) ∈ qrstep nfs Q (Rs ∩ ?R)"
and vs: "(v,?s (Suc m)) ∈ ?Q^*" by auto
from S[OF tu uv] have uvS: "(u,v) ∈ S" .
from uv have "(u,v) ∈ qrstep nfs Q ?R" by auto
with tu have tv: "(?t m, v) ∈ ?Q^*" by auto
from both_steps[OF tu] have tuNS: "(?t m, u) ∈ ?NSS^*" by auto
from both_steps_gen[OF tv vs] have vsNS: "(v, ?s (Suc m)) ∈ ?NSS^*" by auto
from converse_rtrancl_into_rtrancl[OF both_P[of m] tuNS] have su: "(?s m, u) ∈ ?NSS^*" .
from su uvS vsNS show ?thesis by blast
qed
with noS show False ..
qed
end
subsection ‹computing innermost usable replacement maps from Moser/Hirokawa›
context
fixes ecap :: "('f,string)cap_fun"
and R :: "('f,string)trs"
and Q :: "('f,string)terms"
begin
fun get_args where
"get_args True t = set (args t)"
| "get_args False t = {t}"
definition innermost_repl_map :: "('f,string)trs ⇒ (('f × nat) × nat) set" where
"innermost_repl_map P ≡ { ((f,length rs),i) | l C f rs i b.
((l,C⟨Fun f rs⟩),b) ∈ R × {True} ∪ P × {False} ∧
i < length rs ∧
Inl () ∈ vars_term (ecap R Q (mv_xvar ` (get_args b l)) (mv_xvar (rs ! i)))}"
definition μ_i_P :: "('f,string)trs ⇒ 'f af" where
"μ_i_P P f = { i. (f,i) ∈ innermost_repl_map P}"
definition μ_i :: "'f af" where
"μ_i = μ_i_P {}"
context
fixes 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
inductive approx_cond :: "('f,string)term list ⇒ ('f,string)term ⇒ ('f,string)rule ⇒ bool" and
μ_cond :: "'f × nat ⇒ nat ⇒ bool"
where
approx_cond_init: "(ss,t,lr) ∈ init ⟹ approx_cond ss t lr"
| approx_cond_rec: "approx_cond ss (Fun f ts) (l,r)
⟹ (l',r') ∈ R
⟹ rule_match R Q ecap (mv_xvar ` set ss) f (map mv_xvar ts) l'
⟹ (l,r) ∈ U (args l') r'
⟹ approx_cond (args l') r' (l,r)"
| approx_cond_sub: "approx_cond ss (Fun f ts) (l,r)
⟹ i < length ts
⟹ (l,r) ∈ U ss (ts ! i)
⟹ approx_cond ss (ts ! i) (l,r)"
| μ_cond: "approx_cond ss (Fun f ts) (l,r)
⟹ i < length ts
⟹ (l,r) ∈ U ss (ts ! i)
⟹ μ_cond (f,length ts) i"
definition "μ_approx f ≡ Collect (μ_cond f)"
end
context
assumes inn: "NF_terms Q ⊆ NF_trs R"
and ecap: "is_ecap ecap"
and wf: "wwf_qtrs Q R"
begin
lemma hirokawa_moser_4_7_1_main:
assumes redex: "(redex,r') ∈ rqrstep nfs Q R"
and lr: "((l,r),b) ∈ R × {True} ∪ P × {False}"
and args: "get_args b l ⋅⇩s⇩e⇩t σ ⊆ NF_terms Q"
and nfs: "NF_subst True (l,r) σ Q"
shows "r ⋅ σ ⊵ C ⟨ redex ⟩ ⟹ af_regarded_pos (μ_i_P P) (C ⟨ redex ⟩) (hole_pos C)"
proof (induct C)
case (More f bef C aft)
let ?μ_i = "μ_i_P P"
from supteq_trans[OF More(2)] have "r ⋅ σ ⊵ C⟨redex⟩" by auto
from More(1)[OF this] have IH: "af_regarded_pos ?μ_i C⟨redex⟩ (hole_pos C)" .
from More(2) obtain D where id: "r ⋅ σ = D ⟨ (More f bef C aft) ⟨ redex ⟩ ⟩"
by (metis supteq_ctxtE)
let ?hp = "hole_pos D"
let ?i = "length bef"
let ?n = "Suc (?i + length aft)"
from redex have "(redex,r') ∈ rstep R" unfolding rqrstep_def by auto
hence redex_NF: "redex ∉ NF_trs R" by auto
{
fix x
assume "σ x ∈ NF_terms Q"
with inn have "σ x ∈ NF_trs R" by auto
from NF_subterm[OF this, of redex] redex_NF have "¬ σ x ⊵ redex" by auto
} note vars = this
let ?mv = "mv_xvar"
from id have "?hp ∈ poss (r ⋅ σ)" by auto
from poss_subst_choice[OF this]
have "?i ∈ ?μ_i (f,?n)"
proof
assume in_r: "?hp ∈ poss r ∧ is_Fun (r |_ ?hp)"
hence [simp]: "r ⋅ σ |_ ?hp = r |_ ?hp ⋅ σ" by auto
from arg_cong[OF id, of "λ t. t |_ ?hp"]
have id: "r |_ ?hp ⋅ σ = Fun f (bef @ C⟨redex⟩ # aft)" by simp
with in_r obtain rs where rhp: "r |_ ?hp = Fun f rs" by (cases "r |_ ?hp", auto)
def E ≡ "ctxt_of_pos_term ?hp r"
from in_r have "r = E ⟨ r |_ ?hp ⟩" unfolding E_def
by (metis ctxt_supt_id)
with rhp have r: "r = E ⟨ Fun f rs ⟩" by auto
note lr = lr[unfolded r]
show ?thesis unfolding μ_i_P_def
proof
let ?m = "length rs"
note id = id[unfolded rhp]
from arg_cong[OF id, of num_args]
have sym: "((f,?n),?i) = ((f,?m),?i)" and im: "?i < ?m" by auto
show "((f,?n),?i) ∈ innermost_repl_map P" unfolding innermost_repl_map_def
proof (rule, intro exI conjI, rule sym, rule lr, rule im)
def ri ≡ "rs ! ?i"
from arg_cong[OF id, of "λ t. args t ! ?i"] sym
have ri_red: "ri ⋅ σ = C⟨redex⟩" unfolding ri_def by auto
from r have "r ⊵ Fun f rs" by auto
moreover have "Fun f rs ⊵ ri" using sym ri_def by auto
ultimately have "r ⊵ ri" by (rule supteq_trans)
hence "vars_term ri ⊆ vars_term r" by (rule supteq_imp_vars_term_subset)
with nfs[unfolded NF_subst_def vars_rule_def]
have "σ ` vars_term ri ⊆ NF_terms Q" by auto
with ri_red
show "Inl () ∈ vars_term (ecap R Q (?mv ` get_args b l) (?mv (rs ! ?i)))"
unfolding ri_def[symmetric]
proof (induct ri arbitrary: C)
case (Var x C)
hence "σ x ⊵ redex" and "σ x ∈ NF_terms Q" by auto
with vars[of x] show ?case by auto
next
case (Fun f rs C)
show ?case
proof (cases C)
case Hole
have id: "get_args b l ⋅⇩s⇩e⇩t σ = ?mv ` get_args b l ⋅⇩s⇩e⇩t mv_subst σ"
using mv_xvar[of _ σ] by auto
from Hole Fun have "Fun f rs ⋅ σ = redex" by simp
with redex have "(Fun f rs ⋅ σ, r') ∈ (qrstep nfs Q R)⇧* O rqrstep nfs Q R" by auto
also have "Fun f rs ⋅ σ = Fun f (map ?mv rs) ⋅ mv_subst σ"
unfolding mv_xvar[of _ σ] by simp
finally have "cap R Q (?mv ` get_args b l) ((Fun f (map ?mv rs))) = Var (Inl ())"
using args[unfolded id]
by force
from cap_Fun_fresh[OF ecap this]
show ?thesis by auto
next
case (More g bef D aft)
let ?i = "length bef"
note id = Fun(2)[unfolded More]
from arg_cong[OF id, of num_args] have len: "length rs = Suc (?i + length aft)" by simp
with arg_cong[OF id, of "λ t. args t ! ?i"] have id: "rs ! ?i ⋅ σ = D⟨redex⟩" by auto
from len have mem: "rs ! ?i ∈ set rs" by auto
from Fun(1)[OF mem id] Fun(3) mem
have IH: "Inl () ∈ vars_term (ecap R Q (?mv ` get_args b l) (?mv (rs ! ?i)))" by auto
with ecap_Fun[OF ecap, of R Q "?mv ` get_args b l" f "map ?mv rs"]
show ?thesis using mem by auto
qed
qed
qed
qed
next
assume "∃ x q1 q2. q1 ∈ poss r ∧ q2 ∈ poss (σ x) ∧
r |_ q1 = Var x ∧ x ∈ vars_term r ∧ ?hp = q1 <#> q2 ∧ r ⋅ σ |_ ?hp = σ x |_ q2"
then obtain x q2 where x: "x ∈ vars_term r" and idd: "r ⋅ σ |_ ?hp = σ x |_ q2"
and q2: "q2 ∈ poss (σ x)" by auto
from idd[unfolded id] have "(More f bef C aft)⟨redex⟩ = σ x |_ q2" by simp
with q2 have "σ x ⊵ redex"
by (metis ctxt_imp_supteq subt_at_imp_supteq subterm.le_imp_less_or_eq subterm.order.strict_trans2 supt_imp_supteq)
with vars[of x] have "σ x ∉ NF_terms Q" by auto
with nfs x have False unfolding NF_subst_def vars_rule_def by auto
thus ?thesis by auto
qed
thus ?case using IH by simp
qed simp
lemma hirokawa_moser_4_7_1_and_DPs:
assumes wfP: "wf_trs P"
and P: "P ⊆ P'"
and s_af: "s ∈ af_nf_compatible_terms (μ_i_P P') (qrstep nfs Q R)"
and step: "(s,t) ∈ qrstep nfs Q R ∪ NF_terms Q × UNIV ∩ rrstep P"
shows "t ∈ af_nf_compatible_terms (μ_i_P P') (qrstep nfs Q R)"
proof -
note d = af_nf_compatible_terms_def
let ?NF = "NF (qrstep nfs Q R)"
let ?μ_i = "μ_i_P P'"
note wwf = wf wf_trs_imp_wwf_qtrs[OF wfP, of Q]
show ?thesis unfolding d
proof (rule, intro allI impI)
fix D u
assume tD: "t = D⟨u⟩"
let ?prop = "λ C σ l r b. s = C⟨l ⋅ σ⟩ ∧ t = C⟨r ⋅ σ⟩ ∧ get_args b l ⋅⇩s⇩e⇩t σ ⊆ NF_terms Q
∧ ((l,r),b) ∈ R × {True} ∪ P × {False} ∧ NF_subst True (l, r) σ Q
∧ ((l ⋅ σ, r ⋅ σ) ∈ qrstep nfs Q R ∨ C = Hole)"
from step have "∃ C σ l r b. ?prop C σ l r b"
proof
assume step: "(s,t) ∈ qrstep nfs Q R"
from qrstepE[OF step[unfolded wwf_qtrs_imp_nfs_switch[OF wwf(1), of nfs True]]]
obtain C σ l r where
NF: "∀u⊲l ⋅ σ. u ∈ NF_terms Q" and
lr: "(l, r) ∈ R" and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩"
and nfs: "NF_subst True (l, r) σ Q" .
from nfs have nfs_F: "NF_subst nfs (l,r) σ Q" unfolding NF_subst_def by auto
from NF lr nfs_F have rstep: "(l ⋅ σ, r ⋅ σ) ∈ qrstep nfs Q R" by auto
from NF[folded NF_terms_args_conv]
have "set (args l) ⋅⇩s⇩e⇩t σ ⊆ NF_terms Q" by (cases l, auto)
hence "?prop C σ l r True"
by (intro conjI s t, insert lr nfs rstep, auto)
thus ?thesis by metis
next
assume "(s,t) ∈ NF_terms Q × UNIV ∩ rrstep P"
from this[unfolded rrstep_def']
obtain σ l r where
NF: "l ⋅ σ ∈ NF_terms Q" and
lr: "(l, r) ∈ P" and s: "s = l ⋅ σ" and t: "t = r ⋅ σ" by auto
have "NF_subst True (l,r) σ Q" using NF unfolding NF_subst_def
proof (intro impI subsetI)
fix t
assume "t ∈ σ ` vars_rule (l,r)"
with wf wfP lr have "t ∈ σ ` vars_term l" unfolding wf_trs_def vars_rule_def by force
with supteq_subst[OF supteq_Var, of _ l σ]
have "l ⋅ σ ⊵ t" by auto
with NF_subterm[OF NF] show "t ∈ NF_terms Q" by auto
qed
hence "?prop Hole σ l r False"
by (insert s t lr NF, auto)
thus ?thesis by metis
qed
then obtain C σ l r b where "?prop C σ l r b" by metis
hence s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩"
and *: "((l, r), b) ∈ R × {True} ∪ P' × {False}" "get_args b l ⋅⇩s⇩e⇩t σ ⊆ NF_terms Q"
and nfs: "NF_subst True (l, r) σ Q" and rstep: "C = Hole ∨ (l ⋅ σ, r ⋅ σ) ∈ qrstep nfs Q R"
using P by auto
note main = hirokawa_moser_4_7_1_main[OF _ * nfs]
let ?l = "l ⋅ σ" let ?r = "r ⋅ σ"
show "af_regarded_pos ?μ_i t (hole_pos D) ∨ u ∈ ?NF"
proof (cases "u ∈ ?NF")
case False note u = this
from s_af[unfolded d] have s_af: "⋀ D u. s = D⟨u⟩ ⟹ af_regarded_pos ?μ_i s (hole_pos D) ∨ u ∈ ?NF" by auto
from s_af[OF s] rstep have reg1: "af_regarded_pos ?μ_i s (hole_pos C)" by auto
from s_af[of _ u] False have reg2: "⋀ D. s = D⟨u⟩ ⟹ af_regarded_pos ?μ_i s (hole_pos D)" by auto
from reg1 reg2 have "af_regarded_pos ?μ_i t (hole_pos D)" using tD unfolding t s
proof (induct C arbitrary: D)
case (More f bef C aft D) note C = this
let ?i = "length bef"
let ?n = "Suc (length bef + length aft)"
from C(2) have i: "?i ∈ ?μ_i (f,?n)" and reg: "af_regarded_pos ?μ_i (C ⟨?l⟩) (hole_pos C)" by auto
show ?case
proof (cases D)
case (More g bbef DD aaft) note D = this
let ?i' = "length bbef"
show ?thesis
proof (cases "?i' = ?i")
case True
with C(4)[unfolded D] have id: "C⟨r ⋅ σ⟩ = DD⟨u⟩" by auto
have "af_regarded_pos ?μ_i C⟨r ⋅ σ⟩ (hole_pos DD)"
proof (rule C(1)[OF reg _ id])
fix DD
assume "C⟨l ⋅ σ⟩ = DD⟨u⟩"
with C(3)[of "More f bef DD aft"] reg
show "af_regarded_pos ?μ_i C⟨l ⋅ σ⟩ (hole_pos DD)" by auto
qed
thus ?thesis using True i unfolding D by simp
next
case False note neq = this
from C(4)[unfolded D]
have id: "bef @ C⟨r ⋅ σ⟩ # aft = bbef @ DD⟨u⟩ # aaft" by simp
from arg_cong[OF id, of length] have i': "?i' < ?n" by simp
from arg_cong[OF id, of "λ ts. ts ! ?i'"]
have idd: "DD⟨u⟩ = (bef @ C⟨?r⟩ # aft) ! ?i'" by simp
show ?thesis
proof (cases "?i < ?i'")
case False
with neq have i': "?i' < ?i" by auto
hence bef: "bef ! ?i' = DD⟨u⟩" unfolding idd by (auto simp: nth_append)
from id_take_nth_drop[OF i', unfolded bef] i' obtain b1 b2 where
bef: "bef = b1 @ DD⟨u⟩ # b2" and len: "length b1 = ?i'" by auto
from C(3)[unfolded bef, of "More f b1 DD (b2 @ C⟨l ⋅ σ⟩ # aft)"]
have "length b1 ∈ ?μ_i (f, Suc (Suc (length b1 + (length b2 + length aft))))"
and "af_regarded_pos ?μ_i DD⟨u⟩ (hole_pos DD)" by auto
thus ?thesis unfolding bef D using len
by (simp add: nth_append)
next
case True
def i'' ≡ "?i' - Suc ?i"
from True i''_def i' have i': "?i' = Suc ?i + i''" and i'': "i'' < length aft" by auto
have aft: "aft ! i'' = DD⟨u⟩" unfolding idd i' by (auto simp: nth_append)
from id_take_nth_drop[OF i'', unfolded aft] i'' obtain a1 a2 where
aft: "aft = a1 @ DD⟨u⟩ # a2" and len: "length a1 = i''" by auto
from C(3)[unfolded aft, of "More f (bef @ C⟨l ⋅ σ⟩ # a1) DD a2"]
have " Suc (?i + length a1) ∈ ?μ_i (f, Suc (Suc (?i + (length a1 + length a2))))"
and "af_regarded_pos ?μ_i ((bef @ C⟨l ⋅ σ⟩ # a1 @ DD⟨u⟩ # a2) ! Suc (?i + length a1)) (hole_pos DD)"
by auto
thus ?thesis unfolding aft D using len
by (simp add: nth_append i')
qed
qed
qed simp
next
case (Hole D)
let ?hp = "hole_pos D"
from Hole have idd: "r ⋅ σ = D⟨u⟩" by simp
from False obtain v where "(u,v) ∈ qrstep nfs Q R" unfolding NF_def by auto
{
from qrstepE[OF this]
obtain E σ' l' r' where
NF: "∀u⊲l' ⋅ σ'. u ∈ NF_terms Q" and
lr: "(l', r') ∈ R" and u: "u = E⟨l' ⋅ σ'⟩" and v: "v = E⟨r' ⋅ σ'⟩"
and nfs: "NF_subst nfs (l', r') σ' Q" .
hence "(l' ⋅ σ', r' ⋅ σ') ∈ rqrstep nfs Q R" by auto
with u have "∃ E red r'. u = E⟨red⟩ ∧ (red,r') ∈ rqrstep nfs Q R" by auto
}
then obtain E red r' where u: "u = E⟨red⟩" and red: "(red,r') ∈ rqrstep nfs Q R" by auto
def rr ≡ "r ⋅ σ"
from main[OF red, of "D ∘⇩c E"] idd[unfolded u]
have "af_regarded_pos ?μ_i (r ⋅ σ) (hole_pos (D ∘⇩c E))" by auto
thus ?case unfolding ctxt_apply_term.simps rr_def[symmetric]
by (simp add: af_regarded_pos_append)
qed
thus ?thesis by simp
qed simp
qed
qed
lemma hirokawa_moser_4_7_1:
assumes s_af: "s ∈ af_nf_compatible_terms (μ_i_P P) (qrstep nfs Q R)"
and step: "(s,t) ∈ qrstep nfs Q R"
shows "t ∈ af_nf_compatible_terms (μ_i_P P) (qrstep nfs Q R)"
by (rule hirokawa_moser_4_7_1_and_DPs[OF _ _ s_af, of "{}"], insert step, auto simp: wf_trs_def)
lemma hirokawa_moser_4_7_1_star:
assumes s_af: "s ∈ af_nf_compatible_terms (μ_i_P P) (qrstep nfs Q R)"
shows "(s,t) ∈ (qrstep nfs Q R)^* ⟹ t ∈ af_nf_compatible_terms (μ_i_P P) (qrstep nfs Q R)"
by (induct rule: rtrancl_induct, rule s_af, rule hirokawa_moser_4_7_1)
lemma runtime_complexity_af_nf_compatible:
fixes T :: "('f,string)terms" and C D :: "('f × nat)list"
defines "T ≡ terms_of (Runtime_Complexity C D)"
assumes C: "⋀ c. c ∈ set C ⟹ ¬ defined R c"
and s: "s ∈ T"
shows "s ∈ af_nf_compatible_terms μ (qrstep nfs Q R)"
proof -
from s[unfolded T_def] obtain f cs where
s: "s = Fun f cs" and f: "(f,length cs) ∈ set D" and
cs: "⋀ c. c ∈ set cs ⟹ funas_term c ⊆ set C" by (force simp: funas_args_term_def)
show ?thesis unfolding s af_nf_compatible_terms_def
proof (rule, intro allI impI)
fix D u
assume id: "Fun f cs = D⟨u⟩"
show "af_regarded_pos μ (Fun f cs) (hole_pos D) ∨ u ∈ NF (qrstep nfs Q R)"
proof (cases D)
case (More g bef E aft)
with id have "E⟨u⟩ ∈ set cs" by auto
from cs[OF this] have u: "funas_term u ⊆ set C" by auto
{
fix v
assume "(u,v) ∈ qrstep nfs Q R"
from qrstepE[OF this]
obtain F l r σ where uu: "u = F⟨l⋅σ⟩" and lr: "(l,r) ∈ R" and NF: "∀u⊲l ⋅ σ. u ∈ NF_terms Q" .
from wwf_qtrs_imp_left_fun[OF wf lr] obtain f ls where l: "l = Fun f ls" by blast
let ?n = "length ls"
from u[unfolded uu l] have "(f,?n) ∈ set C" by auto
from C[OF this] lr[unfolded l] have False unfolding defined_def by auto
}
hence "u ∈ NF (qrstep nfs Q R)" by auto
thus ?thesis by auto
qed simp
qed
qed
theorem hirokawa_moser_4_8_1:
fixes T :: "('f,string)terms" and C D :: "('f × nat)list"
defines "T ≡ terms_of (Runtime_Complexity C D)"
assumes C: "⋀ c. c ∈ set C ⟹ ¬ defined R c"
shows "usable_replacement_map μ_i T nfs R Q R"
proof (unfold usable_replacement_map_def, rule)
fix t
assume "t ∈ (qrstep nfs Q R)⇧* `` T"
then obtain s where steps: "(s,t) ∈ (qrstep nfs Q R)⇧*" and s: "s ∈ T" by blast
show "t ∈ af_nf_compatible_terms μ_i (qrstep nfs Q R)" unfolding μ_i_def
by (rule hirokawa_moser_4_7_1_star[OF runtime_complexity_af_nf_compatible[OF C] steps],
insert s T_def, auto)
qed
lemma NF_imp_af_nf_compatible:
assumes NF: "s ∈ NF_terms Q"
shows "s ∈ af_nf_compatible_terms μ (qrstep nfs Q R)"
unfolding af_nf_compatible_terms_def
proof (rule, intro allI impI disjI2)
fix C t
assume "s = C⟨t⟩"
hence "s ⊵ t" by auto
from NF_subterm[OF NF this] inn have "t ∈ NF_trs R" by auto
thus "t ∈ NF (qrstep nfs Q R)" by blast
qed
theorem urm_for_DP:
assumes P: "(s,t) ∈ P"
and NF: "s ⋅ σ ∈ NF_terms Q"
and wfP: "wf_trs P"
shows "usable_replacement_map (μ_i_P P) {t ⋅ σ} nfs R Q R"
proof (unfold usable_replacement_map_def, rule)
fix u
assume "u ∈ (qrstep nfs Q R)⇧* `` {t ⋅ σ}"
hence steps: "(t ⋅ σ, u) ∈ (qrstep nfs Q R)⇧*" by auto
from P NF have P: "(s ⋅ σ, t ⋅ σ) ∈ NF_terms Q × UNIV ∩ rrstep P" unfolding rrstep_def' by auto
show "u ∈ af_nf_compatible_terms (μ_i_P P) (qrstep nfs Q R)"
by (rule hirokawa_moser_4_7_1_star[OF hirokawa_moser_4_7_1_and_DPs[OF wfP subset_refl
NF_imp_af_nf_compatible[OF NF]] steps], insert P, auto)
qed
text ‹The following approximation of usable replacement maps is a refinement
of the one that is used within AProVE (as it is described in the JAR11 induction paper
of Carsten, Juergen, et al.).
The refinement integrated so far is using icap instead of just symbol comparisons›
context
fixes U :: "('f,string)term list ⇒ ('f,string)term ⇒ ('f,string)trs"
and init :: "(('f,string)term list × ('f,string)term × ('f,string)rule)set"
assumes U: "usable_rules_approx Q R True U"
begin
lemma approx_cond_main:
assumes σ: "σ ` vars_term t ⊆ NF_terms Q" "set ss ⋅⇩s⇩e⇩t σ ⊆ NF_terms Q"
and steps: "(t ⋅ σ, C⟨l ⋅ δ⟩) ∈ (qrstep nfs Q R)^*"
and step: "(C⟨l ⋅ δ⟩, C⟨r ⋅ δ⟩) ∈ qrstep_r_p_s nfs Q R (l,r) (hole_pos C) δ"
and cond: "approx_cond U init ss t (l,r)"
shows "af_regarded_pos (μ_approx U init) (C⟨l ⋅ δ⟩) (hole_pos C)"
proof -
let ?approx_cond = "approx_cond U init"
let ?μ = "μ_approx U init"
note switch = wwf_qtrs_imp_nfs_switch[OF wf, of nfs True]
note step = step[unfolded wwf_qtrs_imp_nfs_switch_r_p_s[OF wf, of nfs True]]
note U = usable_rules_approxD[OF U]
let ?R = "qrstep True Q R"
let ?N = "nrqrstep True Q R"
from rtrancl_imp_UN_relpow[OF steps[unfolded switch]] obtain n where
steps: "(t ⋅ σ, C⟨l ⋅ δ⟩) ∈ ?R^^n" by auto
show ?thesis using σ steps step cond
proof (induct n arbitrary: ss t σ l r C δ rule: less_induct)
case (less n ss t σ l r C δ)
from inn have inn2: "NF_terms Q ⊆ NF ?R" by force
{
fix t u n
assume tu: "(t,u) ∈ ?R^^n" and t: "t ∈ NF ?R"
have "n = 0"
proof (cases n)
case (Suc m)
from tu[unfolded Suc] obtain v where tv: "(t,v) ∈ ?R" by blast
with t show ?thesis by auto
qed simp
} note NF_steps_0 = this
from less.prems
show ?case
proof (induct t arbitrary: ss σ l r C δ)
case (Var x)
with inn2 have NF: "σ x ∈ NF ?R" by auto
with Var(3) NF_steps_0[OF Var(3)] have C: "C ⟨ l ⋅ δ ⟩ = σ x" by simp
from Var(4)[unfolded C] have "(σ x, C ⟨ r ⋅ δ ⟩) ∈ ?R^^1" using qrstep_qrstep_r_p_s_conv[of _ _ True Q R]
unfolding switch by auto
from NF_steps_0[OF this NF] show ?case by simp
next
case (Fun f ts ss σ l r C δ)
let ?n = "length ts"
show ?case
proof (cases "(Fun f ts ⋅ σ, C⟨l ⋅ δ⟩) ∈ ?N^^n")
case True
show ?thesis
proof (cases C)
case (More g bef D aft)
let ?i = "length bef"
let ?m = "Suc (?i + length aft)"
from nrqrsteps_preserve_root[OF relpow_imp_rtrancl[OF True], unfolded More]
have gf: "g = f" and mn: "?m = ?n" by auto
hence i: "?i < ?n" by auto
from nrqrsteps_imp_arg_qrsteps_count[OF True, of ?i] obtain m where m: "m ≤ n"
and steps: "(ts ! ?i ⋅ σ, D⟨l ⋅ δ⟩) ∈ ?R^^m" using i unfolding More by auto
from i have ti: "ts ! ?i ∈ set ts" by auto
from ti Fun(2) have σ: "σ ` vars_term (ts ! ?i) ⊆ NF_terms Q" by auto
from Fun(5) have step: "(D⟨l ⋅ δ⟩, D⟨r ⋅ δ⟩) ∈ qrstep_r_p_s True Q R (l, r) (hole_pos D) δ"
unfolding qrstep_r_p_s_def by auto
have U: "(l, r) ∈ U ss (ts ! ?i)"
by (rule U[OF σ Fun(3) relpow_imp_rtrancl[OF steps] step])
from approx_cond_sub[OF Fun(6) i U] μ_cond[OF Fun(6) i U]
have cond: "?approx_cond ss (ts ! ?i) (l,r)" and μ: "?i ∈ ?μ (f,?n)" unfolding μ_approx_def by auto
from steps m Fun(1)[OF ti σ Fun(3) _ step cond] less(1)[OF _ σ Fun(3) _ step cond]
have "af_regarded_pos ?μ D⟨l ⋅ δ⟩ (hole_pos D)" by (cases "m < n", auto)
with μ
show ?thesis unfolding More mn[symmetric] gf by simp
qed simp
next
case False
note qr = qrstep_iff_rqrstep_or_nrqrstep
from relpow_union_cases[OF Fun(4)[unfolded qr]] False
obtain u v m k where tu: "(Fun f ts ⋅ σ, u) ∈ ?N^^m"
and uv: "(u,v) ∈ rqrstep True Q R" and vl: "(v,C⟨l ⋅ δ⟩) ∈ ?R^^k" and n: "n = Suc (m + k)"
unfolding qr[symmetric] by blast
note tu = relpow_imp_rtrancl[OF tu]
from n have k: "k < n" by auto
from uv obtain l' r' σ' where u: "u = l' ⋅ σ'" and v: "v = r' ⋅ σ'" and lr': "(l',r') ∈ R"
and σ': "NF_subst True (l',r') σ' Q"
and NF1: "∀u⊲l' ⋅ σ'. u ∈ NF_terms Q" by auto
from only_applicable_rules[OF NF1] lr' wf
have "vars_term r' ⊆ vars_term l'" and l': "is_Fun l'" unfolding wwf_qtrs_def by force+
with σ' have σ': "σ' ` vars_term r' ⊆ NF_terms Q" unfolding NF_subst_def vars_rule_def by auto
from NF1 have NF: "set (args l') ⋅⇩s⇩e⇩t σ' ⊆ NF_terms Q" unfolding NF_terms_args_conv[symmetric]
using l' by (cases l', auto)
have rm: "rule_match R Q ecap (mv_xvar ` set ss) f (map mv_xvar ts) l'"
by (rule rule_matchI[OF ecap Fun(3) NF1 tu[unfolded u]])
have "?approx_cond (args l') r' (l, r)"
by (rule approx_cond_rec[OF Fun(6) lr' rm U[OF σ' NF relpow_imp_rtrancl[OF vl[unfolded v]] Fun(5)]])
from less(1)[OF k σ' NF vl[unfolded v] Fun(5) this]
show ?thesis .
qed
qed
qed
qed
context
fixes S :: "('f,string)trs"
assumes S: "S ⊆ R"
begin
lemma approx_cond:
assumes σ: "σ ` vars_term t ⊆ NF_terms Q" "set ss ⋅⇩s⇩e⇩t σ ⊆ NF_terms Q"
and steps: "(t ⋅ σ, u) ∈ (qrstep nfs Q R)^*"
and init: "{ss} × {t} × S ⊆ init"
shows "u ∈ af_nf_compatible_terms (μ_approx U init) (qrstep nfs Q S)"
unfolding af_nf_compatible_terms_def
proof (rule, intro allI impI)
fix C s
let ?μ = "μ_approx U init"
assume u: "u = C ⟨ s ⟩"
show "af_regarded_pos ?μ u (hole_pos C) ∨ s ∈ NF (qrstep nfs Q S)"
proof (cases "s ∈ NF (qrstep nfs Q S)")
case False
then obtain v where sv: "(s,v) ∈ qrstep nfs Q S" by blast
from this[unfolded qrstep_qrstep_r_p_s_conv] obtain lr p δ
where step: "(s,v) ∈ qrstep_r_p_s nfs Q S lr p δ" by blast
obtain l r where lr: "lr = (l,r)" by force
from step[unfolded lr] S have lrS: "(l,r) ∈ S" and step: "(s,v) ∈ qrstep_r_p_s nfs Q R (l,r) p δ"
unfolding qrstep_r_p_s_def by auto
from qrstep_r_p_s_conv[OF step[unfolded lr]] obtain D where s: "s = D ⟨ l ⋅ δ ⟩" and v: "v = D ⟨ r ⋅ δ ⟩"
and p: "p = hole_pos D" by auto
let ?C = "C ∘⇩c D"
from step[unfolded s v p lr] have step: "(?C ⟨ l ⋅ δ ⟩, ?C ⟨ r ⋅ δ ⟩) ∈ qrstep_r_p_s nfs Q R (l,r) (hole_pos ?C) δ"
unfolding qrstep_r_p_s_def by (simp, induct C, auto)
from u s have u: "u = ?C ⟨ l ⋅ δ ⟩" by simp
from init lrS have "(ss,t,(l,r)) ∈ init" by auto
from approx_cond_main[OF σ steps[unfolded u] step approx_cond_init[OF this]]
have "af_regarded_pos ?μ (?C⟨l ⋅ δ⟩) (hole_pos ?C)" .
hence "af_regarded_pos ?μ (?C⟨l ⋅ δ⟩) (hole_pos C)"
by (induct C, auto)
thus ?thesis unfolding u ..
qed simp
qed
theorem aprove_urm_complexity:
fixes T :: "('f,string)terms" and C D :: "('f × nat)list" and name :: string
defines "T ≡ terms_of (Runtime_Complexity C D)"
and "gen_xs ≡ λ n. (map Var (x⇩1_to_x⇩n n)) :: ('f,string)term list"
assumes C: "⋀ c. c ∈ set C ⟹ ¬ defined R c"
and approx: "⋀ f n. (f,n) ∈ set D
⟹ {gen_xs n} × {(Fun f (gen_xs n))} × S ⊆ init"
shows "usable_replacement_map (μ_approx U init) T nfs R Q S"
proof (unfold usable_replacement_map_def, rule)
let ?μ = "μ_approx U init"
fix t
assume "t ∈ (qrstep nfs Q R)⇧* `` T"
then obtain s where steps: "(s,t) ∈ (qrstep nfs Q R)⇧*" and s: "s ∈ T" by blast
from s[unfolded T_def, simplified] obtain f ss where s: "s = Fun f ss"
and funas: "⋀ si. si ∈ set ss ⟹ funas_term si ⊆ set C" and D: "(f,length ss) ∈ set D"
by (cases s, auto simp: funas_args_term_def)
let ?n = "length ss"
def xs ≡ "x⇩1_to_x⇩n ?n"
have xs: "length xs = ?n" unfolding xs_def by simp
def σ ≡ "inv_x⇩1_to_x⇩n ss"
from inv_x⇩1_to_x⇩n[of ss, folded σ_def xs_def]
have ss: "ss = map σ xs" by simp
hence s: "s = Fun f (map Var xs) ⋅ σ" unfolding s by (simp add: o_def)
show "t ∈ af_nf_compatible_terms ?μ (qrstep nfs Q S)"
proof (cases "set ss ⊆ NF_terms Q")
case True
show ?thesis
proof (rule approx_cond[OF _ _ steps[unfolded s] approx[OF D, unfolded gen_xs_def, folded xs_def]], rule)
from True show "set (map Var xs) ⋅⇩s⇩e⇩t σ ⊆ NF_terms Q" using ss by auto
fix u
assume "u ∈ σ ` vars_term (Fun f (map Var xs))"
then obtain i where u: "u = σ (xs ! i)" and i: "i < length xs"
by (auto simp: set_conv_nth)
have u: "u = ss ! i" unfolding ss u using i xs by auto
with i xs have "u ∈ set ss" by auto
with True
show "u ∈ NF_terms Q" by auto
qed
next
case False
from ‹s ∈ T› T_def have s: "s ∈ terms_of (Runtime_Complexity C D)" by auto
from runtime_complexity_af_nf_compatible[OF C this]
have s: "⋀ μ. s ∈ af_nf_compatible_terms μ (qrstep nfs Q R)" by simp
have "s = t"
proof (cases rule: converse_rtranclE[OF steps])
fix u
assume "(s,u) ∈ qrstep nfs Q R"
then obtain C l r σ where "(l,r) ∈ R" and NF: "⋀ u. u⊲l ⋅ σ ⟹ u ∈ NF_terms Q" and su: "s = C⟨l ⋅ σ⟩" "u = C⟨r ⋅ σ⟩" and step: "(l ⋅ σ, r ⋅ σ) ∈ qrstep nfs Q R"
by blast
have False
proof (cases C)
case (More f bef D aft)
from s[of "λ _. {}", unfolded af_nf_compatible_terms_def, simplified, rule_format, OF su(1)[unfolded More]] step
show False by auto
next
case Hole
with su(1) ‹s = Fun f ss› have l: "l ⋅ σ = Fun f ss" by auto
from False obtain si where si: "si ∈ set ss" and "si ∉ NF_terms Q" by auto
with NF[unfolded l, of si]
show False by auto
qed
thus "s = t" by simp
qed
with s have t: "t ∈ af_nf_compatible_terms ?μ (qrstep nfs Q R)" by auto
show ?thesis
by (rule set_mp[OF af_nf_compatible_terms_mono[OF qrstep_mono[OF S]] t]) auto
qed
qed
theorem aprove_urm_for_DP:
assumes P: "(s,t) ∈ P"
and NF: "s ⋅ σ ∈ NF_terms Q"
and approx: "{[s]} × {t} × S ⊆ init"
and wfP: "wf_trs P"
shows "usable_replacement_map (μ_approx U init) {t ⋅ σ} nfs R Q S"
unfolding usable_replacement_map_def
proof
let ?μ = "μ_approx U init"
fix u
assume "u ∈ (qrstep nfs Q R)⇧* `` {t ⋅ σ}"
hence steps: "(t ⋅ σ, u) ∈ (qrstep nfs Q R)⇧*" by simp
show "u ∈ af_nf_compatible_terms ?μ (qrstep nfs Q S)"
proof (rule approx_cond[OF _ _ steps approx], rule)
show "set [s] ⋅⇩s⇩e⇩t σ ⊆ NF_terms Q" using NF by simp
fix v
assume "v ∈ σ ` vars_term t"
then obtain x where v: "v = σ x" and x: "x ∈ vars_term t" by auto
with wfP P have x: "x ∈ vars_term s" unfolding wf_trs_def by auto
hence "s ⊵ Var x" by auto
from NF_subterm[OF NF supteq_subst[OF this, of σ]]
show "v ∈ NF_terms Q" unfolding v by simp
qed
qed
end
end
end
end
lemma avanzini_14_34: assumes us: "usable_replacement_map μ (terms_of cm) nfs (RS ∪ R) Q RS'"
and DP: "is_DP_complexity Cp FS F RS R cm"
and RS': "RS' ⊆ RS"
and μ_com: "⋀ f. f ∈ Cp ⟹ μ_com f ⊇ μ f"
shows "usable_replacement_map μ_com (terms_of cm) nfs (RS ∪ R) Q RS'"
unfolding usable_replacement_map_def
proof
fix t
assume tt: "t ∈ (qrstep nfs Q (RS ∪ R))⇧* `` terms_of cm"
with avanzini_14_20(2)[OF DP] have t: "t ∈ Tsharp_terms Cp FS F" by auto
from tt us[unfolded usable_replacement_map_def]
have tt: "t ∈ af_nf_compatible_terms μ (qrstep nfs Q RS')" by auto
note d = af_nf_compatible_terms_def
show "t ∈ af_nf_compatible_terms μ_com (qrstep nfs Q RS')" unfolding d
proof (rule, intro allI impI)
fix C s
assume ts: "t = C⟨s⟩"
with tt[unfolded d] have af: "af_regarded_pos μ t (hole_pos C) ∨ s ∈ NF (qrstep nfs Q RS')" by auto
show "af_regarded_pos μ_com t (hole_pos C) ∨ s ∈ NF (qrstep nfs Q RS')"
proof (cases "s ∈ NF (qrstep nfs Q RS')")
case False
with af have af: "af_regarded_pos μ t (hole_pos C)" by auto
from False obtain u where "(s,u) ∈ qrstep nfs Q RS'" unfolding NF_def by auto
{
from qrstepE[OF this] obtain l r C σ where lr: "(l,r) ∈ RS'" and s: "s = C⟨l ⋅ σ⟩" .
from lr RS' have lr: "(l,r) ∈ RS" by auto
from DP have "wf_trs RS" and RS: "lhss RS ⊆ Fsharp_terms FS F" by (cases, auto)+
from wf_trs_imp_lhs_Fun[OF this(1) lr] obtain f ls where l: "l = Fun f ls" by auto
from RS lr have "l ∈ Fsharp_terms FS F" by auto
from this[unfolded l] have "(f,length ls) ∈ FS" by (cases, auto)
with s l have "funas_term s ∩ FS ≠ {}" by simp
} note s_FS = this
from DP have FS_F: "FS ∩ F = {}" by (cases, auto)
with s_FS have sF: "¬ funas_term s ⊆ F" by auto
from t ts af have "af_regarded_pos μ_com t (hole_pos C)"
proof (induct t arbitrary: C)
case (compound f ts C)
show ?case
proof (cases C)
case (More g bef D aft) note C = this
let ?i = "length bef"
let ?n = "length ts"
from compound(1) have "(f,?n) ∈ Cp" by simp
note μ_com = μ_com[OF this]
from compound(5)[unfolded C]
have i[simp]: "?i < ?n"
and mu: "?i ∈ μ (f, ?n)"
and af: "af_regarded_pos μ (ts ! ?i) (hole_pos D)" by auto
from mu μ_com have [simp]: "?i ∈ μ_com (f,?n)" by auto
have [simp]: "af_regarded_pos μ_com (ts ! ?i) (hole_pos D)"
by (rule compound(3)[OF _ _ af], insert i compound(4) C, auto)
show ?thesis unfolding C by simp
qed simp
next
case (base t C)
with sF have False by auto
thus ?case by simp
next
case (sharp t C)
show ?case
proof (cases C)
case (More g bef D aft)
from sharp(1)[unfolded sharp(2) More]
have "funas_term s ⊆ F" by (cases, force)
with sF have False by simp
thus ?thesis by simp
qed simp
qed
thus ?thesis ..
qed simp
qed
qed
end