theory AC_Reduction_Pair_Processor
imports
"Check-NT.Relative_DP_Framework"
"Check-NT.Reduction_Pair"
"Check-NT.Usable_Rules"
begin
lemma (in ce_af_redpair) i_trans_sound_dp_ac:
assumes
fin_R: "finite R"
and mode: "mode_cond mode m"
and m: "m ≥ n"
and P: "(s,t) ∈ P"
and steps: "(t ⋅ σ, u ⋅ τ) ∈ (rstep RE)^*"
and SN: "SN_on (relstep R E) {t ⋅ σ}"
and ur_closed: "ur_closed_af RE ur us π"
and ur_P_closed: "ur_P_closed_af RE ur us π P"
and orient: "ur ⊆ mode_left mode"
and RE: "RE = R ∪ E"
and sym_E: "symmetric_trs E"
and AC_E: "AC_theory E"
shows "(t ⋅ itrans.i_trans_subst {} R RE E ur us (c,m) σ,
u ⋅ itrans.i_trans_subst {} R RE E ur us (c,m) τ) ∈ mode_NS mode"
proof -
let ?cn = "(c,m)"
note pre = fin_R RE sym_E AC_E
interpret itrans "{}" R RE E ur us ?cn by (rule itrans[OF pre])
let ?s = "s ⋅ σ"
let ?t = "t ⋅ σ"
let ?u = "u ⋅ τ"
let ?I = "i_trans"
let ?Is = "i_trans_subst"
let ?ssig = "s ⋅ ?Is σ"
let ?tsig = "t ⋅ ?Is σ"
let ?utau = "u ⋅ ?Is τ"
let ?QR = "qrelac {} R E"
have switch': "relstep R E = ?QR" unfolding qrelac_def by auto
have switch: "rstep RE = qrstep False {} R ∪ rstep E" unfolding RE by auto
note SN' = SN[unfolded switch']
note steps' = steps[unfolded switch]
from SN_ac_preservation_steps[OF pre SN' steps']
have SNu: "SN_on (qrelac {} R E) {u ⋅ τ}" .
from i_transVI[OF pre mode m SN' steps' ur_closed orient]
have one: "(?I ?t, ?I ?u) ∈ mode_NS mode" by simp
from P ur_P_closed have "ur_closed_term_af RE ur us π t" by auto
from i_transI[OF pre this SN'] have two: "(?tsig, ?I ?t) ∈ NS^*" by simp
from i_transII[OF SNu, THEN conjunct1] ce_orient[OF m]
have three: "(?I ?u, ?utau ) ∈ NS^*" by auto
from one two three have "(?tsig,?utau) ∈ NS^* O mode_NS mode O NS^*" by blast
thus ?thesis by simp
qed
context
fixes R E :: "('f,'v)trs"
assumes fin_R: "finite R"
and sym_E: "symmetric_trs E"
and AC_E: "AC_theory E"
begin
lemma ac_redtriple_proc_main:
assumes ur: "ur ⊆ NS"
and oP: "P ⊆ NST ∪ S"
and D: "D ∩ P ⊆ S"
and redtriple: "ce_af_redtriple S NS NST π"
and ur_closed: "ur_closed_af (R ∪ E) ur us π"
and ur_P_closed: "ur_P_closed_af (R ∪ E) ur us π P"
shows "finite_rel_dpp (D ∩ P, P - D, {}, R, E)"
proof
def mode ≡ False
fix s t σ
assume chain: "min_relchain (D ∩ P, P - D, {}, R, E) s t σ"
interpret ce_af_redtriple S NS NST π by fact
let ?I = "itrans.i_trans_subst {} R (R ∪ E) E ur us (c,n)"
def τ ≡ "λ i. ?I (σ i)"
let ?R = "rstep (R ∪ E)"
have mode: "mode_cond mode n" unfolding mode_def mode_cond_def by auto
note chain = chain[unfolded min_relchain_via_ichain ichain.simps minimal_cond_def]
from chain have P: "⋀ i. (s i, t i) ∈ P" by auto
from chain have steps: "⋀ i. (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ ?R^*" by auto
from chain have SNt: "⋀ i. SN_on (relstep R E) {t i ⋅ σ i}" by auto
let ?s = "λ i. s i ⋅ τ i"
let ?t = "λ i. t i ⋅ τ i"
let ?next = "λ i. (s (Suc i), t (Suc i))"
from ur have NS: "ur ⊆ mode_left mode" unfolding mode_def mode_left_def by auto
from i_trans_sound_dp_ac[OF fin_R mode le_refl P steps SNt ur_closed ur_P_closed NS _ sym_E AC_E]
have "⋀ i. (?t i, ?s (Suc i)) ∈ mode_NS mode" unfolding τ_def by auto
hence stepsNS: "⋀ i. (?t i, ?s (Suc i)) ∈ NS^*" unfolding mode_NS_def mode_def by auto
from oP P have allP: "⋀ i. (s i, t i) ∈ NST ∪ S" by (auto simp: ichain.simps)
from chain have inf: "INFM i. (s i, t i) ∈ D ∩ P" by simp
have piece1: "∀ i. (?t i, ?t (Suc i)) ∈ S ∨ (?t i, ?t (Suc i)) ∈ (NS ∪ NST)^* ∧ (?next i) ∉ D"
proof
fix i
show "(?t i, ?t (Suc i)) ∈ S ∨ (?t i, ?t (Suc i)) ∈ (NS ∪ NST)^* ∧ (?next i) ∉ D"
proof (cases "?next i ∈ S")
case True
hence "(?s (Suc i), ?t (Suc i)) ∈ S" using subst_S by (auto simp: subst.closed_def)
with stepsNS NS.trCompat show ?thesis by auto
next
case False
with stepsNS allP[of "Suc i"]
have one: "?next i ∈ NST" and two: "?next i ∉ S" by auto
from one have "(?s (Suc i), ?t (Suc i)) ∈ NST" using subst_NST by (auto simp: subst.closed_def)
with stepsNS[of i] have steps: "(?t i, ?t (Suc i)) ∈ NS^* O NST" by auto
have "(?t i, ?t (Suc i)) ∈ (NS ∪ NST)^*"
by (rule set_mp[OF _ steps], regexp)
with two D P show ?thesis by auto
qed
qed
hence infSeq: "∀ i. (?t i, ?t (Suc i)) ∈ (NS ∪ NST)^* ∪ S" by auto
from SN have "SN_on S {?t 0}" unfolding SN_defs by blast
from infSeq both.trCompat this have "∃ j. ∀ i ≥ j. (?t i, ?t (Suc i)) ∈ (NS ∪ NST)^* - S" by (rule non_strict_ending)
from this obtain j where one: "∀ i ≥ j. (?t i, ?t (Suc i)) ∈ (NS ∪ NST)^* - S" ..
with piece1 have ns: "∀ i ≥ j. ?next i ∉ D" by blast
from inf[unfolded INFM_nat] obtain n where n: "n > j" and s: "(s n, t n) ∈ D" by auto
from n obtain m where n: "n = Suc m" and m: "m ≥ j" by (cases n, auto)
from ns[THEN spec[of _ m]] s show False unfolding n using m by auto
qed
lemma ac_redtriple_proc:
assumes ur: "ur ⊆ NS"
and PQ: "P ∪ Q ⊆ NST ∪ S"
and D: "D ∩ (P ∪ Q) ⊆ S"
and redtriple: "ce_af_redtriple S NS NST π"
and ur_closed: "ur_closed_af (R ∪ E) ur us π"
and ur_P_closed: "ur_P_closed_af (R ∪ E) ur us π (P ∪ Q)"
and R: "R = Rs ∪ Rw"
and fin: "finite_rel_dpp (P - D, Q - D, Rs, Rw, E)"
shows "finite_rel_dpp (P, Q, Rs, Rw, E)"
by (rule finite_rel_dpp_split_top[OF fin], unfold R[symmetric],
rule ac_redtriple_proc_main[OF ur PQ D redtriple ur_closed ur_P_closed])
lemma ac_redtriple_mono_proc_main:
assumes ur: "ur ⊆ NS ∪ S"
and orient: "P ⊆ NS ∪ S"
and DP: "(D_P ∩ P) - {lr | lr. ¬ funas_term (fst lr) ⊆ us} ⊆ S"
and DR: "(D_R ∩ ur) - {lr | lr. ¬ funas_term (fst lr) ⊆ us} ⊆ S"
and mono: "ctxt.closed S"
and redtriple: "mono_ce_af_redtriple S NS NST π"
and ur_closed: "ur_closed_af (R ∪ E) ur us π"
and ur_P_closed: "ur_P_closed_af (R ∪ E) ur us π P"
shows "finite_rel_dpp (D_P ∩ P, P - D_P, D_R ∩ R, R - D_R, E)"
proof
def mode ≡ True
fix s t σ
assume chain: "min_relchain (D_P ∩ P, P - D_P, D_R ∩ R, R - D_R, E) s t σ"
interpret mono_ce_af_redtriple S NS NST π by fact
let ?R = "rstep (R ∪ E)"
have [simp]: "D_R ∩ R ∪ (R - D_R ∪ E) = R ∪ E" "D_R ∩ R ∪ (R - D_R) = R" by auto
from S_ce_compat obtain n' where S_compat: "⋀ m. m ≥ n' ⟹ ce_trs (c,m) ⊆ S" by blast
obtain k where k: "k = max n n'" by auto
hence n: "n ≤ k" by simp
from S_compat k have mode: "mode_cond mode k" unfolding mode_cond_def using mono by auto
let ?cn = "(c,k)"
note pre = fin_R refl sym_E AC_E
interpret itrans "{}" R "R ∪ E" E ur us ?cn by (rule itrans[OF pre])
let ?I = "i_trans_subst"
let ?i = i_trans
def τ ≡ "λ i. ?I (σ i)"
note chain = chain[unfolded min_relchain_via_ichain ichain.simps minimal_cond_def]
from chain have P: "⋀ i. (s i, t i) ∈ P" by auto
from chain have steps: "⋀ i. (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ ?R^*" by auto
from chain have SNt: "⋀ i. SN_on (relstep R E) {t i ⋅ σ i}" by auto
let ?s = "λ i. s i ⋅ τ i"
let ?t = "λ i. t i ⋅ τ i"
let ?next = "λ i. (s (Suc i), t (Suc i))"
from ur have NS: "ur ⊆ mode_left mode" unfolding mode_def mode_left_def by auto
{
fix i
from i_trans_sound_dp_ac[OF fin_R mode n P steps SNt ur_closed ur_P_closed NS _ sym_E AC_E]
have steps: "(?t i, ?s (Suc i)) ∈ mode_NS mode" unfolding τ_def by auto
also have "mode_NS mode ⊆ monoNS" unfolding mode_NS_def mode_def by auto
also have "… ⊆ (rstep (NS ∪ S))^*"
using rtrancl_mono[OF subset_rstep[of "NS ∪ S"]] by auto
finally have "(?t i, ?s (Suc i)) ∈ (rstep (NS ∪ S))^*" .
} note steps = this
def nfs ≡ False
def m ≡ False
have idS: "S ∪ NS = NS ∪ S" by auto
have chain: "ichain (nfs,m,S,NS,{},S,NS) s t τ"
unfolding ichain.simps qrstep_rstep_conv idS
proof (intro conjI allI)
fix i
from P[of i] orient show "(s i, t i) ∈ NS ∪ S" by auto
next
let ?Q = "qrstep False {} R ∪ rstep E"
let ?QQ = "?Q^* O qrstep False {} (D_R ∩ R) O ?Q^*"
let ?R = "rstep (NS ∪ S)"
let ?RR = "?R^* O rstep S O ?R^*"
let ?QR = "qrelac {} R E"
have switch: "relto (rstep R) (rstep E)= ?QR" unfolding qrelac_empty_is_qrstep qrelac_def by auto
have url: "ur ⊆ mode_left mode" using ur by (auto simp: mode_def mode_left_def)
show "(INFM i. (s i, t i) ∈ S) ∨
(INFM i. (t i ⋅ τ i, s (Suc i) ⋅ τ (Suc i)) ∈ ?RR)" unfolding INFM_disj_distrib[symmetric]
unfolding INFM_nat
proof (intro allI)
fix m
from chain
have "(INFM i. (s i, t i) ∈ D_P ∩ P) ∨
(INFM i. (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ ?QQ)" by (simp add: rstep_union)
from this[unfolded INFM_disj_distrib[symmetric], unfolded INFM_nat]
obtain l where l: "Suc m < l" and alt:"(s l, t l) ∈ D_P ∩ P ∨
(t l ⋅ σ l, s (Suc l) ⋅ σ (Suc l)) ∈ ?QQ" by blast
hence l': "m < l" by auto
from chain have SN: "⋀ l. SN_on ?QR {t l ⋅ σ l}" by (simp add: switch)
from alt show "∃ l > m. (s l, t l) ∈ S ∨ (t l ⋅ τ l, s (Suc l) ⋅ τ (Suc l)) ∈ ?RR"
proof
assume Ssteps: "(t l ⋅ σ l, s (Suc l) ⋅ σ (Suc l)) ∈ ?QQ"
let ?tt = "t l ⋅ τ l"
let ?st = "s (Suc l) ⋅ τ (Suc l)"
have "(?tt, ?st) ∈ monoS" unfolding τ_def
by (rule i_trans_strict_step[OF pre mode _ n SN Ssteps ur_closed ur_P_closed P url],
insert DR, auto simp: mode_def)
with rtrancl_mono[OF subset_rstep[of "NS ∪ S"]] subset_rstep[of S] have "(?tt, ?st) ∈ ?RR" by auto
with l' show ?thesis by auto
next
assume "(s l, t l) ∈ D_P ∩ P"
with DP have "(s l, t l) ∈ S ∨ ¬ funas_term (s l) ⊆ us" by force
thus ?thesis
proof
assume nwf: "¬ funas_term (s l) ⊆ us"
from l obtain ll where ll: "l = Suc ll" by (cases l, auto)
let ?ts = "t ll ⋅ σ ll"
let ?tt = "t ll ⋅ τ ll"
let ?ss = "s (Suc ll) ⋅ σ (Suc ll)"
let ?st = "s (Suc ll) ⋅ τ (Suc ll)"
from P ur_P_closed have urt: "ur_closed_term_af (R ∪ E) ur us π (t ll)" by force
from chain have steps: "(?ts, ?ss) ∈ ?Q^*" by (simp add: rstep_union)
from steps_preserve_SN_on_relto[OF steps] SN have SNs: "SN_on ?QR {?ss}" by (simp add: switch)
from i_transI[OF pre urt] have ns0: "(?tt, ?i ?ts) ∈ NS^*" unfolding τ_def using SN by simp
from i_transVI[OF pre mode n SN steps ur_closed url]
have ns1: "(?i ?ts, ?i ?ss) ∈ monoNS" unfolding mode_def mode_NS_def by simp
from i_transII[OF SNs, THEN conjunct2] nwf[unfolded ll]
have "(?i ?ss, ?st) ∈ (rstep (ce_trs (c,k)))^+" unfolding τ_def by auto
from trancl_mono[OF this mono_ce[OF mode[unfolded mode_cond_def, THEN mp[OF _ _]]]]
have strict: "(?i ?ss, ?st) ∈ S^+" unfolding mode_def by simp
from ns0 ns1 strict have strict: "(?tt,?st) ∈ NS^* O monoNS O S^+" by auto
hence "(?tt,?st) ∈ monoS" by regexp
with rtrancl_mono[OF subset_rstep[of "NS ∪ S"]] subset_rstep[of S]
have strict: "(?tt, ?st) ∈ ?RR" by auto
from l ll have "m < ll" by auto
with strict show ?thesis by blast
qed (insert l', auto)
qed
qed
qed (auto simp: steps)
have idS: "S ∩ (NS ∪ S) = S" by auto
from ichain_mono[OF chain subset_refl _ subset_refl subset_refl, of "NS ∪ S - S" "NS ∪ S - S"]
mono_redpair_sound_ichain[OF mono subset_refl subset_refl, of nfs m "{}" s t τ]
show False unfolding idS by blast
qed
lemma ac_redtriple_mono_proc:
assumes ur: "ur ⊆ NS ∪ S"
and PQ: "P ∪ Q ⊆ NS ∪ S"
and DP: "(D_P ∩ (P ∪ Q)) - {lr | lr. ¬ funas_term (fst lr) ⊆ us} ⊆ S"
and DR: "(D_R ∩ ur) - {lr | lr. ¬ funas_term (fst lr) ⊆ us} ⊆ S"
and mono: "ctxt.closed S"
and redtriple: "mono_ce_af_redtriple S NS NST π"
and ur_closed: "ur_closed_af (R ∪ E) ur us π"
and ur_P_closed: "ur_P_closed_af (R ∪ E) ur us π (P ∪ Q)"
and R: "R = Rs ∪ Rw"
and fin: "finite_rel_dpp (P - D_P, Q - D_P, Rs - D_R, Rw - D_R, E)"
shows "finite_rel_dpp (P, Q, Rs, Rw, E)"
by (rule finite_rel_dpp_split[OF fin], unfold R[symmetric],
rule ac_redtriple_mono_proc_main[OF ur PQ DP DR mono redtriple ur_closed ur_P_closed])
end
lemma SN_rel_AOCEQ: "SN_rel R (aoc_rewriting.AOCEQ A C) =
SN_rel R (acrstep A C)"
unfolding SN_rel_defs conversion_def rtrancl_idemp symcl_acstep ..
lemma (in redtriple) ac_rule_removal:
assumes re: "R ∪ E ⊆ NS ∪ S"
and r: "r ⊆ S"
and E: "acrstep A C ⊆ rstep E"
and mono: "ctxt.closed S"
and SN_rel: "SN_rel (rstep (R - r)) (aoc_rewriting.AOCEQ A C)"
shows "SN_rel (rstep R) (aoc_rewriting.AOCEQ A C)"
unfolding SN_rel_AOCEQ
unfolding SN_rel_ideriv
proof
let ?AC = "acrstep A C"
assume "∃ f. ideriv (rstep R) ?AC f"
then obtain f where f: "ideriv (rstep R) ?AC f" by auto
{
assume "∃i. ideriv (rstep R - rstep r) (?AC - rstep r) (shift f i)"
then obtain i where f: "ideriv (rstep R - rstep r) (?AC - rstep r) (shift f i)" ..
have "ideriv (rstep (R - r)) ?AC (shift f i)"
by (rule ideriv_mono[OF _ _ f], auto)
with SN_rel[unfolded SN_rel_AOCEQ, unfolded SN_rel_ideriv] have False by blast
}
with ideriv_split[OF f, of "rstep r"] have
f: "ideriv (rstep r ∩ (rstep R ∪ ?AC)) (rstep R ∪ ?AC - rstep r) f" by blast
have f: "ideriv (rstep r) (rstep (R ∪ E)) f"
by (rule ideriv_mono[OF _ _ f], insert E, auto simp: rstep_union)
have f: "ideriv S (NS ∪ S) f"
by (rule ideriv_mono[OF rstep_subset[OF mono subst_S r]
rstep_subset[OF ctxt.closed_Un[OF wm_NS mono] subst.closed_Un[OF subst_NS subst_S] re] f])
from compatible_SN'[OF compat_NS_S SN] have "SN_rel S (NS ∪ S)" unfolding SN_rel_defs .
from this[unfolded SN_rel_ideriv] f show False by blast
qed
end