theory DP_Transformation_Impl
imports
TA.DP_Transformation
QTRS.Linear_Orders
QTRS.QDP_Framework_Impl
"../Rewriting/Q_Restricted_Rewriting_Impl"
begin
context
fixes shp :: "'f ⇒ 'f"
begin
interpretation sharp_syntax .
definition DP_list :: "('f, 'v) rules ⇒ ('f × nat) list ⇒ ('f, 'v) rules"
where
"DP_list R d_list =
concat (map (λlr.
let l = fst lr; s = ♯ l in
map (λu. (s, ♯ u)) (filter
(λu. ¬ l ⊳ u ∧ is_Fun u ∧ (the (root u)) ∈ set d_list) (supteq_list (snd lr)))) R)"
lemma DP_list [simp]:
shows "set (DP_list R F) = DP_on ♯ (set F) (set R)" (is "?L = ?R")
proof
show "?L ⊆ ?R"
proof
fix s t assume "(s, t) ∈ ?L"
then obtain l r u where "(l, r) ∈ set R" and "r ⊵ u" and "¬ l ⊳ u"
and "s = ♯ l" and "t = ♯ u"
and "is_Fun u" and "the (root u) ∈ set F"
unfolding DP_list_def Let_def by auto
thus "(s, t) ∈ DP_on ♯ (set F) (set R)" unfolding DP_on_def by (cases u) auto
qed
next
show "?R ⊆ ?L"
proof
fix s t assume "(s, t) ∈ ?R"
then obtain lr u where "lr ∈ set R" and "snd lr ⊵ u" and "¬ fst lr ⊳ u"
and "s = ♯ (fst lr)" and "t = ♯ u"
and "is_Fun u" and "the (root u) ∈ set F" unfolding DP_on_def by auto
thus "(s, t) ∈ ?L" unfolding DP_list_def Let_def by auto
qed
qed
end
context
fixes shp :: "'f ⇒ 'f::{show, linorder}"
begin
interpretation sharp_syntax .
definition
dependency_pairs_tt ::
"('tp, 'f::{show,linorder}, 'v::{show,linorder}) tp_ops ⇒
('dpp, 'f, 'v) dpp_ops ⇒ 'tp ⇒ bool ⇒ bool ⇒ ('f, 'v) rules ⇒ 'dpp result"
where
"dependency_pairs_tt I J tp nfs m P ≡
let R = tp_ops.rules I tp;
Q = tp_ops.Q I tp;
iQ = tp_ops.is_QNF I tp;
U = filter (applicable_rule_impl iQ) R
in
check_return (do {
(if isOK(check_wf_trs U) then succeed else
check (nfs ∧ tp_ops.nfs I tp ∧ tp_ops.NFQ_subset_NF_rules I tp ∧ (∀ l ∈ set (map fst R). is_Fun l))
(shows ''neither is the TRS well-formed, nor is the restriction to innermost with normal form substitutions present''));
check_allm (λ q. check_no_var q) Q;
let Qr = map (λ q. case q of Fun f ss ⇒ (f,length ss)) Q;
let D = defined_list U;
check_allm (λ (f,n). check ((♯ f,n) ∉ set D) (shows_string ''sharping '' +@+ shows f +@+ shows_string '' yields the defined symbol '' +@+ shows (♯ f))) D;
check_allm (λ (f,n). check ((♯ f,n) ∉ set Qr) (shows_string ''sharping '' +@+ shows f +@+ shows_string '' yields the symbol '' +@+ shows (♯ f) +@+ shows_string '' which is a root of Q'')) D;
let P' = set P;
check_all (λ dp. dp ∈ P' ∨ (∃ dp' ∈ set P. dp =⇩v dp')) (DP_list ♯ U D)
<+? (λdp. ''the DP '' +#+ shows_rule dp
+@+ '' does not appear in the DP problem'' +#+ shows_nl)
} <+? (λs. ''the DP-transformation is not applied correctly.'' +#+ shows_nl +@+ s))
(dpp_ops.mk J nfs m P [] Q [] R)"
lemma dependency_pairs_tt:
assumes I: "tp_spec I"
and J: "dpp_spec J"
and tt: "dependency_pairs_tt I J tp nfs m P = return d"
and fin: "finite_dpp (dpp_ops.dpp J d)"
shows "SN_qrel (tp_ops.qreltrs I tp)"
proof -
interpret tp_spec I by fact
interpret spec: dpp_spec J by fact
let ?R = "set (R tp)"
let ?Rw = "set (Rw tp)"
let ?Q = "set (Q tp)"
let ?Qr = "map (λq. case q of Fun f ss ⇒ (f, length ss)) (Q tp)"
let ?nfs = "NFS tp"
let ?B = "set (R tp) ∪ set (Rw tp)"
let ?u = "{x. (x ∈ set (R tp) ∨ x ∈ set (Rw tp)) ∧ applicable_rule ?Q x}"
let ?U = "applicable_rules ?Q ?B"
have u: "?u = ?U" by (auto simp: applicable_rules_def)
note tt = tt[unfolded dependency_pairs_tt_def Let_def, simplified]
note ttu = tt[unfolded u]
from tt have idpp: "d = dpp_ops.mk J nfs m P [] (Q tp) [] (rules tp)" by auto
from ttu have P: "⋀ dp. dp ∈ DP ♯ ?U ⟹ dp ∈ set P ∨ (∃ dp' ∈ set P. dp =⇩v dp')" by (auto simp: u)
have wf: "wf_qtrs nfs ?Q ?B ∧ qrstep nfs ?Q ?B = qrstep ?nfs ?Q ?B"
proof (cases "wf_trs ?U")
case True
have "wwf_qtrs ?Q ?B" using True unfolding wwf_qtrs_def u[symmetric] wf_trs_def by auto
with wwf_qtrs_imp_nfs_switch[OF this, of nfs ?nfs]
show ?thesis using ttu unfolding wf_qtrs_def by auto
next
case False
with ttu
have "nfs ∧ ?nfs ∧ NF_terms (set (Q tp)) ⊆ NF_trs (set (rules tp)) ∧ (∀t∈lhss (set (rules tp)). is_Fun t)" by auto
thus ?thesis unfolding wf_qtrs_def wwf_inn_qtrs_def using ttu by auto
qed
hence wf: "wf_qtrs nfs ?Q ?B" and switch: "qrstep nfs ?Q ?B = qrstep ?nfs ?Q ?B" by blast+
have SN: "SN (qrstep nfs ?Q ?B)"
proof (rule ccontr)
assume nSN: "¬ ?thesis"
have easy: "⋀ p. ⟦ ⋀ f n. p f n⟧ ⟹ True = (∀ f n. p f n)" by blast
have "∃ s t σ. min_ichain (initial_dpp ♯ nfs True ?Q ?B) s t σ"
proof (rule not_SN_imp_min_ichain[OF wf nSN _ easy])
fix f n
show "defined (applicable_rules ?Q ?B) (f, n) ⟶
¬ defined (applicable_rules ?Q ?B) (♯ f, n)" using ttu by auto
next
fix f n and ss :: "('f, 'b) term list"
assume d: "defined (applicable_rules ?Q ?B) (f,n)" "length ss = n"
with ttu have not: "(♯ f,n) ∉ set ?Qr" by auto
from d have n: "n = length ss" by auto
show "Fun (♯ f) ss ∉ ?Q" using not unfolding n by force
qed
then obtain s t σ where mic: "min_ichain (initial_dpp ♯ nfs True ?Q ?B) s t σ" by blast
hence mic: "min_ichain (initial_dpp ♯ nfs m ?Q ?B) s t σ" by (simp add: minimal_cond_def ichain.simps)
let ?P = "DP ♯ ?U"
let ?init = "(nfs, m, ?P, {}, ?Q, {}, ?B)"
from mic have inf: "¬ finite_dpp ?init" unfolding finite_dpp_def initial_dpp.simps by blast
have "finite_dpp
(nfs, m, ?P, {}, ?Q, set [], set (rules tp))"
proof (rule finite_dpp_rename_vars[OF fin[unfolded idpp dpp_spec.mk_sound[OF J]]])
fix dp
assume "dp ∈ ?P"
from P[OF this] show "∃dp'. dp' ∈ set P ∧ dp =⇩v dp'" using eq_rule_mod_vars_refl[of dp]
by blast
qed auto
with inf show False by auto
qed
with switch have "SN (qrstep ?nfs ?Q ?B)" by simp
hence SN: "SN_qrel (?nfs, ?Q, ?B, {})" by simp
show ?thesis unfolding qreltrs_sound
by (rule SN_qrel_mono[OF subset_refl _ _ SN]) simp_all
qed
end
end