theory Usable_Rules_Impl
imports
"Check-NT.Usable_Rules"
QTRS.QDP_Framework_Impl
"Check-NT.Tcap_Impl"
"Check-NT.Q_Restricted_Rewriting_Impl"
"Check-NT.Term_Order_Impl"
begin
fun matchCapRMBelow :: "('f × nat ⇒ ('f,'v)rules) ⇒ ('f,'v)term ⇒ ('f,'v)term ⇒ bool"
where "matchCapRMBelow rm l (Fun f ts) = Ground_Context.match (GCFun f (map (tcapRM2 rm) ts)) l"
lemma matchCapRMBelow:
assumes noLeftVars: "⋀ lr. lr ∈ set R ⟹ is_Fun (fst lr)"
and rm: "⋀f n. set (rm (f, n)) = {(l, r). (l, r) ∈ set R ∧ root l = Some (f, n)}"
shows "matchCapRMBelow rm l (Fun f ts) = match_tcap_below l (set R) (Fun f ts)"
proof -
from tcapRM2_sound[OF noLeftVars rm] have id: "tcapRM2 rm = tcap (set R)"
by (intro ext, auto)
show ?thesis unfolding matchCapRMBelow.simps match_tcap_below.simps id ..
qed
fun
check_ur_closed_term_rm_af :: "(('f × nat) ⇒ ('f, 'v) rules) ⇒ ('f::show, 'v::show) rules ⇒ 'f af ⇒ ('f, 'v) term ⇒ shows check"
where
"check_ur_closed_term_rm_af _ _ _ (Var x) = succeed" |
"check_ur_closed_term_rm_af rm ur π (Fun f ts) = do {
let n = length ts;
let pi = π (f, n);
check_allm_index (λt i. if i ∈ pi then check_ur_closed_term_rm_af rm ur π t else succeed) ts;
check_allm (λlr.
check (lr ∈ set ur ∨ ¬ matchCapRMBelow rm (fst lr) (Fun f ts))
(''due to the subterm '' +#+ shows(Fun f ts) +@+ '' of some usable rhs, rule '' +#+ shows_rule lr +@+ shows_string '' should be usable.'')
) (rm (f,n))
}"
lemma check_ur_closed_term_rm_af_sound:
assumes noLeftVars: "⋀lr. lr ∈ set R ⟹ is_Fun (fst lr)"
and rm: "⋀f n. set (rm (f,n)) = {(l, r). (l, r) ∈ set R ∧ root l = Some (f, n)}"
and check: "isOK(check_ur_closed_term_rm_af rm ur π t)"
and tus: "funas_term t ⊆ us"
shows "ur_closed_term_af (set R) (set ur) us π t"
using check tus proof (induct t)
case (Fun f ts)
from Fun(3) have fus: "(f, length ts) ∈ us" by auto
from Fun(3) have "∀ i < length ts. funas_term (ts ! i) ⊆ us" by force
with Fun(1) Fun(2)
have rls: "∀ (l,r) ∈ set (rm (f,length ts)). (l,r) ∈ set ur ∨ ¬ matchCapRMBelow rm l (Fun f ts)"
and ind: " (∀i<length ts. i ∈ π (f, (length ts)) ⟶ ur_closed_term_af (set R) (set ur) us π (ts ! i))" by (auto simp: Let_def)
have "∀ (l,r) ∈ set R. (l,r) ∈ set ur ∨ ¬ matchCapRMBelow rm l (Fun f ts)" (is "∀(l, r) ∈ set R. ?P l r")
proof
fix l r
assume lr: "(l, r) ∈ set R"
show "?P l r"
proof (cases "(l, r) ∈ set (rm (f, length ts))")
case True
with rls show ?thesis by auto
next
case False
from noLeftVars[OF lr] obtain g ss where l: "l = Fun g ss" by (cases l, auto)
with rm False lr have "¬ (f = g ∧ length ss = length ts)" by auto
with l rm have "¬ matchCapRMBelow rm l (Fun f ts)" by (auto simp: Ground_Context.match_def)
with rls show ?thesis by auto
qed
qed
with ind fus show ?case
using matchCapRMBelow[OF noLeftVars rm] by auto
qed simp
definition
check_ur_P_closed_rm_af ::
"('f × nat ⇒ ('f,'v)rules) ⇒ ('f :: show, 'v :: show) rules ⇒ 'f af ⇒ ('f, 'v) rules ⇒ shows check"
where
"check_ur_P_closed_rm_af rm ur π P ≡ do {
check_allm (λlr. check_ur_closed_term_rm_af rm ur π (snd lr)) ur
<+? (λs. ''error when checking closure properties of rhs of usable rules'' +#+ shows_nl +@+ s);
check_allm (λst. check_ur_closed_term_rm_af rm ur π (snd st)) P
<+? (λs. ''error when checking closure properties of rhs of DPs'' +#+ shows_nl +@+ s)
}"
lemma check_ur_P_closed_rm_af_sound:
assumes noLeftVars: "⋀lr. lr ∈ set R ⟹ is_Fun (fst lr)"
and rm: "⋀f n. set (rm (f, n)) = {(l, r). (l, r) ∈ set R ∧ root l = Some (f, n)}"
and check: "isOK(check_ur_P_closed_rm_af rm ur π P)"
and us: "(⋃((funas_term o snd) ` (set ur ∪ set P))) ⊆ us"
shows "ur_closed_af (set R) (set ur) us π ∧ ur_P_closed_af (set R) (set ur) us π (set P)"
proof -
note closure = check_ur_closed_term_rm_af_sound[OF noLeftVars rm]
{
fix l r
assume lr: "(l, r) ∈ set ur"
with us have rus: "funas_term r ⊆ us" by force
from closure[OF _ _ rus] check lr
have "ur_closed_term_af (set R) (set ur) us π r" unfolding check_ur_P_closed_rm_af_def by auto
} note part1 = this
{
fix l r
assume lr: "(l,r) ∈ set P"
with us have rus: "funas_term r ⊆ us" by force
from closure[OF _ _ rus] check lr
have "ur_closed_term_af (set R) (set ur) us π r" unfolding check_ur_P_closed_rm_af_def by auto
} note part2 = this
from part1 part2 show ?thesis by auto
qed
definition
mono_ur_redpair_proc ::
"('dpp, 'f, 'v) dpp_ops ⇒ ('f::show, 'v::show) redtriple ⇒
('f,'v)rules ⇒ ('f,'v)rules ⇒ ('f,'v)rules ⇒ 'dpp proc"
where
"mono_ur_redpair_proc I rp Premove Rremove ur dpp = check_return (do {
check (dpp_ops.minimal I dpp) (shows ''minimality required'');
check (dpp_ops.nfs I dpp ⟶ ¬ dpp_ops.Q_empty I dpp ⟶ dpp_ops.wwf_rules I dpp) (shows ''well formedness required'');
let P = dpp_ops.pairs I dpp;
let us = ⋃ set (map (funas_term o snd) (P @ ur));
let filt = (λ lr. (∀ f ∈ funas_term (fst lr). f ∈ us));
let (pms, pns) = dpp_ops.split_pairs I dpp Premove;
let (ps, pnwf) = partition filt pms;
let (urms, urns) = partition (λ u. u ∈ set Rremove) ur;
let (urs, urnwf) = partition filt urms;
let rm = dpp_ops.rules_map I dpp;
redtriple.valid rp;
redtriple.mono rp (ps @ urs @ urns @ urnwf @ pns @ pnwf);
check_ur_P_closed_rm_af rm ur full_af P;
check_allm (λ (l,r). check (is_Fun l) (shows ''variables as lhss not allowed'')) (dpp_ops.rules I dpp);
check_allm (redtriple.ns rp) (urns @ urnwf)
<+? (λs. ''problem when orienting usable rules'' +#+ shows_nl +@+ s);
check_allm (redtriple.s rp) urs
<+? (λs. ''problem when orienting usable rules'' +#+ shows_nl +@+ s);
check_allm (redtriple.ns rp) (pns @ pnwf)
<+? (λs. ''problem when orienting DPs'' +#+ shows_nl +@+ s);
check_allm (redtriple.s rp) ps
<+? (λs. ''problem when orienting DPs'' +#+ shows_nl +@+ s)
} <+? (λs. ''could not apply the monotonic reduction pair processor with the following'' +#+ shows_nl +@+
(redtriple.desc rp) +@+ shows_nl +@+ s))
(dpp_spec.delete_pairs_rules I dpp Premove Rremove)"
context dpp_spec
begin
lemma mono_ur_redpair_proc:
assumes grp: "generic_redtriple_impl grp"
shows "sound_proc_impl (mono_ur_redpair_proc I (grp rp) ps rs ur)"
proof
fix d d'
assume fin: "finite_dpp (dpp d')"
and ok: "mono_ur_redpair_proc I (grp rp) ps rs ur d = return d'"
let ?rp = "grp rp"
let ?S = "set ps"
let ?P = "set (P d)"
let ?Pw = "set (Pw d)"
let ?S' = "(?P ∪ ?Pw) ∩ ?S"
let ?Pb = "set (dpp_ops.pairs I d)"
let ?PP = "?P ∪ ?Pw"
let ?Q = "set (Q d)"
let ?R = "set (R d)"
let ?Rw = "set (Rw d)"
let ?Sr = "set rs"
let ?Rb = "set (dpp_ops.rules I d)"
let ?RR = "set (dpp_ops.R I d @ dpp_ops.Rw I d)"
let ?RR' = "set (dpp_ops.R I d) ∪ set (dpp_ops.Rw I d)"
have RR': "?RR' = ?RR" by auto
let ?nfs = "NFS d"
let ?m = "M d"
have RR_conv: "?RR = ?Rb" unfolding dpp_spec_sound by auto
have PP_conv: "?PP = ?Pb" unfolding dpp_spec_sound by auto
interpret generic_redtriple_impl grp by (rule grp)
obtain us where us: "us = ⋃ ( set (map (funas_term o snd) (dpp_ops.pairs I d @ ur)))" by auto
let ?filt = "λ lr. (∀ f ∈ funas_term (fst lr). f ∈ us)"
let ?WF = "{lr. ?filt lr}"
obtain Pms Pns where p1: "dpp_ops.split_pairs I d ps = (Pms,Pns)" by force
obtain Ps Pnwf where p2: "partition ?filt Pms = (Ps,Pnwf)" by force
obtain Rms Rns where r1: "partition (λ r. r ∈ set rs) ur = (Rms,Rns)" by force
obtain Rs Rnwf where r2: "partition ?filt Rms = (Rs,Rnwf)" by force
from r1 r2 have ur: "set ur = set Rs ∪ set Rnwf ∪ set Rns" and Rs: "set Rs = (set ur ∩ set rs) ∩ ?WF" by auto
from split_pairs_sound[OF p1] have Pms: "set Pms = (?P ∪ ?Pw) ∩ ?S" and Pns: "set Pns = (?P ∪ ?Pw) - ?S" by auto
from p2 have Ps: "set Ps = ((?P ∪ ?Pw) ∩ ?S) ∩ ?WF" and Pnwf: "set Pnwf = ((?P ∪ ?Pw) ∩ ?S) - ?WF" unfolding Pms[symmetric] by auto
note P = Ps Pnwf Pns
note ok = ok[unfolded mono_ur_redpair_proc_def Let_def p1 r1 split p2[unfolded us] r2[unfolded us], simplified]
let ?π = "full_af"
let ?all = "(Ps @ Rs) @ (Rns @ Rnwf @ Pns @ Pnwf) @ []"
from ok have valid: "isOK(redtriple.valid ?rp)"
and mono: "isOK(redtriple.mono ?rp ?all)"
and compat: "isOK(check_ur_P_closed_rm_af (dpp_ops.rules_map I d) ur ?π (dpp_ops.pairs I d))"
and NS: "isOK (check_allm (redtriple.ns ?rp) (Rns @ Rnwf @ Pns @ Pnwf))"
and S: "isOK(check_allm (redtriple.s ?rp) (Ps @ Rs))"
and d': "d' = dpp_spec.delete_pairs_rules I d ps rs"
and vars: "⋀ l r. (l,r) ∈ ?R ∪ ?Rw ⟹ is_Fun l"
and wwf: "?nfs ⟹ ?Q ≠ {} ⟹ wwf_qtrs ?Q (set (R d) ∪ set (Rw d))"
and m: ?m by auto
let ?us = "(⋃ ( (funas_term o snd) ` (set ur ∪ ?Pb)))"
have ur_cl: "ur_closed_af ?RR' (set ur) ?us ?π ∧
ur_P_closed_af ?RR' (set ur) ?us ?π ?PP " (is "?ur1 ∧ ?ur2")
unfolding RR' RR_conv PP_conv
by (rule check_ur_P_closed_rm_af_sound[OF _ _ compat subset_refl], insert vars,
unfold dpp_spec_sound, force+)
hence ?ur1 and ?ur2 by auto
from generate_redtriple[OF valid S NS, of Nil] mono
obtain S NS NST where "mono_ce_af_redtriple_order S NS NST (redtriple.af ?rp)" and S: "set Ps ∪ set Rs ⊆ S" and NS: "set Rns ∪ set Rnwf ∪ set Pns ∪ set Pnwf ⊆ NS" and mono: "ctxt.closed S"
by auto
then interpret old: mono_ce_af_redtriple_order S NS NST "redtriple.af ?rp" by simp
interpret mono_ce_af_redtriple S NS NST full_af
by (unfold_locales, rule full_af)
from S NS have ur: "set ur ⊆ NS ∪ S" unfolding ur by auto
have P: "?P ∪ ?Pw = set Ps ∪ set Pns ∪ set Pnwf" unfolding P by blast
from S NS have p: "?P ∪ ?Pw ⊆ NS ∪ S" unfolding P by auto
let ?NWF = "{lr | lr. ¬ funas_term (fst lr) ⊆ ?us}"
have swap: "set ur ∪ ?Pb = ?Pb ∪ set ur" by auto
have "?S' - ?NWF ⊆ set Ps" unfolding Ps us pairs_sound[symmetric] swap by auto
also have "... ⊆ S" using S by auto
finally have Ps: "?S' - ?NWF ⊆ S" .
have "(?Sr ∩ set ur) - ?NWF = (set ur ∩ ?Sr) - ?NWF" by auto
also have "... ⊆ set Rs" unfolding Rs us swap by auto
also have "... ⊆ S" using S by auto
finally have Rs: "(?Sr ∩ set ur) - ?NWF ⊆ S" .
note proc = mono_redpair_ur_sound[OF _ mono ur p Ps Rs ‹?ur1› ‹?ur2› m wwf]
show "finite_dpp (dpp d)"
unfolding finite_dpp_def
proof(rule, elim exE)
fix s t σ
assume "min_ichain (dpp_ops.dpp I d) s t σ"
from proc[OF _ _ _ this[unfolded dpp_spec_sound]]
obtain i where chain: "min_ichain (?nfs,?m,?P - ?S',?Pw - ?S',?Q,?R - ?Sr,?Rw - ?Sr) (shift s i) (shift t i) (shift σ i)"
by auto
have "min_ichain (?nfs,?m,?P - ?S,?Pw - ?S,?Q,?R - ?Sr,?Rw - ?Sr) (shift s i) (shift t i) (shift σ i)"
by (rule min_ichain_mono[OF chain], auto)
with fin[unfolded d' delete_simps finite_dpp_def]
show False by blast
qed
qed
end
end