section ‹Infeasibility of Conditional Critical Pairs›
theory Infeasibility
imports
"../Nonreachability/Nonreachability"
Conditional_Critical_Pairs
Conditional_Rewriting_Impl
begin
datatype ('f, 'v) infeasibility_proof =
Infeasible_Compound_Conditions 'f "('f, 'v) nonreachability_proof"
| Infeasible_Equation "('f, 'v) term" "('f, 'v) term" "('f, 'v) nonreachability_proof"
| Infeasible_Subset "('f, 'v) rules" "('f, 'v) infeasibility_proof"
| Infeasible_Rhss_Equal "('f, 'v) term" "('f, 'v) term" "('f, 'v) term" "('f, 'v) nonjoinability_proof"
abbreviation "err_not_cond e ≡
shows ''equation '' ∘ shows_eq e ∘ shows '' is not in list of conditions'' ∘ shows_nl"
definition "trancl_of_list xs =
concat (map (λx. map (λy. (x, y)) (trancl_list_impl xs [x])) (map fst xs))"
lemma set_trancl_of_list [simp]:
"set (trancl_of_list R) = (set R)⇧+"
proof (intro equalityI subrelI)
fix x y assume "(x, y) ∈ (set R)⇧+"
then show "(x, y) ∈ set (trancl_of_list R)"
by (induct) (auto dest: trancl_into_trancl simp: trancl_list_impl trancl_of_list_def, force)
qed (auto simp: trancl_list_impl trancl_of_list_def)
lemma conds_n_sat_trancl_of_list:
assumes "conds_n_sat R n cs σ"
shows "conds_n_sat R n (trancl_of_list cs) σ"
using assms by (fastforce simp: conds_n_sat_iff elim: trancl.induct)
fun check_infeasible'
where
"check_infeasible' R cs (Infeasible_Compound_Conditions f p) =
check_nonreachable (map fst R) (Fun f (map fst cs)) (Fun f (map snd cs)) p"
| "check_infeasible' R cs (Infeasible_Equation s t p) = do {
check ((s, t) ∈ set cs) (err_not_cond (s, t));
check_nonreachable (map fst R) s t p
}"
| "check_infeasible' R cs (Infeasible_Subset cs' p) = do {
check_subseteq cs' cs <+? err_not_cond;
check_infeasible' R cs' p
}"
| "check_infeasible' R cs (Infeasible_Rhss_Equal s t u p) = do {
check ((s, u) ∈ set cs) (err_not_cond (s, u));
check ((t, u) ∈ set cs) (err_not_cond (t, u));
check_nonjoinable (map fst R) s t p
}"
definition
check_infeasible ::
"(('f::{key, show}, 'v::{key, show}) rules × ('f, 'v) infeasibility_proof) list ⇒
('f, 'v) crules ⇒ ('f, 'v) rules ⇒ ('f, 'v) rules ⇒ shows check"
where
"check_infeasible css R cs⇩1 cs⇩2 = check_exm (λ(cs, p). do {
let cs' = cs⇩1 @ cs⇩2;
check (match_rules cs cs' ≠ None ∧ match_rules cs' cs ≠ None) id;
check_infeasible' R (trancl_of_list cs) p
}) css (shows_sep id shows_nl)"
lemma perm_term_of_crule_eq_conv:
"π ∙ term_of_crule ρ⇩1 = term_of_crule ρ⇩2 ⟷ π ∙ ρ⇩1 = ρ⇩2"
by (cases ρ⇩1 rule: crule_cases; cases ρ⇩2 rule: crule_cases; auto simp: eqvt rules_enc_aux)
lemma match_crule_imp_variants:
fixes ρ⇩1 ρ⇩2 :: "('f, 'v :: infinite) crule"
assumes "match_crule ρ⇩2 ρ⇩1 = Some σ⇩1" and "match_crule ρ⇩1 ρ⇩2 = Some σ⇩2"
shows "∃π. π ∙ ρ⇩1 = ρ⇩2"
proof -
have "term_of_crule ρ⇩2 ⋅ σ⇩2 = term_of_crule ρ⇩1"
and "term_of_crule ρ⇩1 ⋅ σ⇩1 = term_of_crule ρ⇩2"
using assms by (auto simp: match_crule_alt_def dest: match_sound)
then obtain π where "π ∙ ρ⇩2 = ρ⇩1"
using term_variants_iff [of "term_of_crule ρ⇩2" "term_of_crule ρ⇩1"]
unfolding perm_term_of_crule_eq_conv by auto
then have "-π ∙ ρ⇩1 = ρ⇩2" by auto
then show ?thesis ..
qed
lemma check_infeasible':
assumes "isOK (check_infeasible' R cs p)"
shows "¬ (∃σ n. conds_n_sat (set R) n cs σ)"
using assms
proof (induct p arbitrary: cs)
case ok: (Infeasible_Compound_Conditions f p)
let ?s = "Fun f (map fst cs)"
let ?t = "Fun f (map snd cs)"
have "¬ (∃σ. (?s ⋅ σ, ?t ⋅ σ) ∈ (rstep (Ru (set R)))⇧*)"
using ok by (auto simp: Ru_def dest: check_nonreachable)
moreover
{ fix σ and n assume "conds_n_sat (set R) n cs σ"
then have "∀(s, t) ∈ set cs. (s ⋅ σ, t ⋅ σ) ∈ (rstep (Ru (set R)))⇧*"
using rtrancl_mono [OF cstep_imp_Ru_step, of "set R"]
by (auto simp: conds_n_sat_iff split: prod.splits dest!: csteps_n_imp_csteps)
then have "(?s ⋅ σ, ?t ⋅ σ) ∈ (rstep (Ru (set R)))⇧*"
by (unfold subst_apply_term.simps, intro args_steps_imp_steps)
(auto intro: args_steps_imp_steps) }
ultimately show ?case by auto
next
case (Infeasible_Equation s t p)
then have "(s, t) ∈ set cs" and "¬ (∃σ. (s ⋅ σ, t ⋅ σ) ∈ (rstep (Ru (set R)))⇧*)"
by (auto simp: Ru_def dest: check_nonreachable)
then show ?case
using csteps_n_imp_csteps [of _ _ "set R"]
and cstep_imp_Ru_step [THEN rtrancl_mono, of "set R"] by (auto simp: conds_n_sat_iff) blast
next
case (Infeasible_Subset cs' p)
then show ?case by (auto simp: conds_n_sat_iff) blast
next
case (Infeasible_Rhss_Equal s t u p)
then have "(s, u) ∈ set cs" and "(t, u) ∈ set cs"
and "¬ (∃σ. (s ⋅ σ, t ⋅ σ) ∈ (rstep (Ru (set R)))⇧↓)" by (auto simp: Ru_def dest: check_nonjoinable)
then show ?case
using csteps_n_imp_csteps [of _ _ "set R"] and cstep_imp_Ru_step [THEN rtrancl_mono, of "set R"]
by (blast dest: conds_n_satD)
qed
lemma check_infeasible:
fixes R :: "('f::{key, show}, 'v::{key, show, infinite}) crules"
assumes "isOK (check_infeasible css R cs⇩1 cs⇩2)"
shows "¬ (∃σ n. conds_n_sat (set R) n (cs⇩1 @ cs⇩2) σ)"
proof -
let ?cs' = "cs⇩1 @ cs⇩2"
obtain π :: "'v perm" and cs and p where "(cs, p) ∈ set css"
and cs: "cs = π ∙ ?cs'" and ok: "isOK (check_infeasible' R (trancl_of_list cs) p)"
using assms and match_rules_imp_variants [of _ ?cs']
by (fastforce simp: check_infeasible_def Ru_def)
then have "¬ (∃σ n. conds_n_sat (set R) n cs σ)"
using conds_n_sat_trancl_of_list [of "set R" _ cs] by (blast dest: check_infeasible')
then show ?thesis by (metis cs conds_n_sat_perm_shift rules_pt.permute_minus_cancel(2))
qed
lemma infeasible_rule:
assumes "¬ (∃σ. conds_sat R (conds ρ) σ)"
shows "(cstep R) = (cstep (R - {ρ}))" (is "_ = (cstep ?R)")
proof -
have "(cstep_n R n) = (cstep_n ?R n)" for n
proof (induct n)
case (Suc n)
show ?case
proof
show "(cstep_n R (Suc n)) ⊆ (cstep_n ?R (Suc n))"
proof
fix s t
assume "(s, t) ∈ cstep_n R (Suc n)"
then obtain C l r σ cs
where rule: "((l, r), cs) ∈ R"
and *: "∀(s⇩i, t⇩i) ∈ set cs. (s⇩i ⋅ σ, t⇩i ⋅ σ) ∈ (cstep_n R n)⇧*"
and s: "s = C⟨l ⋅ σ⟩"
and t: "t = C⟨r ⋅ σ⟩"
by (fast elim: cstep_nE)
then consider (ρ) "((l, r), cs) = ρ" | (not_ρ) "((l, r), cs) ∈ ?R" by fast
then show "(s, t) ∈ cstep_n ?R (Suc n)"
proof (cases)
case (ρ)
then have "conds_n_sat R n (conds ρ) σ" unfolding conds_n_sat_iff using * by fastforce
then have "conds_sat R (conds ρ) σ" using * conds_sat_conds_n_sat by blast
then show ?thesis using assms by auto
next
case (not_ρ)
then show ?thesis
using * by (intro cstep_n_SucI [of l r cs _ σ _ _ C]) (auto simp: Suc s t)
qed
qed
qed (auto intro: cstep_n_subset [THEN subsetD])
qed (simp)
then show ?thesis by (auto simp: cstep_iff)
qed
lemma infeasible_rules:
assumes "finite S"
and "∀ρ ∈ S. ¬ (∃σ. conds_sat R (conds ρ) σ)"
shows "(cstep R) = (cstep (R - S))" (is "_ = (cstep ?R)")
using assms
proof (induct)
case (insert ρ S)
then have *: "∄σ. conds_sat (R - S) (conds ρ) σ"
using conds_sat_mono [of "R - S" R "conds ρ"] by blast
from insert have [simp]: "cstep R = cstep (R - S)" by auto
from infeasible_rule [OF *] and insert.hyps
show ?case
by (subst Diff_insert) simp
qed (simp)
definition check_infeasible_rules
where
"check_infeasible_rules R = check_allm (λ(r, ps).
check_infeasible' R (conds r) ps
<+? (λe. shows ''rule '' ∘ shows_crule r ∘ shows '' is not infeasible '' ∘ shows_nl ∘ e))"
lemma check_infeasible_rules:
assumes "isOK (check_infeasible_rules R rps)"
shows "cstep (set R) = cstep (set R - fst ` set rps)"
proof -
have "∀r ∈ fst ` set rps. ¬ (∃σ. conds_sat (set R) (conds r) σ)"
using assms and check_infeasible' [of R]
by (fastforce simp: check_infeasible_rules_def conds_sat_conds_n_sat)
from infeasible_rules [OF _ this] show ?thesis by simp
qed
end