Theory Relative_Rewriting
section ‹Relative Rewriting›
theory Relative_Rewriting
imports Abstract_Rewriting
begin
text ‹Considering a relation @{term R} relative to another relation @{term S}, i.e.,
@{term R}-steps may be preceded and followed by arbitrary many @{term S}-steps.›
abbreviation (input) relto :: "'a rel ⇒ 'a rel ⇒ 'a rel" where
"relto R S ≡ S^* O R O S^*"
definition SN_rel_on :: "'a rel ⇒ 'a rel ⇒ 'a set ⇒ bool" where
"SN_rel_on R S ≡ SN_on (relto R S)"
definition SN_rel_on_alt :: "'a rel ⇒ 'a rel ⇒ 'a set ⇒ bool" where
"SN_rel_on_alt R S T = (∀f. chain (R ∪ S) f ∧ f 0 ∈ T ⟶ ¬ (INFM j. (f j, f (Suc j)) ∈ R))"
abbreviation SN_rel :: "'a rel ⇒ 'a rel ⇒ bool" where
"SN_rel R S ≡ SN_rel_on R S UNIV"
abbreviation SN_rel_alt :: "'a rel ⇒ 'a rel ⇒ bool" where
"SN_rel_alt R S ≡ SN_rel_on_alt R S UNIV"
lemma relto_absorb [simp]: "relto R E O E⇧* = relto R E" "E⇧* O relto R E = relto R E"
using O_assoc and rtrancl_idemp_self_comp by (metis)+
lemma steps_preserve_SN_on_relto:
assumes steps: "(a, b) ∈ (R ∪ S)^*"
and SN: "SN_on (relto R S) {a}"
shows "SN_on (relto R S) {b}"
proof -
let ?RS = "relto R S"
have "(R ∪ S)^* ⊆ S^* ∪ ?RS^*" by regexp
with steps have "(a,b) ∈ S^* ∨ (a,b) ∈ ?RS^*" by auto
thus ?thesis
proof
assume "(a,b) ∈ ?RS^*"
from steps_preserve_SN_on[OF this SN] show ?thesis .
next
assume Ssteps: "(a,b) ∈ S^*"
show ?thesis
proof
fix f
assume "f 0 ∈ {b}" and "chain ?RS f"
hence f0: "f 0 = b" and steps: "⋀i. (f i, f (Suc i)) ∈ ?RS" by auto
let ?g = "λ i. if i = 0 then a else f i"
have "¬ SN_on ?RS {a}" unfolding SN_on_def not_not
proof (rule exI[of _ ?g], intro conjI allI)
fix i
show "(?g i, ?g (Suc i)) ∈ ?RS"
proof (cases i)
case (Suc j)
show ?thesis using steps[of i] unfolding Suc by simp
next
case 0
from steps[of 0, unfolded f0] Ssteps have steps: "(a,f (Suc 0)) ∈ S^* O ?RS" by blast
have "(a,f (Suc 0)) ∈ ?RS"
by (rule subsetD[OF _ steps], regexp)
thus ?thesis unfolding 0 by simp
qed
qed simp
with SN show False by simp
qed
qed
qed
lemma step_preserves_SN_on_relto: assumes st: "(s,t) ∈ R ∪ E"
and SN: "SN_on (relto R E) {s}"
shows "SN_on (relto R E) {t}"
by (rule steps_preserve_SN_on_relto[OF _ SN], insert st, auto)
lemma SN_rel_on_imp_SN_rel_on_alt: "SN_rel_on R S T ⟹ SN_rel_on_alt R S T"
proof (unfold SN_rel_on_def)
assume SN: "SN_on (relto R S) T"
show ?thesis
proof (unfold SN_rel_on_alt_def, intro allI impI)
fix f
assume steps: "chain (R ∪ S) f ∧ f 0 ∈ T"
with SN have SN: "SN_on (relto R S) {f 0}"
and steps: "⋀ i. (f i, f (Suc i)) ∈ R ∪ S" unfolding SN_defs by auto
obtain r where r: "⋀ j. r j ≡ (f j, f (Suc j)) ∈ R" by auto
show "¬ (INFM j. (f j, f (Suc j)) ∈ R)"
proof (rule ccontr)
assume "¬ ?thesis"
hence ih: "infinitely_many r" unfolding infinitely_many_def r by blast
obtain r_index where "r_index = infinitely_many.index r" by simp
with infinitely_many.index_p[OF ih] infinitely_many.index_ordered[OF ih] infinitely_many.index_not_p_between[OF ih]
have r_index: "⋀ i. r (r_index i) ∧ r_index i < r_index (Suc i) ∧ (∀ j. r_index i < j ∧ j < r_index (Suc i) ⟶ ¬ r j)" by auto
obtain g where g: "⋀ i. g i ≡ f (r_index i)" ..
{
fix i
let ?ri = "r_index i"
let ?rsi = "r_index (Suc i)"
from r_index have isi: "?ri < ?rsi" by auto
obtain ri rsi where ri: "ri = ?ri" and rsi: "rsi = ?rsi" by auto
with r_index[of i] steps have inter: "⋀ j. ri < j ∧ j < rsi ⟹ (f j, f (Suc j)) ∈ S" unfolding r by auto
from ri isi rsi have risi: "ri < rsi" by simp
{
fix n
assume "Suc n ≤ rsi - ri"
hence "(f (Suc ri), f (Suc (n + ri))) ∈ S^*"
proof (induct n, simp)
case (Suc n)
hence stepps: "(f (Suc ri), f (Suc (n+ri))) ∈ S^*" by simp
have "(f (Suc (n+ri)), f (Suc (Suc n + ri))) ∈ S"
using inter[of "Suc n + ri"] Suc(2) by auto
with stepps show ?case by simp
qed
}
from this[of "rsi - ri - 1"] risi have
"(f (Suc ri), f rsi) ∈ S^*" by simp
with ri rsi have ssteps: "(f (Suc ?ri), f ?rsi) ∈ S^*" by simp
with r_index[of i] have "(f ?ri, f ?rsi) ∈ R O S^*" unfolding r by auto
hence "(g i, g (Suc i)) ∈ S^* O R O S^*" using rtrancl_refl unfolding g by auto
}
hence nSN: "¬ SN_on (S^* O R O S^*) {g 0}" unfolding SN_defs by blast
have SN: "SN_on (S^* O R O S^*) {f (r_index 0)}"
proof (rule steps_preserve_SN_on_relto[OF _ SN])
show "(f 0, f (r_index 0)) ∈ (R ∪ S)^*"
unfolding rtrancl_fun_conv
by (rule exI[of _ f], rule exI[of _ "r_index 0"], insert steps, auto)
qed
with nSN show False unfolding g ..
qed
qed
qed
lemma SN_rel_on_alt_imp_SN_rel_on: "SN_rel_on_alt R S T ⟹ SN_rel_on R S T"
proof (unfold SN_rel_on_def)
assume SN: "SN_rel_on_alt R S T"
show "SN_on (relto R S) T"
proof
fix f
assume start: "f 0 ∈ T" and "chain (relto R S) f"
hence steps: "⋀ i. (f i, f (Suc i)) ∈ S^* O R O S^*" by auto
let ?prop = "λ i ai bi. (f i, bi) ∈ S^* ∧ (bi, ai) ∈ R ∧ (ai, f (Suc (i))) ∈ S^*"
{
fix i
from steps obtain bi ai where "?prop i ai bi" by blast
hence "∃ ai bi. ?prop i ai bi" by blast
}
hence "∀ i. ∃ bi ai. ?prop i ai bi" by blast
from choice[OF this] obtain b where "∀ i. ∃ ai. ?prop i ai (b i)" by blast
from choice[OF this] obtain a where steps: "⋀ i. ?prop i (a i) (b i)" by blast
from steps[of 0] have fa0: "(f 0, a 0) ∈ S^* O R" by auto
let ?prop = "λ i li. (b i, a i) ∈ R ∧ (∀ j < length li. ((a i # li) ! j, (a i # li) ! Suc j) ∈ S) ∧ last (a i # li) = b (Suc i)"
{
fix i
from steps[of i] steps[of "Suc i"] have "(a i, f (Suc i)) ∈ S^*" and "(f (Suc i), b (Suc i)) ∈ S^*" by auto
from rtrancl_trans[OF this] steps[of i] have R: "(b i, a i) ∈ R" and S: "(a i, b (Suc i)) ∈ S^*" by blast+
from S[unfolded rtrancl_list_conv] obtain li where "last (a i # li) = b (Suc i) ∧ (∀ j < length li. ((a i # li) ! j, (a i # li) ! Suc j) ∈ S)" ..
with R have "?prop i li" by blast
hence "∃ li. ?prop i li" ..
}
hence "∀ i. ∃ li. ?prop i li" ..
from choice[OF this] obtain l where steps: "⋀ i. ?prop i (l i)" by auto
let ?p = "λ i. ?prop i (l i)"
from steps have steps: "⋀ i. ?p i" by blast
let ?l = "λ i. a i # l i"
let ?l' = "λ i. length (?l i)"
let ?g = "λ i. inf_concat_simple ?l' i"
obtain g where g: "⋀ i. g i = (let (ii,jj) = ?g i in ?l ii ! jj)" by auto
have g0: "g 0 = a 0" unfolding g Let_def by simp
with fa0 have fg0: "(f 0, g 0) ∈ S^* O R" by auto
have fg0: "(f 0, g 0) ∈ (R ∪ S)^*"
by (rule subsetD[OF _ fg0], regexp)
have len: "⋀ i j n. ?g n = (i,j) ⟹ j < length (?l i)"
proof -
fix i j n
assume n: "?g n = (i,j)"
show "j < length (?l i)"
proof (cases n)
case 0
with n have "j = 0" by auto
thus ?thesis by simp
next
case (Suc nn)
obtain ii jj where nn: "?g nn = (ii,jj)" by (cases "?g nn", auto)
show ?thesis
proof (cases "Suc jj < length (?l ii)")
case True
with nn Suc have "?g n = (ii, Suc jj)" by auto
with n True show ?thesis by simp
next
case False
with nn Suc have "?g n = (Suc ii, 0)" by auto
with n show ?thesis by simp
qed
qed
qed
have gsteps: "⋀ i. (g i, g (Suc i)) ∈ R ∪ S"
proof -
fix n
obtain i j where n: "?g n = (i, j)" by (cases "?g n", auto)
show "(g n, g (Suc n)) ∈ R ∪ S"
proof (cases "Suc j < length (?l i)")
case True
with n have "?g (Suc n) = (i, Suc j)" by auto
with n have gn: "g n = ?l i ! j" and gsn: "g (Suc n) = ?l i ! (Suc j)" unfolding g by auto
thus ?thesis using steps[of i] True by auto
next
case False
with n have "?g (Suc n) = (Suc i, 0)" by auto
with n have gn: "g n = ?l i ! j" and gsn: "g (Suc n) = a (Suc i)" unfolding g by auto
from gn len[OF n] False have "j = length (?l i) - 1" by auto
with gn have gn: "g n = last (?l i)" using last_conv_nth[of "?l i"] by auto
from gn gsn show ?thesis using steps[of i] steps[of "Suc i"] by auto
qed
qed
have infR: "INFM j. (g j, g (Suc j)) ∈ R" unfolding INFM_nat_le
proof
fix n
obtain i j where n: "?g n = (i,j)" by (cases "?g n", auto)
from len[OF n] have j: "j < ?l' i" .
let ?k = "?l' i - 1 - j"
obtain k where k: "k = j + ?k" by auto
from j k have k2: "k = ?l' i - 1" and k3: "j + ?k < ?l' i" by auto
from inf_concat_simple_add[OF n, of ?k, OF k3]
have gnk: "?g (n + ?k) = (i, k)" by (simp only: k)
hence "g (n + ?k) = ?l i ! k" unfolding g by auto
hence gnk2: "g (n + ?k) = last (?l i)" using last_conv_nth[of "?l i"] k2 by auto
from k2 gnk have "?g (Suc (n+?k)) = (Suc i, 0)" by auto
hence gnsk2: "g (Suc (n+?k)) = a (Suc i)" unfolding g by auto
from steps[of i] steps[of "Suc i"] have main: "(g (n+?k), g (Suc (n+?k))) ∈ R"
by (simp only: gnk2 gnsk2)
show "∃ j ≥ n. (g j, g (Suc j)) ∈ R"
by (rule exI[of _ "n + ?k"], auto simp: main[simplified])
qed
from fg0[unfolded rtrancl_fun_conv] obtain gg n where start: "gg 0 = f 0"
and n: "gg n = g 0" and steps: "⋀ i. i < n ⟹ (gg i, gg (Suc i)) ∈ R ∪ S" by auto
let ?h = "λ i. if i < n then gg i else g (i - n)"
obtain h where h: "h = ?h" by auto
{
fix i
assume i: "i ≤ n"
have "h i = gg i" using i unfolding h
by (cases "i < n", auto simp: n)
} note gg = this
from gg[of 0] ‹f 0 ∈ T› have h0: "h 0 ∈ T" unfolding start by auto
{
fix i
have "(h i, h (Suc i)) ∈ R ∪ S"
proof (cases "i < n")
case True
from steps[of i] gg[of i] gg[of "Suc i"] True show ?thesis by auto
next
case False
hence "i = n + (i - n)" by auto
then obtain k where i: "i = n + k" by auto
from gsteps[of k] show ?thesis unfolding h i by simp
qed
} note hsteps = this
from SN[unfolded SN_rel_on_alt_def, rule_format, OF conjI[OF allI[OF hsteps] h0]]
have "¬ (INFM j. (h j, h (Suc j)) ∈ R)" .
moreover have "INFM j. (h j, h (Suc j)) ∈ R" unfolding INFM_nat_le
proof (rule)
fix m
from infR[unfolded INFM_nat_le, rule_format, of m]
obtain i where i: "i ≥ m" and g: "(g i, g (Suc i)) ∈ R" by auto
show "∃ n ≥ m. (h n , h (Suc n)) ∈ R"
by (rule exI[of _ "i + n"], unfold h, insert g i, auto)
qed
ultimately show False ..
qed
qed
lemma SN_rel_on_conv: "SN_rel_on = SN_rel_on_alt"
by (intro ext) (blast intro: SN_rel_on_imp_SN_rel_on_alt SN_rel_on_alt_imp_SN_rel_on)
lemmas SN_rel_defs = SN_rel_on_def SN_rel_on_alt_def
lemma SN_rel_on_alt_r_empty : "SN_rel_on_alt {} S T"
unfolding SN_rel_defs by auto
lemma SN_rel_on_alt_s_empty : "SN_rel_on_alt R {} = SN_on R"
by (intro ext, unfold SN_rel_defs SN_defs, auto)
lemma SN_rel_on_mono':
assumes R: "R ⊆ R'" and S: "S ⊆ R' ∪ S'" and SN: "SN_rel_on R' S' T"
shows "SN_rel_on R S T"
proof -
note conv = SN_rel_on_conv SN_rel_on_alt_def INFM_nat_le
show ?thesis unfolding conv
proof(intro allI impI)
fix f
assume "chain (R ∪ S) f ∧ f 0 ∈ T"
with R S have "chain (R' ∪ S') f ∧ f 0 ∈ T" by auto
from SN[unfolded conv, rule_format, OF this]
show "¬ (∀ m. ∃ n ≥ m. (f n, f (Suc n)) ∈ R)" using R by auto
qed
qed
lemma relto_mono:
assumes "R ⊆ R'" and "S ⊆ S'"
shows "relto R S ⊆ relto R' S'"
using assms rtrancl_mono by blast
lemma SN_rel_on_mono:
assumes R: "R ⊆ R'" and S: "S ⊆ S'"
and SN: "SN_rel_on R' S' T"
shows "SN_rel_on R S T"
using SN
unfolding SN_rel_on_def using SN_on_mono[OF _ relto_mono[OF R S]] by blast
lemmas SN_rel_on_alt_mono = SN_rel_on_mono[unfolded SN_rel_on_conv]
lemma SN_rel_on_imp_SN_on:
assumes "SN_rel_on R S T" shows "SN_on R T"
proof
fix f
assume "chain R f"
and f0: "f 0 ∈ T"
hence "⋀i. (f i, f (Suc i)) ∈ relto R S" by blast
thus False using assms f0 unfolding SN_rel_on_def SN_defs by blast
qed
lemma relto_Id: "relto R (S ∪ Id) = relto R S" by simp
lemma SN_rel_on_Id:
shows "SN_rel_on R (S ∪ Id) T = SN_rel_on R S T"
unfolding SN_rel_on_def by (simp only: relto_Id)
lemma SN_rel_on_empty[simp]: "SN_rel_on R {} T = SN_on R T"
unfolding SN_rel_on_def by auto
lemma SN_rel_on_ideriv: "SN_rel_on R S T = (¬ (∃ as. ideriv R S as ∧ as 0 ∈ T))" (is "?L = ?R")
proof
assume ?L
show ?R
proof
assume "∃ as. ideriv R S as ∧ as 0 ∈ T"
then obtain as where id: "ideriv R S as" and T: "as 0 ∈ T" by auto
note id = id[unfolded ideriv_def]
from ‹?L›[unfolded SN_rel_on_conv SN_rel_on_alt_def, THEN spec[of _ as]]
id T obtain i where i: "⋀ j. j ≥ i ⟹ (as j, as (Suc j)) ∉ R" by auto
with id[unfolded INFM_nat, THEN conjunct2, THEN spec[of _ "Suc i"]] show False by auto
qed
next
assume ?R
show ?L
unfolding SN_rel_on_conv SN_rel_on_alt_def
proof(intro allI impI)
fix as
assume "chain (R ∪ S) as ∧ as 0 ∈ T"
with ‹?R›[unfolded ideriv_def] have "¬ (INFM i. (as i, as (Suc i)) ∈ R)" by auto
from this[unfolded INFM_nat] obtain i where i: "⋀j. i < j ⟹ (as j, as (Suc j)) ∉ R" by auto
show "¬ (INFM j. (as j, as (Suc j)) ∈ R)" unfolding INFM_nat using i by blast
qed
qed
lemma SN_rel_to_SN_rel_alt: "SN_rel R S ⟹ SN_rel_alt R S"
proof (unfold SN_rel_on_def)
assume SN: "SN (relto R S)"
show ?thesis
proof (unfold SN_rel_on_alt_def, intro allI impI)
fix f
presume steps: "chain (R ∪ S) f"
obtain r where r: "⋀j. r j ≡ (f j, f (Suc j)) ∈ R" by auto
show "¬ (INFM j. (f j, f (Suc j)) ∈ R)"
proof (rule ccontr)
assume "¬ ?thesis"
hence ih: "infinitely_many r" unfolding infinitely_many_def r by blast
obtain r_index where "r_index = infinitely_many.index r" by simp
with infinitely_many.index_p[OF ih] infinitely_many.index_ordered[OF ih] infinitely_many.index_not_p_between[OF ih]
have r_index: "⋀ i. r (r_index i) ∧ r_index i < r_index (Suc i) ∧ (∀ j. r_index i < j ∧ j < r_index (Suc i) ⟶ ¬ r j)" by auto
obtain g where g: "⋀ i. g i ≡ f (r_index i)" ..
{
fix i
let ?ri = "r_index i"
let ?rsi = "r_index (Suc i)"
from r_index have isi: "?ri < ?rsi" by auto
obtain ri rsi where ri: "ri = ?ri" and rsi: "rsi = ?rsi" by auto
with r_index[of i] steps have inter: "⋀ j. ri < j ∧ j < rsi ⟹ (f j, f (Suc j)) ∈ S" unfolding r by auto
from ri isi rsi have risi: "ri < rsi" by simp
{
fix n
assume "Suc n ≤ rsi - ri"
hence "(f (Suc ri), f (Suc (n + ri))) ∈ S^*"
proof (induct n, simp)
case (Suc n)
hence stepps: "(f (Suc ri), f (Suc (n+ri))) ∈ S^*" by simp
have "(f (Suc (n+ri)), f (Suc (Suc n + ri))) ∈ S"
using inter[of "Suc n + ri"] Suc(2) by auto
with stepps show ?case by simp
qed
}
from this[of "rsi - ri - 1"] risi have
"(f (Suc ri), f rsi) ∈ S^*" by simp
with ri rsi have ssteps: "(f (Suc ?ri), f ?rsi) ∈ S^*" by simp
with r_index[of i] have "(f ?ri, f ?rsi) ∈ R O S^*" unfolding r by auto
hence "(g i, g (Suc i)) ∈ S^* O R O S^*" using rtrancl_refl unfolding g by auto
}
hence "¬ SN (S^* O R O S^*)" unfolding SN_defs by blast
with SN show False by simp
qed
qed simp
qed
lemma SN_rel_alt_to_SN_rel : "SN_rel_alt R S ⟹ SN_rel R S"
proof (unfold SN_rel_on_def)
assume SN: "SN_rel_alt R S"
show "SN (relto R S)"
proof
fix f
assume "chain (relto R S) f"
hence steps: "⋀i. (f i, f (Suc i)) ∈ S^* O R O S^*" by auto
let ?prop = "λ i ai bi. (f i, bi) ∈ S^* ∧ (bi, ai) ∈ R ∧ (ai, f (Suc (i))) ∈ S^*"
{
fix i
from steps obtain bi ai where "?prop i ai bi" by blast
hence "∃ ai bi. ?prop i ai bi" by blast
}
hence "∀ i. ∃ bi ai. ?prop i ai bi" by blast
from choice[OF this] obtain b where "∀ i. ∃ ai. ?prop i ai (b i)" by blast
from choice[OF this] obtain a where steps: "⋀ i. ?prop i (a i) (b i)" by blast
let ?prop = "λ i li. (b i, a i) ∈ R ∧ (∀ j < length li. ((a i # li) ! j, (a i # li) ! Suc j) ∈ S) ∧ last (a i # li) = b (Suc i)"
{
fix i
from steps[of i] steps[of "Suc i"] have "(a i, f (Suc i)) ∈ S^*" and "(f (Suc i), b (Suc i)) ∈ S^*" by auto
from rtrancl_trans[OF this] steps[of i] have R: "(b i, a i) ∈ R" and S: "(a i, b (Suc i)) ∈ S^*" by blast+
from S[unfolded rtrancl_list_conv] obtain li where "last (a i # li) = b (Suc i) ∧ (∀ j < length li. ((a i # li) ! j, (a i # li) ! Suc j) ∈ S)" ..
with R have "?prop i li" by blast
hence "∃ li. ?prop i li" ..
}
hence "∀ i. ∃ li. ?prop i li" ..
from choice[OF this] obtain l where steps: "⋀ i. ?prop i (l i)" by auto
let ?p = "λ i. ?prop i (l i)"
from steps have steps: "⋀ i. ?p i" by blast
let ?l = "λ i. a i # l i"
let ?l' = "λ i. length (?l i)"
let ?g = "λ i. inf_concat_simple ?l' i"
obtain g where g: "⋀ i. g i = (let (ii,jj) = ?g i in ?l ii ! jj)" by auto
have len: "⋀ i j n. ?g n = (i,j) ⟹ j < length (?l i)"
proof -
fix i j n
assume n: "?g n = (i,j)"
show "j < length (?l i)"
proof (cases n)
case 0
with n have "j = 0" by auto
thus ?thesis by simp
next
case (Suc nn)
obtain ii jj where nn: "?g nn = (ii,jj)" by (cases "?g nn", auto)
show ?thesis
proof (cases "Suc jj < length (?l ii)")
case True
with nn Suc have "?g n = (ii, Suc jj)" by auto
with n True show ?thesis by simp
next
case False
with nn Suc have "?g n = (Suc ii, 0)" by auto
with n show ?thesis by simp
qed
qed
qed
have gsteps: "⋀ i. (g i, g (Suc i)) ∈ R ∪ S"
proof -
fix n
obtain i j where n: "?g n = (i, j)" by (cases "?g n", auto)
show "(g n, g (Suc n)) ∈ R ∪ S"
proof (cases "Suc j < length (?l i)")
case True
with n have "?g (Suc n) = (i, Suc j)" by auto
with n have gn: "g n = ?l i ! j" and gsn: "g (Suc n) = ?l i ! (Suc j)" unfolding g by auto
thus ?thesis using steps[of i] True by auto
next
case False
with n have "?g (Suc n) = (Suc i, 0)" by auto
with n have gn: "g n = ?l i ! j" and gsn: "g (Suc n) = a (Suc i)" unfolding g by auto
from gn len[OF n] False have "j = length (?l i) - 1" by auto
with gn have gn: "g n = last (?l i)" using last_conv_nth[of "?l i"] by auto
from gn gsn show ?thesis using steps[of i] steps[of "Suc i"] by auto
qed
qed
have infR: "INFM j. (g j, g (Suc j)) ∈ R" unfolding INFM_nat_le
proof
fix n
obtain i j where n: "?g n = (i,j)" by (cases "?g n", auto)
from len[OF n] have j: "j < ?l' i" .
let ?k = "?l' i - 1 - j"
obtain k where k: "k = j + ?k" by auto
from j k have k2: "k = ?l' i - 1" and k3: "j + ?k < ?l' i" by auto
from inf_concat_simple_add[OF n, of ?k, OF k3]
have gnk: "?g (n + ?k) = (i, k)" by (simp only: k)
hence "g (n + ?k) = ?l i ! k" unfolding g by auto
hence gnk2: "g (n + ?k) = last (?l i)" using last_conv_nth[of "?l i"] k2 by auto
from k2 gnk have "?g (Suc (n+?k)) = (Suc i, 0)" by auto
hence gnsk2: "g (Suc (n+?k)) = a (Suc i)" unfolding g by auto
from steps[of i] steps[of "Suc i"] have main: "(g (n+?k), g (Suc (n+?k))) ∈ R"
by (simp only: gnk2 gnsk2)
show "∃ j ≥ n. (g j, g (Suc j)) ∈ R"
by (rule exI[of _ "n + ?k"], auto simp: main[simplified])
qed
from SN[unfolded SN_rel_on_alt_def] gsteps infR show False by blast
qed
qed
lemma SN_rel_alt_r_empty : "SN_rel_alt {} S"
unfolding SN_rel_defs by auto
lemma SN_rel_alt_s_empty : "SN_rel_alt R {} = SN R"
unfolding SN_rel_defs SN_defs by auto
lemma SN_rel_mono':
"R ⊆ R' ⟹ S ⊆ R' ∪ S' ⟹ SN_rel R' S' ⟹ SN_rel R S"
unfolding SN_rel_on_conv SN_rel_defs INFM_nat_le
by (metis contra_subsetD sup.left_idem sup.mono)
lemma SN_rel_mono:
assumes R: "R ⊆ R'" and S: "S ⊆ S'" and SN: "SN_rel R' S'"
shows "SN_rel R S"
using SN unfolding SN_rel_defs using SN_subset[OF _ relto_mono[OF R S]] by blast
lemmas SN_rel_alt_mono = SN_rel_mono[unfolded SN_rel_on_conv]
lemma SN_rel_imp_SN : assumes "SN_rel R S" shows "SN R"
proof
fix f
assume "∀ i. (f i, f (Suc i)) ∈ R"
hence "⋀ i. (f i, f (Suc i)) ∈ relto R S" by blast
thus False using assms unfolding SN_rel_defs SN_defs by fast
qed
lemma relto_trancl_conv : "(relto R S)^+ = ((R ∪ S))^* O R O ((R ∪ S))^*" by regexp
lemma SN_rel_Id:
shows "SN_rel R (S ∪ Id) = SN_rel R S"
unfolding SN_rel_defs by (simp only: relto_Id)
lemma relto_rtrancl: "relto R (S^*) = relto R S" by regexp
lemma SN_rel_empty[simp]: "SN_rel R {} = SN R"
unfolding SN_rel_defs by auto
lemma SN_rel_ideriv: "SN_rel R S = (¬ (∃ as. ideriv R S as))" (is "?L = ?R")
proof
assume ?L
show ?R
proof
assume "∃ as. ideriv R S as"
then obtain as where id: "ideriv R S as" by auto
note id = id[unfolded ideriv_def]
from ‹?L›[unfolded SN_rel_on_conv SN_rel_defs, THEN spec[of _ as]]
id obtain i where i: "⋀ j. j ≥ i ⟹ (as j, as (Suc j)) ∉ R" by auto
with id[unfolded INFM_nat, THEN conjunct2, THEN spec[of _ "Suc i"]] show False by auto
qed
next
assume ?R
show ?L
unfolding SN_rel_on_conv SN_rel_defs
proof (intro allI impI)
fix as
presume "chain (R ∪ S) as"
with ‹?R›[unfolded ideriv_def] have "¬ (INFM i. (as i, as (Suc i)) ∈ R)" by auto
from this[unfolded INFM_nat] obtain i where i: "⋀ j. i < j ⟹ (as j, as (Suc j)) ∉ R" by auto
show "¬ (INFM j. (as j, as (Suc j)) ∈ R)" unfolding INFM_nat using i by blast
qed simp
qed
lemma SN_rel_map:
fixes R Rw R' Rw' :: "'a rel"
defines A: "A ≡ R' ∪ Rw'"
assumes SN: "SN_rel R' Rw'"
and R: "⋀s t. (s,t) ∈ R ⟹ (f s, f t) ∈ A^* O R' O A^*"
and Rw: "⋀s t. (s,t) ∈ Rw ⟹ (f s, f t) ∈ A^*"
shows "SN_rel R Rw"
unfolding SN_rel_defs
proof
fix g
assume steps: "chain (relto R Rw) g"
let ?f = "λi. (f (g i))"
obtain h where h: "h = ?f" by auto
{
fix i
let ?m = "λ (x,y). (f x, f y)"
{
fix s t
assume "(s,t) ∈ Rw^*"
hence "?m (s,t) ∈ A^*"
proof (induct)
case base show ?case by simp
next
case (step t u)
from Rw[OF step(2)] step(3)
show ?case by auto
qed
} note Rw = this
from steps have "(g i, g (Suc i)) ∈ relto R Rw" ..
from this
obtain s t where gs: "(g i,s) ∈ Rw^*" and st: "(s,t) ∈ R" and tg: "(t, g (Suc i)) ∈ Rw^*" by auto
from Rw[OF gs] R[OF st] Rw[OF tg]
have step: "(?f i, ?f (Suc i)) ∈ A^* O (A^* O R' O A^*) O A^*"
by fast
have "(?f i, ?f (Suc i)) ∈ A^* O R' O A^*"
by (rule subsetD[OF _ step], regexp)
hence "(h i, h (Suc i)) ∈ (relto R' Rw')^+"
unfolding A h relto_trancl_conv .
}
hence "¬ SN ((relto R' Rw')^+)" by auto
with SN_imp_SN_trancl[OF SN[unfolded SN_rel_on_def]]
show False by simp
qed