Theory Abstract_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 ‹Abstract Rewrite Systems›

theory Abstract_Rewriting
imports
  "HOL-Library.Infinite_Set"
  "Regular-Sets.Regexp_Method"
  Seq
begin

(*FIXME: move*)
lemma trancl_mono_set:
  "r ⊆ s ⟹ r⇧⁺ ⊆ s⇧⁺"
  by (blast intro: trancl_mono)

lemma relpow_mono:
  fixes r :: "'a rel"
  assumes "r ⊆ r'" shows "r ^^ n ⊆ r' ^^ n"
  using assms by (induct n) auto

lemma refl_inv_image:
  "refl R ⟹ refl (inv_image R f)"
  by (simp add: inv_image_def refl_on_def)

subsection ‹Definitions›

text ‹Two elements are \emph{joinable} (and then have in the joinability relation)
w.r.t.\ @{term "A"}, iff they have a common reduct.›
definition join :: "'a rel ⇒ 'a rel"  (‹(_⇧^↓)› [1000] 999) where
  "A⇧^↓ = A⇧^* O (A¯)⇧^*"

text ‹Two elements are \emph{meetable} (and then have in the meetability relation)
w.r.t.\ @{term "A"}, iff they have a common ancestor.›
definition meet :: "'a rel ⇒ 'a rel"  (‹(_⇧^↑)› [1000] 999) where
  "A⇧^↑ = (A¯)⇧^* O A⇧^*"

text ‹The \emph{symmetric closure} of a relation allows steps in both directions.›
abbreviation symcl :: "'a rel ⇒ 'a rel"  (‹(_⇧^↔)› [1000] 999) where
  "A⇧^↔ ≡ A ∪ A¯"

text ‹A \emph{conversion} is a (possibly empty) sequence of steps in the symmetric closure.›
definition conversion :: "'a rel ⇒ 'a rel"  (‹(_⇧^↔⇧^*)› [1000] 999) where
  "A⇧^↔⇧^* = (A⇧^↔)⇧^*"

text ‹The set of \emph{normal forms} of an ARS constitutes all the elements that do
not have any successors.›
definition NF :: "'a rel ⇒ 'a set" where
  "NF A = {a. A `` {a} = {}}"

definition normalizability :: "'a rel ⇒ 'a rel"  (‹(_⇧^!)› [1000] 999) where
  "A⇧^! = {(a, b). (a, b) ∈ A⇧^* ∧ b ∈ NF A}"

notation (ASCII)
  symcl  (‹(_^<->)› [1000] 999) and
  conversion  (‹(_^<->*)› [1000] 999) and
  normalizability  (‹(_^!)› [1000] 999)

lemma symcl_converse:
  "(A⇧^↔)¯ = A⇧^↔" by auto

lemma symcl_Un: "(A ∪ B)⇧^↔ = A⇧^↔ ∪ B⇧^↔" by auto

lemma no_step:
  assumes "A `` {a} = {}" shows "a ∈ NF A"
  using assms by (auto simp: NF_def)

lemma joinI:
  "(a, c) ∈ A⇧^* ⟹ (b, c) ∈ A⇧^* ⟹ (a, b) ∈ A⇧^↓"
  by (auto simp: join_def rtrancl_converse)

lemma joinI_left:
  "(a, b) ∈ A⇧^* ⟹ (a, b) ∈ A⇧^↓"
  by (auto simp: join_def)

lemma joinI_right: "(b, a) ∈ A⇧^* ⟹ (a, b) ∈ A⇧^↓"
  by (rule joinI) auto

lemma joinE:
  assumes "(a, b) ∈ A⇧^↓"
  obtains c where "(a, c) ∈ A⇧^*" and "(b, c) ∈ A⇧^*"
  using assms by (auto simp: join_def rtrancl_converse)

lemma joinD:
  "(a, b) ∈ A⇧^↓ ⟹ ∃c. (a, c) ∈ A⇧^* ∧ (b, c) ∈ A⇧^*"
  by (blast elim: joinE)

lemma meetI:
  "(a, b) ∈ A⇧^* ⟹ (a, c) ∈ A⇧^* ⟹ (b, c) ∈ A⇧^↑"
  by (auto simp: meet_def rtrancl_converse)

lemma meetE:
  assumes "(b, c) ∈ A⇧^↑"
  obtains a where "(a, b) ∈ A⇧^*" and "(a, c) ∈ A⇧^*"
  using assms by (auto simp: meet_def rtrancl_converse)

lemma meetD: "(b, c) ∈ A⇧^↑ ⟹ ∃a. (a, b) ∈ A⇧^* ∧ (a, c) ∈ A⇧^*"
  by (blast elim: meetE)

lemma conversionI: "(a, b) ∈ (A⇧^↔)⇧^* ⟹ (a, b) ∈ A⇧^↔⇧^*"
  by (simp add: conversion_def)

lemma conversion_refl [simp]: "(a, a) ∈ A⇧^↔⇧^*"
  by (simp add: conversion_def)

lemma conversionI':
  assumes "(a, b) ∈ A⇧^*" shows "(a, b) ∈ A⇧^↔⇧^*"
using assms
proof (induct)
  case base then show ?case by simp
next
  case (step b c)
  then have "(b, c) ∈ A⇧^↔" by simp
  with ‹(a, b) ∈ A⇧^↔⇧^*› show ?case unfolding conversion_def by (rule rtrancl.intros)
qed

lemma rtrancl_comp_trancl_conv:
  "r⇧^* O r = r⇧⁺" by regexp

lemma trancl_o_refl_is_trancl:
  "r⇧⁺ O r⇧⁼ = r⇧⁺" by regexp

lemma conversionE:
  "(a, b) ∈ A⇧^↔⇧^* ⟹ ((a, b) ∈ (A⇧^↔)⇧^* ⟹ P) ⟹ P"
  by (simp add: conversion_def)

text ‹Later declarations are tried first for `proof' and `rule,' then have the ``main''
introduction\,/\, elimination rules for constants should be declared last.›
declare joinI_left [intro]
declare joinI_right [intro]
declare joinI [intro]
declare joinD [dest]
declare joinE [elim]

declare meetI [intro]
declare meetD [dest]
declare meetE [elim]

declare conversionI' [intro]
declare conversionI [intro]
declare conversionE [elim]

lemma conversion_trans:
  "trans (A⇧^↔⇧^*)"
  unfolding trans_def
proof (intro allI impI)
  fix a b c assume "(a, b) ∈ A⇧^↔⇧^*" and "(b, c) ∈ A⇧^↔⇧^*"
  then show "(a, c) ∈ A⇧^↔⇧^*" unfolding conversion_def
  proof (induct)
    case base then show ?case by simp
  next
    case (step b c')
    from ‹(b, c') ∈ A⇧^↔› and ‹(c', c) ∈ (A⇧^↔)⇧^*›
      have "(b, c) ∈ (A⇧^↔)⇧^*" by (rule converse_rtrancl_into_rtrancl)
    with step show ?case by simp
  qed
qed

lemma conversion_sym:
  "sym (A⇧^↔⇧^*)"
  unfolding sym_def
proof (intro allI impI)
  fix a b assume "(a, b) ∈ A⇧^↔⇧^*" then show "(b, a) ∈ A⇧^↔⇧^*" unfolding conversion_def
  proof (induct)
    case base then show ?case by simp
  next
    case (step b c)
    then have "(c, b) ∈ A⇧^↔" by blast
    from ‹(c, b) ∈ A⇧^↔› and ‹(b, a) ∈ (A⇧^↔)⇧^*›
      show ?case by (rule converse_rtrancl_into_rtrancl)
  qed
qed

lemma conversion_inv:
  "(x, y) ∈ R⇧^↔⇧^* ⟷ (y, x) ∈ R⇧^↔⇧^*"
  by (auto simp: conversion_def)
     (metis (full_types) rtrancl_converseD symcl_converse)+


lemma conversion_converse [simp]:
  "(A⇧^↔⇧^*)¯ = A⇧^↔⇧^*"
  by (metis conversion_sym sym_conv_converse_eq)

lemma conversion_rtrancl [simp]:
  "(A⇧^↔⇧^*)⇧^* = A⇧^↔⇧^*"
  by (metis conversion_def rtrancl_idemp)

lemma rtrancl_join_join:
  assumes "(a, b) ∈ A⇧^*" and "(b, c) ∈ A⇧^↓" shows "(a, c) ∈ A⇧^↓"
proof -
  from ‹(b, c) ∈ A⇧^↓› obtain b' where "(b, b') ∈ A⇧^*" and "(b', c) ∈ (A¯)⇧^*"
    unfolding join_def by blast
  with ‹(a, b) ∈ A⇧^*› have "(a, b') ∈ A⇧^*" by simp
  with ‹(b', c) ∈ (A¯)⇧^*› show ?thesis unfolding join_def by blast
qed

lemma join_rtrancl_join:
  assumes "(a, b) ∈ A⇧^↓" and "(c, b) ∈ A⇧^*" shows "(a, c) ∈ A⇧^↓"
proof -
  from ‹(c, b) ∈ A⇧^*› have "(b, c) ∈ (A¯)⇧^*" unfolding rtrancl_converse by simp
  from ‹(a, b) ∈ A⇧^↓› obtain a' where "(a, a') ∈ A⇧^*" and "(a', b) ∈ (A¯)⇧^*"
    unfolding join_def by best
  with ‹(b, c) ∈ (A¯)⇧^*› have "(a', c) ∈ (A¯)⇧^*" by simp
  with ‹(a, a') ∈ A⇧^*› show ?thesis unfolding join_def by blast
qed

lemma NF_I: "(⋀b. (a, b) ∉ A) ⟹ a ∈ NF A" by (auto intro: no_step)

lemma NF_E: "a ∈ NF A ⟹ ((a, b) ∉ A ⟹ P) ⟹ P" by (auto simp: NF_def)

declare NF_I [intro]
declare NF_E [elim]

lemma NF_no_step: "a ∈ NF A ⟹ ∀b. (a, b) ∉ A" by auto

lemma NF_anti_mono:
  assumes "A ⊆ B" shows "NF B ⊆ NF A"
  using assms by auto

lemma NF_iff_no_step: "a ∈ NF A = (∀b. (a, b) ∉ A)" by auto

lemma NF_no_trancl_step:
  assumes "a ∈ NF A" shows "∀b. (a, b) ∉ A⇧⁺"
proof -
  from assms have "∀b. (a, b) ∉ A" by auto
  show ?thesis
  proof (intro allI notI)
    fix b assume "(a, b) ∈ A⇧⁺"
    then show False by (induct) (auto simp: ‹∀b. (a, b) ∉ A›)
   qed
qed

lemma NF_Id_on_fst_image [simp]: "NF (Id_on (fst ` A)) = NF A" by force

lemma fst_image_NF_Id_on [simp]: "fst ` R = Q ⟹ NF (Id_on Q) = NF R" by force

lemma NF_empty [simp]: "NF {} = UNIV" by auto

lemma normalizability_I: "(a, b) ∈ A⇧^* ⟹ b ∈ NF A ⟹ (a, b) ∈ A⇧^!"
by (simp add: normalizability_def)

lemma normalizability_I': "(a, b) ∈ A⇧^* ⟹ (b, c) ∈ A⇧^! ⟹ (a, c) ∈ A⇧^!"
by (auto simp add: normalizability_def)

lemma normalizability_E: "(a, b) ∈ A⇧^! ⟹ ((a, b) ∈ A⇧^* ⟹ b ∈ NF A ⟹ P) ⟹ P"
by (simp add: normalizability_def)

declare normalizability_I' [intro]
declare normalizability_I [intro]
declare normalizability_E [elim]


subsection ‹Properties of ARSs›

text ‹The following properties on (elements of) ARSs are defined: completeness,
Church-Rosser property, semi-completeness, strong normalization, unique normal
forms, Weak Church-Rosser property, and weak normalization.›

definition CR_on :: "'a rel ⇒ 'a set ⇒ bool" where
  "CR_on r A ⟷ (∀a∈A. ∀b c. (a, b) ∈ r⇧^* ∧ (a, c) ∈ r⇧^* ⟶ (b, c) ∈ join r)"

abbreviation CR :: "'a rel ⇒ bool" where
  "CR r ≡ CR_on r UNIV"

definition SN_on :: "'a rel ⇒ 'a set ⇒ bool" where
  "SN_on r A ⟷ ¬ (∃f. f 0 ∈ A ∧ chain r f)"

abbreviation SN :: "'a rel ⇒ bool" where
  "SN r ≡ SN_on r UNIV"

text ‹Alternative definition of @{term "SN"}.›
lemma SN_def: "SN r = (∀x. SN_on r {x})"
  unfolding SN_on_def by blast

definition UNF_on :: "'a rel ⇒ 'a set ⇒ bool" where
  "UNF_on r A ⟷ (∀a∈A. ∀b c. (a, b) ∈ r⇧^! ∧ (a, c) ∈ r⇧^! ⟶ b = c)"

abbreviation UNF :: "'a rel ⇒ bool" where "UNF r ≡ UNF_on r UNIV"

definition WCR_on :: "'a rel ⇒ 'a set ⇒ bool" where
  "WCR_on r A ⟷ (∀a∈A. ∀b c. (a, b) ∈ r ∧ (a, c) ∈ r ⟶ (b, c) ∈ join r)"

abbreviation WCR :: "'a rel ⇒ bool" where "WCR r ≡ WCR_on r UNIV"

definition WN_on :: "'a rel ⇒ 'a set ⇒ bool" where
  "WN_on r A ⟷ (∀a∈A. ∃b. (a, b) ∈ r⇧^!)"

abbreviation WN :: "'a rel ⇒ bool" where
  "WN r ≡ WN_on r UNIV"

lemmas CR_defs = CR_on_def
lemmas SN_defs = SN_on_def
lemmas UNF_defs = UNF_on_def
lemmas WCR_defs = WCR_on_def
lemmas WN_defs = WN_on_def

definition complete_on :: "'a rel ⇒ 'a set ⇒ bool" where
  "complete_on r A ⟷ SN_on r A ∧ CR_on r A"

abbreviation complete :: "'a rel ⇒ bool" where
  "complete r ≡ complete_on r UNIV"

definition semi_complete_on :: "'a rel ⇒ 'a set ⇒ bool" where
  "semi_complete_on r A ⟷  WN_on r A ∧ CR_on r A"

abbreviation semi_complete :: "'a rel ⇒ bool" where
  "semi_complete r ≡ semi_complete_on r UNIV"

lemmas complete_defs = complete_on_def
lemmas semi_complete_defs = semi_complete_on_def

text ‹Unique normal forms with respect to conversion.›
definition UNC :: "'a rel ⇒ bool" where
  "UNC A ⟷ (∀a b. a ∈ NF A ∧ b ∈ NF A ∧ (a, b) ∈ A⇧^↔⇧^* ⟶ a = b)"

lemma complete_onI:
  "SN_on r A ⟹ CR_on r A ⟹ complete_on r A"
  by (simp add: complete_defs)

lemma complete_onE:
  "complete_on r A ⟹ (SN_on r A ⟹ CR_on r A ⟹ P) ⟹ P"
  by (simp add: complete_defs)

lemma CR_onI:
  "(⋀a b c. a ∈ A ⟹ (a, b) ∈ r⇧^* ⟹ (a, c) ∈ r⇧^* ⟹ (b, c) ∈ join r) ⟹ CR_on r A"
  by (simp add: CR_defs)

lemma CR_on_singletonI:
  "(⋀b c. (a, b) ∈ r⇧^* ⟹ (a, c) ∈ r⇧^* ⟹ (b, c) ∈ join r) ⟹ CR_on r {a}"
  by (simp add: CR_defs)

lemma CR_onE:
  "CR_on r A ⟹ a ∈ A ⟹ ((b, c) ∈ join r ⟹ P) ⟹ ((a, b) ∉ r⇧^* ⟹ P) ⟹ ((a, c) ∉ r⇧^* ⟹ P) ⟹ P"
  unfolding CR_defs by blast

lemma CR_onD:
  "CR_on r A ⟹ a ∈ A ⟹ (a, b) ∈ r⇧^* ⟹ (a, c) ∈ r⇧^* ⟹ (b, c) ∈ join r"
  by (blast elim: CR_onE)

lemma semi_complete_onI: "WN_on r A ⟹ CR_on r A ⟹ semi_complete_on r A"
  by (simp add: semi_complete_defs)

lemma semi_complete_onE:
  "semi_complete_on r A ⟹ (WN_on r A ⟹ CR_on r A ⟹ P) ⟹ P"
  by (simp add: semi_complete_defs)

declare semi_complete_onI [intro]
declare semi_complete_onE [elim]

declare complete_onI [intro]
declare complete_onE [elim]

declare CR_onI [intro]
declare CR_on_singletonI [intro]

declare CR_onD [dest]
declare CR_onE [elim]

lemma UNC_I:
  "(⋀a b. a ∈ NF A ⟹ b ∈ NF A ⟹ (a, b) ∈ A⇧^↔⇧^* ⟹ a = b) ⟹ UNC A"
  by (simp add: UNC_def)

lemma UNC_E:
  "⟦UNC A; a = b ⟹ P; a ∉ NF A ⟹ P; b ∉ NF A ⟹ P; (a, b) ∉ A⇧^↔⇧^* ⟹ P⟧ ⟹ P"
  unfolding UNC_def by blast

lemma UNF_onI: "(⋀a b c. a ∈ A ⟹ (a, b) ∈ r⇧^! ⟹ (a, c) ∈ r⇧^! ⟹ b = c) ⟹ UNF_on r A"
  by (simp add: UNF_defs)

lemma UNF_onE:
  "UNF_on r A ⟹ a ∈ A ⟹ (b = c ⟹ P) ⟹ ((a, b) ∉ r⇧^! ⟹ P) ⟹ ((a, c) ∉ r⇧^! ⟹ P) ⟹ P"
  unfolding UNF_on_def by blast

lemma UNF_onD:
  "UNF_on r A ⟹ a ∈ A ⟹ (a, b) ∈ r⇧^! ⟹ (a, c) ∈ r⇧^! ⟹ b = c"
  by (blast elim: UNF_onE)

declare UNF_onI [intro]
declare UNF_onD [dest]
declare UNF_onE [elim]

lemma SN_onI:
  assumes "⋀f. ⟦f 0 ∈ A; chain r f⟧ ⟹ False"
  shows "SN_on r A"
  using assms unfolding SN_defs by blast

lemma SN_I: "(⋀a. SN_on A {a}) ⟹ SN A"
  unfolding SN_on_def by blast

lemma SN_on_trancl_imp_SN_on:
  assumes "SN_on (R⇧⁺) T" shows "SN_on R T"
proof (rule ccontr)
  assume "¬ SN_on R T"
  then obtain s where "s 0 ∈ T" and "chain R s" unfolding SN_defs by auto
  then have "chain (R⇧⁺) s" by auto
  with ‹s 0 ∈ T› have "¬ SN_on (R⇧⁺) T" unfolding SN_defs by auto
  with assms show False by simp
qed

lemma SN_onE:
  assumes "SN_on r A"
    and "¬ (∃f. f 0 ∈ A ∧ chain r f) ⟹ P"
  shows "P"
  using assms unfolding SN_defs by simp

lemma not_SN_onE:
  assumes "¬ SN_on r A"
    and "⋀f. ⟦f 0 ∈ A; chain r f⟧ ⟹ P"
  shows "P"
  using assms unfolding SN_defs by blast

declare SN_onI [intro]
declare SN_onE [elim]
declare not_SN_onE [Pure.elim, elim]

lemma refl_not_SN: "(x, x) ∈ R ⟹ ¬ SN R"
  unfolding SN_defs by force

lemma SN_on_irrefl:
  assumes "SN_on r A"
  shows "∀a∈A. (a, a) ∉ r"
proof (intro ballI notI)
  fix a assume "a ∈ A" and "(a, a) ∈ r"
  with assms show False unfolding SN_defs by auto
qed

lemma WCR_onI: "(⋀a b c. a ∈ A ⟹ (a, b) ∈ r ⟹ (a, c) ∈ r ⟹ (b, c) ∈ join r) ⟹ WCR_on r A"
  by (simp add: WCR_defs)

lemma WCR_onE:
  "WCR_on r A ⟹ a ∈ A ⟹ ((b, c) ∈ join r ⟹ P) ⟹ ((a, b) ∉ r ⟹ P) ⟹ ((a, c) ∉ r ⟹ P) ⟹ P"
  unfolding WCR_on_def by blast

lemma SN_nat_bounded: "SN {(x, y :: nat). x < y ∧ y ≤ b}" (is "SN ?R")
proof 
  fix f
  assume "chain ?R f"
  then have steps: "⋀i. (f i, f (Suc i)) ∈ ?R" ..
  {
    fix i
    have inc: "f 0 + i ≤ f i"
    proof (induct i)
      case 0 then show ?case by auto
    next
      case (Suc i)
      have "f 0 + Suc i ≤ f i + Suc 0" using Suc by simp
      also have "... ≤ f (Suc i)" using steps [of i]
        by auto
      finally show ?case by simp
    qed
  }
  from this [of "Suc b"] steps [of b]
  show False by simp
qed

lemma WCR_onD:
  "WCR_on r A ⟹ a ∈ A ⟹ (a, b) ∈ r ⟹ (a, c) ∈ r ⟹ (b, c) ∈ join r"
  by (blast elim: WCR_onE)

lemma WN_onI: "(⋀a. a ∈ A ⟹ ∃b. (a, b) ∈ r⇧^!) ⟹ WN_on r A"
  by (auto simp: WN_defs)

lemma WN_onE: "WN_on r A ⟹ a ∈ A ⟹ (⋀b. (a, b) ∈ r⇧^! ⟹ P) ⟹ P"
 unfolding WN_defs by blast

lemma WN_onD: "WN_on r A ⟹ a ∈ A ⟹ ∃b. (a, b) ∈ r⇧^!"
  by (blast elim: WN_onE)

declare WCR_onI [intro]
declare WCR_onD [dest]
declare WCR_onE [elim]

declare WN_onI [intro]
declare WN_onD [dest]
declare WN_onE [elim]

text ‹Restricting a relation @{term r} to those elements that are strongly
normalizing with respect to a relation @{term s}.›
definition restrict_SN :: "'a rel ⇒ 'a rel ⇒ 'a rel" where
  "restrict_SN r s = {(a, b) | a b. (a, b) ∈ r ∧ SN_on s {a}}"

lemma SN_restrict_SN_idemp [simp]: "SN (restrict_SN A A)"
  by (auto simp: restrict_SN_def SN_defs)

lemma SN_on_Image:
  assumes "SN_on r A"
  shows "SN_on r (r `` A)"
proof
  fix f
  assume "f 0 ∈ r `` A" and chain: "chain r f"
  then obtain a where "a ∈ A" and 1: "(a, f 0) ∈ r" by auto
  let ?g = "case_nat a f"
  from cons_chain [OF 1 chain] have "chain r ?g" .
  moreover have "?g 0 ∈ A" by (simp add: ‹a ∈ A›)
  ultimately have "¬ SN_on r A" unfolding SN_defs by best
  with assms show False by simp
qed

lemma SN_on_subset2:
  assumes "A ⊆ B" and "SN_on r B"
  shows "SN_on r A"
  using assms unfolding SN_on_def by blast

lemma step_preserves_SN_on:
  assumes 1: "(a, b) ∈ r"
    and 2: "SN_on r {a}"
  shows "SN_on r {b}"
  using 1 and SN_on_Image [OF 2] and SN_on_subset2 [of "{b}" "r `` {a}"] by auto

lemma steps_preserve_SN_on: "(a, b) ∈ A⇧^* ⟹ SN_on A {a} ⟹ SN_on A {b}"
  by (induct rule: rtrancl.induct) (auto simp: step_preserves_SN_on)

(*FIXME: move*)
lemma relpow_seq:
  assumes "(x, y) ∈ r^^n"
  shows "∃f. f 0 = x ∧ f n = y ∧ (∀i<n. (f i, f (Suc i)) ∈ r)"
using assms
proof (induct n arbitrary: y)
  case 0 then show ?case by auto
next
  case (Suc n)
  then obtain z where "(x, z) ∈ r^^n" and "(z, y) ∈ r" by auto
  from Suc(1)[OF ‹(x, z) ∈ r^^n›]
    obtain f where "f 0 = x" and "f n = z" and seq: "∀i<n. (f i, f (Suc i)) ∈ r" by auto
  let ?n = "Suc n"
  let ?f = "λi. if i = ?n then y else f i"
  have "?f ?n = y" by simp
  from ‹f 0 = x› have "?f 0 = x" by simp
  from seq have seq': "∀i<n. (?f i, ?f (Suc i)) ∈ r" by auto
  with ‹f n = z› and ‹(z, y) ∈ r› have "∀i<?n. (?f i, ?f (Suc i)) ∈ r" by auto
  with ‹?f 0 = x› and ‹?f ?n = y› show ?case by best
qed

lemma rtrancl_imp_seq:
  assumes "(x, y) ∈ r⇧^*"
  shows "∃f n. f 0 = x ∧ f n = y ∧ (∀i<n. (f i, f (Suc i)) ∈ r)"
  using assms [unfolded rtrancl_power] and relpow_seq [of x y _ r] by blast

lemma SN_on_Image_rtrancl:
  assumes "SN_on r A"
  shows "SN_on r (r⇧^* `` A)"
proof
  fix f
  assume f0: "f 0 ∈ r⇧^* `` A" and chain: "chain r f"
  then obtain a where a: "a ∈ A" and "(a, f 0) ∈ r⇧^*" by auto
  then obtain n where "(a, f 0) ∈ r^^n" unfolding rtrancl_power by auto
  show False
  proof (cases n)
    case 0
    with ‹(a, f 0) ∈ r^^n› have "f 0 = a" by simp
    then have "f 0 ∈ A" by (simp add: a)
    with chain have "¬ SN_on r A" by auto
    with assms show False by simp
  next
    case (Suc m)
    from relpow_seq [OF ‹(a, f 0) ∈ r^^n›]
      obtain g where g0: "g 0 = a" and "g n = f 0"
      and gseq: "∀i<n. (g i, g (Suc i)) ∈ r" by auto
    let ?f = "λi. if i < n then g i else f (i - n)"
    have "chain r ?f"
    proof
      fix i
      {
        assume "Suc i < n"
        then have "(?f i, ?f (Suc i)) ∈ r" by (simp add: gseq)
      }
      moreover
      {
        assume "Suc i > n"
        then have eq: "Suc (i - n) = Suc i - n" by arith
        from chain have "(f (i - n), f (Suc (i - n))) ∈ r" by simp
        then have "(f (i - n), f (Suc i - n)) ∈ r" by (simp add: eq)
        with ‹Suc i > n› have "(?f i, ?f (Suc i)) ∈ r" by simp
      }
      moreover
      {
        assume "Suc i = n"
        then have eq: "f (Suc i - n) = g n" by (simp add: ‹g n = f 0›)
        from ‹Suc i = n› have eq': "i = n - 1" by arith
        from gseq have "(g i, f (Suc i - n)) ∈ r" unfolding eq by (simp add: Suc eq')
        then have "(?f i, ?f (Suc i)) ∈ r" using ‹Suc i = n› by simp
      }
      ultimately show "(?f i, ?f (Suc i)) ∈ r" by simp
    qed
    moreover have "?f 0 ∈ A"
    proof (cases n)
      case 0
      with ‹(a, f 0) ∈ r^^n› have eq: "a = f 0" by simp
      from a show ?thesis by (simp add: eq 0)
    next
      case (Suc m)
      then show ?thesis by (simp add: a g0)
    qed
    ultimately have "¬ SN_on r A" unfolding SN_defs by best
    with assms show False by simp
  qed
qed

(* FIXME: move somewhere else *)
declare subrelI [Pure.intro]

lemma restrict_SN_trancl_simp [simp]: "(restrict_SN A A)⇧⁺ = restrict_SN (A⇧⁺) A" (is "?lhs = ?rhs")
proof
  show "?lhs ⊆ ?rhs"
  proof
    fix a b assume "(a, b) ∈ ?lhs" then show "(a, b) ∈ ?rhs"
      unfolding restrict_SN_def by (induct rule: trancl.induct) auto
  qed
next
  show "?rhs ⊆ ?lhs"
  proof
    fix a b assume "(a, b) ∈ ?rhs"
    then have "(a, b) ∈ A⇧⁺" and "SN_on A {a}" unfolding restrict_SN_def by auto
    then show "(a, b) ∈ ?lhs"
    proof (induct rule: trancl.induct)
      case (r_into_trancl x y) then show ?case unfolding restrict_SN_def by auto
    next
      case (trancl_into_trancl a b c)
      then have IH: "(a, b) ∈ ?lhs" by auto
      from trancl_into_trancl have "(a, b) ∈ A⇧^*" by auto
      from this and ‹SN_on A {a}› have "SN_on A {b}" by (rule steps_preserve_SN_on)
      with ‹(b, c) ∈ A› have "(b, c) ∈ ?lhs" unfolding restrict_SN_def by auto
      with IH show ?case by simp
    qed
  qed
qed

lemma SN_imp_WN:
  assumes "SN A" shows "WN A"
proof -
  from ‹SN A› have "wf (A¯)" by (simp add: SN_defs wf_iff_no_infinite_down_chain)
  show "WN A"
  proof
    fix a
    show "∃b. (a, b) ∈ A⇧^!" unfolding normalizability_def NF_def Image_def
      by (rule wfE_min [OF ‹wf (A¯)›, of a "A⇧^* `` {a}", simplified])
         (auto intro: rtrancl_into_rtrancl)
  qed
qed

lemma UNC_imp_UNF:
 assumes "UNC r" shows "UNF r"
proof - {
  fix x y z assume "(x, y) ∈ r⇧^!" and "(x, z) ∈ r⇧^!"
  then have "(x, y) ∈ r⇧^*" and "(x, z) ∈ r⇧^*" and "y ∈ NF r" and "z ∈ NF r" by auto
  then have "(x, y) ∈ r⇧^↔⇧^*" and "(x, z) ∈ r⇧^↔⇧^*" by auto
  then have "(z, x) ∈ r⇧^↔⇧^*" using conversion_sym unfolding sym_def by best
  with ‹(x, y) ∈ r⇧^↔⇧^*› have "(z, y) ∈ r⇧^↔⇧^*" using conversion_trans unfolding trans_def by best
  from assms and this and ‹z ∈ NF r› and ‹y ∈ NF r› have "z = y" unfolding UNC_def by auto
} then show ?thesis by auto
qed

lemma join_NF_imp_eq:
 assumes "(x, y) ∈ r⇧^↓" and "x ∈ NF r" and "y ∈ NF r"
 shows "x = y"
proof -
  from ‹(x, y) ∈ r⇧^↓› obtain z where "(x, z)∈r⇧^*" and "(z, y)∈(r¯)⇧^*" unfolding join_def by auto
  then have "(y, z) ∈ r⇧^*" unfolding rtrancl_converse by simp
  from ‹x ∈ NF r› have "(x, z) ∉ r⇧⁺" using NF_no_trancl_step by best
  then have "x = z" using rtranclD [OF ‹(x, z) ∈ r⇧^*›] by auto
  from ‹y ∈ NF r› have "(y, z) ∉ r⇧⁺" using NF_no_trancl_step by best
  then have "y = z" using rtranclD [OF ‹(y, z) ∈ r⇧^*›] by auto
  with ‹x = z› show ?thesis by simp
qed

lemma rtrancl_Restr:
  assumes "(x, y) ∈ (Restr r A)⇧^*"
  shows "(x, y) ∈ r⇧^*"
  using assms by induct auto

lemma join_mono:
  assumes "r ⊆ s"
  shows "r⇧^↓ ⊆ s⇧^↓"
  using rtrancl_mono [OF assms] by (auto simp: join_def rtrancl_converse)


lemma CR_iff_meet_subset_join: "CR r = (r⇧^↑ ⊆ r⇧^↓)"
proof
 assume "CR r" show "r⇧^↑ ⊆ r⇧^↓"
 proof (rule subrelI)
  fix x y assume "(x, y) ∈ r⇧^↑"
  then obtain z where "(z, x) ∈ r⇧^*" and "(z, y) ∈ r⇧^*" using meetD by best
  with ‹CR r› show "(x, y) ∈ r⇧^↓" by (auto simp: CR_defs)
 qed
next
 assume "r⇧^↑ ⊆ r⇧^↓" {
  fix x y z assume "(x, y) ∈ r⇧^*" and "(x, z) ∈ r⇧^*"
  then have "(y, z) ∈ r⇧^↑" unfolding meet_def rtrancl_converse by auto
  with ‹r⇧^↑ ⊆ r⇧^↓› have "(y, z) ∈ r⇧^↓" by auto
 } then show "CR r" by (auto simp: CR_defs)
qed

lemma CR_divergence_imp_join:
  assumes "CR r" and "(x, y) ∈ r⇧^*" and "(x, z) ∈ r⇧^*"
  shows "(y, z) ∈ r⇧^↓"
using assms by auto

lemma join_imp_conversion: "r⇧^↓ ⊆ r⇧^↔⇧^*"
proof
  fix x z assume "(x, z) ∈ r⇧^↓"
  then obtain y where "(x, y) ∈ r⇧^*" and "(z, y) ∈ r⇧^*" by auto
  then have "(x, y) ∈ r⇧^↔⇧^*" and "(z, y) ∈ r⇧^↔⇧^*" by auto
  from ‹(z, y) ∈ r⇧^↔⇧^*› have "(y, z) ∈ r⇧^↔⇧^*" using conversion_sym unfolding sym_def by best
  with ‹(x, y) ∈ r⇧^↔⇧^*› show "(x, z) ∈ r⇧^↔⇧^*" using conversion_trans unfolding trans_def by best
qed

lemma meet_imp_conversion: "r⇧^↑ ⊆ r⇧^↔⇧^*"
proof (rule subrelI)
  fix y z assume "(y, z) ∈ r⇧^↑"
  then obtain x where "(x, y) ∈ r⇧^*" and "(x, z) ∈ r⇧^*" by auto
  then have "(x, y) ∈ r⇧^↔⇧^*" and "(x, z) ∈ r⇧^↔⇧^*" by auto
  from ‹(x, y) ∈ r⇧^↔⇧^*› have "(y, x) ∈ r⇧^↔⇧^*" using conversion_sym unfolding sym_def by best
  with ‹(x, z) ∈ r⇧^↔⇧^*› show "(y, z) ∈ r⇧^↔⇧^*" using conversion_trans unfolding trans_def by best
qed

lemma CR_imp_UNF:
  assumes "CR r" shows "UNF r"
proof - {
fix x y z assume "(x, y) ∈ r⇧^!" and "(x, z) ∈ r⇧^!"
  then have "(x, y) ∈ r⇧^*" and "y ∈ NF r" and "(x, z) ∈ r⇧^*" and "z ∈ NF r"
    unfolding normalizability_def by auto
  from assms and ‹(x, y) ∈ r⇧^*› and ‹(x, z) ∈ r⇧^*› have "(y, z) ∈ r⇧^↓"
    by (rule CR_divergence_imp_join)
  from this and ‹y ∈ NF r› and ‹z ∈ NF r› have "y = z" by (rule join_NF_imp_eq)
} then show ?thesis by auto
qed

lemma CR_iff_conversion_imp_join: "CR r = (r⇧^↔⇧^* ⊆ r⇧^↓)"
proof (intro iffI subrelI)
  fix x y assume "CR r" and "(x, y) ∈ r⇧^↔⇧^*"
  then obtain n where "(x, y) ∈ (r⇧^↔)^^n" unfolding conversion_def rtrancl_is_UN_relpow by auto
  then show "(x, y) ∈ r⇧^↓"
  proof (induct n arbitrary: x)
    case 0
    assume "(x, y) ∈ r⇧^↔ ^^ 0" then have "x = y" by simp
    show ?case unfolding ‹x = y› by auto
  next
    case (Suc n)
    from ‹(x, y) ∈ r⇧^↔ ^^ Suc n› obtain  z where "(x, z) ∈ r⇧^↔" and "(z, y) ∈ r⇧^↔ ^^ n"
      using relpow_Suc_D2 by best
    with Suc have "(z, y) ∈ r⇧^↓" by simp
    from ‹(x, z) ∈ r⇧^↔› show ?case
    proof
      assume "(x, z) ∈ r" with ‹(z, y) ∈ r⇧^↓› show ?thesis by (auto intro: rtrancl_join_join)
    next
      assume "(x, z) ∈ r¯"
      then have "(z, x) ∈ r⇧^*" by simp
      from ‹(z, y) ∈ r⇧^↓› obtain z' where "(z, z') ∈ r⇧^*" and "(y, z') ∈ r⇧^*" by auto
      from ‹CR r› and ‹(z, x) ∈ r⇧^*› and ‹(z, z') ∈ r⇧^*› have "(x, z') ∈ r⇧^↓"
        by (rule CR_divergence_imp_join)
      then obtain x' where "(x, x') ∈ r⇧^*" and "(z', x') ∈ r⇧^*" by auto
      with ‹(y, z') ∈ r⇧^*› show ?thesis by auto
    qed
  qed
next
  assume "r⇧^↔⇧^* ⊆ r⇧^↓" then show "CR r" unfolding CR_iff_meet_subset_join
    using meet_imp_conversion by auto
qed

lemma CR_imp_conversionIff_join:
  assumes "CR r" shows "r⇧^↔⇧^* = r⇧^↓"
proof
  show "r⇧^↔⇧^* ⊆ r⇧^↓" using CR_iff_conversion_imp_join assms by auto
next
  show "r⇧^↓ ⊆ r⇧^↔⇧^*" by (rule join_imp_conversion)
qed

lemma sym_join: "sym (join r)" by (auto simp: sym_def)

lemma join_sym: "(s, t) ∈ A⇧^↓ ⟹ (t, s) ∈ A⇧^↓" by auto

lemma CR_join_left_I:
  assumes "CR r" and "(x, y) ∈ r⇧^*" and "(x, z) ∈ r⇧^↓" shows "(y, z) ∈ r⇧^↓"
proof -
  from ‹(x, z) ∈ r⇧^↓› obtain x' where "(x, x') ∈ r⇧^*" and "(z, x') ∈ r⇧^↓" by auto
  from ‹CR r› and ‹(x, x') ∈ r⇧^*› and ‹(x, y) ∈ r⇧^*› have "(x, y) ∈ r⇧^↓" by auto
  then have "(y, x) ∈ r⇧^↓" using join_sym by best
  from ‹CR r› have "r⇧^↔⇧^* = r⇧^↓" by (rule CR_imp_conversionIff_join)
  from ‹(y, x) ∈ r⇧^↓› and ‹(x, z) ∈ r⇧^↓› show ?thesis using conversion_trans
    unfolding trans_def ‹r⇧^↔⇧^* = r⇧^↓› [symmetric] by best
qed

lemma CR_join_right_I:
 assumes "CR r" and "(x, y) ∈ r⇧^↓" and "(y, z) ∈ r⇧^*" shows "(x, z) ∈ r⇧^↓"
proof -
  have "r⇧^↔⇧^* = r⇧^↓" by (rule CR_imp_conversionIff_join [OF ‹CR r›])
  from ‹(y, z) ∈ r⇧^*› have "(y, z) ∈ r⇧^↔⇧^*" by auto
  with ‹(x, y) ∈ r⇧^↓› show ?thesis unfolding ‹r⇧^↔⇧^* = r⇧^↓› [symmetric] using conversion_trans
    unfolding trans_def by fast
qed

lemma NF_not_suc:
  assumes "(x, y) ∈ r⇧^*" and "x ∈ NF r" shows "x = y"
proof -
  from ‹x ∈ NF r› have "∀y. (x, y) ∉ r" using NF_no_step by auto
  then have "x ∉ Domain r" unfolding Domain_unfold by simp
  from ‹(x, y) ∈ r⇧^*› show ?thesis unfolding Not_Domain_rtrancl [OF ‹x ∉ Domain r›] by simp
qed

lemma semi_complete_imp_conversionIff_same_NF:
  assumes "semi_complete r"
  shows "((x, y) ∈ r⇧^↔⇧^*) = (∀u v. (x, u) ∈ r⇧^! ∧ (y, v) ∈ r⇧^! ⟶ u = v)"
proof -
  from assms have "WN r" and "CR r" unfolding semi_complete_defs by auto
  then have "r⇧^↔⇧^* = r⇧^↓" using CR_imp_conversionIff_join by auto
  show ?thesis
  proof
    assume "(x, y) ∈ r⇧^↔⇧^*"
    from ‹(x, y) ∈ r⇧^↔⇧^*› have "(x, y) ∈ r⇧^↓" unfolding ‹r⇧^↔⇧^* = r⇧^↓› .
    show "∀u v. (x, u) ∈ r⇧^! ∧ (y, v) ∈ r⇧^! ⟶ u = v"
    proof (intro allI impI, elim conjE)
      fix u v assume "(x, u) ∈ r⇧^!" and "(y, v) ∈ r⇧^!"
      then have "(x, u) ∈ r⇧^*" and "(y, v) ∈ r⇧^*" and "u ∈ NF r" and "v ∈ NF r" by auto
      from ‹CR r› and ‹(x, u) ∈ r⇧^*› and ‹(x, y) ∈ r⇧^↓› have "(u, y) ∈ r⇧^↓"
        by (auto intro: CR_join_left_I)
      then have "(y, u) ∈ r⇧^↓" using join_sym by best
      with ‹(x, y) ∈ r⇧^↓› have "(x, u) ∈ r⇧^↓" unfolding ‹r⇧^↔⇧^* = r⇧^↓› [symmetric]
        using conversion_trans unfolding trans_def by best
      from ‹CR r› and ‹(x, y) ∈ r⇧^↓› and ‹(y, v) ∈ r⇧^*› have "(x, v) ∈ r⇧^↓"
        by (auto intro: CR_join_right_I)
      then have "(v, x) ∈ r⇧^↓" using join_sym unfolding sym_def by best
      with ‹(x, u) ∈ r⇧^↓› have "(v, u) ∈ r⇧^↓" unfolding ‹r⇧^↔⇧^* = r⇧^↓› [symmetric]
        using conversion_trans unfolding trans_def by best
      then obtain v' where "(v, v') ∈ r⇧^*" and "(u, v') ∈ r⇧^*" by auto
      from ‹(u, v') ∈ r⇧^*› and ‹u ∈ NF r› have "u = v'" by (rule NF_not_suc)
      from ‹(v, v') ∈ r⇧^*› and ‹v ∈ NF r› have "v = v'" by (rule NF_not_suc)
      then show "u = v" unfolding ‹u = v'› by simp
    qed
  next
    assume equal_NF:"∀u v. (x, u) ∈ r⇧^! ∧ (y, v) ∈ r⇧^! ⟶ u = v"
    from ‹WN r› obtain u where "(x, u) ∈ r⇧^!" by auto
    from ‹WN r› obtain v where "(y, v) ∈ r⇧^!" by auto
    from ‹(x, u) ∈ r⇧^!› and ‹(y, v) ∈ r⇧^!› have "u = v" using equal_NF by simp
    from ‹(x, u) ∈ r⇧^!› and ‹(y, v) ∈ r⇧^!› have "(x, v) ∈ r⇧^*" and "(y, v) ∈ r⇧^*"
      unfolding ‹u = v› by auto
    then have "(x, v) ∈ r⇧^↔⇧^*" and "(y, v) ∈ r⇧^↔⇧^*" by auto
    from ‹(y, v) ∈ r⇧^↔⇧^*› have "(v, y) ∈ r⇧^↔⇧^*" using conversion_sym unfolding sym_def by best
    with ‹(x, v) ∈ r⇧^↔⇧^*› show "(x, y) ∈ r⇧^↔⇧^*" using conversion_trans unfolding trans_def by best
  qed
qed

lemma CR_imp_UNC:
  assumes "CR r" shows "UNC r"
proof - {
  fix x y assume "x ∈ NF r" and "y ∈ NF r" and "(x, y) ∈ r⇧^↔⇧^*"
  have "r⇧^↔⇧^* = r⇧^↓" by (rule CR_imp_conversionIff_join [OF assms])
  from ‹(x, y) ∈ r⇧^↔⇧^*› have "(x, y) ∈ r⇧^↓" unfolding ‹r⇧^↔⇧^* = r⇧^↓› by simp
  then obtain x' where "(x, x') ∈ r⇧^*" and "(y, x') ∈ r⇧^*" by best
  from ‹(x, x') ∈ r⇧^*› and ‹x ∈ NF r› have "x = x'" by (rule NF_not_suc)
  from ‹(y, x') ∈ r⇧^*› and ‹y ∈ NF r› have "y = x'" by (rule NF_not_suc)
  then have "x = y" unfolding ‹x = x'› by simp
} then show ?thesis by (auto simp: UNC_def)
qed

lemma WN_UNF_imp_CR:
  assumes "WN r" and "UNF r" shows "CR r"
proof - {
  fix x y z assume "(x, y) ∈ r⇧^*" and "(x, z) ∈ r⇧^*"
  from assms obtain y' where "(y, y') ∈ r⇧^!" unfolding WN_defs by best
  with ‹(x, y) ∈ r⇧^*› have "(x, y') ∈ r⇧^!" by auto
  from assms obtain z' where "(z, z') ∈ r⇧^!" unfolding WN_defs by best
  with ‹(x, z) ∈ r⇧^*› have "(x, z') ∈ r⇧^!" by auto
  with ‹(x, y') ∈ r⇧^!› have "y' = z'" using ‹UNF r› unfolding UNF_defs by auto
  from ‹(y, y') ∈ r⇧^!› and ‹(z, z') ∈ r⇧^!› have "(y, z) ∈ r⇧^↓" unfolding ‹y' = z'› by auto
} then show ?thesis by auto
qed

definition diamond :: "'a rel ⇒ bool" (‹◇›) where
  "◇ r ⟷ (r¯ O r) ⊆ (r O r¯)"

lemma diamond_I [intro]: "(r¯ O r) ⊆ (r O r¯) ⟹ ◇ r" unfolding diamond_def by simp

lemma diamond_E [elim]: "◇ r ⟹ ((r¯ O r) ⊆ (r O r¯) ⟹ P) ⟹ P"
  unfolding diamond_def by simp

lemma diamond_imp_semi_confluence:
  assumes "◇ r" shows "(r¯ O r⇧^*) ⊆ r⇧^↓"
proof (rule subrelI)
  fix y z assume "(y, z) ∈  r¯ O r⇧^*"
  then obtain x where "(x, y) ∈ r" and "(x, z) ∈ r⇧^*" by best
  then obtain n where "(x, z) ∈ r^^n" using rtrancl_imp_UN_relpow by best
  with ‹(x, y) ∈ r› show "(y, z) ∈ r⇧^↓"
  proof (induct n arbitrary: x z y)
    case 0 then show ?case by auto
  next
    case (Suc n)
    from ‹(x, z) ∈ r^^Suc n› obtain x' where "(x, x') ∈ r" and "(x', z) ∈ r^^n"
      using relpow_Suc_D2 by best
    with ‹(x, y) ∈ r› have "(y, x') ∈ (r¯ O r)" by auto
    with ‹◇ r› have "(y, x') ∈ (r O r¯)" by auto
    then obtain y' where "(x', y') ∈ r" and "(y, y') ∈ r" by best
    with Suc and ‹(x', z) ∈ r^^n› have "(y', z) ∈ r⇧^↓" by auto
    with ‹(y, y') ∈ r› show ?case by (auto intro: rtrancl_join_join)
  qed
qed

lemma semi_confluence_imp_CR:
  assumes "(r¯ O r⇧^*) ⊆ r⇧^↓" shows "CR r"
proof - {
  fix x y z assume "(x, y) ∈ r⇧^*" and "(x, z) ∈ r⇧^*"
  then obtain n where "(x, z) ∈ r^^n" using rtrancl_imp_UN_relpow by best
  with ‹(x, y) ∈ r⇧^*› have "(y, z) ∈ r⇧^↓"
  proof (induct n arbitrary: x y z)
    case 0 then show ?case by auto
  next
    case (Suc n)
    from ‹(x, z) ∈ r^^Suc n› obtain x' where "(x, x') ∈ r" and "(x', z) ∈ r^^n"
      using relpow_Suc_D2 by best
    from ‹(x, x') ∈ r› and ‹(x, y) ∈ r⇧^*› have "(x', y) ∈ (r¯ O r⇧^* )" by auto
    with assms have "(x', y) ∈ r⇧^↓" by auto
    then obtain y' where "(x', y') ∈ r⇧^*" and "(y, y') ∈ r⇧^*" by best
    with Suc and ‹(x', z) ∈ r^^n› have "(y', z) ∈ r⇧^↓" by simp
    then obtain u where "(z, u) ∈ r⇧^*" and "(y', u) ∈ r⇧^*" by best
    from ‹(y, y') ∈ r⇧^*› and ‹(y', u) ∈ r⇧^*› have "(y, u) ∈ r⇧^*" by auto
    with ‹(z, u) ∈ r⇧^*› show ?case by best
  qed
} then show ?thesis by auto
qed
 
lemma diamond_imp_CR:
  assumes "◇ r" shows "CR r"
  using assms by (rule diamond_imp_semi_confluence [THEN semi_confluence_imp_CR])

lemma diamond_imp_CR':
  assumes "◇ s" and "r ⊆ s" and "s ⊆ r⇧^*" shows "CR r"
  unfolding CR_iff_meet_subset_join
proof -
  from ‹◇ s› have "CR s" by (rule diamond_imp_CR)
  then have "s⇧^↑ ⊆ s⇧^↓" unfolding CR_iff_meet_subset_join by simp
  from ‹r ⊆ s› have "r⇧^* ⊆ s⇧^*" by (rule rtrancl_mono)
  from ‹s ⊆ r⇧^*› have "s⇧^* ⊆ (r⇧^*)⇧^*" by (rule rtrancl_mono)
  then have "s⇧^* ⊆ r⇧^*" by simp
  with ‹r⇧^* ⊆ s⇧^*› have "r⇧^* = s⇧^*" by simp
  show "r⇧^↑ ⊆ r⇧^↓" unfolding meet_def join_def rtrancl_converse ‹r⇧^* = s⇧^*›
    unfolding rtrancl_converse [symmetric] meet_def [symmetric]
      join_def [symmetric] by (rule ‹s⇧^↑ ⊆ s⇧^↓›)
qed

lemma SN_imp_minimal:
  assumes "SN A"
  shows "∀Q x. x ∈ Q ⟶ (∃z∈Q. ∀y. (z, y) ∈ A ⟶ y ∉ Q)"
proof (rule ccontr)
  assume "¬ (∀Q x. x ∈ Q ⟶ (∃z∈Q. ∀y. (z, y) ∈ A ⟶ y ∉ Q))"
  then obtain Q x where "x ∈ Q" and "∀z∈Q. ∃y. (z, y) ∈ A ∧ y ∈ Q" by auto
  then have "∀z. ∃y. z ∈ Q ⟶ (z, y) ∈ A ∧ y ∈ Q" by auto
  then have "∃f. ∀x. x ∈ Q ⟶ (x, f x) ∈ A ∧ f x ∈ Q" by (rule choice)
  then obtain f where a:"∀x. x ∈ Q ⟶ (x, f x) ∈ A ∧ f x ∈ Q" (is "∀x. ?P x") by best
  let ?S = "λi. (f ^^ i) x"
  have "?S 0 = x" by simp
  have "∀i. (?S i, ?S (Suc i)) ∈ A ∧ ?S (Suc i) ∈ Q"
  proof
    fix i show "(?S i, ?S (Suc i)) ∈ A ∧ ?S (Suc i) ∈ Q"
      by (induct i) (auto simp: ‹x ∈ Q› a)
  qed
  with ‹?S 0 = x› have "∃S. S 0 = x ∧ chain A S" by fast
  with assms show False by auto
qed

lemma SN_on_imp_on_minimal:
  assumes "SN_on r {x}"
  shows "∀Q. x ∈ Q ⟶ (∃z∈Q. ∀y. (z, y) ∈ r ⟶ y ∉ Q)"
proof (rule ccontr)
  assume "¬(∀Q. x ∈ Q ⟶ (∃z∈Q. ∀y. (z, y) ∈ r ⟶ y ∉ Q))"
  then obtain Q where "x ∈ Q" and "∀z∈Q. ∃y. (z, y) ∈ r ∧ y ∈ Q" by auto
  then have "∀z. ∃y. z ∈ Q ⟶ (z, y) ∈ r ∧ y ∈ Q" by auto
  then have "∃f. ∀x. x ∈ Q ⟶ (x, f x) ∈ r ∧ f x ∈ Q" by (rule choice)
  then obtain f where a: "∀x. x ∈ Q ⟶ (x, f x) ∈ r ∧ f x ∈ Q" (is "∀x. ?P x") by best
  let ?S = "λi. (f ^^ i) x"
  have "?S 0 = x" by simp
  have "∀i. (?S i,?S(Suc i)) ∈ r ∧ ?S(Suc i) ∈ Q"
  proof
    fix i show "(?S i,?S(Suc i)) ∈ r ∧ ?S(Suc i) ∈ Q" by (induct i) (auto simp:‹x ∈ Q› a)
  qed
  with ‹?S 0 = x› have "∃S. S 0 = x ∧ chain r S" by fast
  with assms show False by auto
qed

lemma minimal_imp_wf:
  assumes "∀Q x. x ∈ Q ⟶ (∃z∈Q. ∀y. (z, y) ∈ r ⟶ y ∉ Q)"
  shows "wf(r¯)"
proof (rule ccontr)
  assume "¬ wf(r¯)"
  then have "∃P. (∀x. (∀y. (x, y) ∈ r ⟶ P y) ⟶ P x) ∧ (∃x. ¬ P x)" unfolding wf_def by simp
  then obtain P x where suc:"∀x. (∀y. (x, y) ∈ r ⟶ P y) ⟶ P x" and "¬ P x" by auto
  let ?Q = "{x. ¬ P x}"
  from ‹¬ P x› have "x ∈ ?Q" by simp
  from assms have "∀x. x ∈ ?Q ⟶ (∃z∈?Q. ∀y. (z, y) ∈ r ⟶ y ∉ ?Q)" by (rule allE [where x = ?Q])
  with ‹x ∈ ?Q› obtain z where "z ∈ ?Q" and min:" ∀y. (z, y) ∈ r ⟶ y ∉ ?Q" by best
  from ‹z ∈ ?Q› have "¬ P z" by simp
  with suc obtain y where "(z, y) ∈ r" and "¬ P y" by best
  then have "y ∈ ?Q" by simp
  with ‹(z, y) ∈ r› and min show False by simp
qed

lemmas SN_imp_wf = SN_imp_minimal [THEN minimal_imp_wf]

lemma wf_imp_SN:
  assumes "wf (A¯)" shows "SN A"
proof - {
  fix a
  let ?P = "λa. ¬(∃S. S 0 = a ∧ chain A S)"
  from ‹wf (A¯)› have "?P a"
  proof induct
    case (less a)
    then have IH: "⋀b. (a, b) ∈ A ⟹ ?P b" by auto
    show "?P a"
    proof (rule ccontr)
      assume "¬ ?P a"
      then obtain S where "S 0 = a" and "chain A S" by auto
      then have "(S 0, S 1) ∈ A" by auto
      with IH have "?P (S 1)" unfolding ‹S 0 = a› by auto
      with ‹chain A S› show False by auto
    qed
  qed
  then have "SN_on A {a}" unfolding SN_defs by auto
} then show ?thesis by fast
qed

lemma SN_nat_gt: "SN {(a, b :: nat) . a > b}"
proof -
  from wf_less have "wf ({(x, y) . (x :: nat) > y}¯)" unfolding converse_unfold by auto
  from wf_imp_SN [OF this] show ?thesis .
qed


lemma SN_iff_wf: "SN A = wf (A¯)" by (auto simp: SN_imp_wf wf_imp_SN)

lemma SN_imp_acyclic: "SN R ⟹ acyclic R"
  using wf_acyclic [of "R¯", unfolded SN_iff_wf [symmetric]] by auto

lemma SN_induct:
  assumes sn: "SN r" and step: "⋀a. (⋀b. (a, b) ∈ r ⟹ P b) ⟹ P a"
  shows "P a"
using sn unfolding SN_iff_wf proof induct
  case (less a)
  with step show ?case by best
qed

(* The same as well-founded induction, but in the 'correct' direction. *)
lemmas SN_induct_rule = SN_induct [consumes 1, case_names IH, induct pred: SN]

lemma SN_on_induct [consumes 2, case_names IH, induct pred: SN_on]:
  assumes SN: "SN_on R A"
    and "s ∈ A"
    and imp: "⋀t. (⋀u. (t, u) ∈ R ⟹ P u) ⟹ P t"
  shows "P s"
proof -
  let ?R = "restrict_SN R R"
  let ?P = "λt. SN_on R {t} ⟶ P t"
  have "SN_on R {s} ⟶ P s"
  proof (rule SN_induct [OF SN_restrict_SN_idemp [of R], of ?P])
    fix a
    assume ind: "⋀b. (a, b) ∈ ?R ⟹ SN_on R {b} ⟶ P b"
    show "SN_on R {a} ⟶ P a"
    proof
      assume SN: "SN_on R {a}"
      show "P a"
      proof (rule imp)
        fix b
        assume "(a, b) ∈ R"
        with SN step_preserves_SN_on [OF this SN]
        show "P b" using ind [of b] unfolding restrict_SN_def by auto
      qed
    qed
  qed
  with SN show "P s" using ‹s ∈ A› unfolding SN_on_def by blast
qed

(* link SN_on to acc / accp *)
lemma accp_imp_SN_on:
  assumes "⋀x. x ∈ A ⟹ Wellfounded.accp g x"
  shows "SN_on {(y, z). g z y} A"
proof - {
  fix x assume "x ∈ A"
  from assms [OF this]
  have "SN_on {(y, z). g z y} {x}"
  proof (induct rule: accp.induct)
    case (accI x)
    show ?case
    proof
      fix f
      assume x: "f 0 ∈ {x}" and steps: "∀ i. (f i, f (Suc i)) ∈ {a. (λ(y, z). g z y) a}"
      then have "g (f 1) x" by auto
      from accI(2)[OF this] steps x show False unfolding SN_on_def by auto
    qed
  qed
  }
  then show ?thesis unfolding SN_on_def by blast
qed

lemma SN_on_imp_accp:
  assumes "SN_on {(y, z). g z y} A"
  shows "∀x∈A. Wellfounded.accp g x"
proof
  fix x assume "x ∈ A"
  with assms show "Wellfounded.accp g x"
  proof (induct rule: SN_on_induct)
    case (IH x)
    show ?case
    proof
      fix y
      assume "g y x"
      with IH show "Wellfounded.accp g y" by simp
    qed
  qed
qed

lemma SN_on_conv_accp:
  "SN_on {(y, z). g z y} {x} = Wellfounded.accp g x"
  using SN_on_imp_accp [of g "{x}"]
        accp_imp_SN_on [of "{x}" g]
  by auto

lemma SN_on_conv_acc: "SN_on {(y, z). (z, y) ∈ r} {x} ⟷ x ∈ Wellfounded.acc r"
  unfolding SN_on_conv_accp accp_acc_eq ..

lemma acc_imp_SN_on:
  assumes "x ∈ Wellfounded.acc r" shows "SN_on {(y, z). (z, y) ∈ r} {x}"
  using assms unfolding SN_on_conv_acc by simp

lemma SN_on_imp_acc:
  assumes "SN_on {(y, z). (z, y) ∈ r} {x}" shows "x ∈ Wellfounded.acc r"
  using assms unfolding SN_on_conv_acc by simp


subsection ‹Newman's Lemma›

lemma rtrancl_len_E [elim]:
  assumes "(x, y) ∈ r⇧^*" obtains n where "(x, y) ∈ r^^n"
  using rtrancl_imp_UN_relpow [OF assms] by best

lemma relpow_Suc_E2' [elim]:
  assumes "(x, z) ∈ A^^Suc n" obtains y where "(x, y) ∈ A" and "(y, z) ∈ A⇧^*"
proof -
  assume assm: "⋀y. (x, y) ∈ A ⟹ (y, z) ∈ A⇧^* ⟹ thesis"
  from relpow_Suc_E2 [OF assms] obtain y where "(x, y) ∈ A" and "(y, z) ∈ A^^n" by auto
  then have "(y, z) ∈ A⇧^*" using (*FIXME*) relpow_imp_rtrancl by auto
  from assm [OF ‹(x, y) ∈ A› this] show thesis .
qed

lemmas SN_on_induct' [consumes 1, case_names IH] = SN_on_induct [OF _ singletonI]

lemma Newman_local:
  assumes "SN_on r X" and WCR: "WCR_on r {x. SN_on r {x}}"
  shows "CR_on r X"
proof - {
  fix x
  assume "x ∈ X"
  with assms have "SN_on r {x}" unfolding SN_on_def by auto
  with this  have "CR_on r {x}"
  proof (induct rule: SN_on_induct')
    case (IH x) show ?case
    proof
      fix y z assume "(x, y) ∈ r⇧^*" and "(x, z) ∈ r⇧^*"
      from ‹(x, y) ∈ r⇧^*› obtain m where "(x, y) ∈ r^^m" ..
      from ‹(x, z) ∈ r⇧^*› obtain n where "(x, z) ∈ r^^n" ..
      show "(y, z) ∈ r⇧^↓"
      proof (cases n)
        case 0
        from ‹(x, z) ∈ r^^n› have eq: "x = z" by (simp add: 0)
        from ‹(x, y) ∈ r⇧^*› show ?thesis unfolding eq ..
      next
        case (Suc n')
        from ‹(x, z) ∈ r^^n› [unfolded Suc] obtain t where "(x, t) ∈ r" and "(t, z) ∈ r⇧^*" ..
        show ?thesis
        proof (cases m)
          case 0
          from ‹(x, y) ∈ r^^m› have eq: "x = y" by (simp add: 0)
          from ‹(x, z) ∈ r⇧^*› show ?thesis unfolding eq ..
        next
          case (Suc m')
          from ‹(x, y) ∈ r^^m› [unfolded Suc] obtain s where "(x, s) ∈ r" and "(s, y) ∈ r⇧^*" ..          
          from WCR IH(2) have "WCR_on r {x}" unfolding WCR_on_def by auto
          with ‹(x, s) ∈ r› and ‹(x, t) ∈ r› have "(s, t) ∈ r⇧^↓" by auto
          then obtain u where "(s, u) ∈ r⇧^*" and "(t, u) ∈ r⇧^*" ..
          from ‹(x, s) ∈ r› IH(2) have "SN_on r {s}" by (rule step_preserves_SN_on)
          from IH(1)[OF ‹(x, s) ∈ r› this] have "CR_on r {s}" .
          from this and ‹(s, u) ∈ r⇧^*› and ‹(s, y) ∈ r⇧^*› have "(u, y) ∈ r⇧^↓" by auto
          then obtain v where "(u, v) ∈ r⇧^*" and "(y, v) ∈ r⇧^*" ..
          from ‹(x, t) ∈ r› IH(2) have "SN_on r {t}" by (rule step_preserves_SN_on)
          from IH(1)[OF ‹(x, t) ∈ r› this] have "CR_on r {t}" .
          moreover from ‹(t, u) ∈ r⇧^*› and ‹(u, v) ∈ r⇧^*› have "(t, v) ∈ r⇧^*" by auto
          ultimately have "(z, v) ∈ r⇧^↓" using ‹(t, z) ∈ r⇧^*› by auto
          then obtain w where "(z, w) ∈ r⇧^*" and "(v, w) ∈ r⇧^*" ..
          from ‹(y, v) ∈ r⇧^*› and ‹(v, w) ∈ r⇧^*› have "(y, w) ∈ r⇧^*" by auto
          with ‹(z, w) ∈ r⇧^*› show ?thesis by auto
        qed
      qed
    qed
  qed
  }
  then show ?thesis unfolding CR_on_def by blast
qed

lemma Newman: "SN r ⟹ WCR r ⟹ CR r"
  using Newman_local [of r UNIV]
  unfolding WCR_on_def by auto
  
lemma Image_SN_on:
  assumes "SN_on r (r `` A)"
  shows "SN_on r A"
proof
  fix f
  assume "f 0 ∈ A" and chain: "chain r f"
  then have "f (Suc 0) ∈ r `` A" by auto
  with assms have "SN_on r {f (Suc 0)}" by (auto simp add: ‹f 0 ∈ A› SN_defs)
  moreover have "¬ SN_on r {f (Suc 0)}"
  proof -
    have "f (Suc 0) ∈ {f (Suc 0)}" by simp
    moreover from chain have "chain r (f ∘ Suc)" by auto
    ultimately show ?thesis by auto
  qed
  ultimately show False by simp
qed

lemma SN_on_Image_conv: "SN_on r (r `` A) = SN_on r A"
  using SN_on_Image and Image_SN_on by blast

text ‹If all successors are terminating, then the current element is also terminating.›
lemma step_reflects_SN_on:
  assumes "(⋀b. (a, b) ∈ r ⟹ SN_on r {b})"
  shows "SN_on r {a}"
  using assms and Image_SN_on [of r "{a}"] by (auto simp: SN_defs)

lemma SN_on_all_reducts_SN_on_conv:
  "SN_on r {a} = (∀b. (a, b) ∈ r ⟶ SN_on r {b})"
  using SN_on_Image_conv [of r "{a}"] by (auto simp: SN_defs)

lemma SN_imp_SN_trancl: "SN R ⟹ SN (R⇧⁺)"
  unfolding SN_iff_wf by (rule wf_converse_trancl)

lemma SN_trancl_imp_SN:
  assumes "SN (R⇧⁺)" shows "SN R"
  using assms by (rule SN_on_trancl_imp_SN_on)

lemma SN_trancl_SN_conv: "SN (R⇧⁺) = SN R"
  using SN_trancl_imp_SN [of R] SN_imp_SN_trancl [of R] by blast

lemma SN_inv_image: "SN R ⟹ SN (inv_image R f)" unfolding SN_iff_wf by simp

lemma SN_subset: "SN R ⟹ R' ⊆ R ⟹ SN R'" unfolding SN_defs by blast
 
lemma SN_pow_imp_SN:
  assumes "SN (A^^Suc n)" shows "SN A"
proof (rule ccontr)
  assume "¬ SN A"
  then obtain S where "chain A S" unfolding SN_defs by auto
  from chain_imp_relpow [OF this]
    have step: "⋀i. (S i, S (i + (Suc n))) ∈ A^^Suc n" .
  let ?T = "λi. S (i * (Suc n))"
  have "chain (A^^Suc n) ?T"
  proof
    fix i show "(?T i, ?T (Suc i)) ∈ A^^Suc n" unfolding mult_Suc
      using step [of "i * Suc n"] by (simp only: add.commute)
  qed
  then have "¬ SN (A^^Suc n)" unfolding SN_defs by fast
  with assms show False by simp
qed

(* TODO: move to Isabelle Library? *)
lemma pow_Suc_subset_trancl: "R^^(Suc n) ⊆ R⇧⁺"
  using trancl_power [of _ R] by blast

lemma SN_imp_SN_pow:
  assumes "SN R" shows "SN (R^^Suc n)"
  using SN_subset [where R="R⇧⁺", OF SN_imp_SN_trancl [OF assms] pow_Suc_subset_trancl] by simp
  
(*FIXME: needed in HOL/Wellfounded.thy*)
lemma SN_pow: "SN R ⟷ SN (R ^^ Suc n)"
  by (rule iffI, rule SN_imp_SN_pow, assumption, rule SN_pow_imp_SN, assumption)

lemma SN_on_trancl:
  assumes "SN_on r A" shows "SN_on (r⇧⁺) A"
using assms
proof (rule contrapos_pp)
  let ?r = "restrict_SN r r"
  assume "¬ SN_on (r⇧⁺) A"
  then obtain f where "f 0 ∈ A" and chain: "chain (r⇧⁺) f" by auto
  have "SN ?r" by (rule SN_restrict_SN_idemp)
  then have "SN (?r⇧⁺)" by (rule SN_imp_SN_trancl)
  have "∀i. (f 0, f i) ∈ r⇧^*"
  proof
    fix i show "(f 0, f i) ∈ r⇧^*"
    proof (induct i)
      case 0 show ?case ..
    next
      case (Suc i)
      from chain have "(f i, f (Suc i)) ∈ r⇧⁺" ..
      with Suc show ?case by auto
    qed
  qed
  with assms have "∀i. SN_on r {f i}"
    using steps_preserve_SN_on [of "f 0" _ r]
    and ‹f 0 ∈ A›
    and SN_on_subset2 [of "{f 0}" "A"] by auto
  with chain have "chain (?r⇧⁺) f"
    unfolding restrict_SN_trancl_simp
    unfolding restrict_SN_def by auto
  then have "¬ SN_on (?r⇧⁺) {f 0}" by auto
  with ‹SN (?r⇧⁺)› have False by (simp add: SN_defs)
  then show "¬ SN_on r A" by simp
qed

lemma SN_on_trancl_SN_on_conv: "SN_on (R⇧⁺) T = SN_on R T"
  using SN_on_trancl_imp_SN_on [of R] SN_on_trancl [of R] by blast


text ‹Restrict an ARS to elements of a given set.›
definition "restrict" :: "'a rel ⇒ 'a set ⇒ 'a rel" where
  "restrict r S = {(x, y). x ∈ S ∧ y ∈ S ∧ (x, y) ∈ r}"

lemma SN_on_restrict:
  assumes "SN_on r A"
  shows "SN_on (restrict r S) A" (is "SN_on ?r A")
proof (rule ccontr)
  assume "¬ SN_on ?r A"
  then have "∃f. f 0 ∈ A ∧ chain ?r f" by auto
  then have "∃f. f 0 ∈ A ∧ chain r f" unfolding restrict_def by auto
  with ‹SN_on r A› show False by auto
qed

lemma restrict_rtrancl: "(restrict r S)⇧^* ⊆ r⇧^*" (is "?r⇧^* ⊆ r⇧^*")
proof - {
  fix x y assume "(x, y) ∈ ?r⇧^*" then have "(x, y) ∈ r⇧^*" unfolding restrict_def by induct auto
} then show ?thesis by auto
qed

lemma rtrancl_Image_step:
  assumes "a ∈ r⇧^* `` A"
    and "(a, b) ∈ r⇧^*"
  shows "b ∈ r⇧^* `` A"
proof -
  from assms(1) obtain c where "c ∈ A" and "(c, a) ∈ r⇧^*" by auto
  with assms have "(c, b) ∈ r⇧^*" by auto
  with ‹c ∈ A› show ?thesis by auto
qed

lemma WCR_SN_on_imp_CR_on:
  assumes "WCR r" and "SN_on r A" shows "CR_on r A"
proof -
  let ?S = "r⇧^* `` A"
  let ?r = "restrict r ?S"
  have "∀x. SN_on ?r {x}"
  proof
    fix y have "y ∉ ?S ∨ y ∈ ?S" by simp
    then show "SN_on ?r {y}"
    proof
      assume "y ∉ ?S" then show ?thesis unfolding restrict_def by auto
    next
      assume "y ∈ ?S"
      then have "y ∈ r⇧^* `` A" by simp
      with SN_on_Image_rtrancl [OF ‹SN_on r A›]
        have "SN_on r {y}" using SN_on_subset2 [of "{y}" "r⇧^* `` A"] by blast
      then show ?thesis by (rule SN_on_restrict)
    qed
  qed
  then have "SN ?r" unfolding SN_defs by auto
  {
    fix x y assume "(x, y) ∈ r⇧^*" and "x ∈ ?S" and "y ∈ ?S"
    then obtain n where "(x, y) ∈ r^^n" and "x ∈ ?S" and "y ∈ ?S"
      using rtrancl_imp_UN_relpow by best
    then have "(x, y) ∈ ?r⇧^*"
    proof (induct n arbitrary: x y)
      case 0 then show ?case by simp
    next
      case (Suc n)
      from ‹(x, y) ∈ r^^Suc n› obtain x' where "(x, x') ∈ r" and "(x', y) ∈ r^^n"
        using relpow_Suc_D2 by best
      then have "(x, x') ∈ r⇧^*" by simp
      with ‹x ∈ ?S› have "x' ∈ ?S" by (rule rtrancl_Image_step)
      with Suc and ‹(x', y) ∈ r^^n› have "(x', y) ∈ ?r⇧^*" by simp
      from ‹(x, x') ∈ r› and ‹x ∈ ?S› and ‹x' ∈ ?S› have "(x, x') ∈ ?r"
        unfolding restrict_def by simp
      with ‹(x', y) ∈ ?r⇧^*› show ?case by simp
    qed
  }
  then have a:"∀x y. (x, y) ∈ r⇧^* ∧ x ∈ ?S ∧ y ∈ ?S ⟶ (x, y) ∈ ?r⇧^*" by simp
  {
    fix x' y z assume "(x', y) ∈ ?r" and "(x', z) ∈ ?r"
    then have "x' ∈ ?S" and "y ∈ ?S" and "z ∈ ?S" and "(x', y) ∈ r" and "(x', z) ∈ r"
      unfolding restrict_def by auto
    with ‹WCR r› have "(y, z) ∈ r⇧^↓" by auto
    then obtain u where "(y, u) ∈ r⇧^*" and "(z, u) ∈ r⇧^*" by auto
    from ‹x' ∈ ?S› obtain x where "x ∈ A" and "(x, x') ∈ r⇧^*" by auto
    from ‹(x', y) ∈ r› have "(x', y) ∈ r⇧^*" by auto
    with ‹(y, u) ∈ r⇧^*› have "(x', u) ∈ r⇧^*" by auto
    with ‹(x, x') ∈ r⇧^*› have "(x, u) ∈ r⇧^*" by simp
    then have "u ∈ ?S" using ‹x ∈ A› by auto
    from ‹y ∈ ?S› and ‹u ∈ ?S› and ‹(y, u) ∈ r⇧^*› have "(y, u) ∈ ?r⇧^*" using a by auto
    from ‹z ∈ ?S› and ‹u ∈ ?S› and ‹(z, u) ∈ r⇧^*› have "(z, u) ∈ ?r⇧^*" using a by auto
    with ‹(y, u) ∈ ?r⇧^*› have "(y, z) ∈ ?r⇧^↓" by auto
  }
  then have "WCR ?r" by auto
  have "CR ?r" using Newman [OF ‹SN ?r› ‹WCR ?r›] by simp
  {
    fix x y z assume "x ∈ A" and "(x, y) ∈ r⇧^*" and "(x, z) ∈ r⇧^*"
    then have "y ∈ ?S" and "z ∈ ?S" by auto
    have "x ∈ ?S" using ‹x ∈ A› by auto
    from a and ‹(x, y) ∈ r⇧^*› and ‹x ∈ ?S› and ‹y ∈ ?S› have "(x, y) ∈ ?r⇧^*" by simp
    from a and ‹(x, z) ∈ r⇧^*› and ‹x ∈ ?S› and ‹z ∈ ?S› have "(x, z) ∈ ?r⇧^*" by simp
    with ‹CR ?r› and ‹(x, y) ∈ ?r⇧^*› have "(y, z) ∈ ?r⇧^↓" by auto
    then obtain u where "(y, u) ∈ ?r⇧^*" and "(z, u) ∈ ?r⇧^*" by best
    then have "(y, u) ∈ r⇧^*" and "(z, u) ∈ r⇧^*" using restrict_rtrancl by auto
    then have "(y, z) ∈ r⇧^↓" by auto
  }
  then show ?thesis by auto
qed

lemma SN_on_Image_normalizable:
  assumes "SN_on r A"
  shows "∀a∈A. ∃b. b ∈ r⇧^! `` A"
proof
  fix a assume a: "a ∈ A"
  show "∃b. b ∈ r⇧^! `` A"
  proof (rule ccontr)
    assume "¬ (∃b. b ∈ r⇧^! `` A)"
    then have A: "∀b. (a, b) ∈ r⇧^* ⟶ b ∉ NF r" using a by auto
    then have "a ∉ NF r" by auto
    let ?Q = "{c. (a, c) ∈ r⇧^* ∧ c ∉ NF r}"
    have "a ∈ ?Q" using ‹a ∉ NF r› by simp
    have "∀c∈?Q. ∃b. (c, b) ∈ r ∧ b ∈ ?Q"
    proof
      fix c
      assume "c ∈ ?Q"
      then have "(a, c) ∈ r⇧^*" and "c ∉ NF r" by auto
      then obtain d where "(c, d) ∈ r" by auto
      with ‹(a, c) ∈ r⇧^*› have "(a, d) ∈ r⇧^*" by simp
      with A have "d ∉ NF r" by simp
      with ‹(c, d) ∈ r› and ‹(a, c) ∈ r⇧^*›
        show "∃b. (c, b) ∈ r ∧ b ∈ ?Q" by auto
    qed
    with ‹a ∈ ?Q› have "a ∈ ?Q ∧ (∀c∈?Q. ∃b. (c, b) ∈ r ∧ b ∈ ?Q)" by auto
    then have "∃Q. a ∈ Q ∧ (∀c∈Q. ∃b. (c, b) ∈ r ∧ b ∈ Q)" by (rule exI [of _ "?Q"])
    then have "¬ (∀Q. a ∈ Q ⟶ (∃c∈Q. ∀b. (c, b) ∈ r ⟶ b ∉ Q))" by simp
    with SN_on_imp_on_minimal [of r a] have "¬ SN_on r {a}" by blast
    with assms and ‹a ∈ A› and SN_on_subset2 [of "{a}" A r] show False by simp
  qed
qed

lemma SN_on_imp_normalizability:
  assumes "SN_on r {a}" shows "∃b. (a, b) ∈ r⇧^!"
  using SN_on_Image_normalizable [OF assms] by auto


subsection ‹Commutation›

definition commute :: "'a rel ⇒ 'a rel ⇒ bool" where
  "commute r s ⟷ ((r¯)⇧^* O s⇧^*) ⊆ (s⇧^* O (r¯)⇧^*)"

lemma CR_iff_self_commute: "CR r = commute r r"
  unfolding commute_def CR_iff_meet_subset_join meet_def join_def
  by simp

(* FIXME: move somewhere else *)
lemma rtrancl_imp_rtrancl_UN: 
  assumes "(x, y) ∈ r⇧^*" and "r ∈ I"
  shows "(x, y) ∈ (⋃r∈I. r)⇧^*" (is "(x, y) ∈ ?r⇧^*")
using assms proof induct
  case base then show ?case by simp
next
  case (step y z)
  then have "(x, y) ∈ ?r⇧^*" by simp
  from ‹(y, z) ∈ r› and ‹r ∈ I› have "(y, z) ∈ ?r⇧^*" by auto
  with ‹(x, y) ∈ ?r⇧^*› show ?case by auto
qed

definition quasi_commute :: "'a rel ⇒ 'a rel ⇒ bool" where
  "quasi_commute r s ⟷ (s O r) ⊆ r O (r ∪ s)⇧^*"

lemma rtrancl_union_subset_rtrancl_union_trancl: "(r ∪ s⇧⁺)⇧^* = (r ∪ s)⇧^*"
proof
  show "(r ∪ s⇧⁺)⇧^* ⊆ (r ∪ s)⇧^*"
  proof (rule subrelI)
    fix x y assume "(x, y) ∈ (r ∪ s⇧⁺)⇧^*"
    then show "(x, y) ∈ (r ∪ s)⇧^*"
    proof (induct)
      case base then show ?case by auto
    next
      case (step y z)
      then have "(y, z) ∈ r ∨ (y, z) ∈ s⇧⁺" by auto
      then have "(y, z) ∈ (r ∪ s)⇧^*"
      proof
        assume "(y, z) ∈ r" then show ?thesis by auto
      next
        assume "(y, z) ∈ s⇧⁺"
        then have "(y, z) ∈ s⇧^*" by auto
        then have "(y, z) ∈ r⇧^* ∪ s⇧^*" by auto
        then show ?thesis using rtrancl_Un_subset by auto
      qed
      with ‹(x, y) ∈ (r ∪ s)⇧^*› show ?case by simp
    qed
  qed
next
  show "(r ∪ s)⇧^* ⊆ (r ∪ s⇧⁺)⇧^*"
  proof (rule subrelI)
    fix x y assume "(x, y) ∈ (r ∪ s)⇧^*"
    then show "(x, y) ∈ (r ∪ s⇧⁺)⇧^*"
    proof (induct)
      case base then show ?case by auto
    next
      case (step y z)
      then have "(y, z) ∈ (r ∪ s⇧⁺)⇧^*" by auto
      with ‹(x, y) ∈ (r ∪ s⇧⁺)⇧^*› show ?case by auto
    qed
  qed
qed

lemma qc_imp_qc_trancl:
  assumes "quasi_commute r s" shows "quasi_commute r (s⇧⁺)"
unfolding quasi_commute_def
proof (rule subrelI)
  fix x z assume "(x, z) ∈ s⇧⁺ O r"
  then obtain y where "(x, y) ∈ s⇧⁺" and "(y, z) ∈ r" by best
  then show "(x, z) ∈ r O (r ∪ s⇧⁺)⇧^*"
  proof (induct arbitrary: z)
    case (base y)
    then have "(x, z) ∈ (s O r)" by auto
    with assms have "(x, z) ∈ r O (r ∪ s)⇧^*" unfolding quasi_commute_def by auto
    then show ?case using rtrancl_union_subset_rtrancl_union_trancl by auto
  next
    case (step a b)
    then have "(a, z) ∈ (s O r)" by auto
    with assms have "(a, z) ∈ r O (r ∪ s)⇧^*" unfolding quasi_commute_def by auto
    then obtain u where "(a, u) ∈ r" and "(u, z) ∈ (r ∪ s)⇧^*" by best
    then have "(u, z) ∈ (r ∪ s⇧⁺)⇧^*" using rtrancl_union_subset_rtrancl_union_trancl by auto
    from ‹(a, u) ∈ r› and step have "(x, u) ∈ r O (r ∪ s⇧⁺)⇧^*" by auto
    then obtain v where "(x, v) ∈ r" and "(v, u) ∈ (r ∪ s⇧⁺)⇧^*" by best
    with ‹(u, z) ∈ (r ∪ s⇧⁺)⇧^*› have "(v, z) ∈ (r ∪ s⇧⁺)⇧^*" by auto
    with ‹(x, v) ∈ r› show ?case by auto
  qed
qed

lemma steps_reflect_SN_on:
  assumes "¬ SN_on r {b}" and "(a, b) ∈ r⇧^*"
  shows "¬ SN_on r {a}"
  using SN_on_Image_rtrancl [of r "{a}"]
  and assms and SN_on_subset2 [of "{b}" "r⇧^* `` {a}" r] by blast

lemma chain_imp_not_SN_on:
   assumes "chain r f"
   shows "¬ SN_on r {f i}"
proof -
  let ?f = "λj. f (i + j)"
  have "?f 0 ∈ {f i}" by simp
  moreover have "chain r ?f" using assms by auto
  ultimately have "?f 0 ∈ {f i} ∧ chain r ?f" by blast
  then have "∃g. g 0 ∈ {f i} ∧ chain r g" by (rule exI [of _ "?f"])
  then show ?thesis unfolding SN_defs by auto
qed

lemma quasi_commute_imp_SN:
  assumes "SN r" and "SN s" and "quasi_commute r s"
  shows "SN (r ∪ s)"
proof -
  have "quasi_commute r (s⇧⁺)" by (rule qc_imp_qc_trancl [OF ‹quasi_commute r s›])
  let ?B = "{a. ¬ SN_on (r ∪ s) {a}}"
  {
    assume "¬ SN(r ∪ s)"
    then obtain a where "a ∈ ?B" unfolding SN_defs by fast
    from ‹SN r› have "∀Q x. x ∈ Q ⟶ (∃z∈Q. ∀y. (z, y) ∈ r ⟶ y ∉ Q)"
      by (rule SN_imp_minimal)
    then have "∀x. x ∈ ?B ⟶ (∃z∈?B. ∀y. (z, y) ∈ r ⟶ y ∉ ?B)" by (rule spec [where x = ?B])
    with ‹a ∈ ?B› obtain b where "b ∈ ?B" and min: "∀y. (b, y) ∈ r ⟶ y ∉ ?B" by auto
    from ‹b ∈ ?B› obtain S where "S 0 = b" and
      chain: "chain (r ∪ s) S" unfolding SN_on_def by auto
    let ?S = "λi. S(Suc i)"
    have "?S 0 = S 1" by simp
    from chain have "chain (r ∪ s) ?S" by auto
    with ‹?S 0 = S 1› have "¬ SN_on (r ∪ s) {S 1}" unfolding SN_on_def by auto
    from ‹S 0 = b› and chain have "(b, S 1) ∈ r ∪ s" by auto
    with min and ‹¬ SN_on (r ∪ s) {S 1}› have "(b, S 1) ∈ s" by auto
    let ?i = "LEAST i. (S i, S(Suc i)) ∉ s"
    {
      assume "chain s S"
      with ‹S 0 = b› have "¬ SN_on s {b}" unfolding SN_on_def by auto
      with ‹SN s› have False unfolding SN_defs by auto
    }
    then have ex: "∃i. (S i, S(Suc i)) ∉ s" by auto
    then have "(S ?i, S(Suc ?i)) ∉ s" by (rule LeastI_ex)
    with chain have "(S ?i, S(Suc ?i)) ∈ r" by auto
    have ini: "∀i<?i. (S i, S(Suc i)) ∈ s" using not_less_Least by auto
    {
      fix i assume "i < ?i" then have "(b, S(Suc i)) ∈ s⇧⁺"
      proof (induct i)
        case 0 then show ?case using ‹(b, S 1) ∈ s› and ‹S 0 = b› by auto
      next
        case (Suc k)
      then have "(b, S(Suc k)) ∈ s⇧⁺" and "Suc k < ?i" by auto
      with ‹∀i<?i. (S i, S(Suc i)) ∈ s› have "(S(Suc k), S(Suc(Suc k))) ∈ s" by fast
      with ‹(b, S(Suc k)) ∈ s⇧⁺› show ?case by auto
    qed
    }
    then have pref: "∀i<?i. (b, S(Suc i)) ∈ s⇧⁺" by auto
    from ‹(b, S 1) ∈ s› and ‹S 0 = b› have "(S 0, S(Suc 0)) ∈ s" by auto
    {
      assume "?i = 0"
      from ex have "(S ?i, S(Suc ?i)) ∉ s" by (rule LeastI_ex)
      with ‹(S 0, S(Suc 0)) ∈ s› have False unfolding ‹?i = 0› by simp
    }
    then have "0 < ?i" by auto
    then obtain j where "?i =  Suc j" unfolding gr0_conv_Suc by best
    with ini have "(S(?i-Suc 0), S(Suc(?i-Suc 0))) ∈ s" by auto
    with pref have "(b, S(Suc j)) ∈ s⇧⁺" unfolding ‹?i = Suc j› by auto
    then have "(b, S ?i) ∈ s⇧⁺" unfolding ‹?i = Suc j› by auto
    with ‹(S ?i, S(Suc ?i)) ∈ r› have "(b, S(Suc ?i)) ∈ (s⇧⁺ O r)" by auto
    with ‹quasi_commute r (s⇧⁺)› have "(b, S(Suc ?i)) ∈ r O (r ∪ s⇧⁺)⇧^*"
      unfolding quasi_commute_def by auto
    then obtain c where "(b, c) ∈ r" and "(c, S(Suc ?i)) ∈ (r ∪ s⇧⁺)⇧^*" by best
    from ‹(b, c) ∈ r› have "(b, c) ∈ (r ∪ s)⇧^*" by auto
    from chain_imp_not_SN_on [of S "r ∪ s"]
      and chain have "¬ SN_on (r ∪ s) {S (Suc ?i)}" by auto
    from ‹(c, S(Suc ?i)) ∈ (r ∪ s⇧⁺)⇧^*› have "(c, S(Suc ?i)) ∈ (r ∪ s)⇧^*"
      unfolding rtrancl_union_subset_rtrancl_union_trancl by auto
    with steps_reflect_SN_on [of "r ∪ s"]
      and ‹¬ SN_on (r ∪ s) {S(Suc ?i)}› have "¬ SN_on (r ∪ s) {c}" by auto
    then have "c ∈ ?B" by simp
    with ‹(b, c) ∈ r› and min have False by auto
  }
  then show ?thesis by auto
qed


subsection ‹Strong Normalization›

lemma non_strict_into_strict:
  assumes compat: "NS O S ⊆ S"
    and steps: "(s, t) ∈ (NS⇧^*) O S"
  shows "(s, t) ∈ S"
using steps proof
  fix x u z
  assume "(s, t) = (x, z)" and "(x, u) ∈ NS⇧^*" and "(u, z) ∈ S"
  then have "(s, u) ∈ NS⇧^*" and "(u, t) ∈ S" by auto
  then show ?thesis
  proof (induct rule:rtrancl.induct)
    case (rtrancl_refl x) then show ?case .
  next
    case (rtrancl_into_rtrancl a b c)
    with compat show ?case by auto
  qed
qed

lemma comp_trancl:
  assumes "R O S ⊆ S" shows "R O S⇧⁺ ⊆ S⇧⁺"
proof (rule subrelI)
  fix w z assume "(w, z) ∈ R O S⇧⁺"
  then obtain x where R_step: "(w, x) ∈ R" and S_seq: "(x, z) ∈ S⇧⁺" by best
  from tranclD [OF S_seq] obtain y where S_step: "(x, y) ∈ S" and S_seq': "(y, z) ∈ S⇧^*" by auto
  from R_step and S_step have "(w, y) ∈ R O S" by auto
  with assms have "(w, y) ∈ S" by auto
  with S_seq' show "(w, z) ∈ S⇧⁺" by simp
qed

lemma comp_rtrancl_trancl:
  assumes comp: "R O S ⊆ S"
    and seq: "(s, t) ∈ (R ∪ S)⇧^* O S"
  shows "(s, t) ∈ S⇧⁺"
using seq proof
  fix x u z
  assume "(s, t) = (x, z)" and "(x, u) ∈ (R ∪ S)⇧^*" and "(u, z) ∈ S"
  then have "(s, u) ∈ (R ∪ S)⇧^*" and "(u, t) ∈ S⇧⁺" by auto
  then show ?thesis
  proof (induct rule: rtrancl.induct)
    case (rtrancl_refl x) then show ?case .
  next
    case (rtrancl_into_rtrancl a b c)
    then have "(b, c) ∈ R ∪ S" by simp
    then show ?case
    proof
      assume "(b, c) ∈ S"
      with rtrancl_into_rtrancl
      have "(b, t) ∈ S⇧⁺" by simp
      with rtrancl_into_rtrancl show ?thesis by simp
    next
      assume "(b, c) ∈ R"
      with comp_trancl [OF comp] rtrancl_into_rtrancl
      show ?thesis by auto
    qed
  qed
qed

lemma trancl_union_right: "r⇧⁺ ⊆ (s ∪ r)⇧⁺"
proof (rule subrelI)
  fix x y assume "(x, y) ∈ r⇧⁺" then show "(x, y) ∈ (s ∪ r)⇧⁺"
  proof (induct)
    case base then show ?case by auto
  next
    case (step a b)
    then have "(a, b) ∈ (s ∪ r)⇧⁺" by auto
    with ‹(x, a) ∈ (s ∪ r)⇧⁺› show ?case by auto
  qed
qed

lemma restrict_SN_subset: "restrict_SN R S ⊆ R"
proof (rule subrelI)
  fix a b assume "(a, b) ∈ restrict_SN R S" then show "(a, b) ∈ R" unfolding restrict_SN_def by simp
qed

lemma chain_Un_SN_on_imp_first_step:
  assumes "chain (R ∪ S) t" and "SN_on S {t 0}"
  shows "∃i. (t i, t (Suc i)) ∈ R ∧ (∀j<i. (t j, t (Suc j)) ∈ S ∧ (t j, t (Suc j)) ∉ R)"
proof -
  from ‹SN_on S {t 0}› obtain i where "(t i, t (Suc i)) ∉ S" by blast
  with assms have "(t i, t (Suc i)) ∈ R" (is "?P i") by auto
  let ?i = "Least ?P"
  from ‹?P i› have "?P ?i" by (rule LeastI)
  have "∀j<?i. (t j, t (Suc j)) ∉ R" using not_less_Least by auto
  moreover with assms have "∀j<?i. (t j, t (Suc j)) ∈ S" by best
  ultimately have "∀j<?i. (t j, t (Suc j)) ∈ S ∧ (t j, t (Suc j)) ∉ R" by best
  with ‹?P ?i› show ?thesis by best
qed

lemma first_step:
  assumes C: "C = A ∪ B" and steps: "(x, y) ∈ C⇧^*" and Bstep: "(y, z) ∈ B"
  shows "∃y. (x, y) ∈ A⇧^* O B"
  using steps
proof (induct rule: converse_rtrancl_induct)
  case base
  show ?case using Bstep by auto
next 
  case (step u x)
  from step(1)[unfolded C] 
  show ?case
  proof
    assume "(u, x) ∈ B"
    then show ?thesis by auto
  next
    assume ux: "(u, x) ∈ A"
    from step(3) obtain y where "(x, y) ∈ A⇧^* O B" by auto
    then obtain z where "(x, z) ∈ A⇧^*" and step: "(z, y) ∈ B" by auto
    with ux have "(u, z) ∈ A⇧^*" by auto
    with step have "(u, y) ∈ A⇧^* O B" by auto
    then show ?thesis by auto
  qed
qed

lemma first_step_O:
  assumes C: "C = A ∪ B" and steps: "(x, y) ∈ C⇧^* O B"
  shows "∃ y. (x, y) ∈ A⇧^* O B"
proof -
  from steps obtain z where "(x, z) ∈ C⇧^*" and "(z, y) ∈ B" by auto
  from first_step [OF C this] show ?thesis .
qed

lemma firstStep:
  assumes LSR: "L = S ∪ R" and xyL: "(x, y) ∈ L⇧^*"
  shows "(x, y) ∈ R⇧^* ∨ (x, y) ∈ R⇧^* O S O L⇧^*"
proof (cases "(x, y) ∈ R⇧^*")
  case True
  then show ?thesis by simp
next
  case False 
  let ?SR = "S ∪ R"
  from xyL and LSR have "(x, y) ∈ ?SR⇧^*" by simp
  from this and False have "(x, y) ∈ R⇧^* O S O ?SR⇧^*" 
  proof (induct rule: rtrancl_induct)
    case base then show ?case by simp
  next
    case (step y z)
    then show ?case
    proof (cases "(x, y) ∈ R⇧^*")
      case False with step have "(x, y) ∈ R⇧^* O S O ?SR⇧^*" by simp
      from this obtain u where xu: "(x, u) ∈ R⇧^* O S" and uy: "(u, y) ∈ ?SR⇧^*" by force
      from ‹(y, z) ∈ ?SR› have "(y, z) ∈ ?SR⇧^*" by auto
      with uy have "(u, z) ∈ ?SR⇧^*" by (rule rtrancl_trans)
      with xu show ?thesis by auto
    next
      case True 
      have "(y, z) ∈ S" 
      proof (rule ccontr)
        assume "(y, z) ∉ S" with ‹(y, z) ∈ ?SR› have "(y, z) ∈ R" by auto
        with True  have "(x, z) ∈ R⇧^*"  by auto
        with ‹(x, z) ∉ R⇧^*› show False ..
      qed
      with True show ?thesis by auto
    qed
  qed
  with LSR show ?thesis by simp
qed


lemma non_strict_ending:
  assumes chain: "chain (R ∪ S) t"
    and comp: "R O S ⊆ S"
    and SN: "SN_on S {t 0}"
  shows "∃j. ∀i≥j. (t i, t (Suc i)) ∈ R - S"
proof (rule ccontr)
  assume "¬ ?thesis"
  with chain have "∀i. ∃j. j ≥ i ∧ (t j, t (Suc j)) ∈ S" by blast
  from choice [OF this] obtain f where S_steps: "∀i. i ≤ f i ∧ (t (f i), t (Suc (f i))) ∈ S" ..
  let ?t = "λi. t (((Suc ∘ f) ^^ i) 0)"
  have S_chain: "∀i. (t i, t (Suc (f i))) ∈ S⇧⁺"
  proof
    fix i
    from S_steps have leq: "i≤f i" and step: "(t(f i), t(Suc(f i))) ∈ S" by auto
    from chain_imp_rtrancl [OF chain leq] have "(t i, t(f i)) ∈ (R ∪ S)⇧^*" .
    with step have "(t i, t(Suc(f i))) ∈ (R ∪ S)⇧^* O S" by auto
    from comp_rtrancl_trancl [OF comp this] show "(t i, t(Suc(f i))) ∈ S⇧⁺" .
  qed
  then have "chain (S⇧⁺) ?t"by simp
  moreover have "SN_on (S⇧⁺) {?t 0}" using SN_on_trancl [OF SN] by simp
  ultimately show False unfolding SN_defs by best
qed

lemma SN_on_subset1:
  assumes "SN_on r A" and "s ⊆ r"
  shows "SN_on s A"
  using assms unfolding SN_defs by blast

lemmas SN_on_mono = SN_on_subset1

lemma rtrancl_fun_conv:
  "((s, t) ∈ R⇧^*) = (∃ f n. f 0 = s ∧ f n = t ∧ (∀ i < n. (f i, f (Suc i)) ∈ R))"
  unfolding rtrancl_is_UN_relpow using relpow_fun_conv [where R = R]
  by auto

lemma compat_tr_compat:
  assumes "NS O S ⊆ S" shows "NS⇧^* O S ⊆ S"
  using non_strict_into_strict [where S = S and NS = NS] assms by blast

lemma right_comp_S [simp]:
  assumes "(x, y) ∈ S O (S O S⇧^* O NS⇧^* ∪ NS⇧^*)"
  shows "(x, y) ∈ (S O S⇧^* O NS⇧^*)"
proof-
  from assms have "(x, y) ∈ (S O S O S⇧^* O NS⇧^*) ∪ (S O NS⇧^*)" by auto
  then have  xy:"(x, y) ∈ (S O (S O S⇧^*) O NS⇧^*) ∪ (S O NS⇧^*)" by auto
  have "S O S⇧^* ⊆ S⇧^*" by auto
  with xy have "(x, y) ∈ (S O S⇧^* O NS⇧^*) ∪ (S O NS⇧^*)" by auto
  then show "(x, y) ∈ (S O S⇧^* O NS⇧^*)" by auto
qed

lemma compatible_SN:
  assumes SN: "SN S"
  and compat: "NS O S ⊆ S" 
  shows "SN (S O S⇧^* O NS⇧^*)" (is "SN ?A")
proof
  fix F assume chain: "chain ?A F"
  from compat compat_tr_compat have tr_compat: "NS⇧^* O S ⊆ S" by blast
  have "∀i. (∃y z. (F i, y) ∈ S ∧ (y, z)  ∈ S⇧^* ∧ (z, F (Suc i)) ∈ NS⇧^*)"
  proof
    fix i
    from chain have "(F i, F (Suc i)) ∈ (S O S⇧^* O NS⇧^*)" by auto
    then show "∃ y z. (F i, y)  ∈ S ∧ (y, z)  ∈ S⇧^* ∧ (z, F (Suc i)) ∈ NS⇧^*"
      unfolding relcomp_def (*FIXME:relcomp_unfold*) using mem_Collect_eq by auto
  qed
  then have "∃ f. (∀ i. (∃ z. (F i, f i)  ∈ S ∧ ((f i, z)  ∈ S⇧^*) ∧(z, F (Suc i)) ∈ NS⇧^*))"
    by (rule choice)
  then obtain f
    where "∀ i. (∃ z. (F i, f i)  ∈ S ∧ ((f i, z)  ∈ S⇧^*) ∧(z, F (Suc i)) ∈ NS⇧^*)" ..
  then have "∃ g. ∀ i. (F i, f i)  ∈ S ∧ (f i, g i)  ∈ S⇧^* ∧ (g i, F (Suc i)) ∈ NS⇧^*"
    by (rule choice)
  then obtain g where "∀ i. (F i, f i)  ∈ S ∧ (f i, g i)  ∈ S⇧^* ∧ (g i, F (Suc i)) ∈ NS⇧^*" ..
  then have "∀ i. (f i, g i)  ∈ S⇧^* ∧ (g i, F (Suc i)) ∈ NS⇧^* ∧ (F (Suc i), f (Suc i))  ∈ S"
    by auto
  then have "∀ i. (f i, g i)  ∈ S⇧^* ∧ (g i, f (Suc i))  ∈ S" unfolding relcomp_def (*FIXME*)
    using tr_compat by auto
  then have all:"∀ i. (f i, g i)  ∈ S⇧^* ∧ (g i, f (Suc i))  ∈ S⇧⁺" by auto
  have "∀ i. (f i, f (Suc i))  ∈ S⇧⁺"
  proof
    fix i
    from all have "(f i, g i)  ∈ S⇧^* ∧ (g i, f (Suc i))  ∈ S⇧⁺" ..
    then show "(f i, f (Suc i))  ∈ S⇧⁺" using transitive_closure_trans by auto
  qed
  then have "∃x. f 0 = x ∧ chain (S⇧⁺) f"by auto
  then obtain x where "f 0 = x ∧ chain (S⇧⁺) f" by auto
  then have "∃f. f 0 = x ∧ chain (S⇧⁺) f" by auto
  then have "¬ SN_on (S⇧⁺) {x}" by auto
  then have "¬ SN (S⇧⁺)" unfolding SN_defs by auto
  then have wfSconv:"¬ wf ((S⇧⁺)¯)" using SN_iff_wf by auto
  from SN have "wf (S¯)" using SN_imp_wf [where?r=S] by simp
  with wf_converse_trancl wfSconv show False by auto
qed

lemma compatible_rtrancl_split:
  assumes compat: "NS O S ⊆ S"
   and steps: "(x, y) ∈ (NS ∪ S)⇧^*"
  shows "(x, y) ∈ S O S⇧^* O NS⇧^* ∪ NS⇧^*"
proof-
  from steps have "∃ n. (x, y) ∈ (NS ∪ S)^^n" using rtrancl_imp_relpow [where ?R="NS ∪ S"] by auto
  then obtain n where "(x, y) ∈ (NS ∪ S)^^n" by auto
  then show "(x, y) ∈  S O S⇧^* O NS⇧^* ∪ NS⇧^*"
  proof (induct n arbitrary: x, simp)
    case (Suc m)
    assume "(x, y) ∈ (NS ∪ S)^^(Suc m)"
    then have "∃ z. (x, z) ∈ (NS ∪ S) ∧ (z, y) ∈ (NS ∪ S)^^m"
      using relpow_Suc_D2 [where ?R="NS ∪ S"] by auto
    then obtain z where xz:"(x, z) ∈ (NS ∪ S)" and zy:"(z, y) ∈ (NS ∪ S)^^m" by auto
    with Suc have zy:"(z, y) ∈  S O S⇧^* O NS⇧^* ∪ NS⇧^*" by auto
    then show "(x, y) ∈  S O S⇧^* O NS⇧^* ∪ NS⇧^*"
    proof (cases "(x, z) ∈ NS")
      case True
      from compat compat_tr_compat have trCompat: "NS⇧^* O S ⊆ S" by blast
      from zy True have "(x, y) ∈ (NS O S O S⇧^* O NS⇧^*) ∪ (NS O NS⇧^*)" by auto
      then have "(x, y) ∈ ((NS O S) O S⇧^* O NS⇧^*) ∪ (NS O NS⇧^*)" by auto
      then have "(x, y) ∈ ((NS⇧^* O S) O S⇧^* O NS⇧^*) ∪ (NS O NS⇧^*)" by auto
      with trCompat have xy:"(x, y) ∈ (S O S⇧^* O NS⇧^*) ∪ (NS O NS⇧^*)" by auto
      have "NS O NS⇧^* ⊆ NS⇧^*" by auto
      with xy show "(x, y) ∈ (S O S⇧^* O NS⇧^*) ∪ NS⇧^*" by auto
    next
      case False
      with xz have xz:"(x, z) ∈ S" by auto
      with zy have "(x, y) ∈ S O (S O S⇧^* O NS⇧^* ∪ NS⇧^*)" by auto
      then show "(x, y) ∈ (S O S⇧^* O NS⇧^*) ∪ NS⇧^*" using right_comp_S by simp
    qed
  qed
qed

lemma compatible_conv:
  assumes compat: "NS O S ⊆ S" 
  shows "(NS ∪ S)⇧^* O S O (NS ∪ S)⇧^* = S O S⇧^* O NS⇧^*" 
proof -
  let ?NSuS = "NS ∪ S"
  let ?NSS = "S O S⇧^* O NS⇧^*"
  let ?midS = "?NSuS⇧^* O S O ?NSuS⇧^*"
  have one: "?NSS ⊆ ?midS" by regexp 
  have "?NSuS⇧^* O S ⊆ (?NSS ∪ NS⇧^*) O S"
    using compatible_rtrancl_split [where S = S and NS = NS] compat by blast
  also have "… ⊆ ?NSS O S ∪ NS⇧^* O S" by auto
  also have "… ⊆ ?NSS O S ∪ S" using compat compat_tr_compat [where S = S and NS = NS] by auto
  also have "… ⊆ S O ?NSuS⇧^*" by regexp
  finally have "?midS ⊆ S O ?NSuS⇧^* O ?NSuS⇧^*" by blast
  also have "… ⊆ S O ?NSuS⇧^*" by regexp
  also have "… ⊆ S O (?NSS ∪ NS⇧^*)"
    using compatible_rtrancl_split [where S = S and NS = NS] compat by blast
  also have "… ⊆ ?NSS" by regexp
  finally have two: "?midS ⊆ ?NSS" . 
  from one two show ?thesis by auto 
qed

lemma compatible_SN': 
  assumes compat: "NS O S ⊆ S" and SN: "SN S"
  shows "SN((NS ∪ S)⇧^* O S O (NS ∪ S)⇧^*)"
using compatible_conv [where S = S and NS = NS] 
  compatible_SN [where S = S and NS = NS] assms by force

lemma rtrancl_diff_decomp:
  assumes "(x, y) ∈ A⇧^* - B⇧^*"
  shows "(x, y) ∈ A⇧^* O (A - B) O A⇧^*"
proof-
  from assms have A: "(x, y) ∈ A⇧^*" and B:"(x, y) ∉ B⇧^*" by auto
  from A have "∃ k. (x, y) ∈ A^^k" by (rule rtrancl_imp_relpow)
  then obtain k where Ak:"(x, y) ∈ A^^k" by auto
  from Ak B show "(x, y) ∈ A⇧^* O (A - B) O A⇧^*"
  proof (induct k arbitrary: x)
    case 0
    with ‹(x, y) ∉ B⇧^*› 0 show ?case using ccontr by auto
  next
    case (Suc i)
    then have B:"(x, y) ∉ B⇧^*" and ASk:"(x, y) ∈ A ^^ Suc i" by auto
    from ASk have "∃z. (x, z) ∈ A ∧ (z, y) ∈ A ^^ i" using relpow_Suc_D2 [where ?R=A] by auto
    then obtain z where xz:"(x, z) ∈ A" and "(z, y) ∈ A ^^ i" by auto
    then have zy:"(z, y) ∈ A⇧^*" using relpow_imp_rtrancl by auto
    from xz show "(x, y) ∈ A⇧^* O (A - B) O A⇧^*"
    proof (cases "(x, z) ∈ B")
      case False
      with xz zy show "(x, y) ∈ A⇧^* O (A - B) O A⇧^*" by auto
    next
      case True
      then have "(x, z) ∈ B⇧^*" by auto
      have "⟦(x, z) ∈ B⇧^*; (z, y) ∈ B⇧^*⟧ ⟹ (x, y) ∈ B⇧^*" using rtrancl_trans [of x z B] by auto
      with  ‹(x, z) ∈ B⇧^*› ‹(x, y) ∉ B⇧^*› have "(z, y) ∉ B⇧^*" by auto
      with Suc ‹(z, y) ∈ A ^^ i› have "(z, y) ∈ A⇧^* O (A - B) O A⇧^*" by auto
      with xz have xy:"(x, y) ∈ A O A⇧^* O (A - B) O A⇧^*" by auto
      have "A O A⇧^* O (A - B) O A⇧^* ⊆ A⇧^* O (A - B) O A⇧^*" by regexp
      from this xy show "(x, y) ∈ A⇧^* O (A - B) O A⇧^*"
        using subsetD [where ?A="A O A⇧^* O (A - B) O A⇧^*"] by auto
    qed
  qed
qed

lemma SN_empty [simp]: "SN {}" by auto

lemma SN_on_weakening:
  assumes "SN_on R1 A"
  shows "SN_on (R1 ∩ R2) A"
proof -
  {
    assume "∃S. S 0 ∈ A ∧ chain (R1 ∩ R2) S"
    then obtain S where
      S0: "S 0 ∈ A" and
      SN: "chain (R1 ∩ R2) S"
      by auto
    from SN have SN': "chain R1 S" by simp
    with S0 and assms have "False" by auto
  }
  then show ?thesis by force
qed

(* an explicit version of infinite reduction *)
definition ideriv :: "'a rel ⇒ 'a rel ⇒ (nat ⇒ 'a) ⇒ bool" where
  "ideriv R S as ⟷ (∀i. (as i, as (Suc i)) ∈ R ∪ S) ∧ (INFM i. (as i, as (Suc i)) ∈ R)"

lemma ideriv_mono: "R ⊆ R' ⟹ S ⊆ S' ⟹ ideriv R S as ⟹ ideriv R' S' as"
  unfolding ideriv_def INFM_nat by blast

fun
  shift :: "(nat ⇒ 'a) ⇒ nat ⇒ nat ⇒ 'a"
where
  "shift f j = (λ i. f (i+j))"

lemma ideriv_split:
  assumes ideriv: "ideriv R S as"
    and nideriv: "¬ ideriv (D ∩ (R ∪ S)) (R ∪ S - D) as"
  shows "∃ i. ideriv (R - D) (S - D) (shift as i)"
proof -
  have RS: "R - D ∪ (S - D) = R ∪ S - D" by auto
  from ideriv [unfolded ideriv_def]
  have as: "⋀ i. (as i, as (Suc i)) ∈ R ∪ S"
    and inf: "INFM i. (as i, as (Suc i)) ∈ R" by auto
  show ?thesis
  proof (cases "INFM i. (as i, as (Suc i)) ∈ D ∩ (R ∪ S)")
    case True
    have "ideriv (D ∩ (R ∪ S)) (R ∪ S - D) as"
      unfolding ideriv_def
      using as True  by auto
    with nideriv show ?thesis ..
  next
    case False
    from False [unfolded INFM_nat]
    obtain i where Dn: "⋀ j. i < j ⟹ (as j, as (Suc j)) ∉ D ∩ (R ∪ S)"
      by auto
    from Dn as have as: "⋀ j. i < j ⟹ (as j, as (Suc j)) ∈ R ∪ S - D" by auto
    show ?thesis
    proof (rule exI [of _ "Suc i"], unfold ideriv_def RS, insert as, intro conjI, simp, unfold INFM_nat, intro allI)
      fix m
      from inf [unfolded INFM_nat] obtain j where j: "j > Suc i + m"
        and R: "(as j, as (Suc j)) ∈ R" by auto
      with as [of j] have RD: "(as j, as (Suc j)) ∈ R - D" by auto      
      show "∃ j > m. (shift as (Suc i) j, shift as (Suc i) (Suc j)) ∈ R - D"
        by (rule exI [of _ "j - Suc i"], insert j RD, auto)
    qed
  qed
qed

lemma ideriv_SN:
  assumes SN: "SN S"
    and compat: "NS O S ⊆ S"
    and R: "R ⊆ NS ∪ S"
  shows "¬ ideriv (S ∩ R) (R - S) as"
proof
  assume "ideriv (S ∩ R) (R - S) as"
  with R have steps: "∀ i. (as i, as (Suc i)) ∈ NS ∪ S"
    and inf: "INFM i. (as i, as (Suc i)) ∈ S ∩ R" unfolding ideriv_def by auto
  from non_strict_ending [OF steps compat] SN
  obtain i where i: "⋀ j. j ≥ i ⟹ (as j, as (Suc j)) ∈ NS - S" by fast
  from inf [unfolded INFM_nat] obtain j where "j > i" and "(as j, as (Suc j)) ∈ S" by auto
  with i [of j] show False by auto
qed

lemma Infm_shift: "(INFM i. P (shift f n i)) = (INFM i. P (f i))" (is "?S = ?O")
proof 
  assume ?S
  show ?O
    unfolding INFM_nat_le 
  proof
    fix m
    from ‹?S› [unfolded INFM_nat_le]
    obtain k where k: "k ≥ m" and p: "P (shift f n k)" by auto
    show "∃ k ≥ m. P (f k)"
      by (rule exI [of _ "k + n"], insert k p, auto)
  qed
next
  assume ?O
  show ?S
    unfolding INFM_nat_le 
  proof
    fix m
    from ‹?O› [unfolded INFM_nat_le]
    obtain k where k: "k ≥ m + n" and p: "P (f k)" by auto
    show "∃ k ≥ m. P (shift f n k)"
      by (rule exI [of _ "k - n"], insert k p, auto)
  qed
qed

lemma rtrancl_list_conv:
  "(s, t) ∈ R⇧^* ⟷ 
    (∃ ts. last (s # ts) = t ∧ (∀i<length ts. ((s # ts) ! i, (s # ts) ! Suc i) ∈ R))" (is "?l = ?r")
proof 
  assume ?r
  then obtain ts where "last (s # ts) = t ∧ (∀i<length ts. ((s # ts) ! i, (s # ts) ! Suc i) ∈ R)" ..
  then show ?l
  proof (induct ts arbitrary: s, simp)
    case (Cons u ll)
    then have "last (u # ll) = t ∧ (∀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
  let ?ts = "map (λ i. S (Suc i)) [0 ..< n]"
  show ?r
  proof (rule exI [of _ ?ts], intro conjI, 
      cases n, simp add: s [symmetric] t [symmetric], simp add: t [symmetric]) 
    show "∀ i < length ?ts. ((s # ?ts) ! i, (s # ?ts) ! Suc i) ∈ R" 
    proof (intro allI impI)
      fix i
      assume i: "i < length ?ts"
      then show "((s # ?ts) ! i, (s # ?ts) ! Suc i) ∈ R"
      proof (cases i, simp add: s [symmetric] steps)
        case (Suc j)
        with i steps show ?thesis by simp
      qed
    qed
  qed
qed

lemma SN_reaches_NF:
  assumes "SN_on r {x}"
  shows "∃y. (x, y) ∈ r⇧^* ∧ y ∈ NF r"
using assms
proof (induct rule: SN_on_induct')
  case (IH x)
  show ?case
  proof (cases "x ∈ NF r")
    case True
    then show ?thesis by auto
  next
    case False
    then obtain y where step: "(x, y) ∈ r" by auto
    from IH [OF this] obtain z where steps: "(y, z) ∈ r⇧^*" and NF: "z ∈ NF r" by auto
    show ?thesis
      by (intro exI, rule conjI [OF _ NF], insert step steps, auto)
  qed
qed

lemma SN_WCR_reaches_NF:
  assumes SN: "SN_on r {x}" 
    and WCR: "WCR_on r {x. SN_on r {x}}"
  shows "∃! y. (x, y) ∈ r⇧^* ∧ y ∈ NF r"
proof -
  from SN_reaches_NF [OF SN] obtain y where steps: "(x, y) ∈ r⇧^*" and NF: "y ∈ NF r" by auto
  show ?thesis
  proof(rule, rule conjI [OF steps NF])
    fix z
    assume steps': "(x, z) ∈ r⇧^* ∧ z ∈ NF r"
    from Newman_local [OF SN WCR] have "CR_on r {x}" by auto
    from CR_onD [OF this _ steps] steps' have "(y, z) ∈ r⇧^↓" by simp
    from join_NF_imp_eq [OF this NF] steps' show "z = y" by simp
  qed
qed

definition some_NF :: "'a rel ⇒ 'a ⇒ 'a" where
  "some_NF r x = (SOME y. (x, y) ∈ r⇧^* ∧ y ∈ NF r)"

lemma some_NF:
  assumes SN: "SN_on r {x}" 
  shows "(x, some_NF r x) ∈ r⇧^* ∧ some_NF r x ∈ NF r"
  using someI_ex [OF SN_reaches_NF [OF SN]]
  unfolding some_NF_def .

lemma some_NF_WCR:
  assumes SN: "SN_on r {x}"
    and WCR: "WCR_on r {x. SN_on r {x}}"
    and steps: "(x, y) ∈ r⇧^*"
    and NF: "y ∈ NF r"
  shows "y = some_NF r x"
proof -
  let ?p = "λ y. (x, y) ∈ r⇧^* ∧ y ∈ NF r"
  from SN_WCR_reaches_NF [OF SN WCR]
  have one: "∃! y. ?p y" .
  from steps NF have y: "?p y" ..
  from some_NF [OF SN] have some: "?p (some_NF r x)" .
  from one some y show ?thesis by auto
qed

lemma some_NF_UNF:
  assumes UNF: "UNF r"
    and steps: "(x, y) ∈ r⇧^*"
    and NF: "y ∈ NF r"
  shows "y = some_NF r x"
proof -
  let ?p = "λ y. (x, y) ∈ r⇧^* ∧ y ∈ NF r"
  from steps NF have py: "?p y" by simp
  then have pNF: "?p (some_NF r x)" unfolding some_NF_def 
    by (rule someI)
  from py have y: "(x, y) ∈ r⇧^!" by auto
  from pNF have nf: "(x, some_NF r x) ∈ r⇧^!" by auto
  from UNF [unfolded UNF_on_def] y nf show ?thesis by auto
qed

definition "the_NF A a = (THE b. (a, b) ∈ A⇧^!)"

context
  fixes A
  assumes SN: "SN A" and CR: "CR A"
begin
lemma the_NF: "(a, the_NF A a) ∈ A⇧^!"
proof -
  obtain b where ab: "(a, b) ∈ A⇧^!" using SN by (meson SN_imp_WN UNIV_I WN_onE)
  moreover have "(a, c) ∈ A⇧^! ⟹ c = b" for c
    using CR and ab by (meson CR_divergence_imp_join join_NF_imp_eq normalizability_E)
  ultimately have "∃!b. (a, b) ∈ A⇧^!" by blast
  then show ?thesis unfolding the_NF_def by (rule theI')
qed

lemma the_NF_NF: "the_NF A a ∈ NF A"
  using the_NF by (auto simp: normalizability_def)

lemma the_NF_step:
  assumes "(a, b) ∈ A"
  shows "the_NF A a = the_NF A b"
  using the_NF and assms
  by (meson CR SN SN_imp_WN conversionI' r_into_rtrancl semi_complete_imp_conversionIff_same_NF semi_complete_onI)

lemma the_NF_steps:
  assumes "(a, b) ∈ A⇧^*"
  shows "the_NF A a = the_NF A b"
  using assms by (induct) (auto dest: the_NF_step)

lemma the_NF_conv:
  assumes "(a, b) ∈ A⇧^↔⇧^*"
  shows "the_NF A a = the_NF A b"
  using assms
  by (meson CR WN_on_def the_NF semi_complete_imp_conversionIff_same_NF semi_complete_onI)

end


definition weak_diamond :: "'a rel ⇒ bool" (‹w◇›) where
  "w◇ r ⟷ (r¯ O r) - Id ⊆ (r O r¯)"

lemma weak_diamond_imp_CR:
  assumes wd: "w◇ r"
  shows "CR r"
proof (rule semi_confluence_imp_CR, rule)
  fix x y
  assume "(x, y) ∈ r¯ O r⇧^*"
  then obtain z where step: "(z, x) ∈ r" and steps: "(z, y) ∈ r⇧^*" by auto
  from steps
  have "∃ u. (x, u) ∈ r⇧^* ∧ (y, u) ∈ r⇧⁼" 
  proof (induct) 
    case base
    show ?case
      by (rule exI [of _ x], insert step, auto)
  next
    case (step y' y)
    from step(3) obtain u where xu: "(x, u) ∈ r⇧^*" and y'u: "(y', u) ∈ r⇧⁼" by auto
    from y'u have "(y', u) ∈ r ∨ y' = u" by auto
    then show ?case
    proof
      assume y'u: "y' = u"
      with xu step(2) have xy: "(x, y) ∈ r⇧^*" by auto
      show ?thesis 
        by (intro exI conjI, rule xy, simp)
    next
      assume "(y', u) ∈ r"
      with step(2) have uy: "(u, y) ∈ r¯ O r" by auto
      show ?thesis
      proof (cases "u = y")
        case True
        show ?thesis
          by (intro exI conjI, rule xu, unfold True, simp)
      next
        case False
        with uy
          wd [unfolded weak_diamond_def] obtain u' where uu': "(u, u') ∈ r"
          and yu': "(y, u') ∈ r" by auto
        from xu uu' have xu: "(x, u') ∈ r⇧^*" by auto
        show ?thesis
          by (intro exI conjI, rule xu, insert yu', auto)
      qed
    qed
  qed        
  then show "(x, y) ∈ r⇧^↓" by auto
qed

lemma steps_imp_not_SN_on:
  fixes t :: "'a ⇒ 'b"
    and R :: "'b rel"
  assumes steps: "⋀ x. (t x, t (f x)) ∈ R"
  shows "¬ SN_on R {t x}"
proof  
  let ?U = "range t"
  assume "SN_on R {t x}"
  from SN_on_imp_on_minimal [OF this, rule_format, of ?U]
  obtain tz where tz: "tz ∈ range t" and min: "⋀ y. (tz, y) ∈ R ⟹ y ∉ range t" by auto
  from tz obtain z where tz: "tz = t z" by auto
  from steps [of z] min [of "t (f z)"] show False unfolding tz by auto
qed

lemma steps_imp_not_SN:
  fixes t :: "'a ⇒ 'b"
    and R :: "'b rel"
  assumes steps: "⋀ x. (t x, t (f x)) ∈ R"
  shows "¬ SN R"
proof -
  from steps_imp_not_SN_on [of t f R, OF steps]
  show ?thesis unfolding SN_def by blast
qed

lemma steps_map:
  assumes fg: "⋀t u R . P t ⟹ Q R ⟹ (t, u) ∈ R ⟹ P u ∧ (f t, f u) ∈ g R"
  and t: "P t"
  and R: "Q R"
  and S: "Q S"
  shows "((t, u) ∈ R⇧^* ⟶ (f t, f u) ∈ (g R)⇧^*)
    ∧ ((t, u) ∈ R⇧^* O S O R⇧^* ⟶ (f t, f u) ∈ (g R)⇧^* O (g S) O (g R)⇧^*)"
proof -
  {
    fix t u
    assume "(t, u) ∈ R⇧^*" and "P t"
    then have "P u ∧ (f t, f u) ∈ (g R)⇧^*"
    proof (induct)
      case (step u v)
      from step(3)[OF step(4)] have Pu: "P u" and steps: "(f t, f u) ∈ (g R)⇧^*" by auto
      from fg [OF Pu R step(2)] have Pv: "P v" and step: "(f u, f v) ∈ g R" by auto
      with steps have "(f t, f v) ∈ (g R)⇧^*" by auto
      with Pv show ?case by simp
    qed simp
  } note main = this
  note maint = main [OF _ t]
  from maint [of u] have one: "(t, u) ∈ R⇧^* ⟶ (f t, f u) ∈ (g R)⇧^*" by simp
  show ?thesis
  proof (rule conjI [OF one impI])
    assume "(t, u) ∈ R⇧^* O S O R⇧^*"
    then obtain s v where ts: "(t, s) ∈ R⇧^*" and sv: "(s, v) ∈ S" and vu: "(v, u) ∈ R⇧^*" by auto
    from maint [OF ts] have Ps: "P s" and ts: "(f t, f s) ∈ (g R)⇧^*" by auto
    from fg [OF Ps S sv] have Pv: "P v" and sv: "(f s, f v) ∈ g S" by auto
    from main [OF vu Pv] have vu: "(f v, f u) ∈ (g R)⇧^*" by auto
    from ts sv vu show "(f t, f u) ∈ (g R)⇧^* O g S O (g R)⇧^*" by auto
  qed
qed


subsection ‹Terminating part of a relation›

inductive_set
  SN_part :: "'a rel ⇒ 'a set"
  for r :: "'a rel"
where
  SN_partI: "(⋀y. (x, y) ∈ r ⟹ y ∈ SN_part r) ⟹ x ∈ SN_part r"

text ‹The accessible part of a relation is the same as the terminating part
(just two names for the same definition -- modulo argument order). See
@{thm accI}.›

text ‹Characterization of @{const SN_on} via terminating part.›
lemma SN_on_SN_part_conv:
  "SN_on r A ⟷ A ⊆ SN_part r"
proof -
  {
    fix x assume "SN_on r A" and "x ∈ A"
    then have "x ∈ SN_part r" by (induct) (auto intro: SN_partI)
  } moreover {
    fix x assume "x ∈ A" and "A ⊆ SN_part r"
    then have "x ∈ SN_part r" by auto
    then have "SN_on r {x}" by (induct) (auto intro: step_reflects_SN_on)
  } ultimately show ?thesis by (force simp: SN_defs)
qed

text ‹Special case for ``full'' termination.›
lemma SN_SN_part_UNIV_conv:
  "SN r ⟷ SN_part r = UNIV"
  using SN_on_SN_part_conv [of r UNIV] by auto

lemma closed_imp_rtrancl_closed: assumes L: "L ⊆ A"
  and R: "R `` A ⊆ A"
  shows "{t | s. s ∈ L ∧ (s,t) ∈ R^*} ⊆ A"
proof -
  {
    fix s t
    assume "(s,t) ∈ R^*" and "s ∈ L" 
    hence "t ∈ A"
      by (induct, insert L R, auto)
  }
  thus ?thesis by auto
qed

lemma trancl_steps_relpow: assumes "a ⊆ b^+"
  shows "(x,y) ∈ a^^n ⟹ ∃ m. m ≥ n ∧ (x,y) ∈ b^^m"
proof (induct n arbitrary: y)
  case 0 thus ?case by (intro exI[of _ 0], auto)
next
  case (Suc n z)
  from Suc(2) obtain y where xy: "(x,y) ∈ a ^^ n" and yz: "(y,z) ∈ a" by auto
  from Suc(1)[OF xy] obtain m where m: "m ≥ n" and xy: "(x,y) ∈ b ^^ m" by auto
  from yz assms have "(y,z) ∈ b^+" by auto
  from this[unfolded trancl_power] obtain k where k: "k > 0" and yz: "(y,z) ∈ b ^^ k" by auto
  from xy yz have "(x,z) ∈ b ^^ (m + k)" unfolding relpow_add by auto
  with k m show ?case by (intro exI[of _ "m + k"], auto)
qed

lemma relpow_image: assumes f: "⋀ s t. (s,t) ∈ r ⟹ (f s, f t) ∈ r'"
  shows "(s,t) ∈ r ^^ n ⟹ (f s, f t) ∈ r' ^^ n"
proof (induct n arbitrary: t)
  case (Suc n u)
  from Suc(2) obtain t where st: "(s,t) ∈ r ^^ n" and tu: "(t,u) ∈ r" by auto
  from Suc(1)[OF st] f[OF tu] show ?case by auto
qed auto

lemma relpow_refl_mono:
 assumes refl:"⋀ x. (x,x) ∈ Rel"
 shows "m ≤ n ⟹(a,b) ∈ Rel ^^ m ⟹ (a,b) ∈ Rel ^^ n"
proof (induct rule:dec_induct)
  case (step i)
  hence abi:"(a, b) ∈ Rel ^^ i" by auto
  from refl[of b] abi relpowp_Suc_I[of i "λ x y. (x,y) ∈ Rel"] show "(a, b) ∈ Rel ^^ Suc i" by auto
qed

lemma SN_on_induct_acc_style [consumes 1, case_names IH]:
  assumes sn: "SN_on R {a}"
    and IH: "⋀x. SN_on R {x} ⟹ ⟦⋀y. (x, y) ∈ R ⟹ P y⟧  ⟹ P x"
  shows "P a"
proof -
  from sn SN_on_conv_acc [of "R¯" a] have a: "a ∈ termi R" by auto
  show ?thesis
  proof (rule Wellfounded.acc.induct [OF a, of P], rule IH)
    fix x
    assume "⋀y. (y, x) ∈ R¯ ⟹ y ∈ termi R"
    from this [folded SN_on_conv_acc]
      show "SN_on R {x}" by simp fast
  qed auto
qed

(* Lemma 2.3 in Huet: Confluent Reductions *)
lemma partially_localize_CR:
  "CR r ⟷ (∀ x y z. (x, y) ∈ r ∧ (x, z) ∈ r⇧^* ⟶ (y, z) ∈ join r)" 
proof
  assume "CR r"
  thus "∀ x y z. (x, y) ∈ r ∧ (x, z) ∈ r⇧^* ⟶ (y, z) ∈ join r" by auto
next
  assume 1:"∀ x y z. (x, y) ∈ r ∧ (x, z) ∈ r⇧^* ⟶ (y, z) ∈ join r" 
  show "CR r"
  proof
    fix a b c
    assume 2: "a ∈ UNIV" and 3: "(a, b) ∈ r⇧^*" and 4: "(a, c) ∈ r⇧^*"
    then obtain n  where "(a,c) ∈ r^^n" using rtrancl_is_UN_relpow by fast
    with 2 3 show "(b,c) ∈ join r" 
    proof (induct n arbitrary: a b c)
      case 0 thus ?case by auto
    next
      case (Suc m)
      from Suc(4) obtain d where ad: "(a, d) ∈ r^^m" and dc: "(d, c) ∈ r" by auto
      from Suc(1) [OF Suc(2) Suc(3) ad] have "(b, d) ∈ join r" .
      with 1 dc joinE joinI [of b _ r c] join_rtrancl_join show ?case by metis
    qed
  qed
qed

definition strongly_confluent_on :: "'a rel ⇒ 'a set ⇒ bool"
where 
  "strongly_confluent_on r A ⟷
    (∀x ∈ A.  ∀y z. (x, y) ∈ r ∧ (x, z) ∈ r ⟶ (∃u. (y, u) ∈ r⇧^* ∧ (z, u) ∈ r⇧⁼))"

abbreviation strongly_confluent :: "'a rel ⇒ bool"
where
  "strongly_confluent r ≡ strongly_confluent_on r UNIV"

lemma strongly_confluent_on_E11:
  "strongly_confluent_on r A ⟹ x ∈ A ⟹ (x, y) ∈ r ⟹ (x, z) ∈ r ⟹
    ∃u. (y, u) ∈ r⇧^* ∧ (z, u) ∈ r⇧⁼"
unfolding strongly_confluent_on_def by blast

lemma strongly_confluentI [intro]:
  "⟦⋀x y z. (x, y) ∈ r ⟹ (x, z) ∈ r ⟹ ∃u. (y, u) ∈ r⇧^* ∧ (z, u) ∈ r⇧⁼⟧ ⟹ strongly_confluent r" 
unfolding strongly_confluent_on_def by auto

lemma strongly_confluent_E1n:
  assumes scr: "strongly_confluent r"
  shows "(x, y) ∈ r⇧⁼ ⟹ (x, z) ∈ r ^^ n ⟹ ∃u. (y, u) ∈ r⇧^* ∧ (z, u) ∈ r⇧⁼"
proof (induct n arbitrary: x y z)
  case (Suc m)
  from Suc(3) obtain w where xw: "(x, w) ∈ r^^m" and wz: "(w, z) ∈ r" by auto
  from Suc(1) [OF Suc(2) xw] obtain u where yu: "(y, u) ∈ r⇧^*" and wu: "(w, u) ∈ r⇧⁼" by auto
  from strongly_confluent_on_E11 [OF scr, of w] wz yu wu show ?case 
    by (metis UnE converse_rtrancl_into_rtrancl iso_tuple_UNIV_I pair_in_Id_conv rtrancl_trans)
qed auto

(* Lemma 2.5 in Huet: Confluent Reductions *)
lemma strong_confluence_imp_CR: 
  assumes "strongly_confluent r"
  shows "CR r"
proof -
  { fix x y z
    have "(x, y) ∈ r ⟹ (x, z) ∈ r⇧^* ⟹ (y, z) ∈ join r" 
      by (cases "x = y", insert strongly_confluent_E1n [OF assms], blast+) }
  then show "CR r" using partially_localize_CR by blast
qed

lemma WCR_alt_def: "WCR A ⟷ A¯ O A ⊆ A⇧^↓" by (auto simp: WCR_defs)

lemma NF_imp_SN_on: "a ∈ NF R ⟹ SN_on R {a}" unfolding SN_on_def NF_def by blast

lemma Union_sym: "(s, t) ∈ (⋃i≤n. (S i)⇧^↔) ⟷ (t, s) ∈ (⋃i≤n. (S i)⇧^↔)" by auto

lemma peak_iff: "(x, y) ∈ A¯ O B ⟷ (∃u. (u, x) ∈ A ∧ (u, y) ∈ B)" by auto

lemma CR_NF_conv:
  assumes "CR r" and "t ∈ NF r" and "(u, t) ∈ r⇧^↔⇧^*"
  shows "(u, t) ∈ r⇧^!"
using assms
unfolding CR_imp_conversionIff_join [OF ‹CR r›]
by (auto simp: NF_iff_no_step normalizability_def)
   (metis (mono_tags) converse_rtranclE joinE)

lemma NF_join_imp_reach:
  assumes "y ∈ NF A" and "(x, y) ∈ A⇧^↓"
  shows "(x, y) ∈ A⇧^*"
using assms by (auto simp: join_def) (metis NF_not_suc rtrancl_converseD)

lemma conversion_O_conversion [simp]:
  "A⇧^↔⇧^* O A⇧^↔⇧^* = A⇧^↔⇧^*"
  by (force simp: converse_def)

lemma trans_O_iff: "trans A ⟷ A O A ⊆ A" unfolding trans_def by auto
lemma refl_O_iff: "refl A ⟷ Id ⊆ A" unfolding refl_on_def by auto

lemma relpow_Suc: "r ^^ Suc n = r O r ^^ n"
  using relpow_add[of 1 n r] by auto

lemma converse_power: fixes r :: "'a rel" shows "(r¯)^^n = (r^^n)¯"
proof (induct n)
  case (Suc n)
  show ?case unfolding relpow.simps(2)[of _ "r¯"] relpow_Suc[of _ r]
    by (simp add: Suc converse_relcomp)
qed simp

lemma conversion_mono: "A ⊆ B ⟹ A⇧^↔⇧^* ⊆ B⇧^↔⇧^*"
by (auto simp: conversion_def intro!: rtrancl_mono)

lemma conversion_conversion_idemp [simp]: "(A⇧^↔⇧^*)⇧^↔⇧^* = A⇧^↔⇧^*"
  by auto

lemma lower_set_imp_not_SN_on:
  assumes "s ∈ X" "∀t ∈ X. ∃u ∈ X. (t,u) ∈ R" shows "¬ SN_on R {s}"
  by (meson SN_on_imp_on_minimal assms)


lemma SN_on_Image_rtrancl_iff[simp]: "SN_on R (R⇧^* `` X) ⟷ SN_on R X" (is "?l = ?r")
proof(intro iffI)
  assume "?l" show "?r" by (rule SN_on_subset2[OF _ ‹?l›], auto)
qed (fact SN_on_Image_rtrancl)

lemma O_mono1: "R ⊆ R' ⟹ S O R ⊆ S O R'" by auto
lemma O_mono2: "R ⊆ R' ⟹ R O T ⊆ R' O T" by auto

lemma rtrancl_O_shift: "(S O R)⇧^* O S = S O (R O S)⇧^*"
  (* regexp does not work, since R is of type 'a x 'b set, not 'a rel *)
proof(intro equalityI subrelI)
  fix x y
  assume "(x,y) ∈ (S O R)⇧^* O S"
  then obtain n where "(x,y) ∈ (S O R)^^n O S" by blast
  then show "(x,y) ∈ S O (R O S)⇧^*"
  proof(induct n arbitrary: y)
    case IH: (Suc n)
    then obtain z where xz: "(x,z) ∈ (S O R)^^n O S" and zy: "(z,y) ∈ R O S" by auto
    from IH.hyps[OF xz] zy have "(x,y) ∈ S O (R O S)⇧^* O R O S" by auto
    then show ?case by(fold trancl_unfold_right, auto)
  qed auto
next
  fix x y
  assume "(x,y) ∈ S O (R O S)⇧^*"
  then obtain n where "(x,y) ∈ S O (R O S)^^n" by blast
  then show "(x,y) ∈ (S O R)⇧^* O S"
  proof(induct n arbitrary: y)
    case IH: (Suc n)
    then obtain z where xz: "(x,z) ∈ S O (R O S)^^n" and zy: "(z,y) ∈ R O S" by auto
    from IH.hyps[OF xz] zy have "(x,y) ∈ ((S O R)⇧^* O S O R) O S" by auto
    from this[folded trancl_unfold_right]
    show ?case by (rule rev_subsetD[OF _ O_mono2], auto simp: O_assoc)
  qed auto
qed

lemma O_rtrancl_O_O: "R O (S O R)⇧^* O S = (R O S)⇧⁺"
  by (unfold rtrancl_O_shift trancl_unfold_left, auto)

lemma SN_on_subset_SN_terms:
  assumes SN: "SN_on R X" shows "X ⊆ {x. SN_on R {x}}"
proof(intro subsetI, unfold mem_Collect_eq)
  fix x assume x: "x ∈ X"
  show "SN_on R {x}" by (rule SN_on_subset2[OF _ SN], insert x, auto)
qed

lemma SN_on_Un2:
  assumes "SN_on R X" and "SN_on R Y" shows "SN_on R (X ∪ Y)"
  using assms by fast

lemma SN_on_UN:
  assumes "⋀x. SN_on R (X x)" shows "SN_on R (⋃x. X x)"
  using assms by fast

lemma Image_subsetI: "R ⊆ R' ⟹ R `` X ⊆ R' `` X" by auto

lemma SN_on_O_comm:
  assumes SN: "SN_on ((R :: ('a×'b) set) O (S :: ('b×'a) set)) (S `` X)"
  shows "SN_on (S O R) X"
proof
  fix seq :: "nat ⇒ 'b" assume seq0: "seq 0 ∈ X" and chain: "chain (S O R) seq"
  from SN have SN: "SN_on (R O S) ((R O S)⇧^* `` S `` X)" by simp
  { fix i a
    assume ia: "(seq i,a) ∈ S" and aSi: "(a,seq (Suc i)) ∈ R"
    have "seq i ∈ (S O R)⇧^* `` X"
    proof (induct i)
      case 0 from seq0 show ?case by auto
    next
      case (Suc i) with chain have "seq (Suc i) ∈ ((S O R)⇧^* O S O R) `` X" by blast
      also have "... ⊆ (S O R)⇧^* `` X" by (fold trancl_unfold_right, auto)
      finally show ?case.
    qed
    with ia have "a ∈ ((S O R)⇧^* O S) `` X" by auto
    then have a: "a ∈ ((R O S)⇧^*) `` S `` X" by (auto simp: rtrancl_O_shift)
    with ia aSi have False
    proof(induct "a" arbitrary: i rule: SN_on_induct[OF SN])
      case 1 show ?case by (fact a)
    next
      case IH: (2 a)
      from chain obtain b
      where *: "(seq (Suc i), b) ∈ S" "(b, seq (Suc (Suc i))) ∈ R" by auto
      with IH have ab: "(a,b) ∈ R O S" by auto
      with ‹a ∈ (R O S)⇧^* `` S `` X› have "b ∈ ((R O S)⇧^* O R O S) `` S `` X" by auto
      then have "b ∈ (R O S)⇧^* `` S `` X"
        by (rule rev_subsetD, intro Image_subsetI, fold trancl_unfold_right, auto)
      from IH.hyps[OF ab * this] IH.prems ab show False by auto
    qed
  }
  with chain show False by auto
qed

lemma SN_O_comm: "SN (R O S) ⟷ SN (S O R)"
  by (intro iffI; rule SN_on_O_comm[OF SN_on_subset2], auto)

lemma chain_mono: assumes "R' ⊆ R" "chain R' seq" shows "chain R seq"
  using assms by auto

context
  fixes S R
  assumes push: "S O R ⊆ R O S⇧^*"
begin

lemma rtrancl_O_push: "S⇧^* O R ⊆ R O S⇧^*"
proof-
  { fix n
    have "⋀s t. (s,t) ∈ S ^^ n O R ⟹ (s,t) ∈ R O S⇧^*"
    proof(induct n)
      case (Suc n)
        then obtain u where "(s,u) ∈ S" "(u,t) ∈ R O S⇧^*" unfolding relpow_Suc by blast
        then have "(s,t) ∈ S O R O S⇧^*" by auto
        also have "... ⊆ R O S⇧^* O S⇧^*" using push by blast
        also have "... ⊆ R O S⇧^*" by auto
        finally show ?case.
    qed auto
  }
  thus ?thesis by blast
qed

lemma rtrancl_U_push: "(S ∪ R)⇧^* = R⇧^* O S⇧^*"
proof(intro equalityI subrelI)
  fix x y
  assume "(x,y) ∈ (S ∪ R)⇧^*"
  also have "... ⊆ (S⇧^* O R)⇧^* O S⇧^*" by regexp
  finally obtain z where xz: "(x,z) ∈ (S⇧^* O R)⇧^*" and zy: "(z,y) ∈ S⇧^*" by auto
  from xz have "(x,z) ∈ R⇧^* O S⇧^*"
  proof (induct rule: rtrancl_induct)
    case (step z w)
      then have "(x,w) ∈ R⇧^* O S⇧^* O S⇧^* O R" by auto
      also have "... ⊆ R⇧^* O S⇧^* O R" by regexp
      also have "... ⊆ R⇧^* O R O S⇧^*" using rtrancl_O_push by auto
      also have "... ⊆ R⇧^* O S⇧^*" by regexp
      finally show ?case.
  qed auto
  with zy show "(x,y) ∈ R⇧^* O S⇧^*" by auto
qed regexp

lemma SN_on_O_push:
  assumes SN: "SN_on R X" shows "SN_on (R O S⇧^*) X"
proof
  fix seq
  have SN: "SN_on R (R⇧^* `` X)" using SN_on_Image_rtrancl[OF SN].
  moreover assume "seq (0::nat) ∈ X"
    then have "seq 0 ∈ R⇧^* `` X" by auto
  ultimately show "chain (R O S⇧^*) seq ⟹ False"
  proof(induct "seq 0" arbitrary: seq rule: SN_on_induct)
    case IH
    then have 01: "(seq 0, seq 1) ∈ R O S⇧^*"
          and 12: "(seq 1, seq 2) ∈ R O S⇧^*"
          and 23: "(seq 2, seq 3) ∈ R O S⇧^*" by (auto simp: eval_nat_numeral)
    then obtain s t
    where s: "(seq 0, s) ∈ R" and s1: "(s, seq 1) ∈ S⇧^*"
      and t: "(seq 1, t) ∈ R" and t2: "(t, seq 2) ∈ S⇧^*" by auto
    from s1 t have "(s,t) ∈ S⇧^* O R" by auto
    with rtrancl_O_push have st: "(s,t) ∈ R O S⇧^*" by auto
    from t2 23 have "(t, seq 3) ∈ S⇧^* O R O S⇧^*" by auto
    also from rtrancl_O_push have "... ⊆ R O S⇧^* O S⇧^*" by blast
    finally have t3: "(t, seq 3) ∈ R O S⇧^*" by regexp
    let ?seq = "λi. case i of 0 ⇒ s | Suc 0 ⇒ t | i ⇒ seq (Suc i)"
    show ?case
    proof(rule IH)
      from s show "(seq 0, ?seq 0) ∈ R" by auto
      show "chain (R O S⇧^*) ?seq"
      proof (intro allI)
        fix i show "(?seq i, ?seq (Suc i)) ∈ R O S⇧^*"
        proof (cases i)
          case 0 with st show ?thesis by auto
        next
          case (Suc i) with t3 IH show ?thesis by (cases i, auto simp: eval_nat_numeral)
        qed
      qed
    qed
  qed
qed

lemma SN_on_Image_push:
  assumes SN: "SN_on R X" shows "SN_on R (S⇧^* `` X)"
proof-
  { fix n
    have "SN_on R ((S^^n) `` X)"
    proof(induct n)
      case 0 from SN show ?case by auto
      case (Suc n)
        from SN_on_O_push[OF this] have "SN_on (R O S⇧^*) ((S ^^ n) `` X)".
        from SN_on_Image[OF this]
        have "SN_on (R O S⇧^*) ((R O S⇧^*) `` (S ^^ n) `` X)".
        then have "SN_on R ((R O S⇧^*) `` (S ^^ n) `` X)" by (rule SN_on_mono, auto)
        from SN_on_subset2[OF Image_mono[OF push subset_refl] this]
        have "SN_on R (R `` (S ^^ Suc n) `` X)" by (auto simp: relcomp_Image)
        then show ?case by fast
    qed
  }
  then show ?thesis by fast
qed

end

lemma not_SN_onI[intro]: "f 0 ∈ X ⟹ chain R f ⟹ ¬ SN_on R X"
  by (unfold SN_on_def not_not, intro exI conjI)
lemma shift_comp[simp]: "shift (f ∘ seq) n = f ∘ (shift seq n)" by auto

lemma Id_on_union: "Id_on (A ∪ B) = Id_on A ∪ Id_on B" unfolding Id_on_def by auto

lemma relpow_union_cases: "(a,d) ∈ (A ∪ B)^^n ⟹ (a,d) ∈ B^^n ∨ (∃ b c k m. (a,b) ∈ B^^k ∧ (b,c) ∈ A ∧ (c,d) ∈ (A ∪ B)^^m ∧ n = Suc (k + m))"
proof (induct n arbitrary: a d)
  case (Suc n a e)
  let ?AB = "A ∪ B"
  from Suc(2) obtain b where ab: "(a,b) ∈ ?AB" and be: "(b,e) ∈ ?AB^^n" by (rule relpow_Suc_E2)
  from ab
  show ?case
  proof
    assume "(a,b) ∈ A"
    show ?thesis
    proof (rule disjI2, intro exI conjI)
      show "Suc n = Suc (0 + n)" by simp
      show "(a,b) ∈ A" by fact
    qed (insert be, auto)
  next
    assume ab: "(a,b) ∈ B"
    from Suc(1)[OF be]
    show ?thesis
    proof
      assume "(b,e) ∈ B ^^ n"
      with ab show ?thesis
        by (intro disjI1 relpow_Suc_I2)
    next
      assume "∃ c d k m. (b, c) ∈ B ^^ k ∧ (c, d) ∈ A ∧ (d, e) ∈ ?AB ^^ m ∧ n = Suc (k + m)"
      then obtain c d k m where "(b, c) ∈ B ^^ k" and *: "(c, d) ∈ A" "(d, e) ∈ ?AB ^^ m" "n = Suc (k + m)" by blast
      with ab have ac: "(a,c) ∈ B ^^ (Suc k)" by (intro relpow_Suc_I2)
      show ?thesis
        by (intro disjI2 exI conjI, rule ac, (rule *)+, simp add: *)
    qed
  qed
qed simp

lemma trans_refl_imp_rtrancl_id:
  assumes "trans r" "refl r"
  shows "r⇧^* = r"
proof
  show "r⇧^* ⊆ r"
  proof
    fix x y
    assume "(x,y) ∈ r⇧^*"
    thus "(x,y) ∈ r"
      by (induct, insert assms, unfold refl_on_def trans_def, blast+)
  qed
qed regexp

lemma trans_refl_imp_O_id:
  assumes "trans r" "refl r"
  shows "r O r = r"
proof(intro equalityI)
  show "r O r ⊆ r" by(fact trans_O_subset[OF assms(1)])
  have "r ⊆ r O Id" by auto
  moreover have "Id ⊆ r" by(fact assms(2)[unfolded refl_O_iff])
  ultimately show "r ⊆ r O r" by auto
qed

lemma relcomp3_I:
  assumes "(t, u) ∈ A" and "(s, t) ∈ B" and "(u, v) ∈ B"
  shows "(s, v) ∈ B O A O B"
  using assms by blast

lemma relcomp3_transI:
  assumes "trans B" and "(t, u) ∈ B O A O B" and "(s, t) ∈ B" and "(u, v) ∈ B"
  shows "(s, v) ∈ B O A O B"
using assms by (auto simp: trans_def intro: relcomp3_I)

lemmas converse_inward = rtrancl_converse[symmetric] converse_Un converse_UNION converse_relcomp
  converse_converse converse_Id

lemma qc_SN_relto_iff:
  assumes "r O s ⊆ s O (s ∪ r)⇧^*"
  shows "SN (r⇧^* O s O r⇧^*) = SN s"
proof -
  from converse_mono [THEN iffD2 , OF assms]
  have *: "s¯ O r¯ ⊆ (s¯ ∪ r¯)⇧^* O s¯" unfolding converse_inward .
  have "(r⇧^* O s O r⇧^*)¯ = (r¯)⇧^* O s¯ O (r¯)⇧^*"
    by (simp only: converse_relcomp O_assoc rtrancl_converse)
  with qc_wf_relto_iff [OF *]
  show ?thesis by (simp add: SN_iff_wf)
qed

lemma conversion_empty [simp]: "conversion {} = Id"
  by (auto simp: conversion_def)

lemma symcl_idemp [simp]: "(r⇧^↔)⇧^↔ = r⇧^↔" by auto

end