section ‹AC Subterm Criterion -- Implementation›
theory AC_Subterm_Criterion_Impl
imports
"../Orderings/Subterm_Multiset"
"../Orderings/Status_Impl"
"Check-NT.Term_Order_Impl"
"../Auxiliaries/Multiset_Extension_Impl"
"Check-NT.AC_Dependency_Pair_Problem_Spec"
QTRS.Dependency_Pair_Problem_Spec
"../AC_Rewriting/AC_Rewriting_Impl"
AC_Subterm_Criterion
begin
lemma irrefl_subt: "irrefl {⊲}" by (auto simp: irrefl_def)
lemma suptmulexeq_impl [code_unfold]:
"M ⊵⇩# N = multeqp (λx y. supt_impl y x) N M"
proof -
have *: "multeqp (λx y. supt_impl y x) N M ⟷ (N, M) ∈ (mult {⊲})⇧="
by (rule multeqp_iff [OF irrefl_subt trans_subt]) (auto simp: supt_impl)
show ?thesis
using mult_subt_converse and suptmulex_eq
unfolding * by fastforce
qed
lemma suptmulex_impl [code_unfold]:
"M ⊳⇩# N ⟷ multeqp (λx y. supt_impl y x) N M ∧ M ≠ N"
by (auto simp: suptmulexeq_impl [symmetric] s_ns_mul_ext suptmulex_not_refl suptmulex_eq)
definition [simp]: "strict_supt_mul = suptproj_pred"
definition [simp]:"weak_supt_mul = suptprojeq_pred"
definition check_suptproj_pred :: "'f status ⇒ 'f sig ⇒ ('f :: show, 'v :: show)rule ⇒ shows check" where
"check_suptproj_pred π F lr = check (case lr of (l, r) ⇒ strict_supt_mul π F l r)
(shows ''could not orient rule '' o shows_rule lr o shows '' by supt^mul'')"
definition check_supteqproj_pred :: "'f status ⇒ 'f sig ⇒ ('f :: show, 'v :: show) rule ⇒ shows check" where
"check_supteqproj_pred π F lr = check (case lr of (l, r) ⇒ weak_supt_mul π F l r)
(shows ''could not orient rule '' o shows_rule lr o shows '' by supteq^mul'')"
lemma check_suptproj_pred [simp]:
"isOK (check_suptproj_pred π F lr) = suptproj_pred π F (fst lr) (snd lr)"
unfolding check_suptproj_pred_def by auto
lemma check_supteqproj_pred [simp]:
"isOK (check_supteqproj_pred π F lr) = suptprojeq_pred π F (fst lr) (snd lr)"
unfolding check_supteqproj_pred_def by auto
definition
ac_subterm_proc ::
"('dpp, 'f :: show, 'v :: show) ac_dpp_ops ⇒ 'f status_impl ⇒
('f, 'v)rules ⇒ 'dpp proc"
where
"ac_subterm_proc I pi P_remove dpp = check_return (do {
let P = ac_dpp_ops.pairs I dpp;
let R = ac_dpp_ops.rules I dpp;
let E = ac_dpp_ops.E I dpp;
let RE = R @ E;
let F = map fst pi;
let FF = set F;
let pi_opt = status_of pi;
check (pi_opt ≠ None) (shows ''argument filter lists invalid positions'');
let π = the pi_opt;
let Premove = set P_remove;
let (ps, pns) = partition (λ lr. lr ∈ Premove) P;
check_allm (λ f. check (status π f ≠ [])
(shows ''status of symbol '' o shows f o shows '' in F must be non-empty'')) F;
check_size_preserving_trs E
<+? (λ s. shows ''E is not size preserving⏎'' o s);
check_allm (λ (l,r). check (is_Fun l) (shows ''variables as lhss not allowed'')) RE;
check_allm (check_supteqproj_pred π FF) (filter (λ lr. the (root (fst lr)) ∈ FF) RE)
<+? (λs. shows ''problem when orienting rules with root in F⏎'' o s);
check_allm (check_supteqproj_pred π FF) pns
<+? (λs. shows ''problem when orienting DPs⏎'' o s);
check_allm (check_suptproj_pred π FF) ps
<+? (λs. shows ''problem when orienting DPs⏎'' o s)
} <+? (λs. shows ''could not apply the AC subterm processor⏎'' o s))
(ac_dpp_ops.delete_pairs_rules I dpp P_remove [])"
lemma (in ac_dpp_spec) ac_subterm_proc:
shows "sound_proc_impl (ac_subterm_proc I pi ps)"
proof
fix d d'
assume fin: "finite_rel_dpp (ac_dpp d')"
and ok: "ac_subterm_proc I pi ps d = return d'"
def F ≡ "map fst pi"
def π ≡ "the (status_of pi)"
let ?P = "set (P d)"
let ?Pw = "set (Pw d)"
let ?PP = "?P ∪ ?Pw"
let ?R = "set (R d)"
let ?Rw = "set (Rw d)"
let ?E = "set (E d)"
let ?RE = "?R ∪ ?Rw ∪ ?E"
let ?Sup = "suptproj_pred π (set F)"
let ?SupEq = "suptprojeq_pred π (set F)"
obtain Ps Pns where p: "partition (λ lr. lr ∈ set ps) (pairs d) = (Ps,Pns)" by force
note ok = ok[unfolded ac_subterm_proc_def Let_def p split, folded F_def π_def, simplified]
from ok have var: "⋀ l r. (l, r)∈ ?RE ⟹ is_Fun l"
and size: "size_preserving_trs (set (E d))"
and d': "d' = ac_dpp_ops.delete_pairs_rules I d ps []"
and π: "∀f∈ set F. status π f ≠ []"
and supt: "⋀ l r. (l,r) ∈ set Ps ⟹ ?Sup l r"
and supteq: "⋀ l r. (l,r) ∈ set Pns ⟹ ?SupEq l r"
by auto
{
fix l r
assume "(l,r) ∈ ?PP"
with p have "(l,r) ∈ set Ps ∪ set Pns" by auto
with s_ns_mul_ext[OF supt[of l r]] supteq[of l r] have "?SupEq l r" by auto
} note PP = this
{
fix l r
assume lr: "(l,r) ∈ ?RE" and "root l ∈ Some ` set F"
with ok have rt: "the (root l) ∈ set F" by (cases l, auto)
from ok have "(l,r) ∈ ?RE ⟹ the (root (fst (l,r))) ∈ set F ⟹ ?SupEq (fst (l,r)) (snd (l,r))"
by blast
with rt lr have "?SupEq l r" by auto
} note RE = this
have id: "?PP = set (pairs d)" "?RE = set (R d @ Rw d @ E d)" by auto
note fin = fin[unfolded d' delete_pairs_rules_sound, simplified]
show "finite_rel_dpp (ac_dpp d)" unfolding ac_dpp_sound
by (rule ac_subterm_proc[OF π fin PP RE supt size var], insert p, auto)
qed
definition
generalized_subterm_proc ::
"('dpp, 'f :: show, 'v :: show) dpp_ops ⇒ 'f status_impl ⇒
('f,'v)rules ⇒ 'dpp proc"
where
"generalized_subterm_proc I pi P_remove dpp = check_return (do {
let P = dpp_ops.pairs I dpp;
let R = dpp_ops.rules I dpp;
let F = map fst pi;
let FF = set F;
let pi_opt = status_of pi;
check (dpp_ops.Q I dpp = []) (shows ''currently generalized subterm criterion does not support strategies'');
check (dpp_ops.minimal I dpp) (shows ''minimality required'');
check (pi_opt ≠ None) (shows ''argument filter lists invalid positions'');
let π = the pi_opt;
let Premove = set P_remove;
let (ps, pns) = partition (λ lr. lr ∈ Premove) P;
check_allm (λ f. check (status π f ≠ [])
(shows ''status of symbol '' o shows f o shows '' in F must be non-empty'')) F;
check_allm (λ (l,r). check (is_Fun l) (shows ''variables as lhss not allowed'')) R;
check_allm (check_supteqproj_pred π FF) (filter (λ lr. the (root (fst lr)) ∈ FF) R)
<+? (λs. shows ''problem when orienting rules with root in F⏎'' o s);
check_allm (check_supteqproj_pred π FF) pns
<+? (λs. shows ''problem when orienting DPs⏎'' o s);
check_allm (check_suptproj_pred π FF) ps
<+? (λs. shows ''problem when orienting DPs⏎'' o s)
} <+? (λs. shows ''could not apply the subterm processor⏎'' o s))
(dpp_ops.delete_P_Pw I dpp P_remove P_remove)"
lemma (in dpp_spec) generalized_subterm_proc:
shows "sound_proc_impl (generalized_subterm_proc I pi ps)"
proof
fix d d'
assume fin: "finite_dpp (dpp d')"
and ok: "generalized_subterm_proc I pi ps d = return d'"
def F ≡ "map fst pi"
def π ≡ "the (status_of pi)"
let ?P = "set (P d)"
let ?Pw = "set (Pw d)"
let ?PP = "?P ∪ ?Pw"
let ?R = "set (R d)"
let ?Q = "set (Q d)"
let ?Rw = "set (Rw d)"
let ?RE = "?R ∪ ?Rw"
let ?M = "M d"
let ?Sup = "suptproj_pred π (set F)"
let ?SupEq = "suptprojeq_pred π (set F)"
obtain Ps Pns where p: "partition (λ lr. lr ∈ set ps) (pairs d) = (Ps,Pns)" by force
note ok = ok[unfolded generalized_subterm_proc_def Let_def p split, folded F_def π_def, simplified]
from ok have var: "⋀ l r. (l, r)∈ ?RE ⟹ is_Fun l"
and d': "d' = dpp_ops.delete_P_Pw I d ps ps"
and π: "∀f∈ set F. status π f ≠ []"
and supt: "⋀ l r. (l,r) ∈ set Ps ⟹ ?Sup l r"
and supteq: "⋀ l r. (l,r) ∈ set Pns ⟹ ?SupEq l r"
and Q: "?Q = {}" and M: "?M = True"
by auto
{
fix l r
assume "(l,r) ∈ ?PP"
with p have "(l,r) ∈ set Ps ∪ set Pns" by auto
with s_ns_mul_ext[OF supt[of l r]] supteq[of l r] have "?SupEq l r" by auto
} note PP = this
{
fix l r
assume lr: "(l,r) ∈ ?RE" and "root l ∈ Some ` set F"
with ok have rt: "the (root l) ∈ set F" by (cases l, auto)
from ok have "(l,r) ∈ ?RE ⟹ the (root (fst (l,r))) ∈ set F ⟹ ?SupEq (fst (l,r)) (snd (l,r))"
by simp
with rt lr have "?SupEq l r" by auto
} note RE = this
have id: "?PP = set (pairs d)" "?RE = set (R d @ Rw d)" by auto
note fin = fin[unfolded d' delete_P_Pw_sound M Q, simplified]
show "finite_dpp (dpp d)" unfolding dpp_sound Q M
by (rule generalized_subterm_proc[OF π fin PP RE supt var], insert p, auto)
qed
end