theory Critical_Pair_Closure_Impl
imports
"Check-NT.Critical_Pairs_Impl"
Parallel_Closed
"Check-NT.Strongly_Closed"
Critical_Pair_Closing_Systems
QTRS.QDP_Framework_Impl
begin
definition check_strongly_closed where
"check_strongly_closed R n = do {
check_linear_trs R;
check_allm (λ (b, s, t). do {
check (¬ Option.is_none (List.find (λx. List.member (reachable_terms R s n) x) (reachable_terms R t (Suc 0))) ∧
¬ Option.is_none (List.find (λx. List.member (reachable_terms R t n) x) (reachable_terms R s (Suc 0))))
(shows ''the critical pair '' +@+ shows_term s +@+ shows '' <- . -> '' +@+ shows_term t +@+
shows '' is not strongly closed within '' +@+ shows n +@+ shows '' steps.'')
}) (critical_pairs_impl R R)
} <+? (λs. s +@+ shows_nl +@+ shows ''hence the following TRS is not strongly closed '' +@+
shows_nl +@+ shows_trs R +@+ indent s)"
lemma check_strongly_closed:
assumes "isOK(check_strongly_closed R n)"
shows "CR (rstep (set R))"
proof (rule strongly_closed_linear_CR)
from assms show "linear_trs (set R)" unfolding check_strongly_closed_def by auto
let ?red = "λs n. reachable_terms R s n"
let ?opt = "λs t. List.find (λx. List.member (?red s n) x) (?red t (Suc 0))"
{ fix s t
assume "¬ Option.is_none (?opt s t)"
then obtain r where r: "?opt s t = Some r" by (cases "?opt s t") auto
then have "List.member (?red s n) r" unfolding find_Some_iff by auto
then have mem:"r ∈ set (?red s n)" using in_set_member by fast
from r have "∃i<length (?red t (Suc 0)). r = (?red t (Suc 0)) ! i" unfolding find_Some_iff by auto
then have "r ∈ set (?red t (Suc 0))" using nth_mem by blast
with mem have "∃r. (s, r) ∈ (rstep (set R))⇧* ∧ (t, r) ∈ (rstep (set R))⇧="
using reachable_terms reachable_terms_one by metis
} note sound=this
{ fix b s t
assume "(b, s, t) ∈ critical_pairs (set R) (set R)"
with assms have *:"¬ Option.is_none (?opt s t) ∧ ¬ Option.is_none (?opt t s)"
unfolding check_strongly_closed_def by fastforce
with sound have "∃r. (s, r) ∈ (rstep (set R))⇧* ∧ (t, r) ∈ (rstep (set R))⇧="
and "∃u. (t, u) ∈ (rstep (set R))⇧* ∧ (s, u) ∈ (rstep (set R))⇧=" by blast+
}
then show "strongly_closed (set R)" unfolding strongly_closed_def by blast
qed
definition is_root_step :: "('f, 'v) rules ⇒ ('f, 'v) term ⇒ ('f, 'v) term ⇒ bool"
where
"is_root_step R s t = (∃ (l, r) ∈ set R. case match s l of
None ⇒ False
| Some σ ⇒ r ⋅ σ = t)"
lemma is_root_step:
assumes "is_root_step R s t"
shows "(s, t) ∈ rrstep (set R)"
using assms
unfolding is_root_step_def rrstep_def rstep_r_p_s_def'
by (auto split: option.splits) (force dest: match_matches)
fun is_par_rstep :: "('f, 'v) rules ⇒ ('f, 'v) term ⇒ ('f, 'v) term ⇒ bool"
where
"is_par_rstep R (Var x) (Var y) = (x = y)"
| "is_par_rstep R (Fun f ss) (Fun g ts) =
(Fun f ss = Fun g ts ∨ is_root_step R (Fun f ss) (Fun g ts) ∨
(if f = g ∧ length ss = length ts then list_all2 (is_par_rstep R) ss ts else False))"
| "is_par_rstep R s t = is_root_step R s t"
lemma is_par_rstep:
assumes "is_par_rstep R s t"
shows "(s, t) ∈ par_rstep (set R)"
using assms
proof (induct rule: is_par_rstep.induct)
case (2 R f ss g ts)
then consider (eq) "Fun f ss = Fun g ts"
| (root) "is_root_step R (Fun f ss) (Fun g ts)"
| (args) "f = g" and "length ss = length ts" and "list_all2 (is_par_rstep R) ss ts"
by (auto split: if_splits)
then show ?case
proof (cases)
case eq then show ?thesis using par_rstep_refl by auto
next
case root
from is_root_step[OF this] obtain l r σ
where "Fun f ss = l ⋅ σ" and "Fun g ts = r ⋅ σ" and lr:"(l, r) ∈ set R"
unfolding rrstep_def' by auto
then show ?thesis using par_rstep.root_step[OF lr] by metis
next
case args
{ fix i
assume i:"i < length ss"
then have si:"ss ! i ∈ set ss" by auto
from i args(2) have ti:"ts ! i ∈ set ts" by auto
from args(3) have "is_par_rstep R (ss ! i) (ts ! i)" using i list_all2_nthD by blast
with 2(1)[of "ss ! i" "ts ! i"] args(1,2) si ti have "(ss ! i, ts ! i) ∈ par_rstep (set R)"
by auto
}
then show ?thesis using args(1,2) by (auto)
qed
next
case ("3_1" R f ss y)
then have "is_root_step R (Fun f ss) (Var y)" by auto
from is_root_step[OF this] obtain l r σ
where "Fun f ss = l ⋅ σ" and "Var y = r ⋅ σ" and lr:"(l, r) ∈ set R"
unfolding rrstep_def' by auto
then show ?case using par_rstep.root_step[OF lr] by metis
next
case ("3_2" R y f ss)
then have "is_root_step R (Var y) (Fun f ss)" by auto
from is_root_step[OF this] obtain l r σ
where "Fun f ss = r ⋅ σ" and "Var y = l ⋅ σ" and lr:"(l, r) ∈ set R"
unfolding rrstep_def' by auto
then show ?case using par_rstep.root_step[OF lr] by metis
qed auto
fun root_rewrite :: "('f, 'v) rules ⇒ ('f, 'v) term ⇒ ('f, 'v) term list"
where
"root_rewrite R s = concat (map (λ (l, r).
(case match s l of
None ⇒ []
| Some σ ⇒ [(r ⋅ σ)])) R)"
lemma root_rewrite_sound:
assumes "t ∈ set (root_rewrite R s)"
shows "(s, t) ∈ rrstep (set R)"
proof -
from assms
have "∃ l r. (l,r) ∈ set R ∧ t ∈ set (case match s l of None ⇒ [] | Some σ ⇒ [r ⋅ σ])"
by auto
from this obtain l r where one:
"(l,r) ∈ set R ∧ t ∈ set (case match s l of None ⇒ [] | Some σ ⇒ [r ⋅ σ])"
by auto
from this obtain σ where two: "match s l = Some σ ∧ t ∈ {r ⋅ σ}" by (cases "match s l", auto)
hence match: "l ⋅ σ = s" using match_sound by auto
with one match one two have "(s,t) ∈ rstep_r_p_s (set R) (l,r) ε σ" unfolding rstep_r_p_s_def by (simp add: Let_def ctxt_supt_id)
thus "(s,t) ∈ rrstep (set R)" unfolding rstep_iff_rstep_r_p_s rrstep_def by blast
qed
fun parallel_rewrite :: "('f, 'v) rules ⇒ ('f, 'v) term ⇒ ('f, 'v) term list"
where
"parallel_rewrite R (Var x) = [Var x]"
| "parallel_rewrite R (Fun f ss) = remdups
(root_rewrite R (Fun f ss) @ map (λss. Fun f ss) (product_lists (map (parallel_rewrite R) ss)))"
lemma parallel_rewrite_par_step:
assumes "t ∈ set (parallel_rewrite R s)"
shows "(s, t) ∈ par_rstep (set R)"
using assms
proof (induct s arbitrary: t)
case (Fun f ss)
then consider (root) "t ∈ set (root_rewrite R (Fun f ss))"
| (args) "t ∈ set (map (λss. Fun f ss) (product_lists (map (parallel_rewrite R) ss)))"
by force
then show ?case
proof (cases)
case root
from root_rewrite_sound[OF this] obtain l r σ where "(l, r) ∈ set R"
and "l ⋅ σ = Fun f ss" and "r ⋅ σ = t"
unfolding rrstep_def rstep_r_p_s_def by auto
then show ?thesis using par_rstep.intros(1) by metis
next
case args
then obtain ts where t:"t = Fun f ts" and ts:"ts ∈ set (product_lists (map (parallel_rewrite R) ss))"
by auto
then have len:"length ss = length ts" using in_set_product_lists_length by force
{ fix i
assume i:"i < length ts"
have "ts ! i ∈ set (parallel_rewrite R (ss ! i))"
using ts[unfolded product_lists_set[of "_ ss"]]
by (auto simp: list_all2_map2[of "(λx ys. x ∈ set ys)"] intro: list_all2_nthD[OF _ i])
with Fun(1) len i have "(ss ! i, ts ! i) ∈ par_rstep (set R)" by auto
}
from par_rstep.intros(2)[OF this len] show ?thesis using t by auto
qed
qed auto
fun is_parallel_closed_cp where
"is_parallel_closed_cp R _ (False, s, t) = is_par_rstep R t s"
| "is_parallel_closed_cp R (Some n) (True, s, t) =
(¬ Option.is_none (List.find (λv. is_par_rstep R t v) (reachable_terms R s n)))"
| "is_parallel_closed_cp R None (True, s, t) =
(¬ Option.is_none (List.find (λv. is_par_rstep R t v) (parallel_rewrite R s)))"
definition check_parallel_closed where
"check_parallel_closed R n = do {
check_left_linear_trs R;
check_allm (λ (b, s, t). do {
check (is_parallel_closed_cp R n (b, s, t))
(shows ''the critical pair '' +@+ shows_term s +@+ shows '' <- . -> '' +@+ shows_term t +@+
shows '' is not (almost) parallel closed within '' +@+ shows n +@+ shows '' steps.'')
}) (critical_pairs_impl R R)
} <+? (λs. s +@+ shows_nl +@+ shows ''hence the following TRS is not (almost) parallel closed '' +@+
shows_nl +@+ shows_trs R +@+ indent s)"
lemma check_parallel_closed:
assumes "isOK(check_parallel_closed R n)"
shows "CR (rstep (set R))"
proof (rule parallel_closed_imp_CR)
from assms show "left_linear_trs (set R)" unfolding check_parallel_closed_def by auto
show "⋀p q. (False, p, q) ∈ critical_pairs (set R) (set R) ⟹ (q, p) ∈ par_rstep (set R)"
proof -
fix p q
assume "(False, p, q) ∈ critical_pairs (set R) (set R)"
with assms have "is_par_rstep R q p" unfolding check_parallel_closed_def by auto
then show "(q, p) ∈ par_rstep (set R)" using is_par_rstep by auto
qed
show "⋀p q. (True, p, q) ∈ critical_pairs (set R) (set R) ⟹
∃v. (q, v) ∈ par_rstep (set R) ∧ (p, v) ∈ (rstep (set R))⇧*"
proof -
fix p q
assume *:"(True, p, q) ∈ critical_pairs (set R) (set R)"
show "∃v. (q, v) ∈ par_rstep (set R) ∧ (p, v) ∈ (rstep (set R))⇧*"
proof (cases n)
case (Some n)
with assms * have "¬ Option.is_none (List.find (λv. is_par_rstep R q v) (reachable_terms R p n))"
unfolding check_parallel_closed_def by auto
then obtain v where "List.find (λv. is_par_rstep R q v) (reachable_terms R p n) = Some v"
by force
then have "is_par_rstep R q v" and "v ∈ set (reachable_terms R p n)"
unfolding find_Some_iff by auto
then show "∃v. (q, v) ∈ par_rstep (set R) ∧ (p, v) ∈ (rstep (set R))⇧*"
using is_par_rstep reachable_terms by blast
next
case None
with assms * have "¬ Option.is_none (List.find (λv. is_par_rstep R q v) (parallel_rewrite R p))"
unfolding check_parallel_closed_def by auto
then obtain v where "List.find (λv. is_par_rstep R q v) (parallel_rewrite R p) = Some v"
by force
then have "is_par_rstep R q v" and "v ∈ set (parallel_rewrite R p)"
unfolding find_Some_iff by auto
then show "∃v. (q, v) ∈ par_rstep (set R) ∧ (p, v) ∈ (rstep (set R))⇧*"
using is_par_rstep parallel_rewrite_par_step par_rstep_rsteps by blast
qed
qed
qed
fun is_critical_pair_closing_cp where
"is_critical_pair_closing_cp C n (False, s, t) =
(¬ Option.is_none (List.find (λv. is_par_rstep C t v) (reachable_terms C s n)))"
| "is_critical_pair_closing_cp C n (True, s, t) =
(¬ Option.is_none (List.find (λx. List.member (reachable_terms C s n) x) (reachable_terms C t n)))"
definition check_critical_pair_closing :: "('f::show, string) rules ⇒ ('f, string) rules ⇒ nat ⇒ shows check"
where
"check_critical_pair_closing R C n = do {
check_left_linear_trs R;
check_subseteq C R <+? (λt. shows ''C not a subsystem of R'');
check_allm (λ (b, s, t). do {
check (is_critical_pair_closing_cp C n (b, s, t))
(shows ''the critical pair '' +@+ shows_term s +@+ shows '' <- . -> '' +@+ shows_term t +@+
shows '' is not closed within '' +@+ shows n +@+ shows '' steps.'')
}) (critical_pairs_impl R R)
} <+? (λs. s +@+ shows_nl +@+ shows ''hence the following TRS is not critical pair closing '' +@+
shows_nl +@+ shows_trs R +@+ indent s)"
lemma check_critical_pair_closing:
assumes "isOK(check_critical_pair_closing R C n)"
"SN (rstep (set C))"
shows "CR (rstep (set R))"
proof (rule cpcs_sn)
from assms show "left_linear_trs (set R)" unfolding check_critical_pair_closing_def by auto
from assms show "SN (rstep (set C))" ..
from assms[unfolded check_critical_pair_closing_def,simplified]
have closed:"⋀ b p q. (b, p, q) ∈ critical_pairs (set R) (set R) ⟹ is_critical_pair_closing_cp C n (b, p, q)"
by fast
show "critical_pair_closing (set C) (set R)" unfolding critical_pair_closing_def
proof
from assms show "set C ⊆ set R" unfolding check_critical_pair_closing_def by auto
{ fix b p q
assume cp:"(b, p, q) ∈ critical_pairs (set R) (set R)"
have "(p, q) ∈ (rstep (set C))⇧↓"
proof (cases b)
case True
with closed[of b p q] cp
have "¬ Option.is_none (find (List.member (reachable_terms C p n)) (reachable_terms C q n))" by auto
then obtain v where "find (List.member (reachable_terms C p n)) (reachable_terms C q n) = Some v"
by force
then have "v ∈ set (reachable_terms C p n) ∧ v ∈ set (reachable_terms C q n)"
unfolding find_Some_iff by (meson in_set_member nth_mem)
then show ?thesis by (auto dest: reachable_terms)
next
case False
with closed[of b p q] cp
have "¬ Option.is_none (find (is_par_rstep C q) (reachable_terms C p n))" by auto
then obtain v where "find (is_par_rstep C q) (reachable_terms C p n) = Some v"
by force
then have "is_par_rstep C q v" and "v ∈ set (reachable_terms C p n)"
unfolding find_Some_iff by auto
then show ?thesis using is_par_rstep reachable_terms par_rstep_rsteps by blast
qed
}
then show "∀(b, p, q) ∈ critical_pairs (set R) (set R). (p, q) ∈ (rstep (set C))⇧↓" by auto
qed
show "⋀p q. (False, p, q) ∈ critical_pairs (set R) (set R) ⟹
∃v. (q, v) ∈ par_rstep (set C) ∧ (p, v) ∈ (rstep (set C))⇧*"
proof -
fix p q
assume "(False, p, q) ∈ critical_pairs (set R) (set R)"
with closed[of False p q]
have "¬ Option.is_none (find (is_par_rstep C q) (reachable_terms C p n))" by auto
then obtain v where "find (is_par_rstep C q) (reachable_terms C p n) = Some v"
by force
then have "is_par_rstep C q v" and "v ∈ set (reachable_terms C p n)"
unfolding find_Some_iff by auto
then show "∃v. (q, v) ∈ par_rstep (set C) ∧ (p, v) ∈ (rstep (set C))⇧*"
using is_par_rstep reachable_terms par_rstep_rsteps by blast
qed
qed
end