theory Redundant_Rules_Impl
imports
Redundant_Rules
Equational_Reasoning_Impl
QTRS.Trs_Impl
begin
definition
check_redundant_rules :: "('f :: show, 'v :: show) rules ⇒ ('f, 'v) rules ⇒ nat ⇒ ('f, 'v) eseq list ⇒ shows check"
where
"check_redundant_rules R R' n convs = do {
let S = list_diff R' R;
let T = list_diff R R';
check_allm (λ (l, r).
check (List.member (reachable_terms R l n) r)
(shows ''could not simulate rule '' +@+ shows_rule (l, r))) S;
check_allm (λ (l, r).
(try existsM (λconv. check_conversion R' conv l r) convs catch
(λe. check_join_BFS_limit n R' l r))) T
}"
lemma check_redundant_rules:
assumes "isOK(check_redundant_rules R R' n convs)"
and "CR (rstep (set R'))"
shows "CR (rstep (set R))"
proof -
let ?S = "list_diff R' R"
let ?T = "list_diff R R'"
note ok = assms(1)[unfolded check_redundant_rules_def, simplified]
from ok have "∀ (l, r) ∈ set ?S. List.member (reachable_terms R l n) r"
by auto
hence "∀ (l, r) ∈ set ?S. r ∈ set (reachable_terms R l n)"
using in_set_member by fast+
hence S:"∀ (l, r) ∈ set ?S. (l, r) ∈ (rstep (set R))^*"
using reachable_terms by blast+
have eq:"set R ∪ set ?S = set R' ∪ set ?T" by auto
have "∀ (l, r) ∈ set ?T. (l, r) ∈ (rstep (set R'))⇧↔⇧*"
proof
fix l r
assume "(l, r) ∈ set ?T"
hence "(l, r) ∈ set R - set R'" by auto
with bspec[OF conjunct2[OF ok] this]
have "isOK (existsM (λconv. check_conversion R' conv l r) convs) ∨ isOK (check_join_BFS_limit n R' l r)"
(is "?C ∨ ?J")
by (auto split: catch_splits simp del: isOK_existsM)
thus "(l, r) ∈ (rstep (set R'))⇧↔⇧*"
proof
assume ?J
hence "(l, r) ∈ join (rstep (set R'))"
using check_join_BFS_limit_sound by blast
thus ?thesis by (metis CR_imp_conversionIff_join assms(2))
next
assume ?C
with check_conversion_sound have "(l, r) ∈ (estep (set R'))⇧*" by auto
thus ?thesis using esteps_is_conversion by auto
qed
qed
from redundant_rules_removal[OF this assms(2)]
redundant_rules[OF S] assms eq
show ?thesis by auto
qed
definition
check_redundant_rules_ncr :: "('f :: show, 'v :: show) rules ⇒ ('f, 'v) rules ⇒ nat ⇒ shows check"
where
"check_redundant_rules_ncr R R' n = do {
check_subseteq R R' <+? (λ _. shows ''old TRS is not a subsystem of given TRS'');
let S = list_diff R' R;
let T = list_diff R R';
check_allm (λ (l, r).
check (List.member (reachable_terms R l n) r)
(shows ''could not simulate rule '' +@+ shows_rule (l, r))
) S;
check_allm (λ (l, r).
check (List.member (reachable_terms R' l n) r)
(shows ''could not simulate rule '' +@+ shows_rule (l, r))
) T
}"
lemma check_redundant_rules_ncr:
assumes "isOK(check_redundant_rules_ncr R R' n)"
and "¬ CR (rstep (set R'))"
shows "¬ CR (rstep (set R))"
proof -
let ?S = "list_diff R' R"
let ?T = "list_diff R R'"
note ok = assms[unfolded check_redundant_rules_ncr_def]
from ok have "∀ (l, r) ∈ set ?S. List.member (reachable_terms R l n) r"
by simp
hence "∀ (l, r) ∈ set ?S. r ∈ set (reachable_terms R l n)"
using in_set_member by fast+
hence S:"∀ (l, r) ∈ set ?S. (l, r) ∈ (rstep (set R))^*"
using reachable_terms by blast+
from ok have "∀ (l, r) ∈ set ?T. List.member (reachable_terms R' l n) r"
by simp
hence "∀ (l, r) ∈ set ?T. r ∈ set (reachable_terms R' l n)"
using in_set_member by fast+
hence T:"∀ (l, r) ∈ set ?T. (l, r) ∈ (rstep (set R'))^*"
using reachable_terms by blast+
have "set R ∪ set ?S = set R' ∪ set ?T" by auto
with redundant_rules[OF S] redundant_rules[OF T] assms(2) show ?thesis
by simp
qed
end