theory Reduction_Pair
imports
Term_Order
TRS.QDP_Framework
begin
context redtriple
begin
lemma SN_rel:
shows "SN_rel S NS"
unfolding SN_rel_defs
by (rule SN_subset[OF compatible_SN'[OF NS.compat SN]], regexp)
lemma SN_rel_rstep:
assumes mono: "ctxt.closed S"
shows "SN_rel (rstep S) (rstep NS)"
by (rule SN_rel_mono[OF rstep_subset[OF mono subst_S subset_refl] rstep_subset[OF wm_NS subst_NS subset_refl] SN_rel])
lemma mono_redpair_sound_ichain:
assumes mono: "ctxt.closed S"
and R: "R ⊆ NS ∪ S"
and P: "P ⊆ NS ∪ S"
shows "¬ ichain (nfs,m,S ∩ P, P - S, Q, S ∩ R, R - S) s t σ"
by (rule SN_rel_ichain, rule SN_rel_mono[OF qrstep_mono[of _ S _ "{}"] qrstep_mono[of _ NS _ "{}"]], insert R P SN_rel_rstep[OF mono], auto)
lemma mono_redpair_sound_ideriv:
assumes mono: "ctxt.closed S"
and R: "R ⊆ NS ∪ S"
shows "¬ qrs_ideriv nfs Q (S ∩ R) (R - S) ts"
using SN_rel_rstep[OF mono] qrs_ideriv_mono[of "S ∩ R" S "R - S" NS Q "{}", of nfs ts]
R unfolding qrs_ideriv_def SN_rel_ideriv by auto
end
fun mono_redpair_proc :: "('f,'v)trs ⇒ ('f,'v)trs ⇒ ('f,'v)trs ⇒ ('f,'v)trs ⇒ ('f,'v)dpp ⇒ ('f,'v)dpp ⇒ bool"
where "mono_redpair_proc S NS Ps Rs (nfs,m,P,Pw,Q,R,Rw) (nfs',m',P',Pw',Q',R',Rw') =
(ctxt.closed S ∧ R ∪ Rw' ⊆ NS ∪ S ∧ P ∪ Pw ⊆ NS ∪ S ∧ (P ∪ Pw) ∩ Ps ⊆ S
∧ (R ∪ Rw) ∩ Rs ⊆ S ∧ P' = P - Ps ∧ Pw' = Pw - Ps ∧ R' = R - Rs
∧ Rw' = Rw - Rs ∧ Q' = Q ∧ nfs' = nfs ∧ (m' ⟶ m))"
fun mono_redpair_tt :: "('f,'v)trs ⇒ ('f,'v)trs ⇒ ('f,'v)trs ⇒ ('f,'v)qreltrs ⇒ ('f,'v)qreltrs ⇒ bool"
where "mono_redpair_tt S NS Rs (nfs,Q,R,Rw) (nfs',Q',R',Rw') =
(ctxt.closed S ∧ R ∪ Rw' ⊆ NS ∪ S ∧ (R ∪ Rw) ∩ Rs ⊆ S ∧ R' = R - Rs ∧ Rw' = Rw - Rs
∧ Q' = Q ∧ nfs' = nfs)"
lemma (in redpair) manna_ness:
assumes mono: "ctxt.closed S"
and strict: "R ⊆ S"
shows "SN (rstep R)"
proof -
from mono strict subst_S have "(rstep R) ⊆ S" by (intro rstep_subset)
from SN_subset[OF SN this] show "SN (rstep R)" .
qed
lemma (in cpx_ce_af_redtriple_order) rule_shift_complexity:
assumes mono: "ctxt.closed S"
and strict: "R1 ⊆ S"
and non_strict: "Rw ∪ R2 ⊆ NS"
and cpx: "cpx_class cm cc'"
and cc': "cc' ≤ cc"
and rec: "deriv_bound_measure_class (relto (qrstep nfs Q R2) (qrstep nfs Q (Rw ∪ R1))) cm cc"
shows "deriv_bound_measure_class (relto (qrstep nfs Q (R1 ∪ R2)) (qrstep nfs Q Rw)) cm cc"
proof -
from mono strict subst_S have one: "rstep R1 ⊆ S" by (intro rstep_subset)
then have one: "qrstep nfs Q R1 ⊆ S" using qrstep_subset_rstep[of nfs Q R1] by blast
from rstep_subset[OF wm_NS subst_NS non_strict] have two: "rstep (Rw ∪ R2) ⊆ NS" .
then have two: "qrstep nfs Q (Rw ∪ R2) ⊆ NS" using qrstep_subset_rstep[of nfs Q "Rw ∪ R2"] by blast
from relto_mono[OF one two] have rel: "relto (qrstep nfs Q R1) (qrstep nfs Q Rw ∪ qrstep nfs Q R2) ⊆ relto S NS" unfolding qrstep_union .
then have rel: "relto (qrstep nfs Q R1) (qrstep nfs Q Rw ∪ qrstep nfs Q R2) ⊆ S" by (simp add: order_simps)
have bound: "deriv_bound_measure_class (relto (qrstep nfs Q R1) (qrstep nfs Q Rw ∪ qrstep nfs Q R2)) cm cc"
by (rule deriv_bound_measure_class_mono[OF rel subset_refl _ cpx_class[OF cpx]], insert cc', auto)
show ?thesis using bound rec unfolding qrstep_union by (rule deriv_bound_relto_measure_class_union)
qed
context redtriple
begin
lemma mono_redpair_proc_subset: "subset_proc (mono_redpair_proc S NS Ps Rs)"
unfolding subset_proc_def
proof (intro allI impI)
fix P Pw Q R Rw P' Pw' Q' R' Rw' and nfs nfs' m m' :: bool
assume proc: "mono_redpair_proc S NS Ps Rs (nfs,m,P,Pw,Q,R,Rw) (nfs',m',P',Pw',Q',R',Rw')"
from proc have mono: "ctxt.closed S" and R: "R' = R - Rs" and Rw: "Rw' = Rw - Rs" and Q: "Q' = Q" and P: "P' = P - Ps"
and Pw: "Pw' = Pw - Ps" and id: "nfs' = nfs" and m: "m' ⟶ m" by auto
show "R' ∪ Rw' ⊆ R ∪ Rw ∧ Q' = Q ∧ nfs' = nfs ∧ (m' ⟶ m) ∧
(∀ s t σ . min_ichain (nfs,m,P, Pw, Q, R, Rw) s t σ ⟶ (∃ i. ichain (nfs,m',P',Pw',Q',R', Rw') (shift s i) (shift t i) (shift σ i)))"
unfolding id[symmetric]
proof (intro conjI, unfold R Rw Q P Pw, rule subsetI, blast, simp, rule refl, rule m,
intro allI impI)
fix s t σ
assume min: "min_ichain (nfs',m,P,Pw,Q,R,Rw) s t σ"
then have ichain: "ichain (nfs',m',P,Pw,Q,R,Rw) s t σ" by (simp add: ichain.simps)
show "∃ i. ichain (nfs',m',P - Ps, Pw - Ps, Q, R - Rs, Rw - Rs) (shift s i) (shift t i) (shift σ i)"
proof (rule ichain_split[OF ichain], rule)
assume chain: "ichain (nfs',m',Ps ∩ (P ∪ Pw), P ∪ Pw - Ps ,Q,Rs ∩ (R ∪ Rw) ,R ∪ Rw - Rs) s t σ"
have "ichain (nfs',m',S ∩ (P ∪ Pw), P ∪ Pw - S ,Q, S ∩ (R ∪ Rw), R ∪ Rw - S) s t σ"
by (rule ichain_mono[OF chain], insert proc, auto)
moreover have "¬ ichain (nfs',m',S ∩ (P ∪ Pw), P ∪ Pw - S ,Q, S ∩ (R ∪ Rw),R ∪ Rw - S) s t σ"
by (rule mono_redpair_sound_ichain[OF mono], insert proc, auto)
ultimately show False by simp
qed
qed
qed
lemma mono_redpair_tt:
"rel_tt (mono_redpair_tt S NS Rs)"
unfolding rel_tt_def
proof (intro allI impI)
fix Q R Rw Q' R' Rw' ts nfs nfs'
assume proc: "mono_redpair_tt S NS Rs (nfs,Q,R,Rw) (nfs',Q',R',Rw')"
and ideriv: "qrs_ideriv nfs Q R Rw ts"
from proc have mono: "ctxt.closed S" and R: "R' = R - Rs" and Rw: "Rw' = Rw - Rs" and
Q: "Q' = Q" and Rns: "R ∪ Rw ⊆ NS ∪ S" and nfs: "nfs = nfs'" by auto
from qrs_ideriv_split[OF ideriv mono_redpair_sound_ideriv[OF mono Rns]]
obtain i where ideriv: "qrs_ideriv nfs Q (R - S) (Rw - S) (shift ts i)" ..
have "qrs_ideriv nfs Q (R - Rs) (Rw - Rs) (shift ts i)"
by (rule qrs_ideriv_mono[OF _ _ _ ideriv], insert proc, auto)
then show "Ex (qrs_ideriv nfs' Q' R' Rw')" unfolding R Rw Q nfs by auto
qed
end
end