(* Title: Abstract Rewriting Author: Christian Sternagel <christian.sternagel@uibk.ac.at> Rene Thiemann <rene.tiemann@uibk.ac.at> Maintainer: Christian Sternagel and Rene Thiemann License: LGPL *) (* Copyright 2010 Christian Sternagel and René Thiemann This file is part of IsaFoR/CeTA. IsaFoR/CeTA is free software: you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. IsaFoR/CeTA is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with IsaFoR/CeTA. If not, see <http://www.gnu.org/licenses/>. *) 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