theory Relative_DP_Framework
imports
TRS.QDP_Framework
Ord.Term_Order
Knuth_Bendix_Order.Lexicographic_Extension
begin
locale order_pair_restrict = base: order_pair
begin
sublocale order_pair "S ↾ X" "(NS ↾ X)⇧="
proof(unfold_locales, unfold trans_O_iff refl_O_iff)
show "Id ⊆ (NS ↾ X)⇧=" by simp
from base.trans_S_point
show "S ↾ X O S ↾ X ⊆ S ↾ X" by auto
from base.trans_NS_point
show "(NS ↾ X)⇧= O (NS ↾ X)⇧= ⊆ (NS ↾ X)⇧=" by auto
from base.compat_S_NS_point
show "S ↾ X O (NS ↾ X)⇧= ⊆ S ↾ X" by auto
from base.compat_NS_S_point
show "(NS ↾ X)⇧= O S ↾ X ⊆ S ↾ X" by auto
qed
end
lemma SN_on_imp_SN_restrict: assumes "SN_on R X" shows "SN (R ↾ X)"
proof
fix f assume chain: "chain (R ↾ X) f"
then have "f 0 ∈ X" "chain R f" by (auto simp: restrict_def)
from not_SN_onI[OF this] assms show False by auto
qed
locale SN_order_pair_restrict = base: order_pair
begin
definition "SN_terms ≡ {x. SN_on S {x}}"
interpretation order_pair_restrict..
sublocale SN_order_pair "S ↾ SN_terms" "(NS ↾ SN_terms)⇧="
by (unfold_locales, auto intro: SN_on_imp_SN_restrict simp: SN_terms_def)
end
lemma subterm_preserves_SN_rel: "SN_on (relstep R S) {s} ⟹ s ⊳ t ⟹ SN_on (relstep R S) {t}"
by(rule subterm_preserves_SN_gen, auto)
lemma SN_on_Un_supt:
assumes cl: "ctxt.closed R" and SN: "SN_on R X"
shows "SN_on (R ∪ {⊳}) X" (is "SN_on _ ?X")
proof(rule SN_on_subset2)
from ctxt_closed_supt_subset[OF cl]
have push: "{⊳} O R ⊆ R O {⊳}⇧*" by auto
from SN have "SN_on R ((({⊳} ∪ R)^^n) `` X)" for n
proof(induct n arbitrary: X)
case 0 then show ?case by auto
next
case (Suc n)
then show ?case
proof (unfold relpow_Suc relcomp_Image, intro Suc, unfold Un_Image, intro SN_on_Un2)
show "SN_on R ({⊳} `` X)" by (rule SN_on_subset2[OF _ SN_on_Image_push[OF push Suc.prems]], auto)
from Suc.prems show "SN_on R (R `` X)" by (unfold SN_on_Image_conv)
qed
qed
then have SN: "SN_on R (({⊳} ∪ R)⇧* `` X)" (is "SN_on _ ?X")
by (unfold rtrancl_is_UN_relpow UN_Image) (rule SN_on_UN, auto)
show "SN_on (R ∪ {⊳}) ?X"
proof(rule iffD2[OF SN_on_Un, OF _ conjI])
show "SN_on (relto R {⊳}) ?X"
apply (unfold SN_on_relto_relcomp, rule SN_on_O_comm, rule SN_on_O_push[OF push])
apply (rule SN_on_subset2[OF _ SN], fold relcomp_Image, rule Image_subsetI, regexp)
done
show "(R ∪ {⊳}) `` ?X ⊆ ?X" by (fold relcomp_Image, rule Image_subsetI, regexp)
show "SN_on {⊳} ?X" by (rule SN_on_subset2[OF _ SN_supt], auto)
qed
show "X ⊆ ?X" by auto
qed
lemma SN_on_relto_Un_supt:
assumes clR: "ctxt.closed R" and clS: "ctxt.closed S" and SN: "SN_on (relto R S) X"
shows "SN_on (relto R (S ∪ {⊳})) X"
proof(unfold SN_on_relto_relcomp, intro SN_onI)
from ctxt_closed_supt_subset[OF assms(2)]
have pushS: "{⊳} O S ⊆ S O {⊳}⇧*" by auto
from ctxt_closed_supt_subset[OF assms(1)]
have pushR: "{⊳} O R ⊆ R O {⊳}⇧*" by auto
from assms have cl: "ctxt.closed (S⇧* O R)" by blast
fix f assume f0: "f 0 ∈ X" and chain: "chain ((S ∪ {⊳})⇧* O R) f"
have "¬ SN_on ((S⇧* O R ∪ {⊳})⇧+) {f 0}" (is "¬ SN_on ?ord _")
proof(intro lower_set_imp_not_SN_on ballI)
fix "fi" assume "fi ∈ range f"
then obtain i where [simp]: "fi = f i" by auto
from chain have "(fi, f (Suc i)) ∈ (S ∪ {⊳})⇧* O R" by auto
also have "... ⊆ S⇧* O {⊳}⇧* O R" using rtrancl_U_push[OF pushS] by (auto simp: ac_simps)
also have "... ⊆ S⇧* O R O {⊳}⇧*" using rtrancl_O_push[OF pushR] by (auto simp: ac_simps)
also have "... ⊆ (S⇧* O R ∪ {⊳})⇧+" by regexp
finally have "(fi, f (Suc i)) ∈ ..." by auto
moreover have "f (Suc i) ∈ range f" by auto
ultimately show "∃t∈ range f. (fi,t) ∈ (S⇧* O R ∪ {⊳})⇧+" by auto
qed auto
moreover
from SN_on_Un_supt[OF cl] SN[unfolded SN_on_relto_relcomp]
have "SN_on ?ord X" by (auto simp: SN_on_trancl_SN_on_conv)
from SN_on_subset2[OF _ this] f0 have "SN_on ?ord {f 0}" by auto
ultimately show False by auto
qed
type_synonym ('f, 'v) rel_dpp =
"('f, 'v) trs × ('f, 'v) trs × ('f, 'v) trs × ('f, 'v) trs × ('f, 'v) trs"
fun min_relchain :: "('f, 'v) rel_dpp ⇒ ('f, 'v) term seq ⇒ ('f, 'v) term seq ⇒ ('f, 'v) subst seq ⇒ bool" where
"min_relchain (P,Q,R,Rw,E) s t σ =
((∀i. (s i, t i) ∈ P ∪ Q) ∧
(∀i. (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ (rstep (R ∪ Rw ∪ E))⇧*) ∧
((∃⇩∞i. (s i, t i) ∈ P) ∨
(∃⇩∞i. (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ relto (rstep R) (rstep (R ∪ Rw ∪ E)))) ∧
(∀i. SN_on (relstep (R ∪ Rw) E) {t i ⋅ σ i}))"
declare min_relchain.simps[simp del]
text ‹The following characterization admits to reuse lemmas such as
@{thm ichain_split} which are crucial for reduction pair processors, etc.›
lemma min_relchain_via_ichain: "min_relchain (P,Q,R,Rw,E) s t σ ⟷
ichain (False, False, P, Q, {}, R, Rw ∪ E) s t σ ∧ (∀i. SN_on (relstep (R ∪ Rw) E) {t i ⋅ σ i})"
by (auto simp: min_relchain.simps ichain.simps ac_simps)
lemma min_relchain_split:
assumes chain: "min_relchain (P,Q,R,Rw,E) s t σ"
and nchain: "¬ min_relchain (Ps ∩ (P ∪ Q), P ∪ Q - Ps, Rs ∩ (R ∪ Rw), R ∪ Rw - Rs, E) s t σ"
shows "∃ i. min_relchain (P - Ps, Q - Ps, R - Rs, Rw - Rs, E) (shift s i) (shift t i) (shift σ i)"
proof -
have Rw: "R ∪ Rw = (Rs ∩ (R ∪ Rw)) ∪ (R ∪ Rw - Rs)" by auto
have nchain: "¬ ichain (False,False,Ps ∩ (P ∪ Q), P ∪ Q - Ps, {}, Rs ∩ (R ∪ Rw), R ∪ Rw - Rs ∪ E) s t σ"
proof
assume ichain: "ichain (False,False,Ps ∩ (P ∪ Q), P ∪ Q - Ps, {}, Rs ∩ (R ∪ Rw), R ∪ Rw - Rs ∪ E) s t σ"
then have "min_relchain (Ps ∩ (P ∪ Q), P ∪ Q - Ps, Rs ∩ (R ∪ Rw), R ∪ Rw - Rs, E) s t σ"
unfolding min_relchain_via_ichain
using chain[unfolded min_relchain_via_ichain]
by (simp add: Rw[symmetric])
with nchain show False by auto
qed
from chain have ichain: "ichain (False,False,P,Q,{},R,Rw ∪ E) s t σ"
unfolding min_relchain_via_ichain by auto
from ichain_split_gen[OF ichain nchain] obtain i
where ichain: "ichain (False,False,P - Ps, Q - Ps, {}, R - Rs, Rw - Rs ∪ E) (shift s i) (shift t i) (shift σ i)" ..
have "min_relchain (P - Ps, Q - Ps, R - Rs, Rw - Rs, E) (shift s i) (shift t i) (shift σ i)"
unfolding min_relchain_via_ichain
by (rule conjI[OF ichain], rule allI,
rule SN_on_mono[OF _ relto_mono[OF rstep_mono[of _ "R ∪ Rw"] subset_refl]],
insert chain[unfolded min_relchain_via_ichain], auto)
then show ?thesis ..
qed
lemma min_relchain_split_top:
assumes chain: "min_relchain (P,Q,R,Rw,E) s t σ"
and nchain: "¬ min_relchain (Ps ∩ (P ∪ Q), P ∪ Q - Ps, {}, R ∪ Rw, E) s t σ"
shows "∃ i. min_relchain (P - Ps, Q - Ps, R, Rw, E) (shift s i) (shift t i) (shift σ i)"
using min_relchain_split [OF chain, of Ps "{}"] nchain by auto
definition "min_relchain_alt P Q R Rw E s t ⟷
(∀i. (s i, t i) ∈ rrstep (P ∪ Q)) ∧
(∀i. (t i, s (Suc i)) ∈ (rstep (R ∪ Rw ∪ E))⇧*) ∧
((∃⇩∞i. (s i, t i) ∈ rrstep P) ∨
(∃⇩∞i. (t i, s (Suc i)) ∈ relstep R (R ∪ Rw ∪ E))) ∧
(∀i. SN_on (relstep (R ∪ Rw) E) {t i})"
lemma min_relchain_altI:
"min_relchain (P,Q,R,Rw,E) s t σ ⟹ min_relchain_alt P Q R Rw E (λi. s i ⋅ σ i) (λi. t i ⋅ σ i)"
by (auto simp: min_relchain.simps min_relchain_alt_def INFM_mono rrstepI)
lemma min_relchain_altD:
assumes "min_relchain_alt P Q R Rw E s t"
shows "∃s t σ. min_relchain (P,Q,R,Rw,E) s t σ"
proof -
{ fix i :: nat
have "∃u v σ. (u, v) ∈ P ∪ Q ∧ s i = u ⋅ σ ∧ t i = v ⋅ σ"
using assms by (auto simp: min_relchain_alt_def elim!: rrstepE dest!: spec [of _ i]) }
then obtain u and v and σ
where *: "∀i. (u i, v i) ∈ P ∪ Q ∧ s i = u i ⋅ σ i ∧ t i = v i ⋅ σ i" by metis
consider (P) "∃⇩∞i. (s i, t i) ∈ rrstep P" | (R) "∃⇩∞i. (t i, s (Suc i)) ∈ relstep R (R ∪ Rw ∪ E)"
using assms by (auto simp: min_relchain_alt_def)
then show ?thesis
proof (cases)
let ?P = "λ i j. j ≥ i ∧ (∃u v σ. (u, v) ∈ P ∧ s j = u ⋅ σ ∧ t j = v ⋅ σ)"
define I where "I = (λi. LEAST j. ?P i j)"
case P
then have P: "∀i. ∃j. ?P i j" by (force simp: INFM_nat_le elim!: rrstepE)
then have "∀i. ∃u v σ. (u, v) ∈ P ∧ s (I i) = u ⋅ σ ∧ t (I i) = v ⋅ σ"
by (auto simp: I_def dest!: LeastI_ex)
then obtain u' and v' and σ'
where **: "∀i. (u' i, v' i) ∈ P ∧ s (I i) = u' i ⋅ σ' i ∧ t (I i) = v' i ⋅ σ' i" by metis
define U where "U ≡ λi. if ∃j. i = I j then u' (LEAST j. i = I j) else u i"
define V where "V ≡ λi. if ∃j. i = I j then v' (LEAST j. i = I j) else v i"
define S where "S ≡ λi. if ∃j. i = I j then σ' (LEAST j. i = I j) else σ i"
{ fix i :: nat
have "(U i, V i) ∈ P ∪ Q ∧ (V i ⋅ S i, U (Suc i) ⋅ S (Suc i)) ∈ (rstep (R ∪ Rw ∪ E))⇧* ∧
SN_on (relstep (R ∪ Rw) E) {V i ⋅ S i}"
using assms and * and **
by (auto simp: min_relchain_alt_def U_def V_def S_def) (metis (mono_tags, lifting) LeastI_ex)+ }
moreover
{ fix i :: nat
have "(U (I i), V (I i)) ∈ P" using ** by (auto simp: U_def V_def)
moreover have "I i ≥ i" using P by (auto simp: I_def dest!: LeastI_ex)
ultimately have "∃j≥i. (U j, V j) ∈ P" by blast }
ultimately show ?thesis by (auto simp: min_relchain.simps INFM_nat_le)
next
case R
then have "min_relchain (P,Q,R,Rw,E) u v σ"
using assms and * by (auto simp: min_relchain_alt_def min_relchain.simps)
then show ?thesis by blast
qed
qed
lemma no_chain_imp_SN_rel_ext:
assumes " ¬ (∃s t σ. min_relchain (P, Q, R, Rw, E) s t σ)"
shows "SN_rel_ext (rrstep P) (rrstep Q) (rstep R) (rstep Rw ∪ rstep E) (λt. SN_on (relstep (R ∪ Rw) E) {t})"
(is "SN_rel_ext ?P ?Q ?R (?Rw ∪ ?E) ?M")
proof (rule ccontr)
let ?rel = "SN_rel_ext_step ?P ?Q ?R (?Rw ∪ ?E)"
assume "¬ ?thesis"
from this[unfolded SN_rel_ext_def] obtain f ty where
steps: "⋀ i. (f i, f (Suc i)) ∈ ?rel (ty i)"
and min: "⋀ i. ?M (f i)"
and inf1: "INFM i. ty i ∈ {top_s,top_ns}"
and inf2: "INFM i. ty i ∈ {top_s,normal_s}" by blast
obtain p where p: "⋀ i. p i = (ty i ∈ {top_s,top_ns})" by auto
interpret infinitely_many p
by (unfold_locales, insert inf1, unfold INFM_nat_le p)
let ?ind = "infinitely_many.index p"
let ?g = "λ i. f (?ind i)"
let ?h = "λ i. f (Suc (?ind i))"
let ?prop = "λ s t σ i. (s, t) ∈ P ∪ Q ∧ ?g i = s ⋅ σ ∧ ?h i = t ⋅ σ ∧ (ty (?ind i) = top_s ⟶ (s, t) ∈ P)"
{
fix i
have "ty (?ind i) ∈ {top_s,top_ns}"
using index_p[of i] unfolding p .
then have one: "(?g i, ?h i) ∈ ?P ∪ ?Q" and two: "ty (?ind i) = top_s ⟹ (?g i, ?h i) ∈ ?P" using steps[of "?ind i"]
by auto
have "∃ s t σ. ?prop s t σ i"
proof (cases "ty (?ind i) = top_s")
case True
with two[OF True] have "(?g i, ?h i) ∈ rrstep P" by simp
then show ?thesis by (auto elim!: rrstepE)
next
case False
moreover from one have "(?g i, ?h i) ∈ rrstep (P ∪ Q)" by (auto simp: rrstep_union)
ultimately show ?thesis by (auto elim!: rrstepE)
qed
}
from choice[OF allI[OF this]] obtain s where "∀ i. ∃ t σ. ?prop (s i) t σ i" ..
from choice[OF this] obtain t where "∀ i. ∃ σ. ?prop (s i) (t i) σ i" ..
from choice[OF this] obtain σ where stσ: "⋀ i. ?prop (s i) (t i) (σ i) i" by auto
from stσ have PQ: "⋀ i. (s i, t i) ∈ P ∪ Q" by auto
from stσ have s: "⋀ i. s i ⋅ σ i = ?g i" by auto
from stσ have t: "⋀ i. t i ⋅ σ i = ?h i" by auto
from stσ have P: "⋀ i. ty (?ind i) = top_s ⟹ (s i, t i) ∈ P" by auto
{
fix i
from stσ[of i] have "?M (t i ⋅ σ i)" using min[of "Suc (?ind i)"] by auto
} note min = this
let ?f = "λ i j. f (Suc (?ind i) + j)"
let ?n = "λ i. ?ind (Suc i) - Suc (?ind i)"
let ?RE = "qrstep False {} (R ∪ (Rw ∪ E))"
have "ichain (False, False, P, Q, {}, R, Rw ∪ E) s t σ"
unfolding ichain_alternative
proof (rule exI[of _ ?f], rule exI[of _ ?n], intro conjI allI impI, rule PQ)
fix i
show "?f i 0 = t i ⋅ σ i" unfolding t by simp
next
fix i
show "?f i (?n i) = s (Suc i) ⋅ σ (Suc i)" unfolding s
using index_ordered[of i] by auto
next
fix i j
let ?k = "Suc (?ind i) + j"
obtain k where k: "?k = k" by auto
assume "j < ?n i"
with index_not_p_between[of i ?k]
have "¬ p ?k" by auto
then have "ty ?k ∈ {normal_s,normal_ns}" unfolding p k by (cases "ty k", auto)
with steps[of ?k] show "(?f i j, ?f i (Suc j)) ∈ ?RE" unfolding qrstep_union
by auto
next
let ?L = "λ i. (s i, t i) ∈ P"
let ?R = "λ i. ∃ j < ?n i. (?f i j, ?f i (Suc j)) ∈ qrstep False {} R"
show "(INFM i. ?L i) ∨ (INFM i. ?R i)"
unfolding INFM_disj_distrib[symmetric]
unfolding INFM_nat_le
proof (intro allI)
fix i
from inf2[unfolded INFM_nat_le]
obtain k where k: "k ≥ ?ind i" and ty: "ty k ∈ {top_s,normal_s}" by auto
from index_surj[OF k]
obtain j j' where kj: "k = ?ind j + j'" and j': "?ind j + j' < ?ind (Suc j)" by auto
note ty = ty[unfolded kj]
from k[unfolded kj] j' have lt: "?ind i < ?ind (Suc j)" by auto
{
assume "j < i"
then have "Suc j ≤ i" by auto
from index_ordered_le[OF this] lt have False by auto
}
then have j: "i ≤ j" by presburger
show "∃ j ≥ i. ?L j ∨ ?R j"
proof (intro exI conjI, rule j)
show "?L j ∨ ?R j"
proof (cases j')
case 0
from index_p[of j]
ty[unfolded 0] have "ty (?ind j) = top_s" unfolding p by auto
from P[OF this] show ?thesis by auto
next
case (Suc j'')
from index_not_p_between[of j "?ind j + j'", OF _ j']
have "ty (?ind j + j') ∉ {top_s,top_ns}" unfolding p Suc by auto
with ty have ty: "ty (?ind j + j') = normal_s" by auto
have j'': "j'' < ?ind (Suc j) - Suc (?ind j)" using j' unfolding Suc by auto
have "?R j"
by (rule exI[of _ j''], rule conjI[OF j''],
insert steps[of "?ind j + j'", unfolded ty], unfold Suc, auto)
then show ?thesis by auto
qed
qed
qed
qed auto
then have "min_relchain (P,Q,R,Rw,E) s t σ"
using min unfolding min_relchain_via_ichain by auto
with assms show False by auto
qed
definition finite_rel_dpp :: "('f,'v) rel_dpp ⇒ bool" where "finite_rel_dpp DPP = (¬(∃s t σ. min_relchain DPP s t σ))"
lemma finite_dpp_via_finite_rel_dpp: "finite_dpp (nfs,True,P,Pw,{},R,Rw) = finite_rel_dpp (P,Pw,R,Rw,{})"
unfolding finite_dpp_def finite_rel_dpp_def min_relchain_via_ichain[abs_def] min_ichain.simps[abs_def]
by (auto simp: minimal_cond_def ichain.simps)
lemma finite_rel_dppI[intro]: "(⋀ s t σ. min_relchain dpp s t σ ⟹ False) ⟹ finite_rel_dpp dpp"
unfolding finite_rel_dpp_def by auto
lemma finite_rel_dpp_split_top: "finite_rel_dpp (P - Ps, Q - Ps, R, Rw, E) ⟹
finite_rel_dpp (Ps ∩ (P ∪ Q), P ∪ Q - Ps, {}, R ∪ Rw, E) ⟹
finite_rel_dpp (P,Q,R,Rw,E)"
unfolding finite_rel_dpp_def using min_relchain_split_top by blast
lemma finite_rel_dpp_split: "finite_rel_dpp (P - Ps, Q - Ps, R - Rs, Rw - Rs, E) ⟹
finite_rel_dpp (Ps ∩ (P ∪ Q), P ∪ Q - Ps, Rs ∩ (R ∪ Rw), R ∪ Rw - Rs, E) ⟹
finite_rel_dpp (P,Q,R,Rw,E)"
unfolding finite_rel_dpp_def using min_relchain_split by blast
lemma finite_rel_dpp_pairs_mono: assumes fin: "finite_rel_dpp (P',Q',R,Rw,E)"
and P: "P ⊆ P'" and Q: "Q ⊆ P' ∪ Q'"
shows "finite_rel_dpp (P,Q,R,Rw,E)"
proof -
from P Q have Q: "P ∪ Q ⊆ P' ∪ Q'" by auto
have *: "⋀ x. x ⊆ x" by auto
from fin show ?thesis
unfolding finite_rel_dpp_def min_relchain_via_ichain[abs_def]
using ichain_mono[OF _ P Q * * *, of False False "{}" R "Rw ∪ E"] by blast
qed
locale relative_trss =
fixes R E :: "('f,'v) trs"
begin
definition "M = {s. SN_on (relstep R E) {s}}"
abbreviation "minstep P ≡ rrstep P ↾ M"
end
lemma Tinf_relstep_defined_root:
assumes "wf_trs (R ∪ E)" and "t ∈ Tinf (relstep R E)"
shows "defined (R ∪ E) (the (root t))"
using assms(1)
and Tinf_imp_SN_nr_first_root_step_rel[of _ False "{}" _ "{}", unfolded qrstep_rstep_conv nrqrstep_nrrstep rqrstep_rrstep_conv, OF assms(2)]
and nrrsteps_imp_eq_root_arg_rsteps [of t _ "R ∪ E"]
and assms
by (auto simp: nrrstep_union wf_trs_def defined_def elim!: rrstepE) (case_tac l; auto)+
lemma trans_trancl_eq: "trans r ⟷ r⇧+ = r" by (metis trancl_id trans_trancl)
locale relative_dp = sharp_syntax + relative_trss R E for R E :: "('f, 'v) trs" +
assumes shp_not_defined: "⋀ f n. defined (R ∪ E) (f, n) ⟹ ¬ defined (R ∪ E) (shp f, n)"
and inj_shp: "⋀ f g. shp f = shp g ⟹ f = g"
and wf: "wf_trs (R ∪ E)"
begin
lemma Tinf_sharp_imp_SN:
assumes "s ∈ Tinf (relstep R E)"
shows "SN_on (relstep R E) {♯ s}"
proof -
from Tinf_imp_SN_nr_first_root_step_rel[of _ False "{}" E "{}" R,
unfolded qrstep_rstep_conv nrqrstep_nrrstep rqrstep_rrstep_conv nrrstep_union[symmetric]
rrstep_union[symmetric], OF assms]
obtain t u where st: "(s,t) ∈ (nrrstep (R ∪ E))⇧*" and tu: "(t,u) ∈ rrstep (R ∪ E)" by auto
from rrstepE[OF tu] obtain l r σ where lr: "(l,r) ∈ R ∪ E" and t: "t = l ⋅ σ" .
from wf lr have "is_Fun l" unfolding wf_trs_def by force
then obtain f ls where l: "l = Fun f ls" by (cases l, auto)
with lr have "defined (R ∪ E) (f,length ls)" unfolding defined_def by auto
from shp_not_defined[OF this] have ndef: "¬ defined (R ∪ E) (♯ f, length ls)" by auto
from nrrsteps_imp_eq_root_arg_rsteps[OF st, unfolded t l, THEN conjunct1]
obtain ss where s: "s = Fun f ss" and len: "length ss = length ls" by (cases s, auto)
show ?thesis unfolding s sharp_term.simps
proof (rule SN_args_imp_SN_rel_rstep[OF _ _ ndef[folded len]])
fix s
assume "s ∈ set ss"
with assms[unfolded s Tinf_def] show "SN_on (relstep R E) {s}" by auto
qed (insert wf, force simp: wf_trs_def)
qed
lemma rrstep_imp_minstep:
defines "NT ≡ Tinf (relstep R E)"
assumes "{f. defined (R ∪ E) f} ⊆ F"
and "wf_trs (R ∪ E)" and "s ∈ NT"
and *: "¬ SN_on (relstep R E) {t}"
shows "(s, t) ∈ rrstep R ⟹ ∃t' ⊴ t. t' ∈ NT ∧ (♯ s, ♯ t') ∈ minstep (DP_on ♯ F R)"
and "(s, t) ∈ rrstep E ⟹ ∃t' ⊴ t. t' ∈ NT ∧ (♯ s, ♯ t') ∈ minstep (DP_on ♯ F E)"
proof -
have "wf_trs R" using assms by (auto simp: wf_trs_def)
assume "(s, t) ∈ rrstep R"
then obtain l and r and σ where "(l, r) ∈ R"
and [simp]: "s = l ⋅ σ" "t = r ⋅ σ" by (auto elim: rrstepE)
obtain u where "u ⊴ r ⋅ σ " and "u ∈ NT" using not_SN_imp_subt_Tinf [OF *] by (auto simp: NT_def)
{ fix x assume "x ∈ vars_term r"
then have "σ x ⊲ s"
using ‹(l, r) ∈ R› and ‹wf_trs R› by (auto simp: wf_trs_def dest: subst_image_subterm)
then have "SN_on (relstep R E) {σ x}" using ‹s ∈ NT› by (auto simp: NT_def Tinf_def) }
note ** = this
then have "∀x ∈ vars_term r. ¬ (σ x ⊵ u)"
using ‹u ∈ NT› by (auto simp: Tinf_def NT_def dest: subterm_preserves_SN_on_relstep)
then obtain v where "r ⊵ v" and [simp]: "u = v ⋅ σ"
using subt_instance_and_not_subst_imp_subt [OF ‹r ⋅ σ ⊵ u›] by auto
with ** obtain f and ts where [simp]: "v = Fun f ts"
using subteq_Var_imp_in_vars_term [of r] and ‹u ∈ NT› by (cases v) (auto simp: NT_def Tinf_def)
from ‹u ∈ NT› have v: "v ⋅ σ ∈ NT" by simp
then have "¬ l ⊳ v" using ‹s ∈ NT› by (auto dest: supt_subst simp: NT_def Tinf_def)
moreover have "(f, length ts) ∈ F" using ‹v ⋅ σ ∈ NT›
using assms by (auto simp: M_def dest: Tinf_relstep_defined_root)
ultimately have "(♯ l, ♯ v) ∈ DP_on ♯ F R"
using ‹r ⊵ v› and ‹(l, r) ∈ R› by (auto simp: DP_on_def)
then have "(♯(l ⋅ σ), ♯(v ⋅ σ)) ∈ rrstep (DP_on ♯ F R)"
using wf_trs_imp_lhs_Fun [OF ‹wf_trs R› ‹(l, r) ∈ R›] by auto
moreover from ‹r ⊵ v› have "r ⋅ σ ⊵ v ⋅ σ" by (rule supteq_subst)
ultimately show "∃u ⊴ t. u ∈ NT ∧ (♯ s, ♯ u) ∈ minstep (DP_on ♯ F R)"
using v ‹s ∈ NT› by (auto intro:Tinf_sharp_imp_SN simp: NT_def M_def)
next
have "wf_trs E" using assms by (auto simp: wf_trs_def)
assume "(s, t) ∈ rrstep E"
then obtain l and r and σ where "(l, r) ∈ E"
and [simp]: "s = l ⋅ σ" "t = r ⋅ σ" by (auto elim: rrstepE)
obtain u where "u ⊴ r ⋅ σ " and "u ∈ NT" using not_SN_imp_subt_Tinf [OF *] by (auto simp: NT_def)
{ fix x assume "x ∈ vars_term r"
then have "σ x ⊲ s"
using ‹(l, r) ∈ E› and ‹wf_trs E› by (auto simp: wf_trs_def dest: subst_image_subterm)
then have "SN_on (relstep R E) {σ x}" using ‹s ∈ NT› by (auto simp: NT_def Tinf_def) }
note ** = this
then have "∀x ∈ vars_term r. ¬ (σ x ⊵ u)"
using ‹u ∈ NT› by (auto simp: Tinf_def NT_def dest: subterm_preserves_SN_on_relstep)
then obtain v where "r ⊵ v" and [simp]: "u = v ⋅ σ"
using subt_instance_and_not_subst_imp_subt [OF ‹r ⋅ σ ⊵ u›] by auto
with ** obtain f and ts where [simp]: "v = Fun f ts"
using subteq_Var_imp_in_vars_term [of r] and ‹u ∈ NT› by (cases v) (auto simp: NT_def Tinf_def)
from ‹u ∈ NT› have v: "v ⋅ σ ∈ NT" by simp
then have "¬ l ⊳ v" using ‹s ∈ NT› by (auto dest: supt_subst simp: NT_def Tinf_def)
moreover have "(f, length ts) ∈ F" using ‹v ⋅ σ ∈ NT›
using assms by (auto dest: Tinf_relstep_defined_root)
ultimately have "(♯ l, ♯ v) ∈ DP_on ♯ F E"
using ‹r ⊵ v› and ‹(l, r) ∈ E› by (auto simp: DP_on_def)
then have "(♯(l ⋅ σ), ♯(v ⋅ σ)) ∈ rrstep (DP_on ♯ F E)"
using wf_trs_imp_lhs_Fun [OF ‹wf_trs E› ‹(l, r) ∈ E›] by auto
moreover from ‹r ⊵ v› have "r ⋅ σ ⊵ v ⋅ σ" by (rule supteq_subst)
ultimately show "∃u ⊴ t. u ∈ NT ∧ (♯ s, ♯ u) ∈ minstep (DP_on ♯ F E)"
using v ‹s∈NT› by (auto intro: Tinf_sharp_imp_SN simp: NT_def M_def)
qed
definition "relchain_part P Q s v n ≡
(∀i. v i ∈ Tinf (relstep R E)) ∧
s = v 0 ∧
(∀i<n. (♯ (v i), ♯ (v (Suc i))) ∈ minstep Q ∪ nrrstep E) ∧
(♯ (v n), ♯ (v (Suc n))) ∈ minstep P ∪ nrrstep R"
lemma relchain_partI [intro]:
assumes "⋀i. v i ∈ Tinf (relstep R E)"
and "s = v 0"
and "⋀i. i<n ⟹ (♯ (v i), ♯ (v (Suc i))) ∈ minstep Q ∪ nrrstep E"
and "(♯ (v n), ♯ (v (Suc n))) ∈ minstep P ∪ nrrstep R"
shows "relchain_part P Q s v n"
using assms by (auto simp: relchain_part_def)
lemma relchain_partD [dest]:
assumes "relchain_part P Q s v n"
shows "⋀i. v i ∈ Tinf (relstep R E)"
and "s = v 0"
and "⋀i. i < n ⟹ (♯ (v i), ♯ (v (Suc i))) ∈ minstep Q ∪ nrrstep E"
and "(♯ (v n), ♯ (v (Suc n))) ∈ minstep P ∪ nrrstep R"
using assms by (auto simp: relchain_part_def)
definition "starts_relchain P Q s ≡ ∃v n. relchain_part P Q s v n"
lemma starts_relchain_pred:
assumes s: "s ∈ Tinf (relstep R E)"
and st: "(♯ s, ♯ t) ∈ rrstep Q ∪ nrrstep E"
and t: "starts_relchain P Q t"
shows "starts_relchain P Q s"
proof -
obtain v n where v: "relchain_part P Q t v n" using t by (auto simp: starts_relchain_def)
define v' where "v' = (λi. if i = 0 then s else v (i-1))"
show ?thesis
proof(unfold starts_relchain_def, intro exI relchain_partI)
note * = relchain_partD[OF v]
show "v' i ∈ Tinf (relstep R E)" for i unfolding v'_def using s *(1) by auto
from Tinf_sharp_imp_SN[OF this] have M: "♯ (v' i) ∈ M" for i by (auto simp: M_def)
show "i < Suc n ⟹ (♯ (v' i), ♯ (v' (Suc i))) ∈ minstep Q ∪ nrrstep E" for i
apply (auto intro: M)
apply (unfold v'_def) using * s st apply (cases i, auto) done
show "s = v' 0" unfolding v'_def by auto
show "(♯ (v' (Suc n)), ♯ (v' (Suc (Suc n)))) ∈ minstep P ∪ nrrstep R" using * unfolding v'_def by auto
qed
qed
lemma Tinf_starts_relchain:
assumes SN_suptrel: "SN (suptrel E)" and F: "{f. defined (R ∪ E) f} ⊆ F"
and s: "s ∈ Tinf (relstep R E)" (is "_ ∈ ?M")
shows "starts_relchain (DP_on ♯ F R) (DP_on ♯ F E) s"
proof -
let ?lextwo = "lex_two (suptrel E) (supteqrel E) {(a,b). (b :: nat) < a}"
have SN: "SN ?lextwo"
by (rule lex_two[OF _ SN_suptrel SN_nat_gt], insert "suptrel_pair.compat_NS_S", blast)
from s obtain n t u
where st: "(s, t) ∈ (rstep E) ^^ n" and tu: "(t, u) ∈ (rstep R)" and u: "¬ SN_on (relstep R E) {u}"
using not_SN_on_rel_succ[OF conjunct1[OF s[unfolded Tinf_def mem_Collect_eq]]] by auto
with s show ?thesis
proof (induct "(s, n)" arbitrary: s t u n rule: SN_induct [OF SN])
case 1
then have s: "s ∈ ?M"
and st: "(s, t) ∈ (rstep E) ^^ n"
and tu: "(t, u) ∈ rstep R"
and u: "¬ SN_on (relstep R E) {u}"
by auto
note IH = 1(1)
show ?case
proof (cases "n")
case 0
then have [simp]: "s = t" using st by auto
show ?thesis
proof (cases rule: rstep_cases[OF tu])
case 1
then obtain t' where st': "(♯ s, ♯ t') ∈ minstep (DP_on ♯ F R)" and t': "t' ∈ ?M"
using rrstep_imp_minstep(1) [OF F wf s u] by auto
then show ?thesis using s unfolding starts_relchain_def
by (intro exI[of _ "λi. if i = 0 then s else t'"] exI relchain_partI, auto)
next
case 2
then have "(♯ t, ♯ u) ∈ nrrstep R" using nrrstep_imp_sharp_nrrstep by auto
moreover from s have u: "u ∈ ?M"
apply(rule Tinf_nrrstep[OF _ _ u]) unfolding nrrstep_union using 2 by auto
ultimately show ?thesis using s unfolding starts_relchain_def
by (intro exI[of _ "λi. if i = 0 then s else u"] exI, auto)
qed
next
case (Suc n')
with st obtain s' where ss': "(s,s') ∈ rstep E" and s't: "(s',t) ∈ (rstep E) ^^ n'"
by (meson relpow_Suc_D2)
from relpow_imp_rtrancl[OF s't] tu have "(s',u) ∈ relstep R E" by auto
from step_preserves_SN_on[OF this] u
have s': "¬ SN_on (relstep R E) {s'}" by auto
show ?thesis
proof (cases rule: rstep_cases[OF ss'])
case 1
from rrstep_imp_minstep(2) [OF F wf s s' this]
obtain s'' where sub: "s'' ⊴ s'" and s's'': "(♯ s, ♯ s'') ∈ rrstep (DP_on ♯ F E)" and s'': "s'' ∈ ?M"
by auto
show ?thesis
proof (cases "s'' = s'")
case
True then have s': "s' ∈ ?M" using s'' by auto
have "(s,s') ∈ supteqrel E" using ss' unfolding supteqrel_def by auto
then have "((s,n),(s',n')) ∈ ?lextwo" using Suc by auto
note IH = IH[OF this s' s't tu u]
show ?thesis
apply (rule starts_relchain_pred[OF s _ IH])
using s's'' True by auto
next
case False then have "s'' ⊲ s'" using sub by auto
then have "(s,s'') ∈ suptrel E" using ss' unfolding suptrel_def by auto
then have *: "⋀m. ((s,n),(s'',m)) ∈ ?lextwo" by auto
from s''
have "¬ SN_on (relstep R E) {s''}" by (simp add: Tinf_def)
from not_SN_on_rel_succ[OF this] obtain t' u' m
where "(s'', t') ∈ rstep E ^^ m" "(t', u') ∈ rstep R"
and "¬ SN_on ((rstep E)⇧* O rstep R O (rstep E)⇧*) {u'}" by auto
with IH[OF *[folded Suc] s'' this] s's''
show ?thesis by(intro starts_relchain_pred[OF s], auto)
qed
next
case 2
from s have s': "s' ∈ ?M"
apply (rule Tinf_nrrstep[OF _ _ s']) using 2 nrrstep_union by auto
have "(s,s') ∈ supteqrel E" using ss' unfolding supteqrel_def by auto
then have "((s,n),(s',n')) ∈ ?lextwo" using Suc by auto
from IH[OF this s' s't tu u]
show ?thesis apply(intro starts_relchain_pred[OF s])
using nrrstep_imp_sharp_nrrstep[OF 2] by auto
qed
qed
qed
qed
end
end