Theory Relative_Rewriting

(*  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

datatype SN_rel_ext_type = top_s | top_ns | normal_s | normal_ns

fun SN_rel_ext_step :: "'a rel  'a rel  'a rel  'a rel  SN_rel_ext_type  'a rel" where
  "SN_rel_ext_step P Pw R Rw top_s = P"
| "SN_rel_ext_step P Pw R Rw top_ns = Pw"
| "SN_rel_ext_step P Pw R Rw normal_s = R"
| "SN_rel_ext_step P Pw R Rw normal_ns = Rw"

(* relative termination with four relations as required in DP-framework *)
definition SN_rel_ext :: "'a rel  'a rel  'a rel  'a rel  ('a  bool)  bool" where
  "SN_rel_ext P Pw R Rw M  (¬ (f t. 
    ( i. (f i, f (Suc i))  SN_rel_ext_step P Pw R Rw (t i))
     ( i. M (f i))
     (INFM i. t i  {top_s,top_ns})
     (INFM i. t i  {top_s,normal_s})))"

lemma SN_rel_ext_step_mono: assumes "P  P'" "Pw  Pw'" "R  R'" "Rw  Rw'"
  shows "SN_rel_ext_step P Pw R Rw t  SN_rel_ext_step P' Pw' R' Rw' t"
  using assms
  by (cases t, auto)

lemma SN_rel_ext_mono: assumes subset: "P  P'" "Pw  Pw'" "R  R'" "Rw  Rw'" and
  SN: "SN_rel_ext P' Pw' R' Rw' M" shows "SN_rel_ext P Pw R Rw M"
  using SN_rel_ext_step_mono[OF subset] SN unfolding SN_rel_ext_def by blast

lemma SN_rel_ext_trans:
  fixes P Pw R Rw :: "'a rel" and M :: "'a  bool"
  defines M': "M'  {(s,t). M t}"
  defines A: "A  (P  Pw  R  Rw)  M'"
  assumes "SN_rel_ext P Pw R Rw M" 
  shows "SN_rel_ext (A^* O (P  M') O A^*) (A^* O ((P  Pw)  M') O A^*) (A^* O ((P  R)  M') O A^*) (A^*) M" (is "SN_rel_ext ?P ?Pw ?R ?Rw M")
proof (rule ccontr)
  let ?relt = "SN_rel_ext_step ?P ?Pw ?R ?Rw"
  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))  ?relt (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 auto
  let ?Un = "λ tt.  (?rel ` tt)"
  let ?UnM = "λ tt. ( (?rel ` tt))  M'"
  let ?A = "?UnM {top_s,top_ns,normal_s,normal_ns}"
  let ?P' = "?UnM {top_s}"
  let ?Pw' = "?UnM {top_s,top_ns}"
  let ?R' = "?UnM {top_s,normal_s}"
  let ?Rw' = "?UnM {top_s,top_ns,normal_s,normal_ns}"
  have A: "A = ?A" unfolding A by auto
  have P: "(P  M') = ?P'" by auto
  have Pw: "(P  Pw)  M' = ?Pw'" by auto
  have R: "(P  R)  M' = ?R'" by auto
  have Rw: "A = ?Rw'" unfolding A ..
  {
    fix s t tt
    assume m: "M s" and st: "(s,t)  ?UnM tt"
    hence " typ  tt. (s,t)  ?rel typ  M s  M t" unfolding M' by auto
  } note one_step = this
  let ?seq = "λ s t g n ty. s = g 0  t = g n  ( i < n. (g i, g (Suc i))  ?rel (ty i))  ( i  n. M (g i))"
  {
    fix s t
    assume m: "M s" and st: "(s,t)  A^*"
    from st[unfolded rtrancl_fun_conv]
    obtain g n where g0: "g 0 = s" and gn: "g n = t" and steps: " i. i < n  (g i, g (Suc i))  ?A" unfolding A by auto
    {
      fix i
      assume "i  n"
      have "M (g i)"
      proof (cases i)
        case 0
        show ?thesis unfolding 0 g0 by (rule m)
      next
        case (Suc j)
        with i  n have "j < n" by auto
        from steps[OF this] show ?thesis unfolding Suc M' by auto
      qed
    } note min = this
    {
      fix i
      assume i: "i < n" hence i': "i  n" by auto
      from i' one_step[OF min steps[OF i]]
      have " ty. (g i, g (Suc i))  ?rel ty" by blast
    }
    hence " i. ( ty. i < n  (g i, g (Suc i))  ?rel ty)" by auto
    from choice[OF this]
    obtain tt where steps: " i. i < n  (g i, g (Suc i))  ?rel (tt i)" by auto
    from g0 gn steps min
    have "?seq s t g n tt" by auto
    hence " g n tt. ?seq s t g n tt" by blast
  } note A_steps = this
  let ?seqtt = "λ s t tt g n ty. s = g 0  t = g n  n > 0  ( i<n. (g i, g (Suc i))  ?rel (ty i))  ( i  n. M (g i))  ( i < n. ty i  tt)"
  {
    fix s t tt
    assume m: "M s" and st: "(s,t)  A^* O ?UnM tt O A^*"
    then obtain u v where su: "(s,u)  A^*" and uv: "(u,v)  ?UnM tt" and vt: "(v,t)  A^*"
      by auto
    from A_steps[OF m su] obtain g1 n1 ty1 where seq1: "?seq s u g1 n1 ty1" by auto
    from uv have "M v" unfolding M' by auto
    from A_steps[OF this vt] obtain g2 n2 ty2 where seq2: "?seq v t g2 n2 ty2" by auto
    from seq1 have "M u" by auto
    from one_step[OF this uv] obtain ty where ty: "ty  tt" and uv: "(u,v)  ?rel ty" by auto
    let ?g = "λ i. if i  n1 then g1 i else g2 (i - (Suc n1))"
    let ?ty = "λ i. if i < n1 then ty1 i else if i = n1 then ty else ty2 (i - (Suc n1))"
    let ?n = "Suc (n1 + n2)"
    have ex: " i < ?n. ?ty i  tt"
      by (rule exI[of _ n1], simp add: ty)
    have steps: " i < ?n. (?g i, ?g (Suc i))  ?rel (?ty i)"
    proof (intro allI impI)
      fix i
      assume "i < ?n"
      show "(?g i, ?g (Suc i))  ?rel (?ty i)"
      proof (cases "i  n1")
        case True
        with seq1 seq2 uv show ?thesis by auto
      next
        case False
        hence "i = Suc n1 + (i - Suc n1)" by auto
        then obtain k where i: "i = Suc n1 + k" by auto
        with i < ?n have "k < n2" by auto
        thus ?thesis using seq2 unfolding i by auto
      qed
    qed
    from steps seq1 seq2 ex 
    have seq: "?seqtt s t tt ?g ?n ?ty" by auto
    have " g n ty. ?seqtt s t tt g n ty" 
      by (intro exI, rule seq)
  } note A_tt_A = this
  let ?tycon = "λ ty1 ty2 tt ty' n. ty1 = ty2  (i < n. ty' i  tt)"
  let ?seqt = "λ i ty g n ty'. f i = g 0  f (Suc i) = g n  ( j < n. (g j, g (Suc j))  ?rel (ty' j))  ( j  n. M (g j)) 
                 (?tycon (ty i) top_s {top_s} ty' n)
                 (?tycon (ty i) top_ns {top_s,top_ns} ty' n)
                 (?tycon (ty i) normal_s {top_s,normal_s} ty' n)"
  {
    fix i
    have " g n ty'. ?seqt i ty g n ty'"
    proof (cases "ty i")
      case top_s
      from steps[of i, unfolded top_s] 
      have "(f i, f (Suc i))  ?P" by auto
      from A_tt_A[OF min this[unfolded P]]
      show ?thesis unfolding top_s by auto
    next
      case top_ns
      from steps[of i, unfolded top_ns] 
      have "(f i, f (Suc i))  ?Pw" by auto
      from A_tt_A[OF min this[unfolded Pw]]
      show ?thesis unfolding top_ns by auto
    next
      case normal_s
      from steps[of i, unfolded normal_s] 
      have "(f i, f (Suc i))  ?R" by auto
      from A_tt_A[OF min this[unfolded R]]
      show ?thesis unfolding normal_s by auto
    next
      case normal_ns
      from steps[of i, unfolded normal_ns] 
      have "(f i, f (Suc i))  ?Rw" by auto
      from A_steps[OF min this]
      show ?thesis unfolding normal_ns by auto
    qed
  }
  hence " i.  g n ty'. ?seqt i ty g n ty'" by auto
  from choice[OF this] obtain g where " i.  n ty'. ?seqt i ty (g i) n ty'" by auto
  from choice[OF this] obtain n where " i.  ty'. ?seqt i ty (g i) (n i) ty'" by auto
  from choice[OF this] obtain ty' where " i. ?seqt i ty (g i) (n i) (ty' i)" by auto
  hence partial: " i. ?seqt i ty (g i) (n i) (ty' i)" ..
  (* it remains to concatenate all these finite sequences to an infinite one *)
  let ?ind = "inf_concat n"
  let ?g = "λ k. (λ (i,j). g i j) (?ind k)"
  let ?ty = "λ k. (λ (i,j). ty' i j) (?ind k)"
  have inf: "INFM i. 0 < n i"
    unfolding INFM_nat_le
  proof (intro allI)
    fix m
    from inf1[unfolded INFM_nat_le]
    obtain k where k: "k  m" and ty: "ty k  {top_s, top_ns}" by auto
    show " k  m. 0 < n k"
    proof (intro exI conjI, rule k)
      from partial[of k] ty show "0 < n k" by (cases "n k", auto)
    qed
  qed
  note bounds = inf_concat_bounds[OF inf]
  note inf_Suc = inf_concat_Suc[OF inf]
  note inf_mono = inf_concat_mono[OF inf]
  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 ik: "?ind k = (i,j)" by force
    from bounds[OF this] have j: "j < n i" by auto
    show "M (?g k)" unfolding ik using partial[of i] j by auto
  next
    fix k
    obtain i j where ik: "?ind k = (i,j)" by force
    from bounds[OF this] have j: "j < n i" by auto
    from partial[of i] j have step: "(g i j, g i (Suc j))  ?rel (ty' i j)" by auto
    obtain i' j' where isk: "?ind (Suc k) = (i',j')" by force
    have i'j': "g i' j' = g i (Suc j)"
    proof (rule inf_Suc[OF _ ik isk])
      fix i
      from partial[of i]
      have "g i (n i) = f (Suc i)" by simp
      also have "... = g (Suc i) 0" using partial[of "Suc i"] by simp
      finally show "g i (n i) = g (Suc i) 0" .
    qed
    show "(?g k, ?g (Suc k))  ?rel (?ty k)"
      unfolding ik isk split i'j'
      by (rule step)
  next
    show "INFM i. ?ty i  {top_s, top_ns}"
      unfolding INFM_nat_le
    proof (intro allI)
      fix k
      obtain i j where ik: "?ind k = (i,j)" by force      
      from inf1[unfolded INFM_nat] obtain i' where i': "i' > i" and ty: "ty i'  {top_s, top_ns}" by auto
      from partial[of i'] ty obtain j' where j': "j' < n i'" and ty': "ty' i' j'  {top_s, top_ns}" by auto      
      from inf_concat_surj[of _ n, OF j'] obtain k' where ik': "?ind k' = (i',j')" ..        
      from inf_mono[OF ik ik' i'] have k: "k  k'" by simp
      show " k'  k. ?ty k'  {top_s, top_ns}"
        by (intro exI conjI, rule k, unfold ik' split, rule ty')
    qed
  next
    show "INFM i. ?ty i  {top_s, normal_s}"
      unfolding INFM_nat_le
    proof (intro allI)
      fix k
      obtain i j where ik: "?ind k = (i,j)" by force      
      from inf2[unfolded INFM_nat] obtain i' where i': "i' > i" and ty: "ty i'  {top_s, normal_s}" by auto
      from partial[of i'] ty obtain j' where j': "j' < n i'" and ty': "ty' i' j'  {top_s, normal_s}" by auto
      from inf_concat_surj[of _ n, OF j'] obtain k' where ik': "?ind k' = (i',j')" ..
      from inf_mono[OF ik ik' i'] have k: "k  k'" by simp
      show " k'  k. ?ty k'  {top_s, normal_s}"
        by (intro exI conjI, rule k, unfold ik' split, rule ty')
    qed
  qed
  with assms show False by auto
qed


lemma SN_rel_ext_map: fixes P Pw R Rw P' Pw' R' Rw' :: "'a rel" and M M' :: "'a  bool"
  defines Ms: "Ms  {(s,t). M' t}"
  defines A: "A  (P'  Pw'  R'  Rw')  Ms"
  assumes SN: "SN_rel_ext P' Pw' R' Rw' M'" 
  and P: " s t. M s  M t  (s,t)  P  (f s, f t)  (A^* O (P'  Ms) O A^*)  I t"
  and Pw: " s t. M s  M t  (s,t)  Pw  (f s, f t)  (A^* O ((P'  Pw')  Ms) O A^*)  I t"
  and R: " s t. I s  M s  M t  (s,t)  R  (f s, f t)  (A^* O ((P'  R')  Ms) O A^*)  I t"
  and Rw: " s t. I s  M s  M t  (s,t)  Rw  (f s, f t)  A^*  I t"
  shows "SN_rel_ext P Pw R Rw M" 
proof -
  note SN = SN_rel_ext_trans[OF SN]
  let ?P = "(A^* O (P'  Ms) O A^*)"
  let ?Pw = "(A^* O ((P'  Pw')  Ms) O A^*)"
  let ?R = "(A^* O ((P'  R')  Ms) O A^*)"
  let ?Rw = "A^*"
  let ?relt = "SN_rel_ext_step ?P ?Pw ?R ?Rw"
  let ?rel = "SN_rel_ext_step P Pw R Rw" 
  show ?thesis 
  proof (rule ccontr)
    assume "¬ ?thesis"
    from this[unfolded SN_rel_ext_def]
    obtain g ty
      where steps: " i. (g i, g (Suc i))  ?rel (ty i)" 
      and min: " i. M (g i)"
      and inf1: "INFM i. ty i  {top_s, top_ns}"
      and inf2: "INFM i. ty i  {top_s, normal_s}"
      by auto
    from inf1[unfolded INFM_nat] obtain k where k: "ty k  {top_s, top_ns}" by auto
    let ?k = "Suc k"
    let ?i = "shift id ?k"
    let ?f = "λ i. f (shift g ?k i)"
    let ?ty = "shift ty ?k"
    {
      fix i
      assume ty: "ty i  {top_s,top_ns}"
      note m = min[of i] 
      note ms = min[of "Suc i"]
      from P[OF m ms]
        Pw[OF m ms]
        steps[of i]
        ty
      have "(f (g i), f (g (Suc i)))  ?relt (ty i)  I (g (Suc i))"
        by (cases "ty i", auto)
    } note stepsP = this
    {
      fix i
      assume I: "I (g i)"
      note m = min[of i] 
      note ms = min[of "Suc i"]
      from P[OF m ms]
        Pw[OF m ms]
        R[OF I m ms]
        Rw[OF I m ms]
        steps[of i]
      have "(f (g i), f (g (Suc i)))  ?relt (ty i)  I (g (Suc i))"
        by (cases "ty i", auto)
    } note stepsI = this
    {
      fix i
      have "I (g (?i i))"
      proof (induct i)
        case 0
        show ?case using stepsP[OF k] by simp
      next
        case (Suc i)
        from stepsI[OF Suc] show ?case by simp
      qed
    } note I = this
    have "¬ SN_rel_ext ?P ?Pw ?R ?Rw M'"
      unfolding SN_rel_ext_def simp_thms
    proof (rule exI[of _ ?f], rule exI[of _ ?ty], intro allI conjI)
      fix i
      show "(?f i, ?f (Suc i))  ?relt (?ty i)"
        using stepsI[OF I[of i]] by auto
    next
      show "INFM i. ?ty i  {top_s, top_ns}"
        unfolding Infm_shift[of "λi. i  {top_s,top_ns}" ty ?k]
        by (rule inf1)
    next
      show "INFM i. ?ty i  {top_s, normal_s}"
        unfolding Infm_shift[of "λi. i  {top_s,normal_s}" ty ?k]
        by (rule inf2)
    next
      fix i
      have A: "A  Ms" unfolding A by auto
      from rtrancl_mono[OF this] have As: "A^*  Ms^*" by auto
      have PM: "?P  Ms^* O Ms O Ms^*" using As by auto
      have PwM: "?Pw  Ms^* O Ms O Ms^*" using As by auto
      have RM: "?R  Ms^* O Ms O Ms^*" using As by auto
      have RwM: "?Rw  Ms^*" using As by auto
      from PM PwM RM have "?P  ?Pw  ?R  Ms^* O Ms O Ms^*" (is "?PPR  _") by auto
      also have "...  Ms^+" by regexp
      also have "... = Ms"
      proof
        have "Ms^+  Ms^* O Ms" by regexp
        also have "...  Ms" unfolding Ms by auto
        finally show "Ms^+  Ms" .
      qed regexp
      finally have PPR: "?PPR  Ms" .
      show "M' (?f i)"
      proof (induct i)
        case 0
        from stepsP[OF k] k
        have "(f (g k), f (g (Suc k)))  ?PPR" by (cases "ty k", auto)
        with PPR show ?case unfolding Ms by simp blast
      next
        case (Suc i)
        show ?case
        proof (cases "?ty i = normal_ns")
          case False
          hence "?ty i  {top_s,top_ns,normal_s}"
            by (cases "?ty i", auto)
          with stepsI[OF I[of i]] have "(?f i, ?f (Suc i))  ?PPR"
            by auto
          from subsetD[OF PPR this] have "(?f i, ?f (Suc i))  Ms" .
          thus ?thesis unfolding Ms by auto
        next
          case True
          with stepsI[OF I[of i]] have "(?f i, ?f (Suc i))  ?Rw" by auto
          with RwM have mem: "(?f i, ?f (Suc i))  Ms^*" by auto
          thus ?thesis
          proof (cases)
            case base
            with Suc show ?thesis by simp
          next
            case step
            thus ?thesis unfolding Ms by simp
          qed
        qed
      qed
    qed
    with SN
    show False unfolding A Ms by simp
  qed
qed

(* and a version where it is assumed that f always preserves M and that R' and Rw' preserve M' *)
lemma SN_rel_ext_map_min: fixes P Pw R Rw P' Pw' R' Rw' :: "'a rel" and M M' :: "'a  bool"
  defines Ms: "Ms  {(s,t). M' t}"
  defines A: "A  P'  Ms  Pw'  Ms  R'  Rw'"
  assumes SN: "SN_rel_ext P' Pw' R' Rw' M'" 
  and M: " t. M t  M' (f t)"
  and M': " s t. M' s  (s,t)  R'  Rw'  M' t"
  and P: " s t. M s  M t  M' (f s)  M' (f t)  (s,t)  P  (f s, f t)  (A^* O (P'  Ms) O A^*)  I t"
  and Pw: " s t. M s  M t  M' (f s)  M' (f t)  (s,t)  Pw  (f s, f t)  (A^* O (P'  Ms  Pw'  Ms) O A^*)  I t"
  and R: " s t. I s  M s  M t  M' (f s)  M' (f t)  (s,t)  R  (f s, f t)  (A^* O (P'  Ms  R') O A^*)  I t"
  and Rw: " s t. I s  M s  M t  M' (f s)  M' (f t)  (s,t)  Rw  (f s, f t)  A^*  I t"
  shows "SN_rel_ext P Pw R Rw M"  
proof -
  let ?Ms = "{(s,t). M' t}"
  let ?A = "(P'  Pw'  R'  Rw')  ?Ms"
  {
    fix s t
    assume s: "M' s" and "(s,t)  A" 
    with M'[OF s, of t] have "(s,t)  ?A  M' t" unfolding Ms A by auto
  } note Aone = this
  {
    fix s t
    assume s: "M' s" and steps: "(s,t)  A^*"
    from steps have "(s,t)  ?A^*  M' t"
    proof (induct)
      case base from s show ?case by simp
    next
      case (step t u)
      note one = Aone[OF step(3)[THEN conjunct2] step(2)] 
      from step(3) one
      have steps: "(s,u)  ?A^* O ?A" by blast      
      have "(s,u)  ?A^*" 
        by (rule subsetD[OF _ steps], regexp)
      with one show ?case by simp
    qed
  } note Amany = this      
  let ?P = "(A^* O (P'  Ms) O A^*)"
  let ?Pw = "(A^* O (P'  Ms  Pw'  Ms) O A^*)"
  let ?R = "(A^* O (P'  Ms  R') O A^*)"
  let ?Rw = "A^*"
  let ?P' = "(?A^* O (P'  ?Ms) O ?A^*)"
  let ?Pw' = "(?A^* O ((P'  Pw')  ?Ms) O ?A^*)"
  let ?R' = "(?A^* O ((P'  R')  ?Ms) O ?A^*)"
  let ?Rw' = "?A^*"
  show ?thesis 
  proof (rule SN_rel_ext_map[OF SN])
    fix s t
    assume s: "M s" and t: "M t" and step: "(s,t)  P"
    from P[OF s t M[OF s] M[OF t] step]
    have "(f s, f t)  ?P" and I: "I t"  by auto
    then obtain u v where su: "(f s, u)  A^*" and uv: "(u,v)  P'  Ms"
      and vt: "(v,f t)  A^*" by auto
    from Amany[OF M[OF s] su] have su: "(f s, u)  ?A^*" and u: "M' u" by auto
    from uv have v: "M' v" unfolding Ms by auto
    from Amany[OF v vt] have vt: "(v, f t)  ?A^*" by auto
    from su uv vt I 
    show "(f s, f t)  ?P'  I t" unfolding Ms by auto
  next
    fix s t
    assume s: "M s" and t: "M t" and step: "(s,t)  Pw"
    from Pw[OF s t M[OF s] M[OF t] step]
    have "(f s, f t)  ?Pw" and I: "I t"  by auto
    then obtain u v where su: "(f s, u)  A^*" and uv: "(u,v)  P'  Ms  Pw'  Ms"
      and vt: "(v,f t)  A^*" by auto
    from Amany[OF M[OF s] su] have su: "(f s, u)  ?A^*" and u: "M' u" by auto
    from uv have uv: "(u,v)  (P'  Pw')  ?Ms" and v: "M' v" unfolding Ms 
      by auto
    from Amany[OF v vt] have vt: "(v, f t)  ?A^*" by auto
    from su uv vt I 
    show "(f s, f t)  ?Pw'  I t"  by auto
  next
    fix s t
    assume I: "I s" and s: "M s" and t: "M t" and step: "(s,t)  R"
    from R[OF I s t M[OF s] M[OF t] step]
    have "(f s, f t)  ?R" and I: "I t"  by auto
    then obtain u v where su: "(f s, u)  A^*" and uv: "(u,v)  P'  Ms  R'"
      and vt: "(v,f t)  A^*" by auto
    from Amany[OF M[OF s] su] have su: "(f s, u)  ?A^*" and u: "M' u" by auto
    from uv M'[OF u, of v] have uv: "(u,v)  (P'  R')  ?Ms" and v: "M' v" unfolding Ms 
      by auto
    from Amany[OF v vt] have vt: "(v, f t)  ?A^*" by auto
    from su uv vt I 
    show "(f s, f t)  ?R'  I t"  by auto
  next
    fix s t
    assume I: "I s" and s: "M s" and t: "M t" and step: "(s,t)  Rw"
    from Rw[OF I s t M[OF s] M[OF t] step]
    have steps: "(f s, f t)  ?Rw" and I: "I t"  by auto
    from Amany[OF M[OF s] steps] I
    show "(f s, f t)  ?Rw'  I t"  by auto
  qed
qed

(*OLD PART*)
lemma SN_relto_imp_SN_rel: "SN (relto R S)  SN_rel R S"
proof -
  assume SN: "SN (relto R S)"
  show ?thesis
  proof (simp only: SN_rel_on_conv SN_rel_defs, 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 INFM_nat_le 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

(*FIXME: move*)
lemma rtrancl_list_conv:
  "((s,t)  R^*) = 
  (list. last (s # list) = t  (i. i < length list  ((s # list) ! i, (s # list) ! Suc i)  R))" (is "?l = ?r")
proof 
  assume ?r
  then obtain list where "last (s # list) = t  ( i. i < length list  ((s # list) ! i, (s # list) ! Suc i)  R)" ..
  thus ?l
  proof (induct list arbitrary: s, simp)
    case (Cons u ll)
    hence "last (u # ll) = t  ( i. i < length ll  ((u # ll) ! i, (u # ll) ! Suc i)  R)" by auto
    from Cons(1)[OF this] have rec: "(u,t)  R^*" .
    from Cons have "(s, u)  R" by auto
    with rec show ?case by auto
  qed
next
  assume ?l
  from rtrancl_imp_seq[OF this]
  obtain S n where s: "S 0 = s" and t: "S n = t" and steps: " i<n. (S i, S (Suc i))  R" by auto