theory QDP_Framework
imports
Q_Relative_Rewriting
begin
type_synonym ('f, 'v) dpp =
"bool × bool × ('f, 'v) trs × ('f, 'v) trs × ('f, 'v) terms × ('f, 'v) trs × ('f, 'v) trs"
fun
ichain :: "('f, 'v) dpp ⇒ ('f, 'v) term seq ⇒ ('f, 'v) term seq ⇒ ('f, 'v) subst seq ⇒ bool"
where
"ichain (nfs, m, P, Pw, Q, R, Rw) s t σ ⟷
(∀i. (s i, t i) ∈ P ∪ Pw) ∧
((INFM i. (s i, t i) ∈ P) ∨
(INFM i. (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈
(qrstep nfs Q (R ∪ Rw))⇧* O qrstep nfs Q R O (qrstep nfs Q (R ∪ Rw))⇧*)) ∧
(∀i. (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ (qrstep nfs Q (R ∪ Rw))⇧*) ∧
(∀i. s i ⋅ σ i ∈ NF_terms Q) ∧
(∀i. NF_subst nfs (s i, t i) (σ i) Q)"
lemma ichain_alternative:
"ichain (nfs, m, P, Pw, Q, R, Rw) s t σ = (∃ f n.
(∀i. (s i,t i) ∈ P ∪ Pw) ∧
(∀i. (f i 0 = t i ⋅ σ i) ∧ (f i (n i) = s (Suc i) ⋅ σ (Suc i)) ∧
(∀ j < n i. (f i j, f i (Suc j)) ∈ qrstep nfs Q (R ∪ Rw))) ∧
(∀i. s i ⋅ σ i ∈ NF_terms Q) ∧
(∀i. NF_subst nfs (s i, t i) (σ i) Q)
∧ ((INFM i. (s i, t i) ∈ P) ∨ (INFM i. ∃ j < n i. (f i j, f i (Suc j)) ∈ qrstep nfs Q R)))" (is "?l = ?r")
proof -
let ?QR = "qrstep nfs Q (R ∪ Rw)"
let ?QRS = "?QR⇧* O qrstep nfs Q R O ?QR⇧*"
show ?thesis
proof
assume ?r
then obtain f n
where P: "(∀i. (s i,t i) ∈ P ∪ Pw)" and
steps: "⋀ i. (f i 0 = t i ⋅ σ i) ∧ (f i (n i) = s (Suc i) ⋅ σ (Suc i)) ∧
(∀ j < n i. (f i j, f i (Suc j)) ∈ qrstep nfs Q (R ∪ Rw))"
and nf: "(∀i. s i ⋅ σ i ∈ NF_terms Q)"
and nfs: "(∀i. NF_subst nfs (s i, t i) (σ i) Q)"
and inf: "(INFM i. (s i, t i) ∈ P) ∨ (INFM i. (∃ j < n i. (f i j, f i (Suc j)) ∈ qrstep nfs Q R))" (is "?one ∨ ?two") by auto
{
fix i j j'
assume j: "j ≤ j'" and j': "j' ≤ n i"
have "(f i j, f i j') ∈ ?QR⇧*"
unfolding rtrancl_fun_conv
proof (rule exI[of _ "λ n. f i (j + n)"], rule exI[of _ "j' - j"], insert j,
simp, intro allI impI)
fix m
assume "m < j' - j"
then have "j + m < j'" by auto
with j' have jm: "j + m < n i" by auto
with steps[of i]
show "(f i (j + m), f i (Suc (j+m))) ∈ ?QR" by auto
qed
} note Rsteps = this
{
fix i
from steps[of i] Rsteps[of 0 "n i" i]
have "(t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ ?QR⇧*" by auto
} note steps' = this
from inf have inf: "(INFM i. (s i, t i) ∈ P) ∨ (INFM i. (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈
?QRS)" (is "?one' ∨ ?two'")
proof
assume ?one then show ?thesis by auto
next
assume ?two
have ?two'
unfolding INFM_nat
proof (intro allI)
fix m
from ‹?two›[unfolded INFM_nat] obtain k j where k: "k > m" and j: "j < n k" and step: "(f k j, f k (Suc j)) ∈ qrstep nfs Q R" by blast
from Rsteps[of 0 j k] j have bef: "(f k 0, f k j) ∈ ?QR⇧*" by auto
from Rsteps[of "Suc j" "n k" k] j have aft: "(f k (Suc j), f k (n k)) ∈ ?QR⇧*" by auto
from bef step aft have "(f k 0, f k (n k)) ∈ ?QRS" by auto
with steps[of k] have main: "(t k ⋅ σ k, s (Suc k) ⋅ σ (Suc k)) ∈ ?QRS" by auto
show "∃ k > m. (t k ⋅ σ k, s (Suc k) ⋅ σ (Suc k)) ∈ ?QRS"
by (intro exI conjI, rule k, rule main)
qed
then show ?thesis ..
qed
from P nf nfs steps' inf show ?l by simp
next
assume ?l
let ?pair = "λ i. (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i))"
let ?strict = "λ i. ?pair i ∈ ?QRS"
from ‹?l› have P: "∀ i. (s i, t i) ∈ P ∪ Pw"
and inf: "(∃⇩∞i. (s i, t i) ∈ P) ∨
(∃⇩∞i. ?strict i)" (is "?one ∨ ?two")
and steps: "⋀ i. ?pair i ∈ ?QR⇧*"
and nf: "∀ i. s i ⋅ σ i ∈ NF_terms Q"
and nfs: "(∀i. NF_subst nfs (s i, t i) (σ i) Q)" by auto
{
fix i
note steps[of i, unfolded rtrancl_fun_conv]
} note fns = this
{
fix i
assume "?strict i"
then obtain u v where bef: "(t i ⋅ σ i, u) ∈ ?QR⇧*"
and step: "(u,v) ∈ qrstep nfs Q R"
and aft: "(v,s (Suc i) ⋅ σ (Suc i)) ∈ ?QR⇧*" by auto
from bef[unfolded rtrancl_fun_conv] obtain fb nb
where b: "fb 0 = t i ⋅ σ i ∧ fb nb = u ∧ (∀ i < nb. (fb i, fb (Suc i)) ∈ ?QR)" by auto
from aft[unfolded rtrancl_fun_conv] obtain fa na
where a: "fa 0 = v ∧ fa na = s (Suc i) ⋅ σ (Suc i) ∧ (∀ i < na. (fa i, fa (Suc i)) ∈ ?QR)" by auto
let ?f = "λ n. if n ≤ nb then fb n else fa (n - Suc nb)"
let ?n = "Suc (nb + na)"
{
fix i
assume i: "i < ?n"
have "(?f i, ?f (Suc i)) ∈ ?QR"
proof (cases "i < nb")
case True
with b show ?thesis by auto
next
case False note oFalse = this
show ?thesis
proof (cases "i = nb")
case True
with a b qrstep_mono[of R "R ∪ Rw" Q Q] step show ?thesis by auto
next
case False
with oFalse have "i > nb" by auto
then have "i = i - Suc nb + Suc nb" by auto
then obtain ii where ii: "i = ii + Suc nb" ..
with i have i: "ii < na" by auto
from i a show ?thesis unfolding ii by simp
qed
qed
} note steps = this
from a b step have step: "(?f nb, ?f (Suc nb)) ∈ qrstep nfs Q R" by auto
have step: "∃ n < ?n. (?f n, ?f (Suc n)) ∈ qrstep nfs Q R"
by (rule exI[of _ nb], rule conjI[OF _ step], simp)
have "∃ f n. f 0 = (t i ⋅ σ i) ∧ f n = (s (Suc i) ⋅ σ (Suc i)) ∧ (∀ m < n. (f m, f (Suc m)) ∈ ?QR) ∧ (∃ k < n. (f k, f (Suc k)) ∈ qrstep nfs Q R)"
by (rule exI[of _ ?f], rule exI[of _ ?n], simp add: step steps a b)
} note gns = this
let ?Pf = "λ f n i.
f 0 = (t i ⋅ σ i) ∧ f n = (s (Suc i) ⋅ σ (Suc i)) ∧ (∀ m < n. (f m, f (Suc m)) ∈ ?QR)"
let ?Pg = "λ f n i. ?strict i ⟶
?Pf f n i ∧ (∃ k < n. (f k, f (Suc k)) ∈ qrstep nfs Q R)"
from choice[OF allI[OF fns]] obtain f where "∀ i. ∃ n. ?Pf (f i) n i" ..
from choice[OF this] obtain nf where f: "⋀ i. ?Pf (f i) (nf i) i" by auto
from gns have "∀ i. ∃ f n. ?Pg f n i" by auto
from choice[OF this] obtain g where "∀ i. ∃ n. ?Pg (g i) n i" by auto
from choice[OF this] obtain ng where g: "⋀ i. ?Pg (g i) (ng i) i" by auto
let ?f = "λ i. if ?strict i then g i else f i"
let ?n = "λ i. if ?strict i then ng i else nf i"
show ?r
proof (rule exI[of _ ?f], rule exI[of _ ?n], rule conjI[OF P], rule conjI[OF _ conjI[OF nf conjI[OF nfs]]])
show "∀ i. ?Pf (?f i) (?n i) i"
proof
fix i
show "?Pf (?f i) (?n i) i"
using f g by (cases "?strict i", auto)
qed
next
from inf
show "?one ∨ (INFM i. ∃ j < ?n i. (?f i j, ?f i (Suc j)) ∈ qrstep nfs Q R)" (is "_ ∨ ?two'")
proof
assume ?one then show ?thesis ..
next
assume ?two
have ?two'
unfolding INFM_nat
proof (intro allI)
fix m
from ‹?two›[unfolded INFM_nat] obtain n where n: "n > m" and s: "?strict n" by blast
from g[of n] s have j: "∃ j < ?n n. (?f n j, ?f n (Suc j)) ∈ qrstep nfs Q R" by auto
show "∃ i > m. ∃ j < ?n i. (?f i j, ?f i (Suc j)) ∈ qrstep nfs Q R"
by (rule exI, intro conjI, rule n, rule j)
qed
then show ?thesis ..
qed
qed
qed
qed
definition "minimal_cond nfs Q R s t σ ⟷ (∀i. SN_on (qrstep nfs Q R) {t i ⋅ σ i})"
text ‹
A \emph{minimal infinite chain} is an infinite chain where additionally all @{term σ}-instances
of terms in the sequence~@{term t} are terminating w.r.t.~@{term R}.
›
fun min_ichain ::
"('f, 'v) dpp ⇒ ('f, 'v) term seq ⇒ ('f, 'v) term seq ⇒ ('f, 'v) subst seq ⇒ bool"
where
"min_ichain (nfs, m, P, Pw, Q, R, Rw) s t σ ⟷
ichain (nfs, m, P, Pw, Q, R, Rw) s t σ ∧ (m ⟶ minimal_cond nfs Q (R ∪ Rw) s t σ)"
definition
funas_ichain ::
"(nat ⇒ ('f, 'v) term) ⇒ (nat ⇒ ('f, 'v) term) ⇒ (nat ⇒ ('f, 'v) subst) ⇒ 'f sig"
where
"funas_ichain s t σ = ⋃{⋃(funas_term ` range (σ i)) | i. True}"
lemma funas_ichain_shift: "funas_ichain (shift s i) (shift t i) (shift σ i) ⊆ funas_ichain s t σ" unfolding funas_ichain_def by auto
fun min_ichain_sig ::
"('f,'v)dpp ⇒ 'f sig ⇒ (nat ⇒ ('f,'v)term) ⇒ (nat ⇒ ('f,'v)term) ⇒ (nat ⇒ ('f,'v)subst) ⇒ bool"
where "min_ichain_sig dpp F s t σ = (min_ichain dpp s t σ ∧ funas_ichain s t σ ⊆ F)"
lemma ichain_imp_map_ichain:
assumes chain: "ichain (nfs,m,P,Pw,Q,R,Rw) s t σ"
shows "ichain (nfs,m,map_funs_trs fg P, map_funs_trs fg Pw,{},map_funs_trs fg R,map_funs_trs fg Rw) (λ i. map_funs_term fg (s i)) (λ i. map_funs_term fg (t i)) (λ i. map_funs_subst fg (σ i))"
(is "ichain (_,_,?lP, ?lPw,{},?lR,?lRw) ?ls ?lt ?lsig")
proof -
have mem: "∀ i. (?ls i, ?lt i) ∈ ?lP ∪ ?lPw"
proof
fix i
from chain have "(s i, t i) ∈ P ∪ Pw" by auto
then show "(?ls i, ?lt i) ∈ ?lP ∪ ?lPw" by (force simp: map_funs_trs.simps)
qed
let ?QRW = "qrstep nfs Q (R ∪ Rw)"
let ?QR = "qrstep nfs Q R"
from chain have inf: "(INFM i. (s i, t i) ∈ P) ∨ (INFM i. (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ ?QRW⇧* O ?QR O ?QRW⇧*) " (is "?P ∨ ?R") by auto
let ?ilP = "INFM i. (?ls i, ?lt i) ∈ ?lP"
{
assume ?P
then have ?ilP unfolding INFM_nat
by (force simp: map_funs_trs.simps)
} note inf1 = this
let ?RR = "(rstep (?lR ∪ ?lRw))⇧* O rstep ?lR O (rstep (?lR ∪ ?lRw))⇧*"
let ?ilR = "INFM i. (?lt i ⋅ ?lsig i, ?ls (Suc i) ⋅ ?lsig (Suc i)) ∈ ?RR"
{
assume ?R
have ?ilR
unfolding INFM_nat
proof
fix m
from ‹?R›[unfolded INFM_nat]
obtain n where n: "n > m" and steps: "(t n ⋅ σ n, s (Suc n) ⋅ σ (Suc n)) ∈ ?QRW⇧* O ?QR O ?QRW⇧*" by blast
from steps obtain u v where steps: "(t n ⋅ σ n, u) ∈ ?QRW⇧*" "(u,v) ∈ ?QR" "(v,s (Suc n) ⋅ σ (Suc n)) ∈ ?QRW⇧*" by auto
from qrsteps_imp_map_rsteps[OF steps(1), of fg]
qrstep_imp_map_rstep[OF steps(2), of fg]
qrsteps_imp_map_rsteps[OF steps(3), of fg]
have "(map_funs_term fg (t n ⋅ σ n), map_funs_term fg (s (Suc n) ⋅ σ (Suc n))) ∈ ?RR"
unfolding map_funs_trs_union by auto
then show "∃ n > m. (?lt n ⋅ ?lsig n, ?ls (Suc n) ⋅ ?lsig (Suc n)) ∈ ?RR"
using n by auto
qed
} note inf2 = this
from inf inf1 inf2 have inf: "?ilP ∨ ?ilR" by blast
have steps: "∀ i. (?lt i ⋅ ?lsig i, ?ls (Suc i) ⋅ ?lsig (Suc i)) ∈ (rstep (?lR ∪ ?lRw))⇧*"
proof
fix i
from chain have "(t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ (qrstep nfs Q (R ∪ Rw))⇧*" by auto
from qrsteps_imp_map_rsteps[OF this]
have steps: "(map_funs_term fg (t i ⋅ σ i), map_funs_term fg (s (Suc i) ⋅ σ (Suc i))) ∈ (rstep (map_funs_trs fg (R ∪ Rw)))⇧*" .
have "map_funs_trs fg (R ∪ Rw) = ?lR ∪ ?lRw" unfolding map_funs_trs_union ..
from steps[unfolded this] show"(?lt i ⋅ ?lsig i, ?ls (Suc i) ⋅ ?lsig (Suc i)) ∈ (rstep (?lR ∪ ?lRw))⇧*" by auto
qed
from mem steps inf show ?thesis by simp
qed
lemma min_ichain_imp_ichain:
assumes "min_ichain DPP s t σ" shows "ichain DPP s t σ"
using assms by (cases DPP) simp_all
definition ci_subset :: "('f, 'v) trs ⇒ ('f, 'v) trs ⇒ bool" where
"ci_subset R S ⟷ (∀ l r. (l,r) ∈ R ⟶ (∃ l' r' C. (l',r') ∈ S ∧ l = C⟨l'⟩ ∧ r = C⟨r'⟩))"
notation (xsymbols)
ci_subset ("(_/ ⊆ci _)" [50,51] 50)
lemma ci_subsetI:
assumes "R ⊆ S"
shows "ci_subset R S"
unfolding ci_subset_def
proof (intro allI impI)
fix l r
assume "(l,r) ∈ R"
with assms have S: "(l,r) ∈ S" by auto
show "∃ l' r' C. (l',r') ∈ S ∧ l = C⟨l'⟩ ∧ r = C⟨r'⟩"
by (rule exI[of _ l], rule exI[of _ r], rule exI[of _ □], simp add: S)
qed
lemma ci_subset_refl: "R ⊆ci R"
proof (unfold ci_subset_def, intro allI impI)
fix l r
assume rule: "(l,r) ∈ R"
show "∃ l' r' C. (l', r') ∈ R ∧ l = C⟨l'⟩ ∧ r = C⟨r'⟩"
by (rule exI[of _ l], rule exI[of _ r], rule exI[of _ □], auto simp: rule)
qed
lemma ctxt_qrstep_subset:
assumes "⋀ l r. (l,r) ∈ R ⟹ (∃ l' r' C σ . (l',r') ∈ S ∧ l = C⟨l' ⋅ σ⟩ ∧ r = C⟨r' ⋅ σ⟩)"
and nnfs: "¬ nfs"
shows "qrstep nfs Q R ⊆ qrstep nfs Q S"
proof (rule subsetI, simp add: split_paired_all)
fix s t
assume "(s,t) ∈ qrstep nfs Q R"
then obtain C σ l r where nf: "∀ u ⊲ l ⋅ σ. u ∈ NF_terms Q" and lr: "(l,r) ∈ R" and s: "s = C⟨l⋅σ⟩" and t: "t = C⟨r⋅σ⟩"
and nfs: "NF_subst nfs (l,r) σ Q" by auto
from lr assms obtain l' r' C' σ' where Srule: "(l',r') ∈ S" and l: "l = C'⟨l' ⋅ σ'⟩" and r: "r = C'⟨r' ⋅ σ'⟩"
by (force simp: Let_def)+
let ?D = "C ∘⇩c (C' ⋅⇩c σ)"
let ?sig = "σ' ∘⇩s σ"
have s2: "s = ?D⟨l' ⋅ ?sig⟩" by (simp add: s l)
have t2: "t = ?D⟨r' ⋅ ?sig⟩" by (simp add: t r)
show "(s,t) ∈ qrstep nfs Q S"
proof(rule qrstepI[OF _ Srule s2 t2], intro allI impI)
fix u
assume gt: "l' ⋅ σ' ∘⇩s σ ⊳ u"
have "l ⋅ σ ⊵ l' ⋅ σ' ∘⇩s σ" unfolding l by auto
from supteq_supt_trans[OF this gt] nf
show "u ∈ NF_terms Q" by auto
qed (insert nnfs, simp)
qed
lemma qrstep_ci_mono: assumes "R ⊆ci S" and nfs: "¬ nfs"
shows "qrstep nfs Q R ⊆ qrstep nfs Q S"
proof(rule ctxt_qrstep_subset[OF _ nfs])
fix l r
assume "(l,r) ∈ R"
with assms obtain l' r' C where cond: "(l',r') ∈ S ∧ l = C⟨l'⟩ ∧ r = C⟨r'⟩" unfolding ci_subset_def by blast
show "∃ l' r' C σ. (l',r') ∈ S ∧ l = C⟨l' ⋅ σ⟩ ∧ r = C⟨r' ⋅ σ⟩"
by (rule exI[of _ l'], rule exI[of _ r'], rule exI[of _ C], rule exI[of _ Var], simp add: cond)
qed
lemma minimal_cond_mono:
assumes subset: "R ⊆ R'" and cond: "minimal_cond nfs Q R' s t σ"
shows "minimal_cond nfs Q R s t σ"
unfolding minimal_cond_def
proof
fix i
from cond have SN: "SN_on (qrstep nfs Q R') {t i ⋅ σ i}"
unfolding minimal_cond_def by auto
have "qrstep nfs Q R ⊆ qrstep nfs Q R'" by (rule qrstep_rules_mono[OF subset])
with SN show "SN_on (qrstep nfs Q R) {t i ⋅ σ i}" by (rule SN_on_subset1)
qed
lemma minimal_cond_ci_mono:
assumes subset: "R ⊆ci R'" and cond: "minimal_cond nfs Q R' s t σ"
and nfs: "¬ nfs"
shows "minimal_cond nfs Q R s t σ"
unfolding minimal_cond_def
proof
fix i
from cond have SN: "SN_on (qrstep nfs Q R') {t i ⋅ σ i}"
unfolding minimal_cond_def by auto
have "qrstep nfs Q R ⊆ qrstep nfs Q R'" by (rule qrstep_ci_mono[OF subset nfs])
with SN show "SN_on (qrstep nfs Q R) {t i ⋅ σ i}" by (rule SN_on_subset1)
qed
lemma min_ichainI[intro]:
assumes sub: "R ∪ Rw ⊆ R' ∪ Rw'" and m: "m ⟹ minimal_cond nfs Q (R' ∪ Rw') s t σ" and i: "ichain (nfs,m,P,Pw,Q,R,Rw) (shift s i) (shift t i) (shift σ i)"
shows "min_ichain (nfs,m,P,Pw,Q,R,Rw) (shift s i) (shift t i) (shift σ i)"
proof (cases m)
case False
with assms show ?thesis by simp
next
case True
from minimal_cond_mono[OF sub m[OF True]]
have "minimal_cond nfs Q (R ∪ Rw) (shift s i) (shift t i) (shift σ i)"
unfolding minimal_cond_def by auto
with i show ?thesis by auto
qed
lemma min_ichain_ciI:
assumes sub: "R ∪ Rw ⊆ci R' ∪ Rw'" and nfs: "¬ nfs" and m: "m ⟹ minimal_cond nfs Q (R' ∪ Rw') s t σ" and i: "ichain (nfs,m,P,Pw,Q,R,Rw) (shift s i) (shift t i) (shift σ i)"
shows "min_ichain (nfs,m,P,Pw,Q,R,Rw) (shift s i) (shift t i) (shift σ i)"
proof (cases m)
case False
with assms show ?thesis by simp
next
case True
from minimal_cond_ci_mono[OF sub m[OF True] nfs]
have "minimal_cond nfs Q (R ∪ Rw) (shift s i) (shift t i) (shift σ i)"
unfolding minimal_cond_def by auto
with i show ?thesis by auto
qed
lemma ichain_split_gen: assumes chain: "ichain (nfs,m,P,Pw,Q,R,Rw ∪ E) s t σ"
and nchain: "¬ ichain (nfs,m,Ps ∩ (P ∪ Pw), P ∪ Pw - Ps, Q, Rs ∩ (R ∪ Rw), R ∪ Rw - Rs ∪ E) s t σ"
shows "∃ i. ichain (nfs,m,P - Ps, Pw - Ps, Q, R - Rs, Rw - Rs ∪ E) (shift s i) (shift t i) (shift σ i)"
proof -
have Pw: "P ∪ Pw = (Ps ∩ (P ∪ Pw)) ∪ (P ∪ Pw - Ps)" by auto
have Rw: "R ∪ (Rw ∪ E) = (Rs ∩ (R ∪ Rw)) ∪ (R ∪ Rw - Rs ∪ E)" by auto
let ?Rw = "qrstep nfs Q (R ∪ (Rw ∪ E))"
let ?R = "qrstep nfs Q R"
from chain[unfolded ichain_alternative]
obtain f n where P: "⋀ i. (s i, t i) ∈ P ∪ Pw"
and steps: "⋀ i. f i 0 = t i ⋅ σ i ∧ f i (n i) = s (Suc i) ⋅ σ (Suc i) ∧ (∀ j < n i. (f i j, f i (Suc j)) ∈ ?Rw)"
and nf: "⋀ i. s i ⋅ σ i ∈ NF_terms Q"
and nfs: "⋀ i. NF_subst nfs (s i, t i) (σ i) Q"
and inf: "(INFM i. (s i, t i) ∈ P) ∨ (INFM i. ∃ j < n i. (f i j, f i (Suc j)) ∈ ?R)" by auto
show ?thesis
proof (cases "(INFM i. (s i, t i) ∈ Ps ∩ (P ∪ Pw)) ∨ (INFM i. ∃ j < n i. (f i j, f i (Suc j)) ∈ qrstep nfs Q (Rs ∩ (R ∪ Rw)))")
case True
have "ichain (nfs,m,Ps ∩ (P ∪ Pw), P ∪ Pw - Ps, Q, Rs ∩ (R ∪ Rw), R ∪ Rw - Rs ∪ E) s t σ"
unfolding ichain_alternative
by (rule exI[of _ f], rule exI[of _ n], insert True P steps nf nfs, simp add: Rw[symmetric])
with nchain
show ?thesis ..
next
case False
from False[unfolded de_Morgan_disj not_INFM MOST_conj_distrib[symmetric], unfolded MOST_nat]
obtain i where Pn: "⋀ j. i < j ⟹ (s j, t j) ∉ Ps ∩ (P ∪ Pw)"
and Rn: "⋀ j k. i < j ⟹ k < n j ⟹ (f j k, f j (Suc k)) ∉ qrstep nfs Q (Rs ∩ (R ∪ Rw))"
by auto
from P Pn have P: "⋀ j. i < j ⟹ (s j, t j) ∈ P ∪ Pw - Ps" by auto
{
fix j
assume j: "i < j"
{
fix k
assume k: "k < n j"
from steps[of j] k have step: "(f j k, f j (Suc k)) ∈ ?Rw" by auto
from Rn[OF j k] have nstep: "(f j k, f j (Suc k)) ∉ qrstep nfs Q (Rs ∩ (R ∪ Rw))" by auto
from step nstep have "(f j k, f j (Suc k)) ∈ qrstep nfs Q (R ∪ Rw - Rs ∪ E)"
unfolding qrstep_rule_conv[where R = "R ∪ (Rw ∪ E)"]
unfolding qrstep_rule_conv[where R = "R ∪ Rw - Rs ∪ E"]
unfolding qrstep_rule_conv[where R = "Rs ∩ (R ∪ Rw)"] by blast
}
} note R = this
from inf have inf: "(INFM j. (shift s (Suc i) j, shift t (Suc i) j) ∈ P - Ps) ∨
(INFM j. ∃ k < n (j + Suc i). (f (j + Suc i) k, f (j + Suc i) (Suc k)) ∈ qrstep nfs Q (R - Rs))" (is "?l ∨ ?r")
proof
assume iP: "INFM i. (s i, t i) ∈ P"
have ?l unfolding INFM_nat
proof
fix m
from iP[unfolded INFM_nat]
obtain n where n: "m + Suc i < n" and "(s n, t n) ∈ P" by auto
with P[of n] have P: "(s n, t n) ∈ P - Ps" by auto
show "∃ n > m. (shift s (Suc i) n, shift t (Suc i) n) ∈ P - Ps"
by (rule exI[of _ "n - Suc i"], insert n P, auto)
qed
then show ?thesis ..
next
assume iR: "INFM j. ∃ k < n j. (f j k, f j (Suc k)) ∈ ?R"
have ?r unfolding INFM_nat
proof
fix m
from iR[unfolded INFM_nat]
obtain mm k where mm: "m + Suc i < mm" and k: "k < n mm" and step: "(f mm k, f mm (Suc k)) ∈ ?R" by blast
from Rn[OF _ k] mm have step2: "(f mm k, f mm (Suc k)) ∉ qrstep nfs Q (Rs ∩ (R ∪ Rw))" by auto
from step step2 have R: "(f mm k, f mm (Suc k)) ∈ qrstep nfs Q (R - Rs)"
unfolding qrstep_rule_conv[of _ _ nfs _ R]
unfolding qrstep_rule_conv[of _ _ nfs _ "Rs ∩ (R ∪ Rw)"]
unfolding qrstep_rule_conv[of _ _ nfs _ "R - Rs"]
by auto
show "∃ mm > m. ∃ k < n (mm + Suc i). (f (mm + Suc i) k, f (mm + Suc i) (Suc k)) ∈ qrstep nfs Q (R - Rs)"
by (rule exI[of _ "mm - Suc i"], insert mm k R, auto)
qed
then show ?thesis ..
qed
let ?g = "λ j. f (j + Suc i)"
let ?n = "λ j. n (j + Suc i)"
have id: "R - Rs ∪ (Rw - Rs ∪ E) = R ∪ Rw - Rs ∪ E" by auto
show ?thesis
by (rule exI[of _ "Suc i"], unfold ichain_alternative, rule exI[of _ ?g], rule exI[of _ ?n], intro conjI,
insert P, simp,
unfold id, insert R steps, simp,
insert nf, simp,
insert nfs, simp,
insert inf, simp)
qed
qed
lemma ichain_split: assumes chain: "ichain (nfs,m,P,Pw,Q,R,Rw) s t σ"
and nchain: "¬ ichain (nfs,m,Ps ∩ (P ∪ Pw), P ∪ Pw - Ps, Q, Rs ∩ (R ∪ Rw), R ∪ Rw - Rs) s t σ"
shows "∃ i. ichain (nfs,m,P - Ps, Pw - Ps, Q, R - Rs, Rw - Rs) (shift s i) (shift t i) (shift σ i)"
using ichain_split_gen[of nfs m P Pw Q R Rw "{}" s t σ Ps Rs] assms by auto
lemma ichain_split_P: assumes chain: "ichain (nfs,m,P,Pw,Q,R,Rw) s t σ"
and nchain: "¬ ichain (nfs,m,Ps ∩ (P ∪ Pw), P ∪ Pw - Ps, Q, {}, R ∪ Rw) s t σ"
shows "∃ i. ichain (nfs,m,P - Ps, Pw - Ps, Q, R, Rw) (shift s i) (shift t i) (shift σ i)"
using ichain_split[OF chain, of Ps "{}"] nchain by auto
lemma ichain_mono_plain: assumes ichain: "ichain (nfs,m,P,Pw,Q,R,Rw) s t σ"
and P: "P ⊆ P'"
and Pw: "P ∪ Pw ⊆ P' ∪ Pw'"
and Q: "NF_terms Q ⊆ NF_terms Q'"
and R: "qrstep nfs Q R ⊆ qrstep nfs Q' R'"
and Rw: "qrstep nfs Q (R ∪ Rw) ⊆ qrstep nfs Q' (R' ∪ Rw')"
shows "ichain (nfs,m,P',Pw',Q',R',Rw') s t σ"
proof -
from ichain obtain f n
where main: " (∀i. (s i, t i) ∈ P ∪ Pw) ∧
(∀i. f i 0 = t i ⋅ σ i ∧
f i (n i) = s (Suc i) ⋅ σ (Suc i) ∧
(∀j<n i. (f i j, f i (Suc j)) ∈ qrstep nfs Q (R ∪ Rw))) ∧
(∀i. s i ⋅ σ i ∈ NF_terms Q)"
and nfs: "⋀ i. NF_subst nfs (s i, t i) (σ i) Q"
and inf: "((INFM i. (s i, t i) ∈ P) ∨ (INFM i. ∃j<n i. (f i j, f i (Suc j)) ∈ qrstep nfs Q R))"
unfolding ichain_alternative by blast
{
fix i
from nfs[of i] have nfs: "NF_subst nfs (s i, t i) (σ i) Q'"
using Q unfolding NF_subst_def by auto
} note nfs = this
from inf have inf: "((INFM i. (s i, t i) ∈ P') ∨ (INFM i. ∃j<n i. (f i j, f i (Suc j)) ∈ qrstep nfs Q' R'))" unfolding INFM_nat using P R by blast
show ?thesis unfolding ichain_alternative
by (rule exI[of _ f], rule exI[of _ n],
insert main R Rw Q P Pw inf nfs, auto)
qed
lemma ichain_mono: assumes ichain: "ichain (nfs,m,P,Pw,Q,R,Rw) s t σ"
and P: "P ⊆ P'"
and Pw: "P ∪ Pw ⊆ P' ∪ Pw'"
and Q: "NF_terms Q ⊆ NF_terms Q'"
and R: "R ⊆ R'"
and Rw: "R ∪ Rw ⊆ R' ∪ Rw'"
shows "ichain (nfs,m,P',Pw',Q',R',Rw') s t σ"
by (rule ichain_mono_plain[OF ichain P Pw Q qrstep_mono[OF R Q] qrstep_mono[OF Rw Q]])
lemma SN_rel_ichain:
assumes SN: "SN_rel (qrstep nfs Q (P ∪ R)) (qrstep nfs Q (Pw ∪ Rw))" (is "SN_rel ?PR ?PRw")
shows "¬ ichain (nfs,m,P,Pw,Q,R,Rw) s t σ"
proof
assume chain: "ichain (nfs,m,P,Pw,Q,R,Rw) s t σ"
let ?NS = "?PR ∪ ?PRw"
obtain NS where NS: "?NS = NS" by auto
let ?S = "?NS⇧* O ?PR O ?NS⇧*"
from SN_imp_SN_trancl[OF SN[unfolded SN_rel_on_def], unfolded relto_trancl_conv]
have SN: "SN ?S" .
let ?s = "λ i. s i ⋅ σ i"
let ?t = "λ i. t i ⋅ σ i"
let ?st = "λ i. (?s i,?t i)"
let ?ss = "λ i. ?s (Suc i)"
from chain have "⋀ i. ?s i ∈ NF_terms Q" by auto
from NF_imp_subt_NF[OF this] have NF: "⋀ i. ∀ u ⊲ ?s i. u ∈ NF_terms Q" .
from chain have nfs: "⋀ i. NF_subst nfs (s i, t i) (σ i) Q" by auto
{
fix i
assume P: "(s i,t i) ∈ P"
then have st: "(s i, t i) ∈ P ∪ R" by auto
have "?st i ∈ ?PR" unfolding qrstep_rule_conv[where R = "P ∪ R"]
by (rule bexI[OF _ st], rule qrstepI[of "s i" "σ i" _ "t i" _ _ Hole], insert NF[of i] nfs[of i], auto)
} note P = this
{
fix i
from chain have st: "(s i, t i) ∈ (P ∪ R) ∪ (Pw ∪ Rw)" by auto
have "?st i ∈ ?NS" unfolding qrstep_union[symmetric] qrstep_rule_conv[where R = "P ∪ R ∪ (Pw ∪ Rw)"]
by (rule bexI[OF _ st], rule qrstepI[of "s i" "σ i" _ "t i" _ _ Hole], insert NF[of i] nfs[of i], auto)
} note Pw = this
note subset = rtrancl_mono[OF qrstep_mono[of "R ∪ Rw" "P ∪ R ∪ (Pw ∪ Rw)" Q Q]]
{
fix i
from chain have "(?t i, ?ss i) ∈ (qrstep nfs Q (R ∪ Rw))⇧*" by auto
then have "(?t i, ?ss i) ∈ ?NS⇧*" unfolding qrstep_union[symmetric] using subset by auto
with Pw[of i] have "(?t i, ?ss i) ∈ ?NS⇧*" and "(?s i, ?ss i) ∈ ?NS⇧*" unfolding NS by auto
} note steps = this
then have asteps: "∀ i. (?s i, ?ss i) ∈ ?NS⇧* ∪ ?S" by auto
from SN have SN: "SN_on ?S {?s 0}" unfolding SN_on_def by auto
have compat: "?NS⇧* O ?S ⊆ ?S" unfolding qrstep_union by regexp
from non_strict_ending[OF asteps, OF compat SN]
obtain i where i: "⋀ j. i ≤ j ⟹ (?s j, ?ss j) ∉ ?S" by auto
let ?QNS = "qrstep nfs Q (R ∪ Rw)"
let ?QS = "?QNS⇧* O qrstep nfs Q R O ?QNS⇧*"
from chain have inf: "(INFM i. (s i, t i) ∈ P) ∨ (INFM i. (?t i, ?ss i) ∈ ?QS)" by auto
from this[unfolded INFM_disj_distrib[symmetric],unfolded INFM_nat, THEN spec[of _ i]]
obtain j where j: "j > i" and S: "(s j, t j) ∈ P ∨ (?t j, ?ss j) ∈ ?QS" by auto
from j have j: "j ≥ i" by auto
from S show False
proof
assume "(s j, t j) ∈ P"
from P[OF this] steps[of j] have S: "(?s j, ?ss j) ∈ qrstep nfs Q (P ∪ R) O ?NS⇧*" by auto
have "qrstep nfs Q (P ∪ R) O ?NS⇧* ⊆ ?S" unfolding NS by regexp
with S have "(?s j, ?ss j) ∈ ?S" by auto
with i[OF j] show False unfolding NS ..
next
assume "(?t j, ?ss j) ∈ ?QS"
then obtain u v where tu: "(?t j, u) ∈ ?QNS⇧*" and uv: "(u,v) ∈ qrstep nfs Q R" and vs: "(v,?ss j) ∈ ?QNS⇧*" by auto
from Pw[of j] have one: "(?s j, ?t j) ∈ ?NS" by auto
from tu vs subset have two: "(?t j, u) ∈ ?NS⇧*" and four: "(v, ?ss j) ∈ ?NS⇧*" unfolding qrstep_union by auto
from qrstep_mono[of R "P ∪ R" Q Q] uv have three: "(u,v) ∈ qrstep nfs Q (P ∪ R)" by auto
from one two three four have step: "(?s j, ?ss j) ∈ ?NS O ?NS⇧* O qrstep nfs Q (P ∪ R) O ?NS⇧*" (is "_ ∈ ?rel") unfolding NS by auto
have "?rel ⊆ ?S" unfolding NS by regexp
from set_mp[OF this step] i[OF j]
show False by simp
qed
qed
declare ichain.simps[simp del]
lemma min_ichain_split: assumes chain: "min_ichain (nfs,m,P,Pw,Q,R,Rw) s t σ"
and nchain: "¬ min_ichain (nfs,m,Ps ∩ (P ∪ Pw), P ∪ Pw - Ps, Q, Rs ∩ (R ∪ Rw), R ∪ Rw - Rs) s t σ"
shows "∃ i. min_ichain (nfs,m,P - Ps, Pw - Ps, Q, R - Rs, Rw - Rs) (shift s i) (shift t i) (shift σ i)"
proof -
have Rw: "R ∪ Rw = (Rs ∩ (R ∪ Rw)) ∪ (R ∪ Rw - Rs)" by auto
have nchain: "¬ ichain (nfs,m,Ps ∩ (P ∪ Pw), P ∪ Pw - Ps, Q, Rs ∩ (R ∪ Rw), R ∪ Rw - Rs) s t σ"
proof
assume ichain: "ichain (nfs,m,Ps ∩ (P ∪ Pw), P ∪ Pw - Ps, Q, Rs ∩ (R ∪ Rw), R ∪ Rw - Rs) s t σ"
then have "min_ichain (nfs,m,Ps ∩ (P ∪ Pw), P ∪ Pw - Ps, Q, Rs ∩ (R ∪ Rw), R ∪ Rw - Rs) s t σ"
using chain
by (simp add: Rw[symmetric])
with nchain show False ..
qed
from chain have ichain: "ichain (nfs,m,P,Pw,Q,R,Rw) s t σ" by auto
from ichain_split[OF ichain nchain] obtain i
where ichain: "ichain (nfs,m,P - Ps, Pw - Ps, Q, R - Rs, Rw - Rs) (shift s i) (shift t i) (shift σ i)" ..
have "min_ichain (nfs,m,P - Ps, Pw - Ps, Q, R - Rs, Rw - Rs) (shift s i) (shift t i) (shift σ i)"
by (rule min_ichainI[OF _ _ ichain, of R Rw], insert chain, auto)
then show ?thesis ..
qed
lemma min_ichain_split_sig: assumes chain: "min_ichain_sig (nfs,m,P,Pw,Q,R,Rw) F s t σ"
and nchain: "¬ min_ichain_sig (nfs,m,Ps ∩ (P ∪ Pw), P ∪ Pw - Ps, Q, Rs ∩ (R ∪ Rw), R ∪ Rw - Rs) F s t σ"
shows "∃ i. min_ichain_sig (nfs,m,P - Ps, Pw - Ps, Q, R - Rs, Rw - Rs) F (shift s i) (shift t i) (shift σ i)"
proof -
from chain have chain: "min_ichain (nfs,m,P,Pw,Q,R,Rw) s t σ" and sig: "funas_ichain s t σ ⊆ F" by auto
from nchain sig have "¬ min_ichain (nfs,m,Ps ∩ (P ∪ Pw), P ∪ Pw - Ps, Q, Rs ∩ (R ∪ Rw), R ∪ Rw - Rs) s t σ" by auto
from min_ichain_split[OF chain this] funas_ichain_shift[of s _ t σ] sig show ?thesis by auto
qed
lemma min_ichain_split_P: assumes chain: "min_ichain (nfs,m,P,Pw,Q,R,Rw) s t σ"
and nchain: "¬ min_ichain (nfs,m,Ps ∩ (P ∪ Pw), P ∪ Pw - Ps, Q, {}, R ∪ Rw) s t σ"
shows "∃ i. min_ichain (nfs,m,P - Ps, Pw - Ps, Q, R, Rw) (shift s i) (shift t i) (shift σ i)"
using min_ichain_split[OF chain, of Ps "{}"] nchain by auto
lemma min_ichain_mono_plain: assumes chain: "min_ichain (nfs,m,P,Pw,Q,R,Rw) s t σ"
and P: "P ⊆ P'"
and Pw: "P ∪ Pw ⊆ P' ∪ Pw'"
and Q: "NF_terms Q ⊆ NF_terms Q'"
and R: "qrstep nfs Q R ⊆ qrstep nfs Q' R'"
and Rw: "qrstep nfs Q (R ∪ Rw) = qrstep nfs Q' (R' ∪ Rw')"
shows "min_ichain (nfs,m,P',Pw',Q',R',Rw') s t σ"
proof -
from chain have ichain: "ichain (nfs,m,P,Pw,Q,R,Rw) s t σ"
by simp
have "ichain (nfs,m,P',Pw',Q',R',Rw') s t σ"
by (rule ichain_mono_plain[OF ichain P Pw Q R], insert Rw, auto)
with chain Rw show ?thesis by (auto simp: minimal_cond_def)
qed
lemma min_ichain_mono: assumes chain: "min_ichain (nfs,m,P,Pw,Q,R,Rw) s t σ"
and P: "P ⊆ P'"
and Pw: "P ∪ Pw ⊆ P' ∪ Pw'"
and Q: "NF_terms Q = NF_terms Q'"
and R: "R ⊆ R'"
and Rw: "R ∪ Rw = R' ∪ Rw'"
shows "min_ichain (nfs,m,P',Pw',Q',R',Rw') s t σ"
proof -
from Q have Q': "NF_terms Q ⊆ NF_terms Q'" and Q'': "NF_terms Q' ⊆ NF_terms Q" by auto
show ?thesis
by (rule min_ichain_mono_plain[OF chain P Pw Q' qrstep_mono[OF R Q']], unfold Rw,
insert qrstep_mono[OF subset_refl Q', of _ "R' ∪ Rw'"] qrstep_mono[OF subset_refl Q'', of nfs "R' ∪ Rw'"], auto)
qed
lemma Infm_double_shift: "(INFM i. P (shift f n i) (shift g n i)) =
(INFM i. P (f i) (g i))" using Infm_shift[of "λ (fi,gi). P fi gi" "λ i. (f i, g i)" n]
unfolding split shift.simps .
lemma Infm_triple_shift: "(INFM i. P (shift f n (Suc i)) (shift h n (Suc i)) (shift g n i) (shift h n i)) =
(INFM i. P (f (Suc i)) (h (Suc i)) (g i) (h i))"
using Infm_shift[of "λ (fsi,hsi,gi,hi). P fsi hsi gi hi" "λ i. (f (Suc i), h (Suc i), g i, h i)" n]
unfolding split shift.simps by simp
lemma ichain_shift_merge: assumes ic: "ichain (nfs,m,Pb,{},Q,R,Rw) (shift s i) (shift t i) (shift σ i)"
and mc: "min_ichain (nfs,m,P,Pw,Q,R,Rw) s t σ"
shows "min_ichain (nfs,m,P ∩ Pb, Pw ∩ Pb, Q,R,Rw) (shift s i) (shift t i) (shift σ i)"
using assms unfolding min_ichain.simps ichain.simps
unfolding Infm_double_shift[of "λ s t. (s,t) ∈ P" s i t for P, symmetric]
unfolding Infm_triple_shift[of "λ s σ t τ. (t ⋅ τ, s ⋅ σ) ∈ P" s i σ t for P, symmetric]
by (auto simp: minimal_cond_def)
definition finite_dpp :: "('f,'v)dpp ⇒ bool" where "finite_dpp DPP = (¬(∃s t σ. min_ichain DPP s t σ))"
lemma finite_dpp_split:
assumes fin1: "finite_dpp (nfs,m,Ps ∩ (P ∪ Pw), P ∪ Pw - Ps, Q, Rs ∩ (R ∪ Rw), R ∪ Rw - Rs)" (is "finite_dpp ?D1")
and fin2: "finite_dpp (nfs,m,P - Ps, Pw - Ps, Q, R - Rs, Rw - Rs)" (is "finite_dpp ?D2")
shows "finite_dpp (nfs,m,P,Pw,Q,R,Rw)" (is "finite_dpp ?D")
unfolding finite_dpp_def
proof
assume "∃ s t σ. min_ichain ?D s t σ"
then obtain s t σ where min: "min_ichain ?D s t σ" by blast
from fin1[unfolded finite_dpp_def] have "¬ min_ichain ?D1 s t σ" by blast
from min_ichain_split[OF min this]
show False using fin2[unfolded finite_dpp_def] by blast
qed
lemma finite_dpp_mono_plain: assumes finite: "finite_dpp (nfs,m,P',Pw',Q,R',Rw')"
and P: "rqrstep nfs Q P ⊆ rqrstep nfs Q P'"
and Pw: "rqrstep nfs Q (P ∪ Pw) ⊆ rqrstep nfs Q (P' ∪ Pw')"
and R: "qrstep nfs Q R ⊆ qrstep nfs Q R'"
and Rw: "qrstep nfs Q (R ∪ Rw) = qrstep nfs Q (R' ∪ Rw')"
shows "finite_dpp (nfs,m,P,Pw,Q,R,Rw)"
unfolding finite_dpp_def
proof (clarify)
fix s t σ
assume mi: "min_ichain (nfs,m,P, Pw, Q, R, Rw) s t σ"
then have "ichain (nfs,m,P, Pw, Q, R, Rw) s t σ"
by simp
then obtain f n
where main: " (∀i. (s i, t i) ∈ P ∪ Pw) ∧
(∀i. f i 0 = t i ⋅ σ i ∧
f i (n i) = s (Suc i) ⋅ σ (Suc i) ∧
(∀j<n i. (f i j, f i (Suc j)) ∈ qrstep nfs Q (R ∪ Rw)))"
and NF: "⋀ i. s i ⋅ σ i ∈ NF_terms Q"
and nfs: "⋀ i. NF_subst nfs (s i, t i) (σ i) Q"
and inf: "((INFM i. (s i, t i) ∈ P) ∨ (INFM i. ∃j<n i. (f i j, f i (Suc j)) ∈ qrstep nfs Q R))"
unfolding ichain_alternative by blast
let ?prop = "λ i s' t' σ'. (s i ⋅ σ i, t i ⋅ σ i) = (s' ⋅ σ', t' ⋅ σ') ∧ NF_subst nfs (s',t') σ' Q ∧ (s', t') ∈ P' ∪ Pw' ∧ ((s i, t i) ∈ P ⟶ (s', t') ∈ P')"
{
fix i
from main have "(s i,t i) ∈ P ∪ Pw" by auto
from rqrstepI[OF NF_imp_subt_NF[OF NF] this refl refl nfs]
have "(s i ⋅ σ i, t i ⋅ σ i) ∈ rqrstep nfs Q (P ∪ Pw)" by auto
with Pw have "(s i ⋅ σ i, t i ⋅ σ i) ∈ rqrstep nfs Q (P' ∪ Pw')" by auto
note one = this[unfolded rqrstep_def]
{
assume "(s i, t i) ∈ P"
from rqrstepI[OF NF_imp_subt_NF[OF NF] this refl refl nfs]
have "(s i ⋅ σ i, t i ⋅ σ i) ∈ rqrstep nfs Q P" by auto
with P have "(s i ⋅ σ i, t i ⋅ σ i) ∈ rqrstep nfs Q P'" by auto
note one = this[unfolded rqrstep_def]
}
with one have "∃ s' t' σ'. ?prop i s' t' σ'" by blast
}
from choice[OF allI[OF this]] obtain s' where "∀ i. (∃ t' σ'. ?prop i (s' i) t' σ')" ..
from choice[OF this] obtain t' where "∀ i. (∃ σ'. ?prop i (s' i) (t' i) σ')" ..
from choice[OF this] obtain σ' where switch: "⋀ i. ?prop i (s' i) (t' i) (σ' i)" by blast
from switch have si: "⋀ i. s i ⋅ σ i = s' i ⋅ σ' i" by auto
from switch have ti: "⋀ i. t i ⋅ σ i = t' i ⋅ σ' i" by auto
from switch have Pw: "∀ i. (s' i, t' i) ∈ P' ∪ Pw'" by auto
from switch have P: "⋀ i. (s i, t i) ∈ P ⟹ (s' i, t' i) ∈ P'" by auto
from switch have nfs: "⋀ i. NF_subst nfs (s' i, t' i) (σ' i) Q" by blast
note main = main[unfolded si ti Rw]
note NF = NF[unfolded si ti]
from inf P R have inf: "(INFM i. (s' i, t' i) ∈ P') ∨ (INFM i. ∃ j < n i. (f i j, f i (Suc j)) ∈ qrstep nfs Q R')" unfolding INFM_nat by blast
have ic: "ichain (nfs,m,P',Pw',Q,R',Rw') s' t' σ'"
unfolding ichain_alternative
by (rule exI[of _ f], rule exI[of _ n], insert Pw main NF nfs inf, auto)
with mi have "min_ichain (nfs,m,P',Pw',Q,R',Rw') s' t' σ'"
by (simp add: minimal_cond_def ti Rw)
with finite show False unfolding finite_dpp_def by auto
qed
lemma finite_dpp_mono:
assumes finite: "finite_dpp (nfs, m, P', Pw', Q, R', Rw')"
and P: "P ⊆ P'"
and Pw: "P ∪ Pw ⊆ P' ∪ Pw'"
and Q: "NF_terms Q = NF_terms Q'"
and R: "R ⊆ R'"
and Rw: "R ∪ Rw = R' ∪ Rw'"
shows "finite_dpp (nfs, m, P, Pw, Q', R, Rw)"
using min_ichain_mono[OF _ P Pw Q[symmetric] R Rw] finite
unfolding finite_dpp_def by blast
lemma SN_rel_ext_imp_finite_dpp:
assumes "SN_rel_ext
(rqrstep nfs Q P ∩ {(s,t) . s ∈ NF_terms Q})
(rqrstep nfs Q Pw ∩ {(s,t) . s ∈ NF_terms Q})
(qrstep nfs Q R)
(qrstep nfs Q Rw)
(λx. m ⟶ SN_on (qrstep nfs Q (R ∪ Rw)) {x})" (is "SN_rel_ext ?P ?Pw ?R ?Rw ?M")
shows "finite_dpp (nfs,m,P,Pw,Q,R,Rw)" (is "finite_dpp ?dpp")
unfolding finite_dpp_def
proof (clarify)
fix s t σ
assume chain: "min_ichain (nfs,m,P,Pw,Q,R,Rw) s t σ"
then have "ichain ?dpp s t σ" by auto
from this[unfolded ichain_alternative]
obtain f n where PPw: "⋀ i. (s i, t i) ∈ P ∪ Pw"
and t: "⋀ i. f i 0 = t i ⋅ σ i"
and s: "⋀ i. f i (n i) = s (Suc i) ⋅ σ (Suc i)"
and RRw: "⋀ i. (∀ j < n i. (f i j, f i (Suc j)) ∈ qrstep nfs Q (R ∪ Rw))"
and NF: "⋀ i. s i ⋅ σ i ∈ NF_terms Q"
and nfs: "⋀ i. NF_subst nfs (s i, t i) (σ i) Q"
and inf: "(INFM i. (s i, t i ) ∈ P) ∨ (INFM i. ∃ j < n i. (f i j, f i (Suc j)) ∈ qrstep nfs Q R)" (is "?one ∨ ?two") by blast
note NF_arg = NF_imp_subt_NF[OF NF]
from chain have min: "⋀ i. m ⟹ SN_on (qrstep nfs Q (R ∪ Rw)) {t i ⋅ σ i}" by (auto simp: minimal_cond_def)
let ?m = m
obtain m where m: "⋀ i. m i = Suc (n i)" by auto
let ?c = "inf_concat_simple m"
let ?g = "λ k. case ?c k of (i,j) ⇒ f i j"
let ?t = "λ i j. if (j = n i) then (if (s (Suc i), t (Suc i)) ∈ P then top_s else top_ns) else (if (f i j, f i (Suc j)) ∈ qrstep nfs Q R then normal_s else normal_ns)"
let ?ty = "λ k. case ?c k of (i,j) ⇒ ?t i j"
{
fix k i j
assume ck: "?c k = (i,j)"
then have "j < m i"
proof (cases k)
case 0
with ck show ?thesis unfolding m by auto
next
case (Suc k')
obtain i' j' where ck': "?c k' = (i',j')" by (cases "?c k'", auto)
from ck[unfolded Suc] ck' show ?thesis
by (cases "Suc j' < m i'", auto simp: m)
qed
} note ck_mi = this
let ?rel = "SN_rel_ext_step ?P ?Pw ?R ?Rw"
note rqrstep = rqrstepI[OF NF_arg _ refl refl nfs]
have "¬ SN_rel_ext ?P ?Pw ?R ?Rw ?M"
unfolding
SN_rel_ext_def
simp_thms
proof (rule exI[of _ ?g], rule exI[of _ ?ty], intro conjI allI)
fix k
obtain i j where ck: "?c k = (i,j)" by (cases "?c k", auto)
show "(?g k, ?g (Suc k)) ∈ ?rel (?ty k)"
proof (cases "Suc j < m i")
case False
from ck_mi[OF ck] False have j: "j = n i" unfolding m by auto
from False ck have csk: "?c (Suc k) = (Suc i, 0)" by auto
show ?thesis unfolding ck csk split t j s
by (cases "(s (Suc i), t (Suc i)) ∈ P", insert PPw[of "Suc i"] rqrstep, auto simp: NF)
next
case True
then have j: "(j = n i) = False" and jn: "j < n i" unfolding m by auto
from True ck have csk: "?c (Suc k) = (i, Suc j)" by auto
show ?thesis unfolding ck csk split j using RRw[THEN spec, THEN mp[OF _ jn]]
by (auto simp: qrstep_union)
qed
next
fix k
obtain i j where ck: "?c k = (i,j)" by (cases "?c k", auto)
from ck_mi[OF ck] have j: "j ≤ n i" unfolding m by simp
show "?M (?g k)" unfolding ck split
using j
proof (induct j)
case 0
show ?case unfolding t using min[of i] by simp
next
case (Suc j)
then have j: "j < n i" and SN: "?m ⟹ SN_on (qrstep nfs Q (R ∪ Rw)) {f i j}" by auto
from step_preserves_SN_on[OF RRw[THEN spec, THEN mp[OF _ j]] SN]
show ?case by auto
qed
next
show "INFM k. ?ty k ∈ {top_s,top_ns}"
unfolding INFM_nat_le
proof (intro allI)
fix k :: nat
obtain i j where ck: "?c k = (i,j)" by (cases "?c k", auto)
let ?a = "m i - Suc j"
let ?j = "j + ?a"
from ck_mi[OF ck] have j: "j < m i" by auto
then have "?j < m i" by auto
from inf_concat_simple_add[OF ck, OF this] have "?c (k + ?a) = (i,?j)" .
also have "... = (i,n i)" using j unfolding m by auto
finally have c: "?c (k + ?a) = (i, n i)" by auto
show "∃ k' ≥ k. ?ty k' ∈ {top_s,top_ns}"
by (rule exI[of _ "k + ?a"], unfold c, auto)
qed
next
show "INFM k. ?ty k ∈ {top_s,normal_s}"
unfolding INFM_nat_le
proof (intro allI)
fix k
obtain i j where ck: "?c k = (i,j)" by (cases "?c k", auto)
from inf
show "∃ k' ≥ k. ?ty k' ∈ {top_s,normal_s}"
proof
assume ?one
then obtain i' where i': "i' > Suc i" and P: "(s i', t i') ∈ P"
unfolding INFM_nat by auto
then obtain i' where i': "i' > i" and P: "(s (Suc i'), t (Suc i')) ∈ P" by (cases i', auto)
have "n i' < m i'" unfolding m by auto
from inf_concat_simple_surj[where f = m, OF this]
obtain k' where ck': "?c k' = (i',n i')" by auto
{
assume "k' ≤ k"
from inf_concat_simple_mono[OF this, of m] i' have False unfolding ck ck' by simp
}
then have k': "k' ≥ k" by presburger
show ?thesis
by (rule exI[of _ k'], unfold ck', auto simp: P k')
next
assume ?two
then obtain i' j' where i': "i' > Suc i" and j': "j' < n i'" and R: "(f i' j', f i' (Suc j')) ∈ qrstep nfs Q R"
unfolding INFM_nat by blast
from j' have jm: "j' < m i'" and jn: "(j' = n i') = False" unfolding m by auto
from inf_concat_simple_surj[where f = m, OF jm]
obtain k' where ck': "?c k' = (i',j')" by auto
{
assume "k' ≤ k"
from inf_concat_simple_mono[OF this, of m] i' have False unfolding ck ck' by simp
}
then have k': "k' ≥ k" by presburger
show ?thesis
by (rule exI[of _ k'], unfold ck' jn split, auto simp: R k')
qed
qed
qed
with assms
show False by simp
qed
lemma finite_dpp_imp_SN_rel_ext:
assumes "finite_dpp (nfs,m,P,Pw,Q,R,Rw)" (is "finite_dpp ?dpp")
shows "SN_rel_ext
(rqrstep nfs Q P ∩ {(s,t) . s ∈ NF_terms Q})
(rqrstep nfs Q Pw ∩ {(s,t) . s ∈ NF_terms Q})
(qrstep nfs Q R)
(qrstep nfs Q Rw)
(λx. m ⟶ SN_on (qrstep nfs Q (R ∪ Rw)) {x})" (is "SN_rel_ext ?P ?Pw ?R ?Rw ?M")
proof (rule ccontr)
let ?rel = "SN_rel_ext_step ?P ?Pw ?R ?Rw"
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 ∪ Pw ∧ ?g i = s ⋅ σ ∧ ?h i = t ⋅ σ ∧ s ⋅ σ ∈ NF_terms Q ∧ NF_subst nfs (s,t) σ Q ∧ (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 ∪ ?Pw" 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
from two[OF True] have "(?g i, ?h i) ∈ rqrstep nfs Q P" by simp
from rqrstepE[OF this] two[OF True]
obtain s t σ where "(s,t) ∈ P" "?g i = s ⋅ σ" "?h i = t ⋅ σ" "s ⋅ σ ∈ NF_terms Q"
and "NF_subst nfs (s,t) σ Q" by auto
then show ?thesis by blast
next
case False
from one have "(?g i, ?h i) ∈ rqrstep nfs Q (P ∪ Pw)"
unfolding rqrstep_def
by auto
from rqrstepE[OF this] one
obtain s t σ where "(s,t) ∈ P ∪ Pw" "?g i = s ⋅ σ" "?h i = t ⋅ σ" "s ⋅ σ ∈ NF_terms Q"
"NF_subst nfs (s,t) σ Q" by force
then show ?thesis using False by blast
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 PPw: "⋀ i. (s i, t i) ∈ P ∪ Pw" by auto
from stσ have NF: "⋀ i. (s i ⋅ σ i) ∈ NF_terms 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 ?RRw = "qrstep nfs Q (R ∪ Rw)"
have "ichain ?dpp s t σ"
unfolding ichain_alternative
proof (rule exI[of _ ?f], rule exI[of _ ?n], intro conjI allI impI, rule PPw)
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
show "s i ⋅ σ i ∈ NF_terms Q" by (rule NF)
next
fix i j
let ?k = "Suc (?ind i) + j"
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 apply (cases "ty ?k", auto)
using SN_rel_ext_type.exhaust apply blast
using SN_rel_ext_type.exhaust apply blast
using SN_rel_ext_type.exhaust apply blast
using SN_rel_ext_type.exhaust by blast
with steps[of ?k] show "(?f i j, ?f i (Suc j)) ∈ ?RRw" 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)) ∈ ?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, unfolded p]
ty[unfolded 0] have "ty (?ind j) = top_s" using index_p p by force
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
next
fix i
show "NF_subst nfs (s i, t i) (σ i) Q"
using stσ[of i] by simp
qed
then have "min_ichain ?dpp s t σ"
unfolding min_ichain.simps minimal_cond_def using min by auto
with assms show False
unfolding finite_dpp_def by auto
qed
lemma finite_dpp_map:
fixes P Pw R Rw P' Pw' R' Rw' :: "('f,'v)trs" and Q Q' :: "('f,'v)terms" and nfs nfs' m m'
defines QR: "QR ≡ qrstep nfs Q R"
defines QRw: "QRw ≡ qrstep nfs Q Rw"
defines QP: "QP ≡ rqrstep nfs Q P ∩ {(s,t). s ∈ NF_terms Q}"
defines QPw: "QPw ≡ rqrstep nfs Q Pw ∩ {(s,t). s ∈ NF_terms Q}"
defines QR': "QR' ≡ qrstep nfs' Q' R'"
defines QRw': "QRw' ≡ qrstep nfs' Q' Rw'"
defines QP': "QP' ≡ rqrstep nfs' Q' P' ∩ {(s,t). s ∈ NF_terms Q'}"
defines QPw': "QPw' ≡ rqrstep nfs' Q' Pw' ∩ {(s,t). s ∈ NF_terms Q'}"
defines M: "M ≡ λx. m ⟶ SN_on (qrstep nfs Q (R ∪ Rw)) {x}"
defines M': "M' ≡ λx. m' ⟶ SN_on (qrstep nfs' Q' (R' ∪ Rw')) {x}"
defines Ms': "Ms' ≡ {(s,t). M' t}"
defines A: "A ≡ (QP' ∪ QPw' ∪ QR' ∪ QRw') ∩ Ms'"
assumes SN: "finite_dpp (nfs',m',P',Pw',Q',R',Rw')"
and P: "⋀ s t. M s ⟹ M t ⟹ (s,t) ∈ QP ⟹ (f s, f t) ∈ (A⇧* O (QP' ∩ Ms') O A⇧*) ∧ I t"
and Pw: "⋀ s t. M s ⟹ M t ⟹ (s,t) ∈ QPw ⟹ (f s, f t) ∈ (A⇧* O ((QP' ∪ QPw') ∩ Ms') O A⇧*) ∧ I t"
and R: "⋀ s t. I s ⟹ M s ⟹ M t ⟹ (s,t) ∈ QR ⟹ (f s, f t) ∈ (A⇧* O ((QP' ∪ QR') ∩ Ms') O A⇧*) ∧ I t"
and Rw: "⋀ s t. I s ⟹ M s ⟹ M t ⟹ (s,t) ∈ QRw ⟹ (f s, f t) ∈ A⇧* ∧ I t"
shows "finite_dpp (nfs,m,P,Pw,Q,R,Rw)"
proof -
from finite_dpp_imp_SN_rel_ext[OF SN]
have SN: "SN_rel_ext QP' QPw' QR' QRw' M'"
unfolding QP' QPw' QR' QRw' M' .
have SN: "SN_rel_ext QP QPw QR QRw M"
by (rule SN_rel_ext_map[OF SN, unfolded Ms'[symmetric] A[symmetric], OF P Pw R Rw], auto)
show ?thesis
by (rule SN_rel_ext_imp_finite_dpp[OF SN[unfolded QP QPw QR QRw M]])
qed
lemma finite_dpp_map_min:
fixes P Pw R Rw P' Pw' R' Rw' :: "('f,'v)trs" and Q Q' :: "('f,'v)terms" and m m' nfs nfs'
defines QR: "QR ≡ qrstep nfs Q R"
defines QRw: "QRw ≡ qrstep nfs Q Rw"
defines QP: "QP ≡ rqrstep nfs Q P ∩ {(s,t). s ∈ NF_terms Q}"
defines QPw: "QPw ≡ rqrstep nfs Q Pw ∩ {(s,t). s ∈ NF_terms Q}"
defines QR': "QR' ≡ qrstep nfs' Q' R'"
defines QRw': "QRw' ≡ qrstep nfs' Q' Rw'"
defines QP': "QP' ≡ rqrstep nfs' Q' P' ∩ {(s,t). s ∈ NF_terms Q'}"
defines QPw': "QPw' ≡ rqrstep nfs' Q' Pw' ∩ {(s,t). s ∈ NF_terms Q'}"
defines M: "M ≡ λx. m ⟶ SN_on (qrstep nfs Q (R ∪ Rw)) {x}"
defines M': "M' ≡ λx. m' ⟶ SN_on (qrstep nfs' Q' (R' ∪ Rw')) {x}"
defines Ms': "Ms' ≡ {(s,t). M' t}"
defines A: "A ≡ QP' ∩ Ms' ∪ QPw' ∩ Ms' ∪ QR' ∪ QRw'"
assumes SN: "finite_dpp (nfs',m',P',Pw',Q',R',Rw')"
and MM': "⋀ t. M t ⟹ M' (f t)"
and P: "⋀ s t. M s ⟹ M t ⟹ M' (f s) ⟹ M' (f t) ⟹ (s,t) ∈ QP ⟹ (f s, f t) ∈ (A⇧* O (QP' ∩ Ms') O A⇧*) ∧ I t"
and Pw: "⋀ s t. M s ⟹ M t ⟹ M' (f s) ⟹ M' (f t) ⟹ (s,t) ∈ QPw ⟹ (f s, f t) ∈ (A⇧* O (QP' ∩ Ms' ∪ QPw' ∩ Ms') O A⇧*) ∧ I t"
and R: "⋀ s t. I s ⟹ M s ⟹ M t ⟹ M' (f s) ⟹ M' (f t) ⟹ (s,t) ∈ QR ⟹ (f s, f t) ∈ (A⇧* O (QP' ∩ Ms' ∪ QR') O A⇧*) ∧ I t"
and Rw: "⋀ s t. I s ⟹ M s ⟹ M t ⟹ M' (f s) ⟹ M' (f t) ⟹ (s,t) ∈ QRw ⟹ (f s, f t) ∈ A⇧* ∧ I t"
shows "finite_dpp (nfs,m,P,Pw,Q,R,Rw)"
proof -
from finite_dpp_imp_SN_rel_ext[OF SN]
have SN: "SN_rel_ext QP' QPw' QR' QRw' M'"
unfolding QP' QPw' QR' QRw' M' .
{
fix s t
assume a: "M' s" and b: "(s,t) ∈ QR' ∪ QRw'"
from b a have "M' t" unfolding M' QR' QRw' qrstep_union
by (intro impI step_preserves_SN_on[of s t], auto)
} note min = this
have SN: "SN_rel_ext QP QPw QR QRw M"
by (rule SN_rel_ext_map_min[OF SN, unfolded Ms'[symmetric] A[symmetric], OF MM' min P Pw R Rw], auto)
show ?thesis
by (rule SN_rel_ext_imp_finite_dpp[OF SN[unfolded QP QPw QR QRw M]])
qed
theorem finite_dpp_iff_SN_rel:
"finite_dpp (nfs,m,P,{},{},{},R) = SN_rel
((subst.closure P ∩ {(s,t) | s t. m ⟶ SN_on (rstep R) {t}})) (rstep R)" (is "_ = SN_rel ?R ?S")
proof
assume SN: "SN_rel ?R ?S"
show "finite_dpp (nfs,m,P,{},{},{},R)"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain s t σ where chain: "min_ichain (nfs,m,P,{},{},{},R) s t σ" unfolding finite_dpp_def by auto
obtain f where f: "⋀ i. f i = s i ⋅ σ i" by auto
from chain have "⋀ i. (s i ⋅ σ i, t i ⋅ σ i) ∈ ?R" and "⋀ i. (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ ?S⇧*"
by (auto simp: minimal_cond_def ichain.simps)
then have "⋀ i. (f i,f (Suc i)) ∈ ?S⇧* O ?R O ?S⇧*" unfolding f by auto
with SN[unfolded SN_rel_on_def]
show False unfolding SN_defs by blast
qed
next
assume finite: "finite_dpp (nfs,m,P,{},{},{},R)"
show "SN_rel ?R ?S"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain t where steps: "⋀ i. (t i, t (Suc i)) ∈ ?S⇧* O ?R O ?S⇧*"
unfolding SN_rel_defs SN_defs by auto
let ?prop = "λ s u i. (t i, s) ∈ ?S⇧* ∧ (s,u) ∈ ?R ∧ (u, t (Suc i)) ∈ ?S⇧*"
have "∀ i. ∃ s u. ?prop s u i"
proof
fix i
from steps[of i] show "∃ s u. ?prop s u i" by auto
qed
from choice[OF this] obtain s where "∀ i. ∃ u. ?prop (s i) u i" ..
from choice[OF this] obtain u where p: "⋀ i. ?prop (s i) (u i) i" by auto
let ?prop2 = "λ l r σ i. (l, r) ∈ P ∧ (m ⟶ SN_on (rstep R) {r ⋅ σ}) ∧ r ⋅ σ = u i ∧ l ⋅ σ = s i"
have "∀ i. ∃ l r σ. ?prop2 l r σ i"
proof
fix i
from p[of i] have "(s i, u i) ∈ subst.closure P" by auto
then obtain l r σ where "s i = l ⋅ σ ∧ u i = r ⋅ σ ∧ (l,r) ∈ P" by (auto elim: subst.closure.cases)
with p[of i] have "?prop2 l r σ i" by auto
then show "∃ l r σ. ?prop2 l r σ i" by blast
qed
from choice[OF this] obtain l where "∀ i. ∃ r σ . ?prop2 (l i) r σ i" ..
from choice[OF this] obtain r where "∀ i. ∃ σ . ?prop2 (l i) (r i) σ i" ..
from choice[OF this] obtain σ where p2: "⋀ i. ?prop2 (l i) (r i) (σ i) i" by auto
{
fix i
from p2[of i] p[of i] p[of "Suc i"] p2[of "Suc i"]
have "(r i ⋅ σ i, l (Suc i) ⋅ σ (Suc i)) ∈ ?S⇧* " by auto
}
with p2 have "min_ichain (nfs,m,P,{},{},{},R) l r σ"
by (auto simp: minimal_cond_def p2 ichain.simps)
with finite show False unfolding finite_dpp_def by blast
qed
qed
lemma min_ichain_imp_var_cond: assumes "min_ichain (nfs,m,P,Pw,Q,R,Rw) s t σ"
and "lr ∈ R ∪ Rw"
and m: m
and nfs: "¬ nfs"
shows "is_Fun (fst lr)"
proof(rule ccontr)
assume n: "¬ ?thesis"
let ?R = "R ∪ Rw"
obtain l r where lr: "lr = (l,r)" by force
with assms(2) n have "(l,r) ∈ ?R"
and "is_Var (fst (l,r))" by auto
then obtain x where lr: "(Var x,r) ∈ ?R" by (cases l, auto)
from assms(1) m have "SN_on (qrstep nfs Q (R ∪ Rw)) {t 0 ⋅ σ 0}"
by (auto simp: minimal_cond_def)
with left_Var_imp_not_SN_qrstep[OF lr nfs]
show False ..
qed
lemma finite_under_var_cond:
assumes var: "(⋀ lr. lr ∈ R ∪ Rw ⟹ is_Fun (fst lr)) ⟹ finite_dpp (nfs,m,P,Pw,Q,R,Rw)"
and m: m and nfs: "¬ nfs"
shows "finite_dpp (nfs,m,P,Pw,Q,R,Rw)"
proof(rule ccontr)
assume n: "¬ ?thesis"
from n[unfolded finite_dpp_def] obtain s t σ where
chain: "min_ichain (nfs,m,P,Pw,Q,R,Rw) s t σ" by auto
have ?thesis
by (rule var, rule min_ichain_imp_var_cond[OF chain _ m nfs])
with n show False ..
qed
fun
nr_ichain ::
"bool × bool × ('f, 'v)trs × ('f,'v)trs × ('f,'v)terms × ('f,'v)trs ⇒ (nat ⇒ ('f, 'v) term) ⇒ (nat ⇒ ('f, 'v) term) ⇒
(nat ⇒ ('f, 'v) subst) ⇒ bool"
where
"nr_ichain (nfs,m,P, Pw, Q, R) s t σ = (
(∀i. (s i ⋅ σ i) ∈ NF_terms Q) ∧
(∀i. (s i,t i) ∈ P ∪ Pw) ∧
(∀i. NF_subst nfs (s i, t i) (σ i) Q) ∧
(INFM i. (s i,t i) ∈ P) ∧
(∀i. (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ (nrqrstep nfs Q R)⇧*))"
lemma ichain_imp_nr_ichain:
assumes ichain: "ichain (nfs,m,P,Pw,Q,{},R) s t σ"
and nvar: "∀ (l,r) ∈ R. is_Fun l"
and nvarP: "∀ (s,t) ∈ P ∪ Pw. is_Fun t"
and ndef: "∀ (s,t) ∈ P ∪ Pw. ¬ defined R (the (root t))"
shows "nr_ichain (nfs,m,P,Pw,Q,R) s t σ"
proof -
from ichain[unfolded ichain.simps] have
zero: "⋀ i. (s i ⋅ σ i) ∈ NF_terms Q" "⋀ i. NF_subst nfs (s i, t i) (σ i) Q"
and one: "∀i. (s i,t i) ∈ P ∪ Pw"
and two: "(INFM i. (s i, t i) ∈ P)"
and three: "(∀i. (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ (qrstep nfs Q R)⇧*)"
by auto
{
fix i
from three have steps: "(t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ (qrstep nfs Q R)⇧*" by auto
from one nvarP have t: "is_Fun (t i)" by auto
then have nvart: "is_Fun (t i ⋅ σ i)" by auto
from one ndef have "¬ defined R (the (root (t i)))" by auto
with t have "¬ defined R (the (root (t i ⋅ σ i)))" by auto
from qrsteps_imp_nrqrsteps[OF nvar ndef_applicable_rules[OF this] steps]
have "(t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ (nrqrstep nfs Q R)⇧*" .
}
with zero one two show ?thesis by auto
qed
lemma nr_ichain_mono: assumes ichain: "nr_ichain (nfs,m,P,Pw,Q,R) s t σ"
and P: "P ⊆ P'"
and Pw: "P ∪ Pw ⊆ P' ∪ Pw'"
and R: "R ⊆ R'"
shows "nr_ichain (nfs,m,P',Pw',Q,R') s t σ"
proof -
from ichain have
zero: "⋀ i. (s i ⋅ σ i) ∈ NF_terms Q" "⋀ i. NF_subst nfs (s i, t i) (σ i) Q"
and one: "∀i. (s i,t i) ∈ P ∪ Pw"
and two: "(INFM i. (s i, t i) ∈ P)"
and three: "(∀i. (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ (nrqrstep nfs Q R)⇧*)"
by auto
show ?thesis unfolding nr_ichain.simps
proof (intro conjI)
show "∀i. (s i,t i) ∈ P' ∪ Pw'" using one Pw by auto
next
show "(INFM i. (s i, t i) ∈ P')" using two P unfolding INFM_nat_le by auto
next
show "(∀i. (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ (nrqrstep nfs Q R')⇧*)"
using rtrancl_mono[OF nrqrstep_mono[OF subset_refl R]] three by auto
qed (insert zero, auto)
qed
fun
nr_min_ichain ::
"bool × bool × ('f, 'v)trs × ('f,'v)trs × ('f,'v)terms × ('f,'v)trs ⇒ (nat ⇒ ('f, 'v) term) ⇒ (nat ⇒ ('f, 'v) term) ⇒
(nat ⇒ ('f, 'v) subst) ⇒ bool"
where
"nr_min_ichain (nfs,m,P, Pw, Q, R) s t σ = (nr_ichain (nfs,m,P, Pw, Q, R) s t σ ∧ (m ⟶ minimal_cond nfs Q R s t σ))"
lemma min_ichain_imp_nr_min_ichain:
assumes ichain: "min_ichain (nfs,m,P,Pw,Q,{},R) s t σ"
and nvarP: "∀ (s,t) ∈ P ∪ Pw. is_Fun t"
and nvarR: "∀ (s,t) ∈ R. is_Fun s"
and ndef: "∀ (s,t) ∈ P ∪ Pw. ¬ defined R (the (root t))"
shows "nr_min_ichain (nfs,m,P,Pw,Q,R) s t σ"
proof -
from ichain have "ichain (nfs,m,P,Pw,Q,{},R) s t σ" by simp
from ichain_imp_nr_ichain[OF this nvarR nvarP ndef]
have nr: "nr_ichain (nfs,m,P,Pw,Q,R) s t σ" by auto
from nr ichain show ?thesis by simp
qed
lemma nr_min_ichain_mono: assumes ichain: "nr_min_ichain (nfs,m,P,Pw,Q,R) s t σ"
and P: "P ⊆ P'"
and Pw: "P ∪ Pw ⊆ P' ∪ Pw'"
shows "nr_min_ichain (nfs,m,P',Pw',Q,R) s t σ"
proof -
from ichain have nr: "nr_ichain (nfs,m,P,Pw,Q,R) s t σ" and min: "m ⟹ minimal_cond nfs Q R s t σ" by auto
from nr_ichain_mono[OF nr P Pw subset_refl] have ichain': "nr_ichain (nfs,m,P', Pw', Q, R) s t σ" by auto
with min show ?thesis by auto
qed
lemma finite_dpp_rename_vars: assumes fin: "finite_dpp (nfs,m,P',Pw',Q,R,Rw)"
and P: "⋀ st. st ∈ P ⟹ ∃ st'. st' ∈ P' ∧ st =⇩v st'"
and Pw: "⋀ st. st ∈ Pw ⟹ ∃ st'. st' ∈ Pw' ∧ st =⇩v st'"
shows "finite_dpp (nfs,m,P,Pw,Q,R,Rw)"
proof -
have P: "rqrstep nfs Q P ⊆ rqrstep nfs Q P'" by (rule rqrstep_rename_vars[OF P])
have Pw: "rqrstep nfs Q Pw ⊆ rqrstep nfs Q Pw'" by (rule rqrstep_rename_vars[OF Pw])
have "SN_rel_ext (rqrstep nfs Q P ∩ {(s, t). s ∈ NF_terms Q}) (rqrstep nfs Q Pw ∩ {(s, t). s ∈ NF_terms Q})
(qrstep nfs Q R) (qrstep nfs Q Rw) (λx. m ⟶ SN_on (qrstep nfs Q (R ∪ Rw)) {x})"
by (rule SN_rel_ext_mono[OF _ _ _ _ finite_dpp_imp_SN_rel_ext[OF fin]], insert P Pw, auto)
from SN_rel_ext_imp_finite_dpp[OF this] show ?thesis .
qed
subsection ‹Soundness and Chain-Identifyingness of Termination Techniques and DP Processors›
definition
subset_proc :: "(('f, 'v) dpp ⇒ ('f, 'v) dpp ⇒ bool) ⇒ bool"
where
"subset_proc proc ⟷ (∀ nfs m P Pw Q R Rw nfs' m' P' Pw' Q' R' Rw'. proc (nfs,m,P,Pw,Q,R,Rw) (nfs',m',P',Pw',Q',R',Rw') ⟶
(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)))))"
definition
sound_proc :: "(('f, 'v) dpp ⇒ ('f, 'v) dpp ⇒ bool) ⇒ bool"
where
"sound_proc proc ⟷ (∀nfs m P Pw Q R Rw nfs' m' P' Pw' Q' R' Rw'.
proc (nfs, m, P, Pw, Q, R, Rw) (nfs', m', P', Pw', Q', R', Rw') ∧ finite_dpp (nfs',m',P', Pw', Q', R', Rw') ⟶
finite_dpp (nfs,m,P, Pw, Q, R, Rw))"
lemma subset_proc_to_sound_proc:
assumes subset_proc: "subset_proc proc"
shows "sound_proc proc"
unfolding sound_proc_def
proof (intro allI impI, erule conjE)
fix DPP DPP'
assume cond: "proc DPP DPP'" and finite: "finite_dpp DPP'"
obtain nfs m P Pw Q R Rw where dpp: "DPP = (nfs,m,P,Pw,Q,R,Rw)" by (cases DPP, blast)
obtain nfs' m' P' Pw' Q' R' Rw' where dpp': "DPP' = (nfs',m',P',Pw',Q',R',Rw')" by (cases DPP', blast)
show "finite_dpp DPP"
proof (rule ccontr)
assume "¬ finite_dpp DPP"
from this[unfolded dpp] obtain s t σ where min: "min_ichain (nfs,m,P,Pw,Q,R,Rw) s t σ" unfolding finite_dpp_def by auto
from subset_proc[unfolded subset_proc_def, rule_format, OF cond[unfolded dpp dpp']] min
obtain i where subset: "R' ∪ Rw' ⊆ R ∪ Rw" and id: "Q' = Q" "nfs' = nfs" and
m': "m' ⟹ m" and
ichain: "ichain (nfs,m',P',Pw',Q',R',Rw') (shift s i) (shift t i) (shift σ i)" by force
have "min_ichain (nfs,m',P',Pw',Q',R',Rw') (shift s i) (shift t i) (shift σ i)"
by (rule min_ichainI[OF subset _ ichain], insert min id m', auto)
then have "¬ finite_dpp DPP'" unfolding finite_dpp_def dpp' id by blast
with finite show False by auto
qed
qed
lemma sound_proc: assumes "finite_dpp DPP'"
and "proc DPP DPP'"
and "sound_proc proc"
shows "finite_dpp DPP"
using assms unfolding sound_proc_def by (cases DPP, cases DPP') blast
lemma subset_proc:
assumes fin: "finite_dpp DPP'"
and proc: "proc DPP DPP'"
and subset: "subset_proc proc"
shows "finite_dpp DPP"
by (rule sound_proc[OF fin proc subset_proc_to_sound_proc[OF subset]])
end