theory Non_Confluence_Impl
imports
Critical_Pairs_Impl
Non_Confluence
Usable_Rules_NJ_Impl
Usable_Rules_NJ_Unif_Impl
"../Orderings/Reduction_Pair_Implementations"
"../Termination_and_Complexity/Semantic_Labeling_Carrier"
"../Tree_Automata/Tree_Automata_Impl"
begin
hide_const (open) Quasi_Order.equiv_class
definition "check_modularity_ncr R R' = do {
check_subseteq R' R <+? (λ _. shows ''new TRS is not a subsystem of given TRS'');
let S = list_diff R R';
let F = funas_trs_list R';
let G = funas_trs_list S;
check (set F ∩ set G ⊆ {}) (shows ''signatures are not disjoint'');
check_varcond_subset R';
check_all (λ(l, r). is_Fun l) S
<+? (λ _. shows ''lhss must not be variables'')
}"
lemma check_modularity_ncr: fixes R :: "('f :: show, 'v :: show) rules"
assumes ok: "isOK (check_modularity_ncr R R')"
and nCR: "¬ CR (rstep (set R'))"
and inf: "infinite (UNIV :: 'f set)"
shows "¬ CR (rstep (set R))"
proof -
let ?S = "set R - set R'"
note ok = ok[unfolded check_modularity_ncr_def, simplified]
from ok have id: "set R = set R' ∪ ?S" and subset: "set R' ⊆ set R" by auto
from id have id: "rstep (set R) = rstep (set R' ∪ ?S)" by auto
show ?thesis unfolding id
by (rule modularity_of_non_confluence[OF nCR],
insert ok inf, auto intro: finite_funas_trs)
qed
abbreviation(input) join where "join ≡ Abstract_Rewriting.join"
fun
check_qmodel_rule_ass ::
"('f::show,'c::show)inter
⇒ ('c ⇒ 'c ⇒ bool)
⇒ ('v::show,'c)assign ⇒ ('f,'v)rule ⇒ shows check"
where
"check_qmodel_rule_ass I cge α (l, r) = do {
let cl = Non_Confluence.eval I α l;
let cr = Non_Confluence.eval I α r;
check (cge cl cr)
(''rule '' +#+ shows_rule (l, r) +@+ '' violates the model condition, [lhs] = ''
+#+ shows cl +@+ '', [rhs] = '' +#+ shows cr)
}"
definition
check_qmodel_rule ::
"('f::show,'c::show)inter
⇒ 'c list
⇒ ('c ⇒ 'c ⇒ bool)
⇒ ('f,'v::show)rule ⇒ shows check"
where
"check_qmodel_rule I C cge lr = check_allm (λα. check_qmodel_rule_ass I cge α lr)
(map fun_of (enum_vectors C (vars_rule_impl lr)))"
definition
check_qmodel ::
"('f::show,'c::show)inter
⇒ 'c list
⇒ ('c ⇒ 'c ⇒ bool)
⇒ ('f,'v::show)sl_check0"
where
"check_qmodel I C cge R = check_allm (check_qmodel_rule I C cge) R"
lemma check_qmodel:
fixes I :: "('f :: show,'c::show)inter"
assumes ok: "isOK (check_qmodel I C cge R)"
shows "qmodel I (set C) cge (set R)"
proof -
let ?L = undefined
let ?LC = undefined
{
fix l r
assume lr: "(l,r) ∈ set R"
{
fix α
have "check_sl_rule_ass True I ?L ?LC cge UNIV α (l,r) = check_qmodel_rule_ass I cge α (l,r)"
by (simp add: Let_def check_def)
} note id = this
from lr ok[unfolded check_qmodel_def] have "True = isOK(check_qmodel_rule I C cge (l,r))" by auto
also have "… = isOK (check_sl_rule I ?L ?LC C cge True UNIV (l,r))"
unfolding check_qmodel_rule_def check_sl_rule.simps id ..
finally have "isOK (check_sl_rule I ?L ?LC C cge True UNIV (l,r))" by simp
from check_sl_rule_sound[OF this] have "Semantic_Labeling.qmodel_rule I ?L ?LC (set C) cge l r" by simp
}
hence "Semantic_Labeling.qmodel I ?L ?LC (set C) cge (set R)" unfolding Semantic_Labeling.qmodel_def by auto
thus ?thesis by simp
qed
definition check_non_join_model ::
"('c ⇒ 'c::show ⇒ bool) ⇒
(('f × nat) list ⇒ ('f × nat) list ⇒ shows + ('f,'c,'l,'v)sl_ops) ⇒
('f :: show,'v :: show)rules ⇒ ('f,'v)rules ⇒
('f,'v)term ⇒
('f,'v)term ⇒
shows check"
where
"check_non_join_model cge gen Rs Rt s t ≡
do {
ops ← gen (funas_trs_list (Rs @ Rt)) [];
let I = sl_ops.sl_I ops;
let e = eval I (λ _. sl_ops.sl_c ops);
let es = e s;
let et = e t;
check (¬ cge et es) (shows ''the inequality must not hold: ['' +@+ shows t +@+ shows ''] = '' +@+ shows et +@+ shows '' >= ''
+@+ shows es +@+ shows '' = ['' +@+ shows s +@+ shows '']'');
check_qmodel I (sl_ops.sl_C ops) cge (reverse_rules Rs @ Rt)
} <+? (λ s. shows ''problem in disproving non-joinability via interpretations'' +@+ shows_nl +@+ s)"
lemma (in sl_finite_impl) check_non_join_model: assumes ok: "isOK(check_non_join_model cge sl_gen Rs Rt s t)"
and refl: "⋀ x. cge x x"
and trans: "⋀ x y z. cge x y ⟹ cge y z ⟹ cge x z"
shows "¬ (∃ u. (s,u) ∈ (rstep (set Rs))^* ∧ (t,u) ∈ (rstep (set Rt))^*)"
proof -
note ok = ok[unfolded check_non_join_model_def Let_def]
from ok obtain ops where gen: "sl_gen (funas_trs_list (Rs @ Rt)) [] = Inr ops" by auto
let ?c = "sl_c ops"
let ?I = "sl_I ops"
let ?C = "sl_C ops"
note ok = ok[unfolded gen, simplified]
from sl_gen_inter[OF gen]
interpret sl_interpr_root_same "set ?C" ?c ?I cge lge "sl_L ops" LC LD "sl_LS ops" "sl_L'' ops" "sl_LS'' ops" .
from ok have "isOK (check_qmodel ?I ?C cge (reverse_rules Rs @ Rt))" by auto
from check_qmodel[OF this]
have "qmodel ?I (set ?C) cge ((set Rs)^-1 ∪ set Rt)" by simp
note aoto = aoto_theorem_2[OF this c wf_I wm_cge refl]
let ?e = "eval ?I (λ _. ?c)"
from ok have "¬ cge (?e t) (?e s)" by simp
note aoto = aoto[OF trans this]
show ?thesis
by (rule aoto)
qed
definition check_non_join_redpair ::
"('f::{show,key}, 'v::show) redtriple ⇒ ('f,'v)rules ⇒ ('f,'v)rules ⇒
('f,'v)term ⇒
('f,'v)term ⇒
shows check" where
"check_non_join_redpair rp Rs Rt s t ≡
do {
redtriple.valid rp;
check_allm (redtriple.ns rp) (reverse_rules Rs @ Rt);
redtriple.s rp (s, t)
} <+? (λ s. shows ''problem in disproving non-joinability via discrimination pairs'' +@+ shows_nl +@+ s)"
lemma check_non_join_redpair: assumes grp: "generic_redtriple_impl grp"
and ok: "isOK(check_non_join_redpair (grp rp) Rs Rt s t)"
shows "¬ (∃ u. (s,u) ∈ (rstep (set Rs))^* ∧ (t,u) ∈ (rstep (set Rt))^*)"
proof -
let ?rp = "grp rp"
note ok = ok[unfolded check_non_join_redpair_def Let_def, simplified]
from ok have valid: "isOK(redtriple.valid ?rp)" by simp
from ok have ns: "isOK (check_allm (redtriple.ns ?rp) (reverse_rules Rs @ Rt))" by simp
from ok have s: "isOK (check_allm (redtriple.s ?rp) ([(s,t)]))" by simp
let ?cpx = "λ cm cc. isOK(redtriple.cpx ?rp cm cc)"
interpret generic_redtriple_impl grp by (rule grp)
from generate_redtriple[OF valid s ns, of Nil]
obtain S NS NST where "cpx_ce_af_redtriple_order S NS NST (redtriple.af ?rp) (redtriple.mono_af ?rp) ?cpx"
and NS: "(set Rs)^-1 ∪ set Rt ⊆ NS" and S: "(s,t) ∈ S" by auto
interpret cpx_ce_af_redtriple_order S NS NST "redtriple.af ?rp" "redtriple.mono_af ?rp" ?cpx by fact
show ?thesis
by (rule aoto_pre_theorem_12[OF discrimination_pair], insert NS S, auto)
qed
text ‹Now we have to link to concrete interpretations and reduction pairs›
type_synonym 'f lt = "('f,label_type)lab"
fun check_non_join_finite_model :: "(('f :: show)lt,'v :: show) sl_variant ⇒
('f lt,'v)rules ⇒ ('f lt,'v)rules ⇒
('f lt,'v)term ⇒
('f lt,'v)term ⇒ shows check" where
"check_non_join_finite_model (Rootlab x) Rs Rt s t = check_non_join_model op = (slm_gen_to_sl_gen (rl_slm x)) Rs Rt s t"
| "check_non_join_finite_model (Finitelab sli) Rs Rt s t =
check_non_join_model op = (slm_gen_to_sl_gen (λ_ _. return (sli_to_slm sli))) Rs Rt s t"
| "check_non_join_finite_model (QuasiFinitelab sli v) Rs Rt s t =
check_non_join_model qmodel_cge (λ F G. qsli_to_sl v F G sli) Rs Rt s t"
lemma check_non_join_finite_model: assumes ok: "isOK(check_non_join_finite_model I Rs Rt s t)"
shows "¬ (∃ u. (s,u) ∈ (rstep (set Rs))^* ∧ (t,u) ∈ (rstep (set Rt))^*)"
proof (cases I)
case (Rootlab I)
with ok show ?thesis
by (intro rl_fin_model.check_non_join_model, auto)
next
case (Finitelab I)
with ok show ?thesis
by (intro sl_fin_model.check_non_join_model, auto)
next
case (QuasiFinitelab I v)
with ok show ?thesis
by (intro arith_finite_qmodel.check_non_join_model, auto simp: qmodel_cge_def)
qed
text ‹combine all techniques for non-joinability›
datatype (dead 'f, dead 'v, 'q) non_join_info =
Diff_NFs
| Tcap_Non_Unif "('f, 'v) term ⇒ ('f, 'v) term ⇒ ('f, 'v) subst"
| Tree_Aut_Intersect_Empty "('q, 'f) tree_automaton" "'q ta_relation"
"('q, 'f) tree_automaton" "'q ta_relation"
| Finite_Model_Gt "('f, 'v) sl_variant"
| Reduction_Pair_Gt "'f redtriple_impl"
| Usable_Rules_Reach_NJ "('f, 'v, 'q) non_join_info"
| Usable_Rules_Reach_Unif_NJ "('f, 'v) rules + ('f, 'v) rules" "('f, 'v, 'q) non_join_info"
| Argument_Filter_NJ "'f afs_list" "('f, 'v, 'q) non_join_info"
| Grounding "('f, 'v) substL" "('f, 'v, 'q) non_join_info"
| Subterm_NJ pos "('f, 'v, 'q) non_join_info"
primrec check_non_join :: "(('f :: {key,show,compare_order})lt,string)rules ⇒ ('f lt,string)rules ⇒ ('f lt,string)term ⇒ ('f lt,string)term ⇒
('f lt,string,'q :: {show,compare_order})non_join_info ⇒ shows check" where
"check_non_join Rs Rt s t Diff_NFs = do {
check (s ≠ t) (shows ''the terms '' +@+ shows s +@+ shows '' and '' +@+ shows t +@+ shows '' are identical'');
let chknf = (λ s R. check (is_NF_trs R s) (shows ''the term '' +@+ shows_term s +@+ shows '' is not in normal form''));
chknf s Rs;
chknf t Rt
}"
| "check_non_join Rs Rt s t (Grounding σ prf) = do {
let σ' = mk_subst Var σ;
check_non_join Rs Rt (s ⋅ σ') (t ⋅ σ') prf
}"
| "check_non_join Rs Rt s t (Subterm_NJ p prf) = do {
check (p ∈ pos_gctxt (tcapI Rs s)) (shows ''position '' +@+ shows p +@+ shows '' not in capped term of '' +@+ shows s);
check (p ∈ pos_gctxt (tcapI Rt t)) (shows ''position '' +@+ shows p +@+ shows '' not in capped term of '' +@+ shows t);
check_non_join Rs Rt (s |_ p) (t |_ p) prf
}"
| "check_non_join Rs Rt s t (Tcap_Non_Unif grd_subst) = do {
let σ = grd_subst s t;
let cs = tcapI Rs (s ⋅ σ);
let ct = tcapI Rt (t ⋅ σ);
check (Ground_Context_Impl.merge cs ct = None) (shows ''could not infer that '' +@+ shows s +@+
shows '' and '' +@+ shows t +@+ shows '' are not joinable'')
}"
| "check_non_join Rs Rt s t (Tree_Aut_Intersect_Empty ta1 rel1 ta2 rel2) = do {
non_join_with_ta ta1 rel1 Rs s ta2 rel2 Rt t
<+? (λ e. (shows ''could not infer that '' +@+ shows s +@+
shows '' and '' +@+ shows t +@+ shows '' are not joinable'' +@+ shows_nl +@+ e))
}"
| "check_non_join Rs Rt s t (Finite_Model_Gt I) = do {
check_non_join_finite_model I Rs Rt s t
<+? (λ e. (shows ''could not infer that '' +@+ shows s +@+
shows '' and '' +@+ shows t +@+ shows '' are not joinable'' +@+ shows_nl +@+ e))
}"
| "check_non_join Rs Rt s t (Reduction_Pair_Gt rp) = do {
check_non_join_redpair (get_redtriple rp) Rs Rt s t
<+? (λ e. (shows ''could not infer that '' +@+ shows s +@+
shows '' and '' +@+ shows t +@+ shows '' are not joinable'' +@+ shows_nl +@+ e))
}"
| "check_non_join Rs Rt s t (Usable_Rules_Reach_NJ prf) =
check_non_join (usable_rules_reach_impl Rs s) (usable_rules_reach_impl Rt t) s t prf"
| "check_non_join Rs Rt s t (Usable_Rules_Reach_Unif_NJ U_sum prf) = (
case U_sum of
Inl U ⇒ do {
check_usable_rules_unif Rs U s;
check_non_join U Rt s t prf
}
| Inr U ⇒ do {
check_usable_rules_unif Rt U t;
check_non_join Rs U s t prf
}
)
"
| "check_non_join Rs Rt s t (Argument_Filter_NJ pi prf) = (case afs_of pi of
None ⇒ error (shows ''invalid argument filter'')
| Some π ⇒ let af = af_term π; afs = af_rules π
in check_non_join (afs Rs) (afs Rt) (af s) (af t) prf
)"
lemma check_non_join:
"isOK(check_non_join Rs Rt s t prf) ⟹ ¬ (∃ u. (s,u) ∈ (rstep (set Rs))^* ∧ (t,u) ∈ (rstep (set Rt))^*)"
proof (induct "prf" arbitrary: Rs Rt s t)
case Diff_NFs
note ok = Diff_NFs[simplified]
show ?case
proof
assume "∃ u. (s,u) ∈ (rstep (set Rs))^* ∧ (t,u) ∈ (rstep (set Rt))^*"
then obtain u where su: "(s,u) ∈ (rstep (set Rs))^*" and tu: "(t,u) ∈ (rstep (set Rt))^*" by auto
from NF_not_suc[OF su] NF_not_suc[OF tu] ok show False by auto
qed
next
case (Subterm_NJ p prof) note IH = this
hence p: "p ∈ pos_gctxt (tcap (set Rs) s)" "p ∈ pos_gctxt (tcap (set Rt) t)"
and ok: "isOK (check_non_join Rs Rt (s |_ p) (t |_p) prof)" by auto
from subterm_tcap_nj[OF p IH(1)[OF ok]]
show ?case .
next
case (Grounding sigma prof)
show ?case
proof
assume "∃ u. (s,u) ∈ (rstep (set Rs))^* ∧ (t,u) ∈ (rstep (set Rt))^*"
then obtain u where su: "(s,u) ∈ (rstep (set Rs))^*" and tu: "(t,u) ∈ (rstep (set Rt))^*" by auto
def σ ≡ "mk_subst Var sigma"
from rsteps_closed_subst[OF su] have s: "(s ⋅ σ, u ⋅ σ) ∈ (rstep (set Rs))^*" .
from rsteps_closed_subst[OF tu] have t: "(t ⋅ σ, u ⋅ σ) ∈ (rstep (set Rt))^*" .
from Grounding(2) have ok: "isOK (check_non_join Rs Rt (s ⋅ σ) (t ⋅ σ) prof)" unfolding σ_def
by (simp add: Let_def)
from Grounding(1)[OF this] s t show False by auto
qed
next
case (Tcap_Non_Unif grd_subst)
obtain σ where sigma: "σ = grd_subst s t" by auto
show ?case
proof
assume "∃ u. (s,u) ∈ (rstep (set Rs))^* ∧ (t,u) ∈ (rstep (set Rt))^*"
then obtain u where su: "(s,u) ∈ (rstep (set Rs))^*" and tu: "(t,u) ∈ (rstep (set Rt))^*" by auto
from rsteps_closed_subst[OF su] have s: "(s ⋅ σ, u ⋅ σ) ∈ (rstep (set Rs))^*" .
from rsteps_closed_subst[OF tu] have t: "(t ⋅ σ, u ⋅ σ) ∈ (rstep (set Rt))^*" .
from tcap_sound[of "s ⋅ σ" Var "u ⋅ σ"] s have u1: "u ⋅ σ ∈ equiv_class (tcap (set Rs) (s ⋅ σ))" by simp
from tcap_sound[of "t ⋅ σ" Var "u ⋅ σ"] t have u2: "u ⋅ σ ∈ equiv_class (tcap (set Rt) (t ⋅ σ))" by simp
from u1 u2 Tcap_Non_Unif show False using sigma by (auto simp: Let_def)
qed
next
case (Tree_Aut_Intersect_Empty ta1 rel1 ta2 rel2)
hence "isOK (non_join_with_ta ta1 rel1 Rs s ta2 rel2 Rt t)" by auto
from non_join_with_ta[OF this] show ?case .
next
case (Finite_Model_Gt I)
hence "isOK (check_non_join_finite_model I Rs Rt s t)" by auto
from check_non_join_finite_model[OF this] show ?case .
next
case (Reduction_Pair_Gt rp)
hence "isOK (check_non_join_redpair (get_redtriple rp) Rs Rt s t)" by auto
from check_non_join_redpair[OF get_redtriple this] show ?case .
next
case (Usable_Rules_Reach_NJ p)
note * = this
from usable_rules_reach_nj[OF *(1)[OF *(2)[unfolded check_non_join.simps], unfolded usable_rules_reach_impl]]
show ?case .
next
case (Usable_Rules_Reach_Unif_NJ U_sum p)
note * = this
show ?case
proof (cases U_sum)
case (Inl U)
show ?thesis
by (rule check_usable_rules_unif_left[OF _ *(1)], insert *(2) Inl, auto)
next
case (Inr U)
show ?thesis
by (rule check_usable_rules_unif_right[OF _ *(1)], insert *(2) Inr, auto)
qed
next
case (Argument_Filter_NJ pi p)
note * = this
note ok = *(2)[simplified]
from ok obtain π where pi: "afs_of pi = Some π" by (cases "afs_of pi", auto)
from ok[unfolded pi]
have rec: "isOK (check_non_join (af_rules π Rs) (af_rules π Rt) (af_term π s) (af_term π t) p)"
by (auto simp: Let_def)
from argument_filter_nj[OF *(1)[OF rec, unfolded af_rules]]
show ?case .
qed
text ‹and combine with reachability checker to disprove CR›
definition check_non_cr :: "(('f :: {key,show,compare_order})lt,string)rules ⇒ ('f lt,string)term ⇒ ('f lt,string)rseq ⇒ ('f lt,string)rseq ⇒
('f lt,string,'q :: {show,compare_order})non_join_info ⇒ shows check"
where "check_non_cr R s seq1 seq2 reason ≡ do {
let chk = check_rsteps_last R s;
chk seq1;
chk seq2;
check_non_join R R (rseq_last s seq1) (rseq_last s seq2) reason
}"
lemma check_non_cr: assumes ok: "isOK(check_non_cr R s seq1 seq2 prf)"
shows "¬ CR (rstep (set R))"
proof
let ?R = "rstep (set R)"
assume CR: "CR ?R"
note ok = ok[unfolded check_non_cr_def Let_def, simplified]
let ?last = "rseq_last s"
let ?l1 = "?last seq1"
let ?l2 = "?last seq2"
from check_rsteps_last_sound ok have s1: "(s,?l1) ∈ (rstep (set R))^*" by auto
from check_rsteps_last_sound ok have s2: "(s,?l2) ∈ (rstep (set R))^*" by auto
from ok have "isOK (check_non_join R R ?l1 ?l2 prf)" by auto
from CR s1 s2 check_non_join[OF this] show False by auto
qed
end